summaryrefslogtreecommitdiff
path: root/tests/hashmap
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hashmap')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst45
1 files changed, 23 insertions, 22 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 48b125d1..12f5d546 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -130,15 +130,14 @@ module InteractiveHelpers = FStar.InteractiveHelpers
/// - the proofs often fail or succeed for extremely unpredictable reasons, and are
/// extremely hard to debug.
///
-/// 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
-/// subtyping. The problem is that it is extremely hard to debug, and I definitely
-/// don't want to waste any more time with this kind of boring, tedious proofs.
+/// 1. See the comments for [hash_map_move_elements_fwd_back_lem_refin], which
+/// are believe are quite instructive: I rarely note down the process of finding
+/// a proof, but the comments for this one describe an experience which is very
+/// similar to experiences I had before.
+///
+/// Also, I still don't understand why the proof currently works, and failed
+/// before. One problem I encountered is that when trying to figure out why F*
+/// fails (and playing with Z3's parameters), we are constantly shooting in the dark.
///
/// 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.
@@ -146,8 +145,9 @@ module InteractiveHelpers = FStar.InteractiveHelpers
/// 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.
+///
+/// Finally: remember (again) that we are in a pure setting. Imagine having to
+/// deal with Low*/separation logic at the same time.
(*** List lemmas *)
@@ -1664,16 +1664,14 @@ val hash_map_move_elements_fwd_back_lem_refin
| _ -> False))
(decreases (length slots - i))
-// 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
-//
// 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.
+// For instance, using the [hash_map_slots_s_nes] type abbreviation
+// in some of the above definitions led to a failure (while it was just a type
+// abbreviation: the signatures were the same if we unfolded this type). This
+// behaviour led me to the hypothesis that maybe 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.
//
@@ -1682,9 +1680,12 @@ val hash_map_move_elements_fwd_back_lem_refin
// 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.
+// other methods. Finally out of angriness I swiched the ifuel to 4 for no
+// specific reason: everything worked fine.
+//
+// I have *no clue* why 4 is the magic number. Also: it fails if I remove
+// the unfolded postconditions (meaning I would probably need to increase
+// the ifuel to unreasonable amounts).
//
// The terrible thing is that this refinement proof is conceptually super simple:
// - there are maybe two arithmetic proofs, which are directly solved by the