Changeset 3036
 Timestamp:
 Mar 29, 2013, 5:12:09 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r2857 r3036 246 246 match u2 with 247 247 [ mk_universe p2 ⇒ p2 ≤ p1 ] ]. 248 248 249 249 definition fte ≝ fresher_than_or_equal. 250 250 … … 256 256 * // qed. 257 257 258 definition labgen_include ≝ 259 λgen1, gen2 : labgen. 260 ∃labels. label_genlist gen2 = labels @ label_genlist gen1. 261 262 definition tmpgen_include ≝ 263 λvartypes. 264 λgen1, gen2 : tmpgen vartypes. 265 ∃idents. tmp_env ? gen2 = idents @ (tmp_env ? gen1). 258 (* Express that the [first] tmpgen generates "newer" ids than an other one. *) 259 definition tmpgen_fresher_than ≝ 260 λvars. λgen1, gen2 : tmpgen vars. 261 fresher_than_or_equal (tmp_universe … gen1) (tmp_universe … gen2). 262 263 (* Map a predicate on all the /keys/ of an environment, i.e. on a set 264 * of identifiers. *) 265 definition env_domain_P : cl_env → ∀P:(ident → Prop). Prop ≝ 266 λe, P. 267 match e with 268 [ an_id_map m ⇒ 269 fold ?? (λkey,elt,acc. P (an_identifier ? key) ∧ acc) m True 270 ]. 271 272 (* Property for an identifier to be out of the set 273 * of identifiers represented by an universe. *) 274 definition ident_below_universe ≝ 275 λi: ident. 276 λu: universe SymbolTag. 277 match i with 278 [ an_identifier id ⇒ 279 match u with 280 [ mk_universe id_u ⇒ 281 id < id_u 282 ] 283 ]. 284 285 (* Property of the domain of an environment to be disjoint of the set 286 * of identifiers represented by an universe. *) 287 definition env_below_freshgen : env → ∀vars. tmpgen vars → Prop ≝ 288 λe, vars, tmpgen. 289 env_domain_P e (λid. ident_below_universe id (tmp_universe … tmpgen)). 290 291 (* The property of interest for the proof. Identifiers generated from an 292 * universe above the environment are not in the said environment. *) 293 lemma lookup_fails_outside_of_env : 294 ∀env, vars, ty, gen, id, gen'. 295 alloc_tmp vars ty gen = 〈id, gen'〉 → 296 env_below_freshgen env vars gen → 297 lookup ?? env id = None ?. 298 @cthulhu 299 qed. 300 301 (* The property of being above an environment is conserved by fresh ident 302 * generation *) 303 lemma alloc_tmp_env_invariant : 304 ∀env, vars, ty, gen, id, gen'. 305 alloc_tmp vars ty gen = 〈id, gen'〉 → 306 env_below_freshgen env vars gen → 307 env_below_freshgen env vars gen'. 308 @cthulhu 309 qed. 266 310 267 311 (*  *) … … 274 318 (* Temporary variables generated during conversion are wellallocated. *) 275 319 definition tmp_vars_well_allocated ≝ 276 λvartypes. 277 λtmp_gen: tmpgen vartypes. 320 λtmpenv: list (ident × type). 278 321 λcm_env. 279 322 λcm_m. … … 282 325 ∀local_variable. 283 326 ∀H:present ?? cm_env local_variable. 284 ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) (tmp_env … tmp_gen)→327 ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) tmpenv → 285 328 ∀v. val_typ v (typ_of_type ty) → 286 329 ∃cm_m'. storev (typ_of_type ty) cm_m (lookup_present ?? cm_env local_variable H) v = Some ? cm_m' ∧ … … 394 437 (*  *) 395 438 396 record frame_data397 (f : function)398 (ge_cl : genv_t clight_fundef)399 (ge_cm : genv_t (fundef internal_function))400 (INV : clight_cminor_inv ge_cl ge_cm) : Type[0] ≝401 {402 }.403 404 439 definition CMcast : ∀t,t'. CMexpr t → t = t' → CMexpr t'. 405 440 #t #t' #e #H destruct (H) @e … … 415 450 ∀cl_f: function. (* current Clight function *) 416 451 internal_function → (* current Cminor function *) 417 cl_env → 418 cm_env → 419 var_types → 420 (*frame_data cl_f cl_ge cm_ge INV →*) (* data for the current stack frame in CL and CM *) 421 option typ → (* optional target type  uniform over a given function *) 452 cl_env → (* Clight local environment *) 453 cm_env → (* Cminor local environment *) 454 mem → (* Cminor memory state *) 455 ∀alloc_type:var_types. (* map vars to alloc type *) 456 ∀tmpenv:list (ident×type). (* list of generated variables *) 457 (*tmpgen alloc_type → (* input freshgen *) 458 tmpgen alloc_type → (* output freshgen *) *) (* bad idea *) 459 option typ → (* optional target type  arg. uniform over a given function *) 422 460 cl_cont → (* CL cont *) 423 461 cm_cont → (* CM cont *) 424 stack → (* CM stack *) 462 stack → (* CM stack *) 425 463 Prop ≝ 426 (* Stop continuation *)464 (* Stop continuation *) 427 465  ClCm_cont_stop: 428 466 ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type. 429 ∀cl_env, cm_env, alloc_type.467 ∀cl_env, cm_env, cm_m, alloc_type, tmpenv. (*, stmt_univ, stmt_univ'.*) 430 468 ∀cm_stack. 431 469 cm_stack = SStop → 432 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_typetarget_type Kstop Kend cm_stack470 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type Kstop Kend cm_stack 433 471 434 472 (* Seq continuation *) … … 437 475 ∀stack. 438 476 ∀alloc_type. 477 ∀tmpenv. 439 478 ∀cl_s: statement. 440 479 ∀cm_s: stmt. 441 480 ∀cl_env: cl_env. 442 481 ∀cm_env: cm_env. 482 ∀cm_m: mem. 443 483 ∀cl_k': cl_cont. 444 484 ∀cm_k': cm_cont. … … 451 491 (*  invariant on label existence  *) 452 492 lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) → 453 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' stack → 454 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') stack 493 (*  invariant on fresh variables  *) 494 lset_inclusion ? (tmp_env alloc_type stmt_univ') tmpenv → 495 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) target_type cl_k' cm_k' stack → 496 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') stack 455 497 456 498 (* While continuation *) … … 460 502 ∀stack. 461 503 ∀alloc_type. 504 ∀tmpenv. 462 505 ∀cl_env. 463 506 ∀cm_env. 464 507 ∀cm_m. 465 508 (* subcontinuations *) 466 509 ∀cl_k': cl_cont. 467 510 ∀cm_k': cm_cont. 468 469 511 (* elements of the source while statement *) 470 512 ∀sz,sg. … … 473 515 ∀cl_body. 474 516 ∀Heq: ASTint sz sg = typ_of_type cl_ty. 475 476 517 (* elements of the converted while statement *) 477 518 ∀cm_cond: CMexpr (ASTint sz sg). 478 519 ∀cm_body. 479 ∀entry,exit: identifier Label. 480 520 ∀entry,exit: identifier Label. 481 521 (* universes used to generate fresh labels and variables *) 482 522 ∀stmt_univ, stmt_univ'. … … 484 524 ∀lbls: lenv. 485 525 ∀Htranslate_inv. 486 487 526 (* relate CL and CM expressions *) 488 ∀Hexpr_vars. 489 translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? («CMcast ?? cm_cond Heq, Hexpr_vars») → 490 527 ∀Hexpr_vars:expr_vars ? cm_cond (local_id alloc_type). 528 translate_expr alloc_type (Expr cl_cond_desc cl_ty) ≃ OK ? («cm_cond, Hexpr_vars») → 491 529 (* Parameters and results to find_label_always *) 492 530 ∀sInv: stmt_inv cm_f cm_env (f_body cm_f). 493 531 ∀Hlabel_declared: Exists (identifier Label) (λl'.l'=entry) (labels_of (f_body cm_f)). 494 532 ∀Hinv. 495 496 533 (* Specify how the labels for the whilereplacing gotos are produced *) 497 534 mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 → 498 535 translate_statement alloc_type stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» → 499 (* Invariant on label existence *) 500 lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) → 536 (*  Invariant on label existence  *) 537 lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) → 538 (*  invariant on fresh variables  *) 539 lset_inclusion ? (tmp_env alloc_type stmt_univ') tmpenv → 501 540 find_label_always entry (f_body cm_f) Kend Hlabel_declared cm_f cm_env sInv I = 502 541 «〈(*St_label entry*) … … 504 543 (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip) 505 544 (St_label exit St_skip)), cm_k'〉, Hinv» → 506 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' stack → 507 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type ( 508 Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k') 509 (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')) stack. 510 (* TODO: Kcall *) 511 512 (* TODO XXX *) 513 (* relation between placeholders for return values *) 514 515 definition return_value_rel : 516 ∀cl_f, cl_ge, cm_ge. 517 ∀INV: clight_cminor_inv cl_ge cm_ge. 518 frame_data cl_f ?? INV → 519 option (block×offset×type) → option (ident×typ) → Prop ≝ 520 λcl_f, cl_ge, cm_ge, INV, data, opt1, opt2. 521 match opt1 with 522 [ None ⇒ 523 match opt2 with 524 [ None ⇒ True 525  _ ⇒ False ] 526  Some ptr ⇒ 527 match opt2 with 528 [ Some id ⇒ True (* TODO, here. *) 529  None ⇒ False 530 ] 531 ]. 545 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type cl_k' cm_k' stack → 546 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type 547 (Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k') 548 (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')) stack 549 550  ClCm_cont_call_store: 551 ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type. 552 ∀stack. 553 ∀alloc_type. 554 ∀tmp_env. 555 ∀cl_env. 556 ∀cm_env. 557 ∀cm_m. 558 (* subcontinuations *) 559 ∀cl_k': cl_cont. 560 ∀cm_k': cm_cont. 561 (* CL return addr *) 562 ∀CL_lvalue_block,CL_lvalue_offset,lhs_ty. 563 ∀CM_lvalue_ptr. 564 (* CM stack content *) 565 ∀stackptr. 566 ∀fInv. 567 ∀tmp_var, ret_var. 568 ∀Htmp_var_present. 569 ∀Hret_present. 570 ∀Hstmt_inv. 571 (* TODO: loads of invariants *) 572 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmp_env (*stmt_univ stmt_univ*) target_type 573 (Kcall (Some ? 〈CL_lvalue_block, CL_lvalue_offset, lhs_ty〉) cl_f cl_env cl_k') 574 cm_k' 575 (Scall (Some ? 〈ret_var,typ_of_type lhs_ty〉) cm_f stackptr 576 (update_present SymbolTag val cm_env tmp_var Htmp_var_present (Vptr CM_lvalue_ptr)) Hret_present 577 (stmt_inv_update cm_f cm_env (f_body cm_f) tmp_var (Vptr CM_lvalue_ptr) fInv Htmp_var_present) 578 (Kseq 579 (St_store (typ_of_type lhs_ty) (Id ASTptr tmp_var) 580 (Id (typ_of_type lhs_ty) ret_var)) cm_k') Hstmt_inv stack) 581 582  ClCm_cont_call_nostore: 583 ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type. 584 ∀stack. 585 ∀alloc_type. 586 ∀tmpenv. 587 ∀cl_env. 588 ∀cm_env. 589 ∀cm_m. 590 (* subcontinuations *) 591 ∀cl_k': cl_cont. 592 ∀cm_k': cm_cont. 593 (* CM stack content *) 594 ∀cl_lhs, cm_lhs. 595 match cl_lhs with 596 [ None ⇒ match cm_lhs with [ None ⇒ True  _ ⇒ False ] 597  Some cl_location ⇒ 598 match cm_lhs with 599 [ None ⇒ False 600  Some cm_location ⇒ 601 ∃CL_lvalue_block, CL_lvalue_offset, lhs_ty, ret_var. 602 cl_location = 〈CL_lvalue_block,CL_lvalue_offset, lhs_ty〉 ∧ 603 cm_location = 〈ret_var, typ_of_type lhs_ty〉 604 ] 605 ] → 606 ∀Hret_present. 607 ∀Hstmt_inv. 608 ∀stackptr. 609 ∀fInv. 610 (* ∀stmt_univ.*) 611 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) target_type 612 (Kcall cl_lhs cl_f cl_env cl_k') 613 cm_k' 614 (Scall cm_lhs cm_f stackptr cm_env Hret_present fInv cm_k' Hstmt_inv stack). 615 616 lemma translate_fundef_internal : 617 ∀ge1, ge2. 618 ∀INV: clight_cminor_inv ge1 ge2. 619 ∀u, cl_f, cm_fundef. 620 ∀H1, H2. 621 translate_fundef u (globals ?? INV) H1 (CL_Internal cl_f) H2 = OK ? cm_fundef → 622 ∃cm_f. cm_fundef = Internal ? cm_f ∧ 623 translate_function u (globals ge1 ge2 INV) cl_f H1 H2 = OK ? cm_f. 624 #ge1 #ge2 #INV #u #cl_f #cm_fd #H1 #H2 625 whd in ⊢ ((??%?) → ?); cases (translate_function u (globals ge1 ge2 INV) cl_f H1 H2) 626 normalize nodelta 627 [ 2: #er #Habsurd destruct (Habsurd) 628  1: #cm_f #Heq destruct (Heq) %{cm_f} @conj @refl ] 629 qed. 630 631 lemma translate_fundef_external : 632 ∀ge1, ge2. 633 ∀INV: clight_cminor_inv ge1 ge2. 634 ∀u, id, tl, ty. 635 ∀H1, H2. 636 translate_fundef u (globals ?? INV) H1 (CL_External id tl ty) H2 = 637 OK ? (External ? (mk_external_function id (signature_of_type tl ty))). 638 #ge1 #ge2 #INV #u #id #tl #ty #H1 #H2 @refl 639 qed. 532 640 533 641 (* Definition of the simulation relation on states. The orders of the parameters is dictated by 534 642 * the necessity of performing an inversion on the continuation sim relation without having to 535 643 * play the usual game of lapplying all previous dependent arguments. *) 644 536 645 inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge → Clight_state → Cminor_state → Prop ≝ 646 (*  *) 647 (* normal state *) 648 (*  *) 537 649  CMR_normal : 538 650 (* Clight and Cminor global envs *) … … 571 683 ∀kInv: cont_inv cm_f cm_env cm_k. 572 684 (*  relate return type variable to actual return type  *) 573 rettyp = opttyp_of_type (fn_return cl_f) → 685 rettyp = opttyp_of_type (fn_return cl_f) → 574 686 (*  relate Clight and Cminor functions  *) 575 687 ∀func_univ: universe SymbolTag. … … 592 704 lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) → 593 705 (*  relate Clight continuation to Cminor continuation  *) 594 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_st → 706 ∀tmpenv. 707 lset_inclusion ? (tmp_env ? stmt_univ') tmpenv → 708 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st → 595 709 (*  state invariants for memory and environments  *) 596 710 (* Embedding *) 597 711 ∀Em: embedding. 598 712 (* locals are properly allocated *) 599 tmp_vars_well_allocated alloc_type stmt_univ'cm_env cm_m cl_m Em →713 tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em → 600 714 (* specify how alloc_type is built *) 601 715 characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 → … … 611 725 (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 → 612 726 mem block b1 (blocks_of_env cl_env)) → 727 (* The fresh name generator is compatible with the clight environment *) 728 env_below_freshgen cl_env alloc_type stmt_univ → 613 729 clight_cminor_rel cl_ge cm_ge INV 614 730 (ClState cl_f cl_s cl_k cl_env cl_m) 615 731 (CmState cm_f cm_s cm_env fInv sInv cm_m stackptr cm_k kInv cm_st) 616 732 (*  *) 733 (* return state *) 734 (*  *) 617 735  CMR_return : 736 (* Clight and Cminor global envs *) 618 737 ∀cl_ge, cm_ge. 738 (* Relates globals to globals and functions to functions. *) 619 739 ∀INV: clight_cminor_inv cl_ge cm_ge. 620 ∀cl_f: function. (* Clight enclosing function *) 621 ∀cm_f: internal_function. (* enclosing function *) 740 (*  Continuations and functions  *) 741 (* Clight continuation *) 742 ∀cl_k: cl_cont. 743 (* Cminor continuation *) 744 ∀cm_k: cm_cont. 745 (* Cminor stack *) 746 ∀cm_st: stack. 747 (* Clight enclosing function *) 748 ∀cl_f: function. 749 (* Cminor enclosing function *) 750 ∀cm_f: internal_function. 751 (* mapping from variables to their Cminor alloc type *) 622 752 ∀alloc_type. 753 (* Clight env/mem *) 623 754 ∀cl_env, cl_m. 755 (* Cminor env/mem *) 624 756 ∀cm_env, cm_m. 625 ∀cm_st: stack. (* Cminor stack*)757 (* Stack pointer (block containing Cminor locals), related size *) 626 758 ∀stackptr, stacksize. 627 ∀stmt_univ. 759 (* fresh label generator *) 760 ∀stmt_univ: tmpgen alloc_type. 761 ∀tmpenv. 762 lset_inclusion ? (tmp_env ? stmt_univ) tmpenv → 763 (*  state invariants for memory and environments  *) 764 (* Embedding *) 628 765 ∀Em: embedding. 629 tmp_vars_well_allocated alloc_type stmt_univ cm_env cm_m cl_m Em → (* locals are properly allocated *) 630 characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 → (* specify how alloc_type is built *) 631 (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *) 632 memory_inj Em cl_m cm_m → (* memory injection *) 633 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type → (* map CL env to CM env *) 634 (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) → (* Force embedding to compute identity on functions *) 766 (* locals are properly allocated *) 767 tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em → 768 (* specify how alloc_type is built *) 769 characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 → 770 (* spec. Clight env at alloc time *) 771 (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → 772 (* memory injection *) 773 memory_inj Em cl_m cm_m → 774 (* map CL env to CM env *) 775 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type → 776 (* Force embedding to compute identity on functions *) 777 (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) → 635 778 (* Make explicit the fact that locals in CL are mapped to a single CM block *) 636 779 (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 → 637 mem block b1 (blocks_of_env cl_env)) → 780 mem block b1 (blocks_of_env cl_env)) → 781 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) (None ?) cl_k cm_k cm_st → 638 782 clight_cminor_rel cl_ge cm_ge INV 639 (ClReturnstate Vundef Kstopcl_m)783 (ClReturnstate Vundef cl_k cl_m) 640 784 (CmReturnstate (None val) cm_m cm_st) 641 642  CMR_call_nostore : 643 (* call to a function with no return value, or which returns in a local variable in Cminor *) 644 ∀cl_ge, cm_ge, cl_f, cm_f. 645 ∀INV: clight_cminor_inv cl_ge cm_ge. 646 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr. 647 (* TODO: put the actual invariants on memory and etc. here *) 648 ∀u: universe SymbolTag. 649 ∀cl_fundef, cm_fundef. 650 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u. 651 ∀Hfundef_fresh: fd_fresh_for_univ cl_fundef u. 652 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) → 653 ∀cl_k, cm_k. 654 ∀fblock. 655 match cl_fundef with 656 [ CL_Internal cl_function ⇒ 657 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧ 658 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧ 659 translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧ 660 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack 661  CL_External name argtypes rettype ⇒ 662 True 663 ] → 664 ∀cl_fun_id, cm_fun_id. 665 cl_fun_id = cm_fun_id → 666 ∀cl_retval, cm_retval. 667 ∀sInv, fInv, kInv. 668 ∀cl_args_values, cm_args_values. 669 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*) 670 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *) 671 clight_cminor_rel cl_ge cm_ge INV 672 (ClCallstate cl_fun_id 673 cl_fundef cl_args_values (Kcall cl_retval cl_f cl_env cl_k) cl_m) 674 (CmCallstate cm_fun_id cm_fundef 675 cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv cm_k kInv cm_stack)) 676 677  CMR_call_store : 678 (* call to a function which returns to some location in memory in Cminor *) 679 ∀cl_ge, cm_ge, cl_f, cm_f. 680 ∀INV: clight_cminor_inv cl_ge cm_ge. 681 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr. 682 (* TODO: put the actual invariants on memory and etc. here *) 683 ∀u: universe SymbolTag. 684 ∀cl_fundef, cm_fundef. 685 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u. 686 ∀Hfundef_fresh: fd_fresh_for_univ cl_fundef u. 687 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) → 688 ∀cl_k, cm_k. 689 ∀fblock. 690 match cl_fundef with 691 [ CL_Internal cl_function ⇒ 692 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧ 693 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧ 694 translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧ 695 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack 696  CL_External name argtypes rettype ⇒ 697 True 698 ] → 699 ∀cl_fun_id, cm_fun_id. 700 cl_fun_id = cm_fun_id → 701 ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval. 702 ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs. 703 (* Explain where the lhs of the postreturn assign comes from *) 704 exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 → 705 translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») → 706 (* TODO: Explain that the actual variable used to store the ret val is fresh and has the 707 * right type, etc *) 708 ∀cm_ret_var. 709 ∀sInv, fInv, kInv. 710 ∀cl_args_values, cm_args_values. 711 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*) 712 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *) 713 ∀cm_stack. 714 clight_cminor_rel cl_ge cm_ge INV 715 (ClCallstate cl_fun_id 716 cl_fundef cl_args_values (Kcall (Some ? 〈cl_retval,cl_rettyp〉) cl_f cl_env cl_k) cl_m) 717 (CmCallstate cm_fun_id cm_fundef 718 cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv 719 (Kseq (St_store (typ_of_type cl_rettyp) cm_lhs 720 (Id (typ_of_type cl_rettyp) cm_ret_var)) cm_k) 721 kInv cm_stack)) 722 785 (*  *) 786 (* call state *) 787 (*  *) 788  CMR_call : 789 (* Clight and Cminor global envs *) 790 ∀cl_ge, cm_ge. 791 (* Relates globals to globals and functions to functions. *) 792 ∀INV: clight_cminor_inv cl_ge cm_ge. 793 (*  Continuations and functions for the current stack frame  *) 794 (* Clight continuation *) 795 ∀cl_k: cl_cont. 796 (* Cminor continuation *) 797 ∀cm_k: cm_cont. 798 (* Cminor stack *) 799 ∀cm_st: stack. 800 (* Clight enclosing function *) 801 ∀cl_f: function. 802 (* Cminor enclosing function *) 803 ∀cm_f: internal_function. 804 (* Clight called fundef *) 805 ∀cl_fundef. 806 (* Cminor called fundef *) 807 ∀cm_fundef. 808 (* block of Clight and Cminor function *) 809 (* XXX why do I need that already ? *) 810 ∀fblock: block. 811 (* optional return type of the function *) 812 ∀target_type. 813 (* mapping from variables to their Cminor alloc type *) 814 ∀alloc_type. 815 (* Clight env/mem *) 816 ∀cl_env, cl_m. 817 (* Cminor env/mem *) 818 ∀cm_env, cm_m. 819 (* Stack pointer (block containing Cminor locals), stack frame size *) 820 ∀stackptr, stacksize. 821 (* fresh label generator for function *) 822 ∀func_univ: universe SymbolTag. 823 (* relate CL and CM enclosing functions *) 824 ∀Hglobals_fresh, Hfundef_fresh. 825 translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f → 826 (* specify fblock *) 827 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cl_fundef → 828 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef → 829 ∀cl_fun_id, cm_fun_id. 830 ∀stmt_univ: tmpgen alloc_type. 831 ∀tmpenv. 832 lset_inclusion ? (tmp_env ? stmt_univ) tmpenv → 833 match cl_fundef with 834 [ CL_Internal _ ⇒ 835 (* specify continuation *) 836 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv target_type cl_k cm_k cm_st 837 (* ∨ 838 (∃cl_blo, cl_off, cl_ty. (* Clight return loscation + type *) 839 ∃cm_loc_ident, cm_return_ident. (* Cminor locals storing the lvalues *) 840 ∃sInv, fInv, kInv. (* Invariants required by the stack construction *) 841 present ?? cm_env cm_loc_ident ∧ 842 present ?? cm_env cm_return_ident ∧ 843 (clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type target_type 844 (Kcall (Some ? 〈cl_blo, cl_off, cl_ty〉) cl_f cl_env cl_k) 845 cm_k (Scall (Some ? 〈cm_return_ident,typ_of_type cl_ty〉) cm_f stackptr cm_env sInv fInv 846 (Kseq (St_store (typ_of_type cl_ty) (Id ? cm_loc_ident) (Id ? cm_return_ident)) cm_k) 847 kInv cm_st))) *) 848  CL_External cl_id cl_argtypes cl_rettype ⇒ 849 match cm_fundef with 850 [ Internal _ ⇒ False 851  External cm_f_ext ⇒ True ] 852 (* match cm_f_ext with 853 [ mk_external_function cm_id sig ⇒ 854 cl_fun_id = cl_id ∧ cm_fun_id = cm_id ∧ cl_fun_id = cm_fun_id 855 ] *) 856 ] → 857 (*  state invariants for memory and environments  *) 858 (* Embedding *) 859 ∀Em: embedding. 860 (* locals are properly allocated *) 861 tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em → 862 (* specify how alloc_type is built *) 863 characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 → 864 (* spec. Clight env at alloc time *) 865 (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → 866 (* memory injection *) 867 memory_inj Em cl_m cm_m → 868 (* map CL env to CM env *) 869 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type → 870 (* Force embedding to compute identity on functions *) 871 (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) → 872 (* Make explicit the fact that locals in CL are mapped to a single CM block *) 873 (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 → 874 mem block b1 (blocks_of_env cl_env)) → 875 ∀cl_args_values, cm_args_values. 876 All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values → 877 clight_cminor_rel cl_ge cm_ge INV 878 (ClCallstate cl_fun_id cl_fundef cl_args_values cl_k cl_m) 879 (CmCallstate cm_fun_id cm_fundef cm_args_values cm_m cm_st) 880 (*  *) 881 (* special while state *) 882 (*  *) 723 883  CMR_while: 724 884 ∀cl_ge,cm_ge,INV,cl_f,cm_f. … … 750 910 translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f → 751 911 (*  relate continuations  *) 752 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack →753 912 ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbl_univ'',lbls. 913 ∀tmpenv'. 914 lset_inclusion ? (tmp_env ? stmt_univ') tmpenv' → 915 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv' rettyp cl_k cm_k cm_stack → 754 916 (* Invariants *) 755 917 ∀Em: embedding. 756 tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em → (* locals are properly allocated *)918 tmp_vars_well_allocated tmpenv' cm_env cm_m cl_m Em → (* locals are properly allocated *) 757 919 characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 → (* specify how alloc_type is built *) 758 920 (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *) … … 761 923 (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) → (* Force embedding to compute identity on functions *) 762 924 (* Make explicit the fact that locals in CL are mapped to a single CM block *) 763 (∀b1.∀delta. Em b1 =Some ? 〈stackptr,delta〉 →925 (∀b1.∀delta. Em b1 = Some ? 〈stackptr,delta〉 → 764 926 mem block b1 (blocks_of_env cl_env)) → 927 (* The fresh name generator is compatible with the clight environment *) 928 env_below_freshgen cl_env alloc_type stmt_univ → 765 929 (* Expression translation and related hypotheses *) 766 ∀Hcond_tr. (* invariant after converting conditional expr *) 767 translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? «CMcast ?? cm_cond Heq_ty, Hcond_tr » → 930 ∀Hcond_tr:expr_vars ? cm_cond (local_id alloc_type). (* invariant after converting conditional expr *) 931 (* translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? «CMcast ?? cm_cond Heq_ty, Hcond_tr » → *) 932 translate_expr alloc_type (Expr cl_cond_desc cl_ty) ≃ OK ? «cm_cond, Hcond_tr » → 768 933 (* Label consistency *) 769 934 Exists ? (λl':identifier Label.l'=entry_label) (labels_of (f_body cm_f)) → … … 795 960 (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip) 796 961 (St_label exit_label St_skip))) 797 cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)). 962 cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)). 963 964 965 (* 966  CMR_call_nostore : 967 (* call to a function with no return value, or which returns in a local variable in Cminor *) 968 ∀cl_ge, cm_ge. (* cl_f, cm_f.*) 969 ∀INV: clight_cminor_inv cl_ge cm_ge. 970 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr. 971 (* TODO: put the actual invariants on memory and etc. here *) 972 ∀func_univ: universe SymbolTag. 973 ∀cl_f, cm_f. 974 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) func_univ. 975 ∀Hfundef_fresh: fd_fresh_for_univ (CL_Internal cl_f) func_univ. 976 ∀rettyp. 977 ∀cl_k, cm_k. 978 ∀fblock. 979 rettyp = opttyp_of_type (fn_return cl_f) ∧ 980 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_f) → 981 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (Internal ? cm_f) → 982 translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f → 983 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack → 984 ∀fun_id. 985 ∀cl_retval, cm_retval. 986 ∀sInv, fInv, kInv. 987 ∀cl_args_values, cm_args_values. 988 All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values → 989 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*) 990 clight_cminor_rel cl_ge cm_ge INV 991 (ClCallstate fun_id (CL_Internal cl_f) cl_args_values cl_k cl_m) 992 (CmCallstate fun_id (Internal ? cm_f) cm_args_values cm_m cm_stack) 993 994  CMR_call_store : 995 (* call to a function which returns to some location in memory in Cminor *) 996 ∀cl_ge, cm_ge. 997 ∀INV: clight_cminor_inv cl_ge cm_ge. 998 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr. 999 (* TODO: put the actual invariants on memory and etc. here *) 1000 ∀func_univ: universe SymbolTag. 1001 ∀cl_f, cm_f. 1002 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) func_univ. 1003 ∀Hfundef_fresh: fd_fresh_for_univ (CL_Internal cl_f) func_univ. 1004 ∀rettyp. 1005 ∀cl_k, cm_k. 1006 ∀fblock. 1007 rettyp = opttyp_of_type (fn_return cl_f) → 1008 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_f) → 1009 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (Internal ? cm_f) → 1010 translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f → 1011 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack → 1012 ∀fun_id. 1013 ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval. 1014 ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs. 1015 (* Explain where the lhs of the postreturn assign comes from *) 1016 exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 → 1017 translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») → 1018 (* TODO: Explain that the actual variable used to store the ret val is fresh and has the 1019 * right type, etc *) 1020 ∀cm_ret_var. 1021 ∀sInv, fInv, kInv. 1022 ∀cl_args_values, cm_args_values. 1023 All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values → 1024 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*) 1025 ∀cm_stack. 1026 clight_cminor_rel cl_ge cm_ge INV 1027 (ClCallstate fun_id (CL_Internal cl_f) 1028 cl_args_values (Kcall (Some ? 〈cl_retval,cl_rettyp〉) cl_f cl_env cl_k) cl_m) 1029 (CmCallstate fun_id (Internal ? cm_f) 1030 cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv 1031 (Kseq (St_store (typ_of_type cl_rettyp) cm_lhs 1032 (Id (typ_of_type cl_rettyp) cm_ret_var)) cm_k) 1033 kInv cm_stack)) 1034 *) 798 1035 799 1036 definition clight_normal : Clight_state → bool ≝ … … 888 1125 #p #Hlookup %{p} @conj try @refl assumption 889 1126 qed. 1127 1128 lemma find_funct_id_inversion : 1129 ∀F: Type[0]. ∀ge: genv_t F. ∀ptr. ∀f. ∀id. 1130 find_funct_id F ge ptr = Some ? 〈f, id〉 → 1131 ∃H:(find_funct F ge ptr = Some ? f). 1132 id = symbol_of_function_val' F ge ptr f H. 1133 #F #ge #ptr #f #id 1134 whd in match (find_funct_id ???); 1135 generalize in match (refl ??); 1136 generalize in ⊢ 1137 (∀_:(???%). 1138 (??(match % 1139 with 1140 [ _ ⇒ λ_. ? 1141  _ ⇒ λ_.λ_. ? ] ?)?) → ?); 1142 #o cases o 1143 normalize nodelta 1144 [ #H #Habsurd destruct (Habsurd) 1145  #f #Hfind #Heq destruct (Heq) %{Hfind} 1146 cases (find_funct_inversion ???? Hfind) #ptr * 1147 * * #Hptr lapply Hfind Hfind >Hptr #Hfind 1148 #Hoff #Hblock * #id * #Hblock_id #Hlookup_opt 1149 normalize nodelta @refl 1150 ] qed. 890 1151 891 1152 (* We should be able to prove that ty = ty' with some more hypotheses, if needed. *) … … 1012 1273 [ #r  #n  ] 1013 1274 * #cl_type * #Heq_lookup normalize nodelta 1275 [ 3: cases (type_eq_dec ??) normalize nodelta #H 1276 [ 2: whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] 1277  *: ] 1014 1278 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 1015 1279 whd in ⊢ ((??%?) → ?); … … 1057 1321 ] 1058 1322 ] qed. 1059 1323 1060 1324 (* lift simulation result to eval_exprlist *) 1325 1061 1326 lemma eval_exprlist_simulation : 1062 1327 ∀cl_f. … … 1211 1476 qed. (* this last lemma has to be refitted. *) 1212 1477 1213 (* This, to say the least, is not pretty. Whenever we update the memory, we have to perform1214 * a kind of functional record update on the frame_data. But of course, we also need equations1215 * relating the old and new frame data. *)1216 (*1217 lemma update_clight_cminor_data_cm :1218 ∀f, cl_ge, cm_ge, INV.1219 ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.1220 ∀cl_m_v.1221 ∀new_cm_mem.1222 cl_m_v = cl_m … frame_data →1223 ∀new_inj: memory_inj (Em … frame_data) cl_m_v new_cm_mem.1224 ∃data:clight_cminor_data f cl_ge cm_ge INV.1225 alloc_type … frame_data = alloc_type … data ∧1226 cl_env … frame_data = cl_env … data ∧1227 cm_env … frame_data = cm_env … data ∧1228 stackptr … frame_data = stackptr … data ∧1229 cl_m … frame_data = cl_m … data ∧1230 new_cm_mem = (cm_m … data).1231 #f #cl_ge #cm_ge #INV #frame_data #cl_m_v #new_cm_mem #H destruct (H) #Hinj1232 %{(mk_clight_cminor_data ????1233 (alloc_type … frame_data)1234 (stacksize … frame_data)1235 (alloc_hyp … frame_data)1236 (cl_env … frame_data)1237 (cm_env … frame_data)1238 (cl_env_hyp … frame_data)1239 (cl_m … frame_data)1240 new_cm_mem1241 (Em … frame_data)1242 Hinj1243 (stackptr … frame_data)1244 (matching … frame_data)1245 (Em_fn_id … frame_data))}1246 @conj try @conj try @conj try @conj try @conj try @refl1247 qed.*)1248 1249 (* Same thing, this time update both CL and CM memory. Here we provide a proof1250 * that the data in local env is not touched. *)1251 (*1252 lemma update_clight_cminor_data_cl_cm_global :1253 ∀f, cl_ge, cm_ge, INV.1254 ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.1255 ∀new_cl_mem, new_cm_mem.1256 ∀new_inj: memory_inj (Em … frame_data) new_cl_mem new_cm_mem.1257 (∀id, b, cl_type.1258 lookup ?? (cl_env … frame_data) id = Some ? b →1259 lookup ?? (alloc_type … frame_data) id = Some ? 〈Local, cl_type〉 →1260 load_value_of_type cl_type (cl_m … frame_data) b zero_offset =1261 load_value_of_type cl_type new_cl_mem b zero_offset) →1262 ∃data:clight_cminor_data f cl_ge cm_ge INV.1263 alloc_type … frame_data = alloc_type … data ∧1264 cl_env … frame_data = cl_env … data ∧1265 cm_env … frame_data = cm_env … data ∧1266 stackptr … frame_data = stackptr … data ∧1267 new_cl_mem = (cl_m … data) ∧1268 new_cm_mem = (cm_m … data).1269 #f #cl_ge #cm_ge #INV #frame_data #new_cl_mem #new_cm_mem #Hinj #Haux1270 %{(mk_clight_cminor_data ????1271 (alloc_type … frame_data)1272 (stacksize … frame_data)1273 (alloc_hyp … frame_data)1274 (cl_env … frame_data)1275 (cm_env … frame_data)1276 (cl_env_hyp … frame_data)1277 new_cl_mem1278 new_cm_mem1279 (Em … frame_data)1280 Hinj1281 (stackptr … frame_data)1282 ? (* (matching … frame_data) *)1283 (Em_fn_id … frame_data))}1284 [ whd #id1285 lapply (matching … frame_data id)1286 lapply (Haux id)1287 cases (lookup ??? id) normalize nodelta1288 [ #_ #H @H1289  #b cases (lookup ??? id) normalize nodelta1290 [ #_ #H @H1291  * #vartype #cltype normalize nodelta1292 cases vartype try // normalize nodelta #Haux1293 #H #v #Hload @H >(Haux ?? (refl ??) (refl ??)) @Hload1294 ]1295 ]1296 1297 @conj try @conj try @conj try @conj try @conj try @conj try @refl1298 qed.*)1299 1300 1478 lemma store_value_of_type_success_by_value : 1301 1479 ∀ty, m, m', b, o, v. … … 1336 1514  *: %1 #id % #Habsurd destruct (Habsurd) ] 1337 1515 qed. 1338 1339 (* Not provable: need to relate (typeof (e=Evar id, ty)) with the type contained1340 in var_ty. Should be doable, but not now. *)1341 (*1342 lemma translate_dest_IdDest_typ :1343 ∀vars,e,var_id,var_ty,H.1344 translate_dest vars e = return (IdDest vars var_id var_ty H) →1345 var_ty = typeof e.1346 #vars * #ed #ety #var_id #var_ty #H1347 cases ed1348 [ #sz #i  #id  #e1  #e1  #op #e1 #op #e1 #e2  #cast_ty #e11349  #cond #iftrue #iffalse  #e1 #e2  #e1 #e2  #sizeofty  #e1 #field  #cost #e1 ]1350 [ 2,3,12:1351 [ 2,3:1352 whd in ⊢ ((??%?) → ?);1353 cases (translate_addr ??) normalize nodelta1354 [ 2,3: #error whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd)1355  1,4: #Hfoo whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd) ]1356  1: #H' lapply (bind2_eq_inversion ?????? H') * #vt * #t * #Eq1357 lapply Eq inversion vt normalize nodelta1358 [ 1,2: #foo #bar #Hlookup1359 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)1360  3: #e whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)1361  *: whd in ⊢ ((??%?) → ?); whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd)1362 normalize nodelta1363 [ 2:*)1364 1365 1516 1366 1517 lemma mk_offset_offv_id : ∀o. mk_offset (offv o) = o. … … 1453 1604 load_value_of_type ty m b o = Some ? v. 1454 1605 1606 (* Make explicit the contents of [exec_bind_parameters ????] *) 1607 lemma exec_alloc_bind_params_same_length : 1608 ∀e,m,m',params,vars. 1609 exec_bind_parameters e m params vars = OK ? m' → 1610 (params = [ ] ∧ vars = [ ]) ∨ 1611 ∃id,ty,tl_pa,v,tl_vars,b,mi. 1612 params = 〈id,ty〉 :: tl_pa ∧ 1613 vars = v :: tl_vars ∧ 1614 lookup ?? e id = Some ? b ∧ 1615 store_value_of_type ty m b zero_offset v = Some ? mi ∧ 1616 exec_bind_parameters e mi tl_pa tl_vars = OK ? m'. 1617 #e #m #m' #params cases params 1618 [ #vars whd in ⊢ ((??%?) → ?); cases vars normalize nodelta 1619 [ #Heq destruct (Heq) %1 @conj try @refl 1620  #hd_pa #tl_pa #Habsurd destruct (Habsurd) ] 1621  * #id #ty #tl_pa #vars 1622 whd in ⊢ ((??%?) → ?); 1623 cases vars normalize nodelta 1624 [ #Habsurd destruct (Habsurd) 1625  #hd_val #tl_val #H 1626 cases (bind_inversion ????? H) H 1627 #blo * #HA #H 1628 cases (bind_inversion ????? H) H 1629 #m'' * #HB #Hexec_bind %2 1630 %{id} %{ty} %{tl_pa} %{hd_val} %{tl_val} %{blo} %{m''} 1631 @conj try @conj try @conj try @conj try @refl 1632 try @(opt_to_res_inversion ???? HA) 1633 try @(opt_to_res_inversion ???? HB) 1634 @Hexec_bind 1635 ] 1636 ] qed. 1637 1638 (* Axiomfest, with all the lemmas we need but won't have time to prove. Most of them are not too hard. *) 1639 1640 (* The way we have of stating this is certainly not the most synthetic. The property we really need is that 1641 * stmt_univ' is fresher than stmt_univ, which sould be trivially provable by a simple induction. *) 1642 axiom env_below_freshgen_preserved_by_translation : 1643 ∀cl_env, alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, s, stmt_univ', lbl_univ', cm_s, H. 1644 env_below_freshgen cl_env alloc_type stmt_univ → 1645 translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp s = return «〈stmt_univ', lbl_univ', cm_s〉, H» → 1646 env_below_freshgen cl_env alloc_type stmt_univ'. 1647 1648 axiom tmp_vars_well_allocated_preserved_by_inclusion : 1649 ∀cm_env, cm_m, cl_m, Em, tmpenv, tmpenv'. 1650 lset_inclusion ? tmpenv tmpenv' → 1651 tmp_vars_well_allocated tmpenv' cm_env cm_m cl_m Em → 1652 tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em. 1653 1654 axiom translation_entails_ident_inclusion : 1655 ∀alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, stmt_univ'. 1656 ∀cl_s, cm_s, labgen, Htrans_inv. 1657 translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = return «〈stmt_univ',labgen,cm_s〉,Htrans_inv» → 1658 lset_inclusion ? (tmp_env … stmt_univ) (tmp_env … stmt_univ'). 1659 1660 (* Same remarks as above apply here too. *) 1661 (* 1662 lemma tmp_vars_well_allocated_preserved_by_translation : 1663 ∀cm_env, alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, stmt_univ'. 1664 ∀Em, cm_m, cl_m, cl_s, cm_s, labgen, Htrans_inv. 1665 translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = return «〈stmt_univ',labgen,cm_s〉,Htrans_inv» → 1666 tmp_vars_well_allocated (tmp_env alloc_type stmt_univ') cm_env cm_m cl_m Em → 1667 tmp_vars_well_allocated (tmp_env alloc_type stmt_univ) cm_env cm_m cl_m Em. 1668 #cm_env #alloc_type #stmt_univ #lbl_univ #lbls #flag #rettyp #stmt_univ' #Em #cm_m #cl_m #cl_s #cm_s 1669 #labgen #Htrans_inv #Htranslate_statement #H #id #Hpresent #ty #Hexists 1670 @H lapply (translation_entails_ident_inclusion … Htranslate_statement) 1671 #H 1672 @H23*) 1673 1674 axiom tmp_vars_well_allocated_conserved_by_frame_free : 1675 ∀alloc_type, tmpenv, cl_env, cm_env, cm_m, cl_m, stackptr. 1676 ∀Em, cl_ge, cm_ge, INV. 1677 ∀Hmatching:memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type. 1678 tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em > 1679 tmp_vars_well_allocated tmpenv cm_env (free cm_m stackptr) (free_list cl_m (blocks_of_env cl_env)) Em. 1680 1681 axiom generated_id_not_in_env : 1682 ∀id, blo, tmp, ty. 1683 ∀env: cl_env. 1684 ∀alloc_type. 1685 ∀freshgen, freshgen': tmpgen alloc_type. 1686 env_below_freshgen env alloc_type freshgen → 1687 lookup ?? env id = Some ? blo → 1688 alloc_tmp alloc_type ty freshgen = 〈tmp, freshgen'〉 → 1689 tmp ≠ id. 1690 1691 (* This should just be lifting a lemma from positive maps to identifier maps. 1692 * Sadly, the way things are designed requires a boring induction. *) 1693 axiom update_lookup_opt_other : 1694 ∀b,a,t,H. 1695 ∀b'. b ≠ b' → 1696 lookup SymbolTag val t b' = lookup SymbolTag val (update_present SymbolTag val t b H a) b'. 1697 1698 1699 (* NOTE: this axiom is way more general than what we need. In practice, cm_m' is cm_m after a store. *) 1700 axiom clight_cminor_cont_rel_parametric_in_mem : 1701 ∀cl_ge, cm_ge, INV, cl_f, cm_f, cl_env, cm_env, cm_m, cm_m', alloc_type, tmpenv, (*stmt_univ, stmt_univ', *) rettyp, cl_k, cm_k, cm_st. 1702 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st → 1703 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m' alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st. 1704 1705 (* Same remark as above. *) 1706 axiom well_allocated_preserved_by_parallel_stores : 1707 ∀tmpenv, cm_env, cm_m, cm_m', cl_m, cl_m', Em. 1708 1709 (* TODO: proper hypotheses (the following, commented out do not exactly fit) 1710 (storen cm_m (mk_pointer cl_blo (mk_offset (offv zero_offset))) (fe_to_be_values (typ_of_type (typeof rhs)) cm_rhs_val) 1711 =Some mem cm_mem_after_store_lhs) 1712 storev (typ_of_type ty) cl_m (Vptr (mk_pointer cl_blo zero_offset)) cl_rhs_val = Some ? cl_m') *) 1713 1714 tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em → 1715 tmp_vars_well_allocated tmpenv cm_env cm_m' cl_m' Em. 1716 1717 (* Same remark as above. Moreover, this should be provable from memory injections. *) 1718 axiom memory_matching_preserved_by_parallel_stores : 1719 ∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cm_m', cl_env, cm_env, INV, stackptr, alloc_type. 1720 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type → 1721 memory_matching Em cl_ge cm_ge cl_m' cm_m' cl_env cm_env INV stackptr alloc_type. 1722 1723 axiom clight_cminor_cont_rel_parametric_in_cm_env : 1724 ∀cl_ge, cm_ge, INV, cl_f, cm_f, cl_env, cm_env, cm_m, alloc_type, tmpenv, (*stmt_univ, stmt_univ',*) rettyp, cl_k, cm_k, cm_st, var_id, v. 1725 ∀Hpresent:present SymbolTag val cm_env var_id. 1726 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st > 1727 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env 1728 (update_present SymbolTag val cm_env var_id Hpresent v) cm_m 1729 alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st. 1730 1731 axiom tmp_vars_well_allocated_preserved_by_local_store : 1732 ∀Em, cl_value, cm_value, lhs_ty, cl_m, cl_m', cm_m, cl_blo, tmpenv, cm_env, var_id. 1733 ∀Hpresent:present SymbolTag val cm_env var_id. 1734 value_eq Em cl_value cm_value → 1735 store_value_of_type' lhs_ty cl_m 〈cl_blo, zero_offset〉 cl_value = Some ? cl_m' → 1736 tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em → 1737 tmp_vars_well_allocated tmpenv 1738 (update_present ?? cm_env var_id Hpresent cm_value) cm_m 1739 cl_m' Em. 1740 1741 axiom memory_inj_preserved_by_local_store : 1742 ∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cl_env, cm_env, INV, stackptr, alloc_type. 1743 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type > 1744 memory_inj Em cl_m cm_m > 1745 memory_inj Em cl_m' cm_m. 1746 1747 axiom memory_matching_preserved_by_local_store : 1748 ∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cl_env, cm_env, INV, stackptr, alloc_type, cl_value, cm_value. 1749 ∀cl_blo, var_id, lhs_ty. 1750 ∀Hpresent:present SymbolTag val cm_env var_id. 1751 value_eq Em cl_value cm_value → 1752 store_value_of_type' lhs_ty cl_m 〈cl_blo, zero_offset〉 cl_value = Some ? cl_m' → 1753 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type → 1754 memory_matching Em cl_ge cm_ge cl_m' cm_m cl_env 1755 (update_present SymbolTag val cm_env var_id Hpresent cm_value) INV stackptr alloc_type. 1756 1757 lemma translate_dest_conservation : 1758 ∀vars, e1. 1759 ∀id, t, H. 1760 translate_dest vars e1 = OK ? (IdDest vars id t H) → 1761 typeof e1 = t. 1762 #vars #e1 #id #t #H #Htranslate lapply (translate_dest_id_inversion … Htranslate) 1763 #Heq >Heq in Htranslate; 1764 whd in ⊢ ((??%?) → ?); 1765 generalize in match (refl ??); 1766 generalize in ⊢ ((???%) → (??(match % with [ _ ⇒ ?  _ ⇒ ? ] ?)?) → ?); * 1767 normalize nodelta 1768 [ 2: #er #_ #Habsurd destruct (Habsurd) ] 1769 * * normalize nodelta 1770 [ #a #b #c #Habsurd 1771  #n #t #H #Habsurd 1772  #ty #H ] 1773 [ 1,2: destruct (Habsurd) ] 1774 cases (type_eq_dec ??) normalize nodelta 1775 #Hty #Heq destruct (Heq) >Hty @refl 1776 qed. 1777 1778 lemma alloc_tmp_monotonic : 1779 ∀alloc_type, ty, univ, univ', v. 1780 alloc_tmp alloc_type ty univ = 〈v, univ'〉 → 1781 lset_inclusion ? (tmp_env ? univ) (tmp_env ? univ'). 1782 #alloc_type #ty #univ #univ' #v cases univ 1783 #u #env #Hfresh #Hyp #Halloc 1784 cases (breakup_dependent_match_on_pairs ?????? Halloc) Halloc 1785 #v * #u' * #Heq * #Heq' normalize nodelta #Heq'' 1786 destruct (Heq'') 1787 @cons_preserves_inclusion @reflexive_lset_inclusion 1788 qed. 1789 1790 (* 1791 lemma lset_inclusion_Exists : 1792 ∀A. ∀l1, l2: lset A. 1793 lset_inclusion ? l1 l2 → 1794 ∀P. Exists ? P l1 → Exists ? P l2. 1795 #A #l1 elim l1 1796 [ #l2 #Hincl #P @False_ind 1797  #hd #tl #Hind #l2 * #Hmem #Hincl2 #P * 1798 [ 2: #Htl @Hind assumption ] 1799 lapply P P 1800 lapply Hincl2 Hincl2 1801 lapply Hmem Hmem elim l2 1802 [ @False_ind ] 1803 #hd2 #tl2 #Hind2 * 1804 [ #Heq destruct (Heq) 1805 #Hincl2 #P #H %1 @H 1806  #Hmem #Hincl2 #P #H %2 1807 elim tl2 in Hmem; 1808 [ @False_ind 1809  #hd2' #tl2' #Hind3 * 1810 [ #Heq destruct (Heq) %1 assumption 1811  #Hmem' %2 @Hind3 @Hmem' ] 1812 ] 1813 ] 1814 ] qed. *) 1815 1455 1816 (*  *) 1456 1817 (* Main simulation results *) 1457 (*  ; *)1818 (*  *) 1458 1819 1459 1820 (* Conjectured simulation results … … 1470 1831 subtrace corresponding to a measurable Clight subtrace. 1471 1832 *) 1472 1473 1833 (* 1834 lemma clight_cminor_call_return : 1835 ∀g1, g2. 1836 ∀INV:clight_cminor_inv g1 g2. 1837 ∀s1,s1'. 1838 clight_cminor_rel g1 g2 INV s1 s1' → 1839 match Clight_classify s1 with 1840 [ cl_call ⇒ true 1841  cl_return ⇒ true 1842  _ ⇒ false ] → 1843 ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 → 1844 ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'. 1845 tr = tr' ∧ 1846 clight_cminor_rel g1 g2 INV s2 s2' ∧ 1847 (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1)) 1848 ). 1849 #g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class 1850 inversion Hstate_rel 1851 [ 1: (* normal *) 1852 #cl_ge #cm_ge #INV' #cl_s 1853 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 1854 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize 1855 (* introduce everything *) 1856 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 1857 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 1858 #flag #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC 1859 #HE #HF #HG #HI #HJ #HK 1860 @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2 1861 destruct (H1 H2) 1862 @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5 1863 destruct (H3 H4 H5) 1864 @False_ind @Hclight_class 1865  5: 1866 #cl_ge #cm_ge #INV' #cl_s 1867 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 1868 #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab 1869 #cm_cond #cm_body #cm_stack #rettyp' #kInv 1870 (* introduce everything *) 1871 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 1872 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 1873 #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr 1874 #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl 1875 #Hlabdecl #Hinv1 #Hinv2 #Hfindlab 1876 @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2 1877 destruct (H1 H2) 1878 @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5 1879 destruct (H3 H4 H5) 1880 @False_ind @Hclight_class 1881  2: 1882 #cl_ge #cm_ge #INV' #cl_f #cm_f #cl_k #cm_k #alloc_type 1883 #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #stacksize 1884 #stmt_univ #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp 1885 #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel 1886 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1887 destruct (HA HB) 1888 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_ 1889 destruct (HC HD HE) 1890 inversion Hcont_rel 1891 [ #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type #kstack #Hkstack 1892 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1893 destruct (HA HB) 1894 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 1895 destruct (HC HD HE) 1896 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH 1897 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL 1898 destruct (HF HG HH HI HJ HK HL) #_ 1899 #s2 #tr 1900 whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd) 1901  (* Kseq *) 1902 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_s #kcm_s 1903 #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag 1904 * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved 1905 #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_ 1906 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1907 destruct (HA HB) 1908 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 1909 destruct (HC HD HE) 1910 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI 1911 @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL 1912 destruct (HF HG HH HI HJ HK HL) #_ 1913 #s2 #tr 1914 whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd) 1915  (* *) 1916 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_env #kcm_env 1917 #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body 1918 #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ'' 1919 #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared 1920 #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHfind_label 1921 (* 1922 * * * * #kHentry_declared * * * * 1923 * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise'' 1924 #kHcont_inv #kHmklabels #kHeq_translate 1925 #kHfind_label *) #kHcont_rel #_ 1926 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1927 destruct (HA HB) 1928 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 1929 destruct (HC HD HE) 1930 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH 1931 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 1932 @(jmeq_absorb ?????) #HL 1933 destruct (HF HG HH HI HJ HK HL) #_ 1934 #s2 #tr 1935 whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd) 1936 ] 1937  3: 1938 #cl_ge #cm_ge #INV' #alloc_type 1939 #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #func_univ 1940 #cl_f #cm_f #Hglobals_fresh #Hfundef_fresh 1941 #rettyp #cl_k #cm_k #fblock * 1942 #Hrettyp #Hfind_funct_cl #Hfind_func_cm #Htranslate_function #Hcont_rel 1943 #fun_id #cl_retval #cm_retval #sInv #fInv #kInv #cl_args #cm_args 1944 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1945 destruct (HA HB) 1946 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 1947 destruct (HC HD HE) #_ 1948 #s2 #tr whd in ⊢ ((??%?) → ?); 1949 @(match (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f)) 1950 return λx. (x = (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))) → ? 1951 with 1952 [ mk_Prod new_cl_env cl_m_alloc ⇒ ? 1953 ] (refl ? (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f)))) 1954 #Hexec_alloc_variables normalize nodelta 1955 #Hstep 1956 cases (bindIO_inversion ??????? Hstep) Hstep 1957 #cl_m_init * #Hexec_bind_parameters 1958 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 1959 %{1} whd whd in ⊢ (??%?); 1960 (* Alloc big chunk of data of size (f_stacksize cm_f) *) 1961 @(match (alloc cm_m 0 (f_stacksize cm_f)) 1962 return λx. (alloc cm_m 0 (f_stacksize cm_f) = x) → ? 1963 with 1964 [ mk_Prod new_cm_mem new_cm_stackptr ⇒ ? 1965 ] (refl ? (alloc cm_m 0 (f_stacksize cm_f)))) 1966 #H_cm_alloc normalize nodelta 1967 (* Initialise CM /parameters/ *) 1968 1969 1970 %{(S (times 3 (fn_vars)))} Hclight_class 1971 lapply (exec_alloc_bind_params_same_length … Hexec_bind_parameters) 1972 elim cl_args in Hstate_rel Hexec_alloc; 1973 [ #Hstate_rel whd in ⊢ ((??%%) → ?); 1974 1975 whd in match (exec_bind_parameters ????); 1976 1977 exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env, cl_m'〉 1978 1979 1980 lapply (let_prod_as_inversion ?????? Hstep) 1981 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH 1982 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 1983 @(jmeq_absorb ?????) #HL 1984 destruct (HF HG HH HI HJ HK HL) #_ 1985 #s2 #tr 1986 1987 1988 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp 1989 #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel 1990 ] qed. *) 1474 1991 1475 1992 lemma clight_cminor_normal : … … 1541 2058  #structname #fieldspec  #unionname #fieldspec  #id ] 1542 2059 #Hlabels_translated #Htmps_preserved 1543 #Hreturn_ok #Hlabel_wf #Htranslate #Hlabel_inclusion 2060 #Hreturn_ok #Hlabel_wf #Htranslate #Hlabel_inclusion #tmpenv #Htmpenv 1544 2061 #Hcont_rel 1545 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id 1546 #Hframe_spec 2062 #Em #Htmp_vars_well_allocated 2063 #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id 2064 #Hframe_spec #Henv_below 1547 2065 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1548 2066 destruct (HA HB) 1549 2067 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_ 1550 destruct (HC HD HE) 1551 lapply Htranslate Htranslate 2068 destruct (HC HD HE) 2069 lapply Htranslate Htranslate 1552 2070 [ 1: generalize in match (conj ????); #Hugly_inv 1553 2071  2: generalize in match (conj ????); #Hugly_inv … … 1637 2155 @(CMR_normal … Htrans_body) try assumption 1638 2156 @(ClCm_cont_while … (sym_eq … Hmk_label_eq) … Htrans_body) try assumption 1639 [ 1,6,11,16: 1640 @refl 1641  2,3,7,8,12,13,17,18: 1642 >CMcast_identity try assumption 1643  4,9,14,19: 2157 try @refl 2158 [ 1,4,7,10: @eq_to_jmeq assumption 2159  2,5,8,11: 1644 2160 @conj try assumption @conj @conj try assumption @conj @conj try assumption 1645 2161 try @conj try assumption try @conj try assumption 1646 2162 try @conj try assumption try @conj try assumption 1647  5,10,15,20: (* find_label_always *)1648 (* TODO /!\ we need to find a clever way to prove this.*)2163  *: (* find_label_always *) 2164 (* TODO /!\ implement necessary invariant on label lookup *) 1649 2165 @cthulhu 1650 2166 ] … … 1676 2192 @conj try @conj try @conj 1677 2193 [ 1,4,7,10: normalize >append_nil >append_nil @refl 1678  2,5,8,11: 1679 @(CMR_normal … Htranslate_function … DoNotConvert … Hcont_rel) try assumption1680 [ 2,4,6,8: @refl  *: ]2194  2,5,8,11: 2195 @(CMR_normal … Htranslate_function … DoNotConvert) try assumption 2196 try @refl try @(env_below_freshgen_preserved_by_translation … Henv_below Htrans_body) 1681 2197  *: #Habsurd destruct (Habsurd) ] 1682 2198 ] … … 1690 2206 (* generalize away ugly proof *) 1691 2207 generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly 1692 #Htranslate #Hlabel_inclusion # Hcont_rel #Em2208 #Htranslate #Hlabel_inclusion #tmpenv #Htmpenv #Hcont_rel #Em 1693 2209 #Htmp_vars_well_allocated 1694 2210 #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id 1695 #Hframe_spec 2211 #Hframe_spec #Henv_below 1696 2212 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1697 2213 destruct (HA HB) … … 1719 2235 #Hdest cases (bind_inversion ????? Hdest) Hdest #dest * 1720 2236 inversion dest normalize nodelta 1721 [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest 2237 [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest 1722 2238 #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1723 2239 (* make explicit the nature of lhs, allowing to prove that no trace is emitted *) … … 1734 2250 generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2 1735 2251 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] 2252 (* Now, execute the Clight call *) 1736 2253 #s2 #tr #Htranslate 1737 2254 cases (bindIO_inversion ??????? Htranslate) Htranslate * 1738 # func_ptr_val #func_trace * #Hexec_func_ptrnormalize nodelta2255 #CL_callee_val #CL_callee_trace * #Hexec_CL_callee normalize nodelta 1739 2256 whd in ⊢ ((???%) → ?); #Htranslate 1740 2257 cases (bindIO_inversion ??????? Htranslate) Htranslate * 1741 # args_values #args_trace * #Hexec_arglist#Htranslate2258 #CL_args #CL_args_trace * #Hexec_CL_args #Htranslate 1742 2259 cases (bindIO_inversion ??????? Htranslate) Htranslate 1743 * #cl_fundef #cl_fun_id * #Hfind_funct 2260 * #CL_callee_fundef #CL_callee_id * #Hfind_funct 2261 (* We've got the CL fundef. Extract a function pointer out of it. *) 1744 2262 lapply (opt_to_io_Value ?????? Hfind_funct) Hfind_funct #Hfind_funct 1745 2263 cases (find_funct_inversion ???? Hfind_funct) 1746 #func_ptr * * * #Hfunc_ptr_eq destruct (Hfunc_ptr_eq) 1747 #Hpoff_eq_zero #Hregion_is_code 1748 * #block_id * #Hblock_id_neg #Hlookup 2264 #CL_callee_ptr * * * #HCL_callee_eq destruct (HCL_callee_eq) 2265 (* Done. Now stash the resulting properties of this pointer in the context. *) 2266 #HCL_callee_ptr_offset_eq_zero #HCL_callee_ptr_region_eq_Code 2267 (* Some more properties, that should stay hidden. XXX we discard them, this should not hinder the proof *) 2268 * #block_id * #Hblock_id_neg #Hlookup Hlookup Hblock_id_neg block_id 2269 (* Now, break up a safety check for the type of the function and finally, execute the 2270 * CL lvalue supposed to store the result of the function call. This will yield a pointer 2271 * that will be stored in the Callstate, until the function call returns and we store te 2272 * result inside it. Of course, this does not apply to the case wich returns void. *) 1749 2273 #Htranslate 1750 2274 cases (bindIO_inversion ??????? Htranslate) Htranslate #Htype_of_fundef * 1751 2275 #Hassert_type_eq 1752 [ 1,2: #Htranslate 1753 cases (bindIO_inversion ??????? Htranslate) Htranslate * * 1754 #lblock #loffset #ltrace * 1755 whd in ⊢ ((???%) → (???%) → ?); 1756 [ >Hlhs_eq #Hexec_lvalue 1757 cut (ltrace = []) 1758 [ lapply (res_to_io ????? Hexec_lvalue) 2276 [ 1,2: (* Cases where we return something. *) 2277 #Htranslate 2278 cases (bindIO_inversion ??????? Htranslate) Htranslate * * 2279 #CL_lvalue_block #CL_lvalue_offset #CL_lvalue_trace * 2280 whd in ⊢ ((???%) → (??%%) → ?); 2281 [ >Hlhs_eq #HCL_exec_lvalue 2282 (* The trace is empty since we execute a variable *) 2283 cut (CL_lvalue_trace = []) 2284 [ lapply (res_to_io ????? HCL_exec_lvalue) 1759 2285 #H' whd in H':(??%?); cases (lookup ????) in H'; normalize nodelta 1760 2286 [ 2: #b #Heq destruct (Heq) @refl … … 1762 2288 whd in H28:(???%); destruct (H28) @refl ] 1763 2289 ] #H destruct (H) 1764  #H exec_lvalue ]2290  #HCL_exec_lvalue ] 1765 2291  3: ] 1766 2292 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 1767 [ 1: %{1} whd whd in ⊢ (??%?); normalize nodelta 1768  2: (* Execute Cminor part: evaluate lhs, evaluate assign *) 2293 (* We have reached the final Clight state. Now execute the Cminor transalted code. *) 2294 [ 1: (* Return to a variable *) 2295 %{1} whd whd in ⊢ (??%?); normalize nodelta 2296  2: (* Return to memory location. Need to create a tmp CM local variable to store the 2297 * lvalue ptr (otherwise trace does not match CL). *) 1769 2298 %{5} whd whd in ⊢ (??%?); normalize nodelta 1770 2299 whd in match (eval_expr ???????); 1771 2300 whd in match (m_bind ?????); 2301 (* Evalue Cminor lvalue. Need to feed some invariants to the simulation lemma, that 2302 * we bake here and now. *) 1772 2303 cut (expr_vars ASTptr cm_expr 1773 2304 (λid:ident.λty:typ.present SymbolTag val cm_env id)) 1774 2305 [ cases sInv * * * * * * * #_ #H #_ #_ #_ @H ] #Hexpr_vars_cut 1775 lapply (translate_dest_MemDest_simulation … Htranslate_dest Hexec_lvalue) 2306 (* Apply simulation lemma for lvalues *) 2307 lapply (translate_dest_MemDest_simulation … Htranslate_dest HCL_exec_lvalue) 1776 2308 try assumption try @refl 1777 * # cm_val_tmp * #Heval_expr_tmp >Heval_expr_tmp #Hvalue_eq2309 * #CM_lvalue * #HCM_eval_lvalue >HCM_eval_lvalue #Hvalue_eq_lvalues 1778 2310 normalize nodelta generalize in match (proj1 ???); #Htmp_var_present 1779 cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_val_tmp #Hcm_ptr_translation 1780 >Hcm_val_tmp 1781 lapply (Htmp_vars_well_allocated … tmp_var Htmp_var_present (Tpointer (typeof lhs)) ? (Vptr cm_ptr) ?) 1782 [ 2: @(alloc_tmp_in_genlist … (sym_eq ??? Heq_alloc_tmp) (sym_eq ??? Heq_alloc_tmp')) 1783  1: normalize cases cm_ptr #b #o %3 ] 1784 * #cm_mem_after_store * #Hstorev #Hnew_inj >Hstorev 2311 (* Make explicit the fact that the CM lvalue is a pointer *) 2312 cases (value_eq_ptr_inversion … Hvalue_eq_lvalues) #CM_lvalue_ptr * #HCM_value_ptr_eq #HCM_lvalue_ptr_trans 2313 >HCM_value_ptr_eq 2314 lapply (Htmp_vars_well_allocated … tmp_var Htmp_var_present (Tpointer (typeof lhs)) ? (Vptr CM_lvalue_ptr) ?) 2315 [ 1: normalize cases CM_lvalue_ptr #b #o %3 2316  2: lapply (alloc_tmp_in_genlist … (sym_eq ??? Heq_alloc_tmp) (sym_eq ??? Heq_alloc_tmp')) 2317 #Hexists' @(lset_inclusion_Exists … Hexists' Htmpenv) 2318 ] 2319 * #CM_mem_after_store * #Hstorev #Hnew_inj >Hstorev 1785 2320 whd in match (m_bind ?????); normalize nodelta 1786 2321 whd whd in ⊢ (??%?); normalize nodelta 1787 (* cases (update_clight_cminor_data_cm … frame_ … Hnew_inj)1788 try assumption #frame_data'1789 * * * * * #Halloctype_eq_frame_data #Hcl_env_eq_frame_data #Hcm_env_eq_frame_data1790 #Hstackptr_eq_frame_data #Hcl_m_eq_frame_data #Hcm_m_eq_frame_data *)1791 2322  3: %{1} whd whd in ⊢ (??%?); normalize nodelta 1792 2323 ] 1793 (* execute Cminor part*)2324 (* cleanup ugliness *) 1794 2325 [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???)); 1795 2326  2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???)); … … 1804 2335 @Hexpr_vars_present_ef' ] 1805 2336 #Hexpr_vars_present_ef 1806 lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_ func_ptr)2337 lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_CL_callee) 1807 2338 Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func 1808 2339 cut (eval_expr cm_ge ASTptr ef' cm_env Hexpr_vars_present_ef' 1809 stackptr cm_m = OK (trace×val) 〈 func_trace,cm_func_ptr_val〉)2340 stackptr cm_m = OK (trace×val) 〈CL_callee_trace,cm_func_ptr_val〉) 1810 2341 [ 1,3: 1811 2342 lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef' … … 1815 2346 Heval_func #Heval_func >Heval_func 1816 2347  2: (* treat case 2 as special, since the type differs slightly *) 1817 cases (eval_expr_sim … INV' … Halloc_hyp ? cm_env Hcl_env_hyp … Hnew_inj stackptr Hmatching) 2348 letin cm_env' ≝ (update_present SymbolTag val cm_env tmp_var Htmp_var_present (Vptr CM_lvalue_ptr)) 2349 cut (memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env' INV' stackptr alloc_type) 2350 (* cut (memory_matching Em cl_ge cm_ge cl_m CM_mem_after_store cl_env cm_env' INV' stackptr alloc_type) *) 2351 [ (* Proving preservation of the memory matching under store in "new" cminor memory zone. 2352 Use the property that the ident [tmp_var] is not in the clight env. *) 2353 #id lapply (Hmatching id) 2354 @(match (lookup ??? id) 2355 return λx. (lookup ??? id = x) → ? 2356 with 2357 [ None ⇒ λHeq_lookup. ? 2358  Some blo ⇒ λHeq_lookup. ? 2359 ] (refl ? (lookup ??? id))) 2360 [ 1: #H @H ] normalize nodelta 2361 cases (lookup ??? id) normalize nodelta 2362 [ 1: #H @H ] * #var_ty #cl_ty cases var_ty normalize nodelta 2363 [ #r #H @H 2364  #n #H @H 2365  #H #v #Hload_value_of_type lapply (H ? Hload_value_of_type) 2366 * #v' * #Hlookup_cm #Hvalue_eq %{v'} @conj try @Hvalue_eq 2367 lapply (alloc_tmp_env_invariant ?????? (sym_eq ??? Heq_alloc_tmp) Henv_below) #Henv_below' 2368 lapply (generated_id_not_in_env ???????? Henv_below' … Heq_lookup (sym_eq ??? Heq_alloc_tmp')) 2369 #Hneq <(update_lookup_opt_other … (Vptr CM_lvalue_ptr) … cm_env … Htmp_var_present … Hneq) 2370 assumption ] ] #Hmatching' 2371 cases (eval_expr_sim … INV' … Halloc_hyp ? cm_env' Hcl_env_hyp … Hinjection stackptr Hmatching') 1818 2372 #Hsim_expr #_ 1819 2373 generalize in match (proj2 ???); #Hall_present … … 1821 2375 generalize in match (proj2 ???); #Hstore_inv 1822 2376 generalize in match (conj ????); #Hstmt_inv 1823 cut (eval_expr cm_ge ? ef' cm_env? stackptr cm_m =1824 (eval_expr cm_ge ASTptr ef' cm_env ? stackptr cm_m)) try assumption try @refl1825 #Heval_expr_rewrite >Heval_expr_rewrite Heval_expr_rewrite 1826 lapply (Hsim_expr … Htranslate_ef … (Vptr func_ptr) func_trace ??)2377 (* cut (eval_expr cm_ge ? ef' cm_env' ? stackptr cm_m = 2378 (eval_expr cm_ge ASTptr ef' cm_env' ? stackptr cm_m)) try assumption try @refl 2379 #Heval_expr_rewrite >Heval_expr_rewrite Heval_expr_rewrite *) 2380 lapply (Hsim_expr … Htranslate_ef … (Vptr CL_callee_ptr) CL_callee_trace ??) 1827 2381 try assumption 1828 2382 [ lapply Hexpr_vars_present_ef' lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef' 1829 2383 lapply ef >Htyp_equality_ef #ef #HA #HB @(jmeq_absorb ?????) #Heq destruct (Heq) #x @x ] 1830 * # cm_func_ptr_val* #Heval_func_cm #Hvalue_eq_func2384 * #CM_callee_ptr * #Heval_func_cm #Hvalue_eq_func 1831 2385 (* And some more shuffling types around to match the goal *) 1832 cut (eval_expr cm_ge ? ef' cm_env Hexpr_vars_present_ef' stackptr cm_mem_after_store = OK ? 〈func_trace,cm_func_ptr_val〉)2386 cut (eval_expr cm_ge ? ef' cm_env' Hexpr_vars_present_ef' stackptr cm_m = OK ? 〈CL_callee_trace,CM_callee_ptr〉) 1833 2387 [ lapply Heval_func_cm Heval_func_cm 1834 2388 generalize in ⊢ ((??(?????%??)?) → ?); … … 1845 2399 #Htranslate_fundef #Hfind_funct_cm 1846 2400 lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr 1847 whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero; 2401 whd in ⊢ ((??%?) → ?); 2402 cases CL_callee_ptr in Hfind_funct Hfind_funct_cm HCL_callee_ptr_region_eq_Code HCL_callee_ptr_offset_eq_zero; 1848 2403 #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero) 1849 2404 whd in ⊢ ((??%?) → ?); 1850 2405 [ 1,2: >(HEm_fn_id … cm_block Hregion_is_code) 1851 2406  3: >(HEm_fn_id … cm_block Hregion_is_code) ] 1852 normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off' 2407 normalize nodelta 2408 cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off' 1853 2409 #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq) 1854 2410 [ 1,2: >addition_n_0 >mk_offset_offv_id … … 1868 2424  3: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ] 1869 2425 #Hall 1870 cases (eval_exprlist_simulation … Halloc_hyp Hcl_env_hyp Hinjection Hmatching ???? Hexec_ arglistHargs_spec Hall)2426 cases (eval_exprlist_simulation … Halloc_hyp Hcl_env_hyp Hinjection Hmatching ???? Hexec_CL_args Hargs_spec Hall) 1871 2427 #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list 1872 2428  3: 1873 (* Arrrgh *) 1874 lapply (eval_exprlist_simulation … Halloc_hyp Hcl_env_hyp Hnew_inj ????? Hexec_arglist Hargs_spec ?) 1875 try assumption * 1876 #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list 2429 lapply (eval_exprlist_simulation … Halloc_hyp Hcl_env_hyp Hinjection ????? Hexec_CL_args Hargs_spec ?) 2430 try assumption 2431 * #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list 1877 2432 ] 1878 2433 whd in match (m_bind ?????); normalize nodelta whd @conj 1879 2434 [ 2,4,6: #Habsurd destruct (Habsurd) ] 1880 2435 @conj 1881 [ 1,3,5: normalize try @refl 1882 >append_nil >append_nil @refl ] 2436 [ 1,3,5: normalize try @refl >append_nil >append_nil @refl ] 1883 2437 [ 1: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres 1884 2438  2: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres 1885 2439  3: ] 1886 (* [ 3: >addition_n_0 ]*) 1887 [ 1,2: (* no return or return to CM local variable *) 1888 @(CMR_call_nostore … tmp_u) try assumption 1889 [ 2,4: (* TODO: prove matching between CL and CM function ids *) 1890 @cthulhu 2440 [ 3: @(CMR_call … Htranslate_function … Hinjection … Hmatching … HEm_fn_id) try assumption 2441 lapply (alloc_tmp_monotonic … (sym_eq ??? Heq_alloc_tmp)) #Hincl1 2442 lapply (alloc_tmp_monotonic … (sym_eq ??? Heq_alloc_tmp')) #Hincl2 2443 lapply (transitive_lset_inclusion … Hincl1 Hincl2) #Hincl3 2444 try /2 by transitive_lset_inclusion/ 2445 lapply Htranslate_fundef Htranslate_fundef 2446 lapply Hfundef_fresh_for_tmp_u Hfundef_fresh_for_tmp_u 2447 cases CL_callee_fundef normalize nodelta 2448 [ 1: #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef @ClCm_cont_call_store 2449  2: #id #tl #ty #Hfd_fresh 2450 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) normalize nodelta @I ] 2451  1,2: (* no return or return to CM local variable *) 2452 @(CMR_call … Htranslate_function … Hinjection … Hmatching … HEm_fn_id) try assumption 2453 cases CL_callee_fundef in Hfundef_fresh_for_tmp_u Htranslate_fundef; normalize nodelta 2454 [ 1,3: (* Internal case *) 2455 #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef 2456 whd nodelta in match (typeof ?); 2457 [ <(translate_dest_conservation … Htranslate_dest) 2458 @ClCm_cont_call_nostore normalize nodelta 2459 %{CL_lvalue_block} %{CL_lvalue_offset} %{(typeof lhs)} %{var_id} 2460 @conj @refl 2461  @ClCm_cont_call_nostore normalize nodelta @I ] 2462  2,4: #fid #tl #ty #H1 #H2 2463 whd in H2:(??%?); destruct (H2) @I 1891 2464 ] 1892 lapply Hfind_funct1893 lapply Hfind_funct_cm1894 lapply Htranslate_fundef1895 lapply Hfundef_fresh_for_tmp_u1896 lapply Hassert_type_eq1897 lapply Htype_of_fundef1898 lapply Hlookup1899 cases cl_fundef1900 [ 2,4: #id #typel #ty #HA #HB #HC #HD #HE #HF #HG @I1901  1,3: #f #HA #HB #HC #HD #HE #HF #HG normalize nodelta1902 @conj try @conj try @conj try assumption ]1903  3: (* type mismatch *)1904 @(CMR_call_store … tmp_u) try assumption1905 [ 2: (* TODO: prove matching between CL and CM function ids *)1906 @cthulhu ]1907 lapply Hfind_funct1908 lapply Htranslate_fundef1909 lapply Hfundef_fresh_for_tmp_u1910 lapply Hassert_type_eq1911 lapply Htype_of_fundef1912 lapply Hlookup1913 cases cl_fundef1914 [ 2: #id #typel #ty #HA #HB #HC #f #HD #HE @I ]1915 #f #HA #HB #HC #HD #HE #HF normalize nodelta @conj try @conj try @conj1916 try assumption1917 2465 ] 1918 2466  1: (* Skip *) … … 1926 2474 #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly 1927 2475 whd in ⊢ ((??%?) → ?); #Heq_translate #Hlabel_inclusion 1928 # Hcont_rel2476 #tmpenv #Htmpenv #Hcont_rel 1929 2477 lapply Heq_translate Heq_translate 1930 lapply Hugly Hugly 1931 lapply Hlabel_wf Hlabel_wf 2478 lapply Hugly Hugly 2479 lapply Hlabel_wf Hlabel_wf 1932 2480 lapply Hreturn_ok Hreturn_ok 1933 lapply Htmps_preserved Htmps_preserved 2481 lapply Htmps_preserved Htmps_preserved 1934 2482 lapply Hlabels_translated Hlabels_translated 1935 lapply Hstmt_inv Hstmt_inv 2483 lapply Hstmt_inv Hstmt_inv 1936 2484 lapply Htranslate_function Htranslate_function 1937 lapply Hfresh_globals Hfresh_globals 2485 lapply Hfresh_globals Hfresh_globals 1938 2486 lapply Hfresh_function Hfresh_function 1939 lapply Htarget_type Htarget_type 1940 lapply kInv kInv 1941 lapply sInv sInv 2487 lapply Htarget_type Htarget_type 2488 lapply kInv kInv 2489 lapply sInv sInv 1942 2490 lapply fInv fInv 1943 lapply stmt_univ stmt_univ 2491 lapply stmt_univ stmt_univ 2492 lapply Htmpenv Htmpenv 1944 2493 lapply stmt_univ' stmt_univ' 1945 2494 lapply Hlabel_inclusion Hlabel_inclusion … … 1948 2497 [ (* Kstop continuation *) 1949 2498 (* simplifying the goal using outcome of the inversion *) 1950 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #k alloc_type#kstack #Hkstack2499 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kcm_m #kalloc_type #ktmpenv #kstack #Hkstack 1951 2500 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1952 2501 destruct (HA HB) 1953 2502 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 1954 2503 destruct (HC HD HE) 1955 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH 1956 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL 1957 destruct (HF HG HH HI HJ HK HL) #_ 2504 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI 2505 destruct (HF HG HH HI) 2506 @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM 2507 @(jmeq_absorb ?????) #HN 2508 destruct (HJ HK HL HM HN) #_ 1958 2509 (* reintroduce everything *) 1959 2510 #Hlabel_inclusion 1960 #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 1961 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf 2511 #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 2512 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved 2513 #Hreturn_ok #Hlabel_wf 1962 2514 #Hugly generalize in match (conj ????); #Hugly' 1963 2515 (* reduce statement translation function *) … … 1965 2517 (* In this simple case, trivial translation *) 1966 2518 destruct (Heq_translate) 1967 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec 2519 #Em #Htmp_vars_well_allocated 2520 #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below 1968 2521 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1969 2522 destruct (HA HB) … … 1979 2532 [ 2: #Habsurd destruct (Habsurd) ] 1980 2533 (* Use the memory injection stuff to produce a new memory injection *) 1981 cut (memory_inj Em (free_list cl_m (blocks_of_env kcl_env)) (free cm_m stackptr))1982 [ @(freelist_memory_inj_m1_m2 Em cl_m cm_m2534 cut (memory_inj Em (free_list cl_m (blocks_of_env kcl_env)) (free kcm_m stackptr)) 2535 [ @(freelist_memory_inj_m1_m2 Em cl_m kcm_m 1983 2536 (free_list cl_m (blocks_of_env kcl_env)) 1984 (free cm_m stackptr) Hinjection (blocks_of_env kcl_env) stackptr ? (refl ??) (refl ??))2537 (free kcm_m stackptr) Hinjection (blocks_of_env kcl_env) stackptr ? (refl ??) (refl ??)) 1985 2538 assumption ] 1986 2539 #Hinjection' 1987 @(CMR_return … Halloc_hyp Hcl_env_hyp … Hinjection') try assumption2540 @(CMR_return … Kend … Halloc_hyp Hcl_env_hyp … Hinjection') try assumption 1988 2541 [ 2: #b lapply (Hmatching b) 1989 2542 cases (lookup ?? kcl_env b) normalize nodelta … … 1997 2550 ] 1998 2551 ] 1999  1: (* TODO: lemma *) @cthulhu 2000 ] 2552  1: @(tmp_vars_well_allocated_conserved_by_frame_free … Hmatching … Htmp_vars_well_allocated) 2553  3: @ClCm_cont_stop @Hkstack 2554 ] 2001 2555  (* Kseq *) 2002 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #k cl_s #kcm_s2003 #kcl_env #kcm_env #kc l_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag2556 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #ktmpenv #kcl_s #kcm_s 2557 #kcl_env #kcm_env #kcm_m #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag 2004 2558 * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved 2005 #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kH cont_rel #_2559 #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHident_inclusion #kHcont_rel #_ 2006 2560 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2007 2561 destruct (HA HB) … … 2009 2563 destruct (HC HD HE) 2010 2564 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI 2011 @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL 2012 destruct (HF HG HH HI HJ HK HL) #_ 2565 destruct (HF HG HH HI) 2566 @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM 2567 @(jmeq_absorb ?????) #HN 2568 destruct (HJ HK HL HM HN) #_ 2013 2569 #Hlabel_inclusion 2014 #stmt_univ' # stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals2570 #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 2015 2571 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf 2016 2572 #Hugly generalize in match (conj ????); #Hugly' 2017 2573 (* In this simple case, trivial translation *) 2018 2574 #Heq_translate destruct (Heq_translate) #Em 2019 #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec 2575 #Htmp_vars_well_alloc 2576 #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below 2020 2577 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2021 2578 destruct (HA HB) … … 2025 2582 %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl 2026 2583 (* close simulation *) 2027 @(CMR_normal … kHeq_translate … Hinjection … Hmatching) try assumption 2028 (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *) 2029 @cthulhu 2030 (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *) 2584 @(CMR_normal … kHeq_translate … kHcont_rel … Hinjection … Hmatching) try assumption 2585 (* TODO Invariant on env_below_freshgen *) 2586 @cthulhu 2031 2587  (* Kwhile continuation *) 2032 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #k cl_env #kcm_env2588 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #ktmpenv #kcl_env #kcm_env #kcm_m 2033 2589 #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body 2034 2590 #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ'' 2035 2591 #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared 2036 #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kH find_label2592 #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHident_inclusion #kHfind_label 2037 2593 (* 2038 2594 * * * * #kHentry_declared * * * * … … 2046 2602 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH 2047 2603 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 2048 @(jmeq_absorb ?????) #HL 2049 destruct (HF HG HH HI HJ HK HL ) #_2604 @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM @(jmeq_absorb ?????) #HN 2605 destruct (HF HG HH HI HJ HK HL HM HN) #_ 2050 2606 #Hlabel_inclusion 2051 #stmt_univ' # stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals2607 #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 2052 2608 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf 2053 2609 #Hugly … … 2055 2611 (* In this simple case, trivial translation *) 2056 2612 #Heq_translate destruct (Heq_translate) 2057 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching 2058 #HEm_fn_id #Hframe_spec 2613 #Em #Htmp_vars_well_allocated 2614 #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching 2615 #HEm_fn_id #Hframe_spec #Henv_below 2059 2616 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2060 2617 destruct (HA HB) … … 2078 2635 @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHmklabels … kHeq_translate) 2079 2636 try assumption 2080 [ 1: @cthulhu 2081 (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *) 2082 (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *) 2637 [ 1: (* TODO: lemma on Henv_below. We need to thread freshgens through cont_rel. *) 2638 @cthulhu 2083 2639  2: cases Hmore_invariant * * #_ * * * * #_ #_ * #_ #_ * * #_ #H 2084 #_ #_ @H ] 2640 #_ #_ @H ] 2641  4,5: (* Continuations for Scall. TODO *) 2642 @cthulhu 2085 2643 ] 2086 2644  2: (* Assign *) … … 2092 2650 #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved 2093 2651 #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate 2094 #Hlabel_inclusion #Hcont_rel 2095 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec 2652 #Hlabel_inclusion #tmpenv #Htmpenv #Hcont_rel 2653 #Em #Htmp_vars_well_allocated 2654 #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below 2096 2655 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2097 2656 destruct (HA HB) … … 2113 2672 normalize nodelta 2114 2673 [ 1: (* Global *) #r 2115 #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq 2674 #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq 2116 2675 destruct (Hlhs_dest_eq) normalize nodelta 2117 2676 generalize in match (conj ????); #Hinvariant … … 2165 2724 whd @conj try @conj try @refl 2166 2725 [ 2: #Habsurd destruct (Habsurd) ] 2167 generalize in match (conj ????); 2168 #Hinv_vars 2726 generalize in match (conj ????); #Hinv_vars 2169 2727 @CMR_normal try assumption 2170 [ 2: @refl  1,3,4: ] 2171 [ 1: (* TODO: lemma on preservation of wellallocatedness through stores *) @cthulhu 2172  2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ] 2728 [ 2: @refl  *: ] 2729 [ 3: @(memory_matching_preserved_by_parallel_stores … Hmatching) 2730  2: @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated) 2731  1: @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel) ] 2173 2732  2: #b #Heq destruct (Heq) 2174 2733 lapply (opt_to_res_inversion ???? Hlookup_var_success) #Hlookup_aux … … 2192 2751 ] (refl ? (lookup ?? cl_env var_id))) 2193 2752 normalize nodelta 2194 [ (* Contradiction: a stackallocated variable was necessarily in the environment *)2753 [ (* Contradiction: a stackallocated variable was necessarily in the environment. TODO *) 2195 2754 @cthulhu 2196 2755  #Heq destruct (Heq) … … 2229 2788 whd in match (m_bind ?????); normalize nodelta 2230 2789 whd @conj try @conj try @refl 2231 [ 2: #Habsurd destruct (Habsurd) ] 2790 [ 2: #Habsurd destruct (Habsurd) ] 2232 2791 @(CMR_normal … Halloc_hyp) try assumption 2233 [ 2: @refl  1,3,4,5: ] 2234 [ 1: (* TODO: lemma on preservation of wellallocatedness through stores *) @cthulhu 2235  2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ] 2792 try @refl 2793 try @(memory_matching_preserved_by_parallel_stores … Hmatching) 2794 try @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated) 2795 @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel) 2236 2796 ] 2237 2797  3: (* Local *) 2238 #Hlookup_var_success whd in ⊢ ((???%) → ?); 2798 #Hlookup_var_success 2799 cases (type_eq_dec ??) normalize nodelta #Htype_eq_dec 2800 whd in ⊢ ((???%) → ?); 2239 2801 #Heq destruct (Heq) normalize nodelta Htranslate_statement 2240 2802 #Htranslate … … 2261 2823 normalize nodelta 2262 2824 [ (* Contradiction: a registerallocated variable was necessarily in the environment *) 2825 (* TODO, cf Hlookup_var_success or sInv *) 2263 2826 @cthulhu 2264 2827  #Heq destruct (Heq) … … 2281 2844 generalize in match (proj1 ???); #Hpresent 2282 2845 generalize in match (conj ????); #Hstmt_vars 2283 @(CMR_normal … Halloc_hyp) try assumption 2284 [ 2: @refl  *: ] 2285 [ (* Need a particular kind of continuation relation *) @cthulhu 2286  (* Lemma on preservation of wellallocatedness through update_present *) @cthulhu 2287  (* Memory injection when writing in clight only, and block not mapped *) @cthulhu 2288  (* Memory matching through env update *) @cthulhu ] 2846 @(CMR_normal … Halloc_hyp) try assumption try @refl 2847 [ 4: @(memory_matching_preserved_by_local_store … Hvalue_eq_rhs Hstore_value_of_type Hmatching) 2848  3: @(memory_inj_preserved_by_local_store … Hmatching Hinjection) 2849  2: @(tmp_vars_well_allocated_preserved_by_local_store … Hvalue_eq_rhs Hstore_value_of_type Htmp_vars_well_allocated) 2850  1: @(clight_cminor_cont_rel_parametric_in_cm_env … Hpresent Hcont_rel) ] 2289 2851 ] 2290 2852 ] … … 2345 2907 whd in match (m_bind ?????); normalize nodelta whd @conj try @conj try @refl 2346 2908 [ 2: #Habsurd destruct (Habsurd) ] 2347 @(CMR_normal … Halloc_hyp) try assumption 2348 [ 2: @refl  *: ]2349 [ 1: (* lemma on well_allocated after CL and CM parallel writes *) @cthulhu2350  2: (* memory matching *) @cthulhu]2909 @(CMR_normal … Halloc_hyp) try assumption try @refl 2910 [ 3: @(memory_matching_preserved_by_parallel_stores … Hmatching) 2911  2: @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated) 2912  1: @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel) ] 2351 2913 ] 2352 2914  4: (* Seq *) … … 2355 2917 (* introduce everything *) 2356 2918 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 2357 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 2919 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 2358 2920 #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved 2359 2921 #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate #Hlabel_inclusion 2360 #Hcont_rel 2361 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec 2922 #tmpenv #Htmpenv #Hcont_rel 2923 #Em #Htmp_vars_well_allocated 2924 #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below 2362 2925 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2363 2926 destruct (HA HB) … … 2376 2939 @transitive_lset_inclusion @lset_inclusion_union %1 2377 2940 @reflexive_lset_inclusion 2378  2: @(ClCm_cont_seq … Htrans_stm2) 2941  2: lapply (translation_entails_ident_inclusion … Htrans_stm2) #H 2942 @(transitive_lset_inclusion … (translation_entails_ident_inclusion … Htrans_stm2)) 2943 assumption 2944  3: @(ClCm_cont_seq … Htrans_stm2) 2379 2945 [ 1: lapply Hlabel_inclusion @transitive_lset_inclusion @lset_inclusion_union %2 2380 2946 @reflexive_lset_inclusion 2381  2: assumption ] 2382  3: @cthulhu ] 2383  *: @cthulhu ] 2947  2: assumption 2948  3: assumption ] 2949 ] 2950  *: (* Other statements *) @cthulhu ] 2384 2951  2: (* Return state *) 2385 #cl_ge #cm_ge #INV' #cl_ f #cm_f #alloc_type2386 #cl_env #cl_m #cm_env #c _m #cm_st #stackptr #stacksize2387 #stmt_univ # Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe2952 #cl_ge #cm_ge #INV' #cl_k #cm_k #cm_st #cl_f #cm_f #alloc_type 2953 #cl_env #cl_m #cm_env #cm_mt #stackptr #stacksize 2954 #stmt_univ #tmpenv #Htmpenv #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe #Hcont 2388 2955 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2389 2956 destruct (HA HB) … … 2393 2960 whd in Hclight_normal:%; 2394 2961 @False_ind @Hclight_normal 2395  3: (* Call state, nostore *) 2396 #cl_ge #cm_ge #cl_f #cm_f #INV' #alloc_types 2397 #cl_env #cl_m #cm_env #cm_m #stackptr #u #cl_fundef #cm_fundef 2398 #Hglobals_fresh #Hfundef_fresh #rettyp #Hrettyp #cl_k #cm_k #fblock 2399 #Hcont_rel #cl_fun_id #cm_fun_id #Hfun_id_eq #cl_retval #cm_retval 2400 #sInv #fInv #kInv #cl_argvals #cm_argvals #cm_stack 2962  3: (* Call state *) 2963 #cl_ge #cm_ge #INV' #cl_k #cm_k #cm_st #cl_f #cm_f #cl_fundef #cm_fundef 2964 #fblock #target_type #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize 2965 #func_univ #Hgobals_fresh #Hfundef_fresh #Htranslate_function #Hfind_cl #Hfind_cm 2966 #cl_id #cm_id #stmt_univ #tmpenv #Htmpenv #Hcont_rel 2967 #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe 2968 #cl_args_values #cm_args_values #Hall2 2401 2969 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2402 2970 destruct (HA HB) 2403 2971 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 2404 destruct (HC HD HE) 2972 destruct (HC HD HE) #_ 2405 2973 whd in Hclight_normal:%; 2406 2974 @False_ind @Hclight_normal 2407  4: (* Call state, store *) 2408 #cl_ge #cm_ge #cl_f #cm_f #INV' #alloc_types 2409 #cl_env #cl_m #cm_env #cm_m #cm_stack #stackptr #u #cl_fundef #cm_fundef 2410 #Hglobals_fresh #Hfundef_fresh #rettyp #Hrettyp #cl_k #cm_k #fblock 2411 #Hcont_rel #cl_fun_id #cm_fun_id #Hfun_id_eq 2412 #cl_rettyp #cl_retval #cl_retrace #cm_retval #cl_lhs #cm_lhs 2413 #Hinvariant_on_cm_lhs #Hexec_lvalue #Htranslate_dest #cm_ret_var 2414 #sInv #fInv #kInv #cl_argvals #cm_argvals #cm_stack 2415 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2416 destruct (HA HB) 2417 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 2418 destruct (HC HD HE) 2419 whd in Hclight_normal:%; 2420 @False_ind @Hclight_normal 2421  5: (* Intermediary While state *) 2975  4: (* Intermediary While state *) 2422 2976 (*  *) 2423 2977 #cl_ge #cm_ge #INV' … … 2426 2980 #cm_stack #rettyp #kInv #fInv #sInv #Heq_ty #Hrettyp_eq #func_univ #Hfresh_globals #Hfresh_function 2427 2981 #Htranslate_function #Hcont_rel 2428 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' # lbls2429 #Em #Htmp_vars_well_allocated #Halloc_hyp2430 #Hc l_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hexpr_vars #Htranslate_expr2431 #He ntry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement2982 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #tmpenv #Htmpenv #Hcont_rel 2983 #Em #Htmp_vars_well_allocated 2984 #Hcharacterise #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below 2985 #Hexpr_vars #Htranslate_expr #Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement 2432 2986 #Hlabel_inclusion #Hlabel_exists #Hinv1 #Hinv2 #Hfind_label 2433 2987 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB … … 2449 3003 generalize in match (proj1 ???); #Hpresent_ifthenelse 2450 3004 (* Exhibit simulation of condition evaluation *) 2451 lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_ 3005 lapply (eval_expr_sim … Hcharacterise … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_ 3006 (* The type of Hsim forces us to wrap cm_cond into a dummy cast. *) 2452 3007 lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?)) 2453 [ >Heq_ty @refl ] Hsim #Hsim 2454 lapply (Hsim … Hexpr_vars … Htranslate_expr ??? Hcl_exec_cond) 2455 [ lapply Hpresent_ifthenelse whd in ⊢ (% → ?); <Heq_ty >CMcast_identity #H @H ] 3008 [ >Heq_ty @refl ] Hsim 3009 whd in match (typeof ?); #Hsim 3010 lapply (Hsim ??????) 3011 [ 2: <Heq_ty >CMcast_identity assumption 3012  1: assumption 3013  6: <Heq_ty >CMcast_identity assumption 3014  5: lapply Htranslate_expr lapply Hexpr_vars lapply cm_cond cm_cond 3015 >Heq_ty #cm_cond #Hexpr_vars @(jmeq_absorb ?????) #Hsol @Hsol 3016  *: ] 2456 3017 * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq Hsim 2457 3018 cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉) … … 2476 3037 generalize in match (proj1 ???); #Hpresent_ifthenelse 2477 3038 (* Exhibit simulation of condition evaluation *) 2478 lapply (eval_expr_sim … H alloc_hyp… Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_3039 lapply (eval_expr_sim … Hcharacterise … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_ 2479 3040 lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?)) 2480 [ >Heq_ty @refl ] Hsim #Hsim 2481 lapply (Hsim … Hexpr_vars … Htranslate_expr ??? Hcl_exec_cond) 2482 [ lapply Hpresent_ifthenelse whd in ⊢ (% → ?); <Heq_ty >CMcast_identity #H @H ] 3041 [ >Heq_ty @refl ] Hsim 3042 whd in match (typeof ?); #Hsim 3043 lapply (Hsim ??????) 3044 [ 2: <Heq_ty >CMcast_identity assumption 3045  1: assumption 3046  6: <Heq_ty >CMcast_identity assumption 3047  5: lapply Htranslate_expr lapply Hexpr_vars lapply cm_cond cm_cond 3048 >Heq_ty #cm_cond #Hexpr_vars @(jmeq_absorb ?????) #Hsol @Hsol 3049  *: ] 2483 3050 * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq Hsim 2484 3051 cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉) … … 2496 3063 whd @conj try @conj 2497 3064 [ 3: #Habsurd destruct (Habsurd) 2498  1: normalize >append_nil >append_nil @refl 3065  1: normalize >append_nil >append_nil @refl 2499 3066  2: @(CMR_normal … DoNotConvert) try assumption 2500 [ 2: @refl  ] 3067 try @refl 3068 @(env_below_freshgen_preserved_by_translation … Htranslate_statement) 3069 assumption 2501 3070 ] 2502 3071 ] … … 2505 3074 2506 3075 2507 lemma clight_cminor_call_return : 2508 ∀g1, g2. 2509 ∀INV:clight_cminor_inv g1 g2. 2510 ∀s1,s1'. 2511 clight_cminor_rel g1 g2 INV s1 s1' → 2512 match Clight_classify s1 with 2513 [ cl_call ⇒ true 2514  cl_return ⇒ true 2515  _ ⇒ false ] → 2516 ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 → 2517 ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'. 2518 tr = tr' ∧ 2519 clight_cminor_rel g1 g2 INV s2 s2' ∧ 2520 (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1)) 2521 ). 2522 #g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class 2523 inversion Hstate_rel 2524 [ 1: (* normal *) 2525 #cl_ge #cm_ge #INV' #cl_s 2526 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 2527 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize 2528 (* introduce everything *) 2529 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 2530 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 2531 #flag #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC 2532 #HE #HF #HG #HI #HJ #HK 2533 @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2 2534 destruct (H1 H2) 2535 @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5 2536 destruct (H3 H4 H5) 2537 @False_ind @Hclight_class 2538  5: 2539 #cl_ge #cm_ge #INV' #cl_s 2540 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 2541 #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab 2542 #cm_cond #cm_body #cm_stack #rettyp' #kInv 2543 (* introduce everything *) 2544 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 2545 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 2546 #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr 2547 #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl 2548 #Hlabdecl #Hinv1 #Hinv2 #Hfindlab 2549 @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2 2550 destruct (H1 H2) 2551 @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5 2552 destruct (H3 H4 H5) 2553 @False_ind @Hclight_class 2554  *: @cthulhu 2555 ] qed. 3076 2556 3077 2557 3078 … … 2574 3095 make_initial_state ?? clight_fullexec cl_program = OK ? s → 2575 3096 make_initial_state ?? Cminor_fullexec cm_program = OK ? s' → 2576 ∃INV. clight_cminor_rel INV s s'. *)3097 ∃INV. clight_cminor_rel INV s
Note: See TracChangeset
for help on using the changeset viewer.