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

---
 .../fstar/hashmap_on_disk/HashmapMain.Properties.fst | 20 ++++++++++----------
 tests/fstar/hashmap_on_disk/Primitives.fst           | 18 +++++++++++++++++-
 2 files changed, 27 insertions(+), 11 deletions(-)

(limited to 'tests/fstar/hashmap_on_disk')

diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
index 106fe05a..358df29e 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
@@ -13,36 +13,36 @@ open HashmapMain.Funs
 
 /// [state_v] gives us the hash map currently stored on disk
 assume
-val state_v : state -> hashmap_hash_map_t u64
+val state_v : state -> hashmap_HashMap_t u64
 
 /// [serialize] updates the hash map stored on disk
 assume
-val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma (
-  match hashmap_utils_serialize_fwd hm st with
+val serialize_lem (hm : hashmap_HashMap_t u64) (st : state) : Lemma (
+  match hashmap_utils_serialize hm st with
   | Fail _ -> True
   | Return (st', ()) -> state_v st' == hm)
-  [SMTPat (hashmap_utils_serialize_fwd hm st)]
+  [SMTPat (hashmap_utils_serialize hm st)]
 
 /// [deserialize] gives us the hash map stored on disk, without updating it
 assume
 val deserialize_lem (st : state) : Lemma (
-  match hashmap_utils_deserialize_fwd st with
+  match hashmap_utils_deserialize st with
   | Fail _ -> True
   | Return (st', hm) -> hm == state_v st /\ st' == st)
-  [SMTPat (hashmap_utils_deserialize_fwd st)]
+  [SMTPat (hashmap_utils_deserialize st)]
 
 (*** Lemmas *)
 
 /// The obvious lemma about [insert_on_disk]: the updated hash map stored on disk
 /// is exactly the hash map produced from inserting the binding ([key], [value])
 /// in the hash map previously stored on disk.
-val insert_on_disk_fwd_lem (key : usize) (value : u64) (st : state) : Lemma (
-  match insert_on_disk_fwd key value st with
+val insert_on_disk_lem (key : usize) (value : u64) (st : state) : Lemma (
+  match insert_on_disk key value st with
   | Fail _ -> True
   | Return (st', ()) ->
     let hm = state_v st in
-    match hashmap_hash_map_insert_fwd_back u64 hm key value with
+    match hashmap_HashMap_insert u64 hm key value with
     | Fail _ -> False
     | Return hm' -> hm' == state_v st')
 
-let insert_on_disk_fwd_lem key value st = ()
+let insert_on_disk_lem key value st = ()
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index 71d75c11..3297803c 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/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 ==
-- 
cgit v1.2.3