From 58a8ee8caf2879d0f351e916b40b7bee90c8d03d Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Wed, 26 Oct 2016 11:12:18 -0700 Subject: Refactors to remove intermediate conversions --- src/Assembly/Compile.v | 7 +- src/Assembly/Conversions.v | 98 ++----------------- src/Assembly/Evaluables.v | 39 ++++++++ src/Assembly/GF25519.v | 239 ++++++++++++++++++++++++--------------------- src/Assembly/HL.v | 91 +++++++++-------- src/Assembly/LL.v | 2 +- src/Assembly/Pipeline.v | 65 ++++++------ 7 files changed, 253 insertions(+), 288 deletions(-) (limited to 'src/Assembly') diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v index 9db4f7188..f0ee42e7c 100644 --- a/src/Assembly/Compile.v +++ b/src/Assembly/Compile.v @@ -15,9 +15,9 @@ Module CompileHL. Section Compilation. Context {T: Type}. - Fixpoint compile {t} (e:@HL.expr T (@LL.arg T T) t) : @LL.expr T T t := + Fixpoint compile {T t} (e:@HL.expr T (@LL.arg T T) t) : @LL.expr T T t := match e with - | HL.Const n => LL.Return (LL.Const n) + | HL.Const _ n => LL.Return (LL.Const n) | HL.Var _ arg => LL.Return arg @@ -41,6 +41,9 @@ Module CompileHL. let (a1, a2) := LL.match_arg_Prod arg in compile (eC a1 a2)) end. + + Definition Compile {T t} (e:@HL.Expr T t) : @LL.expr T T t := + compile (e (@LL.arg T T)). End Compilation. Section Correctness. diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v index 6caaa3019..c7801c63a 100644 --- a/src/Assembly/Conversions.v +++ b/src/Assembly/Conversions.v @@ -31,29 +31,9 @@ Defined. Module HLConversions. Import HL. - Fixpoint mapVar {A: Type} {t V0 V1} (f: forall t, V0 t -> V1 t) (g: forall t, V1 t -> V0 t) (a: expr (T := A) (var := V0) t): expr (T := A) (var := V1) t := + Fixpoint convertExpr {A B: Type} {EB: Evaluable B} {t v} (a: expr (T := A) (var := v) t): expr (T := B) (var := v) t := match a with - | Const x => Const x - | Var t x => Var (f _ x) - | Binop t1 t2 t3 o e1 e2 => Binop o (mapVar f g e1) (mapVar f g e2) - | Let tx e tC h => Let (mapVar f g e) (fun x => mapVar f g (h (g _ x))) - | Pair t1 e1 t2 e2 => Pair (mapVar f g e1) (mapVar f g e2) - | MatchPair t1 t2 e tC h => MatchPair (mapVar f g e) (fun x y => mapVar f g (h (g _ x) (g _ y))) - end. - - Definition convertVar {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t} (a: interp_type (T := A) t): interp_type (T := B) t. - Proof. - induction t as [| t3 IHt1 t4 IHt2]. - - - refine (@toT B EB (@fromT A EA _)); assumption. - - - destruct a as [a1 a2]; constructor; - [exact (IHt1 a1) | exact (IHt2 a2)]. - Defined. - - Fixpoint convertExpr {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t v} (a: expr (T := A) (var := v) t): expr (T := B) (var := v) t := - match a with - | Const x => Const (@toT B EB (@fromT A EA x)) + | Const E x => Const (@toT B EB (@fromT A E x)) | Var t x => @Var B _ t x | Binop t1 t2 t3 o e1 e2 => @Binop B _ t1 t2 t3 o (convertExpr e1) (convertExpr e2) @@ -63,32 +43,6 @@ Module HLConversions. | MatchPair t1 t2 e tC f => MatchPair (convertExpr e) (fun x y => convertExpr (f x y)) end. - - Definition convertZToWord {t} n v a := - @convertExpr Z (word n) (@ZEvaluable n) (@WordEvaluable n) t v a. - - Definition convertZToBounded {t} n v a := - @convertExpr Z (option (@BoundedWord n)) - (@ZEvaluable n) (@BoundedEvaluable n) t v a. - - Definition ZToWord {t} n (a: @Expr Z t): @Expr (word n) t := - fun v => convertZToWord n v (a v). - - Definition ZToRange {t} n (a: @Expr Z t): @Expr (option (@BoundedWord n)) t := - fun v => convertZToBounded n v (a v). - - Definition BInterp {n t} E: @interp_type (option (@BoundedWord n)) t := - @Interp (option (@BoundedWord n)) (@BoundedEvaluable n) t E. - - Example example_Expr : Expr TT := fun var => ( - Let (Const 7) (fun a => - Let (Let (Binop OPadd (Var a) (Var a)) (fun b => Pair (Var b) (Var b))) (fun p => - MatchPair (Var p) (fun x y => - Binop OPadd (Var x) (Var y)))))%Z. - - Example interp_example_range : - option_map bw_high (BInterp (ZToRange 32 example_Expr)) = Some 28%N. - Proof. cbv; reflexivity. Qed. End HLConversions. Module LLConversions. @@ -148,7 +102,7 @@ Module LLConversions. Transparent Word Bounded RWV. Instance RWVEvaluable' : Evaluable RWV := @RWVEvaluable n. - Instance ZEvaluable' : Evaluable Z := @ZEvaluable n. + Instance ZEvaluable' : Evaluable Z := ZEvaluable. Existing Instance ZEvaluable'. Existing Instance WordEvaluable. @@ -207,7 +161,7 @@ Module LLConversions. Definition R := (option RangeWithValue). Instance RE : Evaluable R := @RWVEvaluable n. - Instance ZE : Evaluable Z := @ZEvaluable n. + Instance ZE : Evaluable Z := ZEvaluable. Instance WE : Evaluable W := @WordEvaluable n. Instance BE : Evaluable B := @BoundedEvaluable n. @@ -272,7 +226,7 @@ Module LLConversions. Lemma ZToBounded_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: @arg Z Z tx) (y: @arg Z Z ty) e f, bcheck (t := tz) (f := f) (LetBinop op x y e) = true - -> opZ (n := n) op (interp_arg x) (interp_arg y) = + -> opZ op (interp_arg x) (interp_arg y) = varBoundedToZ (n := n) (opBounded op (interp_arg' f (convertArg _ x)) (interp_arg' f (convertArg _ y))). @@ -281,7 +235,7 @@ Module LLConversions. Lemma ZToWord_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e f, bcheck (t := tz) (f := f) (LetBinop op x y e) = true - -> opZ (n := n) op (interp_arg x) (interp_arg y) = + -> opZ op (interp_arg x) (interp_arg y) = varWordToZ (opWord (n := n) op (varZToWord (interp_arg x)) (varZToWord (interp_arg y))). Proof. Admitted. @@ -289,7 +243,7 @@ Module LLConversions. Lemma roundTrip_0 : @toT Correctness.B BE (@fromT Z ZE 0%Z) <> None. Proof. intros; unfold toT, fromT, BE, ZE, BoundedEvaluable, ZEvaluable, bwFromRWV; - break_match; simpl; try break_match; simpl; try abstract (intro Z; inversion Z); + simpl; try break_match; simpl; try abstract (intro Z; inversion Z); pose proof (Npow2_gt0 n); simpl in *; nomega. Qed. @@ -337,7 +291,7 @@ Module LLConversions. Lemma RangeInterp_bounded_spec: forall {t} (E: @expr Z Z t), bcheck (f := ZtoB) E = true - -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp (n := n) E) = wordInterp (ZToWord _ E). + -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E) = wordInterp (ZToWord _ E). Proof. intros t E S. unfold zinterp, ZToWord, wordInterp. @@ -491,7 +445,7 @@ Module LLConversions. Lemma RangeInterp_spec: forall {t} (E: @expr Z Z t), check (f := rangeOf) (@convertExpr Z R _ _ _ _ E) = true - -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp (n := n) E) + -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E) = wordInterp (ZToWord _ E). Proof. intros. @@ -502,37 +456,3 @@ Module LLConversions. End RWVSpec. End Correctness. End LLConversions. - -Section ConversionTest. - Import HL HLConversions. - - Fixpoint keepAddingOne {var} (x : @expr Z var TT) (n : nat) : @expr Z var TT := - match n with - | O => x - | S n' => Let (Binop OPadd x (Const 1%Z)) (fun y => keepAddingOne (Var y) n') - end. - - Definition KeepAddingOne (n : nat) : Expr (T := Z) TT := - fun var => keepAddingOne (Const 1%Z) n. - - Definition testCase := Eval vm_compute in KeepAddingOne 4000. - - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 0 testCase))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 1 testCase))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 10 testCase))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 32 testCase))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 64 testCase))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 128 testCase))). - - Definition nefarious : Expr (T := Z) TT := - fun var => Let (Binop OPadd (Const 10%Z) (Const 20%Z)) - (fun y => Binop OPmul (Var y) (Const 0%Z)). - - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 0 nefarious))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 1 nefarious))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 4 nefarious))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 5 nefarious))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 32 nefarious))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 64 nefarious))). - Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 128 nefarious))). -End ConversionTest. diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v index 5d2f557e0..0678c80bb 100644 --- a/src/Assembly/Evaluables.v +++ b/src/Assembly/Evaluables.v @@ -50,9 +50,29 @@ End Evaluability. Section Z. Context {n: nat}. + Instance ZEvaluable : Evaluable Z := { ezero := 0%Z; + (* Conversions *) + toT := fun x => Z.of_N (orElse 0%N (option_map rwv_value x)); + fromT := fun x => Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x)); + + (* Operations *) + eadd := Z.add; + esub := Z.sub; + emul := Z.mul; + eshiftr := Z.shiftr; + eand := Z.land; + + (* Comparisons *) + eltb := Z.ltb; + eeqb := Z.eqb + }. + + Instance ConstEvaluable : Evaluable Z := { + ezero := 0%Z; + (* Conversions *) toT := fun x => Z.of_N (orElse 0%N (option_map rwv_value x)); fromT := fun x => @@ -71,6 +91,25 @@ Section Z. eltb := Z.ltb; eeqb := Z.eqb }. + + Instance InputEvaluable : Evaluable Z := { + ezero := 0%Z; + + (* Conversions *) + toT := fun x => Z.of_N (orElse 0%N (option_map rwv_value x)); + fromT := fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x)); + + (* Operations *) + eadd := Z.add; + esub := Z.sub; + emul := Z.mul; + eshiftr := Z.shiftr; + eand := Z.land; + + (* Comparisons *) + eltb := Z.ltb; + eeqb := Z.eqb + }. End Z. Section Word. diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 9a9215c4d..5011237ee 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -1,5 +1,4 @@ Require Import Crypto.Assembly.Pipeline. - Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.ModularArithmetic.ModularBaseSystem. Require Import Crypto.Specific.GF25519. @@ -9,8 +8,7 @@ Module GF25519. Definition bits: nat := 64. Definition width: Width bits := W64. - Instance ZE : Evaluable Z := @ZEvaluable bits. - Existing Instance ZE. + Existing Instance ZEvaluable. Fixpoint makeBoundList {n} k (b: @BoundedWord n) := match k with @@ -35,168 +33,188 @@ Module GF25519. exact t. Defined. - 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. + Section Expressions. + 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}: + 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. + 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. - Module AddExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. + Ltac intro_vars_for R := revert R; + match goal with + | [ |- forall x, @?T x ] => apply (@unflatten T); intros + end. Definition ge25519_add_expr := - Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in carry_add. + Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in carry_add. - 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 }. + Definition ge25519_sub_expr := + Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in carry_sub. + + Definition ge25519_mul_expr := + Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in mul. + + Definition ge25519_opp_expr := + Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in opp. + + Definition ge25519_add' (P Q: @interp_type Z FE): + { r: @HL.Expr Z FE | HL.Interp r = ge25519_add_expr P Q }. Proof. intro_vars_for P. intro_vars_for Q. eexists. + cbv beta delta [ge25519_add_expr]. + etransitivity; [reflexivity|]. + let R := HL.rhs_of_goal in - let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (t := ResultType) X); [reflexivity|]. + let X := HL.Reify R in + transitivity (HL.Interp (X bits)); [reflexivity|]. + + cbv iota beta delta [ HL.Interp + interp_type interp_binop HL.interp + Z.land ZEvaluable eadd esub emul eshiftr eand]. - cbv iota beta delta [ - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. reflexivity. Defined. - Definition ge25519_add (P Q: @interp_type Z ResultType) := - proj1_sig (ge25519_add' P Q). - - Definition hlProg: NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := - 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 }. + Definition ge25519_sub' (P Q: @interp_type Z FE): + { r: @HL.Expr Z FE | HL.Interp r = ge25519_sub_expr P Q }. Proof. intro_vars_for P. intro_vars_for Q. eexists. + cbv beta delta [ge25519_sub_expr]. + etransitivity; [reflexivity|]. + let R := HL.rhs_of_goal in - let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (t := ResultType) X); [reflexivity|]. + let X := HL.Reify R in + transitivity (HL.Interp (X bits)); [reflexivity|]. + + cbv iota beta delta [ HL.Interp + interp_type interp_binop HL.interp + Z.land ZEvaluable eadd esub emul eshiftr eand]. - 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 ge25519_mul' (P Q: @interp_type Z FE): + { r: @HL.Expr Z FE | HL.Interp r = ge25519_mul_expr P Q }. + Proof. + intro_vars_for P. + intro_vars_for 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. + eexists. - Module MulExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. + cbv beta delta [ge25519_mul_expr]. - Definition ge25519_mul_expr := - Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in mul. + etransitivity; [reflexivity|]. + + let R := HL.rhs_of_goal in + let X := HL.Reify R in + transitivity (HL.Interp (X bits)); [reflexivity|]. + + cbv iota beta delta [ HL.Interp + interp_type interp_binop HL.interp + Z.land ZEvaluable eadd esub emul eshiftr eand]. - 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 }. + reflexivity. + Defined. + + Definition ge25519_opp' (P: @interp_type Z FE): + { r: @HL.Expr Z FE | HL.Interp r = ge25519_opp_expr P }. Proof. intro_vars_for P. - intro_vars_for Q. eexists. - cbv beta delta [ge25519_mul_expr]. + + cbv beta delta [ge25519_opp_expr zero_]. + + etransitivity; [reflexivity|]. let R := HL.rhs_of_goal in - let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (t := ResultType) X); [reflexivity|]. + let X := HL.Reify R in + transitivity (HL.Interp (X bits)); [reflexivity|]. + + cbv iota beta delta [ HL.Interp + interp_type interp_binop HL.interp + Z.land ZEvaluable eadd esub emul eshiftr eand]. - 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) := + Definition ge25519_add (P Q: @interp_type Z FE) := + proj1_sig (ge25519_add' P Q). + + Definition ge25519_sub (P Q: @interp_type Z FE) := + proj1_sig (ge25519_sub' P Q). + + Definition ge25519_mul (P Q: @interp_type Z FE) := 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. + Definition ge25519_opp (P: @interp_type Z FE) := + proj1_sig (ge25519_opp' P). + End Expressions. - Module OppExpr <: Expression. + Module AddExpr <: Expression. Definition bits: nat := bits. - Definition inputs: nat := 10. + Definition inputs: nat := 20. Definition width: Width bits := width. Definition ResultType := FE. - Definition inputBounds := feBound. + Definition inputBounds := feBound ++ feBound. - Definition ge25519_opp_expr := - Eval cbv beta delta [fe25519 carry_add mul carry_sub carry_opp Let_In] in carry_opp. + Definition prog: NAry 20 Z (@HL.Expr Z ResultType) := + Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_add p q)))). + End AddExpr. - Definition ge25519_opp' (P: @interp_type Z FE) : - { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := @ZEvaluable bits) (t := FE) r = ge25519_opp_expr P }. - Proof. - intro_vars_for P. + Module SubExpr <: Expression. + Definition bits: nat := bits. + Definition inputs: nat := 20. + Definition width: Width bits := width. + Definition ResultType := FE. + Definition inputBounds := feBound ++ feBound. - eexists. - cbv beta delta [ge25519_opp_expr zero_]. + Definition ge25519_sub_expr := + Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in + carry_sub. - let R := HL.rhs_of_goal in - let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := @ZEvaluable bits) (t := ResultType) X); - [reflexivity|]. + Definition prog: NAry 20 Z (@HL.Expr Z ResultType) := + Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_sub p q)))). + End SubExpr. - cbv iota beta delta [ - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - reflexivity. - Defined. + 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_opp (P: @interp_type Z ResultType) := - proj1_sig (ge25519_opp' P). + Definition prog: NAry 20 Z (@HL.Expr 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. + Definition width: Width bits := width. + Definition ResultType := FE. + Definition inputBounds := feBound. - Definition hlProg: NAry 10 Z (@HL.expr Z (@interp_type Z) ResultType) := - Eval cbv in (flatten (fun p => ge25519_opp p)). + Definition prog: NAry 10 Z (@HL.Expr Z ResultType) := + Eval cbv in (flatten ge25519_opp). End OppExpr. Module Add := Pipeline AddExpr. @@ -205,12 +223,7 @@ Module GF25519. Module Opp := Pipeline OppExpr. End GF25519. -Set Printing All. -Opaque eadd esub emul eshiftr eand toT fromT. -Eval cbv iota beta delta in GF25519.Add.HL.progZ. -Eval cbv iota beta delta in GF25519.Add.AST.progZ. - Extraction "GF25519Add" GF25519.Add. Extraction "GF25519Sub" GF25519.Sub. Extraction "GF25519Mul" GF25519.Mul. -Extraction "GF25519Opp" GF25519.Opp. +Extraction "GF25519Opp" GF25519.Opp. \ No newline at end of file diff --git a/src/Assembly/HL.v b/src/Assembly/HL.v index b1147ccf8..e9eecd4c8 100644 --- a/src/Assembly/HL.v +++ b/src/Assembly/HL.v @@ -18,7 +18,7 @@ Module HL. Context {var : type -> Type}. Inductive expr : type -> Type := - | Const : @interp_type T TT -> expr TT + | Const : forall {_ : Evaluable T}, @interp_type T TT -> expr TT | Var : forall {t}, var t -> expr t | Binop : forall {t1 t2 t3}, binop t1 t2 t3 -> expr t1 -> expr t2 -> expr t3 | Let : forall {tx}, expr tx -> forall {tC}, (var tx -> expr tC) -> expr tC @@ -26,11 +26,11 @@ Module HL. | MatchPair : forall {t1 t2}, expr (Prod t1 t2) -> forall {tC}, (var t1 -> var t2 -> expr tC) -> expr tC. End expr. - Local Notation ZConst z := (@Const Z ZEvaluable _ z%Z). + Local Notation ZConst z := (@Const Z ConstEvaluable _ z%Z). - Fixpoint interp {t} (e: @expr interp_type t) : interp_type t := + Fixpoint interp {t} (e: @expr interp_type t) : @interp_type T t := match e in @expr _ t return interp_type t with - | Const n => n + | Const _ x => x | Var _ n => n | Binop _ _ _ op e1 e2 => interp_binop op (interp e1) (interp e2) | Let _ ex _ eC => dlet x := interp ex in interp (eC x) @@ -40,29 +40,26 @@ Module HL. Definition Expr t : Type := forall var, @expr var t. - Definition Interp {t} (E: Expr t) : interp_type t := interp (E interp_type). - - Definition Expr' t : Type := forall var, (forall t', @interp_type Z t' -> var t') -> @expr var t. - - Definition Interp' {t} (f: Z -> T) (E: Expr' t) : interp_type t := - interp (E (@interp_type T) (fun t' x => typeMap (t := t') f x)). + Definition Interp {t} (e: Expr t) : interp_type t := interp (e interp_type). End Language. - Definition zinterp {n t} E := @interp Z (@ZEvaluable n) t E. + Definition zinterp {t} E := @interp Z ZEvaluable t E. - Definition ZInterp {n t} E := @Interp Z (@ZEvaluable n) t E. + Definition ZInterp {t} E := @Interp Z ZEvaluable t E. Definition wordInterp {n t} E := @interp (word n) (@WordEvaluable n) t E. Definition WordInterp {n t} E := @Interp (word n) (@WordEvaluable n) t E. + Existing Instance ZEvaluable. + Example example_Expr : Expr TT := fun var => ( Let (Const 7) (fun a => Let (Let (Binop OPadd (Var a) (Var a)) (fun b => Pair (Var b) (Var b))) (fun p => MatchPair (Var p) (fun x y => Binop OPadd (Var x) (Var y)))))%Z. - Example interp_example_Expr : ZInterp (n := 16) example_Expr = 28%Z. + Example interp_example_Expr : ZInterp example_Expr = 28%Z. Proof. reflexivity. Qed. (* Reification assumes the argument type is Z *) @@ -85,68 +82,68 @@ Module HL. | Z.shiftr => constr:(OPshiftr) end. - Class reify {varT} (var:varT) {eT} (e:eT) {T:Type} := Build_reify : T. + Class reify (n: nat) {varT} (var:varT) {eT} (e:eT) {T:Type} := Build_reify : T. Definition reify_var_for_in_is {T} (x:T) (t:type) {eT} (e:eT) := False. - Ltac reify var e := + Ltac reify n var e := lazymatch e with | let x := ?ex in @?eC x => - let ex := reify var ex in - let eC := reify var eC in - constr:(Let (T := Z) (var:=var) ex eC) + let ex := reify n var ex in + let eC := reify n var eC in + constr:(Let (T:=Z) (var:=var) ex eC) | match ?ep with (v1, v2) => @?eC v1 v2 end => - let ep := reify var ep in - let eC := reify var eC in - constr:(MatchPair (T := Z) (var:=var) ep eC) + let ep := reify n var ep in + let eC := reify n var eC in + constr:(MatchPair (T:=Z) (var:=var) ep eC) | pair ?a ?b => - let a := reify var a in - let b := reify var b in - constr:(Pair (T := Z) (var:=var) a b) + let a := reify n var a in + let b := reify n var b in + constr:(Pair (T:=Z) (var:=var) a b) | ?op ?a ?b => let op := reify_binop op in - let b := reify var b in - let a := reify var a in - constr:(Binop (T := Z) (var:=var) op a b) + let b := reify n var b in + let a := reify n var a in + constr:(Binop (T:=Z) (var:=var) op a b) | (fun x : ?T => ?C) => let t := reify_type T in (* Work around Coq 8.5 and 8.6 bug *) (* *) (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) (* even if its Gallina name matches a Ltac in this tactic. *) + (* [C] here is an open term that references "x" by name *) let maybe_x := fresh x in let not_x := fresh x in lazymatch constr:(fun (x : T) (not_x : var t) (_:reify_var_for_in_is x t not_x) => - (_ : reify var C)) (* [C] here is an open term that references "x" by name *) + (_ : reify n var C)) with fun _ v _ => @?C v => C end | ?x => lazymatch goal with | _:reify_var_for_in_is x ?t ?v |- _ => constr:(@Var Z var t v) - | _ => - let x' := eval cbv in x in - match isZcst x' with - | true => constr:(@Const Z var x) - | false => constr:(@Var Z var TT x) + | _ => let x' := eval cbv in x in + match isZcst x with + | true => constr:(@Const Z var (@ConstEvaluable n) x) + | false => constr:(@Const Z var InputEvaluable x) end end end. - Hint Extern 0 (reify ?var ?e) => (let e := reify var e in eexact e) : typeclass_instances. + Hint Extern 0 (reify ?n ?var ?e) => (let e := reify n var e in eexact e) : typeclass_instances. Ltac Reify e := - lazymatch constr:(fun (var:type->Type) => (_:reify var e)) with - (fun var => ?C) => constr:(fun (var:type->Type) => C) (* copy the term but not the type cast *) + lazymatch constr:(fun (n: nat) (var:type->Type) => (_:reify n var e)) with + (fun n var => ?C) => constr:(fun (n: nat) (var:type->Type) => C) (* copy the term but not the type cast *) end. Definition zinterp_type := @interp_type Z. Transparent zinterp_type. - Goal forall (x : Z) (v : zinterp_type TT) (_:reify_var_for_in_is x TT v), reify(T:=Z) zinterp_type ((fun x => x+x) x)%Z. + Goal forall (x : Z) (v : zinterp_type TT) (_:reify_var_for_in_is x TT v), reify (T:=Z) 16 zinterp_type ((fun x => x+x) x)%Z. intros. - let A := (reify zinterp_type (x + x + 1)%Z) in pose A. + let A := (reify 16 zinterp_type (x + x + 1)%Z) in idtac A. Abort. Goal False. - let z := reify zinterp_type (let x := 0 in x)%Z in pose z. + let z := (reify 16 zinterp_type (let x := 0 in x)%Z) in pose z. Abort. Ltac lhs_of_goal := match goal with |- ?R ?LHS ?RHS => constr:(LHS) end. @@ -155,7 +152,7 @@ Module HL. Ltac Reify_rhs n := let rhs := rhs_of_goal in let RHS := Reify rhs in - transitivity (ZInterp (n := n) RHS); + transitivity (ZInterp (RHS n)); [|cbv iota beta delta [ZInterp Interp interp_type interp_binop interp]; reflexivity]. Goal (0 = let x := 1+2 in x*3)%Z. @@ -171,7 +168,7 @@ Module HL. Local Notation "x ≡ y" := (existT _ _ (x, y)). - Definition Texpr var t := @expr T var t. + Definition Texpr var t := @expr Z var t. Inductive wf : list (sigT (fun t => var1 t * var2 t))%type -> forall {t}, Texpr var1 t -> Texpr var2 t -> Prop := | WfConst : forall G n, wf G (Const n) (Const n) @@ -181,25 +178,25 @@ Module HL. (op: binop t1 t2 t3), wf G e1 e1' -> wf G e2 e2' - -> wf G (Binop (T := T) op e1 e2) (Binop (T := T) op e1' e2') + -> wf G (Binop op e1 e2) (Binop op e1' e2') | WfLet : forall G t1 t2 e1 e1' (e2 : _ t1 -> Texpr _ t2) e2', wf G e1 e1' -> (forall x1 x2, wf ((x1 ≡ x2) :: G) (e2 x1) (e2' x2)) - -> wf G (Let (T := T) e1 e2) (Let (T := T) e1' e2') + -> wf G (Let e1 e2) (Let e1' e2') | WfPair : forall G {t1} {t2} (e1: Texpr var1 t1) (e2: Texpr var1 t2) (e1': Texpr var2 t1) (e2': Texpr var2 t2), wf G e1 e1' -> wf G e2 e2' - -> wf G (Pair (T := T) e1 e2) (Pair (T := T) e1' e2') + -> wf G (Pair e1 e2) (Pair e1' e2') | WfMatchPair : forall G t1 t2 tC ep ep' (eC : _ t1 -> _ t2 -> Texpr _ tC) eC', wf G ep ep' -> (forall x1 x2 y1 y2, wf ((x1 ≡ x2) :: (y1 ≡ y2) :: G) (eC x1 y1) (eC' x2 y2)) - -> wf G (MatchPair (T := T) ep eC) (MatchPair (T := T) ep' eC'). + -> wf G (MatchPair ep eC) (MatchPair ep' eC'). End wf. - Definition Wf {T: Type} {t} (E : @Expr T t) := forall var1 var2, wf nil (E var1) (E var2). + Definition Wf {T: Type} {t} (E : Expr t) := forall var1 var2, wf nil (E var1) (E var2). - Example example_Expr_Wf : Wf example_Expr. + Example example_Expr_Wf : Wf (T := Z) example_Expr. Proof. unfold Wf; repeat match goal with | [ |- wf _ _ _ ] => constructor diff --git a/src/Assembly/LL.v b/src/Assembly/LL.v index e0588214c..60587eb19 100644 --- a/src/Assembly/LL.v +++ b/src/Assembly/LL.v @@ -92,7 +92,7 @@ Module LL. Transparent interp interp_arg. Example example_expr : - (@interp Z (ZEvaluable (n := 32)) _ + (@interp Z (ZEvaluable) _ (LetBinop OPadd (Const 7%Z) (Const 8%Z) (fun v => Return v)) = 15)%Z. Proof. reflexivity. Qed. diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index fc888bc56..8eaa07161 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -20,9 +20,10 @@ Module Type Expression. Parameter bits: nat. Parameter width: Width bits. Parameter inputs: nat. - Parameter ResultType: type. - Parameter hlProg: NAry inputs Z (@HL.Expr' Z ResultType). Parameter inputBounds: list Z. + Parameter ResultType: type. + + Parameter prog: NAry inputs Z (@HL.Expr Z ResultType). End Expression. Module Pipeline (Input: Expression). @@ -37,7 +38,7 @@ Module Pipeline (Input: Expression). Definition R: Type := option RangeWithValue. Definition B: Type := option (@BoundedWord bits). - Instance ZEvaluable : Evaluable Z := @ZEvaluable bits. + Instance ZEvaluable : Evaluable Z := ZEvaluable. Instance WEvaluable : Evaluable W := @WordEvaluable bits. Instance REvaluable : Evaluable R := @RWVEvaluable bits. Instance BEvaluable : Evaluable B := @BoundedEvaluable bits. @@ -57,36 +58,25 @@ Module Pipeline (Input: Expression). End Util. Module HL. - Transparent HL.Expr'. + Definition progZ: NAry inputs Z (@HL.Expr Z ResultType) := + Input.prog. - Definition progZ: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN _ Input.hlProg); intro X; apply X. - refine (fun t x => @LL.uninterp_arg Z Z t x). - Defined. + Definition progR: NAry inputs Z (@HL.Expr R ResultType) := + liftN (fun x v => @HLConversions.convertExpr Z R _ _ _ (x v)) Input.prog. - Definition progR: NAry inputs Z (@HL.expr R (@LL.arg R R) ResultType). - refine (liftN _ _); [eapply (@HLConversions.convertExpr Z R _ _)|]. - refine (liftN _ Input.hlProg); intro X; apply X. - refine (fun t x => @LL.uninterp_arg R R t (typeMap LLConversions.rangeOf x)). - Defined. - - Definition progW: NAry inputs Z (@HL.expr W (@LL.arg W W) ResultType). - refine (liftN _ _); [eapply (@HLConversions.convertExpr Z W _ _)|]. - refine (liftN _ Input.hlProg); intro X; apply X. - refine (fun t x => @LL.uninterp_arg W W t (typeMap (fun v => - NToWord bits (Z.to_N v)) x)). - Defined. + Definition progW: NAry inputs Z (@HL.Expr W ResultType) := + liftN (fun x v => @HLConversions.convertExpr Z W _ _ _ (x v)) Input.prog. End HL. Module LL. Definition progZ: NAry inputs Z (@LL.expr Z Z ResultType) := - liftN CompileHL.compile HL.progZ. + liftN CompileHL.Compile HL.progZ. Definition progR: NAry inputs Z (@LL.expr R R ResultType) := - liftN CompileHL.compile HL.progR. + liftN CompileHL.Compile HL.progR. Definition progW: NAry inputs Z (@LL.expr W W ResultType) := - liftN CompileHL.compile HL.progW. + liftN CompileHL.Compile HL.progW. End LL. Module AST. @@ -101,7 +91,8 @@ Module Pipeline (Input: Expression). End AST. Module Qhasm. - Definition pair := @CompileLL.compile bits width ResultType _ LL.progW. + Definition pair := + @CompileLL.compile bits width ResultType _ LL.progW. Definition prog := option_map fst pair. @@ -111,13 +102,18 @@ Module Pipeline (Input: Expression). End Qhasm. Module Bounds. - Definition input := Input.inputBounds. + Definition input := map (fun x => range N 0%N (Z.to_N x)) Input.inputBounds. - Definition prog := Util.applyProgOn (2 ^ (Z.of_nat bits) - 1)%Z input LL.progR. + Definition upper := Z.of_N (wordToN (wones bits)). + + Definition prog := + Util.applyProgOn upper Input.inputBounds LL.progR. Definition valid := LLConversions.check (n := bits) (f := id) prog. - Definition output := LL.interp prog. + Definition output := + typeMap (option_map (fun x => range N (rwv_low x) (rwv_high x))) + (LL.interp prog). End Bounds. End Pipeline. @@ -130,19 +126,16 @@ Module SimpleExample. Definition inputs: nat := 1. Definition ResultType := TT. - Definition hlProg': NAry 1 Z (@HL.Expr' Z TT). - intros x t f. - refine (HL.Binop OPadd (HL.Var (f TT x)) (HL.Const 5%Z)). - Defined. + Definition inputBounds: list Z := [ (2^30)%Z ]. - Definition hlProg: NAry 1 Z (@HL.Expr' Z TT) := - Eval vm_compute in hlProg'. + Existing Instance ZEvaluable. - Definition inputBounds: list Z := [ (2^30)%Z ]. + Definition prog: NAry 1 Z (@HL.Expr Z TT). + intros x var. + refine (HL.Binop OPadd (HL.Const x) (HL.Const 5%Z)). + Defined. End SimpleExpression. Module SimplePipeline := Pipeline SimpleExpression. - - Export SimplePipeline. End SimpleExample. -- cgit v1.2.3