Changeset 2545
- Timestamp:
- Dec 7, 2012, 6:39:15 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/toCminorCorrectness.ma
r2527 r2545 422 422 423 423 lemma variable_not_in_env_but_in_vartypes_is_global : 424 ∀env,env',f,vars,stacksize,globals,var_id ,allocty,ty.424 ∀env,env',f,vars,stacksize,globals,var_id. 425 425 (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) → 426 426 characterise_vars globals f =〈vars,stacksize〉 → 427 427 lookup ?? env' var_id = None ? → 428 lookup' vars var_id = OK ? 〈allocty, ty〉 →428 ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 → 429 429 ∃r.allocty = Global r. 430 #env #env' #f #vars #stacksize #globals #var_id #allocty #ty#Hexec_alloc431 #Hcharacterise #Hlookup_fail # Hlookup_type_ok430 #env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc 431 #Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok 432 432 lapply (characterise_vars_src … Hcharacterise var_id ?) 433 433 [ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t * … … 471 471 qed. 472 472 473 (* TODO convert Clight unary ops to front-end ops ops, then prove correspondence for operators (with equal values). *) 474 473 475 474 476 lemma eval_expr_sim : … … 486 488 ∀E:embedding. 487 489 ∀minj:memory_inj E cl_m cm_m. 488 memory_matching E cl_m cm_m cl_env cm_env inv sp vars → 490 memory_matching E cl_m cm_m cl_env cm_env inv sp vars → 491 (* clight expr to cminor expr *) 489 492 (∀(e:expr). 490 ∀(e':CMexpr (typ_of_type (typeof e))). 493 ∀(e':CMexpr (typ_of_type (typeof e))). 491 494 ∀Hexpr_vars. 492 495 translate_expr vars e = OK ? («e', Hexpr_vars») → … … 495 498 ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧ 496 499 value_eq E cl_val cm_val) ∧ 500 (* clight /lvalue/ to cminor /expr/ *) 497 501 (∀ed,ty. 498 ∀(e':CMexpr (typ_of_type ty)).502 ∀(e':CMexpr ASTptr). 499 503 ∀Hexpr_vars. 500 translate_ expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →504 translate_addr vars (Expr ed ty) = OK ? («e', Hexpr_vars») → 501 505 ∀cl_blo,cl_off,trace,Hyp_present. 502 506 exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 → 503 match E cl_blo with 504 [ Some loc ⇒ 505 let 〈cm_blo, delta〉 ≝ loc in 506 match access_mode ty with 507 [ By_value t ⇒ 508 (∃cm_val. loadv t cm_m (Vptr (mk_pointer cm_blo (offset_plus cl_off delta))) = Some ? cm_val ∧ 509 eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉) 510 | By_reference ⇒ 511 eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m 512 = OK ? 〈trace, Vptr (mk_pointer cm_blo (offset_plus cl_off delta))〉 513 | By_nothing _ ⇒ True ] 514 | None ⇒ False ]). 515 #inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env 516 #sp #cm_m #E #Hinj #Hlocal_matching 507 ∃cm_val. eval_expr (ge_cm inv) ASTptr e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧ 508 value_eq E (Vptr (mk_pointer cl_blo cl_off)) cm_val). 509 #inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env #sp #cm_m #E #Hinj #Hlocal_matching 517 510 @expr_lvalue_ind_combined 518 511 [ 1: (* Integer constant *) 519 512 #csz #ty cases ty 520 513 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 521 | #structname #fieldspec | #unionname #fieldspec | #id ] 514 | #structname #fieldspec | #unionname #fieldspec | #id ] 522 515 #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate 523 516 #val #trace #Hpresent #Hexec_cl … … 564 557 * #var_id_alloctype * #var_id_type * #Heq 565 558 cases (variable_not_in_env_but_in_vartypes_is_global … 566 Hexec_alloc Hcharacterise Hcl_lookup Heq)559 Hexec_alloc Hcharacterise Hcl_lookup ?? Heq) 567 560 #r #Heq' destruct (Heq') normalize nodelta 568 561 lapply Hcl_load_success -Hcl_load_success … … 699 692 (* seems ok *) 700 693 ] 701 ] 702 | 2: whd in match (typeof ?) in Hind; 703 lapply (Hind cm_expr Hexpr_vars Htranslate_expr cl_b cl_o cl_t Hyp_present) -Hind 704 cases (bind_inversion ????? Hcl_success) -Hcl_success * #cl_subexpr_val #cl_trace * 705 #Hexec_expr 706 @(match cl_subexpr_val 707 return λx. cl_subexpr_val = x → ? 708 with 709 [ Vundef ⇒ λHval_eq. ? 710 | Vint sz' i ⇒ λHval_eq. ? 711 | Vnull ⇒ λHval_eq. ? 712 | Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta 694 ] 695 | 2: lapply Hcl_success -Hcl_success 696 lapply Htranslate_expr -Htranslate_expr 697 lapply Hind -Hind cases ty1 698 [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1 699 | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] 700 #Hind #Htranslate_expr #Hexec_cl 701 cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr 702 * whd in match (typ_of_type ?); normalize nodelta 703 #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind 713 704 whd in ⊢ ((???%) → ?); 714 [ 1,2,3: #Habsurd destruct ] #Heq destruct (Heq) destruct (Hptr_eq) 715 whd in match (exec_lvalue' ?????) in Hind; #Hind 716 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val 717 * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 718 lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hload_success 719 whd in Hexec_expr:(???%); whd in match (exec_lvalue' ?????) in Hind; 720 lapply Hind -Hind >Hexec_expr normalize nodelta 705 [ 1,2,6,7: #Heq destruct (Heq) ] 706 lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind 707 whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta 708 #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind 709 [ 1,3,5,7: @cthulhu ] 710 whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta 711 cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 * 712 #Hexec_cl_ind #Hcl_ptr 713 cut (∃ptr. cl_ptr = Vptr ptr) 714 [ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize 715 #H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ] 716 * * #cl_ptr_block #cl_ptr_off -Hcl_ptr 717 #Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl 721 718 #Hind lapply (Hind (refl ??)) -Hind 722 @(match E (pblock p) 723 return λx. (E (pblock p) = x) → ? 724 with 725 [ None ⇒ λHembed. ? 726 | Some loc ⇒ λHembed. ? ] (refl ? (E (pblock p)))) 727 normalize nodelta 728 [ 1: @False_ind ] 729 cases loc in Hembed; normalize nodelta 730 lapply Hload_success -Hload_success 731 lapply Hexec_expr -Hexec_expr 719 * #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind 720 lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr 721 destruct (Hcm_ptr) #Hpointer_translation 722 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res 723 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res) 724 -Hopt_to_res 732 725 lapply Hyp_present -Hyp_present 733 lapply Htranslate_expr -Htranslate_expr734 726 lapply Hexpr_vars -Hexpr_vars 735 727 lapply cm_expr -cm_expr 736 cases ty 737 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 738 | #structname #fieldspec | #unionname #fieldspec | #id ] 739 normalize nodelta 740 #cm_expr #Hexpr_vars #Htranslate_expr #Hyp_present #Hexec_expr 741 #Hload_success #BL #OFF #Hembed 742 [ 1,6,7: normalize in Hload_success; #_ destruct 743 | 4,5: whd in match (typ_of_type ?); #Heval >Heval 744 %{(Vptr (mk_pointer BL (offset_plus (poff p) OFF)))} 745 @conj try @refl 746 lapply (load_value_of_type_by_ref … Hload_success ??) try // 747 #Heq >Heq %4 whd in ⊢ (??%%); >Hembed @refl 748 | *: * #cm_val * #Hloadv #Heval_expr >Heval_expr 749 lapply (mi_inj … Hinj … (pblock p) (poff p) BL (offset_plus (poff p) OFF) … Hload_success) 750 [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl 751 | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ] 752 * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq' 753 %{cm_val'} @conj try assumption 754 whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success'; 755 #Heq destruct @refl ] 728 inversion (access_mode ty) 729 [ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode 730 lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp) 731 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta 732 #Heq destruct (Heq) 733 [ 1,2,3,4: (* By_value *) 734 (* project Hcl_load_success in Cminor through memory_inj *) 735 lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success) 736 [ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ] 737 * #cm_val * #Hcm_load_success #Hvalue_eq 738 lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success) 739 #Hloadv_cm 740 whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta 741 >Hloadv_cm normalize %{cm_val} @conj try @refl assumption 742 | *: (* By reference *) 743 >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl 744 lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode) 745 #Hval >Hval %4 assumption ] 756 746 | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success 757 747 lapply (refl ? (typeof e1)) 758 748 cases (typeof e1) in ⊢ ((???%) → %); 759 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain760 | #structname #fieldspec | #unionname #fieldspec | #id ]749 [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1 750 | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta 761 751 #Heq_typeof normalize nodelta 762 [ 1,2,3,4,5,8: #Habsurd destruct ] 763 #Hexec_compound_clight 764 lapply (Hind … Htranslate_expr) -Hind -Htranslate_expr 765 cases (bind_inversion ????? Hexec_compound_clight) -Hexec_compound_clight 766 * * #CLB #CLO #CLTR 767 * #Hexec_lvalue #Hfield_offset whd in match (exec_lvalue' ?????); 768 >Hexec_lvalue normalize nodelta >Heq_typeof normalize nodelta 769 whd in match (m_bind ?????); 770 [ 2: normalize in Hfield_offset; destruct (Hfield_offset) 771 #Hind lapply (Hind ??? Hyp_present (refl ??)) -Hind 772 @(match E cl_b 773 return λx. (E cl_b = x) → ? 774 with 775 [ None ⇒ λHembed. ? 776 | Some loc ⇒ λHembed. ? ] (refl ? (E cl_b))) normalize nodelta 777 [ 1: @False_ind ] cases loc in Hembed; #BLO #OFF #Hembed normalize nodelta 778 lapply Hyp_present -Hyp_present 779 lapply Hexpr_vars -Hexpr_vars 780 lapply cm_expr -cm_expr 781 cases ty normalize nodelta 782 [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' 783 | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ] 784 #cm_expr #Hexpr_vars #Hyp_present 785 [ 1,6,7: #_ #Hload_void cases (bind_inversion ????? Hload_void) 786 #val * #Hopt_to_res #Hok lapply (opt_to_res_inversion ???? Hopt_to_res) 787 normalize in ⊢ (% → ?); #Habsurd destruct 788 | 4,5: whd in match (typ_of_type ?); #Heval >Heval 789 #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) 790 #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); 791 lapply (opt_to_res_inversion ???? Hopt_to_res) 792 #Hload_success #Heq destruct (Heq) 793 lapply (load_value_of_type_by_ref … Hload_success ??) try // 794 #Hval_eq >Hval_eq 795 %{(Vptr (mk_pointer BLO (offset_plus cl_o OFF)))} 796 @conj try @refl 797 %4 whd in ⊢ (??%%); >Hembed @refl 798 | 2,3,8: * #cm_val * #Hloadv #Heval_expr >Heval_expr 799 #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) 800 #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 801 lapply (opt_to_res_inversion ???? Hopt_to_res) 802 #Hload_success 803 lapply (mi_inj … Hinj … cl_b cl_o BLO (offset_plus cl_o OFF) … Hload_success) 804 [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl 805 | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ] 806 * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq' 807 %{cm_val'} @conj try assumption 808 whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success'; 809 #Heq destruct (Heq) @refl ] 810 | 1: cases (bind_inversion ????? Hfield_offset) -Hfield_offset #field_offset * #Hfield_offset_eq 811 #Heq whd in Heq:(???%); destruct (Heq) >Hfield_offset_eq normalize nodelta 812 #Hind lapply (Hind ??? Hyp_present (refl ??)) -Hind 813 @(match E cl_b 814 return λx. (E cl_b = x) → ? 815 with 816 [ None ⇒ λHembed. ? 817 | Some loc ⇒ λHembed. ? ] (refl ? (E cl_b))) 818 normalize nodelta 819 [ 1: @False_ind ] cases loc in Hembed; #BLO #OFF #Hembed normalize nodelta 820 lapply Hyp_present -Hyp_present 821 lapply Hexpr_vars -Hexpr_vars 822 lapply cm_expr -cm_expr 823 cases ty normalize nodelta 824 [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' 825 | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ] 826 #cm_expr #Hexpr_vars #Hyp_present 827 [ 1,6,7: #_ #Hload_void cases (bind_inversion ????? Hload_void) 828 #val * #Hopt_to_res #Hok lapply (opt_to_res_inversion ???? Hopt_to_res) 829 normalize in ⊢ (% → ?); #Habsurd destruct 830 | 4,5: whd in match (typ_of_type ?); #Heval >Heval 831 #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) -Hload_success_hyp 832 #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); 833 lapply (opt_to_res_inversion ???? Hopt_to_res) 834 #Hload_success #Heq destruct (Heq) 835 lapply (load_value_of_type_by_ref … Hload_success ??) try // 836 #Hval_eq >Hval_eq 837 %{(Vptr (mk_pointer BLO (offset_plus (shift_offset (bitsize_of_intsize I32) CLO (repr I32 field_offset)) OFF)))} 838 @conj try @refl 839 %4 whd in ⊢ (??%%); >Hembed @refl 840 | 2,3,8: * #cm_val * #Hloadv #Heval_expr >Heval_expr 841 #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) 842 #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 843 lapply (opt_to_res_inversion ???? Hopt_to_res) 844 #Hload_success 845 lapply (mi_inj ??? Hinj 846 cl_b 847 (mk_offset 848 (addition_n offset_size (offv CLO) 849 (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 field_offset)))) 850 BLO (offset_plus (mk_offset 851 (addition_n offset_size (offv CLO) 852 (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 field_offset)))) OFF) ? val ?? Hload_success) 853 [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl 854 | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ] 855 * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq' 856 %{cm_val'} @conj try assumption 857 whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success'; 858 #Heq destruct (Heq) @refl ] 859 ] ] 752 [ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success 753 whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr; 754 normalize nodelta #Htranslate_expr 755 cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr 756 * whd in match (typ_of_type ?); normalize nodelta 757 #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2 758 [ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2 759 #cm_field_off * #Hcm_field_off 760 | lapply Htranslate_expr2 -Htranslate_expr2 ] 761 cases (bind_inversion ????? Hexec_cl) -Hexec_cl 762 * * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl 763 whd in Hexec_lvalue:(???%); 764 [ cases (bind_inversion ????? Hexec_cl) -Hexec_cl 765 #cl_field_off * #Hcl_field_off #Hoffset_eq ] 766 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success 767 #cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 768 lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value 769 [ (* Struct case *) 770 lapply Hcl_load_value -Hcl_load_value 771 lapply Hyp_present -Hyp_present 772 lapply Hexpr_vars -Hexpr_vars 773 lapply cm_expr -cm_expr 774 lapply Hind -Hind 775 cases ty 776 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 777 | #structname #fieldspec | #unionname #fieldspec | #id ] 778 #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value 779 normalize nodelta 780 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 781 whd in match (eval_expr ???????); 782 (* applying the arguments of the induction hypothesis progressively *) 783 lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddp I16) cm_expr_ind 784 (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?) 785 [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind 786 lapply (Hind ?) 787 [ 1,3,5,7,9: 788 whd in ⊢ (??%?); >Heq_typeof normalize nodelta 789 >Htranslate_expr_ind whd in match (m_bind ?????); 790 >Hcm_field_off normalize nodelta @refl ] -Hind #Hind 791 whd in Hoffset_eq:(???%); destruct (offset_eq) 792 cut (cl_field_off = cm_field_off) 793 [ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off 794 normalize #Heq destruct (Heq) @refl ] 795 #Heq destruct (Heq) 796 lapply (Hind cl_b cl_o trace ?) 797 [ 1,3,5,7,9: @Hyp_present ] -Hind #Hind 798 lapply (Hind ?) -Hind 799 [ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta 800 >Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta 801 @Hoffset_eq ] 802 * #cm_val' * #Heval_expr #Hvalue_eq 803 lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off 804 * #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans 805 [ 1,2,5: (* by-value *) 806 lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value) 807 [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ] 808 * #cm_val * #Hcm_load_value #Hvalue_eq 809 lapply (load_value_of_type_by_value … Hcm_load_value) 810 [ 1,3,5: @refl ] 811 #Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj 812 try @refl try assumption 813 | 3,4: (* by-ref *) 814 whd in match (eval_expr ???????) in Heval_expr; >Heval_expr 815 %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl 816 whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption 817 ] 818 | (* union case *) 819 lapply Hcl_load_value -Hcl_load_value 820 lapply Hyp_present -Hyp_present 821 lapply Hexpr_vars -Hexpr_vars 822 lapply cm_expr -cm_expr 823 lapply Hind -Hind 824 cases ty 825 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 826 | #structname #fieldspec | #unionname #fieldspec | #id ] 827 whd in match (typ_of_type ?); normalize nodelta 828 #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value 829 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 830 [ 1,2,5: (* by-value *) 831 whd in match (eval_expr ???????); 832 lapply (Hind cm_expr_ind Hexpr_vars ?) 833 [ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ] 834 whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta 835 -Hind #Hind 836 lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta 837 whd in match (m_bind ?????); #Hind 838 cases (Hind (refl ??)) -Hind 839 #cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta 840 cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans 841 destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl) 842 lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value) 843 [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ] 844 * #cm_val * #Hcm_load_value #Hvalue_eq 845 lapply (load_value_of_type_by_value … Hcm_load_value) 846 [ 1,3,5: @refl ] 847 #Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj 848 try @refl assumption 849 | 3,4: 850 whd in Hexec_cl:(???%); destruct (Hexec_cl) 851 lapply (Hind cm_expr Hexpr_vars) 852 whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind 853 lapply (Hind Htranslate_expr_ind) -Hind 854 whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta 855 >Hexec_lvalue whd in match (m_bind ?????); 856 #Hind cases (Hind … Hyp_present (refl ??)) 857 #cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj 858 try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) 859 assumption ] 860 ] 861 ] 860 862 | 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var 861 863 whd in Hexec_lvalue_var:(??%?); 862 864 (* check whether var is local or global *) 863 lapply (Hlocal_matching var) cases (lookup ?? cl_env var) in Hexec_lvalue_var; 865 lapply (Hlocal_matching var) 866 lapply (variable_not_in_env_but_in_vartypes_is_global … var Hexec_alloc … Hcharacterise) 867 cases (lookup ?? cl_env var) in Hexec_lvalue_var; 864 868 normalize nodelta 865 869 [ 1: (* global *) 866 #Hexec_opt 870 #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global 867 871 cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq 868 872 whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq) 869 >(opt_to_res_inversion ???? Hopt_to_res) normalize nodelta 870 #Hembed >Hembed normalize nodelta 871 (* Standard stuff. *) 872 @cthulhu 873 lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta 874 #Hembed 875 cases (bind_inversion ????? Htranslate_var) -Htranslate_var 876 * #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype 877 cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype; 878 normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 879 whd in match (eval_expr ???????); 880 whd in match (eval_constant ????); 881 <(eq_sym inv var) >Hfind_symbol normalize nodelta 882 %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))} 883 @conj try @refl %4 whd in match (pointer_translation ??); 884 >Hembed normalize nodelta whd in match (shift_offset ???); 885 >addition_n_0 @refl 873 886 | 2: (* local *) 874 @cthulhu 875 ] 887 #BL #Heq destruct (Heq) #_ 888 @(match (lookup ?? vars var) 889 return λx. (lookup ?? vars var = x) → ? 890 with 891 [ None ⇒ ? 892 | Some kind ⇒ ? 893 ] (refl ??)) 894 normalize nodelta 895 #Hlookup [ @False_ind ] 896 cases kind in Hlookup; #var_alloctype #var_type normalize nodelta 897 #Hlookup 898 lapply (refl ? var_alloctype) 899 cases var_alloctype in ⊢ ((???%) → %); normalize nodelta 900 [ #reg #Heq @False_ind | #stacksize #Hvar_alloc #Hembed | #Hvar_alloc #Hlookup' ] 901 [ (* stack alloc*) 902 cases (bind_inversion ????? Htranslate_var) -Htranslate_var 903 * #var_alloctype' #var_type' * #Hlookup_vartype' 904 whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta 905 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta 906 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????); 907 %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))} 908 @conj try @refl %4 whd in match (pointer_translation ??); 909 >Hembed @refl 910 | (* local alloc *) 911 cases (bind_inversion ????? Htranslate_var) -Htranslate_var 912 * #var_alloctype' #var_type' * #Hlookup_vartype' 913 whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta 914 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta 915 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ] 916 (*| 4: #e #ty*) 917 | 4: 918 * #ed #ety cases ety 919 [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1 920 | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta 921 whd in match (typeof ?); 922 #ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue 923 cases (bind_inversion ????? Htranslate) -Htranslate 924 * #cm_expr #Hexpr_vars_cm * #Htranslate_ind 925 cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue 926 * #cl_val #trace0 * #Hexec_expr #Hcl_val 927 whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta 928 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 929 cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0) 930 [ 1,3,5,7: cases cl_val in Hcl_val; normalize 931 [ 1,5,9,13: #Heq destruct (Heq) 932 | 2,6,10,14: #sz #vec #Heq destruct (Heq) 933 | 3,7,11,15: #Heq destruct (Heq) 934 | 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ] 935 * #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq) 936 cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr) 937 #cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm 938 %{cm_val} @conj try @refl try assumption 939 | 5: 940 #ty cases ty 941 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 942 | #structname #fieldspec | #unionname #fieldspec | #id ] 943 #ed #ty' #Hind 944 whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr 945 #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr 946 cases (bind_inversion ????? Htranslate) -Htranslate 947 * #cm_expr #Hexpr_vars_cm * #Htranslate_ind 948 cases (bind_inversion ????? Hexec_expr) -Hexec_expr 949 * * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta 950 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 951 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 952 cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue) 953 #cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm 954 %{cm_val} @conj try @refl assumption 955 | 6: 956 #ty cases ty 957 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 958 | #structname #fieldspec | #unionname #fieldspec | #id ] 959 whd in match (typeof ?); 960 #op #e #Hind 961 whd in match (typeof ?); whd in match (typ_of_type ?); 962 #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec 963 cases (bind_inversion ????? Htranslate) -Htranslate 964 #op * #Htranslate_unop #Hexec_arg 965 cases (bind_inversion ????? Hexec_arg) -Hexec_arg 966 * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 967 cases (bind_inversion ????? Hexec) -Hexec 968 * #cl_val #cl_trace * #Hexec_cl 969 whd in ⊢ ((???%) → ?); #Hexec_unop 970 cases (bind_inversion ????? Hexec_unop) -Hexec_unop 971 #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 972 lapply (opt_to_res_inversion ???? Hopt) -Hopt 973 #Hsem_cl whd in match (eval_expr ???????); 974 cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl) 975 #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta 976 lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl) 977 @cthulhu 876 978 | *: @cthulhu 877 979 ] qed. 980 981 878 982 879 983
Note: See TracChangeset
for help on using the changeset viewer.