Changeset 2722 for src/correctness.ma


Ignore:
Timestamp:
Feb 23, 2013, 5:05:03 PM (7 years ago)
Author:
campbell
Message:

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2677 r2722  
    4747definition stack_cost_T ≝ ident → nat.
    4848
    49 (* Again, in principle we can use the fact that the state must be a call and
    50    also show some relevant invariants about call states, but we go with the
    51    easier option of returning zero elsewhere. *)
    52 definition Clight_stack_cost :
    53   stack_cost_T →
     49definition Clight_stack_ident :
    5450  cl_genv →
    5551  ∀s:Clight_state.
    5652  match Clight_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
    57   nat ≝
    58 λcost,ge,s,H.
    59 match s with
    60 [ Callstate v _ _ _ _ ⇒
    61   match v with [ Vptr p ⇒ match symbol_for_block … ge (pblock p) with [ Some id ⇒ cost id | _ ⇒ 0 ] | _ ⇒ 0 ]
    62 | _ ⇒ 0
     53  ident ≝
     54λge,s.
     55match s return λs. match Clight_classify s with [ cl_call ⇒ True | _ ⇒ False ] → ident with
     56[ Callstate id _ _ _ _ ⇒ λ_. id
     57| _ ⇒ λH.⊥
    6358].
     59@H
     60qed.
    6461
    6562definition Clight_pcs : preclassified_system ≝
     
    6865  (λ_.Clight_labelled)
    6966  (λ_.Clight_classify)
    70   Clight_stack_cost.
     67  Clight_stack_ident.
    7168
    7269(* From measurable on Clight, we will end up with an RTLabs flat trace where
     
    8077 *)
    8178
    82 axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).
     79axiom observables_8051 : object_code → nat → nat → res ((list intensional_event) × (list intensional_event)).
    8380
    8481definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
     
    132129  ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound →
    133130  ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 →
    134   ∃n1,n2. observables clight_fullexec labelled m1 m2 = observables_8051 object_code n1 n2 ∧
     131  ∃n1,n2. observables Clight_pcs labelled m1 m2 = observables_8051 object_code n1 n2 ∧
    135132          c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
    136133
Note: See TracChangeset for help on using the changeset viewer.