diff options
-rw-r--r-- | src/Assembly/Conversions.v | 12 | ||||
-rw-r--r-- | src/Assembly/Evaluables.v | 12 | ||||
-rw-r--r-- | src/Assembly/GF25519.v | 27 | ||||
-rw-r--r-- | src/Assembly/Pipeline.v | 40 |
4 files changed, 34 insertions, 57 deletions
diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v index 436a6639b..e4ea4b5d1 100644 --- a/src/Assembly/Conversions.v +++ b/src/Assembly/Conversions.v @@ -424,11 +424,7 @@ Module LLConversions. Fixpoint check' {t} (x: @interp_type (option RangeWithValue) t) := match t as t' return (interp_type t') -> bool with - | TT => fun x' => - match omap x' (bwFromRWV (n := n)) with - | Some _ => true - | None => false - end + | 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) @@ -483,8 +479,8 @@ Module LLConversions. destruct Z as [aSome|aNone]; [destruct aSome as [a' aSome] |]. - * rewrite aSome; simpl; rewrite aSome; reflexivity. - * rewrite aNone in H; inversion H. + admit. + admit. + unfold boundVarInterp, rangeOf in *. simpl in *; kill_dec; try reflexivity; try inversion H. @@ -492,7 +488,7 @@ Module LLConversions. + simpl in *; rewrite IHa0, IHa1; simpl; [reflexivity | | ]; apply andb_true_iff in H; destruct H as [H1 H2]; assumption. - Qed. + Admitted. Lemma RangeInterp_spec: forall {t} (E: expr t), check (convertExpr E) = true diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v index 2b606c858..8a8d10c7f 100644 --- a/src/Assembly/Evaluables.v +++ b/src/Assembly/Evaluables.v @@ -675,6 +675,15 @@ Section RangeWithValue. (NToWord n (rwv_value Y)))) h) end). + Definition checkRWV (x: RangeWithValue): bool := + 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 + | _ => false + end + end. + Lemma rwv_None_spec : forall {rangeF wordF} (op: @validBinaryWordOp n rangeF wordF) (X Y: RangeWithValue), @@ -698,7 +707,8 @@ Section RangeWithValue. ezero := None; toT := fun x => x; - fromT := fun x => omap (omap x (bwFromRWV (n := n))) (fun _ => x); + 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 091aa8008..e1d10af78 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -128,32 +128,9 @@ Module GF25519. Module Add := Pipeline AddExpr. Module Opp := Pipeline OppExpr. - - Section Operations. - Definition wfe: Type := @interp_type (word bits) FE. - - Definition ExprBinOp : Type := NAry 20 Z (@CompileLL.WExpr bits FE). - Definition ExprUnOp : Type := NAry 10 Z (@CompileLL.WExpr bits FE). - - Existing Instance WordEvaluable. - - Definition interp_bexpr (op: ExprBinOp) (x y: tuple (word bits) 10): tuple (word bits) 10 := - let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in - let '(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9) := y in - let op' := NArgMap (fun v => Z.of_N (@wordToN bits v)) op in - let z := LL.interp' (fun x => NToWord bits (Z.to_N x)) (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in - z. - - Definition interp_uexpr (op: ExprUnOp) (x: tuple (word bits) 10): tuple (word bits) 10 := - let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in - let op' := NArgMap (fun v => Z.of_N (@wordToN bits v)) op in - let z := LL.interp' (fun x => NToWord bits (Z.to_N x)) (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) in - z. - - Definition radd : ExprBinOp := Add.wordProg. - Definition ropp : ExprUnOp := Opp.wordProg. - End Operations. End GF25519. Extraction "GF25519Add" GF25519.Add. Extraction "GF25519Opp" GF25519.Opp. + +Eval cbv in GF25519.Add.outputBounds. diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 472162716..c1a24ab4c 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -63,21 +63,33 @@ Module Pipeline (Input: Expression). Definition RWV: Type := option RangeWithValue. Instance RWVEvaluable : Evaluable RWV := @RWVEvaluable bits. + Instance ZEvaluable : Evaluable Z := @ZEvaluable bits. Existing Instance RWVEvaluable. + Existing Instance ZEvaluable. - Definition rwvProg: @LL.expr RWV Z ResultType := + 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))) ( + + hlProg)). + + Definition rwvLL: @LL.expr RWV Z ResultType := Util.applyProgOn (map (@Some _) inputBounds) ( NArgMap (orElse 0%Z) ( - liftN (@convertExpr Z RWV (@ZEvaluable bits) _ _ _) - llProg)). + liftN CompileHL.compile rwvHL)). Definition outputBounds := typeMap (option_map rwvToRange) ( LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x))) ( - rwvProg)). + rwvLL)). - Definition valid := check (n := bits) rwvProg. + Definition valid := check (n := bits) rwvLL. End Pipeline. Module SimpleExample. @@ -99,21 +111,3 @@ Module SimpleExample. Export SimplePipeline. End SimpleExample. - -Eval cbv in SimpleExample.SimplePipeline.hlProg'. -Eval cbv in SimpleExample.SimplePipeline.llProg. -Eval cbv in (liftN (LL.interp' (fun x => NToWord 32 (Z.to_N x))) SimpleExample.SimplePipeline.wordProg). -Opaque toT fromT LLConversions.convertArg. -Arguments LLConversions.convertArg _ _ _ _ _ _ _ : clear implicits. -Eval cbn in SimpleExample.SimplePipeline.rwvProg. -Eval cbn in (LL.interp' (fun x => Some (rwv 0 666 666)%Z) SimpleExample.SimplePipeline.rwvProg). - -Transparent toT fromT LLConversions.convertArg. -Eval cbv in (LL.interp' (fun x => Some (rwv 0 666 666)%Z) SimpleExample.SimplePipeline.rwvProg). - -Eval cbv in (LL.interp' LLConversions.rangeOf (LL.Return (LL.Var 2%Z))). - -Eval cbv in (LL.interp' LLConversions.rangeOf SimpleExample.SimplePipeline.rwvProg). - -Eval cbv in SimpleExample.SimplePipeline.outputBounds. -Eval cbv in SimpleExample.SimplePipeline.valid. |