Changeset 2923


Ignore:
Timestamp:
Mar 21, 2013, 8:38:52 AM (4 years ago)
Author:
campbell
Message:

Remove some leftovers.

Location:
src/RTLabs
Files:
1 deleted
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_partial_traces.ma

    r2897 r2923  
    13751375destruct //
    13761376qed.
    1377 (*
    1378 (* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
    1379        a trace_label_diverges value, but I only know how to construct those
    1380        using a cofixpoint in Type[0], which means I can't use the termination
    1381        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) with
    1393 [ ex_intro n B ⇒
    1394     match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
    1395       return λs:RTLabs_ext_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
    1396     with
    1397     [ 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 ? in
    1399             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 ? with
    1402         [ ex_intro T' _ ⇒
    1403             ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
    1404         ]*)
    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 ? in
    1407             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 ? with
    1410         [ ex_intro T' _ ⇒
    1411             ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
    1412         ]*)
    1413     ] STATEMENT_COSTLABEL
    1414 ].
    1415 [ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T)
    1416 | @EV
    1417 | 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) #CL
    1420   [ @simplify_cl @CL
    1421   | @⊥ @(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 destruct
    1435 #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 #_ destruct
    1437      inversion SP
    1438      [ 3: #s1 #r #M0 #S #E1 #E2 #E3 #E4 destruct % #E whd in E:(??%?); destruct
    1439      | *: #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 destruct
    1441      ]
    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 destruct
    1443 ] 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 destruct
    1453 @refl
    1454 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 with
    1470 [ 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) with
    1476 [ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
    1477     let IS_CALL ≝ initial_state_is_call … INITIAL in
    1478     let s' ≝ mk_RTLabs_ext_state ge s stk mtc in
    1479     let next' ≝ next_state ge s' next tr EV in
    1480     match ORACLE ge O next trace' with
    1481     [ or_introl TERMINATES ⇒
    1482         match TERMINATES with
    1483         [ witness TERMINATES ⇒
    1484           let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
    1485           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 destruct
    1495   cases FINAL #E @E @refl
    1496 | %{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 destruct
    1507     ]
    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 ? fd
    1517    | _ ⇒ False ].
    1518 #p #s
    1519 @bind_ok #m #Em
    1520 @bind_ok #b #Eb
    1521 @bind_ok #f #Ef
    1522 #E whd in E:(??%%); destruct
    1523 %{b} whd
    1524 % [% [%] ] // [ @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) #b
    1530 cases s
    1531 [ #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.
    15361377
    15371378lemma well_cost_labelled_initial : ∀p,s.
     
    15621403* #id * #fn // * /2/
    15631404qed.
    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 in
    1573  
    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 in
    1578  
    1579   trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).
    1580 
    1581 #ORACLE #p #WCL #s #I
    1582 letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
    1583 #NOIO #NW
    1584 letin flat_trace ≝ (make_whole_flat_trace p s NOIO NW I)
    1585 whd
    1586 @(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_trace
    1590 | @I
    1591 | @(proj1 ?? (well_cost_labelled_initial … I WCL))
    1592 | @(proj2 ?? (well_cost_labelled_initial … I WCL))
    1593 ] qed.
    1594 *)
    15951405
    15961406lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge.
Note: See TracChangeset for help on using the changeset viewer.