diff options
author | Robert Sloan <varomodt@google.com> | 2016-10-18 22:07:24 -0700 |
---|---|---|
committer | Robert Sloan <varomodt@google.com> | 2016-10-18 22:07:24 -0700 |
commit | ff878dbde61374e42235b10d85c5fec2ab22e7d1 (patch) | |
tree | 4151a06594a82b21300c6dbcb6485497ca2c9d1d /src/Assembly/Pipeline.v | |
parent | f8680ec8e73f8acb39cb55f6e616a0e5d10347f8 (diff) |
Fast bounds-checking machinery but lower-bounds are broken
Diffstat (limited to 'src/Assembly/Pipeline.v')
-rw-r--r-- | src/Assembly/Pipeline.v | 33 |
1 files changed, 19 insertions, 14 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 87fc8cc92..e7fc23e0a 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -1,4 +1,5 @@ Require Export Crypto.Assembly.QhasmCommon. + Require Export Crypto.Assembly.PhoasCommon. Require Export Crypto.Assembly.HL. Require Export Crypto.Assembly.LL. @@ -21,7 +22,7 @@ Module Type Expression. Parameter inputs: nat. Parameter ResultType: type. Parameter hlProg: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType). - Parameter inputBounds: list (@BoundedWord bits). + Parameter inputBounds: list (Range N). End Expression. Module Pipeline (Input: Expression). @@ -42,28 +43,32 @@ Module Pipeline (Input: Expression). | None => None end. - Definition B: Type := option (@BoundedWord bits). + Import LLConversions. + + Definition RWV: Type := option RangeWithValue. - Definition boundedProg: NAry inputs B (@LL.expr B B ResultType) := - NArgMap (fun x => - orElse (Z.of_N (N.pred (Npow2 bits))) - (option_map Z.of_N (option_map Evaluables.high x))) ( - liftN (LLConversions.convertZToBounded bits) llProg). + Definition rwvProg: NAry inputs RWV (@LL.expr RWV RWV ResultType) := + NArgMap (fun x => orElse 0%Z (option_map (fun v => Z.of_N (value v)) x) ) ( + liftN (@convertExpr Z RWV ZEvaluable (RWVEval (n := bits)) _) llProg). - Fixpoint valid' {T k} ins (f: NAry k B T) := - match k as k' return NAry k' B T -> T with + 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 | O => id | S m => fun f' => match ins with - | cons x xs => @valid' _ m xs (f' x) - | nil => @valid' _ m nil (f' None) + | cons x xs => @applyProgOn A B m xs (f' x) + | nil => @applyProgOn A B m nil (f' None) end end f. - Definition outputBounds := valid' (map (@Some _) inputBounds) boundedProg. + Definition outputBounds := + applyProgOn (map (@Some _) (map from_range inputBounds)) ( + liftN (fun e => typeMap (option_map proj) (@LL.interp RWV (@RWVEval bits) _ e)) + rwvProg). Definition valid := - valid' (map (@Some _) inputBounds) (liftN (LLConversions.check) boundedProg). + applyProgOn (map (@Some _) (map from_range inputBounds)) ( + liftN (@check bits _ RWV (@RWVEval bits)) rwvProg). End Pipeline. Module SimpleExample. @@ -78,7 +83,7 @@ Module SimpleExample. Definition hlProg: NAry 1 Z (@HL.expr Z (@LL.arg Z Z) TT) := Eval vm_compute in (fun x => HL.Binop OPadd (HL.Const x) (HL.Const 5%Z)). - Definition inputBounds: list (@BoundedWord bits) := [ any ]. + Definition inputBounds: list (Range N) := [ range N 0%N (Npow2 31) ]. End SimpleExpression. Module SimplePipeline := Pipeline SimpleExpression. |