Changeset 1666 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jan 28, 2012, 1:42:15 PM (6 years ago)
Author:
sacerdot
Message:

PreStatus? datatype change: the code_memory field is not a left parameter.
This greatly simplify the dependent type madness due to policy depending
on the code_memory and not really on the status. On the other hand it
makes the rest of the code uglier.

Note: the changes have not been propagated yet to ASMCosts, CostsProof? and
Interpret2. The AssemlyProof? is almost repaired.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1606 r1666  
    1 include "ASM/Status.ma".
     1include "ASM/StatusProofs.ma".
    22include "ASM/Fetch.ma".
    33
     
    119119include alias "ASM/BitVectorTrie.ma".
    120120
    121 
    122 lemma set_flags_ignores_clock:
    123  ∀M,s,f1,f2,f3. clock M s = clock … (set_flags … s f1 f2 f3).
    124 //
    125 qed.
    126 
    127 lemma set_program_counter_ignores_clock:
    128   ∀M: Type[0].
    129   ∀s: PreStatus M.
    130   ∀pc: Word.
    131     clock M (set_program_counter … s pc) = clock … s.
    132   #M #s #pc %
    133 qed.
    134 
    135 lemma set_low_internal_ram_ignores_clock:
    136   ∀M: Type[0].
    137   ∀s: PreStatus M.
    138   ∀ram: BitVectorTrie Byte 7.
    139     clock … (set_low_internal_ram … s ram) = clock … s.
    140   #M #s #ram %
    141 qed.
    142 
    143 lemma set_high_internal_ram_ignores_clock:
    144   ∀m: Type[0].
    145   ∀s: PreStatus m.
    146   ∀ram: BitVectorTrie Byte 7.
    147     clock … (set_high_internal_ram … s ram) = clock … s.
    148   #m #s #ram %
    149 qed.
    150 
    151 lemma set_8051_sfr_ignores_clock:
    152   ∀M: Type[0].
    153   ∀s: PreStatus M.
    154   ∀sfr: SFR8051.
    155   ∀v: Byte.
    156     clock … (set_8051_sfr ? s sfr v) = clock … s.
    157   #M #s #sfr #v %
    158 qed.
    159 
    160 lemma write_at_stack_pointer_ignores_clock:
    161   ∀m: Type[0].
    162   ∀s: PreStatus m.
    163   ∀v: Byte.
    164     clock … (write_at_stack_pointer m s v) = clock … s.
    165   #m #s #v
    166   whd in match write_at_stack_pointer; normalize nodelta
    167   cases(split … 4 4 ?) #nu #nl normalize nodelta
    168   cases(get_index_v … 4 nu 0 ?) normalize nodelta
    169   [ >set_low_internal_ram_ignores_clock | >set_high_internal_ram_ignores_clock ] %
    170 qed.
    171 
    172 lemma clock_set_clock:
    173   ∀M: Type[0].
    174   ∀s: PreStatus M.
    175   ∀v.
    176     clock … (set_clock … s v) = v.
    177   #M #s #v %
    178 qed.
    179 
    180121definition execute_1_preinstruction':
    181122  ∀ticks: nat × nat.
    182   ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a →
    183   ∀s: PreStatus m.
    184     Σs': PreStatus m.
    185       Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) ≝
     123  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
     124  ∀s: PreStatus m cm.
     125    Σs': PreStatus m cm.
     126      Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) ≝
    186127  λticks: nat × nat.
    187   λa, m: Type[0].
    188   λaddr_of: a → PreStatus m → Word.
     128  λa, m: Type[0]. λcm.
     129  λaddr_of: a → PreStatus m cm → Word.
    189130  λinstr: preinstruction a.
    190   λs: PreStatus m.
    191   let add_ticks1 ≝ λs: PreStatus m. set_clock … s (\fst ticks + clock … s) in
    192   let add_ticks2 ≝ λs: PreStatus m. set_clock … s (\snd ticks + clock … s) in
    193   match instr return λx. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
     131  λs: PreStatus m cm.
     132  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
     133  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
     134  match instr in preinstruction return λx. Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock ?? s) (clock ?? s' = \snd ticks + clock ?? s) with
    194135        [ ADD addr1 addr2 ⇒
    195136            let s ≝ add_ticks1 s in
    196             let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
    197                                                    (get_arg_8 ? s false addr2) false in
     137            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
     138                                                   (get_arg_8 s false addr2) false in
    198139            let cy_flag ≝ get_index' ? O  ? flags in
    199140            let ac_flag ≝ get_index' ? 1 ? flags in
    200141            let ov_flag ≝ get_index' ? 2 ? flags in
    201             let s ≝ set_arg_8 ? s ACC_A result in
    202               set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
     142            let s ≝ set_arg_8 s ACC_A result in
     143              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    203144        | ADDC addr1 addr2 ⇒
    204145            let s ≝ add_ticks1 s in
    205             let old_cy_flag ≝ get_cy_flag ? s in
    206             let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
    207                                                    (get_arg_8 ? s false addr2) old_cy_flag in
     146            let old_cy_flag ≝ get_cy_flag ?? s in
     147            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
     148                                                   (get_arg_8 s false addr2) old_cy_flag in
    208149            let cy_flag ≝ get_index' ? O ? flags in
    209150            let ac_flag ≝ get_index' ? 1 ? flags in
    210151            let ov_flag ≝ get_index' ? 2 ? flags in
    211             let s ≝ set_arg_8 ? s ACC_A result in
    212               set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
     152            let s ≝ set_arg_8 s ACC_A result in
     153              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    213154        | SUBB addr1 addr2 ⇒
    214155            let s ≝ add_ticks1 s in
    215             let old_cy_flag ≝ get_cy_flag ? s in
    216             let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
    217                                                    (get_arg_8 ? s false addr2) old_cy_flag in
     156            let old_cy_flag ≝ get_cy_flag ?? s in
     157            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
     158                                                   (get_arg_8 s false addr2) old_cy_flag in
    218159            let cy_flag ≝ get_index' ? O ? flags in
    219160            let ac_flag ≝ get_index' ? 1 ? flags in
    220161            let ov_flag ≝ get_index' ? 2 ? flags in
    221             let s ≝ set_arg_8 ? s ACC_A result in
    222               set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
     162            let s ≝ set_arg_8 s ACC_A result in
     163              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    223164        | ANL addr ⇒
    224165          let s ≝ add_ticks1 s in
     
    228169                [ inl l' ⇒
    229170                  let 〈addr1, addr2〉 ≝ l' in
    230                   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
     171                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     172                    set_arg_8 s addr1 and_val
    232173                | inr r ⇒
    233174                  let 〈addr1, addr2〉 ≝ r in
    234                   let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    235                     set_arg_8 ? s addr1 and_val
     175                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     176                    set_arg_8 s addr1 and_val
    236177                ]
    237178            | inr r ⇒
    238179              let 〈addr1, addr2〉 ≝ r in
    239               let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
    240                set_flags ? s and_val (None ?) (get_ov_flag ? s)
     180              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
     181               set_flags … s and_val (None ?) (get_ov_flag ?? s)
    241182            ]
    242183        | ORL addr ⇒
     
    247188                [ inl l' ⇒
    248189                  let 〈addr1, addr2〉 ≝ l' in
    249                   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
     190                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     191                    set_arg_8 s addr1 or_val
    251192                | inr r ⇒
    252193                  let 〈addr1, addr2〉 ≝ r in
    253                   let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    254                     set_arg_8 ? s addr1 or_val
     194                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     195                    set_arg_8 s addr1 or_val
    255196                ]
    256197            | inr r ⇒
    257198              let 〈addr1, addr2〉 ≝ r in
    258               let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
    259                set_flags ? s or_val (None ?) (get_ov_flag ? s)
     199              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
     200               set_flags … s or_val (None ?) (get_ov_flag … s)
    260201            ]
    261202        | XRL addr ⇒
     
    264205            [ inl l' ⇒
    265206              let 〈addr1, addr2〉 ≝ l' in
    266               let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    267                 set_arg_8 ? s addr1 xor_val
     207              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     208                set_arg_8 s addr1 xor_val
    268209            | inr r ⇒
    269210              let 〈addr1, addr2〉 ≝ r in
    270               let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    271                 set_arg_8 ? s addr1 xor_val
     211              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     212                set_arg_8 s addr1 xor_val
    272213            ]
    273214        | INC addr ⇒
    274             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
     215            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
    275216              [ ACC_A ⇒ λacc_a: True.
    276217                let s' ≝ add_ticks1 s in
    277                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in
    278                  set_arg_8 ? s' ACC_A result
     218                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s' true ACC_A) (bitvector_of_nat 8 1) in
     219                 set_arg_8 s' ACC_A result
    279220              | REGISTER r ⇒ λregister: True.
    280221                let s' ≝ add_ticks1 s in
    281                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in
    282                  set_arg_8 ? s' (REGISTER r) result
     222                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s' true (REGISTER r)) (bitvector_of_nat 8 1) in
     223                 set_arg_8 s' (REGISTER r) result
    283224              | DIRECT d ⇒ λdirect: True.
    284225                let s' ≝ add_ticks1 s in
    285                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in
    286                  set_arg_8 ? s' (DIRECT d) result
     226                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s' true (DIRECT d)) (bitvector_of_nat 8 1) in
     227                 set_arg_8 s' (DIRECT d) result
    287228              | INDIRECT i ⇒ λindirect: True.
    288229                let s' ≝ add_ticks1 s in
    289                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
    290                  set_arg_8 ? s' (INDIRECT i) result
     230                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
     231                 set_arg_8 s' (INDIRECT i) result
    291232              | DPTR ⇒ λdptr: True.
    292233                let s' ≝ add_ticks1 s in
    293                 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s' SFR_DPL) (bitvector_of_nat 8 1) in
    294                 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in
    295                 let s ≝ set_8051_sfr ? s' SFR_DPL bl in
    296                  set_8051_sfr ? s' SFR_DPH bu
     234                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s' SFR_DPL) (bitvector_of_nat 8 1) in
     235                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s' SFR_DPH) (zero 8) carry in
     236                let s ≝ set_8051_sfr s' SFR_DPL bl in
     237                 set_8051_sfr s' SFR_DPH bu
    297238              | _ ⇒ λother: False. ⊥
    298239              ] (subaddressing_modein … addr)
     
    302243        | DEC addr ⇒
    303244           let s ≝ add_ticks1 s in
    304            let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
    305              set_arg_8 ? s addr result
     245           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat 8 1) false in
     246             set_arg_8 s addr result
    306247        | MUL addr1 addr2 ⇒
    307248           let s ≝ add_ticks1 s in
    308            let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
    309            let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
     249           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
     250           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
    310251           let product ≝ acc_a_nat * acc_b_nat in
    311252           let ov_flag ≝ product ≥ 256 in
    312253           let low ≝ bitvector_of_nat 8 (product mod 256) in
    313254           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
    314            let s ≝ set_8051_sfr ? s SFR_ACC_A low in
    315              set_8051_sfr ? s SFR_ACC_B high
     255           let s ≝ set_8051_sfr s SFR_ACC_A low in
     256             set_8051_sfr s SFR_ACC_B high
    316257        | DIV addr1 addr2 ⇒
    317258           let s ≝ add_ticks1 s in
    318            let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
    319            let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
     259           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
     260           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
    320261             match acc_b_nat with
    321                [ O ⇒ set_flags ? s false (None Bit) true
     262               [ O ⇒ set_flags s false (None Bit) true
    322263               | S o ⇒
    323264                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
    324265                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
    325                  let s ≝ set_8051_sfr ? s SFR_ACC_A q in
    326                  let s ≝ set_8051_sfr ? s SFR_ACC_B r in
    327                    set_flags ? s false (None Bit) false
     266                 let s ≝ set_8051_sfr s SFR_ACC_A q in
     267                 let s ≝ set_8051_sfr s SFR_ACC_B r in
     268                   set_flags s false (None Bit) false
    328269               ]
    329270        | DA addr ⇒
    330271            let s ≝ add_ticks1 s in
    331             let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
    332               if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
    333                 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
     272            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr s SFR_ACC_A) in
     273              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag s) then
     274                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat 8 6) false in
    334275                let cy_flag ≝ get_index' ? O ? flags in
    335276                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     
    337278                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
    338279                    let new_acc ≝ nu @@ acc_nl' in
    339                     let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
    340                       set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
     280                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
     281                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
    341282                  else
    342283                    s
     
    344285                s
    345286        | CLR addr ⇒
    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
     287          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
    347288            [ ACC_A ⇒ λacc_a: True.
    348289              let s ≝ add_ticks1 s in
    349                set_arg_8 ? s ACC_A (zero 8)
     290               set_arg_8 s ACC_A (zero 8)
    350291            | CARRY ⇒ λcarry: True.
    351292              let s ≝ add_ticks1 s in
    352                set_arg_1 ? s CARRY false
     293               set_arg_1 s CARRY false
    353294            | BIT_ADDR b ⇒ λbit_addr: True.
    354295              let s ≝ add_ticks1 s in
    355                set_arg_1 ? s (BIT_ADDR b) false
     296               set_arg_1 s (BIT_ADDR b) false
    356297            | _ ⇒ λother: False. ⊥
    357298            ] (subaddressing_modein … addr)
    358299        | CPL addr ⇒
    359           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
     300          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
    360301            [ ACC_A ⇒ λacc_a: True.
    361302                let s ≝ add_ticks1 s in
    362                 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     303                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    363304                let new_acc ≝ negation_bv ? old_acc in
    364                  set_8051_sfr ? s SFR_ACC_A new_acc
     305                 set_8051_sfr s SFR_ACC_A new_acc
    365306            | CARRY ⇒ λcarry: True.
    366307                let s ≝ add_ticks1 s in
    367                 let old_cy_flag ≝ get_arg_1 ? s CARRY true in
     308                let old_cy_flag ≝ get_arg_1 s CARRY true in
    368309                let new_cy_flag ≝ ¬old_cy_flag in
    369                  set_arg_1 ? s CARRY new_cy_flag
     310                 set_arg_1 s CARRY new_cy_flag
    370311            | BIT_ADDR b ⇒ λbit_addr: True.
    371312                let s ≝ add_ticks1 s in
    372                 let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
     313                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
    373314                let new_bit ≝ ¬old_bit in
    374                  set_arg_1 ? s (BIT_ADDR b) new_bit
     315                 set_arg_1 s (BIT_ADDR b) new_bit
    375316            | _ ⇒ λother: False. ?
    376317            ] (subaddressing_modein … addr)
    377318        | SETB b ⇒
    378319            let s ≝ add_ticks1 s in
    379             set_arg_1 ? s b false
     320            set_arg_1 s b false
    380321        | RL _ ⇒ (* DPM: always ACC_A *)
    381322            let s ≝ add_ticks1 s in
    382             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     323            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    383324            let new_acc ≝ rotate_left … 1 old_acc in
    384               set_8051_sfr ? s SFR_ACC_A new_acc
     325              set_8051_sfr s SFR_ACC_A new_acc
    385326        | RR _ ⇒ (* DPM: always ACC_A *)
    386327            let s ≝ add_ticks1 s in
    387             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     328            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    388329            let new_acc ≝ rotate_right … 1 old_acc in
    389               set_8051_sfr ? s SFR_ACC_A new_acc
     330              set_8051_sfr s SFR_ACC_A new_acc
    390331        | RLC _ ⇒ (* DPM: always ACC_A *)
    391332            let s ≝ add_ticks1 s in
    392             let old_cy_flag ≝ get_cy_flag ? s in
    393             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     333            let old_cy_flag ≝ get_cy_flag ?? s in
     334            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    394335            let new_cy_flag ≝ get_index' ? O ? old_acc in
    395336            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
    396             let s ≝ set_arg_1 ? s CARRY new_cy_flag in
    397               set_8051_sfr ? s SFR_ACC_A new_acc
     337            let s ≝ set_arg_1 s CARRY new_cy_flag in
     338              set_8051_sfr s SFR_ACC_A new_acc
    398339        | RRC _ ⇒ (* DPM: always ACC_A *)
    399340            let s ≝ add_ticks1 s in
    400             let old_cy_flag ≝ get_cy_flag ? s in
    401             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     341            let old_cy_flag ≝ get_cy_flag ?? s in
     342            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    402343            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
    403344            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
    404             let s ≝ set_arg_1 ? s CARRY new_cy_flag in
    405               set_8051_sfr ? s SFR_ACC_A new_acc
     345            let s ≝ set_arg_1 s CARRY new_cy_flag in
     346              set_8051_sfr s SFR_ACC_A new_acc
    406347        | SWAP _ ⇒ (* DPM: always ACC_A *)
    407348            let s ≝ add_ticks1 s in
    408             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     349            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    409350            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
    410351            let new_acc ≝ nl @@ nu in
    411               set_8051_sfr ? s SFR_ACC_A new_acc
     352              set_8051_sfr s SFR_ACC_A new_acc
    412353        | PUSH addr ⇒
    413             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
     354            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
    414355              [ DIRECT d ⇒ λdirect: True.
    415356                let s ≝ add_ticks1 s in
    416                 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    417                 let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    418                   write_at_stack_pointer ? s d
     357                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     358                let s ≝ set_8051_sfr s SFR_SP new_sp in
     359                  write_at_stack_pointer s d
    419360              | _ ⇒ λother: False. ⊥
    420361              ] (subaddressing_modein … addr)
    421362        | POP addr ⇒
    422363            let s ≝ add_ticks1 s in
    423             let contents ≝ read_at_stack_pointer ? s in
    424             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    425             let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    426               set_arg_8 ? s addr contents
     364            let contents ≝ read_at_stack_pointer ?? s in
     365            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
     366            let s ≝ set_8051_sfr s SFR_SP new_sp in
     367              set_arg_8 s addr contents
    427368        | XCH addr1 addr2 ⇒
    428369            let s ≝ add_ticks1 s in
    429             let old_addr ≝ get_arg_8 ? s false addr2 in
    430             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    431             let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
    432               set_arg_8 ? s addr2 old_acc
     370            let old_addr ≝ get_arg_8 s false addr2 in
     371            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     372            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
     373              set_arg_8 s addr2 old_acc
    433374        | XCHD addr1 addr2 ⇒
    434375            let s ≝ add_ticks1 s in
    435             let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
    436             let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
     376            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr s SFR_ACC_A) in
     377            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 s false addr2) in
    437378            let new_acc ≝ acc_nu @@ arg_nl in
    438379            let new_arg ≝ arg_nu @@ acc_nl in
    439             let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
    440               set_arg_8 ? s addr2 new_arg
     380            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
     381              set_arg_8 s addr2 new_arg
    441382        | RET ⇒
    442383            let s ≝ add_ticks1 s in
    443             let high_bits ≝ read_at_stack_pointer ? s in
    444             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    445             let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    446             let low_bits ≝ read_at_stack_pointer ? s in
    447             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    448             let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     384            let high_bits ≝ read_at_stack_pointer ?? s in
     385            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
     386            let s ≝ set_8051_sfr s SFR_SP new_sp in
     387            let low_bits ≝ read_at_stack_pointer ?? s in
     388            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
     389            let s ≝ set_8051_sfr s SFR_SP new_sp in
    449390            let new_pc ≝ high_bits @@ low_bits in
    450               set_program_counter ? s new_pc
     391              set_program_counter s new_pc
    451392        | RETI ⇒
    452393            let s ≝ add_ticks1 s in
    453             let high_bits ≝ read_at_stack_pointer ? s in
    454             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    455             let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    456             let low_bits ≝ read_at_stack_pointer ? s in
    457             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    458             let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     394            let high_bits ≝ read_at_stack_pointer ?? s in
     395            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
     396            let s ≝ set_8051_sfr s SFR_SP new_sp in
     397            let low_bits ≝ read_at_stack_pointer ?? s in
     398            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
     399            let s ≝ set_8051_sfr s SFR_SP new_sp in
    459400            let new_pc ≝ high_bits @@ low_bits in
    460               set_program_counter ? s new_pc
     401              set_program_counter s new_pc
    461402        | MOVX addr ⇒
    462403          let s ≝ add_ticks1 s in
     
    465406            [ inl l ⇒
    466407              let 〈addr1, addr2〉 ≝ l in
    467                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     408                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    468409            | inr r ⇒
    469410              let 〈addr1, addr2〉 ≝ r in
    470                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     411                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    471412            ]
    472413        | MOV addr ⇒
     
    483424                            [ inl l'''' ⇒
    484425                              let 〈addr1, addr2〉 ≝ l'''' in
    485                                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     426                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    486427                            | inr r'''' ⇒
    487428                              let 〈addr1, addr2〉 ≝ r'''' in
    488                                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     429                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    489430                            ]
    490431                        | inr r''' ⇒
    491432                          let 〈addr1, addr2〉 ≝ r''' in
    492                             set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     433                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    493434                        ]
    494435                    | inr r'' ⇒
    495436                      let 〈addr1, addr2〉 ≝ r'' in
    496                        set_arg_16 ? s (get_arg_16 ? s addr2) addr1
     437                       set_arg_16 … s (get_arg_16 … s addr2) addr1
    497438                    ]
    498439                | inr r ⇒
    499440                  let 〈addr1, addr2〉 ≝ r in
    500                    set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
     441                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
    501442                ]
    502443            | inr r ⇒
    503444              let 〈addr1, addr2〉 ≝ r in
    504                set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
     445               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
    505446            ]
    506447          | JC addr ⇒
    507                   if get_cy_flag ? s then
     448                  if get_cy_flag ?? s then
    508449                    let s ≝ add_ticks1 s in
    509                       set_program_counter ? s (addr_of addr s)
     450                      set_program_counter s (addr_of addr s)
    510451                  else
    511452                    let s ≝ add_ticks2 s in
    512453                      s
    513454            | JNC addr ⇒
    514                   if ¬(get_cy_flag ? s) then
     455                  if ¬(get_cy_flag ?? s) then
    515456                   let s ≝ add_ticks1 s in
    516                      set_program_counter ? s (addr_of addr s)
     457                     set_program_counter s (addr_of addr s)
    517458                  else
    518459                   let s ≝ add_ticks2 s in
    519460                    s
    520461            | JB addr1 addr2 ⇒
    521                   if get_arg_1 ? s addr1 false then
     462                  if get_arg_1 s addr1 false then
    522463                   let s ≝ add_ticks1 s in
    523                     set_program_counter ? s (addr_of addr2 s)
     464                    set_program_counter s (addr_of addr2 s)
    524465                  else
    525466                   let s ≝ add_ticks2 s in
    526467                    s
    527468            | JNB addr1 addr2 ⇒
    528                   if ¬(get_arg_1 ? s addr1 false) then
     469                  if ¬(get_arg_1 s addr1 false) then
    529470                   let s ≝ add_ticks1 s in
    530                     set_program_counter ? s (addr_of addr2 s)
     471                    set_program_counter s (addr_of addr2 s)
    531472                  else
    532473                   let s ≝ add_ticks2 s in
    533474                    s
    534475            | JBC addr1 addr2 ⇒
    535                   let s ≝ set_arg_1 ? s addr1 false in
    536                     if get_arg_1 ? s addr1 false then
     476                  let s ≝ set_arg_1 s addr1 false in
     477                    if get_arg_1 s addr1 false then
    537478                     let s ≝ add_ticks1 s in
    538                       set_program_counter ? s (addr_of addr2 s)
     479                      set_program_counter s (addr_of addr2 s)
    539480                    else
    540481                     let s ≝ add_ticks2 s in
    541482                      s
    542483            | JZ addr ⇒
    543                     if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
     484                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then
    544485                     let s ≝ add_ticks1 s in
    545                       set_program_counter ? s (addr_of addr s)
     486                      set_program_counter s (addr_of addr s)
    546487                    else
    547488                     let s ≝ add_ticks2 s in
    548489                      s
    549490            | JNZ addr ⇒
    550                     if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
     491                    if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
    551492                     let s ≝ add_ticks1 s in
    552                       set_program_counter ? s (addr_of addr s)
     493                      set_program_counter s (addr_of addr s)
    553494                    else
    554495                     let s ≝ add_ticks2 s in
     
    558499                    [ inl l ⇒
    559500                        let 〈addr1, addr2'〉 ≝ l in
    560                         let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
    561                                                  (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
    562                           if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
     501                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
     502                                                 (nat_of_bitvector ? (get_arg_8 s false addr2')) in
     503                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
    563504                            let s ≝ add_ticks1 s in
    564                             let s ≝ set_program_counter ? s (addr_of addr2 s) in
    565                               set_flags ? s new_cy (None ?) (get_ov_flag ? s)
     505                            let s ≝ set_program_counter s (addr_of addr2 s) in
     506                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
    566507                          else
    567508                            let s ≝ add_ticks2 s in
    568                               set_flags ? s new_cy (None ?) (get_ov_flag ? s)
     509                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
    569510                    | inr r' ⇒
    570511                        let 〈addr1, addr2'〉 ≝ r' in
    571                         let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
    572                                                  (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
    573                           if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
     512                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
     513                                                 (nat_of_bitvector ? (get_arg_8 s false addr2')) in
     514                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
    574515                            let s ≝ add_ticks1 s in
    575                             let s ≝ set_program_counter ? s (addr_of addr2 s) in
    576                               set_flags ? s new_cy (None ?) (get_ov_flag ? s)
     516                            let s ≝ set_program_counter s (addr_of addr2 s) in
     517                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
    577518                          else
    578519                            let s ≝ add_ticks2 s in
    579                               set_flags ? s new_cy (None ?) (get_ov_flag ? s)
     520                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
    580521                    ]
    581522            | DJNZ addr1 addr2 ⇒
    582               let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
    583               let s ≝ set_arg_8 ? s addr1 result in
     523              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
     524              let s ≝ set_arg_8 s addr1 result in
    584525                if ¬(eq_bv ? result (zero 8)) then
    585526                 let s ≝ add_ticks1 s in
    586                   set_program_counter ? s (addr_of addr2 s)
     527                  set_program_counter s (addr_of addr2 s)
    587528                else
    588529                 let s ≝ add_ticks2 s in
    589530                  s
    590         ]. (*15s*)
     531 |_ ⇒ ?            ]. (*15s*)
    591532    try (cases(other))
    592533    try assumption (*20s*)
     
    597538    ) (*66s*)
    598539    normalize nodelta /2 by or_introl, or_intror/ (*35s*)
     540    (*CSC: the times are now much longer. I suspect because the inclusion of
     541      all StatusProofs makes the search space larger :-( *)
    599542qed.
    600543
    601544definition execute_1_preinstruction:
    602545  ∀ticks: nat × nat.
    603   ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a →
    604   PreStatus m → PreStatus m ≝ execute_1_preinstruction'.
     546  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
     547  PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'.
    605548 
    606549lemma execute_1_preinstruction_ok:
    607  ∀ticks,a,m,f,i,s.
    608   clock ? (execute_1_preinstruction ticks a m f i s) = \fst ticks + clock … s ∨
    609   clock ? (execute_1_preinstruction ticks a m f i s) = \snd ticks + clock … s.
    610  #ticks #a #m #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
     550 ∀ticks,a,m,cm,f,i,s.
     551  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
     552  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s.
     553 #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
    611554qed.
    612555
    613 definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat.
    614   Σs': Status. clock … s' = \snd current + clock … s ≝
    615   λs0,instr_pc_ticks.
     556definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
     557  Σs': Status cm. clock ?? s' = \snd current + clock … s ≝
     558  λcm,s0,instr_pc_ticks.
    616559    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    617560    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    618     let s ≝ set_program_counter ? s0 pc in
    619       match instr return λ_.Status with
    620       [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?
     561    let s ≝ set_program_counter s0 pc in
     562      match instr return λ_.Status cm with
     563      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]]
    621564        (λx. λs.
    622565        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    623         [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
     566        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter s) (sign_extension r))
    624567        | _ ⇒ λabsd. ⊥
    625568        ] (subaddressing_modein … x)) instr s
    626569      | MOVC addr1 addr2 ⇒
    627           let s ≝ set_clock ? s (ticks + clock ? s) in
    628           match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     570          let s ≝ set_clock … s (ticks + clock … s) in
     571          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    629572            [ ACC_DPTR ⇒ λacc_dptr: True.
    630               let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    631               let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
     573              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     574              let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    632575              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
    633               let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
    634                 set_8051_sfr ? s SFR_ACC_A result
     576              let result ≝ lookup ? ? new_addr cm (zero ?) in
     577                set_8051_sfr s SFR_ACC_A result
    635578            | ACC_PC ⇒ λacc_pc: True.
    636               let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    637               let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
     579              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     580              let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ?? s) (bitvector_of_nat 16 1) in
    638581              (* DPM: Under specified: does the carry from PC incrementation affect the *)
    639582              (*      addition of the PC with the DPTR? At the moment, no.              *)
    640               let s ≝ set_program_counter ? s inc_pc in
     583              let s ≝ set_program_counter s inc_pc in
    641584              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
    642               let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
    643                 set_8051_sfr ? s SFR_ACC_A result
     585              let result ≝ lookup ? ? new_addr cm (zero ?) in
     586                set_8051_sfr s SFR_ACC_A result
    644587            | _ ⇒ λother: False. ⊥
    645588            ] (subaddressing_modein … addr2)
    646589      | JMP _ ⇒ (* DPM: always indirect_dptr *)
    647           let s ≝ set_clock ? s (ticks + clock ? s) in
    648           let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    649           let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
     590          let s ≝ set_clock … s (ticks + clock … s) in
     591          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
     592          let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    650593          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
    651           let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
    652             set_program_counter ? s new_pc
     594          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
     595            set_program_counter s new_pc
    653596      | LJMP addr ⇒
    654           let s ≝ set_clock ? s (ticks + clock ? s) in
    655           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     597          let s ≝ set_clock … s (ticks + clock … s) in
     598          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    656599            [ ADDR16 a ⇒ λaddr16: True.
    657                 set_program_counter ? s a
     600                set_program_counter s a
    658601            | _ ⇒ λother: False. ⊥
    659602            ] (subaddressing_modein … addr)
    660603      | SJMP addr ⇒
    661           let s ≝ set_clock ? s (ticks + clock ? s) in
    662           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     604          let s ≝ set_clock … s (ticks + clock … s) in
     605          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    663606            [ RELATIVE r ⇒ λrelative: True.
    664                 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    665                   set_program_counter ? s new_pc
     607                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     608                  set_program_counter s new_pc
    666609            | _ ⇒ λother: False. ⊥
    667610            ] (subaddressing_modein … addr)
    668611      | AJMP addr ⇒
    669           let s ≝ set_clock ? s (ticks + clock ? s) in
    670           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     612          let s ≝ set_clock … s (ticks + clock … s) in
     613          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    671614            [ ADDR11 a ⇒ λaddr11: True.
    672               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     615              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    673616              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
    674617              let bit ≝ get_index' ? O ? nl in
    675618              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
    676619              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    677               let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
    678                 set_program_counter ? s new_pc
     620              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
     621                set_program_counter s new_pc
    679622            | _ ⇒ λother: False. ⊥
    680623            ] (subaddressing_modein … addr)
    681624      | ACALL addr ⇒
    682           let s ≝ set_clock ? s (ticks + clock ? s) in
    683           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     625          let s ≝ set_clock … s (ticks + clock … s) in
     626          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    684627            [ ADDR11 a ⇒ λaddr11: True.
    685               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    686               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    687               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    688               let s ≝ write_at_stack_pointer ? s pc_bl in
    689               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    690               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    691               let s ≝ write_at_stack_pointer ? s pc_bu in
     628              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     629              let s ≝ set_8051_sfr s SFR_SP new_sp in
     630              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     631              let s ≝ write_at_stack_pointer s pc_bl in
     632              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     633              let s ≝ set_8051_sfr s SFR_SP new_sp in
     634              let s ≝ write_at_stack_pointer s pc_bu in
    692635              let 〈thr, eig〉 ≝ split ? 3 8 a in
    693636              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
    694637              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    695                 set_program_counter ? s new_addr
     638                set_program_counter s new_addr
    696639            | _ ⇒ λother: False. ⊥
    697640            ] (subaddressing_modein … addr)
    698641        | LCALL addr ⇒
    699           let s ≝ set_clock ? s (ticks + clock ? s) in
    700           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     642          let s ≝ set_clock … s (ticks + clock … s) in
     643          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    701644            [ ADDR16 a ⇒ λaddr16: True.
    702               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    703               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    704               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    705               let s ≝ write_at_stack_pointer ? s pc_bl in
    706               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    707               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    708               let s ≝ write_at_stack_pointer ? s pc_bu in
    709                 set_program_counter ? s a
     645              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     646              let s ≝ set_8051_sfr s SFR_SP new_sp in
     647              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     648              let s ≝ write_at_stack_pointer s pc_bl in
     649              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     650              let s ≝ set_8051_sfr s SFR_SP new_sp in
     651              let s ≝ write_at_stack_pointer s pc_bu in
     652                set_program_counter s a
    710653            | _ ⇒ λother: False. ⊥
    711654            ] (subaddressing_modein … addr)
    712       ]. (*10s*)
     655        ]. (*10s*)
    713656    [||||||||*:try assumption]
    714657    [1,2,3,4,5,7: @pi2 (*35s*)
    715     |8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ?
     658    |8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]]
    716659        (λx. λs.
    717660        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    718         [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
     661        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter s) (sign_extension r))
    719662        | _ ⇒ λabsd. ⊥
    720663        ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H
    721664    |*: normalize nodelta try // (*17s*)
    722         >set_program_counter_ignores_clock // (* Andrea:??*) ]
     665        >clock_set_program_counter // (* Andrea:??*) ]
    723666qed.
    724667
    725668definition current_instruction_cost ≝
    726   λs: Status.
    727     \snd (fetch (code_memory … s) (program_counter … s)).
    728 
    729 definition execute_1': ∀s:Status.
    730   Σs':Status. clock … s' = current_instruction_cost s + clock … s ≝
    731   λs: Status.
    732     let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
    733      execute_1_0 s instr_pc_ticks.
    734 
    735 definition execute_1: Status → Status ≝ execute_1'.
    736 
    737 lemma execute_1_ok: ∀s. clock … (execute_1 s) = current_instruction_cost s + clock … s.
    738  #s whd in match execute_1; normalize nodelta @pi2
     669  λcm.λs: Status cm.
     670    \snd (fetch cm (program_counter … s)).
     671
     672definition execute_1': ∀cm.∀s:Status cm.
     673  Σs':Status cm. clock ?? s' = current_instruction_cost cm s + clock … s ≝
     674  λcm. λs: Status cm.
     675    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
     676     execute_1_0 cm s instr_pc_ticks.
     677
     678definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.
     679
     680lemma execute_1_ok: ∀cm.∀s. clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
     681 #cm #s whd in match execute_1; normalize nodelta @pi2
    739682qed-. (*x Andrea: indexing takes ages here *)
    740683
    741 definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus
    742   λticks,s,instr,pc.
    743   let s ≝ set_program_counter ? s pc in
     684definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm
     685  λticks,cm,s,instr,pc.
     686  let s ≝ set_program_counter ?? s pc in
    744687  let s ≝
    745688    match instr with
    746     [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
    747     | Comment cmt ⇒
    748        let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    749         s
     689    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s
     690    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
    750691    | Cost cst ⇒ s
    751692    | Jmp jmp ⇒
    752        let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    753         set_program_counter ? s (address_of_word_labels s jmp)
     693       let s ≝ set_clock … s (\fst ticks + clock … s) in
     694        set_program_counter … s (address_of_word_labels cm jmp)
    754695    | Call call ⇒
    755       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    756       let a ≝ address_of_word_labels s call in
    757       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    758       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    759       let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    760       let s ≝ write_at_stack_pointer ? s pc_bl in
    761       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    762       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    763       let s ≝ write_at_stack_pointer ? s pc_bu in
    764         set_program_counter ? s a
     696      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
     697      let a ≝ address_of_word_labels cm call in
     698      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     699      let s ≝ set_8051_sfr s SFR_SP new_sp in
     700      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     701      let s ≝ write_at_stack_pointer s pc_bl in
     702      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     703      let s ≝ set_8051_sfr s SFR_SP new_sp in
     704      let s ≝ write_at_stack_pointer s pc_bu in
     705        set_program_counter s a
    765706    | Mov dptr ident ⇒
    766       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    767       let the_preamble ≝ \fst (code_memory ? s) in
     707      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
     708      let the_preamble ≝ \fst cm in
    768709      let data_labels ≝ construct_datalabels the_preamble in
    769         set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
     710        set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
    770711    ]
    771712  in
     
    775716qed.
    776717
    777 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus
    778   λticks_of,s.
    779   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
    780   let ticks ≝ ticks_of (program_counter ? s) in
    781    execute_1_pseudo_instruction0 ticks s instr pc.
    782 
    783 let rec execute (n: nat) (s: Status) on n: Status
     718definition execute_1_pseudo_instruction: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm
     719  λticks_of,cm,s.
     720  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in
     721  let ticks ≝ ticks_of (program_counter s) in
     722   execute_1_pseudo_instruction0 ticks cm s instr pc.
     723
     724let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm
    784725  match n with
    785726    [ O ⇒ s
    786     | S o ⇒ execute o (execute_1 s)
     727    | S o ⇒ execute o … (execute_1 … s)
    787728    ].
    788729
    789 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus
     730let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm
    790731  match n with
    791732    [ O ⇒ s
    792     | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
     733    | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
    793734    ].
Note: See TracChangeset for help on using the changeset viewer.