From f670e48c3b74fbb3a9f21d6c9351b08593af311f Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 1 Nov 2016 16:57:04 -0400 Subject: Changes to sqrt for easier bounds proofs; currently blocked on broken proof in GF25519Bounded --- src/ModularArithmetic/ModularBaseSystem.v | 7 ++-- src/ModularArithmetic/ModularBaseSystemOpt.v | 41 +++++++++++++--------- src/ModularArithmetic/ModularBaseSystemProofs.v | 46 ++++++++----------------- 3 files changed, 42 insertions(+), 52 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index d8303d1a7..6df49173e 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -95,13 +95,10 @@ Section ModularBaseSystem. (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 4 + 1)) (x : digits) : digits := pow x chain. - (* sqrt_5mod8 is parameterized over implementation of [mul] and [pow] because it relies on bounds-checking - for these two functions, which is much easier for simplified implementations than the more generalized - ones defined here. *) - Definition sqrt_5mod8 B mul_ pow_ (chain : list (nat * nat)) + Definition sqrt_5mod8 B powx powx_squared (chain : list (nat * nat)) (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 8 + 1)) (sqrt_minus1 x : digits) : digits := - let b := pow_ x chain in if eqb B (mul_ b b) x then b else mul_ sqrt_minus1 b. + if eqb B powx_squared x then powx else mul sqrt_minus1 powx. Import Morphisms. Global Instance eq_Equivalence : Equivalence eq. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index f7f6efad7..d302f83a8 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -1069,32 +1069,41 @@ Section SquareRoots. End SquareRoot3mod4. - Import Morphisms. - Global Instance eqb_Proper : Proper (Logic.eq ==> 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)). Context {int_width} (preconditions : freezePreconditions prm int_width). - Definition sqrt_5mod8_opt_sig (us : digits) : + Definition sqrt_5mod8_opt_sig (powx powx_squared us : digits) : { vs : digits | - eq vs (sqrt_5mod8 int_width (carry_mul_opt k_ c_) (pow_opt k_ c_ one_) chain chain_correct sqrt_m1 us)}. + eq vs (sqrt_5mod8 int_width powx powx_squared chain chain_correct sqrt_m1 us)}. Proof. - eexists; cbv [sqrt_5mod8]. - 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. + cbv [sqrt_5mod8]. + match goal with + |- appcontext[(if ?P then ?t else mul ?a ?b)] => + assert (eq (carry_mul_opt k_ c_ a b) (mul a b)) + by (rewrite carry_mul_opt_correct by auto; + cbv [eq]; rewrite carry_mul_rep, mul_rep; reflexivity) + end. + let RHS := match goal with |- {vs | eq ?vs ?RHS} => RHS end in + let RHSf := match (eval pattern powx in RHS) with ?RHSf _ => RHSf end in + change ({vs | eq vs (Let_In powx RHSf)}). + match goal with + | H : eq (?g powx) (?f powx) + |- {vs | eq vs (Let_In powx (fun x => if ?P then x else ?f x))} => + exists (Let_In powx (fun x => if P then x else g x)) + end. + break_if; try reflexivity. + cbv [Let_In]. + auto. 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 powx powx_squared us := Eval cbv [proj1_sig sqrt_5mod8_opt_sig] in + proj1_sig (sqrt_5mod8_opt_sig powx powx_squared us). - Definition sqrt_5mod8_opt_correct us - : eq (sqrt_5mod8_opt us) (ModularBaseSystem.sqrt_5mod8 int_width _ _ chain chain_correct sqrt_m1 us) - := Eval cbv [proj2_sig sqrt_5mod8_opt_sig] in proj2_sig (sqrt_5mod8_opt_sig us). + Definition sqrt_5mod8_opt_correct powx powx_squared us + : eq (sqrt_5mod8_opt powx powx_squared us) (ModularBaseSystem.sqrt_5mod8 int_width _ _ chain chain_correct sqrt_m1 us) + := Eval cbv [proj2_sig sqrt_5mod8_opt_sig] in proj2_sig (sqrt_5mod8_opt_sig powx powx_squared us). End SquareRoot5mod8. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 330dc4e2f..b454daab6 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -1017,7 +1017,7 @@ Section SquareRootProofs. then 0 else (2 ^ B) >> (nth_default 0 limb_widths (pred n)))). Definition bounded_by u bounds := - (forall n : nat, + (forall n : nat, (n < length limb_widths)%nat -> 0 <= nth_default 0 (to_list (length limb_widths) u) n < bounds n). Lemma eqb_true_iff : forall u v x y, @@ -1063,48 +1063,32 @@ Section SquareRootProofs. Context (modulus_5mod8 : modulus mod 8 = 5). Context {ec : ExponentiationChain (modulus / 8 + 1)}. Context (sqrt_m1 : digits) (sqrt_m1_correct : mul sqrt_m1 sqrt_m1 ~= F.opp 1%F). - Context (mul_ : digits -> digits -> digits) - (mul_equiv : forall x y, ModularBaseSystem.eq (mul_ x y) (mul x y)) - {mul_input_bounds : nat -> Z} - (mul_bounded : forall x y, bounded_by x mul_input_bounds -> - bounded_by y mul_input_bounds -> - bounded_by (mul_ x y) freeze_input_bounds). - Context (pow_ : digits -> list (nat * nat) -> digits) - (pow_equiv : forall x is, ModularBaseSystem.eq (pow_ x is) (pow x is)) - {pow_input_bounds : nat -> Z} - (pow_bounded : forall x is, bounded_by x pow_input_bounds -> - bounded_by (pow_ x is) mul_input_bounds). - - Lemma sqrt_5mod8_correct : forall u x, u ~= x -> - bounded_by u pow_input_bounds -> bounded_by u freeze_input_bounds -> - (sqrt_5mod8 B mul_ pow_ chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. + + Lemma sqrt_5mod8_correct : forall u x powx powx_squared, u ~= x -> + bounded_by u freeze_input_bounds -> + bounded_by powx_squared freeze_input_bounds -> + ModularBaseSystem.eq powx (pow u chain) -> + ModularBaseSystem.eq powx_squared (mul powx powx) -> + (sqrt_5mod8 B powx powx_squared chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. Proof. cbv [sqrt_5mod8 F.sqrt_5mod8]. intros. repeat match goal with | |- _ => progress (cbv [sqrt_5mod8 F.sqrt_5mod8]; intros) | |- _ => rewrite @F.pow_2_r in * - | |- _ => rewrite mul_equiv - | |- _ => rewrite pow_equiv | |- _ => rewrite eqb_correct in * by eassumption | |- (if eqb _ ?a ?b then _ else _) ~= (if dec (?c = _) then _ else _) => - assert (a ~= c) by (cbv [rep]; rewrite mul_equiv; - apply mul_rep; cbv [rep]; - rewrite pow_equiv, <-chain_correct; - apply pow_rep; auto); - cbv [rep]; rewrite ?mul_equiv, ?pow_equiv; - repeat break_if + assert (a ~= c) by + (cbv [rep]; rewrite <-chain_correct, <-pow_rep, <-mul_rep; + eassumption); repeat break_if | |- _ => apply mul_rep; try reflexivity; - rewrite <-chain_correct; cbv [rep]; - rewrite pow_equiv; apply pow_rep; eassumption - | |- _ => rewrite <-chain_correct; apply pow_rep; eassumption + rewrite <-chain_correct, <-pow_rep; eassumption + | |- _ => rewrite <-chain_correct, <-pow_rep; eassumption | H : eqb _ ?a ?b = true, H1 : ?b ~= ?y, H2 : ?a ~= ?x |- _ => - rewrite <-(eqb_true_iff a b x y) in H - by (eassumption || apply mul_bounded, pow_bounded; auto) + rewrite <-(eqb_true_iff a b x y) in H by eassumption | H : eqb _ ?a ?b = false, H1 : ?b ~= ?y, H2 : ?a ~= ?x |- _ => - rewrite <-(eqb_false_iff a b x y) in H - by (eassumption || apply mul_bounded, pow_bounded; auto) + rewrite <-(eqb_false_iff a b x y) in H by eassumption | |- _ => congruence end. Qed. -- cgit v1.2.3