Skip to content

Commit

Permalink
Derive EdDSA.verify from equational specification
Browse files Browse the repository at this point in the history 
Experiments/SpecEd25519 will come back soon
  • Loading branch information
@andres-erbsen
andres-erbsen committed Sep 16, 2016
1 parent 7d139de commit 1ea69cd
Show file tree
Hide file tree
Showing 9 changed files with 254 additions and 272 deletions.
4 changes: 2 additions & 2 deletions _CoqProject
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,6 @@ src/Encoding/PointEncodingPre.v
src/Experiments/DerivationsOptionRectLetInEncoding.v
src/Experiments/EdDSARefinement.v
src/Experiments/GenericFieldPow.v
src/Experiments/SpecEd25519.v
src/Experiments/SpecificCurve25519.v
src/ModularArithmetic/ExtPow2BaseMulProofs.v
src/ModularArithmetic/ExtendedBaseVector.v
src/ModularArithmetic/ModularArithmeticTheorems.v
Expand Down Expand Up @@ -102,12 +100,14 @@ src/Util/HProp.v
src/Util/Isomorphism.v
src/Util/IterAssocOp.v
src/Util/ListUtil.v
src/Util/Logic.v
src/Util/NatUtil.v
src/Util/Notations.v
src/Util/NumTheoryUtil.v
src/Util/Option.v
src/Util/PointedProp.v
src/Util/Prod.v
src/Util/Relations.v
src/Util/Sigma.v
src/Util/Sum.v
src/Util/Tactics.v
Expand Down
244 changes: 151 additions & 93 deletions src/Experiments/EdDSARefinement.v
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,12 @@
Require Import Crypto.Util.FixCoqMistakes.
Require Import Crypto.Spec.EdDSA Bedrock.Word.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions.
Require Import Crypto.Algebra. Import Group ScalarMult.
Require Import Crypto.Util.Decidable Crypto.Util.Option Crypto.Util.Tactics.
Require Import Coq.omega.Omega.
Require Import Crypto.Util.Notations.
Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil.
Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems.

Module Import NotationsFor8485.
Import NPeano Nat.
Expand All @@ -12,118 +15,173 @@ End NotationsFor8485.

Section EdDSA.
Context `{prm:EdDSA}.
Context {eq_dec:DecidableRel Eeq}.
Local Infix "==" := Eeq.
Local Notation valid := (@valid E Eeq Eadd EscalarMult b H l B Eenc Senc).
Local Infix "*" := EscalarMult. Local Infix "+" := Eadd. Local Infix "++" := combine.
Local Notation "P - Q" := (P + Eopp Q).
Local Arguments H {_} _.

Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}.
Context {Proper_Eopp : Proper (Eeq==>Eeq) Eopp}.
Context {Proper_Eadd : Proper (Eeq==>Eeq==>Eeq) Eadd}.

Context {decE:word b-> option E}.
Context {decS:word b-> option nat}.

Context {decE_canonical: forall x s, decE x = Some s -> x = Eenc s }.
Context {decS_canonical: forall x s, decS x = Some s -> x = Senc s }.

Context {decS_Senc: forall x, decS (Senc x) = Some x}.
Context {decE_Eenc: forall x, decE (Eenc x) = Some x}. (* FIXME: equivalence relation *)

Lemma solve_for_R : forall s B R n A, s * B == R + n * A <-> R == s*B - n*A.
Proof.
intros; split;
intro Heq; rewrite Heq; clear Heq.
{ rewrite <-associative, right_inverse, right_identity; reflexivity. }
{ rewrite <-associative, left_inverse, right_identity; reflexivity. }
Qed.
Local Infix "==" := Eeq. Local Infix "+" := Eadd. Local Infix "*" := EscalarMult.

Definition verify {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool :=
option_rect (fun _ => bool) (fun S : nat =>
option_rect (fun _ => bool) (fun A : E =>
weqb
(split1 b b sig)
(Eenc (S * B - (wordToNat (H (split1 b b sig ++ pk ++ message))) mod l * A))
) false (decE pk)
) false (decS (split2 b b sig))
.

Lemma verify_correct mlen (message:word mlen) (pk:word b) (sig:word (b+b)) :
verify message pk sig = true <-> valid message pk sig.
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.
cbv [verify option_rect option_map].
split.
{
cbv [sign public Spec.EdDSA.valid]; intros; subst;
repeat match goal with
| |- false = true -> _ => let H:=fresh "H" in intro H; discriminate H
| [H: _ |- _ ] => apply decS_canonical in H
| [H: _ |- _ ] => apply decE_canonical in H
| _ => rewrite weqb_true_iff
| _ => break_match
| |- exists _, _ => eexists
| |- _ /\ _ => eapply conj
| |- _ => reflexivity
end.
intro.
subst.
rewrite <-combine_split.
rewrite Heqo.
rewrite H0.
constructor.
rewrite <-H0.
rewrite solve_for_R.
reflexivity.
}
{
intros [? ? ? ? Hvalid].
rewrite solve_for_R in Hvalid.
rewrite split1_combine.
rewrite split2_combine.
rewrite decS_Senc.
rewrite decE_Eenc.
rewrite weqb_true_iff.
f_equiv. exact Hvalid.
}
Qed.

Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M).
Proof.
cbv [sign public]. intros. subst. split.
rewrite scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, NPeano.Nat.mul_comm, scalarmult_assoc;
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
| pose proof EdDSA_l_odd; omega
| 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. intros ? ? Hx; rewrite Hx; reflexivity. Qed.

Context {Edec:word b-> option E} {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> 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.
repeat setoid_rewrite <-option_rect_false_returns_true_iff.

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. exact (proj2_sig verify_sig). Qed.

Section ChangeRep.
Context {A Aeq Aadd Aid Aopp} {Agroup:@group A Aeq Aadd Aid Aopp}.
Context {EtoA} {Ahomom:@is_homomorphism E Eeq Eadd A Aeq Aadd EtoA}.
Context {Erep ErepEq ErepAdd ErepId ErepOpp} {Agroup:@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 {Aenc : A -> word b} {Proper_Aenc:Proper (Aeq==>Logic.eq) Aenc}
{Aenc_correct : forall P:E, Eenc P = Aenc (EtoA P)}.
Context {ERepDec : word b -> option Erep}
{ERepDec_correct : forall w, ERepDec w = option_map EToRep (Edec w) }.

Context {S Seq} `{@Equivalence S Seq} {natToS:nat->S}
{SAmul:S->A->A} {Proper_SAmul: Proper (Seq==>Aeq==>Aeq) SAmul}
{SAmul_correct: forall n P, Aeq (EtoA (n*P)) (SAmul (natToS n) (EtoA P))}
{SdecS} {SdecS_correct : forall w, (decS w) = (SdecS w)} (* FIXME: equivalence relation *)
{natToS_modl : forall n, Seq (natToS (n mod l)) (natToS n)}.
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*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.
pose proof EdDSA_l_odd.
assert (l_pos:(0 < l)%Z) by omega.
eexists.
cbv [verify].
repeat (
setoid_rewrite Aenc_correct
|| setoid_rewrite homomorphism
|| setoid_rewrite homomorphism_id
|| setoid_rewrite (homomorphism_inv(INV:=Eopp)(inv:=Aopp)(eq:=Aeq)(phi:=EtoA))
|| setoid_rewrite SAmul_correct
|| setoid_rewrite SdecS_correct
|| setoid_rewrite natToS_modl
).

etransitivity. Focus 2. {
eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
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 _ l_pos _)
|| rewrite (@F.of_nat_mod _ l_pos _)
).
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 <-(ERepDec_correct pk).

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.
End ChangeRep.
Expand Down

0 comments on commit 1ea69cd

Please sign in to comment.