-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsstack_val_cmp_impl.v
215 lines (190 loc) · 9.52 KB
/
sstack_val_cmp_impl.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
212
213
214
215
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.
Require Import FORVES2.symbolic_state.
Import SymbolicState.
Require Import FORVES2.symbolic_state_eval.
Import SymbolicStateEval.
Require Import FORVES2.valid_symbolic_state.
Import ValidSymbolicState.
Require Import FORVES2.valid_symbolic_state.
Import ValidSymbolicState.
Require Import FORVES2.symbolic_state_cmp.
Import SymbolicStateCmp.
Require Import FORVES2.eval_common.
Import EvalCommon.
Require Import FORVES2.symbolic_state_dec.
Import SymbolicStateDec.
Require Import FORVES2.constraints.
Import Constraints.
Require Import FORVES2.context.
Import Context.
Module SStackValCmpImpl.
Definition trivial_compare_sstack_val (smemory_cmp: smemory_cmp_ext_t) (sstorage_cmp: sstorage_cmp_ext_t) (sha3_cmp: sha3_cmp_ext_t) (d: nat) (ctx: ctx_t) (sv1 sv2: sstack_val) (maxidx1: nat) (sb1: sbindings) (maxidx2: nat) (sb2: sbindings) (ops: stack_op_instr_map) : bool :=
match d with
| 0 => false
| S d' =>
match sv1,sv2 with
| Val w1, Val w2 => weqb w1 w2
| InVar n1, InVar n2 => (n1 =? n2)
| FreshVar n1, FreshVar n2 =>
if (n1 =? n2)
then if (maxidx1 =? maxidx2)
then if (sbindings_eq_dec sb1 sb2)
then true
else false
else false
else false
| _, _ => false
end
end.
Fixpoint basic_compare_sstack_val (smemory_cmp: smemory_cmp_ext_t) (sstorage_cmp: sstorage_cmp_ext_t) (sha3_cmp: sha3_cmp_ext_t) (d: nat) (ctx: ctx_t) (sv1 sv2: sstack_val) (maxidx1: nat) (sb1: sbindings) (maxidx2: nat) (sb2: sbindings) (ops: stack_op_instr_map) : bool :=
match d with
| 0 => false
| S d' =>
let basic_compare_sstack_val_rec :=
basic_compare_sstack_val smemory_cmp sstorage_cmp sha3_cmp d' in
match follow_in_smap sv1 maxidx1 sb1 with
| None => false
| Some (FollowSmapVal smv1 maxidx1' sb1') =>
match follow_in_smap sv2 maxidx2 sb2 with
| None => false
| Some (FollowSmapVal smv2 maxidx2' sb2') =>
match smv1, smv2 with
| SymBasicVal sv1', SymBasicVal sv2' =>
match sv1',sv2' with
| Val w1, Val w2 => weqb w1 w2
| InVar n1, InVar n2 => if (n1 =? n2) then true else chk_eq_wrt_ctx ctx sv1' sv2'
| _, _ => chk_eq_wrt_ctx ctx sv1' sv2'
end
| SymMETAPUSH cat1 v1, SymMETAPUSH cat2 v2 => andb (cat1 =? cat2)%N (v1 =? v2)%N
| SymOp label1 args1, SymOp label2 args2 =>
if label1 =?i label2 then
match ops label1 with
OpImp _ _ H_Comm _ =>
match (fold_right_two_lists (fun e1 e2 => basic_compare_sstack_val_rec ctx e1 e2 maxidx1' sb1' maxidx2' sb2' ops) args1 args2) with
| true => true
| false =>
match H_Comm with
| Some comm_proof =>
match args1, args2 with
| [a1;a2],[b1;b2] =>
if basic_compare_sstack_val_rec ctx a1 b2 maxidx1' sb1' maxidx2' sb2' ops
then basic_compare_sstack_val_rec ctx a2 b1 maxidx1' sb1' maxidx2' sb2' ops
else false
| _, _ => false
end
| None => false
end
end
end
else false
| SymMLOAD soffset1 smem1, SymMLOAD soffset2 smem2 =>
if basic_compare_sstack_val smemory_cmp sstorage_cmp sha3_cmp d' ctx soffset1 soffset2 maxidx1' sb1' maxidx2' sb2' ops
then smemory_cmp basic_compare_sstack_val_rec ctx smem1 smem2 maxidx1' sb1' maxidx2' sb2' ops
else false
| SymSLOAD skey1 sstrg1, SymSLOAD skey2 sstrg2 =>
if basic_compare_sstack_val smemory_cmp sstorage_cmp sha3_cmp d' ctx skey1 skey2 maxidx1' sb1' maxidx2' sb2' ops
then sstorage_cmp basic_compare_sstack_val_rec ctx sstrg1 sstrg2 maxidx1' sb1' maxidx2' sb2' ops
else false
| SymSHA3 soffset1 ssize1 smem1, SymSHA3 soffset2 ssize2 smem2 =>
(* the nested if is to avoid using band *)
if (if basic_compare_sstack_val_rec ctx soffset1 soffset2 maxidx1' sb1' maxidx2' sb2' ops then
if basic_compare_sstack_val_rec ctx ssize1 ssize2 maxidx1' sb1' maxidx2' sb2' ops then
smemory_cmp basic_compare_sstack_val_rec ctx smem1 smem2 maxidx1' sb1' maxidx2' sb2' ops
else
false
else
false)
then true
else
sha3_cmp basic_compare_sstack_val_rec ctx soffset1 ssize1 smem1 soffset2 ssize2 smem2 maxidx1' sb1' maxidx2' sb2' ops
| _, _ => false
end
end
end
end.
Fixpoint basic_compare_sstack_val_w_eq_chk (smemory_cmp: smemory_cmp_ext_t) (sstorage_cmp: sstorage_cmp_ext_t) (sha3_cmp: sha3_cmp_ext_t) (d: nat) (ctx: ctx_t) (sv1 sv2: sstack_val) (maxidx1: nat) (sb1: sbindings) (maxidx2: nat) (sb2: sbindings) (ops: stack_op_instr_map) : bool :=
if (trivial_compare_sstack_val smemory_cmp sstorage_cmp sha3_cmp d ctx sv1 sv2 maxidx1 sb1 maxidx2 sb2 ops)
then true
else
match d with
| 0 => false
| S d' =>
let basic_compare_sstack_val_w_eq_chk_rec :=
basic_compare_sstack_val_w_eq_chk smemory_cmp sstorage_cmp sha3_cmp d' in
match follow_in_smap sv1 maxidx1 sb1 with
| None => false
| Some (FollowSmapVal smv1 maxidx1' sb1') =>
match follow_in_smap sv2 maxidx2 sb2 with
| None => false
| Some (FollowSmapVal smv2 maxidx2' sb2') =>
match smv1, smv2 with
| SymBasicVal sv1', SymBasicVal sv2' =>
match sv1',sv2' with
| Val w1, Val w2 => weqb w1 w2
| InVar n1, InVar n2 => if (n1 =? n2) then true else chk_eq_wrt_ctx ctx sv1' sv2'
| _, _ => chk_eq_wrt_ctx ctx sv1' sv2'
end
| SymMETAPUSH cat1 v1, SymMETAPUSH cat2 v2 => andb (cat1 =? cat2)%N (v1 =? v2)%N
| SymOp label1 args1, SymOp label2 args2 =>
if label1 =?i label2 then
match ops label1 with
OpImp _ _ H_Comm _ =>
match (fold_right_two_lists (fun e1 e2 => basic_compare_sstack_val_w_eq_chk_rec ctx e1 e2 maxidx1' sb1' maxidx2' sb2' ops) args1 args2) with
| true => true
| false =>
match H_Comm with
| Some comm_proof =>
match args1, args2 with
| [a1;a2],[b1;b2] =>
if basic_compare_sstack_val_w_eq_chk_rec ctx a1 b2 maxidx1' sb1' maxidx2' sb2' ops
then basic_compare_sstack_val_w_eq_chk_rec ctx a2 b1 maxidx1' sb1' maxidx2' sb2' ops
else false
| _, _ => false
end
| None => false
end
end
end
else false
| SymMLOAD soffset1 smem1, SymMLOAD soffset2 smem2 =>
if basic_compare_sstack_val_w_eq_chk smemory_cmp sstorage_cmp sha3_cmp d' ctx soffset1 soffset2 maxidx1' sb1' maxidx2' sb2' ops
then smemory_cmp basic_compare_sstack_val_w_eq_chk_rec ctx smem1 smem2 maxidx1' sb1' maxidx2' sb2' ops
else false
| SymSLOAD skey1 sstrg1, SymSLOAD skey2 sstrg2 =>
if basic_compare_sstack_val_w_eq_chk smemory_cmp sstorage_cmp sha3_cmp d' ctx skey1 skey2 maxidx1' sb1' maxidx2' sb2' ops
then sstorage_cmp basic_compare_sstack_val_w_eq_chk_rec ctx sstrg1 sstrg2 maxidx1' sb1' maxidx2' sb2' ops
else false
| SymSHA3 soffset1 ssize1 smem1, SymSHA3 soffset2 ssize2 smem2 =>
(* the nested if is to avoid using band *)
if (if basic_compare_sstack_val_w_eq_chk_rec ctx soffset1 soffset2 maxidx1' sb1' maxidx2' sb2' ops then
if basic_compare_sstack_val_w_eq_chk_rec ctx ssize1 ssize2 maxidx1' sb1' maxidx2' sb2' ops then
smemory_cmp basic_compare_sstack_val_w_eq_chk_rec ctx smem1 smem2 maxidx1' sb1' maxidx2' sb2' ops
else
false
else
false)
then true
else
sha3_cmp basic_compare_sstack_val_w_eq_chk_rec ctx soffset1 ssize1 smem1 soffset2 ssize2 smem2 maxidx1' sb1' maxidx2' sb2' ops
| _, _ => false
end
end
end
end.
End SStackValCmpImpl.