diff options
| -rw-r--r-- | src/Reflection/Z/InterpretationsGen.v | 8 | ||||
| -rw-r--r-- | src/Util/FixedWordSizesEquality.v | 55 | ||||
| -rw-r--r-- | src/Util/WordUtil.v | 44 | ||||
| -rw-r--r-- | src/Util/ZUtil.v | 50 |
4 files changed, 111 insertions, 46 deletions
diff --git a/src/Reflection/Z/InterpretationsGen.v b/src/Reflection/Z/InterpretationsGen.v index 6ccb23960..f11837e60 100644 --- a/src/Reflection/Z/InterpretationsGen.v +++ b/src/Reflection/Z/InterpretationsGen.v @@ -233,9 +233,9 @@ Module InterpretationsGen (Bit : BitSize). Lemma wordWToZ_shl : bounds_2statement shl Z.shiftl. Proof. wWToZ_t; wWToZ_extra_t; unfold wordWToZ, wordBin. - rewrite wordToN_NToWord_idempotent; [rewrite <- Z_inj_shiftl; reflexivity|]. + rewrite wordToN_NToWord_idempotent; [rewrite <- N2Z.inj_shiftl; reflexivity|]. apply N2Z.inj_lt. - rewrite Z_inj_shiftl. + rewrite N2Z.inj_shiftl. destruct (Z.lt_ge_cases 0 ((wordWToZ x) << (wordWToZ y)))%Z; [|eapply Z.le_lt_trans; [|apply N2Z.inj_lt, Npow2_gt0]; assumption]. rewrite Npow2_N, N2Z.inj_pow, ?nat_N_Z. @@ -245,9 +245,9 @@ Module InterpretationsGen (Bit : BitSize). Lemma wordWToZ_shr : bounds_2statement shr Z.shiftr. Proof. wWToZ_t; wWToZ_extra_t; unfold wordWToZ, wordBin. - rewrite wordToN_NToWord_idempotent; [rewrite <- Z_inj_shiftr; reflexivity|]. + rewrite wordToN_NToWord_idempotent; [rewrite <- N2Z.inj_shiftr; reflexivity|]. apply N2Z.inj_lt. - rewrite Z_inj_shiftr. + rewrite N2Z.inj_shiftr. destruct (Z.lt_ge_cases 0 ((wordWToZ x) >> (wordWToZ y)))%Z; [|eapply Z.le_lt_trans; [|apply N2Z.inj_lt, Npow2_gt0]; assumption]. rewrite Npow2_N, N2Z.inj_pow, nat_N_Z. diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 749750625..271668032 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -4,6 +4,7 @@ Require Import Coq.Arith.Arith. Require Import Bedrock.Word. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Util.WordUtil. +Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics.BreakMatch. Definition wordT_beq_hetero {logsz1 logsz2} : wordT logsz1 -> wordT logsz2 -> bool @@ -225,7 +226,7 @@ Ltac syntactic_fixed_size_op_to_word := let P := lazymatch (eval pattern logsz in P) with ?P _ => P end in revert logsz x; refine (@wordToZ_word_case_dep_unop wop P _); - intros logsz x; unfold wordToZ_gen; intros + intros logsz x; intros | [ |- context[wordToZ (word_case_dep (T:=?T) ?logsz (?wop 32) (?wop 64) (?wop 128) ?f ?x ?y)] ] => lazymatch type of x with | context[logsz] @@ -236,7 +237,7 @@ Ltac syntactic_fixed_size_op_to_word := let P := lazymatch (eval pattern logsz in P) with ?P _ => P end in revert logsz x y; refine (@wordToZ_word_case_dep_binop wop P _); - intros logsz x y; unfold wordToZ_gen; intros + intros logsz x y; intros | _ => move y at top; revert dependent logsz; intros logsz y; @@ -245,7 +246,7 @@ Ltac syntactic_fixed_size_op_to_word := let P := lazymatch (eval pattern logsz in P) with ?P _ => P end in revert logsz y; refine (@wordToZ_word_case_dep_11op _ wop P x _); - intros logsz y; unfold wordToZ_gen; intros + intros logsz y; intros end | [ |- context[wordToZ (word_case_dep (T:=?T) ?logsz (?wop 32) (?wop 64) (?wop 128) ?f ?x ?y ?z ?w)] ] => move w at top; move z at top; move y at top; move x at top; @@ -299,7 +300,7 @@ Section Updates. g. Proof. intros H n; specialize (H (2^n)%nat). - unfold valid_update; intros; fixed_size_op_to_word; auto. + unfold valid_update; intros; fixed_size_op_to_word; unfold wordToZ_gen; auto. Qed. Lemma wadd_valid_update: forall n, @@ -351,3 +352,49 @@ Section Updates. (fun l0 u0 l1 u1 => Z.shiftl u0 u1)%Z. Proof. apply word_case_dep_valid_update, shl_valid_update. Qed. End Updates. + +Section pull_ZToWord. + Local Ltac t0 := + intros; + etransitivity; [ symmetry; apply ZToWord_wordToZ | ]; fixed_size_op_to_word; unfold wordToZ_gen, wordBin; + apply f_equal. + Local Ltac t1 lem := + let solver := solve [ apply Npow2_Zlog2; autorewrite with push_Zof_N; assumption + | apply N2Z.inj_ge; unfold wordToZ_gen in *; omega ] in + first [ rewrite <- lem by solver | rewrite -> lem by solver ]. + Local Ltac t2 := + autorewrite with push_Zof_N; unfold wordToZ_gen in *; + try first [ reflexivity + | apply Z.max_case_strong; omega ]. + + Local Ltac t lem := + t0; t1 lem; solve [ t2 ]. + + Local Notation pull_ZToWordT_2op wop zop + := (forall {logsz} (x y : wordT logsz), + (Z.log2 (zop (wordToZ x) (wordToZ y)) < Z.of_nat (2^logsz))%Z + -> wop logsz x y = ZToWord (zop (wordToZ x) (wordToZ y))) + (only parsing). + Local Notation pull_ZToWordT_2op' wop zop + := (forall {logsz} (x y : wordT logsz), + (0 <= zop (wordToZ x) (wordToZ y))%Z + -> wop logsz x y = ZToWord (zop (wordToZ x) (wordToZ y))) + (only parsing). + + Lemma wadd_def_ZToWord : pull_ZToWordT_2op (@wadd) (@Z.add). + Proof. t (@wordize_plus). Qed. + Lemma wsub_def_ZToWord : pull_ZToWordT_2op' (@wsub) (@Z.sub). + Proof. t (@wordize_minus). Qed. + Lemma wmul_def_ZToWord : pull_ZToWordT_2op (@wmul) (@Z.mul). + Proof. t (@wordize_mult). Qed. + Lemma wland_def_ZToWord : pull_ZToWordT_2op (@wland) (@Z.land). + Proof. t (@wordize_and). Qed. + Lemma wlor_def_ZToWord : pull_ZToWordT_2op (@wlor) (@Z.lor). + Proof. t (@wordize_or). Qed. + Lemma wshl_def_ZToWord : pull_ZToWordT_2op (@wshl) (@Z.shiftl). + Proof. t (@wordToN_NToWord_idempotent). Qed. + Lemma wshr_def_ZToWord : pull_ZToWordT_2op (@wshr) (@Z.shiftr). + Proof. t (@wordToN_NToWord_idempotent). Qed. +End pull_ZToWord. +Hint Rewrite wadd_def_ZToWord wsub_def_ZToWord wmul_def_ZToWord wland_def_ZToWord wlor_def_ZToWord wshl_def_ZToWord wshr_def_ZToWord : pull_ZToWord. +Hint Rewrite <- wadd_def_ZToWord wsub_def_ZToWord wmul_def_ZToWord wland_def_ZToWord wlor_def_ZToWord wshl_def_ZToWord wshr_def_ZToWord : push_ZToWord. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index fd4863ce1..1a38c873f 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -22,9 +22,13 @@ Local Open Scope nat_scope. Create HintDb pull_wordToN discriminated. Create HintDb push_wordToN discriminated. +Create HintDb pull_ZToWord discriminated. +Create HintDb push_ZToWord discriminated. Hint Extern 1 => autorewrite with pull_wordToN in * : pull_wordToN. Hint Extern 1 => autorewrite with push_wordToN in * : push_wordToN. +Hint Extern 1 => autorewrite with pull_ZToWord in * : pull_ZToWord. +Hint Extern 1 => autorewrite with push_ZToWord in * : push_ZToWord. Module Word. Fixpoint weqb_hetero sz1 sz2 (x : word sz1) (y : word sz2) : bool := @@ -256,42 +260,6 @@ Section Pow2. Qed. End Pow2. -Section Z2N. - Lemma Z_inj_shiftl: forall x y, Z.of_N (N.shiftl x y) = Z.shiftl (Z.of_N x) (Z.of_N y). - Proof. - intros. - apply Z.bits_inj_iff'; intros k Hpos. - rewrite Z2N.inj_testbit; [|assumption]. - rewrite Z.shiftl_spec; [|assumption]. - - assert ((Z.to_N k) >= y \/ (Z.to_N k) < y)%N as g by ( - unfold N.ge, N.lt; induction (N.compare (Z.to_N k) y); [left|auto|left]; - intro H; inversion H). - - destruct g as [g|g]; - [ rewrite N.shiftl_spec_high; [|apply N2Z.inj_le; rewrite Z2N.id|apply N.ge_le] - | rewrite N.shiftl_spec_low]; try assumption. - - - rewrite <- N2Z.inj_testbit; f_equal. - rewrite N2Z.inj_sub, Z2N.id; [reflexivity|assumption|apply N.ge_le; assumption]. - - - apply N2Z.inj_lt in g. - rewrite Z2N.id in g; [symmetry|assumption]. - apply Z.testbit_neg_r; omega. - Qed. - - Lemma Z_inj_shiftr: forall x y, Z.of_N (N.shiftr x y) = Z.shiftr (Z.of_N x) (Z.of_N y). - Proof. - intros. - apply Z.bits_inj_iff'; intros k Hpos. - rewrite Z2N.inj_testbit; [|assumption]. - rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption. - rewrite <- N2Z.inj_testbit; f_equal. - rewrite N2Z.inj_add; f_equal. - apply Z2N.id; assumption. - Qed. -End Z2N. - Section WordToN. Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N -> wordToN (NToWord sz n) = n. @@ -1231,7 +1199,7 @@ Section Updates. do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1; intros. repeat split; [assumption| | |assumption]; - (rewrite wordToN_NToWord_idempotent; [|apply Npow2_Zlog2]; rewrite Z_inj_shiftr); + (rewrite wordToN_NToWord_idempotent; [|apply Npow2_Zlog2]; rewrite N2Z.inj_shiftr); [ | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption] | | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]]; apply Z.shiftr_le_mono; shift_mono. @@ -1247,7 +1215,7 @@ Section Updates. do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1; intros. repeat split; [assumption| | |assumption]; - (rewrite wordToN_NToWord_idempotent; [|apply Npow2_Zlog2]; rewrite Z_inj_shiftl); + (rewrite wordToN_NToWord_idempotent; [|apply Npow2_Zlog2]; rewrite N2Z.inj_shiftl); [ | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption] | | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]]; apply Z.shiftl_le_mono; shift_mono. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 277b38121..bc9278960 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -3097,6 +3097,56 @@ for name in names: End RemoveEquivModuloInstances. End Z. +Module N2Z. + Lemma inj_land n m : Z.of_N (N.land n m) = Z.land (Z.of_N n) (Z.of_N m). + Proof. destruct n, m; reflexivity. Qed. + Hint Rewrite inj_land : push_Zof_N. + Hint Rewrite <- inj_land : pull_Zof_N. + + Lemma inj_lor n m : Z.of_N (N.lor n m) = Z.lor (Z.of_N n) (Z.of_N m). + Proof. destruct n, m; reflexivity. Qed. + Hint Rewrite inj_lor : push_Zof_N. + Hint Rewrite <- inj_lor : pull_Zof_N. + + Lemma inj_shiftl: forall x y, Z.of_N (N.shiftl x y) = Z.shiftl (Z.of_N x) (Z.of_N y). + Proof. + intros. + apply Z.bits_inj_iff'; intros k Hpos. + rewrite Z2N.inj_testbit; [|assumption]. + rewrite Z.shiftl_spec; [|assumption]. + + assert ((Z.to_N k) >= y \/ (Z.to_N k) < y)%N as g by ( + unfold N.ge, N.lt; induction (N.compare (Z.to_N k) y); [left|auto|left]; + intro H; inversion H). + + destruct g as [g|g]; + [ rewrite N.shiftl_spec_high; [|apply N2Z.inj_le; rewrite Z2N.id|apply N.ge_le] + | rewrite N.shiftl_spec_low]; try assumption. + + - rewrite <- N2Z.inj_testbit; f_equal. + rewrite N2Z.inj_sub, Z2N.id; [reflexivity|assumption|apply N.ge_le; assumption]. + + - apply N2Z.inj_lt in g. + rewrite Z2N.id in g; [symmetry|assumption]. + apply Z.testbit_neg_r; omega. + Qed. + Hint Rewrite inj_shiftl : push_Zof_N. + Hint Rewrite <- inj_shiftl : pull_Zof_N. + + Lemma inj_shiftr: forall x y, Z.of_N (N.shiftr x y) = Z.shiftr (Z.of_N x) (Z.of_N y). + Proof. + intros. + apply Z.bits_inj_iff'; intros k Hpos. + rewrite Z2N.inj_testbit; [|assumption]. + rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption. + rewrite <- N2Z.inj_testbit; f_equal. + rewrite N2Z.inj_add; f_equal. + apply Z2N.id; assumption. + Qed. + Hint Rewrite inj_shiftr : push_Zof_N. + Hint Rewrite <- inj_shiftr : pull_Zof_N. +End N2Z. + Module Export BoundsTactics. Ltac prime_bound := Z.prime_bound. Ltac zero_bounds := Z.zero_bounds. |