Changeset 1540


Ignore:
Timestamp:
Nov 23, 2011, 4:03:38 PM (8 years ago)
Author:
mulligan
Message:

changes to proof in interrupt.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1538 r1540  
    589589                 let s ≝ add_ticks2 s in
    590590                  s
    591         ]. (*14s*)
     591        ]. cases daemon (*
     592        (*14s*)
    592593(*    try assumption (*20s*)
    593594    try % (*6s*)
     
    606607   normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock
    607608   >set_8051_sfr_ignores_clock >clock_set_clock //
    608  |24:
     609 |21,24:
    609610   normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock
    610611   >clock_set_clock //
    611  |25: normalize nodelta @(le_n (clock M s))
     612 |25,26,28:
     613   normalize nodelta //
     614 |30,32,35:
     615   normalize nodelta //
    612616 |13,14,15,16,18:
    613617   normalize nodelta >set_arg_8_ignores_clock >clock_set_clock //
    614618 |17:
    615619   normalize nodelta >set_8051_sfr_ignores_clock >clock_set_clock //
    616  |17,18,23,24,25,28: /by/
    617  |3,4,7,8,11,12,19,20:
     620 |3,4,7,8,11,12,19,20,33,36: cases daemon
     621 |27,29,31,34,37:
     622   normalize nodelta >set_program_counter_ignores_clock >clock_set_clock //
     623 |22:
     624   normalize nodelta <set_flags_ignores_clock >clock_set_clock //
    618625 [9: (* normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock
    619626     >clock_set_clock // *) (* segfault now *)
     
    640647 |57,58,59,60,61: <set_args_8_ignores_clock /by/ (*0.5s ??*)
    641648 (* 5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *)
    642  |*:cases daemon]
    643 qed.
    644 
    645 (*CSC: indexing diverges, why?*)
    646 example set_program_counter_ignores_clock:
    647   ∀M.∀s: PreStatus M.
    648   ∀pc: Word.
    649     clock … (set_program_counter … s pc) = clock … s.
    650  //
    651 qed.
    652 
    653 lemma set_8051_sfr_ignores_clock:
    654   ∀M.∀s: PreStatus M.
    655   ∀sfr: SFR8051.
    656   ∀v: Byte.
    657     clock … (set_8051_sfr ? s sfr v) = clock … s.
    658   //
     649 |*:cases daemon] *)
    659650qed.
    660651
Note: See TracChangeset for help on using the changeset viewer.