From bb94d52be2d0ddb317577dc3cd468754646e4b64 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 5 May 2022 17:12:02 +0200
Subject: Update the hashmap_on_disk example
---
.../HashmapMain.Clauses.Template.fst | 18 +-
tests/hashmap_on_disk/HashmapMain.Clauses.fst | 18 +-
tests/hashmap_on_disk/HashmapMain.Funs.fst | 712 +++++++--------------
tests/hashmap_on_disk/HashmapMain.Properties.fst | 263 +-------
4 files changed, 240 insertions(+), 771 deletions(-)
(limited to 'tests/hashmap_on_disk')
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index f3b4d6db..6179e6b2 100644
--- a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -9,55 +9,55 @@ open HashmapMain.Types
(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: decreases clause *)
unfold
let hashmap_hash_map_allocate_slots_decreases (t : Type0)
- (slots : vec (hashmap_list_t t)) (n : usize) (st : state) : nat =
+ (slots : vec (hashmap_list_t t)) (n : usize) : nat =
admit ()
(** [hashmap_main::hashmap::HashMap::{0}::clear_slots]: decreases clause *)
unfold
let hashmap_hash_map_clear_slots_decreases (t : Type0)
- (slots : vec (hashmap_list_t t)) (i : usize) (st : state) : nat =
+ (slots : vec (hashmap_list_t t)) (i : usize) : nat =
admit ()
(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: decreases clause *)
unfold
let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize)
- (value : t) (ls : hashmap_list_t t) (st : state) : nat =
+ (value : t) (ls : hashmap_list_t t) : nat =
admit ()
(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *)
unfold
let hashmap_hash_map_move_elements_from_list_decreases (t : Type0)
- (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) (st : state) : nat =
+ (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : nat =
admit ()
(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: decreases clause *)
unfold
let hashmap_hash_map_move_elements_decreases (t : Type0)
(ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) (i : usize)
- (st : state) : nat =
+ : nat =
admit ()
(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: decreases clause *)
unfold
let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (key : usize)
- (ls : hashmap_list_t t) (st : state) : nat =
+ (ls : hashmap_list_t t) : nat =
admit ()
(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: decreases clause *)
unfold
let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize)
- (ls : hashmap_list_t t) (st : state) : nat =
+ (ls : hashmap_list_t t) : nat =
admit ()
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
unfold
let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
- (ls : hashmap_list_t t) (st : state) : nat =
+ (ls : hashmap_list_t t) : nat =
admit ()
(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
unfold
let hashmap_hash_map_remove_from_list_decreases (t : Type0) (key : usize)
- (ls : hashmap_list_t t) (st : state) : nat =
+ (ls : hashmap_list_t t) : nat =
admit ()
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.fst
index 84e6494a..b864e32a 100644
--- a/tests/hashmap_on_disk/HashmapMain.Clauses.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Clauses.fst
@@ -9,53 +9,53 @@ open HashmapMain.Types
(** [hashmap::HashMap::allocate_slots]: decreases clause *)
unfold
let hashmap_hash_map_allocate_slots_decreases (t : Type0) (slots : vec (hashmap_list_t t))
- (n : usize) (st : state) : nat = n
+ (n : usize) : nat = n
(** [hashmap::HashMap::clear_slots]: decreases clause *)
unfold
let hashmap_hash_map_clear_slots_decreases (t : Type0) (slots : vec (hashmap_list_t t))
- (i : usize) (st : state) : nat =
+ (i : usize) : nat =
if i < length slots then length slots - i else 0
(** [hashmap::HashMap::insert_in_list]: decreases clause *)
unfold
let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t)
- (ls : hashmap_list_t t) (st : state) : hashmap_list_t t =
+ (ls : hashmap_list_t t) : hashmap_list_t t =
ls
(** [hashmap::HashMap::move_elements_from_list]: decreases clause *)
unfold
let hashmap_hash_map_move_elements_from_list_decreases (t : Type0)
- (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) (st : state) : hashmap_list_t t =
+ (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : hashmap_list_t t =
ls
(** [hashmap::HashMap::move_elements]: decreases clause *)
unfold
let hashmap_hash_map_move_elements_decreases (t : Type0) (ntable : hashmap_hash_map_t t)
- (slots : vec (hashmap_list_t t)) (i : usize) (st : state) : nat =
+ (slots : vec (hashmap_list_t t)) (i : usize) : nat =
if i < length slots then length slots - i else 0
(** [hashmap::HashMap::contains_key_in_list]: decreases clause *)
unfold
let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (key : usize)
- (ls : hashmap_list_t t) (st : state) : hashmap_list_t t =
+ (ls : hashmap_list_t t) : hashmap_list_t t =
ls
(** [hashmap::HashMap::get_in_list]: decreases clause *)
unfold
-let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
+let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) :
hashmap_list_t t =
ls
(** [hashmap::HashMap::get_mut_in_list]: decreases clause *)
unfold
let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
- (ls : hashmap_list_t t) (st : state) : hashmap_list_t t =
+ (ls : hashmap_list_t t) : hashmap_list_t t =
ls
(** [hashmap::HashMap::remove_from_list]: decreases clause *)
unfold
let hashmap_hash_map_remove_from_list_decreases (t : Type0) (key : usize)
- (ls : hashmap_list_t t) (st : state) : hashmap_list_t t =
+ (ls : hashmap_list_t t) : hashmap_list_t t =
ls
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index 1b281acb..4177f77d 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -9,17 +9,16 @@ include HashmapMain.Clauses
#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
(** [hashmap_main::hashmap::hash_key] *)
-let hashmap_hash_key_fwd (k : usize) (st : state) : result (state & usize) =
- Return (st, k)
+let hashmap_hash_key_fwd (k : usize) : result usize = Return k
(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
let rec hashmap_hash_map_allocate_slots_fwd
- (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) (st : state) :
- Tot (result (state & (vec (hashmap_list_t t))))
- (decreases (hashmap_hash_map_allocate_slots_decreases t slots n st))
+ (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) :
+ Tot (result (vec (hashmap_list_t t)))
+ (decreases (hashmap_hash_map_allocate_slots_decreases t slots n))
=
begin match n with
- | 0 -> Return (st, slots)
+ | 0 -> Return slots
| _ ->
begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
| Fail -> Fail
@@ -27,9 +26,9 @@ let rec hashmap_hash_map_allocate_slots_fwd
begin match usize_sub n 1 with
| Fail -> Fail
| Return i ->
- begin match hashmap_hash_map_allocate_slots_fwd t slots0 i st with
+ begin match hashmap_hash_map_allocate_slots_fwd t slots0 i with
| Fail -> Fail
- | Return (st0, v) -> Return (st0, v)
+ | Return v -> Return v
end
end
end
@@ -38,62 +37,37 @@ let rec hashmap_hash_map_allocate_slots_fwd
(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
let hashmap_hash_map_new_with_capacity_fwd
(t : Type0) (capacity : usize) (max_load_dividend : usize)
- (max_load_divisor : usize) (st : state) :
- result (state & (hashmap_hash_map_t t))
+ (max_load_divisor : usize) :
+ result (hashmap_hash_map_t t)
=
let v = vec_new (hashmap_list_t t) in
- begin match hashmap_hash_map_allocate_slots_fwd t v capacity st with
+ begin match hashmap_hash_map_allocate_slots_fwd t v capacity with
| Fail -> Fail
- | Return (st0, slots) ->
+ | Return slots ->
begin match usize_mul capacity max_load_dividend with
| Fail -> Fail
| Return i ->
begin match usize_div i max_load_divisor with
| Fail -> Fail
| Return i0 ->
- Return (st0, Mkhashmap_hash_map_t 0 (max_load_dividend,
- max_load_divisor) i0 slots)
+ Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0
+ slots)
end
end
end
(** [hashmap_main::hashmap::HashMap::{0}::new] *)
-let hashmap_hash_map_new_fwd
- (t : Type0) (st : state) : result (state & (hashmap_hash_map_t t)) =
- begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 st with
+let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
+ begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 with
| Fail -> Fail
- | Return (st0, hm) -> Return (st0, hm)
+ | Return hm -> Return hm
end
(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-let rec hashmap_hash_map_clear_slots_fwd
- (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) (st : state) :
- Tot (result (state & unit))
- (decreases (hashmap_hash_map_clear_slots_decreases t slots i st))
- =
- let i0 = vec_len (hashmap_list_t t) slots in
- if i < i0
- then
- begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
- with
- | Fail -> Fail
- | Return slots0 ->
- begin match usize_add i 1 with
- | Fail -> Fail
- | Return i1 ->
- begin match hashmap_hash_map_clear_slots_fwd t slots0 i1 st with
- | Fail -> Fail
- | Return (st0, _) -> Return (st0, ())
- end
- end
- end
- else Return (st, ())
-
-(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-let rec hashmap_hash_map_clear_slots_back
- (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) (st : state) :
+let rec hashmap_hash_map_clear_slots_fwd_back
+ (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) :
Tot (result (vec (hashmap_list_t t)))
- (decreases (hashmap_hash_map_clear_slots_decreases t slots i st))
+ (decreases (hashmap_hash_map_clear_slots_decreases t slots i))
=
let i0 = vec_len (hashmap_list_t t) slots in
if i < i0
@@ -105,7 +79,7 @@ let rec hashmap_hash_map_clear_slots_back
begin match usize_add i 1 with
| Fail -> Fail
| Return i1 ->
- begin match hashmap_hash_map_clear_slots_back t slots0 i1 st with
+ begin match hashmap_hash_map_clear_slots_fwd_back t slots0 i1 with
| Fail -> Fail
| Return slots1 -> Return slots1
end
@@ -114,23 +88,10 @@ let rec hashmap_hash_map_clear_slots_back
else Return slots
(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
-let hashmap_hash_map_clear_fwd
- (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
- result (state & unit)
- =
+let hashmap_hash_map_clear_fwd_back
+ (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
begin match
- hashmap_hash_map_clear_slots_fwd t self.hashmap_hash_map_slots 0 st with
- | Fail -> Fail
- | Return (st0, _) -> Return (st0, ())
- end
-
-(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
-let hashmap_hash_map_clear_back
- (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
- result (hashmap_hash_map_t t)
- =
- begin match
- hashmap_hash_map_clear_slots_back t self.hashmap_hash_map_slots 0 st with
+ hashmap_hash_map_clear_slots_fwd_back t self.hashmap_hash_map_slots 0 with
| Fail -> Fail
| Return v ->
Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
@@ -139,41 +100,39 @@ let hashmap_hash_map_clear_back
(** [hashmap_main::hashmap::HashMap::{0}::len] *)
let hashmap_hash_map_len_fwd
- (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
- result (state & usize)
- =
- Return (st, self.hashmap_hash_map_num_entries)
+ (t : Type0) (self : hashmap_hash_map_t t) : result usize =
+ Return self.hashmap_hash_map_num_entries
(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
let rec hashmap_hash_map_insert_in_list_fwd
- (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
- Tot (result (state & bool))
- (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
+ (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
+ Tot (result bool)
+ (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls))
=
begin match ls with
| HashmapListCons ckey cvalue ls0 ->
if ckey = key
- then Return (st, false)
+ then Return false
else
- begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 st with
+ begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 with
| Fail -> Fail
- | Return (st0, b) -> Return (st0, b)
+ | Return b -> Return b
end
- | HashmapListNil -> Return (st, true)
+ | HashmapListNil -> Return true
end
(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
let rec hashmap_hash_map_insert_in_list_back
- (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
+ (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
Tot (result (hashmap_list_t t))
- (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
+ (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls))
=
begin match ls with
| HashmapListCons ckey cvalue ls0 ->
if ckey = key
then Return (HashmapListCons ckey value ls0)
else
- begin match hashmap_hash_map_insert_in_list_back t key value ls0 st with
+ begin match hashmap_hash_map_insert_in_list_back t key value ls0 with
| Fail -> Fail
| Return ls1 -> Return (HashmapListCons ckey cvalue ls1)
end
@@ -182,47 +141,13 @@ let rec hashmap_hash_map_insert_in_list_back
end
(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
-let hashmap_hash_map_insert_no_resize_fwd
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
- (st : state) :
- result (state & unit)
- =
- begin match hashmap_hash_key_fwd key st with
- | Fail -> Fail
- | Return (st0, hash) ->
- let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_rem hash i with
- | Fail -> Fail
- | Return hash_mod ->
- begin match
- vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
- hash_mod with
- | Fail -> Fail
- | Return l ->
- begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with
- | Fail -> Fail
- | Return (st1, inserted) ->
- if inserted
- then
- begin match usize_add self.hashmap_hash_map_num_entries 1 with
- | Fail -> Fail
- | Return _ -> Return (st1, ())
- end
- else Return (st1, ())
- end
- end
- end
- end
-
-(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
-let hashmap_hash_map_insert_no_resize_back
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
- (st : state) :
+let hashmap_hash_map_insert_no_resize_fwd_back
+ (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) :
result (hashmap_hash_map_t t)
=
- begin match hashmap_hash_key_fwd key st with
+ begin match hashmap_hash_key_fwd key with
| Fail -> Fail
- | Return (st0, hash) ->
+ | Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
| Fail -> Fail
@@ -232,16 +157,16 @@ let hashmap_hash_map_insert_no_resize_back
hash_mod with
| Fail -> Fail
| Return l ->
- begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with
+ begin match hashmap_hash_map_insert_in_list_fwd t key value l with
| Fail -> Fail
- | Return (_, inserted) ->
+ | Return inserted ->
if inserted
then
begin match usize_add self.hashmap_hash_map_num_entries 1 with
| Fail -> Fail
| Return i0 ->
- begin match
- hashmap_hash_map_insert_in_list_back t key value l st0 with
+ begin match hashmap_hash_map_insert_in_list_back t key value l
+ with
| Fail -> Fail
| Return l0 ->
begin match
@@ -256,8 +181,7 @@ let hashmap_hash_map_insert_no_resize_back
end
end
else
- begin match hashmap_hash_map_insert_in_list_back t key value l st0
- with
+ begin match hashmap_hash_map_insert_in_list_back t key value l with
| Fail -> Fail
| Return l0 ->
begin match
@@ -276,104 +200,31 @@ let hashmap_hash_map_insert_no_resize_back
end
(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
-let rec hashmap_hash_map_move_elements_from_list_fwd
- (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t)
- (st : state) :
- Tot (result (state & unit))
- (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls
- st))
- =
- begin match ls with
- | HashmapListCons k v tl ->
- begin match hashmap_hash_map_insert_no_resize_fwd t ntable k v st with
- | Fail -> Fail
- | Return (st0, _) ->
- begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
- | Fail -> Fail
- | Return ntable0 ->
- begin match
- hashmap_hash_map_move_elements_from_list_fwd t ntable0 tl st0 with
- | Fail -> Fail
- | Return (st1, _) -> Return (st1, ())
- end
- end
- end
- | HashmapListNil -> Return (st, ())
- end
-
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
-let rec hashmap_hash_map_move_elements_from_list_back
- (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t)
- (st : state) :
+let rec hashmap_hash_map_move_elements_from_list_fwd_back
+ (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
Tot (result (hashmap_hash_map_t t))
- (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls
- st))
+ (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls))
=
begin match ls with
| HashmapListCons k v tl ->
- begin match hashmap_hash_map_insert_no_resize_fwd t ntable k v st with
+ begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with
| Fail -> Fail
- | Return (st0, _) ->
- begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
+ | Return ntable0 ->
+ begin match
+ hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl with
| Fail -> Fail
- | Return ntable0 ->
- begin match
- hashmap_hash_map_move_elements_from_list_back t ntable0 tl st0 with
- | Fail -> Fail
- | Return ntable1 -> Return ntable1
- end
+ | Return ntable1 -> Return ntable1
end
end
| HashmapListNil -> Return ntable
end
(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
-let rec hashmap_hash_map_move_elements_fwd
+let rec hashmap_hash_map_move_elements_fwd_back
(t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
- (i : usize) (st : state) :
- Tot (result (state & unit))
- (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st))
- =
- let i0 = vec_len (hashmap_list_t t) slots in
- if i < i0
- then
- begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
- | Fail -> Fail
- | Return l ->
- let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
- begin match hashmap_hash_map_move_elements_from_list_fwd t ntable ls st
- with
- | Fail -> Fail
- | Return (st0, _) ->
- begin match
- hashmap_hash_map_move_elements_from_list_back t ntable ls st with
- | Fail -> Fail
- | Return ntable0 ->
- let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
- begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
- | Fail -> Fail
- | Return slots0 ->
- begin match usize_add i 1 with
- | Fail -> Fail
- | Return i1 ->
- begin match
- hashmap_hash_map_move_elements_fwd t ntable0 slots0 i1 st0 with
- | Fail -> Fail
- | Return (st1, _) -> Return (st1, ())
- end
- end
- end
- end
- end
- end
- else Return (st, ())
-
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
-let rec hashmap_hash_map_move_elements_back
- (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
- (i : usize) (st : state) :
+ (i : usize) :
Tot (result ((hashmap_hash_map_t t) & (vec (hashmap_list_t t))))
- (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st))
+ (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i))
=
let i0 = vec_len (hashmap_list_t t) slots in
if i < i0
@@ -382,27 +233,21 @@ let rec hashmap_hash_map_move_elements_back
| Fail -> Fail
| Return l ->
let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
- begin match hashmap_hash_map_move_elements_from_list_fwd t ntable ls st
+ begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls
with
| Fail -> Fail
- | Return (st0, _) ->
- begin match
- hashmap_hash_map_move_elements_from_list_back t ntable ls st with
+ | Return ntable0 ->
+ let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
+ begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
| Fail -> Fail
- | Return ntable0 ->
- let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
- begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
+ | Return slots0 ->
+ begin match usize_add i 1 with
| Fail -> Fail
- | Return slots0 ->
- begin match usize_add i 1 with
+ | Return i1 ->
+ begin match
+ hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 with
| Fail -> Fail
- | Return i1 ->
- begin match
- hashmap_hash_map_move_elements_back t ntable0 slots0 i1 st0
- with
- | Fail -> Fail
- | Return (ntable1, slots1) -> Return (ntable1, slots1)
- end
+ | Return (ntable1, slots1) -> Return (ntable1, slots1)
end
end
end
@@ -411,49 +256,8 @@ let rec hashmap_hash_map_move_elements_back
else Return (ntable, slots)
(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
-let hashmap_hash_map_try_resize_fwd
- (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
- result (state & unit)
- =
- let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_div 4294967295 2 with
- | Fail -> Fail
- | Return n1 ->
- let (i, i0) = self.hashmap_hash_map_max_load_factor in
- begin match usize_div n1 i with
- | Fail -> Fail
- | Return i1 ->
- if capacity <= i1
- then
- begin match usize_mul capacity 2 with
- | Fail -> Fail
- | Return i2 ->
- begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 st with
- | Fail -> Fail
- | Return (st0, ntable) ->
- begin match
- hashmap_hash_map_move_elements_fwd t ntable
- self.hashmap_hash_map_slots 0 st0 with
- | Fail -> Fail
- | Return (st1, _) ->
- begin match
- hashmap_hash_map_move_elements_back t ntable
- self.hashmap_hash_map_slots 0 st0 with
- | Fail -> Fail
- | Return (_, _) -> Return (st1, ())
- end
- end
- end
- end
- else Return (st, ())
- end
- end
-
-(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
-let hashmap_hash_map_try_resize_back
- (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
- result (hashmap_hash_map_t t)
- =
+let hashmap_hash_map_try_resize_fwd_back
+ (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_div 4294967295 2 with
| Fail -> Fail
@@ -467,12 +271,12 @@ let hashmap_hash_map_try_resize_back
begin match usize_mul capacity 2 with
| Fail -> Fail
| Return i2 ->
- begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 st with
+ begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with
| Fail -> Fail
- | Return (st0, ntable) ->
+ | Return ntable ->
begin match
- hashmap_hash_map_move_elements_back t ntable
- self.hashmap_hash_map_slots 0 st0 with
+ hashmap_hash_map_move_elements_fwd_back t ntable
+ self.hashmap_hash_map_slots 0 with
| Fail -> Fail
| Return (ntable0, _) ->
Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
@@ -488,96 +292,57 @@ let hashmap_hash_map_try_resize_back
end
(** [hashmap_main::hashmap::HashMap::{0}::insert] *)
-let hashmap_hash_map_insert_fwd
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
- (st : state) :
- result (state & unit)
- =
- begin match hashmap_hash_map_insert_no_resize_fwd t self key value st with
- | Fail -> Fail
- | Return (st0, _) ->
- begin match hashmap_hash_map_insert_no_resize_back t self key value st with
- | Fail -> Fail
- | Return self0 ->
- begin match hashmap_hash_map_len_fwd t self0 st0 with
- | Fail -> Fail
- | Return (st1, i) ->
- if i > self0.hashmap_hash_map_max_load
- then
- begin match
- hashmap_hash_map_try_resize_fwd t (Mkhashmap_hash_map_t
- self0.hashmap_hash_map_num_entries
- self0.hashmap_hash_map_max_load_factor
- self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) st1
- with
- | Fail -> Fail
- | Return (st2, _) -> Return (st2, ())
- end
- else Return (st1, ())
- end
- end
- end
-
-(** [hashmap_main::hashmap::HashMap::{0}::insert] *)
-let hashmap_hash_map_insert_back
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
- (st : state) :
+let hashmap_hash_map_insert_fwd_back
+ (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) :
result (hashmap_hash_map_t t)
=
- begin match hashmap_hash_map_insert_no_resize_fwd t self key value st with
+ begin match hashmap_hash_map_insert_no_resize_fwd_back t self key value with
| Fail -> Fail
- | Return (st0, _) ->
- begin match hashmap_hash_map_insert_no_resize_back t self key value st with
+ | Return self0 ->
+ begin match hashmap_hash_map_len_fwd t self0 with
| Fail -> Fail
- | Return self0 ->
- begin match hashmap_hash_map_len_fwd t self0 st0 with
- | Fail -> Fail
- | Return (st1, i) ->
- if i > self0.hashmap_hash_map_max_load
- then
- begin match
- hashmap_hash_map_try_resize_back t (Mkhashmap_hash_map_t
- self0.hashmap_hash_map_num_entries
- self0.hashmap_hash_map_max_load_factor
- self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) st1
- with
- | Fail -> Fail
- | Return self1 -> Return self1
- end
- else
- Return (Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries
+ | Return i ->
+ if i > self0.hashmap_hash_map_max_load
+ then
+ begin match
+ hashmap_hash_map_try_resize_fwd_back t (Mkhashmap_hash_map_t
+ self0.hashmap_hash_map_num_entries
self0.hashmap_hash_map_max_load_factor
- self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
- end
+ self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) with
+ | Fail -> Fail
+ | Return self1 -> Return self1
+ end
+ else
+ Return (Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries
+ self0.hashmap_hash_map_max_load_factor
+ self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
end
end
(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
let rec hashmap_hash_map_contains_key_in_list_fwd
- (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
- Tot (result (state & bool))
- (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls st))
+ (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+ Tot (result bool)
+ (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls))
=
begin match ls with
| HashmapListCons ckey x ls0 ->
if ckey = key
- then Return (st, true)
+ then Return true
else
- begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 st with
+ begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 with
| Fail -> Fail
- | Return (st0, b) -> Return (st0, b)
+ | Return b -> Return b
end
- | HashmapListNil -> Return (st, false)
+ | HashmapListNil -> Return false
end
(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
let hashmap_hash_map_contains_key_fwd
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
- result (state & bool)
- =
- begin match hashmap_hash_key_fwd key st with
+ (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool =
+ begin match hashmap_hash_key_fwd key with
| Fail -> Fail
- | Return (st0, hash) ->
+ | Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
| Fail -> Fail
@@ -587,9 +352,9 @@ let hashmap_hash_map_contains_key_fwd
with
| Fail -> Fail
| Return l ->
- begin match hashmap_hash_map_contains_key_in_list_fwd t key l st0 with
+ begin match hashmap_hash_map_contains_key_in_list_fwd t key l with
| Fail -> Fail
- | Return (st1, b) -> Return (st1, b)
+ | Return b -> Return b
end
end
end
@@ -597,30 +362,27 @@ let hashmap_hash_map_contains_key_fwd
(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
let rec hashmap_hash_map_get_in_list_fwd
- (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
- Tot (result (state & t))
- (decreases (hashmap_hash_map_get_in_list_decreases t key ls st))
+ (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+ Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t key ls))
=
begin match ls with
| HashmapListCons ckey cvalue ls0 ->
if ckey = key
- then Return (st, cvalue)
+ then Return cvalue
else
- begin match hashmap_hash_map_get_in_list_fwd t key ls0 st with
+ begin match hashmap_hash_map_get_in_list_fwd t key ls0 with
| Fail -> Fail
- | Return (st0, x) -> Return (st0, x)
+ | Return x -> Return x
end
| HashmapListNil -> Fail
end
(** [hashmap_main::hashmap::HashMap::{0}::get] *)
let hashmap_hash_map_get_fwd
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
- result (state & t)
- =
- begin match hashmap_hash_key_fwd key st with
+ (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
+ begin match hashmap_hash_key_fwd key with
| Fail -> Fail
- | Return (st0, hash) ->
+ | Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
| Fail -> Fail
@@ -630,9 +392,9 @@ let hashmap_hash_map_get_fwd
with
| Fail -> Fail
| Return l ->
- begin match hashmap_hash_map_get_in_list_fwd t key l st0 with
+ begin match hashmap_hash_map_get_in_list_fwd t key l with
| Fail -> Fail
- | Return (st1, x) -> Return (st1, x)
+ | Return x -> Return x
end
end
end
@@ -640,34 +402,34 @@ let hashmap_hash_map_get_fwd
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
let rec hashmap_hash_map_get_mut_in_list_fwd
- (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
- Tot (result (state & t))
- (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls st))
+ (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+ Tot (result t)
+ (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
=
begin match ls with
| HashmapListCons ckey cvalue ls0 ->
if ckey = key
- then Return (st, cvalue)
+ then Return cvalue
else
- begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 st with
+ begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 with
| Fail -> Fail
- | Return (st0, x) -> Return (st0, x)
+ | Return x -> Return x
end
| HashmapListNil -> Fail
end
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
let rec hashmap_hash_map_get_mut_in_list_back
- (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) (ret : t) :
+ (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) :
Tot (result (hashmap_list_t t))
- (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls st))
+ (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
=
begin match ls with
| HashmapListCons ckey cvalue ls0 ->
if ckey = key
then Return (HashmapListCons ckey ret ls0)
else
- begin match hashmap_hash_map_get_mut_in_list_back t key ls0 st ret with
+ begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret with
| Fail -> Fail
| Return ls1 -> Return (HashmapListCons ckey cvalue ls1)
end
@@ -676,12 +438,10 @@ let rec hashmap_hash_map_get_mut_in_list_back
(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
let hashmap_hash_map_get_mut_fwd
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
- result (state & t)
- =
- begin match hashmap_hash_key_fwd key st with
+ (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
+ begin match hashmap_hash_key_fwd key with
| Fail -> Fail
- | Return (st0, hash) ->
+ | Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
| Fail -> Fail
@@ -691,9 +451,9 @@ let hashmap_hash_map_get_mut_fwd
hash_mod with
| Fail -> Fail
| Return l ->
- begin match hashmap_hash_map_get_mut_in_list_fwd t key l st0 with
+ begin match hashmap_hash_map_get_mut_in_list_fwd t key l with
| Fail -> Fail
- | Return (st1, x) -> Return (st1, x)
+ | Return x -> Return x
end
end
end
@@ -701,13 +461,12 @@ let hashmap_hash_map_get_mut_fwd
(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
let hashmap_hash_map_get_mut_back
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state)
- (ret : t) :
+ (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t) :
result (hashmap_hash_map_t t)
=
- begin match hashmap_hash_key_fwd key st with
+ begin match hashmap_hash_key_fwd key with
| Fail -> Fail
- | Return (st0, hash) ->
+ | Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
| Fail -> Fail
@@ -717,7 +476,7 @@ let hashmap_hash_map_get_mut_back
hash_mod with
| Fail -> Fail
| Return l ->
- begin match hashmap_hash_map_get_mut_in_list_back t key l st0 ret with
+ begin match hashmap_hash_map_get_mut_in_list_back t key l ret with
| Fail -> Fail
| Return l0 ->
begin match
@@ -736,9 +495,9 @@ let hashmap_hash_map_get_mut_back
(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
let rec hashmap_hash_map_remove_from_list_fwd
- (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
- Tot (result (state & (option t)))
- (decreases (hashmap_hash_map_remove_from_list_decreases t key ls st))
+ (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+ Tot (result (option t))
+ (decreases (hashmap_hash_map_remove_from_list_decreases t key ls))
=
begin match ls with
| HashmapListCons ckey x tl ->
@@ -748,22 +507,22 @@ let rec hashmap_hash_map_remove_from_list_fwd
mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
HashmapListNil in
begin match mv_ls with
- | HashmapListCons i cvalue tl0 -> Return (st, Some cvalue)
+ | HashmapListCons i cvalue tl0 -> Return (Some cvalue)
| HashmapListNil -> Fail
end
else
- begin match hashmap_hash_map_remove_from_list_fwd t key tl st with
+ begin match hashmap_hash_map_remove_from_list_fwd t key tl with
| Fail -> Fail
- | Return (st0, opt) -> Return (st0, opt)
+ | Return opt -> Return opt
end
- | HashmapListNil -> Return (st, None)
+ | HashmapListNil -> Return None
end
(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
let rec hashmap_hash_map_remove_from_list_back
- (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
+ (t : Type0) (key : usize) (ls : hashmap_list_t t) :
Tot (result (hashmap_list_t t))
- (decreases (hashmap_hash_map_remove_from_list_decreases t key ls st))
+ (decreases (hashmap_hash_map_remove_from_list_decreases t key ls))
=
begin match ls with
| HashmapListCons ckey x tl ->
@@ -777,7 +536,7 @@ let rec hashmap_hash_map_remove_from_list_back
| HashmapListNil -> Fail
end
else
- begin match hashmap_hash_map_remove_from_list_back t key tl st with
+ begin match hashmap_hash_map_remove_from_list_back t key tl with
| Fail -> Fail
| Return tl0 -> Return (HashmapListCons ckey x tl0)
end
@@ -786,12 +545,10 @@ let rec hashmap_hash_map_remove_from_list_back
(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
let hashmap_hash_map_remove_fwd
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
- result (state & (option t))
- =
- begin match hashmap_hash_key_fwd key st with
+ (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) =
+ begin match hashmap_hash_key_fwd key with
| Fail -> Fail
- | Return (st0, hash) ->
+ | Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
| Fail -> Fail
@@ -801,15 +558,15 @@ let hashmap_hash_map_remove_fwd
hash_mod with
| Fail -> Fail
| Return l ->
- begin match hashmap_hash_map_remove_from_list_fwd t key l st0 with
+ begin match hashmap_hash_map_remove_from_list_fwd t key l with
| Fail -> Fail
- | Return (st1, x) ->
+ | Return x ->
begin match x with
- | None -> Return (st1, None)
+ | None -> Return None
| Some x0 ->
begin match usize_sub self.hashmap_hash_map_num_entries 1 with
| Fail -> Fail
- | Return _ -> Return (st1, Some x0)
+ | Return _ -> Return (Some x0)
end
end
end
@@ -819,12 +576,12 @@ let hashmap_hash_map_remove_fwd
(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
let hashmap_hash_map_remove_back
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
+ (t : Type0) (self : hashmap_hash_map_t t) (key : usize) :
result (hashmap_hash_map_t t)
=
- begin match hashmap_hash_key_fwd key st with
+ begin match hashmap_hash_key_fwd key with
| Fail -> Fail
- | Return (st0, hash) ->
+ | Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
| Fail -> Fail
@@ -834,12 +591,12 @@ let hashmap_hash_map_remove_back
hash_mod with
| Fail -> Fail
| Return l ->
- begin match hashmap_hash_map_remove_from_list_fwd t key l st0 with
+ begin match hashmap_hash_map_remove_from_list_fwd t key l with
| Fail -> Fail
- | Return (_, x) ->
+ | Return x ->
begin match x with
| None ->
- begin match hashmap_hash_map_remove_from_list_back t key l st0 with
+ begin match hashmap_hash_map_remove_from_list_back t key l with
| Fail -> Fail
| Return l0 ->
begin match
@@ -856,8 +613,7 @@ let hashmap_hash_map_remove_back
begin match usize_sub self.hashmap_hash_map_num_entries 1 with
| Fail -> Fail
| Return i0 ->
- begin match hashmap_hash_map_remove_from_list_back t key l st0
- with
+ begin match hashmap_hash_map_remove_from_list_back t key l with
| Fail -> Fail
| Return l0 ->
begin match
@@ -878,112 +634,80 @@ let hashmap_hash_map_remove_back
end
(** [hashmap_main::hashmap::test1] *)
-let hashmap_test1_fwd (st : state) : result (state & unit) =
- begin match hashmap_hash_map_new_fwd u64 st with
+let hashmap_test1_fwd : result unit =
+ begin match hashmap_hash_map_new_fwd u64 with
| Fail -> Fail
- | Return (st0, hm) ->
- begin match hashmap_hash_map_insert_fwd u64 hm 0 42 st0 with
+ | Return hm ->
+ begin match hashmap_hash_map_insert_fwd_back u64 hm 0 42 with
| Fail -> Fail
- | Return (st1, _) ->
- begin match hashmap_hash_map_insert_back u64 hm 0 42 st0 with
+ | Return hm0 ->
+ begin match hashmap_hash_map_insert_fwd_back u64 hm0 128 18 with
| Fail -> Fail
- | Return hm0 ->
- begin match hashmap_hash_map_insert_fwd u64 hm0 128 18 st1 with
+ | Return hm1 ->
+ begin match hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 with
| Fail -> Fail
- | Return (st2, _) ->
- begin match hashmap_hash_map_insert_back u64 hm0 128 18 st1 with
+ | Return hm2 ->
+ begin match hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 with
| Fail -> Fail
- | Return hm1 ->
- begin match hashmap_hash_map_insert_fwd u64 hm1 1024 138 st2 with
+ | Return hm3 ->
+ begin match hashmap_hash_map_get_fwd u64 hm3 128 with
| Fail -> Fail
- | Return (st3, _) ->
- begin match hashmap_hash_map_insert_back u64 hm1 1024 138 st2
- with
- | Fail -> Fail
- | Return hm2 ->
- begin match hashmap_hash_map_insert_fwd u64 hm2 1056 256 st3
- with
+ | Return i ->
+ if not (i = 18)
+ then Fail
+ else
+ begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 with
| Fail -> Fail
- | Return (st4, _) ->
- begin match hashmap_hash_map_insert_back u64 hm2 1056 256 st3
- with
+ | Return hm4 ->
+ begin match hashmap_hash_map_get_fwd u64 hm4 1024 with
| Fail -> Fail
- | Return hm3 ->
- begin match hashmap_hash_map_get_fwd u64 hm3 128 st4 with
- | Fail -> Fail
- | Return (st5, i) ->
- if not (i = 18)
- then Fail
- else
- begin match
- hashmap_hash_map_get_mut_fwd u64 hm3 1024 st5 with
- | Fail -> Fail
- | Return (st6, _) ->
- begin match
- hashmap_hash_map_get_mut_back u64 hm3 1024 st5 56
- with
- | Fail -> Fail
- | Return hm4 ->
+ | Return i0 ->
+ if not (i0 = 56)
+ then Fail
+ else
+ begin match hashmap_hash_map_remove_fwd u64 hm4 1024 with
+ | Fail -> Fail
+ | Return x ->
+ begin match x with
+ | None -> Fail
+ | Some x0 ->
+ if not (x0 = 56)
+ then Fail
+ else
begin match
- hashmap_hash_map_get_fwd u64 hm4 1024 st6 with
+ hashmap_hash_map_remove_back u64 hm4 1024 with
| Fail -> Fail
- | Return (st7, i0) ->
- if not (i0 = 56)
- then Fail
- else
- begin match
- hashmap_hash_map_remove_fwd u64 hm4 1024 st7
- with
- | Fail -> Fail
- | Return (st8, x) ->
- begin match x with
- | None -> Fail
- | Some x0 ->
- if not (x0 = 56)
+ | Return hm5 ->
+ begin match hashmap_hash_map_get_fwd u64 hm5 0
+ with
+ | Fail -> Fail
+ | Return i1 ->
+ if not (i1 = 42)
+ then Fail
+ else
+ begin match
+ hashmap_hash_map_get_fwd u64 hm5 128 with
+ | Fail -> Fail
+ | Return i2 ->
+ if not (i2 = 18)
then Fail
else
begin match
- hashmap_hash_map_remove_back u64 hm4
- 1024 st7 with
+ hashmap_hash_map_get_fwd u64 hm5 1056
+ with
| Fail -> Fail
- | Return hm5 ->
- begin match
- hashmap_hash_map_get_fwd u64 hm5 0
- st8 with
- | Fail -> Fail
- | Return (st9, i1) ->
- if not (i1 = 42)
- then Fail
- else
- begin match
- hashmap_hash_map_get_fwd u64 hm5
- 128 st9 with
- | Fail -> Fail
- | Return (st10, i2) ->
- if not (i2 = 18)
- then Fail
- else
- begin match
- hashmap_hash_map_get_fwd u64
- hm5 1056 st10 with
- | Fail -> Fail
- | Return (st11, i3) ->
- if not (i3 = 256)
- then Fail
- else Return (st11, ())
- end
- end
- end
+ | Return i3 ->
+ if not (i3 = 256)
+ then Fail
+ else Return ()
end
end
- end
+ end
end
- end
end
- end
+ end
end
end
- end
end
end
end
@@ -991,26 +715,28 @@ let hashmap_test1_fwd (st : state) : result (state & unit) =
end
end
+(** Unit test for [hashmap_main::hashmap::test1] *)
+let _ = assert_norm (hashmap_test1_fwd = Return ())
+
(** [hashmap_main::insert_on_disk] *)
let insert_on_disk_fwd
(key : usize) (value : u64) (st : state) : result (state & unit) =
begin match hashmap_utils_deserialize_fwd st with
| Fail -> Fail
| Return (st0, hm) ->
- begin match hashmap_hash_map_insert_fwd u64 hm key value st0 with
+ begin match hashmap_hash_map_insert_fwd_back u64 hm key value with
| Fail -> Fail
- | Return (st1, _) ->
- begin match hashmap_hash_map_insert_back u64 hm key value st0 with
+ | Return hm0 ->
+ begin match hashmap_utils_serialize_fwd hm0 st0 with
| Fail -> Fail
- | Return hm0 ->
- begin match hashmap_utils_serialize_fwd hm0 st1 with
- | Fail -> Fail
- | Return (st2, _) -> Return (st2, ())
- end
+ | Return (st1, _) -> Return (st1, ())
end
end
end
(** [hashmap_main::main] *)
-let main_fwd (st : state) : result (state & unit) = Return (st, ())
+let main_fwd : result unit = Return ()
+
+(** Unit test for [hashmap_main::main] *)
+let _ = assert_norm (main_fwd = Return ())
diff --git a/tests/hashmap_on_disk/HashmapMain.Properties.fst b/tests/hashmap_on_disk/HashmapMain.Properties.fst
index 99b5424a..4df039a8 100644
--- a/tests/hashmap_on_disk/HashmapMain.Properties.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Properties.fst
@@ -9,16 +9,6 @@ open HashmapMain.Funs
/// how such reasoning which mixes opaque functions together with a state-error
/// monad can be performed.
-/// Also note that for now, whenever we want to use a state-error monad, we translate
-/// all the LLBC functions to pure functions living in the state-error monad (this
-/// is the reason why we regenerate all the hash map definitions for this example).
-///
-/// In the future, we will probably do some analysis to use the proper monad when
-/// generating the definitions (no monad if functions can't fail, error monad if
-/// they can fail but don't need manipulate the state, etc. in addition to proper
-/// lifting).
-
-
(*** Hypotheses *)
/// [state_v] gives us the hash map currently stored on disk
@@ -41,238 +31,6 @@ val deserialize_lem (st : state) : Lemma (
| Return (st', hm) -> hm == state_v st /\ st' == st)
[SMTPat (hashmap_utils_deserialize_fwd st)]
-(*** Lemmas - auxiliary *)
-
-/// The below proofs are trivial: we just prove that the hashmap insert function
-/// doesn't update the state... As F* is made for *intrinsic* proofs, we have to
-/// copy-paste the definitions to insert the proper lemma calls wherever needed,
-/// hence the verbosity...
-
-#push-options "--fuel 1"
-let rec hashmap_hash_map_insert_in_list_fwd_lem
- (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
- Lemma
- (ensures (
- match hashmap_hash_map_insert_in_list_fwd t key value ls st with
- | Fail -> True
- | Return (st', _) -> st' == st))
- (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
- =
- begin match ls with
- | HashmapListCons ckey cvalue ls0 ->
- if ckey = key
- then ()
- else
- hashmap_hash_map_insert_in_list_fwd_lem t key value ls0 st
- | HashmapListNil -> ()
- end
-#pop-options
-
-#push-options "--fuel 1"
-let rec hashmap_hash_map_insert_in_list_back_lem
- (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
- Lemma
- (ensures (
- match hashmap_hash_map_insert_in_list_back t key value ls st with
- | Fail -> True
- | Return (st', _) -> st' == st))
- (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
- =
- begin match ls with
- | HashmapListCons ckey cvalue ls0 ->
- if ckey = key then ()
- else hashmap_hash_map_insert_in_list_back_lem t key value ls0 st
- | HashmapListNil -> ()
- end
-#pop-options
-
-let hashmap_hash_map_insert_no_resize_back_lem
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
- (st : state) :
- Lemma
- (ensures (
- match hashmap_hash_map_insert_no_resize_back t self key value st with
- | Fail -> True
- | Return (st', _) -> st' == st))
- =
- begin match hashmap_hash_key_fwd key st with
- | Fail -> ()
- | Return (st0, i) ->
- let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_rem i i0 with
- | Fail -> ()
- | Return hash_mod ->
- begin match
- vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
- hash_mod with
- | Fail -> ()
- | Return l ->
- hashmap_hash_map_insert_in_list_fwd_lem t key value l st0;
- begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with
- | Fail -> ()
- | Return (st1, b) ->
- if b
- then
- begin match usize_add self.hashmap_hash_map_num_entries 1 with
- | Fail -> ()
- | Return i1 -> hashmap_hash_map_insert_in_list_back_lem t key value l st1
- end
- else hashmap_hash_map_insert_in_list_back_lem t key value l st1
- end
- end
- end
- end
-
-#push-options "--fuel 1"
-let rec hashmap_hash_map_allocate_slots_fwd_lem
- (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) (st : state) :
- Lemma (ensures (
- match hashmap_hash_map_allocate_slots_fwd t slots n st with
- | Fail -> True
- | Return (st', _) -> st' == st))
- (decreases (hashmap_hash_map_allocate_slots_decreases t slots n st))
- =
- begin match n with
- | 0 -> ()
- | _ ->
- begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
- | Fail -> ()
- | Return v ->
- begin match usize_sub n 1 with
- | Fail -> ()
- | Return i ->
- hashmap_hash_map_allocate_slots_fwd_lem t v i st
- end
- end
- end
-#pop-options
-
-let hashmap_hash_map_new_with_capacity_fwd_lem
- (t : Type0) (capacity : usize) (max_load_dividend : usize)
- (max_load_divisor : usize) (st : state) :
- Lemma (ensures (
- match hashmap_hash_map_new_with_capacity_fwd t capacity max_load_dividend max_load_divisor st with
- | Fail -> True
- | Return (st', _) -> st' == st))
- =
- let v = vec_new (hashmap_list_t t) in
- hashmap_hash_map_allocate_slots_fwd_lem t v capacity st
-
-#push-options "--fuel 1"
-let rec hashmap_hash_map_move_elements_from_list_back_lem
- (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t)
- (st : state) :
- Lemma (ensures (
- match hashmap_hash_map_move_elements_from_list_back t ntable ls st with
- | Fail -> True
- | Return (st', _) -> st' == st))
- (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls st))
- =
- begin match ls with
- | HashmapListCons k v tl ->
- hashmap_hash_map_insert_no_resize_back_lem t ntable k v st;
- begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
- | Fail -> ()
- | Return (st0, hm) ->
- hashmap_hash_map_move_elements_from_list_back_lem t hm tl st0
- end
- | HashmapListNil -> ()
- end
-#pop-options
-
-#push-options "--fuel 1"
-let rec hashmap_hash_map_move_elements_back_lem
- (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
- (i : usize) (st : state) :
- Lemma (ensures (
- match hashmap_hash_map_move_elements_back t ntable slots i st with
- | Fail -> True
- | Return (st', _) -> st' == st))
- (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st))
- =
- let i0 = vec_len (hashmap_list_t t) slots in
- if i < i0
- then
- begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
- | Fail -> ()
- | Return l ->
- let l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
- hashmap_hash_map_move_elements_from_list_back_lem t ntable l0 st;
- begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st
- with
- | Fail -> ()
- | Return (st0, hm) ->
- let l1 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
- begin match vec_index_mut_back (hashmap_list_t t) slots i l1 with
- | Fail -> ()
- | Return v ->
- begin match usize_add i 1 with
- | Fail -> ()
- | Return i1 -> hashmap_hash_map_move_elements_back_lem t hm v i1 st0
- end
- end
- end
- end
- else ()
-#pop-options
-
-let hashmap_hash_map_try_resize_back_lem
- (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
- Lemma (ensures (
- match hashmap_hash_map_try_resize_back t self st with
- | Fail -> True
- | Return (st', _) -> st' == st))
- =
- let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_div 4294967295 2 with
- | Fail -> ()
- | Return n1 ->
- let (i0, i1) = self.hashmap_hash_map_max_load_factor in
- begin match usize_div n1 i0 with
- | Fail -> ()
- | Return i2 ->
- if i <= i2
- then
- begin match usize_mul i 2 with
- | Fail -> ()
- | Return i3 ->
- hashmap_hash_map_new_with_capacity_fwd_lem t i3 i0 i1 st;
- begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with
- | Fail -> ()
- | Return (st0, hm) ->
- hashmap_hash_map_move_elements_back_lem t hm self.hashmap_hash_map_slots 0 st0
- end
- end
- else ()
- end
- end
-
-let hashmap_hash_map_insert_back_lem
- (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
- (st : state) :
- Lemma (ensures (
- match hashmap_hash_map_insert_back t self key value st with
- | Fail -> True
- | Return (st', _) -> st' == st))
- [SMTPat (hashmap_hash_map_insert_back t self key value st)]
- =
- hashmap_hash_map_insert_no_resize_back_lem t self key value st;
- begin match hashmap_hash_map_insert_no_resize_back t self key value st with
- | Fail -> ()
- | Return (st0, hm) ->
- begin match hashmap_hash_map_len_fwd t hm st0 with
- | Fail -> ()
- | Return (st1, i) ->
- if i > hm.hashmap_hash_map_max_load
- then
- hashmap_hash_map_try_resize_back_lem t (Mkhashmap_hash_map_t
- hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor
- hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1
- else ()
- end
- end
-
-
(*** Lemmas *)
/// The obvious lemma about [insert_on_disk]: the updated hash map stored on disk
@@ -283,23 +41,8 @@ val insert_on_disk_fwd_lem (key : usize) (value : u64) (st : state) : Lemma (
| Fail -> True
| Return (st', ()) ->
let hm = state_v st in
- match hashmap_hash_map_insert_back u64 hm key value st with
+ match hashmap_hash_map_insert_fwd_back u64 hm key value with
| Fail -> False
- | Return (_, hm') -> hm' == state_v st')
+ | Return hm' -> hm' == state_v st')
-let insert_on_disk_fwd_lem key value st =
- deserialize_lem st;
- begin match hashmap_utils_deserialize_fwd st with
- | Fail -> ()
- | Return (st0, hm) ->
- hashmap_hash_map_insert_back_lem u64 hm key value st0;
- begin match hashmap_hash_map_insert_back u64 hm key value st0 with
- | Fail -> ()
- | Return (st1, hm0) ->
- serialize_lem hm0 st1;
- begin match hashmap_utils_serialize_fwd hm0 st1 with
- | Fail -> ()
- | Return (st2, _) -> ()
- end
- end
- end
+let insert_on_disk_fwd_lem key value st = ()
--
cgit v1.2.3