Changeset 1573
- Timestamp:
- Nov 28, 2011, 5:13:04 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 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 *) -
src/ASM/Interpret.ma
r1547 r1573 785 785 786 786 definition current_instruction_cost ≝ 787 λs: Status. \snd (fetch (code_memory … s) (program_counter … s)). 787 λs: Status. 788 \snd (fetch (code_memory … s) (program_counter … s)). 788 789 789 790 definition execute_1: ∀s:Status. Σs':Status. clock … s' - clock … s = current_instruction_cost s ≝
Note: See TracChangeset
for help on using the changeset viewer.