-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathmemory_ops_solvers_impl_soundness.v
2401 lines (1992 loc) · 112 KB
/
memory_ops_solvers_impl_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 FORVES.constants.
Import Constants.
Require Import FORVES.program.
Import Program.
Require Import FORVES.execution_state.
Import ExecutionState.
Require Import FORVES.stack_operation_instructions.
Import StackOpInstrs.
Require Import FORVES.misc.
Import Misc.
Require Import FORVES.symbolic_state.
Import SymbolicState.
Require Import FORVES.symbolic_state_eval.
Import SymbolicStateEval.
Require Import FORVES.symbolic_state_eval_facts.
Import SymbolicStateEvalFacts.
Require Import FORVES.valid_symbolic_state.
Import ValidSymbolicState.
Require Import FORVES.memory_ops_solvers.
Import MemoryOpsSolvers.
Require Import FORVES.memory_ops_solvers_impl.
Import MemoryOpsSolversImpl.
Require Import FORVES.symbolic_state_cmp.
Import SymbolicStateCmp.
Require Import FORVES.eval_common.
Import EvalCommon.
Require Import FORVES.concrete_interpreter.
Import ConcreteInterpreter.
Require Import FORVES.symbolic_execution_soundness.
Import SymbolicExecutionSoundness.
Require Import storage_ops_solvers_impl_soundness.
Import StorageOpsSolversImplSoundness.
Require Import memory_ops_solvers_impl_soundness_misc.
Import MemoryOpsSolversImplSoundnessMisc.
Module MemoryOpsSolversImplSoundness.
Lemma trivial_mload_solver_snd: mload_solver_ext_snd trivial_mload_solver.
Proof.
unfold mload_solver_ext_snd.
unfold mload_solver_snd.
intros.
split.
- unfold mload_solver_valid_res.
intros.
unfold trivial_mload_solver in H2.
rewrite <- H2.
simpl.
intuition.
- unfold mload_solver_correct_res.
intros.
unfold trivial_mload_solver in H3.
rewrite <- H3 in H4.
rewrite H4.
exists idx1.
exists m1.
split; try reflexivity.
intros.
unfold eval_sstack_val.
symmetry in H5.
assert (H_valid_smap_value: valid_smap_value instk_height (get_maxidx_smap m) ops (SymMLOAD soffset smem)). simpl. intuition.
symmetry in H4.
pose proof (add_to_smap_key_lt_maxidx m m1 idx1 (SymMLOAD soffset smem) H4).
pose proof (valid_sstack_val_freshvar instk_height (get_maxidx_smap m1) idx1 H6).
symmetry in H4.
pose proof (add_to_smap_valid_smap instk_height idx1 m m1 (SymMLOAD soffset smem) ops H0 H_valid_smap_value H4).
pose proof (eval_sstack_val'_succ (S (get_maxidx_smap m1)) instk_height (FreshVar idx1) stk mem strg exts (get_maxidx_smap m1) (get_bindings_smap m1) ops H5 H7 H8 (gt_Sn_n (get_maxidx_smap m1))).
destruct H9 as [v H9].
exists v.
split; apply H9.
Qed.
Lemma trivial_smemory_updater_snd: smemory_updater_ext_snd trivial_smemory_updater.
Proof.
unfold smemory_updater_ext_snd.
intros sstack_val_cmp H_valid_sstack_val_cmp.
unfold smemory_updater_snd.
split.
- unfold smemory_updater_valid_res.
intros m smem smem' u instk_height ops H_valid_smem H_valid_u H_updater.
unfold trivial_smemory_updater in H_updater.
rewrite <- H_updater.
simpl.
split.
+ apply H_valid_u.
+ apply H_valid_smem.
- unfold smemory_updater_correct_res.
intros m smem smem' u instk_height ops H_valid_smap H_valid_smem H_valid_u H_updater.
unfold trivial_smemory_updater in H_updater.
rewrite <- H_updater.
intros stk mem strg exts H_len_stk.
pose proof (valid_smemory_when_extended_with_valid_update instk_height (get_maxidx_smap m) u smem H_valid_u H_valid_smem) as H_valid_u_smem.
unfold valid_smap in H_valid_smap.
symmetry in H_len_stk.
pose proof (eval_smemory_succ instk_height (get_maxidx_smap m) (get_bindings_smap m) stk mem strg exts ops (u::smem) H_len_stk H_valid_u_smem H_valid_smap) as H_eval_smemory_u_smem.
destruct H_eval_smemory_u_smem as [smem'' H_eval_smemory_u_smem].
exists smem''.
exists smem''.
repeat split; apply H_eval_smemory_u_smem.
Qed.
Lemma H_memory_slots_do_not_overlap:
forall soffset soffset' size size' maxidx sbindings instk_height ops,
valid_bindings instk_height maxidx sbindings ops ->
valid_sstack_value instk_height maxidx soffset ->
valid_sstack_value instk_height maxidx soffset' ->
memory_slots_do_not_overlap soffset soffset' size size' maxidx sbindings instk_height ops = true ->
forall stk mem strg exts,
(length stk) = instk_height ->
exists v1 v2,
eval_sstack_val' (S maxidx) soffset stk mem strg exts maxidx sbindings ops = Some v1 /\
eval_sstack_val' (S maxidx) soffset' stk mem strg exts maxidx sbindings ops = Some v2 /\
orb ((wordToN v1)+size <? (wordToN v2))%N ((wordToN v2) + size' <? (wordToN v1))%N = true.
Proof.
intros soffset soffset' size size' maxidx sbindings instk_height ops.
intros H_valid_sbindings H_valid_offset H_valid_offset' H_addr_nover.
unfold memory_slots_do_not_overlap in H_addr_nover.
destruct (follow_in_smap soffset maxidx sbindings) as [soffset_m|] eqn:E_follow_soffset; try discriminate.
destruct soffset_m; try discriminate.
destruct smv; try discriminate.
destruct val; try discriminate.
destruct (follow_in_smap soffset' maxidx sbindings) as [soffset'_m|] eqn:E_follow_soffset'; try discriminate.
destruct soffset'_m; try discriminate.
destruct smv; try discriminate.
destruct val0; try discriminate.
intros stk mem strg exts.
intros H_stk_len.
unfold eval_sstack_val' at 1.
rewrite E_follow_soffset.
unfold eval_sstack_val' at 1.
rewrite E_follow_soffset'.
exists val.
exists val0.
split; try split; try reflexivity.
apply H_addr_nover.
Qed.
Lemma H_mstore8_is_included_in_mstore:
forall soffset_mstore8 soffset_mstore maxidx sbindings instk_height ops,
valid_bindings instk_height maxidx sbindings ops ->
valid_sstack_value instk_height maxidx soffset_mstore8 ->
valid_sstack_value instk_height maxidx soffset_mstore ->
mstore8_is_included_in_mstore soffset_mstore8 soffset_mstore maxidx sbindings instk_height ops = true ->
forall stk mem strg exts,
(length stk) = instk_height ->
exists v1 v2,
eval_sstack_val' (S maxidx) soffset_mstore8 stk mem strg exts maxidx sbindings ops = Some v1 /\
eval_sstack_val' (S maxidx) soffset_mstore stk mem strg exts maxidx sbindings ops = Some v2 /\
andb ((wordToN v2) <=? (wordToN v1) )%N ((wordToN v1) <=? (wordToN v2)+31)%N = true.
Proof.
intros soffset_mstore8 soffset_mstore maxidx sbindings instk_height ops.
intros H_valid_sbindings H_valid_offset_mstore8 H_valid_offset_mstore H_addr_not_inc.
unfold mstore8_is_included_in_mstore in H_addr_not_inc.
destruct (follow_in_smap soffset_mstore8 maxidx sbindings) as [soffset_mstore8_m|] eqn:E_follow_soffset_mstore8; try discriminate.
destruct soffset_mstore8_m; try discriminate.
destruct smv; try discriminate.
destruct val; try discriminate.
destruct (follow_in_smap soffset_mstore maxidx sbindings) as [soffset_mstore_m|] eqn:E_follow_soffset_mstore; try discriminate.
destruct soffset_mstore_m; try discriminate.
destruct smv; try discriminate.
destruct val0; try discriminate.
intros stk mem strg exts.
intros H_stk_len.
unfold eval_sstack_val' at 1.
rewrite E_follow_soffset_mstore8.
unfold eval_sstack_val' at 1.
rewrite E_follow_soffset_mstore.
exists val.
exists val0.
split; try split; try reflexivity.
apply H_addr_not_inc.
Qed.
Lemma basic_mload_solver_valid:
forall sstack_val_cmp,
mload_solver_valid_res (basic_mload_solver sstack_val_cmp).
Proof.
intros sstack_val_cmp.
unfold mload_solver_valid_res.
intros m smem soffset instk_height smv ops H_valid_smem H_valid_offset.
revert H_valid_smem.
revert smem.
induction smem as [|u smem' IHsmem'].
+ intros H_valid_smem H_basic_solver.
simpl in H_basic_solver.
rewrite <- H_basic_solver.
simpl.
split; auto.
+ intros H_valid_smem H_basic_solver.
simpl in H_basic_solver.
destruct u as [soffset' svalue|].
++ destruct (sstack_val_cmp (S (get_maxidx_smap m)) soffset soffset' (get_maxidx_smap m) (get_bindings_smap m) (get_maxidx_smap m) (get_bindings_smap m) instk_height ops) eqn:E_soffset_soffset'_cmp.
+++ rewrite <- H_basic_solver.
simpl.
apply H_valid_smem.
+++ destruct (memory_slots_do_not_overlap soffset soffset' 31 31) eqn:E_do_not_overlap.
++++ apply IHsmem'.
apply H_valid_smem.
apply H_basic_solver.
++++ rewrite <- H_basic_solver.
simpl.
split; auto.
++ destruct (memory_slots_do_not_overlap soffset offset 31 0) eqn:E_do_not_overlap.
+++ apply IHsmem'.
apply H_valid_smem.
apply H_basic_solver.
+++ rewrite <- H_basic_solver.
simpl.
split; auto.
Qed.
Lemma S_S_n_gt_n: forall n, S (S n) > n.
Proof.
auto.
Qed.
Lemma H_map_o_smem:
forall instk_height d stk mem strg exts maxidx bs ops smem,
valid_smemory instk_height maxidx smem ->
valid_bindings instk_height maxidx bs ops ->
d > maxidx ->
instk_height = length stk ->
exists v,
map_option (instantiate_memory_update (fun sv : sstack_val => eval_sstack_val' d sv stk mem strg exts maxidx bs ops)) smem = Some v.
Proof.
induction smem as [|u sstrg' IHsstrg'].
+ intros. simpl. exists []. reflexivity.
+ intros H_valid_smemory H_valid_bs H_d_gt_maxidx H_len_stk.
unfold map_option.
rewrite <- map_option_ho.
unfold instantiate_memory_update at 1.
destruct u as [soffset' svalue' | soffset' svalue'].
++ unfold valid_smemory in H_valid_smemory. fold valid_smemory in H_valid_smemory.
destruct H_valid_smemory as [H_valid_smemory_0 H_valid_smemory_1].
unfold valid_smemory_update in H_valid_smemory_0.
destruct H_valid_smemory_0 as [H_valid_smemory_0_0 H_valid_smemory_0_1].
pose proof (eval_sstack_val'_succ d instk_height soffset' stk mem strg exts maxidx bs ops H_len_stk H_valid_smemory_0_0 H_valid_bs H_d_gt_maxidx) as eval_sstack_val'_succ_0.
destruct eval_sstack_val'_succ_0 as [v eval_sstack_val'_succ_0].
rewrite eval_sstack_val'_succ_0.
pose proof (eval_sstack_val'_succ d instk_height svalue' stk mem strg exts maxidx bs ops H_len_stk H_valid_smemory_0_1 H_valid_bs H_d_gt_maxidx) as eval_sstack_val'_succ_1.
destruct eval_sstack_val'_succ_1 as [v' eval_sstack_val'_succ_1].
rewrite eval_sstack_val'_succ_1.
pose proof (IHsstrg' H_valid_smemory_1 H_valid_bs H_d_gt_maxidx H_len_stk) as IHsstrg'_0.
destruct IHsstrg'_0 as [v'' IHsstrg'_0].
rewrite IHsstrg'_0.
exists (U_MSTORE EVMWord v v' :: v'').
reflexivity.
++ unfold valid_smemory in H_valid_smemory. fold valid_smemory in H_valid_smemory.
destruct H_valid_smemory as [H_valid_smemory_0 H_valid_smemory_1].
unfold valid_smemory_update in H_valid_smemory_0.
destruct H_valid_smemory_0 as [H_valid_smemory_0_0 H_valid_smemory_0_1].
pose proof (eval_sstack_val'_succ d instk_height soffset' stk mem strg exts maxidx bs ops H_len_stk H_valid_smemory_0_0 H_valid_bs H_d_gt_maxidx) as eval_sstack_val'_succ_0.
destruct eval_sstack_val'_succ_0 as [v eval_sstack_val'_succ_0].
rewrite eval_sstack_val'_succ_0.
pose proof (eval_sstack_val'_succ d instk_height svalue' stk mem strg exts maxidx bs ops H_len_stk H_valid_smemory_0_1 H_valid_bs H_d_gt_maxidx) as eval_sstack_val'_succ_1.
destruct eval_sstack_val'_succ_1 as [v' eval_sstack_val'_succ_1].
rewrite eval_sstack_val'_succ_1.
pose proof (IHsstrg' H_valid_smemory_1 H_valid_bs H_d_gt_maxidx H_len_stk) as IHsstrg'_0.
destruct IHsstrg'_0 as [v'' IHsstrg'_0].
rewrite IHsstrg'_0.
exists (U_MSTORE8 EVMWord v v' :: v'').
reflexivity.
Qed.
Lemma mstore'_aux:
forall sz addr (value : word (sz * 8)) mem,
(fix mstore' (sz : nat) (mem0 : memory) {struct sz} : word (sz * 8) -> N -> memory :=
match sz as sz0 return (word (sz0 * 8) -> N -> memory) with
| 0 => fun (_ : word (0 * 8)) (_ : N) => mem0
| S sz1' =>
fun (value0 : word (S sz1' * 8)) (offset offset'0 : N) =>
if (offset'0 =? offset)%N
then ConcreteInterpreter.split1_byte value0
else mstore' sz1' mem0 (ConcreteInterpreter.split2_byte value0) (offset + 1)%N offset'0
end) sz mem value addr = ConcreteInterpreter.mstore' mem value addr.
Proof.
auto.
Qed.
Lemma mload''_aux:
forall n addr addr' x y,
(addr' > addr)%N ->
(ConcreteInterpreter.mload''
(fun offset' : N =>
if (offset' =? addr)%N
then x
else y offset') addr' n) =
(ConcreteInterpreter.mload'' y addr' n).
Proof.
induction n as [|n' IHn'].
+ intros.
simpl.
reflexivity.
+ intros addr addr' x y H_addr'_gt_addr'.
unfold ConcreteInterpreter.mload'' at 1.
fold ConcreteInterpreter.mload''.
assert (H_addr'_neqb_addr: (addr' =? addr)%N = false).
(* proof of assert *)
rewrite N.eqb_neq.
intuition.
assert (H_addr'_1_gt_addr: (addr'+1> addr)%N).
apply N.lt_gt.
apply N.lt_lt_add_r.
apply N.gt_lt in H_addr'_gt_addr'.
apply H_addr'_gt_addr'.
(****)
rewrite H_addr'_neqb_addr.
unfold ConcreteInterpreter.mload'' at 2.
fold ConcreteInterpreter.mload''.
pose proof (IHn' addr (addr'+1)%N x y H_addr'_1_gt_addr) as IHn'_0.
rewrite IHn'_0.
reflexivity.
Qed.
Lemma mload''_mstore'_same_address:
forall n mem addr value,
ConcreteInterpreter.mload'' (ConcreteInterpreter.mstore' mem (value: word (n*8)) addr) addr n = value.
Proof.
induction n as [|n' IHn'].
+ intros mem addr value.
simpl.
rewrite word0.
reflexivity.
+ intros mem addr value.
unfold ConcreteInterpreter.mstore'.
rewrite mstore'_aux.
unfold ConcreteInterpreter.mload''.
rewrite N.eqb_refl.
fold ConcreteInterpreter.mload''.
destruct n' as [|n''] eqn:E_n'.
++ unfold ConcreteInterpreter.mload''.
unfold ConcreteInterpreter.split1_byte.
unfold ConcreteInterpreter.split1_byte.
unfold mul.
pose proof (wordToZ_combine_WO (split1 8 0 value)) as H_wordToZ_combine_WO.
apply wordToZ_inj in H_wordToZ_combine_WO.
rewrite H_wordToZ_combine_WO at 1.
pose proof (split1_0 value) as H_split1_0_0.
unfold mul in H_split1_0_0.
unfold add in H_split1_0_0.
pose proof (H_split1_0_0 (eq_refl 8)) as H_split1_0_1.
unfold eq_rect in H_split1_0_1.
apply H_split1_0_1.
++ rewrite mload''_aux.
+++ pose proof (IHn' mem (addr+1)%N (ConcreteInterpreter.split2_byte value)) as IHn'_0.
rewrite IHn'_0.
unfold ConcreteInterpreter.split1_byte.
unfold ConcreteInterpreter.split2_byte.
apply Word.combine_split.
+++ apply N.lt_gt.
apply Nlt_in.
rewrite N2Nat.inj_add.
simpl.
intuition.
Qed.
Lemma mload_mstore_same_address:
forall mem addr value,
(ConcreteInterpreter.mload
(ConcreteInterpreter.mstore mem value addr) addr) = value.
Proof.
intros mem addr value.
unfold ConcreteInterpreter.mload.
unfold ConcreteInterpreter.mload'.
unfold ConcreteInterpreter.mstore.
apply mload''_mstore'_same_address.
Qed.
Lemma do_not_overlap_mload:
forall mem offset offset' value' updates,
(wordToN offset + 31 <? wordToN offset')%N || (wordToN offset' + 31 <? wordToN offset)%N = true ->
(ConcreteInterpreter.mload'' (update_memory mem (U_MSTORE EVMWord offset' value' :: updates)) (wordToN offset) 32) =
(ConcreteInterpreter.mload'' (update_memory mem updates) (wordToN (offset : EVMWord)) 32).
Proof.
intros mem offset offset' value' updates H_o.
unfold ConcreteInterpreter.mload''.
rewrite assoc_ones_31.
rewrite Reduce_ones_31.
rewrite assoc_ones_30.
rewrite Reduce_ones_30.
rewrite assoc_ones_29.
rewrite Reduce_ones_29.
rewrite assoc_ones_28.
rewrite Reduce_ones_28.
rewrite assoc_ones_27.
rewrite Reduce_ones_27.
rewrite assoc_ones_26.
rewrite Reduce_ones_26.
rewrite assoc_ones_25.
rewrite Reduce_ones_25.
rewrite assoc_ones_24.
rewrite Reduce_ones_24.
rewrite assoc_ones_23.
rewrite Reduce_ones_23.
rewrite assoc_ones_22.
rewrite Reduce_ones_22.
rewrite assoc_ones_21.
rewrite Reduce_ones_21.
rewrite assoc_ones_20.
rewrite Reduce_ones_20.
rewrite assoc_ones_19.
rewrite Reduce_ones_19.
rewrite assoc_ones_18.
rewrite Reduce_ones_18.
rewrite assoc_ones_17.
rewrite Reduce_ones_17.
rewrite assoc_ones_16.
rewrite Reduce_ones_16.
rewrite assoc_ones_15.
rewrite Reduce_ones_15.
rewrite assoc_ones_14.
rewrite Reduce_ones_14.
rewrite assoc_ones_13.
rewrite Reduce_ones_13.
rewrite assoc_ones_12.
rewrite Reduce_ones_12.
rewrite assoc_ones_11.
rewrite Reduce_ones_11.
rewrite assoc_ones_10.
rewrite Reduce_ones_10.
rewrite assoc_ones_9.
rewrite Reduce_ones_9.
rewrite assoc_ones_8.
rewrite Reduce_ones_8.
rewrite assoc_ones_7.
rewrite Reduce_ones_7.
rewrite assoc_ones_6.
rewrite Reduce_ones_6.
rewrite assoc_ones_5.
rewrite Reduce_ones_5.
rewrite assoc_ones_4.
rewrite Reduce_ones_4.
rewrite assoc_ones_3.
rewrite Reduce_ones_3.
rewrite assoc_ones_2.
rewrite Reduce_ones_2.
rewrite (do_not_overlap_mload_aux mem value' updates 1 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 2 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 3 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 4 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 5 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 6 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 7 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 8 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 9 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 10 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 11 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 12 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 13 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 14 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 15 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 16 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 17 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 18 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 19 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 20 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 21 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 22 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 23 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 24 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 25 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 26 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 27 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 28 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 29 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 30 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux mem value' updates 31 offset offset' H_31_lt_32 H_o).
assert ( H_O_0: (wordToN offset + 0 = wordToN offset)%N). apply N.add_0_r.
rewrite <- H_O_0.
rewrite (do_not_overlap_mload_aux mem value' updates 0 offset offset' H_31_lt_32 H_o).
reflexivity.
Qed.
Lemma do_not_overlap_mload_0:
forall mem offset offset' value' updates,
(wordToN offset + 31 <? wordToN offset')%N || (wordToN offset' + 0 <? wordToN offset)%N = true ->
(ConcreteInterpreter.mload'' (update_memory mem (U_MSTORE8 EVMWord offset' value' :: updates)) (wordToN offset) 32) =
(ConcreteInterpreter.mload'' (update_memory mem updates) (wordToN (offset : EVMWord)) 32).
Proof.
Proof.
intros mem offset offset' value' updates H_o.
unfold ConcreteInterpreter.mload''.
rewrite assoc_ones_31.
rewrite Reduce_ones_31.
rewrite assoc_ones_30.
rewrite Reduce_ones_30.
rewrite assoc_ones_29.
rewrite Reduce_ones_29.
rewrite assoc_ones_28.
rewrite Reduce_ones_28.
rewrite assoc_ones_27.
rewrite Reduce_ones_27.
rewrite assoc_ones_26.
rewrite Reduce_ones_26.
rewrite assoc_ones_25.
rewrite Reduce_ones_25.
rewrite assoc_ones_24.
rewrite Reduce_ones_24.
rewrite assoc_ones_23.
rewrite Reduce_ones_23.
rewrite assoc_ones_22.
rewrite Reduce_ones_22.
rewrite assoc_ones_21.
rewrite Reduce_ones_21.
rewrite assoc_ones_20.
rewrite Reduce_ones_20.
rewrite assoc_ones_19.
rewrite Reduce_ones_19.
rewrite assoc_ones_18.
rewrite Reduce_ones_18.
rewrite assoc_ones_17.
rewrite Reduce_ones_17.
rewrite assoc_ones_16.
rewrite Reduce_ones_16.
rewrite assoc_ones_15.
rewrite Reduce_ones_15.
rewrite assoc_ones_14.
rewrite Reduce_ones_14.
rewrite assoc_ones_13.
rewrite Reduce_ones_13.
rewrite assoc_ones_12.
rewrite Reduce_ones_12.
rewrite assoc_ones_11.
rewrite Reduce_ones_11.
rewrite assoc_ones_10.
rewrite Reduce_ones_10.
rewrite assoc_ones_9.
rewrite Reduce_ones_9.
rewrite assoc_ones_8.
rewrite Reduce_ones_8.
rewrite assoc_ones_7.
rewrite Reduce_ones_7.
rewrite assoc_ones_6.
rewrite Reduce_ones_6.
rewrite assoc_ones_5.
rewrite Reduce_ones_5.
rewrite assoc_ones_4.
rewrite Reduce_ones_4.
rewrite assoc_ones_3.
rewrite Reduce_ones_3.
rewrite assoc_ones_2.
rewrite Reduce_ones_2.
rewrite (do_not_overlap_mload_aux' mem value' updates 1 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 2 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 3 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 4 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 5 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 6 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 7 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 8 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 9 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 10 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 11 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 12 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 13 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 14 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 15 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 16 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 17 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 18 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 19 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 20 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 21 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 22 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 23 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 24 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 25 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 26 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 27 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 28 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 29 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 30 offset offset' H_31_lt_32 H_o).
rewrite (do_not_overlap_mload_aux' mem value' updates 31 offset offset' H_31_lt_32 H_o).
assert ( H_O_0: (wordToN offset + 0 = wordToN offset)%N). apply N.add_0_r.
rewrite <- H_O_0.
rewrite (do_not_overlap_mload_aux' mem value' updates 0 offset offset' H_31_lt_32 H_o).
reflexivity.
Qed.
Lemma update_same_address_mstore'_aux:
forall n mem (value: word (n*8)) z offset1 offset2 x,
(x =? offset1)%N = false ->
(ConcreteInterpreter.mstore' mem value offset2) x =
(ConcreteInterpreter.mstore'
(fun (offset':N) => if (offset' =? offset1)%N then z else mem offset')
value
offset2) x.
Proof.
induction n as [|n' IHn'].
+ intros.
simpl.
rewrite H.
reflexivity.
+ intros.
simpl.
pose proof (IHn' mem (ConcreteInterpreter.split2_byte value) z offset1 (offset2+1)%N x).
rewrite H0.
reflexivity.
apply H.
Qed.
Lemma update_same_address_mstore'_a:
forall n m mem (value: word (n*8)) (value' : word (m*8)) offset,
n>=m ->
ConcreteInterpreter.mstore' mem value offset =
ConcreteInterpreter.mstore' (ConcreteInterpreter.mstore' mem value' offset) value offset.
Proof.
induction n as [|n' IHn'].
+ intros.
assert(m=0). intuition.
simpl.
unfold ConcreteInterpreter.mstore'.
destruct m; try (discriminate || reflexivity).
+ intros.
destruct m as [|m'] eqn:E_m.
++ unfold ConcreteInterpreter.mstore' at 3.
reflexivity.
++ assert(n'>=m'). intuition.
pose proof (IHn' m' mem (ConcreteInterpreter.split2_byte value) (ConcreteInterpreter.split2_byte value') (offset+1)%N H0) as IHn'_0.
apply functional_extensionality.
intro x.
simpl.
destruct (x =? offset)%N eqn:E_x_offset; try reflexivity.
pose proof (update_same_address_mstore'_aux n' (ConcreteInterpreter.mstore' mem
(ConcreteInterpreter.split2_byte value') (offset + 1)) (ConcreteInterpreter.split2_byte value) (ConcreteInterpreter.split1_byte value') offset (offset+1) x E_x_offset).
rewrite <- H1.
rewrite IHn'_0.
reflexivity.
Qed.
Lemma update_same_address_mstore':
forall n mem (value value': word (n*8)) offset,
ConcreteInterpreter.mstore' mem value offset =
ConcreteInterpreter.mstore' (ConcreteInterpreter.mstore' mem value' offset) value offset.
Proof.
intros.
assert(H_ge_refl: n>=n). intuition.
pose proof (update_same_address_mstore'_a n n mem value value' offset H_ge_refl) as H_0.
apply H_0.
Qed.
Lemma ge_Sn_Sm_ge_1:
forall n m,
S n > 0 -> S m < S n -> exists i, n = S i.
Proof.
intros n m H1 H2.
destruct n as [|n'] eqn:E_n.
+ apply lt_S_n in H2.
destruct m.
++ apply Nat.lt_irrefl in H2. contradiction.
++ apply Nat.nlt_0_r in H2. contradiction.
+ exists n'.
reflexivity.
Qed.
Lemma N_x_nat_of_Si:
forall x i,
(x + N.of_nat (S i) = x + 1 + N.of_nat i)%N.
Proof.
intros x i.
rewrite Nat2N.inj_succ.
rewrite <- N.add_1_l.
repeat rewrite N.add_assoc.
reflexivity.
Qed.
Lemma update_same_address_mstore8_mstore':
forall i n mem (value : word (n*8)) (value': word (1*8)) offset,
n > 0 ->
i < n ->
ConcreteInterpreter.mstore' mem value offset =
ConcreteInterpreter.mstore' (ConcreteInterpreter.mstore' mem value' (offset+ N.of_nat i)%N) value offset.
Proof.
induction i as [|i' IHi'].
+ intros n mem value value' offset H_n_gt_0 H_i_lt_n.
unfold N.of_nat.
rewrite N.add_0_r.
apply update_same_address_mstore'_a.
intuition.
+ destruct n as [|n'] eqn:E_n.
++ intros mem value value' offset H_n_gt_0 H_i_l.
apply gt_irrefl in H_n_gt_0.
contradiction.
++ intros mem value value' offset H_n_gt_0 H_i_lt_n.
pose proof (ge_Sn_Sm_ge_1 n' i' H_n_gt_0 H_i_lt_n) as H_n'_ge_1.
destruct H_n'_ge_1 as [n'' H_n'_ge_1].
rewrite N_x_nat_of_Si.
apply functional_extensionality.
intro x.
simpl.
destruct (x =? offset)%N eqn:E_x_offset; try reflexivity.
assert(H_n'_gt_0: n'>0). intuition.
assert(H_i'_lt_n': i'<n'). intuition.
pose proof (IHi' n' mem (ConcreteInterpreter.split2_byte value) value' (offset+1)%N H_n'_gt_0 H_i'_lt_n') as IHi'_0.
rewrite IHi'_0.
simpl.
reflexivity.
Qed.
Lemma two_consecutive_updates_same_address_conc:
forall v v1 v2 mem mem',
update_memory mem (U_MSTORE EVMWord v v1 :: U_MSTORE EVMWord v v2 :: mem') = update_memory mem (U_MSTORE EVMWord v v1 :: mem').
Proof.
intros v v1 v2 mem mem'.
simpl.
remember (update_memory mem mem') as mem_i.
unfold ConcreteInterpreter.mstore.
pose proof (update_same_address_mstore' 32 mem_i v1 v2 (wordToN v)).
symmetry in H.
rewrite H at 1.
reflexivity.
Qed.
Lemma two_consecutive_mstore8_updates_same_address_conc:
forall v v1 v2 mem mem',
update_memory mem (U_MSTORE8 EVMWord v v1 :: U_MSTORE8 EVMWord v v2 :: mem') = update_memory mem (U_MSTORE8 EVMWord v v1 :: mem').
Proof.
intros v v1 v2 mem mem'.
simpl.
remember (update_memory mem mem') as mem_i.
unfold ConcreteInterpreter.mstore.
pose proof (update_same_address_mstore' 1 mem_i (ConcreteInterpreter.split1_byte (v1 : word (BytesInEVMWord*8))) (ConcreteInterpreter.split1_byte (v2 : word (BytesInEVMWord*8))) (wordToN v)).
symmetry in H.
rewrite H at 1.
reflexivity.
Qed.
Lemma inter_n_j:
forall n m j,
(n <=? m) && (m <=? n+j) = true ->
exists i, i <= j /\ (m = n+i).
Proof.
intros n m j H.
exists (m-n).
apply andb_prop in H.
destruct H as [H1 H2].
rewrite Nat.leb_le in H1.
rewrite Nat.leb_le in H2.
split; try intuition.
Qed.
Lemma N_inter_n_j:
forall n m j,
((n <=? m) && (m <=? n+ j) = true)%N ->
exists i, (i <= j)%N /\ (m = n+i)%N.
Proof.
intros n m j H0.
apply andb_prop in H0.
destruct H0 as [H0_1 H0_2].
rewrite N.leb_le in H0_1.
rewrite N.leb_le in H0_2.
assert (H0_1_nat: N.to_nat n <= N.to_nat m). intuition.
assert (H0_2_nat: N.to_nat m <= N.to_nat n + N.to_nat j). intuition.
rewrite <- Nat.leb_le in H0_1_nat.
rewrite <- Nat.leb_le in H0_2_nat.
pose proof (conj H0_1_nat H0_2_nat) as H0_12.
apply andb_true_intro in H0_12.
pose proof (inter_n_j (N.to_nat n) (N.to_nat m) (N.to_nat j) H0_12) as H_nat.
destruct H_nat as [i [H_nat_1 H_nat_2]].
exists (N.of_nat i).
split.
+ rewrite N.le_lteq.
apply Nat.le_lteq in H_nat_1.
destruct H_nat_1.
++ left. apply Nlt_in. rewrite Nat2N.id.
apply H.
++ right. rewrite H. rewrite N2Nat.id. reflexivity.
+ pose proof N2Nat.inj.
apply N2Nat.inj.
rewrite N2Nat.inj_add.
rewrite Nat2N.id.
apply H_nat_2.
Qed.
Lemma two_consecutive_updates_same_address_mstore8_conc:
forall offset offset_8 v1 v2 mem mem',
(wordToN offset <=? wordToN offset_8)%N && (wordToN offset_8 <=? wordToN offset + 31)%N = true ->
update_memory mem (U_MSTORE EVMWord offset v1 :: U_MSTORE8 EVMWord offset_8 v2 :: mem') = update_memory mem (U_MSTORE EVMWord offset v1 :: mem').
Proof.
intros offset offset_8 v1 v2 mem mem' H.
simpl.
unfold ConcreteInterpreter.mstore.
pose proof (N_inter_n_j (wordToN offset) (wordToN offset_8) 31 H) as H_0.
destruct H_0 as [i [H_0_0 H_0_1]].
rewrite H_0_1.
assert(H_32: (N.to_nat 32%N = 32)). intuition.
assert(H1: BytesInEVMWord > 0). unfold BytesInEVMWord. intuition.
assert(H2: N.to_nat i < BytesInEVMWord).
unfold BytesInEVMWord.
rewrite <- H_32.
apply Nlt_out.
rewrite <- N.lt_succ_r in H_0_0.
simpl in H_0_0.
apply H_0_0.
pose proof (update_same_address_mstore8_mstore' (N.to_nat i) BytesInEVMWord (update_memory mem mem') v1 (ConcreteInterpreter.split1_byte (v2: word ((S (pred BytesInEVMWord))*8))) (wordToN offset) H1 H2) as H3.
rewrite N2Nat.id in H3.
rewrite H3.
reflexivity.
Qed.
Lemma two_consecutive_updates_same_address:
forall soffset soffset' svalue svalue' smem instk_height maxidx bs stk mem strg exts ops v,
eval_sstack_val soffset stk mem strg exts maxidx bs ops = Some v ->
eval_sstack_val soffset' stk mem strg exts maxidx bs ops = Some v ->
valid_smemory instk_height maxidx smem ->
valid_bindings instk_height maxidx bs ops ->
valid_sstack_value instk_height maxidx soffset ->
valid_sstack_value instk_height maxidx svalue ->
valid_sstack_value instk_height maxidx soffset' ->
valid_sstack_value instk_height maxidx svalue' ->
length stk = instk_height ->
eval_smemory (U_MSTORE sstack_val soffset svalue :: U_MSTORE sstack_val soffset' svalue' :: smem) maxidx bs stk mem strg exts ops =
eval_smemory (U_MSTORE sstack_val soffset svalue :: smem) maxidx bs stk mem strg exts ops.
Proof.
intros soffset soffset' svalue svalue' smem instk_height maxidx bs stk mem strg exts ops v H_eval_soffset H_eval_soffset' H_valid_smem H_valid_bs H_valid_soffset H_valid_svalue H_vlaid_soffset' H_valid_svalue' H_stk_len.
pose proof (eval_sstack_val'_succ (S maxidx) instk_height svalue stk mem strg exts maxidx bs ops (eq_sym H_stk_len) H_valid_svalue H_valid_bs (gt_Sn_n maxidx)) as H_eval_svalue.
destruct H_eval_svalue as [v1 H_eval_svalue].
pose proof (eval_sstack_val'_succ (S maxidx) instk_height svalue' stk mem strg exts maxidx bs ops (eq_sym H_stk_len) H_valid_svalue' H_valid_bs (gt_Sn_n maxidx)) as H_eval_svalue'.
destruct H_eval_svalue' as [v2 H_eval_svalue'].
unfold eval_smemory.
unfold eval_sstack_val.
assert( H_valid_u1_u2_smem: valid_smemory instk_height maxidx (U_MSTORE sstack_val soffset svalue :: U_MSTORE sstack_val soffset' svalue' :: smem)). simpl. auto.
pose proof (H_map_o_smem instk_height (S maxidx) stk mem strg exts maxidx bs ops (U_MSTORE sstack_val soffset svalue :: U_MSTORE sstack_val soffset' svalue' :: smem) H_valid_u1_u2_smem H_valid_bs (gt_Sn_n maxidx) (eq_sym H_stk_len)) as H_map_o_smem_0.
destruct H_map_o_smem_0 as [u1_u2_smem_v H_map_o_smem_0].
rewrite H_map_o_smem_0.
assert( H_valid_u1_smem: valid_smemory instk_height maxidx (U_MSTORE sstack_val soffset svalue :: smem)). simpl. auto.
pose proof (H_map_o_smem instk_height (S maxidx) stk mem strg exts maxidx bs ops (U_MSTORE sstack_val soffset svalue :: smem) H_valid_u1_smem H_valid_bs (gt_Sn_n maxidx) (eq_sym H_stk_len)) as H_map_o_smem_1.
destruct H_map_o_smem_1 as [u1_smem_v H_map_o_smem_1].
rewrite H_map_o_smem_1.
pose proof (map_option_split_2 (memory_update sstack_val) (memory_update EVMWord) (instantiate_memory_update (fun sv : sstack_val => eval_sstack_val' (S maxidx) sv stk mem strg exts maxidx bs ops)) smem u1_u2_smem_v (U_MSTORE sstack_val soffset svalue) (U_MSTORE sstack_val soffset' svalue') H_map_o_smem_0) as H_map_o_smem_0_0.
destruct H_map_o_smem_0_0 as [u1_v [u2_v [smem_v [H_u1_u2_smem_v [H_map_o_smem_0_u1 [H_map_o_smem_0_u2 H_map_o_smem_0_smem]]]]]].
unfold instantiate_memory_update in H_map_o_smem_0_u1.
unfold eval_sstack_val in H_eval_soffset.
rewrite H_eval_soffset in H_map_o_smem_0_u1.
unfold eval_sstack_val in H_eval_svalue.
rewrite H_eval_svalue in H_map_o_smem_0_u1.
injection H_map_o_smem_0_u1 as H_map_o_smem_0_u1.
unfold instantiate_memory_update in H_map_o_smem_0_u2.
unfold eval_sstack_val in H_eval_soffset'.
rewrite H_eval_soffset' in H_map_o_smem_0_u2.
unfold eval_sstack_val in H_eval_svalue'.
rewrite H_eval_svalue' in H_map_o_smem_0_u2.
injection H_map_o_smem_0_u2 as H_map_o_smem_0_u2.