diff options
| -rw-r--r-- | src/Assembly/Evaluables.v | 3 | ||||
| -rw-r--r-- | src/Assembly/GF25519.v | 123 | ||||
| -rw-r--r-- | src/Assembly/Pipeline.v | 120 |
3 files changed, 178 insertions, 68 deletions
diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v index 8a8d10c7f..8d68ac696 100644 --- a/src/Assembly/Evaluables.v +++ b/src/Assembly/Evaluables.v @@ -707,8 +707,7 @@ Section RangeWithValue. ezero := None; toT := fun x => x; - fromT := fun x => omap x (fun x' => - if (checkRWV x') then x else None); + fromT := fun x => omap x (fun x' => if (checkRWV x') then x else None); eadd := fun x y => omap x (fun X => omap y (fun Y => rwv_app range_add_valid X Y)); diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index e1d10af78..2e6329f18 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -35,8 +35,24 @@ Module GF25519. exact t. Defined. - Definition liftFE {T} (F: @interp_type Z FE -> T) := - fun (a b c d e f g h i j: Z) => F (a, b, c, d, e, f, g, h, i, j). + Definition flatten {T}: (@interp_type Z FE -> T) -> NAry 10 Z T. + intro F; refine (fun (a b c d e f g h i j: Z) => + F (a, b, c, d, e, f, g, h, i, j)). + Defined. + + Definition unflatten {T}: + (forall a b c d e f g h i j, T (a, b, c, d, e, f, g, h, i, j)) + -> (forall x: @interp_type Z FE, T x). + Proof. + intro F; refine (fun (x: @interp_type Z FE) => + let '(a, b, c, d, e, f, g, h, i, j) := x in + F a b c d e f g h i j). + Defined. + + Ltac intro_vars_for R := revert R; + match goal with + | [ |- forall x, @?T x ] => apply (@unflatten T); intros + end. Module AddExpr <: Expression. Definition bits: nat := bits. @@ -51,15 +67,8 @@ Module GF25519. Definition ge25519_add' (P Q: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_add_expr P Q }. Proof. - vm_compute in P, Q; repeat - match goal with - | [x:?T |- _] => - lazymatch T with - | Z => fail - | prod _ _ => destruct x - | _ => clear x - end - end. + intro_vars_for P. + intro_vars_for Q. eexists. cbv beta delta [ge25519_add_expr]. @@ -78,9 +87,81 @@ Module GF25519. proj1_sig (ge25519_add' P Q). Definition hlProg: NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := - liftFE (fun p => (liftFE (fun q => ge25519_add p q))). + Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_add p q)))). End AddExpr. + Module SubExpr <: Expression. + Definition bits: nat := bits. + Definition inputs: nat := 20. + Definition width: Width bits := width. + Definition ResultType := FE. + Definition inputBounds := feBound ++ feBound. + + Definition ge25519_sub_expr := + Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in carry_sub. + + Definition ge25519_sub' (P Q: @interp_type Z FE) : + { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_sub_expr P Q }. + Proof. + intro_vars_for P. + intro_vars_for Q. + + eexists. + cbv beta delta [ge25519_sub_expr]. + + let R := HL.rhs_of_goal in + let X := HL.reify (@interp_type Z) R in + transitivity (HL.interp (t := ResultType) X); [reflexivity|]. + + cbv iota beta delta [ + interp_type interp_binop HL.interp + Z.land ZEvaluable eadd esub emul eshiftr eand]. + reflexivity. + Defined. + + Definition ge25519_sub (P Q: @interp_type Z ResultType) := + proj1_sig (ge25519_sub' P Q). + + Definition hlProg: NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := + Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_sub p q)))). + End SubExpr. + + Module MulExpr <: Expression. + Definition bits: nat := bits. + Definition inputs: nat := 20. + Definition width: Width bits := width. + Definition ResultType := FE. + Definition inputBounds := feBound ++ feBound. + + Definition ge25519_mul_expr := + Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in mul. + + Definition ge25519_mul' (P Q: @interp_type Z FE) : + { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_mul_expr P Q }. + Proof. + intro_vars_for P. + intro_vars_for Q. + + eexists. + cbv beta delta [ge25519_mul_expr]. + + let R := HL.rhs_of_goal in + let X := HL.reify (@interp_type Z) R in + transitivity (HL.interp (t := ResultType) X); [reflexivity|]. + + cbv iota beta delta [ + interp_type interp_binop HL.interp + Z.land ZEvaluable eadd esub emul eshiftr eand]. + reflexivity. + Defined. + + Definition ge25519_mul (P Q: @interp_type Z ResultType) := + proj1_sig (ge25519_mul' P Q). + + Definition hlProg: NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := + Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_mul p q)))). + End MulExpr. + Module OppExpr <: Expression. Definition bits: nat := bits. Definition inputs: nat := 10. @@ -95,15 +176,7 @@ Module GF25519. { r: @HL.expr Z (@interp_type Z) FE | HL.interp (E := @ZEvaluable bits) (t := FE) r = ge25519_opp_expr P }. Proof. - vm_compute in P; repeat - match goal with - | [x:?T |- _] => - lazymatch T with - | Z => fail - | prod _ _ => destruct x - | _ => clear x - end - end. + intro_vars_for P. eexists. cbv beta delta [ge25519_opp_expr zero_]. @@ -123,14 +196,16 @@ Module GF25519. proj1_sig (ge25519_opp' P). Definition hlProg: NAry 10 Z (@HL.expr Z (@interp_type Z) ResultType) := - liftFE (fun p => ge25519_opp p). + Eval cbv in (flatten (fun p => ge25519_opp p)). End OppExpr. Module Add := Pipeline AddExpr. + Module Sub := Pipeline SubExpr. + Module Mul := Pipeline MulExpr. Module Opp := Pipeline OppExpr. End GF25519. Extraction "GF25519Add" GF25519.Add. +Extraction "GF25519Sub" GF25519.Sub. +Extraction "GF25519Mul" GF25519.Mul. Extraction "GF25519Opp" GF25519.Opp. - -Eval cbv in GF25519.Add.outputBounds. diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index c1a24ab4c..53f4bdd56 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -26,70 +26,105 @@ Module Type Expression. End Expression. Module Pipeline (Input: Expression). - Export Input. + Definition bits := Input.bits. + Definition inputs := Input.inputs. + Definition ResultType := Input.ResultType. + + Hint Unfold bits inputs ResultType. + Definition width: Width bits := Input.width. + + Definition W: Type := word bits. + Definition R: Type := option RangeWithValue. + Definition B: Type := option (@BoundedWord bits). + + Instance ZEvaluable : Evaluable Z := @ZEvaluable bits. + Instance WEvaluable : Evaluable W := @WordEvaluable bits. + Instance REvaluable : Evaluable R := @RWVEvaluable bits. + Instance BEvaluable : Evaluable B := @BoundedEvaluable bits. + + Existing Instances ZEvaluable WEvaluable REvaluable BEvaluable. Module Util. - Fixpoint applyProgOn {A B k} ins (f: NAry k (option A) B): B := - match k as k' return NAry k' (option A) B -> B with + Fixpoint applyProgOn {A B k} (d: A) ins (f: NAry k A B): B := + match k as k' return NAry k' A B -> B with | O => id | S m => fun f' => match ins with - | cons x xs => @applyProgOn A B m xs (f' x) - | nil => @applyProgOn A B m nil (f' None) + | cons x xs => @applyProgOn A B m d xs (f' x) + | nil => @applyProgOn A B m d nil (f' d) end end f. End Util. - Definition hlProg': NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - liftN (HLConversions.mapVar (fun t => @LL.uninterp_arg_as_var _ _ t) - (fun t => @LL.interp_arg _ t)) hlProg. + Module HL. + Definition progZ: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType) := + liftN (HLConversions.mapVar + (fun t => @LL.uninterp_arg_as_var _ _ t) + (fun t => @LL.interp_arg _ t)) + Input.hlProg. - Definition llProg: NAry inputs Z (@LL.expr Z Z ResultType) := - liftN CompileHL.compile hlProg'. + Definition progR: NAry inputs Z (@HL.expr R (@LL.arg R Z) ResultType) := + liftN (@HLConversions.convertExpr Z R _ _ ResultType _) ( + liftN (HLConversions.mapVar + (fun t => @LL.uninterp_arg_as_var R Z t) + (fun t => fun x => typeMap (fun x => + Z.of_N (orElse 0%N (option_map rwv_value x))) ( + @LL.interp_arg' _ _ t LLConversions.rangeOf x))) ( - Definition wordProg: NAry inputs Z (@CompileLL.WExpr bits ResultType) := - liftN (LLConversions.ZToWord (n := bits) Z) llProg. + Input.hlProg)). - Definition qhasmProg := CompileLL.compile (w := width) wordProg. + Definition progW: NAry inputs Z (@HL.expr W (@LL.arg W Z) ResultType) := + liftN (@HLConversions.convertExpr Z W _ _ ResultType _) ( + liftN (HLConversions.mapVar + (fun t => @LL.uninterp_arg_as_var W Z t) + (fun t => fun x => typeMap (fun x => Z.of_N (wordToN x)) ( + @LL.interp_arg' _ _ t (fun x => NToWord bits (Z.to_N x)) x))) ( - Definition qhasmString : option string := - match qhasmProg with - | Some (p, _) => StringConversion.convertProgram p - | None => None - end. + Input.hlProg)). + End HL. - Import LLConversions. + Module LL. + Definition progZ: NAry inputs Z (@LL.expr Z Z ResultType) := + liftN CompileHL.compile HL.progZ. - Definition RWV: Type := option RangeWithValue. + Definition progR: NAry inputs Z (@LL.expr R Z ResultType) := + liftN CompileHL.compile HL.progR. - Instance RWVEvaluable : Evaluable RWV := @RWVEvaluable bits. - Instance ZEvaluable : Evaluable Z := @ZEvaluable bits. + Definition progW: NAry inputs Z (@LL.expr W Z ResultType) := + liftN CompileHL.compile HL.progW. + End LL. - Existing Instance RWVEvaluable. - Existing Instance ZEvaluable. + Module AST. + Definition progZ: NAry inputs Z (@interp_type Z ResultType) := + liftN (LL.interp' (fun x => x)) LL.progZ. - Arguments HL.expr _ _ _ : clear implicits. - Arguments LL.arg _ _ _ : clear implicits. - Arguments interp_type _ _ : clear implicits. - Definition rwvHL: NAry inputs Z (@HL.expr RWV (@LL.arg RWV Z) ResultType) := - liftN (@HLConversions.convertExpr Z RWV _ _ ResultType _) ( - liftN (HLConversions.mapVar - (fun t => @LL.uninterp_arg_as_var RWV Z t) - (fun t => fun x => typeMap (fun x => Z.of_N (orElse 0%N (option_map rwv_value x))) (@LL.interp_arg' _ _ t rangeOf x))) ( + Definition progR: NAry inputs Z (@interp_type R ResultType) := + liftN (LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x)))) LL.progR. + + Definition progW: NAry inputs Z (@interp_type W ResultType) := + liftN (LL.interp' (fun x => NToWord bits (Z.to_N x))) LL.progW. + End AST. + + Module Qhasm. + Definition pair := @CompileLL.compile bits width ResultType _ LL.progW. + + Definition prog := option_map fst pair. - hlProg)). + Definition outputRegisters := option_map snd pair. - Definition rwvLL: @LL.expr RWV Z ResultType := - Util.applyProgOn (map (@Some _) inputBounds) ( - NArgMap (orElse 0%Z) ( - liftN CompileHL.compile rwvHL)). + Definition code := option_map StringConversion.convertProgram prog. + End Qhasm. - Definition outputBounds := - typeMap (option_map rwvToRange) ( - LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x))) ( - rwvLL)). + Module Bounds. + Definition input := Input.inputBounds. - Definition valid := check (n := bits) rwvLL. + Definition prog := Util.applyProgOn (2 ^ (Z.of_nat bits) - 1)%Z input LL.progR. + + Definition valid := LLConversions.check (n := bits) prog. + + Definition output := + LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x))) prog. + End Bounds. End Pipeline. Module SimpleExample. @@ -111,3 +146,4 @@ Module SimpleExample. Export SimplePipeline. End SimpleExample. + |