Merge pull request #213 from AeneasVerif/cleanup-tests

1 files changed, 9 insertions, 9 deletions

diff --git a/tests/fstar/hashmap_main/HashmapMain.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index beb3dc2c..ed118c46 100644
--- a/tests/fstar/hashmap_main/HashmapMain.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -1,7 +1,7 @@
 (** Properties about the hashmap written on disk *)
-module HashmapMain.Properties
+module Hashmap.Properties
 open Primitives
-open HashmapMain.Funs
+open Hashmap.Funs
 
 #set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
 
@@ -13,23 +13,23 @@ open HashmapMain.Funs
 
 /// [state_v] gives us the hash map currently stored on disk
 assume
-val state_v : state -> hashmap_HashMap_t u64
+val state_v : state -> hashMap_t u64
 
 /// [serialize] updates the hash map stored on disk
 assume
-val serialize_lem (hm : hashmap_HashMap_t u64) (st : state) : Lemma (
-  match hashmap_utils_serialize hm st with
+val serialize_lem (hm : hashMap_t u64) (st : state) : Lemma (
+  match utils_serialize hm st with
   | Fail _ -> True
   | Ok (st', ()) -> state_v st' == hm)
-  [SMTPat (hashmap_utils_serialize hm st)]
+  [SMTPat (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 st with
+  match utils_deserialize st with
   | Fail _ -> True
   | Ok (st', hm) -> hm == state_v st /\ st' == st)
-  [SMTPat (hashmap_utils_deserialize st)]
+  [SMTPat (utils_deserialize st)]
 
 (*** Lemmas *)
 
@@ -41,7 +41,7 @@ val insert_on_disk_lem (key : usize) (value : u64) (st : state) : Lemma (
   | Fail _ -> True
   | Ok (st', ()) ->
     let hm = state_v st in
-    match hashmap_HashMap_insert u64 hm key value with
+    match hashMap_insert u64 hm key value with
     | Fail _ -> False
     | Ok hm' -> hm' == state_v st')