Changeset 1929 for src/ASM/ASMCostsSplit.ma
 Timestamp:
 May 9, 2012, 2:44:39 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCostsSplit.ma
r1928 r1929 6 6 let rec traverse_code_internal 7 7 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 8 (program_counter: Word) (fixed_program_size: nat) (program_size: nat) 9 (reachable_program_counter_witness: 10 ∀lbl: costlabel. 11 ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → 12 reachable_program_counter code_memory fixed_program_size program_counter) 13 (good_program_witness: good_program code_memory fixed_program_size) 14 (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size) 15 (fixed_program_size_limit: fixed_program_size ≤ 2^16) 8 (program_counter: Word) (program_size: nat) 9 (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16) 16 10 on program_size: 17 11 Σcost_map: identifier_map CostTag nat. 18 12 (∀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) ∧ 19 13 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧ 20 ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc. 21 pi1 … (block_cost code_memory pc fixed_program_size fixed_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ 14 pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝ 22 15 match program_size return λx. x = program_size → Σcost_map: ?. ? with 23 16 [ O ⇒ λprogram_size_refl. empty_map CostTag nat 24 17  S program_size' ⇒ λprogram_size_refl. 25 18 deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in 26 let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' fixed_program_size program_size' ? good_program_witness ? fixed_program_size_limitin19 let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in 27 20 match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with 28 21 [ None ⇒ λlookup_refl. pi1 … cost_mapping 29 22  Some lbl ⇒ λlookup_refl. 30 let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size_limit cost_labels ? good_program_witness in23 let cost ≝ block_cost code_memory program_counter cost_labels in 31 24 add … cost_mapping lbl cost 32 25 ] (refl … (lookup_opt … program_counter cost_labels)) 33 26 ] (refl … program_size). 34 [5: 35 assumption 36 4: 37 @(reachable_program_counter_witness lbl) 38 @lookup_refl 39 3: 27 [3: 40 28 cases program_size_invariant 41 29 [1: … … 80 68 @succ_nat_of_bitvector_half_add_1 81 69 @le_plus_to_minus_r 82 @(transitive_le … fixed_program_size_limit)83 70 change with (S ? ≤ ?) >plus_n_Sm 71 <program_size_invariant' 84 72 @monotonic_le_plus_r 85 73 @le_S_S @le_S_S @le_O_n … … 128 116 >eq_assm >lookup_refl % 129 117 2: 130 %{(reachable_program_counter_witness …)} try assumption131 118 >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % 132 119 ] … … 142 129 cases ind_hyp' #assm #_ assumption 143 130 2: 144 cases ind_hyp' #lookup_opt_assm * #reachable_witness' 145 #ind_hyp'' %{reachable_witness'} >ind_hyp'' 131 cases ind_hyp' #lookup_opt_assm #ind_hyp'' >ind_hyp'' 146 132 @sym_eq @lookup_present_add_miss assumption 147 133 ] … … 207 193 @succ_nat_of_bitvector_half_add_1 208 194 @le_plus_to_minus_r 209 @(transitive_le … fixed_program_size_limit)210 195 change with (S ? ≤ ?) >plus_n_Sm 196 <program_size_invariant 211 197 @monotonic_le_plus_r 212 198 @le_S_S @le_S_S @le_O_n … … 228 214 @succ_nat_of_bitvector_half_add_1 229 215 @le_plus_to_minus_r 230 @(transitive_le … fixed_program_size_limit)231 216 change with (S ? ≤ ?) >plus_n_Sm 217 <program_size_invariant 232 218 @monotonic_le_plus_r 233 219 @le_S_S @le_S_S @le_O_n … … 244 230 assumption 245 231 ] 246  6:232 4: 247 233 inversion program_size' 248 234 [1: … … 262 248 @succ_nat_of_bitvector_half_add_1 263 249 @le_plus_to_minus_r 264 @(transitive_le … fixed_program_size_limit)265 250 change with (S ? ≤ ?) >plus_n_Sm 251 <relevant 266 252 @monotonic_le_plus_r 267 253 @le_S_S @le_S_S @le_O_n … … 288 274 qed. 289 275 276 (* XXX: 277 * At the moment we do a full traversal of the code memory, however we could do 278 * a fold over the domain of the cost labels map. 279 * 280 *) 290 281 definition traverse_code: 291 282 ∀code_memory: BitVectorTrie Byte 16. … … 295 286 lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → 296 287 pc = pc'. 297 ∀program_size: nat.298 ∀program_size_limit: program_size ≤ 2^16.299 ∀reachable_program_counter_witness:300 ∀lbl: costlabel.301 ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →302 reachable_program_counter code_memory program_size program_counter.303 ∀good_program_witness: good_program code_memory program_size.304 288 Σcost_map: identifier_map CostTag nat. 305 (∀pc,k. nat_of_bitvector … pc < program_size→ lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧289 (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧ 306 290 (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 307 ∃reachable_witness: reachable_program_counter code_memory program_size pc. 308 pi1 … (block_cost code_memory pc program_size program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ 291 pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝ 309 292 λcode_memory: BitVectorTrie Byte 16. 310 293 λcost_labels: BitVectorTrie costlabel 16. 311 294 λcost_labels_injective. 312 λprogram_size: nat. 313 λprogram_size_limit: program_size ≤ 2^16. 314 λreachable_program_counter_witness: 315 ∀lbl: costlabel. 316 ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → 317 reachable_program_counter code_memory program_size program_counter. 318 λgood_program_witness: good_program code_memory program_size. 319 pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness ? program_size_limit). 295 pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?). 320 296 [1: 321 297 @or_intror % 322 298 2: 323 cases (traverse_code_internal ? ? ? ? ? ? ? ??)299 cases (traverse_code_internal ?????) 324 300 #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 % 325 301 [1: … … 335 311 #k #k_pres #pc #lookup_opt_assm 336 312 cases (inductive_hypothesis2 ? k_pres) 337 #program_counter' * #lookup_opt_assm' * #reachable_witness 338 #block_cost_assm 313 #program_counter' * #lookup_opt_assm' #block_cost_assm 339 314 >(cost_labels_injective … lookup_opt_assm lookup_opt_assm') 340 %{reachable_witness}assumption315 assumption 341 316 ] 342 317 ] … … 350 325 lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → 351 326 pc = pc'. 352 λreachable_program_witness.353 λgood_program_witness: good_program (load_code_memory program) (program).354 λprogram_size_limit: program ≤ 2^16.355 327 let program_size ≝ program in 356 328 let code_memory ≝ load_code_memory program in 357 traverse_code code_memory cost_labels cost_labels_injective program_size program_size_limit reachable_program_witness good_program_witness.329 traverse_code code_memory cost_labels cost_labels_injective.
Note: See TracChangeset
for help on using the changeset viewer.