Changeset 2545


Ignore:
Timestamp:
Dec 7, 2012, 6:39:15 PM (7 years ago)
Author:
garnier
Message:

Comitting current progress of CL to CM

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2527 r2545  
    422422
    423423lemma 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.
    425425  (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
    426426  characterise_vars globals f =〈vars,stacksize〉 →
    427427  lookup ?? env' var_id = None ? →       
    428   lookup' vars var_id = OK ? 〈allocty, ty〉 →
     428  ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
    429429  ∃r.allocty = Global r.
    430 #env #env' #f #vars #stacksize #globals #var_id #allocty #ty #Hexec_alloc
    431 #Hcharacterise #Hlookup_fail #Hlookup_type_ok
     430#env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
     431#Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
    432432lapply (characterise_vars_src … Hcharacterise var_id ?)
    433433[ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
     
    471471qed.
    472472
     473(* TODO convert Clight unary ops to front-end ops ops, then prove correspondence for operators (with equal values). *)
     474
    473475
    474476lemma eval_expr_sim :
     
    486488  ∀E:embedding.
    487489  ∀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 *)
    489492  (∀(e:expr).
    490    ∀(e':CMexpr (typ_of_type (typeof e))). 
     493   ∀(e':CMexpr (typ_of_type (typeof e))).
    491494   ∀Hexpr_vars.
    492495   translate_expr vars e = OK ? («e', Hexpr_vars») →
     
    495498   ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
    496499            value_eq E cl_val cm_val) ∧
     500   (* clight /lvalue/ to cminor /expr/ *)
    497501  (∀ed,ty.
    498    ∀(e':CMexpr (typ_of_type ty)).
     502   ∀(e':CMexpr ASTptr).
    499503   ∀Hexpr_vars.
    500    translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
     504   translate_addr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
    501505   ∀cl_blo,cl_off,trace,Hyp_present.
    502506   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
    517510@expr_lvalue_ind_combined
    518511[ 1: (* Integer constant *)
    519512  #csz #ty cases ty
    520513  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    521   | #structname #fieldspec | #unionname #fieldspec | #id ] 
     514  | #structname #fieldspec | #unionname #fieldspec | #id ]
    522515  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
    523516  #val #trace #Hpresent #Hexec_cl
     
    564557            * #var_id_alloctype * #var_id_type * #Heq
    565558            cases (variable_not_in_env_but_in_vartypes_is_global …
    566                         Hexec_alloc Hcharacterise Hcl_lookup Heq)
     559                        Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
    567560            #r #Heq' destruct (Heq') normalize nodelta
    568561            lapply Hcl_load_success -Hcl_load_success
     
    699692                 (* seems ok *)
    700693            ]
    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
    713704       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
    721718       #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
    732725       lapply Hyp_present -Hyp_present
    733        lapply Htranslate_expr -Htranslate_expr
    734726       lapply Hexpr_vars -Hexpr_vars
    735727       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 ]
    756746  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
    757747       lapply (refl ? (typeof e1))
    758748       cases (typeof e1) in ⊢ ((???%) → %);
    759        [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    760        | #structname #fieldspec | #unionname #fieldspec | #id ]
     749       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
     750       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta
    761751       #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  ]
    860862| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
    861863     whd in Hexec_lvalue_var:(??%?);
    862864     (* 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;
    864868     normalize nodelta
    865869     [ 1: (* global *)
    866           #Hexec_opt
     870          #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
    867871          cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
    868872          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
    873886     | 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
    876978| *: @cthulhu
    877979] qed.
     980
     981
    878982
    879983
Note: See TracChangeset for help on using the changeset viewer.