diff options
Diffstat (limited to 'tests/fstar/hashmap_on_disk')
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst | 67 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst | 61 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 742 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti | 16 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst | 48 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti | 28 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/Makefile | 47 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/Primitives.fst | 287 |
8 files changed, 1296 insertions, 0 deletions
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst new file mode 100644 index 00000000..55685114 --- /dev/null +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst @@ -0,0 +1,67 @@ +(** 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 1 --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) : 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) : 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) : nat = + admit () + +(** [core::num::u32::{9}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + +(** [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) : 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) + : 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) : 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) : 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) : 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) : nat = + admit () + diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst new file mode 100644 index 00000000..b864e32a --- /dev/null +++ b/tests/fstar/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) : 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) : 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) : 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) : 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) : 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) : 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) : + 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) : 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) : hashmap_list_t t = + ls + diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst new file mode 100644 index 00000000..82b44dbd --- /dev/null +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -0,0 +1,742 @@ +(** 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 1 --ifuel 1" + +(** [hashmap_main::hashmap::hash_key] *) +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) : + Tot (result (vec (hashmap_list_t t))) + (decreases (hashmap_hash_map_allocate_slots_decreases t slots n)) + = + if n = 0 + then Return slots + else + begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with + | Fail -> Fail + | Return slots0 -> + begin match usize_sub n 1 with + | Fail -> Fail + | Return i -> + begin match hashmap_hash_map_allocate_slots_fwd t slots0 i with + | Fail -> Fail + | Return v -> Return v + 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) : + 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 with + | Fail -> Fail + | 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 (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) : result (hashmap_hash_map_t t) = + begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 with + | Fail -> Fail + | Return hm -> Return hm + end + +(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) +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)) + = + 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_back t slots0 i1 with + | Fail -> Fail + | Return slots1 -> Return slots1 + end + end + end + else Return slots + +(** [hashmap_main::hashmap::HashMap::{0}::clear] *) +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_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 + 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) : 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) : + 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 false + else + begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 with + | Fail -> Fail + | Return b -> Return b + end + | 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) : + Tot (result (hashmap_list_t t)) + (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 with + | Fail -> Fail + | Return ls1 -> Return (HashmapListCons ckey cvalue ls1) + end + | HashmapListNil -> + let l = HashmapListNil in Return (HashmapListCons key value l) + end + +(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *) +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 with + | Fail -> Fail + | 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 + | 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 with + | Fail -> Fail + | 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 + with + | Fail -> Fail + | Return 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 (Mkhashmap_hash_map_t i0 + 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 with + | Fail -> Fail + | Return 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 (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 + +(** [core::num::u32::{9}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + +(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) +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)) + = + begin match ls with + | HashmapListCons k v tl -> + begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with + | Fail -> Fail + | Return ntable0 -> + begin match + hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl with + | Fail -> Fail + | 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_back + (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) + (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)) + = + 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_back t ntable ls + 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_back t ntable0 slots0 i1 with + | Fail -> Fail + | Return (ntable1, slots1) -> Return (ntable1, slots1) + end + end + end + end + end + else Return (ntable, slots) + +(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) +let hashmap_hash_map_try_resize_fwd_back + (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = + begin match scalar_cast U32 Usize core_num_u32_max_c with + | Fail -> Fail + | Return max_usize -> + let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_div max_usize 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 with + | Fail -> Fail + | Return ntable -> + begin match + 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 + (i, i0) ntable0.hashmap_hash_map_max_load + ntable0.hashmap_hash_map_slots) + end + end + end + else + Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, + i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) + end + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::insert] *) +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_back t self key value with + | Fail -> Fail + | Return self0 -> + begin match hashmap_hash_map_len_fwd t self0 with + | Fail -> Fail + | Return i -> + if i > self0.hashmap_hash_map_max_load + then + begin match hashmap_hash_map_try_resize_fwd_back t self0 with + | Fail -> Fail + | Return self1 -> Return self1 + end + else Return self0 + 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) : + 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 true + else + begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 with + | Fail -> Fail + | Return b -> Return b + end + | 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) : result bool = + begin match hashmap_hash_key_fwd key with + | Fail -> Fail + | 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 + | 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 with + | Fail -> Fail + | Return b -> Return 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) : + 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 cvalue + else + begin match hashmap_hash_map_get_in_list_fwd t key ls0 with + | Fail -> Fail + | 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) : result t = + begin match hashmap_hash_key_fwd key with + | Fail -> Fail + | 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 + | 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 with + | Fail -> Fail + | Return x -> Return 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) : + 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 cvalue + else + begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 with + | Fail -> Fail + | 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) (ret : t) : + Tot (result (hashmap_list_t 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 (HashmapListCons ckey ret ls0) + else + 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 + | 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) : result t = + begin match hashmap_hash_key_fwd key with + | Fail -> Fail + | 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 + | 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 with + | Fail -> Fail + | Return x -> Return 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) : + result (hashmap_hash_map_t t) + = + begin match hashmap_hash_key_fwd key with + | Fail -> Fail + | 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 + | 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 with + | Fail -> Fail + | Return 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 (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) : + Tot (result (option t)) + (decreases (hashmap_hash_map_remove_from_list_decreases t key ls)) + = + 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 (Some cvalue) + | HashmapListNil -> Fail + end + else + begin match hashmap_hash_map_remove_from_list_fwd t key tl with + | Fail -> Fail + | Return opt -> Return opt + end + | 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) : + Tot (result (hashmap_list_t t)) + (decreases (hashmap_hash_map_remove_from_list_decreases t key ls)) + = + 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 tl0 + | HashmapListNil -> Fail + end + else + begin match hashmap_hash_map_remove_from_list_back t key tl with + | Fail -> Fail + | Return tl0 -> Return (HashmapListCons ckey x tl0) + end + | HashmapListNil -> Return HashmapListNil + end + +(** [hashmap_main::hashmap::HashMap::{0}::remove] *) +let hashmap_hash_map_remove_fwd + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) = + begin match hashmap_hash_key_fwd key with + | Fail -> Fail + | 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 + | 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 with + | Fail -> Fail + | Return x -> + begin match x with + | None -> Return None + | Some x0 -> + begin match usize_sub self.hashmap_hash_map_num_entries 1 with + | Fail -> Fail + | Return _ -> Return (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) : + result (hashmap_hash_map_t t) + = + begin match hashmap_hash_key_fwd key with + | Fail -> Fail + | 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 + | 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 with + | Fail -> Fail + | Return x -> + begin match x with + | None -> + begin match hashmap_hash_map_remove_from_list_back t key l with + | Fail -> Fail + | Return 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 (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 i0 -> + begin match hashmap_hash_map_remove_from_list_back t key l with + | Fail -> Fail + | Return 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 (Mkhashmap_hash_map_t i0 + 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 : result unit = + begin match hashmap_hash_map_new_fwd u64 with + | Fail -> Fail + | Return hm -> + begin match hashmap_hash_map_insert_fwd_back u64 hm 0 42 with + | Fail -> Fail + | Return hm0 -> + begin match hashmap_hash_map_insert_fwd_back u64 hm0 128 18 with + | Fail -> Fail + | Return hm1 -> + begin match hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 with + | Fail -> Fail + | Return hm2 -> + begin match hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 with + | Fail -> Fail + | Return hm3 -> + begin match hashmap_hash_map_get_fwd u64 hm3 128 with + | Fail -> Fail + | 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 hm4 -> + begin match hashmap_hash_map_get_fwd u64 hm4 1024 with + | Fail -> Fail + | 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_remove_back u64 hm4 1024 with + | Fail -> Fail + | 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_get_fwd u64 hm5 1056 + with + | Fail -> Fail + | Return i3 -> + if not (i3 = 256) + then Fail + else Return () + end + end + end + end + end + end + end + end + end + end + end + end + 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_back u64 hm key value with + | Fail -> Fail + | Return hm0 -> + begin match hashmap_utils_serialize_fwd hm0 st0 with + | Fail -> Fail + | Return (st1, _) -> Return (st1, ()) + end + end + end + +(** [hashmap_main::main] *) +let main_fwd : result unit = Return () + +(** Unit test for [hashmap_main::main] *) +let _ = assert_norm (main_fwd = Return ()) + diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti new file mode 100644 index 00000000..6e54ea10 --- /dev/null +++ b/tests/fstar/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 1 --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/fstar/hashmap_on_disk/HashmapMain.Properties.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst new file mode 100644 index 00000000..4df039a8 --- /dev/null +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst @@ -0,0 +1,48 @@ +(** Properties about the hashmap written on disk *) +module HashmapMain.Properties +open Primitives +open HashmapMain.Funs + +#set-options "--z3rlimit 50 --fuel 0 --ifuel 1" + +/// Below, we focus on the functions to read from disk/write to disk to showcase +/// how such reasoning which mixes opaque functions together with a state-error +/// monad can be performed. + +(*** Hypotheses *) + +/// [state_v] gives us the hash map currently stored on disk +assume +val state_v : state -> hashmap_hash_map_t u64 + +/// [serialize] updates the hash map stored on disk +assume +val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma ( + match hashmap_utils_serialize_fwd hm st with + | Fail -> True + | Return (st', ()) -> state_v st' == hm) + [SMTPat (hashmap_utils_serialize_fwd hm st)] + +/// [deserialize] gives us the hash map stored on disk, without updating it +assume +val deserialize_lem (st : state) : Lemma ( + match hashmap_utils_deserialize_fwd st with + | Fail -> True + | Return (st', hm) -> hm == state_v st /\ st' == st) + [SMTPat (hashmap_utils_deserialize_fwd st)] + +(*** Lemmas *) + +/// The obvious lemma about [insert_on_disk]: the updated hash map stored on disk +/// is exactly the hash map produced from inserting the binding ([key], [value]) +/// in the hash map previously stored on disk. +val insert_on_disk_fwd_lem (key : usize) (value : u64) (st : state) : Lemma ( + match insert_on_disk_fwd key value st with + | Fail -> True + | Return (st', ()) -> + let hm = state_v st in + match hashmap_hash_map_insert_fwd_back u64 hm key value with + | Fail -> False + | Return hm' -> hm' == state_v st') + +let insert_on_disk_fwd_lem key value st = () diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti new file mode 100644 index 00000000..ce4d6485 --- /dev/null +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti @@ -0,0 +1,28 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: type definitions *) +module HashmapMain.Types +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --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); +} + +(** [core::num::u32::{9}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + +(** The state type used in the state-error monad *) +val state : Type0 + diff --git a/tests/fstar/hashmap_on_disk/Makefile b/tests/fstar/hashmap_on_disk/Makefile new file mode 100644 index 00000000..a16b0edb --- /dev/null +++ b/tests/fstar/hashmap_on_disk/Makefile @@ -0,0 +1,47 @@ +INCLUDE_DIRS = . + +FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) + +FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints + +FSTAR_OPTIONS = $(FSTAR_HINTS) \ + --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --warn_error '+241@247+285-274' \ + +FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj + +FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) + +# The F* roots are used to compute the dependency graph, and generate the .depend file +FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) + +# Build all the files +all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS))) + +# This is the right way to ensure the .depend file always gets re-built. +ifeq (,$(filter %-in,$(MAKECMDGOALS))) +ifndef NODEPEND +ifndef MAKE_RESTARTS +.depend: .FORCE + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ + +.PHONY: .FORCE +.FORCE: +endif +endif + +include .depend +endif + +# For the interactive mode +%.fst-in %.fsti-in: + @echo $(FSTAR_OPTIONS) + +# Generete the .checked files in batch mode +%.checked: + $(FSTAR) $(FSTAR_OPTIONS) $< && \ + touch -c $@ + +.PHONY: clean +clean: + rm -f obj/* diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst new file mode 100644 index 00000000..96138e46 --- /dev/null +++ b/tests/fstar/hashmap_on_disk/Primitives.fst @@ -0,0 +1,287 @@ +/// 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 + +// Normalize and unwrap a successful result (used for globals). +let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x + +(*** 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 // TODO: should be opaque +let isize_max : int = 9223372036854775807 // TODO: should be opaque +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 // TODO: should be opaque +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) + +(** Cast an integer from a [src_ty] to a [tgt_ty] *) +// TODO: check the semantics of casts in Rust +let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = + mk_scalar tgt_ty x + +/// 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 + |