Changeset 1805


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

RTLabs structured traces: package up some of the properties we need about
finite segments of nonterminating executions to use in the corecursive
function.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1784 r1805  
    14031403   use the fact that the trace is soundly labelled to achieve this. *)
    14041404
     1405record remainder_ok (ge:genv) (s:state) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
     1406  ro_well_cost_labelled: well_cost_labelled_state s;
     1407  ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
     1408  ro_not_undefined: not_wrong … t;
     1409  ro_not_final: RTLabs_is_final s = None ?
     1410}.
     1411
    14051412inductive finite_prefix (ge:genv) : state → Prop ≝
    14061413| fp_tal : ∀s,s'.
    14071414           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
    1408            flat_trace io_out io_in ge s' →
     1415           ∀t:flat_trace io_out io_in ge s'.
     1416           remainder_ok ge s' t →
    14091417           finite_prefix ge s
    14101418| fp_tac : ∀s,s'.
    14111419           trace_any_call (RTLabs_status ge) s s' →
    1412            flat_trace io_out io_in ge s' →
     1420           ∀t:flat_trace io_out io_in ge s'.
     1421           remainder_ok ge s' t →
    14131422           finite_prefix ge s
    14141423.
     
    14221431λge,s,s',OTHER,fp.
    14231432match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
    1424 [ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf
     1433[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
    14251434    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
    1426     rem
    1427 | fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf
    1428     (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem
     1435    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
    14291438].
    14301439
     
    14391448λge,s,s1,s',EVAL,CALL,fp.
    14401449match 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
    1441 [ fp_tal s' sf TAL rem ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
     1450[ fp_tal s' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
    14421451    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
    1443     rem
    1444 | fp_tac s' sf TAC rem ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf
     1452    rem rok
     1453| fp_tac s' sf TAC rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf
    14451454    (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
    1446     rem
     1455    rem rok
    14471456].
    14481457
     
    14621471let rec finite_segment ge s n trace
    14631472  (ORACLE: termination_oracle)
     1473  (TRACE_OK: remainder_ok ge s trace)
    14641474  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    1465   (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    1466   (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
    1467   (NOT_UNDEFINED: not_wrong … trace)
    14681475  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
    1469   (NOT_FINAL: RTLabs_is_final s = None ?)
    14701476  on n : finite_prefix ge s ≝
    14711477match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
    14721478[ O ⇒ λLABEL_LIMIT. ⊥
    14731479| S n' ⇒
    1474     match trace return λs,trace. not_wrong ??? s trace → well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → RTLabs_is_final s = None ? → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with
    1475     [ ft_stop st FINAL ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,NOT_FINAL,LABEL_LIMIT. ⊥
    1476     | ft_step start tr next EV trace' ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,NOT_FINAL,LABEL_LIMIT.
     1480    match trace return λs,trace. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with
     1481    [ ft_stop st FINAL ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
     1482    | ft_step start tr next EV trace' ⇒ λTRACE_OK,LABEL_LIMIT.
    14771483        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
    14781484        [ cl_other ⇒ λCL.
     1485            let TRACE_OK' ≝ ? in
    14791486            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
    14801487            [ true ⇒ λCS.
    1481                 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace'
     1488                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' TRACE_OK'
    14821489            | false ⇒ λCS.
    1483                 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ????? in
     1490                let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ? in
    14841491                fp_add_default ge ?? CL fs ? CS
    14851492            ] (refl ??)
    14861493        | cl_jump ⇒ λCL.
    1487             fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace'
     1494            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' ?
    14881495        | cl_call ⇒ λCL.
    14891496            match ORACLE ge O next trace' return λ_. finite_prefix ge start with
     
    14911498              match TERMINATES with [ witness TERMINATES ⇒
    14921499                let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
     1500                let TRACE_OK' ≝ ? in
    14931501                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
    1494                 [ 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)
     1502                [ 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'
    14951503                | false ⇒ λCS.
    1496                     let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE ENV_COSTLABELLED ????? in
     1504                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ? in
    14971505                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
    14981506                ] (refl ??)
    14991507              ]
    15001508            | or_intror NO_TERMINATION ⇒
    1501                 fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace')
     1509                fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace') ?
    15021510            ]
    15031511        | cl_return ⇒ λCL. ⊥
    15041512        ] (refl ??)
    1505     | ft_wrong start m EV ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,NOT_FINAL,LABEL_LIMIT. ⊥
    1506     ] NOT_UNDEFINED STATE_COSTLABELLED NO_TERMINATION NOT_FINAL
     1513    | ft_wrong start m EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
     1514    ] TRACE_OK
    15071515] LABEL_LIMIT.
    15081516[ cases (state_bound_on_steps_to_cost_zero s) /2/
    1509 | @(absurd …  NOT_FINAL FINAL)
    1510 | @(absurd ?? NO_TERMINATION)
     1517| @(absurd …  (ro_not_final … TRACE_OK) FINAL)
     1518| @(absurd ?? (ro_no_termination … TRACE_OK))
    15111519     %{0} % @wr_base //
    1512 | @(well_cost_labelled_jump … EV) //
    1513 | 5,6,7,8,9,10: /2/
     1520| @(well_cost_labelled_jump … EV) /2/
     1521| 5,6,8,9,10,11: /3/
     1522| % [ @(well_cost_labelled_state_step … EV) /2/
     1523    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
     1524    | @(still_not_wrong … EV) /2/
     1525    | @(not_return_to_not_final … EV) >CL % #E destruct
     1526    ]
    15141527| /2/
    1515 | //
    1516 | @(not_to_not … NO_TERMINATION) * #depth * #TM1 %{depth} %
    1517   @wr_call //
    1518   @(will_return_prepend … TERMINATES … TM1)
    1519   cases (terminates … tlr) //
    1520 | @(will_return_not_wrong … TERMINATES)
    1521   [ @(still_not_wrong … EV) //
    1522   | cases (terminates … tlr) //
    1523   ]
    15241528| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
    15251529  @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
    1526 | (* By stack preservation we cannot be in the final state *)
    1527   inversion (stack_ok … tlr)
    1528   [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
    1529   | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
    1530   | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct
    1531     cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
    1532     inversion (eval_perserves … EV)
    1533     [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 -NOT_UNDEFINED -NO_TERMINATION destruct ]
    1534     #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -NOT_UNDEFINED -NO_TERMINATION destruct
    1535     inversion S
    1536     [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
    1537     (* state_bound_on_steps_to_cost needs to know about the current stack frame,
    1538        so we can use it as a witness that at least one frame exists *)
    1539     inversion LABEL_LIMIT
    1540     #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct
    1541   | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct
    1542   ]
    1543 | @(well_cost_labelled_state_step … EV) //
    1544 | @(well_cost_labelled_call … EV) //
    1545 | 19,20,21: /2/
    1546 | @(well_cost_labelled_state_step … EV) //
    1547 | @(not_to_not … NO_TERMINATION)
    1548   * #depth * #TERM %{depth} % @wr_step /2/
    1549 | @(still_not_wrong … NOT_UNDEFINED)
     1530| % [ /2/
     1531    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
     1532      @wr_call //
     1533      @(will_return_prepend … TERMINATES … TM1)
     1534      cases (terminates … tlr) //
     1535    | @(will_return_not_wrong … TERMINATES)
     1536      [ @(still_not_wrong … EV) /2/
     1537      | cases (terminates … tlr) //
     1538      ]
     1539    | (* By stack preservation we cannot be in the final state *)
     1540      inversion (stack_ok … tlr)
     1541      [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
     1542      | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
     1543      | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct
     1544        cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
     1545        inversion (eval_perserves … EV)
     1546        [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 -TRACE_OK destruct ]
     1547        #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
     1548        inversion S
     1549        [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
     1550        (* state_bound_on_steps_to_cost needs to know about the current stack frame,
     1551           so we can use it as a witness that at least one frame exists *)
     1552        inversion LABEL_LIMIT
     1553        #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct
     1554      | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct
     1555      ]
     1556    ]
     1557| @(well_cost_labelled_state_step … EV) /2/
     1558| @(well_cost_labelled_call … EV) /2/
     1559| % /2/
     1560| 18,19,20: /2/
    15501561| cases (bound_after_step … LABEL_LIMIT EV ?)
    1551   [ * [ #TERMINATES @⊥ @(absurd ?? NO_TERMINATION) %{0} % @wr_step [ %1 // |
     1562  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
    15521563    inversion trace'
    1553     [ #s0 #FINAL #E1 #E2 destruct @⊥
     1564    [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
    15541565      @(absurd ?? FINAL) @(not_return_to_not_final … EV)
    15551566      % >CL #E destruct
    1556     | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 destruct
     1567    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
    15571568      @wr_base //
    1558     | #H99 #H100 #H101 #H102 #H103 destruct
    1559       inversion NOT_UNDEFINED
     1569    | #H99 #H100 #H101 #H102 #H103 -TRACE_OK' destruct
     1570      inversion (ro_not_undefined … TRACE_OK)
    15601571      [ #H137 #H138 #H139 #H140 #H141 destruct
    15611572      | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 destruct
     
    15721583  | //
    15731584  ]
    1574 | @(not_return_to_not_final … EV) >CL % #E destruct
    1575 | inversion NOT_UNDEFINED
     1585| % [ @(well_cost_labelled_state_step … EV) /2/
     1586    | @(not_to_not … (ro_no_termination … TRACE_OK))
     1587      * #depth * #TERM %{depth} % @wr_step /2/
     1588    | @(still_not_wrong … (ro_not_undefined … TRACE_OK))
     1589    | @(not_return_to_not_final … EV) >CL % #E destruct
     1590    ]
     1591| inversion (ro_not_undefined … TRACE_OK)
    15761592  [ #H169 #H170 #H171 #H172 #H173 destruct
    15771593  | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
     
    16071623  (trace: flat_trace io_out io_in ge s)
    16081624  (ORACLE: termination_oracle)
     1625  (TRACE_OK: remainder_ok ge s trace)
    16091626  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    16101627  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
    1611   (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    16121628  (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)
    16131629  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    1614   (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
    1615   (NOT_UNDEFINED: not_wrong … trace)
    1616   (NOT_FINAL: RTLabs_is_final s = None ?)
    16171630  : ∃T:trace_label_diverges (RTLabs_status ge) s. True ≝
    16181631match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with
    16191632[ ex_intro n B ⇒
    1620     match finite_segment ge s n trace ORACLE ENV_COSTLABELLED STATE_COSTLABELLED NO_TERMINATION NOT_UNDEFINED B NOT_FINAL
     1633    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED B
    16211634      return λs.λ_. RTLabs_cost s = true → ∃T:trace_label_diverges (RTLabs_status ge) s. True
    16221635    with
    1623     [ fp_tal s s' T t ⇒ λSTATEMENT_COSTLABEL.
    1624         match make_label_diverges ge s' t ORACLE ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?????? with
     1636    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
     1637        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
    16251638        [ ex_intro T' _ ⇒
    16261639            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
    16271640        ]
    1628     | fp_tac s s' T t ⇒ λSTATEMENT_COSTLABEL.
    1629         match t return λs',t. trace_any_call ? s s' → ∃T:trace_label_diverges (RTLabs_status ge) s. True
     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
    16301643        with
    1631         [ ft_step s' tr next EV t' ⇒ λT.
    1632             match make_label_diverges ge next t' ORACLE ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?????? 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
    16331646            [ ex_intro T' _ ⇒
    16341647                ex_intro ?? (tld_base (RTLabs_status ge) s s' next (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
    16351648            ]
    16361649        | _ ⇒ λT. ⊥
    1637         ] T
     1650        ] T tOK
    16381651    ] STATEMENT_COSTLABEL
    16391652].
     1653[
Note: See TracChangeset for help on using the changeset viewer.