Merge pull request #1004 from creusot-rs/small-coma-cleanups

Small coma related cleanups
creusot-rs · May 18, 2024 · 5077cda · 5077cda
2 parents c96ccbb + 890fbd4
commit 5077cda
Show file tree

Hide file tree

Showing 126 changed files with 8,064 additions and 3,523 deletions.
diff --git a/creusot/src/cleanup_spec_closures.rs b/creusot/src/cleanup_spec_closures.rs
@@ -3,8 +3,8 @@ use rustc_hir::def_id::DefId;
 use rustc_index::{Idx, IndexVec};
 use rustc_middle::{
     mir::{
-        dump_mir, visit::MutVisitor, AggregateKind, BasicBlock, BasicBlockData, Body, Local,
-        Location, Rvalue, SourceInfo, StatementKind, Terminator, TerminatorKind,
+        visit::MutVisitor, AggregateKind, BasicBlock, BasicBlockData, Body, Local, Location,
+        Rvalue, SourceInfo, StatementKind, Terminator, TerminatorKind,
     },
     ty::TyCtxt,
 };
@@ -24,7 +24,6 @@ pub(crate) fn cleanup_spec_closures<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, body
         *body.basic_blocks_mut() = make_loop(tcx);
         body.var_debug_info = Vec::new();
     } else {
-        // dump_mir(tcx, false, "speccleanup", &"before", &body, |_, _| Ok(()));
         let mut cleanup = NoTranslateNoMoves { tcx, unused: IndexSet::new() };
         cleanup.visit_body(body);
 
@@ -34,7 +33,6 @@ pub(crate) fn cleanup_spec_closures<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, body
         updater.visit_body(body);
 
         body.local_decls.shrink_to_fit();
-        dump_mir(tcx, false, "speccleanup", &"after", &body, |_, _| Ok(()));
     }
 }
 

diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness.mlcfg b/creusot/tests/should_fail/bug/01_resolve_unsoundness.mlcfg
@@ -95,7 +95,9 @@ module C01ResolveUnsoundness_MakeVecOfSize
     ensures { result = shallow_model0 self }
 
   axiom shallow_model0_spec : forall self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global) . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] inv0 self)
-   -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] inv3 (shallow_model0 self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model0 self) <= UIntSize.to_int max0)
+   -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] inv3 (shallow_model0 self))
+  && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model0 self)
+  <= UIntSize.to_int max0)
   predicate invariant0 (self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) =
     [#"../../../../../creusot-contracts/src/std/vec.rs" 60 20 60 41] inv3 (shallow_model0 self)
   val invariant0 (self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) : bool
@@ -113,7 +115,8 @@ module C01ResolveUnsoundness_MakeVecOfSize
   val push0 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) (value : bool) : ()
     requires {inv1 self}
     requires {inv2 value}
-    ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 78 26 78 51] shallow_model0 ( ^ self) = Seq.snoc (shallow_model1 self) value }
+    ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 78 26 78 51] shallow_model0 ( ^ self)
+    = Seq.snoc (shallow_model1 self) value }
 
   val new0 (_1 : ()) : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)
     ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 68 26 68 44] Seq.length (shallow_model0 result) = 0 }

diff --git a/creusot/tests/should_fail/bug/222.mlcfg b/creusot/tests/should_fail/bug/222.mlcfg
@@ -74,7 +74,8 @@ module C222_UsesInvariant
 
   val take0 (self : borrowed (Core_Option_Option_Type.t_option t)) : Core_Option_Option_Type.t_option t
     requires {inv2 self}
-    ensures { [#"../../../../../creusot-contracts/src/std/option.rs" 29 0 126 1] result =  * self /\  ^ self = Core_Option_Option_Type.C_None }
+    ensures { [#"../../../../../creusot-contracts/src/std/option.rs" 29 0 126 1] result =  * self
+    /\  ^ self = Core_Option_Option_Type.C_None }
     ensures { inv0 result }
 
   let rec cfg uses_invariant [#"../222.rs" 40 0 40 41] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed (C222_Once_Type.t_once t)) : ()

diff --git a/creusot/tests/should_fail/bug/492.mlcfg b/creusot/tests/should_fail/bug/492.mlcfg
@@ -95,7 +95,8 @@ module C492_Test
     ensures { result = resolve2 self }
 
   predicate resolve0 (self : (borrowed int32, uint32)) =
-    [#"../../../../../creusot-contracts/src/resolve.rs" 17 8 17 60] resolve1 (let (a, _) = self in a) /\ resolve2 (let (_, a) = self in a)
+    [#"../../../../../creusot-contracts/src/resolve.rs" 17 8 17 60] resolve1 (let (a, _) = self in a)
+    /\ resolve2 (let (_, a) = self in a)
   val resolve0 (self : (borrowed int32, uint32)) : bool
     ensures { result = resolve0 self }
 

diff --git a/creusot/tests/should_fail/bug/692.mlcfg b/creusot/tests/should_fail/bug/692.mlcfg
@@ -41,7 +41,8 @@ module C692_Incorrect
   axiom fn_mut_once0_spec : forall self : c, args : (), res : bool . ([#"../../../../../creusot-contracts/src/std/ops.rs" 123 19 123 23] inv1 self)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 123 25 123 29] inv3 args)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 123 37 123 40] inv4 res)
-   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 122 14 122 135] postcondition_once0 self args res = (exists s : borrowed c . inv2 s /\  * s = self /\ postcondition_mut0 s args res /\ resolve1 ( ^ s)))
+   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 122 14 122 135] postcondition_once0 self args res
+  = (exists s : borrowed c . inv2 s /\  * s = self /\ postcondition_mut0 s args res /\ resolve1 ( ^ s)))
   predicate unnest0 (self : c) (_2 : c)
   val unnest0 (self : c) (_2 : c) : bool
     ensures { result = unnest0 self _2 }
@@ -112,7 +113,8 @@ module C692_Incorrect
   axiom fn_once0_spec : forall self : c, args : (), res : bool . ([#"../../../../../creusot-contracts/src/std/ops.rs" 145 15 145 19] inv1 self)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 145 21 145 25] inv3 args)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 145 33 145 36] inv4 res)
-   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 144 14 144 101] postcondition_once0 self args res = (resolve1 self /\ postcondition0 self args res))
+   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 144 14 144 101] postcondition_once0 self args res
+  = (resolve1 self /\ postcondition0 self args res))
   predicate resolve2 (self : borrowed c) =
     [#"../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34]  ^ self =  * self
   val resolve2 (self : borrowed c) : bool
@@ -128,7 +130,8 @@ module C692_Incorrect
   axiom fn_mut0_spec : forall self : borrowed c, args : (), res : bool . ([#"../../../../../creusot-contracts/src/std/ops.rs" 139 19 139 23] inv2 self)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 139 25 139 29] inv3 args)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 139 37 139 40] inv4 res)
-   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 138 14 138 100] postcondition_mut0 self args res = (resolve2 self /\ postcondition0 ( * self) args res))
+   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 138 14 138 100] postcondition_mut0 self args res
+  = (resolve2 self /\ postcondition0 ( * self) args res))
   predicate invariant1 (self : c)
   val invariant1 (self : c) : bool
     ensures { result = invariant1 self }
@@ -156,8 +159,9 @@ module C692_Incorrect
     ensures { result = resolve0 self }
 
   let rec cfg incorrect [#"../692.rs" 8 0 8 76] [@cfg:stackify] [@cfg:subregion_analysis] (cond : c) (branch : b) : ()
-    requires {[#"../692.rs" 5 0 6 87] precondition0 cond () /\ (forall b : bool . precondition1 branch (b) /\ (exists b : bool . forall b0 : bool . postcondition0 cond () b0
-     -> b0 = b))}
+    requires {[#"../692.rs" 5 0 6 87] precondition0 cond ()
+    /\ (forall b : bool . precondition1 branch (b)
+    /\ (exists b : bool . forall b0 : bool . postcondition0 cond () b0  -> b0 = b))}
     requires {[#"../692.rs" 8 57 8 61] inv1 cond}
     requires {[#"../692.rs" 8 66 8 72] inv0 branch}
     ensures { [#"../692.rs" 7 10 7 15] false }
@@ -220,7 +224,8 @@ module C692_ValidNormal_Closure2
     ensures { result = resolve0 self }
 
   let rec cfg c692_validnormal_closure2 [#"../692.rs" 15 17 15 64] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : borrowed C692_ValidNormal_Closure2_Type.c692_validnormal_closure2) (b : bool) : ()
-    ensures { [#"../692.rs" 15 27 15 62] b /\  * field_00 ( ^ _1) = (2 : uint32) \/ not b /\  * field_00 ( ^ _1) = (1 : uint32) }
+    ensures { [#"../692.rs" 15 27 15 62] b /\  * field_00 ( ^ _1) = (2 : uint32)
+    \/ not b /\  * field_00 ( ^ _1) = (1 : uint32) }
     ensures { unnest0 ( * _1) ( ^ _1) }
 
    = [@vc:do_not_keep_trace] [@vc:sp]
@@ -343,8 +348,9 @@ module C692_ValidNormal
    =
     true
   val incorrect0 [#"../692.rs" 8 0 8 76] (cond : C692_ValidNormal_Closure1_Type.c692_validnormal_closure1) (branch : C692_ValidNormal_Closure2_Type.c692_validnormal_closure2) : ()
-    requires {[#"../692.rs" 5 0 6 87] precondition0 cond () /\ (forall b : bool . precondition1 branch (b) /\ (exists b : bool . forall b0 : bool . postcondition0 cond () b0
-     -> b0 = b))}
+    requires {[#"../692.rs" 5 0 6 87] precondition0 cond ()
+    /\ (forall b : bool . precondition1 branch (b)
+    /\ (exists b : bool . forall b0 : bool . postcondition0 cond () b0  -> b0 = b))}
     requires {[#"../692.rs" 8 57 8 61] inv0 cond}
     requires {[#"../692.rs" 8 66 8 72] inv1 branch}
     ensures { [#"../692.rs" 7 10 7 15] false }

diff --git a/creusot/tests/should_fail/bug/695.mlcfg b/creusot/tests/should_fail/bug/695.mlcfg
@@ -41,7 +41,8 @@ module C695_InversedIf
   axiom fn_mut_once0_spec : forall self : c, args : (), res : bool . ([#"../../../../../creusot-contracts/src/std/ops.rs" 123 19 123 23] inv0 self)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 123 25 123 29] inv3 args)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 123 37 123 40] inv4 res)
-   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 122 14 122 135] postcondition_once1 self args res = (exists s : borrowed c . inv6 s /\  * s = self /\ postcondition_mut0 s args res /\ resolve0 ( ^ s)))
+   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 122 14 122 135] postcondition_once1 self args res
+  = (exists s : borrowed c . inv6 s /\  * s = self /\ postcondition_mut0 s args res /\ resolve0 ( ^ s)))
   predicate unnest0 (self : c) (_2 : c)
   val unnest0 (self : c) (_2 : c) : bool
     ensures { result = unnest0 self _2 }
@@ -131,7 +132,8 @@ module C695_InversedIf
   axiom fn_once0_spec : forall self : c, args : (), res : bool . ([#"../../../../../creusot-contracts/src/std/ops.rs" 145 15 145 19] inv0 self)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 145 21 145 25] inv3 args)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 145 33 145 36] inv4 res)
-   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 144 14 144 101] postcondition_once1 self args res = (resolve0 self /\ postcondition0 self args res))
+   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 144 14 144 101] postcondition_once1 self args res
+  = (resolve0 self /\ postcondition0 self args res))
   predicate resolve1 (self : borrowed c) =
     [#"../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34]  ^ self =  * self
   val resolve1 (self : borrowed c) : bool
@@ -147,7 +149,8 @@ module C695_InversedIf
   axiom fn_mut0_spec : forall self : borrowed c, args : (), res : bool . ([#"../../../../../creusot-contracts/src/std/ops.rs" 139 19 139 23] inv6 self)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 139 25 139 29] inv3 args)
    -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 139 37 139 40] inv4 res)
-   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 138 14 138 100] postcondition_mut0 self args res = (resolve1 self /\ postcondition0 ( * self) args res))
+   -> ([#"../../../../../creusot-contracts/src/std/ops.rs" 138 14 138 100] postcondition_mut0 self args res
+  = (resolve1 self /\ postcondition0 ( * self) args res))
   predicate invariant1 (self : b)
   val invariant1 (self : b) : bool
     ensures { result = invariant1 self }
@@ -192,7 +195,8 @@ module C695_InversedIf
     requires {[#"../695.rs" 4 0 4 79] precondition0 cond () /\ (forall b : bool . precondition1 branch (b))}
     requires {[#"../695.rs" 6 59 6 63] inv0 cond}
     requires {[#"../695.rs" 6 68 6 74] inv1 branch}
-    ensures { [#"../695.rs" 5 0 5 91] exists b : bool . postcondition0 cond () b /\ postcondition_once0 branch (not b) () }
+    ensures { [#"../695.rs" 5 0 5 91] exists b : bool . postcondition0 cond () b
+    /\ postcondition_once0 branch (not b) () }
 
    = [@vc:do_not_keep_trace] [@vc:sp]
   var _0 : ();
@@ -288,7 +292,8 @@ module C695_Valid_Closure2
     ensures { result = resolve0 self }
 
   let rec cfg c695_valid_closure2 [#"../695.rs" 19 17 19 64] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : borrowed C695_Valid_Closure2_Type.c695_valid_closure2) (b : bool) : ()
-    ensures { [#"../695.rs" 19 27 19 62] b /\  * field_00 ( ^ _1) = (2 : uint32) \/ not b /\  * field_00 ( ^ _1) = (1 : uint32) }
+    ensures { [#"../695.rs" 19 27 19 62] b /\  * field_00 ( ^ _1) = (2 : uint32)
+    \/ not b /\  * field_00 ( ^ _1) = (1 : uint32) }
     ensures { unnest0 ( * _1) ( ^ _1) }
 
    = [@vc:do_not_keep_trace] [@vc:sp]
@@ -397,7 +402,8 @@ module C695_Valid
   predicate postcondition_once0 [#"../695.rs" 19 17 19 64] (self : C695_Valid_Closure2_Type.c695_valid_closure2) (args : bool) (result : ())
 
    =
-    [#"../695.rs" 19 27 19 62] let (b) = args in b /\  ^ field_01 self = (2 : uint32) \/ not b /\  ^ field_01 self = (1 : uint32)
+    [#"../695.rs" 19 27 19 62] let (b) = args in b /\  ^ field_01 self = (2 : uint32)
+    \/ not b /\  ^ field_01 self = (1 : uint32)
   function field_00 [#"../695.rs" 17 15 17 47] (self : C695_Valid_Closure1_Type.c695_valid_closure1) : uint32 =
     let C695_Valid_Closure1_Type.C695_valid_closure1 a = self in a
   val field_00 [#"../695.rs" 17 15 17 47] (self : C695_Valid_Closure1_Type.c695_valid_closure1) : uint32
@@ -416,12 +422,14 @@ module C695_Valid
     requires {[#"../695.rs" 4 0 4 79] precondition0 cond () /\ (forall b : bool . precondition1 branch (b))}
     requires {[#"../695.rs" 6 59 6 63] inv0 cond}
     requires {[#"../695.rs" 6 68 6 74] inv1 branch}
-    ensures { [#"../695.rs" 5 0 5 91] exists b : bool . postcondition0 cond () b /\ postcondition_once0 branch (not b) () }
+    ensures { [#"../695.rs" 5 0 5 91] exists b : bool . postcondition0 cond () b
+    /\ postcondition_once0 branch (not b) () }
 
   predicate resolve0 [#"../695.rs" 17 15 17 47] (_1 : C695_Valid_Closure1_Type.c695_valid_closure1) =
     true
   let rec cfg valid [#"../695.rs" 15 0 15 27] [@cfg:stackify] [@cfg:subregion_analysis] (n : uint32) : uint32
-    ensures { [#"../695.rs" 14 10 14 71] n > (7 : uint32) /\ result = (2 : uint32) \/ n <= (7 : uint32) /\ result = (1 : uint32) }
+    ensures { [#"../695.rs" 14 10 14 71] n > (7 : uint32) /\ result = (2 : uint32)
+    \/ n <= (7 : uint32) /\ result = (1 : uint32) }
 
    = [@vc:do_not_keep_trace] [@vc:sp]
   var _0 : uint32;

diff --git a/creusot/tests/should_fail/bug/869.mlcfg b/creusot/tests/should_fail/bug/869.mlcfg
@@ -46,13 +46,15 @@ module C869_Unsound
     goto BB2
   }
   BB2 {
-    assert { [@expl:assertion] [#"../869.rs" 11 20 11 50] Snapshot.inner ( * Snapshot.inner bg) = true /\ Snapshot.inner ( ^ Snapshot.inner bg) = true };
+    assert { [@expl:assertion] [#"../869.rs" 11 20 11 50] Snapshot.inner ( * Snapshot.inner bg) = true
+    /\ Snapshot.inner ( ^ Snapshot.inner bg) = true };
     [#"../869.rs" 13 36 13 44] _12 <- Borrow.borrow_final ( * xm) (Borrow.get_id xm);
     [#"../869.rs" 13 36 13 44] xm <- { xm with current = ( ^ _12) ; };
     [#"../869.rs" 13 36 13 44] evil <- Borrow.borrow_final ( * _12) (Borrow.get_id _12);
     [#"../869.rs" 13 36 13 44] _12 <- { _12 with current = ( ^ evil) ; };
     assume { resolve0 _12 };
-    assert { [@expl:assertion] [#"../869.rs" 17 20 17 53] (evil = Snapshot.inner bg) = (Snapshot.inner ( ^ evil) = true) };
+    assert { [@expl:assertion] [#"../869.rs" 17 20 17 53] (evil = Snapshot.inner bg)
+    = (Snapshot.inner ( ^ evil) = true) };
     [#"../869.rs" 18 12 18 64] _15 <- ([#"../869.rs" 18 12 18 64] Snapshot.new (if evil = Snapshot.inner bg then
       false
     else

diff --git a/creusot/tests/should_fail/bug/specialize.mlcfg b/creusot/tests/should_fail/bug/specialize.mlcfg
@@ -106,7 +106,9 @@ module Specialize_G
     ensures { result = shallow_model0 self }
 
   axiom shallow_model0_spec : forall self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] inv0 self)
-   -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] inv1 (shallow_model0 self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model0 self) <= UIntSize.to_int max0)
+   -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] inv1 (shallow_model0 self))
+  && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model0 self)
+  <= UIntSize.to_int max0)
   predicate invariant0 (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) =
     [#"../../../../../creusot-contracts/src/std/vec.rs" 60 20 60 41] inv1 (shallow_model0 self)
   val invariant0 (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) : bool
@@ -172,7 +174,9 @@ module Specialize_H
     ensures { result = shallow_model0 self }
 
   axiom shallow_model0_spec : forall self : Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global) . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] inv0 self)
-   -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] inv1 (shallow_model0 self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model0 self) <= UIntSize.to_int max0)
+   -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] inv1 (shallow_model0 self))
+  && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model0 self)
+  <= UIntSize.to_int max0)
   predicate invariant0 (self : Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global)) =
     [#"../../../../../creusot-contracts/src/std/vec.rs" 60 20 60 41] inv1 (shallow_model0 self)
   val invariant0 (self : Alloc_Vec_Vec_Type.t_vec int32 (Alloc_Alloc_Global_Type.t_global)) : bool
@@ -237,7 +241,9 @@ module Specialize_Impl0
     ensures { result = shallow_model0 self }
 
   axiom shallow_model0_spec : forall self : Alloc_Vec_Vec_Type.t_vec u (Alloc_Alloc_Global_Type.t_global) . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] inv0 self)
-   -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] inv1 (shallow_model0 self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model0 self) <= UIntSize.to_int max0)
+   -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] inv1 (shallow_model0 self))
+  && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model0 self)
+  <= UIntSize.to_int max0)
   predicate invariant0 (self : Alloc_Vec_Vec_Type.t_vec u (Alloc_Alloc_Global_Type.t_global)) =
     [#"../../../../../creusot-contracts/src/std/vec.rs" 60 20 60 41] inv1 (shallow_model0 self)
   val invariant0 (self : Alloc_Vec_Vec_Type.t_vec u (Alloc_Alloc_Global_Type.t_global)) : bool