Pearlite support for Range

creusot-contracts-proc/src/pretyping.rs

@@ -149,7 +149,18 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
             Ok(quote_spanned! {sp=> (#term) })
         }
         RT::Path(_) => Ok(quote_spanned! {sp=> #term }),
-        RT::Range(_) => Err(EncodeError::Unsupported(term.span(), "Range".into())),
+        RT::Range(TermRange { from, limits, to }) => {
+            let from = match from {
+                None => None,
+                Some(from) => Some(encode_term(from)?),
+            };
+            let to = match to {
+                None => None,
+                Some(to) => Some(encode_term(to)?),
+            };
+            let limits = limits;
+            Ok(quote_spanned! {sp=>#from #limits #to})
+        }
         RT::Reference(TermReference { mutability, expr, .. }) => {
             let term = encode_term(expr)?;
             Ok(quote! {

creusot-contracts/src/logic/seq.rs

@@ -1,3 +1,5 @@
+use ::std::ops::Range;
+
 use crate::{logic::ops::IndexLogic, *};
 
 #[cfg_attr(creusot, creusot::builtins = "seq.Seq.seq")]
@@ -165,3 +167,14 @@ impl<T> IndexLogic<Int> for Seq<T> {
         absurd
     }
 }
+
+impl<T> IndexLogic<Range<Int>> for Seq<T> {
+    type Item = Seq<T>;
+
+    #[ghost]
+    #[open]
+    #[why3::attr = "inline:trivial"]
+    fn index_logic(self, r: Range<Int>) -> Self::Item {
+        self.subsequence(r.start, r.end)
+    }
+}

creusot-contracts/src/std/deque.rs

@@ -1,4 +1,5 @@
-use crate::{logic::IndexLogic, std::alloc::Allocator, *};
+use crate::{invariant::Invariant, logic::IndexLogic, std::alloc::Allocator, *};
+use ::std::collections::vec_deque::{IntoIter, Iter};
 pub use ::std::collections::VecDeque;
 
 impl<T, A: Allocator> ShallowModel for VecDeque<T, A> {
@@ -13,6 +14,131 @@ impl<T, A: Allocator> ShallowModel for VecDeque<T, A> {
     }
 }
 
+impl<'a, T> Invariant for Iter<'a, T> {}
+
+impl<T, A: Allocator> ShallowModel for IntoIter<T, A> {
+    type ShallowModelTy = Seq<T>;
+
+    #[open(self)]
+    #[ghost]
+    #[trusted]
+    fn shallow_model(self) -> Self::ShallowModelTy {
+        absurd
+    }
+}
+
+impl<'a, T> ShallowModel for Iter<'a, T> {
+    // TODO : This seems wrong
+    type ShallowModelTy = &'a [T];
+
+    #[ghost]
+    #[open(self)]
+    #[trusted]
+    fn shallow_model(self) -> Self::ShallowModelTy {
+        absurd
+    }
+}
+
+impl<'a, T> Iterator for Iter<'a, T> {
+    #[predicate]
+    #[open]
+    fn completed(&mut self) -> bool {
+        pearlite! { self.resolve() && (*self)@@ == Seq::EMPTY }
+    }
+
+    #[predicate]
+    #[open]
+    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
+        pearlite! {
+            [email protected]_ref_seq() == visited.concat([email protected]_ref_seq())
+        }
+    }
+
+    #[law]
+    #[open]
+    #[ensures(a.produces(Seq::EMPTY, a))]
+    fn produces_refl(a: Self) {}
+
+    #[law]
+    #[open]
+    #[requires(a.produces(ab, b))]
+    #[requires(b.produces(bc, c))]
+    #[ensures(a.produces(ab.concat(bc), c))]
+    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
+}
+
+impl<T, A: Allocator> Invariant for IntoIter<T, A> {}
+
+impl<T, A: Allocator> Iterator for IntoIter<T, A> {
+    #[predicate]
+    #[open]
+    fn completed(&mut self) -> bool {
+        pearlite! { self.resolve() && self@ == Seq::EMPTY }
+    }
+
+    #[predicate]
+    #[open]
+    fn produces(self, visited: Seq<T>, rhs: Self) -> bool {
+        pearlite! {
+            self@ == visited.concat(rhs@)
+        }
+    }
+
+    #[law]
+    #[open]
+    #[ensures(a.produces(Seq::EMPTY, a))]
+    fn produces_refl(a: Self) {}
+
+    #[law]
+    #[open]
+    #[requires(a.produces(ab, b))]
+    #[requires(b.produces(bc, c))]
+    #[ensures(a.produces(ab.concat(bc), c))]
+    fn produces_trans(a: Self, ab: Seq<T>, b: Self, bc: Seq<T>, c: Self) {}
+}
+
+impl<T, A: Allocator> IntoIterator for VecDeque<T, A> {
+    #[predicate]
+    #[open]
+    fn into_iter_pre(self) -> bool {
+        pearlite! { true }
+    }
+
+    #[predicate]
+    #[open]
+    fn into_iter_post(self, res: Self::IntoIter) -> bool {
+        pearlite! { self@ == res@ }
+    }
+}
+
+impl<T, A: Allocator> IntoIterator for &VecDeque<T, A> {
+    #[predicate]
+    #[open]
+    fn into_iter_pre(self) -> bool {
+        pearlite! { true }
+    }
+
+    #[predicate]
+    #[open]
+    fn into_iter_post(self, res: Self::IntoIter) -> bool {
+        pearlite! { self@ == res@@ }
+    }
+}
+
+// impl<T, A: Allocator> IntoIterator for &mut VecDeque<T, A> {
+//     #[predicate]
+//     #[open]
+//     fn into_iter_pre(self) -> bool {
+//         pearlite! { true }
+//     }
+
+//     #[predicate]
+//     #[open]
+//     fn into_iter_post(self, res: Self::IntoIter) -> bool {
+//         pearlite! { self@ == res@@ }
+//     }
+// }
+
 impl<T: DeepModel, A: Allocator> DeepModel for VecDeque<T, A> {
     type DeepModelTy = Seq<T::DeepModelTy>;
 

creusot-contracts/src/std/ops.rs

@@ -247,12 +247,12 @@ extern_spec! {
 extern_spec! {
     mod std {
         mod ops {
-            trait IndexMut<Idx>  {
+            trait IndexMut<Idx> where Self : ?Sized  {
                 #[requires(false)]
                 fn index_mut(&mut self, _ix : Idx) -> &mut Self::Output;
             }
 
-            trait Index<Idx> {
+            trait Index<Idx> where Self : ?Sized {
                 #[requires(false)]
                 fn index(&self, _ix : Idx) -> &Self::Output;
             }

creusot-contracts/src/std/slice.rs

@@ -231,6 +231,11 @@ impl<T> SliceIndex<[T]> for RangeToInclusive<usize> {
 
 extern_spec! {
     impl<T> [T] {
+        #[requires([email protected]() == [email protected]())]
+        #[ensures((^self)@ == src@)]
+        fn copy_from_slice(&mut self, src: &[T])
+            where T : Copy;
+
         #[ensures([email protected]() == result@)]
         fn len(&self) -> usize;
 

creusot/tests/should_succeed/bug/217.mlcfg

@@ -17,7 +17,7 @@ module CreusotContracts_Logic_Seq_Impl0_Tail
   use seq.Seq
   use seq_ext.SeqExt
   function tail (self : Seq.seq t) : Seq.seq t =
-    [#"../../../../../creusot-contracts/src/logic/seq.rs" 47 8 47 39] SeqExt.subsequence self 1 (Seq.length self)
+    [#"../../../../../creusot-contracts/src/logic/seq.rs" 49 8 49 39] SeqExt.subsequence self 1 (Seq.length self)
   val tail (self : Seq.seq t) : Seq.seq t
     ensures { result = tail self }
 

creusot/tests/should_succeed/heapsort_generic.mlcfg

@@ -1082,7 +1082,7 @@ module CreusotContracts_Logic_Seq_Impl0_PermutationOf
   use seq.Seq
   use seq.Permut
   predicate permutation_of (self : Seq.seq t) (o : Seq.seq t) =
-    [#"../../../../creusot-contracts/src/logic/seq.rs" 101 8 101 37] Permut.permut self o 0 (Seq.length self)
+    [#"../../../../creusot-contracts/src/logic/seq.rs" 103 8 103 37] Permut.permut self o 0 (Seq.length self)
   val permutation_of (self : Seq.seq t) (o : Seq.seq t) : bool
     ensures { result = permutation_of self o }
 
@@ -1490,10 +1490,10 @@ module Core_Slice_Impl0_Swap_Interface
     type t = slice t,
     type ShallowModelTy0.shallowModelTy = Seq.seq t
   val swap (self : borrowed (slice t)) (a : usize) (b : usize) : ()
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 237 19 237 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 238 19 238 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 242 19 242 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 243 19 243 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 239 8 239 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 244 8 244 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
 
 end
 module CreusotContracts_Std1_Slice_Impl5_InBounds_Stub

creusot/tests/should_succeed/hillel.mlcfg

@@ -1323,7 +1323,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" 378 12 378 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" 383 12 383 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 }
 
@@ -1433,7 +1433,7 @@ module Core_Slice_Impl0_Iter_Interface
     type t = slice t
   val iter (self : slice t) : Core_Slice_Iter_Iter_Type.t_iter t
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] ShallowModel0.shallow_model result = self }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] ShallowModel0.shallow_model result = self }
 
 end
 module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPre_Stub
@@ -1534,7 +1534,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" 371 20 371 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty 
+    [#"../../../../creusot-contracts/src/std/slice.rs" 376 20 376 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 }
 
@@ -1641,10 +1641,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" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 389 14 389 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" 384 14 384 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" 389 14 389 39] Produces0.produces a (Seq.empty ) a
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
   type t
@@ -1653,12 +1653,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" 382 4 382 10] ()
+    [#"../../../../creusot-contracts/src/std/slice.rs" 387 4 387 10] ()
   val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 389 14 389 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" 384 14 384 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" 389 14 389 39] Produces0.produces a (Seq.empty ) a
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Stub
   type t
@@ -1680,12 +1680,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" 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 }
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c}
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 396 14 396 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" 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)
+  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" 394 15 394 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
   type t
@@ -1697,14 +1697,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" 387 4 387 10] ()
+    [#"../../../../creusot-contracts/src/std/slice.rs" 392 4 392 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" 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 }
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c}
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 396 14 396 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" 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)
+  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" 394 15 394 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module Hillel_InsertUnique_Interface
   type t
@@ -2209,7 +2209,7 @@ module CreusotContracts_Logic_Seq_Impl0_New
   type t
   use seq.Seq
   function new (_1 : ()) : Seq.seq t =
-    [#"../../../../creusot-contracts/src/logic/seq.rs" 15 8 15 19] Seq.empty 
+    [#"../../../../creusot-contracts/src/logic/seq.rs" 17 8 17 19] Seq.empty 
   val new (_1 : ()) : Seq.seq t
     ensures { result = new _1 }
 
@@ -2335,7 +2335,7 @@ module Core_Slice_Impl0_Len_Interface
     type t = slice t
   val len (self : slice t) : usize
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
 
 end
 module CreusotContracts_Std1_Iter_Iterator_Completed_Stub
@@ -3257,7 +3257,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" 330 20 330 24] true
+    [#"../../../../creusot-contracts/src/std/slice.rs" 335 20 335 24] true
   val into_iter_pre (self : slice t) : bool
     ensures { result = into_iter_pre self }
 
@@ -3287,7 +3287,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" 336 20 336 32] self = ShallowModel0.shallow_model res
+    [#"../../../../creusot-contracts/src/std/slice.rs" 341 20 341 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

@@ -665,7 +665,7 @@ module Core_Slice_Impl0_Len_Interface
     type t = slice t
   val len (self : slice t) : usize
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
 
 end
 module Alloc_Vec_Impl8_Deref_Interface
@@ -726,8 +726,8 @@ module Core_Slice_Impl0_Get_Interface
   val get (self : slice t) (index : i) : Core_Option_Option_Type.t_option Output0.output
     requires {Inv0.inv self}
     requires {Inv1.inv index}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 242 8 242 102] InBounds0.in_bounds index (ShallowModel0.shallow_model self) -> (exists r : Output0.output . Inv2.inv r /\ result = Core_Option_Option_Type.C_Some r /\ HasValue0.has_value index (ShallowModel0.shallow_model self) r) }
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 243 18 243 55] InBounds0.in_bounds index (ShallowModel0.shallow_model self) \/ result = Core_Option_Option_Type.C_None }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 247 8 247 102] InBounds0.in_bounds index (ShallowModel0.shallow_model self) -> (exists r : Output0.output . Inv2.inv r /\ result = Core_Option_Option_Type.C_Some r /\ HasValue0.has_value index (ShallowModel0.shallow_model self) r) }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 248 18 248 55] InBounds0.in_bounds index (ShallowModel0.shallow_model self) \/ result = Core_Option_Option_Type.C_None }
     ensures { Inv3.inv result }
 
 end