4 files changed, 107 insertions, 33 deletions
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 47807a0d..615e0783 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -13,7 +13,7 @@ import Base.Progress.Base
 
 namespace Primitives
 
-open Result Error
+open Result Error core.ops.range
 
 def Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val }
 
@@ -406,7 +406,7 @@ structure core.slice.index.private_slice_index.Sealed (Self : Type) where
 
 /- Trait declaration: [core::slice::index::SliceIndex] -/
 structure core.slice.index.SliceIndex (Self T0 : Type) where
-  sealedInst :core.slice.index.private_slice_index.Sealed Self
+  sealedInst : core.slice.index.private_slice_index.Sealed Self
   Output : Type
   get : Self → T0 → Result (Option Output)
   get_mut : Self → T0 → Result (Option Output)
@@ -557,4 +557,61 @@ def core.array.Array.coreopsindexIndexMutInst (T0 I : Type) (N : Usize)
   index_mut_back := core.array.Array.index_mut_back T0 I N inst
 }
 
+/- [core::slice::index::usize::get]: forward function -/
+def core.slice.index.Usize.get
+  (T : Type) : Usize → Slice T → Result (Option T) :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::get_mut]: forward function -/
+def core.slice.index.Usize.get_mut
+  (T : Type) : Usize → Slice T → Result (Option T) :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::get_mut]: backward function 0 -/
+def core.slice.index.Usize.get_mut_back
+  (T : Type) : Usize → Slice T → Option T → Result (Slice T) :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::get_unchecked]: forward function -/
+def core.slice.index.Usize.get_unchecked
+  (T : Type) : Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr T) :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::get_unchecked_mut]: forward function -/
+def core.slice.index.Usize.get_unchecked_mut
+  (T : Type) : Usize → MutRawPtr (Slice T) → Result (MutRawPtr T) :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::index]: forward function -/
+def core.slice.index.Usize.index (T : Type) : Usize → Slice T → Result T :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::index_mut]: forward function -/
+def core.slice.index.Usize.index_mut (T : Type) : Usize → Slice T → Result T :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::index_mut]: backward function 0 -/
+def core.slice.index.Usize.index_mut_back
+  (T : Type) : Usize → Slice T → T → Result (Slice T) :=
+  sorry -- TODO
+
+/- Trait implementation: [core::slice::index::private_slice_index::usize] -/
+def core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+  : core.slice.index.private_slice_index.Sealed Usize := {}
+
+/- Trait implementation: [core::slice::index::usize] -/
+def core.slice.index.usize.coresliceindexSliceIndexInst (T : Type) :
+  core.slice.index.SliceIndex Usize (Slice T) := {
+  sealedInst := core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+  Output := T
+  get := core.slice.index.Usize.get T
+  get_mut := core.slice.index.Usize.get_mut T
+  get_mut_back := core.slice.index.Usize.get_mut_back T
+  get_unchecked := core.slice.index.Usize.get_unchecked T
+  get_unchecked_mut := core.slice.index.Usize.get_unchecked_mut T
+  index := core.slice.index.Usize.index T
+  index_mut := core.slice.index.Usize.index_mut T
+  index_mut_back := core.slice.index.Usize.index_mut_back T
+}
+
 end Primitives
diff --git a/backends/lean/Base/Primitives/Range.lean b/backends/lean/Base/Primitives/Range.lean
index 26cbee42..a268bcba 100644
--- a/backends/lean/Base/Primitives/Range.lean
+++ b/backends/lean/Base/Primitives/Range.lean
@@ -11,7 +11,7 @@ import Base.Progress.Base
 
 namespace Primitives
 
-structure Range (α : Type u) where
+structure core.ops.range.Range (α : Type u) where
   mk ::
   start: α
   end_: α
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 99fcedc6..e1b7e87b 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -14,6 +14,8 @@ namespace Primitives
 
 open Result Error
 
+namespace alloc.vec
+
 def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max }
 
 instance (a : Type u) : Arith.HasIntProp (Vec a) where
@@ -79,7 +81,7 @@ theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
   ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
   simp [insert, *]
 
-def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α :=
+def Vec.index_usize (α : Type u) (v: Vec α) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some x => ret x
@@ -90,51 +92,65 @@ def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α :=
  -/
 
 @[pspec]
-theorem Vec.index_shared_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_shared α i = ret x ∧ x = v.val.index i.val := by
-  simp only [index_shared]
+  ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by
+  simp only [index_usize]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
   simp [*]
 
--- This shouldn't be used
-def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
-  if i.val < List.length v.val then
-    .ret ()
-  else
-    .fail arrayOutOfBounds
-
-def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α :=
-  match v.val.indexOpt i.val with
-  | none => fail .arrayOutOfBounds
-  | some x => ret x
-
-@[pspec]
-theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
-  (hbound : i.val < v.length) :
-  ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by
-  simp only [index_mut]
-  -- TODO: dependent rewrite
-  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
-  simp [*]
-
-def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+def Vec.update_usize (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
     .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
-theorem Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
+theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.index_mut_back α i x = ret nv ∧
+  ∃ nv, v.update_usize α i x = ret nv ∧
   nv.val = v.val.update i.val x
   := by
-  simp only [index_mut_back]
+  simp only [update_usize]
   have h := List.indexOpt_bounds v.val i.val
   split
   . simp_all [length]; cases h <;> scalar_tac
   . simp_all
 
+/- [alloc::vec::Vec::index]: forward function -/
+def Vec.index (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+  (self : Vec T) (i : I) : Result inst.Output :=
+  sorry -- TODO
+
+/- [alloc::vec::Vec::index_mut]: forward function -/
+def Vec.index_mut (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+  (self : Vec T) (i : I) : Result inst.Output :=
+  sorry -- TODO
+
+/- [alloc::vec::Vec::index_mut]: backward function 0 -/
+def Vec.index_mut_back
+  (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+  (self : Vec T) (i : I) (x : inst.Output) : Result (alloc.vec.Vec T) :=
+  sorry -- TODO
+
+/- Trait implementation: [alloc::vec::Vec] -/
+def Vec.coreopsindexIndexInst (T I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T)) :
+  core.ops.index.Index (alloc.vec.Vec T) I := {
+  Output := inst.Output
+  index := Vec.index T I inst
+}
+
+/- Trait implementation: [alloc::vec::Vec] -/
+def Vec.coreopsindexIndexMutInst (T I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T)) :
+  core.ops.index.IndexMut (alloc.vec.Vec T) I := {
+  indexInst := Vec.coreopsindexIndexInst T I inst
+  index_mut := Vec.index_mut T I inst
+  index_mut_back := Vec.index_mut_back T I inst
+}
+
+end alloc.vec
+
 end Primitives
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index ecf05dab..24c6f912 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -383,6 +383,7 @@ namespace Test
   -- #eval showStoredPSpec
   -- #eval showStoredPSpecClass
   -- #eval showStoredPSpecExprClass
+  open alloc.vec
 
   example {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
@@ -408,7 +409,7 @@ namespace Test
      `α : Type u` where u is quantified, while here we use `α : Type 0` -/
   example {α : Type} (v: Vec α) (i: Usize) (x : α)
     (hbounds : i.val < v.length) :
-    ∃ nv, v.index_mut_back α i x = ret nv ∧
+    ∃ nv, v.update_usize α i x = ret nv ∧
     nv.val = v.val.update i.val x := by
     progress
     simp [*]