1 | include "Clight/Csyntax.ma". |
---|
2 | include "Clight/fresh.ma". |
---|
3 | include "common/Identifiers.ma". |
---|
4 | include "utilities/extralib.ma". |
---|
5 | include "Clight/Cexec.ma". |
---|
6 | include "Clight/CexecInd.ma". |
---|
7 | include "Clight/frontend_misc.ma". |
---|
8 | include "Clight/memoryInjections.ma". |
---|
9 | include "Clight/MemProperties.ma". |
---|
10 | include "basics/lists/list.ma". |
---|
11 | include "basics/lists/listb.ma". |
---|
12 | |
---|
13 | (* ----------------------------------------------------------------------------- |
---|
14 | ----------------------------------------------------------------------------*) |
---|
15 | |
---|
16 | (* ----------------------------------------------------------------------------- |
---|
17 | Documentation |
---|
18 | ----------------------------------------------------------------------------*) |
---|
19 | |
---|
20 | (* This file implements transformation of switches to linear sequences of |
---|
21 | * if/then/else. The implementation roughly follows the lines of the prototype. |
---|
22 | * /!\ We assume that the program is well-typed (the type of the evaluated |
---|
23 | * expression must match the constants on each branch of the switch). /!\ *) |
---|
24 | |
---|
25 | (* Documentation. Let the follwing be our input switch construct: |
---|
26 | // --------------------------------- |
---|
27 | switch(e) { |
---|
28 | case v1: |
---|
29 | stmt1 |
---|
30 | case v2: |
---|
31 | stmt2 |
---|
32 | . |
---|
33 | . |
---|
34 | . |
---|
35 | default: |
---|
36 | stmt_default |
---|
37 | } |
---|
38 | // --------------------------------- |
---|
39 | |
---|
40 | Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting |
---|
41 | the switch statement. In the absence of break, the execution falls through each case sequentially. |
---|
42 | |
---|
43 | Given such a statement, we produce an equivalent sequence of if-then-elses chained by gotos: |
---|
44 | |
---|
45 | // --------------------------------- |
---|
46 | fresh = e; |
---|
47 | if(fresh == v1) { |
---|
48 | stmt1'; |
---|
49 | goto lbl_case2; |
---|
50 | } |
---|
51 | if(fresh == v2) { |
---|
52 | lbl_case2: |
---|
53 | stmt2'; |
---|
54 | goto lbl_case2; |
---|
55 | } |
---|
56 | ... |
---|
57 | stmt_default'; |
---|
58 | exit_label: |
---|
59 | // --------------------------------- |
---|
60 | |
---|
61 | where stmt1', stmt2', ... stmt_default' are the statements where all top-level [break] statements |
---|
62 | were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels. |
---|
63 | *) |
---|
64 | |
---|
65 | |
---|
66 | (* ----------------------------------------------------------------------------- |
---|
67 | Definitions allowing to state that the program resulting of the transformation |
---|
68 | is switch-free. |
---|
69 | ---------------------------------------------------------------------------- *) |
---|
70 | |
---|
71 | (* Property of a Clight statement of containing no switch. Could be generalized into a kind of |
---|
72 | * statement_P, if useful elsewhere. *) |
---|
73 | let rec switch_free (st : statement) : Prop ≝ |
---|
74 | match st with |
---|
75 | [ Sskip ⇒ True |
---|
76 | | Sassign _ _ ⇒ True |
---|
77 | | Scall _ _ _ ⇒ True |
---|
78 | | Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2 |
---|
79 | | Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2 |
---|
80 | | Swhile e body ⇒ switch_free body |
---|
81 | | Sdowhile e body ⇒ switch_free body |
---|
82 | | Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3 |
---|
83 | | Sbreak ⇒ True |
---|
84 | | Scontinue ⇒ True |
---|
85 | | Sreturn _ ⇒ True |
---|
86 | | Sswitch _ _ ⇒ False |
---|
87 | | Slabel _ body ⇒ switch_free body |
---|
88 | | Sgoto _ ⇒ True |
---|
89 | | Scost _ body ⇒ switch_free body |
---|
90 | ]. |
---|
91 | |
---|
92 | (* Property of a list of labeled statements of being switch-free *) |
---|
93 | let rec branches_switch_free (sts : labeled_statements) : Prop ≝ |
---|
94 | match sts with |
---|
95 | [ LSdefault st => |
---|
96 | switch_free st |
---|
97 | | LScase _ _ st tl => |
---|
98 | switch_free st ∧ branches_switch_free tl |
---|
99 | ]. |
---|
100 | |
---|
101 | let rec branches_ind |
---|
102 | (sts : labeled_statements) |
---|
103 | (H : labeled_statements → Prop) |
---|
104 | (defcase : ∀st. H (LSdefault st)) |
---|
105 | (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝ |
---|
106 | match sts with |
---|
107 | [ LSdefault st ⇒ |
---|
108 | defcase st |
---|
109 | | LScase sz int st tl ⇒ |
---|
110 | indcase sz int st tl (branches_ind tl H defcase indcase) |
---|
111 | ]. |
---|
112 | |
---|
113 | (* ----------------------------------------------------------------------------- |
---|
114 | Switch-removal code for statements, functions and fundefs. |
---|
115 | ----------------------------------------------------------------------------*) |
---|
116 | |
---|
117 | (* Converts the directly accessible ("free") breaks to gotos toward the [lab] label. *) |
---|
118 | let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝ |
---|
119 | match st with |
---|
120 | [ Sbreak ⇒ |
---|
121 | Sgoto lab |
---|
122 | | Ssequence s1 s2 ⇒ |
---|
123 | Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab) |
---|
124 | | Sifthenelse e iftrue iffalse ⇒ |
---|
125 | Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab) |
---|
126 | | Sfor init e update body ⇒ |
---|
127 | Sfor (convert_break_to_goto init lab) e update body |
---|
128 | | Slabel l body ⇒ |
---|
129 | Slabel l (convert_break_to_goto body lab) |
---|
130 | | Scost cost body ⇒ |
---|
131 | Scost cost (convert_break_to_goto body lab) |
---|
132 | | _ ⇒ st |
---|
133 | ]. |
---|
134 | |
---|
135 | (* Converting breaks preserves switch-freeness. *) |
---|
136 | lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label). |
---|
137 | #s elim s // |
---|
138 | [ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ |
---|
139 | | 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ |
---|
140 | | 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize |
---|
141 | try @conj try @conj /3/ |
---|
142 | | 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/ |
---|
143 | | 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/ |
---|
144 | ] qed. |
---|
145 | |
---|
146 | (* (def_case : ident × sf_statement) *) |
---|
147 | |
---|
148 | let rec produce_cond |
---|
149 | (e : expr) |
---|
150 | (switch_cases : labeled_statements) |
---|
151 | (u : universe SymbolTag) |
---|
152 | (exit : label) on switch_cases : statement × label × (universe SymbolTag) ≝ |
---|
153 | match switch_cases with |
---|
154 | [ LSdefault st ⇒ |
---|
155 | let 〈lab,u1〉 ≝ fresh ? u in |
---|
156 | let st' ≝ convert_break_to_goto st exit in |
---|
157 | 〈Slabel lab st', lab, u1〉 |
---|
158 | | LScase sz tag st other_cases ⇒ |
---|
159 | let 〈sub_statements, sub_label, u1〉 ≝ produce_cond e other_cases u exit in |
---|
160 | let st' ≝ convert_break_to_goto st exit in |
---|
161 | let 〈lab, u2〉 ≝ fresh ? u1 in |
---|
162 | let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz tag) (typeof e))) (Tint I32 Signed) in |
---|
163 | let case_statement ≝ |
---|
164 | Sifthenelse test |
---|
165 | (Slabel lab (Ssequence st' (Sgoto sub_label))) |
---|
166 | Sskip |
---|
167 | in |
---|
168 | 〈Ssequence case_statement sub_statements, lab, u2〉 |
---|
169 | ]. |
---|
170 | |
---|
171 | definition simplify_switch ≝ |
---|
172 | λ(e : expr). |
---|
173 | λ(switch_cases : labeled_statements). |
---|
174 | λ(uv : universe SymbolTag). |
---|
175 | let 〈exit_label, uv1〉 ≝ fresh ? uv in |
---|
176 | let 〈result, useless_label, uv2〉 ≝ produce_cond e switch_cases uv1 exit_label in |
---|
177 | 〈Ssequence result (Slabel exit_label Sskip), uv2〉. |
---|
178 | |
---|
179 | lemma produce_cond_switch_free : ∀l.∀H:branches_switch_free l.∀e,lab,u.switch_free (\fst (\fst (produce_cond e l u lab))). |
---|
180 | #l @(labeled_statements_ind … l) |
---|
181 | [ 1: #s #Hsf #e #lab #u normalize cases (fresh ??) #lab0 #u1 |
---|
182 | normalize in Hsf ⊢ %; @(convert_break_lift … Hsf) |
---|
183 | | 2: #sz #i #hd #tl #Hind whd in ⊢ (% → ?); * #Hsf_hd #Hsf_tl |
---|
184 | #e #lab #u normalize |
---|
185 | lapply (Hind Hsf_tl e lab u) |
---|
186 | cases (produce_cond e tl u lab) * #cond #lab' #u' #Hsf normalize nodelta |
---|
187 | cases (fresh ??) #lab0 #u2 normalize nodelta |
---|
188 | normalize try @conj try @conj try @conj try // |
---|
189 | @(convert_break_lift … Hsf_hd) |
---|
190 | ] qed. |
---|
191 | |
---|
192 | lemma simplify_switch_switch_free : ∀e,l. ∀H:branches_switch_free l. ∀u. switch_free (\fst (simplify_switch e l u)). |
---|
193 | #e #l cases l |
---|
194 | [ 1: #def normalize #H #u cases (fresh ? u) #exit_label #uv normalize cases (fresh ? uv) #lab #uv' normalize nodelta |
---|
195 | whd @conj whd |
---|
196 | [ 1: @convert_break_lift assumption |
---|
197 | | 2: @I ] |
---|
198 | | 2: #sz #i #case #tl normalize * #Hsf #Hsftl #u |
---|
199 | cases (fresh ? u) #exit_label #uv1 normalize nodelta |
---|
200 | lapply (produce_cond_switch_free tl Hsftl e exit_label uv1) |
---|
201 | cases (produce_cond e tl uv1 exit_label) |
---|
202 | * #cond #lab #u1 #Hsf_cond normalize nodelta |
---|
203 | cases (fresh ??) #lab0 #u2 normalize nodelta |
---|
204 | normalize @conj try @conj try @conj try @conj try // |
---|
205 | @(convert_break_lift ?? Hsf) |
---|
206 | ] qed. |
---|
207 | |
---|
208 | (* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in |
---|
209 | order to circumvent the associativity problems in notations. *) |
---|
210 | (* |
---|
211 | record swret (A : Type[0]) : Type[0] ≝ { |
---|
212 | ret_st : A; |
---|
213 | ret_acc : list (ident × type); |
---|
214 | ret_u : universe SymbolTag |
---|
215 | }. |
---|
216 | |
---|
217 | notation > "vbox('let' 〈ident v1, ident v2, ident v3〉 ≝ e in break e')" with precedence 48 |
---|
218 | for @{ (λ${ident v1}.λ${ident v2}.λ${ident v3}. ${e'}) |
---|
219 | (ret_st ? ${e}) |
---|
220 | (ret_acc ? ${e}) |
---|
221 | (ret_u ? ${e}) }. |
---|
222 | |
---|
223 | definition ret ≝ λe1,e2,e3. mk_swret statement e1 e2 e3. *) |
---|
224 | |
---|
225 | (* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list |
---|
226 | of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another |
---|
227 | 'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables |
---|
228 | allows it to proceed without failing. This is all in order to ease the proof of simulation. *) |
---|
229 | let rec switch_removal |
---|
230 | (st : statement) (* the statement in which we will remove switches *) |
---|
231 | (u : universe SymbolTag) (* a fresh label and ident generator *) |
---|
232 | : statement × (list (ident × type)) × (universe SymbolTag) ≝ |
---|
233 | match st with |
---|
234 | [ Sskip ⇒ 〈st, [ ], u〉 |
---|
235 | | Sassign _ _ ⇒ 〈st, [ ], u〉 |
---|
236 | | Scall _ _ _ ⇒ 〈st, [ ], u〉 |
---|
237 | | Ssequence s1 s2 ⇒ |
---|
238 | let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in |
---|
239 | let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in |
---|
240 | 〈Ssequence s1' s2', acc1 @ acc2, u''〉 |
---|
241 | | Sifthenelse e s1 s2 ⇒ |
---|
242 | let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in |
---|
243 | let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in |
---|
244 | 〈Sifthenelse e s1' s2', acc1 @ acc2, u''〉 |
---|
245 | | Swhile e body ⇒ |
---|
246 | let 〈body', acc, u'〉 ≝ switch_removal body u in |
---|
247 | 〈Swhile e body', acc, u'〉 |
---|
248 | | Sdowhile e body ⇒ |
---|
249 | let 〈body', acc, u'〉 ≝ switch_removal body u in |
---|
250 | 〈Sdowhile e body', acc, u'〉 |
---|
251 | | Sfor s1 e s2 s3 ⇒ |
---|
252 | let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in |
---|
253 | let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in |
---|
254 | let 〈s3', acc3, u'''〉 ≝ switch_removal s3 u'' in |
---|
255 | 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, u'''〉 |
---|
256 | | Sbreak ⇒ |
---|
257 | 〈st, [ ], u〉 |
---|
258 | | Scontinue ⇒ |
---|
259 | 〈st, [ ], u〉 |
---|
260 | | Sreturn _ ⇒ |
---|
261 | 〈st, [ ], u〉 |
---|
262 | | Sswitch e branches ⇒ |
---|
263 | let 〈sf_branches, acc, u'〉 ≝ switch_removal_branches branches u in |
---|
264 | let 〈switch_tmp, u''〉 ≝ fresh ? u' in |
---|
265 | let ident ≝ Expr (Evar switch_tmp) (typeof e) in |
---|
266 | let assign ≝ Sassign ident e in |
---|
267 | let 〈result, u'''〉 ≝ simplify_switch ident sf_branches u'' in |
---|
268 | 〈Ssequence assign result, (〈switch_tmp, typeof e〉 :: acc), u'''〉 |
---|
269 | | Slabel label body ⇒ |
---|
270 | let 〈body', acc, u'〉 ≝ switch_removal body u in |
---|
271 | 〈Slabel label body', acc, u'〉 |
---|
272 | | Sgoto _ ⇒ |
---|
273 | 〈st, [ ], u〉 |
---|
274 | | Scost cost body ⇒ |
---|
275 | let 〈body', acc, u'〉 ≝ switch_removal body u in |
---|
276 | 〈Scost cost body', acc, u'〉 |
---|
277 | ] |
---|
278 | |
---|
279 | and switch_removal_branches |
---|
280 | (l : labeled_statements) |
---|
281 | (u : universe SymbolTag) |
---|
282 | : (labeled_statements × (list (ident × type)) × (universe SymbolTag)) ≝ |
---|
283 | match l with |
---|
284 | [ LSdefault st ⇒ |
---|
285 | let 〈st', acc1, u'〉 ≝ switch_removal st u in |
---|
286 | 〈LSdefault st', acc1, u'〉 |
---|
287 | | LScase sz int st tl ⇒ |
---|
288 | let 〈tl_result, acc1, u'〉 ≝ switch_removal_branches tl u in |
---|
289 | let 〈st', acc2, u''〉 ≝ switch_removal st u' in |
---|
290 | 〈LScase sz int st' tl_result, acc1 @ acc2, u''〉 |
---|
291 | ]. |
---|
292 | |
---|
293 | definition ret_st : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → A ≝ |
---|
294 | λA,x. |
---|
295 | let 〈s,vars,u〉 ≝ x in s. |
---|
296 | |
---|
297 | definition ret_vars : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → list (ident × type) ≝ |
---|
298 | λA,x. |
---|
299 | let 〈s,vars,u〉 ≝ x in vars. |
---|
300 | |
---|
301 | definition ret_u : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → (universe SymbolTag) ≝ |
---|
302 | λA,x. |
---|
303 | let 〈s,vars,u〉 ≝ x in u. |
---|
304 | |
---|
305 | axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *) |
---|
306 | |
---|
307 | (* Proof that switch_removal_switch_free does its job. *) |
---|
308 | lemma switch_removal_switch_free : ∀st,u. switch_free (ret_st ? (switch_removal st u)). |
---|
309 | #st @(statement_ind2 ? (λls. ∀u. branches_switch_free (ret_st ? (switch_removal_branches ls u))) … st) |
---|
310 | try // |
---|
311 | [ 1: #s1 #s2 #H1 #H2 #u normalize |
---|
312 | lapply (H1 u) |
---|
313 | cases (switch_removal s1 u) * #st1 #vars1 #u' normalize #HA |
---|
314 | lapply (H2 u') |
---|
315 | cases (switch_removal s2 u') * #st2 #vars2 #u'' normalize #HB |
---|
316 | @conj assumption |
---|
317 | | *: |
---|
318 | (* TODO the first few cases show that the lemma is routinely proved. TBF later. *) |
---|
319 | @cthulhu ] |
---|
320 | qed. |
---|
321 | |
---|
322 | (* ----------------------------------------------------------------------------- |
---|
323 | Switch-removal code for programs. |
---|
324 | ----------------------------------------------------------------------------*) |
---|
325 | |
---|
326 | (* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to |
---|
327 | * name clashes for labels. We have no choice but to actually run through the function and to |
---|
328 | * compute the maximum of labels+identifiers. This way we can generate both fresh variables and |
---|
329 | * fresh labels using the same univ. While we're at it we also consider record fields. |
---|
330 | * Cost labels are not considered, though. They already live in a separate universe. |
---|
331 | * |
---|
332 | * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes, |
---|
333 | * but in the end it might be good to move the following functions into fresh.ma. |
---|
334 | *) |
---|
335 | |
---|
336 | (* Least element in the total order of identifiers. *) |
---|
337 | definition least_identifier ≝ an_identifier SymbolTag one. |
---|
338 | |
---|
339 | (* This is certainly overkill: variables adressed in an expression should be declared in the |
---|
340 | * enclosing function's prototype. *) |
---|
341 | let rec max_of_expr (e : expr) : ident ≝ |
---|
342 | match e with |
---|
343 | [ Expr ed _ ⇒ |
---|
344 | match ed with |
---|
345 | [ Econst_int _ _ ⇒ least_identifier |
---|
346 | | Econst_float _ ⇒ least_identifier |
---|
347 | | Evar id ⇒ id |
---|
348 | | Ederef e1 ⇒ max_of_expr e1 |
---|
349 | | Eaddrof e1 ⇒ max_of_expr e1 |
---|
350 | | Eunop _ e1 ⇒ max_of_expr e1 |
---|
351 | | Ebinop _ e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) |
---|
352 | | Ecast _ e1 ⇒ max_of_expr e1 |
---|
353 | | Econdition e1 e2 e3 ⇒ |
---|
354 | max_id (max_of_expr e1) (max_id (max_of_expr e2) (max_of_expr e3)) |
---|
355 | | Eandbool e1 e2 ⇒ |
---|
356 | max_id (max_of_expr e1) (max_of_expr e2) |
---|
357 | | Eorbool e1 e2 ⇒ |
---|
358 | max_id (max_of_expr e1) (max_of_expr e2) |
---|
359 | | Esizeof _ ⇒ least_identifier |
---|
360 | | Efield r f ⇒ max_id f (max_of_expr r) |
---|
361 | | Ecost _ e1 ⇒ max_of_expr e1 |
---|
362 | ] |
---|
363 | ]. |
---|
364 | |
---|
365 | (* Reasoning about this promises to be a serious pain. Especially the Scall case. *) |
---|
366 | let rec max_of_statement (s : statement) : ident ≝ |
---|
367 | match s with |
---|
368 | [ Sskip ⇒ least_identifier |
---|
369 | | Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) |
---|
370 | | Scall r f args ⇒ |
---|
371 | let retmax ≝ |
---|
372 | match r with |
---|
373 | [ None ⇒ least_identifier |
---|
374 | | Some e ⇒ max_of_expr e ] |
---|
375 | in |
---|
376 | max_id (max_of_expr f) |
---|
377 | (max_id retmax |
---|
378 | (foldr ?? (λelt,acc. max_id (max_of_expr elt) acc) least_identifier args) ) |
---|
379 | | Ssequence s1 s2 ⇒ |
---|
380 | max_id (max_of_statement s1) (max_of_statement s2) |
---|
381 | | Sifthenelse e s1 s2 ⇒ |
---|
382 | max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2)) |
---|
383 | | Swhile e body ⇒ |
---|
384 | max_id (max_of_expr e) (max_of_statement body) |
---|
385 | | Sdowhile e body ⇒ |
---|
386 | max_id (max_of_expr e) (max_of_statement body) |
---|
387 | | Sfor init test incr body ⇒ |
---|
388 | max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body)) |
---|
389 | | Sbreak ⇒ least_identifier |
---|
390 | | Scontinue ⇒ least_identifier |
---|
391 | | Sreturn opt ⇒ |
---|
392 | match opt with |
---|
393 | [ None ⇒ least_identifier |
---|
394 | | Some e ⇒ max_of_expr e |
---|
395 | ] |
---|
396 | | Sswitch e ls ⇒ |
---|
397 | max_id (max_of_expr e) (max_of_ls ls) |
---|
398 | | Slabel lab body ⇒ |
---|
399 | max_id lab (max_of_statement body) |
---|
400 | | Sgoto lab ⇒ |
---|
401 | lab |
---|
402 | | Scost _ body ⇒ |
---|
403 | max_of_statement body |
---|
404 | ] |
---|
405 | and max_of_ls (ls : labeled_statements) : ident ≝ |
---|
406 | match ls with |
---|
407 | [ LSdefault s ⇒ max_of_statement s |
---|
408 | | LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s) |
---|
409 | ]. |
---|
410 | |
---|
411 | definition max_id_of_function : function → ident ≝ |
---|
412 | λf. max_id (max_of_statement (fn_body f)) (max_id_of_fn f). |
---|
413 | |
---|
414 | (* We compute fresh universes on a function-by function basis, since there can't |
---|
415 | * be cross-functions gotos or stuff like that. *) |
---|
416 | definition function_switch_removal : function → function × (list (ident × type)) ≝ |
---|
417 | λf. |
---|
418 | let u ≝ universe_of_max (max_id_of_function f) in |
---|
419 | let 〈st, vars, u'〉 ≝ switch_removal (fn_body f) u in |
---|
420 | let result ≝ mk_function (fn_return f) (fn_params f) (vars @ (fn_vars f)) st in |
---|
421 | 〈result, vars〉. |
---|
422 | |
---|
423 | let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝ |
---|
424 | match f with |
---|
425 | [ CL_Internal f ⇒ |
---|
426 | CL_Internal (\fst (function_switch_removal f)) |
---|
427 | | CL_External _ _ _ ⇒ |
---|
428 | f |
---|
429 | ]. |
---|
430 | |
---|
431 | let rec program_switch_removal (p : clight_program) : clight_program ≝ |
---|
432 | let prog_funcs ≝ prog_funct ?? p in |
---|
433 | let sf_funcs ≝ map ?? (λcl_fundef. |
---|
434 | let 〈fun_id, fun_def〉 ≝ cl_fundef in |
---|
435 | 〈fun_id, fundef_switch_removal fun_def〉 |
---|
436 | ) prog_funcs in |
---|
437 | mk_program ?? |
---|
438 | (prog_vars … p) |
---|
439 | sf_funcs |
---|
440 | (prog_main … p). |
---|
441 | |
---|
442 | (* ----------------------------------------------------------------------------- |
---|
443 | Applying two relations on all substatements and all subexprs (directly under). |
---|
444 | ---------------------------------------------------------------------------- *) |
---|
445 | |
---|
446 | let rec substatement_P (s1 : statement) (P : statement → Prop) (Q : expr → Prop) : Prop ≝ |
---|
447 | match s1 with |
---|
448 | [ Sskip ⇒ True |
---|
449 | | Sassign e1 e2 ⇒ Q e1 ∧ Q e2 |
---|
450 | | Scall r f args ⇒ |
---|
451 | match r with |
---|
452 | [ None ⇒ Q f ∧ (All … Q args) |
---|
453 | | Some r ⇒ Q r ∧ Q f ∧ (All … Q args) |
---|
454 | ] |
---|
455 | | Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2 |
---|
456 | | Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2 |
---|
457 | | Swhile e sub ⇒ Q e ∧ P sub |
---|
458 | | Sdowhile e sub ⇒ Q e ∧ P sub |
---|
459 | | Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3 |
---|
460 | | Sbreak ⇒ True |
---|
461 | | Scontinue ⇒ True |
---|
462 | | Sreturn r ⇒ |
---|
463 | match r with |
---|
464 | [ None ⇒ True |
---|
465 | | Some r ⇒ Q r ] |
---|
466 | | Sswitch e ls ⇒ Q e ∧ (substatement_ls ls P) |
---|
467 | | Slabel _ sub ⇒ P sub |
---|
468 | | Sgoto _ ⇒ True |
---|
469 | | Scost _ sub ⇒ P sub |
---|
470 | ] |
---|
471 | and substatement_ls ls (P : statement → Prop) : Prop ≝ |
---|
472 | match ls with |
---|
473 | [ LSdefault sub ⇒ P sub |
---|
474 | | LScase _ _ sub tl ⇒ P sub ∧ (substatement_ls tl P) |
---|
475 | ]. |
---|
476 | |
---|
477 | (* ----------------------------------------------------------------------------- |
---|
478 | Freshness conservation results on switch removal. |
---|
479 | ---------------------------------------------------------------------------- *) |
---|
480 | |
---|
481 | (* Similar stuff in toCminor.ma. *) |
---|
482 | lemma fresh_for_univ_still_fresh : |
---|
483 | ∀u,i. fresh_for_univ SymbolTag i u → ∀v,u'. 〈v, u'〉 = fresh ? u → fresh_for_univ ? i u'. |
---|
484 | * #p * #i #H1 #v * #p' lapply H1 normalize |
---|
485 | #H1 #H2 destruct (H2) /2/ qed. |
---|
486 | |
---|
487 | definition fresher_than_or_equal : universe SymbolTag → universe SymbolTag → Prop ≝ |
---|
488 | λu1,u2. |
---|
489 | match u1 with |
---|
490 | [ mk_universe p1 ⇒ |
---|
491 | match u2 with |
---|
492 | [ mk_universe p2 ⇒ p2 ≤ p1 ] ]. |
---|
493 | |
---|
494 | definition fte ≝ fresher_than_or_equal. |
---|
495 | |
---|
496 | lemma transitive_fte : ∀u1,u2,u3. fte u1 u2 → fte u2 u3 → fte u1 u3. |
---|
497 | * #u1 * #u2 * #u3 normalize /2 by transitive_le/ |
---|
498 | qed. |
---|
499 | |
---|
500 | lemma reflexive_fte : ∀u. fte u u. |
---|
501 | * // qed. |
---|
502 | |
---|
503 | lemma fresher_for_univ : ∀u1,u2. fte u1 u2 → ∀i. fresh_for_univ ? i u2 → fresh_for_univ ? i u1. |
---|
504 | * #p * #p' normalize #H * #i normalize |
---|
505 | /2 by transitive_le/ |
---|
506 | qed. |
---|
507 | |
---|
508 | lemma fresh_fte : ∀u2,u1,fv. fresh ? u2 = 〈fv,u1〉 → fte u1 u2. |
---|
509 | * #u1 * #u2 * #fv normalize #H1 destruct // |
---|
510 | qed. |
---|
511 | |
---|
512 | lemma produce_cond_fte : ∀e,exit,ls,u. fte (\snd (produce_cond e ls u exit)) u. |
---|
513 | #e #exit #ls @(branches_ind … ls) |
---|
514 | [ 1: #st #u normalize lapply (fresh_fte u) |
---|
515 | cases (fresh ? u) #lab #u1 #H lapply (H u1 lab (refl ??)) normalize // |
---|
516 | | 2: #sz #i #hd #tl #Hind #u normalize |
---|
517 | lapply (Hind u) cases (produce_cond e tl u exit) * |
---|
518 | #subcond #sublabel #u1 #Hfte normalize |
---|
519 | lapply (fresh_fte u1) |
---|
520 | cases (fresh ? u1) #lab #u2 #H2 lapply (H2 u2 lab (refl ??)) |
---|
521 | #Hfte' normalize cases u2 in Hfte'; #u2 |
---|
522 | cases u in Hfte; #u cases u1 #u1 normalize |
---|
523 | /2 by transitive_le/ |
---|
524 | ] qed. |
---|
525 | |
---|
526 | 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)). |
---|
527 | #e #exit #ls #u #i @fresher_for_univ @produce_cond_fte qed. |
---|
528 | |
---|
529 | lemma simplify_switch_fte : ∀u,e,ls. |
---|
530 | fte (\snd (simplify_switch e ls u)) u. |
---|
531 | #u #e #ls normalize |
---|
532 | lapply (fresh_fte u) |
---|
533 | cases (fresh ? u) |
---|
534 | #exit_label #uv1 #Haux lapply (Haux uv1 exit_label (refl ??)) -Haux #Haux |
---|
535 | normalize |
---|
536 | lapply (produce_cond_fte e exit_label ls uv1) |
---|
537 | cases (produce_cond ????) * #stm #label #uv2 normalize nodelta |
---|
538 | cases uv2 #uv2 cases uv1 in Haux; #uv1 cases u #u normalize |
---|
539 | /2 by transitive_le/ |
---|
540 | qed. |
---|
541 | |
---|
542 | lemma simplify_switch_fresh : ∀u,i,e,ls. |
---|
543 | fresh_for_univ ? i u → |
---|
544 | fresh_for_univ ? i (\snd (simplify_switch e ls u)). |
---|
545 | #u #i #e #ls @fresher_for_univ @simplify_switch_fte qed. |
---|
546 | |
---|
547 | lemma switch_removal_fte : ∀st,u. |
---|
548 | fte (ret_u ? (switch_removal … st u)) u. |
---|
549 | #st @(statement_ind2 ? (λls. ∀u. fte (ret_u ? (switch_removal_branches ls u)) u) … st) |
---|
550 | try /2 by reflexive_fte/ |
---|
551 | [ 1: #s1 #s2 #Hind1 #Hind2 #u normalize |
---|
552 | lapply (Hind1 u) |
---|
553 | cases (switch_removal s1 u) * #s1' #fvs1 #u' normalize nodelta |
---|
554 | lapply (Hind2 u') |
---|
555 | cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize |
---|
556 | #HA #HB @(transitive_fte … HA HB) |
---|
557 | | 2: #e #s1 #s2 #Hind1 #Hind2 #u normalize |
---|
558 | lapply (Hind1 u) |
---|
559 | cases (switch_removal s1 u) * #s1' #fvs1 #u' normalize nodelta |
---|
560 | lapply (Hind2 u') |
---|
561 | cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize |
---|
562 | #HA #HB @(transitive_fte … HA HB) |
---|
563 | | 3,7,8: #e #s #Hind #u normalize |
---|
564 | lapply (Hind u) |
---|
565 | cases (switch_removal s u) * #s' #fvs #u' normalize #H @H |
---|
566 | | 4: #e #s #Hind #u normalize |
---|
567 | lapply (Hind u) |
---|
568 | cases (switch_removal s u) * #s' #fvs #u' normalize #H @H |
---|
569 | | 5: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #u normalize |
---|
570 | lapply (Hind1 u) cases (switch_removal s1 u) * #s1' #fvs1 #u' #Hfte1 |
---|
571 | normalize nodelta |
---|
572 | lapply (Hind2 u') cases (switch_removal s2 u') * #s2' #fvs2 #u'' #Hfte2 |
---|
573 | normalize nodelta |
---|
574 | lapply (Hind3 u'') cases (switch_removal s3 u'') * #s2' #fvs2 #u'' #Hfte3 |
---|
575 | normalize nodelta |
---|
576 | /3 by transitive_fte/ |
---|
577 | | 6: #e #ls #Hind #u whd in match (switch_removal ??); |
---|
578 | lapply (Hind u) |
---|
579 | cases (switch_removal_branches ls u) * #ls #fvs #u' #Hfte1 |
---|
580 | normalize nodelta |
---|
581 | lapply (fresh_fte … u') cases (fresh ? u') #fv #u'' #H lapply (H u'' fv (refl ??)) #Hfte2 |
---|
582 | normalize nodelta |
---|
583 | lapply (simplify_switch_fte u'' (Expr (Evar fv) (typeof e)) ls) |
---|
584 | cases (simplify_switch ???) |
---|
585 | normalize nodelta |
---|
586 | #st' #u''' #Hfte3 |
---|
587 | /3 by transitive_fte/ |
---|
588 | | 9: #s #H #u normalize |
---|
589 | lapply (H u) cases (switch_removal s u) * #st' #fvs normalize #u' #H @H |
---|
590 | | 10: #sz #i #st #ls #Hind1 #Hind2 #u normalize |
---|
591 | lapply (Hind2 u) cases (switch_removal_branches ls u) * #ls' #fvs' #u' |
---|
592 | normalize nodelta #Hfte1 |
---|
593 | lapply (Hind1 … u') cases (switch_removal st u') * #st' #fvs'' #u'' |
---|
594 | normalize nodelta #Hfte2 |
---|
595 | /3 by transitive_fte/ |
---|
596 | ] qed. |
---|
597 | |
---|
598 | lemma switch_removal_fresh : ∀u,i,st. |
---|
599 | fresh_for_univ ? i u → |
---|
600 | fresh_for_univ ? i (ret_u … (switch_removal st u)). |
---|
601 | #u #i #st @fresher_for_univ @switch_removal_fte qed. |
---|
602 | |
---|
603 | (* ----------------------------------------------------------------------------- |
---|
604 | Simulation proof and related voodoo. |
---|
605 | ----------------------------------------------------------------------------*) |
---|
606 | |
---|
607 | definition expr_lvalue_ind_combined ≝ |
---|
608 | λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. |
---|
609 | conj ?? |
---|
610 | (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx) |
---|
611 | (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx). |
---|
612 | |
---|
613 | let rec expr_ind2 |
---|
614 | (P : expr → Prop) (Q : expr_descr → type → Prop) |
---|
615 | (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) |
---|
616 | (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) |
---|
617 | (Iconst_float : ∀f, t. Q (Econst_float f) t) |
---|
618 | (Ivar : ∀id, t. Q (Evar id) t) |
---|
619 | (Ideref : ∀e, t. P e → Q (Ederef e) t) |
---|
620 | (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) |
---|
621 | (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) |
---|
622 | (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) |
---|
623 | (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) |
---|
624 | (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) |
---|
625 | (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) |
---|
626 | (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) |
---|
627 | (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) |
---|
628 | (Ifield : ∀e,f,t. P e → Q (Efield e f) t) |
---|
629 | (Icost : ∀c,e,t. P e → Q (Ecost c e) t) |
---|
630 | (e : expr) on e : P e ≝ |
---|
631 | match e with |
---|
632 | [ 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) ] |
---|
633 | |
---|
634 | and expr_desc_ind2 |
---|
635 | (P : expr → Prop) (Q : expr_descr → type → Prop) |
---|
636 | (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) |
---|
637 | (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) |
---|
638 | (Iconst_float : ∀f, t. Q (Econst_float f) t) |
---|
639 | (Ivar : ∀id, t. Q (Evar id) t) |
---|
640 | (Ideref : ∀e, t. P e → Q (Ederef e) t) |
---|
641 | (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) |
---|
642 | (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) |
---|
643 | (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) |
---|
644 | (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) |
---|
645 | (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) |
---|
646 | (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) |
---|
647 | (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) |
---|
648 | (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) |
---|
649 | (Ifield : ∀e,f,t. P e → Q (Efield e f) t) |
---|
650 | (Icost : ∀c,e,t. P e → Q (Ecost c e) t) |
---|
651 | (ed : expr_descr) (t : type) on ed : Q ed t ≝ |
---|
652 | match ed with |
---|
653 | [ Econst_int sz i ⇒ Iconst_int sz i t |
---|
654 | | Econst_float f ⇒ Iconst_float f t |
---|
655 | | Evar id ⇒ Ivar id t |
---|
656 | | 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) |
---|
657 | | 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) |
---|
658 | | 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) |
---|
659 | | 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) |
---|
660 | | 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) |
---|
661 | | 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) |
---|
662 | | 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) |
---|
663 | | 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) |
---|
664 | | Esizeof sizeoft ⇒ Isizeof sizeoft t |
---|
665 | | 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) |
---|
666 | | 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) |
---|
667 | ]. |
---|
668 | |
---|
669 | (* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched |
---|
670 | by a non-constant number of evaluations in the converted program. More precisely, |
---|
671 | [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps |
---|
672 | necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *) |
---|
673 | |
---|
674 | (* A version of simplify_switch hiding the ugly projs *) |
---|
675 | definition fresh_for_expression ≝ |
---|
676 | λe,u. fresh_for_univ SymbolTag (max_of_expr e) u. |
---|
677 | |
---|
678 | definition fresh_for_statement ≝ |
---|
679 | λs,u. fresh_for_univ SymbolTag (max_of_statement s) u. |
---|
680 | |
---|
681 | (* needed during mutual induction ... *) |
---|
682 | definition fresh_for_labeled_statements ≝ |
---|
683 | λls,u. fresh_for_univ ? (max_of_ls ls) u. |
---|
684 | |
---|
685 | definition fresh_for_function ≝ |
---|
686 | λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u. |
---|
687 | |
---|
688 | (* misc properties of the max function on positives. *) |
---|
689 | |
---|
690 | lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v. |
---|
691 | * #p whd in ⊢ (??%?); >max_one_neutral // qed. |
---|
692 | |
---|
693 | lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1. |
---|
694 | * #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%); |
---|
695 | >commutative_max // qed. |
---|
696 | |
---|
697 | lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3). |
---|
698 | * #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max // |
---|
699 | qed. |
---|
700 | |
---|
701 | 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. |
---|
702 | * #a * #b * #u normalize |
---|
703 | lapply (pos_compare_to_Prop a b) |
---|
704 | cases (pos_compare a b) whd in ⊢ (% → ?); #Hab |
---|
705 | [ 1: >(le_to_leb_true a b) try /2/ #Hbu @conj /2/ |
---|
706 | | 2: destruct >reflexive_leb /2/ |
---|
707 | | 3: >(not_le_to_leb_false a b) try /2/ #Hau @conj /2/ |
---|
708 | ] qed. |
---|
709 | |
---|
710 | lemma fresh_to_substatements : |
---|
711 | ∀s,u. fresh_for_statement s u → |
---|
712 | substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u). |
---|
713 | #s #u cases s |
---|
714 | whd in match (fresh_for_statement ??); |
---|
715 | whd in match (substatement_P ???); try /2/ |
---|
716 | [ 1: #e1 #e2 |
---|
717 | whd in match (fresh_for_statement ??); |
---|
718 | whd in match (substatement_P ???); |
---|
719 | #H lapply (fresh_max_split … H) * /2 by conj/ |
---|
720 | | 2: #e1 #e2 #args |
---|
721 | whd in match (fresh_for_statement ??); |
---|
722 | whd in match (substatement_P ???); |
---|
723 | cases e1 normalize nodelta |
---|
724 | [ 1: #H lapply (fresh_max_split … H) * #HA #HB @conj try @HA |
---|
725 | elim args in HB; try /2 by I/ #hd #tl normalize nodelta #Hind #HB |
---|
726 | elim (fresh_max_split … HB) #HC #HD |
---|
727 | whd in match (foldr ?????) in HD; |
---|
728 | elim (fresh_max_split … HD) #HE #HF |
---|
729 | @conj try assumption |
---|
730 | @Hind >max_id_commutative >max_id_one_neutral @HF |
---|
731 | | 2: #expr #H cases (fresh_max_split … H) #HA normalize nodelta #HB |
---|
732 | cases (fresh_max_split … HB) #HC #HD @conj try @conj try // elim args in HD; try // |
---|
733 | #e #l #Hind #HD |
---|
734 | whd in match (foldr ?????) in HD; |
---|
735 | elim (fresh_max_split … HD) #HE #HF |
---|
736 | @conj try assumption |
---|
737 | @Hind @HF ] |
---|
738 | | 3: #stmt1 #stmt2 whd in ⊢ (% → %); @fresh_max_split |
---|
739 | | 4: #e #s1 #s2 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) * |
---|
740 | #H1 @fresh_max_split |
---|
741 | | 5: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H) |
---|
742 | | 6: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H) |
---|
743 | | 7: #s1 #e #s2 #s3 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) * #H1 #H2 |
---|
744 | @conj try @conj try @I try @conj try @I |
---|
745 | elim (fresh_max_split … H1) elim (fresh_max_split … H2) /2/ |
---|
746 | | 8: #opt cases opt try /2/ |
---|
747 | | 9: #e #ls #H whd @conj lapply (fresh_max_split … H) * #HA #HB try // lapply HB |
---|
748 | @(labeled_statements_ind … ls) |
---|
749 | [ 1: #s' #H' // |
---|
750 | | 2: #sz #i #s' #tl #Hind #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj |
---|
751 | [ 1: // |
---|
752 | | 2: @Hind @H1 ] ] |
---|
753 | | 10: #lab #stmt #H whd lapply (fresh_max_split … H) * // |
---|
754 | ] qed. |
---|
755 | |
---|
756 | (* Auxilliary commutation lemma used in [substatement_fresh]. *) |
---|
757 | lemma foldl_max : ∀l,a,b. |
---|
758 | foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l = |
---|
759 | max_id a (foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) b l). |
---|
760 | #l elim l |
---|
761 | [ 1: * #a * #b whd in match (foldl ?????) in ⊢ (??%%); @refl |
---|
762 | | 2: #hd #tl #Hind #a #b whd in match (foldl ?????) in ⊢ (??%%); |
---|
763 | <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl |
---|
764 | ] qed. |
---|
765 | |
---|
766 | (* Lookup functions in list environments (used to type local variables in functions) *) |
---|
767 | let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝ |
---|
768 | match l with |
---|
769 | [ nil ⇒ false |
---|
770 | | cons hd tl ⇒ |
---|
771 | let 〈id, ty〉 ≝ hd in |
---|
772 | match identifier_eq SymbolTag i id with |
---|
773 | [ inl Hid_eq ⇒ true |
---|
774 | | inr Hid_neq ⇒ mem_assoc_env i tl |
---|
775 | ] |
---|
776 | ]. |
---|
777 | |
---|
778 | (* --------------------------------------------------------------------------- *) |
---|
779 | (* Memory extensions (limited form on memoryInjection.ma). Note that we state the |
---|
780 | properties at the back-end level. *) |
---|
781 | (* --------------------------------------------------------------------------- *) |
---|
782 | |
---|
783 | (* A writeable_block is a block that is: |
---|
784 | . valid |
---|
785 | . non-empty (i.e. it has been allocated a non-empty size) |
---|
786 | *) |
---|
787 | record nonempty_block (m : mem) (b : block) : Prop ≝ |
---|
788 | { |
---|
789 | wb_valid : valid_block m b; |
---|
790 | wb_nonempty : low (blocks m b) < high (blocks m b) |
---|
791 | }. |
---|
792 | |
---|
793 | (* Type stating that m2 is an extension of m1, parameterised by a list of blocks where we can write freely *) |
---|
794 | record sr_memext (m1 : mem) (m2 : mem) (writeable : list block) : Prop ≝ |
---|
795 | { (* Non-empty blocks are preserved as they are. This entails [load_sim]. *) |
---|
796 | me_nonempty : ∀b. nonempty_block m1 b → nonempty_block m2 b ∧ blocks m1 b = blocks m2 b; |
---|
797 | (* These blocks are valid in [m2] *) |
---|
798 | me_writeable_valid : ∀b. meml ? b writeable → nonempty_block m2 b; |
---|
799 | (* blocks in [m1] than can be validly pointed to cannot be in [me_writeable]. *) |
---|
800 | me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable) |
---|
801 | |
---|
802 | (* This field is not entailed [me_not_writeable] and is necessary to prove valid |
---|
803 | pointer conservation after a [free]. *) |
---|
804 | |
---|
805 | (* Extension blocks contain nothing in [m1] *) |
---|
806 | (* me_not_mapped : ∀b. meml … b me_writeable → blocks m1 b = empty_block OZ OZ; *) |
---|
807 | (* Valid pointers are still valid in m2. One could think that this is superfluous as |
---|
808 | being implied by me_inj, and it is but for a small detail: valid_pointer allows a pointer |
---|
809 | to be one off the end of a block bound. The internal check in beloadv does not. |
---|
810 | valid_pointer should be understood as "pointer making sense" rather than "pointer from |
---|
811 | which you can load stuff". [mi_valid_pointers] is used for instance when proving the |
---|
812 | semantics preservation for equality testing (where we check that the pointers we |
---|
813 | compare are valid before being equal). |
---|
814 | *) |
---|
815 | (* me_valid_pointers : ∀p. |
---|
816 | valid_pointer m1 p = true → |
---|
817 | valid_pointer m2 p = true *) |
---|
818 | }. |
---|
819 | |
---|
820 | (* Since we removed end_pointers, we can prove some stuff that was previously given as a field of |
---|
821 | sr_memext. *) |
---|
822 | lemma me_not_writeable_ptr : |
---|
823 | ∀m1,m2,writeable. |
---|
824 | sr_memext m1 m2 writeable → |
---|
825 | ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable). |
---|
826 | #m1 #m2 #writeable #Hext #p #Hvalid |
---|
827 | cut (nonempty_block m1 (pblock p)) |
---|
828 | [ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % // |
---|
829 | /2 by Zle_to_Zlt_to_Zlt/ |
---|
830 | | 2: @(me_not_writeable … Hext) ] |
---|
831 | qed. |
---|
832 | |
---|
833 | (* If we have a memory extension, we can simulate loads *) |
---|
834 | lemma sr_memext_load_sim : ∀m1,m2,writeable. sr_memext m1 m2 writeable → load_sim m1 m2. |
---|
835 | #m1 #m2 #writeable #Hext #ptr #bev whd in match (beloadv ??) in ⊢ (% → %); |
---|
836 | #H cut (nonempty_block m1 (pblock ptr) ∧ |
---|
837 | Zle (low (blocks m1 (pblock ptr))) |
---|
838 | (Z_of_unsigned_bitvector 16 (offv (poff ptr))) ∧ |
---|
839 | Zlt (Z_of_unsigned_bitvector 16 (offv (poff ptr))) |
---|
840 | (high (blocks m1 (pblock ptr))) ∧ |
---|
841 | bev = (contents (blocks m1 (pblock ptr)) (Z_of_unsigned_bitvector 16 (offv (poff ptr))))) |
---|
842 | [ @conj try @conj try @conj try % |
---|
843 | [ 1: @Zltb_true_to_Zlt ] |
---|
844 | cases (Zltb (block_id (pblock ptr)) (nextblock m1)) in H; normalize nodelta |
---|
845 | [ 1: // |
---|
846 | | 2,4,6,8,10: #Habsurd destruct ] |
---|
847 | generalize in match (Z_of_unsigned_bitvector offset_size (offv (poff ptr))); #z |
---|
848 | lapply (Zleb_true_to_Zle (low (blocks m1 (pblock ptr))) z) |
---|
849 | lapply (Zltb_true_to_Zlt z (high (blocks m1 (pblock ptr)))) |
---|
850 | cases (Zleb (low (blocks m1 (pblock ptr))) z) |
---|
851 | cases (Zltb z (high (blocks m1 (pblock ptr)))) #H1 #H2 |
---|
852 | [ 2,3,4,6,7,8,10,11,12,14,15,16: normalize #Habsurd destruct ] normalize #Heq |
---|
853 | lapply (H1 (refl ??)) lapply (H2 (refl ??)) |
---|
854 | #Hle #Hlt destruct try assumption try @refl |
---|
855 | @(Zle_to_Zlt_to_Zlt … Hle Hlt) ] |
---|
856 | * * * #Hnonempty #Hlow #Hhigh #Hres lapply (me_nonempty … Hext … Hnonempty) * |
---|
857 | * #Hvalid #Hlt #Hblocks_eq |
---|
858 | >(Zlt_to_Zltb_true … Hvalid) normalize <Hblocks_eq |
---|
859 | >(Zle_to_Zleb_true … Hlow) >(Zlt_to_Zltb_true … Hhigh) normalize |
---|
860 | >Hres @refl |
---|
861 | qed. |
---|
862 | |
---|
863 | lemma me_valid_pointers : |
---|
864 | ∀m1,m2,writeable. |
---|
865 | sr_memext m1 m2 writeable → |
---|
866 | ∀p. valid_pointer m1 p = true → valid_pointer m2 p = true. |
---|
867 | * #contents1 #nextblock1 #Hnextblock_pos1 |
---|
868 | * #contents2 #nextblock2 #Hnextblock_pos2 #writeable #Hmemext * #pb #po #Hvalid |
---|
869 | cut (nonempty_block (mk_mem contents1 nextblock1 Hnextblock_pos1) pb) |
---|
870 | [ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % // |
---|
871 | /2 by Zle_to_Zlt_to_Zlt/ ] |
---|
872 | #Hnonempty lapply (me_nonempty … Hmemext … Hnonempty) * * #Hvalid_block #Hlow_lt_high |
---|
873 | #Hcontents_eq normalize >(Zlt_to_Zltb_true … Hvalid_block) normalize nodelta |
---|
874 | <Hcontents_eq cases (valid_pointer_to_Prop … Hvalid) * #_ #Hle #Hlt |
---|
875 | >(Zle_to_Zleb_true … Hle) normalize nodelta |
---|
876 | >(Zlt_to_Zltb_true … Hlt) @refl |
---|
877 | qed. |
---|
878 | |
---|
879 | (* --------------------------------------------------------------------------- *) |
---|
880 | (* Some lemmas on environments and their contents *) |
---|
881 | |
---|
882 | |
---|
883 | (* Definition of environment inclusion and equivalence *) |
---|
884 | (* Environment "inclusion". *) |
---|
885 | definition environment_sim ≝ λenv1,env2. |
---|
886 | ∀id, res. lookup SymbolTag block env1 id = Some ? res → |
---|
887 | lookup SymbolTag block env2 id = Some ? res. |
---|
888 | |
---|
889 | lemma environment_sim_invert_aux : ∀en1,en2. |
---|
890 | (∀id,res. lookup_opt block id en1 = Some ? res → lookup_opt ? id en2 = Some ? res) → |
---|
891 | ∀id. lookup_opt ? id en2 = None ? → lookup_opt ? id en1 = None ?. |
---|
892 | #en1 elim en1 try // |
---|
893 | #opt1 #left1 #right1 #Hindl1 #Hindr1 #en2 #Hsim |
---|
894 | normalize #id elim id normalize nodelta |
---|
895 | [ 1: #Hlookup cases opt1 in Hsim; try // #res #Hsim lapply (Hsim one res (refl ??)) |
---|
896 | #Hlookup2 >Hlookup2 in Hlookup; #H @H |
---|
897 | | 2: #id' cases en2 in Hsim; |
---|
898 | [ 1: normalize #Hsim #_ #_ lapply (Hsim (p1 id')) normalize nodelta |
---|
899 | cases (lookup_opt block id' right1) try // |
---|
900 | #res #Hsim' lapply (Hsim' ? (refl ??)) #Habsurd destruct |
---|
901 | | 2: #opt2 #left2 #right2 #Hsim #Hlookup whd in ⊢ ((??%?) → ?); #Hlookup' |
---|
902 | @(Hindr1 right2) try // #id0 #res0 |
---|
903 | lapply (Hsim (p1 id0) res0) normalize #Hsol #H @Hsol @H ] |
---|
904 | | 3: #id' cases en2 in Hsim; |
---|
905 | [ 1: normalize #Hsim #_ #_ lapply (Hsim (p0 id')) normalize nodelta |
---|
906 | cases (lookup_opt block id' left1) try // |
---|
907 | #res #Hsim' lapply (Hsim' ? (refl ??)) #Habsurd destruct |
---|
908 | | 2: #opt2 #left2 #right2 #Hsim #Hlookup whd in ⊢ ((??%?) → ?); #Hlookup' |
---|
909 | @(Hindl1 left2) try // #id0 #res0 |
---|
910 | lapply (Hsim (p0 id0) res0) normalize #Hsol #H @Hsol @H ] |
---|
911 | ] qed. |
---|
912 | |
---|
913 | lemma environment_sim_invert : |
---|
914 | ∀en1,en2. environment_sim en1 en2 → |
---|
915 | ∀id. lookup SymbolTag block en2 id = None ? → |
---|
916 | lookup SymbolTag block en1 id = None ?. |
---|
917 | * #en1 * #en2 #Hsim * #id @environment_sim_invert_aux |
---|
918 | #id' #res #Hlookup normalize in Hsim; |
---|
919 | lapply (Hsim (an_identifier … id') res) normalize #Hsol @Hsol @Hlookup |
---|
920 | qed. |
---|
921 | |
---|
922 | (* Environment equivalence. *) |
---|
923 | definition environment_eq ≝ λenv1,env2. environment_sim env1 env2 ∧ environment_sim env2 env1. |
---|
924 | |
---|
925 | lemma symmetric_environment_eq : ∀env1,env2. environment_eq env1 env2 → environment_eq env2 env1. |
---|
926 | #env1 #env2 * #Hsim1 #Hsim2 % // qed. |
---|
927 | |
---|
928 | lemma reflexive_environment_eq : ∀env. environment_eq env env. |
---|
929 | #env % // qed. |
---|
930 | |
---|
931 | (* An environment [e2] is a disjoint extension of [e1] iff (the new bindings are |
---|
932 | fresh and [e2] is equivalent to adding extension blocks to [e1]). *) |
---|
933 | definition disjoint_extension ≝ |
---|
934 | λ(e1, e2 : env). |
---|
935 | λ(new_vars : list (ident × type)). |
---|
936 | (∀id. mem_assoc_env id new_vars = true → lookup ?? e1 id = None ?) ∧ (* extension not in e1 *) |
---|
937 | (∀id. mem_assoc_env id new_vars = true → ∃res.lookup ?? e2 id = Some ? res) ∧ (* all of the extension is in e2 *) |
---|
938 | (∀id. mem_assoc_env id new_vars = false → lookup ?? e1 id = lookup ?? e2 id). (* only [new_vars] extends e2 *) |
---|
939 | |
---|
940 | lemma disjoint_extension_to_inclusion : |
---|
941 | ∀e1,e2,vars. disjoint_extension e1 e2 vars → |
---|
942 | environment_sim e1 e2. |
---|
943 | #e1 #e2 #vars * * #HA #HB #HC whd #id #res |
---|
944 | @(match (mem_assoc_env id vars) return λx.(mem_assoc_env id vars = x) → ? |
---|
945 | with |
---|
946 | [ true ⇒ λH. ? |
---|
947 | | false ⇒ λH. ? |
---|
948 | ] (refl ? (mem_assoc_env id vars))) |
---|
949 | [ 1: #Hlookup lapply (HA ? H) #Habsurd >Habsurd in Hlookup; #H destruct |
---|
950 | | 2: #Hlookup <(HC ? H) assumption ] |
---|
951 | qed. |
---|
952 | |
---|
953 | (* Small aux lemma to decompose folds on maps with list accumulators *) |
---|
954 | lemma fold_to_concat : ∀A:Type[0].∀m:positive_map A.∀l.∀f. |
---|
955 | (fold ?? (λx,a,el. 〈an_identifier SymbolTag (f x), a〉::el) m l) |
---|
956 | = (fold ?? (λx,a,el. 〈an_identifier SymbolTag (f x), a〉::el) m []) @ l. |
---|
957 | #A #m elim m |
---|
958 | [ 1: #l #f normalize @refl |
---|
959 | | 2: #optblock #left #right |
---|
960 | #Hind1 #Hind2 #l #f |
---|
961 | whd in match (fold ?????) in ⊢ (??%%); |
---|
962 | cases optblock |
---|
963 | [ 1: normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%); |
---|
964 | >associative_append @refl |
---|
965 | | 2: #block normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%); |
---|
966 | >Hind1 in ⊢ (???%); >append_cons <associative_append @refl |
---|
967 | ] |
---|
968 | ] qed. |
---|
969 | |
---|
970 | lemma map_proj_fold : ∀A:Type[0].∀m:positive_map A. ∀f. ∀l. |
---|
971 | map ?? (λx.\snd x) (fold ?? (λx,a,el.〈an_identifier SymbolTag x,a〉::el) m l) = |
---|
972 | map ?? (λx.\snd x) (fold ?? (λx,a,el.〈an_identifier SymbolTag (f x),a〉::el) m l). |
---|
973 | #A #m elim m |
---|
974 | [ 1: #f #l normalize @refl |
---|
975 | | 2: #opt #left #right #Hind1 #Hind2 #f #l |
---|
976 | normalize cases opt |
---|
977 | [ 1: normalize nodelta >fold_to_concat >fold_to_concat in ⊢ (???%); |
---|
978 | <map_append <map_append <Hind2 <Hind2 in ⊢ (???%); |
---|
979 | <Hind1 <Hind1 in ⊢ (???%); @refl |
---|
980 | | 2: #elt normalize nodelta >fold_to_concat >fold_to_concat in ⊢ (???%); |
---|
981 | <map_append <map_append <Hind2 <Hind2 in ⊢ (???%); |
---|
982 | <(Hind1 p0) <Hind1 in ⊢ (???%); |
---|
983 | >(fold_to_concat ?? (〈an_identifier SymbolTag one,elt〉::l)) |
---|
984 | >(fold_to_concat ?? (〈an_identifier SymbolTag (f one),elt〉::l)) |
---|
985 | <map_append <map_append normalize in match (map ??? (cons ???)); @refl |
---|
986 | ] |
---|
987 | ] qed. |
---|
988 | |
---|
989 | lemma lookup_entails_block : ∀en:env.∀id,res. |
---|
990 | lookup SymbolTag block en id = Some ? res → |
---|
991 | meml ? res (blocks_of_env en). |
---|
992 | * #map * #id #res |
---|
993 | whd in match (blocks_of_env ?); |
---|
994 | whd in match (elements ???); |
---|
995 | whd in match (lookup ????); |
---|
996 | normalize nodelta |
---|
997 | lapply res lapply id -id -res |
---|
998 | elim map |
---|
999 | [ 1: #id #res normalize #Habsurd destruct (Habsurd) |
---|
1000 | | 2: #optblock #left #right #Hind1 #Hind2 #id #res #Hind3 |
---|
1001 | whd in match (fold ?????); |
---|
1002 | cases optblock in Hind3; |
---|
1003 | [ 1: normalize nodelta |
---|
1004 | whd in match (lookup_opt ???); |
---|
1005 | cases id normalize nodelta |
---|
1006 | [ 1: #Habsurd destruct (Habsurd) |
---|
1007 | | 2: #p #Hright lapply (Hind2 … Hright) |
---|
1008 | normalize >fold_to_concat in ⊢ (? → %); |
---|
1009 | <map_append #Haux @mem_append_backwards %1 |
---|
1010 | <map_proj_fold @Haux |
---|
1011 | | 3: #p #Hleft lapply (Hind1 … Hleft) |
---|
1012 | normalize >fold_to_concat in ⊢ (? → %); |
---|
1013 | <map_append #Haux @mem_append_backwards %2 |
---|
1014 | <map_proj_fold @Haux ] |
---|
1015 | | 2: #blo whd in match (lookup_opt ???); |
---|
1016 | normalize >fold_to_concat <map_append |
---|
1017 | cases id normalize nodelta |
---|
1018 | [ 1: #Heq destruct (Heq) |
---|
1019 | @mem_append_backwards %2 >fold_to_concat |
---|
1020 | <map_append @mem_append_backwards %2 normalize %1 @refl |
---|
1021 | | 2: #p #Hlookup lapply (Hind2 … Hlookup) #H |
---|
1022 | @mem_append_backwards %1 |
---|
1023 | <map_proj_fold @H |
---|
1024 | | 3: #p #Hlookup lapply (Hind1 … Hlookup) #H |
---|
1025 | @mem_append_backwards %2 >fold_to_concat |
---|
1026 | <map_append @mem_append_backwards %1 |
---|
1027 | <map_proj_fold @H |
---|
1028 | ] |
---|
1029 | ] |
---|
1030 | ] qed. |
---|
1031 | |
---|
1032 | lemma blocks_of_env_cons : |
---|
1033 | ∀en,id,hd. mem ? hd (blocks_of_env (add SymbolTag block en id hd)). |
---|
1034 | #en #id #hd @(lookup_entails_block … id) |
---|
1035 | cases id #p elim p try /2/ qed. |
---|
1036 | |
---|
1037 | lemma in_blocks_exists_id : ∀env.∀bl. meml … bl (blocks_of_env env) → ∃id. lookup SymbolTag block env id = Some ? bl. |
---|
1038 | #env elim env #m elim m |
---|
1039 | [ 1: #bl normalize @False_ind |
---|
1040 | | 2: #opt #left #right #Hind1 #Hind2 #bl normalize |
---|
1041 | >fold_to_concat <map_append #H |
---|
1042 | elim (mem_append_forward ???? H) |
---|
1043 | [ 1: <map_proj_fold -H #H lapply (Hind2 … H) |
---|
1044 | * * #id #Hlookup normalize in Hlookup; |
---|
1045 | %{(an_identifier SymbolTag (p1 id))} normalize nodelta @Hlookup |
---|
1046 | | 2: <map_proj_fold cases opt |
---|
1047 | [ 1: normalize -H #H lapply (Hind1 … H) |
---|
1048 | * * #id #Hlookup normalize in Hlookup; |
---|
1049 | %{(an_identifier SymbolTag (p0 id))} normalize nodelta @Hlookup |
---|
1050 | | 2: #bl' normalize >fold_to_concat <map_append normalize |
---|
1051 | #H' elim (mem_append_forward ???? H') |
---|
1052 | [ 1: -H #H lapply (Hind1 … H) * * #id normalize #Hlookup |
---|
1053 | %{(an_identifier ? (p0 id))} normalize nodelta @Hlookup |
---|
1054 | | 2: normalize * [ 2: @False_ind ] |
---|
1055 | #Heq destruct (Heq) |
---|
1056 | %{(an_identifier SymbolTag one)} @refl |
---|
1057 | ] |
---|
1058 | ] |
---|
1059 | ] |
---|
1060 | ] qed. |
---|
1061 | |
---|
1062 | let rec inclusion_elim |
---|
1063 | (A : Type[0]) |
---|
1064 | (m1, m2 : positive_map A) |
---|
1065 | (P : positive_map A → positive_map A → Prop) |
---|
1066 | (H1 : ∀m2. P (pm_leaf A) m2) |
---|
1067 | (H2 : ∀opt1,left1,right1. P left1 (pm_leaf A) → P right1 (pm_leaf A) → P (pm_node A opt1 left1 right1) (pm_leaf A)) |
---|
1068 | (H3 : ∀opt1,left1,right1,opt2,left2,right2. P left1 left2 → P right1 right2 → P (pm_node A opt1 left1 right1) (pm_node A opt2 left2 right2)) |
---|
1069 | on m1 : P m1 m2 ≝ |
---|
1070 | match m1 with |
---|
1071 | [ pm_leaf ⇒ |
---|
1072 | H1 m2 |
---|
1073 | | pm_node opt1 left1 right1 ⇒ |
---|
1074 | match m2 with |
---|
1075 | [ pm_leaf ⇒ |
---|
1076 | H2 opt1 left1 right1 (inclusion_elim A left1 (pm_leaf A) P H1 H2 H3) (inclusion_elim A right1 (pm_leaf A) P H1 H2 H3) |
---|
1077 | | pm_node opt2 left2 right2 ⇒ |
---|
1078 | H3 opt1 left1 right1 opt2 left2 right2 (inclusion_elim A left1 left2 P H1 H2 H3) (inclusion_elim A right1 right2 P H1 H2 H3) |
---|
1079 | ] |
---|
1080 | ]. |
---|
1081 | |
---|
1082 | (* Environment inclusion entails block inclusion. *) |
---|
1083 | lemma environment_sim_blocks_inclusion : |
---|
1084 | ∀env1, env2. environment_sim env1 env2 → lset_inclusion ? (blocks_of_env env1) (blocks_of_env env2). |
---|
1085 | * #m1 * #m2 @(inclusion_elim … m1 m2) -m1 -m2 |
---|
1086 | [ 1: #m2 normalize #_ @I |
---|
1087 | | 2: #opt1 #left1 #right1 #Hind1 #Hind2 #Hsim |
---|
1088 | normalize >fold_to_concat in ⊢ (???%); <map_append @All_append |
---|
1089 | [ 1: <map_proj_fold @Hind2 #id #res elim id #id' #Hlookup @(Hsim (an_identifier ? (p1 id')) res Hlookup) |
---|
1090 | | 2: cases opt1 in Hsim; |
---|
1091 | [ 1: normalize nodelta #Hsim |
---|
1092 | <map_proj_fold @Hind1 #id #res elim id #id' #Hlookup @(Hsim (an_identifier ? (p0 id')) res Hlookup) |
---|
1093 | | 2: #bl #Hsim lapply (Hsim (an_identifier ? one) bl ?) normalize try @refl |
---|
1094 | #Habsurd destruct (Habsurd) |
---|
1095 | ] |
---|
1096 | ] |
---|
1097 | | 3: #opt1 #left1 #right1 #opt2 #left2 #right2 #Hind1 #Hind2 #Hsim |
---|
1098 | normalize >fold_to_concat >fold_to_concat in ⊢ (???%); |
---|
1099 | <map_append <map_append in ⊢ (???%); @All_append |
---|
1100 | [ 1: cases opt2; normalize nodelta |
---|
1101 | [ 1: <map_proj_fold <map_proj_fold in ⊢ (???%); <(map_proj_fold ?? p0) |
---|
1102 | cut (environment_sim (an_id_map SymbolTag block right1) (an_id_map SymbolTag block right2)) |
---|
1103 | [ 1: * #id' #res #Hlookup |
---|
1104 | lapply (Hsim (an_identifier ? (p1 id')) res) normalize #H @H @Hlookup ] |
---|
1105 | #Hsim' lapply (Hind2 Hsim') @All_mp |
---|
1106 | #a #Hmem @mem_append_backwards %1 @Hmem |
---|
1107 | | 2: #bl <map_proj_fold <map_proj_fold in ⊢ (???%); <(map_proj_fold ?? p0) |
---|
1108 | cut (environment_sim (an_id_map SymbolTag block right1) (an_id_map SymbolTag block right2)) |
---|
1109 | [ 1: * #id' #res #Hlookup |
---|
1110 | lapply (Hsim (an_identifier ? (p1 id')) res) normalize #H @H @Hlookup ] |
---|
1111 | #Hsim' lapply (Hind2 Hsim') @All_mp |
---|
1112 | #a #Hmem @mem_append_backwards %1 @Hmem ] |
---|
1113 | | 2: cut (environment_sim (an_id_map SymbolTag block left1) (an_id_map SymbolTag block left2)) |
---|
1114 | [ 1: * #id' #res #Hlookup |
---|
1115 | lapply (Hsim (an_identifier ? (p0 id')) res) normalize #H @H @Hlookup ] #Hsim' |
---|
1116 | lapply (Hind1 … Hsim') |
---|
1117 | <map_proj_fold <map_proj_fold in ⊢ (? → (???%)); <(map_proj_fold ?? p0) |
---|
1118 | cases opt1 in Hsim; normalize nodelta |
---|
1119 | [ 1: #Hsim @All_mp #a #Hmem @mem_append_backwards %2 |
---|
1120 | cases opt2 normalize nodelta |
---|
1121 | [ 1: @Hmem |
---|
1122 | | 2: #bl >fold_to_concat <map_append @mem_append_backwards %1 @Hmem ] |
---|
1123 | | 2: #bl #Hsim #Hmem >fold_to_concat in ⊢ (???%); <map_append @All_append |
---|
1124 | [ 2: normalize @conj try @I |
---|
1125 | cases opt2 in Hsim; |
---|
1126 | [ 1: #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) |
---|
1127 | normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
1128 | | 2: #bl2 #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) |
---|
1129 | normalize in ⊢ (% → ?); #Heq >Heq normalize nodelta |
---|
1130 | @mem_append_backwards %2 >fold_to_concat <map_append |
---|
1131 | @mem_append_backwards %2 normalize %1 @refl ] |
---|
1132 | | 1: cases opt2 in Hsim; |
---|
1133 | [ 1: #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) |
---|
1134 | normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
1135 | | 2: #bl2 #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) |
---|
1136 | normalize in ⊢ (% → ?); #Heq lapply (Hind1 Hsim') |
---|
1137 | @All_mp #a #Hmem >Heq normalize nodelta |
---|
1138 | @mem_append_backwards %2 >fold_to_concat <map_append |
---|
1139 | @mem_append_backwards %1 @Hmem ] ] |
---|
1140 | ] |
---|
1141 | ] |
---|
1142 | ] qed. |
---|
1143 | |
---|
1144 | |
---|
1145 | (* equivalent environments yield "equal" sets of block (cf. frontend_misc.ma) *) |
---|
1146 | lemma environment_eq_blocks_eq : ∀env1,env2. |
---|
1147 | environment_eq env1 env2 → |
---|
1148 | lset_eq ? (blocks_of_env env1) (blocks_of_env env2). |
---|
1149 | #env1 #env2 * #Hsim1 #Hsim2 @conj |
---|
1150 | @environment_sim_blocks_inclusion assumption |
---|
1151 | qed. |
---|
1152 | |
---|
1153 | (* [env_codomain env vars] is the image of vars through env seen as a function. *) |
---|
1154 | definition env_codomain : env → list (ident×type) → lset block ≝ λe,l. |
---|
1155 | foldi … (λid,block,acc. |
---|
1156 | if mem_assoc_env … id l then |
---|
1157 | block :: acc |
---|
1158 | else |
---|
1159 | acc |
---|
1160 | ) e [ ]. |
---|
1161 | |
---|
1162 | (* --------------------------------------------------------------------------- *) |
---|
1163 | |
---|
1164 | (* Two equivalent memories yield a trivial memory extension. *) |
---|
1165 | lemma memory_eq_to_mem_ext : ∀m1,m2. memory_eq m1 m2 → sr_memext m1 m2 [ ]. |
---|
1166 | * #contents1 #nextblock1 #Hpos * #contents2 #nextblock2 #Hpos' normalize * |
---|
1167 | #Hnextblock #Hcontents_eq destruct % |
---|
1168 | [ 1: #b #H @conj try % elim H try // |
---|
1169 | | 2: #b * |
---|
1170 | | 3: #b #_ normalize % // ] |
---|
1171 | qed. |
---|
1172 | |
---|
1173 | (* memory extensions form a preorder relation *) |
---|
1174 | |
---|
1175 | lemma memory_ext_transitive : |
---|
1176 | ∀m1,m2,m3,writeable1,writeable2. |
---|
1177 | sr_memext m1 m2 writeable1 → |
---|
1178 | sr_memext m2 m3 writeable2 → |
---|
1179 | sr_memext m1 m3 (writeable1 @ writeable2). |
---|
1180 | #m1 #m2 #m3 #writeable1 #writeable2 #H12 #H23 % |
---|
1181 | [ 1: #b #Hnonempty1 |
---|
1182 | lapply (me_nonempty … H12 b Hnonempty1) * #Hnonempty2 #Hblocks_eq |
---|
1183 | lapply (me_nonempty … H23 b Hnonempty2) * #Hnonempty3 #Hblocks_eq' @conj |
---|
1184 | try assumption >Hblocks_eq >Hblocks_eq' @refl |
---|
1185 | | 2: #b #Hmem lapply (mem_append_forward ???? Hmem) * |
---|
1186 | [ 1: #Hmem12 lapply (me_writeable_valid … H12 b Hmem12) #Hnonempty2 |
---|
1187 | elim (me_nonempty … H23 … Hnonempty2) // |
---|
1188 | | 2: #Hmem23 @(me_writeable_valid … H23 b Hmem23) ] |
---|
1189 | | 3: #b #Hvalid % #Hmem lapply (mem_append_forward ???? Hmem) * |
---|
1190 | [ 1: #Hmem12 |
---|
1191 | lapply (me_not_writeable … H12 … Hvalid) * #H @H assumption |
---|
1192 | | 2: #Hmem23 lapply (me_nonempty … H12 … Hvalid) * #Hvalid2 |
---|
1193 | lapply (me_not_writeable … H23 … Hvalid2) * #H #_ @H assumption |
---|
1194 | ] |
---|
1195 | ] qed. |
---|
1196 | |
---|
1197 | lemma memory_ext_reflexive : ∀m. sr_memext m m [ ]. |
---|
1198 | #m % /2/ #b * qed. |
---|
1199 | |
---|
1200 | (* --------------------------------------------------------------------------- *) |
---|
1201 | (* Lemmas relating memory extensions to [free] *) |
---|
1202 | |
---|
1203 | lemma beloadv_free_simulation : |
---|
1204 | ∀m1,m2,writeable,block,ptr,res. |
---|
1205 | ∀mem_hyp : sr_memext m1 m2 writeable. |
---|
1206 | beloadv (free m1 block) ptr = Some ? res → beloadv (free m2 block) ptr = Some ? res. |
---|
1207 | * #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2 #writeable |
---|
1208 | * #br #bid * * #pr #pid #poff #res #Hext |
---|
1209 | (*#Hme_nonempty #Hme_writeable #Hme_nonempty #Hvalid_conserv*) |
---|
1210 | #Hload |
---|
1211 | lapply (beloadv_free_beloadv … Hload) #Hload_before_free |
---|
1212 | lapply (beloadv_free_blocks_neq … Hload) #Hblocks_neq |
---|
1213 | @beloadv_free_beloadv2 |
---|
1214 | [ 1: @Hblocks_neq ] |
---|
1215 | @(sr_memext_load_sim … Hext) assumption |
---|
1216 | qed. |
---|
1217 | |
---|
1218 | |
---|
1219 | (* Lifting the property of being valid after a free to memory extensions *) |
---|
1220 | lemma valid_pointer_free : ∀m1,m2,writeable. sr_memext m1 m2 writeable → ∀p,b. valid_pointer (free m1 b) p = true → valid_pointer (free m2 b) p = true. |
---|
1221 | #m1 #m2 #writeable #Hext #p #b #Hvalid |
---|
1222 | lapply (valid_free_to_valid … Hvalid) #Hvalid_before_free |
---|
1223 | lapply (me_valid_pointers … Hext … Hvalid_before_free) |
---|
1224 | lapply (valid_after_free … Hvalid) #Hneq |
---|
1225 | whd in match (free ??); |
---|
1226 | whd in match (update_block ????); |
---|
1227 | whd in match (valid_pointer ??) in ⊢ (% → %); |
---|
1228 | whd in match (low_bound ??) in ⊢ (% → %); |
---|
1229 | whd in match (high_bound ??) in ⊢ (% → %); |
---|
1230 | >(not_eq_block_rev … Hneq) normalize nodelta #H @H |
---|
1231 | qed. |
---|
1232 | |
---|
1233 | lemma nonempty_block_mismatch : ∀m,b,bl. |
---|
1234 | nonempty_block (free m bl) b → |
---|
1235 | nonempty_block m b ∧ b ≠ bl. |
---|
1236 | #m #b #bl #Hnonempty |
---|
1237 | @(eq_block_elim … b bl) |
---|
1238 | [ 1: #Heq >Heq in Hnonempty; * #_ normalize |
---|
1239 | cases (block_region bl) normalize >eqZb_reflexive normalize * |
---|
1240 | | 2: #Hneq @conj try assumption elim Hnonempty #Hvalid #Hlh % |
---|
1241 | [ 1: lapply Hvalid normalize // |
---|
1242 | | 2: lapply Hlh normalize |
---|
1243 | cases (block_region b) normalize nodelta |
---|
1244 | cases (block_region bl) normalize nodelta try // |
---|
1245 | @(eqZb_elim … (block_id b) (block_id bl)) |
---|
1246 | [ 1,3: * normalize * |
---|
1247 | | 2,4: #_ // ] ] ] |
---|
1248 | qed. |
---|
1249 | |
---|
1250 | lemma eqb_to_eq_block : ∀a,b : block. a == b = eq_block a b. |
---|
1251 | #a #b lapply (eqb_true ? a b) @(eq_block_elim … a b) |
---|
1252 | /2 by neq_block_eq_block_false, true_to_andb_true/ |
---|
1253 | qed. |
---|
1254 | |
---|
1255 | (* We can free in both sides of a memory extension if we take care of removing |
---|
1256 | the freed block from the set of writeable blocks. *) |
---|
1257 | lemma free_memory_ext : |
---|
1258 | ∀m1,m2,writeable,bl. |
---|
1259 | sr_memext m1 m2 writeable → |
---|
1260 | sr_memext (free m1 bl) (free m2 bl) (lset_remove ? writeable bl). |
---|
1261 | #m1 #m2 #writeable #bl #Hext % |
---|
1262 | [ 1: #b #Hnonempty lapply (nonempty_block_mismatch … Hnonempty) |
---|
1263 | * #Hnonempty' #Hblocks_neq lapply (me_nonempty … Hext … Hnonempty') * |
---|
1264 | #Hnonempty2 #Hcontents_eq @conj |
---|
1265 | [ 1: % try @(wb_valid … Hnonempty2) |
---|
1266 | whd in match (free ??); |
---|
1267 | whd in match (update_block ?????); |
---|
1268 | >(neq_block_eq_block_false … Hblocks_neq) normalize |
---|
1269 | try @(wb_nonempty … Hnonempty2) |
---|
1270 | | 2: whd in match (free ??) in ⊢ (??%%); |
---|
1271 | whd in match (update_block ?????) in ⊢ (??%%); |
---|
1272 | >(neq_block_eq_block_false … Hblocks_neq) |
---|
1273 | normalize nodelta assumption ] |
---|
1274 | | 2: #b #Hmem |
---|
1275 | cut (mem block b writeable ∧ b ≠ bl) |
---|
1276 | [ elim writeable in Hmem; |
---|
1277 | [ 1: normalize * |
---|
1278 | | 2: #hd #tl #Hind whd in match (filter ???); |
---|
1279 | >eqb_to_eq_block |
---|
1280 | @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta |
---|
1281 | [ 1: #Heq #H whd in match (meml ???); elim (Hind H) #H0 #H1 @conj |
---|
1282 | [ 1: %2 ] assumption |
---|
1283 | | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * |
---|
1284 | [ 1: #H destruct /3 by conj, or_introl, refl/ |
---|
1285 | | 2: #H elim (Hind H) #H1 #H2 /3 by conj, or_intror, refl/ ] ] ] |
---|
1286 | ] * #Hmem2 #Hblocks_neq |
---|
1287 | lapply (me_writeable_valid … Hext … Hmem2) * #Hvalid #Hnonempty % |
---|
1288 | try assumption whd in match (free ??); whd in match (update_block ?????); |
---|
1289 | >(neq_block_eq_block_false … Hblocks_neq) @Hnonempty |
---|
1290 | | 3: #p #Hvalid lapply (nonempty_block_mismatch … Hvalid) * #Hnonempty #Hblocks_neq |
---|
1291 | % #Hmem lapply (me_not_writeable … Hext … Hnonempty) * #H @H |
---|
1292 | elim writeable in Hmem; |
---|
1293 | [ 1: * |
---|
1294 | | 2: #hd #tl #Hind whd in match (filter ???) in ⊢ (% → ?); >eqb_to_eq_block |
---|
1295 | @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta |
---|
1296 | [ 1: #Heq #H normalize %2 @(Hind H) |
---|
1297 | | 2: #Hblocks_neq whd in match (meml ???); * |
---|
1298 | [ 1: #Hneq normalize %1 assumption |
---|
1299 | | 2: #Hmem normalize %2 @(Hind Hmem) ] |
---|
1300 | ] |
---|
1301 | ] |
---|
1302 | ] qed. |
---|
1303 | |
---|
1304 | |
---|
1305 | (* Freeing from an extension block is ok. *) |
---|
1306 | lemma memext_free_extended_conservation : |
---|
1307 | ∀m1,m2 : mem. |
---|
1308 | ∀writeable. |
---|
1309 | ∀mem_hyp : sr_memext m1 m2 writeable. |
---|
1310 | ∀b. meml ? b writeable → |
---|
1311 | sr_memext m1 (free m2 b) (lset_remove … writeable b). |
---|
1312 | #m1 #m2 #writeable #Hext #b #Hb_writeable % |
---|
1313 | [ 1: #bl #Hnonempty lapply (me_not_writeable … Hext … Hnonempty) #Hnot_mem |
---|
1314 | lapply (mem_not_mem_neq … Hb_writeable Hnot_mem) #Hblocks_neq |
---|
1315 | @conj |
---|
1316 | [ 2: whd in match (free ??); whd in match (update_block ?????); |
---|
1317 | >(neq_block_eq_block_false … (sym_neq … Hblocks_neq)) normalize |
---|
1318 | elim (me_nonempty … Hext … Hnonempty) // |
---|
1319 | | 1: % elim (me_nonempty … Hext … Hnonempty) * try // |
---|
1320 | #Hvalid2 #Hlh #Hcontents_eq whd in match (free ??); |
---|
1321 | whd in match (update_block ?????); |
---|
1322 | >(neq_block_eq_block_false … (sym_neq … Hblocks_neq)) normalize assumption |
---|
1323 | ] |
---|
1324 | | 2: #b' #Hmem (* contradiction in first premise *) |
---|
1325 | cut (mem block b' writeable ∧ b' ≠ b) |
---|
1326 | [ elim writeable in Hmem; |
---|
1327 | [ 1: normalize @False_ind |
---|
1328 | | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block |
---|
1329 | @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta |
---|
1330 | [ 1: #Heq #H whd in match (meml ???); destruct |
---|
1331 | elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption |
---|
1332 | | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * |
---|
1333 | [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] |
---|
1334 | | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ] |
---|
1335 | ] ] ] |
---|
1336 | * #Hb' #Hneq lapply (me_writeable_valid … Hext … Hb') #Hvalid % |
---|
1337 | [ 1: @(wb_valid … Hvalid) |
---|
1338 | | 2: whd in match (free ??); |
---|
1339 | whd in match (update_block ?????); |
---|
1340 | >(neq_block_eq_block_false … Hneq) |
---|
1341 | @(wb_nonempty … Hvalid) ] |
---|
1342 | | 3: #b' #Hnonempty % #Hmem |
---|
1343 | cut (mem block b' writeable ∧ b' ≠ b) |
---|
1344 | [ elim writeable in Hmem; |
---|
1345 | [ 1: normalize @False_ind |
---|
1346 | | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block |
---|
1347 | @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta |
---|
1348 | [ 1: #Heq #H whd in match (meml ???); destruct |
---|
1349 | elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption |
---|
1350 | | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * |
---|
1351 | [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] |
---|
1352 | | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ] |
---|
1353 | ] ] ] * #Hmem' #Hblocks_neq |
---|
1354 | lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption |
---|
1355 | ] qed. |
---|
1356 | |
---|
1357 | |
---|
1358 | lemma disjoint_extension_nil_eq_set : |
---|
1359 | ∀env1,env2. |
---|
1360 | disjoint_extension env1 env2 [ ] → |
---|
1361 | lset_eq ? (blocks_of_env env1) (blocks_of_env env2). |
---|
1362 | #env1 #env whd in ⊢ (% → ?); * * #_ #_ #H normalize in H; |
---|
1363 | @environment_eq_blocks_eq whd @conj |
---|
1364 | #id #res >(H id) // |
---|
1365 | qed. |
---|
1366 | |
---|
1367 | lemma free_list_equivalent_sets : |
---|
1368 | ∀m,set1,set2. |
---|
1369 | lset_eq ? set1 set2 → |
---|
1370 | memory_eq (free_list m set1) (free_list m set2). |
---|
1371 | #m #set1 #set2 #Heq whd in match (free_list ??) in ⊢ (?%%); |
---|
1372 | @(lset_eq_fold block_DeqSet mem memory_eq … Heq) |
---|
1373 | [ 1: @reflexive_memory_eq |
---|
1374 | | 2: @transitive_memory_eq |
---|
1375 | | 3: @symmetric_memory_eq |
---|
1376 | | 4: #x #acc1 #acc2 |
---|
1377 | whd in match (free ??) in ⊢ (? → (?%%)); |
---|
1378 | whd in match (memory_eq ??) in ⊢ (% → %); * |
---|
1379 | #Hnextblock_eq #Hcontents_eq @conj try assumption |
---|
1380 | #b normalize >Hcontents_eq @refl |
---|
1381 | | 5: #x1 #x2 #acc normalize @conj try @refl |
---|
1382 | * * #id normalize nodelta cases (block_region x1) |
---|
1383 | cases (block_region x2) normalize nodelta |
---|
1384 | @(eqZb_elim id (block_id x1)) #Hx1 normalize nodelta |
---|
1385 | @(eqZb_elim id (block_id x2)) #Hx2 normalize nodelta try @refl |
---|
1386 | | 6: * #r #i * #contents #nextblock #Hpos @conj |
---|
1387 | [ 1: @refl |
---|
1388 | | 2: #b normalize cases (block_region b) normalize |
---|
1389 | cases r normalize cases (eqZb (block_id b) i) |
---|
1390 | normalize @refl |
---|
1391 | ] |
---|
1392 | ] qed. |
---|
1393 | |
---|
1394 | lemma foldr_identity : ∀A:Type[0]. ∀l:list A. foldr A ? (λx:A.λl0.x::l0) [] l = l. |
---|
1395 | #A #l elim l // |
---|
1396 | #hd #tl #Hind whd in match (foldr ?????); >Hind @refl |
---|
1397 | qed. |
---|
1398 | |
---|
1399 | lemma mem_not_mem_diff_aux : |
---|
1400 | ∀s1,s2,s3,hd. |
---|
1401 | mem ? hd s1 → |
---|
1402 | ¬(mem ? hd s2) → |
---|
1403 | mem block hd (lset_difference ? s1 (s2@(filter block_DeqSet (λx:block_DeqSet.¬x==hd) s3))). |
---|
1404 | #s1 #s2 #s3 #hd #Hmem #Hnotmem lapply Hmem lapply s1 -s1 |
---|
1405 | elim s3 |
---|
1406 | [ 1: #s1 >append_nil elim s1 try // |
---|
1407 | #hd' #tl' #Hind * |
---|
1408 | [ 1: #Heq >lset_difference_unfold |
---|
1409 | @(match hd'∈s2 return λx. (hd'∈s2 = x) → ? with |
---|
1410 | [ true ⇒ λH. ? |
---|
1411 | | false ⇒ λH. ? |
---|
1412 | ] (refl ? (hd'∈s2))) normalize nodelta |
---|
1413 | [ 1: lapply (memb_to_mem … H) #Hmem elim Hnotmem #H' destruct |
---|
1414 | @(False_ind … (H' Hmem)) |
---|
1415 | | 2: whd %1 assumption ] |
---|
1416 | | 2: #Hmem >lset_difference_unfold |
---|
1417 | @(match hd'∈s2 return λx. (hd'∈s2 = x) → ? with |
---|
1418 | [ true ⇒ λH. ? |
---|
1419 | | false ⇒ λH. ? |
---|
1420 | ] (refl ? (hd'∈s2))) normalize nodelta |
---|
1421 | [ 1: @Hind @Hmem |
---|
1422 | | 2: %2 @Hind @Hmem ] ] |
---|
1423 | | 2: #hd' #tl' #H #s1 #Hmem >filter_cons_unfold >eqb_to_eq_block |
---|
1424 | @(eq_block_elim … hd' hd) |
---|
1425 | [ 1: >notb_true normalize nodelta #Heq @H @Hmem |
---|
1426 | | 2: #Hneq >notb_false normalize nodelta |
---|
1427 | >lset_difference_permute >(cons_to_append … hd') |
---|
1428 | >associative_append >lset_difference_unfold2 >nil_append |
---|
1429 | >lset_difference_permute @H |
---|
1430 | elim s1 in Hmem; try // |
---|
1431 | #hd'' #tl'' #Hind * |
---|
1432 | [ 1: #Heq destruct whd in match (lset_remove ???); |
---|
1433 | >eqb_to_eq_block >(neq_block_eq_block_false … (sym_neq … Hneq)) |
---|
1434 | >notb_false normalize nodelta %1 @refl |
---|
1435 | | 2: #Hmem whd in match (lset_remove ???); |
---|
1436 | cases (¬(hd''==hd')) normalize nodelta |
---|
1437 | [ 1: %2 @Hind @Hmem |
---|
1438 | | 2: @Hind @Hmem ] ] ] |
---|
1439 | ] qed. |
---|
1440 | |
---|
1441 | (* freeing equivalent sets of blocks on memory extensions yields memory extensions *) |
---|
1442 | lemma free_equivalent_sets : |
---|
1443 | ∀m1,m2,writeable,set1,set2. |
---|
1444 | lset_eq ? set1 set2 → |
---|
1445 | sr_memext m1 m2 writeable → |
---|
1446 | sr_memext (free_list m1 set1) (free_list m2 set2) (lset_difference ? writeable set1). |
---|
1447 | #m1 #m2 #writeable #set1 #set2 #Heq #Hext |
---|
1448 | lapply (free_list_equivalent_sets m2 … (symmetric_lset_eq … Heq)) |
---|
1449 | #Heq |
---|
1450 | lapply (memory_eq_to_mem_ext … (symmetric_memory_eq … Heq)) #Hext' |
---|
1451 | lapply (memory_ext_transitive (free_list m1 set1) (free_list m2 set1) (free_list m2 set2) (filter block_eq (λwb:block_eq.¬wb∈set1) writeable) [ ] ? Hext') |
---|
1452 | [ 2: >append_nil #H @H ] |
---|
1453 | elim set1 |
---|
1454 | [ 1: whd in match (free_list ??); whd in match (free_list ??); |
---|
1455 | normalize >foldr_identity @Hext |
---|
1456 | | 2: #hd #tl #Hind >free_list_cons >free_list_cons |
---|
1457 | lapply (free_memory_ext … hd … Hind) |
---|
1458 | cut ((lset_remove block_eq (filter block_eq (λwb:block_eq.¬wb∈tl) writeable) hd) = |
---|
1459 | (filter block_eq (λwb:block_eq.¬wb∈hd::tl) writeable)) |
---|
1460 | [ whd in match (lset_remove ???); elim writeable // |
---|
1461 | #hd' #tl' #Hind_cut >filter_cons_unfold >filter_cons_unfold |
---|
1462 | whd in match (memb ???) in ⊢ (???%); >eqb_to_eq_block |
---|
1463 | (* elim (eqb_true block_DeqSet hd' hd)*) |
---|
1464 | @(eq_block_elim … hd' hd) normalize nodelta |
---|
1465 | [ 1: #Heq |
---|
1466 | cases (¬hd'∈tl) normalize nodelta |
---|
1467 | [ 1: whd in match (foldr ?????); >Heq >eqb_to_eq_block >eq_block_b_b normalize in match (notb ?); |
---|
1468 | normalize nodelta |
---|
1469 | lapply Hind_cut destruct #H @H |
---|
1470 | | 2: lapply Hind_cut destruct #H @H ] |
---|
1471 | | 2: #Hneq cases (¬hd'∈tl) normalize nodelta try assumption |
---|
1472 | whd in match (foldr ?????); >eqb_to_eq_block |
---|
1473 | >(neq_block_eq_block_false … Hneq) |
---|
1474 | normalize in match (notb ?); normalize nodelta >Hind_cut @refl |
---|
1475 | ] |
---|
1476 | ] |
---|
1477 | #Heq >Heq #H @H |
---|
1478 | ] qed. |
---|
1479 | |
---|
1480 | (* Remove a writeable block. *) |
---|
1481 | lemma memory_ext_weaken : |
---|
1482 | ∀m1,m2,hd,writeable. |
---|
1483 | sr_memext m1 m2 (hd :: writeable) → |
---|
1484 | sr_memext m1 m2 writeable. |
---|
1485 | #m1 #m2 #hd #writeable * |
---|
1486 | #Hnonempty #Hwriteable_valid #Hnot_writeable % |
---|
1487 | try assumption |
---|
1488 | [ 1: #b #Hmem @Hwriteable_valid whd %2 assumption |
---|
1489 | | 2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem |
---|
1490 | ] qed. |
---|
1491 | |
---|
1492 | (* Perform a "rewrite" using lset_eq on the writeable blocks *) |
---|
1493 | lemma memory_ext_writeable_eq : |
---|
1494 | ∀m1,m2,wr1,wr2. |
---|
1495 | sr_memext m1 m2 wr1 → |
---|
1496 | lset_eq ? wr1 wr2 → |
---|
1497 | sr_memext m1 m2 wr2. |
---|
1498 | #m1 #m2 #wr1 #wr2 #Hext #Hset_eq % |
---|
1499 | [ 1: @(me_nonempty … Hext) |
---|
1500 | | 2: #b #Hmem lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) |
---|
1501 | @(me_writeable_valid … Hext) |
---|
1502 | | 3: #b #Hnonempty % #Hmem |
---|
1503 | lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem' |
---|
1504 | lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption |
---|
1505 | ] qed. |
---|
1506 | |
---|
1507 | |
---|
1508 | |
---|
1509 | lemma memory_eq_to_memory_ext_pre : |
---|
1510 | ∀m1,m1',m2,writeable. |
---|
1511 | memory_eq m1 m1' → |
---|
1512 | sr_memext m1' m2 writeable → |
---|
1513 | sr_memext m1 m2 writeable. |
---|
1514 | #m1 #m1' #m2 #writeable #Heq #Hext |
---|
1515 | lapply (memory_eq_to_mem_ext … Heq) #Hext' |
---|
1516 | @(memory_ext_transitive … Hext' Hext) |
---|
1517 | qed. |
---|
1518 | |
---|
1519 | lemma memory_eq_to_memory_ext_post : |
---|
1520 | ∀m1,m2,m2',writeable. |
---|
1521 | memory_eq m2' m2 → |
---|
1522 | sr_memext m1 m2' writeable → |
---|
1523 | sr_memext m1 m2 writeable. |
---|
1524 | #m1 #m2 #m2' #writeable #Heq #Hext |
---|
1525 | lapply (memory_eq_to_mem_ext … Heq) #Hext' |
---|
1526 | lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H |
---|
1527 | qed. |
---|
1528 | |
---|
1529 | |
---|
1530 | lemma memext_free_extended_environment : |
---|
1531 | ∀m1,m2,writeable. |
---|
1532 | sr_memext m1 m2 writeable → |
---|
1533 | ∀env,env_ext,vars. |
---|
1534 | disjoint_extension env env_ext vars → |
---|
1535 | lset_inclusion ? (lset_difference ? (blocks_of_env env_ext) (blocks_of_env env)) writeable → |
---|
1536 | sr_memext |
---|
1537 | (free_list m1 (blocks_of_env env)) |
---|
1538 | (free_list m2 (blocks_of_env env_ext)) |
---|
1539 | (lset_difference ? writeable (blocks_of_env env_ext)). |
---|
1540 | #m1 #m2 #writeable #Hext #env #env_ext #vars #Hdisjoint #Hext_in_writeable |
---|
1541 | (* Disjoint extension induces environment "inclusion", i.e. simulation *) |
---|
1542 | lapply (disjoint_extension_to_inclusion … Hdisjoint) #Hincl |
---|
1543 | (* Environment inclusion entails set inclusion on the mapped blocks *) |
---|
1544 | lapply (environment_sim_blocks_inclusion … Hincl) #Hblocks_incl |
---|
1545 | (* This set inclusion can be decomposed on a common part and an extended part. *) |
---|
1546 | lapply (lset_inclusion_difference ??? Hblocks_incl) |
---|
1547 | * #extended_part * * #Hset_eq #Henv_disjoint_ext #Hextended_eq |
---|
1548 | lapply (lset_difference_lset_eq … writeable … Hset_eq) #HeqA |
---|
1549 | cut (lset_inclusion ? extended_part writeable) |
---|
1550 | [ 1: cases Hextended_eq #HinclA #_ @(transitive_lset_inclusion … HinclA … Hext_in_writeable) ] |
---|
1551 | -Hext_in_writeable #Hext_in_writeable |
---|
1552 | @(memory_ext_writeable_eq ????? (symmetric_lset_eq … HeqA)) |
---|
1553 | lapply (free_list_equivalent_sets m2 ?? Hset_eq) #Hmem_eq |
---|
1554 | @(memory_eq_to_memory_ext_post … (symmetric_memory_eq … Hmem_eq)) |
---|
1555 | (* Add extended ⊆ (lset_difference block_eq writeable (blocks_of_env env @ tl)) in Hind *) |
---|
1556 | cut (∀x. mem ? x extended_part → ¬ (mem ? x (blocks_of_env env))) |
---|
1557 | [ 1: cases Hextended_eq #Hincl_ext #_ @(lset_not_mem_difference … Hincl_ext) ] |
---|
1558 | lapply (proj2 … Hset_eq) lapply Hext_in_writeable |
---|
1559 | @(WF_rect ????? (filtered_list_wf block_DeqSet extended_part)) |
---|
1560 | * |
---|
1561 | [ 1: #_ #_ #_ #_ #_ >append_nil |
---|
1562 | @(free_equivalent_sets ???? (blocks_of_env env) (reflexive_lset_eq ??) Hext) |
---|
1563 | | 2: #hd #tl #Hwf_step #Hind_wf #Hext_in_writeable #Hset_incl #Hin_ext_not_in_env |
---|
1564 | cut (lset_eq ? (blocks_of_env env@hd::tl) (hd::(blocks_of_env env@tl))) |
---|
1565 | [ 1: >cons_to_append >cons_to_append in ⊢ (???%); |
---|
1566 | @lset_eq_concrete_to_lset_eq // ] |
---|
1567 | #Hpermute |
---|
1568 | lapply (free_list_equivalent_sets m2 ?? Hpermute) #Hmem_eq2 |
---|
1569 | @(memory_eq_to_memory_ext_post … (symmetric_memory_eq … Hmem_eq2)) |
---|
1570 | >free_list_cons |
---|
1571 | lapply (lset_difference_lset_eq … writeable … Hpermute) #HeqB |
---|
1572 | @(memory_ext_writeable_eq ????? (symmetric_lset_eq … HeqB)) |
---|
1573 | >lset_difference_unfold2 |
---|
1574 | lapply (lset_difference_lset_remove_commute ? hd writeable (blocks_of_env env@tl)) |
---|
1575 | #Heq_commute >Heq_commute |
---|
1576 | (* lapply (memory_ext_writeable_eq ????? (symmetric_lset_eq … Heq_commute)) *) |
---|
1577 | lapply (Hind_wf (filter … (λx.¬(x==hd)) tl) ????) |
---|
1578 | [ 2: @(transitive_lset_inclusion … Hset_incl) |
---|
1579 | @lset_inclusion_concat_monotonic |
---|
1580 | @cons_preserves_inclusion |
---|
1581 | @lset_inclusion_filter_self |
---|
1582 | | 3: @(transitive_lset_inclusion … Hext_in_writeable) |
---|
1583 | @cons_preserves_inclusion |
---|
1584 | @lset_inclusion_filter_self |
---|
1585 | | 4: whd whd in ⊢ (???%); |
---|
1586 | lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?); |
---|
1587 | normalize nodelta @refl |
---|
1588 | | 1: #x #H @Hin_ext_not_in_env %2 elim tl in H; // |
---|
1589 | #hd' #tl' #Hind >filter_cons_unfold >eqb_to_eq_block @(eq_block_elim … hd' hd) |
---|
1590 | >notb_true >notb_false normalize nodelta |
---|
1591 | [ 1: #Heq >Heq #H %2 @Hind @H |
---|
1592 | | 2: #Hneq * |
---|
1593 | [ 1: #Heq destruct %1 @refl |
---|
1594 | | 2: #H %2 @Hind @H ] ] |
---|
1595 | ] |
---|
1596 | #Hext_ind |
---|
1597 | lapply (Hin_ext_not_in_env … hd (or_introl … (refl ??))) |
---|
1598 | #Hnot_in_env |
---|
1599 | lapply (memext_free_extended_conservation … Hext_ind hd ?) |
---|
1600 | [ 1: @mem_not_mem_diff_aux try assumption elim Hext_in_writeable #H #_ @H ] |
---|
1601 | -Hext_ind #Hext_ind |
---|
1602 | cut (memory_eq (free (free_list m2 (blocks_of_env env@filter block_DeqSet (λx:block_DeqSet.¬x==hd) tl)) hd) |
---|
1603 | (free (free_list m2 (blocks_of_env env@tl)) hd)) |
---|
1604 | [ 1: <free_list_cons <free_list_cons |
---|
1605 | @free_list_equivalent_sets @lset_eq_concrete_to_lset_eq |
---|
1606 | >cons_to_append >cons_to_append in ⊢ (???%); |
---|
1607 | @(transitive_lset_eq_concrete … (switch_lset_eq_concrete ????)) |
---|
1608 | @symmetric_lset_eq_concrete |
---|
1609 | @(transitive_lset_eq_concrete ????? (switch_lset_eq_concrete ????)) |
---|
1610 | @lset_eq_to_lset_eq_concrete |
---|
1611 | elim (blocks_of_env env) |
---|
1612 | [ 1: @symmetric_lset_eq @lset_eq_filter |
---|
1613 | | 2: #hd0 #tl0 #Hind >cons_to_append |
---|
1614 | >associative_append in ⊢ (??%%); |
---|
1615 | >associative_append in ⊢ (??%%); |
---|
1616 | @cons_monotonic_eq @Hind ] ] |
---|
1617 | #Hmem_eq3 @(memory_eq_to_memory_ext_post … Hmem_eq3) |
---|
1618 | @(memory_ext_writeable_eq … Hext_ind) |
---|
1619 | <lset_difference_lset_remove_commute <lset_difference_lset_remove_commute |
---|
1620 | <lset_difference_unfold2 <lset_difference_unfold2 |
---|
1621 | @lset_difference_lset_eq |
---|
1622 | (* Note: exactly identical to the proof in the cut. *) |
---|
1623 | @lset_eq_concrete_to_lset_eq |
---|
1624 | >cons_to_append >cons_to_append in ⊢ (???%); |
---|
1625 | @(transitive_lset_eq_concrete … (switch_lset_eq_concrete ????)) |
---|
1626 | @symmetric_lset_eq_concrete |
---|
1627 | @(transitive_lset_eq_concrete ????? (switch_lset_eq_concrete ????)) |
---|
1628 | @lset_eq_to_lset_eq_concrete |
---|
1629 | elim (blocks_of_env env) |
---|
1630 | [ 1: @symmetric_lset_eq @lset_eq_filter |
---|
1631 | | 2: #hd0 #tl0 #Hind >cons_to_append |
---|
1632 | >associative_append in ⊢ (??%%); |
---|
1633 | >associative_append in ⊢ (??%%); |
---|
1634 | @cons_monotonic_eq @Hind ] |
---|
1635 | ] qed. |
---|
1636 | |
---|
1637 | (* --------------------------------------------------------------------------- *) |
---|
1638 | (* Some lemmas allowing to reason on writes to extended memories. *) |
---|
1639 | |
---|
1640 | (* Writing in the extended part of the memory preserves the extension (that's the point) *) |
---|
1641 | lemma bestorev_writeable_memory_ext : |
---|
1642 | ∀m1,m2,writeable. |
---|
1643 | ∀Hext:sr_memext m1 m2 writeable. |
---|
1644 | ∀wb,wo,v. meml ? wb writeable → |
---|
1645 | ∀m2'.bestorev m2 (mk_pointer wb wo) v = Some ? m2' → |
---|
1646 | sr_memext m1 m2' writeable. |
---|
1647 | #m1 * #contents2 #nextblock2 #Hpos2 #writeable #Hext #wb #wo #v #Hmem #m2' |
---|
1648 | whd in ⊢ ((??%?) → ?); |
---|
1649 | lapply (me_writeable_valid … Hext ? Hmem) * whd in ⊢ (% → ?); #Hlt |
---|
1650 | >(Zlt_to_Zltb_true … Hlt) normalize nodelta #Hnonempty2 #H |
---|
1651 | lapply (if_opt_inversion ???? H) -H * #Hzltb |
---|
1652 | lapply (andb_inversion … Hzltb) * #Hleb #Hltb -Hzltb |
---|
1653 | #Heq destruct % |
---|
1654 | [ 1: #b #Hnonempty1 |
---|
1655 | lapply (me_nonempty … Hext b Hnonempty1) * * #Hvalid_b #Hnonempty_b |
---|
1656 | #Heq @conj |
---|
1657 | [ 1: % whd whd in Hvalid_b; try @Hvalid_b |
---|
1658 | normalize cases (block_region b) normalize nodelta |
---|
1659 | cases (block_region wb) normalize nodelta try // |
---|
1660 | @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta |
---|
1661 | try // |
---|
1662 | | 2: whd in ⊢ (??%%); |
---|
1663 | @(eq_block_elim … b wb) normalize nodelta // #Heq_b_wb |
---|
1664 | lapply (me_not_writeable … Hext b Hnonempty1) destruct (Heq_b_wb) |
---|
1665 | * #H @(False_ind … (H Hmem)) ] |
---|
1666 | | 2: #b #Hmem_writeable |
---|
1667 | lapply (me_writeable_valid … Hext … Hmem_writeable) #H % |
---|
1668 | [ 1: normalize cases H // |
---|
1669 | | 2: cases H normalize #Hb_lt #Hb_nonempty2 |
---|
1670 | cases (block_region b) |
---|
1671 | cases (block_region wb) normalize nodelta |
---|
1672 | // |
---|
1673 | @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta |
---|
1674 | // ] |
---|
1675 | | 3: #b #Hnonempty |
---|
1676 | lapply (me_not_writeable … Hext … Hnonempty) // |
---|
1677 | ] qed. |
---|
1678 | |
---|
1679 | (* If we manage to write in a block, then it is nonempty *) |
---|
1680 | lemma bestorev_success_nonempty : |
---|
1681 | ∀m,wb,wo,v,m'. |
---|
1682 | bestorev m (mk_pointer wb wo) v = Some ? m' → |
---|
1683 | nonempty_block m wb. |
---|
1684 | #m #wb #wo #v #m' normalize #Hstore |
---|
1685 | cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H |
---|
1686 | cases (if_opt_inversion ???? H) -H #nonempty #H % |
---|
1687 | [ 1: whd @Zltb_true_to_Zlt assumption |
---|
1688 | | 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H' |
---|
1689 | cut (Zleb (low (blocks m wb)) z = true) |
---|
1690 | [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ] |
---|
1691 | #Hleb >Hleb in H'; normalize nodelta #Hlt |
---|
1692 | lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt) |
---|
1693 | /2 by Zle_to_Zlt_to_Zlt/ |
---|
1694 | ] qed. |
---|
1695 | |
---|
1696 | (* If we manage to write in a block, it is still non-empty after the write *) |
---|
1697 | lemma bestorev_success_nonempty2 : |
---|
1698 | ∀m,wb,wo,v,m'. |
---|
1699 | bestorev m (mk_pointer wb wo) v = Some ? m' → |
---|
1700 | nonempty_block m' wb. |
---|
1701 | #m #wb #wo #v #m' normalize #Hstore |
---|
1702 | cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H |
---|
1703 | cases (if_opt_inversion ???? H) -H #nonempty #H % |
---|
1704 | [ 1: whd destruct @Zltb_true_to_Zlt assumption |
---|
1705 | | 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H' |
---|
1706 | cut (Zleb (low (blocks m wb)) z = true) |
---|
1707 | [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ] |
---|
1708 | #Hleb >Hleb in H'; normalize nodelta #Hlt |
---|
1709 | lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt) |
---|
1710 | destruct cases (block_region wb) normalize >eqZb_z_z normalize |
---|
1711 | /2 by Zle_to_Zlt_to_Zlt/ |
---|
1712 | ] qed. |
---|
1713 | |
---|
1714 | (* A nonempty block stays nonempty after a write. *) |
---|
1715 | lemma nonempty_block_update_ok : |
---|
1716 | ∀m,b,wb,offset,v. |
---|
1717 | nonempty_block m b → |
---|
1718 | nonempty_block |
---|
1719 | (mk_mem |
---|
1720 | (update_block ? wb |
---|
1721 | (mk_block_contents (low (blocks m wb)) (high (blocks m wb)) |
---|
1722 | (update beval offset v (contents (blocks m wb)))) (blocks m)) |
---|
1723 | (nextblock m) (nextblock_pos m)) b. |
---|
1724 | #m #b #wb #offset #v * #Hvalid #Hnonempty % // |
---|
1725 | cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize |
---|
1726 | cases br normalize nodelta cases wbr normalize nodelta // |
---|
1727 | @(eqZb_elim … bid wbid) // #Heq #Hlt normalize // |
---|
1728 | qed. |
---|
1729 | |
---|
1730 | lemma nonempty_block_update_ok2 : |
---|
1731 | ∀m,b,wb,offset,v. |
---|
1732 | nonempty_block |
---|
1733 | (mk_mem |
---|
1734 | (update_block ? wb |
---|
1735 | (mk_block_contents (low (blocks m wb)) (high (blocks m wb)) |
---|
1736 | (update beval offset v (contents (blocks m wb)))) (blocks m)) |
---|
1737 | (nextblock m) (nextblock_pos m)) b → |
---|
1738 | nonempty_block m b. |
---|
1739 | #m #b #wb #offset #v * #Hvalid #Hnonempty % // |
---|
1740 | cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize |
---|
1741 | cases br normalize nodelta cases wbr normalize nodelta // |
---|
1742 | @(eqZb_elim … bid wbid) // #Heq #Hlt normalize // |
---|
1743 | qed. |
---|
1744 | |
---|
1745 | (* Writing in the non-extended part of the memory preserves the extension as long |
---|
1746 | * as it's done identically in both memories. *) |
---|
1747 | lemma bestorev_not_writeable_memory_ext : |
---|
1748 | ∀m1,m2,writeable. |
---|
1749 | ∀Hext:sr_memext m1 m2 writeable. |
---|
1750 | ∀wb,wo,v. |
---|
1751 | ∀m1'. bestorev m1 (mk_pointer wb wo) v = Some ? m1' → |
---|
1752 | ∃m2'. bestorev m2 (mk_pointer wb wo) v = Some ? m2' ∧ |
---|
1753 | sr_memext m1' m2' writeable. |
---|
1754 | #m1 #m2 #writeable #Hext #wb #wo #v #m1' #Hstore1 |
---|
1755 | lapply (bestorev_success_nonempty … Hstore1) #Hwb_nonempty |
---|
1756 | cases (me_nonempty … Hext … Hwb_nonempty) #Hwb_nonempty2 #Hblocks_eq |
---|
1757 | cut (∃m2'. bestorev m2 (mk_pointer wb wo) v=Some mem m2') |
---|
1758 | [ cases Hwb_nonempty2 #Hwb_valid #Hnonempty normalize |
---|
1759 | normalize in Hwb_valid; >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta |
---|
1760 | whd in Hstore1:(??%%); normalize |
---|
1761 | cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H |
---|
1762 | cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H |
---|
1763 | cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1 |
---|
1764 | >Hblocks_eq in Hleb1 Hltb1 ⊢ %; #Hleb1 #Hltb1 >Hleb1 >Hltb1 |
---|
1765 | normalize nodelta /2 by ex_intro/ ] |
---|
1766 | * #m2' #Hstore2 %{m2'} @conj try assumption |
---|
1767 | whd in Hstore1:(??%%); |
---|
1768 | whd in Hstore2:(??%%); |
---|
1769 | cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H |
---|
1770 | cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H |
---|
1771 | cases (if_opt_inversion ???? Hstore2) -Hstore2 #block_valid2 #H |
---|
1772 | cases (if_opt_inversion ???? H) #Hin_bounds2 #Hm2' -H |
---|
1773 | cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1 |
---|
1774 | cases (andb_inversion … Hin_bounds2) #Hleb2 #Hltb2 -Hin_bounds2 |
---|
1775 | cut (valid_pointer m1 (mk_pointer wb wo)) |
---|
1776 | [ 1: normalize >block_valid1 normalize nodelta >Hleb1 normalize nodelta |
---|
1777 | >Hltb1 @I ] |
---|
1778 | #Hvalid |
---|
1779 | lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_in_writeable |
---|
1780 | destruct % |
---|
1781 | [ 1: #b #Hnonempty lapply (me_nonempty … Hext … (nonempty_block_update_ok2 … Hnonempty)) * #HA #HB |
---|
1782 | @conj |
---|
1783 | [ 1: @nonempty_block_update_ok // |
---|
1784 | | 2: normalize cases b in HB; #br #bid cases wb #wbr #wbid |
---|
1785 | cases br cases wbr normalize nodelta |
---|
1786 | @(eqZb_elim … bid wbid) normalize nodelta // |
---|
1787 | #Hid_eq >Hid_eq #Hblock_eq >Hblock_eq @refl ] |
---|
1788 | | 2: #b #Hmem lapply (me_writeable_valid … Hext … Hmem) @nonempty_block_update_ok |
---|
1789 | | 3: #b #Hnonempty lapply (nonempty_block_update_ok2 … Hnonempty) |
---|
1790 | @(me_not_writeable … Hext) |
---|
1791 | ] qed. |
---|
1792 | |
---|
1793 | (* If we successfuly store something in the first memory, then we can store it in the |
---|
1794 | * second one and the memory extension is preserved. *) |
---|
1795 | lemma memext_store_value_of_type : |
---|
1796 | ∀m, m_ext, m', writeable, ty, loc, off, v. |
---|
1797 | sr_memext m m_ext writeable → |
---|
1798 | store_value_of_type ty m loc off v = Some ? m' → |
---|
1799 | ∃m_ext'. store_value_of_type ty m_ext loc off v = Some ? m_ext' ∧ |
---|
1800 | sr_memext m' m_ext' writeable. |
---|
1801 | #m #m_ext #m' #writeable #ty #loc #off #v #Hext |
---|
1802 | (* case analysis on access mode of [ty] *) |
---|
1803 | cases ty |
---|
1804 | [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain |
---|
1805 | | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] |
---|
1806 | whd in ⊢ ((??%?) → (?%?)); |
---|
1807 | [ 1,5,6,7,8: #Habsurd destruct ] |
---|
1808 | whd in ⊢ (? → (??(λ_.?(??%?)?))); |
---|
1809 | lapply loc lapply off lapply Hext lapply m_ext lapply m lapply m' -loc -off -Hext -m_ext -m -m' |
---|
1810 | elim (fe_to_be_values ??) |
---|
1811 | [ 1,3,5,7: #m' #m #m_ext #Hext #off #loc normalize in ⊢ (% → ?); #Heq destruct (Heq) %{m_ext} @conj normalize // |
---|
1812 | | 2,4,6,8: #hd #tl #Hind #m' #m #m_ext #Hext #off #loc whd in ⊢ ((??%?) → ?); #H |
---|
1813 | cases (some_inversion ????? H) #m'' * #Hstore_eq #Hstoren_eq |
---|
1814 | lapply (bestorev_not_writeable_memory_ext … Hext … Hstore_eq) |
---|
1815 | * #m_ext'' * #Hstore_eq2 #Hext2 |
---|
1816 | lapply (Hind … Hext2 … Hstoren_eq) -Hind * #m_ext' * |
---|
1817 | #Hstoren' #Hext3 |
---|
1818 | %{m_ext'} @conj try assumption |
---|
1819 | whd in ⊢ (??%%); >Hstore_eq2 normalize nodelta |
---|
1820 | @Hstoren' |
---|
1821 | ] qed. |
---|
1822 | |
---|
1823 | lemma memext_store_value_of_type' : |
---|
1824 | ∀m, m_ext, m', writeable, ty, ptr, v. |
---|
1825 | sr_memext m m_ext writeable → |
---|
1826 | store_value_of_type' ty m ptr v = Some ? m' → |
---|
1827 | ∃m_ext'. store_value_of_type' ty m_ext ptr v = Some ? m_ext' ∧ |
---|
1828 | sr_memext m' m_ext' writeable. |
---|
1829 | #m #m_ext #m' #writeable #ty #p #v #Hext cases p #b #o |
---|
1830 | @memext_store_value_of_type @Hext qed. |
---|
1831 | |
---|
1832 | lemma memext_store_value_of_type_writeable : |
---|
1833 | ∀m1,m2,writeable. |
---|
1834 | ∀Hext:sr_memext m1 m2 writeable. |
---|
1835 | ∀wb. meml ? wb writeable → |
---|
1836 | ∀ty,off,v,m2'. store_value_of_type ty m2 wb off v = Some ? m2' → |
---|
1837 | sr_memext m1 m2' writeable. |
---|
1838 | #m1 #m2 #writeable #Hext #wb #Hmem |
---|
1839 | #ty #off #v #m2' |
---|
1840 | cases ty |
---|
1841 | [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain |
---|
1842 | | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] |
---|
1843 | whd in ⊢ ((??%?) → ?); |
---|
1844 | [ 1,5,6,7,8: #Habsurd destruct ] |
---|
1845 | lapply Hext lapply m1 lapply m2 lapply m2' lapply off -Hext -m1 -m2 -m2' -off -ty |
---|
1846 | elim (fe_to_be_values ??) |
---|
1847 | [ 1,3,5,7: #o #m2' #m2 #m1 #Hext normalize #Heq destruct assumption |
---|
1848 | | *: #hd #tl #Hind #o #m2_end #m2 #m1 #Hext whd in match (storen ???); #Hbestorev |
---|
1849 | cases (some_inversion ????? Hbestorev) #m2' * #Hbestorev #Hstoren |
---|
1850 | lapply (bestorev_writeable_memory_ext … Hext … o hd Hmem … Hbestorev) #Hext' |
---|
1851 | @(Hind … Hstoren) // |
---|
1852 | ] qed. |
---|
1853 | |
---|
1854 | (* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if |
---|
1855 | * the variable is not in a local environment, then we search into the global one. |
---|
1856 | * A proper "extension" of a local environment should be such that the extension |
---|
1857 | * does not collide with a given global env. |
---|
1858 | * To see the details of why we need that, see [exec_lvalue'], Evar id case. |
---|
1859 | *) |
---|
1860 | definition ext_fresh_for_genv ≝ |
---|
1861 | λ(ext : list (ident × type)). λ(ge : genv). |
---|
1862 | ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?. |
---|
1863 | |
---|
1864 | (* "generic" simulation relation on [res ?] *) |
---|
1865 | definition res_sim ≝ |
---|
1866 | λ(A : Type[0]). |
---|
1867 | λ(r1, r2 : res A). |
---|
1868 | ∀a. r1 = OK ? a → r2 = OK ? a. |
---|
1869 | |
---|
1870 | (* Specialisation of [res_sim] to match [exec_expr] *) |
---|
1871 | definition exec_expr_sim ≝ res_sim (val × trace). |
---|
1872 | |
---|
1873 | (* Specialisation of [res_sim] to match [exec_lvalue] *) |
---|
1874 | definition exec_lvalue_sim ≝ res_sim (block × offset × trace). |
---|
1875 | |
---|
1876 | 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. |
---|
1877 | #ty #m #b #o cases (load_value_of_type ty m b o) |
---|
1878 | [ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed. |
---|
1879 | |
---|
1880 | (* Simulation relations. *) |
---|
1881 | inductive switch_cont_sim : list (ident × type) → cont → cont → Prop ≝ |
---|
1882 | | swc_stop : |
---|
1883 | ∀new_vars. switch_cont_sim new_vars Kstop Kstop |
---|
1884 | | swc_seq : ∀s,k,k',u,s',new_vars. |
---|
1885 | fresh_for_statement s u → |
---|
1886 | switch_cont_sim new_vars k k' → |
---|
1887 | s' = ret_st ? (switch_removal s u) → |
---|
1888 | lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → |
---|
1889 | switch_cont_sim new_vars (Kseq s k) (Kseq s' k') |
---|
1890 | | swc_while : ∀e,s,k,k',u,s',new_vars. |
---|
1891 | fresh_for_statement (Swhile e s) u → |
---|
1892 | switch_cont_sim new_vars k k' → |
---|
1893 | s' = ret_st ? (switch_removal s u) → |
---|
1894 | lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → |
---|
1895 | switch_cont_sim new_vars (Kwhile e s k) (Kwhile e s' k') |
---|
1896 | | swc_dowhile : ∀e,s,k,k',u,s',new_vars. |
---|
1897 | fresh_for_statement (Sdowhile e s) u → |
---|
1898 | switch_cont_sim new_vars k k' → |
---|
1899 | s' = ret_st ? (switch_removal s u) → |
---|
1900 | lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → |
---|
1901 | switch_cont_sim new_vars (Kdowhile e s k) (Kdowhile e s' k') |
---|
1902 | | swc_for1 : ∀e,s1,s2,k,k',u,s',new_vars. |
---|
1903 | fresh_for_statement (Sfor Sskip e s1 s2) u → |
---|
1904 | switch_cont_sim new_vars k k' → |
---|
1905 | s' = (ret_st ? (switch_removal (Sfor Sskip e s1 s2) u)) → |
---|
1906 | lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → |
---|
1907 | switch_cont_sim new_vars (Kseq (Sfor Sskip e s1 s2) k) (Kseq s' k') |
---|
1908 | | swc_for2 : ∀e,s1,s2,k,k',u,result1,result2,new_vars. |
---|
1909 | fresh_for_statement (Sfor Sskip e s1 s2) u → |
---|
1910 | switch_cont_sim new_vars k k' → |
---|
1911 | result1 = ret_st ? (switch_removal s1 u) → |
---|
1912 | result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) → |
---|
1913 | lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → |
---|
1914 | switch_cont_sim new_vars (Kfor2 e s1 s2 k) (Kfor2 e result1 result2 k') |
---|
1915 | | swc_for3 : ∀e,s1,s2,k,k',u,result1,result2,new_vars. |
---|
1916 | fresh_for_statement (Sfor Sskip e s1 s2) u → |
---|
1917 | switch_cont_sim new_vars k k' → |
---|
1918 | result1 = ret_st ? (switch_removal s1 u) → |
---|
1919 | result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) → |
---|
1920 | lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → |
---|
1921 | switch_cont_sim new_vars (Kfor3 e s1 s2 k) (Kfor3 e result1 result2 k') |
---|
1922 | | swc_switch : ∀k,k',new_vars. |
---|
1923 | switch_cont_sim new_vars k k' → |
---|
1924 | switch_cont_sim new_vars (Kswitch k) (Kswitch k') |
---|
1925 | | swc_call : ∀en,en',r,f,k,k',old_vars,new_vars. (* Warning: possible caveat with environments here. *) |
---|
1926 | switch_cont_sim old_vars k k' → |
---|
1927 | old_vars = \snd (function_switch_removal f) → |
---|
1928 | disjoint_extension en en' old_vars → |
---|
1929 | switch_cont_sim |
---|
1930 | new_vars |
---|
1931 | (Kcall r f en k) |
---|
1932 | (Kcall r (\fst (function_switch_removal f)) en' k'). |
---|
1933 | |
---|
1934 | record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { |
---|
1935 | rg_find_symbol: ∀s. |
---|
1936 | find_symbol ? ge s = find_symbol ? ge' s; |
---|
1937 | rg_find_funct: ∀v,f. |
---|
1938 | find_funct ? ge v = Some ? f → |
---|
1939 | find_funct ? ge' v = Some ? (t f); |
---|
1940 | rg_find_funct_ptr: ∀b,f. |
---|
1941 | find_funct_ptr ? ge b = Some ? f → |
---|
1942 | find_funct_ptr ? ge' b = Some ? (t f) |
---|
1943 | }. |
---|
1944 | |
---|
1945 | inductive switch_state_sim (ge : genv) : state → state → Prop ≝ |
---|
1946 | | sws_state : |
---|
1947 | (* current statement *) |
---|
1948 | ∀sss_statement : statement. |
---|
1949 | (* label universe *) |
---|
1950 | ∀sss_lu : universe SymbolTag. |
---|
1951 | (* [sss_lu] must be fresh *) |
---|
1952 | ∀sss_lu_fresh : fresh_for_statement sss_statement sss_lu. |
---|
1953 | (* current function *) |
---|
1954 | ∀sss_func : function. |
---|
1955 | (* current function after translation *) |
---|
1956 | ∀sss_func_tr : function. |
---|
1957 | (* variables generated during conversion of the function *) |
---|
1958 | ∀sss_new_vars : list (ident × type). |
---|
1959 | (* statement of the transformation *) |
---|
1960 | ∀sss_func_hyp : 〈sss_func_tr, sss_new_vars〉 = function_switch_removal sss_func. |
---|
1961 | (* memory state before conversion *) |
---|
1962 | ∀sss_m : mem. |
---|
1963 | (* memory state after conversion *) |
---|
1964 | ∀sss_m_ext : mem. |
---|
1965 | (* environment before conversion *) |
---|
1966 | ∀sss_env : env. |
---|
1967 | (* environment after conversion *) |
---|
1968 | ∀sss_env_ext : env. |
---|
1969 | (* continuation before conversion *) |
---|
1970 | ∀sss_k : cont. |
---|
1971 | (* continuation after conversion *) |
---|
1972 | ∀sss_k_ext : cont. |
---|
1973 | (* writeable blocks *) |
---|
1974 | ∀sss_writeable : list block. |
---|
1975 | (* memory "injection" *) |
---|
1976 | ∀sss_mem_hyp : sr_memext sss_m sss_m_ext sss_writeable. |
---|
1977 | (* The extended environment does not interfer with the old one. *) |
---|
1978 | ∀sss_env_hyp : disjoint_extension sss_env sss_env_ext sss_new_vars. |
---|
1979 | (* The new variables are allocated to a size corresponding to their types. *) |
---|
1980 | ∀sss_new_alloc : |
---|
1981 | (∀v.meml ? v sss_new_vars → |
---|
1982 | ∀vb. lookup … sss_env_ext (\fst v) = Some ? vb → |
---|
1983 | valid_block sss_m_ext vb ∧ |
---|
1984 | low (blocks sss_m_ext vb) = OZ ∧ |
---|
1985 | high (blocks sss_m_ext vb) = sizeof (\snd v)). |
---|
1986 | (* Exit label for the enclosing switch, if any. Use for [break] conversion in switches. *) |
---|
1987 | ∀sss_enclosing_label : option label. |
---|
1988 | (* Extension blocks are writeable. *) |
---|
1989 | ∀sss_ext_write : lset_inclusion ? (lset_difference ? (blocks_of_env sss_env_ext) (blocks_of_env sss_env)) sss_writeable. |
---|
1990 | (* conversion of the current statement, using the variables produced during the conversion of the current function *) |
---|
1991 | ∀sss_result_rec. |
---|
1992 | ∀sss_result_hyp : switch_removal sss_statement sss_lu = sss_result_rec. |
---|
1993 | ∀sss_result. |
---|
1994 | sss_result = ret_st ? sss_result_rec → |
---|
1995 | (* inclusion of the locally produced new variables in the global new variables *) |
---|
1996 | lset_inclusion ? (ret_vars ? sss_result_rec) sss_new_vars → |
---|
1997 | (* simulation between the continuations before and after conversion. *) |
---|
1998 | ∀sss_k_hyp : switch_cont_sim sss_new_vars sss_k sss_k_ext. |
---|
1999 | ext_fresh_for_genv sss_new_vars ge → |
---|
2000 | switch_state_sim |
---|
2001 | ge |
---|
2002 | (State sss_func sss_statement sss_k sss_env sss_m) |
---|
2003 | (State sss_func_tr sss_result sss_k_ext sss_env_ext sss_m_ext) |
---|
2004 | | sws_callstate : |
---|
2005 | ∀ssc_fd. |
---|
2006 | ∀ssc_args. |
---|
2007 | ∀ssc_k. |
---|
2008 | ∀ssc_k_ext. |
---|
2009 | ∀ssc_m. |
---|
2010 | ∀ssc_m_ext. |
---|
2011 | ∀ssc_writeable. |
---|
2012 | ∀ssc_mem_hyp : sr_memext ssc_m ssc_m_ext ssc_writeable. |
---|
2013 | (match ssc_fd with |
---|
2014 | [ CL_Internal ssc_f ⇒ |
---|
2015 | switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext |
---|
2016 | | _ ⇒ True ]) → |
---|
2017 | switch_state_sim ge (Callstate ssc_fd ssc_args ssc_k ssc_m) |
---|
2018 | (Callstate (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext) |
---|
2019 | | sws_returnstate : |
---|
2020 | ∀ssr_result. |
---|
2021 | ∀ssr_k : cont. |
---|
2022 | ∀ssr_k_ext : cont. |
---|
2023 | ∀ssr_m : mem. |
---|
2024 | ∀ssr_m_ext : mem. |
---|
2025 | ∀ssr_writeable : list block. |
---|
2026 | ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext ssr_writeable. |
---|
2027 | ∀ssr_vars. |
---|
2028 | switch_cont_sim ssr_vars ssr_k ssr_k_ext → |
---|
2029 | switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext) |
---|
2030 | | sws_finalstate : ∀r. |
---|
2031 | switch_state_sim ge (Finalstate r) (Finalstate r). |
---|
2032 | |
---|
2033 | lemma call_cont_swremoval : ∀k,k',vars. |
---|
2034 | switch_cont_sim vars k k' → |
---|
2035 | switch_cont_sim vars (call_cont k) (call_cont k'). |
---|
2036 | #k0 #k0' #vars #K elim K /2/ |
---|
2037 | qed. |
---|
2038 | |
---|
2039 | (* [eventually ge P s tr] states that after a finite number of [exec_step], the |
---|
2040 | property P on states will be verified. *) |
---|
2041 | inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝ |
---|
2042 | | eventually_base : ∀s,t,s'. |
---|
2043 | exec_step ge s = Value io_out io_in ? 〈t, s'〉 → |
---|
2044 | P s' → |
---|
2045 | eventually ge P s t |
---|
2046 | | eventually_step : ∀s,t,s',t',trace. |
---|
2047 | exec_step ge s = Value io_out io_in ? 〈t, s'〉 → |
---|
2048 | eventually ge P s' t' → |
---|
2049 | trace = (t ⧺ t') → |
---|
2050 | eventually ge P s trace. |
---|
2051 | |
---|
2052 | (* [eventually] is not so nice to use directly, we would like to make the mandatory |
---|
2053 | * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not |
---|
2054 | to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *) |
---|
2055 | lemma eventually_now : ∀ge,P,s,t. |
---|
2056 | (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → |
---|
2057 | eventually ge P s t. |
---|
2058 | #ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP} (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *) |
---|
2059 | qed. |
---|
2060 | |
---|
2061 | lemma eventually_later : ∀ge,P,s,t. |
---|
2062 | (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) → |
---|
2063 | eventually ge P s t. |
---|
2064 | #ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq} |
---|
2065 | try assumption |
---|
2066 | qed. |
---|
2067 | |
---|
2068 | lemma exec_lvalue_expr_elim : |
---|
2069 | ∀r1,r2,Pok,Qok. |
---|
2070 | exec_lvalue_sim r1 r2 → |
---|
2071 | (∀val,trace. |
---|
2072 | match Pok 〈val,trace〉 with |
---|
2073 | [ Error err ⇒ True |
---|
2074 | | OK pvt ⇒ |
---|
2075 | let 〈pval,ptrace〉 ≝ pvt in |
---|
2076 | match Qok 〈val,trace〉 with |
---|
2077 | [ Error err ⇒ False |
---|
2078 | | OK qvt ⇒ |
---|
2079 | let 〈qval,qtrace〉 ≝ qvt in |
---|
2080 | ptrace = qtrace ∧ pval = qval |
---|
2081 | ] |
---|
2082 | ]) → |
---|
2083 | exec_expr_sim |
---|
2084 | (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) |
---|
2085 | (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). |
---|
2086 | #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); |
---|
2087 | elim r1 |
---|
2088 | [ 2: #error #_ #_ normalize #a #Habsurd destruct (Habsurd) |
---|
2089 | | 1: normalize nodelta #a #H lapply (H a (refl ??)) |
---|
2090 | #Hr2 >Hr2 normalize #H #a' elim a * #b #o #tr |
---|
2091 | lapply (H 〈b, o〉 tr) #H1 #H2 >H2 in H1; |
---|
2092 | normalize nodelta elim a' in H2; #pval #ptrace #Hpok |
---|
2093 | normalize nodelta cases (Qok 〈b,o,tr〉) |
---|
2094 | [ 2: #error normalize #Habsurd @(False_ind … Habsurd) |
---|
2095 | | 1: * #qval #qtrace normalize nodelta * #Htrace #Hval |
---|
2096 | destruct @refl |
---|
2097 | ] ] qed. |
---|
2098 | |
---|
2099 | |
---|
2100 | lemma exec_expr_expr_elim : |
---|
2101 | ∀r1,r2,Pok,Qok. |
---|
2102 | exec_expr_sim r1 r2 → |
---|
2103 | (∀val,trace. |
---|
2104 | match Pok 〈val,trace〉 with |
---|
2105 | [ Error err ⇒ True |
---|
2106 | | OK pvt ⇒ |
---|
2107 | let 〈pval,ptrace〉 ≝ pvt in |
---|
2108 | match Qok 〈val,trace〉 with |
---|
2109 | [ Error err ⇒ False |
---|
2110 | | OK qvt ⇒ |
---|
2111 | let 〈qval,qtrace〉 ≝ qvt in |
---|
2112 | ptrace = qtrace ∧ pval = qval |
---|
2113 | ] |
---|
2114 | ]) → |
---|
2115 | exec_expr_sim |
---|
2116 | (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) |
---|
2117 | (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). |
---|
2118 | #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); |
---|
2119 | elim r1 |
---|
2120 | [ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd) |
---|
2121 | | 1: normalize nodelta #a #H lapply (H a (refl ??)) |
---|
2122 | #Hr2 >Hr2 normalize nodelta #H |
---|
2123 | elim a in Hr2; #val #trace |
---|
2124 | lapply (H … val trace) |
---|
2125 | cases (Pok 〈val, trace〉) |
---|
2126 | [ 2: #error normalize #_ #_ #a' #Habsurd destruct (Habsurd) |
---|
2127 | | 1: * #pval #ptrace normalize nodelta |
---|
2128 | cases (Qok 〈val,trace〉) |
---|
2129 | [ 2: #error normalize #Hfalse @(False_ind … Hfalse) |
---|
2130 | | 1: * #qval #qtrace normalize nodelta * #Htrace_eq #Hval_eq |
---|
2131 | #Hr2_eq destruct #a #H @H |
---|
2132 | ] ] ] qed. |
---|
2133 | |
---|
2134 | lemma load_value_of_type_inj : ∀m1,m2,writeable,b,off,ty. |
---|
2135 | sr_memext m1 m2 writeable → ∀v. |
---|
2136 | load_value_of_type ty m1 b off = Some ? v → |
---|
2137 | load_value_of_type ty m2 b off = Some ? v. |
---|
2138 | #m1 #m2 #writeable #b #off #ty #Hinj #v |
---|
2139 | @(load_sim_fe ?? (sr_memext_load_sim … Hinj) (mk_pointer b off)) |
---|
2140 | qed. |
---|
2141 | |
---|
2142 | (* Conservation of the semantics of binary operators under memory extensions. |
---|
2143 | Tried to factorise it a bit but the play with indexes just becomes too messy. *) |
---|
2144 | lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,writeable. |
---|
2145 | ∀Hext:sr_memext m1 m2 writeable. ∀res. |
---|
2146 | sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res → |
---|
2147 | sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 = Some ? res. |
---|
2148 | #op #v1 #v2 #e1 #e2 #m1 #m2 #writeable #Hmemext #res cases op |
---|
2149 | whd in match (sem_binary_operation ??????); |
---|
2150 | try // |
---|
2151 | whd in match (sem_binary_operation ??????); |
---|
2152 | lapply (me_valid_pointers … Hmemext) |
---|
2153 | lapply (me_not_writeable_ptr … Hmemext) |
---|
2154 | elim m1 in Hmemext; #contents1 #nextblocks1 #Hnextpos1 |
---|
2155 | elim m2 #contents2 #nextblocks2 #Hnextpos2 |
---|
2156 | * #Hnonempty #Hwriteable #Hnot_writeable #Hnot_writeable_ptr #Hvalid |
---|
2157 | whd in match (sem_cmp ??????); |
---|
2158 | whd in match (sem_cmp ??????); |
---|
2159 | [ 1,2: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
2160 | normalize nodelta |
---|
2161 | [ 1,5: #sz #sg try // |
---|
2162 | | 2,6: #opt #ty |
---|
2163 | cases v1 normalize nodelta |
---|
2164 | [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ] |
---|
2165 | [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) |
---|
2166 | | 7,8: #H @H ] |
---|
2167 | cases v2 normalize nodelta |
---|
2168 | [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ] |
---|
2169 | [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) |
---|
2170 | | 7,8: #H @H ] |
---|
2171 | lapply (Hvalid ptr) |
---|
2172 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
2173 | [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] |
---|
2174 | #Hvalid' >(Hvalid' (refl ??)) |
---|
2175 | lapply (Hvalid ptr') |
---|
2176 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
2177 | [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
2178 | #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H |
---|
2179 | | 3,7: #fsz #H @H |
---|
2180 | | 4,8: #ty1 #ty2 #H @H ] |
---|
2181 | | 3,4: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
2182 | normalize nodelta |
---|
2183 | [ 1,5: #sz #sg try // |
---|
2184 | | 2,6: #opt #ty |
---|
2185 | cases v1 normalize nodelta |
---|
2186 | [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ] |
---|
2187 | [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) |
---|
2188 | | 7,8: #H @H ] |
---|
2189 | cases v2 normalize nodelta |
---|
2190 | [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ] |
---|
2191 | [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) |
---|
2192 | | 7,8: #H @H ] |
---|
2193 | lapply (Hvalid ptr) |
---|
2194 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
2195 | [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] |
---|
2196 | #Hvalid' >(Hvalid' (refl ??)) |
---|
2197 | lapply (Hvalid ptr') |
---|
2198 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
2199 | [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
2200 | #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H |
---|
2201 | | 3,7: #fsz #H @H |
---|
2202 | | 4,8: #ty1 #ty2 #H @H ] |
---|
2203 | | 5,6: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
2204 | normalize nodelta |
---|
2205 | [ 1,5: #sz #sg try // |
---|
2206 | | 2,6: #opt #ty |
---|
2207 | cases v1 normalize nodelta |
---|
2208 | [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ] |
---|
2209 | [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) |
---|
2210 | | 7,8: #H @H ] |
---|
2211 | cases v2 normalize nodelta |
---|
2212 | [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ] |
---|
2213 | [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) |
---|
2214 | | 7,8: #H @H ] |
---|
2215 | lapply (Hvalid ptr) |
---|
2216 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
2217 | [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] |
---|
2218 | #Hvalid' >(Hvalid' (refl ??)) |
---|
2219 | lapply (Hvalid ptr') |
---|
2220 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
2221 | [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
2222 | #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H |
---|
2223 | | 3,7: #fsz #H @H |
---|
2224 | | 4,8: #ty1 #ty2 #H @H ] |
---|
2225 | ] qed. |
---|
2226 | |
---|
2227 | (* Simulation relation on expressions *) |
---|
2228 | lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,writeable,ext. |
---|
2229 | ∀Hext:sr_memext m1 m2 writeable. |
---|
2230 | switch_removal_globals ? fundef_switch_removal ge ge' → |
---|
2231 | disjoint_extension en1 en2 ext → |
---|
2232 | (* disjoint_extension en1 en2 ext Hext → *) |
---|
2233 | ext_fresh_for_genv ext ge → |
---|
2234 | (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧ |
---|
2235 | (∀ed, ty. exec_lvalue_sim (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)). |
---|
2236 | #ge #ge' #en1 #m1 #en2 #m2 #writeable #ext #Hext #Hrelated #Hdisjoint (* #Hdisjoint *) #Hext_fresh_for_genv |
---|
2237 | @expr_lvalue_ind_combined |
---|
2238 | [ 1: #csz #cty #i #a1 |
---|
2239 | whd in match (exec_expr ????); elim cty |
---|
2240 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
2241 | normalize nodelta |
---|
2242 | [ 2: cases (eq_intsize csz sz) normalize nodelta |
---|
2243 | [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/ |
---|
2244 | | 2: #Habsurd destruct (Habsurd) ] |
---|
2245 | | 4,5,6: #_ #H destruct (H) |
---|
2246 | | *: #H destruct (H) ] |
---|
2247 | | 2: #ty #fl #a1 |
---|
2248 | whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/ |
---|
2249 | | 3: * |
---|
2250 | [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
2251 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
2252 | #ty whd in ⊢ (% → ?); #Hind try @I |
---|
2253 | whd in match (Plvalue ???); |
---|
2254 | [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1 |
---|
2255 | cases (exec_lvalue' ge en1 m1 ? ty) in Hind; |
---|
2256 | [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
2257 | | 1,3,5: normalize nodelta #b1 #H lapply (H b1 (refl ??)) #Heq >Heq |
---|
2258 | normalize nodelta |
---|
2259 | elim b1 * #bl1 #o1 #tr1 (* elim b2 * #bl2 #o2 #tr2 *) |
---|
2260 | whd in match (load_value_of_type' ???); |
---|
2261 | whd in match (load_value_of_type' ???); |
---|
2262 | lapply (load_value_of_type_inj m1 m2 writeable bl1 o1 ty Hext) |
---|
2263 | cases (load_value_of_type ty m1 bl1 o1) |
---|
2264 | [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2265 | | 2,4,6: #v #H normalize in ⊢ (% → ?); #Heq destruct (Heq) |
---|
2266 | >(H v (refl ??)) @refl |
---|
2267 | ] ] ] |
---|
2268 | | 4: #v #ty whd * * #b #o #tr |
---|
2269 | whd in match (exec_lvalue' ?????); |
---|
2270 | whd in match (exec_lvalue' ?????); cases Hdisjoint * |
---|
2271 | #HA #HB #HC lapply (HA v) lapply (HB v) lapply (HC v) -HA -HB -HC |
---|
2272 | lapply (Hext_fresh_for_genv v) |
---|
2273 | cases (mem_assoc_env v ext) #Hglobal |
---|
2274 | [ 1: >(Hglobal (refl ??)) #_ #HB #HA >(HA (refl ??)) normalize |
---|
2275 | #Habsurd destruct |
---|
2276 | | 2: normalize nodelta #Hsim #_ #_ |
---|
2277 | cases (lookup ?? en1 v) in Hsim; normalize nodelta |
---|
2278 | [ 1: #Hlookup2 <(Hlookup2 (refl ??)) normalize nodelta |
---|
2279 | lapply (rg_find_symbol … Hrelated v) #Heq_find_sym >Heq_find_sym |
---|
2280 | #H @H |
---|
2281 | | 2: #blo #Hlookup2 <(Hlookup2 (refl ??)) #Heq normalize nodelta @Heq ] ] |
---|
2282 | | 5: #e #ty whd in ⊢ (% → %); |
---|
2283 | whd in match (exec_lvalue' ?????); |
---|
2284 | whd in match (exec_lvalue' ?????); |
---|
2285 | cases (exec_expr ge en1 m1 e) |
---|
2286 | [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' #H @H |
---|
2287 | | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ] |
---|
2288 | | 6: #ty #e #ty' |
---|
2289 | #Hsim @(exec_lvalue_expr_elim … Hsim) |
---|
2290 | cases ty |
---|
2291 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
2292 | * #b #o normalize nodelta try /2 by I/ |
---|
2293 | #tr @conj try @refl |
---|
2294 | | 7: #ty #op #e |
---|
2295 | #Hsim @(exec_expr_expr_elim … Hsim) #v #trace |
---|
2296 | cases (sem_unary_operation op v (typeof e)) normalize nodelta |
---|
2297 | try @I |
---|
2298 | #v @conj @refl |
---|
2299 | | 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 |
---|
2300 | @(exec_expr_expr_elim … Hsim1) #v #trace |
---|
2301 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
2302 | [ 2: #error // ] |
---|
2303 | * #pval #ptrace normalize in ⊢ (% → ?); #Hsim2 |
---|
2304 | whd in match (m_bind ?????); |
---|
2305 | >(Hsim2 ? (refl ??)) |
---|
2306 | whd in match (m_bind ?????); |
---|
2307 | lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 writeable Hext) |
---|
2308 | cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1) |
---|
2309 | [ 1: #_ // ] #val #H >(H val (refl ??)) |
---|
2310 | normalize destruct @conj @refl |
---|
2311 | | 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim) |
---|
2312 | #v #tr |
---|
2313 | cut (exec_cast m1 v (typeof e) cast_ty = exec_cast m2 v (typeof e) cast_ty) |
---|
2314 | [ @refl ] |
---|
2315 | #Heq >Heq |
---|
2316 | cases (exec_cast m2 v (typeof e) cast_ty) |
---|
2317 | [ 2: // |
---|
2318 | | 1: #v normalize @conj @refl ] |
---|
2319 | | 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 |
---|
2320 | @(exec_expr_expr_elim … Hsim1) #v #tr |
---|
2321 | cases (exec_bool_of_val ? (typeof e1)) #b |
---|
2322 | [ 2: normalize @I ] |
---|
2323 | cases b normalize nodelta |
---|
2324 | whd in match (m_bind ?????); |
---|
2325 | whd in match (m_bind ?????); |
---|
2326 | normalize nodelta |
---|
2327 | [ 1: (* true branch *) |
---|
2328 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
2329 | [ 2: #error normalize #_ @I |
---|
2330 | | 1: * #e2v #e2tr normalize #H >(H ? (refl ??)) normalize nodelta |
---|
2331 | @conj @refl ] |
---|
2332 | | 2: (* false branch *) |
---|
2333 | cases (exec_expr ge en1 m1 e3) in Hsim3; |
---|
2334 | [ 2: #error normalize #_ @I |
---|
2335 | | 1: * #e3v #e3tr normalize #H >(H ? (refl ??)) normalize nodelta |
---|
2336 | @conj @refl ] ] |
---|
2337 | | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 |
---|
2338 | @(exec_expr_expr_elim … Hsim1) #v #tr |
---|
2339 | cases (exec_bool_of_val v (typeof e1)) |
---|
2340 | [ 2,4: #error normalize @I ] |
---|
2341 | * |
---|
2342 | whd in match (m_bind ?????); |
---|
2343 | whd in match (m_bind ?????); |
---|
2344 | [ 2,3: normalize @conj try @refl ] |
---|
2345 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
2346 | [ 2,4: #error #_ normalize @I ] |
---|
2347 | * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta >(H2 ? (refl ??)) |
---|
2348 | normalize nodelta |
---|
2349 | cases (exec_bool_of_val v2 (typeof e2)) |
---|
2350 | [ 2,4: #error normalize @I ] |
---|
2351 | * normalize @conj @refl |
---|
2352 | | 13: #ty #ty' cases ty |
---|
2353 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n |
---|
2354 | | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
2355 | whd in match (exec_expr ????); whd #a #H @H |
---|
2356 | | 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr |
---|
2357 | whd in match (exec_lvalue' ?????); |
---|
2358 | whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty); |
---|
2359 | whd in match (typeof ?); |
---|
2360 | cases aggregty in Hsim; |
---|
2361 | [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n' |
---|
2362 | | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ] |
---|
2363 | normalize nodelta #Hsim |
---|
2364 | [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ] |
---|
2365 | whd in match (m_bind ?????); |
---|
2366 | whd in match (m_bind ?????); |
---|
2367 | whd in match (exec_lvalue ge en1 m1 (Expr ed ?)); |
---|
2368 | cases (exec_lvalue' ge en1 m1 ed ?) in Hsim; |
---|
2369 | [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] |
---|
2370 | * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H |
---|
2371 | whd in match (exec_lvalue ge' en2 m2 (Expr ed ?)); |
---|
2372 | >(H ? (refl ??)) normalize nodelta #H @H |
---|
2373 | | 15: #ty #l #e #Hsim |
---|
2374 | @(exec_expr_expr_elim … Hsim) #v #tr normalize nodelta @conj // |
---|
2375 | | 16: * |
---|
2376 | [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
2377 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
2378 | #ty normalize in ⊢ (% → ?); |
---|
2379 | [ 3,4,13: @False_ind |
---|
2380 | | *: #_ normalize #a1 #Habsurd @Habsurd ] |
---|
2381 | ] qed. |
---|
2382 | |
---|
2383 | lemma exec_lvalue_sim_aux : ∀ge,ge',env,env_ext,m,m_ext. |
---|
2384 | (∀ed,ty. exec_lvalue_sim (exec_lvalue' ge env m ed ty) |
---|
2385 | (exec_lvalue' ge' env_ext m_ext ed ty)) → |
---|
2386 | ∀e. exec_lvalue_sim (exec_lvalue ge env m e) |
---|
2387 | (exec_lvalue ge' env_ext m_ext e). |
---|
2388 | #ge #ge' #env #env_ext #m #m_ext #H * #ed #ty @H qed. |
---|
2389 | |
---|
2390 | lemma exec_expr_sim_to_exec_exprlist : |
---|
2391 | ∀ge,ge',en1,en2,m1,m2. |
---|
2392 | (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) → |
---|
2393 | ∀l. res_sim ? (exec_exprlist ge en1 m1 l) (exec_exprlist ge' en2 m2 l). |
---|
2394 | #ge #ge' #en1 #en2 #m1 #m2 #Hsim #l elim l |
---|
2395 | [ 1: whd #a #Heq normalize in Heq ⊢ %; destruct @refl |
---|
2396 | | 2: #hd #tl #Hind whd * #lv #tr whd in ⊢ ((??%?) → (??%?)); |
---|
2397 | lapply (Hsim hd) |
---|
2398 | cases (exec_expr ge en1 m1 hd) |
---|
2399 | [ 2: #error normalize #_ #Habsurd destruct (Habsurd) |
---|
2400 | | 1: * #v #vtr whd in ⊢ (% → ?); #Hsim >(Hsim ? (refl ??)) |
---|
2401 | normalize nodelta |
---|
2402 | cases (exec_exprlist ge en1 m1 tl) in Hind; |
---|
2403 | [ 2: #error normalize #_ #Habsurd destruct (Habsurd) |
---|
2404 | | 1: #a normalize #H >(H ? (refl ??)) #Heq destruct normalize @refl |
---|
2405 | ] |
---|
2406 | ] |
---|
2407 | ] qed. |
---|
2408 | |
---|
2409 | (* The return type of any function is invariant under switch removal *) |
---|
2410 | lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f. |
---|
2411 | #f elim f #ty #args #vars #body whd in match (function_switch_removal ?); |
---|
2412 | cases (switch_removal ??) * #stmt #fvs #u @refl |
---|
2413 | qed. |
---|
2414 | |
---|
2415 | (* Similar stuff for fundefs *) |
---|
2416 | lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd). |
---|
2417 | * // * #ty #args #vars #body whd in ⊢ (??%%); |
---|
2418 | whd in match (function_switch_removal ?); cases (switch_removal ??) * #st #u |
---|
2419 | normalize nodelta #u @refl |
---|
2420 | qed. |
---|
2421 | |
---|
2422 | lemma while_fresh_lift : ∀e,s,u. |
---|
2423 | fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u. |
---|
2424 | #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??)); |
---|
2425 | cases (max_of_expr e) #e cases (max_of_statement s) #s normalize |
---|
2426 | cases (leb e s) try /2/ |
---|
2427 | qed. |
---|
2428 | |
---|
2429 | (* |
---|
2430 | lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0). |
---|
2431 | #e0 #s0 #us0 normalize |
---|
2432 | cases (switch_removal s0 us0) * #body #newvars #u' normalize // |
---|
2433 | qed.*) |
---|
2434 | |
---|
2435 | lemma dowhile_fresh_lift : ∀e,s,u. |
---|
2436 | fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u. |
---|
2437 | #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??)); |
---|
2438 | cases (max_of_expr e) #e cases (max_of_statement s) #s normalize |
---|
2439 | cases (leb e s) try /2/ |
---|
2440 | qed. |
---|
2441 | |
---|
2442 | (* |
---|
2443 | lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0). |
---|
2444 | #e0 #s0 #us0 normalize |
---|
2445 | cases (switch_removal s0 us0) * #body #newvars #u' normalize // |
---|
2446 | qed.*) |
---|
2447 | |
---|
2448 | lemma for_fresh_lift : ∀cond,step,body,u. |
---|
2449 | fresh_for_statement step u → |
---|
2450 | fresh_for_statement body u → |
---|
2451 | fresh_for_expression cond u → |
---|
2452 | fresh_for_statement (Sfor Sskip cond step body) u. |
---|
2453 | #cond #step #body #u |
---|
2454 | whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????)); |
---|
2455 | cases (max_of_statement step) #s |
---|
2456 | cases (max_of_statement body) #b |
---|
2457 | cases (max_of_expr cond) #c |
---|
2458 | whd in match (max_of_statement Sskip); |
---|
2459 | >(max_id_commutative least_identifier) |
---|
2460 | >max_id_one_neutral normalize nodelta |
---|
2461 | normalize elim u #u |
---|
2462 | cases (leb s b) cases (leb c b) cases (leb c s) try /2/ |
---|
2463 | qed. |
---|
2464 | |
---|
2465 | (* |
---|
2466 | lemma for_commute : ∀e,stm1,stm2,u,uA. |
---|
2467 | (uA=\snd (switch_removal stm1 u)) → |
---|
2468 | sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)). |
---|
2469 | #e #stm1 #stm2 #u #uA #HuA |
---|
2470 | whd in match (sw_rem (Sfor ????) u); |
---|
2471 | whd in match (switch_removal ??); |
---|
2472 | destruct |
---|
2473 | normalize in match (\snd (switch_removal Sskip u)); |
---|
2474 | whd in match (sw_rem stm1 u); |
---|
2475 | cases (switch_removal stm1 u) |
---|
2476 | * #stm1' #fresh_vars #uA normalize nodelta |
---|
2477 | whd in match (sw_rem stm2 uA); |
---|
2478 | cases (switch_removal stm2 uA) |
---|
2479 | * #stm2' #fresh_vars2 #uB normalize nodelta |
---|
2480 | // |
---|
2481 | qed.*) |
---|
2482 | |
---|
2483 | lemma simplify_is_not_skip : ∀s. s ≠ Sskip → ∀u. ∃pf. is_Sskip (ret_st ? (switch_removal s u)) = inr ?? pf. |
---|
2484 | * |
---|
2485 | [ 1: * #H @(False_ind … (H (refl ??))) ] |
---|
2486 | try /2/ |
---|
2487 | [ 1: #s1 #s2 #_ #u normalize |
---|
2488 | cases (switch_removal ? ?) * #a #b #c normalize nodelta |
---|
2489 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
2490 | /2 by ex_intro/ |
---|
2491 | | 2: #e #s1 #s2 #_ #u normalize |
---|
2492 | cases (switch_removal ? ?) * #a #b #c normalize nodelta |
---|
2493 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
2494 | /2 by ex_intro/ |
---|
2495 | | 3,4: #e #s #_ #u normalize |
---|
2496 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
2497 | /2 by ex_intro/ |
---|
2498 | | 5: #s1 #e #s2 #s3 #_ #u normalize |
---|
2499 | cases (switch_removal ? ?) * #a #b #c normalize nodelta |
---|
2500 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
2501 | cases (switch_removal ? ?) * #h #i #j normalize nodelta |
---|
2502 | /2 by ex_intro/ |
---|
2503 | | 6: #e #ls #_ #u normalize |
---|
2504 | cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta |
---|
2505 | cases (fresh ??) #e #f normalize nodelta |
---|
2506 | cases (fresh ? f) #g #h normalize nodelta |
---|
2507 | cases (produce_cond ????) * #k #l #m normalize nodelta |
---|
2508 | /2 by ex_intro/ |
---|
2509 | | 7,8: #ls #st #_ #u normalize |
---|
2510 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
2511 | /2 by ex_intro/ |
---|
2512 | ] qed. |
---|
2513 | |
---|
2514 | (* |
---|
2515 | lemma sw_rem_commute : ∀stm,u. |
---|
2516 | (\fst (\fst (switch_removal stm u))) = sw_rem stm u. |
---|
2517 | #stm #u whd in match (sw_rem stm u); // qed. |
---|
2518 | *) |
---|
2519 | |
---|
2520 | lemma fresh_for_statement_inv : |
---|
2521 | ∀u,s. fresh_for_statement s u → |
---|
2522 | match u with |
---|
2523 | [ mk_universe p ⇒ le (p0 one) p ]. |
---|
2524 | * #p #s whd in match (fresh_for_statement ??); |
---|
2525 | cases (max_of_statement s) #s |
---|
2526 | normalize /2/ qed. |
---|
2527 | |
---|
2528 | lemma fresh_for_Sskip : |
---|
2529 | ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u. |
---|
2530 | #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. |
---|
2531 | |
---|
2532 | lemma fresh_for_Sbreak : |
---|
2533 | ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u. |
---|
2534 | #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. |
---|
2535 | |
---|
2536 | lemma fresh_for_Scontinue : |
---|
2537 | ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u. |
---|
2538 | #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. |
---|
2539 | |
---|
2540 | (* |
---|
2541 | lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉. |
---|
2542 | #s #u elim (switch_removal s u) * #res #fvs #u' |
---|
2543 | %{res} %{fvs} %{u'} // |
---|
2544 | qed. |
---|
2545 | |
---|
2546 | lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉. |
---|
2547 | #switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u' |
---|
2548 | %{res} %{fvs} %{u'} // |
---|
2549 | qed. |
---|
2550 | *) |
---|
2551 | |
---|
2552 | lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉. |
---|
2553 | #e #ls #u #exit_label cases (produce_cond e ls u exit_label) * |
---|
2554 | #s #lab #u' %{s} %{lab} %{u'} // |
---|
2555 | qed. |
---|
2556 | |
---|
2557 | (* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *) |
---|
2558 | lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false. |
---|
2559 | * * * |
---|
2560 | [ 1,5,9: #H @(False_ind … (H (refl ??))) |
---|
2561 | | *: #_ normalize @refl ] |
---|
2562 | qed. |
---|
2563 | |
---|
2564 | lemma exec_expr_int : ∀ge,e,m,expr. |
---|
2565 | (∃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〉)). |
---|
2566 | #ge #e #m #expr cases (exec_expr ge e m expr) |
---|
2567 | [ 2: #error %2 #sz #n #tr % #H destruct (H) |
---|
2568 | | 1: * #val #trace cases val |
---|
2569 | [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl |
---|
2570 | | 3: #fl | 4: | 5: #ptr ] |
---|
2571 | %2 #sz #n #tr % #H destruct (H) |
---|
2572 | ] qed. |
---|
2573 | |
---|
2574 | lemma switch_removal_elim : ∀s,u. ∃s',fvs',u'. switch_removal s u = 〈s',fvs',u'〉. |
---|
2575 | #s #u cases (switch_removal s u) * #s' #fvs' #u' |
---|
2576 | %{s'} %{fvs'} %{u'} @refl |
---|
2577 | qed. |
---|
2578 | |
---|
2579 | lemma switch_removal_branches_elim : ∀ls,u. ∃ls',fvs',u'. switch_removal_branches ls u = 〈ls',fvs',u'〉. |
---|
2580 | #ls #u cases (switch_removal_branches ls u) * * #ls' #fvs' #u' /4 by ex_intro/ qed. |
---|
2581 | |
---|
2582 | lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed. |
---|
2583 | |
---|
2584 | lemma simplify_switch_elim : ∀e,ls,u. ∃res,u'. simplify_switch e ls u = 〈res, u'〉. |
---|
2585 | #e #ls #u cases (simplify_switch e ls u) #res #u /3 by ex_intro/ qed. |
---|
2586 | |
---|
2587 | lemma store_int_success : |
---|
2588 | ∀b,m,sz,sg,i. valid_block m b → low (blocks m b) = OZ → high (blocks m b) = sizeof (Tint sz sg) → |
---|
2589 | ∃m'. store_value_of_type (Tint sz sg) m b zero_offset (Vint sz i) = Some ? m'. |
---|
2590 | #b #m #sz #sg |
---|
2591 | cases sz |
---|
2592 | [ 1: #i #Hvalid #Hlow #Hhigh |
---|
2593 | whd in match (store_value_of_type ?????); |
---|
2594 | whd in match (fe_to_be_values ??); |
---|
2595 | normalize nodelta |
---|
2596 | normalize in match (size_intsize ?); |
---|
2597 | whd in match (bytes_of_bitvector ??); |
---|
2598 | lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i |
---|
2599 | <(vsplit_prod … Heq_i) normalize nodelta |
---|
2600 | >(BitVector_O … ri) whd in match (storen ???); |
---|
2601 | lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte li) ?) |
---|
2602 | [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true |
---|
2603 | >unfold_low_bound >unfold_high_bound >Hlow >Hhigh |
---|
2604 | >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta |
---|
2605 | @Zlt_to_Zltb_true // ] |
---|
2606 | * #m' #Hbestorev >Hbestorev %{m'} @refl |
---|
2607 | | 2: #i #Hvalid #Hlow #Hhigh |
---|
2608 | whd in match (store_value_of_type ?????); |
---|
2609 | whd in match (fe_to_be_values ??); |
---|
2610 | normalize nodelta |
---|
2611 | normalize in match (size_intsize ?); |
---|
2612 | whd in match (bytes_of_bitvector ??); |
---|
2613 | lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i |
---|
2614 | <(vsplit_prod … Heq_i) normalize nodelta whd in match (storen ???); |
---|
2615 | lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte li) ?) |
---|
2616 | [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true |
---|
2617 | >unfold_low_bound >unfold_high_bound >Hlow >Hhigh |
---|
2618 | >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta |
---|
2619 | @Zlt_to_Zltb_true // ] |
---|
2620 | * #m0 #Hbestorev >Hbestorev normalize nodelta |
---|
2621 | whd in match (bytes_of_bitvector ??); |
---|
2622 | lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri |
---|
2623 | <(vsplit_prod … Heq_ri) normalize nodelta |
---|
2624 | cases (mem_bounds_invariant_after_bestorev … Hbestorev) * * * #Hnext0 #Hblocks0 #_ #_ #_ |
---|
2625 | lapply (valid_pointer_to_bestorev_ok m0 |
---|
2626 | (mk_pointer b (mk_offset |
---|
2627 | [[false; false; false; false; false; false; false; false; |
---|
2628 | false; false; false; false; false; false; false; true]])) |
---|
2629 | (BVByte rli) ?) |
---|
2630 | [ 1: whd in match (valid_pointer ??); >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true |
---|
2631 | cases (Hblocks0 b) #HA #HB |
---|
2632 | >unfold_low_bound >unfold_high_bound >HA >HB >Hlow >Hhigh normalize nodelta |
---|
2633 | @Zlt_to_Zltb_true normalize // ] |
---|
2634 | * #m1 #Hbestorev1 %{m1} whd in ⊢ (??(???%)?); whd in match (storen ???); |
---|
2635 | normalize in match (shift_pointer ???); >Hbestorev1 normalize nodelta |
---|
2636 | @refl |
---|
2637 | | 3: #i #Hvalid #Hlow #Hhigh |
---|
2638 | whd in match (store_value_of_type ?????); |
---|
2639 | whd in match (fe_to_be_values ??); |
---|
2640 | normalize nodelta |
---|
2641 | normalize in match (size_intsize ?); |
---|
2642 | whd in match (bytes_of_bitvector ??); |
---|
2643 | lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i |
---|
2644 | <(vsplit_prod … Heq_i) normalize nodelta whd in match (storen ???); |
---|
2645 | lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte iA) ?) |
---|
2646 | [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true |
---|
2647 | >unfold_low_bound >unfold_high_bound >Hlow >Hhigh |
---|
2648 | >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta |
---|
2649 | @Zlt_to_Zltb_true // ] |
---|
2650 | * #m0 #Hbestorev >Hbestorev normalize nodelta |
---|
2651 | whd in match (bytes_of_bitvector ??); |
---|
2652 | lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB |
---|
2653 | <(vsplit_prod … Heq_iB) normalize nodelta |
---|
2654 | cases (mem_bounds_invariant_after_bestorev … Hbestorev) * * * #Hnext0 #Hblocks0 #_ #_ #_ |
---|
2655 | lapply (valid_pointer_to_bestorev_ok m0 |
---|
2656 | (shift_pointer 2 (mk_pointer b zero_offset) (bitvector_of_nat 2 1)) |
---|
2657 | (BVByte iC) ?) |
---|
2658 | [ 1: whd in match (valid_pointer ??); >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true |
---|
2659 | cases (Hblocks0 b) #HA #HB |
---|
2660 | >unfold_low_bound >unfold_high_bound >HA >HB >Hlow >Hhigh normalize nodelta |
---|
2661 | @Zlt_to_Zltb_true normalize // ] |
---|
2662 | * #m1 #Hbestorev1 whd in ⊢ (??(λ_.??(???%)?)); whd in match (storen ???); |
---|
2663 | normalize in match (shift_pointer 2 (mk_pointer b zero_offset) (bitvector_of_nat 2 1)); |
---|
2664 | >Hbestorev1 normalize nodelta |
---|
2665 | lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD |
---|
2666 | whd in match (bytes_of_bitvector ??); |
---|
2667 | <(vsplit_prod … Heq_iD) normalize nodelta |
---|
2668 | whd in ⊢ (??(λ_.??(???%)?)); |
---|
2669 | whd in match (storen ???); |
---|
2670 | cases (mem_bounds_invariant_after_bestorev … Hbestorev1) * * * #Hnext1 #Hblocks1 #_ #_ #_ |
---|
2671 | lapply (valid_pointer_to_bestorev_ok m1 |
---|
2672 | (shift_pointer 2 (mk_pointer b (mk_offset |
---|
2673 | [[ false; false; false; false; false; false; false; false; false; false; |
---|
2674 | false; false; false; false; false; true ]])) |
---|
2675 | (bitvector_of_nat 2 1)) |
---|
2676 | (BVByte iE) ?) |
---|
2677 | [ 1: normalize in match (shift_pointer ???); whd in match (valid_pointer ??); |
---|
2678 | >Hnext1 >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) |
---|
2679 | >andb_lsimpl_true cases (Hblocks1 b) #HA #HB cases (Hblocks0 b) #HC #HD |
---|
2680 | >unfold_low_bound >unfold_high_bound >HA >HB >HC >HD >Hlow >Hhigh normalize nodelta |
---|
2681 | @Zlt_to_Zltb_true normalize // ] |
---|
2682 | * #m2 #Hbestorev2 >Hbestorev2 normalize nodelta |
---|
2683 | whd in match (bytes_of_bitvector ??); |
---|
2684 | lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF |
---|
2685 | <(vsplit_prod … Heq_iF) normalize nodelta |
---|
2686 | >(BitVector_O … iH) whd in ⊢ (??(λ_.??(???%)?)); |
---|
2687 | whd in match (storen ???); |
---|
2688 | cases (mem_bounds_invariant_after_bestorev … Hbestorev2) * * * #Hnext2 #Hblocks2 #_ #_ #_ |
---|
2689 | lapply (valid_pointer_to_bestorev_ok m2 |
---|
2690 | (shift_pointer 2 (shift_pointer 2 (mk_pointer b (mk_offset |
---|
2691 | [[ false; false; false; false; false; false; false; false; false; false; |
---|
2692 | false; false; false; false; false; true ]])) |
---|
2693 | (bitvector_of_nat 2 1)) (bitvector_of_nat 2 1)) |
---|
2694 | (BVByte iG) ?) |
---|
2695 | [ 1: normalize in match (shift_pointer ???); whd in match (valid_pointer ??); |
---|
2696 | >Hnext2 >Hnext1 >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) |
---|
2697 | >andb_lsimpl_true cases (Hblocks2 b) #HA #HB cases (Hblocks1 b) #HC #HD cases (Hblocks0 b) #HE #HF |
---|
2698 | >unfold_low_bound >unfold_high_bound >HA >HB >HC >HD >HE >HF >Hlow >Hhigh normalize nodelta |
---|
2699 | @Zlt_to_Zltb_true normalize // ] |
---|
2700 | * #m3 #Hbestorev3 >Hbestorev3 normalize nodelta %{m3} @refl |
---|
2701 | ] qed. |
---|
2702 | |
---|
2703 | |
---|
2704 | (* Main theorem. |
---|
2705 | 9th November 2012 |
---|
2706 | We decided to interrupt the development of this particular proof. What follows is a description of what |
---|
2707 | has to be done in order to finish it. |
---|
2708 | |
---|
2709 | What has been done up to now is the simulation proof for all "easy" cases, that do not interact with the |
---|
2710 | switch removal per se, plus a bit of switch. This still implies propagating the memory extension through |
---|
2711 | each statement (except switch), as well as various invariants that are needed for the switch case. |
---|
2712 | |
---|
2713 | The proof for the switch case has been started. Here is how I picture the simulation proof. |
---|
2714 | The simulation proof must be broken down in several steps. The source statement executes as this for the first step : |
---|
2715 | |
---|
2716 | mem, env, k |
---|
2717 | ----------------------------------------------------- |
---|
2718 | switch(e) case_list ===> |
---|
2719 | e ⇓ Vint i, |
---|
2720 | case_list' ← select_switch sz n case_list; |
---|
2721 | Result = State (seq_of_labeled_statement case_list') (Kswitch k) env mem |
---|
2722 | |
---|
2723 | The resulting statement executes like this. |
---|
2724 | |
---|
2725 | mem ⊕ writeable, env ⊕ ext, k' |
---|
2726 | fresh ∈ dom(ext) |
---|
2727 | ext(fresh) ∈ writeable |
---|
2728 | ----------------------------------------------------- |
---|
2729 | fresh = e; |
---|
2730 | if(e == case0) { --- |
---|
2731 | substatement0; | |
---|
2732 | goto next0; | |
---|
2733 | } else { }; | |
---|
2734 | if(e == case1) { |- = converted_cases |
---|
2735 | label next0: | |
---|
2736 | substatement1; | |
---|
2737 | goto next1; | |
---|
2738 | } else { }; --- |
---|
2739 | ... ===> |
---|
2740 | Result = State (fresh = e) (Kseq converted_cases k) (env ⊕ ext) (mem ⊕ writeable) |
---|
2741 | ===> |
---|
2742 | fresh ⇓ Loc l; |
---|
2743 | e ⇓ Vint i; |
---|
2744 | m' → store_value_of_type' (typeof a1) m l (Vint i) |
---|
2745 | Result = State Sskip (Kseq converted_cases k) (env ⊕ ext) (m' ⊕ writeable) |
---|
2746 | ===> |
---|
2747 | Result = State converted_cases k (env ⊕ ext) (m' ⊕ writeable) |
---|
2748 | This has been done. But this state is still not equivalent with the source one. |
---|
2749 | TODO 1: we must prove that after a finite number of Ssequence in [converted_cases], we |
---|
2750 | stumble upon a "if(e == casen) { blahblah } else {}; foo" that corresponds to "(seq_of_labeled_statement case_list')" |
---|
2751 | (remember that "case_list'" has been truncated to the case corresponding to "i"). |
---|
2752 | TODO 2: the resulting pair of states will not be in the standard simulation relation currently defined in |
---|
2753 | [switch_state_sim]. We must come up with an additional set of relations with enough informations |
---|
2754 | to handle the gotos : |
---|
2755 | 1. the gotos from one if to the other avoiding the execution of conditions |
---|
2756 | 2. most importantly, the gotos into which "break"s have been converted ! |
---|
2757 | This particular subset of the simulation will need some equations allowing to prove that |
---|
2758 | the current continuation actually contains a label corresponding to the break. |
---|
2759 | Note that when encountering e.g. a while loop inside a converted case, breaks should stop |
---|
2760 | beeing converted to gotos and we should go to the 'standard' simulation relation. |
---|
2761 | TODO 3: some standard cases remain after that, nothing special (halt case ...). |
---|
2762 | |
---|
2763 | This should be about it. TODO 1 and 2 will probably require some form of induction over switch cases ... |
---|
2764 | *) |
---|
2765 | |
---|
2766 | theorem switch_removal_correction : |
---|
2767 | ∀ge,ge'. |
---|
2768 | switch_removal_globals ? fundef_switch_removal ge ge' → |
---|
2769 | ∀s1,s1',tr,s2. |
---|
2770 | switch_state_sim ge s1 s1' → |
---|
2771 | exec_step ge s1 = Value … 〈tr,s2〉 → |
---|
2772 | ∃n. after_n_steps (S n) … clight_exec ge' s1' |
---|
2773 | (λtr',s2'. tr = tr' ∧ switch_state_sim ge' s2 s2'). |
---|
2774 | #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state |
---|
2775 | inversion Hsim_state |
---|
2776 | [ 1: (* regular state *) |
---|
2777 | #sss_statement #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars |
---|
2778 | #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp |
---|
2779 | #sss_env_hyp #sss_new_alloc #sss_enclosing_label #sss_writeable_hyp #sss_result_rec #sss_result_hyp |
---|
2780 | #sss_result #sss_result_proj #sss_incl #sss_k_hyp #Hext_fresh_for_ge |
---|
2781 | #Hs1_eq #Hs1_eq' |
---|
2782 | elim (sim_related_globals … ge ge' |
---|
2783 | sss_env sss_m sss_env_ext sss_m_ext sss_writeable sss_new_vars |
---|
2784 | sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge) |
---|
2785 | #Hsim_expr #Hsim_lvalue #_ |
---|
2786 | (* II. Case analysis on the statement. *) |
---|
2787 | cases sss_statement in sss_lu_fresh sss_result_hyp; |
---|
2788 | (* Perform the intros for the statements *) |
---|
2789 | [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body |
---|
2790 | | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body |
---|
2791 | | 14: #lab | 15: #cost #body ] |
---|
2792 | #sss_lu_fresh #sss_result_hyp |
---|
2793 | [ 1: (* Skip statement *) |
---|
2794 | whd in match (switch_removal ??) in sss_result_hyp; >sss_result_proj <sss_result_hyp |
---|
2795 | (* III. Case analysis on the continuation. *) |
---|
2796 | inversion sss_k_hyp normalize nodelta |
---|
2797 | [ 1: #new_vars #Hnew_vars_eq #Hk #Hk' #_ #Hexec_step %{0} whd whd in ⊢ (??%?); |
---|
2798 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
2799 | >fn_return_simplify |
---|
2800 | whd in match (exec_step ??) in Hexec_step; |
---|
2801 | (* IV. Case analysis on the return type *) |
---|
2802 | cases (fn_return sss_func) in Hexec_step; |
---|
2803 | [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain |
---|
2804 | | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] |
---|
2805 | normalize nodelta |
---|
2806 | whd in ⊢ ((??%?) → ?); |
---|
2807 | [ 1: #H destruct (H) % try @refl |
---|
2808 | /3 by sws_returnstate, swc_stop, memext_free_extended_environment, memory_ext_writeable_eq/ |
---|
2809 | | *: #Habsurd destruct (Habsurd) ] |
---|
2810 | | 2: #s #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #Hsss_k_hyp |
---|
2811 | #Hexec_step %{0} whd |
---|
2812 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
2813 | whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl |
---|
2814 | <sss_func_hyp |
---|
2815 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
2816 | %1{u (refl ? (switch_removal s u))} try assumption try @refl |
---|
2817 | #id #Hmem lapply (Hext_fresh_for_ge id Hmem) #Hfind <(rg_find_symbol … Hrelated id) @Hfind |
---|
2818 | | 3: #cond #body #k #k' #fgen #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
2819 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
2820 | #Hexec_step %{0} whd whd in Hexec_step; |
---|
2821 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
2822 | whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl |
---|
2823 | %1{ ((switch_removal (Swhile cond body) fgen))} try assumption try @refl |
---|
2824 | [ 1: <sss_func_hyp @refl |
---|
2825 | | 2: destruct normalize cases (switch_removal ??) * #body' #fvs' #u' @refl |
---|
2826 | | 3: whd in match (switch_removal ??); |
---|
2827 | cases (switch_removal body fgen) in Hincl; * #body' #fvs' #fgen' normalize nodelta #H @H |
---|
2828 | | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
2829 | | 4: #cond #body #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
2830 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
2831 | #Hexec_step %{0} whd whd in Hexec_step:(??%?) ⊢ (??%?); |
---|
2832 | cases (bindIO_inversion ??????? Hexec_step) #x1 * #Hexec |
---|
2833 | >(Hsim_expr … Hexec) |
---|
2834 | >bindIO_Value cases (exec_bool_of_val ??) |
---|
2835 | [ 2: #err normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] |
---|
2836 | #b whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
2837 | cases b normalize nodelta #H whd in H:(??%%) ⊢ %; destruct (H) |
---|
2838 | try @conj try @refl |
---|
2839 | [ 1: %{u … (switch_removal (Sdowhile cond body) u)} try assumption try // |
---|
2840 | [ 1: destruct normalize cases (switch_removal body u) * #body' #fvs' #u' @refl |
---|
2841 | | 2: whd in match (switch_removal ??); |
---|
2842 | cases (switch_removal body u) in Hincl; * #body' #fvs' #u' normalize nodelta #H @H |
---|
2843 | | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
2844 | | 2: %{u … (switch_removal Sskip u) } try assumption try // |
---|
2845 | [ 1: @(fresh_for_Sskip … Hfresh) |
---|
2846 | | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ] |
---|
2847 | | 5: #cond #stmt1 #stmt2 #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ |
---|
2848 | #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
2849 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
2850 | #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step) |
---|
2851 | @conj try @refl |
---|
2852 | %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // try assumption |
---|
2853 | #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
2854 | | 6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars |
---|
2855 | #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
2856 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
2857 | #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl |
---|
2858 | %1{u … new_vars … sss_writeable (switch_removal stmt1 u)} try assumption try // |
---|
2859 | [ 1: lapply (fresh_to_substatements … Hfresh) normalize * * // |
---|
2860 | | 2: whd in match (switch_removal ??) in Hincl; |
---|
2861 | cases (switch_removal stmt1 u) in Hincl; * #stmt1' #fvs1' #u' normalize nodelta |
---|
2862 | cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' normalize nodelta |
---|
2863 | whd in match (ret_vars ??); /2 by All_append_l/ |
---|
2864 | | 3: @(swc_for3 … u) // |
---|
2865 | | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
2866 | | 7: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars |
---|
2867 | #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
2868 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
2869 | #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl |
---|
2870 | %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} |
---|
2871 | try // try assumption |
---|
2872 | [ 1: whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize |
---|
2873 | cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize |
---|
2874 | cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' @refl |
---|
2875 | | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
2876 | | 8: #k #k' #new_vars #Hsimcont #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
2877 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
2878 | #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl |
---|
2879 | %1{sss_lu … new_vars … sss_writeable} try // try assumption |
---|
2880 | [ 1: destruct (sss_result_hyp) @refl |
---|
2881 | | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
2882 | | 9: #en #en' #r #f #k #k' #old_vars #new_vars #Hsimcont #Hnew_vars_eq #Hdisjoint_k #_ |
---|
2883 | #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
2884 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
2885 | #Hexec %{0} whd in Hexec:(??%?) ⊢ %; whd in ⊢ (??%?); |
---|
2886 | >(prod_eq_lproj ????? sss_func_hyp) >fn_return_simplify |
---|
2887 | cases (fn_return sss_func) in Hexec; normalize nodelta |
---|
2888 | [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain |
---|
2889 | | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] |
---|
2890 | #Hexec whd in Hexec:(??%?); destruct (Hexec) whd @conj try @refl |
---|
2891 | /3 by sws_returnstate, swc_call, memext_free_extended_environment/ |
---|
2892 | ] |
---|
2893 | | 2: (* Assign statement *) |
---|
2894 | lapply (exec_lvalue_sim_aux … Hsim_lvalue) #Hsim |
---|
2895 | #Hexec %{0} whd in sss_result_hyp:(??%?); |
---|
2896 | cases (bindIO_inversion ??????? Hexec) #xl * #Heq_lhs #Hexec_lhs |
---|
2897 | cases (bindIO_inversion ??????? Hexec_lhs) #xr * #Heq_rhs #Hexec_rhs -Hexec_lhs |
---|
2898 | cases (bindIO_inversion ??????? Hexec_rhs) #m' * #Heq_store #Hexec_store -Hexec_rhs |
---|
2899 | whd whd in Hexec_store:(??%%) ⊢ (??%?); >sss_result_proj <sss_result_hyp normalize nodelta |
---|
2900 | >(Hsim … Heq_lhs) whd in match (m_bind ?????); |
---|
2901 | >(Hsim_expr … Heq_rhs) >bindIO_Value |
---|
2902 | lapply (memext_store_value_of_type' sss_m sss_m_ext m' sss_writeable (typeof lhs) (\fst xl) (\fst xr) sss_mem_hyp ?) |
---|
2903 | [ 1: cases (store_value_of_type' ????) in Heq_store; |
---|
2904 | [ 1: normalize #Habsurd destruct (Habsurd) |
---|
2905 | | 2: #m normalize #Heq destruct (Heq) @refl ] ] |
---|
2906 | * #m_ext' * #Heq_store' #Hnew_ext >Heq_store' whd in match (m_bind ?????); |
---|
2907 | whd destruct @conj try @refl |
---|
2908 | %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip sss_lu) } |
---|
2909 | try // try assumption |
---|
2910 | [ 1: @(fresh_for_Sskip … sss_lu_fresh) |
---|
2911 | | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
2912 | | 2: #v #Hmem #vb #Hlookup lapply (sss_new_alloc v Hmem vb Hlookup) * * #Hvb #Hlow #Hhigh |
---|
2913 | cut (store_value_of_type' (typeof lhs) sss_m (\fst xl) (\fst xr) = Some ? m') |
---|
2914 | [ cases (store_value_of_type' (typeof lhs) sss_m (\fst xl) (\fst xr)) in Heq_store; |
---|
2915 | [ whd in ⊢ ((??%%) → ?); #Habsurd destruct |
---|
2916 | | #m0 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl ] ] |
---|
2917 | #Hstore lapply (mem_bounds_after_store_value_of_type' … Heq_store') * |
---|
2918 | #HA #HB cases (HB vb) #Hlow' #Hhigh' @conj try @conj |
---|
2919 | [ 2: >Hlow' in Hlow; // |
---|
2920 | | 3: >Hhigh' in Hhigh; // |
---|
2921 | | 1: whd >HA @Hvb ] ] |
---|
2922 | | 3: (* Call statement *) |
---|
2923 | #Hexec %{0} whd in sss_result_hyp:(??%?); destruct (sss_result_hyp) |
---|
2924 | whd whd in ⊢ (??%?); >sss_result_proj normalize nodelta |
---|
2925 | whd in Hexec:(??%?); |
---|
2926 | cases (bindIO_inversion ??????? Hexec) #xfunc * #Heq_func #Hexec_func |
---|
2927 | cases (bindIO_inversion ??????? Hexec_func) #xargs * #Heq_args #Hexec_args |
---|
2928 | cases (bindIO_inversion ??????? Hexec_args) #called_fundef * #Heq_fundef #Hexec_typeeq |
---|
2929 | cases (bindIO_inversion ??????? Hexec_typeeq) #Htype_eq * #Heq_assert #Hexec_ret |
---|
2930 | >(Hsim_expr … Heq_func) whd in match (m_bind ?????); |
---|
2931 | >(exec_expr_sim_to_exec_exprlist … Hsim_expr … Heq_args) |
---|
2932 | whd in ⊢ (??%?); |
---|
2933 | >(rg_find_funct … Hrelated … (opt_to_io_Value … Heq_fundef)) |
---|
2934 | whd in ⊢ (??%?); <fundef_type_simplify >Heq_assert |
---|
2935 | whd in ⊢ (??%?); -Hexec -Hexec_func -Hexec_args -Hexec_typeeq lapply Hexec_ret -Hexec_ret |
---|
2936 | @(option_ind … retv) normalize nodelta |
---|
2937 | [ 1: whd in ⊢ ((??%%) → (??%%)); #Heq whd destruct (Heq) @conj try @refl |
---|
2938 | %2{sss_writeable … sss_mem_hyp} |
---|
2939 | cases called_fundef |
---|
2940 | [ 2: #id #tl #ty @I |
---|
2941 | | 1: #called_function whd |
---|
2942 | cut (sss_func_tr = \fst (function_switch_removal sss_func)) |
---|
2943 | [ 1: <sss_func_hyp @refl ] #H >H -H |
---|
2944 | cut (sss_new_vars = \snd (function_switch_removal sss_func)) |
---|
2945 | [ 1: <sss_func_hyp @refl ] #H >H -H |
---|
2946 | @(swc_call … sss_k_hyp) try assumption |
---|
2947 | <sss_func_hyp @refl ] |
---|
2948 | | 2: #ret_expr #Hexec_ret_expr |
---|
2949 | cases (bindIO_inversion ??????? Hexec_ret_expr) #xret * #Heq_ret |
---|
2950 | whd in ⊢ ((??%%) → (??%%)); #H destruct (H) |
---|
2951 | >(exec_lvalue_sim_aux … Hsim_lvalue … Heq_ret) |
---|
2952 | whd in ⊢ (??%?); whd @conj try @refl |
---|
2953 | cut (sss_func_tr = \fst (function_switch_removal sss_func)) |
---|
2954 | [ 1: <sss_func_hyp @refl ] #H >H -H |
---|
2955 | @(sws_callstate … sss_writeable … sss_mem_hyp) |
---|
2956 | cases called_fundef |
---|
2957 | [ 2: #id #tl #ty @I |
---|
2958 | | 1: #called_function whd |
---|
2959 | cut (sss_func_tr = \fst (function_switch_removal sss_func)) |
---|
2960 | [ 1: <sss_func_hyp @refl ] #H >H -H |
---|
2961 | cut (sss_new_vars = \snd (function_switch_removal sss_func)) |
---|
2962 | [ 1: <sss_func_hyp @refl ] #H >H -H |
---|
2963 | @(swc_call … sss_k_hyp) try assumption |
---|
2964 | <sss_func_hyp @refl ] ] |
---|
2965 | | 4: (* Sequence statement *) |
---|
2966 | #Hexec %{0} whd in sss_result_hyp:(??%?); whd whd in Hexec:(??%?) ⊢ (??%?); destruct (Hexec) |
---|
2967 | >sss_result_proj <sss_result_hyp |
---|
2968 | cases (switch_removal_elim stm1 sss_lu) #stm1' * #fvs1' * #u' #HeqA >HeqA normalize nodelta |
---|
2969 | cases (switch_removal_elim stm2 u') #stm2' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta |
---|
2970 | normalize @conj try @refl %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} |
---|
2971 | try // try assumption |
---|
2972 | [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * // |
---|
2973 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta |
---|
2974 | /2 by All_append_l/ |
---|
2975 | | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
2976 | @(swc_seq … u') try // |
---|
2977 | [ 2: >HeqB @refl |
---|
2978 | | 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * #_ @fresher_for_univ |
---|
2979 | lapply (switch_removal_fte stm1 sss_lu) >HeqA #H @H |
---|
2980 | | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta |
---|
2981 | /2 by All_append_r/ |
---|
2982 | ] |
---|
2983 | | 5: (* If-then-else *) |
---|
2984 | #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp |
---|
2985 | cases (switch_removal_elim iftrue sss_lu) #iftrue' * #fvs1' * #u' #HeqA >HeqA normalize nodelta |
---|
2986 | cases (switch_removal_elim iffalse u') #iffalse' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta |
---|
2987 | whd whd in ⊢ (??%?); |
---|
2988 | cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond |
---|
2989 | cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hresult |
---|
2990 | whd in Hresult:(??%%); destruct (Hresult) |
---|
2991 | >(Hsim_expr … Heq_cond) >bindIO_Value |
---|
2992 | >Heq_bool whd in match (m_bind ?????); whd @conj try @refl |
---|
2993 | cases b normalize nodelta |
---|
2994 | [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try // |
---|
2995 | [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize // |
---|
2996 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta |
---|
2997 | /2 by All_append_l/ |
---|
2998 | | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
2999 | | 2: %1{u' … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqB} try assumption try // |
---|
3000 | [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize #_ |
---|
3001 | @fresher_for_univ lapply (switch_removal_fte iftrue sss_lu) >HeqA #H @H |
---|
3002 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta |
---|
3003 | /2 by All_append_r/ |
---|
3004 | | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ] |
---|
3005 | | 6: (* While loop *) |
---|
3006 | #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp |
---|
3007 | >sss_result_proj <sss_result_hyp whd |
---|
3008 | cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond |
---|
3009 | cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool whd in ⊢ ((??%%) → ?); |
---|
3010 | cases (switch_removal_elim body sss_lu) #body' * #fvs1' * #u' #HeqA >HeqA normalize nodelta |
---|
3011 | whd in ⊢ (? → (??%?)); |
---|
3012 | >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool |
---|
3013 | whd in match (m_bind ?????); cases b normalize nodelta #Hresult destruct (Hresult) |
---|
3014 | whd @conj try @refl |
---|
3015 | [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try // |
---|
3016 | [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize // |
---|
3017 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H |
---|
3018 | | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
3019 | | 3: @(swc_while … sss_lu) try // |
---|
3020 | [ 1: >HeqA @refl |
---|
3021 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H ] |
---|
3022 | ] |
---|
3023 | | 2: %{… sss_func_hyp … (switch_removal Sskip u')} try assumption try // |
---|
3024 | [ 1: lapply (switch_removal_fte body sss_lu) >HeqA #Hfte whd in match (ret_u ??) in Hfte; |
---|
3025 | @(fresher_for_univ … Hfte) @(fresh_for_Sskip … sss_lu_fresh) |
---|
3026 | | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ] |
---|
3027 | | 7: (* do while loop *) |
---|
3028 | #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp |
---|
3029 | >sss_result_proj <sss_result_hyp whd destruct (Hexec) whd in ⊢ (??%?); |
---|
3030 | cases (switch_removal_elim body sss_lu) #body' * #fvs1' * #u' #HeqA >HeqA normalize nodelta |
---|
3031 | whd @conj try @refl |
---|
3032 | %1{sss_lu … sss_func_hyp … (switch_removal body sss_lu) } |
---|
3033 | try assumption try // |
---|
3034 | [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * // |
---|
3035 | | 2: >HeqA @refl |
---|
3036 | | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H |
---|
3037 | | 5: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
3038 | | 4: @(swc_dowhile … sss_lu) try assumption try // |
---|
3039 | [ 1: >HeqA @refl |
---|
3040 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H |
---|
3041 | ] ] |
---|
3042 | | 8: (* for loop *) |
---|
3043 | #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp |
---|
3044 | >sss_result_proj <sss_result_hyp whd destruct (Hexec) whd in ⊢ (??%?); |
---|
3045 | cases (switch_removal_elim init sss_lu) #init' * #fvs1' * #u' #HeqA >HeqA normalize nodelta |
---|
3046 | cases (switch_removal_elim step u') #step' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta |
---|
3047 | cases (switch_removal_elim body u'') #body' * #fvs3' * #u''' #HeqC >HeqC normalize nodelta |
---|
3048 | lapply Hexec |
---|
3049 | @(match is_Sskip init with |
---|
3050 | [ inl Heq ⇒ ? |
---|
3051 | | inr Hneq ⇒ ? |
---|
3052 | ]) normalize nodelta |
---|
3053 | [ 2: lapply (simplify_is_not_skip … Hneq sss_lu) >HeqA * #pf |
---|
3054 | whd in match (ret_st ??) in ⊢ ((??%%) → ?); #Hneq >Hneq normalize nodelta |
---|
3055 | #Hexec' whd in Hexec':(??%%); destruct (Hexec') whd @conj try @refl |
---|
3056 | %1{sss_lu … sss_func_hyp (switch_removal init sss_lu)} try assumption try // |
---|
3057 | [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * * * // |
---|
3058 | | 2: >HeqA @refl |
---|
3059 | | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta |
---|
3060 | >HeqB normalize nodelta >HeqC normalize nodelta |
---|
3061 | /2 by All_append_l/ |
---|
3062 | | 4: @(swc_for1 … u') try assumption try // |
---|
3063 | [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #HW #HX #HY #HZ |
---|
3064 | @for_fresh_lift |
---|
3065 | [ 1: @(fresher_for_univ … HY) |
---|
3066 | | 2: @(fresher_for_univ … HZ) |
---|
3067 | | 3: @(fresher_for_univ … HX) ] |
---|
3068 | lapply (switch_removal_fte init sss_lu) >HeqA #Hs @Hs |
---|
3069 | | 2: normalize >HeqB normalize nodelta >HeqC @refl |
---|
3070 | | 3: lapply sss_incl <sss_result_hyp |
---|
3071 | whd in match (ret_vars ??) in ⊢ (% → %); |
---|
3072 | whd in match (switch_removal ??) in ⊢ (% → %); |
---|
3073 | >HeqA normalize nodelta >HeqB normalize nodelta >HeqC |
---|
3074 | normalize nodelta #H /2 by All_append_r/ |
---|
3075 | ] ] |
---|
3076 | | 1: -Hexec #Hexec' cases (bindIO_inversion ??????? Hexec') #condres * #Heq_cond #Hexec_cond |
---|
3077 | cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool |
---|
3078 | destruct (Heq) normalize in HeqA; lapply HeqA #HeqA' destruct (HeqA') |
---|
3079 | normalize nodelta |
---|
3080 | >(Hsim_expr … Heq_cond) whd in ⊢ ((??%?) → ?); #Hexec' |
---|
3081 | whd in match (m_bind ?????); >Heq_bool |
---|
3082 | cases b in Hexec'; normalize nodelta whd in match (bindIO ??????); |
---|
3083 | normalize #Hexec'' destruct (Hexec'') @conj try @refl |
---|
3084 | [ 1: %1{u'' … sss_func_hyp (switch_removal body u'')} try assumption try // |
---|
3085 | [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #_ #_ #_ |
---|
3086 | @fresher_for_univ lapply (switch_removal_fte step u') >HeqB |
---|
3087 | #H @H |
---|
3088 | | 2: >HeqC @refl |
---|
3089 | | 3: lapply sss_incl <sss_result_hyp |
---|
3090 | whd in match (ret_vars ??) in ⊢ (% → %); |
---|
3091 | whd in match (switch_removal ??) in ⊢ (% → %); normalize nodelta |
---|
3092 | >HeqB normalize nodelta >HeqC normalize nodelta |
---|
3093 | /2 by All_append_r/ |
---|
3094 | | 4: @(swc_for2 … u') try assumption |
---|
3095 | [ 1: >HeqB @refl |
---|
3096 | | 2: >HeqB >HeqC @refl |
---|
3097 | | 3: lapply sss_incl <sss_result_hyp |
---|
3098 | whd in match (ret_vars ??) in ⊢ (% → %); |
---|
3099 | whd in match (switch_removal ??) in ⊢ (% → %); normalize nodelta |
---|
3100 | >HeqB normalize nodelta >HeqC normalize nodelta #H @H |
---|
3101 | ] |
---|
3102 | ] |
---|
3103 | | 2: %1{u' … sss_func_hyp … (switch_removal Sskip u')} try assumption try // |
---|
3104 | [ 1: @(fresh_for_Sskip … sss_lu_fresh) ] ] ] |
---|
3105 | #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
3106 | | 9: (* break *) |
---|
3107 | (* sss_enclosing_label TODO : switch case *) |
---|
3108 | #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta |
---|
3109 | lapply Hexec -Hexec |
---|
3110 | inversion sss_k_hyp |
---|
3111 | [ 1: #new_vars #Hv #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Habsurd destruct (Habsurd) |
---|
3112 | | 2: #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars_eq |
---|
3113 | #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
3114 | destruct |
---|
3115 | %1{sss_lu … (switch_removal Sbreak sss_lu)} try assumption try // |
---|
3116 | | 3,4: #e #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ |
---|
3117 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
3118 | destruct |
---|
3119 | %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try // |
---|
3120 | | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ |
---|
3121 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
3122 | destruct |
---|
3123 | %1{sss_lu … (switch_removal Sbreak sss_lu)} try assumption try // |
---|
3124 | | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk' |
---|
3125 | #Hres1 #Hres2 #Hincl #_ #Hnew_vars |
---|
3126 | #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
3127 | destruct |
---|
3128 | %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try // |
---|
3129 | | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk' #_ #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); |
---|
3130 | #Heq destruct (Heq) whd @conj try @refl destruct |
---|
3131 | %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try // |
---|
3132 | | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold #Hdisjoint #_ |
---|
3133 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); |
---|
3134 | #Heq destruct (Heq) ] |
---|
3135 | #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
3136 | | 10: (* continue *) |
---|
3137 | #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta |
---|
3138 | lapply Hexec -Hexec |
---|
3139 | inversion sss_k_hyp |
---|
3140 | [ 1: #new_vars #Hv #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Habsurd destruct (Habsurd) |
---|
3141 | | 2: #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars_eq |
---|
3142 | #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
3143 | destruct |
---|
3144 | %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // |
---|
3145 | | 3: #ek #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ |
---|
3146 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
3147 | destruct |
---|
3148 | %1{uk … (switch_removal (Swhile ek sk) uk)} try assumption try // |
---|
3149 | [ 1: normalize cases (switch_removal sk uk) * #sk' #fvs' #uk' @refl |
---|
3150 | | 2: whd in match (switch_removal ??); lapply Hincl |
---|
3151 | cases (switch_removal sk uk) * #body' #fvs' #uk' |
---|
3152 | /2 by All_append_r/ ] |
---|
3153 | | 4: #ek #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ |
---|
3154 | #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Hexec |
---|
3155 | cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond |
---|
3156 | cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hexec_bool |
---|
3157 | >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool whd in match (m_bind ?????); |
---|
3158 | cases b in Hexec_bool; normalize nodelta whd in ⊢ ((??%?) → ?); |
---|
3159 | #Heq whd whd in Heq:(??%%); destruct (Heq) @conj try @refl |
---|
3160 | [ 1: destruct %1{uk … (switch_removal (Sdowhile ek sk) uk)} try assumption try // |
---|
3161 | [ 1: normalize cases (switch_removal sk uk) * #body' #fvs' #uk' @refl |
---|
3162 | | 2: whd in match (switch_removal ??); lapply Hincl cases (switch_removal sk uk) |
---|
3163 | * #body' #fvs' #uk' #H @H |
---|
3164 | ] |
---|
3165 | | 2: destruct %1{uk … (switch_removal Sskip uk)} try assumption try // |
---|
3166 | try @(fresh_for_Sskip … Hfresh_suk) ] |
---|
3167 | | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ |
---|
3168 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
3169 | destruct %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // |
---|
3170 | | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk' #Hres1 #Hres2 #Hincl #_ |
---|
3171 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
3172 | destruct %1{uk … (switch_removal s1k uk)} try assumption try // |
---|
3173 | [ 1: cases (fresh_to_substatements … Hfresh_suk) * * // |
---|
3174 | | 2: lapply Hincl whd in match (ret_vars ??) in ⊢ (% → ?); |
---|
3175 | whd in match (switch_removal ??); |
---|
3176 | cases (switch_removal s1k uk) * #s1k' #fvs1' #uk' normalize nodelta |
---|
3177 | cases (switch_removal s2k uk') * #s2k' #fvs2' #uk'' normalize nodelta |
---|
3178 | /2 by All_append_l/ |
---|
3179 | | 3: @(swc_for3 … uk) try assumption try // |
---|
3180 | ] |
---|
3181 | | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk #_ #Hnew_vars_eq #Hk #Hk' #_ |
---|
3182 | whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) |
---|
3183 | whd @conj try @refl destruct |
---|
3184 | %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // |
---|
3185 | | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold_vars_eq #Hdisjoint |
---|
3186 | #_ #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); |
---|
3187 | #Heq destruct (Heq) ] |
---|
3188 | #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
3189 | | 11: (* return *) |
---|
3190 | #Hexec %{0} whd whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec |
---|
3191 | >sss_result_proj <sss_result_hyp normalize nodelta |
---|
3192 | cases retval in sss_lu_fresh sss_result_hyp; normalize nodelta |
---|
3193 | [ 1: #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?)); |
---|
3194 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
3195 | >fn_return_simplify |
---|
3196 | cases (fn_return sss_func) normalize nodelta |
---|
3197 | [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain |
---|
3198 | | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] |
---|
3199 | [ 1: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj try @refl |
---|
3200 | /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/ |
---|
3201 | | *: #Habsurd destruct (Habsurd) ] |
---|
3202 | | 2: #ret_expr #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?)); |
---|
3203 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
3204 | >fn_return_simplify |
---|
3205 | @(match type_eq_dec (fn_return sss_func) Tvoid with |
---|
3206 | [ inl H ⇒ ? |
---|
3207 | | inr H ⇒ ? ]) normalize nodelta |
---|
3208 | [ 1: #Habsurd destruct (Habsurd) |
---|
3209 | | 2: #Hexec |
---|
3210 | cases (bindIO_inversion ??????? Hexec) #retres * #Heq_ret #Hexec_ret |
---|
3211 | whd in Hexec_ret:(??%%); destruct (Hexec_ret) |
---|
3212 | >(Hsim_expr … Heq_ret) whd in match (m_bind ?????); whd |
---|
3213 | @conj try @refl |
---|
3214 | /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/ |
---|
3215 | ] ] |
---|
3216 | | 12: (* switch ! at long last *) |
---|
3217 | #Hexec whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec |
---|
3218 | >sss_result_proj <sss_result_hyp normalize nodelta #Hexec |
---|
3219 | cases (bindIO_inversion ??????? Hexec) * #condval #condtrace -Hexec |
---|
3220 | cases condval normalize nodelta |
---|
3221 | [ 1: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
3222 | | 3: #f * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
3223 | | 4: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
3224 | | 5: #ptr * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ] |
---|
3225 | #sz #i * #Hexec_eq #Heq |
---|
3226 | cut (∃sg. typeof cond = Tint sz sg) whd in Heq:(??%%); destruct (Heq) |
---|
3227 | [ 1: cases (typeof cond) in Heq; normalize nodelta |
---|
3228 | [ 1: | 2: #sz' #sg' | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty |
---|
3229 | | 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ] |
---|
3230 | [ 2: cases (sz_eq_dec ??) normalize nodelta #H |
---|
3231 | [ 2: #Habsurd destruct |
---|
3232 | | 1: destruct (H) #_ %{sg'} try @refl ] |
---|
3233 | | *: #Habsurd destruct (Habsurd) ] ] |
---|
3234 | * #sg #Htypeof_cond >Htypeof_cond in Heq; normalize nodelta >sz_eq_identity normalize nodelta |
---|
3235 | #Heq whd in Heq:(??%%); |
---|
3236 | cases (bindIO_inversion ??????? Heq) #switchcases_truncated * #Heq1 #Heq2 -Heq |
---|
3237 | whd in Heq1:(??%%); whd in Heq2:(??%%); |
---|
3238 | cut (select_switch sz i switchcases = Some ? switchcases_truncated) |
---|
3239 | [ 1: cases (select_switch sz i switchcases) in Heq1; normalize nodelta |
---|
3240 | [ 1: #Habsurd destruct | 2: #ls #Heq destruct (Heq) @refl ] ] |
---|
3241 | -Heq1 #Heq_select_switch destruct (Heq2) |
---|
3242 | cases (switch_removal_branches_elim … switchcases sss_lu) #switchcases' * #fvs' * #u' #Hbranch_eq |
---|
3243 | >Hbranch_eq normalize nodelta |
---|
3244 | cases (fresh_elim … u') #new * #u'' #Hfresh_eq >Hfresh_eq normalize nodelta |
---|
3245 | cases (simplify_switch_elim (Expr (Evar new) (Tint sz sg)) switchcases' u'') #simplified * #u''' |
---|
3246 | #Hswitch_eq >Hswitch_eq normalize nodelta |
---|
3247 | %{2} whd whd in ⊢ (??%?); |
---|
3248 | (* A. Execute lhs of assign, i.e. fresh variable that will hold value of condition *) |
---|
3249 | whd in match (exec_lvalue ????); |
---|
3250 | (* show that the resulting ident is in the memory extension and that the lookup succeeds *) |
---|
3251 | >Hbranch_eq in sss_result_hyp; normalize nodelta |
---|
3252 | >Hfresh_eq normalize nodelta >Hswitch_eq normalize nodelta >Htypeof_cond >Hswitch_eq |
---|
3253 | normalize nodelta #sss_result_hyp |
---|
3254 | <sss_result_hyp in sss_incl; whd in match (ret_vars ??); #sss_incl |
---|
3255 | cases sss_env_hyp * |
---|
3256 | #Hlookup_new_in_old |
---|
3257 | #Hlookup_new_in_new |
---|
3258 | #Hlookup_old |
---|
3259 | cut (mem_assoc_env new sss_new_vars=true) |
---|
3260 | [ 1: cases sss_incl #Hmem #_ elim sss_new_vars in Hmem; |
---|
3261 | [ 1: @False_ind |
---|
3262 | | 2: * #hdv #hdty #tl #Hind whd in ⊢ (% → (??%?)); * |
---|
3263 | [ 1: #Heq destruct (Heq) |
---|
3264 | cases (identifier_eq_i_i … hdv) #Hrefl #Heq >Heq -Heq normalize nodelta |
---|
3265 | @refl |
---|
3266 | | 2: #Hmem lapply (Hind Hmem) #Hmem_in_tl |
---|
3267 | cases (identifier_eq ? new hdv) normalize nodelta |
---|
3268 | [ 1: #_ @refl | 2: #_ @Hmem_in_tl ] ] ] ] |
---|
3269 | #Hnew_in_new_vars |
---|
3270 | lapply (Hlookup_new_in_new new Hnew_in_new_vars) |
---|
3271 | * #res #Hlookup >Hlookup normalize nodelta whd in match (bindIO ??????); |
---|
3272 | (* B. Reduce rhs of assign, i.e. the condition. Do this using simulation hypothesis. *) |
---|
3273 | >(Hsim_expr … Hexec_eq) >bindIO_Value |
---|
3274 | (* C. Execute assign. We must prove that this cannot fail. In order for the proof to proceed, we need |
---|
3275 | to set up things so that loading from that fresh location will yield exactly the stored value. *) |
---|
3276 | normalize in match store_value_of_type'; normalize nodelta |
---|
3277 | whd in match (typeof ?); |
---|
3278 | lapply (sss_new_alloc 〈new,Tint sz sg〉 ? res Hlookup) |
---|
3279 | [ 1: cases sss_incl // ] * * #Hvalid #Hlow #Hhigh |
---|
3280 | lapply (store_int_success … i … Hvalid Hlow Hhigh) * #m_ext' #Hstore |
---|
3281 | lapply (store_value_load_value_ok … Hstore) // #Hload_value_correct |
---|
3282 | >Hstore whd in match (m_bind ?????); whd @conj try // |
---|
3283 | cut (mem block res sss_writeable) |
---|
3284 | [ 1: @cthulhu ] |
---|
3285 | (* lapply (memext_store_value_of_type_writeable … sss_mem_hyp … Hstore) *) |
---|
3286 | @cthulhu |
---|
3287 | | *: @cthulhu ] |
---|
3288 | | *: @cthulhu ] qed. |
---|