5 files changed, 161 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
diff --git a/src/Assembly/.#QhasmExtraction.v b/src/Assembly/.#QhasmExtraction.v
new file mode 120000
index 000000000..74379fe2d
--- /dev/null
+++ b/src/Assembly/.#QhasmExtraction.v
@@ -0,0 +1 @@
+varomodt@dhcp-18-189-8-224.dyn.MIT.EDU.19197
+\ No newline at end of file
diff --git a/src/Assembly/HighLevel.v b/src/Assembly/HighLevel.v
new file mode 100644
index 000000000..bae67f312
--- /dev/null
+++ b/src/Assembly/HighLevel.v
@@ -0,0 +1,9 @@
+
+Inductive Const32 : Set = | const32: word 32 -> Const32.
+
+Inductive HL :=
+  | Input: Const32 -> HL
+  | Variable: Const32 -> HL
+  | Let: forall m, nat -> HL -> HL -> HL
+  | Lift1: (Const32 -> Const32) -> HL -> HL
+  | Lift2: (Const32 -> Const32 -> Const32) -> HL -> HL -> HL.
diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v
new file mode 100644
index 000000000..f30d10e94
--- /dev/null
+++ b/src/Assembly/Qhasm.v
@@ -0,0 +1,102 @@
+
+Require Import String.
+
+Inductive Const32 : Set = | const32: word 32 -> Const32.
+
+Inductive Reg (len: nat) : Set =
+  | reg32: string -> Reg 32
+  | reg3232: string -> Reg 64
+  | reg6464: string -> Reg 128
+  | float80: string -> Reg 80.
+
+Inductive Stack (len: nat) : Set =
+  | stack32: string -> Stack 32.
+  | stack64: string -> Stack 64.
+  | stack128: string -> Stack 128.
+
+Definition Index (limit: nat) := {x: nat | x < limit}.
+
+Inductive Assignment : Set :=
+  | Assign32Stack32: Reg 32 -> Stack32 -> Assignment
+  | Assign32Stack16: Reg 32 -> Stack32 -> Index 2 -> Assignment
+  | Assign32Stack8: Reg 32 -> Stack32 -> Index 4 -> Assignment
+  | Assign32Stack64: Reg 32 -> Stack64 -> Index 2 -> Assignment
+  | Assign32Stack128: Reg 32 -> Stack128 -> Index 2 -> Assignment
+
+  | Assign32Reg32: Reg 32 -> Reg 32 -> Assignment
+  | Assign32Reg16: Reg 32 -> Reg 32 -> Index 2 -> Assignment
+  | Assign32Reg8: Reg 32 -> Reg 32 -> Index 4 -> Assignment
+  | Assign32Reg64: Reg 32 -> Reg64 -> Index 2 -> Assignment
+  | Assign32Reg128: Reg 32 -> Reg 128 -> Index 4 -> Assignment
+
+  | Assign3232Stack32: Reg 64 -> Index 2 -> Stack32 -> Assignment
+  | Assign3232Stack64: Reg 64 -> Stack64 -> Assignment
+  | Assign3232Stack128: Reg 64 -> Stack128 -> Index 2 -> Assignment
+
+  | Assign3232Reg32: Reg 64 -> Index 2 -> Reg 32 -> Assignment
+  | Assign3232Reg64: Reg 64 -> Reg64 -> Assignment
+  | Assign3232Reg128: Reg 64 -> Reg 128 -> M 2 -> Assignment
+
+  | AssignConstant: Reg 32 -> Const32 -> Assignment
+  | AssignPtr: Reg 32 -> Stack64.
+
+Hint Constructors Assignment.
+                          
+Inductive BinOp :=
+  | Plus: BinOp | Minus: BinOp | Mult: BinOp
+  | Div: BinOp | Xor: BinOp | And: BinOp.
+
+Inductive RotOp :=
+  | Shl: NatOp | Shr: NatOp | Rotl: NatOp | Rotr: NatOp.
+
+Inductive Operation :=
+  | OpReg32Constant: BinOp -> Reg 32 -> Const32 -> Operation
+  | OpReg32Reg32: BinOp -> Reg 32 -> Reg 32 -> Operation
+  | RotReg32: RotOp -> Reg 32 -> Index 32 -> Operation
+
+  | OpReg64Constant: BinOp -> Reg 32 -> Const32 -> Operation
+  | OpReg64Reg64: BinOp -> Reg 64 -> Reg 64 -> Operation
+
+  | OpReg128Constant: BinOp -> Reg 128 -> Const32 -> Operation
+  | OpReg128Reg128: BinOp -> Reg 128 -> Reg 128 -> Operation.
+
+Hint Constructors Operation.
+
+Inductive TestOp :=
+  | Eq: TestOp
+  | Lt: TestOp
+  | UnsignedLt: TestOp
+  | Gt: TestOp
+  | UnsignedGt: TestOp.
+
+Definition Invert := bool.
+
+Definition Conditional :=
+  | TestReg32Reg32: TestOp -> Invert -> Reg 32 -> Reg 32 -> Conditional
+  | TestReg32Const: TestOp -> Invert -> Reg 32 -> W -> Conditional.
+
+Hint Constructors Conditional.
+
+Definition Label := nat.
+
+Inductive AlmostQhasm :=
+  | QSeq: AlmostQhasm -> AlmostQhasm -> AlmostQhasm
+  | QAssign: Assignment -> AlmostQhasm
+  | QOp: Operation -> AlmostQhasm 
+  | QCond: Conditional -> AlmostQhasm -> AlmostQhasm -> AlmostQhasm
+  | QWhile: Conditional -> AlmostQhasm -> AlmostQhasm
+
+Hint Constructors AlmostQhasm.
+
+Inductive Qhasm :=
+  | QSeq: Qhasm -> Qhasm -> Qhasm
+  | QAssign: Assignment -> Qhasm
+  | QOp: Operation -> Qhasm
+  | QCond: Conditional -> Qhasm -> Qhasm -> Qhasm
+  | QWhile: Conditional -> Qhasm -> Qhasm
+
+Hint Constructors Qhasm.
+
+(* evalReg: Qhasm -> Reg 32 -> Reg 32
+   evalStack: Qhasm -> Stack32 -> Stack32 *)
+
diff --git a/src/Assembly/QhasmExtraction.v b/src/Assembly/QhasmExtraction.v
new file mode 100644
index 000000000..d773bbc65
--- /dev/null
+++ b/src/Assembly/QhasmExtraction.v
@@ -0,0 +1,25 @@
+
+
+
+(*
+- 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