-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmemory_ops_solvers_impl_soundness.v
2743 lines (2268 loc) · 133 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 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.symbolic_state_eval_facts.
Import SymbolicStateEvalFacts.
Require Import FORVES2.valid_symbolic_state.
Import ValidSymbolicState.
Require Import FORVES2.memory_ops_solvers.
Import MemoryOpsSolvers.
Require Import FORVES2.memory_ops_solvers_impl.
Import MemoryOpsSolversImpl.
Require Import FORVES2.symbolic_state_cmp.
Import SymbolicStateCmp.
Require Import FORVES2.symbolic_execution_soundness.
Import SymbolicExecutionSoundness.
Require Import storage_ops_solvers_impl_soundness.
Import StorageOpsSolversImplSoundness.
Require Import memory_ops_solvers_impl_soundness_misc.
Import MemoryOpsSolversImplSoundnessMisc.
Require Import FORVES2.constraints.
Import Constraints.
Require Import FORVES2.context.
Import Context.
Require Import FORVES2.context_facts.
Import ContextFacts.
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 (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 (get_maxidx_smap m1) idx1 H6).
symmetry in H4.
pose proof (add_to_smap_valid_smap idx1 m m1 (SymMLOAD soffset smem) ops H0 H_valid_smap_value H4).
pose proof (eval_sstack_val'_succ (S (get_maxidx_smap m1)) (FreshVar idx1) model mem strg exts (get_maxidx_smap m1) (get_bindings_smap m1) ops 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 ctx m smem smem' u 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 ctx m smem smem' u ops H_valid_smap H_valid_smem H_valid_u H_updater.
unfold trivial_smemory_updater in H_updater.
rewrite <- H_updater.
intros model mem strg exts H_is_model.
pose proof (valid_smemory_when_extended_with_valid_update (get_maxidx_smap m) u smem H_valid_u H_valid_smem) as H_valid_u_smem.
unfold valid_smap in H_valid_smap.
pose proof (eval_smemory_succ (get_maxidx_smap m) (get_bindings_smap m) model mem strg exts ops (u::smem) 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 ctx soffset soffset' size size' maxidx sbindings ops,
valid_bindings maxidx sbindings ops ->
valid_sstack_value maxidx soffset ->
valid_sstack_value maxidx soffset' ->
memory_slots_do_not_overlap ctx soffset soffset' size size' maxidx sbindings ops = true ->
forall model mem strg exts,
is_model (ctx_cs ctx) model = true ->
exists v1 v2,
eval_sstack_val' (S maxidx) soffset model mem strg exts maxidx sbindings ops = Some v1 /\
eval_sstack_val' (S maxidx) soffset' model mem strg exts maxidx sbindings ops = Some v2 /\
orb ((wordToN v1)+size <? (wordToN v2))%N ((wordToN v2) + size' <? (wordToN v1))%N = true.
Proof.
intros ctx soffset soffset' size size' maxidx sbindings 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 (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; destruct val0; try discriminate.
intros modfe mem strg exts.
intros H_is_model.
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.
intros model mem strg exts H_is_model.
pose proof (eval_sstack_val'_succ (S maxidx) soffset model mem strg exts maxidx sbindings ops H_valid_offset H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset.
pose proof (eval_sstack_val'_succ (S maxidx) soffset' model mem strg exts maxidx sbindings ops H_valid_offset' H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset'.
destruct H_eval_soffset as [v_soffset H_eval_soffset].
destruct H_eval_soffset' as [v_soffset' H_eval_soffset'].
exists v_soffset.
exists v_soffset'.
repeat split; try auto.
unfold eval_sstack_val' in H_eval_soffset.
rewrite E_follow_soffset in H_eval_soffset.
injection H_eval_soffset as H_eval_soffset.
unfold eval_sstack_val' in H_eval_soffset'.
rewrite E_follow_soffset' in H_eval_soffset'.
injection H_eval_soffset' as H_eval_soffset'.
apply orb_prop in H_addr_nover.
destruct H_addr_nover as [H_addr_nover | H_addr_nover].
pose proof (chk_lt_lshift_wrt_ctx_snd ctx (Val val) (InVar var) size H_addr_nover model mem strg exts maxidx sbindings ops H_is_model) as H_chk_lt_wshit_wrt_ctx_snd.
destruct H_chk_lt_wshit_wrt_ctx_snd as [v1 [v2 [H_chk_newq_wrt_ctx_snd_1 [H_chk_newq_wrt_ctx_snd_2 H_chk_newq_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_Val val model mem strg exts maxidx sbindings ops) as H_eval_val.
rewrite H_eval_val in H_chk_newq_wrt_ctx_snd_1.
injection H_chk_newq_wrt_ctx_snd_1 as H_chk_newq_wrt_ctx_snd_1.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var.
rewrite H_eval_var in H_chk_newq_wrt_ctx_snd_2.
injection H_chk_newq_wrt_ctx_snd_2 as H_chk_newq_wrt_ctx_snd_2.
rewrite <- H_eval_soffset.
rewrite <- H_eval_soffset'.
rewrite H_chk_newq_wrt_ctx_snd_1.
rewrite H_chk_newq_wrt_ctx_snd_2.
rewrite orb_true_iff.
left.
rewrite N.ltb_lt.
apply H_chk_newq_wrt_ctx_snd_3.
pose proof (chk_lt_lshift_wrt_ctx_snd ctx (InVar var) (Val val) size' H_addr_nover model mem strg exts maxidx sbindings ops H_is_model) as H_chk_lt_wshit_wrt_ctx_snd.
destruct H_chk_lt_wshit_wrt_ctx_snd as [v1 [v2 [H_chk_newq_wrt_ctx_snd_1 [H_chk_newq_wrt_ctx_snd_2 H_chk_newq_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_Val val model mem strg exts maxidx sbindings ops) as H_eval_val.
rewrite H_eval_val in H_chk_newq_wrt_ctx_snd_2.
injection H_chk_newq_wrt_ctx_snd_2 as H_chk_newq_wrt_ctx_snd_2.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var.
rewrite H_eval_var in H_chk_newq_wrt_ctx_snd_1.
injection H_chk_newq_wrt_ctx_snd_1 as H_chk_newq_wrt_ctx_snd_1.
rewrite <- H_eval_soffset.
rewrite <- H_eval_soffset'.
rewrite H_chk_newq_wrt_ctx_snd_1.
rewrite H_chk_newq_wrt_ctx_snd_2.
rewrite orb_true_iff.
right.
rewrite N.ltb_lt.
apply H_chk_newq_wrt_ctx_snd_3.
intros model mem strg exts H_is_model.
pose proof (eval_sstack_val'_succ (S maxidx) soffset model mem strg exts maxidx sbindings ops H_valid_offset H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset.
pose proof (eval_sstack_val'_succ (S maxidx) soffset' model mem strg exts maxidx sbindings ops H_valid_offset' H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset'.
destruct H_eval_soffset as [v_soffset H_eval_soffset].
destruct H_eval_soffset' as [v_soffset' H_eval_soffset'].
exists v_soffset.
exists v_soffset'.
repeat split; try auto.
unfold eval_sstack_val' in H_eval_soffset.
rewrite E_follow_soffset in H_eval_soffset.
injection H_eval_soffset as H_eval_soffset.
unfold eval_sstack_val' in H_eval_soffset'.
rewrite E_follow_soffset' in H_eval_soffset'.
injection H_eval_soffset' as H_eval_soffset'.
apply orb_prop in H_addr_nover.
destruct H_addr_nover as [H_addr_nover | H_addr_nover].
pose proof (chk_lt_lshift_wrt_ctx_snd ctx (InVar var) (Val val) size H_addr_nover model mem strg exts maxidx sbindings ops H_is_model) as H_chk_lt_wshit_wrt_ctx_snd.
destruct H_chk_lt_wshit_wrt_ctx_snd as [v1 [v2 [H_chk_newq_wrt_ctx_snd_1 [H_chk_newq_wrt_ctx_snd_2 H_chk_newq_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_Val val model mem strg exts maxidx sbindings ops) as H_eval_val.
rewrite H_eval_val in H_chk_newq_wrt_ctx_snd_2.
injection H_chk_newq_wrt_ctx_snd_2 as H_chk_newq_wrt_ctx_snd_2.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var.
rewrite H_eval_var in H_chk_newq_wrt_ctx_snd_1.
injection H_chk_newq_wrt_ctx_snd_1 as H_chk_newq_wrt_ctx_snd_1.
rewrite <- H_eval_soffset.
rewrite <- H_eval_soffset'.
rewrite H_chk_newq_wrt_ctx_snd_1.
rewrite H_chk_newq_wrt_ctx_snd_2.
rewrite orb_true_iff.
left.
rewrite N.ltb_lt.
apply H_chk_newq_wrt_ctx_snd_3.
pose proof (chk_lt_lshift_wrt_ctx_snd ctx (Val val) (InVar var) size' H_addr_nover model mem strg exts maxidx sbindings ops H_is_model) as H_chk_lt_wshit_wrt_ctx_snd.
destruct H_chk_lt_wshit_wrt_ctx_snd as [v1 [v2 [H_chk_newq_wrt_ctx_snd_1 [H_chk_newq_wrt_ctx_snd_2 H_chk_newq_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_Val val model mem strg exts maxidx sbindings ops) as H_eval_val.
rewrite H_eval_val in H_chk_newq_wrt_ctx_snd_1.
injection H_chk_newq_wrt_ctx_snd_1 as H_chk_newq_wrt_ctx_snd_1.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var.
rewrite H_eval_var in H_chk_newq_wrt_ctx_snd_2.
injection H_chk_newq_wrt_ctx_snd_2 as H_chk_newq_wrt_ctx_snd_2.
rewrite <- H_eval_soffset.
rewrite <- H_eval_soffset'.
rewrite H_chk_newq_wrt_ctx_snd_1.
rewrite H_chk_newq_wrt_ctx_snd_2.
rewrite orb_true_iff.
right.
rewrite N.ltb_lt.
apply H_chk_newq_wrt_ctx_snd_3.
intros model mem strg exts H_is_model.
pose proof (eval_sstack_val'_succ (S maxidx) soffset model mem strg exts maxidx sbindings ops H_valid_offset H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset.
pose proof (eval_sstack_val'_succ (S maxidx) soffset' model mem strg exts maxidx sbindings ops H_valid_offset' H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset'.
destruct H_eval_soffset as [v_soffset H_eval_soffset].
destruct H_eval_soffset' as [v_soffset' H_eval_soffset'].
exists v_soffset.
exists v_soffset'.
repeat split; try auto.
unfold eval_sstack_val' in H_eval_soffset.
rewrite E_follow_soffset in H_eval_soffset.
injection H_eval_soffset as H_eval_soffset.
unfold eval_sstack_val' in H_eval_soffset'.
rewrite E_follow_soffset' in H_eval_soffset'.
injection H_eval_soffset' as H_eval_soffset'.
apply orb_prop in H_addr_nover.
destruct H_addr_nover as [H_addr_nover | H_addr_nover].
pose proof (chk_lt_lshift_wrt_ctx_snd ctx (InVar var) (InVar var0) size H_addr_nover model mem strg exts maxidx sbindings ops H_is_model) as H_chk_lt_wshit_wrt_ctx_snd.
destruct H_chk_lt_wshit_wrt_ctx_snd as [v1 [v2 [H_chk_newq_wrt_ctx_snd_1 [H_chk_newq_wrt_ctx_snd_2 H_chk_newq_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_InVar var0 model mem strg exts maxidx sbindings ops) as H_eval_var0.
rewrite H_eval_var0 in H_chk_newq_wrt_ctx_snd_2.
injection H_chk_newq_wrt_ctx_snd_2 as H_chk_newq_wrt_ctx_snd_2.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var.
rewrite H_eval_var in H_chk_newq_wrt_ctx_snd_1.
injection H_chk_newq_wrt_ctx_snd_1 as H_chk_newq_wrt_ctx_snd_1.
rewrite <- H_eval_soffset.
rewrite <- H_eval_soffset'.
rewrite H_chk_newq_wrt_ctx_snd_1.
rewrite H_chk_newq_wrt_ctx_snd_2.
rewrite orb_true_iff.
left.
rewrite N.ltb_lt.
apply H_chk_newq_wrt_ctx_snd_3.
pose proof (chk_lt_lshift_wrt_ctx_snd ctx (InVar var0) (InVar var) size' H_addr_nover model mem strg exts maxidx sbindings ops H_is_model) as H_chk_lt_wshit_wrt_ctx_snd.
destruct H_chk_lt_wshit_wrt_ctx_snd as [v1 [v2 [H_chk_newq_wrt_ctx_snd_1 [H_chk_newq_wrt_ctx_snd_2 H_chk_newq_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_InVar var0 model mem strg exts maxidx sbindings ops) as H_eval_var0.
rewrite H_eval_var0 in H_chk_newq_wrt_ctx_snd_1.
injection H_chk_newq_wrt_ctx_snd_1 as H_chk_newq_wrt_ctx_snd_1.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var.
rewrite H_eval_var in H_chk_newq_wrt_ctx_snd_2.
injection H_chk_newq_wrt_ctx_snd_2 as H_chk_newq_wrt_ctx_snd_2.
rewrite <- H_eval_soffset.
rewrite <- H_eval_soffset'.
rewrite H_chk_newq_wrt_ctx_snd_1.
rewrite H_chk_newq_wrt_ctx_snd_2.
rewrite orb_true_iff.
right.
rewrite N.ltb_lt.
apply H_chk_newq_wrt_ctx_snd_3.
Qed.
Lemma H_mstore8_is_included_in_mstore:
forall sstack_val_cmp ctx soffset_mstore8 soffset_mstore maxidx sbindings ops,
safe_sstack_val_cmp_ext_1 sstack_val_cmp ->
valid_bindings maxidx sbindings ops ->
valid_sstack_value maxidx soffset_mstore8 ->
valid_sstack_value maxidx soffset_mstore ->
mstore8_is_included_in_mstore sstack_val_cmp ctx soffset_mstore8 soffset_mstore maxidx sbindings ops = true ->
forall model mem strg exts,
is_model (ctx_cs ctx) model = true ->
exists v1 v2,
eval_sstack_val' (S maxidx) soffset_mstore8 model mem strg exts maxidx sbindings ops = Some v1 /\
eval_sstack_val' (S maxidx) soffset_mstore model mem strg exts maxidx sbindings ops = Some v2 /\
andb ((wordToN v2) <=? (wordToN v1) )%N ((wordToN v1) <=? (wordToN v2)+31)%N = true.
Proof.
intros sstack_val_cmp ctx soffset_mstore8 soffset_mstore maxidx sbindings ops.
intros H_sstack_val_cmp_snd 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 (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 val; destruct val0; try discriminate.
intros model mem strg exts.
intros H_is_model.
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.
intros model mem strg exts H_is_model.
pose proof (eval_sstack_val'_succ (S maxidx) soffset_mstore8 model mem strg exts maxidx sbindings ops H_valid_offset_mstore8 H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset_mstore8.
pose proof (eval_sstack_val'_succ (S maxidx) soffset_mstore model mem strg exts maxidx sbindings ops H_valid_offset_mstore H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset_mstore.
destruct H_eval_soffset_mstore8 as [v_soffset_mstore8 H_eval_soffset_mstore8].
destruct H_eval_soffset_mstore as [v_soffset_mstore H_eval_soffset_mstore].
exists v_soffset_mstore8.
exists v_soffset_mstore.
repeat split; try auto.
unfold eval_sstack_val' in H_eval_soffset_mstore8.
rewrite E_follow_soffset_mstore8 in H_eval_soffset_mstore8.
injection H_eval_soffset_mstore8 as H_eval_soffset_mstore8.
unfold eval_sstack_val' in H_eval_soffset_mstore.
rewrite E_follow_soffset_mstore in H_eval_soffset_mstore.
injection H_eval_soffset_mstore as H_eval_soffset_mstore.
apply andb_prop in H_addr_not_inc.
destruct H_addr_not_inc as [H_addr_not_inc_l H_addr_not_inc_r].
pose proof (chk_le_wrt_ctx_snd ctx (InVar var) (Val val) H_addr_not_inc_l model mem strg exts maxidx sbindings ops H_is_model) as H_chk_le_wrt_ctx_snd.
destruct H_chk_le_wrt_ctx_snd as [v1 [v2 [H_chk_le_wrt_ctx_snd_1 [H_chk_le_wrt_ctx_snd_2 H_chk_le_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_Val val model mem strg exts maxidx sbindings ops) as H_eval_val.
rewrite H_eval_val in H_chk_le_wrt_ctx_snd_2.
injection H_chk_le_wrt_ctx_snd_2 as H_chk_le_wrt_ctx_snd_2.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var.
rewrite H_eval_var in H_chk_le_wrt_ctx_snd_1.
injection H_chk_le_wrt_ctx_snd_1 as H_chk_le_wrt_ctx_snd_1.
rewrite <- H_eval_soffset_mstore8.
rewrite <- H_eval_soffset_mstore.
rewrite H_chk_le_wrt_ctx_snd_1.
rewrite H_chk_le_wrt_ctx_snd_2.
pose proof (chk_le_rshift_wrt_ctx_snd ctx (Val val) (InVar var) 31%N H_addr_not_inc_r model mem strg exts maxidx sbindings ops H_is_model) as H_chk_le_rshift_wrt_ctx_snd.
destruct H_chk_le_rshift_wrt_ctx_snd as [v1' [v2' [H_chk_le_rshift_wrt_ctx_snd_1 [H_chk_le_rshift_wrt_ctx_snd_2 H_chk_le_rshift_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_Val val model mem strg exts maxidx sbindings ops) as H_eval_val_aux.
rewrite H_eval_val_aux in H_chk_le_rshift_wrt_ctx_snd_1.
injection H_chk_le_rshift_wrt_ctx_snd_1 as H_chk_le_rshift_wrt_ctx_snd_1.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var_aux.
rewrite H_eval_var_aux in H_chk_le_rshift_wrt_ctx_snd_2.
injection H_chk_le_rshift_wrt_ctx_snd_2 as H_chk_le_rshift_wrt_ctx_snd_2.
rewrite <- H_chk_le_rshift_wrt_ctx_snd_1 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite <- H_chk_le_rshift_wrt_ctx_snd_2 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite H_chk_le_wrt_ctx_snd_1 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite H_chk_le_wrt_ctx_snd_2 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite andb_true_iff.
apply N.leb_le in H_chk_le_wrt_ctx_snd_3.
apply N.leb_le in H_chk_le_rshift_wrt_ctx_snd_3.
split; try (apply H_chk_le_wrt_ctx_snd_3 || apply H_chk_le_rshift_wrt_ctx_snd_3).
intros model mem strg exts H_is_model.
pose proof (eval_sstack_val'_succ (S maxidx) soffset_mstore8 model mem strg exts maxidx sbindings ops H_valid_offset_mstore8 H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset_mstore8.
pose proof (eval_sstack_val'_succ (S maxidx) soffset_mstore model mem strg exts maxidx sbindings ops H_valid_offset_mstore H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset_mstore.
destruct H_eval_soffset_mstore8 as [v_soffset_mstore8 H_eval_soffset_mstore8].
destruct H_eval_soffset_mstore as [v_soffset_mstore H_eval_soffset_mstore].
exists v_soffset_mstore8.
exists v_soffset_mstore.
repeat split; try auto.
unfold eval_sstack_val' in H_eval_soffset_mstore8.
rewrite E_follow_soffset_mstore8 in H_eval_soffset_mstore8.
injection H_eval_soffset_mstore8 as H_eval_soffset_mstore8.
unfold eval_sstack_val' in H_eval_soffset_mstore.
rewrite E_follow_soffset_mstore in H_eval_soffset_mstore.
injection H_eval_soffset_mstore as H_eval_soffset_mstore.
apply andb_prop in H_addr_not_inc.
destruct H_addr_not_inc as [H_addr_not_inc_l H_addr_not_inc_r].
pose proof (chk_le_wrt_ctx_snd ctx (Val val) (InVar var) H_addr_not_inc_l model mem strg exts maxidx sbindings ops H_is_model) as H_chk_le_wrt_ctx_snd.
destruct H_chk_le_wrt_ctx_snd as [v1 [v2 [H_chk_le_wrt_ctx_snd_1 [H_chk_le_wrt_ctx_snd_2 H_chk_le_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_Val val model mem strg exts maxidx sbindings ops) as H_eval_val.
rewrite H_eval_val in H_chk_le_wrt_ctx_snd_1.
injection H_chk_le_wrt_ctx_snd_1 as H_chk_le_wrt_ctx_snd_1.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var.
rewrite H_eval_var in H_chk_le_wrt_ctx_snd_2.
injection H_chk_le_wrt_ctx_snd_2 as H_chk_le_wrt_ctx_snd_2.
rewrite <- H_eval_soffset_mstore8.
rewrite <- H_eval_soffset_mstore.
rewrite H_chk_le_wrt_ctx_snd_1.
rewrite H_chk_le_wrt_ctx_snd_2.
pose proof (chk_le_rshift_wrt_ctx_snd ctx (InVar var) (Val val) 31%N H_addr_not_inc_r model mem strg exts maxidx sbindings ops H_is_model) as H_chk_le_rshift_wrt_ctx_snd.
destruct H_chk_le_rshift_wrt_ctx_snd as [v1' [v2' [H_chk_le_rshift_wrt_ctx_snd_1 [H_chk_le_rshift_wrt_ctx_snd_2 H_chk_le_rshift_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_Val val model mem strg exts maxidx sbindings ops) as H_eval_val_aux.
rewrite H_eval_val_aux in H_chk_le_rshift_wrt_ctx_snd_2.
injection H_chk_le_rshift_wrt_ctx_snd_2 as H_chk_le_rshift_wrt_ctx_snd_2.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var_aux.
rewrite H_eval_var_aux in H_chk_le_rshift_wrt_ctx_snd_1.
injection H_chk_le_rshift_wrt_ctx_snd_1 as H_chk_le_rshift_wrt_ctx_snd_1.
rewrite <- H_chk_le_rshift_wrt_ctx_snd_1 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite <- H_chk_le_rshift_wrt_ctx_snd_2 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite H_chk_le_wrt_ctx_snd_1 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite H_chk_le_wrt_ctx_snd_2 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite andb_true_iff.
apply N.leb_le in H_chk_le_wrt_ctx_snd_3.
apply N.leb_le in H_chk_le_rshift_wrt_ctx_snd_3.
split; try (apply H_chk_le_wrt_ctx_snd_3 || apply H_chk_le_rshift_wrt_ctx_snd_3).
intros model mem strg exts H_is_model.
pose proof (eval_sstack_val'_succ (S maxidx) soffset_mstore8 model mem strg exts maxidx sbindings ops H_valid_offset_mstore8 H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset_mstore8.
pose proof (eval_sstack_val'_succ (S maxidx) soffset_mstore model mem strg exts maxidx sbindings ops H_valid_offset_mstore H_valid_sbindings (gt_Sn_n maxidx)) as H_eval_soffset_mstore.
destruct H_eval_soffset_mstore8 as [v_soffset_mstore8 H_eval_soffset_mstore8].
destruct H_eval_soffset_mstore as [v_soffset_mstore H_eval_soffset_mstore].
exists v_soffset_mstore8.
exists v_soffset_mstore.
repeat split; try auto.
unfold eval_sstack_val' in H_eval_soffset_mstore8.
rewrite E_follow_soffset_mstore8 in H_eval_soffset_mstore8.
injection H_eval_soffset_mstore8 as H_eval_soffset_mstore8.
unfold eval_sstack_val' in H_eval_soffset_mstore.
rewrite E_follow_soffset_mstore in H_eval_soffset_mstore.
injection H_eval_soffset_mstore as H_eval_soffset_mstore.
apply andb_prop in H_addr_not_inc.
destruct H_addr_not_inc as [H_addr_not_inc_l H_addr_not_inc_r].
pose proof (chk_le_wrt_ctx_snd ctx (InVar var0) (InVar var) H_addr_not_inc_l model mem strg exts maxidx sbindings ops H_is_model) as H_chk_le_wrt_ctx_snd.
destruct H_chk_le_wrt_ctx_snd as [v1 [v2 [H_chk_le_wrt_ctx_snd_1 [H_chk_le_wrt_ctx_snd_2 H_chk_le_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_InVar var0 model mem strg exts maxidx sbindings ops) as H_eval_var0.
rewrite H_eval_var0 in H_chk_le_wrt_ctx_snd_1.
injection H_chk_le_wrt_ctx_snd_1 as H_chk_le_wrt_ctx_snd_1.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var.
rewrite H_eval_var in H_chk_le_wrt_ctx_snd_2.
injection H_chk_le_wrt_ctx_snd_2 as H_chk_le_wrt_ctx_snd_2.
rewrite <- H_eval_soffset_mstore8.
rewrite <- H_eval_soffset_mstore.
rewrite H_chk_le_wrt_ctx_snd_1.
rewrite H_chk_le_wrt_ctx_snd_2.
pose proof (chk_le_rshift_wrt_ctx_snd ctx (InVar var) (InVar var0) 31%N H_addr_not_inc_r model mem strg exts maxidx sbindings ops H_is_model) as H_chk_le_rshift_wrt_ctx_snd.
destruct H_chk_le_rshift_wrt_ctx_snd as [v1' [v2' [H_chk_le_rshift_wrt_ctx_snd_1 [H_chk_le_rshift_wrt_ctx_snd_2 H_chk_le_rshift_wrt_ctx_snd_3]]]].
pose proof (eval_sstack_val_InVar var0 model mem strg exts maxidx sbindings ops) as H_eval_var0_aux.
rewrite H_eval_var0_aux in H_chk_le_rshift_wrt_ctx_snd_2.
injection H_chk_le_rshift_wrt_ctx_snd_2 as H_chk_le_rshift_wrt_ctx_snd_2.
pose proof (eval_sstack_val_InVar var model mem strg exts maxidx sbindings ops) as H_eval_var_aux.
rewrite H_eval_var_aux in H_chk_le_rshift_wrt_ctx_snd_1.
injection H_chk_le_rshift_wrt_ctx_snd_1 as H_chk_le_rshift_wrt_ctx_snd_1.
rewrite <- H_chk_le_rshift_wrt_ctx_snd_1 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite <- H_chk_le_rshift_wrt_ctx_snd_2 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite H_chk_le_wrt_ctx_snd_1 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite H_chk_le_wrt_ctx_snd_2 in H_chk_le_rshift_wrt_ctx_snd_3.
rewrite andb_true_iff.
apply N.leb_le in H_chk_le_wrt_ctx_snd_3.
apply N.leb_le in H_chk_le_rshift_wrt_ctx_snd_3.
split; try (apply H_chk_le_wrt_ctx_snd_3 || apply H_chk_le_rshift_wrt_ctx_snd_3).
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 ctx m smem soffset 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)) ctx soffset soffset' (get_maxidx_smap m) (get_bindings_smap m) (get_maxidx_smap m) (get_bindings_smap m) ops) eqn:E_soffset_soffset'_cmp.
+++ rewrite <- H_basic_solver.
simpl.
apply H_valid_smem.
+++ destruct (memory_slots_do_not_overlap ctx 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 ctx 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 ctx d model mem strg exts maxidx bs ops smem,
valid_smemory maxidx smem ->
valid_bindings maxidx bs ops ->
d > maxidx ->
is_model (ctx_cs ctx) model = true ->
exists v,
map_option (eval_common.EvalCommon.instantiate_memory_update (fun sv : sstack_val => eval_sstack_val' d sv model 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_is_model.
unfold map_option.
rewrite <- map_option_ho.
unfold eval_common.EvalCommon.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 soffset' model mem strg exts maxidx bs ops 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 svalue' model mem strg exts maxidx bs ops 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_is_model) 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 soffset' model mem strg exts maxidx bs ops 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 svalue' model mem strg exts maxidx bs ops 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_is_model) 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 concrete_interpreter.ConcreteInterpreter.split1_byte value0
else mstore' sz1' mem0 (concrete_interpreter.ConcreteInterpreter.split2_byte value0) (offset + 1)%N offset'0
end) sz mem value addr = concrete_interpreter.ConcreteInterpreter.mstore' mem value addr.
Proof.
auto.
Qed.
Lemma mload''_aux:
forall n addr addr' x y,
(addr' > addr)%N ->
(concrete_interpreter.ConcreteInterpreter.mload''
(fun offset' : N =>
if (offset' =? addr)%N
then x
else y offset') addr' n) =
(concrete_interpreter.ConcreteInterpreter.mload'' y addr' n).
Proof.
induction n as [|n' IHn'].
+ intros.
simpl.
reflexivity.
+ intros addr addr' x y H_addr'_gt_addr'.
unfold concrete_interpreter.ConcreteInterpreter.mload'' at 1.
fold concrete_interpreter.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 concrete_interpreter.ConcreteInterpreter.mload'' at 2.
fold concrete_interpreter.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,
concrete_interpreter.ConcreteInterpreter.mload'' (concrete_interpreter.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 concrete_interpreter.ConcreteInterpreter.mstore'.
rewrite mstore'_aux.
unfold concrete_interpreter.ConcreteInterpreter.mload''.
rewrite N.eqb_refl.
fold concrete_interpreter.ConcreteInterpreter.mload''.
destruct n' as [|n''] eqn:E_n'.
++ unfold concrete_interpreter.ConcreteInterpreter.mload''.
unfold concrete_interpreter.ConcreteInterpreter.split1_byte.
unfold concrete_interpreter.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 (concrete_interpreter.ConcreteInterpreter.split2_byte value)) as IHn'_0.
rewrite IHn'_0.
unfold concrete_interpreter.ConcreteInterpreter.split1_byte.
unfold concrete_interpreter.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,
(concrete_interpreter.ConcreteInterpreter.mload
(concrete_interpreter.ConcreteInterpreter.mstore mem value addr) addr) = value.
Proof.
intros mem addr value.
unfold concrete_interpreter.ConcreteInterpreter.mload.
unfold concrete_interpreter.ConcreteInterpreter.mload'.
unfold concrete_interpreter.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 ->
(concrete_interpreter.ConcreteInterpreter.mload'' (eval_common.EvalCommon.update_memory mem (U_MSTORE EVMWord offset' value' :: updates)) (wordToN offset) 32) =
(concrete_interpreter.ConcreteInterpreter.mload'' (eval_common.EvalCommon.update_memory mem updates) (wordToN (offset : EVMWord)) 32).
Proof.
intros mem offset offset' value' updates H_o.
unfold concrete_interpreter.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 ->
(concrete_interpreter.ConcreteInterpreter.mload'' (eval_common.EvalCommon.update_memory mem (U_MSTORE8 EVMWord offset' value' :: updates)) (wordToN offset) 32) =
(concrete_interpreter.ConcreteInterpreter.mload'' (eval_common.EvalCommon.update_memory mem updates) (wordToN (offset : EVMWord)) 32).
Proof.
Proof.
intros mem offset offset' value' updates H_o.
unfold concrete_interpreter.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.