more suggestions from MR and unfolding lemmas

theories/bitvector.v

@@ -101,11 +101,14 @@ Definition bv_modulus (n : N) : Z := 2 ^ (Z.of_N n).
 Definition bv_half_modulus (n : N) : Z := bv_modulus n `div` 2.
 Definition bv_wrap (n : N) (z : Z) : Z := z `mod` bv_modulus n.
 Definition bv_swrap (n : N) (z : Z) : Z := bv_wrap n (z + bv_half_modulus n) - bv_half_modulus n.
-Definition bv_wf (n : N) (z : Z) : Prop := -1 < z < bv_modulus n.
+Local Definition bv_wf (n : N) (z : Z) : Prop := -1 < z < bv_modulus n.
 
 Lemma bv_modulus_pos n :
   0 < bv_modulus n.
 Proof. apply Z.pow_pos_nonneg; lia. Qed.
+Lemma bv_half_modulus_nonneg n :
+  0 ≤ bv_half_modulus n.
+Proof. apply Z.div_pos; [|done]. pose proof bv_modulus_pos n. lia. Qed.
 
 Lemma bv_modulus_add n1 n2 :
   bv_modulus (n1 + n2) = bv_modulus n1 * bv_modulus n2.
@@ -120,6 +123,25 @@ Proof.
   rewrite <-Z_pow_pred_r by lia. rewrite Z.mul_comm. by apply Z.mod_mul.
 Qed.
 
+Lemma bv_half_modulus_lt_modulus n:
+  bv_half_modulus n < bv_modulus n.
+Proof.
+  pose proof bv_modulus_pos n.
+  apply Z_div_lt; [done| lia].
+Qed.
+
+Lemma bv_modulus_le_mono n m:
+  (n ≤ m)%N →
+  bv_modulus n ≤ bv_modulus m.
+Proof. intros. apply Z.pow_le_mono; [done|lia]. Qed.
+Lemma bv_half_modulus_le_mono n m:
+  (n ≤ m)%N →
+  bv_half_modulus n ≤ bv_half_modulus m.
+Proof. intros. apply Z.div_le_mono; [done|]. by apply bv_modulus_le_mono. Qed.
+
+Lemma bv_modulus_0:
+  bv_modulus 0 = 1.
+Proof. done. Qed.
 Lemma bv_half_modulus_0:
   bv_half_modulus 0 = 0.
 Proof. done. Qed.
@@ -132,18 +154,50 @@ Lemma bv_wf_in_range n z:
   bv_wf n z ↔ 0 ≤ z < bv_modulus n.
 Proof. unfold bv_wf. lia. Qed.
 
-Lemma bv_wrap_wf n z :
-  bv_wf n (bv_wrap n z).
+Lemma bv_wrap_in_range n z:
+  0 ≤ bv_wrap n z < bv_modulus n.
+Proof. apply Z.mod_pos_bound. apply bv_modulus_pos. Qed.
+
+Lemma bv_swrap_in_range n z:
+  n ≠ 0%N →
+  - bv_half_modulus n ≤ bv_swrap n z < bv_half_modulus n.
 Proof.
-  unfold bv_wrap.
-  pose proof (Z.mod_pos_bound z (bv_modulus n)) as [??]. { apply bv_modulus_pos. }
-  split; lia.
+  intros ?. unfold bv_swrap.
+  pose proof bv_half_modulus_twice n.
+  pose proof bv_wrap_in_range n (z + bv_half_modulus n).
+  lia.
 Qed.
 
+Lemma bv_wrap_wf n z :
+  bv_wf n (bv_wrap n z).
+Proof. pose proof (bv_wrap_in_range n z). split; lia. Qed.
+
 Lemma bv_wrap_small n z :
   0 ≤ z < bv_modulus n → bv_wrap n z = z.
 Proof. intros. by apply Z.mod_small. Qed.
 
+Lemma bv_swrap_small n z :
+  - bv_half_modulus n ≤ z < bv_half_modulus n →
+  bv_swrap n z = z.
+Proof.
+  intros Hrange. unfold bv_swrap.
+  destruct (decide (n = 0%N)); subst.
+  { rewrite bv_half_modulus_0 in Hrange. lia. }
+  pose proof bv_half_modulus_twice n.
+  rewrite bv_wrap_small by lia. lia.
+Qed.
+
+Lemma bv_wrap_0 n :
+  bv_wrap n 0 = 0.
+Proof. done. Qed.
+Lemma bv_swrap_0 n :
+  bv_swrap n 0 = 0.
+Proof.
+  pose proof bv_half_modulus_lt_modulus n.
+  pose proof bv_half_modulus_nonneg n.
+  unfold bv_swrap. rewrite bv_wrap_small; lia.
+Qed.
+
 Definition bv_wrap_factor (n : N) (x z : Z) :=
   x = - z `div` bv_modulus n.
 
@@ -213,37 +267,21 @@ Record bv (n : N) := BV {
 }.
 Global Arguments bv_unsigned {_}.
 Global Arguments bv_is_wf {_}.
+Add Printing Constructor bv.
+
+Global Arguments bv_unsigned : simpl never.
 
 Definition bv_signed {n} (b : bv n) := bv_swrap n (bv_unsigned b).
 
 Lemma bv_eq n (b1 b2 : bv n) :
   b1 = b2 ↔ b1.(bv_unsigned) = b2.(bv_unsigned).
 Proof.
-  destruct b1, b2. split; simpl; [ naive_solver|].
+  destruct b1, b2. unfold bv_unsigned. split; [ naive_solver|].
   intros. subst. f_equal. apply proof_irrel.
 Qed.
 
-Global Program Instance bv_eq_dec n : EqDecision (bv n) := λ '(BV _ v1 p1) '(BV _ v2 p2),
-   match decide (v1 = v2) with
-   | left eqv => left _
-   | right eqv => right _
-   end.
-Next Obligation. intros. subst. rewrite (proof_irrel p1 p2). exact eq_refl. Defined.
-Next Obligation. intros. by injection. Qed.
-
-Global Instance bv_countable n : Countable (bv n).
-Proof.
-  refine (inj_countable bv_unsigned
-    (λ x, match decide (bv_wf n x) with | left b => Some (BV n x b) | _ => None end) _).
-  intros x. case_decide; [ f_equal; by apply bv_eq|].
-  by pose proof bv_is_wf x.
-Qed.
-
 Definition bv_of_Z_checked (n : N) (z : Z) : option (bv n) :=
-  match decide (bv_wf n z) with
-  | left Heq => Some (BV n z Heq)
-  | right _ => None
-  end.
+  guard (bv_wf n z) as H; Some (BV n z H).
 
 Program Definition bv_of_Z (n : N) (z : Z) : bv n :=
   BV n (bv_wrap n z) _.
@@ -257,18 +295,47 @@ Lemma bv_of_Z_signed n z:
   bv_signed (bv_of_Z n z) = bv_swrap n z.
 Proof. apply bv_swrap_wrap. Qed.
 
-Global Arguments bv_of_Z : simpl never.
-Global Opaque bv_of_Z.
-
 Lemma bv_of_Z_small n z:
   0 ≤ z < bv_modulus n →
   bv_unsigned (bv_of_Z n z) = z.
 Proof. rewrite bv_of_Z_unsigned. apply bv_wrap_small. Qed.
 
-Lemma bv_in_range n (b : bv n):
+Lemma bv_unsigned_in_range n (b : bv n):
   0 ≤ bv_unsigned b < bv_modulus n.
 Proof. apply bv_wf_in_range. apply bv_is_wf. Qed.
 
+Lemma bv_signed_in_range n (b : bv n):
+  n ≠ 0%N →
+  - bv_half_modulus n ≤ bv_signed b < bv_half_modulus n.
+Proof. apply bv_swrap_in_range. Qed.
+
+Lemma bv_unsigned_N_0 (b : bv 0):
+  bv_unsigned b = 0.
+Proof.
+  pose proof bv_unsigned_in_range 0 b as H.
+  rewrite bv_modulus_0 in H. lia.
+Qed.
+Lemma bv_signed_N_0 (b : bv 0):
+  bv_signed b = 0.
+Proof. unfold bv_signed. by rewrite bv_unsigned_N_0, bv_swrap_0. Qed.
+
+
+Global Program Instance bv_eq_dec n : EqDecision (bv n) := λ '(BV _ v1 p1) '(BV _ v2 p2),
+   match decide (v1 = v2) with
+   | left eqv => left _
+   | right eqv => right _
+   end.
+Next Obligation. intros. subst. rewrite (proof_irrel p1 p2). exact eq_refl. Defined.
+Next Obligation. intros. by injection. Qed.
+
+Global Program Instance bv_countable n : Countable (bv n) :=
+  inj_countable bv_unsigned (bv_of_Z_checked n) _.
+Next Obligation.
+  intros n x. pose proof bv_is_wf x.
+  unfold bv_of_Z_checked. case_option_guard; [|done].
+  f_equal. by apply bv_eq.
+Qed.
+
 Global Program Instance bv_finite n : Finite (bv n) :=
   {| enum := bv_of_Z n <$> (seqZ 0 (bv_modulus n)) |}.
 Next Obligation.
@@ -281,7 +348,7 @@ Qed.
 Next Obligation.
   intros. apply elem_of_list_lookup. eexists (Z.to_nat (bv_unsigned x)).
   rewrite list_lookup_fmap. apply fmap_Some. eexists _.
-  pose proof (bv_in_range _ x). split.
+  pose proof (bv_unsigned_in_range _ x). split.
   - apply lookup_seqZ. split; [done|]. rewrite Z2Nat.id; lia.
   - apply bv_eq. rewrite bv_of_Z_small; rewrite Z2Nat.id; lia.
 Qed.
@@ -303,7 +370,9 @@ Notation "'[BV{' l }  v ]" := (BV l v ltac:(solve_bitvector_eq)) (at level 9, on
 
 (** * Automation *)
 Ltac bv_saturate :=
-  repeat match goal with | b : bv _ |- _ => learn_hyp (bv_in_range _ b) end.
+  repeat match goal with b : bv _ |- _ => first [
+     learn_hyp (bv_unsigned_in_range _ b) | learn_hyp (bv_signed_in_range _ b)
+  ] end.
 
 Definition bv_wrap_simplify_marker (z1 z2 : Z) : Z := z1 + z2.
 
@@ -356,6 +425,8 @@ Ltac bv_wrap_simplify_cancel :=
   first [ apply bv_wrap_simplify_marker_remove_end | apply bv_wrap_simplify_marker_remove_end_opp | apply bv_wrap_simplify_marker_move_end].
 
 Ltac bv_wrap_simplify :=
+  unfold bv_signed, bv_swrap;
+  try match goal with | |- _ - _ = _ - _ => f_equal end;
   match goal with
   | |- bv_wrap ?n1 ?z1 = bv_wrap ?n2 ?z2 => change (block bv_wrap n1 z1 = block bv_wrap n2 z2)
   end;
@@ -518,52 +589,178 @@ Definition bv_of_little n (bs : list (bv n)) : Z :=
 
 (** * Lemmas about [bv n] operations *)
 
-(** ** Lemmas about [bv_opp], [bv_add], and [bv_sub] *)
-Section add_sub.
+(** ** Unfolding lemmas for the operations. *)
+Section unfolding.
   Context {n : N}.
   Implicit Types (b : bv n).
 
-  Lemma bv_sub_add_opp b1 b2:
-    bv_sub b1 b2 = bv_add b1 (bv_opp b2).
-  Proof.
-    apply bv_eq. unfold bv_sub, bv_add, bv_opp.
-    rewrite !bv_of_Z_unsigned. bv_wrap_simplify_solve.
-  Qed.
-
+  Lemma bv_succ_unsigned b :
+    bv_unsigned (bv_succ b) = bv_wrap n (Z.succ (bv_unsigned b)).
+  Proof. done. Qed.
+  Lemma bv_succ_signed b :
+    bv_signed (bv_succ b) = bv_swrap n (Z.succ (bv_signed b)).
+  Proof. unfold bv_succ. rewrite bv_of_Z_signed. bv_wrap_simplify_solve. Qed.
+
+  Lemma bv_pred_unsigned b :
+    bv_unsigned (bv_pred b) = bv_wrap n (Z.pred (bv_unsigned b)).
+  Proof. done. Qed.
+  Lemma bv_pred_signed b :
+    bv_signed (bv_pred b) = bv_swrap n (Z.pred (bv_signed b)).
+  Proof. unfold bv_pred. rewrite bv_of_Z_signed. bv_wrap_simplify_solve. Qed.
+
+  Lemma bv_add_unsigned b1 b2 :
+    bv_unsigned (bv_add b1 b2) = bv_wrap n (bv_unsigned b1 + bv_unsigned b2).
+  Proof. done. Qed.
   Lemma bv_add_signed b1 b2 :
     bv_signed (bv_add b1 b2) = bv_swrap n (bv_signed b1 + bv_signed b2).
-  Proof.
-    unfold bv_add. rewrite bv_of_Z_signed. unfold bv_signed, bv_swrap. f_equal.
-    bv_wrap_simplify_solve.
-  Qed.
+  Proof. unfold bv_add. rewrite bv_of_Z_signed. bv_wrap_simplify_solve. Qed.
+
+  Lemma bv_sub_unsigned b1 b2 :
+    bv_unsigned (bv_sub b1 b2) = bv_wrap n (bv_unsigned b1 - bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_sub_signed b1 b2 :
+    bv_signed (bv_sub b1 b2) = bv_swrap n (bv_signed b1 - bv_signed b2).
+  Proof. unfold bv_sub. rewrite bv_of_Z_signed. bv_wrap_simplify_solve. Qed.
 
+  Lemma bv_opp_unsigned b :
+    bv_unsigned (bv_opp b) = bv_wrap n (- bv_unsigned b).
+  Proof. done. Qed.
   Lemma bv_opp_signed b :
     bv_signed (bv_opp b) = bv_swrap n (- bv_signed b).
-  Proof.
-    unfold bv_opp. rewrite bv_of_Z_signed. unfold bv_signed, bv_swrap. f_equal.
-    bv_wrap_simplify_solve.
-  Qed.
+  Proof. unfold bv_opp. rewrite bv_of_Z_signed. bv_wrap_simplify_solve. Qed.
 
-  Lemma bv_sub_signed b1 b2 :
-    bv_signed (bv_sub b1 b2) = bv_swrap n (bv_signed b1 - bv_signed b2).
+  Lemma bv_mul_unsigned b1 b2 :
+    bv_unsigned (bv_mul b1 b2) = bv_wrap n (bv_unsigned b1 * bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_mul_signed b1 b2 :
+    bv_signed (bv_mul b1 b2) = bv_swrap n (bv_signed b1 * bv_signed b2).
+  Proof. unfold bv_mul. rewrite bv_of_Z_signed. bv_wrap_simplify_solve. Qed.
+
+  Lemma bv_divu_unsigned b1 b2 :
+    bv_unsigned (bv_divu b1 b2) = Z.div (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_divu_signed b1 b2 :
+    bv_signed (bv_divu b1 b2) = bv_swrap n (Z.div (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+
+  Lemma bv_modu_unsigned b1 b2 :
+    bv_unsigned (bv_modu b1 b2) = Z.modulo (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_modu_signed b1 b2 :
+    bv_signed (bv_modu b1 b2) = bv_swrap n (Z.modulo (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+
+  Lemma bv_divs_unsigned b1 b2 :
+    bv_unsigned (bv_divs b1 b2) = bv_wrap n (Z.div (bv_signed b1) (bv_signed b2)).
+  Proof. done. Qed.
+  Lemma bv_divs_signed b1 b2 :
+    bv_signed (bv_divs b1 b2) = bv_swrap n (Z.div (bv_signed b1) (bv_signed b2)).
+  Proof. unfold bv_divs. rewrite bv_of_Z_signed. done. Qed.
+
+  Lemma bv_quots_unsigned b1 b2 :
+    bv_unsigned (bv_quots b1 b2) = bv_wrap n (Z.quot (bv_signed b1) (bv_signed b2)).
+  Proof. done. Qed.
+  Lemma bv_quots_signed b1 b2 :
+    bv_signed (bv_quots b1 b2) = bv_swrap n (Z.quot (bv_signed b1) (bv_signed b2)).
+  Proof. unfold bv_quots. rewrite bv_of_Z_signed. done. Qed.
+
+  Lemma bv_mods_unsigned b1 b2 :
+    bv_unsigned (bv_mods b1 b2) = bv_wrap n (Z.modulo (bv_signed b1) (bv_signed b2)).
+  Proof. done. Qed.
+  Lemma bv_mods_signed b1 b2 :
+    bv_signed (bv_mods b1 b2) = bv_swrap n (Z.modulo (bv_signed b1) (bv_signed b2)).
+  Proof. unfold bv_mods. rewrite bv_of_Z_signed. done. Qed.
+
+  Lemma bv_rems_unsigned b1 b2 :
+    bv_unsigned (bv_rems b1 b2) = bv_wrap n (Z.rem (bv_signed b1) (bv_signed b2)).
+  Proof. done. Qed.
+  Lemma bv_rem_signed b1 b2 :
+    bv_signed (bv_rems b1 b2) = bv_swrap n (Z.rem (bv_signed b1) (bv_signed b2)).
+  Proof. unfold bv_rems. rewrite bv_of_Z_signed. done. Qed.
+
+  Lemma bv_shiftl_unsigned b1 b2 :
+    bv_unsigned (bv_shiftl b1 b2) = bv_wrap n (Z.shiftl (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+  Lemma bv_shiftl_signed b1 b2 :
+    bv_signed (bv_shiftl b1 b2) = bv_swrap n (Z.shiftl (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. unfold bv_shiftl. rewrite bv_of_Z_signed. done. Qed.
+
+  Lemma bv_shiftr_unsigned b1 b2 :
+    bv_unsigned (bv_shiftr b1 b2) = Z.shiftr (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_shiftr_signed b1 b2 :
+    bv_signed (bv_shiftr b1 b2) = bv_swrap n (Z.shiftr (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+
+  Lemma bv_ashiftr_unsigned b1 b2 :
+    bv_unsigned (bv_ashiftr b1 b2) = bv_wrap n (Z.shiftr (bv_signed b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+  Lemma bv_ashiftr_signed b1 b2 :
+    bv_signed (bv_ashiftr b1 b2) = bv_swrap n (Z.shiftr (bv_signed b1) (bv_unsigned b2)).
+  Proof. unfold bv_ashiftr. rewrite bv_of_Z_signed. done. Qed.
+
+  Lemma bv_or_unsigned b1 b2 :
+    bv_unsigned (bv_or b1 b2) = Z.lor (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_or_signed b1 b2 :
+    bv_signed (bv_or b1 b2) = bv_swrap n (Z.lor (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+
+  Lemma bv_and_unsigned b1 b2 :
+    bv_unsigned (bv_and b1 b2) = Z.land (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_and_signed b1 b2 :
+    bv_signed (bv_and b1 b2) = bv_swrap n (Z.land (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+
+  Lemma bv_xor_unsigned b1 b2 :
+    bv_unsigned (bv_xor b1 b2) = Z.lxor (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_xor_signed b1 b2 :
+    bv_signed (bv_xor b1 b2) = bv_swrap n (Z.lxor (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+
+  Lemma bv_not_unsigned b :
+    bv_unsigned (bv_not b) = bv_wrap n (Z.lnot (bv_unsigned b)).
+  Proof. done. Qed.
+  Lemma bv_not_signed b :
+    bv_signed (bv_not b) = bv_swrap n (Z.lnot (bv_unsigned b)).
+  Proof. unfold bv_not. rewrite bv_of_Z_signed. done. Qed.
+
+  Lemma bv_zero_extend_unsigned z b :
+    bv_unsigned (bv_zero_extend z b) = bv_unsigned b.
+  Proof. done. Qed.
+  Lemma bv_zero_extend_signed z b :
+    bv_signed (bv_zero_extend z b) = bv_swrap (n + z) (bv_unsigned b).
+  Proof. done. Qed.
+
+  Lemma bv_sign_extend_unsigned z b :
+    bv_unsigned (bv_sign_extend z b) = bv_wrap (n + z) (bv_signed b).
+  Proof. done. Qed.
+  Lemma bv_sign_extend_signed z b :
+    bv_signed (bv_sign_extend z b) = bv_signed b.
   Proof.
-    unfold bv_sub. rewrite bv_of_Z_signed. unfold bv_signed, bv_swrap. f_equal.
-    bv_wrap_simplify_solve.
+    unfold bv_sign_extend. rewrite bv_of_Z_signed.
+    destruct (decide (n = 0%N)); subst.
+    { by rewrite bv_signed_N_0, bv_swrap_0. }
+    apply bv_swrap_small. bv_saturate.
+    pose proof bv_half_modulus_le_mono n (n + z). lia.
   Qed.
-End add_sub.
 
-(** ** Lemmas about [bv_mul] *)
-Section mul.
+End unfolding.
+
+(** ** Properties of bv operations *)
+Section properties.
   Context {n : N}.
   Implicit Types (b : bv n).
 
-  Lemma bv_mul_signed b1 b2 :
-    bv_signed (bv_mul b1 b2) = bv_swrap n (bv_signed b1 * bv_signed b2).
+  Lemma bv_sub_add_opp b1 b2:
+    bv_sub b1 b2 = bv_add b1 (bv_opp b2).
   Proof.
-    unfold bv_mul. rewrite bv_of_Z_signed. unfold bv_signed, bv_swrap. f_equal.
+    apply bv_eq. unfold bv_sub, bv_add, bv_opp. rewrite !bv_of_Z_unsigned.
     bv_wrap_simplify_solve.
   Qed.
-End mul.
+End properties.
 
 (** ** Lemmas about [bv_to_little] and [bv_of_little] *)
 Section little.
@@ -585,7 +782,7 @@ Section little.
   Proof.
     intros ->. eapply (fmap_inj bv_unsigned). { intros ???. by apply bv_eq. }
     rewrite bv_to_litte_unsigned. apply Z_to_of_little; [by rewrite fmap_length | lia |].
-    apply Forall_forall. intros ? [?[->?]]%elem_of_list_fmap_2. apply bv_in_range.
+    apply Forall_forall. intros ? [?[->?]]%elem_of_list_fmap_2. apply bv_unsigned_in_range.
   Qed.
 
   Lemma bv_of_to_little m n z:
@@ -665,7 +862,7 @@ End test_automation.
 Require Import Coq.micromega.ZifyClasses.
 
 Global Instance Inj_bv_Z n : InjTyp (bv n) Z :=
-  mkinj _ _ bv_unsigned (fun x => 0 ≤ x < bv_modulus n ) (bv_in_range _).
+  mkinj _ _ bv_unsigned (fun x => 0 ≤ x < bv_modulus n ) (bv_unsigned_in_range _).
 
 Global Instance Op_bv_unsigned n : UnOp bv_unsigned :=
   { TUOp := fun x => x ; TUOpInj := (fun x : bv n => @eq_refl Z (bv_unsigned x)) }.