Changeset 821


Ignore:
Timestamp:
May 23, 2011, 3:23:17 PM (8 years ago)
Author:
mulligan
Message:

changes to introduce pseudostatus

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r820 r821  
    158158include alias "ASM/BitVectorTrie.ma".
    159159
    160 definition execute_1_preinstruction: ∀A: Type[0]. (A → Byte) → preinstruction A → Status → Status
    161   λA: Type[0].
     160definition execute_1_preinstruction: ∀A, M: Type[0]. (A → Byte) → preinstruction A → PreStatus M → PreStatus M
     161  λA, M: Type[0].
    162162  λaddr_of: A → Byte.
    163163  λinstr: preinstruction A.
    164   λs: Status.
     164  λs: PreStatus M.
    165165  match instr with
    166166        [ ADD addr1 addr2 ⇒
    167             let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
    168                                                    (get_arg_8 s false addr2) false in
     167            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
     168                                                   (get_arg_8 ? s false addr2) false in
    169169            let cy_flag ≝ get_index' ? O  ? flags in
    170170            let ac_flag ≝ get_index' ? 1 ? flags in
    171171            let ov_flag ≝ get_index' ? 2 ? flags in
    172             let s ≝ set_arg_8 s ACC_A result in
    173               set_flags s cy_flag (Some Bit ac_flag) ov_flag
     172            let s ≝ set_arg_8 ? s ACC_A result in
     173              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
    174174        | ADDC addr1 addr2 ⇒
    175             let old_cy_flag ≝ get_cy_flag s in
    176             let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
    177                                                    (get_arg_8 s false addr2) old_cy_flag in
     175            let old_cy_flag ≝ get_cy_flag ? s in
     176            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
     177                                                   (get_arg_8 ? s false addr2) old_cy_flag in
    178178            let cy_flag ≝ get_index' ? O ? flags in
    179179            let ac_flag ≝ get_index' ? 1 ? flags in
    180180            let ov_flag ≝ get_index' ? 2 ? flags in
    181             let s ≝ set_arg_8 s ACC_A result in
    182               set_flags s cy_flag (Some Bit ac_flag) ov_flag
     181            let s ≝ set_arg_8 ? s ACC_A result in
     182              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
    183183        | SUBB addr1 addr2 ⇒
    184             let old_cy_flag ≝ get_cy_flag s in
    185             let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
    186                                                    (get_arg_8 s false addr2) old_cy_flag in
     184            let old_cy_flag ≝ get_cy_flag ? s in
     185            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
     186                                                   (get_arg_8 ? s false addr2) old_cy_flag in
    187187            let cy_flag ≝ get_index' ? O ? flags in
    188188            let ac_flag ≝ get_index' ? 1 ? flags in
    189189            let ov_flag ≝ get_index' ? 2 ? flags in
    190             let s ≝ set_arg_8 s ACC_A result in
    191               set_flags s cy_flag (Some Bit ac_flag) ov_flag
     190            let s ≝ set_arg_8 ? s ACC_A result in
     191              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
    192192        | ANL addr ⇒
    193193          match addr with
     
    196196                [ inl l' ⇒
    197197                  let 〈addr1, addr2〉 ≝ l' in
    198                   let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    199                     set_arg_8 s addr1 and_val
     198                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
     199                    set_arg_8 ? s addr1 and_val
    200200                | inr r ⇒
    201201                  let 〈addr1, addr2〉 ≝ r in
    202                   let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    203                     set_arg_8 s addr1 and_val
     202                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
     203                    set_arg_8 ? s addr1 and_val
    204204                ]
    205205            | inr r ⇒
    206206              let 〈addr1, addr2〉 ≝ r in
    207               let and_val ≝ (get_cy_flag s) ∧ (get_arg_1 s addr2 true) in
    208                 set_flags s and_val (None ?) (get_ov_flag s)
     207              let and_val ≝ (get_cy_flag ? s) ∧ (get_arg_1 ? s addr2 true) in
     208                set_flags ? s and_val (None ?) (get_ov_flag ? s)
    209209            ]
    210210        | ORL addr ⇒
     
    214214                [ inl l' ⇒
    215215                  let 〈addr1, addr2〉 ≝ l' in
    216                   let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    217                     set_arg_8 s addr1 or_val
     216                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
     217                    set_arg_8 ? s addr1 or_val
    218218                | inr r ⇒
    219219                  let 〈addr1, addr2〉 ≝ r in
    220                   let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    221                     set_arg_8 s addr1 or_val
     220                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
     221                    set_arg_8 ? s addr1 or_val
    222222                ]
    223223            | inr r ⇒
    224224              let 〈addr1, addr2〉 ≝ r in
    225               let or_val ≝ (get_cy_flag s) ∨ (get_arg_1 s addr2 true) in
    226                 set_flags s or_val (None ?) (get_ov_flag s)
     225              let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
     226                set_flags ? s or_val (None ?) (get_ov_flag ? s)
    227227            ]
    228228        | XRL addr ⇒
     
    230230            [ inl l' ⇒
    231231              let 〈addr1, addr2〉 ≝ l' in
    232               let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    233                 set_arg_8 s addr1 xor_val
     232              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
     233                set_arg_8 ? s addr1 xor_val
    234234            | inr r ⇒
    235235              let 〈addr1, addr2〉 ≝ r in
    236               let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    237                 set_arg_8 s addr1 xor_val
     236              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
     237                set_arg_8 ? s addr1 xor_val
    238238            ]
    239239        | INC addr ⇒
     
    244244                                                           dptr ]] x) → ? with
    245245              [ ACC_A ⇒ λacc_a: True.
    246                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat 8 1) in
    247                   set_arg_8 s ACC_A result
     246                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true ACC_A) (bitvector_of_nat 8 1) in
     247                  set_arg_8 ? s ACC_A result
    248248              | REGISTER r ⇒ λregister: True.
    249                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat 8 1) in
    250                   set_arg_8 s (REGISTER r) result
     249                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (REGISTER r)) (bitvector_of_nat 8 1) in
     250                  set_arg_8 ? s (REGISTER r) result
    251251              | DIRECT d ⇒ λdirect: True.
    252                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat 8 1) in
    253                   set_arg_8 s (DIRECT d) result
     252                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (DIRECT d)) (bitvector_of_nat 8 1) in
     253                  set_arg_8 ? s (DIRECT d) result
    254254              | INDIRECT i ⇒ λindirect: True.
    255                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat 8 1) in
    256                   set_arg_8 s (INDIRECT i) result
     255                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (INDIRECT i)) (bitvector_of_nat 8 1) in
     256                  set_arg_8 ? s (INDIRECT i) result
    257257              | DPTR ⇒ λdptr: True.
    258                 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat 8 1) in
    259                 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero 8) carry in
    260                 let s ≝ set_8051_sfr s SFR_DPL bl in
    261                   set_8051_sfr s SFR_DPH bu
     258                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s SFR_DPL) (bitvector_of_nat 8 1) in
     259                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s SFR_DPH) (zero 8) carry in
     260                let s ≝ set_8051_sfr ? s SFR_DPL bl in
     261                  set_8051_sfr ? s SFR_DPH bu
    262262              | _ ⇒ λother: False. ⊥
    263263              ] (subaddressing_modein … addr)
    264264        | DEC addr ⇒
    265            let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat 8 1) false in
    266              set_arg_8 s addr result
     265           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
     266             set_arg_8 ? s addr result
    267267        | MUL addr1 addr2 ⇒
    268            let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
    269            let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
     268           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
     269           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
    270270           let product ≝ acc_a_nat * acc_b_nat in
    271271           let ov_flag ≝ product ≥ 256 in
    272272           let low ≝ bitvector_of_nat 8 (product mod 256) in
    273273           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
    274            let s ≝ set_8051_sfr s SFR_ACC_A low in
    275              set_8051_sfr s SFR_ACC_B high
     274           let s ≝ set_8051_sfr ? s SFR_ACC_A low in
     275             set_8051_sfr ? s SFR_ACC_B high
    276276        | DIV addr1 addr2 ⇒
    277            let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
    278            let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
     277           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
     278           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
    279279             match acc_b_nat with
    280                [ O ⇒ set_flags s false (None Bit) true
     280               [ O ⇒ set_flags ? s false (None Bit) true
    281281               | S o ⇒
    282282                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
    283283                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
    284                  let s ≝ set_8051_sfr s SFR_ACC_A q in
    285                  let s ≝ set_8051_sfr s SFR_ACC_B r in
    286                    set_flags s false (None Bit) false
     284                 let s ≝ set_8051_sfr ? s SFR_ACC_A q in
     285                 let s ≝ set_8051_sfr ? s SFR_ACC_B r in
     286                   set_flags ? s false (None Bit) false
    287287               ]
    288288        | DA addr ⇒
    289             let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_ACC_A) in
    290               if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag s) then
    291                 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat 8 6) false in
     289            let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
     290              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
     291                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
    292292                let cy_flag ≝ get_index' ? O ? flags in
    293293                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     
    295295                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
    296296                    let new_acc ≝ nu @@ acc_nl' in
    297                     let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
    298                       set_flags s cy_flag (Some ? (get_ac_flag s)) (get_ov_flag s)
     297                    let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
     298                      set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
    299299                  else
    300300                    s
     
    303303        | CLR addr ⇒
    304304          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    305             [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero 8)
    306             | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
    307             | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
     305            [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8)
     306            | CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false
     307            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false
    308308            | _ ⇒ λother: False. ⊥
    309309            ] (subaddressing_modein … addr)
     
    311311          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    312312            [ ACC_A ⇒ λacc_a: True.
    313                 let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     313                let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    314314                let new_acc ≝ negation_bv ? old_acc in
    315                   set_8051_sfr s SFR_ACC_A new_acc
     315                  set_8051_sfr ? s SFR_ACC_A new_acc
    316316            | CARRY ⇒ λcarry: True.
    317                 let old_cy_flag ≝ get_arg_1 s CARRY true in
     317                let old_cy_flag ≝ get_arg_1 ? s CARRY true in
    318318                let new_cy_flag ≝ ¬old_cy_flag in
    319                   set_arg_1 s CARRY new_cy_flag
     319                  set_arg_1 ? s CARRY new_cy_flag
    320320            | BIT_ADDR b ⇒ λbit_addr: True.
    321                 let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
     321                let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
    322322                let new_bit ≝ ¬old_bit in
    323                   set_arg_1 s (BIT_ADDR b) new_bit
     323                  set_arg_1 ? s (BIT_ADDR b) new_bit
    324324            | _ ⇒ λother: False. ?
    325325            ] (subaddressing_modein … addr)
    326         | SETB b ⇒ set_arg_1 s b false
     326        | SETB b ⇒ set_arg_1 ? s b false
    327327        | RL _ ⇒ (* DPM: always ACC_A *)
    328             let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     328            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    329329            let new_acc ≝ rotate_left … 1 old_acc in
    330               set_8051_sfr s SFR_ACC_A new_acc
     330              set_8051_sfr ? s SFR_ACC_A new_acc
    331331        | RR _ ⇒ (* DPM: always ACC_A *)
    332             let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     332            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    333333            let new_acc ≝ rotate_right … 1 old_acc in
    334               set_8051_sfr s SFR_ACC_A new_acc
     334              set_8051_sfr ? s SFR_ACC_A new_acc
    335335        | RLC _ ⇒ (* DPM: always ACC_A *)
    336             let old_cy_flag ≝ get_cy_flag s in
    337             let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     336            let old_cy_flag ≝ get_cy_flag ? s in
     337            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    338338            let new_cy_flag ≝ get_index' ? O ? old_acc in
    339339            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
    340             let s ≝ set_arg_1 s CARRY new_cy_flag in
    341               set_8051_sfr s SFR_ACC_A new_acc
     340            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
     341              set_8051_sfr ? s SFR_ACC_A new_acc
    342342        | RRC _ ⇒ (* DPM: always ACC_A *)
    343             let old_cy_flag ≝ get_cy_flag s in
    344             let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     343            let old_cy_flag ≝ get_cy_flag ? s in
     344            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    345345            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
    346346            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
    347             let s ≝ set_arg_1 s CARRY new_cy_flag in
    348               set_8051_sfr s SFR_ACC_A new_acc
     347            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
     348              set_8051_sfr ? s SFR_ACC_A new_acc
    349349        | SWAP _ ⇒ (* DPM: always ACC_A *)
    350             let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     350            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    351351            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
    352352            let new_acc ≝ nl @@ nu in
    353               set_8051_sfr s SFR_ACC_A new_acc
     353              set_8051_sfr ? s SFR_ACC_A new_acc
    354354        | PUSH addr ⇒
    355355            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
    356356              [ DIRECT d ⇒ λdirect: True.
    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
     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
    360360              | _ ⇒ λother: False. ⊥
    361361              ] (subaddressing_modein … addr)
    362362        | POP addr ⇒
    363             let contents ≝ read_at_stack_pointer s in
    364             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
    365             let s ≝ set_8051_sfr s SFR_SP new_sp in
    366               set_arg_8 s addr contents
     363            let contents ≝ read_at_stack_pointer ? s in
     364            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
     365            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     366              set_arg_8 ? s addr contents
    367367        | XCH addr1 addr2 ⇒
    368             let old_addr ≝ get_arg_8 s false addr2 in
    369             let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    370             let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
    371               set_arg_8 s addr2 old_acc
     368            let old_addr ≝ get_arg_8 ? s false addr2 in
     369            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     370            let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
     371              set_arg_8 ? s addr2 old_acc
    372372        | XCHD addr1 addr2 ⇒
    373             let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr s SFR_ACC_A) in
    374             let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 s false addr2) in
     373            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
     374            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
    375375            let new_acc ≝ acc_nu @@ arg_nl in
    376376            let new_arg ≝ arg_nu @@ acc_nl in
    377             let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
    378               set_arg_8 s addr2 new_arg
     377            let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
     378              set_arg_8 ? s addr2 new_arg
    379379        | RET ⇒
    380             let high_bits ≝ read_at_stack_pointer s in
    381             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
    382             let s ≝ set_8051_sfr s SFR_SP new_sp in
    383             let low_bits ≝ read_at_stack_pointer s in
    384             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
    385             let s ≝ set_8051_sfr s SFR_SP new_sp in
     380            let high_bits ≝ read_at_stack_pointer ? s in
     381            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
     382            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     383            let low_bits ≝ read_at_stack_pointer ? s in
     384            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
     385            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    386386            let new_pc ≝ high_bits @@ low_bits in
    387               set_program_counter s new_pc
     387              set_program_counter ? s new_pc
    388388        | RETI ⇒
    389             let high_bits ≝ read_at_stack_pointer s in
    390             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
    391             let s ≝ set_8051_sfr s SFR_SP new_sp in
    392             let low_bits ≝ read_at_stack_pointer s in
    393             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
    394             let s ≝ set_8051_sfr s SFR_SP new_sp in
     389            let high_bits ≝ read_at_stack_pointer ? s in
     390            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
     391            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     392            let low_bits ≝ read_at_stack_pointer ? s in
     393            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
     394            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    395395            let new_pc ≝ high_bits @@ low_bits in
    396               set_program_counter s new_pc
     396              set_program_counter ? s new_pc
    397397        | MOVX addr ⇒
    398398          (* DPM: only copies --- doesn't affect I/O *)
     
    400400            [ inl l ⇒
    401401              let 〈addr1, addr2〉 ≝ l in
    402                 set_arg_8 s addr1 (get_arg_8 s false addr2)
     402                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
    403403            | inr r ⇒
    404404              let 〈addr1, addr2〉 ≝ r in
    405                 set_arg_8 s addr1 (get_arg_8 s false addr2)
     405                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
    406406            ]
    407407        | MOV addr ⇒
     
    417417                            [ inl l'''' ⇒
    418418                              let 〈addr1, addr2〉 ≝ l'''' in
    419                                 set_arg_8 s addr1 (get_arg_8 s false addr2)
     419                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
    420420                            | inr r'''' ⇒
    421421                              let 〈addr1, addr2〉 ≝ r'''' in
    422                                 set_arg_8 s addr1 (get_arg_8 s false addr2)
     422                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
    423423                            ]
    424424                        | inr r''' ⇒
    425425                          let 〈addr1, addr2〉 ≝ r''' in
    426                             set_arg_8 s addr1 (get_arg_8 s false addr2)
     426                            set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
    427427                        ]
    428428                    | inr r'' ⇒
    429429                      let 〈addr1, addr2〉 ≝ r'' in
    430                         set_arg_16 s (get_arg_16 s addr2) addr1
     430                        set_arg_16 ? s (get_arg_16 ? s addr2) addr1
    431431                    ]
    432432                | inr r ⇒
    433433                  let 〈addr1, addr2〉 ≝ r in
    434                     set_arg_1 s addr1 (get_arg_1 s addr2 false)
     434                    set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
    435435                ]
    436436            | inr r ⇒
    437437              let 〈addr1, addr2〉 ≝ r in
    438                 set_arg_1 s addr1 (get_arg_1 s addr2 false)
     438                set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
    439439            ]
    440440          | JC addr ⇒
    441441              let r ≝ addr_of addr in
    442                   if get_cy_flag s then
    443                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    444                       set_program_counter s new_pc
     442                  if get_cy_flag ? s then
     443                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     444                      set_program_counter ? s new_pc
    445445                  else
    446446                    s
    447447            | JNC addr ⇒
    448448              let r ≝ addr_of addr in
    449                   if ¬(get_cy_flag s) then
    450                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    451                       set_program_counter s new_pc
     449                  if ¬(get_cy_flag ? s) then
     450                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     451                      set_program_counter ? s new_pc
    452452                  else
    453453                    s
    454454            | JB addr1 addr2 ⇒
    455455              let r ≝ addr_of addr2 in
    456                   if get_arg_1 s addr1 false then
    457                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    458                       set_program_counter s new_pc
     456                  if get_arg_1 ? s addr1 false then
     457                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     458                      set_program_counter ? s new_pc
    459459                  else
    460460                    s
    461461            | JNB addr1 addr2 ⇒
    462462              let r ≝ addr_of addr2 in
    463                   if ¬(get_arg_1 s addr1 false) then
    464                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    465                       set_program_counter s new_pc
     463                  if ¬(get_arg_1 ? s addr1 false) then
     464                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     465                      set_program_counter ? s new_pc
    466466                  else
    467467                    s
    468468            | JBC addr1 addr2 ⇒
    469469              let r ≝ addr_of addr2 in
    470                   let s ≝ set_arg_1 s addr1 false in
    471                     if get_arg_1 s addr1 false then
    472                       let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    473                         set_program_counter s new_pc
     470                  let s ≝ set_arg_1 ? s addr1 false in
     471                    if get_arg_1 ? s addr1 false then
     472                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     473                        set_program_counter ? s new_pc
    474474                    else
    475475                      s
    476476            | JZ addr ⇒
    477477              let r ≝ addr_of addr in
    478                     if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then
    479                       let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    480                         set_program_counter s new_pc
     478                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
     479                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     480                        set_program_counter ? s new_pc
    481481                    else
    482482                      s
    483483            | JNZ addr ⇒
    484484              let r ≝ addr_of addr in
    485                     if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
    486                       let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    487                         set_program_counter s new_pc
     485                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
     486                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     487                        set_program_counter ? s new_pc
    488488                    else
    489489                      s
     
    493493                    [ inl l ⇒
    494494                        let 〈addr1, addr2〉 ≝ l in
    495                         let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
    496                                                  (nat_of_bitvector ? (get_arg_8 s false addr2)) in
    497                           if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
    498                             let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    499                             let s ≝ set_program_counter s new_pc in
    500                               set_flags s new_cy (None ?) (get_ov_flag s)
     495                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
     496                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2)) in
     497                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2)) then
     498                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     499                            let s ≝ set_program_counter ? s new_pc in
     500                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    501501                          else
    502                             (set_flags s new_cy (None ?) (get_ov_flag s))
     502                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    503503                    | inr r' ⇒
    504504                        let 〈addr1, addr2〉 ≝ r' in
    505                         let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
    506                                                  (nat_of_bitvector ? (get_arg_8 s false addr2)) in
    507                           if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
    508                             let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    509                             let s ≝ set_program_counter s new_pc in
    510                               set_flags s new_cy (None ?) (get_ov_flag s)
     505                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
     506                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2)) in
     507                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2)) then
     508                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     509                            let s ≝ set_program_counter ? s new_pc in
     510                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    511511                          else
    512                             (set_flags s new_cy (None ?) (get_ov_flag s))
     512                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    513513                    ]
    514514            | DJNZ addr1 addr2 ⇒
    515515              let r ≝ addr_of addr2 in
    516               let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
    517               let s ≝ set_arg_8 s addr1 result in
     516              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
     517              let s ≝ set_arg_8 ? s addr1 result in
    518518                if ¬(eq_bv ? result (zero 8)) then
    519                   let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    520                     set_program_counter s new_pc
     519                  let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     520                    set_program_counter ? s new_pc
    521521                else
    522522                  s
     
    541541definition execute_1: Status → Status ≝
    542542  λs: Status.
    543     let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counter s) in
     543    let 〈instr_pc, ticks〉 ≝ fetch (code_memory ? s) (program_counter ? s) in
    544544    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    545     let s ≝ set_clock s (clock s + ticks) in
    546     let s ≝ set_program_counter s pc in
     545    let s ≝ set_clock ? s (clock ? s + ticks) in
     546    let s ≝ set_program_counter ? s pc in
    547547    let s ≝
    548548      match instr with
    549       [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]]
     549      [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ?
    550550        (λx.
    551551        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
     
    556556          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    557557            [ ADDR11 a ⇒ λaddr11: True.
    558               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    559               let s ≝ set_8051_sfr s SFR_SP new_sp in
    560               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    561               let s ≝ write_at_stack_pointer s pc_bl in
    562               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    563               let s ≝ set_8051_sfr s SFR_SP new_sp in
    564               let s ≝ write_at_stack_pointer s pc_bu in
     558              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     559              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     560              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     561              let s ≝ write_at_stack_pointer ? s pc_bl in
     562              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     563              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     564              let s ≝ write_at_stack_pointer ? s pc_bu in
    565565              let 〈thr, eig〉 ≝ split ? 3 8 a in
    566566              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
    567567              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    568                 set_program_counter s new_addr
     568                set_program_counter ? s new_addr
    569569            | _ ⇒ λother: False. ⊥
    570570            ] (subaddressing_modein … addr)
     
    572572          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    573573            [ ADDR16 a ⇒ λaddr16: True.
    574               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    575               let s ≝ set_8051_sfr s SFR_SP new_sp in
    576               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    577               let s ≝ write_at_stack_pointer s pc_bl in
    578               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    579               let s ≝ set_8051_sfr s SFR_SP new_sp in
    580               let s ≝ write_at_stack_pointer s pc_bu in
    581                 set_program_counter s a
     574              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     575              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     576              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     577              let s ≝ write_at_stack_pointer ? s pc_bl in
     578              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     579              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     580              let s ≝ write_at_stack_pointer ? s pc_bu in
     581                set_program_counter ? s a
    582582            | _ ⇒ λother: False. ⊥
    583583            ] (subaddressing_modein … addr)
     
    585585          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
    586586            [ ACC_DPTR ⇒ λacc_dptr: True.
    587               let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    588               let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     587              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
     588              let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    589589              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
    590               let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
    591                 set_8051_sfr s SFR_ACC_A result
     590              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
     591                set_8051_sfr ? s SFR_ACC_A result
    592592            | ACC_PC ⇒ λacc_pc: True.
    593               let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    594               let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
     593              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
     594              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
    595595              (* DPM: Under specified: does the carry from PC incrementation affect the *)
    596596              (*      addition of the PC with the DPTR? At the moment, no.              *)
    597               let s ≝ set_program_counter s inc_pc in
     597              let s ≝ set_program_counter ? s inc_pc in
    598598              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
    599               let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
    600                 set_8051_sfr s SFR_ACC_A result
     599              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
     600                set_8051_sfr ? s SFR_ACC_A result
    601601            | _ ⇒ λother: False. ⊥
    602602            ] (subaddressing_modein … addr2)
    603603        | JMP _ ⇒ (* DPM: always indirect_dptr *)
    604           let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    605           let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     604          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
     605          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    606606          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
    607           let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
    608             set_program_counter s new_pc
     607          let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
     608            set_program_counter ? s new_pc
    609609        | LJMP addr ⇒
    610610          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    611611            [ ADDR16 a ⇒ λaddr16: True.
    612                 set_program_counter s a
     612                set_program_counter ? s a
    613613            | _ ⇒ λother: False. ⊥
    614614            ] (subaddressing_modein … addr)
     
    616616          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    617617            [ RELATIVE r ⇒ λrelative: True.
    618                 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    619                   set_program_counter s new_pc
     618                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     619                  set_program_counter ? s new_pc
    620620            | _ ⇒ λother: False. ⊥
    621621            ] (subaddressing_modein … addr)
     
    623623          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    624624            [ ADDR11 a ⇒ λaddr11: True.
    625               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     625              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    626626              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
    627627              let bit ≝ get_index' ? O ? nl in
    628628              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
    629629              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    630               let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
    631                 set_program_counter s new_pc
     630              let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
     631                set_program_counter ? s new_pc
    632632            | _ ⇒ λother: False. ⊥
    633633            ] (subaddressing_modein … addr)
     
    652652
    653653axiom fetch_pseudo_instruction:
    654   ∀p: list labelled_instruction.
     654  ∀ps: PseudoStatus.
    655655  ∀pc: Word.
    656656    (pseudo_instruction × Word) × nat.
     
    659659axiom address_of_word_labels: Identifier → Word.
    660660
    661 definition execute_1_pseudo_instruction: pseudo_assembly_program → Status → Status ≝
    662   λp.
     661definition execute_1_pseudo_instruction: PseudoStatus → PseudoStatus ≝
    663662  λs.
    664   let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction (\snd p) (program_counter s) in
     663  let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction s (program_counter ? s) in
    665664  let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    666   let s ≝ set_clock s (clock s + ticks) in
    667   let s ≝ set_program_counter s pc in
     665  let s ≝ set_clock ? s (clock ? s + ticks) in
     666  let s ≝ set_program_counter ? s pc in
    668667  let s ≝
    669668    match instr with
    670     [ Instruction instr ⇒ execute_1_preinstruction ? address_of_labels instr s
     669    [ Instruction instr ⇒ execute_1_preinstruction address_of_labels instr s
    671670    | Comment cmt ⇒ s
    672671    | Cost cst ⇒ s
    673     | Jmp jmp ⇒ set_program_counter s (address_of_word_labels jmp)
     672    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels jmp)
    674673    | Call call ⇒
    675674      let a ≝ address_of_word_labels call in
    676       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    677       let s ≝ set_8051_sfr s SFR_SP new_sp in
    678       let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    679       let s ≝ write_at_stack_pointer s pc_bl in
    680       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    681       let s ≝ set_8051_sfr s SFR_SP new_sp in
    682       let s ≝ write_at_stack_pointer s pc_bu in
    683         set_program_counter s a
    684     | Mov dptr ident ⇒ set_arg_16 s (get_arg_16 s (DATA16 (address_of_word_labels ident))) dptr
     675      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     676      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     677      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     678      let s ≝ write_at_stack_pointer ? s pc_bl in
     679      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     680      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     681      let s ≝ write_at_stack_pointer ? s pc_bu in
     682        set_program_counter ? s a
     683    | Mov dptr ident ⇒ set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels ident))) dptr
    685684    ]
    686685  in
     
    696695    ].
    697696
    698 let rec execute_pseudo_instruction (n: nat) (p: pseudo_assembly_program) (s: Status) on n: Status ≝
     697let rec execute_pseudo_instruction (n: nat) (s: PseudoStatus) on n: PseudoStatus ≝
    699698  match n with
    700699    [ O ⇒ s
    701     | S o ⇒ execute_pseudo_instruction o p (execute_1_pseudo_instruction p s)
     700    | S o ⇒ execute_pseudo_instruction o (execute_1_pseudo_instruction s)
    702701    ].
  • src/ASM/Status.ma

    r757 r821  
    8585(* Processor status.                                                          *)
    8686(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    87 record Status: Type[0] ≝
     87record PreStatus (M: Type[0]): Type[0] ≝
    8888{
    89   code_memory: BitVectorTrie Byte 16;
     89  code_memory: M;
    9090  low_internal_ram: BitVectorTrie Byte 7;
    9191  high_internal_ram: BitVectorTrie Byte 7;
     
    103103}.
    104104
     105definition Status ≝ PreStatus (BitVectorTrie Byte 16).
     106definition PseudoStatus ≝ PreStatus (list labelled_instruction).
     107
    105108lemma sfr8051_index_19:
    106109  ∀i: SFR8051.
     
    124127   
    125128definition set_clock ≝
    126   λs: Status.
     129  λM: Type[0].
     130  λs: PreStatus M.
    127131  λt: Time.
    128     let old_code_memory ≝ code_memory s in
    129     let old_low_internal_ram ≝ low_internal_ram s in
    130     let old_high_internal_ram ≝ high_internal_ram s in
    131     let old_external_ram ≝ external_ram s in
    132     let old_program_counter ≝ program_counter s in
    133     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    134     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    135     let old_p1_latch ≝ p1_latch s in   
    136     let old_p3_latch ≝ p3_latch s in
    137       mk_Status old_code_memory
     132    let old_code_memory ≝ code_memory ? s in
     133    let old_low_internal_ram ≝ low_internal_ram ? s in
     134    let old_high_internal_ram ≝ high_internal_ram ? s in
     135    let old_external_ram ≝ external_ram ? s in
     136    let old_program_counter ≝ program_counter ? s in
     137    let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
     138    let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
     139    let old_p1_latch ≝ p1_latch ? s in   
     140    let old_p3_latch ≝ p3_latch ? s in
     141      mk_PreStatus M old_code_memory
    138142                old_low_internal_ram
    139143                old_high_internal_ram
     
    147151   
    148152definition set_p1_latch ≝
    149   λs: Status.
     153  λM: Type[0].
     154  λs: PreStatus M.
    150155  λb: Byte.
    151     let old_code_memory ≝ code_memory s in
    152     let old_low_internal_ram ≝ low_internal_ram s in
    153     let old_high_internal_ram ≝ high_internal_ram s in
    154     let old_external_ram ≝ external_ram s in
    155     let old_program_counter ≝ program_counter s in
    156     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    157     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    158     let old_p3_latch ≝ p3_latch s in
    159     let old_clock ≝ clock s in
    160       mk_Status old_code_memory
     156    let old_code_memory ≝ code_memory ? s in
     157    let old_low_internal_ram ≝ low_internal_ram ? s in
     158    let old_high_internal_ram ≝ high_internal_ram ? s in
     159    let old_external_ram ≝ external_ram ? s in
     160    let old_program_counter ≝ program_counter ? s in
     161    let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
     162    let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
     163    let old_p3_latch ≝ p3_latch ? s in
     164    let old_clock ≝ clock ? s in
     165      mk_PreStatus M old_code_memory
    161166                old_low_internal_ram
    162167                old_high_internal_ram
     
    170175
    171176definition set_p3_latch ≝
    172   λs: Status.
     177  λM: Type[0].
     178  λs: PreStatus M.
    173179  λb: Byte.
    174     let old_code_memory ≝ code_memory s in
    175     let old_low_internal_ram ≝ low_internal_ram s in
    176     let old_high_internal_ram ≝ high_internal_ram s in
    177     let old_external_ram ≝ external_ram s in
    178     let old_program_counter ≝ program_counter s in
    179     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    180     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    181     let old_p1_latch ≝ p1_latch s in
    182     let old_clock ≝ clock s in
    183       mk_Status old_code_memory
     180    let old_code_memory ≝ code_memory ? s in
     181    let old_low_internal_ram ≝ low_internal_ram ? s in
     182    let old_high_internal_ram ≝ high_internal_ram ? s in
     183    let old_external_ram ≝ external_ram ? s in
     184    let old_program_counter ≝ program_counter ? s in
     185    let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
     186    let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
     187    let old_p1_latch ≝ p1_latch ? s in
     188    let old_clock ≝ clock ? s in
     189      mk_PreStatus M old_code_memory
    184190                old_low_internal_ram
    185191                old_high_internal_ram
     
    193199
    194200definition get_8051_sfr ≝
    195   λs: Status.
     201  λM: Type[0].
     202  λs: PreStatus M.
    196203  λi: SFR8051.
    197     let sfr ≝ special_function_registers_8051 s in
     204    let sfr ≝ special_function_registers_8051 ? s in
    198205    let index ≝ sfr_8051_index i in
    199206      get_index_v … sfr index ?.
     
    202209
    203210definition get_8052_sfr ≝
    204   λs: Status.
     211  λM: Type[0].
     212  λs: PreStatus M.
    205213  λi: SFR8052.
    206     let sfr ≝ special_function_registers_8052 s in
     214    let sfr ≝ special_function_registers_8052 ? s in
    207215    let index ≝ sfr_8052_index i in
    208216      get_index_v … sfr index ?.
     
    211219
    212220definition set_8051_sfr ≝
    213   λs: Status.
     221  λM: Type[0].
     222  λs: PreStatus M.
    214223  λi: SFR8051.
    215224  λb: Byte.
    216225    let index ≝ sfr_8051_index i in
    217     let old_code_memory ≝ code_memory s in
    218     let old_low_internal_ram ≝ low_internal_ram s in
    219     let old_high_internal_ram ≝ high_internal_ram s in
    220     let old_external_ram ≝ external_ram s in
    221     let old_program_counter ≝ program_counter s in
    222     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    223     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     226    let old_code_memory ≝ code_memory ? s in
     227    let old_low_internal_ram ≝ low_internal_ram ? s in
     228    let old_high_internal_ram ≝ high_internal_ram ? s in
     229    let old_external_ram ≝ external_ram ? s in
     230    let old_program_counter ≝ program_counter ? s in
     231    let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
     232    let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
    224233    let new_special_function_registers_8051 ≝
    225234      set_index Byte 19 old_special_function_registers_8051 index b ? in
    226     let old_p1_latch ≝ p1_latch s in
    227     let old_p3_latch ≝ p3_latch s in
    228     let old_clock ≝ clock s in
    229       mk_Status old_code_memory
     235    let old_p1_latch ≝ p1_latch ? s in
     236    let old_p3_latch ≝ p3_latch ? s in
     237    let old_clock ≝ clock ? s in
     238      mk_PreStatus M old_code_memory
    230239                old_low_internal_ram
    231240                old_high_internal_ram
     
    241250
    242251definition set_8052_sfr ≝
    243   λs: Status.
     252  λM: Type[0].
     253  λs: PreStatus M.
    244254  λi: SFR8052.
    245255  λb: Byte.
    246256    let index ≝ sfr_8052_index i in
    247     let old_code_memory ≝ code_memory s in
    248     let old_low_internal_ram ≝ low_internal_ram s in
    249     let old_high_internal_ram ≝ high_internal_ram s in
    250     let old_external_ram ≝ external_ram s in
    251     let old_program_counter ≝ program_counter s in
    252     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    253     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     257    let old_code_memory ≝ code_memory ? s in
     258    let old_low_internal_ram ≝ low_internal_ram ? s in
     259    let old_high_internal_ram ≝ high_internal_ram ? s in
     260    let old_external_ram ≝ external_ram ? s in
     261    let old_program_counter ≝ program_counter ? s in
     262    let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
     263    let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
    254264    let new_special_function_registers_8052 ≝
    255265      set_index Byte 5 old_special_function_registers_8052 index b ? in
    256     let old_p1_latch ≝ p1_latch s in
    257     let old_p3_latch ≝ p3_latch s in
    258     let old_clock ≝ clock s in
    259       mk_Status old_code_memory
     266    let old_p1_latch ≝ p1_latch ? s in
     267    let old_p3_latch ≝ p3_latch ? s in
     268    let old_clock ≝ clock ? s in
     269      mk_PreStatus M old_code_memory
    260270                old_low_internal_ram
    261271                old_high_internal_ram
     
    271281
    272282definition set_program_counter ≝
    273   λs: Status.
     283  λM: Type[0].
     284  λs: PreStatus M.
    274285  λw: Word.
    275     let old_code_memory ≝ code_memory s in
    276     let old_low_internal_ram ≝ low_internal_ram s in
    277     let old_high_internal_ram ≝ high_internal_ram s in
    278     let old_external_ram ≝ external_ram s in
    279     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    280     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    281     let old_p1_latch ≝ p1_latch s in
    282     let old_p3_latch ≝ p3_latch s in
    283     let old_clock ≝ clock s in
    284       mk_Status old_code_memory
     286    let old_code_memory ≝ code_memory ? s in
     287    let old_low_internal_ram ≝ low_internal_ram ? s in
     288    let old_high_internal_ram ≝ high_internal_ram ? s in
     289    let old_external_ram ≝ external_ram ? s in
     290    let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
     291    let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
     292    let old_p1_latch ≝ p1_latch ? s in
     293    let old_p3_latch ≝ p3_latch ? s in
     294    let old_clock ≝ clock ? s in
     295      mk_PreStatus M old_code_memory
    285296                old_low_internal_ram
    286297                old_high_internal_ram
     
    294305               
    295306definition set_code_memory ≝
    296   λs: Status.
    297   λr: BitVectorTrie Byte 16.
    298     let old_low_internal_ram ≝ low_internal_ram s in
    299     let old_high_internal_ram ≝ high_internal_ram s in
    300     let old_external_ram ≝ external_ram s in
    301     let old_program_counter ≝ program_counter s in
    302     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    303     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    304     let old_p1_latch ≝ p1_latch s in
    305     let old_p3_latch ≝ p3_latch s in
    306     let old_clock ≝ clock s in
    307       mk_Status r
     307  λM: Type[0].
     308  λs: PreStatus M.
     309  λr: M.
     310    let old_low_internal_ram ≝ low_internal_ram ? s in
     311    let old_high_internal_ram ≝ high_internal_ram ? s in
     312    let old_external_ram ≝ external_ram ? s in
     313    let old_program_counter ≝ program_counter ? s in
     314    let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
     315    let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
     316    let old_p1_latch ≝ p1_latch ? s in
     317    let old_p3_latch ≝ p3_latch ? s in
     318    let old_clock ≝ clock ? s in
     319      mk_PreStatus M r
    308320                old_low_internal_ram
    309321                old_high_internal_ram
     
    317329               
    318330definition set_low_internal_ram ≝
    319   λs: Status.
     331  λM: Type[0].
     332  λs: PreStatus M.
    320333  λr: BitVectorTrie Byte 7.
    321     let old_code_memory ≝ code_memory s in
    322     let old_high_internal_ram ≝ high_internal_ram s in
    323     let old_external_ram ≝ external_ram s in
    324     let old_program_counter ≝ program_counter s in
    325     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    326     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    327     let old_p1_latch ≝ p1_latch s in
    328     let old_p3_latch ≝ p3_latch s in
    329     let old_clock ≝ clock s in
    330       mk_Status old_code_memory
     334    let old_code_memory ≝ code_memory ? s in
     335    let old_high_internal_ram ≝ high_internal_ram ? s in
     336    let old_external_ram ≝ external_ram ? s in
     337    let old_program_counter ≝ program_counter ? s in
     338    let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
     339    let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
     340    let old_p1_latch ≝ p1_latch ? s in
     341    let old_p3_latch ≝ p3_latch ? s in
     342    let old_clock ≝ clock ? s in
     343      mk_PreStatus M old_code_memory
    331344                r
    332345                old_high_internal_ram
     
    340353               
    341354definition set_high_internal_ram ≝
    342   λs: Status.
     355  λM: Type[0].
     356  λs: PreStatus M.
    343357  λr: BitVectorTrie Byte 7.
    344     let old_code_memory ≝ code_memory s in
    345     let old_low_internal_ram ≝ low_internal_ram s in
    346     let old_high_internal_ram ≝ high_internal_ram s in
    347     let old_external_ram ≝ external_ram s in
    348     let old_program_counter ≝ program_counter s in
    349     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    350     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    351     let old_p1_latch ≝ p1_latch s in
    352     let old_p3_latch ≝ p3_latch s in
    353     let old_clock ≝ clock s in
    354       mk_Status old_code_memory
     358    let old_code_memory ≝ code_memory ? s in
     359    let old_low_internal_ram ≝ low_internal_ram ? s in
     360    let old_high_internal_ram ≝ high_internal_ram ? s in
     361    let old_external_ram ≝ external_ram ? s in
     362    let old_program_counter ≝ program_counter ? s in
     363    let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
     364    let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
     365    let old_p1_latch ≝ p1_latch ? s in
     366    let old_p3_latch ≝ p3_latch ? s in
     367    let old_clock ≝ clock ? s in
     368      mk_PreStatus M old_code_memory
    355369                old_low_internal_ram
    356370                r
     
    364378               
    365379definition set_external_ram ≝
    366   λs: Status.
     380  λM: Type[0].
     381  λs: PreStatus M.
    367382  λr: BitVectorTrie Byte 16.
    368     let old_code_memory ≝ code_memory s in
    369     let old_low_internal_ram ≝ low_internal_ram s in
    370     let old_high_internal_ram ≝ high_internal_ram s in
    371     let old_program_counter ≝ program_counter s in
    372     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    373     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    374     let old_p1_latch ≝ p1_latch s in
    375     let old_p3_latch ≝ p3_latch s in
    376     let old_clock ≝ clock s in
    377       mk_Status old_code_memory
     383    let old_code_memory ≝ code_memory ? s in
     384    let old_low_internal_ram ≝ low_internal_ram ? s in
     385    let old_high_internal_ram ≝ high_internal_ram ? s in
     386    let old_program_counter ≝ program_counter ? s in
     387    let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
     388    let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
     389    let old_p1_latch ≝ p1_latch ? s in
     390    let old_p3_latch ≝ p3_latch ? s in
     391    let old_clock ≝ clock ? s in
     392      mk_PreStatus M old_code_memory
    378393                old_low_internal_ram
    379394                old_high_internal_ram
     
    387402               
    388403definition get_cy_flag ≝
    389   λs: Status.
    390     let sfr ≝ special_function_registers_8051 s in
     404  λM: Type[0].
     405  λs: PreStatus M.
     406    let sfr ≝ special_function_registers_8051 ? s in
    391407    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    392408      get_index_v bool 8 psw O ?.
     
    400416
    401417definition get_ac_flag ≝
    402   λs: Status.
    403     let sfr ≝ special_function_registers_8051 s in
     418  λM: Type[0].
     419  λs: PreStatus M.
     420    let sfr ≝ special_function_registers_8051 ? s in
    404421    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    405422      get_index_v bool 8 psw (S O) ?.
     
    410427
    411428definition get_fo_flag ≝
    412   λs: Status.
    413     let sfr ≝ special_function_registers_8051 s in
     429  λM: Type[0].
     430  λs: PreStatus M.
     431    let sfr ≝ special_function_registers_8051 ? s in
    414432    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    415433      get_index_v bool 8 psw 2 ?.
     
    420438
    421439definition get_rs1_flag ≝
    422   λs: Status.
    423     let sfr ≝ special_function_registers_8051 s in
     440  λM: Type[0].
     441  λs: PreStatus M.
     442    let sfr ≝ special_function_registers_8051 ? s in
    424443    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    425444      get_index_v bool 8 psw 3 ?.
     
    430449
    431450definition get_rs0_flag ≝
    432   λs: Status.
    433     let sfr ≝ special_function_registers_8051 s in
     451  λM: Type[0].
     452  λs: PreStatus M.
     453    let sfr ≝ special_function_registers_8051 ? s in
    434454    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    435455      get_index_v bool 8 psw 4 ?.
     
    440460
    441461definition get_ov_flag ≝
    442   λs: Status.
    443     let sfr ≝ special_function_registers_8051 s in
     462  λM: Type[0].
     463  λs: PreStatus M.
     464    let sfr ≝ special_function_registers_8051 ? s in
    444465    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    445466      get_index_v bool 8 psw 5 ?.
     
    450471
    451472definition get_ud_flag ≝
    452   λs: Status.
    453     let sfr ≝ special_function_registers_8051 s in
     473  λM: Type[0].
     474  λs: PreStatus M.
     475    let sfr ≝ special_function_registers_8051 ? s in
    454476    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    455477      get_index_v bool 8 psw 6 ?.
     
    460482
    461483definition get_p_flag ≝
    462   λs: Status.
    463     let sfr ≝ special_function_registers_8051 s in
     484  λM: Type[0].
     485  λs: PreStatus M.
     486    let sfr ≝ special_function_registers_8051 ? s in
    464487    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    465488      get_index_v bool 8 psw 7 ?.
     
    470493
    471494definition set_flags ≝
    472   λs: Status.
     495  λM: Type[0].
     496  λs: PreStatus M.
    473497  λcy: Bit.
    474498  λac: option Bit.
    475499  λov: Bit.
    476     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_PSW) in
     500    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_PSW) in
    477501    let old_cy ≝ get_index_v… nu O ? in
    478502    let old_ac ≝ get_index_v… nu 1 ? in
     
    486510    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
    487511                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
    488       set_8051_sfr s SFR_PSW new_psw.
     512      set_8051_sfr ? s SFR_PSW new_psw.
    489513    [1,2,3,4,5,6,7,8:
    490514       normalize
     
    495519
    496520definition initialise_status ≝
    497   let status ≝ mk_Status (Stub Byte 16)                    (* Code mem. *)
     521  λM: Type[0].
     522  λcode_mem: M.
     523  let status ≝ mk_PreStatus M code_mem                    (* Code mem. *)
    498524                         (Stub Byte 7)                      (* Low mem.  *)
    499525                         (Stub Byte 7)                      (* High mem. *)
     
    506532                         O                                      (* Clock.    *)
    507533  in
    508     set_8051_sfr status SFR_SP (bitvector_of_nat 8 7).
     534    set_8051_sfr ? status SFR_SP (bitvector_of_nat 8 7).
    509535 
    510536axiom not_implemented: False.
    511537 
    512538definition get_bit_addressable_sfr ≝
    513   λs: Status.
     539  λM: Type[0].
     540  λs: PreStatus M.
    514541  λn: nat.
    515542  λb: BitVector n.
     
    520547      else if (eqb address 144) then
    521548        if l then
    522           (p1_latch s)
     549          (p1_latch ? s)
    523550        else
    524           (get_8051_sfr s SFR_P1)
     551          (get_8051_sfr ? s SFR_P1)
    525552      else if (eqb address 160) then
    526553        ?
    527554      else if (eqb address 176) then
    528555        if l then
    529           (p3_latch s)
     556          (p3_latch ? s)
    530557        else
    531           (get_8051_sfr s SFR_P3)
     558          (get_8051_sfr ? s SFR_P3)
    532559      else if (eqb address 153) then
    533         get_8051_sfr s SFR_SBUF
     560        get_8051_sfr ? s SFR_SBUF
    534561      else if (eqb address 138) then
    535         get_8051_sfr s SFR_TL0
     562        get_8051_sfr ? s SFR_TL0
    536563      else if (eqb address 139) then
    537         get_8051_sfr s SFR_TL1
     564        get_8051_sfr ? s SFR_TL1
    538565      else if (eqb address 140) then
    539         get_8051_sfr s SFR_TH0
     566        get_8051_sfr ? s SFR_TH0
    540567      else if (eqb address 141) then
    541         get_8051_sfr s SFR_TH1
     568        get_8051_sfr ? s SFR_TH1
    542569      else if (eqb address 200) then
    543         get_8052_sfr s SFR_T2CON
     570        get_8052_sfr ? s SFR_T2CON
    544571      else if (eqb address 202) then
    545         get_8052_sfr s SFR_RCAP2L
     572        get_8052_sfr ? s SFR_RCAP2L
    546573      else if (eqb address 203) then
    547         get_8052_sfr s SFR_RCAP2H
     574        get_8052_sfr ? s SFR_RCAP2H
    548575      else if (eqb address 204) then
    549         get_8052_sfr s SFR_TL2
     576        get_8052_sfr ? s SFR_TL2
    550577      else if (eqb address 205) then
    551         get_8052_sfr s SFR_TH2
     578        get_8052_sfr ? s SFR_TH2
    552579      else if (eqb address 135) then
    553         get_8051_sfr s SFR_PCON
     580        get_8051_sfr ? s SFR_PCON
    554581      else if (eqb address 136) then
    555         get_8051_sfr s SFR_TCON
     582        get_8051_sfr ? s SFR_TCON
    556583      else if (eqb address 137) then
    557         get_8051_sfr s SFR_TMOD
     584        get_8051_sfr ? s SFR_TMOD
    558585      else if (eqb address 152) then
    559         get_8051_sfr s SFR_SCON
     586        get_8051_sfr ? s SFR_SCON
    560587      else if (eqb address 168) then
    561         get_8051_sfr s SFR_IE
     588        get_8051_sfr ? s SFR_IE
    562589      else if (eqb address 184) then
    563         get_8051_sfr s SFR_IP
     590        get_8051_sfr ? s SFR_IP
    564591      else if (eqb address 129) then
    565         get_8051_sfr s SFR_SP
     592        get_8051_sfr ? s SFR_SP
    566593      else if (eqb address 130) then
    567         get_8051_sfr s SFR_DPL
     594        get_8051_sfr ? s SFR_DPL
    568595      else if (eqb address 131) then
    569         get_8051_sfr s SFR_DPH
     596        get_8051_sfr ? s SFR_DPH
    570597      else if (eqb address 208) then
    571         get_8051_sfr s SFR_PSW
     598        get_8051_sfr ? s SFR_PSW
    572599      else if (eqb address 224) then
    573         get_8051_sfr s SFR_ACC_A
     600        get_8051_sfr ? s SFR_ACC_A
    574601      else if (eqb address 240) then
    575         get_8051_sfr s SFR_ACC_B
     602        get_8051_sfr ? s SFR_ACC_B
    576603      else
    577604        ?.
     
    580607
    581608definition set_bit_addressable_sfr ≝
    582   λs: Status.
     609  λM: Type[0].
     610  λs: PreStatus M.
    583611  λb: Byte.
    584612  λv: Byte.
     
    587615        ?
    588616      else if (eqb address 144) then
    589         let status_1 ≝ set_8051_sfr s SFR_P1 v in
    590         let status_2 ≝ set_p1_latch s v in
     617        let status_1 ≝ set_8051_sfr ? s SFR_P1 v in
     618        let status_2 ≝ set_p1_latch ? s v in
    591619          status_2
    592620      else if (eqb address 160) then
    593621        ?
    594622      else if (eqb address 176) then
    595         let status_1 ≝ set_8051_sfr s SFR_P3 v in
    596         let status_2 ≝ set_p3_latch s v in
     623        let status_1 ≝ set_8051_sfr ? s SFR_P3 v in
     624        let status_2 ≝ set_p3_latch ? s v in
    597625          status_2
    598626      else if (eqb address 153) then
    599         set_8051_sfr s SFR_SBUF v
     627        set_8051_sfr ? s SFR_SBUF v
    600628      else if (eqb address 138) then
    601         set_8051_sfr s SFR_TL0 v
     629        set_8051_sfr ? s SFR_TL0 v
    602630      else if (eqb address 139) then
    603         set_8051_sfr s SFR_TL1 v
     631        set_8051_sfr ? s SFR_TL1 v
    604632      else if (eqb address 140) then
    605         set_8051_sfr s SFR_TH0 v
     633        set_8051_sfr ? s SFR_TH0 v
    606634      else if (eqb address 141) then
    607         set_8051_sfr s SFR_TH1 v
     635        set_8051_sfr ? s SFR_TH1 v
    608636      else if (eqb address 200) then
    609         set_8052_sfr s SFR_T2CON v
     637        set_8052_sfr ? s SFR_T2CON v
    610638      else if (eqb address 202) then
    611         set_8052_sfr s SFR_RCAP2L v
     639        set_8052_sfr ? s SFR_RCAP2L v
    612640      else if (eqb address 203) then
    613         set_8052_sfr s SFR_RCAP2H v
     641        set_8052_sfr ? s SFR_RCAP2H v
    614642      else if (eqb address 204) then
    615         set_8052_sfr s SFR_TL2 v
     643        set_8052_sfr ? s SFR_TL2 v
    616644      else if (eqb address 205) then
    617         set_8052_sfr s SFR_TH2 v
     645        set_8052_sfr ? s SFR_TH2 v
    618646      else if (eqb address 135) then
    619         set_8051_sfr s SFR_PCON v
     647        set_8051_sfr ? s SFR_PCON v
    620648      else if (eqb address 136) then
    621         set_8051_sfr s SFR_TCON v
     649        set_8051_sfr ? s SFR_TCON v
    622650      else if (eqb address 137) then
    623         set_8051_sfr s SFR_TMOD v
     651        set_8051_sfr ? s SFR_TMOD v
    624652      else if (eqb address 152) then
    625         set_8051_sfr s SFR_SCON v
     653        set_8051_sfr ? s SFR_SCON v
    626654      else if (eqb address 168) then
    627         set_8051_sfr s SFR_IE v
     655        set_8051_sfr ? s SFR_IE v
    628656      else if (eqb address 184) then
    629         set_8051_sfr s SFR_IP v
     657        set_8051_sfr ? s SFR_IP v
    630658      else if (eqb address 129) then
    631         set_8051_sfr s SFR_SP v
     659        set_8051_sfr ? s SFR_SP v
    632660      else if (eqb address 130) then
    633         set_8051_sfr s SFR_DPL v
     661        set_8051_sfr ? s SFR_DPL v
    634662      else if (eqb address 131) then
    635         set_8051_sfr s SFR_DPH v
     663        set_8051_sfr ? s SFR_DPH v
    636664      else if (eqb address 208) then
    637         set_8051_sfr s SFR_PSW v
     665        set_8051_sfr ? s SFR_PSW v
    638666      else if (eqb address 224) then
    639         set_8051_sfr s SFR_ACC_A v
     667        set_8051_sfr ? s SFR_ACC_A v
    640668      else if (eqb address 240) then
    641         set_8051_sfr s SFR_ACC_B v
     669        set_8051_sfr ? s SFR_ACC_B v
    642670      else
    643671        ?.
     
    646674
    647675definition bit_address_of_register ≝
    648   λs: Status.
     676  λM: Type[0].
     677  λs: PreStatus M.
    649678  λr: BitVector 3.
    650679    let b ≝ get_index_v … r O ? in
    651680    let c ≝ get_index_v … r 1 ? in
    652681    let d ≝ get_index_v … r 2 ? in
    653     let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
     682    let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
    654683    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
    655684    let offset ≝
     
    672701
    673702definition get_register ≝
    674   λs: Status.
     703  λM: Type[0].
     704  λs: PreStatus M.
    675705  λr: BitVector 3.
    676     let address ≝ bit_address_of_register s r in
    677       lookup … address (low_internal_ram s) (zero 8).
     706    let address ≝ bit_address_of_register ? s r in
     707      lookup … address (low_internal_ram ? s) (zero 8).
    678708     
    679709definition set_register ≝
    680   λs: Status.
     710  λM: Type[0].
     711  λs: PreStatus M.
    681712  λr: BitVector 3.
    682713  λv: Byte.
    683     let address ≝ bit_address_of_register s r in
    684     let old_low_internal_ram ≝ low_internal_ram s in
     714    let address ≝ bit_address_of_register ? s r in
     715    let old_low_internal_ram ≝ low_internal_ram ? s in
    685716    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
    686       set_low_internal_ram s new_low_internal_ram.
     717      set_low_internal_ram ? s new_low_internal_ram.
    687718     
    688719definition read_at_stack_pointer ≝
    689   λs: Status.
    690     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in
     720  λM: Type[0].
     721  λs: PreStatus M.
     722    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
    691723    let m ≝ get_index_v … nu O ? in
    692724    let r1 ≝ get_index_v … nu 1 ? in
     
    696728    let memory ≝
    697729      if m then
    698         (low_internal_ram s)
     730        (low_internal_ram ? s)
    699731      else
    700         (high_internal_ram s)
     732        (high_internal_ram ? s)
    701733    in
    702734      lookup … address memory (zero 8).
     
    709741
    710742definition write_at_stack_pointer ≝
    711   λs: Status.
     743  λM: Type[0].
     744  λs: PreStatus M.
    712745  λv: Byte.
    713     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in
     746    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
    714747    let bit_zero ≝ get_index_v… nu O ? in
    715748    let bit_1 ≝ get_index_v… nu 1 ? in
     
    718751      if bit_zero then
    719752        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    720                               v (low_internal_ram s) in
    721           set_low_internal_ram s memory
     753                              v (low_internal_ram ? s) in
     754          set_low_internal_ram ? s memory
    722755      else
    723756        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    724                               v (high_internal_ram s) in
    725           set_high_internal_ram s memory.
     757                              v (high_internal_ram ? s) in
     758          set_high_internal_ram ? s memory.
    726759  [1,2,3,4:
    727760     normalize
     
    731764qed.
    732765
    733 definition set_arg_16: Status → Word → [[ dptr ]] → Status ≝
    734   λs,v,a.
     766definition set_arg_16: ∀M: Type[0]. PreStatus M → Word → [[ dptr ]] → PreStatus M ≝
     767  λM.
     768  λs.
     769  λv.
     770  λa.
    735771   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
    736772     [ DPTR ⇒ λ_:True.
    737773       let 〈 bu, bl 〉 ≝ split … 8 8 v in
    738        let status ≝ set_8051_sfr s SFR_DPH bu in
    739        let status ≝ set_8051_sfr status SFR_DPL bl in
     774       let status ≝ set_8051_sfr ? s SFR_DPH bu in
     775       let status ≝ set_8051_sfr ? status SFR_DPL bl in
    740776         status
    741777     | _ ⇒ λK.
     
    745781     ] (subaddressing_modein … a).
    746782   
    747 definition get_arg_16: Status → [[ data16 ]] → Word ≝
    748   λs, a.
     783definition get_arg_16: ∀M: Type[0]. PreStatus M → [[ data16 ]] → Word ≝
     784  λm, s, a.
    749785    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
    750786      [ DATA16 d ⇒ λ_:True. d
     
    755791      ] (subaddressing_modein … a).
    756792     
    757 definition get_arg_8: Status → bool → [[ direct ; indirect ; registr ;
     793definition get_arg_8: ∀M: Type[0]. PreStatus M → bool → [[ direct ; indirect ; registr ;
    758794                                          acc_a ; acc_b ; data ; acc_dptr ;
    759795                                          acc_pc ; ext_indirect ;
    760796                                          ext_indirect_dptr ]] → Byte ≝
    761   λs, l, a.
     797  λm, s, l, a.
    762798    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    763799                                                acc_a ; acc_b ; data ; acc_dptr ;
    764800                                                acc_pc ; ext_indirect ;
    765801                                                ext_indirect_dptr ]] x) → ? with
    766       [ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A
    767       | ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B
     802      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ? s SFR_ACC_A
     803      | ACC_B ⇒ λacc_b: True. get_8051_sfr ? s SFR_ACC_B
    768804      | DATA d ⇒ λdata: True. d
    769       | REGISTER r ⇒ λregister: True. get_register s r
     805      | REGISTER r ⇒ λregister: True. get_register ? s r
    770806      | EXT_INDIRECT_DPTR ⇒
    771807        λext_indirect_dptr: True.
    772           let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    773             lookup … 16 address (external_ram s) (zero 8)
     808          let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
     809            lookup … 16 address (external_ram ? s) (zero 8)
    774810      | EXT_INDIRECT e ⇒
    775811        λext_indirect: True.
    776           let address ≝ get_register s [[ false; false; e ]]  in
     812          let address ≝ get_register ? s [[ false; false; e ]]  in
    777813          let padded_address ≝ pad 8 8 address in
    778             lookup … 16 padded_address (external_ram s) (zero 8)
     814            lookup … 16 padded_address (external_ram ? s) (zero 8)
    779815      | ACC_DPTR ⇒
    780816        λacc_dptr: True.
    781           let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    782           let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in
     817          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
     818          let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in
    783819          let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
    784             lookup … 16 address (external_ram s) (zero 8)
     820            lookup … 16 address (external_ram ? s) (zero 8)
    785821      | ACC_PC ⇒
    786822        λacc_pc: True.
    787           let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in
    788           let 〈 carry, address 〉 ≝ half_add 16 (program_counter s) padded_acc in
    789             lookup … 16 address (external_ram s) (zero 8)
     823          let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in
     824          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ? s) padded_acc in
     825            lookup … 16 address (external_ram ? s) (zero 8)
    790826      | DIRECT d ⇒
    791827        λdirect: True.
     
    796832                  let 〈 bit_one, three_bits 〉 ≝ split ? 1 3 nu in
    797833                  let address ≝ three_bits @@ nl in
    798                     lookup ? 7 address (low_internal_ram s) (zero 8)
    799               | false ⇒ get_bit_addressable_sfr s 8 d l
     834                    lookup ? 7 address (low_internal_ram ? s) (zero 8)
     835              | false ⇒ get_bit_addressable_sfr ? s 8 d l
    800836              ]
    801837      | INDIRECT i ⇒
    802838        λindirect: True.
    803           let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register s [[ false; false; i]]) in
     839          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ? s [[ false; false; i]]) in
    804840          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
    805841          let bit_1 ≝ get_index_v … bit_one_v O ? in
    806842          match bit_1 with
    807843            [ true ⇒
    808                 lookup ? 7 (three_bits @@ nl) (low_internal_ram s) (zero 8)
     844                lookup ? 7 (three_bits @@ nl) (low_internal_ram ? s) (zero 8)
    809845            | false ⇒
    810                 lookup ? 7 (three_bits @@ nl) (high_internal_ram s) (zero 8)
     846                lookup ? 7 (three_bits @@ nl) (high_internal_ram ? s) (zero 8)
    811847            ]
    812848      | _ ⇒ λother.
     
    820856qed.
    821857
    822 definition set_arg_8: Status → [[ direct ; indirect ; registr ;
     858definition set_arg_8: ∀M: Type[0]. PreStatus M → [[ direct ; indirect ; registr ;
    823859                                   acc_a ; acc_b ; ext_indirect ;
    824                                    ext_indirect_dptr ]] → Byte → Status
    825   λs, a, v.
     860                                   ext_indirect_dptr ]] → Byte → PreStatus M
     861  λm, s, a, v.
    826862    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    827863                                                acc_a ; acc_b ; ext_indirect ;
     
    833869          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
    834870            match bit_1 with
    835               [ true ⇒ set_bit_addressable_sfr s d v
     871              [ true ⇒ set_bit_addressable_sfr ? s d v
    836872              | false ⇒
    837                 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram s) in
    838                   set_low_internal_ram s memory
     873                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ? s) in
     874                  set_low_internal_ram ? s memory
    839875              ]
    840876      | INDIRECT i ⇒
    841877        λindirect: True.
    842           let register ≝ get_register s [[ false; false; i ]] in
     878          let register ≝ get_register ? s [[ false; false; i ]] in
    843879          let 〈nu, nl〉 ≝ split ? 4 4 register in
    844880          let bit_1 ≝ get_index_v … nu 1 ? in
     
    846882            match bit_1 with
    847883              [ true ⇒
    848                 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
    849                   set_low_internal_ram s memory
     884                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ? s) in
     885                  set_low_internal_ram ? s memory
    850886              | false ⇒
    851                 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
    852                   set_high_internal_ram s memory
     887                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ? s) in
     888                  set_high_internal_ram ? s memory
    853889              ]
    854       | REGISTER r ⇒ λregister: True. set_register s r v
    855       | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
    856       | ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v
     890      | REGISTER r ⇒ λregister: True. set_register ? s r v
     891      | ACC_A ⇒ λacc_a: True. set_8051_sfr ? s SFR_ACC_A v
     892      | ACC_B ⇒ λacc_b: True. set_8051_sfr ? s SFR_ACC_B v
    857893      | EXT_INDIRECT e ⇒
    858894        λext_indirect: True.
    859           let address ≝ get_register s [[ false; false; e ]] in
     895          let address ≝ get_register ? s [[ false; false; e ]] in
    860896          let padded_address ≝ pad 8 8 address in
    861           let memory ≝ insert ? 16 padded_address v (external_ram s) in
    862             set_external_ram s memory
     897          let memory ≝ insert ? 16 padded_address v (external_ram ? s) in
     898            set_external_ram ? s memory
    863899      | EXT_INDIRECT_DPTR ⇒
    864900        λext_indirect_dptr: True.
    865           let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    866           let memory ≝ insert ? 16 address v (external_ram s) in
    867             set_external_ram s memory
     901          let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
     902          let memory ≝ insert ? 16 address v (external_ram ? s) in
     903            set_external_ram ? s memory
    868904      | _ ⇒
    869905        λother: False.
     
    928964qed.
    929965
    930 definition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
     966definition get_arg_1: ∀M: Type[0]. PreStatus M → [[ bit_addr ; n_bit_addr ; carry ]] →
    931967                       bool → bool ≝
    932   λs, a, l.
     968  λm, s, a, l.
    933969    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
    934970                                                 n_bit_addr ;
     
    945981                let m ≝ address mod 8 in
    946982                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    947                 let sfr ≝ get_bit_addressable_sfr s ? trans l in
     983                let sfr ≝ get_bit_addressable_sfr ? s ? trans l in
    948984                  get_index_v … sfr m ?
    949985              | false ⇒
    950986                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    951987                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    952                 let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
     988                let t ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in
    953989                  get_index_v … t (modulus address 8) ?
    954990              ]
     
    9641000                let m ≝ address mod 8 in
    9651001                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    966                 let sfr ≝ get_bit_addressable_sfr s ? trans l in
     1002                let sfr ≝ get_bit_addressable_sfr ? s ? trans l in
    9671003                  ¬(get_index_v … sfr m ?)
    9681004              | false ⇒
    9691005                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    9701006                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    971                 let trans ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
     1007                let trans ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in
    9721008                  ¬(get_index_v … trans (modulus address 8) ?)
    9731009              ]
    974       | CARRY ⇒ λcarry: True. get_cy_flag s
     1010      | CARRY ⇒ λcarry: True. get_cy_flag ? s
    9751011      | _ ⇒ λother.
    9761012        match other in False with [ ]
     
    9851021qed.
    9861022     
    987 definition set_arg_1: Status → [[ bit_addr ; carry ]] →
    988                        Bit → Status
    989   λs, a, v.
     1023definition set_arg_1: ∀M: Type[0]. PreStatus M → [[ bit_addr ; carry ]] →
     1024                       Bit → PreStatus M
     1025  λm, s, a, v.
    9901026    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
    9911027      [ BIT_ADDR b ⇒ λbit_addr: True.
    992           let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
     1028          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
    9931029          let bit_1 ≝ get_index_v … nu 1 ? in
    9941030          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
     
    9991035                let m ≝ address mod 8 in
    10001036                let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1001                 let sfr ≝ get_bit_addressable_sfr s ? t true in
     1037                let sfr ≝ get_bit_addressable_sfr ? s ? t true in
    10021038                let new_sfr ≝ set_index … sfr m v ? in
    1003                   set_bit_addressable_sfr s new_sfr t
     1039                  set_bit_addressable_sfr ? s new_sfr t
    10041040            | false ⇒
    10051041                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    10061042                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1007                 let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
     1043                let t ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in
    10081044                let n_bit ≝ set_index … t (modulus address 8) v ? in
    1009                 let memory ≝ insert ? 7 address' n_bit (low_internal_ram s) in
    1010                   set_low_internal_ram s memory
     1045                let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
     1046                  set_low_internal_ram ? s memory
    10111047            ]
    10121048      | CARRY ⇒
    10131049        λcarry: True.
    1014           let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
     1050          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
    10151051          let bit_1 ≝ get_index_v… nu 1 ? in
    10161052          let bit_2 ≝ get_index_v… nu 2 ? in
    10171053          let bit_3 ≝ get_index_v… nu 3 ? in
    10181054          let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
    1019             set_8051_sfr s SFR_PSW new_psw
     1055            set_8051_sfr ? s SFR_PSW new_psw
    10201056      | _ ⇒
    10211057        λother: False.
     
    10381074
    10391075definition load ≝
    1040  λl, status.
    1041    set_code_memory status (load_code_memory l).
     1076 λl.
     1077 λstatus.
     1078   set_code_memory ? status (load_code_memory l).
Note: See TracChangeset for help on using the changeset viewer.