Changeset 2438 for src/Clight/switchRemoval.ma
- Timestamp:
- Nov 7, 2012, 11:18:56 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/switchRemoval.ma
r2391 r2438 9 9 include "basics/lists/list.ma". 10 10 include "basics/lists/listb.ma". 11 include "Clight/SimplifyCasts.ma". 12 11 13 12 14 … … 204 206 normalize @conj try @conj try @conj try @conj try // 205 207 @(convert_break_lift ?? Hsf) 206 ] qed. 208 ] qed. 207 209 208 210 (* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in 209 211 order to circumvent the associativity problems in notations. *) 212 (* 210 213 record swret (A : Type[0]) : Type[0] ≝ { 211 214 ret_st : A; 212 215 ret_acc : list (ident × type); 213 ret_fvs : list ident;214 216 ret_u : universe SymbolTag 215 217 }. 216 218 217 notation > "vbox('do' 〈ident v1, ident v2, ident v3, ident v4〉 ← e; break e')" with precedence 48 218 for @{ match ${e} with 219 [ None ⇒ None ? 220 | Some ${fresh ret} ⇒ 221 (λ${ident v1}.λ${ident v2}.λ${ident v3}.λ${ident v4}. ${e'}) 222 (ret_st ? ${fresh ret}) 223 (ret_acc ? ${fresh ret}) 224 (ret_fvs ? ${fresh ret}) 225 (ret_u ? ${fresh ret}) ] }. 226 227 notation > "vbox('ret' 〈e1, e2, e3, e4〉)" with precedence 49 228 for @{ Some ? (mk_swret ? ${e1} ${e2} ${e3} ${e4}) }. 219 notation > "vbox('let' 〈ident v1, ident v2, ident v3〉 ≝ e in break e')" with precedence 48 220 for @{ (λ${ident v1}.λ${ident v2}.λ${ident v3}. ${e'}) 221 (ret_st ? ${e}) 222 (ret_acc ? ${e}) 223 (ret_u ? ${e}) }. 224 225 definition ret ≝ λe1,e2,e3. mk_swret statement e1 e2 e3. *) 229 226 230 227 (* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list … … 234 231 let rec switch_removal 235 232 (st : statement) (* the statement in which we will remove switches *) 236 (fvs : list ident) (* a finite list of names usable to create variables. *) 237 (u : universe SymbolTag) (* a fresh /label/ generator *) 238 : option (swret statement) ≝ 233 (u : universe SymbolTag) (* a fresh label and ident generator *) 234 : statement × (list (ident × type)) × (universe SymbolTag) ≝ 239 235 match st with 240 [ Sskip ⇒ ret 〈st, [ ], fvs, u〉241 | Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉242 | Scall _ _ _ ⇒ ret 〈st, [ ], fvs, u〉236 [ Sskip ⇒ 〈st, [ ], u〉 237 | Sassign _ _ ⇒ 〈st, [ ], u〉 238 | Scall _ _ _ ⇒ 〈st, [ ], u〉 243 239 | Ssequence s1 s2 ⇒ 244 do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;245 do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';246 ret 〈Ssequence s1' s2', acc1 @ acc2, fvs'', u''〉240 let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in 241 let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in 242 〈Ssequence s1' s2', acc1 @ acc2, u''〉 247 243 | Sifthenelse e s1 s2 ⇒ 248 do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;249 do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';250 ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉244 let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in 245 let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in 246 〈Sifthenelse e s1' s2', acc1 @ acc2, u''〉 251 247 | Swhile e body ⇒ 252 do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;253 ret 〈Swhile e body', acc, fvs', u'〉248 let 〈body', acc, u'〉 ≝ switch_removal body u in 249 〈Swhile e body', acc, u'〉 254 250 | Sdowhile e body ⇒ 255 do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;256 ret 〈Sdowhile e body', acc, fvs', u'〉251 let 〈body', acc, u'〉 ≝ switch_removal body u in 252 〈Sdowhile e body', acc, u'〉 257 253 | Sfor s1 e s2 s3 ⇒ 258 do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;259 do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';260 do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u'';261 ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉254 let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in 255 let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in 256 let 〈s3', acc3, u'''〉 ≝ switch_removal s3 u'' in 257 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, u'''〉 262 258 | Sbreak ⇒ 263 ret 〈st, [ ], fvs, u〉259 〈st, [ ], u〉 264 260 | Scontinue ⇒ 265 ret 〈st, [ ], fvs, u〉261 〈st, [ ], u〉 266 262 | Sreturn _ ⇒ 267 ret 〈st, [ ], fvs, u〉263 〈st, [ ], u〉 268 264 | Sswitch e branches ⇒ 269 do 〈sf_branches, acc, fvs', u'〉 ← switch_removal_branches branches fvs u; 270 match fvs' with 271 [ nil ⇒ None ? 272 | cons fresh tl ⇒ 273 (* let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in *) 274 let ident ≝ Expr (Evar fresh) (typeof e) in 275 let assign ≝ Sassign ident e in 276 let 〈result, u''〉 ≝ simplify_switch ident sf_branches u' in 277 ret 〈Ssequence assign result, (〈fresh, typeof e〉 :: acc), tl, u'〉 278 ] 265 let 〈sf_branches, acc, u'〉 ≝ switch_removal_branches branches u in 266 let 〈switch_tmp, u''〉 ≝ fresh ? u' in 267 let ident ≝ Expr (Evar switch_tmp) (typeof e) in 268 let assign ≝ Sassign ident e in 269 let 〈result, u'''〉 ≝ simplify_switch ident sf_branches u'' in 270 〈Ssequence assign result, (〈switch_tmp, typeof e〉 :: acc), u'''〉 279 271 | Slabel label body ⇒ 280 do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;281 ret 〈Slabel label body', acc, fvs', u'〉272 let 〈body', acc, u'〉 ≝ switch_removal body u in 273 〈Slabel label body', acc, u'〉 282 274 | Sgoto _ ⇒ 283 ret 〈st, [ ], fvs, u〉275 〈st, [ ], u〉 284 276 | Scost cost body ⇒ 285 do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;286 ret 〈Scost cost body', acc, fvs', u'〉277 let 〈body', acc, u'〉 ≝ switch_removal body u in 278 〈Scost cost body', acc, u'〉 287 279 ] 288 280 289 281 and switch_removal_branches 290 282 (l : labeled_statements) 291 (fvs : list ident)292 283 (u : universe SymbolTag) 293 (* : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝284 : (labeled_statements × (list (ident × type)) × (universe SymbolTag)) ≝ 294 285 match l with 295 286 [ LSdefault st ⇒ 296 do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u;297 ret 〈LSdefault st', acc1, fvs', u'〉298 | LScase sz int st tl =>299 do 〈tl_result, acc1, fvs', u'〉 ← switch_removal_branches tl fvs u;300 do 〈st', acc2, fvs'', u''〉 ← switch_removal st fvs' u';301 ret 〈LScase sz int st' tl_result, acc1 @ acc2, fvs'', u''〉287 let 〈st', acc1, u'〉 ≝ switch_removal st u in 288 〈LSdefault st', acc1, u'〉 289 | LScase sz int st tl ⇒ 290 let 〈tl_result, acc1, u'〉 ≝ switch_removal_branches tl u in 291 let 〈st', acc2, u''〉 ≝ switch_removal st u' in 292 〈LScase sz int st' tl_result, acc1 @ acc2, u''〉 302 293 ]. 303 294 304 let rec mk_fresh_variables 305 (st : statement) (* the statement in which we will remove switches *) 306 (u : universe SymbolTag) (* a fresh /label/ generator *) 307 : (list ident) × (universe SymbolTag) ≝ 308 match st with 309 [ Sskip ⇒ 〈[ ], u〉 310 | Sassign _ _ ⇒ 〈[ ], u〉 311 | Scall _ _ _ ⇒ 〈[ ], u〉 312 | Ssequence s1 s2 ⇒ 313 let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in 314 let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in 315 〈fvs @ fvs', u''〉 316 | Sifthenelse e s1 s2 ⇒ 317 let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in 318 let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in 319 〈fvs @ fvs', u''〉 320 | Swhile e body ⇒ 321 mk_fresh_variables body u 322 | Sdowhile e body ⇒ 323 mk_fresh_variables body u 324 | Sfor s1 e s2 s3 ⇒ 325 let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in 326 let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in 327 let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in 328 〈fvs @ fvs' @fvs'', u'''〉 329 | Sbreak ⇒ 330 〈[ ], u〉 331 | Scontinue ⇒ 332 〈[ ], u〉 333 | Sreturn _ ⇒ 334 〈[ ], u〉 335 | Sswitch e branches ⇒ 336 let 〈ident, u'〉 ≝ fresh ? u in (* This is actually the only point where we need to create a fresh var. *) 337 let 〈fvs, u''〉 ≝ mk_fresh_variables_branches branches u' in 338 〈fvs @ [ident], u''〉 (* reversing the order to match a proof invariant *) 339 | Slabel label body ⇒ 340 mk_fresh_variables body u 341 | Sgoto _ ⇒ 342 〈[ ], u〉 343 | Scost cost body ⇒ 344 mk_fresh_variables body u 345 ] 346 347 and mk_fresh_variables_branches 348 (l : labeled_statements) 349 (u : universe SymbolTag) 350 (* : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝ 351 match l with 352 [ LSdefault st ⇒ 353 mk_fresh_variables st u 354 | LScase sz int st tl => 355 let 〈fvs, u'〉 ≝ mk_fresh_variables_branches tl u in 356 let 〈fvs',u''〉 ≝ mk_fresh_variables st u' in 357 〈fvs @ fvs', u''〉 358 ]. 359 360 (* Copied this from Csyntax.ma, lifted from Prop to Type 361 (I needed to eliminate something proved with this towards Type) *) 362 let rec statement_indT 363 (P:statement → Type[1]) (Q:labeled_statements → Type[1]) 364 (Ssk:P Sskip) 365 (Sas:∀e1,e2. P (Sassign e1 e2)) 366 (Sca:∀eo,e,args. P (Scall eo e args)) 367 (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2)) 368 (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2)) 369 (Swh:∀e,s. P s → P (Swhile e s)) 370 (Sdo:∀e,s. P s → P (Sdowhile e s)) 371 (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3)) 372 (Sbr:P Sbreak) 373 (Sco:P Scontinue) 374 (Sre:∀eo. P (Sreturn eo)) 375 (Ssw:∀e,ls. Q ls → P (Sswitch e ls)) 376 (Sla:∀l,s. P s → P (Slabel l s)) 377 (Sgo:∀l. P (Sgoto l)) 378 (Scs:∀l,s. P s → P (Scost l s)) 379 (LSd:∀s. P s → Q (LSdefault s)) 380 (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t)) 381 (s:statement) on s : P s ≝ 382 match s with 383 [ Sskip ⇒ Ssk 384 | Sassign e1 e2 ⇒ Sas e1 e2 385 | Scall eo e args ⇒ Sca eo e args 386 | Ssequence s1 s2 ⇒ Ssq s1 s2 387 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) 388 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) 389 | Sifthenelse e s1 s2 ⇒ Sif e s1 s2 390 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) 391 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) 392 | Swhile e s ⇒ Swh e s 393 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 394 | Sdowhile e s ⇒ Sdo e s 395 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 396 | Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3 397 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) 398 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) 399 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3) 400 | Sbreak ⇒ Sbr 401 | Scontinue ⇒ Sco 402 | Sreturn eo ⇒ Sre eo 403 | Sswitch e ls ⇒ Ssw e ls 404 (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls) 405 | Slabel l s ⇒ Sla l s 406 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 407 | Sgoto l ⇒ Sgo l 408 | Scost l s ⇒ Scs l s 409 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 410 ] 411 and labeled_statements_indT 412 (P:statement → Type[1]) (Q:labeled_statements → Type[1]) 413 (Ssk:P Sskip) 414 (Sas:∀e1,e2. P (Sassign e1 e2)) 415 (Sca:∀eo,e,args. P (Scall eo e args)) 416 (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2)) 417 (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2)) 418 (Swh:∀e,s. P s → P (Swhile e s)) 419 (Sdo:∀e,s. P s → P (Sdowhile e s)) 420 (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3)) 421 (Sbr:P Sbreak) 422 (Sco:P Scontinue) 423 (Sre:∀eo. P (Sreturn eo)) 424 (Ssw:∀e,ls. Q ls → P (Sswitch e ls)) 425 (Sla:∀l,s. P s → P (Slabel l s)) 426 (Sgo:∀l. P (Sgoto l)) 427 (Scs:∀l,s. P s → P (Scost l s)) 428 (LSd:∀s. P s → Q (LSdefault s)) 429 (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t)) 430 (ls:labeled_statements) on ls : Q ls ≝ 431 match ls with 432 [ LSdefault s ⇒ LSd s 433 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 434 | LScase sz i s t ⇒ LSc sz i s t 435 (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 436 (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t) 437 ]. 438 439 lemma switch_removal_ok : 440 ∀st, u0, u1, post. 441 Σresult. 442 (switch_removal st ((\fst (mk_fresh_variables st u0)) @ post) u1 = Some ? result) ∧ (ret_fvs ? result = post). 443 #st 444 @(statement_indT ? (λls. ∀u0, u1, post. 445 Σresult. 446 (switch_removal_branches ls ((\fst (mk_fresh_variables_branches ls u0)) @ post) u1 = Some ? result) 447 ∧ (ret_fvs ? result = post) 448 ) … st) 449 [ 1: #u0 #u1 #post normalize 450 %{(mk_swret statement Sskip [] post u1)} % // 451 | 2: #e1 #e2 #u0 #u1 #post normalize 452 %{((mk_swret statement (Sassign e1 e2) [] post u1))} % try // 453 | 3: #e0 #e #args #u0 #u1 #post normalize 454 %{(mk_swret statement (Scall e0 e args) [] post u1)} % try // 455 | 4: #s1 #s2 #H1 #H2 #u0 #u1 #post normalize 456 elim (H1 u0 u1 ((\fst (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' * 457 cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta 458 elim (H2 u' (ret_u ? s1') post) #s2' * 459 cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta 460 #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize 461 %{(mk_swret statement (Ssequence (ret_st statement s1') (ret_st statement s2')) 462 (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2') 463 (ret_u statement s2'))} % try // 464 | 5: #e #s1 #s2 #H1 #H2 #u0 #u1 #post normalize 465 elim (H1 u0 u1 ((\fst (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' * 466 cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta 467 elim (H2 u' (ret_u ? s1') post) #s2' * 468 cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta 469 #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize 470 %{((mk_swret statement 471 (Sifthenelse e (ret_st statement s1') (ret_st statement s2')) 472 (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2') 473 (ret_u statement s2')))} % try // 474 | 6: #e #s #H #u0 #u1 #post normalize 475 elim (H u0 u1 post) #s1' * normalize 476 cases (mk_fresh_variables s u0) #fvs #u' 477 #Heq1 #Heq1_fvs >Heq1 normalize nodelta 478 %{(mk_swret statement (Swhile e (ret_st statement s1')) (ret_acc statement s1') 479 (ret_fvs statement s1') (ret_u statement s1'))} % try // 480 | 7: #e #s #H #u0 #u1 #post normalize 481 elim (H u0 u1 post) #s1' * normalize 482 cases (mk_fresh_variables s u0) #fvs #u' 483 #Heq1 #Heq1_fvs >Heq1 normalize nodelta 484 %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1') 485 (ret_fvs statement s1') (ret_u statement s1'))} % try // 486 | 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize 487 elim (H1 u0 u1 488 (\fst (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0))) @ 489 (\fst (mk_fresh_variables s3 (\snd (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @ 490 post)) #s1' * 491 cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta 492 elim (H2 u' (ret_u ? s1') ((\fst (mk_fresh_variables s3 (\snd (mk_fresh_variables s2 u')))) @ 493 post)) #s2' * 494 cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta 495 elim (H3 u'' (ret_u ? s2') post) #s3' * 496 cases (mk_fresh_variables s3 u'') #fvs'' #u''' normalize nodelta 497 #Heq3 #Heq3_fvs #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs 498 >associative_append >associative_append >Heq1 normalize >Heq1_fvs 499 >Heq2 normalize >Heq2_fvs >Heq3 normalize 500 %{(mk_swret statement 501 (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3')) 502 (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3') 503 (ret_fvs statement s3') (ret_u statement s3'))} % try // 504 | 9: #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % // 505 | 10: #u0 #u1 #post normalize %{(mk_swret statement Scontinue [] post u1)} % // 506 | 11: #e #u0 #u1 #post normalize %{(mk_swret statement (Sreturn e) [] post u1)} % // 507 | 12: #e #ls #H #u0 #u1 #post 508 whd in match (mk_fresh_variables ??); 509 whd in match (switch_removal ???); 510 elim (fresh ? u0) #fresh #u' 511 elim (H u' u1 ([fresh] @ post)) #ls' * normalize nodelta 512 cases (mk_fresh_variables_branches ls u') #fvs #u'' normalize nodelta 513 >associative_append #Heq #Heq_fvs >Heq normalize nodelta 514 >Heq_fvs normalize nodelta 515 cases (simplify_switch ???) #st' #u''' normalize nodelta 516 %{((mk_swret statement 517 (Ssequence (Sassign (Expr (Evar fresh) (typeof e)) e) st') 518 (〈fresh,typeof e〉::ret_acc labeled_statements ls') ([]@post) 519 (ret_u labeled_statements ls')))} % // 520 | 13: #l #s #H #u0 #u1 #post normalize 521 elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs 522 %{(mk_swret statement (Slabel l (ret_st statement s')) (ret_acc statement s') 523 post (ret_u statement s'))} % // 524 | 14: #l #u0 #u1 #post normalize %{((mk_swret statement (Sgoto l) [] post u1))} % // 525 | 15: #l #s #H #u0 #u1 #post normalize 526 elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs 527 %{(mk_swret statement (Scost l (ret_st statement s')) (ret_acc statement s') 528 post (ret_u statement s'))} % // 529 | 16: #s #H #u0 #u1 #post normalize 530 elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs 531 %{(mk_swret labeled_statements (LSdefault (ret_st statement s')) 532 (ret_acc statement s') post (ret_u statement s'))} % // 533 | 17: #sz #i #hd #tl #H1 #H2 #u0 #u1 #post normalize 534 elim (H2 u0 u1 (\fst (mk_fresh_variables hd (\snd (mk_fresh_variables_branches tl u0))) @ post)) #ls' * 535 cases (mk_fresh_variables_branches tl u0) #fvs #u' normalize 536 elim (H1 u' (ret_u labeled_statements ls') post) #s1' * 537 cases (mk_fresh_variables hd u') #fvs' #u' normalize #Heq #Heq_fvs #Heql #Heql_fvs 538 >associative_append >Heql normalize >Heql_fvs >Heq normalize 539 %{(mk_swret labeled_statements 540 (LScase sz i (ret_st statement s1') (ret_st labeled_statements ls')) 541 (ret_acc labeled_statements ls'@ret_acc statement s1') 542 (ret_fvs statement s1') (ret_u statement s1'))} % // 543 ] qed. 295 definition ret_st : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → A ≝ 296 λA,x. 297 let 〈s,vars,u〉 ≝ x in s. 298 299 definition ret_vars : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → list (ident × type) ≝ 300 λA,x. 301 let 〈s,vars,u〉 ≝ x in vars. 302 303 definition ret_u : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → (universe SymbolTag) ≝ 304 λA,x. 305 let 〈s,vars,u〉 ≝ x in u. 544 306 545 307 axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *) 546 308 547 309 (* Proof that switch_removal_switch_free does its job. *) 548 lemma switch_removal_switch_free : ∀st,fvs,u,result. switch_removal st fvs u = Some ? result → switch_free (ret_st ? result). 549 #st @(statement_ind2 ? (λls. ∀fvs,u,ls_result. switch_removal_branches ls fvs u = Some ? ls_result → 550 branches_switch_free (ret_st ? ls_result)) … st) 551 [ 1: #fvs #u #result normalize #Heq destruct (Heq) // 552 | 2: #e1 #e2 #fvs #u #result normalize #Heq destruct (Heq) // 553 | 3: #e0 #e #args #fvs #u #result normalize #Heq destruct (Heq) // 554 | 4: #s1 #s2 #H1 #H2 #fvs #u #result normalize lapply (H1 fvs u) 555 elim (switch_removal s1 fvs u) normalize 556 [ 1: #_ #Habsurd destruct (Habsurd) 557 | 2: #res1 #Heq1 lapply (H2 (ret_fvs statement res1) (ret_u statement res1)) 558 elim (switch_removal s2 (ret_fvs statement res1) (ret_u statement res1)) 559 [ 1: normalize #_ #Habsurd destruct (Habsurd) 560 | 2: normalize #res2 #Heq2 #Heq destruct (Heq) 561 normalize @conj 562 [ 1: @Heq1 // | 2: @Heq2 // ] 563 ] ] 310 lemma switch_removal_switch_free : ∀st,u. switch_free (ret_st ? (switch_removal st u)). 311 #st @(statement_ind2 ? (λls. ∀u. branches_switch_free (ret_st ? (switch_removal_branches ls u))) … st) 312 try // 313 [ 1: #s1 #s2 #H1 #H2 #u normalize 314 lapply (H1 u) 315 cases (switch_removal s1 u) * #st1 #vars1 #u' normalize #HA 316 lapply (H2 u') 317 cases (switch_removal s2 u') * #st2 #vars2 #u'' normalize #HB 318 @conj assumption 564 319 | *: 565 320 (* TODO the first few cases show that the lemma is routinely proved. TBF later. *) … … 623 378 max_id (max_of_expr f) 624 379 (max_id retmax 625 (fold l ?? (λacc,elt. max_id (max_of_expr elt) acc) least_identifier args) )380 (foldr ?? (λelt,acc. max_id (max_of_expr elt) acc) least_identifier args) ) 626 381 | Ssequence s1 s2 ⇒ 627 382 max_id (max_of_statement s1) (max_of_statement s2) … … 663 418 definition function_switch_removal : function → function × (list (ident × type)) ≝ 664 419 λf. 665 (λres_record. 666 let new_vars ≝ ret_acc ? res_record in 667 let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (ret_st ? res_record) in 668 〈result, new_vars〉) 669 (let u ≝ universe_of_max (max_id_of_function f) in 670 let 〈fvs,u'〉 as Hfv ≝ mk_fresh_variables (fn_body f) u in 671 match switch_removal (fn_body f) fvs u' return λx. (switch_removal (fn_body f) fvs u' = x) → ? with 672 [ None ⇒ λHsr. ? 673 | Some res_record ⇒ λ_. res_record 674 ] (refl ? (switch_removal (fn_body f) fvs u'))). 675 lapply (switch_removal_ok (fn_body f) u u' [ ]) * #result' * #Heq #Hret_eq 676 <Hfv in Heq; >append_nil >Hsr #Habsurd destruct (Habsurd) 677 qed. 420 let u ≝ universe_of_max (max_id_of_function f) in 421 let 〈st, vars, u'〉 ≝ switch_removal (fn_body f) u in 422 let result ≝ mk_function (fn_return f) (fn_params f) (vars @ (fn_vars f)) st in 423 〈result, vars〉. 678 424 679 425 let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝ … … 695 441 sf_funcs 696 442 (prog_main … p). 697 698 443 699 444 (* ----------------------------------------------------------------------------- … … 742 487 #H1 #H2 destruct (H2) /2/ qed. 743 488 744 lemma fresh_eq : ∀u,i. fresh_for_univ SymbolTag i u → ∃fv,u'. fresh ? u = 〈fv, u'〉 ∧ fresh_for_univ ? i u'. 745 #u #i #Hfresh lapply (fresh_for_univ_still_fresh … Hfresh) 746 cases (fresh SymbolTag u) 747 #fv #u' #H %{fv} %{u'} @conj try // @H // 748 qed. 489 definition fresher_than_or_equal : universe SymbolTag → universe SymbolTag → Prop ≝ 490 λu1,u2. 491 match u1 with 492 [ mk_universe p1 ⇒ 493 match u2 with 494 [ mk_universe p2 ⇒ p2 ≤ p1 ] ]. 495 496 definition fte ≝ fresher_than_or_equal. 497 498 lemma transitive_fte : ∀u1,u2,u3. fte u1 u2 → fte u2 u3 → fte u1 u3. 499 * #u1 * #u2 * #u3 normalize /2 by transitive_le/ 500 qed. 501 502 lemma reflexive_fte : ∀u. fte u u. 503 * // qed. 504 505 lemma fresher_for_univ : ∀u1,u2. fte u1 u2 → ∀i. fresh_for_univ ? i u2 → fresh_for_univ ? i u1. 506 * #p * #p' normalize #H * #i normalize 507 /2 by transitive_le/ 508 qed. 509 510 lemma fresh_fte : ∀u2,u1,fv. fresh ? u2 = 〈fv,u1〉 → fte u1 u2. 511 * #u1 * #u2 * #fv normalize #H1 destruct // 512 qed. 513 514 lemma produce_cond_fte : ∀e,exit,ls,u. fte (\snd (produce_cond e ls u exit)) u. 515 #e #exit #ls @(branches_ind … ls) 516 [ 1: #st #u normalize lapply (fresh_fte u) 517 cases (fresh ? u) #lab #u1 #H lapply (H u1 lab (refl ??)) normalize // 518 | 2: #sz #i #hd #tl #Hind #u normalize 519 lapply (Hind u) cases (produce_cond e tl u exit) * 520 #subcond #sublabel #u1 #Hfte normalize 521 lapply (fresh_fte u1) 522 cases (fresh ? u1) #lab #u2 #H2 lapply (H2 u2 lab (refl ??)) 523 #Hfte' normalize cases u2 in Hfte'; #u2 524 cases u in Hfte; #u cases u1 #u1 normalize 525 /2 by transitive_le/ 526 ] qed. 749 527 750 528 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)). 751 #e #exit #ls @(branches_ind … ls) 752 [ 1: #st #u #i #Hfresh normalize 753 lapply (fresh_for_univ_still_fresh … Hfresh) 754 cases (fresh ? u) #lab #u1 #H lapply (H lab u1 (refl ??)) normalize // 755 | 2: #sz #i #hd #tl #Hind #u #i' #Hfresh normalize 756 lapply (Hind u i' Hfresh) elim (produce_cond e tl u exit) * 757 #subcond #sublabel #u1 #Hfresh1 normalize 758 lapply (fresh_for_univ_still_fresh … Hfresh1) 759 cases (fresh ? u1) #lab #u2 #H2 lapply (H2 lab u2 (refl ??)) normalize // 760 ] qed. 761 762 lemma simplify_switch_fresh : ∀u,i,e,ls. 763 fresh_for_univ ? i u → 529 #e #exit #ls #u #i @fresher_for_univ @produce_cond_fte qed. 530 531 lemma simplify_switch_fte : ∀u,e,ls. 532 fte (\snd (simplify_switch e ls u)) u. 533 #u #e #ls normalize 534 lapply (fresh_fte u) 535 cases (fresh ? u) 536 #exit_label #uv1 #Haux lapply (Haux uv1 exit_label (refl ??)) -Haux #Haux 537 normalize 538 lapply (produce_cond_fte e exit_label ls uv1) 539 cases (produce_cond ????) * #stm #label #uv2 normalize nodelta 540 cases uv2 #uv2 cases uv1 in Haux; #uv1 cases u #u normalize 541 /2 by transitive_le/ 542 qed. 543 544 lemma simplify_switch_fresh : ∀u,i,e,ls. 545 fresh_for_univ ? i u → 764 546 fresh_for_univ ? i (\snd (simplify_switch e ls u)). 765 #u #i #e #ls #Hfresh 766 normalize 767 lapply (fresh_for_univ_still_fresh … Hfresh) 768 cases (fresh ? u) 769 #exit_label #uv1 #Haux lapply (Haux exit_label uv1 (refl ??)) -Haux #Haux 770 normalize lapply (produce_cond_fresh e exit_label ls … Haux) 771 elim (produce_cond ????) * #stm #label #uv2 normalize nodelta // 772 qed. 547 #u #i #e #ls @fresher_for_univ @simplify_switch_fte qed. 548 549 lemma switch_removal_fte : ∀st,u. 550 fte (ret_u ? (switch_removal … st u)) u. 551 #st @(statement_ind2 ? (λls. ∀u. fte (ret_u ? (switch_removal_branches ls u)) u) … st) 552 try /2 by reflexive_fte/ 553 [ 1: #s1 #s2 #Hind1 #Hind2 #u normalize 554 lapply (Hind1 u) 555 cases (switch_removal s1 u) * #s1' #fvs1 #u' normalize nodelta 556 lapply (Hind2 u') 557 cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize 558 #HA #HB @(transitive_fte … HA HB) 559 | 2: #e #s1 #s2 #Hind1 #Hind2 #u normalize 560 lapply (Hind1 u) 561 cases (switch_removal s1 u) * #s1' #fvs1 #u' normalize nodelta 562 lapply (Hind2 u') 563 cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize 564 #HA #HB @(transitive_fte … HA HB) 565 | 3,7,8: #e #s #Hind #u normalize 566 lapply (Hind u) 567 cases (switch_removal s u) * #s' #fvs #u' normalize #H @H 568 | 4: #e #s #Hind #u normalize 569 lapply (Hind u) 570 cases (switch_removal s u) * #s' #fvs #u' normalize #H @H 571 | 5: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #u normalize 572 lapply (Hind1 u) cases (switch_removal s1 u) * #s1' #fvs1 #u' #Hfte1 573 normalize nodelta 574 lapply (Hind2 u') cases (switch_removal s2 u') * #s2' #fvs2 #u'' #Hfte2 575 normalize nodelta 576 lapply (Hind3 u'') cases (switch_removal s3 u'') * #s2' #fvs2 #u'' #Hfte3 577 normalize nodelta 578 /3 by transitive_fte/ 579 | 6: #e #ls #Hind #u whd in match (switch_removal ??); 580 lapply (Hind u) 581 cases (switch_removal_branches ls u) * #ls #fvs #u' #Hfte1 582 normalize nodelta 583 lapply (fresh_fte … u') cases (fresh ? u') #fv #u'' #H lapply (H u'' fv (refl ??)) #Hfte2 584 normalize nodelta 585 lapply (simplify_switch_fte u'' (Expr (Evar fv) (typeof e)) ls) 586 cases (simplify_switch ???) 587 normalize nodelta 588 #st' #u''' #Hfte3 589 /3 by transitive_fte/ 590 | 9: #s #H #u normalize 591 lapply (H u) cases (switch_removal s u) * #st' #fvs normalize #u' #H @H 592 | 10: #sz #i #st #ls #Hind1 #Hind2 #u normalize 593 lapply (Hind2 u) cases (switch_removal_branches ls u) * #ls' #fvs' #u' 594 normalize nodelta #Hfte1 595 lapply (Hind1 … u') cases (switch_removal st u') * #st' #fvs'' #u'' 596 normalize nodelta #Hfte2 597 /3 by transitive_fte/ 598 ] qed. 599 600 lemma switch_removal_fresh : ∀u,i,st. 601 fresh_for_univ ? i u → 602 fresh_for_univ ? i (ret_u … (switch_removal st u)). 603 #u #i #st @fresher_for_univ @switch_removal_fte qed. 773 604 774 605 (* ----------------------------------------------------------------------------- … … 879 710 ] qed. 880 711 712 lemma fresh_to_substatements : 713 ∀s,u. fresh_for_statement s u → 714 substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u). 715 #s #u cases s 716 whd in match (fresh_for_statement ??); 717 whd in match (substatement_P ???); try /2/ 718 [ 1: #e1 #e2 719 whd in match (fresh_for_statement ??); 720 whd in match (substatement_P ???); 721 #H lapply (fresh_max_split … H) * /2 by conj/ 722 | 2: #e1 #e2 #args 723 whd in match (fresh_for_statement ??); 724 whd in match (substatement_P ???); 725 cases e1 normalize nodelta 726 [ 1: #H lapply (fresh_max_split … H) * #HA #HB @conj try @HA 727 elim args in HB; try /2 by I/ #hd #tl normalize nodelta #Hind #HB 728 elim (fresh_max_split … HB) #HC #HD 729 whd in match (foldr ?????) in HD; 730 elim (fresh_max_split … HD) #HE #HF 731 @conj try assumption 732 @Hind >max_id_commutative >max_id_one_neutral @HF 733 | 2: #expr #H cases (fresh_max_split … H) #HA normalize nodelta #HB 734 cases (fresh_max_split … HB) #HC #HD @conj try @conj try // elim args in HD; try // 735 #e #l #Hind #HD 736 whd in match (foldr ?????) in HD; 737 elim (fresh_max_split … HD) #HE #HF 738 @conj try assumption 739 @Hind @HF ] 740 | 3: #stmt1 #stmt2 whd in ⊢ (% → %); @fresh_max_split 741 | 4: #e #s1 #s2 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) * 742 #H1 @fresh_max_split 743 | 5: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H) 744 | 6: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H) 745 | 7: #s1 #e #s2 #s3 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) * #H1 #H2 746 @conj try @conj try @I try @conj try @I 747 elim (fresh_max_split … H1) elim (fresh_max_split … H2) /2/ 748 | 8: #opt cases opt try /2/ 749 | 9: #e #ls #H whd @conj lapply (fresh_max_split … H) * #HA #HB try // lapply HB 750 @(labeled_statements_ind … ls) 751 [ 1: #s' #H' // 752 | 2: #sz #i #s' #tl #Hind #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj 753 [ 1: // 754 | 2: @Hind @H1 ] ] 755 | 10: #lab #stmt #H whd lapply (fresh_max_split … H) * // 756 ] qed. 757 881 758 (* Auxilliary commutation lemma used in [substatement_fresh]. *) 882 883 759 lemma foldl_max : ∀l,a,b. 884 760 foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l = … … 945 821 definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res. 946 822 947 definition outbound_pointer ≝ λm,p. 948 Zltb (block_id (pblock p)) (nextblock m) = true ∧ 949 Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))) = true ∧ 950 high_bound m (pblock p) = Z_of_unsigned_bitvector … (offv (poff p)). 951 952 (* a valid_pointer is either /inside/ the bounds of the target block xor /one off/ the end. *) 953 lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p ∨ outbound_pointer m p. 823 lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p. 954 824 #m #p @conj 955 825 [ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??); 956 whd in match (outbound_pointer ??);957 826 whd in match (do_if_in_bounds); normalize nodelta 958 827 cases (Zltb (block_id (pblock p)) (nextblock m)) 959 [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] 828 [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] 960 829 >andb_lsimpl_true normalize nodelta 961 830 cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) 962 831 [ 2: normalize nodelta #Habsurd destruct (Habsurd) ] 963 832 >andb_lsimpl_true normalize nodelta 964 lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p))) 965 elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p))) 966 [ 1: #H >H #_ normalize nodelta #_ %1 #A #f /2 by ex_intro/ 967 | 2: * #_ #H1 #_ #H2 >(Zleb_true_to_Zleb_true_to_eq … H1 H2) %2 @conj try @conj @refl ] 968 | 2: whd in match (valid_pointer ??); * 969 [ 1: whd in match (in_bounds_pointer ??); #H 970 lapply (H bool (λblock,contents,off. true)) 971 * #foo whd in match (do_if_in_bounds ????); 972 cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta 973 [ 2: #Habsurd destruct (Habsurd) ] 974 >andb_lsimpl_true 975 cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) 976 normalize nodelta 977 [ 2: #Habsurd destruct (Habsurd) ] 978 >andb_lsimpl_true 979 elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p)))) 980 [ 1: #H >(Zltb_to_Zleb_true … H) #_ @refl 981 | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ] 982 | 2: whd in match (outbound_pointer ??); * * #Hlt #Hleb >Hlt >Hleb 983 #Hhigh >Hhigh >andb_lsimpl_true 984 lapply (reflexive_Zle … (Z_of_unsigned_bitvector offset_size (offv (poff p)))) 985 #Hle >(Zle_to_Zleb_true … Hle) @refl 986 ] 987 ] qed. 833 #Hlt >Hlt normalize nodelta #A #f /2 by ex_intro/ 834 | 2: whd in match (valid_pointer ??); 835 whd in match (in_bounds_pointer ??); #H 836 lapply (H bool (λblock,contents,off. true)) 837 * #foo whd in match (do_if_in_bounds ????); 838 cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta 839 [ 2: #Habsurd destruct (Habsurd) ] 840 >andb_lsimpl_true 841 cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) 842 normalize nodelta 843 [ 2: #Habsurd destruct (Habsurd) ] 844 >andb_lsimpl_true 845 elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p)))) 846 [ 1: #H >H // 847 | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ] 848 ] qed. 849 850 lemma valid_pointer_to_Prop : 851 ∀m,p. valid_pointer m p = true → 852 (block_id (pblock p)) < (nextblock m) ∧ 853 (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧ 854 (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)). 855 #m #p whd in match (valid_pointer ??); 856 #H 857 lapply (Zleb_true_to_Zle (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) 858 lapply (Zltb_true_to_Zlt (block_id (pblock p)) (nextblock m)) 859 cases (Zltb (block_id (pblock p)) (nextblock m)) in H; 860 [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true 861 cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) 862 normalize nodelta 863 [ 2: #Habsurd destruct ] 864 #Hlt1 #Hlt2 #Hle @conj try @conj 865 try @(Hlt2 (refl ??)) try @(Hle (refl ??)) @(Zltb_true_to_Zlt … Hlt1) 866 qed. 988 867 989 868 (* A writeable_block is a block that is: … … 995 874 wb_valid : valid_block m b; 996 875 wb_nonempty : low (blocks m b) < high (blocks m b) 997 }. 876 }. 998 877 999 878 (* Type stating that m2 is an extension of m1, parameterised by a list of blocks where we can write freely *) … … 1004 883 me_writeable_valid : ∀b. meml ? b writeable → nonempty_block m2 b; 1005 884 (* blocks in [m1] than can be validly pointed to cannot be in [me_writeable]. *) 1006 me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable); 1007 (* This field does not entail [me_not_writeable] and is necessary to prove valid 885 me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable) 886 887 (* This field is not entailed [me_not_writeable] and is necessary to prove valid 1008 888 pointer conservation after a [free]. *) 1009 me_not_writeable_ptr : ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable); 1010 889 1011 890 (* Extension blocks contain nothing in [m1] *) 1012 891 (* me_not_mapped : ∀b. meml … b me_writeable → blocks m1 b = empty_block OZ OZ; *) … … 1019 898 compare are valid before being equal). 1020 899 *) 1021 me_valid_pointers : ∀p. (* ¬ (freed_pointer m1 p) → *) 900 (* me_valid_pointers : ∀p. 1022 901 valid_pointer m1 p = true → 1023 valid_pointer m2 p = true 902 valid_pointer m2 p = true *) 1024 903 }. 904 905 (* Since we removed end_pointers, we can prove some stuff that was previously given as a field of 906 sr_memext. *) 907 lemma me_not_writeable_ptr : 908 ∀m1,m2,writeable. 909 sr_memext m1 m2 writeable → 910 ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable). 911 #m1 #m2 #writeable #Hext #p #Hvalid 912 cut (nonempty_block m1 (pblock p)) 913 [ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % // 914 /2 by Zle_to_Zlt_to_Zlt/ 915 | 2: @(me_not_writeable … Hext) ] 916 qed. 1025 917 1026 918 (* If we have a memory extension, we can simulate loads *) … … 1052 944 >(Zle_to_Zleb_true … Hlow) >(Zlt_to_Zltb_true … Hhigh) normalize 1053 945 >Hres @refl 946 qed. 947 948 lemma me_valid_pointers : 949 ∀m1,m2,writeable. 950 sr_memext m1 m2 writeable → 951 ∀p. valid_pointer m1 p = true → valid_pointer m2 p = true. 952 * #contents1 #nextblock1 #Hnextblock_pos1 953 * #contents2 #nextblock2 #Hnextblock_pos2 #writeable #Hmemext * #pb #po #Hvalid 954 cut (nonempty_block (mk_mem contents1 nextblock1 Hnextblock_pos1) pb) 955 [ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % // 956 /2 by Zle_to_Zlt_to_Zlt/ ] 957 #Hnonempty lapply (me_nonempty … Hmemext … Hnonempty) * * #Hvalid_block #Hlow_lt_high 958 #Hcontents_eq normalize >(Zlt_to_Zltb_true … Hvalid_block) normalize nodelta 959 <Hcontents_eq cases (valid_pointer_to_Prop … Hvalid) * #_ #Hle #Hlt 960 >(Zle_to_Zleb_true … Hle) normalize nodelta 961 >(Zlt_to_Zltb_true … Hlt) @refl 1054 962 qed. 1055 963 … … 1087 995 lapply (Hsim (p0 id0) res0) normalize #Hsol #H @Hsol @H ] 1088 996 ] qed. 1089 997 1090 998 lemma environment_sim_invert : 1091 999 ∀en1,en2. environment_sim en1 en2 → … … 1206 1114 ] 1207 1115 ] qed. 1208 1209 1116 1210 1117 lemma blocks_of_env_cons : … … 1346 1253 [ 1: #b #H @conj try % elim H try // 1347 1254 | 2: #b * 1348 | 3: #b #_ normalize % // 1349 | 4: #p #Hvalid % * 1350 (* | 4: #b * *) 1351 | 5: #p normalize >Hcontents_eq #H @H 1352 ] qed. 1255 | 3: #b #_ normalize % // ] 1256 qed. 1353 1257 1354 1258 (* memory extensions form a preorder relation *) … … 1374 1278 lapply (me_not_writeable … H23 … Hvalid2) * #H #_ @H assumption 1375 1279 ] 1376 | 4: #p #Hvalid % #Hmem lapply (mem_append_forward ???? Hmem) * 1377 [ 1: #Hmem12 1378 lapply (me_not_writeable_ptr … H12 … Hvalid) * #H @H assumption 1379 | 2: #Hmem23 1380 lapply (me_valid_pointers … H12 … Hvalid) #Hvalid2 1381 lapply (me_not_writeable_ptr … H23 … Hvalid2) * #H @H assumption 1382 ] 1383 | 5: #p #Hvalid @(me_valid_pointers … H23) @(me_valid_pointers … H12) @Hvalid 1384 ] qed. 1385 1386 lemma memory_ext_reflexive : 1387 ∀m. sr_memext m m [ ]. 1280 ] qed. 1281 1282 lemma memory_ext_reflexive : ∀m. sr_memext m m [ ]. 1388 1283 #m % /2/ #b * qed. 1389 1284 … … 1456 1351 >andb_lsimpl_true 1457 1352 normalize nodelta #H 1458 @Zltb_to_Zleb_true1459 1353 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H; 1460 1354 try // normalize #Habsurd destruct (Habsurd) 1355 qed. 1356 1357 lemma bestorev_to_valid_pointer : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer m ptr = true. 1358 * #contents #next #nextpos #ptr #v #res 1359 whd in match (bestorev ???); 1360 whd in match (valid_pointer ??); 1361 cases (Zltb (block_id (pblock ptr)) next) 1362 normalize nodelta 1363 [ 2: #Habsurd destruct (Habsurd) ] 1364 >andb_lsimpl_true 1365 whd in match (low_bound ??); 1366 whd in match (high_bound ??); 1367 cases (Zleb (low (contents (pblock ptr))) 1368 (Z_of_unsigned_bitvector offset_size (offv (poff ptr)))) 1369 [ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ] 1370 >andb_lsimpl_true 1371 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) 1372 normalize nodelta try // #Habsurd destruct (Habsurd) 1461 1373 qed. 1462 1374 … … 1557 1469 qed. 1558 1470 1471 (* If a pointer is still valid after a free (meaning we freed another block), then it was valid before. *) 1559 1472 lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p. 1560 1473 #m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %); 1561 1474 #H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %); 1562 1475 elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b))) 1563 [ 1: #Hlt >Hlt normalize nodelta 1476 [ 1: #Hlt >Hlt normalize nodelta 1564 1477 @(eq_block_elim … b (pblock p)) 1565 1478 [ 1: #Heq >Heq whd in match (free ??); … … 1583 1496 qed. 1584 1497 1585 lemma outbound_free_to_outbound : ∀m,b,p. outbound_pointer (free m b) p → outbound_pointer m p. 1586 #m #b #p whd in match (free ??); 1587 whd in match (outbound_pointer ??) in ⊢ (% → %); 1588 whd in match (update_block ????); 1589 whd in match (low_bound ??); whd in match (high_bound ??); 1590 @(eq_block_elim … (pblock p) b) normalize nodelta 1591 [ 1: #Heq >Heq cases (Zltb ? (nextblock m)) 1592 [ 2: * * #Habsurd destruct (Habsurd) ] 1593 * * #_ whd in match (low ?); whd in match (high ?); 1594 #H1 #H2 <H2 in H1; normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 1595 | 2: #Hneq #H @H ] 1596 qed. 1597 1498 (* Cf [in_bounds_free_to_in_bounds] *) 1598 1499 lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true. 1599 1500 #m #b #p #Hvalid 1600 lapply (valid_pointer_def … m p) * #_ #Hdef @Hdef 1601 elim (valid_pointer_def … (free m b) p) #H #_ 1602 elim (H Hvalid)1603 [ 1: #Hin %1 @in_bounds_free_to_in_bounds assumption 1604 | 2: #Hout %2 @outbound_free_to_outbound assumption ] 1605 qed. 1606 1501 cases (valid_pointer_def … m p) #HA #HB 1502 cases (valid_pointer_def … (free m b) p) #HC #HD 1503 @HB @(in_bounds_free_to_in_bounds … b) 1504 @HC @Hvalid 1505 qed. 1506 1507 (* Making explicit the argument above. *) 1607 1508 lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p. 1608 1509 #m #b #p … … 1613 1514 whd in match (high_bound ??); 1614 1515 @(eq_block_elim … b (pblock p)) 1615 [ 1: #Heq >Heq >eq_block_b_b normalize nodelta1516 [ 1: #Heq <Heq >eq_block_b_b normalize nodelta 1616 1517 whd in match (low ?); whd in match (high ?); 1617 1518 cases (Zltb ? (nextblock m)) … … 1621 1522 qed. 1622 1523 1524 (* Lifting the property of being valid after a free to memory extensions *) 1623 1525 lemma valid_pointer_free : ∀m1,m2,writeable. sr_memext m1 m2 writeable → ∀p,b. valid_pointer (free m1 b) p = true → valid_pointer (free m2 b) p = true. 1624 1526 #m1 #m2 #writeable #Hext #p #b #Hvalid … … 1703 1605 ] 1704 1606 ] 1705 | 4: #p #Hvalid 1706 lapply (valid_free_to_valid … Hvalid) #Hvalid' 1707 lapply (me_not_writeable_ptr … Hext … Hvalid') * #HA % #HB @HA 1708 elim writeable in HB; 1709 [ 1: * 1710 | 2: #hd #tl #Hind whd in match (filter ???) in ⊢ (% → ?); >eqb_to_eq_block 1711 @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta 1712 [ 1: #Heq #H normalize %2 @(Hind H) 1713 | 2: #Hblocks_neq whd in match (meml ???); * 1714 [ 1: #Hneq normalize %1 assumption 1715 | 2: #Hmem normalize %2 @(Hind Hmem) ] 1716 ] 1717 ] 1718 | 5: #p @(valid_pointer_free … writeable) @Hext 1719 ] qed. 1607 ] qed. 1608 1720 1609 1721 1610 (* Freeing from an extension block is ok. *) … … 1769 1658 ] ] ] * #Hmem' #Hblocks_neq 1770 1659 lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption 1771 | 4: #p #Hnonempty % #Hmem 1772 cut (mem block (pblock p) writeable ∧ (pblock p) ≠ b) 1773 [ elim writeable in Hmem; 1774 [ 1: normalize @False_ind 1775 | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block 1776 @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta 1777 [ 1: #Heq #H whd in match (meml ???); destruct 1778 elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption 1779 | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * 1780 [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] 1781 | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ] 1782 ] ] ] * #Hmem' #Hblocks_neq 1783 lapply (me_not_writeable_ptr … Hext … Hnonempty) * #H @H assumption 1784 | 5: #p #Hvalid lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_mem 1785 lapply (mem_not_mem_neq … Hb_writeable … Hnot_mem) #Hneq 1786 lapply (me_valid_pointers … Hext … Hvalid) #Hvalid' 1787 whd in match (free ??); 1788 whd in match (valid_pointer ??) in ⊢ (??%%); 1789 whd in match (low_bound ??); whd in match (high_bound ??); 1790 whd in match (update_block ?????); 1791 >(not_eq_block_rev … Hneq) normalize 1792 @Hvalid' 1793 ] qed. 1794 1795 1660 ] qed. 1796 1661 1797 1662 … … 1881 1746 sr_memext m1 m2 (hd :: writeable) → 1882 1747 sr_memext m1 m2 writeable. 1883 #m1 #m2 #hd #writeable * 1884 #Hnonempty #Hwriteable_valid #Hnot_writeable #Hnot_writeable_ptr #Hvalid_pointers%1748 #m1 #m2 #hd #writeable * 1749 #Hnonempty #Hwriteable_valid #Hnot_writeable % 1885 1750 try assumption 1886 1751 [ 1: #b #Hmem @Hwriteable_valid whd %2 assumption 1887 1752 | 2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem 1888 | 3: #p #Hvalid % #Hmem elim (Hnot_writeable_ptr … Hvalid) #H @H whd %2 @Hmem1889 1753 ] qed. 1890 1754 … … 1902 1766 lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem' 1903 1767 lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption 1904 | 4: #p #Hvalid % #Hmem 1905 lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem' 1906 lapply (me_not_writeable_ptr … Hext … Hvalid) * #H @H assumption 1907 | 5: @(me_valid_pointers … Hext) ] 1908 qed. 1909 1910 axiom lset_inclusion_difference : 1768 ] qed. 1769 1770 lemma lset_difference_empty : 1911 1771 ∀A : DeqSet. 1912 ∀s1,s2 : lset (carr A). 1913 lset_inclusion ? s1 s2 → 1914 ∃s2'. lset_eq ? s2 (s1 @ s2') ∧ 1915 lset_disjoint ? s1 s2' ∧ 1916 lset_eq ? s2' (lset_difference ? s2 s1). 1917 1918 lemma memory_eq_to_memory_ext_pre : 1919 ∀m1,m1',m2,writeable. 1920 memory_eq m1 m1' → 1921 sr_memext m1' m2 writeable → 1922 sr_memext m1 m2 writeable. 1923 #m1 #m1' #m2 #writeable #Heq #Hext 1924 lapply (memory_eq_to_mem_ext … Heq) #Hext' 1925 @(memory_ext_transitive … Hext' Hext) 1926 qed. 1927 1928 lemma memory_eq_to_memory_ext_post : 1929 ∀m1,m2,m2',writeable. 1930 memory_eq m2' m2 → 1931 sr_memext m1 m2' writeable → 1932 sr_memext m1 m2 writeable. 1933 #m1 #m2 #m2' #writeable #Heq #Hext 1934 lapply (memory_eq_to_mem_ext … Heq) #Hext' 1935 lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H 1772 ∀s1. lset_difference A s1 [ ] = s1. 1773 #A #s1 elim s1 try // 1774 #hd #tl #Hind >lset_difference_unfold >Hind @refl 1936 1775 qed. 1937 1776 … … 1946 1785 | 1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ] 1947 1786 ] qed. 1948 1949 lemma lset_difference_nil : ∀A,s. lset_difference A s [ ] = s. #A #s elim s //1950 #hd #tl #Hind >lset_difference_unfold normalize in match (memb ???); normalize nodelta >Hind @refl1951 qed.1952 1787 1953 1788 lemma lset_mem_inclusion_mem : … … 2049 1884 [ 1: %2 @Hind @Hmem 2050 1885 | 2: @Hind @Hmem ] ] ] 2051 ] qed. 1886 ] qed. 1887 1888 lemma lset_disjoint_dec : 1889 ∀A : DeqSet. 1890 ∀s1,elt,s2. 1891 mem ? elt s1 ∨ mem ? elt (lset_difference A (elt :: s2) s1). 1892 #A #s1 #elt #s2 1893 @(match elt ∈ s1 return λx. ((elt ∈ s1) = x) → ? 1894 with 1895 [ false ⇒ λHA. ? 1896 | true ⇒ λHA. ? ] (refl ? (elt ∈ s1))) 1897 [ 1: lapply (memb_to_mem … HA) #Hmem 1898 %1 @Hmem 1899 | 2: %2 elim s1 in HA; 1900 [ 1: #_ whd %1 @refl 1901 | 2: #hd1 #tl1 #Hind normalize in ⊢ (% → ?); 1902 >lset_difference_unfold 1903 >lset_difference_unfold2 1904 lapply (eqb_true ? elt hd1) whd in match (memb ???) in ⊢ (? → ? → %); 1905 cases (elt==hd1) normalize nodelta 1906 [ 1: #_ #Habsurd destruct 1907 | 2: #HA #HB >HB normalize nodelta %1 @refl ] ] ] 1908 qed. 1909 1910 lemma mem_filter : ∀A : DeqSet. ∀l,elt1,elt2. 1911 mem A elt1 (filter A (λx:A.¬x==elt2) l) → mem A elt1 l. 1912 #A #l elim l try // #hd #tl #Hind #elt1 #elt2 /2 by lset_mem_inclusion_mem/ 1913 qed. 1914 1915 lemma lset_inclusion_difference_aux : 1916 ∀A : DeqSet. ∀s1,s2. 1917 lset_inclusion A s1 s2 → 1918 (lset_eq A s2 (s1@lset_difference A s2 s1)). 1919 #A #s1 1920 @(WF_ind ????? (filtered_list_wf A s1)) 1921 * 1922 [ 1: #_ #_ #s2 #_ >nil_append >lset_difference_empty @reflexive_lset_eq 1923 | 2: #hd1 #tl1 #Hwf #Hind #s2 * #Hmem #Hincl 1924 lapply (Hind (filter ? (λx.¬x==hd1) tl1) ?) 1925 [ 1: whd normalize 1926 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta @refl ] 1927 #Hind_wf 1928 elim (list_mem_split ??? Hmem) #s2A * #s2B #Heq >Heq 1929 >cons_to_append in ⊢ (???%); >associative_append 1930 >lset_difference_unfold2 1931 >nil_append 1932 >lset_remove_split >lset_remove_split 1933 normalize in match (lset_remove ? [hd1] hd1); 1934 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta 1935 >nil_append <lset_remove_split >lset_difference_lset_remove_commute 1936 lapply (Hind_wf (lset_remove A (s2A@s2B) hd1) ?) 1937 [ 1: lapply (lset_inclusion_remove … Hincl hd1) 1938 >Heq @lset_inclusion_eq2 1939 >lset_remove_split >lset_remove_split >lset_remove_split 1940 normalize in match (lset_remove ? [hd1] hd1); 1941 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta 1942 >nil_append @reflexive_lset_eq ] 1943 #Hind >lset_difference_lset_remove_commute in Hind; <lset_remove_split #Hind 1944 @lset_eq_concrete_to_lset_eq 1945 lapply (lset_eq_to_lset_eq_concrete … (cons_monotonic_eq … Hind hd1)) #Hindc 1946 @(square_lset_eq_concrete ????? Hindc) -Hindc -Hind 1947 [ 1: @(transitive_lset_eq_concrete ?? ([hd1]@s2A@s2B) (s2A@[hd1]@s2B)) 1948 [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete 1949 | 1: @lset_eq_to_lset_eq_concrete @lset_eq_filter ] 1950 | 2: @lset_eq_to_lset_eq_concrete @(transitive_lset_eq A … (lset_eq_filter ? ? hd1 …)) 1951 elim (s2A@s2B) 1952 [ 1: normalize in match (lset_difference ???); @reflexive_lset_eq 1953 | 2: #hd2 #tl2 #Hind >lset_difference_unfold >lset_difference_unfold 1954 @(match (hd2∈filter A (λx:A.¬x==hd1) tl1) 1955 return λx. ((hd2∈filter A (λx:A.¬x==hd1) tl1) = x) → ? 1956 with 1957 [ false ⇒ λH. ? 1958 | true ⇒ λH. ? 1959 ] (refl ? (hd2∈filter A (λx:A.¬x==hd1) tl1))) normalize nodelta 1960 [ 1: lapply (memb_to_mem … H) #Hfilter >(mem_to_memb … (mem_filter … Hfilter)) 1961 normalize nodelta @Hind 1962 | 2: @(match (hd2∈tl1) 1963 return λx. ((hd2∈tl1) = x) → ? 1964 with 1965 [ false ⇒ λH'. ? 1966 | true ⇒ λH'. ? 1967 ] (refl ? (hd2∈tl1))) normalize nodelta 1968 [ 1: (* We have hd2 = hd1 *) 1969 cut (hd2 = hd1) 1970 [ elim tl1 in H H'; 1971 [ 1: normalize #_ #Habsurd destruct (Habsurd) 1972 | 2: #hdtl1 #tltl1 #Hind normalize in ⊢ (% → % → ?); 1973 lapply (eqb_true ? hdtl1 hd1) 1974 cases (hdtl1==hd1) normalize nodelta 1975 [ 1: * #H >(H (refl ??)) #_ 1976 lapply (eqb_true ? hd2 hd1) 1977 cases (hd2==hd1) normalize nodelta * 1978 [ 1: #H' >(H' (refl ??)) #_ #_ #_ @refl 1979 | 2: #_ #_ @Hind ] 1980 | 2: #_ normalize lapply (eqb_true ? hd2 hdtl1) 1981 cases (hd2 == hdtl1) normalize nodelta * 1982 [ 1: #_ #_ #Habsurd destruct (Habsurd) 1983 | 2: #_ #_ @Hind ] ] ] ] 1984 #Heq_hd2hd1 destruct (Heq_hd2hd1) 1985 @lset_eq_concrete_to_lset_eq lapply (lset_eq_to_lset_eq_concrete … Hind) 1986 #Hind' @(square_lset_eq_concrete … Hind') 1987 [ 2: @lset_refl 1988 | 1: >cons_to_append >cons_to_append in ⊢ (???%); 1989 @(transitive_lset_eq_concrete … ([hd1]@[hd1]@tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1))) 1990 [ 1: @lset_eq_to_lset_eq_concrete @symmetric_lset_eq @lset_eq_contract 1991 | 2: >(cons_to_append … hd1 (lset_difference ???)) 1992 @lset_eq_concrete_cons >nil_append >nil_append 1993 @symmetric_lset_eq_concrete @switch_lset_eq_concrete ] ] 1994 | 2: @(match hd2 == hd1 1995 return λx. ((hd2 == hd1) = x) → ? 1996 with 1997 [ true ⇒ λH''. ? 1998 | false ⇒ λH''. ? 1999 ] (refl ? (hd2 == hd1))) 2000 [ 1: whd in match (lset_remove ???) in ⊢ (???%); 2001 >H'' normalize nodelta >((proj1 … (eqb_true …)) H'') 2002 @(transitive_lset_eq … Hind) 2003 @(transitive_lset_eq … (hd1::hd1::tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1))) 2004 [ 2: @lset_eq_contract ] 2005 @lset_eq_concrete_to_lset_eq @lset_eq_concrete_cons 2006 @switch_lset_eq_concrete 2007 | 2: whd in match (lset_remove ???) in ⊢ (???%); 2008 >H'' >notb_false normalize nodelta 2009 @lset_eq_concrete_to_lset_eq 2010 lapply (lset_eq_to_lset_eq_concrete … Hind) #Hindc 2011 lapply (lset_eq_concrete_cons … Hindc hd2) #Hindc' -Hindc 2012 @(square_lset_eq_concrete … Hindc') 2013 [ 1: @symmetric_lset_eq_concrete 2014 >cons_to_append >cons_to_append in ⊢ (???%); 2015 >(cons_to_append … hd2) >(cons_to_append … hd1) in ⊢ (???%); 2016 @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?) 2017 | 2: @symmetric_lset_eq_concrete @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?) 2018 ] 2019 ] 2020 ] 2021 ] 2022 ] 2023 ] 2024 ] qed. 2025 2026 lemma lset_inclusion_difference : 2027 ∀A : DeqSet. 2028 ∀s1,s2 : lset (carr A). 2029 lset_inclusion ? s1 s2 → 2030 ∃s2'. lset_eq ? s2 (s1 @ s2') ∧ 2031 lset_disjoint ? s1 s2' ∧ 2032 lset_eq ? s2' (lset_difference ? s2 s1). 2033 #A #s1 #s2 #Hincl %{(lset_difference A s2 s1)} @conj try @conj 2034 [ 1: @lset_inclusion_difference_aux @Hincl 2035 | 2: /2 by lset_difference_disjoint/ 2036 | 3,4: @reflexive_lset_inclusion ] 2037 qed. 2038 2039 2040 lemma memory_eq_to_memory_ext_pre : 2041 ∀m1,m1',m2,writeable. 2042 memory_eq m1 m1' → 2043 sr_memext m1' m2 writeable → 2044 sr_memext m1 m2 writeable. 2045 #m1 #m1' #m2 #writeable #Heq #Hext 2046 lapply (memory_eq_to_mem_ext … Heq) #Hext' 2047 @(memory_ext_transitive … Hext' Hext) 2048 qed. 2049 2050 lemma memory_eq_to_memory_ext_post : 2051 ∀m1,m2,m2',writeable. 2052 memory_eq m2' m2 → 2053 sr_memext m1 m2' writeable → 2054 sr_memext m1 m2 writeable. 2055 #m1 #m2 #m2' #writeable #Heq #Hext 2056 lapply (memory_eq_to_mem_ext … Heq) #Hext' 2057 lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H 2058 qed. 2059 2052 2060 2053 2061 lemma memext_free_extended_environment : … … 2158 2166 ] qed. 2159 2167 2168 (* --------------------------------------------------------------------------- *) 2169 (* Some lemmas allowing to reason on writes to extended memories. *) 2170 2171 (* Writing in the extended part of the memory preserves the extension (that's the point) *) 2172 lemma bestorev_writeable_memory_ext : 2173 ∀m1,m2,writeable. 2174 ∀Hext:sr_memext m1 m2 writeable. 2175 ∀wb,wo,v. meml ? wb writeable → 2176 ∀m2'.bestorev m2 (mk_pointer wb wo) v = Some ? m2' → 2177 sr_memext m1 m2' writeable. 2178 #m1 * #contents2 #nextblock2 #Hpos2 #writeable #Hext #wb #wo #v #Hmem #m2' 2179 whd in ⊢ ((??%?) → ?); 2180 lapply (me_writeable_valid … Hext ? Hmem) * whd in ⊢ (% → ?); #Hlt 2181 >(Zlt_to_Zltb_true … Hlt) normalize nodelta #Hnonempty2 #H 2182 lapply (if_opt_inversion ???? H) -H * #Hzltb 2183 lapply (andb_inversion … Hzltb) * #Hleb #Hltb -Hzltb 2184 #Heq destruct % 2185 [ 1: #b #Hnonempty1 2186 lapply (me_nonempty … Hext b Hnonempty1) * * #Hvalid_b #Hnonempty_b 2187 #Heq @conj 2188 [ 1: % whd whd in Hvalid_b; try @Hvalid_b 2189 normalize cases (block_region b) normalize nodelta 2190 cases (block_region wb) normalize nodelta try // 2191 @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta 2192 try // 2193 | 2: whd in ⊢ (??%%); 2194 @(eq_block_elim … b wb) normalize nodelta // #Heq_b_wb 2195 lapply (me_not_writeable … Hext b Hnonempty1) destruct (Heq_b_wb) 2196 * #H @(False_ind … (H Hmem)) ] 2197 | 2: #b #Hmem_writeable 2198 lapply (me_writeable_valid … Hext … Hmem_writeable) #H % 2199 [ 1: normalize cases H // 2200 | 2: cases H normalize #Hb_lt #Hb_nonempty2 2201 cases (block_region b) 2202 cases (block_region wb) normalize nodelta 2203 // 2204 @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta 2205 // ] 2206 | 3: #b #Hnonempty 2207 lapply (me_not_writeable … Hext … Hnonempty) // 2208 ] qed. 2209 2210 (* If we manage to write in a block, then it is nonempty *) 2211 lemma bestorev_success_nonempty : 2212 ∀m,wb,wo,v,m'. 2213 bestorev m (mk_pointer wb wo) v = Some ? m' → 2214 nonempty_block m wb. 2215 #m #wb #wo #v #m' normalize #Hstore 2216 cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H 2217 cases (if_opt_inversion ???? H) -H #nonempty #H % 2218 [ 1: whd @Zltb_true_to_Zlt assumption 2219 | 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H' 2220 cut (Zleb (low (blocks m wb)) z = true) 2221 [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ] 2222 #Hleb >Hleb in H'; normalize nodelta #Hlt 2223 lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt) 2224 /2 by Zle_to_Zlt_to_Zlt/ 2225 ] qed. 2226 2227 (* If we manage to write in a block, it is still non-empty after the write *) 2228 lemma bestorev_success_nonempty2 : 2229 ∀m,wb,wo,v,m'. 2230 bestorev m (mk_pointer wb wo) v = Some ? m' → 2231 nonempty_block m' wb. 2232 #m #wb #wo #v #m' normalize #Hstore 2233 cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H 2234 cases (if_opt_inversion ???? H) -H #nonempty #H % 2235 [ 1: whd destruct @Zltb_true_to_Zlt assumption 2236 | 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H' 2237 cut (Zleb (low (blocks m wb)) z = true) 2238 [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ] 2239 #Hleb >Hleb in H'; normalize nodelta #Hlt 2240 lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt) 2241 destruct cases (block_region wb) normalize >eqZb_z_z normalize 2242 /2 by Zle_to_Zlt_to_Zlt/ 2243 ] qed. 2244 2245 (* A nonempty block stays nonempty after a write. *) 2246 lemma nonempty_block_update_ok : 2247 ∀m,b,wb,offset,v. 2248 nonempty_block m b → 2249 nonempty_block 2250 (mk_mem 2251 (update_block ? wb 2252 (mk_block_contents (low (blocks m wb)) (high (blocks m wb)) 2253 (update beval offset v (contents (blocks m wb)))) (blocks m)) 2254 (nextblock m) (nextblock_pos m)) b. 2255 #m #b #wb #offset #v * #Hvalid #Hnonempty % // 2256 cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize 2257 cases br normalize nodelta cases wbr normalize nodelta // 2258 @(eqZb_elim … bid wbid) // #Heq #Hlt normalize // 2259 qed. 2260 2261 lemma nonempty_block_update_ok2 : 2262 ∀m,b,wb,offset,v. 2263 nonempty_block 2264 (mk_mem 2265 (update_block ? wb 2266 (mk_block_contents (low (blocks m wb)) (high (blocks m wb)) 2267 (update beval offset v (contents (blocks m wb)))) (blocks m)) 2268 (nextblock m) (nextblock_pos m)) b → 2269 nonempty_block m b. 2270 #m #b #wb #offset #v * #Hvalid #Hnonempty % // 2271 cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize 2272 cases br normalize nodelta cases wbr normalize nodelta // 2273 @(eqZb_elim … bid wbid) // #Heq #Hlt normalize // 2274 qed. 2275 2276 (* Writing in the non-extended part of the memory preserves the extension as long 2277 * as it's done identically in both memories. *) 2278 lemma bestorev_not_writeable_memory_ext : 2279 ∀m1,m2,writeable. 2280 ∀Hext:sr_memext m1 m2 writeable. 2281 ∀wb,wo,v. 2282 ∀m1'. bestorev m1 (mk_pointer wb wo) v = Some ? m1' → 2283 ∃m2'. bestorev m2 (mk_pointer wb wo) v = Some ? m2' ∧ 2284 sr_memext m1' m2' writeable. 2285 #m1 #m2 #writeable #Hext #wb #wo #v #m1' #Hstore1 2286 lapply (bestorev_success_nonempty … Hstore1) #Hwb_nonempty 2287 cases (me_nonempty … Hext … Hwb_nonempty) #Hwb_nonempty2 #Hblocks_eq 2288 cut (∃m2'. bestorev m2 (mk_pointer wb wo) v=Some mem m2') 2289 [ cases Hwb_nonempty2 #Hwb_valid #Hnonempty normalize 2290 normalize in Hwb_valid; >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta 2291 whd in Hstore1:(??%%); normalize 2292 cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H 2293 cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H 2294 cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1 2295 >Hblocks_eq in Hleb1 Hltb1 ⊢ %; #Hleb1 #Hltb1 >Hleb1 >Hltb1 2296 normalize nodelta /2 by ex_intro/ ] 2297 * #m2' #Hstore2 %{m2'} @conj try assumption 2298 whd in Hstore1:(??%%); 2299 whd in Hstore2:(??%%); 2300 cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H 2301 cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H 2302 cases (if_opt_inversion ???? Hstore2) -Hstore2 #block_valid2 #H 2303 cases (if_opt_inversion ???? H) #Hin_bounds2 #Hm2' -H 2304 cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1 2305 cases (andb_inversion … Hin_bounds2) #Hleb2 #Hltb2 -Hin_bounds2 2306 cut (valid_pointer m1 (mk_pointer wb wo)) 2307 [ 1: normalize >block_valid1 normalize nodelta >Hleb1 normalize nodelta 2308 >Hltb1 @I ] 2309 #Hvalid 2310 lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_in_writeable 2311 destruct % 2312 [ 1: #b #Hnonempty lapply (me_nonempty … Hext … (nonempty_block_update_ok2 … Hnonempty)) * #HA #HB 2313 @conj 2314 [ 1: @nonempty_block_update_ok // 2315 | 2: normalize cases b in HB; #br #bid cases wb #wbr #wbid 2316 cases br cases wbr normalize nodelta 2317 @(eqZb_elim … bid wbid) normalize nodelta // 2318 #Hid_eq >Hid_eq #Hblock_eq >Hblock_eq @refl ] 2319 | 2: #b #Hmem lapply (me_writeable_valid … Hext … Hmem) @nonempty_block_update_ok 2320 | 3: #b #Hnonempty lapply (nonempty_block_update_ok2 … Hnonempty) 2321 @(me_not_writeable … Hext) 2322 ] qed. 2323 2324 (* If we successfuly store something in the first memory, then we can store it in the 2325 * second one and the memory extension is preserved. *) 2326 lemma memext_store_value_of_type : 2327 ∀m, m_ext, m', writeable, ty, loc, off, v. 2328 sr_memext m m_ext writeable → 2329 store_value_of_type ty m loc off v = Some ? m' → 2330 ∃m_ext'. store_value_of_type ty m_ext loc off v = Some ? m_ext' ∧ 2331 sr_memext m' m_ext' writeable. 2332 #m #m_ext #m' #writeable #ty #loc #off #v #Hext 2333 (* case analysis on access mode of [ty] *) 2334 cases ty 2335 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 2336 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] 2337 whd in ⊢ ((??%?) → (?%?)); 2338 [ 1,5,6,7,8: #Habsurd destruct ] 2339 whd in ⊢ (? → (??(λ_.?(??%?)?))); 2340 lapply loc lapply off lapply Hext lapply m_ext lapply m lapply m' -loc -off -Hext -m_ext -m -m' 2341 elim (fe_to_be_values ??) 2342 [ 1,3,5,7: #m' #m #m_ext #Hext #off #loc normalize in ⊢ (% → ?); #Heq destruct (Heq) %{m_ext} @conj normalize // 2343 | 2,4,6,8: #hd #tl #Hind #m' #m #m_ext #Hext #off #loc whd in ⊢ ((??%?) → ?); #H 2344 cases (some_inversion ????? H) #m'' * #Hstore_eq #Hstoren_eq 2345 lapply (bestorev_not_writeable_memory_ext … Hext … Hstore_eq) 2346 * #m_ext'' * #Hstore_eq2 #Hext2 2347 lapply (Hind … Hext2 … Hstoren_eq) -Hind * #m_ext' * 2348 #Hstoren' #Hext3 2349 %{m_ext'} @conj try assumption 2350 whd in ⊢ (??%%); >Hstore_eq2 normalize nodelta 2351 @Hstoren' 2352 ] qed. 2353 2354 lemma memext_store_value_of_type' : 2355 ∀m, m_ext, m', writeable, ty, ptr, v. 2356 sr_memext m m_ext writeable → 2357 store_value_of_type' ty m ptr v = Some ? m' → 2358 ∃m_ext'. store_value_of_type' ty m_ext ptr v = Some ? m_ext' ∧ 2359 sr_memext m' m_ext' writeable. 2360 #m #m_ext #m' #writeable #ty #p #v #Hext cases p #b #o 2361 @memext_store_value_of_type @Hext qed. 2160 2362 2161 2363 (* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if … … 2186 2388 2187 2389 (* Simulation relations. *) 2188 inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝2189 | swc_stop : ∀fvs.2190 switch_cont_sim fvs Kstop Kstop2191 | swc_seq : ∀ fvs,s,k,k',u,result.2390 inductive switch_cont_sim : list (ident × type) → cont → cont → Prop ≝ 2391 | swc_stop : 2392 ∀new_vars. switch_cont_sim new_vars Kstop Kstop 2393 | swc_seq : ∀s,k,k',u,s',new_vars. 2192 2394 fresh_for_statement s u → 2193 switch_cont_sim fvs k k' → 2194 switch_removal s fvs u = Some ? result → 2195 switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k') 2196 | swc_while : ∀fvs,e,s,k,k',u,result. 2395 switch_cont_sim new_vars k k' → 2396 s' = ret_st ? (switch_removal s u) → 2397 lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → 2398 switch_cont_sim new_vars (Kseq s k) (Kseq s' k') 2399 | swc_while : ∀e,s,k,k',u,s',new_vars. 2197 2400 fresh_for_statement (Swhile e s) u → 2198 switch_cont_sim fvs k k' → 2199 switch_removal s fvs u = Some ? result → 2200 switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k') 2201 | swc_dowhile : ∀fvs,e,s,k,k',u,result. 2401 switch_cont_sim new_vars k k' → 2402 s' = ret_st ? (switch_removal s u) → 2403 lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → 2404 switch_cont_sim new_vars (Kwhile e s k) (Kwhile e s' k') 2405 | swc_dowhile : ∀e,s,k,k',u,s',new_vars. 2202 2406 fresh_for_statement (Sdowhile e s) u → 2203 switch_cont_sim fvs k k' → 2204 switch_removal s fvs u = Some ? result → 2205 switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k') 2206 | swc_for1 : ∀fvs,e,s1,s2,k,k',u,result. 2407 switch_cont_sim new_vars k k' → 2408 s' = ret_st ? (switch_removal s u) → 2409 lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → 2410 switch_cont_sim new_vars (Kdowhile e s k) (Kdowhile e s' k') 2411 | swc_for1 : ∀e,s1,s2,k,k',u,s',new_vars. 2207 2412 fresh_for_statement (Sfor Sskip e s1 s2) u → 2208 switch_cont_sim fvs k k' → 2209 switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result → 2210 switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k') 2211 | swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2. 2413 switch_cont_sim new_vars k k' → 2414 s' = (ret_st ? (switch_removal (Sfor Sskip e s1 s2) u)) → 2415 lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → 2416 switch_cont_sim new_vars (Kseq (Sfor Sskip e s1 s2) k) (Kseq s' k') 2417 | swc_for2 : ∀e,s1,s2,k,k',u,result1,result2,new_vars. 2212 2418 fresh_for_statement (Sfor Sskip e s1 s2) u → 2213 switch_cont_sim fvs k k' → 2214 switch_removal s1 fvs u = Some ? result1 → 2215 switch_removal s2 fvs (ret_u ? result1) = Some ? result2 → 2216 switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k') 2217 | swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2. 2419 switch_cont_sim new_vars k k' → 2420 result1 = ret_st ? (switch_removal s1 u) → 2421 result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) → 2422 lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → 2423 switch_cont_sim new_vars (Kfor2 e s1 s2 k) (Kfor2 e result1 result2 k') 2424 | swc_for3 : ∀e,s1,s2,k,k',u,result1,result2,new_vars. 2218 2425 fresh_for_statement (Sfor Sskip e s1 s2) u → 2219 switch_cont_sim fvs k k' → 2220 switch_removal s1 fvs u = Some ? result1 → 2221 switch_removal s2 fvs (ret_u ? result1) = Some ? result2 -> 2222 switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k') 2223 | swc_switch : ∀fvs,k,k'. 2224 switch_cont_sim fvs k k' → 2225 switch_cont_sim fvs (Kswitch k) (Kswitch k') 2226 | swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *) 2227 switch_cont_sim fvs k k' → 2228 (* /!\ Update [en] with [fvs'] ... *) 2229 switch_cont_sim 2230 (map … (fst ??) (\snd (function_switch_removal f))) 2426 switch_cont_sim new_vars k k' → 2427 result1 = ret_st ? (switch_removal s1 u) → 2428 result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) → 2429 lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → 2430 switch_cont_sim new_vars (Kfor3 e s1 s2 k) (Kfor3 e result1 result2 k') 2431 | swc_switch : ∀k,k',new_vars. 2432 switch_cont_sim new_vars k k' → 2433 switch_cont_sim new_vars (Kswitch k) (Kswitch k') 2434 | swc_call : ∀en,en',r,f,k,k',old_vars,new_vars. (* Warning: possible caveat with environments here. *) 2435 switch_cont_sim old_vars k k' → 2436 old_vars = \snd (function_switch_removal f) → 2437 disjoint_extension en en' old_vars → 2438 switch_cont_sim 2439 new_vars 2231 2440 (Kcall r f en k) 2232 2441 (Kcall r (\fst (function_switch_removal f)) en' k'). 2233 2234 (*2235 en' = exec_alloc_variables en m (\snd (function_switch_removal f))2236 TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc2237 variable dans en'.2238 2239 1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que2240 dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est2241 de savoir que :2242 si je lookup une variable générée à partir d'un univers frais dans l'environement en',2243 alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step,2244 et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s"2245 et à etre "(function_switch_removal f)-contained".2246 2247 2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup2248 et l'update n'altèrent pas le comportement du reste du programme.2249 2250 relation : si un statement S0 est inclus dans un statement S1, alors les variables générées2251 depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1.2252 en particulier, si u est frais pour S1 u est frais pour S0.2253 2254 Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique2255 "environment_extension en en' (\fst (\fst (switch_removal s u)))"2256 2257 ---------------------------------------------------------------2258 . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction2259 et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération.2260 on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner2261 en argument les freshgens qui correspondent à ce que la fonction switch_removal fait.2262 *)2263 2442 2264 2443 record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { … … 2277 2456 (* current statement *) 2278 2457 ∀sss_statement : statement. 2279 (* statement after transformation *)2280 ∀sss_result : swret statement.2281 2458 (* label universe *) 2282 2459 ∀sss_lu : universe SymbolTag. … … 2309 2486 (* The extended environment does not interfer with the old one. *) 2310 2487 ∀sss_env_hyp : disjoint_extension sss_env sss_env_ext sss_new_vars. 2488 (* Extension blocks are writeable. *) 2489 ∀sss_ext_write : lset_inclusion ? (lset_difference ? (blocks_of_env sss_env_ext) (blocks_of_env sss_env)) sss_writeable. 2311 2490 (* conversion of the current statement, using the variables produced during the conversion of the current function *) 2312 ∀sss_result_hyp : switch_removal sss_statement (map ?? (fst ??) sss_new_vars) sss_lu = Some ? sss_result. 2491 ∀sss_result_rec. 2492 ∀sss_result_hyp : switch_removal sss_statement sss_lu = sss_result_rec. 2493 ∀sss_result. 2494 sss_result = ret_st ? sss_result_rec → 2495 (* inclusion of the locally produced new variables in the global new variables *) 2496 lset_inclusion ? (ret_vars ? sss_result_rec) sss_new_vars → 2313 2497 (* simulation between the continuations before and after conversion. *) 2314 ∀sss_k_hyp : switch_cont_sim (map ?? (fst ??) sss_new_vars) sss_k sss_k_ext.2498 ∀sss_k_hyp : switch_cont_sim sss_new_vars sss_k sss_k_ext. 2315 2499 ext_fresh_for_genv sss_new_vars ge → 2316 2500 switch_state_sim 2317 2501 ge 2318 2502 (State sss_func sss_statement sss_k sss_env sss_m) 2319 (State sss_func_tr (ret_st … sss_result) sss_k_ext sss_env_ext sss_m_ext) 2320 | sws_callstate : ∀vars, fd,args,k,k',m. 2321 switch_cont_sim vars k k' → 2322 switch_state_sim ge (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m) 2323 | sws_returnstate : 2324 ∀ssr_vars. 2503 (State sss_func_tr sss_result sss_k_ext sss_env_ext sss_m_ext) 2504 | sws_callstate : 2505 ∀ssc_fd. 2506 ∀ssc_args. 2507 ∀ssc_k. 2508 ∀ssc_k_ext. 2509 ∀ssc_m. 2510 ∀ssc_m_ext. 2511 ∀ssc_writeable. 2512 ∀ssc_mem_hyp : sr_memext ssc_m ssc_m_ext ssc_writeable. 2513 (match ssc_fd with 2514 [ CL_Internal ssc_f ⇒ 2515 switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext 2516 | _ ⇒ True ]) → 2517 switch_state_sim ge (Callstate ssc_fd ssc_args ssc_k ssc_m) 2518 (Callstate (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext) 2519 | sws_returnstate : 2325 2520 ∀ssr_result. 2326 2521 ∀ssr_k : cont. … … 2330 2525 ∀ssr_writeable : list block. 2331 2526 ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext ssr_writeable. 2527 ∀ssr_vars. 2332 2528 switch_cont_sim ssr_vars ssr_k ssr_k_ext → 2333 2529 switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext) … … 2335 2531 switch_state_sim ge (Finalstate r) (Finalstate r). 2336 2532 2337 lemma call_cont_swremoval : ∀ fv,k,k'.2338 switch_cont_sim fvk k' →2339 switch_cont_sim fv(call_cont k) (call_cont k').2340 # fv #k0 #k0'#K elim K /2/2533 lemma call_cont_swremoval : ∀k,k',vars. 2534 switch_cont_sim vars k k' → 2535 switch_cont_sim vars (call_cont k) (call_cont k'). 2536 #k0 #k0' #vars #K elim K /2/ 2341 2537 qed. 2342 2538 … … 2444 2640 qed. 2445 2641 2446 2447 (* Conservation of the smenantics of binary operators under memory extensions*)2642 (* Conservation of the semantics of binary operators under memory extensions. 2643 Tried to factorise it a bit but the play with indexes just becomes too messy. *) 2448 2644 lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,writeable. 2449 2645 ∀Hext:sr_memext m1 m2 writeable. ∀res. … … 2454 2650 try // 2455 2651 whd in match (sem_binary_operation ??????); 2652 lapply (me_valid_pointers … Hmemext) 2653 lapply (me_not_writeable_ptr … Hmemext) 2456 2654 elim m1 in Hmemext; #contents1 #nextblocks1 #Hnextpos1 2457 2655 elim m2 #contents2 #nextblocks2 #Hnextpos2 2458 * #H ptrsim #writeable #Hvalid #Hdisjoint #Hvalid_cons2656 * #Hnonempty #Hwriteable #Hnot_writeable #Hnot_writeable_ptr #Hvalid 2459 2657 whd in match (sem_cmp ??????); 2460 2658 whd in match (sem_cmp ??????); 2461 [ 1 : cases (classify_cmp (typeof e1) (typeof e2))2659 [ 1,2: cases (classify_cmp (typeof e1) (typeof e2)) 2462 2660 normalize nodelta 2463 [ 1 : #sz #sg try //2464 | 2 : #opt #ty2661 [ 1,5: #sz #sg try // 2662 | 2,6: #opt #ty 2465 2663 cases v1 normalize nodelta 2466 [ 1 : | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]2467 [ 1,2,3 : #Habsurd destruct (Habsurd)2468 | 4: #H @H ]2664 [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ] 2665 [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) 2666 | 7,8: #H @H ] 2469 2667 cases v2 normalize nodelta 2470 [ 1 : | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]2471 [ 1,2,3 : #Habsurd destruct (Habsurd)2472 | 4: #H @H ]2473 lapply (Hvalid _consptr)2668 [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ] 2669 [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) 2670 | 7,8: #H @H ] 2671 lapply (Hvalid ptr) 2474 2672 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 2475 [ 2 : >andb_lsimpl_false normalize nodelta #_#Habsurd destruct (Habsurd) ]2476 #Hvalid >(Hvalid(refl ??))2477 lapply (Hvalid _consptr')2673 [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] 2674 #Hvalid' >(Hvalid' (refl ??)) 2675 lapply (Hvalid ptr') 2478 2676 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 2479 [ 2 : >andb_lsimpl_true #_normalize nodelta #Habsurd destruct (Habsurd) ]2480 #H' >(H' (refl ??)) >andb_lsimpl_true #Hres @Hres2481 | 3 : #fsz #H @H2482 | 4 : #ty1 #ty2 #H @H ]2483 | 2: cases (classify_cmp (typeof e1) (typeof e2))2677 [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] 2678 #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H 2679 | 3,7: #fsz #H @H 2680 | 4,8: #ty1 #ty2 #H @H ] 2681 | 3,4: cases (classify_cmp (typeof e1) (typeof e2)) 2484 2682 normalize nodelta 2485 [ 1 : #sz #sg try //2486 | 2 : #opt #ty2683 [ 1,5: #sz #sg try // 2684 | 2,6: #opt #ty 2487 2685 cases v1 normalize nodelta 2488 [ 1 : | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]2489 [ 1,2,3 : #Habsurd destruct (Habsurd)2490 | 4: #H @H ]2686 [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ] 2687 [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) 2688 | 7,8: #H @H ] 2491 2689 cases v2 normalize nodelta 2492 [ 1 : | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]2493 [ 1,2,3 : #Habsurd destruct (Habsurd)2494 | 4: #H @H ]2495 lapply (Hvalid _consptr)2690 [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ] 2691 [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) 2692 | 7,8: #H @H ] 2693 lapply (Hvalid ptr) 2496 2694 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 2497 [ 2 :#_ normalize #Habsurd destruct (Habsurd) ]2498 #H >(H(refl ??))2499 lapply (Hvalid _consptr')2695 [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] 2696 #Hvalid' >(Hvalid' (refl ??)) 2697 lapply (Hvalid ptr') 2500 2698 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 2501 [ 2 : #_ normalize#Habsurd destruct (Habsurd) ]2502 #H' >(H' (refl ??)) #Hok @Hok2503 | 3 : #fsz #H @H2504 | 4 : #ty1 #ty2 #H @H ]2505 | 3: cases (classify_cmp (typeof e1) (typeof e2))2699 [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] 2700 #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H 2701 | 3,7: #fsz #H @H 2702 | 4,8: #ty1 #ty2 #H @H ] 2703 | 5,6: cases (classify_cmp (typeof e1) (typeof e2)) 2506 2704 normalize nodelta 2507 [ 1 : #sz #sg try //2508 | 2 : #opt #ty2705 [ 1,5: #sz #sg try // 2706 | 2,6: #opt #ty 2509 2707 cases v1 normalize nodelta 2510 [ 1 : | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]2511 [ 1,2,3 : #Habsurd destruct (Habsurd)2512 | 4: #H @H ]2708 [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ] 2709 [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) 2710 | 7,8: #H @H ] 2513 2711 cases v2 normalize nodelta 2514 [ 1 : | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]2515 [ 1,2,3 : #Habsurd destruct (Habsurd)2516 | 4: #H @H ]2517 lapply (Hvalid _consptr)2712 [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ] 2713 [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd) 2714 | 7,8: #H @H ] 2715 lapply (Hvalid ptr) 2518 2716 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 2519 [ 2 :#_ normalize #Habsurd destruct (Habsurd) ]2520 #H >(H(refl ??))2521 lapply (Hvalid _consptr')2717 [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] 2718 #Hvalid' >(Hvalid' (refl ??)) 2719 lapply (Hvalid ptr') 2522 2720 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 2523 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 2524 #H' >(H' (refl ??)) #Hok @Hok 2525 | 3: #fsz #H @H 2526 | 4: #ty1 #ty2 #H @H ] 2527 | 4: cases (classify_cmp (typeof e1) (typeof e2)) 2528 normalize nodelta 2529 [ 1: #sz #sg #H @H 2530 | 2: #opt #ty 2531 cases v1 normalize nodelta 2532 [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] 2533 [ 1,2,3: #Habsurd destruct (Habsurd) 2534 | 4: #H @H ] 2535 cases v2 normalize nodelta 2536 [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] 2537 [ 1,2,3: #Habsurd destruct (Habsurd) 2538 | 4: #H @H ] 2539 lapply (Hvalid_cons ptr) 2540 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 2541 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 2542 #H >(H (refl ??)) 2543 lapply (Hvalid_cons ptr') 2544 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 2545 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 2546 #H' >(H' (refl ??)) #Hok @Hok 2547 | 3: #fsz #H @H 2548 | 4: #ty1 #ty2 #H @H ] 2549 | 5: cases (classify_cmp (typeof e1) (typeof e2)) 2550 normalize nodelta 2551 [ 1: #sz #sg #H @H 2552 | 2: #opt #ty 2553 cases v1 normalize nodelta 2554 [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] 2555 [ 1,2,3: #Habsurd destruct (Habsurd) 2556 | 4: #H @H ] 2557 cases v2 normalize nodelta 2558 [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] 2559 [ 1,2,3: #Habsurd destruct (Habsurd) 2560 | 4: #H @H ] 2561 lapply (Hvalid_cons ptr) 2562 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 2563 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 2564 #H >(H (refl ??)) 2565 lapply (Hvalid_cons ptr') 2566 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 2567 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 2568 #H' >(H' (refl ??)) #Hok @Hok 2569 | 3: #fsz #H @H 2570 | 4: #ty1 #ty2 #H @H ] 2571 | 6: cases (classify_cmp (typeof e1) (typeof e2)) 2572 normalize nodelta 2573 [ 1: #sz #sg #H @H 2574 | 2: #opt #ty 2575 cases v1 normalize nodelta 2576 [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ] 2577 [ 1,2,3: #Habsurd destruct (Habsurd) 2578 | 4: #H @H ] 2579 cases v2 normalize nodelta 2580 [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ] 2581 [ 1,2,3: #Habsurd destruct (Habsurd) 2582 | 4: #H @H ] 2583 lapply (Hvalid_cons ptr) 2584 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) 2585 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 2586 #H >(H (refl ??)) 2587 lapply (Hvalid_cons ptr') 2588 cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') 2589 [ 2: #_ normalize #Habsurd destruct (Habsurd) ] 2590 #H' >(H' (refl ??)) #Hok @Hok 2591 | 3: #fsz #H @H 2592 | 4: #ty1 #ty2 #H @H ] 2721 [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] 2722 #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H 2723 | 3,7: #fsz #H @H 2724 | 4,8: #ty1 #ty2 #H @H ] 2593 2725 ] qed. 2594 2726 … … 2749 2881 ] qed. 2750 2882 2883 lemma exec_lvalue_sim_aux : ∀ge,ge',env,env_ext,m,m_ext. 2884 (∀ed,ty. exec_lvalue_sim (exec_lvalue' ge env m ed ty) 2885 (exec_lvalue' ge' env_ext m_ext ed ty)) → 2886 ∀e. exec_lvalue_sim (exec_lvalue ge env m e) 2887 (exec_lvalue ge' env_ext m_ext e). 2888 #ge #ge' #env #env_ext #m #m_ext #H * #ed #ty @H qed. 2889 2890 lemma exec_expr_sim_to_exec_exprlist : 2891 ∀ge,ge',en1,en2,m1,m2. 2892 (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) → 2893 ∀l. res_sim ? (exec_exprlist ge en1 m1 l) (exec_exprlist ge' en2 m2 l). 2894 #ge #ge' #en1 #en2 #m1 #m2 #Hsim #l elim l 2895 [ 1: whd #a #Heq normalize in Heq ⊢ %; destruct @refl 2896 | 2: #hd #tl #Hind whd * #lv #tr whd in ⊢ ((??%?) → (??%?)); 2897 lapply (Hsim hd) 2898 cases (exec_expr ge en1 m1 hd) 2899 [ 2: #error normalize #_ #Habsurd destruct (Habsurd) 2900 | 1: * #v #vtr whd in ⊢ (% → ?); #Hsim >(Hsim ? (refl ??)) 2901 normalize nodelta 2902 cases (exec_exprlist ge en1 m1 tl) in Hind; 2903 [ 2: #error normalize #_ #Habsurd destruct (Habsurd) 2904 | 1: #a normalize #H >(H ? (refl ??)) #Heq destruct normalize @refl 2905 ] 2906 ] 2907 ] qed. 2908 2751 2909 (* 2752 2910 lemma related_globals_exprlist_simulation : ∀ge,ge',en,m. … … 2776 2934 (* The return type of any function is invariant under switch removal *) 2777 2935 lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f. 2778 #f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl 2936 #f elim f #ty #args #vars #body whd in match (function_switch_removal ?); 2937 cases (switch_removal ??) * #stmt #fvs #u @refl 2779 2938 qed. 2780 2939 2781 2940 (* Similar stuff for fundefs *) 2782 2941 lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd). 2783 * // qed. 2942 * // * #ty #args #vars #body whd in ⊢ (??%%); 2943 whd in match (function_switch_removal ?); cases (switch_removal ??) * #st #u 2944 normalize nodelta #u @refl 2945 qed. 2784 2946 2785 2947 (* … … 2820 2982 cases (leb e s) try /2/ 2821 2983 qed. 2984 2822 2985 (* 2823 2986 lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0). … … 2861 3024 qed.*) 2862 3025 2863 (* 2864 lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf. 3026 lemma simplify_is_not_skip : ∀s. s ≠ Sskip → ∀u. ∃pf. is_Sskip (ret_st ? (switch_removal s u)) = inr ?? pf. 2865 3027 * 2866 [ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip)) 2867 | 2: #e1 #e2 #u #_ 2868 whd in match (sw_rem ??); 2869 whd in match (is_Sskip ?); 2870 try /2 by refl, ex_intro/ 2871 | 3: #ret #f #args #u 2872 whd in match (sw_rem ??); 2873 whd in match (is_Sskip ?); 2874 try /2 by refl, ex_intro/ 2875 | 4: #s1 #s2 #u 2876 whd in match (sw_rem ??); 2877 whd in match (switch_removal ??); 2878 cases (switch_removal ? ?) * #a #b #c #d normalize nodelta 2879 cases (switch_removal ? ?) * #e #f #g normalize nodelta 2880 whd in match (is_Sskip ?); 2881 try /2 by refl, ex_intro/ 2882 | 5: #e #s1 #s2 #u #_ 2883 whd in match (sw_rem ??); 2884 whd in match (switch_removal ??); 2885 cases (switch_removal ? ?) * #a #b #c normalize nodelta 2886 cases (switch_removal ? ?) * #e #f #h normalize nodelta 2887 whd in match (is_Sskip ?); 2888 try /2 by refl, ex_intro/ 2889 | 6,7: #e #s #u #_ 2890 whd in match (sw_rem ??); 2891 whd in match (switch_removal ??); 2892 cases (switch_removal ? ?) * #a #b #c normalize nodelta 2893 whd in match (is_Sskip ?); 2894 try /2 by refl, ex_intro/ 2895 | 8: #s1 #e #s2 #s3 #u #_ 2896 whd in match (sw_rem ??); 2897 whd in match (switch_removal ??); 3028 [ 1: * #H @(False_ind … (H (refl ??))) ] 3029 try /2/ 3030 [ 1: #s1 #s2 #_ #u normalize 2898 3031 cases (switch_removal ? ?) * #a #b #c normalize nodelta 2899 3032 cases (switch_removal ? ?) * #e #f #g normalize nodelta 2900 cases (switch_removal ? ?) * #i #j #k normalize nodelta 2901 whd in match (is_Sskip ?); 2902 try /2 by refl, ex_intro/ 2903 | 9,10: #u #_ 2904 whd in match (is_Sskip ?); 2905 try /2 by refl, ex_intro/ 2906 | 11: #e #u #_ 2907 whd in match (is_Sskip ?); 2908 try /2 by refl, ex_intro/ 2909 | 12: #e #ls #u #_ 2910 whd in match (sw_rem ??); 2911 whd in match (switch_removal ??); 3033 /2 by ex_intro/ 3034 | 2: #e #s1 #s2 #_ #u normalize 3035 cases (switch_removal ? ?) * #a #b #c normalize nodelta 3036 cases (switch_removal ? ?) * #e #f #g normalize nodelta 3037 /2 by ex_intro/ 3038 | 3,4: #e #s #_ #u normalize 3039 cases (switch_removal ? ?) * #e #f #g normalize nodelta 3040 /2 by ex_intro/ 3041 | 5: #s1 #e #s2 #s3 #_ #u normalize 3042 cases (switch_removal ? ?) * #a #b #c normalize nodelta 3043 cases (switch_removal ? ?) * #e #f #g normalize nodelta 3044 cases (switch_removal ? ?) * #h #i #j normalize nodelta 3045 /2 by ex_intro/ 3046 | 6: #e #ls #_ #u normalize 2912 3047 cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta 2913 3048 cases (fresh ??) #e #f normalize nodelta 2914 normalize in match (simplify_switch ???);2915 3049 cases (fresh ? f) #g #h normalize nodelta 2916 3050 cases (produce_cond ????) * #k #l #m normalize nodelta 2917 whd in match (is_Sskip ?); 2918 try /2 by refl, ex_intro/ 2919 | 13,15: #lab #st #u #_ 2920 whd in match (sw_rem ??); 2921 whd in match (switch_removal ??); 2922 cases (switch_removal ? ?) * #a #b #c normalize nodelta 2923 whd in match (is_Sskip ?); 2924 try /2 by refl, ex_intro/ 2925 | 14: #lab #u 2926 whd in match (is_Sskip ?); 2927 try /2 by refl, ex_intro/ ] 2928 qed. 2929 *) 3051 /2 by ex_intro/ 3052 | 7,8: #ls #st #_ #u normalize 3053 cases (switch_removal ? ?) * #e #f #g normalize nodelta 3054 /2 by ex_intro/ 3055 ] qed. 2930 3056 2931 3057 (* … … 2989 3115 ] qed. 2990 3116 2991 lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed. 2992 2993 lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c. 2994 #A #B #a #b * #a' #b' #H destruct @refl 2995 qed. 2996 2997 lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c. 2998 #A #B #a #b * #a' #b' #H destruct @refl 2999 qed. 3117 lemma switch_removal_elim : ∀s,u. ∃s',fvs',u'. switch_removal s u = 〈s',fvs',u'〉. 3118 #s #u cases (switch_removal s u) * #s' #fvs' #u' 3119 %{s'} %{fvs'} %{u'} @refl 3120 qed. 3121 3122 lemma switch_removal_branches_elim : ∀ls,u. ∃ls',fvs',u'. switch_removal_branches ls u = 〈ls',fvs',u'〉. 3123 #ls #u cases (switch_removal_branches ls u) * * #ls' #fvs' #u' /4 by ex_intro/ qed. 3124 3125 lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed. 3126 3127 lemma simplify_switch_elim : ∀e,ls,u. ∃res,u'. simplify_switch e ls u = 〈res, u'〉. 3128 #e #ls #u cases (simplify_switch e ls u) #res #u /3 by ex_intro/ qed. 3129 3130 (* ---------------------------------------------------------------------------- 3131 What follows is some rather generic stuff on proving that reading where we 3132 just wrote yields what we expect. We have to prove everything at the back-end 3133 level, and then lift this to the front-end. This entails having to reason on 3134 invariants bearing on "intervals" of memories, and a lot of annoying stuff 3135 to go back and forth nats, Zs and bitvectors ... *) 3136 3137 lemma fold_left_neq_acc_neq : 3138 ∀m. ∀acc1,acc2. ∀y1,y2:BitVector m. 3139 acc1 ≠ acc2 → 3140 fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc1 y1 ≠ 3141 fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc2 y2. 3142 #m elim m 3143 [ 1: #acc1 #acc2 #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) // 3144 | 2: #m' #Hind #acc1 #acc2 #y1 #y2 3145 elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1 3146 elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2 3147 >Heq1 >Heq2 * #Hneq % whd in ⊢ ((??%%) → ?); 3148 cases hd1 cases hd2 normalize nodelta #H 3149 [ 1: lapply (Hind (p1 acc1) (p1 acc2) tl1 tl2 ?) 3150 [ 1: % #H' @Hneq destruct (H') @refl ] 3151 * #H' @H' @H 3152 | 4: lapply (Hind (p0 acc1) (p0 acc2) tl1 tl2 ?) 3153 [ 1: % #H' @Hneq destruct (H') @refl ] 3154 * #H' @H' @H 3155 | 2: lapply (Hind (p1 acc1) (p0 acc2) tl1 tl2 ?) 3156 [ 1: % #H' destruct ] 3157 * #H' @H' try @H 3158 | 3: lapply (Hind (p0 acc1) (p1 acc2) tl1 tl2 ?) 3159 [ 1: % #H' destruct ] 3160 * #H' @H' try @H ] 3161 ] qed. 3162 3163 lemma fold_left_eq : 3164 ∀m. ∀acc. ∀y1,y2:BitVector m. 3165 fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y1 = 3166 fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y2 → 3167 y1 = y2. 3168 #m elim m 3169 [ 1: #acc #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) // 3170 | 2: #m' #Hind #acc #y1 #y2 3171 elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1 3172 elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2 3173 >Heq1 >Heq2 whd in ⊢ ((??%%) → ?); 3174 cases hd1 cases hd2 normalize nodelta 3175 [ 1,4: #H >(Hind … H) @refl 3176 | 2: #Habsurd lapply (fold_left_neq_acc_neq ? (p1 acc) (p0 acc) tl1 tl2 ?) 3177 [ 1: % #H' destruct ] 3178 * #H @(False_ind … (H Habsurd)) 3179 | 3: #Habsurd lapply (fold_left_neq_acc_neq ? (p0 acc) (p1 acc) tl1 tl2 ?) 3180 [ 1: % #H' destruct ] 3181 * #H @(False_ind … (H Habsurd)) ] 3182 ] qed. 3183 3184 lemma bv_neq_Z_neq_aux : 3185 ∀n. ∀bv1,bv2 : BitVector n. ∀f. 3186 Z_of_unsigned_bitvector n bv1 ≠ 3187 pos (fold_left Pos bool n (λacc:Pos.λb:bool.if b then p1 acc else p0 acc ) (f one) bv2). 3188 #n elim n 3189 [ 1: #bv1 #bv2 >(BitVector_O … bv1) >(BitVector_O … bv2) #f normalize % #H destruct 3190 | 2: #n' #Hind #bv1 #bv2 #f 3191 elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1 3192 elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2 3193 >Heq1 >Heq2 % 3194 whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?); 3195 cases hd1 cases hd2 normalize nodelta 3196 normalize in ⊢ ((??%%) → ?); 3197 [ 1: #Hpos destruct (Hpos) 3198 lapply (fold_left_neq_acc_neq ? one (p1 (f one)) tl1 tl2 ?) 3199 [ 1: % #H destruct ] 3200 * #H @H @e0 3201 | 2: #Hpos destruct (Hpos) 3202 lapply (fold_left_neq_acc_neq ? one (p0 (f one)) tl1 tl2 ?) 3203 [ 1: % #H destruct ] 3204 * #H @H @e0 3205 | 3: #H cases (Hind tl1 tl2 (λx. p1 (f x))) #H' @H' @H 3206 | 4: #H cases (Hind tl1 tl2 (λx. p0 (f x))) #H' @H' @H 3207 ] 3208 ] qed. 3209 3210 lemma bv_neq_Z_neq : ∀n. ∀bv1,bv2: BitVector n. 3211 bv1 ≠ bv2 → Z_of_unsigned_bitvector n bv1 ≠ Z_of_unsigned_bitvector n bv2. 3212 #n #bv1 #bv2 * #Hneq % #Hneq' @Hneq -Hneq lapply Hneq' -Hneq' 3213 lapply bv2 lapply bv1 -bv1 -bv2 3214 elim n 3215 [ 1: #bv1 #bv2 >(BitVector_O bv1) >(BitVector_O bv2) // 3216 | 2: #n' #Hind #bv1 #bv2 3217 elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1 3218 elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2 3219 >Heq1 >Heq2 3220 whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?); 3221 cases hd1 cases hd2 normalize nodelta 3222 [ 1: #Heq destruct (Heq) lapply (fold_left_eq … e0) * @refl 3223 | 4: #H >(Hind ?? H) @refl 3224 | 2: #H lapply (sym_eq ??? H) -H #H 3225 cases (bv_neq_Z_neq_aux ? tl2 tl1 (λx.x)) #H' @(False_ind … (H' H)) 3226 | 3: #H 3227 cases (bv_neq_Z_neq_aux ? tl1 tl2 (λx.x)) #H' @(False_ind … (H' H)) ] 3228 ] qed. 3229 3230 definition Z_of_offset ≝ λofs.Z_of_unsigned_bitvector ? (offv ofs). 3231 3232 (* This axiom looks reasonable to me. But I slept 3 hours last night. *) 3233 axiom bv_incr_to_Z : ∀sz.∀bv:BitVector sz. 3234 Z_of_unsigned_bitvector ? (increment ? bv) = OZ ∨ 3235 Z_of_unsigned_bitvector ? (increment ? bv) = (Zsucc (Z_of_unsigned_bitvector ? bv)). 3236 3237 (* Note the possibility of overflow of bv. But it should be allright in the big picture. *) 3238 lemma offset_succ_to_Z_succ : 3239 ∀bv : BitVector 16. ∀x. Z_of_unsigned_bitvector ? bv < x → Z_of_unsigned_bitvector ? (increment ? bv) ≤ x. 3240 #bv #x 3241 cases (bv_incr_to_Z ? bv) 3242 [ 1: #Heq >Heq lapply (Z_of_unsigned_not_neg bv) * 3243 [ 1: #Heq >Heq elim x // 3244 | 2: * #p #H >H elim x // ] 3245 | 2: #H >H elim x 3246 elim (Z_of_unsigned_bitvector 16 bv) try /2/ 3247 ] qed. 3248 3249 (* 3250 lemma Z_not_le_shifted : ∀ofs. 3251 (Z_of_unsigned_bitvector 16 (offv (shift_offset 2 ofs (bitvector_of_nat 2 1))) ≤ Z_of_unsigned_bitvector 16 (offv ofs)) → False. 3252 * #vec *) 3253 3254 (* We prove the following properties for bestorev : 3255 1) storing doesn't modify the nextblock 3256 2) it does not modify the extents of the block written to 3257 3) since we succeeded in storing, the offset is in the bounds 3258 4) reading where we wrote yields the obvious result 3259 5) besides the written offset, the memory contains the same stuff 3260 *) 3261 lemma mem_bounds_invariant_after_bestorev : 3262 ∀m,m',b,ofs,bev. 3263 bestorev m (mk_pointer b ofs) bev = Some ? m' → 3264 nextblock m' = nextblock m ∧ 3265 (∀b.low (blocks m' b) = low (blocks m b) ∧ 3266 high (blocks m' b) = high (blocks m b)) ∧ 3267 (low (blocks m b) ≤ (Z_of_offset ofs) ∧ 3268 (Z_of_offset ofs) < high (blocks m b)) ∧ 3269 (contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv ofs)) = bev) ∧ 3270 (∀o. o ≠ ofs → contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv o)) = 3271 contents (blocks m b) (Z_of_unsigned_bitvector ? (offv o))). 3272 #m #m' #b #ofs #bev whd in ⊢ ((??%?) → ?); 3273 #H 3274 cases (if_opt_inversion ???? H) #Hlt -H normalize nodelta #H 3275 cases (if_opt_inversion ???? H) #Hlelt -H #H 3276 cases (andb_inversion … Hlelt) #Hle #Hlt @conj try @conj try @conj try @conj 3277 destruct try @refl 3278 [ 1: 3279 #b' normalize cases b #br #bid cases b' #br' #bid' 3280 cases br' cases br normalize @(eqZb_elim … bid' bid) #H normalize 3281 try /2 by conj, refl/ 3282 | 2: @Zleb_true_to_Zle cases ofs in Hle; #o #H @H 3283 | 3: @Zltb_true_to_Zlt cases ofs in Hlt; #o #H @H 3284 | 4: normalize cases b #br #bid cases br normalize >eqZb_z_z normalize 3285 >eqZb_z_z @refl 3286 | 5: #o #Hneq normalize in ⊢ (??%%); cases b * #bid normalize nodelta 3287 >eqZb_z_z normalize nodelta 3288 @(eqZb_elim … (Z_of_unsigned_bitvector 16 (offv o)) (Z_of_unsigned_bitvector 16 (offv ofs))) 3289 [ 1,3: lapply Hneq cases o #bv1 cases ofs #bv2 3290 #Hneq lapply (bv_neq_Z_neq ? bv1 bv2 ?) 3291 [ 1,3: % #Heq destruct cases Hneq #H @H @refl ] 3292 * #H #Habsurd @(False_ind … (H Habsurd)) 3293 | 2,4: normalize nodelta #H @refl ] 3294 ] qed. 3295 3296 (* Shifts an offset [i] times. storen uses a similar operation internally. *) 3297 let rec shiftn (off:offset) (i:nat) on i : offset ≝ 3298 match i with 3299 [ O ⇒ off 3300 | S n ⇒ 3301 shiftn (shift_offset 2 off (bitvector_of_nat … 1)) n 3302 ]. 3303 3304 (* This axioms states that if we do not stray too far, we cannot circle back to ourselves. Pretty trivial, but a 3305 serious PITA to prove. *) 3306 axiom shiftn_no_wrap : ∀i. i ≤ 8 → ∀ofs. shiftn ofs i ≠ ofs. 3307 3308 (* We prove some properties of [storen m ptr data]. Note that [data] is a list of back-end chunks. 3309 What we expect [storen] to do is to store this list starting at [ptr]. The property we expect to 3310 have is that the contents of this particular zone (ptr to ptr+|data|-1) match exactly [data], and 3311 that elsewhere the memory is untouched. 3312 Not so simple. Some observations: 3313 A) Pointers are encoded as block+offsets, and offsets are bitvectors, hence limited in range (2^16). 3314 On the other hand, block extents are encoded on Zs and are unbounded. This entails some problems 3315 when writing at the edge of the range of offsets and wrapping around, but that can be solved 3316 resorting to ugliness and trickery. 3317 B) The [data] list is unbounded. Taking into account the point A), this means that we can lose 3318 data when writing (exactly as when we write in a circular buffer, overwriting previous stuff). 3319 The only solution to that is to explicitly bound |data| with something reasonable. 3320 Taking these observations into account, we prove the following invariants: 3321 1) storing doesn't modify the nextblock (trivial) 3322 2) it does not modify the extents of the block written to (trivial) 3323 3) all the offsets on which we run while writing are legal (trivial) 3324 3) if we index properly, we hit the stored data in the same order as in the list 3325 4) If we hit elsewhere, we find the memory unmodified. We have a problem for defining "elsewhere", 3326 because bitvectors (hence offsets) are limited in their range. For now, we define "elsewhere" as 3327 "not reachable by shiftn from [ofs] to |data|" 3328 5) the pointer we write to is valid (trivial) 3329 *) 3330 lemma mem_bounds_invariant_after_storen : 3331 ∀data,m,m',b,ofs. 3332 |data| ≤ 8 → (* 8 is the size of a double. *) 3333 storen m (mk_pointer b ofs) data = Some ? m' → 3334 (nextblock m' = nextblock m ∧ 3335 (∀b.low (blocks m' b) = low (blocks m b) ∧ 3336 high (blocks m' b) = high (blocks m b)) ∧ 3337 (∀index. index < |data| → low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧ 3338 Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧ 3339 (∀index. index < |data| → nth_opt ? index data = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧ 3340 (∀o. (∀i. i < |data| → o ≠ shiftn ofs i) → 3341 contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧ 3342 (|data| > 0 → valid_pointer m (mk_pointer b ofs) = true)). 3343 #l elim l 3344 [ 1: #m #m' #b #ofs #_ normalize #H destruct @conj try @conj try @conj try @conj try @conj try @refl 3345 [ 1: #b0 @conj try @refl 3346 (* | 2: #Habsurd @False_ind /2 by le_S_O_absurd/*) 3347 | 2,3: #i #Habsurd @False_ind elim i in Habsurd; try /2/ 3348 | 4: #o #Hout @refl 3349 | 5: #H @False_ind /2 by le_S_O_absurd/ ] 3350 | 2: #hd #tl #Hind #m #m' #b #ofs #Hsize_bound #Hstoren 3351 whd in Hstoren:(??%?); 3352 cases (some_inversion ????? Hstoren) #m'' * #Hbestorev -Hstoren #Hstoren 3353 lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HI #HJ #HK 3354 lapply (Hind … Hstoren) [ 1: /2 by le_S_to_le/ ] * * * * * 3355 #HC #HD #HE #HF #HV #HW @conj try @conj try @conj try @conj try @conj 3356 [ 1: <HA <HC @refl 3357 | 2: #b elim (HB b) #HF #HG elim (HD b) #HG #HH @conj try // 3358 | 4: * 3359 [ 1: #_ <HJ whd in match (nth 0 ???); 3360 lapply (HV ofs ?) 3361 [ 1: #i #Hlt @sym_neq % #Heq lapply (shiftn_no_wrap (S i) ? ofs) 3362 [ 1: normalize in Hsize_bound; 3363 cut (|tl| < 8) [ /2 by lt_plus_to_minus_r/ ] 3364 #Hlt' lapply (transitive_lt … Hlt Hlt') // ] 3365 * #H @H whd in match (shiftn ??); @Heq 3366 | 2: cases ofs #ofs' normalize // ] 3367 | 2: #i' #Hlt lapply (HF i' ?) 3368 [ 1: normalize normalize in Hlt; lapply (monotonic_pred … Hlt) // 3369 | 2: #H whd in match (nth_opt ???); >H @refl ] ] 3370 | 5: #o #H >HV 3371 [ 2: #i #Hlt @(H (S i) ?) 3372 normalize normalize in Hlt; /2 by le_S_S/ 3373 | 1: @HK @(H 0) // ] 3374 | 6: #_ @(bestorev_to_valid_pointer … Hbestorev) 3375 | 3: * 3376 [ 1: #_ <HJ whd in match (shiftn ??); 3377 lapply (Zleb_true_to_Zle (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) 3378 lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?); 3379 whd in match (low_bound ??); whd in match (high_bound ??); 3380 cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true 3381 cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) 3382 [ 2: normalize #Habsurd destruct ] normalize nodelta #Hltb 3383 lapply (Zltb_true_to_Zlt … Hltb) #Hlt' #Hleb lapply (Hleb (refl ??)) -Hleb #Hleb' 3384 normalize @conj try assumption 3385 | 2: #i' #Hlt cases (HB b) #Hlow1 #Hhigh1 cases (HD b) #Hlow2 #Hhigh2 3386 lapply (HE i' ?) [ 1: normalize in Hlt ⊢ %;lapply (monotonic_pred … Hlt) // ] 3387 >Hlow1 >Hhigh1 * #H1 #H2 @conj try @H1 try @H2 3388 ] 3389 ] 3390 ] qed. 3391 3392 lemma storen_beloadv_ok : 3393 ∀m,m',b,ofs,hd,tl. 3394 |hd::tl| ≤ 8 → (* 8 is the size of a double. *) 3395 storen m (mk_pointer b ofs) (hd::tl) = Some ? m' → 3396 ∀i. i < |hd::tl| → beloadv m' (mk_pointer b (shiftn ofs i)) = nth_opt ? i (hd::tl). 3397 #m #m' #b #ofs #hd #tl #Hle #Hstoren 3398 lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * * 3399 #Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr 3400 #i #Hle lapply (Hdata i Hle) #Helt >Helt 3401 whd in match (beloadv ??); whd in match (nth_opt ???); 3402 lapply (Hvalid_ptr ?) try // 3403 whd in ⊢ ((??%?) → ?); 3404 >Hnext cases (Zltb (block_id b) (nextblock m)) 3405 [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct ] 3406 >andb_lsimpl_true normalize nodelta 3407 whd in match (low_bound ??); whd in match (high_bound ??); 3408 cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh #H 3409 lapply (Hvalid_offs i Hle) * #Hzle #Hzlt 3410 >(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl 3411 qed. 3412 3413 lemma loadn_beloadv_ok : 3414 ∀size,m,b,ofs,result. 3415 loadn m (mk_pointer b ofs) size = Some ? result → 3416 ∀i. i < size → beloadv m (mk_pointer b (shiftn ofs i)) = nth_opt ? i result. 3417 #size elim size 3418 [ 1: #m #b #ofs #result #Hloadn * 3419 [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/ 3420 | 2: #i' #Habsurd @False_ind /2 by le_S_O_absurd/ ] 3421 | 2: #size' #Hind_size #m #b #ofs #result #Hloadn #i 3422 elim i 3423 [ 1: #_ 3424 cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn' 3425 cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq 3426 destruct (Heq) whd in match (shiftn ofs 0); 3427 >Hbeloadv @refl 3428 | 2: #i' #Hind #Hlt 3429 whd in match (shiftn ofs (S i')); 3430 lapply (Hind ?) 3431 [ /2 by lt_S_to_lt/ ] #Hbeloadv_ind 3432 whd in Hloadn:(??%?); 3433 cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn' 3434 cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq -Hloadn' 3435 destruct (Heq) 3436 @Hind_size [ 2: lapply Hlt normalize @monotonic_pred ] 3437 @Hloadn_tl 3438 ] 3439 ] qed. 3440 3441 lemma storen_loadn_nonempty : 3442 ∀data,m,m',b,ofs. 3443 |data| ≤ 8 → 3444 storen m (mk_pointer b ofs) data = Some ? m' → 3445 ∃result. loadn m' (mk_pointer b ofs) (|data|) = Some ? result ∧ |result|=|data|. 3446 #data elim data 3447 [ 1: #m #m' #b #ofs #_ #Hstoren normalize in Hstoren; destruct %{[ ]} @conj try @refl ] 3448 #hd #tl #Hind #m #m' #b #ofs #Hle #Hstoren 3449 lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * * 3450 #Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr 3451 cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0 3452 whd in match (loadn ???); 3453 lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?); 3454 whd in match (beloadv ??); 3455 whd in match (low_bound ??); whd in match (high_bound ??); 3456 >Hnext 3457 cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true 3458 normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh 3459 cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) normalize nodelta 3460 [ 2: #Habsurd destruct ] >andb_lsimpl_true 3461 #Hltb >Hltb normalize nodelta 3462 cases (Hind … Hstoren0) [ 2: lapply Hle normalize /2 by le_S_to_le/ ] 3463 #tl' * #Hloadn >Hloadn #Htl' normalize nodelta 3464 %{(contents (blocks m' b) (Z_of_unsigned_bitvector offset_size (offv ofs))::tl')} @conj try @refl 3465 normalize >Htl' @refl 3466 qed. 3467 3468 let rec double_list_ind 3469 (A : Type[0]) 3470 (P : list A → list A → Prop) 3471 (base_nil : P [ ] [ ]) 3472 (base_l1 : ∀hd1,l1. P (hd1::l1) [ ]) 3473 (base_l2 : ∀hd2,l2. P [ ] (hd2::l2)) 3474 (ind : ∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1 :: tl1) (hd2 :: tl2)) 3475 (l1, l2 : list A) on l1 ≝ 3476 match l1 with 3477 [ nil ⇒ 3478 match l2 with 3479 [ nil ⇒ base_nil 3480 | cons hd2 tl2 ⇒ base_l2 hd2 tl2 ] 3481 | cons hd1 tl1 ⇒ 3482 match l2 with 3483 [ nil ⇒ base_l1 hd1 tl1 3484 | cons hd2 tl2 ⇒ 3485 ind hd1 hd2 tl1 tl2 (double_list_ind A P base_nil base_l1 base_l2 ind tl1 tl2) 3486 ] 3487 ]. 3488 3489 lemma nth_eq_tl : 3490 ∀A:Type[0]. ∀l1,l2:list A. ∀hd1,hd2. 3491 (∀i. nth_opt A i (hd1::l1) = nth_opt A i (hd2::l2)) → 3492 (∀i. nth_opt A i l1 = nth_opt A i l2). 3493 #A #l1 #l2 @(double_list_ind … l1 l2) 3494 [ 1: #hd1 #hd2 #_ #i elim i try /2/ 3495 | 2: #hd1' #l1' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct 3496 | 3: #hd2' #l2' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct 3497 | 4: #hd1' #hd2' #tl1' #tl2' #H #hd1 #hd2 3498 #Hind 3499 @(λi. Hind (S i)) 3500 ] qed. 3501 3502 3503 lemma nth_eq_to_eq : 3504 ∀A:Type[0]. ∀l1,l2:list A. (∀i. nth_opt A i l1 = nth_opt A i l2) → l1 = l2. 3505 #A #l1 elim l1 3506 [ 1: #l2 #H lapply (H 0) normalize 3507 cases l2 3508 [ 1: // 3509 | 2: #hd2 #tl2 normalize #Habsurd destruct ] 3510 | 2: #hd1 #tl1 #Hind * 3511 [ 1: #H lapply (H 0) normalize #Habsurd destruct 3512 | 2: #hd2 #tl2 #H lapply (H 0) normalize #Heq destruct (Heq) 3513 >(Hind tl2) try @refl @(nth_eq_tl … H) 3514 ] 3515 ] qed. 3516 3517 (* for leb_elim, shadowed in positive.ma *) 3518 definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop. 3519 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim. 3520 3521 include alias "arithmetics/nat.ma". 3522 3523 lemma nth_miss : ∀A:Type[0]. ∀l:list A. ∀i. |l| ≤ i → nth_opt A i l = None ?. 3524 #A #l elim l // 3525 #hd #tl #H #i elim i 3526 [ 1: normalize #Habsurd @False_ind /2 by le_S_O_absurd/ 3527 | 2: #i' #H' #Hle whd in match (nth_opt ???); @H /2 by monotonic_pred/ 3528 ] qed. 3529 3530 lemma storen_loadn_ok : 3531 ∀data. 3532 |data| ≤ 8 → (* 8 is the size of a double. *) 3533 ∀m,m',b,ofs. 3534 storen m (mk_pointer b ofs) data = Some ? m' → 3535 loadn m' (mk_pointer b ofs) (|data|) = Some ? data. 3536 #data elim data try // #hd #tl #Hind #Hle #m #m' #b #ofs #Hstoren 3537 lapply (storen_beloadv_ok m m' … Hle Hstoren) #Hyp_storen 3538 cases (storen_loadn_nonempty … Hle Hstoren) #result * #Hloadn #Hresult_sz 3539 lapply (loadn_beloadv_ok (|hd::tl|) m' b ofs … Hloadn) #Hyp_loadn 3540 cut (∀i. i < |hd::tl| → nth_opt ? i (hd::tl) = nth_opt ? i result) 3541 [ #i #Hlt lapply (Hyp_storen … i Hlt) #Heq1 3542 lapply (Hyp_loadn … i Hlt) #Heq2 >Heq1 in Heq2; // ] 3543 #Hyp 3544 cut (result = hd :: tl) 3545 [ 2: #Heq destruct (Heq) @Hloadn ] 3546 @nth_eq_to_eq #i @sym_eq 3547 @(leb_elim' … (S i) (|hd::tl|)) 3548 [ 1: #Hle @(Hyp ? Hle) 3549 | 2: #Hnle cut (|hd::tl| ≤ i) 3550 [ lapply (not_le_to_lt … Hnle) normalize /2 by monotonic_pred/ ] 3551 #Hle' 3552 >nth_miss // >nth_miss // 3553 ] qed. 3554 3555 (* In order to prove the lemma on store_value_of_type and load_value_of_type, 3556 we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *) 3557 lemma typesize_bounded : ∀ty. typesize ty ≤ 8. 3558 * try // 3559 [ 1: * try // 3560 | 2: * try // 3561 ] qed. 3562 3563 (* Lifting bound on make_list *) 3564 lemma makelist_bounded : ∀A,sz,bound,elt. sz ≤ bound → |make_list A elt sz| ≤ bound. 3565 #A #sz elim sz try // 3566 #sz' #Hind #bound #elt #Hbound normalize 3567 cases bound in Hbound; 3568 [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/ 3569 | 2: #bound' #Hbound' lapply (Hind bound' elt ?) 3570 [ 1: /2 by monotonic_pred/ 3571 | 2: /2 by le_S_S/ ] 3572 ] qed. 3573 3574 lemma bytes_of_bitvector_bounded : 3575 ∀sz,bv. |bytes_of_bitvector (size_intsize sz) bv| = size_intsize sz. 3576 * #bv normalize 3577 [ 1: cases (vsplit ????) normalize nodelta #bv0 #bv1 // 3578 | 2: cases (vsplit ????) normalize nodelta #bv0 #bv1 3579 cases (vsplit ????) normalize nodelta #bv2 #bv3 // 3580 | 3: cases (vsplit ????) normalize nodelta #bv0 #bv1 3581 cases (vsplit ????) normalize nodelta #bv2 #bv3 3582 cases (vsplit ????) normalize nodelta #bv4 #bv5 3583 cases (vsplit ????) normalize nodelta #bv6 #bv7 3584 // 3585 ] qed. 3586 3587 lemma map_bounded : 3588 ∀A,B:Type[0]. ∀l:list A. ∀f. |map A B f l| = |l|. 3589 #A #B #l elim l try // 3590 qed. 3591 3592 lemma fe_to_be_values_bounded : 3593 ∀ty,v. |fe_to_be_values ty v| ≤ 8. 3594 #ty cases ty 3595 [ 3: #fsz #v whd in match (fe_to_be_values ??); 3596 cases v normalize nodelta 3597 [ 1: @makelist_bounded @typesize_bounded 3598 | 2: * normalize nodelta #bv 3599 >map_bounded >bytes_of_bitvector_bounded // 3600 | 3: #fl @makelist_bounded @typesize_bounded 3601 | 4: // 3602 | 5: #ptr // ] 3603 | 2: #v whd in match (fe_to_be_values ??); 3604 cases v normalize nodelta 3605 [ 1: @makelist_bounded @typesize_bounded 3606 | 2: * normalize nodelta #bv 3607 >map_bounded >bytes_of_bitvector_bounded // 3608 | 3: #fl @makelist_bounded @typesize_bounded 3609 | 4: // 3610 | 5: #ptr // ] 3611 | 1: #sz #sg #v whd in match (fe_to_be_values ??); 3612 cases v normalize nodelta 3613 [ 1: @makelist_bounded @typesize_bounded 3614 | 2: * normalize nodelta #bv 3615 >map_bounded >bytes_of_bitvector_bounded // 3616 | 3: #fl @makelist_bounded @typesize_bounded 3617 | 4: // 3618 | 5: #ptr // ] 3619 ] qed. 3620 3621 3622 definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v. 3623 match ty with 3624 [ ASTint sz sg ⇒ 3625 match v with 3626 [ Vint sz' sg' ⇒ sz = sz' (* The sign does not matter *) 3627 | _ ⇒ False ] 3628 | ASTptr ⇒ 3629 match v with 3630 [ Vptr p ⇒ True 3631 | _ ⇒ False ] 3632 | ASTfloat fsz ⇒ 3633 match v with 3634 [ Vfloat _ ⇒ True 3635 | _ ⇒ False ] 3636 ]. 3637 3638 3639 definition type_consistent_with_value : type → val → Prop ≝ λty,v. 3640 match access_mode ty with 3641 [ By_value chunk ⇒ ast_typ_consistent_with_value chunk v 3642 | _ ⇒ True 3643 ]. 3644 3645 3646 (* We also need the following property. It is not provable unless [v] and [ty] are consistent. *) 3647 lemma fe_to_be_values_size : 3648 ∀ty,v. ast_typ_consistent_with_value ty v → 3649 typesize ty = |fe_to_be_values ty v|. 3650 * 3651 [ 1: #sz #sg #v 3652 whd in match (fe_to_be_values ??); cases v 3653 normalize in ⊢ (% → ?); 3654 [ 1,4: @False_ind 3655 | 2: #sz' #i normalize in ⊢ (% → ?); #Heq destruct normalize nodelta 3656 >map_bounded >bytes_of_bitvector_bounded cases sz' // 3657 | 3: #f normalize in ⊢ (% → ?); @False_ind 3658 | 5: #p normalize in ⊢ (% → ?); @False_ind ] 3659 | 2: #v cases v 3660 normalize in ⊢ (% → ?); 3661 [ 1,4: @False_ind 3662 | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind 3663 | 3: #f normalize in ⊢ (% → ?); @False_ind 3664 | 5: #p #_ // ] 3665 | 3: #fsz #v cases v 3666 normalize in ⊢ (% → ?); 3667 [ 1: @False_ind 3668 | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind 3669 | 3: #f #_ cases fsz // 3670 | 4: @False_ind 3671 | 5: #p normalize in ⊢ (% → ?); @False_ind ] 3672 ] qed. 3673 3674 (* Not verified for floats atm. Restricting to integers. *) 3675 lemma fe_to_be_to_fe_value : ∀sz,sg,v. 3676 ast_typ_consistent_with_value (ASTint sz sg) v → 3677 (be_to_fe_value (ASTint sz sg) (fe_to_be_values (ASTint sz sg) v) = v). 3678 #sz #sg #v 3679 whd in match (fe_to_be_values ??); 3680 cases v normalize in ⊢ (% → ?); 3681 [ 1,4: @False_ind 3682 | 3: #f @False_ind 3683 | 5: #p @False_ind 3684 | 2: #sz' #i' #Heq normalize in Heq; destruct (Heq) normalize nodelta 3685 cases sz' in i'; #i normalize nodelta 3686 normalize in i; 3687 whd in match (be_to_fe_value ??); 3688 normalize in match (size_intsize ?); 3689 whd in match (bytes_of_bitvector ??); 3690 [ 1: lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i 3691 <(vsplit_prod … Heq_i) normalize nodelta >Heq_i 3692 whd in match (build_integer_val ??); 3693 >(BitVector_O … ri) // 3694 | 2: lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i 3695 <(vsplit_prod … Heq_i) normalize nodelta >Heq_i 3696 whd in match (build_integer_val ??); 3697 normalize in match (size_intsize ?); 3698 whd in match (bytes_of_bitvector ??); 3699 lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri 3700 <(vsplit_prod … Heq_ri) normalize nodelta >Heq_ri 3701 whd in match (build_integer_val ??); 3702 >(BitVector_O … rri) // 3703 | 3: lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i 3704 <(vsplit_prod … Heq_i) normalize nodelta >Heq_i 3705 whd in match (build_integer_val ??); 3706 normalize in match (size_intsize ?); 3707 whd in match (bytes_of_bitvector ??); 3708 lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB 3709 <(vsplit_prod … Heq_iB) normalize nodelta >Heq_iB 3710 whd in match (bytes_of_bitvector ??); 3711 lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD 3712 <(vsplit_prod … Heq_iD) normalize nodelta >Heq_iD 3713 whd in match (bytes_of_bitvector ??); 3714 lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF 3715 <(vsplit_prod … Heq_iF) normalize nodelta >Heq_iF 3716 >(BitVector_O … iH) @refl ] 3717 ] qed. 3718 3719 (* It turns out that the following property is not true in general. Floats are converted to 3720 BVundef, which are converted back to Vundef. But we care only about ints. *) 3721 lemma storev_loadv_ok : 3722 ∀sz,sg,m,b,ofs,v,m'. 3723 ast_typ_consistent_with_value (ASTint sz sg) v → 3724 store (ASTint sz sg) m (mk_pointer b ofs) v = Some ? m' → 3725 load (ASTint sz sg) m' (mk_pointer b ofs) = Some ? v. 3726 #sz #sg #m #b #ofs #v #m' #H 3727 whd in ⊢ ((??%?) → (??%?)); #Hstoren 3728 lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint sz sg) v) m m' b ofs Hstoren) 3729 >(fe_to_be_values_size … H) #H >H normalize nodelta 3730 >fe_to_be_to_fe_value try // 3731 qed. 3732 3733 (* For the arguments exposed before, we restrict the lemma to ints. 3734 *) 3735 lemma store_value_load_value_ok : 3736 ∀sz,sg,m,b,ofs,v,m'. 3737 type_consistent_with_value (Tint sz sg) v → 3738 store_value_of_type (Tint sz sg) m b ofs v = Some ? m' → 3739 load_value_of_type (Tint sz sg) m' b ofs = Some ? v. 3740 #sz #sg #m #b #ofs #v #m' #H lapply H whd in ⊢ (% → ?); 3741 cases v in H; normalize nodelta 3742 [ 1: #_ @False_ind | 2: #vsz #vi #H | 3: #vf #_ @False_ind | 4: #_ @False_ind | 5: #vp #_ @False_ind ] 3743 #Heq >Heq in H; #H 3744 (* The lack of control on unfolds is extremely annoying. *) 3745 whd in match (store_value_of_type ?????); #Hstoren 3746 lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint vsz sg) (Vint vsz vi)) m m' b ofs Hstoren) 3747 whd in match (load_value_of_type ????); 3748 >(fe_to_be_values_size … H) #H' >H' normalize nodelta 3749 >fe_to_be_to_fe_value try // 3750 qed. 3751 3752 lemma load_int_value_inversion : 3753 ∀t,m,p,sz,i. load_value_of_type' t m p = Some ? (Vint sz i) → ∃sg. t = Tint sz sg. 3754 #t #m * #b #o #sz #i whd in match (load_value_of_type' ???); 3755 cases t 3756 [ 2: #tsz #tsg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 3757 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] normalize nodelta 3758 whd in match (load_value_of_type ????); 3759 [ 4,5,6,7,9: #Habsurd destruct ] 3760 whd in match (be_to_fe_value ??); 3761 cases (loadn ???) normalize nodelta 3762 [ 1,3,5,7: #Habsurd destruct ] 3763 * 3764 [ 1,3,5,7: #Heq normalize in Heq; destruct ] 3765 #hd #tl 3766 [ 2,3,4: cases hd 3767 [ 1,2,7,8,13,14: whd in match (be_to_fe_value ??); #Heq destruct 3768 | 4,5,10,11,16,17: #HA #Heq destruct (Heq) cases (eqb ??∧?) in e0; 3769 normalize nodelta #Heq' destruct 3770 | 6,12,18: #ptr #part #Heq destruct cases (pointer_of_bevals ?) in e0; 3771 #foo normalize #Habsurd destruct 3772 | *: #op1 #op2 #part #Heq destruct ] 3773 | 1: #H destruct cases hd in e0; normalize nodelta 3774 [ 1,2: #Heq destruct 3775 | 3: #op1 #op2 #part #Habsurd destruct 3776 | 4: #by whd in match (build_integer_val ??); 3777 cases (build_integer ??) normalize nodelta 3778 [ 1: #Heq destruct 3779 | 2: #bv #Heq destruct /2 by ex_intro/ ] 3780 | 5: #p cases (eqb ?? ∧ ?) normalize nodelta #Heq destruct 3781 | 6: #ptr #part cases (pointer_of_bevals ?) #foo normalize nodelta #Heq destruct ] 3782 ] qed. 3783 3784 lemma opt_to_res_load_int_value_inversion : 3785 ∀t,m,p,sz,i. 3786 (opt_to_res val (msg FailedLoad) (load_value_of_type' t m p) = OK ? (Vint sz i)) 3787 → ∃sg. t = Tint sz sg. 3788 #t #m #p #sz #i whd in match (opt_to_res ???); 3789 lapply (load_int_value_inversion t m p sz i) 3790 cases (load_value_of_type' t m p) 3791 [ 1: #H normalize nodelta #Habsurd destruct 3792 | 2: #v #H normalize nodelta #Heq destruct lapply (H (refl ??)) * 3793 #sg #Heq >Heq /2 by ex_intro/ 3794 ] qed. 3795 3796 lemma res_inversion : ∀A,B:Type[0]. ∀e:res A. ∀f:A → res B. ∀res:B. 3797 match e with 3798 [ OK x ⇒ f x 3799 | Error msg ⇒ Error ? msg ] = OK ? res → 3800 ∃res_e. e = OK ? res_e ∧ OK ? res = f res_e. 3801 #A #B * 3802 [ 2: #err #f #res normalize nodelta #Habsurd destruct 3803 | 1: #a #f #res normalize nodelta #Heq destruct %{a} @conj try @refl >Heq @refl 3804 ] qed. 3805 3806 (* In order to prove the consistency of types wrt values, we need the following lemma. *) 3807 (* 3808 lemma exec_expr_Vint_type_inversion : 3809 ∀ge,env,m,e,sz,i,tr. (exec_expr ge env m e=return 〈Vint sz i,tr〉) → 3810 ∃sg. typeof e = Tint sz sg. 3811 #ge #env #m * #ed #ty 3812 @(expr_ind2 … (λed,ty.∀sz:intsize.∀i:bvint sz.∀tr:trace. 3813 exec_expr ge env m (Expr ed ty)=return 〈Vint sz i,tr〉 → 3814 ∃sg:signedness.typeof (Expr ed ty)=Tint sz sg) … (Expr ed ty)) 3815 [ 1: #e' #ty' #H @H 3816 | 2: #sz #i #t #sz0 #i0 #tr whd in ⊢ ((??%?) → ?); cases t 3817 [ 2: #tsz #tsg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 3818 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] normalize nodelta 3819 [ 1: @(eq_intsize_elim … sz tsz) normalize nodelta 3820 [ 2: #Hsz_eq destruct (Hsz_eq) normalize #Heq destruct (Heq) 3821 %{tsg} @refl 3822 | 1: #_ normalize #Habsurd destruct (Habsurd) ] 3823 | *: #Habsurd normalize in Habsurd; destruct ] 3824 | 3: #f #t #sz #i #tr whd in ⊢ ((??%?) → ?); #H normalize in H; destruct (H) 3825 | 4: #id #t #sz #i #tr whd in ⊢ ((??%?) → ?); 3826 @(match exec_lvalue' ge env m (Evar id) t 3827 return λr. r = exec_lvalue' ge env m (Evar id) t → ? 3828 with 3829 [ OK x ⇒ λHeq. ? 3830 | Error msg ⇒ λHeq. ? 3831 ] (refl ? (exec_lvalue' ge env m (Evar id) t))) normalize nodelta 3832 [ 2: normalize #Habsurd destruct ] #Hload 3833 cases (bind_inversion ????? Hload) #loadval * #Heq_loadval #Heq_res 3834 normalize in Heq_res; destruct (Heq_res) 3835 -Hload 3836 whd in Heq_loadval:(??%%); lapply Heq_loadval 3837 @(match load_value_of_type' t m (\fst x) 3838 return λr. r = load_value_of_type' t m (\fst x) → ? 3839 with 3840 [ None ⇒ λHeq. ? 3841 | Some v' ⇒ λHeq. ? 3842 ] (refl ? (load_value_of_type' t m (\fst x)))) normalize nodelta 3843 [ 1: #Habsurd destruct ] 3844 #Heq_v' destruct (Heq_v') 3845 cases (load_int_value_inversion … (sym_eq ??? Heq)) #sg #Htyp_eq 3846 >Htyp_eq %{sg} @refl 3847 | 5: #e #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?); 3848 whd in match (exec_lvalue' ?????); 3849 @(match exec_expr ge env m e 3850 return λx. x = (exec_expr ge env m e) → ? 3851 with 3852 [ OK res ⇒ λH. ? 3853 | Error msg ⇒ λH. ? ] (refl ? (exec_expr ge env m e))) 3854 normalize nodelta 3855 [ 2: #Habsurd destruct ] 3856 cases res in H; #vres #trres #Hexec #H 3857 cases (res_inversion ????? H) -H * * #b' #o' #tr' * 3858 cases vres in Hexec; normalize nodelta 3859 [ 1: #_ #Habsurd destruct 3860 | 2: #sz' #i' #_ #Habsurd destruct 3861 | 3: #f #_ #Habsurd destruct 3862 | 4: #_ #Habsurd destruct ] 3863 #p #Heq_exec_expr #Heq destruct (Heq) #Heq 3864 lapply (sym_eq ??? Heq) -Heq #Heq 3865 cases (bind_inversion ????? Heq) -Heq #x * #Hload_value 3866 #Heq normalize in Heq; destruct (Heq) 3867 @(opt_to_res_load_int_value_inversion … Hload_value) 3868 | 6: #e #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?); #H 3869 cases (res_inversion ????? H) * * #b #o #tr * #Hexec_lvalue 3870 cases t 3871 [ 2: #tsz #tsg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 3872 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] normalize nodelta 3873 #Habsurd destruct 3874 | 7: #op #arg #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?); #H 3875 cases (res_inversion ????? H) * #v #tr * #Hexec_expr 3876 #H' lapply (sym_eq ??? H') -H' #H' 3877 cases (bind_inversion ????? H') #v' * #Hopt_sem #Hvalues 3878 normalize in Hvalues:(??%%); destruct (Hvalues) -H' -H 3879 3880 lapp 3881 >Hopt_sem in H'; 3882 destruct (Hvalues) 3883 3884 whd in match (exec_lvalue ????);*) 3885 3886 3887 3000 3888 3001 3889 (* Main theorem. To be ported and completed to memory injections. TODO *) 3002 3890 theorem switch_removal_correction : 3003 ∀ge,ge' ,s1, s1', tr, s2.3891 ∀ge,ge'. 3004 3892 switch_removal_globals ? fundef_switch_removal ge ge' → 3893 ∀s1,s1',tr,s2. 3005 3894 switch_state_sim ge s1 s1' → 3006 exec_step ge s1 = Value … 〈tr,s2〉 → 3007 eventually ge' (λs2'. switch_state_sim ge s2 s2') s1' tr. 3008 #ge #ge' #st1 #st1' #tr #st2 #Hrelated #Hsim_state 3009 @cthulhu 3010 qed. 3011 3012 (* 3895 exec_step ge s1 = Value … 〈tr,s2〉 → 3896 ∃n. after_n_steps (S n) … clight_exec ge' s1' 3897 (λtr',s2'. tr = tr' ∧ switch_state_sim ge' s2 s2'). 3898 #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state 3013 3899 inversion Hsim_state 3014 3900 [ 1: (* regular state *) 3015 #sss_statement #sss_ result #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars3901 #sss_statement #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars 3016 3902 #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp 3017 #sss_env_hyp #sss_result_hyp #sss_k_hyp #Hext_fresh_for_ge 3903 #sss_env_hyp #sss_writeable_hyp #sss_result_rec #sss_result_hyp #sss_result #sss_result_proj #sss_incl #sss_k_hyp #Hext_fresh_for_ge 3904 #Hs1_eq #Hs1_eq' 3018 3905 elim (sim_related_globals … ge ge' 3019 3906 sss_env sss_m sss_env_ext sss_m_ext sss_writeable sss_new_vars 3020 3907 sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge) 3021 #Hsim_expr #Hsim_lvalue #Hst1_eq #Hst1_eq' #_ 3908 #Hsim_expr #Hsim_lvalue #_ 3909 (* II. Case analysis on the statement. *) 3022 3910 cases sss_statement in sss_lu_fresh sss_result_hyp; 3023 3911 (* Perform the intros for the statements *) … … 3026 3914 | 14: #lab | 15: #cost #body ] 3027 3915 #sss_lu_fresh #sss_result_hyp 3028 [ 1: (* Skip *)3029 whd in match (switch_removal ?? ?) in sss_result_hyp;3030 <(some_inj ??? sss_result_hyp)3916 [ 1: (* Skip statement *) 3917 whd in match (switch_removal ??) in sss_result_hyp; >sss_result_proj <sss_result_hyp 3918 (* III. Case analysis on the continuation. *) 3031 3919 inversion sss_k_hyp normalize nodelta 3032 [ 1: #fvs #Hfvs_eq #Hk #Hk' #_ #Hexec_step 3033 @(eventually_now ????) whd in match (exec_step ??); 3920 [ 1: #new_vars #Hnew_vars_eq #Hk #Hk' #_ #Hexec_step %{0} whd whd in ⊢ (??%?); 3034 3921 >(prod_eq_lproj ????? sss_func_hyp) 3035 3922 >fn_return_simplify 3036 3923 whd in match (exec_step ??) in Hexec_step; 3924 (* IV. Case analysis on the return type *) 3037 3925 cases (fn_return sss_func) in Hexec_step; 3038 3926 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain … … 3040 3928 normalize nodelta 3041 3929 whd in ⊢ ((??%?) → ?); 3042 [ 1: #H destruct (H) %{(Returnstate Vundef Kstop (free_list sss_m_ext (blocks_of_env sss_env_ext)))} 3043 @conj try @refl %3{(map (ident×type) ident \fst sss_new_vars)} 3044 [ 1: @(lset_difference ? sss_writeable (blocks_of_env sss_env_ext)) 3045 | 3: @swc_stop 3046 | 2: 3047 *) 3048 3930 [ 1: #H destruct (H) % try @refl 3931 /3 by sws_returnstate, swc_stop, memext_free_extended_environment, memory_ext_writeable_eq/ 3932 | *: #Habsurd destruct (Habsurd) ] 3933 | 2: #s #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #Hsss_k_hyp 3934 #Hexec_step %{0} whd 3935 >(prod_eq_lproj ????? sss_func_hyp) 3936 whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl 3937 <sss_func_hyp 3938 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') 3939 %1{u (refl ? (switch_removal s u))} try assumption try @refl 3940 #id #Hmem lapply (Hext_fresh_for_ge id Hmem) #Hfind <(rg_find_symbol … Hrelated id) @Hfind 3941 | 3: #cond #body #k #k' #fgen #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ 3942 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') 3943 #Hexec_step %{0} whd whd in Hexec_step; 3944 >(prod_eq_lproj ????? sss_func_hyp) 3945 whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl 3946 %1{ ((switch_removal (Swhile cond body) fgen))} try assumption try @refl 3947 [ 1: <sss_func_hyp @refl 3948 | 2: destruct normalize cases (switch_removal ??) * #body' #fvs' #u' @refl 3949 | 3: whd in match (switch_removal ??); 3950 cases (switch_removal body fgen) in Hincl; * #body' #fvs' #fgen' normalize nodelta #H @H 3951 | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 3952 | 4: #cond #body #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ 3953 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') 3954 #Hexec_step %{0} whd whd in Hexec_step:(??%?) ⊢ (??%?); 3955 cases (bindIO_inversion ??????? Hexec_step) #x1 * #Hexec 3956 >(Hsim_expr … Hexec) 3957 >bindIO_Value cases (exec_bool_of_val ??) 3958 [ 2: #err normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 3959 #b whd in match (m_bind ?????); whd in match (m_bind ?????); 3960 cases b normalize nodelta #H whd in H:(??%%) ⊢ %; destruct (H) 3961 try @conj try @refl 3962 [ 1: %{u … (switch_removal (Sdowhile cond body) u)} try assumption try // 3963 [ 1: destruct normalize cases (switch_removal body u) * #body' #fvs' #u' @refl 3964 | 2: whd in match (switch_removal ??); 3965 cases (switch_removal body u) in Hincl; * #body' #fvs' #u' normalize nodelta #H @H 3966 | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 3967 | 2: %{u … (switch_removal Sskip u) } try assumption try // 3968 [ 1: @(fresh_for_Sskip … Hfresh) 3969 | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ] 3970 | 5: #cond #stmt1 #stmt2 #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ 3971 #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ 3972 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') 3973 #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step) 3974 @conj try @refl 3975 %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // 3976 #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 3977 | 6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars 3978 #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ 3979 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') 3980 #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl 3981 %1{u … new_vars … sss_writeable (switch_removal stmt1 u)} try assumption try // 3982 [ 1: lapply (fresh_to_substatements … Hfresh) normalize * * // 3983 | 2: whd in match (switch_removal ??) in Hincl; 3984 cases (switch_removal stmt1 u) in Hincl; * #stmt1' #fvs1' #u' normalize nodelta 3985 cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' normalize nodelta 3986 whd in match (ret_vars ??); /2 by All_append_l/ 3987 | 3: @(swc_for3 … u) // 3988 | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 3989 | 7: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars 3990 #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ 3991 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') 3992 #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl 3993 %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} 3994 try // 3995 [ 1: whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize 3996 cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize 3997 cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' @refl 3998 | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 3999 | 8: #k #k' #new_vars #Hsimcont #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ 4000 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') 4001 #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl 4002 %1{sss_lu … new_vars … sss_writeable} try // try assumption 4003 [ 1: destruct (sss_result_hyp) @refl 4004 | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 4005 | 9: #en #en' #r #f #k #k' #old_vars #new_vars #Hsimcont #Hnew_vars_eq #Hdisjoint_k #_ 4006 #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ 4007 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') 4008 #Hexec %{0} whd in Hexec:(??%?) ⊢ %; whd in ⊢ (??%?); 4009 >(prod_eq_lproj ????? sss_func_hyp) >fn_return_simplify 4010 cases (fn_return sss_func) in Hexec; normalize nodelta 4011 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 4012 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] 4013 #Hexec whd in Hexec:(??%?); destruct (Hexec) whd @conj try @refl 4014 /3 by sws_returnstate, swc_call, memext_free_extended_environment/ 4015 ] 4016 | 2: (* Assign statement *) 4017 lapply (exec_lvalue_sim_aux … Hsim_lvalue) #Hsim 4018 #Hexec %{0} whd in sss_result_hyp:(??%?); 4019 cases (bindIO_inversion ??????? Hexec) #xl * #Heq_lhs #Hexec_lhs 4020 cases (bindIO_inversion ??????? Hexec_lhs) #xr * #Heq_rhs #Hexec_rhs 4021 cases (bindIO_inversion ??????? Hexec_rhs) #xs * #Heq_store #Hexec_store 4022 whd whd in Hexec_store:(??%%) ⊢ (??%?); >sss_result_proj <sss_result_hyp normalize nodelta 4023 >(Hsim … Heq_lhs) whd in match (m_bind ?????); 4024 >(Hsim_expr … Heq_rhs) >bindIO_Value 4025 lapply (memext_store_value_of_type' sss_m sss_m_ext xs sss_writeable (typeof lhs) (\fst xl) (\fst xr) sss_mem_hyp ?) 4026 [ 1: cases (store_value_of_type' ????) in Heq_store; 4027 [ 1: normalize #Habsurd destruct (Habsurd) 4028 | 2: #m normalize #Heq destruct (Heq) @refl ] ] 4029 * #m_ext' * #Hstore_eq #Hnew_ext >Hstore_eq whd in match (m_bind ?????); 4030 whd destruct @conj try @refl 4031 %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip sss_lu) } try // try assumption 4032 [ 1: @(fresh_for_Sskip … sss_lu_fresh) 4033 | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 4034 | 3: (* Call statement *) 4035 #Hexec %{0} whd in sss_result_hyp:(??%?); destruct (sss_result_hyp) 4036 whd whd in ⊢ (??%?); >sss_result_proj normalize nodelta 4037 whd in Hexec:(??%?); 4038 cases (bindIO_inversion ??????? Hexec) #xfunc * #Heq_func #Hexec_func 4039 cases (bindIO_inversion ??????? Hexec_func) #xargs * #Heq_args #Hexec_args 4040 cases (bindIO_inversion ??????? Hexec_args) #called_fundef * #Heq_fundef #Hexec_typeeq 4041 cases (bindIO_inversion ??????? Hexec_typeeq) #Htype_eq * #Heq_assert #Hexec_ret 4042 >(Hsim_expr … Heq_func) whd in match (m_bind ?????); 4043 >(exec_expr_sim_to_exec_exprlist … Hsim_expr … Heq_args) 4044 whd in ⊢ (??%?); 4045 >(rg_find_funct … Hrelated … (opt_to_io_Value … Heq_fundef)) 4046 whd in ⊢ (??%?); <fundef_type_simplify >Heq_assert 4047 whd in ⊢ (??%?); -Hexec -Hexec_func -Hexec_args -Hexec_typeeq lapply Hexec_ret -Hexec_ret 4048 @(option_ind … retv) normalize nodelta 4049 [ 1: whd in ⊢ ((??%%) → (??%%)); #Heq whd destruct (Heq) @conj try @refl 4050 %2{sss_writeable … sss_mem_hyp} 4051 cases called_fundef 4052 [ 2: #id #tl #ty @I 4053 | 1: #called_function whd 4054 cut (sss_func_tr = \fst (function_switch_removal sss_func)) 4055 [ 1: <sss_func_hyp @refl ] #H >H -H 4056 cut (sss_new_vars = \snd (function_switch_removal sss_func)) 4057 [ 1: <sss_func_hyp @refl ] #H >H -H 4058 @(swc_call … sss_k_hyp) try assumption 4059 <sss_func_hyp @refl ] 4060 | 2: #ret_expr #Hexec_ret_expr 4061 cases (bindIO_inversion ??????? Hexec_ret_expr) #xret * #Heq_ret 4062 whd in ⊢ ((??%%) → (??%%)); #H destruct (H) 4063 >(exec_lvalue_sim_aux … Hsim_lvalue … Heq_ret) 4064 whd in ⊢ (??%?); whd @conj try @refl 4065 cut (sss_func_tr = \fst (function_switch_removal sss_func)) 4066 [ 1: <sss_func_hyp @refl ] #H >H -H 4067 @(sws_callstate … sss_writeable … sss_mem_hyp) 4068 cases called_fundef 4069 [ 2: #id #tl #ty @I 4070 | 1: #called_function whd 4071 cut (sss_func_tr = \fst (function_switch_removal sss_func)) 4072 [ 1: <sss_func_hyp @refl ] #H >H -H 4073 cut (sss_new_vars = \snd (function_switch_removal sss_func)) 4074 [ 1: <sss_func_hyp @refl ] #H >H -H 4075 @(swc_call … sss_k_hyp) try assumption 4076 <sss_func_hyp @refl ] ] 4077 | 4: (* Sequence statement *) 4078 #Hexec %{0} whd in sss_result_hyp:(??%?); whd whd in Hexec:(??%?) ⊢ (??%?); destruct (Hexec) 4079 >sss_result_proj <sss_result_hyp 4080 cases (switch_removal_elim stm1 sss_lu) #stm1' * #fvs1' * #u' #HeqA >HeqA normalize nodelta 4081 cases (switch_removal_elim stm2 u') #stm2' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta 4082 normalize @conj try @refl %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try // 4083 [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * // 4084 | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta 4085 /2 by All_append_l/ 4086 | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 4087 @(swc_seq … u') try // 4088 [ 2: >HeqB @refl 4089 | 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * #_ @fresher_for_univ 4090 lapply (switch_removal_fte stm1 sss_lu) >HeqA #H @H 4091 | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta 4092 /2 by All_append_r/ 4093 ] 4094 | 5: (* If-then-else *) 4095 #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp 4096 cases (switch_removal_elim iftrue sss_lu) #iftrue' * #fvs1' * #u' #HeqA >HeqA normalize nodelta 4097 cases (switch_removal_elim iffalse u') #iffalse' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta 4098 whd whd in ⊢ (??%?); 4099 cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond 4100 cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hresult 4101 whd in Hresult:(??%%); destruct (Hresult) 4102 >(Hsim_expr … Heq_cond) >bindIO_Value 4103 >Heq_bool whd in match (m_bind ?????); whd @conj try @refl 4104 cases b normalize nodelta 4105 [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try // 4106 [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize // 4107 | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta 4108 /2 by All_append_l/ 4109 | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 4110 | 2: %1{u' … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqB} try assumption try // 4111 [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize #_ 4112 @fresher_for_univ lapply (switch_removal_fte iftrue sss_lu) >HeqA #H @H 4113 | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta 4114 /2 by All_append_r/ 4115 | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ] 4116 | 6: (* While loop *) 4117 #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp 4118 >sss_result_proj <sss_result_hyp whd 4119 cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond 4120 cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool whd in ⊢ ((??%%) → ?); 4121 cases (switch_removal_elim body sss_lu) #body' * #fvs1' * #u' #HeqA >HeqA normalize nodelta 4122 whd in ⊢ (? → (??%?)); 4123 >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool 4124 whd in match (m_bind ?????); cases b normalize nodelta #Hresult destruct (Hresult) 4125 whd @conj try @refl 4126 [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try // 4127 [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize // 4128 | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H 4129 | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 4130 | 3: @(swc_while … sss_lu) try // 4131 [ 1: >HeqA @refl 4132 | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H ] 4133 ] 4134 | 2: %{… sss_func_hyp … (switch_removal Sskip u')} try assumption try // 4135 [ 1: lapply (switch_removal_fte body sss_lu) >HeqA #Hfte whd in match (ret_u ??) in Hfte; 4136 @(fresher_for_univ … Hfte) @(fresh_for_Sskip … sss_lu_fresh) 4137 | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ] 4138 | 7: (* do while loop *) 4139 #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp 4140 >sss_result_proj <sss_result_hyp whd destruct (Hexec) whd in ⊢ (??%?); 4141 cases (switch_removal_elim body sss_lu) #body' * #fvs1' * #u' #HeqA >HeqA normalize nodelta 4142 whd @conj try @refl 4143 %1{sss_lu … sss_func_hyp … (switch_removal body sss_lu) } 4144 try assumption try // 4145 [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * // 4146 | 2: >HeqA @refl 4147 | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H 4148 | 5: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 4149 | 4: @(swc_dowhile … sss_lu) try assumption try // 4150 [ 1: >HeqA @refl 4151 | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H 4152 ] ] 4153 | 8: (* for loop *) 4154 #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp 4155 >sss_result_proj <sss_result_hyp whd destruct (Hexec) whd in ⊢ (??%?); 4156 cases (switch_removal_elim init sss_lu) #init' * #fvs1' * #u' #HeqA >HeqA normalize nodelta 4157 cases (switch_removal_elim step u') #step' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta 4158 cases (switch_removal_elim body u'') #body' * #fvs3' * #u''' #HeqC >HeqC normalize nodelta 4159 lapply Hexec 4160 @(match is_Sskip init with 4161 [ inl Heq ⇒ ? 4162 | inr Hneq ⇒ ? 4163 ]) normalize nodelta 4164 [ 2: lapply (simplify_is_not_skip … Hneq sss_lu) >HeqA * #pf 4165 whd in match (ret_st ??) in ⊢ ((??%%) → ?); #Hneq >Hneq normalize nodelta 4166 #Hexec' whd in Hexec':(??%%); destruct (Hexec') whd @conj try @refl 4167 %1{sss_lu … sss_func_hyp (switch_removal init sss_lu)} try assumption try // 4168 [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * * * // 4169 | 2: >HeqA @refl 4170 | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta 4171 >HeqB normalize nodelta >HeqC normalize nodelta 4172 /2 by All_append_l/ 4173 | 4: @(swc_for1 … u') try assumption try // 4174 [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #HW #HX #HY #HZ 4175 @for_fresh_lift 4176 [ 1: @(fresher_for_univ … HY) 4177 | 2: @(fresher_for_univ … HZ) 4178 | 3: @(fresher_for_univ … HX) ] 4179 lapply (switch_removal_fte init sss_lu) >HeqA #Hs @Hs 4180 | 2: normalize >HeqB normalize nodelta >HeqC @refl 4181 | 3: lapply sss_incl <sss_result_hyp 4182 whd in match (ret_vars ??) in ⊢ (% → %); 4183 whd in match (switch_removal ??) in ⊢ (% → %); 4184 >HeqA normalize nodelta >HeqB normalize nodelta >HeqC 4185 normalize nodelta #H /2 by All_append_r/ 4186 ] ] 4187 | 1: -Hexec #Hexec' cases (bindIO_inversion ??????? Hexec') #condres * #Heq_cond #Hexec_cond 4188 cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool 4189 destruct (Heq) normalize in HeqA; lapply HeqA #HeqA' destruct (HeqA') 4190 normalize nodelta 4191 >(Hsim_expr … Heq_cond) whd in ⊢ ((??%?) → ?); #Hexec' 4192 whd in match (m_bind ?????); >Heq_bool 4193 cases b in Hexec'; normalize nodelta whd in match (bindIO ??????); 4194 normalize #Hexec'' destruct (Hexec'') @conj try @refl 4195 [ 1: %1{u'' … sss_func_hyp (switch_removal body u'')} try assumption try // 4196 [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #_ #_ #_ 4197 @fresher_for_univ lapply (switch_removal_fte step u') >HeqB 4198 #H @H 4199 | 2: >HeqC @refl 4200 | 3: lapply sss_incl <sss_result_hyp 4201 whd in match (ret_vars ??) in ⊢ (% → %); 4202 whd in match (switch_removal ??) in ⊢ (% → %); normalize nodelta 4203 >HeqB normalize nodelta >HeqC normalize nodelta 4204 /2 by All_append_r/ 4205 | 4: @(swc_for2 … u') try assumption 4206 [ 1: >HeqB @refl 4207 | 2: >HeqB >HeqC @refl 4208 | 3: lapply sss_incl <sss_result_hyp 4209 whd in match (ret_vars ??) in ⊢ (% → %); 4210 whd in match (switch_removal ??) in ⊢ (% → %); normalize nodelta 4211 >HeqB normalize nodelta >HeqC normalize nodelta #H @H 4212 ] 4213 ] 4214 | 2: %1{u' … sss_func_hyp … (switch_removal Sskip u')} try assumption try // 4215 [ 1: @(fresh_for_Sskip … sss_lu_fresh) ] ] ] 4216 #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 4217 | 9: (* break *) 4218 #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta 4219 lapply Hexec -Hexec 4220 inversion sss_k_hyp 4221 [ 1: #new_vars #Hv #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Habsurd destruct (Habsurd) 4222 | 2: #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars_eq 4223 #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl 4224 destruct 4225 %1{sss_lu … (switch_removal Sbreak sss_lu)} try assumption try // 4226 | 3,4: #e #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ 4227 #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl 4228 destruct 4229 %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try // 4230 | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ 4231 #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl 4232 destruct 4233 %1{sss_lu … (switch_removal Sbreak sss_lu)} try assumption try // 4234 | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk' 4235 #Hres1 #Hres2 #Hincl #_ #Hnew_vars 4236 #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl 4237 destruct 4238 %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try // 4239 | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk' #_ #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); 4240 #Heq destruct (Heq) whd @conj try @refl destruct 4241 %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try // 4242 | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold #Hdisjoint #_ 4243 #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); 4244 #Heq destruct (Heq) ] 4245 #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 4246 | 10: (* continue *) 4247 #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta 4248 lapply Hexec -Hexec 4249 inversion sss_k_hyp 4250 [ 1: #new_vars #Hv #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Habsurd destruct (Habsurd) 4251 | 2: #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars_eq 4252 #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl 4253 destruct 4254 %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // 4255 | 3: #ek #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ 4256 #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl 4257 destruct 4258 %1{uk … (switch_removal (Swhile ek sk) uk)} try assumption try // 4259 [ 1: normalize cases (switch_removal sk uk) * #sk' #fvs' #uk' @refl 4260 | 2: whd in match (switch_removal ??); lapply Hincl 4261 cases (switch_removal sk uk) * #body' #fvs' #uk' 4262 /2 by All_append_r/ ] 4263 | 4: #ek #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ 4264 #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Hexec 4265 cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond 4266 cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hexec_bool 4267 >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool whd in match (m_bind ?????); 4268 cases b in Hexec_bool; normalize nodelta whd in ⊢ ((??%?) → ?); 4269 #Heq whd whd in Heq:(??%%); destruct (Heq) @conj try @refl 4270 [ 1: destruct %1{uk … (switch_removal (Sdowhile ek sk) uk)} try assumption try // 4271 [ 1: normalize cases (switch_removal sk uk) * #body' #fvs' #uk' @refl 4272 | 2: whd in match (switch_removal ??); lapply Hincl cases (switch_removal sk uk) 4273 * #body' #fvs' #uk' #H @H 4274 ] 4275 | 2: destruct %1{uk … (switch_removal Sskip uk)} try assumption try // 4276 try @(fresh_for_Sskip … Hfresh_suk) ] 4277 | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ 4278 #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl 4279 destruct %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // 4280 | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk' #Hres1 #Hres2 #Hincl #_ 4281 #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl 4282 destruct %1{uk … (switch_removal s1k uk)} try assumption try // 4283 [ 1: cases (fresh_to_substatements … Hfresh_suk) * * // 4284 | 2: lapply Hincl whd in match (ret_vars ??) in ⊢ (% → ?); 4285 whd in match (switch_removal ??); 4286 cases (switch_removal s1k uk) * #s1k' #fvs1' #uk' normalize nodelta 4287 cases (switch_removal s2k uk') * #s2k' #fvs2' #uk'' normalize nodelta 4288 /2 by All_append_l/ 4289 | 3: @(swc_for3 … uk) try assumption try // 4290 ] 4291 | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk #_ #Hnew_vars_eq #Hk #Hk' #_ 4292 whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) 4293 whd @conj try @refl destruct 4294 %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // 4295 | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold_vars_eq #Hdisjoint 4296 #_ #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); 4297 #Heq destruct (Heq) ] 4298 #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 4299 | 11: (* return *) 4300 #Hexec %{0} whd whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec 4301 >sss_result_proj <sss_result_hyp normalize nodelta 4302 cases retval in sss_lu_fresh sss_result_hyp; normalize nodelta 4303 [ 1: #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?)); 4304 >(prod_eq_lproj ????? sss_func_hyp) 4305 >fn_return_simplify 4306 cases (fn_return sss_func) normalize nodelta 4307 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 4308 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] 4309 [ 1: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj try @refl 4310 /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/ 4311 | *: #Habsurd destruct (Habsurd) ] 4312 | 2: #ret_expr #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?)); 4313 >(prod_eq_lproj ????? sss_func_hyp) 4314 >fn_return_simplify 4315 @(match type_eq_dec (fn_return sss_func) Tvoid with 4316 [ inl H ⇒ ? 4317 | inr H ⇒ ? ]) normalize nodelta 4318 [ 1: #Habsurd destruct (Habsurd) 4319 | 2: #Hexec 4320 cases (bindIO_inversion ??????? Hexec) #retres * #Heq_ret #Hexec_ret 4321 whd in Hexec_ret:(??%%); destruct (Hexec_ret) 4322 >(Hsim_expr … Heq_ret) whd in match (m_bind ?????); whd 4323 @conj try @refl 4324 /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/ 4325 ] ] 4326 | 12: (* switch ! at long last *) 4327 #Hexec whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec 4328 >sss_result_proj <sss_result_hyp normalize nodelta #Hexec 4329 cases (bindIO_inversion ??????? Hexec) * #condval #condtrace 4330 cases condval normalize nodelta 4331 [ 1: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 4332 | 3: #f * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 4333 | 4: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 4334 | 5: #ptr * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ] 4335 #sz #i * #Hexec_eq #Heq whd in Heq:(??%%); destruct (Heq) 4336 4337 cases (switch_removal_branches_elim … switchcases sss_lu) #switchcases' * #fvs' * #u' #Hbranch_eq 4338 >Hbranch_eq normalize nodelta 4339 cases (fresh_elim … u') #new * #u'' #Hfresh_eq >Hfresh_eq normalize nodelta 4340 cases (simplify_switch_elim (Expr (Evar new) (typeof cond)) switchcases' u'') #simplified * #u''' 4341 #Hswitch_eq >Hswitch_eq normalize nodelta 4342 %{1} whd whd in ⊢ (??%?); 4343 (* A. Execute lhs of assign, i.e. fresh variable that will hold value of condition *) 4344 whd in match (exec_lvalue ????); 4345 (* show that the resulting ident is in the memory extension and that the lookup succeeds *) 4346 -Hexec >Hbranch_eq in sss_result_hyp; normalize nodelta 4347 >Hfresh_eq normalize nodelta >Hswitch_eq normalize nodelta #sss_result_hyp 4348 <sss_result_hyp in sss_incl; whd in match (ret_vars ??); #sss_incl 4349 cases sss_env_hyp * 4350 #Hlookup_new_in_old 4351 #Hlookup_new_in_new 4352 #Hlookup_old 4353 lapply (Hlookup_new_in_new new ?) 4354 [ 1: cases sss_incl #Hmem #_ elim sss_new_vars in Hmem; 4355 [ 1: @False_ind 4356 | 2: * #hdv #hdty #tl #Hind whd in ⊢ (% → (??%?)); * 4357 [ 1: #Heq destruct (Heq) 4358 cases (identifier_eq_i_i … hdv) #Hrefl #Heq >Heq -Heq normalize nodelta 4359 @refl 4360 | 2: #Hmem lapply (Hind Hmem) #Hmem_in_tl 4361 cases (identifier_eq ? new hdv) normalize nodelta 4362 [ 1: #_ @refl | 2: #_ @Hmem_in_tl ] ] ] ] 4363 * #res #Hlookup >Hlookup normalize nodelta whd in match (bindIO ??????); 4364 (* B. Reduce rhs of assign, i.e. the condition. Do this using simulation hypothesis. *) 4365 >(Hsim_expr … Hexec_eq) >bindIO_Value 4366 (* C. Execute assign. We must prove that this cannot fail. In order for the proof to proceed, we need 4367 to set up things so that loading from that fresh location will yield exactly the stored value. *) 4368 normalize in match store_value_of_type'; normalize nodelta 4369 @cthulhu 4370 | *: @cthulhu ] 4371 | *: @cthulhu ] qed.
Note: See TracChangeset
for help on using the changeset viewer.