Ignore:
Timestamp:
Mar 7, 2013, 6:03:18 PM (7 years ago)
Author:
tranquil
Message:

added local_stacksize to joint internal functions to accomodate for locals in the stack inherited from the front end

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2570 r2808  
    209209definition graph_prog_params ≝
    210210λp,p',prog,stack_sizes.
    211 mk_prog_params (make_sem_graph_params p p') prog stack_sizes.
     211mk_prog_params (mk_sem_graph_params p p') prog stack_sizes.
    212212
    213213definition graph_abstract_status:
     
    223223definition lin_prog_params ≝
    224224λp,p',prog,stack_sizes.
    225 mk_prog_params (make_sem_lin_params p p') prog stack_sizes.
     225mk_prog_params (mk_sem_lin_params p p') prog stack_sizes.
    226226
    227227definition lin_abstract_status:
     
    296296 ≝
    297297  λp,p',prog,sigma,pc.
    298   let pars ≝ make_sem_graph_params p p' in
     298  let pars ≝ mk_sem_graph_params p p' in
    299299  let ge ≝ globalenv_noinit … prog in
    300300  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
     
    304304    ! lin_point ← sigma fd (point_of_pc pars pc) ;
    305305    return pc_of_point
    306     (make_sem_lin_params ? p') (pc_block pc) lin_point.
     306    (mk_sem_lin_params ? p') (pc_block pc) lin_point.
    307307
    308308definition well_formed_pc:
     
    574574  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
    575575  (sigma : sigma_map p graph_prog) : Type[0] ≝
    576 { well_formed_frames : framesT (make_sem_graph_params p p') → Prop
    577 ; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
     576{ well_formed_frames : framesT (mk_sem_graph_params p p') → Prop
     577; sigma_frames : ∀frms.well_formed_frames frms → framesT (mk_sem_lin_params p p')
    578578; sigma_empty_frames_commute :
    579579  ∃prf.
    580   empty_framesT (make_sem_lin_params p p') =
    581   sigma_frames (empty_framesT (make_sem_graph_params p p')) prf
    582 
    583 ; well_formed_regs : regsT (make_sem_graph_params p p') → Prop
    584 ; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p')
     580  empty_framesT (mk_sem_lin_params p p') =
     581  sigma_frames (empty_framesT (mk_sem_graph_params p p')) prf
     582
     583; well_formed_regs : regsT (mk_sem_graph_params p p') → Prop
     584; sigma_regs : ∀regs.well_formed_regs regs → regsT (mk_sem_lin_params p p')
    585585; sigma_empty_regsT_commute :
    586586  ∀ptr.∃ prf.
    587   empty_regsT (make_sem_lin_params p p') ptr =
    588   sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf
     587  empty_regsT (mk_sem_lin_params p p') ptr =
     588  sigma_regs (empty_regsT (mk_sem_graph_params p p') ptr) prf
    589589; sigma_load_sp_commute :
    590590  preserving … res_preserve …
     
    593593    sigma_regs
    594594    (λx.λ_.x)
    595     (load_sp (make_sem_graph_params p p'))
    596     (load_sp (make_sem_lin_params p p'))
     595    (load_sp (mk_sem_graph_params p p'))
     596    (load_sp (mk_sem_lin_params p p'))
    597597; sigma_save_sp_commute :
    598598  ∀reg,ptr,prf1. ∃prf2.
    599   save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr =
    600   sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2
     599  save_sp (mk_sem_lin_params p p') (sigma_regs reg prf1) ptr =
     600  sigma_regs (save_sp (mk_sem_graph_params p p') reg ptr) prf2
    601601}.
    602602
     
    605605 ∀sigma.
    606606 good_sem_state_sigma p p' graph_prog sigma →
    607  state (make_sem_graph_params p p') → Prop ≝
     607 state (mk_sem_graph_params p p') → Prop ≝
    608608λp,p',graph_prog,sigma,gsss,st.
    609609well_formed_frames … gsss (st_frms … st) ∧
     
    616616 ∀sigma.
    617617 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
    618  ∀st : state (make_sem_graph_params p p').
     618 ∀st : state (mk_sem_graph_params p p').
    619619 well_formed_state … gsss st →
    620  state (make_sem_lin_params p p') ≝
     620 state (mk_sem_lin_params p p') ≝
    621621λp,p',graph_prog,sigma,gsss,st,prf.
    622622mk_state …
     
    694694 ∀p,p',graph_prog,sigma.
    695695  good_sem_state_sigma p p' graph_prog sigma →
    696   state_pc (make_sem_graph_params p p') → Prop ≝
     696  state_pc (mk_sem_graph_params p p') → Prop ≝
    697697 λp,p',prog,sigma,gsss,st.
    698698 well_formed_pc p p' prog sigma (last_pop … st) ∧
     
    707707(*   let lin_prog ≝ linearise ? graph_prog in *)
    708708  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
    709     ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
     709    ∀s:state_pc (mk_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
    710710     well_formed_state_pc p p' graph_prog sigma gsss s →
    711       state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
     711      state_pc (mk_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
    712712
    713713 λp,p',graph_prog,sigma,gsss,s,prf.
     
    796796    (λr.pair_reg_move_ ? ? (p' ?) r mv)
    797797    (λr.pair_reg_move_ ? ? (p' ?) r mv)
    798 ; allocate_locals__commute :
    799   ∀loc, r1, prf1. ∃ prf2.
    800   allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =
    801   sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2
    802798; save_frame_commute :
    803799  ∀dest,fl.
     
    12211217    (joint_closed_internal_function
    12221218     (graph_prog_params p p' graph_prog
    1223       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1219      (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12241220       (linearise_int_fun p) graph_prog stack_sizes))
    12251221     (globals
    12261222      (graph_prog_params p p' graph_prog
    1227        (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1223       (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12281224        (linearise_int_fun p) graph_prog stack_sizes)))))
    12291225   (ev_genv
    12301226    (graph_prog_params p p' graph_prog
    1231      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1227     (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12321228      (linearise_int_fun p) graph_prog stack_sizes)))
    1233    (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
     1229   (pblock (pc (mk_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
    12341230 
    12351231
     
    12401236    (joint_closed_internal_function
    12411237     (graph_prog_params p p' graph_prog
    1242       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1238      (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12431239       (linearise_int_fun p) graph_prog stack_sizes))
    12441240     (globals
    12451241      (graph_prog_params p p' graph_prog
    1246        (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1242       (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12471243        (linearise_int_fun p) graph_prog stack_sizes)))))
    12481244   (ev_genv
    12491245    (graph_prog_params p p' graph_prog
    1250      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1246     (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12511247      (linearise_int_fun p) graph_prog stack_sizes)))
    1252    (pblock (pc (make_sem_graph_params p p') st))) in H;
     1248   (pblock (pc (mk_sem_graph_params p p') st))) in H;
    12531249
    12541250
     
    13581354  fetch_internal_function …
    13591355    (globalenv_noinit … graph_prog) bl = return 〈i, fn〉 →
    1360   let pc' ≝ pc_of_point (make_sem_graph_params p p') … bl lbl in
     1356  let pc' ≝ pc_of_point (mk_sem_graph_params p p') … bl lbl in
    13611357  code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl →
    1362   ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
     1358  ∃prf'.pc_of_label (mk_sem_lin_params p p') … (globalenv_noinit … lin_prog)
    13631359    bl lbl =
    13641360        return sigma_pc p p' graph_prog sigma pc' prf'.
     
    14061402  ∀prf : well_formed_pc p p' graph_prog sigma pc.
    14071403 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 →
    1408  sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n →
    1409  point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
     1404 sigma fn (point_of_pc (mk_sem_graph_params p p') pc) = return n →
     1405 point_of_pc (mk_sem_lin_params p p') (sigma_pc … pc prf) = n.
    14101406#p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma
    14111407whd in match sigma_pc; normalize nodelta
     
    14311427  ∀sigma.good_sigma p graph_prog sigma →
    14321428  ∀prf : well_formed_pc p p' graph_prog sigma pc.
    1433   fetch_statement (make_sem_graph_params p p') …
     1429  fetch_statement (mk_sem_graph_params p p') …
    14341430    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
    14351431  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
    1436       (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl).
    1437       pc_of_label (make_sem_lin_params p p') …
     1432      (pc_of_point (mk_sem_graph_params p p') (pc_block pc) lbl).
     1433      pc_of_label (mk_sem_lin_params p p') …
    14381434          (globalenv_noinit … lin_prog)
    14391435          (pc_block pc)
     
    14441440        match s with
    14451441        [ step_seq x ⇒
    1446           fetch_statement (make_sem_lin_params p p') …
     1442          fetch_statement (mk_sem_lin_params p p') …
    14471443          (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    14481444              return 〈f, \fst (linearise_int_fun … fn),
    14491445                      sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
    14501446          ∃prf'.
    1451             let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
    1452             let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
     1447            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (mk_sem_graph_params p p') pc nxt) prf' in
     1448            let nxt_pc ≝ succ_pc (mk_sem_lin_params p p') (sigma_pc … pc prf) it in
    14531449            (nxt_pc = sigma_nxt ∨
    1454               (fetch_statement (make_sem_lin_params p p') …
     1450              (fetch_statement (mk_sem_lin_params p p') …
    14551451                (globalenv_noinit … lin_prog) nxt_pc =
    14561452                return 〈f, \fst (linearise_int_fun … fn),
    14571453                         final (mk_lin_params p) … (GOTO … nxt)〉 ∧
    1458               (pc_of_label (make_sem_lin_params p p') …
     1454              (pc_of_label (mk_sem_lin_params p p') …
    14591455                (globalenv_noinit … lin_prog)
    14601456                (pc_block pc)
     
    14621458        | COND a ltrue ⇒
    14631459            ∃prf'.
    1464             let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
     1460            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (mk_sem_graph_params p p') pc nxt) prf' in
    14651461            (let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
    1466             (fetch_statement (make_sem_lin_params p p') …
     1462            (fetch_statement (mk_sem_lin_params p p') …
    14671463            (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    14681464              return 〈f, \fst (linearise_int_fun … fn),
    14691465                      sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧
    14701466             nxt_pc = sigma_nxt)) ∨
    1471             (fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 
     1467            (fetch_statement (mk_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 
    14721468             =
    14731469             return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ∧
    1474             pc_of_label (make_sem_lin_params p p') …
     1470            pc_of_label (mk_sem_lin_params p p') …
    14751471                (globalenv_noinit … lin_prog)
    14761472                (pc_block pc)
    14771473                nxt = return sigma_nxt)
    14781474         ]
    1479     | final z ⇒   fetch_statement (make_sem_lin_params p p') …
     1475    | final z ⇒   fetch_statement (mk_sem_lin_params p p') …
    14801476                   (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    14811477                   return 〈f, \fst (linearise_int_fun … fn), final  (mk_lin_params p) … z〉
     
    21802176 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt →
    21812177 ∀prf : well_formed_state_pc … gss st.
    2182    fetch_statement (make_sem_graph_params p p') …
     2178   fetch_statement (mk_sem_graph_params p p') …
    21832179    (globalenv_noinit ? graph_prog) (pc … st) =
    21842180      return 〈f, fn,  sequential … (step_seq (mk_graph_params p) … stmt) nxt〉 →
     
    22472243   (sigma_state p p' graph_prog sigma gss)
    22482244   (λx.λ_ : True .x)
    2249    (block_of_call (make_sem_graph_params p p') …
     2245   (block_of_call (mk_sem_graph_params p p') …
    22502246      (globalenv_noinit ? graph_prog) cl)   
    2251    (block_of_call (make_sem_lin_params p p') …
     2247   (block_of_call (mk_sem_lin_params p p') …
    22522248      (globalenv_noinit ? (linearise ? graph_prog)) cl).
    22532249#p #p' #graph_prog #sigma #gss #cl #st #prf
     
    22952291∃prf.
    22962292sigma_pc p p' graph_prog sigma
    2297    (pc_of_point (make_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf =
    2298       pc_of_point (make_sem_lin_params p p') bl 0.
     2293   (pc_of_point (mk_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf =
     2294      pc_of_point (mk_sem_lin_params p p') bl 0.
    22992295#p #p' #graph_prog #sigma #good #bl #f1 #fn1 #fn1_spec
    23002296cases (good fn1) * #entry_in #_ #_
     
    23182314 ∀st,st',f,fn,called,args,dest,nxt.
    23192315 ∀prf : well_formed_state_pc … gss st.
    2320   fetch_statement (make_sem_graph_params p p') …
     2316  fetch_statement (mk_sem_graph_params p p') …
    23212317    (globalenv_noinit ? graph_prog) (pc … st) =
    23222318      return 〈f, fn,
     
    23252321    return st' →
    23262322(* let st_pc' ≝ mk_state_pc ? st'
    2327   (succ_pc (make_sem_graph_params p p') …
     2323  (succ_pc (mk_sem_graph_params p p') …
    23282324    (pc … st) nxt) in
    23292325 ∀prf'.
    2330  fetch_statement (make_sem_lin_params p p') …
     2326 fetch_statement (mk_sem_lin_params p p') …
    23312327   (globalenv_noinit … lin_prog)
    2332      (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
     2328     (succ_pc (mk_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
    23332329   return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
    2334  pc_of_label (make_sem_lin_params p p') ?
     2330 pc_of_label (mk_sem_lin_params p p') ?
    23352331                (globalenv_noinit ? (linearise p … graph_prog))
    23362332                (pc_block (pc … st))
    23372333                nxt = return sigma_pc p p' graph_prog sigma
    2338     (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →*)
     2334    (succ_pc (mk_sem_graph_params p p') (pc … st) nxt) prf' →*)
    23392335  let st2_pre_call ≝ sigma_state_pc … gss st prf in
    23402336  ∃is_call, is_call'.
     
    24322428 ∀st,st',f,fn,nxt.
    24332429 ∀prf : well_formed_state_pc … gss st.
    2434    fetch_statement (make_sem_graph_params p p') …
     2430   fetch_statement (mk_sem_graph_params p p') …
    24352431    (globalenv_noinit ? graph_prog) (pc … st) =
    24362432      return 〈f, fn,  final … (GOTO (mk_graph_params p) … nxt)〉 →
     
    24802476∀st,st',f,fn,a,ltrue,lfalse.
    24812477∀prf : well_formed_state_pc … gss st.
    2482  fetch_statement (make_sem_graph_params p p') …
     2478 fetch_statement (mk_sem_graph_params p p') …
    24832479  (globalenv_noinit ? graph_prog) (pc … st) =
    24842480    return 〈f, fn,  sequential … (COND (mk_graph_params p) … a ltrue) lfalse〉 →
     
    25512547∀st,st',f,fn.
    25522548∀prf : well_formed_state_pc … gss st.
    2553  fetch_statement (make_sem_graph_params p p') …
     2549 fetch_statement (mk_sem_graph_params p p') …
    25542550  (globalenv_noinit ? graph_prog) (pc … st) =
    25552551    return 〈f, fn,  final … (RETURN (mk_graph_params p) … )〉 →
     
    26592655∀st,st',f,fn,fl,called,args.
    26602656∀prf : well_formed_state_pc … gss st.
    2661  fetch_statement (make_sem_graph_params p p') …
     2657 fetch_statement (mk_sem_graph_params p p') …
    26622658  (globalenv_noinit ? graph_prog) (pc … st) =
    26632659    return 〈f, fn,  final … (TAILCALL (mk_graph_params p) … fl called args)〉 →
     
    27332729qed.
    27342730   
    2735    
    2736    
    2737 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    2738     ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
    2739 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
    27402731
    27412732lemma linearise_ok:
     
    27442735 ∀stack_sizes.
    27452736 (∀sigma.good_state_sigma p p' graph_prog sigma) →
    2746    ex_Type1 … (λR.
     2737   ∃[1] R.
    27472738   status_simulation
    27482739    (graph_abstract_status p p' graph_prog stack_sizes)
     
    27682759whd in ⊢ (%→?);
    27692760change with
    2770   (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
     2761  (eval_state (mk_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
    27712762#EQeval
    27722763@('bind_inversion EQeval)
Note: See TracChangeset for help on using the changeset viewer.