summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Hashmap.Clauses.Template.fst62
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst63
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Clauses.fst61
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Funs.fst949
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Opaque.fsti16
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Types.fsti24
-rw-r--r--tests/hashmap_on_disk/Primitives.fst279
-rw-r--r--tests/misc/Primitives.fst279
8 files changed, 1733 insertions, 0 deletions
diff --git a/tests/hashmap/Hashmap.Clauses.Template.fst b/tests/hashmap/Hashmap.Clauses.Template.fst
new file mode 100644
index 00000000..257cf7a6
--- /dev/null
+++ b/tests/hashmap/Hashmap.Clauses.Template.fst
@@ -0,0 +1,62 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap]: templates for the decreases clauses *)
+module Hashmap.Clauses.Template
+open Primitives
+open Hashmap.Types
+
+#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+
+(** [hashmap::HashMap::{0}::allocate_slots]: decreases clause *)
+unfold
+let hash_map_allocate_slots_decreases (t : Type0) (slots : vec (list_t t))
+ (n : usize) : nat =
+ admit ()
+
+(** [hashmap::HashMap::{0}::clear_slots]: decreases clause *)
+unfold
+let hash_map_clear_slots_decreases (t : Type0) (slots : vec (list_t t))
+ (i : usize) : nat =
+ admit ()
+
+(** [hashmap::HashMap::{0}::insert_in_list]: decreases clause *)
+unfold
+let hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t)
+ (ls : list_t t) : nat =
+ admit ()
+
+(** [hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *)
+unfold
+let hash_map_move_elements_from_list_decreases (t : Type0)
+ (ntable : hash_map_t t) (ls : list_t t) : nat =
+ admit ()
+
+(** [hashmap::HashMap::{0}::move_elements]: decreases clause *)
+unfold
+let hash_map_move_elements_decreases (t : Type0) (ntable : hash_map_t t)
+ (slots : vec (list_t t)) (i : usize) : nat =
+ admit ()
+
+(** [hashmap::HashMap::{0}::contains_key_in_list]: decreases clause *)
+unfold
+let hash_map_contains_key_in_list_decreases (t : Type0) (key : usize)
+ (ls : list_t t) : nat =
+ admit ()
+
+(** [hashmap::HashMap::{0}::get_in_list]: decreases clause *)
+unfold
+let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) :
+ nat =
+ admit ()
+
+(** [hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
+unfold
+let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
+ (ls : list_t t) : nat =
+ admit ()
+
+(** [hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
+unfold
+let hash_map_remove_from_list_decreases (t : Type0) (key : usize)
+ (ls : list_t t) : nat =
+ admit ()
+
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
new file mode 100644
index 00000000..f3b4d6db
--- /dev/null
+++ b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -0,0 +1,63 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: templates for the decreases clauses *)
+module HashmapMain.Clauses.Template
+open Primitives
+open HashmapMain.Types
+
+#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+
+(** [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 =
+ 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 =
+ 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 =
+ 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 =
+ 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 =
+ 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 =
+ 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 =
+ 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 =
+ 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 =
+ admit ()
+
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.fst
new file mode 100644
index 00000000..84e6494a
--- /dev/null
+++ b/tests/hashmap_on_disk/HashmapMain.Clauses.fst
@@ -0,0 +1,61 @@
+(** [hashmap]: the decreases clauses *)
+module HashmapMain.Clauses
+open Primitives
+open FStar.List.Tot
+open HashmapMain.Types
+
+#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+
+(** [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
+
+(** [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 =
+ 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::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 =
+ 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 =
+ 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::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) :
+ 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::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
+
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
new file mode 100644
index 00000000..0eda588f
--- /dev/null
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -0,0 +1,949 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: function definitions *)
+module HashmapMain.Funs
+open Primitives
+include HashmapMain.Types
+include HashmapMain.Opaque
+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)
+
+(** [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))
+ =
+ begin match n with
+ | 0 -> Return (st, slots)
+ | _ ->
+ begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
+ | Fail -> Fail
+ | Return v ->
+ begin match usize_sub n 1 with
+ | Fail -> Fail
+ | Return i ->
+ begin match hashmap_hash_map_allocate_slots_fwd t v i st with
+ | Fail -> Fail
+ | Return (st0, v0) -> Return (st0, v0)
+ end
+ end
+ end
+ end
+
+(** [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))
+ =
+ let v = vec_new (hashmap_list_t t) in
+ begin match hashmap_hash_map_allocate_slots_fwd t v capacity st with
+ | Fail -> Fail
+ | Return (st0, v0) ->
+ 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 v0)
+ 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
+ | Fail -> Fail
+ | Return (st0, hm) -> Return (st0, 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 v ->
+ begin match usize_add i 1 with
+ | Fail -> Fail
+ | Return i1 ->
+ begin match hashmap_hash_map_clear_slots_fwd t v 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) :
+ Tot (result (state & (vec (hashmap_list_t t))))
+ (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 v ->
+ begin match usize_add i 1 with
+ | Fail -> Fail
+ | Return i1 ->
+ begin match hashmap_hash_map_clear_slots_back t v i1 st with
+ | Fail -> Fail
+ | Return (st0, v0) -> Return (st0, v0)
+ end
+ end
+ end
+ else Return (st, 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)
+ =
+ 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 (state & (hashmap_hash_map_t t))
+ =
+ begin match
+ hashmap_hash_map_clear_slots_back t self.hashmap_hash_map_slots 0 st with
+ | Fail -> Fail
+ | Return (st0, v) ->
+ Return (st0, Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
+ self.hashmap_hash_map_max_load v)
+ end
+
+(** [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)
+
+(** [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))
+ =
+ begin match ls with
+ | HashmapListCons ckey cvalue ls0 ->
+ if ckey = key
+ then Return (st, false)
+ else
+ begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 st with
+ | Fail -> Fail
+ | Return (st0, b) -> Return (st0, b)
+ end
+ | HashmapListNil -> Return (st, 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) :
+ Tot (result (state & (hashmap_list_t t)))
+ (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 Return (st, HashmapListCons ckey value ls0)
+ else
+ begin match hashmap_hash_map_insert_in_list_back t key value ls0 st with
+ | Fail -> Fail
+ | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l)
+ end
+ | HashmapListNil ->
+ let l = HashmapListNil in Return (st, HashmapListCons key value l)
+ 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, i) ->
+ let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_rem i i0 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, b) ->
+ if b
+ 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) :
+ result (state & (hashmap_hash_map_t t))
+ =
+ begin match hashmap_hash_key_fwd key st with
+ | Fail -> 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 -> 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, b) ->
+ if b
+ then
+ begin match usize_add self.hashmap_hash_map_num_entries 1 with
+ | Fail -> Fail
+ | Return i1 ->
+ begin match
+ hashmap_hash_map_insert_in_list_back t key value l st1 with
+ | Fail -> Fail
+ | Return (st2, l0) ->
+ begin match
+ vec_index_mut_back (hashmap_list_t t)
+ self.hashmap_hash_map_slots hash_mod l0 with
+ | Fail -> Fail
+ | Return v ->
+ Return (st2, Mkhashmap_hash_map_t i1
+ self.hashmap_hash_map_max_load_factor
+ self.hashmap_hash_map_max_load v)
+ end
+ end
+ end
+ else
+ begin match hashmap_hash_map_insert_in_list_back t key value l st1
+ with
+ | Fail -> Fail
+ | Return (st2, l0) ->
+ begin match
+ vec_index_mut_back (hashmap_list_t t)
+ self.hashmap_hash_map_slots hash_mod l0 with
+ | Fail -> Fail
+ | Return v ->
+ Return (st2, Mkhashmap_hash_map_t
+ self.hashmap_hash_map_num_entries
+ self.hashmap_hash_map_max_load_factor
+ self.hashmap_hash_map_max_load v)
+ end
+ end
+ end
+ end
+ end
+ 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_back t ntable k v st with
+ | Fail -> Fail
+ | Return (st0, hm) ->
+ begin match hashmap_hash_map_move_elements_from_list_fwd t hm tl st0 with
+ | Fail -> Fail
+ | Return (st1, _) -> Return (st1, ())
+ 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) :
+ Tot (result (state & (hashmap_hash_map_t t)))
+ (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_back t ntable k v st with
+ | Fail -> Fail
+ | Return (st0, hm) ->
+ begin match hashmap_hash_map_move_elements_from_list_back t hm tl st0
+ with
+ | Fail -> Fail
+ | Return (st1, hm0) -> Return (st1, hm0)
+ end
+ end
+ | HashmapListNil -> Return (st, ntable)
+ end
+
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+let rec hashmap_hash_map_move_elements_fwd
+ (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 l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
+ begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st
+ with
+ | Fail -> 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 -> Fail
+ | Return v ->
+ begin match usize_add i 1 with
+ | Fail -> Fail
+ | Return i1 ->
+ begin match hashmap_hash_map_move_elements_fwd t hm v i1 st0 with
+ | Fail -> Fail
+ | Return (st1, _) -> Return (st1, ())
+ 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) :
+ Tot (result (state & ((hashmap_hash_map_t t) & (vec (hashmap_list_t t)))))
+ (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 l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
+ begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st
+ with
+ | Fail -> 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 -> Fail
+ | Return v ->
+ begin match usize_add i 1 with
+ | Fail -> Fail
+ | Return i1 ->
+ begin match hashmap_hash_map_move_elements_back t hm v i1 st0 with
+ | Fail -> Fail
+ | Return (st1, (hm0, v0)) -> Return (st1, (hm0, v0))
+ end
+ end
+ end
+ end
+ end
+ else Return (st, (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 i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_div 4294967295 2 with
+ | Fail -> Fail
+ | Return n1 ->
+ let (i0, i1) = self.hashmap_hash_map_max_load_factor in
+ begin match usize_div n1 i0 with
+ | Fail -> Fail
+ | Return i2 ->
+ if i <= i2
+ then
+ begin match usize_mul i 2 with
+ | Fail -> Fail
+ | Return i3 ->
+ begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with
+ | Fail -> Fail
+ | Return (st0, hm) ->
+ begin match
+ hashmap_hash_map_move_elements_back t hm
+ self.hashmap_hash_map_slots 0 st0 with
+ | Fail -> Fail
+ | Return (st1, (_, _)) -> Return (st1, ())
+ 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 (state & (hashmap_hash_map_t t))
+ =
+ let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_div 4294967295 2 with
+ | Fail -> Fail
+ | Return n1 ->
+ let (i0, i1) = self.hashmap_hash_map_max_load_factor in
+ begin match usize_div n1 i0 with
+ | Fail -> Fail
+ | Return i2 ->
+ if i <= i2
+ then
+ begin match usize_mul i 2 with
+ | Fail -> Fail
+ | Return i3 ->
+ begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with
+ | Fail -> Fail
+ | Return (st0, hm) ->
+ begin match
+ hashmap_hash_map_move_elements_back t hm
+ self.hashmap_hash_map_slots 0 st0 with
+ | Fail -> Fail
+ | Return (st1, (hm0, v)) ->
+ let v0 =
+ mem_replace_back (vec (hashmap_list_t t)) v
+ hm0.hashmap_hash_map_slots in
+ Return (st1, Mkhashmap_hash_map_t
+ self.hashmap_hash_map_num_entries (i0, i1)
+ hm0.hashmap_hash_map_max_load v0)
+ end
+ end
+ end
+ else
+ Return (st, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (
+ i0, i1) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+ end
+ 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_back t self key value st with
+ | Fail -> Fail
+ | Return (st0, hm) ->
+ begin match hashmap_hash_map_len_fwd t hm st0 with
+ | Fail -> Fail
+ | Return (st1, i) ->
+ if i > hm.hashmap_hash_map_max_load
+ then
+ begin match
+ hashmap_hash_map_try_resize_fwd 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 with
+ | Fail -> Fail
+ | Return (st2, _) -> Return (st2, ())
+ end
+ else Return (st1, ())
+ 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) :
+ result (state & (hashmap_hash_map_t t))
+ =
+ begin match hashmap_hash_map_insert_no_resize_back t self key value st with
+ | Fail -> Fail
+ | Return (st0, hm) ->
+ begin match hashmap_hash_map_len_fwd t hm st0 with
+ | Fail -> Fail
+ | Return (st1, i) ->
+ if i > hm.hashmap_hash_map_max_load
+ then
+ begin match
+ hashmap_hash_map_try_resize_back 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 with
+ | Fail -> Fail
+ | Return (st2, hm0) -> Return (st2, hm0)
+ end
+ else
+ Return (st1, 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)
+ 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))
+ =
+ begin match ls with
+ | HashmapListCons ckey x ls0 ->
+ if ckey = key
+ then Return (st, true)
+ else
+ begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 st with
+ | Fail -> Fail
+ | Return (st0, b) -> Return (st0, b)
+ end
+ | HashmapListNil -> Return (st, 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
+ | Fail -> 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 -> Fail
+ | Return hash_mod ->
+ begin match
+ vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
+ with
+ | Fail -> Fail
+ | Return l ->
+ begin match hashmap_hash_map_contains_key_in_list_fwd t key l st0 with
+ | Fail -> Fail
+ | Return (st1, b) -> Return (st1, b)
+ end
+ end
+ end
+ end
+
+(** [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))
+ =
+ begin match ls with
+ | HashmapListCons ckey cvalue ls0 ->
+ if ckey = key
+ then Return (st, cvalue)
+ else
+ begin match hashmap_hash_map_get_in_list_fwd t key ls0 st with
+ | Fail -> Fail
+ | Return (st0, x) -> Return (st0, 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
+ | Fail -> 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 -> Fail
+ | Return hash_mod ->
+ begin match
+ vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
+ with
+ | Fail -> Fail
+ | Return l ->
+ begin match hashmap_hash_map_get_in_list_fwd t key l st0 with
+ | Fail -> Fail
+ | Return (st1, x) -> Return (st1, x)
+ end
+ end
+ end
+ end
+
+(** [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))
+ =
+ begin match ls with
+ | HashmapListCons ckey cvalue ls0 ->
+ if ckey = key
+ then Return (st, cvalue)
+ else
+ begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 st with
+ | Fail -> Fail
+ | Return (st0, x) -> Return (st0, 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) (ret : t) (st : state) :
+ Tot (result (state & (hashmap_list_t t)))
+ (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls st))
+ =
+ begin match ls with
+ | HashmapListCons ckey cvalue ls0 ->
+ if ckey = key
+ then Return (st, HashmapListCons ckey ret ls0)
+ else
+ begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret st with
+ | Fail -> Fail
+ | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l)
+ end
+ | HashmapListNil -> Fail
+ end
+
+(** [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
+ | Fail -> 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 -> 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_get_mut_in_list_fwd t key l st0 with
+ | Fail -> Fail
+ | Return (st1, x) -> Return (st1, x)
+ end
+ end
+ end
+ end
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+let hashmap_hash_map_get_mut_back
+ (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t)
+ (st : state) :
+ result (state & (hashmap_hash_map_t t))
+ =
+ begin match hashmap_hash_key_fwd key st with
+ | Fail -> 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 -> 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_get_mut_in_list_back t key l ret st0 with
+ | Fail -> Fail
+ | Return (st1, l0) ->
+ begin match
+ vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
+ hash_mod l0 with
+ | Fail -> Fail
+ | Return v ->
+ Return (st1, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+ self.hashmap_hash_map_max_load_factor
+ self.hashmap_hash_map_max_load v)
+ end
+ end
+ end
+ end
+ end
+
+(** [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))
+ =
+ begin match ls with
+ | HashmapListCons ckey x tl ->
+ if ckey = key
+ then
+ let mv_ls =
+ 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)
+ | HashmapListNil -> Fail
+ end
+ else
+ begin match hashmap_hash_map_remove_from_list_fwd t key tl st with
+ | Fail -> Fail
+ | Return (st0, opt) -> Return (st0, opt)
+ end
+ | HashmapListNil -> Return (st, 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) :
+ Tot (result (state & (hashmap_list_t t)))
+ (decreases (hashmap_hash_map_remove_from_list_decreases t key ls st))
+ =
+ begin match ls with
+ | HashmapListCons ckey x tl ->
+ if ckey = key
+ then
+ let mv_ls =
+ mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
+ HashmapListNil in
+ begin match mv_ls with
+ | HashmapListCons i cvalue tl0 -> Return (st, tl0)
+ | HashmapListNil -> Fail
+ end
+ else
+ begin match hashmap_hash_map_remove_from_list_back t key tl st with
+ | Fail -> Fail
+ | Return (st0, l) -> Return (st0, HashmapListCons ckey x l)
+ end
+ | HashmapListNil -> Return (st, HashmapListNil)
+ end
+
+(** [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
+ | Fail -> 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 -> 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_remove_from_list_fwd t key l st0 with
+ | Fail -> Fail
+ | Return (st1, x) ->
+ begin match x with
+ | None -> Return (st1, None)
+ | Some x0 ->
+ begin match usize_sub self.hashmap_hash_map_num_entries 1 with
+ | Fail -> Fail
+ | Return _ -> Return (st1, Some x0)
+ end
+ end
+ end
+ end
+ end
+ end
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+let hashmap_hash_map_remove_back
+ (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
+ result (state & (hashmap_hash_map_t t))
+ =
+ begin match hashmap_hash_key_fwd key st with
+ | Fail -> 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 -> 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_remove_from_list_fwd t key l st0 with
+ | Fail -> Fail
+ | Return (st1, x) ->
+ begin match x with
+ | None ->
+ begin match hashmap_hash_map_remove_from_list_back t key l st1 with
+ | Fail -> Fail
+ | Return (st2, l0) ->
+ begin match
+ vec_index_mut_back (hashmap_list_t t)
+ self.hashmap_hash_map_slots hash_mod l0 with
+ | Fail -> Fail
+ | Return v ->
+ Return (st2, Mkhashmap_hash_map_t
+ self.hashmap_hash_map_num_entries
+ self.hashmap_hash_map_max_load_factor
+ self.hashmap_hash_map_max_load v)
+ end
+ end
+ | Some x0 ->
+ begin match usize_sub self.hashmap_hash_map_num_entries 1 with
+ | Fail -> Fail
+ | Return i1 ->
+ begin match hashmap_hash_map_remove_from_list_back t key l st1
+ with
+ | Fail -> Fail
+ | Return (st2, l0) ->
+ begin match
+ vec_index_mut_back (hashmap_list_t t)
+ self.hashmap_hash_map_slots hash_mod l0 with
+ | Fail -> Fail
+ | Return v ->
+ Return (st2, Mkhashmap_hash_map_t i1
+ self.hashmap_hash_map_max_load_factor
+ self.hashmap_hash_map_max_load v)
+ end
+ end
+ end
+ end
+ end
+ end
+ end
+ end
+
+(** [hashmap_main::hashmap::test1] *)
+let hashmap_test1_fwd (st : state) : result (state & unit) =
+ begin match hashmap_hash_map_new_fwd u64 st with
+ | Fail -> Fail
+ | Return (st0, hm) ->
+ begin match hashmap_hash_map_insert_back u64 hm 0 42 st0 with
+ | Fail -> Fail
+ | Return (st1, hm0) ->
+ begin match hashmap_hash_map_insert_back u64 hm0 128 18 st1 with
+ | Fail -> Fail
+ | Return (st2, hm1) ->
+ begin match hashmap_hash_map_insert_back u64 hm1 1024 138 st2 with
+ | Fail -> Fail
+ | Return (st3, hm2) ->
+ begin match hashmap_hash_map_insert_back u64 hm2 1056 256 st3 with
+ | Fail -> Fail
+ | Return (st4, 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_back u64 hm3 1024 56 st5
+ with
+ | Fail -> Fail
+ | Return (st6, hm4) ->
+ begin match hashmap_hash_map_get_fwd u64 hm4 1024 st6 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)
+ then Fail
+ else
+ begin match
+ hashmap_hash_map_remove_back u64 hm4 1024 st8
+ with
+ | Fail -> Fail
+ | Return (st9, hm5) ->
+ begin match
+ hashmap_hash_map_get_fwd u64 hm5 0 st9 with
+ | Fail -> Fail
+ | Return (st10, i1) ->
+ if not (i1 = 42)
+ then Fail
+ else
+ begin match
+ hashmap_hash_map_get_fwd u64 hm5 128 st10
+ with
+ | Fail -> Fail
+ | Return (st11, i2) ->
+ if not (i2 = 18)
+ then Fail
+ else
+ begin match
+ hashmap_hash_map_get_fwd u64
+ hm5 1056 st11 with
+ | Fail -> Fail
+ | Return (st12, i3) ->
+ if not (i3 = 256)
+ then Fail
+ else Return (st12, ())
+ end
+ end
+ end
+ end
+ end
+ end
+ end
+ end
+ end
+ end
+ end
+ end
+ end
+ end
+
+(** [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_back u64 hm key value st0 with
+ | Fail -> Fail
+ | Return (st1, hm0) ->
+ begin match hashmap_utils_serialize_fwd hm0 st1 with
+ | Fail -> Fail
+ | Return (st2, _) -> Return (st2, ())
+ end
+ end
+ end
+
+(** [hashmap_main::main] *)
+let main_fwd (st : state) : result (state & unit) = Return (st, ())
+
diff --git a/tests/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/hashmap_on_disk/HashmapMain.Opaque.fsti
new file mode 100644
index 00000000..a8ec347f
--- /dev/null
+++ b/tests/hashmap_on_disk/HashmapMain.Opaque.fsti
@@ -0,0 +1,16 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: opaque function definitions *)
+module HashmapMain.Opaque
+open Primitives
+include HashmapMain.Types
+
+#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+
+(** [hashmap_main::hashmap_utils::deserialize] *)
+val hashmap_utils_deserialize_fwd
+ : state -> result (state & (hashmap_hash_map_t u64))
+
+(** [hashmap_main::hashmap_utils::serialize] *)
+val hashmap_utils_serialize_fwd
+ : hashmap_hash_map_t u64 -> state -> result (state & unit)
+
diff --git a/tests/hashmap_on_disk/HashmapMain.Types.fsti b/tests/hashmap_on_disk/HashmapMain.Types.fsti
new file mode 100644
index 00000000..b9798076
--- /dev/null
+++ b/tests/hashmap_on_disk/HashmapMain.Types.fsti
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: type definitions *)
+module HashmapMain.Types
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+
+(** [hashmap_main::hashmap::List] *)
+type hashmap_list_t (t : Type0) =
+| HashmapListCons : usize -> t -> hashmap_list_t t -> hashmap_list_t t
+| HashmapListNil : hashmap_list_t t
+
+(** [hashmap_main::hashmap::HashMap] *)
+type hashmap_hash_map_t (t : Type0) =
+{
+ hashmap_hash_map_num_entries : usize;
+ hashmap_hash_map_max_load_factor : (usize & usize);
+ hashmap_hash_map_max_load : usize;
+ hashmap_hash_map_slots : vec (hashmap_list_t t);
+}
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
new file mode 100644
index 00000000..77cf59aa
--- /dev/null
+++ b/tests/hashmap_on_disk/Primitives.fst
@@ -0,0 +1,279 @@
+/// This file lists primitive and assumed functions and types
+module Primitives
+open FStar.Mul
+open FStar.List.Tot
+
+#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
+
+(*** Utilities *)
+val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) :
+ ls':list a{
+ length ls' = length ls /\
+ index ls' i == x
+ }
+#push-options "--fuel 1"
+let rec list_update #a ls i x =
+ match ls with
+ | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x
+#pop-options
+
+(*** Result *)
+type result (a : Type0) : Type0 =
+| Return : v:a -> result a
+| Fail : result a
+
+// Monadic bind and return.
+// Re-definining those allows us to customize the result of the monadic notations
+// like: `y <-- f x;`
+let return (#a : Type0) (x:a) : result a = Return x
+let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
+ match m with
+ | Return x -> f x
+ | Fail -> Fail
+
+// Monadic assert(...)
+let massert (b:bool) : result unit = if b then Return () else Fail
+
+(*** Misc *)
+type char = FStar.Char.char
+type string = string
+
+let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
+let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
+
+(*** Scalars *)
+/// Rk.: most of the following code was at least partially generated
+
+let isize_min : int = -9223372036854775808
+let isize_max : int = 9223372036854775807
+let i8_min : int = -128
+let i8_max : int = 127
+let i16_min : int = -32768
+let i16_max : int = 32767
+let i32_min : int = -2147483648
+let i32_max : int = 2147483647
+let i64_min : int = -9223372036854775808
+let i64_max : int = 9223372036854775807
+let i128_min : int = -170141183460469231731687303715884105728
+let i128_max : int = 170141183460469231731687303715884105727
+let usize_min : int = 0
+let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let u8_min : int = 0
+let u8_max : int = 255
+let u16_min : int = 0
+let u16_max : int = 65535
+let u32_min : int = 0
+let u32_max : int = 4294967295
+let u64_min : int = 0
+let u64_max : int = 18446744073709551615
+let u128_min : int = 0
+let u128_max : int = 340282366920938463463374607431768211455
+
+type scalar_ty =
+| Isize
+| I8
+| I16
+| I32
+| I64
+| I128
+| Usize
+| U8
+| U16
+| U32
+| U64
+| U128
+
+let scalar_min (ty : scalar_ty) : int =
+ match ty with
+ | Isize -> isize_min
+ | I8 -> i8_min
+ | I16 -> i16_min
+ | I32 -> i32_min
+ | I64 -> i64_min
+ | I128 -> i128_min
+ | Usize -> usize_min
+ | U8 -> u8_min
+ | U16 -> u16_min
+ | U32 -> u32_min
+ | U64 -> u64_min
+ | U128 -> u128_min
+
+let scalar_max (ty : scalar_ty) : int =
+ match ty with
+ | Isize -> isize_max
+ | I8 -> i8_max
+ | I16 -> i16_max
+ | I32 -> i32_max
+ | I64 -> i64_max
+ | I128 -> i128_max
+ | Usize -> usize_max
+ | U8 -> u8_max
+ | U16 -> u16_max
+ | U32 -> u32_max
+ | U64 -> u64_max
+ | U128 -> u128_max
+
+type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
+
+let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
+ if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+
+let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
+
+let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+ if y <> 0 then mk_scalar ty (x / y) else Fail
+
+/// The remainder operation
+let int_rem (x : int) (y : int{y <> 0}) : int =
+ if x >= 0 then (x % y) else -(x % y)
+
+(* Checking consistency with Rust *)
+let _ = assert_norm(int_rem 1 2 = 1)
+let _ = assert_norm(int_rem (-1) 2 = -1)
+let _ = assert_norm(int_rem 1 (-2) = 1)
+let _ = assert_norm(int_rem (-1) (-2) = -1)
+
+let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+ if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+
+let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+ mk_scalar ty (x + y)
+
+let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+ mk_scalar ty (x - y)
+
+let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+ mk_scalar ty (x * y)
+
+/// The scalar types
+type isize : eqtype = scalar Isize
+type i8 : eqtype = scalar I8
+type i16 : eqtype = scalar I16
+type i32 : eqtype = scalar I32
+type i64 : eqtype = scalar I64
+type i128 : eqtype = scalar I128
+type usize : eqtype = scalar Usize
+type u8 : eqtype = scalar U8
+type u16 : eqtype = scalar U16
+type u32 : eqtype = scalar U32
+type u64 : eqtype = scalar U64
+type u128 : eqtype = scalar U128
+
+/// Negation
+let isize_neg = scalar_neg #Isize
+let i8_neg = scalar_neg #I8
+let i16_neg = scalar_neg #I16
+let i32_neg = scalar_neg #I32
+let i64_neg = scalar_neg #I64
+let i128_neg = scalar_neg #I128
+
+/// Division
+let isize_div = scalar_div #Isize
+let i8_div = scalar_div #I8
+let i16_div = scalar_div #I16
+let i32_div = scalar_div #I32
+let i64_div = scalar_div #I64
+let i128_div = scalar_div #I128
+let usize_div = scalar_div #Usize
+let u8_div = scalar_div #U8
+let u16_div = scalar_div #U16
+let u32_div = scalar_div #U32
+let u64_div = scalar_div #U64
+let u128_div = scalar_div #U128
+
+/// Remainder
+let isize_rem = scalar_rem #Isize
+let i8_rem = scalar_rem #I8
+let i16_rem = scalar_rem #I16
+let i32_rem = scalar_rem #I32
+let i64_rem = scalar_rem #I64
+let i128_rem = scalar_rem #I128
+let usize_rem = scalar_rem #Usize
+let u8_rem = scalar_rem #U8
+let u16_rem = scalar_rem #U16
+let u32_rem = scalar_rem #U32
+let u64_rem = scalar_rem #U64
+let u128_rem = scalar_rem #U128
+
+/// Addition
+let isize_add = scalar_add #Isize
+let i8_add = scalar_add #I8
+let i16_add = scalar_add #I16
+let i32_add = scalar_add #I32
+let i64_add = scalar_add #I64
+let i128_add = scalar_add #I128
+let usize_add = scalar_add #Usize
+let u8_add = scalar_add #U8
+let u16_add = scalar_add #U16
+let u32_add = scalar_add #U32
+let u64_add = scalar_add #U64
+let u128_add = scalar_add #U128
+
+/// Substraction
+let isize_sub = scalar_sub #Isize
+let i8_sub = scalar_sub #I8
+let i16_sub = scalar_sub #I16
+let i32_sub = scalar_sub #I32
+let i64_sub = scalar_sub #I64
+let i128_sub = scalar_sub #I128
+let usize_sub = scalar_sub #Usize
+let u8_sub = scalar_sub #U8
+let u16_sub = scalar_sub #U16
+let u32_sub = scalar_sub #U32
+let u64_sub = scalar_sub #U64
+let u128_sub = scalar_sub #U128
+
+/// Multiplication
+let isize_mul = scalar_mul #Isize
+let i8_mul = scalar_mul #I8
+let i16_mul = scalar_mul #I16
+let i32_mul = scalar_mul #I32
+let i64_mul = scalar_mul #I64
+let i128_mul = scalar_mul #I128
+let usize_mul = scalar_mul #Usize
+let u8_mul = scalar_mul #U8
+let u16_mul = scalar_mul #U16
+let u32_mul = scalar_mul #U32
+let u64_mul = scalar_mul #U64
+let u128_mul = scalar_mul #U128
+
+(*** Vector *)
+type vec (a : Type0) = v:list a{length v <= usize_max}
+
+let vec_new (a : Type0) : vec a = assert_norm(length #a [] == 0); []
+let vec_len (a : Type0) (v : vec a) : usize = length v
+
+// The **forward** function shouldn't be used
+let vec_push_fwd (a : Type0) (v : vec a) (x : a) : unit = ()
+let vec_push_back (a : Type0) (v : vec a) (x : a) :
+ Pure (result (vec a))
+ (requires True)
+ (ensures (fun res ->
+ match res with
+ | Fail -> True
+ | Return v' -> length v' = length v + 1)) =
+ if length v < usize_max then begin
+ (**) assert_norm(length [x] == 1);
+ (**) append_length v [x];
+ (**) assert(length (append v [x]) = length v + 1);
+ Return (append v [x])
+ end
+ else Fail
+
+// The **forward** function shouldn't be used
+let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
+ if i < length v then Return () else Fail
+let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
+ if i < length v then Return (list_update v i x) else Fail
+
+// The **backward** function shouldn't be used
+let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
+ if i < length v then Return (index v i) else Fail
+let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
+ if i < length v then Return () else Fail
+
+let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
+ if i < length v then Return (index v i) else Fail
+let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
+ if i < length v then Return (list_update v i nx) else Fail
+
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
new file mode 100644
index 00000000..77cf59aa
--- /dev/null
+++ b/tests/misc/Primitives.fst
@@ -0,0 +1,279 @@
+/// This file lists primitive and assumed functions and types
+module Primitives
+open FStar.Mul
+open FStar.List.Tot
+
+#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
+
+(*** Utilities *)
+val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) :
+ ls':list a{
+ length ls' = length ls /\
+ index ls' i == x
+ }
+#push-options "--fuel 1"
+let rec list_update #a ls i x =
+ match ls with
+ | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x
+#pop-options
+
+(*** Result *)
+type result (a : Type0) : Type0 =
+| Return : v:a -> result a
+| Fail : result a
+
+// Monadic bind and return.
+// Re-definining those allows us to customize the result of the monadic notations
+// like: `y <-- f x;`
+let return (#a : Type0) (x:a) : result a = Return x
+let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
+ match m with
+ | Return x -> f x
+ | Fail -> Fail
+
+// Monadic assert(...)
+let massert (b:bool) : result unit = if b then Return () else Fail
+
+(*** Misc *)
+type char = FStar.Char.char
+type string = string
+
+let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
+let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
+
+(*** Scalars *)
+/// Rk.: most of the following code was at least partially generated
+
+let isize_min : int = -9223372036854775808
+let isize_max : int = 9223372036854775807
+let i8_min : int = -128
+let i8_max : int = 127
+let i16_min : int = -32768
+let i16_max : int = 32767
+let i32_min : int = -2147483648
+let i32_max : int = 2147483647
+let i64_min : int = -9223372036854775808
+let i64_max : int = 9223372036854775807
+let i128_min : int = -170141183460469231731687303715884105728
+let i128_max : int = 170141183460469231731687303715884105727
+let usize_min : int = 0
+let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let u8_min : int = 0
+let u8_max : int = 255
+let u16_min : int = 0
+let u16_max : int = 65535
+let u32_min : int = 0
+let u32_max : int = 4294967295
+let u64_min : int = 0
+let u64_max : int = 18446744073709551615
+let u128_min : int = 0
+let u128_max : int = 340282366920938463463374607431768211455
+
+type scalar_ty =
+| Isize
+| I8
+| I16
+| I32
+| I64
+| I128
+| Usize
+| U8
+| U16
+| U32
+| U64
+| U128
+
+let scalar_min (ty : scalar_ty) : int =
+ match ty with
+ | Isize -> isize_min
+ | I8 -> i8_min
+ | I16 -> i16_min
+ | I32 -> i32_min
+ | I64 -> i64_min
+ | I128 -> i128_min
+ | Usize -> usize_min
+ | U8 -> u8_min
+ | U16 -> u16_min
+ | U32 -> u32_min
+ | U64 -> u64_min
+ | U128 -> u128_min
+
+let scalar_max (ty : scalar_ty) : int =
+ match ty with
+ | Isize -> isize_max
+ | I8 -> i8_max
+ | I16 -> i16_max
+ | I32 -> i32_max
+ | I64 -> i64_max
+ | I128 -> i128_max
+ | Usize -> usize_max
+ | U8 -> u8_max
+ | U16 -> u16_max
+ | U32 -> u32_max
+ | U64 -> u64_max
+ | U128 -> u128_max
+
+type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
+
+let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
+ if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+
+let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
+
+let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+ if y <> 0 then mk_scalar ty (x / y) else Fail
+
+/// The remainder operation
+let int_rem (x : int) (y : int{y <> 0}) : int =
+ if x >= 0 then (x % y) else -(x % y)
+
+(* Checking consistency with Rust *)
+let _ = assert_norm(int_rem 1 2 = 1)
+let _ = assert_norm(int_rem (-1) 2 = -1)
+let _ = assert_norm(int_rem 1 (-2) = 1)
+let _ = assert_norm(int_rem (-1) (-2) = -1)
+
+let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+ if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+
+let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+ mk_scalar ty (x + y)
+
+let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+ mk_scalar ty (x - y)
+
+let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+ mk_scalar ty (x * y)
+
+/// The scalar types
+type isize : eqtype = scalar Isize
+type i8 : eqtype = scalar I8
+type i16 : eqtype = scalar I16
+type i32 : eqtype = scalar I32
+type i64 : eqtype = scalar I64
+type i128 : eqtype = scalar I128
+type usize : eqtype = scalar Usize
+type u8 : eqtype = scalar U8
+type u16 : eqtype = scalar U16
+type u32 : eqtype = scalar U32
+type u64 : eqtype = scalar U64
+type u128 : eqtype = scalar U128
+
+/// Negation
+let isize_neg = scalar_neg #Isize
+let i8_neg = scalar_neg #I8
+let i16_neg = scalar_neg #I16
+let i32_neg = scalar_neg #I32
+let i64_neg = scalar_neg #I64
+let i128_neg = scalar_neg #I128
+
+/// Division
+let isize_div = scalar_div #Isize
+let i8_div = scalar_div #I8
+let i16_div = scalar_div #I16
+let i32_div = scalar_div #I32
+let i64_div = scalar_div #I64
+let i128_div = scalar_div #I128
+let usize_div = scalar_div #Usize
+let u8_div = scalar_div #U8
+let u16_div = scalar_div #U16
+let u32_div = scalar_div #U32
+let u64_div = scalar_div #U64
+let u128_div = scalar_div #U128
+
+/// Remainder
+let isize_rem = scalar_rem #Isize
+let i8_rem = scalar_rem #I8
+let i16_rem = scalar_rem #I16
+let i32_rem = scalar_rem #I32
+let i64_rem = scalar_rem #I64
+let i128_rem = scalar_rem #I128
+let usize_rem = scalar_rem #Usize
+let u8_rem = scalar_rem #U8
+let u16_rem = scalar_rem #U16
+let u32_rem = scalar_rem #U32
+let u64_rem = scalar_rem #U64
+let u128_rem = scalar_rem #U128
+
+/// Addition
+let isize_add = scalar_add #Isize
+let i8_add = scalar_add #I8
+let i16_add = scalar_add #I16
+let i32_add = scalar_add #I32
+let i64_add = scalar_add #I64
+let i128_add = scalar_add #I128
+let usize_add = scalar_add #Usize
+let u8_add = scalar_add #U8
+let u16_add = scalar_add #U16
+let u32_add = scalar_add #U32
+let u64_add = scalar_add #U64
+let u128_add = scalar_add #U128
+
+/// Substraction
+let isize_sub = scalar_sub #Isize
+let i8_sub = scalar_sub #I8
+let i16_sub = scalar_sub #I16
+let i32_sub = scalar_sub #I32
+let i64_sub = scalar_sub #I64
+let i128_sub = scalar_sub #I128
+let usize_sub = scalar_sub #Usize
+let u8_sub = scalar_sub #U8
+let u16_sub = scalar_sub #U16
+let u32_sub = scalar_sub #U32
+let u64_sub = scalar_sub #U64
+let u128_sub = scalar_sub #U128
+
+/// Multiplication
+let isize_mul = scalar_mul #Isize
+let i8_mul = scalar_mul #I8
+let i16_mul = scalar_mul #I16
+let i32_mul = scalar_mul #I32
+let i64_mul = scalar_mul #I64
+let i128_mul = scalar_mul #I128
+let usize_mul = scalar_mul #Usize
+let u8_mul = scalar_mul #U8
+let u16_mul = scalar_mul #U16
+let u32_mul = scalar_mul #U32
+let u64_mul = scalar_mul #U64
+let u128_mul = scalar_mul #U128
+
+(*** Vector *)
+type vec (a : Type0) = v:list a{length v <= usize_max}
+
+let vec_new (a : Type0) : vec a = assert_norm(length #a [] == 0); []
+let vec_len (a : Type0) (v : vec a) : usize = length v
+
+// The **forward** function shouldn't be used
+let vec_push_fwd (a : Type0) (v : vec a) (x : a) : unit = ()
+let vec_push_back (a : Type0) (v : vec a) (x : a) :
+ Pure (result (vec a))
+ (requires True)
+ (ensures (fun res ->
+ match res with
+ | Fail -> True
+ | Return v' -> length v' = length v + 1)) =
+ if length v < usize_max then begin
+ (**) assert_norm(length [x] == 1);
+ (**) append_length v [x];
+ (**) assert(length (append v [x]) = length v + 1);
+ Return (append v [x])
+ end
+ else Fail
+
+// The **forward** function shouldn't be used
+let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
+ if i < length v then Return () else Fail
+let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
+ if i < length v then Return (list_update v i x) else Fail
+
+// The **backward** function shouldn't be used
+let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
+ if i < length v then Return (index v i) else Fail
+let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
+ if i < length v then Return () else Fail
+
+let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
+ if i < length v then Return (index v i) else Fail
+let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
+ if i < length v then Return (list_update v i nx) else Fail
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 06:59:06 +0000