From 2b40c5c3de1ee2caca2c0072f812fea04b5a0238 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 14:59:10 +0200
Subject: tests: Merge the hashmap test files

---
 tests/fstar/hashmap/Hashmap.Properties.fst | 48 ++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 tests/fstar/hashmap/Hashmap.Properties.fst

(limited to 'tests/fstar/hashmap/Hashmap.Properties.fst')

diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
new file mode 100644
index 00000000..0d6372c1
--- /dev/null
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -0,0 +1,48 @@
+(** Properties about the hashmap written on disk *)
+module Hashmap.Properties
+open Primitives
+open Hashmap.Funs
+
+#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+
+/// Below, we focus on the functions to read from disk/write to disk to showcase
+/// how such reasoning which mixes opaque functions together with a state-error
+/// monad can be performed.
+
+(*** Hypotheses *)
+
+/// [state_v] gives us the hash map currently stored on disk
+assume
+val state_v : state -> hashMap_t u64
+
+/// [serialize] updates the hash map stored on disk
+assume
+val serialize_lem (hm : hashMap_t u64) (st : state) : Lemma (
+  match hashmap_utils_serialize hm st with
+  | Fail _ -> True
+  | Ok (st', ()) -> state_v st' == hm)
+  [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 st with
+  | Fail _ -> True
+  | Ok (st', hm) -> hm == state_v st /\ st' == 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_lem (key : usize) (value : u64) (st : state) : Lemma (
+  match insert_on_disk key value st with
+  | Fail _ -> True
+  | Ok (st', ()) ->
+    let hm = state_v st in
+    match hashMap_insert u64 hm key value with
+    | Fail _ -> False
+    | Ok hm' -> hm' == state_v st')
+
+let insert_on_disk_lem key value st = ()
-- 
cgit v1.2.3


From c4d2af051c18c4c81b1e57a45210c37c89c8330f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 May 2024 11:18:35 +0200
Subject: tests: Rename hashmap_utils -> utils

---
 tests/fstar/hashmap/Hashmap.Properties.fst | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tests/fstar/hashmap/Hashmap.Properties.fst')

diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index 0d6372c1..ed118c46 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -18,18 +18,18 @@ val state_v : state -> hashMap_t u64
 /// [serialize] updates the hash map stored on disk
 assume
 val serialize_lem (hm : hashMap_t u64) (st : state) : Lemma (
-  match hashmap_utils_serialize hm st with
+  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 *)
 
-- 
cgit v1.2.3