From 00705bba68fed61d3b0bcde2c5fe0ecc83880870 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 18:37:07 +0100
Subject: Update the failing proofs

---
 backends/fstar/Primitives.fst             | 18 +++++++++++++++++-
 backends/lean/Base/Primitives/Vec.lean    | 26 ++++++++++++++++++++++----
 backends/lean/Base/Progress/Progress.lean |  2 +-
 3 files changed, 40 insertions(+), 6 deletions(-)

(limited to 'backends')

diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index 71d75c11..3297803c 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -427,7 +427,7 @@ let alloc_vec_Vec_new (a  : Type0) : alloc_vec_Vec a = assert_norm(length #a []
 let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v
 
 // Helper
-let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result a =
+let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a =
   if i < length v then Return (index v i) else Fail Failure
 // Helper
 let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
@@ -704,6 +704,22 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
 
 (*** Theorems *)
 
+let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
+  Lemma (
+    alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i ==
+      alloc_vec_Vec_index_usize v i)
+  [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)]
+  =
+  admit()
+
+let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
+  Lemma (
+    alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i ==
+      alloc_vec_Vec_index_usize v i)
+  [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)]
+  =
+  admit()
+
 let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
   Lemma (
     alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x ==
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index e1b7e87b..bbed6082 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -81,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_usize (α : 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
@@ -94,13 +94,13 @@ def Vec.index_usize (α : Type u) (v: Vec α) (i: Usize) : Result α :=
 @[pspec]
 theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by
+  ∃ 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 [*]
 
-def Vec.update_usize (α : 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 _ =>
@@ -109,7 +109,7 @@ def Vec.update_usize (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec
 @[pspec]
 theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.update_usize α i x = ret nv ∧
+  ∃ nv, v.update_usize i x = ret nv ∧
   nv.val = v.val.update i.val x
   := by
   simp only [update_usize]
@@ -151,6 +151,24 @@ def Vec.coreopsindexIndexMutInst (T I : Type)
   index_mut_back := Vec.index_mut_back T I inst
 }
 
+@[simp]
+theorem Vec.index_slice_index {α : Type} (v : Vec α) (i : Usize) :
+  Vec.index α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i =
+  Vec.index_usize v i :=
+  sorry
+
+@[simp]
+theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) :
+  Vec.index_mut α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i =
+  Vec.index_usize v i :=
+  sorry
+
+@[simp]
+theorem Vec.index_mut_back_slice_index {α : Type} (v : Vec α) (i : Usize) (x : α) :
+  Vec.index_mut_back α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i x =
+  Vec.update_usize v i x :=
+  sorry
+
 end alloc.vec
 
 end Primitives
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 24c6f912..ba63f09d 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -409,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.update_usize α i x = ret nv ∧
+    ∃ nv, v.update_usize i x = ret nv ∧
     nv.val = v.val.update i.val x := by
     progress
     simp [*]
-- 
cgit v1.2.3