Ignore:
Timestamp:
May 15, 2012, 5:51:25 PM (8 years ago)
Author:
tranquil
Message:
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r1882 r1949  
    22include "joint/semantics_paolo.ma".
    33
    4 (* WARNING: all the following breaks apart if statements are allowed to depend
    5    on flow. Execution of blocks does not update flow information in the state
    6    (e.g. the program counter) until the end *)
    7 
    8 definition goto_no_seq : ∀g.∀p:sem_params.genv g p → label →
    9   state p → Z → res (state_pc p) ≝ λg,p,ge,lbl,st,id.
    10       ! newpc ← pointer_of_label ? p … ge
    11         (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) lbl ;
    12       return mk_state_pc … st newpc. % qed.
    13 
    14 lemma goto_no_seq_to_normal : ∀p : sem_params.∀g,ge.∀st : state_pc p.∀id,lbl.
    15   block_id (pblock (pc p st)) = id →
    16   goto_no_seq g p ge lbl st id = goto g p ge lbl st.
    17 #p #g #ge * #st ** #typ * #r #id
    18 #H inversion H [1,3: #r'] #id'
    19 #EQ1 #EQ2 #EQ3 #o #EQ4 #id'' #lbl #EQ5 destruct
    20 whd in match goto_no_seq;
    21 whd in match goto; normalize nodelta //
    22 qed.
    23 
    24 (* executes a block of instructions, until its end or before if a
    25    function call or a redirection is encountered. If executed until end,
    26    or is a non-tail call is encountered, the next program counter must be
    27    provided *)
    28 let rec eval_block_cont globals (p:sem_params) (ge : genv globals p)
    29   (st : state p) id (b : block_cont p globals) (dst : option cpointer) on b :
    30     IO io_out io_in (trace×(state_pc p)) ≝
     4
     5axiom ExecutingInternalCallInBlock : String.
     6
     7let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
    318  match b with
    32   [ Skip ⇒
    33     ! nxt ← opt_to_res … (msg SuccessorNotProvided) dst ;
    34     return 〈E0, mk_state_pc ? st nxt〉
    35   | Final s ⇒
    36     ! 〈flow, tr, st'〉 ← eval_statement_no_seq … ge st s;
    37     ! st ← eval_stmt_flow_no_seq … ge st' id flow;
    38     return 〈tr, st〉
    39   | Cons hd tl ⇒
    40     ! 〈flow, tr1, st'〉 ← eval_step ?? ge st hd ;
     9  [ nil ⇒ [ ]
     10  | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl
     11  ].
     12
     13definition 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
     23coercion 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
     28definition 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
     35coercion 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
     40let 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
     53definition 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
     63coercion 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
     68definition 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
     75coercion 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
     80definition 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
     87definition 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
     116lemma m_pred
     117
     118lemma attach_m_pred_bind : ∀M.∀MP : MonadPred P.∀P,X,Y.m : monad M X.
     119  ∀f : X → monad M Y.m_pred MP P … m →
     120  ! x ← m ; f x = ! x ← 
     121
     122definition no_init : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
     123  λp,globals,lbls,A,flp.
     124  match \fst flp with
     125  [ Init _ _ _ _ ⇒ False
     126  | _ ⇒ True
     127  ].
     128
     129definition truly_sequential : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
     130  λp,globals,lbls,A,flp.
     131  match \fst flp with
     132  [ Proceed ⇒ True
     133  | _ ⇒ False
     134  ].
     135
     136definition never_calls : ∀p : sem_params.∀globals.genv globals p → joint_step p globals → Prop ≝
     137λp,globals,ge,s.match s with
     138[ CALL_ID f args dest ⇒
     139  Try
     140    ! b ← find_symbol … ge f ;
     141    ! fd ← find_funct_ptr … ge b ;
     142    match fd with
     143    [ Internal _ ⇒ return False
     144    | External _ ⇒ return True
     145    ]
     146  catch ⇒
     147    True
     148| extension c ⇒
     149  ∀st : state p.
     150  pred_io … (λ_.True) (no_init …) (exec_extended … ge c st)
     151| _ ⇒ True
     152].
     153
     154definition unbranching ≝ λp,globals,ge,s.never_calls p globals ge s ∧ step_labels … s = [ ].
     155
     156lemma err_to_io_bind : ∀O,I,X,Y.∀m : res X.∀f : X → res Y.
     157  err_to_io O I ? (! x ← m ; f x) = ! x ← m : IO O I X ; f x.
     158#O #I #X #Y * //
     159qed.
     160
     161lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m.
     162#O #I #X #m elim m // qed.
     163lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m.
     164#X #m elim m // qed.
     165
     166lemma never_calls_no_init : ∀p,globals,ge,s.
     167  never_calls p globals ge s →
     168  ∀st : state p.
     169  pred_io … (λ_.True) (no_init …) (eval_step … ge st s).
     170#p#g#ge * //
     171[10,12:
     172|*:
     173  #a #b #c try #d try #e try #f try #g
     174  @res_io_pred
     175  @(mp_bind … (λ_.True) … (pred_res_True …))
     176  #st *  try (@mp_return @I)
     177  @(mp_bind … (λ_.True) … (pred_res_True …))
     178  #st * [9: elim st] normalize nodelta try (@mp_return @I)
     179  @(mp_bind … (λ_.True) … (pred_res_True …))
     180  #st *  try (@mp_return @I)
     181  @(mp_bind … (λ_.True) … (pred_res_True …))
     182  #st * [elim (opaccs ????) #by1 #by2 normalize nodelta]
     183  @(mp_bind … (λ_.True) … (pred_res_True …))
     184  #st * [2: elim (op2 ?????) #by #bit  normalize nodelta]
     185  try (@mp_return @I)
     186  @(mp_bind … (λ_.True) … (pred_res_True …))
     187  #st * @mp_return @I
     188]
     189[ #id #args #dest #H whd in H;
     190  #st change with (! x ← ? ; ?) in match (eval_step ?????);
     191  elim (find_symbol ????) in H ⊢ %; [//]
     192  #b >m_return_bind  >m_return_bind
     193  change with (! x ← ? ; ?) in match (eval_call_block ?????????);
     194  elim (find_funct_ptr ????) [//]
     195  #fd >m_return_bind  >m_return_bind
     196  elim fd #fn normalize nodelta *
     197  @(mp_bind … (λ_.True)) [//]
     198  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
     199  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
     200  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
     201  #st * @mp_return %
     202| #s #H @H
     203]
     204qed.
     205
     206lemma unbranching_truly_sequential : ∀p,globals,ge,s.
     207  unbranching p globals ge s →
     208  ∀st : state p.
     209  pred_io … (λ_.True) (truly_sequential …) (eval_step … ge st s).
     210#p#globals#ge#s * #H #G #st
     211lapply (never_calls_no_init … H st) @m_pred_mp
     212>G * *
     213[ * #lbl * | #id #fd #args #dest ] #st * %
     214qed.
     215
     216lemma seq_list_labels_append : ∀p,globals,b1,b2.
     217  seq_list_labels p globals (b1 @ b2) =
     218  seq_list_labels … b1 @ seq_list_labels … b2.
     219#p #g #b1 elim b1
     220[ //
     221| #hd #tl #IH #b2 whd in ⊢ (??%%);
     222  >associative_append <IH %
     223]
     224qed.
     225
     226lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2.
     227  eval_seq_list globals p ge st (b1@b2) =
     228  ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
     229  match flow with
     230  [ Proceed ⇒
     231    ! 〈flow',st''〉 ← eval_seq_list … ge st' b2 ;
     232    return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉
     233  | _ ⇒ return 〈(flow : step_flow … (seq_list_labels … (b1@b2))), st'〉
     234  ].
     235[2,3,4:
     236  #lbl #H >seq_list_labels_append
     237  [1,2: @Exists_append_l | @Exists_append_r ] @H ]
     238#globals#p#ge#st#b1 lapply st -st elim b1
     239[ #st #b2 >m_return_bind normalize nodelta
     240  <(m_bind_return … (eval_seq_list … b2)) in ⊢ (??%?);
     241  @m_bind_ext_eq **
     242  [ * #lbl #H | #id #fd #args #dest ] #st' %
     243| #hd #tl #IH #st #b2
     244  whd in match (? @ b2);
     245  whd in match (eval_seq_list ?????);
     246  whd in match (eval_seq_list ???? (hd :: tl));
     247  >m_bind_bind
     248  @m_bind_ext_eq
     249  ** [ #lbl | #id #fd #args #dest] #st' normalize nodelta
     250  [1,2: @m_return_bind]
     251  >m_bind_bind
     252  >IH >m_bind_bind
     253  @m_bind_ext_eq **
     254  [#lbl | #id #fd #args #dest ] #st' normalize nodelta
     255  >m_return_bind
     256  [1,2: @m_return_bind ]
     257  >m_bind_bind normalize nodelta
     258  @m_bind_ext_eq **
     259  [#lbl|#id #fd #args #dest] #st'' >m_return_bind %
     260]
     261qed.
     262
     263lemma eval_seq_list_unbranching :
     264∀globals,p,ge,st,b.
     265  All ? (unbranching … ge) b →
     266  pred_io … (λ_.True) (truly_sequential …)
     267    (eval_seq_list globals p ge st b).
     268#globals#p#ge#st #b lapply st -st elim b
     269[ #st * %
     270| #hd #tl #IH #st * #hd_ok #tl_ok
     271  @mp_bind
     272  [2: @(unbranching_truly_sequential … hd_ok st) |]
     273  ** [#lbl|#id#fd#args#dest] #st' *
     274  normalize nodelta
     275  @mp_bind [2: @(IH st' tl_ok)|]
     276  ** [#lbl|#id#fd#args#dest] #st'' * %
     277]
     278qed.
     279
     280lemma io_pred_as_rel : ∀O,I,A,Perr,P,v.
     281  pred_io O I A Perr P v →
     282  rel_io O I (eq …) … (λx,y.x = y ∧ P x) v v.
     283#O #I #A #Perr #P #v elim v
     284[ #o #f #IH whd in ⊢ (%→%);
     285  #H %{(refl …)} #i @IH @H
     286|*: /2/
     287]
     288qed.
     289
     290lemma eval_seq_list_append_unbranching : ∀globals,p,ge,st,b1,b2.
     291  All ? (unbranching … ge) b1 →
     292  eval_seq_list globals p ge st (b1@b2) =
     293  ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
     294  ! 〈flow', st''〉 ← eval_seq_list … ge st' b2 ;
     295  return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉.
     296[2: #lbl #H >seq_list_labels_append @Exists_append_r @H ]
     297#globals #p #ge #st #b1 #b2 #H
     298>eval_seq_list_append
     299@mr_bind
     300[2: @(io_pred_as_rel … (eval_seq_list_unbranching … H)) |]
     301** [#lbl|#id#fd#args#dest] #st
     302#y * #EQ <EQ -y * @rel_io_eq normalize nodelta %
     303qed.
     304
     305lemma block_cont_labels_append : ∀p,globals,ty,b1,b2.
     306  block_cont_labels p globals ty (b1 @ b2) =
     307  block_cont_labels … b1 @ block_cont_labels … b2.
     308#p #g #ty * #l1 #s1 * #l2 #s2
     309whd in match (〈?,?〉@?); whd in ⊢ (??%?);
     310>seq_list_labels_append
     311>associative_append
     312>associative_append
     313>associative_append %
     314qed.
     315
     316lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st.
     317  ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty.
     318  eval_block_cont ??? ge st (b1@b2) =
     319  ! 〈flow, st'〉 ← eval_block_cont ??? ge st b1 ;
     320  match ty return λx.
     321    block_cont p globals x → IO ?? ((stmt_type_if ? x  step_flow fin_step_flow ???) × ?) with
     322  [ SEQ ⇒ λb2.
    41323    match flow with
    42     [ Proceed ⇒
    43       ! 〈tr2, st〉 ← eval_block_cont globals p ge st id tl dst ;
    44       return 〈tr1 ⧺ tr2, st〉
    45     | Init id fn args dest ⇒
    46       ! ra ← opt_to_res … (msg SuccessorNotProvided) dst ;
    47       let st' ≝ set_frms … (save_frame … ra dest st) st in
    48       ! st ← do_call ?? ge st' id fn args ;
    49       return 〈tr1, st〉
    50     | Redirect l ⇒
    51       ! st ← goto_no_seq ? p … ge l st id ;
    52       return 〈tr1, st〉
    53     ]
     324    [ Proceed ⇒
     325      ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
     326      return 〈?, st''〉
     327    | Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
     328    | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
     329    ]
     330  | FIN ⇒ λb2.
     331    match flow with
     332    [ Proceed ⇒
     333      ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
     334      return 〈?, st''〉
     335    | Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
     336    | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
     337    ]
     338  ] b2.
     339[3,5: whd in flow'; @flow'
     340  #lbl >block_cont_labels_append @Exists_append_r
     341|2,4: cases l -l #l >block_cont_labels_append @Exists_append_l
     342]
     343#globals#p * whd in match stmt_type_if; normalize nodelta
     344#ge#st * #l1 #s1 * #l2 #s2
     345whd in match (〈?,?〉@?);
     346whd in match eval_block_cont; normalize nodelta
     347>m_bind_bind
     348>eval_seq_list_append
     349>m_bind_bind
     350@m_bind_ext_eq
     351
     352 whd in ⊢ (??%?);
     353    match ty return λx.IO ?? ((stmt_type_if ? x ?????) × ?) with
     354    [ SEQ ⇒
     355    | FIN ⇒ return 〈FRedirect ??? «l,?», st'〉
     356    ]
     357  | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
    54358  ].
    55  
    56 lemma Eapp_E0 : ∀tr1 : trace.tr1 ⧺ E0 = tr1 ≝ append_nil ….
    57 
    58 (* just like repeat, but without the full_exec infrastructure *)
    59 let rec repeat_eval_state n globals (p:sem_params) (ge : genv globals p)
     359#globals#p#ty#ge#st*#l1#s1*#l2#s2
     360whd in match (〈?,?〉@?);
     361whd in match eval_block_cont; normalize nodelta
     362>m_bind_bind
     363>eval_seq_list_append
     364>m_bind_bind
     365@m_bind_ext_eq
     366** [#l|#id#fd#args#dest] normalize nodelta #st'
     367[1,2:>m_return_bind normalize nodelta
     368  [ >m_return_bind ] % ]
     369change with (! x ← ? ; ?) in match (eval_seq_list ???? (?::?));
     370>m_bind_bind whd in match stmt_type_if;
     371normalize nodelta
     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 % | % ]
     376qed.
     377
     378
     379
     380(* just like repeat, but without the full_exec infrastructure, and it
     381   stops upon a non-proceed flow cmd *)
     382let rec repeat_eval_state_flag n globals (p:sem_params) (ge : genv globals p)
    60383  (st : state_pc p) on n :
    61     IO io_out io_in (trace×(state_pc p)) ≝
     384    IO io_out io_in (bool × (state_pc p)) ≝
    62385match n with
    63 [ O ⇒ return 〈E0, st〉
     386[ O ⇒ return 〈false,st〉
    64387| S k ⇒
    65   ! 〈tr1, st〉 ← eval_state globals p ge st ;
    66   ! 〈tr2, st〉 ← repeat_eval_state k globals p ge st ;
    67   return 〈tr1 ⧺ tr2, st〉
     388  ! 〈flag,st'〉 ← eval_state_flag globals p ge st ;
     389  if flag then return 〈true,st'〉 else repeat_eval_state_flag k globals p ge st'
    68390].
    69391
    70 lemma repeat_eval_state_plus : ∀n1,n2,globals, p, ge, st.
    71   repeat_eval_state (n1 + n2) globals p ge st =
    72   ! 〈tr1, st〉 ← repeat_eval_state n1 globals p ge st ;
    73   ! 〈tr2, st〉 ← repeat_eval_state n2 globals p ge st ;
    74   return 〈tr1 ⧺ tr2, st〉.
     392definition block_size : ∀p,g,ty.block_cont p g ty → ℕ ≝
     393λp,g,ty,b.S (|\fst b|).
     394
     395interpretation "block cont size" 'norm b = (block_size ??? b).
     396
     397lemma repeat_eval_state_flag_plus : ∀n1,n2,globals, p, ge, st.
     398  repeat_eval_state_flag (n1 + n2) globals p ge st =
     399  ! 〈flag,st〉 ← repeat_eval_state_flag n1 globals p ge st ;
     400  if flag then return 〈true, st〉 else repeat_eval_state_flag n2 globals p ge st.
    75401#n1 elim n1 -n1 [| #n1 #IH]
    76402#n2 #globals #p #ge #st
    77 [ >m_return_bind change with n2 in match (0 + n2);
    78   change with (! x ← ? ; ?) in ⊢ (???%);
    79   <(m_bind_return … (repeat_eval_state ?????)) in ⊢ (??%?);
    80   @m_bind_ext_eq * //
    81 | change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S ?) ????);
    82   change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S n1) ????);
     403[ @m_return_bind
     404| change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
     405  change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S n1) ????);
    83406  >m_bind_bind in ⊢ (???%);
    84   @m_bind_ext_eq * #tr1 #st1
    85   >IH >m_bind_bind in ⊢ (??%?); >m_bind_bind in ⊢ (???%);
    86   @m_bind_ext_eq * #tr2 #st2 >m_return_bind
    87   >m_bind_bind @m_bind_ext_eq * #tr3 #st3 >m_return_bind >Eapp_assoc %
    88 ]
    89 qed.
    90 
    91 lemma repeat_eval_state_one : ∀globals, p, ge, st.
    92   repeat_eval_state 1 globals p ge st = eval_state globals p ge st.
     407  @m_bind_ext_eq ** #st' normalize nodelta
     408  [ % | @IH ]
     409]
     410qed.
     411
     412lemma repeat_eval_state_flag_one : ∀globals, p, ge, st.
     413  repeat_eval_state_flag 1 globals p ge st = eval_state_flag globals p ge st.
    93414#globals #p #ge #st
    94 change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S ?) ????);
    95 <(m_bind_return … (eval_state ????)) in ⊢ (???%);
    96 @m_bind_ext_eq * #tr1 #st1 >m_return_bind >Eapp_E0 %
    97 qed.
    98 
    99 lemma If_true : ∀A.∀b : bool.∀f : b → A.∀g.∀prf' : bool_to_Prop b.If b then with prf do f prf else with prf do g prf = f prf'.
    100 #A * #f #g * normalize % qed.
     415change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
     416<(m_bind_return … (eval_state_flag ????)) in ⊢ (???%);
     417@m_bind_ext_eq ** #st %
     418qed.
    101419
    102420lemma eval_tunnel_step :
     
    105423  point_of_pointer ? p … (pc … st) = OK … src →
    106424  src ~~> dst in joint_if_code … fn →
    107   eval_state g p ge st =
    108     OK … 〈E0, set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
     425  eval_state_flag g p ge st =
     426    return 〈true,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
    109427#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #lbl * #EQ1 #EQ2
    110 change with (! s ← ? ; ?) in match (eval_state ????);
     428change with (! s ← ? ; ?) in match (eval_state_flag ????);
    111429change with (! fn ← ? ; ?) in match (fetch_statement ?????);
    112430>pc_pt in ⊢ (??%?); >m_return_bind
    113431>fetch_fn in ⊢ (??%?); >m_return_bind
    114432>EQ1 in ⊢ (??%?);  >m_return_bind
    115 >EQ2 in ⊢ (??%?);  >m_return_bind
    116 change with (! st ← ? ; ?) in ⊢ (??%?);
    117 whd in match eval_stmt_flow; normalize nodelta
    118 change with (! ptr ← ? ; ?) in match (goto ?????);
    119 whd in match pointer_of_label; normalize nodelta
     433>EQ2 in ⊢ (??%?);
     434change with (! st ← ? ; ?) in match (eval_statement ?????);
     435whd in match eval_fin_step; normalize nodelta
     436>m_return_bind
     437whd in match eval_fin_step_flow; normalize nodelta
     438change with (! ptr ← ? ; ?) in match (goto ??????);
     439whd in match pointer_of_label_in_block; normalize nodelta
     440whd in match fetch_function in fetch_fn;
     441normalize nodelta in fetch_fn;
    120442>fetch_fn in ⊢ (??%?); >m_return_bind
    121 >EQ2 in ⊢ (??%?); >m_return_bind %
    122 qed.
    123 
     443>EQ2 in ⊢ (??%?); >m_return_bind
     444cases st #st' ** #ty ** #id #H #o #EQ destruct(EQ)
     445elim (pointer_compat_from_ind … H) %
     446qed.
    124447
    125448lemma fetch_function_from_block_eq :
     
    131454@m_bind_ext_eq // qed.
    132455
     456(*
    133457lemma eval_tunnel :
    134458  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
     
    137461  src ~~>^* dst in joint_if_code … fn →
    138462  ∃n.repeat_eval_state n g p ge st =
    139     OK … 〈E0, set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
     463    return 〈f,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
    140464#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #through
    141465lapply pc_pt -pc_pt lapply fetch_fn -fetch_fn lapply src -src lapply st -st
     
    153477]
    154478#n' #EQ %{(S n')}
    155 change with (! 〈tr1,st1〉 ← ? ; ?) in match (repeat_eval_state ?????);
     479change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
    156480>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
    157 >EQ  >m_return_bind %
     481>EQ %
    158482qed.
    159483
     
    164488  src ~~>^+ dst in joint_if_code … fn →
    165489  ∃n.repeat_eval_state (S n) g p ge st =
    166     OK … 〈E0, set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
     490    return set_pc … (pointer_of_point ? p (pc … st) dst) st.
    167491#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #mid * #H1 #H2
    168492letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
     
    174498]
    175499#n #EQ %{n}
    176 change with (! 〈tr1,st1〉 ← ? ; ?) in match (repeat_eval_state ?????);
     500change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
    177501>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
    178 >EQ  >m_return_bind %
    179 qed.
     502>EQ %
     503qed.
     504*)
    180505
    181506lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer.
     
    190515qed.
    191516
    192 lemma eval_block_cont_in_code :
     517lemma eval_seq_list_in_code :
    193518  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
    194519  fetch_function … ge (pc … st) = OK … fn →
    195520  point_of_pointer ? p … (pc … st) = OK … src →
     521  All ? (never_calls … ge) B →
     522  seq_list_in_code … (joint_if_code … fn) src B dst →
     523  repeat_eval_state_flag (|B|) g p ge st =
     524   ! 〈flow,st'〉 ← eval_seq_list g p ge st B ;
     525   match flow with
     526   [ Redirect l ⇒
     527     ! st'' ← goto ?? ge l st' (pblock … (pc ? st)) ;
     528     return 〈true, st''〉
     529   | Init id fn args dest ⇒ Error … (msg ExecutingInternalCallInBlock)
     530       (* dummy, never happens *)
     531   | Proceed ⇒
     532     let nxt_ptr ≝ pointer_of_point p p … (pc … st) dst in
     533     return 〈false, mk_state_pc ? st' nxt_ptr〉
     534   ].
     535#p #g #ge #st #fn #src #B lapply src -src
     536lapply st -st elim B [|#hd #tl #IH]
     537#st #src #dst #fetch_fn #pc_pt * [2: #hd_ok #tl_ok]
     538[2: #EQ normalize in EQ; <EQ
     539  whd in match (eval_seq_list ???? [ ]);
     540  >m_return_bind normalize nodelta
     541  >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st //
     542|1: * #n * #EQat #H
     543  change with (! st' ← ? ; ?) in match (eval_seq_list ?????);
     544  change with (! st' ← ? ; ?) in match (repeat_eval_state_flag ?????);
     545  >m_bind_bind
     546  >(fetch_statement_eq … fetch_fn pc_pt EQat) >m_return_bind
     547  >m_bind_bind >m_bind_bind
     548  lapply (never_calls_no_init … hd_ok st) #hd_ok'
     549  @(mr_bind …
     550    (λfst1,fst2.fst1 = fst2 ∧ no_init … fst1))
     551  [ lapply hd_ok' elim (eval_step ?????)
     552    [ #o #f #IH'
     553      whd in ⊢ (%→%); #G
     554      %{(refl …)} #i @IH' @G
     555    |*: #v whd in ⊢ (%→%); #H
     556      % [ % ] @H
     557    ]
     558  | ** [#lbl | #id #fd #args #dest ] #st'
     559    #y * #EQ <EQ -y * normalize nodelta @rel_io_eq
     560    whd in match succ_pc; normalize nodelta
     561    >pc_pt >m_return_bind
     562    letin src' ≝ (point_of_succ p src n) in H ⊢ %;
     563    letin pc' ≝ (pointer_of_point p p … (pc ? st) src') #H
     564    [>m_return_bind whd in match eval_step_flow; normalize nodelta
     565     whd in match (pblock ?);
     566     elim (goto … ge lbl st' ?)
     567     [ #st'' >m_return_bind %
     568     | #e %
     569     ]
     570    | normalize nodelta in IH ⊢ %; @(IH … tl_ok H)
     571      [ @fetch_fn
     572      | @point_of_pointer_of_point
     573      ]
     574    ]
     575  ]
     576]
     577qed.
     578
     579definition eval_block_cont_pc :
     580  ∀globals.∀p : sem_params.∀ty.genv globals p →
     581  state_pc p → block_cont p globals ty → stmt_type_if ? ty (code_point p) unit →
     582  IO io_out io_in (bool × (state_pc p)) ≝
     583  λglobals,p,ty,ge,st,b,nxt.
     584  ! 〈flow, st'〉 ← eval_block_cont globals p ty ge st b ;
     585  match ty return λx.stmt_type_if ? x ?? → stmt_type_if ? x ?? → ? with
     586  [ SEQ ⇒ λflow,nxt.eval_step_flow ?? ge st'
     587        (pointer_of_point ? p (pc ? st) nxt) flow
     588  | FIN ⇒ λflow.λ_.
     589    ! st' ← eval_fin_step_flow ?? ge st' (pblock … (pc ? st)) flow ;
     590    return 〈true, st'〉
     591  ] flow nxt.
     592
     593lemma eval_block_cont_in_code :
     594  ∀p : sem_params.∀g,ty.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
     595  fetch_function … ge (pc … st) = OK … fn →
     596  point_of_pointer ? p … (pc … st) = OK … src →
     597  All ? (never_calls … ge) (\fst B) →
    196598  src ~❨B❩~> dst in joint_if_code … fn →
    197   ∃n.repeat_eval_state n g p ge st =
    198     eval_block_cont g p ge st (block_id (pblock (pc … st))) B (! x ← dst; return pointer_of_point … p (pc … st) x).
    199 #p #g #ge #st #fn #src #B lapply src -src
    200 lapply st -st elim B [|#s|#s #B' #IH]
    201 #st #src #dst #fetch_fn #pc_pt
    202 [ cases dst [*] #z @eval_tunnel assumption
     599  repeat_eval_state_flag (|B|) g p ge st =
     600    eval_block_cont_pc g p ty ge st B dst.
     601#p #g #ty #ge #st #fn #src * #l #s #dst #fetch_fn #pc_pt #l_ok
     602* #mid * #l_in_code #s_in_code
     603change with (1 + |l|) in match (|?|);
     604>commutative_plus
     605>repeat_eval_state_flag_plus
     606change with (! x ← ? ; ?) in ⊢ (???%);
     607>m_bind_bind
     608>(eval_seq_list_in_code … fetch_fn pc_pt l_ok l_in_code)
     609>m_bind_bind
     610@m_bind_ext_eq ** [#lbl | #id #fd #args #dest] #st'
     611normalize nodelta
     612[ -s_in_code lapply dst -dst cases ty
     613  whd in match stmt_type_if; normalize nodelta
     614  #dst >m_return_bind
     615  [whd in match eval_step_flow; | whd in match eval_fin_step_flow; ]
     616  normalize nodelta
     617  whd in match (pblock ?);
     618  elim (goto g p ge lbl st' ?) #x //
     619| %
     620| >m_return_bind normalize nodelta
     621  >repeat_eval_state_flag_one
     622  >m_bind_bind
     623  lapply s_in_code -s_in_code lapply dst -dst lapply s -s cases ty
     624  whd in match stmt_type_if; normalize nodelta
     625  #s #dst [* #n * ] #s_in_code [ #n_is_dst ]
     626  whd in match eval_state_flag; normalize nodelta
     627  letin pc' ≝ (pointer_of_point p p (pc ? st) mid)
     628  letin st_pc' ≝ (mk_state_pc ? st' pc')
     629  >(fetch_statement_eq … ?? s_in_code)
     630  [2,5: @point_of_pointer_of_point
     631  |3,6: @fetch_fn
     632  |*: >m_return_bind
     633    whd in match eval_statement; normalize nodelta
     634    @m_bind_ext_eq * #flow #st'' >m_return_bind [2:%]
     635    whd in match succ_pc; normalize nodelta
     636    >point_of_pointer_of_point >m_return_bind
     637    >pointer_of_point_of_pointer [2: @refl |*:]
     638    [ >point_of_pointer_of_point >n_is_dst %
     639    | %
     640    ]
     641  ]
     642]
     643qed.
     644     cases dst [*] #z @eval_tunnel assumption
    203645| cases dst [2: #z *]]
    204646* #mid * #tunn [#H | * #n * #H #G ]
Note: See TracChangeset for help on using the changeset viewer.