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

Almost finished whole program equivalence.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.