-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathIdSimMutrecBIdInv.v
179 lines (158 loc) · 5.34 KB
/
IdSimMutrecBIdInv.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
Require Import Program.
Require Import Sem SimProg Skeleton Mod ModSem SimMod SimModSem SimSymb SimMem Sound SimSymb.
Require Import Cop Ctypes ClightC.
Require Import AsmC.
Require SimMemInjInvC.
Require Import MutrecB MutrecBspec MutrecBproof.
Require Import CoqlibC.
Require Import ValuesC.
Require Import LinkingC.
Require Import MapsC.
Require Import AxiomsC.
Require Import Ord.
Require Import MemoryC.
Require Import SmallstepC.
Require Import Events.
Require Import Preservation.
Require Import Integers.
Require Import LocationsC Conventions.
Require Import Conventions1C.
Require Import AsmregsC.
Require Import MatchSimModSem.
Require Import StoreArguments.
Require Import AsmStepInj IntegersC.
Require Import Coq.Logic.PropExtensionality.
Require Import CtypingC.
Require Import CopC.
Require Import MatchSimModSem ModSemProps.
Require Import Conventions1C.
Require Import IdSimExtra IdSimInvExtra.
Require Import mktac.
Set Implicit Arguments.
Local Opaque Z.mul Z.add Z.sub Z.div.
Inductive match_states_b_internal:
state -> state -> meminj -> mem -> mem -> Prop :=
| match_Callstate
i m_src m_tgt j
:
match_states_b_internal
(Callstate i m_src)
(Callstate i m_tgt)
j m_src m_tgt
| match_Interstate
i m_src m_tgt j
:
match_states_b_internal
(Interstate i m_src)
(Interstate i m_tgt)
j m_src m_tgt
| match_Returnstate
i m_src m_tgt j
:
match_states_b_internal
(Returnstate i m_src)
(Returnstate i m_tgt)
j m_src m_tgt
.
Section INJINV.
Variable P: SimMemInjInv.memblk_invariant.
Local Instance SimMemP: SimMem.class := SimMemInjInvC.SimMemInjInv SimMemInjInv.top_inv P.
Local Instance SimSymbP: SimSymb.class SimMemP := SimMemInjInvC.SimSymbIdInv P.
Local Existing Instance SoundTop.Top.
Inductive match_states_b_inv
: unit -> state -> state -> SimMem.t -> Prop :=
| match_states_a_intro
st_src st_tgt j m_src m_tgt sm0
(MWFSRC: m_src = sm0.(SimMem.src))
(MWFTGT: m_tgt = sm0.(SimMem.tgt))
(MWFINJ: j = sm0.(SimMemInjInv.minj).(SimMemInj.inj))
(MATCHST: match_states_b_internal st_src st_tgt j m_src m_tgt)
(MWF: SimMem.wf sm0)
:
match_states_b_inv
tt st_src st_tgt sm0
.
Lemma b_inj_inv_id
(WF: Sk.wf (MutrecBspec.module))
:
exists mp,
(<<SIM: ModPair.sim mp>>)
/\ (<<SRC: mp.(ModPair.src) = (MutrecBspec.module)>>)
/\ (<<TGT: mp.(ModPair.tgt) = (MutrecBspec.module)>>)
.
Proof.
eexists (ModPair.mk _ _ _); s.
esplits; eauto. instantiate (1:=SimMemInjInvC.mk bot1 _ _).
econs; ss; i.
{ econs; ss; i; clarify. }
eapply match_states_sim with (match_states := match_states_b_inv); ss.
- apply unit_ord_wf.
- eapply SoundTop.sound_state_local_preservation.
- i. ss.
cinv SIMSKENV. ss.
exploit (@SimSymbIdInv_match_globals fundef _ _ sm_arg (MutrecBspec.module) (MutrecBspec.module) (SkEnv.project skenv_link_src (Sk.of_program fn_sig prog)) (SkEnv.project skenv_link_tgt (Sk.of_program fn_sig prog)) prog).
{ eauto. } intros GEMATCH.
inv INITTGT. inv SAFESRC. inv SIMARGS. inv H. ss.
inv GEMATCH. exploit SYMBLE; eauto. i. des.
clarify.
esplits; eauto.
+ econs; eauto.
+ refl.
+ econs; eauto.
assert (i = i0).
{ inv VALS. inv H2. auto. }
subst. econs; eauto.
+ ss.
- i. ss.
cinv SIMSKENV. ss.
exploit (@SimSymbIdInv_match_globals fundef _ _ sm_arg (MutrecBspec.module) (MutrecBspec.module) (SkEnv.project skenv_link_src (Sk.of_program fn_sig prog)) (SkEnv.project skenv_link_tgt (Sk.of_program fn_sig prog)) prog).
{ eauto. } intros GEMATCH.
des. inv SAFESRC. inv SIMARGS.
inv GEMATCH. exploit SYMBLE; eauto. i. des; eauto.
esplits. econs; ss; eauto.
+ clear -MWF INJ FPTR FPTR0.
rewrite FPTR in FPTR0. inv FPTR0; ss.
rewrite H1 in INJ. clarify.
+ rewrite VS in VALS. inv VALS; ss. inv H3. inv H1. auto.
+ ss.
- i. ss. inv MATCH; eauto.
- i. ss. clear SOUND. inv CALLSRC. inv MATCH. inv MATCHST. inversion SIMSKENV; subst. ss.
i. ss. cinv SIMSKENV. ss.
exploit (@SimSymbIdInv_match_globals fundef _ _ sm0 (MutrecBspec.module) (MutrecBspec.module) (SkEnv.project skenv_link_src (Sk.of_program fn_sig prog)) (SkEnv.project skenv_link_tgt (Sk.of_program fn_sig prog)) prog).
{ eauto. } intros GEMATCH.
inv GEMATCH. exploit SYMBLE; eauto. i. des; eauto.
esplits; eauto.
+ econs; ss; eauto.
+ econs; ss; econs; eauto.
+ refl.
+ instantiate (1:=top4). ss.
- i. ss. clear SOUND HISTORY.
exists (SimMemInjInvC.unlift' sm_arg sm_ret).
inv AFTERSRC. inv MATCH. inv MATCHST.
esplits; eauto.
+ econs; eauto. inv SIMRET; ss. rewrite INT in *. inv RETV. ss.
+ inv SIMRET; ss. econs; eauto. econs; eauto.
+ refl.
- i. ss. inv FINALSRC. inv MATCH. inv MATCHST.
esplits; eauto.
+ econs.
+ econs; eauto. econs.
+ refl.
- right. ii. des.
esplits.
+ i. inv MATCH. inv MATCHST.
* unfold ModSem.is_step. do 2 eexists. ss. econs; eauto.
* unfold safe_modsem in H.
exploit H. eapply star_refl. ii. des; clarify. inv EVSTEP.
* ss. exfalso. eapply NOTRET. econs. ss.
+ ii. inv STEPTGT; inv MATCH; inv MATCHST.
* esplits; eauto.
{ left. eapply plus_one. econs. }
refl.
econs; eauto. econs.
* esplits; eauto.
{ left. eapply plus_one. econs 2. eauto. }
refl.
econs; eauto. econs.
Qed.
End INJINV.