1 | include "Clight/Csyntax.ma". |
---|
2 | include "Clight/fresh.ma". |
---|
3 | include "basics/lists/list.ma". |
---|
4 | include "basics/lists/listb.ma". |
---|
5 | include "common/Identifiers.ma". |
---|
6 | include "utilities/extralib.ma". |
---|
7 | include "Clight/Cexec.ma". |
---|
8 | include "Clight/CexecInd.ma". |
---|
9 | include "Clight/frontend_misc.ma". |
---|
10 | include "Clight/memoryInjections.ma". |
---|
11 | |
---|
12 | (* ----------------------------------------------------------------------------- |
---|
13 | ----------------------------------------------------------------------------*) |
---|
14 | |
---|
15 | (* ----------------------------------------------------------------------------- |
---|
16 | Documentation |
---|
17 | ----------------------------------------------------------------------------*) |
---|
18 | |
---|
19 | (* This file implements transformation of switches to linear sequences of |
---|
20 | * if/then/else. The implementation roughly follows the lines of the prototype. |
---|
21 | * /!\ We assume that the program is well-typed (the type of the evaluated |
---|
22 | * expression must match the constants on each branch of the switch). /!\ *) |
---|
23 | |
---|
24 | (* Documentation. Let the follwing be our input switch construct: |
---|
25 | // --------------------------------- |
---|
26 | switch(e) { |
---|
27 | case v1: |
---|
28 | stmt1 |
---|
29 | case v2: |
---|
30 | stmt2 |
---|
31 | . |
---|
32 | . |
---|
33 | . |
---|
34 | default: |
---|
35 | stmt_default |
---|
36 | } |
---|
37 | // --------------------------------- |
---|
38 | |
---|
39 | Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting |
---|
40 | the switch statement. In the absence of break, the execution falls through each case sequentially. |
---|
41 | |
---|
42 | Given such a statement, we produce an equivalent sequence of if-then-elses chained by gotos: |
---|
43 | |
---|
44 | // --------------------------------- |
---|
45 | fresh = e; |
---|
46 | if(fresh == v1) { |
---|
47 | stmt1'; |
---|
48 | goto lbl_case2; |
---|
49 | } |
---|
50 | if(fresh == v2) { |
---|
51 | lbl_case2: |
---|
52 | stmt2'; |
---|
53 | goto lbl_case2; |
---|
54 | } |
---|
55 | ... |
---|
56 | stmt_default'; |
---|
57 | exit_label: |
---|
58 | // --------------------------------- |
---|
59 | |
---|
60 | where stmt1', stmt2', ... stmt_default' are the statements where all top-level [break] statements |
---|
61 | were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels. |
---|
62 | *) |
---|
63 | |
---|
64 | |
---|
65 | (* ----------------------------------------------------------------------------- |
---|
66 | Definitions allowing to state that the program resulting of the transformation |
---|
67 | is switch-free. |
---|
68 | ---------------------------------------------------------------------------- *) |
---|
69 | |
---|
70 | (* Property of a Clight statement of containing no switch. Could be generalized into a kind of |
---|
71 | * statement_P, if useful elsewhere. *) |
---|
72 | let rec switch_free (st : statement) : Prop ≝ |
---|
73 | match st with |
---|
74 | [ Sskip ⇒ True |
---|
75 | | Sassign _ _ ⇒ True |
---|
76 | | Scall _ _ _ ⇒ True |
---|
77 | | Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2 |
---|
78 | | Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2 |
---|
79 | | Swhile e body _ ⇒ switch_free body |
---|
80 | | Sdowhile e body ⇒ switch_free body |
---|
81 | | Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3 |
---|
82 | | Sbreak ⇒ True |
---|
83 | | Scontinue ⇒ True |
---|
84 | | Sreturn _ ⇒ True |
---|
85 | | Sswitch _ _ ⇒ False |
---|
86 | | Slabel _ body ⇒ switch_free body |
---|
87 | | Sgoto _ ⇒ True |
---|
88 | | Scost _ body ⇒ switch_free body |
---|
89 | ]. |
---|
90 | |
---|
91 | (* Property of a list of labeled statements of being switch-free *) |
---|
92 | let rec branches_switch_free (sts : labeled_statements) : Prop ≝ |
---|
93 | match sts with |
---|
94 | [ LSdefault st => |
---|
95 | switch_free st |
---|
96 | | LScase _ _ st tl => |
---|
97 | switch_free st ∧ branches_switch_free tl |
---|
98 | ]. |
---|
99 | |
---|
100 | let rec branches_ind |
---|
101 | (sts : labeled_statements) |
---|
102 | (H : labeled_statements → Prop) |
---|
103 | (defcase : ∀st. H (LSdefault st)) |
---|
104 | (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝ |
---|
105 | match sts with |
---|
106 | [ LSdefault st ⇒ |
---|
107 | defcase st |
---|
108 | | LScase sz int st tl ⇒ |
---|
109 | indcase sz int st tl (branches_ind tl H defcase indcase) |
---|
110 | ]. |
---|
111 | |
---|
112 | (* ----------------------------------------------------------------------------- |
---|
113 | Switch-removal code for statements, functions and fundefs. |
---|
114 | ----------------------------------------------------------------------------*) |
---|
115 | |
---|
116 | (* Converts the directly accessible ("free") breaks to gotos toward the [lab] label. *) |
---|
117 | let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝ |
---|
118 | match st with |
---|
119 | [ Sbreak ⇒ |
---|
120 | Sgoto lab |
---|
121 | | Ssequence s1 s2 ⇒ |
---|
122 | Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab) |
---|
123 | | Sifthenelse e iftrue iffalse ⇒ |
---|
124 | Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab) |
---|
125 | | Sfor init e update body ⇒ |
---|
126 | Sfor (convert_break_to_goto init lab) e update body |
---|
127 | | Slabel l body ⇒ |
---|
128 | Slabel l (convert_break_to_goto body lab) |
---|
129 | | Scost cost body ⇒ |
---|
130 | Scost cost (convert_break_to_goto body lab) |
---|
131 | | _ ⇒ st |
---|
132 | ]. |
---|
133 | |
---|
134 | (* Converting breaks preserves switch-freeness. *) |
---|
135 | lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label). |
---|
136 | #s elim s // |
---|
137 | [ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ |
---|
138 | | 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ |
---|
139 | | 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize |
---|
140 | try @conj try @conj /3/ |
---|
141 | | 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/ |
---|
142 | | 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/ |
---|
143 | ] qed. |
---|
144 | |
---|
145 | (* (def_case : ident × sf_statement) *) |
---|
146 | |
---|
147 | let rec produce_cond |
---|
148 | (e : expr) |
---|
149 | (switch_cases : labeled_statements) |
---|
150 | (u : universe SymbolTag) |
---|
151 | (exit : label) on switch_cases : statement × label × (universe SymbolTag) ≝ |
---|
152 | match switch_cases with |
---|
153 | [ LSdefault st ⇒ |
---|
154 | let 〈lab,u1〉 ≝ fresh ? u in |
---|
155 | let st' ≝ convert_break_to_goto st exit in |
---|
156 | 〈Slabel lab st', lab, u1〉 |
---|
157 | | LScase sz tag st other_cases ⇒ |
---|
158 | let 〈sub_statements, sub_label, u1〉 ≝ produce_cond e other_cases u exit in |
---|
159 | let st' ≝ convert_break_to_goto st exit in |
---|
160 | let 〈lab, u2〉 ≝ fresh ? u1 in |
---|
161 | let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz tag) (typeof e))) (Tint I32 Signed) in |
---|
162 | let case_statement ≝ |
---|
163 | Sifthenelse test |
---|
164 | (Slabel lab (Ssequence st' (Sgoto sub_label))) |
---|
165 | Sskip |
---|
166 | in |
---|
167 | 〈Ssequence case_statement sub_statements, lab, u2〉 |
---|
168 | ]. |
---|
169 | |
---|
170 | definition simplify_switch ≝ |
---|
171 | λ(e : expr). |
---|
172 | λ(switch_cases : labeled_statements). |
---|
173 | λ(uv : universe SymbolTag). |
---|
174 | let 〈exit_label, uv1〉 ≝ fresh ? uv in |
---|
175 | let 〈result, useless_label, uv2〉 ≝ produce_cond e switch_cases uv1 exit_label in |
---|
176 | 〈Ssequence result (Slabel exit_label Sskip), uv2〉. |
---|
177 | |
---|
178 | lemma produce_cond_switch_free : ∀l.∀H:branches_switch_free l.∀e,lab,u.switch_free (\fst (\fst (produce_cond e l u lab))). |
---|
179 | #l @(labeled_statements_ind … l) |
---|
180 | [ 1: #s #Hsf #e #lab #u normalize cases (fresh ??) #lab0 #u1 |
---|
181 | normalize in Hsf ⊢ %; @(convert_break_lift … Hsf) |
---|
182 | | 2: #sz #i #hd #tl #Hind whd in ⊢ (% → ?); * #Hsf_hd #Hsf_tl |
---|
183 | #e #lab #u normalize |
---|
184 | lapply (Hind Hsf_tl e lab u) |
---|
185 | cases (produce_cond e tl u lab) * #cond #lab' #u' #Hsf normalize nodelta |
---|
186 | cases (fresh ??) #lab0 #u2 normalize nodelta |
---|
187 | normalize try @conj try @conj try @conj try // |
---|
188 | @(convert_break_lift … Hsf_hd) |
---|
189 | ] qed. |
---|
190 | |
---|
191 | lemma simplify_switch_switch_free : ∀e,l. ∀H:branches_switch_free l. ∀u. switch_free (\fst (simplify_switch e l u)). |
---|
192 | #e #l cases l |
---|
193 | [ 1: #def normalize #H #u cases (fresh ? u) #exit_label #uv normalize cases (fresh ? uv) #lab #uv' normalize nodelta |
---|
194 | whd @conj whd |
---|
195 | [ 1: @convert_break_lift assumption |
---|
196 | | 2: @I ] |
---|
197 | | 2: #sz #i #case #tl normalize * #Hsf #Hsftl #u |
---|
198 | cases (fresh ? u) #exit_label #uv1 normalize nodelta |
---|
199 | lapply (produce_cond_switch_free tl Hsftl e exit_label uv1) |
---|
200 | cases (produce_cond e tl uv1 exit_label) |
---|
201 | * #cond #lab #u1 #Hsf_cond normalize nodelta |
---|
202 | cases (fresh ??) #lab0 #u2 normalize nodelta |
---|
203 | normalize @conj try @conj try @conj try @conj try // |
---|
204 | @(convert_break_lift ?? Hsf) |
---|
205 | ] qed. |
---|
206 | |
---|
207 | (* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in |
---|
208 | order to circumvent the associativity problems in notations. *) |
---|
209 | record swret (A : Type[0]) : Type[0] ≝ { |
---|
210 | ret_st : A; |
---|
211 | ret_acc : list (ident × type); |
---|
212 | ret_fvs : list ident; |
---|
213 | ret_u : universe SymbolTag |
---|
214 | }. |
---|
215 | |
---|
216 | notation > "vbox('do' 〈ident v1, ident v2, ident v3, ident v4〉 ← e; break e')" with precedence 48 |
---|
217 | for @{ match ${e} with |
---|
218 | [ None ⇒ None ? |
---|
219 | | Some ${fresh ret} ⇒ |
---|
220 | (λ${ident v1}.λ${ident v2}.λ${ident v3}.λ${ident v4}. ${e'}) |
---|
221 | (ret_st ? ${fresh ret}) |
---|
222 | (ret_acc ? ${fresh ret}) |
---|
223 | (ret_fvs ? ${fresh ret}) |
---|
224 | (ret_u ? ${fresh ret}) ] }. |
---|
225 | |
---|
226 | notation > "vbox('ret' 〈e1, e2, e3, e4〉)" with precedence 49 |
---|
227 | for @{ Some ? (mk_swret ? ${e1} ${e2} ${e3} ${e4}) }. |
---|
228 | |
---|
229 | (* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list |
---|
230 | of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another |
---|
231 | 'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables |
---|
232 | allows it to proceed without failing. This is all in order to ease the proof of simulation. *) |
---|
233 | let rec switch_removal |
---|
234 | (st : statement) (* the statement in which we will remove switches *) |
---|
235 | (fvs : list ident) (* a finite list of names usable to create variables. *) |
---|
236 | (u : universe SymbolTag) (* a fresh /label/ generator *) |
---|
237 | : option (swret statement) ≝ |
---|
238 | match st with |
---|
239 | [ Sskip ⇒ ret 〈st, [ ], fvs, u〉 |
---|
240 | | Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉 |
---|
241 | | Scall _ _ _ ⇒ ret 〈st, [ ], fvs, u〉 |
---|
242 | | Ssequence s1 s2 ⇒ |
---|
243 | do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u; |
---|
244 | do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u'; |
---|
245 | ret 〈Ssequence s1' s2', acc1 @ acc2, fvs'', u''〉 |
---|
246 | | Sifthenelse e s1 s2 ⇒ |
---|
247 | do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u; |
---|
248 | do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u'; |
---|
249 | ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉 |
---|
250 | | Swhile e body cl ⇒ |
---|
251 | do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u; |
---|
252 | ret 〈Swhile e body' cl, acc, fvs', u'〉 |
---|
253 | | Sdowhile e body ⇒ |
---|
254 | do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u; |
---|
255 | ret 〈Sdowhile e body', acc, fvs', u'〉 |
---|
256 | | Sfor s1 e s2 s3 ⇒ |
---|
257 | do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u; |
---|
258 | do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u'; |
---|
259 | do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u''; |
---|
260 | ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉 |
---|
261 | | Sbreak ⇒ |
---|
262 | ret 〈st, [ ], fvs, u〉 |
---|
263 | | Scontinue ⇒ |
---|
264 | ret 〈st, [ ], fvs, u〉 |
---|
265 | | Sreturn _ ⇒ |
---|
266 | ret 〈st, [ ], fvs, u〉 |
---|
267 | | Sswitch e branches ⇒ |
---|
268 | do 〈sf_branches, acc, fvs', u'〉 ← switch_removal_branches branches fvs u; |
---|
269 | match fvs' with |
---|
270 | [ nil ⇒ None ? |
---|
271 | | cons fresh tl ⇒ |
---|
272 | (* let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in *) |
---|
273 | let ident ≝ Expr (Evar fresh) (typeof e) in |
---|
274 | let assign ≝ Sassign ident e in |
---|
275 | let 〈result, u''〉 ≝ simplify_switch ident sf_branches u' in |
---|
276 | ret 〈Ssequence assign result, (〈fresh, typeof e〉 :: acc), tl, u'〉 |
---|
277 | ] |
---|
278 | | Slabel label body ⇒ |
---|
279 | do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u; |
---|
280 | ret 〈Slabel label body', acc, fvs', u'〉 |
---|
281 | | Sgoto _ ⇒ |
---|
282 | ret 〈st, [ ], fvs, u〉 |
---|
283 | | Scost cost body ⇒ |
---|
284 | do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u; |
---|
285 | ret 〈Scost cost body', acc, fvs', u'〉 |
---|
286 | ] |
---|
287 | |
---|
288 | and switch_removal_branches |
---|
289 | (l : labeled_statements) |
---|
290 | (fvs : list ident) |
---|
291 | (u : universe SymbolTag) |
---|
292 | (* : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝ |
---|
293 | match l with |
---|
294 | [ LSdefault st ⇒ |
---|
295 | do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u; |
---|
296 | ret 〈LSdefault st', acc1, fvs', u'〉 |
---|
297 | | LScase sz int st tl => |
---|
298 | do 〈tl_result, acc1, fvs', u'〉 ← switch_removal_branches tl fvs u; |
---|
299 | do 〈st', acc2, fvs'', u''〉 ← switch_removal st fvs' u'; |
---|
300 | ret 〈LScase sz int st' tl_result, acc1 @ acc2, fvs'', u''〉 |
---|
301 | ]. |
---|
302 | |
---|
303 | let rec mk_fresh_variables |
---|
304 | (st : statement) (* the statement in which we will remove switches *) |
---|
305 | (u : universe SymbolTag) (* a fresh /label/ generator *) |
---|
306 | : (list ident) × (universe SymbolTag) ≝ |
---|
307 | match st with |
---|
308 | [ Sskip ⇒ 〈[ ], u〉 |
---|
309 | | Sassign _ _ ⇒ 〈[ ], u〉 |
---|
310 | | Scall _ _ _ ⇒ 〈[ ], u〉 |
---|
311 | | Ssequence s1 s2 ⇒ |
---|
312 | let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in |
---|
313 | let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in |
---|
314 | 〈fvs @ fvs', u''〉 |
---|
315 | | Sifthenelse e s1 s2 ⇒ |
---|
316 | let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in |
---|
317 | let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in |
---|
318 | 〈fvs @ fvs', u''〉 |
---|
319 | | Swhile e body cl ⇒ |
---|
320 | mk_fresh_variables body u |
---|
321 | | Sdowhile e body ⇒ |
---|
322 | mk_fresh_variables body u |
---|
323 | | Sfor s1 e s2 s3 ⇒ |
---|
324 | let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in |
---|
325 | let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in |
---|
326 | let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in |
---|
327 | 〈fvs @ fvs' @fvs'', u'''〉 |
---|
328 | | Sbreak ⇒ |
---|
329 | 〈[ ], u〉 |
---|
330 | | Scontinue ⇒ |
---|
331 | 〈[ ], u〉 |
---|
332 | | Sreturn _ ⇒ |
---|
333 | 〈[ ], u〉 |
---|
334 | | Sswitch e branches ⇒ |
---|
335 | let 〈ident, u'〉 ≝ fresh ? u in (* This is actually the only point where we need to create a fresh var. *) |
---|
336 | let 〈fvs, u''〉 ≝ mk_fresh_variables_branches branches u' in |
---|
337 | 〈fvs @ [ident], u''〉 (* reversing the order to match a proof invariant *) |
---|
338 | | Slabel label body ⇒ |
---|
339 | mk_fresh_variables body u |
---|
340 | | Sgoto _ ⇒ |
---|
341 | 〈[ ], u〉 |
---|
342 | | Scost cost body ⇒ |
---|
343 | mk_fresh_variables body u |
---|
344 | ] |
---|
345 | |
---|
346 | and mk_fresh_variables_branches |
---|
347 | (l : labeled_statements) |
---|
348 | (u : universe SymbolTag) |
---|
349 | (* : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝ |
---|
350 | match l with |
---|
351 | [ LSdefault st ⇒ |
---|
352 | mk_fresh_variables st u |
---|
353 | | LScase sz int st tl => |
---|
354 | let 〈fvs, u'〉 ≝ mk_fresh_variables_branches tl u in |
---|
355 | let 〈fvs',u''〉 ≝ mk_fresh_variables st u' in |
---|
356 | 〈fvs @ fvs', u''〉 |
---|
357 | ]. |
---|
358 | |
---|
359 | (* Copied this from Csyntax.ma, lifted from Prop to Type |
---|
360 | (I needed to eliminate something proved with this towards Type) *) |
---|
361 | let rec statement_indT |
---|
362 | (P:statement → Type[1]) (Q:labeled_statements → Type[1]) |
---|
363 | (Ssk:P Sskip) |
---|
364 | (Sas:∀e1,e2. P (Sassign e1 e2)) |
---|
365 | (Sca:∀eo,e,args. P (Scall eo e args)) |
---|
366 | (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2)) |
---|
367 | (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2)) |
---|
368 | (Swh:∀e,s,cl. P s → P (Swhile e s cl)) |
---|
369 | (Sdo:∀e,s. P s → P (Sdowhile e s)) |
---|
370 | (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3)) |
---|
371 | (Sbr:P Sbreak) |
---|
372 | (Sco:P Scontinue) |
---|
373 | (Sre:∀eo. P (Sreturn eo)) |
---|
374 | (Ssw:∀e,ls. Q ls → P (Sswitch e ls)) |
---|
375 | (Sla:∀l,s. P s → P (Slabel l s)) |
---|
376 | (Sgo:∀l. P (Sgoto l)) |
---|
377 | (Scs:∀l,s. P s → P (Scost l s)) |
---|
378 | (LSd:∀s. P s → Q (LSdefault s)) |
---|
379 | (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t)) |
---|
380 | (s:statement) on s : P s ≝ |
---|
381 | match s with |
---|
382 | [ Sskip ⇒ Ssk |
---|
383 | | Sassign e1 e2 ⇒ Sas e1 e2 |
---|
384 | | Scall eo e args ⇒ Sca eo e args |
---|
385 | | Ssequence s1 s2 ⇒ Ssq s1 s2 |
---|
386 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) |
---|
387 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) |
---|
388 | | Sifthenelse e s1 s2 ⇒ Sif e s1 s2 |
---|
389 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) |
---|
390 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) |
---|
391 | | Swhile e s cl ⇒ Swh e s cl |
---|
392 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) |
---|
393 | | Sdowhile e s ⇒ Sdo e s |
---|
394 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) |
---|
395 | | Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3 |
---|
396 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) |
---|
397 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) |
---|
398 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3) |
---|
399 | | Sbreak ⇒ Sbr |
---|
400 | | Scontinue ⇒ Sco |
---|
401 | | Sreturn eo ⇒ Sre eo |
---|
402 | | Sswitch e ls ⇒ Ssw e ls |
---|
403 | (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls) |
---|
404 | | Slabel l s ⇒ Sla l s |
---|
405 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) |
---|
406 | | Sgoto l ⇒ Sgo l |
---|
407 | | Scost l s ⇒ Scs l s |
---|
408 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) |
---|
409 | ] |
---|
410 | and labeled_statements_indT |
---|
411 | (P:statement → Type[1]) (Q:labeled_statements → Type[1]) |
---|
412 | (Ssk:P Sskip) |
---|
413 | (Sas:∀e1,e2. P (Sassign e1 e2)) |
---|
414 | (Sca:∀eo,e,args. P (Scall eo e args)) |
---|
415 | (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2)) |
---|
416 | (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2)) |
---|
417 | (Swh:∀e,s,cl. P s → P (Swhile e s cl)) |
---|
418 | (Sdo:∀e,s. P s → P (Sdowhile e s)) |
---|
419 | (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3)) |
---|
420 | (Sbr:P Sbreak) |
---|
421 | (Sco:P Scontinue) |
---|
422 | (Sre:∀eo. P (Sreturn eo)) |
---|
423 | (Ssw:∀e,ls. Q ls → P (Sswitch e ls)) |
---|
424 | (Sla:∀l,s. P s → P (Slabel l s)) |
---|
425 | (Sgo:∀l. P (Sgoto l)) |
---|
426 | (Scs:∀l,s. P s → P (Scost l s)) |
---|
427 | (LSd:∀s. P s → Q (LSdefault s)) |
---|
428 | (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t)) |
---|
429 | (ls:labeled_statements) on ls : Q ls ≝ |
---|
430 | match ls with |
---|
431 | [ LSdefault s ⇒ LSd s |
---|
432 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) |
---|
433 | | LScase sz i s t ⇒ LSc sz i s t |
---|
434 | (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) |
---|
435 | (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t) |
---|
436 | ]. |
---|
437 | |
---|
438 | lemma switch_removal_ok : |
---|
439 | ∀st, u0, u1, post. |
---|
440 | Σresult. |
---|
441 | (switch_removal st ((\fst (mk_fresh_variables st u0)) @ post) u1 = Some ? result) ∧ (ret_fvs ? result = post). |
---|
442 | #st |
---|
443 | @(statement_indT ? (λls. ∀u0, u1, post. |
---|
444 | Σresult. |
---|
445 | (switch_removal_branches ls ((\fst (mk_fresh_variables_branches ls u0)) @ post) u1 = Some ? result) |
---|
446 | ∧ (ret_fvs ? result = post) |
---|
447 | ) … st) |
---|
448 | [ 1: #u0 #u1 #post normalize |
---|
449 | %{(mk_swret statement Sskip [] post u1)} % // |
---|
450 | | 2: #e1 #e2 #u0 #u1 #post normalize |
---|
451 | %{((mk_swret statement (Sassign e1 e2) [] post u1))} % try // |
---|
452 | | 3: #e0 #e #args #u0 #u1 #post normalize |
---|
453 | %{(mk_swret statement (Scall e0 e args) [] post u1)} % try // |
---|
454 | | 4: #s1 #s2 #H1 #H2 #u0 #u1 #post normalize |
---|
455 | elim (H1 u0 u1 ((\fst (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' * |
---|
456 | cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta |
---|
457 | elim (H2 u' (ret_u ? s1') post) #s2' * |
---|
458 | cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta |
---|
459 | #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize |
---|
460 | %{(mk_swret statement (Ssequence (ret_st statement s1') (ret_st statement s2')) |
---|
461 | (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2') |
---|
462 | (ret_u statement s2'))} % try // |
---|
463 | | 5: #e #s1 #s2 #H1 #H2 #u0 #u1 #post normalize |
---|
464 | elim (H1 u0 u1 ((\fst (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' * |
---|
465 | cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta |
---|
466 | elim (H2 u' (ret_u ? s1') post) #s2' * |
---|
467 | cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta |
---|
468 | #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize |
---|
469 | %{((mk_swret statement |
---|
470 | (Sifthenelse e (ret_st statement s1') (ret_st statement s2')) |
---|
471 | (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2') |
---|
472 | (ret_u statement s2')))} % try // |
---|
473 | | 6: #e #s #cl #H #u0 #u1 #post normalize |
---|
474 | elim (H u0 u1 post) #s1' * normalize |
---|
475 | cases (mk_fresh_variables s u0) #fvs #u' |
---|
476 | #Heq1 #Heq1_fvs >Heq1 normalize nodelta |
---|
477 | %{(mk_swret statement (Swhile e (ret_st statement s1') cl) (ret_acc statement s1') |
---|
478 | (ret_fvs statement s1') (ret_u statement s1'))} % try // |
---|
479 | | 7: #e #s #H #u0 #u1 #post normalize |
---|
480 | elim (H u0 u1 post) #s1' * normalize |
---|
481 | cases (mk_fresh_variables s u0) #fvs #u' |
---|
482 | #Heq1 #Heq1_fvs >Heq1 normalize nodelta |
---|
483 | %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1') |
---|
484 | (ret_fvs statement s1') (ret_u statement s1'))} % try // |
---|
485 | | 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize |
---|
486 | elim (H1 u0 u1 |
---|
487 | (\fst (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0))) @ |
---|
488 | (\fst (mk_fresh_variables s3 (\snd (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @ |
---|
489 | post)) #s1' * |
---|
490 | cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta |
---|
491 | elim (H2 u' (ret_u ? s1') ((\fst (mk_fresh_variables s3 (\snd (mk_fresh_variables s2 u')))) @ |
---|
492 | post)) #s2' * |
---|
493 | cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta |
---|
494 | elim (H3 u'' (ret_u ? s2') post) #s3' * |
---|
495 | cases (mk_fresh_variables s3 u'') #fvs'' #u''' normalize nodelta |
---|
496 | #Heq3 #Heq3_fvs #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs |
---|
497 | >associative_append >associative_append >Heq1 normalize >Heq1_fvs |
---|
498 | >Heq2 normalize >Heq2_fvs >Heq3 normalize |
---|
499 | %{(mk_swret statement |
---|
500 | (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3')) |
---|
501 | (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3') |
---|
502 | (ret_fvs statement s3') (ret_u statement s3'))} % try // |
---|
503 | | 9: #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % // |
---|
504 | | 10: #u0 #u1 #post normalize %{(mk_swret statement Scontinue [] post u1)} % // |
---|
505 | | 11: #e #u0 #u1 #post normalize %{(mk_swret statement (Sreturn e) [] post u1)} % // |
---|
506 | | 12: #e #ls #H #u0 #u1 #post |
---|
507 | whd in match (mk_fresh_variables ??); |
---|
508 | whd in match (switch_removal ???); |
---|
509 | elim (fresh ? u0) #fresh #u' |
---|
510 | elim (H u' u1 ([fresh] @ post)) #ls' * normalize nodelta |
---|
511 | cases (mk_fresh_variables_branches ls u') #fvs #u'' normalize nodelta |
---|
512 | >associative_append #Heq #Heq_fvs >Heq normalize nodelta |
---|
513 | >Heq_fvs normalize nodelta |
---|
514 | cases (simplify_switch ???) #st' #u''' normalize nodelta |
---|
515 | %{((mk_swret statement |
---|
516 | (Ssequence (Sassign (Expr (Evar fresh) (typeof e)) e) st') |
---|
517 | (〈fresh,typeof e〉::ret_acc labeled_statements ls') ([]@post) |
---|
518 | (ret_u labeled_statements ls')))} % // |
---|
519 | | 13: #l #s #H #u0 #u1 #post normalize |
---|
520 | elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs |
---|
521 | %{(mk_swret statement (Slabel l (ret_st statement s')) (ret_acc statement s') |
---|
522 | post (ret_u statement s'))} % // |
---|
523 | | 14: #l #u0 #u1 #post normalize %{((mk_swret statement (Sgoto l) [] post u1))} % // |
---|
524 | | 15: #l #s #H #u0 #u1 #post normalize |
---|
525 | elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs |
---|
526 | %{(mk_swret statement (Scost l (ret_st statement s')) (ret_acc statement s') |
---|
527 | post (ret_u statement s'))} % // |
---|
528 | | 16: #s #H #u0 #u1 #post normalize |
---|
529 | elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs |
---|
530 | %{(mk_swret labeled_statements (LSdefault (ret_st statement s')) |
---|
531 | (ret_acc statement s') post (ret_u statement s'))} % // |
---|
532 | | 17: #sz #i #hd #tl #H1 #H2 #u0 #u1 #post normalize |
---|
533 | elim (H2 u0 u1 (\fst (mk_fresh_variables hd (\snd (mk_fresh_variables_branches tl u0))) @ post)) #ls' * |
---|
534 | cases (mk_fresh_variables_branches tl u0) #fvs #u' normalize |
---|
535 | elim (H1 u' (ret_u labeled_statements ls') post) #s1' * |
---|
536 | cases (mk_fresh_variables hd u') #fvs' #u' normalize #Heq #Heq_fvs #Heql #Heql_fvs |
---|
537 | >associative_append >Heql normalize >Heql_fvs >Heq normalize |
---|
538 | %{(mk_swret labeled_statements |
---|
539 | (LScase sz i (ret_st statement s1') (ret_st labeled_statements ls')) |
---|
540 | (ret_acc labeled_statements ls'@ret_acc statement s1') |
---|
541 | (ret_fvs statement s1') (ret_u statement s1'))} % // |
---|
542 | ] qed. |
---|
543 | |
---|
544 | axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *) |
---|
545 | |
---|
546 | (* Proof that switch_removal_switch_free does its job. *) |
---|
547 | lemma switch_removal_switch_free : ∀st,fvs,u,result. switch_removal st fvs u = Some ? result → switch_free (ret_st ? result). |
---|
548 | #st @(statement_ind2 ? (λls. ∀fvs,u,ls_result. switch_removal_branches ls fvs u = Some ? ls_result → |
---|
549 | branches_switch_free (ret_st ? ls_result)) … st) |
---|
550 | [ 1: #fvs #u #result normalize #Heq destruct (Heq) // |
---|
551 | | 2: #e1 #e2 #fvs #u #result normalize #Heq destruct (Heq) // |
---|
552 | | 3: #e0 #e #args #fvs #u #result normalize #Heq destruct (Heq) // |
---|
553 | | 4: #s1 #s2 #H1 #H2 #fvs #u #result normalize lapply (H1 fvs u) |
---|
554 | elim (switch_removal s1 fvs u) normalize |
---|
555 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
556 | | 2: #res1 #Heq1 lapply (H2 (ret_fvs statement res1) (ret_u statement res1)) |
---|
557 | elim (switch_removal s2 (ret_fvs statement res1) (ret_u statement res1)) |
---|
558 | [ 1: normalize #_ #Habsurd destruct (Habsurd) |
---|
559 | | 2: normalize #res2 #Heq2 #Heq destruct (Heq) |
---|
560 | normalize @conj |
---|
561 | [ 1: @Heq1 // | 2: @Heq2 // ] |
---|
562 | ] ] |
---|
563 | | *: |
---|
564 | (* TODO the first few cases show that the lemma is routinely proved. TBF later. *) |
---|
565 | @cthulhu ] |
---|
566 | qed. |
---|
567 | |
---|
568 | (* ----------------------------------------------------------------------------- |
---|
569 | Switch-removal code for programs. |
---|
570 | ----------------------------------------------------------------------------*) |
---|
571 | |
---|
572 | (* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to |
---|
573 | * name clashes for labels. We have no choice but to actually run through the function and to |
---|
574 | * compute the maximum of labels+identifiers. This way we can generate both fresh variables and |
---|
575 | * fresh labels using the same univ. While we're at it we also consider record fields. |
---|
576 | * Cost labels are not considered, though. They already live in a separate universe. |
---|
577 | * |
---|
578 | * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes, |
---|
579 | * but in the end it might be good to move the following functions into fresh.ma. |
---|
580 | *) |
---|
581 | |
---|
582 | (* Least element in the total order of identifiers. *) |
---|
583 | definition least_identifier ≝ an_identifier SymbolTag one. |
---|
584 | |
---|
585 | (* This is certainly overkill: variables adressed in an expression should be declared in the |
---|
586 | * enclosing function's prototype. *) |
---|
587 | let rec max_of_expr (e : expr) : ident ≝ |
---|
588 | match e with |
---|
589 | [ Expr ed _ ⇒ |
---|
590 | match ed with |
---|
591 | [ Econst_int _ _ ⇒ least_identifier |
---|
592 | | Econst_float _ ⇒ least_identifier |
---|
593 | | Evar id ⇒ id |
---|
594 | | Ederef e1 ⇒ max_of_expr e1 |
---|
595 | | Eaddrof e1 ⇒ max_of_expr e1 |
---|
596 | | Eunop _ e1 ⇒ max_of_expr e1 |
---|
597 | | Ebinop _ e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) |
---|
598 | | Ecast _ e1 ⇒ max_of_expr e1 |
---|
599 | | Econdition e1 e2 e3 ⇒ |
---|
600 | max_id (max_of_expr e1) (max_id (max_of_expr e2) (max_of_expr e3)) |
---|
601 | | Eandbool e1 e2 ⇒ |
---|
602 | max_id (max_of_expr e1) (max_of_expr e2) |
---|
603 | | Eorbool e1 e2 ⇒ |
---|
604 | max_id (max_of_expr e1) (max_of_expr e2) |
---|
605 | | Esizeof _ ⇒ least_identifier |
---|
606 | | Efield r f ⇒ max_id f (max_of_expr r) |
---|
607 | | Ecost _ e1 ⇒ max_of_expr e1 |
---|
608 | ] |
---|
609 | ]. |
---|
610 | |
---|
611 | (* Reasoning about this promises to be a serious pain. Especially the Scall case. *) |
---|
612 | let rec max_of_statement (s : statement) : ident ≝ |
---|
613 | match s with |
---|
614 | [ Sskip ⇒ least_identifier |
---|
615 | | Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) |
---|
616 | | Scall r f args ⇒ |
---|
617 | let retmax ≝ |
---|
618 | match r with |
---|
619 | [ None ⇒ least_identifier |
---|
620 | | Some e ⇒ max_of_expr e ] |
---|
621 | in |
---|
622 | max_id (max_of_expr f) |
---|
623 | (max_id retmax |
---|
624 | (foldl ?? (λacc,elt. max_id (max_of_expr elt) acc) least_identifier args) ) |
---|
625 | | Ssequence s1 s2 ⇒ |
---|
626 | max_id (max_of_statement s1) (max_of_statement s2) |
---|
627 | | Sifthenelse e s1 s2 ⇒ |
---|
628 | max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2)) |
---|
629 | | Swhile e body _ ⇒ |
---|
630 | max_id (max_of_expr e) (max_of_statement body) |
---|
631 | | Sdowhile e body ⇒ |
---|
632 | max_id (max_of_expr e) (max_of_statement body) |
---|
633 | | Sfor init test incr body ⇒ |
---|
634 | max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body)) |
---|
635 | | Sbreak ⇒ least_identifier |
---|
636 | | Scontinue ⇒ least_identifier |
---|
637 | | Sreturn opt ⇒ |
---|
638 | match opt with |
---|
639 | [ None ⇒ least_identifier |
---|
640 | | Some e ⇒ max_of_expr e |
---|
641 | ] |
---|
642 | | Sswitch e ls ⇒ |
---|
643 | max_id (max_of_expr e) (max_of_ls ls) |
---|
644 | | Slabel lab body ⇒ |
---|
645 | max_id lab (max_of_statement body) |
---|
646 | | Sgoto lab ⇒ |
---|
647 | lab |
---|
648 | | Scost _ body ⇒ |
---|
649 | max_of_statement body |
---|
650 | ] |
---|
651 | and max_of_ls (ls : labeled_statements) : ident ≝ |
---|
652 | match ls with |
---|
653 | [ LSdefault s ⇒ max_of_statement s |
---|
654 | | LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s) |
---|
655 | ]. |
---|
656 | |
---|
657 | definition max_id_of_function : function → ident ≝ |
---|
658 | λf. max_id (max_of_statement (fn_body f)) (max_id_of_fn f). |
---|
659 | |
---|
660 | (* We compute fresh universes on a function-by function basis, since there can't |
---|
661 | * be cross-functions gotos or stuff like that. *) |
---|
662 | definition function_switch_removal : function → function × (list (ident × type)) ≝ |
---|
663 | λf. |
---|
664 | (λres_record. |
---|
665 | let new_vars ≝ ret_acc ? res_record in |
---|
666 | let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (ret_st ? res_record) in |
---|
667 | 〈result, new_vars〉) |
---|
668 | (let u ≝ universe_of_max (max_id_of_function f) in |
---|
669 | let 〈fvs,u'〉 as Hfv ≝ mk_fresh_variables (fn_body f) u in |
---|
670 | match switch_removal (fn_body f) fvs u' return λx. (switch_removal (fn_body f) fvs u' = x) → ? with |
---|
671 | [ None ⇒ λHsr. ? |
---|
672 | | Some res_record ⇒ λ_. res_record |
---|
673 | ] (refl ? (switch_removal (fn_body f) fvs u'))). |
---|
674 | lapply (switch_removal_ok (fn_body f) u u' [ ]) * #result' * #Heq #Hret_eq |
---|
675 | <Hfv in Heq; >append_nil >Hsr #Habsurd destruct (Habsurd) |
---|
676 | qed. |
---|
677 | |
---|
678 | let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝ |
---|
679 | match f with |
---|
680 | [ CL_Internal f ⇒ |
---|
681 | CL_Internal (\fst (function_switch_removal f)) |
---|
682 | | CL_External _ _ _ ⇒ |
---|
683 | f |
---|
684 | ]. |
---|
685 | |
---|
686 | let rec program_switch_removal (p : clight_program) : clight_program ≝ |
---|
687 | let prog_funcs ≝ prog_funct ?? p in |
---|
688 | let sf_funcs ≝ map ?? (λcl_fundef. |
---|
689 | let 〈fun_id, fun_def〉 ≝ cl_fundef in |
---|
690 | 〈fun_id, fundef_switch_removal fun_def〉 |
---|
691 | ) prog_funcs in |
---|
692 | mk_program ?? |
---|
693 | (prog_vars … p) |
---|
694 | sf_funcs |
---|
695 | (prog_main … p). |
---|
696 | |
---|
697 | |
---|
698 | (* ----------------------------------------------------------------------------- |
---|
699 | Applying two relations on all substatements and all subexprs (directly under). |
---|
700 | ---------------------------------------------------------------------------- *) |
---|
701 | |
---|
702 | let rec substatement_P (s1 : statement) (P : statement → Prop) (Q : expr → Prop) : Prop ≝ |
---|
703 | match s1 with |
---|
704 | [ Sskip ⇒ True |
---|
705 | | Sassign e1 e2 ⇒ Q e1 ∧ Q e2 |
---|
706 | | Scall r f args ⇒ |
---|
707 | match r with |
---|
708 | [ None ⇒ Q f ∧ (All … Q args) |
---|
709 | | Some r ⇒ Q r ∧ Q f ∧ (All … Q args) |
---|
710 | ] |
---|
711 | | Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2 |
---|
712 | | Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2 |
---|
713 | | Swhile e sub _ ⇒ Q e ∧ P sub |
---|
714 | | Sdowhile e sub ⇒ Q e ∧ P sub |
---|
715 | | Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3 |
---|
716 | | Sbreak ⇒ True |
---|
717 | | Scontinue ⇒ True |
---|
718 | | Sreturn r ⇒ |
---|
719 | match r with |
---|
720 | [ None ⇒ True |
---|
721 | | Some r ⇒ Q r ] |
---|
722 | | Sswitch e ls ⇒ Q e ∧ (substatement_ls ls P) |
---|
723 | | Slabel _ sub ⇒ P sub |
---|
724 | | Sgoto _ ⇒ True |
---|
725 | | Scost _ sub ⇒ P sub |
---|
726 | ] |
---|
727 | and substatement_ls ls (P : statement → Prop) : Prop ≝ |
---|
728 | match ls with |
---|
729 | [ LSdefault sub ⇒ P sub |
---|
730 | | LScase _ _ sub tl ⇒ P sub ∧ (substatement_ls tl P) |
---|
731 | ]. |
---|
732 | |
---|
733 | (* ----------------------------------------------------------------------------- |
---|
734 | Freshness conservation results on switch removal. |
---|
735 | ---------------------------------------------------------------------------- *) |
---|
736 | |
---|
737 | (* Similar stuff in toCminor.ma. *) |
---|
738 | lemma fresh_for_univ_still_fresh : |
---|
739 | ∀u,i. fresh_for_univ SymbolTag i u → ∀v,u'. 〈v, u'〉 = fresh ? u → fresh_for_univ ? i u'. |
---|
740 | * #p * #i #H1 #v * #p' lapply H1 normalize |
---|
741 | #H1 #H2 destruct (H2) /2/ qed. |
---|
742 | |
---|
743 | lemma fresh_eq : ∀u,i. fresh_for_univ SymbolTag i u → ∃fv,u'. fresh ? u = 〈fv, u'〉 ∧ fresh_for_univ ? i u'. |
---|
744 | #u #i #Hfresh lapply (fresh_for_univ_still_fresh … Hfresh) |
---|
745 | cases (fresh SymbolTag u) |
---|
746 | #fv #u' #H %{fv} %{u'} @conj try // @H // |
---|
747 | qed. |
---|
748 | |
---|
749 | lemma produce_cond_fresh : ∀e,exit,ls,u,i. fresh_for_univ ? i u → fresh_for_univ ? i (\snd (produce_cond e ls u exit)). |
---|
750 | #e #exit #ls @(branches_ind … ls) |
---|
751 | [ 1: #st #u #i #Hfresh normalize |
---|
752 | lapply (fresh_for_univ_still_fresh … Hfresh) |
---|
753 | cases (fresh ? u) #lab #u1 #H lapply (H lab u1 (refl ??)) normalize // |
---|
754 | | 2: #sz #i #hd #tl #Hind #u #i' #Hfresh normalize |
---|
755 | lapply (Hind u i' Hfresh) elim (produce_cond e tl u exit) * |
---|
756 | #subcond #sublabel #u1 #Hfresh1 normalize |
---|
757 | lapply (fresh_for_univ_still_fresh … Hfresh1) |
---|
758 | cases (fresh ? u1) #lab #u2 #H2 lapply (H2 lab u2 (refl ??)) normalize // |
---|
759 | ] qed. |
---|
760 | |
---|
761 | lemma simplify_switch_fresh : ∀u,i,e,ls. |
---|
762 | fresh_for_univ ? i u → |
---|
763 | fresh_for_univ ? i (\snd (simplify_switch e ls u)). |
---|
764 | #u #i #e #ls #Hfresh |
---|
765 | normalize |
---|
766 | lapply (fresh_for_univ_still_fresh … Hfresh) |
---|
767 | cases (fresh ? u) |
---|
768 | #exit_label #uv1 #Haux lapply (Haux exit_label uv1 (refl ??)) -Haux #Haux |
---|
769 | normalize lapply (produce_cond_fresh e exit_label ls … Haux) |
---|
770 | elim (produce_cond ????) * #stm #label #uv2 normalize nodelta // |
---|
771 | qed. |
---|
772 | |
---|
773 | (* ----------------------------------------------------------------------------- |
---|
774 | Simulation proof and related voodoo. |
---|
775 | ----------------------------------------------------------------------------*) |
---|
776 | |
---|
777 | definition expr_lvalue_ind_combined ≝ |
---|
778 | λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. |
---|
779 | conj ?? |
---|
780 | (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx) |
---|
781 | (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx). |
---|
782 | |
---|
783 | let rec expr_ind2 |
---|
784 | (P : expr → Prop) (Q : expr_descr → type → Prop) |
---|
785 | (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) |
---|
786 | (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) |
---|
787 | (Iconst_float : ∀f, t. Q (Econst_float f) t) |
---|
788 | (Ivar : ∀id, t. Q (Evar id) t) |
---|
789 | (Ideref : ∀e, t. P e → Q (Ederef e) t) |
---|
790 | (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) |
---|
791 | (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) |
---|
792 | (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) |
---|
793 | (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) |
---|
794 | (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) |
---|
795 | (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) |
---|
796 | (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) |
---|
797 | (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) |
---|
798 | (Ifield : ∀e,f,t. P e → Q (Efield e f) t) |
---|
799 | (Icost : ∀c,e,t. P e → Q (Ecost c e) t) |
---|
800 | (e : expr) on e : P e ≝ |
---|
801 | match e with |
---|
802 | [ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ] |
---|
803 | |
---|
804 | and expr_desc_ind2 |
---|
805 | (P : expr → Prop) (Q : expr_descr → type → Prop) |
---|
806 | (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) |
---|
807 | (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) |
---|
808 | (Iconst_float : ∀f, t. Q (Econst_float f) t) |
---|
809 | (Ivar : ∀id, t. Q (Evar id) t) |
---|
810 | (Ideref : ∀e, t. P e → Q (Ederef e) t) |
---|
811 | (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) |
---|
812 | (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) |
---|
813 | (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) |
---|
814 | (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) |
---|
815 | (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) |
---|
816 | (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) |
---|
817 | (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) |
---|
818 | (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) |
---|
819 | (Ifield : ∀e,f,t. P e → Q (Efield e f) t) |
---|
820 | (Icost : ∀c,e,t. P e → Q (Ecost c e) t) |
---|
821 | (ed : expr_descr) (t : type) on ed : Q ed t ≝ |
---|
822 | match ed with |
---|
823 | [ Econst_int sz i ⇒ Iconst_int sz i t |
---|
824 | | Econst_float f ⇒ Iconst_float f t |
---|
825 | | Evar id ⇒ Ivar id t |
---|
826 | | Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
827 | | Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
828 | | Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
829 | | Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) |
---|
830 | | Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
831 | | Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e3) |
---|
832 | | Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) |
---|
833 | | Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) |
---|
834 | | Esizeof sizeoft ⇒ Isizeof sizeoft t |
---|
835 | | Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
836 | | Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
837 | ]. |
---|
838 | |
---|
839 | (* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched |
---|
840 | by a non-constant number of evaluations in the converted program. More precisely, |
---|
841 | [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps |
---|
842 | necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *) |
---|
843 | |
---|
844 | (* A version of simplify_switch hiding the ugly projs *) |
---|
845 | definition fresh_for_expression ≝ |
---|
846 | λe,u. fresh_for_univ SymbolTag (max_of_expr e) u. |
---|
847 | |
---|
848 | definition fresh_for_statement ≝ |
---|
849 | λs,u. fresh_for_univ SymbolTag (max_of_statement s) u. |
---|
850 | |
---|
851 | (* needed during mutual induction ... *) |
---|
852 | definition fresh_for_labeled_statements ≝ |
---|
853 | λls,u. fresh_for_univ ? (max_of_ls ls) u. |
---|
854 | |
---|
855 | definition fresh_for_function ≝ |
---|
856 | λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u. |
---|
857 | |
---|
858 | (* misc properties of the max function on positives. *) |
---|
859 | |
---|
860 | lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v. |
---|
861 | * #p whd in ⊢ (??%?); >max_one_neutral // qed. |
---|
862 | |
---|
863 | lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1. |
---|
864 | * #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%); |
---|
865 | >commutative_max // qed. |
---|
866 | |
---|
867 | lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3). |
---|
868 | * #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max // |
---|
869 | qed. |
---|
870 | |
---|
871 | lemma fresh_max_split : ∀a,b,u. fresh_for_univ SymbolTag (max_id a b) u → fresh_for_univ ? a u ∧ fresh_for_univ ? b u. |
---|
872 | * #a * #b * #u normalize |
---|
873 | lapply (pos_compare_to_Prop a b) |
---|
874 | cases (pos_compare a b) whd in ⊢ (% → ?); #Hab |
---|
875 | [ 1: >(le_to_leb_true a b) try /2/ #Hbu @conj /2/ |
---|
876 | | 2: destruct >reflexive_leb /2/ |
---|
877 | | 3: >(not_le_to_leb_false a b) try /2/ #Hau @conj /2/ |
---|
878 | ] qed. |
---|
879 | |
---|
880 | (* Auxilliary commutation lemma used in [substatement_fresh]. *) |
---|
881 | |
---|
882 | lemma foldl_max : ∀l,a,b. |
---|
883 | foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l = |
---|
884 | max_id a (foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) b l). |
---|
885 | #l elim l |
---|
886 | [ 1: * #a * #b whd in match (foldl ?????) in ⊢ (??%%); @refl |
---|
887 | | 2: #hd #tl #Hind #a #b whd in match (foldl ?????) in ⊢ (??%%); |
---|
888 | <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl |
---|
889 | ] qed. |
---|
890 | |
---|
891 | (* Lookup functions in list environments (used to type local variables in functions) *) |
---|
892 | let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝ |
---|
893 | match l with |
---|
894 | [ nil ⇒ false |
---|
895 | | cons hd tl ⇒ |
---|
896 | let 〈id, ty〉 ≝ hd in |
---|
897 | match identifier_eq SymbolTag i id with |
---|
898 | [ inl Hid_eq ⇒ true |
---|
899 | | inr Hid_neq ⇒ mem_assoc_env i tl |
---|
900 | ] |
---|
901 | ]. |
---|
902 | |
---|
903 | let rec assoc_env (i : ident) (l : list (ident×type)) on l : option type ≝ |
---|
904 | match l with |
---|
905 | [ nil ⇒ None ? |
---|
906 | | cons hd tl ⇒ |
---|
907 | let 〈id, ty〉 ≝ hd in |
---|
908 | match identifier_eq SymbolTag i id with |
---|
909 | [ inl Hid_eq ⇒ Some ? ty |
---|
910 | | inr Hid_neq ⇒ assoc_env i tl |
---|
911 | ] |
---|
912 | ]. |
---|
913 | |
---|
914 | (* --------------------------------------------------------------------------- *) |
---|
915 | (* Memory extensions (limited form on memoryInjection.ma). Note that we state the |
---|
916 | properties at the back-end level. *) |
---|
917 | (* --------------------------------------------------------------------------- *) |
---|
918 | |
---|
919 | (* |
---|
920 | definition block_DeqSet : DeqSet ≝ mk_DeqSet block eq_blockb ?. |
---|
921 | * #r1 #id1 * #r2 #id2 @(eqZb_elim … id1 id2) |
---|
922 | [ 1: #Heq >Heq cases r1 cases r2 normalize |
---|
923 | >eqZb_reflexive normalize @conj #H destruct (H) |
---|
924 | try @refl |
---|
925 | | 2: #Hneq cases r1 cases r2 normalize |
---|
926 | >(eqZb_false … Hneq) normalize @conj |
---|
927 | #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??))) |
---|
928 | ] qed. *) |
---|
929 | |
---|
930 | (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the back-end values are equal. *) |
---|
931 | definition load_sim ≝ |
---|
932 | λ(m1 : mem).λ(m2 : mem). |
---|
933 | ∀ptr,bev. |
---|
934 | beloadv m1 ptr = Some ? bev → |
---|
935 | beloadv m2 ptr = Some ? bev. |
---|
936 | |
---|
937 | (* The [valid_pointer] property is too weak to be preserved by [free]. We use the following guard. *) |
---|
938 | (* definition freed_pointer ≝ λ(m : mem).λ(p : pointer). |
---|
939 | low_bound m (pblock p) = OZ ∧ |
---|
940 | high_bound m (pblock p) = OZ. *) |
---|
941 | |
---|
942 | (* definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res. *) |
---|
943 | |
---|
944 | definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res. |
---|
945 | |
---|
946 | definition outbound_pointer ≝ λm,p. |
---|
947 | Zltb (block_id (pblock p)) (nextblock m) = true ∧ |
---|
948 | Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))) = true ∧ |
---|
949 | high_bound m (pblock p) = Z_of_unsigned_bitvector … (offv (poff p)). |
---|
950 | |
---|
951 | lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p ∨ outbound_pointer m p. |
---|
952 | #m #p @conj |
---|
953 | [ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??); |
---|
954 | whd in match (outbound_pointer ??); |
---|
955 | whd in match (do_if_in_bounds); normalize nodelta |
---|
956 | cases (Zltb (block_id (pblock p)) (nextblock m)) |
---|
957 | [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
958 | >andb_lsimpl_true normalize nodelta |
---|
959 | cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) |
---|
960 | [ 2: normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
961 | >andb_lsimpl_true normalize nodelta |
---|
962 | lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p))) |
---|
963 | elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p))) |
---|
964 | [ 1: #H >H #_ normalize nodelta #_ %1 #A #f /2 by ex_intro/ |
---|
965 | | 2: * #_ #H1 #_ #H2 >(Zleb_true_to_Zleb_true_to_eq … H1 H2) %2 @conj try @conj @refl ] |
---|
966 | | 2: whd in match (valid_pointer ??); * |
---|
967 | [ 1: whd in match (in_bounds_pointer ??); #H |
---|
968 | lapply (H bool (λblock,contents,off. true)) |
---|
969 | * #foo whd in match (do_if_in_bounds ????); |
---|
970 | cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta |
---|
971 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
972 | >andb_lsimpl_true |
---|
973 | cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) |
---|
974 | normalize nodelta |
---|
975 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
976 | >andb_lsimpl_true |
---|
977 | elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p)))) |
---|
978 | [ 1: #H >(Zltb_to_Zleb_true … H) #_ @refl |
---|
979 | | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
980 | | 2: whd in match (outbound_pointer ??); * * #Hlt #Hleb >Hlt >Hleb |
---|
981 | #Hhigh >Hhigh >andb_lsimpl_true |
---|
982 | lapply (reflexive_Zle … (Z_of_unsigned_bitvector offset_size (offv (poff p)))) |
---|
983 | #Hle >(Zle_to_Zleb_true … Hle) @refl |
---|
984 | ] |
---|
985 | ] qed. |
---|
986 | |
---|
987 | (* |
---|
988 | lemma freed_pointer_dec : ∀m,p. freed_pointer m p ∨ (¬freed_pointer m p). |
---|
989 | #m #p |
---|
990 | whd in match (freed_pointer ??); |
---|
991 | cases (low_bound m (pblock p)) |
---|
992 | [ 2,3: #low %2 % * #H destruct (H) ] |
---|
993 | cases (high_bound m (pblock p)) |
---|
994 | [ 1: %1 @conj @refl | 2,3: #low %2 % * #_ #H destruct (H) ] |
---|
995 | qed. *) |
---|
996 | |
---|
997 | (* In the limited setting of switch removal, a memory extension is a list of fresh blocks |
---|
998 | * to which we can write. *) |
---|
999 | record sr_memext (m1 : mem) (m2 : mem) : Type[0] ≝ |
---|
1000 | { me_inj : load_sim m1 m2; |
---|
1001 | (* A list of blocks where we can write freely *) |
---|
1002 | me_writeable : list block; |
---|
1003 | (* These blocks are valid *) |
---|
1004 | me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b; |
---|
1005 | (* And pointers to m1 are oblivious to these blocks *) |
---|
1006 | me_writeable_ok : ∀p.valid_pointer m1 p = true → |
---|
1007 | ¬ (meml ? (pblock p) me_writeable); |
---|
1008 | (* Valid pointers are still valid in m2. One could think that this is superfluous as |
---|
1009 | being implied by me_inj, and it is but for a small detail: valid_pointer allows a pointer |
---|
1010 | to be one off the end of a block bound. The internal check in beloadv does not. |
---|
1011 | valid_pointer should be understood as "pointer making sense" rather than "pointer from |
---|
1012 | which you can load stuff". [mi_valid_pointers] is used for instance when proving the |
---|
1013 | semantics preservation for equality testing (where we check that the pointers we |
---|
1014 | compare are valid before being equal). |
---|
1015 | *) |
---|
1016 | me_valid_pointers : ∀p. (* ¬ (freed_pointer m1 p) → *) |
---|
1017 | valid_pointer m1 p = true → |
---|
1018 | valid_pointer m2 p = true |
---|
1019 | }. |
---|
1020 | |
---|
1021 | (* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension |
---|
1022 | of the environment [e1] s.t. the new binders are in [new], and such that those |
---|
1023 | new binders are "writeable" in the memory extension [Hext] *) |
---|
1024 | definition disjoint_extension ≝ |
---|
1025 | λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem). |
---|
1026 | λ(new : list (ident × type)). λ(Hext: sr_memext m1 m2). |
---|
1027 | ∀id. match mem_assoc_env id new with |
---|
1028 | [ true ⇒ |
---|
1029 | ∃b. lookup ?? e2 id = Some ? b |
---|
1030 | ∧ meml ? b (me_writeable … Hext) |
---|
1031 | ∧ lookup ?? e1 id = None ? |
---|
1032 | | false ⇒ lookup ?? e1 id = lookup ?? e2 id |
---|
1033 | ]. |
---|
1034 | |
---|
1035 | (* Lift load_sim to loadn. *) |
---|
1036 | lemma load_sim_loadn : |
---|
1037 | ∀m1,m2. load_sim m1 m2 → |
---|
1038 | ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res. |
---|
1039 | #m1 #m2 #Hload_sim #sz |
---|
1040 | elim sz |
---|
1041 | [ 1: #p #res #H @H |
---|
1042 | | 2: #n' #Hind #p #res |
---|
1043 | whd in match (loadn ???); |
---|
1044 | whd in match (loadn m2 ??); |
---|
1045 | lapply (Hload_sim p) |
---|
1046 | cases (beloadv m1 p) normalize nodelta |
---|
1047 | [ 1: #_ #Habsurd destruct (Habsurd) ] |
---|
1048 | #bval #H >(H ? (refl ??)) normalize nodelta |
---|
1049 | lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1))) |
---|
1050 | cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n') |
---|
1051 | normalize nodelta |
---|
1052 | [ 1: #_ #Habsurd destruct (Habsurd) ] |
---|
1053 | #res' #H >(H ? (refl ??)) normalize |
---|
1054 | #H @H |
---|
1055 | ] qed. |
---|
1056 | |
---|
1057 | (* Lift load_sim to front-end values. *) |
---|
1058 | lemma load_sim_fe : |
---|
1059 | ∀m1,m2. load_sim m1 m2 → |
---|
1060 | ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v → |
---|
1061 | load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v. |
---|
1062 | #m1 #m2 #Hloadsim #ptr #ty #v |
---|
1063 | cases ty |
---|
1064 | [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty |
---|
1065 | | 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ] |
---|
1066 | whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?)); |
---|
1067 | [ 1,7,8: #Habsurd destruct (Habsurd) |
---|
1068 | | 5,6: #H @H |
---|
1069 | | 2,3,4,9: |
---|
1070 | generalize in match (mk_pointer (pblock ptr) (poff ptr)); |
---|
1071 | elim (typesize ?) |
---|
1072 | [ 1,3,5,7: #p #H @H |
---|
1073 | | 2,4,6,8: #n' #Hind #p |
---|
1074 | lapply (load_sim_loadn … Hloadsim (S n') p) |
---|
1075 | cases (loadn m1 p (S n')) normalize nodelta |
---|
1076 | [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ] |
---|
1077 | #bv #H >(H ? (refl ??)) #H @H |
---|
1078 | ] |
---|
1079 | ] qed. |
---|
1080 | |
---|
1081 | (* Lemmas relating memory extensions to [free] *) |
---|
1082 | |
---|
1083 | (* Successful beloadv implies valid_pointer. The converse is *NOT* true. *) |
---|
1084 | lemma beloadv_to_valid_pointer : ∀m,ptr,res. beloadv m ptr = Some ? res → valid_pointer m ptr = true. |
---|
1085 | * #contents #next #nextpos #ptr #res |
---|
1086 | whd in match (beloadv ??); |
---|
1087 | whd in match (valid_pointer ??); |
---|
1088 | cases (Zltb (block_id (pblock ptr)) next) |
---|
1089 | normalize nodelta |
---|
1090 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
1091 | >andb_lsimpl_true |
---|
1092 | whd in match (low_bound ??); |
---|
1093 | whd in match (high_bound ??); |
---|
1094 | cases (Zleb (low (contents (pblock ptr))) |
---|
1095 | (Z_of_unsigned_bitvector offset_size (offv (poff ptr)))) |
---|
1096 | [ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ] |
---|
1097 | >andb_lsimpl_true |
---|
1098 | normalize nodelta #H |
---|
1099 | @Zltb_to_Zleb_true |
---|
1100 | cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H; |
---|
1101 | try // normalize #Habsurd destruct (Habsurd) qed. |
---|
1102 | |
---|
1103 | lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1). |
---|
1104 | * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize |
---|
1105 | @(eqZb_elim … bid1 bid2) |
---|
1106 | [ 1: #Heq >Heq cases br1 cases br2 normalize |
---|
1107 | [ 1,4: * #H @(False_ind … (H (refl ??))) ] |
---|
1108 | #_ @refl |
---|
1109 | | 2: cases br1 cases br2 normalize #_ #_ @refl ] |
---|
1110 | qed. |
---|
1111 | |
---|
1112 | lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1). |
---|
1113 | * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize |
---|
1114 | @(eqZb_elim … bid1 bid2) |
---|
1115 | [ 1: #Heq >Heq cases br1 cases br2 normalize |
---|
1116 | [ 1,4: * #H @(False_ind … (H (refl ??))) ] |
---|
1117 | #_ @refl |
---|
1118 | | 2: cases br1 cases br2 normalize #_ #_ @refl ] |
---|
1119 | qed. |
---|
1120 | |
---|
1121 | lemma beloadv_free_blocks_neq : |
---|
1122 | ∀m,block,pblock,poff,res. |
---|
1123 | beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block. |
---|
1124 | * #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res |
---|
1125 | normalize |
---|
1126 | cases (Zltb pbid next) normalize nodelta |
---|
1127 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
1128 | cases pbr cases br normalize nodelta |
---|
1129 | [ 2,3: #_ % #Habsurd destruct (Habsurd) ] |
---|
1130 | @(eqZb_elim pbid bid) normalize nodelta |
---|
1131 | #Heq destruct (Heq) |
---|
1132 | [ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
1133 | #_ % #H destruct (H) elim Heq #H @H @refl |
---|
1134 | qed. |
---|
1135 | |
---|
1136 | (* |
---|
1137 | lemma be_to_fe_value_inj : ∀bv1,bv2. |
---|
1138 | be_to_fe_value (ASTint I8 Unsigned) [bv1] |
---|
1139 | = be_to_fe_value (ASTint I8 Unsigned) [bv2] → bv1 = bv2. |
---|
1140 | #bv1 #bv2 |
---|
1141 | whd in match (be_to_fe_value ??); |
---|
1142 | whd in match (be_to_fe_value ??); |
---|
1143 | cases bv1 normalize nodelta |
---|
1144 | [ 1: cases bv2 normalize nodelta |
---|
1145 | [ 1: #H @refl | 2: |
---|
1146 | try // |
---|
1147 | [ cases bv2 *) |
---|
1148 | |
---|
1149 | lemma beloadv_free_beloadv : |
---|
1150 | ∀m,block,ptr,res. |
---|
1151 | beloadv (free m block) ptr = Some ? res → |
---|
1152 | beloadv m ptr = Some ? res. |
---|
1153 | * #contents #next #nextpos #block * #pblock #poff #res |
---|
1154 | #H lapply (beloadv_free_blocks_neq … H) #Hblocks_neq |
---|
1155 | lapply H |
---|
1156 | whd in match (beloadv ??); |
---|
1157 | whd in match (beloadv ??) in ⊢ (? → %); |
---|
1158 | whd in match (nextblock (free ??)); |
---|
1159 | cases (Zltb (block_id pblock) next) |
---|
1160 | [ 2: normalize #Habsurd destruct (Habsurd) ] |
---|
1161 | normalize nodelta |
---|
1162 | <(low_free_eq … Hblocks_neq) |
---|
1163 | <(high_free_eq … Hblocks_neq) |
---|
1164 | whd in match (free ??); |
---|
1165 | whd in match (update_block ?????); |
---|
1166 | @(eq_block_elim … pblock block) |
---|
1167 | [ 1: #Habsurd >Habsurd in Hblocks_neq; * #H @(False_ind … (H (refl ??))) ] |
---|
1168 | #_ normalize nodelta |
---|
1169 | #H @H |
---|
1170 | qed. |
---|
1171 | |
---|
1172 | lemma beloadv_free_beloadv2 : |
---|
1173 | ∀m,block,ptr,res. |
---|
1174 | pblock ptr ≠ block → |
---|
1175 | beloadv m ptr = Some ? res → |
---|
1176 | beloadv (free m block) ptr = Some ? res. |
---|
1177 | * #contents #next #nextpos #block * #pblock #poff #res #Hneq |
---|
1178 | whd in match (beloadv ??); |
---|
1179 | whd in match (beloadv ??) in ⊢ (? → %); |
---|
1180 | whd in match (nextblock (free ??)); |
---|
1181 | cases (Zltb (block_id pblock) next) |
---|
1182 | [ 2: normalize #Habsurd destruct (Habsurd) ] |
---|
1183 | normalize nodelta |
---|
1184 | <(low_free_eq … Hneq) |
---|
1185 | <(high_free_eq … Hneq) |
---|
1186 | whd in match (free ??); |
---|
1187 | whd in match (update_block ?????); |
---|
1188 | @(eq_block_elim … pblock block) |
---|
1189 | [ 1: #Habsurd >Habsurd in Hneq; * #H @(False_ind … (H (refl ??))) ] |
---|
1190 | #_ normalize nodelta |
---|
1191 | #H @H |
---|
1192 | qed. |
---|
1193 | |
---|
1194 | lemma beloadv_free_simulation : |
---|
1195 | ∀m1,m2,block,ptr,res. |
---|
1196 | ∀mem_hyp : sr_memext m1 m2. |
---|
1197 | beloadv (free m1 block) ptr = Some ? res → beloadv (free m2 block) ptr = Some ? res. |
---|
1198 | * #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2 |
---|
1199 | * #br #bid * * #pr #pid #poff #res * |
---|
1200 | #Hload_sim #Hme_writeable #Hme_writeable_valid #Hptr_not_mem #Hvalid_conserv |
---|
1201 | #Hload |
---|
1202 | lapply (beloadv_free_beloadv … Hload) #Hload_before_free |
---|
1203 | lapply (beloadv_free_blocks_neq … Hload) #Hblocks_neq |
---|
1204 | @beloadv_free_beloadv2 |
---|
1205 | [ 1: @Hblocks_neq ] |
---|
1206 | @Hload_sim assumption |
---|
1207 | qed. |
---|
1208 | |
---|
1209 | lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p. |
---|
1210 | #m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %); |
---|
1211 | #H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %); |
---|
1212 | elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b))) |
---|
1213 | [ 1: #Hlt >Hlt normalize nodelta |
---|
1214 | @(eq_block_elim … b (pblock p)) |
---|
1215 | [ 1: #Heq >Heq whd in match (free ??); |
---|
1216 | whd in match (update_block ?????); >eq_block_b_b |
---|
1217 | normalize nodelta normalize in match (low ?); |
---|
1218 | >Zltb_unsigned_OZ >andb_comm >andb_lsimpl_false normalize nodelta |
---|
1219 | #Habsurd destruct (Habsurd) |
---|
1220 | | 2: #Hblock_neq whd in match (free ? ?); |
---|
1221 | whd in match (update_block ?????); |
---|
1222 | >(not_eq_block_rev … Hblock_neq) normalize nodelta |
---|
1223 | cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) |
---|
1224 | [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
1225 | >andb_lsimpl_true |
---|
1226 | lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p))) |
---|
1227 | (high (blocks m (pblock p)))) |
---|
1228 | cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p)))) |
---|
1229 | [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
1230 | normalize nodelta #H #_ /2 by ex_intro/ |
---|
1231 | ] |
---|
1232 | | 2: * #Hlt #Hle >Hlt normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
1233 | qed. |
---|
1234 | |
---|
1235 | lemma outbound_free_to_outbound : ∀m,b,p. outbound_pointer (free m b) p → outbound_pointer m p. |
---|
1236 | #m #b #p whd in match (free ??); |
---|
1237 | whd in match (outbound_pointer ??) in ⊢ (% → %); |
---|
1238 | whd in match (update_block ????); |
---|
1239 | whd in match (low_bound ??); whd in match (high_bound ??); |
---|
1240 | @(eq_block_elim … (pblock p) b) normalize nodelta |
---|
1241 | [ 1: #Heq >Heq cases (Zltb ? (nextblock m)) |
---|
1242 | [ 2: * * #Habsurd destruct (Habsurd) ] |
---|
1243 | * * #_ whd in match (low ?); whd in match (high ?); |
---|
1244 | #H1 #H2 <H2 in H1; normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
1245 | | 2: #Hneq #H @H ] |
---|
1246 | qed. |
---|
1247 | |
---|
1248 | lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true. |
---|
1249 | #m #b #p #Hvalid |
---|
1250 | lapply (valid_pointer_def … m p) * #_ #Hdef @Hdef |
---|
1251 | elim (valid_pointer_def … (free m b) p) #H #_ |
---|
1252 | elim (H Hvalid) |
---|
1253 | [ 1: #Hin %1 @in_bounds_free_to_in_bounds assumption |
---|
1254 | | 2: #Hout %2 @outbound_free_to_outbound assumption ] |
---|
1255 | qed. |
---|
1256 | |
---|
1257 | lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p. |
---|
1258 | #m #b #p |
---|
1259 | whd in match (valid_pointer ??); |
---|
1260 | whd in match (free ??); |
---|
1261 | whd in match (update_block ????); |
---|
1262 | whd in match (low_bound ??); |
---|
1263 | whd in match (high_bound ??); |
---|
1264 | @(eq_block_elim … b (pblock p)) |
---|
1265 | [ 1: #Heq >Heq >eq_block_b_b normalize nodelta |
---|
1266 | whd in match (low ?); whd in match (high ?); |
---|
1267 | cases (Zltb ? (nextblock m)) |
---|
1268 | [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
1269 | >andb_lsimpl_true >free_not_valid #Habsurd destruct (Habsurd) |
---|
1270 | | 2: #Hneq #_ @Hneq ] |
---|
1271 | qed. |
---|
1272 | |
---|
1273 | lemma valid_pointer_free : ∀m1,m2. sr_memext m1 m2 → ∀p,b. valid_pointer (free m1 b) p = true → valid_pointer (free m2 b) p = true. |
---|
1274 | #m1 #m2 #Hext #p #b #Hvalid |
---|
1275 | lapply (valid_free_to_valid … Hvalid) #Hvalid_before_free |
---|
1276 | lapply (me_valid_pointers … Hext … Hvalid_before_free) |
---|
1277 | lapply (valid_after_free … Hvalid) #Hneq |
---|
1278 | whd in match (free ??); |
---|
1279 | whd in match (update_block ????); |
---|
1280 | whd in match (valid_pointer ??) in ⊢ (% → %); |
---|
1281 | whd in match (low_bound ??) in ⊢ (% → %); |
---|
1282 | whd in match (high_bound ??) in ⊢ (% → %); |
---|
1283 | >(not_eq_block_rev … Hneq) normalize nodelta #H @H |
---|
1284 | qed. |
---|
1285 | |
---|
1286 | (* Performing a [free] preserves memory extensions. *) |
---|
1287 | lemma free_memory_ext : |
---|
1288 | ∀m1,m2,bl. |
---|
1289 | sr_memext m1 m2 → |
---|
1290 | sr_memext (free m1 bl) (free m2 bl). |
---|
1291 | #m1 #m2 #bl #Hext |
---|
1292 | % |
---|
1293 | [ 1: @(λptr,bev. beloadv_free_simulation m1 m2 bl ptr bev Hext) |
---|
1294 | | 2: @(filter ? (λwb. notb (eq_block wb bl)) (me_writeable … Hext)) |
---|
1295 | | 3: #b #Hmem |
---|
1296 | cut (mem block b (me_writeable m1 m2 Hext)) |
---|
1297 | [ elim (me_writeable m1 m2 Hext) in Hmem; |
---|
1298 | [ 1: #H @H |
---|
1299 | | 2: #h #tl #Hind whd in match (filter ???); |
---|
1300 | @(eq_block_elim … h bl) normalize in match (notb ?); normalize nodelta |
---|
1301 | [ 1: #Heq #H whd in match (meml ???); destruct %2 @Hind @H |
---|
1302 | | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * |
---|
1303 | [ 1: #H %1 @H |
---|
1304 | | 2: #H %2 @Hind @H ] ] ] ] |
---|
1305 | #Hmem2 lapply (me_writeable_valid … Hmem2) |
---|
1306 | elim m2 #contents #nextblock #pos elim b #br #bid |
---|
1307 | normalize #H @H |
---|
1308 | | 4: #p #Hvalid elim (valid_pointer_free_ok_alt … Hvalid) |
---|
1309 | [ 1: #Heq >Heq elim (me_writeable m1 m2 Hext) |
---|
1310 | [ 1: normalize % // |
---|
1311 | | 2: #hd #tl #Hind |
---|
1312 | whd in match (filter ???); |
---|
1313 | @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta |
---|
1314 | [ 1: #Heq @Hind |
---|
1315 | | 2: #Hneq whd in match (meml ???); % * |
---|
1316 | [ 1: #Heq elim Hneq #H @H @(sym_eq … Heq) |
---|
1317 | | 2: #H elim Hind #Hind @Hind @H ] ] ] |
---|
1318 | | 2: * #_ #Hvalid lapply (me_writeable_ok … Hext … Hvalid) |
---|
1319 | * #Hyp % #Htarget @Hyp |
---|
1320 | elim (me_writeable m1 m2 Hext) in Htarget; |
---|
1321 | [ 1: normalize // |
---|
1322 | | 2: #hd #tl #Hind |
---|
1323 | whd in match (filter ???); |
---|
1324 | @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta |
---|
1325 | [ 1: #Heq whd in match (meml ???) in ⊢ (? → %); |
---|
1326 | #H %2 @Hind @H |
---|
1327 | | 2: #Hneq whd in match (meml ???); |
---|
1328 | whd in match (meml ???) in ⊢ (? → %); * |
---|
1329 | [ 1: #H %1 @H |
---|
1330 | | 2: #H %2@Hind @H ] ] ] ] |
---|
1331 | | 5: #p @valid_pointer_free @Hext |
---|
1332 | ] qed. |
---|
1333 | |
---|
1334 | |
---|
1335 | lemma free_list_memory_ext : |
---|
1336 | ∀l,m1,m2. |
---|
1337 | sr_memext m1 m2 → |
---|
1338 | sr_memext (free_list m1 l) (free_list m2 l). |
---|
1339 | #l elim l |
---|
1340 | [ 1: #m1 #m2 #H @H |
---|
1341 | | 2: #hd #tl #Hind #m1 #m2 #H >free_list_cons >free_list_cons |
---|
1342 | @free_memory_ext @Hind @H |
---|
1343 | ] qed. |
---|
1344 | |
---|
1345 | (* Extend the previous lemma to [free_list] *) |
---|
1346 | lemma beloadv_free_list_memory_ext : |
---|
1347 | ∀m1,m2,blocks,ptr,res. |
---|
1348 | ∀mem_hyp : sr_memext m1 m2. |
---|
1349 | beloadv (free_list m1 blocks) ptr = Some ? res → beloadv (free_list m2 blocks) ptr = Some ? res. |
---|
1350 | #m1 #m2 #blocks #mtr #res #Hext #Hload |
---|
1351 | lapply (free_list_memory_ext blocks … Hext) #Hext_list |
---|
1352 | lapply (me_inj … Hext_list) #H @H @Hload |
---|
1353 | qed. |
---|
1354 | |
---|
1355 | |
---|
1356 | (* Prove that memory extensions are preserved by free.*) |
---|
1357 | (* |
---|
1358 | lemma memext_free_conservation : |
---|
1359 | ∀m1,m2 : mem. |
---|
1360 | ∀mem_hyp : sr_memext m1 m2. |
---|
1361 | ∀env,env_ext. |
---|
1362 | ∀new_vars. |
---|
1363 | ∀env_hyp : disjoint_extension env m1 env_ext m2 new_vars mem_hyp. |
---|
1364 | (sr_memext (free_list m1 (blocks_of_env env)) |
---|
1365 | (free_list m2 (blocks_of_env env_ext))). |
---|
1366 | #m1 #m2 * #Hloadsim #Hwriteable #Hwritevalid #Holdnotwriteable #Hvalidok #env #env_ext #new_vars |
---|
1367 | whd in ⊢ (% → ?); #Hdisjoint *) |
---|
1368 | |
---|
1369 | |
---|
1370 | (* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if |
---|
1371 | * the variable is not in a local environment, then we search into the global one. |
---|
1372 | * A proper "extension" of a local environment should be such that the extension |
---|
1373 | * does not collide with a given global env. |
---|
1374 | * To see the details of why we need that, see [exec_lvalue'], Evar id case. |
---|
1375 | *) |
---|
1376 | definition ext_fresh_for_genv ≝ |
---|
1377 | λ(ext : list (ident × type)). λ(ge : genv). |
---|
1378 | ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?. |
---|
1379 | |
---|
1380 | (* Any environment is a "disjoint" extension of itself with nothing. *) |
---|
1381 | (* |
---|
1382 | lemma disjoint_extension_nil : ∀e,m,types. disjoint_extension e m e m types []. |
---|
1383 | #e #m #ty #id |
---|
1384 | normalize in match (mem_assoc_env id []); normalize nodelta |
---|
1385 | cases (lookup ?? e id) try // |
---|
1386 | #b normalize nodelta |
---|
1387 | % #ty cases (load_value_of_type ????) |
---|
1388 | [ 1: %2 /2/ | 2: #v %1 %{v} %{v} @conj // |
---|
1389 | cases (assoc_env id ty) // |
---|
1390 | qed. *) |
---|
1391 | |
---|
1392 | (* "generic" simulation relation on [res ?] *) |
---|
1393 | definition res_sim ≝ |
---|
1394 | λ(A : Type[0]). |
---|
1395 | λ(r1, r2 : res A). |
---|
1396 | ∀a. r1 = OK ? a → r2 = OK ? a. |
---|
1397 | |
---|
1398 | (* Specialisation of [res_sim] to match [exec_expr] *) |
---|
1399 | definition exec_expr_sim ≝ res_sim (val × trace). |
---|
1400 | |
---|
1401 | (* Specialisation of [res_sim] to match [exec_lvalue] *) |
---|
1402 | definition exec_lvalue_sim ≝ res_sim (block × offset × trace). |
---|
1403 | |
---|
1404 | lemma load_value_of_type_dec : ∀ty, m, b, o. load_value_of_type ty m b o = None ? ∨ ∃r. load_value_of_type ty m b o = Some ? r. |
---|
1405 | #ty #m #b #o cases (load_value_of_type ty m b o) |
---|
1406 | [ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed. |
---|
1407 | |
---|
1408 | (* Simulation relations. *) |
---|
1409 | inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝ |
---|
1410 | | swc_stop : ∀fvs. |
---|
1411 | switch_cont_sim fvs Kstop Kstop |
---|
1412 | | swc_seq : ∀fvs,s,k,k',u,result. |
---|
1413 | fresh_for_statement s u → |
---|
1414 | switch_cont_sim fvs k k' → |
---|
1415 | switch_removal s fvs u = Some ? result → |
---|
1416 | switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k') |
---|
1417 | | swc_while : ∀fvs,e,s,cl,k,k',u,result. |
---|
1418 | fresh_for_statement (Swhile e s cl) u → |
---|
1419 | switch_cont_sim fvs k k' → |
---|
1420 | switch_removal s fvs u = Some ? result → |
---|
1421 | switch_cont_sim fvs (Kwhile e s cl k) (Kwhile e (ret_st ? result) cl k') |
---|
1422 | | swc_dowhile : ∀fvs,e,s,k,k',u,result. |
---|
1423 | fresh_for_statement (Sdowhile e s) u → |
---|
1424 | switch_cont_sim fvs k k' → |
---|
1425 | switch_removal s fvs u = Some ? result → |
---|
1426 | switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k') |
---|
1427 | | swc_for1 : ∀fvs,e,s1,s2,k,k',u,result. |
---|
1428 | fresh_for_statement (Sfor Sskip e s1 s2) u → |
---|
1429 | switch_cont_sim fvs k k' → |
---|
1430 | switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result → |
---|
1431 | switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k') |
---|
1432 | | swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2. |
---|
1433 | fresh_for_statement (Sfor Sskip e s1 s2) u → |
---|
1434 | switch_cont_sim fvs k k' → |
---|
1435 | switch_removal s1 fvs u = Some ? result1 → |
---|
1436 | switch_removal s2 fvs (ret_u ? result1) = Some ? result2 → |
---|
1437 | switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k') |
---|
1438 | | swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2. |
---|
1439 | fresh_for_statement (Sfor Sskip e s1 s2) u → |
---|
1440 | switch_cont_sim fvs k k' → |
---|
1441 | switch_removal s1 fvs u = Some ? result1 → |
---|
1442 | switch_removal s2 fvs (ret_u ? result1) = Some ? result2 -> |
---|
1443 | switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k') |
---|
1444 | | swc_switch : ∀fvs,k,k'. |
---|
1445 | switch_cont_sim fvs k k' → |
---|
1446 | switch_cont_sim fvs (Kswitch k) (Kswitch k') |
---|
1447 | | swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *) |
---|
1448 | switch_cont_sim fvs k k' → |
---|
1449 | (* /!\ Update [en] with [fvs'] ... *) |
---|
1450 | switch_cont_sim |
---|
1451 | (map … (fst ??) (\snd (function_switch_removal f))) |
---|
1452 | (Kcall r f en k) |
---|
1453 | (Kcall r (\fst (function_switch_removal f)) en' k'). |
---|
1454 | |
---|
1455 | (* |
---|
1456 | en' = exec_alloc_variables en m (\snd (function_switch_removal f)) |
---|
1457 | TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc |
---|
1458 | variable dans en'. |
---|
1459 | |
---|
1460 | 1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que |
---|
1461 | dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est |
---|
1462 | de savoir que : |
---|
1463 | si je lookup une variable générée à partir d'un univers frais dans l'environement en', |
---|
1464 | alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step, |
---|
1465 | et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s" |
---|
1466 | et à etre "(function_switch_removal f)-contained". |
---|
1467 | |
---|
1468 | 2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup |
---|
1469 | et l'update n'altèrent pas le comportement du reste du programme. |
---|
1470 | |
---|
1471 | relation : si un statement S0 est inclus dans un statement S1, alors les variables générées |
---|
1472 | depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1. |
---|
1473 | en particulier, si u est frais pour S1 u est frais pour S0. |
---|
1474 | |
---|
1475 | Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique |
---|
1476 | "environment_extension en en' (\fst (\fst (switch_removal s u)))" |
---|
1477 | |
---|
1478 | --------------------------------------------------------------- |
---|
1479 | . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction |
---|
1480 | et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération. |
---|
1481 | on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner |
---|
1482 | en argument les freshgens qui correspondent à ce que la fonction switch_removal fait. |
---|
1483 | *) |
---|
1484 | |
---|
1485 | (* env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) → |
---|
1486 | env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) → *) |
---|
1487 | record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { |
---|
1488 | rg_find_symbol: ∀s. |
---|
1489 | find_symbol ? ge s = find_symbol ? ge' s; |
---|
1490 | rg_find_funct: ∀v,f. |
---|
1491 | find_funct ? ge v = Some ? f → |
---|
1492 | find_funct ? ge' v = Some ? (t f); |
---|
1493 | rg_find_funct_ptr: ∀b,f. |
---|
1494 | find_funct_ptr ? ge b = Some ? f → |
---|
1495 | find_funct_ptr ? ge' b = Some ? (t f) |
---|
1496 | }. |
---|
1497 | |
---|
1498 | (* This record aims to shorten the definition of the simulation relation on states more readeable. *) |
---|
1499 | inductive switch_state_sim (ge : genv) : state → state → Prop ≝ |
---|
1500 | | sws_state : |
---|
1501 | (* current statement *) |
---|
1502 | ∀sss_statement : statement. |
---|
1503 | (* statement after transformation *) |
---|
1504 | ∀sss_result : swret statement. |
---|
1505 | (* label universe *) |
---|
1506 | ∀sss_lu : universe SymbolTag. |
---|
1507 | (* [sss_lu] must be fresh *) |
---|
1508 | ∀sss_lu_fresh : fresh_for_statement sss_statement sss_lu. |
---|
1509 | (* current function *) |
---|
1510 | ∀sss_func : function. |
---|
1511 | (* current function after translation *) |
---|
1512 | ∀sss_func_tr : function. |
---|
1513 | (* variables generated during conversion of the function *) |
---|
1514 | ∀sss_new_vars : list (ident × type). |
---|
1515 | (* statement of the transformation *) |
---|
1516 | ∀sss_func_hyp : 〈sss_func_tr, sss_new_vars〉 = function_switch_removal sss_func. |
---|
1517 | (* memory state before conversion *) |
---|
1518 | ∀sss_m : mem. |
---|
1519 | (* memory state after conversion *) |
---|
1520 | ∀sss_m_ext : mem. |
---|
1521 | (* environment before conversion *) |
---|
1522 | ∀sss_env : env. |
---|
1523 | (* environment after conversion *) |
---|
1524 | ∀sss_env_ext : env. |
---|
1525 | (* continuation before conversion *) |
---|
1526 | ∀sss_k : cont. |
---|
1527 | (* continuation after conversion *) |
---|
1528 | ∀sss_k_ext : cont. |
---|
1529 | (* memory "injection" *) |
---|
1530 | ∀sss_mem_hyp : sr_memext sss_m sss_m_ext. |
---|
1531 | (* The extended environment does not interfer with the old one. *) |
---|
1532 | ∀sss_env_hyp : disjoint_extension sss_env sss_m sss_env_ext sss_m_ext sss_new_vars sss_mem_hyp. |
---|
1533 | (* conversion of the current statement, using the variables produced during the conversion of the current function *) |
---|
1534 | ∀sss_result_hyp : switch_removal sss_statement (map ?? (fst ??) sss_new_vars) sss_lu = Some ? sss_result. |
---|
1535 | (* simulation between the continuations before and after conversion. *) |
---|
1536 | ∀sss_k_hyp : switch_cont_sim (map ?? (fst ??) sss_new_vars) sss_k sss_k_ext. |
---|
1537 | ext_fresh_for_genv sss_new_vars ge → |
---|
1538 | switch_state_sim |
---|
1539 | ge |
---|
1540 | (State sss_func sss_statement sss_k sss_env sss_m) |
---|
1541 | (State sss_func_tr (ret_st … sss_result) sss_k_ext sss_env_ext sss_m_ext) |
---|
1542 | | sws_callstate : ∀vars, fd,args,k,k',m. |
---|
1543 | switch_cont_sim vars k k' → |
---|
1544 | switch_state_sim ge (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m) |
---|
1545 | | sws_returnstate : |
---|
1546 | ∀ssr_vars. |
---|
1547 | ∀ssr_result. |
---|
1548 | ∀ssr_k : cont. |
---|
1549 | ∀ssr_k_ext : cont. |
---|
1550 | ∀ssr_m : mem. |
---|
1551 | ∀ssr_m_ext : mem. |
---|
1552 | ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext. |
---|
1553 | switch_cont_sim ssr_vars ssr_k ssr_k_ext → |
---|
1554 | switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext) |
---|
1555 | | sws_finalstate : ∀r. |
---|
1556 | switch_state_sim ge (Finalstate r) (Finalstate r). |
---|
1557 | |
---|
1558 | lemma call_cont_swremoval : ∀fv,k,k'. |
---|
1559 | switch_cont_sim fv k k' → |
---|
1560 | switch_cont_sim fv (call_cont k) (call_cont k'). |
---|
1561 | #fv #k0 #k0' #K elim K /2/ |
---|
1562 | qed. |
---|
1563 | |
---|
1564 | (* [eventually ge P s tr] states that after a finite number of [exec_step], the |
---|
1565 | property P on states will be verified. *) |
---|
1566 | inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝ |
---|
1567 | | eventually_base : ∀s,t,s'. |
---|
1568 | exec_step ge s = Value io_out io_in ? 〈t, s'〉 → |
---|
1569 | P s' → |
---|
1570 | eventually ge P s t |
---|
1571 | | eventually_step : ∀s,t,s',t',trace. |
---|
1572 | exec_step ge s = Value io_out io_in ? 〈t, s'〉 → |
---|
1573 | eventually ge P s' t' → |
---|
1574 | trace = (t ⧺ t') → |
---|
1575 | eventually ge P s trace. |
---|
1576 | |
---|
1577 | (* [eventually] is not so nice to use directly, we would like to make the mandatory |
---|
1578 | * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not |
---|
1579 | to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *) |
---|
1580 | lemma eventually_now : ∀ge,P,s,t. |
---|
1581 | (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → |
---|
1582 | eventually ge P s t. |
---|
1583 | #ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP} (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *) |
---|
1584 | qed. |
---|
1585 | |
---|
1586 | lemma eventually_later : ∀ge,P,s,t. |
---|
1587 | (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) → |
---|
1588 | eventually ge P s t. |
---|
1589 | #ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq} |
---|
1590 | try assumption |
---|
1591 | qed. |
---|
1592 | |
---|
1593 | lemma exec_lvalue_expr_elim : |
---|
1594 | ∀r1,r2,Pok,Qok. |
---|
1595 | exec_lvalue_sim r1 r2 → |
---|
1596 | (∀val,trace. |
---|
1597 | match Pok 〈val,trace〉 with |
---|
1598 | [ Error err ⇒ True |
---|
1599 | | OK pvt ⇒ |
---|
1600 | let 〈pval,ptrace〉 ≝ pvt in |
---|
1601 | match Qok 〈val,trace〉 with |
---|
1602 | [ Error err ⇒ False |
---|
1603 | | OK qvt ⇒ |
---|
1604 | let 〈qval,qtrace〉 ≝ qvt in |
---|
1605 | ptrace = qtrace ∧ pval = qval |
---|
1606 | ] |
---|
1607 | ]) → |
---|
1608 | exec_expr_sim |
---|
1609 | (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) |
---|
1610 | (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). |
---|
1611 | #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); |
---|
1612 | elim r1 |
---|
1613 | [ 2: #error #_ #_ normalize #a #Habsurd destruct (Habsurd) |
---|
1614 | | 1: normalize nodelta #a #H lapply (H a (refl ??)) |
---|
1615 | #Hr2 >Hr2 normalize #H #a' elim a * #b #o #tr |
---|
1616 | lapply (H 〈b, o〉 tr) #H1 #H2 >H2 in H1; |
---|
1617 | normalize nodelta elim a' in H2; #pval #ptrace #Hpok |
---|
1618 | normalize nodelta cases (Qok 〈b,o,tr〉) |
---|
1619 | [ 2: #error normalize #Habsurd @(False_ind … Habsurd) |
---|
1620 | | 1: * #qval #qtrace normalize nodelta * #Htrace #Hval |
---|
1621 | destruct @refl |
---|
1622 | ] ] qed. |
---|
1623 | |
---|
1624 | |
---|
1625 | lemma exec_expr_expr_elim : |
---|
1626 | ∀r1,r2,Pok,Qok. |
---|
1627 | exec_expr_sim r1 r2 → |
---|
1628 | (∀val,trace. |
---|
1629 | match Pok 〈val,trace〉 with |
---|
1630 | [ Error err ⇒ True |
---|
1631 | | OK pvt ⇒ |
---|
1632 | let 〈pval,ptrace〉 ≝ pvt in |
---|
1633 | match Qok 〈val,trace〉 with |
---|
1634 | [ Error err ⇒ False |
---|
1635 | | OK qvt ⇒ |
---|
1636 | let 〈qval,qtrace〉 ≝ qvt in |
---|
1637 | ptrace = qtrace ∧ pval = qval |
---|
1638 | ] |
---|
1639 | ]) → |
---|
1640 | exec_expr_sim |
---|
1641 | (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) |
---|
1642 | (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). |
---|
1643 | #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); |
---|
1644 | elim r1 |
---|
1645 | [ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd) |
---|
1646 | | 1: normalize nodelta #a #H lapply (H a (refl ??)) |
---|
1647 | #Hr2 >Hr2 normalize nodelta #H |
---|
1648 | elim a in Hr2; #val #trace |
---|
1649 | lapply (H … val trace) |
---|
1650 | cases (Pok 〈val, trace〉) |
---|
1651 | [ 2: #error normalize #_ #_ #a' #Habsurd destruct (Habsurd) |
---|
1652 | | 1: * #pval #ptrace normalize nodelta |
---|
1653 | cases (Qok 〈val,trace〉) |
---|
1654 | [ 2: #error normalize #Hfalse @(False_ind … Hfalse) |
---|
1655 | | 1: * #qval #qtrace normalize nodelta * #Htrace_eq #Hval_eq |
---|
1656 | #Hr2_eq destruct #a #H @H |
---|
1657 | ] ] ] qed. |
---|
1658 | |
---|
1659 | |
---|
1660 | lemma load_value_of_type_inj : ∀m1,m2,b,off,ty. |
---|
1661 | sr_memext m1 m2 → ∀v. |
---|
1662 | load_value_of_type ty m1 b off = Some ? v → |
---|
1663 | load_value_of_type ty m2 b off = Some ? v. |
---|
1664 | #m1 #m2 #b #off #ty #Hinj #v |
---|
1665 | @(load_sim_fe … (me_inj … Hinj) (mk_pointer b off)) |
---|
1666 | qed. |
---|
1667 | |
---|
1668 | (* Conservation of the smenantics of binary operators *) |
---|
1669 | lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2. |
---|
1670 | ∀Hext:sr_memext m1 m2. ∀res. |
---|
1671 | sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res → |
---|
1672 | sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 = Some ? res. |
---|
1673 | #op #v1 #v2 #e1 #e2 #m1 #m2 #Hmemext #res cases op |
---|
1674 | whd in match (sem_binary_operation ??????); |
---|
1675 | try // |
---|
1676 | whd in match (sem_binary_operation ??????); |
---|
1677 | elim m1 in Hmemext; #contents1 #nextblocks1 #Hnextpos1 |
---|
1678 | elim m2 #contents2 #nextblocks2 #Hnextpos2 |
---|
1679 | * #Hptrsim #writeable #Hvalid #Hdisjoint #Hvalid_cons |
---|
1680 | whd in match (sem_cmp ??????); |
---|
1681 | whd in match (sem_cmp ??????); |
---|
1682 | [ 1: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
1683 | normalize nodelta |
---|
1684 | [ 1: #sz #sg try // |
---|
1685 | | 2: #opt #ty |
---|
1686 | cases v1 normalize nodelta |
---|
1687 | [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] |
---|
1688 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1689 | | 4: #H @H ] |
---|
1690 | cases v2 normalize nodelta |
---|
1691 | [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] |
---|
1692 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1693 | | 4: #H @H ] |
---|
1694 | lapply (Hvalid_cons ptr) |
---|
1695 | elim (freed_pointer_dec … (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
1696 | [ 2: #Hnot_freed #Hvalid lapply (Hvalid … Hnot_freed) |
---|
1697 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
1698 | [ 2: >andb_lsimpl_false normalize nodelta #_ #Habsurd destruct (Habsurd) ] |
---|
1699 | #Hvalid >(Hvalid (refl ??)) |
---|
1700 | lapply (Hvalid_cons ptr') |
---|
1701 | elim (freed_pointer_dec … (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
1702 | [ 2: #Hnot_freed' #Hvalid' lapply (Hvalid' … Hnot_freed') |
---|
1703 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
1704 | [ 2: >andb_lsimpl_true #_ normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
1705 | #H' >(H' (refl ??)) >andb_lsimpl_true #Hres @Hres |
---|
1706 | | 1: normalize in ⊢ (% → ?); * #Hlow' #Hhigh' #_ |
---|
1707 | >andb_lsimpl_true >andb_lsimpl_true |
---|
1708 | whd in match (valid_pointer ??); |
---|
1709 | whd in match (low_bound ??); |
---|
1710 | whd in match (high_bound ??); |
---|
1711 | >Hlow' >Hhigh' >Zleb_unsigned_OZ >andb_comm >andb_lsimpl_true |
---|
1712 | whd in match (valid_pointer ??); |
---|
1713 | |
---|
1714 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
1715 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1716 | #H' >(H' (refl ??)) #Hok @Hok |
---|
1717 | | 1: |
---|
1718 | ] |
---|
1719 | | 3: #fsz #H @H |
---|
1720 | | 4: #ty1 #ty2 #H @H ] |
---|
1721 | | 2: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
1722 | normalize nodelta |
---|
1723 | [ 1: #sz #sg try // |
---|
1724 | | 2: #opt #ty |
---|
1725 | cases v1 normalize nodelta |
---|
1726 | [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] |
---|
1727 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1728 | | 4: #H @H ] |
---|
1729 | cases v2 normalize nodelta |
---|
1730 | [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] |
---|
1731 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1732 | | 4: #H @H ] |
---|
1733 | lapply (Hvalid_cons ptr) |
---|
1734 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
1735 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1736 | #H >(H (refl ??)) |
---|
1737 | lapply (Hvalid_cons ptr') |
---|
1738 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
1739 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1740 | #H' >(H' (refl ??)) #Hok @Hok |
---|
1741 | | 3: #fsz #H @H |
---|
1742 | | 4: #ty1 #ty2 #H @H ] |
---|
1743 | | 3: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
1744 | normalize nodelta |
---|
1745 | [ 1: #sz #sg try // |
---|
1746 | | 2: #opt #ty |
---|
1747 | cases v1 normalize nodelta |
---|
1748 | [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] |
---|
1749 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1750 | | 4: #H @H ] |
---|
1751 | cases v2 normalize nodelta |
---|
1752 | [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] |
---|
1753 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1754 | | 4: #H @H ] |
---|
1755 | lapply (Hvalid_cons ptr) |
---|
1756 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
1757 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1758 | #H >(H (refl ??)) |
---|
1759 | lapply (Hvalid_cons ptr') |
---|
1760 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
1761 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1762 | #H' >(H' (refl ??)) #Hok @Hok |
---|
1763 | | 3: #fsz #H @H |
---|
1764 | | 4: #ty1 #ty2 #H @H ] |
---|
1765 | | 4: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
1766 | normalize nodelta |
---|
1767 | [ 1: #sz #sg #H @H |
---|
1768 | | 2: #opt #ty |
---|
1769 | cases v1 normalize nodelta |
---|
1770 | [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] |
---|
1771 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1772 | | 4: #H @H ] |
---|
1773 | cases v2 normalize nodelta |
---|
1774 | [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] |
---|
1775 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1776 | | 4: #H @H ] |
---|
1777 | lapply (Hvalid_cons ptr) |
---|
1778 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
1779 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1780 | #H >(H (refl ??)) |
---|
1781 | lapply (Hvalid_cons ptr') |
---|
1782 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
1783 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1784 | #H' >(H' (refl ??)) #Hok @Hok |
---|
1785 | | 3: #fsz #H @H |
---|
1786 | | 4: #ty1 #ty2 #H @H ] |
---|
1787 | | 5: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
1788 | normalize nodelta |
---|
1789 | [ 1: #sz #sg #H @H |
---|
1790 | | 2: #opt #ty |
---|
1791 | cases v1 normalize nodelta |
---|
1792 | [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] |
---|
1793 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1794 | | 4: #H @H ] |
---|
1795 | cases v2 normalize nodelta |
---|
1796 | [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] |
---|
1797 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1798 | | 4: #H @H ] |
---|
1799 | lapply (Hvalid_cons ptr) |
---|
1800 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
1801 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1802 | #H >(H (refl ??)) |
---|
1803 | lapply (Hvalid_cons ptr') |
---|
1804 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
1805 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1806 | #H' >(H' (refl ??)) #Hok @Hok |
---|
1807 | | 3: #fsz #H @H |
---|
1808 | | 4: #ty1 #ty2 #H @H ] |
---|
1809 | | 6: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
1810 | normalize nodelta |
---|
1811 | [ 1: #sz #sg #H @H |
---|
1812 | | 2: #opt #ty |
---|
1813 | cases v1 normalize nodelta |
---|
1814 | [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] |
---|
1815 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1816 | | 4: #H @H ] |
---|
1817 | cases v2 normalize nodelta |
---|
1818 | [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] |
---|
1819 | [ 1,2,3: #Habsurd destruct (Habsurd) |
---|
1820 | | 4: #H @H ] |
---|
1821 | lapply (Hvalid_cons ptr) |
---|
1822 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
1823 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1824 | #H >(H (refl ??)) |
---|
1825 | lapply (Hvalid_cons ptr') |
---|
1826 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
1827 | [ 2: #_ normalize #Habsurd destruct (Habsurd) ] |
---|
1828 | #H' >(H' (refl ??)) #Hok @Hok |
---|
1829 | | 3: #fsz #H @H |
---|
1830 | | 4: #ty1 #ty2 #H @H ] |
---|
1831 | ] qed. |
---|
1832 | |
---|
1833 | |
---|
1834 | (* Simulation relation on expressions *) |
---|
1835 | lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext. |
---|
1836 | ∀Hext:sr_memext m1 m2. |
---|
1837 | switch_removal_globals ? fundef_switch_removal ge ge' → |
---|
1838 | disjoint_extension en1 m1 en2 m2 ext Hext → |
---|
1839 | ext_fresh_for_genv ext ge → |
---|
1840 | (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧ |
---|
1841 | (∀ed, ty. exec_lvalue_sim (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)). |
---|
1842 | #ge #ge' #en1 #m1 #en2 #m2 #ext #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv |
---|
1843 | @expr_lvalue_ind_combined |
---|
1844 | [ 1: #csz #cty #i #a1 |
---|
1845 | whd in match (exec_expr ????); elim cty |
---|
1846 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
1847 | normalize nodelta |
---|
1848 | [ 2: cases (eq_intsize csz sz) normalize nodelta |
---|
1849 | [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/ |
---|
1850 | | 2: #Habsurd destruct (Habsurd) ] |
---|
1851 | | 4,5,6: #_ #H destruct (H) |
---|
1852 | | *: #H destruct (H) ] |
---|
1853 | | 2: #ty #fl #a1 |
---|
1854 | whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/ |
---|
1855 | | 3: * |
---|
1856 | [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
1857 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
1858 | #ty whd in ⊢ (% → ?); #Hind try @I |
---|
1859 | whd in match (Plvalue ???); |
---|
1860 | [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1 |
---|
1861 | cases (exec_lvalue' ge en1 m1 ? ty) in Hind; |
---|
1862 | [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
1863 | | 1,3,5: normalize nodelta #b1 #H lapply (H b1 (refl ??)) #Heq >Heq |
---|
1864 | normalize nodelta |
---|
1865 | elim b1 * #bl1 #o1 #tr1 (* elim b2 * #bl2 #o2 #tr2 *) |
---|
1866 | whd in match (load_value_of_type' ???); |
---|
1867 | whd in match (load_value_of_type' ???); |
---|
1868 | lapply (load_value_of_type_inj m1 m2 bl1 o1 ty Hext) |
---|
1869 | cases (load_value_of_type ty m1 bl1 o1) |
---|
1870 | [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
1871 | | 2,4,6: #v #H normalize in ⊢ (% → ?); #Heq destruct (Heq) |
---|
1872 | >(H v (refl ??)) @refl |
---|
1873 | ] ] ] |
---|
1874 | | 4: #v #ty whd * * #b #o #tr |
---|
1875 | whd in match (exec_lvalue' ?????); |
---|
1876 | whd in match (exec_lvalue' ?????); |
---|
1877 | lapply (Hdisjoint v) |
---|
1878 | lapply (Hext_fresh_for_genv v) |
---|
1879 | cases (mem_assoc_env v ext) #Hglobal |
---|
1880 | [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1 |
---|
1881 | >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?); |
---|
1882 | >(Hglobal (refl ??)) normalize |
---|
1883 | #Habsurd destruct (Habsurd) |
---|
1884 | | 2: normalize nodelta |
---|
1885 | cases (lookup ?? en1 v) normalize nodelta |
---|
1886 | [ 1: #Hlookup2 <Hlookup2 normalize nodelta |
---|
1887 | lapply (rg_find_symbol … Hrelated v) #Heq_find_sym >Heq_find_sym |
---|
1888 | #H @H |
---|
1889 | | 2: #block |
---|
1890 | cases (lookup ?? en2 v) normalize nodelta |
---|
1891 | [ 1: #Habsurd destruct (Habsurd) |
---|
1892 | | 2: #b #Heq destruct (Heq) #H @H ] |
---|
1893 | ] |
---|
1894 | ] |
---|
1895 | | 5: #e #ty whd in ⊢ (% → %); |
---|
1896 | whd in match (exec_lvalue' ?????); |
---|
1897 | whd in match (exec_lvalue' ?????); |
---|
1898 | cases (exec_expr ge en1 m1 e) |
---|
1899 | [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' #H @H |
---|
1900 | | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ] |
---|
1901 | | 6: #ty #e #ty' |
---|
1902 | #Hsim @(exec_lvalue_expr_elim … Hsim) |
---|
1903 | cases ty |
---|
1904 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
1905 | * #b #o normalize nodelta try /2 by I/ |
---|
1906 | #tr @conj try @refl |
---|
1907 | | 7: #ty #op #e |
---|
1908 | #Hsim @(exec_expr_expr_elim … Hsim) #v #trace |
---|
1909 | cases (sem_unary_operation op v (typeof e)) normalize nodelta |
---|
1910 | try @I |
---|
1911 | #v @conj @refl |
---|
1912 | | 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 |
---|
1913 | @(exec_expr_expr_elim … Hsim1) #v #trace |
---|
1914 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
1915 | [ 2: #error // ] |
---|
1916 | * #pval #ptrace normalize in ⊢ (% → ?); #Hsim2 |
---|
1917 | whd in match (m_bind ?????); |
---|
1918 | >(Hsim2 ? (refl ??)) |
---|
1919 | whd in match (m_bind ?????); |
---|
1920 | lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 Hext) |
---|
1921 | cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1) |
---|
1922 | [ 1: #_ // ] #val #H >(H val (refl ??)) |
---|
1923 | normalize destruct @conj @refl |
---|
1924 | | 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim) |
---|
1925 | #v #tr |
---|
1926 | cut (exec_cast m1 v (typeof e) cast_ty = exec_cast m2 v (typeof e) cast_ty) |
---|
1927 | [ @refl ] |
---|
1928 | #Heq >Heq |
---|
1929 | cases (exec_cast m2 v (typeof e) cast_ty) |
---|
1930 | [ 2: // |
---|
1931 | | 1: #v normalize @conj @refl ] |
---|
1932 | | 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 |
---|
1933 | @(exec_expr_expr_elim … Hsim1) #v #tr |
---|
1934 | cases (exec_bool_of_val ? (typeof e1)) #b |
---|
1935 | [ 2: normalize @I ] |
---|
1936 | cases b normalize nodelta |
---|
1937 | whd in match (m_bind ?????); |
---|
1938 | whd in match (m_bind ?????); |
---|
1939 | normalize nodelta |
---|
1940 | [ 1: (* true branch *) |
---|
1941 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
1942 | [ 2: #error normalize #_ @I |
---|
1943 | | 1: * #e2v #e2tr normalize #H >(H ? (refl ??)) normalize nodelta |
---|
1944 | @conj @refl ] |
---|
1945 | | 2: (* false branch *) |
---|
1946 | cases (exec_expr ge en1 m1 e3) in Hsim3; |
---|
1947 | [ 2: #error normalize #_ @I |
---|
1948 | | 1: * #e3v #e3tr normalize #H >(H ? (refl ??)) normalize nodelta |
---|
1949 | @conj @refl ] ] |
---|
1950 | | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 |
---|
1951 | @(exec_expr_expr_elim … Hsim1) #v #tr |
---|
1952 | cases (exec_bool_of_val v (typeof e1)) |
---|
1953 | [ 2,4: #error normalize @I ] |
---|
1954 | * |
---|
1955 | whd in match (m_bind ?????); |
---|
1956 | whd in match (m_bind ?????); |
---|
1957 | [ 2,3: normalize @conj try @refl ] |
---|
1958 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
1959 | [ 2,4: #error #_ normalize @I ] |
---|
1960 | * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta >(H2 ? (refl ??)) |
---|
1961 | normalize nodelta |
---|
1962 | cases (exec_bool_of_val v2 (typeof e2)) |
---|
1963 | [ 2,4: #error normalize @I ] |
---|
1964 | * normalize @conj @refl |
---|
1965 | | 13: #ty #ty' cases ty |
---|
1966 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n |
---|
1967 | | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
1968 | whd in match (exec_expr ????); whd #a #H @H |
---|
1969 | | 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr |
---|
1970 | whd in match (exec_lvalue' ?????); |
---|
1971 | whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty); |
---|
1972 | whd in match (typeof ?); |
---|
1973 | cases aggregty in Hsim; |
---|
1974 | [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n' |
---|
1975 | | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ] |
---|
1976 | normalize nodelta #Hsim |
---|
1977 | [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ] |
---|
1978 | whd in match (m_bind ?????); |
---|
1979 | whd in match (m_bind ?????); |
---|
1980 | whd in match (exec_lvalue ge en1 m1 (Expr ed ?)); |
---|
1981 | cases (exec_lvalue' ge en1 m1 ed ?) in Hsim; |
---|
1982 | [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] |
---|
1983 | * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H |
---|
1984 | whd in match (exec_lvalue ge' en2 m2 (Expr ed ?)); |
---|
1985 | >(H ? (refl ??)) normalize nodelta #H @H |
---|
1986 | | 15: #ty #l #e #Hsim |
---|
1987 | @(exec_expr_expr_elim … Hsim) #v #tr normalize nodelta @conj // |
---|
1988 | | 16: * |
---|
1989 | [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
1990 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
1991 | #ty normalize in ⊢ (% → ?); |
---|
1992 | [ 3,4,13: @False_ind |
---|
1993 | | *: #_ normalize #a1 #Habsurd @Habsurd ] |
---|
1994 | ] qed. |
---|
1995 | |
---|
1996 | |
---|
1997 | |
---|
1998 | (* |
---|
1999 | lemma related_globals_exprlist_simulation : ∀ge,ge',en,m. |
---|
2000 | related_globals ? fundef_switch_removal ge ge' → |
---|
2001 | ∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args). |
---|
2002 | #ge #ge' #en #m #Hrelated #args |
---|
2003 | elim args |
---|
2004 | [ 1: /3/ |
---|
2005 | | 2: #hd #tl #Hind normalize |
---|
2006 | elim (sim_related_globals ge ge' en m Hrelated) |
---|
2007 | #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd) |
---|
2008 | cases (exec_expr ge en m hd) |
---|
2009 | [ 2: #error #_ @SimFail /2 by refl, ex_intro/ |
---|
2010 | | 1: * #val_hd #trace_hd normalize nodelta |
---|
2011 | cases Hind |
---|
2012 | [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/ |
---|
2013 | | 1: cases (exec_exprlist ge en m tl) |
---|
2014 | [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/ |
---|
2015 | | 1: * #values #trace #H >(H 〈values, trace〉 (refl ??)) |
---|
2016 | normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H2 |
---|
2017 | cases Hexec_hd |
---|
2018 | [ 2: * #error #Habsurd destruct (Habsurd) |
---|
2019 | | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ] |
---|
2020 | ] ] ] ] qed. |
---|
2021 | *) |
---|
2022 | |
---|
2023 | (* The return type of any function is invariant under switch removal *) |
---|
2024 | lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f. |
---|
2025 | #f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl |
---|
2026 | qed. |
---|
2027 | |
---|
2028 | (* Similar stuff for fundefs *) |
---|
2029 | lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd). |
---|
2030 | * // qed. |
---|
2031 | |
---|
2032 | (* |
---|
2033 | lemma expr_fresh_lift : |
---|
2034 | ∀e,u,id. |
---|
2035 | fresh_for_expression e u → |
---|
2036 | fresh_for_univ SymbolTag id u → |
---|
2037 | fresh_for_univ SymbolTag (max_of_expr e id) u. |
---|
2038 | #e #u #id |
---|
2039 | normalize in match (fresh_for_expression e u); |
---|
2040 | #H1 #H2 |
---|
2041 | >max_of_expr_rewrite |
---|
2042 | normalize in match (fresh_for_univ ???); |
---|
2043 | cases (max_of_expr e ?) in H1; #p #H1 |
---|
2044 | cases id in H2; #p' #H2 |
---|
2045 | normalize nodelta |
---|
2046 | cases (leb p p') normalize nodelta |
---|
2047 | [ 1: @H2 | 2: @H1 ] |
---|
2048 | qed. *) |
---|
2049 | |
---|
2050 | lemma while_fresh_lift : ∀e,s,cl,u. |
---|
2051 | fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s cl) u. |
---|
2052 | #e #s #cl * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ???)); |
---|
2053 | cases (max_of_expr e) #e cases (max_of_statement s) #s normalize |
---|
2054 | cases (leb e s) try /2/ |
---|
2055 | qed. |
---|
2056 | |
---|
2057 | (* |
---|
2058 | lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0). |
---|
2059 | #e0 #s0 #us0 normalize |
---|
2060 | cases (switch_removal s0 us0) * #body #newvars #u' normalize // |
---|
2061 | qed.*) |
---|
2062 | |
---|
2063 | lemma dowhile_fresh_lift : ∀e,s,u. |
---|
2064 | fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u. |
---|
2065 | #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??)); |
---|
2066 | cases (max_of_expr e) #e cases (max_of_statement s) #s normalize |
---|
2067 | cases (leb e s) try /2/ |
---|
2068 | qed. |
---|
2069 | (* |
---|
2070 | lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0). |
---|
2071 | #e0 #s0 #us0 normalize |
---|
2072 | cases (switch_removal s0 us0) * #body #newvars #u' normalize // |
---|
2073 | qed.*) |
---|
2074 | |
---|
2075 | lemma for_fresh_lift : ∀cond,step,body,u. |
---|
2076 | fresh_for_statement step u → |
---|
2077 | fresh_for_statement body u → |
---|
2078 | fresh_for_expression cond u → |
---|
2079 | fresh_for_statement (Sfor Sskip cond step body) u. |
---|
2080 | #cond #step #body #u |
---|
2081 | whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????)); |
---|
2082 | cases (max_of_statement step) #s |
---|
2083 | cases (max_of_statement body) #b |
---|
2084 | cases (max_of_expr cond) #c |
---|
2085 | whd in match (max_of_statement Sskip); |
---|
2086 | >(max_id_commutative least_identifier) |
---|
2087 | >max_id_one_neutral normalize nodelta |
---|
2088 | normalize elim u #u |
---|
2089 | cases (leb s b) cases (leb c b) cases (leb c s) try /2/ |
---|
2090 | qed. |
---|
2091 | |
---|
2092 | (* |
---|
2093 | lemma for_commute : ∀e,stm1,stm2,u,uA. |
---|
2094 | (uA=\snd (switch_removal stm1 u)) → |
---|
2095 | sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)). |
---|
2096 | #e #stm1 #stm2 #u #uA #HuA |
---|
2097 | whd in match (sw_rem (Sfor ????) u); |
---|
2098 | whd in match (switch_removal ??); |
---|
2099 | destruct |
---|
2100 | normalize in match (\snd (switch_removal Sskip u)); |
---|
2101 | whd in match (sw_rem stm1 u); |
---|
2102 | cases (switch_removal stm1 u) |
---|
2103 | * #stm1' #fresh_vars #uA normalize nodelta |
---|
2104 | whd in match (sw_rem stm2 uA); |
---|
2105 | cases (switch_removal stm2 uA) |
---|
2106 | * #stm2' #fresh_vars2 #uB normalize nodelta |
---|
2107 | // |
---|
2108 | qed.*) |
---|
2109 | |
---|
2110 | (* |
---|
2111 | lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf. |
---|
2112 | * |
---|
2113 | [ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip)) |
---|
2114 | | 2: #e1 #e2 #u #_ |
---|
2115 | whd in match (sw_rem ??); |
---|
2116 | whd in match (is_Sskip ?); |
---|
2117 | try /2 by refl, ex_intro/ |
---|
2118 | | 3: #ret #f #args #u |
---|
2119 | whd in match (sw_rem ??); |
---|
2120 | whd in match (is_Sskip ?); |
---|
2121 | try /2 by refl, ex_intro/ |
---|
2122 | | 4: #s1 #s2 #u |
---|
2123 | whd in match (sw_rem ??); |
---|
2124 | whd in match (switch_removal ??); |
---|
2125 | cases (switch_removal ? ?) * #a #b #c #d normalize nodelta |
---|
2126 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
2127 | whd in match (is_Sskip ?); |
---|
2128 | try /2 by refl, ex_intro/ |
---|
2129 | | 5: #e #s1 #s2 #u #_ |
---|
2130 | whd in match (sw_rem ??); |
---|
2131 | whd in match (switch_removal ??); |
---|
2132 | cases (switch_removal ? ?) * #a #b #c normalize nodelta |
---|
2133 | cases (switch_removal ? ?) * #e #f #h normalize nodelta |
---|
2134 | whd in match (is_Sskip ?); |
---|
2135 | try /2 by refl, ex_intro/ |
---|
2136 | | 6,7: #e #s #u #_ |
---|
2137 | whd in match (sw_rem ??); |
---|
2138 | whd in match (switch_removal ??); |
---|
2139 | cases (switch_removal ? ?) * #a #b #c normalize nodelta |
---|
2140 | whd in match (is_Sskip ?); |
---|
2141 | try /2 by refl, ex_intro/ |
---|
2142 | | 8: #s1 #e #s2 #s3 #u #_ |
---|
2143 | whd in match (sw_rem ??); |
---|
2144 | whd in match (switch_removal ??); |
---|
2145 | cases (switch_removal ? ?) * #a #b #c normalize nodelta |
---|
2146 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
2147 | cases (switch_removal ? ?) * #i #j #k normalize nodelta |
---|
2148 | whd in match (is_Sskip ?); |
---|
2149 | try /2 by refl, ex_intro/ |
---|
2150 | | 9,10: #u #_ |
---|
2151 | whd in match (is_Sskip ?); |
---|
2152 | try /2 by refl, ex_intro/ |
---|
2153 | | 11: #e #u #_ |
---|
2154 | whd in match (is_Sskip ?); |
---|
2155 | try /2 by refl, ex_intro/ |
---|
2156 | | 12: #e #ls #u #_ |
---|
2157 | whd in match (sw_rem ??); |
---|
2158 | whd in match (switch_removal ??); |
---|
2159 | cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta |
---|
2160 | cases (fresh ??) #e #f normalize nodelta |
---|
2161 | normalize in match (simplify_switch ???); |
---|
2162 | cases (fresh ? f) #g #h normalize nodelta |
---|
2163 | cases (produce_cond ????) * #k #l #m normalize nodelta |
---|
2164 | whd in match (is_Sskip ?); |
---|
2165 | try /2 by refl, ex_intro/ |
---|
2166 | | 13,15: #lab #st #u #_ |
---|
2167 | whd in match (sw_rem ??); |
---|
2168 | whd in match (switch_removal ??); |
---|
2169 | cases (switch_removal ? ?) * #a #b #c normalize nodelta |
---|
2170 | whd in match (is_Sskip ?); |
---|
2171 | try /2 by refl, ex_intro/ |
---|
2172 | | 14: #lab #u |
---|
2173 | whd in match (is_Sskip ?); |
---|
2174 | try /2 by refl, ex_intro/ ] |
---|
2175 | qed. |
---|
2176 | *) |
---|
2177 | |
---|
2178 | (* |
---|
2179 | lemma sw_rem_commute : ∀stm,u. |
---|
2180 | (\fst (\fst (switch_removal stm u))) = sw_rem stm u. |
---|
2181 | #stm #u whd in match (sw_rem stm u); // qed. |
---|
2182 | *) |
---|
2183 | |
---|
2184 | lemma fresh_for_statement_inv : |
---|
2185 | ∀u,s. fresh_for_statement s u → |
---|
2186 | match u with |
---|
2187 | [ mk_universe p ⇒ le (p0 one) p ]. |
---|
2188 | * #p #s whd in match (fresh_for_statement ??); |
---|
2189 | cases (max_of_statement s) #s |
---|
2190 | normalize /2/ qed. |
---|
2191 | |
---|
2192 | lemma fresh_for_Sskip : |
---|
2193 | ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u. |
---|
2194 | #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. |
---|
2195 | |
---|
2196 | lemma fresh_for_Sbreak : |
---|
2197 | ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u. |
---|
2198 | #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. |
---|
2199 | |
---|
2200 | lemma fresh_for_Scontinue : |
---|
2201 | ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u. |
---|
2202 | #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. |
---|
2203 | |
---|
2204 | (* |
---|
2205 | lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉. |
---|
2206 | #s #u elim (switch_removal s u) * #res #fvs #u' |
---|
2207 | %{res} %{fvs} %{u'} // |
---|
2208 | qed. |
---|
2209 | |
---|
2210 | lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉. |
---|
2211 | #switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u' |
---|
2212 | %{res} %{fvs} %{u'} // |
---|
2213 | qed. |
---|
2214 | *) |
---|
2215 | |
---|
2216 | lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉. |
---|
2217 | #e #ls #u #exit_label cases (produce_cond e ls u exit_label) * |
---|
2218 | #s #lab #u' %{s} %{lab} %{u'} // |
---|
2219 | qed. |
---|
2220 | |
---|
2221 | (* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *) |
---|
2222 | lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false. |
---|
2223 | * * * |
---|
2224 | [ 1,5,9: #H @(False_ind … (H (refl ??))) |
---|
2225 | | *: #_ normalize @refl ] |
---|
2226 | qed. |
---|
2227 | |
---|
2228 | lemma exec_expr_int : ∀ge,e,m,expr. |
---|
2229 | (∃sz,n,tr. exec_expr ge e m expr = (OK ? 〈Vint sz n, tr〉)) ∨ (∀sz,n,tr. exec_expr ge e m expr ≠ (OK ? 〈Vint sz n, tr〉)). |
---|
2230 | #ge #e #m #expr cases (exec_expr ge e m expr) |
---|
2231 | [ 2: #error %2 #sz #n #tr % #H destruct (H) |
---|
2232 | | 1: * #val #trace cases val |
---|
2233 | [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl |
---|
2234 | | 3: #fl | 4: | 5: #ptr ] |
---|
2235 | %2 #sz #n #tr % #H destruct (H) |
---|
2236 | ] qed. |
---|
2237 | |
---|
2238 | lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed. |
---|
2239 | |
---|
2240 | lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c. |
---|
2241 | #A #B #a #b * #a' #b' #H destruct @refl |
---|
2242 | qed. |
---|
2243 | |
---|
2244 | lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c. |
---|
2245 | #A #B #a #b * #a' #b' #H destruct @refl |
---|
2246 | qed. |
---|
2247 | |
---|
2248 | (* Main theorem. To be ported and completed to memory injections. TODO *) |
---|
2249 | theorem switch_removal_correction : |
---|
2250 | ∀ge,ge',s1, s1', tr, s2. |
---|
2251 | switch_removal_globals ? fundef_switch_removal ge ge' → |
---|
2252 | switch_state_sim ge s1 s1' → |
---|
2253 | exec_step ge s1 = Value … 〈tr,s2〉 → |
---|
2254 | eventually ge' (λs2'. switch_state_sim ge s2 s2') s1' tr. |
---|
2255 | #ge #ge' #st1 #st1' #tr #st2 #Hrelated #Hsim_state |
---|
2256 | inversion Hsim_state |
---|
2257 | [ 1: (* regular state *) |
---|
2258 | #sss_statement #sss_result #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars |
---|
2259 | #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_mem_hyp |
---|
2260 | #sss_env_hyp #sss_result_hyp #sss_k_hyp #Hext_fresh_for_ge |
---|
2261 | elim (sim_related_globals … ge ge' |
---|
2262 | sss_env sss_m sss_env_ext sss_m_ext sss_new_vars |
---|
2263 | sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge) |
---|
2264 | #Hsim_expr #Hsim_lvalue #Hst1_eq #Hst1_eq' #_ |
---|
2265 | cases sss_statement in sss_lu_fresh sss_result_hyp; |
---|
2266 | (* Perform the intros for the statements *) |
---|
2267 | [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body |
---|
2268 | | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body |
---|
2269 | | 14: #lab | 15: #cost #body ] |
---|
2270 | #sss_lu_fresh #sss_result_hyp |
---|
2271 | [ 1: (* Skip *) |
---|
2272 | whd in match (switch_removal ???) in sss_result_hyp; |
---|
2273 | <(some_inj ??? sss_result_hyp) |
---|
2274 | inversion sss_k_hyp normalize nodelta |
---|
2275 | [ 1: #fvs #Hfvs_eq #Hk #Hk' #_ #Hexec_step |
---|
2276 | @(eventually_now ????) whd in match (exec_step ??); |
---|
2277 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
2278 | >fn_return_simplify |
---|
2279 | whd in match (exec_step ??) in Hexec_step; |
---|
2280 | cases (fn_return sss_func) in Hexec_step; |
---|
2281 | [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain |
---|
2282 | | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] |
---|
2283 | normalize nodelta |
---|
2284 | whd in ⊢ ((??%?) → ?); |
---|
2285 | [ 1: #H destruct (H) %{(Returnstate Vundef Kstop (free_list sss_m_ext (blocks_of_env sss_env_ext)))} |
---|
2286 | @conj try @refl %3{(map (ident×type) ident \fst sss_new_vars)} try // |
---|
2287 | %{(Returnstate Vundef Kstop (free1_list sss_m_ext (blocks_of_env sss_env_ext)))} @conj try // |
---|
2288 | normalize in Heq_env; destruct (Heq_env) |
---|
2289 | %3 // |
---|
2290 | (* cut (blocks_of_env e = blocks_of_env e') |
---|
2291 | [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl; |
---|
2292 | lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ] |
---|
2293 | #Heq >Heq %3 // *) |
---|
2294 | | *: #H destruct (H) ] |
---|
2295 | | 2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq |
---|
2296 | whd in match (ret ??) in Heq; destruct (Heq) |
---|
2297 | @(eventually_now ????) whd in match (exec_step ??); |
---|
2298 | %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try // |
---|
2299 | %1 try // |
---|
2300 | | 3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq |
---|
2301 | @(eventually_now ????) whd in match (exec_step ??); |
---|
2302 | whd in match (ret ??) in Heq; destruct (Heq) |
---|
2303 | %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try // |
---|
2304 | >while_commute %1 try // |
---|
2305 | | 4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq |
---|
2306 | @(eventually_now ????) whd in match (exec_step ??); |
---|
2307 | lapply (Hexpr_related e0) |
---|
2308 | cases (exec_expr ge e m e0) in Heq; |
---|
2309 | [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
2310 | | 1: * #b #tr whd in match (m_bind ?????); #Heq |
---|
2311 | * |
---|
2312 | [ 2: * #error #Habsurd destruct (Habsurd) |
---|
2313 | | 1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉))) |
---|
2314 | whd in match (bindIO ??????); |
---|
2315 | cases (exec_bool_of_val b (typeof e0)) in Heq; |
---|
2316 | [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd) |
---|
2317 | | 1: * whd in match (bindIO ??????); #Heq destruct (Heq) |
---|
2318 | whd in match (bindIO ??????); |
---|
2319 | [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)} |
---|
2320 | @conj // >dowhile_commute %1 try // |
---|
2321 | | 2: %{(State (function_switch_removal f) Sskip k0' e m)} |
---|
2322 | @conj // %1{us} try // |
---|
2323 | @(fresh_for_Sskip … Hus_fresh) |
---|
2324 | ] ] ] ] |
---|
2325 | | 5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq |
---|
2326 | @(eventually_now ????) whd in match (exec_step ??); |
---|
2327 | whd in match (ret ??) in Heq; destruct |
---|
2328 | %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)} |
---|
2329 | @conj try // %1{u} try // |
---|
2330 | | 6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq |
---|
2331 | @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq; |
---|
2332 | destruct (Heq) |
---|
2333 | %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)} |
---|
2334 | @conj try // %1 |
---|
2335 | [ 2: @swc_for3 // |
---|
2336 | | 1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ] |
---|
2337 | | 7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq |
---|
2338 | @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq; |
---|
2339 | destruct (Heq) |
---|
2340 | %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)} |
---|
2341 | @conj try // <(for_commute ??? u uA) try // %1 |
---|
2342 | [ 2: assumption |
---|
2343 | | 1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ] |
---|
2344 | | 8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?); |
---|
2345 | #Heq @(eventually_now ????) whd in match (exec_step ??); |
---|
2346 | destruct (Heq) |
---|
2347 | %{(State (function_switch_removal f) Sskip k0' e m)} @conj // |
---|
2348 | %1{u} // |
---|
2349 | | 9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq |
---|
2350 | @(eventually_now ????) whd in match (exec_step ??); |
---|
2351 | >fn_return_simplify cases (fn_return f) in Heq; |
---|
2352 | [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain |
---|
2353 | | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ] |
---|
2354 | normalize nodelta |
---|
2355 | [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H) |
---|
2356 | %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))} |
---|
2357 | @conj try // %3 destruct // |
---|
2358 | | *: #H destruct (H) ] |
---|
2359 | ] |
---|
2360 | | 2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????) |
---|
2361 | whd in match (exec_step ??); |
---|
2362 | cases lhs in Hu_fresh Heq; #lhs #lhs_type |
---|
2363 | cases (Hlvalue_related lhs lhs_type) |
---|
2364 | whd in match (exec_lvalue ge e m (Expr ??)); |
---|
2365 | whd in match (exec_lvalue ge' e m (Expr ??)); |
---|
2366 | [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ] |
---|
2367 | cases (exec_lvalue' ge e m lhs lhs_type) |
---|
2368 | [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd) |
---|
2369 | | 1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??)) |
---|
2370 | whd in match (m_bind ?????); |
---|
2371 | cases (Hexpr_related rhs) |
---|
2372 | [ 2: * #error #Hfail >Hfail #_ |
---|
2373 | whd in match (bindIO ??????); #Habsurd destruct (Habsurd) |
---|
2374 | | 1: cases (exec_expr ge e m rhs) |
---|
2375 | [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd) |
---|
2376 | | 1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??)) |
---|
2377 | whd in match (bindIO ??????) in ⊢ (% → % → %); |
---|
2378 | cases (opt_to_io io_out io_in ???) |
---|
2379 | [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd) |
---|
2380 | | 3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd) |
---|
2381 | | 2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq) |
---|
2382 | %{(State (function_switch_removal f) Sskip k' e mem)} |
---|
2383 | whd in match (bindIO ??????); @conj // |
---|
2384 | %1{u} try // @(fresh_for_Sskip … Hfresh) |
---|
2385 | ] ] ] ] |
---|
2386 | | 3: (* Scall *) normalize nodelta #Heq @(eventually_now ????) |
---|
2387 | whd in match (exec_step ??); |
---|
2388 | cases (Hexpr_related func) in Heq; |
---|
2389 | [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2390 | | 1: cases (exec_expr ge e m func) |
---|
2391 | [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2392 | | 1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??)) |
---|
2393 | whd in match (m_bind ?????); normalize nodelta |
---|
2394 | lapply (related_globals_exprlist_simulation ge ge' e m Hrelated) |
---|
2395 | #Hexprlist_sim cases (Hexprlist_sim args) |
---|
2396 | [ 2: * #error #Hfail >Hfail |
---|
2397 | whd in match (bindIO ??????); #Habsurd destruct (Habsurd) |
---|
2398 | | 1: cases (exec_exprlist ge e m args) |
---|
2399 | [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd) |
---|
2400 | | 1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??)) |
---|
2401 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2402 | elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval) |
---|
2403 | cases (find_funct clight_fundef ge fval) |
---|
2404 | [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??)) |
---|
2405 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2406 | >fundef_type_simplify |
---|
2407 | cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func)) |
---|
2408 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2409 | | 1: #Heq whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2410 | cases retv normalize nodelta |
---|
2411 | [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct |
---|
2412 | %{(Callstate (fundef_switch_removal clfd) values |
---|
2413 | (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)} |
---|
2414 | @conj try // %2 try // @swc_call // |
---|
2415 | | 2: * #retval_ed #retval_type |
---|
2416 | whd in match (exec_lvalue ge ???); |
---|
2417 | whd in match (exec_lvalue ge' ???); |
---|
2418 | elim (Hlvalue_related retval_ed retval_type) |
---|
2419 | [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2420 | | 1: cases (exec_lvalue' ge e m retval_ed retval_type) |
---|
2421 | [ 2: #error #_ whd in match (m_bind ?????); #Habsurd |
---|
2422 | destruct (Habsurd) |
---|
2423 | | 1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??)) |
---|
2424 | whd in match (m_bind ?????) in ⊢ (% → %); |
---|
2425 | #Heq destruct (Heq) |
---|
2426 | %{(Callstate (fundef_switch_removal clfd) values |
---|
2427 | (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉) |
---|
2428 | (function_switch_removal f) e k') m)} |
---|
2429 | @conj try // |
---|
2430 | %2 @swc_call // |
---|
2431 | ] ] ] ] |
---|
2432 | | 1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %); |
---|
2433 | whd in match (bindIO ??????); #Habsurd destruct (Habsurd) |
---|
2434 | ] ] ] ] ] |
---|
2435 | | 4: (* Ssequence *) normalize nodelta |
---|
2436 | whd in match (ret ??) in ⊢ (% → ?); #Heq |
---|
2437 | @(eventually_now ????) |
---|
2438 | %{(State (function_switch_removal f) |
---|
2439 | (\fst (\fst (switch_removal stm1 u))) |
---|
2440 | (Kseq (\fst (\fst (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)} |
---|
2441 | @conj |
---|
2442 | [ 2: destruct (Heq) %1 |
---|
2443 | [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // |
---|
2444 | | 2: @swc_seq try // @switch_removal_fresh |
---|
2445 | elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ] |
---|
2446 | | 1: whd in match (sw_rem ??); whd in match (switch_removal ??); |
---|
2447 | cases (switch_removal stm1 u) |
---|
2448 | * #stm1' #fresh_vars #u' normalize nodelta |
---|
2449 | cases (switch_removal stm2 u') |
---|
2450 | * #stm2' #fresh_vars2 #u'' normalize nodelta |
---|
2451 | whd in match (exec_step ??); |
---|
2452 | destruct (Heq) @refl |
---|
2453 | ] |
---|
2454 | | 5: (* If-then-else *) normalize nodelta |
---|
2455 | whd in match (ret ??) in ⊢ (% → ?); #Heq |
---|
2456 | @(eventually_now ????) whd in match (sw_rem ??); |
---|
2457 | whd in match (switch_removal ??); |
---|
2458 | elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta |
---|
2459 | elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta |
---|
2460 | whd in match (exec_step ??); |
---|
2461 | cases (Hexpr_related cond) in Heq; |
---|
2462 | [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2463 | | 1: cases (exec_expr ge e m cond) |
---|
2464 | [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2465 | | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??)) |
---|
2466 | whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %); |
---|
2467 | cases (exec_bool_of_val condval (typeof cond)) |
---|
2468 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2469 | | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval |
---|
2470 | destruct (Heq_condval) whd in match (bindIO ??????); |
---|
2471 | normalize nodelta |
---|
2472 | [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try // |
---|
2473 | cut (iftrue' = (\fst (\fst (switch_removal iftrue u)))) |
---|
2474 | [ 1: >Hiftrue_eq normalize // ] |
---|
2475 | #Hrewrite >Hrewrite %1 |
---|
2476 | elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) // |
---|
2477 | | 2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try // |
---|
2478 | cut (iffalse' = (\fst (\fst (switch_removal iffalse uA)))) |
---|
2479 | [ 1: >Hiffalse_eq // ] |
---|
2480 | #Hrewrite >Hrewrite %1 try // |
---|
2481 | cut (uA = (\snd (switch_removal iftrue u))) |
---|
2482 | [ 1: >Hiftrue_eq // |
---|
2483 | | 2: #Heq_uA >Heq_uA |
---|
2484 | elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) |
---|
2485 | #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh // |
---|
2486 | ] ] ] ] ] |
---|
2487 | | 6: (* While loop *) normalize nodelta |
---|
2488 | whd in match (ret ??) in ⊢ (% → ?); #Heq |
---|
2489 | @(eventually_now ????) whd in match (sw_rem ??); |
---|
2490 | whd in match (switch_removal ??); |
---|
2491 | elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta |
---|
2492 | whd in match (exec_step ??); |
---|
2493 | cases (Hexpr_related cond) in Heq; |
---|
2494 | [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2495 | | 1: cases (exec_expr ge e m cond) |
---|
2496 | [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2497 | | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??)) |
---|
2498 | whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %); |
---|
2499 | cases (exec_bool_of_val condval (typeof cond)) |
---|
2500 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2501 | | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval |
---|
2502 | destruct (Heq_condval) whd in match (bindIO ??????); |
---|
2503 | normalize nodelta |
---|
2504 | [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try // |
---|
2505 | cut (body' = (\fst (\fst (switch_removal body u)))) |
---|
2506 | [ 1: >Hbody_eq // ] |
---|
2507 | #Hrewrite >Hrewrite %1 |
---|
2508 | [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) // |
---|
2509 | | 2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ] |
---|
2510 | | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj // |
---|
2511 | %1{u} try // @(fresh_for_Sskip … Hu_fresh) |
---|
2512 | ] ] ] ] |
---|
2513 | | 7: (* Dowhile loop *) normalize nodelta |
---|
2514 | whd in match (ret ??) in ⊢ (% → ?); #Heq |
---|
2515 | @(eventually_now ????) whd in match (sw_rem ??); |
---|
2516 | whd in match (switch_removal ??); |
---|
2517 | elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta |
---|
2518 | whd in match (exec_step ??); |
---|
2519 | destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj |
---|
2520 | try // |
---|
2521 | cut (body' = (\fst (\fst (switch_removal body u)))) |
---|
2522 | [ 1: >Hbody_eq // ] |
---|
2523 | #Hrewrite >Hrewrite %1 |
---|
2524 | [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) // |
---|
2525 | | 2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ] |
---|
2526 | | 8: (* For loop *) normalize nodelta |
---|
2527 | whd in match (ret ??) in ⊢ (% → ?); #Heq |
---|
2528 | @(eventually_now ????) whd in match (sw_rem ??); |
---|
2529 | whd in match (switch_removal ??); |
---|
2530 | cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip |
---|
2531 | [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta |
---|
2532 | elim (switch_removal_eq step u) #step' * #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta |
---|
2533 | elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta |
---|
2534 | whd in match (exec_step ??); |
---|
2535 | cases (Hexpr_related cond) |
---|
2536 | [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2537 | | 1: cases (exec_expr ge e m cond) |
---|
2538 | [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2539 | | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??)) |
---|
2540 | whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %); |
---|
2541 | cases (exec_bool_of_val condval (typeof cond)) |
---|
2542 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2543 | | 1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval |
---|
2544 | destruct (Heq_condval) |
---|
2545 | [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj |
---|
2546 | try // |
---|
2547 | cut (body' = (\fst (\fst (switch_removal body uA)))) |
---|
2548 | [ 1: >Hbody_eq // ] |
---|
2549 | #Hrewrite >Hrewrite |
---|
2550 | cut (uA = (\snd (switch_removal step u))) |
---|
2551 | [ 1: >Hstep_eq // ] #HuA |
---|
2552 | elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * * |
---|
2553 | #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1 |
---|
2554 | [ 1: >HuA @switch_removal_fresh assumption |
---|
2555 | | 2: cut (step' = (\fst (\fst (switch_removal step u)))) |
---|
2556 | [ >Hstep_eq // ] |
---|
2557 | #Hstep >Hstep @swc_for2 try assumption |
---|
2558 | @for_fresh_lift try assumption ] |
---|
2559 | | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj |
---|
2560 | try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption |
---|
2561 | ] ] ] ] |
---|
2562 | | 2: #Heq |
---|
2563 | elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta |
---|
2564 | elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta |
---|
2565 | elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta |
---|
2566 | whd in match (exec_step ??); |
---|
2567 | cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ] |
---|
2568 | #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip) |
---|
2569 | whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta |
---|
2570 | whd in match (ret ??); destruct (Heq) |
---|
2571 | %{(State (function_switch_removal f) (\fst (\fst (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)} |
---|
2572 | @conj try // |
---|
2573 | cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep' |
---|
2574 | cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody' |
---|
2575 | <for_commute [ 2: >Hstep_eq // ] |
---|
2576 | elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * * |
---|
2577 | #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption |
---|
2578 | @swc_seq try // @for_fresh_lift |
---|
2579 | cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq |
---|
2580 | >HuA_eq @switch_removal_fresh assumption |
---|
2581 | ] |
---|
2582 | | 9: (* break *) normalize nodelta |
---|
2583 | inversion Hsim_cont |
---|
2584 | [ 1: #Hk #Hk' #_ |
---|
2585 | | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_ |
---|
2586 | | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_ |
---|
2587 | | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_ |
---|
2588 | | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_ |
---|
2589 | | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_ |
---|
2590 | | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_ |
---|
2591 | | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ] |
---|
2592 | normalize nodelta #H try (destruct (H)) |
---|
2593 | whd in match (ret ??) in H; destruct (H) |
---|
2594 | @(eventually_now ????) |
---|
2595 | [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: // | 2,4: %1{u} // ] |
---|
2596 | | 2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ] |
---|
2597 | | 10: (* Continue *) normalize nodelta |
---|
2598 | inversion Hsim_cont |
---|
2599 | [ 1: #Hk #Hk' #_ |
---|
2600 | | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_ |
---|
2601 | | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_ |
---|
2602 | | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_ |
---|
2603 | | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_ |
---|
2604 | | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_ |
---|
2605 | | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_ |
---|
2606 | | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ] |
---|
2607 | normalize nodelta #H try (destruct (H)) |
---|
2608 | @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H; |
---|
2609 | destruct (H) |
---|
2610 | [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption |
---|
2611 | | 2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try // |
---|
2612 | >while_commute %1{u0} try assumption |
---|
2613 | | 3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H; |
---|
2614 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2615 | | 1: * #condval #trace whd in match (m_bind ?????); |
---|
2616 | #Heq * |
---|
2617 | [ 2: * #error #Habsurd destruct (Habsurd) |
---|
2618 | | 1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) -Hexec #Hexec >Hexec |
---|
2619 | whd in match (bindIO ??????); |
---|
2620 | cases (exec_bool_of_val condval (typeof cond)) in Heq; |
---|
2621 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2622 | | 1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????); |
---|
2623 | [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)} |
---|
2624 | @conj try // >dowhile_commute %1{u0} assumption |
---|
2625 | | 2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // |
---|
2626 | %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ] |
---|
2627 | ] ] ] |
---|
2628 | | 4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0} |
---|
2629 | try // @(fresh_for_Scontinue … Hfor_fresh) |
---|
2630 | | 5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)} |
---|
2631 | @conj try // %1{u0} |
---|
2632 | elim (substatement_fresh … Hfor_fresh) * * try // |
---|
2633 | #HSskip #Hcond #Hstep #Hbody |
---|
2634 | @swc_for3 assumption |
---|
2635 | | 6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // |
---|
2636 | %1{u} try // |
---|
2637 | ] |
---|
2638 | | 11: (* Sreturn *) normalize nodelta #Heq |
---|
2639 | @(eventually_now ????) |
---|
2640 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2641 | cases retval in Heq; normalize nodelta |
---|
2642 | [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta |
---|
2643 | whd in match (ret ??) in ⊢ (% → %); |
---|
2644 | [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty' |
---|
2645 | | 7: #id #fl | 8: #id #fl | 9: #rg #id ] |
---|
2646 | #H destruct (H) |
---|
2647 | %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))} |
---|
2648 | @conj [ 1: // | 2: %3 @call_cont_swremoval // ] |
---|
2649 | | 2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta |
---|
2650 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
2651 | | 2: #_ elim (Hexpr_related expr) |
---|
2652 | [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2653 | | 1: cases (exec_expr ??? expr) |
---|
2654 | [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2655 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) |
---|
2656 | #Hrewrite >Hrewrite |
---|
2657 | whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
2658 | #Heq destruct (Heq) |
---|
2659 | %{(Returnstate (\fst a) (call_cont k') (free_list m (blocks_of_env e)))} |
---|
2660 | @conj [ 1: // | 2: %3 @call_cont_swremoval // ] |
---|
2661 | ] ] ] ] |
---|
2662 | | 12: (* Sswitch. Main proof case. *) normalize nodelta |
---|
2663 | (* Case analysis on the outcome of the tested expression *) |
---|
2664 | cases (exec_expr_int ge e m cond) |
---|
2665 | [ 2: cases (exec_expr ge e m cond) |
---|
2666 | [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd) |
---|
2667 | | 1: * #val #trace cases val |
---|
2668 | [ 1: | 2: #condsz #condv | 3: #condf | 4: #condrg | 5: #condptr ] |
---|
2669 | whd in match (m_bind ?????); |
---|
2670 | [ 1,3,4,5: #_ #Habsurd destruct (Habsurd) |
---|
2671 | | 2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ] ] |
---|
2672 | ] |
---|
2673 | * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond |
---|
2674 | whd in match (m_bind ?????); #Heq |
---|
2675 | destruct (Heq) |
---|
2676 | @eventually_later |
---|
2677 | whd in match (sw_rem (Sswitch cond switchcases) u); |
---|
2678 | whd in match (switch_removal (Sswitch cond switchcases) u); |
---|
2679 | elim (switch_removal_branches_eq switchcases u) |
---|
2680 | #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta |
---|
2681 | cut (uv1 = (\snd (switch_removal_branches switchcases u))) |
---|
2682 | [ 1: >Hsrb_eq // ] #Huv1_eq |
---|
2683 | cut (fresh_for_statement (Sswitch cond switchcases) uv1) |
---|
2684 | [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] -Huv1_eq #Huv1_eq |
---|
2685 | elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv2_eq normalize nodelta |
---|
2686 | whd in match (simplify_switch ???); |
---|
2687 | elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv3_eq normalize nodelta |
---|
2688 | lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq) |
---|
2689 | elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label) |
---|
2690 | #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta |
---|
2691 | #Huv4_eq |
---|
2692 | whd in match (exec_step ??); |
---|
2693 | %{(State (function_switch_removal f) |
---|
2694 | (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond) |
---|
2695 | (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)} |
---|
2696 | %{E0} @conj try @refl |
---|
2697 | %{tr} normalize in match (eq ???); @conj try // |
---|
2698 | (* execute the conditional *) |
---|
2699 | @eventually_later |
---|
2700 | (* lift the result of the previous case analysis from [ge] to [ge'] *) |
---|
2701 | whd in match (exec_step ??); |
---|
2702 | whd in match (exec_lvalue ????); |
---|
2703 | |
---|
2704 | >(exec_expr_related … Hexec_cond (Hexpr_related cond)) |
---|
2705 | |
---|
2706 | *) |
---|
2707 | |
---|
2708 | (* |
---|
2709 | lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr. |
---|
2710 | exec_expr ge e m cond = OK ? 〈v,tr〉 → |
---|
2711 | (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) → |
---|
2712 | exec_expr ge' e m cond = OK ? 〈v,tr〉. |
---|
2713 | #ge #ge' #e #m #cond #v #tr #H * |
---|
2714 | [ 1: #Hsim >(Hsim ? H) // |
---|
2715 | | 2: * #error >H #Habsurd destruct (Habsurd) ] |
---|
2716 | qed. *) |
---|
2717 | |
---|
2718 | (* |
---|
2719 | lemma switch_simulation : |
---|
2720 | ∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u. |
---|
2721 | switch_cont_sim k k' → |
---|
2722 | (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) → |
---|
2723 | fresh_for_statement (Sswitch cond switchcases) u → |
---|
2724 | ∃tr'. |
---|
2725 | (eventually ge' |
---|
2726 | (λs2':state |
---|
2727 | .switch_state_sim |
---|
2728 | (State f |
---|
2729 | (seq_of_labeled_statement (select_switch condsz condval switchcases)) |
---|
2730 | (Kswitch k) e m) s2') |
---|
2731 | (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m) |
---|
2732 | tr'). |
---|
2733 | #ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh |
---|
2734 | whd in match (sw_rem (Sswitch cond switchcases) u); |
---|
2735 | whd in match (switch_removal (Sswitch cond switchcases) u); |
---|
2736 | cases switchcases in Hfresh; |
---|
2737 | [ 1: #default_statement #Hfresh_for_default |
---|
2738 | whd in match (switch_removal_branches ??); |
---|
2739 | whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?); |
---|
2740 | elim (switch_removal_eq default_statement u) |
---|
2741 | #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq |
---|
2742 | normalize nodelta |
---|
2743 | cut (u' = (\snd (switch_removal default_statement u))) |
---|
2744 | [ 1: >Hdefault_statement_eq // ] #Heq_u' |
---|
2745 | cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u') |
---|
2746 | [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u' |
---|
2747 | lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u') |
---|
2748 | #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉)) |
---|
2749 | -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *) |
---|
2750 | normalize nodelta |
---|
2751 | whd in match (simplify_switch (Expr ??) ?? uv2); |
---|
2752 | lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2) |
---|
2753 | #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉)) |
---|
2754 | -Hfreshness #Heq_uv3 |
---|
2755 | normalize nodelta whd in match (add_starting_lbl_list ????); |
---|
2756 | lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3) |
---|
2757 | #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉)) |
---|
2758 | -Hfreshness #Heq_uv4 |
---|
2759 | normalize nodelta |
---|
2760 | @(eventually_later ge' ?? E0) |
---|
2761 | whd in match (exec_step ??); |
---|
2762 | %{(State (function_switch_removal f) |
---|
2763 | (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond) |
---|
2764 | (Kseq |
---|
2765 | (Ssequence |
---|
2766 | (Slabel default_lab (convert_break_to_goto default_statement' exit_label)) |
---|
2767 | (Slabel exit_label Sskip)) |
---|
2768 | k') e m)} @conj try // |
---|
2769 | @(eventually_later ge' ?? E0) |
---|
2770 | whd in match (exec_step ??); |
---|
2771 | |
---|
2772 | @chthulhu | @chthulhu |
---|
2773 | qed. *) |
---|
2774 | |
---|
2775 | |
---|
2776 | |
---|
2777 | |
---|