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
|
Require Import ZArith.
Require Import List. Import ListNotations.
Inductive Instruction : Type :=
| Nop
| Push (n : Z)
| BCall (n : Z) (* How many things to pass as arguments *)
| BRet
| Add
| Load
| Store.
Inductive OpCode : Type :=
| OpBCall
| OpBRet
| OpNop
| OpPush
| OpAdd
| OpLoad
| OpStore.
Definition opCodes := [
OpBCall;
OpBRet;
OpNop;
OpPush;
OpAdd;
OpLoad;
OpStore].
Definition opCode_eq_dec : forall o1 o2 : OpCode,
{o1 = o2} + {o1 <> o2}.
Proof. decide equality. Defined.
Definition opcode_of_instr (i : Instruction) : OpCode :=
match i with
| BCall _ => OpBCall
| BRet => OpBRet
| Push _ => OpPush
| Nop => OpNop
| Add => OpAdd
| Load => OpLoad
| Store => OpStore
end.
|
