Changeset 398 for C-semantics/CexecIO.ma


Ignore:
Timestamp:
Dec 9, 2010, 8:35:41 PM (10 years ago)
Author:
campbell
Message:

This time actually prove the result I intended.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r389 r398  
    13241324##] nqed.
    13251325
    1326 (* starting after state s, zero or more steps of execution e reach state s'
    1327    after which comes e'. *)
    1328 ninductive execution_isteps : trace → state → execution → state → execution → Prop ≝
    1329 | isteps_none : ∀s,e. execution_isteps E0 s e s e
    1330 | isteps_one : ∀e,e',tr,tr',s,s',s0.
    1331     execution_isteps tr' s e s' e' →
    1332     execution_isteps (tr⧺tr') s0 (e_step tr s e) s' e'
    1333 | isteps_interact : ∀e,e',o,k,i,s,s',s0,tr,tr'.
    1334     execution_isteps tr' s e s' e' →
    1335     k i = e_step tr s e →
    1336 (*    (¬ ∃r.final_state s r) → (* used to avoid showing that k i doesn't end prog *)*)
    1337     execution_isteps (tr⧺tr') s0 (e_interact o k) s' e'.
    1338 
    1339 nlemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3.
    1340   execution_isteps tr1 s1 e1 s2 e2 →
    1341   execution_isteps tr2 s2 e2 s3 e3 →
    1342   execution_isteps (tr1⧺tr2) s1 e1 s3 e3.
    1343 #tr1 tr2 s1 s2 s3 e1 e2 e3 H1; nelim H1;
    1344 ##[ #s e; //;
    1345 ##| #e e' tr tr' s1' s2' s3' H1 H2 H3;
    1346     nrewrite > (Eapp_assoc …);
    1347     napply isteps_one;
    1348     napply H2; napply H3;
    1349 ##| #e e' o k i s1' s2' s3' tr tr' H1 H2 H3 H4;
    1350     nrewrite > (Eapp_assoc …);
    1351     napply (isteps_interact … H2); /2/;
    1352 ##] nqed.
    1353 
    1354 nlemma exec_e_step: ∀ge,x,tr,s,e.
    1355   exec_inf_aux ge x = e_step tr s e →
    1356   exec_inf_aux ge (exec_step ge s) = e.
    1357 #ge x tr s e;
    1358 nrewrite > (exec_inf_aux_unfold …); ncases x;
    1359 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    1360 ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
    1361     ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    1362     napply refl;
    1363 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct
    1364 ##] nqed.
    1365 
    1366 nlemma exec_e_step_inv: ∀ge,x,tr,s,e.
    1367   exec_inf_aux ge x = e_step tr s e →
    1368   x = Value ??? 〈tr,s〉.
    1369 #ge x tr s e;
    1370 nrewrite > (exec_inf_aux_unfold …); ncases x;
    1371 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    1372 ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
    1373     ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    1374     napply refl;
    1375 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct
    1376 ##] nqed.
    1377 
    1378 nlemma exec_e_step_inv2: ∀ge,x,tr,s,e.
    1379   exec_inf_aux ge x = e_step tr s e →
    1380   ¬∃r.final_state s r.
    1381 #ge x tr s e;
    1382 nrewrite > (exec_inf_aux_unfold …); ncases x;
    1383 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    1384 ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
    1385     ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    1386     napply FINAL;
    1387 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct
    1388 ##] nqed.
    1389 
    1390 (* NB: the E0 in the execs are irrelevant. *)
    1391 nlemma several_steps: ∀ge,tr,e,e',s,s'.
    1392   execution_isteps tr s e s' e' →
    1393   exec_inf_aux ge (Value ??? 〈E0,s〉) = e_step E0 s e →
    1394   star (mk_transrel … step) ge s tr s' ∧
    1395   exec_inf_aux ge (Value ??? 〈E0,s'〉) = e_step E0 s' e'.
    1396 #ge tr0 e0 e0' s0 s0' H;
    1397 nelim H;
    1398 ##[ #s e EXEC; @; //; napply EXEC;
    1399 ##| #e1 e2 tr1 tr2 s1 s2 s3 STEPS IH EXEC;
    1400     nrewrite > (exec_inf_aux_unfold ge ?) in EXEC;
    1401     nwhd in ⊢ (??%? → ?);
    1402     ncases (is_final_state s3); ##[ nwhd in ⊢ (? → ??%? → ?); #FINAL BAD; ndestruct (BAD) ##]
    1403     #NOTFINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    1404     nrewrite > (exec_inf_aux_unfold ge ?) in e3;
    1405     nlapply (refl ? (exec_step ge s3));
    1406     ncases (exec_step ge s3) in ⊢ (???% → %);
    1407     ##[ #o k E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
    1408     ##| #x; ncases x; #tr' s' EXEC3;
    1409         nwhd in ⊢ (??%? → ?);
    1410         ncases (is_final_state s'); #FINAL' EXEC'; nwhd in EXEC':(??%?); ##[ ndestruct ##]
    1411         ncut (exec_inf_aux ge (exec_step ge s1) = e1); ##[ ndestruct (EXEC'); napply refl ##]
    1412         #EXEC'';
    1413         nlapply (IH ?);
    1414         ##[ nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%?);
    1415             ncases (is_final_state s1); #FINAL1;
    1416             ##[ napply False_ind; napply (absurd ?? FINAL'); ncases FINAL1;
    1417                 #r' Hr; @ r'; ndestruct (EXEC'); napply Hr;
    1418             ##| nwhd in ⊢ (??%?); nrewrite < EXEC''; napply refl
    1419             ##]
    1420         ##| *; #STARs1s2 EXEC2; @;
    1421             ##[ nlapply (exec_step_sound ge s3); nrewrite > EXEC3;
    1422                 nwhd in ⊢ (% → ?); #STEP3; ndestruct (EXEC');
    1423                 napply (star_step (mk_transrel ?? step) … STEP3 STARs1s2); //;
    1424             ##| napply EXEC2;
    1425             ##]
    1426         ##]
    1427     ##| #E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
    1428     ##]
    1429 ##| #e e' o k i s s' s0 tr tr' H1 H2 IH;
    1430     nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%? → ?);
    1431     ncases (is_final_state s0); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    1432    
    1433     nrewrite > (exec_inf_aux_unfold ge ?) in e1;
    1434     nlapply (exec_step_sound ge s0);
    1435     ncases (exec_step ge s0);
    1436     ##[ #i' k' SOUND E1; nwhd in SOUND E1:(??%?); ndestruct (E1);
    1437     ##| #x; ncases x; #tr' s'' SOUND; nwhd in ⊢ (??%? → ?);
    1438         ncases (is_final_state s''); #FINAL'; nwhd in ⊢ (??%? → ?); #EXEC';
    1439         ndestruct (EXEC');
    1440     ##| #_; nwhd in ⊢ (??%? → ?); #EXEC'; ndestruct (EXEC');
    1441     ##]
    1442     nlapply (IH ?);
    1443     ##[ nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%?);
    1444         ncases (is_final_state s);
    1445         ##[ #X; ncases X; #r FINAL'; napply False_ind;
    1446             ncases (exec_e_step_inv2 … H2); #H; napply H;
    1447             @ r; napply FINAL' ##]
    1448         #FINAL'; nwhd in ⊢ (??%?);
    1449         nrewrite > (exec_e_step … H2);
    1450         napply refl;
    1451     ##| *; #STARsTOs' EXECs'; @;
    1452       ##[ napply (star_step … STARsTOs');
    1453           ##[ ##2: nlapply (SOUND i);
    1454                    nrewrite > (exec_e_step_inv … H2); nwhd in ⊢ (% → ?);
    1455                    #STEP; napply STEP;
    1456           ##| ##skip;
    1457           ##| napply refl
    1458           ##]
    1459       ##| napply EXECs';
    1460       ##]
    1461     ##]
    1462 ##] nqed.
    1463 
    1464 ninductive execution_terminates : trace → state → execution → int → mem → Prop ≝
    1465 | terminates : ∀s,s',tr,tr',r,e,m.
    1466     execution_isteps tr s e s' (e_stop tr' r m) →
    1467     execution_terminates (tr⧺tr') s (e_step E0 s e) r m
    1468 (* We should only be able to get to here if main is an external function, which is silly. *)
    1469 | annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i.
    1470     execution_isteps tr s e s' (e_interact o k) →
    1471     k i = e_stop tr' r m →
    1472     execution_terminates (tr⧺tr') s (e_step E0 s e) r m.
    1473 
    1474 ncoinductive execution_diverging : execution → Prop ≝
    1475 | diverging_step : ∀s,e. execution_diverging e → execution_diverging (e_step E0 s e).
    1476 
    1477 (* Makes a finite number of interactions (including cost labels) before diverging. *)
    1478 ninductive execution_diverges : trace → state → execution → Prop ≝
    1479 | diverges_diverging: ∀tr,s,s',e,e'.
    1480     execution_isteps tr s e s' e' →
    1481     execution_diverging e' →
    1482     execution_diverges tr s (e_step E0 s e).
    1483 
    1484 (* NB: "reacting" includes hitting a cost label. *)
    1485 ncoinductive execution_reacting : traceinf → state → execution → Prop ≝
    1486 | reacting: ∀tr,tr',s,s',e,e'.
    1487     execution_reacting tr' s' e' →
    1488     execution_isteps tr s e s' e' →
    1489     tr ≠ E0 →
    1490     execution_reacting (tr⧻tr') s e.
    1491 
    1492 ninductive execution_reacts : traceinf → state → execution → Prop ≝
    1493 | reacts: ∀tr,s,e.
    1494     execution_reacting tr s e →
    1495     execution_reacts tr s (e_step E0 s e).
    1496 
    1497 ninductive execution_goes_wrong: trace → state → execution → state → Prop ≝
    1498 | go_wrong: ∀tr,s,s',e.
    1499     execution_isteps tr s e s' e_wrong →
    1500     execution_goes_wrong tr s (e_step E0 s e) s'.
    1501 
    1502 nlet corec silent_sound ge s e
    1503   (H0:execution_diverging e)
    1504   (EXEC:exec_inf_aux ge (Value ??? 〈E0,s〉) = e_step E0 s e)
    1505   : 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);
    1507 ##[ ncases H0 in EXEC ⊢ %; #s1 e1 H1;
    1508     nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
    1509     ncases (is_final_state s); #p EXEC; nwhd in EXEC:(??%?); ndestruct;
    1510     @ s1; @ e1; @; //; napply e0;
    1511 ##| *; #s2; *; #e2; *; #H2 EXEC2;
    1512     napply (forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??));
    1513     ncut (exec_step ge s = Value ??? 〈E0,s2〉);
    1514     ##[ ##1,3,5: nrewrite > (exec_inf_aux_unfold …) in EXEC2; nelim (exec_step ge s);
    1515       ##[ ##1,4,7: #o k IH EXEC2; nwhd in EXEC2:(??%?); ndestruct;
    1516       ##| ##2,5,8: #x; ncases x; #tr s'; nwhd in ⊢ (??%? → ?);
    1517           ncases (is_final_state s'); #p' EXEC2; nwhd in EXEC2:(??%?); ndestruct;
    1518           napply refl;
    1519       ##| ##3,6,9: #EXEC2; nwhd in EXEC2:(??%?); ndestruct
    1520       ##]
    1521     ##| #EXEC1; nlapply (exec_step_sound ge s); nrewrite > EXEC1; nwhd in ⊢ (% → %); //
    1522     ##| #EXEC1; nrewrite > EXEC1 in EXEC2; #EXEC2; napply EXEC2;
    1523     ##| #EXEC1; napply H2;
    1524     ##]
    1525 ##]
    1526 nqed.
    1527 
    1528 nlemma final_step: ∀ge,tr,r,m,s.
    1529   exec_inf_aux ge (exec_step ge s) = e_stop tr r m →
    1530   step ge s tr (Returnstate (Vint r) Kstop m).
    1531 #ge tr r m s;
    1532 nrewrite > (exec_inf_aux_unfold …);
    1533 nlapply (exec_step_sound ge s);
    1534 ncases (exec_step ge s);
    1535 ##[ #o k H EXEC; nwhd in EXEC:(??%?); ndestruct
    1536 ##| #x; ncases x; #tr' s' SOUND; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
    1537     #FINAL EXEC; nwhd in SOUND EXEC:(??%?); ndestruct;
    1538     ncases FINAL; #r' FINAL'; ninversion FINAL';
    1539     #r'' m' E1 E2; ndestruct;
    1540     napply SOUND;
    1541 ##| #_; #EXEC; nwhd in EXEC:(??%?); ndestruct
    1542 ##] nqed.
    1543 
    1544 nlemma e_stop_inv: ∀ge,x,tr,r,m.
    1545   exec_inf_aux ge x = e_stop tr r m →
    1546   x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
    1547 #ge x tr r m;
    1548 nrewrite > (exec_inf_aux_unfold …); ncases x;
    1549 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct;
    1550 ##| #z; ncases z; #tr' s'; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
    1551   ##[ #F; ncases F; #r' FINAL; ncases FINAL; #r'' m' EXEC; nwhd in EXEC:(??%?);
    1552       ndestruct (EXEC); napply refl;
    1553   ##| #F EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
    1554   ##]
    1555 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
    1556 ##] nqed.
    1557 
    1558 nlemma terminates_sound: ∀ge,tr,s,r,m,e.
    1559   execution_terminates tr s (e_step E0 s e) r m →
    1560   exec_inf_aux ge (Value ??? 〈E0, s〉) = (e_step E0 s e) →
    1561   star (mk_transrel … step) ge s tr (Returnstate (Vint r) Kstop m).
    1562 #ge tr0 s0 r m e0 H; ncases H;
    1563 ##[ #s s' tr tr' r e m ESTEPS EXEC;
    1564     ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
    1565     napply (star_right … STARs');
    1566     ##[ ##2: napply (final_step ge tr' r m s');
    1567              napply (exec_e_step … EXECs');
    1568     ##| ##skip
    1569     ##| napply refl
    1570     ##]
    1571 ##| #s s' tr tr' r e m o k i ESTEPS EXECK EXEC;
    1572     ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
    1573     napply (star_right … STARs');
    1574     ##[ ##2: nlapply (exec_step_sound ge s');
    1575              nlapply (exec_e_step … EXECs');
    1576              ncases (exec_step ge s');
    1577              ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …); #EXECs'';
    1578                  nwhd in EXECs'':(??%?) ⊢ (% → ?);
    1579                  ncut (o' = o); ##[ ndestruct (EXECs''); // ##] #E1;
    1580                  nrewrite > E1 in k' EXECs'' ⊢ %; #k' EXECs'';
    1581                  ncut (k = λv.exec_inf_aux ge (k' v)); ##[ ndestruct (EXECs''); // ##] #E2;
    1582                  nrewrite > E2 in ESTEPS EXECK EXECs' EXECs'';
    1583                  #ESTEPS EXECK EXECs' EXECs'' STEP; nlapply (STEP i);
    1584                  nrewrite > (e_stop_inv … EXECK); nwhd in ⊢ (% → ?);
    1585                  //;
    1586              ##| #z; ncases z; #tr'' s''; nrewrite > (exec_inf_aux_unfold …);
    1587                  nwhd in ⊢ (??%? → ?); ncases (is_final_state s'');
    1588                  #H EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC)
    1589              ##| nrewrite > (exec_inf_aux_unfold …);
    1590                  #EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC)
    1591              ##]
    1592     ##| ##skip
    1593     ##| napply refl
    1594     ##]
    1595 ##] nqed.
    1596 
    1597 nlet corec reacts_sound ge tr s e
    1598   (REACTS:execution_reacting tr s e)
    1599   (EXEC:exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e) :
    1600   forever_reactive (mk_transrel … step) ge s tr ≝ ?.
    1601 ncut (∃s'.∃e'.∃tr'.∃tr''.execution_reacting tr'' s' e' ∧ execution_isteps tr' s e s' e' ∧ tr' ≠ E0 ∧ tr = tr'⧻tr'');
    1602 ##[ ninversion REACTS;
    1603     #tr0 tr' s0 s' e0 e' EREACTS ESTEPS REACTED E1 E2 E3; ndestruct (E2 E3);
    1604     @ s'; @ e'; @ tr0; @ tr'; @; ##[ @; ##[ @; //; ##| napply REACTED ##] ##| napply refl ##]
    1605 ##| *; #s'; *; #e'; *; #tr'; *; #tr'';
    1606     *; *; *; #REACTS' ESTEPS REACTED APPTR;
    1607 (*    nrewrite > APPTR;*)
    1608     napply (match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ]);
    1609     @;
    1610     ncases (several_steps … ESTEPS EXEC); #STEPS EXEC';
    1611     ##[ ##2: napply STEPS;
    1612     ##| ##skip
    1613     ##| napply REACTED
    1614     ##| napply reacts_sound;
    1615       ##[ ##2: napply REACTS';
    1616       ##| ##skip
    1617       ##| napply EXEC'
    1618       ##]
    1619     ##]
    1620 nqed.
Note: See TracChangeset for help on using the changeset viewer.