diff options
| author |  Robert Sloan <varomodt@google.com> | 2016-10-21 14:12:55 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@google.com> | 2016-10-21 14:12:55 -0700 |
| commit | 8ff79580fc6b473d15fcc566aca5b3045d0e64c0 (patch) | |
| tree | b703ea930e2ad8d739352c6d2b9c598b7a34dc96 /src/Assembly | |
| parent | eed4e2ee6d6a60268c6729920613962ff3fc5285 (diff) | |
| parent | cd5c85c08274b6d3cbb646247c3017c1639944e2 (diff) | |
merge rsloan-phoas refactors into master
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/GF25519.v | 1 | ||||
| -rw-r--r-- | src/Assembly/Pipeline.v | 18 |
2 files changed, 19 insertions, 0 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 605bcfd2e..091aa8008 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -20,6 +20,7 @@ Module GF25519. Section DefaultBounds. Import ListNotations. + Local Notation rr exp := (2^exp + 2^exp/10)%Z. Definition feBound: list Z := diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 31988ab10..472162716 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -99,3 +99,21 @@ 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. |