Changeset 2399 for src/correctness.ma


Ignore:
Timestamp:
Oct 17, 2012, 6:45:20 PM (8 years ago)
Author:
campbell
Message:

Fill in some details about the statement of correctness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2325 r2399  
    1212 
    1313  ∀object_code,costlabel_map,labelled,cost_map.
    14   compile input_program = OK ? 〈〈object_code,costlabel_map〉,labelled,cost_map〉 →
     14  compile input_program = OK ? 〈〈object_code,costlabel_map〉,❬labelled,cost_map❭〉 →
    1515
    1616  not_wrong … (exec_inf … clight_fullexec input_program) →
     
    4141
    4242definition execution_prefix : Type[0] ≝ list (trace × Clight_state).
    43 axiom split_trace : execution Clight_state io_out io_in → nat → option (execution_prefix × (execution Clight_state io_out io_in)).
    44 axiom stack_after : execution_prefix → nat.
     43let rec split_trace (x:execution Clight_state io_out io_in) (n:nat) on n : option (execution_prefix × (execution Clight_state io_out io_in)) ≝
     44match n with
     45[ O ⇒ Some ? 〈[ ], x〉
     46| S n' ⇒
     47  match x with
     48  [ e_step tr s x' ⇒
     49    ! 〈pre,x''〉 ← split_trace x' n';
     50    Some ? 〈〈tr,s〉::pre,x''〉
     51  | _ ⇒ None ?
     52  ]
     53].
     54
     55definition trace_labelled : execution_prefix → Prop ≝
     56λx. ∃tr1,s1,x',tr2,s2. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉]) ∧ bool_to_Prop (Clight_labelled s1) ∧ bool_to_Prop (Clight_labelled s2).
     57
     58definition measure_stack : Clight_stack_T → execution_prefix → nat × nat ≝
     59λstack_cost.
     60  foldl … (λx, trs.
     61    let 〈current,max_stack〉 ≝ x in
     62    let 〈tr,s〉 ≝ trs in
     63    let new ≝
     64      match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
     65      [ cl_call ⇒ λsc. current + sc I
     66      | cl_return ⇒ λsc. current - sc I
     67      | _ ⇒ λ_. current
     68      ] (stack_cost s) in
     69    〈new, max max_stack new〉) 〈0,0〉.
     70
     71definition stack_after : Clight_stack_T → execution_prefix → nat ≝
     72λsc,x. \fst (measure_stack sc x).
     73
     74definition max_stack :  Clight_stack_T → execution_prefix → nat ≝
     75λsc,x. \snd (measure_stack sc x).
    4576
    4677(* TODO: cost labels *)
     
    72103  split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧
    73104  split_trace suffix n = Some ? 〈interesting,remainder〉 ∧
    74   will_return' stack_cost (stack_after prefix) interesting = Some ? max_stack ∧
     105  trace_labelled interesting →
     106  will_return' stack_cost (stack_after stack_cost prefix) interesting = Some ? max_stack ∧
    75107  max_stack < max_allowed_stack.
    76108
     
    85117 *)
    86118
    87 axiom observables : clight_program → nat → nat → option ((list trace) × (list trace)).
     119definition observables : clight_program → nat → nat → option ((list trace) × (list trace)) ≝
     120λp,m,n.
     121  let cl_trace ≝ exec_inf … clight_fullexec p in
     122  match split_trace cl_trace m with
     123  [ Some x ⇒
     124    let 〈prefix,suffix〉 ≝ x in
     125    match split_trace suffix n with
     126    [ Some y ⇒
     127      let interesting ≝ \fst y in
     128      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
     129    | _ ⇒ None ?
     130    ]
     131  | _ ⇒ None ?
     132  ].
     133
    88134axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).
    89 axiom clight_clock_after : clight_program → nat → option nat.
     135
     136definition in_execution_prefix : execution_prefix → costlabel → Prop ≝
     137λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.
     138
     139let rec foldl_exists_aux (A,B:Type[0]) (l,l':list B) (f:A → ∀b:B. Exists … (λx.x=b) l → A) (a:A) on l' : (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A ≝
     140match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with
     141[ nil ⇒ λ_. a
     142| cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ?
     143].
     144[ %1 %
     145| #b #H' @H %2 @H'
     146] qed.
     147
     148definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝
     149λA,B,l,f,a.  foldl_exists_aux A B l l f a (λb,H. H).
     150
     151lemma Exists_lift : ∀A,P,Q,l.
     152  (∀x. P x → Q x) →
     153  Exists A P l →
     154  Exists A Q l.
     155#A #P #Q #l elim l
     156[ //
     157| #h #t #IH #H * [ #H' %1 @H @H' | #H' %2 @IH /2/ ]
     158] qed.
     159
     160definition measure_clock : ∀x:execution_prefix. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝
     161λx,costmap. foldl_exists … x
     162 (λclock,trs,H.
     163    foldl_exists … (\fst trs) (λclock,ev. match ev return λev. Exists … (λx. x=ev) ? → nat with [ EVcost l ⇒ λH'. clock + costmap «l,?» | _ ⇒ λ_. clock ]) clock)
     164 0.
     165whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E
     166qed.
     167
     168definition clight_clock_after : ∀p:clight_program. nat → ((Σl:costlabel.in_clight_program p l)→ℕ) → option nat ≝
     169λp,n,costmap.
     170  let x ≝ exec_inf … clight_fullexec p in
     171  match split_trace x n with
     172  [ Some traces ⇒
     173    Some ? (measure_clock (\fst traces) (λl.costmap «l,?»))
     174  | None ⇒ None ?
     175  ].
     176cases daemon
     177qed.
     178
    90179axiom initial_8051_status : ∀oc. Status oc.
    91180
    92181definition simulates ≝
    93   λstack_cost, stack_bound, labelled, object_code.
     182  λstack_cost, stack_bound, labelled, object_code, cost_map.
    94183  let initial_status ≝ initial_8051_status (load_code_memory object_code) in
    95184  ∀m1,m2. measurable labelled m1 m2 stack_cost stack_bound →
    96   ∀c1,c2. clight_clock_after labelled m1 = Some ? c1 → clight_clock_after labelled m2 = Some ? c2 →
     185  ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 →
    97186  ∃n1,n2. observables labelled m1 m2 = observables_8051 object_code n1 n2 ∧
    98187          c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
    99188
    100 axiom compile' : clight_program → res (object_code × costlabel_map × clight_program
    101  × ((Σl:costlabel.in_clight_program l)→ℕ) × Clight_stack_T × nat).
     189axiom compile' : clight_program → res (object_code × costlabel_map ×
     190  (𝚺labelled:clight_program. ((Σl:costlabel.in_clight_program labelled l)→ℕ)) × Clight_stack_T × nat).
    102191
    103192theorem correct' :
     
    107196 
    108197  ∀object_code,costlabel_map,labelled,cost_map,stack_cost,stack_bound.
    109   compile' input_program = OK ? 〈〈〈〈object_code,costlabel_map〉,labelled〉,cost_map〉,stack_cost,stack_bound〉 →
     198  compile' input_program = OK ? 〈〈〈object_code,costlabel_map〉,❬labelled,cost_map❭〉,stack_cost,stack_bound〉 →
    110199 
    111200  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
    112201  ∧
    113202
    114   simulates stack_cost stack_bound labelled object_code.
     203  simulates stack_cost stack_bound labelled object_code cost_map.
    115204 
    116205
Note: See TracChangeset for help on using the changeset viewer.