Changeset 3021 for src/correctness.ma


Ignore:
Timestamp:
Mar 28, 2013, 7:11:09 PM (7 years ago)
Author:
campbell
Message:

Replace clight_clock_after with a more sensible definition that uses
an intensional trace. Also drop the proof argument for the clight cost
map to avoid proving that costs come from the clight program - it doesn't
seem to give us much of a benefit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r3003 r3021  
    7272] qed.
    7373
    74 definition measure_clock : ∀x:execution_prefix Clight_state. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝
    75 λx,costmap. foldl_exists … x
    76  (λclock,trs,H.
    77     foldl_exists … (\fst trs) (λclock,ev. match ev return λev. Exists … (λx. x=ev) ? → nat with [ EVcost l ⇒ λH'. clock + costmap «l,?» | _ ⇒ λ_. clock ]) clock)
    78  0.
    79 whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E
    80 qed.
    81 
    82 definition clight_clock_after : ∀p:clight_program. nat → ((Σl:costlabel.in_clight_program p l)→ℕ) → option nat ≝
     74include "RTLabs/MeasurableToStructured.ma".
     75
     76definition clight_clock_after : ∀p:clight_program. nat → (costlabel→ℕ) → res nat ≝
    8377λp,n,costmap.
    84   let x ≝ exec_inf … clight_fullexec p in
    85   match split_trace … x n with
    86   [ Some traces ⇒
    87     Some ? (measure_clock (\fst traces) (λl.costmap «l,?»))
    88   | None ⇒ None ?
    89   ].
    90 cases daemon
    91 qed.
     78  ! 〈s,itrace〉 ← exec_steps_with_obs Clight_pcs p n;
     79  let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl | _ ⇒ None ? ]) itrace in
     80  return Σ_{l ∈ ctrace}(costmap l).
    9281
    9382include "common/AssocList.ma".
     
    10493    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
    10594  ∀c1,c2.
    106    clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = Some ? c1 →
    107    clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = Some ? c2 →
     95   clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
     96   clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = OK … c2 →
    10897  ∃n1,n2.
    10998   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
Note: See TracChangeset for help on using the changeset viewer.