diff options
author | jadep <jade.philipoom@gmail.com> | 2016-08-31 09:43:55 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-08-31 10:03:57 -0400 |
commit | da8a8d84e4a07aff1be5b7754cd686d4f7da7dd8 (patch) | |
tree | 68dca8ea508323d7517b42a5cf1b2501745f500c /src/ModularArithmetic | |
parent | 8889a7b29faca543c4727455f34bcde36cefcdcf (diff) |
Added square roots to GF1305, started reworking freeze_opt in preparation for instantiating it in GF25519 (needed for equality comparison in sqrt_5mod8)
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 134 |
1 files changed, 129 insertions, 5 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 9b482ed89..cb79ff868 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -883,13 +883,37 @@ Section Canonicalization. carry_full_3_opt_cps f us = f (carry_full (carry_full (carry_full us))) := proj2_sig (carry_full_3_opt_cps_sig f us). + Definition conditional_subtract_modulus_opt_sig (f : list Z) (cond : bool) : + { g | g = conditional_subtract_modulus f cond}. + Proof. + eexists. + cbv [conditional_subtract_modulus]. + match goal with |- appcontext[if cond then ?a else ?b] => + let LHS := match goal with |- ?LHS = ?RHS => LHS end in + let RHS := match goal with |- ?LHS = ?RHS => RHS end in + let RHSf := match (eval pattern (if cond then a else b) in RHS) with ?RHSf _ => RHSf end in + change (LHS = Let_In (if cond then a else b) RHSf) end. + cbv [map2 map]. + change modulus_digits with modulus_digits_opt. + change @max_ones with max_ones_opt. + reflexivity. + Defined. + + Definition conditional_subtract_modulus_opt f cond : list Z + := Eval cbv [proj1_sig conditional_subtract_modulus_opt_sig] in proj1_sig (conditional_subtract_modulus_opt_sig f cond). + + Definition conditional_subtract_modulus_opt_correct f cond + : conditional_subtract_modulus_opt f cond = conditional_subtract_modulus f cond + := Eval cbv [proj2_sig conditional_subtract_modulus_opt_sig] in proj2_sig (conditional_subtract_modulus_opt_sig f cond). + Definition freeze_opt_sig (us : digits) : { b : digits | b = freeze us }. Proof. eexists. - cbv [freeze conditional_subtract_modulus]. + cbv [freeze]. rewrite <-from_list_default_eq with (d := 0%Z). change (@from_list_default Z) with (@from_list_default_opt Z). + rewrite <-conditional_subtract_modulus_opt_correct. let LHS := match goal with |- ?LHS = ?RHS => LHS end in let RHS := match goal with |- ?LHS = ?RHS => RHS end in let RHSf := match (eval pattern (to_list (length limb_widths) (carry_full (carry_full (carry_full us)))) in RHS) with ?RHSf _ => RHSf end in @@ -901,12 +925,8 @@ Section Canonicalization. cbv beta iota delta [ge_modulus ge_modulus']. change length with length_opt. change (nth_default 0 modulus_digits) with (nth_default_opt 0 modulus_digits_opt). - change @max_ones with max_ones_opt. change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. change minus with minus_opt. - change @map with @map_opt. - change Z.sub with Z_sub_opt at 1. - rewrite <-modulus_digits_opt_correct. reflexivity. Defined. @@ -919,3 +939,107 @@ Section Canonicalization. End Canonicalization. +Section SquareRoots. + Context `{prm : PseudoMersenneBaseParams}. + Context {cc : CarryChain limb_widths}. + Local Notation digits := (tuple Z (length limb_widths)). + (* allows caller to precompute k and c *) + Context (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_) + (one_ : digits) (one_subst : one = one_). + + Definition eqb_opt_sig (us vs : digits) : + { b | b = ModularBaseSystem.eqb us vs}. + Proof. + eexists; cbv [ModularBaseSystem.eqb]. + cbv [fieldwiseb fieldwiseb']. + erewrite <-!freeze_opt_correct by eassumption. + reflexivity. + Defined. + + Definition eqb_opt us vs := Eval cbv [proj1_sig eqb_opt_sig] in proj1_sig (eqb_opt_sig us vs). + + Definition eqb_opt_correct us vs + : eqb_opt us vs = ModularBaseSystem.eqb us vs + := Eval cbv [proj2_sig eqb_opt_sig] in proj2_sig (eqb_opt_sig us vs). + + (* TODO : where should this lemma go? Alternatively, is there a standard-library + tactic/lemma for this? *) + Lemma if_equiv : forall {A} (eqA : A -> A -> Prop) (x0 x1 : bool) y0 y1 z0 z1, + x0 = x1 -> eqA y0 y1 -> eqA z0 z1 -> + eqA (if x0 then y0 else z0) (if x1 then y1 else z1). + Proof. + intros; repeat break_if; congruence. + Qed. + + Section SquareRoot3mod4. + Context {ec : ExponentiationChain (modulus / 4 + 1)}. + + Definition sqrt_3mod4_opt_sig (us : digits) : + { vs : digits | eq vs (sqrt_3mod4 chain chain_correct us)}. + Proof. + eexists; cbv [sqrt_3mod4]. + apply @pow_opt_correct; eassumption. + Defined. + + Definition sqrt_3mod4_opt us := Eval cbv [proj1_sig sqrt_3mod4_opt_sig] in + proj1_sig (sqrt_3mod4_opt_sig us). + + Definition sqrt_3mod4_opt_correct us + : eq (sqrt_3mod4_opt us) (sqrt_3mod4 chain chain_correct us) + := Eval cbv [proj2_sig sqrt_3mod4_opt_sig] in proj2_sig (sqrt_3mod4_opt_sig us). + + End SquareRoot3mod4. + + Import Morphisms. + Global Instance eqb_Proper : Proper (eq ==> eq ==> Logic.eq) ModularBaseSystem.eqb. Admitted. + + Section SquareRoot5mod8. + Context {ec : ExponentiationChain (modulus / 8 + 1)}. + Context (sqrt_m1 : digits) (sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F)). + + Definition sqrt_5mod8_opt_sig (us : digits) : + { vs : digits | eq vs (sqrt_5mod8 chain chain_correct sqrt_m1 us)}. + Proof. + eexists; cbv [sqrt_5mod8]. + etransitivity. + Focus 2. { + apply if_equiv. { + apply eqb_Proper; [ | reflexivity ]. + transitivity (carry_mul_opt k_ c_ (pow_opt k_ c_ one_ us chain) (pow_opt k_ c_ one_ us chain)); [ reflexivity | ]. + cbv [eq]. + rewrite carry_mul_opt_correct by eassumption. + rewrite carry_mul_rep by reflexivity. + rewrite mul_rep by reflexivity. + f_equal; apply pow_opt_correct; auto. + } { + apply pow_opt_correct; auto. + } { + match goal with |- eq _ (mul ?a (ModularBaseSystem.pow ?d ?e)) => + transitivity (carry_mul_opt k_ c_ a (pow_opt k_ c_ one_ us chain)); [ reflexivity | ] end. + cbv [eq]. + rewrite !mul_rep by reflexivity. + erewrite <-pow_opt_correct by eassumption. + rewrite <-carry_mul_rep by reflexivity. + erewrite <-carry_mul_opt_correct by eassumption. + reflexivity. + } + } Unfocus. + rewrite <-eqb_opt_correct. + rewrite k_subst, c_subst, one_subst. + let LHS := match goal with |- eq ?LHS ?RHS => LHS end in + let RHS := match goal with |- eq ?LHS ?RHS => RHS end in + let RHSf := match (eval pattern (pow_opt k_ c_ one_ us chain) in RHS) with ?RHSf _ => RHSf end in + change (eq LHS (Let_In (pow_opt k_ c_ one_ us chain) RHSf)). + reflexivity. + Defined. + + Definition sqrt_5mod8_opt us := Eval cbv [proj1_sig sqrt_5mod8_opt_sig] in + proj1_sig (sqrt_5mod8_opt_sig us). + + Definition sqrt_5mod8_opt_correct us + : eq (sqrt_5mod8_opt us) (ModularBaseSystem.sqrt_5mod8 chain chain_correct sqrt_m1 us) + := Eval cbv [proj2_sig sqrt_5mod8_opt_sig] in proj2_sig (sqrt_5mod8_opt_sig us). + + End SquareRoot5mod8. + +End SquareRoots. |