1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
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.
|
