Changeset 1899
 Timestamp:
 Apr 23, 2012, 6:10:51 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCostsSplit.ma
r1897 r1899 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 (*44 lemma test:45 ∀b: nat.46 ∀c: nat × nat.47 Σx: nat. ∃y: nat. c = 〈y, x〉 ≝48 λb: nat.49 λc: nat × nat.50 match b return λb': nat. ∀r:b' = b. Σx: ?. ? with51 [ O ⇒ λr.52 let 〈left, right〉 as T return Σz:nat.∃y. c = 〈y,z〉 ≝ c in53 deplet 〈left', right'〉 as T' ≝ c in left'54  S n ⇒ λr. deplet 〈left, right〉 as T ≝ c in left55 ] (refl … b).56 57 lemma test:58 ∀b: nat.59 ∀c: nat × nat.60 Σx: nat. ∃y: nat. c = 〈y, x〉 ≝61 λb: nat.62 λc: nat × nat.63 match b return λb': nat. b' = b → Σx: ?. ? with64 [ O ⇒ λr.65 deplet 〈left, right〉 as T ≝ c in66 deplet 〈left', right'〉 as T' ≝ c in67 left'68  S n ⇒ λr. deplet 〈left, right〉 as T ≝ c in left69 ] (refl … b).70 71 lemma test:72 ∀b: nat.73 ∀c: nat × nat × nat.74 Σx: nat. ∃y: nat × nat. c = 〈y, x〉 ≝75 λb: nat.76 λc: nat × nat × nat.77 match b return λb': nat. b' = b → Σx: ?. ? with78 [ O ⇒ λr.79 deplet 〈left, centre, right〉 as T ≝ c in80 deplet 〈left', centre', right'〉 as T' ≝ c in81 left'82  S n ⇒ λr. deplet 〈left, centre, right〉 as T ≝ c in left83 ] (refl … b).84 85 lemma pair_elim_as:86 ∀A,B,C: Type[0].87 ∀p.88 ∀T: ∀a: A. ∀b: B. 〈a, b〉 = p → C.89 ∀P: A×B → C → Prop.90 (∀lft, rgt. ∀H: 〈lft,rgt〉 = p. P 〈lft,rgt〉 (T lft rgt H)) →91 P p (let 〈lft, rgt〉 as H ≝ p in T lft rgt H).92 #A #B #C * /2/93 qed.94 95 lemma triple_elim_as:96 ∀A,B,C,D: Type[0].97 ∀p.98 ∀T: ∀a: A. ∀b: B. ∀c: C. 〈a, b, c〉 = p → D.99 ∀P: A×B×C → D → Prop.100 (∀lft, cntr, rgt. ∀H: 〈lft,cntr,rgt〉 = p. P 〈lft,cntr,rgt〉 (T lft cntr rgt H)) →101 P p (let 〈lft, cntr, rgt〉 as H ≝ p in T lft cntr rgt H).102 #A #B #C #D * * /2/103 qed. *)104 105 42 106 43 let rec traverse_code_internal … … 117 54 Σcost_map: identifier_map CostTag nat. 118 55 (∀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) ∧ 119 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →56 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧ 120 57 ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc. 121 58 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ … … 224 161 @(eq_identifier_elim … k lbl) 225 162 [1: 226 #eq_assm %{program_counter} #lookup_opt_assm 227 %{(reachable_program_counter_witness …)} try assumption 228 >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % 163 #eq_assm %{program_counter} % 164 [1: 165 >eq_assm >lookup_refl % 166 2: 167 %{(reachable_program_counter_witness …)} try assumption 168 >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % 169 ] 229 170 2: 230 171 #neq_assm … … 234 175 @(present_add_present … present_assm) assumption 235 176 1: 236 #program_counter' #ind_hyp' %{program_counter'} 237 #relevant cases (ind_hyp' relevant) #reachable_witness' 238 #ind_hyp'' %{reachable_witness'} >ind_hyp'' 239 @sym_eq @lookup_present_add_miss assumption 177 #program_counter' #ind_hyp' %{program_counter'} % 178 [1: 179 cases ind_hyp' #assm #_ assumption 180 2: 181 cases ind_hyp' #lookup_opt_assm * #reachable_witness' 182 #ind_hyp'' %{reachable_witness'} >ind_hyp'' 183 @sym_eq @lookup_present_add_miss assumption 184 ] 240 185 ] 241 186 ] … … 402 347 ∀code_memory: BitVectorTrie Byte 16. 403 348 ∀cost_labels: BitVectorTrie costlabel 16. 349 ∀cost_labels_injective: 350 ∀pc, pc',l. 351 lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → 352 pc = pc'. 404 353 ∀program_size: nat. 405 354 ∀program_size_limit: program_size ≤ 2^16. … … 411 360 Σcost_map: identifier_map CostTag nat. 412 361 (∀pc,k. nat_of_bitvector … pc < program_size → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧ 413 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →362 (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 414 363 ∃reachable_witness: reachable_program_counter code_memory program_size pc. 415 364 pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ 416 365 λcode_memory: BitVectorTrie Byte 16. 417 366 λcost_labels: BitVectorTrie costlabel 16. 367 λcost_labels_injective. 418 368 λprogram_size: nat. 419 369 λprogram_size_limit: program_size ≤ 2^16. … … 429 379 cases (traverse_code_internal ? ? ? ? ? ? ? ? ?) 430 380 #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 % 431 try assumption #pc #k #pc_program_size_assm432 @inductive_hypothesis1433 381 [1: 434 @le_O_n 382 #pc #k #pc_program_size_assm 383 @inductive_hypothesis1 384 [1: 385 @le_O_n 386 2: 387 normalize in match (nat_of_bitvector 16 (zero 16)); 388 <plus_n_O assumption 389 ] 435 390 2: 436 normalize in match (nat_of_bitvector 16 (zero 16)); 437 <plus_n_O assumption 391 #k #k_pres #pc #lookup_opt_assm 392 cases (inductive_hypothesis2 ? k_pres) 393 #program_counter' * #lookup_opt_assm' * #reachable_witness 394 #block_cost_assm 395 >(cost_labels_injective … lookup_opt_assm lookup_opt_assm') 396 %{reachable_witness} assumption 438 397 ] 439 398 ] … … 443 402 λprogram: list Byte. 444 403 λcost_labels: BitVectorTrie costlabel 16. 404 λcost_labels_injective: 405 ∀pc, pc',l. 406 lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → 407 pc = pc'. 445 408 λreachable_program_witness. 446 409 λgood_program_witness: good_program (load_code_memory program) (program). … … 448 411 let program_size ≝ program in 449 412 let code_memory ≝ load_code_memory program in 450 traverse_code code_memory cost_labels program_size program_size_limit reachable_program_witness good_program_witness.413 traverse_code code_memory cost_labels cost_labels_injective program_size program_size_limit reachable_program_witness good_program_witness.
Note: See TracChangeset
for help on using the changeset viewer.