From 4d30546c809cb2c512e0c3fd8ee540fff1330eab Mon Sep 17 00:00:00 2001 From: Son HO Date: Fri, 21 Jun 2024 23:24:01 +0200 Subject: Add some proofs for the Lean backend (#255) * Make progress on the proofs of the hashmap * Make a minor modification to the hashmap * Make progress on the hashmap * Make progress on the proofs * Make progress on the proofs * Make progress on the proof of the hashmap * Progress on the proofs of the hashmap * Update a proof * Update the Charon pin * Make minor modifications to the hashmap * Regenerate the tests * Regenerate the hashmap * Add lemmas to the Lean backend * Make progress on the proofs of the hashmap * Make a minor fix * Finish the proof about the hashmap * Update scalar_tac * Make a minor modification in the hashmap * Update the proofs of the hashmap --------- Co-authored-by: Son Ho Co-authored-by: Son Ho --- tests/fstar/hashmap/Hashmap.Clauses.Template.fst | 8 ++-- tests/fstar/hashmap/Hashmap.Funs.fst | 55 ++++++++++++++---------- tests/fstar/hashmap/Hashmap.Types.fst | 1 + 3 files changed, 37 insertions(+), 27 deletions(-) (limited to 'tests/fstar') diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst index d6ba503e..21789c69 100644 --- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst +++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst @@ -7,21 +7,21 @@ open Hashmap.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap::{hashmap::HashMap}::allocate_slots]: decreases clause - Source: 'tests/src/hashmap.rs', lines 61:4-67:5 *) + Source: 'tests/src/hashmap.rs', lines 63:4-69:5 *) unfold let hashMap_allocate_slots_loop_decreases (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (n : usize) : nat = admit () (** [hashmap::{hashmap::HashMap}::clear]: decreases clause - Source: 'tests/src/hashmap.rs', lines 94:8-99:5 *) + Source: 'tests/src/hashmap.rs', lines 97:8-102:5 *) unfold let hashMap_clear_loop_decreases (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (i : usize) : nat = admit () (** [hashmap::{hashmap::HashMap}::insert_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 108:4-125:5 *) + Source: 'tests/src/hashmap.rs', lines 111:4-128:5 *) unfold let hashMap_insert_in_list_loop_decreases (t : Type0) (key : usize) (value : t) (ls : aList_t t) : nat = @@ -35,7 +35,7 @@ let hashMap_move_elements_from_list_loop_decreases (t : Type0) admit () (** [hashmap::{hashmap::HashMap}::move_elements]: decreases clause - Source: 'tests/src/hashmap.rs', lines 182:4-191:5 *) + Source: 'tests/src/hashmap.rs', lines 182:8-191:5 *) unfold let hashMap_move_elements_loop_decreases (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (aList_t t)) (i : usize) : nat = diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 40362176..223bde57 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -14,7 +14,7 @@ let hash_key (k : usize) : result usize = Ok k (** [hashmap::{hashmap::HashMap}::allocate_slots]: loop 0: - Source: 'tests/src/hashmap.rs', lines 61:4-67:5 *) + Source: 'tests/src/hashmap.rs', lines 63:4-69:5 *) let rec hashMap_allocate_slots_loop (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (n : usize) : Tot (result (alloc_vec_Vec (aList_t t))) @@ -28,7 +28,7 @@ let rec hashMap_allocate_slots_loop else Ok slots (** [hashmap::{hashmap::HashMap}::allocate_slots]: - Source: 'tests/src/hashmap.rs', lines 61:4-61:78 *) + Source: 'tests/src/hashmap.rs', lines 63:4-63:78 *) let hashMap_allocate_slots (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (n : usize) : result (alloc_vec_Vec (aList_t t)) @@ -36,7 +36,7 @@ let hashMap_allocate_slots hashMap_allocate_slots_loop t slots n (** [hashmap::{hashmap::HashMap}::new_with_capacity]: - Source: 'tests/src/hashmap.rs', lines 70:4-74:13 *) + Source: 'tests/src/hashmap.rs', lines 72:4-76:13 *) let hashMap_new_with_capacity (t : Type0) (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : @@ -51,16 +51,17 @@ let hashMap_new_with_capacity num_entries = 0; max_load_factor = (max_load_dividend, max_load_divisor); max_load = i1; + saturated = false; slots = slots } (** [hashmap::{hashmap::HashMap}::new]: - Source: 'tests/src/hashmap.rs', lines 86:4-86:24 *) + Source: 'tests/src/hashmap.rs', lines 89:4-89:24 *) let hashMap_new (t : Type0) : result (hashMap_t t) = hashMap_new_with_capacity t 32 4 5 (** [hashmap::{hashmap::HashMap}::clear]: loop 0: - Source: 'tests/src/hashmap.rs', lines 94:8-99:5 *) + Source: 'tests/src/hashmap.rs', lines 97:8-102:5 *) let rec hashMap_clear_loop (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (i : usize) : Tot (result (alloc_vec_Vec (aList_t t))) @@ -78,18 +79,18 @@ let rec hashMap_clear_loop else Ok slots (** [hashmap::{hashmap::HashMap}::clear]: - Source: 'tests/src/hashmap.rs', lines 91:4-91:27 *) + Source: 'tests/src/hashmap.rs', lines 94:4-94:27 *) let hashMap_clear (t : Type0) (self : hashMap_t t) : result (hashMap_t t) = let* hm = hashMap_clear_loop t self.slots 0 in Ok { self with num_entries = 0; slots = hm } (** [hashmap::{hashmap::HashMap}::len]: - Source: 'tests/src/hashmap.rs', lines 101:4-101:30 *) + Source: 'tests/src/hashmap.rs', lines 104:4-104:30 *) let hashMap_len (t : Type0) (self : hashMap_t t) : result usize = Ok self.num_entries (** [hashmap::{hashmap::HashMap}::insert_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 108:4-125:5 *) + Source: 'tests/src/hashmap.rs', lines 111:4-128:5 *) let rec hashMap_insert_in_list_loop (t : Type0) (key : usize) (value : t) (ls : aList_t t) : Tot (result (bool & (aList_t t))) @@ -106,7 +107,7 @@ let rec hashMap_insert_in_list_loop end (** [hashmap::{hashmap::HashMap}::insert_in_list]: - Source: 'tests/src/hashmap.rs', lines 108:4-108:72 *) + Source: 'tests/src/hashmap.rs', lines 111:4-111:72 *) let hashMap_insert_in_list (t : Type0) (key : usize) (value : t) (ls : aList_t t) : result (bool & (aList_t t)) @@ -114,7 +115,7 @@ let hashMap_insert_in_list hashMap_insert_in_list_loop t key value ls (** [hashmap::{hashmap::HashMap}::insert_no_resize]: - Source: 'tests/src/hashmap.rs', lines 128:4-128:54 *) + Source: 'tests/src/hashmap.rs', lines 131:4-131:54 *) let hashMap_insert_no_resize (t : Type0) (self : hashMap_t t) (key : usize) (value : t) : result (hashMap_t t) @@ -155,7 +156,7 @@ let hashMap_move_elements_from_list hashMap_move_elements_from_list_loop t ntable ls (** [hashmap::{hashmap::HashMap}::move_elements]: loop 0: - Source: 'tests/src/hashmap.rs', lines 182:4-191:5 *) + Source: 'tests/src/hashmap.rs', lines 182:8-191:5 *) let rec hashMap_move_elements_loop (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (aList_t t)) (i : usize) : @@ -176,43 +177,51 @@ let rec hashMap_move_elements_loop else Ok (ntable, slots) (** [hashmap::{hashmap::HashMap}::move_elements]: - Source: 'tests/src/hashmap.rs', lines 182:4-182:96 *) + Source: 'tests/src/hashmap.rs', lines 181:4-181:82 *) let hashMap_move_elements - (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (aList_t t)) - (i : usize) : + (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (aList_t t)) : result ((hashMap_t t) & (alloc_vec_Vec (aList_t t))) = - hashMap_move_elements_loop t ntable slots i + hashMap_move_elements_loop t ntable slots 0 (** [hashmap::{hashmap::HashMap}::try_resize]: - Source: 'tests/src/hashmap.rs', lines 151:4-151:28 *) + Source: 'tests/src/hashmap.rs', lines 154:4-154:28 *) let hashMap_try_resize (t : Type0) (self : hashMap_t t) : result (hashMap_t t) = - let* max_usize = scalar_cast U32 Usize core_u32_max in let capacity = alloc_vec_Vec_len (aList_t t) self.slots in - let* n1 = usize_div max_usize 2 in + let* n1 = usize_div core_usize_max 2 in let (i, i1) = self.max_load_factor in let* i2 = usize_div n1 i in if capacity <= i2 then let* i3 = usize_mul capacity 2 in let* ntable = hashMap_new_with_capacity t i3 i i1 in - let* p = hashMap_move_elements t ntable self.slots 0 in + let* p = hashMap_move_elements t ntable self.slots in let (ntable1, _) = p in Ok - { ntable1 with num_entries = self.num_entries; max_load_factor = (i, i1) + { + self + with + max_load_factor = (i, i1); + max_load = ntable1.max_load; + slots = ntable1.slots } - else Ok { self with max_load_factor = (i, i1) } + else Ok { self with max_load_factor = (i, i1); saturated = true } (** [hashmap::{hashmap::HashMap}::insert]: - Source: 'tests/src/hashmap.rs', lines 140:4-140:48 *) + Source: 'tests/src/hashmap.rs', lines 143:4-143:48 *) let hashMap_insert (t : Type0) (self : hashMap_t t) (key : usize) (value : t) : result (hashMap_t t) = let* self1 = hashMap_insert_no_resize t self key value in let* i = hashMap_len t self1 in - if i > self1.max_load then hashMap_try_resize t self1 else Ok self1 + if i > self1.max_load + then + if self1.saturated + then Ok { self1 with saturated = true } + else hashMap_try_resize t { self1 with saturated = false } + else Ok self1 (** [hashmap::{hashmap::HashMap}::contains_key_in_list]: loop 0: Source: 'tests/src/hashmap.rs', lines 217:4-230:5 *) diff --git a/tests/fstar/hashmap/Hashmap.Types.fst b/tests/fstar/hashmap/Hashmap.Types.fst index a10bd16c..accc5e21 100644 --- a/tests/fstar/hashmap/Hashmap.Types.fst +++ b/tests/fstar/hashmap/Hashmap.Types.fst @@ -19,6 +19,7 @@ type hashMap_t (t : Type0) = num_entries : usize; max_load_factor : (usize & usize); max_load : usize; + saturated : bool; slots : alloc_vec_Vec (aList_t t); } -- cgit v1.2.3