blob: e7fc23e0a874c7e75503c878ca417227bc5b52ca (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
Require Export Crypto.Assembly.QhasmCommon.
Require Export Crypto.Assembly.PhoasCommon.
Require Export Crypto.Assembly.HL.
Require Export Crypto.Assembly.LL.
Require Export Crypto.Assembly.Compile.
Require Export Crypto.Assembly.Conversions.
Require Export Crypto.Assembly.StringConversion.
Require Export Crypto.Assembly.State.
Require Export Crypto.Util.Notations.
Require Export Crypto.Util.LetIn.
Require Export Coq.ZArith.BinInt.
Require Export ExtrOcamlBasic.
Require Export ExtrOcamlString.
Module Type Expression.
Parameter bits: nat.
Parameter width: Width bits.
Parameter inputs: nat.
Parameter ResultType: type.
Parameter hlProg: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType).
Parameter inputBounds: list (Range N).
End Expression.
Module Pipeline (Input: Expression).
Export Input.
Definition llProg: NAry inputs Z (@LL.expr Z Z ResultType) :=
liftN CompileHL.compile hlProg.
Definition wordProg: NAry inputs (@CompileLL.WArg bits TT) (@LL.expr _ _ ResultType) :=
NArgMap (fun x => Z.of_N (wordToN (LL.interp_arg (t := TT) x))) (
liftN (LLConversions.convertZToWord bits) llProg).
Definition qhasmProg := CompileLL.compile (w := width) wordProg.
Definition qhasmString : option string :=
match qhasmProg with
| Some (p, _) => StringConversion.convertProgram p
| None => None
end.
Import LLConversions.
Definition RWV: Type := option RangeWithValue.
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 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 => @applyProgOn A B m xs (f' x)
| nil => @applyProgOn A B m nil (f' None)
end
end f.
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 :=
applyProgOn (map (@Some _) (map from_range inputBounds)) (
liftN (@check bits _ RWV (@RWVEval bits)) rwvProg).
End Pipeline.
Module SimpleExample.
Module SimpleExpression <: Expression.
Import ListNotations.
Definition bits: nat := 32.
Definition width: Width bits := W32.
Definition inputs: nat := 1.
Definition ResultType := TT.
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 (Range N) := [ range N 0%N (Npow2 31) ].
End SimpleExpression.
Module SimplePipeline := Pipeline SimpleExpression.
Export SimplePipeline.
End SimpleExample.
|
