diff options
| author | Son HO | 2024-04-11 20:32:15 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-11 20:32:15 +0200 |
| commit | 77d74452489f85f558efe07d72d0200c80b16444 (patch) | |
| tree | 810c6504b8e5b2fcde58841e25079d5e8c8e92ae /tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst | |
| parent | 4fb9c9f655a9ffc3b4a1a717988311c057c9c599 (diff) | |
| parent | 2f8aa9b47acb5c98aed91c29b04f71099452e781 (diff) | |
Merge pull request #123 from AeneasVerif/son/clean
Cleanup the code in preparation of the nested loops
Diffstat (limited to 'tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst')
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst | 8 |
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 = () |