Make word more powerful

- Use div_mod_to_equations and unfold word.wrap locally but only if it
  solves the goal
- Make progress on disequalities between words by proving their Z values
  differ.

src/Helpers/Integers.v

@@ -188,11 +188,11 @@ Proof.
 Qed.
 
 Theorem swrap_small `{word: Interface.word width} {ok: word.ok word} (x:Z) :
-  width > 0 ->
   -(2^(width-1)) <= x < 2^(width-1) ->
   @word.swrap _ word x = x.
 Proof.
   unfold word.swrap; intros.
+  pose proof (ok.(word.width_pos)).
   unshelve epose proof ZLib.Z.pow2_times2 width _; first by lia.
   rewrite Zmod_small; lia.
 Qed.
@@ -226,15 +226,15 @@ Theorem s8_to_s64_Z (x:w8) : sint.Z (W64 (sint.Z x)) = sint.Z x.
 Proof.
   unfold W64.
   rewrite word.signed_of_Z.
-  rewrite swrap_small; auto; first by lia.
+  rewrite swrap_small; auto.
   pose proof (word.signed_range x); lia.
 Qed.
 
 Theorem s32_to_s64_Z (x:w32) : sint.Z (W64 (sint.Z x)) = sint.Z x.
 Proof.
   unfold W64.
   rewrite word.signed_of_Z.
-  rewrite swrap_small; auto; first by lia.
+  rewrite swrap_small; auto.
   pose proof (word.signed_range x); lia.
 Qed.
 
@@ -243,7 +243,7 @@ Theorem s32_from_s64_Z (x: w64) : -2^(32-1) ≤ sint.Z x < 2^(32-1) ->
 Proof.
   unfold W32; intros.
   rewrite word.signed_of_Z.
-  rewrite swrap_small; auto; first by lia.
+  rewrite swrap_small; auto.
 Qed.
 
 Theorem tuple_to_list_length A n (t: tuple A n) :
@@ -471,6 +471,11 @@ Proof.
   - apply (inj sint.Z); auto.
 Qed.
 
+Lemma f_not_equal {A B} (f: A → B) (x y: A) :
+  f x ≠ f y →
+  x ≠ y.
+Proof. congruence. Qed.
+
 Lemma word_unsigned_ltu {width: Z} (word: Interface.word width) {Hok: word.ok word} (x y: word) :
   word.ltu x y = bool_decide (uint.Z x < uint.Z y).
 Proof.
@@ -494,12 +499,18 @@ Qed.
 
 Create HintDb word.
 
-Ltac word_cleanup :=
+Ltac word_cleanup_core :=
   repeat autounfold with word in *;
-  try match goal with
+  try lazymatch goal with
+      (* TODO: this isn't the right strategy if the numbers in the goal are used
+      signed. [word] can try both via backtracking, but this can't be part of
+      "cleanup".  *)
       | |- @eq u64 _ _ => apply word.unsigned_inj
       | |- @eq u32 _ _ => apply word.unsigned_inj
       | |- @eq u8 _ _ => apply word.unsigned_inj
+      | |- not (@eq u64 _ _) => apply (f_not_equal uint.Z)
+      | |- not (@eq u32 _ _) => apply (f_not_equal uint.Z)
+      | |- not (@eq u8 _ _) => apply (f_not_equal uint.Z)
       end;
   (* can't replace this with [autorewrite], probably because typeclass inference
   isn't the same *)
@@ -533,16 +544,39 @@ Ltac word_cleanup :=
            | [ H': 0 <= uint.Z x < 2^_ |- _ ] => fail
            | _ => pose proof (word.unsigned_range x)
            end
+         | [ |- context[sint.Z ?x] ] =>
+           lazymatch goal with
+           | [ H': - (2^ _) ≤ sint.Z x < 2^_ |- _ ] => fail
+           | _ => pose proof (word.signed_range x)
+           end
+         | [ H: context[sint.Z ?x] |- _ ] =>
+           lazymatch goal with
+           | [ H': - (2^ _) ≤ sint.Z x < 2^_ |- _ ] => fail
+           | _ => pose proof (word.signed_range x)
+           end
          end;
   repeat match goal with
          | |- context[@word.wrap _ ?word ?ok ?z] =>
            rewrite (@wrap_small _ word ok z) by lia
+         | |- context[@word.swrap _ ?word ?ok ?z] =>
+           rewrite (@swrap_small _ word ok z) by lia
          | |- context[Z.of_nat (Z.to_nat ?z)] =>
            rewrite (Z2Nat.id z) by lia
-         end;
-  try lia.
+         end.
+
+(* TODO: only for backwards compatibility.
+
+[word_cleanup] should be be replaced with a new tactic
+that does a subset of safe and useful rewrites *)
+Ltac word_cleanup := word_cleanup_core; try lia.
 
-Ltac word := solve [ word_cleanup ].
+Ltac word := 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
+               ].
 
 Theorem Z_u32 z :
   0 <= z < 2 ^ 32 ->
@@ -640,31 +674,9 @@ Lemma u64_round_up_spec x div :
   uint.Z (u64_round_up x div) < 2^64.
 Proof.
   intros. unfold u64_round_up.
-  rewrite word.unsigned_mul, word.unsigned_divu. 2:word.
-  rewrite word.unsigned_add.
-  rewrite (wrap_small (_ + _)). 2:word.
-  rewrite (wrap_small (_ `div` _)).
-  2:{
-    split.
-    - apply Z_div_nonneg_nonneg; word.
-    - assert (0 < word.unsigned div) as Hdiv by lia.
-      pose proof (ZLib.Z.div_mul_undo_le (uint.Z x + uint.Z div) (uint.Z div) Hdiv) as Hdivle.
-      lia. }
-  rewrite wrap_small.
-  2:{
-    split.
-    - apply Z.mul_nonneg_nonneg. 2:word. apply Z_div_nonneg_nonneg; word.
-    - apply Z.lt_le_pred. etrans. 1: apply ZLib.Z.div_mul_undo_le. all: word. }
+  rewrite -> word.unsigned_mul_nowrap, word.unsigned_divu_nowrap by word.
+  rewrite -> word.unsigned_add_nowrap by word.
   split.
   { rewrite Z.mul_comm. apply ZLib.Z.Z_mod_mult'. }
-  set (x' := uint.Z x).
-  set (div' := uint.Z div).
-  opose proof (Z.div_mod (x' + div') div' _) as Heq. 1:word.
-  replace ((x' + div') `div` div' * div') with (x' + div' - (x' + div') `mod` div') by lia.
-  assert ((x' + div') `mod` div' < div').
-  { apply Z.mod_pos_bound. lia. }
-  split.
-  { apply Z.le_succ_l. lia. }
-  assert (0 ≤ (x' + div') `mod` div'). 2:lia.
-  apply Z_mod_nonneg_nonneg; word.
+  word.
 Qed.

src/Helpers/range_set.v

@@ -62,7 +62,7 @@ Proof.
       simpl. repeat f_equal; lia.
     + intro H.
       eapply rangeSet_lookup in H; try lia.
-      intuition idtac. revert H0. word_cleanup.
+      intuition idtac. revert H0. word.
 Qed.
 
 Lemma rangeSet_append_one:

src/goose_lang/ffi/grove_ffi/grove_ffi.v

@@ -649,8 +649,7 @@ lemmas. *)
       destruct (Z.leb (uint.Z _) (uint.Z (word.add _ _))) eqn:Hlt.
       {
         rewrite Z.leb_le in Hlt.
-        apply Z2Nat.inj_le; [try word..|].
-        { apply word.unsigned_range. }
+        apply Z2Nat.inj_le; [word..|].
         done.
       }
       { word. }

src/program_proof/alloc/alloc_proof.v

@@ -125,8 +125,6 @@ Proof.
   wp_pures. by iApply "HΦ".
 Qed.
 
-Local Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.
-
 Lemma wp_MkMaxAlloc (max: u64) :
   0 < uint.Z max →
   uint.Z max `mod` 8 = 0 →
@@ -441,5 +439,3 @@ Proof.
 Qed.
 
 End proof.
-
-Ltac Zify.zify_post_hook ::= idtac.

src/program_proof/examples/async_mem_alloc_dir_proof.v

@@ -624,10 +624,7 @@ Section goose.
         iIntros (???) "Hpre".
         change (uint.Z (W64 5)) with 5%Z in Hbound'.
         iExactEq "Hpre".
-        f_equal; len.
-        rewrite H /num_inodes.
-        replace (uint.nat i `min` 5)%nat with (uint.nat i) by lia.
-        f_equal. }
+        f_equal; len. }
     iIntros "!> (Hinv&Haddr)". iNamed "Hinv".
     change (uint.Z (W64 5)) with 5%Z.
     rewrite -> take_ge by word.
@@ -815,6 +812,7 @@ Section goose.
     {{{ l, RET #l; pre_dir l (uint.Z sz) σ0 }}}
     {{{ dir_cinv (uint.Z sz) σ0 false }}}.
   Proof using Type* - P.
+    clear P.
     iIntros (? Φ Φc) "Hcinv HΦ".
     wpc_call.
     { iApply dir_cinv_post_crash; auto. }

src/program_proof/examples/dir_proof.v

@@ -592,10 +592,7 @@ Section goose.
         iIntros (???) "Hpre".
         change (uint.Z (W64 5)) with 5%Z in Hbound'.
         iExactEq "Hpre".
-        f_equal; len.
-        rewrite H /num_inodes.
-        replace (uint.nat i `min` 5)%nat with (uint.nat i) by lia.
-        f_equal. }
+        f_equal; len. }
     iIntros "!> (Hinv&Haddr)". iNamed "Hinv".
     change (uint.Z (W64 5)) with 5%Z.
     rewrite -> take_ge by word.
@@ -783,6 +780,7 @@ Section goose.
     {{{ l, RET #l; pre_dir l (uint.Z sz) σ0 }}}
     {{{ dir_cinv (uint.Z sz) σ0 false }}}.
   Proof using Type* - P.
+    clear P.
     iIntros (? Φ Φc) "Hcinv HΦ".
     wpc_call.
     { iApply dir_cinv_post_crash; auto. }

src/program_proof/examples/single_inode_proof.v

@@ -167,6 +167,7 @@ Section goose.
     {{{ l, RET #l; pre_s_inode l (uint.Z sz) σ0 }}}
     {{{ s_inode_cinv (uint.Z sz) σ0 true }}}.
   Proof.
+    clear P.
     iIntros (? Φ Φc) "Hpre HΦ"; iNamed "Hpre".
     rewrite /Open.
     wpc_call.

src/program_proof/lockmap_proof.v

@@ -445,8 +445,6 @@ Definition NSHARD_eq : @NSHARD = @NSHARD_def := NSHARD_aux.(seal_eq).
 
 Ltac unseal_nshard := rewrite NSHARD_eq /NSHARD_def.
 
-Local Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.
-
 Definition covered_by_shard (shardnum : Z) (covered: gset u64) : gset u64 :=
   filter (λ x, Z.modulo (uint.Z x) NSHARD = shardnum) covered.
 
@@ -493,8 +491,7 @@ Lemma rangeSet_lookup_mod (x : u64) (n : Z) :
 Proof.
   intros.
   apply rangeSet_lookup; try word.
-  word_cleanup.
-  word.
+  repeat word_cleanup; word.
 Qed.
 
 Lemma covered_by_shard_split (P : u64 -> iProp Σ) covered :

src/program_proof/wal/circ_proof.v

@@ -58,7 +58,6 @@ Context `{!heapGS Σ}.
 Context `{!circG Σ}.
 
 Context (N: namespace).
-Context (P: circΣ.t -> iProp Σ).
 
 Record circ_names : Set :=
   { addrs_name: gname;
@@ -276,6 +275,8 @@ Definition circular_crash_ghost_exchange (γold γnew : circ_names) : iProp Σ :
   (diskEnd_is γold (1/2) dend ∨ diskEnd_is γnew (1/2) dend).
 *)
 
+Context (P: circΣ.t -> iProp Σ).
+
 Definition is_circular γ : iProp Σ :=
   ncinv N (∃ σ, is_circular_state γ σ ∗ P σ).
 
@@ -533,6 +534,7 @@ Lemma diskEnd_advance_unchanged:
              (set upds (drop (Z.to_nat (uint.Z newStart - uint.Z (start σ)))) σ))
     = circΣ.diskEnd σ.
 Proof.
+  clear P.
   rewrite /circΣ.diskEnd /=.
   intros.
   len.
@@ -570,6 +572,7 @@ Lemma circ_positions_advance (newStart: u64) γ σ (start0: u64) :
                         (set upds (drop (Z.to_nat (uint.Z newStart - uint.Z (start σ)))) σ)) ∗
   start_is γ (1/2) newStart ∗ start_at_least γ newStart.
 Proof.
+  clear P.
   iIntros (Hwf Hmono) "[Hpos Hstart1]".
   iDestruct (start_is_to_eq with "[$] [$]") as %?; subst.
   iDestruct "Hpos" as "[Hstart2 Hend2]".
@@ -981,8 +984,7 @@ Proof.
   induction upds; simpl; intros; auto.
   rewrite -> IHupds by word.
   rewrite list_lookup_insert_ne; auto.
-  apply Zto_nat_neq_inj; try (mod_bound; word).
-  apply mod_neq_gt; try word.
+  word.
 Qed.
 
 Theorem lookup_update_circ_new {A B} (f: A -> B) xs (endpos: Z) upds i :
@@ -1070,6 +1072,7 @@ Lemma circ_positions_append upds γ σ (startpos endpos: u64) :
   |==> circ_positions γ (set circ_proof.upds (λ u : list update.t, u ++ upds) σ) ∗
        diskEnd_is γ (1/2) (uint.Z endpos + length upds).
 Proof.
+  clear P.
   iIntros (Hendpos_overflow Hhasspace) "[$ Hend1] #Hstart Hend2".
   rewrite /circΣ.diskEnd /=; autorewrite with len.
   iDestruct (diskEnd_is_agree with "Hend1 Hend2") as %Heq; rewrite Heq.

src/program_proof/wal/circ_proof_crash.v

@@ -129,6 +129,7 @@ Lemma circular_init :
             start_is γ (1/2) (W64 0) ∗
             diskEnd_is γ (1/2) 0.
 Proof.
+  clear P.
   set (σ:={| upds := []; start := W64 0; |}).
   assert (circΣ.diskEnd σ = 0) as HdiskEnd by reflexivity.
   rewrite split_513_blocks.
@@ -279,8 +280,6 @@ Proof.
     wpc_frame_seq.
     wp_load.
     list_elem addrs0 (uint.Z i `mod` LogSz) as a.
-    { destruct Hlow_wf.
-      mod_bound; word. }
     wp_apply (wp_SliceGet _ _ _ _ (DfracOwn 1) addrs0 with "[$Hdiskaddrs]"); eauto.
     { iPureIntro.
       change (word.divu _ _) with (W64 LogSz).

src/program_proof/wal/common_proof.v

@@ -191,6 +191,7 @@ Lemma is_txn_mid σ (a b c : nat) pos :
   a ≤ b ≤ c ->
   is_txn σ.(log_state.txns) b pos.
 Proof.
+  clear P.
   rewrite /is_txn /wal_wf; intros Hwf Ha Hc Hle.
   destruct Hwf as [_ [Hwf _]].
   destruct (decide (a < b)).

src/program_proof/wal/invariant.v

@@ -923,6 +923,7 @@ Lemma wal_wf_txns_mono_pos {σ txn_id1 pos1 txn_id2 pos2} :
   uint.Z pos1 < uint.Z pos2 ->
   (txn_id1 < txn_id2)%nat.
 Proof.
+  clear P.
   destruct 1 as (_&Hmono&_).
   destruct (decide (txn_id1 = txn_id2)).
   { subst. intros.
@@ -959,6 +960,7 @@ Lemma wal_wf_txns_mono_highest {σ txn_id1 pos1 txn_id2 pos2} :
   uint.Z pos1 ≤ uint.Z pos2 ->
   (txn_id1 ≤ txn_id2)%nat.
 Proof.
+  clear P.
   intros Hwf Htxn1 Htxn2 Hle.
   destruct (decide (pos1 = pos2)); subst.
   - apply Htxn2 in Htxn1; lia.

src/program_proof/wal/recovery_proof.v

@@ -112,6 +112,7 @@ Lemma log_crash_to_wf σ σ' x :
   relation.denote log_crash σ σ' x →
   wal_wf σ'.
 Proof.
+  clear P.
   simpl.
   intros Hwf Htrans; monad_inv.
   destruct Hwf as (Haddrs&Hmono&Hb1&hb2).

src/program_proof/wal/write_proof.v

@@ -206,6 +206,7 @@ Lemma is_mem_memLog_append (bs : list update.t) (σ : locked_state) (σs : log_s
                     (σs.(log_state.txns) ++ [(slidingM.endPos (memWrite σ.(memLog) bs), bs)])
                     memStart_txn_id.
 Proof.
+  clear P.
   intros Hwf HmemStart_bound.
   rewrite /is_mem_memLog /has_updates.
   intros [Hupdates Hpos_bound].