diff options
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. |