From bc6d82ecd6163f0784085b0f4a33b2e867595235 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 12 Feb 2022 21:20:57 +0100
Subject: Make minor updates and fix an unstable proof

---
 tests/hashmap/Hashmap.Properties.fst | 113 ++++++++++++++++++++++++++---------
 1 file changed, 85 insertions(+), 28 deletions(-)

diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 272819dc..48b125d1 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -133,6 +133,7 @@ module InteractiveHelpers = FStar.InteractiveHelpers
 ///   1. See [hash_map_slots_s_nes] below: it is simply a definition with a refinment.
 ///   For some reason, at some places if we use this type abbreviation some proofs
 ///   break, meaning we have to write the unfolded version instead.
+///   In particular, it made [hash_map_move_elements_fwd_back_lem_refin] annoying.
 ///   
 ///   I guess this specific type has something to do with the fact that F*'s type
 ///   inference yields a different result, in combination with the poor support for
@@ -663,10 +664,10 @@ let hash_map_t_base_inv (#t : Type0) (hm : hash_map_t t) : Type0 =
 /// Invariant for the hashmap
 let hash_map_t_inv (#t : Type0) (hm : hash_map_t t) : Type0 =
   // Base invariant
-  hash_map_t_base_inv hm
+  hash_map_t_base_inv hm /\
   // The hash map is either: not overloaded, or we can't resize it
-//  (hm.hash_map_num_entries <= hm.hash_map_max_load
-//   || length hm.hash_map_slots * 2 > usize_max)
+  (hm.hash_map_num_entries <= hm.hash_map_max_load
+   || length hm.hash_map_slots * 2 > usize_max)
 
 /// The following predicate links the hashmap to an associative list.
 /// Note that it does not compute the representant: different (permuted)
@@ -877,13 +878,15 @@ let rec hash_map_clear_slots_fwd_back_lem
 val hash_map_clear_fwd_back_lem_fun
   (t : Type0) (self : hash_map_t t) :
   Lemma
-  (requires (hash_map_t_inv self))
+  (requires (hash_map_t_base_inv self))
   (ensures (
     match hash_map_clear_fwd_back t self with
     | Fail -> False
     | Return hm ->
       // The hash map invariant is satisfied
-      hash_map_t_inv hm /\
+      hash_map_t_base_inv hm /\
+      // We preserved the parameters
+      hash_map_same_params hm self /\
       // The hash map has 0 values
       hash_map_t_len_s hm = 0 /\
       // It contains no bindings
@@ -1367,7 +1370,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
   (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
   Lemma
   (requires (
-    hash_map_t_inv self /\
+    hash_map_t_base_inv self /\
     hash_map_slots_s_len (hash_map_t_slots_v self) = hash_map_t_len_s self))
   (ensures (
     begin
@@ -1376,7 +1379,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
     with
     | Fail, Fail -> True
     | Return hm, Return hm_v ->
-      hash_map_t_inv hm /\
+      hash_map_t_base_inv hm /\
       hash_map_same_params hm self /\
       hash_map_t_slots_v hm == hm_v /\
       hash_map_slots_s_len hm_v == hash_map_t_len_s hm
@@ -1580,14 +1583,14 @@ let rec hash_map_move_elements_from_list_s
 /// Refinement lemma
 val hash_map_move_elements_from_list_fwd_back_lem
   (t : Type0) (ntable : hash_map_t_nes t) (ls : list_t t) :
-  Lemma (requires (hash_map_t_inv ntable))
+  Lemma (requires (hash_map_t_base_inv ntable))
   (ensures (
     match hash_map_move_elements_from_list_fwd_back t ntable ls,
           hash_map_move_elements_from_list_s (hash_map_t_slots_v ntable) (slot_t_v ls)
     with
     | Fail, Fail -> True
     | Return hm', Return hm_v ->
-      hash_map_t_inv hm' /\
+      hash_map_t_base_inv hm' /\
       hash_map_t_slots_v hm' == hm_v /\
       hash_map_same_params hm' ntable
     | _ -> False))
@@ -1648,14 +1651,14 @@ val hash_map_move_elements_fwd_back_lem_refin
   (slots : vec (list_t t)) (i : usize{i <= length slots}) :
   Lemma
   (requires (
-    hash_map_t_inv ntable))
+    hash_map_t_base_inv ntable))
   (ensures (
     match hash_map_move_elements_fwd_back t ntable slots i,
           hash_map_move_elements_s (hash_map_t_slots_v ntable) (slots_t_v slots) i
     with
     | Fail, Fail -> True // We will prove later that this is not possible
     | Return (ntable', _), Return ntable'_v ->
-      hash_map_t_inv ntable' /\
+      hash_map_t_base_inv ntable' /\
       hash_map_t_slots_v ntable' == ntable'_v /\
       hash_map_same_params ntable' ntable
     | _ -> False))
@@ -1663,13 +1666,37 @@ val hash_map_move_elements_fwd_back_lem_refin
 
 // Rk.: if above we update some definitions to use [hash_map_slots_s_nes]
 // instead of writing refinements explicitly, it makes the proof breaks.
-// I guess it is because F* does a different type inference, which combines
-// poorly with its poor support for subtyping. Problem is: I have no idea
-// where this happens and it is extremely hard to debug.
+// I guess it is because
+//
+// This proof was super unstable for some reasons.
+// 
+// For instance, a type abbreviation instead of the same type but expanded
+// led to a failure. This behaviour led me to the hypothesis that maybe it
+// it made F*'s type inference end up with a different result, which combined
+// with its poor support for subtyping made the proof failed.
+//
+// However, later, unwrapping a definition led to another failure.
+// 
+// I thus tried to manually unfold some postconditions because it
+// seemed to work for [hash_map_move_elements_fwd_back_lem] but it didn't
+// succeed.
+//
+// I tried to increase the ifuel to 2, 3: it didn't work, and I fell back to
+// other methods. Finally out of angriness I swiched the ifuel to 4 for some
+// reason: everything worked fine.
+// I have *no clue* why 4 is the magic number.
+//
+// The terrible thing is that this refinement proof is conceptually super simple:
+// - there are maybe two arithmetic proofs, which are directly solved by the
+//   precondition
+// - we need to refine the call to [hash_map_move_elements_from_list_fwd_back]:
+//   this is proven by another refinement lemma we proved above
+// - there is the recursive call (trivial)
+// Huge waste of time...
 #restart-solver
-#push-options "--z3rlimit 200 --fuel 1"
+#push-options "--z3rlimit 300 --fuel 1 --ifuel 4"
 let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i =
-  assert(hash_map_t_inv ntable);
+  assert(hash_map_t_base_inv ntable);
   let i0 = vec_len (list_t t) slots in
   let b = i < i0 in
   if b
@@ -1680,6 +1707,17 @@ let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i =
       let l0 = mem_replace_fwd (list_t t) l ListNil in
       assert(l0 == l);
       hash_map_move_elements_from_list_fwd_back_lem t ntable l0;
+      begin
+      match hash_map_move_elements_from_list_fwd_back t ntable l0,
+            hash_map_move_elements_from_list_s (hash_map_t_slots_v ntable) (slot_t_v l0)
+      with
+      | Fail, Fail -> ()
+      | Return hm', Return hm_v ->
+        assert(hash_map_t_base_inv hm');
+        assert(hash_map_t_slots_v hm' == hm_v);
+        assert(hash_map_same_params hm' ntable)
+      | _ -> assert(False)
+      end;
       begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with
       | Fail -> ()
       | Return h ->
@@ -1692,9 +1730,28 @@ let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i =
           | Fail -> ()
           | Return i1 ->
             hash_map_move_elements_fwd_back_lem_refin t h v i1;
+            begin
+            match hash_map_move_elements_fwd_back t h v i1,
+                  hash_map_move_elements_s (hash_map_t_slots_v h) (slots_t_v v) i1
+            with
+            | Fail, Fail -> ()
+            | Return (ntable', _), Return ntable'_v ->
+              assert(hash_map_t_base_inv ntable');
+              assert(hash_map_t_slots_v ntable' == ntable'_v);
+              assert(hash_map_same_params ntable' ntable)
+            | _ -> assert(False)
+            end;
             begin match hash_map_move_elements_fwd_back t h v i1 with
-            | Fail -> ()
-            | Return (h0, v0) -> ()
+            | Fail ->
+              assert(hash_map_move_elements_fwd_back t ntable slots i == Fail);
+              ()
+            | Return (ntable', v0) ->
+              begin
+              // Trying to prove the postcondition
+              match hash_map_move_elements_fwd_back t ntable slots i with
+              | Fail -> assert(False)
+              | Return (ntable'', _) -> assert(ntable'' == ntable')
+              end
             end
           end
         end
@@ -2017,12 +2074,12 @@ let slots_t_inv_implies_slots_s_inv #t slots =
   // Problem is: I can never really predict for sure with F*...
   ()
 
-val hash_map_t_inv_implies_hash_map_slots_s_inv
+val hash_map_t_base_inv_implies_hash_map_slots_s_inv
   (#t : Type0) (hm : hash_map_t t) :
-  Lemma (requires (hash_map_t_inv hm))
+  Lemma (requires (hash_map_t_base_inv hm))
   (ensures (hash_map_slots_s_inv (hash_map_t_slots_v hm)))
 
-let hash_map_t_inv_implies_hash_map_slots_s_inv #t hm = () // same as previous
+let hash_map_t_base_inv_implies_hash_map_slots_s_inv #t hm = () // same as previous
 
 /// Introducing a "partial" version of the hash map invariant, which operates on
 /// a suffix of the hash map.
@@ -2076,12 +2133,12 @@ val hash_map_slots_s_inv_implies_assoc_list_lem
 let hash_map_slots_s_inv_implies_assoc_list_lem #t hm =
   partial_hash_map_slots_s_inv_implies_assoc_list_lem (length hm) 0 hm
 
-val hash_map_t_inv_implies_assoc_list_lem
+val hash_map_t_base_inv_implies_assoc_list_lem
   (#t : Type0) (hm : hash_map_t t):
-  Lemma (requires (hash_map_t_inv hm))
+  Lemma (requires (hash_map_t_base_inv hm))
   (ensures (assoc_list_inv (hash_map_t_v hm)))
 
-let hash_map_t_inv_implies_assoc_list_lem #t hm =
+let hash_map_t_base_inv_implies_assoc_list_lem #t hm =
   hash_map_slots_s_inv_implies_assoc_list_lem (hash_map_t_slots_v hm)
 
 /// For some reason, we can't write the below [forall] directly in the [ensures]
@@ -2099,7 +2156,7 @@ val hash_map_move_elements_fwd_back_lem
   Lemma
   (requires (
     let al = flatten (slots_t_v slots) in
-    hash_map_t_inv ntable /\
+    hash_map_t_base_inv ntable /\
     length al <= usize_max /\
     assoc_list_inv al /\
     // The table is empty
@@ -2112,7 +2169,7 @@ val hash_map_move_elements_fwd_back_lem
     with
     | Return (ntable', _), Return ntable'_v ->
       // The invariant is preserved
-      hash_map_t_inv ntable' /\
+      hash_map_t_base_inv ntable' /\
       // The table has the same number of slots
       length ntable'.hash_map_slots = length ntable.hash_map_slots /\
       // The count is good
@@ -2144,7 +2201,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
   with
   | Fail, Fail -> ()
   | Return (ntable', _), Return ntable'_v ->
-    assert(hash_map_t_inv ntable');
+    assert(hash_map_t_base_inv ntable');
     assert(hash_map_t_slots_v ntable' == ntable'_v)
   | _ -> assert(False)
   end;
@@ -2163,7 +2220,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
         hash_map_move_elements_s_flat ntable_v al
   with
   | Return (ntable', _), Return ntable'_v ->
-    assert(hash_map_t_inv ntable');
+    assert(hash_map_t_base_inv ntable');
     assert(length ntable'.hash_map_slots = length ntable.hash_map_slots);
     // Rk.: Adding the following let binding makes the proof fails even with a huge
     // rlitmit. Really having fun here...
-- 
cgit v1.2.3