diff --git a/creusot/tests/should_fail/cycle.stderr b/creusot/tests/should_fail/cycle.stderr index 8be9abb0bb..bb5442039e 100644 --- a/creusot/tests/should_fail/cycle.stderr +++ b/creusot/tests/should_fail/cycle.stderr @@ -6,7 +6,7 @@ warning: unused import: `creusot_contracts::*` | = note: `#[warn(unused_imports)]` on by default -error[creusot]: encountered a cycle during translation: [{DefId(0:5 ~ cycle[c4ca]::f)}, {DefId(0:6 ~ cycle[c4ca]::g)}, {DefId(0:5 ~ cycle[c4ca]::f)}] +error[creusot]: encountered a cycle during translation: [{Item(DefId(0:5 ~ cycle[c4ca]::f))}, {Item(DefId(0:6 ~ cycle[c4ca]::g))}, {Item(DefId(0:5 ~ cycle[c4ca]::f))}] --> cycle.rs:4:1 | 4 | pub fn f() { diff --git a/creusot/tests/should_succeed/all_zero.mlcfg b/creusot/tests/should_succeed/all_zero.mlcfg index f4152e3efe..f67c51f3da 100644 --- a/creusot/tests/should_succeed/all_zero.mlcfg +++ b/creusot/tests/should_succeed/all_zero.mlcfg @@ -104,35 +104,6 @@ module CreusotContracts_Resolve_Impl1_Resolve val resolve (self : borrowed t) : bool ensures { result = resolve self } -end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - end module AllZero_AllZero_Interface use prelude.Int @@ -152,9 +123,7 @@ module AllZero_AllZero use prelude.Borrow use prelude.Int use prelude.UInt32 - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use AllZero_List_Type as AllZero_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with type t = AllZero_List_Type.t_list clone CreusotContracts_Resolve_Impl1_Resolve as Resolve1 with diff --git a/creusot/tests/should_succeed/all_zero/why3session.xml b/creusot/tests/should_succeed/all_zero/why3session.xml index f1e6ba2510..ec35048501 100644 --- a/creusot/tests/should_succeed/all_zero/why3session.xml +++ b/creusot/tests/should_succeed/all_zero/why3session.xml @@ -7,7 +7,7 @@ - + diff --git a/creusot/tests/should_succeed/all_zero/why3shapes.gz b/creusot/tests/should_succeed/all_zero/why3shapes.gz index e0c43d4138..8f1223c25d 100644 Binary files a/creusot/tests/should_succeed/all_zero/why3shapes.gz and b/creusot/tests/should_succeed/all_zero/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/bdd.mlcfg b/creusot/tests/should_succeed/bdd.mlcfg index 71471aa68e..d650aab7cf 100644 --- a/creusot/tests/should_succeed/bdd.mlcfg +++ b/creusot/tests/should_succeed/bdd.mlcfg @@ -155,9 +155,9 @@ module Bdd_Hashmap_Impl1_Add_Interface type v use prelude.Borrow use map.Map + use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k - use Core_Option_Option_Type as Core_Option_Option_Type use map.Map use Bdd_Hashmap_MyHashMap_Type as Bdd_Hashmap_MyHashMap_Type clone CreusotContracts_Model_Impl3_ShallowModel_Stub as ShallowModel1 with @@ -3314,7 +3314,7 @@ module Bdd_Impl10_Not function Interp0.interp = Interp0.interp, val Max0.mAX' = Max0.mAX', function Leastvar0.leastvar = Leastvar0.leastvar - clone Bdd_Impl10_Node_Interface as Node1 with + clone Bdd_Impl10_Node_Interface as Node0 with predicate Invariant0.invariant' = Invariant0.invariant', predicate IsValidBdd0.is_valid_bdd = IsValidBdd0.is_valid_bdd, function Leastvar0.leastvar = Leastvar0.leastvar, @@ -3445,7 +3445,7 @@ module Bdd_Impl10_Not BB14 { _32 <- borrow_mut ( * self); self <- { self with current = ( ^ _32) }; - r1 <- ([#"../bdd.rs" 522 16 522 44] Node1.node _32 v childt1 childf1); + r1 <- ([#"../bdd.rs" 522 16 522 44] Node0.node _32 v childt1 childf1); _32 <- any borrowed (Bdd_Context_Type.t_context); goto BB15 } @@ -3640,7 +3640,7 @@ module Bdd_Impl10_And function Interp0.interp = Interp0.interp, val Max0.mAX' = Max0.mAX', function Leastvar0.leastvar = Leastvar0.leastvar - clone Bdd_Impl10_Node_Interface as Node1 with + clone Bdd_Impl10_Node_Interface as Node0 with predicate Invariant0.invariant' = Invariant0.invariant', predicate IsValidBdd0.is_valid_bdd = IsValidBdd0.is_valid_bdd, function Leastvar0.leastvar = Leastvar0.leastvar, @@ -3887,7 +3887,7 @@ module Bdd_Impl10_And BB31 { _76 <- borrow_mut ( * self); self <- { self with current = ( ^ _76) }; - r1 <- ([#"../bdd.rs" 568 16 568 44] Node1.node _76 v childt childf); + r1 <- ([#"../bdd.rs" 568 16 568 44] Node0.node _76 v childt childf); _76 <- any borrowed (Bdd_Context_Type.t_context); goto BB32 } diff --git a/creusot/tests/should_succeed/binary_search.mlcfg b/creusot/tests/should_succeed/binary_search.mlcfg index 759e3e800d..19c54e3cbe 100644 --- a/creusot/tests/should_succeed/binary_search.mlcfg +++ b/creusot/tests/should_succeed/binary_search.mlcfg @@ -118,35 +118,6 @@ module CreusotContracts_Resolve_Resolve_Resolve val resolve (self : self) : bool ensures { result = resolve self } -end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - end module BinarySearch_Impl0_Index_Interface type t @@ -170,10 +141,8 @@ module BinarySearch_Impl0_Index use prelude.UIntSize use prelude.Int use prelude.Borrow - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use BinarySearch_List_Type as BinarySearch_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use Core_Option_Option_Type as Core_Option_Option_Type + use BinarySearch_List_Type as BinarySearch_List_Type clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve2 with type self = BinarySearch_List_Type.t_list t clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with @@ -271,9 +240,7 @@ module BinarySearch_Impl0_Len use prelude.Int use prelude.UIntSize use prelude.Borrow - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use BinarySearch_List_Type as BinarySearch_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with type self = BinarySearch_List_Type.t_list t clone BinarySearch_Impl0_LenLogic as LenLogic0 with diff --git a/creusot/tests/should_succeed/binary_search/why3session.xml b/creusot/tests/should_succeed/binary_search/why3session.xml index 59b664667b..286b7b8d98 100644 --- a/creusot/tests/should_succeed/binary_search/why3session.xml +++ b/creusot/tests/should_succeed/binary_search/why3session.xml @@ -12,12 +12,12 @@ - + - + diff --git a/creusot/tests/should_succeed/binary_search/why3shapes.gz b/creusot/tests/should_succeed/binary_search/why3shapes.gz index 1f472fda46..0b6b89003a 100644 Binary files a/creusot/tests/should_succeed/binary_search/why3shapes.gz and b/creusot/tests/should_succeed/binary_search/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/bug/387.mlcfg b/creusot/tests/should_succeed/bug/387.mlcfg index 5dd1d377dd..73fee43aa0 100644 --- a/creusot/tests/should_succeed/bug/387.mlcfg +++ b/creusot/tests/should_succeed/bug/387.mlcfg @@ -10,40 +10,9 @@ module Core_Option_Option_Type | C_Some a -> a end end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - -end module C387_Node_Type use prelude.Int use prelude.UInt32 - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use Core_Option_Option_Type as Core_Option_Option_Type type t_node = | C_Node (t_tree) uint32 (t_tree) @@ -328,9 +297,6 @@ module C387_Impl0_Height clone CreusotContracts_Logic_Ord_Impl2_LeLog as LeLog0 clone CreusotContracts_Logic_Ord_Impl2_GeLog as GeLog0 clone CreusotContracts_Std1_Num_Impl10_DeepModel as DeepModel0 - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use C387_Node_Type as C387_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone Core_Cmp_Ord_Max_Interface as Max0 with type self = uint64, function DeepModel0.deep_model = DeepModel0.deep_model, @@ -338,6 +304,7 @@ module C387_Impl0_Height predicate LeLog0.le_log = LeLog0.le_log, predicate LtLog0.lt_log = LtLog0.lt_log, type DeepModelTy0.deepModelTy = int + use C387_Node_Type as C387_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use C387_Tree_Type as C387_Tree_Type let rec cfg height [#"../387.rs" 16 4 16 31] [@cfg:stackify] [@cfg:subregion_analysis] (self : C387_Tree_Type.t_tree) : uint64 diff --git a/creusot/tests/should_succeed/cell/02.mlcfg b/creusot/tests/should_succeed/cell/02.mlcfg index e733e32f89..a517ea1e9c 100644 --- a/creusot/tests/should_succeed/cell/02.mlcfg +++ b/creusot/tests/should_succeed/cell/02.mlcfg @@ -227,14 +227,14 @@ module C02_Impl1_Inv use prelude.Borrow use prelude.Int use prelude.UIntSize - clone C02_Fib_Stub as Fib1 with + clone C02_Fib_Stub as Fib0 with axiom . use Core_Option_Option_Type as Core_Option_Option_Type use C02_Fib_Type as C02_Fib_Type predicate inv [#"../02.rs" 70 4 70 43] (self : C02_Fib_Type.t_fib) (v : Core_Option_Option_Type.t_option usize) = [#"../02.rs" 72 12 75 13] match (v) with | Core_Option_Option_Type.C_None -> true - | Core_Option_Option_Type.C_Some i -> UIntSize.to_int i = Fib1.fib (UIntSize.to_int (C02_Fib_Type.fib_ix self)) + | Core_Option_Option_Type.C_Some i -> UIntSize.to_int i = Fib0.fib (UIntSize.to_int (C02_Fib_Type.fib_ix self)) end val inv [#"../02.rs" 70 4 70 43] (self : C02_Fib_Type.t_fib) (v : Core_Option_Option_Type.t_option usize) : bool ensures { result = inv self v } @@ -665,7 +665,7 @@ module C02_FibMemo clone C02_Fib as Fib0 with axiom . clone C02_Impl1_Inv as Inv0 with - function Fib1.fib = Fib0.fib + function Fib0.fib = Fib0.fib clone CreusotContracts_Std1_Slice_Impl5_HasValue as HasValue0 with type t = C02_Cell_Type.t_cell (Core_Option_Option_Type.t_option usize) (C02_Fib_Type.t_fib) clone CreusotContracts_Std1_Slice_Impl5_InBounds as InBounds0 with diff --git a/creusot/tests/should_succeed/hashmap.mlcfg b/creusot/tests/should_succeed/hashmap.mlcfg index e04b9b7740..44a0dc8cfd 100644 --- a/creusot/tests/should_succeed/hashmap.mlcfg +++ b/creusot/tests/should_succeed/hashmap.mlcfg @@ -1215,21 +1215,15 @@ module CreusotContracts_Std1_Slice_Impl5_ResolveElswhere val resolve_elswhere [@inline:trivial] (self : usize) (old' : Seq.seq t) (fin : Seq.seq t) : bool ensures { result = resolve_elswhere self old' fin } -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 Hashmap_Impl5_Add_Interface type k type v use prelude.Borrow use map.Map + use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k - use Core_Option_Option_Type as Core_Option_Option_Type use map.Map use Hashmap_MyHashMap_Type as Hashmap_MyHashMap_Type clone CreusotContracts_Model_Impl3_ShallowModel_Stub as ShallowModel1 with @@ -1265,9 +1259,9 @@ module Hashmap_Impl5_Add use prelude.Borrow use map.Map use seq.Seq + use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k - use Core_Option_Option_Type as Core_Option_Option_Type use map.Map use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use Hashmap_List_Type as Hashmap_List_Type @@ -1300,7 +1294,6 @@ module Hashmap_Impl5_Add type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, function BucketIx0.bucket_ix = BucketIx0.bucket_ix, function IndexLogic0.index_logic = IndexLogic0.index_logic - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use prelude.Ghost clone CreusotContracts_Std1_Slice_Impl5_ResolveElswhere as ResolveElswhere0 with type t = Hashmap_List_Type.t_list (k, v) @@ -1696,7 +1689,6 @@ module Hashmap_Impl5_Get type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, function Get0.get = Get0.get, function BucketIx0.bucket_ix = BucketIx0.bucket_ix - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Std1_Slice_Impl5_HasValue as HasValue0 with type t = Hashmap_List_Type.t_list (k, v) clone CreusotContracts_Std1_Slice_Impl5_InBounds as InBounds0 with @@ -1902,9 +1894,9 @@ module Hashmap_Impl5_Resize_Interface use seq.Seq use prelude.Int use map.Map + use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k - use Core_Option_Option_Type as Core_Option_Option_Type use map.Map use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use Hashmap_List_Type as Hashmap_List_Type @@ -1942,20 +1934,19 @@ module Hashmap_Impl5_Resize use prelude.Borrow use map.Map use seq.Seq - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use Hashmap_List_Type as Hashmap_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k clone CreusotContracts_Model_DeepModel_DeepModel_Interface as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use Hashmap_List_Type as Hashmap_List_Type clone CreusotContracts_Std1_Slice_Impl5_ResolveElswhere as ResolveElswhere0 with type t = Hashmap_List_Type.t_list (k, v) clone CreusotContracts_Std1_Slice_Impl5_HasValue as HasValue0 with type t = Hashmap_List_Type.t_list (k, v) clone CreusotContracts_Std1_Slice_Impl5_InBounds as InBounds0 with type t = Hashmap_List_Type.t_list (k, v) + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type clone Core_Num_Impl11_Max as Max0 clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Interface as ShallowModel2 with diff --git a/creusot/tests/should_succeed/hashmap/why3session.xml b/creusot/tests/should_succeed/hashmap/why3session.xml index 2eaef11154..07765b9c55 100644 --- a/creusot/tests/should_succeed/hashmap/why3session.xml +++ b/creusot/tests/should_succeed/hashmap/why3session.xml @@ -2,8 +2,8 @@ + - @@ -30,16 +30,16 @@ - + - + - + - + @@ -66,12 +66,12 @@ - + - + @@ -81,13 +81,13 @@ - + - + - + @@ -96,7 +96,7 @@ - + @@ -115,24 +115,24 @@ - + - + - + - + @@ -143,7 +143,7 @@ - + @@ -156,7 +156,7 @@ - + @@ -177,7 +177,7 @@ - + @@ -189,40 +189,40 @@ - + - + - + - + - + - + - + - + @@ -234,13 +234,13 @@ - + - + @@ -252,7 +252,7 @@ - + diff --git a/creusot/tests/should_succeed/hashmap/why3shapes.gz b/creusot/tests/should_succeed/hashmap/why3shapes.gz index a8c2067a1e..d8633d7660 100644 Binary files a/creusot/tests/should_succeed/hashmap/why3shapes.gz and b/creusot/tests/should_succeed/hashmap/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/ite_normalize.mlcfg b/creusot/tests/should_succeed/ite_normalize.mlcfg index 7ccef4e420..200d3c1569 100644 --- a/creusot/tests/should_succeed/ite_normalize.mlcfg +++ b/creusot/tests/should_succeed/ite_normalize.mlcfg @@ -233,9 +233,9 @@ module IteNormalize_Impl0_Insert_Interface type v use prelude.Borrow use map.Map + use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k - use Core_Option_Option_Type as Core_Option_Option_Type use map.Map use IteNormalize_BTreeMap_Type as IteNormalize_BTreeMap_Type clone CreusotContracts_Model_Impl3_ShallowModel_Stub as ShallowModel1 with diff --git a/creusot/tests/should_succeed/iterators/01_range.mlcfg b/creusot/tests/should_succeed/iterators/01_range.mlcfg index 1248aa0c7e..f2124e9d9d 100644 --- a/creusot/tests/should_succeed/iterators/01_range.mlcfg +++ b/creusot/tests/should_succeed/iterators/01_range.mlcfg @@ -454,12 +454,12 @@ end module C01Range_Impl0 end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -467,13 +467,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -497,7 +497,7 @@ module C01Range_Impl1 predicate Resolve0.resolve = Resolve0.resolve clone CreusotContracts_Invariant_Invariant_Invariant as Invariant0 with type self = C01Range_Range_Type.t_range - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C01Range_Range_Type.t_range, predicate Invariant0.invariant' = Invariant0.invariant' clone C01Range_Impl1_Produces as Produces0 diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg b/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg index 8ae2485ad3..e8db412080 100644 --- a/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg +++ b/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg @@ -568,12 +568,12 @@ module CreusotContracts_Invariant_Invariant_Invariant ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -581,13 +581,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -662,7 +662,7 @@ module C02IterMut_Impl1_Next_Interface clone C02IterMut_Impl1_Completed_Stub as Completed0 with type t = t use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C02IterMut_IterMut_Type.t_itermut t val next [#"../02_iter_mut.rs" 57 4 57 44] (self : borrowed (C02IterMut_IterMut_Type.t_itermut t)) : Core_Option_Option_Type.t_option (borrowed t) requires {[#"../02_iter_mut.rs" 57 17 57 21] Invariant0.invariant' self} @@ -721,7 +721,7 @@ module C02IterMut_Impl1_Next type t = t, predicate Resolve0.resolve = Resolve0.resolve, function ShallowModel0.shallow_model = ShallowModel1.shallow_model - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C02IterMut_IterMut_Type.t_itermut t, predicate Invariant0.invariant' = Invariant1.invariant' use Core_Option_Option_Type as Core_Option_Option_Type @@ -1286,7 +1286,7 @@ module C02IterMut_AllZero type t = usize, function ShallowModel0.shallow_model = ShallowModel3.shallow_model, val Max0.mAX' = Max0.mAX' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C02IterMut_IterMut_Type.t_itermut usize, predicate Invariant0.invariant' = Invariant0.invariant' clone CreusotContracts_Logic_Ops_Impl0_IndexLogic as IndexLogic2 with @@ -1491,7 +1491,7 @@ module C02IterMut_Impl1 type t = t, function ShallowModel0.shallow_model = ShallowModel0.shallow_model, val Max0.mAX' = Max0.mAX' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C02IterMut_IterMut_Type.t_itermut t, predicate Invariant0.invariant' = Invariant0.invariant' clone C02IterMut_Impl1_Produces as Produces0 with diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg b/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg index ebfebb59c0..781f2b9829 100644 --- a/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg +++ b/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg @@ -1554,12 +1554,12 @@ module Core_Slice_Impl0_IterMut_Interface ensures { Invariant0.invariant' result } end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -1567,13 +1567,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -1629,7 +1629,7 @@ module Core_Slice_Iter_Impl189_Next_Interface type t = t clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with type self = Core_Slice_Iter_IterMut_Type.t_itermut t - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = Core_Slice_Iter_IterMut_Type.t_itermut t val next (self : borrowed (Core_Slice_Iter_IterMut_Type.t_itermut t)) : Core_Option_Option_Type.t_option (borrowed t) requires {Invariant0.invariant' self} @@ -1801,7 +1801,7 @@ module C03StdIterators_AllZero function ShallowModel0.shallow_model = ShallowModel4.shallow_model, function ShallowModel1.shallow_model = ShallowModel3.shallow_model, val Max0.mAX' = Max0.mAX' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = Core_Slice_Iter_IterMut_Type.t_itermut usize, predicate Invariant0.invariant' = Invariant0.invariant' use seq.Seq @@ -2315,7 +2315,7 @@ module Core_Iter_Adapters_Skip_Impl1_Next_Interface type self = Core_Iter_Adapters_Skip_Skip_Type.t_skip i clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with type self = Core_Iter_Adapters_Skip_Skip_Type.t_skip i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = Core_Iter_Adapters_Skip_Skip_Type.t_skip i val next (self : borrowed (Core_Iter_Adapters_Skip_Skip_Type.t_skip i)) : Core_Option_Option_Type.t_option Item1.item requires {Invariant0.invariant' self} @@ -2359,7 +2359,7 @@ module CreusotContracts_Std1_Iter_Skip_Impl2_Completed use Core_Iter_Adapters_Skip_Skip_Type as Core_Iter_Adapters_Skip_Skip_Type clone CreusotContracts_Std1_Iter_Skip_Impl0_Iter_Stub as Iter0 with type i = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = i clone CreusotContracts_Std1_Iter_Skip_Impl0_N_Stub as N0 with type i = i, @@ -2987,7 +2987,7 @@ module C03StdIterators_SkipTake function Iter0.iter = Iter0.iter clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve3 with type self = Item0.item - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant4 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant4 with type t = Core_Iter_Adapters_Take_Take_Type.t_take i, predicate Invariant0.invariant' = Invariant1.invariant' use Core_Iter_Adapters_Skip_Skip_Type as Core_Iter_Adapters_Skip_Skip_Type @@ -3039,7 +3039,7 @@ module C03StdIterators_SkipTake predicate Resolve0.resolve = Resolve3.resolve, predicate Completed0.completed = Completed1.completed, val Max0.mAX' = Max0.mAX' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant3 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant3 with type t = Core_Iter_Adapters_Skip_Skip_Type.t_skip (Core_Iter_Adapters_Take_Take_Type.t_take i), predicate Invariant0.invariant' = Invariant2.invariant' use Core_Option_Option_Type as Core_Option_Option_Type @@ -3554,7 +3554,7 @@ module CreusotContracts_Std1_Iter_MapInv_Impl3_Reinitialize type b = b, type f = f, type Item0.item = Item0.item - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = CreusotContracts_Std1_Iter_MapInv_MapInv_Type.t_mapinv i Item0.item f predicate reinitialize (_1 : ()) = [#"../../../../../creusot-contracts/src/std/iter/map_inv.rs" 122 8 128 9] forall reset : borrowed (CreusotContracts_Std1_Iter_MapInv_MapInv_Type.t_mapinv i Item0.item f) . Invariant0.invariant' reset -> Completed0.completed reset -> Invariant1.invariant' (CreusotContracts_Std1_Iter_MapInv_MapInv_Type.mapinv_iter ( ^ reset)) -> NextPrecondition0.next_precondition ( ^ reset) /\ Preservation0.preservation (CreusotContracts_Std1_Iter_MapInv_MapInv_Type.mapinv_iter ( ^ reset)) (CreusotContracts_Std1_Iter_MapInv_MapInv_Type.mapinv_func ( ^ reset)) @@ -3773,7 +3773,7 @@ module Core_Iter_Traits_Iterator_Iterator_Collect_Interface type self = self clone CreusotContracts_Resolve_Resolve_Resolve_Stub as Resolve0 with type self = self - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant1 with type t = self clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = self @@ -4233,7 +4233,7 @@ module C03StdIterators_Counter type f = Closure00.c03stditerators_counter_closure0, predicate Resolve1.resolve = Closure00.resolve, predicate Resolve0.resolve = Resolve4.resolve - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = CreusotContracts_Std1_Iter_MapInv_MapInv_Type.t_mapinv (Core_Slice_Iter_Iter_Type.t_iter uint32) uint32 Closure00.c03stditerators_counter_closure0, predicate Invariant0.invariant' = Invariant1.invariant' clone CreusotContracts_Std1_Iter_MapInv_Impl3_Preservation as Preservation0 with @@ -4810,7 +4810,7 @@ module CreusotContracts_Std1_Iter_Enumerate_Impl1_Invariant use prelude.Borrow clone CreusotContracts_Std1_Iter_Iterator_Completed_Stub as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant1 with type t = i clone Core_Usize_Max_Stub as Max0 use Core_Iter_Adapters_Enumerate_Enumerate_Type as Core_Iter_Adapters_Enumerate_Enumerate_Type @@ -4967,7 +4967,7 @@ module Core_Iter_Adapters_Enumerate_Impl1_Next_Interface type self = Core_Iter_Adapters_Enumerate_Enumerate_Type.t_enumerate i clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with type self = Core_Iter_Adapters_Enumerate_Enumerate_Type.t_enumerate i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = Core_Iter_Adapters_Enumerate_Enumerate_Type.t_enumerate i val next (self : borrowed (Core_Iter_Adapters_Enumerate_Enumerate_Type.t_enumerate i)) : Core_Option_Option_Type.t_option (usize, Item1.item) requires {Invariant0.invariant' self} @@ -5123,7 +5123,7 @@ module CreusotContracts_Std1_Iter_Enumerate_Impl2_Completed use Core_Iter_Adapters_Enumerate_Enumerate_Type as Core_Iter_Adapters_Enumerate_Enumerate_Type clone CreusotContracts_Std1_Iter_Enumerate_Impl0_Iter_Stub as Iter0 with type i = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = i predicate completed (self : borrowed (Core_Iter_Adapters_Enumerate_Enumerate_Type.t_enumerate i)) = [#"../../../../../creusot-contracts/src/std/iter/enumerate.rs" 57 8 57 115] exists inner : borrowed i . Invariant0.invariant' inner /\ * inner = Iter0.iter ( * self) /\ ^ inner = Iter0.iter ( ^ self) /\ Completed0.completed inner @@ -5173,7 +5173,7 @@ module C03StdIterators_EnumerateRange function DeepModel0.deep_model = DeepModel0.deep_model clone CreusotContracts_Invariant_Invariant_Invariant as Invariant1 with type self = Core_Ops_Range_Range_Type.t_range usize - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant3 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant3 with type t = Core_Ops_Range_Range_Type.t_range usize, predicate Invariant0.invariant' = Invariant1.invariant' clone CreusotContracts_Std1_Iter_Range_Impl0_Produces as Produces1 with @@ -5205,7 +5205,7 @@ module C03StdIterators_EnumerateRange predicate Completed0.completed = Completed1.completed clone CreusotContracts_Std1_Iter_Enumerate_Impl1_Invariant_Interface as Invariant0 with type i = Core_Ops_Range_Range_Type.t_range usize - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = Core_Iter_Adapters_Enumerate_Enumerate_Type.t_enumerate (Core_Ops_Range_Range_Type.t_range usize), predicate Invariant0.invariant' = Invariant0.invariant' clone CreusotContracts_Std1_Iter_Enumerate_Impl0_N_Interface as N0 with diff --git a/creusot/tests/should_succeed/iterators/04_skip.mlcfg b/creusot/tests/should_succeed/iterators/04_skip.mlcfg index 2a01182a54..473153fe9d 100644 --- a/creusot/tests/should_succeed/iterators/04_skip.mlcfg +++ b/creusot/tests/should_succeed/iterators/04_skip.mlcfg @@ -57,12 +57,12 @@ module C04Skip_Impl0_Invariant ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -70,13 +70,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -181,7 +181,7 @@ module C04Skip_Impl1_Completed clone C04Skip_Common_Iterator_Produces_Stub as Produces0 with type self = i, type Item0.item = Item0.item - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = i use C04Skip_Skip_Type as C04Skip_Skip_Type predicate completed [#"../04_skip.rs" 33 4 33 35] (self : borrowed (C04Skip_Skip_Type.t_skip i)) = @@ -653,7 +653,7 @@ module C04Skip_Common_Iterator_Next_Interface clone C04Skip_Common_Iterator_Completed_Stub as Completed0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = self val next [#"../common.rs" 27 4 27 45] (self : borrowed self) : Core_Option_Option_Type.t_option Item0.item requires {[#"../common.rs" 27 17 27 21] Invariant0.invariant' self} @@ -701,7 +701,7 @@ module C04Skip_Impl1_Next_Interface clone C04Skip_Impl1_Completed_Stub as Completed0 with type i = i use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C04Skip_Skip_Type.t_skip i val next [#"../04_skip.rs" 74 4 74 41] (self : borrowed (C04Skip_Skip_Type.t_skip i)) : Core_Option_Option_Type.t_option Item0.item requires {[#"../04_skip.rs" 74 17 74 21] Invariant0.invariant' self} @@ -727,7 +727,7 @@ module C04Skip_Impl1_Next axiom . clone C04Skip_Common_Iterator_Completed_Interface as Completed1 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant3.invariant' clone C04Skip_Common_Iterator_Item_Type as Item0 with @@ -780,7 +780,7 @@ module C04Skip_Impl1_Next predicate Completed0.completed = Completed1.completed, predicate Produces0.produces = Produces0.produces, predicate Invariant1.invariant' = Invariant3.invariant' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C04Skip_Skip_Type.t_skip i, predicate Invariant0.invariant' = Invariant1.invariant' clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve2 with @@ -920,7 +920,7 @@ module C04Skip_Impl1 type self = i clone CreusotContracts_Invariant_Invariant_Invariant_Interface as Invariant2 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant3 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant3 with type t = i, predicate Invariant0.invariant' = Invariant2.invariant' clone C04Skip_Common_Iterator_Item_Type as Item0 with @@ -944,7 +944,7 @@ module C04Skip_Impl1 clone C04Skip_Impl0_Invariant as Invariant0 with type i = i, predicate Invariant0.invariant' = Invariant2.invariant' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C04Skip_Skip_Type.t_skip i, predicate Invariant0.invariant' = Invariant0.invariant' clone C04Skip_Impl1_Produces as Produces0 with diff --git a/creusot/tests/should_succeed/iterators/05_map.mlcfg b/creusot/tests/should_succeed/iterators/05_map.mlcfg index 9f2840a5cf..ddee7f5f6e 100644 --- a/creusot/tests/should_succeed/iterators/05_map.mlcfg +++ b/creusot/tests/should_succeed/iterators/05_map.mlcfg @@ -1380,12 +1380,12 @@ module C05Map_Impl0_ProducesTrans_Impl = [@vc:do_not_keep_trace] [@vc:sp] [#"../05_map.rs" 30 4 30 10] () end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -1393,13 +1393,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -1669,7 +1669,7 @@ module C05Map_Common_Iterator_Next_Interface clone C05Map_Common_Iterator_Completed_Stub as Completed0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = self val next [#"../common.rs" 27 4 27 45] (self : borrowed self) : Core_Option_Option_Type.t_option Item0.item requires {[#"../common.rs" 27 17 27 21] Invariant0.invariant' self} @@ -2008,7 +2008,7 @@ module C05Map_Impl0_Next_Interface type b = b, type f = f use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant1 with type t = C05Map_Map_Type.t_map i f clone C05Map_Impl2_Invariant_Stub as Invariant0 with type i = i, @@ -2139,7 +2139,7 @@ module C05Map_Impl0_Next predicate Produces0.produces = Produces0.produces, predicate Precondition0.precondition = Precondition0.precondition, predicate PostconditionMut0.postcondition_mut = PostconditionMut0.postcondition_mut - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant3.invariant' clone C05Map_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with @@ -2173,7 +2173,7 @@ module C05Map_Impl0_Next predicate Invariant0.invariant' = Invariant3.invariant', predicate NextPrecondition0.next_precondition = NextPrecondition0.next_precondition, predicate Preservation0.preservation = Preservation0.preservation - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C05Map_Map_Type.t_map i f, predicate Invariant0.invariant' = Invariant0.invariant' use Core_Option_Option_Type as Core_Option_Option_Type @@ -2622,7 +2622,7 @@ module C05Map_Impl0 predicate Invariant0.invariant' = Invariant2.invariant', predicate NextPrecondition0.next_precondition = NextPrecondition0.next_precondition, predicate Preservation0.preservation = Preservation0.preservation - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C05Map_Map_Type.t_map i f, predicate Invariant0.invariant' = Invariant1.invariant' goal next_refn : [#"../05_map.rs" 60 4 60 44] forall self : borrowed (C05Map_Map_Type.t_map i f) . Invariant0.invariant' self -> Invariant0.invariant' self /\ Invariant1.invariant' ( * self) /\ (forall result : Core_Option_Option_Type.t_option b . Invariant1.invariant' ( ^ self) /\ Invariant1.invariant' ( ^ self) /\ match (result) with diff --git a/creusot/tests/should_succeed/iterators/05_take.mlcfg b/creusot/tests/should_succeed/iterators/05_take.mlcfg index 803330f565..37e85ed999 100644 --- a/creusot/tests/should_succeed/iterators/05_take.mlcfg +++ b/creusot/tests/should_succeed/iterators/05_take.mlcfg @@ -542,12 +542,12 @@ module C05Take_Impl0_ProducesTrans_Impl = [@vc:do_not_keep_trace] [@vc:sp] [#"../05_take.rs" 42 4 42 10] () end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -555,13 +555,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -586,7 +586,7 @@ module C05Take_Common_Iterator_Next_Interface clone C05Take_Common_Iterator_Completed_Stub as Completed0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = self val next [#"../common.rs" 27 4 27 45] (self : borrowed self) : Core_Option_Option_Type.t_option Item0.item requires {[#"../common.rs" 27 17 27 21] Invariant0.invariant' self} @@ -612,7 +612,7 @@ module C05Take_Impl0_Next_Interface clone C05Take_Impl0_Completed_Stub as Completed0 with type i = i use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C05Take_Take_Type.t_take i val next [#"../05_take.rs" 53 4 53 41] (self : borrowed (C05Take_Take_Type.t_take i)) : Core_Option_Option_Type.t_option Item0.item requires {[#"../05_take.rs" 53 17 53 21] Invariant0.invariant' self} @@ -642,7 +642,7 @@ module C05Take_Impl0_Next type Item0.item = Item0.item clone C05Take_Common_Iterator_Completed_Interface as Completed1 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant3.invariant' clone C05Take_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with @@ -671,7 +671,7 @@ module C05Take_Impl0_Next type i = i, predicate Resolve0.resolve = Resolve0.resolve, predicate Completed0.completed = Completed1.completed - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C05Take_Take_Type.t_take i, predicate Invariant0.invariant' = Invariant1.invariant' use Core_Option_Option_Type as Core_Option_Option_Type @@ -755,7 +755,7 @@ module C05Take_Impl0 clone C05Take_Impl1_Invariant as Invariant1 with type i = i, predicate Invariant0.invariant' = Invariant2.invariant' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C05Take_Take_Type.t_take i, predicate Invariant0.invariant' = Invariant1.invariant' goal next_refn : [#"../05_take.rs" 53 4 53 41] forall self : borrowed (C05Take_Take_Type.t_take i) . Invariant0.invariant' self -> Invariant0.invariant' self /\ (forall result : Core_Option_Option_Type.t_option Item0.item . Invariant1.invariant' ( ^ self) /\ match (result) with diff --git a/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg b/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg index f51fee7656..281e7dbece 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg +++ b/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg @@ -1480,12 +1480,12 @@ module C06MapPrecond_Impl0_ProducesTrans_Impl = [@vc:do_not_keep_trace] [@vc:sp] [#"../06_map_precond.rs" 32 4 32 10] () end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -1493,13 +1493,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -1787,7 +1787,7 @@ module C06MapPrecond_Common_Iterator_Next_Interface clone C06MapPrecond_Common_Iterator_Completed_Stub as Completed0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = self val next [#"../common.rs" 27 4 27 45] (self : borrowed self) : Core_Option_Option_Type.t_option Item0.item requires {[#"../common.rs" 27 17 27 21] Invariant0.invariant' self} @@ -2155,7 +2155,7 @@ module C06MapPrecond_Impl0_Next_Interface type f = f, type Item0.item = Item0.item use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant1 with type t = C06MapPrecond_Map_Type.t_map i Item0.item f clone C06MapPrecond_Impl2_Invariant_Stub as Invariant0 with type i = i, @@ -2291,7 +2291,7 @@ module C06MapPrecond_Impl0_Next predicate Produces0.produces = Produces0.produces, predicate Precondition0.precondition = Precondition0.precondition, predicate PostconditionMut0.postcondition_mut = PostconditionMut0.postcondition_mut - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant3.invariant' clone C06MapPrecond_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with @@ -2326,7 +2326,7 @@ module C06MapPrecond_Impl0_Next predicate Invariant0.invariant' = Invariant3.invariant', predicate NextPrecondition0.next_precondition = NextPrecondition0.next_precondition, predicate Preservation0.preservation = Preservation0.preservation - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C06MapPrecond_Map_Type.t_map i Item0.item f, predicate Invariant0.invariant' = Invariant0.invariant' clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve3 with @@ -2859,10 +2859,10 @@ module C06MapPrecond_Identity type i = i, type b = Item0.item, type f = Closure00.c06mapprecond_identity_closure0 i, + type Item0.item = Item0.item, predicate Unnest0.unnest = Closure00.unnest, predicate Precondition0.precondition = Closure00.precondition, predicate PostconditionMut0.postcondition_mut = Closure00.postcondition_mut, - type Item0.item = Item0.item, predicate Produces0.produces = Produces0.produces clone C06MapPrecond_Common_Iterator_Completed_Interface as Completed1 with type self = i @@ -2872,28 +2872,28 @@ module C06MapPrecond_Identity type i = i, type b = Item0.item, type f = Closure00.c06mapprecond_identity_closure0 i, + type Item0.item = Item0.item, predicate Unnest0.unnest = Closure00.unnest, predicate Precondition0.precondition = Closure00.precondition, predicate PostconditionMut0.postcondition_mut = Closure00.postcondition_mut, - type Item0.item = Item0.item, predicate Invariant0.invariant' = Invariant0.invariant', predicate Produces0.produces = Produces0.produces clone C06MapPrecond_Impl1_NextPrecondition as NextPrecondition0 with type i = i, type b = Item0.item, type f = Closure00.c06mapprecond_identity_closure0 i, - predicate Precondition0.precondition = Closure00.precondition, type Item0.item = Item0.item, + predicate Precondition0.precondition = Closure00.precondition, predicate Invariant0.invariant' = Invariant0.invariant', predicate Produces0.produces = Produces0.produces clone C06MapPrecond_Impl1_PreservationInv as PreservationInv0 with type i = i, type b = Item0.item, type f = Closure00.c06mapprecond_identity_closure0 i, + type Item0.item = Item0.item, predicate Unnest0.unnest = Closure00.unnest, predicate Precondition0.precondition = Closure00.precondition, predicate PostconditionMut0.postcondition_mut = Closure00.postcondition_mut, - type Item0.item = Item0.item, predicate Preservation0.preservation = Preservation0.preservation, predicate Invariant0.invariant' = Invariant0.invariant', predicate Produces0.produces = Produces0.produces, @@ -2961,8 +2961,8 @@ module C06MapPrecond_Identity type i = i, type b = Item0.item, type f = Closure00.c06mapprecond_identity_closure0 i, - predicate Precondition0.precondition = Closure00.precondition, type Item0.item = Item0.item, + predicate Precondition0.precondition = Closure00.precondition, predicate Invariant0.invariant' = Invariant0.invariant', predicate Produces0.produces = Produces0.produces, predicate Reinitialize0.reinitialize = Reinitialize0.reinitialize, @@ -3098,7 +3098,7 @@ module C06MapPrecond_Increment_Interface type self = i clone C06MapPrecond_Common_Iterator_Completed_Stub as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = i val increment [#"../06_map_precond.rs" 185 0 185 50] (iter : i) : () requires {[#"../06_map_precond.rs" 181 0 181 187] forall done_ : borrowed i . Invariant0.invariant' done_ -> Completed0.completed done_ -> Invariant1.invariant' ( ^ done_) -> (forall steps : Seq.seq uint32 . forall next : i . Invariant1.invariant' next -> Produces0.produces ( ^ done_) steps next -> steps = Seq.empty /\ ^ done_ = next)} @@ -3220,7 +3220,7 @@ module C06MapPrecond_Increment predicate Produces0.produces = Produces0.produces, type Item0.item = uint32, axiom . - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = i, predicate Invariant0.invariant' = Invariant2.invariant' clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with @@ -3406,7 +3406,7 @@ module C06MapPrecond_Counter_Interface type self = i clone C06MapPrecond_Common_Iterator_Completed_Stub as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = i val counter [#"../06_map_precond.rs" 201 0 201 48] (iter : i) : () requires {[#"../06_map_precond.rs" 199 0 199 187] forall done_ : borrowed i . Invariant0.invariant' done_ -> Completed0.completed done_ -> Invariant1.invariant' ( ^ done_) -> (forall steps : Seq.seq uint32 . forall next : i . Invariant1.invariant' next -> Produces0.produces ( ^ done_) steps next -> steps = Seq.empty /\ ^ done_ = next)} @@ -3534,7 +3534,7 @@ module C06MapPrecond_Counter predicate Produces0.produces = Produces0.produces, type Item0.item = uint32, axiom . - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = i, predicate Invariant0.invariant' = Invariant1.invariant' clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with @@ -3695,7 +3695,7 @@ module C06MapPrecond_Impl0 predicate Invariant0.invariant' = Invariant2.invariant', predicate NextPrecondition0.next_precondition = NextPrecondition0.next_precondition, predicate Preservation0.preservation = Preservation0.preservation - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C06MapPrecond_Map_Type.t_map i Item0.item f, predicate Invariant0.invariant' = Invariant1.invariant' goal next_refn : [#"../06_map_precond.rs" 63 4 63 44] forall self : borrowed (C06MapPrecond_Map_Type.t_map i Item0.item f) . Invariant0.invariant' self -> Invariant0.invariant' self /\ Invariant1.invariant' ( * self) /\ (forall result : Core_Option_Option_Type.t_option b . Invariant1.invariant' ( ^ self) /\ Invariant1.invariant' ( ^ self) /\ match (result) with diff --git a/creusot/tests/should_succeed/iterators/07_fuse.mlcfg b/creusot/tests/should_succeed/iterators/07_fuse.mlcfg index 3b9d490c9b..1944c2d5fc 100644 --- a/creusot/tests/should_succeed/iterators/07_fuse.mlcfg +++ b/creusot/tests/should_succeed/iterators/07_fuse.mlcfg @@ -313,12 +313,12 @@ module C07Fuse_Impl1_Produces ensures { result = produces self prod other } end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -326,13 +326,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -448,7 +448,7 @@ module C07Fuse_Common_Iterator_Next_Interface clone C07Fuse_Common_Iterator_Completed_Stub as Completed0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = self val next [#"../common.rs" 27 4 27 45] (self : borrowed self) : Core_Option_Option_Type.t_option Item0.item requires {[#"../common.rs" 27 17 27 21] Invariant0.invariant' self} @@ -474,7 +474,7 @@ module C07Fuse_Impl1_Next_Interface clone C07Fuse_Impl1_Completed_Stub as Completed0 with type i = i use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C07Fuse_Fuse_Type.t_fuse i val next [#"../07_fuse.rs" 45 4 45 44] (self : borrowed (C07Fuse_Fuse_Type.t_fuse i)) : Core_Option_Option_Type.t_option Item0.item requires {[#"../07_fuse.rs" 45 17 45 21] Invariant0.invariant' self} @@ -508,7 +508,7 @@ module C07Fuse_Impl1_Next type Item0.item = Item0.item clone C07Fuse_Common_Iterator_Completed_Interface as Completed1 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant3.invariant' clone C07Fuse_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with @@ -533,7 +533,7 @@ module C07Fuse_Impl1_Next predicate Produces0.produces = Produces1.produces clone C07Fuse_Impl1_Completed as Completed0 with type i = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C07Fuse_Fuse_Type.t_fuse i, predicate Invariant0.invariant' = Invariant1.invariant' clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve4 with @@ -878,7 +878,7 @@ module C07Fuse_Impl3_IsFused_Stub use C07Fuse_Fuse_Type as C07Fuse_Fuse_Type clone C07Fuse_Impl2_Invariant_Stub as Invariant1 with type i = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C07Fuse_Fuse_Type.t_fuse i clone C07Fuse_Impl1_Produces_Stub as Produces0 with type i = i, @@ -897,7 +897,7 @@ module C07Fuse_Impl3_IsFused_Interface use C07Fuse_Fuse_Type as C07Fuse_Fuse_Type clone C07Fuse_Impl2_Invariant_Stub as Invariant1 with type i = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C07Fuse_Fuse_Type.t_fuse i clone C07Fuse_Impl1_Produces_Stub as Produces0 with type i = i, @@ -926,7 +926,7 @@ module C07Fuse_Impl3_IsFused use C07Fuse_Fuse_Type as C07Fuse_Fuse_Type clone C07Fuse_Impl2_Invariant_Stub as Invariant1 with type i = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C07Fuse_Fuse_Type.t_fuse i clone C07Fuse_Impl1_Produces_Stub as Produces0 with type i = i, @@ -1000,7 +1000,7 @@ module C07Fuse_Impl3_IsFused_Impl predicate Produces0.produces = Produces0.produces, type Item0.item = Item0.item, axiom . - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C07Fuse_Fuse_Type.t_fuse i, predicate Invariant0.invariant' = Invariant1.invariant' clone C07Fuse_Impl1_Completed as Completed0 with @@ -1045,7 +1045,7 @@ module C07Fuse_Impl1 clone C07Fuse_Impl2_Invariant as Invariant1 with type i = i, predicate Invariant0.invariant' = Invariant2.invariant' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C07Fuse_Fuse_Type.t_fuse i, predicate Invariant0.invariant' = Invariant1.invariant' goal next_refn : [#"../07_fuse.rs" 45 4 45 44] forall self : borrowed (C07Fuse_Fuse_Type.t_fuse i) . Invariant0.invariant' self -> Invariant0.invariant' self /\ (forall result : Core_Option_Option_Type.t_option Item0.item . Invariant1.invariant' ( ^ self) /\ match (result) with @@ -1087,7 +1087,7 @@ module C07Fuse_Impl3 clone C07Fuse_Impl2_Invariant as Invariant0 with type i = i, predicate Invariant0.invariant' = Invariant2.invariant' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C07Fuse_Fuse_Type.t_fuse i, predicate Invariant0.invariant' = Invariant0.invariant' goal is_fused_refn : [#"../07_fuse.rs" 98 4 98 62] forall self : borrowed (C07Fuse_Fuse_Type.t_fuse i) . forall steps : Seq.seq Item0.item . forall next : C07Fuse_Fuse_Type.t_fuse i . Invariant0.invariant' next /\ Invariant1.invariant' self /\ Produces0.produces ( ^ self) steps next /\ Completed0.completed self -> Invariant0.invariant' next /\ Invariant1.invariant' self /\ Produces0.produces ( ^ self) steps next /\ Completed0.completed self /\ (forall result : () . Invariant0.invariant' ( ^ self) /\ steps = Seq.empty /\ ^ self = next -> Invariant0.invariant' ( ^ self) /\ steps = Seq.empty /\ ^ self = next) diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg b/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg index c5ed6a4ac2..ae53af35ab 100644 --- a/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg +++ b/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg @@ -18,12 +18,12 @@ module CreusotContracts_Invariant_Invariant_Invariant ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -31,13 +31,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -433,7 +433,7 @@ module Core_Iter_Traits_Iterator_Iterator_Next_Interface clone CreusotContracts_Std1_Iter_Iterator_Completed_Stub as Completed0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = self val next (self : borrowed self) : Core_Option_Option_Type.t_option Item0.item requires {Invariant0.invariant' self} @@ -661,7 +661,7 @@ module C08CollectExtend_Extend_Interface type Item0.item = t clone CreusotContracts_Std1_Iter_Iterator_Completed_Stub as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant1 with type t = i clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = i @@ -722,7 +722,7 @@ module C08CollectExtend_Extend predicate Invariant0.invariant' = Invariant0.invariant' clone CreusotContracts_Std1_Iter_Iterator_Completed_Interface as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = i, predicate Invariant0.invariant' = Invariant0.invariant' clone Alloc_Vec_Impl1_Push_Interface as Push0 with @@ -1005,7 +1005,7 @@ module C08CollectExtend_Collect_Interface type Item0.item = Item0.item clone CreusotContracts_Std1_Iter_Iterator_Completed_Stub as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant1 with type t = i clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = i @@ -1019,9 +1019,9 @@ module C08CollectExtend_Collect use prelude.Ghost use seq.Seq use prelude.Borrow + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with type self = i - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type clone Core_Num_Impl11_Max as Max0 clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Interface as ShallowModel0 with @@ -1069,7 +1069,7 @@ module C08CollectExtend_Collect predicate Invariant0.invariant' = Invariant0.invariant' clone CreusotContracts_Std1_Iter_Iterator_Completed_Interface as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = i, predicate Invariant0.invariant' = Invariant0.invariant' clone Alloc_Vec_Impl1_Push_Interface as Push0 with @@ -1689,7 +1689,7 @@ module C08CollectExtend_ExtendIndex type a = Alloc_Alloc_Global_Type.t_global, predicate Resolve0.resolve = Resolve3.resolve, function ShallowModel0.shallow_model = ShallowModel7.shallow_model - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = Alloc_Vec_IntoIter_IntoIter_Type.t_intoiter uint32 (Alloc_Alloc_Global_Type.t_global), predicate Invariant0.invariant' = Invariant0.invariant' clone CreusotContracts_Std1_Vec_Impl3_IntoIterPost as IntoIterPost0 with @@ -1842,7 +1842,7 @@ module C08CollectExtend_CollectExample clone Core_Num_Impl11_Max as Max0 clone CreusotContracts_Std1_Iter_Iterator_Completed_Interface as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = i, predicate Invariant0.invariant' = Invariant0.invariant' use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz b/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz index c667278c34..713d0fc209 100644 Binary files a/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz and b/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/09_empty.mlcfg b/creusot/tests/should_succeed/iterators/09_empty.mlcfg index 58d5070aef..5138f6dbe4 100644 --- a/creusot/tests/should_succeed/iterators/09_empty.mlcfg +++ b/creusot/tests/should_succeed/iterators/09_empty.mlcfg @@ -266,12 +266,12 @@ module CreusotContracts_Invariant_Invariant_Invariant ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -279,13 +279,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -311,7 +311,7 @@ module C09Empty_Impl0 clone C09Empty_Impl0_Completed as Completed0 with type t = t, predicate Resolve0.resolve = Resolve0.resolve - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C09Empty_Empty_Type.t_empty t, predicate Invariant0.invariant' = Invariant1.invariant' goal next_refn : [#"../09_empty.rs" 41 4 41 35] forall self : borrowed (C09Empty_Empty_Type.t_empty t) . Invariant0.invariant' self -> (forall result : Core_Option_Option_Type.t_option t . match (result) with diff --git a/creusot/tests/should_succeed/iterators/10_once.mlcfg b/creusot/tests/should_succeed/iterators/10_once.mlcfg index d6c99f4b39..0f4f6d8f0e 100644 --- a/creusot/tests/should_succeed/iterators/10_once.mlcfg +++ b/creusot/tests/should_succeed/iterators/10_once.mlcfg @@ -286,12 +286,12 @@ module CreusotContracts_Invariant_Invariant_Invariant ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -299,13 +299,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -329,7 +329,7 @@ module C10Once_Impl0 predicate Resolve0.resolve = Resolve0.resolve clone CreusotContracts_Invariant_Invariant_Invariant as Invariant0 with type self = C10Once_Once_Type.t_once t - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C10Once_Once_Type.t_once t, predicate Invariant0.invariant' = Invariant0.invariant' clone C10Once_Impl0_Produces as Produces0 with diff --git a/creusot/tests/should_succeed/iterators/11_repeat.mlcfg b/creusot/tests/should_succeed/iterators/11_repeat.mlcfg index 2e28d167ac..e0bd6e1264 100644 --- a/creusot/tests/should_succeed/iterators/11_repeat.mlcfg +++ b/creusot/tests/should_succeed/iterators/11_repeat.mlcfg @@ -277,12 +277,12 @@ module CreusotContracts_Invariant_Invariant_Invariant ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -290,13 +290,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -317,7 +317,7 @@ module C11Repeat_Impl0 type a = a clone CreusotContracts_Invariant_Invariant_Invariant as Invariant0 with type self = C11Repeat_Repeat_Type.t_repeat a - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C11Repeat_Repeat_Type.t_repeat a, predicate Invariant0.invariant' = Invariant0.invariant' clone C11Repeat_Impl0_Produces as Produces0 with diff --git a/creusot/tests/should_succeed/iterators/12_zip.mlcfg b/creusot/tests/should_succeed/iterators/12_zip.mlcfg index 576dcbb614..82c14c14d4 100644 --- a/creusot/tests/should_succeed/iterators/12_zip.mlcfg +++ b/creusot/tests/should_succeed/iterators/12_zip.mlcfg @@ -629,12 +629,12 @@ module C12Zip_Impl0_ProducesTrans_Impl = [@vc:do_not_keep_trace] [@vc:sp] [#"../12_zip.rs" 39 4 39 10] () end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -642,13 +642,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -744,7 +744,7 @@ module C12Zip_Common_Iterator_Next_Interface clone C12Zip_Common_Iterator_Completed_Stub as Completed0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = self val next [#"../common.rs" 27 4 27 45] (self : borrowed self) : Core_Option_Option_Type.t_option Item0.item requires {[#"../common.rs" 27 17 27 21] Invariant0.invariant' self} @@ -777,7 +777,7 @@ module C12Zip_Impl0_Next_Interface type i = i, type j = j use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C12Zip_Zip_Type.t_zip i j val next [#"../12_zip.rs" 50 4 50 44] (self : borrowed (C12Zip_Zip_Type.t_zip i j)) : Core_Option_Option_Type.t_option (Item0.item, Item1.item) requires {[#"../12_zip.rs" 50 17 50 21] Invariant0.invariant' self} @@ -819,7 +819,7 @@ module C12Zip_Impl0_Next type Item0.item = Item1.item clone C12Zip_Common_Iterator_Completed_Interface as Completed2 with type self = j - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant4 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant4 with type t = j, predicate Invariant0.invariant' = Invariant5.invariant' clone C12Zip_Common_Iterator_ProducesTrans_Interface as ProducesTrans1 with @@ -839,7 +839,7 @@ module C12Zip_Impl0_Next type Item0.item = Item0.item clone C12Zip_Common_Iterator_Completed_Interface as Completed1 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant3.invariant' clone C12Zip_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with @@ -872,7 +872,7 @@ module C12Zip_Impl0_Next type j = j, predicate Completed0.completed = Completed1.completed, predicate Completed1.completed = Completed2.completed - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C12Zip_Zip_Type.t_zip i j, predicate Invariant0.invariant' = Invariant1.invariant' clone CreusotContracts_Resolve_Impl0_Resolve as Resolve1 with @@ -1033,7 +1033,7 @@ module C12Zip_Impl0 type j = j, predicate Invariant0.invariant' = Invariant2.invariant', predicate Invariant1.invariant' = Invariant3.invariant' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C12Zip_Zip_Type.t_zip i j, predicate Invariant0.invariant' = Invariant1.invariant' goal next_refn : [#"../12_zip.rs" 50 4 50 44] forall self : borrowed (C12Zip_Zip_Type.t_zip i j) . Invariant0.invariant' self -> Invariant0.invariant' self /\ (forall result : Core_Option_Option_Type.t_option (Item0.item, Item1.item) . Invariant1.invariant' ( ^ self) /\ match (result) with diff --git a/creusot/tests/should_succeed/iterators/13_cloned.mlcfg b/creusot/tests/should_succeed/iterators/13_cloned.mlcfg index 4192ec7750..de118c386a 100644 --- a/creusot/tests/should_succeed/iterators/13_cloned.mlcfg +++ b/creusot/tests/should_succeed/iterators/13_cloned.mlcfg @@ -515,12 +515,12 @@ module C13Cloned_Impl0_ProducesTrans_Impl = [@vc:do_not_keep_trace] [@vc:sp] [#"../13_cloned.rs" 41 4 41 10] () end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -528,13 +528,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -581,7 +581,7 @@ module C13Cloned_Common_Iterator_Next_Interface clone C13Cloned_Common_Iterator_Completed_Stub as Completed0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = self val next [#"../common.rs" 27 4 27 45] (self : borrowed self) : Core_Option_Option_Type.t_option Item0.item requires {[#"../common.rs" 27 17 27 21] Invariant0.invariant' self} @@ -617,7 +617,7 @@ module C13Cloned_Impl0_Next_Interface type i = i, type t = t use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C13Cloned_Cloned_Type.t_cloned i val next [#"../13_cloned.rs" 52 4 52 35] (self : borrowed (C13Cloned_Cloned_Type.t_cloned i)) : Core_Option_Option_Type.t_option t requires {[#"../13_cloned.rs" 52 17 52 21] Invariant0.invariant' self} @@ -645,7 +645,7 @@ module C13Cloned_Impl0_Next clone C13Cloned_Common_Iterator_Completed_Interface as Completed1 with type self = i use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant3.invariant' clone C13Cloned_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with @@ -673,10 +673,10 @@ module C13Cloned_Impl0_Next type i = i, type t = t, predicate Completed0.completed = Completed1.completed - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C13Cloned_Cloned_Type.t_cloned i, predicate Invariant0.invariant' = Invariant1.invariant' - clone Core_Option_Impl2_Cloned_Interface as Cloned1 with + clone Core_Option_Impl2_Cloned_Interface as Cloned0 with type t = t clone C13Cloned_Common_Iterator_Next_Interface as Next0 with type self = i, @@ -709,7 +709,7 @@ module C13Cloned_Impl0_Next } BB1 { assume { Resolve0.resolve self }; - _0 <- ([#"../13_cloned.rs" 53 8 53 33] Cloned1.cloned ([#"../13_cloned.rs" 53 8 53 24] Next0.next _4)); + _0 <- ([#"../13_cloned.rs" 53 8 53 33] Cloned0.cloned ([#"../13_cloned.rs" 53 8 53 24] Next0.next _4)); _4 <- any borrowed i; goto BB2 } @@ -746,7 +746,7 @@ module C13Cloned_Impl0 type i = i, type t = t, predicate Invariant0.invariant' = Invariant2.invariant' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C13Cloned_Cloned_Type.t_cloned i, predicate Invariant0.invariant' = Invariant1.invariant' goal next_refn : [#"../13_cloned.rs" 52 4 52 35] forall self : borrowed (C13Cloned_Cloned_Type.t_cloned i) . Invariant0.invariant' self -> Invariant0.invariant' self /\ (forall result : Core_Option_Option_Type.t_option t . Invariant1.invariant' ( ^ self) /\ match (result) with diff --git a/creusot/tests/should_succeed/iterators/14_copied.mlcfg b/creusot/tests/should_succeed/iterators/14_copied.mlcfg index cfba103b82..379063b113 100644 --- a/creusot/tests/should_succeed/iterators/14_copied.mlcfg +++ b/creusot/tests/should_succeed/iterators/14_copied.mlcfg @@ -515,12 +515,12 @@ module C14Copied_Impl0_ProducesTrans_Impl = [@vc:do_not_keep_trace] [@vc:sp] [#"../14_copied.rs" 41 4 41 10] () end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -528,13 +528,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -581,7 +581,7 @@ module C14Copied_Common_Iterator_Next_Interface clone C14Copied_Common_Iterator_Completed_Stub as Completed0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = self val next [#"../common.rs" 27 4 27 45] (self : borrowed self) : Core_Option_Option_Type.t_option Item0.item requires {[#"../common.rs" 27 17 27 21] Invariant0.invariant' self} @@ -617,7 +617,7 @@ module C14Copied_Impl0_Next_Interface type i = i, type t = t use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C14Copied_Copied_Type.t_copied i val next [#"../14_copied.rs" 52 4 52 35] (self : borrowed (C14Copied_Copied_Type.t_copied i)) : Core_Option_Option_Type.t_option t requires {[#"../14_copied.rs" 52 17 52 21] Invariant0.invariant' self} @@ -645,7 +645,7 @@ module C14Copied_Impl0_Next clone C14Copied_Common_Iterator_Completed_Interface as Completed1 with type self = i use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant3.invariant' clone C14Copied_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with @@ -673,10 +673,10 @@ module C14Copied_Impl0_Next type i = i, type t = t, predicate Completed0.completed = Completed1.completed - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C14Copied_Copied_Type.t_copied i, predicate Invariant0.invariant' = Invariant1.invariant' - clone Core_Option_Impl2_Copied_Interface as Copied1 with + clone Core_Option_Impl2_Copied_Interface as Copied0 with type t = t clone C14Copied_Common_Iterator_Next_Interface as Next0 with type self = i, @@ -709,7 +709,7 @@ module C14Copied_Impl0_Next } BB1 { assume { Resolve0.resolve self }; - _0 <- ([#"../14_copied.rs" 53 8 53 33] Copied1.copied ([#"../14_copied.rs" 53 8 53 24] Next0.next _4)); + _0 <- ([#"../14_copied.rs" 53 8 53 33] Copied0.copied ([#"../14_copied.rs" 53 8 53 24] Next0.next _4)); _4 <- any borrowed i; goto BB2 } @@ -742,7 +742,7 @@ module C14Copied_Impl0 type i = i, type t = t, predicate Invariant0.invariant' = Invariant2.invariant' - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C14Copied_Copied_Type.t_copied i, predicate Invariant0.invariant' = Invariant0.invariant' clone C14Copied_Impl0_Produces as Produces0 with diff --git a/creusot/tests/should_succeed/iterators/15_enumerate.mlcfg b/creusot/tests/should_succeed/iterators/15_enumerate.mlcfg index 13750a1a5f..84b3a743b9 100644 --- a/creusot/tests/should_succeed/iterators/15_enumerate.mlcfg +++ b/creusot/tests/should_succeed/iterators/15_enumerate.mlcfg @@ -294,12 +294,12 @@ module C15Enumerate_Impl0_Produces ensures { result = produces self visited o } end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -307,13 +307,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -350,7 +350,7 @@ module C15Enumerate_Impl1_Invariant use prelude.Borrow clone C15Enumerate_Common_Iterator_Completed_Stub as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant1 with type t = i clone Core_Usize_Max_Stub as Max0 clone C15Enumerate_Common_Iterator_Item_Type as Item0 with @@ -447,7 +447,7 @@ module C15Enumerate_Impl0_ProducesRefl_Impl axiom . clone C15Enumerate_Common_Iterator_Completed_Interface as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant1.invariant' clone Core_Usize_Max as Max0 @@ -571,7 +571,7 @@ module C15Enumerate_Impl0_ProducesTrans_Impl axiom . clone C15Enumerate_Common_Iterator_Completed_Interface as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant1.invariant' clone Core_Usize_Max as Max0 @@ -664,7 +664,7 @@ module C15Enumerate_Common_Iterator_Next_Interface clone C15Enumerate_Common_Iterator_Completed_Stub as Completed0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = self val next [#"../common.rs" 27 4 27 45] (self : borrowed self) : Core_Option_Option_Type.t_option Item0.item requires {[#"../common.rs" 27 17 27 21] Invariant0.invariant' self} @@ -692,7 +692,7 @@ module C15Enumerate_Impl0_Next_Interface clone C15Enumerate_Impl0_Completed_Stub as Completed0 with type i = i use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = C15Enumerate_Enumerate_Type.t_enumerate i val next [#"../15_enumerate.rs" 53 4 53 44] (self : borrowed (C15Enumerate_Enumerate_Type.t_enumerate i)) : Core_Option_Option_Type.t_option (usize, Item0.item) requires {[#"../15_enumerate.rs" 53 17 53 21] Invariant0.invariant' self} @@ -723,7 +723,7 @@ module C15Enumerate_Impl0_Next type Item0.item = Item0.item clone C15Enumerate_Common_Iterator_Completed_Interface as Completed1 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = i, predicate Invariant0.invariant' = Invariant3.invariant' clone C15Enumerate_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with @@ -754,7 +754,7 @@ module C15Enumerate_Impl0_Next clone C15Enumerate_Impl0_Completed as Completed0 with type i = i, predicate Completed0.completed = Completed1.completed - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = C15Enumerate_Enumerate_Type.t_enumerate i, predicate Invariant0.invariant' = Invariant1.invariant' use Core_Option_Option_Type as Core_Option_Option_Type @@ -861,7 +861,7 @@ module C15Enumerate_Enumerate_Interface type Item0.item = Item0.item clone C15Enumerate_Common_Iterator_Completed_Stub as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = i val enumerate [#"../15_enumerate.rs" 82 0 82 54] (iter : i) : C15Enumerate_Enumerate_Type.t_enumerate i requires {[#"../15_enumerate.rs" 80 0 80 75] forall i : borrowed i . Invariant0.invariant' i -> Completed0.completed i -> Produces0.produces ( * i) (Seq.empty ) ( ^ i)} @@ -901,7 +901,7 @@ module C15Enumerate_Enumerate axiom . clone C15Enumerate_Common_Iterator_Completed_Interface as Completed0 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = i, predicate Invariant0.invariant' = Invariant1.invariant' clone Core_Usize_Max as Max0 @@ -952,7 +952,7 @@ module C15Enumerate_Impl0 type self = i clone CreusotContracts_Invariant_Invariant_Invariant_Interface as Invariant2 with type self = i - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant3 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant3 with type t = i, predicate Invariant0.invariant' = Invariant2.invariant' clone Core_Usize_Max as Max0 @@ -976,7 +976,7 @@ module C15Enumerate_Impl0 val Max0.mAX' = Max0.mAX', predicate Invariant1.invariant' = Invariant3.invariant', predicate Completed0.completed = Completed1.completed - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = C15Enumerate_Enumerate_Type.t_enumerate i, predicate Invariant0.invariant' = Invariant0.invariant' clone C15Enumerate_Impl0_Produces as Produces0 with diff --git a/creusot/tests/should_succeed/list_index_mut.mlcfg b/creusot/tests/should_succeed/list_index_mut.mlcfg index 5d910b4b6a..9a4239cc19 100644 --- a/creusot/tests/should_succeed/list_index_mut.mlcfg +++ b/creusot/tests/should_succeed/list_index_mut.mlcfg @@ -10,40 +10,9 @@ module ListIndexMut_Option_Type | C_Some a -> a end end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - -end module ListIndexMut_List_Type use prelude.Int use prelude.UInt32 - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use ListIndexMut_Option_Type as ListIndexMut_Option_Type type t_list = | C_List uint32 (ListIndexMut_Option_Type.t_option (t_list)) @@ -72,9 +41,7 @@ module ListIndexMut_Len_Interface end module ListIndexMut_Len use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use ListIndexMut_List_Type as ListIndexMut_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use ListIndexMut_Option_Type as ListIndexMut_Option_Type function len [#"../list_index_mut.rs" 14 0 14 22] (l : ListIndexMut_List_Type.t_list) : int = [#"../list_index_mut.rs" 13 0 13 8] let ListIndexMut_List_Type.C_List _ ls = l in 1 + match (ls) with @@ -107,9 +74,7 @@ end module ListIndexMut_Get use prelude.Int use prelude.UInt32 - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use ListIndexMut_List_Type as ListIndexMut_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use ListIndexMut_Option_Type as ListIndexMut_Option_Type function get [#"../list_index_mut.rs" 25 0 25 39] (l : ListIndexMut_List_Type.t_list) (ix : int) : ListIndexMut_Option_Type.t_option uint32 @@ -171,12 +136,10 @@ module ListIndexMut_IndexMut use prelude.Int use prelude.UIntSize use prelude.UInt32 - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use ListIndexMut_List_Type as ListIndexMut_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use ListIndexMut_Option_Type as ListIndexMut_Option_Type clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with type t = uint32 + use ListIndexMut_List_Type as ListIndexMut_List_Type clone CreusotContracts_Resolve_Impl1_Resolve as Resolve1 with type t = ListIndexMut_List_Type.t_list clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with @@ -292,9 +255,7 @@ module ListIndexMut_Write use prelude.Int use prelude.UIntSize use prelude.UInt32 - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use ListIndexMut_List_Type as ListIndexMut_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use ListIndexMut_Option_Type as ListIndexMut_Option_Type clone ListIndexMut_Get as Get0 clone ListIndexMut_Len as Len0 @@ -345,9 +306,7 @@ module ListIndexMut_F use prelude.UInt32 use prelude.UIntSize use prelude.Borrow - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use ListIndexMut_List_Type as ListIndexMut_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use ListIndexMut_Option_Type as ListIndexMut_Option_Type clone ListIndexMut_Get as Get0 clone ListIndexMut_Len as Len0 diff --git a/creusot/tests/should_succeed/list_index_mut/why3session.xml b/creusot/tests/should_succeed/list_index_mut/why3session.xml index 238fcddd2f..2ea2208cd6 100644 --- a/creusot/tests/should_succeed/list_index_mut/why3session.xml +++ b/creusot/tests/should_succeed/list_index_mut/why3session.xml @@ -7,7 +7,7 @@ - + diff --git a/creusot/tests/should_succeed/list_index_mut/why3shapes.gz b/creusot/tests/should_succeed/list_index_mut/why3shapes.gz index b845885ea9..f973ea49c6 100644 Binary files a/creusot/tests/should_succeed/list_index_mut/why3shapes.gz and b/creusot/tests/should_succeed/list_index_mut/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/red_black_tree.mlcfg b/creusot/tests/should_succeed/red_black_tree.mlcfg index 36ed77793e..bf3e98defe 100644 --- a/creusot/tests/should_succeed/red_black_tree.mlcfg +++ b/creusot/tests/should_succeed/red_black_tree.mlcfg @@ -60,38 +60,7 @@ module Core_Option_Option_Type | C_Some a -> a end end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - -end module RedBlackTree_Node_Type - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type type t_node 'k 'v = @@ -180,14 +149,12 @@ end module RedBlackTree_Impl0_HasMapping type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type predicate has_mapping [#"../red_black_tree.rs" 31 4 31 57] (self : RedBlackTree_Tree_Type.t_tree k v) (k : DeepModelTy0.deepModelTy) (v : v) @@ -265,14 +232,12 @@ module RedBlackTree_Impl0_ModelAcc type k type v use map.Map - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type function model_acc [#"../red_black_tree.rs" 49 4 52 47] (self : RedBlackTree_Tree_Type.t_tree k v) (accu : Map.map DeepModelTy0.deepModelTy (Core_Option_Option_Type.t_option v)) : Map.map DeepModelTy0.deepModelTy (Core_Option_Option_Type.t_option v) @@ -333,14 +298,12 @@ module RedBlackTree_Impl0_ModelAccHasMapping type k type v use map.Map - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl0_HasMapping_Stub as HasMapping0 with @@ -368,14 +331,12 @@ module RedBlackTree_Impl0_ModelAccHasMapping_Impl type k type v use map.Map - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k clone CreusotContracts_Model_DeepModel_DeepModel_Interface as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl0_HasMapping as HasMapping0 with @@ -502,9 +463,7 @@ end module RedBlackTree_Impl5_BstInvariant type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone RedBlackTree_Impl4_BstInvariantHere_Stub as BstInvariantHere0 with type k = k, type v = v @@ -950,9 +909,6 @@ module RedBlackTree_Impl0_HasMappingModelAcc type k type v use map.Map - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type @@ -975,6 +931,7 @@ module RedBlackTree_Impl0_HasMappingModelAcc clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type clone RedBlackTree_Impl5_BstInvariant_Stub as BstInvariant0 with type k = k, type v = v @@ -1049,13 +1006,11 @@ module RedBlackTree_Impl0_HasMappingModelAcc_Impl predicate LeLog0.le_log = LeLog0.le_log, function CmpLog0.cmp_log = CmpLog0.cmp_log, axiom . - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone CreusotContracts_Model_DeepModel_DeepModel_Interface as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl0_HasMapping as HasMapping0 with type k = k, @@ -1300,12 +1255,10 @@ module RedBlackTree_Impl0_HasMappingModel_Impl predicate LeLog0.le_log = LeLog0.le_log, function CmpLog0.cmp_log = CmpLog0.cmp_log, axiom . - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModel_Interface as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl0_ModelAcc as ModelAcc0 with @@ -1499,12 +1452,10 @@ module RedBlackTree_Impl0_HasMappingInj_Impl predicate LeLog0.le_log = LeLog0.le_log, function CmpLog0.cmp_log = CmpLog0.cmp_log, axiom . - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModel_Interface as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl0_ModelAcc as ModelAcc0 with @@ -1577,9 +1528,6 @@ end module RedBlackTree_Impl1_HasMapping_Stub type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type @@ -1587,6 +1535,7 @@ module RedBlackTree_Impl1_HasMapping_Stub type k = k, type v = v, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type predicate has_mapping [#"../red_black_tree.rs" 140 4 140 57] (self : RedBlackTree_Node_Type.t_node k v) (k : DeepModelTy0.deepModelTy) (v : v) @@ -1594,9 +1543,6 @@ end module RedBlackTree_Impl1_HasMapping_Interface type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type @@ -1604,6 +1550,7 @@ module RedBlackTree_Impl1_HasMapping_Interface type k = k, type v = v, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type predicate has_mapping [#"../red_black_tree.rs" 140 4 140 57] (self : RedBlackTree_Node_Type.t_node k v) (k : DeepModelTy0.deepModelTy) (v : v) @@ -1616,9 +1563,6 @@ end module RedBlackTree_Impl1_HasMapping type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with @@ -1629,6 +1573,7 @@ module RedBlackTree_Impl1_HasMapping type k = k, type v = v, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type predicate has_mapping [#"../red_black_tree.rs" 140 4 140 57] (self : RedBlackTree_Node_Type.t_node k v) (k : DeepModelTy0.deepModelTy) (v : v) @@ -1643,14 +1588,12 @@ end module RedBlackTree_Impl1_HasMapping_Impl type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k clone CreusotContracts_Model_DeepModel_DeepModel_Interface as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl0_HasMapping as HasMapping0 with @@ -1684,9 +1627,6 @@ end module RedBlackTree_Impl1_SameMappings type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type @@ -1694,6 +1634,7 @@ module RedBlackTree_Impl1_SameMappings type k = k, type v = v, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl1_HasMapping_Stub as HasMapping0 with type k = k, @@ -1849,9 +1790,7 @@ end module RedBlackTree_Impl7_Color type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type @@ -1914,9 +1853,7 @@ end module RedBlackTree_Impl7_ColorInvariant type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone RedBlackTree_Impl8_ColorInvariantHere_Stub as ColorInvariantHere0 with type k = k, type v = v @@ -1953,10 +1890,8 @@ end module RedBlackTree_Impl6_MatchT type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl7_ColorInvariant_Stub as ColorInvariant0 with @@ -2074,10 +2009,8 @@ module RedBlackTree_Impl9_Height type k type v use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type function height [#"../red_black_tree.rs" 296 4 296 26] (self : RedBlackTree_Tree_Type.t_tree k v) : int = @@ -2098,10 +2031,8 @@ module RedBlackTree_Impl9_Height_Impl type k type v use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type let rec ghost function height [#"../red_black_tree.rs" 296 4 296 26] (self : RedBlackTree_Tree_Type.t_tree k v) : int @@ -2164,9 +2095,7 @@ end module RedBlackTree_Impl9_HeightInvariant type k type v - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone RedBlackTree_Impl10_HeightInvariantHere_Stub as HeightInvariantHere0 with type k = k, type v = v @@ -2185,14 +2114,12 @@ module RedBlackTree_Impl10_Height_Stub type k type v use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl9_Height_Stub as Height0 with type k = k, type v = v, axiom . + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type function height [#"../red_black_tree.rs" 328 4 328 26] (self : RedBlackTree_Node_Type.t_node k v) : int end @@ -2200,14 +2127,12 @@ module RedBlackTree_Impl10_Height_Interface type k type v use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl9_Height_Stub as Height0 with type k = k, type v = v, axiom . + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type function height [#"../red_black_tree.rs" 328 4 328 26] (self : RedBlackTree_Node_Type.t_node k v) : int val height [#"../red_black_tree.rs" 328 4 328 26] (self : RedBlackTree_Node_Type.t_node k v) : int @@ -2220,15 +2145,13 @@ module RedBlackTree_Impl10_Height type k type v use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl9_Height_Stub as Height0 with type k = k, type v = v, axiom . + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type function height [#"../red_black_tree.rs" 328 4 328 26] (self : RedBlackTree_Node_Type.t_node k v) : int = [#"../red_black_tree.rs" 330 12 333 13] match (RedBlackTree_Node_Type.node_color self) with @@ -2245,10 +2168,8 @@ module RedBlackTree_Impl10_Height_Impl type k type v use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl9_Height as Height0 with @@ -2428,19 +2349,17 @@ module RedBlackTree_Impl13_IsRed type k type v use prelude.Borrow - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with type self = RedBlackTree_Tree_Type.t_tree k v let rec cfg is_red [#"../red_black_tree.rs" 388 4 388 28] [@cfg:stackify] [@cfg:subregion_analysis] (self : RedBlackTree_Tree_Type.t_tree k v) : bool - ensures { [#"../red_black_tree.rs" 387 14 387 45] result = (Color1.color self = RedBlackTree_Color_Type.C_Red) } + ensures { [#"../red_black_tree.rs" 387 14 387 45] result = (Color0.color self = RedBlackTree_Color_Type.C_Red) } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : bool; @@ -2573,9 +2492,6 @@ module RedBlackTree_Impl14_RotateRight_Interface type k type v use prelude.Borrow - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type @@ -2583,6 +2499,7 @@ module RedBlackTree_Impl14_RotateRight_Interface type k = k, type v = v, axiom . + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Logic_Ord_OrdLogic_LtLog_Stub as LtLog0 with type self = DeepModelTy0.deepModelTy @@ -2632,11 +2549,9 @@ module RedBlackTree_Impl14_RotateRight type self = DeepModelTy0.deepModelTy clone CreusotContracts_Logic_Ord_OrdLogic_LeLog_Interface as LeLog0 with type self = DeepModelTy0.deepModelTy - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height1 with type k = k, @@ -2742,7 +2657,7 @@ module RedBlackTree_Impl14_RotateRight type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, predicate HasMapping0.has_mapping = HasMapping1.has_mapping, predicate HasMapping1.has_mapping = HasMapping0.has_mapping - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl12_InternalInvariant as InternalInvariant0 with @@ -2777,12 +2692,12 @@ module RedBlackTree_Impl14_RotateRight type self = Ghost.ghost_ty (borrowed (RedBlackTree_Node_Type.t_node k v)) let rec cfg rotate_right [#"../red_black_tree.rs" 412 4 412 30] [@cfg:stackify] [@cfg:subregion_analysis] (self : borrowed (RedBlackTree_Node_Type.t_node k v)) : () requires {[#"../red_black_tree.rs" 400 15 400 43] InternalInvariant0.internal_invariant ( * self)} - requires {[#"../red_black_tree.rs" 401 15 401 42] Color1.color (RedBlackTree_Node_Type.node_left ( * self)) = RedBlackTree_Color_Type.C_Red} + requires {[#"../red_black_tree.rs" 401 15 401 42] Color0.color (RedBlackTree_Node_Type.node_left ( * self)) = RedBlackTree_Color_Type.C_Red} ensures { [#"../red_black_tree.rs" 402 14 402 42] SameMappings0.same_mappings ( * self) ( ^ self) } ensures { [#"../red_black_tree.rs" 403 14 403 42] InternalInvariant0.internal_invariant ( ^ self) } ensures { [#"../red_black_tree.rs" 404 14 404 50] Height0.height ( * self) = Height0.height ( ^ self) } ensures { [#"../red_black_tree.rs" 405 14 405 65] LtLog0.lt_log (DeepModel0.deep_model (RedBlackTree_Node_Type.node_key ( ^ self))) (DeepModel0.deep_model (RedBlackTree_Node_Type.node_key ( * self))) } - ensures { [#"../red_black_tree.rs" 406 14 406 42] Color1.color (RedBlackTree_Node_Type.node_right ( ^ self)) = RedBlackTree_Color_Type.C_Red } + ensures { [#"../red_black_tree.rs" 406 14 406 42] Color0.color (RedBlackTree_Node_Type.node_right ( ^ self)) = RedBlackTree_Color_Type.C_Red } ensures { [#"../red_black_tree.rs" 407 14 407 44] RedBlackTree_Node_Type.node_color ( ^ self) = RedBlackTree_Node_Type.node_color ( * self) } ensures { [#"../red_black_tree.rs" 408 4 411 36] exists r : RedBlackTree_Node_Type.t_node k v . exists l : RedBlackTree_Node_Type.t_node k v . RedBlackTree_Tree_Type.tree_node (RedBlackTree_Node_Type.node_left ( * self)) = Core_Option_Option_Type.C_Some l /\ RedBlackTree_Tree_Type.tree_node (RedBlackTree_Node_Type.node_right ( ^ self)) = Core_Option_Option_Type.C_Some r /\ (RedBlackTree_Node_Type.node_left ( ^ self), RedBlackTree_Node_Type.node_left r, RedBlackTree_Node_Type.node_right r) = (RedBlackTree_Node_Type.node_left l, RedBlackTree_Node_Type.node_right l, RedBlackTree_Node_Type.node_right ( * self)) /\ RedBlackTree_Node_Type.node_key r = RedBlackTree_Node_Type.node_key ( * self) } @@ -2903,9 +2818,6 @@ module RedBlackTree_Impl14_RotateLeft_Interface type k type v use prelude.Borrow - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type @@ -2913,6 +2825,7 @@ module RedBlackTree_Impl14_RotateLeft_Interface type k = k, type v = v, axiom . + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Logic_Ord_OrdLogic_LtLog_Stub as LtLog0 with type self = DeepModelTy0.deepModelTy @@ -2962,11 +2875,9 @@ module RedBlackTree_Impl14_RotateLeft type self = DeepModelTy0.deepModelTy clone CreusotContracts_Logic_Ord_OrdLogic_LeLog_Interface as LeLog0 with type self = DeepModelTy0.deepModelTy - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height1 with type k = k, @@ -3072,7 +2983,7 @@ module RedBlackTree_Impl14_RotateLeft type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, predicate HasMapping0.has_mapping = HasMapping1.has_mapping, predicate HasMapping1.has_mapping = HasMapping0.has_mapping - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl12_InternalInvariant as InternalInvariant0 with @@ -3107,12 +3018,12 @@ module RedBlackTree_Impl14_RotateLeft type self = Ghost.ghost_ty (borrowed (RedBlackTree_Node_Type.t_node k v)) let rec cfg rotate_left [#"../red_black_tree.rs" 462 4 462 29] [@cfg:stackify] [@cfg:subregion_analysis] (self : borrowed (RedBlackTree_Node_Type.t_node k v)) : () requires {[#"../red_black_tree.rs" 450 15 450 43] InternalInvariant0.internal_invariant ( * self)} - requires {[#"../red_black_tree.rs" 451 15 451 43] Color1.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Red} + requires {[#"../red_black_tree.rs" 451 15 451 43] Color0.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Red} ensures { [#"../red_black_tree.rs" 452 14 452 42] SameMappings0.same_mappings ( * self) ( ^ self) } ensures { [#"../red_black_tree.rs" 453 14 453 42] InternalInvariant0.internal_invariant ( ^ self) } ensures { [#"../red_black_tree.rs" 454 14 454 50] Height0.height ( * self) = Height0.height ( ^ self) } ensures { [#"../red_black_tree.rs" 455 14 455 65] LtLog0.lt_log (DeepModel0.deep_model (RedBlackTree_Node_Type.node_key ( * self))) (DeepModel0.deep_model (RedBlackTree_Node_Type.node_key ( ^ self))) } - ensures { [#"../red_black_tree.rs" 456 14 456 41] Color1.color (RedBlackTree_Node_Type.node_left ( ^ self)) = RedBlackTree_Color_Type.C_Red } + ensures { [#"../red_black_tree.rs" 456 14 456 41] Color0.color (RedBlackTree_Node_Type.node_left ( ^ self)) = RedBlackTree_Color_Type.C_Red } ensures { [#"../red_black_tree.rs" 457 14 457 44] RedBlackTree_Node_Type.node_color ( ^ self) = RedBlackTree_Node_Type.node_color ( * self) } ensures { [#"../red_black_tree.rs" 458 4 461 36] exists r : RedBlackTree_Node_Type.t_node k v . exists l : RedBlackTree_Node_Type.t_node k v . RedBlackTree_Tree_Type.tree_node (RedBlackTree_Node_Type.node_right ( * self)) = Core_Option_Option_Type.C_Some r /\ RedBlackTree_Tree_Type.tree_node (RedBlackTree_Node_Type.node_left ( ^ self)) = Core_Option_Option_Type.C_Some l /\ (RedBlackTree_Node_Type.node_left l, RedBlackTree_Node_Type.node_right l, RedBlackTree_Node_Type.node_right ( ^ self)) = (RedBlackTree_Node_Type.node_left ( * self), RedBlackTree_Node_Type.node_left r, RedBlackTree_Node_Type.node_right r) /\ RedBlackTree_Node_Type.node_key l = RedBlackTree_Node_Type.node_key ( * self) } @@ -3248,9 +3159,7 @@ module RedBlackTree_Impl14_FlipColors_Interface type v = v, axiom . use RedBlackTree_Color_Type as RedBlackTree_Color_Type - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone RedBlackTree_Impl1_SameMappings_Stub as SameMappings0 with type k = k, type v = v @@ -3339,11 +3248,9 @@ module RedBlackTree_Impl14_FlipColors clone CreusotContracts_Model_DeepModel_DeepModel_Interface as DeepModel0 with type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height1 with type k = k, @@ -3401,7 +3308,7 @@ module RedBlackTree_Impl14_FlipColors type v = v, function Height0.height = Height1.height, axiom . - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl12_InternalInvariant as InternalInvariant0 with @@ -3425,7 +3332,7 @@ module RedBlackTree_Impl14_FlipColors requires {[#"../red_black_tree.rs" 472 15 472 43] InternalInvariant0.internal_invariant ( * self)} requires {[#"../red_black_tree.rs" 473 15 473 40] RedBlackTree_Tree_Type.tree_node (RedBlackTree_Node_Type.node_left ( * self)) <> Core_Option_Option_Type.C_None} requires {[#"../red_black_tree.rs" 474 15 474 41] RedBlackTree_Tree_Type.tree_node (RedBlackTree_Node_Type.node_right ( * self)) <> Core_Option_Option_Type.C_None} - requires {[#"../red_black_tree.rs" 475 15 475 60] Color1.color (RedBlackTree_Node_Type.node_left ( * self)) = Color1.color (RedBlackTree_Node_Type.node_right ( * self))} + requires {[#"../red_black_tree.rs" 475 15 475 60] Color0.color (RedBlackTree_Node_Type.node_left ( * self)) = Color0.color (RedBlackTree_Node_Type.node_right ( * self))} ensures { [#"../red_black_tree.rs" 476 14 476 42] InternalInvariant0.internal_invariant ( ^ self) } ensures { [#"../red_black_tree.rs" 477 14 477 50] Height0.height ( * self) = Height0.height ( ^ self) } ensures { [#"../red_black_tree.rs" 478 14 478 42] SameMappings0.same_mappings ( * self) ( ^ self) } @@ -3507,14 +3414,12 @@ module RedBlackTree_Impl14_Balance_Interface type k type v use prelude.Borrow - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl9_Height_Stub as Height1 with type k = k, type v = v, axiom . + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Cp_Type as RedBlackTree_Cp_Type clone RedBlackTree_Impl6_MatchN_Stub as MatchN0 with @@ -3533,7 +3438,7 @@ module RedBlackTree_Impl14_Balance_Interface clone RedBlackTree_Impl7_ColorInvariant_Stub as ColorInvariant0 with type k = k, type v = v - clone RedBlackTree_Impl7_Color_Stub as Color1 with + clone RedBlackTree_Impl7_Color_Stub as Color0 with type k = k, type v = v clone RedBlackTree_Impl12_InternalInvariant_Stub as InternalInvariant0 with @@ -3541,13 +3446,13 @@ module RedBlackTree_Impl14_Balance_Interface type v = v val balance [#"../red_black_tree.rs" 510 4 510 25] (self : borrowed (RedBlackTree_Node_Type.t_node k v)) : () requires {[#"../red_black_tree.rs" 491 15 491 43] InternalInvariant0.internal_invariant ( * self)} - requires {[#"../red_black_tree.rs" 492 4 493 47] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color1.color (RedBlackTree_Node_Type.node_left ( * self)) = RedBlackTree_Color_Type.C_Red -> ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_left ( * self))} - requires {[#"../red_black_tree.rs" 494 4 495 48] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color1.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Red -> ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_right ( * self))} - requires {[#"../red_black_tree.rs" 496 4 496 110] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color1.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Red /\ Color1.color (RedBlackTree_Node_Type.node_left ( * self)) = RedBlackTree_Color_Type.C_Red -> false} + requires {[#"../red_black_tree.rs" 492 4 493 47] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color0.color (RedBlackTree_Node_Type.node_left ( * self)) = RedBlackTree_Color_Type.C_Red -> ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_left ( * self))} + requires {[#"../red_black_tree.rs" 494 4 495 48] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color0.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Red -> ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_right ( * self))} + requires {[#"../red_black_tree.rs" 496 4 496 110] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color0.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Red /\ Color0.color (RedBlackTree_Node_Type.node_left ( * self)) = RedBlackTree_Color_Type.C_Red -> false} ensures { [#"../red_black_tree.rs" 497 14 497 42] SameMappings0.same_mappings ( * self) ( ^ self) } ensures { [#"../red_black_tree.rs" 498 14 498 42] InternalInvariant0.internal_invariant ( ^ self) } ensures { [#"../red_black_tree.rs" 499 14 499 50] Height0.height ( * self) = Height0.height ( ^ self) } - ensures { [#"../red_black_tree.rs" 500 4 501 34] ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_left ( * self)) /\ Color1.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Black -> * self = ^ self } + ensures { [#"../red_black_tree.rs" 500 4 501 34] ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_left ( * self)) /\ Color0.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Black -> * self = ^ self } ensures { [#"../red_black_tree.rs" 502 4 503 39] MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (Cpn0.cpn (RedBlackTree_Color_Type.C_Red) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( * self) -> MatchN0.match_n (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) ( ^ self) } ensures { [#"../red_black_tree.rs" 504 4 505 63] MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red))) ( * self) -> MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( ^ self) } ensures { [#"../red_black_tree.rs" 506 4 507 61] MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Red) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red))) ( * self) -> MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Red) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( ^ self) } @@ -3569,11 +3474,9 @@ module RedBlackTree_Impl14_Balance type self = DeepModelTy0.deepModelTy clone CreusotContracts_Logic_Ord_OrdLogic_LeLog_Interface as LeLog0 with type self = DeepModelTy0.deepModelTy - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height1 with type k = k, @@ -3648,13 +3551,13 @@ module RedBlackTree_Impl14_Balance predicate LeLog0.le_log = LeLog0.le_log, function CmpLog0.cmp_log = CmpLog0.cmp_log, axiom . - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone RedBlackTree_Impl7_ColorInvariant as ColorInvariant0 with type k = k, type v = v, @@ -3663,7 +3566,7 @@ module RedBlackTree_Impl14_Balance clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant clone RedBlackTree_Impl8_ColorInvariant as ColorInvariant1 with type k = k, @@ -3715,7 +3618,7 @@ module RedBlackTree_Impl14_Balance type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, - function Color0.color = Color1.color, + function Color0.color = Color0.color, function Height0.height = Height0.height, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height1.height = Height1.height @@ -3723,7 +3626,7 @@ module RedBlackTree_Impl14_Balance type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height0.height, function DeepModel0.deep_model = DeepModel0.deep_model, @@ -3740,7 +3643,7 @@ module RedBlackTree_Impl14_Balance type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height0.height, function DeepModel0.deep_model = DeepModel0.deep_model, @@ -3750,16 +3653,16 @@ module RedBlackTree_Impl14_Balance clone RedBlackTree_Impl13_IsRed_Interface as IsRed0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color let rec cfg balance [#"../red_black_tree.rs" 510 4 510 25] [@cfg:stackify] [@cfg:subregion_analysis] (self : borrowed (RedBlackTree_Node_Type.t_node k v)) : () requires {[#"../red_black_tree.rs" 491 15 491 43] InternalInvariant0.internal_invariant ( * self)} - requires {[#"../red_black_tree.rs" 492 4 493 47] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color1.color (RedBlackTree_Node_Type.node_left ( * self)) = RedBlackTree_Color_Type.C_Red -> ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_left ( * self))} - requires {[#"../red_black_tree.rs" 494 4 495 48] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color1.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Red -> ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_right ( * self))} - requires {[#"../red_black_tree.rs" 496 4 496 110] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color1.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Red /\ Color1.color (RedBlackTree_Node_Type.node_left ( * self)) = RedBlackTree_Color_Type.C_Red -> false} + requires {[#"../red_black_tree.rs" 492 4 493 47] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color0.color (RedBlackTree_Node_Type.node_left ( * self)) = RedBlackTree_Color_Type.C_Red -> ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_left ( * self))} + requires {[#"../red_black_tree.rs" 494 4 495 48] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color0.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Red -> ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_right ( * self))} + requires {[#"../red_black_tree.rs" 496 4 496 110] RedBlackTree_Node_Type.node_color ( * self) = RedBlackTree_Color_Type.C_Red /\ Color0.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Red /\ Color0.color (RedBlackTree_Node_Type.node_left ( * self)) = RedBlackTree_Color_Type.C_Red -> false} ensures { [#"../red_black_tree.rs" 497 14 497 42] SameMappings0.same_mappings ( * self) ( ^ self) } ensures { [#"../red_black_tree.rs" 498 14 498 42] InternalInvariant0.internal_invariant ( ^ self) } ensures { [#"../red_black_tree.rs" 499 14 499 50] Height0.height ( * self) = Height0.height ( ^ self) } - ensures { [#"../red_black_tree.rs" 500 4 501 34] ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_left ( * self)) /\ Color1.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Black -> * self = ^ self } + ensures { [#"../red_black_tree.rs" 500 4 501 34] ColorInvariant0.color_invariant (RedBlackTree_Node_Type.node_left ( * self)) /\ Color0.color (RedBlackTree_Node_Type.node_right ( * self)) = RedBlackTree_Color_Type.C_Black -> * self = ^ self } ensures { [#"../red_black_tree.rs" 502 4 503 39] MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (Cpn0.cpn (RedBlackTree_Color_Type.C_Red) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( * self) -> MatchN0.match_n (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) ( ^ self) } ensures { [#"../red_black_tree.rs" 504 4 505 63] MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red))) ( * self) -> MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( ^ self) } ensures { [#"../red_black_tree.rs" 506 4 507 61] MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Red) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red))) ( * self) -> MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Red) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( ^ self) } @@ -3936,13 +3839,11 @@ module RedBlackTree_Impl14_MoveRedLeft_Interface type k = k, type v = v, axiom . - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type - clone RedBlackTree_Impl7_Color_Stub as Color1 with + clone RedBlackTree_Impl7_Color_Stub as Color0 with type k = k, type v = v + use RedBlackTree_Node_Type as RedBlackTree_Node_Type clone RedBlackTree_Impl8_ColorInvariant_Stub as ColorInvariant0 with type k = k, type v = v @@ -3983,7 +3884,7 @@ module RedBlackTree_Impl14_MoveRedLeft_Interface ensures { [#"../red_black_tree.rs" 534 4 535 47] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( * self) k v /\ LeLog0.le_log k (DeepModel0.deep_model (RedBlackTree_Node_Type.node_key ( * self))) -> HasMapping0.has_mapping ( * result) k v } ensures { [#"../red_black_tree.rs" 536 4 537 108] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( ^ self) k v = (HasMapping0.has_mapping ( ^ result) k v \/ HasMapping0.has_mapping ( * self) k v /\ not HasMapping0.has_mapping ( * result) k v) } ensures { [#"../red_black_tree.rs" 538 14 539 61] MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( * result) \/ MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red))) ( * result) } - ensures { [#"../red_black_tree.rs" 540 4 541 45] ColorInvariant0.color_invariant ( ^ result) /\ (Color1.color (RedBlackTree_Node_Type.node_right ( * result)) = RedBlackTree_Color_Type.C_Black -> RedBlackTree_Node_Type.node_color ( ^ result) = RedBlackTree_Color_Type.C_Black) -> ColorInvariant0.color_invariant ( ^ self) } + ensures { [#"../red_black_tree.rs" 540 4 541 45] ColorInvariant0.color_invariant ( ^ result) /\ (Color0.color (RedBlackTree_Node_Type.node_right ( * result)) = RedBlackTree_Color_Type.C_Black -> RedBlackTree_Node_Type.node_color ( ^ result) = RedBlackTree_Color_Type.C_Black) -> ColorInvariant0.color_invariant ( ^ self) } end module RedBlackTree_Impl14_MoveRedLeft @@ -3999,11 +3900,9 @@ module RedBlackTree_Impl14_MoveRedLeft use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type clone CreusotContracts_Logic_Ord_OrdLogic_CmpLog_Interface as CmpLog0 with type self = DeepModelTy0.deepModelTy - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height1 with type k = k, @@ -4038,13 +3937,13 @@ module RedBlackTree_Impl14_MoveRedLeft type k = k, type v = v, predicate BstInvariantHere0.bst_invariant_here = BstInvariantHere0.bst_invariant_here - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone RedBlackTree_Impl7_ColorInvariant as ColorInvariant1 with type k = k, type v = v, @@ -4095,7 +3994,7 @@ module RedBlackTree_Impl14_MoveRedLeft clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant1.color_invariant clone RedBlackTree_Impl10_HeightInvariant as HeightInvariant0 with type k = k, @@ -4147,7 +4046,7 @@ module RedBlackTree_Impl14_MoveRedLeft type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height0.height, function DeepModel0.deep_model = DeepModel0.deep_model, @@ -4158,7 +4057,7 @@ module RedBlackTree_Impl14_MoveRedLeft type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height0.height, function DeepModel0.deep_model = DeepModel0.deep_model, @@ -4168,7 +4067,7 @@ module RedBlackTree_Impl14_MoveRedLeft clone RedBlackTree_Impl13_IsRed_Interface as IsRed0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with type t = RedBlackTree_Node_Type.t_node k v clone Core_Option_Impl0_Unwrap_Interface as Unwrap0 with @@ -4179,7 +4078,7 @@ module RedBlackTree_Impl14_MoveRedLeft type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, - function Color0.color = Color1.color, + function Color0.color = Color0.color, function Height0.height = Height0.height, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height1.height = Height1.height @@ -4195,7 +4094,7 @@ module RedBlackTree_Impl14_MoveRedLeft ensures { [#"../red_black_tree.rs" 534 4 535 47] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( * self) k v /\ LeLog0.le_log k (DeepModel0.deep_model (RedBlackTree_Node_Type.node_key ( * self))) -> HasMapping0.has_mapping ( * result) k v } ensures { [#"../red_black_tree.rs" 536 4 537 108] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( ^ self) k v = (HasMapping0.has_mapping ( ^ result) k v \/ HasMapping0.has_mapping ( * self) k v /\ not HasMapping0.has_mapping ( * result) k v) } ensures { [#"../red_black_tree.rs" 538 14 539 61] MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( * result) \/ MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red))) ( * result) } - ensures { [#"../red_black_tree.rs" 540 4 541 45] ColorInvariant0.color_invariant ( ^ result) /\ (Color1.color (RedBlackTree_Node_Type.node_right ( * result)) = RedBlackTree_Color_Type.C_Black -> RedBlackTree_Node_Type.node_color ( ^ result) = RedBlackTree_Color_Type.C_Black) -> ColorInvariant0.color_invariant ( ^ self) } + ensures { [#"../red_black_tree.rs" 540 4 541 45] ColorInvariant0.color_invariant ( ^ result) /\ (Color0.color (RedBlackTree_Node_Type.node_right ( * result)) = RedBlackTree_Color_Type.C_Black -> RedBlackTree_Node_Type.node_color ( ^ result) = RedBlackTree_Color_Type.C_Black) -> ColorInvariant0.color_invariant ( ^ self) } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : borrowed (RedBlackTree_Node_Type.t_node k v); @@ -4321,13 +4220,11 @@ module RedBlackTree_Impl14_MoveRedRight_Interface type k = k, type v = v, axiom . - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type - clone RedBlackTree_Impl7_Color_Stub as Color1 with + clone RedBlackTree_Impl7_Color_Stub as Color0 with type k = k, type v = v + use RedBlackTree_Node_Type as RedBlackTree_Node_Type clone RedBlackTree_Impl8_ColorInvariant_Stub as ColorInvariant0 with type k = k, type v = v @@ -4368,7 +4265,7 @@ module RedBlackTree_Impl14_MoveRedRight_Interface ensures { [#"../red_black_tree.rs" 563 4 564 47] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( * self) k v /\ LeLog0.le_log (DeepModel0.deep_model (RedBlackTree_Node_Type.node_key ( * self))) k -> HasMapping0.has_mapping ( * result) k v } ensures { [#"../red_black_tree.rs" 565 4 566 108] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( ^ self) k v = (HasMapping0.has_mapping ( ^ result) k v \/ HasMapping0.has_mapping ( * self) k v /\ not HasMapping0.has_mapping ( * result) k v) } ensures { [#"../red_black_tree.rs" 567 14 568 61] MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red))) ( * result) \/ MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red))) ( * result) } - ensures { [#"../red_black_tree.rs" 569 4 570 45] ColorInvariant0.color_invariant ( ^ result) /\ (Color1.color (RedBlackTree_Node_Type.node_left ( * result)) = RedBlackTree_Color_Type.C_Black -> RedBlackTree_Node_Type.node_color ( ^ result) = RedBlackTree_Color_Type.C_Black) -> ColorInvariant0.color_invariant ( ^ self) } + ensures { [#"../red_black_tree.rs" 569 4 570 45] ColorInvariant0.color_invariant ( ^ result) /\ (Color0.color (RedBlackTree_Node_Type.node_left ( * result)) = RedBlackTree_Color_Type.C_Black -> RedBlackTree_Node_Type.node_color ( ^ result) = RedBlackTree_Color_Type.C_Black) -> ColorInvariant0.color_invariant ( ^ self) } end module RedBlackTree_Impl14_MoveRedRight @@ -4384,11 +4281,9 @@ module RedBlackTree_Impl14_MoveRedRight use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type clone CreusotContracts_Logic_Ord_OrdLogic_CmpLog_Interface as CmpLog0 with type self = DeepModelTy0.deepModelTy - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height1 with type k = k, @@ -4423,13 +4318,13 @@ module RedBlackTree_Impl14_MoveRedRight type k = k, type v = v, predicate BstInvariantHere0.bst_invariant_here = BstInvariantHere0.bst_invariant_here - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone RedBlackTree_Impl7_ColorInvariant as ColorInvariant1 with type k = k, type v = v, @@ -4480,7 +4375,7 @@ module RedBlackTree_Impl14_MoveRedRight clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant1.color_invariant clone RedBlackTree_Impl10_HeightInvariant as HeightInvariant0 with type k = k, @@ -4532,7 +4427,7 @@ module RedBlackTree_Impl14_MoveRedRight type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height0.height, function DeepModel0.deep_model = DeepModel0.deep_model, @@ -4542,7 +4437,7 @@ module RedBlackTree_Impl14_MoveRedRight clone RedBlackTree_Impl13_IsRed_Interface as IsRed0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with type t = RedBlackTree_Node_Type.t_node k v clone Core_Option_Impl0_Unwrap_Interface as Unwrap0 with @@ -4553,7 +4448,7 @@ module RedBlackTree_Impl14_MoveRedRight type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, - function Color0.color = Color1.color, + function Color0.color = Color0.color, function Height0.height = Height0.height, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height1.height = Height1.height @@ -4569,7 +4464,7 @@ module RedBlackTree_Impl14_MoveRedRight ensures { [#"../red_black_tree.rs" 563 4 564 47] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( * self) k v /\ LeLog0.le_log (DeepModel0.deep_model (RedBlackTree_Node_Type.node_key ( * self))) k -> HasMapping0.has_mapping ( * result) k v } ensures { [#"../red_black_tree.rs" 565 4 566 108] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( ^ self) k v = (HasMapping0.has_mapping ( ^ result) k v \/ HasMapping0.has_mapping ( * self) k v /\ not HasMapping0.has_mapping ( * result) k v) } ensures { [#"../red_black_tree.rs" 567 14 568 61] MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red))) ( * result) \/ MatchN0.match_n (Cpn0.cpn (RedBlackTree_Color_Type.C_Black) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red))) ( * result) } - ensures { [#"../red_black_tree.rs" 569 4 570 45] ColorInvariant0.color_invariant ( ^ result) /\ (Color1.color (RedBlackTree_Node_Type.node_left ( * result)) = RedBlackTree_Color_Type.C_Black -> RedBlackTree_Node_Type.node_color ( ^ result) = RedBlackTree_Color_Type.C_Black) -> ColorInvariant0.color_invariant ( ^ self) } + ensures { [#"../red_black_tree.rs" 569 4 570 45] ColorInvariant0.color_invariant ( ^ result) /\ (Color0.color (RedBlackTree_Node_Type.node_left ( * result)) = RedBlackTree_Color_Type.C_Black -> RedBlackTree_Node_Type.node_color ( ^ result) = RedBlackTree_Color_Type.C_Black) -> ColorInvariant0.color_invariant ( ^ self) } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : borrowed (RedBlackTree_Node_Type.t_node k v); @@ -4735,10 +4630,8 @@ module RedBlackTree_Impl15_New predicate LeLog0.le_log = LeLog0.le_log, function CmpLog0.cmp_log = CmpLog0.cmp_log, axiom . - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl9_Height as Height0 with @@ -4852,7 +4745,7 @@ module RedBlackTree_Impl15_InsertRec_Interface type self = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy use RedBlackTree_Color_Type as RedBlackTree_Color_Type - clone RedBlackTree_Impl7_Color_Stub as Color1 with + clone RedBlackTree_Impl7_Color_Stub as Color0 with type k = k, type v = v use RedBlackTree_Cp_Type as RedBlackTree_Cp_Type @@ -4875,7 +4768,7 @@ module RedBlackTree_Impl15_InsertRec_Interface requires {[#"../red_black_tree.rs" 593 15 593 40] ColorInvariant0.color_invariant ( * self)} ensures { [#"../red_black_tree.rs" 594 14 594 42] InternalInvariant0.internal_invariant ( ^ self) } ensures { [#"../red_black_tree.rs" 595 14 595 50] Height0.height ( * self) = Height0.height ( ^ self) } - ensures { [#"../red_black_tree.rs" 596 14 597 39] MatchT0.match_t (Cpn0.cpn (RedBlackTree_Color_Type.C_Red) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( ^ self) /\ Color1.color ( * self) = RedBlackTree_Color_Type.C_Red \/ ColorInvariant0.color_invariant ( ^ self) } + ensures { [#"../red_black_tree.rs" 596 14 597 39] MatchT0.match_t (Cpn0.cpn (RedBlackTree_Color_Type.C_Red) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( ^ self) /\ Color0.color ( * self) = RedBlackTree_Color_Type.C_Red \/ ColorInvariant0.color_invariant ( ^ self) } ensures { [#"../red_black_tree.rs" 598 14 598 56] HasMapping0.has_mapping ( ^ self) (DeepModel0.deep_model key) val' } ensures { [#"../red_black_tree.rs" 599 4 599 127] forall v : v . forall k : DeepModelTy0.deepModelTy . k = DeepModel0.deep_model key \/ HasMapping0.has_mapping ( * self) k v = HasMapping0.has_mapping ( ^ self) k v } @@ -4895,10 +4788,8 @@ module RedBlackTree_Impl15_InsertRec clone CreusotContracts_Logic_Ord_OrdLogic_LeLog_Interface as LeLog0 with type self = DeepModelTy0.deepModelTy use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height0 with type k = k, @@ -4923,13 +4814,13 @@ module RedBlackTree_Impl15_InsertRec predicate HasMapping0.has_mapping = HasMapping0.has_mapping, function DeepModel0.deep_model = DeepModel0.deep_model, predicate LtLog0.lt_log = LtLog0.lt_log - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone RedBlackTree_Impl7_ColorInvariant as ColorInvariant0 with type k = k, type v = v, @@ -5011,7 +4902,7 @@ module RedBlackTree_Impl15_InsertRec clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant clone RedBlackTree_Impl6_MatchN as MatchN0 with type k = k, @@ -5044,7 +4935,7 @@ module RedBlackTree_Impl15_InsertRec type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant1.internal_invariant, - function Color1.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height1.height, @@ -5075,7 +4966,7 @@ module RedBlackTree_Impl15_InsertRec requires {[#"../red_black_tree.rs" 593 15 593 40] ColorInvariant0.color_invariant ( * self)} ensures { [#"../red_black_tree.rs" 594 14 594 42] InternalInvariant0.internal_invariant ( ^ self) } ensures { [#"../red_black_tree.rs" 595 14 595 50] Height0.height ( * self) = Height0.height ( ^ self) } - ensures { [#"../red_black_tree.rs" 596 14 597 39] MatchT0.match_t (Cpn0.cpn (RedBlackTree_Color_Type.C_Red) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( ^ self) /\ Color1.color ( * self) = RedBlackTree_Color_Type.C_Red \/ ColorInvariant0.color_invariant ( ^ self) } + ensures { [#"../red_black_tree.rs" 596 14 597 39] MatchT0.match_t (Cpn0.cpn (RedBlackTree_Color_Type.C_Red) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Red)) (RedBlackTree_Cp_Type.C_CPL (RedBlackTree_Color_Type.C_Black))) ( ^ self) /\ Color0.color ( * self) = RedBlackTree_Color_Type.C_Red \/ ColorInvariant0.color_invariant ( ^ self) } ensures { [#"../red_black_tree.rs" 598 14 598 56] HasMapping0.has_mapping ( ^ self) (DeepModel0.deep_model key) val' } ensures { [#"../red_black_tree.rs" 599 4 599 127] forall v : v . forall k : DeepModelTy0.deepModelTy . k = DeepModel0.deep_model key \/ HasMapping0.has_mapping ( * self) k v = HasMapping0.has_mapping ( ^ self) k v } @@ -5313,9 +5204,9 @@ module RedBlackTree_Impl15_Insert_Interface type v use prelude.Borrow use map.Map + use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k - use Core_Option_Option_Type as Core_Option_Option_Type use map.Map use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with @@ -5397,10 +5288,8 @@ module RedBlackTree_Impl15_Insert function CmpLog0.cmp_log = CmpLog0.cmp_log, axiom . use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height0 with type k = k, @@ -5425,13 +5314,13 @@ module RedBlackTree_Impl15_Insert predicate HasMapping0.has_mapping = HasMapping0.has_mapping, function DeepModel0.deep_model = DeepModel0.deep_model, predicate LtLog0.lt_log = LtLog0.lt_log - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone RedBlackTree_Impl9_HeightInvariant as HeightInvariant0 with type k = k, type v = v, @@ -5473,7 +5362,7 @@ module RedBlackTree_Impl15_Insert clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant clone RedBlackTree_Cpn as Cpn0 clone RedBlackTree_Impl11_InternalInvariant as InternalInvariant0 with @@ -5495,7 +5384,7 @@ module RedBlackTree_Impl15_Insert type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve2 with type self = Ghost.ghost_ty () clone RedBlackTree_Impl0_HasMappingModel as HasMappingModel0 with @@ -5525,7 +5414,7 @@ module RedBlackTree_Impl15_Insert function Height0.height = Height0.height, function Cpn0.cpn = Cpn0.cpn, predicate MatchT0.match_t = MatchT0.match_t, - function Color1.color = Color1.color, + function Color0.color = Color0.color, function DeepModel0.deep_model = DeepModel0.deep_model, predicate HasMapping0.has_mapping = HasMapping0.has_mapping, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy @@ -5597,6 +5486,11 @@ module Alloc_Boxed_Impl57_AsMut_Interface ensures { [#"../../../../creusot-contracts/src/std/boxed.rs" 33 26 33 43] * self = * result } ensures { [#"../../../../creusot-contracts/src/std/boxed.rs" 34 26 34 43] ^ self = ^ result } +end +module Alloc_Alloc_Global_Type + type t_global = + | C_Global + end module RedBlackTree_Impl15_DeleteMaxRec_Interface type k @@ -5604,7 +5498,7 @@ module RedBlackTree_Impl15_DeleteMaxRec_Interface use prelude.Borrow use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type - clone RedBlackTree_Impl7_Color_Stub as Color1 with + clone RedBlackTree_Impl7_Color_Stub as Color0 with type k = k, type v = v clone RedBlackTree_Impl7_ColorInvariant_Stub as ColorInvariant0 with @@ -5642,7 +5536,7 @@ module RedBlackTree_Impl15_DeleteMaxRec_Interface ensures { [#"../red_black_tree.rs" 638 4 638 104] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( * self) k v -> LeLog0.le_log k (DeepModel0.deep_model (let (a, _) = result in a)) } ensures { [#"../red_black_tree.rs" 639 4 640 73] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( ^ self) k v = (DeepModel0.deep_model (let (a, _) = result in a) <> k /\ HasMapping0.has_mapping ( * self) k v) } ensures { [#"../red_black_tree.rs" 641 14 641 39] ColorInvariant0.color_invariant ( ^ self) } - ensures { [#"../red_black_tree.rs" 642 4 642 69] Color1.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color1.color ( ^ self) = RedBlackTree_Color_Type.C_Black } + ensures { [#"../red_black_tree.rs" 642 4 642 69] Color0.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color0.color ( ^ self) = RedBlackTree_Color_Type.C_Black } end module RedBlackTree_Impl15_DeleteMaxRec @@ -5659,10 +5553,8 @@ module RedBlackTree_Impl15_DeleteMaxRec clone CreusotContracts_Logic_Ord_OrdLogic_CmpLog_Interface as CmpLog0 with type self = DeepModelTy0.deepModelTy use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height0 with type k = k, @@ -5707,13 +5599,13 @@ module RedBlackTree_Impl15_DeleteMaxRec type v = v, predicate BstInvariantHere0.bst_invariant_here = BstInvariantHere0.bst_invariant_here, predicate BstInvariant0.bst_invariant = BstInvariant0.bst_invariant - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Logic_Ord_OrdLogic_EqCmp_Interface as EqCmp0 with type self = DeepModelTy0.deepModelTy, function CmpLog0.cmp_log = CmpLog0.cmp_log, @@ -5778,7 +5670,7 @@ module RedBlackTree_Impl15_DeleteMaxRec clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant clone RedBlackTree_Impl6_MatchN as MatchN0 with type k = k, @@ -5801,6 +5693,7 @@ module RedBlackTree_Impl15_DeleteMaxRec type v = v, predicate BstInvariant0.bst_invariant = BstInvariant1.bst_invariant, predicate HeightInvariant0.height_invariant = HeightInvariant1.height_invariant + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type clone RedBlackTree_Cpn as Cpn0 clone RedBlackTree_Impl11_InternalInvariant as InternalInvariant0 with type k = k, @@ -5822,7 +5715,7 @@ module RedBlackTree_Impl15_DeleteMaxRec type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant1.internal_invariant, - function Color1.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height1.height, @@ -5843,7 +5736,7 @@ module RedBlackTree_Impl15_DeleteMaxRec function DeepModel0.deep_model = DeepModel0.deep_model, predicate LeLog0.le_log = LeLog0.le_log, predicate ColorInvariant0.color_invariant = ColorInvariant1.color_invariant, - function Color1.color = Color1.color, + function Color0.color = Color0.color, function Height1.height = Height0.height, predicate HasMapping1.has_mapping = HasMapping0.has_mapping clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with @@ -5856,7 +5749,7 @@ module RedBlackTree_Impl15_DeleteMaxRec type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant1.internal_invariant, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height1.height, function DeepModel0.deep_model = DeepModel0.deep_model, @@ -5866,7 +5759,7 @@ module RedBlackTree_Impl15_DeleteMaxRec clone RedBlackTree_Impl13_IsRed_Interface as IsRed0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with type t = RedBlackTree_Node_Type.t_node k v clone Alloc_Boxed_Impl57_AsMut_Interface as AsMut1 with @@ -5885,7 +5778,7 @@ module RedBlackTree_Impl15_DeleteMaxRec ensures { [#"../red_black_tree.rs" 638 4 638 104] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( * self) k v -> LeLog0.le_log k (DeepModel0.deep_model (let (a, _) = result in a)) } ensures { [#"../red_black_tree.rs" 639 4 640 73] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( ^ self) k v = (DeepModel0.deep_model (let (a, _) = result in a) <> k /\ HasMapping0.has_mapping ( * self) k v) } ensures { [#"../red_black_tree.rs" 641 14 641 39] ColorInvariant0.color_invariant ( ^ self) } - ensures { [#"../red_black_tree.rs" 642 4 642 69] Color1.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color1.color ( ^ self) = RedBlackTree_Color_Type.C_Black } + ensures { [#"../red_black_tree.rs" 642 4 642 69] Color0.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color0.color ( ^ self) = RedBlackTree_Color_Type.C_Black } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : (k, v); @@ -6083,9 +5976,9 @@ module RedBlackTree_Impl15_DeleteMax_Interface use prelude.Borrow use map.Map use map.Const + use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k - use Core_Option_Option_Type as Core_Option_Option_Type use map.Map use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl3_ShallowModel_Stub as ShallowModel1 with @@ -6120,10 +6013,8 @@ module RedBlackTree_Impl15_DeleteMax use map.Map use map.Const use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height0 with type k = k, @@ -6159,13 +6050,13 @@ module RedBlackTree_Impl15_DeleteMax predicate HasMapping0.has_mapping = HasMapping0.has_mapping, function DeepModel0.deep_model = DeepModel0.deep_model, predicate LtLog0.lt_log = LtLog0.lt_log - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone RedBlackTree_Impl9_HeightInvariant as HeightInvariant0 with type k = k, type v = v, @@ -6250,7 +6141,7 @@ module RedBlackTree_Impl15_DeleteMax clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant clone RedBlackTree_Impl11_InternalInvariant as InternalInvariant0 with type k = k, @@ -6271,7 +6162,7 @@ module RedBlackTree_Impl15_DeleteMax type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve4 with type self = Ghost.ghost_ty () clone RedBlackTree_Impl0_HasMappingModel as HasMappingModel0 with @@ -6301,7 +6192,7 @@ module RedBlackTree_Impl15_DeleteMax type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, predicate LeLog0.le_log = LeLog0.le_log, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, - function Color1.color = Color1.color + function Color0.color = Color0.color clone RedBlackTree_Impl0_SameMappings as SameMappings0 with type k = k, type v = v, @@ -6312,7 +6203,7 @@ module RedBlackTree_Impl15_DeleteMax clone RedBlackTree_Impl13_IsRed_Interface as IsRed0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with type t = RedBlackTree_Tree_Type.t_tree k v clone CreusotContracts_Resolve_Impl1_Resolve as Resolve1 with @@ -6455,7 +6346,7 @@ module RedBlackTree_Impl15_DeleteMinRec_Interface use prelude.Borrow use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type - clone RedBlackTree_Impl7_Color_Stub as Color1 with + clone RedBlackTree_Impl7_Color_Stub as Color0 with type k = k, type v = v clone RedBlackTree_Impl7_ColorInvariant_Stub as ColorInvariant0 with @@ -6493,7 +6384,7 @@ module RedBlackTree_Impl15_DeleteMinRec_Interface ensures { [#"../red_black_tree.rs" 691 4 691 104] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( * self) k v -> LeLog0.le_log (DeepModel0.deep_model (let (a, _) = result in a)) k } ensures { [#"../red_black_tree.rs" 692 4 693 73] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( ^ self) k v = (DeepModel0.deep_model (let (a, _) = result in a) <> k /\ HasMapping0.has_mapping ( * self) k v) } ensures { [#"../red_black_tree.rs" 694 14 694 39] ColorInvariant0.color_invariant ( ^ self) } - ensures { [#"../red_black_tree.rs" 695 4 695 69] Color1.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color1.color ( ^ self) = RedBlackTree_Color_Type.C_Black } + ensures { [#"../red_black_tree.rs" 695 4 695 69] Color0.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color0.color ( ^ self) = RedBlackTree_Color_Type.C_Black } end module RedBlackTree_Impl15_DeleteMinRec @@ -6512,10 +6403,8 @@ module RedBlackTree_Impl15_DeleteMinRec clone CreusotContracts_Logic_Ord_OrdLogic_CmpLog_Interface as CmpLog0 with type self = DeepModelTy0.deepModelTy use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height0 with type k = k, @@ -6558,13 +6447,13 @@ module RedBlackTree_Impl15_DeleteMinRec type v = v, predicate BstInvariantHere0.bst_invariant_here = BstInvariantHere0.bst_invariant_here, predicate BstInvariant0.bst_invariant = BstInvariant0.bst_invariant - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Logic_Ord_OrdLogic_EqCmp_Interface as EqCmp0 with type self = DeepModelTy0.deepModelTy, function CmpLog0.cmp_log = CmpLog0.cmp_log, @@ -6640,7 +6529,7 @@ module RedBlackTree_Impl15_DeleteMinRec clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant clone RedBlackTree_Impl6_MatchN as MatchN0 with type k = k, @@ -6652,6 +6541,7 @@ module RedBlackTree_Impl15_DeleteMinRec type v = v, predicate BstInvariant0.bst_invariant = BstInvariant1.bst_invariant, predicate HeightInvariant0.height_invariant = HeightInvariant1.height_invariant + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type clone RedBlackTree_Cpn as Cpn0 clone RedBlackTree_Impl11_InternalInvariant as InternalInvariant0 with type k = k, @@ -6673,7 +6563,7 @@ module RedBlackTree_Impl15_DeleteMinRec type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant1.internal_invariant, - function Color1.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height1.height, @@ -6694,7 +6584,7 @@ module RedBlackTree_Impl15_DeleteMinRec function DeepModel0.deep_model = DeepModel0.deep_model, predicate LeLog0.le_log = LeLog0.le_log, predicate ColorInvariant0.color_invariant = ColorInvariant1.color_invariant, - function Color1.color = Color1.color, + function Color0.color = Color0.color, function Height1.height = Height0.height, predicate HasMapping1.has_mapping = HasMapping0.has_mapping clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with @@ -6706,7 +6596,7 @@ module RedBlackTree_Impl15_DeleteMinRec clone RedBlackTree_Impl13_IsRed_Interface as IsRed0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with type t = RedBlackTree_Node_Type.t_node k v clone Alloc_Boxed_Impl57_AsMut_Interface as AsMut1 with @@ -6725,7 +6615,7 @@ module RedBlackTree_Impl15_DeleteMinRec ensures { [#"../red_black_tree.rs" 691 4 691 104] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( * self) k v -> LeLog0.le_log (DeepModel0.deep_model (let (a, _) = result in a)) k } ensures { [#"../red_black_tree.rs" 692 4 693 73] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( ^ self) k v = (DeepModel0.deep_model (let (a, _) = result in a) <> k /\ HasMapping0.has_mapping ( * self) k v) } ensures { [#"../red_black_tree.rs" 694 14 694 39] ColorInvariant0.color_invariant ( ^ self) } - ensures { [#"../red_black_tree.rs" 695 4 695 69] Color1.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color1.color ( ^ self) = RedBlackTree_Color_Type.C_Black } + ensures { [#"../red_black_tree.rs" 695 4 695 69] Color0.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color0.color ( ^ self) = RedBlackTree_Color_Type.C_Black } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : (k, v); @@ -6898,9 +6788,9 @@ module RedBlackTree_Impl15_DeleteMin_Interface use prelude.Borrow use map.Map use map.Const + use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k - use Core_Option_Option_Type as Core_Option_Option_Type use map.Map use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl3_ShallowModel_Stub as ShallowModel1 with @@ -6935,10 +6825,8 @@ module RedBlackTree_Impl15_DeleteMin use map.Map use map.Const use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height0 with type k = k, @@ -6959,13 +6847,13 @@ module RedBlackTree_Impl15_DeleteMin use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type clone CreusotContracts_Logic_Ord_OrdLogic_CmpLog_Interface as CmpLog0 with type self = DeepModelTy0.deepModelTy - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone RedBlackTree_Impl9_HeightInvariant as HeightInvariant0 with type k = k, type v = v, @@ -7037,7 +6925,7 @@ module RedBlackTree_Impl15_DeleteMin clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant clone RedBlackTree_Impl5_BstInvariant as BstInvariant0 with type k = k, @@ -7086,7 +6974,7 @@ module RedBlackTree_Impl15_DeleteMin type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, - function Color0.color = Color1.color + function Color0.color = Color0.color clone Core_Option_Impl0_Unwrap_Interface as Unwrap0 with type t = borrowed (RedBlackTree_Node_Type.t_node k v) clone Core_Option_Impl0_AsMut_Interface as AsMut0 with @@ -7103,13 +6991,13 @@ module RedBlackTree_Impl15_DeleteMin type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, predicate LeLog0.le_log = LeLog0.le_log, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, - function Color1.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Impl1_Resolve as Resolve3 with type t = RedBlackTree_Node_Type.t_node k v clone RedBlackTree_Impl13_IsRed_Interface as IsRed0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with type t = RedBlackTree_Tree_Type.t_tree k v clone CreusotContracts_Resolve_Impl1_Resolve as Resolve1 with @@ -7295,7 +7183,7 @@ module RedBlackTree_Impl15_DeleteRec_Interface use prelude.Borrow use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type - clone RedBlackTree_Impl7_Color_Stub as Color1 with + clone RedBlackTree_Impl7_Color_Stub as Color0 with type k = k, type v = v clone RedBlackTree_Impl7_ColorInvariant_Stub as ColorInvariant0 with @@ -7337,7 +7225,7 @@ module RedBlackTree_Impl15_DeleteRec_Interface end } ensures { [#"../red_black_tree.rs" 745 4 745 129] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( ^ self) k v = (DeepModel0.deep_model key <> k /\ HasMapping0.has_mapping ( * self) k v) } ensures { [#"../red_black_tree.rs" 746 14 746 39] ColorInvariant0.color_invariant ( ^ self) } - ensures { [#"../red_black_tree.rs" 747 4 747 69] Color1.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color1.color ( ^ self) = RedBlackTree_Color_Type.C_Black } + ensures { [#"../red_black_tree.rs" 747 4 747 69] Color0.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color0.color ( ^ self) = RedBlackTree_Color_Type.C_Black } end module RedBlackTree_Impl15_DeleteRec @@ -7352,10 +7240,8 @@ module RedBlackTree_Impl15_DeleteRec clone CreusotContracts_Logic_Ord_OrdLogic_GeLog_Interface as GeLog0 with type self = DeepModelTy0.deepModelTy use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height0 with type k = k, @@ -7468,13 +7354,13 @@ module RedBlackTree_Impl15_DeleteRec predicate LeLog0.le_log = LeLog0.le_log, function CmpLog0.cmp_log = CmpLog0.cmp_log, axiom . - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color use prelude.Ghost clone RedBlackTree_Impl3_ShallowModel as ShallowModel0 with type k = k, @@ -7512,7 +7398,7 @@ module RedBlackTree_Impl15_DeleteRec clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant clone RedBlackTree_Impl6_MatchN as MatchN0 with type k = k, @@ -7537,6 +7423,7 @@ module RedBlackTree_Impl15_DeleteRec type v = v, predicate BstInvariant0.bst_invariant = BstInvariant1.bst_invariant, predicate HeightInvariant0.height_invariant = HeightInvariant1.height_invariant + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type clone CreusotContracts_Model_Impl0_DeepModel as DeepModel0 with type t = k, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, @@ -7551,7 +7438,7 @@ module RedBlackTree_Impl15_DeleteRec type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant1.internal_invariant, - function Color1.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height1.height, @@ -7570,7 +7457,7 @@ module RedBlackTree_Impl15_DeleteRec function DeepModel0.deep_model = DeepModel1.deep_model, predicate LeLog0.le_log = LeLog0.le_log, predicate ColorInvariant0.color_invariant = ColorInvariant1.color_invariant, - function Color1.color = Color1.color, + function Color0.color = Color0.color, function Height1.height = Height0.height, predicate HasMapping1.has_mapping = HasMapping0.has_mapping clone CreusotContracts_Resolve_Impl1_Resolve as Resolve9 with @@ -7604,7 +7491,7 @@ module RedBlackTree_Impl15_DeleteRec type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, predicate LeLog0.le_log = LeLog0.le_log, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, - function Color1.color = Color1.color + function Color0.color = Color0.color clone RedBlackTree_Impl14_MoveRedRight_Interface as MoveRedRight0 with type k = k, type v = v, @@ -7617,7 +7504,7 @@ module RedBlackTree_Impl15_DeleteRec function DeepModel0.deep_model = DeepModel1.deep_model, predicate LeLog0.le_log = LeLog0.le_log, predicate ColorInvariant0.color_invariant = ColorInvariant1.color_invariant, - function Color1.color = Color1.color, + function Color0.color = Color0.color, function Height1.height = Height0.height, predicate HasMapping1.has_mapping = HasMapping0.has_mapping clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve6 with @@ -7645,7 +7532,7 @@ module RedBlackTree_Impl15_DeleteRec type k = k, type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant1.internal_invariant, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate SameMappings0.same_mappings = SameMappings0.same_mappings, function Height0.height = Height1.height, function DeepModel0.deep_model = DeepModel1.deep_model, @@ -7655,7 +7542,7 @@ module RedBlackTree_Impl15_DeleteRec clone RedBlackTree_Impl13_IsRed_Interface as IsRed0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone Core_Cmp_Ord_Cmp_Interface as Cmp0 with type self = k, function DeepModel0.deep_model = DeepModel1.deep_model, @@ -7683,7 +7570,7 @@ module RedBlackTree_Impl15_DeleteRec end } ensures { [#"../red_black_tree.rs" 745 4 745 129] forall v : v . forall k : DeepModelTy0.deepModelTy . HasMapping0.has_mapping ( ^ self) k v = (DeepModel0.deep_model key <> k /\ HasMapping0.has_mapping ( * self) k v) } ensures { [#"../red_black_tree.rs" 746 14 746 39] ColorInvariant0.color_invariant ( ^ self) } - ensures { [#"../red_black_tree.rs" 747 4 747 69] Color1.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color1.color ( ^ self) = RedBlackTree_Color_Type.C_Black } + ensures { [#"../red_black_tree.rs" 747 4 747 69] Color0.color ( * self) = RedBlackTree_Color_Type.C_Black -> Color0.color ( ^ self) = RedBlackTree_Color_Type.C_Black } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : Core_Option_Option_Type.t_option (k, v); @@ -8117,9 +8004,9 @@ module RedBlackTree_Impl15_Delete_Interface type v use prelude.Borrow use map.Map + use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = k - use Core_Option_Option_Type as Core_Option_Option_Type use map.Map use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl3_ShallowModel_Stub as ShallowModel1 with @@ -8208,10 +8095,8 @@ module RedBlackTree_Impl15_Delete function CmpLog0.cmp_log = CmpLog0.cmp_log, axiom . use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type clone RedBlackTree_Impl9_Height as Height0 with type k = k, @@ -8221,13 +8106,13 @@ module RedBlackTree_Impl15_Delete type k = k, type v = v, function Height0.height = Height0.height - clone RedBlackTree_Impl7_Color as Color1 with + clone RedBlackTree_Impl7_Color as Color0 with type k = k, type v = v clone RedBlackTree_Impl8_ColorInvariantHere as ColorInvariantHere0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone RedBlackTree_Impl9_HeightInvariant as HeightInvariant0 with type k = k, type v = v, @@ -8257,7 +8142,7 @@ module RedBlackTree_Impl15_Delete clone RedBlackTree_Impl6_MatchT as MatchT0 with type k = k, type v = v, - function Color0.color = Color1.color, + function Color0.color = Color0.color, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant clone RedBlackTree_Impl5_BstInvariant as BstInvariant0 with type k = k, @@ -8310,7 +8195,7 @@ module RedBlackTree_Impl15_Delete type v = v, predicate InternalInvariant0.internal_invariant = InternalInvariant0.internal_invariant, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, - function Color0.color = Color1.color + function Color0.color = Color0.color clone Core_Option_Impl0_Unwrap_Interface as Unwrap0 with type t = borrowed (RedBlackTree_Node_Type.t_node k v) clone Core_Option_Impl0_AsMut_Interface as AsMut0 with @@ -8327,13 +8212,13 @@ module RedBlackTree_Impl15_Delete function DeepModel1.deep_model = DeepModel0.deep_model, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, predicate ColorInvariant0.color_invariant = ColorInvariant0.color_invariant, - function Color1.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Impl1_Resolve as Resolve4 with type t = RedBlackTree_Node_Type.t_node k v clone RedBlackTree_Impl13_IsRed_Interface as IsRed0 with type k = k, type v = v, - function Color0.color = Color1.color + function Color0.color = Color0.color clone CreusotContracts_Resolve_Impl1_Resolve as Resolve3 with type t = RedBlackTree_Tree_Type.t_tree k v clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with @@ -8541,10 +8426,8 @@ module RedBlackTree_Impl15_Get use prelude.Ghost use prelude.Borrow use map.Map - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type clone RedBlackTree_Impl9_Height as Height0 with @@ -8924,11 +8807,9 @@ module RedBlackTree_Impl15_GetMut axiom . use Core_Option_Option_Type as Core_Option_Option_Type use map.Map - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use RedBlackTree_Node_Type as RedBlackTree_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use RedBlackTree_Tree_Type as RedBlackTree_Tree_Type use RedBlackTree_Color_Type as RedBlackTree_Color_Type + use RedBlackTree_Node_Type as RedBlackTree_Node_Type clone RedBlackTree_Impl9_Height as Height0 with type k = k, type v = v, diff --git a/creusot/tests/should_succeed/red_black_tree/why3session.xml b/creusot/tests/should_succeed/red_black_tree/why3session.xml index 12baf36c0f..f5c7068695 100644 --- a/creusot/tests/should_succeed/red_black_tree/why3session.xml +++ b/creusot/tests/should_succeed/red_black_tree/why3session.xml @@ -2,9 +2,10 @@ - + + @@ -14,12 +15,12 @@ - + - + @@ -46,10 +47,10 @@ - + - + @@ -63,19 +64,19 @@ - + - + - + - + @@ -87,7 +88,7 @@ - + @@ -99,35 +100,35 @@ - + - + - + - + - + - + - + - + @@ -140,42 +141,42 @@ - + - + - + - + - + - + - + - + - + @@ -191,10 +192,10 @@ - + - + @@ -218,25 +219,305 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + @@ -263,25 +544,25 @@ - + - + - + - + - + - + @@ -296,12 +577,12 @@ - + - + @@ -313,7 +594,7 @@ - + @@ -323,22 +604,22 @@ - + - + - + - + @@ -347,12 +628,12 @@ - + - + @@ -365,7 +646,7 @@ - + @@ -381,12 +662,12 @@ - + - + @@ -397,12 +678,12 @@ - + - + @@ -411,7 +692,7 @@ - + @@ -442,16 +723,16 @@ - + - + - + @@ -460,10 +741,10 @@ - + - + @@ -472,7 +753,43 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -484,21 +801,21 @@ - + - + - + - + - + @@ -509,19 +826,58 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + @@ -531,12 +887,107 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + @@ -561,45 +1012,52 @@ - + - + - + - + - + - + - + + + + + + + + - + - + - + - + - + @@ -608,17 +1066,32 @@ - + - + - + + + + + + + + + + + + + + + + @@ -630,10 +1103,10 @@ - + - + @@ -646,36 +1119,85 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + @@ -685,10 +1207,10 @@ - + - + @@ -697,25 +1219,25 @@ - + - + - + - + - + @@ -724,17 +1246,35 @@ - + - + + + + + + + + + + + + - + + + + + + + + @@ -746,10 +1286,10 @@ - + - + @@ -764,20 +1304,52 @@ - + - + + + + + + + + + + + + + + + + + + + + + + - + - + + + + + + + + + + + + @@ -793,10 +1365,10 @@ - + - + @@ -805,15 +1377,15 @@ - + - + - + @@ -824,20 +1396,34 @@ - + - + + + + + + + + + + + + + + + - + - + @@ -851,27 +1437,27 @@ - + - + - + - + - + - + - + @@ -883,12 +1469,12 @@ - + - + @@ -909,62 +1495,118 @@ - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + - + @@ -980,10 +1622,10 @@ - + - + @@ -997,10 +1639,10 @@ - + - + @@ -1009,15 +1651,15 @@ - + - + - + @@ -1026,10 +1668,10 @@ - + - + @@ -1038,27 +1680,27 @@ - + - + - + - + - + - + @@ -1070,12 +1712,12 @@ - + - + @@ -1096,59 +1738,83 @@ - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + - + - + @@ -1158,22 +1824,46 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + @@ -1182,12 +1872,52 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + @@ -1198,7 +1928,7 @@ - + @@ -1207,10 +1937,10 @@ - + - + @@ -1219,29 +1949,36 @@ - + - + - + - + - + - + - + + + + + + + + @@ -1251,25 +1988,81 @@ - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + - + + + + + + + + + + + + @@ -1278,21 +2071,21 @@ - + - + - + - + - + @@ -1303,17 +2096,17 @@ - + - + - + @@ -1325,7 +2118,18 @@ - + + + + + + + + + + + + @@ -1334,12 +2138,19 @@ - + - + + + + + + + + @@ -1355,10 +2166,10 @@ - + - + @@ -1368,18 +2179,33 @@ - + - + - + + + + + + + + + + + + + + + + - + @@ -1392,15 +2218,15 @@ - + - + - + @@ -1409,12 +2235,24 @@ - + - + + + + + + + + + + + + + @@ -1427,10 +2265,10 @@ - + - + @@ -1441,10 +2279,10 @@ - + - + @@ -1458,34 +2296,34 @@ - + - + - + - + - + - + @@ -1496,29 +2334,29 @@ - + - + - + - + - + @@ -1527,12 +2365,12 @@ - + - + @@ -1547,28 +2385,57 @@ - + - + - + - + + + + + + + + + + + + - + + + + + + + + + + + + - + + + + + + + + @@ -1577,21 +2444,21 @@ - + - + - + - + - + @@ -1607,27 +2474,27 @@ - + - + - + - + - + - + - + @@ -1636,7 +2503,7 @@ - + @@ -1649,7 +2516,7 @@ - + @@ -1661,67 +2528,67 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/red_black_tree/why3shapes.gz b/creusot/tests/should_succeed/red_black_tree/why3shapes.gz index 9dba101a38..37c2554fdc 100644 Binary files a/creusot/tests/should_succeed/red_black_tree/why3shapes.gz and b/creusot/tests/should_succeed/red_black_tree/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/replace.mlcfg b/creusot/tests/should_succeed/replace.mlcfg index b3d7a6e1cf..90dc343ff6 100644 --- a/creusot/tests/should_succeed/replace.mlcfg +++ b/creusot/tests/should_succeed/replace.mlcfg @@ -4,41 +4,10 @@ module Core_Option_Option_Type | C_None | C_Some 't -end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - end module Replace_Something_Type use prelude.Int use prelude.UInt32 - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use Core_Option_Option_Type as Core_Option_Option_Type type t_something = | C_Something uint32 (Core_Option_Option_Type.t_option (t_something)) diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_list.mlcfg b/creusot/tests/should_succeed/rusthorn/inc_some_2_list.mlcfg index 263a2afebc..b48991a0ae 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_2_list.mlcfg +++ b/creusot/tests/should_succeed/rusthorn/inc_some_2_list.mlcfg @@ -235,35 +235,6 @@ module CreusotContracts_Resolve_Impl1_Resolve val resolve (self : borrowed t) : bool ensures { result = resolve self } -end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - end module CreusotContracts_Std1_Num_Impl6_ShallowModel_Stub use prelude.Int @@ -310,13 +281,11 @@ module IncSome2List_Impl0_TakeSomeRest use prelude.UInt32 clone CreusotContracts_Std1_Num_Impl6_ShallowModel as ShallowModel1 use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use IncSome2List_List_Type as IncSome2List_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_Impl3_ShallowModel as ShallowModel0 with type t = uint32, type ShallowModelTy0.shallowModelTy = int, function ShallowModel0.shallow_model = ShallowModel1.shallow_model + use IncSome2List_List_Type as IncSome2List_List_Type clone IncSome2List_Impl0_Sum as Sum0 clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with type t = IncSome2List_List_Type.t_list diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml index 1c7dfa62e9..1bcc3a30a3 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml @@ -18,7 +18,7 @@ - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3shapes.gz b/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3shapes.gz index be78866448..2b07ebedc5 100644 Binary files a/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3shapes.gz and b/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree.mlcfg b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree.mlcfg index 1cfe6a75d0..3770182cce 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree.mlcfg +++ b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree.mlcfg @@ -249,35 +249,6 @@ module CreusotContracts_Resolve_Impl1_Resolve val resolve (self : borrowed t) : bool ensures { result = resolve self } -end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - end module CreusotContracts_Std1_Num_Impl6_ShallowModel_Stub use prelude.Int @@ -323,13 +294,11 @@ module IncSome2Tree_Impl0_TakeSomeRest use prelude.UInt32 clone CreusotContracts_Std1_Num_Impl6_ShallowModel as ShallowModel1 use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use IncSome2Tree_Tree_Type as IncSome2Tree_Tree_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_Impl3_ShallowModel as ShallowModel0 with type t = uint32, type ShallowModelTy0.shallowModelTy = int, function ShallowModel0.shallow_model = ShallowModel1.shallow_model + use IncSome2Tree_Tree_Type as IncSome2Tree_Tree_Type clone IncSome2Tree_Impl0_Sum as Sum0 clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with type t = uint32 diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml index d64c483ac4..a98a39a45d 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml @@ -2,6 +2,7 @@ + @@ -18,7 +19,7 @@ - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3shapes.gz b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3shapes.gz index 347dc6cf5f..6882206972 100644 Binary files a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3shapes.gz and b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_list.mlcfg b/creusot/tests/should_succeed/rusthorn/inc_some_list.mlcfg index be7819cbf7..40cb2bb4e9 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_list.mlcfg +++ b/creusot/tests/should_succeed/rusthorn/inc_some_list.mlcfg @@ -235,35 +235,6 @@ module CreusotContracts_Resolve_Impl1_Resolve val resolve (self : borrowed t) : bool ensures { result = resolve self } -end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - end module CreusotContracts_Std1_Num_Impl6_ShallowModel_Stub use prelude.Int @@ -309,13 +280,11 @@ module IncSomeList_Impl0_TakeSome use prelude.UInt32 clone CreusotContracts_Std1_Num_Impl6_ShallowModel as ShallowModel1 use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use IncSomeList_List_Type as IncSomeList_List_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_Impl3_ShallowModel as ShallowModel0 with type t = uint32, type ShallowModelTy0.shallowModelTy = int, function ShallowModel0.shallow_model = ShallowModel1.shallow_model + use IncSomeList_List_Type as IncSomeList_List_Type clone IncSomeList_Impl0_Sum as Sum0 clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with type t = uint32 diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml index 8d5c9bad96..7c458282f3 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml @@ -17,7 +17,7 @@ - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_list/why3shapes.gz b/creusot/tests/should_succeed/rusthorn/inc_some_list/why3shapes.gz index 5b1bd60d70..10cd81380b 100644 Binary files a/creusot/tests/should_succeed/rusthorn/inc_some_list/why3shapes.gz and b/creusot/tests/should_succeed/rusthorn/inc_some_list/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_tree.mlcfg b/creusot/tests/should_succeed/rusthorn/inc_some_tree.mlcfg index 8d7316510a..2fa7d509be 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_tree.mlcfg +++ b/creusot/tests/should_succeed/rusthorn/inc_some_tree.mlcfg @@ -249,35 +249,6 @@ module CreusotContracts_Resolve_Impl1_Resolve val resolve (self : borrowed t) : bool ensures { result = resolve self } -end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - end module CreusotContracts_Std1_Num_Impl6_ShallowModel_Stub use prelude.Int @@ -322,13 +293,11 @@ module IncSomeTree_Impl0_TakeSome use prelude.UInt32 clone CreusotContracts_Std1_Num_Impl6_ShallowModel as ShallowModel1 use prelude.Int - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use IncSomeTree_Tree_Type as IncSomeTree_Tree_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone CreusotContracts_Model_Impl3_ShallowModel as ShallowModel0 with type t = uint32, type ShallowModelTy0.shallowModelTy = int, function ShallowModel0.shallow_model = ShallowModel1.shallow_model + use IncSomeTree_Tree_Type as IncSomeTree_Tree_Type clone IncSomeTree_Impl0_Sum as Sum0 clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with type t = uint32 diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml index 81bc99c1f6..8088825c41 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml @@ -17,7 +17,7 @@ - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3shapes.gz b/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3shapes.gz index 8aab114815..6c87191b96 100644 Binary files a/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3shapes.gz and b/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/syntax/10_mutual_rec_types.mlcfg b/creusot/tests/should_succeed/syntax/10_mutual_rec_types.mlcfg index dd874ac661..031749c9b4 100644 --- a/creusot/tests/should_succeed/syntax/10_mutual_rec_types.mlcfg +++ b/creusot/tests/should_succeed/syntax/10_mutual_rec_types.mlcfg @@ -10,40 +10,9 @@ module Core_Option_Option_Type | C_Some a -> a end end -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_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 Alloc_Alloc_Global_Type - type t_global = - | C_Global - -end module C10MutualRecTypes_Node_Type use prelude.Int use prelude.UInt32 - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type use Core_Option_Option_Type as Core_Option_Option_Type type t_node = | C_Node (t_tree) uint32 (t_tree) @@ -328,9 +297,6 @@ module C10MutualRecTypes_Impl0_Height clone CreusotContracts_Logic_Ord_Impl2_LeLog as LeLog0 clone CreusotContracts_Logic_Ord_Impl2_GeLog as GeLog0 clone CreusotContracts_Std1_Num_Impl10_DeepModel as DeepModel0 - use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type - use C10MutualRecTypes_Node_Type as C10MutualRecTypes_Node_Type - use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type clone Core_Cmp_Ord_Max_Interface as Max0 with type self = uint64, function DeepModel0.deep_model = DeepModel0.deep_model, @@ -338,6 +304,7 @@ module C10MutualRecTypes_Impl0_Height predicate LeLog0.le_log = LeLog0.le_log, predicate LtLog0.lt_log = LtLog0.lt_log, type DeepModelTy0.deepModelTy = int + use C10MutualRecTypes_Node_Type as C10MutualRecTypes_Node_Type use Core_Option_Option_Type as Core_Option_Option_Type use C10MutualRecTypes_Tree_Type as C10MutualRecTypes_Tree_Type let rec cfg height [#"../10_mutual_rec_types.rs" 16 4 16 31] [@cfg:stackify] [@cfg:subregion_analysis] (self : C10MutualRecTypes_Tree_Type.t_tree) : uint64 diff --git a/creusot/tests/should_succeed/type_invariants/borrows.mlcfg b/creusot/tests/should_succeed/type_invariants/borrows.mlcfg index 7d72349148..172e5cb881 100644 --- a/creusot/tests/should_succeed/type_invariants/borrows.mlcfg +++ b/creusot/tests/should_succeed/type_invariants/borrows.mlcfg @@ -83,12 +83,12 @@ module CreusotContracts_Invariant_Invariant_Invariant ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -96,13 +96,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -135,7 +135,7 @@ module Borrows_Impl1_SubMut_Interface use prelude.Int use Borrows_NonZeroU32_Type as Borrows_NonZeroU32_Type clone Borrows_Impl0_Invariant_Stub as Invariant1 - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = Borrows_NonZeroU32_Type.t_nonzerou32 val sub_mut [#"../borrows.rs" 23 4 23 40] (self : borrowed (Borrows_NonZeroU32_Type.t_nonzerou32)) (rhs : Borrows_NonZeroU32_Type.t_nonzerou32) : () requires {[#"../borrows.rs" 21 15 21 31] UInt32.to_int (Borrows_NonZeroU32_Type.nonzerou32_0 ( * self)) > UInt32.to_int (Borrows_NonZeroU32_Type.nonzerou32_0 rhs)} @@ -151,7 +151,7 @@ module Borrows_Impl1_SubMut use prelude.Borrow use Borrows_NonZeroU32_Type as Borrows_NonZeroU32_Type clone Borrows_Impl0_Invariant as Invariant1 - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant0 with type t = Borrows_NonZeroU32_Type.t_nonzerou32, predicate Invariant0.invariant' = Invariant1.invariant' clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with @@ -195,7 +195,7 @@ module Borrows_Dec use prelude.Borrow use Borrows_NonZeroU32_Type as Borrows_NonZeroU32_Type clone Borrows_Impl0_Invariant as Invariant0 - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant1 with type t = Borrows_NonZeroU32_Type.t_nonzerou32, predicate Invariant0.invariant' = Invariant0.invariant' clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with diff --git a/creusot/tests/should_succeed/type_invariants/generated.mlcfg b/creusot/tests/should_succeed/type_invariants/generated.mlcfg index b62bf56968..1c70b03b03 100644 --- a/creusot/tests/should_succeed/type_invariants/generated.mlcfg +++ b/creusot/tests/should_succeed/type_invariants/generated.mlcfg @@ -120,7 +120,7 @@ module Generated_UseList type t = Core_Option_Option_Type.t_option (Generated_List_Type.t_list int32) clone CreusotContracts_Invariant_Inv_Interface as Inv2 with type t = Core_Option_Option_Type.t_option (Generated_List_Type.t_list int32) - clone Core_Option_Option_Type_Inv as Core_Option_Option_Type_Inv with + clone Core_Option_Option_Type_Inv as Core_Option_Option_Type_Inv0 with type t = Generated_List_Type.t_list int32, predicate Inv0.inv = Inv2.inv, predicate UserInv0.user_inv = UserInv1.user_inv, @@ -128,7 +128,7 @@ module Generated_UseList axiom . clone CreusotContracts_Invariant_Inv_Interface as Inv1 with type t = int32 - clone TyInv_Trivial as TyInv_Trivial with + clone TyInv_Trivial as TyInv_Trivial0 with type t = int32, predicate Inv0.inv = Inv1.inv, axiom . @@ -136,7 +136,7 @@ module Generated_UseList type t = Generated_List_Type.t_list int32 clone CreusotContracts_Invariant_Inv_Interface as Inv0 with type t = Generated_List_Type.t_list int32 - clone Generated_List_Type_Inv as Generated_List_Type_Inv with + clone Generated_List_Type_Inv as Generated_List_Type_Inv0 with type t = int32, predicate Inv0.inv = Inv0.inv, predicate UserInv0.user_inv = UserInv0.user_inv, @@ -147,13 +147,12 @@ module Generated_UseList = [@vc:do_not_keep_trace] [@vc:sp] var _0 : (); - var l_1 : Generated_List_Type.t_list int32; + var l : Generated_List_Type.t_list int32 = l; { - l_1 <- l; goto BB0 } BB0 { - assert { [@expl:assertion] [#"../generated.rs" 7 18 7 35] Inv0.inv l_1 }; + assert { [@expl:assertion] [#"../generated.rs" 7 18 7 35] Inv0.inv l }; goto BB1 } BB1 { diff --git a/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg b/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg index e0005d3ebe..1e5cff575c 100644 --- a/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg +++ b/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg @@ -599,12 +599,12 @@ module CreusotContracts_Std1_Iter_MapInv_MapInv_Type | C_MapInv _ a _ -> a end end -module CreusotContracts_Invariant_Impl1_Invariant_Stub +module CreusotContracts_Invariant_Impl3_Invariant_Stub type t use prelude.Borrow predicate invariant' (self : borrowed t) end -module CreusotContracts_Invariant_Impl1_Invariant_Interface +module CreusotContracts_Invariant_Impl3_Invariant_Interface type t use prelude.Borrow predicate invariant' (self : borrowed t) @@ -612,13 +612,13 @@ module CreusotContracts_Invariant_Impl1_Invariant_Interface ensures { result = invariant' self } end -module CreusotContracts_Invariant_Impl1_Invariant +module CreusotContracts_Invariant_Impl3_Invariant type t use prelude.Borrow clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = t predicate invariant' (self : borrowed t) = - [#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self) + [#"../../../../../creusot-contracts/src/invariant.rs" 67 20 67 39] Invariant0.invariant' ( * self) val invariant' (self : borrowed t) : bool ensures { result = invariant' self } @@ -853,7 +853,7 @@ module CreusotContracts_Std1_Iter_MapInv_Impl3_Reinitialize type b = b, type f = f, type Item0.item = Item0.item - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant0 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant0 with type t = CreusotContracts_Std1_Iter_MapInv_MapInv_Type.t_mapinv i Item0.item f predicate reinitialize (_1 : ()) = [#"../../../../../creusot-contracts/src/std/iter/map_inv.rs" 122 8 128 9] forall reset : borrowed (CreusotContracts_Std1_Iter_MapInv_MapInv_Type.t_mapinv i Item0.item f) . Invariant0.invariant' reset -> Completed0.completed reset -> Invariant1.invariant' (CreusotContracts_Std1_Iter_MapInv_MapInv_Type.mapinv_iter ( ^ reset)) -> NextPrecondition0.next_precondition ( ^ reset) /\ Preservation0.preservation (CreusotContracts_Std1_Iter_MapInv_MapInv_Type.mapinv_iter ( ^ reset)) (CreusotContracts_Std1_Iter_MapInv_MapInv_Type.mapinv_func ( ^ reset)) @@ -1090,7 +1090,7 @@ module Core_Iter_Traits_Iterator_Iterator_Collect_Interface type self = self clone CreusotContracts_Resolve_Resolve_Resolve_Stub as Resolve0 with type self = self - clone CreusotContracts_Invariant_Impl1_Invariant_Stub as Invariant1 with + clone CreusotContracts_Invariant_Impl3_Invariant_Stub as Invariant1 with type t = self clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with type self = self @@ -1853,7 +1853,7 @@ module C06KnightsTour_Impl1_New type f = Closure30.c06knightstour_impl1_new_closure3, predicate Resolve1.resolve = Closure30.resolve, predicate Resolve0.resolve = Resolve1.resolve - clone CreusotContracts_Invariant_Impl1_Invariant as Invariant2 with + clone CreusotContracts_Invariant_Impl3_Invariant as Invariant2 with type t = CreusotContracts_Std1_Iter_MapInv_MapInv_Type.t_mapinv (Core_Ops_Range_Range_Type.t_range usize) usize Closure30.c06knightstour_impl1_new_closure3, predicate Invariant0.invariant' = Invariant1.invariant' clone CreusotContracts_Std1_Iter_MapInv_Impl3_Preservation as Preservation0 with