aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/#QhasmExtraction.v#
diff options
context:
space:
mode:
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