Changeset 2445 for src/joint


Ignore:
Timestamp:
Nov 9, 2012, 11:47:57 AM (7 years ago)
Author:
piccolo
Message:
  1. sigma function axiomatically defined (together with its spec). It should come from Paolo's linearise function, but there it is existentially (not sigma) quantified and Paolo's records for simulation relations are in Type and not in Prop. One of the two things need to be changed (hopefully the records...)
  2. sigma extended to statuses (PC only atm)
  3. some preliminary lemmas about commutation of sigma with fetching
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2443 r2445  
    1818include "joint/SemanticUtils.ma".
    1919
     20definition 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
     31definition 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   
    2042definition graph_abstract_status:
    2143 ∀p:unserialized_params.
     
    2547 ≝
    2648 λp,p',prog.
    27   joint_abstract_status
    28    (mk_prog_params
    29     (make_sem_graph_params p p')
    30     prog).
     49  joint_abstract_status (graph_prog_params p p' prog).
    3150
    3251definition lin_abstract_status:
     
    3756 ≝
    3857 λp,p',prog.
    39   joint_abstract_status
    40    (mk_prog_params
    41     (make_sem_lin_params p p')
    42     prog).
     58  joint_abstract_status (lin_prog_params p p' prog).
     59
     60(*CSC: BUG, the natural must be ≤ 2^16! *)
     61(*CSC: already defined? *)
     62definition pointer_of_block_and_lin_offset :
     63 ∀b:block. block_region b = Code → nat → cpointer ≝
     64  λb,p,n. «mk_pointer b (mk_offset (bitvector_of_nat … n)), p».
     65
     66definition well_formed_status:
     67 ∀p,p',graph_prog.
     68  ∀sigma: identifier LabelTag → option ℕ.
     69  graph_abstract_status p p' graph_prog → Prop
     70 ≝
     71 λp,p',graph_prog,sigma,s.
     72  sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
     73   ≠ None ….
     74
     75definition sigma_pc_of_status:
     76 ∀p,p',graph_prog.
     77  ∀sigma: identifier LabelTag → option ℕ.
     78   ∀s:graph_abstract_status p p' graph_prog.
     79    well_formed_status … sigma s → ℕ
     80 ≝
     81  λp,p',prog,sigma,s.
     82   match sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
     83   return λx. x ≠ None ? → ℕ
     84   with
     85   [ None ⇒ λprf.⊥
     86   | Some n ⇒ λ_.n ].
     87 @(absurd ?? prf) //
     88qed.
     89   
     90definition linearise_status_fun:
     91 ∀p,p',graph_prog.
     92  ∀sigma: identifier LabelTag → option ℕ.
     93   let lin_prog ≝ linearise ? graph_prog in
     94    ∀s:graph_abstract_status p p' graph_prog.
     95     well_formed_status … sigma s →
     96      lin_abstract_status p p' lin_prog
     97
     98 λp,p',graph_prog,sigma,s,prf.
     99  mk_state_pc ??
     100   (pointer_of_block_and_lin_offset (pblock (pc ? s)) …
     101    (sigma_pc_of_status … sigma … prf)).
     102[2: cases (pc ??) * normalize //
     103| cases daemon (* TODO *) ]
     104qed.
    43105
    44106definition linearise_status_rel:
    45107 ∀p,p',graph_prog.
     108  ∀sigma: identifier LabelTag → option ℕ.
    46109  let lin_prog ≝ linearise ? graph_prog in
    47110   status_rel
    48111    (graph_abstract_status p p' graph_prog)
    49     (lin_abstract_status p p' lin_prog).
    50  cases daemon
     112    (lin_abstract_status p p' lin_prog)
     113 ≝ λp,p',graph_prog,sigma.mk_status_rel …
     114    (λs1,s2.
     115     ∃prf: well_formed_status … sigma s1.
     116      s2 = linearise_status_fun p p' graph_prog sigma s1 prf) ….
     117 cases daemon (* TODO *)
     118qed.
     119
     120(*CSC: Paolo, come to the rescue*)
     121axiom choose_sigma:
     122  ∀p:unserialized_params.
     123  (∀F.sem_unserialized_params p F) →
     124    joint_program (mk_graph_params p) →
     125   identifier LabelTag → option ℕ.
     126
     127(*CSC: Paolo, come to the rescue*)
     128axiom linearise_code_spec:
     129 ∀p : unserialized_params.
     130 ∀p':(∀F.sem_unserialized_params p F).
     131 ∀graph_prog:joint_program (mk_graph_params p).
     132 ∀graph_fun:joint_closed_internal_function (mk_graph_params p)
     133                           (globals (graph_prog_params p p' graph_prog)).
     134 let sigma ≝ choose_sigma p p' graph_prog in
     135 let lin_fun ≝ linearise_int_fun … graph_fun in
     136 let g ≝ joint_if_code ?? (pi1 … graph_fun) in
     137 let c ≝ joint_if_code ?? (pi1 … lin_fun) in
     138 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
     139      code_closed … c ∧
     140      sigma entry = Some ? 0 ∧
     141      ∀l,n.sigma l = Some ? n →
     142        ∃s. lookup … g l = Some ? s ∧
     143          opt_Exists ?
     144            (λls.let 〈lopt, ts〉 ≝ ls in
     145              opt_All ? (eq ? l) lopt ∧
     146              ts = graph_to_lin_statement … s ∧
     147              opt_All ?
     148                (λnext.Or (sigma next = Some ? (S n))
     149                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
     150                (stmt_implicit_label … s)) (nth_opt … n c).
     151
     152axiom fetch_function_sigma_commute:
     153 ∀p,p',graph_prog,sigma,st1.
     154 ∀prf:well_formed_status ??? sigma st1.
     155 let lin_prog ≝ linearise ? graph_prog in
     156  fetch_function
     157   (lin_prog_params p p' lin_prog)
     158   (globals (lin_prog_params p p' lin_prog))
     159   (ev_genv (lin_prog_params p p' lin_prog))
     160   (pc (lin_prog_params p p' lin_prog)
     161    (linearise_status_fun p p' graph_prog sigma st1 prf))
     162 =
     163  m_map …
     164   (linearise_int_fun ??)
     165   (fetch_function
     166    (graph_prog_params p p' graph_prog)
     167    (globals (graph_prog_params p p' graph_prog))
     168    (ev_genv (graph_prog_params p p' graph_prog))
     169    (pc (graph_prog_params p p' graph_prog) st1)).
     170
     171lemma stm_at_sigma_commute:
     172 ∀p,p',graph_prog,graph_fun,s1.
     173 let lin_prog ≝ linearise ? graph_prog in
     174 let sigma ≝ choose_sigma p p' graph_prog in
     175 ∀prf:well_formed_status ??? sigma s1.
     176  stmt_at (lin_prog_params p p' (linearise p graph_prog))
     177   (globals (lin_prog_params p p' (linearise p graph_prog)))
     178   (joint_if_code (lin_prog_params p p' (linearise p graph_prog))
     179    (globals (lin_prog_params p p' (linearise p graph_prog)))
     180    (linearise_int_fun p (globals (graph_prog_params p p' graph_prog)) graph_fun))
     181   (point_of_pointer (lin_prog_params p p' (linearise p graph_prog))
     182    (lin_prog_params p p' (linearise p graph_prog))
     183    (pc (lin_prog_params p p' (linearise p graph_prog))
     184     (linearise_status_fun p p' graph_prog sigma s1 prf)))
     185 =
     186  option_map …
     187   (graph_to_lin_statement …)
     188   (stmt_at (graph_prog_params p p' graph_prog)
     189    (globals (graph_prog_params p p' graph_prog))
     190    (joint_if_code (graph_prog_params p p' graph_prog)
     191     (globals (graph_prog_params p p' graph_prog)) graph_fun)
     192    (point_of_pointer (graph_prog_params p p' graph_prog)
     193     (graph_prog_params p p' graph_prog)
     194     (pc (graph_prog_params p p' graph_prog) s1))).
     195 #p #p' #graph_prog #graph_fun #s1 #prf
     196 whd in match (stmt_at ????);
     197 whd in match (stmt_at ????);
     198
     199================================
     200  normalize nodelta
     201
     202lemma fetch_statement_sigma_commute:
     203 ∀p,p',graph_prog,sigma,st1.
     204 let lin_prog ≝ linearise ? graph_prog in
     205  fetch_statement
     206   (lin_prog_params p p' lin_prog)
     207   (lin_prog_params p p' lin_prog)
     208   (globals (lin_prog_params p p' lin_prog))
     209   (ev_genv (lin_prog_params p p' lin_prog))
     210   (pc (lin_prog_params p p' lin_prog)
     211    (linearise_status_fun p p' graph_prog sigma st1))
     212 =
     213  m_map …
     214   (λfun_stm.
     215     let 〈fun,stm〉 ≝ fun_stm in
     216      〈linearise_int_fun ?? fun, graph_to_lin_statement ?? stm〉)
     217   (fetch_statement
     218    (graph_prog_params p p' graph_prog)
     219    (graph_prog_params p p' graph_prog)
     220    (globals (graph_prog_params p p' graph_prog))
     221    (ev_genv (graph_prog_params p p' graph_prog))
     222    (pc (graph_prog_params p p' graph_prog) st1)).
     223 #p #p' #graph_prog #sigma #s1
     224 whd in match fetch_statement; normalize nodelta
     225 >fetch_function_sigma_commute
     226 cases (fetch_function ????) [2://]
     227 #graph_fun whd in ⊢ (??%%);
     228 whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
     229 >stm_at_sigma_commute
     230 cases (stmt_at ????) //
    51231qed.
    52232
     
    57237    (graph_abstract_status p p' graph_prog)
    58238    (lin_abstract_status p p' lin_prog) ≝
    59  λp,p',graph_prog. mk_status_simulation … (linearise_status_rel p p' graph_prog) ….
    60  cases daemon
    61 qed.
     239 λp,p',graph_prog.
     240  let sigma ≝ choose_sigma p p' graph_prog in
     241   mk_status_simulation … (linearise_status_rel p p' graph_prog sigma) ….
     242#st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl
     243cases cl in classified_st1_cl; -cl #classified_st1_cl whd
     244[4:
     245 whd in rel_st1_st2; >rel_st1_st2 -st2
     246 whd in move_st1_st1';
     247 letin lin_prog ≝ (linearise ? graph_prog)
     248 letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
     249               (ev_genv (lin_prog_params p p' lin_prog))
     250               (linearise_status_fun … sigma st1))
     251 whd in st2';
     252 whd in match (fetch_statement ?????) in st2';
     253 >fetch_function_sigma_commute in st2';
     254 whd in match (fetch_function ????) in st2';
     255 XXX
     256 check fetch_statement
     257 CSC
     258 %{}
     259
     260whd in classified_st1_cl;
     261whd in classified_st1_cl:(??%?);
     262inversion (fetch_statement ?????) in classified_st1_cl;
     263
     264<classified_st1_cl -cl
     265whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ] ?);
     266inversion (fetch_statement ?????)
     267
     268inversion (fetch_statement ?????)
     269qed.
Note: See TracChangeset for help on using the changeset viewer.