 Timestamp:
 May 8, 2012, 3:29:25 PM (9 years ago)
 Location:
 src
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1919 r1921 113 113 program_counter ? code_memory after = program_counter_after. 114 114 115 lemma eq_bv_true_to_refl: 116 ∀n: nat. 117 ∀x: BitVector n. 118 ∀y: BitVector n. 119 eq_bv n x y = true → x = y. 120 #n #x #y 121 cases daemon (* XXX: !!! *) 122 qed. 123 124 lemma refl_to_eq_bv_true: 125 ∀n: nat. 126 ∀x: BitVector n. 127 ∀y: BitVector n. 128 x = y → eq_bv n x y = true. 129 #n #x #y #refl destruct /2/ 130 qed. 131 132 corollary refl_iff_eq_bv_true: 133 ∀n: nat. 134 ∀x: BitVector n. 135 ∀y: BitVector n. 136 eq_bv n x y = true ↔ x = y. 137 #n #x #y whd in match iff; normalize nodelta 138 @conj /2/ 139 qed. 140 141 definition word_deqset: DeqSet ≝ 142 mk_DeqSet Word (eq_bv 16) ?. 143 @refl_iff_eq_bv_true 144 qed. 145 115 146 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝ 116 147 λcode_memory. … … 119 150 (Status code_memory) 120 151 (λs,s'. (execute_1 … s) = s') 121 ?122 ?152 word_deqset 153 (program_counter …) 123 154 (λs,class. ASM_classify … s = class) 124 155 (current_instruction_is_labelled … cost_labels) 125 156 (next_instruction_properly_relates_program_counters code_memory) 126 157 ?. 127 cases daemon (* XXX: new additions to abstract status record*)158 cases daemon (* XXX: is final predicate *) 128 159 qed. 129 160 … … 156 187 λthe_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status. 157 188 as_trace_any_label_length' … the_trace. 189 190 let rec all_program_counter_list 191 (n: nat) 192 on n ≝ 193 match n with 194 [ O ⇒ [ ] 195  S n' ⇒ (bitvector_of_nat 16 n')::(all_program_counter_list n') 196 ]. 197 198 lemma all_program_counter_list_bound_eq: 199 ∀bound: nat. 200 all_program_counter_list bound = bound. 201 #bound elim bound try % 202 #bound' #inductive_hypothesis normalize 203 >inductive_hypothesis % 204 qed. 205 206 axiom nat_of_bitvector_bitvector_of_nat_inverse: 207 ∀n: nat. 208 ∀b: nat. 209 b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b. 210 211 axiom bitvector_of_nat_inverse_nat_of_bitvector: 212 ∀n: nat. 213 ∀b: BitVector n. 214 bitvector_of_nat n (nat_of_bitvector n b) = b. 215 216 lemma mem_all_program_counter_list_lt_bound: 217 ∀bound: nat. 218 ∀bound_proof: bound ≤ 2^16. 219 ∀e: Word. 220 memb word_deqset e (all_program_counter_list bound) = true → 221 nat_of_bitvector … e < bound. 222 #bound elim bound 223 [1: 224 #bound_proof #e 225 normalize #absurd destruct(absurd) 226 2: 227 #bound' #inductive_hypothesis 228 #bound_proof #e 229 change with (if eq_bv ??? then ? else ? = ? → ?) 230 @eq_bv_elim 231 [1: 232 #eq_assm 233 normalize nodelta destruct #_ 234 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 235 normalize % 236 2: 237 #neq_assm normalize nodelta 238 #memb_assm %2 @inductive_hypothesis 239 try assumption 240 @(transitive_le bound' (S bound')) 241 try assumption %2 % 242 ] 243 ] 244 qed. 245 246 lemma lt_bound_mem_all_program_counter_list: 247 ∀bound: nat. 248 ∀bound_proof: bound ≤ 2^16. 249 ∀e: Word. 250 nat_of_bitvector … e < bound → 251 memb word_deqset e (all_program_counter_list bound) = true. 252 #bound elim bound 253 [1: 254 #bound_proof #e normalize 255 #absurd cases (lt_to_not_zero … absurd) 256 2: 257 #bound' #inductive_hypothesis 258 #bound_proof #e 259 change with (? → if eq_bv ??? then ? else ? = ?) 260 #assm 261 cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?) 262 [1: 263 #e_lt_assm 264 @eq_bv_elim 265 [1: 266 #eq_assm normalize nodelta % 267 2: 268 #neq_assm normalize nodelta 269 @inductive_hypothesis try assumption 270 @(transitive_le bound' (S bound')) try assumption 271 %2 % 272 ] 273 2: 274 #relevant >eq_eq_bv normalize nodelta try % 275 destruct >bitvector_of_nat_inverse_nat_of_bitvector % 276 3: 277 normalize in assm; 278 @le_S_S_to_le assumption 279 ] 280 ] 281 qed. 282 283 include alias "arithmetics/nat.ma". 284 285 lemma fetch_program_counter_n_Sn: 286 ∀instruction: instruction. 287 ∀program_counter, program_counter': Word. 288 ∀ticks, n: nat. 289 ∀code_memory: BitVectorTrie Byte 16. 290 Some … program_counter = fetch_program_counter_n n code_memory (zero 16) → 291 〈instruction,program_counter',ticks〉 = fetch code_memory program_counter → 292 nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' → 293 Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …). 294 #instruction #program_counter #program_counter' #ticks #n #code_memory 295 #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp 296 whd in match (fetch_program_counter_n (S n) code_memory (zero …)); 297 <fetch_program_counter_n_hyp normalize nodelta 298 <fetch_hyp normalize nodelta 299 change with ( 300 leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter') 301 ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter')); 302 >(le_to_leb_true … lt_hyp) % 303 qed. 304 305 (* XXX: indexing bug *) 306 lemma execute_1_and_program_counter_after_other_in_lockstep: 307 ∀code_memory: BitVectorTrie Byte 16. 308 ∀start_status: Status code_memory. 309 ASM_classify code_memory start_status = cl_other → 310 let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in 311 program_counter ? ? (execute_1 … start_status) = 312 program_counter_after_other pc instruction. 313 #code_memory #start_status #classify_assm 314 whd in match execute_1; normalize nodelta 315 cases (execute_1' code_memory start_status) #the_status 316 * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm; 317 cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks 318 #classify_assm #classify_assm' @classify_assm' assumption 319 qed. 320 321 let rec tal_pc_list_lt_total_program_size 322 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 323 (total_program_size: nat) (total_program_size_invariant: total_program_size ≤ 2^16) 324 (good_program_witness: good_program code_memory total_program_size) 325 (start: Status code_memory) (final: Status code_memory) (trace_ends_flag: trace_ends_with_ret) 326 (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final) 327 (pc: as_pc (ASM_abstract_status code_memory cost_labels)) 328 on the_trace: 329 reachable_program_counter code_memory total_program_size (program_counter … start) → 330 memb word_deqset pc (tal_pc_list (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace) = true → 331 nat_of_bitvector 16 pc<total_program_size ≝ 332 match the_trace with 333 [ tal_base_not_return the_status _ _ _ _ ⇒ ? 334  tal_base_return the_status _ _ _ ⇒ ? 335  tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ ? 336  tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final 337 _ classifier after_return call_trace _ final_trace ⇒ ? 338  tal_step_default end_flag status_pre status_init status_end execute tail_trace classifier _ ⇒ ? 339 ]. 340 #reachable_program_counter_witness 341 whd in ⊢ (??%? → ?); @(bool_inv_ind … (pc==as_pc_of (ASM_abstract_status code_memory cost_labels) ?)) 342 normalize nodelta #eq_assm cases reachable_program_counter_witness 343 [1,3,5,7,9: 344 >(eq_bv_eq … eq_assm) #_ #relevant #_ 345 assumption 346 2,4,6: 347 #_ #_ #absurd 348 normalize in absurd; destruct(absurd) 349 8: 350 #Some_assm #tps_lt_assm @tal_pc_list_lt_total_program_size try assumption 351 whd in after_return; 352 lapply after_return 353 @pair_elim * normalize nodelta #instruction #pc' #ticks 354 #fetch_eq #pc_assm' >pc_assm' 355 lapply (good_program_witness ? reachable_program_counter_witness) 356 whd in classifier; whd in classifier:(??%?); 357 whd in match (current_instruction ??) in classifier; 358 whd in match current_instruction0 in classifier; 359 >fetch_eq in classifier; 360 normalize nodelta cases instruction 361 normalize nodelta tal_pc_list_lt_total_program_size 362 [8: 363 #preinstruction elim preinstruction 364 normalize in match (? = cl_call); 365 ] 366 try (#assm1 #assm2 #absurd destruct(absurd) @I) 367 try (#assm1 #absurd destruct(absurd) @I) 368 try (#absurd destruct(absurd) @I) 369 [1: 370 #addr #_ 371 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] 372 #w 373 @pair_elim #lft #rgt @pair_elim #lft' #rgt' @pair_elim #lft'' #rgt'' 374 #_ #_ #_ * * #_ 375 2: 376 #addr #_ 377 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] 378 #w * * #_ 379 3: 380 #addr #_ * 381 ] 382 #relevant #pc_tps_assm' 383 whd cases reachable_program_counter_witness * #n 384 #Some_assm #_ % try assumption 385 %{(S n)} 386 @(fetch_program_counter_n_Sn … Some_assm (sym_eq … fetch_eq)) 387 assumption 388 10: 389 #Some_assm #tps_lt_assm @tal_pc_list_lt_total_program_size try assumption tal_pc_list_lt_total_program_size 390 lapply (execute_1_and_program_counter_after_other_in_lockstep … status_pre classifier) 391 @pair_elim * #instruction #pc #ticks normalize nodelta 392 #fetch_eq whd in match program_counter_after_other; normalize nodelta 393 lapply (good_program_witness … reachable_program_counter_witness) 394 whd in classifier; whd in classifier:(??%?); 395 whd in match (current_instruction ??) in classifier; 396 whd in match current_instruction0 in classifier; 397 >fetch_eq in classifier; normalize nodelta cases instruction 398 normalize nodelta 399 [8: 400 #preinstruction elim preinstruction 401 normalize in match (? = cl_other); 402 ] 403 try (#assm1 #assm2 #absurd destruct(absurd) @I) 404 try (#assm1 #absurd destruct(absurd) @I) 405 try (#absurd destruct(absurd) @I) normalize nodelta 406 [27,28,29: 407 #addr #_ #reachable 408 #program_counter_execute_1_refl 409 whd in execute; <execute 410 >program_counter_execute_1_refl assumption 411 *: 412 try (#assm1 #assm2 #_ * #relevant #pc_lt_assm) 413 try (#assm1 #_ * #relevant #pc_lt_assm) 414 try (#_ * #relevant #pc_lt_assm) #pc_refl 415 cases reachable_program_counter_witness * #n 416 #Some_assm #tps_lt_assm 417 whd in match reachable_program_counter; normalize nodelta % 418 try %{(S n)} 419 whd in execute; <execute 420 try (@(fetch_program_counter_n_Sn instruction ?? ticks ?? Some_assm ?) >execute >fetch_eq <pc_refl >execute try %) 421 <pc_refl in relevant; <execute #assm 422 >pc_refl >pc_refl in assm; #assm assumption 423 ] 424 ] 425 qed. 426 427 lemma sublist_tal_pc_list_all_program_counter_list: 428 ∀code_memory: BitVectorTrie Byte 16. 429 ∀cost_labels: BitVectorTrie costlabel 16. 430 ∀total_program_size: nat. 431 ∀total_program_size_invariant: total_program_size ≤ 2^16. 432 ∀good_program_witness: good_program code_memory total_program_size. 433 ∀start, final: Status code_memory. 434 ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size 435 (program_counter (BitVectorTrie Byte 16) code_memory start). 436 ∀trace_ends_flag. 437 ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final. 438 sublist ? (tal_pc_list … the_trace) (all_program_counter_list total_program_size). 439 #code_memory #cost_labels #total_program_size #total_program_size_invariant 440 #good_program_witness #start #final #reachable_program_counter_witness 441 #trace_ends_flag #the_trace 442 whd in match (sublist ???); #pc #memb_assm 443 @lt_bound_mem_all_program_counter_list 444 try assumption destruct 445 lapply memb_assm memb_assm 446 @tal_pc_list_lt_total_program_size 447 assumption 448 qed. 449 450 corollary tal_pc_list_length_leq_total_program_size: 451 ∀code_memory: BitVectorTrie Byte 16. 452 ∀cost_labels: BitVectorTrie costlabel 16. 453 ∀total_program_size: nat. 454 ∀total_program_size_invariant: total_program_size ≤ 2^16. 455 ∀good_program_witness: good_program code_memory total_program_size. 456 ∀start, final: Status code_memory. 457 ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size 458 (program_counter (BitVectorTrie Byte 16) code_memory start). 459 ∀trace_ends_flag. 460 ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final. 461 ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace. 462 tal_pc_list … the_trace ≤ total_program_size. 463 #code_memory #cost_labels #total_program_size #total_program_size_invariant 464 #good_program_witness #start #final #reachable_program_counter_witness 465 #trace_ends_flag #the_trace #unrepeating_witness 466 <(all_program_counter_list_bound_eq total_program_size) 467 @sublist_length 468 [1: 469 @tal_unrepeating_uniqueb 470 assumption 471 2: 472 @sublist_tal_pc_list_all_program_counter_list 473 assumption 474 ] 475 qed. 158 476 159 477 let rec compute_paid_trace_any_label … … 214 532 #m #n #proof /2 by plus_minus/ 215 533 qed. 216 217 (* XXX: indexing bug *)218 lemma execute_1_and_program_counter_after_other_in_lockstep:219 ∀code_memory: BitVectorTrie Byte 16.220 ∀start_status: Status code_memory.221 ASM_classify code_memory start_status = cl_other →222 let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in223 program_counter ? ? (execute_1 … start_status) =224 program_counter_after_other pc instruction.225 #code_memory #start_status #classify_assm226 whd in match execute_1; normalize nodelta227 cases (execute_1' code_memory start_status) #the_status228 * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;229 cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks230 #classify_assm #classify_assm' @classify_assm' assumption231 qed.232 534 233 535 lemma reachable_program_counter_to_0_lt_total_program_size: … … 878 1180 ∀program_counter': Word. 879 1181 ∀total_program_size: nat. 1182 ∀total_program_size_invariant: total_program_size ≤ 2^16. 880 1183 ∀cost_labels: BitVectorTrie costlabel 16. 881 1184 ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'. … … 886 1189 ∀trace_ends_flag. 887 1190 ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. 888 trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace889 ≤ total_program_size →1191 ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size (program_counter (BitVectorTrie Byte 16) code_memory' start_status). 1192 ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status the_trace. 890 1193 program_counter' = program_counter … start_status → 891 1194 cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝ … … 893 1196 λprogram_counter: Word. 894 1197 λtotal_program_size: nat. 1198 λtotal_program_size_invariant: total_program_size ≤ 2^16. 895 1199 λcost_labels: BitVectorTrie costlabel 16. 896 1200 λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter. … … 902 1206 cases(lookup_opt … cost_labels) in block_cost_hyp; 903 1207 [2: #cost_label] normalize nodelta 904 #hyp assumption 905 qed. 906 907 lemma fetch_program_counter_n_Sn: 908 ∀instruction: instruction. 909 ∀program_counter, program_counter': Word. 910 ∀ticks, n: nat. 911 ∀code_memory: BitVectorTrie Byte 16. 912 Some … program_counter = fetch_program_counter_n n code_memory (zero 16) → 913 〈instruction,program_counter',ticks〉 = fetch code_memory program_counter → 914 nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' → 915 Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …). 916 #instruction #program_counter #program_counter' #ticks #n #code_memory 917 #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp 918 whd in match (fetch_program_counter_n (S n) code_memory (zero …)); 919 <fetch_program_counter_n_hyp normalize nodelta 920 <fetch_hyp normalize nodelta 921 change with ( 922 leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter') 923 ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter')); 924 >(le_to_leb_true … lt_hyp) % 1208 #hyp #start_status #final_status #trace_ends_flag #the_trace 1209 #reachable_program_counter_witness #unrepeating_witness 1210 @hyp @tal_pc_list_length_leq_total_program_size try assumption 925 1211 qed. 926 1212 
src/ASM/ASMCostsSplit.ma
r1919 r1921 40 40 match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒ 41 41 λ${ident E}.$s ] ] (refl ? $t) }. 42 43 definition nat_of_bool: bool → nat ≝ 44 λb: bool. 45 match b with 46 [ true ⇒ 1 47  false ⇒ 0 48 ]. 49 50 lemma blah: 51 ∀n: nat. 52 ∀bv: BitVector n. 53 ∀buffer: nat. 54 nat_of_bitvector_aux n buffer bv = nat_of_bitvector n bv + (buffer * 2^n). 55 #n #bv elim bv 56 [1: 57 #buffer elim buffer try % 58 #buffer' #inductive_hypothesis 59 normalize <times_n_1 % 60 2: 61 #n' #hd #tl #inductive_hypothesis 62 #buffer cases hd normalize 63 >inductive_hypothesis 64 >inductive_hypothesis 65 [1: 66 change with ( 67 ? + (2 * buffer + 1) * ?) in ⊢ (??%?); 68 change with ( 69 ? + buffer * (2 * 2^n')) in ⊢ (???%); 70 cases daemon 71 ] 72 ] 73 cases daemon 74 qed. 75 76 lemma nat_of_bitvector_aux_hd_tl: 77 ∀n: nat. 78 ∀tl: BitVector n. 79 ∀hd: bool. 80 nat_of_bitvector (S n) (hd:::tl) = 81 nat_of_bitvector n tl + (nat_of_bool hd * 2^n). 82 #n #tl elim tl 83 [1: 84 #hd cases hd % 85 2: 86 #n' #hd' #tl' #inductive_hypothesis #hd 87 cases hd whd in ⊢ (??%?); normalize nodelta 88 >inductive_hypothesis cases hd' normalize nodelta 89 normalize in match (nat_of_bool ?); 90 normalize in match (nat_of_bool ?); 91 [4: 92 normalize in match (2 * ?); 93 <plus_n_O <plus_n_O % 94 3: 95 normalize in match (2 * ?); 96 normalize in match (0 + 1); 97 <plus_n_O 98 normalize in match (1 * ?); 99 <plus_n_O 100 cases daemon 101 (* XXX: lemma *) 102 *: 103 cases daemon 104 ] 105 ] 106 qed. 42 107 43 108 lemma succ_nat_of_bitvector_aux_half_add_1: … … 74 139 qed. 75 140 141 include alias "arithmetics/nat.ma". 142 include alias "basics/logic.ma". 143 76 144 let rec traverse_code_internal 77 145 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) … … 89 157 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧ 90 158 ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc. 91 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝159 pi1 … (block_cost code_memory pc fixed_program_size fixed_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ 92 160 match program_size return λx. x = program_size → Σcost_map: ?. ? with 93 161 [ O ⇒ λprogram_size_refl. empty_map CostTag nat … … 98 166 [ None ⇒ λlookup_refl. pi1 … cost_mapping 99 167  Some lbl ⇒ λlookup_refl. 100 let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in168 let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size_limit cost_labels ? good_program_witness in 101 169 add … cost_mapping lbl cost 102 170 ] (refl … (lookup_opt … program_counter cost_labels)) … … 395 463 (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 396 464 ∃reachable_witness: reachable_program_counter code_memory program_size pc. 397 pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝465 pi1 … (block_cost code_memory pc program_size program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ 398 466 λcode_memory: BitVectorTrie Byte 16. 399 467 λcost_labels: BitVectorTrie costlabel 16. 
src/ASM/CostsProof.ma
r1919 r1921 594 594 (* XXX: here *) 595 595 let rec compute_trace_label_return_using_paid_ok_with_trace 596 (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size) 596 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16) 597 (good_program_witness: good_program cm total_program_size) 597 598 (cost_labels: BitVectorTrie costlabel 16) 598 599 (cost_map: identifier_map CostTag nat) … … 601 602 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k)) 602 603 on trace: 604 ∀unrepeating_witness: tlr_unrepeating … trace. 603 605 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 604 606 ∃reachable_witness: reachable_program_counter cm total_program_size pc. 605 pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).607 pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres). 606 608 let ctrace ≝ compute_cost_trace_label_return cm … trace in 607 609 compute_trace_label_return_cost_using_paid cm … trace = … … 609 611 ≝ ? 610 612 and compute_trace_any_label_using_paid_ok_with_trace 611 (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size) 613 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16) 614 (good_program_witness: good_program cm total_program_size) 612 615 (cost_labels: BitVectorTrie costlabel 16) 613 616 (trace_ends_flag: trace_ends_with_ret) … … 618 621 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 619 622 ∃reachable_witness: reachable_program_counter cm total_program_size pc. 620 pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))623 pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres)) 621 624 on trace: 625 ∀unrepeating_witness: tal_unrepeating … trace. 622 626 let ctrace ≝ compute_cost_trace_any_label … trace in 623 627 compute_trace_any_label_cost_using_paid … trace = … … 625 629 ≝ ? 626 630 and compute_trace_label_label_using_paid_ok_with_trace 627 (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size) 631 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16) 632 (good_program_witness: good_program cm total_program_size) 628 633 (cost_labels: BitVectorTrie costlabel 16) 629 634 (trace_ends_flag: trace_ends_with_ret) … … 631 636 (initial: Status cm) (final: Status cm) 632 637 (trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final) 638 (unrepeating_witness: tll_unrepeating … trace) 633 639 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k)) 634 640 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 635 641 ∃reachable_witness: reachable_program_counter cm total_program_size pc. 636 pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))642 pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres)) 637 643 on trace: 644 ∀unrepeating_witness: tll_unrepeating … trace. 638 645 let ctrace ≝ compute_cost_trace_label_label … trace in 639 646 compute_trace_label_label_cost_using_paid … trace = … … 641 648 ≝ ?. 642 649 cases trace normalize nodelta 643 [ #sb #sa #tr # dom_codom whd in ⊢ (??%?);650 [ #sb #sa #tr #unrepeating_witness #dom_codom whd in ⊢ (??%?); 644 651 whd in match (compute_cost_trace_label_return ?????); 645 @(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness) @dom_codom 646  #si #sl #sf #tr1 #tr2 #dom_codom 652 @(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness) 653 assumption 654  #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom 647 655 whd in ⊢ (??%?); 648 656 whd in match (compute_cost_trace_label_return ?????); 649 657 >append_length >bigop_sum_rev >commutative_plus @eq_f2 650 [ >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)658 [ >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom) 651 659 compute_trace_label_return_using_paid_ok_with_trace 652 @same_bigop [//] #i #H #_ dom_codom @tech_cost_of_label_shift // 660 [1: 661 @same_bigop [//] #i #H #_ dom_codom @tech_cost_of_label_shift // 662 2: 663 inversion unrepeating_witness 664 #tll_unrepeating #tlr_unrepeating #_ assumption 665 ] 653 666  >(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom) 654 667 compute_trace_label_label_using_paid_ok_with_trace 655 @same_bigop [//] #i #H #_ @(tech_cost_of_label_prefix … H) 668 [1: 669 @same_bigop [//] #i #H #_ @(tech_cost_of_label_prefix … H) 670 2,3: 671 inversion unrepeating_witness 672 #tll_unrepeating #tlr_unrepeating #_ assumption 673 ] 656 674 ] 657 675 8: 658 676 #end_flag #start_status #end_status #trace_any_label #costed_assm 677 #unrepeating_witness 659 678 whd in ⊢ (??%?); whd in ⊢ (??(?%?)?); 660 679 >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom) 661 >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2662 680 [1: 663 @same_bigop [//] #i #H #_ dom_codom >(plus_n_O i) >plus_n_Sm 664 <(tech_cost_of_label_shift ??? [?] ? i) // 681 >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2 682 [1: 683 @same_bigop [//] #i #H #_ dom_codom >(plus_n_O i) >plus_n_Sm 684 <(tech_cost_of_label_shift ??? [?] ? i) // 685 2: 686 change with (? = lookup_present ? ? ? ? ?) 687 generalize in match (tech_cost_of_label0 ? ? ? ? ? ?); 688 normalize in match (nth_safe ? ? ? ?); 689 whd in costed_assm; lapply costed_assm costed_assm 690 inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels) 691 [1: 692 #_ #absurd cases absurd 693 2: 694 normalize nodelta #cost_label #Some_assm #_ #p 695 cases (dom_codom ? p ? Some_assm) 696 #reachable_witness #block_cost_assm <block_cost_assm 697 cases (block_cost ???????) 698 #cost block_cost_assm #block_cost_assm 699 cases (block_cost_assm ??? trace_any_label ???) 700 try @refl 701 [1: 702 assumption 703 2: 704 (* XXX: !!! *) 705 cases daemon 706 ] 707 ] 708 ] 665 709 2: 666 change with (? = lookup_present ? ? ? ? ?) 667 generalize in match (tech_cost_of_label0 ? ? ? ? ? ?); 668 normalize in match (nth_safe ? ? ? ?); 669 whd in costed_assm; lapply costed_assm costed_assm 670 inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels) 671 [1: 672 #_ #absurd cases absurd 673 2: 674 normalize nodelta #cost_label #Some_assm #_ #p 675 cases (dom_codom ? p ? Some_assm) 676 #reachable_witness #block_cost_assm <block_cost_assm 677 cases (block_cost ? ? ? ? ? ?) 678 #cost block_cost_assm #block_cost_assm 679 cases (block_cost_assm ? ? ? trace_any_label ? (refl …)) 680 try % (* XXX: assumption about length of trace *) cases daemon 681 ] 710 assumption 682 711 ] 683 712 3: 684 713 #start_status #final_status #execute_assm #classifier_assm #costed_assm 714 #unrepeating_witness 685 715 % 686 716 4: 687 #start_status #final_status #execute_assm #classifier_assm % 717 #start_status #final_status #execute_assm #classifier_assm #unrepeating_witness 718 % 688 719 5: 689 720 #status_pre_fun_call #status_start_fun_call #status_final #execute_assm 690 #classifier_assm #after_return_assm #trace_label_return #costed_assm 721 #classifier_assm #after_return_assm #trace_label_return #costed_assm #unrepeating_witness 691 722 whd in ⊢ (??%?); 692 @(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom) 723 @(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom) 724 assumption 693 725 6: 694 726 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 695 727 #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return 696 #costed_assm #trace_any_label 728 #costed_assm #trace_any_label #unrepeating_witness 697 729 whd in ⊢ (??%?); 698 >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom) 699 >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom) 700 >length_append >bigop_sum_rev >commutative_plus @eq_f2 701 [ @same_bigop [2: #i #H #_ dom_codom @tech_cost_of_label_shift assumption 702 1: #i #H % ] 703  @same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H) 730 >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom) 731 [1: 732 >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom) 733 [1: 734 >length_append >bigop_sum_rev >commutative_plus @eq_f2 735 [ @same_bigop [2: #i #H #_ dom_codom @tech_cost_of_label_shift assumption 736 1: #i #H % ] 737  @same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H) 738 ] 739 2: 740 inversion unrepeating_witness 741 * #memb_1 #tal_unrepeating #tlr_unrepeating #_ assumption 742 ] 743 2: 744 inversion unrepeating_witness 745 * #memb_1 #tal_unrepeating #tlr_unrepeating #_ assumption 704 746 ] 705 747 7: 706 748 #end_flag #status_pre_fun_call #status_start_fun_call #status_final 707 #execute_assm #trace_any_label #classifier_assm #costed_assm 749 #execute_assm #trace_any_label #classifier_assm #costed_assm #unrepeating_witness 708 750 whd in ⊢ (??%?); 709 751 @(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom) 752 inversion unrepeating_witness 753 #memb_1 #tal_unrepeating #_ assumption 710 754 ] 711 755 qed. … … 714 758 ∀code_memory: BitVectorTrie Byte 16. 715 759 ∀total_program_size: nat. 760 ∀total_program_size_limit: total_program_size ≤ 2^16. 716 761 ∀good_program_witness: good_program code_memory total_program_size. 717 762 ∀cost_labels: BitVectorTrie costlabel 16. … … 720 765 ∀final: Status code_memory. 721 766 ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final. 767 ∀unrepeating_witness: tlr_unrepeating … trace. 722 768 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). 723 769 ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 724 770 ∃reachable_witness: reachable_program_counter code_memory total_program_size pc. 725 pi1 … (block_cost code_memory pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).771 pi1 … (block_cost code_memory pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres). 726 772 let ctrace ≝ compute_cost_trace_label_return code_memory … trace in 727 773 clock … code_memory … final = 728 774 clock … code_memory … initial + (Σ_{i < ctrace} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)). 729 #code_memory #total_program_size #good_program_witness #cost_labels #cost_map 730 #initial #final #trace #codom_dom #dom_codom normalize nodelta 775 #code_memory #total_program_size #total_program_size_limit 776 #good_program_witness #cost_labels #cost_map 777 #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta 731 778 <compute_trace_label_return_using_paid_ok_with_trace try assumption 732 779 >commutative_plus >compute_trace_label_return_cost_using_paid_ok // … … 751 798 ∀final: Status code_memory. 752 799 ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final. 800 ∀unrepeating_witness: tlr_unrepeating … trace. 753 801 let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective total_program_size total_program_size_invariant 754 802 reachable_program_counter_witness good_program_witness in … … 758 806 #code_memory #total_program_size #total_program_size_invariant #good_program_witness 759 807 #cost_labels #cost_labels_injective #reachable_program_counter_witness #initial #final #trace 808 #unrepeating_witness 760 809 @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption 761 810 2: 
src/common/StructuredTraces.ma
r1918 r1921 12 12 13 13 record abstract_status : Type[1] ≝ 14 { as_status :> Type[0] 14 { 15 as_status :> Type[0] 15 16 ; as_execute : as_status → as_status → Prop 16 17 ; as_pc : DeqSet … … 112 113  tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre] 113 114 ]. 115 116 definition as_trace_any_label_length': 117 ∀S: abstract_status. 118 ∀trace_ends_flag: trace_ends_with_ret. 119 ∀start_status: S. 120 ∀final_status: S. 121 ∀the_trace: trace_any_label S trace_ends_flag start_status final_status. 122 nat ≝ 123 λS: abstract_status. 124 λtrace_ends_flag: trace_ends_with_ret. 125 λstart_status: S. 126 λfinal_status: S. 127 λthe_trace: trace_any_label S trace_ends_flag start_status final_status. 128 tal_pc_list … the_trace. 114 129 115 130 let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝ … … 131 146 bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧ 132 147 tal_unrepeating … tl 148  tal_base_call status_pre_fun_call status_start_fun_call status_final _ _ _ 149 fun_call_trace _ ⇒ tlr_unrepeating … fun_call_trace 133 150  _ ⇒ True 134 151 ].
Note: See TracChangeset
for help on using the changeset viewer.