Changeset 1416 for src/ASM


Ignore:
Timestamp:
Oct 19, 2011, 4:43:49 PM (8 years ago)
Author:
sacerdot
Message:

Maps from hardware registers to beval now implemented in ASM/I8051 (in place
of the old huge implementation to Bytes).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1415 r1416  
    66include "ASM/Arithmetic.ma".
    77include "utilities/Compare.ma".
     8include "joint/BEValues.ma".
    89
    910definition int_size ≝ bitvector_of_nat 8 1.
     
    113114definition physical_register_count ≝ 36.
    114115
    115 definition word_of_register: Register → Word
     116definition bitvector_of_register: Register → BitVector 6
    116117  λregister.
    117118    bitvector_of_nat ? (nat_of_register register).
     
    205206    ]
    206207qed.
    207    
    208 record RegisterMap: Type[0] ≝
    209 {
    210   register_00_value: option Byte;
    211   register_01_value: option Byte;
    212   register_02_value: option Byte;
    213   register_03_value: option Byte;
    214   register_04_value: option Byte;
    215   register_05_value: option Byte;
    216   register_06_value: option Byte;
    217   register_07_value: option Byte;
    218   register_10_value: option Byte;
    219   register_11_value: option Byte;
    220   register_12_value: option Byte;
    221   register_13_value: option Byte;
    222   register_14_value: option Byte;
    223   register_15_value: option Byte;
    224   register_16_value: option Byte;
    225   register_17_value: option Byte;
    226   register_20_value: option Byte;
    227   register_21_value: option Byte;
    228   register_22_value: option Byte;
    229   register_23_value: option Byte;
    230   register_24_value: option Byte;
    231   register_25_value: option Byte;
    232   register_26_value: option Byte;
    233   register_27_value: option Byte;
    234   register_30_value: option Byte;
    235   register_31_value: option Byte;
    236   register_32_value: option Byte;
    237   register_33_value: option Byte;
    238   register_34_value: option Byte;
    239   register_35_value: option Byte;
    240   register_36_value: option Byte;
    241   register_37_value: option Byte;
    242   register_A_value: option Byte;
    243   register_B_value: option Byte;
    244   register_DPL_value: option Byte;
    245   register_DPH_value: option Byte;
    246   register_Carry_value: option Byte
    247   (* carry only used in liveness analysis *)
    248 }.
    249 
    250 definition initialize_register_map: RegisterMap ≝
    251   mk_RegisterMap (None ?) (None ?) (None ?) (None ?)
    252                  (None ?) (None ?) (None ?) (None ?)
    253                  (None ?) (None ?) (None ?) (None ?)
    254                  (None ?) (None ?) (None ?) (None ?)
    255                  (None ?) (None ?) (None ?) (None ?)
    256                  (None ?) (None ?) (None ?) (None ?)
    257                  (None ?) (None ?) (None ?) (None ?)
    258                  (None ?) (None ?) (None ?) (None ?)
    259                  (None ?) (None ?) (None ?) (None ?)
    260                  (None ?).
    261                  
    262 definition lookup_register_map: Register → RegisterMap → option Byte ≝
    263   λr: Register.
    264   λm: RegisterMap.
    265   match r with
    266   [ Register00 ⇒ register_00_value m
    267   | Register01 ⇒ register_01_value m
    268   | Register02 ⇒ register_02_value m
    269   | Register03 ⇒ register_03_value m
    270   | Register04 ⇒ register_04_value m
    271   | Register05 ⇒ register_05_value m
    272   | Register06 ⇒ register_06_value m
    273   | Register07 ⇒ register_07_value m
    274   | Register10 ⇒ register_10_value m
    275   | Register11 ⇒ register_11_value m
    276   | Register12 ⇒ register_12_value m
    277   | Register13 ⇒ register_13_value m
    278   | Register14 ⇒ register_14_value m
    279   | Register15 ⇒ register_15_value m
    280   | Register16 ⇒ register_16_value m
    281   | Register17 ⇒ register_17_value m
    282   | Register20 ⇒ register_20_value m
    283   | Register21 ⇒ register_21_value m
    284   | Register22 ⇒ register_22_value m
    285   | Register23 ⇒ register_23_value m
    286   | Register24 ⇒ register_24_value m
    287   | Register25 ⇒ register_25_value m
    288   | Register26 ⇒ register_26_value m
    289   | Register27 ⇒ register_27_value m
    290   | Register30 ⇒ register_30_value m
    291   | Register31 ⇒ register_31_value m
    292   | Register32 ⇒ register_32_value m
    293   | Register33 ⇒ register_33_value m
    294   | Register34 ⇒ register_34_value m
    295   | Register35 ⇒ register_35_value m
    296   | Register36 ⇒ register_36_value m
    297   | Register37 ⇒ register_37_value m
    298   | RegisterA ⇒ register_A_value m
    299   | RegisterB ⇒ register_B_value m
    300   | RegisterDPL ⇒ register_DPL_value m
    301   | RegisterDPH ⇒ register_DPH_value m
    302   | RegisterCarry ⇒ register_Carry_value m
    303   ].
    304  
    305 definition update_register_00: Byte → RegisterMap → RegisterMap ≝
    306   λb: Byte.
    307   λm: RegisterMap.
    308   let old_register_00_value ≝ register_00_value m in
    309   let old_register_01_value ≝ register_01_value m in
    310   let old_register_02_value ≝ register_02_value m in
    311   let old_register_03_value ≝ register_03_value m in
    312   let old_register_04_value ≝ register_04_value m in
    313   let old_register_05_value ≝ register_05_value m in
    314   let old_register_06_value ≝ register_06_value m in
    315   let old_register_07_value ≝ register_07_value m in
    316   let old_register_10_value ≝ register_01_value m in
    317   let old_register_11_value ≝ register_01_value m in
    318   let old_register_12_value ≝ register_02_value m in
    319   let old_register_13_value ≝ register_03_value m in
    320   let old_register_14_value ≝ register_04_value m in
    321   let old_register_15_value ≝ register_05_value m in
    322   let old_register_16_value ≝ register_06_value m in
    323   let old_register_17_value ≝ register_07_value m in
    324   let old_register_20_value ≝ register_01_value m in
    325   let old_register_21_value ≝ register_02_value m in
    326   let old_register_22_value ≝ register_02_value m in
    327   let old_register_23_value ≝ register_03_value m in
    328   let old_register_24_value ≝ register_04_value m in
    329   let old_register_25_value ≝ register_05_value m in
    330   let old_register_26_value ≝ register_06_value m in
    331   let old_register_27_value ≝ register_07_value m in
    332   let old_register_30_value ≝ register_01_value m in
    333   let old_register_31_value ≝ register_02_value m in
    334   let old_register_32_value ≝ register_02_value m in
    335   let old_register_33_value ≝ register_03_value m in
    336   let old_register_34_value ≝ register_04_value m in
    337   let old_register_35_value ≝ register_05_value m in
    338   let old_register_36_value ≝ register_06_value m in
    339   let old_register_37_value ≝ register_07_value m in
    340   let old_register_A_value ≝ register_A_value m in
    341   let old_register_B_value ≝ register_B_value m in
    342   let old_register_DPL_value ≝ register_DPL_value m in
    343   let old_register_DPH_value ≝ register_DPH_value m in
    344   let old_register_Carry_value ≝ register_Carry_value m in
    345     mk_RegisterMap (Some ? b)
    346                    old_register_01_value
    347                    old_register_02_value
    348                    old_register_03_value
    349                    old_register_04_value
    350                    old_register_05_value
    351                    old_register_06_value
    352                    old_register_07_value
    353                    old_register_10_value
    354                    old_register_11_value
    355                    old_register_12_value
    356                    old_register_13_value
    357                    old_register_14_value
    358                    old_register_15_value
    359                    old_register_16_value
    360                    old_register_17_value
    361                    old_register_20_value
    362                    old_register_21_value
    363                    old_register_22_value
    364                    old_register_23_value
    365                    old_register_24_value
    366                    old_register_25_value
    367                    old_register_26_value
    368                    old_register_27_value
    369                    old_register_30_value
    370                    old_register_31_value
    371                    old_register_32_value
    372                    old_register_33_value
    373                    old_register_34_value
    374                    old_register_35_value
    375                    old_register_36_value
    376                    old_register_37_value
    377                    old_register_A_value
    378                    old_register_B_value
    379                    old_register_DPL_value
    380                    old_register_DPH_value
    381                    old_register_Carry_value.
    382 
    383 definition update_register_01: Byte → RegisterMap → RegisterMap ≝
    384   λb: Byte.
    385   λm: RegisterMap.
    386   let old_register_00_value ≝ register_00_value m in
    387   let old_register_01_value ≝ register_01_value m in
    388   let old_register_02_value ≝ register_02_value m in
    389   let old_register_03_value ≝ register_03_value m in
    390   let old_register_04_value ≝ register_04_value m in
    391   let old_register_05_value ≝ register_05_value m in
    392   let old_register_06_value ≝ register_06_value m in
    393   let old_register_07_value ≝ register_07_value m in
    394   let old_register_10_value ≝ register_01_value m in
    395   let old_register_11_value ≝ register_01_value m in
    396   let old_register_12_value ≝ register_02_value m in
    397   let old_register_13_value ≝ register_03_value m in
    398   let old_register_14_value ≝ register_04_value m in
    399   let old_register_15_value ≝ register_05_value m in
    400   let old_register_16_value ≝ register_06_value m in
    401   let old_register_17_value ≝ register_07_value m in
    402   let old_register_20_value ≝ register_01_value m in
    403   let old_register_21_value ≝ register_02_value m in
    404   let old_register_22_value ≝ register_02_value m in
    405   let old_register_23_value ≝ register_03_value m in
    406   let old_register_24_value ≝ register_04_value m in
    407   let old_register_25_value ≝ register_05_value m in
    408   let old_register_26_value ≝ register_06_value m in
    409   let old_register_27_value ≝ register_07_value m in
    410   let old_register_30_value ≝ register_01_value m in
    411   let old_register_31_value ≝ register_02_value m in
    412   let old_register_32_value ≝ register_02_value m in
    413   let old_register_33_value ≝ register_03_value m in
    414   let old_register_34_value ≝ register_04_value m in
    415   let old_register_35_value ≝ register_05_value m in
    416   let old_register_36_value ≝ register_06_value m in
    417   let old_register_37_value ≝ register_07_value m in
    418   let old_register_A_value ≝ register_A_value m in
    419   let old_register_B_value ≝ register_B_value m in
    420   let old_register_DPL_value ≝ register_DPL_value m in
    421   let old_register_DPH_value ≝ register_DPH_value m in
    422   let old_register_Carry_value ≝ register_Carry_value m in
    423     mk_RegisterMap old_register_00_value
    424                    (Some ? b)
    425                    old_register_02_value
    426                    old_register_03_value
    427                    old_register_04_value
    428                    old_register_05_value
    429                    old_register_06_value
    430                    old_register_07_value
    431                    old_register_10_value
    432                    old_register_11_value
    433                    old_register_12_value
    434                    old_register_13_value
    435                    old_register_14_value
    436                    old_register_15_value
    437                    old_register_16_value
    438                    old_register_17_value
    439                    old_register_20_value
    440                    old_register_21_value
    441                    old_register_22_value
    442                    old_register_23_value
    443                    old_register_24_value
    444                    old_register_25_value
    445                    old_register_26_value
    446                    old_register_27_value
    447                    old_register_30_value
    448                    old_register_31_value
    449                    old_register_32_value
    450                    old_register_33_value
    451                    old_register_34_value
    452                    old_register_35_value
    453                    old_register_36_value
    454                    old_register_37_value
    455                    old_register_A_value
    456                    old_register_B_value
    457                    old_register_DPL_value
    458                    old_register_DPH_value
    459                    old_register_Carry_value.
    460 
    461 definition update_register_02: Byte → RegisterMap → RegisterMap ≝
    462   λb: Byte.
    463   λm: RegisterMap.
    464   let old_register_00_value ≝ register_00_value m in
    465   let old_register_01_value ≝ register_01_value m in
    466   let old_register_02_value ≝ register_02_value m in
    467   let old_register_03_value ≝ register_03_value m in
    468   let old_register_04_value ≝ register_04_value m in
    469   let old_register_05_value ≝ register_05_value m in
    470   let old_register_06_value ≝ register_06_value m in
    471   let old_register_07_value ≝ register_07_value m in
    472   let old_register_10_value ≝ register_01_value m in
    473   let old_register_11_value ≝ register_01_value m in
    474   let old_register_12_value ≝ register_02_value m in
    475   let old_register_13_value ≝ register_03_value m in
    476   let old_register_14_value ≝ register_04_value m in
    477   let old_register_15_value ≝ register_05_value m in
    478   let old_register_16_value ≝ register_06_value m in
    479   let old_register_17_value ≝ register_07_value m in
    480   let old_register_20_value ≝ register_01_value m in
    481   let old_register_21_value ≝ register_02_value m in
    482   let old_register_22_value ≝ register_02_value m in
    483   let old_register_23_value ≝ register_03_value m in
    484   let old_register_24_value ≝ register_04_value m in
    485   let old_register_25_value ≝ register_05_value m in
    486   let old_register_26_value ≝ register_06_value m in
    487   let old_register_27_value ≝ register_07_value m in
    488   let old_register_30_value ≝ register_01_value m in
    489   let old_register_31_value ≝ register_02_value m in
    490   let old_register_32_value ≝ register_02_value m in
    491   let old_register_33_value ≝ register_03_value m in
    492   let old_register_34_value ≝ register_04_value m in
    493   let old_register_35_value ≝ register_05_value m in
    494   let old_register_36_value ≝ register_06_value m in
    495   let old_register_37_value ≝ register_07_value m in
    496   let old_register_A_value ≝ register_A_value m in
    497   let old_register_B_value ≝ register_B_value m in
    498   let old_register_DPL_value ≝ register_DPL_value m in
    499   let old_register_DPH_value ≝ register_DPH_value m in
    500   let old_register_Carry_value ≝ register_Carry_value m in
    501     mk_RegisterMap old_register_00_value
    502                    old_register_01_value
    503                    (Some ? b)
    504                    old_register_03_value
    505                    old_register_04_value
    506                    old_register_05_value
    507                    old_register_06_value
    508                    old_register_07_value
    509                    old_register_10_value
    510                    old_register_11_value
    511                    old_register_12_value
    512                    old_register_13_value
    513                    old_register_14_value
    514                    old_register_15_value
    515                    old_register_16_value
    516                    old_register_17_value
    517                    old_register_20_value
    518                    old_register_21_value
    519                    old_register_22_value
    520                    old_register_23_value
    521                    old_register_24_value
    522                    old_register_25_value
    523                    old_register_26_value
    524                    old_register_27_value
    525                    old_register_30_value
    526                    old_register_31_value
    527                    old_register_32_value
    528                    old_register_33_value
    529                    old_register_34_value
    530                    old_register_35_value
    531                    old_register_36_value
    532                    old_register_37_value
    533                    old_register_A_value
    534                    old_register_B_value
    535                    old_register_DPL_value
    536                    old_register_DPH_value
    537                    old_register_Carry_value.
    538 
    539 definition update_register_03: Byte → RegisterMap → RegisterMap ≝
    540   λb: Byte.
    541   λm: RegisterMap.
    542   let old_register_00_value ≝ register_00_value m in
    543   let old_register_01_value ≝ register_01_value m in
    544   let old_register_02_value ≝ register_02_value m in
    545   let old_register_03_value ≝ register_03_value m in
    546   let old_register_04_value ≝ register_04_value m in
    547   let old_register_05_value ≝ register_05_value m in
    548   let old_register_06_value ≝ register_06_value m in
    549   let old_register_07_value ≝ register_07_value m in
    550   let old_register_10_value ≝ register_01_value m in
    551   let old_register_11_value ≝ register_01_value m in
    552   let old_register_12_value ≝ register_02_value m in
    553   let old_register_13_value ≝ register_03_value m in
    554   let old_register_14_value ≝ register_04_value m in
    555   let old_register_15_value ≝ register_05_value m in
    556   let old_register_16_value ≝ register_06_value m in
    557   let old_register_17_value ≝ register_07_value m in
    558   let old_register_20_value ≝ register_01_value m in
    559   let old_register_21_value ≝ register_02_value m in
    560   let old_register_22_value ≝ register_02_value m in
    561   let old_register_23_value ≝ register_03_value m in
    562   let old_register_24_value ≝ register_04_value m in
    563   let old_register_25_value ≝ register_05_value m in
    564   let old_register_26_value ≝ register_06_value m in
    565   let old_register_27_value ≝ register_07_value m in
    566   let old_register_30_value ≝ register_01_value m in
    567   let old_register_31_value ≝ register_02_value m in
    568   let old_register_32_value ≝ register_02_value m in
    569   let old_register_33_value ≝ register_03_value m in
    570   let old_register_34_value ≝ register_04_value m in
    571   let old_register_35_value ≝ register_05_value m in
    572   let old_register_36_value ≝ register_06_value m in
    573   let old_register_37_value ≝ register_07_value m in
    574   let old_register_A_value ≝ register_A_value m in
    575   let old_register_B_value ≝ register_B_value m in
    576   let old_register_DPL_value ≝ register_DPL_value m in
    577   let old_register_DPH_value ≝ register_DPH_value m in
    578   let old_register_Carry_value ≝ register_Carry_value m in
    579     mk_RegisterMap old_register_00_value
    580                    old_register_01_value
    581                    old_register_02_value
    582                    (Some ? b)
    583                    old_register_04_value
    584                    old_register_05_value
    585                    old_register_06_value
    586                    old_register_07_value
    587                    old_register_10_value
    588                    old_register_11_value
    589                    old_register_12_value
    590                    old_register_13_value
    591                    old_register_14_value
    592                    old_register_15_value
    593                    old_register_16_value
    594                    old_register_17_value
    595                    old_register_20_value
    596                    old_register_21_value
    597                    old_register_22_value
    598                    old_register_23_value
    599                    old_register_24_value
    600                    old_register_25_value
    601                    old_register_26_value
    602                    old_register_27_value
    603                    old_register_30_value
    604                    old_register_31_value
    605                    old_register_32_value
    606                    old_register_33_value
    607                    old_register_34_value
    608                    old_register_35_value
    609                    old_register_36_value
    610                    old_register_37_value
    611                    old_register_A_value
    612                    old_register_B_value
    613                    old_register_DPL_value
    614                    old_register_DPH_value
    615                    old_register_Carry_value.
    616 
    617 definition update_register_04: Byte → RegisterMap → RegisterMap ≝
    618   λb: Byte.
    619   λm: RegisterMap.
    620   let old_register_00_value ≝ register_00_value m in
    621   let old_register_01_value ≝ register_01_value m in
    622   let old_register_02_value ≝ register_02_value m in
    623   let old_register_03_value ≝ register_03_value m in
    624   let old_register_04_value ≝ register_04_value m in
    625   let old_register_05_value ≝ register_05_value m in
    626   let old_register_06_value ≝ register_06_value m in
    627   let old_register_07_value ≝ register_07_value m in
    628   let old_register_10_value ≝ register_01_value m in
    629   let old_register_11_value ≝ register_01_value m in
    630   let old_register_12_value ≝ register_02_value m in
    631   let old_register_13_value ≝ register_03_value m in
    632   let old_register_14_value ≝ register_04_value m in
    633   let old_register_15_value ≝ register_05_value m in
    634   let old_register_16_value ≝ register_06_value m in
    635   let old_register_17_value ≝ register_07_value m in
    636   let old_register_20_value ≝ register_01_value m in
    637   let old_register_21_value ≝ register_02_value m in
    638   let old_register_22_value ≝ register_02_value m in
    639   let old_register_23_value ≝ register_03_value m in
    640   let old_register_24_value ≝ register_04_value m in
    641   let old_register_25_value ≝ register_05_value m in
    642   let old_register_26_value ≝ register_06_value m in
    643   let old_register_27_value ≝ register_07_value m in
    644   let old_register_30_value ≝ register_01_value m in
    645   let old_register_31_value ≝ register_02_value m in
    646   let old_register_32_value ≝ register_02_value m in
    647   let old_register_33_value ≝ register_03_value m in
    648   let old_register_34_value ≝ register_04_value m in
    649   let old_register_35_value ≝ register_05_value m in
    650   let old_register_36_value ≝ register_06_value m in
    651   let old_register_37_value ≝ register_07_value m in
    652   let old_register_A_value ≝ register_A_value m in
    653   let old_register_B_value ≝ register_B_value m in
    654   let old_register_DPL_value ≝ register_DPL_value m in
    655   let old_register_DPH_value ≝ register_DPH_value m in
    656   let old_register_Carry_value ≝ register_Carry_value m in
    657     mk_RegisterMap old_register_00_value
    658                    old_register_01_value
    659                    old_register_02_value
    660                    old_register_03_value
    661                    (Some ? b)
    662                    old_register_05_value
    663                    old_register_06_value
    664                    old_register_07_value
    665                    old_register_10_value
    666                    old_register_11_value
    667                    old_register_12_value
    668                    old_register_13_value
    669                    old_register_14_value
    670                    old_register_15_value
    671                    old_register_16_value
    672                    old_register_17_value
    673                    old_register_20_value
    674                    old_register_21_value
    675                    old_register_22_value
    676                    old_register_23_value
    677                    old_register_24_value
    678                    old_register_25_value
    679                    old_register_26_value
    680                    old_register_27_value
    681                    old_register_30_value
    682                    old_register_31_value
    683                    old_register_32_value
    684                    old_register_33_value
    685                    old_register_34_value
    686                    old_register_35_value
    687                    old_register_36_value
    688                    old_register_37_value
    689                    old_register_A_value
    690                    old_register_B_value
    691                    old_register_DPL_value
    692                    old_register_DPH_value
    693                    old_register_Carry_value.
    694 
    695 definition update_register_05: Byte → RegisterMap → RegisterMap ≝
    696   λb: Byte.
    697   λm: RegisterMap.
    698   let old_register_00_value ≝ register_00_value m in
    699   let old_register_01_value ≝ register_01_value m in
    700   let old_register_02_value ≝ register_02_value m in
    701   let old_register_03_value ≝ register_03_value m in
    702   let old_register_04_value ≝ register_04_value m in
    703   let old_register_05_value ≝ register_05_value m in
    704   let old_register_06_value ≝ register_06_value m in
    705   let old_register_07_value ≝ register_07_value m in
    706   let old_register_10_value ≝ register_01_value m in
    707   let old_register_11_value ≝ register_01_value m in
    708   let old_register_12_value ≝ register_02_value m in
    709   let old_register_13_value ≝ register_03_value m in
    710   let old_register_14_value ≝ register_04_value m in
    711   let old_register_15_value ≝ register_05_value m in
    712   let old_register_16_value ≝ register_06_value m in
    713   let old_register_17_value ≝ register_07_value m in
    714   let old_register_20_value ≝ register_01_value m in
    715   let old_register_21_value ≝ register_02_value m in
    716   let old_register_22_value ≝ register_02_value m in
    717   let old_register_23_value ≝ register_03_value m in
    718   let old_register_24_value ≝ register_04_value m in
    719   let old_register_25_value ≝ register_05_value m in
    720   let old_register_26_value ≝ register_06_value m in
    721   let old_register_27_value ≝ register_07_value m in
    722   let old_register_30_value ≝ register_01_value m in
    723   let old_register_31_value ≝ register_02_value m in
    724   let old_register_32_value ≝ register_02_value m in
    725   let old_register_33_value ≝ register_03_value m in
    726   let old_register_34_value ≝ register_04_value m in
    727   let old_register_35_value ≝ register_05_value m in
    728   let old_register_36_value ≝ register_06_value m in
    729   let old_register_37_value ≝ register_07_value m in
    730   let old_register_A_value ≝ register_A_value m in
    731   let old_register_B_value ≝ register_B_value m in
    732   let old_register_DPL_value ≝ register_DPL_value m in
    733   let old_register_DPH_value ≝ register_DPH_value m in
    734   let old_register_Carry_value ≝ register_Carry_value m in
    735     mk_RegisterMap old_register_00_value
    736                    old_register_01_value
    737                    old_register_02_value
    738                    old_register_03_value
    739                    old_register_04_value
    740                    (Some ? b)
    741                    old_register_06_value
    742                    old_register_07_value
    743                    old_register_10_value
    744                    old_register_11_value
    745                    old_register_12_value
    746                    old_register_13_value
    747                    old_register_14_value
    748                    old_register_15_value
    749                    old_register_16_value
    750                    old_register_17_value
    751                    old_register_20_value
    752                    old_register_21_value
    753                    old_register_22_value
    754                    old_register_23_value
    755                    old_register_24_value
    756                    old_register_25_value
    757                    old_register_26_value
    758                    old_register_27_value
    759                    old_register_30_value
    760                    old_register_31_value
    761                    old_register_32_value
    762                    old_register_33_value
    763                    old_register_34_value
    764                    old_register_35_value
    765                    old_register_36_value
    766                    old_register_37_value
    767                    old_register_A_value
    768                    old_register_B_value
    769                    old_register_DPL_value
    770                    old_register_DPH_value
    771                    old_register_Carry_value.
    772 
    773 definition update_register_06: Byte → RegisterMap → RegisterMap ≝
    774   λb: Byte.
    775   λm: RegisterMap.
    776   let old_register_00_value ≝ register_00_value m in
    777   let old_register_01_value ≝ register_01_value m in
    778   let old_register_02_value ≝ register_02_value m in
    779   let old_register_03_value ≝ register_03_value m in
    780   let old_register_04_value ≝ register_04_value m in
    781   let old_register_05_value ≝ register_05_value m in
    782   let old_register_06_value ≝ register_06_value m in
    783   let old_register_07_value ≝ register_07_value m in
    784   let old_register_10_value ≝ register_01_value m in
    785   let old_register_11_value ≝ register_01_value m in
    786   let old_register_12_value ≝ register_02_value m in
    787   let old_register_13_value ≝ register_03_value m in
    788   let old_register_14_value ≝ register_04_value m in
    789   let old_register_15_value ≝ register_05_value m in
    790   let old_register_16_value ≝ register_06_value m in
    791   let old_register_17_value ≝ register_07_value m in
    792   let old_register_20_value ≝ register_01_value m in
    793   let old_register_21_value ≝ register_02_value m in
    794   let old_register_22_value ≝ register_02_value m in
    795   let old_register_23_value ≝ register_03_value m in
    796   let old_register_24_value ≝ register_04_value m in
    797   let old_register_25_value ≝ register_05_value m in
    798   let old_register_26_value ≝ register_06_value m in
    799   let old_register_27_value ≝ register_07_value m in
    800   let old_register_30_value ≝ register_01_value m in
    801   let old_register_31_value ≝ register_02_value m in
    802   let old_register_32_value ≝ register_02_value m in
    803   let old_register_33_value ≝ register_03_value m in
    804   let old_register_34_value ≝ register_04_value m in
    805   let old_register_35_value ≝ register_05_value m in
    806   let old_register_36_value ≝ register_06_value m in
    807   let old_register_37_value ≝ register_07_value m in
    808   let old_register_A_value ≝ register_A_value m in
    809   let old_register_B_value ≝ register_B_value m in
    810   let old_register_DPL_value ≝ register_DPL_value m in
    811   let old_register_DPH_value ≝ register_DPH_value m in
    812   let old_register_Carry_value ≝ register_Carry_value m in
    813     mk_RegisterMap old_register_00_value
    814                    old_register_01_value
    815                    old_register_02_value
    816                    old_register_03_value
    817                    old_register_04_value
    818                    old_register_05_value
    819                    (Some ? b)
    820                    old_register_07_value
    821                    old_register_10_value
    822                    old_register_11_value
    823                    old_register_12_value
    824                    old_register_13_value
    825                    old_register_14_value
    826                    old_register_15_value
    827                    old_register_16_value
    828                    old_register_17_value
    829                    old_register_20_value
    830                    old_register_21_value
    831                    old_register_22_value
    832                    old_register_23_value
    833                    old_register_24_value
    834                    old_register_25_value
    835                    old_register_26_value
    836                    old_register_27_value
    837                    old_register_30_value
    838                    old_register_31_value
    839                    old_register_32_value
    840                    old_register_33_value
    841                    old_register_34_value
    842                    old_register_35_value
    843                    old_register_36_value
    844                    old_register_37_value
    845                    old_register_A_value
    846                    old_register_B_value
    847                    old_register_DPL_value
    848                    old_register_DPH_value
    849                    old_register_Carry_value.
    850 
    851 definition update_register_07: Byte → RegisterMap → RegisterMap ≝
    852   λb: Byte.
    853   λm: RegisterMap.
    854   let old_register_00_value ≝ register_00_value m in
    855   let old_register_01_value ≝ register_01_value m in
    856   let old_register_02_value ≝ register_02_value m in
    857   let old_register_03_value ≝ register_03_value m in
    858   let old_register_04_value ≝ register_04_value m in
    859   let old_register_05_value ≝ register_05_value m in
    860   let old_register_06_value ≝ register_06_value m in
    861   let old_register_07_value ≝ register_07_value m in
    862   let old_register_10_value ≝ register_01_value m in
    863   let old_register_11_value ≝ register_01_value m in
    864   let old_register_12_value ≝ register_02_value m in
    865   let old_register_13_value ≝ register_03_value m in
    866   let old_register_14_value ≝ register_04_value m in
    867   let old_register_15_value ≝ register_05_value m in
    868   let old_register_16_value ≝ register_06_value m in
    869   let old_register_17_value ≝ register_07_value m in
    870   let old_register_20_value ≝ register_01_value m in
    871   let old_register_21_value ≝ register_02_value m in
    872   let old_register_22_value ≝ register_02_value m in
    873   let old_register_23_value ≝ register_03_value m in
    874   let old_register_24_value ≝ register_04_value m in
    875   let old_register_25_value ≝ register_05_value m in
    876   let old_register_26_value ≝ register_06_value m in
    877   let old_register_27_value ≝ register_07_value m in
    878   let old_register_30_value ≝ register_01_value m in
    879   let old_register_31_value ≝ register_02_value m in
    880   let old_register_32_value ≝ register_02_value m in
    881   let old_register_33_value ≝ register_03_value m in
    882   let old_register_34_value ≝ register_04_value m in
    883   let old_register_35_value ≝ register_05_value m in
    884   let old_register_36_value ≝ register_06_value m in
    885   let old_register_37_value ≝ register_07_value m in
    886   let old_register_A_value ≝ register_A_value m in
    887   let old_register_B_value ≝ register_B_value m in
    888   let old_register_DPL_value ≝ register_DPL_value m in
    889   let old_register_DPH_value ≝ register_DPH_value m in
    890   let old_register_Carry_value ≝ register_Carry_value m in
    891     mk_RegisterMap old_register_00_value
    892                    old_register_01_value
    893                    old_register_02_value
    894                    old_register_03_value
    895                    old_register_04_value
    896                    old_register_05_value
    897                    old_register_06_value
    898                    (Some ? b)
    899                    old_register_10_value
    900                    old_register_11_value
    901                    old_register_12_value
    902                    old_register_13_value
    903                    old_register_14_value
    904                    old_register_15_value
    905                    old_register_16_value
    906                    old_register_17_value
    907                    old_register_20_value
    908                    old_register_21_value
    909                    old_register_22_value
    910                    old_register_23_value
    911                    old_register_24_value
    912                    old_register_25_value
    913                    old_register_26_value
    914                    old_register_27_value
    915                    old_register_30_value
    916                    old_register_31_value
    917                    old_register_32_value
    918                    old_register_33_value
    919                    old_register_34_value
    920                    old_register_35_value
    921                    old_register_36_value
    922                    old_register_37_value
    923                    old_register_A_value
    924                    old_register_B_value
    925                    old_register_DPL_value
    926                    old_register_DPH_value
    927                    old_register_Carry_value.
    928 
    929 definition update_register_10: Byte → RegisterMap → RegisterMap ≝
    930   λb: Byte.
    931   λm: RegisterMap.
    932   let old_register_00_value ≝ register_00_value m in
    933   let old_register_01_value ≝ register_01_value m in
    934   let old_register_02_value ≝ register_02_value m in
    935   let old_register_03_value ≝ register_03_value m in
    936   let old_register_04_value ≝ register_04_value m in
    937   let old_register_05_value ≝ register_05_value m in
    938   let old_register_06_value ≝ register_06_value m in
    939   let old_register_07_value ≝ register_07_value m in
    940   let old_register_10_value ≝ register_01_value m in
    941   let old_register_11_value ≝ register_01_value m in
    942   let old_register_12_value ≝ register_02_value m in
    943   let old_register_13_value ≝ register_03_value m in
    944   let old_register_14_value ≝ register_04_value m in
    945   let old_register_15_value ≝ register_05_value m in
    946   let old_register_16_value ≝ register_06_value m in
    947   let old_register_17_value ≝ register_07_value m in
    948   let old_register_20_value ≝ register_01_value m in
    949   let old_register_21_value ≝ register_02_value m in
    950   let old_register_22_value ≝ register_02_value m in
    951   let old_register_23_value ≝ register_03_value m in
    952   let old_register_24_value ≝ register_04_value m in
    953   let old_register_25_value ≝ register_05_value m in
    954   let old_register_26_value ≝ register_06_value m in
    955   let old_register_27_value ≝ register_07_value m in
    956   let old_register_30_value ≝ register_01_value m in
    957   let old_register_31_value ≝ register_02_value m in
    958   let old_register_32_value ≝ register_02_value m in
    959   let old_register_33_value ≝ register_03_value m in
    960   let old_register_34_value ≝ register_04_value m in
    961   let old_register_35_value ≝ register_05_value m in
    962   let old_register_36_value ≝ register_06_value m in
    963   let old_register_37_value ≝ register_07_value m in
    964   let old_register_A_value ≝ register_A_value m in
    965   let old_register_B_value ≝ register_B_value m in
    966   let old_register_DPL_value ≝ register_DPL_value m in
    967   let old_register_DPH_value ≝ register_DPH_value m in
    968   let old_register_Carry_value ≝ register_Carry_value m in
    969     mk_RegisterMap old_register_00_value
    970                    old_register_01_value
    971                    old_register_02_value
    972                    old_register_03_value
    973                    old_register_04_value
    974                    old_register_05_value
    975                    old_register_06_value
    976                    old_register_07_value
    977                    (Some ? b)
    978                    old_register_11_value
    979                    old_register_12_value
    980                    old_register_13_value
    981                    old_register_14_value
    982                    old_register_15_value
    983                    old_register_16_value
    984                    old_register_17_value
    985                    old_register_20_value
    986                    old_register_21_value
    987                    old_register_22_value
    988                    old_register_23_value
    989                    old_register_24_value
    990                    old_register_25_value
    991                    old_register_26_value
    992                    old_register_27_value
    993                    old_register_30_value
    994                    old_register_31_value
    995                    old_register_32_value
    996                    old_register_33_value
    997                    old_register_34_value
    998                    old_register_35_value
    999                    old_register_36_value
    1000                    old_register_37_value
    1001                    old_register_A_value
    1002                    old_register_B_value
    1003                    old_register_DPL_value
    1004                    old_register_DPH_value
    1005                    old_register_Carry_value.
    1006 
    1007 definition update_register_11: Byte → RegisterMap → RegisterMap ≝
    1008   λb: Byte.
    1009   λm: RegisterMap.
    1010   let old_register_00_value ≝ register_00_value m in
    1011   let old_register_01_value ≝ register_01_value m in
    1012   let old_register_02_value ≝ register_02_value m in
    1013   let old_register_03_value ≝ register_03_value m in
    1014   let old_register_04_value ≝ register_04_value m in
    1015   let old_register_05_value ≝ register_05_value m in
    1016   let old_register_06_value ≝ register_06_value m in
    1017   let old_register_07_value ≝ register_07_value m in
    1018   let old_register_10_value ≝ register_01_value m in
    1019   let old_register_11_value ≝ register_01_value m in
    1020   let old_register_12_value ≝ register_02_value m in
    1021   let old_register_13_value ≝ register_03_value m in
    1022   let old_register_14_value ≝ register_04_value m in
    1023   let old_register_15_value ≝ register_05_value m in
    1024   let old_register_16_value ≝ register_06_value m in
    1025   let old_register_17_value ≝ register_07_value m in
    1026   let old_register_20_value ≝ register_01_value m in
    1027   let old_register_21_value ≝ register_02_value m in
    1028   let old_register_22_value ≝ register_02_value m in
    1029   let old_register_23_value ≝ register_03_value m in
    1030   let old_register_24_value ≝ register_04_value m in
    1031   let old_register_25_value ≝ register_05_value m in
    1032   let old_register_26_value ≝ register_06_value m in
    1033   let old_register_27_value ≝ register_07_value m in
    1034   let old_register_30_value ≝ register_01_value m in
    1035   let old_register_31_value ≝ register_02_value m in
    1036   let old_register_32_value ≝ register_02_value m in
    1037   let old_register_33_value ≝ register_03_value m in
    1038   let old_register_34_value ≝ register_04_value m in
    1039   let old_register_35_value ≝ register_05_value m in
    1040   let old_register_36_value ≝ register_06_value m in
    1041   let old_register_37_value ≝ register_07_value m in
    1042   let old_register_A_value ≝ register_A_value m in
    1043   let old_register_B_value ≝ register_B_value m in
    1044   let old_register_DPL_value ≝ register_DPL_value m in
    1045   let old_register_DPH_value ≝ register_DPH_value m in
    1046   let old_register_Carry_value ≝ register_Carry_value m in
    1047     mk_RegisterMap old_register_00_value
    1048                    old_register_01_value
    1049                    old_register_02_value
    1050                    old_register_03_value
    1051                    old_register_04_value
    1052                    old_register_05_value
    1053                    old_register_06_value
    1054                    old_register_07_value
    1055                    old_register_10_value
    1056                    (Some ? b)
    1057                    old_register_12_value
    1058                    old_register_13_value
    1059                    old_register_14_value
    1060                    old_register_15_value
    1061                    old_register_16_value
    1062                    old_register_17_value
    1063                    old_register_20_value
    1064                    old_register_21_value
    1065                    old_register_22_value
    1066                    old_register_23_value
    1067                    old_register_24_value
    1068                    old_register_25_value
    1069                    old_register_26_value
    1070                    old_register_27_value
    1071                    old_register_30_value
    1072                    old_register_31_value
    1073                    old_register_32_value
    1074                    old_register_33_value
    1075                    old_register_34_value
    1076                    old_register_35_value
    1077                    old_register_36_value
    1078                    old_register_37_value
    1079                    old_register_A_value
    1080                    old_register_B_value
    1081                    old_register_DPL_value
    1082                    old_register_DPH_value
    1083                    old_register_Carry_value.
    1084 
    1085 definition update_register_12: Byte → RegisterMap → RegisterMap ≝
    1086   λb: Byte.
    1087   λm: RegisterMap.
    1088   let old_register_00_value ≝ register_00_value m in
    1089   let old_register_01_value ≝ register_01_value m in
    1090   let old_register_02_value ≝ register_02_value m in
    1091   let old_register_03_value ≝ register_03_value m in
    1092   let old_register_04_value ≝ register_04_value m in
    1093   let old_register_05_value ≝ register_05_value m in
    1094   let old_register_06_value ≝ register_06_value m in
    1095   let old_register_07_value ≝ register_07_value m in
    1096   let old_register_10_value ≝ register_01_value m in
    1097   let old_register_11_value ≝ register_01_value m in
    1098   let old_register_12_value ≝ register_02_value m in
    1099   let old_register_13_value ≝ register_03_value m in
    1100   let old_register_14_value ≝ register_04_value m in
    1101   let old_register_15_value ≝ register_05_value m in
    1102   let old_register_16_value ≝ register_06_value m in
    1103   let old_register_17_value ≝ register_07_value m in
    1104   let old_register_20_value ≝ register_01_value m in
    1105   let old_register_21_value ≝ register_02_value m in
    1106   let old_register_22_value ≝ register_02_value m in
    1107   let old_register_23_value ≝ register_03_value m in
    1108   let old_register_24_value ≝ register_04_value m in
    1109   let old_register_25_value ≝ register_05_value m in
    1110   let old_register_26_value ≝ register_06_value m in
    1111   let old_register_27_value ≝ register_07_value m in
    1112   let old_register_30_value ≝ register_01_value m in
    1113   let old_register_31_value ≝ register_02_value m in
    1114   let old_register_32_value ≝ register_02_value m in
    1115   let old_register_33_value ≝ register_03_value m in
    1116   let old_register_34_value ≝ register_04_value m in
    1117   let old_register_35_value ≝ register_05_value m in
    1118   let old_register_36_value ≝ register_06_value m in
    1119   let old_register_37_value ≝ register_07_value m in
    1120   let old_register_A_value ≝ register_A_value m in
    1121   let old_register_B_value ≝ register_B_value m in
    1122   let old_register_DPL_value ≝ register_DPL_value m in
    1123   let old_register_DPH_value ≝ register_DPH_value m in
    1124   let old_register_Carry_value ≝ register_Carry_value m in
    1125     mk_RegisterMap old_register_00_value
    1126                    old_register_01_value
    1127                    old_register_02_value
    1128                    old_register_03_value
    1129                    old_register_04_value
    1130                    old_register_05_value
    1131                    old_register_06_value
    1132                    old_register_07_value
    1133                    old_register_10_value
    1134                    old_register_11_value
    1135                    (Some ? b)
    1136                    old_register_13_value
    1137                    old_register_14_value
    1138                    old_register_15_value
    1139                    old_register_16_value
    1140                    old_register_17_value
    1141                    old_register_20_value
    1142                    old_register_21_value
    1143                    old_register_22_value
    1144                    old_register_23_value
    1145                    old_register_24_value
    1146                    old_register_25_value
    1147                    old_register_26_value
    1148                    old_register_27_value
    1149                    old_register_30_value
    1150                    old_register_31_value
    1151                    old_register_32_value
    1152                    old_register_33_value
    1153                    old_register_34_value
    1154                    old_register_35_value
    1155                    old_register_36_value
    1156                    old_register_37_value
    1157                    old_register_A_value
    1158                    old_register_B_value
    1159                    old_register_DPL_value
    1160                    old_register_DPH_value
    1161                    old_register_Carry_value.
    1162 
    1163 definition update_register_13: Byte → RegisterMap → RegisterMap ≝
    1164   λb: Byte.
    1165   λm: RegisterMap.
    1166   let old_register_00_value ≝ register_00_value m in
    1167   let old_register_01_value ≝ register_01_value m in
    1168   let old_register_02_value ≝ register_02_value m in
    1169   let old_register_03_value ≝ register_03_value m in
    1170   let old_register_04_value ≝ register_04_value m in
    1171   let old_register_05_value ≝ register_05_value m in
    1172   let old_register_06_value ≝ register_06_value m in
    1173   let old_register_07_value ≝ register_07_value m in
    1174   let old_register_10_value ≝ register_01_value m in
    1175   let old_register_11_value ≝ register_01_value m in
    1176   let old_register_12_value ≝ register_02_value m in
    1177   let old_register_13_value ≝ register_03_value m in
    1178   let old_register_14_value ≝ register_04_value m in
    1179   let old_register_15_value ≝ register_05_value m in
    1180   let old_register_16_value ≝ register_06_value m in
    1181   let old_register_17_value ≝ register_07_value m in
    1182   let old_register_20_value ≝ register_01_value m in
    1183   let old_register_21_value ≝ register_02_value m in
    1184   let old_register_22_value ≝ register_02_value m in
    1185   let old_register_23_value ≝ register_03_value m in
    1186   let old_register_24_value ≝ register_04_value m in
    1187   let old_register_25_value ≝ register_05_value m in
    1188   let old_register_26_value ≝ register_06_value m in
    1189   let old_register_27_value ≝ register_07_value m in
    1190   let old_register_30_value ≝ register_01_value m in
    1191   let old_register_31_value ≝ register_02_value m in
    1192   let old_register_32_value ≝ register_02_value m in
    1193   let old_register_33_value ≝ register_03_value m in
    1194   let old_register_34_value ≝ register_04_value m in
    1195   let old_register_35_value ≝ register_05_value m in
    1196   let old_register_36_value ≝ register_06_value m in
    1197   let old_register_37_value ≝ register_07_value m in
    1198   let old_register_A_value ≝ register_A_value m in
    1199   let old_register_B_value ≝ register_B_value m in
    1200   let old_register_DPL_value ≝ register_DPL_value m in
    1201   let old_register_DPH_value ≝ register_DPH_value m in
    1202   let old_register_Carry_value ≝ register_Carry_value m in
    1203     mk_RegisterMap old_register_00_value
    1204                    old_register_01_value
    1205                    old_register_02_value
    1206                    old_register_03_value
    1207                    old_register_04_value
    1208                    old_register_05_value
    1209                    old_register_06_value
    1210                    old_register_07_value
    1211                    old_register_10_value
    1212                    old_register_11_value
    1213                    old_register_12_value
    1214                    (Some ? b)
    1215                    old_register_14_value
    1216                    old_register_15_value
    1217                    old_register_16_value
    1218                    old_register_17_value
    1219                    old_register_20_value
    1220                    old_register_21_value
    1221                    old_register_22_value
    1222                    old_register_23_value
    1223                    old_register_24_value
    1224                    old_register_25_value
    1225                    old_register_26_value
    1226                    old_register_27_value
    1227                    old_register_30_value
    1228                    old_register_31_value
    1229                    old_register_32_value
    1230                    old_register_33_value
    1231                    old_register_34_value
    1232                    old_register_35_value
    1233                    old_register_36_value
    1234                    old_register_37_value
    1235                    old_register_A_value
    1236                    old_register_B_value
    1237                    old_register_DPL_value
    1238                    old_register_DPH_value
    1239                    old_register_Carry_value.
    1240 
    1241 definition update_register_14: Byte → RegisterMap → RegisterMap ≝
    1242   λb: Byte.
    1243   λm: RegisterMap.
    1244   let old_register_00_value ≝ register_00_value m in
    1245   let old_register_01_value ≝ register_01_value m in
    1246   let old_register_02_value ≝ register_02_value m in
    1247   let old_register_03_value ≝ register_03_value m in
    1248   let old_register_04_value ≝ register_04_value m in
    1249   let old_register_05_value ≝ register_05_value m in
    1250   let old_register_06_value ≝ register_06_value m in
    1251   let old_register_07_value ≝ register_07_value m in
    1252   let old_register_10_value ≝ register_01_value m in
    1253   let old_register_11_value ≝ register_01_value m in
    1254   let old_register_12_value ≝ register_02_value m in
    1255   let old_register_13_value ≝ register_03_value m in
    1256   let old_register_14_value ≝ register_04_value m in
    1257   let old_register_15_value ≝ register_05_value m in
    1258   let old_register_16_value ≝ register_06_value m in
    1259   let old_register_17_value ≝ register_07_value m in
    1260   let old_register_20_value ≝ register_01_value m in
    1261   let old_register_21_value ≝ register_02_value m in
    1262   let old_register_22_value ≝ register_02_value m in
    1263   let old_register_23_value ≝ register_03_value m in
    1264   let old_register_24_value ≝ register_04_value m in
    1265   let old_register_25_value ≝ register_05_value m in
    1266   let old_register_26_value ≝ register_06_value m in
    1267   let old_register_27_value ≝ register_07_value m in
    1268   let old_register_30_value ≝ register_01_value m in
    1269   let old_register_31_value ≝ register_02_value m in
    1270   let old_register_32_value ≝ register_02_value m in
    1271   let old_register_33_value ≝ register_03_value m in
    1272   let old_register_34_value ≝ register_04_value m in
    1273   let old_register_35_value ≝ register_05_value m in
    1274   let old_register_36_value ≝ register_06_value m in
    1275   let old_register_37_value ≝ register_07_value m in
    1276   let old_register_A_value ≝ register_A_value m in
    1277   let old_register_B_value ≝ register_B_value m in
    1278   let old_register_DPL_value ≝ register_DPL_value m in
    1279   let old_register_DPH_value ≝ register_DPH_value m in
    1280   let old_register_Carry_value ≝ register_Carry_value m in
    1281     mk_RegisterMap old_register_00_value
    1282                    old_register_01_value
    1283                    old_register_02_value
    1284                    old_register_03_value
    1285                    old_register_04_value
    1286                    old_register_05_value
    1287                    old_register_06_value
    1288                    old_register_07_value
    1289                    old_register_10_value
    1290                    old_register_11_value
    1291                    old_register_12_value
    1292                    old_register_13_value
    1293                    (Some ? b)
    1294                    old_register_15_value
    1295                    old_register_16_value
    1296                    old_register_17_value
    1297                    old_register_20_value
    1298                    old_register_21_value
    1299                    old_register_22_value
    1300                    old_register_23_value
    1301                    old_register_24_value
    1302                    old_register_25_value
    1303                    old_register_26_value
    1304                    old_register_27_value
    1305                    old_register_30_value
    1306                    old_register_31_value
    1307                    old_register_32_value
    1308                    old_register_33_value
    1309                    old_register_34_value
    1310                    old_register_35_value
    1311                    old_register_36_value
    1312                    old_register_37_value
    1313                    old_register_A_value
    1314                    old_register_B_value
    1315                    old_register_DPL_value
    1316                    old_register_DPH_value
    1317                    old_register_Carry_value.
    1318 
    1319 definition update_register_15: Byte → RegisterMap → RegisterMap ≝
    1320   λb: Byte.
    1321   λm: RegisterMap.
    1322   let old_register_00_value ≝ register_00_value m in
    1323   let old_register_01_value ≝ register_01_value m in
    1324   let old_register_02_value ≝ register_02_value m in
    1325   let old_register_03_value ≝ register_03_value m in
    1326   let old_register_04_value ≝ register_04_value m in
    1327   let old_register_05_value ≝ register_05_value m in
    1328   let old_register_06_value ≝ register_06_value m in
    1329   let old_register_07_value ≝ register_07_value m in
    1330   let old_register_10_value ≝ register_01_value m in
    1331   let old_register_11_value ≝ register_01_value m in
    1332   let old_register_12_value ≝ register_02_value m in
    1333   let old_register_13_value ≝ register_03_value m in
    1334   let old_register_14_value ≝ register_04_value m in
    1335   let old_register_15_value ≝ register_05_value m in
    1336   let old_register_16_value ≝ register_06_value m in
    1337   let old_register_17_value ≝ register_07_value m in
    1338   let old_register_20_value ≝ register_01_value m in
    1339   let old_register_21_value ≝ register_02_value m in
    1340   let old_register_22_value ≝ register_02_value m in
    1341   let old_register_23_value ≝ register_03_value m in
    1342   let old_register_24_value ≝ register_04_value m in
    1343   let old_register_25_value ≝ register_05_value m in
    1344   let old_register_26_value ≝ register_06_value m in
    1345   let old_register_27_value ≝ register_07_value m in
    1346   let old_register_30_value ≝ register_01_value m in
    1347   let old_register_31_value ≝ register_02_value m in
    1348   let old_register_32_value ≝ register_02_value m in
    1349   let old_register_33_value ≝ register_03_value m in
    1350   let old_register_34_value ≝ register_04_value m in
    1351   let old_register_35_value ≝ register_05_value m in
    1352   let old_register_36_value ≝ register_06_value m in
    1353   let old_register_37_value ≝ register_07_value m in
    1354   let old_register_A_value ≝ register_A_value m in
    1355   let old_register_B_value ≝ register_B_value m in
    1356   let old_register_DPL_value ≝ register_DPL_value m in
    1357   let old_register_DPH_value ≝ register_DPH_value m in
    1358   let old_register_Carry_value ≝ register_Carry_value m in
    1359     mk_RegisterMap old_register_00_value
    1360                    old_register_01_value
    1361                    old_register_02_value
    1362                    old_register_03_value
    1363                    old_register_04_value
    1364                    old_register_05_value
    1365                    old_register_06_value
    1366                    old_register_07_value
    1367                    old_register_10_value
    1368                    old_register_11_value
    1369                    old_register_12_value
    1370                    old_register_13_value
    1371                    old_register_14_value
    1372                    (Some ? b)
    1373                    old_register_16_value
    1374                    old_register_17_value
    1375                    old_register_20_value
    1376                    old_register_21_value
    1377                    old_register_22_value
    1378                    old_register_23_value
    1379                    old_register_24_value
    1380                    old_register_25_value
    1381                    old_register_26_value
    1382                    old_register_27_value
    1383                    old_register_30_value
    1384                    old_register_31_value
    1385                    old_register_32_value
    1386                    old_register_33_value
    1387                    old_register_34_value
    1388                    old_register_35_value
    1389                    old_register_36_value
    1390                    old_register_37_value
    1391                    old_register_A_value
    1392                    old_register_B_value
    1393                    old_register_DPL_value
    1394                    old_register_DPH_value
    1395                    old_register_Carry_value.
    1396 
    1397 definition update_register_16: Byte → RegisterMap → RegisterMap ≝
    1398   λb: Byte.
    1399   λm: RegisterMap.
    1400   let old_register_00_value ≝ register_00_value m in
    1401   let old_register_01_value ≝ register_01_value m in
    1402   let old_register_02_value ≝ register_02_value m in
    1403   let old_register_03_value ≝ register_03_value m in
    1404   let old_register_04_value ≝ register_04_value m in
    1405   let old_register_05_value ≝ register_05_value m in
    1406   let old_register_06_value ≝ register_06_value m in
    1407   let old_register_07_value ≝ register_07_value m in
    1408   let old_register_10_value ≝ register_01_value m in
    1409   let old_register_11_value ≝ register_01_value m in
    1410   let old_register_12_value ≝ register_02_value m in
    1411   let old_register_13_value ≝ register_03_value m in
    1412   let old_register_14_value ≝ register_04_value m in
    1413   let old_register_15_value ≝ register_05_value m in
    1414   let old_register_16_value ≝ register_06_value m in
    1415   let old_register_17_value ≝ register_07_value m in
    1416   let old_register_20_value ≝ register_01_value m in
    1417   let old_register_21_value ≝ register_02_value m in
    1418   let old_register_22_value ≝ register_02_value m in
    1419   let old_register_23_value ≝ register_03_value m in
    1420   let old_register_24_value ≝ register_04_value m in
    1421   let old_register_25_value ≝ register_05_value m in
    1422   let old_register_26_value ≝ register_06_value m in
    1423   let old_register_27_value ≝ register_07_value m in
    1424   let old_register_30_value ≝ register_01_value m in
    1425   let old_register_31_value ≝ register_02_value m in
    1426   let old_register_32_value ≝ register_02_value m in
    1427   let old_register_33_value ≝ register_03_value m in
    1428   let old_register_34_value ≝ register_04_value m in
    1429   let old_register_35_value ≝ register_05_value m in
    1430   let old_register_36_value ≝ register_06_value m in
    1431   let old_register_37_value ≝ register_07_value m in
    1432   let old_register_A_value ≝ register_A_value m in
    1433   let old_register_B_value ≝ register_B_value m in
    1434   let old_register_DPL_value ≝ register_DPL_value m in
    1435   let old_register_DPH_value ≝ register_DPH_value m in
    1436   let old_register_Carry_value ≝ register_Carry_value m in
    1437     mk_RegisterMap old_register_00_value
    1438                    old_register_01_value
    1439                    old_register_02_value
    1440                    old_register_03_value
    1441                    old_register_04_value
    1442                    old_register_05_value
    1443                    old_register_06_value
    1444                    old_register_07_value
    1445                    old_register_10_value
    1446                    old_register_11_value
    1447                    old_register_12_value
    1448                    old_register_13_value
    1449                    old_register_14_value
    1450                    old_register_15_value
    1451                    (Some ? b)
    1452                    old_register_17_value
    1453                    old_register_20_value
    1454                    old_register_21_value
    1455                    old_register_22_value
    1456                    old_register_23_value
    1457                    old_register_24_value
    1458                    old_register_25_value
    1459                    old_register_26_value
    1460                    old_register_27_value
    1461                    old_register_30_value
    1462                    old_register_31_value
    1463                    old_register_32_value
    1464                    old_register_33_value
    1465                    old_register_34_value
    1466                    old_register_35_value
    1467                    old_register_36_value
    1468                    old_register_37_value
    1469                    old_register_A_value
    1470                    old_register_B_value
    1471                    old_register_DPL_value
    1472                    old_register_DPH_value
    1473                    old_register_Carry_value.
    1474 
    1475 definition update_register_17: Byte → RegisterMap → RegisterMap ≝
    1476   λb: Byte.
    1477   λm: RegisterMap.
    1478   let old_register_00_value ≝ register_00_value m in
    1479   let old_register_01_value ≝ register_01_value m in
    1480   let old_register_02_value ≝ register_02_value m in
    1481   let old_register_03_value ≝ register_03_value m in
    1482   let old_register_04_value ≝ register_04_value m in
    1483   let old_register_05_value ≝ register_05_value m in
    1484   let old_register_06_value ≝ register_06_value m in
    1485   let old_register_07_value ≝ register_07_value m in
    1486   let old_register_10_value ≝ register_01_value m in
    1487   let old_register_11_value ≝ register_01_value m in
    1488   let old_register_12_value ≝ register_02_value m in
    1489   let old_register_13_value ≝ register_03_value m in
    1490   let old_register_14_value ≝ register_04_value m in
    1491   let old_register_15_value ≝ register_05_value m in
    1492   let old_register_16_value ≝ register_06_value m in
    1493   let old_register_17_value ≝ register_07_value m in
    1494   let old_register_20_value ≝ register_01_value m in
    1495   let old_register_21_value ≝ register_02_value m in
    1496   let old_register_22_value ≝ register_02_value m in
    1497   let old_register_23_value ≝ register_03_value m in
    1498   let old_register_24_value ≝ register_04_value m in
    1499   let old_register_25_value ≝ register_05_value m in
    1500   let old_register_26_value ≝ register_06_value m in
    1501   let old_register_27_value ≝ register_07_value m in
    1502   let old_register_30_value ≝ register_01_value m in
    1503   let old_register_31_value ≝ register_02_value m in
    1504   let old_register_32_value ≝ register_02_value m in
    1505   let old_register_33_value ≝ register_03_value m in
    1506   let old_register_34_value ≝ register_04_value m in
    1507   let old_register_35_value ≝ register_05_value m in
    1508   let old_register_36_value ≝ register_06_value m in
    1509   let old_register_37_value ≝ register_07_value m in
    1510   let old_register_A_value ≝ register_A_value m in
    1511   let old_register_B_value ≝ register_B_value m in
    1512   let old_register_DPL_value ≝ register_DPL_value m in
    1513   let old_register_DPH_value ≝ register_DPH_value m in
    1514   let old_register_Carry_value ≝ register_Carry_value m in
    1515     mk_RegisterMap old_register_00_value
    1516                    old_register_01_value
    1517                    old_register_02_value
    1518                    old_register_03_value
    1519                    old_register_04_value
    1520                    old_register_05_value
    1521                    old_register_06_value
    1522                    old_register_07_value
    1523                    old_register_10_value
    1524                    old_register_11_value
    1525                    old_register_12_value
    1526                    old_register_13_value
    1527                    old_register_14_value
    1528                    old_register_15_value
    1529                    old_register_16_value
    1530                    (Some ? b)
    1531                    old_register_20_value
    1532                    old_register_21_value
    1533                    old_register_22_value
    1534                    old_register_23_value
    1535                    old_register_24_value
    1536                    old_register_25_value
    1537                    old_register_26_value
    1538                    old_register_27_value
    1539                    old_register_30_value
    1540                    old_register_31_value
    1541                    old_register_32_value
    1542                    old_register_33_value
    1543                    old_register_34_value
    1544                    old_register_35_value
    1545                    old_register_36_value
    1546                    old_register_37_value
    1547                    old_register_A_value
    1548                    old_register_B_value
    1549                    old_register_DPL_value
    1550                    old_register_DPH_value
    1551                    old_register_Carry_value.
    1552 
    1553 definition update_register_20: Byte → RegisterMap → RegisterMap ≝
    1554   λb: Byte.
    1555   λm: RegisterMap.
    1556   let old_register_00_value ≝ register_00_value m in
    1557   let old_register_01_value ≝ register_01_value m in
    1558   let old_register_02_value ≝ register_02_value m in
    1559   let old_register_03_value ≝ register_03_value m in
    1560   let old_register_04_value ≝ register_04_value m in
    1561   let old_register_05_value ≝ register_05_value m in
    1562   let old_register_06_value ≝ register_06_value m in
    1563   let old_register_07_value ≝ register_07_value m in
    1564   let old_register_10_value ≝ register_01_value m in
    1565   let old_register_11_value ≝ register_01_value m in
    1566   let old_register_12_value ≝ register_02_value m in
    1567   let old_register_13_value ≝ register_03_value m in
    1568   let old_register_14_value ≝ register_04_value m in
    1569   let old_register_15_value ≝ register_05_value m in
    1570   let old_register_16_value ≝ register_06_value m in
    1571   let old_register_17_value ≝ register_07_value m in
    1572   let old_register_20_value ≝ register_01_value m in
    1573   let old_register_21_value ≝ register_02_value m in
    1574   let old_register_22_value ≝ register_02_value m in
    1575   let old_register_23_value ≝ register_03_value m in
    1576   let old_register_24_value ≝ register_04_value m in
    1577   let old_register_25_value ≝ register_05_value m in
    1578   let old_register_26_value ≝ register_06_value m in
    1579   let old_register_27_value ≝ register_07_value m in
    1580   let old_register_30_value ≝ register_01_value m in
    1581   let old_register_31_value ≝ register_02_value m in
    1582   let old_register_32_value ≝ register_02_value m in
    1583   let old_register_33_value ≝ register_03_value m in
    1584   let old_register_34_value ≝ register_04_value m in
    1585   let old_register_35_value ≝ register_05_value m in
    1586   let old_register_36_value ≝ register_06_value m in
    1587   let old_register_37_value ≝ register_07_value m in
    1588   let old_register_A_value ≝ register_A_value m in
    1589   let old_register_B_value ≝ register_B_value m in
    1590   let old_register_DPL_value ≝ register_DPL_value m in
    1591   let old_register_DPH_value ≝ register_DPH_value m in
    1592   let old_register_Carry_value ≝ register_Carry_value m in
    1593     mk_RegisterMap old_register_00_value
    1594                    old_register_01_value
    1595                    old_register_02_value
    1596                    old_register_03_value
    1597                    old_register_04_value
    1598                    old_register_05_value
    1599                    old_register_06_value
    1600                    old_register_07_value
    1601                    old_register_10_value
    1602                    old_register_11_value
    1603                    old_register_12_value
    1604                    old_register_13_value
    1605                    old_register_14_value
    1606                    old_register_15_value
    1607                    old_register_16_value
    1608                    old_register_17_value
    1609                    (Some ? b)
    1610                    old_register_21_value
    1611                    old_register_22_value
    1612                    old_register_23_value
    1613                    old_register_24_value
    1614                    old_register_25_value
    1615                    old_register_26_value
    1616                    old_register_27_value
    1617                    old_register_30_value
    1618                    old_register_31_value
    1619                    old_register_32_value
    1620                    old_register_33_value
    1621                    old_register_34_value
    1622                    old_register_35_value
    1623                    old_register_36_value
    1624                    old_register_37_value
    1625                    old_register_A_value
    1626                    old_register_B_value
    1627                    old_register_DPL_value
    1628                    old_register_DPH_value
    1629                    old_register_Carry_value.
    1630 
    1631 definition update_register_21: Byte → RegisterMap → RegisterMap ≝
    1632   λb: Byte.
    1633   λm: RegisterMap.
    1634   let old_register_00_value ≝ register_00_value m in
    1635   let old_register_01_value ≝ register_01_value m in
    1636   let old_register_02_value ≝ register_02_value m in
    1637   let old_register_03_value ≝ register_03_value m in
    1638   let old_register_04_value ≝ register_04_value m in
    1639   let old_register_05_value ≝ register_05_value m in
    1640   let old_register_06_value ≝ register_06_value m in
    1641   let old_register_07_value ≝ register_07_value m in
    1642   let old_register_10_value ≝ register_01_value m in
    1643   let old_register_11_value ≝ register_01_value m in
    1644   let old_register_12_value ≝ register_02_value m in
    1645   let old_register_13_value ≝ register_03_value m in
    1646   let old_register_14_value ≝ register_04_value m in
    1647   let old_register_15_value ≝ register_05_value m in
    1648   let old_register_16_value ≝ register_06_value m in
    1649   let old_register_17_value ≝ register_07_value m in
    1650   let old_register_20_value ≝ register_01_value m in
    1651   let old_register_21_value ≝ register_02_value m in
    1652   let old_register_22_value ≝ register_02_value m in
    1653   let old_register_23_value ≝ register_03_value m in
    1654   let old_register_24_value ≝ register_04_value m in
    1655   let old_register_25_value ≝ register_05_value m in
    1656   let old_register_26_value ≝ register_06_value m in
    1657   let old_register_27_value ≝ register_07_value m in
    1658   let old_register_30_value ≝ register_01_value m in
    1659   let old_register_31_value ≝ register_02_value m in
    1660   let old_register_32_value ≝ register_02_value m in
    1661   let old_register_33_value ≝ register_03_value m in
    1662   let old_register_34_value ≝ register_04_value m in
    1663   let old_register_35_value ≝ register_05_value m in
    1664   let old_register_36_value ≝ register_06_value m in
    1665   let old_register_37_value ≝ register_07_value m in
    1666   let old_register_A_value ≝ register_A_value m in
    1667   let old_register_B_value ≝ register_B_value m in
    1668   let old_register_DPL_value ≝ register_DPL_value m in
    1669   let old_register_DPH_value ≝ register_DPH_value m in
    1670   let old_register_Carry_value ≝ register_Carry_value m in
    1671     mk_RegisterMap old_register_00_value
    1672                    old_register_01_value
    1673                    old_register_02_value
    1674                    old_register_03_value
    1675                    old_register_04_value
    1676                    old_register_05_value
    1677                    old_register_06_value
    1678                    old_register_07_value
    1679                    old_register_10_value
    1680                    old_register_11_value
    1681                    old_register_12_value
    1682                    old_register_13_value
    1683                    old_register_14_value
    1684                    old_register_15_value
    1685                    old_register_16_value
    1686                    old_register_17_value
    1687                    old_register_20_value
    1688                    (Some ? b)
    1689                    old_register_22_value
    1690                    old_register_23_value
    1691                    old_register_24_value
    1692                    old_register_25_value
    1693                    old_register_26_value
    1694                    old_register_27_value
    1695                    old_register_30_value
    1696                    old_register_31_value
    1697                    old_register_32_value
    1698                    old_register_33_value
    1699                    old_register_34_value
    1700                    old_register_35_value
    1701                    old_register_36_value
    1702                    old_register_37_value
    1703                    old_register_A_value
    1704                    old_register_B_value
    1705                    old_register_DPL_value
    1706                    old_register_DPH_value
    1707                    old_register_Carry_value.
    1708 
    1709 definition update_register_22: Byte → RegisterMap → RegisterMap ≝
    1710   λb: Byte.
    1711   λm: RegisterMap.
    1712   let old_register_00_value ≝ register_00_value m in
    1713   let old_register_01_value ≝ register_01_value m in
    1714   let old_register_02_value ≝ register_02_value m in
    1715   let old_register_03_value ≝ register_03_value m in
    1716   let old_register_04_value ≝ register_04_value m in
    1717   let old_register_05_value ≝ register_05_value m in
    1718   let old_register_06_value ≝ register_06_value m in
    1719   let old_register_07_value ≝ register_07_value m in
    1720   let old_register_10_value ≝ register_01_value m in
    1721   let old_register_11_value ≝ register_01_value m in
    1722   let old_register_12_value ≝ register_02_value m in
    1723   let old_register_13_value ≝ register_03_value m in
    1724   let old_register_14_value ≝ register_04_value m in
    1725   let old_register_15_value ≝ register_05_value m in
    1726   let old_register_16_value ≝ register_06_value m in
    1727   let old_register_17_value ≝ register_07_value m in
    1728   let old_register_20_value ≝ register_01_value m in
    1729   let old_register_21_value ≝ register_02_value m in
    1730   let old_register_22_value ≝ register_02_value m in
    1731   let old_register_23_value ≝ register_03_value m in
    1732   let old_register_24_value ≝ register_04_value m in
    1733   let old_register_25_value ≝ register_05_value m in
    1734   let old_register_26_value ≝ register_06_value m in
    1735   let old_register_27_value ≝ register_07_value m in
    1736   let old_register_30_value ≝ register_01_value m in
    1737   let old_register_31_value ≝ register_02_value m in
    1738   let old_register_32_value ≝ register_02_value m in
    1739   let old_register_33_value ≝ register_03_value m in
    1740   let old_register_34_value ≝ register_04_value m in
    1741   let old_register_35_value ≝ register_05_value m in
    1742   let old_register_36_value ≝ register_06_value m in
    1743   let old_register_37_value ≝ register_07_value m in
    1744   let old_register_A_value ≝ register_A_value m in
    1745   let old_register_B_value ≝ register_B_value m in
    1746   let old_register_DPL_value ≝ register_DPL_value m in
    1747   let old_register_DPH_value ≝ register_DPH_value m in
    1748   let old_register_Carry_value ≝ register_Carry_value m in
    1749     mk_RegisterMap old_register_00_value
    1750                    old_register_01_value
    1751                    old_register_02_value
    1752                    old_register_03_value
    1753                    old_register_04_value
    1754                    old_register_05_value
    1755                    old_register_06_value
    1756                    old_register_07_value
    1757                    old_register_10_value
    1758                    old_register_11_value
    1759                    old_register_12_value
    1760                    old_register_13_value
    1761                    old_register_14_value
    1762                    old_register_15_value
    1763                    old_register_16_value
    1764                    old_register_17_value
    1765                    old_register_20_value
    1766                    old_register_21_value
    1767                    (Some ? b)
    1768                    old_register_23_value
    1769                    old_register_24_value
    1770                    old_register_25_value
    1771                    old_register_26_value
    1772                    old_register_27_value
    1773                    old_register_30_value
    1774                    old_register_31_value
    1775                    old_register_32_value
    1776                    old_register_33_value
    1777                    old_register_34_value
    1778                    old_register_35_value
    1779                    old_register_36_value
    1780                    old_register_37_value
    1781                    old_register_A_value
    1782                    old_register_B_value
    1783                    old_register_DPL_value
    1784                    old_register_DPH_value
    1785                    old_register_Carry_value.
    1786                    
    1787 definition update_register_23: Byte → RegisterMap → RegisterMap ≝
    1788   λb: Byte.
    1789   λm: RegisterMap.
    1790   let old_register_00_value ≝ register_00_value m in
    1791   let old_register_01_value ≝ register_01_value m in
    1792   let old_register_02_value ≝ register_02_value m in
    1793   let old_register_03_value ≝ register_03_value m in
    1794   let old_register_04_value ≝ register_04_value m in
    1795   let old_register_05_value ≝ register_05_value m in
    1796   let old_register_06_value ≝ register_06_value m in
    1797   let old_register_07_value ≝ register_07_value m in
    1798   let old_register_10_value ≝ register_01_value m in
    1799   let old_register_11_value ≝ register_01_value m in
    1800   let old_register_12_value ≝ register_02_value m in
    1801   let old_register_13_value ≝ register_03_value m in
    1802   let old_register_14_value ≝ register_04_value m in
    1803   let old_register_15_value ≝ register_05_value m in
    1804   let old_register_16_value ≝ register_06_value m in
    1805   let old_register_17_value ≝ register_07_value m in
    1806   let old_register_20_value ≝ register_01_value m in
    1807   let old_register_21_value ≝ register_02_value m in
    1808   let old_register_22_value ≝ register_02_value m in
    1809   let old_register_23_value ≝ register_03_value m in
    1810   let old_register_24_value ≝ register_04_value m in
    1811   let old_register_25_value ≝ register_05_value m in
    1812   let old_register_26_value ≝ register_06_value m in
    1813   let old_register_27_value ≝ register_07_value m in
    1814   let old_register_30_value ≝ register_01_value m in
    1815   let old_register_31_value ≝ register_02_value m in
    1816   let old_register_32_value ≝ register_02_value m in
    1817   let old_register_33_value ≝ register_03_value m in
    1818   let old_register_34_value ≝ register_04_value m in
    1819   let old_register_35_value ≝ register_05_value m in
    1820   let old_register_36_value ≝ register_06_value m in
    1821   let old_register_37_value ≝ register_07_value m in
    1822   let old_register_A_value ≝ register_A_value m in
    1823   let old_register_B_value ≝ register_B_value m in
    1824   let old_register_DPL_value ≝ register_DPL_value m in
    1825   let old_register_DPH_value ≝ register_DPH_value m in
    1826   let old_register_Carry_value ≝ register_Carry_value m in
    1827     mk_RegisterMap old_register_00_value
    1828                    old_register_01_value
    1829                    old_register_02_value
    1830                    old_register_03_value
    1831                    old_register_04_value
    1832                    old_register_05_value
    1833                    old_register_06_value
    1834                    old_register_07_value
    1835                    old_register_10_value
    1836                    old_register_11_value
    1837                    old_register_12_value
    1838                    old_register_13_value
    1839                    old_register_14_value
    1840                    old_register_15_value
    1841                    old_register_16_value
    1842                    old_register_17_value
    1843                    old_register_20_value
    1844                    old_register_21_value
    1845                    old_register_22_value
    1846                    (Some ? b)
    1847                    old_register_24_value
    1848                    old_register_25_value
    1849                    old_register_26_value
    1850                    old_register_27_value
    1851                    old_register_30_value
    1852                    old_register_31_value
    1853                    old_register_32_value
    1854                    old_register_33_value
    1855                    old_register_34_value
    1856                    old_register_35_value
    1857                    old_register_36_value
    1858                    old_register_37_value
    1859                    old_register_A_value
    1860                    old_register_B_value
    1861                    old_register_DPL_value
    1862                    old_register_DPH_value
    1863                    old_register_Carry_value.
    1864                    
    1865 definition update_register_24: Byte → RegisterMap → RegisterMap ≝
    1866   λb: Byte.
    1867   λm: RegisterMap.
    1868   let old_register_00_value ≝ register_00_value m in
    1869   let old_register_01_value ≝ register_01_value m in
    1870   let old_register_02_value ≝ register_02_value m in
    1871   let old_register_03_value ≝ register_03_value m in
    1872   let old_register_04_value ≝ register_04_value m in
    1873   let old_register_05_value ≝ register_05_value m in
    1874   let old_register_06_value ≝ register_06_value m in
    1875   let old_register_07_value ≝ register_07_value m in
    1876   let old_register_10_value ≝ register_01_value m in
    1877   let old_register_11_value ≝ register_01_value m in
    1878   let old_register_12_value ≝ register_02_value m in
    1879   let old_register_13_value ≝ register_03_value m in
    1880   let old_register_14_value ≝ register_04_value m in
    1881   let old_register_15_value ≝ register_05_value m in
    1882   let old_register_16_value ≝ register_06_value m in
    1883   let old_register_17_value ≝ register_07_value m in
    1884   let old_register_20_value ≝ register_01_value m in
    1885   let old_register_21_value ≝ register_02_value m in
    1886   let old_register_22_value ≝ register_02_value m in
    1887   let old_register_23_value ≝ register_03_value m in
    1888   let old_register_24_value ≝ register_04_value m in
    1889   let old_register_25_value ≝ register_05_value m in
    1890   let old_register_26_value ≝ register_06_value m in
    1891   let old_register_27_value ≝ register_07_value m in
    1892   let old_register_30_value ≝ register_01_value m in
    1893   let old_register_31_value ≝ register_02_value m in
    1894   let old_register_32_value ≝ register_02_value m in
    1895   let old_register_33_value ≝ register_03_value m in
    1896   let old_register_34_value ≝ register_04_value m in
    1897   let old_register_35_value ≝ register_05_value m in
    1898   let old_register_36_value ≝ register_06_value m in
    1899   let old_register_37_value ≝ register_07_value m in
    1900   let old_register_A_value ≝ register_A_value m in
    1901   let old_register_B_value ≝ register_B_value m in
    1902   let old_register_DPL_value ≝ register_DPL_value m in
    1903   let old_register_DPH_value ≝ register_DPH_value m in
    1904   let old_register_Carry_value ≝ register_Carry_value m in
    1905     mk_RegisterMap old_register_00_value
    1906                    old_register_01_value
    1907                    old_register_02_value
    1908                    old_register_03_value
    1909                    old_register_04_value
    1910                    old_register_05_value
    1911                    old_register_06_value
    1912                    old_register_07_value
    1913                    old_register_10_value
    1914                    old_register_11_value
    1915                    old_register_12_value
    1916                    old_register_13_value
    1917                    old_register_14_value
    1918                    old_register_15_value
    1919                    old_register_16_value
    1920                    old_register_17_value
    1921                    old_register_20_value
    1922                    old_register_21_value
    1923                    old_register_22_value
    1924                    old_register_23_value
    1925                    (Some ? b)
    1926                    old_register_25_value
    1927                    old_register_26_value
    1928                    old_register_27_value
    1929                    old_register_30_value
    1930                    old_register_31_value
    1931                    old_register_32_value
    1932                    old_register_33_value
    1933                    old_register_34_value
    1934                    old_register_35_value
    1935                    old_register_36_value
    1936                    old_register_37_value
    1937                    old_register_A_value
    1938                    old_register_B_value
    1939                    old_register_DPL_value
    1940                    old_register_DPH_value
    1941                    old_register_Carry_value.
    1942 
    1943 definition update_register_25: Byte → RegisterMap → RegisterMap ≝
    1944   λb: Byte.
    1945   λm: RegisterMap.
    1946   let old_register_00_value ≝ register_00_value m in
    1947   let old_register_01_value ≝ register_01_value m in
    1948   let old_register_02_value ≝ register_02_value m in
    1949   let old_register_03_value ≝ register_03_value m in
    1950   let old_register_04_value ≝ register_04_value m in
    1951   let old_register_05_value ≝ register_05_value m in
    1952   let old_register_06_value ≝ register_06_value m in
    1953   let old_register_07_value ≝ register_07_value m in
    1954   let old_register_10_value ≝ register_01_value m in
    1955   let old_register_11_value ≝ register_01_value m in
    1956   let old_register_12_value ≝ register_02_value m in
    1957   let old_register_13_value ≝ register_03_value m in
    1958   let old_register_14_value ≝ register_04_value m in
    1959   let old_register_15_value ≝ register_05_value m in
    1960   let old_register_16_value ≝ register_06_value m in
    1961   let old_register_17_value ≝ register_07_value m in
    1962   let old_register_20_value ≝ register_01_value m in
    1963   let old_register_21_value ≝ register_02_value m in
    1964   let old_register_22_value ≝ register_02_value m in
    1965   let old_register_23_value ≝ register_03_value m in
    1966   let old_register_24_value ≝ register_04_value m in
    1967   let old_register_25_value ≝ register_05_value m in
    1968   let old_register_26_value ≝ register_06_value m in
    1969   let old_register_27_value ≝ register_07_value m in
    1970   let old_register_30_value ≝ register_01_value m in
    1971   let old_register_31_value ≝ register_02_value m in
    1972   let old_register_32_value ≝ register_02_value m in
    1973   let old_register_33_value ≝ register_03_value m in
    1974   let old_register_34_value ≝ register_04_value m in
    1975   let old_register_35_value ≝ register_05_value m in
    1976   let old_register_36_value ≝ register_06_value m in
    1977   let old_register_37_value ≝ register_07_value m in
    1978   let old_register_A_value ≝ register_A_value m in
    1979   let old_register_B_value ≝ register_B_value m in
    1980   let old_register_DPL_value ≝ register_DPL_value m in
    1981   let old_register_DPH_value ≝ register_DPH_value m in
    1982   let old_register_Carry_value ≝ register_Carry_value m in
    1983     mk_RegisterMap old_register_00_value
    1984                    old_register_01_value
    1985                    old_register_02_value
    1986                    old_register_03_value
    1987                    old_register_04_value
    1988                    old_register_05_value
    1989                    old_register_06_value
    1990                    old_register_07_value
    1991                    old_register_10_value
    1992                    old_register_11_value
    1993                    old_register_12_value
    1994                    old_register_13_value
    1995                    old_register_14_value
    1996                    old_register_15_value
    1997                    old_register_16_value
    1998                    old_register_17_value
    1999                    old_register_20_value
    2000                    old_register_21_value
    2001                    old_register_22_value
    2002                    old_register_23_value
    2003                    old_register_24_value
    2004                    (Some ? b)
    2005                    old_register_26_value
    2006                    old_register_27_value
    2007                    old_register_30_value
    2008                    old_register_31_value
    2009                    old_register_32_value
    2010                    old_register_33_value
    2011                    old_register_34_value
    2012                    old_register_35_value
    2013                    old_register_36_value
    2014                    old_register_37_value
    2015                    old_register_A_value
    2016                    old_register_B_value
    2017                    old_register_DPL_value
    2018                    old_register_DPH_value
    2019                    old_register_Carry_value.
    2020 
    2021 definition update_register_26: Byte → RegisterMap → RegisterMap ≝
    2022   λb: Byte.
    2023   λm: RegisterMap.
    2024   let old_register_00_value ≝ register_00_value m in
    2025   let old_register_01_value ≝ register_01_value m in
    2026   let old_register_02_value ≝ register_02_value m in
    2027   let old_register_03_value ≝ register_03_value m in
    2028   let old_register_04_value ≝ register_04_value m in
    2029   let old_register_05_value ≝ register_05_value m in
    2030   let old_register_06_value ≝ register_06_value m in
    2031   let old_register_07_value ≝ register_07_value m in
    2032   let old_register_10_value ≝ register_01_value m in
    2033   let old_register_11_value ≝ register_01_value m in
    2034   let old_register_12_value ≝ register_02_value m in
    2035   let old_register_13_value ≝ register_03_value m in
    2036   let old_register_14_value ≝ register_04_value m in
    2037   let old_register_15_value ≝ register_05_value m in
    2038   let old_register_16_value ≝ register_06_value m in
    2039   let old_register_17_value ≝ register_07_value m in
    2040   let old_register_20_value ≝ register_01_value m in
    2041   let old_register_21_value ≝ register_02_value m in
    2042   let old_register_22_value ≝ register_02_value m in
    2043   let old_register_23_value ≝ register_03_value m in
    2044   let old_register_24_value ≝ register_04_value m in
    2045   let old_register_25_value ≝ register_05_value m in
    2046   let old_register_26_value ≝ register_06_value m in
    2047   let old_register_27_value ≝ register_07_value m in
    2048   let old_register_30_value ≝ register_01_value m in
    2049   let old_register_31_value ≝ register_02_value m in
    2050   let old_register_32_value ≝ register_02_value m in
    2051   let old_register_33_value ≝ register_03_value m in
    2052   let old_register_34_value ≝ register_04_value m in
    2053   let old_register_35_value ≝ register_05_value m in
    2054   let old_register_36_value ≝ register_06_value m in
    2055   let old_register_37_value ≝ register_07_value m in
    2056   let old_register_A_value ≝ register_A_value m in
    2057   let old_register_B_value ≝ register_B_value m in
    2058   let old_register_DPL_value ≝ register_DPL_value m in
    2059   let old_register_DPH_value ≝ register_DPH_value m in
    2060   let old_register_Carry_value ≝ register_Carry_value m in
    2061     mk_RegisterMap old_register_00_value
    2062                    old_register_01_value
    2063                    old_register_02_value
    2064                    old_register_03_value
    2065                    old_register_04_value
    2066                    old_register_05_value
    2067                    old_register_06_value
    2068                    old_register_07_value
    2069                    old_register_10_value
    2070                    old_register_11_value
    2071                    old_register_12_value
    2072                    old_register_13_value
    2073                    old_register_14_value
    2074                    old_register_15_value
    2075                    old_register_16_value
    2076                    old_register_17_value
    2077                    old_register_20_value
    2078                    old_register_21_value
    2079                    old_register_22_value
    2080                    old_register_23_value
    2081                    old_register_24_value
    2082                    old_register_25_value
    2083                    (Some ? b)
    2084                    old_register_27_value
    2085                    old_register_30_value
    2086                    old_register_31_value
    2087                    old_register_32_value
    2088                    old_register_33_value
    2089                    old_register_34_value
    2090                    old_register_35_value
    2091                    old_register_36_value
    2092                    old_register_37_value
    2093                    old_register_A_value
    2094                    old_register_B_value
    2095                    old_register_DPL_value
    2096                    old_register_DPH_value
    2097                    old_register_Carry_value.
    2098 
    2099 definition update_register_27: Byte → RegisterMap → RegisterMap ≝
    2100   λb: Byte.
    2101   λm: RegisterMap.
    2102   let old_register_00_value ≝ register_00_value m in
    2103   let old_register_01_value ≝ register_01_value m in
    2104   let old_register_02_value ≝ register_02_value m in
    2105   let old_register_03_value ≝ register_03_value m in
    2106   let old_register_04_value ≝ register_04_value m in
    2107   let old_register_05_value ≝ register_05_value m in
    2108   let old_register_06_value ≝ register_06_value m in
    2109   let old_register_07_value ≝ register_07_value m in
    2110   let old_register_10_value ≝ register_01_value m in
    2111   let old_register_11_value ≝ register_01_value m in
    2112   let old_register_12_value ≝ register_02_value m in
    2113   let old_register_13_value ≝ register_03_value m in
    2114   let old_register_14_value ≝ register_04_value m in
    2115   let old_register_15_value ≝ register_05_value m in
    2116   let old_register_16_value ≝ register_06_value m in
    2117   let old_register_17_value ≝ register_07_value m in
    2118   let old_register_20_value ≝ register_01_value m in
    2119   let old_register_21_value ≝ register_02_value m in
    2120   let old_register_22_value ≝ register_02_value m in
    2121   let old_register_23_value ≝ register_03_value m in
    2122   let old_register_24_value ≝ register_04_value m in
    2123   let old_register_25_value ≝ register_05_value m in
    2124   let old_register_26_value ≝ register_06_value m in
    2125   let old_register_27_value ≝ register_07_value m in
    2126   let old_register_30_value ≝ register_01_value m in
    2127   let old_register_31_value ≝ register_02_value m in
    2128   let old_register_32_value ≝ register_02_value m in
    2129   let old_register_33_value ≝ register_03_value m in
    2130   let old_register_34_value ≝ register_04_value m in
    2131   let old_register_35_value ≝ register_05_value m in
    2132   let old_register_36_value ≝ register_06_value m in
    2133   let old_register_37_value ≝ register_07_value m in
    2134   let old_register_A_value ≝ register_A_value m in
    2135   let old_register_B_value ≝ register_B_value m in
    2136   let old_register_DPL_value ≝ register_DPL_value m in
    2137   let old_register_DPH_value ≝ register_DPH_value m in
    2138   let old_register_Carry_value ≝ register_Carry_value m in
    2139     mk_RegisterMap old_register_00_value
    2140                    old_register_01_value
    2141                    old_register_02_value
    2142                    old_register_03_value
    2143                    old_register_04_value
    2144                    old_register_05_value
    2145                    old_register_06_value
    2146                    old_register_07_value
    2147                    old_register_10_value
    2148                    old_register_11_value
    2149                    old_register_12_value
    2150                    old_register_13_value
    2151                    old_register_14_value
    2152                    old_register_15_value
    2153                    old_register_16_value
    2154                    old_register_17_value
    2155                    old_register_20_value
    2156                    old_register_21_value
    2157                    old_register_22_value
    2158                    old_register_23_value
    2159                    old_register_24_value
    2160                    old_register_25_value
    2161                    old_register_26_value
    2162                    (Some ? b)
    2163                    old_register_30_value
    2164                    old_register_31_value
    2165                    old_register_32_value
    2166                    old_register_33_value
    2167                    old_register_34_value
    2168                    old_register_35_value
    2169                    old_register_36_value
    2170                    old_register_37_value
    2171                    old_register_A_value
    2172                    old_register_B_value
    2173                    old_register_DPL_value
    2174                    old_register_DPH_value
    2175                    old_register_Carry_value.
    2176 
    2177 definition update_register_30: Byte → RegisterMap → RegisterMap ≝
    2178   λb: Byte.
    2179   λm: RegisterMap.
    2180   let old_register_00_value ≝ register_00_value m in
    2181   let old_register_01_value ≝ register_01_value m in
    2182   let old_register_02_value ≝ register_02_value m in
    2183   let old_register_03_value ≝ register_03_value m in
    2184   let old_register_04_value ≝ register_04_value m in
    2185   let old_register_05_value ≝ register_05_value m in
    2186   let old_register_06_value ≝ register_06_value m in
    2187   let old_register_07_value ≝ register_07_value m in
    2188   let old_register_10_value ≝ register_01_value m in
    2189   let old_register_11_value ≝ register_01_value m in
    2190   let old_register_12_value ≝ register_02_value m in
    2191   let old_register_13_value ≝ register_03_value m in
    2192   let old_register_14_value ≝ register_04_value m in
    2193   let old_register_15_value ≝ register_05_value m in
    2194   let old_register_16_value ≝ register_06_value m in
    2195   let old_register_17_value ≝ register_07_value m in
    2196   let old_register_20_value ≝ register_01_value m in
    2197   let old_register_21_value ≝ register_02_value m in
    2198   let old_register_22_value ≝ register_02_value m in
    2199   let old_register_23_value ≝ register_03_value m in
    2200   let old_register_24_value ≝ register_04_value m in
    2201   let old_register_25_value ≝ register_05_value m in
    2202   let old_register_26_value ≝ register_06_value m in
    2203   let old_register_27_value ≝ register_07_value m in
    2204   let old_register_30_value ≝ register_01_value m in
    2205   let old_register_31_value ≝ register_02_value m in
    2206   let old_register_32_value ≝ register_02_value m in
    2207   let old_register_33_value ≝ register_03_value m in
    2208   let old_register_34_value ≝ register_04_value m in
    2209   let old_register_35_value ≝ register_05_value m in
    2210   let old_register_36_value ≝ register_06_value m in
    2211   let old_register_37_value ≝ register_07_value m in
    2212   let old_register_A_value ≝ register_A_value m in
    2213   let old_register_B_value ≝ register_B_value m in
    2214   let old_register_DPL_value ≝ register_DPL_value m in
    2215   let old_register_DPH_value ≝ register_DPH_value m in
    2216   let old_register_Carry_value ≝ register_Carry_value m in
    2217     mk_RegisterMap old_register_00_value
    2218                    old_register_01_value
    2219                    old_register_02_value
    2220                    old_register_03_value
    2221                    old_register_04_value
    2222                    old_register_05_value
    2223                    old_register_06_value
    2224                    old_register_07_value
    2225                    old_register_10_value
    2226                    old_register_11_value
    2227                    old_register_12_value
    2228                    old_register_13_value
    2229                    old_register_14_value
    2230                    old_register_15_value
    2231                    old_register_16_value
    2232                    old_register_17_value
    2233                    old_register_20_value
    2234                    old_register_21_value
    2235                    old_register_22_value
    2236                    old_register_23_value
    2237                    old_register_24_value
    2238                    old_register_25_value
    2239                    old_register_26_value
    2240                    old_register_27_value
    2241                    (Some ? b)
    2242                    old_register_31_value
    2243                    old_register_32_value
    2244                    old_register_33_value
    2245                    old_register_34_value
    2246                    old_register_35_value
    2247                    old_register_36_value
    2248                    old_register_37_value
    2249                    old_register_A_value
    2250                    old_register_B_value
    2251                    old_register_DPL_value
    2252                    old_register_DPH_value
    2253                    old_register_Carry_value.
    2254 
    2255 definition update_register_31: Byte → RegisterMap → RegisterMap ≝
    2256   λb: Byte.
    2257   λm: RegisterMap.
    2258   let old_register_00_value ≝ register_00_value m in
    2259   let old_register_01_value ≝ register_01_value m in
    2260   let old_register_02_value ≝ register_02_value m in
    2261   let old_register_03_value ≝ register_03_value m in
    2262   let old_register_04_value ≝ register_04_value m in
    2263   let old_register_05_value ≝ register_05_value m in
    2264   let old_register_06_value ≝ register_06_value m in
    2265   let old_register_07_value ≝ register_07_value m in
    2266   let old_register_10_value ≝ register_01_value m in
    2267   let old_register_11_value ≝ register_01_value m in
    2268   let old_register_12_value ≝ register_02_value m in
    2269   let old_register_13_value ≝ register_03_value m in
    2270   let old_register_14_value ≝ register_04_value m in
    2271   let old_register_15_value ≝ register_05_value m in
    2272   let old_register_16_value ≝ register_06_value m in
    2273   let old_register_17_value ≝ register_07_value m in
    2274   let old_register_20_value ≝ register_01_value m in
    2275   let old_register_21_value ≝ register_02_value m in
    2276   let old_register_22_value ≝ register_02_value m in
    2277   let old_register_23_value ≝ register_03_value m in
    2278   let old_register_24_value ≝ register_04_value m in
    2279   let old_register_25_value ≝ register_05_value m in
    2280   let old_register_26_value ≝ register_06_value m in
    2281   let old_register_27_value ≝ register_07_value m in
    2282   let old_register_30_value ≝ register_01_value m in
    2283   let old_register_31_value ≝ register_02_value m in
    2284   let old_register_32_value ≝ register_02_value m in
    2285   let old_register_33_value ≝ register_03_value m in
    2286   let old_register_34_value ≝ register_04_value m in
    2287   let old_register_35_value ≝ register_05_value m in
    2288   let old_register_36_value ≝ register_06_value m in
    2289   let old_register_37_value ≝ register_07_value m in
    2290   let old_register_A_value ≝ register_A_value m in
    2291   let old_register_B_value ≝ register_B_value m in
    2292   let old_register_DPL_value ≝ register_DPL_value m in
    2293   let old_register_DPH_value ≝ register_DPH_value m in
    2294   let old_register_Carry_value ≝ register_Carry_value m in
    2295     mk_RegisterMap old_register_00_value
    2296                    old_register_01_value
    2297                    old_register_02_value
    2298                    old_register_03_value
    2299                    old_register_04_value
    2300                    old_register_05_value
    2301                    old_register_06_value
    2302                    old_register_07_value
    2303                    old_register_10_value
    2304                    old_register_11_value
    2305                    old_register_12_value
    2306                    old_register_13_value
    2307                    old_register_14_value
    2308                    old_register_15_value
    2309                    old_register_16_value
    2310                    old_register_17_value
    2311                    old_register_20_value
    2312                    old_register_21_value
    2313                    old_register_22_value
    2314                    old_register_23_value
    2315                    old_register_24_value
    2316                    old_register_25_value
    2317                    old_register_26_value
    2318                    old_register_27_value
    2319                    old_register_30_value
    2320                    (Some ? b)
    2321                    old_register_32_value
    2322                    old_register_33_value
    2323                    old_register_34_value
    2324                    old_register_35_value
    2325                    old_register_36_value
    2326                    old_register_37_value
    2327                    old_register_A_value
    2328                    old_register_B_value
    2329                    old_register_DPL_value
    2330                    old_register_DPH_value
    2331                    old_register_Carry_value.
    2332 
    2333 definition update_register_32: Byte → RegisterMap → RegisterMap ≝
    2334   λb: Byte.
    2335   λm: RegisterMap.
    2336   let old_register_00_value ≝ register_00_value m in
    2337   let old_register_01_value ≝ register_01_value m in
    2338   let old_register_02_value ≝ register_02_value m in
    2339   let old_register_03_value ≝ register_03_value m in
    2340   let old_register_04_value ≝ register_04_value m in
    2341   let old_register_05_value ≝ register_05_value m in
    2342   let old_register_06_value ≝ register_06_value m in
    2343   let old_register_07_value ≝ register_07_value m in
    2344   let old_register_10_value ≝ register_01_value m in
    2345   let old_register_11_value ≝ register_01_value m in
    2346   let old_register_12_value ≝ register_02_value m in
    2347   let old_register_13_value ≝ register_03_value m in
    2348   let old_register_14_value ≝ register_04_value m in
    2349   let old_register_15_value ≝ register_05_value m in
    2350   let old_register_16_value ≝ register_06_value m in
    2351   let old_register_17_value ≝ register_07_value m in
    2352   let old_register_20_value ≝ register_01_value m in
    2353   let old_register_21_value ≝ register_02_value m in
    2354   let old_register_22_value ≝ register_02_value m in
    2355   let old_register_23_value ≝ register_03_value m in
    2356   let old_register_24_value ≝ register_04_value m in
    2357   let old_register_25_value ≝ register_05_value m in
    2358   let old_register_26_value ≝ register_06_value m in
    2359   let old_register_27_value ≝ register_07_value m in
    2360   let old_register_30_value ≝ register_01_value m in
    2361   let old_register_31_value ≝ register_02_value m in
    2362   let old_register_32_value ≝ register_02_value m in
    2363   let old_register_33_value ≝ register_03_value m in
    2364   let old_register_34_value ≝ register_04_value m in
    2365   let old_register_35_value ≝ register_05_value m in
    2366   let old_register_36_value ≝ register_06_value m in
    2367   let old_register_37_value ≝ register_07_value m in
    2368   let old_register_A_value ≝ register_A_value m in
    2369   let old_register_B_value ≝ register_B_value m in
    2370   let old_register_DPL_value ≝ register_DPL_value m in
    2371   let old_register_DPH_value ≝ register_DPH_value m in
    2372   let old_register_Carry_value ≝ register_Carry_value m in
    2373     mk_RegisterMap old_register_00_value
    2374                    old_register_01_value
    2375                    old_register_02_value
    2376                    old_register_03_value
    2377                    old_register_04_value
    2378                    old_register_05_value
    2379                    old_register_06_value
    2380                    old_register_07_value
    2381                    old_register_10_value
    2382                    old_register_11_value
    2383                    old_register_12_value
    2384                    old_register_13_value
    2385                    old_register_14_value
    2386                    old_register_15_value
    2387                    old_register_16_value
    2388                    old_register_17_value
    2389                    old_register_20_value
    2390                    old_register_21_value
    2391                    old_register_22_value
    2392                    old_register_23_value
    2393                    old_register_24_value
    2394                    old_register_25_value
    2395                    old_register_26_value
    2396                    old_register_27_value
    2397                    old_register_30_value
    2398                    old_register_31_value
    2399                    (Some ? b)
    2400                    old_register_33_value
    2401                    old_register_34_value
    2402                    old_register_35_value
    2403                    old_register_36_value
    2404                    old_register_37_value
    2405                    old_register_A_value
    2406                    old_register_B_value
    2407                    old_register_DPL_value
    2408                    old_register_DPH_value
    2409                    old_register_Carry_value.
    2410 
    2411 definition update_register_33: Byte → RegisterMap → RegisterMap ≝
    2412   λb: Byte.
    2413   λm: RegisterMap.
    2414   let old_register_00_value ≝ register_00_value m in
    2415   let old_register_01_value ≝ register_01_value m in
    2416   let old_register_02_value ≝ register_02_value m in
    2417   let old_register_03_value ≝ register_03_value m in
    2418   let old_register_04_value ≝ register_04_value m in
    2419   let old_register_05_value ≝ register_05_value m in
    2420   let old_register_06_value ≝ register_06_value m in
    2421   let old_register_07_value ≝ register_07_value m in
    2422   let old_register_10_value ≝ register_01_value m in
    2423   let old_register_11_value ≝ register_01_value m in
    2424   let old_register_12_value ≝ register_02_value m in
    2425   let old_register_13_value ≝ register_03_value m in
    2426   let old_register_14_value ≝ register_04_value m in
    2427   let old_register_15_value ≝ register_05_value m in
    2428   let old_register_16_value ≝ register_06_value m in
    2429   let old_register_17_value ≝ register_07_value m in
    2430   let old_register_20_value ≝ register_01_value m in
    2431   let old_register_21_value ≝ register_02_value m in
    2432   let old_register_22_value ≝ register_02_value m in
    2433   let old_register_23_value ≝ register_03_value m in
    2434   let old_register_24_value ≝ register_04_value m in
    2435   let old_register_25_value ≝ register_05_value m in
    2436   let old_register_26_value ≝ register_06_value m in
    2437   let old_register_27_value ≝ register_07_value m in
    2438   let old_register_30_value ≝ register_01_value m in
    2439   let old_register_31_value ≝ register_02_value m in
    2440   let old_register_32_value ≝ register_02_value m in
    2441   let old_register_33_value ≝ register_03_value m in
    2442   let old_register_34_value ≝ register_04_value m in
    2443   let old_register_35_value ≝ register_05_value m in
    2444   let old_register_36_value ≝ register_06_value m in
    2445   let old_register_37_value ≝ register_07_value m in
    2446   let old_register_A_value ≝ register_A_value m in
    2447   let old_register_B_value ≝ register_B_value m in
    2448   let old_register_DPL_value ≝ register_DPL_value m in
    2449   let old_register_DPH_value ≝ register_DPH_value m in
    2450   let old_register_Carry_value ≝ register_Carry_value m in
    2451     mk_RegisterMap old_register_00_value
    2452                    old_register_01_value
    2453                    old_register_02_value
    2454                    old_register_03_value
    2455                    old_register_04_value
    2456                    old_register_05_value
    2457                    old_register_06_value
    2458                    old_register_07_value
    2459                    old_register_10_value
    2460                    old_register_11_value
    2461                    old_register_12_value
    2462                    old_register_13_value
    2463                    old_register_14_value
    2464                    old_register_15_value
    2465                    old_register_16_value
    2466                    old_register_17_value
    2467                    old_register_20_value
    2468                    old_register_21_value
    2469                    old_register_22_value
    2470                    old_register_23_value
    2471                    old_register_24_value
    2472                    old_register_25_value
    2473                    old_register_26_value
    2474                    old_register_27_value
    2475                    old_register_30_value
    2476                    old_register_31_value
    2477                    old_register_32_value
    2478                    (Some ? b)
    2479                    old_register_34_value
    2480                    old_register_35_value
    2481                    old_register_36_value
    2482                    old_register_37_value
    2483                    old_register_A_value
    2484                    old_register_B_value
    2485                    old_register_DPL_value
    2486                    old_register_DPH_value
    2487                    old_register_Carry_value.
    2488 
    2489 definition update_register_34: Byte → RegisterMap → RegisterMap ≝
    2490   λb: Byte.
    2491   λm: RegisterMap.
    2492   let old_register_00_value ≝ register_00_value m in
    2493   let old_register_01_value ≝ register_01_value m in
    2494   let old_register_02_value ≝ register_02_value m in
    2495   let old_register_03_value ≝ register_03_value m in
    2496   let old_register_04_value ≝ register_04_value m in
    2497   let old_register_05_value ≝ register_05_value m in
    2498   let old_register_06_value ≝ register_06_value m in
    2499   let old_register_07_value ≝ register_07_value m in
    2500   let old_register_10_value ≝ register_01_value m in
    2501   let old_register_11_value ≝ register_01_value m in
    2502   let old_register_12_value ≝ register_02_value m in
    2503   let old_register_13_value ≝ register_03_value m in
    2504   let old_register_14_value ≝ register_04_value m in
    2505   let old_register_15_value ≝ register_05_value m in
    2506   let old_register_16_value ≝ register_06_value m in
    2507   let old_register_17_value ≝ register_07_value m in
    2508   let old_register_20_value ≝ register_01_value m in
    2509   let old_register_21_value ≝ register_02_value m in
    2510   let old_register_22_value ≝ register_02_value m in
    2511   let old_register_23_value ≝ register_03_value m in
    2512   let old_register_24_value ≝ register_04_value m in
    2513   let old_register_25_value ≝ register_05_value m in
    2514   let old_register_26_value ≝ register_06_value m in
    2515   let old_register_27_value ≝ register_07_value m in
    2516   let old_register_30_value ≝ register_01_value m in
    2517   let old_register_31_value ≝ register_02_value m in
    2518   let old_register_32_value ≝ register_02_value m in
    2519   let old_register_33_value ≝ register_03_value m in
    2520   let old_register_34_value ≝ register_04_value m in
    2521   let old_register_35_value ≝ register_05_value m in
    2522   let old_register_36_value ≝ register_06_value m in
    2523   let old_register_37_value ≝ register_07_value m in
    2524   let old_register_A_value ≝ register_A_value m in
    2525   let old_register_B_value ≝ register_B_value m in
    2526   let old_register_DPL_value ≝ register_DPL_value m in
    2527   let old_register_DPH_value ≝ register_DPH_value m in
    2528   let old_register_Carry_value ≝ register_Carry_value m in
    2529     mk_RegisterMap old_register_00_value
    2530                    old_register_01_value
    2531                    old_register_02_value
    2532                    old_register_03_value
    2533                    old_register_04_value
    2534                    old_register_05_value
    2535                    old_register_06_value
    2536                    old_register_07_value
    2537                    old_register_10_value
    2538                    old_register_11_value
    2539                    old_register_12_value
    2540                    old_register_13_value
    2541                    old_register_14_value
    2542                    old_register_15_value
    2543                    old_register_16_value
    2544                    old_register_17_value
    2545                    old_register_20_value
    2546                    old_register_21_value
    2547                    old_register_22_value
    2548                    old_register_23_value
    2549                    old_register_24_value
    2550                    old_register_25_value
    2551                    old_register_26_value
    2552                    old_register_27_value
    2553                    old_register_30_value
    2554                    old_register_31_value
    2555                    old_register_32_value
    2556                    old_register_33_value
    2557                    (Some ? b)
    2558                    old_register_35_value
    2559                    old_register_36_value
    2560                    old_register_37_value
    2561                    old_register_A_value
    2562                    old_register_B_value
    2563                    old_register_DPL_value
    2564                    old_register_DPH_value
    2565                    old_register_Carry_value.
    2566 
    2567 definition update_register_35: Byte → RegisterMap → RegisterMap ≝
    2568   λb: Byte.
    2569   λm: RegisterMap.
    2570   let old_register_00_value ≝ register_00_value m in
    2571   let old_register_01_value ≝ register_01_value m in
    2572   let old_register_02_value ≝ register_02_value m in
    2573   let old_register_03_value ≝ register_03_value m in
    2574   let old_register_04_value ≝ register_04_value m in
    2575   let old_register_05_value ≝ register_05_value m in
    2576   let old_register_06_value ≝ register_06_value m in
    2577   let old_register_07_value ≝ register_07_value m in
    2578   let old_register_10_value ≝ register_01_value m in
    2579   let old_register_11_value ≝ register_01_value m in
    2580   let old_register_12_value ≝ register_02_value m in
    2581   let old_register_13_value ≝ register_03_value m in
    2582   let old_register_14_value ≝ register_04_value m in
    2583   let old_register_15_value ≝ register_05_value m in
    2584   let old_register_16_value ≝ register_06_value m in
    2585   let old_register_17_value ≝ register_07_value m in
    2586   let old_register_20_value ≝ register_01_value m in
    2587   let old_register_21_value ≝ register_02_value m in
    2588   let old_register_22_value ≝ register_02_value m in
    2589   let old_register_23_value ≝ register_03_value m in
    2590   let old_register_24_value ≝ register_04_value m in
    2591   let old_register_25_value ≝ register_05_value m in
    2592   let old_register_26_value ≝ register_06_value m in
    2593   let old_register_27_value ≝ register_07_value m in
    2594   let old_register_30_value ≝ register_01_value m in
    2595   let old_register_31_value ≝ register_02_value m in
    2596   let old_register_32_value ≝ register_02_value m in
    2597   let old_register_33_value ≝ register_03_value m in
    2598   let old_register_34_value ≝ register_04_value m in
    2599   let old_register_35_value ≝ register_05_value m in
    2600   let old_register_36_value ≝ register_06_value m in
    2601   let old_register_37_value ≝ register_07_value m in
    2602   let old_register_A_value ≝ register_A_value m in
    2603   let old_register_B_value ≝ register_B_value m in
    2604   let old_register_DPL_value ≝ register_DPL_value m in
    2605   let old_register_DPH_value ≝ register_DPH_value m in
    2606   let old_register_Carry_value ≝ register_Carry_value m in
    2607     mk_RegisterMap old_register_00_value
    2608                    old_register_01_value
    2609                    old_register_02_value
    2610                    old_register_03_value
    2611                    old_register_04_value
    2612                    old_register_05_value
    2613                    old_register_06_value
    2614                    old_register_07_value
    2615                    old_register_10_value
    2616                    old_register_11_value
    2617                    old_register_12_value
    2618                    old_register_13_value
    2619                    old_register_14_value
    2620                    old_register_15_value
    2621                    old_register_16_value
    2622                    old_register_17_value
    2623                    old_register_20_value
    2624                    old_register_21_value
    2625                    old_register_22_value
    2626                    old_register_23_value
    2627                    old_register_24_value
    2628                    old_register_25_value
    2629                    old_register_26_value
    2630                    old_register_27_value
    2631                    old_register_30_value
    2632                    old_register_31_value
    2633                    old_register_32_value
    2634                    old_register_33_value
    2635                    old_register_34_value
    2636                    (Some ? b)
    2637                    old_register_36_value
    2638                    old_register_37_value
    2639                    old_register_A_value
    2640                    old_register_B_value
    2641                    old_register_DPL_value
    2642                    old_register_DPH_value
    2643                    old_register_Carry_value.
    2644 
    2645 definition update_register_36: Byte → RegisterMap → RegisterMap ≝
    2646   λb: Byte.
    2647   λm: RegisterMap.
    2648   let old_register_00_value ≝ register_00_value m in
    2649   let old_register_01_value ≝ register_01_value m in
    2650   let old_register_02_value ≝ register_02_value m in
    2651   let old_register_03_value ≝ register_03_value m in
    2652   let old_register_04_value ≝ register_04_value m in
    2653   let old_register_05_value ≝ register_05_value m in
    2654   let old_register_06_value ≝ register_06_value m in
    2655   let old_register_07_value ≝ register_07_value m in
    2656   let old_register_10_value ≝ register_01_value m in
    2657   let old_register_11_value ≝ register_01_value m in
    2658   let old_register_12_value ≝ register_02_value m in
    2659   let old_register_13_value ≝ register_03_value m in
    2660   let old_register_14_value ≝ register_04_value m in
    2661   let old_register_15_value ≝ register_05_value m in
    2662   let old_register_16_value ≝ register_06_value m in
    2663   let old_register_17_value ≝ register_07_value m in
    2664   let old_register_20_value ≝ register_01_value m in
    2665   let old_register_21_value ≝ register_02_value m in
    2666   let old_register_22_value ≝ register_02_value m in
    2667   let old_register_23_value ≝ register_03_value m in
    2668   let old_register_24_value ≝ register_04_value m in
    2669   let old_register_25_value ≝ register_05_value m in
    2670   let old_register_26_value ≝ register_06_value m in
    2671   let old_register_27_value ≝ register_07_value m in
    2672   let old_register_30_value ≝ register_01_value m in
    2673   let old_register_31_value ≝ register_02_value m in
    2674   let old_register_32_value ≝ register_02_value m in
    2675   let old_register_33_value ≝ register_03_value m in
    2676   let old_register_34_value ≝ register_04_value m in
    2677   let old_register_35_value ≝ register_05_value m in
    2678   let old_register_36_value ≝ register_06_value m in
    2679   let old_register_37_value ≝ register_07_value m in
    2680   let old_register_A_value ≝ register_A_value m in
    2681   let old_register_B_value ≝ register_B_value m in
    2682   let old_register_DPL_value ≝ register_DPL_value m in
    2683   let old_register_DPH_value ≝ register_DPH_value m in
    2684   let old_register_Carry_value ≝ register_Carry_value m in
    2685     mk_RegisterMap old_register_00_value
    2686                    old_register_01_value
    2687                    old_register_02_value
    2688                    old_register_03_value
    2689                    old_register_04_value
    2690                    old_register_05_value
    2691                    old_register_06_value
    2692                    old_register_07_value
    2693                    old_register_10_value
    2694                    old_register_11_value
    2695                    old_register_12_value
    2696                    old_register_13_value
    2697                    old_register_14_value
    2698                    old_register_15_value
    2699                    old_register_16_value
    2700                    old_register_17_value
    2701                    old_register_20_value
    2702                    old_register_21_value
    2703                    old_register_22_value
    2704                    old_register_23_value
    2705                    old_register_24_value
    2706                    old_register_25_value
    2707                    old_register_26_value
    2708                    old_register_27_value
    2709                    old_register_30_value
    2710                    old_register_31_value
    2711                    old_register_32_value
    2712                    old_register_33_value
    2713                    old_register_34_value
    2714                    old_register_35_value
    2715                    (Some ? b)
    2716                    old_register_37_value
    2717                    old_register_A_value
    2718                    old_register_B_value
    2719                    old_register_DPL_value
    2720                    old_register_DPH_value
    2721                    old_register_Carry_value.
    2722 
    2723 definition update_register_37: Byte → RegisterMap → RegisterMap ≝
    2724   λb: Byte.
    2725   λm: RegisterMap.
    2726   let old_register_00_value ≝ register_00_value m in
    2727   let old_register_01_value ≝ register_01_value m in
    2728   let old_register_02_value ≝ register_02_value m in
    2729   let old_register_03_value ≝ register_03_value m in
    2730   let old_register_04_value ≝ register_04_value m in
    2731   let old_register_05_value ≝ register_05_value m in
    2732   let old_register_06_value ≝ register_06_value m in
    2733   let old_register_07_value ≝ register_07_value m in
    2734   let old_register_10_value ≝ register_01_value m in
    2735   let old_register_11_value ≝ register_01_value m in
    2736   let old_register_12_value ≝ register_02_value m in
    2737   let old_register_13_value ≝ register_03_value m in
    2738   let old_register_14_value ≝ register_04_value m in
    2739   let old_register_15_value ≝ register_05_value m in
    2740   let old_register_16_value ≝ register_06_value m in
    2741   let old_register_17_value ≝ register_07_value m in
    2742   let old_register_20_value ≝ register_01_value m in
    2743   let old_register_21_value ≝ register_02_value m in
    2744   let old_register_22_value ≝ register_02_value m in
    2745   let old_register_23_value ≝ register_03_value m in
    2746   let old_register_24_value ≝ register_04_value m in
    2747   let old_register_25_value ≝ register_05_value m in
    2748   let old_register_26_value ≝ register_06_value m in
    2749   let old_register_27_value ≝ register_07_value m in
    2750   let old_register_30_value ≝ register_01_value m in
    2751   let old_register_31_value ≝ register_02_value m in
    2752   let old_register_32_value ≝ register_02_value m in
    2753   let old_register_33_value ≝ register_03_value m in
    2754   let old_register_34_value ≝ register_04_value m in
    2755   let old_register_35_value ≝ register_05_value m in
    2756   let old_register_36_value ≝ register_06_value m in
    2757   let old_register_37_value ≝ register_07_value m in
    2758   let old_register_A_value ≝ register_A_value m in
    2759   let old_register_B_value ≝ register_B_value m in
    2760   let old_register_DPL_value ≝ register_DPL_value m in
    2761   let old_register_DPH_value ≝ register_DPH_value m in
    2762   let old_register_Carry_value ≝ register_Carry_value m in
    2763     mk_RegisterMap old_register_00_value
    2764                    old_register_01_value
    2765                    old_register_02_value
    2766                    old_register_03_value
    2767                    old_register_04_value
    2768                    old_register_05_value
    2769                    old_register_06_value
    2770                    old_register_07_value
    2771                    old_register_10_value
    2772                    old_register_11_value
    2773                    old_register_12_value
    2774                    old_register_13_value
    2775                    old_register_14_value
    2776                    old_register_15_value
    2777                    old_register_16_value
    2778                    old_register_17_value
    2779                    old_register_20_value
    2780                    old_register_21_value
    2781                    old_register_22_value
    2782                    old_register_23_value
    2783                    old_register_24_value
    2784                    old_register_25_value
    2785                    old_register_26_value
    2786                    old_register_27_value
    2787                    old_register_30_value
    2788                    old_register_31_value
    2789                    old_register_32_value
    2790                    old_register_33_value
    2791                    old_register_34_value
    2792                    old_register_35_value
    2793                    old_register_36_value
    2794                    (Some ? b)
    2795                    old_register_A_value
    2796                    old_register_B_value
    2797                    old_register_DPL_value
    2798                    old_register_DPH_value
    2799                    old_register_Carry_value.
    2800 
    2801 definition update_register_A: Byte → RegisterMap → RegisterMap ≝
    2802   λb: Byte.
    2803   λm: RegisterMap.
    2804   let old_register_00_value ≝ register_00_value m in
    2805   let old_register_01_value ≝ register_01_value m in
    2806   let old_register_02_value ≝ register_02_value m in
    2807   let old_register_03_value ≝ register_03_value m in
    2808   let old_register_04_value ≝ register_04_value m in
    2809   let old_register_05_value ≝ register_05_value m in
    2810   let old_register_06_value ≝ register_06_value m in
    2811   let old_register_07_value ≝ register_07_value m in
    2812   let old_register_10_value ≝ register_01_value m in
    2813   let old_register_11_value ≝ register_01_value m in
    2814   let old_register_12_value ≝ register_02_value m in
    2815   let old_register_13_value ≝ register_03_value m in
    2816   let old_register_14_value ≝ register_04_value m in
    2817   let old_register_15_value ≝ register_05_value m in
    2818   let old_register_16_value ≝ register_06_value m in
    2819   let old_register_17_value ≝ register_07_value m in
    2820   let old_register_20_value ≝ register_01_value m in
    2821   let old_register_21_value ≝ register_02_value m in
    2822   let old_register_22_value ≝ register_02_value m in
    2823   let old_register_23_value ≝ register_03_value m in
    2824   let old_register_24_value ≝ register_04_value m in
    2825   let old_register_25_value ≝ register_05_value m in
    2826   let old_register_26_value ≝ register_06_value m in
    2827   let old_register_27_value ≝ register_07_value m in
    2828   let old_register_30_value ≝ register_01_value m in
    2829   let old_register_31_value ≝ register_02_value m in
    2830   let old_register_32_value ≝ register_02_value m in
    2831   let old_register_33_value ≝ register_03_value m in
    2832   let old_register_34_value ≝ register_04_value m in
    2833   let old_register_35_value ≝ register_05_value m in
    2834   let old_register_36_value ≝ register_06_value m in
    2835   let old_register_37_value ≝ register_07_value m in
    2836   let old_register_A_value ≝ register_A_value m in
    2837   let old_register_B_value ≝ register_B_value m in
    2838   let old_register_DPL_value ≝ register_DPL_value m in
    2839   let old_register_DPH_value ≝ register_DPH_value m in
    2840   let old_register_Carry_value ≝ register_Carry_value m in
    2841     mk_RegisterMap old_register_00_value
    2842                    old_register_01_value
    2843                    old_register_02_value
    2844                    old_register_03_value
    2845                    old_register_04_value
    2846                    old_register_05_value
    2847                    old_register_06_value
    2848                    old_register_07_value
    2849                    old_register_10_value
    2850                    old_register_11_value
    2851                    old_register_12_value
    2852                    old_register_13_value
    2853                    old_register_14_value
    2854                    old_register_15_value
    2855                    old_register_16_value
    2856                    old_register_17_value
    2857                    old_register_20_value
    2858                    old_register_21_value
    2859                    old_register_22_value
    2860                    old_register_23_value
    2861                    old_register_24_value
    2862                    old_register_25_value
    2863                    old_register_26_value
    2864                    old_register_27_value
    2865                    old_register_30_value
    2866                    old_register_31_value
    2867                    old_register_32_value
    2868                    old_register_33_value
    2869                    old_register_34_value
    2870                    old_register_35_value
    2871                    old_register_36_value
    2872                    old_register_37_value
    2873                    (Some ? b)
    2874                    old_register_B_value
    2875                    old_register_DPL_value
    2876                    old_register_DPH_value
    2877                    old_register_Carry_value.
    2878 
    2879 definition update_register_B: Byte → RegisterMap → RegisterMap ≝
    2880   λb: Byte.
    2881   λm: RegisterMap.
    2882   let old_register_00_value ≝ register_00_value m in
    2883   let old_register_01_value ≝ register_01_value m in
    2884   let old_register_02_value ≝ register_02_value m in
    2885   let old_register_03_value ≝ register_03_value m in
    2886   let old_register_04_value ≝ register_04_value m in
    2887   let old_register_05_value ≝ register_05_value m in
    2888   let old_register_06_value ≝ register_06_value m in
    2889   let old_register_07_value ≝ register_07_value m in
    2890   let old_register_10_value ≝ register_01_value m in
    2891   let old_register_11_value ≝ register_01_value m in
    2892   let old_register_12_value ≝ register_02_value m in
    2893   let old_register_13_value ≝ register_03_value m in
    2894   let old_register_14_value ≝ register_04_value m in
    2895   let old_register_15_value ≝ register_05_value m in
    2896   let old_register_16_value ≝ register_06_value m in
    2897   let old_register_17_value ≝ register_07_value m in
    2898   let old_register_20_value ≝ register_01_value m in
    2899   let old_register_21_value ≝ register_02_value m in
    2900   let old_register_22_value ≝ register_02_value m in
    2901   let old_register_23_value ≝ register_03_value m in
    2902   let old_register_24_value ≝ register_04_value m in
    2903   let old_register_25_value ≝ register_05_value m in
    2904   let old_register_26_value ≝ register_06_value m in
    2905   let old_register_27_value ≝ register_07_value m in
    2906   let old_register_30_value ≝ register_01_value m in
    2907   let old_register_31_value ≝ register_02_value m in
    2908   let old_register_32_value ≝ register_02_value m in
    2909   let old_register_33_value ≝ register_03_value m in
    2910   let old_register_34_value ≝ register_04_value m in
    2911   let old_register_35_value ≝ register_05_value m in
    2912   let old_register_36_value ≝ register_06_value m in
    2913   let old_register_37_value ≝ register_07_value m in
    2914   let old_register_A_value ≝ register_A_value m in
    2915   let old_register_B_value ≝ register_B_value m in
    2916   let old_register_DPL_value ≝ register_DPL_value m in
    2917   let old_register_DPH_value ≝ register_DPH_value m in
    2918   let old_register_Carry_value ≝ register_Carry_value m in
    2919     mk_RegisterMap old_register_00_value
    2920                    old_register_01_value
    2921                    old_register_02_value
    2922                    old_register_03_value
    2923                    old_register_04_value
    2924                    old_register_05_value
    2925                    old_register_06_value
    2926                    old_register_07_value
    2927                    old_register_10_value
    2928                    old_register_11_value
    2929                    old_register_12_value
    2930                    old_register_13_value
    2931                    old_register_14_value
    2932                    old_register_15_value
    2933                    old_register_16_value
    2934                    old_register_17_value
    2935                    old_register_20_value
    2936                    old_register_21_value
    2937                    old_register_22_value
    2938                    old_register_23_value
    2939                    old_register_24_value
    2940                    old_register_25_value
    2941                    old_register_26_value
    2942                    old_register_27_value
    2943                    old_register_30_value
    2944                    old_register_31_value
    2945                    old_register_32_value
    2946                    old_register_33_value
    2947                    old_register_34_value
    2948                    old_register_35_value
    2949                    old_register_36_value
    2950                    old_register_37_value
    2951                    old_register_A_value
    2952                    (Some ? b)
    2953                    old_register_DPL_value
    2954                    old_register_DPH_value
    2955                    old_register_Carry_value.
    2956 
    2957 definition update_register_DPL: Byte → RegisterMap → RegisterMap ≝
    2958   λb: Byte.
    2959   λm: RegisterMap.
    2960   let old_register_00_value ≝ register_00_value m in
    2961   let old_register_01_value ≝ register_01_value m in
    2962   let old_register_02_value ≝ register_02_value m in
    2963   let old_register_03_value ≝ register_03_value m in
    2964   let old_register_04_value ≝ register_04_value m in
    2965   let old_register_05_value ≝ register_05_value m in
    2966   let old_register_06_value ≝ register_06_value m in
    2967   let old_register_07_value ≝ register_07_value m in
    2968   let old_register_10_value ≝ register_01_value m in
    2969   let old_register_11_value ≝ register_01_value m in
    2970   let old_register_12_value ≝ register_02_value m in
    2971   let old_register_13_value ≝ register_03_value m in
    2972   let old_register_14_value ≝ register_04_value m in
    2973   let old_register_15_value ≝ register_05_value m in
    2974   let old_register_16_value ≝ register_06_value m in
    2975   let old_register_17_value ≝ register_07_value m in
    2976   let old_register_20_value ≝ register_01_value m in
    2977   let old_register_21_value ≝ register_02_value m in
    2978   let old_register_22_value ≝ register_02_value m in
    2979   let old_register_23_value ≝ register_03_value m in
    2980   let old_register_24_value ≝ register_04_value m in
    2981   let old_register_25_value ≝ register_05_value m in
    2982   let old_register_26_value ≝ register_06_value m in
    2983   let old_register_27_value ≝ register_07_value m in
    2984   let old_register_30_value ≝ register_01_value m in
    2985   let old_register_31_value ≝ register_02_value m in
    2986   let old_register_32_value ≝ register_02_value m in
    2987   let old_register_33_value ≝ register_03_value m in
    2988   let old_register_34_value ≝ register_04_value m in
    2989   let old_register_35_value ≝ register_05_value m in
    2990   let old_register_36_value ≝ register_06_value m in
    2991   let old_register_37_value ≝ register_07_value m in
    2992   let old_register_A_value ≝ register_A_value m in
    2993   let old_register_B_value ≝ register_B_value m in
    2994   let old_register_DPL_value ≝ register_DPL_value m in
    2995   let old_register_DPH_value ≝ register_DPH_value m in
    2996   let old_register_Carry_value ≝ register_Carry_value m in
    2997     mk_RegisterMap old_register_00_value
    2998                    old_register_01_value
    2999                    old_register_02_value
    3000                    old_register_03_value
    3001                    old_register_04_value
    3002                    old_register_05_value
    3003                    old_register_06_value
    3004                    old_register_07_value
    3005                    old_register_10_value
    3006                    old_register_11_value
    3007                    old_register_12_value
    3008                    old_register_13_value
    3009                    old_register_14_value
    3010                    old_register_15_value
    3011                    old_register_16_value
    3012                    old_register_17_value
    3013                    old_register_20_value
    3014                    old_register_21_value
    3015                    old_register_22_value
    3016                    old_register_23_value
    3017                    old_register_24_value
    3018                    old_register_25_value
    3019                    old_register_26_value
    3020                    old_register_27_value
    3021                    old_register_30_value
    3022                    old_register_31_value
    3023                    old_register_32_value
    3024                    old_register_33_value
    3025                    old_register_34_value
    3026                    old_register_35_value
    3027                    old_register_36_value
    3028                    old_register_37_value
    3029                    old_register_A_value
    3030                    old_register_B_value
    3031                    (Some ? b)
    3032                    old_register_DPH_value
    3033                    old_register_Carry_value.
    3034 
    3035 definition update_register_DPH: Byte → RegisterMap → RegisterMap ≝
    3036   λb: Byte.
    3037   λm: RegisterMap.
    3038   let old_register_00_value ≝ register_00_value m in
    3039   let old_register_01_value ≝ register_01_value m in
    3040   let old_register_02_value ≝ register_02_value m in
    3041   let old_register_03_value ≝ register_03_value m in
    3042   let old_register_04_value ≝ register_04_value m in
    3043   let old_register_05_value ≝ register_05_value m in
    3044   let old_register_06_value ≝ register_06_value m in
    3045   let old_register_07_value ≝ register_07_value m in
    3046   let old_register_10_value ≝ register_01_value m in
    3047   let old_register_11_value ≝ register_01_value m in
    3048   let old_register_12_value ≝ register_02_value m in
    3049   let old_register_13_value ≝ register_03_value m in
    3050   let old_register_14_value ≝ register_04_value m in
    3051   let old_register_15_value ≝ register_05_value m in
    3052   let old_register_16_value ≝ register_06_value m in
    3053   let old_register_17_value ≝ register_07_value m in
    3054   let old_register_20_value ≝ register_01_value m in
    3055   let old_register_21_value ≝ register_02_value m in
    3056   let old_register_22_value ≝ register_02_value m in
    3057   let old_register_23_value ≝ register_03_value m in
    3058   let old_register_24_value ≝ register_04_value m in
    3059   let old_register_25_value ≝ register_05_value m in
    3060   let old_register_26_value ≝ register_06_value m in
    3061   let old_register_27_value ≝ register_07_value m in
    3062   let old_register_30_value ≝ register_01_value m in
    3063   let old_register_31_value ≝ register_02_value m in
    3064   let old_register_32_value ≝ register_02_value m in
    3065   let old_register_33_value ≝ register_03_value m in
    3066   let old_register_34_value ≝ register_04_value m in
    3067   let old_register_35_value ≝ register_05_value m in
    3068   let old_register_36_value ≝ register_06_value m in
    3069   let old_register_37_value ≝ register_07_value m in
    3070   let old_register_A_value ≝ register_A_value m in
    3071   let old_register_B_value ≝ register_B_value m in
    3072   let old_register_DPL_value ≝ register_DPL_value m in
    3073   let old_register_DPH_value ≝ register_DPH_value m in
    3074   let old_register_Carry_value ≝ register_Carry_value m in
    3075     mk_RegisterMap old_register_00_value
    3076                    old_register_01_value
    3077                    old_register_02_value
    3078                    old_register_03_value
    3079                    old_register_04_value
    3080                    old_register_05_value
    3081                    old_register_06_value
    3082                    old_register_07_value
    3083                    old_register_10_value
    3084                    old_register_11_value
    3085                    old_register_12_value
    3086                    old_register_13_value
    3087                    old_register_14_value
    3088                    old_register_15_value
    3089                    old_register_16_value
    3090                    old_register_17_value
    3091                    old_register_20_value
    3092                    old_register_21_value
    3093                    old_register_22_value
    3094                    old_register_23_value
    3095                    old_register_24_value
    3096                    old_register_25_value
    3097                    old_register_26_value
    3098                    old_register_27_value
    3099                    old_register_30_value
    3100                    old_register_31_value
    3101                    old_register_32_value
    3102                    old_register_33_value
    3103                    old_register_34_value
    3104                    old_register_35_value
    3105                    old_register_36_value
    3106                    old_register_37_value
    3107                    old_register_A_value
    3108                    old_register_B_value
    3109                    old_register_DPL_value
    3110                    (Some ? b)
    3111                    old_register_Carry_value.
    3112 
    3113 definition update_register_Carry: Byte → RegisterMap → RegisterMap ≝
    3114   λb: Byte.
    3115   λm: RegisterMap.
    3116   let old_register_00_value ≝ register_00_value m in
    3117   let old_register_01_value ≝ register_01_value m in
    3118   let old_register_02_value ≝ register_02_value m in
    3119   let old_register_03_value ≝ register_03_value m in
    3120   let old_register_04_value ≝ register_04_value m in
    3121   let old_register_05_value ≝ register_05_value m in
    3122   let old_register_06_value ≝ register_06_value m in
    3123   let old_register_07_value ≝ register_07_value m in
    3124   let old_register_10_value ≝ register_01_value m in
    3125   let old_register_11_value ≝ register_01_value m in
    3126   let old_register_12_value ≝ register_02_value m in
    3127   let old_register_13_value ≝ register_03_value m in
    3128   let old_register_14_value ≝ register_04_value m in
    3129   let old_register_15_value ≝ register_05_value m in
    3130   let old_register_16_value ≝ register_06_value m in
    3131   let old_register_17_value ≝ register_07_value m in
    3132   let old_register_20_value ≝ register_01_value m in
    3133   let old_register_21_value ≝ register_02_value m in
    3134   let old_register_22_value ≝ register_02_value m in
    3135   let old_register_23_value ≝ register_03_value m in
    3136   let old_register_24_value ≝ register_04_value m in
    3137   let old_register_25_value ≝ register_05_value m in
    3138   let old_register_26_value ≝ register_06_value m in
    3139   let old_register_27_value ≝ register_07_value m in
    3140   let old_register_30_value ≝ register_01_value m in
    3141   let old_register_31_value ≝ register_02_value m in
    3142   let old_register_32_value ≝ register_02_value m in
    3143   let old_register_33_value ≝ register_03_value m in
    3144   let old_register_34_value ≝ register_04_value m in
    3145   let old_register_35_value ≝ register_05_value m in
    3146   let old_register_36_value ≝ register_06_value m in
    3147   let old_register_37_value ≝ register_07_value m in
    3148   let old_register_A_value ≝ register_A_value m in
    3149   let old_register_B_value ≝ register_B_value m in
    3150   let old_register_DPL_value ≝ register_DPL_value m in
    3151   let old_register_DPH_value ≝ register_DPH_value m in
    3152     mk_RegisterMap old_register_00_value
    3153                    old_register_01_value
    3154                    old_register_02_value
    3155                    old_register_03_value
    3156                    old_register_04_value
    3157                    old_register_05_value
    3158                    old_register_06_value
    3159                    old_register_07_value
    3160                    old_register_10_value
    3161                    old_register_11_value
    3162                    old_register_12_value
    3163                    old_register_13_value
    3164                    old_register_14_value
    3165                    old_register_15_value
    3166                    old_register_16_value
    3167                    old_register_17_value
    3168                    old_register_20_value
    3169                    old_register_21_value
    3170                    old_register_22_value
    3171                    old_register_23_value
    3172                    old_register_24_value
    3173                    old_register_25_value
    3174                    old_register_26_value
    3175                    old_register_27_value
    3176                    old_register_30_value
    3177                    old_register_31_value
    3178                    old_register_32_value
    3179                    old_register_33_value
    3180                    old_register_34_value
    3181                    old_register_35_value
    3182                    old_register_36_value
    3183                    old_register_37_value
    3184                    old_register_A_value
    3185                    old_register_B_value
    3186                    old_register_DPL_value
    3187                    old_register_DPH_value
    3188                    (Some ? b).
    3189 
    3190 definition update_register_map: Register → Byte → RegisterMap → RegisterMap ≝
    3191   λr: Register.
    3192   λb: Byte.
    3193   λm: RegisterMap.
    3194   match r with
    3195   [ Register00 ⇒ update_register_00 b m
    3196   | Register01 ⇒ update_register_01 b m
    3197   | Register02 ⇒ update_register_02 b m
    3198   | Register03 ⇒ update_register_03 b m
    3199   | Register04 ⇒ update_register_04 b m
    3200   | Register05 ⇒ update_register_05 b m
    3201   | Register06 ⇒ update_register_06 b m
    3202   | Register07 ⇒ update_register_07 b m
    3203   | Register10 ⇒ update_register_10 b m
    3204   | Register11 ⇒ update_register_11 b m
    3205   | Register12 ⇒ update_register_12 b m
    3206   | Register13 ⇒ update_register_13 b m
    3207   | Register14 ⇒ update_register_14 b m
    3208   | Register15 ⇒ update_register_15 b m
    3209   | Register16 ⇒ update_register_16 b m
    3210   | Register17 ⇒ update_register_17 b m
    3211   | Register20 ⇒ update_register_20 b m
    3212   | Register21 ⇒ update_register_21 b m
    3213   | Register22 ⇒ update_register_22 b m
    3214   | Register23 ⇒ update_register_23 b m
    3215   | Register24 ⇒ update_register_24 b m
    3216   | Register25 ⇒ update_register_25 b m
    3217   | Register26 ⇒ update_register_26 b m
    3218   | Register27 ⇒ update_register_27 b m
    3219   | Register30 ⇒ update_register_30 b m
    3220   | Register31 ⇒ update_register_31 b m
    3221   | Register32 ⇒ update_register_32 b m
    3222   | Register33 ⇒ update_register_33 b m
    3223   | Register34 ⇒ update_register_34 b m
    3224   | Register35 ⇒ update_register_35 b m
    3225   | Register36 ⇒ update_register_36 b m
    3226   | Register37 ⇒ update_register_37 b m
    3227   | RegisterA ⇒ update_register_A b m
    3228   | RegisterB ⇒ update_register_B b m
    3229   | RegisterDPL ⇒ update_register_DPL b m
    3230   | RegisterDPH ⇒ update_register_DPH b m
    3231   | RegisterCarry ⇒ update_register_Carry b m
    3232   ].
     208
     209definition hw_register_env ≝ BitVectorTrie beval 6.
     210definition empty_hw_register_env: hw_register_env ≝ Stub ….
     211definition hwreg_retrieve: hw_register_env → Register → beval ≝
     212 λenv,r. lookup … (bitvector_of_register r) env BVundef.
     213definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
     214 λr,v,env. insert … (bitvector_of_register r) v env.
    3233215 
    3234216record Eval: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.