Skip to content

Commit e1bb713

Browse files
WolframPfeiferWolframPfeifer
committed
refactored proof for prettier script
1 parent 3ee1ff7 commit e1bb713

File tree

1 file changed

+46
-75
lines changed

1 file changed

+46
-75
lines changed

‎src/main/java/de/wiesler/Sorter.java‎

Lines changed: 46 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -480,16 +480,13 @@ private static void sample_sort_recurse_on(int[] values, int begin, int end, Sto
480480
macro "simp-int";
481481
witness "\forall int b; (0 <= b & b <= bucket -> de.wiesler.Functions::isSortedSlice(Heap::_, int[]::_, int::_, int::_) = TRUE)" as="b_0";
482482
483-
cut "b_0 != bucket";
484-
branches "push";
485-
branches "select" branch="show";
483+
assert "b_0 != bucket" \by {
486484
set key="CLASS_AXIOM_OPTIONS_KEY" value="CLASS_AXIOM_DELAYED";
487485
set key="DEP_OPTIONS_KEY" value="DEP_ON";
488486
set key="NON_LIN_ARITH_OPTIONS_KEY" value="NON_LIN_ARITH_DEF_OPS";
489487
set key="QUERYAXIOM_OPTIONS_KEY" value="QUERYAXIOM_OFF";
490488
tryclose branch steps=200;
491-
branches "select" branch="use";
492-
branches "pop";
489+
}
493490
494491
expand on="de.wiesler.Sorter::allBucketsInRangeSorted(Heap::_, values, begin, end, bucket_starts, num_buckets, 0, bucket)";
495492
oss;
@@ -516,12 +513,9 @@ private static void sample_sort_recurse_on(int[] values, int begin, int end, Sto
516513
expand on="de.wiesler.Sorter::isBucketPartitioned(heap, values, begin, end, int::_, int::_)";
517514
expand on="de.wiesler.Sorter::isBucketPartitioned(Heap::_, values, begin, end, int::_, int::_)";
518515
519-
cut "0 <= b_0 & b_0 < num_buckets";
520-
branches "push";
521-
branches "select" branch="show";
516+
assert "0 <= b_0 & b_0 < num_buckets" \by {
522517
tryclose branch steps=1000;
523-
branches "select" branch="use";
524-
branches "pop";
518+
}
525519
526520
macro "nosplit-prop";
527521
macro "simp-int";
@@ -532,105 +526,83 @@ private static void sample_sort_recurse_on(int[] values, int begin, int end, Sto
532526
rule allRight;
533527
rule allLeftHide on="\forall int b; __" inst_t="b_0";
534528
535-
cut "b_0 = bucket";
536-
branches "push";
537-
branches "select" branch="show";
529+
assert "b_0 = bucket" \by {
538530
539-
cut "int::select(anon(heap, union(LocSet::final(storage, de.wiesler.Storage::$allArrays), arrayRange(values, add(begin, int::select(heap, bucket_starts, arr(bucket))), add(add(Z(neglit(1(#))), begin), int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))))), anonOut_heap<<anonHeapFunction>>), values, arr(i_0)) = int::select(heap, values, arr(i_0))";
540-
branches "push";
541-
branches "select" branch="show";
531+
assert "int::select(anon(heap, union(LocSet::final(storage, de.wiesler.Storage::$allArrays), arrayRange(values, add(begin, int::select(heap, bucket_starts, arr(bucket))), add(add(Z(neglit(1(#))), begin), int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))))), anonOut_heap<<anonHeapFunction>>), values, arr(i_0)) = int::select(heap, values, arr(i_0))" \by {
542532
set key="CLASS_AXIOM_OPTIONS_KEY" value="CLASS_AXIOM_OFF";
543533
set key="DEP_OPTIONS_KEY" value="DEP_OFF";
544534
set key="NON_LIN_ARITH_OPTIONS_KEY" value="NON_LIN_ARITH_DEF_OPS";
545535
set key="QUERYAXIOM_OPTIONS_KEY" value="QUERYAXIOM_OFF";
546536
tryclose branch steps=2000;
547-
branches "select" branch="use";
548-
branches "pop";
537+
}
549538
550539
rule impLeft occ=1;
551540
tryclose branch steps=200;
552541
553-
cut "b_0 > bucket";
554-
branches "push";
555-
branches "select" branch="use"; // branches swapped!!!
542+
assert "b_0 > bucket" \by {
543+
rule applyEq on="int::select(anon(heap, union(LocSet::final(storage, de.wiesler.Storage::$allArrays), arrayRange(values, add(begin, int::select(heap, bucket_starts, arr(bucket))), add(add(Z(neglit(1(#))), begin), int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))))), anonOut_heap<<anonHeapFunction>>), values, arr(i_0))" occ=1;
544+
545+
rule allLeft inst_t="i_0";
546+
rule impLeft on="__ -> (\forall int j; __)";
547+
tryclose branch steps=1000;
548+
549+
rule allLeftHide on="(\forall int j; __)" inst_t="j_0" occ=0;
550+
rule impLeft occ=0;
551+
tryclose branch steps=1000;
556552
557-
cut "int::select(anon(heap, union(LocSet::final(storage, de.wiesler.Storage::$allArrays), arrayRange(values, add(begin, int::select(heap, bucket_starts, arr(bucket))), add(add(Z(neglit(1(#))), begin), int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))))), anonOut_heap), values, arr(j_0)) = int::select(heap, values, arr(j_0))";
558-
branches "push";
559-
branches "select" branch="show";
560-
macro "simp-heap";
553+
assert "begin + bucket_starts[bucket] <= j_0 & j_0 < begin + bucket_starts[bucket + 1]" \by {
561554
set key="CLASS_AXIOM_OPTIONS_KEY" value="CLASS_AXIOM_OFF";
562555
set key="DEP_OPTIONS_KEY" value="DEP_OFF";
563556
set key="NON_LIN_ARITH_OPTIONS_KEY" value="NON_LIN_ARITH_DEF_OPS";
564557
set key="QUERYAXIOM_OPTIONS_KEY" value="QUERYAXIOM_OFF";
565-
tryclose branch steps=500;
566-
branches "select" branch="use";
567-
branches "pop";
558+
tryclose branch steps=10000;
559+
}
568560
561+
// TODO: for the schemaVariable x, it is necessary to state the exact next (!) name that is free!!!
562+
rule seqPermForall inst_phi="lt(int::select(heap, values, arr(i_0)), (int)x_6)" assumes="seqPerm(seqDef{int j;}(begin + bucket_starts[bucket], int::_, any::_), Seq::_)==>";
569563
570-
rule allLeftHide inst_t="i_0";
571-
rule impLeft on="__ -> (\forall int j; __)";
572-
tryclose branch steps=1000;
573-
rule allLeftHide inst_t="j_0";
574-
tryclose branch steps=1000;
564+
rule equiv_left;
565+
rule allLeftHide inst_t="j_0 - (begin + bucket_starts[bucket])" occ=0;
566+
tryclose branch steps=2000;
575567
576-
branches "select" branch="show"; // branches swapped!!!
577-
branches "pop";
568+
witness "\forall int iv; (__ -> lt(int::select(heap, values, arr(i_0)), (int)(any::seqGet(seqDef{int j;}(add(begin, int::select(heap, bucket_starts, arr(bucket))), add(begin, int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))), int::select(heap, values, arr(j))), iv))))" as="iv_0";
578569
579-
rule applyEq on="int::select(anon(heap, union(LocSet::final(storage, de.wiesler.Storage::$allArrays), arrayRange(values, add(begin, int::select(heap, bucket_starts, arr(bucket))), add(add(Z(neglit(1(#))), begin), int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))))), anonOut_heap<<anonHeapFunction>>), values, arr(i_0))" occ=1;
580570
581-
rule allLeft inst_t="i_0";
582-
rule impLeft on="__ -> (\forall int j; __)";
583-
tryclose branch steps=1000;
571+
rule allLeftHide inst_t="i_0";
572+
rule impLeft on="__ -> (\forall int j; __)";
573+
tryclose branch steps=600;
584574
585-
rule allLeftHide on="(\forall int j; __)" inst_t="j_0" occ=0;
586-
rule impLeft occ=0;
587-
tryclose branch steps=1000;
575+
rule allLeftHide inst_t="iv_0 + begin + bucket_starts[bucket]";
576+
577+
tryclose branch steps=2000;
578+
}
588579
589-
cut "begin + bucket_starts[bucket] <= j_0 & j_0 < begin + bucket_starts[bucket + 1]";
590-
branches "push";
591-
branches "select" branch="show";
580+
assert "int::select(anon(heap, union(LocSet::final(storage, de.wiesler.Storage::$allArrays), arrayRange(values, add(begin, int::select(heap, bucket_starts, arr(bucket))), add(add(Z(neglit(1(#))), begin), int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))))), anonOut_heap), values, arr(j_0)) = int::select(heap, values, arr(j_0))" \by {
581+
macro "simp-heap";
592582
set key="CLASS_AXIOM_OPTIONS_KEY" value="CLASS_AXIOM_OFF";
593583
set key="DEP_OPTIONS_KEY" value="DEP_OFF";
594584
set key="NON_LIN_ARITH_OPTIONS_KEY" value="NON_LIN_ARITH_DEF_OPS";
595585
set key="QUERYAXIOM_OPTIONS_KEY" value="QUERYAXIOM_OFF";
596-
tryclose branch steps=10000;
597-
branches "select" branch="use";
598-
branches "pop";
599-
600-
// TODO: for the schemaVariable x, it is necessary to state the exact next (!) name that is free!!!
601-
rule seqPermForall inst_phi="lt(int::select(heap, values, arr(i_0)), (int)x_6)" assumes="seqPerm(seqDef{int j;}(begin + bucket_starts[bucket], int::_, any::_), Seq::_)==>";
602-
603-
rule equiv_left;
604-
rule allLeftHide inst_t="j_0 - (begin + bucket_starts[bucket])" occ=0;
605-
tryclose branch steps=2000;
606-
607-
witness "\forall int iv; (__ -> lt(int::select(heap, values, arr(i_0)), (int)(any::seqGet(seqDef{int j;}(add(begin, int::select(heap, bucket_starts, arr(bucket))), add(begin, int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))), int::select(heap, values, arr(j))), iv))))" as="iv_0";
608-
609-
610-
rule allLeftHide inst_t="i_0";
611-
rule impLeft on="__ -> (\forall int j; __)";
612-
tryclose branch steps=600;
613-
614-
rule allLeftHide inst_t="iv_0 + begin + bucket_starts[bucket]";
615-
616-
tryclose branch steps=2000;
586+
tryclose branch steps=500;
587+
}
617588
618-
branches "select" branch="use";
619-
branches "pop";
589+
rule allLeftHide inst_t="i_0";
590+
rule impLeft on="__ -> (\forall int j; __)";
591+
tryclose branch steps=1000;
592+
rule allLeftHide inst_t="j_0";
593+
tryclose branch steps=1000;
594+
}
620595
621596
// TODO: seems that abbreviations do not work in cuts ...
622597
// let @vjAtLargerHeap="int::select(anon(heap, union(LocSet::final(storage, de.wiesler.Storage::$allArrays), arrayRange(values, add(begin, int::select(heap, bucket_starts, arr(bucket))), add(add(Z(neglit(1(#))), begin), int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))))), anonOut_heap), values, arr(j_0))";
623598
624-
cut "int::select(anon(heap, union(LocSet::final(storage, de.wiesler.Storage::$allArrays), arrayRange(values, add(begin, int::select(heap, bucket_starts, arr(bucket))), add(add(Z(neglit(1(#))), begin), int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))))), anonOut_heap), values, arr(j_0)) = int::select(heap, values, arr(j_0))";
625-
branches "push";
626-
branches "select" branch="show";
599+
assert "int::select(anon(heap, union(LocSet::final(storage, de.wiesler.Storage::$allArrays), arrayRange(values, add(begin, int::select(heap, bucket_starts, arr(bucket))), add(add(Z(neglit(1(#))), begin), int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))))), anonOut_heap), values, arr(j_0)) = int::select(heap, values, arr(j_0))" \by {
627600
set key="CLASS_AXIOM_OPTIONS_KEY" value="CLASS_AXIOM_OFF";
628601
set key="DEP_OPTIONS_KEY" value="DEP_OFF";
629602
set key="NON_LIN_ARITH_OPTIONS_KEY" value="NON_LIN_ARITH_DEF_OPS";
630603
set key="QUERYAXIOM_OPTIONS_KEY" value="QUERYAXIOM_OFF";
631604
tryclose branch steps=400;
632-
branches "select" branch="use";
633-
branches "pop";
605+
}
634606
635607
rule applyEq on="int::select(anon(heap, union(LocSet::final(storage, de.wiesler.Storage::$allArrays), arrayRange(values, add(begin, int::select(heap, bucket_starts, arr(bucket))), add(add(Z(neglit(1(#))), begin), int::select(heap, bucket_starts, arr(add(Z(1(#)), bucket)))))), anonOut_heap), values, arr(j_0))" occ=1;
636608
@@ -886,8 +858,7 @@ public static void insertion_sort(int[] values, int begin, int end) {
886858
// 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!
887859
/*@ assert insSort1: \dl_seqPerm(seqUpd(\dl_seq_def_workaround(begin, end, values), hole - begin, value), \old(\dl_seq_def_workaround(begin, end, values))) \by {
888860
leave;
889-
}
890-
@*/
861+
} @*/
891862
/* @ assert insSort1: \dl_seqPerm(seqUpd(\dl_seq_def_workaround(begin, end, values), hole - begin, value), \old(\dl_seq_def_workaround(begin, end, values))) \by {
892863
893864
oss;

0 commit comments

Comments
 (0)