From 9882fc2f9ac5ce0b265de9f771319a6045704abc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 11 Apr 2024 19:51:08 +0200
Subject: Fix some F* proofs

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

(limited to 'tests')

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 = ()
-- 
cgit v1.2.3