Changeset 2737 for src/Clight
 Timestamp:
 Feb 26, 2013, 7:37:41 PM (8 years ago)
 Location:
 src/Clight
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Clight_abstract.ma
r2677 r2737 50 50 definition ClState ≝ State. 51 51 52 definition ClReturnstate ≝ Returnstate. 53 54 definition ClCallstate ≝ Callstate. 55 52 56 definition ClKseq ≝ Kseq. 
src/Clight/toCminorCorrectness.ma
r2667 r2737 5 5 include "Clight/Clight_abstract.ma". 6 6 include "Cminor/Cminor_abstract.ma". 7 include "common/Measurable.ma". 7 8 8 9 (* Expr simulation. Contains important definitions for statements, too. *) 9 10 include "Clight/toCminorCorrectnessExpr.ma". 10 11 11 12 12 (* When we characterise the local Clight variables, those that are stack 13 13 allocated are given disjoint regions of the stack. *) 14 15 14 lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty. 16 15 characterise_vars globals f = 〈vartypes, stacksize〉 → … … 233 232 ] qed. 234 233 235 236 (* This is the statement for expression simulation copied from toCminorCorrectnessExpr.ma, 237 for easier reference. 238 lemma eval_expr_sim : 239 (* [cl_cm_inv] maps CL globals to CM globals, including functions *) 240 ∀cl_cm_inv : clight_cminor_inv. 241 (* current function (defines local environment) *) 242 ∀f : function. 243 ∀data : clight_cminor_data f cl_cm_inv. 244 (* clight expr to cminor expr *) 245 (∀(e:expr). 246 ∀(e':CMexpr (typ_of_type (typeof e))). 247 ∀Hexpr_vars. 248 translate_expr (alloc_type ?? data) e = OK ? («e', Hexpr_vars») → 249 ∀cl_val,trace,Hyp_present. 250 exec_expr (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) e = OK ? 〈cl_val, trace〉 → 251 ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧ 252 value_eq (E ?? data) cl_val cm_val) ∧ 253 (* clight /lvalue/ to cminor /expr/ *) 254 (∀ed,ty. 255 ∀(e':CMexpr ASTptr). 256 ∀Hexpr_vars. 257 translate_addr (alloc_type ?? data) (Expr ed ty) = OK ? («e', Hexpr_vars») → 258 ∀cl_blo,cl_off,trace,Hyp_present. 259 exec_lvalue' (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) ed ty = OK ? 〈cl_blo, cl_off, trace〉 → 260 ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧ 261 value_eq (E ?? data) (Vptr (mk_pointer cl_blo cl_off)) cm_val). 262 *) 263 264 definition foo ≝ 3. 234 (* A measure on Clight states that is decreasing along execution sequences *) 235 236 (* statements *) 237 let rec measure_Clight_statement (s : statement) : ℕ ≝ 238 match s with 239 [ Sskip ⇒ 0 240  Ssequence s1 s2 ⇒ 241 measure_Clight_statement s1 + measure_Clight_statement s2 + 1 242  Sifthenelse e s1 s2 => 243 measure_Clight_statement s1 + measure_Clight_statement s2 + 1 244  Swhile e s => 245 measure_Clight_statement s + 1 246  Sdowhile e s => 247 measure_Clight_statement s + 1 248  Sfor s1 e s2 s3 => 249 measure_Clight_statement s1 + 250 measure_Clight_statement s2 + 251 measure_Clight_statement s3 + 1 252  Sswitch e ls => 253 measure_Clight_ls ls + 1 254  Slabel l s => 255 measure_Clight_statement s + 1 256  Scost cl s => 257 measure_Clight_statement s + 1 258  _ => 1 259 ] 260 and measure_Clight_ls (ls : labeled_statements) : ℕ := 261 match ls with 262 [ LSdefault s => 263 measure_Clight_statement s 264  LScase sz i s ls => 265 measure_Clight_statement s + 266 measure_Clight_ls ls 267 ]. 268 269 (* continuations *) 270 let rec measure_Clight_cont (cont : cl_cont) : ℕ ≝ 271 match cont with 272 [ Kstop => 0 273  Kseq s k => 274 measure_Clight_statement s + 275 measure_Clight_cont k + 1 276  Kwhile e s k => 277 measure_Clight_statement s + 278 measure_Clight_cont k + 1 279  Kdowhile e s k => 280 measure_Clight_statement s + 281 measure_Clight_cont k + 1 282  Kfor2 e s1 s2 k => 283 measure_Clight_statement s1 + 284 measure_Clight_statement s2 + 285 measure_Clight_cont k + 1 286  Kfor3 e s1 s2 k => 287 measure_Clight_statement s1 + 288 measure_Clight_statement s2 + 289 measure_Clight_cont k + 1 290  Kswitch k => 291 measure_Clight_cont k + 1 292  Kcall retaddr f e k => 293 measure_Clight_statement (fn_body f) + 294 measure_Clight_cont k + 1 295 ]. 296 297 (* Shamelessly copying Compcert. *) 298 definition measure_Clight : Clight_state → ℕ × ℕ ≝ 299 λstate. 300 match state with 301 [ State f s k e m ⇒ 302 〈measure_Clight_statement s + measure_Clight_cont k + 1, measure_Clight_statement s + 1〉 303  Callstate fb fd args k m ⇒ 〈0, 0〉 304  Returnstate res k m ⇒ 〈0, 0〉 305  Finalstate r ⇒ 〈0, 0〉 306 ]. 307 308 (* Stuff on lexicographic orders *) 309 definition lexicographic : ∀A:Type[0]. (A → A → Prop) → A × A → A × A → Prop ≝ 310 λA,Ord, x, y. 311 let 〈xa, xb〉 ≝ x in 312 let 〈ya, yb〉 ≝ y in 313 Ord xa ya ∨ (xa = ya ∧ Ord xb yb). 314 315 definition lex_lt ≝ lexicographic nat lt. 316 265 317 266 318 (* relate Clight continuations and Cminor ones. *) 267 319 inductive clight_cminor_cont_rel : 268 ∀INV: clight_cminor_inv. (* stuff on global variables and functions (matching between CL and CM) *) 269 ∀cl_f: function. (* current Clight function *) 270 internal_function → (* current Cminor function *) 271 clight_cminor_data cl_f INV → (* data for the current stack frame in CL and CM *) 272 option typ → (* optional target type  uniform over a given function *) 273 cl_cont → (* CL cont *) 274 cm_cont → (* CM cont *) 320 ∀cl_ge, cm_ge. 321 ∀INV: clight_cminor_inv cl_ge cm_ge. (* stuff on global variables and functions (matching between CL and CM) *) 322 ∀cl_f: function. (* current Clight function *) 323 internal_function → (* current Cminor function *) 324 clight_cminor_data cl_f cl_ge cm_ge INV → (* data for the current stack frame in CL and CM *) 325 option typ → (* optional target type  uniform over a given function *) 326 cl_cont → (* CL cont *) 327 cm_cont → (* CM cont *) 275 328 Prop ≝ 276 329  ClCm_cont_stop: 277 ∀ INV, cl_f, cm_f, frame_data, target_type.278 clight_cminor_cont_rel INV cl_f cm_f frame_data target_type Kstop Kend330 ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type. 331 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type Kstop Kend 279 332  ClCm_cont_seq: 280 ∀ INV, cl_f, cm_f, frame_data, target_type.333 ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type. 281 334 ∀cl_s: statement. 282 335 ∀cm_s: stmt. … … 288 341 ∀flag. 289 342 ∀Htranslate_inv. 290 translate_statement (alloc_type ??frame_data) stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →291 clight_cminor_cont_rel INV cl_f cm_f frame_data target_type cl_k' cm_k' →292 clight_cminor_cont_rel INV cl_f cm_f frame_data target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')343 translate_statement (alloc_type … frame_data) stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 344 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type cl_k' cm_k' → 345 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') 293 346  ClCm_cont_while: 294 347 (* Inductive family parameters *) 295 ∀ INV, cl_f, cm_f, frame_data, target_type.348 ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type. 296 349 297 350 (* subcontinuations *) … … 317 370 (* relate CL and CM expressions *) 318 371 ∀Hexpr_vars. 319 translate_expr (alloc_type ??frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →372 translate_expr (alloc_type … frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») → 320 373 321 374 (* Parameters and results to find_label_always *) 322 ∀sInv: stmt_inv cm_f (cm_env ??frame_data) (f_body cm_f).375 ∀sInv: stmt_inv cm_f (cm_env … frame_data) (f_body cm_f). 323 376 ∀Hinv. 324 377 325 378 (* Specify how the labels for the whilereplacing gotos are produced *) 326 379 mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 → 327 translate_statement (alloc_type ??frame_data) stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» →328 find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f (cm_env ??frame_data) sInv I =380 translate_statement (alloc_type … frame_data) stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» → 381 find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f (cm_env … frame_data) sInv I = 329 382 «〈St_label entry 330 383 (St_seq 331 384 (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip) 332 385 (St_label exit St_skip)), cm_k'〉, Hinv» → 333 clight_cminor_cont_rel INV cl_f cm_f frame_data target_type cl_k' cm_k' → 334 clight_cminor_cont_rel INV cl_f cm_f frame_data target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')). 335 336 337 (* The type of maps from labels to Clight continuations *) 338 (* definition label_map ≝ identifier_map SymbolTag cont. *) 386 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type cl_k' cm_k' → 387 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')). 339 388 340 389 (* Definition of the simulation relation on states. The orders of the parameters is dictated by 341 390 * the necessity of performing an inversion on the continuation sim relation without having to 342 391 * play the usual game of lapplying all previous dependent arguments. *) 343 inductive clight_cminor_rel : clight_cminor_inv→ Clight_state → Cminor_state → Prop ≝392 inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge → Clight_state → Cminor_state → Prop ≝ 344 393  CMR_normal : 394 ∀cl_ge, cm_ge. 345 395 (* Relates globals to globals and functions to functions. *) 346 ∀INV: clight_cminor_inv .396 ∀INV: clight_cminor_inv cl_ge cm_ge. 347 397 348 398 (*  Statements  *) … … 357 407 ∀cl_f: function. (* Clight enclosing function *) 358 408 ∀cm_f: internal_function. (* enclosing function *) 359 ∀frame_data: clight_cminor_data cl_f INV. 360 (*∀alloctype: var_types.*) (* map from var to alloc type *) 409 ∀frame_data: clight_cminor_data cl_f ?? INV. 361 410 ∀rettyp. (* return type of the function *) 362 411 363 412 (*  Relate Clight continuation to Cminor continuation  *) 364 clight_cminor_cont_rel INV cl_f cm_f frame_data rettyp cl_k cm_k →413 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data rettyp cl_k cm_k → 365 414 366 415 (*  Other Cminor variables  *) 367 ∀fInv: stmt_inv cm_f (cm_env ??frame_data) (f_body cm_f). (* Cminor invariants *)368 ∀sInv: stmt_inv cm_f (cm_env ??frame_data) cm_s.369 ∀kInv: cont_inv cm_f (cm_env ??frame_data) cm_k.416 ∀fInv: stmt_inv cm_f (cm_env … frame_data) (f_body cm_f). (* Cminor invariants *) 417 ∀sInv: stmt_inv cm_f (cm_env … frame_data) cm_s. 418 ∀kInv: cont_inv cm_f (cm_env … frame_data) cm_k. 370 419 371 420 (*  Relate return type variable to actual return type  *) … … 376 425 (*  relate Clight and Cminor functions  *) 377 426 ∀func_univ: universe SymbolTag. 378 ∀Hfresh_globals: globals_fresh_for_univ ? (globals INV) func_univ.427 ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ. 379 428 ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ. 380 translate_function func_univ (globals INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →429 translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f → 381 430 382 431 (*  relate Clight and Cminor statements  *) 383 ∀stmt_univ,stmt_univ': tmpgen (alloc_type ??frame_data).432 ∀stmt_univ,stmt_univ': tmpgen (alloc_type … frame_data). 384 433 ∀lbl_univ,lbl_univ': labgen. 385 434 ∀lbls: lenv. 386 435 ∀flag: convert_flag. 387 436 ∀Htranslate_inv. 388 translate_statement (alloc_type ??frame_data) stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →437 translate_statement (alloc_type … frame_data) stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 389 438 390 clight_cminor_rel INV 391 (ClState cl_f cl_s cl_k (cl_env ?? frame_data) (cl_m ?? frame_data)) 392 (CmState cm_f cm_s (cm_env ?? frame_data) fInv sInv (cm_m ?? frame_data) (stackptr ?? frame_data) cm_k kInv cm_st). 439 clight_cminor_rel cl_ge cm_ge INV 440 (ClState cl_f cl_s cl_k (cl_env … frame_data) (cl_m … frame_data)) 441 (CmState cm_f cm_s (cm_env … frame_data) fInv sInv (cm_m … frame_data) (stackptr … frame_data) cm_k kInv cm_st) 442 443  CMR_return : 444 ∀cl_ge, cm_ge, cl_f. 445 ∀INV: clight_cminor_inv cl_ge cm_ge. 446 ∀frame_data: clight_cminor_data cl_f ?? INV. 447 ∀cl_mem, cm_mem. 448 cl_mem = cl_m … frame_data → 449 cm_mem = cm_m … frame_data → 450 ∀cm_st: stack. (* Cminor stack *) 451 clight_cminor_rel cl_ge cm_ge INV 452 (ClReturnstate Vundef Kstop cl_mem) 453 (CmReturnstate (None val) cm_mem cm_st) 454 455  CMR_call : 456 ∀cl_ge, cm_ge, cl_f, cm_f. 457 ∀INV: clight_cminor_inv cl_ge cm_ge. 458 ∀frame_data: clight_cminor_data cl_f cl_ge cm_ge INV. 459 ∀u: universe SymbolTag. 460 ∀cl_fundef, cm_fundef. 461 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u. 462 ∀Hfundef_fresh: fd_fresh_for_univ cl_fundef u. 463 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) → 464 ∀cl_k, cm_k. 465 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data rettyp cl_k cm_k → 466 ∀fblock. 467 match cl_fundef with 468 [ CL_Internal cl_function ⇒ 469 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧ 470 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧ 471 translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef 472  CL_External name argtypes rettype ⇒ 473 True 474 ] → 475 ∀fptr_block. 476 ∀sInv, fInv, kInv. 477 ∀cl_args_values, cm_args_values. 478 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *) 479 ∀cm_stack. 480 clight_cminor_rel cl_ge cm_ge INV 481 (ClCallstate (Vptr (mk_pointer fptr_block zero_offset)) 482 cl_fundef cl_args_values 483 (Kcall (None (block×offset×type)) cl_f (cl_env ???? frame_data) cl_k) 484 (cl_m ???? frame_data)) 485 (CmCallstate (Vptr (mk_pointer fptr_block zero_offset)) cm_fundef 486 cm_args_values (cm_m ???? frame_data) 487 (Scall (None (ident×typ)) cm_f (stackptr ???? frame_data) (cm_env ???? frame_data) sInv fInv cm_k kInv cm_stack)). 488 489 definition clight_normal : Clight_state → bool ≝ 490 λs. match Clight_classify s with [ cl_other ⇒ true  cl_jump ⇒ true  _ ⇒ false ]. 491 492 definition cminor_normal : Cminor_state → bool ≝ 493 λs. match Cminor_classify s with [ cl_other ⇒ true  cl_jump ⇒ true  _ ⇒ false ]. 494 495 definition cl_pre : preclassified_system ≝ 496 mk_preclassified_system 497 clight_fullexec 498 (λg. Clight_labelled) 499 (λg. Clight_classify) 500 (λf,g,s,H. 0). (* XXX TODO *) 501 502 definition cm_pre : preclassified_system ≝ 503 mk_preclassified_system 504 Cminor_fullexec 505 (λg. Cminor_labelled) 506 (λg. Cminor_classify) 507 (λf,g,s,H. 0). (* XXX TODO *) 508 509 (* Auxilliary lemmas. *) 393 510 394 511 lemma invert_assert : … … 411 528 qed. 412 529 413 414 (* axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop. *) 530 lemma jmeq_absorb : ∀A:Type[0]. ∀a,b: A. ∀P:Prop. (a = b → P) → a ≃ b → P. 531 #A #a #b #P #H #Heq lapply (jmeq_to_eq ??? Heq) #Heq' @H @Heq' qed. 532 533 (* wrap up some trivial bit of reasoning to alleviate strange destruct behaviour *) 534 lemma pair_eq_split : 535 ∀A,B:Type[0]. ∀a1,a2:A. ∀b1,b2:B. 536 〈a1,b1〉 = 〈a2, b2〉 → 537 a1 = a2 ∧ b1 = b2. 538 #A #B #a1 #a2 #b1 #b2 #Heq destruct (Heq) @conj try @refl 539 qed. 540 541 lemma ok_eq_ok_destruct : 542 ∀A:Type[0]. ∀a,b:A. OK ? a = OK ? b → a = b. 543 #H1 #H2 #H3 #H4 destruct @refl qed. 544 545 lemma sigma_eq_destruct : ∀A:Type[0]. ∀a,b:A. ∀P: A → Prop. ∀Ha: P a. ∀Hb: P b. «a, Ha» = «b,Hb» → a = b ∧ Ha ≃ Hb. 546 #A #a #b #P #Ha #Hb #Heq destruct (Heq) 547 @conj try % 548 qed. 549 550 (* inverting find_funct and find_funct_ptr *) 551 lemma find_funct_inversion : 552 ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀res: F. 553 find_funct F ge v = Some ? res → 554 (∃ptr. v = Vptr ptr ∧ 555 (poff ptr) = zero_offset ∧ 556 block_region (pblock ptr) = Code ∧ 557 (∃p. block_id (pblock ptr) = neg p ∧ 558 lookup_opt … p (functions … ge) = Some ? res)). 559 #F #ge #v #res 560 cases v 561 [  #sz #i   #ptr ] 562 whd in ⊢ ((??%?) → ?); 563 #Heq destruct (Heq) 564 %{ptr} @conj try @conj try @conj try @refl 565 lapply Heq Heq 566 @(eq_offset_elim … (poff ptr) zero_offset) // 567 normalize nodelta 568 [ 1,3,5: #_ #Habsurd destruct (Habsurd) ] 569 #Heq destruct (Heq) 570 whd in ⊢ ((??%?) → ?); 571 cases ptr #blo #off cases (block_region blo) normalize nodelta 572 [ 1,3: #Habsurd destruct (Habsurd) ] 573 [ // ] 574 cases (block_id blo) normalize nodelta 575 [ #Habsurd destruct (Habsurd)  #p #Habsurd destruct (Habsurd) ] 576 #p #Hlookup %{p} @conj try @refl assumption 577 qed. 578 579 (* We should be able to prove that ty = ty' with some more hypotheses, if needed. *) 580 lemma translate_dest_id_inversion : 581 ∀var_types, e, var_id, ty,H. 582 translate_dest var_types e = return IdDest var_types var_id ty H → 583 e = Expr (Evar var_id) (typeof e). 584 @cthulhu 585 (* 586 #vars #e #var_id #ty #H 587 cases e #ed #ty' 588 cases ed 589 [ #sz #i  #id  #e1  #e1  #op #e1 #op #e1 #e2  #cast_ty #e1 590  #cond #iftrue #iffalse  #e1 #e2  #e1 #e2  #sizeofty  #e1 #field  #cost #e1 ] 591 whd in ⊢ ((??%%) → ?); 592 #Heq 593 [ 1,4,5,6,7,8,9,10,11,13: destruct (Heq) 594  3,12: cases (bind_inversion ????? Heq) * #H1 #H2 #H3 cases H3 595 #_ whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ] 596 lapply Heq Heq 597 change with (bind2_eq ????? ) in ⊢ ((??%?) → ?); #Heq 598 cases (bind2_eq_inversion ?????? Heq) 599 #alloctype 600 (* * #alloctype *) * #typ' * 601 cases alloctype 602 [ #r  #n  ] normalize nodelta #Hlookup' 603 [ 1,2: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ] 604 whd in ⊢ ((??%%) → ?); #Heq' destruct (Heq') 605 @refl*) 606 qed. 607 608 609 (* Note: duplicate in switchRemoval.ma *) 610 lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed. 611 612 lemma breakup_dependent_match_on_pairs : 613 ∀A,B,C: Type[0]. 614 ∀term: A × B. 615 ∀F: ∀x,y. 〈x, y〉 = term → C. 616 ∀z:C. 617 match term 618 return λx.x = term → ? with 619 [ mk_Prod x y ⇒ λEq. F x y Eq ] (refl ? term) = z → 620 ∃xa,xb,H. term = 〈xa, xb〉 ∧ 621 F xa xb H = z. 622 #A #B #C * #xa #xb #F #z normalize nodelta #H %{xa} %{xb} %{(refl ??)} @conj try @conj 623 // qed. 624 625 626 lemma translate_expr_sigma_welltyped : ∀vars, cl_expr, cm_expr. 627 translate_expr_sigma vars cl_expr = OK ? cm_expr → 628 dpi1 ?? (pi1 ?? cm_expr) = typ_of_type (typeof cl_expr). 629 #vars #cl_expr * * #typ #cm_expr normalize nodelta #Hexpr_vars 630 whd in ⊢ ((??%?) → ?); #H 631 cases (bind_inversion ????? H) H * #cm_expr' #Hexpr_vars' * 632 #Htranslate_expr 633 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl 634 qed. 635 636 lemma translate_exprlist_sigma_welltyped : 637 ∀vars, cl_exprs, cm_exprs. 638 mmap_sigma ??? (translate_expr_sigma vars) cl_exprs = OK ? cm_exprs → 639 All2 ?? (λcl, cm. dpi1 ?? cm = typ_of_type (typeof cl)) cl_exprs (pi1 ?? cm_exprs). 640 #vars #cl_exprs 641 elim cl_exprs 642 [ * #cm_exprs #Hall whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) @I 643  #hd #tl #Hind * #cm_exprs #Hall #H 644 cases (bind_inversion ????? H) H 645 * * #cm_typ #cm_expr normalize nodelta 646 #Hexpr_vars_cm * #Htranslate_hd 647 lapply (translate_expr_sigma_welltyped … Htranslate_hd) 648 #Heq_cm_typ #H 649 cases (bind_inversion ????? H) H 650 #cm_tail lapply (Hind cm_tail) cases cm_tail 651 #cm_tail_expr #Hall_tail Hind #Hind * #Heq_cm_tail normalize nodelta 652 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj 653 [ @Heq_cm_typ 654  @Hind assumption ] 655 ] qed. 656 657 lemma translate_dest_MemDest_simulation : 658 ∀f. 659 ∀cl_ge : genv_t clight_fundef. 660 ∀cm_ge : genv_t (fundef internal_function). 661 ∀INV : clight_cminor_inv cl_ge cm_ge. 662 ∀frame_data : clight_cminor_data f cl_ge cm_ge INV. 663 ∀cl_expr. ∀cm_expr. 664 ∀cl_block, cl_offset, trace. 665 ∀Hyp_present. 666 translate_dest (alloc_type … frame_data) cl_expr = OK ? (MemDest ? cm_expr) → 667 exec_lvalue cl_ge (cl_env … frame_data) (cl_m … frame_data) cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 → 668 ∃cm_val. eval_expr cm_ge ASTptr cm_expr (cm_env … frame_data) Hyp_present (stackptr … frame_data) (cm_m … frame_data) = OK ? 〈trace, cm_val〉 ∧ 669 value_eq (Em … frame_data) (Vptr (mk_pointer cl_block cl_offset)) cm_val. 670 #f #cl_ge #cm_ge #INV #frame_data #cl_expr * #cm_expr #Hexpr_vars #cl_block #cl_offset #trace #Hyp_present 671 whd in match (translate_dest ??); cases cl_expr #cl_desc #cl_typ normalize nodelta 672 cases cl_desc normalize nodelta 673 [ #sz #i  #id  #e1  #e1  #op #e1 #op #e1 #e2  #cast_ty #e1 674  #cond #iftrue #iffalse  #e1 #e2  #e1 #e2  #sizeofty  #e1 #field  #cost #e1 ] 675 #Htranslate 676 [ 2: 677  *: cases (bind_inversion ????? Htranslate) Htranslate * #cm_expr' #Hexpr_vars' * 678 #Htranslate_addr 679 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) #Hexec_lvalue 680 cases (eval_expr_sim cl_ge cm_ge INV ? frame_data) #_ #Hsim 681 @(Hsim ??? Hexpr_vars … Htranslate_addr ??? ? Hexec_lvalue) ] 682 cases (bind2_eq_inversion ?????? Htranslate) Htranslate * 683 [ #r  #n  ] 684 * #cl_type * #Heq_lookup normalize nodelta 685 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 686 whd in ⊢ ((??%?) → ?); 687 @(match lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id 688 return λx. (lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id = x) → ? 689 with 690 [ None ⇒ ? 691  Some loc ⇒ ? 692 ] (refl ? (lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id ))) normalize nodelta 693 #Hlookup_eq 694 [ 2,4: #Heq destruct (Heq) whd in match (eval_expr ???????); 695 [ 2: %{(Vptr (mk_pointer (stackptr f cl_ge cm_ge INV frame_data) 696 (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 n))))} 697 @conj try @refl 698 lapply (matching … frame_data id) 699 >Hlookup_eq normalize nodelta 700 >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta 701 #Hembed %4 whd in ⊢ (??%?); >Hembed @refl 702  1: whd in match (eval_constant ????); 703 lapply (matching … frame_data id) 704 >Hlookup_eq normalize nodelta 705 >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta 706 @False_ind 707 ] 708  1,3: #Hfind_symbol 709 cases (bind_inversion ????? Hfind_symbol) Hfind_symbol #block * 710 whd in ⊢ ((??%%) → ?); #Hfind_symbol 711 lapply (opt_to_res_inversion ???? Hfind_symbol) #Hfind_symbol_eq 712 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 713 whd in match (eval_expr ???????); 714 whd in match (eval_constant ????); 715 lapply (matching … frame_data id) 716 [ >Hlookup_eq normalize nodelta >Hfind_symbol_eq normalize nodelta 717 #Hembed 718 <(eq_sym … INV id) >Hfind_symbol_eq normalize nodelta 719 %{(Vptr 720 (mk_pointer cl_block 721 (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))} 722 @conj try @refl 723 %4 whd in ⊢ (??%?); >Hembed try @refl 724  (* A stack variable is not in the local environment but in the global one. *) 725 (* we have a contradiction somewhere in the context *) 726 (* TODO *) 727 @cthulhu 728 ] 729 ] qed. 730 731 (* lift simulation result to eval_exprlist *) 732 lemma eval_exprlist_simulation : 733 ∀f. 734 ∀cl_ge : genv_t clight_fundef. 735 ∀cm_ge : genv_t (fundef internal_function). 736 ∀INV : clight_cminor_inv cl_ge cm_ge. 737 ∀frame_data : clight_cminor_data f cl_ge cm_ge INV. 738 ∀cl_exprs,cm_exprs. 739 ∀cl_results,trace. 740 exec_exprlist cl_ge (cl_env … frame_data) (cl_m … frame_data) cl_exprs = OK ? 〈cl_results, trace〉 → 741 mmap_sigma ??? (translate_expr_sigma (alloc_type … frame_data)) cl_exprs = OK ? cm_exprs → 742 ∀H:All ? (λx:𝚺t:typ.expr t. 743 match x with 744 [ mk_DPair ty e ⇒ 745 (expr_vars ty e 746 (λid:ident.λty:typ.present SymbolTag val (cm_env … frame_data) id)) ]) cm_exprs. 747 ∃cm_results. 748 trace_map_inv … (λe. match e return λe. 749 match e with 750 [ mk_DPair _ _ ⇒ ? ] → ? 751 with 752 [ mk_DPair ty e ⇒ λp. eval_expr cm_ge ? e (cm_env … frame_data) p (stackptr … frame_data) (cm_m … frame_data) ]) cm_exprs H = OK ? 〈trace, cm_results〉 ∧ 753 All2 ?? (λcl_val, cm_val. value_eq (Em … frame_data) cl_val cm_val) cl_results cm_results. 754 #f #cl_ge #cm_ge #INV #frame_data #cl_exprs 755 elim cl_exprs 756 [ #cm_exprs #cl_results #trace 757 whd in ⊢ ((??%?) → ?); 758 #Heq destruct (Heq) 759 whd in ⊢ ((??%?) → ?); 760 #Heq destruct (Heq) #H %{[]} 761 @conj try @refl try @I 762  #cl_hd #cl_tl #Hind #cm_exprs #cl_results #trace 763 #Heq cases (bind_inversion ????? Heq) Heq 764 * #hd_val #hd_trace * #Hexec_expr_cl 765 #Heq cases (bind_inversion ????? Heq) Heq 766 * #cl_tl_vals #cl_tl_trace * #Hexec_expr_tl 767 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 768 #Htranslate 769 lapply (translate_exprlist_sigma_welltyped … Htranslate) 770 #Htype_eq_all #Hall 771 cases (bind_inversion ????? Htranslate) Htranslate 772 * * #cmtype #cmexpr normalize nodelta 773 #Hexpr_vars_local_cm * #Htranslate_expr_sigma #Htranslate 774 cases (bind_inversion ????? Htranslate) Htranslate 775 * #cm_tail #Hexpr_vars_local_cm_tail * #Htranslate_tail 776 normalize nodelta 777 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 778 cases Htype_eq_all Htype_eq_all #Hcm_type_eq #Htype_eq_all 779 lapply (Hind cm_tail cl_tl_vals cl_tl_trace Hexec_expr_tl) 780 [ assumption ] Hind #Hind 781 lapply (Hind Htranslate_tail (proj2 ?? Hall)) Hind 782 * #cm_results_tl * #Hcm_exec_tl #Hvalues_eq_tl 783 cases (eval_expr_sim cl_ge cm_ge INV ? frame_data) #Hsim #_ 784 cases (bind_inversion ????? Htranslate_expr_sigma) 785 * #cmexpr' #Hexpr_vars_local_cm' * #Htranslate 786 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 787 lapply (Hsim cl_hd cmexpr ??????) Hsim try assumption 788 [ @(proj1 ?? Hall) ] 789 * #cm_val_hd * #Heval_expr_cm #Hvalue_eq 790 %{(cm_val_hd :: cm_results_tl)} @conj 791 [ 2: @conj try assumption 792  1: whd in ⊢ (??%?); normalize nodelta >Heval_expr_cm 793 normalize nodelta >Hcm_exec_tl @refl 794 ] 795 ] qed. 415 796 416 797 (* Conjectured simulation results … … 428 809 *) 429 810 430 definition clight_normal : Clight_state → bool ≝431 λs. match Clight_classify s with [ cl_other ⇒ true  cl_jump ⇒ true  _ ⇒ false ].432 433 definition cminor_normal : Cminor_state → bool ≝434 λs. match Cminor_classify s with [ cl_other ⇒ true  cl_jump ⇒ true  _ ⇒ false ].435 436 437 811 lemma clight_cminor_normal : 438 ∀INV:clight_cminor_inv. 439 ∀s1,s1',s2,tr. 440 clight_cminor_rel INV s1 s1' → 441 clight_normal s1 = true → 442 ¬ Clight_labelled s1 → 443 ∃n. after_n_steps (S n) … clight_exec (ge_cl INV) s1 (λs.clight_normal s ∧ ¬ Clight_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → 444 ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'. 445 tr = tr' ∧ 446 clight_cminor_rel INV s2 s2' 447 ). 448 #INV #s1 #s1' #s2 #tr #Hstate_rel #Hclight_normal #Hnot_labeleld 812 ∀g1,g2. 813 ∀INV:clight_cminor_inv g1 g2. 814 ∀s1,s1'. 815 clight_cminor_rel g1 g2 INV s1 s1' → 816 clight_normal s1 → 817 ¬ pcs_labelled cl_pre g1 s1 → 818 ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr,s2〉 → 819 ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'. 820 tr = tr' ∧ 821 clight_cminor_rel g1 g2 INV s2 s2' ∧ 822 (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1)) 823 ). 824 #g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_normal #Hnot_labeleld 449 825 inversion Hstate_rel 450 # INV' #cl_s826 #cl_ge #cm_ge #INV' #cl_s 451 827 (* case analysis on Clight statement *) 452 828 cases cl_s … … 454 830  7: #cond #body  8: #init #cond #step #body  9,10:  11: #retval  12: #cond #switchcases  13: #lab #body 455 831  14: #lab  15: #cost #body ] 832 [ 3: (* Call *) 833 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel 834 (* introduce everything *) 835 #fInv #sInv #kInv 836 #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 837 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 838 #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved 839 #Hreturn_ok #Hlabel_wf 840 (* generalize away ugly proof *) 841 generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly 842 #Htranslate 843 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 844 destruct (HA HB) 845 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 846 destruct (HC HD HE) #_ 847 (* back to unfolding Clight execution *) 848 cases (bind_inversion ????? Htranslate) Htranslate * 849 #ef #Hexpr_vars_ef * #Htranslate_ef normalize nodelta #Htranslate 850 cases (bind_inversion ????? Htranslate) Htranslate * 851 #ef' #Hexpr_vars_local_ef' * #Htyp_should_eq_ef 852 cases (typ_should_eq_inversion (typ_of_type (typeof func)) ASTptr … Htyp_should_eq_ef) 853 Htyp_should_eq_ef #Htyp_equality_ef 854 #Heq_ef_ef' #Htranslate 855 cases (bind_inversion ????? Htranslate) Htranslate * 856 #args #Hall_variables_from_args_local * 857 whd in ⊢ ((???%) → ?); #Hargs_spec 858 cases retv normalize nodelta 859 [ 2: (* return something *) 860 #lhs #Hdest 861 cases (bind_inversion ????? Hdest) Hdest #dest * 862 inversion dest normalize nodelta 863 [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest 864 #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 865 (* make explicit the nature of lhs, allowing to prove that no trace is emitted *) 866 lapply (translate_dest_id_inversion … Htranslate_dest) #Hlhs_eq 867  * #cm_expr #Hexpr_vars_cm #Hdest #Htranslate_dest #Hgensym 868 lapply (breakup_dependent_match_on_pairs ?????? Hgensym) Hgensym 869 * #ret_var * #new_gensym * #Heq_alloc_tmp * #Halloc_tmp #Hgensym 870 lapply (breakup_dependent_match_on_pairs ?????? Hgensym) Hgensym 871 * #tmp_var * #new_gensym' * #Heq_alloc_tmp' * #Halloc_tmp' 872 generalize in ⊢ ((??(?? (????%) )?) → ?); #Hstmt_inv_after_gensym 873 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 874 ] 875  1: (* return void *) 876 generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2 877 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] 878 #s2 #tr #Htranslate 879 cases (bindIO_inversion ??????? Htranslate) Htranslate * 880 #func_ptr_val #func_trace * #Hexec_func_ptr normalize nodelta 881 whd in ⊢ ((???%) → ?); #Htranslate 882 cases (bindIO_inversion ??????? Htranslate) Htranslate * 883 #args_values #args_trace * #Hexec_arglist #Htranslate 884 cases (bindIO_inversion ??????? Htranslate) Htranslate 885 #cl_fundef * #Hfind_funct 886 lapply (opt_to_io_Value ?????? Hfind_funct) Hfind_funct #Hfind_funct 887 cases (find_funct_inversion ???? Hfind_funct) 888 #func_ptr * * * #Hfunc_ptr_eq destruct (Hfunc_ptr_eq) 889 #Hpoff_eq_zero #Hregion_is_code 890 * #block_id * #Hblock_id_neg #Hlookup 891 #Htranslate 892 cases (bindIO_inversion ??????? Htranslate) Htranslate #Htype_of_fundef * 893 #Hassert_type_eq 894 [ 1,2: #Htranslate 895 cases (bindIO_inversion ??????? Htranslate) Htranslate * * 896 #lblock #loffset #ltrace * 897 #Hexec_lvalue 898 [ 1: (* empty trace *) @cthulhu (* TODO wip *) 899  2: @cthulhu (* TODO wip *) 900 ] 901  3: @cthulhu ] 902 (* TODO wip *) 903 (* 904 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 905 [ 1: >Hlhs_eq in Hexec_lvalue; #Hexec_lvalue %{1} 906  2: (* Execute Cminor part: evaluate lhs, evaluate assign *) 907 %{2} whd whd in ⊢ (??%?); normalize nodelta 908 whd in match (eval_expr ???????); 909 whd in match (m_bind ?????); 910 lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr) 911 Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func 912 913  3: 914 ] 915 (* execute Cminor part *) 916 [ %{1}  %{2}  %{1} ] 917 whd whd in ⊢ (??%?); normalize nodelta 918 [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???)); 919  2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???)); 920  3: generalize in match (proj2 True ??); ] 921 #Hexpr_vars_present_ef' 922 cases (eval_expr_sim … frame_data) #Hsim_expr #_ 923 cut (expr_vars (typ_of_type (typeof func)) ef 924 (λid:ident.λty:typ.present SymbolTag val (cm_env cl_f cl_ge cm_ge INV' frame_data) id)) 925 [ 1,3,5: lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply ef >Htyp_equality_ef 926 #ef #Hexpr_vars_ef @(jmeq_absorb ?????) #Heq destruct (Heq) 927 @Hexpr_vars_present_ef' ] 928 #Hexpr_vars_present_ef 929 (* use simulation lemma on expressions for function *) 930 lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr) 931 Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func 932 cut (eval_expr cm_ge ASTptr ef' 933 (cm_env cl_f cl_ge cm_ge INV' frame_data) Hexpr_vars_present_ef' 934 (stackptr cl_f cl_ge cm_ge INV' frame_data) 935 (cm_m cl_f cl_ge cm_ge INV' frame_data) 936 =OK (trace×val) 〈func_trace,cm_func_ptr_val〉) 937 [ 1,3,5: 938 lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef' 939 lapply Hexpr_vars_present_ef lapply ef lapply Hexpr_vars_present_ef' lapply ef' 940 <Htyp_equality_ef #ef' #HA #ef #HB #HC #HD #HE 941 @(jmeq_absorb ?????) #Heq destruct (Heq) @HE ] 942 Heval_func #Heval_func >Heval_func 943 whd in match (m_bind ?????); 944 lapply (trans_fn … INV' … Hfind_funct) 945 * #tmp_u * #cminor_fundef * #Hglobals_fresh_for_tmp_u * #Hfundef_fresh_for_tmp_u * 946 #Htranslate_fundef #Hfind_funct_cm 947 lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr 948 whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero; 949 #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero) 950 whd in ⊢ ((??%?) → ?); >(Em_fn_id … frame_data … cm_block Hregion_is_code) 951 normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off' 952 #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq) >addition_n_0 953 >Hfind_funct_cm 954 whd in match (opt_to_res ???); normalize nodelta 955 cut (All (𝚺t:typ.CMexpr t) 956 (λx:𝚺t:typ.expr t.( 957 match x with 958 [ mk_DPair ty e ⇒ 959 expr_vars ty e 960 (λid:ident 961 .λty0:typ.present SymbolTag val (cm_env cl_f cl_ge cm_ge INV' frame_data) id)])) args) 962 [ 1: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall 963  3: cases sInv * * * * * * * normalize nodelta * #_ #_ #Hall #_ #_ #_ @Hall 964  5: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ] 965 #Hall 966 cases (eval_exprlist_simulation … frame_data ???? Hexec_arglist Hargs_spec Hall) 967 #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list 968 whd in match (m_bind ?????); normalize nodelta whd (* TODO here bug in toCminor to be fixed before going on *) @conj 969 [ 2,4,6: #Habsurd destruct (Habsurd) ] 970 @conj try @refl 971 generalize in match (proj1 True (expr_vars ???) (proj1 ???)); 972 * @(CMR_call … tmp_u) try assumption normalize nodelta 973 (* a dependency somewhere prevents case analysis *) 974 lapply Hfind_funct lapply Hfind_funct_cm lapply Htranslate_fundef lapply Hfundef_fresh_for_tmp_u 975 cases cl_fundef 976 [ 2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 @I 977  1: #H9 #H10 #H11 #H12 #H13 @conj try @conj try // ] 978  (* return something *) 979 #lhs #Hdest 980 cases (bind_inversion ????? Hdest) Hdest #dest * 981 inversion dest normalize nodelta 982 [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest 983 #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 984 generalize in match (conj ???); 985 ] 986 987 988 whd in match (proj1 ???); whd in match (proj2 ???); 989 990 991 [ 2: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ] 992 993 >Hfind_funct_cm 994 (* case split away the invariants *) 995 cases sInv * * normalize nodelta * * #Hexpr_vars_ef' #Hall_args_present 996 whd in ⊢ (% → ?); * * normalize nodelta * #Heval_expr #Hvalue_eq 997 >Heval_expr 998 * 999 456 1000 [ 1: (* Skip *) 457 1001 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel … … 460 1004 [ (* Kstop continuation *) 461 1005 (* simplifying the goal using outcome of the inversion *) 462 #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #Heq_INV 463 #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k #_ 464 (* get rid of jmeqs and destruct *) 465 lapply (jmeq_to_eq ??? Heq_INV) Heq_INV #Heq_INV 466 lapply (jmeq_to_eq ??? Heq_cl_f) Heq_cl_f #Heq_cl_f 467 destruct (Heq_INV Heq_cl_f) 468 lapply (jmeq_to_eq ??? Heq_frame) Heq_frame #Heq_frame 469 lapply (jmeq_to_eq ??? Heq_cm_f) Heq_cm_f #Heq_cm_f 470 lapply (jmeq_to_eq ??? Heq_rettyp) Heq_rettyp #Heq_rettypv 471 lapply (jmeq_to_eq ??? Heq_cm_k) Heq_cm_k #Heq_cm_k 472 lapply (jmeq_to_eq ??? Heq_cl_k) Heq_cl_k #Heq_cl_k 473 destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp) 1006 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #kframe_data #ktarget_type 1007 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1008 destruct (HA HB) 1009 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 1010 destruct (HC HD HE) 1011 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI 1012 destruct (HF HG HH HI) #_ 474 1013 (* introduce everything *) 475 1014 #fInv #sInv #kInv … … 483 1022 (* In this simple case, trivial translation *) 484 1023 destruct (Heq_translate) 485 #Heq_INV' #Heq_s1 #Heq_s1' 486 lapply (jmeq_to_eq ??? Heq_INV') Heq_INV' #Heq_INV' 487 lapply (jmeq_to_eq ??? Heq_s1) Heq_s1 #Heq_s1 488 lapply (jmeq_to_eq ??? Heq_s1') Heq_s1' #Heq_s1' 489 destruct (Heq_INV' Heq_s1 Heq_s1') #_ 1024 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1025 destruct (HA HB) 1026 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 1027 destruct (HC HD HE) #_ 490 1028 (* unfold the clight execution *) 491 %{0} 492 whd in ⊢ (% → ?); whd in match (step io_out io_in clight_exec ??); 1029 #s2 #tr whd in ⊢ ((??%?) → ?); 493 1030 inversion (fn_return kcl_f) normalize nodelta 1031 normalize nodelta 494 1032 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 495 1033  #structname #fieldspec  #unionname #fieldspec  #id ] 496 #Hfn_return 497 whd in ⊢ (% → ?); 498 @False_ind 1034 #Hfn_return whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 1035 %{1} whd @conj try @conj try @refl 1036 [ 2: #Habsurd destruct (Habsurd) ] 1037 %2{kcl_f} 1038 [ %{ (alloc_type … kframe_data) 1039 (stacksize … kframe_data) 1040 (alloc_hyp … kframe_data) 1041 (cl_env … kframe_data) 1042 (cm_env … kframe_data) 1043 (cl_env_hyp … kframe_data) 1044 (free_list (cl_m … kframe_data) (blocks_of_env (cl_env … kframe_data))) 1045 (free (cm_m … kframe_data) (stackptr … kframe_data)) 1046 (Em … kframe_data) 1047 ? (* injection *) 1048 (stackptr … kframe_data) 1049 ? (* matching *)} 1050 [ @(freelist_memory_inj_m1_m2 … (injection … kframe_data) (blocks_of_env (cl_env … kframe_data)) (stackptr … kframe_data)) 1051 [ 2,3: @refl 1052  1053 1054 @cthulhu 499 1055  (* KSeq continuation *) 500 # kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k'1056 #gcl_ge #kcm_ge #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k' 501 1057 #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag 502 1058 * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved 503 1059 #kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_ 1060 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1061 destruct (HA HB) 1062 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 1063 destruct (HC HD HE) 1064 @(jmeq_absorb ?????) #HF 1065 504 1066 #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k #_ 505 1067 (* get rid of jmeqs and destruct *) … … 687 1249  3: (* Local *) @cthulhu 688 1250 ] 689  *: (* memdest *) @cthulhu ] 1251  *: (* memdest *) @cthulhu ] *) 690 1252  *: @cthulhu 691 1253 ] qed. 692 1254 1255 (* TODO: adapt the following to the new goal shape. *) 693 1256 axiom clight_cminor_call_return : 694 1257 ∀INV:clight_cminor_inv.
Note: See TracChangeset
for help on using the changeset viewer.