diff options
-rw-r--r-- | src/Experiments/Ed25519.v | 12 | ||||
-rw-r--r-- | src/Util/IterAssocOp.v | 58 | ||||
-rw-r--r-- | src/Util/Relations.v | 16 |
3 files changed, 84 insertions, 2 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 090644756..3c2c0baf8 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -661,7 +661,17 @@ Qed. Let SRepEnc : SRep -> Word.word b := (fun x => Word.NToWord _ (Z.to_N x)). -Axiom Proper_SRepERepMul : Proper (SC25519.SRepEq ==> ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519) ==> ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519)) SRepERepMul. +Local Instance Proper_SRepERepMul : Proper (SC25519.SRepEq ==> ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519) ==> ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519)) SRepERepMul. + unfold SRepERepMul, SC25519.SRepEq. + repeat intro. + eapply IterAssocOp.Proper_iter_op. + { eapply ExtendedCoordinates.Extended.Proper_add. } + { reflexivity. } + { repeat intro; subst; reflexivity. } + { unfold ERepSel; repeat intro; break_match; solve [ discriminate | eauto ]. } + { reflexivity. } + { assumption. } +Qed. Lemma SRepEnc_correct : forall x : ModularArithmetic.F.F l, Senc x = SRepEnc (S2Rep x). unfold SRepEnc, Senc, Fencode; intros; f_equal. diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index e520ca9f9..773fea8fd 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -191,4 +191,60 @@ Section IterAssocOp. rewrite Nshiftr_size by auto. reflexivity. Qed. -End IterAssocOp.
\ No newline at end of file +End IterAssocOp. + +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Relations. + +Global Instance Proper_funexp {T R} {Equivalence_R:Equivalence R} + : Proper ((R==>R) ==> R ==> Logic.eq ==> R) (@funexp T). +Proof. + repeat intro; subst. + match goal with [n0 : nat |- _ ] => rename n0 into n; induction n end; [solve [trivial]|]. + match goal with + [H: (_ ==> _)%signature _ _ |- _ ] => + etransitivity; solve [eapply (H _ _ IHn)|reflexivity] + end. +Qed. + +Global Instance Proper_test_and_op {T R} {Equivalence_R:@Equivalence T R} : + Proper ((R==>R==>R) + ==> pointwise_relation _ Logic.eq + ==> (Logic.eq==>R==>R==>R) + ==> R + ==> (fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)) + ==> (fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)) + ) (@test_and_op T). +Proof. + repeat match goal with + | _ => intro + | _ => split + | [p:prod _ _ |- _ ] => destruct p + | [p:and _ _ |- _ ] => destruct p + | _ => progress (cbv [fst snd test_and_op pointwise_relation respectful] in * ) + | _ => progress subst + | _ => progress break_match + | _ => solve [ congruence | eauto 99 ] + end. +Qed. + +Global Instance Proper_iter_op {T R} {Equivalence_R:@Equivalence T R} : + Proper ((R==>R==>R) + ==> R + ==> pointwise_relation _ Logic.eq + ==> (Logic.eq==>R==>R==>R) + ==> Logic.eq + ==> R + ==> R) + (@iter_op T). +Proof. + repeat match goal with + | _ => solve [ reflexivity | congruence | eauto 99 ] + | _ => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)))) + | _ => progress eapply Proper_test_and_op + | _ => progress eapply conj + | _ => progress (cbv [fst snd pointwise_relation respectful] in * ) + | _ => intro + end. +Qed.
\ No newline at end of file diff --git a/src/Util/Relations.v b/src/Util/Relations.v index 4612fa8a8..4926bd74c 100644 --- a/src/Util/Relations.v +++ b/src/Util/Relations.v @@ -31,4 +31,20 @@ Qed. Lemma iff_R_R_same_r {T R} {Req:@Equivalence T R} x y ref : R x y -> (R x ref <-> R y ref). Proof. intro Hx; rewrite Hx; clear Hx. reflexivity. +Qed. + +Global Instance Equivalence_and {A B RA RB} + {Equivalence_RA:@Equivalence A RA} + {Equivalence_RB:@Equivalence B RB} + : Equivalence (fun ab AB => RA (fst ab) (fst AB) /\ RB (snd ab) (snd AB)). +Proof. + destruct Equivalence_RA as [], Equivalence_RB as []; cbv in *|-. + repeat match goal with + | _ => intro + | _ => split + | [p:prod _ _ |- _ ] => destruct p + | [p:and _ _ |- _ ] => destruct p + | _ => progress (cbv [fst snd] in * ) + | _ => solve[eauto] + end. Qed.
\ No newline at end of file |