Merge branch 'main' into afromher_shifts

1 files changed, 10 insertions, 10 deletions

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 = ()