Permalink
Browse files

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
  • Loading branch information...
1 parent c02c866 commit 5c825f263698433ed4e8db8ccd0c14394520535a letouzey committed Aug 11, 2012
@@ -46,7 +46,8 @@ void init_arity () {
arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]=
arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]=
arity[HEAD0INT31]=arity[TAIL0INT31]=
- arity[COMPINT31]=arity[DECOMPINT31]=0;
+ arity[COMPINT31]=arity[DECOMPINT31]=
+ arity[ORINT31]=arity[ANDINT31]=arity[XORINT31]=0;
/* instruction with one operand */
arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
@@ -49,6 +49,7 @@ enum instructions {
HEAD0INT31, TAIL0INT31,
ISCONST, ARECONST,
COMPINT31, DECOMPINT31,
+ ORINT31, ANDINT31, XORINT31,
/* /spiwack */
STOP
};
@@ -1373,7 +1373,29 @@ value coq_interprete
Next;
}
+ Instruct (ORINT31) {
+ /* returns the bitwise or */
+ print_instr("ORINT31");
+ accu =
+ value_of_uint32((uint32_of_value(accu)) | (uint32_of_value(*sp++)));
+ Next;
+ }
+ Instruct (ANDINT31) {
+ /* returns the bitwise and */
+ print_instr("ANDINT31");
+ accu =
+ value_of_uint32((uint32_of_value(accu)) & (uint32_of_value(*sp++)));
+ Next;
+ }
+
+ Instruct (XORINT31) {
+ /* returns the bitwise xor */
+ print_instr("XORINT31");
+ accu =
+ value_of_uint32((uint32_of_value(accu)) ^ (uint32_of_value(*sp++)));
+ Next;
+ }
/* /spiwack */
View
@@ -114,6 +114,9 @@ type instruction =
| Kareconst of int*Label.t (* conditional jump *)
| Kcompint31 (* dynamic compilation of int31 *)
| Kdecompint31 (* dynamic decompilation of int31 *)
+ | Klorint31 (* bitwise operations: or and xor *)
+ | Klandint31
+ | Klxorint31
(* /spiwack *)
and bytecodes = instruction list
@@ -220,6 +223,9 @@ let rec instruction ppf = function
| Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
| Kcompint31 -> fprintf ppf "\tcompint31"
| Kdecompint31 -> fprintf ppf "\tdecompint"
+ | Klorint31 -> fprintf ppf "\tlorint31"
+ | Klandint31 -> fprintf ppf "\tlandint31"
+ | Klxorint31 -> fprintf ppf "\tlxorint31"
(* /spiwack *)
View
@@ -107,9 +107,10 @@ type instruction =
| Kisconst of Label.t (** conditional jump *)
| Kareconst of int*Label.t (** conditional jump *)
| Kcompint31 (** dynamic compilation of int31 *)
- | Kdecompint31 (** dynamix decompilation of int31
- /spiwack *)
-
+ | Kdecompint31 (** dynamix decompilation of int31 *)
+ | Klorint31 (** bitwise operations: or and xor *)
+ | Klandint31
+ | Klxorint31
and bytecodes = instruction list
View
@@ -258,6 +258,9 @@ let emit_instr = function
| Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl
| Kcompint31 -> out opCOMPINT31
| Kdecompint31 -> out opDECOMPINT31
+ | Klorint31 -> out opORINT31
+ | Klandint31 -> out opANDINT31
+ | Klxorint31 -> out opXORINT31
(*/spiwack *)
| Kstop ->
out opSTOP
View
@@ -521,6 +521,9 @@ fun env field value ->
| KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31
| KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31
| KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31
+ | KInt31 (_, Int31Lor) -> add_int31_binop_from_const Cbytecodes.Klorint31
+ | KInt31 (_, Int31Land) -> add_int31_binop_from_const Cbytecodes.Klandint31
+ | KInt31 (_, Int31Lxor) -> add_int31_binop_from_const Cbytecodes.Klxorint31
| _ -> env.retroknowledge
in
Retroknowledge.add_field retroknowledge_with_reactive_info field value
View
@@ -65,6 +65,9 @@ type int31_field =
| Int31Compare
| Int31Head0
| Int31Tail0
+ | Int31Lor
+ | Int31Land
+ | Int31Lxor
type field =
(* | KEq
@@ -52,6 +52,9 @@ type int31_field =
| Int31Compare
| Int31Head0
| Int31Tail0
+ | Int31Lor
+ | Int31Land
+ | Int31Lxor
type field =
View
@@ -383,7 +383,9 @@ PRINTED BY pr_r_int31_field
| [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ]
| [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ]
| [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ]
-
+| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ]
+| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ]
+| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ]
END
ARGUMENT EXTEND retroknowledge_field
@@ -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.
@@ -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.
@@ -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.
@@ -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
Oops, something went wrong.

0 comments on commit 5c825f2

Please sign in to comment.