From bd73cf946a2e51e07137a64602479755ca56f35b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 13 Feb 2022 20:40:31 +0100
Subject: Add some comments

---
 tests/hashmap/Hashmap.Properties.fst | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index a6becc96..ad9b39e1 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -151,6 +151,10 @@ open Hashmap.Funs
 ///   directly given by some postconditions which failed for no reasons, or
 ///   "unknown assertion failed" which forced us to manually unfold postconditions...
 ///
+///   4. As usual, the unstable arithmetic proofs are a lot of fun. We have a few
+///   of them because we prove that the table is never over-loaded (it resizes itself
+///   in order to respect the max load factor). See [new_max_load_lem] for instance.
+///
 ///   Finally: remember (again) that we are in a pure setting. Imagine having to
 ///   deal with Low*/separation logic at the same time.
 ///
@@ -542,7 +546,10 @@ let slots_s_inv (#t : Type0) (slots : slots_s t{length slots <= usize_max}) : Ty
   {:pattern index slots i}
   slot_s_inv (length slots) i (index slots i)
 
-// TODO: write that in terms of slots_s_inv
+// At some point we tried to rewrite this in terms of [slots_s_inv]. However it
+// made a lot of proofs fail because those proofs relied on the [index_map_lem]
+// pattern. We tried writing others lemmas with patterns (like [slots_s_inv]
+// implies [slots_t_inv]) but it didn't succeed, so we keep things as they are.
 let slots_t_inv (#t : Type0) (slots : slots_t t{length slots <= usize_max}) : Type0 =
   forall(i:nat{i < length slots}).
   {:pattern index slots i}
@@ -2474,7 +2481,6 @@ let times_divid_lem (n m p : pos) : Lemma ((n * m) / p >= n * (m / p))
 #pop-options
 
 /// The good old arithmetic proofs and their unstability...
-/// It seems OK now that I moved an assertion (I ran `quake 100`).
 #restart-solver
 #push-options "--z3rlimit 200 --z3cliopt smt.arith.nl=false"
 let new_max_load_lem
@@ -2497,7 +2503,10 @@ let new_max_load_lem
   let ncapacity = 2 * capacity in
   let nmax_load = (ncapacity * divid) / divis in
   FStar.Math.Lemmas.paren_mul_left 2 capacity divid;
-  assert(2 * (capacity * divid) == 2 * capacity * divid); // Often broke (though given by lemma above): we moved it up
+  // The following assertion often breaks though it is given by the above
+  // lemma. I really don't know what to do (I deactivated non-linear
+  // arithmetic and added the previous lemma, moved the lemma up...).
+  assert(2 * (capacity * divid) == 2 * capacity * divid);
   assert(nmax_load = (2 * capacity * divid) / divis);
   times_divid_lem 2 (capacity * divid) divis;
   assert((2 * (capacity * divid)) / divis >= 2 * ((capacity * divid) / divis));
-- 
cgit v1.2.3