From 756f9ce45eb3b99647f655c4ada3c285c0b62470 Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Fri, 29 Sep 2023 11:29:26 +0200 Subject: [PATCH] Fix #874 --- creusot-contracts/src/std/vec.rs | 8 +- creusot/src/ctx.rs | 3 +- creusot/tests/should_succeed/100doors.mlcfg | 18 +- creusot/tests/should_succeed/bug/874.mlcfg | 1156 +++++++++++++++++ creusot/tests/should_succeed/bug/874.rs | 11 + .../should_succeed/bug/874/why3session.xml | 37 + .../should_succeed/bug/874/why3shapes.gz | Bin 0 -> 931 bytes creusot/tests/should_succeed/cell/02.mlcfg | 4 +- .../should_succeed/filter_positive.mlcfg | 18 +- creusot/tests/should_succeed/hashmap.mlcfg | 18 +- .../should_succeed/heapsort_generic.mlcfg | 8 +- creusot/tests/should_succeed/hillel.mlcfg | 2 +- .../tests/should_succeed/index_range.mlcfg | 16 +- .../iterators/02_iter_mut.mlcfg | 10 +- .../iterators/03_std_iterators.mlcfg | 12 +- .../iterators/08_collect_extend.mlcfg | 62 +- creusot/tests/should_succeed/knapsack.mlcfg | 18 +- .../tests/should_succeed/knapsack_full.mlcfg | 18 +- .../should_succeed/list_reversal_lasso.mlcfg | 14 +- .../selection_sort_generic.mlcfg | 8 +- .../tests/should_succeed/sparse_array.mlcfg | 18 +- .../should_succeed/syntax/13_vec_macro.mlcfg | 4 +- creusot/tests/should_succeed/vector/01.mlcfg | 10 +- .../should_succeed/vector/02_gnome.mlcfg | 8 +- .../vector/02_gnome/why3session.xml | 30 +- .../vector/03_knuth_shuffle.mlcfg | 4 +- .../vector/04_binary_search.mlcfg | 4 +- .../vector/05_binary_search_generic.mlcfg | 4 +- .../vector/06_knights_tour.mlcfg | 86 +- .../should_succeed/vector/07_read_write.mlcfg | 14 +- .../should_succeed/vector/08_haystack.mlcfg | 4 +- 31 files changed, 1417 insertions(+), 210 deletions(-) create mode 100644 creusot/tests/should_succeed/bug/874.mlcfg create mode 100644 creusot/tests/should_succeed/bug/874.rs create mode 100644 creusot/tests/should_succeed/bug/874/why3session.xml create mode 100644 creusot/tests/should_succeed/bug/874/why3shapes.gz diff --git a/creusot-contracts/src/std/vec.rs b/creusot-contracts/src/std/vec.rs index 5f98a55ae3..8cb2c536c1 100644 --- a/creusot-contracts/src/std/vec.rs +++ b/creusot-contracts/src/std/vec.rs @@ -118,12 +118,14 @@ extern_spec! { } impl Extend for Vec { - #[ensures(exists> - done_.completed() && iter.produces(prod, *done_) && (^self)@ == self@.concat(prod) + #[requires(iter.into_iter_pre())] + #[ensures(exists> + iter.into_iter_post(start_) && + done_.completed() && start_.produces(prod, *done_) && (^self)@ == self@.concat(prod) )] fn extend(&mut self, iter: I) where - I : Iterator; + I : IntoIterator, I::IntoIter : Iterator; } impl, A : Allocator> IndexMut for Vec { diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs index dc59fc62fe..8a52cd7cce 100644 --- a/creusot/src/ctx.rs +++ b/creusot/src/ctx.rs @@ -191,7 +191,8 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> { pub(crate) fn body_with_facts(&mut self, def_id: LocalDefId) -> &BodyWithBorrowckFacts<'tcx> { if !self.bodies.contains_key(&def_id) { - let body = callbacks::get_body(self.tcx, def_id).unwrap(); + let body = callbacks::get_body(self.tcx, def_id) + .unwrap_or_else(|| panic!("did not find body for {def_id:?}")); // Basic clean up, replace FalseEdges with Gotos. Could potentially also replace other statement with Nops. // Investigate if existing MIR passes do this as part of 'post borrowck cleanup'. diff --git a/creusot/tests/should_succeed/100doors.mlcfg b/creusot/tests/should_succeed/100doors.mlcfg index d770df63f8..19d19189d0 100644 --- a/creusot/tests/should_succeed/100doors.mlcfg +++ b/creusot/tests/should_succeed/100doors.mlcfg @@ -367,8 +367,8 @@ module Alloc_Vec_FromElem_Interface type t = t val from_elem (elem : t) (n : usize) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) requires {Inv0.inv elem} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 155 22 155 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 156 12 156 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 157 22 157 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 158 12 158 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } ensures { Inv1.inv result } end @@ -677,10 +677,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -792,13 +792,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/bug/874.mlcfg b/creusot/tests/should_succeed/bug/874.mlcfg new file mode 100644 index 0000000000..904e18c1a5 --- /dev/null +++ b/creusot/tests/should_succeed/bug/874.mlcfg @@ -0,0 +1,1156 @@ + +module Core_Ptr_NonNull_NonNull_Type + use prelude.Opaque + type t_nonnull 't = + | C_NonNull opaque_ptr + +end +module Core_Marker_PhantomData_Type + type t_phantomdata 't = + | C_PhantomData + +end +module Core_Ptr_Unique_Unique_Type + use Core_Marker_PhantomData_Type as Core_Marker_PhantomData_Type + use Core_Ptr_NonNull_NonNull_Type as Core_Ptr_NonNull_NonNull_Type + type t_unique 't = + | C_Unique (Core_Ptr_NonNull_NonNull_Type.t_nonnull 't) (Core_Marker_PhantomData_Type.t_phantomdata 't) + +end +module Alloc_RawVec_RawVec_Type + use prelude.Int + use prelude.UIntSize + use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type + type t_rawvec 't 'a = + | C_RawVec (Core_Ptr_Unique_Unique_Type.t_unique 't) usize 'a + +end +module Alloc_Vec_Vec_Type + use prelude.Int + use prelude.UIntSize + use Alloc_RawVec_RawVec_Type as Alloc_RawVec_RawVec_Type + type t_vec 't 'a = + | C_Vec (Alloc_RawVec_RawVec_Type.t_rawvec 't 'a) usize + +end +module Alloc_Alloc_Global_Type + type t_global = + | C_Global + +end +module CreusotContracts_Invariant_Inv_Stub + type t + predicate inv (_x : t) +end +module CreusotContracts_Invariant_Inv_Interface + type t + predicate inv (_x : t) + val inv (_x : t) : bool + ensures { result = inv _x } + +end +module CreusotContracts_Invariant_Inv + type t + predicate inv (_x : t) = + [#"../../../../../creusot-contracts/src/invariant.rs" 16 4 16 8] true + val inv (_x : t) : bool + ensures { result = inv _x } + +end +module Core_Num_Impl11_Max_Stub + use prelude.Int + use prelude.UIntSize + val constant mAX' : usize +end +module Core_Num_Impl11_Max + use prelude.Int + use prelude.UIntSize + let constant mAX' : usize = [@vc:do_not_keep_trace] [@vc:sp] + (18446744073709551615 : usize) +end +module CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub + type t + type a + use seq.Seq + use prelude.UIntSize + use prelude.Int + use seq.Seq + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone Core_Num_Impl11_Max_Stub as Max0 + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_Vec_Type.t_vec t a + function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t +end +module CreusotContracts_Std1_Vec_Impl0_ShallowModel_Interface + type t + type a + use seq.Seq + use prelude.UIntSize + use prelude.Int + use seq.Seq + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone Core_Num_Impl11_Max_Stub as Max0 + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_Vec_Type.t_vec t a + function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t + val shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length result <= UIntSize.to_int Max0.mAX' } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv result } + ensures { result = shallow_model self } + + axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX') +end +module CreusotContracts_Std1_Vec_Impl0_ShallowModel + type t + type a + use seq.Seq + use prelude.UIntSize + use prelude.Int + use seq.Seq + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone Core_Num_Impl11_Max_Stub as Max0 + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_Vec_Type.t_vec t a + function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t + val shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length result <= UIntSize.to_int Max0.mAX' } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv result } + ensures { result = shallow_model self } + + axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX') +end +module CreusotContracts_Logic_Ops_Impl0_IndexLogic_Stub + type t + type a + use prelude.Int + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t +end +module CreusotContracts_Logic_Ops_Impl0_IndexLogic_Interface + type t + type a + use prelude.Int + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t + val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t + ensures { result = index_logic self ix } + +end +module CreusotContracts_Logic_Ops_Impl0_IndexLogic + type t + type a + use prelude.Int + use seq.Seq + use seq.Seq + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone Core_Num_Impl11_Max_Stub as Max0 + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_Vec_Type.t_vec t a + clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub as ShallowModel0 with + type t = t, + type a = a, + predicate Inv0.inv = Inv0.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv1.inv = Inv1.inv, + axiom . + function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t = + [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix + val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t + ensures { result = index_logic self ix } + +end +module CreusotContracts_Resolve_Resolve_Resolve_Stub + type self + predicate resolve (self : self) +end +module CreusotContracts_Resolve_Resolve_Resolve_Interface + type self + predicate resolve (self : self) + val resolve (self : self) : bool + ensures { result = resolve self } + +end +module CreusotContracts_Resolve_Resolve_Resolve + type self + predicate resolve (self : self) + val resolve (self : self) : bool + ensures { result = resolve self } + +end +module CreusotContracts_Std1_Vec_Impl10_Resolve_Stub + type t + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + predicate resolve (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) +end +module CreusotContracts_Std1_Vec_Impl10_Resolve_Interface + type t + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + predicate resolve (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) + val resolve (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) : bool + ensures { result = resolve self } + +end +module CreusotContracts_Std1_Vec_Impl10_Resolve + type t + use prelude.Int + use seq.Seq + use seq.Seq + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone Core_Num_Impl11_Max_Stub as Max0 + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) + clone CreusotContracts_Resolve_Resolve_Resolve_Stub as Resolve0 with + type self = t + clone CreusotContracts_Logic_Ops_Impl0_IndexLogic_Stub as IndexLogic0 with + type t = t, + type a = Alloc_Alloc_Global_Type.t_global + clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub as ShallowModel0 with + type t = t, + type a = Alloc_Alloc_Global_Type.t_global, + predicate Inv0.inv = Inv0.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv1.inv = Inv1.inv, + axiom . + predicate resolve (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) = + [#"../../../../../creusot-contracts/src/std/vec.rs" 51 8 51 85] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model self) -> Resolve0.resolve (IndexLogic0.index_logic self i) + val resolve (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) : bool + ensures { result = resolve self } + +end +module CreusotContracts_Model_ShallowModel_ShallowModelTy_Type + type self + type shallowModelTy +end +module CreusotContracts_Model_ShallowModel_ShallowModel_Stub + type self + clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with + type self = self + function shallow_model (self : self) : ShallowModelTy0.shallowModelTy +end +module CreusotContracts_Model_ShallowModel_ShallowModel_Interface + type self + clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with + type self = self + function shallow_model (self : self) : ShallowModelTy0.shallowModelTy + val shallow_model (self : self) : ShallowModelTy0.shallowModelTy + ensures { result = shallow_model self } + +end +module CreusotContracts_Model_ShallowModel_ShallowModel + type self + clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with + type self = self + function shallow_model (self : self) : ShallowModelTy0.shallowModelTy + val shallow_model (self : self) : ShallowModelTy0.shallowModelTy + ensures { result = shallow_model self } + +end +module CreusotContracts_Std1_Boxed_Impl1_ShallowModel_Stub + type t + type a + clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with + type self = t + function shallow_model (self : t) : ShallowModelTy0.shallowModelTy +end +module CreusotContracts_Std1_Boxed_Impl1_ShallowModel_Interface + type t + type a + clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with + type self = t + function shallow_model (self : t) : ShallowModelTy0.shallowModelTy + val shallow_model (self : t) : ShallowModelTy0.shallowModelTy + ensures { result = shallow_model self } + +end +module CreusotContracts_Std1_Boxed_Impl1_ShallowModel + type t + type a + clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with + type self = t + clone CreusotContracts_Model_ShallowModel_ShallowModel_Stub as ShallowModel0 with + type self = t, + type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy + function shallow_model (self : t) : ShallowModelTy0.shallowModelTy = + [#"../../../../../creusot-contracts/src/std/boxed.rs" 20 8 20 31] ShallowModel0.shallow_model self + val shallow_model (self : t) : ShallowModelTy0.shallowModelTy + ensures { result = shallow_model self } + +end +module Alloc_Slice_Impl0_IntoVec_Interface + type t + type a + use prelude.Slice + use seq.Seq + use seq.Seq + clone CreusotContracts_Invariant_Inv_Stub as Inv2 with + type t = Seq.seq t + clone Core_Num_Impl11_Max_Stub as Max0 + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Alloc_Vec_Vec_Type.t_vec t a + clone CreusotContracts_Std1_Boxed_Impl1_ShallowModel_Stub as ShallowModel1 with + type t = slice t, + type a = a, + type ShallowModelTy0.shallowModelTy = Seq.seq t + clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub as ShallowModel0 with + type t = t, + type a = a, + predicate Inv0.inv = Inv1.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv1.inv = Inv2.inv, + axiom . + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = slice t + val into_vec (self : slice t) : Alloc_Vec_Vec_Type.t_vec t a + requires {Inv0.inv self} + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 303 18 303 35] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } + ensures { Inv1.inv result } + +end +module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPre_Stub + type self + predicate into_iter_pre (self : self) +end +module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPre_Interface + type self + predicate into_iter_pre (self : self) + val into_iter_pre (self : self) : bool + ensures { result = into_iter_pre self } + +end +module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPre + type self + predicate into_iter_pre (self : self) = + [#"../../../../../creusot-contracts/src/std/iter.rs" 63 20 63 24] true + val into_iter_pre (self : self) : bool + ensures { result = into_iter_pre self } + +end +module Core_Iter_Traits_Collect_IntoIterator_IntoIter_Type + type self + type intoIter +end +module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPost_Stub + type self + clone Core_Iter_Traits_Collect_IntoIterator_IntoIter_Type as IntoIter0 with + type self = self + predicate into_iter_post (self : self) (res : IntoIter0.intoIter) +end +module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPost_Interface + type self + clone Core_Iter_Traits_Collect_IntoIterator_IntoIter_Type as IntoIter0 with + type self = self + predicate into_iter_post (self : self) (res : IntoIter0.intoIter) + val into_iter_post (self : self) (res : IntoIter0.intoIter) : bool + ensures { result = into_iter_post self res } + +end +module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPost + type self + clone Core_Iter_Traits_Collect_IntoIterator_IntoIter_Type as IntoIter0 with + type self = self + predicate into_iter_post (self : self) (res : IntoIter0.intoIter) + val into_iter_post (self : self) (res : IntoIter0.intoIter) : bool + ensures { result = into_iter_post self res } + +end +module CreusotContracts_Std1_Iter_Iterator_Completed_Stub + type self + use prelude.Borrow + predicate completed (self : borrowed self) +end +module CreusotContracts_Std1_Iter_Iterator_Completed_Interface + type self + use prelude.Borrow + predicate completed (self : borrowed self) + val completed (self : borrowed self) : bool + ensures { result = completed self } + +end +module CreusotContracts_Std1_Iter_Iterator_Completed + type self + use prelude.Borrow + predicate completed (self : borrowed self) + val completed (self : borrowed self) : bool + ensures { result = completed self } + +end +module Core_Iter_Traits_Iterator_Iterator_Item_Type + type self + type item +end +module CreusotContracts_Std1_Iter_Iterator_Produces_Stub + type self + use seq.Seq + clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with + type self = self + predicate produces (self : self) (visited : Seq.seq Item0.item) (_o : self) +end +module CreusotContracts_Std1_Iter_Iterator_Produces_Interface + type self + use seq.Seq + clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with + type self = self + predicate produces (self : self) (visited : Seq.seq Item0.item) (_o : self) + val produces (self : self) (visited : Seq.seq Item0.item) (_o : self) : bool + ensures { result = produces self visited _o } + +end +module CreusotContracts_Std1_Iter_Iterator_Produces + type self + use seq.Seq + clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with + type self = self + predicate produces (self : self) (visited : Seq.seq Item0.item) (_o : self) + val produces (self : self) (visited : Seq.seq Item0.item) (_o : self) : bool + ensures { result = produces self visited _o } + +end +module CreusotContracts_Model_Impl7_ShallowModel_Stub + type t + use prelude.Borrow + clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with + type self = t + function shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy +end +module CreusotContracts_Model_Impl7_ShallowModel_Interface + type t + use prelude.Borrow + clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with + type self = t + function shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy + val shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy + ensures { result = shallow_model self } + +end +module CreusotContracts_Model_Impl7_ShallowModel + type t + use prelude.Borrow + clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with + type self = t + clone CreusotContracts_Model_ShallowModel_ShallowModel_Stub as ShallowModel0 with + type self = t, + type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy + function shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy = + [#"../../../../../creusot-contracts/src/model.rs" 101 8 101 31] ShallowModel0.shallow_model ( * self) + val shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy + ensures { result = shallow_model self } + +end +module Alloc_Vec_Impl18_Extend_Interface + type t + type a + type i + use seq.Seq + use prelude.Borrow + clone Core_Num_Impl11_Max_Stub as Max0 + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv5 with + type t = Alloc_Vec_Vec_Type.t_vec t a + use seq.Seq + clone CreusotContracts_Model_Impl7_ShallowModel_Stub as ShallowModel1 with + type t = Alloc_Vec_Vec_Type.t_vec t a, + type ShallowModelTy0.shallowModelTy = Seq.seq t + clone CreusotContracts_Invariant_Inv_Stub as Inv2 with + type t = Seq.seq t + clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub as ShallowModel0 with + type t = t, + type a = a, + predicate Inv0.inv = Inv5.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv1.inv = Inv2.inv, + axiom . + clone Core_Iter_Traits_Collect_IntoIterator_IntoIter_Type as IntoIter0 with + type self = i + clone CreusotContracts_Std1_Iter_Iterator_Produces_Stub as Produces0 with + type self = IntoIter0.intoIter, + type Item0.item = t + clone CreusotContracts_Std1_Iter_Iterator_Completed_Stub as Completed0 with + type self = IntoIter0.intoIter + clone CreusotContracts_Std1_Iter_IntoIterator_IntoIterPost_Stub as IntoIterPost0 with + type self = i, + type IntoIter0.intoIter = IntoIter0.intoIter + clone CreusotContracts_Invariant_Inv_Stub as Inv4 with + type t = IntoIter0.intoIter + clone CreusotContracts_Invariant_Inv_Stub as Inv3 with + type t = borrowed IntoIter0.intoIter + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = i + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = borrowed (Alloc_Vec_Vec_Type.t_vec t a) + clone CreusotContracts_Std1_Iter_IntoIterator_IntoIterPre_Stub as IntoIterPre0 with + type self = i + val extend (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (iter : i) : () + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 121 27 121 47] IntoIterPre0.into_iter_pre iter} + requires {Inv0.inv self} + requires {Inv1.inv iter} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 122 16 125 18] exists prod : Seq.seq t . exists done_ : borrowed IntoIter0.intoIter . exists start_ : IntoIter0.intoIter . Inv2.inv prod /\ Inv3.inv done_ /\ Inv4.inv start_ /\ IntoIterPost0.into_iter_post iter start_ /\ Completed0.completed done_ /\ Produces0.produces start_ prod ( * done_) /\ ShallowModel0.shallow_model ( ^ self) = Seq.(++) (ShallowModel1.shallow_model self) prod } + +end +module TyInv_Trivial + type t + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = t + axiom inv_trivial : forall self : t . Inv0.inv self = true +end +module CreusotContracts_Std1_Vec_Impl4_IntoIterPre_Stub + type t + type a + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + predicate into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) +end +module CreusotContracts_Std1_Vec_Impl4_IntoIterPre_Interface + type t + type a + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + predicate into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) + val into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) : bool + ensures { result = into_iter_pre self } + +end +module CreusotContracts_Std1_Vec_Impl4_IntoIterPre + type t + type a + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + predicate into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) = + [#"../../../../../creusot-contracts/src/std/vec.rs" 168 20 168 24] true + val into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) : bool + ensures { result = into_iter_pre self } + +end +module Core_Mem_ManuallyDrop_ManuallyDrop_Type + type t_manuallydrop 't = + | C_ManuallyDrop 't + +end +module Alloc_Vec_IntoIter_IntoIter_Type + use prelude.Int + use prelude.UIntSize + use prelude.Opaque + use Core_Mem_ManuallyDrop_ManuallyDrop_Type as Core_Mem_ManuallyDrop_ManuallyDrop_Type + use Core_Marker_PhantomData_Type as Core_Marker_PhantomData_Type + use Core_Ptr_NonNull_NonNull_Type as Core_Ptr_NonNull_NonNull_Type + type t_intoiter 't 'a = + | C_IntoIter (Core_Ptr_NonNull_NonNull_Type.t_nonnull 't) (Core_Marker_PhantomData_Type.t_phantomdata 't) usize (Core_Mem_ManuallyDrop_ManuallyDrop_Type.t_manuallydrop 'a) opaque_ptr opaque_ptr + +end +module CreusotContracts_Std1_Vec_Impl7_ShallowModel_Stub + type t + type a + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + function shallow_model (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : Seq.seq t +end +module CreusotContracts_Std1_Vec_Impl7_ShallowModel_Interface + type t + type a + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + function shallow_model (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : Seq.seq t + val shallow_model (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : Seq.seq t + ensures { result = shallow_model self } + +end +module CreusotContracts_Std1_Vec_Impl7_ShallowModel + type t + type a + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + function shallow_model (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : Seq.seq t + val shallow_model (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : Seq.seq t + ensures { result = shallow_model self } + +end +module CreusotContracts_Std1_Vec_Impl4_IntoIterPost_Stub + type t + type a + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + predicate into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) +end +module CreusotContracts_Std1_Vec_Impl4_IntoIterPost_Interface + type t + type a + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + predicate into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) + val into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : bool + ensures { result = into_iter_post self res } + +end +module CreusotContracts_Std1_Vec_Impl4_IntoIterPost + type t + type a + use seq.Seq + use seq.Seq + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone Core_Num_Impl11_Max_Stub as Max0 + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_Vec_Type.t_vec t a + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Std1_Vec_Impl7_ShallowModel_Stub as ShallowModel1 with + type t = t, + type a = a + clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub as ShallowModel0 with + type t = t, + type a = a, + predicate Inv0.inv = Inv0.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv1.inv = Inv1.inv, + axiom . + predicate into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) + = + [#"../../../../../creusot-contracts/src/std/vec.rs" 174 20 174 33] ShallowModel0.shallow_model self = ShallowModel1.shallow_model res + val into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : bool + ensures { result = into_iter_post self res } + +end +module CreusotContracts_Resolve_Impl1_Resolve_Stub + type t + use prelude.Borrow + predicate resolve (self : borrowed t) +end +module CreusotContracts_Resolve_Impl1_Resolve_Interface + type t + use prelude.Borrow + predicate resolve (self : borrowed t) + val resolve (self : borrowed t) : bool + ensures { result = resolve self } + +end +module CreusotContracts_Resolve_Impl1_Resolve + type t + use prelude.Borrow + predicate resolve (self : borrowed t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self + val resolve (self : borrowed t) : bool + ensures { result = resolve self } + +end +module CreusotContracts_Std1_Vec_Impl8_Completed_Stub + type t + type a + use prelude.Borrow + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + predicate completed (self : borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a)) +end +module CreusotContracts_Std1_Vec_Impl8_Completed_Interface + type t + type a + use prelude.Borrow + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + predicate completed (self : borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a)) + val completed (self : borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a)) : bool + ensures { result = completed self } + +end +module CreusotContracts_Std1_Vec_Impl8_Completed + type t + type a + use prelude.Borrow + use seq.Seq + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Model_Impl7_ShallowModel_Stub as ShallowModel0 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, + type ShallowModelTy0.shallowModelTy = Seq.seq t + clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a + predicate completed (self : borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a)) = + [#"../../../../../creusot-contracts/src/std/vec.rs" 230 20 230 57] Resolve0.resolve self /\ ShallowModel0.shallow_model self = Seq.empty + val completed (self : borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a)) : bool + ensures { result = completed self } + +end +module CreusotContracts_Std1_Vec_Impl8_Produces_Stub + type t + type a + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + predicate produces (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (visited : Seq.seq t) (rhs : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) + +end +module CreusotContracts_Std1_Vec_Impl8_Produces_Interface + type t + type a + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + predicate produces (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (visited : Seq.seq t) (rhs : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) + + val produces (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (visited : Seq.seq t) (rhs : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : bool + ensures { result = produces self visited rhs } + +end +module CreusotContracts_Std1_Vec_Impl8_Produces + type t + type a + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Std1_Vec_Impl7_ShallowModel_Stub as ShallowModel0 with + type t = t, + type a = a + predicate produces (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (visited : Seq.seq t) (rhs : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) + + = + [#"../../../../../creusot-contracts/src/std/vec.rs" 237 12 237 41] ShallowModel0.shallow_model self = Seq.(++) visited (ShallowModel0.shallow_model rhs) + val produces (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (visited : Seq.seq t) (rhs : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : bool + ensures { result = produces self visited rhs } + +end +module CreusotContracts_Resolve_Impl2_Resolve_Stub + type t + predicate resolve (self : t) +end +module CreusotContracts_Resolve_Impl2_Resolve_Interface + type t + predicate resolve (self : t) + val resolve (self : t) : bool + ensures { result = resolve self } + +end +module CreusotContracts_Resolve_Impl2_Resolve + type t + predicate resolve (self : t) = + [#"../../../../../creusot-contracts/src/resolve.rs" 36 8 36 12] true + val resolve (self : t) : bool + ensures { result = resolve self } + +end +module Alloc_Boxed_Box_Type + use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type + type t_box 't 'a = + | C_Box (Core_Ptr_Unique_Unique_Type.t_unique 't) 'a + +end +module CreusotContracts_Std1_Slice_Impl0_ShallowModel_Stub + type t + use seq.Seq + use prelude.UIntSize + use prelude.Int + use prelude.Slice + use seq.Seq + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone Core_Num_Impl11_Max_Stub as Max0 + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = slice t + function shallow_model (self : slice t) : Seq.seq t +end +module CreusotContracts_Std1_Slice_Impl0_ShallowModel_Interface + type t + use seq.Seq + use prelude.UIntSize + use prelude.Int + use prelude.Slice + use seq.Seq + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone Core_Num_Impl11_Max_Stub as Max0 + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = slice t + function shallow_model (self : slice t) : Seq.seq t + val shallow_model (self : slice t) : Seq.seq t + requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 19 21 19 25] Inv0.inv self} + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 17 14 17 41] Seq.length result <= UIntSize.to_int Max0.mAX' } + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 18 14 18 41] result = Slice.id self } + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 19 4 19 50] Inv1.inv result } + ensures { result = shallow_model self } + + axiom shallow_model_spec : forall self : slice t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 19 4 19 50] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/slice.rs" 18 14 18 41] shallow_model self = Slice.id self) && ([#"../../../../../creusot-contracts/src/std/slice.rs" 17 14 17 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX') +end +module CreusotContracts_Std1_Slice_Impl0_ShallowModel + type t + use seq.Seq + use prelude.UIntSize + use prelude.Int + use prelude.Slice + use seq.Seq + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone Core_Num_Impl11_Max_Stub as Max0 + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = slice t + function shallow_model (self : slice t) : Seq.seq t + val shallow_model (self : slice t) : Seq.seq t + requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 19 21 19 25] Inv0.inv self} + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 17 14 17 41] Seq.length result <= UIntSize.to_int Max0.mAX' } + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 18 14 18 41] result = Slice.id self } + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 19 4 19 50] Inv1.inv result } + ensures { result = shallow_model self } + + axiom shallow_model_spec : forall self : slice t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 19 4 19 50] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/slice.rs" 18 14 18 41] shallow_model self = Slice.id self) && ([#"../../../../../creusot-contracts/src/std/slice.rs" 17 14 17 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX') +end +module CreusotContracts_Std1_Vec_Impl8_ProducesRefl_Stub + type t + type a + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Std1_Vec_Impl8_Produces_Stub as Produces0 with + type t = t, + type a = a + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a + function produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () +end +module CreusotContracts_Std1_Vec_Impl8_ProducesRefl_Interface + type t + type a + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Std1_Vec_Impl8_Produces_Stub as Produces0 with + type t = t, + type a = a + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a + function produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () + val produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a } + ensures { result = produces_refl a } + + axiom produces_refl_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a) +end +module CreusotContracts_Std1_Vec_Impl8_ProducesRefl + type t + type a + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Std1_Vec_Impl8_Produces_Stub as Produces0 with + type t = t, + type a = a + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a + function produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () = + [#"../../../../../creusot-contracts/src/std/vec.rs" 241 4 241 10] () + val produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a } + ensures { result = produces_refl a } + + axiom produces_refl_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a) +end +module CreusotContracts_Std1_Vec_Impl8_ProducesTrans_Stub + type t + type a + use seq.Seq + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a + clone CreusotContracts_Std1_Vec_Impl8_Produces_Stub as Produces0 with + type t = t, + type a = a + function produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () + +end +module CreusotContracts_Std1_Vec_Impl8_ProducesTrans_Interface + type t + type a + use seq.Seq + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a + clone CreusotContracts_Std1_Vec_Impl8_Produces_Stub as Produces0 with + type t = t, + type a = a + function produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () + + val produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c } + ensures { result = produces_trans a ab b bc c } + + axiom produces_trans_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, ab : Seq.seq t, b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, bc : Seq.seq t, c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c) +end +module CreusotContracts_Std1_Vec_Impl8_ProducesTrans + type t + type a + use seq.Seq + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = Seq.seq t + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a + clone CreusotContracts_Std1_Vec_Impl8_Produces_Stub as Produces0 with + type t = t, + type a = a + function produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () + + = + [#"../../../../../creusot-contracts/src/std/vec.rs" 246 4 246 10] () + val produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c } + ensures { result = produces_trans a ab b bc c } + + axiom produces_trans_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, ab : Seq.seq t, b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, bc : Seq.seq t, c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c) +end +module C874_CanExtend_Interface + val can_extend [#"../874.rs" 4 0 4 19] (_1 : ()) : () +end +module C874_CanExtend + use prelude.Int + use prelude.Int32 + use prelude.Borrow + use seq.Seq + use prelude.Slice + clone CreusotContracts_Invariant_Inv_Interface as Inv6 with + type t = slice int32 + clone TyInv_Trivial as TyInv_Trivial6 with + type t = slice int32, + predicate Inv0.inv = Inv6.inv, + axiom . + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Std1_Vec_Impl7_ShallowModel_Interface as ShallowModel4 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global + use seq.Seq + clone CreusotContracts_Model_Impl7_ShallowModel as ShallowModel5 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter int32 (Alloc_Alloc_Global_Type.t_global), + type ShallowModelTy0.shallowModelTy = Seq.seq int32, + function ShallowModel0.shallow_model = ShallowModel4.shallow_model + clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter int32 (Alloc_Alloc_Global_Type.t_global) + clone CreusotContracts_Invariant_Inv_Interface as Inv2 with + type t = Seq.seq int32 + clone CreusotContracts_Invariant_Inv_Interface as Inv5 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter int32 (Alloc_Alloc_Global_Type.t_global) + clone CreusotContracts_Std1_Vec_Impl8_Produces as Produces0 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global, + function ShallowModel0.shallow_model = ShallowModel4.shallow_model + clone CreusotContracts_Std1_Vec_Impl8_ProducesTrans as ProducesTrans0 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global, + predicate Produces0.produces = Produces0.produces, + predicate Inv0.inv = Inv5.inv, + predicate Inv1.inv = Inv2.inv, + axiom . + clone CreusotContracts_Std1_Vec_Impl8_ProducesRefl as ProducesRefl0 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global, + predicate Inv0.inv = Inv5.inv, + predicate Produces0.produces = Produces0.produces, + axiom . + clone TyInv_Trivial as TyInv_Trivial5 with + type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter int32 (Alloc_Alloc_Global_Type.t_global), + predicate Inv0.inv = Inv5.inv, + axiom . + clone CreusotContracts_Invariant_Inv_Interface as Inv4 with + type t = borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter int32 (Alloc_Alloc_Global_Type.t_global)) + clone TyInv_Trivial as TyInv_Trivial4 with + type t = borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter int32 (Alloc_Alloc_Global_Type.t_global)), + predicate Inv0.inv = Inv4.inv, + axiom . + use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type + clone CreusotContracts_Invariant_Inv_Interface as Inv3 with + type t = borrowed (Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global)) + clone TyInv_Trivial as TyInv_Trivial3 with + type t = borrowed (Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global)), + predicate Inv0.inv = Inv3.inv, + axiom . + clone TyInv_Trivial as TyInv_Trivial2 with + type t = Seq.seq int32, + predicate Inv0.inv = Inv2.inv, + axiom . + clone CreusotContracts_Invariant_Inv_Interface as Inv1 with + type t = Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global) + clone TyInv_Trivial as TyInv_Trivial1 with + type t = Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global), + predicate Inv0.inv = Inv1.inv, + axiom . + clone Core_Num_Impl11_Max as Max0 + clone CreusotContracts_Std1_Slice_Impl0_ShallowModel_Interface as ShallowModel3 with + type t = int32, + predicate Inv0.inv = Inv6.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv1.inv = Inv2.inv, + axiom . + clone CreusotContracts_Invariant_Inv_Interface as Inv0 with + type t = slice int32 + clone TyInv_Trivial as TyInv_Trivial0 with + type t = slice int32, + predicate Inv0.inv = Inv0.inv, + axiom . + clone CreusotContracts_Resolve_Impl2_Resolve as Resolve1 with + type t = int32 + clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Interface as ShallowModel0 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global, + predicate Inv0.inv = Inv1.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv1.inv = Inv2.inv, + axiom . + clone CreusotContracts_Logic_Ops_Impl0_IndexLogic as IndexLogic0 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global, + function ShallowModel0.shallow_model = ShallowModel0.shallow_model, + predicate Inv0.inv = Inv1.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv1.inv = Inv2.inv + clone CreusotContracts_Model_Impl7_ShallowModel as ShallowModel2 with + type t = Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global), + type ShallowModelTy0.shallowModelTy = Seq.seq int32, + function ShallowModel0.shallow_model = ShallowModel0.shallow_model + clone CreusotContracts_Std1_Vec_Impl8_Completed as Completed0 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global, + predicate Resolve0.resolve = Resolve2.resolve, + function ShallowModel0.shallow_model = ShallowModel5.shallow_model + clone CreusotContracts_Std1_Vec_Impl4_IntoIterPost as IntoIterPost0 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global, + function ShallowModel0.shallow_model = ShallowModel0.shallow_model, + function ShallowModel1.shallow_model = ShallowModel4.shallow_model, + predicate Inv0.inv = Inv1.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv1.inv = Inv2.inv + clone CreusotContracts_Std1_Vec_Impl4_IntoIterPre as IntoIterPre0 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global + clone CreusotContracts_Std1_Boxed_Impl1_ShallowModel as ShallowModel1 with + type t = slice int32, + type a = Alloc_Alloc_Global_Type.t_global, + type ShallowModelTy0.shallowModelTy = Seq.seq int32, + function ShallowModel0.shallow_model = ShallowModel3.shallow_model + clone CreusotContracts_Std1_Vec_Impl10_Resolve as Resolve0 with + type t = int32, + function ShallowModel0.shallow_model = ShallowModel0.shallow_model, + function IndexLogic0.index_logic = IndexLogic0.index_logic, + predicate Resolve0.resolve = Resolve1.resolve, + predicate Inv0.inv = Inv1.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv1.inv = Inv2.inv + clone Alloc_Vec_Impl18_Extend_Interface as Extend0 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global, + type i = Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global), + predicate IntoIterPre0.into_iter_pre = IntoIterPre0.into_iter_pre, + predicate Inv0.inv = Inv3.inv, + predicate Inv1.inv = Inv1.inv, + predicate Inv5.inv = Inv1.inv, + type IntoIter0.intoIter = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter int32 (Alloc_Alloc_Global_Type.t_global), + predicate Inv2.inv = Inv2.inv, + predicate Inv3.inv = Inv4.inv, + predicate Inv4.inv = Inv5.inv, + predicate IntoIterPost0.into_iter_post = IntoIterPost0.into_iter_post, + predicate Completed0.completed = Completed0.completed, + predicate Produces0.produces = Produces0.produces, + function ShallowModel0.shallow_model = ShallowModel0.shallow_model, + function ShallowModel1.shallow_model = ShallowModel2.shallow_model, + val Max0.mAX' = Max0.mAX' + clone Alloc_Slice_Impl0_IntoVec_Interface as IntoVec0 with + type t = int32, + type a = Alloc_Alloc_Global_Type.t_global, + predicate Inv0.inv = Inv0.inv, + function ShallowModel0.shallow_model = ShallowModel0.shallow_model, + function ShallowModel1.shallow_model = ShallowModel1.shallow_model, + predicate Inv1.inv = Inv1.inv, + val Max0.mAX' = Max0.mAX', + predicate Inv2.inv = Inv2.inv + let rec cfg can_extend [#"../874.rs" 4 0 4 19] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : () + = [@vc:do_not_keep_trace] [@vc:sp] + var _0 : (); + var v : Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global); + var w : Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global); + var _9 : (); + var _10 : borrowed (Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global)); + var z : Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global); + { + goto BB0 + } + BB0 { + goto BB1 + } + BB1 { + goto BB2 + } + BB2 { + v <- ([#"../874.rs" 5 16 5 29] IntoVec0.into_vec (Slice.create 3 [|[#"../874.rs" 5 21 5 22] (1 : int32); [#"../874.rs" 5 24 5 25] (2 : int32); [#"../874.rs" 5 27 5 28] (3 : int32)|])); + goto BB3 + } + BB3 { + goto BB4 + } + BB4 { + goto BB5 + } + BB5 { + w <- ([#"../874.rs" 6 12 6 25] IntoVec0.into_vec (Slice.create 3 [|[#"../874.rs" 6 17 6 18] (4 : int32); [#"../874.rs" 6 20 6 21] (5 : int32); [#"../874.rs" 6 23 6 24] (6 : int32)|])); + goto BB6 + } + BB6 { + _10 <- Borrow.borrow_mut v; + v <- ^ _10; + _9 <- ([#"../874.rs" 7 4 7 15] Extend0.extend _10 w); + _10 <- any borrowed (Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global)); + w <- any Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global); + goto BB7 + } + BB7 { + assume { Resolve0.resolve v }; + goto BB8 + } + BB8 { + goto BB9 + } + BB9 { + z <- ([#"../874.rs" 9 12 9 34] IntoVec0.into_vec (Slice.create 6 [|[#"../874.rs" 9 17 9 18] (1 : int32); [#"../874.rs" 9 20 9 21] (2 : int32); [#"../874.rs" 9 23 9 24] (3 : int32); [#"../874.rs" 9 26 9 27] (4 : int32); [#"../874.rs" 9 29 9 30] (5 : int32); [#"../874.rs" 9 32 9 33] (6 : int32)|])); + goto BB10 + } + BB10 { + assume { Resolve0.resolve z }; + assert { [@expl:assertion] [#"../874.rs" 10 4 10 32] Seq.(==) (ShallowModel0.shallow_model z) (ShallowModel0.shallow_model v) }; + goto BB11 + } + BB11 { + _0 <- (); + goto BB12 + } + BB12 { + goto BB13 + } + BB13 { + goto BB14 + } + BB14 { + return _0 + } + +end diff --git a/creusot/tests/should_succeed/bug/874.rs b/creusot/tests/should_succeed/bug/874.rs new file mode 100644 index 0000000000..cfbaee2a2e --- /dev/null +++ b/creusot/tests/should_succeed/bug/874.rs @@ -0,0 +1,11 @@ +extern crate creusot_contracts; +use creusot_contracts::{vec, *}; + +pub fn can_extend() { + let mut v = vec![1, 2, 3]; + let w = vec![4, 5, 6]; + v.extend(w); + + let z = vec![1, 2, 3, 4, 5, 6]; + proof_assert!(z@.ext_eq(v@)); +} diff --git a/creusot/tests/should_succeed/bug/874/why3session.xml b/creusot/tests/should_succeed/bug/874/why3session.xml new file mode 100644 index 0000000000..507eab5980 --- /dev/null +++ b/creusot/tests/should_succeed/bug/874/why3session.xml @@ -0,0 +1,37 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/bug/874/why3shapes.gz b/creusot/tests/should_succeed/bug/874/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..4d962f2ae04f075219308d3b239782d0c00f5d4c GIT binary patch literal 931 zcmV;U16=$ciwFP!00000|D9CJZX-7kyz47;OX9t-yZM?R0wM$!=pP_*ioqc{Spl-f zktTAoU!UeYJeJ10N$i7FY_hwH)y4V#Zhih7p7VKq$*1$aJ^r}X>$@LT-5+6pym+x& zh38Y7{*3wTA$y&Fk@ zHxndpCn$Y2LG&OdtULf${b>^p`S^SHIq>ZchxX<1sZIId0Yle5?vGt~+Wz|8Hf)yr z`^5jZeci=oPmO=4ZrTHVy&DT4uiGt)mNO3{aml4NAs@PPXhS^Z(B(*(LqB`qZN1;` zBSi`u#t|b903r;a%&Kq-?dtiIV|z^djt9EBy(EOobpSb|rw}eP0k~ygJlMiOM_u|^ zW}pTDQ4U~c0Pl2tS#*W5?Mpd*7alG_bmoch(9cI~+fFMM=6Sa1Y19xI-!?(gqc;grwq;gXs2 ztQ}6;=|MZ>CqeuEZ?A$dSLwmt zyno`)HO;ycjqjgmeE&p)xSRe{pVvhLKy{`pf)q;Fihy*}NT{t+ z6im~THV(BzW F00279$A|y` literal 0 HcmV?d00001 diff --git a/creusot/tests/should_succeed/cell/02.mlcfg b/creusot/tests/should_succeed/cell/02.mlcfg index 70a530ec15..c9319eff17 100644 --- a/creusot/tests/should_succeed/cell/02.mlcfg +++ b/creusot/tests/should_succeed/cell/02.mlcfg @@ -624,10 +624,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/filter_positive.mlcfg b/creusot/tests/should_succeed/filter_positive.mlcfg index 441559f072..095aaab518 100644 --- a/creusot/tests/should_succeed/filter_positive.mlcfg +++ b/creusot/tests/should_succeed/filter_positive.mlcfg @@ -514,8 +514,8 @@ module Alloc_Vec_FromElem_Interface type t = t val from_elem (elem : t) (n : usize) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) requires {Inv0.inv elem} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 155 22 155 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 156 12 156 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 157 22 157 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 158 12 158 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } ensures { Inv1.inv result } end @@ -618,10 +618,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -733,13 +733,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/hashmap.mlcfg b/creusot/tests/should_succeed/hashmap.mlcfg index d31ded8645..09fb2ab47a 100644 --- a/creusot/tests/should_succeed/hashmap.mlcfg +++ b/creusot/tests/should_succeed/hashmap.mlcfg @@ -762,8 +762,8 @@ module Alloc_Vec_FromElem_Interface type t = t val from_elem (elem : t) (n : usize) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) requires {Inv0.inv elem} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 155 22 155 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 156 12 156 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 157 22 157 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 158 12 158 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } ensures { Inv1.inv result } end @@ -1278,13 +1278,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end @@ -1955,10 +1955,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/heapsort_generic.mlcfg b/creusot/tests/should_succeed/heapsort_generic.mlcfg index 3dff045d62..8ce519abec 100644 --- a/creusot/tests/should_succeed/heapsort_generic.mlcfg +++ b/creusot/tests/should_succeed/heapsort_generic.mlcfg @@ -1347,10 +1347,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -1531,8 +1531,8 @@ module Alloc_Vec_Impl9_DerefMut_Interface type t = borrowed (Alloc_Vec_Vec_Type.t_vec t a) val deref_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) : borrowed (slice t) requires {Inv0.inv self} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 150 26 150 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 151 26 151 48] ShallowModel2.shallow_model ( ^ result) = ShallowModel3.shallow_model ( ^ self) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 152 26 152 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 153 26 153 48] ShallowModel2.shallow_model ( ^ result) = ShallowModel3.shallow_model ( ^ self) } ensures { Inv1.inv result } end diff --git a/creusot/tests/should_succeed/hillel.mlcfg b/creusot/tests/should_succeed/hillel.mlcfg index 191b53dcdc..bb761b7daf 100644 --- a/creusot/tests/should_succeed/hillel.mlcfg +++ b/creusot/tests/should_succeed/hillel.mlcfg @@ -1554,7 +1554,7 @@ module Alloc_Vec_Impl8_Deref_Interface type t = Alloc_Vec_Vec_Type.t_vec t a val deref (self : Alloc_Vec_Vec_Type.t_vec t a) : slice t requires {Inv0.inv self} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 145 26 145 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 147 26 147 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } ensures { Inv1.inv result } end diff --git a/creusot/tests/should_succeed/index_range.mlcfg b/creusot/tests/should_succeed/index_range.mlcfg index 0e9de15765..39bcb73b87 100644 --- a/creusot/tests/should_succeed/index_range.mlcfg +++ b/creusot/tests/should_succeed/index_range.mlcfg @@ -684,10 +684,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -729,7 +729,7 @@ module Alloc_Vec_Impl8_Deref_Interface type t = Alloc_Vec_Vec_Type.t_vec t a val deref (self : Alloc_Vec_Vec_Type.t_vec t a) : slice t requires {Inv0.inv self} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 145 26 145 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 147 26 147 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } ensures { Inv1.inv result } end @@ -860,13 +860,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg b/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg index 9c88b286f0..fa54f27062 100644 --- a/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg +++ b/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg @@ -1302,13 +1302,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg b/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg index 545bcef790..ae30d61ec1 100644 --- a/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg +++ b/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg @@ -1042,7 +1042,7 @@ module CreusotContracts_Std1_Vec_Impl5_IntoIterPre use prelude.Borrow use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type predicate into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 180 20 180 24] true + [#"../../../../../creusot-contracts/src/std/vec.rs" 182 20 182 24] true val into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) : bool ensures { result = into_iter_pre self } @@ -1084,7 +1084,7 @@ module CreusotContracts_Std1_Vec_Impl5_IntoIterPost type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t predicate into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Core_Slice_Iter_Iter_Type.t_iter t) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 186 20 186 34] ShallowModel0.shallow_model self = ShallowModel2.shallow_model (ShallowModel1.shallow_model res) + [#"../../../../../creusot-contracts/src/std/vec.rs" 188 20 188 34] ShallowModel0.shallow_model self = ShallowModel2.shallow_model (ShallowModel1.shallow_model res) val into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Core_Slice_Iter_Iter_Type.t_iter t) : bool ensures { result = into_iter_post self res } @@ -1846,8 +1846,8 @@ module Alloc_Vec_Impl9_DerefMut_Interface type t = borrowed (Alloc_Vec_Vec_Type.t_vec t a) val deref_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) : borrowed (slice t) requires {Inv0.inv self} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 150 26 150 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 151 26 151 48] ShallowModel2.shallow_model ( ^ result) = ShallowModel3.shallow_model ( ^ self) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 152 26 152 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 153 26 153 48] ShallowModel2.shallow_model ( ^ result) = ShallowModel3.shallow_model ( ^ self) } ensures { Inv1.inv result } end @@ -3804,7 +3804,7 @@ module Alloc_Vec_Impl8_Deref_Interface type t = Alloc_Vec_Vec_Type.t_vec t a val deref (self : Alloc_Vec_Vec_Type.t_vec t a) : slice t requires {Inv0.inv self} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 145 26 145 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 147 26 147 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } ensures { Inv1.inv result } end @@ -4316,7 +4316,7 @@ module CreusotContracts_Std1_Vec_Impl9_FromIterPost predicate Inv1.inv = Inv1.inv, axiom . predicate from_iter_post (prod : Seq.seq t) (res : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 256 20 256 32] prod = ShallowModel0.shallow_model res + [#"../../../../../creusot-contracts/src/std/vec.rs" 258 20 258 32] prod = ShallowModel0.shallow_model res val from_iter_post (prod : Seq.seq t) (res : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) : bool ensures { result = from_iter_post prod res } diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg b/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg index 814a1167f4..1a4b747819 100644 --- a/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg +++ b/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg @@ -1449,7 +1449,7 @@ module Alloc_Vec_Impl8_Deref_Interface type t = Alloc_Vec_Vec_Type.t_vec t a val deref (self : Alloc_Vec_Vec_Type.t_vec t a) : slice t requires {Inv0.inv self} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 145 26 145 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 147 26 147 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } ensures { Inv1.inv result } end @@ -1489,7 +1489,7 @@ module CreusotContracts_Std1_Vec_Impl4_IntoIterPre type a use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type predicate into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 166 20 166 24] true + [#"../../../../../creusot-contracts/src/std/vec.rs" 168 20 168 24] true val into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) : bool ensures { result = into_iter_pre self } @@ -1562,7 +1562,7 @@ module CreusotContracts_Std1_Vec_Impl4_IntoIterPost axiom . predicate into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 172 20 172 33] ShallowModel0.shallow_model self = ShallowModel1.shallow_model res + [#"../../../../../creusot-contracts/src/std/vec.rs" 174 20 174 33] ShallowModel0.shallow_model self = ShallowModel1.shallow_model res val into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : bool ensures { result = into_iter_post self res } @@ -1619,7 +1619,7 @@ module CreusotContracts_Std1_Vec_Impl8_Completed clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a predicate completed (self : borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a)) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 228 20 228 57] Resolve0.resolve self /\ ShallowModel0.shallow_model self = Seq.empty + [#"../../../../../creusot-contracts/src/std/vec.rs" 230 20 230 57] Resolve0.resolve self /\ ShallowModel0.shallow_model self = Seq.empty val completed (self : borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a)) : bool ensures { result = completed self } @@ -1654,7 +1654,7 @@ module CreusotContracts_Std1_Vec_Impl8_Produces predicate produces (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (visited : Seq.seq t) (rhs : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 235 12 235 41] ShallowModel0.shallow_model self = Seq.(++) visited (ShallowModel0.shallow_model rhs) + [#"../../../../../creusot-contracts/src/std/vec.rs" 237 12 237 41] ShallowModel0.shallow_model self = Seq.(++) visited (ShallowModel0.shallow_model rhs) val produces (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (visited : Seq.seq t) (rhs : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : bool ensures { result = produces self visited rhs } @@ -1760,11 +1760,11 @@ module CreusotContracts_Std1_Vec_Impl8_ProducesRefl_Interface type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a function produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () val produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 242 21 242 22] Inv0.inv a} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 241 14 241 39] Produces0.produces a (Seq.empty ) a } + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a } ensures { result = produces_refl a } - axiom produces_refl_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 242 21 242 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 241 14 241 39] Produces0.produces a (Seq.empty ) a) + axiom produces_refl_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a) end module CreusotContracts_Std1_Vec_Impl8_ProducesRefl type t @@ -1777,13 +1777,13 @@ module CreusotContracts_Std1_Vec_Impl8_ProducesRefl clone CreusotContracts_Invariant_Inv_Stub as Inv0 with type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a function produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () = - [#"../../../../../creusot-contracts/src/std/vec.rs" 239 4 239 10] () + [#"../../../../../creusot-contracts/src/std/vec.rs" 241 4 241 10] () val produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 242 21 242 22] Inv0.inv a} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 241 14 241 39] Produces0.produces a (Seq.empty ) a } + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a } ensures { result = produces_refl a } - axiom produces_refl_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 242 21 242 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 241 14 241 39] Produces0.produces a (Seq.empty ) a) + axiom produces_refl_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a) end module CreusotContracts_Std1_Vec_Impl8_ProducesTrans_Stub type t @@ -1817,17 +1817,17 @@ module CreusotContracts_Std1_Vec_Impl8_ProducesTrans_Interface function produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () val produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 246 15 246 32] Produces0.produces a ab b} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 247 15 247 32] Produces0.produces b bc c} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 22 249 23] Inv0.inv a} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 31 249 33] Inv1.inv ab} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 43 249 44] Inv0.inv b} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 52 249 54] Inv1.inv bc} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 64 249 65] Inv0.inv c} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 248 14 248 42] Produces0.produces a (Seq.(++) ab bc) c } + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c } ensures { result = produces_trans a ab b bc c } - axiom produces_trans_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, ab : Seq.seq t, b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, bc : Seq.seq t, c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 246 15 246 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 247 15 247 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 22 249 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 31 249 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 43 249 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 52 249 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 64 249 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 248 14 248 42] Produces0.produces a (Seq.(++) ab bc) c) + axiom produces_trans_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, ab : Seq.seq t, b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, bc : Seq.seq t, c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c) end module CreusotContracts_Std1_Vec_Impl8_ProducesTrans type t @@ -1845,19 +1845,19 @@ module CreusotContracts_Std1_Vec_Impl8_ProducesTrans function produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () = - [#"../../../../../creusot-contracts/src/std/vec.rs" 244 4 244 10] () + [#"../../../../../creusot-contracts/src/std/vec.rs" 246 4 246 10] () val produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 246 15 246 32] Produces0.produces a ab b} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 247 15 247 32] Produces0.produces b bc c} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 22 249 23] Inv0.inv a} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 31 249 33] Inv1.inv ab} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 43 249 44] Inv0.inv b} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 52 249 54] Inv1.inv bc} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 64 249 65] Inv0.inv c} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 248 14 248 42] Produces0.produces a (Seq.(++) ab bc) c } + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c } ensures { result = produces_trans a ab b bc c } - axiom produces_trans_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, ab : Seq.seq t, b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, bc : Seq.seq t, c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 246 15 246 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 247 15 247 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 22 249 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 31 249 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 43 249 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 52 249 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 64 249 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 248 14 248 42] Produces0.produces a (Seq.(++) ab bc) c) + axiom produces_trans_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, ab : Seq.seq t, b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, bc : Seq.seq t, c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c) end module C08CollectExtend_ExtendIndex_Interface use prelude.Int diff --git a/creusot/tests/should_succeed/knapsack.mlcfg b/creusot/tests/should_succeed/knapsack.mlcfg index 5e3ae0ea69..a6c204c396 100644 --- a/creusot/tests/should_succeed/knapsack.mlcfg +++ b/creusot/tests/should_succeed/knapsack.mlcfg @@ -493,8 +493,8 @@ module Alloc_Vec_FromElem_Interface type t = t val from_elem (elem : t) (n : usize) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) requires {Inv0.inv elem} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 155 22 155 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 156 12 156 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 157 22 157 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 158 12 158 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } ensures { Inv1.inv result } end @@ -641,10 +641,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -788,13 +788,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/knapsack_full.mlcfg b/creusot/tests/should_succeed/knapsack_full.mlcfg index 07e593f0f9..a23606dbcf 100644 --- a/creusot/tests/should_succeed/knapsack_full.mlcfg +++ b/creusot/tests/should_succeed/knapsack_full.mlcfg @@ -1171,8 +1171,8 @@ module Alloc_Vec_FromElem_Interface type t = t val from_elem (elem : t) (n : usize) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) requires {Inv0.inv elem} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 155 22 155 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 156 12 156 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 157 22 157 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 158 12 158 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } ensures { Inv1.inv result } end @@ -1435,10 +1435,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -1612,13 +1612,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/list_reversal_lasso.mlcfg b/creusot/tests/should_succeed/list_reversal_lasso.mlcfg index f63919199d..7da4d52c65 100644 --- a/creusot/tests/should_succeed/list_reversal_lasso.mlcfg +++ b/creusot/tests/should_succeed/list_reversal_lasso.mlcfg @@ -434,10 +434,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -749,13 +749,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/selection_sort_generic.mlcfg b/creusot/tests/should_succeed/selection_sort_generic.mlcfg index a8c3170b8c..a08fe7199a 100644 --- a/creusot/tests/should_succeed/selection_sort_generic.mlcfg +++ b/creusot/tests/should_succeed/selection_sort_generic.mlcfg @@ -972,10 +972,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -1154,8 +1154,8 @@ module Alloc_Vec_Impl9_DerefMut_Interface type t = borrowed (Alloc_Vec_Vec_Type.t_vec t a) val deref_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) : borrowed (slice t) requires {Inv0.inv self} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 150 26 150 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 151 26 151 48] ShallowModel2.shallow_model ( ^ result) = ShallowModel3.shallow_model ( ^ self) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 152 26 152 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 153 26 153 48] ShallowModel2.shallow_model ( ^ result) = ShallowModel3.shallow_model ( ^ self) } ensures { Inv1.inv result } end diff --git a/creusot/tests/should_succeed/sparse_array.mlcfg b/creusot/tests/should_succeed/sparse_array.mlcfg index 5f8c26a854..8d072c1b63 100644 --- a/creusot/tests/should_succeed/sparse_array.mlcfg +++ b/creusot/tests/should_succeed/sparse_array.mlcfg @@ -522,10 +522,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -1185,13 +1185,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end @@ -1643,8 +1643,8 @@ module Alloc_Vec_FromElem_Interface type t = t val from_elem (elem : t) (n : usize) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) requires {Inv0.inv elem} - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 155 22 155 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } - ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 156 12 156 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 157 22 157 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } + ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 158 12 158 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } ensures { Inv1.inv result } end diff --git a/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg b/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg index 8b7869b2d0..9754193cfc 100644 --- a/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg +++ b/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg @@ -282,8 +282,8 @@ module Alloc_Vec_FromElem_Interface type t = t val from_elem (elem : t) (n : usize) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) requires {Inv0.inv elem} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 155 22 155 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 156 12 156 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 157 22 157 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 158 12 158 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } ensures { Inv1.inv result } end diff --git a/creusot/tests/should_succeed/vector/01.mlcfg b/creusot/tests/should_succeed/vector/01.mlcfg index d8aa1578a2..646ae58fbc 100644 --- a/creusot/tests/should_succeed/vector/01.mlcfg +++ b/creusot/tests/should_succeed/vector/01.mlcfg @@ -709,13 +709,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/vector/02_gnome.mlcfg b/creusot/tests/should_succeed/vector/02_gnome.mlcfg index e6b66f5753..852761acaf 100644 --- a/creusot/tests/should_succeed/vector/02_gnome.mlcfg +++ b/creusot/tests/should_succeed/vector/02_gnome.mlcfg @@ -746,10 +746,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -906,8 +906,8 @@ module Alloc_Vec_Impl9_DerefMut_Interface type t = borrowed (Alloc_Vec_Vec_Type.t_vec t a) val deref_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) : borrowed (slice t) requires {Inv0.inv self} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 150 26 150 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 151 26 151 48] ShallowModel2.shallow_model ( ^ result) = ShallowModel3.shallow_model ( ^ self) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 152 26 152 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 153 26 153 48] ShallowModel2.shallow_model ( ^ result) = ShallowModel3.shallow_model ( ^ self) } ensures { Inv1.inv result } end diff --git a/creusot/tests/should_succeed/vector/02_gnome/why3session.xml b/creusot/tests/should_succeed/vector/02_gnome/why3session.xml index 09e3ce664b..0f176444fb 100644 --- a/creusot/tests/should_succeed/vector/02_gnome/why3session.xml +++ b/creusot/tests/should_succeed/vector/02_gnome/why3session.xml @@ -2,7 +2,7 @@ - + @@ -16,7 +16,7 @@ - + @@ -25,13 +25,13 @@ - + - + @@ -40,10 +40,10 @@ - + - + @@ -58,13 +58,13 @@ - + - + @@ -73,35 +73,35 @@ - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg b/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg index fdfbec34f6..b36c780a28 100644 --- a/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg +++ b/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg @@ -669,8 +669,8 @@ module Alloc_Vec_Impl9_DerefMut_Interface type t = borrowed (Alloc_Vec_Vec_Type.t_vec t a) val deref_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) : borrowed (slice t) requires {Inv0.inv self} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 150 26 150 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 151 26 151 48] ShallowModel2.shallow_model ( ^ result) = ShallowModel3.shallow_model ( ^ self) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 152 26 152 42] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 153 26 153 48] ShallowModel2.shallow_model ( ^ result) = ShallowModel3.shallow_model ( ^ self) } ensures { Inv1.inv result } end diff --git a/creusot/tests/should_succeed/vector/04_binary_search.mlcfg b/creusot/tests/should_succeed/vector/04_binary_search.mlcfg index 0e1bc494ba..8c49d49580 100644 --- a/creusot/tests/should_succeed/vector/04_binary_search.mlcfg +++ b/creusot/tests/should_succeed/vector/04_binary_search.mlcfg @@ -403,10 +403,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/vector/05_binary_search_generic.mlcfg b/creusot/tests/should_succeed/vector/05_binary_search_generic.mlcfg index 41a55c245f..f91b918f38 100644 --- a/creusot/tests/should_succeed/vector/05_binary_search_generic.mlcfg +++ b/creusot/tests/should_succeed/vector/05_binary_search_generic.mlcfg @@ -457,10 +457,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg b/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg index 83191940bc..c6ae7decfe 100644 --- a/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg +++ b/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg @@ -449,8 +449,8 @@ module Alloc_Vec_FromElem_Interface type t = t val from_elem (elem : t) (n : usize) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) requires {Inv0.inv elem} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 155 22 155 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 156 12 156 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 157 22 157 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 158 12 158 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem } ensures { Inv1.inv result } end @@ -1376,7 +1376,7 @@ module CreusotContracts_Std1_Vec_Impl9_FromIterPost predicate Inv1.inv = Inv1.inv, axiom . predicate from_iter_post (prod : Seq.seq t) (res : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 256 20 256 32] prod = ShallowModel0.shallow_model res + [#"../../../../../creusot-contracts/src/std/vec.rs" 258 20 258 32] prod = ShallowModel0.shallow_model res val from_iter_post (prod : Seq.seq t) (res : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) : bool ensures { result = from_iter_post prod res } @@ -2218,10 +2218,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end @@ -2579,7 +2579,7 @@ module CreusotContracts_Std1_Vec_Impl8_Produces predicate produces (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (visited : Seq.seq t) (rhs : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 235 12 235 41] ShallowModel0.shallow_model self = Seq.(++) visited (ShallowModel0.shallow_model rhs) + [#"../../../../../creusot-contracts/src/std/vec.rs" 237 12 237 41] ShallowModel0.shallow_model self = Seq.(++) visited (ShallowModel0.shallow_model rhs) val produces (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (visited : Seq.seq t) (rhs : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : bool ensures { result = produces self visited rhs } @@ -2648,7 +2648,7 @@ module CreusotContracts_Std1_Vec_Impl11_Resolve type t = t, type a = a predicate resolve (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 220 8 220 85] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model self) -> Resolve0.resolve (Seq.get (ShallowModel0.shallow_model self) i) + [#"../../../../../creusot-contracts/src/std/vec.rs" 222 8 222 85] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model self) -> Resolve0.resolve (Seq.get (ShallowModel0.shallow_model self) i) val resolve (self : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : bool ensures { result = resolve self } @@ -2700,7 +2700,7 @@ module CreusotContracts_Std1_Vec_Impl4_IntoIterPre type a use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type predicate into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 166 20 166 24] true + [#"../../../../../creusot-contracts/src/std/vec.rs" 168 20 168 24] true val into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) : bool ensures { result = into_iter_pre self } @@ -2746,7 +2746,7 @@ module CreusotContracts_Std1_Vec_Impl4_IntoIterPost axiom . predicate into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 172 20 172 33] ShallowModel0.shallow_model self = ShallowModel1.shallow_model res + [#"../../../../../creusot-contracts/src/std/vec.rs" 174 20 174 33] ShallowModel0.shallow_model self = ShallowModel1.shallow_model res val into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : bool ensures { result = into_iter_post self res } @@ -2834,7 +2834,7 @@ module CreusotContracts_Std1_Vec_Impl8_Completed clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a predicate completed (self : borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a)) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 228 20 228 57] Resolve0.resolve self /\ ShallowModel0.shallow_model self = Seq.empty + [#"../../../../../creusot-contracts/src/std/vec.rs" 230 20 230 57] Resolve0.resolve self /\ ShallowModel0.shallow_model self = Seq.empty val completed (self : borrowed (Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a)) : bool ensures { result = completed self } @@ -2891,11 +2891,11 @@ module CreusotContracts_Std1_Vec_Impl8_ProducesRefl_Interface type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a function produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () val produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 242 21 242 22] Inv0.inv a} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 241 14 241 39] Produces0.produces a (Seq.empty ) a } + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a } ensures { result = produces_refl a } - axiom produces_refl_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 242 21 242 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 241 14 241 39] Produces0.produces a (Seq.empty ) a) + axiom produces_refl_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a) end module CreusotContracts_Std1_Vec_Impl8_ProducesRefl type t @@ -2908,13 +2908,13 @@ module CreusotContracts_Std1_Vec_Impl8_ProducesRefl clone CreusotContracts_Invariant_Inv_Stub as Inv0 with type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a function produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () = - [#"../../../../../creusot-contracts/src/std/vec.rs" 239 4 239 10] () + [#"../../../../../creusot-contracts/src/std/vec.rs" 241 4 241 10] () val produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 242 21 242 22] Inv0.inv a} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 241 14 241 39] Produces0.produces a (Seq.empty ) a } + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a } ensures { result = produces_refl a } - axiom produces_refl_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 242 21 242 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 241 14 241 39] Produces0.produces a (Seq.empty ) a) + axiom produces_refl_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 244 21 244 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 243 14 243 39] Produces0.produces a (Seq.empty ) a) end module CreusotContracts_Std1_Vec_Impl8_ProducesTrans_Stub type t @@ -2948,17 +2948,17 @@ module CreusotContracts_Std1_Vec_Impl8_ProducesTrans_Interface function produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () val produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 246 15 246 32] Produces0.produces a ab b} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 247 15 247 32] Produces0.produces b bc c} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 22 249 23] Inv0.inv a} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 31 249 33] Inv1.inv ab} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 43 249 44] Inv0.inv b} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 52 249 54] Inv1.inv bc} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 64 249 65] Inv0.inv c} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 248 14 248 42] Produces0.produces a (Seq.(++) ab bc) c } + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c } ensures { result = produces_trans a ab b bc c } - axiom produces_trans_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, ab : Seq.seq t, b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, bc : Seq.seq t, c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 246 15 246 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 247 15 247 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 22 249 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 31 249 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 43 249 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 52 249 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 64 249 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 248 14 248 42] Produces0.produces a (Seq.(++) ab bc) c) + axiom produces_trans_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, ab : Seq.seq t, b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, bc : Seq.seq t, c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c) end module CreusotContracts_Std1_Vec_Impl8_ProducesTrans type t @@ -2976,19 +2976,19 @@ module CreusotContracts_Std1_Vec_Impl8_ProducesTrans function produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () = - [#"../../../../../creusot-contracts/src/std/vec.rs" 244 4 244 10] () + [#"../../../../../creusot-contracts/src/std/vec.rs" 246 4 246 10] () val produces_trans (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (ab : Seq.seq t) (b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) (bc : Seq.seq t) (c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 246 15 246 32] Produces0.produces a ab b} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 247 15 247 32] Produces0.produces b bc c} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 22 249 23] Inv0.inv a} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 31 249 33] Inv1.inv ab} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 43 249 44] Inv0.inv b} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 52 249 54] Inv1.inv bc} - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 64 249 65] Inv0.inv c} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 248 14 248 42] Produces0.produces a (Seq.(++) ab bc) c } + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c } ensures { result = produces_trans a ab b bc c } - axiom produces_trans_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, ab : Seq.seq t, b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, bc : Seq.seq t, c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 246 15 246 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 247 15 247 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 22 249 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 31 249 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 43 249 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 52 249 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 64 249 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 248 14 248 42] Produces0.produces a (Seq.(++) ab bc) c) + axiom produces_trans_spec : forall a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, ab : Seq.seq t, b : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a, bc : Seq.seq t, c : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 248 15 248 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 249 15 249 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 22 251 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 31 251 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 43 251 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 52 251 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 64 251 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 250 14 250 42] Produces0.produces a (Seq.(++) ab bc) c) end module C06KnightsTour_Impl1_CountDegree_Interface use prelude.Borrow @@ -3402,13 +3402,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end @@ -3923,7 +3923,7 @@ module CreusotContracts_Std1_Vec_Impl5_IntoIterPre use prelude.Borrow use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type predicate into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 180 20 180 24] true + [#"../../../../../creusot-contracts/src/std/vec.rs" 182 20 182 24] true val into_iter_pre (self : Alloc_Vec_Vec_Type.t_vec t a) : bool ensures { result = into_iter_pre self } @@ -3965,7 +3965,7 @@ module CreusotContracts_Std1_Vec_Impl5_IntoIterPost type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t predicate into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Core_Slice_Iter_Iter_Type.t_iter t) = - [#"../../../../../creusot-contracts/src/std/vec.rs" 186 20 186 34] ShallowModel0.shallow_model self = ShallowModel2.shallow_model (ShallowModel1.shallow_model res) + [#"../../../../../creusot-contracts/src/std/vec.rs" 188 20 188 34] ShallowModel0.shallow_model self = ShallowModel2.shallow_model (ShallowModel1.shallow_model res) val into_iter_post (self : Alloc_Vec_Vec_Type.t_vec t a) (res : Core_Slice_Iter_Iter_Type.t_iter t) : bool ensures { result = into_iter_post self res } diff --git a/creusot/tests/should_succeed/vector/07_read_write.mlcfg b/creusot/tests/should_succeed/vector/07_read_write.mlcfg index bba5f6d404..c89786099b 100644 --- a/creusot/tests/should_succeed/vector/07_read_write.mlcfg +++ b/creusot/tests/should_succeed/vector/07_read_write.mlcfg @@ -377,13 +377,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) } ensures { Inv2.inv result } end @@ -449,10 +449,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end diff --git a/creusot/tests/should_succeed/vector/08_haystack.mlcfg b/creusot/tests/should_succeed/vector/08_haystack.mlcfg index a005e33a9b..58f8f2b5af 100644 --- a/creusot/tests/should_succeed/vector/08_haystack.mlcfg +++ b/creusot/tests/should_succeed/vector/08_haystack.mlcfg @@ -1043,10 +1043,10 @@ module Alloc_Vec_Impl12_Index_Interface type t = Alloc_Vec_Vec_Type.t_vec t a, type ShallowModelTy0.shallowModelTy = Seq.seq t val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output - requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)} requires {Inv0.inv self} requires {Inv1.inv index} - ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result } ensures { Inv2.inv result } end