diff options
Diffstat (limited to 'src/Assembly/#QhasmExtraction.v#')
-rw-r--r-- | src/Assembly/#QhasmExtraction.v# | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/Assembly/#QhasmExtraction.v# b/src/Assembly/#QhasmExtraction.v# new file mode 100644 index 000000000..0584553fc --- /dev/null +++ b/src/Assembly/#QhasmExtraction.v# @@ -0,0 +1,24 @@ + + +(* +- Define an evaluation function over the QH type, which can be terribly inefficient. This function will be parametrized in the following way: + + evalReg x InputRegs OutputRegs + evalStack x InputStack OutputStack + +Then, produce a lemma which shows that evaluating a given QH will perform an appropriate register operation. This will not check side-effects, which should be okay since we’re synthesizing in a very controlled manner. + +- Work on {x: QH | eval x _ _ = AST}, like the bounding code + +- Introduce all Inputs as StackX + +- Replace upward as: + + + Lifted functions by lemma (as above) + + Conditionals as QCond, by lemma + +- Then we can convert to string: + + + We can introduce stack inputs, etc. by traversing the AST + + QSeq, QStatement, QAssign are convertible directly + + QCond, QWhile are fixed assembly wrappers *)
\ No newline at end of file |