diff options
| author | Nadrieril | 2024-05-28 11:18:35 +0200 |
|---|---|---|
| committer | Nadrieril | 2024-05-28 11:36:31 +0200 |
| commit | c4d2af051c18c4c81b1e57a45210c37c89c8330f (patch) | |
| tree | a72fae46702fc4c2eb32e1361a2538eb7a5f5545 /tests/fstar/hashmap/Hashmap.Properties.fst | |
| parent | c81c96f20b1dbf428a9ed42e83b910e798e1a225 (diff) | |
tests: Rename hashmap_utils -> utils
Diffstat (limited to 'tests/fstar/hashmap/Hashmap.Properties.fst')
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Properties.fst | 8 |
1 files changed, 4 insertions, 4 deletions
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 *) |