Changeset 385


Ignore:
Timestamp:
Dec 7, 2010, 5:22:51 PM (9 years ago)
Author:
campbell
Message:

Almost finished whole program equivalence.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r378 r385  
    11431143nqed.
    11441144
    1145 nlet rec make_initial_state (p:program) : IO io_out io_in state ≝
     1145nlet rec make_initial_state (p:program) : res state ≝
    11461146  let ge ≝ globalenv Genv ?? p in
    11471147  let m0 ≝ init_mem Genv ?? p in
    1148     ! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p);
    1149     ! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
    1150     ! f ← find_funct_ptr ? ? ge b;
    1151     ret ? (Callstate f (nil ?) Kstop m0).
    1152 
    1153 nlemma make_initial_state_sound : ∀p. P_io ??? (λs.initial_state p s) (make_initial_state p).
     1148    do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
     1149    do u ← opt_to_res ? (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
     1150    do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
     1151    OK ? (Callstate f (nil ?) Kstop m0).
     1152
     1153nlemma make_initial_state_sound : ∀p. P_res ? (λs.initial_state p s) (make_initial_state p).
    11541154#p; ncases p; #fns main vars;
    1155 nwhd in ⊢ (?????%);
    1156 napply opt_bindIO2_OK; #sp b esb;
    1157 napply opt_bindIO_OK; #u ecode;
    1158 napply opt_bindIO_OK; #f ef;
     1155nwhd in ⊢ (???%);
     1156napply opt_bind_OK; #x; ncases x; #sp b esb;
     1157napply opt_bind_OK; #u ecode;
     1158napply opt_bind_OK; #f ef;
    11591159ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##]
    11601160nwhd; napply (initial_state_intro … esb ef);
     
    14571457##] nqed.
    14581458
    1459 ninductive execution_terminates : trace → state → execution → state → Prop ≝
     1459ninductive execution_terminates : trace → state → execution → int → mem → Prop ≝
    14601460| terminates : ∀s,s',tr,tr',r,e,m.
    1461     execution_isteps tr s e s' (e_stop tr' r m) → execution_terminates (tr⧺tr') s e (Returnstate (Vint r) Kstop m)
     1461    execution_isteps tr s e s' (e_stop tr' r m) →
     1462    execution_terminates (tr⧺tr') s (e_step E0 s e) r m
    14621463(* We should only be able to get to here if main is an external function, which is silly. *)
    14631464| annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i.
    14641465    execution_isteps tr s e s' (e_interact o k) →
    14651466    k i = e_stop tr' r m →
    1466     execution_terminates (tr⧺tr') s e (Returnstate (Vint r) Kstop m).
     1467    execution_terminates (tr⧺tr') s (e_step E0 s e) r m.
    14671468
    14681469ncoinductive execution_diverging : execution → Prop ≝
     
    14701471
    14711472(* Makes a finite number of interactions (including cost labels) before diverging. *)
    1472 ninductive execution_diverges : trace → execution → Prop ≝
     1473ninductive execution_diverges : trace → state → execution → Prop ≝
    14731474| diverges_diverging: ∀tr,s,s',e,e'.
    14741475    execution_isteps tr s e s' e' →
    14751476    execution_diverging e' →
    1476     execution_diverges tr e.
     1477    execution_diverges tr s (e_step E0 s e).
    14771478
    14781479(* NB: "reacting" includes hitting a cost label. *)
    1479 ncoinductive execution_reacts : traceinf → state → execution → Prop ≝
    1480 | reacting: ∀tr,tr',s,s',e,e'. execution_reacts tr' s' e' → execution_isteps tr s e s' e' → tr ≠ E0 → execution_reacts (tr⧻tr') s e.
     1480ncoinductive execution_reacting : traceinf → state → execution → Prop ≝
     1481| reacting: ∀tr,tr',s,s',e,e'.
     1482    execution_reacting tr' s' e' →
     1483    execution_isteps tr s e s' e' →
     1484    tr ≠ E0 →
     1485    execution_reacting (tr⧻tr') s e.
     1486
     1487ninductive execution_reacts : traceinf → state → execution → Prop ≝
     1488| reacts: ∀tr,s,e.
     1489    execution_reacting tr s e →
     1490    execution_reacts tr s (e_step E0 s e).
    14811491
    14821492ninductive execution_goes_wrong: trace → state → execution → state → Prop ≝
    1483 | go_wrong: ∀tr,s,s',e. execution_isteps tr s e s' e_wrong → execution_goes_wrong tr s e s'.
    1484 
    1485 ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
    1486 | emb_terminates: ∀s,s',e,tr,r.
    1487     execution_terminates tr s e s' →
    1488     execution_matches_behavior e (Terminates tr r)
    1489 | emb_diverges: ∀e,tr.
    1490     execution_diverges tr e →
    1491     execution_matches_behavior e (Diverges tr)
     1493| go_wrong: ∀tr,s,s',e.
     1494    execution_isteps tr s e s' e_wrong →
     1495    execution_goes_wrong tr s (e_step E0 s e) s'.
     1496
     1497ninductive execution_matches_behavior: state → execution → program_behavior → Prop ≝
     1498| emb_terminates: ∀s,e,tr,r,m.
     1499    execution_terminates tr s e r m →
     1500    execution_matches_behavior s e (Terminates tr r)
     1501| emb_diverges: ∀s,e,tr.
     1502    execution_diverges tr s e →
     1503    execution_matches_behavior s e (Diverges tr)
    14921504| emb_reacts: ∀s,e,tr.
    14931505    execution_reacts tr s e →
    1494     execution_matches_behavior e (Reacts tr)
     1506    execution_matches_behavior s e (Reacts tr)
    14951507| emb_wrong: ∀e,s,s',tr.
    14961508    execution_goes_wrong tr s e s' →
    1497     execution_matches_behavior e (Goes_wrong tr).
     1509    execution_matches_behavior s e (Goes_wrong tr).
    14981510
    14991511(* We don't morally need the cut, but the proof I tried without it failed the
    15001512   guarded-by-constructors check and it wasn't apparent why. *)
    1501 
     1513(*
    15021514nlet corec silent_sound ge s e
    15031515  (H0:execution_diverging e)
    1504   (EXEC:exec_inf_aux ge (Value ??? 〈E0,s〉) = e)
     1516  (EXEC:exec_inf_aux ge (Value ??? 〈E0,s〉) = e_step E0 s e)
    15051517  : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
    1506 ncut (∃s2.∃e2.execution_diverging e2 ∧ exec_inf_aux ge (exec_step ge s) = e_step E0 s2 e2);
     1518(*ncut (∃s2.∃e2.execution_diverging e2 ∧ exec_inf_aux ge (exec_step ge s) = e_step E0 s2 e2);*)
    15071519##[ ncases H0 in EXEC ⊢ %; #s1 e1 H1;
    15081520    nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
     
    15251537    ##]
    15261538##]
     1539nqed.*)
     1540nlet corec silent_sound ge s e
     1541  (H0:execution_diverging e)
     1542  (EXEC:exec_inf_aux ge (Value ??? 〈E0,s〉) = e_step E0 s e)
     1543  : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
     1544ncut (∃s2.∃e2.execution_diverging e2 ∧ exec_inf_aux ge (exec_step ge s) = e_step E0 s2 e2);
     1545##[ ncases H0 in EXEC ⊢ %; #s1 e1 H1;
     1546    nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
     1547    ncases (is_final_state s); #p EXEC; nwhd in EXEC:(??%?); ndestruct;
     1548    @ s1; @ e1; @; //; napply e0;
     1549##| *; #s2; *; #e2; *; #H2 EXEC2;
     1550    napply (forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??));
     1551    ncut (exec_step ge s = Value ??? 〈E0,s2〉);
     1552    ##[ ##1,3,5: nrewrite > (exec_inf_aux_unfold …) in EXEC2; nelim (exec_step ge s);
     1553      ##[ ##1,4,7: #o k IH EXEC2; nwhd in EXEC2:(??%?); ndestruct;
     1554      ##| ##2,5,8: #x; ncases x; #tr s'; nwhd in ⊢ (??%? → ?);
     1555          ncases (is_final_state s'); #p' EXEC2; nwhd in EXEC2:(??%?); ndestruct;
     1556          napply refl;
     1557      ##| ##3,6,9: #EXEC2; nwhd in EXEC2:(??%?); ndestruct
     1558      ##]
     1559    ##| #EXEC1; nlapply (exec_step_sound ge s); nrewrite > EXEC1; nwhd in ⊢ (% → %); //
     1560    ##| #EXEC1; nrewrite > EXEC1 in EXEC2; #EXEC2; napply EXEC2;
     1561    ##| #EXEC1; napply H2;
     1562    ##]
     1563##]
    15271564nqed.
    15281565
     
    15571594##] nqed.
    15581595
    1559 nlemma terminates_sound: ∀ge,tr,s,s',e.
    1560   execution_terminates tr s e s'
     1596nlemma terminates_sound: ∀ge,tr,s,r,m,e.
     1597  execution_terminates tr s (e_step E0 s e) r m
    15611598  exec_inf_aux ge (Value ??? 〈E0, s〉) = (e_step E0 s e) →
    1562   ∃r. star (mk_transrel … step) ge s tr s' ∧ final_state s' r.
    1563 #ge tr0 s0 s0' e0 H; ncases H;
    1564 ##[ #s s' tr tr' r e m ESTEPS EXEC; @r; @; //;
     1599  star (mk_transrel … step) ge s tr (Returnstate (Vint r) Kstop m).
     1600#ge tr0 s0 r m e0 H; ncases H;
     1601##[ #s s' tr tr' r e m ESTEPS EXEC;
    15651602    ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
    15661603    napply (star_right … STARs');
     
    15701607    ##| napply refl
    15711608    ##]
    1572 ##| #s s' tr tr' r e m o k i ESTEPS EXECK EXEC; @r; @; //;
     1609##| #s s' tr tr' r e m o k i ESTEPS EXECK EXEC;
    15731610    ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
    15741611    napply (star_right … STARs');
     
    15971634
    15981635nlet corec reacts_sound ge tr s e
    1599   (REACTS:execution_reacts tr s e)
     1636  (REACTS:execution_reacting tr s e)
    16001637  (EXEC:exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e) :
    16011638  forever_reactive (mk_transrel … step) ge s tr ≝ ?.
    1602 ncut (∃s'.∃e'.∃tr'.∃tr''.execution_reacts tr'' s' e' ∧ execution_isteps tr' s e s' e' ∧ tr' ≠ E0 ∧ tr = tr'⧻tr'');
     1639ncut (∃s'.∃e'.∃tr'.∃tr''.execution_reacting tr'' s' e' ∧ execution_isteps tr' s e s' e' ∧ tr' ≠ E0 ∧ tr = tr'⧻tr'');
    16031640##[ ninversion REACTS;
    16041641    #tr0 tr' s0 s' e0 e' EREACTS ESTEPS REACTED E1 E2 E3; ndestruct (E2 E3);
  • C-semantics/CexecIOcomplete.ma

    r379 r385  
    5959##] nqed.
    6060
     61ndefinition yieldsbare ≝ λA.λa:res A.λv':A.
     62match a with [ OK v ⇒ v' = v | _ ⇒ False ].
     63
     64nlemma yieldsbare_eq: ∀A,a,v'. yieldsbare A a v' → a = OK ? v'.
     65#A a v'; ncases a; //; nwhd in ⊢ (% → ?); *;
     66nqed.
     67
     68nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
     69yieldsbare A a v' →
     70yields A P (err_inject A (λx.P x) (Some ? a) p) v'.
     71#A P a; ncases a;
     72##[ #v v' p H; napply H;
     73##| #a b; *;
     74##] nqed.
     75
    6176
    6277ntheorem the_initial_state:
    63   ∀p,s. initial_state p s → yieldsIObare ? (make_initial_state p) s.
     78  ∀p,s. initial_state p s → yieldsbare ? (make_initial_state p) s.
    6479#p s; ncases p; #fns main globs H;
    6580ninversion H;
     
    7186nwhd; napply refl;
    7287nqed.
    73 
    74 ndefinition yieldsbare ≝ λA.λa:res A.λv':A.
    75 match a with [ OK v ⇒ v' = v | _ ⇒ False ].
    76 
    77 nlemma yieldsbare_eq: ∀A,a,v'. yieldsbare A a v' → a = OK ? v'.
    78 #A a v'; ncases a; //; nwhd in ⊢ (% → ?); *;
    79 nqed.
    80 
    81 nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
    82 yieldsbare A a v' →
    83 yields A P (err_inject A (λx.P x) (Some ? a) p) v'.
    84 #A P a; ncases a;
    85 ##[ #v v' p H; napply H;
    86 ##| #a b; *;
    87 ##] nqed.
    8888
    8989nlemma cast_complete: ∀m,v,ty,ty',v'.
     
    482482 
    483483nlemma wrong_sound: ∀ge,tr,s,s',e.
    484   execution_goes_wrong tr s e s' →
     484  execution_goes_wrong tr s (e_step E0 s e) s' →
    485485  exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e →
    486486  star (mk_transrel … step) ge s tr s' ∧
     
    513513##] nqed.
    514514
    515 ninductive execution_characterisation : execution → Prop ≝
    516 | ec_terminates: ∀s,s',e,tr.
    517     execution_terminates tr s e s'
    518     execution_characterisation (e_step E0 s e)
     515ninductive execution_characterisation : state → execution → Prop ≝
     516| ec_terminates: ∀s,r,m,e,tr.
     517    execution_terminates tr s e r m
     518    execution_characterisation s e
    519519| ec_diverges: ∀s,e,tr.
    520     execution_diverges tr e →
    521     execution_characterisation (e_step E0 s e)
     520    execution_diverges tr s e →
     521    execution_characterisation s e
    522522| ec_reacts: ∀s,e,tr.
    523523    execution_reacts tr s e →
    524     execution_characterisation (e_step E0 s e)
     524    execution_characterisation s e
    525525| ec_wrong: ∀e,s,s',tr.
    526526    execution_goes_wrong tr s e s' →
    527     execution_characterisation (e_step E0 s e).
     527    execution_characterisation s e.
    528528
    529529(* bit of a hack to avoid inability to reduce term in match *)
     
    790790    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
    791791    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    792   : execution_reacts (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)) ≝ ?.
     792  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)) ≝ ?.
    793793napply daemon; (*
    794794nrewrite > (unroll_traceinf' (reactive_traceinf' …));
     
    804804  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
    805805   ∀ge,s. ¬ (∃r. final_state s r) →
    806    execution_characterisation (exec_inf_aux ge (Value ??? 〈E0,s〉)).
     806   execution_characterisation s (exec_inf_aux ge (Value ??? 〈E0,s〉)).
    807807#classic constructive_indefinite_description ge s; *; #NOTFINAL;
    808 nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (?%);
     808nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%);
    809809ncases (is_final_state s); ##[ #x; ncases x; #r FINAL; napply False_rect_Type0; napply NOTFINAL; @r; napply FINAL ##]
    810 #NOTFINAL'; nwhd in ⊢ (?%);
     810#NOTFINAL'; nwhd in ⊢ (??%);
    811811ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
    812812                 execution_not_over e1));
     
    815815                     ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
    816816  ##[ *; #tr; *; #s1; *; #e1; *; #INITIAL UNREACTIVE;
    817       napply (ec_diverges … tr);
     817      napply (ec_diverges … s ? tr);
    818818      napply (diverges_diverging … INITIAL);
    819819      napply (show_divergence s1);
     
    848848      ##| #REACTIVE;
    849849          napply ec_reacts;
    850           ##[ ##2: napply (show_reactive ge s …);
     850          ##[ ##2: napply reacts;
     851                   napply (show_reactive ge s …);
    851852                   #tr s1 e1 STEPS;
    852853                   napply constructive_indefinite_description;
     
    863864    ncases e;
    864865    ##[ #tr' r m; #STEPS NOSTEP;
    865         napply (ec_terminates s (Returnstate (Vint r) Kstop m) ? (Eapp tr tr')); @;
     866        napply (ec_terminates s r m ? (Eapp tr tr')); @;
    866867        ##[ napply s'
    867868        ##| napply STEPS
     
    871872    ##| #STEPS NOSTEP;
    872873        napply (ec_wrong ? s s' tr); @; //;
    873     (* The following is stupidly complicated for an impossible case.
     874    (* The following is stupidly complicated when most of the cases are impossible.
    874875       It ought to be simplified. *)
    875876    ##| #o; ncases o; #o_id o_args o_rty; ncases o_rty; #k STEPS NOSTEP;
     
    879880        ##[ ##1,5: #tr' r m K;
    880881                   napply (ec_terminates s ???);
    881                    ##[ ##3,6: napply (annoying_corner_case_terminates … STEPS K);
     882                   ##[ ##4,8: napply (annoying_corner_case_terminates … STEPS K);
    882883                   ##| ##*: ##skip
    883884                   ##]
     
    920921nqed.   
    921922
     923nlemma behavior_of_execution: ∀s,e.
     924  execution_characterisation s e →
     925  ∃b:program_behavior. execution_matches_behavior s e b.
     926#s0 e0 exec;
     927ncases exec;
     928##[ #s r m e tr TERM;
     929    @ (Terminates tr r);
     930    napply (emb_terminates … TERM);
     931##| #s e tr DIV;
     932    @ (Diverges tr);
     933    napply (emb_diverges … DIV);
     934##| #s e tr REACTS;
     935    @ (Reacts tr);
     936    napply (emb_reacts … REACTS);
     937##| #e s s' tr WRONG;
     938    @ (Goes_wrong tr);
     939    napply (emb_wrong … WRONG);
     940##] nqed.
     941
     942nlemma initial_state_not_final: ∀ge,s.
     943  initial_state ge s →
     944  ¬ ∃r.final_state s r.
     945#ge s H; ncases H;
     946#b f E1 E2; @; *; #r H2;
     947ninversion H2;
     948#r' m E3 E4; ndestruct (E3);
     949nqed.
     950
     951nlemma initial_step: ∀ge,s,e.
     952  exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
     953  ¬(∃r.final_state s r) →
     954  ∃e'.e = e_step E0 s e'.
     955#ge s e; nrewrite > (exec_inf_aux_unfold …);
     956nwhd in ⊢ (??%? → ?); ncases (is_final_state s);
     957##[ #FINAL EXEC NOTFINAL;
     958    napply False_ind; napply (absurd ?? NOTFINAL);
     959    ncases FINAL;
     960    #r F; @r; napply F;
     961##| #F1 EXEC F2; nwhd in EXEC:(??%?); @; ##[ ##2: nrewrite < EXEC; napply refl ##]
     962nqed.
     963
     964ntheorem exec_inf_sound:
     965  ∀classic:(∀P:Prop.P ∨ ¬P).
     966  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
     967  ∀p. ∃s,b.execution_matches_behavior s (exec_inf p) b ∧ exec_program p b.
     968#classic constructive_indefinite_description p;
     969nwhd in ⊢ (??(λ_.??(λ_.?(??%?)%))); nletin ge ≝ (globalenv Genv fundef type p);
     970nlapply (make_initial_state_sound p);
     971ncases (make_initial_state p);
     972##[ #s INITIAL; @s; nwhd in INITIAL ⊢ (??(λ_.?(??(??%)?)?));
     973    nlapply (behavior_of_execution ??
     974              (execution_characterisation_complete classic constructive_indefinite_description ge s ?));
     975    ##[ napply (initial_state_not_final … INITIAL);
     976    ##| *; #b MATCHES; @b; @; //;
     977        ninversion MATCHES;
     978        ##[ #s0 e tr r m TERM E1 EXEC BEHAVES;
     979            nrewrite < E1 in TERM; #TERM;
     980            nlapply (initial_step … EXEC ?);
     981            ##[ napply initial_state_not_final; //; ##]
     982            *; #e' E2; nrewrite > E2 in EXEC TERM; #EXEC TERM;
     983            napply (program_terminates (mk_transrel … step) ?? ge s);
     984            ##[ ##2: napply INITIAL
     985            ##| ##3: napply (terminates_sound … TERM EXEC);
     986            ##| ##skip
     987            ##| //;
     988            ##]
     989        ##| #s0 e tr DIVERGES E1 EXEC E2;
     990            nlapply (initial_step … EXEC ?);
     991            ##[ napply initial_state_not_final; //; ##]
     992            *; #e' E3; nrewrite < E1 in DIVERGES; nrewrite > E3 in EXEC ⊢ %;
     993            #EXEC DIVERGES;
     994            ninversion DIVERGES; #tr' s1 s2 e1 e2 INITSTEPS DIVERGING E4 E5 E6;
     995            nrewrite < E4 in INITSTEPS ⊢ %; nrewrite < E5 in E6 ⊢ %; #E6 INITSTEPS;
     996            ncut (e' = e1); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
     997            #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS;
     998            ncases (several_steps … INITSTEPS EXEC); #INITSTAR EXECDIV;
     999            napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);
     1000            napply (silent_sound … DIVERGING EXECDIV);
     1001        ##| #s0 e tr REACTS E1 EXEC E2;
     1002            nlapply (initial_step … EXEC ?);
     1003            ##[ napply initial_state_not_final; //; ##]
     1004            *; #e' E3; nrewrite < E1 in REACTS; nrewrite > E3 in EXEC ⊢ %;
     1005            #EXEC REACTS;
     1006            ninversion REACTS; #tr' s' e'' REACTING E4 E5;
     1007            nrewrite < E4 in REACTING ⊢ %; nrewrite < E5; #REACTING E6;
     1008            ncut (e' = e''); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
     1009            #E7; nrewrite < E7 in REACTING; #REACTING;
     1010            napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL);
     1011            napply (reacts_sound … REACTING EXEC);
     1012        ##| #e s1 s2 tr WRONG E1 EXEC E2;
     1013            nlapply (initial_step … EXEC ?);
     1014            ##[ napply initial_state_not_final; //; ##]
     1015            *; #e' E3; nrewrite < E1 in WRONG; nrewrite > E3 in EXEC ⊢ %;
     1016            #EXEC WRONG;
     1017            ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
     1018            nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
     1019            ncut (e' = e''); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
     1020            #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG;
     1021            nelim (wrong_sound … WRONG EXEC); *; #STAR STOP FINAL;
     1022            napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);
     1023            #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
     1024        ##]
     1025   ##]
     1026##| #_;
     1027
    9221028ndefinition behaviour_of_execution: ∀e.
    9231029 execution_characterisation e → program_behavior ≝
    9241030λe,exec.match exec with
    925 [ ec_terminates s s' e tr H ⇒ Terminates tr ?
     1031[ ec_terminates s r m e tr H ⇒ Terminates tr r
    9261032| ec_diverges _ e tr H ⇒ Diverges tr
    9271033| ec_reacts s e tr H ⇒ Reacts tr
Note: See TracChangeset for help on using the changeset viewer.