Update proofs

creusot-rs · Jun 14, 2023 · e768e46 · e768e46
1 parent d73bbae
commit e768e46
Show file tree

Hide file tree

Showing 54 changed files with 1,546 additions and 1,133 deletions.
diff --git 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
@@ -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
@@ -7,7 +7,7 @@
 <path name=".."/><path name="all_zero.mlcfg"/>
 <theory name="AllZero_AllZero" proved="true">
  <goal name="all_zero&#39;vc" expl="VC for all_zero" proved="true">
- <proof prover="1"><result status="valid" time="0.06" steps="738"/></proof>
+ <proof prover="1"><result status="valid" time="0.06" steps="739"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/creusot/tests/should_succeed/all_zero/why3shapes.gz b/creusot/tests/should_succeed/all_zero/why3shapes.gz
diff --git 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
@@ -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
@@ -12,12 +12,12 @@
 </theory>
 <theory name="BinarySearch_Impl0_Index" proved="true">
  <goal name="index&#39;vc" expl="VC for index" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="122"/></proof>
+ <proof prover="1"><result status="valid" time="0.03" steps="120"/></proof>
  </goal>
 </theory>
 <theory name="BinarySearch_Impl0_Len" proved="true">
  <goal name="len&#39;vc" expl="VC for len" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="113"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="114"/></proof>
  </goal>
 </theory>
 <theory name="BinarySearch_BinarySearch" proved="true">

diff --git a/creusot/tests/should_succeed/binary_search/why3shapes.gz b/creusot/tests/should_succeed/binary_search/why3shapes.gz
diff --git 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,16 +297,14 @@ 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,
     predicate GeLog0.ge_log = GeLog0.ge_log,
     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
@@ -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
@@ -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