diff options
author | jadep <jade.philipoom@gmail.com> | 2016-08-28 16:29:16 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-08-31 10:03:57 -0400 |
commit | a8f0148ef74356e7e11faede459cd271503d088f (patch) | |
tree | a8282b34a4e28aeed351b38970cf558340bb35db | |
parent | b52edcb4a5ba5757b3a384997d501611aa1feb00 (diff) |
Proofs for MBS square roots.
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 56 |
1 files changed, 56 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 1369bbbf1..cdcf17e8b 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -696,4 +696,60 @@ Section CanonicalizationProofs. in BaseSystem in canonical form, splitting along word capacities) *) + Lemma freeze_canonical : forall u v x y, rep u x -> rep v y -> + (x = y <-> fieldwise Logic.eq (freeze u) (freeze v)). + Admitted. + End CanonicalizationProofs. + +Section SquareRootProofs. + Context `{prm : PseudoMersenneBaseParams}. + Local Notation "u ~= x" := (rep u x). + Local Notation digits := (tuple Z (length limb_widths)). + Local Notation base := (base_from_limb_widths limb_widths). + Local Hint Resolve (@limb_widths_nonneg _ prm) sum_firstn_limb_widths_nonneg. + + Lemma eqb_correct : forall u v x y, u ~= x -> v ~= y -> + (x = y <-> eqb u v = true). + Proof. + cbv [eqb]. intros. + rewrite fieldwiseb_fieldwise by (apply Z.eqb_eq). + auto using freeze_canonical. + Qed. + + Section Sqrt3mod4. + Context (modulus_3mod4 : modulus mod 4 = 3). + + Lemma sqrt_3mod4_correct : forall u x chain pf, u ~= x -> + (sqrt_3mod4 chain pf u) ~= F.sqrt_3mod4 x. + Proof. + repeat match goal with + | |- _ => progress (cbv [sqrt_3mod4 F.sqrt_3mod4]; intros) + | |- _ => rewrite @F.pow_2_r in * + | |- _ => rewrite eqb_correct in * by eassumption + | |- _ => rewrite <-pf; apply pow_rep; eassumption + end. + Qed. + End Sqrt3mod4. + + Section Sqrt5mod8. + Context (modulus_5mod8 : modulus mod 8 = 5). + Context (sqrt_m1 : digits) (sqrt_m1_correct : mul sqrt_m1 sqrt_m1 ~= F.opp 1%F). + + Lemma sqrt_5mod8_correct : forall u x chain pf, u ~= x -> + (sqrt_5mod8 chain pf sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. + Proof. + repeat match goal with + | |- _ => progress (cbv [sqrt_5mod8 F.sqrt_5mod8]; intros) + | |- _ => rewrite @F.pow_2_r in * + | |- _ => rewrite eqb_correct in * by eassumption + | |- (if eqb ?a ?b then _ else _) ~= + (if dec (?c = _) then _ else _) => + assert (a ~= c); repeat break_if; try apply mul_rep; + try solve [rewrite <-pf; apply pow_rep; eassumption] + | |- _ => congruence + end. + Qed. + End Sqrt5mod8. + +End SquareRootProofs.
\ No newline at end of file |