Changeset 1577


Ignore:
Timestamp:
Nov 30, 2011, 5:32:52 PM (8 years ago)
Author:
mulligan
Message:

A lot more cases added to the proof at the bottom of execute_1_preinstruction, thought these make use of tacticals, with one in particular taking 1000+ seconds to complete. Changed all the Russell specifications in Interpret.ma to use the new, simplified specification.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1576 r1577  
    252252  ∀s: Status.
    253253    clock … (execute_1 s) = current_instruction_cost s + clock … s.
    254 
    255 axiom plus_minus_minus:
    256   ∀m, n, o: nat.
    257     m - (n + o) = (m - n) - o.
    258254
    259255axiom plus_le_le:
     
    353349          (current_instruction_cost status_pre_fun_call
    354350            + clock (BitVectorTrie Byte 16) status_pre_fun_call));
    355         >plus_minus_minus
     351        <minus_plus
    356352        <(plus_minus_m_m (clock (BitVectorTrie Byte 16) status_after_fun_call
    357353  -clock (BitVectorTrie Byte 16) status_pre_fun_call) (current_instruction_cost status_pre_fun_call))
     
    406402        >clock_execute_1
    407403        >commutative_plus in match ((current_instruction_cost status_pre+clock (BitVectorTrie Byte 16) status_pre));
    408         >plus_minus_minus
     404        <minus_plus
    409405        <plus_minus_m_m
    410406        [1: %
  • src/ASM/Interpret.ma

    r1575 r1577  
    166166
    167167definition execute_1_preinstruction:
    168  ∀ticks: nat × nat.
    169  ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A →
    170  ∀s:PreStatus M.
    171   Σs': PreStatus M.
    172    And
    173    (Or (clock … s' - clock … s = \fst ticks)
    174       (clock … s' - clock … s = \snd ticks))
    175    (clock … s ≤ clock … s')
    176  ≝
    177   λticks.
    178   λA, M: Type[0].
    179   λaddr_of: A → (PreStatus M) → Word.
    180   λinstr: preinstruction A.
    181   λs: PreStatus M.
    182   let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
    183   let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
    184   match instr return λx.
    185     Σs': PreStatus M.
    186       And
    187         (Or (clock … s' - clock … s = \fst ticks)
    188             (clock … s' - clock … s = \snd ticks))
    189                 (clock … s ≤ clock … s') with
     168  ∀ticks: nat × nat.
     169  ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a →
     170  ∀s: PreStatus m.
     171    Σs': PreStatus m.
     172      Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) ≝
     173  λticks: nat × nat.
     174  λa, m: Type[0].
     175  λaddr_of: a → PreStatus m → Word.
     176  λinstr: preinstruction a.
     177  λs: PreStatus m.
     178  let add_ticks1 ≝ λs: PreStatus m. set_clock … s (\fst ticks + clock … s) in
     179  let add_ticks2 ≝ λs: PreStatus m. set_clock … s (\snd ticks + clock … s) in
     180  match instr return λx. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
    190181        [ ADD addr1 addr2 ⇒
    191182            let s ≝ add_ticks1 s in
     
    225216                  let 〈addr1, addr2〉 ≝ l' in
    226217                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    227                     set_arg_8 ? s addr1 and_val
     218                    eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val)
    228219                | inr r ⇒
    229220                  let 〈addr1, addr2〉 ≝ r in
    230221                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    231                     set_arg_8 ? s addr1 and_val
     222                    eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val)
    232223                ]
    233224            | inr r ⇒
    234225              let 〈addr1, addr2〉 ≝ r in
    235226              let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
    236                 set_flags ? s and_val (None ?) (get_ov_flag ? s)
     227                eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s and_val (None ?) (get_ov_flag ? s))
    237228            ]
    238229        | ORL addr ⇒
     
    240231          match addr with
    241232            [ inl l ⇒
    242               match l with
     233              match l return λ_. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
    243234                [ inl l' ⇒
    244235                  let 〈addr1, addr2〉 ≝ l' in
    245236                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    246                     set_arg_8 ? s addr1 or_val
     237                    eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val)
    247238                | inr r ⇒
    248239                  let 〈addr1, addr2〉 ≝ r in
    249240                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    250                     set_arg_8 ? s addr1 or_val
     241                    eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val)
    251242                ]
    252243            | inr r ⇒
    253244              let 〈addr1, addr2〉 ≝ r in
    254245              let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
    255                 set_flags ? s or_val (None ?) (get_ov_flag ? s)
     246                eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s or_val (None ?) (get_ov_flag ? s))
    256247            ]
    257248        | XRL addr ⇒
     
    261252              let 〈addr1, addr2〉 ≝ l' in
    262253              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    263                 eject (set_arg_8 ? s addr1 xor_val)
     254                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val)
    264255            | inr r ⇒
    265256              let 〈addr1, addr2〉 ≝ r in
    266257              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    267                 eject (set_arg_8 ? s addr1 xor_val)
     258                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val)
    268259            ]
    269260        | INC addr ⇒
    270             match addr
    271             return
    272              λx. bool_to_Prop
    273               (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) →
    274                Σs': PreStatus M.
    275                 And
    276                 (Or (clock … s' - clock … s = \fst ticks)
    277                    (clock … s' - clock … s = \snd ticks))
    278                 (clock … s ≤ clock … s')
    279              with
     261            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
    280262              [ ACC_A ⇒ λacc_a: True.
    281263                let s' ≝ add_ticks1 s in
    282264                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in
    283                  eject (set_arg_8 ? s' ACC_A result)
     265                 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' ACC_A result)
    284266              | REGISTER r ⇒ λregister: True.
    285267                let s' ≝ add_ticks1 s in
    286268                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in
    287                  eject (set_arg_8 ? s' (REGISTER r) result)
     269                 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (REGISTER r) result)
    288270              | DIRECT d ⇒ λdirect: True.
    289271                let s' ≝ add_ticks1 s in
    290272                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in
    291                  eject (set_arg_8 ? s' (DIRECT d) result)
     273                 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (DIRECT d) result)
    292274              | INDIRECT i ⇒ λindirect: True.
    293275                let s' ≝ add_ticks1 s in
    294276                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
    295                  eject (set_arg_8 ? s' (INDIRECT i) result)
     277                 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (INDIRECT i) result)
    296278              | DPTR ⇒ λdptr: True.
    297279                let s' ≝ add_ticks1 s in
     
    299281                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in
    300282                let s ≝ set_8051_sfr ? s' SFR_DPL bl in
    301                   eject (set_8051_sfr ? s' SFR_DPH bu)
     283                  eject (PreStatus m) (λx. clock … s' = clock … x) (set_8051_sfr ? s' SFR_DPH bu)
    302284              | _ ⇒ λother: False. ⊥
    303285              ] (subaddressing_modein … addr)
     
    308290           let s ≝ add_ticks1 s in
    309291           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
    310              eject (set_arg_8 ? s addr result)
     292             eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr result)
    311293        | MUL addr1 addr2 ⇒
    312294           let s ≝ add_ticks1 s in
     
    318300           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
    319301           let s ≝ set_8051_sfr ? s SFR_ACC_A low in
    320              eject … (set_8051_sfr ? s SFR_ACC_B high)
     302             set_8051_sfr ? s SFR_ACC_B high
    321303        | DIV addr1 addr2 ⇒
    322304           let s ≝ add_ticks1 s in
     
    330312                 let s ≝ set_8051_sfr ? s SFR_ACC_A q in
    331313                 let s ≝ set_8051_sfr ? s SFR_ACC_B r in
    332                    eject … (set_flags ? s false (None Bit) false)
     314                   set_flags ? s false (None Bit) false
    333315               ]
    334316        | DA addr ⇒
     
    349331                s
    350332        | CLR addr ⇒
    351           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) →
    352               Σs': PreStatus M.
    353                               And
    354                 (Or (clock … s' - clock … s = \fst ticks)
    355                    (clock … s' - clock … s = \snd ticks))
    356                 (clock … s ≤ clock … s') with
     333          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
    357334            [ ACC_A ⇒ λacc_a: True.
    358335              let s ≝ add_ticks1 s in
    359                 eject (set_arg_8 ? s ACC_A (zero 8))
     336                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s ACC_A (zero 8))
    360337            | CARRY ⇒ λcarry: True.
    361338              let s ≝ add_ticks1 s in
    362                 eject (set_arg_1 ? s CARRY false)
     339                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY false)
    363340            | BIT_ADDR b ⇒ λbit_addr: True.
    364341              let s ≝ add_ticks1 s in
    365                 eject (set_arg_1 ? s (BIT_ADDR b) false)
     342                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) false)
    366343            | _ ⇒ λother: False. ⊥
    367344            ] (subaddressing_modein … addr)
    368345        | CPL addr ⇒
    369           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) →
    370             Σs': PreStatus M.
    371                            And
    372                 (Or (clock … s' - clock … s = \fst ticks)
    373                    (clock … s' - clock … s = \snd ticks))
    374                 (clock … s ≤ clock … s') with
     346          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
    375347            [ ACC_A ⇒ λacc_a: True.
    376348                let s ≝ add_ticks1 s in
    377349                let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    378350                let new_acc ≝ negation_bv ? old_acc in
    379                   eject (set_8051_sfr ? s SFR_ACC_A new_acc)
     351                  eject (PreStatus m) (λx. clock … s = clock … x) (set_8051_sfr ? s SFR_ACC_A new_acc)
    380352            | CARRY ⇒ λcarry: True.
    381353                let s ≝ add_ticks1 s in
    382354                let old_cy_flag ≝ get_arg_1 ? s CARRY true in
    383355                let new_cy_flag ≝ ¬old_cy_flag in
    384                   eject (set_arg_1 ? s CARRY new_cy_flag)
     356                  eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY new_cy_flag)
    385357            | BIT_ADDR b ⇒ λbit_addr: True.
    386358                let s ≝ add_ticks1 s in
    387359                let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
    388360                let new_bit ≝ ¬old_bit in
    389                   eject (set_arg_1 ? s (BIT_ADDR b) new_bit)
     361                  eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) new_bit)
    390362            | _ ⇒ λother: False. ?
    391363            ] (subaddressing_modein … addr)
     
    426398              set_8051_sfr ? s SFR_ACC_A new_acc
    427399        | PUSH addr ⇒
    428             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) →
    429               Σs': PreStatus M.
    430                 And
    431                 (Or (clock … s' - clock … s = \fst ticks)
    432                    (clock … s' - clock … s = \snd ticks))
    433                 (clock … s ≤ clock … s') with
     400            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
    434401              [ DIRECT d ⇒ λdirect: True.
    435402                let s ≝ add_ticks1 s in
     
    450417            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    451418            let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
    452               eject (set_arg_8 ? s addr2 old_acc)
     419              eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr2 old_acc)
    453420        | XCHD addr1 addr2 ⇒
    454421            let s ≝ add_ticks1 s in
     
    485452            [ inl l ⇒
    486453              let 〈addr1, addr2〉 ≝ l in
    487                 eject (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
     454                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
    488455            | inr r ⇒
    489456              let 〈addr1, addr2〉 ≝ r in
    490                 eject (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
     457                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
    491458            ]
    492459        | MOV addr ⇒
     
    503470                            [ inl l'''' ⇒
    504471                              let 〈addr1, addr2〉 ≝ l'''' in
    505                                 eject (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
     472                                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
    506473                            | inr r'''' ⇒
    507474                              let 〈addr1, addr2〉 ≝ r'''' in
    508                                 eject (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
     475                                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
    509476                            ]
    510477                        | inr r''' ⇒
    511478                          let 〈addr1, addr2〉 ≝ r''' in
    512                             eject (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
     479                            eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
    513480                        ]
    514481                    | inr r'' ⇒
    515482                      let 〈addr1, addr2〉 ≝ r'' in
    516                         eject (set_arg_16 ? s (get_arg_16 ? s addr2) addr1)
     483                        eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_16 ? s (get_arg_16 ? s addr2) addr1)
    517484                    ]
    518485                | inr r ⇒
    519486                  let 〈addr1, addr2〉 ≝ r in
    520                     eject (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
     487                    eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
    521488                ]
    522489            | inr r ⇒
    523490              let 〈addr1, addr2〉 ≝ r in
    524                 eject (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
     491                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
    525492            ]
    526493          | JC addr ⇒
     
    534501                  if ¬(get_cy_flag ? s) then
    535502                   let s ≝ add_ticks1 s in
    536                      eject … (set_program_counter ? s (addr_of addr s))
     503                     set_program_counter ? s (addr_of addr s)
    537504                  else
    538505                   let s ≝ add_ticks2 s in
     
    583550                            let s ≝ add_ticks1 s in
    584551                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
    585                               eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
     552                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    586553                          else
    587554                            let s ≝ add_ticks2 s in
    588                               eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
     555                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    589556                    | inr r' ⇒
    590557                        let 〈addr1, addr2'〉 ≝ r' in
     
    594561                            let s ≝ add_ticks1 s in
    595562                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
    596                               eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
     563                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    597564                          else
    598565                            let s ≝ add_ticks2 s in
    599                               eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
     566                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    600567                    ]
    601568            | DJNZ addr1 addr2 ⇒
     
    609576                  s
    610577        ]. (*15s*)
     578    try (destruct(other))
    611579    try assumption (*20s*)
    612580    try % (*6s*)
     
    615583      @ I
    616584    ) (*66s*)
    617  try @le_n
    618  [ /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ /2 by or_introl/
    619  | /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ //
    620  |*: cases daemon (* XXX: easy? *) ]
     585    try (<set_arg_8_ignores_clock normalize nodelta /demod/ %)
     586    try (/demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ %)
     587    try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock /demod/ %)
     588    try (normalize nodelta <set_flags_ignores_clock /demod/ %)
     589    try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)
     590    try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock @commutative_plus)
     591    try (/demod/ normalize nodelta >clock_set_clock @commutative_plus)
     592(* XXX: weird open goals here *)
     593(*    [14: normalize nodelta <set_arg_8_ignores_clock /demod/ normalize nodelta
     594    try (normalize nodelta /demod/ %)
     595    try (/demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock @commutative_plus)
     596
     597    try (normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)*)
     598    cases daemon
    621599qed.
    622600
     
    632610  #nu #nl normalize nodelta;
    633611  cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
    634   [ normalize nodelta; %
    635   | normalize nodelta; %
    636   ]
     612  normalize nodelta; %
    637613qed.
    638614
    639615definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat.
    640   Σs': Status. And (clock … s' - clock … s = \snd current) (clock … s ≤ clock … s')
     616  Σs': Status. clock … s' = \snd current + clock … s
    641617  λs0,instr_pc_ticks.
    642618    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    643619    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    644620    let s ≝ set_program_counter ? s0 pc in
    645       match instr return λ_. Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
     621      match instr return λ_. Σs': Status. clock … s' = ticks + clock … s0 with
    646622      [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?
    647623        (λx. λs.
     
    652628      | MOVC addr1 addr2 ⇒
    653629          let s ≝ set_clock ? s (ticks + clock ? s) in
    654           match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) →
    655             Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
     630          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
    656631            [ ACC_DPTR ⇒ λacc_dptr: True.
    657632              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
     
    680655      | LJMP addr ⇒
    681656          let s ≝ set_clock ? s (ticks + clock ? s) in
    682           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) →
    683             Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
     657          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
    684658            [ ADDR16 a ⇒ λaddr16: True.
    685659                set_program_counter ? s a
     
    688662      | SJMP addr ⇒
    689663          let s ≝ set_clock ? s (ticks + clock ? s) in
    690           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) →
    691             Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
     664          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
    692665            [ RELATIVE r ⇒ λrelative: True.
    693666                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     
    697670      | AJMP addr ⇒
    698671          let s ≝ set_clock ? s (ticks + clock ? s) in
    699           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) →
    700             Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
     672          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
    701673            [ ADDR11 a ⇒ λaddr11: True.
    702674              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     
    711683      | ACALL addr ⇒
    712684          let s ≝ set_clock ? s (ticks + clock ? s) in
    713           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) →
    714             Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
     685          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
    715686            [ ADDR11 a ⇒ λaddr11: True.
    716687              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     
    729700        | LCALL addr ⇒
    730701          let s ≝ set_clock ? s (ticks + clock ? s) in
    731           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) →
    732             Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
     702          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
    733703            [ ADDR16 a ⇒ λaddr16: True.
    734704              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     
    743713            ] (subaddressing_modein … addr)
    744714      ]. (*10s*)
    745     cases daemon (* XXX: problem with russell here *)
     715    try (cases(other))
     716    [2: normalize nodelta
     717        >set_program_counter_ignores_clock
     718        >write_at_stack_pointer_ignores_clock
     719        >set_8051_sfr_ignores_clock
     720        >write_at_stack_pointer_ignores_clock
     721        >set_8051_sfr_ignores_clock >clock_set_clock
     722        >set_program_counter_ignores_clock %
     723    |*:  cases daemon
     724    ]
    746725(*
    747726    [||||||||*:try assumption]
     
    772751
    773752definition execute_1: ∀s:Status.
    774   Σs':Status. And (clock … s' - clock … s = current_instruction_cost s) (clock … s ≤ clock … s')
     753  Σs':Status. clock … s' = current_instruction_cost s + clock … s
    775754  λs: Status.
    776755    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
     
    810789    s.
    811790  normalize
    812   @ I
     791  @I
    813792qed.
    814793
Note: See TracChangeset for help on using the changeset viewer.