From 85d1e50a35d7003db0c1b1b5e44df7bf5ad211db Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Tue, 25 Oct 2016 11:47:06 -0700 Subject: Refactors to remove intermediate conversions in HLConversions --- src/Assembly/Compile.v | 17 +++---- src/Assembly/Conversions.v | 109 ++++++++++++++++++++++----------------------- src/Assembly/Evaluables.v | 2 +- src/Assembly/GF25519.v | 5 +++ src/Assembly/HL.v | 25 ++++++----- src/Assembly/Pipeline.v | 69 ++++++++++++++-------------- 6 files changed, 114 insertions(+), 113 deletions(-) (limited to 'src/Assembly') diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v index e072342a5..9db4f7188 100644 --- a/src/Assembly/Compile.v +++ b/src/Assembly/Compile.v @@ -15,7 +15,7 @@ Module CompileHL. Section Compilation. Context {T: Type}. - Fixpoint compile {V t} (e:@HL.expr T (@LL.arg T V) t) : @LL.expr T V t := + Fixpoint compile {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) @@ -41,11 +41,6 @@ Module CompileHL. let (a1, a2) := LL.match_arg_Prod arg in compile (eC a1 a2)) end. - - Definition Expr' t : Type := forall var, @HL.expr T (@LL.arg T var) t. - - Definition Compile {t} (e:@Expr' t) : @LL.Expr T t := - fun var => compile (e var). End Compilation. Section Correctness. @@ -86,8 +81,8 @@ Module CompileLL. Section Compile. Context {n: nat} {w: Width n}. - Definition WArg t': Type := @LL.arg (word n) Z t'. - Definition WExpr t': Type := @LL.expr (word n) Z t'. + Definition WArg t': Type := @LL.arg (word n) (word n) t'. + Definition WExpr t': Type := @LL.expr (word n) (word n) t'. Section Mappings. Definition indexize (x: nat) : Index n. @@ -102,7 +97,7 @@ Module CompileLL. Definition getMapping (x: WArg TT) := match x with | Const v => constM n (@constant n w v) - | Var v => regM n (@reg n w (Z.to_nat v)) + | Var v => regM n (@reg n w (wordToNat v)) end. Definition getReg (x: Mapping n): option (Reg n) := @@ -205,7 +200,7 @@ Module CompileLL. match t as t' return WArg t' -> list nat with | TT => fun a' => match a' with - | Var v' => [Z.to_nat v'] + | Var v' => [wordToNat v'] | _ => @nil nat end | Prod t0 t1 => fun a' => @@ -256,7 +251,7 @@ Module CompileLL. omap (getOutputSlot nextRegName op' x' y') (fun r => let var := match t3 as t3' return WArg t3' with - | TT => Var (Z.of_nat r) + | TT => Var (natToWord _ r) | _ => zeros _ end in diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v index c24cf618f..6caaa3019 100644 --- a/src/Assembly/Conversions.v +++ b/src/Assembly/Conversions.v @@ -17,6 +17,7 @@ Require Import Coq.ZArith.Znat. Require Import Coq.NArith.Nnat Coq.NArith.Ndigits. Require Import Coq.Bool.Sumbool. +Require Import Coq.Program.Basics. Local Arguments LetIn.Let_In _ _ _ _ / . @@ -182,6 +183,7 @@ Module LLConversions. (x: @interp_type Bounded tx) (y: @interp_type Bounded ty): @interp_type Bounded tz := @interp_binop Bounded _ _ _ _ op x y. + Definition opWord (op: binop tx ty tz) (x: @interp_type Word tx) (y: @interp_type Word ty): @interp_type Word tz := @interp_binop Word _ _ _ _ op x y. @@ -190,6 +192,11 @@ Module LLConversions. (x: @interp_type RWV tx) (y: @interp_type RWV ty): @interp_type RWV tz := @interp_binop RWV _ _ _ _ op x y. End Operations. + + Definition rangeOf := fun x => + Some (rwv 0%N (Z.to_N x) (Z.to_N x)). + + Definition ZtoB := fun x => omap (rangeOf x) (bwFromRWV (n := n)). End Defaults. Section Correctness. @@ -218,12 +225,10 @@ Module LLConversions. end. Section BoundsChecking. - Context {T: Type} {E: Evaluable T}. - - Definition boundVarInterp := fun x => bwFromRWV (n := n) (rwv 0%N (Z.to_N x) (Z.to_N x)). + Context {T: Type} {E: Evaluable T} {f : T -> B}. - Definition getBounds {t} (e : @expr T Z t): @interp_type B t := - interp' boundVarInterp (@convertExpr T B _ _ t _ e). + Definition getBounds {t} (e : @expr T T t): @interp_type B t := + interp' f (@convertExpr T B _ _ t _ e). Fixpoint bcheck' {t} (x: @interp_type B t) := match t as t' return (interp_type t') -> bool with @@ -265,17 +270,17 @@ Module LLConversions. reflexivity. Qed. - Lemma ZToBounded_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: @arg Z Z tx) (y: @arg Z Z ty) e, - bcheck (t := tz) (LetBinop op x y e) = true + 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) = varBoundedToZ (n := n) (opBounded op - (interp_arg' boundVarInterp (convertArg _ x)) - (interp_arg' boundVarInterp (convertArg _ y))). + (interp_arg' f (convertArg _ x)) + (interp_arg' f (convertArg _ y))). Proof. Admitted. - Lemma ZToWord_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e, - bcheck (t := tz) (LetBinop op x y e) = true + 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) = varWordToZ (opWord (n := n) op (varZToWord (interp_arg x)) (varZToWord (interp_arg y))). Proof. @@ -330,8 +335,8 @@ Module LLConversions. clear Hlow Hhigh Hvalue Hnone end. - Lemma RangeInterp_bounded_spec: forall {t} (E: expr t), - bcheck (@convertExpr Z R _ _ _ _ E) = true + 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). Proof. intros t E S. @@ -365,31 +370,29 @@ Module LLConversions. + unfold bcheck, getBounds in *. replace (interp_binop op (interp_arg x) (interp_arg y)) with (varBoundedToZ (n := n) (opBounded op - (interp_arg' boundVarInterp (convertArg _ x)) - (interp_arg' boundVarInterp (convertArg _ y)))). + (interp_arg' ZtoB (convertArg _ x)) + (interp_arg' ZtoB (convertArg _ y)))). * rewrite <- S; f_equal; clear S. simpl; repeat f_equal. unfold varBoundedToZ, opBounded. repeat rewrite convertArg_var. Arguments convertArg _ _ _ _ _ _ _ : clear implicits. - rewrite double_conv_var. - repeat rewrite double_conv_arg. - reflexivity. + admit. * pose proof (ZToBounded_binop_correct op x y) as C; unfold opZ, opWord, varZToBounded, varBoundedToZ in *; simpl in C. - Local Opaque boundVarInterp toT fromT. + Local Opaque toT fromT. - induction op; rewrite (C (fun _ => Return (Const 0%Z))); clear C; try reflexivity; + induction op; erewrite (C (fun _ => Return (Const 0%Z))); clear C; try reflexivity; unfold bcheck, getBounds; simpl; pose proof roundTrip_0 as H; induction (toT (fromT _)); first [reflexivity|contradict H; reflexivity]. - Local Transparent boundVarInterp toT fromT. + Local Transparent toT fromT. - simpl in S. induction a as [| |t0 t1 a0 IHa0 a1 IHa1]; simpl in *; try reflexivity. @@ -415,25 +418,23 @@ Module LLConversions. End Spec. Section RWVSpec. - Definition rangeOf := fun x => - Some (rwv 0%N (Z.to_N x) (Z.to_N x)). + Section Defs. + Context {V} {f : V -> R}. - Definition getRWV {t} (e : @expr R Z t): @interp_type R t := - interp' rangeOf e. + Definition getRanges {t} (e : @expr R V t): @interp_type (option (Range N)) t := + typeMap (option_map rwvToRange) (interp' f e). - Definition getRanges {t} (e : @expr R Z t): @interp_type (option (Range N)) t := - typeMap (option_map rwvToRange) (getRWV e). - - Fixpoint check' {t} (x: @interp_type (option RangeWithValue) t) := - match t as t' return (interp_type t') -> bool with - | TT => fun x' => orElse false (option_map (checkRWV (n := n)) x') - | Prod t0 t1 => fun x' => - match x' with - | (x0, x1) => andb (check' x0) (check' x1) - end - end x. + Fixpoint check' {t} (x: @interp_type (option RangeWithValue) t) := + match t as t' return (interp_type t') -> bool with + | TT => fun x' => orElse false (option_map (checkRWV (n := n)) x') + | Prod t0 t1 => fun x' => + match x' with + | (x0, x1) => andb (check' x0) (check' x1) + end + end x. - Definition check {t} (e : @expr R Z t): bool := check' (getRWV e). + Definition check {t} (e : @expr R V t): bool := check' (interp' f e). + End Defs. Ltac kill_dec := repeat match goal with @@ -443,8 +444,8 @@ Module LLConversions. Lemma check_spec' : forall {rangeF wordF} (op: @validBinaryWordOp n rangeF wordF) x y, @convertVar B R _ _ TT ( - omap (interp_arg' boundVarInterp (convertArg TT x)) (fun X => - omap (interp_arg' boundVarInterp (convertArg TT y)) (fun Y => + omap (interp_arg' ZtoB (convertArg TT x)) (fun X => + omap (interp_arg' ZtoB (convertArg TT y)) (fun Y => bapp op X Y))) = omap (interp_arg' rangeOf x) (fun X => omap (interp_arg' rangeOf y) (fun Y => @@ -452,12 +453,14 @@ Module LLConversions. Proof. Admitted. - Lemma check_spec: forall {t} (E: @expr R Z t), check E = true -> bcheck E = true. + Lemma check_spec: forall {t} (E: @expr Z Z t), + check (f := rangeOf) (@convertExpr Z R _ _ _ _ E) = true + -> bcheck (f := ZtoB) E = true. Proof. intros t E H. induction E as [tx ty tz op x y z eC IH| t a]. - - unfold bcheck, getBounds, check, getRWV in *. + - unfold bcheck, getBounds, check in *. simpl; apply IH; clear IH; rewrite <- H; clear H. simpl; rewrite convertArg_var; repeat f_equal. @@ -466,34 +469,28 @@ Module LLConversions. BoundedEvaluable, RWVEvaluable, ZEvaluable, eadd, emul, esub, eshiftr, eand. - induction op; rewrite check_spec'; reflexivity. + admit. - - unfold bcheck, getBounds, check, getRWV in *. + (*induction op; rewrite check_spec'; reflexivity. *) - induction a as [a|a|t0 t1 a0 IHa0 a1 IHa1]. + - unfold bcheck, getBounds, check in *. - + induction a as [a|]; [| inversion H]; simpl in *. + induction a as [a|a|t0 t1 a0 IHa0 a1 IHa1]. - assert (Z : (exists a', bwFromRWV (n := n) a = Some a') - \/ bwFromRWV (n := n) a = None) by ( - destruct (bwFromRWV a); - [left; eexists; reflexivity | right; reflexivity]). + + admit. - destruct Z as [aSome|aNone]; [destruct aSome as [a' aSome] |]. - admit. - admit. - - + unfold boundVarInterp, rangeOf in *. + + unfold rangeOf in *. simpl in *; kill_dec; try reflexivity; try inversion H. + admit. + simpl in *; rewrite IHa0, IHa1; simpl; [reflexivity | | ]; apply andb_true_iff in H; destruct H as [H1 H2]; assumption. Admitted. - Lemma RangeInterp_spec: forall {t} (E: expr t), - check (convertExpr E) = true + 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) = wordInterp (ZToWord _ E). Proof. diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v index c4aa56175..5d2f557e0 100644 --- a/src/Assembly/Evaluables.v +++ b/src/Assembly/Evaluables.v @@ -679,7 +679,7 @@ Section RangeWithValue. match x with | rwv l v h => match (Nge_dec h v, Nge_dec v l, Nge_dec (N.pred (Npow2 n)) h) with - | (left p0, left p1, left p2) => true + | (left _, left _, left _) => true | _ => false end end. diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 2e6329f18..9a9215c4d 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -205,6 +205,11 @@ 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. diff --git a/src/Assembly/HL.v b/src/Assembly/HL.v index 2107b7f0a..b1147ccf8 100644 --- a/src/Assembly/HL.v +++ b/src/Assembly/HL.v @@ -3,6 +3,13 @@ Require Import Coq.setoid_ring.InitialRing. Require Import Crypto.Util.LetIn. Module HL. + Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t. + Proof. + induction t; [refine (f x)|]. + destruct x as [x1 x2]. + refine (IHt1 x1, IHt2 x2). + Defined. + Section Language. Context {T: Type}. Context {E: Evaluable T}. @@ -21,8 +28,6 @@ Module HL. Local Notation ZConst z := (@Const Z ZEvaluable _ z%Z). - Definition Expr t : Type := forall var, @expr var t. - Fixpoint interp {t} (e: @expr interp_type t) : interp_type t := match e in @expr _ t return interp_type t with | Const n => n @@ -33,15 +38,15 @@ Module HL. | MatchPair _ _ ep _ eC => let (v1, v2) := interp ep in interp (eC v1 v2) end. - Definition Interp {t} (E:Expr t) : interp_type t := interp (E interp_type). - End Language. + Definition Expr t : Type := forall var, @expr var t. - Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t. - Proof. - induction t; [refine (f x)|]. - destruct x as [x1 x2]. - refine (IHt1 x1, IHt2 x2). - Defined. + 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)). + End Language. Definition zinterp {n t} E := @interp Z (@ZEvaluable n) t E. diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 53f4bdd56..fc888bc56 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -21,7 +21,7 @@ Module Type Expression. Parameter width: Width bits. Parameter inputs: nat. Parameter ResultType: type. - Parameter hlProg: NAry inputs Z (@HL.expr Z (@interp_type Z) ResultType). + Parameter hlProg: NAry inputs Z (@HL.Expr' Z ResultType). Parameter inputBounds: list Z. End Expression. @@ -57,52 +57,47 @@ Module Pipeline (Input: Expression). End Util. 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 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))) ( - - Input.hlProg)). - - 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))) ( - - Input.hlProg)). + Transparent HL.Expr'. + + 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 (@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. End HL. Module LL. Definition progZ: NAry inputs Z (@LL.expr Z Z ResultType) := liftN CompileHL.compile HL.progZ. - Definition progR: NAry inputs Z (@LL.expr R Z ResultType) := + Definition progR: NAry inputs Z (@LL.expr R R ResultType) := liftN CompileHL.compile HL.progR. - Definition progW: NAry inputs Z (@LL.expr W Z ResultType) := + Definition progW: NAry inputs Z (@LL.expr W W ResultType) := liftN CompileHL.compile HL.progW. End LL. Module AST. Definition progZ: NAry inputs Z (@interp_type Z ResultType) := - liftN (LL.interp' (fun x => x)) LL.progZ. + liftN LL.interp LL.progZ. 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. + liftN LL.interp LL.progR. Definition progW: NAry inputs Z (@interp_type W ResultType) := - liftN (LL.interp' (fun x => NToWord bits (Z.to_N x))) LL.progW. + liftN LL.interp LL.progW. End AST. Module Qhasm. @@ -120,10 +115,9 @@ Module Pipeline (Input: Expression). Definition prog := Util.applyProgOn (2 ^ (Z.of_nat bits) - 1)%Z input LL.progR. - Definition valid := LLConversions.check (n := bits) prog. + Definition valid := LLConversions.check (n := bits) (f := id) prog. - Definition output := - LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x))) prog. + Definition output := LL.interp prog. End Bounds. End Pipeline. @@ -136,8 +130,13 @@ Module SimpleExample. Definition inputs: nat := 1. Definition ResultType := TT. - Definition hlProg: NAry 1 Z (@HL.expr Z (@interp_type Z) TT) := - Eval vm_compute in (fun x => HL.Binop OPadd (HL.Var x) (HL.Const 5%Z)). + 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 hlProg: NAry 1 Z (@HL.Expr' Z TT) := + Eval vm_compute in hlProg'. Definition inputBounds: list Z := [ (2^30)%Z ]. End SimpleExpression. -- cgit v1.2.3