Changeset 3055


Ignore:
Timestamp:
Apr 1, 2013, 7:04:57 PM (4 years ago)
Author:
campbell
Message:

Start getting partial Clight to Cminor proof in shape for
measurability preservation.

Location:
src/Clight
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r3054 r3055  
    30493049
    30503050 
    3051 
    3052 
    3053 
    3054 (* TODO: adapt the following to the new goal shape. *)
    3055 (*
    3056  
    3057 axiom clight_cminor_cost :
    3058   ∀INV:clight_cminor_inv.
    3059   ∀s1,s1',s2,tr.
    3060   clight_cminor_rel INV s1 s1' →
    3061   Clight_labelled s1 →
    3062   after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
    3063   after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
    3064     tr = tr' ∧
    3065     clight_cminor_rel INV s2 s2'
    3066   ).
    3067 
    3068 axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
    3069   clight_to_cminor cl_program = OK ? cm_program →
    3070   make_initial_state ?? clight_fullexec cl_program = OK ? s →
    3071   make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
    3072   ∃INV. clight_cminor_rel INV s
     3051(* TODO: move to globalenvs *)
     3052lemma find_funct_match:
     3053    ∀M:matching.∀initV,initW.
     3054    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     3055    ∀MATCH:match_program … M p p'.
     3056    ∀v. ∀f: m_A M (prog_var_names … p).
     3057    find_funct … (globalenv … initV p) v = Some ? f →
     3058    ∃tf : m_B M (prog_var_names … p').
     3059    find_funct … (globalenv … initW p') v = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
     3060[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
     3061#M #initV #initW #p #p' #MP * [ | #sz #i | | #p ] #f
     3062[ 1,2,3: #FF whd in FF:(??%?); destruct ]
     3063whd in ⊢ (??%? → ?); @eq_offset_elim #OFF #FFP
     3064[2: whd in FFP:(??%?); destruct ]
     3065cases (find_funct_ptr_match M initV initW … MP (pblock p) f FFP)
     3066#f' * #FFP' #MF %{f'} %
     3067[ whd in ⊢ (??%?); >OFF >reflexive_eq_offset @FFP'
     3068| @MF
     3069] qed.
     3070
     3071lemma clight_cminor_inv_exists : ∀p,p'.
     3072  clight_to_cminor p = OK … p' →
     3073  clight_cminor_inv (make_global … clight_fullexec p) (make_global … Cminor_fullexec p').
     3074#p #p' #COMPILE
     3075lapply (clight_to_cminor_matches … COMPILE) #MATCHES -COMPILE
     3076%
     3077[2: #sym lapply (find_symbol_match (clight_cminor_matching p) ????? MATCHES)
     3078    [4: #H @sym_eq @H | #X #Y * #id #r #v1 #v2 * % | skip | skip ]
     3079|3: #v #f #FF cases (find_funct_match … MATCHES … FF)
     3080  [ #f' * #FF' whd in ⊢ (% → ?); * #H1 * #H2 #Efd
     3081    % [2: %{f'} %{H1} %{H2} % [ >Efd
     3082    -Efd -H1 -H2 -FF' -FF
     3083    generalize in ⊢ (??(??(match % with [_⇒?]))?);
     3084    >(matching_vars … (mp_vars … MATCHES)) -MATCHES
     3085    #E @(streicherK ???? E) %
     3086    | @FF'
     3087    ]
     3088   | skip
     3089   ]
     3090  | skip
     3091  ]
     3092| skip
     3093] qed.
     3094
     3095
     3096lemma init_clight_cminor : ∀p,p',s.
     3097  make_initial_state … clight_fullexec p = OK … s →
     3098  clight_to_cminor p = OK … p' →
     3099  ∃INV:clight_cminor_inv (make_global … clight_fullexec p) (make_global … Cminor_fullexec p').
     3100  ∃s'.
     3101    make_initial_state … Cminor_fullexec p' = OK … s' ∧
     3102    clight_cminor_rel (make_global … clight_fullexec p) (make_global … Cminor_fullexec p') INV s s'.
     3103#p #p' #s #INIT #COMPILE
     3104lapply (clight_to_cminor_matches … COMPILE) #MATCHES
     3105
     3106%{(clight_cminor_inv_exists … COMPILE)}
     3107
     3108lapply (find_funct_ptr_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES)
     3109lapply (find_symbol_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES)
     3110[ #v #w * // ]
     3111lapply (init_mem_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES)
     3112[ #v #w * // ]
     3113cases p in INIT COMPILE MATCHES ⊢ %; #vars #fns #main #INIT #COMPILE #MATCHES
     3114cases (bind_inversion ????? INIT) -INIT #m * #INITMEM #INIT
     3115cases (bind_inversion ????? INIT) -INIT #b * #FINDSYM #INIT
     3116cases (bind_inversion ????? INIT) -INIT #fd * #FFP #INIT
     3117whd in INIT:(??%%); destruct
     3118whd in match (m_A ??); whd in match (m_B ??); whd in match (m_V ?); whd in match (m_W ?);
     3119#M_initmem #M_findsym #M_ffp
     3120cases (M_ffp … FFP) -M_ffp #f' * #FFP' #Mf'
     3121%{(Callstate main f' [ ] m SStop)} %
     3122[ whd in ⊢ (??%?); normalize in M_initmem:(??(?%%%?)(?%%%?)); >M_initmem >INITMEM
     3123  whd in ⊢ (??%?); lapply (M_findsym main) <(mp_main … MATCHES)
     3124  whd in match (m_A ??); whd in match (m_B ??);
     3125  change with (make_global p') in match (globalenv ????); #E >E
     3126  >FINDSYM
     3127  whd in ⊢ (??%?); >FFP'
     3128  whd in ⊢ (??%?); %
     3129| (* Axiomatised - we don't have the simulation step out of Callstate yet anyway. *)
     3130  cases daemon
     3131] qed.
     3132
Note: See TracChangeset for help on using the changeset viewer.