Merge pull request creusot-rs#805 from xldenis/tyinv-open

Add `open_inv` attribute to pass arguments with an open type invariant

Author: voidc

creusot-contracts/src/invariant.rs

@@ -24,7 +24,6 @@ pub trait Invariant {
 impl<'a, T: Invariant + ?Sized> Invariant for &'a T {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant = "maybe"]
     fn invariant(self) -> bool {
         pearlite! { (*self).invariant() }
     }
@@ -33,7 +32,6 @@ impl<'a, T: Invariant + ?Sized> Invariant for &'a T {
 impl<'a, T: Invariant + ?Sized> Invariant for &'a mut T {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant = "maybe"]
     fn invariant(self) -> bool {
         pearlite! { (*self).invariant() }
     }
@@ -42,7 +40,6 @@ impl<'a, T: Invariant + ?Sized> Invariant for &'a mut T {
 impl<T: Invariant + ?Sized> Invariant for Box<T> {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant = "maybe"]
     fn invariant(self) -> bool {
         pearlite! { (*self).invariant() }
     }
@@ -51,7 +48,6 @@ impl<T: Invariant + ?Sized> Invariant for Box<T> {
 impl<T: Invariant, U: Invariant> Invariant for (T, U) {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant = "maybe"]
     fn invariant(self) -> bool {
         pearlite! { self.0.invariant() && self.1.invariant() }
     }
@@ -60,7 +56,6 @@ impl<T: Invariant, U: Invariant> Invariant for (T, U) {
 impl<T: Invariant> Invariant for Option<T> {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant = "maybe"]
     fn invariant(self) -> bool {
         pearlite! {
             match self {

creusot-contracts/src/std/iter/map_inv.rs

@@ -65,7 +65,6 @@ impl<I: Iterator, B, F: FnMut(I::Item, Ghost<Seq<I::Item>>) -> B> Invariant
     // Should not quantify over self or the `invariant` cannot be made into a type invariant
     #[open(self)]
     #[predicate]
-    #[creusot::ignore_type_invariant]
     fn invariant(self) -> bool {
         pearlite! {
             Self::reinitialize() &&
@@ -108,6 +107,7 @@ impl<I: Iterator, B, F: FnMut(I::Item, Ghost<Seq<I::Item>>) -> B> ::std::iter::I
 impl<I: Iterator, B, F: FnMut(I::Item, Ghost<Seq<I::Item>>) -> B> MapInv<I, I::Item, F> {
     #[open]
     #[predicate]
+    #[creusot::open_inv]
     pub fn next_precondition(self) -> bool {
         pearlite! {
             forall<e: I::Item, i: I>
@@ -131,6 +131,7 @@ impl<I: Iterator, B, F: FnMut(I::Item, Ghost<Seq<I::Item>>) -> B> MapInv<I, I::I
     #[open(self)]
     #[predicate]
     #[ensures(self.produced.inner() == Seq::EMPTY ==> result == Self::preservation(self.iter, self.func))]
+    #[creusot::open_inv]
     pub fn preservation_inv(self) -> bool {
         pearlite! {
             forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>

creusot-contracts/src/std/slice.rs

@@ -279,7 +279,6 @@ extern_spec! {
         fn iter(&self) -> Iter<'_, T>;
 
         #[ensures(result@ == self)]
-        #[ensures(result.invariant())]
         fn iter_mut(&mut self) -> IterMut<'_, T>;
 
         #[ensures(result == None ==> self@.len() == 0)]
@@ -400,6 +399,7 @@ impl<'a, T> ShallowModel for IterMut<'a, T> {
     #[open(self)]
     #[trusted]
     #[ensures((^result)@.len() == (*result)@.len())]
+    #[creusot::open_inv]
     fn shallow_model(self) -> Self::ShallowModelTy {
         absurd
     }
@@ -417,7 +417,6 @@ impl<'a, T> Resolve for IterMut<'a, T> {
 impl<'a, T> Invariant for IterMut<'a, T> {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant]
     fn invariant(self) -> bool {
         // Property that is always true but we must carry around..
         pearlite! { (^self@)@.len() == (*self@)@.len() }

creusot/src/ctx.rs

@@ -29,10 +29,7 @@ use rustc_infer::traits::{Obligation, ObligationCause};
 use rustc_middle::{
     mir::{Body, Promoted},
     thir,
-    ty::{
-        subst::{GenericArgKind, InternalSubsts},
-        GenericArg, ParamEnv, SubstsRef, Ty, TyCtxt, Visibility,
-    },
+    ty::{subst::InternalSubsts, GenericArg, ParamEnv, SubstsRef, Ty, TyCtxt, Visibility},
 };
 use rustc_span::{RealFileName, Span, Symbol, DUMMY_SP};
 use rustc_trait_selection::traits::SelectionContext;
@@ -209,6 +206,10 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
         def_id: DefId,
         ty: Ty<'tcx>,
     ) -> Option<(DefId, SubstsRef<'tcx>)> {
+        if util::is_open_ty_inv(self.tcx, def_id) {
+            return None;
+        }
+
         debug!("resolving type invariant of {ty:?} in {def_id:?}");
         let param_env = self.param_env(def_id);
         let trait_did = self.get_diagnostic_item(Symbol::intern("creusot_invariant_method"))?;
@@ -221,41 +222,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
             return None;
         }
 
-        match util::ignore_type_invariant(self.tcx, inv.0) {
-            util::TypeInvariantAttr::None => return Some(inv),
-            util::TypeInvariantAttr::AlwaysIgnore => return None,
-            util::TypeInvariantAttr::MaybeIgnore => {}
-        }
-
-        let mut walker = ty.walk();
-        walker.next(); // skip root type
-        while let Some(arg) = walker.next() {
-            if !matches!(arg.unpack(), GenericArgKind::Type(_)) {
-                walker.skip_current_subtree();
-                continue;
-            }
-
-            let substs = self.mk_substs(&[arg]);
-            let Some(arg_inv) = traits::resolve_opt(self.tcx, param_env, trait_did, substs) else {
-                walker.skip_current_subtree();
-                continue;
-            };
-
-            if arg_inv.0 == trait_did
-                && !traits::still_specializable(self.tcx, param_env, arg_inv.0, arg_inv.1)
-            {
-                walker.skip_current_subtree();
-                continue;
-            }
-
-            match util::ignore_type_invariant(self.tcx, arg_inv.0) {
-                util::TypeInvariantAttr::None => return Some(inv),
-                util::TypeInvariantAttr::AlwaysIgnore => walker.skip_current_subtree(),
-                util::TypeInvariantAttr::MaybeIgnore => {}
-            }
-        }
-
-        None
+        Some(inv)
     }
 
     pub(crate) fn crash_and_error(&self, span: Span, msg: &str) -> ! {

creusot/src/util.rs

@@ -93,6 +93,10 @@ pub(crate) fn is_extern_spec(tcx: TyCtxt, def_id: DefId) -> bool {
     get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "extern_spec"]).is_some()
 }
 
+pub(crate) fn is_open_ty_inv(tcx: TyCtxt, def_id: DefId) -> bool {
+    get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "open_inv"]).is_some()
+}
+
 pub(crate) fn is_type_invariant(tcx: TyCtxt, def_id: DefId) -> bool {
     let Some(assoc_item) = tcx.opt_associated_item(def_id) else { return false };
     let Some(trait_item_did) = (match assoc_item.container {
@@ -114,24 +118,6 @@ pub(crate) fn opacity_witness_name(tcx: TyCtxt, def_id: DefId) -> Option<Symbol>
     })
 }
 
-pub(crate) enum TypeInvariantAttr {
-    None,
-    MaybeIgnore,
-    AlwaysIgnore,
-}
-
-pub(crate) fn ignore_type_invariant(tcx: TyCtxt, def_id: DefId) -> TypeInvariantAttr {
-    match get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "ignore_type_invariant"]) {
-        None => TypeInvariantAttr::None,
-        Some(AttrItem { args: AttrArgs::Eq(_, AttrArgsEq::Hir(v)), .. })
-            if v.symbol.as_str() == "maybe" =>
-        {
-            TypeInvariantAttr::MaybeIgnore
-        }
-        _ => TypeInvariantAttr::AlwaysIgnore,
-    }
-}
-
 pub(crate) fn why3_attrs(tcx: TyCtxt, def_id: DefId) -> Vec<why3::declaration::Attribute> {
     let matches = get_attrs(tcx.get_attrs_unchecked(def_id), &["why3", "attr"]);
     matches
@@ -471,7 +457,17 @@ fn elaborate_type_invariants<'tcx>(
     }
 
     let subst = InternalSubsts::identity_for_item(ctx.tcx, def_id);
-    for (name, span, ty) in pre_sig.inputs.iter() {
+
+    let param_attrs = def_id
+        .as_local()
+        .and_then(|def_id| get_param_attrs(ctx.tcx, def_id))
+        .filter(|attrs| attrs.len() == pre_sig.inputs.len());
+
+    for (i, (name, span, ty)) in pre_sig.inputs.iter().enumerate() {
+        if let Some(attrs) = &param_attrs && get_attr(attrs[i], &["creusot", "open_inv"]).is_some() {
+            continue;
+        }
+
         if let Some(term) = pearlite::type_invariant_term(ctx, def_id, *name, *span, *ty) {
             let term = EarlyBinder(term).subst(ctx.tcx, subst);
 
@@ -480,8 +476,9 @@ fn elaborate_type_invariants<'tcx>(
                 let arg = Term { ty: *ty, span: *span, kind: TermKind::Var(*name) };
                 let arg =
                     Term { ty: inner, span: *span, kind: TermKind::Fin { term: Box::new(arg) } };
-                let term =
-                    pearlite::type_invariant_term_with_arg(ctx, def_id, arg, *span, inner).unwrap();
+                // FIXME: why can this be none?
+                let Some(term) =
+                    pearlite::type_invariant_term_with_arg(ctx, def_id, arg, *span, inner) else {continue; };
                 pre_sig.contract.ensures.push(term);
             }
 
@@ -568,6 +565,16 @@ pub(crate) fn is_attr(attr: &Attribute, str: &str) -> bool {
     }
 }
 
+/// Returns `None` if the `def_id` does not refer to a body owner.
+pub(crate) fn get_param_attrs<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    def_id: LocalDefId,
+) -> Option<Vec<&'tcx [Attribute]>> {
+    let body_id = tcx.hir().maybe_body_owned_by(def_id)?;
+    let params = tcx.hir().body(body_id).params;
+    Some(params.iter().map(|p| tcx.hir().attrs(p.hir_id)).collect())
+}
+
 use rustc_span::def_id::LocalDefId;
 use rustc_target::abi::FieldIdx;
 

creusot/tests/should_succeed/hillel.mlcfg

@@ -1110,7 +1110,7 @@ module CreusotContracts_Std1_Slice_Impl15_Produces
   predicate produces (self : Core_Slice_Iter_Iter_Type.t_iter t) (visited : Seq.seq t) (tl : Core_Slice_Iter_Iter_Type.t_iter t)
 
    =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 379 12 379 66] ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model tl))
+    [#"../../../../creusot-contracts/src/std/slice.rs" 378 12 378 66] ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model tl))
   val produces (self : Core_Slice_Iter_Iter_Type.t_iter t) (visited : Seq.seq t) (tl : Core_Slice_Iter_Iter_Type.t_iter t) : bool
     ensures { result = produces self visited tl }
 
@@ -1183,7 +1183,7 @@ module Core_Slice_Impl0_Iter_Interface
   clone CreusotContracts_Std1_Slice_Impl13_ShallowModel_Stub as ShallowModel0 with
     type t = t
   val iter (self : slice t) : Core_Slice_Iter_Iter_Type.t_iter t
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 325 1] ShallowModel0.shallow_model result = self }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] ShallowModel0.shallow_model result = self }
 
 end
 module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPre_Stub
@@ -1320,7 +1320,7 @@ module CreusotContracts_Std1_Slice_Impl15_Completed
   clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with
     type t = Core_Slice_Iter_Iter_Type.t_iter t
   predicate completed (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 372 20 372 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty 
+    [#"../../../../creusot-contracts/src/std/slice.rs" 371 20 371 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty 
   val completed (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) : bool
     ensures { result = completed self }
 
@@ -1451,10 +1451,10 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesRefl_Interface
     type t = t
   function produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
   val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 385 14 385 39] Produces0.produces a (Seq.empty ) a }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
     ensures { result = produces_refl a }
 
-  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 385 14 385 39] Produces0.produces a (Seq.empty ) a
+  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
   type t
@@ -1463,12 +1463,12 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
   clone CreusotContracts_Std1_Slice_Impl15_Produces_Stub as Produces0 with
     type t = t
   function produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : () =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 383 4 383 10] ()
+    [#"../../../../creusot-contracts/src/std/slice.rs" 382 4 382 10] ()
   val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 385 14 385 39] Produces0.produces a (Seq.empty ) a }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
     ensures { result = produces_refl a }
 
-  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 385 14 385 39] Produces0.produces a (Seq.empty ) a
+  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Stub
   type t
@@ -1490,12 +1490,12 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Interface
   function produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
 
   val produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces a ab b}
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 391 15 391 32] Produces0.produces b bc c}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 392 14 392 42] Produces0.produces a (Seq.(++) ab bc) c }
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c}
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c }
     ensures { result = produces_trans a ab b bc c }
 
-  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 391 15 391 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 392 14 392 42] Produces0.produces a (Seq.(++) ab bc) c)
+  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
   type t
@@ -1507,14 +1507,14 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
   function produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
 
    =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 388 4 388 10] ()
+    [#"../../../../creusot-contracts/src/std/slice.rs" 387 4 387 10] ()
   val produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces a ab b}
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 391 15 391 32] Produces0.produces b bc c}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 392 14 392 42] Produces0.produces a (Seq.(++) ab bc) c }
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c}
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c }
     ensures { result = produces_trans a ab b bc c }
 
-  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 391 15 391 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 392 14 392 42] Produces0.produces a (Seq.(++) ab bc) c)
+  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module Hillel_InsertUnique_Interface
   type t
@@ -2034,7 +2034,7 @@ module Core_Slice_Impl0_Len_Interface
     type t = slice t,
     type ShallowModelTy0.shallowModelTy = Seq.seq t
   val len (self : slice t) : usize
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 325 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
 
 end
 module CreusotContracts_Std1_Iter_Iterator_Completed_Stub
@@ -2857,7 +2857,7 @@ module CreusotContracts_Std1_Slice_Impl11_IntoIterPre
   use prelude.Borrow
   use prelude.Slice
   predicate into_iter_pre (self : slice t) =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 331 20 331 24] true
+    [#"../../../../creusot-contracts/src/std/slice.rs" 330 20 330 24] true
   val into_iter_pre (self : slice t) : bool
     ensures { result = into_iter_pre self }
 
@@ -2887,7 +2887,7 @@ module CreusotContracts_Std1_Slice_Impl11_IntoIterPost
   clone CreusotContracts_Std1_Slice_Impl13_ShallowModel_Stub as ShallowModel0 with
     type t = t
   predicate into_iter_post (self : slice t) (res : Core_Slice_Iter_Iter_Type.t_iter t) =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 337 20 337 32] self = ShallowModel0.shallow_model res
+    [#"../../../../creusot-contracts/src/std/slice.rs" 336 20 336 32] self = ShallowModel0.shallow_model res
   val into_iter_post (self : slice t) (res : Core_Slice_Iter_Iter_Type.t_iter t) : bool
     ensures { result = into_iter_post self res }
 

creusot/tests/should_succeed/index_range.mlcfg

@@ -563,7 +563,7 @@ module Core_Slice_Impl0_Len_Interface
     type t = slice t,
     type ShallowModelTy0.shallowModelTy = Seq.seq t
   val len (self : slice t) : usize
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 325 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
 
 end
 module Alloc_Vec_Impl9_Deref_Interface