Changeset 2555


Ignore:
Timestamp:
Dec 14, 2012, 12:40:37 AM (7 years ago)
Author:
piccolo
Message:

lemma eval_call_ok finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2553 r2555  
    21472147qed.
    21482148
     2149lemma block_of_call_sigma_commute :
     2150∀p,p',graph_prog,sigma.
     2151∀gss : good_state_sigma p p' graph_prog sigma.∀cl.
     2152 preserving … res_preserve …
     2153   (sigma_state p p' graph_prog sigma gss)
     2154   (λx.λ_ : True .x)
     2155   (block_of_call (make_sem_graph_params p p') …
     2156      (globalenv_noinit ? graph_prog) cl)   
     2157   (block_of_call (make_sem_lin_params p p') …
     2158      (globalenv_noinit ? (linearise ? graph_prog)) cl).
     2159#p #p' #graph_prog #sigma #gss #cl #st #prf
     2160@mfr_bind
     2161[3: cases cl
     2162  [ #id normalize nodelta @opt_to_res_preserve
     2163    >(find_symbol_transf …
     2164          (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog id)
     2165   #s #EQs %{I} >EQs in ⊢ (??%?); %
     2166  | * #dpl #dph normalize nodelta
     2167    @mfr_bind [3: @dpl_arg_retrieve_commute |*:]
     2168    #bv1 #bv1_prf
     2169    @mfr_bind [3: @dph_arg_retrieve_commute |*:]
     2170    #bv2 #bv2_prf
     2171    @(mfr_bind … (λptr.λ_:True.ptr))
     2172    [ lapply bv2_prf lapply bv2 lapply bv1_prf lapply bv1
     2173      @bv_pc_other
     2174      [ #pc1 #p #bv1_prf #bv2 #bv2_prf @res_preserve_error ]
     2175      #bv1 #bv1_no_pc #bv1_prf
     2176      @bv_pc_other
     2177      [ cases bv1 in bv1_prf;
     2178        [||#a #b #c| #a | #a | #a #b | #a #b ] #bv1_prf
     2179        #pc2 #p #bv2_prf @res_preserve_error ]
     2180      #bv2 #bv2_no_pc #bv2_prf
     2181      >sigma_bv_no_pc try assumption
     2182      >sigma_bv_no_pc try assumption
     2183      whd #ptr #EQ %{I EQ}
     2184   ] #ptr *
     2185   @if_elim #_ [ @mfr_return | @res_preserve_error ] %
     2186 ]
     2187|4: #bl * @opt_to_res_preserve #x #EQ %{I} @EQ
     2188|*:
     2189]
     2190qed.
     2191
     2192   
    21492193lemma eval_call_ok :
    21502194 ∀p,p',graph_prog.
    21512195 let lin_prog ≝ linearise p graph_prog in
    21522196 ∀stack_sizes.
    2153  ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     2197 ∀sigma. good_sigma p graph_prog sigma →
     2198 ∀gss : good_state_sigma p p' graph_prog sigma.
    21542199 ∀st,st',f,fn,called,args,dest,nxt.
    21552200 ∀prf : well_formed_state_pc … gss st.
    2156   fetch_statement (make_sem_lin_params p p') …
    2157     (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =
    2158       return 〈f, \fst (linearise_int_fun … fn),
    2159         sequential … (CALL (mk_lin_params p) … called args dest ) it〉 →
     2201  fetch_statement (make_sem_graph_params p p') …
     2202    (globalenv_noinit ? graph_prog) (pc … st) =
     2203      return 〈f, fn,
     2204        sequential … (CALL (mk_graph_params p) … called args dest ) nxt〉 →
    21602205   eval_seq_advance ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes))
    21612206      (CALL … called args dest) nxt st = return st' →
     
    21812226  eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes))
    21822227    st2_pre_call = return st2_after_call.
    2183 cases daemon
    2184 qed.
    2185 
     2228#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st1 #f #fn
     2229#called #args #dest #nxt #prf #fetch_spec
     2230cases(fetch_statement_sigma_commute … good (proj1 … prf) … fetch_spec) #_
     2231normalize nodelta * #lin_fetch_spec #_
     2232whd in match eval_seq_advance; whd in match eval_seq_call; normalize nodelta
     2233@('bind_inversion) #bl #H lapply (err_eq_from_io ????? H) -H #bl_spec
     2234@('bind_inversion) * #id #int_f #H lapply (err_eq_from_io ????? H) -H
     2235cases int_f -int_f [ #fn | #ext_f] #int_f_spec normalize nodelta
     2236[2:#H @('bind_inversion H) -H #st' #H #_ @('bind_inversion H) -H #vals #_
     2237  @'bind_inversion #vals' #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
     2238#H %
     2239[  @hide_prf
     2240  whd in match joint_classify; normalize nodelta >fetch_spec >m_return_bind
     2241  normalize nodelta whd in match joint_classify_step;
     2242  whd in match joint_classify_seq; normalize nodelta
     2243  >bl_spec >m_return_bind >int_f_spec normalize nodelta %
     2244| %
     2245  [ @hide_prf whd in match joint_classify; normalize nodelta >lin_fetch_spec
     2246    >m_return_bind normalize nodelta whd in match joint_classify_step;
     2247    whd in match joint_classify_seq; normalize nodelta
     2248    cases bl in bl_spec int_f_spec; #reg #reg_prf -bl #reg_spec #int_f_spec
     2249    cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ?
     2250            reg_spec)
     2251    * #EQ >EQ -EQ >m_return_bind
     2252    lapply(fetch_function_transf ?????
     2253      (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) ????)
     2254        [
     2255        | @(Internal ? fn)
     2256        | @id
     2257        | assumption assumption
     2258        |
     2259        |
     2260        | %
     2261          [@(prog_vars … graph_prog) 
     2262          |@(prog_funct … graph_prog)
     2263          |@(prog_main … graph_prog)
     2264          ]
     2265        ]
     2266      [>int_f_spec % | | |] #EQ >EQ normalize nodelta %
     2267   | %
     2268     [2: %
     2269         [  change with ((λx.joint_call_ident (lin_prog_params p p' (linearise p graph_prog) stack_sizes)
     2270              (mk_Sig ? ? ? x)) ? = (λx.joint_call_ident ? (mk_Sig ? ? ? x)) ?)
     2271            whd in match joint_call_ident in ⊢ (??(%?)?); normalize nodelta in ⊢ (??(%?)?);
     2272            whd in match (pc ?); >lin_fetch_spec in ⊢ (??(%?)?); normalize nodelta in ⊢ (??%?);
     2273            whd in match joint_call_ident in ⊢ (???(%?)); normalize nodelta in ⊢ (???(%?));
     2274            >fetch_spec in ⊢ (???(%?)); normalize nodelta >bl_spec in ⊢ (???%);
     2275            >m_return_bind in ⊢ (???%);
     2276         |  whd in match eval_state; normalize nodelta
     2277            >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2278             whd in match eval_statement_no_pc; normalize nodelta
     2279             whd in match eval_seq_no_pc; normalize nodelta
     2280             >m_return_bind in ⊢ (??%?);
     2281             whd in match eval_statement_advance; whd in match eval_seq_advance;
     2282             whd in match eval_seq_call; normalize nodelta
     2283         ]
     2284         cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ?
     2285             bl_spec) * #EQ >EQ in ⊢ (??%?); >m_return_bind in ⊢ (??%?); -EQ
     2286         [ whd in match fetch_internal_function; normalize nodelta >int_f_spec in ⊢ (???%);
     2287           >m_return_bind in ⊢ (???%); normalize nodelta ]
     2288         lapply(fetch_function_transf ?????
     2289                (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) ????)
     2290            [
     2291            | 2,12: @(Internal ? fn)
     2292            | 3,13: @id
     2293            | 4,14: assumption assumption
     2294            | 5,15:
     2295            | 6,16:
     2296            |7,17: %
     2297               [1,4: @(prog_vars … graph_prog) 
     2298               |2,5: @(prog_funct … graph_prog)
     2299               |3,6: @(prog_main … graph_prog)
     2300               ]
     2301            ]
     2302         [1,5: >int_f_spec % |*:] #EQ >EQ in ⊢ (??%?); -EQ
     2303          >m_return_bind in ⊢ (??%?); normalize nodelta [ %]
     2304      ]
     2305  ]
     2306]
     2307[2: @hide_prf]
     2308lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H)
     2309#st' #st_spec' #H @('bind_inversion H) -H #st'' #st_spec''
     2310whd in ⊢ (??%% → ?); #EQ destruct(EQ) [ % ]
     2311[2,3: elim(save_frame_commute p p' graph_prog sigma gss … prf … st_spec')
     2312      #wf_st' #sigma_st_spec' [2: >sigma_st_spec' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);]
     2313      lapply st_spec'' -st_spec''  whd in match eval_internal_call; normalize nodelta
     2314      #H @('bind_inversion H) -H #dim_s #dim_s_spec #H
     2315      [ >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);]
     2316      elim(bind_inversion ????? H) -H #st''' * #st_spec'''
     2317      elim(setup_call_commute p p' graph_prog sigma gss … wf_st' … st_spec''')
     2318      #wf_st''' #sigma_st_spec''' whd in ⊢ (??%% → ?);
     2319      whd in match allocate_locals; whd in match set_regs; normalize nodelta
     2320      #EQ destruct(EQ)
     2321]
     2322[  >sigma_st_spec''' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2323   whd in match sigma_state_pc; normalize nodelta
     2324   change with (return mk_state_pc (make_sem_lin_params p p') ? ? = ?)
     2325   cut(∀A,semp,pc,pc',st,st'.∀ f : ? → A.pc = pc' ∧ st = st' →
     2326          f(mk_state_pc semp st pc) = f(mk_state_pc semp st' pc'))
     2327   [#A #H1 #H2 #H3 #H4 #H5 #f * #H8 #H9 //]
     2328   #APP @APP %
     2329]
     2330[1,4: [whd in match sigma_pc; normalize nodelta @opt_safe_elim #lin_pc | whd in match well_formed_pc;]
     2331      whd in match sigma_pc_opt; normalize nodelta @if_elim
     2332      [1,3: @eqZb_elim [2,4: #_ *] #EQbl cases bl in EQbl int_f_spec; *
     2333            #reg #pos #reg_prf normalize in ⊢ (% → ?);
     2334            #EQbl whd in match fetch_function; normalize nodelta
     2335            >EQbl cases(symbol_for_block ???)
     2336            [1,3: whd in ⊢ (??%% → ?); #ABS destruct(ABS)]
     2337            #id1 >m_return_bind inversion(find_funct_ptr ???)
     2338            [1,3:#_ whd in ⊢ (??%% → ?); #ABS destruct(ABS)]
     2339            #z lapply(globalenv_no_minus_one ??? graph_prog) [1,3: @(λn.[Init_space n])]
     2340            #EQ 
     2341            change with ((find_funct_ptr ? (globalenv_noinit ? graph_prog) ? = ?) → ?)
     2342            change with ((find_funct_ptr ? (globalenv_noinit ? graph_prog) ? = ?)) in EQ;
     2343            cases reg in ⊢ (% → ?);
     2344            [1,3: whd in match find_funct_ptr; normalize nodelta #ABS destruct(ABS)
     2345            |2,4: >EQ #ABS destruct(ABS)
     2346            ]
     2347      |2,4: #_ whd in match fetch_internal_function; normalize nodelta
     2348            whd in match (pc_block ?); >int_f_spec >m_return_bind
     2349             >point_of_pc_of_point lapply(good fn) ** #EQ #_ #_ >EQ -EQ
     2350              >m_return_bind [2:%] whd in ⊢ (??%? → ?); #EQ destruct(EQ)
     2351              %
     2352      ]
     2353| whd in match sigma_state; normalize nodelta
     2354  cut(∀A,semp,fr,fr',is,is',c,c',r,r',m,m'.∀ f : ? → A.
     2355      fr = fr' ∧ is = is' ∧ c = c' ∧ r = r' ∧ m = m'→
     2356          f(mk_state semp fr is c r m) = f(mk_state semp fr' is' c' r' m'))
     2357  [#A #semp #fr #fr' #is #is' #c #c' #r #r' #m #m' #f **** //]
     2358  #APP @APP % [% [% [% [%]]]] // [whd in match sigma_is; normalize nodelta % |3:
     2359  whd in match sigma_mem; normalize nodelta %]
     2360|  % [2:  @(proj2 … wf_st')] % [  %  [ @(proj1 … (proj1 … (proj1 … wf_st'))) |
     2361          @(proj2 … (proj1 … (proj1 … wf_st')))] ]
     2362]
     2363[ change with (? = (λx.sigma_regs ? ? ? ? ? (foldr ? ? ? ? x) ?)?)
     2364  [ cut((joint_if_locals (lin_prog_params p p' (linearise p graph_prog) stack_sizes)
     2365   (globals (lin_prog_params p p' (linearise p graph_prog) stack_sizes))
     2366   (\fst  (linearise_int_fun p
     2367                (globals (graph_prog_params p p' graph_prog stack_sizes)) fn))) = (joint_if_locals (graph_prog_params p p' graph_prog stack_sizes)
     2368   (globals (graph_prog_params p p' graph_prog stack_sizes)) fn))
     2369   [%] #EQ >EQ
     2370    elim(joint_if_locals (graph_prog_params p p' graph_prog stack_sizes)
     2371     (globals (graph_prog_params p p' graph_prog stack_sizes)) fn) in ⊢ (??%(?%));
     2372  | @hide_prf elim x
     2373  ]
     2374| @hide_prf elim(joint_if_locals (graph_prog_params p p' graph_prog stack_sizes)
     2375     (globals (graph_prog_params p p' graph_prog stack_sizes)) fn)
     2376]
     2377[3,5: whd in match (foldr ? ? ???); @(proj2 … (proj1 … wf_st'))
     2378|4,6: #locs_t #tl_list #wf_regs_tail whd in match (foldr ? ? ???);
     2379      elim(allocate_locals_commute p p' graph_prog sigma gss locs_t
     2380               ? wf_regs_tail) #wf_regs_locs_t #_ assumption
     2381|*: normalize nodelta
     2382    [  whd in match (foldr ? ? ???) in ⊢ (??%%); %
     2383    | #locs_t #tl_list #EQtl whd in match (foldr ?????) in ⊢ (??%%);
     2384      >EQtl
     2385      lapply(allocate_locals_commute p p' graph_prog sigma gss locs_t
     2386        (foldr (localsT ?) (regsT ?) (allocate_locals_ ???) (regs ? st') tl_list) ?)
     2387      [2: * #x #H >H % |]
     2388    ]
     2389]
     2390qed.         
     2391               
    21862392lemma eval_goto_ok :
    2187 lemma eval_tailcall_ok :
     2393lemma eval_tailcall_ok
     2394 :
    21882395lemma eval_cond_cond_ok :
    21892396lemma eval_cond_fcond_ok :
Note: See TracChangeset for help on using the changeset viewer.