Ignore:
Timestamp:
Nov 14, 2012, 5:38:57 PM (7 years ago)
Author:
piccolo
Message:

adapted lineariseProof to new semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2452 r2464  
    1616include "common/StatusSimulation.ma".   
    1717include "joint/Traces.ma".
    18 include "joint/SemanticUtils.ma".
    19 
    20 definition graph_prog_params:
    21   ∀p:unserialized_params.
    22   (∀F.sem_unserialized_params p F) →
    23     joint_program (mk_graph_params p) →
    24    prog_params
    25  ≝
    26  λp,p',prog.
    27   (mk_prog_params
    28    (make_sem_graph_params (mk_graph_params p) p')
    29    prog).
    30 
    31 definition lin_prog_params:
    32   ∀p:unserialized_params.
    33   (∀F.sem_unserialized_params p F) →
    34     joint_program (mk_lin_params p) →
    35    prog_params
    36  ≝
    37  λp,p',prog.
    38   (mk_prog_params
    39    (make_sem_lin_params (mk_lin_params p) p')
    40    prog).
    41 
    42 (*CSC: Paolo, come to the rescue*)
    43 axiom choose_sigma:
    44   ∀p:unserialized_params.
    45   (∀F.sem_unserialized_params p F) →
    46     joint_program (mk_graph_params p) →
    47    identifier LabelTag → option ℕ.
    48 
    49 (*CSC: Paolo, come to the rescue*)
    50 axiom linearise_code_spec:
    51  ∀p : unserialized_params.
    52  ∀p':(∀F.sem_unserialized_params p F).
    53  ∀graph_prog:joint_program (mk_graph_params p).
    54  ∀graph_fun:joint_closed_internal_function (mk_graph_params p)
    55                            (globals (graph_prog_params p p' graph_prog)).
    56  let sigma ≝ choose_sigma p p' graph_prog in
    57  let lin_fun ≝ linearise_int_fun … graph_fun in
    58  let g ≝ joint_if_code ?? (pi1 … graph_fun) in
    59  let c ≝ joint_if_code ?? (pi1 … lin_fun) in
    60  ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
    61       code_closed … c ∧
    62       sigma entry = Some ? 0 ∧
    63       ∀l,n.sigma l = Some ? n →
    64         ∃s. lookup … g l = Some ? s ∧
    65           opt_Exists ?
    66             (λls.let 〈lopt, ts〉 ≝ ls in
    67               opt_All ? (eq ? l) lopt ∧
    68               ts = graph_to_lin_statement … s ∧
    69               opt_All ?
    70                 (λnext.Or (sigma next = Some ? (S n))
    71                 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    72                 (stmt_implicit_label … s)) (nth_opt … n c).
    73    
     18include "joint/semanticsUtils.ma".
     19
     20definition 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
     45axiom 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
     50definition 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
     56coercion 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
     63definition 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.
     73
     74definition graph_prog_params ≝
     75λp,p',prog,stack_sizes.
     76mk_prog_params (make_sem_graph_params p p') prog stack_sizes.
     77
    7478definition graph_abstract_status:
    7579 ∀p:unserialized_params.
    7680  (∀F.sem_unserialized_params p F) →
    77     joint_program (mk_graph_params p) →
     81    ∀prog : joint_program (mk_graph_params p).
     82  ((Σi.is_internal_function_of_program … prog i) → ℕ) →
    7883     abstract_status
    7984 ≝
    80  λp,p',prog.
    81   joint_abstract_status (graph_prog_params p p' prog).
     85 λp,p',prog,stack_sizes.
     86 joint_abstract_status (graph_prog_params ? p' prog stack_sizes).
     87
     88definition lin_prog_params ≝
     89λp,p',prog,stack_sizes.
     90mk_prog_params (make_sem_lin_params p p') prog stack_sizes.
    8291
    8392definition lin_abstract_status:
    8493 ∀p:unserialized_params.
    8594  (∀F.sem_unserialized_params p F) →
    86     joint_program (mk_lin_params p) →
     95    ∀prog : joint_program (mk_lin_params p).
     96  ((Σi.is_internal_function_of_program … prog i) → ℕ) →
    8797     abstract_status
    8898 ≝
    89  λp,p',prog.
    90   joint_abstract_status (lin_prog_params p p' prog).
    91 
    92 (*CSC: BUG, the natural must be ≤ 2^16! *)
    93 (*CSC: already defined? *)
    94 definition pointer_of_block_and_lin_offset :
    95  ∀b:block. block_region b = Code → nat → cpointer ≝
    96   λb,p,n. «mk_pointer b (mk_offset (bitvector_of_nat … n)), p».
     99 λp,p',prog,stack_sizes.
     100 joint_abstract_status (lin_prog_params ? p' prog stack_sizes).
     101
     102definition sigma_pc_opt:
     103 ∀p,p',graph_prog,stack_sizes.
     104  ((Σi.is_internal_function_of_program … graph_prog i) →
     105    code_point (mk_graph_params p) → option ℕ) →
     106   cpointer → option cpointer
     107 ≝
     108  λp,p',prog,stack_sizes,sigma,pc.
     109  let pars ≝ graph_prog_params p p' prog stack_sizes in
     110  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).
     114
     115definition well_formed_pc:
     116 ∀p,p',graph_prog,stack_sizes.
     117  ((Σi.is_internal_function_of_program … graph_prog i) →
     118    label → option ℕ) →
     119   cpointer → Prop
     120 ≝
     121 λp,p',prog,stack_sizes,sigma,pc.
     122  sigma_pc_opt p p' prog stack_sizes sigma pc
     123   ≠ None ….
    97124
    98125definition well_formed_status:
     126 ∀p,p',graph_prog,stack_sizes.
     127  ((Σi.is_internal_function_of_program … graph_prog i) →
     128    label → option ℕ) →
     129  state_pc (make_sem_graph_params p p') → Prop ≝
     130 λp,p',prog,stack_sizes,sigma,st.
     131 well_formed_pc p p' prog stack_sizes sigma (pc … st) ∧ ?.
     132cases daemon (* TODO *)
     133qed.
     134
     135(*
     136lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?.
     137[ #p #s #st #prf
     138  whd in match sigma_pc_of_status; normalize nodelta
     139  @opt_safe_elim
     140  #n
     141  lapply (refl …  (int_funct_of_block (joint_closed_internal_function p) (globals p)
     142        (ev_genv p) (pblock (pc p st))))
     143  elim (int_funct_of_block (joint_closed_internal_function p) (globals p)
     144        (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%);
     145  [ #_ #ABS normalize in ABS; destruct(ABS) ]
     146  #f #EQ >m_return_bind
     147*)
     148
     149
     150(*
     151lemma wf_status_to_wf_pc :
     152∀p,p',graph_prog,stack_sizes.
     153∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
     154    code_point (mk_graph_params p) → option ℕ).
     155∀st.
     156well_formed_status p p' graph_prog stack_sizes sigma st →
     157well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st).
     158#p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H
     159qed.
     160
     161lemma sigma_pc_of_status_ok:
     162  ∀p,p',graph_prog,stack_sizes.
     163  ∀sigma.
     164   ∀st.
     165    ∀prf:well_formed_status p p' graph_prog stack_sizes sigma st.
     166    sigma_pc_opt p p' graph_prog stack_sizes sigma (pc ? st) =
     167    Some … (sigma_pc_of_status p p' graph_prog stack_sizes sigma st prf).
     168    #p #p' #graph_prog #stack_sizes #sigma #st #prf @opt_to_opt_safe qed.
     169
     170*)
     171
     172definition sigma_pc :
     173∀p,p',graph_prog,stack_sizes.
     174∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
     175    label → option ℕ).
     176∀pc.
     177∀prf : well_formed_pc p p' graph_prog stack_sizes sigma pc.
     178cpointer ≝
     179λp,p',graph_prog,stack_sizes,sigma,st.opt_safe ….
     180
     181definition sigma_state :
     182 ∀p.
     183 ∀p':∀F.sem_unserialized_params p F.
     184 ∀graph_prog,stack_sizes.
     185  ∀sigma.
     186(*   let lin_prog ≝ linearise ? graph_prog in *)
     187    ∀s:state_pc (p' ?). (* = graph_abstract_status p p' graph_prog stack_sizes *)
     188     well_formed_status p p' graph_prog stack_sizes sigma s →
     189      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
     190
     191 λp,p',graph_prog,stack_sizes,sigma,s,prf.
     192 let pc' ≝ sigma_pc … (proj1 … prf) in
     193 mk_state_pc ? ? pc'.
     194 cases daemon (* TODO *) qed.
     195
     196lemma sigma_pc_commute:
     197 ∀p,p',graph_prog,stack_sizes,sigma,st.
     198 ∀prf : well_formed_status p p' graph_prog stack_sizes sigma st.
     199 sigma_pc … (pc ? st) (proj1 … prf) =
     200 pc ? (sigma_state … st prf).
     201#p #p' #prog #stack_sizes #sigma #st #prf %
     202qed.
     203
     204lemma res_eq_from_opt :
     205  ∀A,m,v.res_to_opt A m = return v → m = return v.
     206#A * #x #v normalize #EQ destruct % qed.
     207
     208lemma if_propagate :
     209∀pars_in, pars_out : sem_params.
     210∀trans : ∀globals.joint_closed_internal_function pars_in globals →
     211                  joint_closed_internal_function pars_out globals.
     212∀prog_in : program (joint_function pars_in) ℕ.
     213let prog_out ≝
     214  transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
     215∀i.is_internal_function_of_program … prog_in i →
     216is_internal_function_of_program … prog_out i.
     217cases daemon (* TODO by paolo *) qed.
     218
     219definition stack_sizes_lift :
     220∀pars_in, pars_out : sem_params.
     221∀trans : ∀globals.joint_closed_internal_function pars_in globals →
     222                  joint_closed_internal_function pars_out globals.
     223∀prog_in : program (joint_function pars_in) ℕ.
     224let prog_out ≝
     225  transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
     226((Σi.is_internal_function_of_program … prog_out i) → ℕ) →
     227((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝
     228λpars_in,pars_out,prog_in,trans,stack_sizes.
     229λi.stack_sizes «i, if_propagate … (pi2 … i)».
     230
     231axiom ok_is_internal_function_of_program :
     232  ∀p.∀prog:joint_program p.∀i.
     233  is_internal_function_of_program p prog i →
     234  is_internal_function ?? (globalenv_noinit ? prog) i.
     235
     236
     237definition sigma_function_name :
    99238 ∀p,p',graph_prog.
    100   ∀sigma: identifier LabelTag → option ℕ.
    101   graph_abstract_status p p' graph_prog → Prop
    102  ≝
    103  λp,p',graph_prog,sigma,s.
    104   sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
    105    ≠ None ….
    106 
    107 definition sigma_pc_of_status:
     239 let lin_prog ≝ linearise p graph_prog in
     240 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     241 let graph_stack_sizes ≝
     242  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     243    ? graph_prog lin_stack_sizes in
     244  (Σf.is_internal_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) f) →
     245  (Σf.is_internal_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) f) ≝
     246λp,p',graph_prog,lin_stack_sizes,f.pi1 … f.
     247@ok_is_internal_function_of_program
     248@(if_propagate (make_sem_graph_params p p') (make_sem_lin_params p p'))
     249@is_internal_function_of_program_ok
     250@(pi2 … f)
     251qed.
     252
     253lemma fetch_function_sigma_commute :
    108254 ∀p,p',graph_prog.
    109   ∀sigma: identifier LabelTag → option ℕ.
    110    ∀s:graph_abstract_status p p' graph_prog.
    111     well_formed_status … sigma s → ℕ
    112  ≝
    113   λp,p',prog,sigma,s.
    114    match sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
    115    return λx. x ≠ None ? → ℕ
    116    with
    117    [ None ⇒ λprf.⊥
    118    | Some n ⇒ λ_.n ].
    119  @(absurd ?? prf) //
    120 qed.
    121 
    122 lemma sigma_pc_of_status_ok:
    123   ∀p,p',graph_prog.
    124   ∀sigma: identifier LabelTag → option ℕ.
    125    ∀s:graph_abstract_status p p' graph_prog.
    126     ∀prf:well_formed_status … sigma s.
    127      sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
    128      = Some … (sigma_pc_of_status … prf).
    129  #p #p' #prog #sigma #s whd in ⊢ (% → ?);
    130  whd in match sigma_pc_of_status; normalize nodelta cases (sigma ?) //
    131  #abs cases (absurd ?? abs)
    132 qed.
    133 
    134 definition linearise_status_fun:
    135  ∀p,p',graph_prog.
    136   ∀sigma: identifier LabelTag → option ℕ.
    137    let lin_prog ≝ linearise ? graph_prog in
    138     ∀s:graph_abstract_status p p' graph_prog.
    139      well_formed_status … sigma s →
    140       lin_abstract_status p p' lin_prog
    141 
    142  λp,p',graph_prog,sigma,s,prf.
    143   mk_state_pc ??
    144    (pointer_of_block_and_lin_offset (pblock (pc ? s)) …
    145     (sigma_pc_of_status … sigma … prf)).
    146 [2: cases (pc ??) * normalize //
    147 | cases daemon (* TODO *) ]
    148 qed.
    149 
    150 lemma sigma_pc_commute:
    151  ∀p,p',graph_prog,s1,prf.
    152  sigma_pc_of_status p p' graph_prog (choose_sigma p p' graph_prog) s1 prf =
    153  point_of_pointer (lin_prog_params p p' (linearise p graph_prog))
    154  (lin_prog_params p p' (linearise p graph_prog))
    155   (pc (lin_prog_params p p' (linearise p graph_prog))
    156    (linearise_status_fun p p' graph_prog (choose_sigma p p' graph_prog) s1 prf)).
    157 #p #p' #prog #s #prf whd in ⊢ (??%%); change with (? = nat_of_bitvector ??);
    158 whd in match (pc … (linearise_status_fun …));
    159 >nat_of_bitvector_bitvector_of_nat_inverse //
    160 cases daemon (* CSC: Paolo, you must prove this additional invariant! *)
     255 let lin_prog ≝ linearise p graph_prog in
     256 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     257 let graph_stack_sizes ≝
     258  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     259    ? graph_prog lin_stack_sizes in
     260 ∀sigma,pc,f.
     261  ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
     262 fetch_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc =
     263  return f
     264→ fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) (sigma_pc … pc prf) =
     265  return sigma_function_name … f.
     266 #p #p' #graph_prog #stack_sizes #sigma #pc #f #prf
     267(* whd in match fetch_function; normalize nodelta
     268whd in match function_of_block; normalize nodelta
     269#H elim (bind_inversion ????? H) -H #fn *
     270#H lapply (opt_eq_from_res ???? H) -H
     271#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
     272-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
     273destruct // *)
     274cases daemon
     275qed.
     276
     277lemma if_of_function_commute:
     278 ∀p,p',graph_prog,stack_sizes.
     279 ∀graph_fun.
     280 let graph_fd ≝ if_of_function ??? graph_fun in
     281 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
     282 let lin_fd ≝ if_of_function … lin_fun in
     283 lin_fd = linearise_int_fun … graph_fd.
     284(* usare match_opt_prf_elim ? *)
     285cases daemon qed.
     286
     287lemma stmt_at_sigma_commute:
     288 ∀p,p',graph_prog,stack_sizes,graph_fun,lbl.
     289 let lin_prog ≝ linearise ? graph_prog in
     290 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
     291 ∀sigma.good_sigma p p' graph_prog sigma →
     292 ∀prf:sigma graph_fun lbl ≠ None ….
     293 ∃stmt.
     294   stmt_at …
     295    (joint_if_code ?? (if_of_function ??? graph_fun)) 
     296    lbl = Some ? stmt ∧
     297   stmt_at …
     298    (joint_if_code ?? (if_of_function ??? lin_fun))
     299    (opt_safe … (sigma graph_fun lbl) prf) = Some ? (graph_to_lin_statement … stmt). 
     300 #p #p' #graph_prog #stack_sizes #graph_fun #lbl #sigma #good #prf
     301 @opt_safe_elim -prf #n #prf
     302 (*
     303 whd in match (stmt_at ????);
     304 whd in match (stmt_at ????);
     305 cases (linearise_code_spec … p' graph_prog graph_fun
     306         (joint_if_entry … graph_fun))
     307 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
     308 lapply (sigma_spec
     309         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
     310 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
     311 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
     312 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
     313 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
     314 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
     315 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
     316 <sigma_pc_commute >lin_lookup_ok // *)
     317 cases daemon
     318qed.
     319
     320lemma fetch_statement_sigma_commute:
     321  ∀p,p',graph_prog,lin_stack_sizes,pc,fn,stmt.
     322  let lin_prog ≝ linearise ? graph_prog in
     323  let graph_stack_sizes ≝
     324   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     325    ? graph_prog lin_stack_sizes in
     326  ∀sigma.good_sigma p p' graph_prog sigma →
     327  ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
     328  fetch_statement ? (make_sem_graph_params p p') … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc =
     329    return 〈fn,stmt〉 →
     330  fetch_statement ? (make_sem_lin_params p p') … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes))
     331   (sigma_pc … pc prf) =
     332    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
     333 #p #p' #graph_prog #stack_sizes #pc #fn #stmt #good #prf
     334(* @opt_safe_elim -prf #n #prf
     335 whd in match fetch_statement; normalize nodelta
     336 >fetch_function_sigma_commute
     337 cases (fetch_function ????) [2://]
     338 #graph_fun whd in ⊢ (??%%);
     339 whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
     340 >stm_at_sigma_commute cases (stmt_at ????) // *)
     341cases daemon
    161342qed.
    162343
    163344definition linearise_status_rel:
    164345 ∀p,p',graph_prog.
    165   ∀sigma: identifier LabelTag → option ℕ.
    166   let lin_prog ≝ linearise ? graph_prog in
     346 let lin_prog ≝ linearise p graph_prog in
     347 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     348 let stack_sizes' ≝
     349  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     350    ? graph_prog stack_sizes in
     351 ∀sigma.
     352 good_sigma p p' graph_prog sigma →
    167353   status_rel
    168     (graph_abstract_status p p' graph_prog)
    169     (lin_abstract_status p p' lin_prog)
    170  ≝ λp,p',graph_prog,sigma.mk_status_rel …
    171     (λs1,s2.
    172      ∃prf: well_formed_status … sigma s1.
    173       s2 = linearise_status_fun p p' graph_prog sigma s1 prf) ….
    174  cases daemon (* TODO *)
     354    (graph_abstract_status p p' graph_prog stack_sizes')
     355    (lin_abstract_status p p' lin_prog stack_sizes)
     356 ≝ λp,p',graph_prog,stack_sizes,sigma,good.
     357   let stack_sizes' ≝
     358    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     359      ? graph_prog ? in
     360   mk_status_rel …
     361    (* sem_rel ≝ *) (λs1,s2.
     362     ∃prf: well_formed_status p p' graph_prog stack_sizes' sigma s1.
     363      s2 = sigma_state … s1 prf)
     364    (* call_rel ≝ *) (λs1,s2.
     365      ∃prf:well_formed_status p p' graph_prog stack_sizes' sigma s1.
     366      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
     367    (* sim_final ≝ *) ?.
     368#st1 #st2 * #prf #EQ2
     369%
     370whd in ⊢ (%→%);
     371#H lapply (opt_to_opt_safe … H)
     372@opt_safe_elim -H
     373#res #_
     374#H lapply (res_eq_from_opt ??? H) -H
     375#H elim (bind_inversion ????? H)
     376* #f #stmt *
     377whd in ⊢ (??%?→?);
     378cases daemon
    175379qed.
    176380
    177381(* To be added to common/Globalenvs, it strenghtens
    178382   find_funct_ptr_transf *)
     383(*   
    179384lemma
    180385  find_funct_ptr_transf_eq:
     
    189394 | #f #H >(find_funct_ptr_transf A B … H) // ]
    190395qed.
    191 
    192 lemma fetch_function_sigma_commute:
     396*)
     397
     398
     399(*lemma fetch_function_sigma_commute:
    193400 ∀p,p',graph_prog,sigma,st1.
    194401 ∀prf:well_formed_status ??? sigma st1.
    195402 let lin_prog ≝ linearise ? graph_prog in
    196   fetch_function
     403  fetch_function               
    197404   (lin_prog_params p p' lin_prog)
    198405   (globals (lin_prog_params p p' lin_prog))
     
    213420cases (find_funct_ptr ???) // * //
    214421qed.
    215 
    216 lemma stm_at_sigma_commute:
    217  ∀p,p',graph_prog,graph_fun,s1.
    218  let lin_prog ≝ linearise ? graph_prog in
    219  let sigma ≝ choose_sigma p p' graph_prog in
    220  ∀prf:well_formed_status ??? sigma s1.
    221   stmt_at (lin_prog_params p p' (linearise p graph_prog))
    222    (globals (lin_prog_params p p' (linearise p graph_prog)))
    223    (joint_if_code (lin_prog_params p p' (linearise p graph_prog))
    224     (globals (lin_prog_params p p' (linearise p graph_prog)))
    225     (linearise_int_fun p (globals (graph_prog_params p p' graph_prog)) graph_fun))
    226    (point_of_pointer (lin_prog_params p p' (linearise p graph_prog))
    227     (lin_prog_params p p' (linearise p graph_prog))
    228     (pc (lin_prog_params p p' (linearise p graph_prog))
    229      (linearise_status_fun p p' graph_prog sigma s1 prf)))
    230  =
    231   option_map …
    232    (graph_to_lin_statement …)
    233    (stmt_at (graph_prog_params p p' graph_prog)
    234     (globals (graph_prog_params p p' graph_prog))
    235     (joint_if_code (graph_prog_params p p' graph_prog)
    236      (globals (graph_prog_params p p' graph_prog)) graph_fun)
    237     (point_of_pointer (graph_prog_params p p' graph_prog)
    238      (graph_prog_params p p' graph_prog)
    239      (pc (graph_prog_params p p' graph_prog) s1))).
    240  #p #p' #graph_prog #graph_fun #s1 #prf
    241  whd in match (stmt_at ????);
    242  whd in match (stmt_at ????);
    243  cases (linearise_code_spec … p' graph_prog graph_fun
    244          (joint_if_entry … graph_fun))
    245  * #lin_code_closed #sigma_entry_is_zero #sigma_spec
    246  lapply (sigma_spec
    247          (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
    248  -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
    249  -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
    250  whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
    251  inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
    252  * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
    253  #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
    254  <sigma_pc_commute >lin_lookup_ok //
    255 qed.
    256 
    257 lemma fetch_statement_sigma_commute:
    258  ∀p,p',graph_prog,st1.
    259  let sigma ≝ choose_sigma p p' graph_prog in
    260  let lin_prog ≝ linearise ? graph_prog in
    261  ∀prf.
    262   fetch_statement
    263    (lin_prog_params p p' lin_prog)
    264    (lin_prog_params p p' lin_prog)
    265    (globals (lin_prog_params p p' lin_prog))
    266    (ev_genv (lin_prog_params p p' lin_prog))
    267    (pc (lin_prog_params p p' lin_prog)
    268     (linearise_status_fun p p' graph_prog sigma st1 prf))
    269  =
    270   m_map …
    271    (λfun_stm.
    272      let 〈fun,stm〉 ≝ fun_stm in
    273       〈linearise_int_fun ?? fun, graph_to_lin_statement ?? stm〉)
    274    (fetch_statement
    275     (graph_prog_params p p' graph_prog)
    276     (graph_prog_params p p' graph_prog)
    277     (globals (graph_prog_params p p' graph_prog))
    278     (ev_genv (graph_prog_params p p' graph_prog))
    279     (pc (graph_prog_params p p' graph_prog) st1)).
    280  #p #p' #graph_prog #s1 #prf
    281  whd in match fetch_statement; normalize nodelta
    282  >fetch_function_sigma_commute
    283  cases (fetch_function ????) [2://]
    284  #graph_fun whd in ⊢ (??%%);
    285  whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
    286  >stm_at_sigma_commute cases (stmt_at ????) //
    287 qed.
     422*)
     423       
     424inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
     425    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
     426interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).
    288427
    289428lemma linearise_ok:
    290429 ∀p,p',graph_prog.
    291430  let lin_prog ≝ linearise ? graph_prog in
     431 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     432 let graph_stack_sizes ≝
     433  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     434    ? graph_prog lin_stack_sizes in
     435   ∃R.
    292436   status_simulation
    293     (graph_abstract_status p p' graph_prog)
    294     (lin_abstract_status p p' lin_prog) ≝
    295  λp,p',graph_prog.
    296   let sigma ≝ choose_sigma p p' graph_prog in
    297    mk_status_simulation … (linearise_status_rel p p' graph_prog sigma) ….
     437    (graph_abstract_status p p' graph_prog graph_stack_sizes)
     438    (lin_abstract_status p p' lin_prog lin_stack_sizes) R.
     439 #p #p' #graph_prog
     440 cut (∃sigma.good_sigma p p' graph_prog sigma)
     441 [ cases daemon (* TODO by Paolo *) ] * #sigma #good
     442 #lin_stack_sizes
     443 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)}
     444 whd
    298445#st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl
    299446cases cl in classified_st1_cl; -cl #classified_st1_cl whd
Note: See TracChangeset for help on using the changeset viewer.