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