diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | src/Assembly/#QhasmExtraction.v# | 24 | ||||
| l--------- | src/Assembly/.#QhasmExtraction.v | 1 | ||||
| -rw-r--r-- | src/Assembly/HighLevel.v | 9 | ||||
| -rw-r--r-- | src/Assembly/Qhasm.v | 102 | ||||
| -rw-r--r-- | src/Assembly/QhasmExtraction.v | 25 | ||||
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 5 | ||||
| -rw-r--r-- | src/Spec/EdDSA.v | 3 | ||||
| -rw-r--r-- | src/Specific/Ed25519.v | 39 |
9 files changed, 196 insertions, 13 deletions
diff --git a/.gitignore b/.gitignore index 423261343..6caadcb20 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,7 @@ bedrock fiat *~ +*# *.vo *.d *.glob diff --git a/src/Assembly/#QhasmExtraction.v# b/src/Assembly/#QhasmExtraction.v# new file mode 100644 index 000000000..0584553fc --- /dev/null +++ b/src/Assembly/#QhasmExtraction.v# @@ -0,0 +1,24 @@ + + +(* +- Define an evaluation function over the QH type, which can be terribly inefficient. This function will be parametrized in the following way: + + evalReg x InputRegs OutputRegs + evalStack x InputStack OutputStack + +Then, produce a lemma which shows that evaluating a given QH will perform an appropriate register operation. This will not check side-effects, which should be okay since we’re synthesizing in a very controlled manner. + +- Work on {x: QH | eval x _ _ = AST}, like the bounding code + +- Introduce all Inputs as StackX + +- Replace upward as: + + + Lifted functions by lemma (as above) + + Conditionals as QCond, by lemma + +- Then we can convert to string: + + + We can introduce stack inputs, etc. by traversing the AST + + QSeq, QStatement, QAssign are convertible directly + + QCond, QWhile are fixed assembly wrappers *)
\ No newline at end of file diff --git a/src/Assembly/.#QhasmExtraction.v b/src/Assembly/.#QhasmExtraction.v new file mode 120000 index 000000000..74379fe2d --- /dev/null +++ b/src/Assembly/.#QhasmExtraction.v @@ -0,0 +1 @@ +varomodt@dhcp-18-189-8-224.dyn.MIT.EDU.19197
\ No newline at end of file diff --git a/src/Assembly/HighLevel.v b/src/Assembly/HighLevel.v new file mode 100644 index 000000000..bae67f312 --- /dev/null +++ b/src/Assembly/HighLevel.v @@ -0,0 +1,9 @@ + +Inductive Const32 : Set = | const32: word 32 -> Const32. + +Inductive HL := + | Input: Const32 -> HL + | Variable: Const32 -> HL + | Let: forall m, nat -> HL -> HL -> HL + | Lift1: (Const32 -> Const32) -> HL -> HL + | Lift2: (Const32 -> Const32 -> Const32) -> HL -> HL -> HL. diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v new file mode 100644 index 000000000..f30d10e94 --- /dev/null +++ b/src/Assembly/Qhasm.v @@ -0,0 +1,102 @@ + +Require Import String. + +Inductive Const32 : Set = | const32: word 32 -> Const32. + +Inductive Reg (len: nat) : Set = + | reg32: string -> Reg 32 + | reg3232: string -> Reg 64 + | reg6464: string -> Reg 128 + | float80: string -> Reg 80. + +Inductive Stack (len: nat) : Set = + | stack32: string -> Stack 32. + | stack64: string -> Stack 64. + | stack128: string -> Stack 128. + +Definition Index (limit: nat) := {x: nat | x < limit}. + +Inductive Assignment : Set := + | Assign32Stack32: Reg 32 -> Stack32 -> Assignment + | Assign32Stack16: Reg 32 -> Stack32 -> Index 2 -> Assignment + | Assign32Stack8: Reg 32 -> Stack32 -> Index 4 -> Assignment + | Assign32Stack64: Reg 32 -> Stack64 -> Index 2 -> Assignment + | Assign32Stack128: Reg 32 -> Stack128 -> Index 2 -> Assignment + + | Assign32Reg32: Reg 32 -> Reg 32 -> Assignment + | Assign32Reg16: Reg 32 -> Reg 32 -> Index 2 -> Assignment + | Assign32Reg8: Reg 32 -> Reg 32 -> Index 4 -> Assignment + | Assign32Reg64: Reg 32 -> Reg64 -> Index 2 -> Assignment + | Assign32Reg128: Reg 32 -> Reg 128 -> Index 4 -> Assignment + + | Assign3232Stack32: Reg 64 -> Index 2 -> Stack32 -> Assignment + | Assign3232Stack64: Reg 64 -> Stack64 -> Assignment + | Assign3232Stack128: Reg 64 -> Stack128 -> Index 2 -> Assignment + + | Assign3232Reg32: Reg 64 -> Index 2 -> Reg 32 -> Assignment + | Assign3232Reg64: Reg 64 -> Reg64 -> Assignment + | Assign3232Reg128: Reg 64 -> Reg 128 -> M 2 -> Assignment + + | AssignConstant: Reg 32 -> Const32 -> Assignment + | AssignPtr: Reg 32 -> Stack64. + +Hint Constructors Assignment. + +Inductive BinOp := + | Plus: BinOp | Minus: BinOp | Mult: BinOp + | Div: BinOp | Xor: BinOp | And: BinOp. + +Inductive RotOp := + | Shl: NatOp | Shr: NatOp | Rotl: NatOp | Rotr: NatOp. + +Inductive Operation := + | OpReg32Constant: BinOp -> Reg 32 -> Const32 -> Operation + | OpReg32Reg32: BinOp -> Reg 32 -> Reg 32 -> Operation + | RotReg32: RotOp -> Reg 32 -> Index 32 -> Operation + + | OpReg64Constant: BinOp -> Reg 32 -> Const32 -> Operation + | OpReg64Reg64: BinOp -> Reg 64 -> Reg 64 -> Operation + + | OpReg128Constant: BinOp -> Reg 128 -> Const32 -> Operation + | OpReg128Reg128: BinOp -> Reg 128 -> Reg 128 -> Operation. + +Hint Constructors Operation. + +Inductive TestOp := + | Eq: TestOp + | Lt: TestOp + | UnsignedLt: TestOp + | Gt: TestOp + | UnsignedGt: TestOp. + +Definition Invert := bool. + +Definition Conditional := + | TestReg32Reg32: TestOp -> Invert -> Reg 32 -> Reg 32 -> Conditional + | TestReg32Const: TestOp -> Invert -> Reg 32 -> W -> Conditional. + +Hint Constructors Conditional. + +Definition Label := nat. + +Inductive AlmostQhasm := + | QSeq: AlmostQhasm -> AlmostQhasm -> AlmostQhasm + | QAssign: Assignment -> AlmostQhasm + | QOp: Operation -> AlmostQhasm + | QCond: Conditional -> AlmostQhasm -> AlmostQhasm -> AlmostQhasm + | QWhile: Conditional -> AlmostQhasm -> AlmostQhasm + +Hint Constructors AlmostQhasm. + +Inductive Qhasm := + | QSeq: Qhasm -> Qhasm -> Qhasm + | QAssign: Assignment -> Qhasm + | QOp: Operation -> Qhasm + | QCond: Conditional -> Qhasm -> Qhasm -> Qhasm + | QWhile: Conditional -> Qhasm -> Qhasm + +Hint Constructors Qhasm. + +(* evalReg: Qhasm -> Reg 32 -> Reg 32 + evalStack: Qhasm -> Stack32 -> Stack32 *) + diff --git a/src/Assembly/QhasmExtraction.v b/src/Assembly/QhasmExtraction.v new file mode 100644 index 000000000..d773bbc65 --- /dev/null +++ b/src/Assembly/QhasmExtraction.v @@ -0,0 +1,25 @@ + + + +(* +- Define an evaluation function over the QH type, which can be terribly inefficient. This function will be parametrized in the following way: + + evalReg x InputRegs OutputRegs + evalStack x InputStack OutputStack + +Then, produce a lemma which shows that evaluating a given QH will perform an appropriate register operation. This will not check side-effects, which should be okay since we’re synthesizing in a very controlled manner. + +- Work on {x: QH | eval x _ _ = AST}, like the bounding code + +- Introduce all Inputs as StackX + +- Replace upward as: + + + Lifted functions by lemma (as above) + + Conditionals as QCond, by lemma + +- Then we can convert to string: + + + We can introduce stack inputs, etc. by traversing the AST + + QSeq, QStatement, QAssign are convertible directly + + QCond, QWhile are fixed assembly wrappers *)
\ No newline at end of file diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 8dbfdf7b9..b7d2c0d8e 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -46,8 +46,11 @@ Section TwistedEdwardsCurves. | O => zero | S n' => unifiedAdd P (scalarMult n' P) end. + + Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. End TwistedEdwardsCurves. Delimit Scope E_scope with E. Infix "+" := unifiedAdd : E_scope. -Infix "*" := scalarMult : E_scope.
\ No newline at end of file +Infix "*" := scalarMult : E_scope. +Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 6f57d7bec..c9660bd98 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -14,6 +14,7 @@ Infix "mod" := NPeano.modulo. Infix "++" := Word.combine. Section EdDSAParams. + Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *) E : TwistedEdwardsParams; (* underlying elliptic curve *) @@ -70,8 +71,6 @@ Section EdDSA. (r + H (enc R ++ public sk ++ M) * s)) in enc R ++ enc S. - Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. - Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. Definition verify (A_:publickey) {n:nat} (M : Word.word n) (sig:signature) : bool := let R_ := Word.split1 b b sig in let S_ := Word.split2 b b sig in diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 33c8398f7..efee4e7af 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -1,30 +1,49 @@ +Require Import Bedrock.Word. Require Import Crypto.Spec.Ed25519. Require Import Crypto.Tactics.VerdiTactics. Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic. -Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.ExtendedCoordinates. +Require Import Crypto.Spec.CompleteEdwardsCurve. +Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. +Require Import Crypto.Util.IterAssocOp. Local Infix "++" := Word.combine. Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40). Local Notation " a '[' i ':]' " := (Word.split2 i _ a) (at level 40). +Local Arguments H {_} _. +Local Arguments scalarMultM1 {_} {_} _ _. +Local Arguments unifiedAddM1 {_} {_} _ _. Lemma sharper_verify : { verify | forall pk l msg sig, verify pk l msg sig = ed25519_verify pk l msg sig}. Proof. eexists; intros. - cbv [ed25519_verify EdDSA.verify Encoding.dec EdDSA.PointEncoding PointEncoding - PointEncoding.point_encoding EdDSA.FlEncoding FlEncoding - Encoding.modular_word_encoding ed25519params]. - break_match. - break_match. - break_match. + cbv [ed25519_verify EdDSA.verify + ed25519params curve25519params + EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H + EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding]. + + (* zoom in to the interesting case *) + repeat match goal with |- context[match ?a with Some x => _ | _ => _ end] => + let n := fresh x in + let H := fresh "Heq" x in + destruct a as [x|] + end. + + let p1 := constr:(scalarMultM1_rep eq_refl) in + let p2 := constr:(unifiedAddM1_rep eq_refl) in repeat match goal with | |- context [(?n * ?P)%E] => rewrite <-(unExtendedPoint_mkExtendedPoint P); - erewrite <-scalarMultM1_rep + erewrite <-p1 | |- context [(?P + unExtendedPoint _)%E] => rewrite <-(unExtendedPoint_mkExtendedPoint P); - erewrite unifiedAddM1_rep + erewrite p2 end. rewrite !Znat.Z_nat_N, <-!Word.wordToN_nat. - (* unfold scalarMultM1 at 1. *) + cbv [scalarMultM1 iter_op]. + Local Arguments funexp {_} _ {_} {_}. (* do not display the initializer and iteration bound for now *) + cbv iota zeta delta [test_and_op]. + + Admitted.
\ No newline at end of file |