1 | |
---|
2 | include "Clight/label.ma". |
---|
3 | include "Clight/Cexec.ma". |
---|
4 | include "Clight/CexecInd.ma". |
---|
5 | |
---|
6 | (* Useful for breaking up the labeling functions, because we don't care about |
---|
7 | *which* cost labels are added here and so can throw away the resulting name |
---|
8 | generator. *) |
---|
9 | lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D. |
---|
10 | \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) = F (\fst e). |
---|
11 | #A #B #C #D * // |
---|
12 | qed. |
---|
13 | |
---|
14 | |
---|
15 | (* Similarly, lemma to break up label_expr, label_exprs and label_statement in |
---|
16 | the labelling functions *) |
---|
17 | lemma label_gen_elim : ∀Syn:Type[0].∀syn,u.∀T:Type[0].∀L:Syn → universe CostTag → Syn × (universe CostTag). ∀F:Syn → universe CostTag → T. ∀P:T → Type[0]. |
---|
18 | (∀u'. P (F (\fst (L syn u)) u')) → |
---|
19 | P (let 〈syn',u'〉 ≝ L syn u in F syn' u'). |
---|
20 | #Syn #syn #u #T #L #F #P |
---|
21 | cases (L syn u) |
---|
22 | #syn' #u' #H @H |
---|
23 | qed. |
---|
24 | |
---|
25 | lemma add_cost_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0]. |
---|
26 | (∀u',l. P (F (Expr (Ecost l e) (typeof e)) u')) → |
---|
27 | P (let 〈e',u'〉 ≝ add_cost_expr e u in F e' u'). |
---|
28 | #e #u #T #F #P #H whd in match (add_cost_expr ??); |
---|
29 | cases (fresh ??) #l #u' @H |
---|
30 | qed. |
---|
31 | |
---|
32 | |
---|
33 | lemma label_expr_type : ∀e,u. |
---|
34 | typeof (\fst (label_expr e u)) = typeof e. |
---|
35 | * #e #ty #u >shift_fst // |
---|
36 | qed. |
---|
37 | |
---|
38 | (* Formalise the notion of a trace with extra cost labels added. Note that |
---|
39 | we don't require the left trace to be cost free. *) |
---|
40 | inductive trace_with_extra_labels : trace → trace → Prop ≝ |
---|
41 | | twel_0 : trace_with_extra_labels E0 E0 |
---|
42 | | twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2) |
---|
43 | | twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2). |
---|
44 | |
---|
45 | lemma twel_refl : ∀tr. trace_with_extra_labels tr tr. |
---|
46 | #tr elim tr /2/ |
---|
47 | qed. |
---|
48 | |
---|
49 | lemma twel_app : ∀tr1,tr2,tr1',tr2'. |
---|
50 | trace_with_extra_labels tr1 tr1' → |
---|
51 | trace_with_extra_labels tr2 tr2' → |
---|
52 | trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2'). |
---|
53 | #tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/ |
---|
54 | qed. |
---|
55 | |
---|
56 | theorem label_expr_ok : ∀ge,ge',en,m. |
---|
57 | related_globals … label_fundef ge ge' → |
---|
58 | (∀e,v,tr. |
---|
59 | exec_expr ge en m e = OK … 〈v,tr〉 → |
---|
60 | ∀u. ∃tr'. exec_expr ge' en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧ |
---|
61 | trace_with_extra_labels tr tr') ∧ |
---|
62 | (∀e,ty,b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 → |
---|
63 | ∀u. ∃tr'. exec_lvalue' ge' en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧ |
---|
64 | trace_with_extra_labels tr tr'). |
---|
65 | (* Proof goes by breaking up the execution in the hypothesis, breaking up the |
---|
66 | labelling function to get a new term and executing it by rewriting what we |
---|
67 | learned from the hypothesis. *) |
---|
68 | #ge #ge' #en #m #RG @expr_lvalue_ind_combined |
---|
69 | [ 1,2: normalize /3 by ex_intro, conj/ |
---|
70 | | * // |
---|
71 | [ #id #ty #IH #v #tr #EX #u |
---|
72 | cases (bind_inversion ????? EX) -EX * * #b #o #tr1 * #EX1 #EX |
---|
73 | cases (bind_inversion ????? EX) -EX #v2 * #EX2 #EX |
---|
74 | normalize in EX; destruct |
---|
75 | cases (IH … EX1 u) #tr1' * #EX1' #T1 |
---|
76 | %{(tr1')} % [ whd in ⊢ (??%?); >EX1' whd in ⊢ (??%?); >EX2 @refl | // ] |
---|
77 | | #e1 #ty #IH #v #tr #EX #u |
---|
78 | cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r |
---|
79 | cases (bind_inversion ????? EX1r) #v * #EXl #EXrem |
---|
80 | normalize in EXrem; destruct |
---|
81 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
82 | %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (?(??%?)?); >EX1' |
---|
83 | whd in ⊢ (?(??%?)?); >EXl /2/ |
---|
84 | | #e1 #id #ty #IH #v #tr #EX #u |
---|
85 | cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r |
---|
86 | cases (bind_inversion ????? EX1r) #v * #EXl #EXrem |
---|
87 | normalize in EXrem; destruct |
---|
88 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
89 | %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' % // whd in ⊢ (??%?); >EX1' |
---|
90 | whd in ⊢ (??%?); >EXl @refl |
---|
91 | ] |
---|
92 | | #v #ty #b #o #tr #EX #u %{tr} % [ |
---|
93 | whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %; |
---|
94 | [ whd in ⊢ (??%? → ??%?); >(rg_find_symbol … RG) // |
---|
95 | | #b // ] |
---|
96 | | // ] |
---|
97 | | #e1 #ty #IH #b #o #tr #EX #u |
---|
98 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
99 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
100 | %{tr1'} >shift_fst whd in ⊢ (?(??%?)?); >EX1' |
---|
101 | whd in ⊢ (?(??%?)?); |
---|
102 | cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct /2/ |
---|
103 | | #ty' #e1 #ty #IH #v #tr #EX #u |
---|
104 | cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem |
---|
105 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
106 | %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (?(??%?)?); |
---|
107 | whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EX1' |
---|
108 | whd in ⊢ (?(??%?)?); |
---|
109 | cases ty' in EX1rem ⊢ %; |
---|
110 | [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r) |
---|
111 | #pc normalize #E destruct /2/ |
---|
112 | | *: normalize #A try #B try #C try #D destruct |
---|
113 | ] |
---|
114 | | #ty #op #e1 #IH #v #tr #EX #u |
---|
115 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
116 | cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem |
---|
117 | normalize in EXrem; destruct |
---|
118 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
119 | %{tr1'} % // >shift_fst |
---|
120 | whd in ⊢ (??(????(?(???%)?))?); |
---|
121 | @label_gen_elim #u2 |
---|
122 | whd in ⊢ (??%?); >EX1' |
---|
123 | whd in ⊢ (??%?); >label_expr_type >EX2 @refl |
---|
124 | | #ty #op #e1 #e2 #IH1 #IH2 #v #tr #EX |
---|
125 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
126 | cases (bind_inversion ????? EX1rem) * #v2 #tr2 * #EX2 #EX2rem |
---|
127 | cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop' |
---|
128 | #u |
---|
129 | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
130 | >shift_fst |
---|
131 | whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); |
---|
132 | @label_gen_elim #u2 |
---|
133 | cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2 |
---|
134 | @label_gen_elim #u3 %{(tr1'⧺tr2')} |
---|
135 | whd in ⊢ (?(??%?)?); >EX1' |
---|
136 | whd in ⊢ (?(??%?)?); >EX2' |
---|
137 | whd in ⊢ (?(??%?)?); >label_expr_type >label_expr_type >EXop |
---|
138 | normalize in EXop'; destruct % /2/ |
---|
139 | | #ty #ty' #e1 #IH #v #tr #EX #u |
---|
140 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
141 | cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem |
---|
142 | normalize in EX2rem; destruct |
---|
143 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
144 | %{tr1'} % // >shift_fst >shift_fst |
---|
145 | whd in ⊢ (??%?); >EX1' |
---|
146 | whd in ⊢ (??%?); >label_expr_type >EX2 @refl |
---|
147 | | #ty #e1 #e2 #e3 #IH1 #IH2 #IH3 #v #tr #EX #u |
---|
148 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
149 | cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem |
---|
150 | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem |
---|
151 | normalize in EX2rem; destruct |
---|
152 | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
153 | >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); |
---|
154 | @label_gen_elim #u2 |
---|
155 | @label_gen_elim #u3 |
---|
156 | @add_cost_expr_elim #u4 #l4 |
---|
157 | @label_gen_elim #u5 |
---|
158 | @add_cost_expr_elim #u6 #l6 |
---|
159 | [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx |
---|
160 | [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ] |
---|
161 | whd in ⊢ (?(??%?)?); >EX1' |
---|
162 | whd in ⊢ (?(??%?)?); >label_expr_type >EXguard |
---|
163 | whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EXx' |
---|
164 | normalize % // @twel_app // <(E0_right tr2) @twel_app /2/ |
---|
165 | | #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u |
---|
166 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
167 | cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem |
---|
168 | >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); |
---|
169 | @label_gen_elim #u2 |
---|
170 | @label_gen_elim #u3 |
---|
171 | @add_cost_expr_elim #u4 #l4 |
---|
172 | @add_cost_expr_elim #u5 #l5 |
---|
173 | [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem |
---|
174 | cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem |
---|
175 | -EX1rem -EXguardrem -EX2rem |
---|
176 | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
177 | cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2 |
---|
178 | %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)} |
---|
179 | whd in ⊢ (?(??%?)?); >EX1' |
---|
180 | whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard |
---|
181 | whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); |
---|
182 | whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2' |
---|
183 | whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3 |
---|
184 | whd in EX3rem:(??%%) ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ] |
---|
185 | | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
186 | %{(tr1'⧺E0⧺Echarge l5)} |
---|
187 | whd in ⊢ (?(??%?)?); >EX1' |
---|
188 | whd in ⊢ (?(??%?)?); >label_expr_type >EXguard |
---|
189 | whd in EXguardrem:(??%%); destruct % // <(E0_right tr) @twel_app /2/ |
---|
190 | ] |
---|
191 | | #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u |
---|
192 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
193 | cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem |
---|
194 | >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); |
---|
195 | @label_gen_elim #u2 |
---|
196 | @add_cost_expr_elim #u4 #l4 |
---|
197 | @label_gen_elim #u3 |
---|
198 | @add_cost_expr_elim #u5 #l5 |
---|
199 | [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
200 | %{(tr1'⧺Echarge l4)} |
---|
201 | whd in ⊢ (?(??%?)?); >EX1' |
---|
202 | whd in ⊢ (?(??%?)?); >label_expr_type >EXguard |
---|
203 | whd in EXguardrem:(??%%) ⊢ %; destruct % // <(E0_right tr) /3/ |
---|
204 | | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem |
---|
205 | cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem |
---|
206 | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
207 | cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2 |
---|
208 | %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)} |
---|
209 | whd in ⊢ (?(??%?)?); >EX1' |
---|
210 | whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard |
---|
211 | whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); |
---|
212 | whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2' |
---|
213 | whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3 |
---|
214 | whd in EX3rem:(??%%) ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/ |
---|
215 | ] |
---|
216 | | #ty #ty' #v #tr normalize /3/ |
---|
217 | | #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %; |
---|
218 | [ 7: #id #fl #IH #EX |
---|
219 | cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem |
---|
220 | cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem |
---|
221 | whd in EXoffrem:(???%); destruct >shift_fst >shift_fst |
---|
222 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
223 | %{tr1'} % // |
---|
224 | whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1' |
---|
225 | whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl |
---|
226 | | 8: #id #fl #IH #EX |
---|
227 | cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem |
---|
228 | whd in EX1rem:(???%); destruct >shift_fst >shift_fst |
---|
229 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
230 | %{tr1'} % // |
---|
231 | whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1' |
---|
232 | whd in ⊢ (??%?); @refl |
---|
233 | | *: normalize #A #B try #C try #D try #F destruct |
---|
234 | ] |
---|
235 | | #ty #l #e1 #IH #v #tr #EX #u |
---|
236 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
237 | whd in EX1rem:(???%); destruct |
---|
238 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)} |
---|
239 | >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1' |
---|
240 | whd in ⊢ (?(??%?)?); /3/ |
---|
241 | | #e1 #ty #NLV #b #o #tr #EX @⊥ |
---|
242 | cases e1 in NLV EX; normalize // |
---|
243 | #A #B #C try #D try #F destruct |
---|
244 | ] qed. |
---|
245 | |
---|
246 | lemma label_exprs_ok : ∀ge,ge'. |
---|
247 | related_globals … label_fundef ge ge' → |
---|
248 | ∀en,m,es,vs,tr. |
---|
249 | exec_exprlist ge en m es = OK … 〈vs,tr〉 → |
---|
250 | ∀u. ∃tr'. exec_exprlist ge' en m (\fst (label_exprs es u)) = OK … 〈vs,tr'〉 ∧ |
---|
251 | trace_with_extra_labels tr tr'. |
---|
252 | #ge #ge' #RG #en #m #es elim es |
---|
253 | [ #vs #tr #EX whd in EX:(??%?); destruct #u %{E0} /2/ |
---|
254 | | #e #tl #IH #vs #tr #EX |
---|
255 | cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
256 | cases (bind_inversion ????? EX) -EX * #tl' #tr' * #EX2 #EX |
---|
257 | whd in EX:(??%%); destruct |
---|
258 | #u whd in match (label_exprs ??); @label_gen_elim #u' >shift_fst |
---|
259 | cases (proj1 ?? (label_expr_ok ge ge' en m RG) ??? EX1 u) #tr1' * #EX1' #T1 |
---|
260 | cases (IH … EX2 u') #tr'' * #EX2' #T2 |
---|
261 | % [2: % [ whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
262 | whd in ⊢ (??%?); >EX2' in ⊢ (??%?); @refl |
---|
263 | | /2/ ] | skip ] |
---|
264 | ] qed. |
---|
265 | |
---|
266 | |
---|
267 | (* Now we move on to describe the simulation relation. First, relate the |
---|
268 | continuations. *) |
---|
269 | inductive cont_with_labels : cont → cont → Prop ≝ |
---|
270 | | cwl_stop : cont_with_labels Kstop Kstop |
---|
271 | | cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k') |
---|
272 | | cwl_while : ∀ue,e,us,s,cs,cpost,k,k'. |
---|
273 | cont_with_labels k k' → |
---|
274 | cont_with_labels (Kwhile e s k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k')) |
---|
275 | | cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'. |
---|
276 | cont_with_labels k k' → |
---|
277 | cont_with_labels (Kdowhile e s k) (Kdowhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k')) |
---|
278 | | cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. |
---|
279 | cont_with_labels k k' → |
---|
280 | cont_with_labels (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2)))) (Kseq (Scost cpost Sskip) k')) |
---|
281 | | cwl_for2 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor2 e s1 s2 k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k')) |
---|
282 | | cwl_for3 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor3 e s1 s2 k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k')) |
---|
283 | | cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k') |
---|
284 | | cwl_call : ∀r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (label_function f) en k') |
---|
285 | | cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' → |
---|
286 | cont_with_labels (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (\fst (label_lstatements ls u))) k'). |
---|
287 | |
---|
288 | lemma call_cont_with_labels : ∀k,k'. |
---|
289 | cont_with_labels k k' → |
---|
290 | cont_with_labels (call_cont k) (call_cont k'). |
---|
291 | #k0 #k0' #K elim K /2/ |
---|
292 | qed. |
---|
293 | |
---|
294 | (* Now define almost all of the simulation relation... *) |
---|
295 | inductive state_with_labels_partial : state → state → Prop ≝ |
---|
296 | | swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m) |
---|
297 | (* Extra matching states that we can reach that don't quite correspond to the |
---|
298 | labelling function *) |
---|
299 | | swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → |
---|
300 | state_with_labels_partial (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) |
---|
301 | | swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → |
---|
302 | state_with_labels_partial (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) |
---|
303 | | swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → |
---|
304 | state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) |
---|
305 | (* and the rest *) |
---|
306 | | swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (label_fundef fd) args k' m) |
---|
307 | | swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m) |
---|
308 | | swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r) |
---|
309 | . |
---|
310 | |
---|
311 | (* ... and add the states where the cases from switch statements are expanded. |
---|
312 | We do these separately because in the LSdefault case we have to execute a |
---|
313 | cost label alongside an arbitrary statement, and we want to reuse the result |
---|
314 | on arbitrary statements we get for state_with_labels_partial. *) |
---|
315 | inductive state_with_labels : state → state → Prop ≝ |
---|
316 | | swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s' |
---|
317 | | swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' → |
---|
318 | state_with_labels (State f (seq_of_labeled_statement ls) k e m) |
---|
319 | (State (label_function f) (seq_of_labeled_statement (\fst (label_lstatements ls u))) k' e m) |
---|
320 | . |
---|
321 | |
---|
322 | (* TODO: this (or something like it) ought to be elsewhere. *) |
---|
323 | inductive plus (ge:genv) : state → trace → state → Prop ≝ |
---|
324 | | plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2 |
---|
325 | | plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3. |
---|
326 | |
---|
327 | (* Some details are invariant under labelling. *) |
---|
328 | lemma label_function_return : ∀f. |
---|
329 | fn_return (label_function f) = fn_return f. |
---|
330 | * #rty #params #vars #body |
---|
331 | whd in ⊢ (??(?%)?); |
---|
332 | cases (label_statement ??) #body' #u' |
---|
333 | whd in ⊢ (??(?%)?); |
---|
334 | cases (add_cost_before ??) #body'' #u'' |
---|
335 | // |
---|
336 | qed. |
---|
337 | |
---|
338 | lemma label_expr_fun_typeof : ∀a,u. |
---|
339 | fun_typeof (\fst (label_expr a u)) = fun_typeof a. |
---|
340 | #a #u whd in ⊢ (??%?); >label_expr_type @refl |
---|
341 | qed. |
---|
342 | |
---|
343 | lemma label_fundef_typeof_fundef : ∀fd. |
---|
344 | type_of_fundef (label_fundef fd) = type_of_fundef fd. |
---|
345 | * // |
---|
346 | * #rty #args #vars #body |
---|
347 | normalize cases (label_statement ??) #body' #u |
---|
348 | normalize cases (fresh ??) // |
---|
349 | qed. |
---|
350 | |
---|
351 | lemma label_fn_params : ∀f. |
---|
352 | fn_params (label_function f) = fn_params f. |
---|
353 | * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // |
---|
354 | qed. |
---|
355 | |
---|
356 | lemma label_fn_vars : ∀f. |
---|
357 | fn_vars (label_function f) = fn_vars f. |
---|
358 | * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // |
---|
359 | qed. |
---|
360 | |
---|
361 | (* Some annoying rewrite rules *) |
---|
362 | lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u. |
---|
363 | exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) = |
---|
364 | exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty. |
---|
365 | #ge #e #m #a #ty #u |
---|
366 | whd in ⊢ (??(????(???%))?); >shift_fst @refl |
---|
367 | qed. |
---|
368 | |
---|
369 | lemma opt_find_funct : ∀ge,ge',m,vf,fd. |
---|
370 | related_globals … label_fundef ge ge' → |
---|
371 | opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd → |
---|
372 | opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd). |
---|
373 | #ge #ge' #m #vf #fd #RG |
---|
374 | lapply (rg_find_funct … RG … vf fd) |
---|
375 | cases (find_funct … vf) |
---|
376 | [ #_ #E normalize in E; destruct |
---|
377 | | #fd' #H #E normalize in E; destruct >(H (refl ??)) // |
---|
378 | ] qed. |
---|
379 | |
---|
380 | lemma labelled_not_skip : ∀s,u. |
---|
381 | s ≠ Sskip → |
---|
382 | (\fst (label_statement s u)) ≠ Sskip. |
---|
383 | * #u |
---|
384 | [ * #H cases (H (refl ??)) |
---|
385 | | *: #a try #b try #c try #d try #e |
---|
386 | (* Use the state-monad-like structure of the labelling function to break |
---|
387 | it up *) |
---|
388 | whd in match (label_statement ??); |
---|
389 | repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip)) |
---|
390 | % #E destruct |
---|
391 | ] qed. |
---|
392 | |
---|
393 | lemma labelled_is_not_skip : ∀s,u. |
---|
394 | s ≠ Sskip → |
---|
395 | ∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf. |
---|
396 | #s #u #NE |
---|
397 | cases (is_Sskip ?) |
---|
398 | [ #E @⊥ @(absurd ? E) @labelled_not_skip // |
---|
399 | | /2/ |
---|
400 | ] qed. |
---|
401 | |
---|
402 | lemma label_select_ls : ∀sz,i,ls,u. |
---|
403 | ∃u'. |
---|
404 | select_switch sz i (\fst (label_lstatements ls u)) = |
---|
405 | \fst (label_lstatements (select_switch sz i ls) u'). |
---|
406 | #sz #i #ls @(labeled_statements_ind … ls) |
---|
407 | [ #s #u % [2: whd in match (label_lstatements ??); |
---|
408 | @label_gen_elim #u1 >shift_fst @refl | skip ] |
---|
409 | | #sz' #i' #s #tl #IH #u |
---|
410 | whd in match (label_lstatements ??); |
---|
411 | whd in match (select_switch ?? (LScase ????)); |
---|
412 | @intsize_eq_elim_elim |
---|
413 | [ #NE |
---|
414 | @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3 |
---|
415 | cases (IH u2) |
---|
416 | #u4 #E %{u4} whd in ⊢ (??%?); |
---|
417 | >intsize_eq_elim_false // |
---|
418 | | #E <E in i' ⊢ %; #i' whd |
---|
419 | @eq_bv_elim |
---|
420 | [ #Ei >Ei |
---|
421 | %{u} |
---|
422 | whd in match (label_lstatements (if ? then ? else ?) ?); |
---|
423 | @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3 |
---|
424 | whd in ⊢ (??%?); |
---|
425 | >intsize_eq_elim_true |
---|
426 | >eq_bv_true |
---|
427 | @refl |
---|
428 | | #NEi |
---|
429 | @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3 |
---|
430 | whd in ⊢ (??(λ_.??%?)); |
---|
431 | >intsize_eq_elim_true |
---|
432 | >eq_bv_false // |
---|
433 | ] |
---|
434 | ] |
---|
435 | ] qed. |
---|
436 | |
---|
437 | (* Break up labelling function in one go for statements. *) |
---|
438 | lemma blindly_label : ∀u,s. ∀P:statement → Prop. |
---|
439 | match s with |
---|
440 | [ Sskip ⇒ P Sskip |
---|
441 | | Sassign e1 e2 ⇒ ∀u1,u2. P (Sassign (\fst (label_expr e1 u1)) (\fst (label_expr e2 u2))) |
---|
442 | | Scall eo e args ⇒ ∀u1,u2,u3. P (Scall (\fst (label_opt_expr eo u1)) (\fst (label_expr e u2)) (\fst (label_exprs args u3))) |
---|
443 | | Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2))) |
---|
444 | | Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3)))) |
---|
445 | | Swhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip)) |
---|
446 | | Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip)) |
---|
447 | | Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip)) |
---|
448 | | Sbreak ⇒ P Sbreak |
---|
449 | | Scontinue ⇒ P Scontinue |
---|
450 | | Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1))) |
---|
451 | | Sswitch e ls ⇒ ∀u1,u2. P (Sswitch (\fst (label_expr e u1)) (\fst (label_lstatements ls u2))) |
---|
452 | | Slabel l s1 ⇒ ∀u1,cs. P (Slabel l (Scost cs (\fst (label_statement s1 u1)))) |
---|
453 | | Sgoto l ⇒ P (Sgoto l) |
---|
454 | | Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1))) |
---|
455 | ] → P (\fst (label_statement s u)). |
---|
456 | #u * // #A #B #C try #D try #E try #F whd in match (label_statement ??); |
---|
457 | @label_gen_elim #u1 // |
---|
458 | @label_gen_elim #u2 // |
---|
459 | [ 6: >shift_fst // |
---|
460 | | *: @label_gen_elim #u3 // |
---|
461 | @label_gen_elim #u4 |
---|
462 | [ @label_gen_elim #u5 >shift_fst >shift_fst // |
---|
463 | | 2,3: >shift_fst >shift_fst // |
---|
464 | | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst // |
---|
465 | ] |
---|
466 | ] qed. |
---|
467 | |
---|
468 | (* Apply induction hypothesis in label_find_label proof below while getting |
---|
469 | Matita to infer the continuations k0 and k0', and the universe u0, rather |
---|
470 | than having to give them explicitly. *) |
---|
471 | lemma lfl_IH : ∀s0,lbl. |
---|
472 | ∀C:option (statement×cont) → option (statement×cont) → Prop. |
---|
473 | ∀IH:cont → cont → universe CostTag → Prop. |
---|
474 | (∀k,k',u. cont_with_labels k k' → IH k k' u) → |
---|
475 | ∀k0,k0',u0. cont_with_labels k0 k0' → |
---|
476 | (IH k0 k0' u0 → |
---|
477 | C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0')) → |
---|
478 | C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0'). |
---|
479 | /3/ |
---|
480 | qed. |
---|
481 | |
---|
482 | (* Finding a goto label in a cost-labelled program gives a labelled version of |
---|
483 | the statement and continuation found by the original function, if any. *) |
---|
484 | lemma label_find_label : ∀lbl,s,k,k',u. |
---|
485 | cont_with_labels k k' → |
---|
486 | match find_label lbl s k with |
---|
487 | [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in |
---|
488 | ∃u',cs,k1'. |
---|
489 | find_label lbl (\fst (label_statement s u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧ |
---|
490 | cont_with_labels k1 k1' |
---|
491 | | None ⇒ find_label lbl (\fst (label_statement s u)) k' = None ? |
---|
492 | ]. |
---|
493 | #lbl #s @(statement_ind2 ? (λls. |
---|
494 | ∀k,k',u. |
---|
495 | cont_with_labels k k' → |
---|
496 | match find_label_ls lbl ls k with |
---|
497 | [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in |
---|
498 | ∃u',cs,k1'. |
---|
499 | find_label_ls lbl (\fst (label_lstatements ls u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧ |
---|
500 | cont_with_labels k1 k1' |
---|
501 | | None ⇒ find_label_ls lbl (\fst (label_lstatements ls u)) k' = None ? |
---|
502 | ]) |
---|
503 | … s) |
---|
504 | [ #k #k' #u #F @refl |
---|
505 | | #e1 #e2 #k #k' #u #K @blindly_label #u1 #u2 whd @refl |
---|
506 | | #e0 #e #args #k #k' #u #K @blindly_label #u1 #u2 #u3 whd @refl |
---|
507 | | #sA #sB #IH1 #IH2 #k #k' #u #K @blindly_label #u1 #u2 whd in match (find_label ???); |
---|
508 | whd in match (find_label ?? k'); |
---|
509 | @(lfl_IH sA … IH1) [ /2/ ] |
---|
510 | cases (find_label ???) |
---|
511 | [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' |
---|
512 | @(lfl_IH … IH2) [ // ] |
---|
513 | cases (find_label ???) |
---|
514 | [ whd in ⊢ (% → %); #FIND2' whd in ⊢ (??%?); >FIND1' >FIND2' @refl |
---|
515 | | * #s3 #k3 whd in ⊢ (% → %); * #u3 * #cs * #k1' * #FIND2' #K1' |
---|
516 | % [2: %{cs} %{k1'} % // whd in ⊢ (??%?); >FIND1' in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl | skip ] |
---|
517 | ] |
---|
518 | | * #sA' #kA' whd in ⊢ (% → %); |
---|
519 | * #u1' * #cs * #k1' * #FA' #K' |
---|
520 | % [2: %{cs} %{k1'} % [ whd in ⊢ (??%?); >FA' in ⊢ (??%?); @refl | // ] |skip] |
---|
521 | ] |
---|
522 | | #e #s1 #s2 #IH1 #IH2 #k #k' #u @blindly_label #u1 #u2 #u3 #c2 #c3 #K |
---|
523 | whd in match (find_label ?? k); whd in match (find_label ?? k'); |
---|
524 | whd in match (find_label ?? k'); |
---|
525 | @(lfl_IH … IH1) [ // ] cases (find_label ???) |
---|
526 | [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' |
---|
527 | lapply (IH2 k k' u3 K) cases (find_label ???) |
---|
528 | [ whd in ⊢ (% → %); #FIND2' |
---|
529 | whd in match (find_label ???); >FIND1' |
---|
530 | whd in match (find_label ???); >FIND2' @refl |
---|
531 | | * #s2' #k2' * #u4 * #cs * #k1' * #FIND2' #K2' |
---|
532 | % [2: % [2: % [2: % [ whd in ⊢ (??%?); |
---|
533 | whd in match (find_label ???); >FIND1' in ⊢ (??%?); |
---|
534 | whd in match (find_label ???); >FIND2' in ⊢ (??%?); @refl |
---|
535 | | // ]|skip]|skip]|skip] |
---|
536 | ] |
---|
537 | | * #s1' #k1 whd in ⊢ (% → %); * #u4 * #cs * #k1' * #FIND1' #K1' |
---|
538 | % [2: % [2: % [2: % [ |
---|
539 | whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?); |
---|
540 | @refl | // ] |skip ]| skip ]| skip ] |
---|
541 | ] |
---|
542 | | #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost |
---|
543 | whd in match (find_label ?? k); normalize in match (find_label ?? k'); |
---|
544 | @(lfl_IH s0 … IH) [ /2/ ] |
---|
545 | cases (find_label ???) |
---|
546 | [ whd in ⊢ (% → %); #FIND1' |
---|
547 | whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl |
---|
548 | | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1' |
---|
549 | % [2: % [2: % [2: % [ |
---|
550 | whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?); |
---|
551 | @refl | // ]| skip ]| skip ]| skip ] |
---|
552 | ] |
---|
553 | | #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost |
---|
554 | whd in match (find_label ?? k); normalize in match (find_label ?? k'); |
---|
555 | @(lfl_IH s0 … IH) [ /2/ ] |
---|
556 | cases (find_label ???) |
---|
557 | [ whd in ⊢ (% → %); #FIND1' |
---|
558 | whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl |
---|
559 | | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1' |
---|
560 | % [2: % [2: % [2: % [ |
---|
561 | whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?); |
---|
562 | @refl | // ]| skip ]| skip ]| skip ] |
---|
563 | ] |
---|
564 | | #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4 |
---|
565 | whd in match (find_label ???); normalize in match (find_label ?? k'); |
---|
566 | @(lfl_IH s1 … IH1) [ /2/ ] |
---|
567 | cases (find_label ???) |
---|
568 | [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' >FIND1' |
---|
569 | @(lfl_IH s3 … IH3) [ /2/ ] |
---|
570 | cases (find_label ???) |
---|
571 | [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND3' >FIND3' |
---|
572 | @(lfl_IH s2 … IH2) [ /2/ ] |
---|
573 | cases (find_label ???) |
---|
574 | [ whd in ⊢ (% → %); #FIND2' >FIND2' @refl |
---|
575 | | * #s2' #k2' * #u2' * #cs' * #k1' * #FIND2' #K2' |
---|
576 | % [2: % [2: % [2: % [ |
---|
577 | whd in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl |
---|
578 | | // ]| skip ]| skip ]| skip ] |
---|
579 | ] |
---|
580 | | * #s3' #k3' * #u3' * #cs' * #k1' * #FIND3' #K3' |
---|
581 | % [2: % [2: % [2: % [ |
---|
582 | >FIND3' in ⊢ (??%?); whd in ⊢ (??%?); @refl |
---|
583 | | // ]| skip ]| skip ]| skip ] |
---|
584 | ] |
---|
585 | | * #s1' #k1' * #u1' * #cs' * #k1' * #FIND1' #K1' |
---|
586 | % [2: % [2: % [2: % [ |
---|
587 | >FIND1' in ⊢ (??%?); whd in ⊢ (??%?); @refl |
---|
588 | | // ]| skip ]| skip ]| skip ] |
---|
589 | ] |
---|
590 | | // |
---|
591 | | // |
---|
592 | | #eo #k #k' #u @blindly_label #u1 // |
---|
593 | | #e #ls #IH #k #k' #u #K @blindly_label #u1 #u2 |
---|
594 | normalize in match (find_label ???); normalize in match (find_label ???); |
---|
595 | lapply (IH (Kswitch k) (Kswitch k') u2 ?) [/2/] cases (find_label_ls ???) |
---|
596 | [ whd in ⊢ (% → %); // |
---|
597 | | * #s1' #k1' * #u' * #cs * #k'' * #FIND' #K' |
---|
598 | % [2: % [2: % [2: % [ @FIND' | // ]|skip ]|skip]|skip] |
---|
599 | ] |
---|
600 | | #l #s0 #IH #k #k' #u #K @blindly_label #u1 #cs |
---|
601 | whd in match (find_label ???); whd in match (find_label ?? k'); |
---|
602 | cases (ident_eq lbl l) |
---|
603 | [ #E destruct whd |
---|
604 | % [2: % [2: % [2: % [ @refl | // ]|skip ]|skip ]| skip ] |
---|
605 | | #NE whd in ⊢ (match % with [_⇒?|_⇒?]); |
---|
606 | normalize in match (find_label ?? k'); |
---|
607 | @(lfl_IH s0 … IH) [ // ] |
---|
608 | cases (find_label ???) |
---|
609 | [ // |
---|
610 | | * #s0' #k0' * #u' * #cs0 * #k1' * #FIND0 #K0 |
---|
611 | % [2: % [2: % [2: % [ @FIND0 | // ]|skip ]|skip]|skip] |
---|
612 | ] |
---|
613 | ] |
---|
614 | | // |
---|
615 | | #l #s0 #IH #k #k' #u #K @blindly_label #u1 /2/ |
---|
616 | | #s0 #IH #k #k' #u whd in match (label_lstatements ??); |
---|
617 | @label_gen_elim #u1 >shift_fst >shift_fst |
---|
618 | whd in match (find_label_ls ???); whd in match (find_label_ls ???); |
---|
619 | @IH |
---|
620 | | #sz #i #s0 #tl #IH1 #IH2 #k #k' #u #K |
---|
621 | whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2 |
---|
622 | @label_gen_elim #u3 >shift_fst |
---|
623 | whd in match (find_label_ls ???); normalize in match (find_label_ls ?? k'); |
---|
624 | @(lfl_IH s0 … IH1) [ /2/ ] |
---|
625 | cases (find_label ???) |
---|
626 | [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND0 >FIND0 |
---|
627 | lapply (IH2 k k' u2 K) cases (find_label_ls ???) |
---|
628 | [ whd in ⊢ (% → %); #FINDtl >FINDtl @refl |
---|
629 | | * #stl #ktl // |
---|
630 | ] |
---|
631 | | * #s0' #k0' whd in ⊢ (% → %); |
---|
632 | * #u' * #cs * #k1' * #FIND0 #K0 >FIND0 |
---|
633 | % [2: % [2: % [2: % [ @refl | // ] | skip ] | skip ] | skip ] |
---|
634 | ] |
---|
635 | ] qed. |
---|
636 | |
---|
637 | lemma label_find_label_fn : ∀lbl,f,k,k',s1,k1. |
---|
638 | cont_with_labels k k' → |
---|
639 | find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 → |
---|
640 | ∃u',cs,k1'. |
---|
641 | find_label lbl (fn_body (label_function f)) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧ |
---|
642 | cont_with_labels k1 k1'. |
---|
643 | #lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND |
---|
644 | whd in match (label_function ?); |
---|
645 | @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst |
---|
646 | lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?) |
---|
647 | [ /2/ ] |
---|
648 | >FIND // |
---|
649 | qed. |
---|
650 | |
---|
651 | |
---|
652 | (* We show the main simulation in two stages. First, we show it for all states |
---|
653 | in the relation *except* those for labeled_statements, then we'll show the |
---|
654 | whole thing. This is so that we can appeal to the other cases in the proof |
---|
655 | for labeled_statements. *) |
---|
656 | lemma step_with_labels_partial : ∀ge,ge'. |
---|
657 | related_globals … label_fundef ge ge' → |
---|
658 | ∀s1,s1',tr,s2. |
---|
659 | state_with_labels_partial s1 s1' → |
---|
660 | exec_step ge s1 = Value … 〈tr,s2〉 → |
---|
661 | ∃tr',s2'. plus ge' s1' tr' s2' ∧ |
---|
662 | trace_with_extra_labels tr tr' ∧ |
---|
663 | state_with_labels s2 s2'. |
---|
664 | |
---|
665 | (* General plan is like the expressions result, except that we do case analysis |
---|
666 | on the simulation first, then: break up the original execution, break up the |
---|
667 | cost labelling, use the earlier results to deal with expressions, then |
---|
668 | run the labelled version for enough steps. We try to avoid having to write |
---|
669 | out the final trace and state and "skip" them afterwards. *) |
---|
670 | #ge #ge' #RG #Xs1 #Xs1' #tr #s2 * |
---|
671 | [ #f #us #s #k #k' #e #m #KL cases s |
---|
672 | [ #EX inversion KL |
---|
673 | [ #E1 #E2 #_ destruct %{tr} |
---|
674 | whd in EX:(??%?); |
---|
675 | lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?); |
---|
676 | [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))} |
---|
677 | % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl |
---|
678 | | // ] | /3/ ] |
---|
679 | | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct |
---|
680 | ] |
---|
681 | | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} |
---|
682 | %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)} |
---|
683 | whd in EX:(??%%); destruct |
---|
684 | % [ % [ @plus_one @refl | // ] | /3/ ] |
---|
685 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} |
---|
686 | whd in EX:(??%%); destruct |
---|
687 | % [ 2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ] |
---|
688 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
689 | cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem |
---|
690 | cases (bindIO_inversion ??????? EXrem) * * #EXb #EXbrem -EXrem |
---|
691 | normalize in EXbrem; destruct |
---|
692 | cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te |
---|
693 | [ % [ 2: % [ 2: % [ % [ @plus_one |
---|
694 | whd in ⊢ (??%?); >EXe' in ⊢ (??%?); |
---|
695 | whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?); |
---|
696 | whd in ⊢ (??%?); @refl |
---|
697 | | // ] |
---|
698 | | @swl_partial @swl_dowhilestate // ] | skip ] | skip ] |
---|
699 | | % [ 2: % [ 2: % [ % [ @plus_succ [ |
---|
700 | 4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?); |
---|
701 | whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?); |
---|
702 | whd in ⊢ (??%?); @refl |
---|
703 | | skip | skip |
---|
704 | | 5: @plus_succ [ 4: @refl | skip | skip |
---|
705 | | 5: @plus_one @refl | skip ] | skip ] |
---|
706 | | <(E0_right tr) @twel_app /2/ ] |
---|
707 | | /3/ ] | skip ] | skip ] |
---|
708 | ] |
---|
709 | | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
710 | whd in EX:(??%?); destruct |
---|
711 | %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ] |
---|
712 | | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
713 | whd in EX:(??%?); destruct |
---|
714 | %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ] |
---|
715 | | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
716 | whd in EX:(??%?); destruct |
---|
717 | %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ] |
---|
718 | | #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
719 | whd in EX:(??%?); destruct |
---|
720 | %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ] |
---|
721 | | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
722 | whd in EX:(??%?); |
---|
723 | lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?); |
---|
724 | [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct |
---|
725 | %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?); |
---|
726 | @refl | // ] | /4/ ] | skip ] |
---|
727 | | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct |
---|
728 | ] |
---|
729 | | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
730 | % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ]| skip ]| skip ] |
---|
731 | ] |
---|
732 | | * #a1 #ty1 #a2 #EX |
---|
733 | cases (bindIO_inversion ??????? EX) -EX * * #b1 #o1 #tr1 * #EX1 #EX |
---|
734 | cases (bindIO_inversion ??????? EX) -EX * #v2 #tr2 * #EX2 #EX |
---|
735 | cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX |
---|
736 | whd in EX:(??%%); destruct |
---|
737 | cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 us) #tr1' * #EX1' #T1 |
---|
738 | whd in match (label_statement ??); |
---|
739 | @label_gen_elim #ua1 @label_gen_elim #ua2 |
---|
740 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2 |
---|
741 | % [2: % [2: % [ % [ |
---|
742 | @plus_one whd in ⊢ (??%?); |
---|
743 | >exec_lvalue_labelled >EX1' in ⊢ (??%?); |
---|
744 | whd in ⊢ (??%?); >EX2' in ⊢ (??%?); |
---|
745 | whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?); |
---|
746 | @refl |
---|
747 | | @twel_app // ] | /3/ ] | skip ] | skip ] |
---|
748 | | * [2: * #er #tyr ] #ef #args #EX |
---|
749 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
750 | cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX |
---|
751 | cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX |
---|
752 | cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX |
---|
753 | whd in EX:(??%%); |
---|
754 | [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ] |
---|
755 | destruct |
---|
756 | whd in match (label_statement ??); |
---|
757 | whd in match (label_opt_expr ??); |
---|
758 | [ @(label_gen_elim … (Expr er tyr)) #u' @breakup_pair | letin u' ≝ us ] |
---|
759 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u') #tr1' * #EX1' #T1 |
---|
760 | @label_gen_elim #u1 |
---|
761 | @label_gen_elim #u2 |
---|
762 | cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2 |
---|
763 | [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ] |
---|
764 | % [2,4: % [2,4: % [1,3: % [1,3: |
---|
765 | @plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *) |
---|
766 | whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ] |
---|
767 | whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?); |
---|
768 | whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ] |
---|
769 | whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ] |
---|
770 | @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ] |
---|
771 | | #st1 #st2 #EX |
---|
772 | whd in EX:(??%%); destruct |
---|
773 | whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 |
---|
774 | %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ] |
---|
775 | | #a #st1 #st2 #EX |
---|
776 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
777 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
778 | normalize in EX; destruct |
---|
779 | whd in match (label_statement ??); @label_gen_elim #u1 |
---|
780 | @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4 |
---|
781 | @label_gen_elim #u5 |
---|
782 | whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 |
---|
783 | whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7 |
---|
784 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 |
---|
785 | % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: |
---|
786 | whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) |
---|
787 | whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] |
---|
788 | whd in ⊢ (??%?); @refl |
---|
789 | | 1,2,6,7: skip |
---|
790 | | 5,10: @plus_one @refl |
---|
791 | | *: skip |
---|
792 | ] |
---|
793 | | 2,4: <(E0_right tr) @twel_app /2/ |
---|
794 | ]| 2,4: /3/ ] | *: skip ] | *: skip ] |
---|
795 | | #a #st #EX |
---|
796 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
797 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
798 | normalize in EX; destruct |
---|
799 | whd in match (label_statement ??); @label_gen_elim #u1 |
---|
800 | @label_gen_elim #u2 |
---|
801 | whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 |
---|
802 | >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 |
---|
803 | >shift_fst |
---|
804 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 |
---|
805 | % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip |
---|
806 | | 5,10: @plus_succ [ 4,9: |
---|
807 | whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) |
---|
808 | whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] |
---|
809 | whd in ⊢ (??%?); @refl |
---|
810 | | 1,2,6,7: skip |
---|
811 | | 5: @plus_one @refl |
---|
812 | | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ] |
---|
813 | | *: skip |
---|
814 | ] |
---|
815 | | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/ |
---|
816 | ]| 2,4: /4/ ] | *: skip ] | *: skip ] |
---|
817 | | #a #st #EX |
---|
818 | normalize in EX; destruct |
---|
819 | whd in match (label_statement ??); @label_gen_elim #u1 |
---|
820 | @label_gen_elim #u2 |
---|
821 | whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst |
---|
822 | whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst |
---|
823 | % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip |
---|
824 | | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ] |
---|
825 | | /2/ ] | /4/ ] | skip ] | skip ] |
---|
826 | | #st1 #a #st2 #st #EX |
---|
827 | lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip |
---|
828 | whd in EX:(??%?); >Eskip in EX; #EX |
---|
829 | whd in match (label_statement ??); @label_gen_elim #u1 |
---|
830 | @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4 |
---|
831 | whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst |
---|
832 | whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst |
---|
833 | [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
834 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
835 | normalize in EX; destruct |
---|
836 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 |
---|
837 | % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip |
---|
838 | | 5,10: @plus_succ [ 4,9: |
---|
839 | whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) |
---|
840 | whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] |
---|
841 | whd in ⊢ (??%?); @refl |
---|
842 | | 1,2,6,7: skip |
---|
843 | | 5: @plus_one @refl |
---|
844 | | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ] |
---|
845 | | *: skip |
---|
846 | ] |
---|
847 | | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/ |
---|
848 | ]| 2,4: /4/ ] | *: skip ] | *: skip ] |
---|
849 | | whd in EX:(??%%); destruct |
---|
850 | % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one |
---|
851 | whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip' |
---|
852 | >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ] |
---|
853 | | skip ] | skip ] |
---|
854 | ] |
---|
855 | | #EX inversion KL |
---|
856 | [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
857 | |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
858 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
859 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
860 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
861 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
862 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
863 | | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
864 | | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
865 | | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
866 | ] |
---|
867 | whd in match (label_statement ??); |
---|
868 | % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: % |
---|
869 | [1,11,13: @plus_one @refl | 2,12,14: // |
---|
870 | | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/ |
---|
871 | | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/ |
---|
872 | | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/ |
---|
873 | | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/ |
---|
874 | ]| *: /3/ ]|*: skip]|*: skip ] |
---|
875 | | #EX inversion KL |
---|
876 | [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
877 | |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
878 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
879 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
880 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
881 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
882 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
883 | | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
884 | | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
885 | | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
886 | ] |
---|
887 | whd in match (label_statement ??); |
---|
888 | [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: % |
---|
889 | [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ] |
---|
890 | | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ] |
---|
891 | | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
892 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
893 | normalize in EX; destruct |
---|
894 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1 |
---|
895 | % [2,4: % [2,4: % [1,3: % [1,3: [ @plus_one | @plus_succ ] [ 1,5: |
---|
896 | whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) |
---|
897 | whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] |
---|
898 | whd in ⊢ (??%?); @refl |
---|
899 | | 6: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ] |
---|
900 | | // | <(E0_right tr) @twel_app /2/ |
---|
901 | ] |
---|
902 | | /3/ | /3/ ] | *: skip ] | *: skip ] |
---|
903 | ] |
---|
904 | | * [2: #a ] #EX |
---|
905 | whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX; |
---|
906 | #Ety #EX whd in EX:(??%?); |
---|
907 | [ destruct |
---|
908 | | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
909 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 |
---|
910 | | >Ety in EX; #EX |
---|
911 | | @⊥ cases (fn_return f) in Ety EX; |
---|
912 | [ * #H cases (H (refl ??)) |
---|
913 | | *: normalize #a #b #c try #d try #e destruct |
---|
914 | ] |
---|
915 | ] |
---|
916 | whd in match (label_statement ??); |
---|
917 | [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ] |
---|
918 | whd in EX:(??%%); destruct |
---|
919 | % [2,4: % [2,4: % [1,3: %[1,3: @plus_one |
---|
920 | whd in ⊢ (??%?); |
---|
921 | [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety'' |
---|
922 | whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
923 | | >label_function_return >Ety in ⊢ (??%?); |
---|
924 | ] whd in ⊢ (??%?); @refl |
---|
925 | | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip] |
---|
926 | | #a #ls #EX |
---|
927 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
928 | cases v1 in EX1 EX; |
---|
929 | [ 2: #sz #i #EX1 #EX |
---|
930 | | *: normalize #A #B try #C destruct |
---|
931 | ] |
---|
932 | whd in EX:(??%%); destruct |
---|
933 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 |
---|
934 | whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 |
---|
935 | % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl |
---|
936 | | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/ |
---|
937 | ]|skip ]| skip ] |
---|
938 | | #l #st #EX |
---|
939 | whd in EX:(??%?); destruct |
---|
940 | whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst |
---|
941 | whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst |
---|
942 | %[2: %[2: %[ %[ @plus_succ |
---|
943 | [ 4: @refl | 5: @plus_one @refl | *: skip ] |
---|
944 | | /2/ ] | /3/ ] |skip ]| skip ] |
---|
945 | | #l #EX |
---|
946 | whd in EX:(??%?); |
---|
947 | @blindly_label whd |
---|
948 | lapply (refl ? (find_label l (fn_body f) (call_cont k))) |
---|
949 | cases (find_label ???) in ⊢ (???% → ?); |
---|
950 | [ #F @⊥ >F in EX; #EX whd in EX:(??%?); destruct |
---|
951 | | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct |
---|
952 | cases (label_find_label_fn … KL F) |
---|
953 | #u' * #cs * #k1' * #F' #K' |
---|
954 | % [2: %[2: %[ %[ @plus_succ |
---|
955 | [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ] |
---|
956 | | /2/ ] | /3/ ] | skip ] | skip ] |
---|
957 | ] |
---|
958 | | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1 |
---|
959 | % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]| skip ] |
---|
960 | ] |
---|
961 | | #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX |
---|
962 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
963 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
964 | whd in EX:(??%%); destruct |
---|
965 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1 |
---|
966 | [ % [2: % [2: % [ % [ |
---|
967 | @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
968 | whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl |
---|
969 | |5: @plus_one @refl | *: skip ] |
---|
970 | | <(E0_right tr) /3/ ]| /4/ ]| skip ]| skip ] |
---|
971 | | % [2: % [2: % [ % [ |
---|
972 | @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
973 | whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl |
---|
974 | | 5: @plus_succ [4: @refl |
---|
975 | | 5: @plus_one @refl | *: skip ] | *: skip ] |
---|
976 | | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ] |
---|
977 | ] |
---|
978 | | #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX |
---|
979 | whd in EX:(??%%); destruct |
---|
980 | % [2: % [2: % [ % [ |
---|
981 | @plus_succ [4: % | 5: @plus_one % | *: skip ] |
---|
982 | | /2/ ]| /4/ ]| skip ]| skip ] |
---|
983 | | #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX |
---|
984 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
985 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
986 | whd in EX:(??%%); destruct |
---|
987 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1 |
---|
988 | [ % [2: % [2: % [ % [ |
---|
989 | @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
990 | whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl |
---|
991 | | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl |
---|
992 | | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ] |
---|
993 | | % [2: % [2: % [ % [ |
---|
994 | @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
995 | whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl |
---|
996 | | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl |
---|
997 | | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip |
---|
998 | ] |
---|
999 | ] |
---|
1000 | | * |
---|
1001 | [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX |
---|
1002 | cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX |
---|
1003 | whd in EX:(??%%); destruct |
---|
1004 | whd in match (label_fundef ?); |
---|
1005 | whd in match (label_function ?); |
---|
1006 | lapply (refl ? (label_function f)) whd in ⊢ (???% → ?); |
---|
1007 | @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef |
---|
1008 | % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?); |
---|
1009 | whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl |
---|
1010 | | 5: @plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ] |
---|
1011 | | #id #tys #ty #args #k #k' #m #K #EX |
---|
1012 | cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX |
---|
1013 | cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX |
---|
1014 | whd in EX2:(??%%); destruct |
---|
1015 | ] |
---|
1016 | | #res #k #k' #m #K #EX inversion K |
---|
1017 | [ #E1 #E2 #E3 destruct cases res in EX ⊢ %; |
---|
1018 | [ 2: * #i #EX whd in EX:(??%?); destruct |
---|
1019 | | *: normalize #A try #B try #C destruct |
---|
1020 | ] |
---|
1021 | % [2: % [2: % [ % [ @plus_one @refl | // ]| /2/ ]| skip ]| skip ] |
---|
1022 | | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %; |
---|
1023 | [ #EX whd in EX:(??%?); destruct |
---|
1024 | % [2: % [2: % [ % [ @plus_one @refl | // ]| /3/ ]| skip ]| skip ] |
---|
1025 | | * * #b #o #ty #EX |
---|
1026 | cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX |
---|
1027 | whd in EX:(??%%); destruct |
---|
1028 | % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ] |
---|
1029 | ] |
---|
1030 | | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O |
---|
1031 | destruct whd in EX:(??%?); destruct |
---|
1032 | ] |
---|
1033 | | #r #EX whd in EX:(??%%); destruct |
---|
1034 | ] qed. |
---|
1035 | |
---|
1036 | |
---|
1037 | theorem step_with_labels : ∀ge,ge'. |
---|
1038 | related_globals … label_fundef ge ge' → |
---|
1039 | ∀s1,s1',tr,s2. |
---|
1040 | state_with_labels s1 s1' → |
---|
1041 | (exec_step ge s1 = Value … 〈tr,s2〉 → |
---|
1042 | ∃tr',s2'. plus ge' s1' tr' s2' ∧ |
---|
1043 | trace_with_extra_labels tr tr' ∧ |
---|
1044 | state_with_labels s2 s2'). |
---|
1045 | #ge #ge' #RG #Xs1 #Xs1' #tr #s2 * |
---|
1046 | [ #s1 #s1' @step_with_labels_partial // |
---|
1047 | | #f #u * |
---|
1048 | (* If we have LSdefault we need to smuggle the execution of the cost label in |
---|
1049 | before the actual statement. *) |
---|
1050 | [ #s #k #k' #e #m #K #EX |
---|
1051 | whd in EX:(??(??(??%???))?); |
---|
1052 | whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2 |
---|
1053 | >shift_fst whd in match (seq_of_labeled_statement ?); |
---|
1054 | cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX) |
---|
1055 | #tr' * #s2' * * #P #T #S |
---|
1056 | % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ] |
---|
1057 | (* but for LScase it's just like the cases in step_with_labels_partial *) |
---|
1058 | | #sz #i #s #ls #k #k' #e #m #K #EX |
---|
1059 | whd in EX:(??(??(??%???))?); |
---|
1060 | whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2 |
---|
1061 | @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?); |
---|
1062 | whd in EX:(??%?); destruct |
---|
1063 | % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ] |
---|
1064 | ] |
---|
1065 | ] qed. |
---|
1066 | |
---|
1067 | |
---|
1068 | lemma initial_state_in_simulation : ∀p,s. |
---|
1069 | make_initial_state p = OK ? s → |
---|
1070 | ∃s'. make_initial_state (clight_label p) = OK ? s' ∧ state_with_labels s s'. |
---|
1071 | * #vars #fns #main #s |
---|
1072 | whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX |
---|
1073 | cases (bind_inversion ????? EX) -EX #m * #Em #EX |
---|
1074 | cases (bind_inversion ????? EX) -EX #b * #Emain #EX |
---|
1075 | cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX |
---|
1076 | whd in EX:(??%%); destruct |
---|
1077 | whd in match (make_initial_state ?); |
---|
1078 | letin ge' ≝ (make_global ?) |
---|
1079 | cut (related_globals … label_fundef ge ge') |
---|
1080 | [ // ] #RG |
---|
1081 | % [2: % |
---|
1082 | [ whd in ⊢ (??%?); |
---|
1083 | change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?); |
---|
1084 | >init_mem_transf >Em in ⊢ (??%?); |
---|
1085 | whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?); |
---|
1086 | whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain') |
---|
1087 | whd in ⊢ (??%?); @refl |
---|
1088 | | /3/ |
---|
1089 | ] | skip ] |
---|
1090 | qed. |
---|
1091 | |
---|
1092 | |
---|
1093 | |
---|