Changeset 1540 for src/ASM/Interpret.ma

Timestamp:

Nov 23, 2011, 4:03:38 PM (9 years ago)

Author:

mulligan

Message:

changes to proof in interrupt.ma

File:

• src/ASM/Interpret.ma (modified) (3 diffs)

src/ASM/Interpret.ma

@@ -589 +589 @@
                  let s ≝ add_ticks2 s in
                   s
-        ]. (*14s*)
+        ]. cases daemon (*
+        (*14s*)
 (*    try assumption (*20s*)
     try % (*6s*)
@@ -606 +607 @@
    normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock
    >set_8051_sfr_ignores_clock >clock_set_clock //
- |24:
+ |21,24:
    normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock
    >clock_set_clock //
- |25: normalize nodelta @(le_n (clock M s))
+ |25,26,28:
+   normalize nodelta //
+ |30,32,35:
+   normalize nodelta //
  |13,14,15,16,18:
    normalize nodelta >set_arg_8_ignores_clock >clock_set_clock //
  |17:
    normalize nodelta >set_8051_sfr_ignores_clock >clock_set_clock //
- |17,18,23,24,25,28: /by/
- |3,4,7,8,11,12,19,20:
+ |3,4,7,8,11,12,19,20,33,36: cases daemon
+ |27,29,31,34,37:
+   normalize nodelta >set_program_counter_ignores_clock >clock_set_clock //
+ |22:
+   normalize nodelta <set_flags_ignores_clock >clock_set_clock //
  [9: (* normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock
      >clock_set_clock // *) (* segfault now *)
@@ -640 +647 @@
  |57,58,59,60,61: <set_args_8_ignores_clock /by/ (*0.5s ??*)
  (* 5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *)
- |*:cases daemon]
-qed.
-
-(*CSC: indexing diverges, why?*)
-example set_program_counter_ignores_clock:
-  ∀M.∀s: PreStatus M.
-  ∀pc: Word.
-    clock … (set_program_counter … s pc) = clock … s.
- //
-qed.
-
-lemma set_8051_sfr_ignores_clock:
-  ∀M.∀s: PreStatus M.
-  ∀sfr: SFR8051.
-  ∀v: Byte.
-    clock … (set_8051_sfr ? s sfr v) = clock … s.
-  //
+ |*:cases daemon] *)
 qed.