wrap Zmod in Word.Naive

Author: andres-erbsen

src/coqutil/Word/Naive.v

@@ -1,28 +1,20 @@
-Require Import Coq.ZArith.BinIntDef Coq.ZArith.BinInt coqutil.Z.Lia.
+From Coq Require Import BinInt Zmod Bits.
 Require Import coqutil.Tactics.destr.
 Require Import coqutil.sanity coqutil.Word.Interface. Import word.
 Local Open Scope Z_scope.
 
-(* TODO: move me? *)
-Definition minimize_eq_proof{A: Type}(eq_dec: forall (x y: A), {x = y} + {x <> y}){x y: A}    (pf: x = y): x = y :=
-  match eq_dec x y with
-  | left p => p
-  | right n => match n pf: False with end
-  end.
-
 Section WithWidth. Local Set Default Proof Using "All".
   Context {width : Z}.
+  Definition rep : Set := bits width.
+  Definition unsigned (w : rep) := Zmod.unsigned w.
+
+  Definition wrap (z:Z) : rep := bits.of_Z width z.
+  Definition signed (w : rep) := Zmod.signed w.
+
   Let wrap_value z := z mod (2^width).
   Let swrap_value z := wrap_value (z + 2 ^ (width - 1)) - 2 ^ (width - 1).
-  Record rep : Set := mk { unsigned : Z ; _unsigned_in_range : wrap_value unsigned = unsigned }.
-
-  Definition wrap (z:Z) : rep :=
-    mk (wrap_value z) (minimize_eq_proof Z.eq_dec (Zdiv.Zmod_mod z _)).
-  Definition signed w := swrap_value (unsigned w).
 
   Record special_cases : Set := {
-    div_by_zero: Z -> Z;
-    mod_by_zero: Z -> Z;
     adjust_too_big_shift_amount: Z -> Z;
   }.
 
@@ -50,81 +42,113 @@ Section WithWidth. Local Set Default Proof Using "All".
     word.signed := signed;
     of_Z := wrap;
 
-    add x y := wrap (Z.add (unsigned x) (unsigned y));
-    sub x y := wrap (Z.sub (unsigned x) (unsigned y));
-    opp x := wrap (Z.opp (unsigned x));
+    add := Zmod.add;
+    sub := Zmod.sub;
+    opp := Zmod.opp;
 
-    or x y := wrap (Z.lor (unsigned x) (unsigned y));
-    and x y := wrap (Z.land (unsigned x) (unsigned y));
-    xor x y := wrap (Z.lxor (unsigned x) (unsigned y));
-    not x := wrap (Z.lnot (unsigned x));
-    ndn x y := wrap (Z.ldiff (unsigned x) (unsigned y));
+    or := Zmod.or;
+    and := Zmod.and;
+    xor := Zmod.xor;
+    not := Zmod.not;
+    ndn := Zmod.ndn;
 
-    mul x y := wrap (Z.mul (unsigned x) (unsigned y));
+    mul := Zmod.mul;
     mulhss x y := wrap (Z.mul (signed x) (signed y) / 2^width);
     mulhsu x y := wrap (Z.mul (signed x) (unsigned y) / 2^width);
     mulhuu x y := wrap (Z.mul (unsigned x) (unsigned y) / 2^width);
 
-    divu x y := wrap (if Z.eqb (unsigned y) 0 then sp.(div_by_zero) (unsigned x)
-                      else Z.div (unsigned x) (unsigned y));
-    divs x y := wrap (if Z.eqb (signed y) 0 then sp.(div_by_zero) (signed x)
-                      else Z.quot (signed x) (signed y));
-    modu x y := wrap (if Z.eqb (unsigned y) 0 then sp.(mod_by_zero) (unsigned x)
-                      else Z.modulo (unsigned x) (unsigned y));
-    mods x y := wrap (if Z.eqb (signed y) 0 then sp.(mod_by_zero) (signed x)
-                      else Z.rem (signed x) (signed y));
+    divu := Zmod.udiv;
+    divs := Zmod.squot;
+    modu := Zmod.umod;
+    mods := Zmod.srem;
 
-    slu x y := wrap (Z.shiftl (unsigned x) (adjust_shift_amount (unsigned y)));
-    sru x y := wrap (Z.shiftr (unsigned x) (adjust_shift_amount (unsigned y)));
-    srs x y := wrap (Z.shiftr (signed x) (adjust_shift_amount (unsigned y)));
+    slu x y := Zmod.slu x (adjust_shift_amount (unsigned y));
+    sru x y := Zmod.sru x (adjust_shift_amount (unsigned y));
+    srs x y := Zmod.srs x (adjust_shift_amount (unsigned y));
 
-    eqb x y := Z.eqb (unsigned x) (unsigned y);
+    eqb := Zmod.eqb;
     ltu x y := Z.ltb (unsigned x) (unsigned y);
     lts x y := Z.ltb (signed x) (signed y);
 
     sextend oldwidth z := wrap ((unsigned z + 2^(oldwidth-1)) mod 2^oldwidth - 2^(oldwidth-1));
   |}.
 
   Lemma eq_unsigned {x y : rep} : unsigned x = unsigned y -> x = y.
-  Proof.
-    cbv [value]; destruct x as [x px], y as [y py]; cbn.
-    intro; subst y.
-    apply f_equal, Eqdep_dec.UIP_dec. eapply Z.eq_dec.
-  Qed.
+  Proof. apply Zmod.unsigned_inj. Qed.
 
   Lemma of_Z_unsigned x : wrap (unsigned x) = x.
-  Proof. eapply eq_unsigned; destruct x; cbn; assumption.  Qed.
+  Proof. apply Zmod.of_Z_to_Z. Qed.
+
+  (* Candidate for stdlib inclusion: *)
+  Lemma smod_swrap z : ZModOffset.Z.smodulo z (2 ^ width) = @swrap width gen_word z.
+  Proof.
+    cbv [swrap gen_word].
+    cbv [ZModOffset.Z.smodulo ZModOffset.Z.omodulo].
+    rewrite Z.add_opp_r, Z.sub_opp_r.
+    case (Z.eqb_spec width 0) as [->|]; trivial.
+    case (Z.eqb_spec width 1) as [->|]; trivial.
+    case (Z.ltb_spec width 0) as []. { rewrite !Z.pow_neg_r by lia; trivial. }
+    rewrite Z.pow_sub_r by try lia; change (2^1) with 2.
+    rewrite Z.quot_div_nonneg by lia; trivial.
+  Qed.
 
   Lemma signed_of_Z z : signed (wrap z) = wrap_value (z + 2 ^ (width - 1)) - 2 ^ (width - 1).
   Proof.
+    cbv [signed wrap]; rewrite Zmod.signed_of_Z.
     cbv [unsigned signed wrap wrap_value swrap_value].
-    rewrite Zdiv.Zplus_mod_idemp_l; auto.
+    apply smod_swrap.
   Qed.
 
   Context (width_nonneg : Z.lt 0 width).
 
   Global Instance gen_ok : word.ok gen_word.
   Proof.
-    split; intros;
-      repeat match goal with
-             | a: @word.rep _ _ |- _ => destruct a
-             end;
-      cbn in *;
-      unfold adjust_shift_amount in *;
-      repeat match goal with
-             | |- context[if ?b then _ else _] => destr b
-             end;
-      eauto using of_Z_unsigned, signed_of_Z;
-      try (exfalso; blia).
-    apply eq_unsigned; assumption.
+    split; trivial;
+      cbv [gen_word adjust_shift_amount signed unsigned wrap]; intros.
+    { apply Zmod.unsigned_of_Z. }
+    { rewrite <-smod_swrap. apply Zmod.signed_of_Z. }
+    { apply Zmod.of_Z_to_Z. }
+    { apply Zmod.unsigned_add. }
+    { apply Zmod.unsigned_sub. }
+    { apply Zmod.unsigned_opp. }
+    { apply Zmod.unsigned_of_Z. }
+    { apply Zmod.unsigned_of_Z. }
+    { apply Zmod.unsigned_of_Z. }
+    { apply Zmod.unsigned_of_Z. }
+    { apply Zmod.unsigned_of_Z. }
+    { apply Zmod.unsigned_mul. }
+    { cbv [word.signed mulhss]. rewrite Zmod.signed_of_Z, smod_swrap; trivial. }
+    { cbv [word.signed mulhsu]. rewrite Zmod.signed_of_Z, smod_swrap; trivial. }
+    { cbv [word.unsigned mulhuu]. apply Zmod.unsigned_of_Z. }
+    { cbv [word.unsigned divu]. rewrite Zmod.unsigned_udiv; trivial. }
+    { cbv [word.signed divs]. rewrite Zmod.signed_squot, <-smod_swrap.
+      case Z.eqb_spec; [contradiction|]; trivial. }
+    { cbv [word.unsigned modu] in *. rewrite Zmod.unsigned_umod; trivial.
+      symmetry; apply Z.mod_small.
+      pose proof Zmod.unsigned_pos_bound x ltac:(lia).
+      pose proof Zmod.unsigned_pos_bound y ltac:(lia).
+      pose proof (Z.mod_pos_bound (Zmod.unsigned x) (Zmod.unsigned y)).
+      lia. }
+    { cbv [word.signed mods]. rewrite Zmod.signed_srem, <-smod_swrap; trivial. }
+    { cbv [word.unsigned slu] in *; case Z.ltb_spec; intros; [|lia].
+      apply Zmod.unsigned_slu. }
+    { cbv [word.unsigned sru] in *; case Z.ltb_spec; intros; [|lia].
+      pose proof Zmod.unsigned_pos_bound x ltac:(lia).
+      pose proof Zmod.unsigned_pos_bound y ltac:(lia).
+      rewrite Zmod.unsigned_sru, Z.mod_small;
+        rewrite ?Z.shiftr_div_pow2; try (Z.to_euclidean_division_equations; nia). }
+    { cbv [word.unsigned word.signed srs] in *; case Z.ltb_spec; intros; [|lia].
+      pose proof Zmod.signed_pos_bound x ltac:(lia).
+      pose proof Zmod.unsigned_pos_bound y ltac:(lia).
+      rewrite Zmod.signed_srs, <-smod_swrap, Z.smod_even_small;
+        rewrite ?Z.shiftr_div_pow2; try (Z.to_euclidean_division_equations; nia).
+      rewrite <-(Z.succ_pred width), Z.pow_succ_r, Z.mul_comm, Z.rem_mul; lia. }
   Qed.
 End WithWidth.
 Arguments gen_word : clear implicits.
 Arguments gen_ok : clear implicits.
 
 Definition default_special_case_handlers width := {|
-  div_by_zero x := -1;
-  mod_by_zero x := x;
   adjust_too_big_shift_amount n := n mod 2 ^ Z.log2 width;
 |}.