diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-07-06 17:46:05 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-07-06 17:46:05 -0400 |
commit | 6e55d0f4ce8be20438c42aaac8852a0aa310b295 (patch) | |
tree | d584274857670183d4c43541a1c8c365ed9f5aea | |
parent | 65e6c7c113aa4a896092161a911aef7eba407127 (diff) |
prove an admit in ArithmeticSynthesisTest
-rw-r--r-- | src/Specific/ArithmeticSynthesisTest.v | 76 | ||||
-rw-r--r-- | src/Specific/Karatsuba.v | 95 | ||||
-rw-r--r-- | src/Util/QUtil.v | 118 |
3 files changed, 145 insertions, 144 deletions
diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v index a2e1442a4..71100cdcf 100644 --- a/src/Specific/ArithmeticSynthesisTest.v +++ b/src/Specific/ArithmeticSynthesisTest.v @@ -6,6 +6,7 @@ Require Import Crypto.Arithmetic.Saturated.Freeze. Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable. Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics. Require Crypto.Util.Tuple. +Require Import Crypto.Util.QUtil. Local Notation tuple := Tuple.tuple. Local Open Scope list_scope. Local Open Scope Z_scope. @@ -24,16 +25,18 @@ Section Ops51. Definition bitwidth := 64. Definition s : Z := 2^255. Definition c : list B.limb := [(1, 19)]. - Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *) Definition carry_chain1 := Eval vm_compute in (seq 0 (pred sz)). - Definition carry_chain2 := ([0;1])%nat. - Definition a24 := 121665%Z. + Definition carry_chain2 := [0;1]%nat. + Definition a24 := 121665%Z. + Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *) (* These definitions are inferred from those above *) Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *) - Definition wt := fun i : nat => - let si := Z.log2 s * i in - 2 ^ ((si/sz) + (if dec ((si/sz)*sz=si) then 0 else 1)). + Section wt. + Import QArith Qround. + Local Coercion QArith_base.inject_Z : Z >-> Q. + Definition wt (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i). + End wt. Definition sz2 := Eval vm_compute in ((sz * 2) - 1)%nat. Definition m_enc := Eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c)). @@ -45,44 +48,15 @@ Section Ops51. | S n => addm (Positional.add_cps wt acc m_enc id) n end) (Positional.zeros sz) coef_div_modulus). Definition coef_mod : mod_eq m (Positional.eval (n:=sz) wt coef) 0 := eq_refl. - Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed. Lemma wt_nonzero i : wt i <> 0. - Proof. - apply Z.pow_nonzero; zero_bounds; try break_match; vm_decide. - Qed. - - Lemma wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0. - Proof. - cbv [In carry_chain1] in H. - repeat match goal with H : _ \/ _ |- _ => destruct H end; - try (exfalso; assumption); subst; try vm_decide. - Qed. - Lemma wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0. - Proof. - cbv [In carry_chain2] in H. - repeat match goal with H : _ \/ _ |- _ => destruct H end; - try (exfalso; assumption); subst; try vm_decide. - Qed. - Lemma wt_divides_full i : wt (S i) / wt i <> 0. - Proof. - cbv [wt]. - match goal with |- _ ^ ?x / _ ^ ?y <> _ => assert (0 <= y <= x) end. - { rewrite Nat2Z.inj_succ. - split; try break_match; ring_simplify; - repeat match goal with - | _ => apply Z.div_le_mono; try vm_decide; [ ] - | _ => apply Z.mul_le_mono_nonneg_l; try vm_decide; [ ] - | _ => apply Z.add_le_mono; try vm_decide; [ ] - | |- ?x <= ?y + 1 => assert (x <= y); [|omega] - | |- ?x + 1 <= ?y => rewrite <- Z.div_add by vm_decide - | _ => progress zero_bounds - | _ => progress ring_simplify - | _ => vm_decide - end. } - break_match; rewrite <-Z.pow_sub_r by omega; - apply Z.pow_nonzero; omega. - Qed. + Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed. + Lemma wt_divides i : wt (S i) / wt i > 0. + Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed. + Lemma wt_divides' i : wt (S i) / wt i <> 0. + Proof. symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides. Qed. + Definition wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0 := wt_divides' i. + Definition wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0 := wt_divides' i. Local Ltac solve_constant_sig := lazymatch goal with @@ -235,20 +209,10 @@ Section Ops51. Section PreFreeze. Lemma wt_pos i : wt i > 0. - Proof. - apply Z.lt_gt. - apply Z.pow_pos_nonneg; zero_bounds; try break_match; vm_decide. - Qed. + Proof. eapply pow_ceil_mul_nat_pos; vm_decide. Qed. Lemma wt_multiples i : wt (S i) mod (wt i) = 0. - Admitted. - - Lemma wt_divides_full_pos i : wt (S i) / wt i > 0. - Proof. - pose proof (wt_divides_full i). - apply Z.div_positive_gt_0; auto using wt_pos. - apply wt_multiples. - Qed. + Proof. apply pow_ceil_mul_nat_multiples; vm_decide. Qed. End PreFreeze. Hint Opaque freeze : uncps. @@ -263,7 +227,7 @@ Section Ops51. Proof. eexists; cbv beta zeta; intros a ?. pose proof wt_nonzero. pose proof wt_pos. - pose proof div_mod. pose proof wt_divides_full_pos. + pose proof div_mod. pose proof wt_divides. pose proof wt_multiples. pose proof div_correct. pose proof modulo_correct. let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in @@ -299,7 +263,7 @@ Section Ops51. (Positional.Fdecode_Fencode_id (sz_nonzero := sz_nonzero) (div_mod := div_mod) - wt eq_refl wt_nonzero wt_divides_full) + wt eq_refl wt_nonzero wt_divides') (Positional.eq_Feq_iff wt) (proj2_sig add_sig) (proj2_sig sub_sig) diff --git a/src/Specific/Karatsuba.v b/src/Specific/Karatsuba.v index 09e014667..7d329a613 100644 --- a/src/Specific/Karatsuba.v +++ b/src/Specific/Karatsuba.v @@ -9,6 +9,7 @@ Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics. Require Import Crypto.Arithmetic.Karatsuba. Require Crypto.Util.Tuple. Require Import Crypto.Util.IdfunWithAlt. +Require Import Crypto.Util.QUtil. Local Notation tuple := Tuple.tuple. Local Open Scope list_scope. Local Open Scope Z_scope. @@ -27,17 +28,18 @@ Section Ops51. Definition bitwidth := 64. Definition s : Z := 2^448. Definition c : list B.limb := [(1, 1); (2^224, 1)]. - Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *) Definition carry_chain1 := [3;7]%nat. Definition carry_chain2 := [0;4;1;5;2;6;3;7]%nat. Definition carry_chain3 := [4;0]%nat. - Definition a24 := 121665%Z. + Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *) (* These definitions are inferred from those above *) Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *) - Definition wt := fun i : nat => - let si := Z.log2 s * i in - 2 ^ ((si/sz) + (if dec ((si/sz)*sz=si) then 0 else 1)). + Section wt. + Import QArith Qround. + Local Coercion QArith_base.inject_Z : Z >-> Q. + Definition wt (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i). + End wt. Definition sz2 := Eval vm_compute in ((sz * 2) - 1)%nat. Definition m_enc := Eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c)). @@ -49,50 +51,16 @@ Section Ops51. | S n => addm (Positional.add_cps wt acc m_enc id) n end) (Positional.zeros sz) coef_div_modulus). Definition coef_mod : mod_eq m (Positional.eval (n:=sz) wt coef) 0 := eq_refl. - Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed. Lemma wt_nonzero i : wt i <> 0. - Proof. - apply Z.pow_nonzero; zero_bounds; try break_match; vm_decide. - Qed. - - Lemma wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0. - Proof. - cbv [In carry_chain1] in H. - repeat match goal with H : _ \/ _ |- _ => destruct H end; - try (exfalso; assumption); subst; try vm_decide. - Qed. - Lemma wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0. - Proof. - cbv [In carry_chain2] in H. - repeat match goal with H : _ \/ _ |- _ => destruct H end; - try (exfalso; assumption); subst; try vm_decide. - Qed. - Lemma wt_divides_chain3 i (H:In i carry_chain3) : wt (S i) / wt i <> 0. - Proof. - cbv [In carry_chain3] in H. - repeat match goal with H : _ \/ _ |- _ => destruct H end; - try (exfalso; assumption); subst; try vm_decide. - Qed. - Lemma wt_divides_full i : wt (S i) / wt i <> 0. - Proof. - cbv [wt]. - match goal with |- _ ^ ?x / _ ^ ?y <> _ => assert (0 <= y <= x) end. - { rewrite Nat2Z.inj_succ. - split; try break_match; ring_simplify; - repeat match goal with - | _ => apply Z.div_le_mono; try vm_decide; [ ] - | _ => apply Z.mul_le_mono_nonneg_l; try vm_decide; [ ] - | _ => apply Z.add_le_mono; try vm_decide; [ ] - | |- ?x <= ?y + 1 => assert (x <= y); [|omega] - | |- ?x + 1 <= ?y => rewrite <- Z.div_add by vm_decide - | _ => progress zero_bounds - | _ => progress ring_simplify - | _ => vm_decide - end. } - break_match; rewrite <-Z.pow_sub_r by omega; - apply Z.pow_nonzero; omega. - Qed. + Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed. + Lemma wt_divides i : wt (S i) / wt i > 0. + Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed. + Lemma wt_divides' i : wt (S i) / wt i <> 0. + Proof. symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides. Qed. + Definition wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0 := wt_divides' i. + Definition wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0 := wt_divides' i. + Definition wt_divides_chain3 i (H:In i carry_chain3) : wt (S i) / wt i <> 0 := wt_divides' i. Local Ltac solve_constant_sig := lazymatch goal with @@ -114,12 +82,6 @@ Section Ops51. solve_constant_sig. Defined. - Definition a24_sig : - { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m a24 }. - Proof. - solve_constant_sig. - Defined. - Definition add_sig : { add : (Z^sz -> Z^sz -> Z^sz)%type | forall a b : Z^sz, @@ -293,24 +255,11 @@ Ltac basesystem_partial_evaluation_RHS := solve_op_F wt x. reflexivity. Defined. - Section PreFreeze. - Lemma wt_pos i : wt i > 0. - Proof. - apply Z.lt_gt. - apply Z.pow_pos_nonneg; zero_bounds; try break_match; vm_decide. - Qed. - - Lemma wt_multiples i : wt (S i) mod (wt i) = 0. - Admitted. - - Lemma wt_divides_full_pos i : wt (S i) / wt i > 0. - Proof. - pose proof (wt_divides_full i). - apply Z.div_positive_gt_0; auto using wt_pos. - apply wt_multiples. - Qed. - End PreFreeze. - + (* [freeze] preconditions *) + Lemma wt_pos i : wt i > 0. + Proof. eapply pow_ceil_mul_nat_pos; vm_decide. Qed. + Lemma wt_multiples i : wt (S i) mod (wt i) = 0. + Proof. apply pow_ceil_mul_nat_multiples; vm_decide. Qed. Hint Opaque freeze : uncps. Hint Rewrite freeze_id : uncps. @@ -323,7 +272,7 @@ Ltac basesystem_partial_evaluation_RHS := Proof. eexists; cbv beta zeta; intros. pose proof wt_nonzero. pose proof wt_pos. - pose proof div_mod. pose proof wt_divides_full_pos. + pose proof div_mod. pose proof wt_divides. pose proof wt_multiples. pose proof div_correct. pose proof modulo_correct. let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in @@ -359,7 +308,7 @@ Ltac basesystem_partial_evaluation_RHS := (Positional.Fdecode_Fencode_id (sz_nonzero := sz_nonzero) (div_mod := div_mod) - wt eq_refl wt_nonzero wt_divides_full) + wt eq_refl wt_nonzero wt_divides') (Positional.eq_Feq_iff wt) (proj2_sig add_sig) (proj2_sig sub_sig) diff --git a/src/Util/QUtil.v b/src/Util/QUtil.v index 453cad308..96bf34c3b 100644 --- a/src/Util/QUtil.v +++ b/src/Util/QUtil.v @@ -1,19 +1,107 @@ Require Import Coq.ZArith.ZArith Coq.QArith.QArith QArith.Qround. +Require Import Crypto.Util.Decidable. +Require Import ZUtil Lia. Local Open Scope Z_scope. -Lemma pow_ceil_mul_nat_nonzero b f - (b_nz:b <> 0) - (f_pos:(0 <= f)%Q) - : forall i, b^Qceiling (f * inject_Z (Z.of_nat i)) <> 0. -Proof. - intros. - eapply Z.pow_nonzero; try omega. - rewrite Zle_Qle. - eapply Qle_trans; [|eapply Qle_ceiling]. - eapply Qle_trans; [|eapply (Qmult_le_compat_r 0)]; trivial. - cbv; discriminate. - apply (Qle_trans _ (inject_Z 0)); [eapply Qle_refl|]. - rewrite <-Zle_Qle. - eapply Zle_0_nat. -Qed.
\ No newline at end of file +Lemma Qfloor_le_add a b : Qfloor a + Qfloor b <= Qfloor (a + b). + destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum]. + Z.div_mod_to_quot_rem; nia. +Qed. + +Lemma Qceiling_le_add a b : Qceiling (a + b) <= Qceiling a + Qceiling b. + destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum]. + Z.div_mod_to_quot_rem. nia. +Qed. + +Lemma add_floor_l_le_ceiling a b : Qfloor a + Qceiling b <= Qceiling (a + b). + destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum]. + Z.div_mod_to_quot_rem; nia. +Qed. + +Lemma Zle_floor_ceiling a : Z.le (Qfloor a) (Qceiling a). + pose proof Qle_floor_ceiling. + destruct a as [x y]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum]. + Z.div_mod_to_quot_rem; nia. +Qed. + +Section pow_ceil_mul_nat. + Context b f (b_nz:0 <> b) (f_pos:(0 <= f)%Q). + Local Notation wt i := (b^Qceiling (f * inject_Z (Z.of_nat i))) (only parsing). + + Lemma zero_le_ceil_mul_nat i : + 0 <= Qceiling (f * inject_Z (Z.of_nat i))%Q. + Proof. + rewrite Zle_Qle. + eapply Qle_trans; [|eapply Qle_ceiling]. + eapply Qle_trans; [|eapply (Qmult_le_compat_r 0)]; trivial. + cbv; discriminate. + apply (Qle_trans _ (inject_Z 0)); [vm_decide|]. + change 0%Q with (inject_Z 0). + rewrite <-Zle_Qle. + eapply Zle_0_nat. + Qed. + + Lemma pow_ceil_mul_nat_nonzero + : forall i, wt i <> 0. + Proof. + intros. + eapply Z.pow_nonzero; try omega. + eapply zero_le_ceil_mul_nat. + Qed. + + Lemma pow_ceil_mul_S i : + wt (S i) = + (b ^ (Qceiling (f + f * inject_Z (Z.of_nat i)) - Qceiling (f * inject_Z (Z.of_nat i))) * wt i). + Proof. + rewrite Nat2Z.inj_succ. + rewrite <-Z.add_1_l. + rewrite inject_Z_plus. + change (inject_Z 1) with 1%Q. + rewrite Qmult_plus_distr_r, Qmult_1_r. + let g := constr:((f * inject_Z (Z.of_nat i))%Q) in + replace (Qceiling (f+g)) with ((Qceiling (f+g)-Qceiling g)+Qceiling g) at 1 by omega. + rewrite Z.pow_add_r; [reflexivity|eapply Zle_minus_le_0|apply zero_le_ceil_mul_nat]. + eapply Qceiling_resp_le. + rewrite <-Qplus_0_l at 1. + eapply Qplus_le_compat; + auto with qarith. + Qed. + + Lemma pow_ceil_mul_nat_multiples i : + wt (S i) mod (wt i) = 0. + Proof. + rewrite pow_ceil_mul_S, Z_mod_mult; reflexivity. + Qed. +End pow_ceil_mul_nat. + +Section pow_ceil_mul_nat2. + Context b f (b_pos:0 < b) (f_ge_1:(1 <= f)%Q). + Local Notation wt i := (b^Qceiling (f * inject_Z (Z.of_nat i))) (only parsing). + + Lemma pow_ceil_mul_nat_pos + : forall i, wt i > 0. + Proof. + intros. + eapply Z.gt_lt_iff. + eapply Z.pow_pos_nonneg; [assumption|]. + eapply zero_le_ceil_mul_nat. + eapply (Qle_trans _ 1 _); [vm_decide|assumption]. + Qed. + + Lemma pow_ceil_mul_nat_divide i : + wt (S i) / (wt i) > 0. + Proof. + rewrite pow_ceil_mul_S. + rewrite Z_div_mult_full; [|apply pow_ceil_mul_nat_nonzero]. + rewrite Z.gt_lt_iff. + eapply Z.pow_pos_nonneg; [assumption|]. + etransitivity; [|eapply Z.sub_le_ge_Proper]. + 2:eapply add_floor_l_le_ceiling. + 2:eapply Z.ge_le_iff; reflexivity. + assert (1 <= Qfloor f); [|omega]. + change 1%Z with (Qfloor 1). + eapply Qfloor_resp_le. + all: trivial; try omega; (eapply (Qle_trans _ 1 _); [vm_decide|assumption]). + Qed. +End pow_ceil_mul_nat2.
\ No newline at end of file |