Update the hashmap_on_disk example

1 files changed, 3 insertions, 260 deletions

diff --git a/tests/hashmap_on_disk/HashmapMain.Properties.fst b/tests/hashmap_on_disk/HashmapMain.Properties.fst
index 99b5424a..4df039a8 100644
--- a/tests/hashmap_on_disk/HashmapMain.Properties.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Properties.fst
@@ -9,16 +9,6 @@ open HashmapMain.Funs
 /// how such reasoning which mixes opaque functions together with a state-error
 /// monad can be performed.
 
-/// Also note that for now, whenever we want to use a state-error monad, we translate
-/// all the LLBC functions to pure functions living in the state-error monad (this
-/// is the reason why we regenerate all the hash map definitions for this example).
-/// 
-/// In the future, we will probably do some analysis to use the proper monad when
-/// generating the definitions (no monad if functions can't fail, error monad if
-/// they can fail but don't need manipulate the state, etc. in addition to proper
-/// lifting).
-
-
 (*** Hypotheses *)
 
 /// [state_v] gives us the hash map currently stored on disk
@@ -41,238 +31,6 @@ val deserialize_lem (st : state) : Lemma (
   | Return (st', hm) -> hm == state_v st /\ st' == st)
   [SMTPat (hashmap_utils_deserialize_fwd st)]
 
-(*** Lemmas - auxiliary *)
-
-/// The below proofs are trivial: we just prove that the hashmap insert function
-/// doesn't update the state... As F* is made for *intrinsic* proofs, we have to
-/// copy-paste the definitions to insert the proper lemma calls wherever needed,
-/// hence the verbosity...
-
-#push-options "--fuel 1"
-let rec hashmap_hash_map_insert_in_list_fwd_lem
-  (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
-  Lemma
-  (ensures (
-    match hashmap_hash_map_insert_in_list_fwd t key value ls st with
-    | Fail -> True
-    | Return (st', _) -> st' == st))
-  (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
-  =
-  begin match ls with
-  | HashmapListCons ckey cvalue ls0 ->
-    if ckey = key
-    then ()
-    else
-      hashmap_hash_map_insert_in_list_fwd_lem t key value ls0 st
-  | HashmapListNil -> ()
-  end
-#pop-options
-
-#push-options "--fuel 1"
-let rec hashmap_hash_map_insert_in_list_back_lem
-  (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
-  Lemma
-  (ensures (
-    match hashmap_hash_map_insert_in_list_back t key value ls st with
-    | Fail -> True
-    | Return (st', _) -> st' == st))
-  (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
-  =
-  begin match ls with
-  | HashmapListCons ckey cvalue ls0 ->
-    if ckey = key then ()
-    else hashmap_hash_map_insert_in_list_back_lem t key value ls0 st
-  | HashmapListNil -> ()
-  end
-#pop-options
-
-let hashmap_hash_map_insert_no_resize_back_lem
-  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
-  (st : state) :
-  Lemma
-  (ensures (
-    match hashmap_hash_map_insert_no_resize_back t self key value st with
-    | Fail -> True
-    | Return (st', _) -> st' == st))
-  =
-  begin match hashmap_hash_key_fwd key st with
-  | Fail -> ()
-  | Return (st0, i) ->
-    let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-    begin match usize_rem i i0 with
-    | Fail -> ()
-    | Return hash_mod ->
-      begin match
-        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
-          hash_mod with
-      | Fail -> ()
-      | Return l ->
-        hashmap_hash_map_insert_in_list_fwd_lem t key value l st0;
-        begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with
-        | Fail -> ()
-        | Return (st1, b) ->
-          if b
-          then
-            begin match usize_add self.hashmap_hash_map_num_entries 1 with
-            | Fail -> ()
-            | Return i1 -> hashmap_hash_map_insert_in_list_back_lem t key value l st1
-            end
-          else hashmap_hash_map_insert_in_list_back_lem t key value l st1
-        end
-      end
-    end
-  end
-
-#push-options "--fuel 1"
-let rec hashmap_hash_map_allocate_slots_fwd_lem
-  (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) (st : state) :
-  Lemma (ensures (
-    match hashmap_hash_map_allocate_slots_fwd t slots n st with
-    | Fail -> True
-    | Return (st', _) -> st' == st))
-  (decreases (hashmap_hash_map_allocate_slots_decreases t slots n st))
-  =
-  begin match n with
-  | 0 -> ()
-  | _ ->
-    begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
-    | Fail -> ()
-    | Return v ->
-      begin match usize_sub n 1 with
-      | Fail ->  ()
-      | Return i ->
-        hashmap_hash_map_allocate_slots_fwd_lem t v i st 
-      end
-    end
-  end
-#pop-options
-
-let hashmap_hash_map_new_with_capacity_fwd_lem
-  (t : Type0) (capacity : usize) (max_load_dividend : usize)
-  (max_load_divisor : usize) (st : state) :
-  Lemma (ensures (
-    match hashmap_hash_map_new_with_capacity_fwd t capacity max_load_dividend max_load_divisor st with
-    | Fail -> True
-    | Return (st', _) -> st' == st))
-  =
-  let v = vec_new (hashmap_list_t t) in
-  hashmap_hash_map_allocate_slots_fwd_lem t v capacity st
-
-#push-options "--fuel 1"
-let rec hashmap_hash_map_move_elements_from_list_back_lem
-  (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t)
-  (st : state) :
-  Lemma (ensures (
-    match hashmap_hash_map_move_elements_from_list_back t ntable ls st with
-    | Fail -> True
-    | Return (st', _) -> st' == st))
-  (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls st))
-  =
-  begin match ls with
-  | HashmapListCons k v tl ->
-    hashmap_hash_map_insert_no_resize_back_lem t ntable k v st;
-    begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
-    | Fail -> ()
-    | Return (st0, hm) ->
-      hashmap_hash_map_move_elements_from_list_back_lem t hm tl st0
-    end
-  | HashmapListNil -> ()
-  end
-#pop-options
-
-#push-options "--fuel 1"
-let rec hashmap_hash_map_move_elements_back_lem
-  (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
-  (i : usize) (st : state) :
-  Lemma (ensures (
-    match hashmap_hash_map_move_elements_back t ntable slots i st with
-    | Fail -> True
-    | Return (st', _) -> st' == st))
-  (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st))
-  =
-  let i0 = vec_len (hashmap_list_t t) slots in
-  if i < i0
-  then
-    begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
-    | Fail -> ()
-    | Return l ->
-      let l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
-      hashmap_hash_map_move_elements_from_list_back_lem t ntable l0 st;
-      begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st
-        with
-      | Fail -> ()
-      | Return (st0, hm) ->
-        let l1 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
-        begin match vec_index_mut_back (hashmap_list_t t) slots i l1 with
-        | Fail -> ()
-        | Return v ->
-          begin match usize_add i 1 with
-          | Fail -> ()
-          | Return i1 -> hashmap_hash_map_move_elements_back_lem t hm v i1 st0
-          end
-        end
-      end
-    end
-  else ()
-#pop-options
-
-let hashmap_hash_map_try_resize_back_lem
-  (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
-  Lemma (ensures (
-    match hashmap_hash_map_try_resize_back t self st with
-    | Fail -> True
-    | Return (st', _) -> st' == st))
-  =
-  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-  begin match usize_div 4294967295 2 with
-  | Fail -> ()
-  | Return n1 ->
-    let (i0, i1) = self.hashmap_hash_map_max_load_factor in
-    begin match usize_div n1 i0 with
-    | Fail -> ()
-    | Return i2 ->
-      if i <= i2
-      then
-        begin match usize_mul i 2 with
-        | Fail -> ()
-        | Return i3 ->
-          hashmap_hash_map_new_with_capacity_fwd_lem t i3 i0 i1 st;
-          begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with
-          | Fail -> ()
-          | Return (st0, hm) ->
-            hashmap_hash_map_move_elements_back_lem t hm self.hashmap_hash_map_slots 0 st0
-          end
-        end
-      else ()
-    end
-  end
-
-let hashmap_hash_map_insert_back_lem
-  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
-  (st : state) :
-  Lemma (ensures (
-    match hashmap_hash_map_insert_back t self key value st with
-    | Fail -> True
-    | Return (st', _) -> st' == st))
-  [SMTPat (hashmap_hash_map_insert_back t self key value st)]
-  =
-  hashmap_hash_map_insert_no_resize_back_lem t self key value st;
-  begin match hashmap_hash_map_insert_no_resize_back t self key value st with
-  | Fail -> ()
-  | Return (st0, hm) ->
-    begin match hashmap_hash_map_len_fwd t hm st0 with
-    | Fail -> ()
-    | Return (st1, i) ->
-      if i > hm.hashmap_hash_map_max_load
-      then
-        hashmap_hash_map_try_resize_back_lem t (Mkhashmap_hash_map_t
-            hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor
-            hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1
-      else ()
-    end
-  end
-
-
 (*** Lemmas *)
 
 /// The obvious lemma about [insert_on_disk]: the updated hash map stored on disk
@@ -283,23 +41,8 @@ val insert_on_disk_fwd_lem (key : usize) (value : u64) (st : state) : Lemma (
   | Fail -> True
   | Return (st', ()) ->
     let hm = state_v st in
-    match hashmap_hash_map_insert_back u64 hm key value st with
+    match hashmap_hash_map_insert_fwd_back u64 hm key value with
     | Fail -> False
-    | Return (_, hm') -> hm' == state_v st')
+    | Return hm' -> hm' == state_v st')
 
-let insert_on_disk_fwd_lem key value st =
-  deserialize_lem st;
-  begin match hashmap_utils_deserialize_fwd st with
-  | Fail -> ()
-  | Return (st0, hm) ->
-    hashmap_hash_map_insert_back_lem u64 hm key value st0;
-    begin match hashmap_hash_map_insert_back u64 hm key value st0 with
-    | Fail -> ()
-    | Return (st1, hm0) ->
-      serialize_lem hm0 st1;
-      begin match hashmap_utils_serialize_fwd hm0 st1 with
-      | Fail -> ()
-      | Return (st2, _) -> ()
-      end
-    end
-  end
+let insert_on_disk_fwd_lem key value st = ()