Fix the word FIXME

mjschwenne · Sep 2, 2024 · 33510ab · 33510ab
1 parent da4042b
commit 33510ab
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 13 deletions.
diff --git a/src/Helpers/Integers.v b/src/Helpers/Integers.v
@@ -500,6 +500,9 @@ Qed.
 Create HintDb word.
 
 Ltac word_cleanup_core :=
+  (* this is so that the following pattern succeeds when (for some reason)
+  instead of w64 we have its unfolding *)
+  fold w64 w32 w8 in *;
   repeat autounfold with word in *;
   try lazymatch goal with
       (* TODO: this isn't the right strategy if the numbers in the goal are used

diff --git a/src/program_proof/reconf/ghost_proof.v b/src/program_proof/reconf/ghost_proof.v
@@ -337,8 +337,7 @@ Proof.
   destruct (decide (uint.nat term' = uint.nat highestTerm)).
   { (* for term' == highestTerm, we have the first part of "oldInfo" *)
     replace (term') with (highestTerm); last first.
-    { fold w64. (* FIXME: [word] is looking for [w64], but the type here has that definition unfolded *)
-      word. }
+    { word. }
     iDestruct (own_valid_2 with "Hproposed' Hproposed") as %Hvalid.
     rewrite singleton_op in Hvalid.
     rewrite singleton_valid in Hvalid.

diff --git a/src/program_proof/tutorial/queue/proof.v b/src/program_proof/tutorial/queue/proof.v
@@ -639,17 +639,14 @@ Proof.
       }
       iRename "Helem" into "Helem_old".
       iExactEq "Helem_old". unfold named. rewrite H0. f_equal. f_equal. f_equal.
-      (* FIXME word *)
-      rewrite u64_Z_through_nat. rewrite u64_Z.
-      reflexivity.
-      }
-      wp_pures.
-      wp_loadField.
-      wp_apply (wp_condBroadcast with "HrcondC").
-      wp_pures.
-      iModIntro.
-      iApply "Post".
-      iFrame.
+      word. }
+    wp_pures.
+    wp_loadField.
+    wp_apply (wp_condBroadcast with "HrcondC").
+    wp_pures.
+    iModIntro.
+    iApply "Post".
+    iFrame.
 Qed.
 
 End proof.