Make good progress on the invariant proofs for remove'back

1 files changed, 132 insertions, 18 deletions

diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 08ae5714..8b53268b 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -170,6 +170,22 @@ module InteractiveHelpers = FStar.InteractiveHelpers
 ///   See [hash_map_insert_fwd_back_lem] for instance.
 
 
+/// The proof strategy is to do exactly as with Low* proofs (we initially tried to
+/// prove more properties in one go, but it was a mistake):
+/// - prove that, under some preconditions, the low-level functions translated
+///   from Rust refine some higher-level functions
+/// - do functional proofs about those high-level functions to prove interesting
+///   properties about the hash map operations, and invariant preservation
+/// - combine everything
+///
+/// The fact that we work in a pure setting allows us to be more modular than when
+/// working with effects. For instance we can do a case disjunction (see the proofs
+/// for insert, which study the cases where the key is already/not in the hash map
+/// in separate proofs). We can also easily prove a refinement lemma, study the
+/// model, and combine those to also prove that the low-level function preserves
+/// the invariants.
+
+
 (*** List lemmas *)
 
 val index_append_lem (#a : Type0) (ls0 ls1 : list a) (i : nat{i < length ls0 + length ls1}) :
@@ -1559,9 +1575,9 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
 
 let hash_map_t_updated_binding
   (#t : Type0) (hm : hash_map_slots_s_nes t)
-  (key : usize) (value : t) (hm' : hash_map_slots_s_nes t) : Type0 =
+  (key : usize) (opt_value : option t) (hm' : hash_map_slots_s_nes t) : Type0 =
   // [key] maps to [value]
-  hash_map_slots_s_find hm' key == Some value /\
+  hash_map_slots_s_find hm' key == opt_value /\
   // The other bindings are preserved
   (forall k'. k' <> key ==> hash_map_slots_s_find hm' k' == hash_map_slots_s_find hm k')
 
@@ -1570,7 +1586,7 @@ let insert_post (#t : Type0) (hm : hash_map_slots_s_nes t)
   // The invariant is preserved
   hash_map_slots_s_inv hm' /\
   // [key] maps to [value] and the other bindings are preserved
-  hash_map_t_updated_binding hm key value hm' /\
+  hash_map_t_updated_binding hm key (Some value) hm' /\
   // The length is incremented, iff we inserted a new key
   (match hash_map_slots_s_find hm key with
    | None -> hash_map_slots_s_len hm' = hash_map_slots_s_len hm + 1
@@ -2734,7 +2750,7 @@ val hash_map_insert_fwd_back_lem
       // The invariant is preserved
       hash_map_t_inv hm' /\
       // [key] maps to [value] and the other bindings are preserved
-      hash_map_t_updated_binding (hash_map_t_slots_v self) key value (hash_map_t_slots_v hm') /\
+      hash_map_t_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_v hm') /\
       // The length is incremented, iff we inserted a new key
       (match hash_map_t_find_s self key with
        | None -> hash_map_t_len_s hm' = hash_map_t_len_s self + 1
@@ -2745,10 +2761,10 @@ let hash_map_insert_fwd_back_bindings_lem
   (hm' hm'' : hash_map_t_nes t) :
   Lemma
   (requires (
-     hash_map_t_updated_binding (hash_map_t_slots_v self) key value (hash_map_t_slots_v hm') /\
+     hash_map_t_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_v hm') /\
      hash_map_t_same_bindings hm' hm''))
   (ensures (
-     hash_map_t_updated_binding (hash_map_t_slots_v self) key value (hash_map_t_slots_v hm'')))
+     hash_map_t_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_v hm'')))
   = ()
 
 #restart-solver
@@ -3180,23 +3196,51 @@ let hash_map_remove_fwd_lem t self key =
 
 (*** remove'back *)
 
+(**** Refinement proofs *)
+
 /// High-level model for [remove_from_list'back]
 let hash_map_remove_from_list_s
   (#t : Type0) (key : usize) (ls : slot_s t) :
   slot_s t =
   filter_one (not_same_key key) ls
 
+(*
+// TODO: remove?
+val filter_one_find (#a : Type) (f g : a -> bool) (ls : list a) :
+  Lemma
+  (requires (forall x. f x <> g x))
+  (ensures (
+    let ls' = filter_one f ls in
+    match find g ls with
+    | None -> length ls' = length ls
+    | Some _ -> length ls' + 1 = length ls))
+
+#push-options "--fuel 1"
+let rec filter_one_find #a f g ls =
+  match ls with
+  | [] -> ()
+  | x :: ls' -> filter_one_find f g ls'
+#pop-options
+*)
+
 /// Refinement lemma
-val hash_map_remove_from_list_back_lem
+val hash_map_remove_from_list_back_lem_refin
   (#t : Type0) (key : usize) (ls : list_t t) :
   Lemma
   (ensures (
     match hash_map_remove_from_list_back t key ls with
     | Fail -> False
-    | Return ls' -> list_t_v ls' == hash_map_remove_from_list_s key (list_t_v ls)))
+    | Return ls' ->
+      list_t_v ls' == hash_map_remove_from_list_s key (list_t_v ls) /\
+      // The length is decremented, iff the key was in the slot
+      (let len = length (list_t_v ls) in
+       let len' = length (list_t_v ls') in
+       match slot_find key (list_t_v ls) with
+       | None -> len = len'
+       | Some _ -> len = len' + 1)))
 
 #push-options "--fuel 1"
-let rec hash_map_remove_from_list_back_lem #t key ls =
+let rec hash_map_remove_from_list_back_lem_refin #t key ls =
   begin match ls with
   | ListCons ckey x tl ->
     let b = ckey = key in
@@ -3209,7 +3253,7 @@ let rec hash_map_remove_from_list_back_lem #t key ls =
       end
     else
       begin
-      hash_map_remove_from_list_back_lem key tl;
+      hash_map_remove_from_list_back_lem_refin key tl;
       match hash_map_remove_from_list_back t key tl with
       | Fail -> ()
       | Return l -> let ls0 = ListCons ckey x l in ()
@@ -3229,7 +3273,7 @@ let hash_map_remove_s
   list_update self hash slot'
 
 /// Refinement lemma
-val hash_map_remove_back_lem
+val hash_map_remove_back_lem_refin
   (#t : Type0) (self : hash_map_t_nes t) (key : usize) :
   Lemma
   (requires (
@@ -3239,9 +3283,17 @@ val hash_map_remove_back_lem
   (ensures (
     match hash_map_remove_back t self key with
     | Fail -> False
-    | Return hm' -> hash_map_t_slots_v hm' == hash_map_remove_s (hash_map_t_slots_v self) key))
-
-let hash_map_remove_back_lem #t self key =
+    | Return hm' ->
+      hash_map_same_params hm' self /\
+      hash_map_t_slots_v hm' == hash_map_remove_s (hash_map_t_slots_v self) key /\
+      // The length is decremented iff the key was in the map
+      (let len = hash_map_t_len_s self in
+       let len' = hash_map_t_len_s hm' in
+       match hash_map_t_find_s self key with
+       | None -> len = len'
+       | Some _ -> len = len' + 1)))
+
+let hash_map_remove_back_lem_refin #t self key =
   begin match hash_key_fwd key with
   | Fail -> ()
   | Return i ->
@@ -3264,11 +3316,13 @@ let hash_map_remove_back_lem #t self key =
           begin match x with
           | None ->
             begin
-            hash_map_remove_from_list_back_lem key l;
+            hash_map_remove_from_list_back_lem_refin key l;
             match hash_map_remove_from_list_back t key l with
             | Fail -> ()
             | Return l0 ->
-              begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+              begin
+              length_flatten_update (slots_t_v v) hash_mod (list_t_v l0);
+              match vec_index_mut_back (list_t t) v hash_mod l0 with
               | Fail -> ()
               | Return v0 -> ()
               end
@@ -3282,11 +3336,13 @@ let hash_map_remove_back_lem #t self key =
             | Fail -> ()
             | Return i3 ->
               begin
-              hash_map_remove_from_list_back_lem key l;
+              hash_map_remove_from_list_back_lem_refin key l;
               match hash_map_remove_from_list_back t key l with
               | Fail -> ()
               | Return l0 ->
-                begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+                begin
+                length_flatten_update (slots_t_v v) hash_mod (list_t_v l0);
+                match vec_index_mut_back (list_t t) v hash_mod l0 with
                 | Fail -> ()
                 | Return v0 -> ()
                 end
@@ -3297,3 +3353,61 @@ let hash_map_remove_back_lem #t self key =
       end
     end
   end
+
+(**** Invariants, high-level properties *)
+
+val hash_map_remove_from_list_s_lem
+  (#t : Type0) (k : usize) (slot : slot_s t) (len : usize{len > 0}) (i : usize) :
+  Lemma
+  (requires (slot_s_inv len i slot))
+  (ensures (
+    let slot' = hash_map_remove_from_list_s k slot in
+    slot_s_inv len i slot' /\
+    slot_find k slot' == None /\
+    (forall (k':key{k' <> k}). slot_find k' slot' == slot_find k' slot) /\
+    // This postcondition is necessary to prove that the invariant is preserved
+    // in the recursive calls. This allows us to do the proof in one go.
+    (forall (b:binding t). for_all (binding_neq b) slot ==> for_all (binding_neq b) slot')
+  ))
+
+#push-options "--fuel 1"
+let rec hash_map_remove_from_list_s_lem #t key slot len i =
+  match slot with
+  | [] -> ()
+  | (k',v) :: slot' ->
+    if k' <> key then
+      begin
+      hash_map_remove_from_list_s_lem key slot' len i;
+      let slot'' = hash_map_remove_from_list_s key slot' in
+      assert(for_all (same_hash_mod_key len i) ((k',v)::slot''));
+      assert(for_all (binding_neq (k',v)) slot'); // Triggers instanciation
+      assert(for_all (binding_neq (k',v)) slot'')
+      end
+    else
+      begin
+      assert(for_all (binding_neq (k',v)) slot');
+      for_all_binding_neq_find_lem key v slot'
+      end
+#pop-options
+
+// TODO: rename hash_map_t_updated_binding to hash_map_slots_updated_binding
+
+val hash_map_remove_s_lem
+  (#t : Type0) (self : hash_map_slots_s_nes t) (key : usize) :
+  Lemma
+  (requires (hash_map_slots_s_inv self))
+  (ensures (
+    let hm' = hash_map_remove_s self key in
+    // The invariant is preserved
+    hash_map_slots_s_inv hm' /\
+    // We updated the binding
+    hash_map_t_updated_binding self key None hm'))
+
+let hash_map_remove_s_lem #t self key =
+  let len = length self in
+  let hash = hash_mod_key key len in
+  let slot = index self hash in
+  hash_map_remove_from_list_s_lem key slot len hash;
+  let slot' = hash_map_remove_from_list_s key slot in
+  let hm' = list_update self hash slot' in
+  assert(hash_map_slots_s_inv self)