Changeset 378 for C-semantics/CexecIO.ma


Ignore:
Timestamp:
Dec 6, 2010, 11:49:57 AM (9 years ago)
Author:
campbell
Message:

More work on equivalence of whole executions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r366 r378  
    13291329    execution_isteps tr' s e s' e' →
    13301330    k i = e_step tr s e →
    1331     (¬ ∃r.final_state s r) → (* used to avoid showing that k i doesn't end prog *)
     1331(*    (¬ ∃r.final_state s r) → (* used to avoid showing that k i doesn't end prog *)*)
    13321332    execution_isteps (tr⧺tr') s0 (e_interact o k) s' e'.
     1333
     1334nlemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3.
     1335  execution_isteps tr1 s1 e1 s2 e2 →
     1336  execution_isteps tr2 s2 e2 s3 e3 →
     1337  execution_isteps (tr1⧺tr2) s1 e1 s3 e3.
     1338#tr1 tr2 s1 s2 s3 e1 e2 e3 H1; nelim H1;
     1339##[ #s e; //;
     1340##| #e e' tr tr' s1' s2' s3' H1 H2 H3;
     1341    nrewrite > (Eapp_assoc …);
     1342    napply isteps_one;
     1343    napply H2; napply H3;
     1344##| #e e' o k i s1' s2' s3' tr tr' H1 H2 H3 H4;
     1345    nrewrite > (Eapp_assoc …);
     1346    napply (isteps_interact … H2); /2/;
     1347##] nqed.
    13331348
    13341349nlemma exec_e_step: ∀ge,x,tr,s,e.
     
    13531368    ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    13541369    napply refl;
     1370##| #EXEC; nwhd in EXEC:(??%?); ndestruct
     1371##] nqed.
     1372
     1373nlemma exec_e_step_inv2: ∀ge,x,tr,s,e.
     1374  exec_inf_aux ge x = e_step tr s e →
     1375  ¬∃r.final_state s r.
     1376#ge x tr s e;
     1377nrewrite > (exec_inf_aux_unfold …); ncases x;
     1378##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
     1379##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
     1380    ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
     1381    napply FINAL;
    13551382##| #EXEC; nwhd in EXEC:(??%?); ndestruct
    13561383##] nqed.
     
    13951422    ##| #E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
    13961423    ##]
    1397 ##| #e e' o k i s s' s0 tr tr' H1 H2 H3 IH;
     1424##| #e e' o k i s s' s0 tr tr' H1 H2 IH;
    13981425    nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%? → ?);
    13991426    ncases (is_final_state s0); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
     
    14111438    ##[ nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%?);
    14121439        ncases (is_final_state s);
    1413         ##[ #X; ncases X; #r FINAL'; napply False_ind; napply (absurd ?? H3);
     1440        ##[ #X; ncases X; #r FINAL'; napply False_ind;
     1441            ncases (exec_e_step_inv2 … H2); #H; napply H;
    14141442            @ r; napply FINAL' ##]
    14151443        #FINAL'; nwhd in ⊢ (??%?);
     
    14311459ninductive execution_terminates : trace → state → execution → state → Prop ≝
    14321460| terminates : ∀s,s',tr,tr',r,e,m.
    1433     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) → execution_terminates (tr⧺tr') s e (Returnstate (Vint r) Kstop m)
     1462(* We should only be able to get to here if main is an external function, which is silly. *)
     1463| annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i.
     1464    execution_isteps tr s e s' (e_interact o k) →
     1465    k i = e_stop tr' r m →
     1466    execution_terminates (tr⧺tr') s e (Returnstate (Vint r) Kstop m).
    14341467
    14351468ncoinductive execution_diverging : execution → Prop ≝
     
    15101543##] nqed.
    15111544
     1545nlemma e_stop_inv: ∀ge,x,tr,r,m.
     1546  exec_inf_aux ge x = e_stop tr r m →
     1547  x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
     1548#ge x tr r m;
     1549nrewrite > (exec_inf_aux_unfold …); ncases x;
     1550##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct;
     1551##| #z; ncases z; #tr' s'; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
     1552  ##[ #F; ncases F; #r' FINAL; ncases FINAL; #r'' m' EXEC; nwhd in EXEC:(??%?);
     1553      ndestruct (EXEC); napply refl;
     1554  ##| #F EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
     1555  ##]
     1556##| #EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
     1557##] nqed.
     1558
    15121559nlemma terminates_sound: ∀ge,tr,s,s',e.
    15131560  execution_terminates tr s e s' →
     
    15151562  ∃r. star (mk_transrel … step) ge s tr s' ∧ final_state s' r.
    15161563#ge tr0 s0 s0' e0 H; ncases H;
    1517 #s s' tr tr' r e m ESTEPS EXEC; @r; @; //;
    1518 ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
    1519 napply (star_right … STARs');
    1520 ##[ ##2: napply (final_step ge tr' r m s');
    1521          napply (exec_e_step … EXECs');
    1522 ##| ##skip
    1523 ##| napply refl
     1564##[ #s s' tr tr' r e m ESTEPS EXEC; @r; @; //;
     1565    ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
     1566    napply (star_right … STARs');
     1567    ##[ ##2: napply (final_step ge tr' r m s');
     1568             napply (exec_e_step … EXECs');
     1569    ##| ##skip
     1570    ##| napply refl
     1571    ##]
     1572##| #s s' tr tr' r e m o k i ESTEPS EXECK EXEC; @r; @; //;
     1573    ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
     1574    napply (star_right … STARs');
     1575    ##[ ##2: nlapply (exec_step_sound ge s');
     1576             nlapply (exec_e_step … EXECs');
     1577             ncases (exec_step ge s');
     1578             ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …); #EXECs'';
     1579                 nwhd in EXECs'':(??%?) ⊢ (% → ?);
     1580                 ncut (o' = o); ##[ ndestruct (EXECs''); // ##] #E1;
     1581                 nrewrite > E1 in k' EXECs'' ⊢ %; #k' EXECs'';
     1582                 ncut (k = λv.exec_inf_aux ge (k' v)); ##[ ndestruct (EXECs''); // ##] #E2;
     1583                 nrewrite > E2 in ESTEPS EXECK EXECs' EXECs'';
     1584                 #ESTEPS EXECK EXECs' EXECs'' STEP; nlapply (STEP i);
     1585                 nrewrite > (e_stop_inv … EXECK); nwhd in ⊢ (% → ?);
     1586                 //;
     1587             ##| #z; ncases z; #tr'' s''; nrewrite > (exec_inf_aux_unfold …);
     1588                 nwhd in ⊢ (??%? → ?); ncases (is_final_state s'');
     1589                 #H EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC)
     1590             ##| nrewrite > (exec_inf_aux_unfold …);
     1591                 #EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC)
     1592             ##]
     1593    ##| ##skip
     1594    ##| napply refl
     1595    ##]
    15241596##] nqed.
    15251597
Note: See TracChangeset for help on using the changeset viewer.