-
Notifications
You must be signed in to change notification settings - Fork 1
/
optimizations_common.v
1921 lines (1705 loc) · 63.1 KB
/
optimizations_common.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 bbv.Word.
Require Import Nat.
Require Import Coq.NArith.NArith.
Require Import Coq.Bool.Bool.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import FORVES.constants.
Import Constants.
Require Import FORVES.symbolic_state.
Import SymbolicState.
Require Import FORVES.symbolic_state_eval.
Import SymbolicStateEval.
Require Import FORVES.symbolic_state_cmp.
Import SymbolicStateCmp.
Require Import FORVES.valid_symbolic_state.
Import ValidSymbolicState.
Require Import FORVES.execution_state.
Import ExecutionState.
Require Import FORVES.stack_operation_instructions.
Import StackOpInstrs.
Require Import FORVES.program.
Import Program.
Require Import FORVES.symbolic_state_cmp_impl.
Import SymbolicStateCmpImpl.
Require Import FORVES.symbolic_state_eval_facts.
Import SymbolicStateEvalFacts.
Require Import FORVES.valid_symbolic_state.
Import ValidSymbolicState.
Require Import FORVES.misc.
Import Misc.
Require Import FORVES.eval_common.
Import EvalCommon.
Require Import FORVES.concrete_interpreter.
Import ConcreteInterpreter.
Require Import Coq.Program.Equality.
(* For dependent induction and dependent destruction *)
Require Import List.
Import ListNotations.
Module Optimizations_Common.
Definition follow_to_val (sv: sstack_val) (maxidx: nat) (sb: sbindings)
: option EVMWord :=
match follow_in_smap sv maxidx sb with
| Some (FollowSmapVal (SymBasicVal (Val v)) idx' sb') => Some v
| _ => None
end.
Definition follow_to_val_args (args: sstack) (maxidx: nat) (sb: sbindings)
: option (list EVMWord) :=
let f_follow_list := fun (sv': sstack_val) => follow_to_val sv' maxidx sb in
map_option f_follow_list args.
(**************************************
Auxiliary results about evaluation
used when proving optimizations
**************************************)
(*************************************************)
(* Results about bitvectors *)
(*************************************************)
Lemma zext_split1: forall [sz : nat] (w : word sz) (n : nat),
split1 sz n (zext w n) = w.
Proof.
intros. unfold zext.
rewrite -> split1_combine.
reflexivity.
Qed.
Lemma wxor_x_x: forall (size: nat) (x: word size), wxor x x = wzero size.
Proof.
dependent induction x.
- reflexivity.
- unfold wxor. unfold bitwp. simpl.
rewrite -> Bool.xorb_nilpotent.
fold bitwp. fold wxor.
rewrite -> IHx.
unfold wzero. unfold natToWord. simpl. fold natToWord.
reflexivity.
Qed.
Lemma wand_x_x: forall (x: EVMWord),
wand x x = x.
Proof.
induction x as [|b n x' IH].
- reflexivity.
- unfold wand. simpl. fold wand.
rewrite -> andb_diag.
rewrite -> IH.
reflexivity.
Qed.
Lemma wor_x_x: forall (x: EVMWord),
wor x x = x.
Proof.
induction x as [|b n x' IH].
- reflexivity.
- unfold wor. simpl. fold wor.
rewrite -> orb_diag.
rewrite -> IH.
reflexivity.
Qed.
Lemma wones_evm:
wones EVMWordSize =
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true
(WS true (WS true (WS true (WS true (WS true (WS true (WS true (WS true WO
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))).
Proof. reflexivity. Qed.
Definition two_exp_160_minus_1 : EVMWord :=
let diff := EVMWordSize - EVMAddrSize in
zext (wones EVMAddrSize) diff.
Lemma two_exp_160_minus_1_ok: wordToN two_exp_160_minus_1 = (Npow2 160 - 1)%N.
Proof.
reflexivity.
Qed.
Lemma two_exp_160_minus_1_ok':
two_exp_160_minus_1 = wminus (wordBin N.pow (natToWord EVMWordSize 2)
(natToWord EVMWordSize 160))
WOne.
Proof.
reflexivity.
Qed.
(* Distribution of wand over combine *)
Lemma wand_combine: forall (n1 n2: nat) (w1 w1': word n1)
(w2 w2': word n2),
wand
(Word.combine w1 w2)
(Word.combine w1' w2') =
Word.combine (wand w1 w1')
(wand w2 w2').
Proof.
dependent induction w1.
- intros. simpl.
dependent destruction w1'. simpl. reflexivity.
- intros. simpl.
dependent destruction w1'. simpl.
unfold wand. simpl.
fold wand.
rewrite -> IHw1.
reflexivity.
Qed.
(* Specialized version of wand_combine for the specific sizes *)
Lemma wand_combine_spec: forall w1 w2 w1' w2',
@wand EVMWordSize
(@Word.combine EVMAddrSize w1 (EVMWordSize - EVMAddrSize) w2)
(@Word.combine EVMAddrSize w1' (EVMWordSize - EVMAddrSize) w2') =
(@Word.combine EVMAddrSize (wand w1 w1')
(EVMWordSize - EVMAddrSize) (wand w2 w2')).
Proof.
intros w1 w2 w1' w2'.
rewrite <- wand_combine.
reflexivity.
Qed.
Lemma masking_address_extension_word: forall (w: word EVMAddrSize),
(zext w (EVMWordSize - EVMAddrSize)) =
(@wand EVMWordSize
(@zext EVMAddrSize w (EVMWordSize - EVMAddrSize))
(@zext EVMAddrSize (wones EVMAddrSize) (EVMWordSize - EVMAddrSize))).
Proof.
intros w. unfold zext.
rewrite -> wand_combine_spec.
rewrite wand_comm.
rewrite wand_wones.
rewrite wand_wzero.
reflexivity.
Qed.
Lemma pow2_shl: forall x,
wlshift WOne x = natToWord EVMWordSize (2 ^ x).
Proof.
induction x as [|x' IH].
- simpl. rewrite -> wlshift_0. reflexivity.
- rewrite -> wlshift_mul_pow2.
rewrite -> wmult_unit.
reflexivity.
Qed.
Lemma pow2_shl': forall x,
wlshift' WOne x = natToWord EVMWordSize (2 ^ x).
Proof.
intros x.
rewrite -> wlshift_alt.
apply pow2_shl.
Qed.
(*************************************************)
(* Miscellaneous results *)
(*************************************************)
Lemma evm_stack_opm_SELFBALANCE:
evm_stack_opm SELFBALANCE = OpImp 0 evm_selfbalance None None.
Proof.
reflexivity.
Qed.
Lemma evm_stack_opm_EQ:
evm_stack_opm EQ = OpImp 2 evm_eq (Some eq_comm) (Some eq_exts_ind).
Proof.
intuition.
Qed.
Lemma evm_stack_opm_GT:
evm_stack_opm GT = OpImp 2 evm_gt None (Some gt_exts_ind).
Proof.
intuition.
Qed.
Lemma evm_stack_opm_ISZERO:
evm_stack_opm ISZERO = OpImp 1 evm_iszero None (Some iszero_exts_ind).
Proof.
intuition.
Qed.
Lemma evm_stack_opm_LT:
evm_stack_opm LT = OpImp 2 evm_lt None (Some lt_exts_ind).
Proof.
intuition.
Qed.
Lemma length_zero: forall {X: Type}, length ([]: list X) =? 0 = true.
Proof.
intuition.
Qed.
Lemma length_one: forall {X: Type} (v: X), length [v] =? 1 = true.
Proof.
intuition.
Qed.
Lemma length_two: forall {T: Type} (x y: T), (length [x; y] =? 2) = true.
Proof.
intros T x y.
reflexivity.
Qed.
Lemma gt_iszero_nat: forall (x: nat),
x < 1 <-> x = 0.
Proof.
intros. intuition.
Qed.
Lemma one_as_N:
N.to_nat (1)%N = 1.
Proof. auto. Qed.
Lemma gt_iszero_nat': forall (x: nat),
x >= 1 <-> x <> 0.
Proof.
intros. intuition.
Qed.
Lemma word_neq_zero: forall (x: EVMWord),
N.to_nat (wordToN x) <> 0 -> x <> WZero.
Proof.
intros. destruct (weqb x WZero) eqn: eq_x_wzero.
- apply weqb_sound in eq_x_wzero. rewrite eq_x_wzero in H.
simpl in H. auto.
- apply weqb_false. assumption.
Qed.
Lemma is_fresh_var_smv_fvar: forall fvar,
is_fresh_var_smv (SymBasicVal (FreshVar fvar)) = Some fvar.
Proof.
intuition.
Qed.
Lemma map_option_empty: forall {A B : Type} (f : A -> option B),
map_option f [] = Some [].
Proof.
intuition.
Qed.
Lemma map_option_preserv_functs: forall {A B : Type} (f g: A -> option B) (l: list A)
(rl: list B),
map_option f l = Some rl ->
(forall x r, f x = Some r -> g x = Some r) ->
map_option g l = Some rl.
Proof.
intros A B f g l.
induction l as [|h t IH].
- intuition.
- intros rl Hmap_f Heq_f_g.
simpl. simpl in Hmap_f.
destruct (f h) as [eh|] eqn: eq_f_h; try discriminate.
apply Heq_f_g in eq_f_h.
rewrite -> eq_f_h.
destruct (map_option f t) as [et|] eqn: eq_map_t; try discriminate.
rewrite <- eq_map_t in IH.
pose proof (IH et eq_map_t Heq_f_g) as eq_map_g_t.
rewrite -> eq_map_g_t.
assumption.
Qed.
Lemma some_is_not_none: forall {T: Type} (x: option T) (v: T),
x = Some v -> x <> None.
Proof.
intros T x v Hx.
rewrite -> Hx.
intuition.
discriminate.
Qed.
(* Macro to reduce some proofs like optimize_add_0_sbinding_snd *)
Ltac inject_rw H eqname:=
injection H as eqname _;
rewrite <- eqname;
assumption.
Lemma gt_neq: forall n m, n > m -> n =? m = false.
Proof.
intros n m. revert n.
induction m as [|m' IH].
- intros n Hgt.
destruct n as [|n']; try intuition.
- intros n Hgt.
destruct n as [|n'].
+ intuition.
+ simpl. apply Gt.gt_S_n in Hgt.
intuition.
Qed.
Lemma is_fresh_var_some: forall v idx,
is_fresh_var_smv v = Some idx ->
v = SymBasicVal (FreshVar idx).
Proof.
intros v idx His_fresh.
destruct v; try (simpl in His_fresh; discriminate).
simpl in His_fresh.
destruct val as [v|var|fvar]; try discriminate.
injection His_fresh as eq_fvar.
rewrite -> eq_fvar.
reflexivity.
Qed.
Lemma leq_add: forall n m,
n <= m -> exists k, n+k=m.
Proof.
intros n m. revert n.
induction m as [|m' IH].
- intros n Hleq. exists 0. intuition.
- intros n Hleq.
destruct n as [|n'] eqn: eq_n.
+ exists (S m'). intuition.
+ apply Le.le_S_n in Hleq.
apply IH in Hleq as [k' eq_n'_k'].
exists k'. intuition.
Qed.
Lemma gt_add: forall n m,
n > m -> exists k, n=m+k.
Proof.
intros n m. revert n.
induction m as [|m' IH].
- intros m Hgt. exists m. intuition.
- intros n Hgt.
destruct n as [|n'] eqn: eq_n.
+ intuition.
+ apply Gt.gt_S_n in Hgt.
apply IH in Hgt as [k' eq_n'_k'].
exists k'. intuition.
Qed.
Lemma leq_diff_lt: forall n m,
n <= m -> n <> m -> n < m.
Proof.
intros n m Hleq Hdiff.
intuition.
Qed.
Lemma not_basic_value_smv_symop: forall label args,
not_basic_value_smv (SymOp label args) = true.
Proof.
reflexivity.
Qed.
(*************************************************)
(* Results about validity of values and bindings *)
(*************************************************)
Lemma valid_sstack_value_const: forall instk_height idx v,
valid_sstack_value instk_height idx (Val v).
Proof.
intros. simpl. intuition.
Qed.
Lemma Hvalid_maxidx: forall instk_height maxidx idx val sb ops,
valid_bindings instk_height maxidx ((idx, val) :: sb) ops ->
S idx = maxidx.
Proof.
intros instk_height maxidx idx val sb ops Hvalid.
unfold valid_bindings in Hvalid.
intuition.
Qed.
Lemma valid_sbindings_rec: forall instk_height maxidx n smapv sb ops,
valid_bindings instk_height maxidx ((n, smapv) :: sb) ops ->
valid_bindings instk_height n sb ops.
Proof.
intros instk_height maxidx n smapv sb ops Hvalid.
unfold valid_bindings in Hvalid.
destruct Hvalid as [_ [_ Hvalid']].
fold valid_bindings in Hvalid'.
assumption.
Qed.
Lemma valid_sstack_value_succ: forall instk_height n sv,
valid_sstack_value instk_height n sv ->
valid_sstack_value instk_height (S n) sv.
Proof.
intros instk_height n sv Hvalid.
unfold valid_sstack_value in Hvalid.
destruct sv as [v|var|fvar].
- intuition.
- intuition.
- simpl. intuition.
Qed.
Lemma valid_sstack_succ: forall instk_height n sstk,
valid_sstack instk_height n sstk ->
valid_sstack instk_height (S n) sstk.
Proof.
intros instk_height n sstk. revert instk_height n.
induction sstk as [| h r IH].
- intuition.
- intros instk_height n Hvalid.
unfold valid_sstack in Hvalid.
destruct Hvalid as [Hvalid_sstack_value Hvalid_sstack'].
fold valid_sstack in Hvalid_sstack'.
unfold valid_sstack.
split.
+ apply valid_sstack_value_succ. assumption.
+ fold valid_sstack. apply IH. assumption.
Qed.
Lemma valid_smemory_update_succ: forall instk_height n mem_upd,
valid_smemory_update instk_height n mem_upd ->
valid_smemory_update instk_height (S n) mem_upd.
Proof.
intros instk_height n mem_upd Hvalid.
destruct mem_upd eqn: eq_mem_upd.
- simpl in Hvalid.
destruct Hvalid as [Hvalid_offset Hvalid_value].
simpl. split.
+ apply valid_sstack_value_succ. assumption.
+ apply valid_sstack_value_succ. assumption.
- simpl in Hvalid.
destruct Hvalid as [Hvalid_offset Hvalid_value].
simpl. split.
+ apply valid_sstack_value_succ. assumption.
+ apply valid_sstack_value_succ. assumption.
Qed.
Lemma valid_smemory_succ: forall instk_height n smem,
valid_smemory instk_height n smem ->
valid_smemory instk_height (S n) smem.
Proof.
intros instk_height n smem. revert instk_height n.
induction smem as [|mem_upd rmem IH].
- intuition.
- intros instk_height n Hvalid.
unfold valid_smemory in Hvalid.
destruct Hvalid as [Hvalid_mem_upd Hvalid_smem_r].
fold valid_smemory in Hvalid_smem_r.
simpl. split.
+ apply valid_smemory_update_succ. assumption.
+ apply IH. assumption.
Qed.
Lemma valid_sstorage_succ: forall instk_height n sstr,
valid_sstorage instk_height n sstr ->
valid_sstorage instk_height (S n) sstr.
Proof.
intros instk_height n sstr. revert instk_height n.
induction sstr as [|sstr_upd rsstr IH].
- intuition.
- intros instk_height n Hvalid.
unfold valid_sstorage in Hvalid.
destruct Hvalid as [Hvalid_sstr_upd Hvalid_rsstr].
fold valid_sstorage in Hvalid_rsstr.
simpl. split.
+ destruct (sstr_upd) eqn: eq_sstr_upd.
unfold valid_sstorage_update in Hvalid_sstr_upd.
destruct Hvalid_sstr_upd as [Hvalid_key Hvalid_value].
simpl. split.
* apply valid_sstack_value_succ. assumption.
* apply valid_sstack_value_succ. assumption.
+ apply IH. assumption.
Qed.
Lemma valid_smap_value_succ: forall instk_height n ops smapv,
valid_smap_value instk_height n ops smapv ->
valid_smap_value instk_height (S n) ops smapv.
Proof.
intros instk_height n ops smapv Hvalid.
unfold valid_smap_value in Hvalid.
destruct smapv as [v|tag|label args|offset smem|key sstr|offset size mem]
eqn: eq_smapv.
- simpl. apply valid_sstack_value_succ. assumption.
- intuition.
- unfold valid_stack_op_instr in Hvalid.
destruct (ops label) as [nargs f Hcomm Hexts] eqn: eq_ops_label.
destruct Hvalid as [Hlen Hvalid2].
simpl. unfold valid_stack_op_instr. rewrite -> eq_ops_label.
split; try assumption.
apply valid_sstack_succ. assumption.
- destruct Hvalid as [Hvalid_offset Hvalid_smem].
unfold valid_smap_value.
split.
+ apply valid_sstack_value_succ. assumption.
+ apply valid_smemory_succ. assumption.
- destruct Hvalid as [Hvalid_key Hvalid_sstr].
simpl. split.
+ apply valid_sstack_value_succ. assumption.
+ apply valid_sstorage_succ. assumption.
- destruct Hvalid as [Hvalid_offset [Hvalid_size Hvalid_smem]].
simpl. split; try split.
+ apply valid_sstack_value_succ. assumption.
+ apply valid_sstack_value_succ. assumption.
+ apply valid_smemory_succ. assumption.
Qed.
Lemma valid_bindings_unique_n: forall n1 n2 sb ops instk_height,
valid_bindings instk_height n1 sb ops ->
valid_bindings instk_height n2 sb ops ->
n1 = n2.
Proof.
intros n1 n2 sb ops instk_height.
intros Hvalid_n1 Hvalid_n2.
destruct sb as [| h t].
- simpl in Hvalid_n1.
simpl in Hvalid_n2.
intuition.
- destruct h as [k v].
simpl in Hvalid_n1.
destruct Hvalid_n1 as [eq_n1 [_ Hvalid_k]].
destruct Hvalid_n2 as [eq_n2 [_ _]].
intuition.
Qed.
Lemma valid_bindings_decr_head: forall n1 k1 k2 v1 v2 instk_height t ops,
valid_bindings instk_height n1 ((k1, v1) :: ((k2, v2) :: t)) ops ->
k1 > k2.
Proof.
intros n1 k1 k2 v1 v2 instk_height t ops.
intros Hvalid.
simpl in Hvalid.
intuition.
Qed.
Lemma valid_bindings_gte: forall instk_height n1 sb ops prefix sb',
valid_bindings instk_height n1 sb ops ->
sb = prefix ++ sb' ->
exists n2, valid_bindings instk_height n2 sb' ops /\
forall k v, In (k,v) prefix -> k >= n2.
Proof.
intros instk_height n1 sb ops prefix.
revert instk_height n1 sb ops.
induction prefix as [|h t IH].
- intros instk_height n1 sb ops sb'.
intros Hvalid Hprefix.
simpl in Hprefix. rewrite <- Hprefix.
exists n1. split.
+ assumption.
+ intros k v Hin. intuition.
- intros instk_height n1 sb ops sb'.
intros Hvalid Hprefix.
simpl in Hprefix. rewrite -> Hprefix in Hvalid.
destruct h as [k1 v1] eqn: eq_h.
assert (Hvalid_copy := Hvalid).
simpl in Hvalid. destruct Hvalid as [eq_n1 [Hvalid_smap Hvalid_t_pref]].
assert (t ++ sb' = t ++ sb') as eq_t_sb'; try reflexivity.
pose proof (IH instk_height k1 (t ++ sb') ops sb' Hvalid_t_pref eq_t_sb')
as H.
destruct H as [n2 [Hvalid' Hin_impl]].
exists n2.
split; try assumption.
intros k v Hin.
simpl in Hin. destruct Hin.
+ injection H as eq_k eq_v.
rewrite <- eq_k.
destruct t as [|h2 t2] eqn: eq_t.
* simpl in Hvalid_t_pref.
simpl in Hvalid_copy.
destruct Hvalid_copy as [_ [_ Hvalid_t']].
pose proof (valid_bindings_unique_n k1 n2 sb' ops instk_height
Hvalid_t_pref Hvalid').
intuition.
* destruct h2 as [k2 v2] eqn: eq_h2.
rewrite <- app_comm_cons in Hvalid_copy.
pose proof (valid_bindings_decr_head n1 k1 k2 v1 v2 instk_height
(t2 ++ sb') ops Hvalid_copy) as k1_gt_k2.
assert (In (k2, v2) ((k2, v2) :: t2)) as Hin_k2; try intuition.
pose proof (Hin_impl k2 v2 Hin_k2) as H.
intuition.
+ apply Hin_impl with (v:=v); try assumption.
Qed.
Lemma valid_smap_value_incr: forall (m instk_height n : nat)
(ops : stack_op_instr_map) (smapv : smap_value),
valid_smap_value instk_height n ops smapv ->
valid_smap_value instk_height (n+m) ops smapv.
Proof.
induction m as [|m' IH].
- intuition. rewrite -> PeanoNat.Nat.add_0_r. assumption.
- intros instk_height n ops smap_value Hvalid_n.
rewrite -> PeanoNat.Nat.add_succ_r.
apply valid_smap_value_succ in Hvalid_n.
apply IH in Hvalid_n.
intuition.
Qed.
Lemma valid_sstack_value_extended_by_i: forall (i instk_height n : nat) (sv : sstack_val),
valid_sstack_value instk_height n sv ->
valid_sstack_value instk_height (n+i) sv.
Proof.
induction i as [|i' IH].
- intros instk_height n sv Hvalid.
rewrite -> PeanoNat.Nat.add_0_r.
assumption.
- intros instk_height n sv Hvalid.
rewrite -> PeanoNat.Nat.add_succ_r.
apply valid_sstack_value_succ.
apply IH.
assumption.
Qed.
Lemma valid_sstack_value_gt: forall (instk_height n m : nat) (sv : sstack_val),
valid_sstack_value instk_height n sv ->
m > n ->
valid_sstack_value instk_height m sv.
Proof.
intros instk_height n m sv.
intros Hvalid Hgt.
apply gt_add in Hgt.
destruct Hgt as [k eq_m_n_k].
rewrite -> eq_m_n_k.
apply valid_sstack_value_extended_by_i.
assumption.
Qed.
(*************************************************)
(* Results about follow_in_smap *)
(*************************************************)
Lemma follow_in_smap_head_op: forall idx maxidx label args sb,
follow_in_smap (FreshVar idx) maxidx ((idx, SymOp label args) :: sb) =
Some (FollowSmapVal (SymOp label args) idx sb).
Proof.
intros. simpl. rewrite -> PeanoNat.Nat.eqb_refl.
reflexivity.
Qed.
Lemma follow_in_smap_head: forall idx m sv sb,
follow_in_smap (FreshVar idx) m ((idx, SymBasicVal sv) :: sb) =
follow_in_smap sv idx sb.
Proof.
intros idx m sv sb.
unfold follow_in_smap at 1.
rewrite -> PeanoNat.Nat.eqb_refl.
fold follow_in_smap.
destruct sv as [val|var|fvar] eqn: eq_sv.
- simpl. destruct sb; try reflexivity.
- simpl. destruct sb; try reflexivity.
- simpl. reflexivity.
Qed.
Lemma follow_in_smap_fvar_maxidx_indep_eq: forall fvar n m sb,
follow_in_smap (FreshVar fvar) n sb =
follow_in_smap (FreshVar fvar) m sb.
Proof.
intros fvar n m sb.
destruct sb as [|h r].
- reflexivity.
- unfold follow_in_smap.
reflexivity.
Qed.
Lemma follow_in_smap_instackvar: forall var maxidx sb,
follow_in_smap (InStackVar var) maxidx sb =
Some (FollowSmapVal (SymBasicVal (InStackVar var)) maxidx sb).
Proof.
intros var maxidx sb.
destruct sb as [|h r]; try intuition.
Qed.
Lemma follow_in_smap_val: forall v maxidx sb,
follow_in_smap (Val v) maxidx sb =
Some (FollowSmapVal (SymBasicVal (Val v)) maxidx sb).
Proof.
intros v maxidx sb.
destruct sb as [|h r]; try intuition.
Qed.
Lemma follow_in_smap_chain: forall n1 n2 m sb,
follow_in_smap (FreshVar n1) m ((n1, SymBasicVal (FreshVar n2)) :: sb) =
follow_in_smap (FreshVar n2) n1 sb.
Proof.
intros n1 n2 m sb.
unfold follow_in_smap.
rewrite -> PeanoNat.Nat.eqb_refl. simpl. fold follow_in_smap.
reflexivity.
Qed.
Lemma follow_then_fvar_lt: forall maxidx sb ops instk_height n fvar fsm,
valid_bindings instk_height n sb ops ->
follow_in_smap (FreshVar fvar) maxidx sb = Some fsm ->
fvar < n.
Proof.
intros maxidx sb. revert maxidx.
induction sb as [| h t IH].
- intros maxidx ops instk_height n fvar fsm.
intros Hvalid Hfollow.
simpl in Hfollow. discriminate.
- intros maxidx ops instk_height n fvar fsm.
intros Hvalid Hfollow.
destruct h as [k v].
simpl in Hvalid.
destruct Hvalid as [eq_n [_ Hvalid']].
simpl in Hfollow.
destruct (k =? fvar) eqn: eq_k_fvar.
+ rewrite -> PeanoNat.Nat.eqb_eq in eq_k_fvar.
rewrite <- eq_k_fvar.
intuition.
+ rewrite -> follow_in_smap_fvar_maxidx_indep_eq with (m:=maxidx) in Hfollow.
pose proof (IH maxidx ops instk_height k fvar fsm Hvalid' Hfollow).
intuition.
Qed.
Lemma follow_in_smap_gt: forall fvar n1 n2 sb r instk_height ops,
follow_in_smap (FreshVar fvar) n1 sb = Some r ->
valid_bindings instk_height n2 sb ops ->
n2 > fvar.
Proof.
intros fvar n1 n2 sb. revert n1 n2.
induction sb as [| h t IH].
- intros n1 n2 r instk_height ops.
intros Hfollow Hvalid.
simpl in Hfollow. discriminate.
- intros n1 n2 r instk_height ops.
intros Hfollow Hvalid.
destruct h as [k v].
simpl in Hfollow.
simpl in Hvalid.
destruct Hvalid as [eq_n2 [_ Hvalid_t]].
destruct (k =? fvar) eqn: eq_k_fvar.
+ destruct (is_fresh_var_smv v) as [idx|].
* rewrite -> PeanoNat.Nat.eqb_eq in eq_k_fvar.
intuition.
* rewrite -> PeanoNat.Nat.eqb_eq in eq_k_fvar.
intuition.
+ pose proof (IH k k r instk_height ops Hfollow Hvalid_t).
intuition.
Qed.
Lemma follow_in_smap_prefix_gt: forall fvar n1 n2 sb' r instk_height sb
ops prefix,
follow_in_smap (FreshVar fvar) n1 sb' = Some r ->
valid_bindings instk_height n2 sb ops ->
sb = prefix ++ sb' ->
forall k v, In (k,v) prefix -> k > fvar.
Proof.
intros fvar n1 n2 sb' r instk_height sb ops prefix.
intros Hfollow Hvalid Hprefix.
intros k v Hin.
pose proof (valid_bindings_gte instk_height n2 sb ops prefix sb' Hvalid
Hprefix) as Hvalid_gte.
destruct Hvalid_gte as [nn [Hvalid_sb' Hk_in_prefix]].
pose proof (Hk_in_prefix k v Hin) as k_gte_nn.
pose proof (follow_in_smap_gt fvar n1 nn sb' r instk_height ops Hfollow
Hvalid_sb').
intuition.
Qed.
Lemma follow_in_smap_prefix_diff: forall fvar n1 n2 sb' r instk_height sb
ops prefix,
follow_in_smap (FreshVar fvar) n1 sb' = Some r ->
valid_bindings instk_height n2 sb ops ->
sb = prefix ++ sb' ->
forall k v, In (k,v) prefix -> k =? fvar = false.
Proof.
intros fvar n1 n2 sb' r instk_height sb ops prefix.
intros Hfollow Hvalid Hprefix.
intros k v Hin.
pose proof (follow_in_smap_prefix_gt fvar n1 n2 sb' r instk_height sb ops
prefix Hfollow Hvalid Hprefix k v Hin) as k_gte_n2.
apply gt_neq. assumption.
Qed.
Lemma follow_in_smap_prefix: forall fvar n1 n2 sb' r instk_height n3 sb ops
prefix,
follow_in_smap (FreshVar fvar) n1 sb' = Some r ->
valid_bindings instk_height n2 sb ops ->
sb = prefix ++ sb' ->
follow_in_smap (FreshVar fvar) n3 (prefix ++ sb') = Some r.
Proof.
intros fvar n1 n2 sb' r instk_height n3 sb ops prefix.
revert fvar n1 n2 sb' r instk_height n3 sb ops.
induction prefix as [| h t IH].
- intros fvar n1 n2 sb' r instk_height n3 sb ops.
intros Hfollow Hvalid Hprefix.
simpl.
rewrite -> follow_in_smap_fvar_maxidx_indep_eq with (m:=n1).
assumption.
- intros fvar n1 n2 sb' r instk_height n3 sb ops.
intros Hfollow Hvalid Hprefix.
destruct h as [k v] eqn: eq_h.
assert (In (k,v) ((k, v) :: t)) as Hin; try intuition.
pose proof (follow_in_smap_prefix_diff fvar n1 n2 sb' r instk_height sb
ops (((k, v) :: t)) Hfollow Hvalid Hprefix k v Hin) as Hk_fvar.
simpl. rewrite -> Hk_fvar.
rewrite Hprefix in Hvalid. simpl in Hvalid.
destruct Hvalid as [_ [_ Hvalid_t]].
assert (t ++ sb' = t ++ sb') as eq_t; try reflexivity.
pose proof (IH fvar n1 k sb' r instk_height k (t ++ sb') ops Hfollow
Hvalid_t eq_t).
assumption.
Qed.
Lemma follow_no_fresh: forall sb sv idx sv' idx' sb',
follow_in_smap sv idx sb = Some (FollowSmapVal sv' idx' sb') ->
is_fresh_var_smv sv' = None.
Proof.
induction sb as [| h t IH].
- intros sv idx sv' idx' sb' Hfollow. simpl in Hfollow.
destruct sv as [val|var|fvar].
+ injection Hfollow as eq_sv' _ _.
rewrite <- eq_sv'. reflexivity.
+ injection Hfollow as eq_sv' _ _.
rewrite <- eq_sv'. reflexivity.
+ discriminate.
- intros sv idx sv' idx' sb' Hfollow. simpl in Hfollow.
destruct sv as [val|var|fvar].
+ injection Hfollow as eq_sv' _ _.
rewrite <- eq_sv'. reflexivity.
+ injection Hfollow as eq_sv' _ _.
rewrite <- eq_sv'. reflexivity.
+ destruct h as [key smv] eqn: eq_h.
destruct (key =? fvar) eqn: eq_key_fvar.
* destruct (is_fresh_var_smv smv) as [idx2|] eqn: eq_is_fresh.
-- apply IH in Hfollow. assumption.
-- injection Hfollow as eq_sv' _ _.
rewrite <- eq_sv'. assumption.
* apply IH in Hfollow. assumption.
Qed.
Lemma follow_suffix: forall sb sv idx sv' idx' sb',
follow_in_smap sv idx sb = Some (FollowSmapVal sv' idx' sb') ->
exists prefix, sb = prefix ++ sb'.
Proof.
induction sb as [|h t IH].
- intros sv idx sv' idx' sb' Hfollow.
destruct sv as [val|var|fvar].
+ simpl in Hfollow.
injection Hfollow as eq_sv' eq_idx' eq_sb'.
rewrite <- eq_sb'.
exists []. reflexivity.
+ simpl in Hfollow.
injection Hfollow as eq_sv' eq_idx' eq_sb'.
rewrite <- eq_sb'.
exists []. reflexivity.
+ simpl in Hfollow. discriminate.
- intros sv idx sv' idx' sb' Hfollow.
destruct sv as [val|var|fvar].
+ simpl in Hfollow.
injection Hfollow as eq_sv' eq_idx' eq_sb'.
rewrite <- eq_sb'.
exists []. reflexivity.
+ simpl in Hfollow.
injection Hfollow as eq_sv' eq_idx' eq_sb'.
rewrite <- eq_sb'.
exists []. reflexivity.
+ simpl in Hfollow.
destruct h as [key value] eqn: eq_h.
destruct (key =? fvar) eqn: eq_key_fvar.
* destruct (is_fresh_var_smv value) as [idx''|] eqn: eq_is_fresh.
-- apply IH in Hfollow.
destruct Hfollow as [prefix' eq_t].
exists ((key, value)::prefix').
rewrite -> eq_t.
simpl.
reflexivity.
-- injection Hfollow as eq_sv' eq_idx' eq_sb'.
rewrite -> eq_sb'.
exists [(key, value)].
simpl.
reflexivity.
* apply IH in Hfollow as [prefix' eq_t].
exists ((key, value)::prefix').
rewrite -> eq_t.
reflexivity.
Qed.
(* Calling follow_in_smap with valid bindings and a valid smap_value