Changeset 2399


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

Fill in some details about the statement of correctness.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2392 r2399  
    11include "Clight/Csyntax.ma".
    22
    3 (* Label freedom *)
    4 
    5 let rec expr_label_free (e:expr) : bool ≝
     3(* Extract cost labels from a program. *)
     4
     5let rec labels_of_expr (e:expr) : list costlabel ≝
    66match e with
    77[ Expr e' _ ⇒
    88  match e' with
    9   [ Ederef e1 ⇒ expr_label_free e1
    10   | Eaddrof e1 ⇒ expr_label_free e1
    11   | Eunop _ e1 ⇒ expr_label_free e1
    12   | Ebinop _ e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
    13   | Ecast _ e1 ⇒ expr_label_free e1
    14   | Econdition e1 e2 e3 ⇒ expr_label_free e1 ∧ expr_label_free e2 ∧ expr_label_free e3
    15   | Eandbool e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
    16   | Eorbool e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
    17   | Efield e1 _ ⇒ expr_label_free e1
    18   | Ecost _ _ ⇒ false
    19   | _ ⇒ true
     9  [ Ederef e1 ⇒ labels_of_expr e1
     10  | Eaddrof e1 ⇒ labels_of_expr e1
     11  | Eunop _ e1 ⇒ labels_of_expr e1
     12  | Ebinop _ e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
     13  | Ecast _ e1 ⇒ labels_of_expr e1
     14  | Econdition e1 e2 e3 ⇒ labels_of_expr e1 @ labels_of_expr e2 @ labels_of_expr e3
     15  | Eandbool e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
     16  | Eorbool e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
     17  | Efield e1 _ ⇒ labels_of_expr e1
     18  | Ecost cl e1 ⇒ cl::(labels_of_expr e1)
     19  | _ ⇒ [ ]
    2020  ]
    2121].
    2222
    23 let rec statement_label_free (s:statement) : bool ≝
     23let rec labels_of_statement (s:statement) : list costlabel ≝
    2424match s with
    25 [ Sassign e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
    26 | Scall oe e1 es ⇒ option_map_def … expr_label_free true oe ∧ expr_label_free e1 ∧ all … expr_label_free es
    27 | Ssequence s1 s2 ⇒ statement_label_free s1 ∧ statement_label_free s2
    28 | Sifthenelse e1 s1 s2 ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ statement_label_free s2
    29 | Swhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_free s1
    30 | Sdowhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_free s1
    31 | Sfor s1 e1 s2 s3 ⇒ statement_label_free s1 ∧ expr_label_free e1 ∧ statement_label_free s2 ∧ statement_label_free s3
    32 | Sreturn oe ⇒ option_map_def … expr_label_free true oe
    33 | Sswitch e1 ls ⇒ expr_label_free e1 ∧ labeled_statements_label_free ls
    34 | Slabel _ s1 ⇒ statement_label_free s1
    35 | Scost _ _ ⇒ false
    36 | _ ⇒ true
    37 ] and labeled_statements_label_free (ls:labeled_statements) : bool ≝
     25[ Sassign e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
     26| Scall oe e1 es ⇒ option_map_def … labels_of_expr [ ] oe @ labels_of_expr e1 @ foldl … (λls,e. labels_of_expr e @ ls) [ ] es
     27| Ssequence s1 s2 ⇒ labels_of_statement s1 @ labels_of_statement s2
     28| Sifthenelse e1 s1 s2 ⇒ labels_of_expr e1 @ labels_of_statement s1 @ labels_of_statement s2
     29| Swhile e1 s1 ⇒ labels_of_expr e1 @ labels_of_statement s1
     30| Sdowhile e1 s1 ⇒ labels_of_expr e1 @ labels_of_statement s1
     31| Sfor s1 e1 s2 s3 ⇒ labels_of_statement s1 @ labels_of_expr e1 @ labels_of_statement s2 @ labels_of_statement s3
     32| Sreturn oe ⇒ option_map_def … labels_of_expr [ ] oe
     33| Sswitch e1 ls ⇒ labels_of_expr e1 @ labels_of_labeled_statements ls
     34| Slabel _ s1 ⇒ labels_of_statement s1
     35| Scost cl s1 ⇒ cl::(labels_of_statement s1)
     36| _ ⇒ [ ]
     37] and labels_of_labeled_statements (ls:labeled_statements) : list costlabel ≝
    3838match ls with
    39 [ LSdefault s1 ⇒ statement_label_free s1
    40 | LScase _ _ s1 ls1 ⇒ statement_label_free s1 ∧ labeled_statements_label_free ls1
    41 ].
    42 
    43 definition clight_fundef_label_free : ident × clight_fundef → bool ≝
     39[ LSdefault s1 ⇒ labels_of_statement s1
     40| LScase _ _ s1 ls1 ⇒ labels_of_statement s1 @ labels_of_labeled_statements ls1
     41].
     42
     43definition labels_of_clight_fundef : ident × clight_fundef → list costlabel ≝
    4444λifd. match \snd ifd with
    45 [ CL_Internal f ⇒ statement_label_free (fn_body f)
    46 | _ ⇒ true
    47 ].
     45[ CL_Internal f ⇒ labels_of_statement (fn_body f)
     46| _ ⇒ [ ]
     47].
     48
     49definition labels_of_clight : clight_program → list costlabel ≝
     50λp. foldl … (λls,f. labels_of_clight_fundef f @ ls) [ ] (prog_funct ?? p).
     51
     52definition in_clight_program : clight_program → costlabel → Prop ≝
     53λp,l. Exists … (λx.x=l) (labels_of_clight p).
    4854
    4955definition clight_label_free : clight_program → bool ≝
    50 λp. all ? clight_fundef_label_free (prog_funct ?? p).
     56λp. match labels_of_clight p with [ nil ⇒ true | _ ⇒ false ].
    5157
    5258(* Adding labels *)
  • src/compiler.ma

    r2320 r2399  
    5757include "RTLabs/semantics.ma".
    5858
    59 axiom RTLabs_abstract_status : genv → abstract_status.
    60 
    6159include "joint/Traces.ma".
    6260
    6361include "ASM/Fetch.ma". (* For load_code_memory only *)
    6462
    65 axiom in_clight_program : costlabel → Prop.
    66 
    6763definition lift_cost_map_back_to_front :
    68   ∀code_memory, lbls.
     64  ∀clight, code_memory, lbls.
    6965   (∀l. (∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l) +
    7066       ¬(∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l)) →
    7167  as_cost_map (ASM_abstract_status code_memory lbls) →
    72   (Σl : costlabel.in_clight_program l) → ℕ ≝ λcode_memory,lbls,dec,k,l_sig.
     68  (Σl : costlabel.in_clight_program clight l) → ℕ ≝ λclight,code_memory,lbls,dec,k,l_sig.
    7369   match dec l_sig with
    7470   [ inl prf ⇒ k «l_sig, prf»
     
    7773
    7874definition compile : clight_program →
    79   res (object_code × costlabel_map × clight_program × ((Σl.in_clight_program l) → ℕ)) ≝
     75  res (object_code × costlabel_map × (𝚺labelled:clight_program. ((Σl.in_clight_program labelled l) → ℕ))) ≝
    8076λp.
    8177  ! 〈init_cost,p',p〉 ← front_end p;
     
    8480  let k ≝ ASM_cost_map p ? in
    8581  let k' ≝ lift_cost_map_back_to_front
     82    p'
    8683    (load_code_memory (\fst p))
    8784    (\snd p)
    8885    ? k
    8986    in
    90   return 〈p, p', k'〉.
     87  return 〈p, ❬p', k'❭〉.
    9188  cases daemon
    9289  qed.
  • 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.