-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDEX_Final.v
2331 lines (2134 loc) · 94.1 KB
/
DEX_Final.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 Export DEX_Framework.
Require Export DEX_ProofBigStepWithType.
Require Export DEX_ElemLemmas.
Require Export DEX_ElemLemmaIntra.
Require Export DEX_ElemLemmaReturn.
(* Require Export ElemLemmaCall1.
Require Export ElemLemmaSideEffect. *)
(* Require DEX_compat. *)
Require Export DEX_step.
Require Export DEX_typing_rules.
Import DEX_BigStepWithTypes DEX_BigStepAnnot.DEX_BigStepAnnot DEX_BigStep.DEX_BigStep DEX_Dom DEX_Prog.
Definition ValidMethod (p:DEX_Program) (m:DEX_Method) : Prop :=
exists c, DEX_PROG.defined_Class p c /\ DEX_CLASS.defined_Method c m.
Definition step (p:DEX_Program) (* subclass_test *) : DEX_Method -> DEX_PC (* -> option DEX_ClassName *) -> option DEX_PC -> Prop :=
fun m pc (* tau *) opc =>
ValidMethod p m /\ exists i, instructionAt m pc = Some i /\ DEX_step (*p subclass_test *) m pc i (* None *) opc.
Variable RT_domain_same : forall rt1 rt2 r, In r (VarMap.dom L.t rt1) -> In r (VarMap.dom L.t rt2).
Variable valid_regs_prop : forall m bm r rt, DEX_METHOD.body m = Some bm ->
~ In r (DEX_BYTECODEMETHOD.regs bm) -> VarMap.get L.t rt r = None.
Variable RT_domain_length_same : forall rt1 rt2, length (VarMap.dom L.t rt1) = length (VarMap.dom L.t rt2).
Section hyps.
Variable kobs: L.t.
Variable p : DEX_ExtendedProgram.
(* Variable subclass_test : ClassName -> ClassName -> bool.
Variable subclass_test_correct : forall c1 c2, if subclass_test c1 c2 then subclass_name p c1 c2 else ~ subclass_name p c1 c2. *)
Definition Reg := DEX_Reg.
Definition PC := DEX_PC.
Definition Method := DEX_Method.
Definition Kind := option DEX_ClassName.
Definition Sign : Set := DEX_sign.
Definition PM := ValidMethod.
Inductive P : SignedMethod Method Sign -> Prop :=
P_def : forall (m:DEX_Method) sgn,
ValidMethod p m ->
(DEX_METHOD.isStatic m = true -> sgn = DEX_static_signature p (DEX_METHOD.signature m)) ->
(DEX_METHOD.isStatic m = false -> exists k, sgn = DEX_virtual_signature p (DEX_METHOD.signature m) k) ->
P (SM _ _ m sgn).
Section for_all.
Variable test : DEX_METHOD.t -> Sign -> bool.
Definition for_all_P : bool :=
for_all_methods p
(fun m =>
if DEX_METHOD.isStatic m then test m (DEX_static_signature p (DEX_METHOD.signature m))
else for_all _ (fun k => test m (DEX_virtual_signature p (DEX_METHOD.signature m) k)) L.all).
Lemma for_all_P_true : for_all_P = true ->
forall m sgn, P (SM _ _ m sgn) -> test m sgn = true.
Proof.
unfold for_all_P; intros.
inversion_mine H0.
generalize (for_all_methods_true _ _ H _ H3).
caseeq (DEX_METHOD.isStatic m); intros.
rewrite <- H4 in H1; auto.
generalize (for_all_true _ _ _ H1); intros.
elim H5; auto.
intros k Hk.
rewrite Hk; apply H2.
apply L.all_in_all.
Qed.
End for_all.
Lemma PM_P : forall m, P m -> PM p (unSign _ _ m).
Proof.
intros.
inversion_clear H; auto.
Qed.
Notation step := (step p (* subclass_test *)).
Variable cdr : forall m, PM p m -> CDR (step m).
Definition istate : Type := DEX_IntraNormalState.
Definition rstate : Type := DEX_ReturnState.
Inductive exec : Method -> (*nat -> Kind ->*) istate -> istate + rstate -> Prop :=
| exec_intra : forall (m:Method) (* tau *) s1 s2,
DEX_BigStepAnnot.DEX_exec_intra p m s1 s2 ->
exec m (* tau *) s1 (inl _ s2)
| exec_return : forall (m:Method) (* tau *) s ret,
DEX_BigStepAnnot.DEX_exec_return p m s ret ->
exec m (* tau *) s (inr _ ret).
(* | exec_call : forall (m:Method) n tau s1 ret' (m':Method) s' r,
BigStepAnnot.exec_call (throwableBy p) p m tau s1 ret' m' s' r ->
evalsto m' n s' ret' ->
exec m (S n) tau s1 r *)
Inductive evalsto : Method -> (* nat -> *) istate -> rstate -> Prop :=
| evalsto_return : forall (m:Method) (* tau *) s r,
exec m (* tau *) s (inr _ r) ->
evalsto m (* 1 *) s r
| evalsto_intra : forall (m:Method) (*n n1 n2 tau *) s1 s2 r,
exec m (* tau *) s1 (inl _ s2) ->
evalsto m (* n *) s2 r ->
evalsto m (* (S (n)) *) s1 r.
Definition pc : istate -> PC := @fst _ _.
Definition registertypes : Type := TypeRegisters.
(* Definition pbij : Set := FFun.t Location. *)
Definition texec : forall m, PM p m -> Sign -> (PC -> L.t) ->
PC -> (* Kind -> *) registertypes -> option registertypes -> Prop :=
fun m H sgn se pc (* tau *) rt ort =>
exists i, texec (*p subclass_test m*) sgn (region (cdr m H)) se pc i (* None *) rt ort
/\ instructionAt m pc = Some i.
(* Definition compat : Sign -> istate -> registertypes -> Prop :=
DEX_compat.compat_state.
Definition compat_res : Sign -> rstate -> Prop :=
DEX_compat.compat_res. *)
Inductive indist : Sign -> registertypes ->
registertypes -> (* pbij -> pbij ->*) istate -> istate -> Prop :=
indist_def :forall sgn rt1 rt2 (* b1 b2 *) r1 r2 pc1 pc2 (* h1 h2 l1 l2*),
st_in kobs (* (newArT p) (ft p) sgn.(lvt) b1 b2 *) rt1 rt2 (pc1,r1) (pc2,r2) ->
indist sgn rt1 rt2 (pc1,r1) (pc2,r2).
(* Inductive irindist : Sign -> stacktype -> pbij -> pbij -> istate -> rstate -> Prop :=
| irindist_def : forall sgn b1 b2 s1 st1 v2 h2,
indist_intra_return kobs p sgn s1 st1 b1 h2 v2 b2 ->
irindist sgn st1 b1 b2 s1 (h2,v2). *)
Inductive rindist : Sign -> (* pbij -> pbij ->*) rstate -> rstate -> Prop :=
| rindist_def : forall sgn (* b1 b2 h1 h2 *) r1 r2,
(* hp_in kobs (newArT p) (ft p) b1 b2 h1 h2 -> *)
indist_return_value kobs sgn (* h1 h2 *) r1 r2 (* b1 b2 *) ->
rindist sgn (* b1 b2 *) (* (h1, *) r1 (* ) (h2, *) r2(* ) *).
(* Lemma lookup_findMethod : forall p c msig cm,
lookup p c msig cm ->
findMethod p (fst cm,msig) = Some (snd cm).
Proof.
induction 1; auto.
inversion_mine H; auto.
Qed.
Lemma findMethod_P : forall m mid,
findMethod p mid = Some m -> ValidMethod p m.
Proof.
destruct mid as [cn mid]; simpl.
caseeq (PROG.class p.(prog) cn).
intros cl T1 T2.
exists cl.
unfold PROG.defined_Class.
rewrite <- (PROG.name_class_invariant1 _ _ _ T1); auto.
unfold CLASS.defined_Method.
rewrite <- (CLASS.method_signature_prop _ _ _ T2); auto.
intros; discriminate.
Qed.
Lemma P_CallStep : forall se (m:P.Method) sgn i s1 st1 m2 os l2 sgn2 st' ok k b1' br b3,
BigStepWithTypes.CallStep kobs p se m sgn i s1 st1 (m2, (os, l2)) sgn2 st' ok k b1' br b3 ->
P (SM _ _ m sgn) -> P (SM _ _ m2 sgn2).
Proof.
intros.
inversion_mine H; inversion_mine H0.
constructor.
eapply findMethod_P; eauto.
rewrite (findMethod_signature _ _ _ H4); auto.
intros; DiscrimateEq.
generalize (lookup_findMethod _ _ _ _ H4); intros.
constructor.
eapply findMethod_P; eauto.
intros; DiscrimateEq.
intros; exists k.
rewrite (lookup_signature _ _ _ _ H4); auto.
Qed.
Lemma P_exec_call : forall se region m sgn i s1 st1 r br b1' m2 sgn2 s0 st0 b1 s2 b3 tau,
BigStepWithTypes.exec_call kobs p se region m sgn i s1 st1 b1 r br m2 sgn2 s0 st0 b1' s2 b3 tau ->
P (SM _ _ m sgn) -> P (SM _ _ m2 sgn2).
Proof.
intros.
inversion_mine H; eapply P_CallStep; eauto.
Qed. *)
Definition default_level := L.High.
Inductive init_pc (m:Method) : PC -> Prop :=
init_pc_def : forall bm,
DEX_METHOD.body m = Some bm ->
init_pc m (DEX_BYTECODEMETHOD.firstAddress bm).
(* Lemma init_pc_exec_call : forall se region m sgn i s1 st1 r br b1' m2 sgn2 s0 st0 b1 s2 b3 tau,
BigStepWithTypes.exec_call kobs p se region m sgn i s1 st1 b1 r br m2 sgn2 s0 st0 b1' s2 b3 tau ->
init_pc m2 (pc s0).
Proof.
intros.
inversion_mine H; simpl; constructor; auto.
Qed. *)
(* Inductive high_opstack : stacktype -> istate -> Prop :=
high_opstack_def : forall pc s l h st,
high_st kobs s st ->
high_opstack st (pc,(h,s,l)). *)
(* Definition s0 : stacktype := nil. *)
(* Inductive rt0 (m:Method) (sgn:Sign): registertypes -> Prop :=
rt0_def : forall bm,
DEX_METHOD.body m = Some bm ->
P (SM _ _ m sgn) ->
rt0 m sgn (Annotated.make_rt_from_lvt_rec (sgn) (DEX_BYTECODEMETHOD.locR bm) (DEX_BYTECODEMETHOD.regs bm) (default_level)). *)
Definition rt0 (m:Method) (sgn:Sign): registertypes :=
match DEX_METHOD.body m with
| Some bm => (Annotated.make_rt_from_lvt_rec (sgn) (DEX_BYTECODEMETHOD.locR bm) (DEX_BYTECODEMETHOD.regs bm) (default_level))
| None => VarMap.empty L.t
end.
(* Definition rt0 (m:Method) : registertypes :=
Annotated.make_rt_from_lvt_rec (sgn) (DEX_BYTECODEMETHOD.locR bm) (DEX_BYTECODEMETHOD.regs bm) (default_level). *)
Definition ni := ni _ _ _ _ _ exec pc registertypes indist rindist (* compat *) rt0 init_pc P.
Open Scope nat_scope.
(* Definition side_effect (sgn:Sign) (is:istate) (os:istate+rstate) : Prop :=
match is with
(pc,(h,s,l)) =>
match os with
| inl (pc',(h',s',l')) => side_effect (newArT p) (ft p) sgn.(heapEffect) h h'
| inr (h',_) => side_effect (newArT p) (ft p) sgn.(heapEffect) h h'
end
end.
Definition ses : nat -> Prop :=
ses _ _ _ _ _ _ exec pc _ compat s0 init_pc side_effect P. *)
Lemma evalsto_Tevalsto : forall m s r,
evalsto m s r ->
exists p, DEX_Framework.evalsto Method istate rstate exec m p s r.
Proof.
(* intros m n; pattern n; apply lt_wf_ind; clear n; intros. *)
intros.
induction H.
exists 1; constructor 1; auto.
inversion IHevalsto.
exists (S x). constructor 2 with (s2:=s2); auto.
Qed.
Lemma evalsto_Tevalsto2 : forall m s r p,
DEX_Framework.evalsto Method istate rstate exec m p s r ->
evalsto m s r.
Proof.
(* intros m n; pattern n; apply lt_wf_ind; clear n; intros. *)
intros.
induction H.
constructor 1; auto.
constructor 2 with (s2:=s2); auto.
Qed.
Lemma tcc0 : forall m s s',
PM p m -> exec m s (inl rstate s') -> step m (pc s) (Some (pc s')).
Proof.
intros m s s' HP H.
split.
auto.
inversion_clear H.
inversion_clear H0.
inversion_clear H;
match goal with
| [ id : instructionAt _ _ = Some ?i |- _] =>
exists i; simpl; split; [assumption|idtac]; constructor;
simpl; auto
end.
Qed.
Lemma tcc1 : forall m s s',
PM p m -> exec m s (inr istate s') -> step m (pc s) None.
Proof.
intros m s s' HM H.
split; auto.
inversion_clear H.
inversion_clear H0.
inversion_clear H.
exists DEX_Return; simpl; split; auto; constructor.
exists (DEX_VReturn k rs); simpl; split; auto; constructor.
Qed.
(* Lemma side_effect_trans : forall (m : Sign) (s1 s2 : istate) (s3 : istate + rstate),
side_effect m s1 (inl rstate s2) ->
side_effect m s2 s3 -> side_effect m s1 s3.
Proof.
unfold side_effect; intros sgn [pc1 [[h1 s1] l1]] [pc2 [[h2 s2] l2]].
destruct s3 as [[pc3 [[h3 s3] l3]]|[h3 v3]].
apply side_effect_trans.
apply side_effect_trans.
Qed. *)
(* Lemma tcc6 : forall sgn m se s s' rt rt',
((* forall k : nat, (k < n)%nat -> *)
cmp _ _ _ _ _ exec pc registertypes compat compat_res rt0 init_pc P) ->
forall H0:P (SM Method Sign m sgn),
exec m s (inl rstate s') ->
texec m (PM_P _ H0) sgn se (pc s) rt (Some rt') ->
compat sgn s rt ->
compat sgn s' rt'.
Proof.
intros.
destruct H2 as [i [H2 Hi]].
inversion_mine H1.
(* eelim well_types_imply_exec_intra with (1:=H7) (2:=Hi) (3:=H2); eauto. *)
assert (DEX_BigStepWithTypes.NormalStep se (region (cdr m (PM_P {| unSign := m; sign := sgn |} H0)))
m sgn i s rt s' rt').
elim well_types_imply_exec_intra with (1:=H7) (2:=Hi) (3:=H2); eauto.
eapply DEX_compat.compat_intra; eauto.
econstructor; eauto.
Qed. *)
(* Lemma tcc7 : forall sgn m se s r rt,
((* forall k : nat,
(k < n)%nat -> *)
cmp _ _ _ _ _ exec pc registertypes compat compat_res rt0 init_pc P) ->
forall H0:P (SM Method Sign m sgn),
exec m s (inr istate r) ->
texec m (PM_P _ H0) sgn se (pc s) rt None ->
compat sgn s rt -> compat_res sgn r.
Proof.
intros.
destruct H2 as [i [H2 Hi]].
inversion_mine H1.
destruct r.
assert (DEX_BigStepWithTypes.ReturnStep p se m sgn i s rt (Normal o)).
elim well_types_imply_exec_return with (1:=H7) (2:=Hi) (3:=H2); eauto.
eapply DEX_compat.compat_return; eauto. econstructor; eauto.
Qed. *)
(* Inductive sub : stacktype -> stacktype -> Prop :=
| sub_nil : sub nil nil
| sub_cons : forall x1 x2 st1 st2,
L.leql' x1 x2 -> sub st1 st2 -> sub (x1::st1) (x2::st2). *)
Inductive sub : registertypes -> registertypes -> Prop :=
| forall_sub : forall rt1 rt2, eq_set (VarMap.dom _ rt1) (VarMap.dom _ rt2) ->
(forall r k1 k2, Some k1 = VarMap.get _ rt1 r -> Some k2 = VarMap.get _ rt2 r -> L.leql k1 k2)
-> sub rt1 rt2
| nil_sub : sub (VarMap.empty _) (VarMap.empty _).
Lemma sub_forall : forall rt rt', sub rt rt' ->
(forall r k1 k2,
Some k1 = VarMap.get _ rt r /\ Some k2 = VarMap.get _ rt' r ->
L.leql k1 k2).
Proof. intros. inversion H0; auto.
inversion H; subst. apply H4 with (r:=r); auto.
rewrite VarMap.get_empty in H1. inversion H1.
Qed.
(* Lemma compat_register_sub : forall (rt1 rt2 : registertypes),
sub rt1 rt2 -> forall r,
DEX_compat.compat_registers r rt1 ->
DEX_compat.compat_registers r rt2.
Proof.
induction 1; simpl; intuition.
unfold DEX_compat.compat_registers in H0.
unfold DEX_compat.compat_registers.
intros. destruct v; constructor; auto.
Qed. *)
(* Lemma compat_sub : forall (sgn : Sign) (s : istate) (rt1 rt2 : registertypes),
sub rt1 rt2 -> compat sgn s rt1 -> compat sgn s rt2.
Proof.
intros.
destruct s.
apply compat_register_sub with (r:=t) in H; auto.
Qed. *)
Ltac assert_some_not_none rt rn H :=
assert (VarMap.get L.t rt rn <> None) by solve [
destruct (VarMap.get L.t rt rn) as [a | ];
try (intros Hf; inversion Hf);
try (inversion H)].
Ltac assert_not_none_some rt rn k t:=
assert (exists k, Some k = VarMap.get L.t rt rn) by solve [
destruct (VarMap.get L.t rt rn) as [t | ] eqn:Hget;
try (exists t; auto);
try (apply False_ind; auto)].
Lemma indist_morphism_proof : forall (y : Sign) (x y0 : registertypes),
eq_rt x y0 ->
forall x0 y1 : registertypes,
eq_rt x0 y1 -> forall y2 y3 : istate, indist y x x0 y2 y3 <-> indist y y0 y1 y2 y3.
Proof.
split; intros.
(* -> *)
inversion_mine H1.
constructor.
inversion_mine H2.
inversion_mine H3.
constructor; constructor; intros.
(* same domain *)
inversion H; inversion H0.
rewrite <- H3; rewrite <- H5; auto.
(* indistinguishable contents *)
assert (H':=H); assert (H0':=H0).
inversion_mine H; inversion_mine H0.
specialize H2 with rn.
inversion H2.
assert_some_not_none x rn H0.
assert_some_not_none x0 rn H6.
apply VarMap.get_some_in_dom in H9.
apply VarMap.get_some_in_dom in H10.
constructor 1 with (k:=k) (k':=k'); auto.
(* apply H2 with (rn:=rn) (v:=v) (v':=v') (k:=k) (k':=k'); auto. *)
(* rewrite H9; auto. *)
(* rewrite H; auto. *)
rewrite eq_rt_get with (rt1:=y0) (rt2:=x); auto. apply eq_rt_sym; auto.
rewrite <- H3; auto.
rewrite eq_rt_get with (rt1:=y1) (rt2:=x0); auto. apply eq_rt_sym; auto.
rewrite H in H10; auto.
constructor 2. auto.
(* <- *)
inversion_mine H1.
constructor.
inversion_mine H2.
inversion_mine H3.
constructor; constructor; intros.
(* same domain *)
inversion H; inversion H0.
rewrite H3; rewrite H5; auto.
(* indistinguishable contents *)
assert (H':=H); assert (H0':=H0).
inversion_mine H; inversion_mine H0.
specialize H2 with rn.
inversion H2.
assert_some_not_none y0 rn H0.
assert_some_not_none y1 rn H6.
apply VarMap.get_some_in_dom in H9.
apply VarMap.get_some_in_dom in H10.
constructor 1 with (k:=k) (k':=k'); auto.
(* apply H2 with (rn:=rn) (v:=v) (v':=v') (k:=k) (k':=k'); auto. *)
(* rewrite H9; auto. *)
(* rewrite H; auto. *)
rewrite eq_rt_get with (rt1:=x) (rt2:=y0); auto. rewrite H3; auto.
rewrite eq_rt_get with (rt1:=x0) (rt2:=y1); auto. rewrite H; auto.
constructor 2. auto.
Qed.
(* Lemma compat_morphism_proof : forall (y : Sign) (y0 : istate) (x y1 : registertypes),
eq_rt x y1 -> compat y y0 x <-> compat y y0 y1.
Proof.
split; intros.
(* -> *)
unfold compat in H0; unfold DEX_compat.compat_state in H0; unfold DEX_compat.compat_registers in H0.
unfold compat; unfold DEX_compat.compat_state; unfold DEX_compat.compat_registers.
destruct y0.
intros.
assert (VarMap.get L.t y1 x0 <> None). unfold not; intros. rewrite H3 in H2; inversion H2.
rewrite eq_rt_get with (rt2:=x) in H2.
apply H0 with (x0:=x0) (v:=v) (k:=k) (1:=H1) (2:=H2).
apply eq_rt_sym; auto.
apply VarMap.get_some_in_dom in H3; auto.
apply VarMap.get_some_in_dom in H3.
inversion H. rewrite H4; auto.
(* <- *)
unfold compat in H0; unfold DEX_compat.compat_state in H0; unfold DEX_compat.compat_registers in H0.
unfold compat; unfold DEX_compat.compat_state; unfold DEX_compat.compat_registers.
destruct y0.
intros.
assert (VarMap.get L.t x x0 <> None). unfold not; intros. rewrite H3 in H2; inversion H2.
rewrite eq_rt_get with (rt2:=y1) in H2; auto.
apply H0 with (x:=x0) (v:=v) (k:=k) (1:=H1) (2:=H2).
apply VarMap.get_some_in_dom in H3; auto.
apply VarMap.get_some_in_dom in H3; auto.
inversion H. rewrite <- H4; auto.
Qed. *)
Definition TypableProg := TypableProg PC Method step (PM p) Sign (* istate pc *) registertypes
texec (*indist*) rt0 init_pc P PM_P sub eq_rt.
Section TypableProg.
Variable se : Method -> Sign -> PC -> L.t.
Variable RT : Method -> Sign -> PC -> registertypes.
Variable typable_hyp : TypableProg se RT.
(* TODO *)
Definition high_reg (rt:registertypes) (r:Reg) : Prop :=
match VarMap.get _ rt r with
| None => False
| Some k => ~L.leql k kobs
end.
Variable not_high_reg : forall rt r, ~high_reg rt r -> (exists k, VarMap.get L.t rt r = Some k /\ L.leql k kobs).
Definition indist_reg_val (s1 s2: istate) (r: Reg) : Prop :=
let rho1 := snd s1 in
let rho2 := snd s2 in
match DEX_Registers.get rho1 r, DEX_Registers.get rho2 r with
| Some v1, Some v2 => v1 = v2
| None, None => True
| _, _ => False
end.
Lemma indist_reg_val_trans : forall s1 s2 s3 r,
indist_reg_val s1 s2 r -> indist_reg_val s2 s3 r -> indist_reg_val s1 s3 r.
Proof.
intros.
unfold indist_reg_val in *.
destruct (DEX_Registers.get (snd s1) r);
destruct (DEX_Registers.get (snd s2) r);
destruct (DEX_Registers.get (snd s3) r); auto.
rewrite H; auto. inversion H.
Qed.
Lemma indist_reg_val_sym : forall s1 s2 r,
indist_reg_val s1 s2 r -> indist_reg_val s2 s1 r.
Proof.
unfold indist_reg_val in *.
intros.
destruct (DEX_Registers.get (snd s1) r);
destruct (DEX_Registers.get (snd s2) r); auto.
Qed.
Definition indist_reg := DEX_Framework.indist_reg Reg istate registertypes high_reg indist_reg_val.
(* Inductive indist_reg : registertypes -> registertypes -> istate -> istate -> Reg -> Prop :=
| high_indist_reg : forall rt1 rt2 s1 s2 r,
high_reg rt1 r -> high_reg rt2 r -> indist_reg rt1 rt2 s1 s2 r
| low_indist_reg : forall rt1 rt2 s1 s2 r, indist_reg_val s1 s2 r -> indist_reg rt1 rt2 s1 s2 r. *)
Lemma indist_from_reg : forall sgn rt1 rt2 s1 s2,
(forall r, indist_reg rt1 rt2 s1 s2 r) -> indist sgn rt1 rt2 s1 s2.
Proof.
intros.
destruct s1; destruct s2.
constructor.
constructor.
constructor.
constructor.
apply RT_domain_length_same.
split; eapply RT_domain_same; eauto.
intros.
specialize H with rn.
inversion H. (* Cleanexand.
inversion H7. subst. *)
unfold high_reg in *.
destruct (VarMap.get L.t rt1 rn) eqn:Hget1; destruct (VarMap.get L.t rt2 rn) eqn:Hget2; try (contradiction).
constructor 1 with (k:=t1) (k':=t2); auto.
constructor 2. subst. unfold indist_reg_val in H0.
simpl in H0. destruct (DEX_Registers.get t rn); destruct (DEX_Registers.get t0 rn); subst; try contradiction.
destruct d2; repeat constructor.
constructor.
Qed.
Lemma indist_reg_from_indist : forall sgn rt1 rt2 s1 s2,
indist sgn rt1 rt2 s1 s2 ->
forall r,
(high_reg rt1 r -> high_reg rt2 r -> indist_reg rt1 rt2 s1 s2 r) /\
((~high_reg rt1 r /\ ~high_reg rt2 r) \/
(high_reg rt1 r /\ ~high_reg rt2 r) \/
(~high_reg rt1 r /\ high_reg rt2 r) ->
indist_reg_val s1 s2 r).
Proof.
intros sgn rt1 rt2 s1 s2 Hindist r.
inversion Hindist. inversion H. inversion H6. subst.
specialize H11 with (rn:=r).
inversion H11.
split; intros.
constructor; auto.
inversion H4. inversion H5.
unfold high_reg in H7, H8.
rewrite H0 in H7; rewrite H1 in H8. contradiction.
inversion H5. inversion H7.
unfold high_reg in H8, H9.
rewrite H0 in H8; rewrite H1 in H9. contradiction.
inversion H7.
unfold high_reg in H8, H9.
rewrite H0 in H8; rewrite H1 in H9. contradiction.
split; intros. constructor; auto.
unfold indist_reg_val. simpl.
destruct (DEX_Registers.get r1 r); destruct (DEX_Registers.get r2 r); subst; auto.
inversion H0. inversion H4. auto.
inversion H0. inversion H0.
Qed.
Definition high_result := high_result kobs.
Lemma tevalsto_high_result : forall m sgn (H:PM p m) se s RT res,
~L.leql (se m sgn (pc s)) kobs ->
exec m s (inr res) ->
texec m H sgn (se m sgn) (pc s) (RT m sgn (pc s)) None -> high_result sgn res.
Proof.
intros.
(* induction typable_hyp with m sgn H. *)
(* Cleanexand. *)
inversion_mine H2.
inversion_mine H1. Cleanexand.
inversion_mine H6. inversion_mine H3.
inversion_mine H1. constructor 1. auto.
simpl in H2. rewrite H2 in H5. inversion H5.
inversion_mine H1. simpl in H2. rewrite H2 in H5. inversion H5.
constructor 2 with (k:=kv); auto.
simpl in H0, H11.
apply leql_join_each in H11. Cleanexand.
apply not_leql_trans with (k1:=se0 m sgn pc0); auto.
Qed.
(* this is only applicable to exception instructions, so normal instructions
only need to be proved via contradiction *)
Lemma tevalsto_diff_high_result : forall m sgn se RT s s' s1' rt res res' (H:PM p m),
pc s = pc s' ->
exec m s (inr res) ->
texec m H sgn (se m sgn) (pc s) (RT m sgn (pc s)) None ->
exec m s' (inl s1') ->
texec m H sgn (se m sgn) (pc s') (RT m sgn (pc s')) (Some rt) ->
evalsto m s' res' ->
high_result sgn res /\ high_result sgn res'.
Proof.
intros.
inversion_mine H1; inversion_mine H2; inversion_mine H3; inversion_mine H4.
Cleanexand.
inversion_mine H1;
inversion_mine H2;
match goal with
| [ H0 : pc s = pc s', H : instructionAt m (pc s) = ?P, H' : instructionAt m (pc s') = ?Q |- _ ] =>
rewrite <- H0 in H'; rewrite H' in H; inversion H
end.
Qed.
Lemma tevalsto_diff_high_result' : forall m sgn s s' p0 res res' (H:PM p m),
pc s = pc s' -> 1 < p0 ->
DEX_Framework.tevalsto PC Method (PM p) Sign istate rstate exec (pc) (registertypes) texec
sub m H sgn (se m sgn) (RT m sgn) 1 s res ->
DEX_Framework.tevalsto PC Method (PM p) Sign istate rstate exec (pc) (registertypes) texec
sub m H sgn (se m sgn) (RT m sgn) p0 s' res' ->
high_result sgn res /\ high_result sgn res'.
Proof.
intros.
inversion_mine H3. omega.
inversion_mine H4.
apply tevalsto_diff_high_result with (m:=m) (se:=se) (RT:=RT) (s:=s) (s':=s') (s1':=s2) (rt:=rt') (H:=H); auto.
inversion_mine H2; auto.
inversion H3; auto.
inversion H8.
inversion_mine H2; auto. inversion_mine H3; auto.
inversion H8.
apply DEX_Framework.tevalsto_evalsto in H5; auto.
apply evalsto_Tevalsto2 with (p:=S n).
constructor 2 with (s2:=s2); auto.
Qed.
Lemma high_result_indist : forall sgn res res0,
(* DEX_resType sgn = Some k -> *)
high_result sgn res -> high_result sgn res0 -> rindist sgn res res0.
Proof.
intros.
constructor.
destruct sgn. destruct DEX_resType eqn:Hres.
destruct res. destruct res0.
destruct o. destruct o0.
constructor 1 with (k:=t); auto.
intros. inversion H0. simpl in H3. inversion H3. subst. contradiction.
inversion H0. simpl in H1. inversion H1.
destruct o0.
inversion H. simpl in H1. inversion H1.
inversion H0. simpl in H1. inversion H1.
inversion H. inversion H0. subst. constructor 2; auto.
simpl in H3. inversion H3.
simpl in H1; inversion H1.
Qed.
Lemma high_reg_dec : forall rt r, high_reg rt r \/ ~high_reg rt r.
Proof.
intros.
apply excluded_middle with (P:=high_reg rt r).
Qed.
(* Lemma high_reg_dec : forall rt r, In r (VarMap.dom _ rt) -> high_reg rt r \/ ~high_reg rt r.
Proof.
intros.
unfold high_reg.
apply VarMap.in_dom_get_some in H.
assert (exists k, VarMap.get L.t rt r = Some k).
unfold not in H.
destruct (VarMap.get L.t rt r); auto.
exists t; auto.
apply False_ind. auto.
destruct H0.
rewrite H0.
generalize (L.leql_dec x kobs); intros.
inversion H1; auto.
Qed. *)
Definition path := DEX_Framework.path Method istate rstate exec.
(* Inductive path (m:Method) (i:istate) : istate -> Type :=
| path_base : forall j, exec m i (inl j) -> path m i j
| path_step : forall j k, path m k j -> exec m i (inl k) -> path m i j. *)
(* Inductive path (m:Method) (sgn:Sign) (H:PM _ m) (i:istate) : istate -> Type :=
| path_base : forall j ort, texec m H sgn (se m sgn) (pc i) (RT m sgn (pc i)) ort ->
exec m i (inl j) -> path m sgn H i j
| path_step : forall j k ort, path m sgn H k j -> exec m i (inl k) ->
texec m H sgn (se m sgn) (pc i) (RT m sgn (pc i)) ort -> path m sgn H i j. *)
Definition path_in_region := DEX_Framework.path_in_region PC Method step istate rstate exec pc.
(* Inductive path_in_region (m:Method) (cdr: CDR (step m)) (s:PC) (i j:istate) : (path m i j) -> Prop :=
| path_in_reg_base : forall (Hexec:exec m i (inl j)), region cdr s (pc i) ->
path_in_region m cdr s i j (path_base m i j Hexec)
| path_in_reg_ind : forall k (Hexec:exec m i (inl k)) (p:path m k j), region cdr s (pc i) ->
path_in_region m cdr s k j p -> path_in_region m cdr s i j (path_step m i j k p Hexec). *)
Inductive path_prop (m:Method) (i j:istate) : Prop := path_exists : path m i j -> path_prop m i j.
(* Inductive path_prop (m:Method) (sgn:Sign) (H:PM _ m) (i j:istate) : Prop :=
path_exists : path m sgn H i j -> path_prop m sgn H i j. *)
Inductive changed_at (m:Method) (i:istate) (r:Reg) : Prop :=
| const_change : forall k v, instructionAt m (pc i) = Some (DEX_Const k r v) -> changed_at m i r
| move_change : forall k rs, instructionAt m (pc i) = Some (DEX_Move k r rs) -> changed_at m i r
| ineg_change : forall rs, instructionAt m (pc i) = Some (DEX_Ineg r rs) -> changed_at m i r
| inot_change : forall rs, instructionAt m (pc i) = Some (DEX_Inot r rs) -> changed_at m i r
| i2b_change : forall rs, instructionAt m (pc i) = Some (DEX_I2b r rs) -> changed_at m i r
| i2s_change : forall rs, instructionAt m (pc i) = Some (DEX_I2s r rs) -> changed_at m i r
| ibinop_change : forall op ra rb, instructionAt m (pc i) = Some (DEX_Ibinop op r ra rb) -> changed_at m i r
| ibinopConst_change : forall op rs v, instructionAt m (pc i) = Some (DEX_IbinopConst op r rs v) -> changed_at m i r.
Definition changed_at_t (m:Method) (i:istate) (r:Reg) : bool :=
match instructionAt m (pc i) with
| Some (DEX_Const k r' v) => Reg_eq r r'
| Some (DEX_Move _ r' _) => Reg_eq r r'
| Some (DEX_Ineg r' _) => Reg_eq r r'
| Some (DEX_Inot r' _) => Reg_eq r r'
| Some (DEX_I2b r' _) => Reg_eq r r'
| Some (DEX_I2s r' _) => Reg_eq r r'
| Some (DEX_Ibinop _ r' _ _) => Reg_eq r r'
| Some (DEX_IbinopConst _ r' _ _) => Reg_eq r r'
| _ => false
end.
Ltac inconsistent_ins :=
match goal with | [H:instructionAt ?m ?i = Some ?P, H':instructionAt ?m ?i = Some ?Q |- _] =>
rewrite H' in H; inversion H end.
Ltac not_changed_auto := unfold not; intros HnotChangedAuto; inversion HnotChangedAuto; inconsistent_ins.
Lemma changed_at_spec : forall m i r, if changed_at_t m i r then changed_at m i r else ~changed_at m i r.
Proof.
intros.
unfold changed_at_t.
destruct (instructionAt m (pc i)) eqn:Hins.
unfold Reg_eq.
destruct d; try (not_changed_auto; fail);
try (destruct (Neq r rt) eqn:Heq; generalize (Neq_spec r rt); rewrite Heq; intros);
try (constructor; subst; auto);
try (not_changed_auto; contradiction).
constructor 2 with (k:=k) (rs:=rs); subst; auto.
constructor 1 with (k:=k) (v:=v); subst; auto.
constructor 3 with (rs:=rs); subst; auto.
constructor 4 with (rs:=rs); subst; auto.
constructor 5 with (rs:=rs); subst; auto.
constructor 6 with (rs:=rs); subst; auto.
constructor 7 with (ra:=ra) (rb:=rb) (op:=op); subst; auto.
constructor 8 with (rs:=r0) (v:=v) (op:=op); subst; auto.
(* the case where the instructionAt is none *)
unfold not; intros H; inversion H;
match goal with
| [H:instructionAt m (pc i) = None, H':instructionAt m (pc i) = Some _ |- _] => rewrite H' in H; inversion H
end.
Qed.
Inductive changed (m:Method) (i j: istate) : (path m i j) -> Reg -> Prop :=
| changed_onestep : forall r (p:path m i j), changed_at m i r -> changed m i j p r
| changed_path : forall k r (p:path m k j) (H:exec m i (inl k)),
changed m k j p r -> changed m i j (path_step Method istate rstate exec m i j k p H) r.
(* Inductive changed (m:Method) (sgn:Sign) (H:PM _ m) (i j: istate) : (path m sgn H i j) -> Reg -> Prop :=
| changed_onestep : forall r (p:path m sgn H i j), changed_at m i r -> changed m sgn H i j p r
| changed_path : forall k r ort (p:path m sgn H k j) (Hexec:exec m i (inl k))
(Htexec:texec m H sgn (se m sgn) (pc i) (RT m sgn (pc i)) ort),
changed m sgn H k j p r -> changed m sgn H i j (path_step m sgn H i j k ort p Hexec Htexec) r.
*)
(* Inductive changed : Set -> Reg -> Prop :=
| changed_onestep : forall m i j r, changed_at m i r -> changed (path m i j) r
(* | changed_onestep : forall k, step m i (Some k) -> path m k j -> changed_at m i r -> changed m i j r *)
| changed_path : forall m i j k r, step m i (Some k) -> (* path m k j -> *)
changed (path m k j) r -> changed (path m i j) r. *)
Lemma changed_dec : forall m (* sgn (H:PM _ m) *) i j r (*p:path m sgn H i j*) (p:path m i j), (* path_prop m i j -> *)
(* changed (path m i j) r \/ ~changed (path m i j) r. *)
changed m (* sgn H *) i j (p) r \/ ~changed m (* sgn H *) i j (p) r.
Proof.
intros.
apply excluded_middle with (P:=changed m i j p0 r).
Qed.
Lemma changed_high_onestep : forall m sgn s i j r (H: P (SM _ _ m sgn)),
(forall k:PC, region (cdr m (PM_P _ H)) s (* kd *) k -> ~ L.leql (se m sgn k) kobs) ->
region (cdr m (PM_P _ H)) s (pc i) ->
exec m i (inl j) ->
(* In r (VarMap.dom _ (RT m sgn (pc j))) -> *)
changed_at m i r -> high_reg (RT m sgn (pc j)) r.
Proof.
intros m sgn s i j r H Hhighreg Hreg Hexec Hchanged_at.
assert (Hexec':=Hexec).
apply tcc0 with (1:=PM_P _ H) in Hexec'.
destruct (typable_hyp m sgn H) as [T1 [T2 T3]].
specialize T3 with (i:=pc i) (j:=pc j) (1:=Hexec').
destruct T3 as [rt [Htexec Hsub]].
specialize Hhighreg with (pc i). apply Hhighreg in Hreg.
inversion Htexec as [x [Htexec' Hins]].
inversion_mine Hchanged_at;
try (rewrite H0 in Hins; injection Hins; intros; subst;
inversion_mine Htexec';
unfold high_reg;
generalize sub_forall; intros Hsub_forall;
specialize Hsub_forall with (1:=Hsub) (r:=r);
destruct (VarMap.get _ (RT m sgn (pc j)) r) eqn:Hval);
try ( match goal with
| [ H:In r ?dom |- False] => apply RT_domain_same with (rt2:=RT m sgn (pc j)) in H;
apply VarMap.in_dom_get_some in H; contradiction
end).
(* Const *)
assert (exists k, VarMap.get L.t (VarMap.update L.t (RT m sgn (pc i)) r (se m sgn (pc i))) r = Some k) as Hget.
exists (se m sgn (pc i)). rewrite VarMap.get_update1; auto.
destruct Hget as [lvl Hget]. specialize Hsub_forall with (k1:=lvl) (k2:=t). rewrite Hget in Hsub_forall.
assert (L.leql lvl t) as Hleql; auto.
rewrite VarMap.get_update1 in Hget. inversion_mine Hget.
apply not_leql_trans with (k1:=(se m sgn (pc i))); auto.
(* Move *)
assert (exists k, VarMap.get L.t (VarMap.update L.t (RT m sgn (pc i)) r (L.join (se m sgn (pc i)) k_rs)) r = Some k) as Hget.
exists ((L.join (se m sgn (pc i)) k_rs)). rewrite VarMap.get_update1; auto.
destruct Hget as [lvl Hget]. specialize Hsub_forall with (k1:=lvl) (k2:=t). rewrite Hget in Hsub_forall.
assert (L.leql lvl t) as Hleql; auto.
rewrite VarMap.get_update1 in Hget. inversion_mine Hget.
apply not_leql_trans with (k1:=(se m sgn (pc i))); auto.
apply leql_join_each in Hleql; destruct Hleql; auto.
(* Ineg *)
assert (exists k, VarMap.get L.t (VarMap.update L.t (RT m sgn (pc i)) r (L.join (se m sgn (pc i)) ks)) r = Some k) as Hget.
exists (L.join (se m sgn (pc i)) ks). rewrite VarMap.get_update1; auto.
destruct Hget as [lvl Hget]. specialize Hsub_forall with (k1:=lvl) (k2:=t). rewrite Hget in Hsub_forall.
assert (L.leql lvl t) as Hleql; auto.
rewrite VarMap.get_update1 in Hget. inversion_mine Hget.
apply not_leql_trans with (k1:=se m sgn (pc i)); auto.
apply leql_join_each in Hleql. Cleanexand; auto.
(* Inot *)
assert (exists k, VarMap.get L.t (VarMap.update L.t (RT m sgn (pc i)) r (L.join (se m sgn (pc i)) ks)) r = Some k) as Hget.
exists (L.join (se m sgn (pc i)) ks). rewrite VarMap.get_update1; auto.
destruct Hget as [lvl Hget]. specialize Hsub_forall with (k1:=lvl) (k2:=t). rewrite Hget in Hsub_forall.
assert (L.leql lvl t) as Hleql; auto.
rewrite VarMap.get_update1 in Hget. inversion_mine Hget.
apply not_leql_trans with (k1:=se m sgn (pc i)); auto.
apply leql_join_each in Hleql. Cleanexand; auto.
(* I2b *)
assert (exists k, VarMap.get L.t (VarMap.update L.t (RT m sgn (pc i)) r (L.join (se m sgn (pc i)) ks)) r = Some k) as Hget.
exists (L.join (se m sgn (pc i)) ks). rewrite VarMap.get_update1; auto.
destruct Hget as [lvl Hget]. specialize Hsub_forall with (k1:=lvl) (k2:=t). rewrite Hget in Hsub_forall.
assert (L.leql lvl t) as Hleql; auto.
rewrite VarMap.get_update1 in Hget. inversion_mine Hget.
apply not_leql_trans with (k1:=se m sgn (pc i)); auto.
apply leql_join_each in Hleql. Cleanexand; auto.
(* I2s *)
assert (exists k, VarMap.get L.t (VarMap.update L.t (RT m sgn (pc i)) r (L.join (se m sgn (pc i)) ks)) r = Some k) as Hget.
exists (L.join (se m sgn (pc i)) ks). rewrite VarMap.get_update1; auto.
destruct Hget as [lvl Hget]. specialize Hsub_forall with (k1:=lvl) (k2:=t). rewrite Hget in Hsub_forall.
assert (L.leql lvl t) as Hleql; auto.
rewrite VarMap.get_update1 in Hget. inversion_mine Hget.
apply not_leql_trans with (k1:=se m sgn (pc i)); auto.
apply leql_join_each in Hleql. Cleanexand; auto.
(* Ibinop *)
assert (exists k, VarMap.get L.t (VarMap.update L.t (RT m sgn (pc i)) r (L.join (L.join ka kb) (se m sgn (pc i)))) r = Some k) as Hget.
exists (L.join (L.join ka kb) (se m sgn (pc i))). rewrite VarMap.get_update1; auto.
destruct Hget as [lvl Hget]. specialize Hsub_forall with (k1:=lvl) (k2:=t). rewrite Hget in Hsub_forall.
assert (L.leql lvl t) as Hleql; auto.
rewrite VarMap.get_update1 in Hget. inversion_mine Hget.
apply not_leql_trans with (k1:=se m sgn (pc i)); auto.
apply leql_join_each in Hleql. Cleanexand; auto.
(* IbinopConst *)
assert (exists k, VarMap.get L.t (VarMap.update L.t (RT m sgn (pc i)) r (L.join ks (se m sgn (pc i)))) r = Some k) as Hget.
exists (L.join ks (se m sgn (pc i))). rewrite VarMap.get_update1; auto.
destruct Hget as [lvl Hget]. specialize Hsub_forall with (k1:=lvl) (k2:=t). rewrite Hget in Hsub_forall.
assert (L.leql lvl t) as Hleql; auto.
rewrite VarMap.get_update1 in Hget. inversion_mine Hget.
apply not_leql_trans with (k1:=se m sgn (pc i)); auto.
apply leql_join_each in Hleql. Cleanexand; auto.
Defined.
Ltac clear_other_ins ins :=
match goal with
| [H:instructionAt ?m ?pc0 = Some ?ins, Hins:instructionAt ?m ?pc = Some ins |- _] =>
try (simpl in Hins; rewrite H in Hins; inversion Hins)
end.
Ltac not_changed_same_onestep_aux1 m sgn HPM Hexec pc0 pc' H r:=
simpl; subst;
destruct (typable_hyp m sgn HPM) as [T1 [T2 T3]];
assert (Hexec':=Hexec); apply tcc0 with (1:=PM_P _ HPM) in Hexec';
specialize T3 with (i:=pc0) (j:=pc') (1:=Hexec');
destruct T3 as [rt' [Htexec Hsub]];
inversion Htexec as [ins [Htexec' Hins']];
rewrite H in Hins'; inversion Hins'; subst; inversion Htexec'; subst;
unfold high_reg; intros;
destruct (VarMap.get L.t (RT m sgn pc0) r) eqn:Hrt0.
Lemma not_changed_same_onestep : forall m sgn i j r (HPM: P (SM _ _ m sgn)),
~changed_at m i r ->
exec m i (inl j) ->
(indist_reg_val i j r) /\ (high_reg (RT m sgn (pc i)) r -> high_reg (RT m sgn (pc j)) r).
Proof.
intros m sgn i j r HPM Hnchanged_at Hexec.
generalize (changed_at_spec m i r); intros Hchanged_at_dec.
destruct (changed_at_t m i r) eqn:Hchanged_at.
contradiction.
unfold changed_at_t in Hchanged_at.
destruct (instructionAt m (pc i)) eqn:Hins.
destruct d eqn:Hins'.
(* const *)
inversion Hexec. inversion_mine H2. inversion_mine H3; clear_other_ins (DEX_Nop).
split.
unfold indist_reg_val. simpl. destruct (DEX_Registers.get regs r); auto.
(* the case where the registers is high *)
not_changed_same_onestep_aux1 m sgn HPM Hexec pc0 pc' H r.
destruct (VarMap.get L.t (RT m sgn pc') r) eqn:Hrt'.
apply sub_forall with (r:=r) (k1:=t) (k2:=t0) in Hsub; auto.
apply not_leql_trans with (k1:=t); auto.
assert (VarMap.get L.t (RT m sgn pc0) r <> None) as Hget.
destruct (VarMap.get L.t (RT m sgn pc0) r). congruence.
inversion Hrt0. apply VarMap.get_some_in_dom in Hget.
try ( match goal with
| [ H:In r ?dom |- False] => apply RT_domain_same with (rt2:=RT m sgn pc') in H;
apply VarMap.in_dom_get_some in H; contradiction
end).
contradiction.
(* move *)
inversion Hexec. inversion_mine H2. inversion_mine H3; clear_other_ins (DEX_Move k rt rs).
split.
unfold indist_reg_val. simpl. rewrite DEX_Registers.get_update_old. destruct (DEX_Registers.get regs r); auto.
unfold Reg_eq in Hchanged_at; generalize (Neq_spec r rt); rewrite Hchanged_at; auto.
(* the case where the registers is high *)
not_changed_same_onestep_aux1 m sgn HPM Hexec pc0 pc' H r.
destruct (VarMap.get L.t (RT m sgn pc') r) eqn:Hrt'.
apply sub_forall with (r:=r) (k1:=t) (k2:=t0) in Hsub; auto.
apply not_leql_trans with (k1:=t); auto.
split; auto. rewrite VarMap.get_update2; auto.
unfold Reg_eq in Hchanged_at. generalize (Neq_spec r rt); rewrite Hchanged_at; auto.
assert (VarMap.get L.t (RT m sgn pc0) r <> None) as Hget.
destruct (VarMap.get L.t (RT m sgn pc0) r). congruence.
inversion Hrt0. apply VarMap.get_some_in_dom in Hget.
try ( match goal with
| [ H:In r ?dom |- False] => apply RT_domain_same with (rt2:=RT m sgn pc') in H;
apply VarMap.in_dom_get_some in H; contradiction
end).
contradiction.
(* Return *)
inversion Hexec. inversion H2. inversion_mine H3; clear_other_ins (DEX_Return).
(* VReturn *)
inversion Hexec. inversion H2. inversion_mine H3; clear_other_ins (DEX_VReturn k rt).
(* Const *)
inversion Hexec. inversion_mine H2. inversion_mine H3; clear_other_ins (DEX_Const k rt v).
split.
unfold indist_reg_val. simpl. rewrite DEX_Registers.get_update_old. destruct (DEX_Registers.get regs r); auto.
unfold Reg_eq in Hchanged_at; generalize (Neq_spec r rt); rewrite Hchanged_at; auto.
(* the case where the registers is high *)
not_changed_same_onestep_aux1 m sgn HPM Hexec pc0 pc' H r.
destruct (VarMap.get L.t (RT m sgn pc') r) eqn:Hrt'.
apply sub_forall with (r:=r) (k1:=t) (k2:=t0) in Hsub; auto.
apply not_leql_trans with (k1:=t); auto.
split; auto. rewrite VarMap.get_update2; auto.
unfold Reg_eq in Hchanged_at. generalize (Neq_spec r rt); rewrite Hchanged_at; auto.
assert (VarMap.get L.t (RT m sgn pc0) r <> None) as Hget.
destruct (VarMap.get L.t (RT m sgn pc0) r). congruence.
inversion Hrt0. apply VarMap.get_some_in_dom in Hget.
try ( match goal with
| [ H:In r ?dom |- False] => apply RT_domain_same with (rt2:=RT m sgn pc') in H;
apply VarMap.in_dom_get_some in H; contradiction
end).
contradiction.
(* goto *)
inversion Hexec. inversion_mine H2. inversion_mine H3; clear_other_ins (DEX_Goto o).
split.
unfold indist_reg_val. simpl. destruct (DEX_Registers.get regs r); auto.
(* the case where the registers is high *)
not_changed_same_onestep_aux1 m sgn HPM Hexec pc0 (DEX_OFFSET.jump pc0 o) H r.
destruct (VarMap.get L.t (RT m sgn (DEX_OFFSET.jump pc0 o)) r) eqn:Hrt'.
apply sub_forall with (r:=r) (k1:=t) (k2:=t0) in Hsub; auto.
apply not_leql_trans with (k1:=t); auto.
assert (VarMap.get L.t (RT m sgn pc0) r <> None) as Hget.
destruct (VarMap.get L.t (RT m sgn pc0) r). congruence.
inversion Hrt0. apply VarMap.get_some_in_dom in Hget.
try ( match goal with
| [ H:In r ?dom |- False] => apply RT_domain_same with (rt2:=RT m sgn (DEX_OFFSET.jump pc0 o)) in H;
apply VarMap.in_dom_get_some in H; contradiction
end).
contradiction.
(* Ifeq *)
inversion Hexec. inversion_mine H2. inversion_mine H3; clear_other_ins (DEX_Ifcmp cmp ra rb o).
(* the case where the successor is the target *)
split. unfold indist_reg_val. simpl. destruct (DEX_Registers.get regs r); auto.
(* the case where the registers is high *)
not_changed_same_onestep_aux1 m sgn HPM Hexec pc0 (DEX_OFFSET.jump pc0 o) H r.
destruct (VarMap.get L.t (RT m sgn (DEX_OFFSET.jump pc0 o)) r) eqn:Hrt'.