From cb5bca7ccaa23a1a7490811806752553eaf36ef9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 12 Feb 2022 20:37:52 +0100
Subject: Make more progress on the proofs

---
 tests/hashmap/Hashmap.Properties.fst | 41 ++++++++++++++++++++++++++++++------
 1 file changed, 34 insertions(+), 7 deletions(-)

(limited to 'tests/hashmap/Hashmap.Properties.fst')

diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index ca3a911f..60eebf19 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -141,6 +141,12 @@ module InteractiveHelpers = FStar.InteractiveHelpers
 ///
 ///   2. See [hash_map_is_assoc_list] and [hash_map_move_elements_fwd_back_lem].
 ///   For this one, I have no clue what's going on.
+///
+///   3. [hash_map_move_elements_fwd_back_lem] was very painful, with assertions
+///   directly given by some postconditions which failed for no reasons, or
+///   "unknown assertion failed" which forced us to manually unfold postconditions...
+///   And we are in a pure setting!! Imagine having to deal with Low*/separation logic
+///   at the same time.
 
 
 (*** List lemmas *)
@@ -2110,6 +2116,12 @@ val hash_map_move_elements_fwd_back_lem
     | _ -> False // We can only succeed
     ))
 
+// Weird, dirty things happen below.
+// Manually unfolding some postconditions allowed to make the proof pass,
+// and also revealed the reason why some proofs failed with "Unknown assertion
+// failed" (resulting in the call to [flatten_0_is_flatten] for instance).
+// I think manually unfolding the postconditions allowed to account for the
+// lack of ifuel (this kind of proofs is annoying, really).
 #restart-solver
 #push-options "--z3rlimit 200"
 let hash_map_move_elements_fwd_back_lem t ntable slots =
@@ -2117,7 +2129,26 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
   let slots_v = slots_t_v slots in
   let al = flatten slots_v in
   hash_map_move_elements_fwd_back_lem_refin t ntable slots 0;
+  begin
+  match hash_map_move_elements_fwd_back t ntable slots 0,
+        hash_map_move_elements_s ntable_v slots_v 0
+  with
+  | Fail, Fail -> ()
+  | Return (ntable', _), Return ntable'_v ->
+    assert(hash_map_t_inv ntable');
+    assert(hash_map_t_slots_v ntable' == ntable'_v)
+  | _ -> assert(False)
+  end;
   hash_map_move_elements_s_lem_refin_flat ntable_v slots_v 0;
+  begin
+  match hash_map_move_elements_s ntable_v slots_v 0,
+        hash_map_move_elements_s_flat ntable_v (flatten_i slots_v 0)
+  with
+  | Fail, Fail -> ()
+  | Return hm, Return hm' -> assert(hm == hm')
+  | _ -> assert(False)
+  end;
+  flatten_0_is_flatten slots_v; // flatten_i slots_v 0 == flatten slots_v
   hash_map_move_elements_s_flat_lem ntable_v al;
   match hash_map_move_elements_fwd_back t ntable slots 0,
         hash_map_move_elements_s_flat ntable_v al
@@ -2125,14 +2156,10 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
   | Return (ntable', _), Return ntable'_v ->
     assert(hash_map_t_inv ntable');
     assume(length ntable'.hash_map_slots = length ntable.hash_map_slots); // TODO
-    // Adding the following let binding makes the proof fails even with a huge
+    // Rk.: Adding the following let binding makes the proof fails even with a huge
     // rlitmit. Really having fun here...
-    // let ntable'_v = hash_map_t_slots_v ntable' in
-//    assume(hash_map_slots_s_len ntable'_v == hash_map_t_len_s ntable'); // TODO
-    assert(hash_map_slots_s_len (hash_map_t_slots_v ntable') == hash_map_t_len_s ntable');
-    assume(hash_map_slots_s_len (hash_map_t_slots_v ntable') == length al); // TODO
     assert(hash_map_t_len_s ntable' = length al);
-    assume(hash_map_t_slots_v ntable' == ntable'_v); // TODO
+    assert(hash_map_t_slots_v ntable' == ntable'_v);
     assert(hash_map_is_assoc_list ntable' al)
-  | _ -> assume(False)
+  | _ -> assert(False)
 #pop-options
-- 
cgit v1.2.3