Changeset 1806 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Mar 5, 2012, 12:38:26 PM (8 years ago)
Author:
campbell
Message:

Show that we could construct RTLabs non-terminating structured traces
if it weren't for Prop/Type?/coinduction issue.
Separate out the inductive part of the coinductive structured traces so
that we get an induction principle.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1805 r1806  
    424424| #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct
    425425  inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
     426] qed.
     427
     428
     429lemma will_return_lower : ∀ge,d,s,t.
     430  will_return ge d s t →
     431  ∀d'. d' ≤ d →
     432  will_return ge d' s t.
     433#ge #d0 #s0 #t0 #TM elim TM
     434[ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/
     435| #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/
     436| #s #tr #s' #d #EX #tr #CL #TM1 #IH *
     437  [ #LE @wr_base //
     438  | #d' #LE %3 // @IH /2/
     439  ]
     440| #s #tr #s' #EX #tr #CL *
     441  [ #_ @wr_base //
     442  | #d' #LE @⊥ /2/
     443  ]
    426444] qed.
    427445
     
    13981416  ]
    13991417] qed.
    1400  
     1418
     1419
     1420
     1421
     1422definition soundly_labelled_fn : internal_function → Prop ≝
     1423λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
     1424
     1425definition soundly_labelled_ge : genv → Prop ≝
     1426λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
     1427
     1428definition soundly_labelled_state : state → Prop ≝
     1429λs. match s with
     1430[ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
     1431| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
     1432                          All ? (λf. soundly_labelled_fn (func f)) fs
     1433| Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
     1434| Finalstate _ ⇒ True
     1435].
     1436
     1437lemma steps_from_sound : ∀s.
     1438  RTLabs_cost s = true →
     1439  soundly_labelled_state s →
     1440  ∃n. state_bound_on_steps_to_cost s n.
     1441* [ #f #fs #m #CS | #a #b #c #d #e #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ]
     1442whd in ⊢ (% → ?); * #SLF #_
     1443cases (SLF (next f) (next_ok f)) #n #B1
     1444%{n} % @B1
     1445qed.
     1446
     1447lemma soundly_labelled_state_step : ∀ge,s,tr,s'.
     1448  soundly_labelled_ge ge →
     1449  eval_statement ge s = Value ??? 〈tr,s'〉 →
     1450  soundly_labelled_state s →
     1451  soundly_labelled_state s'.
     1452#ge #s #tr #s' #ENV #EV #S
     1453inversion (eval_perserves … EV)
     1454[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct
     1455  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
     1456| #ge' #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
     1457  whd in S ⊢ %; %
     1458  [ cases fd in FFP ⊢ %; // #fn #FFP @ENV //
     1459  | inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S
     1460  ]
     1461| #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
     1462  whd in S ⊢ %; @S
     1463| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
     1464  whd in S ⊢ %; cases S //
     1465| #ge' #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct
     1466  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
     1467| #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I
     1468] qed.
     1469
     1470lemma soundly_labelled_state_preserved : ∀s,s'.
     1471  stack_preserved ends_with_ret s s' →
     1472  soundly_labelled_state s →
     1473  soundly_labelled_state s'.
     1474#s0 #s0' #SP inversion SP
     1475[ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
     1476| #s1 #f #f' #fs #m #N #F #S1 #E1 #E2 #E3 #E4 destruct
     1477  inversion S1
     1478  [ #f1 #fs1 #m1 #E1 #E2 #E3 destruct
     1479    * #_ #S whd in S;
     1480    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
     1481    destruct @S
     1482  | #fd #args #dst #f1 #fs1 #m1 #E1 #E2 #E3 destruct * #_ * #_ #S
     1483    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
     1484    destruct @S
     1485  | #rtv #dst #fs1 #m1 #E1 #E2 #E3 destruct #S
     1486    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
     1487    destruct @S
     1488  ]
     1489| //
     1490| //
     1491] qed.
     1492
    14011493(* When constructing an infinite trace, we need to be able to grab the finite
    14021494   portion of the trace for the next [trace_label_diverges] constructor.  We
     
    14051497record remainder_ok (ge:genv) (s:state) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
    14061498  ro_well_cost_labelled: well_cost_labelled_state s;
     1499  ro_soundly_labelled: soundly_labelled_state s;
    14071500  ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
    14081501  ro_not_undefined: not_wrong … t;
     
    14161509           remainder_ok ge s' t →
    14171510           finite_prefix ge s
    1418 | fp_tac : ∀s,s'.
    1419            trace_any_call (RTLabs_status ge) s s' →
    1420            ∀t:flat_trace io_out io_in ge s'.
    1421            remainder_ok ge s' t →
    1422            finite_prefix ge s
     1511| fp_tac : ∀s1,s2,s3,tr.
     1512           trace_any_call (RTLabs_status ge) s1 s2 →
     1513           well_cost_labelled_state s2 →
     1514           eval_statement ge s2 = Value ??? 〈tr,s3〉 →
     1515           ∀t:flat_trace io_out io_in ge s3.
     1516           remainder_ok ge s3 t →
     1517           finite_prefix ge s1
    14231518.
    14241519
     
    14341529    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
    14351530    rem rok
    1436 | fp_tac s' sf TAC rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s sf
    1437     (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem rok
     1531| fp_tac s1 s2 s3 tr TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3 tr
     1532    (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
     1533    WCL2 EV rem rok
    14381534].
    14391535
    1440 definition fp_add_terminating_call : ∀ge,s,s1,s'.
     1536definition fp_add_terminating_call : ∀ge,s,s1,s''.
    14411537  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
    14421538  ∀CALL:RTLabs_classify s = cl_call.
    1443   finite_prefix ge s'
    1444   trace_label_return (RTLabs_status ge) s1 s'
    1445   as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s'
    1446   RTLabs_cost s' = false →
     1539  finite_prefix ge s''
     1540  trace_label_return (RTLabs_status ge) s1 s''
     1541  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s''
     1542  RTLabs_cost s'' = false →
    14471543  finite_prefix ge s ≝
    1448 λge,s,s1,s',EVAL,CALL,fp.
    1449 match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → RTLabs_cost s' = false → finite_prefix ge s with
    1450 [ fp_tal s' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
    1451     (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
     1544λge,s,s1,s'',EVAL,CALL,fp.
     1545match fp return λs''.λ_. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with
     1546[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
     1547    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
    14521548    rem rok
    1453 | fp_tac s' sf TAC rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf
    1454     (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
    1455     rem rok
     1549| fp_tac s'' s2 s3 tr TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3 tr
     1550    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
     1551    WCL2 EV rem rok
    14561552].
    14571553
     
    14731569  (TRACE_OK: remainder_ok ge s trace)
    14741570  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     1571  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
     1572  (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)
    14751573  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
    14761574  on n : finite_prefix ge s ≝
     
    14881586                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' TRACE_OK'
    14891587            | false ⇒ λCS.
    1490                 let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ? in
     1588                let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
    14911589                fp_add_default ge ?? CL fs ? CS
    14921590            ] (refl ??)
     
    15021600                [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr) TRACE_OK'
    15031601                | false ⇒ λCS.
    1504                     let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ? in
     1602                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
    15051603                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
    15061604                ] (refl ??)
    15071605              ]
    15081606            | or_intror NO_TERMINATION ⇒
    1509                 fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace') ?
     1607                fp_tac ????? (tac_base (RTLabs_status ge) start CL) ? EV trace' ?
    15101608            ]
    15111609        | cl_return ⇒ λCL. ⊥
     
    15211619| 5,6,8,9,10,11: /3/
    15221620| % [ @(well_cost_labelled_state_step … EV) /2/
     1621    | @(soundly_labelled_state_step … EV) /2/
    15231622    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
    15241623    | @(still_not_wrong … EV) /2/
     
    15261625    ]
    15271626| /2/
     1627| @(soundly_labelled_state_preserved … (stack_ok … tlr))
     1628  @(soundly_labelled_state_step … EV) /2/
    15281629| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
    15291630  @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
    15301631| % [ /2/
     1632    | @(soundly_labelled_state_preserved … (stack_ok … tlr))
     1633      @(soundly_labelled_state_step … EV) /2/
    15311634    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
    15321635      @wr_call //
     
    15571660| @(well_cost_labelled_state_step … EV) /2/
    15581661| @(well_cost_labelled_call … EV) /2/
    1559 | % /2/
    1560 | 18,19,20: /2/
     1662| /2/
     1663| % [ @(well_cost_labelled_state_step … EV) /2/
     1664    | @(soundly_labelled_state_step … EV) /2/
     1665    | @(not_to_not … NO_TERMINATION) * #depth * #TM %
     1666      @(will_return_lower … TM) //
     1667    | @(still_not_wrong … EV) /2/
     1668    | @(not_return_to_not_final … EV) >CL % #E destruct
     1669    ]
     1670| 20,21,22: /2/
     1671| @(soundly_labelled_state_step … EV) /2/
    15611672| cases (bound_after_step … LABEL_LIMIT EV ?)
    15621673  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
     
    15841695  ]
    15851696| % [ @(well_cost_labelled_state_step … EV) /2/
     1697    | @(soundly_labelled_state_step … EV) /2/
    15861698    | @(not_to_not … (ro_no_termination … TRACE_OK))
    15871699      * #depth * #TERM %{depth} % @wr_step /2/
     
    15951707] qed.
    15961708
    1597 definition soundly_labelled_fn : internal_function → Prop ≝
    1598 λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
    1599 
    1600 definition soundly_labelled_ge : genv → Prop ≝
    1601 λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
    1602 
    1603 definition soundly_labelled_state : state → Prop ≝
    1604 λs. match s with
    1605 [ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
    1606 | Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
    1607                           All ? (λf. soundly_labelled_fn (func f)) fs
    1608 | Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
    1609 | Finalstate _ ⇒ True
    1610 ].
    1611 
    1612 lemma steps_from_sound : ∀s.
    1613   RTLabs_cost s = true →
    1614   soundly_labelled_state s →
    1615   ∃n. state_bound_on_steps_to_cost s n.
    1616 * [ #f #fs #m #CS | #a #b #c #d #e #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ]
    1617 whd in ⊢ (% → ?); * #SLF #_
    1618 cases (SLF (next f) (next_ok f)) #n #B1
    1619 %{n} % @B1
    1620 qed.
     1709(* FIXME:
     1710
     1711   This isn't going to work in this form: the existential isn't the coinductive
     1712   type, so this isn't technically a cofixpoint.  Try to return just the
     1713   structured trace won't either, because the termination oracle is in Prop.
     1714   
     1715   Not sure how to get out of this situation...
     1716*)
    16211717
    16221718let corec make_label_diverges ge s
     
    16311727match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with
    16321728[ ex_intro n B ⇒
    1633     match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED B
     1729    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED STATE_SOUNDLY_LABELLED B
    16341730      return λs.λ_. RTLabs_cost s = true → ∃T:trace_label_diverges (RTLabs_status ge) s. True
    16351731    with
     
    16391735            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
    16401736        ]
    1641     | fp_tac s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
    1642         match t return λs',t. trace_any_call ? s s' → remainder_ok ge s' t → ∃T:trace_label_diverges (RTLabs_status ge) s. True
    1643         with
    1644         [ ft_step s' tr next EV t' ⇒ λT,tOK.
    1645             match make_label_diverges ge next t' ORACLE ? ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
    1646             [ ex_intro T' _ ⇒
    1647                 ex_intro ?? (tld_base (RTLabs_status ge) s s' next (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
    1648             ]
    1649         | _ ⇒ λT. ⊥
    1650         ] T tOK
     1737    | fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
     1738        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
     1739        [ ex_intro T' _ ⇒
     1740            ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
     1741        ]
    16511742    ] STATEMENT_COSTLABEL
    16521743].
    1653 [
     1744[ /2/
     1745| @(trace_any_label_label … T)
     1746| @(trace_any_call_call … T)
     1747| %{tr} @EV
     1748| @I
     1749| /2/
     1750| @(well_cost_labelled_call … EV) // @(trace_any_call_call … T)
     1751] (* XXX fails, see above. *) qed.
Note: See TracChangeset for help on using the changeset viewer.