Changeset 1098


Ignore:
Timestamp:
Aug 3, 2011, 2:48:11 PM (8 years ago)
Author:
campbell
Message:

Merge branch with trunk

Location:
Deliverables/D3.3/id-lookup-branch
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

    • Property svn:mergeinfo changed
      /srcmerged: 1094
  • Deliverables/D3.3/id-lookup-branch/ASM

  • Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma

    r1091 r1098  
    147147definition RegisterSPL ≝ Register06.
    148148definition RegisterSPH ≝ Register07.
     149definition Registers ≝
     150  [Register00; Register01; Register02; Register03; Register04;
     151   Register05; Register06; Register07; Register10; Register11;
     152   Register12; Register13; Register14; Register15; Register16;
     153   Register17; Register20; Register21; Register22; Register23;
     154   Register24; Register25; Register26; Register27; Register30;
     155   Register31; Register32; Register33; Register34; Register35;
     156   Register36; Register37; RegisterA; RegisterB; RegisterDPL;
     157   RegisterDPH; RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
     158   RegisterSST].
    149159definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
     160definition RegisterCallerSaved ≝
     161  [Register00; Register01; Register02; Register03; Register04;
     162   Register05; Register06; Register07; Register10; Register11;
     163   Register12; Register13; Register14; Register15; Register16;
     164   Register17; Register30; Register31; Register32; Register33;
     165   Register34; Register35; Register36; Register37].
    150166definition RegisterCalleeSaved ≝
    151   [Register20 ; Register21 ; Register22 ; Register23 ; Register24 ; Register25 ; Register26 ; Register27].
     167  [Register20; Register21; Register22; Register23; Register24;
     168   Register25; Register26; Register27].
     169definition RegisterParameters ≝
     170  [Register30; Register31; Register32; Register33; Register34; Register35;
     171   Register36; Register37].
    152172
    153173definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     
    231251  register_B_value: option Byte;
    232252  register_DPL_value: option Byte;
    233   register_DPH_value: option Byte
     253  register_DPH_value: option Byte;
     254  register_Carry_value: option Byte
    234255  (* carry only used in liveness analysis *)
    235256}.
     
    244265                 (None ?) (None ?) (None ?) (None ?)
    245266                 (None ?) (None ?) (None ?) (None ?)
    246                  (None ?) (None ?) (None ?) (None ?).
     267                 (None ?) (None ?) (None ?) (None ?)
     268                 (None ?).
    247269                 
    248270definition lookup_register_map: Register → RegisterMap → option Byte ≝
     
    286308  | RegisterDPL ⇒ register_DPL_value m
    287309  | RegisterDPH ⇒ register_DPH_value m
     310  | RegisterCarry ⇒ register_Carry_value m
    288311  ].
    289312 
     
    327350  let old_register_DPL_value ≝ register_DPL_value m in
    328351  let old_register_DPH_value ≝ register_DPH_value m in
     352  let old_register_Carry_value ≝ register_Carry_value m in
    329353    mk_RegisterMap (Some ? b)
    330354                   old_register_01_value
     
    362386                   old_register_B_value
    363387                   old_register_DPL_value
    364                    old_register_DPH_value.
     388                   old_register_DPH_value
     389                   old_register_Carry_value.
    365390
    366391definition update_register_01: Byte → RegisterMap → RegisterMap ≝
     
    403428  let old_register_DPL_value ≝ register_DPL_value m in
    404429  let old_register_DPH_value ≝ register_DPH_value m in
    405     mk_RegisterMap old_register_00_value
    406                    (Some ? b)
    407                    old_register_02_value
    408                    old_register_03_value
    409                    old_register_04_value
    410                    old_register_05_value
    411                    old_register_06_value
    412                    old_register_07_value
    413                    old_register_10_value
    414                    old_register_11_value
    415                    old_register_12_value
    416                    old_register_13_value
    417                    old_register_14_value
    418                    old_register_15_value
    419                    old_register_16_value
    420                    old_register_17_value
    421                    old_register_20_value
    422                    old_register_21_value
    423                    old_register_22_value
    424                    old_register_23_value
    425                    old_register_24_value
    426                    old_register_25_value
    427                    old_register_26_value
    428                    old_register_27_value
    429                    old_register_30_value
    430                    old_register_31_value
    431                    old_register_32_value
    432                    old_register_33_value
    433                    old_register_34_value
    434                    old_register_35_value
    435                    old_register_36_value
    436                    old_register_37_value
    437                    old_register_A_value
    438                    old_register_B_value
    439                    old_register_DPL_value
    440                    old_register_DPH_value.
     430  let old_register_Carry_value ≝ register_Carry_value m in
     431    mk_RegisterMap old_register_00_value
     432                   (Some ? b)
     433                   old_register_02_value
     434                   old_register_03_value
     435                   old_register_04_value
     436                   old_register_05_value
     437                   old_register_06_value
     438                   old_register_07_value
     439                   old_register_10_value
     440                   old_register_11_value
     441                   old_register_12_value
     442                   old_register_13_value
     443                   old_register_14_value
     444                   old_register_15_value
     445                   old_register_16_value
     446                   old_register_17_value
     447                   old_register_20_value
     448                   old_register_21_value
     449                   old_register_22_value
     450                   old_register_23_value
     451                   old_register_24_value
     452                   old_register_25_value
     453                   old_register_26_value
     454                   old_register_27_value
     455                   old_register_30_value
     456                   old_register_31_value
     457                   old_register_32_value
     458                   old_register_33_value
     459                   old_register_34_value
     460                   old_register_35_value
     461                   old_register_36_value
     462                   old_register_37_value
     463                   old_register_A_value
     464                   old_register_B_value
     465                   old_register_DPL_value
     466                   old_register_DPH_value
     467                   old_register_Carry_value.
    441468
    442469definition update_register_02: Byte → RegisterMap → RegisterMap ≝
     
    479506  let old_register_DPL_value ≝ register_DPL_value m in
    480507  let old_register_DPH_value ≝ register_DPH_value m in
    481     mk_RegisterMap old_register_00_value
    482                    old_register_01_value
    483                    (Some ? b)
    484                    old_register_03_value
    485                    old_register_04_value
    486                    old_register_05_value
    487                    old_register_06_value
    488                    old_register_07_value
    489                    old_register_10_value
    490                    old_register_11_value
    491                    old_register_12_value
    492                    old_register_13_value
    493                    old_register_14_value
    494                    old_register_15_value
    495                    old_register_16_value
    496                    old_register_17_value
    497                    old_register_20_value
    498                    old_register_21_value
    499                    old_register_22_value
    500                    old_register_23_value
    501                    old_register_24_value
    502                    old_register_25_value
    503                    old_register_26_value
    504                    old_register_27_value
    505                    old_register_30_value
    506                    old_register_31_value
    507                    old_register_32_value
    508                    old_register_33_value
    509                    old_register_34_value
    510                    old_register_35_value
    511                    old_register_36_value
    512                    old_register_37_value
    513                    old_register_A_value
    514                    old_register_B_value
    515                    old_register_DPL_value
    516                    old_register_DPH_value.
     508  let old_register_Carry_value ≝ register_Carry_value m in
     509    mk_RegisterMap old_register_00_value
     510                   old_register_01_value
     511                   (Some ? b)
     512                   old_register_03_value
     513                   old_register_04_value
     514                   old_register_05_value
     515                   old_register_06_value
     516                   old_register_07_value
     517                   old_register_10_value
     518                   old_register_11_value
     519                   old_register_12_value
     520                   old_register_13_value
     521                   old_register_14_value
     522                   old_register_15_value
     523                   old_register_16_value
     524                   old_register_17_value
     525                   old_register_20_value
     526                   old_register_21_value
     527                   old_register_22_value
     528                   old_register_23_value
     529                   old_register_24_value
     530                   old_register_25_value
     531                   old_register_26_value
     532                   old_register_27_value
     533                   old_register_30_value
     534                   old_register_31_value
     535                   old_register_32_value
     536                   old_register_33_value
     537                   old_register_34_value
     538                   old_register_35_value
     539                   old_register_36_value
     540                   old_register_37_value
     541                   old_register_A_value
     542                   old_register_B_value
     543                   old_register_DPL_value
     544                   old_register_DPH_value
     545                   old_register_Carry_value.
    517546
    518547definition update_register_03: Byte → RegisterMap → RegisterMap ≝
     
    555584  let old_register_DPL_value ≝ register_DPL_value m in
    556585  let old_register_DPH_value ≝ register_DPH_value m in
    557     mk_RegisterMap old_register_00_value
    558                    old_register_01_value
    559                    old_register_02_value
    560                    (Some ? b)
    561                    old_register_04_value
    562                    old_register_05_value
    563                    old_register_06_value
    564                    old_register_07_value
    565                    old_register_10_value
    566                    old_register_11_value
    567                    old_register_12_value
    568                    old_register_13_value
    569                    old_register_14_value
    570                    old_register_15_value
    571                    old_register_16_value
    572                    old_register_17_value
    573                    old_register_20_value
    574                    old_register_21_value
    575                    old_register_22_value
    576                    old_register_23_value
    577                    old_register_24_value
    578                    old_register_25_value
    579                    old_register_26_value
    580                    old_register_27_value
    581                    old_register_30_value
    582                    old_register_31_value
    583                    old_register_32_value
    584                    old_register_33_value
    585                    old_register_34_value
    586                    old_register_35_value
    587                    old_register_36_value
    588                    old_register_37_value
    589                    old_register_A_value
    590                    old_register_B_value
    591                    old_register_DPL_value
    592                    old_register_DPH_value.
     586  let old_register_Carry_value ≝ register_Carry_value m in
     587    mk_RegisterMap old_register_00_value
     588                   old_register_01_value
     589                   old_register_02_value
     590                   (Some ? b)
     591                   old_register_04_value
     592                   old_register_05_value
     593                   old_register_06_value
     594                   old_register_07_value
     595                   old_register_10_value
     596                   old_register_11_value
     597                   old_register_12_value
     598                   old_register_13_value
     599                   old_register_14_value
     600                   old_register_15_value
     601                   old_register_16_value
     602                   old_register_17_value
     603                   old_register_20_value
     604                   old_register_21_value
     605                   old_register_22_value
     606                   old_register_23_value
     607                   old_register_24_value
     608                   old_register_25_value
     609                   old_register_26_value
     610                   old_register_27_value
     611                   old_register_30_value
     612                   old_register_31_value
     613                   old_register_32_value
     614                   old_register_33_value
     615                   old_register_34_value
     616                   old_register_35_value
     617                   old_register_36_value
     618                   old_register_37_value
     619                   old_register_A_value
     620                   old_register_B_value
     621                   old_register_DPL_value
     622                   old_register_DPH_value
     623                   old_register_Carry_value.
    593624
    594625definition update_register_04: Byte → RegisterMap → RegisterMap ≝
     
    631662  let old_register_DPL_value ≝ register_DPL_value m in
    632663  let old_register_DPH_value ≝ register_DPH_value m in
    633     mk_RegisterMap old_register_00_value
    634                    old_register_01_value
    635                    old_register_02_value
    636                    old_register_03_value
    637                    (Some ? b)
    638                    old_register_05_value
    639                    old_register_06_value
    640                    old_register_07_value
    641                    old_register_10_value
    642                    old_register_11_value
    643                    old_register_12_value
    644                    old_register_13_value
    645                    old_register_14_value
    646                    old_register_15_value
    647                    old_register_16_value
    648                    old_register_17_value
    649                    old_register_20_value
    650                    old_register_21_value
    651                    old_register_22_value
    652                    old_register_23_value
    653                    old_register_24_value
    654                    old_register_25_value
    655                    old_register_26_value
    656                    old_register_27_value
    657                    old_register_30_value
    658                    old_register_31_value
    659                    old_register_32_value
    660                    old_register_33_value
    661                    old_register_34_value
    662                    old_register_35_value
    663                    old_register_36_value
    664                    old_register_37_value
    665                    old_register_A_value
    666                    old_register_B_value
    667                    old_register_DPL_value
    668                    old_register_DPH_value.
     664  let old_register_Carry_value ≝ register_Carry_value m in
     665    mk_RegisterMap old_register_00_value
     666                   old_register_01_value
     667                   old_register_02_value
     668                   old_register_03_value
     669                   (Some ? b)
     670                   old_register_05_value
     671                   old_register_06_value
     672                   old_register_07_value
     673                   old_register_10_value
     674                   old_register_11_value
     675                   old_register_12_value
     676                   old_register_13_value
     677                   old_register_14_value
     678                   old_register_15_value
     679                   old_register_16_value
     680                   old_register_17_value
     681                   old_register_20_value
     682                   old_register_21_value
     683                   old_register_22_value
     684                   old_register_23_value
     685                   old_register_24_value
     686                   old_register_25_value
     687                   old_register_26_value
     688                   old_register_27_value
     689                   old_register_30_value
     690                   old_register_31_value
     691                   old_register_32_value
     692                   old_register_33_value
     693                   old_register_34_value
     694                   old_register_35_value
     695                   old_register_36_value
     696                   old_register_37_value
     697                   old_register_A_value
     698                   old_register_B_value
     699                   old_register_DPL_value
     700                   old_register_DPH_value
     701                   old_register_Carry_value.
    669702
    670703definition update_register_05: Byte → RegisterMap → RegisterMap ≝
     
    707740  let old_register_DPL_value ≝ register_DPL_value m in
    708741  let old_register_DPH_value ≝ register_DPH_value m in
    709     mk_RegisterMap old_register_00_value
    710                    old_register_01_value
    711                    old_register_02_value
    712                    old_register_03_value
    713                    old_register_04_value
    714                    (Some ? b)
    715                    old_register_06_value
    716                    old_register_07_value
    717                    old_register_10_value
    718                    old_register_11_value
    719                    old_register_12_value
    720                    old_register_13_value
    721                    old_register_14_value
    722                    old_register_15_value
    723                    old_register_16_value
    724                    old_register_17_value
    725                    old_register_20_value
    726                    old_register_21_value
    727                    old_register_22_value
    728                    old_register_23_value
    729                    old_register_24_value
    730                    old_register_25_value
    731                    old_register_26_value
    732                    old_register_27_value
    733                    old_register_30_value
    734                    old_register_31_value
    735                    old_register_32_value
    736                    old_register_33_value
    737                    old_register_34_value
    738                    old_register_35_value
    739                    old_register_36_value
    740                    old_register_37_value
    741                    old_register_A_value
    742                    old_register_B_value
    743                    old_register_DPL_value
    744                    old_register_DPH_value.
     742  let old_register_Carry_value ≝ register_Carry_value m in
     743    mk_RegisterMap old_register_00_value
     744                   old_register_01_value
     745                   old_register_02_value
     746                   old_register_03_value
     747                   old_register_04_value
     748                   (Some ? b)
     749                   old_register_06_value
     750                   old_register_07_value
     751                   old_register_10_value
     752                   old_register_11_value
     753                   old_register_12_value
     754                   old_register_13_value
     755                   old_register_14_value
     756                   old_register_15_value
     757                   old_register_16_value
     758                   old_register_17_value
     759                   old_register_20_value
     760                   old_register_21_value
     761                   old_register_22_value
     762                   old_register_23_value
     763                   old_register_24_value
     764                   old_register_25_value
     765                   old_register_26_value
     766                   old_register_27_value
     767                   old_register_30_value
     768                   old_register_31_value
     769                   old_register_32_value
     770                   old_register_33_value
     771                   old_register_34_value
     772                   old_register_35_value
     773                   old_register_36_value
     774                   old_register_37_value
     775                   old_register_A_value
     776                   old_register_B_value
     777                   old_register_DPL_value
     778                   old_register_DPH_value
     779                   old_register_Carry_value.
    745780
    746781definition update_register_06: Byte → RegisterMap → RegisterMap ≝
     
    783818  let old_register_DPL_value ≝ register_DPL_value m in
    784819  let old_register_DPH_value ≝ register_DPH_value m in
    785     mk_RegisterMap old_register_00_value
    786                    old_register_01_value
    787                    old_register_02_value
    788                    old_register_03_value
    789                    old_register_04_value
    790                    old_register_05_value
    791                    (Some ? b)
    792                    old_register_07_value
    793                    old_register_10_value
    794                    old_register_11_value
    795                    old_register_12_value
    796                    old_register_13_value
    797                    old_register_14_value
    798                    old_register_15_value
    799                    old_register_16_value
    800                    old_register_17_value
    801                    old_register_20_value
    802                    old_register_21_value
    803                    old_register_22_value
    804                    old_register_23_value
    805                    old_register_24_value
    806                    old_register_25_value
    807                    old_register_26_value
    808                    old_register_27_value
    809                    old_register_30_value
    810                    old_register_31_value
    811                    old_register_32_value
    812                    old_register_33_value
    813                    old_register_34_value
    814                    old_register_35_value
    815                    old_register_36_value
    816                    old_register_37_value
    817                    old_register_A_value
    818                    old_register_B_value
    819                    old_register_DPL_value
    820                    old_register_DPH_value.
     820  let old_register_Carry_value ≝ register_Carry_value m in
     821    mk_RegisterMap old_register_00_value
     822                   old_register_01_value
     823                   old_register_02_value
     824                   old_register_03_value
     825                   old_register_04_value
     826                   old_register_05_value
     827                   (Some ? b)
     828                   old_register_07_value
     829                   old_register_10_value
     830                   old_register_11_value
     831                   old_register_12_value
     832                   old_register_13_value
     833                   old_register_14_value
     834                   old_register_15_value
     835                   old_register_16_value
     836                   old_register_17_value
     837                   old_register_20_value
     838                   old_register_21_value
     839                   old_register_22_value
     840                   old_register_23_value
     841                   old_register_24_value
     842                   old_register_25_value
     843                   old_register_26_value
     844                   old_register_27_value
     845                   old_register_30_value
     846                   old_register_31_value
     847                   old_register_32_value
     848                   old_register_33_value
     849                   old_register_34_value
     850                   old_register_35_value
     851                   old_register_36_value
     852                   old_register_37_value
     853                   old_register_A_value
     854                   old_register_B_value
     855                   old_register_DPL_value
     856                   old_register_DPH_value
     857                   old_register_Carry_value.
    821858
    822859definition update_register_07: Byte → RegisterMap → RegisterMap ≝
     
    859896  let old_register_DPL_value ≝ register_DPL_value m in
    860897  let old_register_DPH_value ≝ register_DPH_value m in
    861     mk_RegisterMap old_register_00_value
    862                    old_register_01_value
    863                    old_register_02_value
    864                    old_register_03_value
    865                    old_register_04_value
    866                    old_register_05_value
    867                    old_register_06_value
    868                    (Some ? b)
    869                    old_register_10_value
    870                    old_register_11_value
    871                    old_register_12_value
    872                    old_register_13_value
    873                    old_register_14_value
    874                    old_register_15_value
    875                    old_register_16_value
    876                    old_register_17_value
    877                    old_register_20_value
    878                    old_register_21_value
    879                    old_register_22_value
    880                    old_register_23_value
    881                    old_register_24_value
    882                    old_register_25_value
    883                    old_register_26_value
    884                    old_register_27_value
    885                    old_register_30_value
    886                    old_register_31_value
    887                    old_register_32_value
    888                    old_register_33_value
    889                    old_register_34_value
    890                    old_register_35_value
    891                    old_register_36_value
    892                    old_register_37_value
    893                    old_register_A_value
    894                    old_register_B_value
    895                    old_register_DPL_value
    896                    old_register_DPH_value.
     898  let old_register_Carry_value ≝ register_Carry_value m in
     899    mk_RegisterMap old_register_00_value
     900                   old_register_01_value
     901                   old_register_02_value
     902                   old_register_03_value
     903                   old_register_04_value
     904                   old_register_05_value
     905                   old_register_06_value
     906                   (Some ? b)
     907                   old_register_10_value
     908                   old_register_11_value
     909                   old_register_12_value
     910                   old_register_13_value
     911                   old_register_14_value
     912                   old_register_15_value
     913                   old_register_16_value
     914                   old_register_17_value
     915                   old_register_20_value
     916                   old_register_21_value
     917                   old_register_22_value
     918                   old_register_23_value
     919                   old_register_24_value
     920                   old_register_25_value
     921                   old_register_26_value
     922                   old_register_27_value
     923                   old_register_30_value
     924                   old_register_31_value
     925                   old_register_32_value
     926                   old_register_33_value
     927                   old_register_34_value
     928                   old_register_35_value
     929                   old_register_36_value
     930                   old_register_37_value
     931                   old_register_A_value
     932                   old_register_B_value
     933                   old_register_DPL_value
     934                   old_register_DPH_value
     935                   old_register_Carry_value.
    897936
    898937definition update_register_10: Byte → RegisterMap → RegisterMap ≝
     
    935974  let old_register_DPL_value ≝ register_DPL_value m in
    936975  let old_register_DPH_value ≝ register_DPH_value m in
    937     mk_RegisterMap old_register_00_value
    938                    old_register_01_value
    939                    old_register_02_value
    940                    old_register_03_value
    941                    old_register_04_value
    942                    old_register_05_value
    943                    old_register_06_value
    944                    old_register_07_value
    945                    (Some ? b)
    946                    old_register_11_value
    947                    old_register_12_value
    948                    old_register_13_value
    949                    old_register_14_value
    950                    old_register_15_value
    951                    old_register_16_value
    952                    old_register_17_value
    953                    old_register_20_value
    954                    old_register_21_value
    955                    old_register_22_value
    956                    old_register_23_value
    957                    old_register_24_value
    958                    old_register_25_value
    959                    old_register_26_value
    960                    old_register_27_value
    961                    old_register_30_value
    962                    old_register_31_value
    963                    old_register_32_value
    964                    old_register_33_value
    965                    old_register_34_value
    966                    old_register_35_value
    967                    old_register_36_value
    968                    old_register_37_value
    969                    old_register_A_value
    970                    old_register_B_value
    971                    old_register_DPL_value
    972                    old_register_DPH_value.
     976  let old_register_Carry_value ≝ register_Carry_value m in
     977    mk_RegisterMap old_register_00_value
     978                   old_register_01_value
     979                   old_register_02_value
     980                   old_register_03_value
     981                   old_register_04_value
     982                   old_register_05_value
     983                   old_register_06_value
     984                   old_register_07_value
     985                   (Some ? b)
     986                   old_register_11_value
     987                   old_register_12_value
     988                   old_register_13_value
     989                   old_register_14_value
     990                   old_register_15_value
     991                   old_register_16_value
     992                   old_register_17_value
     993                   old_register_20_value
     994                   old_register_21_value
     995                   old_register_22_value
     996                   old_register_23_value
     997                   old_register_24_value
     998                   old_register_25_value
     999                   old_register_26_value
     1000                   old_register_27_value
     1001                   old_register_30_value
     1002                   old_register_31_value
     1003                   old_register_32_value
     1004                   old_register_33_value
     1005                   old_register_34_value
     1006                   old_register_35_value
     1007                   old_register_36_value
     1008                   old_register_37_value
     1009                   old_register_A_value
     1010                   old_register_B_value
     1011                   old_register_DPL_value
     1012                   old_register_DPH_value
     1013                   old_register_Carry_value.
    9731014
    9741015definition update_register_11: Byte → RegisterMap → RegisterMap ≝
     
    10111052  let old_register_DPL_value ≝ register_DPL_value m in
    10121053  let old_register_DPH_value ≝ register_DPH_value m in
    1013     mk_RegisterMap old_register_00_value
    1014                    old_register_01_value
    1015                    old_register_02_value
    1016                    old_register_03_value
    1017                    old_register_04_value
    1018                    old_register_05_value
    1019                    old_register_06_value
    1020                    old_register_07_value
    1021                    old_register_10_value
    1022                    (Some ? b)
    1023                    old_register_12_value
    1024                    old_register_13_value
    1025                    old_register_14_value
    1026                    old_register_15_value
    1027                    old_register_16_value
    1028                    old_register_17_value
    1029                    old_register_20_value
    1030                    old_register_21_value
    1031                    old_register_22_value
    1032                    old_register_23_value
    1033                    old_register_24_value
    1034                    old_register_25_value
    1035                    old_register_26_value
    1036                    old_register_27_value
    1037                    old_register_30_value
    1038                    old_register_31_value
    1039                    old_register_32_value
    1040                    old_register_33_value
    1041                    old_register_34_value
    1042                    old_register_35_value
    1043                    old_register_36_value
    1044                    old_register_37_value
    1045                    old_register_A_value
    1046                    old_register_B_value
    1047                    old_register_DPL_value
    1048                    old_register_DPH_value.
     1054  let old_register_Carry_value ≝ register_Carry_value m in
     1055    mk_RegisterMap old_register_00_value
     1056                   old_register_01_value
     1057                   old_register_02_value
     1058                   old_register_03_value
     1059                   old_register_04_value
     1060                   old_register_05_value
     1061                   old_register_06_value
     1062                   old_register_07_value
     1063                   old_register_10_value
     1064                   (Some ? b)
     1065                   old_register_12_value
     1066                   old_register_13_value
     1067                   old_register_14_value
     1068                   old_register_15_value
     1069                   old_register_16_value
     1070                   old_register_17_value
     1071                   old_register_20_value
     1072                   old_register_21_value
     1073                   old_register_22_value
     1074                   old_register_23_value
     1075                   old_register_24_value
     1076                   old_register_25_value
     1077                   old_register_26_value
     1078                   old_register_27_value
     1079                   old_register_30_value
     1080                   old_register_31_value
     1081                   old_register_32_value
     1082                   old_register_33_value
     1083                   old_register_34_value
     1084                   old_register_35_value
     1085                   old_register_36_value
     1086                   old_register_37_value
     1087                   old_register_A_value
     1088                   old_register_B_value
     1089                   old_register_DPL_value
     1090                   old_register_DPH_value
     1091                   old_register_Carry_value.
    10491092
    10501093definition update_register_12: Byte → RegisterMap → RegisterMap ≝
     
    10871130  let old_register_DPL_value ≝ register_DPL_value m in
    10881131  let old_register_DPH_value ≝ register_DPH_value m in
    1089     mk_RegisterMap old_register_00_value
    1090                    old_register_01_value
    1091                    old_register_02_value
    1092                    old_register_03_value
    1093                    old_register_04_value
    1094                    old_register_05_value
    1095                    old_register_06_value
    1096                    old_register_07_value
    1097                    old_register_10_value
    1098                    old_register_11_value
    1099                    (Some ? b)
    1100                    old_register_13_value
    1101                    old_register_14_value
    1102                    old_register_15_value
    1103                    old_register_16_value
    1104                    old_register_17_value
    1105                    old_register_20_value
    1106                    old_register_21_value
    1107                    old_register_22_value
    1108                    old_register_23_value
    1109                    old_register_24_value
    1110                    old_register_25_value
    1111                    old_register_26_value
    1112                    old_register_27_value
    1113                    old_register_30_value
    1114                    old_register_31_value
    1115                    old_register_32_value
    1116                    old_register_33_value
    1117                    old_register_34_value
    1118                    old_register_35_value
    1119                    old_register_36_value
    1120                    old_register_37_value
    1121                    old_register_A_value
    1122                    old_register_B_value
    1123                    old_register_DPL_value
    1124                    old_register_DPH_value.
     1132  let old_register_Carry_value ≝ register_Carry_value m in
     1133    mk_RegisterMap old_register_00_value
     1134                   old_register_01_value
     1135                   old_register_02_value
     1136                   old_register_03_value
     1137                   old_register_04_value
     1138                   old_register_05_value
     1139                   old_register_06_value
     1140                   old_register_07_value
     1141                   old_register_10_value
     1142                   old_register_11_value
     1143                   (Some ? b)
     1144                   old_register_13_value
     1145                   old_register_14_value
     1146                   old_register_15_value
     1147                   old_register_16_value
     1148                   old_register_17_value
     1149                   old_register_20_value
     1150                   old_register_21_value
     1151                   old_register_22_value
     1152                   old_register_23_value
     1153                   old_register_24_value
     1154                   old_register_25_value
     1155                   old_register_26_value
     1156                   old_register_27_value
     1157                   old_register_30_value
     1158                   old_register_31_value
     1159                   old_register_32_value
     1160                   old_register_33_value
     1161                   old_register_34_value
     1162                   old_register_35_value
     1163                   old_register_36_value
     1164                   old_register_37_value
     1165                   old_register_A_value
     1166                   old_register_B_value
     1167                   old_register_DPL_value
     1168                   old_register_DPH_value
     1169                   old_register_Carry_value.
    11251170
    11261171definition update_register_13: Byte → RegisterMap → RegisterMap ≝
     
    11631208  let old_register_DPL_value ≝ register_DPL_value m in
    11641209  let old_register_DPH_value ≝ register_DPH_value m in
    1165     mk_RegisterMap old_register_00_value
    1166                    old_register_01_value
    1167                    old_register_02_value
    1168                    old_register_03_value
    1169                    old_register_04_value
    1170                    old_register_05_value
    1171                    old_register_06_value
    1172                    old_register_07_value
    1173                    old_register_10_value
    1174                    old_register_11_value
    1175                    old_register_12_value
    1176                    (Some ? b)
    1177                    old_register_14_value
    1178                    old_register_15_value
    1179                    old_register_16_value
    1180                    old_register_17_value
    1181                    old_register_20_value
    1182                    old_register_21_value
    1183                    old_register_22_value
    1184                    old_register_23_value
    1185                    old_register_24_value
    1186                    old_register_25_value
    1187                    old_register_26_value
    1188                    old_register_27_value
    1189                    old_register_30_value
    1190                    old_register_31_value
    1191                    old_register_32_value
    1192                    old_register_33_value
    1193                    old_register_34_value
    1194                    old_register_35_value
    1195                    old_register_36_value
    1196                    old_register_37_value
    1197                    old_register_A_value
    1198                    old_register_B_value
    1199                    old_register_DPL_value
    1200                    old_register_DPH_value.
     1210  let old_register_Carry_value ≝ register_Carry_value m in
     1211    mk_RegisterMap old_register_00_value
     1212                   old_register_01_value
     1213                   old_register_02_value
     1214                   old_register_03_value
     1215                   old_register_04_value
     1216                   old_register_05_value
     1217                   old_register_06_value
     1218                   old_register_07_value
     1219                   old_register_10_value
     1220                   old_register_11_value
     1221                   old_register_12_value
     1222                   (Some ? b)
     1223                   old_register_14_value
     1224                   old_register_15_value
     1225                   old_register_16_value
     1226                   old_register_17_value
     1227                   old_register_20_value
     1228                   old_register_21_value
     1229                   old_register_22_value
     1230                   old_register_23_value
     1231                   old_register_24_value
     1232                   old_register_25_value
     1233                   old_register_26_value
     1234                   old_register_27_value
     1235                   old_register_30_value
     1236                   old_register_31_value
     1237                   old_register_32_value
     1238                   old_register_33_value
     1239                   old_register_34_value
     1240                   old_register_35_value
     1241                   old_register_36_value
     1242                   old_register_37_value
     1243                   old_register_A_value
     1244                   old_register_B_value
     1245                   old_register_DPL_value
     1246                   old_register_DPH_value
     1247                   old_register_Carry_value.
    12011248
    12021249definition update_register_14: Byte → RegisterMap → RegisterMap ≝
     
    12391286  let old_register_DPL_value ≝ register_DPL_value m in
    12401287  let old_register_DPH_value ≝ register_DPH_value m in
    1241     mk_RegisterMap old_register_00_value
    1242                    old_register_01_value
    1243                    old_register_02_value
    1244                    old_register_03_value
    1245                    old_register_04_value
    1246                    old_register_05_value
    1247                    old_register_06_value
    1248                    old_register_07_value
    1249                    old_register_10_value
    1250                    old_register_11_value
    1251                    old_register_12_value
    1252                    old_register_13_value
    1253                    (Some ? b)
    1254                    old_register_15_value
    1255                    old_register_16_value
    1256                    old_register_17_value
    1257                    old_register_20_value
    1258                    old_register_21_value
    1259                    old_register_22_value
    1260                    old_register_23_value
    1261                    old_register_24_value
    1262                    old_register_25_value
    1263                    old_register_26_value
    1264                    old_register_27_value
    1265                    old_register_30_value
    1266                    old_register_31_value
    1267                    old_register_32_value
    1268                    old_register_33_value
    1269                    old_register_34_value
    1270                    old_register_35_value
    1271                    old_register_36_value
    1272                    old_register_37_value
    1273                    old_register_A_value
    1274                    old_register_B_value
    1275                    old_register_DPL_value
    1276                    old_register_DPH_value.
     1288  let old_register_Carry_value ≝ register_Carry_value m in
     1289    mk_RegisterMap old_register_00_value
     1290                   old_register_01_value
     1291                   old_register_02_value
     1292                   old_register_03_value
     1293                   old_register_04_value
     1294                   old_register_05_value
     1295                   old_register_06_value
     1296                   old_register_07_value
     1297                   old_register_10_value
     1298                   old_register_11_value
     1299                   old_register_12_value
     1300                   old_register_13_value
     1301                   (Some ? b)
     1302                   old_register_15_value
     1303                   old_register_16_value
     1304                   old_register_17_value
     1305                   old_register_20_value
     1306                   old_register_21_value
     1307                   old_register_22_value
     1308                   old_register_23_value
     1309                   old_register_24_value
     1310                   old_register_25_value
     1311                   old_register_26_value
     1312                   old_register_27_value
     1313                   old_register_30_value
     1314                   old_register_31_value
     1315                   old_register_32_value
     1316                   old_register_33_value
     1317                   old_register_34_value
     1318                   old_register_35_value
     1319                   old_register_36_value
     1320                   old_register_37_value
     1321                   old_register_A_value
     1322                   old_register_B_value
     1323                   old_register_DPL_value
     1324                   old_register_DPH_value
     1325                   old_register_Carry_value.
    12771326
    12781327definition update_register_15: Byte → RegisterMap → RegisterMap ≝
     
    13151364  let old_register_DPL_value ≝ register_DPL_value m in
    13161365  let old_register_DPH_value ≝ register_DPH_value m in
    1317     mk_RegisterMap old_register_00_value
    1318                    old_register_01_value
    1319                    old_register_02_value
    1320                    old_register_03_value
    1321                    old_register_04_value
    1322                    old_register_05_value
    1323                    old_register_06_value
    1324                    old_register_07_value
    1325                    old_register_10_value
    1326                    old_register_11_value
    1327                    old_register_12_value
    1328                    old_register_13_value
    1329                    old_register_14_value
    1330                    (Some ? b)
    1331                    old_register_16_value
    1332                    old_register_17_value
    1333                    old_register_20_value
    1334                    old_register_21_value
    1335                    old_register_22_value
    1336                    old_register_23_value
    1337                    old_register_24_value
    1338                    old_register_25_value
    1339                    old_register_26_value
    1340                    old_register_27_value
    1341                    old_register_30_value
    1342                    old_register_31_value
    1343                    old_register_32_value
    1344                    old_register_33_value
    1345                    old_register_34_value
    1346                    old_register_35_value
    1347                    old_register_36_value
    1348                    old_register_37_value
    1349                    old_register_A_value
    1350                    old_register_B_value
    1351                    old_register_DPL_value
    1352                    old_register_DPH_value.
     1366  let old_register_Carry_value ≝ register_Carry_value m in
     1367    mk_RegisterMap old_register_00_value
     1368                   old_register_01_value
     1369                   old_register_02_value
     1370                   old_register_03_value
     1371                   old_register_04_value
     1372                   old_register_05_value
     1373                   old_register_06_value
     1374                   old_register_07_value
     1375                   old_register_10_value
     1376                   old_register_11_value
     1377                   old_register_12_value
     1378                   old_register_13_value
     1379                   old_register_14_value
     1380                   (Some ? b)
     1381                   old_register_16_value
     1382                   old_register_17_value
     1383                   old_register_20_value
     1384                   old_register_21_value
     1385                   old_register_22_value
     1386                   old_register_23_value
     1387                   old_register_24_value
     1388                   old_register_25_value
     1389                   old_register_26_value
     1390                   old_register_27_value
     1391                   old_register_30_value
     1392                   old_register_31_value
     1393                   old_register_32_value
     1394                   old_register_33_value
     1395                   old_register_34_value
     1396                   old_register_35_value
     1397                   old_register_36_value
     1398                   old_register_37_value
     1399                   old_register_A_value
     1400                   old_register_B_value
     1401                   old_register_DPL_value
     1402                   old_register_DPH_value
     1403                   old_register_Carry_value.
    13531404
    13541405definition update_register_16: Byte → RegisterMap → RegisterMap ≝
     
    13911442  let old_register_DPL_value ≝ register_DPL_value m in
    13921443  let old_register_DPH_value ≝ register_DPH_value m in
    1393     mk_RegisterMap old_register_00_value
    1394                    old_register_01_value
    1395                    old_register_02_value
    1396                    old_register_03_value
    1397                    old_register_04_value
    1398                    old_register_05_value
    1399                    old_register_06_value
    1400                    old_register_07_value
    1401                    old_register_10_value
    1402                    old_register_11_value
    1403                    old_register_12_value
    1404                    old_register_13_value
    1405                    old_register_14_value
    1406                    old_register_15_value
    1407                    (Some ? b)
    1408                    old_register_17_value
    1409                    old_register_20_value
    1410                    old_register_21_value
    1411                    old_register_22_value
    1412                    old_register_23_value
    1413                    old_register_24_value
    1414                    old_register_25_value
    1415                    old_register_26_value
    1416                    old_register_27_value
    1417                    old_register_30_value
    1418                    old_register_31_value
    1419                    old_register_32_value
    1420                    old_register_33_value
    1421                    old_register_34_value
    1422                    old_register_35_value
    1423                    old_register_36_value
    1424                    old_register_37_value
    1425                    old_register_A_value
    1426                    old_register_B_value
    1427                    old_register_DPL_value
    1428                    old_register_DPH_value.
     1444  let old_register_Carry_value ≝ register_Carry_value m in
     1445    mk_RegisterMap old_register_00_value
     1446                   old_register_01_value
     1447                   old_register_02_value
     1448                   old_register_03_value
     1449                   old_register_04_value
     1450                   old_register_05_value
     1451                   old_register_06_value
     1452                   old_register_07_value
     1453                   old_register_10_value
     1454                   old_register_11_value
     1455                   old_register_12_value
     1456                   old_register_13_value
     1457                   old_register_14_value
     1458                   old_register_15_value
     1459                   (Some ? b)
     1460                   old_register_17_value
     1461                   old_register_20_value
     1462                   old_register_21_value
     1463                   old_register_22_value
     1464                   old_register_23_value
     1465                   old_register_24_value
     1466                   old_register_25_value
     1467                   old_register_26_value
     1468                   old_register_27_value
     1469                   old_register_30_value
     1470                   old_register_31_value
     1471                   old_register_32_value
     1472                   old_register_33_value
     1473                   old_register_34_value
     1474                   old_register_35_value
     1475                   old_register_36_value
     1476                   old_register_37_value
     1477                   old_register_A_value
     1478                   old_register_B_value
     1479                   old_register_DPL_value
     1480                   old_register_DPH_value
     1481                   old_register_Carry_value.
    14291482
    14301483definition update_register_17: Byte → RegisterMap → RegisterMap ≝
     
    14671520  let old_register_DPL_value ≝ register_DPL_value m in
    14681521  let old_register_DPH_value ≝ register_DPH_value m in
    1469     mk_RegisterMap old_register_00_value
    1470                    old_register_01_value
    1471                    old_register_02_value
    1472                    old_register_03_value
    1473                    old_register_04_value
    1474                    old_register_05_value
    1475                    old_register_06_value
    1476                    old_register_07_value
    1477                    old_register_10_value
    1478                    old_register_11_value
    1479                    old_register_12_value
    1480                    old_register_13_value
    1481                    old_register_14_value
    1482                    old_register_15_value
    1483                    old_register_16_value
    1484                    (Some ? b)
    1485                    old_register_20_value
    1486                    old_register_21_value
    1487                    old_register_22_value
    1488                    old_register_23_value
    1489                    old_register_24_value
    1490                    old_register_25_value
    1491                    old_register_26_value
    1492                    old_register_27_value
    1493                    old_register_30_value
    1494                    old_register_31_value
    1495                    old_register_32_value
    1496                    old_register_33_value
    1497                    old_register_34_value
    1498                    old_register_35_value
    1499                    old_register_36_value
    1500                    old_register_37_value
    1501                    old_register_A_value
    1502                    old_register_B_value
    1503                    old_register_DPL_value
    1504                    old_register_DPH_value.
     1522  let old_register_Carry_value ≝ register_Carry_value m in
     1523    mk_RegisterMap old_register_00_value
     1524                   old_register_01_value
     1525                   old_register_02_value
     1526                   old_register_03_value
     1527                   old_register_04_value
     1528                   old_register_05_value
     1529                   old_register_06_value
     1530                   old_register_07_value
     1531                   old_register_10_value
     1532                   old_register_11_value
     1533                   old_register_12_value
     1534                   old_register_13_value
     1535                   old_register_14_value
     1536                   old_register_15_value
     1537                   old_register_16_value
     1538                   (Some ? b)
     1539                   old_register_20_value
     1540                   old_register_21_value
     1541                   old_register_22_value
     1542                   old_register_23_value
     1543                   old_register_24_value
     1544                   old_register_25_value
     1545                   old_register_26_value
     1546                   old_register_27_value
     1547                   old_register_30_value
     1548                   old_register_31_value
     1549                   old_register_32_value
     1550                   old_register_33_value
     1551                   old_register_34_value
     1552                   old_register_35_value
     1553                   old_register_36_value
     1554                   old_register_37_value
     1555                   old_register_A_value
     1556                   old_register_B_value
     1557                   old_register_DPL_value
     1558                   old_register_DPH_value
     1559                   old_register_Carry_value.
    15051560
    15061561definition update_register_20: Byte → RegisterMap → RegisterMap ≝
     
    15431598  let old_register_DPL_value ≝ register_DPL_value m in
    15441599  let old_register_DPH_value ≝ register_DPH_value m in
    1545     mk_RegisterMap old_register_00_value
    1546                    old_register_01_value
    1547                    old_register_02_value
    1548                    old_register_03_value
    1549                    old_register_04_value
    1550                    old_register_05_value
    1551                    old_register_06_value
    1552                    old_register_07_value
    1553                    old_register_10_value
    1554                    old_register_11_value
    1555                    old_register_12_value
    1556                    old_register_13_value
    1557                    old_register_14_value
    1558                    old_register_15_value
    1559                    old_register_16_value
    1560                    old_register_17_value
    1561                    (Some ? b)
    1562                    old_register_21_value
    1563                    old_register_22_value
    1564                    old_register_23_value
    1565                    old_register_24_value
    1566                    old_register_25_value
    1567                    old_register_26_value
    1568                    old_register_27_value
    1569                    old_register_30_value
    1570                    old_register_31_value
    1571                    old_register_32_value
    1572                    old_register_33_value
    1573                    old_register_34_value
    1574                    old_register_35_value
    1575                    old_register_36_value
    1576                    old_register_37_value
    1577                    old_register_A_value
    1578                    old_register_B_value
    1579                    old_register_DPL_value
    1580                    old_register_DPH_value.
     1600  let old_register_Carry_value ≝ register_Carry_value m in
     1601    mk_RegisterMap old_register_00_value
     1602                   old_register_01_value
     1603                   old_register_02_value
     1604                   old_register_03_value
     1605                   old_register_04_value
     1606                   old_register_05_value
     1607                   old_register_06_value
     1608                   old_register_07_value
     1609                   old_register_10_value
     1610                   old_register_11_value
     1611                   old_register_12_value
     1612                   old_register_13_value
     1613                   old_register_14_value
     1614                   old_register_15_value
     1615                   old_register_16_value
     1616                   old_register_17_value
     1617                   (Some ? b)
     1618                   old_register_21_value
     1619                   old_register_22_value
     1620                   old_register_23_value
     1621                   old_register_24_value
     1622                   old_register_25_value
     1623                   old_register_26_value
     1624                   old_register_27_value
     1625                   old_register_30_value
     1626                   old_register_31_value
     1627                   old_register_32_value
     1628                   old_register_33_value
     1629                   old_register_34_value
     1630                   old_register_35_value
     1631                   old_register_36_value
     1632                   old_register_37_value
     1633                   old_register_A_value
     1634                   old_register_B_value
     1635                   old_register_DPL_value
     1636                   old_register_DPH_value
     1637                   old_register_Carry_value.
    15811638
    15821639definition update_register_21: Byte → RegisterMap → RegisterMap ≝
     
    16191676  let old_register_DPL_value ≝ register_DPL_value m in
    16201677  let old_register_DPH_value ≝ register_DPH_value m in
    1621     mk_RegisterMap old_register_00_value
    1622                    old_register_01_value
    1623                    old_register_02_value
    1624                    old_register_03_value
    1625                    old_register_04_value
    1626                    old_register_05_value
    1627                    old_register_06_value
    1628                    old_register_07_value
    1629                    old_register_10_value
    1630                    old_register_11_value
    1631                    old_register_12_value
    1632                    old_register_13_value
    1633                    old_register_14_value
    1634                    old_register_15_value
    1635                    old_register_16_value
    1636                    old_register_17_value
    1637                    old_register_20_value
    1638                    (Some ? b)
    1639                    old_register_22_value
    1640                    old_register_23_value
    1641                    old_register_24_value
    1642                    old_register_25_value
    1643                    old_register_26_value
    1644                    old_register_27_value
    1645                    old_register_30_value
    1646                    old_register_31_value
    1647                    old_register_32_value
    1648                    old_register_33_value
    1649                    old_register_34_value
    1650                    old_register_35_value
    1651                    old_register_36_value
    1652                    old_register_37_value
    1653                    old_register_A_value
    1654                    old_register_B_value
    1655                    old_register_DPL_value
    1656                    old_register_DPH_value.
     1678  let old_register_Carry_value ≝ register_Carry_value m in
     1679    mk_RegisterMap old_register_00_value
     1680                   old_register_01_value
     1681                   old_register_02_value
     1682                   old_register_03_value
     1683                   old_register_04_value
     1684                   old_register_05_value
     1685                   old_register_06_value
     1686                   old_register_07_value
     1687                   old_register_10_value
     1688                   old_register_11_value
     1689                   old_register_12_value
     1690                   old_register_13_value
     1691                   old_register_14_value
     1692                   old_register_15_value
     1693                   old_register_16_value
     1694                   old_register_17_value
     1695                   old_register_20_value
     1696                   (Some ? b)
     1697                   old_register_22_value
     1698                   old_register_23_value
     1699                   old_register_24_value
     1700                   old_register_25_value
     1701                   old_register_26_value
     1702                   old_register_27_value
     1703                   old_register_30_value
     1704                   old_register_31_value
     1705                   old_register_32_value
     1706                   old_register_33_value
     1707                   old_register_34_value
     1708                   old_register_35_value
     1709                   old_register_36_value
     1710                   old_register_37_value
     1711                   old_register_A_value
     1712                   old_register_B_value
     1713                   old_register_DPL_value
     1714                   old_register_DPH_value
     1715                   old_register_Carry_value.
    16571716
    16581717definition update_register_22: Byte → RegisterMap → RegisterMap ≝
     
    16951754  let old_register_DPL_value ≝ register_DPL_value m in
    16961755  let old_register_DPH_value ≝ register_DPH_value m in
    1697     mk_RegisterMap old_register_00_value
    1698                    old_register_01_value
    1699                    old_register_02_value
    1700                    old_register_03_value
    1701                    old_register_04_value
    1702                    old_register_05_value
    1703                    old_register_06_value
    1704                    old_register_07_value
    1705                    old_register_10_value
    1706                    old_register_11_value
    1707                    old_register_12_value
    1708                    old_register_13_value
    1709                    old_register_14_value
    1710                    old_register_15_value
    1711                    old_register_16_value
    1712                    old_register_17_value
    1713                    old_register_20_value
    1714                    old_register_21_value
    1715                    (Some ? b)
    1716                    old_register_23_value
    1717                    old_register_24_value
    1718                    old_register_25_value
    1719                    old_register_26_value
    1720                    old_register_27_value
    1721                    old_register_30_value
    1722                    old_register_31_value
    1723                    old_register_32_value
    1724                    old_register_33_value
    1725                    old_register_34_value
    1726                    old_register_35_value
    1727                    old_register_36_value
    1728                    old_register_37_value
    1729                    old_register_A_value
    1730                    old_register_B_value
    1731                    old_register_DPL_value
    1732                    old_register_DPH_value.
     1756  let old_register_Carry_value ≝ register_Carry_value m in
     1757    mk_RegisterMap old_register_00_value
     1758                   old_register_01_value
     1759                   old_register_02_value
     1760                   old_register_03_value
     1761                   old_register_04_value
     1762                   old_register_05_value
     1763                   old_register_06_value
     1764                   old_register_07_value
     1765                   old_register_10_value
     1766                   old_register_11_value
     1767                   old_register_12_value
     1768                   old_register_13_value
     1769                   old_register_14_value
     1770                   old_register_15_value
     1771                   old_register_16_value
     1772                   old_register_17_value
     1773                   old_register_20_value
     1774                   old_register_21_value
     1775                   (Some ? b)
     1776                   old_register_23_value
     1777                   old_register_24_value
     1778                   old_register_25_value
     1779                   old_register_26_value
     1780                   old_register_27_value
     1781                   old_register_30_value
     1782                   old_register_31_value
     1783                   old_register_32_value
     1784                   old_register_33_value
     1785                   old_register_34_value
     1786                   old_register_35_value
     1787                   old_register_36_value
     1788                   old_register_37_value
     1789                   old_register_A_value
     1790                   old_register_B_value
     1791                   old_register_DPL_value
     1792                   old_register_DPH_value
     1793                   old_register_Carry_value.
    17331794                   
    17341795definition update_register_23: Byte → RegisterMap → RegisterMap ≝
     
    17711832  let old_register_DPL_value ≝ register_DPL_value m in
    17721833  let old_register_DPH_value ≝ register_DPH_value m in
    1773     mk_RegisterMap old_register_00_value
    1774                    old_register_01_value
    1775                    old_register_02_value
    1776                    old_register_03_value
    1777                    old_register_04_value
    1778                    old_register_05_value
    1779                    old_register_06_value
    1780                    old_register_07_value
    1781                    old_register_10_value
    1782                    old_register_11_value
    1783                    old_register_12_value
    1784                    old_register_13_value
    1785                    old_register_14_value
    1786                    old_register_15_value
    1787                    old_register_16_value
    1788                    old_register_17_value
    1789                    old_register_20_value
    1790                    old_register_21_value
    1791                    old_register_22_value
    1792                    (Some ? b)
    1793                    old_register_24_value
    1794                    old_register_25_value
    1795                    old_register_26_value
    1796                    old_register_27_value
    1797                    old_register_30_value
    1798                    old_register_31_value
    1799                    old_register_32_value
    1800                    old_register_33_value
    1801                    old_register_34_value
    1802                    old_register_35_value
    1803                    old_register_36_value
    1804                    old_register_37_value
    1805                    old_register_A_value
    1806                    old_register_B_value
    1807                    old_register_DPL_value
    1808                    old_register_DPH_value.
     1834  let old_register_Carry_value ≝ register_Carry_value m in
     1835    mk_RegisterMap old_register_00_value
     1836                   old_register_01_value
     1837                   old_register_02_value
     1838                   old_register_03_value
     1839                   old_register_04_value
     1840                   old_register_05_value
     1841                   old_register_06_value
     1842                   old_register_07_value
     1843                   old_register_10_value
     1844                   old_register_11_value
     1845                   old_register_12_value
     1846                   old_register_13_value
     1847                   old_register_14_value
     1848                   old_register_15_value
     1849                   old_register_16_value
     1850                   old_register_17_value
     1851                   old_register_20_value
     1852                   old_register_21_value
     1853                   old_register_22_value
     1854                   (Some ? b)
     1855                   old_register_24_value
     1856                   old_register_25_value
     1857                   old_register_26_value
     1858                   old_register_27_value
     1859                   old_register_30_value
     1860                   old_register_31_value
     1861                   old_register_32_value
     1862                   old_register_33_value
     1863                   old_register_34_value
     1864                   old_register_35_value
     1865                   old_register_36_value
     1866                   old_register_37_value
     1867                   old_register_A_value
     1868                   old_register_B_value
     1869                   old_register_DPL_value
     1870                   old_register_DPH_value
     1871                   old_register_Carry_value.
    18091872                   
    18101873definition update_register_24: Byte → RegisterMap → RegisterMap ≝
     
    18471910  let old_register_DPL_value ≝ register_DPL_value m in
    18481911  let old_register_DPH_value ≝ register_DPH_value m in
    1849     mk_RegisterMap old_register_00_value
    1850                    old_register_01_value
    1851                    old_register_02_value
    1852                    old_register_03_value
    1853                    old_register_04_value
    1854                    old_register_05_value
    1855                    old_register_06_value
    1856                    old_register_07_value
    1857                    old_register_10_value
    1858                    old_register_11_value
    1859                    old_register_12_value
    1860                    old_register_13_value
    1861                    old_register_14_value
    1862                    old_register_15_value
    1863                    old_register_16_value
    1864                    old_register_17_value
    1865                    old_register_20_value
    1866                    old_register_21_value
    1867                    old_register_22_value
    1868                    old_register_23_value
    1869                    (Some ? b)
    1870                    old_register_25_value
    1871                    old_register_26_value
    1872                    old_register_27_value
    1873                    old_register_30_value
    1874                    old_register_31_value
    1875                    old_register_32_value
    1876                    old_register_33_value
    1877                    old_register_34_value
    1878                    old_register_35_value
    1879                    old_register_36_value
    1880                    old_register_37_value
    1881                    old_register_A_value
    1882                    old_register_B_value
    1883                    old_register_DPL_value
    1884                    old_register_DPH_value.
     1912  let old_register_Carry_value ≝ register_Carry_value m in
     1913    mk_RegisterMap old_register_00_value
     1914                   old_register_01_value
     1915                   old_register_02_value
     1916                   old_register_03_value
     1917                   old_register_04_value
     1918                   old_register_05_value
     1919                   old_register_06_value
     1920                   old_register_07_value
     1921                   old_register_10_value
     1922                   old_register_11_value
     1923                   old_register_12_value
     1924                   old_register_13_value
     1925                   old_register_14_value
     1926                   old_register_15_value
     1927                   old_register_16_value
     1928                   old_register_17_value
     1929                   old_register_20_value
     1930                   old_register_21_value
     1931                   old_register_22_value
     1932                   old_register_23_value
     1933                   (Some ? b)
     1934                   old_register_25_value
     1935                   old_register_26_value
     1936                   old_register_27_value
     1937                   old_register_30_value
     1938                   old_register_31_value
     1939                   old_register_32_value
     1940                   old_register_33_value
     1941                   old_register_34_value
     1942                   old_register_35_value
     1943                   old_register_36_value
     1944                   old_register_37_value
     1945                   old_register_A_value
     1946                   old_register_B_value
     1947                   old_register_DPL_value
     1948                   old_register_DPH_value
     1949                   old_register_Carry_value.
    18851950
    18861951definition update_register_25: Byte → RegisterMap → RegisterMap ≝
     
    19231988  let old_register_DPL_value ≝ register_DPL_value m in
    19241989  let old_register_DPH_value ≝ register_DPH_value m in
    1925     mk_RegisterMap old_register_00_value
    1926                    old_register_01_value
    1927                    old_register_02_value
    1928                    old_register_03_value
    1929                    old_register_04_value
    1930                    old_register_05_value
    1931                    old_register_06_value
    1932                    old_register_07_value
    1933                    old_register_10_value
    1934                    old_register_11_value
    1935                    old_register_12_value
    1936                    old_register_13_value
    1937                    old_register_14_value
    1938                    old_register_15_value
    1939                    old_register_16_value
    1940                    old_register_17_value
    1941                    old_register_20_value
    1942                    old_register_21_value
    1943                    old_register_22_value
    1944                    old_register_23_value
    1945                    old_register_24_value
    1946                    (Some ? b)
    1947                    old_register_26_value
    1948                    old_register_27_value
    1949                    old_register_30_value
    1950                    old_register_31_value
    1951                    old_register_32_value
    1952                    old_register_33_value
    1953                    old_register_34_value
    1954                    old_register_35_value
    1955                    old_register_36_value
    1956                    old_register_37_value
    1957                    old_register_A_value
    1958                    old_register_B_value
    1959                    old_register_DPL_value
    1960                    old_register_DPH_value.
     1990  let old_register_Carry_value ≝ register_Carry_value m in
     1991    mk_RegisterMap old_register_00_value
     1992                   old_register_01_value
     1993                   old_register_02_value
     1994                   old_register_03_value
     1995                   old_register_04_value
     1996                   old_register_05_value
     1997                   old_register_06_value
     1998                   old_register_07_value
     1999                   old_register_10_value
     2000                   old_register_11_value
     2001                   old_register_12_value
     2002                   old_register_13_value
     2003                   old_register_14_value
     2004                   old_register_15_value
     2005                   old_register_16_value
     2006                   old_register_17_value
     2007                   old_register_20_value
     2008                   old_register_21_value
     2009                   old_register_22_value
     2010                   old_register_23_value
     2011                   old_register_24_value
     2012                   (Some ? b)
     2013                   old_register_26_value
     2014                   old_register_27_value
     2015                   old_register_30_value
     2016                   old_register_31_value
     2017                   old_register_32_value
     2018                   old_register_33_value
     2019                   old_register_34_value
     2020                   old_register_35_value
     2021                   old_register_36_value
     2022                   old_register_37_value
     2023                   old_register_A_value
     2024                   old_register_B_value
     2025                   old_register_DPL_value
     2026                   old_register_DPH_value
     2027                   old_register_Carry_value.
    19612028
    19622029definition update_register_26: Byte → RegisterMap → RegisterMap ≝
     
    19992066  let old_register_DPL_value ≝ register_DPL_value m in
    20002067  let old_register_DPH_value ≝ register_DPH_value m in
    2001     mk_RegisterMap old_register_00_value
    2002                    old_register_01_value
    2003                    old_register_02_value
    2004                    old_register_03_value
    2005                    old_register_04_value
    2006                    old_register_05_value
    2007                    old_register_06_value
    2008                    old_register_07_value
    2009                    old_register_10_value
    2010                    old_register_11_value
    2011                    old_register_12_value
    2012                    old_register_13_value
    2013                    old_register_14_value
    2014                    old_register_15_value
    2015                    old_register_16_value
    2016                    old_register_17_value
    2017                    old_register_20_value
    2018                    old_register_21_value
    2019                    old_register_22_value
    2020                    old_register_23_value
    2021                    old_register_24_value
    2022                    old_register_25_value
    2023                    (Some ? b)
    2024                    old_register_27_value
    2025                    old_register_30_value
    2026                    old_register_31_value
    2027                    old_register_32_value
    2028                    old_register_33_value
    2029                    old_register_34_value
    2030                    old_register_35_value
    2031                    old_register_36_value
    2032                    old_register_37_value
    2033                    old_register_A_value
    2034                    old_register_B_value
    2035                    old_register_DPL_value
    2036                    old_register_DPH_value.
     2068  let old_register_Carry_value ≝ register_Carry_value m in
     2069    mk_RegisterMap old_register_00_value
     2070                   old_register_01_value
     2071                   old_register_02_value
     2072                   old_register_03_value
     2073                   old_register_04_value
     2074                   old_register_05_value
     2075                   old_register_06_value
     2076                   old_register_07_value
     2077                   old_register_10_value
     2078                   old_register_11_value
     2079                   old_register_12_value
     2080                   old_register_13_value
     2081                   old_register_14_value
     2082                   old_register_15_value
     2083                   old_register_16_value
     2084                   old_register_17_value
     2085                   old_register_20_value
     2086                   old_register_21_value
     2087                   old_register_22_value
     2088                   old_register_23_value
     2089                   old_register_24_value
     2090                   old_register_25_value
     2091                   (Some ? b)
     2092                   old_register_27_value
     2093                   old_register_30_value
     2094                   old_register_31_value
     2095                   old_register_32_value
     2096                   old_register_33_value
     2097                   old_register_34_value
     2098                   old_register_35_value
     2099                   old_register_36_value
     2100                   old_register_37_value
     2101                   old_register_A_value
     2102                   old_register_B_value
     2103                   old_register_DPL_value
     2104                   old_register_DPH_value
     2105                   old_register_Carry_value.
    20372106
    20382107definition update_register_27: Byte → RegisterMap → RegisterMap ≝
     
    20752144  let old_register_DPL_value ≝ register_DPL_value m in
    20762145  let old_register_DPH_value ≝ register_DPH_value m in
    2077     mk_RegisterMap old_register_00_value
    2078                    old_register_01_value
    2079                    old_register_02_value
    2080                    old_register_03_value
    2081                    old_register_04_value
    2082                    old_register_05_value
    2083                    old_register_06_value
    2084                    old_register_07_value
    2085                    old_register_10_value
    2086                    old_register_11_value
    2087                    old_register_12_value
    2088                    old_register_13_value
    2089                    old_register_14_value
    2090                    old_register_15_value
    2091                    old_register_16_value
    2092                    old_register_17_value
    2093                    old_register_20_value
    2094                    old_register_21_value
    2095                    old_register_22_value
    2096                    old_register_23_value
    2097                    old_register_24_value
    2098                    old_register_25_value
    2099                    old_register_26_value
    2100                    (Some ? b)
    2101                    old_register_30_value
    2102                    old_register_31_value
    2103                    old_register_32_value
    2104                    old_register_33_value
    2105                    old_register_34_value
    2106                    old_register_35_value
    2107                    old_register_36_value
    2108                    old_register_37_value
    2109                    old_register_A_value
    2110                    old_register_B_value
    2111                    old_register_DPL_value
    2112                    old_register_DPH_value.
     2146  let old_register_Carry_value ≝ register_Carry_value m in
     2147    mk_RegisterMap old_register_00_value
     2148                   old_register_01_value
     2149                   old_register_02_value
     2150                   old_register_03_value
     2151                   old_register_04_value
     2152                   old_register_05_value
     2153                   old_register_06_value
     2154                   old_register_07_value
     2155                   old_register_10_value
     2156                   old_register_11_value
     2157                   old_register_12_value
     2158                   old_register_13_value
     2159                   old_register_14_value
     2160                   old_register_15_value
     2161                   old_register_16_value
     2162                   old_register_17_value
     2163                   old_register_20_value
     2164                   old_register_21_value
     2165                   old_register_22_value
     2166                   old_register_23_value
     2167                   old_register_24_value
     2168                   old_register_25_value
     2169                   old_register_26_value
     2170                   (Some ? b)
     2171                   old_register_30_value
     2172                   old_register_31_value
     2173                   old_register_32_value
     2174                   old_register_33_value
     2175                   old_register_34_value
     2176                   old_register_35_value
     2177                   old_register_36_value
     2178                   old_register_37_value
     2179                   old_register_A_value
     2180                   old_register_B_value
     2181                   old_register_DPL_value
     2182                   old_register_DPH_value
     2183                   old_register_Carry_value.
    21132184
    21142185definition update_register_30: Byte → RegisterMap → RegisterMap ≝
     
    21512222  let old_register_DPL_value ≝ register_DPL_value m in
    21522223  let old_register_DPH_value ≝ register_DPH_value m in
    2153     mk_RegisterMap old_register_00_value
    2154                    old_register_01_value
    2155                    old_register_02_value
    2156                    old_register_03_value
    2157                    old_register_04_value
    2158                    old_register_05_value
    2159                    old_register_06_value
    2160                    old_register_07_value
    2161                    old_register_10_value
    2162                    old_register_11_value
    2163                    old_register_12_value
    2164                    old_register_13_value
    2165                    old_register_14_value
    2166                    old_register_15_value
    2167                    old_register_16_value
    2168                    old_register_17_value
    2169                    old_register_20_value
    2170                    old_register_21_value
    2171                    old_register_22_value
    2172                    old_register_23_value
    2173                    old_register_24_value
    2174                    old_register_25_value
    2175                    old_register_26_value
    2176                    old_register_27_value
    2177                    (Some ? b)
    2178                    old_register_31_value
    2179                    old_register_32_value
    2180                    old_register_33_value
    2181                    old_register_34_value
    2182                    old_register_35_value
    2183                    old_register_36_value
    2184                    old_register_37_value
    2185                    old_register_A_value
    2186                    old_register_B_value
    2187                    old_register_DPL_value
    2188                    old_register_DPH_value.
     2224  let old_register_Carry_value ≝ register_Carry_value m in
     2225    mk_RegisterMap old_register_00_value
     2226                   old_register_01_value
     2227                   old_register_02_value
     2228                   old_register_03_value
     2229                   old_register_04_value
     2230                   old_register_05_value
     2231                   old_register_06_value
     2232                   old_register_07_value
     2233                   old_register_10_value
     2234                   old_register_11_value
     2235                   old_register_12_value
     2236                   old_register_13_value
     2237                   old_register_14_value
     2238                   old_register_15_value
     2239                   old_register_16_value
     2240                   old_register_17_value
     2241                   old_register_20_value
     2242                   old_register_21_value
     2243                   old_register_22_value
     2244                   old_register_23_value
     2245                   old_register_24_value
     2246                   old_register_25_value
     2247                   old_register_26_value
     2248                   old_register_27_value
     2249                   (Some ? b)
     2250                   old_register_31_value
     2251                   old_register_32_value
     2252                   old_register_33_value
     2253                   old_register_34_value
     2254                   old_register_35_value
     2255                   old_register_36_value
     2256                   old_register_37_value
     2257                   old_register_A_value
     2258                   old_register_B_value
     2259                   old_register_DPL_value
     2260                   old_register_DPH_value
     2261                   old_register_Carry_value.
    21892262
    21902263definition update_register_31: Byte → RegisterMap → RegisterMap ≝
     
    22272300  let old_register_DPL_value ≝ register_DPL_value m in
    22282301  let old_register_DPH_value ≝ register_DPH_value m in
    2229     mk_RegisterMap old_register_00_value
    2230                    old_register_01_value
    2231                    old_register_02_value
    2232                    old_register_03_value
    2233                    old_register_04_value
    2234                    old_register_05_value
    2235                    old_register_06_value
    2236                    old_register_07_value
    2237                    old_register_10_value
    2238                    old_register_11_value
    2239                    old_register_12_value
    2240                    old_register_13_value
    2241                    old_register_14_value
    2242                    old_register_15_value
    2243                    old_register_16_value
    2244                    old_register_17_value
    2245                    old_register_20_value
    2246                    old_register_21_value
    2247                    old_register_22_value
    2248                    old_register_23_value
    2249                    old_register_24_value
    2250                    old_register_25_value
    2251                    old_register_26_value
    2252                    old_register_27_value
    2253                    old_register_30_value
    2254                    (Some ? b)
    2255                    old_register_32_value
    2256                    old_register_33_value
    2257                    old_register_34_value
    2258                    old_register_35_value
    2259                    old_register_36_value
    2260                    old_register_37_value
    2261                    old_register_A_value
    2262                    old_register_B_value
    2263                    old_register_DPL_value
    2264                    old_register_DPH_value.
     2302  let old_register_Carry_value ≝ register_Carry_value m in
     2303    mk_RegisterMap old_register_00_value
     2304                   old_register_01_value
     2305                   old_register_02_value
     2306                   old_register_03_value
     2307                   old_register_04_value
     2308                   old_register_05_value
     2309                   old_register_06_value
     2310                   old_register_07_value
     2311                   old_register_10_value
     2312                   old_register_11_value
     2313                   old_register_12_value
     2314                   old_register_13_value
     2315                   old_register_14_value
     2316                   old_register_15_value
     2317                   old_register_16_value
     2318                   old_register_17_value
     2319                   old_register_20_value
     2320                   old_register_21_value
     2321                   old_register_22_value
     2322                   old_register_23_value
     2323                   old_register_24_value
     2324                   old_register_25_value
     2325                   old_register_26_value
     2326                   old_register_27_value
     2327                   old_register_30_value
     2328                   (Some ? b)
     2329                   old_register_32_value
     2330                   old_register_33_value
     2331                   old_register_34_value
     2332                   old_register_35_value
     2333                   old_register_36_value
     2334                   old_register_37_value
     2335                   old_register_A_value
     2336                   old_register_B_value
     2337                   old_register_DPL_value
     2338                   old_register_DPH_value
     2339                   old_register_Carry_value.
    22652340
    22662341definition update_register_32: Byte → RegisterMap → RegisterMap ≝
     
    23032378  let old_register_DPL_value ≝ register_DPL_value m in
    23042379  let old_register_DPH_value ≝ register_DPH_value m in
    2305     mk_RegisterMap old_register_00_value
    2306                    old_register_01_value
    2307                    old_register_02_value
    2308                    old_register_03_value
    2309                    old_register_04_value
    2310                    old_register_05_value
    2311                    old_register_06_value
    2312                    old_register_07_value
    2313                    old_register_10_value
    2314                    old_register_11_value
    2315                    old_register_12_value
    2316                    old_register_13_value
    2317                    old_register_14_value
    2318                    old_register_15_value
    2319                    old_register_16_value
    2320                    old_register_17_value
    2321                    old_register_20_value
    2322                    old_register_21_value
    2323                    old_register_22_value
    2324                    old_register_23_value
    2325                    old_register_24_value
    2326                    old_register_25_value
    2327                    old_register_26_value
    2328                    old_register_27_value
    2329                    old_register_30_value
    2330                    old_register_31_value
    2331                    (Some ? b)
    2332                    old_register_33_value
    2333                    old_register_34_value
    2334                    old_register_35_value
    2335                    old_register_36_value
    2336                    old_register_37_value
    2337                    old_register_A_value
    2338                    old_register_B_value
    2339                    old_register_DPL_value
    2340                    old_register_DPH_value.
     2380  let old_register_Carry_value ≝ register_Carry_value m in
     2381    mk_RegisterMap old_register_00_value
     2382                   old_register_01_value
     2383                   old_register_02_value
     2384                   old_register_03_value
     2385                   old_register_04_value
     2386                   old_register_05_value
     2387                   old_register_06_value
     2388                   old_register_07_value
     2389                   old_register_10_value
     2390                   old_register_11_value
     2391                   old_register_12_value
     2392                   old_register_13_value
     2393                   old_register_14_value
     2394                   old_register_15_value
     2395                   old_register_16_value
     2396                   old_register_17_value
     2397                   old_register_20_value
     2398                   old_register_21_value
     2399                   old_register_22_value
     2400                   old_register_23_value
     2401                   old_register_24_value
     2402                   old_register_25_value
     2403                   old_register_26_value
     2404                   old_register_27_value
     2405                   old_register_30_value
     2406                   old_register_31_value
     2407                   (Some ? b)
     2408                   old_register_33_value
     2409                   old_register_34_value
     2410                   old_register_35_value
     2411                   old_register_36_value
     2412                   old_register_37_value
     2413                   old_register_A_value
     2414                   old_register_B_value
     2415                   old_register_DPL_value
     2416                   old_register_DPH_value
     2417                   old_register_Carry_value.
    23412418
    23422419definition update_register_33: Byte → RegisterMap → RegisterMap ≝
     
    23792456  let old_register_DPL_value ≝ register_DPL_value m in
    23802457  let old_register_DPH_value ≝ register_DPH_value m in
    2381     mk_RegisterMap old_register_00_value
    2382                    old_register_01_value
    2383                    old_register_02_value
    2384                    old_register_03_value
    2385                    old_register_04_value
    2386                    old_register_05_value
    2387                    old_register_06_value
    2388                    old_register_07_value
    2389                    old_register_10_value
    2390                    old_register_11_value
    2391                    old_register_12_value
    2392                    old_register_13_value
    2393                    old_register_14_value
    2394                    old_register_15_value
    2395                    old_register_16_value
    2396                    old_register_17_value
    2397                    old_register_20_value
    2398                    old_register_21_value
    2399                    old_register_22_value
    2400                    old_register_23_value
    2401                    old_register_24_value
    2402                    old_register_25_value
    2403                    old_register_26_value
    2404                    old_register_27_value
    2405                    old_register_30_value
    2406                    old_register_31_value
    2407                    old_register_32_value
    2408                    (Some ? b)
    2409                    old_register_34_value
    2410                    old_register_35_value
    2411                    old_register_36_value
    2412                    old_register_37_value
    2413                    old_register_A_value
    2414                    old_register_B_value
    2415                    old_register_DPL_value
    2416                    old_register_DPH_value.
     2458  let old_register_Carry_value ≝ register_Carry_value m in
     2459    mk_RegisterMap old_register_00_value
     2460                   old_register_01_value
     2461                   old_register_02_value
     2462                   old_register_03_value
     2463                   old_register_04_value
     2464                   old_register_05_value
     2465                   old_register_06_value
     2466                   old_register_07_value
     2467                   old_register_10_value
     2468                   old_register_11_value
     2469                   old_register_12_value
     2470                   old_register_13_value
     2471                   old_register_14_value
     2472                   old_register_15_value
     2473                   old_register_16_value
     2474                   old_register_17_value
     2475                   old_register_20_value
     2476                   old_register_21_value
     2477                   old_register_22_value
     2478                   old_register_23_value
     2479                   old_register_24_value
     2480                   old_register_25_value
     2481                   old_register_26_value
     2482                   old_register_27_value
     2483                   old_register_30_value
     2484                   old_register_31_value
     2485                   old_register_32_value
     2486                   (Some ? b)
     2487                   old_register_34_value
     2488                   old_register_35_value
     2489                   old_register_36_value
     2490                   old_register_37_value
     2491                   old_register_A_value
     2492                   old_register_B_value
     2493                   old_register_DPL_value
     2494                   old_register_DPH_value
     2495                   old_register_Carry_value.
    24172496
    24182497definition update_register_34: Byte → RegisterMap → RegisterMap ≝
     
    24552534  let old_register_DPL_value ≝ register_DPL_value m in
    24562535  let old_register_DPH_value ≝ register_DPH_value m in
    2457     mk_RegisterMap old_register_00_value
    2458                    old_register_01_value
    2459                    old_register_02_value
    2460                    old_register_03_value
    2461                    old_register_04_value
    2462                    old_register_05_value
    2463                    old_register_06_value
    2464                    old_register_07_value
    2465                    old_register_10_value
    2466                    old_register_11_value
    2467                    old_register_12_value
    2468                    old_register_13_value
    2469                    old_register_14_value
    2470                    old_register_15_value
    2471                    old_register_16_value
    2472                    old_register_17_value
    2473                    old_register_20_value
    2474                    old_register_21_value
    2475                    old_register_22_value
    2476                    old_register_23_value
    2477                    old_register_24_value
    2478                    old_register_25_value
    2479                    old_register_26_value
    2480                    old_register_27_value
    2481                    old_register_30_value
    2482                    old_register_31_value
    2483                    old_register_32_value
    2484                    old_register_33_value
    2485                    (Some ? b)
    2486                    old_register_35_value
    2487                    old_register_36_value
    2488                    old_register_37_value
    2489                    old_register_A_value
    2490                    old_register_B_value
    2491                    old_register_DPL_value
    2492                    old_register_DPH_value.
     2536  let old_register_Carry_value ≝ register_Carry_value m in
     2537    mk_RegisterMap old_register_00_value
     2538                   old_register_01_value
     2539                   old_register_02_value
     2540                   old_register_03_value
     2541                   old_register_04_value
     2542                   old_register_05_value
     2543                   old_register_06_value
     2544                   old_register_07_value
     2545                   old_register_10_value
     2546                   old_register_11_value
     2547                   old_register_12_value
     2548                   old_register_13_value
     2549                   old_register_14_value
     2550                   old_register_15_value
     2551                   old_register_16_value
     2552                   old_register_17_value
     2553                   old_register_20_value
     2554                   old_register_21_value
     2555                   old_register_22_value
     2556                   old_register_23_value
     2557                   old_register_24_value
     2558                   old_register_25_value
     2559                   old_register_26_value
     2560                   old_register_27_value
     2561                   old_register_30_value
     2562                   old_register_31_value
     2563                   old_register_32_value
     2564                   old_register_33_value
     2565                   (Some ? b)
     2566                   old_register_35_value
     2567                   old_register_36_value
     2568                   old_register_37_value
     2569                   old_register_A_value
     2570                   old_register_B_value
     2571                   old_register_DPL_value
     2572                   old_register_DPH_value
     2573                   old_register_Carry_value.
    24932574
    24942575definition update_register_35: Byte → RegisterMap → RegisterMap ≝
     
    25312612  let old_register_DPL_value ≝ register_DPL_value m in
    25322613  let old_register_DPH_value ≝ register_DPH_value m in
    2533     mk_RegisterMap old_register_00_value
    2534                    old_register_01_value
    2535                    old_register_02_value
    2536                    old_register_03_value
    2537                    old_register_04_value
    2538                    old_register_05_value
    2539                    old_register_06_value
    2540                    old_register_07_value
    2541                    old_register_10_value
    2542                    old_register_11_value
    2543                    old_register_12_value
    2544                    old_register_13_value
    2545                    old_register_14_value
    2546                    old_register_15_value
    2547                    old_register_16_value
    2548                    old_register_17_value
    2549                    old_register_20_value
    2550                    old_register_21_value
    2551                    old_register_22_value
    2552                    old_register_23_value
    2553                    old_register_24_value
    2554                    old_register_25_value
    2555                    old_register_26_value
    2556                    old_register_27_value
    2557                    old_register_30_value
    2558                    old_register_31_value
    2559                    old_register_32_value
    2560                    old_register_33_value
    2561                    old_register_34_value
    2562                    (Some ? b)
    2563                    old_register_36_value
    2564                    old_register_37_value
    2565                    old_register_A_value
    2566                    old_register_B_value
    2567                    old_register_DPL_value
    2568                    old_register_DPH_value.
     2614  let old_register_Carry_value ≝ register_Carry_value m in
     2615    mk_RegisterMap old_register_00_value
     2616                   old_register_01_value
     2617                   old_register_02_value
     2618                   old_register_03_value
     2619                   old_register_04_value
     2620                   old_register_05_value
     2621                   old_register_06_value
     2622                   old_register_07_value
     2623                   old_register_10_value
     2624                   old_register_11_value
     2625                   old_register_12_value
     2626                   old_register_13_value
     2627                   old_register_14_value
     2628                   old_register_15_value
     2629                   old_register_16_value
     2630                   old_register_17_value
     2631                   old_register_20_value
     2632                   old_register_21_value
     2633                   old_register_22_value
     2634                   old_register_23_value
     2635                   old_register_24_value
     2636                   old_register_25_value
     2637                   old_register_26_value
     2638                   old_register_27_value
     2639                   old_register_30_value
     2640                   old_register_31_value
     2641                   old_register_32_value
     2642                   old_register_33_value
     2643                   old_register_34_value
     2644                   (Some ? b)
     2645                   old_register_36_value
     2646                   old_register_37_value
     2647                   old_register_A_value
     2648                   old_register_B_value
     2649                   old_register_DPL_value
     2650                   old_register_DPH_value
     2651                   old_register_Carry_value.
    25692652
    25702653definition update_register_36: Byte → RegisterMap → RegisterMap ≝
     
    26072690  let old_register_DPL_value ≝ register_DPL_value m in
    26082691  let old_register_DPH_value ≝ register_DPH_value m in
    2609     mk_RegisterMap old_register_00_value
    2610                    old_register_01_value
    2611                    old_register_02_value
    2612                    old_register_03_value
    2613                    old_register_04_value
    2614                    old_register_05_value
    2615                    old_register_06_value
    2616                    old_register_07_value
    2617                    old_register_10_value
    2618                    old_register_11_value
    2619                    old_register_12_value
    2620                    old_register_13_value
    2621                    old_register_14_value
    2622                    old_register_15_value
    2623                    old_register_16_value
    2624                    old_register_17_value
    2625                    old_register_20_value
    2626                    old_register_21_value
    2627                    old_register_22_value
    2628                    old_register_23_value
    2629                    old_register_24_value
    2630                    old_register_25_value
    2631                    old_register_26_value
    2632                    old_register_27_value
    2633                    old_register_30_value
    2634                    old_register_31_value
    2635                    old_register_32_value
    2636                    old_register_33_value
    2637                    old_register_34_value
    2638                    old_register_35_value
    2639                    (Some ? b)
    2640                    old_register_37_value
    2641                    old_register_A_value
    2642                    old_register_B_value
    2643                    old_register_DPL_value
    2644                    old_register_DPH_value.
     2692  let old_register_Carry_value ≝ register_Carry_value m in
     2693    mk_RegisterMap old_register_00_value
     2694                   old_register_01_value
     2695                   old_register_02_value
     2696                   old_register_03_value
     2697                   old_register_04_value
     2698                   old_register_05_value
     2699                   old_register_06_value
     2700                   old_register_07_value
     2701                   old_register_10_value
     2702                   old_register_11_value
     2703                   old_register_12_value
     2704                   old_register_13_value
     2705                   old_register_14_value
     2706                   old_register_15_value
     2707                   old_register_16_value
     2708                   old_register_17_value
     2709                   old_register_20_value
     2710                   old_register_21_value
     2711                   old_register_22_value
     2712                   old_register_23_value
     2713                   old_register_24_value
     2714                   old_register_25_value
     2715                   old_register_26_value
     2716                   old_register_27_value
     2717                   old_register_30_value
     2718                   old_register_31_value
     2719                   old_register_32_value
     2720                   old_register_33_value
     2721                   old_register_34_value
     2722                   old_register_35_value
     2723                   (Some ? b)
     2724                   old_register_37_value
     2725                   old_register_A_value
     2726                   old_register_B_value
     2727                   old_register_DPL_value
     2728                   old_register_DPH_value
     2729                   old_register_Carry_value.
    26452730
    26462731definition update_register_37: Byte → RegisterMap → RegisterMap ≝
     
    26832768  let old_register_DPL_value ≝ register_DPL_value m in
    26842769  let old_register_DPH_value ≝ register_DPH_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                    old_register_36_value
    2716                    (Some ? b)
    2717                    old_register_A_value
    2718                    old_register_B_value
    2719                    old_register_DPL_value
    2720                    old_register_DPH_value.
     2770  let old_register_Carry_value ≝ register_Carry_value m in
     2771    mk_RegisterMap old_register_00_value
     2772                   old_register_01_value
     2773                   old_register_02_value
     2774                   old_register_03_value
     2775                   old_register_04_value
     2776                   old_register_05_value
     2777                   old_register_06_value
     2778                   old_register_07_value
     2779                   old_register_10_value
     2780                   old_register_11_value
     2781                   old_register_12_value
     2782                   old_register_13_value
     2783                   old_register_14_value
     2784                   old_register_15_value
     2785                   old_register_16_value
     2786                   old_register_17_value
     2787                   old_register_20_value
     2788                   old_register_21_value
     2789                   old_register_22_value
     2790                   old_register_23_value
     2791                   old_register_24_value
     2792                   old_register_25_value
     2793                   old_register_26_value
     2794                   old_register_27_value
     2795                   old_register_30_value
     2796                   old_register_31_value
     2797                   old_register_32_value
     2798                   old_register_33_value
     2799                   old_register_34_value
     2800                   old_register_35_value
     2801                   old_register_36_value
     2802                   (Some ? b)
     2803                   old_register_A_value
     2804                   old_register_B_value
     2805                   old_register_DPL_value
     2806                   old_register_DPH_value
     2807                   old_register_Carry_value.
    27212808
    27222809definition update_register_A: Byte → RegisterMap → RegisterMap ≝
     
    27592846  let old_register_DPL_value ≝ register_DPL_value m in
    27602847  let old_register_DPH_value ≝ register_DPH_value m in
    2761     mk_RegisterMap old_register_00_value
    2762                    old_register_01_value
    2763                    old_register_02_value
    2764                    old_register_03_value
    2765                    old_register_04_value
    2766                    old_register_05_value
    2767                    old_register_06_value
    2768                    old_register_07_value
    2769                    old_register_10_value
    2770                    old_register_11_value
    2771                    old_register_12_value
    2772                    old_register_13_value
    2773                    old_register_14_value
    2774                    old_register_15_value
    2775                    old_register_16_value
    2776                    old_register_17_value
    2777                    old_register_20_value
    2778                    old_register_21_value
    2779                    old_register_22_value
    2780                    old_register_23_value
    2781                    old_register_24_value
    2782                    old_register_25_value
    2783                    old_register_26_value
    2784                    old_register_27_value
    2785                    old_register_30_value
    2786                    old_register_31_value
    2787                    old_register_32_value
    2788                    old_register_33_value
    2789                    old_register_34_value
    2790                    old_register_35_value
    2791                    old_register_36_value
    2792                    old_register_37_value
    2793                    (Some ? b)
    2794                    old_register_B_value
    2795                    old_register_DPL_value
    2796                    old_register_DPH_value.
     2848  let old_register_Carry_value ≝ register_Carry_value m in
     2849    mk_RegisterMap old_register_00_value
     2850                   old_register_01_value
     2851                   old_register_02_value
     2852                   old_register_03_value
     2853                   old_register_04_value
     2854                   old_register_05_value
     2855                   old_register_06_value
     2856                   old_register_07_value
     2857                   old_register_10_value
     2858                   old_register_11_value
     2859                   old_register_12_value
     2860                   old_register_13_value
     2861                   old_register_14_value
     2862                   old_register_15_value
     2863                   old_register_16_value
     2864                   old_register_17_value
     2865                   old_register_20_value
     2866                   old_register_21_value
     2867                   old_register_22_value
     2868                   old_register_23_value
     2869                   old_register_24_value
     2870                   old_register_25_value
     2871                   old_register_26_value
     2872                   old_register_27_value
     2873                   old_register_30_value
     2874                   old_register_31_value
     2875                   old_register_32_value
     2876                   old_register_33_value
     2877                   old_register_34_value
     2878                   old_register_35_value
     2879                   old_register_36_value
     2880                   old_register_37_value
     2881                   (Some ? b)
     2882                   old_register_B_value
     2883                   old_register_DPL_value
     2884                   old_register_DPH_value
     2885                   old_register_Carry_value.
    27972886
    27982887definition update_register_B: Byte → RegisterMap → RegisterMap ≝
     
    28352924  let old_register_DPL_value ≝ register_DPL_value m in
    28362925  let old_register_DPH_value ≝ register_DPH_value m in
    2837     mk_RegisterMap old_register_00_value
    2838                    old_register_01_value
    2839                    old_register_02_value
    2840                    old_register_03_value
    2841                    old_register_04_value
    2842                    old_register_05_value
    2843                    old_register_06_value
    2844                    old_register_07_value
    2845                    old_register_10_value
    2846                    old_register_11_value
    2847                    old_register_12_value
    2848                    old_register_13_value
    2849                    old_register_14_value
    2850                    old_register_15_value
    2851                    old_register_16_value
    2852                    old_register_17_value
    2853                    old_register_20_value
    2854                    old_register_21_value
    2855                    old_register_22_value
    2856                    old_register_23_value
    2857                    old_register_24_value
    2858                    old_register_25_value
    2859                    old_register_26_value
    2860                    old_register_27_value
    2861                    old_register_30_value
    2862                    old_register_31_value
    2863                    old_register_32_value
    2864                    old_register_33_value
    2865                    old_register_34_value
    2866                    old_register_35_value
    2867                    old_register_36_value
    2868                    old_register_37_value
    2869                    old_register_A_value
    2870                    (Some ? b)
    2871                    old_register_DPL_value
    2872                    old_register_DPH_value.
     2926  let old_register_Carry_value ≝ register_Carry_value m in
     2927    mk_RegisterMap old_register_00_value
     2928                   old_register_01_value
     2929                   old_register_02_value
     2930                   old_register_03_value
     2931                   old_register_04_value
     2932                   old_register_05_value
     2933                   old_register_06_value
     2934                   old_register_07_value
     2935                   old_register_10_value
     2936                   old_register_11_value
     2937                   old_register_12_value
     2938                   old_register_13_value
     2939                   old_register_14_value
     2940                   old_register_15_value
     2941                   old_register_16_value
     2942                   old_register_17_value
     2943                   old_register_20_value
     2944                   old_register_21_value
     2945                   old_register_22_value
     2946                   old_register_23_value
     2947                   old_register_24_value
     2948                   old_register_25_value
     2949                   old_register_26_value
     2950                   old_register_27_value
     2951                   old_register_30_value
     2952                   old_register_31_value
     2953                   old_register_32_value
     2954                   old_register_33_value
     2955                   old_register_34_value
     2956                   old_register_35_value
     2957                   old_register_36_value
     2958                   old_register_37_value
     2959                   old_register_A_value
     2960                   (Some ? b)
     2961                   old_register_DPL_value
     2962                   old_register_DPH_value
     2963                   old_register_Carry_value.
    28732964
    28742965definition update_register_DPL: Byte → RegisterMap → RegisterMap ≝
     
    29113002  let old_register_DPL_value ≝ register_DPL_value m in
    29123003  let old_register_DPH_value ≝ register_DPH_value m in
    2913     mk_RegisterMap old_register_00_value
    2914                    old_register_01_value
    2915                    old_register_02_value
    2916                    old_register_03_value
    2917                    old_register_04_value
    2918                    old_register_05_value
    2919                    old_register_06_value
    2920                    old_register_07_value
    2921                    old_register_10_value
    2922                    old_register_11_value
    2923                    old_register_12_value
    2924                    old_register_13_value
    2925                    old_register_14_value
    2926                    old_register_15_value
    2927                    old_register_16_value
    2928                    old_register_17_value
    2929                    old_register_20_value
    2930                    old_register_21_value
    2931                    old_register_22_value
    2932                    old_register_23_value
    2933                    old_register_24_value
    2934                    old_register_25_value
    2935                    old_register_26_value
    2936                    old_register_27_value
    2937                    old_register_30_value
    2938                    old_register_31_value
    2939                    old_register_32_value
    2940                    old_register_33_value
    2941                    old_register_34_value
    2942                    old_register_35_value
    2943                    old_register_36_value
    2944                    old_register_37_value
    2945                    old_register_A_value
    2946                    old_register_B_value
    2947                    (Some ? b)
    2948                    old_register_DPH_value.
     3004  let old_register_Carry_value ≝ register_Carry_value m in
     3005    mk_RegisterMap old_register_00_value
     3006                   old_register_01_value
     3007                   old_register_02_value
     3008                   old_register_03_value
     3009                   old_register_04_value
     3010                   old_register_05_value
     3011                   old_register_06_value
     3012                   old_register_07_value
     3013                   old_register_10_value
     3014                   old_register_11_value
     3015                   old_register_12_value
     3016                   old_register_13_value
     3017                   old_register_14_value
     3018                   old_register_15_value
     3019                   old_register_16_value
     3020                   old_register_17_value
     3021                   old_register_20_value
     3022                   old_register_21_value
     3023                   old_register_22_value
     3024                   old_register_23_value
     3025                   old_register_24_value
     3026                   old_register_25_value
     3027                   old_register_26_value
     3028                   old_register_27_value
     3029                   old_register_30_value
     3030                   old_register_31_value
     3031                   old_register_32_value
     3032                   old_register_33_value
     3033                   old_register_34_value
     3034                   old_register_35_value
     3035                   old_register_36_value
     3036                   old_register_37_value
     3037                   old_register_A_value
     3038                   old_register_B_value
     3039                   (Some ? b)
     3040                   old_register_DPH_value
     3041                   old_register_Carry_value.
    29493042
    29503043definition update_register_DPH: Byte → RegisterMap → RegisterMap ≝
     
    29873080  let old_register_DPL_value ≝ register_DPL_value m in
    29883081  let old_register_DPH_value ≝ register_DPH_value m in
    2989     mk_RegisterMap old_register_00_value
    2990                    old_register_01_value
    2991                    old_register_02_value
    2992                    old_register_03_value
    2993                    old_register_04_value
    2994                    old_register_05_value
    2995                    old_register_06_value
    2996                    old_register_07_value
    2997                    old_register_10_value
    2998                    old_register_11_value
    2999                    old_register_12_value
    3000                    old_register_13_value
    3001                    old_register_14_value
    3002                    old_register_15_value
    3003                    old_register_16_value
    3004                    old_register_17_value
    3005                    old_register_20_value
    3006                    old_register_21_value
    3007                    old_register_22_value
    3008                    old_register_23_value
    3009                    old_register_24_value
    3010                    old_register_25_value
    3011                    old_register_26_value
    3012                    old_register_27_value
    3013                    old_register_30_value
    3014                    old_register_31_value
    3015                    old_register_32_value
    3016                    old_register_33_value
    3017                    old_register_34_value
    3018                    old_register_35_value
    3019                    old_register_36_value
    3020                    old_register_37_value
    3021                    old_register_A_value
    3022                    old_register_B_value
    3023                    old_register_DPL_value
     3082  let old_register_Carry_value ≝ register_Carry_value m in
     3083    mk_RegisterMap old_register_00_value
     3084                   old_register_01_value
     3085                   old_register_02_value
     3086                   old_register_03_value
     3087                   old_register_04_value
     3088                   old_register_05_value
     3089                   old_register_06_value
     3090                   old_register_07_value
     3091                   old_register_10_value
     3092                   old_register_11_value
     3093                   old_register_12_value
     3094                   old_register_13_value
     3095                   old_register_14_value
     3096                   old_register_15_value
     3097                   old_register_16_value
     3098                   old_register_17_value
     3099                   old_register_20_value
     3100                   old_register_21_value
     3101                   old_register_22_value
     3102                   old_register_23_value
     3103                   old_register_24_value
     3104                   old_register_25_value
     3105                   old_register_26_value
     3106                   old_register_27_value
     3107                   old_register_30_value
     3108                   old_register_31_value
     3109                   old_register_32_value
     3110                   old_register_33_value
     3111                   old_register_34_value
     3112                   old_register_35_value
     3113                   old_register_36_value
     3114                   old_register_37_value
     3115                   old_register_A_value
     3116                   old_register_B_value
     3117                   old_register_DPL_value
     3118                   (Some ? b)
     3119                   old_register_Carry_value.
     3120
     3121definition update_register_Carry: Byte → RegisterMap → RegisterMap ≝
     3122  λb: Byte.
     3123  λm: RegisterMap.
     3124  let old_register_00_value ≝ register_00_value m in
     3125  let old_register_01_value ≝ register_01_value m in
     3126  let old_register_02_value ≝ register_02_value m in
     3127  let old_register_03_value ≝ register_03_value m in
     3128  let old_register_04_value ≝ register_04_value m in
     3129  let old_register_05_value ≝ register_05_value m in
     3130  let old_register_06_value ≝ register_06_value m in
     3131  let old_register_07_value ≝ register_07_value m in
     3132  let old_register_10_value ≝ register_01_value m in
     3133  let old_register_11_value ≝ register_01_value m in
     3134  let old_register_12_value ≝ register_02_value m in
     3135  let old_register_13_value ≝ register_03_value m in
     3136  let old_register_14_value ≝ register_04_value m in
     3137  let old_register_15_value ≝ register_05_value m in
     3138  let old_register_16_value ≝ register_06_value m in
     3139  let old_register_17_value ≝ register_07_value m in
     3140  let old_register_20_value ≝ register_01_value m in
     3141  let old_register_21_value ≝ register_02_value m in
     3142  let old_register_22_value ≝ register_02_value m in
     3143  let old_register_23_value ≝ register_03_value m in
     3144  let old_register_24_value ≝ register_04_value m in
     3145  let old_register_25_value ≝ register_05_value m in
     3146  let old_register_26_value ≝ register_06_value m in
     3147  let old_register_27_value ≝ register_07_value m in
     3148  let old_register_30_value ≝ register_01_value m in
     3149  let old_register_31_value ≝ register_02_value m in
     3150  let old_register_32_value ≝ register_02_value m in
     3151  let old_register_33_value ≝ register_03_value m in
     3152  let old_register_34_value ≝ register_04_value m in
     3153  let old_register_35_value ≝ register_05_value m in
     3154  let old_register_36_value ≝ register_06_value m in
     3155  let old_register_37_value ≝ register_07_value m in
     3156  let old_register_A_value ≝ register_A_value m in
     3157  let old_register_B_value ≝ register_B_value m in
     3158  let old_register_DPL_value ≝ register_DPL_value m in
     3159  let old_register_DPH_value ≝ register_DPH_value m in
     3160    mk_RegisterMap old_register_00_value
     3161                   old_register_01_value
     3162                   old_register_02_value
     3163                   old_register_03_value
     3164                   old_register_04_value
     3165                   old_register_05_value
     3166                   old_register_06_value
     3167                   old_register_07_value
     3168                   old_register_10_value
     3169                   old_register_11_value
     3170                   old_register_12_value
     3171                   old_register_13_value
     3172                   old_register_14_value
     3173                   old_register_15_value
     3174                   old_register_16_value
     3175                   old_register_17_value
     3176                   old_register_20_value
     3177                   old_register_21_value
     3178                   old_register_22_value
     3179                   old_register_23_value
     3180                   old_register_24_value
     3181                   old_register_25_value
     3182                   old_register_26_value
     3183                   old_register_27_value
     3184                   old_register_30_value
     3185                   old_register_31_value
     3186                   old_register_32_value
     3187                   old_register_33_value
     3188                   old_register_34_value
     3189                   old_register_35_value
     3190                   old_register_36_value
     3191                   old_register_37_value
     3192                   old_register_A_value
     3193                   old_register_B_value
     3194                   old_register_DPL_value
     3195                   old_register_DPH_value
    30243196                   (Some ? b).
    30253197
     
    30653237  | RegisterDPL ⇒ update_register_DPL b m
    30663238  | RegisterDPH ⇒ update_register_DPH b m
     3239  | RegisterCarry ⇒ update_register_Carry b m
    30673240  ].
    30683241 
  • Deliverables/D3.3/id-lookup-branch/ASM/Util.ma

    r1075 r1098  
    3232  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
    3333  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     34  ].
     35
     36let rec prefix
     37  (A: Type[0]) (k: nat) (l: list A)
     38    on l ≝
     39  match l with
     40  [ nil ⇒ [ ]
     41  | cons hd tl ⇒
     42    match k with
     43    [ O ⇒ [ ]
     44    | S k' ⇒ hd :: prefix A k' tl
     45    ]
    3446  ].
    3547 
  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1091 r1098  
    3030  λr: list A.
    3131    foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
     32
     33definition list_set_member ≝
     34  λA: Type[0].
     35  λeq_a: A → A → bool.
     36  λa: A.
     37  λl: list A.
     38    member A eq_a a l.
    3239
    3340definition statement_successors ≝
     
    106113  | ertl_st_cond _ _ _ ⇒ lattice_bottom
    107114  | ertl_st_return _ ⇒ lattice_bottom
    108   | ertl_st_clear_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉
    109   | ertl_st_set_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉
    110   | _ ⇒ ?
    111   ].
    112 
    113 let defined (stmt : statement) : L.t =
     115  | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
     116  | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
     117  | ertl_st_op2 op2 r _ _ _ ⇒
     118    match op2 with
     119    [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     120    | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     121    | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     122    | _ ⇒ lattice_psingleton r
     123    ]
     124  | ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r
     125  | ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r
     126  | ertl_st_frame_size r _ ⇒ lattice_psingleton r
     127  | ertl_st_pop r _ ⇒ lattice_psingleton r
     128  | ertl_st_int r _ _ ⇒ lattice_psingleton r
     129  | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r
     130  | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r
     131  | ertl_st_move r _ _ ⇒ lattice_psingleton r
     132  | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
     133  | ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r
     134  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
     135  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
     136  | ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r
     137  (* Potentially destroys all caller-save hardware registers. *)
     138  | ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉
     139  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     140  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     141  ].
     142
     143definition list_set_of_list ≝
     144  λrl.
     145    foldr ? ? (list_set_add Register eq_Register) rl [ ].
     146
     147definition list_set_of_list2 ≝
     148  let f ≝ λset. λr. list_set_add Register eq_Register r set in
     149    foldl ? ? f [ ].
     150
     151definition ret_regs ≝ list_set_of_list RegisterRets.
     152
     153definition used: ertl_statement → register_lattice ≝
     154  λstmt.
    114155  match stmt with
    115   | St_clear_carry _
    116   | St_set_carry _ ->
    117     Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
    118   | St_op2 (I8051.Add, r, _, _, _)
    119   | St_op2 (I8051.Addc, r, _, _, _)
    120   | St_op2 (I8051.Sub, r, _, _, _) ->
    121     L.join (L.hsingleton I8051.carry) (L.psingleton r)
    122   | St_op1 (I8051.Inc, r, _, _)
    123   | St_get_hdw (r, _, _)
    124   | St_framesize (r, _)
    125   | St_pop (r, _)
    126   | St_int (r, _, _)
    127   | St_addrH (r, _, _)
    128   | St_addrL (r, _, _)
    129   | St_move (r, _, _)
    130   | St_opaccsA (_, r, _, _, _)
    131   | St_opaccsB (_, r, _, _, _)
    132   | St_op1 (_, r, _, _)
    133   | St_op2 (_, r, _, _, _)
    134   | St_load (r, _, _, _) ->
    135     L.psingleton r
    136   | St_set_hdw (r, _, _)
    137   | St_hdw_to_hdw (r, _, _) ->
    138     L.hsingleton r
    139   | St_call_id _ ->
    140       (* Potentially destroys all caller-save hardware registers. *)
    141     Register.Set.empty, I8051.caller_saved
    142   | St_newframe _
    143   | St_delframe _ ->
    144     L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
     156  [ ertl_st_skip _ ⇒ lattice_bottom
     157  | ertl_st_cost _ _ ⇒ lattice_bottom
     158  | ertl_st_comment _ _ ⇒ lattice_bottom
     159  | ertl_st_frame_size _ _ ⇒ lattice_bottom
     160  | ertl_st_pop _ _ ⇒ lattice_bottom
     161  | ertl_st_addr_h _ _ _ ⇒ lattice_bottom
     162  | ertl_st_addr_l _ _ _ ⇒ lattice_bottom
     163  | ertl_st_int _ _ _ ⇒ lattice_bottom
     164  | ertl_st_clear_carry _ ⇒ lattice_bottom
     165  | ertl_st_set_carry _ ⇒ lattice_bottom
     166    (* Reads the hardware registers that are used to pass parameters. *)
     167  | ertl_st_call_id _ nparams _ ⇒
     168    〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉
     169  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
     170  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
     171  | ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r
     172  | ertl_st_push r _ ⇒ lattice_psingleton r
     173  | ertl_st_move _ r _ ⇒ lattice_psingleton r
     174  | ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r
     175  | ertl_st_cond r _ _ ⇒ lattice_psingleton r
     176  | ertl_st_op2 op2 _ r1 r2 _ ⇒
     177    match op2 with
     178    [ Addc ⇒
     179      lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
     180    | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     181    ]
     182  | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     183  | ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     184  | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     185  | ertl_st_store r1 r2 r3 _ ⇒
     186    lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3)
     187  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     188  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     189  | ertl_st_return _ ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     190  ].
     191
     192definition eliminable: register_lattice → ertl_statement → option label ≝
     193  λl.
     194  λstmt.
     195  let 〈pliveafter, hliveafter〉 ≝ l in
     196  match stmt with
     197  [ ertl_st_skip _ ⇒ None ?
     198  | ertl_st_comment _ _ ⇒ None ?
     199  | ertl_st_cost _ _ ⇒ None ?
     200  | ertl_st_new_frame _ ⇒ None ?
     201  | ertl_st_del_frame _ ⇒ None ?
     202  | ertl_st_pop _ _ ⇒ None ?
     203  | ertl_st_push _ _ ⇒ None ?
     204  | ertl_st_clear_carry _  ⇒ None ?
     205  | ertl_st_set_carry _  ⇒ None ?
     206  | ertl_st_store _ _ _ _ ⇒ None ?
     207  | ertl_st_call_id _ _ _ ⇒ None ?
     208  | ertl_st_cond _ _ _ ⇒ None ?
     209  | ertl_st_return _ ⇒ None ?
     210  | ertl_st_get_hdw r _ l ⇒
     211    if list_set_member register (eq_identifier ?) r pliveafter ∨
     212       list_set_member Register eq_Register RegisterCarry hliveafter then
     213      None ?
     214    else
     215      Some ? l
     216  | ertl_st_frame_size r l ⇒
     217    if list_set_member register (eq_identifier ?) r pliveafter ∨
     218       list_set_member Register eq_Register RegisterCarry hliveafter then
     219      None ?
     220    else
     221      Some ? l
     222  | ertl_st_int r _ l ⇒
     223    if list_set_member register (eq_identifier ?) r pliveafter ∨
     224       list_set_member Register eq_Register RegisterCarry hliveafter then
     225      None ?
     226    else
     227      Some ? l
     228  | ertl_st_addr_h r _ l ⇒
     229    if list_set_member register (eq_identifier ?) r pliveafter ∨
     230       list_set_member Register eq_Register RegisterCarry hliveafter then
     231      None ?
     232    else
     233      Some ? l
     234  | ertl_st_addr_l r _ l ⇒
     235    if list_set_member register (eq_identifier ?) r pliveafter ∨
     236       list_set_member Register eq_Register RegisterCarry hliveafter then
     237      None ?
     238    else
     239      Some ? l
     240  | ertl_st_move r _ l ⇒
     241    if list_set_member register (eq_identifier ?) r pliveafter ∨
     242       list_set_member Register eq_Register RegisterCarry hliveafter then
     243      None ?
     244    else
     245      Some ? l
     246  | ertl_st_opaccs_a _ r _ _ l ⇒
     247    if list_set_member register (eq_identifier ?) r pliveafter ∨
     248       list_set_member Register eq_Register RegisterCarry hliveafter then
     249      None ?
     250    else
     251      Some ? l
     252  | ertl_st_opaccs_b _ r _ _ l ⇒
     253    if list_set_member register (eq_identifier ?) r pliveafter ∨
     254       list_set_member Register eq_Register RegisterCarry hliveafter then
     255      None ?
     256    else
     257      Some ? l
     258  | ertl_st_op1 _ r _ l ⇒
     259    if list_set_member register (eq_identifier ?) r pliveafter ∨
     260       list_set_member Register eq_Register RegisterCarry hliveafter then
     261      None ?
     262    else
     263      Some ? l
     264  | ertl_st_op2 _ r _ _ l ⇒
     265    if list_set_member register (eq_identifier ?) r pliveafter ∨
     266       list_set_member Register eq_Register RegisterCarry hliveafter then
     267      None ?
     268    else
     269      Some ? l
     270  | ertl_st_load r _ _ l ⇒
     271    if list_set_member register (eq_identifier ?) r pliveafter ∨
     272       list_set_member Register eq_Register RegisterCarry hliveafter then
     273      None ?
     274    else
     275      Some ? l
     276  | ertl_st_set_hdw r _ l ⇒
     277    if list_set_member Register eq_Register r hliveafter then
     278      None ?
     279    else
     280      Some ? l
     281  | ertl_st_hdw_to_hdw r _ l ⇒
     282    if list_set_member Register eq_Register r hliveafter then
     283      None ?
     284    else
     285      Some ? l
     286  ].
     287
     288definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝
     289  λstmt.
     290  λliveafter.
     291  match eliminable liveafter stmt with
     292  [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt)
     293  | Some l ⇒ liveafter
     294  ].
     295
     296definition valuation ≝ label → register_lattice.
     297
     298definition analyse: ertl_internal_function → valuation ≝
     299  λint_fun.
     300  let livebefore ≝ λlabel. λliveafter: valuation.
     301    match lookup ? ? (ertl_if_graph int_fun) label with
     302    [ None      ⇒ ?
     303    | Some stmt ⇒ statement_semantics stmt (liveafter label)
     304    ]
     305  in ?.
Note: See TracChangeset for help on using the changeset viewer.