-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathconcrete_interpreter.v
211 lines (168 loc) · 6.25 KB
/
concrete_interpreter.v
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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
Require Import Arith.
Require Import Nat.
Require Import Bool.
Require Import bbv.Word.
Require Import Coq.NArith.NArith.
Require Import List.
Import ListNotations.
Require Import FORVES2.constants.
Import Constants.
Require Import FORVES2.program.
Import Program.
Require Import FORVES2.execution_state.
Import ExecutionState.
Require Import FORVES2.stack_operation_instructions.
Import StackOpInstrs.
Require Import FORVES2.misc.
Import Misc.
Module ConcreteInterpreter.
Definition push_c (v : EVMWord) (st : state) (ops : stack_op_instr_map) : option state :=
let stk := get_stack_st st in
match push v stk with
| None => None
| Some stk' => Some (set_stack_st st stk')
end.
Definition metapush_c (v1 v2 : N) (st : state) (ops : stack_op_instr_map) : option state :=
let stk := get_stack_st st in
let tags := (get_tags_exts (get_externals_st st)) in
let v' := tags v1 v2 in
match push v' stk with
| None => None
| Some stk' => Some (set_stack_st st stk')
end.
Definition pop_c (st : state) (ops : stack_op_instr_map): option state := let stk := get_stack_st
st in match pop stk with | None => None | Some stk' => Some
(set_stack_st st stk') end.
Definition dup_c (k : nat) (st : state) (ops : stack_op_instr_map) : option state :=
let stk := get_stack_st st in
match dup k stk with
| None => None
| Some stk' => Some (set_stack_st st stk')
end.
Definition swap_c (k : nat) (st : state) (ops : stack_op_instr_map) : option state :=
let stk := get_stack_st st in
match swap k stk with
| None => None
| Some stk' => Some (set_stack_st st stk')
end.
Fixpoint mload'' (mem : memory) (offset : N) (n: nat) : word (n*8) :=
match n with
| O => WO : word (0*8)
| S n' => bbv.Word.combine (mem offset) (mload'' mem (offset + 1)%N n')
end.
Definition mload' (mem : memory) (offset : EVMWord) (n: nat) : word (n*8) :=
mload'' mem (wordToN offset) n.
Definition mload (mem : memory) (offset : EVMWord) : EVMWord :=
mload' mem offset 32.
Definition split1_byte {sz : nat} (w : word ((S sz)*8)) : word ((S 0)*8) :=
split1 8 (sz*8) w.
Definition split2_byte {sz : nat} (w : word ((S sz)*8)):=
split2 8 (sz*8) w.
Fixpoint mstore' {sz : nat} (mem : memory) : (word (sz*8)) -> N -> memory :=
match sz with
| O => fun _ _ => mem
| S sz1' =>
fun value offset =>
let mem' := mstore' mem (split2_byte value) (offset+1)%N in
let byte := split1_byte value in (* split1 8 (8*sz1') value in *)
fun offset' => if (offset' =? offset)%N then byte else mem' offset'
end.
Definition mstore {sz : nat} (mem : memory) (value : word (sz*8)) (offset: EVMWord) : memory :=
mstore' mem value (wordToN offset).
Definition sload (strg : storage) (key : EVMWord) := strg (wordToN key).
Definition sstore (strg : storage) (key : EVMWord) (value : EVMWord) :=
let nkey := (wordToN key) in
fun key' => if (key' =? nkey)%N then value else strg key'.
Definition mload_c (st : state) (ops : stack_op_instr_map) : option state :=
match get_stack_st st with
| offset::stk => let v := mload (get_memory_st st) offset in
let st' := set_stack_st st (v::stk) in
Some st'
| _ => None
end.
Definition mstore8_c (st : state) (ops : stack_op_instr_map) : option state :=
match get_stack_st st with
| offset::value::stk =>
let mem := mstore (get_memory_st st) (split1_byte (value: word ((S (pred BytesInEVMWord))*8))) offset in
let st' := set_memory_st st mem in
let st'' := set_stack_st st' stk in
Some st''
| _ => None
end.
Definition mstore_c (st : state) (ops : stack_op_instr_map) : option state :=
match get_stack_st st with
| offset::value::stk =>
let mem := mstore (get_memory_st st) value offset in
let st' := set_memory_st st mem in
let st'' := set_stack_st st' stk in Some st''
| _ => None
end.
Definition sload_c (st : state) (ops : stack_op_instr_map) : option state :=
match get_stack_st st with
| key::stk =>
let v := sload (get_storage_st st) key in
let st' := set_stack_st st (v::stk) in
Some st'
| _ => None
end.
Definition sstore_c (st : state) (ops : stack_op_instr_map) : option state :=
match get_stack_st st with
| key::value::stk =>
let strg := sstore (get_storage_st st) key value in
let st' := set_store_st st strg in
let st'' := set_stack_st st' stk in
Some st''
| _ => None
end.
(* just return 0 for now *)
Definition sha3_c (st : state) (ops : stack_op_instr_map) : option state :=
match get_stack_st st with
| offset::size::stk =>
let f := (get_sha3_info_op (get_keccak256_exts (get_externals_st st))) in
let v := f (wordToNat size) (mload' (get_memory_st st) offset (wordToNat size)) in
let st' := set_stack_st st (v::stk) in
Some st'
| _ => None
end.
Definition exec_stack_op_intsr_c (label : stack_op_instr) (st : state) (ops : stack_op_instr_map) : option state :=
match (ops label) with
| OpImp nb_args func _ _ =>
let stk := get_stack_st st in
match firstn_e nb_args stk with
| None => None
| Some args => match skipn_e nb_args stk with
| None => None
| Some stk' =>
let v := func (get_externals_st st) args in
let st':= set_stack_st st (v :: stk') in
Some st'
end
end
end.
(* Concrete interpreter *)
Definition evm_exec_instr_c (inst : instr) (st: state) (ops : stack_op_instr_map) : option state :=
match inst with
| PUSH size v => push_c (NToWord EVMWordSize v) st ops
| METAPUSH cat v => metapush_c cat v st ops
| POP => pop_c st ops
| DUP k => dup_c k st ops
| SWAP k => swap_c k st ops
| MLOAD => mload_c st ops
| MSTORE8 => mstore8_c st ops
| MSTORE => mstore_c st ops
| SLOAD => sload_c st ops
| SSTORE => sstore_c st ops
| SHA3 => sha3_c st ops
| KECCAK256 => sha3_c st ops
| OpInstr label => exec_stack_op_intsr_c label st ops
end.
Fixpoint evm_exec_block_c (p : block) (st : state) (ops : stack_op_instr_map) : option state :=
match p with
| [] => Some st
| instr::instrs' =>
match evm_exec_instr_c instr st ops with
| None => None
| Some st' => evm_exec_block_c instrs' st' ops
end
end.
End ConcreteInterpreter.