Ignore:
Timestamp:
Nov 22, 2012, 6:40:31 PM (7 years ago)
Author:
piccolo
Message:

fixed Traces and semantics
added commutation record (not yet finished) and proofs in lineariseProof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2481 r2484  
    120120   ≠ None ….
    121121
    122 definition well_formed_status:
    123  ∀p,p',graph_prog.
     122definition sigma_beval_opt :
     123 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    124124  ((Σi.is_internal_function_of_program … graph_prog i) →
    125     label → option ℕ) →
    126   state_pc (make_sem_graph_params p p') → Prop ≝
    127  λp,p',prog,sigma,st.
    128  well_formed_pc p p' prog sigma (pc … st) ∧ ?.
    129 cases daemon (* TODO *)
    130 qed.
     125    code_point (mk_graph_params p) → option ℕ) →
     126  beval → option beval ≝
     127λp,p',graph_prog,sigma,bv.
     128match bv with
     129[ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt p p' graph_prog sigma pc ; return BVpc pc' prt
     130| _ ⇒ return bv
     131].
     132
     133definition sigma_beval :
     134 ∀p,p',graph_prog,sigma,bv.
     135 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝
     136 λp,p',graph_prog,sigma,bv.opt_safe ….
    131137
    132138(*
     
    165171λp,p',graph_prog,sigma,st.opt_safe ….
    166172 
    167 lemma sigma_pc_of_status_ok:
     173lemma sigma_pc_ok:
    168174  ∀p,p',graph_prog.
    169175  ∀sigma.
     
    174180    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
    175181
    176 definition sigma_state :
    177  ∀p.
    178  ∀p':∀F.sem_unserialized_params p F.
    179  ∀graph_prog.
    180   ∀sigma.
    181 (*   let lin_prog ≝ linearise ? graph_prog in *)
    182     ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
    183      well_formed_status p p' graph_prog sigma s →
    184       state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
    185 
    186  λp,p',graph_prog,sigma,s,prf.
    187  let pc' ≝ sigma_pc … (proj1 … prf) in
    188  mk_state_pc ? ? pc'.
    189  cases daemon (* TODO *) qed.
    190 
    191 lemma sigma_pc_commute:
    192  ∀p,p',graph_prog,sigma,st.
    193  ∀prf : well_formed_status p p' graph_prog sigma st.
    194  sigma_pc … (pc ? st) (proj1 … prf) =
    195  pc ? (sigma_state … st prf).
    196 #p #p' #prog #sigma #st #prf %
    197 qed.
    198 
    199 lemma res_eq_from_opt :
    200   ∀A,m,v.res_to_opt A m = return v → m = return v.
    201 #A * #x #v normalize #EQ destruct % qed.
    202 
    203182definition sigma_function_name :
    204183 ∀p,graph_prog.
     
    207186  (Σf.is_internal_function_of_program … lin_prog f) ≝
    208187λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
     188
     189record good_sigma_state (p : unserialized_params)
     190  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
     191 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
     192    graph_prog i) →
     193      label → option ℕ)
     194: Type[0] ≝
     195{ well_formed_state : state (make_sem_graph_params p p') → Prop
     196; sigma_state : ∀st.well_formed_state st → state (make_sem_lin_params p p')
     197
     198; acca_store_ok :
     199  ∀a,bv,bv',st,st',prf1,prf2.
     200  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
     201  acca_store ?? (p' ?) a bv st = return st' →
     202  acca_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
     203; acca_store_wf :  ∀a,bv,bv',st,st'.
     204  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
     205  acca_store ?? (p' ?) a bv st = return st' →
     206  well_formed_state st → well_formed_state st'
     207
     208; acca_retrieve_ok :
     209  ∀a,st,bv,prf1,prf2.
     210  acca_retrieve ?? (p' ?) st a = return bv →
     211  acca_retrieve ?? (p' ?) (sigma_state st prf1) a =
     212  return sigma_beval p p' graph_prog sigma bv prf2
     213; acca_retrieve_wf :  ∀a,st,bv.
     214  acca_retrieve ?? (p' ?) st a = return bv →
     215  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
     216
     217; acca_arg_retrieve_ok :
     218  ∀a,st,bv,prf1,prf2.
     219  acca_arg_retrieve ?? (p' ?) st a = return bv →
     220  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
     221  return sigma_beval p p' graph_prog sigma bv prf2
     222; acca_arg_retrieve_wf :  ∀a,st,bv.
     223  acca_arg_retrieve ?? (p' ?) st a = return bv →
     224  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
     225
     226; accb_store_ok :
     227  ∀a,bv,bv',st,st',prf1,prf2.
     228  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
     229  accb_store ?? (p' ?) a bv st = return st' →
     230  accb_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
     231; accb_store_wf :  ∀a,bv,bv',st,st'.
     232  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
     233  accb_store ?? (p' ?) a bv st = return st' →
     234  well_formed_state st → well_formed_state st'
     235
     236; accb_retrieve_ok :
     237  ∀a,st,bv,prf1,prf2.
     238  accb_retrieve ?? (p' ?) st a = return bv →
     239  accb_retrieve ?? (p' ?) (sigma_state st prf1) a =
     240  return sigma_beval p p' graph_prog sigma bv prf2
     241; accb_retrieve_wf :  ∀a,st,bv.
     242  accb_retrieve ?? (p' ?) st a = return bv →
     243  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
     244
     245; accb_arg_retrieve_ok :
     246  ∀a,st,bv,prf1,prf2.
     247  acca_arg_retrieve ?? (p' ?) st a = return bv →
     248  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
     249  return sigma_beval p p' graph_prog sigma bv prf2
     250; accb_arg_retrieve_wf :  ∀a,st,bv.
     251  accb_arg_retrieve ?? (p' ?) st a = return bv →
     252  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
     253
     254
     255; dpl_store_ok :
     256  ∀a,bv,bv',st,st',prf1,prf2.
     257  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
     258  dpl_store ?? (p' ?) a bv st = return st' →
     259  dpl_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
     260; dpl_store_wf :  ∀a,bv,bv',st,st'.
     261  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
     262  dpl_store ?? (p' ?) a bv st = return st' →
     263  well_formed_state st → well_formed_state st'
     264
     265; dpl_retrieve_ok :
     266  ∀a,st,bv,prf1,prf2.
     267  dpl_retrieve ?? (p' ?) st a = return bv →
     268  dpl_retrieve ?? (p' ?) (sigma_state st prf1) a =
     269  return sigma_beval p p' graph_prog sigma bv prf2
     270; dpl_retrieve_wf :  ∀a,st,bv.
     271  dpl_retrieve ?? (p' ?) st a = return bv →
     272  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
     273
     274; dpl_arg_retrieve_ok :
     275  ∀a,st,bv,prf1,prf2.
     276  acca_arg_retrieve ?? (p' ?) st a = return bv →
     277  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
     278  return sigma_beval p p' graph_prog sigma bv prf2
     279; dpl_arg_retrieve_wf :  ∀a,st,bv.
     280  dpl_arg_retrieve ?? (p' ?) st a = return bv →
     281  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
     282
     283
     284; dph_store_ok :
     285  ∀a,bv,bv',st,st',prf1,prf2.
     286  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
     287  dph_store ?? (p' ?) a bv st = return st' →
     288  dph_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
     289; dph_store_wf :  ∀a,bv,bv',st,st'.
     290  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
     291  dph_store ?? (p' ?) a bv st = return st' →
     292  well_formed_state st → well_formed_state st'
     293
     294; dph_retrieve_ok :
     295  ∀a,st,bv,prf1,prf2.
     296  dph_retrieve ?? (p' ?) st a = return bv →
     297  dph_retrieve ?? (p' ?) (sigma_state st prf1) a =
     298  return sigma_beval p p' graph_prog sigma bv prf2
     299; dph_retrieve_wf :  ∀a,st,bv.
     300  dph_retrieve ?? (p' ?) st a = return bv →
     301  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
     302
     303; dph_arg_retrieve_ok :
     304  ∀a,st,bv,prf1,prf2.
     305  acca_arg_retrieve ?? (p' ?) st a = return bv →
     306  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
     307  return sigma_beval p p' graph_prog sigma bv prf2
     308; dph_arg_retrieve_wf :  ∀a,st,bv.
     309  dph_arg_retrieve ?? (p' ?) st a = return bv →
     310  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
     311
     312
     313; snd_arg_retrieve_ok :
     314  ∀a,st,bv,prf1,prf2.
     315  snd_arg_retrieve ?? (p' ?) st a = return bv →
     316  snd_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
     317  return sigma_beval p p' graph_prog sigma bv prf2
     318; snd_arg_retrieve_wf :  ∀a,st,bv.
     319  snd_arg_retrieve ?? (p' ?) st a = return bv →
     320  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
     321
     322; pair_reg_move_ok :
     323  ∀mv,st1,st2,prf1,prf2.
     324  pair_reg_move ?? (p' ?) st1 mv = return st2 →
     325  pair_reg_move ?? (p' ?) (sigma_state st1 prf1) mv =
     326    return sigma_state st2 prf2
     327; pair_reg_move_wf :
     328  ∀mv,st1,st2.
     329  pair_reg_move ?? (p' ?) st1 mv = return st2 →
     330  well_formed_state st1 → well_formed_state st2
     331
     332; allocate_locals_ok :
     333  ∀l,st1,prf1,prf2.
     334  allocate_locals ?? (p' ?) l (sigma_state st1 prf1) =
     335    sigma_state (allocate_locals ?? (p' ?) l st1) prf2
     336; allocate_locals_wf :
     337  ∀l,st1.
     338  well_formed_state st1 →
     339    well_formed_state (allocate_locals ?? (p' ?) l st1)
     340
     341; save_frame_ok :
     342  ∀dest,st1,st2,prf1,prf2.
     343  save_frame ?? (p' ?) dest st1 = return st2 →
     344  let st1' ≝ mk_state_pc … (sigma_state st1 (proj2 … prf1))
     345    (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in
     346  save_frame ?? (p' ?) dest st1' = return sigma_state st2 prf2
     347; save_frame_wf :
     348  ∀dest,st1,st2.
     349  save_frame ?? (p' ?) dest st1 = return st2 →
     350  (well_formed_pc p p' graph_prog sigma (pc … st1) ∧
     351   well_formed_state st1) → well_formed_state st2
     352
     353; eval_ext_seq_ok :
     354  let lin_prog ≝ linearise p graph_prog in
     355  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     356  let stack_sizes' ≝
     357   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     358     ? graph_prog stack_sizes in
     359  ∀ext,fn,st1,st2,prf1,prf2.
     360  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     361    ext fn st1 = return st2 →
     362  eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
     363    ext (sigma_function_name … fn) (sigma_state st1 prf1) = return sigma_state st2 prf2
     364; eval_ext_seq_wf :
     365  let lin_prog ≝ linearise p graph_prog in
     366  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     367  let stack_sizes' ≝
     368   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     369     ? graph_prog stack_sizes in
     370  ∀ext,fn,st1,st2.
     371  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     372    ext fn st1 = return st2 →
     373  well_formed_state st1 → well_formed_state st2
     374
     375}.
     376
     377(* restano:
     378; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
     379    state st_pars → res (state st_pars)
     380; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
     381    res (list val)
     382; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
     383
     384(* from now on, parameters that use the type of functions *)
     385; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
     386(* change of pc must be left to *_flow execution *)
     387; pop_frame: ∀globals.∀ge : genv_gen F globals.
     388  (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
     389*)
     390
     391definition well_formed_state_pc :
     392 ∀p,p',graph_prog,sigma.
     393  good_sigma_state p p' graph_prog sigma →
     394  state_pc (make_sem_graph_params p p') → Prop ≝
     395 λp,p',prog,sigma,gss,st.
     396 well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gss st.
     397 
     398definition sigma_state_pc :
     399 ∀p.
     400 ∀p':∀F.sem_unserialized_params p F.
     401 ∀graph_prog.
     402  ∀sigma.
     403(*   let lin_prog ≝ linearise ? graph_prog in *)
     404  ∀gss : good_sigma_state p p' graph_prog sigma.
     405    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
     406     well_formed_state_pc p p' graph_prog sigma gss s →
     407      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
     408
     409 λp,p',graph_prog,sigma,gss,s,prf.
     410 let pc' ≝ sigma_pc … (proj1 … prf) in
     411 let st' ≝ sigma_state … (proj2 … prf) in
     412 mk_state_pc ? st' pc'.
     413
     414(*
     415lemma sigma_pc_commute:
     416 ∀p,p',graph_prog,sigma,gss,st.
     417 ∀prf : well_formed_state_pc p p' graph_prog sigma gss st.
     418 sigma_pc … (pc ? st) (proj1 … prf) =
     419 pc ? (sigma_state_pc … st prf). // qed.
     420*)
     421
     422lemma res_eq_from_opt :
     423  ∀A,m,v.res_to_opt A m = return v → m = return v.
     424#A * #x #v normalize #EQ destruct % qed.
    209425
    210426lemma if_of_function_commute:
     
    358574*)
    359575
    360 lemma int_funct_of_block_transf_commute:
     576lemma int_funct_of_block_transf:
    361577 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ.
    362578  ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf.
     
    393609 >(sigma_pblock_eq_lemma … prf) #H
    394610 lapply (opt_eq_from_res ???? H) -H #H
    395  >(int_funct_of_block_transf_commute ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
     611 >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
    396612 //
    397613qed.
     
    457673qed. *)
    458674
     675lemma opt_Exists_elim:
     676 ∀A:Type[0].∀P:A → Prop.
     677  ∀o:option A.
     678   opt_Exists A P o →
     679    ∃v:A. o = Some … v ∧ P v.
     680 #A #P * normalize /3/ *
     681qed.
     682
     683
    459684lemma stmt_at_sigma_commute:
    460685 ∀p,graph_prog,graph_fun,lbl,pt.
     
    470695    (joint_if_code ?? (if_of_function ?? lin_fun))
    471696    pt = return (graph_to_lin_statement … stmt). 
    472  #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf
    473  (*
     697 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt
     698cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun)))
     699#sigma_entry_is_zero #lin_stmt_spec
     700lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 *
     701#EQlookup_stmt1 #H
     702elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt
     703* #EQnth_opt_graph_stmt normalize nodelta
     704* #optEQlbl_optlbl_graph_stmt #next_spec
     705whd in match (stmt_at ????) in ⊢ (% → ?);
     706normalize nodelta
     707>EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ)
     708whd in match (stmt_at ????); > EQnth_opt_graph_stmt
     709normalize nodelta elim  optEQlbl_optlbl_graph_stmt #_ #EQ >EQ //
     710qed.
     711(*
     712
     713 >(if_of_function_commute … graph_fun)
     714
     715check opt_Exists
     716check linearise_int_fun
     717check
    474718 whd in match (stmt_at ????);
    475719 whd in match (stmt_at ????);
     
    486730 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
    487731 <sigma_pc_commute >lin_lookup_ok // *)
    488  cases daemon
    489 qed.
    490732
    491733lemma fetch_statement_sigma_commute:
     
    516758qed.
    517759
     760lemma point_of_pc_sigma_commute :
     761 ∀p,p',graph_prog.
     762 let lin_prog ≝ linearise p graph_prog in
     763 ∀sigma,pc,fn,n.
     764  ∀prf : well_formed_pc p p' graph_prog sigma pc.
     765 int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return fn →
     766 sigma fn (point_of_pc ? (make_sem_graph_params p p') pc) = return n →
     767 point_of_pc ? (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
     768#p #p' #graph_prog #sigma #pc #fn #n #prf #EQfetch #EQsigma
     769whd in match sigma_pc; normalize nodelta
     770@opt_safe_elim #pc' whd in match sigma_pc_opt;
     771normalize nodelta >EQfetch >m_return_bind >EQsigma
     772>m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ)
     773change with (point_of_offset ??? = ?) @point_of_offset_of_point
     774qed.
     775
    518776definition linearise_status_rel:
    519777 ∀p,p',graph_prog.
     
    523781  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    524782    ? graph_prog stack_sizes in
    525  ∀sigma.
     783 ∀sigma,gss.
    526784 good_sigma p graph_prog sigma →
    527785   status_rel
    528786    (graph_abstract_status p p' graph_prog stack_sizes')
    529787    (lin_abstract_status p p' lin_prog stack_sizes)
    530  ≝ λp,p',graph_prog,stack_sizes,sigma,good.
     788 ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good.
    531789   mk_status_rel …
    532790    (* sem_rel ≝ *) (λs1,s2.
    533      ∃prf: well_formed_status p p' graph_prog sigma s1.
    534       s2 = sigma_state … s1 prf)
     791     ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1.
     792      s2 = sigma_state_pc … s1 prf)
    535793    (* call_rel ≝ *) (λs1,s2.
    536       ∃prf:well_formed_status p p' graph_prog sigma s1.
     794      ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1.
    537795      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
    538796    (* sim_final ≝ *) ?.
     
    544802#res #_
    545803#H lapply (res_eq_from_opt ??? H) -H
    546 #H elim (bind_inversion ????? H)
     804cases daemon
     805(*#H elim (bind_inversion ????? H) in ⊢ ?;
    547806* #f #stmt *
    548 whd in ⊢ (??%?→?);
    549 cases daemon
     807whd in ⊢ (??%?→?);*)
    550808qed.
    551 
    552 (* To be added to common/Globalenvs, it strenghtens
    553    find_funct_ptr_transf *)
    554 (*   
    555 lemma
    556   find_funct_ptr_transf_eq:
    557     ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
    558     ∀b: block.
    559     find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b =
    560      m_map ???
    561       (transf …)
    562       (find_funct_ptr ? (globalenv … iV p) b).
    563  #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%);
    564  [ cases daemon (* TODO in Globalenvs.ma *)
    565  | #f #H >(find_funct_ptr_transf A B … H) // ]
    566 qed.
    567 *)
    568 
    569 
    570 (*lemma fetch_function_sigma_commute:
    571  ∀p,p',graph_prog,sigma,st1.
    572  ∀prf:well_formed_status ??? sigma st1.
    573  let lin_prog ≝ linearise ? graph_prog in
    574   fetch_function               
    575    (lin_prog_params p p' lin_prog)
    576    (globals (lin_prog_params p p' lin_prog))
    577    (ev_genv (lin_prog_params p p' lin_prog))
    578    (pc (lin_prog_params p p' lin_prog)
    579     (linearise_status_fun p p' graph_prog sigma st1 prf))
    580  =
    581   m_map …
    582    (linearise_int_fun ??)
    583    (fetch_function
    584     (graph_prog_params p p' graph_prog)
    585     (globals (graph_prog_params p p' graph_prog))
    586     (ev_genv (graph_prog_params p p' graph_prog))
    587     (pc (graph_prog_params p p' graph_prog) st1)).
    588 #p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta
    589 whd in match function_of_block; normalize nodelta
    590 >(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …)
    591 cases (find_funct_ptr ???) // * //
    592 qed.
    593 *)
    594809
    595810lemma IO_bind_inversion:
     
    603818] qed.
    604819
    605 lemma opt_Exists_elim:
    606  ∀A:Type[0].∀P:A → Prop.
    607   ∀o:option A.
    608    opt_Exists A P o →
    609     ∃v:A. o = Some … v ∧ P v.
    610  #A #P * normalize /3/ *
    611 qed.
     820lemma err_eq_from_io : ∀O,I,X,m,v.
     821  err_to_io O I X m = return v → m = return v.
     822#O #I #X * #x #v normalize #EQ destruct % qed.
     823
     824lemma eval_seq_no_pc_sigma_commute :
     825 ∀p,p',graph_prog.
     826 let lin_prog ≝ linearise p graph_prog in
     827 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     828 let stack_sizes' ≝
     829  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     830    ? graph_prog stack_sizes in
     831 ∀sigma.∀gss : good_sigma_state … graph_prog sigma.
     832 ∀fn,st,stmt,st'.
     833 ∀prf : well_formed_state … gss st.∀prf'.
     834  eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes'))
     835   fn st stmt = return st' →
     836  eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes))
     837    (sigma_function_name … fn) (sigma_state … gss st prf) stmt =
     838  return sigma_state … gss st' prf'.
     839  #p #p' #graph_prog #stack_sizes #sigma #gss
     840  #fn #st #stmt
     841  #st' #prf #prf'
     842  cases daemon (*
     843  whd in match eval_seq_no_pc;
     844  cases stmt normalize nodelta
     845  [1,2: #_ #EQ whd in EQ : (??%%); destruct(EQ) //
     846  | #mv_sig whd in match pair_reg_move in ⊢ (%→?); normalize nodelta     
     847    #H
     848  ] *)
     849qed.       
    612850       
    613851inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    614852    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
    615853(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
    616 
    617 lemma err_eq_from_io : ∀O,I,X,m,v.
    618   err_to_io O I X m = return v → m = return v.
    619 #O #I #X * #x #v normalize #EQ destruct % qed.
    620854
    621855lemma linearise_ok:
     
    626860  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    627861    ? graph_prog lin_stack_sizes in
     862 (∀sigma.good_sigma_state p p' graph_prog sigma) →
    628863   ex_Type1 … (λR.
    629864   status_simulation
     
    633868 cases (linearise_spec … graph_prog) #sigma #good
    634869 #lin_stack_sizes
    635  %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)}
    636  whd whd in ⊢ (%→%→?);
    637  change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?)
    638  #st1
    639  change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?)
    640  #st1'
    641  change with (∀st : state_pc (p' (joint_closed_internal_function (mk_lin_params ?))).?)
    642  #st2
    643  #ex * #wfprf #rel_st1_st2
    644  whd in ex;
    645  change with
    646   (eval_state
    647     (make_sem_graph_params p p')
    648     (prog_var_names ?? graph_prog)
    649      ?
    650     st1 = ?) in ex;
    651  whd in match eval_state in ex;
    652  normalize nodelta in ex;
    653  cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt
    654  change with (Σi.is_internal_function_of_program … graph_prog i) in fn; *
    655  change with (globalenv_noinit ? graph_prog) in
    656   ⊢ (??(???%?)?→?);
    657     match (ge ?? (ev_genv ?)) in ⊢ (%→?);
    658  st1'
     870 #gss lapply (gss sigma) -gss #gss
     871 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma gss good)}
     872whd in match graph_abstract_status;
     873whd in match lin_abstract_status;
     874whd in match graph_prog_params;
     875whd in match lin_prog_params;
     876normalize nodelta
     877whd
     878whd in ⊢ (%→%→%→?);
     879whd in ⊢ (?(?%)→?(?%)→?(?%)→?);
     880whd in ⊢ (?%→?%→?%→?);
     881#st1 #st1' #st2
     882whd in ⊢ (%→?);
     883change with
     884  (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
     885whd in match eval_state in ⊢ (%→?); normalize nodelta
     886change with (Σi.is_internal_function_of_program ? graph_prog i) in
     887match (Sig ??) in ⊢ (%→?);
     888letin globals ≝ (prog_var_names ?? graph_prog)
     889change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in
     890  match (fetch_statement ?????) in ⊢ (%→?);
     891#ex
     892cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex
     893#EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch
     894#EQfetch
     895cases (bind_inversion ????? EQfetch)
     896#f_id * #H lapply (opt_eq_from_res ???? H) -H
     897#EQfunc_of_block
     898#H elim (bind_inversion ????? H) -H #stmt' *
     899#H lapply (opt_eq_from_res ???? H) -H #EQstmt_at
     900whd in ⊢ (??%%→?); #EQ destruct(EQ)
     901#EQeval
     902cases (good fn (pi2 … (sigma_function_name p graph_prog fn)))
     903letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at
     904#entry_0
     905#good_local
     906* * #wf_pc #wf_state #EQst2
     907generalize in match wf_pc in ⊢ ?;
     908whd in ⊢ (%→?);
     909inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ]
     910#lin_pc
     911whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta
     912>EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?);
     913#H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt *
     914#EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_
     915elim (good_local … EQsigma) -good_local
     916#stmt' *
     917change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?)
     918>EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
     919#H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta
     920>(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ]
     921change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?);
     922letin lin_fun ≝ (\fst  (linearise_int_fun p globals graph_fun))
     923change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?);
     924*
     925#EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec
     926letin lin_prog ≝ (linearise … graph_prog)
     927lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
     928destruct(EQst2)
     929whd in match eval_state in ⊢ (???%→?); normalize nodelta
     930letin st2 ≝ (sigma_state_pc ????? st1 ?)
     931>(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?);
     932>m_return_bind in ⊢ (%→?);
     933#ex'
     934(* resolve classifier *)
    659935whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    660 >fetch_statement_spec in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     936>EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     937normalize nodelta
     938cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex';
     939[ *
     940  [ #stmt #nxt
     941    whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
     942    #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
     943    whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
     944    whd in match eval_statement in ⊢ (%→?); normalize nodelta
     945    elim (IO_bind_inversion ??????? EQeval) #st1_no_pc *
     946    #EQeval_no_pc #EQeval_pc
     947    >(eval_seq_no_pc_sigma_commute … EQeval_no_pc)
     948    [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ]
     949        >m_return_bind
     950    cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec;
     951    [14: #f #args #dest
     952    | #c
     953    | #lbl
     954    | #move_sig
     955    | #a
     956    | #a
     957    | #sy #sy_prf #dpl #dph
     958    | #op #a #b #arg1 #arg2
     959    | #op #a #arg
     960    | #op #a #arg1 #arg2
     961    ||
     962    | #a #dpl #dph
     963    | #dpl #dph #a
     964    | #s_ext
     965    ]
     966    [ (* CALL *)
     967    |(*:*)
     968      normalize nodelta
     969      #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec
     970      whd in match eval_seq_pc; normalize nodelta
     971      #ex1
     972      cases next_spec
     973      [ #EQnext_sigma
     974        %[2: %{(taaf_step … (taa_base …) ex1 ?)}
     975         [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|]
     976        normalize nodelta
     977        cut (? : Prop) [3: #R' % [ %{I R'} ] |*:]
     978        [ cases daemon (* TODO lemma joint_label_sigma_commute *)
     979        | %
     980          [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon
     981          | whd in match eval_seq_pc in EQeval_pc;
     982            whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?);
     983            destruct (EQeval_pc)
     984            whd in ⊢ (??%%);
     985            change with (sigma_pc ??????) in match
     986              (pc ? (sigma_state_pc ???????));
     987            whd in match (succ_pc ????) in ⊢ (??%%);
     988            whd in match (point_of_succ ???) in ⊢ (??%%);
     989            >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma)
     990            whd in match sigma_pc in ⊢ (???%);
     991            whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta
     992            @opt_safe_elim #pc'
     993            >EQfunc_of_block >m_return_bind
     994            whd in match point_of_pc; normalize nodelta
     995            >point_of_offset_of_point
     996            >EQnext_sigma whd in ⊢ (??%?→?);
     997            whd in match pc_of_point; normalize nodelta
     998            #EQ destruct(EQ)
     999            >sigma_pblock_eq_lemma %
     1000          ]
     1001        ]
     1002      | -next_spec #next_spec
     1003        %
     1004     
     1005     
     1006        whd in ⊢ (?→???%→?);
     1007        generalize in ⊢ (??%? → ???(????%) → ?); |*: skip]  | #a #lbltrue #next
     1008  ] #next change with label in next;
     1009| *
     1010  [ #lbl
     1011  |
     1012  | #fl #f #args
     1013  ]
     1014]
     1015whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
     1016#EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
     1017normalize nodelta
     1018whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
     1019whd in match eval_statement in ⊢ (%→?); normalize nodelta
     1020[ >m_return_bind in ⊢ (%→?);
     1021  >m_return_bind in EQeval;
     1022
     1023
     1024
     1025  (* common for all non-call seq *)
     1026  >m_return_bind in ⊢ (%→?);
     1027  whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1028  >m_return_bind in ⊢ (%→?);
     1029
     1030 
     1031  #ex1
     1032lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
     1033
     1034whd in match (point_of_pc ???);
     1035whd in match (point_of_succ ???);
     1036whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim
     1037#pc' #H
     1038elim (bind_opt_inversion ????? H) #fn * #EQbl
     1039-H #H 
     1040elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?);
     1041#EQ destruct(EQ)
     1042whd in match (succ_pc ????);
     1043whd in match (point_of_succ ???);
     1044change with (point_of_offset ???) in match (point_of_pc ???);
     1045>point_of_offset_of_point
     1046whd in match sigma_pc; normalize nodelta @opt_safe_elim
     1047#pc' whd in match sigma_pc_opt; normalize nodelta
     1048
     1049 
     1050 
     1051        whd in match (succ_pc ????);
     1052               
     1053        change with next in match (offset_of_point ???) in ⊢ (???%);
    6611054whd in fetch_statement_spec : (??()%);
    6621055cases cl in classified_st1_cl; -cl #classified_st1_cl whd
     
    6761069   letin st2_opt' ≝ (eval_state …
    6771070               (ev_genv (lin_prog_params … lin_prog lin_stack_sizes))
    678                (sigma_state … wf_st1))
     1071               (sigma_state_pc … wf_st1))
    6791072   cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2')
    6801073   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
     
    6951088 | ....
    6961089qed.
     1090
     1091
     1092
     1093
     1094
     1095[ *
     1096  [ *
     1097    [ letin C_COMMENT ≝ 0 in ⊢ ?; #c
     1098    | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl
     1099    | letin C_MOVE       ≝ 0 in ⊢ ?; #move_sig
     1100    | letin C_POP        ≝ 0 in ⊢ ?; #a
     1101    | letin C_PUSH       ≝ 0 in ⊢ ?; #a
     1102    | letin C_ADDRESS    ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph
     1103    | letin C_OPACCS     ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2
     1104    | letin C_OP1        ≝ 0 in ⊢ ?; #op #a #arg
     1105    | letin C_OP2        ≝ 0 in ⊢ ?; #op #a #arg1 #arg2
     1106    | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?;
     1107    | letin C_SET_CARRY  ≝ 0 in ⊢ ?;
     1108    | letin C_LOAD       ≝ 0 in ⊢ ?; #a #dpl #dph
     1109    | letin C_STORE      ≝ 0 in ⊢ ?; #dpl #dph #a
     1110    | letin C_CALL       ≝ 0 in ⊢ ?; #f #args #dest
     1111    | letin C_EXT        ≝ 0 in ⊢ ?; #s_ext
     1112    ]
     1113  | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue
     1114  ] #next change with label in next;
     1115| *
     1116  [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl
     1117  | letin C_RETURN ≝ 0 in ⊢ ?;
     1118  | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args
     1119  ]
     1120]
Note: See TracChangeset for help on using the changeset viewer.