 Timestamp:
 Oct 17, 2012, 6:45:20 PM (7 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/label.ma
r2392 r2399 1 1 include "Clight/Csyntax.ma". 2 2 3 (* Label freedom*)4 5 let rec expr_label_free (e:expr) : bool ≝3 (* Extract cost labels from a program. *) 4 5 let rec labels_of_expr (e:expr) : list costlabel ≝ 6 6 match e with 7 7 [ Expr e' _ ⇒ 8 8 match e' with 9 [ Ederef e1 ⇒ expr_label_freee110  Eaddrof e1 ⇒ expr_label_freee111  Eunop _ e1 ⇒ expr_label_freee112  Ebinop _ e1 e2 ⇒ expr_label_free e1 ∧ expr_label_freee213  Ecast _ e1 ⇒ expr_label_freee114  Econdition e1 e2 e3 ⇒ expr_label_free e1 ∧ expr_label_free e2 ∧ expr_label_freee315  Eandbool e1 e2 ⇒ expr_label_free e1 ∧ expr_label_freee216  Eorbool e1 e2 ⇒ expr_label_free e1 ∧ expr_label_freee217  Efield e1 _ ⇒ expr_label_freee118  Ecost _ _ ⇒ false19  _ ⇒ true9 [ 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  _ ⇒ [ ] 20 20 ] 21 21 ]. 22 22 23 let rec statement_label_free (s:statement) : bool ≝23 let rec labels_of_statement (s:statement) : list costlabel ≝ 24 24 match s with 25 [ Sassign e1 e2 ⇒ expr_label_free e1 ∧ expr_label_freee226  Scall oe e1 es ⇒ option_map_def … expr_label_free true oe ∧ expr_label_free e1 ∧ all … expr_label_freees27  Ssequence s1 s2 ⇒ statement_label_free s1 ∧ statement_label_frees228  Sifthenelse e1 s1 s2 ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ statement_label_frees229  Swhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_frees130  Sdowhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_frees131  Sfor s1 e1 s2 s3 ⇒ statement_label_free s1 ∧ expr_label_free e1 ∧ statement_label_free s2 ∧ statement_label_frees332  Sreturn oe ⇒ option_map_def … expr_label_free trueoe33  Sswitch e1 ls ⇒ expr_label_free e1 ∧ labeled_statements_label_freels34  Slabel _ s1 ⇒ statement_label_frees135  Scost _ _ ⇒ false36  _ ⇒ true37 ] and label ed_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 ≝ 38 38 match ls with 39 [ LSdefault s1 ⇒ statement_label_frees140  LScase _ _ s1 ls1 ⇒ statement_label_free s1 ∧ labeled_statements_label_freels141 ]. 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 43 definition labels_of_clight_fundef : ident × clight_fundef → list costlabel ≝ 44 44 λ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 49 definition labels_of_clight : clight_program → list costlabel ≝ 50 λp. foldl … (λls,f. labels_of_clight_fundef f @ ls) [ ] (prog_funct ?? p). 51 52 definition in_clight_program : clight_program → costlabel → Prop ≝ 53 λp,l. Exists … (λx.x=l) (labels_of_clight p). 48 54 49 55 definition 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 ]. 51 57 52 58 (* Adding labels *) 
src/compiler.ma
r2320 r2399 57 57 include "RTLabs/semantics.ma". 58 58 59 axiom RTLabs_abstract_status : genv → abstract_status.60 61 59 include "joint/Traces.ma". 62 60 63 61 include "ASM/Fetch.ma". (* For load_code_memory only *) 64 62 65 axiom in_clight_program : costlabel → Prop.66 67 63 definition lift_cost_map_back_to_front : 68 ∀c ode_memory, lbls.64 ∀clight, code_memory, lbls. 69 65 (∀l. (∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l) + 70 66 ¬(∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l)) → 71 67 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. 73 69 match dec l_sig with 74 70 [ inl prf ⇒ k «l_sig, prf» … … 77 73 78 74 definition 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) → ℕ))) ≝ 80 76 λp. 81 77 ! 〈init_cost,p',p〉 ← front_end p; … … 84 80 let k ≝ ASM_cost_map p ? in 85 81 let k' ≝ lift_cost_map_back_to_front 82 p' 86 83 (load_code_memory (\fst p)) 87 84 (\snd p) 88 85 ? k 89 86 in 90 return 〈p, p', k'〉.87 return 〈p, ❬p', k'❭〉. 91 88 cases daemon 92 89 qed. 
src/correctness.ma
r2325 r2399 12 12 13 13 ∀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❭〉 → 15 15 16 16 not_wrong … (exec_inf … clight_fullexec input_program) → … … 41 41 42 42 definition 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. 43 let 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)) ≝ 44 match 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 55 definition 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 58 definition 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 71 definition stack_after : Clight_stack_T → execution_prefix → nat ≝ 72 λsc,x. \fst (measure_stack sc x). 73 74 definition max_stack : Clight_stack_T → execution_prefix → nat ≝ 75 λsc,x. \snd (measure_stack sc x). 45 76 46 77 (* TODO: cost labels *) … … 72 103 split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧ 73 104 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 ∧ 75 107 max_stack < max_allowed_stack. 76 108 … … 85 117 *) 86 118 87 axiom observables : clight_program → nat → nat → option ((list trace) × (list trace)). 119 definition 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 88 134 axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)). 89 axiom clight_clock_after : clight_program → nat → option nat. 135 136 definition in_execution_prefix : execution_prefix → costlabel → Prop ≝ 137 λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x. 138 139 let 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 ≝ 140 match 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 148 definition 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 151 lemma 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 160 definition 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. 165 whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E 166 qed. 167 168 definition 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 ]. 176 cases daemon 177 qed. 178 90 179 axiom initial_8051_status : ∀oc. Status oc. 91 180 92 181 definition simulates ≝ 93 λstack_cost, stack_bound, labelled, object_code .182 λstack_cost, stack_bound, labelled, object_code, cost_map. 94 183 let initial_status ≝ initial_8051_status (load_code_memory object_code) in 95 184 ∀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 → 97 186 ∃n1,n2. observables labelled m1 m2 = observables_8051 object_code n1 n2 ∧ 98 187 c2  c1 = clock … (execute n2 ? initial_status)  clock … (execute n1 ? initial_status). 99 188 100 axiom compile' : clight_program → res (object_code × costlabel_map × clight_program101 × ((Σl:costlabel.in_clight_program l)→ℕ) × Clight_stack_T × nat).189 axiom compile' : clight_program → res (object_code × costlabel_map × 190 (𝚺labelled:clight_program. ((Σl:costlabel.in_clight_program labelled l)→ℕ)) × Clight_stack_T × nat). 102 191 103 192 theorem correct' : … … 107 196 108 197 ∀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〉 → 110 199 111 200 sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled) 112 201 ∧ 113 202 114 simulates stack_cost stack_bound labelled object_code .203 simulates stack_cost stack_bound labelled object_code cost_map. 115 204 116 205
Note: See TracChangeset
for help on using the changeset viewer.