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..655ee004c --- /dev/null +++ b/creusot/tests/should_succeed/insertion_sort/why3session.xml @@ -0,0 +1,126 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 000000000..264cba463 Binary files /dev/null and b/creusot/tests/should_succeed/insertion_sort/why3shapes.gz differ diff --git a/guide/src/snapshots.md b/guide/src/snapshots.md index eb2cdb914..8aee6b095 100644 --- a/guide/src/snapshots.md +++ b/guide/src/snapshots.md @@ -12,21 +12,28 @@ A useful tool to have in proofs is the `Snapshot` 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]