Changeset 2923 for src/RTLabs/RTLabs_partial_traces.ma
 Timestamp:
 Mar 21, 2013, 8:38:52 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabs_partial_traces.ma
r2897 r2923 1375 1375 destruct // 1376 1376 qed. 1377 (*1378 (* NB: This isn't quite what I'd like. Ideally, we'd show the existence of1379 a trace_label_diverges value, but I only know how to construct those1380 using a cofixpoint in Type[0], which means I can't use the termination1381 oracle.1382 *)1383 1384 let corec make_label_diverges ge (s:RTLabs_ext_state ge)1385 (trace: flat_trace io_out io_in ge s)1386 (ORACLE: termination_oracle)1387 (TRACE_OK: remainder_ok ge s trace)1388 (ENV_COSTLABELLED: well_cost_labelled_ge ge)1389 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)1390 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *)1391 : trace_label_diverges_exists (RTLabs_status ge) s ≝1392 match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with1393 [ ex_intro n B ⇒1394 match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B1395 return λs:RTLabs_ext_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s1396 with1397 [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.1398 let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in1399 tld_step' (RTLabs_status ge) s s' (tll_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) T'1400 (*1401 match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with1402 [ ex_intro T' _ ⇒1403 ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I1404 ]*)1405  fp_tac s s2 s3 T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.1406 let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in1407 tld_base' (RTLabs_status ge) s s2 s3 (tlc_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) ?? T'1408 (*1409 match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with1410 [ ex_intro T' _ ⇒1411 ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?1412 ]*)1413 ] STATEMENT_COSTLABEL1414 ].1415 [ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T)1416  @EV1417  cases (trace_any_call_call … T) // #CL cases (RTLabs_notail' … CL)1418  cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') //1419 cases (trace_any_call_call … T) #CL1420 [ @simplify_cl @CL1421  @⊥ @(RTLabs_notail' … CL)1422 ]1423 ] qed.1424 1425 lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_ext_state ge.1426 as_execute (RTLabs_status ge) s1 s2 →1427 make_initial_state p = OK ? s1 →1428 stack_preserved ge ends_with_ret s2 s' →1429 RTLabs_is_final s' ≠ None ?.1430 #ge #p * #s1 #S1 #M1 * #s2 #S2 #M2 * #s' #S' #M' #EV whd in ⊢ (??%? → ?);1431 @bind_ok #m #_1432 @bind_ok #b #_1433 @bind_ok #f #_1434 #E destruct1435 #SP inversion (eval_preserves_ext … EV)1436 [ 3: #ge' #vf #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #S #M #M0' #E1 #E2 #E3 #_ destruct1437 inversion SP1438 [ 3: #s1 #r #M0 #S #E1 #E2 #E3 #E4 destruct % #E whd in E:(??%?); destruct1439  *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 try #H41 destruct @⊥1440 inversion H39 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 try #H71 try #H72 try #H73 try #H74 try #H75 destruct1441 ]1442  *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 try #H111 try #H112 try #H113 destruct1443 ] qed.1444 1445 lemma initial_state_is_call : ∀p,s.1446 make_initial_state p = OK ? s →1447 RTLabs_classify s = cl_call.1448 #p #s whd in ⊢ (??%? → ?);1449 @bind_ok #m #_1450 @bind_ok #b #_1451 @bind_ok #f #_1452 #E destruct1453 @refl1454 qed.1455 1456 let rec whole_structured_trace_exists ge p (s:RTLabs_ext_state ge)1457 (ORACLE: termination_oracle)1458 (ENV_COSTLABELLED: well_cost_labelled_ge ge)1459 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)1460 : ∀trace: flat_trace io_out io_in ge s.1461 ∀INITIAL: make_initial_state p = OK state s.1462 ∀STATE_COSTLABELLED: well_cost_labelled_state s.1463 ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.1464 trace_whole_program_exists (RTLabs_status ge) s ≝1465 match s return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.1466 make_initial_state p = OK ? s →1467 well_cost_labelled_state s →1468 soundly_labelled_state s →1469 trace_whole_program_exists (RTLabs_status ge) s with1470 [ mk_RTLabs_ext_state s0 stk mtc0 ⇒ λtrace.1471 match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.1472 make_initial_state p = OK state s →1473 well_cost_labelled_state s →1474 soundly_labelled_state s →1475 trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_ext_state ge s stk mtc) with1476 [ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.1477 let IS_CALL ≝ initial_state_is_call … INITIAL in1478 let s' ≝ mk_RTLabs_ext_state ge s stk mtc in1479 let next' ≝ next_state ge s' next tr EV in1480 match ORACLE ge O next trace' with1481 [ or_introl TERMINATES ⇒1482 match TERMINATES with1483 [ witness TERMINATES ⇒1484 let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in1485 twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) (IS_CALL) ? (new_trace … tlr) ?1486 ]1487  or_intror NO_TERMINATION ⇒1488 twp_diverges (RTLabs_status ge) s' next' (IS_CALL) ?1489 (make_label_diverges ge next' trace' ORACLE ?1490 ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)1491 ]1492  ft_stop st FINAL ⇒ λmtc,INITIAL. ⊥1493 ] mtc0 ].1494 [ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #vf * #fn * #args * #dst * #stk * #m #E destruct1495 cases FINAL #E @E @refl1496  %{tr} %{EV} %1497  @(after_the_initial_call_is_the_final_state … p s' next')1498 [ %{tr} %{EV} %  @INITIAL  @(stack_ok … tlr) ]1499  @(well_cost_labelled_state_step … EV) //1500  @(well_cost_labelled_call … EV) //1501  %{tr} %{EV} %1502  @(well_cost_labelled_call … EV) //1503  % [ @(well_cost_labelled_state_step … EV) //1504  @(soundly_labelled_state_step … EV) //1505  @(not_to_not … NO_TERMINATION) * #d * #TM % /2/1506  @(not_return_to_not_final … EV) >IS_CALL % #E destruct1507 ]1508 ] qed.1509 *)1510 lemma init_state_is : ∀p,s.1511 make_initial_state p = OK ? s →1512 𝚺b. match s with [ Callstate fid fd _ _ fs _ ⇒1513 fs = [ ] ∧1514 fid = prog_main … p ∧1515 find_symbol ? (make_global p) (prog_main … p) = Some ? b ∧1516 find_funct_ptr ? (make_global p) b = Some ? fd1517  _ ⇒ False ].1518 #p #s1519 @bind_ok #m #Em1520 @bind_ok #b #Eb1521 @bind_ok #f #Ef1522 #E whd in E:(??%%); destruct1523 %{b} whd1524 % [% [%] ] // [ @Eb  @Ef ]1525 qed.1526 1527 definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_ext_state (make_global p) ≝1528 λp,s,I. mk_RTLabs_ext_state (make_global p) s [init_state_is p s I] ?.1529 cases (init_state_is p s I) #b1530 cases s1531 [ #f #fs #m *1532  #fid #fd #args #dst #fs #m * * * #E1 #E2 #E3 #E4 destruct whd % /2/1533  #rv #rr #fs #m *1534  #r *1535 ] qed.1536 1377 1537 1378 lemma well_cost_labelled_initial : ∀p,s. … … 1562 1403 * #id * #fn // * /2/ 1563 1404 qed. 1564 (*1565 theorem program_trace_exists :1566 termination_oracle →1567 ∀p:RTLabs_program.1568 well_cost_labelled_program p →1569 ∀s:state.1570 ∀I: make_initial_state p = OK ? s.1571 1572 let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in1573 1574 ∀NOIO:exec_no_io … plain_trace.1575 ∀NW:not_wrong … plain_trace.1576 1577 let flat_trace ≝ make_whole_flat_trace p s NOIO NW I in1578 1579 trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).1580 1581 #ORACLE #p #WCL #s #I1582 letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)1583 #NOIO #NW1584 letin flat_trace ≝ (make_whole_flat_trace p s NOIO NW I)1585 whd1586 @(whole_structured_trace_exists (make_global p) p ? ORACLE)1587 [ @(proj1 … (well_cost_labelled_make_global … WCL))1588  @(proj2 … (well_cost_labelled_make_global … WCL))1589  @flat_trace1590  @I1591  @(proj1 ?? (well_cost_labelled_initial … I WCL))1592  @(proj2 ?? (well_cost_labelled_initial … I WCL))1593 ] qed.1594 *)1595 1405 1596 1406 lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge.
Note: See TracChangeset
for help on using the changeset viewer.