Changeset 1670


Ignore:
Timestamp:
Feb 1, 2012, 4:16:04 PM (6 years ago)
Author:
campbell
Message:

Snapshot of non-terminating RTLabs structured traces work.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1656 r1670  
    5454  normalize try #a try #b try #c try #d try #e try #g try #h destruct
    5555] qed.
     56
     57lemma RTLabs_not_cost : ∀ge,s.
     58  RTLabs_cost s = false →
     59  ¬ as_costed (RTLabs_status ge) s.
     60#ge #s #E % whd in ⊢ (% → ?); >E #E' destruct
     61qed.
    5662
    5763(* Before attempting to construct a structured trace, let's show that we can
     
    580586              doesnt_end_with_ret
    581587              (mk_trace_result ge ??? next trace' ?
    582                 (tal_base_not_return (RTLabs_status ge) start next ???) ?)
     588                (tal_base_not_return (RTLabs_status ge) start next ?? CS) ?)
    583589        (* An ordinary step, keep going. *)
    584590        | false ⇒ λCS.
     
    586592                replace_sub_trace … r
    587593                  (tal_step_default (RTLabs_status ge) (ends … r)
    588                      start next (new_state … r) ? (new_trace … r) ??)
     594                     start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS))
    589595        ] (refl ??)
    590596       
     
    613619              (tal_step_call (RTLabs_status ge) (ends … r')
    614620                start next (new_state … r) (new_state … r') ? CL ?
    615                 (new_trace … r) ? (new_trace … r'))
     621                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r'))
    616622        ] (refl ??)
    617623
     
    664670  cases (will_return_call … CL TERMINATES)
    665671  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
    666 | whd in ⊢ (?%); >CS % #E destruct
    667672| (* TODO oh dear *)
    668673| %{tr} @EV
     
    687692| %{tr} @EV
    688693| %2 whd @CL
    689 | @CS
    690694| @(well_cost_labelled_state_step  … EV) //
    691695| cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
    692 | % whd in ⊢ (% → ?); >CS #E destruct
    693696| @CL
    694697| %{tr} @EV
     
    770773   use the fact that the trace is soundly labelled to achieve this. *)
    771774
    772 inductive finite_prefix (ge:genv) : state → Type[0]
     775inductive finite_prefix (ge:genv) : state → Prop
    773776| fp_tal : ∀s,s'.
    774777           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
     
    790793match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
    791794[ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf
    792     (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER ?)
     795    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
    793796    rem
    794797| fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf
    795     (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER ?) rem
     798    (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem
    796799].
    797 % whd in ⊢ (% → ?); >NOT_COST #E destruct
    798 qed.
    799 (* I'll come back to this.
     800
    800801definition fp_add_terminating_call : ∀ge,s,s1,s'.
    801802  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
     
    804805  trace_label_return (RTLabs_status ge) s1 s' →
    805806  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' →
     807  RTLabs_cost s' = false →
    806808  finite_prefix ge s ≝
    807809λge,s,s1,s',EVAL,CALL,fp.
    808 match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → finite_prefix ge s with
    809 [ fp_tal s' sf TAL rem ⇒ λTLR,RET. fp_tal ge s sf
    810     (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR TAL)
     810match 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
     811[ fp_tal s' sf TAL rem ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
     812    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
    811813    rem
    812 | fp_tac s' sf TAC rem ⇒ λTLR,RET. fp_tac ge s sf
    813     (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR TAC)
     814| fp_tac s' sf TAC rem ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf
     815    (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
    814816    rem
    815817].
    816 *)
     818
     819definition termination_oracle ≝ ∀ge,depth,s,trace.
     820  inhabited (will_return ge depth s trace) ⊎ ¬ inhabited (will_return ge depth s trace).
     821
     822let rec finite_segment ge s n trace
     823  (ORACLE: termination_oracle)
     824  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     825  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
     826  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
     827  (LABEL_LIMIT: ∃s'. And (nth_state ge s trace (S n) = Some ? s') (RTLabs_cost s' = true))
     828  : finite_prefix ge s ≝
     829match n return λn. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S n) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
     830[ O ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ?
     831| S n' ⇒
     832    match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S (S n')) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
     833    [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
     834    | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT.
     835        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
     836        [ cl_other ⇒ λCL.
     837            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
     838            [ true ⇒ λCS.
     839                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace'
     840            | false ⇒ λCS.
     841                let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ?? LABEL_LIMIT in
     842                fp_add_default ge ?? CL fs ? CS
     843            ] (refl ??)
     844        | cl_jump ⇒ λCL.
     845            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace'
     846        | cl_call ⇒ λCL.
     847            match ORACLE ge O next trace' with
     848            [ inl TERMINATES ⇒
     849                let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ??? in
     850                ?
     851            | inr NO_TERMINATION ⇒ ?
     852            ]
     853        | cl_return ⇒ λCL. ⊥
     854        ] (refl ??)
     855    | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
     856    ]
     857] STATE_COSTLABELLED NO_TERMINATION LABEL_LIMIT.
     858[ 2,17: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct
     859| 3: @(absurd ?? NO_TERMINATION)
     860     %{0} % @wr_base //
     861| 4: @(well_cost_labelled_jump … EV) //
     862| 5,6: /2/
     863| 8: @(well_cost_labelled_state_step … EV) //
     864| 9: @(well_cost_labelled_call … EV) //
     865| 10: cases TERMINATES //
     866| 12,13,14: /2/
     867| 15: @(well_cost_labelled_state_step … EV) //
     868| 16: @(not_to_not … NO_TERMINATION)
     869     * #depth * #TERM %{depth} % @wr_step /2/
     870] cases daemon qed.
     871
    817872(*
    818873let corec make_label_diverges ge s
Note: See TracChangeset for help on using the changeset viewer.