From 723df645882a73f5f191d781d619bdd207237f65 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E5=A4=A7=E6=9D=BE=20=E7=94=9F=E8=BC=9D?= Date: Mon, 20 May 2024 17:32:35 +0900 Subject: [PATCH 1/3] fix: missing decrementing j in snapshots example. --- guide/src/snapshots.md | 1 + 1 file changed, 1 insertion(+) diff --git a/guide/src/snapshots.md b/guide/src/snapshots.md index eb2cdb914..01a923ccc 100644 --- a/guide/src/snapshots.md +++ b/guide/src/snapshots.md @@ -25,6 +25,7 @@ fn insertion_sort(array: &mut [i32]) { if array[j - 1] > array[j] { array.swap(j - 1, j); } + j -= 1; } } } From 5343f59a26824a047210d54055bbf48337205b0d Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Mon, 20 May 2024 12:36:15 +0200 Subject: [PATCH 2/3] Adjust documented version of insertion_sort and add proof --- .../tests/should_succeed/insertion_sort.mlcfg | 475 ++++++++++++++++++ .../tests/should_succeed/insertion_sort.rs | 45 ++ .../insertion_sort/why3session.xml | 127 +++++ .../insertion_sort/why3shapes.gz | Bin 0 -> 2812 bytes guide/src/snapshots.md | 16 +- 5 files changed, 658 insertions(+), 5 deletions(-) create mode 100644 creusot/tests/should_succeed/insertion_sort.mlcfg create mode 100644 creusot/tests/should_succeed/insertion_sort.rs create mode 100644 creusot/tests/should_succeed/insertion_sort/why3session.xml create mode 100644 creusot/tests/should_succeed/insertion_sort/why3shapes.gz diff --git a/creusot/tests/should_succeed/insertion_sort.mlcfg b/creusot/tests/should_succeed/insertion_sort.mlcfg new file mode 100644 index 000000000..3d3aa9f27 --- /dev/null +++ b/creusot/tests/should_succeed/insertion_sort.mlcfg @@ -0,0 +1,475 @@ + +module Core_Cmp_Ordering_Type + type t_ordering = + | C_Less + | C_Equal + | C_Greater + +end +module Core_Ops_Range_Range_Type + type t_range 'idx = + | C_Range 'idx 'idx + + let function range_end (self : t_range 'idx) : 'idx = [@vc:do_not_keep_trace] [@vc:sp] + match self with + | C_Range _ a -> a + end + let function range_start (self : t_range 'idx) : 'idx = [@vc:do_not_keep_trace] [@vc:sp] + match self with + | C_Range a _ -> a + end +end +module Core_Option_Option_Type + type t_option 't = + | C_None + | C_Some 't + + let function some_0 (self : t_option 't) : 't = [@vc:do_not_keep_trace] [@vc:sp] + match self with + | C_None -> any 't + | C_Some a -> a + end +end +module InsertionSort_InsertionSort + use prelude.UIntSize + use seq.Seq + predicate invariant7 (self : Seq.seq usize) = + [#"../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true + val invariant7 (self : Seq.seq usize) : bool + ensures { result = invariant7 self } + + predicate inv7 (_x : Seq.seq usize) + val inv7 (_x : Seq.seq usize) : bool + ensures { result = inv7 _x } + + axiom inv7 : forall x : Seq.seq usize . inv7 x = true + use prelude.Int32 + predicate invariant6 (self : Seq.seq int32) = + [#"../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true + val invariant6 (self : Seq.seq int32) : bool + ensures { result = invariant6 self } + + predicate inv6 (_x : Seq.seq int32) + val inv6 (_x : Seq.seq int32) : bool + ensures { result = inv6 _x } + + axiom inv6 : forall x : Seq.seq int32 . inv6 x = true + use prelude.Slice + predicate invariant5 (self : slice int32) = + [#"../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true + val invariant5 (self : slice int32) : bool + ensures { result = invariant5 self } + + predicate inv5 (_x : slice int32) + val inv5 (_x : slice int32) : bool + ensures { result = inv5 _x } + + axiom inv5 : forall x : slice int32 . inv5 x = true + use prelude.Borrow + predicate invariant4 (self : borrowed (slice int32)) = + [#"../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true + val invariant4 (self : borrowed (slice int32)) : bool + ensures { result = invariant4 self } + + predicate inv4 (_x : borrowed (slice int32)) + val inv4 (_x : borrowed (slice int32)) : bool + ensures { result = inv4 _x } + + axiom inv4 : forall x : borrowed (slice int32) . inv4 x = true + use Core_Option_Option_Type as Core_Option_Option_Type + predicate invariant3 (self : Core_Option_Option_Type.t_option usize) = + [#"../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true + val invariant3 (self : Core_Option_Option_Type.t_option usize) : bool + ensures { result = invariant3 self } + + predicate inv3 (_x : Core_Option_Option_Type.t_option usize) + val inv3 (_x : Core_Option_Option_Type.t_option usize) : bool + ensures { result = inv3 _x } + + axiom inv3 : forall x : Core_Option_Option_Type.t_option usize . inv3 x = true + use Core_Ops_Range_Range_Type as Core_Ops_Range_Range_Type + predicate invariant2 (self : borrowed (Core_Ops_Range_Range_Type.t_range usize)) = + [#"../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true + val invariant2 (self : borrowed (Core_Ops_Range_Range_Type.t_range usize)) : bool + ensures { result = invariant2 self } + + predicate inv2 (_x : borrowed (Core_Ops_Range_Range_Type.t_range usize)) + val inv2 (_x : borrowed (Core_Ops_Range_Range_Type.t_range usize)) : bool + ensures { result = inv2 _x } + + axiom inv2 : forall x : borrowed (Core_Ops_Range_Range_Type.t_range usize) . inv2 x = true + predicate invariant1 (self : slice int32) = + [#"../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true + val invariant1 (self : slice int32) : bool + ensures { result = invariant1 self } + + predicate inv1 (_x : slice int32) + val inv1 (_x : slice int32) : bool + ensures { result = inv1 _x } + + axiom inv1 : forall x : slice int32 . inv1 x = true + use seq.Seq + predicate inv0 (_x : Core_Ops_Range_Range_Type.t_range usize) + val inv0 (_x : Core_Ops_Range_Range_Type.t_range usize) : bool + ensures { result = inv0 _x } + + use prelude.Int + use seq.Seq + use seq.Seq + use prelude.Int + use prelude.UIntSize + function deep_model0 (self : usize) : int = + [#"../../../../creusot-contracts/src/std/num.rs" 22 16 22 35] UIntSize.to_int self + val deep_model0 (self : usize) : int + ensures { result = deep_model0 self } + + predicate produces0 (self : Core_Ops_Range_Range_Type.t_range usize) (visited : Seq.seq usize) (o : Core_Ops_Range_Range_Type.t_range usize) + + = + [#"../../../../creusot-contracts/src/std/iter/range.rs" 21 8 27 9] Core_Ops_Range_Range_Type.range_end self + = Core_Ops_Range_Range_Type.range_end o + /\ deep_model0 (Core_Ops_Range_Range_Type.range_start self) <= deep_model0 (Core_Ops_Range_Range_Type.range_start o) + /\ (Seq.length visited > 0 + -> deep_model0 (Core_Ops_Range_Range_Type.range_start o) <= deep_model0 (Core_Ops_Range_Range_Type.range_end o)) + /\ Seq.length visited + = deep_model0 (Core_Ops_Range_Range_Type.range_start o) - deep_model0 (Core_Ops_Range_Range_Type.range_start self) + /\ (forall i : int . 0 <= i /\ i < Seq.length visited + -> deep_model0 (Seq.get visited i) = deep_model0 (Core_Ops_Range_Range_Type.range_start self) + i) + val produces0 (self : Core_Ops_Range_Range_Type.t_range usize) (visited : Seq.seq usize) (o : Core_Ops_Range_Range_Type.t_range usize) : bool + ensures { result = produces0 self visited o } + + function produces_trans0 (a : Core_Ops_Range_Range_Type.t_range usize) (ab : Seq.seq usize) (b : Core_Ops_Range_Range_Type.t_range usize) (bc : Seq.seq usize) (c : Core_Ops_Range_Range_Type.t_range usize) : () + + val produces_trans0 (a : Core_Ops_Range_Range_Type.t_range usize) (ab : Seq.seq usize) (b : Core_Ops_Range_Range_Type.t_range usize) (bc : Seq.seq usize) (c : Core_Ops_Range_Range_Type.t_range usize) : () + requires {[#"../../../../creusot-contracts/src/std/iter/range.rs" 37 15 37 32] produces0 a ab b} + requires {[#"../../../../creusot-contracts/src/std/iter/range.rs" 38 15 38 32] produces0 b bc c} + requires {[#"../../../../creusot-contracts/src/std/iter/range.rs" 40 22 40 23] inv0 a} + requires {[#"../../../../creusot-contracts/src/std/iter/range.rs" 40 31 40 33] inv7 ab} + requires {[#"../../../../creusot-contracts/src/std/iter/range.rs" 40 52 40 53] inv0 b} + requires {[#"../../../../creusot-contracts/src/std/iter/range.rs" 40 61 40 63] inv7 bc} + requires {[#"../../../../creusot-contracts/src/std/iter/range.rs" 40 82 40 83] inv0 c} + ensures { result = produces_trans0 a ab b bc c } + + axiom produces_trans0_spec : forall a : Core_Ops_Range_Range_Type.t_range usize, ab : Seq.seq usize, b : Core_Ops_Range_Range_Type.t_range usize, bc : Seq.seq usize, c : Core_Ops_Range_Range_Type.t_range usize . ([#"../../../../creusot-contracts/src/std/iter/range.rs" 37 15 37 32] produces0 a ab b) + -> ([#"../../../../creusot-contracts/src/std/iter/range.rs" 38 15 38 32] produces0 b bc c) + -> ([#"../../../../creusot-contracts/src/std/iter/range.rs" 40 22 40 23] inv0 a) + -> ([#"../../../../creusot-contracts/src/std/iter/range.rs" 40 31 40 33] inv7 ab) + -> ([#"../../../../creusot-contracts/src/std/iter/range.rs" 40 52 40 53] inv0 b) + -> ([#"../../../../creusot-contracts/src/std/iter/range.rs" 40 61 40 63] inv7 bc) + -> ([#"../../../../creusot-contracts/src/std/iter/range.rs" 40 82 40 83] inv0 c) + -> ([#"../../../../creusot-contracts/src/std/iter/range.rs" 39 14 39 42] produces0 a (Seq.(++) ab bc) c) + use seq.Seq + function produces_refl0 (self : Core_Ops_Range_Range_Type.t_range usize) : () + val produces_refl0 (self : Core_Ops_Range_Range_Type.t_range usize) : () + requires {[#"../../../../creusot-contracts/src/std/iter/range.rs" 33 21 33 25] inv0 self} + ensures { result = produces_refl0 self } + + axiom produces_refl0_spec : forall self : Core_Ops_Range_Range_Type.t_range usize . ([#"../../../../creusot-contracts/src/std/iter/range.rs" 33 21 33 25] inv0 self) + -> ([#"../../../../creusot-contracts/src/std/iter/range.rs" 32 14 32 45] produces0 self (Seq.empty ) self) + predicate invariant0 (self : Core_Ops_Range_Range_Type.t_range usize) = + [#"../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true + val invariant0 (self : Core_Ops_Range_Range_Type.t_range usize) : bool + ensures { result = invariant0 self } + + axiom inv0 : forall x : Core_Ops_Range_Range_Type.t_range usize . inv0 x = true + use int.Int + use seq.Seq + predicate sorted_range0 [#"../insertion_sort.rs" 6 0 6 63] (s : Seq.seq int32) (l : int) (u : int) = + [#"../insertion_sort.rs" 7 4 9 5] forall j : int . forall i : int . l <= i /\ i < j /\ j < u + -> Seq.get s i <= Seq.get s j + val sorted_range0 [#"../insertion_sort.rs" 6 0 6 63] (s : Seq.seq int32) (l : int) (u : int) : bool + ensures { result = sorted_range0 s l u } + + use seq.Seq + predicate sorted0 [#"../insertion_sort.rs" 13 0 13 41] (s : Seq.seq int32) = + [#"../insertion_sort.rs" 15 8 15 35] sorted_range0 s 0 (Seq.length s) + val sorted0 [#"../insertion_sort.rs" 13 0 13 41] (s : Seq.seq int32) : bool + ensures { result = sorted0 s } + + use prelude.Slice + let constant max0 : usize = [@vc:do_not_keep_trace] [@vc:sp] + (18446744073709551615 : usize) + function shallow_model2 (self : slice int32) : Seq.seq int32 + val shallow_model2 (self : slice int32) : Seq.seq int32 + requires {[#"../../../../creusot-contracts/src/std/slice.rs" 19 21 19 25] inv5 self} + ensures { result = shallow_model2 self } + + axiom shallow_model2_spec : forall self : slice int32 . ([#"../../../../creusot-contracts/src/std/slice.rs" 19 21 19 25] inv5 self) + -> ([#"../../../../creusot-contracts/src/std/slice.rs" 19 4 19 50] inv6 (shallow_model2 self)) + && ([#"../../../../creusot-contracts/src/std/slice.rs" 18 14 18 42] shallow_model2 self = Slice.id self) + && ([#"../../../../creusot-contracts/src/std/slice.rs" 17 14 17 41] Seq.length (shallow_model2 self) + <= UIntSize.to_int max0) + use prelude.Snapshot + predicate resolve1 (self : borrowed (slice int32)) = + [#"../../../../creusot-contracts/src/resolve.rs" 26 20 26 34] ^ self = * self + val resolve1 (self : borrowed (slice int32)) : bool + ensures { result = resolve1 self } + + use seq.Permut + function shallow_model0 (self : borrowed (slice int32)) : Seq.seq int32 = + [#"../../../../creusot-contracts/src/model.rs" 108 8 108 31] shallow_model2 ( * self) + val shallow_model0 (self : borrowed (slice int32)) : Seq.seq int32 + ensures { result = shallow_model0 self } + + val swap0 (self : borrowed (slice int32)) (a : usize) (b : usize) : () + requires {[#"../../../../creusot-contracts/src/std/slice.rs" 247 19 247 35] UIntSize.to_int a + < Seq.length (shallow_model0 self)} + requires {[#"../../../../creusot-contracts/src/std/slice.rs" 248 19 248 35] UIntSize.to_int b + < Seq.length (shallow_model0 self)} + requires {inv4 self} + ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 249 8 249 52] Permut.exchange (shallow_model2 ( ^ self)) (shallow_model0 self) (UIntSize.to_int a) (UIntSize.to_int b) } + + function index_logic1 [@inline:trivial] (self : slice int32) (ix : usize) : int32 = + [#"../../../../creusot-contracts/src/logic/ops.rs" 54 8 54 32] Seq.get (shallow_model2 self) (UIntSize.to_int ix) + val index_logic1 [@inline:trivial] (self : slice int32) (ix : usize) : int32 + ensures { result = index_logic1 self ix } + + function index_logic0 [@inline:trivial] (self : slice int32) (ix : int) : int32 = + [#"../../../../creusot-contracts/src/logic/ops.rs" 43 8 43 31] Seq.get (shallow_model2 self) ix + val index_logic0 [@inline:trivial] (self : slice int32) (ix : int) : int32 + ensures { result = index_logic0 self ix } + + use seq.Seq + predicate resolve0 (self : borrowed (Core_Ops_Range_Range_Type.t_range usize)) = + [#"../../../../creusot-contracts/src/resolve.rs" 26 20 26 34] ^ self = * self + val resolve0 (self : borrowed (Core_Ops_Range_Range_Type.t_range usize)) : bool + ensures { result = resolve0 self } + + predicate completed0 (self : borrowed (Core_Ops_Range_Range_Type.t_range usize)) = + [#"../../../../creusot-contracts/src/std/iter/range.rs" 14 12 14 78] resolve0 self + /\ deep_model0 (Core_Ops_Range_Range_Type.range_start ( * self)) + >= deep_model0 (Core_Ops_Range_Range_Type.range_end ( * self)) + val completed0 (self : borrowed (Core_Ops_Range_Range_Type.t_range usize)) : bool + ensures { result = completed0 self } + + val next0 (self : borrowed (Core_Ops_Range_Range_Type.t_range usize)) : Core_Option_Option_Type.t_option usize + requires {inv2 self} + ensures { [#"../../../../creusot-contracts/src/std/iter.rs" 95 26 98 17] match result with + | Core_Option_Option_Type.C_None -> completed0 self + | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self) + end } + ensures { inv3 result } + + use seq.Permut + predicate permutation_of0 (self : Seq.seq int32) (o : Seq.seq int32) = + [#"../../../../creusot-contracts/src/logic/seq.rs" 107 8 107 37] Permut.permut self o 0 (Seq.length self) + val permutation_of0 (self : Seq.seq int32) (o : Seq.seq int32) : bool + ensures { result = permutation_of0 self o } + + function shallow_model3 (self : slice int32) : Seq.seq int32 = + [#"../../../../creusot-contracts/src/model.rs" 90 8 90 31] shallow_model2 self + val shallow_model3 (self : slice int32) : Seq.seq int32 + ensures { result = shallow_model3 self } + + use prelude.Snapshot + function shallow_model1 (self : Snapshot.snap_ty (slice int32)) : Seq.seq int32 = + [#"../../../../creusot-contracts/src/snapshot.rs" 27 20 27 48] shallow_model3 (Snapshot.inner self) + val shallow_model1 (self : Snapshot.snap_ty (slice int32)) : Seq.seq int32 + ensures { result = shallow_model1 self } + + use prelude.Snapshot + use prelude.Snapshot + use prelude.Snapshot + use prelude.Snapshot + use prelude.Snapshot + predicate into_iter_post0 (self : Core_Ops_Range_Range_Type.t_range usize) (res : Core_Ops_Range_Range_Type.t_range usize) + + = + [#"../../../../creusot-contracts/src/std/iter.rs" 80 8 80 19] self = res + val into_iter_post0 (self : Core_Ops_Range_Range_Type.t_range usize) (res : Core_Ops_Range_Range_Type.t_range usize) : bool + ensures { result = into_iter_post0 self res } + + predicate into_iter_pre0 (self : Core_Ops_Range_Range_Type.t_range usize) = + [#"../../../../creusot-contracts/src/std/iter.rs" 74 20 74 24] true + val into_iter_pre0 (self : Core_Ops_Range_Range_Type.t_range usize) : bool + ensures { result = into_iter_pre0 self } + + val into_iter0 (self : Core_Ops_Range_Range_Type.t_range usize) : Core_Ops_Range_Range_Type.t_range usize + requires {[#"../../../../creusot-contracts/src/std/iter.rs" 89 0 166 1] into_iter_pre0 self} + requires {inv0 self} + ensures { [#"../../../../creusot-contracts/src/std/iter.rs" 89 0 166 1] into_iter_post0 self result } + ensures { inv0 result } + + val len0 (self : slice int32) : usize + requires {inv1 self} + ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 238 0 334 1] Seq.length (shallow_model3 self) + = UIntSize.to_int result } + + use prelude.Snapshot + let rec cfg insertion_sort [#"../insertion_sort.rs" 21 0 21 40] [@cfg:stackify] [@cfg:subregion_analysis] (array : borrowed (slice int32)) : () + ensures { [#"../insertion_sort.rs" 19 0 19 44] permutation_of0 (shallow_model0 array) (shallow_model2 ( ^ array)) } + ensures { [#"../insertion_sort.rs" 20 10 20 27] sorted0 (shallow_model2 ( ^ array)) } + + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : (); + var array : borrowed (slice int32) = array; + var original : Snapshot.snap_ty (slice int32); + var n : usize; + var iter : Core_Ops_Range_Range_Type.t_range usize; + var _10 : Core_Ops_Range_Range_Type.t_range usize; + var iter_old : Snapshot.snap_ty (Core_Ops_Range_Range_Type.t_range usize); + var produced : Snapshot.snap_ty (Seq.seq usize); + var _21 : (); + var _22 : Core_Option_Option_Type.t_option usize; + var _23 : borrowed (Core_Ops_Range_Range_Type.t_range usize); + var _24 : borrowed (Core_Ops_Range_Range_Type.t_range usize); + var __creusot_proc_iter_elem : usize; + var _27 : Snapshot.snap_ty (Seq.seq usize); + var i : usize; + var j : usize; + var _36 : bool; + var _39 : bool; + var _41 : usize; + var _43 : usize; + var _44 : bool; + var _46 : usize; + var _47 : usize; + var _48 : bool; + var _49 : (); + var _50 : borrowed (slice int32); + var _51 : usize; + { + goto BB0 + } + BB0 { + [#"../insertion_sort.rs" 22 19 22 36] original <- ([#"../insertion_sort.rs" 22 19 22 36] Snapshot.new ( * array)); + goto BB1 + } + BB1 { + [#"../insertion_sort.rs" 23 12 23 23] n <- ([#"../insertion_sort.rs" 23 12 23 23] len0 ( * array)); + goto BB2 + } + BB2 { + [#"../insertion_sort.rs" 27 13 27 17] _10 <- Core_Ops_Range_Range_Type.C_Range ([#"../insertion_sort.rs" 27 13 27 14] (1 : usize)) n; + [#"../insertion_sort.rs" 24 4 24 61] iter <- ([#"../insertion_sort.rs" 24 4 24 61] into_iter0 _10); + _10 <- any Core_Ops_Range_Range_Type.t_range usize; + goto BB3 + } + BB3 { + [#"../insertion_sort.rs" 24 4 24 61] iter_old <- ([#"../insertion_sort.rs" 24 4 24 61] Snapshot.new iter); + goto BB4 + } + BB4 { + [#"../insertion_sort.rs" 24 4 24 61] produced <- ([#"../insertion_sort.rs" 24 4 24 61] Snapshot.new (Seq.empty )); + goto BB5 + } + BB5 { + goto BB6 + } + BB6 { + invariant { [#"../insertion_sort.rs" 24 4 24 61] inv0 iter }; + invariant { [#"../insertion_sort.rs" 24 4 24 61] produces0 (Snapshot.inner iter_old) (Snapshot.inner produced) iter }; + invariant { [#"../insertion_sort.rs" 24 16 24 59] sorted_range0 (shallow_model0 array) 0 (Seq.length (Snapshot.inner produced) + + 1) }; + invariant { [#"../insertion_sort.rs" 25 16 25 34] Seq.length (shallow_model0 array) = UIntSize.to_int n }; + invariant { [#"../insertion_sort.rs" 24 4 24 61] permutation_of0 (shallow_model1 original) (shallow_model0 array) }; + goto BB7 + } + BB7 { + [#"../insertion_sort.rs" 24 4 24 61] _24 <- Borrow.borrow_mut iter; + [#"../insertion_sort.rs" 24 4 24 61] iter <- ^ _24; + [#"../insertion_sort.rs" 24 4 24 61] _23 <- Borrow.borrow_final ( * _24) (Borrow.get_id _24); + [#"../insertion_sort.rs" 24 4 24 61] _24 <- { _24 with current = ( ^ _23) ; }; + [#"../insertion_sort.rs" 24 4 24 61] _22 <- ([#"../insertion_sort.rs" 24 4 24 61] next0 _23); + _23 <- any borrowed (Core_Ops_Range_Range_Type.t_range usize); + goto BB8 + } + BB8 { + assume { resolve0 _24 }; + switch (_22) + | Core_Option_Option_Type.C_None -> goto BB11 + | Core_Option_Option_Type.C_Some _ -> goto BB10 + end + } + BB9 { + assume { resolve1 array }; + assert { [#"../insertion_sort.rs" 24 4 24 61] false }; + absurd + } + BB10 { + goto BB12 + } + BB11 { + assume { resolve1 array }; + assert { [@expl:assertion] [#"../insertion_sort.rs" 44 18 44 55] sorted_range0 (shallow_model0 array) 0 (Seq.length (shallow_model0 array)) }; + [#"../insertion_sort.rs" 21 41 45 1] _0 <- ([#"../insertion_sort.rs" 21 41 45 1] ()); + return _0 + } + BB12 { + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _22; + [#"../insertion_sort.rs" 24 4 24 61] _27 <- ([#"../insertion_sort.rs" 24 4 24 61] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem))); + goto BB13 + } + BB13 { + [#"../insertion_sort.rs" 24 4 24 61] produced <- _27; + _27 <- any Snapshot.snap_ty (Seq.seq usize); + [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem; + [#"../insertion_sort.rs" 28 20 28 21] j <- i; + goto BB14 + } + BB14 { + invariant { [#"../insertion_sort.rs" 29 20 29 26] j <= i }; + invariant { [#"../insertion_sort.rs" 30 20 30 38] Seq.length (shallow_model0 array) = UIntSize.to_int n }; + invariant { [#"../insertion_sort.rs" 29 8 29 28] permutation_of0 (shallow_model1 original) (shallow_model0 array) }; + invariant { [#"../insertion_sort.rs" 29 8 29 28] forall b : int . forall a : int . 0 <= a + /\ a <= b /\ b <= UIntSize.to_int i + -> a <> UIntSize.to_int j -> b <> UIntSize.to_int j -> index_logic0 ( * array) a <= index_logic0 ( * array) b }; + invariant { [#"../insertion_sort.rs" 29 8 29 28] forall a : int . UIntSize.to_int j + 1 <= a + /\ a <= UIntSize.to_int i -> index_logic1 ( * array) j < index_logic0 ( * array) a }; + goto BB15 + } + BB15 { + [#"../insertion_sort.rs" 34 14 34 19] _36 <- j > ([#"../insertion_sort.rs" 34 18 34 19] (0 : usize)); + switch (_36) + | False -> goto BB22 + | True -> goto BB16 + end + } + BB16 { + [#"../insertion_sort.rs" 35 21 35 26] _41 <- j - ([#"../insertion_sort.rs" 35 25 35 26] (1 : usize)); + [#"../insertion_sort.rs" 35 15 35 27] _43 <- Slice.length ( * array); + [#"../insertion_sort.rs" 35 15 35 27] _44 <- _41 < _43; + assert { [@expl:index in bounds] [#"../insertion_sort.rs" 35 15 35 27] _44 }; + goto BB17 + } + BB17 { + [#"../insertion_sort.rs" 35 36 35 37] _46 <- j; + [#"../insertion_sort.rs" 35 30 35 38] _47 <- Slice.length ( * array); + [#"../insertion_sort.rs" 35 30 35 38] _48 <- _46 < _47; + assert { [@expl:index in bounds] [#"../insertion_sort.rs" 35 30 35 38] _48 }; + goto BB18 + } + BB18 { + [#"../insertion_sort.rs" 35 15 35 38] _39 <- Slice.get ( * array) _41 > Slice.get ( * array) _46; + switch (_39) + | False -> goto BB21 + | True -> goto BB19 + end + } + BB19 { + [#"../insertion_sort.rs" 36 16 36 21] _50 <- Borrow.borrow_mut ( * array); + [#"../insertion_sort.rs" 36 16 36 21] array <- { array with current = ( ^ _50) ; }; + [#"../insertion_sort.rs" 36 27 36 32] _51 <- j - ([#"../insertion_sort.rs" 36 31 36 32] (1 : usize)); + [#"../insertion_sort.rs" 36 16 36 36] _49 <- ([#"../insertion_sort.rs" 36 16 36 36] swap0 _50 _51 j); + _50 <- any borrowed (slice int32); + _51 <- any usize; + goto BB20 + } + BB20 { + [#"../insertion_sort.rs" 40 12 40 18] j <- j - ([#"../insertion_sort.rs" 40 17 40 18] (1 : usize)); + [#"../insertion_sort.rs" 34 20 41 9] _21 <- ([#"../insertion_sort.rs" 34 20 41 9] ()); + goto BB14 + } + BB21 { + [#"../insertion_sort.rs" 38 16 38 21] _21 <- ([#"../insertion_sort.rs" 38 16 38 21] ()); + goto BB23 + } + BB22 { + [#"../insertion_sort.rs" 34 8 41 9] _21 <- ([#"../insertion_sort.rs" 34 8 41 9] ()); + goto BB23 + } + BB23 { + goto BB6 + } + +end diff --git a/creusot/tests/should_succeed/insertion_sort.rs b/creusot/tests/should_succeed/insertion_sort.rs new file mode 100644 index 000000000..ebac1f450 --- /dev/null +++ b/creusot/tests/should_succeed/insertion_sort.rs @@ -0,0 +1,45 @@ +#![allow(dead_code)] +extern crate creusot_contracts; +use creusot_contracts::*; + +#[predicate] +fn sorted_range(s: Seq, l: Int, u: Int) -> bool { + pearlite! { + forall l <= i && i < j && j < u ==> s[i] <= s[j] + } +} + +#[predicate] +fn sorted(s: Seq) -> bool { + pearlite! { + sorted_range(s, 0, s.len()) + } +} + +#[ensures(array@.permutation_of((^array)@))] +#[ensures(sorted((^array)@))] +pub fn insertion_sort(array: &mut [i32]) { + let original = snapshot!(*array); // remember the original value + let n = array.len(); + #[invariant(sorted_range(array@, 0, produced.len() + 1))] + #[invariant(array@.len() == n@)] + #[invariant(original@.permutation_of(array@))] + for i in 1..n { + let mut j = i; + #[invariant(j <= i)] + #[invariant(array@.len() == n@)] + #[invariant(original@.permutation_of(array@))] + #[invariant(forall< a : Int, b : Int> 0 <= a && a <= b && b <= i@ ==> a != j@ ==> b != j@ ==> array[a] <= array[b])] + #[invariant(forall< a : _> j@ + 1 <= a && a <= i@ ==> array[j] < array[a])] + while j > 0 { + if array[j - 1] > array[j] { + array.swap(j - 1, j); + } else { + break; + } + j -= 1; + } + } + + proof_assert!(sorted_range(array@, 0, array@.len())); +} diff --git a/creusot/tests/should_succeed/insertion_sort/why3session.xml b/creusot/tests/should_succeed/insertion_sort/why3session.xml new file mode 100644 index 000000000..7be6cc99c --- /dev/null +++ b/creusot/tests/should_succeed/insertion_sort/why3session.xml @@ -0,0 +1,127 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/insertion_sort/why3shapes.gz b/creusot/tests/should_succeed/insertion_sort/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..264cba463e96b3d63420eded8dd31e56daa364e0 GIT binary patch literal 2812 zcmV;3ns?wKKnlz8}BM}Dx_M|E{wUG>%YFE3^fzxn(8F#C|#56f=#x0#x~`0Lf? zzka#;pc{5G3{?Z;P&POYMZ?D-Z^SsnMvg;h)XkN@Uw7$!%nz*5{^iTYG{72wH-%t3 z(6l(L*kQp8bNyz*!H$O~Oo^l2y9UtbyZg-_G#GE$%1mPt+Q0h6-{#fZ&2OFzaC_VR zzPRgBzQqQF-*k)RYUA(xM>hArJVCHb^mktE@_6@6ZzLdl(BW>qe7juvTffS``xoA? z*Zz;IYMSlrew|~tO3Mw|zZ`i=Em9Rx zx@FVzedyMkoEGb%0o&J@_4-EUUyc^pXA$9;vDhP1-RJe)`;9LaUUcojO|Wy)Q*17g z5{`=rXXS*iBxt>-t=j|N$)q|q!ML*>4!(ck7bq_F9*p#Tuz>&fI4$dZvP-08;ceb5 zmT6q2AMl}Due;xK`swaJ^*A4-rOn}(sIp<%ySnzVySu;5ms|5)dXxX$k%x((%sF828#-{w1Fb(a^cx6UqL zM}r6kPtOfo(B~>MU zDyj9|bW(RI8hxemKGfeZrs3t)uf-?h^j)2X-Lw$Xh-1%emGZ~MZTEH=*;u40Z=9tF zm+)!8o+mMHNI?48O4!fsZcaB%_LuWICnROYFtj&4Bzn0$LwI5|&(mj1@yK4kx|_51AqzVFS*2BNxKO70?b?^o%;|9n6QS2W0P^Lo}% z`_Yn%%E<}Mf^fp)LxsEGLy+u@)31v?(Ow;L+ne&?NH1tLC!yF`FYRHNE`)lNL%vD; z&_xFUR93!L1Qj*DG=zx9E{0Ap%BSAmPALDNYJwHaOMW@GSr-JP6I#A=?lUf`!rql`(^8VmY z_1A1P_t&W|`~X700fvAJvIjp4BKSohf;ZFvoF(at7Q#UlLp-QrJBmIBA*G8E%_2U6 z5isD0GkJ-huWV$FtLt{?(5^TA6C8ir{w>mjnt#0~I-lf``KPC$`H_s)uPgs8C&f-ywCBxc%7C@zO+2 z<}mFDJ6>?Y_Bh2%SCdUS0z0BHfxyi~>kf8peK*GWFx-xdjr*qK!1;>$wJIt4~eokxBkd&f-FnJK%PpB)yDE@nySW@H3dmI z29V%;DY42;+oyA4<)lw<_sxh@JI4Kjo-9;R)V?T0L2JXqmil};{Gzw>YTt=+Z^nCf zi|vRvybl3-A_D6YmQ2@(8pED`8)r>MHYy zDSHtti=Jt#P@n~stv3-RiWwj}KybjEb;fC@oOHr*N6U^~DcP#*QO2MXVm6Xx#-e2g zHM9wE2AqyNILaVMjWX~oJfchn5qS%l9+VQ1qiQPyVYDapkyloQ~28Iu4FAhjg29s6XjWkr;+#NGFLDHQXC|0UlatEjcHc znILN61a|_R04JE^_A843+G?*sbBZ(anFy)aRkjv_1&A}DolxIe3Z0_XIjSgA;yQq* zykcXUjj*i>(3TVHtjFNIX<*7DMvQsJBz;fVH2|>wKFkNL-$|>oTaEd!cQ~2&uhwR%ZSX7v- z#pGkDmdPk(7;lBD*-ta4tWzYW{_gT}mQzSAS5Zi+R^D3{0!4$55xq}gX22Qdv~`*e zYp0dd(rMu|cbZgz?6lE))i#9Bf9t1B5W+)p7TuM|ZEkkP62pq+#&9m_hCLLv9QblAu zS(dEGKIKe+q6KnQdEulh{iE~NS>vpJF1kggs3o9>Pp_yI(V#F93>Z$@X%qV1gq45z zEcMF;S%pxuLR8jMx%N>rZeu3+V+Z}jv(~YtG;Si7Ib)O<3C9r}F_H&bur`QZNBQja zv{G=<+Lqd8B|TahrI$$(j;0bEncclZ^=x%yjMOrW+P}zE5}vY*2&OeWA*rp|445eu z7npw5dLrh;Bz5Ejms4t~)sKu}sTM$}KV#JsnEerSHJ+=MlV=GM0yVy*bnxD^!FmFY zA@;h`;U7d_A3cWFl&?#aV+~Lj0!GoBC7>J#ArJaeBC21#VAp&6Kt>RvO|6i^+GwH; zMzEwJW#Mdf^oE+R-UzBRGEkURZa<9r8VDr`DnHV5Oc@!|V3iIWvd9V2pnmzMzg6ic zK#f^RCO!DpAd87AV&a@fP534cBG_*%h7OF2#FRxU$xQg*g|{FI=t7au^kNit-&_

TqtpaX%(A4n-VU^LUFE02eNdxpeT8RYCOb)G$S}CcO@G7` type (`creusot_contracts::S They can be useful if you need a way to remember a previous value, but only for the proof: ```rust -#[ensures(permutation_of((*array)@, (^array)@))] -#[ensures(is_sorted(^array))] -fn insertion_sort(array: &mut [i32]) { +#[ensures(array@.permutation_of((^array)@))] +#[ensures(sorted((^array)@))] +pub fn insertion_sort(array: &mut [i32]) { let original = snapshot!(*array); // remember the original value let n = array.len(); - #[invariant(permutation_of(original@, (*array)@))] + #[invariant(original@.permutation_of(array@))] + #[invariant(...)] for i in 1..n { let mut j = i; - #[invariant(permutation_of(original@, (*array)@))] + #[invariant(original@.permutation_of(array@))] + #[invariant(...)] while j > 0 { if array[j - 1] > array[j] { array.swap(j - 1, j); + } else { + break; } j -= 1; } } + + proof_assert!(sorted_range(array@, 0, array@.len())); } #[logic] From adf83419584585010a8252a025b9a504dcba85cd Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Mon, 20 May 2024 14:20:49 +0200 Subject: [PATCH 3/3] Update proof to alt-ergo 2.5.3 --- .../insertion_sort/why3session.xml | 75 +++++++++---------- 1 file changed, 37 insertions(+), 38 deletions(-) diff --git a/creusot/tests/should_succeed/insertion_sort/why3session.xml b/creusot/tests/should_succeed/insertion_sort/why3session.xml index 7be6cc99c..655ee004c 100644 --- a/creusot/tests/should_succeed/insertion_sort/why3session.xml +++ b/creusot/tests/should_succeed/insertion_sort/why3session.xml @@ -3,122 +3,121 @@ "https://www.why3.org/why3session.dtd"> - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - +