summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
authorSon Ho2024-04-11 19:51:08 +0200
committerSon Ho2024-04-11 19:51:08 +0200
commit9882fc2f9ac5ce0b265de9f771319a6045704abc (patch)
tree24d36462905bcd97bfb39939cb81807293fccab1 /tests/fstar
parent86c3680b1f3f50b4c4e6198eebc145cadfff3876 (diff)
Fix some F* proofs
Diffstat (limited to '')
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst8
1 files changed, 4 insertions, 4 deletions
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
index 358df29e..beb3dc2c 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
@@ -20,7 +20,7 @@ assume
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)
+ | Ok (st', ()) -> state_v st' == hm)
[SMTPat (hashmap_utils_serialize hm st)]
/// [deserialize] gives us the hash map stored on disk, without updating it
@@ -28,7 +28,7 @@ assume
val deserialize_lem (st : state) : Lemma (
match hashmap_utils_deserialize st with
| Fail _ -> True
- | Return (st', hm) -> hm == state_v st /\ st' == st)
+ | Ok (st', hm) -> hm == state_v st /\ st' == st)
[SMTPat (hashmap_utils_deserialize st)]
(*** Lemmas *)
@@ -39,10 +39,10 @@ val deserialize_lem (st : state) : Lemma (
val insert_on_disk_lem (key : usize) (value : u64) (st : state) : Lemma (
match insert_on_disk key value st with
| Fail _ -> True
- | Return (st', ()) ->
+ | Ok (st', ()) ->
let hm = state_v st in
match hashmap_HashMap_insert u64 hm key value with
| Fail _ -> False
- | Return hm' -> hm' == state_v st')
+ | Ok hm' -> hm' == state_v st')
let insert_on_disk_lem key value st = ()