Changeset 2476 for src/joint


Ignore:
Timestamp:
Nov 19, 2012, 6:04:24 PM (9 years ago)
Author:
piccolo
Message:

fixed commutation lemmas in lineariseProof
started proof of main theorem in lineariseProof

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/joint/lineariseProof.ma

    r2467 r2476  
    1818include "joint/semanticsUtils.ma".
    1919
    20 definition good_local_sigma :
    21   ∀p:unserialized_params.
    22   ∀p':(∀F.sem_unserialized_params p F).
    23   ∀globals.
    24   joint_closed_internal_function (mk_graph_params p) globals →
    25   (label → option ℕ) → Prop ≝
    26   λp,p',globals,graph_fun,sigma.
    27    let lin_fun ≝ linearise_int_fun … graph_fun in
    28    let g ≝ joint_if_code ?? (pi1 … graph_fun) in
    29    let c ≝ joint_if_code ?? (pi1 … lin_fun) in
    30    ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
    31         code_closed … c ∧
    32         sigma entry = Some ? 0 ∧
    33         ∀l,n.sigma l = Some ? n →
    34           lt n 2^offset_size →
    35           ∃s. lookup … g l = Some ? s ∧
    36             opt_Exists ?
    37               (λls.let 〈lopt, ts〉 ≝ ls in
    38                 opt_All ? (eq ? l) lopt ∧
    39                 ts = graph_to_lin_statement … s ∧
    40                 opt_All ?
    41                   (λnext.Or (sigma next = Some ? (S n))
    42                   (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    43                   (stmt_implicit_label … s)) (nth_opt … n c).
    44 
    45 axiom prog_if_of_function :
    46   ∀p.∀prog : joint_program p.
    47   (Σi.is_internal_function_of_program … prog i) →
    48     joint_closed_internal_function p (prog_var_names … prog).
    49 
    50 definition if_in_global_env_to_if_in_prog :
    51   ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i.
    52   Σi.is_internal_function_of_program ? (prog prog_pars) i ≝
    53   λprog_pars,f.pi1 ?? f.
    54 @is_internal_function_of_program_ok @(pi2 … f) qed.
    55 
     20
     21lemma ok_is_internal_function_of_program_noinit :
     22  ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.∀i.
     23  is_internal_function_of_program … prog i →
     24  is_internal_function ? (globalenv_noinit ? prog) i ≝
     25 λA,prog.ok_is_internal_function_of_program … prog.
     26
     27lemma is_internal_function_of_program_ok_noinit :
     28  ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.∀i.
     29  is_internal_function ? (globalenv_noinit ? prog) i →
     30  is_internal_function_of_program … prog i ≝
     31  λA,prog.is_internal_function_of_program_ok … prog.
     32
     33definition if_in_global_env_to_if_in_prog_noinit :
     34  ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.
     35  (Σi.is_internal_function ? (globalenv_noinit ? prog) i) →
     36  Σi.is_internal_function_of_program ?? prog i ≝
     37  λA,prog,f.«f, is_internal_function_of_program_ok_noinit … (pi2 … f)».
     38
     39(*
    5640coercion if_in_prog_from_if_in_global_env nocomposites :
    57   ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i.
    58   Σi.is_internal_function_of_program ? (prog prog_pars) i ≝
    59   if_in_global_env_to_if_in_prog
    60   on _f : Sig ident (λi.is_internal_function ??? i)
    61   to Sig ident (λi.is_internal_function_of_program ?? i).
    62 
    63 definition good_sigma :
    64   ∀p:unserialized_params.
    65   ∀p':(∀F.sem_unserialized_params p F).
    66   ∀prog : joint_program (mk_graph_params p).
    67   ((Σi.is_internal_function_of_program … prog i) → label → option ℕ) → Prop ≝
    68   λp,p',graph_prog,sigma.
    69   ∀i.
    70   let graph_fun ≝ prog_if_of_function ?? i in
    71   let sigma_local ≝ sigma i in
    72   good_local_sigma ? p' ? graph_fun sigma_local.
     41  ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.
     42  ∀f:Σi.is_internal_function ? (globalenv_noinit ? prog) i.
     43  Σi.is_internal_function_of_program ?? prog i ≝
     44  if_in_global_env_to_if_in_prog_noinit
     45  on _f : Sig ident (λi.is_internal_function ?? i)
     46  to Sig ident (λi.is_internal_function_of_program ??? i).
     47*)
    7348
    7449definition graph_prog_params ≝
    … …  
    10075 joint_abstract_status (lin_prog_params ? p' prog stack_sizes).
    10176
     77(*
     78axiom P :
     79  ∀A,B,prog.A (prog_var_names (λvars.fundef (A vars)) B prog) → Prop.
     80
     81check (λpars.let pars' ≝ make_global pars in λx :joint_closed_internal_function pars' (globals pars'). P … x)
     82(*
     83unification hint 0 ≔ p, prog, stack_sizes ;
     84pars ≟ mk_prog_params p prog stack_sizes ,
     85pars' ≟ make_global pars,
     86A ≟ λvars.joint_closed_internal_function p vars,
     87B ≟ ℕ
     88⊢
     89A (prog_var_names (λvars.fundef (A vars)) B prog) ≡
     90joint_closed_internal_function pars' (globals pars').
     91*)
     92axiom T : ∀A,B,prog.genv_t (fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) B prog))) → Prop.
     93(*axiom Q : ∀A,B,init,prog.
     94 T … (globalenv (λvars:list ident.fundef (A vars)) B
     95  init prog) → Prop.
     96
     97lemma pippo :
     98  ∀p,p',prog,stack_sizes.
     99  let pars ≝ graph_prog_params p p' prog stack_sizes in
     100  let ge ≝ ev_genv pars in T ?? prog ge → Prop.
     101 
     102  #H1 #H2 #H3 #H4
     103   #H5
     104  whd in match (ev_genv ?) in H5;               
     105  whd in match (globalenv_noinit) in H5; normalize nodelta in H5;
     106  whd in match (prog ?) in H5;
     107  whd in match (joint_function ?) in H5;
     108  @(Q … H5)
     109 λx:T ??? ge.Q ???? x)
     110*)
     111axiom Q : ∀A,B,init,prog,i.
     112is_internal_function
     113 (A
     114  (prog_var_names (λvars:list ident.fundef (A vars)) B
     115   prog))
     116 (globalenv (λvars:list ident.fundef (A vars)) B
     117  init prog)
     118 i → Prop.
     119
     120check
     121  (λp,p',prog,stack_sizes,i.
     122  let pars ≝ graph_prog_params p p' prog stack_sizes in
     123  let ge ≝ ev_genv pars in
     124 λx:is_internal_function (joint_closed_internal_function pars (globals pars))
     125  ge i.Q ??? prog ? x)
     126*)
     127
    102128definition sigma_pc_opt:
    103129 ∀p,p',graph_prog,stack_sizes.
    104130  ((Σi.is_internal_function_of_program … graph_prog i) →
    105131    code_point (mk_graph_params p) → option ℕ) →
    106    cpointer → option cpointer
     132   program_counter → option program_counter
    107133 ≝
    108134  λp,p',prog,stack_sizes,sigma,pc.
    109135  let pars ≝ graph_prog_params p p' prog stack_sizes in
    110136  let ge ≝ ev_genv pars in
    111   ! f ← int_funct_of_block ?? ge (pblock pc) ;
    112   ! lin_point ← sigma f (point_of_pointer … pars pc) ;
    113   res_to_opt … (pointer_of_point ? (make_sem_lin_params ? p') pc lin_point).
     137  ! f ← int_funct_of_block ? ge (pc_block pc) ;
     138  ! lin_point ← sigma (pi1 … f) (point_of_pc ? pars pc) ;
     139  return pc_of_point ? (make_sem_lin_params ? p') pc lin_point.
     140  @(is_internal_function_of_program_ok … prog … (pi2 … f))
     141qed.
    114142
    115143definition well_formed_pc:
    … …  
    117145  ((Σi.is_internal_function_of_program … graph_prog i) →
    118146    label → option ℕ) →
    119    cpointer → Prop
     147   program_counter → Prop
    120148 ≝
    121149 λp,p',prog,stack_sizes,sigma,pc.
    … …  
    165193∀pc.
    166194∀prf : well_formed_pc p p' graph_prog stack_sizes sigma pc.
    167 cpointer ≝
     195program_counter ≝
    168196λp,p',graph_prog,stack_sizes,sigma,st.opt_safe ….
    169197 
    … …  
    205233#A * #x #v normalize #EQ destruct % qed.
    206234
    207 lemma if_propagate :
    208 ∀pars_in, pars_out : sem_params.
    209 ∀trans : ∀globals.joint_closed_internal_function pars_in globals →
    210                   joint_closed_internal_function pars_out globals.
    211 ∀prog_in : program (joint_function pars_in) ℕ.
    212 let prog_out ≝
    213   transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
    214 ∀i.is_internal_function_of_program … prog_in i →
    215 is_internal_function_of_program … prog_out i.
    216 cases daemon (* TODO by paolo *) qed.
    217 
    218 definition stack_sizes_lift :
    219 ∀pars_in, pars_out : sem_params.
    220 ∀trans : ∀globals.joint_closed_internal_function pars_in globals →
    221                   joint_closed_internal_function pars_out globals.
    222 ∀prog_in : program (joint_function pars_in) ℕ.
    223 let prog_out ≝
    224   transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
    225 ((Σi.is_internal_function_of_program … prog_out i) → ℕ) →
    226 ((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝
    227 λpars_in,pars_out,prog_in,trans,stack_sizes.
    228 λi.stack_sizes «i, if_propagate … (pi2 … i)».
    229 
    230 axiom ok_is_internal_function_of_program :
    231   ∀p.∀prog:joint_program p.∀i.
    232   is_internal_function_of_program p prog i →
    233   is_internal_function ?? (globalenv_noinit ? prog) i.
    234 
    235 
    236235definition sigma_function_name :
    237236 ∀p,p',graph_prog.
    … …  
    244243  (Σf.is_internal_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) f) ≝
    245244λp,p',graph_prog,lin_stack_sizes,f.pi1 … f.
    246 @ok_is_internal_function_of_program
    247 @(if_propagate (make_sem_graph_params p p') (make_sem_lin_params p p'))
    248 @is_internal_function_of_program_ok
    249 @(pi2 … f)
    250 qed.
    251 
     245@(ok_is_internal_function_of_program ??? (linearise … graph_prog) ??)
     246@if_propagate
     247@is_internal_function_of_program_ok [2: @(pi2 … f) |]
     248qed.
    252249
    253250lemma if_of_function_commute:
    254  ∀p,p',graph_prog,stack_sizes.
    255  ∀graph_fun.
    256  let graph_fd ≝ if_of_function ??? graph_fun in
    257  let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
     251 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).∀stack_sizes.
     252 ∀graph_fun,prf.
     253 let graph_fd ≝ if_of_function ? (globalenv_noinit … graph_prog) graph_fun in
     254 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes «graph_fun, prf» in
    258255 let lin_fd ≝ if_of_function … lin_fun in
    259  lin_fd = linearise_int_fun … graph_fd.
    260 (* usare match_opt_prf_elim ? *)
    261 cases daemon qed.
     256 lin_fd = \fst (linearise_int_fun ?? graph_fd).
     257 #p #p' #graph_prog #stack_sizes #graph_fun #prf whd
     258(* Old comment? usare match_opt_prf_elim ? *)
     259cases daemon (* Job for Paolo *) qed.
    262260
    263261lemma bind_opt_inversion:
    … …  
    277275 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    278276    ? graph_prog lin_stack_sizes in
    279 ∀sigma,st.
    280 ∀prf : well_formed_status p p' graph_prog graph_stack_sizes sigma st.
    281  pblock (sigma_pc ? p' graph_prog graph_stack_sizes sigma (pc ? st) (proj1 … prf)) =
    282  pblock (pc ? st).
    283  #p #p' #graph_prog #stack_sizes #sigma #st #prf
     277∀sigma,pc.
     278∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
     279 pc_block (sigma_pc ? p' graph_prog graph_stack_sizes sigma pc prf) =
     280 pc_block pc.
     281 #p #p' #graph_prog #stack_sizes #sigma #pc #prf
    284282 whd in match sigma_pc; normalize nodelta
    285283 @opt_safe_elim #x #x_spec
    286  whd in x_spec:(??%?); cases (int_funct_of_block ????) in x_spec;
     284 whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec;
    287285 normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H
    288  #offset * #_ whd in ⊢ (??%? → ?); whd in match pointer_of_point; normalize nodelta
    289  cases (opt_to_res ???) [2: #msg #abs normalize in abs; destruct]
    290  #offset_lin whd in ⊢ (??%? → ?); #EQ destruct //
    291 qed.
     286 #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct //
     287qed.
     288
     289lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B.
     290(! x ← m ; g x) ≠ None ? → m ≠ None ?.
     291#A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize 
     292[ #abs elim abs -abs #abs @abs %
     293| #abs elim abs -abs #abs #v @abs %
     294]
     295qed.
     296
     297lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A.
     298∀ b : B .∀ f : A → B. ∀g : B → option C.
     299g (match m with [None  ⇒ b  | Some  x ⇒ f x])≠ None ? →  g b = None ? → m ≠ None ?.
     300#A #B #C #m #x #b  #f #g #H1 #H2 % #m_eq_none >m_eq_none in H1; normalize #H elim H -H #H @H assumption
     301qed.
     302
     303axiom int_funct_of_block_transf_commute:
     304 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ.
     305  ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf.
     306   let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
     307     int_funct_of_block ? (globalenv_noinit … progr) bl = return f →
     308     int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf».
    292309
    293310lemma fetch_function_sigma_commute :
    … …  
    298315  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    299316    ? graph_prog lin_stack_sizes in
    300  ∀sigma,st,f.
    301   ∀prf : well_formed_status p p' graph_prog graph_stack_sizes sigma st.
    302   let pc_st ≝ pc ? st in
     317 ∀sigma,pc_st,f.
     318  ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc_st.
    303319 fetch_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc_st =
    304320  return f
    305 → fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) (sigma_pc … pc_st (proj1 … prf)) =
     321→ fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes))
     322 (sigma_pc … pc_st prf) =
    306323  return sigma_function_name … f.
    307324 #p #p' #graph_prog #stack_sizes #sigma #st #f #prf
    308  >(sigma_pc_commute … prf)
    309 whd in match fetch_function; normalize nodelta
    310 >(sigma_pblock_eq_lemma … prf) #H
    311 lapply (opt_eq_from_res ???? H) -H
    312 whd in match int_funct_of_block in ⊢ (%→?); normalize nodelta
    313 
    314 XXXX ENTRARE IN PRF CHE C'E' FUNCT OF BLOCK XXXX
    315 
     325 whd in match fetch_function; normalize nodelta
     326 >(sigma_pblock_eq_lemma … prf) #H
     327 lapply (opt_eq_from_res ???? H) -H #H
     328 >(int_funct_of_block_transf_commute ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
     329 //
     330qed.
     331 
     332(*
    316333#H elim (bind_opt_inversion ????? H) -H
    317334#x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta
    … …  
    369386#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
    370387-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
    371 destruct // *)
     388destruct //
    372389cases daemon
    373 qed.
     390qed. *)
    374391
    375392lemma stmt_at_sigma_commute:
    376  ∀p,p',graph_prog,stack_sizes,graph_fun,lbl.
     393 ∀p,p',graph_prog,stack_sizes,graph_fun,prf2,lbl,pt.
    377394 let lin_prog ≝ linearise ? graph_prog in
    378395 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
    379  ∀sigma.good_sigma p p' graph_prog sigma →
    380  ∀prf:sigma graph_fun lbl ≠ None ….
    381  ∃stmt.
     396 ∀sigma.good_sigma p graph_prog sigma →
     397 sigma «pi1 … graph_fun,prf2» lbl = return pt →
     398 ∀stmt.
    382399   stmt_at …
    383     (joint_if_code ?? (if_of_function ??? graph_fun)) 
    384     lbl = Some ? stmt ∧
    385    stmt_at …
    386     (joint_if_code ?? (if_of_function ??? lin_fun))
    387     (opt_safe … (sigma graph_fun lbl) prf) = Some ? (graph_to_lin_statement … stmt). 
    388  #p #p' #graph_prog #stack_sizes #graph_fun #lbl #sigma #good #prf
    389  @opt_safe_elim -prf #n #prf
     400    (joint_if_code ?? (if_of_function ?? graph_fun)) 
     401    lbl = return stmt →
     402   stmt_at ??
     403    (joint_if_code ?? (if_of_function ?? lin_fun))
     404    pt = return (graph_to_lin_statement … stmt). 
     405 #p #p' #graph_prog #stack_sizes #graph_fun #prf2 #lbl #pt #sigma #good #prf
     406 #prf
    390407 (*
    391408 whd in match (stmt_at ????);
    … …  
    412429   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    413430    ? graph_prog lin_stack_sizes in
    414   ∀sigma.good_sigma p p' graph_prog sigma →
     431  ∀sigma.good_sigma p graph_prog sigma →
    415432  ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
    416433  fetch_statement ? (make_sem_graph_params p p') … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc =
    … …  
    419436   (sigma_pc … pc prf) =
    420437    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
    421  #p #p' #graph_prog #stack_sizes #pc #fn #stmt #good #prf
    422 (* @opt_safe_elim -prf #n #prf
    423  whd in match fetch_statement; normalize nodelta
    424  >fetch_function_sigma_commute
    425  cases (fetch_function ????) [2://]
    426  #graph_fun whd in ⊢ (??%%);
    427  whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
    428  >stm_at_sigma_commute cases (stmt_at ????) // *)
    429 cases daemon
     438 #p #p' #graph_prog #stack_sizes #pc #fn #stmt #sigma #good #wfprf
     439 whd in match fetch_statement; normalize nodelta #H
     440 cases (bind_inversion ????? H) #id * -H #H
     441 >(fetch_function_sigma_commute … wfprf … H) -H >m_return_bind
     442 #H cases (bind_inversion ????? H) #fstmt * -H #H
     443 lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct
     444 >(stmt_at_sigma_commute … good … H)
     445 [3: @is_internal_function_of_program_ok [2: @(pi2 … fn)|]
     446 |2: cases daemon (* TO BE DONE, COMMUTATION LEMMA NEEDED *) ]
     447 %
    430448qed.
    431449
    … …  
    438456    ? graph_prog stack_sizes in
    439457 ∀sigma.
    440  good_sigma p p' graph_prog sigma →
     458 good_sigma p graph_prog sigma →
    441459   status_rel
    442460    (graph_abstract_status p p' graph_prog stack_sizes')
    … …  
    509527qed.
    510528*)
     529
     530lemma IO_bind_inversion:
     531  ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
     532  (! x ← f ; g x = return y) →
     533  ∃x. (f = return x) ∧ (g x = return y).
     534#O #I #A #B #f #g #y cases f normalize
     535[ #o #f #H destruct
     536| #a #e %{a} /2 by conj/
     537| #m #H destruct (H)
     538] qed.
     539
     540lemma opt_Exists_elim:
     541 ∀A:Type[0].∀P:A → Prop.
     542  ∀o:option A.
     543   opt_Exists A P o →
     544    ∃v:A. o = Some … v ∧ P v.
     545 #A #P * normalize /3/ *
     546qed.
    511547       
    512548inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    513549    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
    514 interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).
     550(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
     551
    515552
    516553lemma linearise_ok:
    … …  
    521558  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    522559    ? graph_prog lin_stack_sizes in
    523    ∃R.
     560   ex_Type1 … (λR.
    524561   status_simulation
    525562    (graph_abstract_status p p' graph_prog graph_stack_sizes)
    526     (lin_abstract_status p p' lin_prog lin_stack_sizes) R.
     563    (lin_abstract_status p p' lin_prog lin_stack_sizes) R).
    527564 #p #p' #graph_prog
    528  cut (∃sigma.good_sigma p p' graph_prog sigma)
    529  [ cases daemon (* TODO by Paolo *) ] * #sigma #good
     565 cases (linearise_spec … graph_prog) #sigma #good
    530566 #lin_stack_sizes
    531567 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)}
    532568 whd
    533 #st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl
     569#st1 #cl #st1' #st2 #move_st1_st1' * #wf_st1 #rel_st1_st2 #classified_st1_cl
     570whd in move_st1_st1'; whd in match eval_state in move_st1_st1':(??%?);
     571normalize nodelta in move_st1_st1';
     572cases (IO_bind_inversion ??????? move_st1_st1') * #fn #stmt *
     573#fetch_statement_spec -move_st1_st1' #move_st1_st1'
    534574cases cl in classified_st1_cl; -cl #classified_st1_cl whd
    535575[4:
    536  cases rel_st1_st2 -rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 -st2
    537  whd in move_st1_st1';
    538  letin lin_prog ≝ (linearise ? graph_prog)
    539 
    540  cut (joint_closed_internal_function (mk_graph_params p) (globals (graph_prog_params p p' graph_prog))) [cases daemon (*???*)] #graph_fun
    541 
    542  cases (linearise_code_spec … p' graph_prog graph_fun
    543          (joint_if_entry … graph_fun))     
    544  * #lin_code_closed #sigma_entry_is_zero #sigma_spec
    545  lapply (sigma_spec
    546          (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … st1)))
    547  -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … wf_st1) |2: skip ]
    548  -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec whd in sigma_spec;
    549  inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
    550  * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
     576 >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog)
     577 cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ]
     578 #sigma_entry_is_zero #sigma_spec
     579 lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1)))
     580 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ]
     581 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec
     582 cases (opt_Exists_elim … sigma_spec) in ⊢ ?;
     583 * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
    551584 #related_lin_stm_graph_stm
     585 
    552586 inversion (stmt_implicit_label ???)
    553587 [ whd in match (opt_All ???); #stmt_implicit_spec #_
    554    letin st2_opt' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
    555                (ev_genv (lin_prog_params p p' lin_prog))
    556                (linearise_status_fun … sigma st1 wf_st1))
    557    check st2_opt'
    558    cut (∃st2': lin_abstract_status p p' lin_prog. st2_opt' = return st2')
     588   letin st2_opt' ≝ (eval_state …
     589               (ev_genv (lin_prog_params … lin_prog lin_stack_sizes))
     590               (sigma_state … wf_st1))
     591   cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2')
    559592   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
    560593   normalize nodelta in st2_spec'; -st2_opt'
    … …  
    563596   | @st2_spec' ]
    564597   %[%] [%]
    565    [ whd
    566      whd in st2_spec':(??%?); >fetch_statement_sigma_commute in st2_spec';
    567      whd in move_st1_st1':(??%?);
    568      cut (fetch_statement (graph_prog_params p p' graph_prog) (graph_prog_params … graph_prog) … (ev_genv (graph_prog_params … graph_prog)) … (pc … st1) = OK ? 〈graph_fun,graph_stmt〉)
    569      [ cases daemon (* TODO once and for all, consequence of graph_lookup_ok *) ]
    570      #fetch_statement_ok >fetch_statement_ok in move_st1_st1';
    571      whd in ⊢ (??%? → ??%? → ?); normalize nodelta
     598   [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec';
     599     >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec';
     600     >m_return_bind
     601     (* Case analysis over the possible statements *)
    572602     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
    573603     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
Note: See TracChangeset for help on using the changeset viewer.