Simpler QhasmCommon grammar

1 files changed, 23 insertions, 55 deletions

diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 46e2664ad..4c9022d21 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -1,4 +1,4 @@
-Require Export String List.
+Require Export String List NPeano.
 Require Export Bedrock.Word.
 
 (* A formalization of x86 qhasm *)
@@ -16,67 +16,43 @@ Inductive Const: nat -> Set :=
   | const128: word 128 -> Const 128.
 
 Inductive Reg: nat -> Set :=
-  | reg32: nat -> Reg 32
-  | reg3232: nat -> Reg 64
-  | reg6464: nat -> Reg 128
-  | reg80: nat -> Reg 80.
+  | reg32: nat -> Reg 32.
 
 Inductive Stack: nat -> Set :=
   | stack32: nat -> Stack 32
   | stack64: nat -> Stack 64
-  | stack128: nat -> Stack 128
-  | stack256: nat -> Stack 256
-  | stack512: nat -> Stack 512.
+  | stack128: nat -> Stack 128.
+
+Definition CarryState := option bool.
 
 (* Assignments *)
 Inductive Assignment : Set :=
-  | Assign32Stack32: Reg 32 -> Stack 32 -> Assignment
-  | Assign32Stack16: Reg 32 -> Stack 32 -> Index 2 -> Assignment
-  | Assign32Stack8: Reg 32 -> Stack 32 -> Index 4 -> Assignment
-  | Assign32Stack64: Reg 32 -> Stack 64 -> Index 2 -> Assignment
-  | Assign32Stack128: Reg 32 -> Stack 128 -> 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 -> Reg 64 -> Index 2 -> Assignment
-  | Assign32Reg128: Reg 32 -> Reg 128 -> Index 4 -> Assignment
-
-  | Assign3232Stack32: Reg 64 -> Index 2 -> Stack 32 -> Assignment
-  | Assign3232Stack64: Reg 64 -> Stack 64 -> Assignment
-  | Assign3232Stack128: Reg 64 -> Stack 128 -> Index 2 -> Assignment
-
-  | Assign3232Reg32: Reg 64 -> Index 2 -> Reg 32 -> Assignment
-  | Assign3232Reg64: Reg 64 -> Reg 64 -> Assignment
-  | Assign3232Reg128: Reg 64 -> Reg 128 -> Index 2 -> Assignment
-
-  | Assign6464Reg32: Reg 128 -> Index 4 -> Reg 32 -> Assignment
-  | Assign6464Reg64: Reg 128 -> Index 2 -> Reg 64 -> Assignment
-  | Assign6464Reg128: Reg 128 -> Reg 128 -> Assignment
-
-  | AssignConstant: Reg 32 -> Const 32 -> Assignment.
+  | AStack: forall n, Reg n -> Stack n -> Assignment
+  | AReg: forall n, Reg n -> Reg n -> Assignment
+  | AIndex: forall n m, Reg n -> Reg m -> Index (n/m)%nat -> Assignment
+  | AConst: forall n, Reg n -> Const n -> Assignment
+  | APtr: forall n, Reg 32 -> Stack n -> Assignment.
 
 Hint Constructors Assignment.
 
 (* Operations *)
 
-Inductive BinOp :=
-  | Plus: BinOp | Minus: BinOp | Mult: BinOp
-  | Div: BinOp | Xor: BinOp | And: BinOp | Or: BinOp.
-
-Inductive RotOp :=
-  | Shl: RotOp | Shr: RotOp | Rotl: RotOp | Rotr: RotOp.
+Inductive QOp :=
+  | QPlus: QOp | QMinus: QOp | QIMult: QOp
+  | QXor: QOp | QAnd: QOp | QOr: QOp.
 
-Inductive Operation :=
-  | OpReg32Constant: BinOp -> Reg 32 -> Const 32 -> Operation
-  | OpReg32Reg32: BinOp -> Reg 32 -> Reg 32 -> Operation
-  | RotReg32: RotOp -> Reg 32 -> Index 32 -> Operation
+Inductive QFixedOp :=
+  | QMult: QFixedOp | UDiv: QFixedOp.
 
-  | OpReg64Constant: BinOp -> Reg 64 -> Const 64 -> Operation
-  | OpReg64Reg64: BinOp -> Reg 64 -> Reg 64 -> Operation
+Inductive QRotOp :=
+  | Shl: QRotOp | Shr: QRotOp | QRotl: QRotOp | QRotr: QRotOp.
 
-  | OpReg128Constant: BinOp -> Reg 128 -> Const 32 -> Operation
-  | OpReg128Reg128: BinOp -> Reg 128 -> Reg 128 -> Operation.
+Inductive Operation :=
+  | OpConst: QOp -> Reg 32 -> Const 32 -> Operation
+  | OpReg: QOp -> Reg 32 -> Reg 32 -> Operation
+  | OpFixedConst: QFixedOp -> Reg 32 -> Const 32 -> Operation
+  | OpFixedReg: QFixedOp -> Reg 32 -> Reg 32 -> Operation
+  | OpRot: QRotOp -> Reg 32 -> Index 32 -> Operation.
 
 Hint Constructors Operation.
 
@@ -110,9 +86,6 @@ Hint Constructors Conditional.
 Definition getRegWords {n} (x: Reg n) :=
   match x with
   | reg32 loc => 1
-  | reg3232 loc => 2
-  | reg6464 loc => 4
-  | reg80 loc => 2
   end.
 
 Definition getStackWords {n} (x: Stack n) :=
@@ -120,8 +93,6 @@ Definition getStackWords {n} (x: Stack n) :=
   | stack32 loc => 1
   | stack64 loc => 2
   | stack128 loc => 4
-  | stack256 loc => 8
-  | stack512 loc => 16
   end.
 
 Definition getRegIndex {n} (x: Reg n): nat :=
@@ -129,7 +100,6 @@ Definition getRegIndex {n} (x: Reg n): nat :=
   | reg32 loc => loc
   | reg3232 loc => loc
   | reg6464 loc => loc
-  | reg80 loc => loc
   end.
 
 Definition getStackIndex {n} (x: Stack n): nat :=
@@ -137,8 +107,6 @@ Definition getStackIndex {n} (x: Stack n): nat :=
   | stack32 loc => loc
   | stack64 loc => loc
   | stack128 loc => loc
-  | stack256 loc => loc
-  | stack512 loc => loc
   end.
 
 (* For register allocation checking *)