Changeset 1548


Ignore:
Timestamp:
Nov 23, 2011, 11:15:07 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1544 r1548  
    4343    | _    ⇒ True
    4444    ].
    45 
    46 definition current_instruction_cost ≝
    47   λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
    4845
    4946definition next_instruction_properly_relates_program_counters ≝
     
    251248  ].
    252249
     250(*Useless now?
    253251(* To be moved *)
    254252lemma pred_minus_1:
     
    278276    S m = m + 1.
    279277 //
    280 qed.
     278qed.*)
    281279
    282280include alias "arithmetics/nat.ma".
    283281
     282(*Useless now?
    284283lemma minus_m_n_minus_minus_plus_1:
    285284  ∀m, n: nat.
     
    304303    (m - n) + (n - o) = m - o.
    305304 /2 by plus_minus_rearrangement_1/
    306 qed.
    307 
    308 lemma current_instruction_cost_is_ok:
    309   ∀s: Status.
    310     current_instruction_cost s = clock … (execute 1 s) - clock … s.
    311   #s
    312   change with (execute_1 s) in match (eject … (execute 1 s));
    313   change with (
    314     let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
    315                                (program_counter (BitVectorTrie Byte 16) s)
    316     in 
    317      eject … (execute_1_0 s instr_pc_ticks)) in match (eject … (execute_1 s));
    318   change with (
    319     \snd (fetch (code_memory … s) (program_counter … s))) in ⊢ (??%?);
    320   normalize nodelta;
    321   whd in match (
    322     execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s)
    323      (program_counter (BitVectorTrie Byte 16) s)));
    324   normalize nodelta;
    325   cases (fetch (code_memory (BitVectorTrie Byte 16) s)
    326            (program_counter (BitVectorTrie Byte 16) s));
    327   #instr_pc #ticks normalize nodelta;
    328   cases (\fst instr_pc)
    329   [1:
    330     #addr11 normalize nodelta;
    331     cases addr11 #addressing_mode
    332     cases addressing_mode
    333     [1,2,3,4,8,9,15,16,17,19:
    334       #assm whd in ⊢ (% → ?)
    335       #absurd cases(absurd)
    336     |5,6,7,10,11,12,13,14:
    337       whd in ⊢ (% → ?)
    338       #absurd cases(absurd)
    339     |18:
    340       #word11 #irrelevant normalize nodelta;
    341       >set_program_counter_ignores_clock
    342       >write_at_stack_pointer_ignores_clock
    343       >set_8051_sfr_ignores_clock
    344       >write_at_stack_pointer_ignores_clock
    345       >set_8051_sfr_ignores_clock
    346       >clock_set_clock
    347       >set_program_counter_ignores_clock
    348       >commutative_plus
    349       <plus_minus
    350       <(minus_n_n (clock (BitVectorTrie Byte 16) s))
    351       %
    352     ]
    353   |2:
    354     #addr16 cases addr16 #addressing_mode
    355     normalize nodelta; cases addressing_mode
    356     normalize nodelta;
    357     [1,2,3,4,8,9,15,16,17,18:
    358       #assm whd in ⊢ (% → ?)
    359       #absurd cases(absurd)
    360     |5,6,7,10,11,12,13,14:
    361       whd in ⊢ (% → ?)
    362       #absurd cases(absurd)
    363     |19:
    364       #addr16 #irrelevant
    365       normalize nodelta;
    366       >set_program_counter_ignores_clock
    367       >write_at_stack_pointer_ignores_clock
    368       >set_8051_sfr_ignores_clock
    369       >write_at_stack_pointer_ignores_clock
    370       >set_8051_sfr_ignores_clock
    371       >clock_set_clock
    372       >set_program_counter_ignores_clock
    373       >commutative_plus
    374       <plus_minus
    375       <(minus_n_n (clock (BitVectorTrie Byte 16) s))
    376       %
    377     ]
    378   |3:
    379     #addr11 cases addr11 #addressing_mode
    380     normalize nodelta; cases addressing_mode
    381     normalize nodelta;
    382     [1,2,3,4,8,9,15,16,17,19:
    383       #assm whd in ⊢ (% → ?)
    384       #absurd cases(absurd)
    385     |5,6,7,10,11,12,13,14:
    386       whd in ⊢ (% → ?)
    387       #absurd cases(absurd)
    388     |18:
    389       #word11 #irrelevant
    390       normalize nodelta;
    391       >set_program_counter_ignores_clock
    392       >clock_set_clock
    393       >set_program_counter_ignores_clock
    394       >commutative_plus
    395       <plus_minus
    396       <(minus_n_n (clock (BitVectorTrie Byte 16) s))
    397       %
    398     ]
    399   |4:
    400     #addr16 cases addr16 #addressing_mode
    401     normalize nodelta; cases addressing_mode
    402     normalize nodelta;
    403     [1,2,3,4,8,9,15,16,17,18:
    404       #assm whd in ⊢ (% → ?)
    405       #absurd cases(absurd)
    406     |5,6,7,10,11,12,13,14:
    407       whd in ⊢ (% → ?)
    408       #absurd cases(absurd)
    409     |19:
    410       #word #irrelevant
    411       normalize nodelta;
    412       >set_program_counter_ignores_clock
    413       >clock_set_clock
    414       >set_program_counter_ignores_clock
    415       >commutative_plus
    416       <plus_minus
    417       <(minus_n_n (clock (BitVectorTrie Byte 16) s))
    418       %
    419     ]
    420   |5:
    421     #relative cases relative #addressing_mode
    422     normalize nodelta; cases addressing_mode
    423     normalize nodelta;
    424     [1,2,3,4,8,9,15,16,18,19:
    425       #assm whd in ⊢ (% → ?)
    426       #absurd cases(absurd)
    427     |5,6,7,10,11,12,13,14:
    428       whd in ⊢ (% → ?)
    429       #absurd cases(absurd)
    430     |17:
    431       #byte #irrelevant
    432       normalize nodelta;
    433       >set_program_counter_ignores_clock
    434       >set_program_counter_ignores_clock
    435       >clock_set_clock
    436       >commutative_plus
    437       <plus_minus
    438       <(minus_n_n (clock (BitVectorTrie Byte 16) s))
    439       %
    440     ]
    441   |6:
    442     #indirect_dptr cases indirect_dptr #addressing_mode
    443     normalize nodelta; cases addressing_mode
    444     normalize nodelta;
    445     [1,2,3,4,8,9,15,16,17,18,19:
    446       #assm whd in ⊢ (% → ?)
    447       #absurd cases(absurd)
    448     |5,6,7,10,11,12,14:
    449       whd in ⊢ (% → ?)
    450       #absurd cases(absurd)
    451     |13:
    452       #irrelevant
    453       normalize nodelta;
    454       >set_program_counter_ignores_clock
    455       >set_program_counter_ignores_clock
    456       >clock_set_clock
    457       >commutative_plus
    458       <plus_minus
    459       <(minus_n_n (clock (BitVectorTrie Byte 16) s))
    460       %
    461     ]
    462   |7:
    463     #acc_a cases acc_a #addressing_mode
    464     normalize nodelta; cases addressing_mode
    465     normalize nodelta;
    466     [1,2,3,4,8,9,15,16,17,18,19:
    467       #assm whd in ⊢ (% → ?)
    468       #absurd cases(absurd)
    469     |6,7,10,11,12,13,14:
    470       whd in ⊢ (% → ?)
    471       #absurd cases(absurd)
    472     |5:
    473       #irrelevant #acc_dptr_acc_pc
    474       normalize nodelta;
    475       cases daemon (* XXX: todo *)
    476     ]
    477   |8: cases daemon (* XXX: todo *)
    478   ]
    479 qed.
     305qed.*)
    480306
    481307let rec compute_max_trace_label_label_cost_is_ok
Note: See TracChangeset for help on using the changeset viewer.