summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst4
-rw-r--r--tests/fstar/hashmap/Hashmap.FunsExternal.fsti8
-rw-r--r--tests/fstar/hashmap/Hashmap.Properties.fst8
3 files changed, 10 insertions, 10 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index a85be4ed..0e991720 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -380,9 +380,9 @@ let hashMap_remove
Source: 'tests/src/hashmap.rs', lines 335:0-335:43 *)
let insert_on_disk
(key : usize) (value : u64) (st : state) : result (state & unit) =
- let* (st1, hm) = hashmap_utils_deserialize st in
+ let* (st1, hm) = utils_deserialize st in
let* hm1 = hashMap_insert u64 hm key value in
- hashmap_utils_serialize hm1 st1
+ utils_serialize hm1 st1
(** [hashmap::test1]:
Source: 'tests/src/hashmap.rs', lines 350:0-350:10 *)
diff --git a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti
index 6e3964c7..f2f305e6 100644
--- a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti
+++ b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti
@@ -6,11 +6,11 @@ include Hashmap.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [hashmap::hashmap_utils::deserialize]:
+(** [hashmap::utils::deserialize]:
Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *)
-val hashmap_utils_deserialize : state -> result (state & (hashMap_t u64))
+val utils_deserialize : state -> result (state & (hashMap_t u64))
-(** [hashmap::hashmap_utils::serialize]:
+(** [hashmap::utils::serialize]:
Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *)
-val hashmap_utils_serialize : hashMap_t u64 -> state -> result (state & unit)
+val utils_serialize : hashMap_t u64 -> state -> result (state & unit)
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 *)