Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3535 r3549 17 17 ; io_instr : Type[0] }. 18 18 19 inductive AssemblerInstr (p : assembler_params) : Type[0] ≝20  Seq : seq_instr p → option (NonFunctionalLabel ) → AssemblerInstrp21  Ijmp: ℕ → AssemblerInstr p 22  CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstrp23  Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstrp24  Icall: FunctionName → AssemblerInstr p 25  Iret: AssemblerInstr p .26 27 definition labels_pc_of_instr : ∀p .AssemblerInstr p → ℕ → list (CostLabel× ℕ) ≝28 λp, i,program_counter.19 inductive AssemblerInstr (p : assembler_params) (l_p : label_params) : Type[0] ≝ 20  Seq : seq_instr p → option (NonFunctionalLabel l_p) → AssemblerInstr p l_p 21  Ijmp: ℕ → AssemblerInstr p l_p 22  CJump : jump_condition p → ℕ → NonFunctionalLabel l_p → NonFunctionalLabel l_p → AssemblerInstr p l_p 23  Iio : NonFunctionalLabel l_p → io_instr p → NonFunctionalLabel l_p → AssemblerInstr p l_p 24  Icall: FunctionName → AssemblerInstr p l_p 25  Iret: AssemblerInstr p l_p. 26 27 definition labels_pc_of_instr : ∀p,l_p.AssemblerInstr p l_p → ℕ → list (CostLabel l_p × ℕ) ≝ 28 λp,l_p,i,program_counter. 29 29 match i with 30 30 [ Seq _ opt_l ⇒ match opt_l with 31 [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉]31 [ Some lbl ⇒ [〈(a_non_functional_label … lbl),S program_counter〉] 32 32  None ⇒ [ ] 33 33 ] 34 34  Ijmp _ ⇒ [ ] 35  CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉;36 〈(a_non_functional_label lfalse),S program_counter〉]37  Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉;38 〈(a_non_functional_label lout),S program_counter〉]35  CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label … ltrue),newpc〉; 36 〈(a_non_functional_label … lfalse),S program_counter〉] 37  Iio lin _ lout ⇒ [〈(a_non_functional_label … lin),program_counter〉; 38 〈(a_non_functional_label … lout),S program_counter〉] 39 39  Icall f ⇒ [ ] 40 40  Iret ⇒ [ ] 41 41 ]. 42 42 43 let rec labels_pc (p : assembler_params) 44 (prog : list (AssemblerInstr p )) (call_label_fun : list (ℕ × CallCostLabel))45 (return_label_fun : list (ℕ × ReturnPostCostLabel)) (i_act : NonFunctionalLabel)46 (program_counter : ℕ) on prog : list ( CostLabel× ℕ) ≝43 let rec labels_pc (p : assembler_params) (l_p : label_params) 44 (prog : list (AssemblerInstr p l_p)) (call_label_fun : list (ℕ × (CallCostLabel l_p))) 45 (return_label_fun : list (ℕ × (ReturnPostCostLabel l_p))) (i_act : NonFunctionalLabel l_p) 46 (program_counter : ℕ) on prog : list ((CostLabel l_p) × ℕ) ≝ 47 47 match prog with 48 [ nil ⇒ [〈a_non_functional_label (i_act),O〉] @49 map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun) @50 map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun)51  cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is call_label_fun return_label_fun i_act (S program_counter)48 [ nil ⇒ [〈a_non_functional_label … (i_act),O〉] @ 49 map … (λx.let〈y,z〉 ≝ x in 〈(a_call … z),y〉) (call_label_fun) @ 50 map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post … z),y〉) (return_label_fun) 51  cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p l_p is call_label_fun return_label_fun i_act (S program_counter) 52 52 ]. 53 53 54 54 include "basics/lists/listb.ma". 55 55 56 (*doppione da mettere a posto*) 57 let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ 58 match l with 59 [ nil ⇒ True 60  cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs 61 ]. 62 63 64 record AssemblerProgram (p : assembler_params) : Type[0] ≝ 65 { instructions : list (AssemblerInstr p) 56 57 record AssemblerProgram (p : assembler_params) (l_p : label_params) : Type[0] ≝ 58 { instructions : list (AssemblerInstr p l_p) 66 59 ; endmain : ℕ 67 60 ; endmain_ok : endmain < instructions 68 61 ; entry_of_function : FunctionName → ℕ 69 ; call_label_fun : list (ℕ × CallCostLabel)70 ; return_label_fun : list (ℕ × ReturnPostCostLabel)71 ; in_act : NonFunctionalLabel 62 ; call_label_fun : list (ℕ × (CallCostLabel l_p)) 63 ; return_label_fun : list (ℕ × (ReturnPostCostLabel l_p)) 64 ; in_act : NonFunctionalLabel l_p 72 65 ; asm_no_duplicates : no_duplicates … (map ?? \fst … (labels_pc … instructions call_label_fun return_label_fun in_act O)) 73 66 }. 74 67 75 68 76 definition fetch: ∀p .AssemblerProgram p → ℕ → option (AssemblerInstrp) ≝77 λp,l ,n. nth_opt ? n (instructions … l).69 definition fetch: ∀p,l_p.AssemblerProgram p l_p → ℕ → option (AssemblerInstr p l_p) ≝ 70 λp,l_p,l,n. nth_opt ? n (instructions … l). 78 71 79 72 definition stackT: Type[0] ≝ list (nat). … … 102 95 103 96 104 inductive vmstep (p : assembler_params) (p' : sem_params p) 105 (prog : AssemblerProgram p ) :106 ActionLabel → relation (vm_state p p') ≝97 inductive vmstep (p : assembler_params) (p' : sem_params p) (l_p : label_params) 98 (prog : AssemblerProgram p l_p) : 99 ActionLabel l_p → relation (vm_state p p') ≝ 107 100  vm_seq : ∀st1,st2 : vm_state p p'.∀i,l. 108 fetch … prog (pc … st1) = return (Seq p i l) →101 fetch … prog (pc … st1) = return (Seq p l_p i l) → 109 102 asm_is_io … st1 = false → 110 103 eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → … … 112 105 asm_is_io … st1 = asm_is_io … st2 → 113 106 S (pc … st1) = pc … st2 → 114 vmstep … (cost_act l) st1 st2107 vmstep … (cost_act … l) st1 st2 115 108  vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ. 116 fetch … prog (pc … st1) = return (Ijmp p new_pc) →109 fetch … prog (pc … st1) = return (Ijmp p l_p new_pc) → 117 110 asm_is_io … st1 = false → 118 111 asm_store … st1 = asm_store … st2 → … … 120 113 asm_is_io … st1 = asm_is_io … st2 → 121 114 new_pc = pc … st2 → 122 vmstep … (cost_act (None ?)) st1 st2115 vmstep … (cost_act … (None ?)) st1 st2 123 116  vm_cjump_true : 124 117 ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse. 125 118 eval_asm_cond p p' cond (asm_store … st1) = return true→ 126 fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →119 fetch … prog (pc … st1) = return (CJump p l_p cond new_pc ltrue lfalse) → 127 120 asm_is_io … st1 = false → 128 121 asm_store … st1 = asm_store … st2 → … … 130 123 asm_is_io … st1 = asm_is_io … st2 → 131 124 pc … st2 = new_pc → 132 vmstep … (cost_act (Some ? ltrue)) st1 st2125 vmstep … (cost_act … (Some ? ltrue)) st1 st2 133 126  vm_cjump_false : 134 127 ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse. 135 128 eval_asm_cond p p' cond (asm_store … st1) = return false→ 136 fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →129 fetch … prog (pc … st1) = return (CJump p l_p cond new_pc ltrue lfalse) → 137 130 asm_is_io … st1 = false → 138 131 asm_store … st1 = asm_store … st2 → … … 140 133 asm_is_io … st1 = asm_is_io … st2 → 141 134 S (pc … st1) = pc … st2 → 142 vmstep … (cost_act (Some ? lfalse)) st1 st2135 vmstep … (cost_act … (Some ? lfalse)) st1 st2 143 136  vm_io_in : 144 137 ∀st1,st2 : vm_state p p'.∀lin,io,lout. 145 fetch … prog (pc … st1) = return (Iio p l in io lout) →138 fetch … prog (pc … st1) = return (Iio p l_p lin io lout) → 146 139 asm_is_io … st1 = false → 147 140 asm_store … st1 = asm_store … st2 → … … 149 142 true = asm_is_io … st2 → 150 143 pc … st1 = pc … st2 → 151 vmstep … (cost_act (Some ? lin)) st1 st2144 vmstep … (cost_act … (Some ? lin)) st1 st2 152 145  vm_io_out : 153 146 ∀st1,st2 : vm_state p p'.∀lin,io,lout. 154 fetch … prog (pc … st1) = return (Iio p l in io lout) →147 fetch … prog (pc … st1) = return (Iio p l_p lin io lout) → 155 148 asm_is_io … st1 = true → 156 149 eval_asm_io … io (asm_store … st1) = return asm_store … st2 → … … 158 151 false = asm_is_io … st2 → 159 152 S (pc … st1) = pc … st2 → 160 vmstep … (cost_act (Some ? lout)) st1 st2153 vmstep … (cost_act … (Some ? lout)) st1 st2 161 154  vm_call : 162 155 ∀st1,st2 : vm_state p p'.∀f,lbl. 163 fetch … prog (pc … st1) = return (Icall p f) →156 fetch … prog (pc … st1) = return (Icall p l_p f) → 164 157 asm_is_io … st1 = false → 165 158 asm_store … st1 = asm_store … st2 → … … 167 160 asm_is_io … st1 = asm_is_io … st2 → 168 161 entry_of_function … prog f = pc … st2 → 169 label_of_pc ?(call_label_fun … prog) (entry_of_function … prog f) = return lbl →170 vmstep … (call_act f lbl) st1 st2162 label_of_pc … (call_label_fun … prog) (entry_of_function … prog f) = return lbl → 163 vmstep … (call_act … f lbl) st1 st2 171 164  vm_ret : 172 165 ∀st1,st2 : vm_state p p'.∀newpc,lbl. 173 fetch … prog (pc … st1) = return (Iret p ) →166 fetch … prog (pc … st1) = return (Iret p l_p) → 174 167 asm_is_io … st1 = false → 175 168 asm_store … st1 = asm_store … st2 → … … 177 170 asm_is_io … st1 = asm_is_io … st2 → 178 171 newpc = pc … st2 → 179 label_of_pc ?(return_label_fun … prog) newpc = return lbl →180 vmstep … (ret_act (Some ? lbl)) st1 st2.181 182 definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p. 183 AssemblerProgram p → vm_state p p' → option (ActionLabel× (vm_state p p')) ≝184 λp,p', prog,st.172 label_of_pc … (return_label_fun … prog) newpc = return lbl → 173 vmstep … (ret_act … (Some ? lbl)) st1 st2. 174 175 definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p.∀l_p : label_params. 176 AssemblerProgram p l_p → vm_state p p' → option ((ActionLabel l_p) × (vm_state p p')) ≝ 177 λp,p',l_p,prog,st. 185 178 ! i ← fetch … prog (pc … st); 186 179 match i with … … 190 183 else 191 184 ! new_store ← eval_asm_seq p p' x (asm_store … st); 192 return 〈cost_act opt_l,185 return 〈cost_act … opt_l, 193 186 mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false〉 194 187  Ijmp newpc ⇒ … … 196 189 None ? 197 190 else 198 return 〈cost_act (None ?),191 return 〈cost_act … (None ?), 199 192 mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉 200 193  CJump cond newpc ltrue lfalse ⇒ … … 204 197 ! b ← eval_asm_cond p p' cond (asm_store … st); 205 198 if b then 206 return 〈cost_act (Some ? ltrue),199 return 〈cost_act …(Some ? ltrue), 207 200 mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉 208 201 else 209 return 〈cost_act (Some ? lfalse),202 return 〈cost_act … (Some ? lfalse), 210 203 mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false〉 211 204  Iio lin io lout ⇒ 212 205 if asm_is_io … st then 213 206 ! new_store ← eval_asm_io … io (asm_store … st); 214 return 〈cost_act (Some ? lout),207 return 〈cost_act … (Some ? lout), 215 208 mk_vm_state ?? (S (pc … st)) (asm_stack … st) 216 209 new_store false〉 217 210 else 218 return 〈cost_act (Some ? lin),211 return 〈cost_act … (Some ? lin), 219 212 mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st) 220 213 true〉 … … 224 217 else 225 218 ! lbl ← label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f); 226 return 〈call_act f lbl,219 return 〈call_act … f lbl, 227 220 mk_vm_state ?? (entry_of_function … prog f) 228 221 ((S (pc … st)) :: (asm_stack … st)) … … 233 226 ! 〈newpc,tl〉 ← option_pop … (asm_stack … st); 234 227 ! lbl ← label_of_pc ? (return_label_fun … prog) newpc; 235 return 〈ret_act (Some ? lbl),228 return 〈ret_act … (Some ? lbl), 236 229 mk_vm_state ?? newpc tl (asm_store … st) false〉 237 230 ]. 238 231 239 lemma eval_vmstate_to_Prop : ∀p,p', prog,st1,st2,l.240 eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2.241 #p #p' # prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta232 lemma eval_vmstate_to_Prop : ∀p,p',l_p,prog,st1,st2,l. 233 eval_vmstate p p' l_p prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2. 234 #p #p' #l_p #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta 242 235 #H cases(bind_inversion ????? H) H * normalize nodelta 243 236 [ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta … … 269 262 270 263 271 lemma vm_step_to_eval : ∀p,p', prog,st1,st2,l.vmstep … prog l st1 st2 →272 eval_vmstate p p' prog st1 = return 〈l,st2〉.273 #p #p' # prog * #pc1 #stack1 #store1 #io1264 lemma vm_step_to_eval : ∀p,p',l_p,prog,st1,st2,l.vmstep … prog l st1 st2 → 265 eval_vmstate p p' l_p prog st1 = return 〈l,st2〉. 266 #p #p' #l_p #prog * #pc1 #stack1 #store1 #io1 274 267 * #pc2 #stack2 #store2 #io2 #l #H inversion H 275 268 [ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc … … 316 309 317 310 definition ass_vmstep ≝ 318 λp,p', prog.311 λp,p',l_p,prog. 319 312 λl.λs1,s2 : vm_ass_state p p'. 320 313 match s1 with … … 322 315 match s2 with 323 316 [ STATE st2 ⇒ 324 (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' prog l st1 st2317 (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' l_p prog l st1 st2 325 318  INITIAL ⇒ False 326 319  FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧ 327 l = cost_act (Some … (in_act … prog))320 l = cost_act … (Some … (in_act … prog)) 328 321 ] 329 322  INITIAL ⇒ match s2 with 330 323 [ STATE st2 ⇒ eqb (pc … st2) O = true ∧ 331 l = cost_act (Some … (in_act … prog))324 l = cost_act … (Some … (in_act … prog)) 332 325  _ ⇒ False 333 326 ] … … 335 328 ]. 336 329 337 definition asm_operational_semantics : ∀p .sem_params p → AssemblerProgram p → abstract_status≝338 λp, p',prog.let init_act ≝ cost_act(Some ? (in_act … prog)) in339 let end_act ≝ cost_act (Some ? (in_act … prog)) in340 mk_abstract_status 330 definition asm_operational_semantics : ∀p,l_p.sem_params p → AssemblerProgram p l_p → abstract_status l_p ≝ 331 λp,l_p,p',prog.let init_act ≝ cost_act … (Some ? (in_act … prog)) in 332 let end_act ≝ cost_act … (Some ? (in_act … prog)) in 333 mk_abstract_status … 341 334 (vm_ass_state p p') 342 335 (ass_vmstep … prog) … … 427 420 428 421 definition asm_concrete_trans_sys ≝ 429 λp,p', prog.mk_concrete_transition_sys …430 (asm_operational_semantics p p' prog).422 λp,p',l_p,prog.mk_concrete_transition_sys … 423 (asm_operational_semantics p p' l_p prog). 431 424 432 425 433 426 definition emits_labels ≝ 434 λp .λinstr : AssemblerInstrp.match instr with427 λp,l_p.λinstr : AssemblerInstr p l_p.match instr with 435 428 [ Seq _ opt_l ⇒ match opt_l with 436 429 [ None ⇒ Some ? (λpc.S pc) … … 441 434 ]. 442 435 443 definition fetch_state : ∀p,p' .AssemblerProgram p → vm_state p p' → option (AssemblerInstrp) ≝444 λp,p', prog,st.fetch … prog (pc … st).445 446 record asm_galois_connection (p: assembler_params) (p': sem_params p) ( prog: AssemblerProgramp) : Type[2] ≝436 definition fetch_state : ∀p,p',l_p.AssemblerProgram p l_p → vm_state p p' → option (AssemblerInstr p l_p) ≝ 437 λp,p',l_p,prog,st.fetch … prog (pc … st). 438 439 record asm_galois_connection (p: assembler_params) (p': sem_params p) (l_p : label_params) (prog: AssemblerProgram p l_p) : Type[2] ≝ 447 440 { aabs_d : abstract_transition_sys 448 ; agalois_rel:> galois_rel (asm_concrete_trans_sysp p' prog) aabs_d441 ; agalois_rel:> galois_rel … (asm_concrete_trans_sys p l_p p' prog) aabs_d 449 442 }. 450 443 451 444 definition galois_connection_of_asm_galois_connection: 452 ∀p,p', prog. asm_galois_connection p p' prog → galois_connection≝453 λp,p', prog,agc.454 mk_galois_connection 455 (asm_concrete_trans_sys p p' prog)445 ∀p,p',l_p,prog. asm_galois_connection p p' l_p prog → galois_connection l_p ≝ 446 λp,p',l_p,prog,agc. 447 mk_galois_connection … 448 (asm_concrete_trans_sys p l_p p' prog) 456 449 (aabs_d … agc) 457 450 (agalois_rel … agc). … … 460 453 461 454 definition ass_fetch ≝ 462 λp,p', prog.463 λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain …prog) then455 λp,p',l_p,prog. 456 λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain p l_p prog) then 464 457 Some ? (None ?) 465 else ! x ← fetch_state p p' prog st; Some ? (Some ? x)458 else ! x ← fetch_state p p' l_p prog st; Some ? (Some ? x) 466 459  INITIAL ⇒ Some ? (None ?) 467 460  FINAL ⇒ None ? ]. 468 461 469 462 definition ass_instr_map ≝ 470 λp,p', prog.λasm_galois_conn: asm_galois_connection p p'prog.471 λinstr_map: AssemblerInstr p → (*option*) (abs_instr … (abs_dasm_galois_conn)).463 λp,p',l_p,prog.λasm_galois_conn: asm_galois_connection p p' l_p prog. 464 λinstr_map: AssemblerInstr p l_p → (*option*) (abs_instr … (abs_d … asm_galois_conn)). 472 465 (λi.match i with [None ⇒ (*Some …*) (e …) Some x ⇒ instr_map … x]). 473 466 474 record asm_abstract_interpretation (p: assembler_params) (p': sem_params p) ( prog: AssemblerProgramp) : Type[2] ≝475 { asm_galois_conn: asm_galois_connection p p' prog476 ; instr_map : AssemblerInstr p → (*option*) (abs_instr … (abs_dasm_galois_conn))467 record asm_abstract_interpretation (p: assembler_params) (p': sem_params p) (l_p : label_params) (prog: AssemblerProgram p l_p) : Type[2] ≝ 468 { asm_galois_conn: asm_galois_connection p p' l_p prog 469 ; instr_map : AssemblerInstr p l_p → (*option*) (abs_instr … (abs_d … asm_galois_conn)) 477 470 ; instr_map_ok : 478 471 ∀s,s': concr … asm_galois_conn. ∀a: abs_d … asm_galois_conn.∀l,i. … … 484 477 485 478 definition abstract_interpretation_of_asm_abstract_interpretation: 486 ∀p,p', prog. asm_abstract_interpretation p p' prog → abstract_interpretation479 ∀p,p',l_p,prog. asm_abstract_interpretation p p' l_p prog → abstract_interpretation l_p 487 480 ≝ 488 λp,p', prog,aai.489 mk_abstract_interpretation 490 (asm_galois_conn … aai) (option (AssemblerInstr p )) (ass_fetch p p'prog)481 λp,p',l_p,prog,aai. 482 mk_abstract_interpretation … 483 (asm_galois_conn … aai) (option (AssemblerInstr p l_p)) (ass_fetch p p' l_p prog) 491 484 (ass_instr_map … prog … (instr_map … aai)) (instr_map_ok … aai). 492 485 … … 496 489 λA,l.match l with [ nil ⇒ false  _ ⇒ true ]. 497 490 498 let rec block_cost (p : assembler_params) 499 (prog: AssemblerProgram p ) (abs_t : monoid)500 (instr_m : AssemblerInstr p → abs_t)491 let rec block_cost (p : assembler_params) (l_p : label_params) 492 (prog: AssemblerProgram p l_p) (abs_t : monoid) 493 (instr_m : AssemblerInstr p l_p → abs_t) 501 494 (prog_c: option ℕ) 502 495 (program_size: ℕ) … … 532 525 533 526 534 lemma labels_pc_ok : ∀p, prog,l1,l2,i_act,i,lbl,pc,m.527 lemma labels_pc_ok : ∀p,l_p,prog,l1,l2,i_act,i,lbl,pc,m. 535 528 nth_opt ? pc prog = return i → 536 529 mem ? lbl (labels_pc_of_instr … i (m+pc)) → 537 mem ? lbl (labels_pc p prog l1 l2 i_act m).538 #p # instrs #l1 #l2 #iact #i #lbl #pc530 mem ? lbl (labels_pc p l_p prog l1 l2 i_act m). 531 #p #l_p #instrs #l1 #l2 #iact #i #lbl #pc 539 532 whd in match fetch; normalize nodelta lapply pc pc 540 533 elim instrs … … 547 540 qed. 548 541 549 lemma labels_pf_in_act: ∀p, prog,pc.550 mem CostLabel (in_actp prog)551 (map ( CostLabel×ℕ) CostLabel\fst552 (labels_pc p (instructions p prog) (call_label_fun pprog)553 (return_label_fun p prog) (in_act pprog) pc)).554 #p # prog elim (instructions pprog) normalize /2/555 qed. 556 557 lemma labels_pc_return: ∀p, prog,l1,l2,iact,x1,x2.558 label_of_pc ReturnPostCostLabell2 x1=return x2 →542 lemma labels_pf_in_act: ∀p,l_p,prog,pc. 543 mem (CostLabel l_p) (in_act p l_p prog) 544 (map ((CostLabel l_p)×ℕ) (CostLabel l_p) \fst 545 (labels_pc p … (instructions p … prog) (call_label_fun p … prog) 546 (return_label_fun p … prog) (in_act p … prog) pc)). 547 #p #l_p #prog elim (instructions … prog) normalize /2/ 548 qed. 549 550 lemma labels_pc_return: ∀p,l_p,prog,l1,l2,iact,x1,x2. 551 label_of_pc (ReturnPostCostLabel l_p) l2 x1=return x2 → 559 552 ∀m. 560 mem … 〈(a_return_post x2),x1〉 (labels_pcp prog l1 l2 iact m).561 #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l553 mem … 〈(a_return_post … x2),x1〉 (labels_pc p l_p prog l1 l2 iact m). 554 #p #l_p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l 562 555 [ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?); 563 556 elim l2 in H; [ whd in ⊢ (??%% → ?); #EQ destruct] … … 569 562 qed. 570 563 571 lemma labels_pc_call: ∀p, prog,l1,l2,iact,x1,x2.572 label_of_pc CallCostLabell1 x1=return x2 →564 lemma labels_pc_call: ∀p,l_p,prog,l1,l2,iact,x1,x2. 565 label_of_pc (CallCostLabel l_p) l1 x1=return x2 → 573 566 ∀m. 574 mem … 〈(a_call x2),x1〉 (labels_pcp prog l1 l2 iact m).575 #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l567 mem … 〈(a_call l_p x2),x1〉 (labels_pc p l_p prog l1 l2 iact m). 568 #p #l_p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l 576 569 [ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?); 577 570 elim l1 in H; [ whd in ⊢ (??%% → ?); #EQ destruct] … … 609 602 ]. 610 603 611 definition static_analisys : ∀p : assembler_params.∀ abs_t : monoid.(AssemblerInstr p → abs_t) →612 ∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgramp → option mT ≝613 λp, abs_t,instr_m,mT,prog.604 definition static_analisys : ∀p : assembler_params.∀l_p : label_params.∀abs_t : monoid.(AssemblerInstr p l_p → abs_t …) → 605 ∀mT : cost_map_T (DEQCostLabel l_p) (abs_t …).AssemblerProgram p l_p → option mT ≝ 606 λp,l_p,abs_t,instr_m,mT,prog. 614 607 let prog_size ≝ S (instructions … prog) in 615 m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m (Some ? w) prog_size;608 m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p l_p prog abs_t instr_m (Some ? w) prog_size; 616 609 return set_map … m z k) (labels_pc … (instructions … prog) 617 610 (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O) 618 611 (empty_map ?? mT). 619 612 620 621 (*falso: necessita di no_duplicates*)622 613 623 614 definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝ … … 658 649 qed. 659 650 660 lemma static_analisys_ok : ∀p, abs_t,instr_m,mT,prog,lbl,pc,map.661 static_analisys p abs_t instr_m mT prog = return map →651 lemma static_analisys_ok : ∀p,l_p,abs_t,instr_m,mT,prog,lbl,pc,map. 652 static_analisys p l_p abs_t instr_m mT prog = return map → 662 653 mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) (call_label_fun … prog) 663 654 (return_label_fun … prog) (in_act … prog) O) → … … 665 656 block_cost … prog abs_t instr_m (Some ? pc) (S ((instructions … prog))) ∧ 666 657 block_cost … prog abs_t instr_m (Some ? pc) (S ((instructions … prog))) ≠ None ?. 667 #p # abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta658 #p #l_p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta 668 659 #endmain #Hendmain #entry_fun #call_label_fun #return_label_fun #inact 669 660 #nodup generalize in match nodup in ⊢ (∀_.∀_.∀_. (??(????%??)?) → %); #Hnodup lapply nodup nodup 670 lapply (labels_pc ?????? ) #l elim l [ #x #y #z #w #h * ]661 lapply (labels_pc ???????) #l elim l [ #x #y #z #w #h * ] 671 662 * #hd1 #hd2 #tl #IH * #H1 #H2 #lbl #pc #map #H 672 663 cases(bind_inversion ????? H) H #map1 * #EQmap1 normalize nodelta #H … … 683 674 qed. 684 675 685 definition terminated_trace : ∀ S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝686 λ S,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind? s2 s3 s3 l prf … (t_base … s3))687 ∧ is_costlabelled_act l ∧ pre_measurable_trace … t1.676 definition terminated_trace : ∀p : label_params.∀S : abstract_status p.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝ 677 λp,S,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind p ? s2 s3 s3 l prf … (t_base … s3)) 678 ∧ is_costlabelled_act … l ∧ pre_measurable_trace … t1. 688 679 689 680 definition big_op: ∀M: monoid. list M → M ≝ … … 716 707 qed. 717 708 718 lemma monotonicity_of_block_cost : ∀p, prog,abs_t,instr_m,pc,size,k.719 block_cost p prog abs_t instr_m (Some ? pc) size = return k →709 lemma monotonicity_of_block_cost : ∀p,l_p,prog,abs_t,instr_m,pc,size,k. 710 block_cost p l_p prog abs_t instr_m (Some ? pc) size = return k → 720 711 ∀size'.size ≤ size' → 721 block_cost p prog abs_t instr_m (Some ? pc) size' = return k.722 #p # prog #abs_t #instr_m #pc #size lapply pc elim size712 block_cost p l_p prog abs_t instr_m (Some ? pc) size' = return k. 713 #p #l_p #prog #abs_t #instr_m #pc #size lapply pc elim size 723 714 [ #pc #k whd in ⊢ (??%% → ?); #EQ destruct] 724 715 #n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim … … 741 732 qed. 742 733 743 lemma step_emit : ∀p,p', prog,st1,st2,l,i.744 fetch p prog (pc … st1) = return i →734 lemma step_emit : ∀p,p',l_p,prog,st1,st2,l,i. 735 fetch p l_p prog (pc … st1) = return i → 745 736 eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 746 737 emits_labels … i = None ? → ∃x. 747 match l in ActionLabel return λ_: ActionLabel.(list CostLabel) with748 [call_act f c ⇒ [a_call c]738 match l in ActionLabel return λ_: (ActionLabel l_p).(list (CostLabel l_p)) with 739 [call_act f c ⇒ [a_call … c] 749 740 ret_act x ⇒ 750 match x with [None⇒[]Some c⇒[a_return_post c]]741 match x with [None⇒[]Some c⇒[a_return_post … c]] 751 742 cost_act x ⇒ 752 match x with [None⇒[]Some c⇒[a_non_functional_label c]]743 match x with [None⇒[]Some c⇒[a_non_functional_label … c]] 753 744 ] = [x] ∧ 754 (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).755 #p #p' # prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta745 (mem … 〈x,pc … st2〉 (labels_pc p l_p (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)). 746 #p #p' #l_p #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta 756 747 >EQi >m_return_bind normalize nodelta cases i in EQi; i normalize nodelta 757 748 [ #seq * [#lab] … … 775 766 qed. 776 767 777 lemma step_non_emit : ∀p,p', prog,st1,st2,l,i,f.778 fetch p prog (pc … st1) = return i →768 lemma step_non_emit : ∀p,p',l_p,prog,st1,st2,l,i,f. 769 fetch p l_p prog (pc … st1) = return i → 779 770 eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 780 771 emits_labels … i = Some ? f → 781 match l in ActionLabel return λ_: ActionLabel.(list CostLabel) with782 [call_act f c ⇒ [a_call c]772 match l in ActionLabel return λ_: (ActionLabel l_p).(list (CostLabel l_p)) with 773 [call_act f c ⇒ [a_call … c] 783 774 ret_act x ⇒ 784 match x with [None⇒[]Some c⇒[a_return_post c]]775 match x with [None⇒[]Some c⇒[a_return_post … c]] 785 776 cost_act x ⇒ 786 match x with [None⇒[]Some c⇒[a_non_functional_label c]]777 match x with [None⇒[]Some c⇒[a_non_functional_label … c]] 787 778 ] = [ ] ∧ pc … st2 = f (pc … st1). 788 #p #p' # prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta779 #p #p' #l_p #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta 789 780 >EQi >m_return_bind normalize nodelta cases i in EQi; i normalize nodelta 790 781 [ #seq * [#lab] … … 807 798 808 799 lemma labels_of_trace_are_in_code : 809 ∀p,p', prog.∀st1,st2 : vm_ass_state p p'.∀t : raw_trace (asm_operational_semanticsp p' prog) … st1 st2.800 ∀p,p',l_p,prog.∀st1,st2 : vm_ass_state p p'.∀t : raw_trace … (asm_operational_semantics p l_p p' prog) … st1 st2. 810 801 ∀lbl. 811 802 mem … lbl (get_costlabels_of_trace … t) → 812 mem … lbl (map … \fst … (labels_pc … (instructions p prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).813 #p #p' # prog #st1 #st2 #t elim t803 mem … lbl (map … \fst … (labels_pc … (instructions p … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)). 804 #p #p' #l_p #prog #st1 #st2 #t elim t 814 805 [ #st #lbl * 815 806  #st1 #st2 #st3 #l whd in ⊢ (% → ?); … … 862 853 863 854 864 lemma tbase_tind_append : ∀ S : abstract_status.∀st1,st2,st3.∀t : raw_trace … st1 st2.855 lemma tbase_tind_append : ∀p : label_params.∀S : abstract_status p.∀st1,st2,st3 : S.∀t : raw_trace … st1 st2. 865 856 ∀l,prf.∀t'. 866 t_base … st1 = t @ t_ind S st2 st3 st1 l prf t' → False.867 # S #st1 #st2 #st3 *857 t_base … st1 = t @ t_ind … S st2 st3 st1 l prf t' → False. 858 #p #S #st1 #st2 #st3 * 868 859 [ #st #l #prf #t' normalize #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct ] 869 860 #s1 #s2 #s3 #l1 #prf1 #t2 #l2 #prf2 #t3 normalize #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct … … 893 884 *) 894 885 895 lemma get_cost_label_of_trace_tind : ∀ S : abstract_status.886 lemma get_cost_label_of_trace_tind : ∀p. ∀S : abstract_status p. 896 887 ∀st1,st2,st3 : S.∀l,prf,t. 897 888 get_costlabels_of_trace … (t_ind … st1 st2 st3 l prf t) = 898 actionlabel_to_costlabel l @ get_costlabels_of_trace … t.899 # S #st1 #st2 #st3 * // qed.889 actionlabel_to_costlabel … l @ get_costlabels_of_trace … t. 890 #p #S #st1 #st2 #st3 * // qed. 900 891 901 892 lemma actionlabel_ok : 902 ∀ l : ActionLabel.903 is_costlabelled_act l → ∃c.actionlabel_to_costlabell = [c].904 * /2/ * /2/ *905 qed. 906 907 lemma i_act_in_map : ∀p, prog,iact,l1,l2.908 mem ? 〈a_non_functional_label iact,O〉 (labels_pcp prog l1 l2 iact O).909 #p # instr #iact #l1 #l2 generalize in match O in ⊢ (???%); elim instr893 ∀p.∀l : ActionLabel p. 894 is_costlabelled_act … l → ∃c.actionlabel_to_costlabel … l = [c]. 895 #p * /2/ * /2/ * 896 qed. 897 898 lemma i_act_in_map : ∀p,l_p,prog,iact,l1,l2. 899 mem ? 〈a_non_functional_label l_p iact,O〉 (labels_pc p l_p prog l1 l2 iact O). 900 #p #l_p #instr #iact #l1 #l2 generalize in match O in ⊢ (???%); elim instr 910 901 [ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???); 911 902 @mem_append_l2 @IH … … 916 907 lemma static_dynamic_inv : 917 908 (* Given an assembly program *) 918 ∀p,p', prog.909 ∀p,p',l_p,prog. 919 910 920 911 (* Given an abstraction interpretation framework for the program *) 921 ∀R: asm_abstract_interpretation p p' prog.912 ∀R: asm_abstract_interpretation p p' l_p prog. 922 913 923 914 (* If the static analysis does not fail *) … … 925 916 926 917 (* For every pre_measurable, terminated trace *) 927 ∀st1,st2. ∀t: raw_trace (asm_operational_semantics … prog) … st1 st2.918 ∀st1,st2. ∀t: raw_trace l_p (asm_operational_semantics … prog) … st1 st2. 928 919 terminated_trace … t → 929 920 … … 933 924 (* Let k be the statically computed abstract action of the prefix of the trace 934 925 up to the first label *) 935 ∀k.block_cost p prog … (instr_map … R) (get_pc … st1 (endmain … prog)) (S ((instructions … prog))) = return k →926 ∀k.block_cost p … prog … (instr_map … R) (get_pc … st1 (endmain … prog)) (S ((instructions … prog))) = return k → 936 927 937 928 (* Let abs_actions be the list of statically computed abstract actions … … 954 945 @(proj2 … (static_analisys_ok … EQmap … Hmem)) 955 946 ] 956 #p #p' # prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *947 #p #p' #l_p #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * 957 948 #l1 * #prf1 ** #EQ destruct #Hlabelled 958 949 >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1)) … … 1002 993 whd in match (dependent_map ????); #costs #EQ destruct #a1 #good_st_a1 1003 994 >neutral_r >act_neutral 1004 lapply(instr_map_ok R … (refl …) good_st_a1)995 lapply(instr_map_ok … l_p … R … (refl …) good_st_a1) 1005 996 [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta 1006 997 [1,3,5,7,9,11,13: #EQ cases(absurd ? EQ Hpc) ] #_ whd in match fetch_state; … … 1009 1000  >EQfetch in ⊢ (??%?);  >EQfetch in ⊢ (??%?);  >EQfetch in ⊢ (??%?); 1010 1001  >EQfetch in ⊢ (??%?); ] % 1011 3,9,15,21,27,33,39: skip *: try assumption // ]]]1002 3,9,15,21,27,33,39: skip *: try assumption #H @H] ]] 1012 1003  st1 * [3: #st1] #st3 #st4 #l [3: *] cases st3 st3 1013 1004 [1,2,4,5: * #H1 #H2 #tl #_ #l1 #exe @⊥ lapply tl tl lapply(refl ? (FINAL p p')) … … 1040 1031 [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??); 1041 1032 >neutral_l assumption 1042 3,6: [ >neutral_r] lapply(instr_map_ok R … (refl …) good_a1)1033 3,6: [ >neutral_r] lapply(instr_map_ok … l_p … R … (refl …) good_a1) 1043 1034 [1,7: whd in ⊢ (??%?); @eqb_elim 1044 1035 [1,3: #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state; … … 1078 1069 [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ] 1079 1070 #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption 1080  lapply(instr_map_ok R … (refl …) good_a1)1071  lapply(instr_map_ok … l_p … R … (refl …) good_a1) 1081 1072 [1: %  assumption *:] normalize in ⊢ (% → ?); #H @H 1082 1073 ] … … 1094 1085 qed. *) 1095 1086 1096 lemma execute_mem_label_pc :∀p,p', prog.∀st0,st1 :vm_state p p'.∀l1,c1.1097 actionlabel_to_costlabel l 1 = [c1] →1098 vmstep p p' prog l1 st0 st1 →1087 lemma execute_mem_label_pc :∀p,p',l_p,prog.∀st0,st1 :vm_state p p'.∀l1,c1. 1088 actionlabel_to_costlabel l_p l1 = [c1] → 1089 vmstep p p' l_p prog l1 st0 st1 → 1099 1090 mem … 〈c1,pc p p' st1〉 1100 1091 (labels_pc … (instructions … prog) (call_label_fun … prog) 1101 1092 (return_label_fun … prog) (in_act … prog) O). 1102 #p #p' # prog #st0 #st1 #l1 #c1 #EQc1 #H lapply(vm_step_to_eval … H) H1093 #p #p' #l_p #prog #st0 #st1 #l1 #c1 #EQc1 #H lapply(vm_step_to_eval … H) H 1103 1094 #H cases(bind_inversion ????? H); #i * #EQi #Hi cases(step_emit … EQi H) 1104 1095 [ #c2 whd in match actionlabel_to_costlabel in EQc1; normalize nodelta in EQc1; … … 1124 1115 include "Simulation.ma". 1125 1116 1126 lemma sub_trace_premeasurable_l1 : ∀p,p', prog.1127 ∀s1,s2,s3. ∀t1: raw_trace (asm_operational_semanticsp p' prog) … s1 s2.1128 ∀t2 : raw_trace (asm_operational_semanticsp p' prog) … s2 s3.1117 lemma sub_trace_premeasurable_l1 : ∀p,p',l_p,prog. 1118 ∀s1,s2,s3. ∀t1: raw_trace l_p (asm_operational_semantics p l_p p' prog) … s1 s2. 1119 ∀t2 : raw_trace l_p (asm_operational_semantics p l_p p' prog) … s2 s3. 1129 1120 pre_measurable_trace … (t1 @ t2) → 1130 1121 pre_measurable_trace … t1. 1131 #p #p' # prog #s1 #s2 #s3 #t1 lapply s3 s3 elim t11132 [ #st #st3 #t2 whd in ⊢ (???? % → ?); #H %1 @(head_of_premeasurable_is_not_io … H) ]1122 #p #p' #l_p #prog #s1 #s2 #s3 #t1 lapply s3 s3 elim t1 1123 [ #st #st3 #t2 whd in ⊢ (?????% → ?); #H %1 @(head_of_premeasurable_is_not_io … H) ] 1133 1124 #st1 #st2 #st3 #l #exe #tl #IH #st4 #t2 #H inversion H in ⊢ ?; 1134 1125 [ #st #class #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%?%); destruct … … 1144 1135 qed. 1145 1136 1146 lemma sub_trace_premeasurable_l2 : ∀p,p', prog.1147 ∀s1,s2,s3. ∀t1: raw_trace (asm_operational_semanticsp p' prog) … s1 s2.1148 ∀t2 : raw_trace (asm_operational_semanticsp p' prog) … s2 s3.1137 lemma sub_trace_premeasurable_l2 : ∀p,p',l_p,prog. 1138 ∀s1,s2,s3. ∀t1: raw_trace l_p (asm_operational_semantics p l_p p' prog) … s1 s2. 1139 ∀t2 : raw_trace l_p (asm_operational_semantics p l_p p' prog) … s2 s3. 1149 1140 pre_measurable_trace … (t1 @ t2) → 1150 1141 pre_measurable_trace … t2. 1151 #p #p' # prog #s1 #s2 #s3 #t1 lapply s3 s3 elim t11152 [ #st #st3 #t2 whd in ⊢ (???? % → ?); #H @H ]1142 #p #p' #l_p #prog #s1 #s2 #s3 #t1 lapply s3 s3 elim t1 1143 [ #st #st3 #t2 whd in ⊢ (?????% → ?); #H @H ] 1153 1144 #st1 #st2 #st3 #l #exe #tl #IH #st4 #t2 #H inversion H in ⊢ ?; 1154 1145 [ #st #class #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%?%); destruct … … 1168 1159 theorem static_dynamic : 1169 1160 (* Given an assembly program *) 1170 ∀p,p', prog.1161 ∀p,p',l_p,prog. 1171 1162 1172 1163 (* Given an abstraction interpretation framework for the program *) 1173 ∀R: asm_abstract_interpretation p p' prog.1164 ∀R: asm_abstract_interpretation p p' l_p prog. 1174 1165 1175 1166 (* If the static analysis does not fail *) … … 1178 1169 (* For every measurable trace whose second state is st1 or, equivalently, 1179 1170 whose first state after the initial labelled transition is st1 *) 1180 ∀si,s1,s2,sn. ∀t: raw_trace (asm_operational_semantics … prog) … si sn.1171 ∀si,s1,s2,sn. ∀t: raw_trace l_p (asm_operational_semantics … prog) … si sn. 1181 1172 measurable … s1 s2 … t → 1182 1173 … … 1203 1194 @(proj2 … (static_analisys_ok … EQmap … Hmem)) 1204 1195 ] 1205 #p #p' # prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable1196 #p #p' #l_p #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable 1206 1197 cases measurable #s0 * #s3 * #ti0 * #t13 * #t2n* #l1 * #l2 * #prf1 * #prf2 1207 1198 ******* #pre_t13 #EQ destruct #Hl1 #Hl2 #Hcall_l2 #sil_ti0 #sil_t2n #Hcall_l1
Note: See TracChangeset
for help on using the changeset viewer.