Changeset 2446


Ignore:
Timestamp:
Nov 9, 2012, 1:21:45 PM (7 years ago)
Author:
piccolo
Message:

Fetch commutation proof reduced to one simple (?) lemma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2445 r2446  
    3939   (make_sem_lin_params (mk_lin_params p) p')
    4040   prog).
    41    
    42 definition graph_abstract_status:
    43  ∀p:unserialized_params.
    44   (∀F.sem_unserialized_params p F) →
    45     joint_program (mk_graph_params p) →
    46      abstract_status
    47  ≝
    48  λp,p',prog.
    49   joint_abstract_status (graph_prog_params p p' prog).
    50 
    51 definition lin_abstract_status:
    52  ∀p:unserialized_params.
    53   (∀F.sem_unserialized_params p F) →
    54     joint_program (mk_lin_params p) →
    55      abstract_status
    56  ≝
    57  λp,p',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? *)
    62 definition 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 
    66 definition 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 
    75 definition 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) //
    88 qed.
    89    
    90 definition 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 *) ]
    104 qed.
    105 
    106 definition linearise_status_rel:
    107  ∀p,p',graph_prog.
    108   ∀sigma: identifier LabelTag → option ℕ.
    109   let lin_prog ≝ linearise ? graph_prog in
    110    status_rel
    111     (graph_abstract_status p p' graph_prog)
    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 *)
    118 qed.
    11941
    12042(*CSC: Paolo, come to the rescue*)
     
    14971                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    15072                (stmt_implicit_label … s)) (nth_opt … n c).
     73   
     74definition graph_abstract_status:
     75 ∀p:unserialized_params.
     76  (∀F.sem_unserialized_params p F) →
     77    joint_program (mk_graph_params p) →
     78     abstract_status
     79 ≝
     80 λp,p',prog.
     81  joint_abstract_status (graph_prog_params p p' prog).
     82
     83definition lin_abstract_status:
     84 ∀p:unserialized_params.
     85  (∀F.sem_unserialized_params p F) →
     86    joint_program (mk_lin_params p) →
     87     abstract_status
     88 ≝
     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? *)
     94definition 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».
     97
     98definition well_formed_status:
     99 ∀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
     107definition sigma_pc_of_status:
     108 ∀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) //
     120qed.
     121
     122lemma 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)
     132qed.
     133
     134definition 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 *) ]
     148qed.
     149
     150axiom 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
     158definition linearise_status_rel:
     159 ∀p,p',graph_prog.
     160  ∀sigma: identifier LabelTag → option ℕ.
     161  let lin_prog ≝ linearise ? graph_prog in
     162   status_rel
     163    (graph_abstract_status p p' graph_prog)
     164    (lin_abstract_status p p' lin_prog)
     165 ≝ λp,p',graph_prog,sigma.mk_status_rel …
     166    (λs1,s2.
     167     ∃prf: well_formed_status … sigma s1.
     168      s2 = linearise_status_fun p p' graph_prog sigma s1 prf) ….
     169 cases daemon (* TODO *)
     170qed.
    151171
    152172axiom fetch_function_sigma_commute:
     
    196216 whd in match (stmt_at ????);
    197217 whd in match (stmt_at ????);
    198 
    199 ================================
    200   normalize nodelta
     218 cases (linearise_code_spec … p' graph_prog graph_fun
     219         (joint_if_entry … graph_fun))
     220 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
     221 lapply (sigma_spec
     222         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
     223 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
     224 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
     225 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
     226 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
     227 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
     228 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
     229 <sigma_pc_commute >lin_lookup_ok //
     230qed.
    201231
    202232lemma fetch_statement_sigma_commute:
    203  ∀p,p',graph_prog,sigma,st1.
     233 ∀p,p',graph_prog,st1.
     234 let sigma ≝ choose_sigma p p' graph_prog in
    204235 let lin_prog ≝ linearise ? graph_prog in
     236 ∀prf.
    205237  fetch_statement
    206238   (lin_prog_params p p' lin_prog)
     
    209241   (ev_genv (lin_prog_params p p' lin_prog))
    210242   (pc (lin_prog_params p p' lin_prog)
    211     (linearise_status_fun p p' graph_prog sigma st1))
     243    (linearise_status_fun p p' graph_prog sigma st1 prf))
    212244 =
    213245  m_map …
     
    221253    (ev_genv (graph_prog_params p p' graph_prog))
    222254    (pc (graph_prog_params p p' graph_prog) st1)).
    223  #p #p' #graph_prog #sigma #s1
     255 #p #p' #graph_prog #s1 #prf
    224256 whd in match fetch_statement; normalize nodelta
    225257 >fetch_function_sigma_commute
     
    227259 #graph_fun whd in ⊢ (??%%);
    228260 whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
    229  >stm_at_sigma_commute
    230  cases (stmt_at ????) //
     261 >stm_at_sigma_commute cases (stmt_at ????) //
    231262qed.
    232263
     
    243274cases cl in classified_st1_cl; -cl #classified_st1_cl whd
    244275[4:
    245  whd in rel_st1_st2; >rel_st1_st2 -st2
     276 cases rel_st1_st2 -rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 -st2
    246277 whd in move_st1_st1';
    247278 letin lin_prog ≝ (linearise ? graph_prog)
    248279 letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
    249280               (ev_genv (lin_prog_params p p' lin_prog))
    250                (linearise_status_fun … sigma st1))
     281               (linearise_status_fun … sigma st1 wf_st1))
    251282 whd in st2';
    252283 whd in match (fetch_statement ?????) in st2';
Note: See TracChangeset for help on using the changeset viewer.