-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsymbolic_execution_soundness.v
3375 lines (2687 loc) · 150 KB
/
symbolic_execution_soundness.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
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
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 Coq.Logic.FunctionalExtensionality.
Require Import FORVES2.constants.
Import Constants.
Require Import FORVES2.program.
Import Program.
Require Import FORVES2.execution_state.
Import ExecutionState.
Require Import FORVES2.execution_state_facts.
Import ExecutionStateFacts.
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_execution.
Import SymbolicExecution.
Require Import FORVES2.symbolic_state_eval.
Import SymbolicStateEval.
Require Import FORVES2.symbolic_state_eval_facts.
Import SymbolicStateEvalFacts.
Require Import FORVES2.valid_symbolic_state.
Import ValidSymbolicState.
Require Import FORVES2.concrete_interpreter.
Import ConcreteInterpreter.
Require Import FORVES2.memory_ops_solvers.
Import MemoryOpsSolvers.
Require Import FORVES2.storage_ops_solvers.
Import StorageOpsSolvers.
Require Import FORVES2.constraints.
Import Constraints.
Require Import FORVES2.context.
Import Context.
Module SymbolicExecutionSoundness.
(* A state st is an instance of a symbolic state sst wrt. to a model
ctx means that evaluating sst wrt. ctx we get st' that is equivalent
of st. *)
Definition st_is_instance_of_sst (mem: memory) (strg: storage) (exts: externals) (st: state) (model: assignment) (sst: sstate) (ops: stack_op_instr_map) : Prop :=
exists st',
eval_sstate sst model mem strg exts ops = Some st' /\
eq_execution_states st st'.
(* A state transformer _tr_ and a symbolic state transformer _str_ are
equivalent, if when _str_ transforms _sst_ to _sst'_, then for any
initial state _init_st_ and a state _st_ such that _st_ is an instance
of _sst_ wrt _init_st_, _tr_ transformes from _st_ to _st'_ such that
_st'_ is an instance of _sst'_ wrt _init_st_. In addition, sst is
supposed to be valid, and sst' must be valid. *)
Definition snd_state_transformer ( tr : state -> stack_op_instr_map -> option state ) (symtr : ctx_t -> sstate -> stack_op_instr_map -> option sstate ) : Prop :=
forall (ctx: ctx_t) (sst sst': sstate) (ops : stack_op_instr_map),
valid_sstate sst ops ->
symtr ctx sst ops = Some sst' ->
valid_sstate sst' ops /\
forall (mem: memory) (strg: storage) (exts: externals) (st: state) (model: assignment),
is_model (ctx_cs ctx) model = true ->
st_is_instance_of_sst mem strg exts st model sst ops ->
exists (st': state),
tr st ops = Some st' /\ st_is_instance_of_sst mem strg exts st' model sst' ops.
(* Abstract transformers in symbolic execution generate valid states when applied to valid states *)
(* push_s generated valid states *)
Lemma push_valid_sst:
forall ctx sst sst' w ops,
valid_sstate sst ops ->
push_s w ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' w ops H_valid_sst H_push_s.
unfold push_s in H_push_s.
destruct (push (Val w) (get_stack_sst sst)) as [sstk'|] eqn:E_push; try discriminate.
injection H_push_s as H_sst'.
unfold valid_sstate in H_valid_sst.
destruct H_valid_sst as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
unfold push in E_push.
destruct (length (get_stack_sst sst) <? StackSize); try discriminate.
injection E_push as H_sstk'.
rewrite <- H_sst'.
unfold valid_sstate.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite smap_preserved_when_updating_stack_sst.
rewrite set_and_then_get_stack_sst.
split.
- apply H_valid_sst_smap.
- split.
+ rewrite <- H_sstk'.
simpl.
split. apply I. apply H_valid_sst_sstack.
+ split.
* simpl. apply H_valid_sst_smemory.
* simpl. apply H_valid_sst_sstorage.
Qed.
(* metapush_s generates valid states *)
Lemma metapush_valid_sst:
forall ctx sst sst' cat v ops,
valid_sstate sst ops ->
metapush_s cat v ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' cat v ops H_valid_sst H_metapush_s.
unfold metapush_s in H_metapush_s.
destruct (add_to_smap (get_smap_sst sst) (SymMETAPUSH cat v)) as [key sm'] eqn:E_add_to_smap.
destruct (push (FreshVar key) (get_stack_sst sst)) as [sstk'|] eqn:E_push; try discriminate.
injection H_metapush_s as H_stt'.
unfold push in E_push.
destruct (length (get_stack_sst sst) <? StackSize); try discriminate.
injection E_push as E_sstk'.
rewrite <- H_stt'.
rewrite <- E_sstk'.
unfold valid_sstate.
rewrite smemory_preserved_when_updating_smap_sst.
rewrite sstorage_preserved_when_updating_smap_sst.
rewrite set_and_then_get_smap_sst.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite sstack_preserved_when_updating_smap_sst.
rewrite set_and_then_get_stack_sst.
pose proof (metapush_valid_smv (get_maxidx_smap (get_smap_sst sst)) ops cat v) as H_valid_smv.
symmetry in E_add_to_smap.
pose proof (add_to_map_valid_sstate sst key sm' (SymMETAPUSH cat v) ops H_valid_sst H_valid_smv E_add_to_smap) as H_valid_sst_add.
unfold valid_sstate in H_valid_sst_add.
rewrite smemory_preserved_when_updating_smap_sst in H_valid_sst_add.
rewrite sstorage_preserved_when_updating_smap_sst in H_valid_sst_add.
rewrite set_and_then_get_smap_sst in H_valid_sst_add.
rewrite sstack_preserved_when_updating_smap_sst in H_valid_sst_add.
destruct H_valid_sst_add as [H_valid_sst_smap_add [H_valid_sst_sstack_add [H_valid_sst_smemory_add H_valid_sst_sstorage_add]]].
unfold valid_sstate.
split.
- apply H_valid_sst_smap_add.
- split.
+ simpl.
split.
* pose proof (add_to_smap_key_lt_maxidx (get_smap_sst sst) sm' key (SymMETAPUSH cat v) E_add_to_smap) as H_key_lt_maxidx.
apply H_key_lt_maxidx.
* apply H_valid_sst_sstack_add.
+ split.
* apply H_valid_sst_smemory_add.
* apply H_valid_sst_sstorage_add.
Qed.
(* pop generates valid states *)
Lemma pop_valid_sst:
forall ctx sst sst' ops,
valid_sstate sst ops ->
pop_s ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' ops H_valid_sst H_pop_s.
unfold pop_s in H_pop_s.
destruct (pop (get_stack_sst sst)) as [sstk|] eqn:E_pop; try discriminate.
injection H_pop_s as H_sst'.
unfold pop in E_pop.
destruct (get_stack_sst sst) as [|sv sstk'] eqn:E_sstk'; try discriminate.
injection E_pop as E_sstk.
unfold valid_sstate in H_valid_sst.
destruct H_valid_sst as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
rewrite E_sstk' in H_valid_sst_sstack.
simpl in H_valid_sst_sstack.
destruct H_valid_sst_sstack as [_ H_valid_sst_sstk'].
rewrite <- H_sst'.
rewrite <- E_sstk.
unfold valid_sstate.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite smap_preserved_when_updating_stack_sst.
rewrite set_and_then_get_stack_sst.
split.
- apply H_valid_sst_smap.
- split.
+ apply H_valid_sst_sstk'.
+ split.
* simpl. apply H_valid_sst_smemory.
* simpl. apply H_valid_sst_sstorage.
Qed.
(* metapush_s generates valid states *)
Lemma dup_valid_sst:
forall ctx sst sst' ops k,
valid_sstate sst ops ->
dup_s k ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' ops k H_valid_sst H_dup_s.
unfold dup_s in H_dup_s.
destruct (dup k (get_stack_sst sst)) as [sstk'|] eqn:E_dup; try discriminate.
injection H_dup_s as H_dup_s.
unfold dup in E_dup.
destruct ((k =? 0) || (16 <? k) || (StackSize <=? length (get_stack_sst sst))); try discriminate.
destruct (nth_error (get_stack_sst sst) (pred k)) as [sv|] eqn:E_nth_error; try discriminate.
injection E_dup as H_sstk'.
unfold valid_sstate in H_valid_sst.
destruct H_valid_sst as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
pose proof (valid_sstack_nth (get_maxidx_smap (get_smap_sst sst)) (get_stack_sst sst) sv (pred k) H_valid_sst_sstack E_nth_error) as H_valid_sv.
rewrite <- H_dup_s.
unfold valid_sstate.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite smap_preserved_when_updating_stack_sst.
rewrite set_and_then_get_stack_sst.
split.
- apply H_valid_sst_smap.
- split.
+ rewrite <- H_sstk'.
simpl.
split.
* apply H_valid_sv.
* apply H_valid_sst_sstack.
+ split.
* apply H_valid_sst_smemory.
* apply H_valid_sst_sstorage.
Qed.
(* metapush_s generates valid states *)
Lemma swap_valid_sst:
forall ctx sst sst' ops k,
valid_sstate sst ops ->
swap_s k ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' ops k H_valid_sst H_swap_s.
unfold swap_s in H_swap_s.
destruct (swap k (get_stack_sst sst)) as [sstk'|] eqn:E_swap; try discriminate.
injection H_swap_s as H_swap_s.
unfold swap in E_swap.
destruct ((k =? 0) || (16 <? k)); try discriminate.
destruct (nth_error (get_stack_sst sst) k) as [sv|] eqn:E_nth_error; try discriminate.
destruct (get_stack_sst sst) as [|h t] eqn:E_sstk; try discriminate.
rewrite <- E_sstk in E_nth_error.
injection E_swap as H_sstk'.
unfold valid_sstate in H_valid_sst.
destruct H_valid_sst as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
rewrite <- H_swap_s.
unfold valid_sstate.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite smap_preserved_when_updating_stack_sst.
rewrite set_and_then_get_stack_sst.
split.
- apply H_valid_sst_smap.
- split.
+ pose proof (valid_sstack_nth (get_maxidx_smap (get_smap_sst sst)) (get_stack_sst sst) sv k H_valid_sst_sstack E_nth_error) as H_valid_sv.
pose proof (valid_sstack_skipn (get_maxidx_smap (get_smap_sst sst)) (get_stack_sst sst) (k+1) H_valid_sst_sstack) as H_valid_skipn.
rewrite E_sstk in H_valid_skipn.
assert (H_valid_t := H_valid_sst_sstack).
rewrite E_sstk in H_valid_t.
simpl in H_valid_t.
destruct H_valid_t as [H_valid_h H_valid_t].
pose proof (valid_sstack_firstn (get_maxidx_smap (get_smap_sst sst)) t (k-1) H_valid_t) as H_valid_firstn.
pose proof (valid_sstack_cons (get_maxidx_smap (get_smap_sst sst)) (skipn (k + 1) (h :: t)) h H_valid_skipn H_valid_h) as H_valid_h_skipn.
pose proof (valid_sstack_app (get_maxidx_smap (get_smap_sst sst)) (firstn (k - 1) t) (h :: skipn (k + 1) (h :: t)) H_valid_firstn H_valid_h_skipn) as H_valid_firstn_h_skipn.
rewrite <- H_sstk'.
simpl.
split.
* apply H_valid_sv.
* apply H_valid_firstn_h_skipn.
+ split.
* apply H_valid_sst_smemory.
* apply H_valid_sst_sstorage.
Qed.
(* exec_stack_op_intsr_s generates valid states *)
Lemma exec_stack_op_intsr_valid_sst:
forall ctx sst sst' label ops,
valid_sstate sst ops ->
exec_stack_op_intsr_s label ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' label ops H_valid_sst H_exec_s.
unfold exec_stack_op_intsr_s in H_exec_s.
destruct (ops label) as [nargs f H_com H_coh] eqn:E_label.
destruct (firstn_e nargs (get_stack_sst sst)) as [args|] eqn:E_firstn; try discriminate.
destruct (skipn_e nargs (get_stack_sst sst)) as [sstk'|] eqn:E_skipn; try discriminate.
destruct (add_to_smap (get_smap_sst sst) (SymOp label args)) as [key sm'] eqn:E_add_to_smap.
injection H_exec_s as H_sst'.
unfold firstn_e in E_firstn.
destruct (nargs <=? length (get_stack_sst sst)) eqn:E_nargs_leb_len; try discriminate.
injection E_firstn as E_args.
unfold skipn_e in E_skipn.
rewrite E_nargs_leb_len in E_skipn.
injection E_skipn as E_sstk'.
assert( H_valid_sst' := H_valid_sst).
unfold valid_sstate in H_valid_sst'.
destruct H_valid_sst' as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
pose proof (valid_sstack_firstn (get_maxidx_smap (get_smap_sst sst)) (get_stack_sst sst) nargs H_valid_sst_sstack) as H_valid_args.
rewrite E_args in H_valid_args.
pose proof (valid_sstack_skipn (get_maxidx_smap (get_smap_sst sst)) (get_stack_sst sst) nargs H_valid_sst_sstack) as H_valid_sstk'.
rewrite E_sstk' in H_valid_sstk'.
apply Nat.leb_le in E_nargs_leb_len as E_nargs_le_len.
pose proof (firstn_length_le (get_stack_sst sst) E_nargs_le_len) as E_len_args.
rewrite E_args in E_len_args.
pose proof (op_instr_valid_smv (get_maxidx_smap (get_smap_sst sst)) ops label nargs args f H_com H_coh H_valid_args E_label E_len_args) as H_valid_smv.
symmetry in E_add_to_smap.
pose proof (add_to_map_valid_sstate sst key sm' (SymOp label args) ops H_valid_sst H_valid_smv E_add_to_smap) as H_valid_sst_add.
unfold valid_sstate in H_valid_sst_add.
rewrite smemory_preserved_when_updating_smap_sst in H_valid_sst_add.
rewrite sstorage_preserved_when_updating_smap_sst in H_valid_sst_add.
rewrite set_and_then_get_smap_sst in H_valid_sst_add.
rewrite sstack_preserved_when_updating_smap_sst in H_valid_sst_add.
destruct H_valid_sst_add as [H_valid_sst_smap_add [H_valid_sst_sstack_add [H_valid_sst_smemory_add H_valid_sst_sstorage_add]]].
rewrite <- H_sst'.
unfold valid_sstate.
rewrite smemory_preserved_when_updating_smap_sst.
rewrite sstorage_preserved_when_updating_smap_sst.
rewrite set_and_then_get_smap_sst.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite sstack_preserved_when_updating_smap_sst.
rewrite set_and_then_get_stack_sst.
split.
- apply H_valid_sst_smap_add.
- split.
+ simpl.
split.
* pose proof (add_to_smap_key_lt_maxidx (get_smap_sst sst) sm' key (SymOp label args) E_add_to_smap) as H_key_lt_maxidx.
apply H_key_lt_maxidx.
* destruct (get_smap_sst sst) as [maxidx sb] eqn:E_smap.
simpl in E_add_to_smap.
injection E_add_to_smap as H_maxidx H_sm'.
rewrite H_sm'.
simpl.
apply valid_sstack_S_maxidx.
simpl in H_valid_sstk'.
apply H_valid_sstk'.
+ split.
* apply H_valid_sst_smemory_add.
* apply H_valid_sst_sstorage_add.
Qed.
(* mload generates valid states *)
Lemma mload_valid_sst:
forall ctx sst sst' ops mload_solver,
valid_sstate sst ops ->
mload_solver_snd mload_solver ->
mload_s mload_solver ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' ops mload_solver H_valid_sst H_valid_solver H_mload_s.
unfold mload_s in H_mload_s.
destruct (get_stack_sst sst) as [|soffset sstk'] eqn:E_sstk; try discriminate.
remember (mload_solver ctx soffset (get_memory_sst sst) (get_smap_sst sst) ops) as smv eqn:H_eqsmv.
destruct (add_to_smap (get_smap_sst sst) smv) as [key sm'] eqn:E_add_to_smap.
injection H_mload_s as H_sst'.
rewrite <- H_sst'.
unfold mload_solver_snd in H_valid_solver.
destruct H_valid_solver as [H_valid_solver _].
unfold mload_solver_valid_res in H_valid_solver.
assert( H_valid_sst' := H_valid_sst ).
unfold valid_sstate in H_valid_sst'.
destruct H_valid_sst' as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
rewrite E_sstk in H_valid_sst_sstack.
simpl in H_valid_sst_sstack.
destruct H_valid_sst_sstack as [H_valid_sst_soffset H_valid_sst_sstk'].
symmetry in H_eqsmv.
pose proof (H_valid_solver ctx (get_smap_sst sst) (get_memory_sst sst) soffset smv ops H_valid_sst_smemory H_valid_sst_soffset H_eqsmv) as H_valid_smv.
symmetry in E_add_to_smap.
pose proof (add_to_map_valid_sstate sst key sm' smv ops H_valid_sst H_valid_smv E_add_to_smap) as H_valid_sst_smap_add.
unfold valid_sstate in H_valid_sst_smap_add.
rewrite smemory_preserved_when_updating_smap_sst in H_valid_sst_smap_add.
rewrite sstorage_preserved_when_updating_smap_sst in H_valid_sst_smap_add.
rewrite set_and_then_get_smap_sst in H_valid_sst_smap_add.
rewrite sstack_preserved_when_updating_smap_sst in H_valid_sst_smap_add.
assert (H_valid_sst_smap_add' := H_valid_sst_smap_add).
destruct H_valid_sst_smap_add' as [H_valid_sst_smap_add_smap [H_valid_sst_smap_add_sstack [H_valid_sst_smap_add_smemory H_valid_sst_smap_add_sstorage]]].
unfold valid_sstate.
rewrite smemory_preserved_when_updating_smap_sst.
rewrite sstorage_preserved_when_updating_smap_sst.
rewrite set_and_then_get_smap_sst.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite sstack_preserved_when_updating_smap_sst.
rewrite set_and_then_get_stack_sst.
split.
- apply H_valid_sst_smap_add.
- split.
+ simpl.
split.
* pose proof (add_to_smap_key_lt_maxidx (get_smap_sst sst) sm' key smv E_add_to_smap) as H_key_lt_maxidx.
apply H_key_lt_maxidx.
* destruct (get_smap_sst sst) as [maxidx sb] eqn:E_smap.
simpl in E_add_to_smap.
injection E_add_to_smap as H_maxidx H_sm'.
rewrite H_sm'.
simpl.
apply valid_sstack_S_maxidx.
simpl in H_valid_sst_sstk'.
apply H_valid_sst_sstk'.
+ split.
* apply H_valid_sst_smap_add_smemory.
* apply H_valid_sst_smap_add_sstorage.
Qed.
(* sload generates valid states *)
Lemma sload_valid_sst:
forall ctx sst sst' ops sload_solver,
valid_sstate sst ops ->
sload_solver_snd sload_solver ->
sload_s sload_solver ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' ops sload_solver H_valid_sst H_valid_solver H_sload_s.
unfold sload_s in H_sload_s.
destruct (get_stack_sst sst) as [|skey sstk'] eqn:E_sstk; try discriminate.
remember (sload_solver ctx skey (get_storage_sst sst) (get_smap_sst sst) ops) as smv eqn:H_eqsmv.
destruct (add_to_smap (get_smap_sst sst) smv) as [key sm'] eqn:E_add_to_smap.
injection H_sload_s as H_sst'.
rewrite <- H_sst'.
unfold sload_solver_snd in H_valid_solver.
destruct H_valid_solver as [H_valid_solver _].
unfold sload_solver_valid_res in H_valid_solver.
assert( H_valid_sst' := H_valid_sst ).
unfold valid_sstate in H_valid_sst'.
destruct H_valid_sst' as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
rewrite E_sstk in H_valid_sst_sstack.
simpl in H_valid_sst_sstack.
destruct H_valid_sst_sstack as [H_valid_sst_soffset H_valid_sst_sstk'].
symmetry in H_eqsmv.
pose proof (H_valid_solver ctx (get_smap_sst sst) (get_storage_sst sst) skey smv ops H_valid_sst_sstorage H_valid_sst_soffset H_eqsmv) as H_valid_smv.
symmetry in E_add_to_smap.
pose proof (add_to_map_valid_sstate sst key sm' smv ops H_valid_sst H_valid_smv E_add_to_smap) as H_valid_sst_smap_add.
unfold valid_sstate in H_valid_sst_smap_add.
rewrite smemory_preserved_when_updating_smap_sst in H_valid_sst_smap_add.
rewrite sstorage_preserved_when_updating_smap_sst in H_valid_sst_smap_add.
rewrite set_and_then_get_smap_sst in H_valid_sst_smap_add.
rewrite sstack_preserved_when_updating_smap_sst in H_valid_sst_smap_add.
assert (H_valid_sst_smap_add' := H_valid_sst_smap_add).
destruct H_valid_sst_smap_add' as [H_valid_sst_smap_add_smap [H_valid_sst_smap_add_sstack [H_valid_sst_smap_add_smemory H_valid_sst_smap_add_sstorage]]].
unfold valid_sstate.
rewrite smemory_preserved_when_updating_smap_sst.
rewrite sstorage_preserved_when_updating_smap_sst.
rewrite set_and_then_get_smap_sst.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite sstack_preserved_when_updating_smap_sst.
rewrite set_and_then_get_stack_sst.
split.
- apply H_valid_sst_smap_add.
- split.
+ simpl.
split.
* pose proof (add_to_smap_key_lt_maxidx (get_smap_sst sst) sm' key smv E_add_to_smap) as H_key_lt_maxidx.
apply H_key_lt_maxidx.
* destruct (get_smap_sst sst) as [maxidx sb] eqn:E_smap.
simpl in E_add_to_smap.
injection E_add_to_smap as H_maxidx H_sm'.
rewrite H_sm'.
simpl.
apply valid_sstack_S_maxidx.
simpl in H_valid_sst_sstk'.
apply H_valid_sst_sstk'.
+ split.
* apply H_valid_sst_smap_add_smemory.
* apply H_valid_sst_smap_add_sstorage.
Qed.
(* mstore generates valid states *)
Lemma mstore_valid_sst:
forall ctx sst sst' ops smemory_updater,
smemory_updater_snd smemory_updater ->
valid_sstate sst ops ->
mstore_s smemory_updater ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' ops smemory_updater H_smemory_updater_snd H_valid_sst H_mstore_s.
unfold mstore_s in H_mstore_s.
destruct (get_stack_sst sst) as [|soffset sstk'] eqn:E_sstk; try discriminate.
destruct sstk' as [|svalue sstk''] eqn:E_sstk'; try discriminate.
injection H_mstore_s as H_sst'.
remember (smemory_updater ctx (U_MSTORE sstack_val soffset svalue) (get_memory_sst sst) (get_smap_sst sst) ops) as smem' eqn:E_smem'.
rewrite <- H_sst'.
assert ( H_valid_sst' := H_valid_sst ).
unfold valid_sstate in H_valid_sst'.
destruct H_valid_sst' as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
rewrite E_sstk in H_valid_sst_sstack.
simpl in H_valid_sst_sstack.
destruct H_valid_sst_sstack as [H_valid_soffset [H_valid_svalue H_valid_sstk']].
pose proof (valid_smemory_update_ov (get_maxidx_smap (get_smap_sst sst)) soffset svalue H_valid_soffset H_valid_svalue) as [H_valid_u _].
unfold smemory_updater_snd in H_smemory_updater_snd.
destruct H_smemory_updater_snd as [H_smemory_updater_valid _].
unfold smemory_updater_valid_res in H_smemory_updater_valid.
symmetry in E_smem'.
pose proof (H_smemory_updater_valid ctx (get_smap_sst sst) (get_memory_sst sst) smem' (U_MSTORE sstack_val soffset svalue) ops H_valid_sst_smemory H_valid_u E_smem') as H_valid_smem'.
unfold valid_sstate.
rewrite smap_preserved_when_updating_stack_sst.
rewrite smap_preserved_when_updating_memory_sst.
rewrite set_and_then_get_stack_sst.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite set_and_then_get_memory_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_memory_sst.
split.
- apply H_valid_sst_smap.
- split.
+ apply H_valid_sstk'.
+ split.
* apply H_valid_smem'.
* apply H_valid_sst_sstorage.
Qed.
(* mstore8 generates valid states *)
Lemma mstore8_valid_sst:
forall ctx sst sst' ops smemory_updater,
smemory_updater_snd smemory_updater ->
valid_sstate sst ops ->
mstore8_s smemory_updater ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' ops smemory_updater H_smemory_updater_snd H_valid_sst H_mstore_s.
unfold mstore8_s in H_mstore_s.
destruct (get_stack_sst sst) as [|soffset sstk'] eqn:E_sstk; try discriminate.
destruct sstk' as [|svalue sstk''] eqn:E_sstk'; try discriminate.
injection H_mstore_s as H_sst'.
remember (smemory_updater ctx (U_MSTORE8 sstack_val soffset svalue) (get_memory_sst sst) (get_smap_sst sst) ops) as smem' eqn:E_smem'.
rewrite <- H_sst'.
assert ( H_valid_sst' := H_valid_sst ).
unfold valid_sstate in H_valid_sst'.
destruct H_valid_sst' as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
rewrite E_sstk in H_valid_sst_sstack.
simpl in H_valid_sst_sstack.
destruct H_valid_sst_sstack as [H_valid_soffset [H_valid_svalue H_valid_sstk']].
pose proof (valid_smemory_update_ov (get_maxidx_smap (get_smap_sst sst)) soffset svalue H_valid_soffset H_valid_svalue) as [H_valid_u _].
unfold smemory_updater_snd in H_smemory_updater_snd.
destruct H_smemory_updater_snd as [H_smemory_updater_valid _].
unfold smemory_updater_valid_res in H_smemory_updater_valid.
symmetry in E_smem'.
pose proof (H_smemory_updater_valid ctx (get_smap_sst sst) (get_memory_sst sst) smem' (U_MSTORE8 sstack_val soffset svalue) ops H_valid_sst_smemory H_valid_u E_smem') as H_valid_smem'.
unfold valid_sstate.
rewrite smap_preserved_when_updating_stack_sst.
rewrite smap_preserved_when_updating_memory_sst.
rewrite set_and_then_get_stack_sst.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite set_and_then_get_memory_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_memory_sst.
split.
- apply H_valid_sst_smap.
- split.
+ apply H_valid_sstk'.
+ split.
* apply H_valid_smem'.
* apply H_valid_sst_sstorage.
Qed.
(* sstore generates valid states *)
Lemma sstore_valid_sst:
forall ctx sst sst' ops sstorage_updater,
sstorage_updater_snd sstorage_updater ->
valid_sstate sst ops ->
sstore_s sstorage_updater ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' ops sstorage_updater H_sstorage_updater_snd H_valid_sst H_sstore_s.
unfold sstore_s in H_sstore_s.
destruct (get_stack_sst sst) as [|skey sstk'] eqn:E_sstk; try discriminate.
destruct sstk' as [|svalue sstk''] eqn:E_sstk'; try discriminate.
injection H_sstore_s as H_sst'.
remember (sstorage_updater ctx (U_SSTORE sstack_val skey svalue) (get_storage_sst sst) (get_smap_sst sst) ops) as sstrg' eqn:E_sstrg'.
rewrite <- H_sst'.
assert ( H_valid_sst' := H_valid_sst ).
unfold valid_sstate in H_valid_sst'.
destruct H_valid_sst' as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
rewrite E_sstk in H_valid_sst_sstack.
simpl in H_valid_sst_sstack.
destruct H_valid_sst_sstack as [H_valid_soffset [H_valid_svalue H_valid_sstk']].
pose proof (valid_sstorage_update_kv (get_maxidx_smap (get_smap_sst sst)) skey svalue H_valid_soffset H_valid_svalue) as H_valid_u.
unfold sstorage_updater_snd in H_sstorage_updater_snd.
destruct H_sstorage_updater_snd as [H_sstorage_updater_valid _].
unfold sstorage_updater_valid_res in H_sstorage_updater_valid.
symmetry in E_sstrg'.
pose proof (H_sstorage_updater_valid ctx (get_smap_sst sst) (get_storage_sst sst) sstrg' (U_SSTORE sstack_val skey svalue) ops H_valid_sst_sstorage H_valid_u E_sstrg') as H_valid_sstrg'.
unfold valid_sstate.
rewrite smap_preserved_when_updating_stack_sst.
rewrite smap_preserved_when_updating_storage_sst.
rewrite set_and_then_get_stack_sst.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite smemory_preserved_when_updating_storage_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
rewrite set_and_then_get_storage_sst.
split.
- apply H_valid_sst_smap.
- split.
+ apply H_valid_sstk'.
+ split.
* apply H_valid_sst_smemory.
* apply H_valid_sstrg'.
Qed.
(* sha3 generates valid states *)
Lemma sha3_valid_sst:
forall ctx sst sst' ops,
valid_sstate sst ops ->
sha3_s ctx sst ops = Some sst' ->
valid_sstate sst' ops.
Proof.
intros ctx sst sst' ops H_valid_sst H_sha3_s.
unfold sha3_s in H_sha3_s.
destruct (get_stack_sst sst) as [|soffset sstk'] eqn:E_sstk; try discriminate.
destruct sstk' as [|ssize sstk''] eqn:E_sstk'; try discriminate.
destruct (add_to_smap (get_smap_sst sst) (SymSHA3 soffset ssize (get_memory_sst sst))) as [key sm'] eqn:E_add_to_smap.
injection H_sha3_s as H_sst'.
assert ( H_valid_sst' := H_valid_sst ).
unfold valid_sstate in H_valid_sst'.
destruct H_valid_sst' as [H_valid_sst_smap [H_valid_sst_sstack [H_valid_sst_smemory H_valid_sst_sstorage]]].
rewrite E_sstk in H_valid_sst_sstack.
simpl in H_valid_sst_sstack.
destruct H_valid_sst_sstack as [H_valid_soffset [H_valid_ssize H_valid_sstk'']].
pose proof (sha3_smv (get_maxidx_smap (get_smap_sst sst)) ops (get_memory_sst sst) soffset ssize H_valid_sst_smemory H_valid_soffset H_valid_ssize) as H_valid_smv.
symmetry in E_add_to_smap.
pose proof (add_to_map_valid_sstate sst key sm' (SymSHA3 soffset ssize (get_memory_sst sst)) ops H_valid_sst H_valid_smv E_add_to_smap) as H_valid_sst_smap_add.
unfold valid_sstate in H_valid_sst_smap_add.
rewrite set_and_then_get_smap_sst in H_valid_sst_smap_add.
rewrite sstack_preserved_when_updating_smap_sst in H_valid_sst_smap_add.
rewrite sstorage_preserved_when_updating_smap_sst in H_valid_sst_smap_add.
rewrite smemory_preserved_when_updating_smap_sst in H_valid_sst_smap_add.
destruct H_valid_sst_smap_add as [H_valid_sst_smap_add_smap [H_valid_sst_smap_add_sstack [H_valid_sst_smap_add_smemory H_valid_sst_smap_add_sstorage]]].
rewrite <- H_sst'.
unfold valid_sstate.
rewrite set_and_then_get_smap_sst.
rewrite sstack_preserved_when_updating_smap_sst.
rewrite set_and_then_get_stack_sst.
rewrite smemory_preserved_when_updating_smap_sst.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_smap_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
split.
(* there are many duplication of destructing (get_smap_sst sst) -- revise later *)
- apply H_valid_sst_smap_add_smap.
- split.
+ unfold valid_sstack. fold valid_sstack.
split.
* unfold valid_sstack_value.
pose proof (add_to_smap_key_lt_maxidx (get_smap_sst sst) sm' key (SymSHA3 soffset ssize (get_memory_sst sst)) E_add_to_smap) as H_key_lt_maxidx.
apply H_key_lt_maxidx.
* destruct (get_smap_sst sst) as [maxidx sb] eqn:E_smap.
simpl in E_add_to_smap.
injection E_add_to_smap as H_maxidx H_sm'.
rewrite H_sm'.
simpl.
apply valid_sstack_S_maxidx.
simpl in H_valid_sstk''.
apply H_valid_sstk''.
+ split.
* destruct (get_smap_sst sst) as [maxidx sb] eqn:E_smap.
simpl in E_add_to_smap.
injection E_add_to_smap as H_maxidx H_sm'.
rewrite H_sm'.
simpl.
simpl in H_valid_sst_smemory.
apply valid_smemory_S_maxidx.
apply H_valid_sst_smemory.
* destruct (get_smap_sst sst) as [maxidx sb] eqn:E_smap.
simpl in E_add_to_smap.
injection E_add_to_smap as H_maxidx H_sm'.
rewrite H_sm'.
simpl.
simpl in H_valid_sst_sstorage.
apply valid_sstorage_S_maxidx.
apply H_valid_sst_sstorage.
Qed.
(* Abstract transformers in symbolic execution are sound *)
(* Applying eval_sstack_val' on (Val w) returns Some w *)
Lemma eval_sstack_val'_Val:
forall (w: EVMWord) (model: assignment) (mem: memory) (strg: storage) (exts: externals) (maxidx: nat) (bs: sbindings) (ops: stack_op_instr_map),
eval_sstack_val' (S maxidx) (Val w) model mem strg exts maxidx bs ops = Some w.
Proof.
intros.
destruct bs; reflexivity.
Qed.
(* Applying eval_sstack_val on (Val w) returns Some w *)
Lemma eval_sstack_val_Val:
forall (w: EVMWord) (model: assignment) (mem: memory) (strg: storage) (exts: externals) (maxidx: nat) (bs: sbindings) (ops: stack_op_instr_map),
eval_sstack_val (Val w) model mem strg exts maxidx bs ops = Some w.
Proof.
intros.
unfold eval_sstack_val.
apply eval_sstack_val'_Val.
Qed.
(* Applying eval_sstack_val' on (InVar i) returns (nth_error stk i) *)
Lemma eval_sstack_val'_InVar:
forall (i:nat) (model: assignment) (mem: memory) (strg: storage) (exts: externals) (maxidx: nat) (bs: sbindings) (ops: stack_op_instr_map),
eval_sstack_val' (S maxidx) (InVar i) model mem strg exts maxidx bs ops = Some (model i).
Proof.
intros.
unfold eval_sstack_val'.
destruct bs; unfold follow_in_smap; reflexivity.
Qed.
(* Applying eval_sstack_val on (InVar i) returns (nth_error stk i) *)
Lemma eval_sstack_val_InVar:
forall (i:nat) (model: assignment) (mem: memory) (strg: storage) (exts: externals) (maxidx: nat) (bs: sbindings) (ops: stack_op_instr_map),
eval_sstack_val (InVar i) model mem strg exts maxidx bs ops = Some (model i).
Proof.
intros.
unfold eval_sstack_val.
apply eval_sstack_val'_InVar.
Qed.
(*
If applying eval_sstack on sstk return Some stk', then applying it on (Val w)::sstk returns Some (w::stk')
*)
Lemma eval_sstack_w:
forall (w : EVMWord) (sstk: sstack) (model: assignment) (stk': stack) (mem: memory) (strg: storage) (exts: externals) (maxidx: nat) (sb: sbindings) (ops: stack_op_instr_map),
eval_sstack sstk maxidx sb model mem strg exts ops = Some stk' ->
eval_sstack ((Val w)::sstk) maxidx sb model mem strg exts ops = Some (w::stk').
Proof.
intros w sstk model stk' mem strg ctx maxidx sb ops H_eval_sstack_stk.
unfold eval_sstack.
unfold map_option.
rewrite <- map_option_ho.
rewrite eval_sstack_val_Val.
unfold eval_sstack in H_eval_sstack_stk.
rewrite H_eval_sstack_stk.
reflexivity.
Qed.
(* Like eval_sstack_w, but stated on states. *)
Lemma eval_sstate_w:
forall (model: assignment) (w : EVMWord) (sst : sstate) (st': state) (mem: memory) (strg: storage) (exts: externals) (ops: stack_op_instr_map),
eval_sstate sst model mem strg exts ops = Some st' ->
eval_sstate (set_stack_sst sst ((Val w)::(get_stack_sst sst))) model mem strg exts ops = Some (set_stack_st st' (w::(get_stack_st st'))).
Proof.
intros model w sst st' mem strg exts ops H_eval_sst.
unfold eval_sstate in H_eval_sst.
destruct (eval_sstack (get_stack_sst sst) (get_maxidx_smap (get_smap_sst sst)) (get_bindings_smap (get_smap_sst sst))
model mem strg exts ops) as [stk|] eqn:E_eval_sstack; try discriminate.
unfold eval_sstate.
rewrite smap_preserved_when_updating_stack_sst.
rewrite set_and_then_get_stack_sst.
pose proof (eval_sstack_w w (get_stack_sst sst) model stk mem strg exts (get_maxidx_smap (get_smap_sst sst)) (get_bindings_smap (get_smap_sst sst)) ops E_eval_sstack) as H_eval_sstack_w.
rewrite H_eval_sstack_w.
rewrite smemory_preserved_when_updating_stack_sst.
rewrite sstorage_preserved_when_updating_stack_sst.
destruct (eval_smemory (get_memory_sst sst) (get_maxidx_smap (get_smap_sst sst)) (get_bindings_smap (get_smap_sst sst)) model mem strg exts ops); try discriminate.
destruct (eval_sstorage (get_storage_sst sst) (get_maxidx_smap (get_smap_sst sst)) (get_bindings_smap (get_smap_sst sst)) model mem strg exts ops); try discriminate.
injection H_eval_sst as H_st'. (* get the value of st' *)
rewrite <- H_st'. simpl.
unfold make_st.
reflexivity.
Qed.
(* eval_sstack generate a list of the smae length as the input *)
Lemma eval_sstack_len:
forall (sstk: sstack) (model: assignment) (stk': stack) (mem: memory) (strg: storage) (exts: externals) (maxidx: nat) (sb: sbindings) (ops: stack_op_instr_map),
eval_sstack sstk maxidx sb model mem strg exts ops = Some stk' ->
length sstk = length stk'.
Proof.
intros sstl model stk' mem strg exts maxidx sb ops H_eval_sstack.
unfold eval_sstack in H_eval_sstack.
apply map_option_len in H_eval_sstack.
apply H_eval_sstack.
Qed.
(* when st is an instance of sst wrt to model, the length stacks in
st and sst are the same *)
Lemma st_is_instance_of_sst_stk_len:
forall (mem: memory) (strg: storage) (exts: externals) (st: state) (model: assignment) (sst: sstate) (ops: stack_op_instr_map),
st_is_instance_of_sst mem strg exts st model sst ops ->
length (get_stack_sst sst) = length (get_stack_st st).
Proof.
intros mem strg exts st model sst ops H_inst.
unfold st_is_instance_of_sst in H_inst.
destruct H_inst as [st' H_inst].
destruct H_inst as [H_inst_l H_inst_r].
unfold eval_sstate in H_inst_l.
destruct (eval_sstack (get_stack_sst sst) (get_maxidx_smap (get_smap_sst sst)) (get_bindings_smap (get_smap_sst sst)) model mem strg exts ops) as [stk'|] eqn:E_eval_sstack; try discriminate.
destruct (eval_smemory (get_memory_sst sst) (get_maxidx_smap (get_smap_sst sst)) (get_bindings_smap (get_smap_sst sst)) model mem strg exts ops) as [mem'|] eqn:E_eval_smemory; try discriminate.
destruct (eval_sstorage (get_storage_sst sst) (get_maxidx_smap (get_smap_sst sst)) (get_bindings_smap (get_smap_sst sst)) model mem strg exts ops) as [strg'|] eqn:E_eval_sstorage; try discriminate.
apply eval_sstack_len in E_eval_sstack.
rewrite E_eval_sstack.
apply eq_execution_states_stack_len in H_inst_r.
rewrite H_inst_r.
injection H_inst_l as H_st'.
rewrite <- H_st'.
unfold make_st.
simpl.
reflexivity.
Qed.
(* Extending an smap with a new value, does not affect follow_in_smap. *)
Lemma follow_in_smap_preserved_when_smap_extended:
forall m m' smv idx' idx x,
valid_sstack_value (get_maxidx_smap m) (FreshVar idx) ->
(add_to_smap m smv) = (idx', m') ->
follow_in_smap (FreshVar idx) (get_maxidx_smap m) (get_bindings_smap m) = Some x ->
follow_in_smap (FreshVar idx) (get_maxidx_smap m') (get_bindings_smap m') = Some x.
Proof.
intros m m' smv idx' idx x.
intros H_valid_sstack_value H_add_to_smap H_follow_in_smap.
destruct m.
destruct m'.
simpl in H_valid_sstack_value.
simpl in H_add_to_smap.
simpl in H_follow_in_smap.
simpl.
injection H_add_to_smap as H_maxid_idx' H_m' H_sb.
rewrite <- H_sb.
destruct bindings; try discriminate.
simpl.
apply Nat.lt_neq in H_valid_sstack_value as H_maxidx_idx.
apply Nat.neq_sym in H_maxidx_idx.
apply Nat.eqb_neq in H_maxidx_idx.
rewrite H_maxidx_idx.
simpl in H_follow_in_smap.
apply H_follow_in_smap.
Qed.
(* Extending an smap with a new value, does not affect eval_sstack_val when applied to valid_sstack_value. *)
Lemma eval_sstack_val'_preserved_when_smap_extended:
forall m m' sv smv v model mem strg exts ops idx',
valid_sstack_value (get_maxidx_smap m) sv ->
(add_to_smap m smv) = (idx', m') ->
eval_sstack_val' (S (get_maxidx_smap m)) sv model mem strg exts (get_maxidx_smap m) (get_bindings_smap m) ops = Some v ->
eval_sstack_val' (S (get_maxidx_smap m')) sv model mem strg exts (get_maxidx_smap m') (get_bindings_smap m') ops = Some v.
Proof.
intros m m' sv smv v model mem strg exts ops idx' H_valid_sv H_add_to_smap H_eval_sstack.
destruct sv as [val|n|idx] eqn:E_sv.
+ pose proof (eval_sstack_val'_Val val model mem strg exts (get_maxidx_smap m) (get_bindings_smap m) ops) as H_eval_sstack_val'_Val.
rewrite H_eval_sstack_val'_Val in H_eval_sstack.
rewrite <- H_eval_sstack.
pose proof (eval_sstack_val'_Val val model mem strg exts (get_maxidx_smap m') (get_bindings_smap m') ops) as H_eval_sstack_val'_Val_0.
rewrite H_eval_sstack_val'_Val_0.
reflexivity.
+ pose proof (eval_sstack_val'_InVar n model mem strg exts (get_maxidx_smap m) (get_bindings_smap m) ops) as H_eval_sstack_val'_InVar.
rewrite H_eval_sstack_val'_InVar in H_eval_sstack.
rewrite <- H_eval_sstack.
pose proof (eval_sstack_val'_InVar n model mem strg exts (get_maxidx_smap m') (get_bindings_smap m') ops) as H_eval_sstack_val'_InVar_0.
rewrite H_eval_sstack_val'_InVar_0.
reflexivity.
+ simpl in H_eval_sstack.
destruct (follow_in_smap (FreshVar idx) (get_maxidx_smap m) (get_bindings_smap m)) as [smv'|] eqn:E_follow; try discriminate.
pose proof (follow_in_smap_preserved_when_smap_extended m m' smv idx' idx smv' H_valid_sv H_add_to_smap E_follow) as E_follow_ext.
destruct m as [maxidx sb].
destruct m' as [maxidx' sb'].
unfold get_bindings_smap.
unfold get_maxidx_smap.
unfold get_bindings_smap in H_eval_sstack.
unfold get_maxidx_smap in H_eval_sstack.
unfold get_bindings_smap in E_follow_ext.
unfold get_maxidx_smap in E_follow_ext.
assert (H_add_to_smap':=H_add_to_smap).
simpl in H_add_to_smap'.
injection H_add_to_smap' as H_idx' H_maxidx' H_sb'.
simpl.
rewrite E_follow_ext.
rewrite <- H_maxidx'.
destruct smv'; try discriminate.
destruct smv0.
* apply H_eval_sstack.
* apply H_eval_sstack.
* destruct (ops label) eqn:E_label; try discriminate.
destruct (length args =? n) eqn:E_len; try discriminate.