Make word rewrite in hypotheses

src/Helpers/Integers.v

@@ -441,6 +441,11 @@ Proof.
   unfold W32; rewrite word.unsigned_of_Z; auto.
 Qed.
 
+Lemma unsigned_U8 z : uint.Z (W8 z) = word.wrap (word:=w8_word_instance) z.
+Proof.
+  unfold W8; rewrite word.unsigned_of_Z; auto.
+Qed.
+
 Lemma signed_U64 z : sint.Z (W64 z) = word.swrap (word:=w64_word_instance) z.
 Proof.
   unfold W64; rewrite word.signed_of_Z; auto.
@@ -499,6 +504,19 @@ Qed.
 
 Create HintDb word.
 
+Hint Rewrite unsigned_U64 unsigned_U32 unsigned_U8 : word.
+
+Ltac simpl_word_constants :=
+  repeat match goal with
+         | [ H: context[word.unsigned (W64 ?x)] |- _ ] => change (uint.Z x) with x in H
+         | [ |- context[word.unsigned (W64 ?x)] ] => change (uint.Z x) with x
+         | [ H: context[word.unsigned (W32 ?x)] |- _ ] => change (uint.Z (W32 x)) with x in H
+         | [ |- context[word.unsigned (W32 ?x)] ] => change (uint.Z (W32 x)) with x
+         | [ H: context[word.unsigned (W8 ?x)] |- _ ] => change (uint.Z (W32 8)) with x in H
+         | [ |- context[word.unsigned (W8 ?x)] ] => change (uint.Z (W8 x)) with x
+        (* TODO: add sint versions *)
+    end.
+
 Ltac word_cleanup_core :=
   (* this is so that the following pattern succeeds when (for some reason)
   instead of w64 we have its unfolding *)
@@ -515,20 +533,19 @@ Ltac word_cleanup_core :=
       | |- not (@eq u32 _ _) => apply (f_not_equal uint.Z)
       | |- not (@eq u8 _ _) => apply (f_not_equal uint.Z)
       end;
+  simpl_word_constants;
   (* can't replace some of these with [autorewrite], probably because typeclass inference
   isn't the same *)
   repeat (
       rewrite -> ?word.unsigned_add, ?word.unsigned_sub,
-      ?word.unsigned_divu_nowrap, ?word.unsigned_modu_nowrap,
-      ?word.unsigned_of_Z, ?word.of_Z_unsigned, ?unsigned_U64, ?unsigned_U32,
-      ?w64_unsigned_ltu
-      || autorewrite with word
+        ?word.unsigned_divu_nowrap, ?word.unsigned_modu_nowrap,
+        ?word.unsigned_mul,
+        ?w64_unsigned_ltu
+      || rewrite -> ?word.unsigned_of_Z, ?word.of_Z_unsigned in *
+      || autorewrite with word in *
     );
   repeat match goal with
-         | [ H: context[word.unsigned (W64 ?x)] |- _ ] => change (uint.Z x) with x in H
-         | [ |- context[word.unsigned (W64 ?x)] ] => change (uint.Z x) with x
-         | [ H: context[word.unsigned (W32 ?x)] |- _ ] => change (uint.Z (W32 x)) with x in H
-         | [ |- context[word.unsigned (W32 ?x)] ] => change (uint.Z (W32 x)) with x
+         | _ => progress simpl_word_constants
          | [ H: @eq w64 _ _ |- _ ] => let H' := fresh H "_signed" in
                                       apply w64_val_f_equal in H as [H H']
          | [ H: @eq w32 _ _ |- _ ] => let H' := fresh H "_signed" in
@@ -575,45 +592,34 @@ Ltac word_cleanup_core :=
 that does a subset of safe and useful rewrites *)
 Ltac word_cleanup := word_cleanup_core; try lia.
 
-Ltac word := solve [
-                 word_cleanup_core;
-                 unfold word.wrap in *;
-                 (* NOTE: some inefficiency here because [lia] will do [zify]
+Ltac word := first [
+                 solve [
+                     word_cleanup_core;
+                     unfold word.wrap in *;
+                     (* NOTE: some inefficiency here because [lia] will do [zify]
                  again, but we can't rebind the zify hooks in Ltac *)
-                 zify; Z.div_mod_to_equations; lia
+                     zify; Z.div_mod_to_equations; lia
+                   ]
+               | fail 1 "word could not solve goal"
                ].
 
 Theorem Z_u32 z :
   0 <= z < 2 ^ 32 ->
   uint.Z (W32 z) = z.
-Proof.
-  intros.
-  unfold W32.
-  rewrite word.unsigned_of_Z.
-  rewrite wrap_small; auto.
-Qed.
+Proof. word. Qed.
 
 Lemma u32_Z (x : u32) :
   W32 (uint.Z x) = x.
-Proof.
-  unfold W32. apply word.of_Z_unsigned.
-Qed.
+Proof. word. Qed.
 
 Theorem Z_u64 z :
   0 <= z < 2 ^ 64 ->
   uint.Z (W64 z) = z.
-Proof.
-  intros.
-  unfold W64.
-  rewrite word.unsigned_of_Z.
-  rewrite wrap_small; auto.
-Qed.
+Proof. word. Qed.
 
 Lemma u64_Z (x : u64) :
   W64 (uint.Z x) = x.
-Proof.
-  unfold W64. apply word.of_Z_unsigned.
-Qed.
+Proof. word. Qed.
 
 Lemma w64_to_nat_id (x : w64) :
   W64 (Z.of_nat (uint.nat x)) = x.

src/Helpers/range_set.v

@@ -109,6 +109,4 @@ Proof.
   intros Hnonneg1 Hoverflow x Hin1 Hin2.
   assert (x = W64 start) by set_solver.
   subst. apply rangeSet_lookup in Hin2; eauto; try word.
-  assert (uint.Z (W64 start) = start) by word.
-  word.
 Qed.

src/goose_lang/lib/encoding/encoding.v

@@ -346,29 +346,19 @@ Theorem u8_to_from_u32 (x:w32) :
   uint.Z (W32 (uint.Z (W8 (uint.Z x)))) =
   uint.Z x `mod` 2 ^ 8.
 Proof.
-  unfold W8, W32.
-  autorewrite with word.
-  rewrite word.unsigned_of_Z.
-  rewrite word_wrap_wrap'; last lia.
-  reflexivity.
+  word.
 Qed.
 
 Lemma val_u8_to_u32 (x:w8) :
   uint.Z (W32 (uint.Z x)) = uint.Z x.
 Proof.
-  unfold W32.
-  rewrite word.unsigned_of_Z.
-  pose proof (word.unsigned_range x).
-  rewrite wrap_small; lia.
+  word.
 Qed.
 
 Lemma val_u8_to_u64 (x:w8) :
   uint.Z (W64 (uint.Z x)) = uint.Z x.
 Proof.
-  unfold W64.
-  rewrite word.unsigned_of_Z.
-  pose proof (word.unsigned_range x).
-  rewrite wrap_small; lia.
+  word.
 Qed.
 
 Lemma word_wrap_8_nonneg (x : Z) : 0 ≤ x -> 0 ≤ word.wrap (width:=8) x.

src/program_proof/addr/addr_proof.v

@@ -811,10 +811,7 @@ Proof.
   wp_rec. wp_pures.
   iApply "HΦ".
   iPureIntro.
-
-  word_cleanup.
-  rewrite ?word.unsigned_mul. (* XXX why is this needed? *)
-  word_cleanup.
+  word.
 Qed.
 
 End heap.

src/program_proof/alloc/alloc_proof.v

@@ -370,7 +370,7 @@ Proof.
     iExists _, _; iFrame.
     iPureIntro.
     pose proof (and_1_u8 x).
-    word_cleanup.
+    word.
   - iExists _, _; iFrame.
     iPureIntro.
     word.
@@ -433,8 +433,6 @@ Proof.
     iModIntro.
     iApply "HΦ".
     iPureIntro.
-    word_cleanup.
-    rewrite word.unsigned_mul.
     word.
 Qed.
 

src/program_proof/aof/proof.v

@@ -931,13 +931,7 @@ Proof.
   wp_loadField.
   wp_pures.
   rewrite -HnewDataSafe in Hsz.
-  assert (W64 (length newData) = data_sl.(Slice.sz)) as HH.
-  {
-    apply Z2Nat.inj in Hsz.
-    { word_cleanup. naive_solver. }
-    { word_cleanup. naive_solver. }
-    word.
-  }
+  assert (W64 (length newData) = data_sl.(Slice.sz)) as HH by word.
   rewrite -HH.
   rewrite -HH in HnoOverflow.
   wp_pures.
@@ -1017,44 +1011,8 @@ Proof.
     rewrite -Hlengthsafe.
     repeat (rewrite Nat2Z.inj_add).
     replace (length newData) with (Z.to_nat (Z.of_nat (length newData))) by lia.
-    rewrite -Z2Nat.inj_add.
-    {
-      rewrite Z2Nat.inj_iff.
-      {
-        rewrite Z2Nat.id.
-        {
-          rewrite wrap_small; first word.
-          split.
-          {
-            apply Z.add_nonneg_nonneg; word_cleanup; naive_solver.
-          }
-          {
-            rewrite Nat2Z.id.
-            rewrite -HnewDataSafe.
-            replace (Z.of_nat (uint.nat (length newData))) with (uint.Z (length newData)); last first.
-            { rewrite u64_Z_through_nat. done. }
-            destruct (bool_decide (uint.Z (length (predurableC ++ membufC)) + (uint.Z (length newData)) < 2 ^ 64))%Z eqn:Hnov.
-            { apply bool_decide_eq_true in Hnov. done. }
-            {
-              apply bool_decide_eq_false in Hnov.
-              word.
-            }
-          }
-        }
-        naive_solver.
-      }
-      {
-        word_cleanup.
-        unfold word.wrap.
-        by apply Z_mod_lt.
-      }
-      {
-        word_cleanup.
-        apply Z.add_nonneg_nonneg; word_cleanup; naive_solver.
-      }
-    }
-    { naive_solver. }
-    { lia. }
+    rewrite /list_safe_size in HnewDataSafe.
+    word.
   }
 
   iAssert (|={⊤}=> (P (γ.(initdata) ++ predurableC) -∗ fmlist_lb γ.(durabledata) (γ.(initdata) ++ predurableC ++ membufC')
@@ -1207,11 +1165,7 @@ Proof.
         (W64 (length (predurableC ++ membufC'))); last first.
     {
       repeat rewrite length_app.
-      rewrite -word.ring_morph_add.
-      word_cleanup.
-      repeat (rewrite Nat2Z.inj_add).
-      rewrite Z.add_assoc.
-      done.
+      word.
     }
     iFrame.
     done.
@@ -1228,11 +1182,7 @@ Proof.
   { iFrame "#". }
 
   repeat rewrite length_app.
-  repeat (rewrite Nat2Z.inj_add).
-  rewrite Z.add_assoc.
-  rewrite -word.ring_morph_add.
-  unfold W64.
-  done.
+  word.
 Qed.
 
 Lemma wp_AppendOnlyFile__WaitAppend aof_ptr γ (l:u64) fname P Pcrash :

src/program_proof/lockmap_proof.v

@@ -594,8 +594,7 @@ Proof.
     2: { unseal_nshard. word. }
     iDestruct (big_sepS_insert with "Hpp") as "[Hp Hpp]".
     { unseal_nshard. intro Hx.
-      apply rangeSet_lookup in Hx; try word.
-      intuition. revert H. word. }
+      apply rangeSet_lookup in Hx; try word. }
     wp_apply (wp_mkLockShard with "Hp").
     iIntros (ls gh) "Hls".
     wp_load.

src/program_proof/marshal_stateless_proof.v

@@ -132,7 +132,7 @@ Proof.
   wp_load.
   wp_if_destruct.
   - wp_store. wp_load. iApply "HΦ". iPureIntro. done.
-  - wp_load. iApply "HΦ". iPureIntro. word.
+  - wp_load. iApply "HΦ". iPureIntro. move: Heqb. word.
 Qed.
 
 Local Theorem wp_reserve s (extra : u64) (vs : list u8) :

src/program_proof/memkv/memkv_coord_make_proof.v

@@ -176,19 +176,15 @@ Proof.
         rewrite Heq_uNSHARD /uNSHARD in Hlen_shardMapping.
         word_cleanup.
         rewrite -Hlen_shardMapping in Hle.
-        rewrite Z_u64 ?Nat2Z.id in Hle; word_cleanup.
+        word.
       }
       iDestruct "H" as (??) "H". iExists _.
       assert (host = hid) as ->.
       {
         assert (uint.nat (W64 (Z.of_nat sid)) = sid) as Hcoerce.
-        { word_cleanup.
-          rewrite wrap_small; first lia.
-          { split.
-          * lia.
-          *  apply lookup_lt_Some in Hlookup.
-            rewrite Heq_uNSHARD /uNSHARD in Hlen_shardMapping. lia.
-          }
+        { apply lookup_lt_Some in Hlookup.
+          rewrite Heq_uNSHARD /uNSHARD in Hlen_shardMapping.
+          word.
         }
         { rewrite Hcoerce in Hlookup2. congruence. }
       }

src/program_proof/memkv/memkv_coord_start_proof.v

@@ -314,8 +314,7 @@ Proof.
       iIntros (fl) "(H1&H2)".
       iDestruct (typed_slice.own_slice_small_acc with "HshardMap_sl") as "[HshardMap_sl HshardMap_close]".
       wp_apply (wp_encodeShardMap with "[$]").
-      { word_cleanup. rewrite wrap_small; last (rewrite /uNSHARD; lia).
-        rewrite -Hlen_shardMapping. lia. }
+      { word. }
       iIntros (sl data) "(%Henc&H)".
       wp_apply (wp_StoreAt with "[$]").
       { apply slice_val_ty. }

src/program_proof/memkv/memkv_marshal_install_shard_proof.v

@@ -719,13 +719,11 @@ Proof.
     replace (word.add (size mdone') 1) with (uint.Z (size mdone') + 1:u64) by word.
     rewrite Z_u64; last first.
     { split; first lia.
-      word_cleanup.
-      rewrite Hsize in Heqb.
       assert (size mdone' ≤ size m)%nat.
       { rewrite -Hunion.
         rewrite ?Map.map_size_dom.
         apply subseteq_size. set_solver. }
-      lia.
+      word.
     }
     replace (Z.of_nat (S (size mdone'))) with (size mdone' + 1)%Z by lia.
     iFrame.
@@ -762,8 +760,7 @@ Proof.
   {
     exfalso.
     set (mtodo:=(list_to_map (p :: l'))) in *.
-    assert (size m <= size mdone').
-    { rewrite ?Z_u64 in Heqb; try word. }
+    assert (size m <= size mdone') by word.
     rewrite -Hunion in Heqb.
     rewrite map_size_disj_union in Heqb; eauto.
     assert (size mtodo > 0).

src/program_proof/rsm/spaxos_propose.v

@@ -934,7 +934,7 @@ Proof.
   iApply "HΦ". iPureIntro.
   case_bool_decide as Hlt; last done.
   unfold reached_quorum.
-  rewrite word.unsigned_divu_nowrap in Hlt; word.
+  rewrite word.unsigned_divu_nowrap in Hlt; try word.
 Qed.
 
 Lemma ite_apply (A B : Type) (b : bool) (f : A -> B) x y :

src/program_proof/verus/wrsmulti.v

@@ -215,6 +215,7 @@ Proof.
     rewrite take_ge.
     2: {
       rewrite -Hlen2 Hslicesz.
+      word_cleanup.
       (* FIXME: would be nice if [word] could handle this. *)
       rewrite Z_u64 in Heqb. 2: word. word.
     }