Changeset 3021


Ignore:
Timestamp:
Mar 28, 2013, 7:11:09 PM (4 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.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2588 r3021  
    5656  λp. Σl. in_clight_program p l.
    5757
     58(* Providing these proofs isn't easy, and doesn't seem to have any benefit, so
     59   let's stick with a simpler form.
    5860definition clight_cost_map ≝
    5961  λp. (in_clight_label p) → ℕ.
     62*)
     63
     64definition clight_cost_map ≝ costlabel → ℕ.
    6065
    6166definition clight_label_free : clight_program → bool ≝
  • src/compiler.ma

    r3018 r3021  
    128128include "ASM/ASMCosts.ma".
    129129
     130definition lift_out_of_sigma :
     131  ∀A,B : Type[0].∀P_out : A → Prop.B →
     132    (∀a.P_out a + ¬ P_out a) →
     133  ((Σa.P_out a) → B) → A → B ≝ λA,B,P_out,dflt,dec,m,a_sig.
     134   match dec a_sig with
     135   [ inl prf ⇒ m «a_sig, prf»
     136   | inr _ ⇒ dflt (* labels not present in out code get 0 *)
     137   ].
     138
    130139definition lift_cost_map_back_to_front :
    131   ∀clight, oc.
     140  ∀oc.
    132141    let abstat ≝ OC_abstract_status oc in
    133   as_cost_map abstat → clight_cost_map clight
    134   λclight,oc,k,asm_cost_map.
    135   lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
    136     (strong_decidable_in_codomain …) k asm_cost_map.
     142  as_cost_map abstat → clight_cost_map
     143  λoc,asm_cost_map.
     144  lift_out_of_sigma … 0 (* labels not present in out code get 0 *)
     145    (strong_decidable_in_codomain …) asm_cost_map.
    137146
    138147(* Cost model computation *)
     
    144153 ; c_max_stack: nat
    145154 ; c_labelled_clight: clight_program
    146  ; c_clight_cost_map: clight_cost_map c_labelled_clight
     155 ; c_clight_cost_map: clight_cost_map
    147156 }.
    148157
     
    154163  let k ≝ ASM_cost_map p in
    155164  let k' ≝
    156    lift_cost_map_back_to_front p' p k in
     165   lift_cost_map_back_to_front p k in
    157166  return mk_compiler_output p stack_cost max_stack p' k'.
  • 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.