Changeset 3155


Ignore:
Timestamp:
Apr 17, 2013, 3:24:13 PM (4 years ago)
Author:
campbell
Message:

Now have proof that the initial states are in simulation for clight to
cminor.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r3055 r3155  
    448448  ∀cl_ge, cm_ge.
    449449  ∀INV:  clight_cminor_inv cl_ge cm_ge.     (* stuff on global variables and functions (matching between CL and CM) *)
    450   ∀cl_f: function.                          (* current Clight function *)
    451   internal_function →                       (* current Cminor function *)
     450  ∀cl_fd: clight_fundef.                    (* current Clight function *)
     451  fundef internal_function →                (* current Cminor function *)
    452452  cl_env →                                  (* Clight local environment *)
    453453  cm_env →                                  (* Cminor local environment *)
     
    493493  (* ---- invariant on fresh variables ---- *)
    494494  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
     495  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … 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_Internal cl_f) (Internal … 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
    497497
    498498(* While continuation *) 
     
    543543            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
    544544            (St_label exit St_skip)), cm_k'〉, Hinv» →
    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
     545  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … 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_Internal cl_f) (Internal … cm_f) cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type
    547547    (Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k')
    548548    (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')) stack
    549549   
    550550| ClCm_cont_call_store:
    551   ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
     551  ∀cl_ge, cm_ge, INV, (* callee fn *) cl_fd, cm_fd, (* caller *) cl_f, cm_f, target_type, target_type'.
    552552  ∀stack.
    553   ∀alloc_type.
    554   ∀tmp_env.
    555   ∀cl_env.
    556   ∀cm_env.
     553  ∀alloc_type,alloc_type'.
     554  ∀tmp_env,tmp_env'.
     555  ∀cl_env,cl_env'.
     556  ∀cm_env,cm_env'.
    557557  ∀cm_m.
    558558  (* sub-continuations *)
     
    570570  ∀Hstmt_inv.
    571571  (* 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
     572  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … cm_f) cl_env' cm_env' cm_m alloc_type' tmp_env' (* stmt_univ stmt_univ' *) target_type' cl_k' cm_k' stack →
     573  clight_cminor_cont_rel cl_ge cm_ge INV cl_fd cm_fd cl_env cm_env cm_m alloc_type tmp_env (*stmt_univ stmt_univ*) target_type
    573574    (Kcall (Some ? 〈CL_lvalue_block, CL_lvalue_offset, lhs_ty〉) cl_f cl_env cl_k')
    574     cm_k'
     575    Kend (* cm_k' is on the Cminor stack, below *)
    575576    (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)
     577     (update_present SymbolTag val cm_env' tmp_var Htmp_var_present (Vptr CM_lvalue_ptr)) Hret_present
     578     (stmt_inv_update cm_f cm_env' (f_body cm_f) tmp_var (Vptr CM_lvalue_ptr) fInv Htmp_var_present)
    578579     (Kseq
    579580      (St_store (typ_of_type lhs_ty) (Id ASTptr tmp_var)
     
    581582
    582583| ClCm_cont_call_nostore:
    583   ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
     584  ∀cl_ge, cm_ge, INV, (* callee *) cl_fd, cm_fd, (* caller *) cl_f, cm_f, target_type, target_type'.
    584585  ∀stack.
    585   ∀alloc_type.
    586   ∀tmpenv.
    587   ∀cl_env.
    588   ∀cm_env.
     586  ∀alloc_type,alloc_type'.
     587  ∀tmpenv, tmpenv'.
     588  ∀cl_env,cl_env'.
     589  ∀cm_env,cm_env'.
    589590  ∀cm_m.
    590591  (* sub-continuations *)
     
    609610  ∀fInv.
    610611(*  ∀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  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … cm_f) cl_env' cm_env' cm_m alloc_type' tmpenv' (* stmt_univ stmt_univ' *) target_type' cl_k' cm_k' stack →
     613  clight_cminor_cont_rel cl_ge cm_ge INV cl_fd cm_fd cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) target_type
    612614   (Kcall cl_lhs cl_f cl_env cl_k')
    613     cm_k'
     615   Kend
    614616   (Scall cm_lhs cm_f stackptr cm_env Hret_present fInv cm_k' Hstmt_inv stack).
    615617
     
    706708  ∀tmpenv.
    707709  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 →
     710  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … cm_f) cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st →
    709711  (* ---- state invariants for memory and environments ---- *)
    710712  (* Embedding *)
     
    779781  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
    780782               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 →
     783  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … cm_f) cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) (None ?) cl_k cm_k cm_st →
    782784  clight_cminor_rel cl_ge cm_ge INV
    783785    (ClReturnstate Vundef cl_k cl_m)
     
    794796  (* Clight continuation *)
    795797  ∀cl_k: cl_cont.
    796   (* Cminor continuation *) 
    797   ∀cm_k: cm_cont.
    798798  (* Cminor stack *)
    799799  ∀cm_st: stack.
    800   (* Clight enclosing function *)
    801   ∀cl_f: function.
    802   (* Cminor enclosing function *)
    803   ∀cm_f: internal_function.
    804800  (* Clight called fundef *)
    805801  ∀cl_fundef.
     
    811807  (* optional return type of the function *)
    812808  ∀target_type.
    813   (* mapping from variables to their Cminor alloc type *)                                 
    814   ∀alloc_type.
    815809  (* Clight env/mem *)
    816810  ∀cl_env, cl_m.
    817811  (* Cminor env/mem *)
    818812  ∀cm_env, cm_m.
    819   (* Stack pointer (block containing Cminor locals), stack frame size *)
    820   ∀stackptr, stacksize.
    821813  (* fresh label generator for function *)
    822814  ∀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 →
    826815  (* specify fblock *)
    827816  find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cl_fundef →
    828817  find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef →
    829818  ∀cl_fun_id, cm_fun_id.
    830   ∀stmt_univ: tmpgen alloc_type.
    831819  ∀tmpenv.
    832   lset_inclusion ? (tmp_env ? stmt_univ) tmpenv →
    833   match cl_fundef with
    834   [ CL_Internal _ ⇒
     820  (*match cl_fundef with
     821  [ CL_Internal _ ⇒*)
    835822     (* 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
     823     clight_cminor_cont_rel cl_ge cm_ge INV cl_fundef cm_fundef cl_env cm_env cm_m (empty_map …) tmpenv target_type cl_k Kend cm_st
    837824(*       ∨
    838825     (∃cl_blo, cl_off, cl_ty.         (* Clight return loscation + type *)
     
    846833                     (Kseq (St_store (typ_of_type cl_ty) (Id ? cm_loc_ident) (Id ? cm_return_ident)) cm_k)
    847834                      kInv cm_st))) *)
    848   | CL_External cl_id cl_argtypes cl_rettype ⇒
     835  (*| CL_External cl_id cl_argtypes cl_rettype ⇒
    849836    match cm_fundef with
    850837    [ Internal _ ⇒ False
     
    854841        cl_fun_id = cl_id ∧ cm_fun_id = cm_id ∧ cl_fun_id = cm_fun_id
    855842      ] *)
    856   ]
     843  ]*)
    857844  (* ---- state invariants for memory and environments ---- *)
    858845  (* Embedding *)
    859846  ∀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'〉) →
    866847  (* memory injection *)
    867848  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 →
    870849  (* Force embedding to compute identity on functions *)
    871850  (∀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)) →
    875851  ∀cl_args_values, cm_args_values.
    876852  All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
     
    913889 ∀tmpenv'.
    914890 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 →
     891 clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … cm_f) cl_env cm_env cm_m alloc_type tmpenv' rettyp cl_k cm_k cm_stack →
    916892 (* Invariants *)
    917893 ∀Em: embedding.
     
    19791955      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
    19801956    ).
    1981 #g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_normal #Hnot_labeleld
    1982 inversion Hstate_rel
     1957#Xg1 #Xg2 #XINV #Xs1 #Xs1' *
    19831958[ 1: (* Normal state *)
    19841959     (* ---------------------------------------------------------------------- *)
     
    20382013     #Em #Htmp_vars_well_allocated
    20392014     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
    2040      #Hframe_spec #Henv_below
    2041      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2042      destruct (HA HB)
    2043      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
    2044      destruct (HC HD HE)
     2015     #Hframe_spec #Henv_below #Hclight_normal #Hnot_labeleld
    20452016     lapply Htranslate -Htranslate
    20462017     [ 1: generalize in match (conj ????); #Hugly_inv
     
    21852156     #Htmp_vars_well_allocated
    21862157     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
    2187      #Hframe_spec #Henv_below
    2188      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2189      destruct (HA HB)
    2190      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2191      destruct (HC HD HE) #_
     2158     #Hframe_spec #Henv_below #Hclight_normal #Hnot_labeleld
    21922159     (* back to unfolding Clight execution *)
    21932160     cases (bind_inversion ????? Htranslate) -Htranslate *
     
    24142381    | 2: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
    24152382    | 3: ]
    2416     [ 3: @(CMR_call … Htranslate_function … Hinjection … Hmatching … HEm_fn_id) try assumption
     2383    [ 3: @(CMR_call … Hinjection … HEm_fn_id) try assumption
    24172384         lapply (alloc_tmp_monotonic … (sym_eq ??? Heq_alloc_tmp)) #Hincl1
    24182385         lapply (alloc_tmp_monotonic … (sym_eq ??? Heq_alloc_tmp')) #Hincl2
     
    24212388         lapply Htranslate_fundef -Htranslate_fundef
    24222389         lapply Hfundef_fresh_for_tmp_u -Hfundef_fresh_for_tmp_u
    2423          cases CL_callee_fundef normalize nodelta
    2424          [ 1: #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef @ClCm_cont_call_store
    2425          | 2: #id #tl #ty #Hfd_fresh
    2426               whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) normalize nodelta @I ]
     2390         #Hfundef_fresh_for_tmp_u #Htranslate_fundef
     2391         @ClCm_cont_call_store assumption
    24272392    | 1,2: (* no return or return to CM local variable *)
    2428            @(CMR_call … Htranslate_function … Hinjection … Hmatching … HEm_fn_id) try assumption
    2429            cases CL_callee_fundef in Hfundef_fresh_for_tmp_u Htranslate_fundef; normalize nodelta
    2430            [ 1,3: (* Internal case *)
    2431              #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef
    2432              whd nodelta in match (typeof ?);
    2433              [ @ClCm_cont_call_nostore normalize nodelta
    2434                %{CL_lvalue_block} %{CL_lvalue_offset} %{(typeof lhs)} %{var_id}
    2435                @conj @refl
    2436              | @ClCm_cont_call_nostore normalize nodelta @I ]
    2437            | 2,4: #fid #tl #ty #H1 #H2
    2438              whd in H2:(??%?); destruct (H2) @I
    2439            ]
     2393           @(CMR_call … Hinjection … HEm_fn_id) try assumption
     2394           @(ClCm_cont_call_nostore … Hcont_rel) try assumption
     2395           whd %{CL_lvalue_block} %{CL_lvalue_offset} %{(typeof lhs)} %{var_id}
     2396           % %
    24402397    ]
    24412398| 1: (* Skip *)
     
    24942451      #Em #Htmp_vars_well_allocated
    24952452      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
    2496       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2497       destruct (HA HB)
    2498       @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2499       destruct (HC HD HE) #_
     2453      #Hclight_normal #Hnot_labeleld
    25002454      (* unfold the clight execution *)
    25012455      #s2 #tr whd in ⊢ ((??%?) → ?);
    2502       inversion (fn_return kcl_f) normalize nodelta
     2456      inversion (fn_return cl_f) normalize nodelta
    25032457      [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    25042458      | #structname #fieldspec | #unionname #fieldspec | #id ]
     
    25502504      #Htmp_vars_well_alloc
    25512505      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
    2552       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2553       destruct (HA HB)
    2554       @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2555       destruct (HC HD HE) #_
     2506      #Hclight_normal #Hnot_labeleld
    25562507      #s2 #tr whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    25572508      %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl
     
    25892540      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
    25902541      #HEm_fn_id #Hframe_spec #Henv_below
    2591       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2592       destruct (HA HB)
    2593       @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2594       destruct (HC HD HE) #_ #s2 #tr
     2542      #Hclight_normal #Hnot_labeleld
     2543      #s2 #tr
    25952544      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    25962545      lapply kHfind_label -kHfind_label
     
    26282577     #Em #Htmp_vars_well_allocated
    26292578     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
    2630      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2631      destruct (HA HB)
    2632      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
    2633      destruct (HC HD HE)
     2579     #Hclight_normal #Hnot_labeleld
    26342580     lapply Htranslate -Htranslate
    26352581     (* case-split on lhs in order to reduce lvalue production in Cminor *)
     
    28982844     #Em #Htmp_vars_well_allocated
    28992845     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
    2900      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2901      destruct (HA HB)
    2902      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
    2903      destruct (HC HD HE)
     2846     #Hclight_normal #Hnot_labeleld
    29042847     cases (bind_inversion ????? Htranslate) -Htranslate
    29052848     * * * #tmp_gen #labgen #cm_s1 #Htrans_inv * #Htrans_stm1 normalize nodelta
     
    29282871  #cl_env #cl_m #cm_env #cm_mt #stackptr #stacksize
    29292872  #stmt_univ #tmpenv #Htmpenv #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe #Hcont
    2930   @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2931   destruct (HA HB)
    2932   @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2933   destruct (HC HD HE)
    2934   #_
     2873  #Hclight_normal #Hnot_labeleld
    29352874  whd in Hclight_normal:%;
    29362875  @False_ind @Hclight_normal
    29372876| 3: (* Call state *)
    2938   #cl_ge #cm_ge #INV' #cl_k #cm_k #cm_st #cl_f #cm_f #cl_fundef #cm_fundef
    2939   #fblock #target_type #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
    2940   #func_univ #Hgobals_fresh #Hfundef_fresh #Htranslate_function #Hfind_cl #Hfind_cm
    2941   #cl_id #cm_id #stmt_univ #tmpenv #Htmpenv #Hcont_rel
    2942   #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe
     2877  #cl_ge #cm_ge #INV' #cl_k #cm_st #cl_fundef #cm_fundef
     2878  #fblock #target_type #cl_env #cl_m #cm_env #cm_m
     2879  #func_univ #Hfind_cl #Hfind_cm
     2880  #cl_id #cm_id #tmpenv #Hcont_rel
     2881  #Em #Hinj #Hem_fn_id
    29432882  #cl_args_values #cm_args_values #Hall2
    2944   @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2945   destruct (HA HB)
    2946   @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2947   destruct (HC HD HE) #_
     2883  #Hclight_normal #Hnot_labeleld
    29482884  whd in Hclight_normal:%;
    29492885  @False_ind @Hclight_normal
     
    29602896#Hexpr_vars #Htranslate_expr #Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement
    29612897#Hlabel_inclusion #Hlabel_exists #Hinv1 #Hinv2 #Hfind_label
    2962 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2963 destruct (HA HB)
    2964 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2965 destruct (HC HD HE) #_
     2898#Hclight_normal #Hnot_labeleld
    29662899#s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
    29672900(* execute clight condition *)
     
    30933026] qed.
    30943027
     3028(* TODO: move to common/Pointers.ma *)
     3029axiom offset_plus_zero : ∀o.
     3030  offset_plus o zero_offset = o.
     3031
     3032(* TODO: move to memory model *)
     3033lemma valid_block_dec: ∀m,b. (valid_block m b) + (¬valid_block m b).
     3034#m * #b
     3035whd in ⊢ (?%(?%));
     3036lapply (refl ? (Zltb b (nextblock m)))
     3037cases (Zltb b (nextblock m)) in ⊢ (???% → ?);
     3038#H
     3039[ %1 @Zltb_true_to_Zlt assumption
     3040| %2 @Zltb_false_to_not_Zlt assumption
     3041] qed.
     3042
     3043definition equal_embedding : mem → block → option (block × offset) ≝
     3044λm,b. match valid_block_dec m b with
     3045[ inl _ ⇒ Some ? 〈b,zero_offset〉
     3046| inr _ ⇒ None ?
     3047].
     3048
     3049lemma valid_pointer_valid_block : ∀m,b,o.
     3050  valid_pointer m (mk_pointer b o) →
     3051  valid_block m b.
     3052#m #b #o #VP
     3053cases (andb_Prop_true … VP) #H
     3054cases (andb_Prop_true … H) #B #_ #_
     3055whd @(Zltb_true_to_Zlt … B)
     3056qed.
     3057
     3058lemma valid_block_dec_true : ∀m,b.
     3059  valid_block m b →
     3060  ∃H. valid_block_dec m b = inl … H.
     3061#m * #b #H whd in ⊢ (??(λ_.??%?)); whd in H;
     3062generalize in ⊢ (??(λ_.??(?%)?));
     3063>(Zlt_to_Zltb_true … H) in ⊢ (???% → ??(λ_.??(match % with [_⇒?|_⇒?]?)?));
     3064#E % [2: % | skip ]
     3065qed.
     3066
     3067lemma not_Zlt_to_Zltb_false : ∀x,y.
     3068  ¬(Zlt x y) →
     3069  Zltb x y = false.
     3070#x #y #N lapply (Zltb_true_to_Zlt x y)
     3071cases (Zltb x y) //
     3072#H @⊥ @(absurd … (H (refl ??))) @N
     3073qed.
     3074
     3075lemma valid_block_dec_false : ∀m,b.
     3076  ¬valid_block m b →
     3077  ∃H. valid_block_dec m b = inr … H.
     3078#m * #b #H whd in ⊢ (??(λ_.??%?)); whd in H;
     3079generalize in ⊢ (??(λ_.??(?%)?));
     3080>(not_Zlt_to_Zltb_false … H) in ⊢ (???% → ??(λ_.??(match % with [_⇒?|_⇒?]?)?));
     3081#E % [2: % | skip ]
     3082qed.
     3083
     3084(* TODO: move to memoryInjections.ma? *)
     3085lemma equal_value_eq : ∀m,ty,b,o,v.
     3086  (∀p. load_value_of_type ty m b o = Some ? (Vptr p) → valid_pointer m p) →
     3087  load_value_of_type ty m b o = Some ? v →
     3088  value_eq (equal_embedding m) v v.
     3089#m #ty #b #o * //
     3090* #b' #o' #H1 #H2 @vptr_eq
     3091whd in ⊢ (??%?); whd in match (equal_embedding ??);
     3092cases (valid_block_dec_true … (valid_pointer_valid_block m b' o' ?))
     3093[2: @H1 @H2 ]
     3094#H3 #E >E whd in ⊢ (??%?);
     3095>offset_plus_zero %
     3096qed.
     3097
     3098lemma equal_embedding_elim : ∀m,b,b',o. ∀P:block → offset → Prop.
     3099  equal_embedding m b = Some ? 〈b',o〉 →
     3100  (valid_block m b → P b zero_offset) →
     3101  P b' o.
     3102#m * #b #b' #o #P
     3103whd in ⊢ (??%? → ?);
     3104cases (valid_block_dec ??) #H #E
     3105whd in E:(??%%); destruct
     3106/2/
     3107qed.
     3108
     3109lemma pointer_translation_elim : ∀m,p,p'. ∀P:pointer → Prop.
     3110  pointer_translation p (equal_embedding m) = Some ? p' →
     3111  P p →
     3112  P p'.
     3113#m * #b #o * #b' #o' #P whd in ⊢ (??%? → ?);
     3114whd in match (equal_embedding m b);
     3115cases (valid_block_dec ??)
     3116#H #E whd in E:(??%?); [ >offset_plus_zero in E; #E ] destruct
     3117//
     3118qed.
     3119
     3120lemma pointer_translation_elim' : ∀m,b,o,b',o'. ∀P:block → offset → Prop.
     3121  pointer_translation (mk_pointer b o) (equal_embedding m) = Some ? (mk_pointer b' o') →
     3122  P b o →
     3123  P b' o'.
     3124#m #b #o #b' #o' #P whd in ⊢ (??%? → ?);
     3125whd in match (equal_embedding m b);
     3126cases (valid_block_dec ??)
     3127#H #E whd in E:(??%?); [ >offset_plus_zero in E; #E ] destruct
     3128//
     3129qed.
     3130
     3131lemma equal_memory_injection : ∀m.
     3132  (∀b. valid_block m b → block_implementable_bv m b) →
     3133  (∀ty,b,o,p. load_value_of_type ty m b o = Some ? (Vptr p) → valid_pointer m p) →
     3134  memory_inj (equal_embedding m) m m.
     3135#m #addr_ok #contents_ok %
     3136[ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans
     3137  @(pointer_translation_elim' … Htrans)
     3138  #Hload
     3139  %{v1} destruct %{Hload} @(equal_value_eq … Hload) @contents_ok
     3140| #b #H whd in ⊢ (??%?);
     3141  cases (valid_block_dec_false … H) #H' #E >E %
     3142| * #b #o #p' #Hv #Ht @(pointer_translation_elim … Ht)
     3143  @Hv
     3144| #b #b' #off #Hem @(equal_embedding_elim … Hem) //
     3145| #b #b' #o' #Hem @(equal_embedding_elim … Hem) //
     3146| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #NE #Hem1 #Hem2
     3147  @(equal_embedding_elim … Hem1)
     3148  @(equal_embedding_elim … Hem2)
     3149  #_ #_ @eq_block_elim [ #E @⊥ @(absurd … E NE) | // ]
     3150| #b whd whd in match (equal_embedding m b);
     3151  cases (valid_block_dec m b) #H whd //
     3152  % [ % @addr_ok assumption | cases (addr_ok … H) #_ * #_ #H' >Zplus_z_OZ @H' ]
     3153] qed.
     3154
     3155axiom init_mem_good : ∀F,V,i,p,m.
     3156  init_mem F V i p = OK … m →
     3157  (∀b. valid_block m b → block_implementable_bv m b) ∧
     3158  (∀ty,b,o,p. load_value_of_type ty m b o = Some ? (Vptr p) → valid_pointer m p).
    30953159
    30963160lemma init_clight_cminor : ∀p,p',s.
     
    31273191  whd in ⊢ (??%?); >FFP'
    31283192  whd in ⊢ (??%?); %
    3129 | (* Axiomatised - we don't have the simulation step out of Callstate yet anyway. *)
    3130   cases daemon
     3193| @(CMR_call … FFP FFP' … (ClCm_cont_stop …))
     3194  [ @(Some ? (ASTint I32 Signed))
     3195  | @(empty_map …)
     3196  | @(empty_map …)
     3197  | @(new_universe …)
     3198  | @([ ])
     3199  | %
     3200  | whd @(equal_embedding m)
     3201  | cases (init_mem_good … INITMEM) #H1 #H2 @equal_memory_injection assumption
     3202  | (* This is a little too concrete... and the property is true but a little
     3203       strong (we always map function blocks in the embedding - even if there's
     3204       no function!) *)
     3205    #b #CODE cut (valid_block m b)
     3206    [ cases b in CODE ⊢ %; * [2,3:#z] #CODE whd in CODE:(??%?); destruct whd
     3207      lapply (nextblock_pos m) cases (nextblock m) [2,3,5,6:#z'] try * %
     3208    ] #VALID
     3209    whd in ⊢ (??%?); cases (valid_block_dec ??)
     3210    [ //
     3211    | #INVALID @⊥ @(absurd … VALID INVALID)
     3212    ]
     3213  | %
     3214  ]
    31313215] qed.
    31323216
  • src/Clight/toCminorMeasurable.ma

    r3063 r3155  
    6464  #ge #ge' #RG #Xs1 #Xs2 * //
    6565  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #E
    66   | #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 #H184 #H185 #H186 #E
     66  | #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 #H169 #H170 #E
    6767  | #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 #H140 #H141 #H142 #E
    6868  ] whd in E:(??%?); destruct
     
    7171  [ #H189 #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 *
    7272  | #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 #H255 #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 #H266 *
    73   | #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 #H278 #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 #H303 #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312
     73  | #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 #H278 #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 #H292 #H293 #H294 #H295 #H296
    7474  | #H314 #H315 #H316 #H317 #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 #H331 #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 #H342 #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 #H356 #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 #H370 #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 *
    7575  ] (* FIXME *) cases daemon
Note: See TracChangeset for help on using the changeset viewer.