fast bitwise operations (lor,land,lxor) on int31 and BigN

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 292 insertions, 32 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 9a8a7691c..39e086c31 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -88,7 +88,11 @@ Module ZnZ.
     is_even     : t -> bool;
     (* square root *)
     sqrt2       : t -> t -> t * carry t;
-    sqrt        : t -> t  }.
+    sqrt        : t -> t;
+    (* bitwise operations *)
+    lor         : t -> t -> t;
+    land        : t -> t -> t;
+    lxor        : t -> t -> t }.
 
  Section Specs.
  Context {t : Type}{ops : Ops t}.
@@ -199,7 +203,10 @@ Module ZnZ.
           [||WW x y||] = [|s|] ^ 2 + [+|r|] /\
           [+|r|] <= 2 * [|s|];
     spec_sqrt : forall x,
-       [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2
+       [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2;
+    spec_lor : forall x y, [|lor x y|] = Z.lor [|x|] [|y|];
+    spec_land : forall x y, [|land x y|] = Z.land [|x|] [|y|];
+    spec_lxor : forall x y, [|lxor x y|] = Z.lxor [|x|] [|y|]
   }.
 
  End Specs.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 35fe948ea..94d3e97a5 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -283,6 +283,27 @@ Section Z_2nZ.
   Eval lazy beta delta [ww_gcd] in
   ww_gcd compare w_0 w_eq0 w_gcd_gt _ww_digits gcd_gt_fix gcd_cont.
 
+ Definition lor (x y : zn2z t) :=
+  match x, y with
+  | W0, _ => y
+  | _, W0 => x
+  | WW hx lx, WW hy ly => WW (ZnZ.lor hx hy) (ZnZ.lor lx ly)
+  end.
+
+ Definition land (x y : zn2z t) :=
+  match x, y with
+  | W0, _ => W0
+  | _, W0 => W0
+  | WW hx lx, WW hy ly => WW (ZnZ.land hx hy) (ZnZ.land lx ly)
+  end.
+
+ Definition lxor (x y : zn2z t) :=
+  match x, y with
+  | W0, _ => y
+  | _, W0 => x
+  | WW hx lx, WW hy ly => WW (ZnZ.lxor hx hy) (ZnZ.lxor lx ly)
+  end.
+
  (* ** Record of operators on 2 words *)
 
  Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) | 1 :=
@@ -303,7 +324,10 @@ Section Z_2nZ.
     pos_mod
     is_even
     sqrt2
-    sqrt.
+    sqrt
+    lor
+    land
+    lxor.
 
  Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) | 2 :=
    ZnZ.MkOps _ww_digits _ww_zdigits
@@ -323,7 +347,10 @@ Section Z_2nZ.
     pos_mod
     is_even
     sqrt2
-    sqrt.
+    sqrt
+    lor
+    land
+    lxor.
 
  (* Proof *)
  Context {specs : ZnZ.Specs ops}.
@@ -787,6 +814,81 @@ refine
  exact ZnZ.spec_sqrt2.
  Qed.
 
+ Let wB_pos : 0 < wB.
+ Proof.
+ unfold wB, base; apply Z.pow_pos_nonneg; auto with zarith.
+ Qed.
+
+ Let ww_testbit_high n x y : Z.pos w_digits <= n ->
+  Z.testbit [|WW x y|] n =
+  Z.testbit (ZnZ.to_Z x) (n - Z.pos w_digits).
+ Proof.
+  intros Hn.
+  assert (E : ZnZ.to_Z x = [|WW x y|] / wB).
+  { simpl.
+    rewrite Z.div_add_l; auto with zarith.
+    now rewrite Z.div_small, Z.add_0_r. }
+  rewrite E.
+  unfold wB, base. rewrite Z.div_pow2_bits.
+  - f_equal; auto with zarith.
+  - easy.
+  - auto with zarith.
+ Qed.
+
+ Let ww_testbit_low n x y : 0 <= n < Z.pos w_digits ->
+  Z.testbit [|WW x y|] n = Z.testbit (ZnZ.to_Z y) n.
+ Proof.
+  intros (Hn,Hn').
+  assert (E : ZnZ.to_Z y = [|WW x y|] mod wB).
+  { simpl; symmetry.
+    rewrite Z.add_comm, Z.mod_add; auto with zarith.
+    apply Z.mod_small; auto with zarith. }
+  rewrite E.
+  unfold wB, base. symmetry. apply Z.mod_pow2_bits_low; auto.
+ Qed.
+
+ Let spec_lor x y : [|lor x y|] = Z.lor [|x|] [|y|].
+ Proof.
+  destruct x as [ |hx lx]. trivial.
+  destruct y as [ |hy ly]. now rewrite Z.lor_comm.
+  change ([|WW (ZnZ.lor hx hy) (ZnZ.lor lx ly)|] =
+          Z.lor [|WW hx lx|] [|WW hy ly|]).
+  apply Z.bits_inj'; intros n Hn.
+  rewrite Z.lor_spec.
+  destruct (Z.le_gt_cases (Z.pos w_digits) n) as [LE|GT].
+  - now rewrite !ww_testbit_high, ZnZ.spec_lor, Z.lor_spec.
+  - rewrite !ww_testbit_low; auto.
+    now rewrite ZnZ.spec_lor, Z.lor_spec.
+ Qed.
+
+ Let spec_land x y : [|land x y|] = Z.land [|x|] [|y|].
+ Proof.
+  destruct x as [ |hx lx]. trivial.
+  destruct y as [ |hy ly]. now rewrite Z.land_comm.
+  change ([|WW (ZnZ.land hx hy) (ZnZ.land lx ly)|] =
+          Z.land [|WW hx lx|] [|WW hy ly|]).
+  apply Z.bits_inj'; intros n Hn.
+  rewrite Z.land_spec.
+  destruct (Z.le_gt_cases (Z.pos w_digits) n) as [LE|GT].
+  - now rewrite !ww_testbit_high, ZnZ.spec_land, Z.land_spec.
+  - rewrite !ww_testbit_low; auto.
+    now rewrite ZnZ.spec_land, Z.land_spec.
+ Qed.
+
+ Let spec_lxor x y : [|lxor x y|] = Z.lxor [|x|] [|y|].
+ Proof.
+  destruct x as [ |hx lx]. trivial.
+  destruct y as [ |hy ly]. now rewrite Z.lxor_comm.
+  change ([|WW (ZnZ.lxor hx hy) (ZnZ.lxor lx ly)|] =
+          Z.lxor [|WW hx lx|] [|WW hy ly|]).
+  apply Z.bits_inj'; intros n Hn.
+  rewrite Z.lxor_spec.
+  destruct (Z.le_gt_cases (Z.pos w_digits) n) as [LE|GT].
+  - now rewrite !ww_testbit_high, ZnZ.spec_lxor, Z.lxor_spec.
+  - rewrite !ww_testbit_low; auto.
+    now rewrite ZnZ.spec_lxor, Z.lxor_spec.
+ Qed.
+
  Global Instance mk_zn2z_specs : ZnZ.Specs mk_zn2z_ops.
  Proof.
   apply ZnZ.MkSpecs; auto.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 385217d05..0284af7aa 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1158,7 +1158,10 @@ Instance int31_ops : ZnZ.Ops int31 :=
   fun i => let (_,r) := i/2 in
   match r ?= 0 with Eq => true | _ => false end;
  sqrt2       := sqrt312;
- sqrt        := sqrt31
+ sqrt        := sqrt31;
+ lor         := lor31;
+ land        := land31;
+ lxor        := lxor31
 }.
 
 Section Int31_Specs.
@@ -2403,6 +2406,51 @@ Qed.
  apply Zmod_unique with [|q|]; auto with zarith.
  Qed.
 
+ (* Bitwise *)
+
+ Lemma log2_phi_bounded x : Z.log2 [|x|] < Z.of_nat size.
+ Proof.
+  destruct (phi_bounded x) as (H,H').
+  Z.le_elim H.
+  - now apply Z.log2_lt_pow2.
+  - now rewrite <- H.
+ Qed.
+
+ Lemma spec_lor x y : [| ZnZ.lor x y |] = Z.lor [|x|] [|y|].
+ Proof.
+ unfold ZnZ.lor; simpl. unfold lor31.
+ rewrite phi_phi_inv.
+ apply Z.mod_small; split; trivial.
+ - apply Z.lor_nonneg; split; apply phi_bounded.
+ - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy.
+   rewrite Z.log2_lor; try apply phi_bounded.
+   apply Z.max_lub_lt; apply log2_phi_bounded.
+ Qed.
+
+ Lemma spec_land x y : [| ZnZ.land x y |] = Z.land [|x|] [|y|].
+ Proof.
+ unfold ZnZ.land; simpl. unfold land31.
+ rewrite phi_phi_inv.
+ apply Z.mod_small; split; trivial.
+ - apply Z.land_nonneg; left; apply phi_bounded.
+ - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy.
+   eapply Z.le_lt_trans.
+   apply Z.log2_land; try apply phi_bounded.
+   apply Z.min_lt_iff; left; apply log2_phi_bounded.
+ Qed.
+
+ Lemma spec_lxor x y : [| ZnZ.lxor x y |] = Z.lxor [|x|] [|y|].
+ Proof.
+ unfold ZnZ.lxor; simpl. unfold lxor31.
+ rewrite phi_phi_inv.
+ apply Z.mod_small; split; trivial.
+ - apply Z.lxor_nonneg; split; intros; apply phi_bounded.
+ - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy.
+   eapply Z.le_lt_trans.
+   apply Z.log2_lxor; try apply phi_bounded.
+   apply Z.max_lub_lt; apply log2_phi_bounded.
+ Qed.
+
  Global Instance int31_specs : ZnZ.Specs int31_ops := {
     spec_to_Z   := phi_bounded;
     spec_of_pos := positive_to_int31_spec;
@@ -2446,7 +2494,10 @@ Qed.
     spec_pos_mod := spec_pos_mod;
     spec_is_even := spec_is_even;
     spec_sqrt2 := spec_sqrt2;
-    spec_sqrt := spec_sqrt }.
+    spec_sqrt := spec_sqrt;
+    spec_lor := spec_lor;
+    spec_land := spec_land;
+    spec_lxor := spec_lxor }.
 
 End Int31_Specs.
 
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index f414663a8..885cd0daf 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -335,6 +335,11 @@ Definition addmuldiv31 p i j :=
  in
  res.
 
+(** Bitwise operations *)
+
+Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)).
+Definition land31 n m := phi_inv (Z.land (phi n) (phi m)).
+Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)).
 
 Register add31 as int31 plus in "coq_int31" by True.
 Register add31c as int31 plusc in "coq_int31" by True.
@@ -348,6 +353,12 @@ Register div3121 as int31 div21 in "coq_int31" by True.
 Register div31 as int31 div in "coq_int31" by True.
 Register compare31 as int31 compare in "coq_int31" by True.
 Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True.
+Register lor31 as int31 lor in "coq_int31" by True.
+Register land31 as int31 land in "coq_int31" by True.
+Register lxor31 as int31 lxor in "coq_int31" by True.
+
+Definition lnot31 n := lxor31 Tn n.
+Definition ldiff31 n m := land31 n (lnot31 m).
 
 Fixpoint euler (guard:nat) (i j:int31) {struct guard} :=
   match guard with
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 9e3f4ef44..334836954 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -796,6 +796,40 @@ Section ZModulo.
  exists 0; simpl; auto with zarith.
  Qed.
 
+ Definition lor := Z.lor.
+ Definition land := Z.land.
+ Definition lxor := Z.lxor.
+
+ Lemma spec_lor x y : [|lor x y|] = Z.lor [|x|] [|y|].
+ Proof.
+ unfold lor, to_Z.
+ apply Z.bits_inj'; intros n Hn. rewrite Z.lor_spec.
+ unfold wB, base.
+ destruct (Z.le_gt_cases (Z.pos digits) n).
+ - rewrite !Z.mod_pow2_bits_high; auto with zarith.
+ - rewrite !Z.mod_pow2_bits_low, Z.lor_spec; auto with zarith.
+ Qed.
+
+ Lemma spec_land x y : [|land x y|] = Z.land [|x|] [|y|].
+ Proof.
+ unfold land, to_Z.
+ apply Z.bits_inj'; intros n Hn. rewrite Z.land_spec.
+ unfold wB, base.
+ destruct (Z.le_gt_cases (Z.pos digits) n).
+ - rewrite !Z.mod_pow2_bits_high; auto with zarith.
+ - rewrite !Z.mod_pow2_bits_low, Z.land_spec; auto with zarith.
+ Qed.
+
+ Lemma spec_lxor x y : [|lxor x y|] = Z.lxor [|x|] [|y|].
+ Proof.
+ unfold lxor, to_Z.
+ apply Z.bits_inj'; intros n Hn. rewrite Z.lxor_spec.
+ unfold wB, base.
+ destruct (Z.le_gt_cases (Z.pos digits) n).
+ - rewrite !Z.mod_pow2_bits_high; auto with zarith.
+ - rewrite !Z.mod_pow2_bits_low, Z.lxor_spec; auto with zarith.
+ Qed.
+
  (** Let's now group everything in two records *)
 
  Instance zmod_ops : ZnZ.Ops Z := ZnZ.MkOps
@@ -849,7 +883,10 @@ Section ZModulo.
 
     (is_even     : t -> bool)
     (sqrt2       : t -> t -> t * carry t)
-    (sqrt        : t -> t).
+    (sqrt        : t -> t)
+    (lor         : t -> t -> t)
+    (land         : t -> t -> t)
+    (lxor         : t -> t -> t).
 
  Instance zmod_specs : ZnZ.Specs zmod_ops := ZnZ.MkSpecs
     spec_to_Z
@@ -906,7 +943,10 @@ Section ZModulo.
 
     spec_is_even
     spec_sqrt2
-    spec_sqrt.
+    spec_sqrt
+    spec_lor
+    spec_land
+    spec_lxor.
 
 End ZModulo.
 
@@ -922,4 +962,3 @@ Module ZModuloCyclicType (P:PositiveNotOne) <: CyclicType.
  Instance ops : ZnZ.Ops t := zmod_ops P.p.
  Instance specs : ZnZ.Specs ops := zmod_specs P.not_one.
 End ZModuloCyclicType.
-
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 5012a1b93..3cfa55bef 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -1617,40 +1617,90 @@ Module Make (W0:CyclicType) <: NType.
   rewrite spec_shiftr, spec_1. apply Z.div2_spec.
  Qed.
 
- (** TODO : provide efficient versions instead of just converting
-   from/to N (see with Laurent) *)
+ Local Notation lorn := (fun n =>
+  let op := dom_op n in
+  let lor := ZnZ.lor in
+  fun x y => reduce n (lor x y)).
+
+ Definition lor : t -> t -> t := Eval red_t in same_level lorn.
 
- Definition lor x y := of_N (N.lor (to_N x) (to_N y)).
- Definition land x y := of_N (N.land (to_N x) (to_N y)).
- Definition ldiff x y := of_N (N.ldiff (to_N x) (to_N y)).
- Definition lxor x y := of_N (N.lxor (to_N x) (to_N y)).
+ Lemma lor_fold : lor = same_level lorn.
+ Proof. red_t; reflexivity. Qed.
 
- Lemma spec_land: forall x y, [land x y] = Z.land [x] [y].
+ Theorem spec_lor x y : [lor x y] = Z.lor [x] [y].
  Proof.
-  intros x y. unfold land. rewrite spec_of_N. unfold to_N.
-  generalize (spec_pos x), (spec_pos y).
-  destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+  rewrite lor_fold. apply spec_same_level; clear x y.
+  intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_lor.
  Qed.
 
- Lemma spec_lor: forall x y, [lor x y] = Z.lor [x] [y].
+ Local Notation landn := (fun n =>
+  let op := dom_op n in
+  let land := ZnZ.land in
+  fun x y => reduce n (land x y)).
+
+ Definition land : t -> t -> t := Eval red_t in same_level landn.
+
+ Lemma land_fold : land = same_level landn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_land x y : [land x y] = Z.land [x] [y].
  Proof.
-  intros x y. unfold lor. rewrite spec_of_N. unfold to_N.
-  generalize (spec_pos x), (spec_pos y).
-  destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+  rewrite land_fold. apply spec_same_level; clear x y.
+  intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_land.
  Qed.
 
- Lemma spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y].
+ Local Notation lxorn := (fun n =>
+  let op := dom_op n in
+  let lxor := ZnZ.lxor in
+  fun x y => reduce n (lxor x y)).
+
+ Definition lxor : t -> t -> t := Eval red_t in same_level lxorn.
+
+ Lemma lxor_fold : lxor = same_level lxorn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_lxor x y : [lxor x y] = Z.lxor [x] [y].
  Proof.
-  intros x y. unfold ldiff. rewrite spec_of_N. unfold to_N.
-  generalize (spec_pos x), (spec_pos y).
-  destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+  rewrite lxor_fold. apply spec_same_level; clear x y.
+  intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_lxor.
  Qed.
 
- Lemma spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y].
- Proof.
-  intros x y. unfold lxor. rewrite spec_of_N. unfold to_N.
-  generalize (spec_pos x), (spec_pos y).
-  destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+ Local Notation ldiffn := (fun n =>
+  let op := dom_op n in
+  let lxor := ZnZ.lxor in
+  let land := ZnZ.land in
+  let m1 := ZnZ.minus_one in
+  fun x y => reduce n (land x (lxor y m1))).
+
+ Definition ldiff : t -> t -> t := Eval red_t in same_level ldiffn.
+
+ Lemma ldiff_fold : ldiff = same_level ldiffn.
+ Proof. red_t; reflexivity. Qed.
+
+ Lemma ldiff_alt x y p :
+  0 <= x < 2^p -> 0 <= y < 2^p ->
+  Z.ldiff x y = Z.land x (Z.lxor y (2^p - 1)).
+ Proof.
+  intros (Hx,Hx') (Hy,Hy').
+  destruct p as [|p|p].
+  - simpl in *; replace x with 0; replace y with 0; auto with zarith.
+  - rewrite <- Z.shiftl_1_l. change (_ - 1) with (Z.ones (Z.pos p)).
+    rewrite <- Z.ldiff_ones_l_low; trivial.
+    rewrite !Z.ldiff_land, Z.land_assoc. f_equal.
+    rewrite Z.land_ones; try easy.
+    symmetry. apply Z.mod_small; now split.
+    Z.le_elim Hy.
+    + now apply Z.log2_lt_pow2.
+    + now subst.
+  - simpl in *; omega.
+ Qed.
+
+ Theorem spec_ldiff x y : [ldiff x y] = Z.ldiff [x] [y].
+ Proof.
+  rewrite ldiff_fold. apply spec_same_level; clear x y.
+  intros n x y. simpl. rewrite spec_reduce.
+  rewrite ZnZ.spec_land, ZnZ.spec_lxor, ZnZ.spec_m1.
+  symmetry. apply ldiff_alt; apply ZnZ.spec_to_Z.
  Qed.
 
 End Make.