Changeset 1573 for src/ASM/CostsProof.ma
 Timestamp:
 Nov 28, 2011, 5:13:04 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1571 r1573 1 1 2 include "ASM/ASMCosts.ma". 2 3 include "ASM/WellLabeled.ma". … … 250 251 lemma current_instruction_cost_non_zero: 251 252 ∀s: Status. 252 0 ≤ current_instruction_cost s. 253 // 254 qed. 253 current_instruction_cost s > 0. 254 #s 255 cases s 256 #code_memory #hi_ram #lo_ram #x_ram #pc #sfr_8051 #sfr_8052 #p1_latch 257 #p2_latch #clock 258 change with (\snd (fetch ? ?)) in ⊢ (?%?); 259 change with (fetch0 ? ?) in match (fetch ? ?); 260 change with ( 261 let 〈pc,v〉 ≝ next code_memory pc in 262 let 〈b,v0〉 ≝head bool 7 v in 263 ?) in match (fetch0 ? ?); 264 normalize nodelta; 265 266 cases(fetch (code_memory … s) (program_counter … s)) 267 #instruction_pc 268 cases(instruction_pc) 269 #instruction #pc 270 cases(instruction) 271 [ #addr11 255 272 256 273 lemma le_monotonic_plus: … … 276 293 qed. 277 294 278 lemma minus_m_n_le_n_m:295 axiom minus_m_n_gt_o_O_le_n_m: 279 296 ∀m, n, o. 280 297 m  n = o → o > 0 → n ≤ m. 281 #m #n #o #eq_hyp282 cases o283 [ #absrd normalize in absrd; @le284 normalize in ⊢ (% → ?);285 <eq_hyp in ⊢ (% → ?);286 #lt_hyp287 generalize in match (le_plus_to_minus_l 1 n m ? lt_hyp);288 [1: /2/ 289 qed.290 291 298 292 299 let rec compute_max_trace_label_label_cost_is_ok … … 333 340 #the_status #assm 334 341 whd in match eject; normalize nodelta 335 @(minus_m_n_gt_o_ 0_le_n_m ? ? (current_instruction_cost start_status))342 @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status)) 336 343 [1: assumption 337 2: @ current_instruction_cost_non_zero344 2: @(current_instruction_cost_non_zero start_status) 338 345 ] 339 346 ] … … 352 359 #the_status #assm 353 360 whd in match eject; normalize nodelta 354 @(minus_m_n_gt_o_ 0_le_n_m ? ? (current_instruction_cost start_status))361 @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status)) 355 362 [1: assumption 356 363 2: @current_instruction_cost_non_zero … … 375 382 #trace_any_label_eq #trace_any_label_le 376 383 >trace_label_return_eq >trace_any_label_eq 377 cases daemon (* XXX: complete me *) 384 >commutative_plus 385 386 cut ((clock (BitVectorTrie Byte 16) status_after_fun_call 387 clock (BitVectorTrie Byte 16) status_start_fun_call 388 +current_instruction_cost status_pre_fun_call 389 +(clock (BitVectorTrie Byte 16) status_final 390 clock (BitVectorTrie Byte 16) status_after_fun_call) = 391 ((clock (BitVectorTrie Byte 16) status_after_fun_call 392  clock (BitVectorTrie Byte 16) status_start_fun_call) 393 + (clock (BitVectorTrie Byte 16) status_final 394  clock (BitVectorTrie Byte 16) status_after_fun_call)) 395 + current_instruction_cost status_pre_fun_call)) 396 [ 1: 397 cases daemon (* XXX: complete me *) 398  2: 399 #eq_hyp >eq_hyp 400 >plus_minus_rearrangement_1 401 [1: 402 2, 3: 403 assumption 404 ] 405 ] 378 406 2: 379 407 cases daemon (* XXX: complete me *)
Note: See TracChangeset
for help on using the changeset viewer.