Changeset 2227 for src/Clight/switchRemoval.ma
- Timestamp:
- Jul 20, 2012, 8:28:57 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/switchRemoval.ma
r2076 r2227 1 include "Clight/Csyntax.ma".1 include "Clight/Csyntax.ma". 2 2 include "Clight/fresh.ma". 3 3 include "basics/lists/list.ma". … … 5 5 include "Clight/Cexec.ma". 6 6 include "Clight/CexecInd.ma". 7 include "Clight/frontend_misc.ma". 8 (* 9 include "Clight/maps_obsequiv.ma". 10 *) 11 7 12 8 13 (* ----------------------------------------------------------------------------- … … 61 66 (* ----------------------------------------------------------------------------- 62 67 Definitions allowing to state that the program resulting of the transformation 63 is switch-free. The actual proof is done using Russell.64 ---------------------------------------------------------------------------- *)68 is switch-free. 69 ---------------------------------------------------------------------------- *) 65 70 66 71 (* Property of a Clight statement of containing no switch. Could be generalized into a kind of … … 85 90 ]. 86 91 87 definition sf_statement ≝ Σs:statement. switch_free s.88 89 definition stlist ≝ list (label × (𝚺sz.bvint sz) × sf_statement).90 91 92 (* Property of a list of labeled statements of being switch-free *) 92 93 let rec branches_switch_free (sts : labeled_statements) : Prop ≝ 93 94 match sts with 94 [ LSdefault st => 95 [ LSdefault st => 95 96 switch_free st 96 97 | LScase _ _ st tl => … … 98 99 ]. 99 100 100 let rec branch _switch_free_ind101 let rec branches_ind 101 102 (sts : labeled_statements) 102 103 (H : labeled_statements → Prop) … … 107 108 defcase st 108 109 | LScase sz int st tl ⇒ 109 indcase sz int st tl (branch _switch_free_ind tl H defcase indcase)110 indcase sz int st tl (branches_ind tl H defcase indcase) 110 111 ]. 111 112 112 113 113 (* ----------------------------------------------------------------------------- 114 114 Switch-removal code for statements, functions and fundefs. 115 115 ----------------------------------------------------------------------------*) 116 117 (* Given a list of switch cases, prefixes each case by a fresh goto label. It is118 assumed as an hypothesis that each sub-statement is already switch-free119 (argument [H]). The whole function returns a list of labelled switch-free switch120 cases, along the particular label of the default statement and its associated121 statement. A fresh label generator [uv] is threaded through the function. *)122 let rec add_starting_lbl_list123 (l : labeled_statements)124 (H : branches_switch_free l)125 (uv : universe SymbolTag)126 (acc : stlist) : stlist × (label × sf_statement) × (universe SymbolTag) ≝127 match l return λl'. l = l' → stlist × (label × sf_statement) × (universe SymbolTag) with128 [ LSdefault st ⇒ λEq.129 let 〈default_lab, uv'〉 ≝ fresh ? uv in130 〈rev ? acc, 〈default_lab, «st, ?»〉, uv'〉131 | LScase sz tag st other_cases ⇒ λEq.132 let 〈lab, uv'〉 ≝ fresh ? uv in133 let acc' ≝ 〈lab, (mk_DPair ?? sz tag), «st, ?»〉 :: acc in134 add_starting_lbl_list other_cases ? uv' acc'135 ] (refl ? l).136 [ 1: destruct whd in H; //137 | 2: letin H1 ≝ H >Eq in H1;138 #H' normalize in H'; elim H' //139 | 3: >Eq in H; normalize * //140 ] qed.141 116 142 117 (* Converts the directly accessible ("free") breaks to gotos toward the [lab] label. *) … … 170 145 171 146 (* Obsolete. This version generates a nested pseudo-sequence of if-then-elses. *) 147 (* 172 148 let rec produce_cond 173 149 (e : expr) … … 203 179 [ 1: @convert_break_lift elim case_statement // 204 180 | 2: elim sub_statement // ] 205 ] qed. 181 ] qed. *) 206 182 207 183 (* We assume that the expression e is consistely typed w.r.t. the switch branches *) 184 (* 208 185 let rec produce_cond2 209 186 (e : expr) … … 237 214 | 2: // ] 238 215 | 2: elim sub_statement // ] 239 ] qed. 240 241 (* takes an expression, a list of switch-free cases and a freshgen and returns a 242 * switch-free equivalent, along an updated freshgen and a new local variable 243 * (for storing the value of the expr). *) 244 definition simplify_switch : 245 expr → ∀l:labeled_statements. branches_switch_free l → (universe SymbolTag) → sf_statement × (universe SymbolTag) ≝ 246 λe.λswitch_cases.λH.λuv. 216 ] qed. *) 217 218 (* (def_case : ident × sf_statement) *) 219 220 let rec produce_cond 221 (e : expr) 222 (switch_cases : labeled_statements) 223 (u : universe SymbolTag) 224 (exit : label) on switch_cases : statement × label × (universe SymbolTag) ≝ 225 match switch_cases with 226 [ LSdefault st ⇒ 227 let 〈lab,u1〉 ≝ fresh ? u in 228 let st' ≝ convert_break_to_goto st exit in 229 〈Slabel lab st', lab, u1〉 230 | LScase sz tag st other_cases ⇒ 231 let 〈sub_statements, sub_label, u1〉 ≝ produce_cond e other_cases u exit in 232 let st' ≝ convert_break_to_goto st exit in 233 let 〈lab, u2〉 ≝ fresh ? u1 in 234 let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz tag) (typeof e))) (Tint I32 Signed) in 235 let case_statement ≝ 236 Sifthenelse test 237 (Slabel lab (Ssequence st' (Sgoto sub_label))) 238 Sskip 239 in 240 〈Ssequence case_statement sub_statements, lab, u2〉 241 ]. 242 243 definition simplify_switch ≝ 244 λ(e : expr). 245 λ(switch_cases : labeled_statements). 246 λ(uv : universe SymbolTag). 247 247 let 〈exit_label, uv1〉 ≝ fresh ? uv in 248 let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list switch_cases ? uv1 [ ] in 249 let 〈result, useless_label〉 ≝ produce_cond2 e switch_cases defcase exit_label in 250 〈«Ssequence (pi1 … result) (Slabel exit_label Sskip), ?», uv2〉. 251 [ 1: normalize try @conj try @conj try // elim result // 252 | 2: @H ] 253 qed. 254 255 (* recursively convert a statement into a switch-free one. *) 256 let rec switch_removal 257 (st : statement) 258 (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝ 259 match st return λs.s = st → ? with 260 [ Sskip ⇒ λEq. 〈«st,?», [ ], uv〉 261 | Sassign _ _ ⇒ λEq. 〈«st,?», [ ], uv〉 262 | Scall _ _ _ ⇒ λEq. 〈«st,?», [ ], uv〉 263 | Ssequence s1 s2 ⇒ λEq. 264 let 〈s1', vars1, uv'〉 ≝ switch_removal s1 uv in 265 let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in 266 〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉 267 | Sifthenelse e s1 s2 ⇒ λEq. 268 let 〈s1', vars1, uv'〉 ≝ switch_removal s1 uv in 269 let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in 270 〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉 271 | Swhile e body ⇒ λEq. 272 let 〈body', vars', uv'〉 ≝ switch_removal body uv in 273 〈«Swhile e (pi1 … body'),?», vars', uv'〉 274 | Sdowhile e body ⇒ λEq. 275 let 〈body', vars', uv'〉 ≝ switch_removal body uv in 276 〈«Sdowhile e (pi1 … body'),?», vars', uv'〉 277 | Sfor s1 e s2 s3 ⇒ λEq. 278 let 〈s1', vars1, uv'〉 ≝ switch_removal s1 uv in 279 let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in 280 let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 uv'' in 281 〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars1 @ vars2 @ vars3, uv'''〉 282 | Sbreak ⇒ λEq. 283 〈«st,?», [ ], uv〉 284 | Scontinue ⇒ λEq. 285 〈«st,?», [ ], uv〉 286 | Sreturn _ ⇒ λEq. 287 〈«st,?», [ ], uv〉 288 | Sswitch e branches ⇒ λEq. 289 let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches uv in 290 match sf_branches with 291 [ mk_Sig branches' H ⇒ 292 let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in 293 let ident ≝ Expr (Evar switch_tmp) (typeof e) in 294 let assign ≝ Sassign ident e in 295 let 〈result, uv3〉 ≝ simplify_switch ident branches' H uv2 in 296 〈«Ssequence assign (pi1 … result), ?», (〈switch_tmp, typeof e〉 :: vars'), uv3〉 248 let 〈result, useless_label, uv2〉 ≝ produce_cond e switch_cases uv1 exit_label in 249 〈Ssequence result (Slabel exit_label Sskip), uv2〉. 250 251 lemma produce_cond_switch_free : ∀l.∀H:branches_switch_free l.∀e,lab,u.switch_free (\fst (\fst (produce_cond e l u lab))). 252 #l @(labeled_statements_ind … l) 253 [ 1: #s #Hsf #e #lab #u normalize cases (fresh ??) #lab0 #u1 254 normalize in Hsf ⊢ %; @(convert_break_lift … Hsf) 255 | 2: #sz #i #hd #tl #Hind whd in ⊢ (% → ?); * #Hsf_hd #Hsf_tl 256 #e #lab #u normalize 257 lapply (Hind Hsf_tl e lab u) 258 cases (produce_cond e tl u lab) * #cond #lab' #u' #Hsf normalize nodelta 259 cases (fresh ??) #lab0 #u2 normalize nodelta 260 normalize try @conj try @conj try @conj try // 261 @(convert_break_lift … Hsf_hd) 262 ] qed. 263 264 lemma simplify_switch_switch_free : ∀e,l. ∀H:branches_switch_free l. ∀u. switch_free (\fst (simplify_switch e l u)). 265 #e #l cases l 266 [ 1: #def normalize #H #u cases (fresh ? u) #exit_label #uv normalize cases (fresh ? uv) #lab #uv' normalize nodelta 267 whd @conj whd 268 [ 1: @convert_break_lift assumption 269 | 2: @I ] 270 | 2: #sz #i #case #tl normalize * #Hsf #Hsftl #u 271 cases (fresh ? u) #exit_label #uv1 normalize nodelta 272 lapply (produce_cond_switch_free tl Hsftl e exit_label uv1) 273 cases (produce_cond e tl uv1 exit_label) 274 * #cond #lab #u1 #Hsf_cond normalize nodelta 275 cases (fresh ??) #lab0 #u2 normalize nodelta 276 normalize @conj try @conj try @conj try @conj try // 277 @(convert_break_lift ?? Hsf) 278 ] qed. 279 280 (* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in 281 order to circumvent the associativity problems in notations. *) 282 record swret (A : Type[0]) : Type[0] ≝ { 283 ret_st : A; 284 ret_acc : list (ident × type); 285 ret_fvs : list ident; 286 ret_u : universe SymbolTag 287 }. 288 289 notation > "vbox('do' 〈ident v1, ident v2, ident v3, ident v4〉 ← e; break e')" with precedence 48 290 for @{ match ${e} with 291 [ None ⇒ None ? 292 | Some ${fresh ret} ⇒ 293 (λ${ident v1}.λ${ident v2}.λ${ident v3}.λ${ident v4}. ${e'}) 294 (ret_st ? ${fresh ret}) 295 (ret_acc ? ${fresh ret}) 296 (ret_fvs ? ${fresh ret}) 297 (ret_u ? ${fresh ret}) ] }. 298 299 notation > "vbox('ret' 〈e1, e2, e3, e4〉)" with precedence 49 300 for @{ Some ? (mk_swret ? ${e1} ${e2} ${e3} ${e4}) }. 301 302 (* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list 303 of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another 304 'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables 305 allows it to proceed without failing. This is all in order to ease the proof of simulation. *) 306 let rec switch_removal 307 (st : statement) (* the statement in which we will remove switches *) 308 (fvs : list ident) (* a finite list of names usable to create variables. *) 309 (u : universe SymbolTag) (* a fresh /label/ generator *) 310 : option (swret statement) ≝ 311 match st with 312 [ Sskip ⇒ ret 〈st, [ ], fvs, u〉 313 | Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉 314 | Scall _ _ _ ⇒ ret 〈st, [ ], fvs, u〉 315 | Ssequence s1 s2 ⇒ 316 do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u; 317 do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u'; 318 ret 〈Ssequence s1' s2', acc1 @ acc2, fvs'', u''〉 319 | Sifthenelse e s1 s2 ⇒ 320 do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u; 321 do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u'; 322 ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉 323 | Swhile e body ⇒ 324 do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u; 325 ret 〈Swhile e body', acc, fvs', u'〉 326 | Sdowhile e body ⇒ 327 do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u; 328 ret 〈Sdowhile e body', acc, fvs', u'〉 329 | Sfor s1 e s2 s3 ⇒ 330 do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u; 331 do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u'; 332 do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u''; 333 ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉 334 | Sbreak ⇒ 335 ret 〈st, [ ], fvs, u〉 336 | Scontinue ⇒ 337 ret 〈st, [ ], fvs, u〉 338 | Sreturn _ ⇒ 339 ret 〈st, [ ], fvs, u〉 340 | Sswitch e branches ⇒ 341 do 〈sf_branches, acc, fvs', u'〉 ← switch_removal_branches branches fvs u; 342 match fvs' with 343 [ nil ⇒ None ? 344 | cons fresh tl ⇒ 345 (* let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in *) 346 let ident ≝ Expr (Evar fresh) (typeof e) in 347 let assign ≝ Sassign ident e in 348 let 〈result, u''〉 ≝ simplify_switch ident sf_branches u' in 349 ret 〈Ssequence assign result, (〈fresh, typeof e〉 :: acc), tl, u'〉 297 350 ] 298 | Slabel label body ⇒ λEq.299 let 〈body', vars', uv'〉 ≝ switch_removal body uv in300 〈«Slabel label (pi1 … body'), ?», vars', uv'〉301 | Sgoto _ ⇒ λEq.302 〈«st, ?», [ ], uv〉303 | Scost cost body ⇒ λEq.304 let 〈body', vars', uv'〉 ≝ switch_removal body uv in305 〈«Scost cost (pi1 … body'),?», vars', uv'〉306 ] (refl ? st)351 | Slabel label body ⇒ 352 do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u; 353 ret 〈Slabel label body', acc, fvs', u'〉 354 | Sgoto _ ⇒ 355 ret 〈st, [ ], fvs, u〉 356 | Scost cost body ⇒ 357 do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u; 358 ret 〈Scost cost body', acc, fvs', u'〉 359 ] 307 360 308 361 and switch_removal_branches 309 362 (l : labeled_statements) 310 (uv : universe SymbolTag) : (Σl'.branches_switch_free l') × (list (ident × type)) × (universe SymbolTag) ≝ 363 (fvs : list ident) 364 (u : universe SymbolTag) 365 (* : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝ 311 366 match l with 312 367 [ LSdefault st ⇒ 313 let 〈st, vars', uv'〉 ≝ switch_removal st uv in314 〈«LSdefault (pi1 … st), ?», vars', uv'〉368 do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u; 369 ret 〈LSdefault st', acc1, fvs', u'〉 315 370 | LScase sz int st tl => 316 let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl uv in317 let 〈st', vars'', uv''〉 ≝ switch_removal st uv' in318 〈«LScase sz int st' (pi1 … tl_result), ?», vars' @ vars'', uv''〉371 do 〈tl_result, acc1, fvs', u'〉 ← switch_removal_branches tl fvs u; 372 do 〈st', acc2, fvs'', u''〉 ← switch_removal st fvs' u'; 373 ret 〈LScase sz int st' tl_result, acc1 @ acc2, fvs'', u''〉 319 374 ]. 320 try @conj destruct try elim s1' try elim s2' try elim s3' try elim body' whd try // 321 [ 1: #st1 #H1 #st2 #H2 #st3 #H3 @conj // 322 | 2: elim result // 323 | 3: elim st // 324 | 4: elim st' // 325 | 5: elim tl_result // 375 376 let rec mk_fresh_variables 377 (st : statement) (* the statement in which we will remove switches *) 378 (u : universe SymbolTag) (* a fresh /label/ generator *) 379 : (list ident) × (universe SymbolTag) ≝ 380 match st with 381 [ Sskip ⇒ 〈[ ], u〉 382 | Sassign _ _ ⇒ 〈[ ], u〉 383 | Scall _ _ _ ⇒ 〈[ ], u〉 384 | Ssequence s1 s2 ⇒ 385 let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in 386 let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in 387 〈fvs @ fvs', u''〉 388 | Sifthenelse e s1 s2 ⇒ 389 let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in 390 let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in 391 〈fvs @ fvs', u''〉 392 | Swhile e body ⇒ 393 mk_fresh_variables body u 394 | Sdowhile e body ⇒ 395 mk_fresh_variables body u 396 | Sfor s1 e s2 s3 ⇒ 397 let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in 398 let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in 399 let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in 400 〈fvs @ fvs' @fvs'', u'''〉 401 | Sbreak ⇒ 402 〈[ ], u〉 403 | Scontinue ⇒ 404 〈[ ], u〉 405 | Sreturn _ ⇒ 406 〈[ ], u〉 407 | Sswitch e branches ⇒ 408 let 〈ident, u'〉 ≝ fresh ? u in (* This is actually the only point where we need to create a fresh var. *) 409 let 〈fvs, u''〉 ≝ mk_fresh_variables_branches branches u' in 410 〈fvs @ [ident], u''〉 (* reversing the order to match a proof invariant *) 411 | Slabel label body ⇒ 412 mk_fresh_variables body u 413 | Sgoto _ ⇒ 414 〈[ ], u〉 415 | Scost cost body ⇒ 416 mk_fresh_variables body u 417 ] 418 419 and mk_fresh_variables_branches 420 (l : labeled_statements) 421 (u : universe SymbolTag) 422 (* : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝ 423 match l with 424 [ LSdefault st ⇒ 425 mk_fresh_variables st u 426 | LScase sz int st tl => 427 let 〈fvs, u'〉 ≝ mk_fresh_variables_branches tl u in 428 let 〈fvs',u''〉 ≝ mk_fresh_variables st u' in 429 〈fvs @ fvs', u''〉 430 ]. 431 432 (* Copied this from Csyntax.ma, lifted from Prop to Type 433 (I needed to eliminate something proved with this towards Type) *) 434 let rec statement_indT 435 (P:statement → Type[1]) (Q:labeled_statements → Type[1]) 436 (Ssk:P Sskip) 437 (Sas:∀e1,e2. P (Sassign e1 e2)) 438 (Sca:∀eo,e,args. P (Scall eo e args)) 439 (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2)) 440 (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2)) 441 (Swh:∀e,s. P s → P (Swhile e s)) 442 (Sdo:∀e,s. P s → P (Sdowhile e s)) 443 (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3)) 444 (Sbr:P Sbreak) 445 (Sco:P Scontinue) 446 (Sre:∀eo. P (Sreturn eo)) 447 (Ssw:∀e,ls. Q ls → P (Sswitch e ls)) 448 (Sla:∀l,s. P s → P (Slabel l s)) 449 (Sgo:∀l. P (Sgoto l)) 450 (Scs:∀l,s. P s → P (Scost l s)) 451 (LSd:∀s. P s → Q (LSdefault s)) 452 (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t)) 453 (s:statement) on s : P s ≝ 454 match s with 455 [ Sskip ⇒ Ssk 456 | Sassign e1 e2 ⇒ Sas e1 e2 457 | Scall eo e args ⇒ Sca eo e args 458 | Ssequence s1 s2 ⇒ Ssq s1 s2 459 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) 460 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) 461 | Sifthenelse e s1 s2 ⇒ Sif e s1 s2 462 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) 463 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) 464 | Swhile e s ⇒ Swh e s 465 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 466 | Sdowhile e s ⇒ Sdo e s 467 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 468 | Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3 469 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) 470 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) 471 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3) 472 | Sbreak ⇒ Sbr 473 | Scontinue ⇒ Sco 474 | Sreturn eo ⇒ Sre eo 475 | Sswitch e ls ⇒ Ssw e ls 476 (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls) 477 | Slabel l s ⇒ Sla l s 478 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 479 | Sgoto l ⇒ Sgo l 480 | Scost l s ⇒ Scs l s 481 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 482 ] 483 and labeled_statements_indT 484 (P:statement → Type[1]) (Q:labeled_statements → Type[1]) 485 (Ssk:P Sskip) 486 (Sas:∀e1,e2. P (Sassign e1 e2)) 487 (Sca:∀eo,e,args. P (Scall eo e args)) 488 (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2)) 489 (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2)) 490 (Swh:∀e,s. P s → P (Swhile e s)) 491 (Sdo:∀e,s. P s → P (Sdowhile e s)) 492 (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3)) 493 (Sbr:P Sbreak) 494 (Sco:P Scontinue) 495 (Sre:∀eo. P (Sreturn eo)) 496 (Ssw:∀e,ls. Q ls → P (Sswitch e ls)) 497 (Sla:∀l,s. P s → P (Slabel l s)) 498 (Sgo:∀l. P (Sgoto l)) 499 (Scs:∀l,s. P s → P (Scost l s)) 500 (LSd:∀s. P s → Q (LSdefault s)) 501 (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t)) 502 (ls:labeled_statements) on ls : Q ls ≝ 503 match ls with 504 [ LSdefault s ⇒ LSd s 505 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 506 | LScase sz i s t ⇒ LSc sz i s t 507 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 508 (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t) 509 ]. 510 511 lemma switch_removal_ok : 512 ∀st, u0, u1, post. 513 Σresult. 514 (switch_removal st ((\fst (mk_fresh_variables st u0)) @ post) u1 = Some ? result) ∧ (ret_fvs ? result = post). 515 #st 516 @(statement_indT ? (λls. ∀u0, u1, post. 517 Σresult. 518 (switch_removal_branches ls ((\fst (mk_fresh_variables_branches ls u0)) @ post) u1 = Some ? result) 519 ∧ (ret_fvs ? result = post) 520 ) … st) 521 [ 1: #u0 #u1 #post normalize 522 %{(mk_swret statement Sskip [] post u1)} % // 523 | 2: #e1 #e2 #u0 #u1 #post normalize 524 %{((mk_swret statement (Sassign e1 e2) [] post u1))} % try // 525 | 3: #e0 #e #args #u0 #u1 #post normalize 526 %{(mk_swret statement (Scall e0 e args) [] post u1)} % try // 527 | 4: #s1 #s2 #H1 #H2 #u0 #u1 #post normalize 528 elim (H1 u0 u1 ((\fst (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' * 529 cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta 530 elim (H2 u' (ret_u ? s1') post) #s2' * 531 cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta 532 #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize 533 %{(mk_swret statement (Ssequence (ret_st statement s1') (ret_st statement s2')) 534 (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2') 535 (ret_u statement s2'))} % try // 536 | 5: #e #s1 #s2 #H1 #H2 #u0 #u1 #post normalize 537 elim (H1 u0 u1 ((\fst (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' * 538 cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta 539 elim (H2 u' (ret_u ? s1') post) #s2' * 540 cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta 541 #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize 542 %{((mk_swret statement 543 (Sifthenelse e (ret_st statement s1') (ret_st statement s2')) 544 (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2') 545 (ret_u statement s2')))} % try // 546 | 6: #e #s #H #u0 #u1 #post normalize 547 elim (H u0 u1 post) #s1' * normalize 548 cases (mk_fresh_variables s u0) #fvs #u' 549 #Heq1 #Heq1_fvs >Heq1 normalize nodelta 550 %{(mk_swret statement (Swhile e (ret_st statement s1')) (ret_acc statement s1') 551 (ret_fvs statement s1') (ret_u statement s1'))} % try // 552 | 7: #e #s #H #u0 #u1 #post normalize 553 elim (H u0 u1 post) #s1' * normalize 554 cases (mk_fresh_variables s u0) #fvs #u' 555 #Heq1 #Heq1_fvs >Heq1 normalize nodelta 556 %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1') 557 (ret_fvs statement s1') (ret_u statement s1'))} % try // 558 | 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize 559 elim (H1 u0 u1 560 (\fst (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0))) @ 561 (\fst (mk_fresh_variables s3 (\snd (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @ 562 post)) #s1' * 563 cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta 564 elim (H2 u' (ret_u ? s1') ((\fst (mk_fresh_variables s3 (\snd (mk_fresh_variables s2 u')))) @ 565 post)) #s2' * 566 cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta 567 elim (H3 u'' (ret_u ? s2') post) #s3' * 568 cases (mk_fresh_variables s3 u'') #fvs'' #u''' normalize nodelta 569 #Heq3 #Heq3_fvs #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs 570 >associative_append >associative_append >Heq1 normalize >Heq1_fvs 571 >Heq2 normalize >Heq2_fvs >Heq3 normalize 572 %{(mk_swret statement 573 (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3')) 574 (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3') 575 (ret_fvs statement s3') (ret_u statement s3'))} % try // 576 | 9: #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % // 577 | 10: #u0 #u1 #post normalize %{(mk_swret statement Scontinue [] post u1)} % // 578 | 11: #e #u0 #u1 #post normalize %{(mk_swret statement (Sreturn e) [] post u1)} % // 579 | 12: #e #ls #H #u0 #u1 #post 580 whd in match (mk_fresh_variables ??); 581 whd in match (switch_removal ???); 582 elim (fresh ? u0) #fresh #u' 583 elim (H u' u1 ([fresh] @ post)) #ls' * normalize nodelta 584 cases (mk_fresh_variables_branches ls u') #fvs #u'' normalize nodelta 585 >associative_append #Heq #Heq_fvs >Heq normalize nodelta 586 >Heq_fvs normalize nodelta 587 cases (simplify_switch ???) #st' #u''' normalize nodelta 588 %{((mk_swret statement 589 (Ssequence (Sassign (Expr (Evar fresh) (typeof e)) e) st') 590 (〈fresh,typeof e〉::ret_acc labeled_statements ls') ([]@post) 591 (ret_u labeled_statements ls')))} % // 592 | 13: #l #s #H #u0 #u1 #post normalize 593 elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs 594 %{(mk_swret statement (Slabel l (ret_st statement s')) (ret_acc statement s') 595 post (ret_u statement s'))} % // 596 | 14: #l #u0 #u1 #post normalize %{((mk_swret statement (Sgoto l) [] post u1))} % // 597 | 15: #l #s #H #u0 #u1 #post normalize 598 elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs 599 %{(mk_swret statement (Scost l (ret_st statement s')) (ret_acc statement s') 600 post (ret_u statement s'))} % // 601 | 16: #s #H #u0 #u1 #post normalize 602 elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs 603 %{(mk_swret labeled_statements (LSdefault (ret_st statement s')) 604 (ret_acc statement s') post (ret_u statement s'))} % // 605 | 17: #sz #i #hd #tl #H1 #H2 #u0 #u1 #post normalize 606 elim (H2 u0 u1 (\fst (mk_fresh_variables hd (\snd (mk_fresh_variables_branches tl u0))) @ post)) #ls' * 607 cases (mk_fresh_variables_branches tl u0) #fvs #u' normalize 608 elim (H1 u' (ret_u labeled_statements ls') post) #s1' * 609 cases (mk_fresh_variables hd u') #fvs' #u' normalize #Heq #Heq_fvs #Heql #Heql_fvs 610 >associative_append >Heql normalize >Heql_fvs >Heq normalize 611 %{(mk_swret labeled_statements 612 (LScase sz i (ret_st statement s1') (ret_st labeled_statements ls')) 613 (ret_acc labeled_statements ls'@ret_acc statement s1') 614 (ret_fvs statement s1') (ret_u statement s1'))} % // 326 615 ] qed. 327 616 328 definition function_switch_removal : function → universe SymbolTag → function × (universe SymbolTag) ≝ 329 λf,u. 330 let 〈body, new_vars, u'〉 ≝ switch_removal (fn_body f) u in 331 let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (pi1 … body) in 332 〈f, u'〉. 333 334 let rec fundef_switch_removal (f : clight_fundef) (u : universe SymbolTag) : clight_fundef × (universe SymbolTag) ≝ 335 match f with 336 [ CL_Internal f ⇒ 337 let 〈f',u'〉 ≝ function_switch_removal f u in 338 〈CL_Internal f', u'〉 339 | CL_External _ _ _ ⇒ 340 〈f, u〉 341 ]. 342 617 axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *) 618 619 (* Proof that switch_removal_switch_free does its job. *) 620 lemma switch_removal_switch_free : ∀st,fvs,u,result. switch_removal st fvs u = Some ? result → switch_free (ret_st ? result). 621 #st @(statement_ind2 ? (λls. ∀fvs,u,ls_result. switch_removal_branches ls fvs u = Some ? ls_result → 622 branches_switch_free (ret_st ? ls_result)) … st) 623 [ 1: #fvs #u #result normalize #Heq destruct (Heq) // 624 | 2: #e1 #e2 #fvs #u #result normalize #Heq destruct (Heq) // 625 | 3: #e0 #e #args #fvs #u #result normalize #Heq destruct (Heq) // 626 | 4: #s1 #s2 #H1 #H2 #fvs #u #result normalize lapply (H1 fvs u) 627 elim (switch_removal s1 fvs u) normalize 628 [ 1: #_ #Habsurd destruct (Habsurd) 629 | 2: #res1 #Heq1 lapply (H2 (ret_fvs statement res1) (ret_u statement res1)) 630 elim (switch_removal s2 (ret_fvs statement res1) (ret_u statement res1)) 631 [ 1: normalize #_ #Habsurd destruct (Habsurd) 632 | 2: normalize #res2 #Heq2 #Heq destruct (Heq) 633 normalize @conj 634 [ 1: @Heq1 // | 2: @Heq2 // ] 635 ] ] 636 | *: 637 (* TODO the first few cases show that the lemma is routinely proved. TBF later. *) 638 @cthulhu ] 639 qed. 343 640 344 641 (* ----------------------------------------------------------------------------- … … 356 653 *) 357 654 655 (* Least element in the total order of identifiers. *) 656 definition least_identifier ≝ an_identifier SymbolTag one. 657 358 658 (* This is certainly overkill: variables adressed in an expression should be declared in the 359 * enclosing function's prototype. *) 360 let rec max_of_expr (e : expr) (current : ident): ident ≝659 * enclosing function's prototype. *) 660 let rec max_of_expr (e : expr) : ident ≝ 361 661 match e with 362 662 [ Expr ed _ ⇒ 363 663 match ed with 364 [ Econst_int _ _ ⇒ current365 | Econst_float _ ⇒ current366 | Evar id ⇒ max_id id current367 | Ederef e1 ⇒ max_of_expr e1 current368 | Eaddrof e1 ⇒ max_of_expr e1 current369 | Eunop _ e1 ⇒ max_of_expr e1 current370 | Ebinop _ e1 e2 ⇒ max_ of_expr e1 (max_of_expr e2 current)371 | Ecast _ e1 ⇒ max_of_expr e1 current372 | Econdition e1 e2 e3 ⇒ 373 max_ of_expr e1 (max_of_expr e2 (max_of_expr e3 current))664 [ Econst_int _ _ ⇒ least_identifier 665 | Econst_float _ ⇒ least_identifier 666 | Evar id ⇒ id 667 | Ederef e1 ⇒ max_of_expr e1 668 | Eaddrof e1 ⇒ max_of_expr e1 669 | Eunop _ e1 ⇒ max_of_expr e1 670 | Ebinop _ e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) 671 | Ecast _ e1 ⇒ max_of_expr e1 672 | Econdition e1 e2 e3 ⇒ 673 max_id (max_of_expr e1) (max_id (max_of_expr e2) (max_of_expr e3)) 374 674 | Eandbool e1 e2 ⇒ 375 max_ of_expr e1 (max_of_expr e2 current)675 max_id (max_of_expr e1) (max_of_expr e2) 376 676 | Eorbool e1 e2 ⇒ 377 max_ of_expr e1 (max_of_expr e2 current)378 | Esizeof _ ⇒ current379 | Efield r f ⇒ max_id f (max_of_expr r current)380 | Ecost _ e1 ⇒ max_of_expr e1 current677 max_id (max_of_expr e1) (max_of_expr e2) 678 | Esizeof _ ⇒ least_identifier 679 | Efield r f ⇒ max_id f (max_of_expr r) 680 | Ecost _ e1 ⇒ max_of_expr e1 381 681 ] 382 682 ]. 383 683 384 (* Re easoning about this promises to be a serious pain. Especially the Scall case. *)385 let rec max_of_statement (s : statement) (current : ident): ident ≝684 (* Reasoning about this promises to be a serious pain. Especially the Scall case. *) 685 let rec max_of_statement (s : statement) : ident ≝ 386 686 match s with 387 [ Sskip ⇒ current388 | Sassign e1 e2 ⇒ max_ of_expr e2 (max_of_expr e1 current)389 | Scall r etf args ⇒687 [ Sskip ⇒ least_identifier 688 | Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) 689 | Scall r f args ⇒ 390 690 let retmax ≝ 391 match r etwith392 [ None ⇒ current393 | Some e ⇒ max_of_expr e current]691 match r with 692 [ None ⇒ least_identifier 693 | Some e ⇒ max_of_expr e ] 394 694 in 395 foldl ?? (λacc,elt. max_of_expr elt acc) (max_of_expr f retmax) args 396 | Ssequence s1 s2 ⇒ 397 max_of_statement s1 (max_of_statement s2 current) 695 max_id (max_of_expr f) 696 (max_id retmax 697 (foldl ?? (λacc,elt. max_id (max_of_expr elt) acc) least_identifier args) ) 698 | Ssequence s1 s2 ⇒ 699 max_id (max_of_statement s1) (max_of_statement s2) 398 700 | Sifthenelse e s1 s2 ⇒ 399 max_ of_expr e (max_of_statement s1 (max_of_statement s2 current))701 max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2)) 400 702 | Swhile e body ⇒ 401 max_ of_expr e (max_of_statement body current)703 max_id (max_of_expr e) (max_of_statement body) 402 704 | Sdowhile e body ⇒ 403 max_ of_expr e (max_of_statement body current)705 max_id (max_of_expr e) (max_of_statement body) 404 706 | Sfor init test incr body ⇒ 405 max_ of_statement init (max_of_expr test (max_of_statement incr (max_of_statement body current)))406 | Sbreak ⇒ current407 | Scontinue ⇒ current707 max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body)) 708 | Sbreak ⇒ least_identifier 709 | Scontinue ⇒ least_identifier 408 710 | Sreturn opt ⇒ 409 711 match opt with 410 [ None ⇒ current411 | Some e ⇒ max_of_expr e current712 [ None ⇒ least_identifier 713 | Some e ⇒ max_of_expr e 412 714 ] 413 715 | Sswitch e ls ⇒ 414 max_ of_expr e (max_of_ls ls current)716 max_id (max_of_expr e) (max_of_ls ls) 415 717 | Slabel lab body ⇒ 416 max_id lab (max_of_statement body current)718 max_id lab (max_of_statement body) 417 719 | Sgoto lab ⇒ 418 max_id lab current720 lab 419 721 | Scost _ body ⇒ 420 max_of_statement body current722 max_of_statement body 421 723 ] 422 and max_of_ls (ls : labeled_statements) (current : ident): ident ≝724 and max_of_ls (ls : labeled_statements) : ident ≝ 423 725 match ls with 424 [ LSdefault s ⇒ max_of_statement s current425 | LScase _ _ s ls' ⇒ max_ of_ls ls' (max_of_statement s current)726 [ LSdefault s ⇒ max_of_statement s 727 | LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s) 426 728 ]. 427 729 428 730 definition max_id_of_function : function → ident ≝ 429 λf. max_of_statement (fn_body f) (max_id_of_fn f). 430 431 definition max_id_of_fundef_deep : clight_fundef → ident ≝ 432 λf. match f with 433 [ CL_Internal f ⇒ max_id_of_function f 434 | CL_External id _ _ ⇒ id 435 ]. 436 437 let rec max_id_of_functs_deep (funcs : list (ident × clight_fundef)) (current : ident) : ident ≝ 438 let func_max ≝ 439 foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef_deep (\snd idf))) id) (an_identifier ? one) funcs 440 in max_id func_max current. 441 442 definition max_id_of_program_deep : clight_program → ident ≝ 443 λp. 444 max_id 445 (max_id_of_functs_deep (prog_funct ?? p) (prog_main ?? p)) 446 (max_id_of_globvars (prog_vars ?? p)). 447 448 (* The previous functions compute an (over?)-approximation of the identifiers and labels. 449 The following function builds a "good" universe for a complete clight program. *) 450 definition universe_for_program_deep : clight_program → universe SymbolTag ≝ 451 λp. universe_of_max (max_id_of_program_deep p). 452 731 λf. max_id (max_of_statement (fn_body f)) (max_id_of_fn f). 732 733 (* We compute fresh universes on a function-by function basis, since there can't 734 * be cross-functions gotos or stuff like that. *) 735 definition function_switch_removal : function → function × (list (ident × type)) ≝ 736 λf. 737 (λres_record. 738 let new_vars ≝ ret_acc ? res_record in 739 let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (ret_st ? res_record) in 740 〈result, new_vars〉) 741 (let u ≝ universe_of_max (max_id_of_function f) in 742 let 〈fvs,u'〉 as Hfv ≝ mk_fresh_variables (fn_body f) u in 743 match switch_removal (fn_body f) fvs u' return λx. (switch_removal (fn_body f) fvs u' = x) → ? with 744 [ None ⇒ λHsr. ? 745 | Some res_record ⇒ λ_. res_record 746 ] (refl ? (switch_removal (fn_body f) fvs u'))). 747 lapply (switch_removal_ok (fn_body f) u u' [ ]) * #result' * #Heq #Hret_eq 748 <Hfv in Heq; >append_nil >Hsr #Habsurd destruct (Habsurd) 749 qed. 750 751 let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝ 752 match f with 753 [ CL_Internal f ⇒ 754 CL_Internal (\fst (function_switch_removal f)) 755 | CL_External _ _ _ ⇒ 756 f 757 ]. 453 758 454 759 let rec program_switch_removal (p : clight_program) : clight_program ≝ 455 let uv ≝ universe_for_program_deep p in456 760 let prog_funcs ≝ prog_funct ?? p in 457 let 〈sf_funcs, final_uv〉 ≝ 458 foldr ?? (λcl_fundef.λacc. 459 let 〈fundefs, uv1〉 ≝ acc in 460 let 〈fun_id, fun_def〉 ≝ cl_fundef in 461 let 〈new_fun_def,uv2〉 ≝ fundef_switch_removal fun_def uv1 in 462 〈〈fun_id, new_fun_def〉 :: fundefs, uv2〉 463 ) 〈[ ], uv〉 prog_funcs 464 in 761 let sf_funcs ≝ map ?? (λcl_fundef. 762 let 〈fun_id, fun_def〉 ≝ cl_fundef in 763 〈fun_id, fundef_switch_removal fun_def〉 764 ) prog_funcs in 465 765 mk_program ?? 466 766 (prog_vars … p) … … 468 768 (prog_main … p). 469 769 770 771 (* ----------------------------------------------------------------------------- 772 Applying two relations on all substatements and all subexprs (directly under). 773 ---------------------------------------------------------------------------- *) 774 775 let rec substatement_P (s1 : statement) (P : statement → Prop) (Q : expr → Prop) : Prop ≝ 776 match s1 with 777 [ Sskip ⇒ True 778 | Sassign e1 e2 ⇒ Q e1 ∧ Q e2 779 | Scall r f args ⇒ 780 match r with 781 [ None ⇒ Q f ∧ (All … Q args) 782 | Some r ⇒ Q r ∧ Q f ∧ (All … Q args) 783 ] 784 | Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2 785 | Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2 786 | Swhile e sub ⇒ Q e ∧ P sub 787 | Sdowhile e sub ⇒ Q e ∧ P sub 788 | Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3 789 | Sbreak ⇒ True 790 | Scontinue ⇒ True 791 | Sreturn r ⇒ 792 match r with 793 [ None ⇒ True 794 | Some r ⇒ Q r ] 795 | Sswitch e ls ⇒ Q e ∧ (substatement_ls ls P) 796 | Slabel _ sub ⇒ P sub 797 | Sgoto _ ⇒ True 798 | Scost _ sub ⇒ P sub 799 ] 800 and substatement_ls ls (P : statement → Prop) : Prop ≝ 801 match ls with 802 [ LSdefault sub ⇒ P sub 803 | LScase _ _ sub tl ⇒ P sub ∧ (substatement_ls tl P) 804 ]. 805 806 (* ----------------------------------------------------------------------------- 807 Freshness conservation results on switch removal. 808 ---------------------------------------------------------------------------- *) 809 810 (* Similar stuff in toCminor.ma. *) 811 lemma fresh_for_univ_still_fresh : 812 ∀u,i. fresh_for_univ SymbolTag i u → ∀v,u'. 〈v, u'〉 = fresh ? u → fresh_for_univ ? i u'. 813 * #p * #i #H1 #v * #p' lapply H1 normalize 814 #H1 #H2 destruct (H2) /2/ qed. 815 816 lemma fresh_eq : ∀u,i. fresh_for_univ SymbolTag i u → ∃fv,u'. fresh ? u = 〈fv, u'〉 ∧ fresh_for_univ ? i u'. 817 #u #i #Hfresh lapply (fresh_for_univ_still_fresh … Hfresh) 818 cases (fresh SymbolTag u) 819 #fv #u' #H %{fv} %{u'} @conj try // @H // 820 qed. 821 822 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)). 823 #e #exit #ls @(branches_ind … ls) 824 [ 1: #st #u #i #Hfresh normalize 825 lapply (fresh_for_univ_still_fresh … Hfresh) 826 cases (fresh ? u) #lab #u1 #H lapply (H lab u1 (refl ??)) normalize // 827 | 2: #sz #i #hd #tl #Hind #u #i' #Hfresh normalize 828 lapply (Hind u i' Hfresh) elim (produce_cond e tl u exit) * 829 #subcond #sublabel #u1 #Hfresh1 normalize 830 lapply (fresh_for_univ_still_fresh … Hfresh1) 831 cases (fresh ? u1) #lab #u2 #H2 lapply (H2 lab u2 (refl ??)) normalize // 832 ] qed. 833 834 lemma simplify_switch_fresh : ∀u,i,e,ls. 835 fresh_for_univ ? i u → 836 fresh_for_univ ? i (\snd (simplify_switch e ls u)). 837 #u #i #e #ls #Hfresh 838 normalize 839 lapply (fresh_for_univ_still_fresh … Hfresh) 840 cases (fresh ? u) 841 #exit_label #uv1 #Haux lapply (Haux exit_label uv1 (refl ??)) -Haux #Haux 842 normalize lapply (produce_cond_fresh e exit_label ls … Haux) 843 elim (produce_cond ????) * #stm #label #uv2 normalize nodelta // 844 qed. 845 846 (* 847 lemma switch_removal_fresh : ∀i,s,u. 848 fresh_for_univ ? i u → 849 fresh_for_univ ? i (\snd (switch_removal s u)). 850 #i #s @(statement_ind2 ? (λls. ∀u. fresh_for_univ ? i u → 851 fresh_for_univ ? i (\snd (switch_removal_branches ls u))) … s) 852 try // 853 [ 1: #s1' #s2' #Hind1 #Hind2 #u #Hyp 854 whd in match (switch_removal (Ssequence s1' s2') u); 855 lapply (Hind1 u Hyp) elim (switch_removal s1' u) 856 * #irr1 #irr2 #uA #HuA normalize nodelta 857 lapply (Hind2 uA HuA) elim (switch_removal s2' uA) 858 * #irr3 #irr4 #uB #HuB normalize nodelta // 859 | 2: #e #s1' #s2' #Hind1 #Hind2 #u #Hyp 860 whd in match (switch_removal (Sifthenelse e s1' s2') u); 861 lapply (Hind1 u Hyp) elim (switch_removal s1' u) 862 * #irr1 #irr2 #uA #HuA normalize nodelta 863 lapply (Hind2 uA HuA) elim (switch_removal s2' uA) 864 * #irr3 #irr4 #uB #HuB normalize nodelta // 865 | 3,4: #e #s' #Hind #u #Hyp 866 whd in match (switch_removal ? u); 867 lapply (Hind u Hyp) elim (switch_removal s' u) 868 * #irr1 #irr2 #uA #HuA normalize nodelta // 869 | 5: #s1' #e #s2' #s3' #Hind1 #Hind2 #Hind3 #u #Hyp 870 whd in match (switch_removal (Sfor s1' e s2' s3') u); 871 lapply (Hind1 u Hyp) elim (switch_removal s1' u) 872 * #irr1 #irr2 #uA #HuA normalize nodelta 873 lapply (Hind2 uA HuA) elim (switch_removal s2' uA) 874 * #irr3 #irr4 #uB #HuB normalize nodelta 875 lapply (Hind3 uB HuB) elim (switch_removal s3' uB) 876 * #irr5 #irr6 #uC #HuC normalize nodelta // 877 | 6: #e #ls #Hind #u #Hyp 878 whd in match (switch_removal (Sswitch e ls) u); 879 lapply (Hind u Hyp) 880 cases (switch_removal_branches ls u) 881 * #irr1 #irr2 #uA #HuA normalize nodelta 882 lapply (fresh_for_univ_still_fresh … HuA) 883 cases (fresh SymbolTag uA) #v #uA' #Haux lapply (Haux v uA' (refl ? 〈v,uA'〉)) 884 -Haux #HuA' normalize nodelta 885 lapply (simplify_switch_fresh uA' i (Expr (Evar v) (typeof e)) irr1 HuA') 886 cases (simplify_switch ???) #stm #uB 887 #Haux normalize nodelta // 888 | 7,8: #label #body #Hind #u #Hyp 889 whd in match (switch_removal ? u); 890 lapply (Hind u Hyp) elim (switch_removal body u) 891 * #irr1 #irr2 #uA #HuA normalize nodelta // 892 | 9: #defcase #Hind #u #Hyp whd in match (switch_removal_branches ??); 893 lapply (Hind u Hyp) elim (switch_removal defcase u) 894 * #irr1 #irr2 #uA #HuA normalize nodelta // 895 | 10: #sz #i0 #s0 #tl #Hind1 #Hind2 #u #Hyp normalize 896 lapply (Hind2 u Hyp) elim (switch_removal_branches tl u) 897 * #irr1 #irr2 #uA #HuA normalize nodelta 898 lapply (Hind1 uA HuA) elim (switch_removal s0 uA) 899 * #irr3 #irr4 #uB #HuB // 900 ] qed. 901 902 lemma switch_removal_branches_fresh : ∀i,ls,u. 903 fresh_for_univ ? i u → 904 fresh_for_univ ? i (\snd (switch_removal_branches ls u)). 905 #i #ls @(labeled_statements_ind2 (λs. ∀u. fresh_for_univ ? i u → 906 fresh_for_univ ? i (\snd (switch_removal s u))) ? … ls) 907 try /2 by switch_removal_fresh/ 908 [ 1: #s #Hind #u #Hfresh normalize lapply (switch_removal_fresh ? s ? Hfresh) 909 cases (switch_removal s u) * // 910 | 2: #sz #i #s #tl #Hs #Htl #u #Hfresh normalize 911 lapply (Htl u Hfresh) 912 cases (switch_removal_branches tl u) * normalize nodelta 913 #ls' #fvs #u' #Hfresh' 914 lapply (Hs u' Hfresh') 915 cases (switch_removal s u') * // 916 ] qed. 917 *) 470 918 (* ----------------------------------------------------------------------------- 471 919 Simulation proof and related voodoo. 472 920 ----------------------------------------------------------------------------*) 473 474 (* Copied from SimplifyCasts.ma. Might be good to create a new file for shared stuff. *)475 inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝476 | SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2477 | SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2.478 921 479 922 definition expr_lvalue_ind_combined ≝ … … 539 982 ]. 540 983 984 541 985 (* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched 542 986 by a non-constant number of evaluations in the converted program. More precisely, … … 544 988 necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *) 545 989 546 (* A version of simplify_switch hiding the ugly proj *) 547 definition sw_rem : statement → (universe SymbolTag) → statement ≝ 548 λs,u. 549 \fst (\fst (switch_removal s u)). 550 990 (* A version of simplify_switch hiding the ugly projs *) 551 991 definition fresh_for_expression ≝ 552 λe,u. fresh_for_univ SymbolTag (max_of_expr e (an_identifier ? one)) u.553 992 λe,u. fresh_for_univ SymbolTag (max_of_expr e) u. 993 554 994 definition fresh_for_statement ≝ 555 λs,u. fresh_for_univ SymbolTag (max_of_statement s (an_identifier ? one)) u. 556 995 λs,u. fresh_for_univ SymbolTag (max_of_statement s) u. 996 997 (* needed during mutual induction ... *) 998 definition fresh_for_labeled_statements ≝ 999 λls,u. fresh_for_univ ? (max_of_ls ls) u. 1000 557 1001 definition fresh_for_function ≝ 558 1002 λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u. 559 1003 560 let rec fresh_for_continuation (k : cont) (u : universe SymbolTag) : Prop ≝ 561 match k with 562 [ Kstop ⇒ True 563 | Kseq s k0 ⇒ (fresh_for_statement s u) ∧ (fresh_for_continuation k0 u) 564 | Kwhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u) 565 | Kdowhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u) 566 | Kfor2 e s1 s2 k0 ⇒ 567 (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧ 568 (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u) 569 | Kfor3 e s1 s2 k0 ⇒ 570 (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧ 571 (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u) 572 | Kswitch k0 ⇒ fresh_for_continuation k0 u 573 | Kcall _ f e k ⇒ (fresh_for_function f u) ∧ (fresh_for_continuation k u) 574 ]. 575 576 inductive switch_cont_sim : cont → cont → Prop ≝ 577 | swc_stop : 578 switch_cont_sim Kstop Kstop 579 | swc_seq : ∀s,k,k',u. 580 fresh_for_statement s u → 581 switch_cont_sim k k' → 582 switch_cont_sim (Kseq s k) (Kseq (sw_rem s u) k') 583 | swc_while : ∀e,s,k,k',u. 584 fresh_for_expression e u → 585 fresh_for_statement s u → 586 switch_cont_sim k k' → 587 switch_cont_sim (Kwhile e s k) (Kwhile e (sw_rem s u) k') 588 | swc_dowhile : ∀e,s,k,k',u. 589 fresh_for_expression e u → 590 fresh_for_statement s u → 591 switch_cont_sim k k' → 592 switch_cont_sim (Kdowhile e s k) (Kdowhile e (sw_rem s u) k') 593 | swc_for1 : ∀e,s1,s2,k,k',u1,u2. 594 fresh_for_statement s1 u1 → 595 fresh_for_statement s2 u2 → 596 switch_cont_sim k k' → 597 switch_cont_sim (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip e (sw_rem s1 u1) (sw_rem s2 u2)) k') 598 | swc_for2 : ∀e,s1,s2,k,k',u1,u2. 599 fresh_for_statement s1 u1 → 600 fresh_for_statement s2 u2 → 601 switch_cont_sim k k' → 602 switch_cont_sim (Kfor2 e s1 s2 k) (Kfor2 e (sw_rem s1 u1) (sw_rem s2 u2) k') 603 | swc_for3 : ∀e,s1,s2,k,k',u1,u2. 604 fresh_for_statement s1 u1 → 605 fresh_for_statement s2 u2 → 606 switch_cont_sim k k' → 607 switch_cont_sim (Kfor3 e s1 s2 k) (Kfor3 e (sw_rem s1 u1) (sw_rem s2 u2) k') 608 | swc_switch : ∀k,k'. 609 switch_cont_sim k k' → 610 switch_cont_sim (Kswitch k) (Kswitch k') 611 | swc_call : ∀r,f,en,k,k',u. 612 fresh_for_function f u → 613 switch_cont_sim k k' → 614 switch_cont_sim (Kcall r f en k) (Kcall r (\fst (function_switch_removal f u)) en k'). 615 616 617 inductive switch_state_sim : state → state → Prop ≝ 618 | sws_state : ∀uf,us,uk,f,s,k,k',e,m. 619 fresh_for_function f uf → 620 fresh_for_statement s us → 621 fresh_for_continuation k' uk → 622 switch_cont_sim k k' → 623 switch_state_sim (State f s k e m) (State (\fst (function_switch_removal f uf)) (sw_rem s us) k' e m) 624 (* Extra matching states that we can reach that don't quite correspond to the 625 labelling function *) 626 (* 627 | sws_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' → 628 switch_state_sim (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 629 | sws_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' → 630 switch_state_sim (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 631 | sws_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' → 632 switch_state_sim (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 633 *) 634 (* and the rest *) 635 | sws_callstate : ∀ufd,fd,args,k,k',m. 636 switch_cont_sim k k' → 637 switch_state_sim (Callstate fd args k m) (Callstate (\fst (fundef_switch_removal fd ufd)) args k' m) 638 | sws_returnstate : ∀res,k,k',m. 639 switch_cont_sim k k' → 640 switch_state_sim (Returnstate res k m) (Returnstate res k' m) 641 | sws_finalstate : ∀r. 642 switch_state_sim (Finalstate r) (Finalstate r) 643 . 644 645 inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝ 646 | eventually_base : ∀s,t,s'. 647 exec_step ge s = Value io_out io_in ? 〈t, s'〉 → 648 P s' → 649 eventually ge P s t 650 | eventually_step : ∀s,t,s',t'. 651 exec_step ge s = Value io_out io_in ? 〈t, s'〉 → 652 eventually ge P s' t' → 653 eventually ge P s (t ⧺ t'). 654 655 (* [eventually] is not so nice to use directly, we would like to make the mandatory 656 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not 657 to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *) 658 lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 659 eventually ge P s t. 660 #ge #P #s #t * #s' * #Hexec #HP %1{? Hexec HP} 661 qed. 662 663 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { 664 rg_find_symbol: ∀s. 665 find_symbol ? ge s = find_symbol ? ge' s; 666 rg_find_funct: ∀v,f. 667 find_funct ? ge v = Some ? f → 668 find_funct ? ge' v = Some ? (t f); 669 rg_find_funct_ptr: ∀b,f. 670 find_funct_ptr ? ge b = Some ? f → 671 find_funct_ptr ? ge' b = Some ? (t f) 672 }. 673 674 (* TODO ... fundef_switch_removal wants a universe which is fresh-for-its argument. *) 675 (* 676 lemma sim_related_globals : ∀ge,ge',en,m,u. related_globals ? fundef_switch_removal ge ge' → 677 (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧ 678 (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)). 679 *) 680 681 (* The return type of any function is invariant under switch removal *) 682 lemma fn_return_simplify : ∀f,u. fn_return (\fst (function_switch_removal f u)) = fn_return f. 683 #f #u elim f #ret #args #vars #body normalize elim (switch_removal body u) 684 * * #body' #Hswitch_free #new_vars #u' normalize // 685 qed. 686 687 lemma while_commute : ∀e0, s0, us0. Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0). 688 #e0 #s0 #us0 normalize 689 cases (switch_removal s0 us0) * * #body #Hswfree #newvars #u' normalize // 690 qed. 1004 (* misc properties of the max function on positives. *) 691 1005 692 1006 lemma max_one_neutral : ∀v. max v one = v. … … 723 1037 #a @(le_to_leb_true a a) // qed. 724 1038 725 (*726 lemma le_S_contradiction : ∀a,b. le (succ a) b → le (succ b) a → False.727 #a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2)) #Heq728 destruct inversion H2729 [ 2: #m #H1 #H2 #H3730 elim b; normalize in match (succ ?);731 [ 1: #H destruct (H)732 | 2: #p #H733 *)734 1039 (* This should be somewhere else. *) 735 1040 lemma associative_max : associative ? max. … … 777 1082 #Hca /2/ 778 1083 ] 779 ] qed. 1084 ] qed. 780 1085 781 1086 lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3). 782 1087 * #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max // 783 1088 qed. 784 1089 (* 785 1090 lemma max_of_expr_rewrite : 786 1091 ∀e,id. max_of_expr e id = max_id (max_of_expr e (an_identifier SymbolTag one)) id. … … 812 1117 whd in match (max_id ??); >associative_max @refl 813 1118 ] qed. 814 1119 *) 1120 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. 1121 * #a * #b * #u normalize 1122 lapply (pos_compare_to_Prop a b) 1123 cases (pos_compare a b) whd in ⊢ (% → ?); #Hab 1124 [ 1: >(le_to_leb_true a b) try /2/ #Hbu @conj /2/ 1125 | 2: destruct >reflexive_leb /2/ 1126 | 3: >(not_le_to_leb_false a b) try /2/ #Hau @conj /2/ 1127 ] qed. 1128 1129 (* Auxilliary commutation lemma used in [substatement_fresh]. *) 1130 1131 lemma foldl_max : ∀l,a,b. 1132 foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l = 1133 max_id a (foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) b l). 1134 #l elim l 1135 [ 1: * #a * #b whd in match (foldl ?????) in ⊢ (??%%); @refl 1136 | 2: #hd #tl #Hind #a #b whd in match (foldl ?????) in ⊢ (??%%); 1137 <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl 1138 ] qed. 1139 1140 (* ----------------------------------------------------------------------------- 1141 Stuff on memory and environments extensions. 1142 Let us recap: the memory model of a function is in two layers. An environment 1143 (type [env]) maps identifiers to blocks, and a memory maps blocks 1144 switch_removal introduces new, fresh variables. What is to be noted is that 1145 switch_removal modifies both the contents of the "disjoint" part of memory, but 1146 also where the data is allocated. The first solution considered was to consider 1147 an extensional equivalence relation on values, saying that equivalent pointers 1148 point to equivalent values. This has to be a coinductive relation, in order to 1149 take into account cyclic data structures. Rather than using coinductive types, 1150 we use the compcert solution, using so-called memory embeddings. 1151 ---------------------------------------------------------------------------- *) 1152 1153 (* ---------------- *) 1154 (* auxillary lemmas *) 1155 lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true. 1156 #a #b #HA 1157 lapply (Zltb_true_to_Zlt … HA) #HA_prop 1158 @Zlt_to_Zltb_true /2/ 1159 qed. 1160 1161 lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true. 1162 #a @Zlt_to_Zltb_true /2/ qed. 1163 1164 1165 definition le_offset : offset → offset → bool ≝ 1166 λx,y. Zleb (offv x) (offv y). 1167 1168 lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed. 1169 1170 lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed. 1171 1172 (* When equality on A is decidable, [mem A elt l] is too. *) 1173 lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l). 1174 #A #dec #elt #l elim l 1175 [ 1: normalize %2 /2/ 1176 | 2: #hd #tl #Hind 1177 elim (dec elt hd) 1178 [ 1: #Heq >Heq %1 /2/ 1179 | 2: #Hneq cases Hind 1180 [ 1: #Hmem %1 /2/ 1181 | 2: #Hnmem %2 normalize 1182 % #H cases H 1183 [ 1: lapply Hneq * #Hl #Eq @(Hl Eq) 1184 | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ] 1185 ] ] ] 1186 qed. 1187 1188 lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b. 1189 #a #b @(eq_block_elim … a b) /2/ qed. 1190 1191 lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2. 1192 #l #elt1 #elt2 elim l 1193 [ 1: normalize #Habsurd @(False_ind … Habsurd) 1194 | 2: #hd #tl #Hind normalize #Hl #Hr 1195 cases Hl 1196 [ 1: #Heq >Heq 1197 @(eq_block_elim … hd elt2) 1198 [ 1: #Heq >Heq /2 by not_to_not/ 1199 | 2: #x @x ] 1200 | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl) 1201 [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2 1202 | 2: #Hmem2 @Hind // 1203 ] 1204 ] 1205 ] qed. 1206 1207 lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false. 1208 #b1 #b2 * #Hb 1209 @(eq_block_elim … b1 b2) 1210 [ 1: #Habsurd @(False_ind … (Hb Habsurd)) 1211 | 2: // ] qed. 1212 1213 (* Type of blocks in a particular region. *) 1214 definition block_in : region → Type[0] ≝ λrg. Σb. (block_region b) = rg. 1215 1216 (* An embedding is a function from blocks to (blocks+offset). *) 1217 definition embedding ≝ block → option (block × offset). 1218 1219 definition offset_plus : offset → offset → offset ≝ 1220 λo1,o2. mk_offset (offv o1 + offv o2). 1221 1222 lemma offset_plus_O : ∀o. offset_plus o (mk_offset OZ) = o. 1223 * #z normalize // qed. 1224 1225 (* Translates a pointer through an embedding. *) 1226 definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝ 1227 λp,E. 1228 match p with 1229 [ mk_pointer pblock poff ⇒ 1230 match E pblock with 1231 [ None ⇒ None ? 1232 | Some loc ⇒ 1233 let 〈dest_block,dest_off〉 ≝ loc in 1234 let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in 1235 Some ? ptr 1236 ] 1237 ]. 1238 1239 (* We parameterise the "equivalence" relation on values with an embedding. *) 1240 (* Front-end values. *) 1241 inductive value_eq (E : embedding) : val → val → Prop ≝ 1242 | undef_eq : ∀v. 1243 value_eq E Vundef v 1244 | vint_eq : ∀sz,i. 1245 value_eq E (Vint sz i) (Vint sz i) 1246 | vfloat_eq : ∀f. 1247 value_eq E (Vfloat f) (Vfloat f) 1248 | vnull_eq : 1249 value_eq E Vnull Vnull 1250 | vptr_eq : ∀p1,p2. 1251 pointer_translation p1 E = Some ? p2 → 1252 value_eq E (Vptr p1) (Vptr p2). 1253 1254 (* [load_sim] states the fact that each successful load in [m1] is matched by such a load in [m2] s.t. 1255 * the values are equivalent. *) 1256 definition load_sim ≝ 1257 λ(E : embedding).λ(m1 : mem).λ(m2 : mem). 1258 ∀b1,off1,b2,off2,ty,v1. 1259 valid_block m1 b1 → 1260 E b1 = Some ? 〈b2,off2〉 → 1261 load_value_of_type ty m1 b1 off1 = Some ? v1 → 1262 (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2). 1263 1264 (* Definition of a memory injection *) 1265 record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝ 1266 { (* Load simulation *) 1267 mi_inj : load_sim E m1 m2; 1268 (* Invalid blocks are not mapped *) 1269 mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; 1270 (* Blocks in the codomain are valid *) 1271 mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; 1272 (* Regions are preserved *) 1273 mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b'; 1274 (* Disjoint blocks are mapped to disjoint blocks. Note that our condition is stronger than compcert's. 1275 * This may cause some problems if we reuse this def for the translation from Clight to Cminor, where 1276 * all variables are allocated in the same block. *) 1277 mi_disjoint : ∀b1,b2,b1',b2',o1',o2'. 1278 b1 ≠ b2 → 1279 E b1 = Some ? 〈b1',o1'〉 → 1280 E b2 = Some ? 〈b2',o2'〉 → 1281 b1' ≠ b2' 1282 }. 1283 1284 (* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\ 1285 * A memory extension is a [memory_inj] with some particular blocks designated *) 1286 1287 alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)". 1288 1289 record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝ 1290 { me_inj : memory_inj E m1 m2; 1291 me_writeable : list block; 1292 me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b; 1293 me_writeable_ok : ∀b,b',o'. 1294 valid_block m1 b → 1295 E b = Some ? 〈b',o'〉 → 1296 ¬ (meml ? b' me_writeable) 1297 }. 1298 1299 (* ---------------------------------------------------------------------------- *) 1300 (* End of the definitions on memory injections. Now, on to proving some lemmas. *) 1301 1302 (* A particular inversion. *) 1303 lemma value_eq_ptr_inversion : 1304 ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2. 1305 #E #p1 #v #Heq inversion Heq 1306 [ 1: #v #Habsurd destruct (Habsurd) 1307 | 2: #sz #i #Habsurd destruct (Habsurd) 1308 | 3: #f #Habsurd destruct (Habsurd) 1309 | 4: #Habsurd destruct (Habsurd) 1310 | 5: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct 1311 %{p2} @conj try @refl try assumption 1312 ] qed. 1313 1314 (* If we succeed to load something by value from a 〈b,off〉 location, 1315 [b] is a valid block. *) 1316 lemma load_by_value_success_valid_block_aux : 1317 ∀ty,m,b,off,v. 1318 access_mode ty = By_value (typ_of_type ty) → 1319 load_value_of_type ty m b off = Some ? v → 1320 Zltb (block_id b) (nextblock m) = true. (* → valid_block m b *) 1321 #ty #m * #brg #bid #off #v whd in match (valid_block ??); 1322 cases ty 1323 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 1324 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] 1325 whd in match (load_value_of_type ????); 1326 [ 1,7,8: #_ #Habsurd destruct (Habsurd) ] 1327 #Hmode 1328 [ 1,2,3,6: [ 1: elim sz | 2: elim fsz ] 1329 normalize in match (typesize ?); 1330 whd in match (loadn ???); 1331 whd in match (beloadv ??); 1332 cases (Zltb bid (nextblock m)) normalize nodelta 1333 try // #Habsurd destruct (Habsurd) 1334 | *: normalize in Hmode; destruct (Hmode) 1335 ] qed. 1336 1337 1338 lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b. 1339 * #rg #id #m normalize 1340 elim id /2/ qed. 1341 1342 lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true. 1343 * #rg #id #m normalize 1344 elim id /2/ qed. 1345 1346 lemma load_by_value_success_valid_block : 1347 ∀ty,m,b,off,v. 1348 access_mode ty = By_value (typ_of_type ty) → 1349 load_value_of_type ty m b off = Some ? v → 1350 valid_block m b. 1351 #ty #m #b #off #v #Haccess_mode #Hload 1352 @valid_block_from_bool 1353 @(load_by_value_success_valid_block_aux ty m b off v Haccess_mode Hload) 1354 qed. 1355 1356 (* Making explicit the contents of memory_inj for load_value_of_type *) 1357 lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty. 1358 memory_inj E m1 m2 → 1359 value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) → 1360 load_value_of_type ty m1 b1 off1 = Some ? v1 → 1361 ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2. 1362 #E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq 1363 lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct 1364 normalize in Hembed; 1365 lapply (mi_inj … Hinj b1 off1) 1366 cases (E b1) in Hembed; 1367 [ 1: normalize #Habsurd destruct (Habsurd) 1368 | 2: * #b2' #off2' #H normalize in H; destruct (H) #Hyp lapply (Hyp b2 off2' ty v1) -Hyp ] 1369 lapply (refl ? (access_mode ty)) 1370 cases ty 1371 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 1372 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] 1373 normalize in ⊢ ((???%) → ?); #Hmode #Hyp 1374 [ 1,7,8: #Habsurd normalize in Habsurd; destruct (Habsurd) 1375 | 5,6: #Heq normalize in Heq; destruct (Heq) /4 by ex_intro, conj/ ] 1376 #Hload_success 1377 lapply (load_by_value_success_valid_block … Hmode … Hload_success) 1378 #Hvalid_block @(Hyp Hvalid_block (refl ??) Hload_success) 1379 qed. 1380 1381 1382 (* -------------------------------------- *) 1383 (* Lemmas pertaining to memory allocation *) 1384 1385 (* A valid block stays valid after an alloc. *) 1386 lemma alloc_valid_block_conservation : 1387 ∀m,m',z1,z2,r,new_block. 1388 alloc m z1 z2 r = 〈m', new_block〉 → 1389 ∀b. valid_block m b → valid_block m' b. 1390 #m #m' #z1 #z2 #r * #b' #Hregion_eq 1391 elim m #contents #nextblock #Hcorrect whd in match (alloc ????); 1392 #Halloc destruct (Halloc) 1393 #b whd in match (valid_block ??) in ⊢ (% → %); /2/ 1394 qed. 1395 1396 (* Allocating a new zone produces a valid block. *) 1397 lemma alloc_valid_new_block : 1398 ∀m,m',z1,z2,r,new_block. 1399 alloc m z1 z2 r = 〈m', new_block〉 → 1400 valid_block m' new_block. 1401 * #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq 1402 whd in match (alloc ????); whd in match (valid_block ??); 1403 #Halloc destruct (Halloc) /2/ 1404 qed. 1405 1406 (* All data in a valid block is unchanged after an alloc. *) 1407 lemma alloc_beloadv_conservation : 1408 ∀m,m',block,offset,z1,z2,r,new_block. 1409 valid_block m block → 1410 alloc m z1 z2 r = 〈m', new_block〉 → 1411 beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset). 1412 * #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc 1413 whd in Halloc:(??%?); destruct (Halloc) 1414 whd in match (beloadv ??) in ⊢ (??%%); 1415 lapply (valid_block_to_bool … Hvalid) #Hlt 1416 >Hlt >(zlt_succ … Hlt) 1417 normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??); 1418 cut (eqZb (block_id block) next = false) 1419 [ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq 1420 >Hneq cases (eq_region ??) normalize nodelta @refl 1421 qed. 1422 1423 (* Lift [alloc_beloadv_conservation] to loadn *) 1424 lemma alloc_loadn_conservation : 1425 ∀m,m',z1,z2,r,new_block. 1426 alloc m z1 z2 r = 〈m', new_block〉 → 1427 ∀n. ∀block,offset. 1428 valid_block m block → 1429 loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n. 1430 #m #m' #z1 #z2 #r #new_block #Halloc #n 1431 elim n try // 1432 #n' #Hind #block #offset #Hvalid_block 1433 whd in ⊢ (??%%); 1434 >(alloc_beloadv_conservation … Hvalid_block Halloc) 1435 cases (beloadv m' (mk_pointer block offset)) // 1436 #bev normalize nodelta 1437 whd in match (shift_pointer ???); >Hind try // 1438 qed. 1439 1440 (* Memory allocation preserves [memory_inj] *) 1441 lemma alloc_memory_inj : 1442 ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2. 1443 alloc m2 z1 z2 r = 〈m2', new_block〉 → 1444 memory_inj E m1 m2'. 1445 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc 1446 % 1447 [ 1: 1448 whd 1449 #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload 1450 elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload) 1451 #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try // 1452 lapply (refl ? (access_mode ty)) 1453 cases ty in Hload_eq; 1454 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 1455 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] 1456 #Hload normalize in ⊢ ((???%) → ?); #Haccess 1457 [ 1,7,8: normalize in Hload; destruct (Hload) 1458 | 2,3,4,9: whd in match (load_value_of_type ????); 1459 whd in match (load_value_of_type ????); 1460 lapply (load_by_value_success_valid_block … Haccess Hload) 1461 #Hvalid_block 1462 whd in match (load_value_of_type ????) in Hload; 1463 <(alloc_loadn_conservation … Halloc … Hvalid_block) 1464 @Hload 1465 | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ] 1466 | 2: @(mi_freeblock … Hmemory_inj) 1467 | 3: #b #b' #o' #HE 1468 lapply (mi_incl … Hmemory_inj … HE) 1469 elim m2 in Halloc; #contents #nextblock #Hnextblock 1470 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 1471 whd in match (valid_block ??) in ⊢ (% → %); /2/ 1472 | 4: @(mi_region … Hmemory_inj) 1473 | 5: @(mi_disjoint … Hmemory_inj) 1474 ] qed. 1475 1476 (* Memory allocation induces a memory extension. *) 1477 lemma alloc_memory_ext : 1478 ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2. 1479 alloc m2 z1 z2 r = 〈m2', new_block〉 → 1480 memory_ext E m1 m2'. 1481 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc 1482 lapply (alloc_memory_inj … Hmemory_inj Halloc) 1483 #Hinj' % 1484 [ 1: @Hinj' 1485 | 2: @[new_block] 1486 | 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ] 1487 #Heq destruct (Heq) whd elim m2 in Halloc; 1488 #Hcontents #nextblock #Hnextblock 1489 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 1490 /2/ 1491 | 4: #b #b' #o' normalize in ⊢ (% → ?); #Hvalid_b #Hload % 1492 normalize in ⊢ (% → ?); * [ 2: #H @(False_ind … H) ] 1493 #Heq destruct (Heq) 1494 lapply (mi_incl … Hmemory_inj … Hload) 1495 whd in ⊢ (% → ?); #Habsurd 1496 (* contradiction car ¬ (valid_block m2 new_block) *) 1497 elim m2 in Halloc Habsurd; 1498 #contents_m2 #nextblock_m2 #Hnextblock_m2 1499 whd in ⊢ ((??%?) → ?); 1500 #Heq_alloc destruct (Heq_alloc) 1501 lapply (irreflexive_Zlt nextblock_m2) * #Hcontr #Habsurd @(Hcontr Habsurd) 1502 ] qed. 1503 1504 lemma bestorev_beloadv_conservation : 1505 ∀mA,mB,wb,wo,v. 1506 bestorev mA (mk_pointer wb wo) v = Some ? mB → 1507 ∀rb,ro. eq_block wb rb = false → 1508 beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro). 1509 #mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq 1510 whd in ⊢ (??%%); 1511 elim mB in Hstore; #contentsB #nextblockB #HnextblockB 1512 normalize in ⊢ (% → ?); 1513 cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta 1514 [ 2: #Habsurd destruct (Habsurd) ] 1515 cases (if Zleb (low (blocks mA wb)) (offv wo) 1516 then Zltb (offv wo) (high (blocks mA wb)) 1517 else false) normalize nodelta 1518 [ 2: #Habsurd destruct (Habsurd) ] 1519 #Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid 1520 cases rr cases wr normalize try // 1521 @(eqZb_elim … rid wid) 1522 [ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ] 1523 try // 1524 qed. 1525 1526 (* lift [bestorev_beloadv_conservation to [loadn] *) 1527 lemma bestorev_loadn_conservation : 1528 ∀mA,mB,n,wb,wo,v. 1529 bestorev mA (mk_pointer wb wo) v = Some ? mB → 1530 ∀rb,ro. eq_block wb rb = false → 1531 loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n. 1532 #mA #mB #n 1533 elim n 1534 [ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl 1535 | 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq 1536 whd in ⊢ (??%%); 1537 >(bestorev_beloadv_conservation … Hstore … Hneq) 1538 >(Hind … Hstore … Hneq) @refl 1539 ] qed. 1540 1541 (* lift [bestorev_loadn_conservation] to [load_value_of_type] *) 1542 lemma bestorev_load_value_of_type_conservation : 1543 ∀mA,mB,wb,wo,v. 1544 bestorev mA (mk_pointer wb wo) v = Some ? mB → 1545 ∀rb,ro. eq_block wb rb = false → 1546 ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro. 1547 #mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty 1548 cases ty 1549 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 1550 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] try // 1551 [ 1: elim sz | 2: elim fsz | 3: | 4: ] 1552 whd in ⊢ (??%%); 1553 >(bestorev_loadn_conservation … Hstore … Hneq) @refl 1554 qed. 1555 1556 (* Writing in the "extended" part of a memory preserves the underlying injection *) 1557 lemma bestorev_memory_ext_to_load_sim : 1558 ∀E,mA,mB,mC. 1559 ∀Hext:memory_ext E mA mB. 1560 ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 1561 bestorev mB (mk_pointer wb wo) v = Some ? mC → 1562 load_sim E mA mC. 1563 #E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd 1564 #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload 1565 (* Show that (wb ≠ b2) *) 1566 lapply (me_writeable_ok … Hext … Hvalid Hembed) #Hb2 1567 lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2 1568 cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false 1569 <(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false) 1570 @(mi_inj … (me_inj … Hext) … Hvalid … Hembed … Hload) 1571 qed. 1572 1573 (* Writing in the "extended" part of a memory preserves the whole memory injection *) 1574 lemma bestorev_memory_ext_to_memory_inj : 1575 ∀E,mA,mB,mC. 1576 ∀Hext:memory_ext E mA mB. 1577 ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 1578 bestorev mB (mk_pointer wb wo) v = Some ? mC → 1579 memory_inj E mA mC. 1580 #E #mA * #contentsB #nextblockB #HnextblockB #mC 1581 #Hext #wb #wo #v #Hwb #Hstore 1582 % 1583 [ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ] 1584 elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok 1585 #Hmem 1586 [ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] - Hvalid -Hregion -Hdisjoint -Hwriteable_ok -Hinj 1587 whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem) 1588 normalize in ⊢ (% → ?); #Hlt_wb 1589 >(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta 1590 cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb))) 1591 normalize nodelta 1592 [ 2: #Habsurd destruct (Habsurd) ] 1593 #Heq destruct (Heq) 1594 #b #b' #o' #Hembed @(Hcodomain … Hembed) 1595 qed. 1596 1597 (* It even preserves memory extensions, with the same writeable blocks. *) 1598 lemma bestorev_memory_ext_to_memory_ext : 1599 ∀E,mA,mB. 1600 ∀Hext:memory_ext E mA mB. 1601 ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 1602 ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC → 1603 ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext). 1604 #E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore 1605 %{(mk_memory_ext … 1606 (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore) 1607 (me_writeable … Hext) 1608 ? 1609 (me_writeable_ok … Hext) 1610 )} try @refl 1611 #b #Hmemb 1612 lapply (me_writeable_valid … Hext b Hmemb) 1613 lapply (me_writeable_valid … Hext wb Hmem) 1614 elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid 1615 lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?); 1616 >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta 1617 cases (if Zleb (low (contentsB wb)) (offv wo) 1618 then Zltb (offv wo) (high (contentsB wb)) 1619 else false) 1620 normalize [ 2: #Habsurd destruct (Habsurd) ] 1621 #Heq destruct (Heq) @Hb_valid 1622 qed. 1623 1624 (* Lift [bestorev_memory_ext_to_memory_ext] to storen *) 1625 lemma storen_memory_ext_to_memory_ext : 1626 ∀E,mA,l,mB,mC. 1627 ∀Hext:memory_ext E mA mB. 1628 ∀wb,wo. meml ? wb (me_writeable … Hext) → 1629 storen mB (mk_pointer wb wo) l = Some ? mC → 1630 memory_ext E mA mC. 1631 #E #mA #l elim l 1632 [ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq) 1633 @Hext 1634 | 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem 1635 whd in ⊢ ((??%?) → ?); 1636 lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem) 1637 cases (bestorev mB (mk_pointer wb wo) hd) 1638 normalize nodelta 1639 [ 1: #H #Habsurd destruct (Habsurd) ] 1640 #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore 1641 @(Hind … HextD … Hstore) 1642 <Heq @Hmem 1643 ] qed. 1644 1645 (* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *) 1646 lemma store_value_of_type_memory_ext_to_memory_ext : 1647 ∀E,mA,mB,mC. 1648 ∀Hext:memory_ext E mA mB. 1649 ∀wb,wo. meml ? wb (me_writeable … Hext) → 1650 ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC → 1651 memory_ext E mA mC. 1652 #E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v 1653 cases ty 1654 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 1655 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] 1656 whd in ⊢ ((??%?) → ?); 1657 [ 1,5,6,7,8: #Habsurd destruct (Habsurd) ] 1658 #Hstore 1659 @(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore) 1660 qed. 1661 1662 (* End of the memory injection-related stuff. *) 1663 (* ------------------------------------------ *) 1664 1665 (* Lookup functions in list environments (used to type local variables in functions) *) 1666 let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝ 1667 match l with 1668 [ nil ⇒ false 1669 | cons hd tl ⇒ 1670 let 〈id, ty〉 ≝ hd in 1671 match identifier_eq SymbolTag i id with 1672 [ inl Hid_eq ⇒ true 1673 | inr Hid_neq ⇒ mem_assoc_env i tl 1674 ] 1675 ]. 1676 1677 let rec assoc_env (i : ident) (l : list (ident×type)) on l : option type ≝ 1678 match l with 1679 [ nil ⇒ None ? 1680 | cons hd tl ⇒ 1681 let 〈id, ty〉 ≝ hd in 1682 match identifier_eq SymbolTag i id with 1683 [ inl Hid_eq ⇒ Some ? ty 1684 | inr Hid_neq ⇒ assoc_env i tl 1685 ] 1686 ]. 1687 1688 (* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension 1689 of the environment [e1] s.t. the new binders are in [new], and such that those 1690 new binders are "writeable" in the memory extension [Hext] *) 1691 definition disjoint_extension ≝ 1692 λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem). 1693 λ(new : list (ident × type)). λ(E:embedding). λ(Hext: memory_ext E m1 m2). 1694 ∀id. match mem_assoc_env id new with 1695 [ true ⇒ 1696 ∃b. lookup ?? e2 id = Some ? b 1697 ∧ meml ? b (me_writeable … Hext) 1698 ∧ lookup ?? e1 id = None ? 1699 | false ⇒ 1700 match lookup ?? e1 id with 1701 [ None ⇒ lookup ?? e2 id = None ? 1702 | Some b1 ⇒ 1703 match lookup ?? e2 id with 1704 [ None ⇒ False 1705 | Some b2 ⇒ 1706 valid_block m1 b1 ∧ 1707 value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset)) 1708 ] 1709 ] 1710 ]. 1711 1712 (* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if 1713 * the variable is not in a local environment, then we search into the global one. 1714 * A proper "extension" of a local environment should be such that the extension 1715 * does not collide with a given global env. 1716 * To see the details of why we need that, see [exec_lvalue'], Evar id case. 1717 *) 1718 definition ext_fresh_for_genv ≝ 1719 λ(ext : list (ident × type)). λ(ge : genv). 1720 ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?. 1721 1722 (* Any environment is a "disjoint" extension of itself with nothing. *) 1723 (* 1724 lemma disjoint_extension_nil : ∀e,m,types. disjoint_extension e m e m types []. 1725 #e #m #ty #id 1726 normalize in match (mem_assoc_env id []); normalize nodelta 1727 cases (lookup ?? e id) try // 1728 #b normalize nodelta 1729 % #ty cases (load_value_of_type ????) 1730 [ 1: %2 /2/ | 2: #v %1 %{v} %{v} @conj // 1731 cases (assoc_env id ty) // 1732 qed. *) 1733 1734 1735 (* "generic" simulation relation on [res ?] *) 1736 definition res_sim ≝ 1737 λ(A : Type[0]). 1738 λ(eq : A → A → Prop). 1739 λ(r1, r2 : res A). 1740 ∀a1. r1 = OK ? a1 → ∃a2. r2 = OK ? a2 ∧ eq a1 a2. 1741 1742 (* Specialisation of [res_sim] to match [exec_expr] *) 1743 definition exec_expr_sim ≝ λE. 1744 res_sim (val × trace) (λr1,r2. value_eq E (\fst r1) (\fst r2) ∧ (\snd r1 = \snd r2)). 1745 1746 (* Specialisation of [res_sim] to match [exec_lvalue] *) 1747 definition exec_lvalue_sim ≝ λE. 1748 res_sim (block × offset × trace) 1749 (λr1,r2. 1750 let 〈b1,o1,tr1〉 ≝ r1 in 1751 let 〈b2,o2,tr2〉 ≝ r2 in 1752 value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) ∧ tr1 = tr2). 1753 1754 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. 1755 #ty #m #b #o cases (load_value_of_type ty m b o) 1756 [ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed. 1757 1758 (* 1759 lemma switch_removal_alloc_extension : ∀f, f', vars, env, env', m, m'. 1760 env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) → 1761 〈f',vars〉 = function_switch_removal f → 1762 env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) → 1763 environment_extension env env' vars. 1764 1765 #f #f' 1766 cut (∀l:list (ident × type). [ ] @ l = l) [ // ] #nil_append 1767 cases (fn_params f) cases (fn_vars f) 1768 [ 1: #vars >append_nil >append_nil >nil_append elim vars 1769 [ 1: #env #env' #m #m' normalize in ⊢ (% → ? → % → ?); #Henv1 #_ #Henv2 destruct // 1770 | 2: #hd #tl #Hind #env #env' #m #m' #Henv1 #Heq 1771 whd in ⊢ ((???(???%)) → ?); 1772 #Henv #Hswrem #Henv' 1773 #id 1774 *) 1775 1776 (* 1777 lemma substatement_fresh : ∀s,u. 1778 fresh_for_statement s u → 1779 substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u). 1780 #s #u @(statement_ind2 ? (λls.fresh_for_labeled_statements ls u → substatement_ls ls (λs':statement.fresh_for_statement s' u)) … s) 1781 try /by I/ 1782 [ 1: #e1 #e2 #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj assumption 1783 | 2: * 1784 [ 1: #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) * 1785 #Hfresh_e #Hfresh_args @conj try assumption 1786 normalize nodelta in Hfresh_args; 1787 >max_id_commutative in Hfresh_args; >max_id_one_neutral 1788 #Hfresh_args 1789 | 2: #ret #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) * 1790 #Hfresh_e #H lapply (fresh_max_split ??? H) * 1791 #Hfresh_ret #Hfresh_args @conj try @conj try assumption ] 1792 elim args in Hfresh_args; 1793 [ 1,3: // 1794 | 2,4: #hd #tl #Hind whd in match (foldl ?????); whd in match (All ???); 1795 >foldl_max #H elim (fresh_max_split ??? H) #Hu #HAll @conj 1796 [ 1,3: @Hu 1797 | 2,4: @Hind assumption ] ] 1798 | 3: #s1 #s2 #_ #_ 1799 whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * 1800 whd in match (substatement_P ??); /2/ 1801 | 4: #e #cond #iftrue #iffalse #_ 1802 whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * 1803 #Hexpr #H2 lapply (fresh_max_split … H2) * /2/ 1804 | 5,6: #e #stm #_ 1805 whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * /2/ 1806 | 7: #init #cond #step #body #_ #_ #_ #H lapply (fresh_max_split … H) * 1807 #H1 #H2 elim (fresh_max_split … H1) #Hinit #Hcond 1808 elim (fresh_max_split … H2) #Hstep #Hbody whd @conj try @conj try @conj /3/ 1809 | 8: #ret #H whd elim ret in H; try // 1810 | 9: #expr #ls #Hind #H whd @conj 1811 [ 1: elim (fresh_max_split … H) // 1812 | 2: @Hind elim (fresh_max_split … H) // ] 1813 | 10: #l #body #Hind #H whd elim (fresh_max_split … H) // 1814 | 11: #sz #i #hd #tl #Hhd #Htl #H whd 1815 elim (fresh_max_split … H) #Htl_fresh #Hhd_fresh @conj // 1816 @Htl // 1817 ] qed. 1818 *) 1819 1820 (* Eliminating switches introduces fresh variables. [environment_extension] characterizes 1821 * a local environment extended by some local variables. *) 1822 1823 1824 (* lookup on environment extension *) 1825 (* 1826 lemma extension_lookup : 1827 ∀map, map', ext, id, result. 1828 environment_extension map map' ext → 1829 lookup ?? map id = Some ? result → 1830 lookup ?? map' id = Some ? result. 1831 #map #map' #ext #id #result #Hext lapply (Hext id) 1832 cases (mem_assoc_env ??) normalize nodelta 1833 [ 1: * * #ext_result #H1 >H1 #Habsurd destruct (Habsurd) 1834 | 2: #H >H // ] qed. 1835 1836 *) 1837 1838 (* Extending a map by an empty list of variables yields an observationally equivalent 1839 * environment. *) 1840 (* 1841 lemma environment_extension_nil : ∀en,en':env. (environment_extension en en' [ ]) → imap_eq ?? en en'. 1842 * #map1 * #map2 whd in ⊢ (% → ?); #Hext whd % #id #v #H 1843 [ 1: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta 1844 cases (lookup_opt block id map2) normalize 1845 [ 1: >H #H2 >H2 @refl 1846 | 2: #b >H cases v 1847 [ 1: normalize * #H @(False_ind … H) 1848 | 2: #block normalize // ] ] 1849 | 2: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta 1850 >H cases v normalize try // 1851 #block cases (lookup_opt ? id map1) normalize try // 1852 * #H @(False_ind … H) 1853 ] qed. *) 1854 1855 (* If two identifier maps are observationally equal, then they contain the same bocks. 1856 * see maps_obsequiv.ma for the details of the proof. *) 1857 (* 1858 lemma blocks_of_env_eq : ∀e,e'. imap_eq ?? e e' → blocks_of_env e = blocks_of_env e'. 1859 * #map1 * #map2 normalize #Hpmap_eq lapply (pmap_eq_fold … Hpmap_eq) #Hfold 1860 >Hfold @refl 1861 qed. 1862 *) 1863 1864 (* Simulation relations. *) 1865 inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝ 1866 | swc_stop : ∀fvs. 1867 switch_cont_sim fvs Kstop Kstop 1868 | swc_seq : ∀fvs,s,k,k',u,result. 1869 fresh_for_statement s u → 1870 switch_cont_sim fvs k k' → 1871 switch_removal s fvs u = Some ? result → 1872 switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k') 1873 | swc_while : ∀fvs,e,s,k,k',u,result. 1874 fresh_for_statement (Swhile e s) u → 1875 switch_cont_sim fvs k k' → 1876 switch_removal s fvs u = Some ? result → 1877 switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k') 1878 | swc_dowhile : ∀fvs,e,s,k,k',u,result. 1879 fresh_for_statement (Sdowhile e s) u → 1880 switch_cont_sim fvs k k' → 1881 switch_removal s fvs u = Some ? result → 1882 switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k') 1883 | swc_for1 : ∀fvs,e,s1,s2,k,k',u,result. 1884 fresh_for_statement (Sfor Sskip e s1 s2) u → 1885 switch_cont_sim fvs k k' → 1886 switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result → 1887 switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k') 1888 | swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2. 1889 fresh_for_statement (Sfor Sskip e s1 s2) u → 1890 switch_cont_sim fvs k k' → 1891 switch_removal s1 fvs u = Some ? result1 → 1892 switch_removal s2 fvs (ret_u ? result1) = Some ? result2 → 1893 switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k') 1894 | swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2. 1895 fresh_for_statement (Sfor Sskip e s1 s2) u → 1896 switch_cont_sim fvs k k' → 1897 switch_removal s1 fvs u = Some ? result1 → 1898 switch_removal s2 fvs (ret_u ? result1) = Some ? result2 -> 1899 switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k') 1900 | swc_switch : ∀fvs,k,k'. 1901 switch_cont_sim fvs k k' → 1902 switch_cont_sim fvs (Kswitch k) (Kswitch k') 1903 | swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *) 1904 switch_cont_sim fvs k k' → 1905 (* /!\ Update [en] with [fvs'] ... *) 1906 switch_cont_sim 1907 (map … (fst ??) (\snd (function_switch_removal f))) 1908 (Kcall r f en k) 1909 (Kcall r (\fst (function_switch_removal f)) en' k'). 1910 1911 1912 (* 1913 en' = exec_alloc_variables en m (\snd (function_switch_removal f)) 1914 TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc 1915 variable dans en'. 1916 1917 1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que 1918 dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est 1919 de savoir que : 1920 si je lookup une variable générée à partir d'un univers frais dans l'environement en', 1921 alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step, 1922 et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s" 1923 et à etre "(function_switch_removal f)-contained". 1924 1925 2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup 1926 et l'update n'altèrent pas le comportement du reste du programme. 1927 1928 relation : si un statement S0 est inclus dans un statement S1, alors les variables générées 1929 depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1. 1930 en particulier, si u est frais pour S1 u est frais pour S0. 1931 1932 Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique 1933 "environment_extension en en' (\fst (\fst (switch_removal s u)))" 1934 1935 --------------------------------------------------------------- 1936 . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction 1937 et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération. 1938 on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner 1939 en argument les freshgens qui correspondent à ce que la fonction switch_removal fait. 1940 *) 1941 1942 inductive switch_state_sim : state → state → Prop ≝ 1943 | sws_state : ∀u,f,s,k,k',m,m',result. 1944 ∀env, env', f', vars. 1945 ∀E:embedding. 1946 ∀Hext:memory_ext E m m'. 1947 fresh_for_statement s u → 1948 (* 1949 env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) → 1950 env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) → 1951 *) 1952 〈f',vars〉 = function_switch_removal f → 1953 disjoint_extension env m env' m' vars E Hext → 1954 switch_removal s (map ?? (fst ??) vars) u = Some ? result → 1955 switch_cont_sim (map ?? (fst ??) vars) k k' → 1956 switch_state_sim 1957 (State f s k env m) 1958 (State f' (ret_st ? result) k' env' m') 1959 | sws_callstate : ∀vars, fd,args,k,k',m. 1960 switch_cont_sim vars k k' → 1961 switch_state_sim (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m) 1962 | sws_returnstate : ∀vars,res,k,k',m. 1963 switch_cont_sim vars k k' → 1964 switch_state_sim (Returnstate res k m) (Returnstate res k' m) 1965 | sws_finalstate : ∀r. 1966 switch_state_sim (Finalstate r) (Finalstate r). 1967 1968 lemma call_cont_swremoval : ∀fv,k,k'. 1969 switch_cont_sim fv k k' → 1970 switch_cont_sim fv (call_cont k) (call_cont k'). 1971 #fv #k0 #k0' #K elim K /2/ 1972 qed. 1973 1974 (* [eventually ge P s tr] states that after a finite number of [exec_step], the 1975 property P on states will be verified. *) 1976 inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝ 1977 | eventually_base : ∀s,t,s'. 1978 exec_step ge s = Value io_out io_in ? 〈t, s'〉 → 1979 P s' → 1980 eventually ge P s t 1981 | eventually_step : ∀s,t,s',t',trace. 1982 exec_step ge s = Value io_out io_in ? 〈t, s'〉 → 1983 eventually ge P s' t' → 1984 trace = (t ⧺ t') → 1985 eventually ge P s trace. 1986 1987 (* [eventually] is not so nice to use directly, we would like to make the mandatory 1988 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not 1989 to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *) 1990 lemma eventually_now : ∀ge,P,s,t. 1991 (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 1992 eventually ge P s t. 1993 #ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP} (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *) 1994 qed. 1995 (* 1996 lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 1997 ∃t'.eventually ge P s (t ⧺ t'). 1998 #ge #P #s #t * #s' * #Hexec #HP %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} 1999 qed. 2000 *) 2001 lemma eventually_later : ∀ge,P,s,t. 2002 (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) → 2003 eventually ge P s t. 2004 #ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq} 2005 try assumption 2006 qed. 2007 2008 (* lift value_eq to option block *) 2009 definition option_block_eq ≝ λE,ob1,ob2. 2010 match ob1 with 2011 [ None ⇒ 2012 match ob2 with 2013 [ None ⇒ True 2014 | Some _ ⇒ False ] 2015 | Some b1 ⇒ 2016 match ob2 with 2017 [ None ⇒ False 2018 | Some b2 ⇒ value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset)) ] 2019 ]. 2020 2021 definition value_eq_opt ≝ λE,ov1,ov2. 2022 match ov1 with 2023 [ None ⇒ 2024 match ov2 with 2025 [ None ⇒ True 2026 | Some _ ⇒ False ] 2027 | Some v1 ⇒ 2028 match ov2 with 2029 [ None ⇒ False 2030 | Some v2 ⇒ 2031 value_eq E v1 v2 ] 2032 ]. 2033 2034 record switch_removal_globals (E : embedding) (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { 2035 rg_find_symbol: ∀s. 2036 option_block_eq E (find_symbol ? ge s) (find_symbol ? ge' s); 2037 rg_find_funct: ∀v,f. 2038 find_funct ? ge v = Some ? f → 2039 find_funct ? ge' v = Some ? (t f); 2040 rg_find_funct_ptr: ∀b,f. 2041 find_funct_ptr ? ge b = Some ? f → 2042 find_funct_ptr ? ge' b = Some ? (t f) 2043 }. 2044 2045 lemma exec_lvalue_expr_elim : 2046 ∀E,r1,r2,Pok,Qok. 2047 ∀H:exec_lvalue_sim E r1 r2. 2048 (∀bo1,bo2,tr. 2049 let 〈b1,o1〉 ≝ bo1 in 2050 let 〈b2,o2〉 ≝ bo2 in 2051 value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) → 2052 match Pok 〈bo1,tr〉 with 2053 [ Error err ⇒ True 2054 | OK vt1 ⇒ 2055 let 〈val1,trace1〉 ≝ vt1 in 2056 match Qok 〈bo2,tr〉 with 2057 [ Error err ⇒ False 2058 | OK vt2 ⇒ 2059 let 〈val2,trace2〉 ≝ vt2 in 2060 trace1 = trace2 ∧ value_eq E val1 val2 2061 ] 2062 ]) → 2063 exec_expr_sim E 2064 (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) 2065 (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). 2066 #E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); 2067 elim r1 2068 [ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd) 2069 | 1: normalize nodelta #a1 #H lapply (H a1 (refl ??)) 2070 * #a2 * #Hr2 >Hr2 normalize nodelta 2071 elim a1 * #b1 #o1 #tr1 2072 elim a2 * #b2 #o2 #tr2 normalize nodelta 2073 * #Hvalue_eq #Htrace_eq #H2 2074 destruct (Htrace_eq) 2075 lapply (H2 〈b1, o1〉 〈b2, o2〉 tr2 Hvalue_eq) 2076 cases (Pok 〈b1, o1, tr2〉) 2077 [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd) 2078 | 1: * #v1 #tr1' normalize nodelta #H3 whd 2079 * #v1' #tr1'' #Heq destruct (Heq) 2080 cases (Qok 〈b2,o2,tr2〉) in H3; 2081 [ 2: #error #Hfalse @(False_ind … Hfalse) 2082 | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq) 2083 #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj // 2084 ] ] ] qed. 2085 2086 lemma exec_expr_expr_elim : 2087 ∀E,r1,r2,Pok,Qok. 2088 ∀H:exec_expr_sim E r1 r2. 2089 (∀v1,v2,trace. 2090 value_eq E v1 v2 → 2091 match Pok 〈v1,trace〉 with 2092 [ Error err ⇒ True 2093 | OK vt1 ⇒ 2094 let 〈val1,trace1〉 ≝ vt1 in 2095 match Qok 〈v2,trace〉 with 2096 [ Error err ⇒ False 2097 | OK vt2 ⇒ 2098 let 〈val2,trace2〉 ≝ vt2 in 2099 trace1 = trace2 ∧ value_eq E val1 val2 2100 ] 2101 ]) → 2102 exec_expr_sim E 2103 (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) 2104 (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). 2105 #E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); 2106 elim r1 2107 [ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd) 2108 | 1: normalize nodelta #a1 #H lapply (H a1 (refl ??)) 2109 * #a2 * #Hr2 >Hr2 normalize nodelta 2110 elim a1 #v1 #tr1 2111 elim a2 #v2 #tr2 normalize nodelta 2112 * #Hvalue_eq #Htrace_eq #H2 2113 destruct (Htrace_eq) 2114 lapply (H2 v1 v2 tr2 Hvalue_eq) 2115 cases (Pok 〈v1, tr2〉) 2116 [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd) 2117 | 1: * #v1 #tr1' normalize nodelta #H3 whd 2118 * #v1' #tr1'' #Heq destruct (Heq) 2119 cases (Qok 〈v2,tr2〉) in H3; 2120 [ 2: #error #Hfalse @(False_ind … Hfalse) 2121 | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq) 2122 #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj // 2123 ] ] ] qed. 2124 2125 (* Commutation results of standard binary operations with value_eq. *) 2126 lemma unary_operation_value_eq : 2127 ∀E,op,v1,v2,ty. 2128 value_eq E v1 v2 → 2129 ∀r1. 2130 sem_unary_operation op v1 ty = Some ? r1 → 2131 ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2. 2132 #E #op #v1 #v2 #ty #Hvalue_eq #r1 2133 inversion Hvalue_eq 2134 [ 1: #v #Hv1 #Hv2 #_ destruct 2135 cases op normalize 2136 [ 1: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2137 normalize #Habsurd destruct (Habsurd) 2138 | 3: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2139 normalize #Habsurd destruct (Habsurd) 2140 | 2: #Habsurd destruct (Habsurd) ] 2141 | 2: #vsz #i #Hv1 #Hv2 #_ 2142 cases op 2143 [ 1: cases ty 2144 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2145 whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???); 2146 [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct 2147 %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))} 2148 cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj 2149 // 2150 | *: #Habsurd destruct (Habsurd) ] 2151 | 2: whd in match (sem_unary_operation ???); 2152 #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj // 2153 | 3: whd in match (sem_unary_operation ???); 2154 cases ty 2155 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2156 normalize nodelta 2157 whd in ⊢ ((??%?) → ?); 2158 [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct 2159 %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj // 2160 | *: #Habsurd destruct (Habsurd) ] ] 2161 | 3: #f #Hv1 #Hv2 #_ destruct whd in match (sem_unary_operation ???); 2162 cases op normalize nodelta 2163 [ 1: cases ty 2164 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2165 whd in match (sem_notbool ??); 2166 #Heq1 destruct 2167 cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/ 2168 | 2: normalize #Habsurd destruct (Habsurd) 2169 | 3: cases ty 2170 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2171 whd in match (sem_neg ??); 2172 #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ] 2173 | 4: #Hv1 #Hv2 #_ destruct whd in match (sem_unary_operation ???); 2174 cases op normalize nodelta 2175 [ 1: cases ty 2176 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2177 whd in match (sem_notbool ??); 2178 #Heq1 destruct /3 by ex_intro, vint_eq, conj/ 2179 | 2: normalize #Habsurd destruct (Habsurd) 2180 | 3: cases ty 2181 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2182 whd in match (sem_neg ??); 2183 #Heq1 destruct ] 2184 | 5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_ whd in match (sem_unary_operation ???); 2185 cases op normalize nodelta 2186 [ 1: cases ty 2187 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2188 whd in match (sem_notbool ??); 2189 #Heq1 destruct /3 by ex_intro, vint_eq, conj/ 2190 | 2: normalize #Habsurd destruct (Habsurd) 2191 | 3: cases ty 2192 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2193 whd in match (sem_neg ??); 2194 #Heq1 destruct ] 2195 ] 2196 qed. 2197 2198 (* A cleaner version of inversion for [value_eq] *) 2199 lemma value_eq_inversion : 2200 ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 → 2201 (∀v. P Vundef v) → 2202 (∀sz,i. P (Vint sz i) (Vint sz i)) → 2203 (∀f. P (Vfloat f) (Vfloat f)) → 2204 (P Vnull Vnull) → 2205 (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) → 2206 P v1 v2. 2207 #E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5 2208 inversion Heq 2209 [ 1: #v #Hv1 #Hv2 #_ destruct @H1 2210 | 2: #sz #i #Hv1 #Hv2 #_ destruct @H2 2211 | 3: #f #Hv1 #Hv2 #_ destruct @H3 2212 | 4: #Hv1 #Hv2 #_ destruct @H4 2213 | 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed. 2214 2215 (* value_eq lifts to addition *) 2216 lemma add_value_eq : 2217 ∀E,v1,v2,v1',v2',ty1,ty2,m1,m2. 2218 value_eq E v1 v2 → 2219 value_eq E v1' v2' → 2220 memory_inj E m1 m2 → (* This injection seems useless TODO *) 2221 ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→ 2222 ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 2223 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1 2224 @(value_eq_inversion E … Hvalue_eq1) 2225 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 2226 [ 1: whd in match (sem_add ????); normalize nodelta 2227 cases (classify_add ty1 ty2) normalize nodelta 2228 [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ] 2229 #Habsurd destruct (Habsurd) 2230 | 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 2231 cases (classify_add ty1 ty2) normalize nodelta 2232 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2233 [ 2,3,5: #Habsurd destruct (Habsurd) ] 2234 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2235 [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ] 2236 [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ] 2237 [ 1: @intsize_eq_elim_elim 2238 [ 1: #_ #Habsurd destruct (Habsurd) 2239 | 2: #Heq destruct (Heq) normalize nodelta 2240 #Heq destruct (Heq) 2241 /3 by ex_intro, conj, vint_eq/ ] 2242 | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct 2243 /3 by ex_intro, conj, vint_eq/ 2244 | 3: #Heq destruct (Heq) 2245 normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed 2246 %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl 2247 @vptr_eq whd in match (pointer_translation ??); 2248 cases (E b1') in Hembed; 2249 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2250 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) 2251 whd in match (shift_pointer_n ????); 2252 cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset = 2253 (shift_offset_n (bitsize_of_intsize sz) (mk_offset (offv o1'+offv offset)) (sizeof ty) i)) 2254 [ 1: normalize >sym_Zplus <associative_Zplus >(sym_Zplus (offv offset) (offv o1')) @refl ] 2255 #Heq >Heq @refl ] 2256 ] 2257 | 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 2258 cases (classify_add ty1 ty2) normalize nodelta 2259 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2260 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2261 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2262 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2263 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 2264 #Heq destruct (Heq) 2265 /3 by ex_intro, conj, vfloat_eq/ 2266 | 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 2267 cases (classify_add ty1 ty2) normalize nodelta 2268 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2269 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 2270 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2271 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2272 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2273 @eq_bv_elim 2274 [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ 2275 | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2276 | 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 2277 cases (classify_add ty1 ty2) normalize nodelta 2278 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2279 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 2280 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2281 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2282 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2283 #Heq destruct (Heq) 2284 %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl 2285 @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; 2286 elim p1 in Hembed; #b1 #o1 normalize nodelta 2287 cases (E b1) 2288 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2289 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) 2290 normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset)) 2291 @refl 2292 ] 2293 ] qed. 2294 2295 (* TODO all other 10 binary operations. Then wrap this in [binary_operation_value_eq] *) 2296 2297 2298 (* Commutation result for binary operators. *) 2299 lemma binary_operation_value_eq : 2300 ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2. 2301 value_eq E v1 v2 → 2302 value_eq E v1' v2' → 2303 memory_inj E m1 m2 → 2304 ∀r1. 2305 sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 → 2306 ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2. 2307 #E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1 2308 cases op 2309 whd in match (sem_binary_operation ??????); 2310 whd in match (sem_binary_operation ??????); 2311 @cthulhu 2312 qed. 2313 2314 2315 (* Simulation relation on expressions *) 2316 lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext. 2317 ∀E:embedding. 2318 ∀Hext:memory_ext E m1 m2. 2319 switch_removal_globals E ? fundef_switch_removal ge ge' → 2320 disjoint_extension en1 m1 en2 m2 ext E Hext → 2321 ext_fresh_for_genv ext ge → 2322 (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧ 2323 (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)). 2324 #ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv 2325 @expr_lvalue_ind_combined 2326 [ 1: #csz #cty #i #a1 2327 whd in match (exec_expr ????); elim cty 2328 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2329 normalize nodelta 2330 [ 2: cases (eq_intsize csz sz) normalize nodelta 2331 [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/ 2332 | 2: #Habsurd destruct (Habsurd) ] 2333 | 4,5,6: #_ #H destruct (H) 2334 | *: #H destruct (H) ] 2335 | 2: #ty #fl #a1 2336 whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/ 2337 | 3: * 2338 [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 2339 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] 2340 #ty whd in ⊢ (% → ?); #Hind try @I 2341 whd in match (Plvalue ???); 2342 [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1 2343 cases (exec_lvalue' ge en1 m1 ? ty) in Hind; 2344 [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2345 | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 * 2346 elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2 2347 #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq 2348 whd in match (load_value_of_type' ???); 2349 whd in match (load_value_of_type' ???); 2350 lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq) 2351 cases (load_value_of_type ty m1 bl1 o1) 2352 [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2353 | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq) 2354 elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload 2355 normalize /4 by ex_intro, conj/ 2356 ] ] ] 2357 | 4: #v #ty whd * * #b1 #o1 #tr1 2358 whd in match (exec_lvalue' ?????); 2359 whd in match (exec_lvalue' ?????); 2360 lapply (Hdisjoint v) 2361 lapply (Hext_fresh_for_genv v) 2362 cases (mem_assoc_env v ext) #Hglobal 2363 [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1 2364 >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?); 2365 >(Hglobal (refl ??)) normalize 2366 #Habsurd destruct (Habsurd) 2367 | 2: normalize nodelta 2368 cases (lookup ?? en1 v) normalize nodelta 2369 [ 1: #Hlookup2 >Hlookup2 normalize nodelta 2370 lapply (rg_find_symbol … Hrelated v) 2371 cases (find_symbol ???) normalize 2372 [ 1: #_ #Habsurd destruct (Habsurd) 2373 | 2: #block cases (lookup ?? (symbols clight_fundef ge') v) 2374 [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse) 2375 | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq) 2376 %{〈block',mk_offset OZ,[]〉} @conj try @refl 2377 normalize /2/ 2378 ] ] 2379 | 2: #block 2380 cases (lookup ?? en2 v) normalize nodelta 2381 [ 1: #Hfalse @(False_ind … Hfalse) 2382 | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq) 2383 %{〈b, zero_offset, E0〉} @conj try @refl 2384 normalize /2/ 2385 ] ] ] 2386 | 5: #e #ty whd in ⊢ (% → %); 2387 whd in match (exec_lvalue' ?????); 2388 whd in match (exec_lvalue' ?????); 2389 cases (exec_expr ge en1 m1 e) 2390 [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta 2391 * elim v1 normalize nodelta 2392 [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd) 2393 | 2: #sz #i #_ #_ #a1 #Habsurd destruct (Habsurd) 2394 | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd) 2395 | 4: #_ #_ #a1 #Habsurd destruct (Habsurd) 2396 | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq 2397 >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2 2398 #Hvalue_eq normalize 2399 cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 2400 * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace) 2401 * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize 2402 %{〈b2,mk_offset (offv o1'+offv o2'),tr1''〉} @conj try @refl 2403 normalize @conj // ] 2404 | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ] 2405 | 6: #ty #e #ty' 2406 #Hsim @(exec_lvalue_expr_elim … Hsim) 2407 cases ty 2408 [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 2409 * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/ 2410 #tr #H @conj try @refl try assumption 2411 | 7: #ty #op #e 2412 #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq 2413 lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq) 2414 cases (sem_unary_operation op v1 (typeof e)) normalize nodelta 2415 [ 1: #_ @I 2416 | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq 2417 normalize /2/ ] 2418 | *: @cthulhu ] qed. 2419 2420 (* TODO: Old cases, to be ported to memory injection. 2421 | 8: #ty #op #e1 #e2 #Hind1 #Hind2 2422 whd in match (exec_expr ge ???); 2423 whd in match (exec_expr ge' ???); 2424 @(exec_expr_expr_elim … Hind1) 2425 cases (exec_expr ge en1 m1 e2) in Hind2; 2426 [ 2: #error normalize // 2427 | 1: * #v1 #tr1 normalize in ⊢ (% → ?); #Hind2 elim (Hind2 〈v1,tr1〉 (refl ??)) * #v2 #tr2 * 2428 #Hexec_eq * #Hvalue_eq #Htrace_eq #v1' #v2' #trace #Hvalue_eq' 2429 >Hexec_eq whd in match (m_bind ?????); whd in match (m_bind ?????); 2430 2431 2432 | 9: #ty #castty #e #Hind 2433 whd in match (exec_expr ge ???); 2434 whd in match (exec_expr ge' ???); 2435 cases Hind 2436 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2437 | 1: cases (exec_expr ge en m e) 2438 [ 2: #error #_ @SimFail /2 by ex_intro/ 2439 | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk // 2440 ] 2441 ] 2442 | 10: #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 2443 whd in match (exec_expr ge ???); 2444 whd in match (exec_expr ge' ???); 2445 cases Hind1 2446 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2447 | 1: cases (exec_expr ge en m e1) 2448 [ 2: #error #_ @SimFail /2 by ex_intro/ 2449 | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1))) 2450 normalize nodelta 2451 cases (exec_bool_of_val ??) 2452 [ 2: #error @SimFail /2 by ex_intro/ 2453 | 1: * whd in match (m_bind ?????); normalize nodelta 2454 [ 1: cases Hind2 2455 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2456 | 1: cases (exec_expr ge en m e2) 2457 [ 2: #error #_ @SimFail /2 by ex_intro/ 2458 | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2))) 2459 @SimOk normalize nodelta #a2 2460 whd in match (m_bind ?????); // ] 2461 ] 2462 | 2: cases Hind3 2463 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2464 | 1: cases (exec_expr ge en m e3) 2465 [ 2: #error #_ @SimFail /2 by ex_intro/ 2466 | 1: #a3 #Hind3 >(Hind3 a3 (refl ? (OK ? a3))) 2467 @SimOk normalize nodelta #a3 2468 whd in match (m_bind ?????); // ] 2469 ] 2470 ] ] ] ] 2471 | 11: #ty #e1 #e2 #Hind1 #Hind2 2472 whd in match (exec_expr ge ???); 2473 whd in match (exec_expr ge' ???); 2474 cases Hind1 2475 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2476 | 1: cases (exec_expr ge en m e1) 2477 [ 2: #error #_ @SimFail /2 by ex_intro/ 2478 | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1))) 2479 normalize nodelta 2480 cases (exec_bool_of_val ??) 2481 [ 2: #error @SimFail /2 by ex_intro/ 2482 | 1: * whd in match (m_bind ?????); 2483 [ 2: @SimOk // ] 2484 cases Hind2 2485 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2486 | 1: cases (exec_expr ge en m e2) 2487 [ 2: #error #_ @SimFail /2 by ex_intro/ 2488 | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2))) 2489 @SimOk #a2 2490 whd in match (m_bind ?????); // 2491 ] ] ] ] ] 2492 | 12: #ty #e1 #e2 #Hind1 #Hind2 2493 whd in match (exec_expr ge ???); 2494 whd in match (exec_expr ge' ???); 2495 cases Hind1 2496 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2497 | 1: cases (exec_expr ge en m e1) 2498 [ 2: #error #_ @SimFail /2 by ex_intro/ 2499 | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1))) 2500 normalize nodelta 2501 cases (exec_bool_of_val ??) 2502 [ 2: #error @SimFail /2 by ex_intro/ 2503 | 1: * whd in match (m_bind ?????); 2504 [ 1: @SimOk // ] 2505 cases Hind2 2506 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2507 | 1: cases (exec_expr ge en m e2) 2508 [ 2: #error #_ @SimFail /2 by ex_intro/ 2509 | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2))) 2510 @SimOk #a2 2511 whd in match (m_bind ?????); // 2512 ] ] ] ] ] 2513 | 13: #ty #sizeof_ty 2514 whd in match (exec_expr ge ???); 2515 whd in match (exec_expr ge' ???); 2516 @SimOk // 2517 | 14: #ty #e #ty' #fld #Hind 2518 whd in match (exec_lvalue' ge ????); 2519 whd in match (exec_lvalue' ge' ????); 2520 whd in match (typeof ?); 2521 cases ty' in Hind; 2522 [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain 2523 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ] 2524 normalize nodelta #Hind 2525 try (@SimFail /2 by ex_intro/) 2526 whd in match (exec_lvalue ????); 2527 whd in match (exec_lvalue ????); 2528 cases Hind 2529 [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2530 | 1,3: cases (exec_lvalue' ge en m e ?) 2531 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 2532 | 1,3: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk // 2533 ] ] 2534 | 15: #ty #l #e #Hind 2535 whd in match (exec_expr ge ???); 2536 whd in match (exec_expr ge' ???); 2537 cases Hind 2538 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2539 | 1: cases (exec_expr ge en m e) 2540 [ 2: #error #_ @SimFail /2 by ex_intro/ 2541 | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk // 2542 ] ] 2543 | 16: * 2544 [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 2545 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] 2546 #ty normalize in ⊢ (% → ?); 2547 [ 1,2: #_ @SimOk #a normalize // 2548 | 3,4,13: #H @(False_ind … H) 2549 | *: #_ @SimFail /2 by ex_intro/ 2550 ] 2551 ] qed. *) 2552 2553 (* 2554 lemma related_globals_exprlist_simulation : ∀ge,ge',en,m. 2555 related_globals ? fundef_switch_removal ge ge' → 2556 ∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args). 2557 #ge #ge' #en #m #Hrelated #args 2558 elim args 2559 [ 1: /3/ 2560 | 2: #hd #tl #Hind normalize 2561 elim (sim_related_globals ge ge' en m Hrelated) 2562 #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd) 2563 cases (exec_expr ge en m hd) 2564 [ 2: #error #_ @SimFail /2 by refl, ex_intro/ 2565 | 1: * #val_hd #trace_hd normalize nodelta 2566 cases Hind 2567 [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/ 2568 | 1: cases (exec_exprlist ge en m tl) 2569 [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/ 2570 | 1: * #values #trace #H >(H 〈values, trace〉 (refl ??)) 2571 normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H2 2572 cases Hexec_hd 2573 [ 2: * #error #Habsurd destruct (Habsurd) 2574 | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ] 2575 ] ] ] ] qed. 2576 *) 2577 2578 (* The return type of any function is invariant under switch removal *) 2579 lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f. 2580 #f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl 2581 qed. 2582 2583 (* Similar stuff for fundefs *) 2584 lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd). 2585 * // qed. 2586 2587 (* 815 2588 lemma expr_fresh_lift : 816 2589 ∀e,u,id. … … 828 2601 cases (leb p p') normalize nodelta 829 2602 [ 1: @H2 | 2: @H1 ] 830 qed. 831 2603 qed. *) 832 2604 833 2605 lemma while_fresh_lift : ∀e,s,u. 834 2606 fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u. 835 #e #s #u normalize #Hfresh_expr 836 elim (max_of_statement s (an_identifier SymbolTag one)) #p 837 #Hfresh_p 838 @expr_fresh_lift 839 [ 2: // 840 | 1: @Hfresh_expr ] 841 qed. 842 843 (* 844 theorem switch_removal_correction : ∀ge, ge', u. 845 related_globals ? (λclfd.\fst (fundef_switch_removal clfd u)) ge ge' → 846 ∀s1, s1', tr, s2. 2607 #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??)); 2608 cases (max_of_expr e) #e cases (max_of_statement s) #s normalize 2609 cases (leb e s) try /2/ 2610 qed. 2611 2612 (* 2613 lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0). 2614 #e0 #s0 #us0 normalize 2615 cases (switch_removal s0 us0) * #body #newvars #u' normalize // 2616 qed.*) 2617 2618 lemma dowhile_fresh_lift : ∀e,s,u. 2619 fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u. 2620 #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??)); 2621 cases (max_of_expr e) #e cases (max_of_statement s) #s normalize 2622 cases (leb e s) try /2/ 2623 qed. 2624 (* 2625 lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0). 2626 #e0 #s0 #us0 normalize 2627 cases (switch_removal s0 us0) * #body #newvars #u' normalize // 2628 qed.*) 2629 2630 lemma for_fresh_lift : ∀cond,step,body,u. 2631 fresh_for_statement step u → 2632 fresh_for_statement body u → 2633 fresh_for_expression cond u → 2634 fresh_for_statement (Sfor Sskip cond step body) u. 2635 #cond #step #body #u 2636 whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????)); 2637 cases (max_of_statement step) #s 2638 cases (max_of_statement body) #b 2639 cases (max_of_expr cond) #c 2640 whd in match (max_of_statement Sskip); 2641 >(max_id_commutative least_identifier) 2642 >max_id_one_neutral normalize nodelta 2643 normalize elim u #u 2644 cases (leb s b) cases (leb c b) cases (leb c s) try /2/ 2645 qed. 2646 2647 (* 2648 lemma for_commute : ∀e,stm1,stm2,u,uA. 2649 (uA=\snd (switch_removal stm1 u)) → 2650 sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)). 2651 #e #stm1 #stm2 #u #uA #HuA 2652 whd in match (sw_rem (Sfor ????) u); 2653 whd in match (switch_removal ??); 2654 destruct 2655 normalize in match (\snd (switch_removal Sskip u)); 2656 whd in match (sw_rem stm1 u); 2657 cases (switch_removal stm1 u) 2658 * #stm1' #fresh_vars #uA normalize nodelta 2659 whd in match (sw_rem stm2 uA); 2660 cases (switch_removal stm2 uA) 2661 * #stm2' #fresh_vars2 #uB normalize nodelta 2662 // 2663 qed.*) 2664 2665 (* 2666 lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf. 2667 * 2668 [ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip)) 2669 | 2: #e1 #e2 #u #_ 2670 whd in match (sw_rem ??); 2671 whd in match (is_Sskip ?); 2672 try /2 by refl, ex_intro/ 2673 | 3: #ret #f #args #u 2674 whd in match (sw_rem ??); 2675 whd in match (is_Sskip ?); 2676 try /2 by refl, ex_intro/ 2677 | 4: #s1 #s2 #u 2678 whd in match (sw_rem ??); 2679 whd in match (switch_removal ??); 2680 cases (switch_removal ? ?) * #a #b #c #d normalize nodelta 2681 cases (switch_removal ? ?) * #e #f #g normalize nodelta 2682 whd in match (is_Sskip ?); 2683 try /2 by refl, ex_intro/ 2684 | 5: #e #s1 #s2 #u #_ 2685 whd in match (sw_rem ??); 2686 whd in match (switch_removal ??); 2687 cases (switch_removal ? ?) * #a #b #c normalize nodelta 2688 cases (switch_removal ? ?) * #e #f #h normalize nodelta 2689 whd in match (is_Sskip ?); 2690 try /2 by refl, ex_intro/ 2691 | 6,7: #e #s #u #_ 2692 whd in match (sw_rem ??); 2693 whd in match (switch_removal ??); 2694 cases (switch_removal ? ?) * #a #b #c normalize nodelta 2695 whd in match (is_Sskip ?); 2696 try /2 by refl, ex_intro/ 2697 | 8: #s1 #e #s2 #s3 #u #_ 2698 whd in match (sw_rem ??); 2699 whd in match (switch_removal ??); 2700 cases (switch_removal ? ?) * #a #b #c normalize nodelta 2701 cases (switch_removal ? ?) * #e #f #g normalize nodelta 2702 cases (switch_removal ? ?) * #i #j #k normalize nodelta 2703 whd in match (is_Sskip ?); 2704 try /2 by refl, ex_intro/ 2705 | 9,10: #u #_ 2706 whd in match (is_Sskip ?); 2707 try /2 by refl, ex_intro/ 2708 | 11: #e #u #_ 2709 whd in match (is_Sskip ?); 2710 try /2 by refl, ex_intro/ 2711 | 12: #e #ls #u #_ 2712 whd in match (sw_rem ??); 2713 whd in match (switch_removal ??); 2714 cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta 2715 cases (fresh ??) #e #f normalize nodelta 2716 normalize in match (simplify_switch ???); 2717 cases (fresh ? f) #g #h normalize nodelta 2718 cases (produce_cond ????) * #k #l #m normalize nodelta 2719 whd in match (is_Sskip ?); 2720 try /2 by refl, ex_intro/ 2721 | 13,15: #lab #st #u #_ 2722 whd in match (sw_rem ??); 2723 whd in match (switch_removal ??); 2724 cases (switch_removal ? ?) * #a #b #c normalize nodelta 2725 whd in match (is_Sskip ?); 2726 try /2 by refl, ex_intro/ 2727 | 14: #lab #u 2728 whd in match (is_Sskip ?); 2729 try /2 by refl, ex_intro/ ] 2730 qed. 2731 *) 2732 2733 (* 2734 lemma sw_rem_commute : ∀stm,u. 2735 (\fst (\fst (switch_removal stm u))) = sw_rem stm u. 2736 #stm #u whd in match (sw_rem stm u); // qed. 2737 *) 2738 2739 lemma fresh_for_statement_inv : 2740 ∀u,s. fresh_for_statement s u → 2741 match u with 2742 [ mk_universe p ⇒ le (p0 one) p ]. 2743 * #p #s whd in match (fresh_for_statement ??); 2744 cases (max_of_statement s) #s 2745 normalize /2/ qed. 2746 2747 lemma fresh_for_Sskip : 2748 ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u. 2749 #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. 2750 2751 lemma fresh_for_Sbreak : 2752 ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u. 2753 #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. 2754 2755 lemma fresh_for_Scontinue : 2756 ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u. 2757 #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. 2758 2759 (* 2760 lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉. 2761 #s #u elim (switch_removal s u) * #res #fvs #u' 2762 %{res} %{fvs} %{u'} // 2763 qed. 2764 2765 lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉. 2766 #switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u' 2767 %{res} %{fvs} %{u'} // 2768 qed. 2769 *) 2770 2771 lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉. 2772 #e #ls #u #exit_label cases (produce_cond e ls u exit_label) * 2773 #s #lab #u' %{s} %{lab} %{u'} // 2774 qed. 2775 2776 (* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *) 2777 lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false. 2778 * * * 2779 [ 1,5,9: #H @(False_ind … (H (refl ??))) 2780 | *: #_ normalize @refl ] 2781 qed. 2782 2783 lemma exec_expr_int : ∀ge,e,m,expr. 2784 (∃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〉)). 2785 #ge #e #m #expr cases (exec_expr ge e m expr) 2786 [ 2: #error %2 #sz #n #tr % #H destruct (H) 2787 | 1: * #val #trace cases val 2788 [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl 2789 | 3: #fl | 4: | 5: #ptr ] 2790 %2 #sz #n #tr % #H destruct (H) 2791 ] qed. 2792 2793 (* 2794 lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr. 2795 exec_expr ge e m cond = OK ? 〈v,tr〉 → 2796 (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) → 2797 exec_expr ge' e m cond = OK ? 〈v,tr〉. 2798 #ge #ge' #e #m #cond #v #tr #H * 2799 [ 1: #Hsim >(Hsim ? H) // 2800 | 2: * #error >H #Habsurd destruct (Habsurd) ] 2801 qed. *) 2802 2803 (* 2804 lemma switch_simulation : 2805 ∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u. 2806 switch_cont_sim k k' → 2807 (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) → 2808 fresh_for_statement (Sswitch cond switchcases) u → 2809 ∃tr'. 2810 (eventually ge' 2811 (λs2':state 2812 .switch_state_sim 2813 (State f 2814 (seq_of_labeled_statement (select_switch condsz condval switchcases)) 2815 (Kswitch k) e m) s2') 2816 (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m) 2817 tr'). 2818 #ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh 2819 whd in match (sw_rem (Sswitch cond switchcases) u); 2820 whd in match (switch_removal (Sswitch cond switchcases) u); 2821 cases switchcases in Hfresh; 2822 [ 1: #default_statement #Hfresh_for_default 2823 whd in match (switch_removal_branches ??); 2824 whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?); 2825 elim (switch_removal_eq default_statement u) 2826 #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq 2827 normalize nodelta 2828 cut (u' = (\snd (switch_removal default_statement u))) 2829 [ 1: >Hdefault_statement_eq // ] #Heq_u' 2830 cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u') 2831 [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u' 2832 lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u') 2833 #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉)) 2834 -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *) 2835 normalize nodelta 2836 whd in match (simplify_switch (Expr ??) ?? uv2); 2837 lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2) 2838 #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉)) 2839 -Hfreshness #Heq_uv3 2840 normalize nodelta whd in match (add_starting_lbl_list ????); 2841 lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3) 2842 #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉)) 2843 -Hfreshness #Heq_uv4 2844 normalize nodelta 2845 @(eventually_later ge' ?? E0) 2846 whd in match (exec_step ??); 2847 %{(State (function_switch_removal f) 2848 (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond) 2849 (Kseq 2850 (Ssequence 2851 (Slabel default_lab (convert_break_to_goto default_statement' exit_label)) 2852 (Slabel exit_label Sskip)) 2853 k') e m)} @conj try // 2854 @(eventually_later ge' ?? E0) 2855 whd in match (exec_step ??); 2856 2857 @chthulhu | @chthulhu 2858 qed. *) 2859 2860 2861 2862 (* Main theorem. To be ported and completed to memory injections. TODO *) 2863 (* 2864 theorem switch_removal_correction : ∀ge, ge'. 2865 related_globals ? fundef_switch_removal ge ge' → 2866 ∀s1, s1', tr, s2. 847 2867 switch_state_sim s1 s1' → 848 2868 exec_step ge s1 = Value … 〈tr,s2〉 → 849 2869 eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr. 850 #ge #ge' # u #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step2870 #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step 851 2871 inversion Hsim_state 852 2872 [ 1: (* regular state *) 853 #uf #us #uk #f #s #k #k' #e #m #Huf_fresh #Hus_fresh #Huk_fresh #Hsim_cont #Hs1_eq #Hs1_eq' #_ 2873 #u #f #s #k #k' #m #m' #result #en #en' #f' #vars 2874 #Hu_fresh #Hen_eq #Hf_eq #Hen_eq' #Hswitch_removal #Hsim_cont #Hs1_eq #Hs1_eq' #_ 2875 2876 lapply (sim_related_globals ge ge' e m Hrelated) * 2877 #Hexpr_related #Hlvalue_related 854 2878 >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?); 855 cases s in Hus_fresh; 2879 cases s in Hu_fresh Heq_env; 2880 2881 2882 theorem switch_removal_correction : ∀ge, ge'. 2883 related_globals ? fundef_switch_removal ge ge' → 2884 ∀s1, s1', tr, s2. 2885 switch_state_sim s1 s1' → 2886 exec_step ge s1 = Value … 〈tr,s2〉 → 2887 eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr. 2888 #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step 2889 inversion Hsim_state 2890 [ 1: (* regular state *) 2891 #u #f #s #k #k' #e #e' #m #m' #Hu_fresh #Heq_env #Hsim_cont #Hs1_eq #Hs1_eq' #_ 2892 lapply (sim_related_globals ge ge' e m Hrelated) * 2893 #Hexpr_related #Hlvalue_related 2894 >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?); 2895 cases s in Hu_fresh Heq_env; 856 2896 (* Perform the intros for the statements*) 857 [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body2897 [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body 858 2898 | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body 859 2899 | 14: #lab | 15: #cost #body ] 860 #Hu s_fresh2900 #Hu_fresh #Heq_env 861 2901 [ 1: (* Skip *) 862 2902 whd in match (sw_rem ??); 863 2903 inversion Hsim_cont normalize nodelta 864 2904 [ 1: #Hk #Hk' #_ #Hexec_step 865 @(eventually_base … (Returnstate Vundef Kstop (free_list m (blocks_of_env e)))) 866 [ 1: whd in match (exec_step ??); >fn_return_simplify ] 2905 @(eventually_now ????) whd in match (exec_step ??); >fn_return_simplify 867 2906 cases (fn_return f) in Hexec_step; 868 2907 [ 1,10: | 2,11: #sz #sg | 3,12: #fsz | 4,13: #rg #ptr_ty | 5,14: #rg #array_ty #array_sz | 6,15: #domain #codomain 869 2908 | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ] 870 2909 normalize nodelta 871 [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H) // %3 destruct // 2910 [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H) 2911 %{(Returnstate Vundef Kstop (free_list m' (blocks_of_env e')))} @conj try // 2912 normalize in Heq_env; destruct (Heq_env) 2913 %3 // 2914 (* cut (blocks_of_env e = blocks_of_env e') 2915 [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl; 2916 lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ] 2917 #Heq >Heq %3 // *) 872 2918 | *: #H destruct (H) ] 873 | 2: #s0 #k0 #k0' #us 0 #Hus0_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq2919 | 2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq 874 2920 whd in match (ret ??) in Heq; destruct (Heq) 875 2921 @(eventually_now ????) whd in match (exec_step ??); 876 %{(State (\fst (function_switch_removal f uf)) (sw_rem s0 us0) k0' e m)} @conj try // 877 %1{uf us0 uk} // 878 >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); >Hk' 879 whd in ⊢ (% → ?); * #_ // 880 | 3: #e0 #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq 2922 %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try // 2923 %1 try // 2924 | 3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq 881 2925 @(eventually_now ????) whd in match (exec_step ??); 882 2926 whd in match (ret ??) in Heq; destruct (Heq) 883 %{(State (\fst (function_switch_removal f uf)) (Swhile e0 (sw_rem s0 us0)) k0' e m)} @conj try // 884 >while_commute %1{uf us0 uk} // 885 [ 1: @while_fresh_lift assumption 886 | 2: >Hk' in Huk_fresh; whd in ⊢ (% → ?); * #_ // ] 887 | 4: #eO #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq 2927 %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try // 2928 >while_commute %1 try // 2929 | 4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq 888 2930 @(eventually_now ????) whd in match (exec_step ??); 889 890 891 892 [ 1: @uk 893 | 2: >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); * * // ] 894 895 whd 896 normalize 897 898 cut (Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0)) 899 [ 1: whd in match (sw_rem (Swhile ??) ?); 900 whd in match (switch_removal ??); 901 whd in match (exec_step ??); 902 903 (* foireux pour le (Expr (Econst_int sz n) ?) *) 904 lemma convert : 905 ∀uv. 906 ∀sz,n,sl. 907 seq_of_labeled_statements (select_switch sz n sl) 908 ~~~u 909 let 〈exit_label, uv1〉 ≝ fresh ? uv in 910 let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list sl ? uv1 [ ] in 911 Ssequence (pi1 … (produce_cond2 (Expr (Econst_int sz n)) sl defcase exit_label)) (Slabel exit_label Sskip) 912 913 914 lemma convert : 915 ∀f,cond,ls,k,ge,e,m. 916 ∀t. 917 ∀sz,n. exec_step ge (State f (Sswitch cond ls) k e m) = Value ??? 〈t,State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m〉 → 918 ∀uf,us. 919 fresh_for_function f uf → 920 fresh_for_statement (Sswitch cond ls) us → 921 ∃s',k'. 922 (exec_plus ge 923 E0 (State (\fst (function_switch_removal f uf)) (sw_rem (Sswitch cond ls) us) k' e m) 924 t s') 925 ∧ switch_cont_sim k k' 926 ∧ switch_state_sim 927 (State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m) 928 s'. 929 #f #cond #ls #k #ge #e #m #t #sz #n #Hexec #uf #us #Huf #Hus 930 whd in match (sw_rem ??); 931 whd in match (switch_removal ??); 932 check eq_ind 933 934 935 936 whd in Hexec:(??%?); cases (exec_expr ge e m cond) in Hexec; 937 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) ] 938 * #cond_val #cond_trace 939 whd in match (bindIO ??????); 940 cases cond_val 941 [ 1: | 2: #sz' #n' | 3: #fl | 4: #rg | 5: #ptr ] 942 [ 1,3,4,5: #Habsurd normalize in Habsurd; destruct (Habsurd) ] 943 normalize nodelta #Heq whd in match (ret ??) in Heq; 944 945 946 947 948 ! 〈v,tr〉 ← exec_expr ge e m a : IO ???; 949 match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉 950 | _ ⇒ Wrong ??? (msg TypeMismatch) ] 951 952 theorem step_with_labels : ∀ge,ge'. 953 related_globals ? label_fundef ge ge' → 954 state_with_labels s1 s1' → 955 exec_expr ge en m e = OK ? 〈Vint sz v, tr〉 → 956 (seq_of_labeled_statement (select_switch sz n sl) ~ simplify_switch 957 (exec_step ge st (Sswitch e ls) 2931 lapply (Hexpr_related e0) 2932 cases (exec_expr ge e m e0) in Heq; 2933 [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2934 | 1: * #b #tr whd in match (m_bind ?????); #Heq 2935 * 2936 [ 2: * #error #Habsurd destruct (Habsurd) 2937 | 1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉))) 2938 whd in match (bindIO ??????); 2939 cases (exec_bool_of_val b (typeof e0)) in Heq; 2940 [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 2941 | 1: * whd in match (bindIO ??????); #Heq destruct (Heq) 2942 whd in match (bindIO ??????); 2943 [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)} 2944 @conj // >dowhile_commute %1 try // 2945 | 2: %{(State (function_switch_removal f) Sskip k0' e m)} 2946 @conj // %1{us} try // 2947 @(fresh_for_Sskip … Hus_fresh) 2948 ] ] ] ] 2949 | 5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq 2950 @(eventually_now ????) whd in match (exec_step ??); 2951 whd in match (ret ??) in Heq; destruct 2952 %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)} 2953 @conj try // %1{u} try // 2954 | 6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq 2955 @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq; 2956 destruct (Heq) 2957 %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)} 2958 @conj try // %1 2959 [ 2: @swc_for3 // 2960 | 1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ] 2961 | 7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq 2962 @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq; 2963 destruct (Heq) 2964 %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)} 2965 @conj try // <(for_commute ??? u uA) try // %1 2966 [ 2: assumption 2967 | 1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ] 2968 | 8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?); 2969 #Heq @(eventually_now ????) whd in match (exec_step ??); 2970 destruct (Heq) 2971 %{(State (function_switch_removal f) Sskip k0' e m)} @conj // 2972 %1{u} // 2973 | 9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq 2974 @(eventually_now ????) whd in match (exec_step ??); 2975 >fn_return_simplify cases (fn_return f) in Heq; 2976 [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain 2977 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ] 2978 normalize nodelta 2979 [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H) 2980 %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))} 2981 @conj try // %3 destruct // 2982 | *: #H destruct (H) ] 2983 ] 2984 | 2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????) 2985 whd in match (exec_step ??); 2986 cases lhs in Hu_fresh Heq; #lhs #lhs_type 2987 cases (Hlvalue_related lhs lhs_type) 2988 whd in match (exec_lvalue ge e m (Expr ??)); 2989 whd in match (exec_lvalue ge' e m (Expr ??)); 2990 [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ] 2991 cases (exec_lvalue' ge e m lhs lhs_type) 2992 [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd) 2993 | 1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??)) 2994 whd in match (m_bind ?????); 2995 cases (Hexpr_related rhs) 2996 [ 2: * #error #Hfail >Hfail #_ 2997 whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 2998 | 1: cases (exec_expr ge e m rhs) 2999 [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd) 3000 | 1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??)) 3001 whd in match (bindIO ??????) in ⊢ (% → % → %); 3002 cases (opt_to_io io_out io_in ???) 3003 [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd) 3004 | 3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 3005 | 2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq) 3006 %{(State (function_switch_removal f) Sskip k' e mem)} 3007 whd in match (bindIO ??????); @conj // 3008 %1{u} try // @(fresh_for_Sskip … Hfresh) 3009 ] ] ] ] 3010 | 3: (* Scall *) normalize nodelta #Heq @(eventually_now ????) 3011 whd in match (exec_step ??); 3012 cases (Hexpr_related func) in Heq; 3013 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 3014 | 1: cases (exec_expr ge e m func) 3015 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 3016 | 1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??)) 3017 whd in match (m_bind ?????); normalize nodelta 3018 lapply (related_globals_exprlist_simulation ge ge' e m Hrelated) 3019 #Hexprlist_sim cases (Hexprlist_sim args) 3020 [ 2: * #error #Hfail >Hfail 3021 whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 3022 | 1: cases (exec_exprlist ge e m args) 3023 [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 3024 | 1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??)) 3025 whd in match (bindIO ??????) in ⊢ (% → %); 3026 elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval) 3027 cases (find_funct clight_fundef ge fval) 3028 [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??)) 3029 whd in match (bindIO ??????) in ⊢ (% → %); 3030 >fundef_type_simplify 3031 cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func)) 3032 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 3033 | 1: #Heq whd in match (bindIO ??????) in ⊢ (% → %); 3034 cases retv normalize nodelta 3035 [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct 3036 %{(Callstate (fundef_switch_removal clfd) values 3037 (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)} 3038 @conj try // %2 try // @swc_call // 3039 | 2: * #retval_ed #retval_type 3040 whd in match (exec_lvalue ge ???); 3041 whd in match (exec_lvalue ge' ???); 3042 elim (Hlvalue_related retval_ed retval_type) 3043 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 3044 | 1: cases (exec_lvalue' ge e m retval_ed retval_type) 3045 [ 2: #error #_ whd in match (m_bind ?????); #Habsurd 3046 destruct (Habsurd) 3047 | 1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??)) 3048 whd in match (m_bind ?????) in ⊢ (% → %); 3049 #Heq destruct (Heq) 3050 %{(Callstate (fundef_switch_removal clfd) values 3051 (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉) 3052 (function_switch_removal f) e k') m)} 3053 @conj try // 3054 %2 @swc_call // 3055 ] ] ] ] 3056 | 1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %); 3057 whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 3058 ] ] ] ] ] 3059 | 4: (* Ssequence *) normalize nodelta 3060 whd in match (ret ??) in ⊢ (% → ?); #Heq 3061 @(eventually_now ????) 3062 %{(State (function_switch_removal f) 3063 (\fst (\fst (switch_removal stm1 u))) 3064 (Kseq (\fst (\fst (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)} 3065 @conj 3066 [ 2: destruct (Heq) %1 3067 [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // 3068 | 2: @swc_seq try // @switch_removal_fresh 3069 elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ] 3070 | 1: whd in match (sw_rem ??); whd in match (switch_removal ??); 3071 cases (switch_removal stm1 u) 3072 * #stm1' #fresh_vars #u' normalize nodelta 3073 cases (switch_removal stm2 u') 3074 * #stm2' #fresh_vars2 #u'' normalize nodelta 3075 whd in match (exec_step ??); 3076 destruct (Heq) @refl 3077 ] 3078 | 5: (* If-then-else *) normalize nodelta 3079 whd in match (ret ??) in ⊢ (% → ?); #Heq 3080 @(eventually_now ????) whd in match (sw_rem ??); 3081 whd in match (switch_removal ??); 3082 elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta 3083 elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta 3084 whd in match (exec_step ??); 3085 cases (Hexpr_related cond) in Heq; 3086 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 3087 | 1: cases (exec_expr ge e m cond) 3088 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 3089 | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??)) 3090 whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %); 3091 cases (exec_bool_of_val condval (typeof cond)) 3092 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 3093 | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval 3094 destruct (Heq_condval) whd in match (bindIO ??????); 3095 normalize nodelta 3096 [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try // 3097 cut (iftrue' = (\fst (\fst (switch_removal iftrue u)))) 3098 [ 1: >Hiftrue_eq normalize // ] 3099 #Hrewrite >Hrewrite %1 3100 elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) // 3101 | 2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try // 3102 cut (iffalse' = (\fst (\fst (switch_removal iffalse uA)))) 3103 [ 1: >Hiffalse_eq // ] 3104 #Hrewrite >Hrewrite %1 try // 3105 cut (uA = (\snd (switch_removal iftrue u))) 3106 [ 1: >Hiftrue_eq // 3107 | 2: #Heq_uA >Heq_uA 3108 elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) 3109 #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh // 3110 ] ] ] ] ] 3111 | 6: (* While loop *) normalize nodelta 3112 whd in match (ret ??) in ⊢ (% → ?); #Heq 3113 @(eventually_now ????) whd in match (sw_rem ??); 3114 whd in match (switch_removal ??); 3115 elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta 3116 whd in match (exec_step ??); 3117 cases (Hexpr_related cond) in Heq; 3118 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 3119 | 1: cases (exec_expr ge e m cond) 3120 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 3121 | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??)) 3122 whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %); 3123 cases (exec_bool_of_val condval (typeof cond)) 3124 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 3125 | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval 3126 destruct (Heq_condval) whd in match (bindIO ??????); 3127 normalize nodelta 3128 [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try // 3129 cut (body' = (\fst (\fst (switch_removal body u)))) 3130 [ 1: >Hbody_eq // ] 3131 #Hrewrite >Hrewrite %1 3132 [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) // 3133 | 2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ] 3134 | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj // 3135 %1{u} try // @(fresh_for_Sskip … Hu_fresh) 3136 ] ] ] ] 3137 | 7: (* Dowhile loop *) normalize nodelta 3138 whd in match (ret ??) in ⊢ (% → ?); #Heq 3139 @(eventually_now ????) whd in match (sw_rem ??); 3140 whd in match (switch_removal ??); 3141 elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta 3142 whd in match (exec_step ??); 3143 destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj 3144 try // 3145 cut (body' = (\fst (\fst (switch_removal body u)))) 3146 [ 1: >Hbody_eq // ] 3147 #Hrewrite >Hrewrite %1 3148 [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) // 3149 | 2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ] 3150 | 8: (* For loop *) normalize nodelta 3151 whd in match (ret ??) in ⊢ (% → ?); #Heq 3152 @(eventually_now ????) whd in match (sw_rem ??); 3153 whd in match (switch_removal ??); 3154 cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip 3155 [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta 3156 elim (switch_removal_eq step u) #step' * #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta 3157 elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta 3158 whd in match (exec_step ??); 3159 cases (Hexpr_related cond) 3160 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 3161 | 1: cases (exec_expr ge e m cond) 3162 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 3163 | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??)) 3164 whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %); 3165 cases (exec_bool_of_val condval (typeof cond)) 3166 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 3167 | 1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval 3168 destruct (Heq_condval) 3169 [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj 3170 try // 3171 cut (body' = (\fst (\fst (switch_removal body uA)))) 3172 [ 1: >Hbody_eq // ] 3173 #Hrewrite >Hrewrite 3174 cut (uA = (\snd (switch_removal step u))) 3175 [ 1: >Hstep_eq // ] #HuA 3176 elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * * 3177 #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1 3178 [ 1: >HuA @switch_removal_fresh assumption 3179 | 2: cut (step' = (\fst (\fst (switch_removal step u)))) 3180 [ >Hstep_eq // ] 3181 #Hstep >Hstep @swc_for2 try assumption 3182 @for_fresh_lift try assumption ] 3183 | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj 3184 try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption 3185 ] ] ] ] 3186 | 2: #Heq 3187 elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta 3188 elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta 3189 elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta 3190 whd in match (exec_step ??); 3191 cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ] 3192 #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip) 3193 whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta 3194 whd in match (ret ??); destruct (Heq) 3195 %{(State (function_switch_removal f) (\fst (\fst (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)} 3196 @conj try // 3197 cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep' 3198 cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody' 3199 <for_commute [ 2: >Hstep_eq // ] 3200 elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * * 3201 #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption 3202 @swc_seq try // @for_fresh_lift 3203 cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq 3204 >HuA_eq @switch_removal_fresh assumption 3205 ] 3206 | 9: (* break *) normalize nodelta 3207 inversion Hsim_cont 3208 [ 1: #Hk #Hk' #_ 3209 | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_ 3210 | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_ 3211 | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_ 3212 | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_ 3213 | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_ 3214 | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_ 3215 | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ] 3216 normalize nodelta #H try (destruct (H)) 3217 whd in match (ret ??) in H; destruct (H) 3218 @(eventually_now ????) 3219 [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: // | 2,4: %1{u} // ] 3220 | 2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ] 3221 | 10: (* Continue *) normalize nodelta 3222 inversion Hsim_cont 3223 [ 1: #Hk #Hk' #_ 3224 | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_ 3225 | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_ 3226 | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_ 3227 | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_ 3228 | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_ 3229 | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_ 3230 | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ] 3231 normalize nodelta #H try (destruct (H)) 3232 @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H; 3233 destruct (H) 3234 [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption 3235 | 2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try // 3236 >while_commute %1{u0} try assumption 3237 | 3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H; 3238 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 3239 | 1: * #condval #trace whd in match (m_bind ?????); 3240 #Heq * 3241 [ 2: * #error #Habsurd destruct (Habsurd) 3242 | 1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) -Hexec #Hexec >Hexec 3243 whd in match (bindIO ??????); 3244 cases (exec_bool_of_val condval (typeof cond)) in Heq; 3245 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 3246 | 1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????); 3247 [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)} 3248 @conj try // >dowhile_commute %1{u0} assumption 3249 | 2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // 3250 %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ] 3251 ] ] ] 3252 | 4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0} 3253 try // @(fresh_for_Scontinue … Hfor_fresh) 3254 | 5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)} 3255 @conj try // %1{u0} 3256 elim (substatement_fresh … Hfor_fresh) * * try // 3257 #HSskip #Hcond #Hstep #Hbody 3258 @swc_for3 assumption 3259 | 6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // 3260 %1{u} try // 3261 ] 3262 | 11: (* Sreturn *) normalize nodelta #Heq 3263 @(eventually_now ????) 3264 whd in match (exec_step ??) in Heq ⊢ %; 3265 cases retval in Heq; normalize nodelta 3266 [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta 3267 whd in match (ret ??) in ⊢ (% → %); 3268 [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty' 3269 | 7: #id #fl | 8: #id #fl | 9: #rg #id ] 3270 #H destruct (H) 3271 %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))} 3272 @conj [ 1: // | 2: %3 @call_cont_swremoval // ] 3273 | 2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta 3274 [ 1: #_ #Habsurd destruct (Habsurd) 3275 | 2: #_ elim (Hexpr_related expr) 3276 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 3277 | 1: cases (exec_expr ??? expr) 3278 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 3279 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) 3280 #Hrewrite >Hrewrite 3281 whd in match (m_bind ?????); whd in match (m_bind ?????); 3282 #Heq destruct (Heq) 3283 %{(Returnstate (\fst a) (call_cont k') (free_list m (blocks_of_env e)))} 3284 @conj [ 1: // | 2: %3 @call_cont_swremoval // ] 3285 ] ] ] ] 3286 | 12: (* Sswitch. Main proof case. *) normalize nodelta 3287 (* Case analysis on the outcome of the tested expression *) 3288 cases (exec_expr_int ge e m cond) 3289 [ 2: cases (exec_expr ge e m cond) 3290 [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd) 3291 | 1: * #val #trace cases val 3292 [ 1: | 2: #condsz #condv | 3: #condf | 4: #condrg | 5: #condptr ] 3293 whd in match (m_bind ?????); 3294 [ 1,3,4,5: #_ #Habsurd destruct (Habsurd) 3295 | 2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ] ] 3296 ] 3297 * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond 3298 whd in match (m_bind ?????); #Heq 3299 destruct (Heq) 3300 @eventually_later 3301 whd in match (sw_rem (Sswitch cond switchcases) u); 3302 whd in match (switch_removal (Sswitch cond switchcases) u); 3303 elim (switch_removal_branches_eq switchcases u) 3304 #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta 3305 cut (uv1 = (\snd (switch_removal_branches switchcases u))) 3306 [ 1: >Hsrb_eq // ] #Huv1_eq 3307 cut (fresh_for_statement (Sswitch cond switchcases) uv1) 3308 [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] -Huv1_eq #Huv1_eq 3309 elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv2_eq normalize nodelta 3310 whd in match (simplify_switch ???); 3311 elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv3_eq normalize nodelta 3312 lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq) 3313 elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label) 3314 #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta 3315 #Huv4_eq 3316 whd in match (exec_step ??); 3317 %{(State (function_switch_removal f) 3318 (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond) 3319 (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)} 3320 %{E0} @conj try @refl 3321 %{tr} normalize in match (eq ???); @conj try // 3322 (* execute the conditional *) 3323 @eventually_later 3324 (* lift the result of the previous case analysis from [ge] to [ge'] *) 3325 whd in match (exec_step ??); 3326 whd in match (exec_lvalue ????); 3327 3328 >(exec_expr_related … Hexec_cond (Hexpr_related cond)) 3329 3330 *) 958 3331 959 960 ∃tr',s2'. plus ge' s1' tr' s2' ∧961 trace_with_extra_labels tr tr' ∧962 state_with_labels s2 s2').963 964 965 *)966
Note: See TracChangeset
for help on using the changeset viewer.