Changeset 1765


Ignore:
Timestamp:
Feb 27, 2012, 2:16:54 PM (8 years ago)
Author:
campbell
Message:

Rule out final states in non-terminating executions chunks (RTLabs
structured trace).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1764 r1765  
    14471447].
    14481448
     1449lemma not_return_to_not_final : ∀ge,s,tr,s'.
     1450  eval_statement ge s = Value ??? 〈tr, s'〉 →
     1451  RTLabs_classify s ≠ cl_return →
     1452  RTLabs_is_final s' = None ?.
     1453#ge #s #tr #s' #EV
     1454inversion (eval_perserves … EV) //
     1455#H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
     1456@⊥ @(absurd ?? CL) @refl
     1457qed.
     1458
    14491459definition termination_oracle ≝ ∀ge,depth,s,trace.
    14501460  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
     
    14571467  (NOT_UNDEFINED: not_wrong … trace)
    14581468  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
     1469  (NOT_FINAL: RTLabs_is_final s = None ?)
    14591470  on n : finite_prefix ge s ≝
    14601471match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
    14611472[ O ⇒ λLABEL_LIMIT. ⊥
    14621473| S n' ⇒
    1463     match trace return λs,trace. not_wrong ??? s trace → well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with
    1464     [ ft_stop st FINAL ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
    1465     | ft_step start tr next EV trace' ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT.
     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.
    14661477        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
    14671478        [ cl_other ⇒ λCL.
     
    14701481                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace'
    14711482            | false ⇒ λCS.
    1472                 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ???? in
     1483                let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ????? in
    14731484                fp_add_default ge ?? CL fs ? CS
    14741485            ] (refl ??)
     
    14831494                [ 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)
    14841495                | false ⇒ λCS.
    1485                     let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE ENV_COSTLABELLED ???? in
     1496                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE ENV_COSTLABELLED ????? in
    14861497                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
    14871498                ] (refl ??)
     
    14921503        | cl_return ⇒ λCL. ⊥
    14931504        ] (refl ??)
    1494     | ft_wrong start m EV ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
    1495     ] NOT_UNDEFINED STATE_COSTLABELLED NO_TERMINATION
     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
    14961507] LABEL_LIMIT.
    14971508[ cases (state_bound_on_steps_to_cost_zero s) /2/
    1498 | (* TODO: how do we know that we're not at the final state? *)
     1509| @(absurd …  NOT_FINAL FINAL)
    14991510| @(absurd ?? NO_TERMINATION)
    15001511     %{0} % @wr_base //
     
    15131524| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
    15141525  @(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 #H130 #H131 #H133 #H134 #H135 #H136 #H137 #H138 #H139 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  ]
    15151543| @(well_cost_labelled_state_step … EV) //
    15161544| @(well_cost_labelled_call … EV) //
    1517 | 18,19,20: /2/
     1545| 19,20,21: /2/
    15181546| @(well_cost_labelled_state_step … EV) //
    15191547| @(not_to_not … NO_TERMINATION)
     
    15231551  [ * [ #TERMINATES @⊥ @(absurd ?? NO_TERMINATION) %{0} % @wr_step [ %1 // |
    15241552    inversion trace'
    1525     [ cases daemon (* TODO again *) | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 destruct
    1526     @wr_base //
     1553    [ #s0 #FINAL #E1 #E2 destruct @⊥
     1554      @(absurd ?? FINAL) @(not_return_to_not_final … EV)
     1555      % >CL #E destruct
     1556    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 destruct
     1557      @wr_base //
    15271558    | #H99 #H100 #H101 #H102 #H103 destruct
    15281559      inversion NOT_UNDEFINED
     
    15411572  | //
    15421573  ]
     1574| @(not_return_to_not_final … EV) >CL % #E destruct
    15431575| inversion NOT_UNDEFINED
    15441576  [ #H169 #H170 #H171 #H172 #H173 destruct
    15451577  | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
    15461578  ]
    1547 ] cases daemon qed.
     1579] qed.
    15481580
    15491581(*
Note: See TracChangeset for help on using the changeset viewer.