From c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 6 Apr 2017 22:53:07 -0400 Subject: rename-everything --- src/Primitives/EdDSARepChange.v | 308 ++++++++++++++++++++++++++++++++++++++++ src/Primitives/MxDHRepChange.v | 162 +++++++++++++++++++++ 2 files changed, 470 insertions(+) create mode 100644 src/Primitives/EdDSARepChange.v create mode 100644 src/Primitives/MxDHRepChange.v (limited to 'src/Primitives') diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v new file mode 100644 index 000000000..1ad4611be --- /dev/null +++ b/src/Primitives/EdDSARepChange.v @@ -0,0 +1,308 @@ +Require Import Crypto.Util.FixCoqMistakes. +Require Import Crypto.Spec.EdDSA Bedrock.Word. +Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions. +Require Import Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.ScalarMult. +Require Import Crypto.Util.Decidable Crypto.Util.Option. +Require Import Crypto.Util.Tactics.SetEvars. +Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Coq.omega.Omega. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Util.LetIn Util.NatUtil. +Require Import Crypto.Spec.ModularArithmetic Crypto.Arithmetic.PrimeFieldTheorems. +Import NPeano. + +Import Notations. + +Section EdDSA. + Context `{prm:EdDSA}. + Local Infix "==" := Eeq. Local Infix "+" := Eadd. Local Infix "*" := EscalarMult. + + Local Notation valid := (@valid E Eeq Eadd EscalarMult b H l B Eenc Senc). + Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M). + Proof using Type. + cbv [sign public Spec.EdDSA.valid]; intros; subst; + repeat match goal with + | |- exists _, _ => eexists + | |- _ /\ _ => eapply conj + | |- _ => reflexivity + end. + rewrite F.to_nat_of_nat, scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, NPeano.Nat.mul_comm, scalarmult_assoc; + try solve [ reflexivity + | setoid_rewrite (*unify 0*) (Z2Nat.inj_iff _ 0); pose proof EdDSA_l_odd; omega + | pose proof EdDSA_l_odd; omega + | apply EdDSA_l_order_B + | rewrite scalarmult_assoc, mult_comm, <-scalarmult_assoc, + EdDSA_l_order_B, scalarmult_zero_r; reflexivity ]. + Qed. + + Lemma solve_for_R_sig : forall s B R n A, { solution | s * B == R + n * A <-> R == solution }. + Proof. + eexists. + set_evars. + setoid_rewrite <-(symmetry_iff(R:=Eeq)) at 1. + setoid_rewrite <-eq_r_opp_r_inv. + setoid_rewrite opp_mul. + subst_evars. + reflexivity. + Defined. + Definition solve_for_R := Eval cbv [proj2_sig solve_for_R_sig] in (fun s B R n A => proj2_sig (solve_for_R_sig s B R n A)). + + Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}. + Global Instance Proper_eq_Eenc ref : Proper (Eeq ==> iff) (fun P => Eenc P = ref). + Proof using Proper_Eenc. intros ? ? Hx; rewrite Hx; reflexivity. Qed. + + Context {Edec:word b-> option E} {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> option_eq Eeq (Edec P_) (Some P)}. + Context {Sdec:word b-> option (F l)} {eq_enc_S_iff: forall n_ n, Senc n = n_ <-> Sdec n_ = Some n}. + + Local Infix "++" := combine. + Definition verify'_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)), + verify mlen message pk sig = true <-> valid message pk sig }. + Proof. + eexists; intros; set_evars. + unfold Spec.EdDSA.valid. + setoid_rewrite solve_for_R. + setoid_rewrite combine_eq_iff. + setoid_rewrite and_comm at 4. setoid_rewrite and_assoc. repeat setoid_rewrite exists_and_indep_l. + setoid_rewrite (and_rewrite_l Eenc (split1 b b sig) + (fun x y => x == _ * B + wordToNat (H _ (y ++ Eenc _ ++ message)) mod _ * Eopp _)); setoid_rewrite eq_enc_S_iff. + setoid_rewrite (@exists_and_equiv_r _ _ _ _ _ _). + setoid_rewrite <- (fun A => and_rewriteleft_l (fun x => x) (Eenc A) (fun pk EencA => exists a, + Sdec (split2 b b sig) = Some a /\ + Eenc (_ * B + wordToNat (H (b + (b + mlen)) (split1 b b sig ++ EencA ++ message)) mod _ * Eopp A) + = split1 b b sig)). setoid_rewrite (eq_enc_E_iff pk). + setoid_rewrite <-weqb_true_iff. + setoid_rewrite <-option_rect_false_returns_true_iff_eq. + rewrite <-option_rect_false_returns_true_iff by + (intros ? ? Hxy; unfold option_rect; break_match; rewrite <-?Hxy; reflexivity). + + subst_evars. + (* TODO: generalize this higher order reflexivity *) + match goal with + |- ?f ?mlen ?msg ?pk ?sig = true <-> ?term = true + => let term := eval pattern sig in term in + let term := eval pattern pk in term in + let term := eval pattern msg in term in + let term := match term with + (fun msg => (fun pk => (fun sig => @?body msg pk sig) sig) pk) msg => + body + end in + let term := eval pattern mlen in term in + let term := match term with + (fun mlen => @?body mlen) mlen => body + end in + unify f term; reflexivity + end. + Defined. + Definition verify' {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool := + Eval cbv [proj1_sig verify'_sig] in proj1_sig verify'_sig mlen message pk sig. + Lemma verify'_correct : forall {mlen} (message:word mlen) pk sig, + verify' message pk sig = true <-> valid message pk sig. + Proof using Type*. exact (proj2_sig verify'_sig). Qed. + + Section ChangeRep. + Context {Erep ErepEq ErepAdd ErepId ErepOpp} {Agroup:@Algebra.Hierarchy.group Erep ErepEq ErepAdd ErepId ErepOpp}. + Context {EToRep} {Ahomom:@is_homomorphism E Eeq Eadd Erep ErepEq ErepAdd EToRep}. + + Context {ERepEnc : Erep -> word b} + {ERepEnc_correct : forall P:E, Eenc P = ERepEnc (EToRep P)} + {Proper_ERepEnc:Proper (ErepEq==>Logic.eq) ERepEnc}. + + Context {ERepDec : word b -> option Erep} + {ERepDec_correct : forall w, option_eq ErepEq (ERepDec w) (option_map EToRep (Edec w)) }. + + Context {SRep SRepEq} `{@Equivalence SRep SRepEq} {S2Rep:F l->SRep}. + + Context {SRepDecModL} {SRepDecModL_correct: forall (w:word (b+b)), SRepEq (S2Rep (F.of_nat _ (wordToNat w))) (SRepDecModL w)}. + + Context {SRepERepMul:SRep->Erep->Erep} + {SRepERepMul_correct:forall n P, ErepEq (EToRep ((n mod Z.to_nat l)*P)) (SRepERepMul (S2Rep (F.of_nat _ n)) (EToRep P))} + {Proper_SRepERepMul: Proper (SRepEq==>ErepEq==>ErepEq) SRepERepMul}. + + Context {SRepDec: word b -> option SRep} + {SRepDec_correct : forall w, option_eq SRepEq (option_map S2Rep (Sdec w)) (SRepDec w)}. + + Definition verify_using_representation + {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) + : { answer | answer = verify' message pk sig }. + Proof. + eexists. + pose proof EdDSA_l_odd. + cbv [verify']. + + etransitivity. Focus 2. { + eapply Proper_option_rect_nd_changebody; [intro|reflexivity]. + eapply Proper_option_rect_nd_changebody; [intro|reflexivity]. + rewrite <-F.to_nat_mod by omega. + repeat ( + rewrite ERepEnc_correct + || rewrite homomorphism + || rewrite homomorphism_id + || rewrite (homomorphism_inv(INV:=Eopp)(inv:=ErepOpp)(eq:=ErepEq)(phi:=EToRep)) + || rewrite SRepERepMul_correct + || rewrite SdecS_correct + || rewrite SRepDecModL_correct + || rewrite (@F.of_nat_to_nat _ _) + || rewrite (@F.of_nat_mod _ _) + ). + reflexivity. + } Unfocus. + + (* lazymatch goal with |- _ _ (option_rect _ ?some _ _) => idtac some end. *) + setoid_rewrite (option_rect_option_map EToRep + (fun s => + option_rect (fun _ : option _ => bool) + (fun s0 => + weqb + (ERepEnc + (ErepAdd (SRepERepMul (_ s0) (EToRep B)) + (SRepERepMul + (SRepDecModL + (H _ (split1 b b sig ++ pk ++ message))) + (ErepOpp (s))))) (split1 b b sig)) false + (Sdec (split2 b b sig))) + false). + (* rewrite with a complicated proper instance for inline code .. *) + etransitivity; + [| eapply Proper_option_rect_nd_changevalue; + [ + | reflexivity + | eapply ERepDec_correct + ]; + [ repeat match goal with + | |- _ => intro + | |- _ => eapply Proper_option_rect_nd_changebody + | |- ?R ?x ?x => reflexivity + | H : _ |- _ => rewrite H; reflexivity + end + ] + ]. + + etransitivity. Focus 2. { + eapply Proper_option_rect_nd_changebody; [intro|reflexivity]. + set_evars. + setoid_rewrite (option_rect_option_map S2Rep + (fun s0 => + weqb + (ERepEnc + (ErepAdd (SRepERepMul (s0) (EToRep B)) + (SRepERepMul + (SRepDecModL (H _ (split1 b b sig ++ pk ++ message))) + (ErepOpp _)))) (split1 b b sig)) + + false). + subst_evars. + + eapply Proper_option_rect_nd_changevalue; + [repeat intro; repeat f_equiv; eassumption|reflexivity|..]. + + symmetry. + eapply SRepDec_correct. + } Unfocus. + + reflexivity. + Defined. + + Definition verify {mlen} (msg:word mlen) pk sig := + Eval cbv beta iota delta [proj1_sig verify_using_representation] in + proj1_sig (verify_using_representation msg pk sig). + Lemma verify_correct {mlen} (msg:word mlen) pk sig : verify msg pk sig = true <-> valid msg pk sig. + Proof using Type*. + etransitivity; [|eapply (verify'_correct msg pk sig)]. + eapply iff_R_R_same_r, (proj2_sig (verify_using_representation _ _ _)). + Qed. + + Context {SRepEnc : SRep -> word b} + {SRepEnc_correct : forall x, Senc x = SRepEnc (S2Rep x)} + {Proper_SRepEnc:Proper (SRepEq==>Logic.eq) SRepEnc}. + Context {SRepAdd : SRep -> SRep -> SRep} + {SRepAdd_correct : forall x y, SRepEq (S2Rep (x+y)%F) (SRepAdd (S2Rep x) (S2Rep y)) } + {Proper_SRepAdd:Proper (SRepEq==>SRepEq==>SRepEq) SRepAdd}. + Context {SRepMul : SRep -> SRep -> SRep} + {SRepMul_correct : forall x y, SRepEq (S2Rep (x*y)%F) (SRepMul (S2Rep x) (S2Rep y)) } + {Proper_SRepMul:Proper (SRepEq==>SRepEq==>SRepEq) SRepMul}. + Context {ErepB:Erep} {ErepB_correct:ErepEq ErepB (EToRep B)}. + + Context {SRepDecModLShort} {SRepDecModLShort_correct: forall (w:word (n+1)), SRepEq (S2Rep (F.of_nat _ (wordToNat w))) (SRepDecModLShort w)}. + + (* We would ideally derive the optimized implementations from + specifications using `setoid_rewrite`, but doing this without + inlining let-bound subexpressions turned out to be quite messy in + the current state of Coq: *) + + Let n_le_bpb : (n <= b+b)%nat. destruct prm. omega. Qed. + + Definition splitSecretPrngCurve (sk:word b) : SRep * word b := + dlet hsk := H _ sk in + dlet curveKey := SRepDecModLShort (clearlow c (@wfirstn n _ hsk n_le_bpb) ++ wones 1) in + dlet prngKey := split2 b b hsk in + (curveKey, prngKey). + + Lemma splitSecretPrngCurve_correct sk : + let (s, r) := splitSecretPrngCurve sk in + SRepEq s (S2Rep (F.of_nat l (curveKey sk))) /\ r = prngKey (H:=H) sk. + Proof using H0 SRepDecModLShort_correct. + cbv [splitSecretPrngCurve EdDSA.curveKey EdDSA.prngKey Let_In]; split; + repeat ( + reflexivity + || rewrite <-SRepDecModLShort_correct + || rewrite wordToNat_split1 + || rewrite wordToNat_wfirstn + || rewrite wordToNat_combine + || rewrite wordToNat_clearlow + || rewrite (eq_refl:wordToNat (wones 1) = 1) + || rewrite mult_1_r + || rewrite setbit_high by + ( pose proof (Nat.pow_nonzero 2 n); specialize_by discriminate; + set (x := wordToNat (H b sk)); + assert (x mod 2 ^ n < 2^n)%nat by (apply Nat.mod_bound_pos; omega); omega) + ). + Qed. + + Definition sign (pk sk : word b) {mlen} (msg:word mlen) := + dlet sp := splitSecretPrngCurve sk in + dlet s := fst sp in + dlet p := snd sp in + dlet r := SRepDecModL (H _ (p ++ msg)) in + dlet R := SRepERepMul r ErepB in + dlet S := SRepAdd r (SRepMul (SRepDecModL (H _ (ERepEnc R ++ pk ++ msg))) s) in + ERepEnc R ++ SRepEnc S. + + Lemma to_nat_l_nonzero : Z.to_nat l <> 0. + Proof using n_le_bpb. + + intro Hx; change 0 with (Z.to_nat 0) in Hx. + destruct prm; rewrite Z2Nat.inj_iff in Hx; omega. + Qed. + + Lemma sign_correct (pk sk : word b) {mlen} (msg:word mlen) + : sign pk sk msg = EdDSA.sign pk sk msg. + Proof using Agroup Ahomom ERepEnc_correct ErepB_correct H0 Proper_ERepEnc Proper_SRepAdd Proper_SRepERepMul Proper_SRepEnc Proper_SRepMul SRepAdd_correct SRepDecModLShort_correct SRepDecModL_correct SRepERepMul_correct SRepEnc_correct SRepMul_correct. + cbv [sign EdDSA.sign Let_In]. + + let H := fresh "H" in + pose proof (splitSecretPrngCurve_correct sk) as H; + destruct (splitSecretPrngCurve sk); + destruct H as [curveKey_correct prngKey_correct]. + + repeat ( + reflexivity + || rewrite ERepEnc_correct + || rewrite SRepEnc_correct + || rewrite SRepDecModL_correct + || rewrite SRepERepMul_correct + || rewrite (F.of_nat_add (m:=l)) + || rewrite (F.of_nat_mul (m:=l)) + || rewrite SRepAdd_correct + || rewrite SRepMul_correct + || rewrite ErepB_correct + || rewrite <-prngKey_correct + || rewrite <-curveKey_correct + || eapply (f_equal2 (fun a b => a ++ b)) + || f_equiv + || rewrite <-(@scalarmult_mod_order _ _ _ _ _ _ _ _ B to_nat_l_nonzero EdDSA_l_order_B) + ). + Qed. + End ChangeRep. +End EdDSA. diff --git a/src/Primitives/MxDHRepChange.v b/src/Primitives/MxDHRepChange.v new file mode 100644 index 000000000..9f0276ef8 --- /dev/null +++ b/src/Primitives/MxDHRepChange.v @@ -0,0 +1,162 @@ +Require Import Crypto.Spec.MxDH. +Require Import Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.Ring Crypto.Algebra.Field. +Require Import Crypto.Util.Tuple Crypto.Util.Prod. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. + +Section MxDHRepChange. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {Fcswap:bool->F*F->F*F->(F*F)*(F*F)} {Fa24:F} {tb1:nat->bool}. + Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {impl_field:@Algebra.Hierarchy.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {Keq_dec:Decidable.DecidableRel Keq} {Kcswap:bool->K*K->K*K->(K*K)*(K*K)} {Ka24:K} {tb2:nat->bool}. + + Context {FtoK} {homom:@Ring.is_homomorphism F Feq Fone Fadd Fmul + K Keq Kone Kadd Kmul FtoK}. + Context {homomorphism_inv_zero:Keq (FtoK (Finv Fzero)) (Kinv Kzero)}. + Context {homomorphism_a24:Keq (FtoK Fa24) Ka24}. + Context {Fcswap_correct:forall b x y, Fcswap b x y = if b then (y,x) else (x,y)}. + Context {Kcswap_correct:forall b x y, Kcswap b x y = if b then (y,x) else (x,y)}. + Context {tb2_correct:forall i, tb2 i = tb1 i}. + + (* TODO: move to algebra *) + Lemma homomorphism_multiplicative_inverse_complete' x : Keq (FtoK (Finv x)) (Kinv (FtoK x)). + Proof using Feq_dec Keq_dec field homom homomorphism_inv_zero impl_field. + eapply (homomorphism_multiplicative_inverse_complete). + intro J; rewrite J. rewrite homomorphism_inv_zero, homomorphism_id. + reflexivity. + Qed. + + Ltac t := + let hom := match goal with H : is_homomorphism |- _ => H end in + let mhom := constr:(@homomorphism_is_homomorphism _ _ _ _ _ _ _ _ _ _ _ hom) in + repeat ( + rewrite (@homomorphism_id _ _ _ _ _ _ _ _ _ _ _ _ _ mhom) || + rewrite (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ hom) || + rewrite (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ hom) || + rewrite (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ hom) || + rewrite (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ hom) || + rewrite homomorphism_a24 || + rewrite homomorphism_multiplicative_inverse_complete' || + reflexivity + ). + + (*Import Crypto.Util.Tactics.*) + Import List. + Import Coq.Classes.Morphisms. + + Global Instance Proper_ladderstep : + Proper (Keq ==> (fieldwise (n:=2) Keq) ==> fieldwise (n:=2) Keq ==> fieldwise (n:=2) (fieldwise (n:=2) Keq)) (@MxDH.ladderstep K Kadd Ksub Kmul Ka24). + Proof using Keq_dec impl_field. + cbv [MxDH.ladderstep tuple tuple' fieldwise fieldwise' fst snd]; + repeat intro; destruct_head' prod; destruct_head' and; repeat split; + repeat match goal with [H:Keq ?x ?y |- _ ] => rewrite !H; clear H x end; reflexivity. + Qed. + + Lemma MxLadderstepRepChange u P Q Ku (Ku_correct:Keq (FtoK u) Ku): + fieldwise (n:=2) (fieldwise (n:=2) Keq) + ((Tuple.map (n:=2) (Tuple.map (n:=2) FtoK)) (@MxDH.ladderstep F Fadd Fsub Fmul Fa24 u P Q)) + (@MxDH.ladderstep K Kadd Ksub Kmul Ka24 Ku (Tuple.map (n:=2) FtoK P) (Tuple.map (n:=2) FtoK Q)). + Proof using Feq_dec Keq_dec field homom homomorphism_a24 impl_field. + destruct P as [? ?], Q as [? ?]; cbv; repeat split; rewrite <-?Ku_correct; t. + Qed. + + Let loopiter_sig F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u : + { loopiter | @MxDH.montladder F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u = + let '(_, _, _) := MxDH.downto _ _ loopiter in _ } := exist _ _ eq_refl. + Let loopiter F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u := + Eval cbv [proj1_sig loopiter_sig] in ( + proj1_sig (loopiter_sig F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u)). + + Let loopiter_phi s : ((K * K) * (K * K)) * bool := + (Tuple.map (n:=2) (Tuple.map (n:=2) FtoK) (fst s), snd s). + + Let loopiter_eq (a b: (((K * K) * (K * K)) * bool)) := + fieldwise (n:=2) (fieldwise (n:=2) Keq) (fst a) (fst b) /\ snd a = snd b. + + Local Instance Equivalence_loopiter_eq : Equivalence loopiter_eq. + Proof using Keq_dec impl_field loopiter_phi. + unfold loopiter_eq; split; repeat intro; + intuition (reflexivity||symmetry;eauto||etransitivity;symmetry;eauto). + Qed. + + Lemma MxLoopIterRepChange b Fu s i Ku (HKu:Keq (FtoK Fu) Ku) : loopiter_eq + (loopiter_phi (loopiter F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb1 Fu s i)) + (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap b tb2 Ku (loopiter_phi s) i). + Proof using Fcswap_correct Feq_dec Kcswap_correct Keq_dec field homom homomorphism_a24 impl_field tb2_correct. + destruct_head' prod; break_match. + simpl. + rewrite !Fcswap_correct, !Kcswap_correct, tb2_correct in *. + break_match; cbv [loopiter_eq loopiter_phi fst snd]; split; try reflexivity; + (etransitivity;[|etransitivity]; [ | eapply (MxLadderstepRepChange _ _ _ _ HKu) | ]; + match goal with Heqp:_ |- _ => rewrite <-Heqp; reflexivity end). + Qed. + + Global Instance Proper_fold_left {A RA B RB} : + Proper ((RA==>RB==>RA) ==> SetoidList.eqlistA RB ==> RA ==> RA) (@fold_left A B). + Proof using Type. + intros ? ? ? ? ? Hl; induction Hl; repeat intro; [assumption|]. + simpl; cbv [Proper respectful] in *; eauto. + Qed. + + Lemma proj_fold_left {A B L} R {Equivalence_R:@Equivalence B R} (proj:A->B) step step' {Proper_step':(R ==> eq ==> R)%signature step' step'} (xs:list L) init init' (H0:R (proj init) init') (Hproj:forall x i, R (proj (step x i)) (step' (proj x) i)) : + R (proj (fold_left step xs init)) (fold_left step' xs init'). + Proof using Type. + generalize dependent init; generalize dependent init'. + induction xs; [solve [eauto]|]. + repeat intro; simpl; rewrite IHxs by eauto. + apply (_ : Proper ((R ==> eq ==> R) ==> SetoidList.eqlistA eq ==> R ==> R) (@fold_left _ _)); + try reflexivity; + eapply Proper_step'; eauto. + Qed. + + Global Instance Proper_downto {T R} {Equivalence_R:@Equivalence T R} : + Proper (R ==> Logic.eq ==> (R==>Logic.eq==>R) ==> R) MxDH.downto. + Proof using Type. + intros s0 s0' Hs0 n' n Hn'; subst n'; generalize dependent s0; generalize dependent s0'. + induction n; repeat intro; [assumption|]. + unfold MxDH.downto; simpl. + eapply Proper_fold_left; try eassumption; try reflexivity. + cbv [Proper respectful] in *; eauto. + Qed. + + Global Instance Proper_loopiter a b c : + Proper (loopiter_eq ==> eq ==> loopiter_eq) (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap a b c). + Proof using Kcswap_correct Keq_dec impl_field. + unfold loopiter; intros [? ?] [? ?] [[[] []] ?]; repeat intro ; cbv [fst snd] in * |-; subst. + repeat (break_match; break_match_hyps). + split; [|reflexivity]. + etransitivity; [|etransitivity]; [ | eapply Proper_ladderstep | ]; + [eapply eq_subrelation; [ exact _ | symmetry; eassumption ] + | reflexivity | | + | eapply eq_subrelation; [exact _ | eassumption ] ]; + rewrite !Kcswap_correct in *; + match goal with [H: (if ?b then _ else _) = _ |- _] => destruct b end; + destruct_head prod; inversion_prod; subst; eauto. + Qed. + + Lemma MxDHRepChange b (x:F) : + Keq + (FtoK (@MxDH.montladder F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb1 x)) + (@MxDH.montladder K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap b tb2 (FtoK x)). + Proof using Fcswap_correct Feq_dec Kcswap_correct Keq_dec field homom homomorphism_a24 homomorphism_inv_zero impl_field tb2_correct. + cbv [MxDH.montladder]. + repeat break_match. + assert (Hrel:loopiter_eq (loopiter_phi (p, p0, b0)) (p1, p3, b1)). + { + rewrite <-Heqp0; rewrite <-Heqp. + unfold MxDH.downto. + eapply (proj_fold_left (L:=nat) loopiter_eq loopiter_phi). + { eapply @Proper_loopiter. } + { cbv; repeat split; t. } + { intros; eapply MxLoopIterRepChange; reflexivity. } + } + { destruct_head' prod; destruct Hrel as [[[] []] ?]; simpl in *; subst. + rewrite !Fcswap_correct, !Kcswap_correct in *. + match goal with [H: (if ?b then _ else _) = _ |- _] => destruct b end; + destruct_head prod; inversion_prod; subst; + repeat match goal with [H: Keq (FtoK ?x) (?kx)|- _ ] => rewrite <- H end; + t. + } + Grab Existential Variables. + exact 0. + exact 0. + Qed. +End MxDHRepChange. -- cgit v1.2.3