From 5357fe92e65712a3e2506fe0a939b358d14183d7 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 21 Sep 2016 20:45:01 -0400 Subject: alternative signing derivation cleanup --- src/Experiments/EdDSARefinement.v | 122 +++++++++++++++++++--- src/ModularArithmetic/ModularArithmeticTheorems.v | 8 ++ src/Spec/EdDSA.v | 3 +- src/Util/LetIn.v | 8 +- src/Util/Relations.v | 5 + 5 files changed, 128 insertions(+), 18 deletions(-) diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v index afdf24604..48845b08e 100644 --- a/src/Experiments/EdDSARefinement.v +++ b/src/Experiments/EdDSARefinement.v @@ -5,13 +5,10 @@ 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.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Util.LetIn. Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems. -Module Import NotationsFor8485. - Import NPeano Nat. - Infix "mod" := modulo. -End NotationsFor8485. +Import Notations. Section EdDSA. Context `{prm:EdDSA}. @@ -55,7 +52,7 @@ Section EdDSA. 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)), + 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. @@ -91,11 +88,11 @@ Section EdDSA. 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. + 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 {Erep ErepEq ErepAdd ErepId ErepOpp} {Agroup:@group Erep ErepEq ErepAdd ErepId ErepOpp}. @@ -121,12 +118,12 @@ Section EdDSA. Definition verify_using_representation {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) - : { answer | answer = verify message pk sig }. + : { answer | answer = verify' message pk sig }. Proof. + eexists. pose proof EdDSA_l_odd. assert (l_pos:(0 < l)%Z) by omega. - eexists. - cbv [verify]. + cbv [verify']. etransitivity. Focus 2. { eapply Proper_option_rect_nd_changebody; [intro|reflexivity]. @@ -184,5 +181,102 @@ Section EdDSA. 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. + 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 {wbRepKeepLow wbRepClearLow wbRepClearBit wbRepSetBit:nat->word b->word b}. + Context {wbRepSetBit_correct : forall n x, wordToNat (wbRepSetBit n x) = setbit (wordToNat x) n}. + Context {wbRepClearLow_correct : forall c x, wordToNat (wbRepClearLow c x) = wordToNat x - wordToNat x mod 2 ^ c}. + Context {wbRepKeepLow_correct : forall n x, wordToNat (wbRepKeepLow n x) = (wordToNat x) mod (2^n)}. + Context {SRepDecModLShort} {SRepDecModLShort_correct: forall (w:word b), 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: *) + + Definition splitSecretPrngCurve (sk:word b) : SRep * word b := + dlet hsk := H _ sk in + dlet curveKey := SRepDecModLShort (wbRepSetBit n (wbRepClearLow c (wbRepKeepLow n (split1 b b hsk)))) in + dlet prngKey := split2 b b hsk in + (curveKey, prngKey). + + (* TODO: prove these, somewhere *) + Axiom wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a). + Axiom wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a). + Axiom nat_mod_smaller_power_of_two : forall n b:nat, + (n <= b -> forall x:nat, (x mod 2 ^ b) mod 2 ^ n = (x mod 2^n))%nat. + + 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. + cbv [splitSecretPrngCurve EdDSA.curveKey EdDSA.prngKey Let_In]; split; + repeat ( + reflexivity + || rewrite <-SRepDecModLShort_correct + || rewrite wbRepSetBit_correct + || rewrite wbRepClearLow_correct + || rewrite wbRepKeepLow_correct + || rewrite wordToNat_split1 + || rewrite wordToNat_wfirstn + || rewrite nat_mod_smaller_power_of_two by (destruct prm; 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 sign_correct (pk sk : word b) {mlen} (msg:word mlen) + : sign pk sk msg = EdDSA.sign pk sk msg. + Proof. + 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 + ). + Qed. End ChangeRep. End EdDSA. diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 5984b4e6d..f1a2d15a4 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -173,6 +173,14 @@ Module F. rewrite Z2Nat.id by omega. rewrite <-F.of_Z_mod; reflexivity. Qed. + + Lemma of_nat_add x y : + F.of_nat m (x + y) = (F.of_nat m x + F.of_nat m y)%F. + Proof. unfold F.of_nat; rewrite Nat2Z.inj_add, F.of_Z_add; reflexivity. Qed. + + Lemma of_nat_mul x y : + F.of_nat m (x * y) = (F.of_nat m x * F.of_nat m y)%F. + Proof. unfold F.of_nat; rewrite Nat2Z.inj_mul, F.of_Z_mul; reflexivity. Qed. End FandNat. Section RingTacticGadgets. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 2971bfef8..f8581c4c9 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -21,6 +21,7 @@ Module Import Notations. Infix "^" := pow. Infix "mod" := modulo (at level 40, no associativity). Infix "++" := Word.combine. + Notation setbit := setbit. End Notations. Generalizable All Variables. @@ -73,7 +74,7 @@ Section EdDSA. Program Definition curveKey (sk:secretkey) : nat := let x := wfirstn n (H sk) in (* hash the key, use first "half" for secret scalar *) let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *) - x + 2^n. (* and the high bit is always set *) + setbit x n. (* and the high bit is always set *) Local Infix "+" := Eadd. Local Infix "*" := EscalarMult. diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v index a472f4090..80310b833 100644 --- a/src/Util/LetIn.v +++ b/src/Util/LetIn.v @@ -14,9 +14,11 @@ Global Instance Proper_Let_In_nd_changevalue {A B} (RA:relation A) {RB:relation : Proper (RA ==> (RA ==> RB) ==> RB) (Let_In (P:=fun _=>B)). Proof. cbv; intuition. Qed. -Lemma app_Let_In_nd {A B C} (f:B -> C) : forall (e:A) (C:A -> B), - f (Let_In e C) = Let_In e (fun v => f (C v)). -Proof. cbv; intuition. Qed. +Definition app_Let_In_nd {A B T} (f:B->T) (e:A) (C:A->B) + : f (Let_In e C) = Let_In e (fun v => f (C v)) := eq_refl. + +Definition Let_app_In_nd {A B T} (f:A->B) (e:A) (C:B->T) + : Let_In (f e) C = Let_In e (fun v => C (f v)) := eq_refl. Class _call_let_in_to_Let_In {T} (e:T) := _let_in_to_Let_In_return : T. (* : forall T, gallina T -> gallina T, structurally recursive in the argument *) diff --git a/src/Util/Relations.v b/src/Util/Relations.v index aa280db26..4612fa8a8 100644 --- a/src/Util/Relations.v +++ b/src/Util/Relations.v @@ -27,3 +27,8 @@ Proof. logic; try match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end. repeat (assumption||reflexivity||econstructor); assumption. (* WHY the last [assumption]?*) 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. \ No newline at end of file -- cgit v1.2.3