minor script refactoring, streamlined settings files, starter files for scripts

WolframPfeifer · WolframPfeifer · commit 8796620b2ff4 · 2024-09-22T00:41:27.000+02:00
diff --git a/src/main/java/de/wiesler/Sorter.java b/src/main/java/de/wiesler/Sorter.java
@@ -24,23 +24,25 @@ private static SampleParameters sample(int[] values, int begin, int end, Storage
         /*@ assert sample0: \dl_seqPerm(\dl_seq_def_workaround(begin, end, values), \old(\dl_seq_def_workaround(begin, end, values))) \by {
                 oss;
                 assert "seqDef{int j;}(begin, end, any::select(heap, values, arr(j))) = seqDef{int j;}(begin, end, any::select(heapAfter_SampleParameters, values, arr(j)))" \by {
-                    auto;
+                    tryclose branch steps=4000;
                 }
-                auto;
+                tryclose branch steps=4000;
             }
           @*/
 
         Functions.select_n(values, begin, end, parameters.num_samples);
         /*@ assert sample1: \dl_seqPerm(\dl_seq_def_workaround(begin, end, values), \old(\dl_seq_def_workaround(begin, end, values))) \by {
-                auto;
+                tryclose branch steps=4000;
             };
           @*/
 
         //@ ghost \seq before_sort = \dl_seq_def_workaround(begin, end, values);
         sort(values, begin, begin + parameters.num_samples, storage);
         /*@ assert sample2: \dl_seqPerm(\dl_seq_def_workaround(begin, end, values), before_sort) \by {
                 oss;
-                assert "wellFormed(heapAfter_sort)" \by { auto; }                   // this is missing in the original proof by JW, but somehow needed here (automode does not find it)
+                assert "wellFormed(heapAfter_sort)" \by {
+                    tryclose branch steps=4000;
+                }                   // this is missing in the original proof by JW, but somehow needed here (automode does not find it)
 
                 // TODO: not very robust: "self" is frequently renamed (e.g. to self_25)
                 let @numSamplesFinal="int::final(self, de.wiesler.SampleParameters::$num_samples)";
@@ -49,15 +51,15 @@ private static SampleParameters sample(int[] values, int begin, int end, Storage
                                 seqDef{int j;}(add(begin, @numSamplesFinal), end, any::select(heapAfter_select_n, values, arr(j))))" \by {
                     assert "seqDef{int j;}(begin + @numSamplesFinal, end, any::select(heapAfter_select_n, values, arr(j)))
                           = seqDef{int j;}(begin + @numSamplesFinal, end, values[j]@heapAfter_sort)" \by {
-                        auto;
+                        tryclose branch steps=4000;
                     }
-                    auto;
+                    tryclose branch steps=4000;
                 }
 
                 //rule seqPermConcatFW on="seqPerm(seqDef{int j;}(begin, add(int::_, int::_)), seqDef{int j;}(begin, add(int::_, int::_)))";            // not needed
                 rule seqDef_split on="seqDef{int j;}(begin, end, any::select(heapAfter_sort, values, arr(j)))" inst_idx="begin+@numSamplesFinal";
                 rule seqDef_split on="seqDef{int j;}(begin, end, any::select(heapAfter_select_n, values, arr(j)))" inst_idx="begin+@numSamplesFinal" occ=2;
-                auto;
+                tryclose branch steps=4000;
             }
           @*/
 
@@ -460,10 +462,6 @@ private static void sample_sort_recurse_on(int[] values, int begin, int end, Sto
                 rule seqDef_split on="seqDef{int uSub1;}(@middle, end, any::select(heap, values, arr(uSub1)))" inst_idx="@middleSucc";
                 rule seqDef_split on="seqDef{int uSub1;}(@middle, end, any::select(anon(Heap::_, LocSet::_, Heap::_), values, arr(uSub1)))" inst_idx="@middleSucc";
 
-                // TODO: same problem as always: does not work
-                //auto steps=1000 dependencies=false classAxioms=false modelSearch=false expandQueries=false;
-                //leave;
-
                 // workaround: this also affects all branches visited afterwards!
                 set key="CLASS_AXIOM_OPTIONS_KEY" value="CLASS_AXIOM_OFF";
                 set key="DEP_OPTIONS_KEY" value="DEP_OFF";
@@ -734,8 +732,7 @@ private static void sample_sort(int[] values, int begin, int end, Storage storag
             }
         }
 
-        /*@ assert sortednessFromPartitionSorted(values, begin, end, bucket_starts, num_buckets);
-          @*/
+        //@ assert sortednessFromPartitionSorted(values, begin, end, bucket_starts, num_buckets);
     }
 
     /*@ public normal_behaviour
@@ -757,10 +754,6 @@ public static void fallback_sort(int[] values, int begin, int end) {
                 oss;
                 rule allRight;
 
-                // of these two, always only the first one works for some reason:
-                //expand on="de.wiesler.Functions.countElement(values, begin, end, element_0)";
-                //expand on="de.wiesler.Functions.countElement(values, begin, end, element_0)@heapAfter_insertion_sort";
-
                 expand on="de.wiesler.Functions::countElement(heap, values, begin, end, element_0)";
                 expand on="de.wiesler.Functions::countElement(heapAfter_insertion_sort, values, begin, end, element_0)";
                 rule seqPermCountsInt;
@@ -776,15 +769,13 @@ public static void fallback_sort(int[] values, int begin, int end) {
                 assert "bsum{int uSub1;}(0, end - begin, \if (values[uSub1 + begin] = element_0) \then (1) \else (0))
                       = bsum{int iv;}(0, end - begin, \if (seqDef{int j;}(begin, end, values[j])[iv] = element_0) \then (1) \else (0))";
 
-                // None of those is able close the goal for some reason. In the GUI, it works fine.
-                // auto;
-                // Not sure if the parameters actually affect anything ...
-                //auto classAxioms=true expandQueries=true modelSearch=true dependencies=true proofSplitting=true steps=2000;
-
-                // workaround (more detailed params not supported at the moment)
+                // workaround: this also affects all branches visited afterwards!
+                set key="CLASS_AXIOM_OPTIONS_KEY" value="CLASS_AXIOM_DELAYED";
+                set key="DEP_OPTIONS_KEY" value="DEP_ON";
+                set key="NON_LIN_ARITH_OPTIONS_KEY" value="NON_LIN_ARITH_DEF_OPS";
+                set key="QUERYAXIOM_OPTIONS_KEY" value="QUERYAXIOM_OFF";
                 tryclose branch steps=2000;
-            };
-          @*/
+            }; */
     }
 
     /*@ model_behaviour
@@ -838,7 +829,7 @@ public static void insertion_sort(int[] values, int begin, int end) {
                         auto steps=7000 classAxioms=true dependency=false modelSearch=false expandQueries=false;
                     }
                     auto steps=200 add_applyEqReverse=high classAxioms=false dependency=false modelSearch=false expandQueries=false;
-                } @*/
+                } */
 
             /*@ loop_invariant hole == i + 1;
               @ loop_invariant begin-1 <= i < k;
@@ -858,7 +849,7 @@ public static void insertion_sort(int[] values, int begin, int end) {
                 // TODO: there seems to be a bug in interplay of loop scopes and script ("program variable h not known") -> make sure to use loop transformation rule here!
                 /*@ assert insSort1: \dl_seqPerm(seqUpd(\dl_seq_def_workaround(begin, end, values), hole - begin, value), \old(\dl_seq_def_workaround(begin, end, values))) \by {
                         leave;
-                    } @*/
+                    } */
                 /* @ assert insSort1: \dl_seqPerm(seqUpd(\dl_seq_def_workaround(begin, end, values), hole - begin, value), \old(\dl_seq_def_workaround(begin, end, values))) \by {
 
                     oss;
@@ -890,8 +881,8 @@ public static void insertion_sort(int[] values, int begin, int end) {
                     set key="DEP_OPTIONS_KEY" value="DEP_OFF";
                     set key="NON_LIN_ARITH_OPTIONS_KEY" value="NON_LIN_ARITH_DEF_OPS";
                     set key="QUERYAXIOM_OPTIONS_KEY" value="QUERYAXIOM_OFF";
-                    tryclose;
-                } @*/
+                    tryclose branch;
+                } */
             }
 
             // @ ghost \dl_seq tmp = \dl_seq_def_workaround(begin, end, values);
@@ -902,14 +893,14 @@ public static void insertion_sort(int[] values, int begin, int end) {
             /* @ assert insSort2: \dl_seqPerm(\dl_seq_def_workaround(begin, end, values), \old(\dl_seq_def_workaround(begin, end, values))) \by {
                     assert \dl_seq_def_workaround(begin, end, values) = seqUpd(tmp, begin * -1 + hole, values[k]);
                     auto;
-                } @*/
+                } */
         }
 
         /* @ assert insSort3: true \by {
 
                 // the last branch still needs quite heavy automation ...
                 auto steps=11000 dependency=false classAxioms=false expandQueries=false modelSearch=false;
-            } @*/
+            } */
     }
 
     /*@ public normal_behaviour
@@ -961,21 +952,21 @@ public static void sort(int[] values) {
         /*@ assert sort0: \disjoint(storage.allArrays, values[*]) \by {
                 oss;
                 rule disjointToElementOf;
-                auto;
-            }; @*/
+                tryclose branch steps=2000;
+            }; */
         sort(values, 0, values.length, storage);
         /*@ assert sort1: \dl_seqPerm(\dl_array2seq(values), \old(\dl_array2seq(values))) \by {
                 oss;
                 assert "seqDef{int u;}(0, values.length, any::select(heap, values, arr(u))) = seqDef{int j;}(0, values.length, any::select(heapAfter_Storage, values, arr(j)))" \by {
-                    auto;
+                    tryclose branch steps=2000;
                 }
-                auto;
-            } @*/
+                tryclose branch steps=2000;
+            } */
         /*@ assert sort2: \dl_assignable(\old(\dl_heap()), values[*]) \by {
                 oss;
                 rule assignableDefinition;
                 macro "simp-heap";
-                auto;
-            } @*/
+                tryclose branch steps=2000;
+            } */
     }
 }
diff --git a/src/main/key/project.key b/src/main/key/project.key
@@ -1,47 +1,47 @@
 \settings {
 "#Proof-Settings-Config-File
 #Thu May 05 18:49:23 CEST 2022
-[NewSMT]NoTypeHierarchy=false
+[Choice]DefaultChoices=JavaCard-JavaCard\\:on , Strings-Strings\\:on , assertions-assertions\\:safe , bigint-bigint\\:on , finalFields-finalFields\\:immutable , floatRules-floatRules\\:strictfpOnly , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , integerSimplificationRules-integerSimplificationRules\\:full , javaLoopTreatment-javaLoopTreatment\\:efficient , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , methodExpansion-methodExpansion\\:modularOnly , modelFields-modelFields\\:treatAsAxiom , moreSeqRules-moreSeqRules\\:on , permissions-permissions\\:off , programRules-programRules\\:Java , reach-reach\\:on , runtimeExceptions-runtimeExceptions\\:ban , sequences-sequences\\:on , wdChecks-wdChecks\\:off , wdOperator-wdOperator\\:L
 [Labels]UseOriginLabels=true
-[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
+[NewSMT]Axiomatisations=false
+[NewSMT]NoTypeHierarchy=false
 [NewSMT]Presburger=false
-[SMTSettings]invariantForall=false
-[Strategy]ActiveStrategy=JavaCardDLStrategy
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
-[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
-[Choice]DefaultChoices=JavaCard-JavaCard\\:on , Strings-Strings\\:on , assertions-assertions\\:safe , bigint-bigint\\:on , finalFields-finalFields\\:immutable , floatRules-floatRules\\:strictfpOnly , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , integerSimplificationRules-integerSimplificationRules\\:full , javaLoopTreatment-javaLoopTreatment\\:efficient , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , methodExpansion-methodExpansion\\:modularOnly , modelFields-modelFields\\:treatAsAxiom , moreSeqRules-moreSeqRules\\:on , permissions-permissions\\:off , programRules-programRules\\:Java , reach-reach\\:on , runtimeExceptions-runtimeExceptions\\:ban , sequences-sequences\\:on , wdChecks-wdChecks\\:off , wdOperator-wdOperator\\:L
-[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET
-[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
-[SMTSettings]UseBuiltUniqueness=false
+[NewSMT]identifier=OPEN
+[NewSMT]sqrtSMTTranslation=SMT
 [SMTSettings]explicitTypeHierarchy=false
 [SMTSettings]instantiateHierarchyAssumptions=true
-[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
+[SMTSettings]integersMaximum=2147483645
+[SMTSettings]integersMinimum=-2147483645
+[SMTSettings]invariantForall=false
+[SMTSettings]maxGenericSorts=2
 [SMTSettings]SelectedTaclets=
-[StrategyProperty]DEP_OPTIONS_KEY=DEP_OFF
-[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
-[Strategy]MaximumNumberOfAutomaticApplications=10000
-[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
-[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED
+[SMTSettings]UseBuiltUniqueness=false
 [SMTSettings]useConstantsForBigOrSmallIntegers=true
-[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
-[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
-[Strategy]Timeout=-1
-[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
-[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
 [SMTSettings]useUninterpretedMultiplication=true
-[NewSMT]sqrtSMTTranslation=SMT
+[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
 [StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
+[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED
+[StrategyProperty]DEP_OPTIONS_KEY=DEP_OFF
+[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
+[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET
 [StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
-[NewSMT]identifier=OPEN
-[SMTSettings]maxGenericSorts=2
+[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
+[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
 [StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
-[NewSMT]Axiomatisations=false
+[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
+[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
+[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
 [StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
-[SMTSettings]integersMinimum=-2147483645
+[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
+[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
+[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
 [StrategyProperty]VBT_PHASE=VBT_SYM_EX
-[SMTSettings]integersMaximum=2147483645
+[Strategy]ActiveStrategy=JavaCardDLStrategy
+[Strategy]MaximumNumberOfAutomaticApplications=10000
+[Strategy]Timeout=-1
 "
 }
 
diff --git a/src/main/script/fallback_sort_script_entry.proof b/src/main/script/fallback_sort_script_entry.proof
@@ -10,14 +10,14 @@
 [NewSMT]Presburger=false
 [NewSMT]identifier=OPEN
 [NewSMT]sqrtSMTTranslation=SMT
-[SMTSettings]SelectedTaclets=
-[SMTSettings]UseBuiltUniqueness=false
 [SMTSettings]explicitTypeHierarchy=false
 [SMTSettings]instantiateHierarchyAssumptions=true
 [SMTSettings]integersMaximum=2147483645
 [SMTSettings]integersMinimum=-2147483645
 [SMTSettings]invariantForall=false
 [SMTSettings]maxGenericSorts=2
+[SMTSettings]SelectedTaclets=
+[SMTSettings]UseBuiltUniqueness=false
 [SMTSettings]useConstantsForBigOrSmallIntegers=true
 [SMTSettings]useUninterpretedMultiplication=true
 [StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
diff --git a/src/main/script/sample_script_entry.proof b/src/main/script/sample_script_entry.proof
@@ -0,0 +1,67 @@
+\profile "Java Profile";
+
+\settings {
+"#Proof-Settings-Config-File
+#Sat Sep 21 14:23:21 CEST 2024
+[Choice]DefaultChoices=JavaCard-JavaCard\\:on , Strings-Strings\\:on , assertions-assertions\\:safe , bigint-bigint\\:on , floatRules-floatRules\\:strictfpOnly , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , integerSimplificationRules-integerSimplificationRules\\:full , javaLoopTreatment-javaLoopTreatment\\:efficient , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , methodExpansion-methodExpansion\\:modularOnly , modelFields-modelFields\\:treatAsAxiom , moreSeqRules-moreSeqRules\\:on , permissions-permissions\\:off , programRules-programRules\\:Java , reach-reach\\:on , runtimeExceptions-runtimeExceptions\\:ban , sequences-sequences\\:on , wdChecks-wdChecks\\:off , wdOperator-wdOperator\\:L , finalFields-finalFields\\:immutable
+[Labels]UseOriginLabels=true
+[NewSMT]Axiomatisations=false
+[NewSMT]NoTypeHierarchy=false
+[NewSMT]Presburger=false
+[NewSMT]identifier=OPEN
+[NewSMT]sqrtSMTTranslation=SMT
+[SMTSettings]explicitTypeHierarchy=false
+[SMTSettings]instantiateHierarchyAssumptions=true
+[SMTSettings]integersMaximum=2147483645
+[SMTSettings]integersMinimum=-2147483645
+[SMTSettings]invariantForall=false
+[SMTSettings]maxGenericSorts=2
+[SMTSettings]SelectedTaclets=
+[SMTSettings]UseBuiltUniqueness=false
+[SMTSettings]useConstantsForBigOrSmallIntegers=true
+[SMTSettings]useUninterpretedMultiplication=true
+[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
+[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
+[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED
+[StrategyProperty]DEP_OPTIONS_KEY=DEP_OFF
+[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
+[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET
+[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
+[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
+[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
+[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
+[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
+[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
+[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_RESTRICTED
+[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
+[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
+[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
+[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
+[StrategyProperty]VBT_PHASE=VBT_SYM_EX
+[Strategy]ActiveStrategy=JavaCardDLStrategy
+[Strategy]MaximumNumberOfAutomaticApplications=10000
+[Strategy]Timeout=-1
+"
+}
+
+\javaSource "../java";
+
+\proofObligation "#Proof Obligation Settings
+#Sat Sep 21 14:23:21 CEST 2024
+class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
+contract=de.wiesler.Sorter[de.wiesler.Sorter\\:\\:sample([I,int,int,de.wiesler.Storage)].JML normal_behavior operation contract.0
+name=de.wiesler.Sorter[de.wiesler.Sorter\\:\\:sample([I,int,int,de.wiesler.Storage)].JML normal_behavior operation contract.0
+";
+
+\proof {
+(keyLog "0" (keyUser "wolfram" ) (keyVersion "7336f2d86e"))
+
+(autoModeTime "0")
+
+(branch "dummy ID"
+ (opengoal " ")
+)
+}
diff --git a/src/main/script/sample_sort_recurse_on_script_entry.proof b/src/main/script/sample_sort_recurse_on_script_entry.proof
diff --git a/src/main/script/sort_script_entry.proof b/src/main/script/sort_script_entry.proof
