rename-everything

2 files changed, 470 insertions, 0 deletions

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: <https://github.com/mit-plv/fiat-crypto/issues/64> *)
+
+    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.