diff options
| author |  Robert Sloan <varomodt@google.com> | 2016-10-13 19:32:04 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@google.com> | 2016-10-13 19:32:04 -0700 |
| commit | fd3165c23f43d006e2e67be9ac8f600eb2e1feef (patch) | |
| tree | d45b0c72a782dc9511851d189d33b3e688f86d7e /src/Assembly/Pipeline.v | |
| parent | e1e8685f531fcd6975a09717e93de895902a6536 (diff) | |
Well, here's the program instance. The string conversion is still running.
Diffstat (limited to 'src/Assembly/Pipeline.v')
| -rw-r--r-- | src/Assembly/Pipeline.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 765bd58f8..306288c7d 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -127,18 +127,19 @@ Module GF25519. Definition llProg: NAry 80 Z (@LL.expr Z Z ResultType) := Eval vm_compute in (liftN CompileHL.compile hlProg). + (* Don't vm_compute because it'll stack overflow (!!) *) Definition wordProg: NAry 80 (@CompileLL.WArg bits TT) (@LL.expr _ _ ResultType) := - Eval vm_compute in (NArgMap (fun x => Z.of_N (wordToN (LL.interp_arg (t := TT) x))) ( - liftN (LLConversions.convertZToWord bits) llProg)). + NArgMap (fun x => Z.of_N (wordToN (LL.interp_arg (t := TT) x))) ( + liftN (LLConversions.convertZToWord bits) llProg). Definition qhasmProg := Eval vm_compute in (CompileLL.compile (w := width) wordProg). Definition qhasmString: option string := - Eval vm_compute in (match qhasmProg with + match qhasmProg with | Some (p, _) => StringConversion.convertProgram p | None => None - end). + end. Section BoundsCheck. Definition R := @WordRangeOpt bits. |