Changeset 239 for C-semantics/CexecIO.ma


Ignore:
Timestamp:
Nov 12, 2010, 7:16:52 PM (9 years ago)
Author:
campbell
Message:

More work on soundness and completeness of executable Clight semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r225 r239  
    865865nqed.
    866866
    867 ndefinition is_final_state : ∀st:state. (r. final_state st r) + (¬∃r. final_state st r).
     867ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r).
    868868#st; nelim st;
    869869##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
     
    931931(* A (possibly non-terminating) execution. *)
    932932ncoinductive execution : Type ≝
    933 | e_stop : trace → state → execution
     933| e_stop : trace → int → execution
    934934| e_step : trace → state → execution → execution
    935935| e_wrong : execution
     
    941941| Value v ⇒ match v with [ mk_pair t s' ⇒
    942942    match is_final_state s' with
    943     [ inl _ ⇒ e_stop t s'
     943    [ inl r ⇒ e_stop t (sig_eject … r)
    944944    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
    945945| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
    946946].
    947947
     948
    948949ndefinition exec_inf : program → execution ≝
    949950λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,sig_eject ?? s〉).
    950951
     952(*
     953FIXME: unfolding cofixpoints appears to be rather tricky.
     954
     955nremark execution_cases: ∀e.
     956 e = match e with [ e_stop tr r ⇒ e_stop tr r | e_step tr s e ⇒ e_step tr s e
     957 | e_wrong ⇒ e_wrong | e_interact o k ⇒ e_interact o k ].
     958#e; ncases e; //; nqed.
     959
     960nlemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s =
     961match s with
     962[ Wrong ⇒ e_wrong
     963| Value v ⇒ match v with [ mk_pair t s' ⇒
     964    match is_final_state s' with
     965    [ inl r ⇒ e_stop t (sig_eject … r)
     966    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
     967| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
     968].
     969#ge s; nrewrite > (execution_cases (exec_inf_aux …));
     970ncases s; //; napply refl;
     971
     972
     973nlemma exec_inf_aux_wrong: ∀ge,s. exec_inf_aux ge s = e_wrong → s = Wrong ….
     974#ge s; ncases s;
     975##[ #o k EXEC; nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC; nnormalize in EXEC;
     976    ndestruct;
     977##| #v; ncases v; #tr s'; #EXEC; nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC; nnormalize in EXEC;
     978    ncases (is_final_state s');
     979    ndestruct;
     980*)
     981
     982(* Finite number of steps without interaction. *)
     983ninductive execution_steps : trace → execution → execution → Prop ≝
     984| steps_none : ∀e. execution_steps E0 e e
     985| steps_one : ∀e,e',tr,tr',s. execution_steps tr' e e' → execution_steps (tr⧺tr') (e_step tr s e) e'.
     986
     987(* Finite number of steps allowing interaction. *)
     988ninductive execution_isteps : trace → execution → execution → Prop ≝
     989| isteps_none : ∀e. execution_isteps E0 e e
     990| isteps_step : ∀e,e',tr,tr',s. execution_isteps tr e e' → execution_isteps (tr⧺tr') (e_step tr s e) e'
     991| isteps_interact : ∀k,o,i,e',tr. execution_isteps tr (k i) e' → execution_isteps tr (e_interact o k) e'.
     992
     993ninductive execution_terminates : trace → int → execution → Prop ≝
     994| terminates : ∀tr,tr',r,e. execution_isteps tr e (e_stop tr' r) → execution_terminates (tr⧺tr') r e.
     995
     996ncoinductive execution_diverging : execution → Prop ≝
     997| diverging_step : ∀s,e. execution_diverging e → execution_diverging (e_step E0 s e).
     998
     999(* Makes a finite number of interactions (including cost labels) before diverging. *)
     1000ninductive execution_diverges : trace → execution → Prop ≝
     1001| diverges_diverging: ∀tr,e,e'.
     1002    execution_isteps tr e e' →
     1003    execution_diverging e' →
     1004    execution_diverges tr e.
     1005
     1006(* NB: "reacting" includes hitting a cost label. *)
     1007ncoinductive execution_reacts : traceinf → execution → Prop ≝
     1008| reacting: ∀tr,tr',e,e'. execution_reacts tr' e' → execution_isteps tr e e' → tr ≠ E0 → execution_reacts (tr⧻tr') e.
     1009
     1010ninductive execution_goes_wrong: trace → execution → Prop ≝
     1011| go_wrong: ∀tr,e. execution_isteps tr e e_wrong → execution_goes_wrong tr e.
     1012
     1013ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
     1014| emb_terminates: ∀e,tr,r.
     1015    execution_terminates tr r e →
     1016    execution_matches_behavior e (Terminates tr r)
     1017| emb_diverges: ∀e,tr.
     1018    execution_diverges tr e →
     1019    execution_matches_behavior e (Diverges tr)
     1020| emb_reacts: ∀e,tr.
     1021    execution_reacts tr e →
     1022    execution_matches_behavior e (Reacts tr)
     1023| emb_wrong: ∀e,tr.
     1024    execution_goes_wrong tr e →
     1025    execution_matches_behavior e (Goes_wrong tr).
     1026
     1027(*
     1028nlemma silent_sound: ∀ge,s,e.
     1029  execution_diverging e →
     1030  exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
     1031  forever_silent (mk_transrel ?? step) … ge s.
     1032#ge s e H; ncases H; #s1 e1 H' EXEC;
     1033napply (forever_silent_intro (mk_transrel ?? step) … ge s s1);
     1034##[ nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC;
     1035    nnormalize in EXEC;
     1036 nnormalize in match exec_inf_aux in EXEC:(??%?);
     1037
     1038ntheorem exec_inf_sound: ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
     1039*)
Note: See TracChangeset for help on using the changeset viewer.