Ignore:
Timestamp:
Jul 16, 2012, 4:59:09 PM (8 years ago)
Author:
tranquil
Message:

updated joint semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2043 r2186  
    11include "joint/blocks.ma".
    2 include "joint/semantics_paolo.ma".
    3 
    4 
    5 axiom ExecutingInternalCallInBlock : String.
    6 
    7 let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
     2include "joint/Traces.ma".
     3
     4(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
    85  match b with
    96  [ nil ⇒ [ ]
    107  | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl
    11   ].
    12 
    13 definition step_flow_change_labels :
    14   ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
    15     step_flow p g lbls1 → step_flow p g lbls2 ≝
    16   λp,g,lbls1,lbls2,prf,flow.
    17   match flow with
    18   [ Redirect l ⇒ Redirect ??? «l, prf ? (pi2 … l)»
    19   | Init id b args dest ⇒ Init … id b args dest
    20   | Proceed ⇒ Proceed ???
    21   ].
    22 
    23 coercion step_flow_diff_lbls :
    24   ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
    25   ∀flow : step_flow p g lbls1.step_flow p g lbls2 ≝
    26   step_flow_change_labels on _flow : step_flow ??? to step_flow ???.
    27 
    28 definition monad_step_flow_times_coerc :
    29   ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    30     monad M ((step_flow p g lbls1) × A) → monad M ((step_flow p g lbls2) × A) ≝
    31     λp,g,lbls1,lbls2,M,A,H,m.
    32     ! 〈flow,a〉 ← m ;
    33     return 〈(flow : step_flow ?? lbls2),a〉. assumption qed.
    34 
    35 coercion step_flow_monad_times :
    36   ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    37     ∀m : monad M ((step_flow p g lbls1) × A).monad M ((step_flow p g lbls2) × A) ≝
    38   monad_step_flow_times_coerc on _m : monad ? ((step_flow ???) × ?) to monad ? ((step_flow ???) × ?).
    39 
    40 let rec eval_seq_list globals (p:sem_params) (ge : genv globals p)
    41   (st : state p) (b : list (joint_step p globals)) on b :
    42     IO io_out io_in ((step_flow p globals (seq_list_labels … b)) × (state p)) ≝
    43     match b return λx.IO ?? ((step_flow ?? (seq_list_labels … x)) × ?) with
    44     [ nil ⇒ return 〈Proceed ???, st〉
    45     | cons hd tl ⇒
    46       ! 〈flow, st'〉 ← eval_step … ge st hd ;
    47       match flow return λ_.IO ?? ((step_flow ?? (seq_list_labels … (hd :: tl))) × ?) with
    48       [ Proceed ⇒ eval_seq_list globals p ge st' tl
    49       | _ ⇒ return 〈flow, st'〉
    50       ]
    51     ]. /2 by Exists_append_r, Exists_append_l/ qed.
    52 
    53 definition fin_step_flow_change_labels :
    54   ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
    55     fin_step_flow p g lbls1 → fin_step_flow p g lbls2 ≝
    56   λp,g,lbls1,lbls2,prf,flow.
    57   match flow with
    58   [ FRedirect l ⇒ FRedirect ??? «l, prf ? (pi2 … l)»
    59   | FTailInit id b args ⇒ FTailInit … id b args
    60   | FEnd ⇒ FEnd ???
    61   ].
    62 
    63 coercion fin_step_flow_diff_lbls :
    64   ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
    65   ∀flow : fin_step_flow p g lbls1.fin_step_flow p g lbls2 ≝
    66   fin_step_flow_change_labels on _flow : fin_step_flow ??? to fin_step_flow ???.
    67 
    68 definition monad_fin_step_flow_times_coerc :
    69   ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    70     monad M ((fin_step_flow p g lbls1) × A) → monad M ((fin_step_flow p g lbls2) × A) ≝
    71     λp,g,lbls1,lbls2,M,A,H,m.
    72     ! 〈flow,a〉 ← m ;
    73     return 〈(flow : fin_step_flow ?? lbls2),a〉. assumption qed.
    74 
    75 coercion fin_step_flow_monad_times :
    76   ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    77     ∀m : monad M ((fin_step_flow p g lbls1) × A).monad M ((fin_step_flow p g lbls2) × A) ≝
    78   monad_fin_step_flow_times_coerc on _m : monad ? ((fin_step_flow ???) × ?) to monad ? ((fin_step_flow ???) × ?).
    79 
    80 definition block_cont_labels ≝ λp,g,ty.λb : block_cont p g ty.
    81   seq_list_labels … (\fst b) @
    82   match ty return λx.stmt_type_if ? x ??? → ? with
    83   [ SEQ ⇒ step_labels …
    84   | FIN ⇒ fin_step_labels …
    85   ] (\snd b).
    86 
    87 definition eval_block_cont :
    88   ∀globals.∀p : sem_params.∀ty.genv globals p →
    89   state p → ∀b : block_cont p globals ty.
    90   IO io_out io_in (
    91     (stmt_type_if ? ty step_flow fin_step_flow p globals (block_cont_labels … b)) ×
    92     (state p)) ≝ λglobals,p,ty,ge,st.
    93   match ty return λx.∀b : block_cont p globals x.
    94     IO io_out io_in (
    95       (stmt_type_if ? x step_flow fin_step_flow p globals (block_cont_labels … b)) ×
    96       (state p))
    97   with
    98   [ SEQ ⇒ λb.
    99     ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
    100     match flow return λ_.IO ?? (step_flow … ((block_cont_labels … b))×?) with
    101     [ Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
    102     | Proceed ⇒ eval_step … ge st' (\snd b)
    103     | Init _ _ _ _ ⇒
    104       Error … (msg ExecutingInternalCallInBlock)
    105     ]
    106   | FIN ⇒ λb.
    107     ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
    108     match flow return λ_.IO ?? ((fin_step_flow … (block_cont_labels … b))×?) with
    109     [ Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
    110     | Proceed ⇒ eval_fin_step … ge st' (\snd b)
    111     | Init _ _ _ _ ⇒
    112       Error … (msg ExecutingInternalCallInBlock)
    113     ]
    114   ]. try cases l /2 by Exists_append_r, Exists_append_l/ qed.
    115 
    116 (*
    117 lemma m_pred
    118 
    119 lemma attach_m_pred_bind : ∀M.∀MP : MonadPred P.∀P,X,Y.m : monad M X.
    120   ∀f : X → monad M Y.m_pred MP P … m →
    121   ! x ← m ; f x = ! x ← 
    122 *)
    123 
    124 definition no_init : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
    125   λp,globals,lbls,A,flp.
    126   match \fst flp with
    127   [ Init _ _ _ _ ⇒ False
    128   | _ ⇒ True
    129   ].
    130 
    131 definition truly_sequential : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
    132   λp,globals,lbls,A,flp.
    133   match \fst flp with
    134   [ Proceed ⇒ True
    135   | _ ⇒ False
    136   ].
    137 
    138 definition never_calls : ∀p : sem_params.∀globals.genv globals p → joint_step p globals → Prop ≝
    139 λp,globals,ge,s.match s with
    140 [ CALL_ID f args dest ⇒
    141   Try
    142     ! b ← find_symbol … ge f ;
    143     ! fd ← find_funct_ptr … ge b ;
    144     match fd with
    145     [ Internal _ ⇒ return False
    146     | External _ ⇒ return True
    147     ]
    148   catch ⇒
    149     True
    150 | extension c ⇒
    151   ∀st : state p.
    152   pred_io … (λ_.True) (no_init …) (exec_extended … ge c st)
    153 | _ ⇒ True
    154 ].
    155 
    156 definition unbranching ≝ λp,globals,ge,s.never_calls p globals ge s ∧ step_labels … s = [ ].
    157 
    158 lemma err_to_io_bind : ∀O,I,X,Y.∀m : res X.∀f : X → res Y.
    159   err_to_io O I ? (! x ← m ; f x) = ! x ← m : IO O I X ; f x.
    160 #O #I #X #Y * //
    161 qed.
    162 
    163 lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m.
    164 #O #I #X #m elim m // qed.
    165 
    166 (*
    167 lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m.
    168 #X #m elim m // qed.
    169 *)
    170 
    171 (*
    172 lemma never_calls_no_init : ∀p,globals,ge,s.
    173   never_calls p globals ge s →
    174   ∀st : state p.
    175   pred_io … (λ_.True) (no_init …) (eval_step … ge st s).
    176 #p#g#ge * //
    177 [10,12:
    178 |*:
    179   #a #b #c try #d try #e try #f try #g
    180   @res_io_pred
    181   @(mp_bind … (λ_.True) … (pred_res_True …))
    182   #st *  try (@mp_return @I)
    183   @(mp_bind … (λ_.True) … (pred_res_True …))
    184   #st * [9: elim st] normalize nodelta try (@mp_return @I)
    185   @(mp_bind … (λ_.True) … (pred_res_True …))
    186   #st *  try (@mp_return @I)
    187   @(mp_bind … (λ_.True) … (pred_res_True …))
    188   #st * [elim (opaccs ????) #by1 #by2 normalize nodelta]
    189   @(mp_bind … (λ_.True) … (pred_res_True …))
    190   #st * [2: elim (op2 ?????) #by #bit  normalize nodelta]
    191   try (@mp_return @I)
    192   @(mp_bind … (λ_.True) … (pred_res_True …))
    193   #st * @mp_return @I
    194 ]
    195 [ #id #args #dest #H whd in H;
    196   #st change with (! x ← ? ; ?) in match (eval_step ?????);
    197   elim (find_symbol ???) in H ⊢ %; [//]
    198   #b >m_return_bind  >m_return_bind
    199   change with (! x ← ? ; ?) in match (eval_call_block ?????????);
    200   elim (find_funct_ptr ???) [//]
    201   #fd >m_return_bind  >m_return_bind
    202   elim fd #fn normalize nodelta *
    203   @(mp_bind … (λ_.True)) [//]
    204   #st * @(mp_bind … (λ_.True) … (pred_io_True …))
    205   #st * @(mp_bind … (λ_.True) … (pred_io_True …))
    206   #st * @(mp_bind … (λ_.True) … (pred_io_True …))
    207   #st * @mp_return %
    208 | #s #H @H
    209 ]
    210 qed.
    211 
    212 lemma unbranching_truly_sequential : ∀p,globals,ge,s.
    213   unbranching p globals ge s →
    214   ∀st : state p.
    215   pred_io … (λ_.True) (truly_sequential …) (eval_step … ge st s).
    216 #p#globals#ge#s * #H #G #st
    217 lapply (never_calls_no_init … H st) @m_pred_mp
    218 >G * *
    219 [ * #lbl * | #id #fd #args #dest ] #st * %
    220 qed.
    221 *)
    222 
    223 lemma seq_list_labels_append : ∀p,globals,b1,b2.
    224   seq_list_labels p globals (b1 @ b2) =
    225   seq_list_labels … b1 @ seq_list_labels … b2.
    226 #p #g #b1 elim b1
    227 [ //
    228 | #hd #tl #IH #b2 whd in ⊢ (??%%);
    229   >associative_append <IH %
    230 ]
    231 qed.
    232 
    233 (*
    234 lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2.
    235   eval_seq_list globals p ge st (b1@b2) =
    236   ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
    237   match flow with
    238   [ Proceed ⇒
    239     ! 〈flow',st''〉 ← eval_seq_list … ge st' b2 ;
    240     return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉
    241   | _ ⇒ return 〈(flow : step_flow … (seq_list_labels … (b1@b2))), st'〉
    242   ].
    243 [2,3,4:
    244   #lbl #H >seq_list_labels_append
    245   [1,2: @Exists_append_l | @Exists_append_r ] @H ]
    246 #globals#p#ge#st#b1 lapply st -st elim b1
    247 [ #st #b2 >m_return_bind normalize nodelta
    248   <(m_bind_return … (eval_seq_list … b2)) in ⊢ (??%?);
    249   @m_bind_ext_eq **
    250   [ * #lbl #H | #id #fd #args #dest ] #st' %
    251 | #hd #tl #IH #st #b2
    252   whd in match (? @ b2);
    253   whd in match (eval_seq_list ?????);
    254   whd in match (eval_seq_list ???? (hd :: tl));
    255   >m_bind_bind
    256   @m_bind_ext_eq
    257   ** [ #lbl | #id #fd #args #dest] #st' normalize nodelta
    258   [1,2: @m_return_bind]
    259   >m_bind_bind
    260   >IH >m_bind_bind
    261   @m_bind_ext_eq **
    262   [#lbl | #id #fd #args #dest ] #st' normalize nodelta
    263   >m_return_bind
    264   [1,2: @m_return_bind ]
    265   >m_bind_bind normalize nodelta
    266   @m_bind_ext_eq **
    267   [#lbl|#id #fd #args #dest] #st'' >m_return_bind %
    268 ]
    269 qed.
    270 
    271 lemma eval_seq_list_unbranching :
    272 ∀globals,p,ge,st,b.
    273   All ? (unbranching … ge) b →
    274   pred_io … (λ_.True) (truly_sequential …)
    275     (eval_seq_list globals p ge st b).
    276 #globals#p#ge#st #b lapply st -st elim b
    277 [ #st * %
    278 | #hd #tl #IH #st * #hd_ok #tl_ok
    279   @mp_bind
    280   [2: @(unbranching_truly_sequential … hd_ok st) |]
    281   ** [#lbl|#id#fd#args#dest] #st' *
    282   normalize nodelta
    283   @mp_bind [2: @(IH st' tl_ok)|]
    284   ** [#lbl|#id#fd#args#dest] #st'' * %
    285 ]
    286 qed.
    287 
    288 lemma io_pred_as_rel : ∀O,I,A,Perr,P,v.
    289   pred_io O I A Perr P v →
    290   rel_io O I (eq …) … (λx,y.x = y ∧ P x) v v.
    291 #O #I #A #Perr #P #v elim v
    292 [ #o #f #IH whd in ⊢ (%→%);
    293   #H %{(refl …)} #i @IH @H
    294 |*: /2/
    295 ]
    296 qed.
    297 
    298 lemma eval_seq_list_append_unbranching : ∀globals,p,ge,st,b1,b2.
    299   All ? (unbranching … ge) b1 →
    300   eval_seq_list globals p ge st (b1@b2) =
    301   ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
    302   ! 〈flow', st''〉 ← eval_seq_list … ge st' b2 ;
    303   return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉.
    304 [2: #lbl #H >seq_list_labels_append @Exists_append_r @H ]
    305 #globals #p #ge #st #b1 #b2 #H
    306 >eval_seq_list_append
    307 @mr_bind
    308 [2: @(io_pred_as_rel … (eval_seq_list_unbranching … H)) |]
    309 ** [#lbl|#id#fd#args#dest] #st
    310 #y * #EQ <EQ -y * @rel_io_eq normalize nodelta %
    311 qed.
    312 *)
    313 lemma block_cont_labels_append : ∀p,globals,ty,b1,b2.
    314   block_cont_labels p globals ty (b1 @ b2) =
    315   block_cont_labels … b1 @ block_cont_labels … b2.
    316 #p #g #ty * #l1 #s1 * #l2 #s2
    317 whd in match (〈?,?〉@?); whd in ⊢ (??%?);
    318 >seq_list_labels_append
    319 >associative_append
    320 >associative_append
    321 >associative_append %
    322 qed.
    323 (*
    324 lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st.
    325   ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty.
    326   eval_block_cont ??? ge st (b1@b2) =
    327   ! 〈flow, st'〉 ← eval_block_cont ??? ge st b1 ;
    328   match ty return λx.
    329     block_cont p globals x → IO ?? ((stmt_type_if ? x  step_flow fin_step_flow ???) × ?) with
    330   [ SEQ ⇒ λb2.
    331     match flow with
    332     [ Proceed ⇒
    333       ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
    334       return 〈?, st''〉
    335     | Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
    336     | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
    337     ]
    338   | FIN ⇒ λb2.
    339     match flow with
    340     [ Proceed ⇒
    341       ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
    342       return 〈?, st''〉
    343     | Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
    344     | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
    345     ]
    346   ] b2.
    347 [3,5: whd in flow'; @flow'
    348   #lbl >block_cont_labels_append @Exists_append_r
    349 |2,4: cases l -l #l >block_cont_labels_append @Exists_append_l
    350 ]
    351 #globals#p * whd in match stmt_type_if; normalize nodelta
    352 #ge#st * #l1 #s1 * #l2 #s2
    353 whd in match (〈?,?〉@?);
    354 whd in match eval_block_cont; normalize nodelta
    355 >m_bind_bind
    356 >eval_seq_list_append
    357 >m_bind_bind
    358 @m_bind_ext_eq
    359 
    360  whd in ⊢ (??%?);
    361     match ty return λx.IO ?? ((stmt_type_if ? x ?????) × ?) with
    362     [ SEQ ⇒
    363     | FIN ⇒ return 〈FRedirect ??? «l,?», st'〉
    364     ]
    365   | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
    366   ].
    367 #globals#p#ty#ge#st*#l1#s1*#l2#s2
    368 whd in match (〈?,?〉@?);
    369 whd in match eval_block_cont; normalize nodelta
    370 >m_bind_bind
    371 >eval_seq_list_append
    372 >m_bind_bind
    373 @m_bind_ext_eq
    374 ** [#l|#id#fd#args#dest] normalize nodelta #st'
    375 [1,2:>m_return_bind normalize nodelta
    376   [ >m_return_bind ] % ]
    377 change with (! x ← ? ; ?) in match (eval_seq_list ???? (?::?));
    378 >m_bind_bind whd in match stmt_type_if;
    379 normalize nodelta
    380 >m_bind_bind
    381 @m_bind_ext_eq
    382 **[#l|#id#fd#args#dest] normalize nodelta #st''
    383 [1,2: >m_return_bind normalize nodelta % | % ]
    384 qed.
    385 *)
    386 
    387 
    388 (* just like repeat, but without the full_exec infrastructure, and it
    389    stops upon a non-proceed flow cmd *)
    390 let rec repeat_eval_state_flag n globals (p:sem_params) (ge : genv globals p)
    391   (st : state_pc p) on n :
    392     IO io_out io_in (bool × (state_pc p)) ≝
    393 match n with
    394 [ O ⇒ return 〈false,st〉
    395 | S k ⇒
    396   ! 〈flag,st'〉 ← eval_state_flag globals p ge st ;
    397   if flag then return 〈true,st'〉 else repeat_eval_state_flag k globals p ge st'
    398 ].
    399 
    400 definition block_size : ∀p,g,ty.block_cont p g ty → ℕ ≝
    401 λp,g,ty,b.S (|\fst b|).
    402 
    403 interpretation "block cont size" 'norm b = (block_size ??? b).
    404 
    405 lemma repeat_eval_state_flag_plus : ∀n1,n2,globals, p, ge, st.
    406   repeat_eval_state_flag (n1 + n2) globals p ge st =
    407   ! 〈flag,st〉 ← repeat_eval_state_flag n1 globals p ge st ;
    408   if flag then return 〈true, st〉 else repeat_eval_state_flag n2 globals p ge st.
    409 #n1 elim n1 -n1 [| #n1 #IH]
    410 #n2 #globals #p #ge #st
    411 [ @m_return_bind
    412 | change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
    413   change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S n1) ????);
    414   >m_bind_bind in ⊢ (???%);
    415   @m_bind_ext_eq ** #st' normalize nodelta
    416   [ % | @IH ]
    417 ]
    418 qed.
    419 
    420 lemma repeat_eval_state_flag_one : ∀globals, p, ge, st.
    421   repeat_eval_state_flag 1 globals p ge st = eval_state_flag globals p ge st.
    422 #globals #p #ge #st
    423 change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
    424 <(m_bind_return … (eval_state_flag ????)) in ⊢ (???%);
    425 @m_bind_ext_eq ** #st %
    426 qed.
    427 
    428 lemma eval_tunnel_step :
    429   ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
    430   fetch_function … ge (pc … st) = OK … fn →
    431   point_of_pointer ? p … (pc … st) = OK … src →
    432   src ~~> dst in joint_if_code … fn →
    433   eval_state_flag g p ge st =
    434     return 〈true,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
    435 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #lbl * #EQ1 #EQ2
    436 change with (! s ← ? ; ?) in match (eval_state_flag ????);
    437 change with (! fn ← ? ; ?) in match (fetch_statement ?????);
    438 >pc_pt in ⊢ (??%?); >m_return_bind
    439 >fetch_fn in ⊢ (??%?); >m_return_bind
    440 >EQ1 in ⊢ (??%?);  >m_return_bind
    441 >EQ2 in ⊢ (??%?);
    442 change with (! st ← ? ; ?) in match (eval_statement ?????);
    443 whd in match eval_fin_step; normalize nodelta
    444 >m_return_bind
    445 whd in match eval_fin_step_flow; normalize nodelta
    446 change with (! ptr ← ? ; ?) in match (goto ??????);
    447 whd in match pointer_of_label_in_block; normalize nodelta
    448 whd in match fetch_function in fetch_fn;
    449 normalize nodelta in fetch_fn;
    450 >fetch_fn in ⊢ (??%?); >m_return_bind
    451 >EQ2 in ⊢ (??%?); >m_return_bind
    452 cases st #st' ** #ty ** #id #H #o #EQ destruct(EQ)
    453 elim (pointer_compat_from_ind … H) %
    454 qed.
    455 
    456 lemma fetch_function_from_block_eq :
    457   ∀p,g,ge.
    458   ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
    459   fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
    460 #p #g #ge #ptr1 #ptr2 #EQ
    461 whd in match fetch_function; normalize nodelta >EQ
    462 @m_bind_ext_eq // qed.
    463 
    464 (*
    465 lemma eval_tunnel :
    466   ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
    467   fetch_function … ge (pc … st) = OK … fn →
    468   point_of_pointer ? p … (pc … st) = OK … src →
    469   src ~~>^* dst in joint_if_code … fn →
    470   ∃n.repeat_eval_state n g p ge st =
    471     return 〈f,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
    472 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #through
    473 lapply pc_pt -pc_pt lapply fetch_fn -fetch_fn lapply src -src lapply st -st
    474 elim through [2: #hd #tl #IH]
    475 #st #src #fetch_fn #pc_pt
    476 [2: #EQ <EQ %{0}
    477   >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st // ]
    478 * #H1 #H2
    479 letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) hd) st)
    480 elim (IH st' … H2)
    481 [3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
    482   @pointer_of_point_block
    483 |2:
    484   whd in match st'; >point_of_pointer_of_point %
    485 ]
    486 #n' #EQ %{(S n')}
    487 change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
    488 >(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
    489 >EQ %
    490 qed.
    491 
    492 lemma eval_tunnel_plus :
    493   ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
    494   fetch_function … ge (pc … st) = OK … fn →
    495   point_of_pointer ? p … (pc … st) = OK … src →
    496   src ~~>^+ dst in joint_if_code … fn →
    497   ∃n.repeat_eval_state (S n) g p ge st =
    498     return set_pc … (pointer_of_point ? p (pc … st) dst) st.
    499 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #mid * #H1 #H2
    500 letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
    501 elim (eval_tunnel … ge st' … H2)
    502 [3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
    503   @pointer_of_point_block
    504 |2:
    505   whd in match st'; >point_of_pointer_of_point %
    506 ]
    507 #n #EQ %{n}
    508 change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
    509 >(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
    510 >EQ %
    511 qed.
    512 *)
     8  ].*)
    5139
    51410lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer.
     
    52218>EQ1 >m_return_bind >EQ3 %
    52319qed.
    524 (*
    525 lemma eval_seq_list_in_code :
    526   ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
    527   fetch_function … ge (pc … st) = OK … fn →
    528   point_of_pointer ? p … (pc … st) = OK … src →
    529   All ? (never_calls … ge) B →
    530   seq_list_in_code … (joint_if_code … fn) src B dst →
    531   repeat_eval_state_flag (|B|) g p ge st =
    532    ! 〈flow,st'〉 ← eval_seq_list g p ge st B ;
    533    match flow with
    534    [ Redirect l ⇒
    535      ! st'' ← goto ?? ge l st' (pblock … (pc ? st)) ;
    536      return 〈true, st''〉
    537    | Init id fn args dest ⇒ Error … (msg ExecutingInternalCallInBlock)
    538        (* dummy, never happens *)
    539    | Proceed ⇒
    540      let nxt_ptr ≝ pointer_of_point p p … (pc … st) dst in
    541      return 〈false, mk_state_pc ? st' nxt_ptr〉
    542    ].
    543 #p #g #ge #st #fn #src #B lapply src -src
    544 lapply st -st elim B [|#hd #tl #IH]
    545 #st #src #dst #fetch_fn #pc_pt * [2: #hd_ok #tl_ok]
    546 [2: #EQ normalize in EQ; <EQ
    547   whd in match (eval_seq_list ???? [ ]);
    548   >m_return_bind normalize nodelta
    549   >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st //
    550 |1: * #n * #EQat #H
    551   change with (! st' ← ? ; ?) in match (eval_seq_list ?????);
    552   change with (! st' ← ? ; ?) in match (repeat_eval_state_flag ?????);
    553   >m_bind_bind
    554   >(fetch_statement_eq … fetch_fn pc_pt EQat) >m_return_bind
    555   >m_bind_bind >m_bind_bind
    556   lapply (never_calls_no_init … hd_ok st) #hd_ok'
    557   @(mr_bind …
    558     (λfst1,fst2.fst1 = fst2 ∧ no_init … fst1))
    559   [ lapply hd_ok' elim (eval_step ?????)
    560     [ #o #f #IH'
    561       whd in ⊢ (%→%); #G
    562       %{(refl …)} #i @IH' @G
    563     |*: #v whd in ⊢ (%→%); #H
    564       % [ % ] @H
     20
     21include alias "basics/logic.ma".
     22lemma io_evaluate_bind : ∀O,I,X,Y,env.
     23∀m : IO O I X.∀f : X → IO O I Y.
     24io_evaluate O I Y env (! x ← m ; f x) =
     25! x ← io_evaluate O I X env m ;
     26io_evaluate O I Y env (f x).
     27#O #I #X #Y #env #m elim m
     28[ #o #g #IH #f whd in match (! x ← Interact ????? ; ?);
     29  change with (! y ← ? ; ?) in ⊢ (??%(????%?));
     30  >m_bind_bind @m_bind_ext_eq #i @IH
     31| #x #f %
     32| #e #f %
     33]
     34qed.
     35
     36lemma fetch_function_from_block_eq :
     37  ∀p,g,ge.
     38  ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
     39  fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
     40#p #g #ge #ptr1 #ptr2 #EQ
     41whd in match fetch_function; normalize nodelta >EQ
     42@m_bind_ext_eq // qed.
     43
     44let rec repeat_eval_seq_no_pc
     45  (p : evaluation_params) env
     46  (l : list (joint_seq p (globals p))) on l :
     47  state p → res (state p) ≝
     48  λst.match l with
     49  [ nil ⇒ return st
     50  | cons hd tl ⇒
     51    ! st' ← io_evaluate … (env st) (eval_seq_no_pc (globals p) p (ev_genv p) st hd) ;
     52    repeat_eval_seq_no_pc p env tl st'
     53  ].
     54
     55lemma err_to_io_evaluate : ∀O,I,X,env,m.
     56  io_evaluate O I X env (err_to_io … m) = m.
     57#O#I#X#env * // qed.
     58
     59definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
     60
     61definition no_call_nor_label : ∀p,g.joint_seq p g → bool ≝
     62  λp,g,s.match s with
     63  [ COST_LABEL _ ⇒ false
     64  | CALL_ID _ _ _ ⇒ false
     65  | extension_call _ ⇒ false
     66  | _ ⇒ true
     67  ].
     68
     69lemma no_call_nor_label_proceed : ∀p : evaluation_params.
     70∀st : state p. ∀s.
     71no_call_nor_label p (globals p) s →
     72eval_seq_pc (globals p) p (ev_genv p) st s = return Proceed ???.
     73#p #st * // [ #f #args #dest | #c ] *
     74qed.
     75
     76lemma no_call_nor_label_other : ∀p : evaluation_params.∀s.
     77no_call_nor_label p (globals p) s →
     78step_classifier … s = cl_other.
     79#p * // [ #f #args #dest | #c ] *
     80qed.
     81
     82lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt.
     83no_call_nor_label p (globals p) s →
     84cost_label_of_stmt … (sequential … s nxt) = None ?.
     85#p * // #lbl#next *
     86qed.
     87
     88let rec produce_trace_any_any
     89  (p : evaluation_params)
     90  (st : state_pc p) fd
     91  (src : code_point p)
     92  (b : list (joint_seq p (globals p))) on b :
     93  ∀l : list (code_point p).
     94  ∀dst : code_point p.
     95  ∀st' : state p.
     96  fetch_function p ? (ev_genv p) (pc … st) = return fd →
     97  point_of_pointer p p (pc … st) = return src →
     98  if list_not_empty ? b then
     99    ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?
     100  else
     101    True →
     102  src ~❨b, l❩~> dst in joint_if_code … fd →
     103  All ? (λx.bool_to_Prop (no_call_nor_label … x)) b →
     104  repeat_eval_seq_no_pc p (io_env p) b st = return st' →
     105  trace_any_any (joint_abstract_status p) st
     106    (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ≝
     107  match b
     108  return λx.?→?→?→?→?→?→?→?→?→?
     109  with
     110  [ nil ⇒
     111    λl,dst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
     112    (taa_base (joint_abstract_status p) st)
     113      ⌈trace_any_any (joint_abstract_status p) st st ↦
     114       trace_any_any (joint_abstract_status p) st
     115        (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst))⌉
     116  | cons hd tl ⇒
     117    λl.
     118    match l return λx.?→?→?→?→?→?→?→?→? with
     119    [ nil ⇒ λdst,st',fd_prf,src_prf,dst_prf,in_code.⊥
     120    | cons mid rest ⇒
     121      λdst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
     122      match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd)
     123      return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd) = x → ?
     124      with
     125      [ OK st_mid ⇒ λEQ2.
     126        taa_step (joint_abstract_status p) st ?
     127          (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ???
     128          (produce_trace_any_any ?
     129            (mk_state_pc ? st_mid (pointer_of_point ? p (pc ? st) mid))
     130            fd mid tl rest dst ???????)
     131      | Error _ ⇒ λEQ2.⊥
     132      ] (refl …)
    565133    ]
    566   | ** [#lbl | #id #fd #args #dest ] #st'
    567     #y * #EQ <EQ -y * normalize nodelta @rel_io_eq
    568     whd in match succ_pc; normalize nodelta
    569     >pc_pt >m_return_bind
    570     letin src' ≝ (point_of_succ p src n) in H ⊢ %;
    571     letin pc' ≝ (pointer_of_point p p … (pc ? st) src') #H
    572     [>m_return_bind whd in match eval_step_flow; normalize nodelta
    573      whd in match (pblock ?);
    574      elim (goto … ge lbl st' ?)
    575      [ #st'' >m_return_bind %
    576      | #e %
    577      ]
    578     | normalize nodelta in IH ⊢ %; @(IH … tl_ok H)
    579       [ @fetch_fn
    580       | @point_of_pointer_of_point
     134  ].
     135  [ cases l in in_code; [2: #mid #rest *] normalize in ⊢ (%→?); #EQ
     136    cases st in src_prf EQ1; -st #st #pc
     137    #src_prf normalize in ⊢ (%→?); #EQ1 destruct
     138    >(pointer_of_point_of_pointer … src_prf) %
     139  | elim in_code
     140  |12: lapply EQ1 whd in ⊢ (??%?→?);
     141    >EQ2 normalize #ABS destruct(ABS)
     142  |*:
     143    elim in_code
     144    * #nxt * #EQ3 #EQ4 #Hrest
     145    elim all_other
     146    #hd_other #tl_other
     147    [ whd whd in match eval_state; normalize nodelta
     148      >(fetch_statement_eq … fd_prf src_prf EQ3) >m_return_bind
     149      whd in match eval_statement; normalize nodelta
     150      whd in match eval_step; normalize nodelta
     151      >m_bind_bind
     152      >(no_call_nor_label_proceed … hd_other) >m_return_bind
     153      >m_bind_bind
     154      >io_evaluate_bind >EQ2 >m_return_bind
     155      >m_return_bind
     156      whd in match succ_pc; normalize nodelta
     157      >m_bind_bind >src_prf >m_return_bind >m_return_bind
     158      whd in match eval_step_flow; normalize nodelta
     159      whd in ⊢ (??%%); >EQ4
     160      >EQ2 %
     161    | %{(sequential … hd nxt)} %{(fetch_statement_eq … fd_prf src_prf EQ3)}
     162      cases all_other #hd_other #_
     163      whd in match stmt_classifier; normalize nodelta
     164      @no_call_nor_label_other assumption
     165    | %* #H @H -H whd in ⊢ (??%?);
     166      cases tl in Hrest tl_other;
     167      [ cases rest [2: #hd' #tl' *] normalize in ⊢ (%→?); #EQ' destruct(EQ') *
     168        lapply dst_prf
     169        whd in match (as_pc_of ??);
     170        whd in match fetch_statement; normalize nodelta
     171        whd in match point_of_pointer; normalize nodelta
     172        >point_of_offset_of_point
     173        >m_return_bind
     174        >fetch_function_from_block_eq
     175        [ >fd_prf
     176          >m_return_bind
     177          cases (stmt_at ????)
     178          [ #_ %
     179          | #stmt #H @H
     180          ]
     181        | %
     182        |
     183        ]
     184      | #hd' #tl' cases rest [*] #mid' #rest' * * #next' * #EQ5 #EQ6
     185        #_ * #hd_other' #_
     186        >fetch_statement_eq try assumption
     187        [ @no_call_nor_label_uncosted assumption
     188        | whd in match (as_pc_of ??);
     189          whd in ⊢ (??%?);
     190          >point_of_offset_of_point %
     191        ]
    581192      ]
     193    | change with (! x ← ?;?) in EQ1 : (??%?);
     194      >EQ2 in EQ1; #H @H
     195    | assumption
     196    | assumption
     197    | cases (list_not_empty ??) [ assumption | % ]
     198    | @point_of_pointer_of_point
     199    | <fd_prf @fetch_function_from_block_eq %
    582200    ]
    583201  ]
    584 ]
    585 qed.
    586 
    587 definition eval_block_cont_pc :
    588   ∀globals.∀p : sem_params.∀ty.genv globals p →
    589   state_pc p → block_cont p globals ty → stmt_type_if ? ty (code_point p) unit →
    590   IO io_out io_in (bool × (state_pc p)) ≝
    591   λglobals,p,ty,ge,st,b,nxt.
    592   ! 〈flow, st'〉 ← eval_block_cont globals p ty ge st b ;
    593   match ty return λx.stmt_type_if ? x ?? → stmt_type_if ? x ?? → ? with
    594   [ SEQ ⇒ λflow,nxt.eval_step_flow ?? ge st'
    595         (pointer_of_point ? p (pc ? st) nxt) flow
    596   | FIN ⇒ λflow.λ_.
    597     ! st' ← eval_fin_step_flow ?? ge st' (pblock … (pc ? st)) flow ;
    598     return 〈true, st'〉
    599   ] flow nxt.
    600 
    601 lemma eval_block_cont_in_code :
    602   ∀p : sem_params.∀g,ty.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
    603   fetch_function … ge (pc … st) = OK … fn →
    604   point_of_pointer ? p … (pc … st) = OK … src →
    605   All ? (never_calls … ge) (\fst B) →
    606   src ~❨B❩~> dst in joint_if_code … fn →
    607   repeat_eval_state_flag (|B|) g p ge st =
    608     eval_block_cont_pc g p ty ge st B dst.
    609 #p #g #ty #ge #st #fn #src * #l #s #dst #fetch_fn #pc_pt #l_ok
    610 * #mid * #l_in_code #s_in_code
    611 change with (1 + |l|) in match (|?|);
    612 >commutative_plus
    613 >repeat_eval_state_flag_plus
    614 change with (! x ← ? ; ?) in ⊢ (???%);
    615 >m_bind_bind
    616 >(eval_seq_list_in_code … fetch_fn pc_pt l_ok l_in_code)
    617 >m_bind_bind
    618 @m_bind_ext_eq ** [#lbl | #id #fd #args #dest] #st'
    619 normalize nodelta
    620 [ -s_in_code lapply dst -dst cases ty
    621   whd in match stmt_type_if; normalize nodelta
    622   #dst >m_return_bind
    623   [whd in match eval_step_flow; | whd in match eval_fin_step_flow; ]
    624   normalize nodelta
    625   whd in match (pblock ?);
    626   elim (goto g p ge lbl st' ?) #x //
    627 | %
    628 | >m_return_bind normalize nodelta
    629   >repeat_eval_state_flag_one
    630   >m_bind_bind
    631   lapply s_in_code -s_in_code lapply dst -dst lapply s -s cases ty
    632   whd in match stmt_type_if; normalize nodelta
    633   #s #dst [* #n * ] #s_in_code [ #n_is_dst ]
    634   whd in match eval_state_flag; normalize nodelta
    635   letin pc' ≝ (pointer_of_point p p (pc ? st) mid)
    636   letin st_pc' ≝ (mk_state_pc ? st' pc')
    637   >(fetch_statement_eq … ?? s_in_code)
    638   [2,5: @point_of_pointer_of_point
    639   |3,6: @fetch_fn
    640   |*: >m_return_bind
    641     whd in match eval_statement; normalize nodelta
    642     @m_bind_ext_eq * #flow #st'' >m_return_bind [2:%]
    643     whd in match succ_pc; normalize nodelta
    644     >point_of_pointer_of_point >m_return_bind
    645     >pointer_of_point_of_pointer [2: @refl |*:]
    646     [ >point_of_pointer_of_point >n_is_dst %
    647     | %
    648     ]
    649   ]
    650 ]
    651 qed.
    652      cases dst [*] #z @eval_tunnel assumption
    653 | cases dst [2: #z *]]
    654 * #mid * #tunn [#H | * #n * #H #G ]
    655   elim (eval_tunnel … fetch_fn pc_pt tunn)
    656   #n
    657   letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
    658   #EQ1
    659   cut (point_of_pointer ? p … (pc … st') = OK … mid)
    660   [1,3:
    661     whd in match st'; >point_of_pointer_of_point % ] #pc_pt'
    662   cut (fetch_function p … ge (pc … st') = OK … fn)
    663   [1,3: >fetch_function_from_block_eq [1,4:@fetch_fn |*:] whd in match st';
    664     @pointer_of_point_block] #fetch_fn'
    665   [ %{(n + 1)}
    666   >repeat_eval_state_plus >EQ1 >m_return_bind
    667   >repeat_eval_state_one change with (None ?) in match (! x ← None ? ; ?);
    668   change with (! 〈flow,tr,st〉 ← ? ; ?) in match (eval_block_cont ??????);
    669   change with (! s ← ? ; ?) in match (eval_state ????);
    670   >(fetch_statement_eq … fetch_fn' pc_pt' H) >m_return_bind
    671   >m_bind_bind
    672   change with ( ! x ← ? ; ?) in match (eval_block_cont ???????);
    673   cases s *
    674  
    675   @m_bind_ext_eq' ** #flow #tr1 #st1 normalize nodelta
    676   >m_bind_bind change with st' in match (set_pc ???); @m_bind_ext_eq
    677   change with (! fn ← ? ; ?) in match (fetch_statement ?????);
    678   >m_bind_bind in ⊢ (??%?);
    679   change with (pointer_of_point ????) in match (pc ??);
    680   >point_of_pointer_of_point >m_return_bind
    681   >(fetch_function_from_block_eq ???? (pc … st))
    682   [2: @pointer_of_point_block ]
    683   >fetch_fn >m_return_bind >H2 >m_return_bind
    684   >m_bind_bind
    685   change with (! x ← ? ; ?) in ⊢ (???%);
    686   >fetch_fn n ⊢ (??(????%?)?); >m_return_bind
    687   >(stmt_at_to_safe … src_prf) in ⊢ (??(????%?)?);
    688   >H1 in ⊢ (??(????%?)?);
    689   whd in ⊢ (??(λ_.???%));
    690 elim b
    691 [ #st #dst #fetch_fn #prf #through
    692   #H elim (block_cont_to_tunnel … H) #dst'
    693   * #EQdst >EQdst >m_return_bind #G
    694   elim (eval_tunnel … fetch_fn prf … G) #x #EQ %{x}
    695   >EQ %
    696 |
    697 
    698  #dst #fetch_fn #prf #through
    699 lapply prf -prf lapply fetch_fn -fetch_fn
    700 lapply b -b lapply st -st
    701 elim through [2: #hd #tl #IH]
    702 [2:
    703  
    704 #st * [1,4,7,10:|2,5,8,11:#s|3,6,9,12:#s#b'] #fetch_fn #prf
    705 normalize in ⊢(%→?);
    706 [8: #EQ1 |*: * [5: |*: *] #lbl [ |*: *] * #H1 #H2 [|*: #H3] #x [ *
    707 [ * || * | * #lbl
    708  * #lbl * [*] #H1 #H2 [#H3]
    709  
    710 let rec block_cont_in_code (p : sem_params) g (b : block_cont p g)
    711   (following : option (succ p)) (c : codeT p g) (at : cpointer) on b : Prop ≝
    712   match b with
    713   [ Skip ⇒
    714     match following with
    715     [ Some l ⇒ succ_pc p p
    716 *)
     202qed.
Note: See TracChangeset for help on using the changeset viewer.