-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathvalid_symbolic_state.v
1163 lines (1028 loc) · 33.2 KB
/
valid_symbolic_state.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.constraints.
Import Constraints.
Module ValidSymbolicState.
Definition valid_sstack_value (maxidx: nat) (value : sstack_val) : Prop :=
match value with
| Val _ => True
| InVar _ => True
| FreshVar idx => idx < maxidx
end.
(* All the FreshVar in the sstack are less than maxidx *)
Fixpoint valid_sstack (maxidx: nat) (sstk : sstack) : Prop :=
match sstk with
| [] => True
| sv::sstk' => valid_sstack_value maxidx sv /\ valid_sstack maxidx sstk'
end.
Definition valid_smemory_update (maxidx: nat) (u : memory_update sstack_val) : Prop :=
match u with
| U_MSTORE _ offset value | U_MSTORE8 _ offset value => valid_sstack_value maxidx offset /\ valid_sstack_value maxidx value
end.
Fixpoint valid_smemory (maxidx: nat) (smem : smemory) : Prop :=
match smem with
| [] => True
| u::smem' => valid_smemory_update maxidx u /\ valid_smemory maxidx smem'
end.
Definition valid_sstorage_update (maxidx: nat) (u : storage_update sstack_val) : Prop :=
match u with
| U_SSTORE _ offset value => valid_sstack_value maxidx offset /\ valid_sstack_value maxidx value
end.
Fixpoint valid_sstorage (maxidx: nat) (sstrg : sstorage) : Prop :=
match sstrg with
| [] => True
| u::sstrg' => valid_sstorage_update maxidx u /\ valid_sstorage maxidx sstrg'
end.
Definition valid_stack_op_instr (maxidx: nat) (ops: stack_op_instr_map) (label: stack_op_instr) (args: list sstack_val): Prop :=
match (ops label) with
| OpImp nargs _ _ _ => length args = nargs /\ valid_sstack maxidx args
end.
Definition valid_smap_value (maxidx: nat) (ops: stack_op_instr_map) (value: smap_value) : Prop :=
match value with
| SymBasicVal v => valid_sstack_value maxidx v
| SymMETAPUSH _ _ => True
| SymOp label args => valid_stack_op_instr maxidx ops label args
| SymMLOAD offset smem => valid_sstack_value maxidx offset /\ valid_smemory maxidx smem
| SymSLOAD key sstrg => valid_sstack_value maxidx key /\ valid_sstorage maxidx sstrg
| SymSHA3 offset size smem => valid_sstack_value maxidx offset /\ valid_sstack_value maxidx size /\ valid_smemory maxidx smem
end.
(* all keys defined *)
Fixpoint valid_bindings (maxid: nat) (sb: sbindings) (ops: stack_op_instr_map): Prop :=
match sb with
| [] => maxid = 0
| (idx,value)::sb' => maxid = (S idx) /\ valid_smap_value idx ops value /\ valid_bindings idx sb' ops
end.
Definition valid_smap (maxidx: nat) (sb: sbindings) (ops: stack_op_instr_map): Prop :=
valid_bindings maxidx sb ops.
Definition valid_sstate (sst: sstate) (ops: stack_op_instr_map): Prop :=
let sstk := get_stack_sst sst in
let smem := get_memory_sst sst in
let sstrg := get_storage_sst sst in
let m := get_smap_sst sst in
let maxidx := get_maxidx_smap m in
let sb := get_bindings_smap m in
valid_smap maxidx sb ops /\
valid_sstack maxidx sstk /\
valid_smemory maxidx smem /\
valid_sstorage maxidx sstrg.
(* Valid state checker *)
Definition chk_valid_sstack_value (maxidx: nat) (value : sstack_val) : bool :=
match value with
| Val _ => true
| InVar _ => true
| FreshVar idx => idx <? maxidx
end.
(* All the FreshVar in the sstack are less than maxidx *)
Fixpoint chk_valid_sstack (maxidx: nat) (sstk : sstack) : bool :=
match sstk with
| [] => true
| sv::sstk' => chk_valid_sstack_value maxidx sv && chk_valid_sstack maxidx sstk'
end.
Definition chk_valid_smemory_update (maxidx: nat) (u : memory_update sstack_val) : bool :=
match u with
| U_MSTORE _ offset value | U_MSTORE8 _ offset value => chk_valid_sstack_value maxidx offset && chk_valid_sstack_value maxidx value
end.
Fixpoint chk_valid_smemory (maxidx: nat) (smem : smemory) : bool :=
match smem with
| [] => true
| u::smem' => chk_valid_smemory_update maxidx u && chk_valid_smemory maxidx smem'
end.
Definition chk_valid_sstorage_update (maxidx: nat) (u : storage_update sstack_val) : bool :=
match u with
| U_SSTORE _ offset value => chk_valid_sstack_value maxidx offset && chk_valid_sstack_value maxidx value
end.
Fixpoint chk_valid_sstorage (maxidx: nat) (sstrg : sstorage) : bool :=
match sstrg with
| [] => true
| u::sstrg' => chk_valid_sstorage_update maxidx u && chk_valid_sstorage maxidx sstrg'
end.
Definition chk_valid_stack_op_instr (maxidx: nat) (ops: stack_op_instr_map) (label: stack_op_instr) (args: list sstack_val): bool :=
match (ops label) with
| OpImp nargs _ _ _ => (length args =? nargs) && chk_valid_sstack maxidx args
end.
Definition chk_valid_smap_value (maxidx: nat) (ops: stack_op_instr_map) (value: smap_value) : bool :=
match value with
| SymBasicVal v => chk_valid_sstack_value maxidx v
| SymMETAPUSH _ _ => true
| SymOp label args => chk_valid_stack_op_instr maxidx ops label args
| SymMLOAD offset smem => chk_valid_sstack_value maxidx offset && chk_valid_smemory maxidx smem
| SymSLOAD key sstrg => chk_valid_sstack_value maxidx key && chk_valid_sstorage maxidx sstrg
| SymSHA3 offset size smem => chk_valid_sstack_value maxidx offset && chk_valid_sstack_value maxidx size && chk_valid_smemory maxidx smem
end.
Fixpoint chk_valid_bindings (maxid: nat) (sb: sbindings) (ops: stack_op_instr_map): bool :=
match sb with
| [] => maxid =? 0
| (idx,value)::sb' => (maxid =? (S idx)) && chk_valid_smap_value idx ops value && chk_valid_bindings idx sb' ops
end.
Definition chk_valid_smap (maxidx: nat) (sb: sbindings) (ops: stack_op_instr_map): bool :=
chk_valid_bindings maxidx sb ops.
Definition chk_valid_sstate (sst: sstate) (ops: stack_op_instr_map): bool :=
let sstk := get_stack_sst sst in
let smem := get_memory_sst sst in
let sstrg := get_storage_sst sst in
let m := get_smap_sst sst in
let maxidx := get_maxidx_smap m in
let sb := get_bindings_smap m in
chk_valid_smap maxidx sb ops &&
chk_valid_sstack maxidx sstk &&
chk_valid_smemory maxidx smem &&
chk_valid_sstorage maxidx sstrg.
Lemma chk_valid_sstack_value_snd:
forall maxidx sv,
chk_valid_sstack_value maxidx sv = true -> valid_sstack_value maxidx sv.
Proof.
intros maxidx sv H_chk.
unfold chk_valid_sstack_value in H_chk.
unfold valid_sstack_value.
destruct sv; try apply I.
rewrite <- Nat.ltb_lt.
apply H_chk.
Qed.
Lemma chk_valid_smemory_update_snd:
forall maxidx u,
chk_valid_smemory_update maxidx u = true -> valid_smemory_update maxidx u.
Proof.
intros maxidx u H_chk.
destruct u as [soffset svalue | soffset svalue].
+ simpl in H_chk.
apply andb_prop in H_chk.
destruct H_chk as [H_chk_soffset H_chk_svalue].
apply chk_valid_sstack_value_snd in H_chk_soffset.
apply chk_valid_sstack_value_snd in H_chk_svalue.
unfold valid_smemory_update.
split; auto.
+ simpl in H_chk.
apply andb_prop in H_chk.
destruct H_chk as [H_chk_soffset H_chk_svalue].
apply chk_valid_sstack_value_snd in H_chk_soffset.
apply chk_valid_sstack_value_snd in H_chk_svalue.
unfold valid_smemory_update.
split; auto.
Qed.
Lemma chk_valid_sstorage_update_snd:
forall maxidx u,
chk_valid_sstorage_update maxidx u = true -> valid_sstorage_update maxidx u.
Proof.
intros maxidx u H_chk.
destruct u as [skey svalue].
simpl in H_chk.
apply andb_prop in H_chk.
destruct H_chk as [H_chk_skey H_chk_svalue].
apply chk_valid_sstack_value_snd in H_chk_skey.
apply chk_valid_sstack_value_snd in H_chk_svalue.
unfold valid_sstorage_update.
split; auto.
Qed.
Lemma chk_valid_smemory_snd:
forall maxidx smem,
chk_valid_smemory maxidx smem = true -> valid_smemory maxidx smem.
Proof.
intros maxidx.
induction smem as [|u smem' IHsmem'].
+ intros H_chk.
simpl.
apply I.
+ intros H_chk.
simpl in H_chk.
apply andb_prop in H_chk.
destruct H_chk as [H_chk_u H_chk_smem'].
apply IHsmem' in H_chk_smem'.
apply chk_valid_smemory_update_snd in H_chk_u.
unfold valid_smemory.
fold valid_smemory.
split; auto.
Qed.
Lemma chk_valid_sstorage_snd:
forall maxidx sstrg,
chk_valid_sstorage maxidx sstrg = true -> valid_sstorage maxidx sstrg.
Proof.
intros maxidx.
induction sstrg as [|u sstrg' IHsstrg'].
+ intros H_chk.
simpl.
apply I.
+ intros H_chk.
simpl in H_chk.
apply andb_prop in H_chk.
destruct H_chk as [H_chk_u H_chk_sstrg'].
apply IHsstrg' in H_chk_sstrg'.
apply chk_valid_sstorage_update_snd in H_chk_u.
unfold valid_sstorage.
fold valid_sstorage.
split; auto.
Qed.
Lemma chk_valid_sstack_snd:
forall maxidx sstk,
chk_valid_sstack maxidx sstk = true -> valid_sstack maxidx sstk.
Proof.
intros maxidx.
induction sstk as [|sv sstk' IHsstk'].
+ intros H_chk.
simpl.
apply I.
+ intros H_chk.
simpl in H_chk.
apply andb_prop in H_chk.
destruct H_chk as [H_chk_sv H_chk_sstk'].
apply IHsstk' in H_chk_sstk'.
apply chk_valid_sstack_value_snd in H_chk_sv.
unfold valid_sstack.
fold valid_sstack.
split; auto.
Qed.
Lemma chk_valid_stack_op_instr_snd:
forall maxidx ops label args,
chk_valid_stack_op_instr maxidx ops label args = true -> valid_stack_op_instr maxidx ops label args.
Proof.
intros maxidx ops label args H_chk.
unfold chk_valid_stack_op_instr in H_chk.
unfold valid_stack_op_instr.
destruct (ops label).
apply andb_prop in H_chk.
destruct H_chk as [H_chk_len H_chk_args].
rewrite Nat.eqb_eq in H_chk_len.
apply chk_valid_sstack_snd in H_chk_args.
split; auto.
Qed.
Lemma chk_valid_smap_value_snd:
forall maxidx ops value,
chk_valid_smap_value maxidx ops value = true -> valid_smap_value maxidx ops value.
Proof.
intros maxidx ops value H_chk.
destruct value.
+ simpl in H_chk.
simpl.
apply chk_valid_sstack_value_snd in H_chk.
apply H_chk.
+ simpl.
apply I.
+ simpl in H_chk.
apply chk_valid_stack_op_instr_snd in H_chk.
simpl.
apply H_chk.
+ simpl in H_chk.
apply andb_prop in H_chk.
destruct H_chk as [H_chk_offset H_chk_smem].
apply chk_valid_sstack_value_snd in H_chk_offset.
apply chk_valid_smemory_snd in H_chk_smem.
simpl.
split; auto.
+ simpl in H_chk.
apply andb_prop in H_chk.
destruct H_chk as [H_chk_key H_chk_sstrg].
apply chk_valid_sstack_value_snd in H_chk_key.
apply chk_valid_sstorage_snd in H_chk_sstrg.
simpl.
split; auto.
+ simpl in H_chk.
apply andb_prop in H_chk.
destruct H_chk as [H_chk H_chk_smem].
apply andb_prop in H_chk.
destruct H_chk as [H_chk_offset H_chk_size].
apply chk_valid_sstack_value_snd in H_chk_offset.
apply chk_valid_sstack_value_snd in H_chk_size.
apply chk_valid_smemory_snd in H_chk_smem.
simpl.
split; auto.
Qed.
Lemma chk_valid_bindings_snd:
forall maxidx sb ops,
chk_valid_bindings maxidx sb ops = true -> valid_bindings maxidx sb ops.
Proof.
intros maxidx sb ops.
revert maxidx.
revert sb.
induction sb as [|b sb' IHsb'].
+ intros maxidx H_chk.
simpl.
destruct maxidx as [| maxidx'].
++ reflexivity.
++ simpl in H_chk.
discriminate.
+ intros maxidx H_chk.
simpl in H_chk.
destruct b as [idx value].
apply andb_prop in H_chk.
destruct H_chk as [H_chk H_chk_sb'].
apply andb_prop in H_chk.
destruct H_chk as [H_chk_maxidx H_chk_value].
apply chk_valid_smap_value_snd in H_chk_value.
apply IHsb' in H_chk_sb'.
rewrite Nat.eqb_eq in H_chk_maxidx.
simpl.
split; auto.
Qed.
Lemma chk_valid_smap_snd:
forall maxidx sb ops,
chk_valid_smap maxidx sb ops = true -> valid_smap maxidx sb ops.
Proof.
apply chk_valid_bindings_snd.
Qed.
Lemma chk_valid_sstate_snd:
forall sst ops,
chk_valid_sstate sst ops = true -> valid_sstate sst ops.
Proof.
intros sst ops H_chk_valid_sst.
unfold chk_valid_sstate in H_chk_valid_sst.
apply andb_prop in H_chk_valid_sst.
destruct H_chk_valid_sst as [H_chk_valid_sst H_chk_valid_sstrorage].
apply chk_valid_sstorage_snd in H_chk_valid_sstrorage.
apply andb_prop in H_chk_valid_sst.
destruct H_chk_valid_sst as [H_chk_valid_sst H_chk_valid_smemory].
apply chk_valid_smemory_snd in H_chk_valid_smemory.
apply andb_prop in H_chk_valid_sst.
destruct H_chk_valid_sst as [H_chk_valid_smap H_chk_valid_sstack].
apply chk_valid_sstack_snd in H_chk_valid_sstack.
apply chk_valid_smap_snd in H_chk_valid_smap.
unfold valid_sstate.
split; try auto.
Qed.
(*Lemma fresh_var_gt_map_maxidx_S:
forall sb maxidx,
fresh_var_gt_map maxidx sb ->
fresh_var_gt_map (S maxidx) sb.
Proof.
induction sb as [|v sb' IHsm'].
- auto.
- intros.
unfold fresh_var_gt_map in H.
fold fresh_var_gt_map in H.
destruct v as [k kvalue].
destruct H.
unfold fresh_var_gt_map.
fold fresh_var_gt_map.
split.
+ auto.
+ apply IHsm'.
apply H0.
Qed.*)
Lemma valid_sstack_app:
forall maxidx l1 l2,
valid_sstack maxidx l1 ->
valid_sstack maxidx l2 ->
valid_sstack maxidx (l1++l2).
Proof.
intros maxidx.
induction l1 as [|sv l1' IHl1'].
- intros l2 H_l1 H_l2.
simpl.
apply H_l2.
- intros l2 H_l1 H_l2.
simpl in H_l1.
destruct H_l1 as [H_l1_0 H_l1_1].
simpl.
split.
+ apply H_l1_0.
+ apply IHl1'.
* apply H_l1_1.
* apply H_l2.
Qed.
Lemma valid_sstack_app1:
forall maxidx l1 l2,
valid_sstack maxidx (l1++l2) ->
valid_sstack maxidx l1 /\
valid_sstack maxidx l2.
Proof.
intros maxidx.
induction l1 as [|sv l1' IHl1'].
- intros l2 H_l1_l2.
simpl.
simpl in H_l1_l2.
split.
+ apply I.
+ apply H_l1_l2.
- intros l2 H_l1_l2.
simpl in H_l1_l2.
destruct H_l1_l2 as [H_sv H_l1'_l2].
simpl.
pose proof (IHl1' l2 H_l1'_l2) as [IHl1'_0 IHl1'_1].
split.
+ split.
* apply H_sv.
* apply IHl1'_0.
+ apply IHl1'_1.
Qed.
Lemma valid_sstack_value_S_maxidx:
forall maxidx sv,
valid_sstack_value maxidx sv ->
valid_sstack_value (S maxidx) sv.
Proof.
intros maxidx sv H_valid_sv.
destruct sv; simpl; try auto.
Qed.
(*
(* TODO: This lemma becomes obsolete after removing instk_height *)
Lemma valid_sstack_value_S_instk_height:
forall maxidx sv,
valid_sstack_value maxidx sv ->
valid_sstack_value maxidx sv.
Proof.
intros maxidx sv H_valid_sv.
destruct sv; simpl; try auto.
Qed.
*)
Lemma valid_sstack_S_maxidx:
forall maxidx l,
valid_sstack maxidx l ->
valid_sstack (S maxidx) l.
Proof.
intros maxidx.
induction l as [|sv l' IHl'].
- intuition.
- simpl.
intros H_l.
destruct H_l as [H_l_0 H_l_1].
split.
+ apply valid_sstack_value_S_maxidx. apply H_l_0.
+ apply IHl'. apply H_l_1.
Qed.
Lemma add_to_smap_valid_smap:
forall idx m m' smv ops,
valid_smap (get_maxidx_smap m) (get_bindings_smap m) ops ->
valid_smap_value (get_maxidx_smap m) ops smv ->
add_to_smap m smv = (idx, m') ->
valid_smap (get_maxidx_smap m') (get_bindings_smap m') ops.
Proof.
intros idx m m' smv ops H_valid_m H_valid_smv H_add.
destruct m as [maxidx sb] eqn:E_m.
destruct m' as [maxidx' sb'] eqn:E_m'.
unfold valid_smap in H_valid_m.
assert(H_add' := H_add).
simpl in H_add'.
injection H_add' as H_maxidx H_maxidx' H_sb'.
unfold valid_smap.
rewrite <- H_sb'.
simpl.
split.
* intuition.
* simpl in H_valid_smv.
split.
** apply H_valid_smv.
** simpl in H_valid_m.
apply H_valid_m.
Qed.
Lemma add_to_smap_valid_sstack:
forall idx m m' smv sstk ops,
valid_sstack (get_maxidx_smap m) sstk ->
valid_smap_value (get_maxidx_smap m) ops smv ->
add_to_smap m smv = (idx, m') ->
valid_sstack (get_maxidx_smap m') sstk.
Proof.
intros idx m m' smv sstk ops H_valid_sstk H_valid_smv H_add_to_map.
destruct m as [maxid sb] eqn:E_m.
destruct m' as [maxid' sb'] eqn:E_m'.
assert (H_add_to_map' := H_add_to_map).
unfold add_to_smap in H_add_to_map'.
injection H_add_to_map' as H_maxid H_maxid' H_sb'.
simpl.
simpl in H_valid_sstk.
simpl in H_valid_smv.
rewrite <- H_maxid'.
apply valid_sstack_S_maxidx.
apply H_valid_sstk.
Qed.
Lemma add_to_smap_valid_sstack_value:
forall idx m m' smv sv ops,
valid_sstack_value (get_maxidx_smap m) sv ->
valid_smap_value (get_maxidx_smap m) ops smv ->
add_to_smap m smv = (idx, m') ->
valid_sstack_value (get_maxidx_smap m') sv.
Proof.
intros idx m m' smv sv ops H_valid_sv H_valid_smv H_add_to_smap.
destruct m as [maxid sb] eqn:E_m.
destruct m' as [maxid' sb'] eqn:E_m'.
simpl.
simpl in H_valid_sv.
simpl in H_valid_smv.
simpl in H_add_to_smap.
injection H_add_to_smap as H_maxidx H_maxidx' H_sb'.
rewrite <- H_maxidx'.
apply valid_sstack_value_S_maxidx.
apply H_valid_sv.
Qed.
(*
Lemma valid_sbinings_S_maxidx:
forall instk_height maxidx ops u sb,
valid_bindings instk_height maxidx (u::sb) ops ->
valid_bindings instk_height (S maxidx) (u::sb) ops.
Proof.
intros instk_height maxidx ops u sb.
revert sb.
induction sb as [|x sb' IHsb'].
- intros H_maxidx.
destruct u.
simpl in H_maxidx.
destruct maxidx; try discriminate.
simpl.
*)
Lemma valid_smemory_update_S_maxidx:
forall maxidx u,
valid_smemory_update maxidx u ->
valid_smemory_update (S maxidx) u.
Proof.
intros maxidx u H_valid_u.
destruct u as [offset value|offset value].
- simpl.
simpl in H_valid_u.
destruct H_valid_u as [H_valid_u_0 H_valid_u_1].
split.
+ apply valid_sstack_value_S_maxidx.
apply H_valid_u_0.
+ apply valid_sstack_value_S_maxidx.
apply H_valid_u_1.
- simpl.
simpl in H_valid_u.
destruct H_valid_u as [H_valid_u_0 H_valid_u_1].
split.
+ apply valid_sstack_value_S_maxidx.
apply H_valid_u_0.
+ apply valid_sstack_value_S_maxidx.
apply H_valid_u_1.
Qed.
Lemma valid_smemory_S_maxidx:
forall maxidx smem,
valid_smemory maxidx smem ->
valid_smemory (S maxidx) smem.
Proof.
intros maxidx.
induction smem as [|u smem' IHsmem'].
- auto.
- simpl.
intro H_valid_smem.
destruct H_valid_smem as [H_valid_smem_0 H_valid_smem_1].
split.
+ apply valid_smemory_update_S_maxidx.
apply H_valid_smem_0.
+ apply IHsmem'.
apply H_valid_smem_1.
Qed.
Lemma valid_sstorage_update_S_maxidx:
forall maxidx u,
valid_sstorage_update maxidx u ->
valid_sstorage_update (S maxidx) u.
Proof.
intros maxidx u H_valid_u.
destruct u as [offset value].
simpl.
simpl in H_valid_u.
destruct H_valid_u as [H_valid_u_0 H_valid_u_1].
split.
+ apply valid_sstack_value_S_maxidx.
apply H_valid_u_0.
+ apply valid_sstack_value_S_maxidx.
apply H_valid_u_1.
Qed.
Lemma valid_sstorage_S_maxidx:
forall maxidx sstrg,
valid_sstorage maxidx sstrg ->
valid_sstorage (S maxidx) sstrg.
Proof.
intros maxidx.
induction sstrg as [|u sstrg' IHsstrg'].
- auto.
- simpl.
intro H_valid_sstrg.
destruct H_valid_sstrg as [H_valid_sstrg_0 H_valid_sstrg_1].
split.
+ apply valid_sstorage_update_S_maxidx.
apply H_valid_sstrg_0.
+ apply IHsstrg'.
apply H_valid_sstrg_1.
Qed.
Lemma add_to_smap_valid_smemory:
forall idx m m' smv smem ops,
valid_smemory (get_maxidx_smap m) smem ->
valid_smap_value (get_maxidx_smap m) ops smv ->
add_to_smap m smv = (idx, m') ->
valid_smemory (get_maxidx_smap m') smem.
Proof.
intros idx m m' smv smem ops H_valid_smem H_valid_smv H_add_to_map.
destruct m as [maxid sb] eqn:E_m.
destruct m' as [maxid' sb'] eqn:E_m'.
assert (H_add_to_map' := H_add_to_map).
unfold add_to_smap in H_add_to_map'.
injection H_add_to_map' as H_maxid H_maxid' H_sb'.
rewrite <- H_sb'.
simpl.
rewrite <- H_maxid'.
apply valid_smemory_S_maxidx.
simpl in H_valid_smem.
apply H_valid_smem.
Qed.
Lemma add_to_smap_valid_sstorage:
forall idx m m' smv sstrg ops,
valid_sstorage (get_maxidx_smap m) sstrg ->
valid_smap_value (get_maxidx_smap m) ops smv ->
add_to_smap m smv = (idx, m') ->
valid_sstorage (get_maxidx_smap m') sstrg.
Proof.
intros idx m m' smv sstrg ops H_valid_sstrg H_valid_smv H_add_to_map.
destruct m as [maxid sb] eqn:E_m.
destruct m' as [maxid' sb'] eqn:E_m'.
assert (H_add_to_map' := H_add_to_map).
unfold add_to_smap in H_add_to_map'.
injection H_add_to_map' as H_maxid H_maxid' H_sb'.
rewrite <- H_sb'.
simpl.
rewrite <- H_maxid'.
apply valid_sstorage_S_maxidx.
simpl in H_valid_sstrg.
apply H_valid_sstrg.
Qed.
Lemma add_to_map_valid_sstate:
forall sst idx m smv ops,
valid_sstate sst ops ->
valid_smap_value (get_maxidx_smap (get_smap_sst sst)) ops smv ->
(idx,m) = add_to_smap (get_smap_sst sst) smv ->
valid_sstate (set_smap_sst sst m) ops.
Proof.
intros sst idx m smv ops.
unfold valid_sstate.
rewrite set_and_then_get_smap_sst.
rewrite sstack_preserved_when_updating_smap_sst.
rewrite smemory_preserved_when_updating_smap_sst.
rewrite sstorage_preserved_when_updating_smap_sst.
intros H_valid_sst H_valid_smap_value H_add_to_smap.
destruct H_valid_sst as [H_valid_sst_0 [H_valid_sst_1 [H_valid_sst_2 H_valid_sst_3]]].
split.
(* The case of smap *)
- symmetry in H_add_to_smap.
pose proof (add_to_smap_valid_smap idx (get_smap_sst sst) m smv ops H_valid_sst_0 H_valid_smap_value H_add_to_smap) as H_add_to_smap_valid_smap.
apply H_add_to_smap_valid_smap.
- split.
(* The case of ssstack *)
+ symmetry in H_add_to_smap.
pose proof (add_to_smap_valid_sstack idx (get_smap_sst sst) m smv (get_stack_sst sst) ops H_valid_sst_1 H_valid_smap_value H_add_to_smap) as H_add_to_smap_valid_sstack.
apply H_add_to_smap_valid_sstack.
+ split.
(* The case of smemory *)
* symmetry in H_add_to_smap.
pose proof (add_to_smap_valid_smemory idx (get_smap_sst sst) m smv (get_memory_sst sst) ops H_valid_sst_2 H_valid_smap_value H_add_to_smap) as H_add_to_smap_valid_smemory.
apply H_add_to_smap_valid_smemory.
(* The case of sstorage *)
* symmetry in H_add_to_smap.
pose proof (add_to_smap_valid_sstorage idx (get_smap_sst sst) m smv (get_storage_sst sst) ops H_valid_sst_3 H_valid_smap_value H_add_to_smap) as H_add_to_smap_valid_sstorage.
apply H_add_to_smap_valid_sstorage.
Qed.
(* when adding a value of the map, it key is smaller that maxidx of the new map *)
Lemma add_to_smap_key_lt_maxidx:
forall m m' key smv,
(key,m') = add_to_smap m smv ->
key < get_maxidx_smap m'.
Proof.
intros m m' key smv H_add_to_smap.
destruct m as [maxid sb].
simpl in H_add_to_smap.
injection H_add_to_smap as H_maxid H_m'.
rewrite H_m'.
simpl.
rewrite H_maxid.
apply Nat.lt_succ_diag_r.
Qed.
Lemma valid_follow_in_smap:
forall sb sv maxidx ops smv maxidx' sb',
valid_sstack_value maxidx sv ->
valid_bindings maxidx sb ops ->
follow_in_smap sv maxidx sb = Some (FollowSmapVal smv maxidx' sb') ->
valid_smap_value maxidx' ops smv /\
valid_bindings maxidx' sb' ops /\
(not_basic_value_smv smv = true -> maxidx > maxidx').
Proof.
induction sb as [|p sb'' IHsb''].
- intros sv maxidx ops smv maxidx' sb' H_valid_sv H_valid_sb H_follow.
destruct sv eqn:E_sv.
+ simpl in H_valid_sv.
simpl in H_valid_sb.
simpl in H_follow.
injection H_follow as H_smv H_maxidx' H_sb'.
rewrite <- H_sb'.
rewrite <- H_smv.
rewrite <- H_maxidx'.
simpl.
split; try intuition.
+ simpl in H_valid_sv.
simpl in H_valid_sb.
simpl in H_follow.
injection H_follow as H_smv H_maxidx' H_sb'.
rewrite <- H_sb'.
rewrite <- H_smv.
rewrite <- H_maxidx'.
simpl.
split; try intuition.
+ discriminate.
- intros sv maxidx ops smv maxidx' sb' H_valid_sv H_valid_sb H_follow.
destruct sv eqn:E_sv.
+ simpl in H_valid_sv.
simpl in H_valid_sb.
simpl in H_follow.
injection H_follow as H_smv H_maxidx' H_sb'.
rewrite <- H_sb'.
rewrite <- H_smv.
rewrite <- H_maxidx'.
simpl.
split; try intuition.
+ simpl in H_valid_sv.
simpl in H_valid_sb.
simpl in H_follow.
injection H_follow as H_smv H_maxidx' H_sb'.
rewrite <- H_sb'.
rewrite <- H_smv.
rewrite <- H_maxidx'.
simpl.
split; try intuition.
+ destruct p as [idx value] eqn:E_p.
simpl in H_valid_sv.
simpl in H_valid_sb.
simpl in H_follow.
destruct H_valid_sb as [H_valid_sb_0 [H_valid_sb_1 H_valid_sb_2]].
destruct (idx =? var) eqn:E_n_var.
* destruct (is_fresh_var_smv value) as [idx'|] eqn:E_is_fresh_var_value.
** destruct value eqn:E_value; try discriminate.
destruct val; try discriminate.
simpl in E_is_fresh_var_value.
injection E_is_fresh_var_value as E_is_fresh_var_value.
simpl in H_valid_sb_1.
rewrite E_is_fresh_var_value in H_valid_sb_1.
assert(H_valid_sstack_value_FreshVar_idx': valid_sstack_value idx (FreshVar idx')). intuition.
pose proof (IHsb'' (FreshVar idx') idx ops smv maxidx' sb' H_valid_sstack_value_FreshVar_idx' H_valid_sb_2 H_follow) as IHsb''_0.
intuition.
** injection H_follow as H_value H_idx H_sb''.
rewrite <- H_idx.
rewrite <- H_sb''.
rewrite <- H_value.
split.
*** apply H_valid_sb_1.
*** split.
***** apply H_valid_sb_2.
***** intro H_not_basic_value.
destruct value; try intuition.
* apply Nat.eqb_neq in E_n_var.
assert(H_valid_sstack_value_FreshVar_idx': valid_sstack_value idx (FreshVar var)). simpl. intuition.
pose proof (IHsb'' (FreshVar var) idx ops smv maxidx' sb' H_valid_sstack_value_FreshVar_idx' H_valid_sb_2 H_follow) as IHsb''_0.
intuition.
Qed.
Lemma follow_in_smap_suc:
forall sb sv maxidx ops,
valid_sstack_value maxidx sv ->
valid_bindings maxidx sb ops ->
exists smv maxidx' sb',
follow_in_smap sv maxidx sb = Some (FollowSmapVal smv maxidx' sb') /\
is_fresh_var_smv smv = None.
Proof.
induction sb as [| p sb' IHsb'].
- intros sv maxidx ops H_valid_sv H_valid_bs.
destruct sv eqn:E_sv.
+ simpl. exists (SymBasicVal (Val val)). exists maxidx. exists [].
split; try reflexivity.
+ simpl. exists (SymBasicVal (InVar var)). exists maxidx. exists [].
split; try reflexivity.
+ simpl in H_valid_bs.
simpl in H_valid_sv.
intuition.
- intros sv maxidx ops H_valid_sv H_valid_bs.
destruct sv eqn:E_sv.
+ simpl. exists (SymBasicVal (Val val)). exists maxidx. exists (p :: sb'). split; try reflexivity.
+ simpl. exists (SymBasicVal (InVar var)). exists maxidx. exists (p :: sb'). split; try reflexivity.
+ destruct p as [key value].
simpl in H_valid_bs.
destruct H_valid_bs as [H_valid_bs_0 [H_valid_bs_1 H_valid_bs_2]].
simpl in H_valid_sv.
simpl.
destruct (key =? var) eqn:E_key_var.
* destruct (is_fresh_var_smv value) as [idx'|] eqn:E_is_fresh_var_smv_value.
** apply IHsb' with (ops:=ops).
*** simpl.
destruct value; try discriminate.
simpl in E_is_fresh_var_smv_value.
destruct val; try discriminate.
injection E_is_fresh_var_smv_value as E_is_fresh_var_smv_value.
simpl in H_valid_bs_1.
intuition.
*** apply H_valid_bs_2.
** exists value. exists key. exists sb'.
split; try reflexivity.
apply E_is_fresh_var_smv_value.
* apply IHsb' with (ops:=ops).
** simpl.
apply Nat.eqb_neq in E_key_var. intuition.
** apply H_valid_bs_2.
Qed.
(* Elements (using nth_error) of a valid sstack are also valid *)
Lemma valid_sstack_nth:
forall maxidx sstk sv k,
valid_sstack maxidx sstk ->
nth_error sstk k = Some sv ->
valid_sstack_value maxidx sv.
Proof.
intros maxidx sstk sv.
revert sstk.
induction sstk as [|a sstk' IHsstk'].
- intros. destruct k; discriminate.
- intros k H_valid_sstk H_nth.
destruct k as [|k'].
+ simpl in H_nth.
injection H_nth as H_nth.
rewrite <- H_nth.
simpl in H_valid_sstk.
destruct H_valid_sstk as [H_valid_a _].
apply H_valid_a.
+ simpl in H_nth.
simpl in H_valid_sstk.
destruct H_valid_sstk as [_ H_valid_sstk'].
apply IHsstk' with (k:=k').
apply H_valid_sstk'.
apply H_nth.
Qed.
(* firstn of a valid sstack is valid *)
Lemma valid_sstack_firstn:
forall maxidx sstk k,
valid_sstack maxidx sstk ->
valid_sstack maxidx (firstn k sstk).
Proof.
intros maxidx.
induction sstk as [|a sstk' IHsstk'].
- intros; destruct k; reflexivity.
- intros k H_valid_sstk.
destruct k as [|k'].
+ reflexivity.
+ simpl in H_valid_sstk.
destruct H_valid_sstk as [H_valid_a H_valid_sstk'].
simpl.
split.
* apply H_valid_a.
* apply IHsstk'.
apply H_valid_sstk'.
Qed.
(* skipn of a valid sstack is valid *)
Lemma valid_sstack_skipn:
forall maxidx sstk k,
valid_sstack maxidx sstk ->
valid_sstack maxidx (skipn k sstk).
Proof.
intros maxidx.
induction sstk as [|a sstk' IHsstk'].
- intros; destruct k; reflexivity.
- intros k H_valid_sstk.
simpl in H_valid_sstk.
destruct H_valid_sstk as [H_valid_a H_valid_sstk'].
destruct k as [|k'].
+ simpl.
split.