Changeset 386


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

Whole program equivalence result for the Clight executable and inductive
semantics (modulo a lemma that requires the unfolding of a cofixpoint).

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r385 r386  
    14951495    execution_goes_wrong tr s (e_step E0 s e) s'.
    14961496
    1497 ninductive 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)
    1504 | emb_reacts: ∀s,e,tr.
    1505     execution_reacts tr s e →
    1506     execution_matches_behavior s e (Reacts tr)
    1507 | emb_wrong: ∀e,s,s',tr.
    1508     execution_goes_wrong tr s e s' →
    1509     execution_matches_behavior s e (Goes_wrong tr).
    1510 
    1511 (* We don't morally need the cut, but the proof I tried without it failed the
    1512    guarded-by-constructors check and it wasn't apparent why. *)
    1513 (*
    1514 nlet corec silent_sound ge s e
    1515   (H0:execution_diverging e)
    1516   (EXEC:exec_inf_aux ge (Value ??? 〈E0,s〉) = e_step E0 s e)
    1517   : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
    1518 (*ncut (∃s2.∃e2.execution_diverging e2 ∧ exec_inf_aux ge (exec_step ge s) = e_step E0 s2 e2);*)
    1519 ##[ ncases H0 in EXEC ⊢ %; #s1 e1 H1;
    1520     nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
    1521     ncases (is_final_state s); #p EXEC; nwhd in EXEC:(??%?); ndestruct;
    1522     ninversion H1; #s2 e2 H2 EXEC2;
    1523     @ s2; @ e2; @; //;
    1524 ##| *; #s2; *; #e2; *; #H2 EXEC2;
    1525     napply (forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 (e_step E0 s2 e2) ??));
    1526     ncut (exec_step ge s = Value ??? 〈E0,s2〉);
    1527     ##[ ##1,3,5: nrewrite > (exec_inf_aux_unfold …) in EXEC2; nelim (exec_step ge s);
    1528       ##[ ##1,4,7: #o k IH EXEC2; nwhd in EXEC2:(??%?); ndestruct;
    1529       ##| ##2,5,8: #x; ncases x; #tr s'; nwhd in ⊢ (??%? → ?);
    1530           ncases (is_final_state s'); #p' EXEC2; nwhd in EXEC2:(??%?); ndestruct;
    1531           napply refl;
    1532       ##| ##3,6,9: #EXEC2; nwhd in EXEC2:(??%?); ndestruct
    1533       ##]
    1534     ##| #EXEC1; nlapply (exec_step_sound ge s); nrewrite > EXEC1; nwhd in ⊢ (% → %); //
    1535     ##| #EXEC1; nrewrite > EXEC1 in EXEC2; #EXEC2; napply EXEC2;
    1536     ##| #EXEC1; @; napply H2;
    1537     ##]
    1538 ##]
    1539 nqed.*)
    15401497nlet corec silent_sound ge s e
    15411498  (H0:execution_diverging e)
     
    16571614    ##]
    16581615nqed.
    1659 
    1660 (* is/needs completeness...
    1661 nlemma wrong_sound: ∀ge,tr,s,s',e.
    1662   execution_goes_wrong tr s e s' →
    1663   exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e →
    1664   star (mk_transrel … step) ge s tr s' ∧
    1665   nostep (mk_transrel … step) ge s' ∧
    1666   (¬∃r. final_state s' r).
    1667 #ge tr0 s0 s0' e0 WRONG; ncases WRONG;
    1668 #tr s s' e ESTEPS EXEC;
    1669 ncases (several_steps … ESTEPS EXEC);
    1670 #STAR EXEC';
    1671 *)
    1672 
    1673 (*
    1674 ntheorem exec_inf_sound: ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
    1675 *)
  • C-semantics/CexecIOcomplete.ma

    r385 r386  
    921921nqed.   
    922922
     923ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
     924| emb_terminates: ∀s,e,tr,r,m.
     925    execution_terminates tr s e r m →
     926    execution_matches_behavior e (Terminates tr r)
     927| emb_diverges: ∀s,e,tr.
     928    execution_diverges tr s e →
     929    execution_matches_behavior e (Diverges tr)
     930| emb_reacts: ∀s,e,tr.
     931    execution_reacts tr s e →
     932    execution_matches_behavior e (Reacts tr)
     933| emb_wrong: ∀e,s,s',tr.
     934    execution_goes_wrong tr s e s' →
     935    execution_matches_behavior e (Goes_wrong tr)
     936| emb_initially_wrong:
     937    execution_matches_behavior e_wrong (Goes_wrong E0).
     938
     939nlemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
     940  execution_terminates tr s (e_step tr' s' e) r m → s = s'.
     941#tr tr' s s' e r m H; ninversion H;
     942##[ #s1 s2 tr1 tr2 r' e' m' H' E1 E2 E3 E4 E5; ndestruct; napply refl
     943##| #s1 s2 tr1 tr2 r' e' m' o k i H' E1 E2 E3 E4 E5 E6; ndestruct; napply refl
     944##] nqed.
     945
     946nlemma exec_state_diverges: ∀tr,tr',s,s',e.
     947  execution_diverges tr s (e_step tr' s' e) → s = s'.
     948#tr tr' s s' e H; ninversion H;
     949#tr1 s1 s2 e1 e2 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
     950
     951nlemma exec_state_reacts: ∀tr,tr',s,s',e.
     952  execution_reacts tr s (e_step tr' s' e) → s = s'.
     953#tr tr' s s' e H; ninversion H;
     954#tr1 s1 e1 H' E1 E2 E3; ndestruct; napply refl; nqed.
     955
     956nlemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
     957  execution_goes_wrong tr s (e_step tr' s' e) s'' → s = s'.
     958#tr tr' s s' s'' e H; ninversion H;
     959#tr1 s1 s2 e1 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
     960
    923961nlemma behavior_of_execution: ∀s,e.
    924962  execution_characterisation s e →
    925   ∃b:program_behavior. execution_matches_behavior s e b.
     963  ∃b:program_behavior. execution_matches_behavior e b.
    926964#s0 e0 exec;
    927965ncases exec;
     
    9651003  ∀classic:(∀P:Prop.P ∨ ¬P).
    9661004  ∀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.
     1005  ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
    9681006#classic constructive_indefinite_description p;
    969 nwhd in ⊢ (??(λ_.??(λ_.?(??%?)%))); nletin ge ≝ (globalenv Genv fundef type p);
     1007nwhd in ⊢ (??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);
    9701008nlapply (make_initial_state_sound p);
     1009nlapply (the_initial_state p);
    9711010ncases (make_initial_state p);
    972 ##[ #s INITIAL; @s; nwhd in INITIAL ⊢ (??(λ_.?(??(??%)?)?));
     1011##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (??(λ_.?(?(??%)?)?));
    9731012    nlapply (behavior_of_execution ??
    9741013              (execution_characterisation_complete classic constructive_indefinite_description ge s ?));
     
    9761015    ##| *; #b MATCHES; @b; @; //;
    9771016        ninversion MATCHES;
    978         ##[ #s0 e tr r m TERM E1 EXEC BEHAVES;
    979             nrewrite < E1 in TERM; #TERM;
     1017        ##[ #s0 e tr r m TERM EXEC BEHAVES;
    9801018            nlapply (initial_step … EXEC ?);
    9811019            ##[ napply initial_state_not_final; //; ##]
    9821020            *; #e' E2; nrewrite > E2 in EXEC TERM; #EXEC TERM;
     1021            nlapply (exec_state_terminates … TERM); #E1;
     1022            nrewrite > E1 in TERM; #TERM;
    9831023            napply (program_terminates (mk_transrel … step) ?? ge s);
    9841024            ##[ ##2: napply INITIAL
     
    9871027            ##| //;
    9881028            ##]
    989         ##| #s0 e tr DIVERGES E1 EXEC E2;
     1029        ##| #s0 e tr DIVERGES EXEC E2;
    9901030            nlapply (initial_step … EXEC ?);
    9911031            ##[ napply initial_state_not_final; //; ##]
    992             *; #e' E3; nrewrite < E1 in DIVERGES; nrewrite > E3 in EXEC ⊢ %;
    993             #EXEC DIVERGES;
     1032            *; #e' E3; nrewrite > E3 in DIVERGES EXEC ⊢ %;
     1033            #DIVERGES EXEC; nlapply (exec_state_diverges … DIVERGES);
     1034            #E1; nrewrite > E1 in DIVERGES; #DIVERGES;
    9941035            ninversion DIVERGES; #tr' s1 s2 e1 e2 INITSTEPS DIVERGING E4 E5 E6;
    9951036            nrewrite < E4 in INITSTEPS ⊢ %; nrewrite < E5 in E6 ⊢ %; #E6 INITSTEPS;
     
    9991040            napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);
    10001041            napply (silent_sound … DIVERGING EXECDIV);
    1001         ##| #s0 e tr REACTS E1 EXEC E2;
     1042        ##| #s0 e tr REACTS EXEC E2;
    10021043            nlapply (initial_step … EXEC ?);
    10031044            ##[ napply initial_state_not_final; //; ##]
    1004             *; #e' E3; nrewrite < E1 in REACTS; nrewrite > E3 in EXEC ⊢ %;
     1045            *; #e' E3; nrewrite > E3 in EXEC REACTS ⊢ %;
    10051046            #EXEC REACTS;
     1047            nlapply (exec_state_reacts … REACTS);
     1048            #E1; nrewrite > E1 in REACTS; #REACTS;
    10061049            ninversion REACTS; #tr' s' e'' REACTING E4 E5;
    10071050            nrewrite < E4 in REACTING ⊢ %; nrewrite < E5; #REACTING E6;
     
    10101053            napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL);
    10111054            napply (reacts_sound … REACTING EXEC);
    1012         ##| #e s1 s2 tr WRONG E1 EXEC E2;
     1055        ##| #e s1 s2 tr WRONG EXEC E2;
    10131056            nlapply (initial_step … EXEC ?);
    10141057            ##[ napply initial_state_not_final; //; ##]
    1015             *; #e' E3; nrewrite < E1 in WRONG; nrewrite > E3 in EXEC ⊢ %;
     1058            *; #e' E3; nrewrite > E3 in EXEC WRONG ⊢ %;
    10161059            #EXEC WRONG;
     1060            nlapply (exec_state_wrong … WRONG);
     1061            #E1; nrewrite > E1 in WRONG; #WRONG;
    10171062            ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
    10181063            nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
     
    10221067            napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);
    10231068            #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
     1069        ##| nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
     1070            ncases (is_final_state s); #F EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
    10241071        ##]
    10251072   ##]
    1026 ##| #_;
    1027 
    1028 ndefinition behaviour_of_execution: ∀e.
    1029  execution_characterisation e → program_behavior ≝
    1030 λe,exec.match exec with
    1031 [ ec_terminates s r m e tr H ⇒ Terminates tr r
    1032 | ec_diverges _ e tr H ⇒ Diverges tr
    1033 | ec_reacts s e tr H ⇒ Reacts tr
    1034 | ec_wrong e s s' tr H ⇒ Goes_wrong tr
    1035 ].
    1036 
     1073##| nwhd in ⊢ ((∀_.? → %) → ?);
     1074    #NOINIT WHATEVER;
     1075    @ (Goes_wrong E0); @;
     1076    ##[ nwhd in ⊢ (?(??%)?);
     1077        nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (?%?);
     1078        napply emb_initially_wrong;
     1079    ##| napply program_goes_initially_wrong;
     1080        #s; @; napply NOINIT;
     1081    ##]
     1082##] nqed.
     1083
Note: See TracChangeset for help on using the changeset viewer.