Changeset 291


Ignore:
Timestamp:
Nov 25, 2010, 12:54:13 PM (9 years ago)
Author:
campbell
Message:

Soundness of behaviour of exec_inf_aux on finite number of steps.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r252 r291  
    12181218*)
    12191219
    1220 (* A (possibly non-terminating) execution. *)
     1220
     1221
     1222(* A (possibly non-terminating) execution.   *)
    12211223ncoinductive execution : Type ≝
    1222 | e_stop : trace → int → execution
     1224| e_stop : trace → int → mem → execution
    12231225| e_step : trace → state → execution → execution
    12241226| e_wrong : execution
    12251227| e_interact : io_out → (eventval → execution) → execution.
     1228
     1229ndefinition mem_of_state : state → mem ≝
     1230λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
     1231
     1232(* This definition is slightly awkward because of the need to provide resumptions.
     1233   It records the last trace/state passed in, then recursively processes the next
     1234   state. *)
    12261235
    12271236nlet corec exec_inf_aux (ge:genv) (s:IO eventval io_out (trace×state)) : execution ≝
     
    12301239| Value v ⇒ match v with [ mk_pair t s' ⇒
    12311240    match is_final_state s' with
    1232     [ inl r ⇒ e_stop t (sig_eject … r)
     1241    [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s')
    12331242    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
    12341243| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
     
    12401249
    12411250nremark execution_cases: ∀e.
    1242  e = match e with [ e_stop tr r ⇒ e_stop tr r | e_step tr s e ⇒ e_step tr s e
     1251 e = match e with [ e_stop tr r m ⇒ e_stop tr r m | e_step tr s e ⇒ e_step tr s e
    12431252 | e_wrong ⇒ e_wrong | e_interact o k ⇒ e_interact o k ].
    12441253#e; ncases e; //; nqed.
     
    12491258| Value v ⇒ match v with [ mk_pair t s' ⇒
    12501259    match is_final_state s' with
    1251     [ inl r ⇒ e_stop t (sig_eject … r)
     1260    [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s')
    12521261    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
    12531262| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
     
    12711280| steps_one : ∀e,e',tr,tr',s. execution_steps tr' e e' → execution_steps (tr⧺tr') (e_step tr s e) e'.
    12721281
    1273 (* Finite number of steps allowing interaction. *)
    1274 ninductive execution_isteps : trace → execution → execution → Prop ≝
    1275 | isteps_none : ∀e. execution_isteps E0 e e
    1276 | isteps_step : ∀e,e',tr,tr',s. execution_isteps tr e e' → execution_isteps (tr⧺tr') (e_step tr s e) e'
    1277 | isteps_interact : ∀k,o,i,e',tr. execution_isteps tr (k i) e' → execution_isteps tr (e_interact o k) e'.
     1282nlemma one_step: ∀ge,tr,s,tr',s',e.
     1283  exec_inf_aux ge (Value ??? 〈tr,s〉) = e_step tr s (e_step tr' s' e) →
     1284  step ge s tr' s'.
     1285#ge tr s tr' s' e;
     1286nrewrite > (exec_inf_aux_unfold ge ?);
     1287nwhd in ⊢ (??%? → ?); ncases (is_final_state s);
     1288##[ #H E; nwhd in E:(??%?); ndestruct (E);
     1289##| #H E; nwhd in E:(??%?); ndestruct;
     1290    nrewrite > (exec_inf_aux_unfold ge ?) in e0;
     1291    nlapply (refl ? (exec_step ge s));
     1292    ncases (exec_step ge s) in ⊢ (???% → %);
     1293    ##[ #i o E1 E2; nwhd in E2:(??%?); ndestruct (E2);
     1294    ##| #x; ncases x; #tr'' s'' E1 E2; nwhd in E2:(??%?);
     1295        ncases (is_final_state s'') in E2;
     1296        #H' E2; nwhd in E2:(??%?); ndestruct (E2);
     1297        nlapply (exec_step_sound ge s);
     1298        nrewrite > E1; nwhd in ⊢ (% → ?);
     1299        #H1; napply H1
     1300    ##| #E1 E2; nwhd in E2:(??%?); ndestruct;
     1301    ##]
     1302##] nqed.
     1303
     1304(* starting after state s, zero or more steps of execution e reach state s'
     1305   after which comes e'. *)
     1306ninductive execution_isteps : trace → state → execution → state → execution → Prop ≝
     1307| isteps_none : ∀s,e. execution_isteps E0 s e s e
     1308| isteps_one : ∀e,e',tr,tr',s,s',s0.
     1309    execution_isteps tr' s e s' e' →
     1310    execution_isteps (tr⧺tr') s0 (e_step tr s e) s' e'
     1311| isteps_interact : ∀e,e',k,o,i,s,s',s0,tr,tr'.
     1312    execution_isteps tr' s e s' e' →
     1313    k i = e_step tr s e →
     1314    (¬ ∃r.final_state s r) → (* used to avoid showing that k i doesn't end prog *)
     1315    execution_isteps (tr⧺tr') s0 (e_interact o k) s' e'.
     1316
     1317nlemma exec_e_step: ∀ge,x,tr,s,e.
     1318  exec_inf_aux ge x = e_step tr s e →
     1319  exec_inf_aux ge (exec_step ge s) = e.
     1320#ge x tr s e;
     1321nrewrite > (exec_inf_aux_unfold …); ncases x;
     1322##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
     1323##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
     1324    ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
     1325    napply refl;
     1326##| #EXEC; nwhd in EXEC:(??%?); ndestruct
     1327##] nqed.
     1328
     1329nlemma exec_e_step_inv: ∀ge,x,tr,s,e.
     1330  exec_inf_aux ge x = e_step tr s e →
     1331  x = Value ??? 〈tr,s〉.
     1332#ge x tr s e;
     1333nrewrite > (exec_inf_aux_unfold …); ncases x;
     1334##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
     1335##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
     1336    ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
     1337    napply refl;
     1338##| #EXEC; nwhd in EXEC:(??%?); ndestruct
     1339##] nqed.
     1340
     1341(* NB: the E0 in the execs are irrelevant. *)
     1342nlemma several_steps: ∀ge,tr,e,e',s,s'.
     1343  execution_isteps tr s e s' e' →
     1344  exec_inf_aux ge (Value ??? 〈E0,s〉) = e_step E0 s e →
     1345  star (mk_transrel … step) ge s tr s' ∧
     1346  exec_inf_aux ge (Value ??? 〈E0,s'〉) = e_step E0 s' e'.
     1347#ge tr0 e0 e0' s0 s0' H;
     1348nelim H;
     1349##[ #s e EXEC; @; //; napply EXEC;
     1350##| #e1 e2 tr1 tr2 s1 s2 s3 STEPS IH EXEC;
     1351    nrewrite > (exec_inf_aux_unfold ge ?) in EXEC;
     1352    nwhd in ⊢ (??%? → ?);
     1353    ncases (is_final_state s3); ##[ nwhd in ⊢ (? → ??%? → ?); #FINAL BAD; ndestruct (BAD) ##]
     1354    #NOTFINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
     1355    nrewrite > (exec_inf_aux_unfold ge ?) in e3;
     1356    nlapply (refl ? (exec_step ge s3));
     1357    ncases (exec_step ge s3) in ⊢ (???% → %);
     1358    ##[ #o k E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
     1359    ##| #x; ncases x; #tr' s' EXEC3;
     1360        nwhd in ⊢ (??%? → ?);
     1361        ncases (is_final_state s'); #FINAL' EXEC'; nwhd in EXEC':(??%?); ##[ ndestruct ##]
     1362        ncut (exec_inf_aux ge (exec_step ge s1) = e1); ##[ ndestruct (EXEC'); napply refl ##]
     1363        #EXEC'';
     1364        nlapply (IH ?);
     1365        ##[ nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%?);
     1366            ncases (is_final_state s1); #FINAL1;
     1367            ##[ napply False_ind; napply (absurd ?? FINAL'); ncases FINAL1;
     1368                #r' Hr; @ r'; ndestruct (EXEC'); napply Hr;
     1369            ##| nwhd in ⊢ (??%?); nrewrite < EXEC''; napply refl
     1370            ##]
     1371        ##| *; #STARs1s2 EXEC2; @;
     1372            ##[ nlapply (exec_step_sound ge s3); nrewrite > EXEC3;
     1373                nwhd in ⊢ (% → ?); #STEP3; ndestruct (EXEC');
     1374                napply (star_step (mk_transrel ?? step) … STEP3 STARs1s2); //;
     1375            ##| napply EXEC2;
     1376            ##]
     1377        ##]
     1378    ##| #E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
     1379    ##]
     1380##| #e e' k o i s s' s0 tr tr' H1 H2 H3 IH;
     1381    nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%? → ?);
     1382    ncases (is_final_state s0); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
     1383   
     1384    nrewrite > (exec_inf_aux_unfold ge ?) in e1;
     1385    nlapply (exec_step_sound ge s0);
     1386    ncases (exec_step ge s0);
     1387    ##[ #i' k' SOUND E1; nwhd in SOUND E1:(??%?); ndestruct (E1);
     1388    ##| #x; ncases x; #tr' s'' SOUND; nwhd in ⊢ (??%? → ?);
     1389        ncases (is_final_state s''); #FINAL'; nwhd in ⊢ (??%? → ?); #EXEC';
     1390        ndestruct (EXEC');
     1391    ##| #_; nwhd in ⊢ (??%? → ?); #EXEC'; ndestruct (EXEC');
     1392    ##]
     1393    nlapply (IH ?);
     1394    ##[ nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%?);
     1395        ncases (is_final_state s);
     1396        ##[ #X; ncases X; #r FINAL'; napply False_ind; napply (absurd ?? H3);
     1397            @ r; napply FINAL' ##]
     1398        #FINAL'; nwhd in ⊢ (??%?);
     1399        nrewrite > (exec_e_step … H2);
     1400        napply refl;
     1401    ##| *; #STARsTOs' EXECs'; @;
     1402      ##[ napply (star_step … STARsTOs');
     1403          ##[ ##2: nlapply (SOUND i);
     1404                   nrewrite > (exec_e_step_inv … H2); nwhd in ⊢ (% → ?);
     1405                   #STEP; napply STEP;
     1406          ##| ##skip;
     1407          ##| napply refl
     1408          ##]
     1409      ##| napply EXECs';
     1410      ##]
     1411    ##]
     1412##] nqed.
    12781413
    12791414ninductive execution_terminates : trace → int → execution → Prop ≝
    1280 | terminates : ∀tr,tr',r,e. execution_isteps tr e (e_stop tr' r) → execution_terminates (tr⧺tr') r e.
     1415| terminates : ∀s,s',tr,tr',r,e,m.
     1416    execution_isteps tr s e s' (e_stop tr' r m) → execution_terminates (tr⧺tr') r e.
    12811417
    12821418ncoinductive execution_diverging : execution → Prop ≝
     
    12851421(* Makes a finite number of interactions (including cost labels) before diverging. *)
    12861422ninductive execution_diverges : trace → execution → Prop ≝
    1287 | diverges_diverging: ∀tr,e,e'.
    1288     execution_isteps tr e e' →
     1423| diverges_diverging: ∀tr,s,s',e,e'.
     1424    execution_isteps tr s e s' e' →
    12891425    execution_diverging e' →
    12901426    execution_diverges tr e.
     
    12921428(* NB: "reacting" includes hitting a cost label. *)
    12931429ncoinductive execution_reacts : traceinf → execution → Prop ≝
    1294 | reacting: ∀tr,tr',e,e'. execution_reacts tr' e' → execution_isteps tr e e' → tr ≠ E0 → execution_reacts (tr⧻tr') e.
     1430| reacting: ∀tr,tr',s,s',e,e'. execution_reacts tr' e' → execution_isteps tr s e s' e' → tr ≠ E0 → execution_reacts (tr⧻tr') e.
    12951431
    12961432ninductive execution_goes_wrong: trace → execution → Prop ≝
    1297 | go_wrong: ∀tr,e. execution_isteps tr e e_wrong → execution_goes_wrong tr e.
     1433| go_wrong: ∀tr,s,s',e. execution_isteps tr s e s' e_wrong → execution_goes_wrong tr e.
    12981434
    12991435ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.