1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
Require Export Coq.Strings.String Coq.Lists.List Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith.
Require Export Bedrock.Word.
(* Utilities *)
Definition Label := nat.
Definition Index (limit: nat) := {x: nat | (x <= (pred limit))%nat}.
Coercion indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
Fixpoint NAry (n: nat) (A: Type) (B: Type): Type :=
match n with
| (S m) => A -> NAry m A B
| O => B
end.
Fixpoint liftN {n A B C} (f: B -> C) (x: NAry n A B) {struct n}: NAry n A C :=
match n as n' return NAry n' A B -> NAry n' A C with
| S m => fun x' => (fun arg => liftN f (x' arg))
| O => f
end x.
Fixpoint NArgMap {n A B C} (f: A -> B) (x: NAry n B C) {struct n}: NAry n A C :=
match n as n' return NAry n' B C -> NAry n' A C with
| S m => fun x' => (fun arg => NArgMap f (x' (f arg)))
| O => id
end x.
Inductive Either A B :=
| xleft: A -> Either A B
| xright: B -> Either A B.
Definition convert {A B: Type} (x: A) (H: A = B): B :=
eq_rect A (fun B0 : Type => B0) x B H.
(* Asm Types *)
Inductive Width: nat -> Type := | W32: Width 32 | W64: Width 64.
(* A constant value *)
Inductive Const: nat -> Type :=
| constant: forall {n}, Width n -> word n -> Const n.
(* A variable in any register *)
Inductive Reg: nat -> Type :=
| reg: forall {n}, Width n -> nat -> Reg n.
(* A variable on the stack. We should use this sparingly. *)
Inductive Stack: nat -> Type :=
| stack: forall {n}, Width n -> nat -> Stack n.
(* A pointer to a memory block. Called as:
mem width index length
where length is in words of size width.
All Mem pointers will be declared as Stack arguments in the
resulting qhasm output *)
Inductive Mem: nat -> nat -> Type :=
| mem: forall {n m}, Width n -> nat -> Mem n m.
(* The state of the carry flag:
1 = Some true
0 = Some false
unknown = None *)
Definition Carry := option bool.
(* Assignments *)
Inductive Assignment : Type :=
| ARegMem: forall {n m}, Reg n -> Mem n m -> Index m -> Assignment
| AMemReg: forall {n m}, Mem n m -> Index m -> Reg n -> Assignment
| AStackReg: forall {n}, Stack n -> Reg n -> Assignment
| ARegStack: forall {n}, Reg n -> Stack n -> Assignment
| ARegReg: forall {n}, Reg n -> Reg n -> Assignment
| AConstInt: forall {n}, Reg n -> Const n -> Assignment.
(* Operations *)
Inductive IntOp :=
| IAdd: IntOp
| ISub: IntOp
| IXor: IntOp
| IAnd: IntOp
| IOr: IntOp.
Inductive CarryOp := | AddWithCarry: CarryOp.
Inductive DualOp := | Mult: DualOp.
Inductive RotOp := | Shl: RotOp | Shr: RotOp.
Inductive Operation :=
| IOpConst: forall {n}, IntOp -> Reg n -> Const n -> Operation
| IOpReg: forall {n}, IntOp -> Reg n -> Reg n -> Operation
| IOpMem: forall {n m}, IntOp -> Reg n -> Mem n m -> Index m -> Operation
| IOpStack: forall {n}, IntOp -> Reg n -> Stack n -> Operation
| DOp: forall {n}, DualOp -> Reg n -> Reg n -> option (Reg n) -> Operation
| ROp: forall {n}, RotOp -> Reg n -> Index n -> Operation
| COp: forall {n}, CarryOp -> Reg n -> Reg n -> Operation.
(* Control Flow *)
Inductive TestOp :=
| TEq: TestOp | TLt: TestOp | TLe: TestOp
| TGt: TestOp | TGe: TestOp.
Inductive Conditional :=
| CTrue: Conditional
| CZero: forall n, Reg n -> Conditional
| CReg: forall n, TestOp -> Reg n -> Reg n -> Conditional
| CConst: forall n, TestOp -> Reg n -> Const n -> Conditional.
(* Generalized Variable Entry *)
Inductive Mapping (n: nat) :=
| regM: forall (r: Reg n), Mapping n
| stackM: forall (s: Stack n), Mapping n
| memM: forall {m} (x: Mem n m) (i: Index m), Mapping n
| constM: forall (x: Const n), Mapping n.
(* Parameter Accessors *)
Definition constWidth {n} (x: Const n): nat := n.
Definition regWidth {n} (x: Reg n): nat := n.
Definition stackWidth {n} (x: Stack n): nat := n.
Definition memWidth {n m} (x: Mem n m): nat := n.
Definition memLength {n m} (x: Mem n m): nat := m.
Definition constValueW {n} (x: Const n): word n :=
match x with | @constant n _ v => v end.
Definition constValueN {n} (x: Const n): nat :=
match x with | @constant n _ v => wordToNat v end.
Definition regName {n} (x: Reg n): nat :=
match x with | @reg n _ v => v end.
Definition stackName {n} (x: Stack n): nat :=
match x with | @stack n _ v => v end.
Definition memName {n m} (x: Mem n m): nat :=
match x with | @mem n m _ v => v end.
(* Hints *)
Hint Constructors
Reg Stack Const Mem Mapping
Assignment Operation Conditional.
|
