Changeset 2907 for src/ASM/ASMCostsSplit.ma
 Timestamp:
 Mar 19, 2013, 7:48:19 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCostsSplit.ma
r2899 r2907 6 6 7 7 let rec traverse_code_internal 8 ( code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)8 (prog: labelled_object_code) 9 9 (program_counter: Word) (program_size: nat) 10 10 (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16) 11 11 on program_size: 12 12 Σcost_map: identifier_map CostTag nat. 13 (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels= Some … k → present … cost_map k) ∧14 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels= Some … k ∧15 pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝13 (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k) ∧ 14 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc (costlabels prog) = Some … k ∧ 15 pi1 … (block_cost prog pc) = lookup_present … k_pres) ≝ 16 16 match program_size return λx. x = program_size → Σcost_map: ?. ? with 17 17 [ O ⇒ λprogram_size_refl. empty_map CostTag nat 18 18  S program_size' ⇒ λprogram_size_refl. 19 19 let new_program_counter' ≝ add 16 (bitvector_of_nat 16 1) program_counter in 20 let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in 21 match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with 20 let cost_mapping ≝ traverse_code_internal prog new_program_counter' program_size' ? in 21 match lookup_opt … program_counter (costlabels prog) 22 return λx. x = lookup_opt … program_counter (costlabels prog) → Σcost_map: ?. ? with 22 23 [ None ⇒ λlookup_refl. pi1 … cost_mapping 23 24  Some lbl ⇒ λlookup_refl. 24 let cost ≝ block_cost code_memory program_counter cost_labelsin25 let cost ≝ block_cost prog program_counter in 25 26 cic:/matita/cerco/common/Identifiers/add.fix(0,2,3) ?? cost_mapping lbl cost 26 ] (refl … (lookup_opt … program_counter cost_labels))27 ] (refl … (lookup_opt … program_counter (costlabels prog))) 27 28 ] (refl … program_size). 28 29 [3: … … 279 280 *) 280 281 definition traverse_code: 281 ∀code_memory: BitVectorTrie Byte 16. 282 ∀cost_labels: BitVectorTrie costlabel 16. 283 ∀cost_labels_injective: 284 ∀pc, pc',l. 285 lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → 286 pc = pc'. 282 ∀prog: labelled_object_code. 283 let cost_labels ≝ costlabels prog in 287 284 Σcost_map: identifier_map CostTag nat. 288 285 (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧ 289 286 (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 290 pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝ 291 λcode_memory: BitVectorTrie Byte 16. 292 λcost_labels: BitVectorTrie costlabel 16. 293 λcost_labels_injective. 294 pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?). 287 pi1 … (block_cost prog pc) = lookup_present … k_pres) ≝ 288 λprog. 289 pi1 ? ? (traverse_code_internal prog (zero …) (2^16) ?). 295 290 [1: 296 291 @or_intror % 297 292 2: 298 cases (traverse_code_internal ??? ??)293 cases (traverse_code_internal ???) 299 294 #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 % 300 295 [1: … … 311 306 cases (inductive_hypothesis2 ? k_pres) 312 307 #program_counter' * #lookup_opt_assm' #block_cost_assm 313 >( cost_labels_injective… lookup_opt_assm lookup_opt_assm')308 >(oc_injective_costlabels … lookup_opt_assm lookup_opt_assm') 314 309 assumption 315 310 ] … … 317 312 qed. 318 313 319 definition compute_costs ≝ 320 λprogram: object_code. 321 λcost_labels: BitVectorTrie costlabel 16. 322 λcost_labels_injective: 323 ∀pc, pc',l. 324 lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → 325 pc = pc'. 326 (* let program_size ≝ program in *) 327 let code_memory ≝ load_code_memory program in 328 traverse_code code_memory cost_labels cost_labels_injective. 314 definition compute_costs ≝ traverse_code. 329 315 330 316 definition ASM_cost_map : 331 317 ∀p: labelled_object_code. 332 318 let code_memory ≝ load_code_memory (oc p) in 333 let a_s ≝ OC_abstract_status code_memory (costlabels p)in319 let a_s ≝ OC_abstract_status p in 334 320 as_cost_map a_s ≝ 335 321 λp. 336 let cost_map ≝ compute_costs (oc p) (costlabels p) (oc_injective_costlabels … p)in322 let cost_map ≝ compute_costs p in 337 323 λl_sig. 338 324 lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
Note: See TracChangeset
for help on using the changeset viewer.