blob: 472162716e5b523f93a1aaf14f29e1d45c686366 (
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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
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 (@interp_type Z) ResultType).
Parameter inputBounds: list Z.
End Expression.
Module Pipeline (Input: Expression).
Export Input.
Module Util.
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.
End Util.
Definition hlProg': 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)) hlProg.
Definition llProg: NAry inputs Z (@LL.expr Z Z ResultType) :=
liftN CompileHL.compile hlProg'.
Definition wordProg: NAry inputs Z (@CompileLL.WExpr bits ResultType) :=
liftN (LLConversions.ZToWord (n := bits) Z) 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.
Instance RWVEvaluable : Evaluable RWV := @RWVEvaluable bits.
Existing Instance RWVEvaluable.
Definition rwvProg: @LL.expr RWV Z ResultType :=
Util.applyProgOn (map (@Some _) inputBounds) (
NArgMap (orElse 0%Z) (
liftN (@convertExpr Z RWV (@ZEvaluable bits) _ _ _)
llProg)).
Definition outputBounds :=
typeMap (option_map rwvToRange) (
LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x))) (
rwvProg)).
Definition valid := check (n := 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 (@interp_type Z) TT) :=
Eval vm_compute in (fun x => HL.Binop OPadd (HL.Var x) (HL.Const 5%Z)).
Definition inputBounds: list Z := [ (2^30)%Z ].
End SimpleExpression.
Module SimplePipeline := Pipeline SimpleExpression.
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.
|
