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_paolo.ma

    r1882 r1949  
    6363
    6464axiom BadProgramCounter : String.
     65
     66definition function_of_block :
     67 ∀pars : params.
     68 ∀globals.
     69  genv globals pars →
     70  block →
     71  res (joint_internal_function … pars) ≝
     72  λpars,blobals,ge,b.
     73  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     74  match def with
     75  [ Internal def' ⇒ OK … def'
     76  | External _ ⇒ Error … [MSG BadProgramCounter]].
     77 
    6578(* this can replace graph_fetch function and lin_fetch_function *)
    6679definition fetch_function:
     
    7083  cpointer →
    7184  res (joint_internal_function … pars) ≝
    72  λpars,globals,ge,p.
    73   let b ≝ pblock p in
    74   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    75   match def with
    76   [ Internal def' ⇒ OK … def'
    77   | External _ ⇒ Error … [MSG BadProgramCounter]].
    78 
    79 inductive step_flow (p : params) (globals : list ident) : Type[0] ≝
    80   | Redirect : label → step_flow p globals (* used for goto-like flow alteration *)
    81   | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals (* call a function with given id, then proceed *)
    82   | Proceed  : step_flow p globals. (* go to implicit successor *)
    83 
    84 inductive stmt_flow (p : params) (globals : list ident) : Type[0] ≝
    85   | SRedirect : label → stmt_flow p globals
    86   | SProceed : succ p → stmt_flow p globals
    87   | SInit     : Z → joint_internal_function globals p → call_args p → call_dest p → succ p → stmt_flow p globals
    88   | STailInit : Z → joint_internal_function globals p → call_args p → stmt_flow p globals
    89   | SEnd  : stmt_flow p globals. (* end flow *)
    90 
     85 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
     86
     87inductive step_flow (p : params) (globals : list ident) (labels : list label) : Type[0] ≝
     88  | Redirect : (Σl.In ? labels l) → step_flow p globals labels (* used for goto-like flow alteration *)
     89  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals labels (* call a function with given id, then proceed *)
     90  | Proceed  : step_flow p globals labels. (* go to implicit successor *)
     91
     92inductive fin_step_flow (p : params) (globals : list ident) (labels : list label): Type[0] ≝
     93  | FRedirect : (Σl.In ? labels l) → fin_step_flow p globals labels
     94  | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals labels
     95  | FEnd  : fin_step_flow p globals labels. (* end flow *)
    9196
    9297record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
     
    164169   serialization and on whether the call is a tail one. *)
    165170definition eval_call_block:
    166  ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
     171 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.∀lbls.
    167172  genv globals p → state p' → block → call_args p → call_dest p →
    168     IO io_out io_in ((step_flow p globals)×trace×(state p')) ≝
    169  λglobals,p,p',ge,st,b,args,dest.
     173    IO io_out io_in ((step_flow p globals lbls)×(state p')) ≝
     174 λglobals,p,p',lbls,ge,st,b,args,dest.
    170175  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
    171176    match fd with
    172177    [ Internal fn ⇒
    173       return 〈Init … (block_id b) fn args dest, E0, st〉
     178      return 〈Init … (block_id b) fn args dest, st〉
    174179    | External fn ⇒
    175180      ! params ← fetch_external_args … p' fn st : IO ???;
     
    181186      let vs ≝ [mk_val ? evres] in
    182187      ! st ← set_result … p' vs st : IO ???;
    183       return 〈Proceed ??, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     188      return 〈Proceed ???, st〉
    184189      ].
    185190
     
    218223  return 〈st'', pr〉.
    219224
    220 definition flow_no_seq : ∀p,g.stmt_flow p g → Prop ≝ λp,g,flow.
    221   match flow with
    222   [ SProceed _ ⇒ False
    223   | SInit _ _ _ _ _ ⇒ False
    224   | _ ⇒ True
    225   ].
    226 
    227225(* parameters that need full params to have type of functions,
    228226   but are still independent of serialization *)
     
    231229  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    232230  (* change of pc must be left to *_flow execution *)
    233   ; exec_extended: ∀globals.genv globals pp → ext_step pp →
     231  ; exec_extended: ∀globals.genv globals pp → ∀s : ext_step pp.
    234232      state msu_pars →
    235       IO io_out io_in ((step_flow pp globals)× trace × (state msu_pars))
    236   ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_stmt pp →
     233      IO io_out io_in ((step_flow pp globals (ext_step_labels … s))× (state msu_pars))
     234  ; exec_fin_extended: ∀globals.genv globals pp → ∀s : ext_fin_stmt pp.
    237235      state msu_pars →
    238       IO io_out io_in ((Σs.flow_no_seq pp globals s)× trace × (state msu_pars))
     236      IO io_out io_in ((fin_step_flow pp globals (ext_fin_stmt_labels … s))×(state msu_pars))
    239237  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    240238  }.
     
    305303  ! fn ← fetch_function … ge ptr ;
    306304  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
     305 
     306definition pointer_of_label_in_block : ∀p : params.∀ msp : more_sem_params p.∀globals.
     307  genv globals p → block → label → res cpointer ≝
     308  λp,msp,globals,ge,b,lbl.
     309  ! fn ← function_of_block … ge b ;
     310  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
     311            (point_of_label … (joint_if_code … fn) lbl) ;
     312  return (mk_pointer Code (mk_block Code (block_id b)) ? (offset_of_point p msp pt) : Σp.?). // qed.
    307313
    308314definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    309315  genv globals p → cpointer → label → res cpointer ≝
    310   λp,msp,globals,ge,ptr,lbl.
    311   ! fn ← fetch_function … ge ptr ;
    312   ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
    313             (point_of_label … (joint_if_code … fn) lbl) ;
    314   return pointer_of_point ? msp ptr pt.
     316  λp,msp,globals,ge,ptr.
     317  pointer_of_label_in_block p msp globals ge (pblock ptr).
    315318
    316319definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
     
    332335
    333336definition goto: ∀globals. ∀p:sem_params.
    334   genv globals p → label → state_pc p → res (state_pc p) ≝
    335  λglobals,p,ge,l,st.
    336   ! newpc ← pointer_of_label ? p … ge (pc … st) l ;
    337   return set_pc … newpc st.
     337  genv globals p → label → state p → block → res (state_pc p) ≝
     338 λglobals,p,ge,l,st,b.
     339  ! newpc ← pointer_of_label_in_block ? p … ge b l ;
     340  return mk_state_pc ? st newpc.
    338341
    339342(*
     
    342345*)
    343346
    344 definition next : ∀p : sem_params.succ p → state_pc p → res (state_pc p) ≝
    345  λp,l,st.
    346  ! nw ← succ_pc ? p … (pc ? st) l ;
    347  return set_pc … nw st.
     347definition next : ∀p : sem_params.succ p → state p → cpointer → res (state_pc p) ≝
     348 λp,l,st,pc.
     349 ! newpc ← succ_pc ? p … pc l ;
     350 return mk_state_pc … st newpc.
    348351
    349352axiom MissingSymbol : String.
     
    355358definition eval_step :
    356359 ∀globals.∀p:sem_params. genv globals p → state p →
    357   joint_step p globals →
    358   IO io_out io_in ((step_flow p globals)×trace×(state p)) ≝
     360  ∀s:joint_step p globals.
     361  IO io_out io_in ((step_flow p globals (step_labels … s))×(state p)) ≝
    359362 λglobals,p,ge,st,seq.
    360   match seq with
     363  match seq return λx.IO ?? ((step_flow ?? (step_labels … x) × ?)) with
    361364  [ extension c ⇒
    362365    exec_extended … ge c st
    363366  | COST_LABEL cl ⇒
    364     return 〈Proceed ??, Echarge cl, st〉
     367    return 〈Proceed ???, st〉
    365368  | COMMENT c ⇒
    366     return 〈Proceed ??, E0, st〉
     369    return 〈Proceed ???, st〉
    367370  | LOAD dst addrl addrh ⇒
    368371    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    371374    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    372375    ! st ← acca_store p … dst v st ;
    373     return 〈Proceed ??, E0, st〉
     376    return 〈Proceed ???, st〉
    374377  | STORE addrl addrh src ⇒
    375378    ! vaddrh ← dph_arg_retrieve … st addrh;
     
    378381    ! v ← acca_arg_retrieve … st src;
    379382    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    380     return 〈Proceed ??, E0, set_m … m' st〉
     383    return 〈Proceed ???, set_m … m' st〉
    381384  | COND src ltrue ⇒
    382385    ! v ← acca_retrieve … st src;
    383386    ! b ← bool_of_beval v;
    384387    if b then
    385       return 〈Redirect ?? ltrue, E0, st〉
     388      return 〈Redirect ??? ltrue, st〉
    386389    else
    387       return 〈Proceed ??, E0, st〉
     390      return 〈Proceed ???, st〉
    388391  | ADDRESS ident prf ldest hdest ⇒
    389392    let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
     
    391394    ! st' ← dpl_store … ldest laddr st;
    392395    ! st'' ← dph_store … hdest haddr st';
    393     return 〈Proceed ??, E0, st''〉
     396    return 〈Proceed ???, st''〉
    394397  | OP1 op dacc_a sacc_a ⇒
    395398    ! v ← acca_retrieve … st sacc_a;
     
    397400    let v' ≝ BVByte (op1 eval op v) in
    398401    ! st ← acca_store … dacc_a v' st;
    399     return 〈Proceed ??, E0, st〉
     402    return 〈Proceed ???, st〉
    400403  | OP2 op dacc_a sacc_a src ⇒
    401404    ! v1 ← acca_arg_retrieve … st sacc_a;
     
    409412    ! st' ← acca_store … dacc_a v' st;
    410413      let st'' ≝ set_carry … carry st' in
    411     return 〈Proceed ??, E0, st''〉
     414    return 〈Proceed ???, st''〉
    412415  | CLEAR_CARRY ⇒
    413416    let st' ≝ set_carry … BVfalse st in
    414     return 〈Proceed ??, E0, st'〉
     417    return 〈Proceed ???, st'〉
    415418  | SET_CARRY ⇒
    416419    let st' ≝ set_carry … BVtrue st in
    417     return 〈Proceed ??, E0, st'〉
     420    return 〈Proceed ???, st'〉
    418421  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    419422    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     
    426429    ! st' ← acca_store … dacc_a_reg v1' st;
    427430    ! st'' ← accb_store … dacc_b_reg v2' st';
    428     return 〈Proceed ??, E0, st''〉
     431    return 〈Proceed ???, st''〉
    429432  | POP dst ⇒
    430433    ! 〈st',v〉 ← pop p st;
    431434    ! st'' ← acca_store p p dst v st';
    432     return 〈Proceed ??, E0, st''〉
     435    return 〈Proceed ???, st''〉
    433436  | PUSH src ⇒
    434437    ! v ← acca_arg_retrieve … st src;
    435438    ! st ← push … st v;
    436     return 〈Proceed ??, E0, st〉
     439    return 〈Proceed ???, st〉
    437440  | MOVE dst_src ⇒
    438441    ! st ← pair_reg_move … st dst_src ;
    439     return 〈Proceed ??, E0, st〉
     442    return 〈Proceed ???, st〉
    440443  | CALL_ID id args dest ⇒
    441444    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
     
    445448  | (* TODO: to prove *)
    446449    elim daemon
     450  | %1 %
    447451  ] qed.
    448452
    449 definition eval_step_flow :
    450  ∀globals.∀p:sem_params.step_flow p globals →
    451   succ p → stmt_flow p globals ≝
    452  λglobals,p,cmd,nxt.
    453  match cmd with
    454  [ Redirect l ⇒ SRedirect … l
    455  | Init id fn args dest ⇒ SInit … id fn args dest nxt
    456  | Proceed ⇒ SProceed … nxt
    457  ].
    458 
    459 definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
    460   state p → joint_statement … p globals →
    461   IO io_out io_in ((stmt_flow p globals) × trace × (state p)) ≝
     453definition eval_fin_step : ∀globals: list ident.∀p:sem_params. genv globals p →
     454  state p → ∀s : joint_fin_step … p globals.
     455  IO io_out io_in ((fin_step_flow p globals (fin_step_labels … s))×(state p)) ≝
    462456 λglobals,p,ge,st,s.
    463   match s with
    464     [ GOTO l ⇒ return 〈SRedirect … l, E0, (st : state ?)〉
    465     | RETURN ⇒ return 〈SEnd ??, E0, (st : state ?) 〉
    466     | sequential seq l ⇒
    467       ! 〈flow, tr, st〉 ← eval_step … ge st seq ;
    468       return 〈eval_step_flow … flow l, tr, st〉
    469     | extension_fin c ⇒
    470       ! 〈flow, tr, st〉 ← exec_fin_extended … ge c st ;
    471       return 〈pi1 … flow, tr, st〉
    472     ].
    473 
    474 definition eval_statement_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
    475   state p → (Σs : joint_statement … p globals.no_seq … s) →
    476   IO io_out io_in ((Σf.flow_no_seq p globals f) × trace × (state p)) ≝
    477  λglobals,p,ge,st,s_sig.
    478   match s_sig with
    479   [ mk_Sig s s_prf ⇒
    480     match s return λx.no_seq p globals x → ? with
    481     [ GOTO l ⇒ λ_.return 〈«SRedirect … l,?», E0, (st : state ?)〉
    482     | RETURN ⇒ λ_.return 〈«SEnd ??,?», E0, (st : state ?) 〉
    483     | sequential seq l ⇒ Ⓧ
    484     | extension_fin c ⇒ λ_.exec_fin_extended … ge c st
    485     ] s_prf
    486   ]. % qed.
    487 
    488 let rec rel_io O I A B (P : A → B → Prop) (v1 : IO O I A)
    489   (v2 : IO O I B) on v1 : Prop ≝
    490   match v1 with
    491   [ Value x ⇒
    492     match v2 with
    493     [ Value y ⇒
    494       P x y
    495     | _ ⇒ False
    496     ]
    497   | Wrong _ ⇒
    498     match v2 with
    499     [ Wrong _ ⇒ True
    500     | _ ⇒ False
    501     ]
    502   | Interact o1 f1 ⇒
    503     match v2 with
    504     [ Interact o2 f2 ⇒
    505       ∃prf:o1 = o2.∀i.rel_io … P (f1 i) (f2 ?)
    506     | _ ⇒ False
    507     ]
    508   ]. <prf @i qed.
    509 
    510 definition IORel ≝ λO,I.
    511   mk_MonadRel (IOMonad O I) (IOMonad O I)
    512     (rel_io O I) ???.
    513 [//
    514 |#X #Y #Z #W #relin #relout #m elim m
    515   [ #o #f #IH * [#o' #f' | #v | #e] * #EQ destruct(EQ) #G
    516     #f1 #f2 #G' whd %{(refl …)} #i
    517     @(IH … (G i) f1 f2 G')
    518   | #v * [#o #f * | #v' | #e *]
    519     #Pvv' #f #g #H normalize @H @Pvv'
    520   | #e1 * [#o #f * | #v' *| #e2] * #f #g #_ %
    521   ]
    522 | #X #Y #P #Q #H #m elim m [#o #f #IH | #v | #e] *
    523   [1,4,7: #o' #f' [2,3: *]
    524     normalize * #prf destruct(prf) normalize #G
    525     % [%] normalize #i @IH @G
    526   |2,5,8: #v' [1,3: *]
    527     @H
    528   |*: #e' [1,2: *] //
    529   ]
    530 ]
    531 qed.
    532 
    533 lemma IORel_refl : ∀O,I,X,rel.reflexive X rel →
    534   reflexive ? (m_rel ?? (IORel O I) ?? rel).
    535 #O #I #X #rel #H #m elim m
    536 [ #o #f #IH whd %[%] #i normalize @IH
    537 | #v @H
    538 | #e %
    539 ]
    540 qed.
    541 
    542 lemma IORel_transitive : ∀O,I,X,Y,Z,rel1,rel2,rel3.
    543   (∀x : X.∀y : Y.∀z : Z.rel1 x y → rel2 y z → rel3 x z) →
    544   ∀m,n,o.
    545   m_rel ?? (IORel O I) … rel1 m n →
    546   m_rel ?? (IORel O I) … rel2 n o →
    547   m_rel ?? (IORel O I) … rel3 m o.
    548 #O #I #X #Y #Z #rel1 #rel2 #rel3 #H #m elim m
    549 [ #o #f #IH * [#o' #f' * [#o'' #f'' | #v #_ * | #e #_ * ] | #v #x * | #e #x * ]
    550   normalize * #EQ #H1 * #EQ' #H2 destruct %[%] normalize #i @(IH ? (f' i)) //
    551 | #v * [#o #f #x * | #v' * [#o #f #_ * | #v'' |#e #_ *] | #e #x *]
    552   @H
    553 | #e * [#o #f #x * | #v #x * | #e' * [#o #f #_ * | #v #_ * | #e'']] //
    554 ]
    555 qed.
    556 
    557 lemma mr_bind' : ∀M1,M2.∀Rel : MonadRel M1 M2.
    558   ∀X,Y,Z,W,relin,relout,m,n.m_rel ?? Rel X Y relin m n →
    559   ∀f,g.(∀x,y.relin x y → m_rel ?? Rel Z W relout (f x) (g y)) →
    560                   m_rel ?? Rel ?? relout (! x ← m ; f x) (! y ← n ; g y).
    561 #M1 #M2 #Rel #X #Y #Z #W #relin #relout #m #n #H #f #g #G
    562 @(mr_bind … H) @G qed.
    563 
    564 lemma m_bind_ext_eq' : ∀M : MonadProps.∀X,Y.∀m1,m2 : monad M X.∀f1,f2 : X → monad M Y.
    565   m1 = m2 → (∀x.f1 x = f2 x) → ! x ← m1 ; f1 x = ! x ← m2 ; f2 x.
    566 #M #X #Y #m1 #m2 #f1 #f2 #EQ >EQ @m_bind_ext_eq
    567 qed.
    568 
    569 lemma eval_statement_no_seq_to_normal : ∀globals,p,ge,st,s1,s2.
    570   pi1 ?? s1 = s2 →
    571   m_rel ?? (IORel ??) ??
    572     (λx,y.pi1 ?? (\fst (\fst x)) = \fst (\fst y) ∧
    573       \snd (\fst x) = \snd (\fst y) ∧ \snd x = \snd y)
    574     (eval_statement_no_seq globals p ge st s1)
    575     (eval_statement globals p ge st s2).
    576 #globals #p #ge #st * * [#s #n | #lbl || #c ]*
    577 #s2 #EQ destruct(EQ)
    578 whd in match eval_statement;
    579 whd in match eval_statement_no_seq;
    580 normalize nodelta
    581 [1,2: @(mr_return … (IORel ??)) /3 by pair_destruct, conj/]
    582 <(m_bind_return … (exec_fin_extended ??????)) in ⊢ (???????%?);
    583 @(mr_bind … (IORel ??)) [@eq | @IORel_refl // |
    584 #x #y #EQ destruct(EQ) cases y ** #a #prf #b #c whd /3 by pair_destruct, conj/
    585 qed.
     457  match s return λx.IO ?? ((fin_step_flow ?? (fin_step_labels … x)) × ?) with
     458    [ GOTO l ⇒ return 〈FRedirect ??? l, st〉
     459    | RETURN ⇒ return 〈FEnd ???, st〉
     460    | extension_fin c ⇒ exec_fin_extended … ge c st
     461    ]. %1 % qed.
     462
    586463
    587464definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
     
    598475    return mk_state_pc ? st' pc. % qed.
    599476
    600 definition eval_stmt_flow : ∀globals: list ident.∀p:sem_params. genv globals p →
    601   state_pc p → stmt_flow p globals → IO io_out io_in (state_pc p) ≝
    602   λglobals,p,ge,st,flow.
    603   match flow with
    604   [ SRedirect l ⇒ goto … ge l st
    605   | SProceed nxt ⇒ next ? nxt st
    606   | SInit id fn args dest nxt ⇒
    607     ! ra ← succ_pc ? p … (pc … st) nxt ;
    608     let st' ≝ set_no_pc … (set_frms … (save_frame … ra dest st) st) st in
    609     do_call ?? ge st' id fn args
    610   | STailInit id fn args ⇒
     477(* The pointer provided is the one to the *next* instruction.
     478   The boolean tells wether a flow changement has occurred (i.e.
     479   a non Proceed cmd was issued). Used in linking block evaluation
     480   with regular one *)
     481definition eval_step_flow :
     482 ∀globals.∀p:sem_params.∀lbls.genv globals p →
     483  state p → cpointer → step_flow p globals lbls →
     484    res (bool × (state_pc p)) ≝
     485 λglobals,p,lbls,ge,st,nxt,cmd.
     486 match cmd with
     487  [ Redirect l ⇒
     488    ! st ← goto … ge l st (pblock nxt) ; return 〈true, st〉
     489  | Init id fn args dest ⇒
     490    let st' ≝ set_frms … (save_frame … nxt dest st) st in
     491    ! st ← do_call ?? ge st' id fn args ;
     492    return 〈true, st〉
     493  | Proceed ⇒
     494    return 〈false, mk_state_pc ? st nxt〉
     495  ].
     496
     497definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀lbls. genv globals p →
     498  state p → block → fin_step_flow p globals lbls → res (state_pc p) ≝
     499  λglobals,p,lbls,ge,st,b,cmd.
     500  match cmd with
     501  [ FRedirect l ⇒ goto … ge l st b
     502  | FTailInit id fn args ⇒
    611503    do_call … ge st id fn args
    612   | SEnd ⇒
    613     ! 〈st,ra〉 ← fetch_ra … st ;
    614     ! st' ← pop_frame … ge st;
    615     return mk_state_pc ? st' ra
     504  | FEnd ⇒
     505    ! 〈st',ra〉 ← fetch_ra … st ;
     506    ! st'' ← pop_frame … ge st;
     507    return mk_state_pc ? st'' ra
    616508  ].
    617509
    618 definition eval_stmt_flow_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
    619   state p → Z → (Σf:stmt_flow p globals.flow_no_seq … f) →
    620     IO io_out io_in (state_pc p) ≝
    621   λglobals,p,ge,st,id,flow_sig.
    622   match flow_sig with
    623   [ mk_Sig flow prf ⇒
    624     match flow return λx.flow_no_seq p globals x → ? with
    625     [ SRedirect l ⇒ λ_.
    626       ! newpc ← pointer_of_label ? p … ge
    627         (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) l ;
    628       return mk_state_pc … st newpc
    629     | STailInit id fn args ⇒ λ_.
    630       do_call … ge st id fn args
    631     | SEnd ⇒ λ_.
    632       ! 〈st,ra〉 ← fetch_ra … st ;
    633       ! st' ← pop_frame … ge st;
    634       return mk_state_pc ? st' ra
    635     | _ ⇒ Ⓧ
    636     ] prf
    637   ]. % qed.
    638 
    639 lemma pointer_of_label_eq_with_id :
    640 ∀g.∀p : sem_params.∀ge : genv g p.∀ptr1,ptr2 : cpointer.∀lbl.
    641   block_id (pblock ptr1) = block_id (pblock ptr2) →
    642   pointer_of_label ? p ? ge ptr1 lbl = pointer_of_label ? p ? ge ptr2 lbl.
    643 #g #p #ge
    644 ** #ty1 * #r1 #id1 #H1 inversion H1 [#s || #s] #id #EQ1 #EQ2 #EQ3 #o #EQ4 destruct
    645 ** #ty2 * #r2 #id2 #H2 inversion H2
    646 [1,3: #s] #id2' #EQ5 #EQ6 #EQ7 #o2 #EQ8 #lbl #EQ9 destruct %
    647 qed.
    648 
    649 
    650 lemma eval_stmt_flow_no_seq_to_normal : ∀g.∀p : sem_params.∀ge.∀st : state_pc p.
    651   ∀id.∀s1 : Σs.flow_no_seq p g s.∀s2.
    652   pi1 … s1 = s2 → block_id (pblock (pc … st)) = id →
    653     (eval_stmt_flow_no_seq g p ge st id s1) =
    654     (eval_stmt_flow g p ge st s2).
    655 #g#p#ge#st#id'
    656 **[#lbl|#nxt*|#id#fn#args#dest#n*|#id#fn#args]*
    657 #s2 #EQ #EQ' destruct(EQ)
    658 whd in match eval_stmt_flow_no_seq; normalize nodelta
    659 whd in match eval_stmt_flow; normalize nodelta
    660 [2,3: %]
    661 whd in match goto; normalize nodelta
    662 whd in match set_pc; normalize nodelta
    663 >pointer_of_label_eq_with_id [% | >EQ' % |]
    664 qed.
    665 
    666 definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
    667   state_pc p → IO io_out io_in (trace × (state_pc p)) ≝
     510definition eval_statement :
     511 ∀globals.∀p:sem_params.genv globals p →
     512  state_pc p → joint_statement p globals →
     513    IO io_out io_in (bool × (state_pc p)) ≝
     514 λglobals,p,ge,st,stmt.
     515 match stmt with
     516 [ sequential s nxt ⇒
     517   ! 〈flow, st'〉 ← eval_step … ge st s ;
     518   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
     519   eval_step_flow … ge st' nxtptr flow
     520 | final s ⇒
     521   ! 〈flow, st'〉 ← eval_fin_step … ge st s ;
     522   ! st ← eval_fin_step_flow … ge st' (pblock … (pc … st)) flow ;
     523   return 〈true, st〉
     524 ].
     525
     526definition eval_state_flag : ∀globals: list ident.∀p:sem_params. genv globals p →
     527  state_pc p → IO io_out io_in (bool × (state_pc p)) ≝
    668528  λglobals,p,ge,st.
    669529  ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
    670   ! 〈flow, tr, st_npc〉 ← eval_statement … ge st s;
    671   let st ≝ set_no_pc … st_npc st in
    672   ! st ← eval_stmt_flow … ge st flow;
    673   return 〈tr, st〉.
    674 
     530  eval_statement … ge st s.
     531
     532definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
     533  state_pc p → IO io_out io_in (state_pc p) ≝
     534  λglobals,p,ge,st.
     535  ! 〈flag,st'〉 ← eval_state_flag … ge st ;
     536  return st'.
     537
     538(* Paolo: what if in an intermediate language main finishes with an external
     539  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
     540  not static... *)
    675541definition is_final: ∀globals:list ident. ∀p: sem_params.
    676542  genv globals p → cpointer → state_pc p → option int ≝
     
    678544  do s ← fetch_statement ? p … ge (pc … st);
    679545  match s with
    680    [ RETURN ⇒
     546  [ final s' ⇒
     547    match s' with
     548    [ RETURN ⇒
    681549      do 〈st,ra〉 ← fetch_ra … st;
    682550      if eq_pointer ra exit then
     
    685553      else
    686554       Error ? [ ]
    687    | _ ⇒ Error ? [ ]]).
     555   | _ ⇒ Error ? [ ]
     556   ]
     557 | _ ⇒ Error ? [ ]
     558 ]).
    688559 
    689560record evaluation_parameters : Type[1] ≝
     
    694565 }.
    695566
     567(* Paolo: with structured traces, eval need not emit labels. However, this
     568  changes trans_system. For now, just putting a dummy thing for
     569  the transition. *)
    696570definition joint_exec: trans_system io_out io_in ≝
    697571  mk_trans_system … evaluation_parameters (λG. state_pc G)
    698572   (λG.is_final (globals G) G (genv2 G) (exit G))
    699    (λG.eval_state (globals G) G (genv2 G)).
     573   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
    700574
    701575definition make_global :
Note: See TracChangeset for help on using the changeset viewer.