Changeset 1946 for src/ASM/ASMCostsSplit.ma
 Timestamp:
 May 15, 2012, 12:01:30 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCostsSplit.ma
r1929 r1946 3 3 include alias "arithmetics/nat.ma". 4 4 include alias "basics/logic.ma". 5 5 6 6 let rec traverse_code_internal 7 7 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) … … 16 16 [ O ⇒ λprogram_size_refl. empty_map CostTag nat 17 17  S program_size' ⇒ λprogram_size_refl. 18 deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in18 let new_program_counter' ≝ add 16 (bitvector_of_nat 16 1) program_counter in 19 19 let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in 20 20 match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with … … 22 22  Some lbl ⇒ λlookup_refl. 23 23 let cost ≝ block_cost code_memory program_counter cost_labels in 24 add …cost_mapping lbl cost24 cic:/matita/cerco/common/Identifiers/add.fix(0,2,2) ?? cost_mapping lbl cost 25 25 ] (refl … (lookup_opt … program_counter cost_labels)) 26 26 ] (refl … program_size). … … 63 63 2: 64 64 #n' #_ #program_size_refl_Sn' traverse_code_internal destruct 65 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 ( \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)))65 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter)) 66 66 [1: 67 67 destruct … … 90 90 #eqb_ref_assm 91 91 ind_hyp 92 < NEW_PC' in S_assm; #relevant <relevant relevant92 <S_assm 93 93 change with (? < ?) 94 94 @le_neq_to_lt assumption … … 97 97 generalize in match H2; whd in ⊢ (??% → ?); 98 98 >plus_n_Sm in ⊢ (% → ?); 99 cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)) 100 [1: 101 <NEW_PC' % 99 cut(new_program_counter' = add 16 (bitvector_of_nat 16 1) program_counter) 100 [1: % 102 101 2: 103 102 #new_program_counter_assm' >new_program_counter_assm' … … 188 187 @(transitive_le ? (S (nat_of_bitvector … program_counter))) 189 188 [1: 190 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 ( \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)))189 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter)) 191 190 [1: 192 191 destruct … … 198 197 @le_S_S @le_S_S @le_O_n 199 198 2: 200 #Sn_refl_assm >Sn_refl_assm <NEW_PC'@le_n199 #Sn_refl_assm >Sn_refl_assm @le_n 201 200 ] 202 201 2: … … 209 208 destruct 210 209 @(transitive_le … H2) 211 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 ( \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)))210 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter)) 212 211 [1: 213 212 destruct … … 222 221 change with (S (S n' + ?) ≤ ?) 223 222 >plus_n_Sm @monotonic_le_plus_r >S_assm 224 <NEW_PC'@le_n223 @le_n 225 224 ] 226 225 ] … … 243 242 @eq_f >program_size_refl_Sn <plus_n_Sm 244 243 change with (? = (S ?) + ?) @eq_f2 try % 245 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 ( \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)))244 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter)) 246 245 [1: 247 246 destruct … … 254 253 2: 255 254 #S_assm 256 cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter)) 257 [1: 258 <NEW_PC' % 255 cut(new_program_counter' = add … (bitvector_of_nat … 1) program_counter) 256 [1: % 259 257 2: 260 258 #new_program_counter_assm' >new_program_counter_assm' 261 259 cases program_size_invariant 262 260 [1: 263 #destruct_assm destruct261 #destruct_assm @⊥ >destruct_assm in program_size_refl; #abs destruct(abs) 264 262 2: 265 263 #program_size_invariant
Note: See TracChangeset
for help on using the changeset viewer.