Changeset 1784


Ignore:
Timestamp:
Feb 27, 2012, 5:55:33 PM (7 years ago)
Author:
campbell
Message:

Start on proof of existence of nonterminating RTLabs structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1782 r1784  
    15791579] qed.
    15801580
    1581 (*
     1581definition soundly_labelled_fn : internal_function → Prop ≝
     1582λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
     1583
     1584definition soundly_labelled_ge : genv → Prop ≝
     1585λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
     1586
     1587definition soundly_labelled_state : state → Prop ≝
     1588λs. match s with
     1589[ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
     1590| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
     1591                          All ? (λf. soundly_labelled_fn (func f)) fs
     1592| Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
     1593| Finalstate _ ⇒ True
     1594].
     1595
     1596lemma steps_from_sound : ∀s.
     1597  RTLabs_cost s = true →
     1598  soundly_labelled_state s →
     1599  ∃n. state_bound_on_steps_to_cost s n.
     1600* [ #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 ]
     1601whd in ⊢ (% → ?); * #SLF #_
     1602cases (SLF (next f) (next_ok f)) #n #B1
     1603%{n} % @B1
     1604qed.
     1605
    15821606let corec make_label_diverges ge s
    15831607  (trace: flat_trace io_out io_in ge s)
     1608  (ORACLE: termination_oracle)
    15841609  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     1610  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
    15851611  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
     1612  (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)
    15861613  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    1587   (SOUNDLY_COSTLABELLED: soundly_labelled_trace … trace)
    15881614  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
    1589   : trace_label_diverges (RTLabs_status ge) s ≝ ?
    1590 .
    1591 *)
     1615  (NOT_UNDEFINED: not_wrong … trace)
     1616  (NOT_FINAL: RTLabs_is_final s = None ?)
     1617  : ∃T:trace_label_diverges (RTLabs_status ge) s. True ≝
     1618match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with
     1619[ ex_intro n B ⇒
     1620    match finite_segment ge s n trace ORACLE ENV_COSTLABELLED STATE_COSTLABELLED NO_TERMINATION NOT_UNDEFINED B NOT_FINAL
     1621      return λs.λ_. RTLabs_cost s = true → ∃T:trace_label_diverges (RTLabs_status ge) s. True
     1622    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
     1625        [ ex_intro T' _ ⇒
     1626            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
     1627        ]
     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
     1630        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
     1633            [ ex_intro T' _ ⇒
     1634                ex_intro ?? (tld_base (RTLabs_status ge) s s' next (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
     1635            ]
     1636        | _ ⇒ λT. ⊥
     1637        ] T
     1638    ] STATEMENT_COSTLABEL
     1639].
Note: See TracChangeset for help on using the changeset viewer.