From a42326e24ab12f9d363118aaf309897759d6514f 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/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 5 files changed, 1209 insertions(+), 3 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 428ee860e1..aaabf34a33 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/tests/should_succeed/bug/874.mlcfg b/creusot/tests/should_succeed/bug/874.mlcfg new file mode 100644 index 0000000000..97914fff87 --- /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" 27 4 27 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_Impl11_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_Impl11_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_Impl11_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" 304 18 304 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" 64 20 64 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_Impl9_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_Impl9_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_Impl9_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" 232 20 232 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_Impl9_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_Impl9_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_Impl9_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" 239 12 239 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" 20 21 20 25] Inv0.inv self} + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 18 14 18 41] Seq.length result <= UIntSize.to_int Max0.mAX' } + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 19 14 19 41] result = Slice.id self } + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 20 4 20 50] Inv1.inv result } + ensures { result = shallow_model self } + + axiom shallow_model_spec : forall self : slice t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 20 21 20 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 20 4 20 50] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/slice.rs" 19 14 19 41] shallow_model self = Slice.id self) && ([#"../../../../../creusot-contracts/src/std/slice.rs" 18 14 18 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" 20 21 20 25] Inv0.inv self} + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 18 14 18 41] Seq.length result <= UIntSize.to_int Max0.mAX' } + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 19 14 19 41] result = Slice.id self } + ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 20 4 20 50] Inv1.inv result } + ensures { result = shallow_model self } + + axiom shallow_model_spec : forall self : slice t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 20 21 20 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 20 4 20 50] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/slice.rs" 19 14 19 41] shallow_model self = Slice.id self) && ([#"../../../../../creusot-contracts/src/std/slice.rs" 18 14 18 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX') +end +module CreusotContracts_Std1_Vec_Impl9_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_Impl9_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_Impl9_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_Impl9_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" 246 21 246 22] Inv0.inv a} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 245 14 245 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" 246 21 246 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 245 14 245 39] Produces0.produces a (Seq.empty ) a) +end +module CreusotContracts_Std1_Vec_Impl9_ProducesRefl + type t + type a + use seq.Seq + use Alloc_Vec_IntoIter_IntoIter_Type as Alloc_Vec_IntoIter_IntoIter_Type + clone CreusotContracts_Std1_Vec_Impl9_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" 243 4 243 10] () + val produces_refl (a : Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter t a) : () + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 246 21 246 22] Inv0.inv a} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 245 14 245 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" 246 21 246 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 245 14 245 39] Produces0.produces a (Seq.empty ) a) +end +module CreusotContracts_Std1_Vec_Impl9_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_Impl9_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_Impl9_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_Impl9_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" 250 15 250 32] Produces0.produces a ab b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 15 251 32] Produces0.produces b bc c} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 253 22 253 23] Inv0.inv a} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 253 31 253 33] Inv1.inv ab} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 253 43 253 44] Inv0.inv b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 253 52 253 54] Inv1.inv bc} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 253 64 253 65] Inv0.inv c} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 252 14 252 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" 250 15 250 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 15 251 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 253 22 253 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 253 31 253 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 253 43 253 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 253 52 253 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 253 64 253 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 252 14 252 42] Produces0.produces a (Seq.(++) ab bc) c) +end +module CreusotContracts_Std1_Vec_Impl9_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_Impl9_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" 248 4 248 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" 250 15 250 32] Produces0.produces a ab b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 251 15 251 32] Produces0.produces b bc c} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 253 22 253 23] Inv0.inv a} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 253 31 253 33] Inv1.inv ab} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 253 43 253 44] Inv0.inv b} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 253 52 253 54] Inv1.inv bc} + requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 253 64 253 65] Inv0.inv c} + ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 252 14 252 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" 250 15 250 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 251 15 251 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 253 22 253 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 253 31 253 33] Inv1.inv ab) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 253 43 253 44] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 253 52 253 54] Inv1.inv bc) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 253 64 253 65] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 252 14 252 42] Produces0.produces a (Seq.(++) ab bc) c) +end +module C874_CanExtend_Interface + val can_extend [#"../874.rs" 5 0 5 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_Impl9_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_Impl9_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_Impl9_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_Impl9_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_Impl11_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" 5 0 5 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" 6 14 6 25] IntoVec0.into_vec (Slice.create 3 [|[#"../874.rs" 6 19 6 20] (1 : int32); [#"../874.rs" 6 21 6 22] (2 : int32); [#"../874.rs" 6 23 6 24] (3 : int32)|])); + goto BB3 + } + BB3 { + goto BB4 + } + BB4 { + goto BB5 + } + BB5 { + w <- ([#"../874.rs" 7 10 7 21] IntoVec0.into_vec (Slice.create 3 [|[#"../874.rs" 7 15 7 16] (4 : int32); [#"../874.rs" 7 17 7 18] (5 : int32); [#"../874.rs" 7 19 7 20] (6 : int32)|])); + goto BB6 + } + BB6 { + _10 <- Borrow.borrow_mut v; + v <- ^ _10; + _9 <- ([#"../874.rs" 8 2 8 13] 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" 10 10 10 27] IntoVec0.into_vec (Slice.create 6 [|[#"../874.rs" 10 15 10 16] (1 : int32); [#"../874.rs" 10 17 10 18] (2 : int32); [#"../874.rs" 10 19 10 20] (3 : int32); [#"../874.rs" 10 21 10 22] (4 : int32); [#"../874.rs" 10 23 10 24] (5 : int32); [#"../874.rs" 10 25 10 26] (6 : int32)|])); + goto BB10 + } + BB10 { + assume { Resolve0.resolve z }; + assert { [@expl:assertion] [#"../874.rs" 11 2 11 30] 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