Skip to main content

🗿 Legacy_script_patches_for_J.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.

Module t.
  Record record : Set := Build {
    legacy_script_hash : Script_expr_hash.t;
    patched_code : Micheline.canonical Michelson_v1_primitives.prim;
    addresses : list string;
  }.
  Definition with_legacy_script_hash legacy_script_hash (r : record) :=
    Build legacy_script_hash r.(patched_code) r.(addresses).
  Definition with_patched_code patched_code (r : record) :=
    Build r.(legacy_script_hash) patched_code r.(addresses).
  Definition with_addresses addresses (r : record) :=
    Build r.(legacy_script_hash) r.(patched_code) addresses.
End t.
Definition t := t.record.

Definition patched_script : Set := t.

Definition script_hash (function_parameter : patched_script)
  : Script_expr_hash.t :=
  let '{| t.legacy_script_hash := legacy_script_hash |} := function_parameter in
  legacy_script_hash.

Definition code (function_parameter : patched_script)
  : Micheline.canonical Michelson_v1_primitives.prim :=
  let '{| t.patched_code := patched_code |} := function_parameter in
  patched_code.

Definition bin_expr_exn (hex : string) : Script_repr.expr :=
  match
    Option.bind (Hex.to_bytes (Hex.Hex hex))
      (fun (bytes_value : bytes) ⇒
        Data_encoding.Binary.of_bytes_opt Script_repr.expr_encoding bytes_value)
    with
  | Some exprexpr
  | None
    Pervasives.raise
      (Build_extensible "Failure" string "Decoding script failed.")
  end.

Definition exprtgpMFzTtyg1STJqANLQsjsMXmkf8UuJTuczQh8GPtqfw18x6Lc : t :=
  {|
    t.legacy_script_hash :=
      Script_expr_hash.of_b58check_exn
        "exprtgpMFzTtyg1STJqANLQsjsMXmkf8UuJTuczQh8GPtqfw18x6Lc";
    t.patched_code :=
      bin_expr_exn
        "02000001d305000764085e036c055f036d0000000325646f046c000000082564656661756c7405010765035d036e050202000001a303210316072e02000000930743036a00000313020000001e020000000403190325072c020000000002000000090200000004034f0327020000000b051f02000000020321034c03170316031e0354034802000000490319033c072c020000002a034807430368010000001b4f6e6c7920746865206f776e65722063616e206f7065726174652e03420327020000000f034f0326051f0200000002031703420200000100051f0200000006031703210317034202000000c203170321053d036d0200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f02000000020320055507640563036e076407650563036e0563036a0764036a076407650563036e0563036a036e020000002e072f020000002207430368010000001742616420636f6e747261637420696e2073746f72616765032702000000000313034803460533076407650563036e0563036a0764036a076407650563036e0563036a036e034d031b0342034c0316034c0200000012020000000d03210316051f02000000020317051f0200000004034c03420342";
    t.addresses := [ "KT1MzfYSbq18fYr4f44aQRoZBQN72BAtiz5j" ]; |}.

Definition exprucjN3PgUnqQHFXQmemT44DjkacU35NrSSKyz18JSSjJB9vtUEw : t :=
  {|
    t.legacy_script_hash :=
      Script_expr_hash.of_b58check_exn
        "exprucjN3PgUnqQHFXQmemT44DjkacU35NrSSKyz18JSSjJB9vtUEw";
    t.patched_code :=
      bin_expr_exn
        "0200000f73050007640865086407640865065a036c000000052564657374046a00000010257472616e736665725f616d6f756e7400000009255472616e7366657206630765065a036c0000000a25706f75725f64657374045c0000001025706f75725f617574686f72697a657200000009255365745f706f757207640865065f0765065f035c0000000c257369676e61746f726965730462000000102567726f75705f7468726573686f6c640000000b256b65795f67726f757073046200000012256f766572616c6c5f7468726573686f6c6400000009255365745f6b6579730663035d0000000d255365745f64656c65676174650000000d25616374696f6e5f696e707574065f055f056303670000000b257369676e6174757265730000000725416374696f6e0563076504670000000a25706f75725f61757468046a0000000c25706f75725f616d6f756e7405010765076504620000000f257265706c61795f636f756e7465720865065f0765065f035c0000000c257369676e61746f726965730462000000102567726f75705f7468726573686f6c640000000b256b65795f67726f757073046200000012256f766572616c6c5f7468726573686f6c6400000009256b65795f696e666f076508650865046a0000000f257665737465645f62616c616e6365046a000000122576657374696e675f696e6372656d656e74000000132576657374696e675f7175616e7469746965730865046b0000000c256e6578745f7061796f7574045b00000010257061796f75745f696e74657276616c000000112576657374696e675f7363686564756c65000000082576657374696e6705630765046e0000000a25706f75725f64657374045c0000001025706f75725f617574686f72697a657205020200000ce503210316072e020000078e051f020000001903170321063d036d0000000b406f7065726174696f6e73034c034c0316032104170000000c256b65795f696e666f204025051f0200000074041600000012257265706c61795f636f756e746572204025051f0200000016032104170000000e257369676e617475726573204025034c051f0200000036051f020000001804160000001025616374696f6e5f696e7075742040250321034903540342034c0342040c00000007407061636b6564034c051f0200000050032104160000000e256b65795f67726f757073204025051f0200000033041700000015256f766572616c6c5f7468726573686f6c64204025043000000010406f766572616c6c5f636f756e746572034c0552020000016c051f020000004f072d020000003a051f0200000002034c0321041600000003402525051f020000001f04170000000340252504300000000e4067726f75705f636f756e746572034c02000000090200000004034f03270552020000008f051f0200000015072d020000000002000000090200000004034f0327072f020000000203200200000065034c051f0200000033051f020000002c034c051f0200000021051f020000001a0743035b004104120000000e4067726f75705f636f756e7465720321041800000007407369675f6f6b0200000015072c020000000002000000090200000004034f0327034c0200000064051f020000005d051f02000000560743035b0000020000001c03190428000000144067726f75705f7468726573686f6c645f6d6574072c0200000023051f020000001c0743035b0041041200000010406f766572616c6c5f636f756e7465720200000000072d02000000090200000004034f03270200000000034c072d02000000090200000004034f0327020000000003200743035b0000020000001e0319042800000016406f766572616c6c5f7468726573686f6c645f6d65740200000015072c020000000002000000090200000004034f03270200000076051f020000006f051f0200000068032103160321041600000012257265706c61795f636f756e74657220402507430362000104120000000f407265706c61795f636f756e746572051f020000001204170000000c256b65795f696e666f2040250442000000052540202540051f020000000203170342072e020000025d072e02000001f40321051f0200000196041700000013257472616e736665725f616d6f756e7420402503210415000000084062616c616e6365020000001e020000000403190328072c020000000002000000090200000004034f0327034c051f0200000141051f020000004003210317032103160416000000162576657374696e675f7175616e7469746965732040250321041600000012257665737465645f62616c616e636520402503210321051f0200000023020000001e020000000403190332072c020000000002000000090200000004034f0327034c0393072f0200000004034f0327020000001504580000000f407665737465645f62616c616e6365051f020000001b0417000000152576657374696e675f696e6372656d656e742040250442000000194076657374696e675f7175616e746974696573202540202540051f0200000038032103160417000000142576657374696e675f7363686564756c65204025051f020000001304170000000d25706f75725f696e666f20402504420000000e4076657374696e672025402025400442000000052540202540034c031603420321041700000013257472616e736665725f616d6f756e74204025051f020000000e0416000000082564657374204025034f044d0000000c407472616e736665725f6f70041b0000000b406f7065726174696f6e73020000005d034c051f020000005405380200000006037a03540342034c03210316051f020000002c031704160000000b2576657374696e672040250442000000132576657374696e672025706f75725f696e666f0442000000084073746f7261676502000001cf072e02000001ab0321032104160000000e256b65795f67726f757073204025051f0200000064041700000021256f766572616c6c5f7468726573686f6c6420406e65775f7468726573686f6c640321074303620000020000001e020000000403190337072c020000000002000000090200000004034f03270843036200000000000840636f756e746572055202000000aa0321041600000010257369676e61746f7269657320402525051f02000000450417000000142567726f75705f7468726573686f6c64204025250321074303620000020000001e020000000403190337072c020000000002000000090200000004034f0327044500000009406e756d5f6b657973020000001e020000000403190328072c020000000002000000090200000004034f032707430362000104120000000840636f756e746572020000001e020000000403190328072c020000000002000000090200000004034f0327034c051f020000004b051f02000000190321031604160000000f257265706c61795f636f756e746572034c04420000000c254020256b65795f696e666f051f020000000203170442000000084073746f726167650200000018044e00000010407365745f64656c65676174655f6f70031b03420200000547072f02000001c80317032103170321051f020000001304170000000d25706f75725f696e666f20402504160000000b2576657374696e6720402503210417000000142576657374696e675f7363686564756c65204025032104160000000f256e6578745f7061796f75742040250321034002000000040319032a0200000015072c020000000002000000090200000004034f0327051f020000001b041700000013257061796f75745f696e74657276616c2040250321041200000010406e65775f6e6578745f7061796f7574044200000025256e6578745f7061796f757420254020406e65775f76657374696e675f7363686564756c65034c0416000000162576657374696e675f7175616e7469746965732040250321041600000012257665737465645f62616c616e6365204025051f020000001d0417000000152576657374696e675f696e6372656d656e74204025032104120000000c406e65775f62616c616e6365044200000012257665737465645f62616c616e63652025400442000000252576657374696e675f7175616e746974696573202576657374696e675f7363686564756c6504420000000b2576657374696e67202540034c03160442000000084073746f72616765053d036d0200000371051f0200000053031703210317032104160000000b2576657374696e6720402503210416000000162576657374696e675f7175616e7469746965732040250321041600000012257665737465645f62616c616e636520402503210321051f02000001e104170000001025706f75725f616d6f756e74204025250321051f0200000023020000001e020000000403190332072c020000000002000000090200000004034f032703210415000000084062616c616e6365020000001e020000000403190328072c020000000002000000090200000004034f0327034c049300000010406e65775f6375725f62616c616e6365072f0200000004034f03270200000000051f020000001b0417000000152576657374696e675f696e6372656d656e74204025044200000026257665737465645f62616c616e6365202540204076657374696e675f7175616e746974696573051f020000001a0417000000142576657374696e675f7363686564756c6520402504420000000e2540202540204076657374696e67051f020000002a04170000000d25706f75725f696e666f2040250321072f02000000090200000004034f03270200000000034c051f02000000870442000000052540202540034c03160321041600000012257265706c61795f636f756e746572204025032107430362000104120000000f407265706c61795f636f756e746572034c034903540342051f0200000032051f020000001204170000000c256b65795f696e666f20402504420000000525402025400442000000084073746f726167650321051f02000000fd034c032104160000000d25706f75725f646573742040250555036c072f0200000023074303680100000018426164207472616e73616374696f6e20726563656976657203270200000000051f02000000ac032104170000001325706f75725f617574686f72697a6572204025051f020000005904160000000d25706f75725f64657374204025034c032104160000000d25706f75725f61757468204025051f020000002804170000000f25706f75725f616d6f756e74204025034c03420342040c00000007407061636b656404180000000d40706f75725f617574685f6f6b0200000015072c020000000002000000090200000004034f0327053d036d04170000000f25706f75725f616d6f756e74204025034f044d0000000840706f75725f6f70031b0342";
    t.addresses :=
      [
        "KT1Kfbk3B6NYPCPohPBDU3Hxf5Xeyy9PdkNp";
        "KT1JW6PwhfaEJu6U3ENsxUeja48AdtqSoekd";
        "KT1VsSxSXUkgw6zkBGgUuDXXuJs9ToPqkrCg";
        "KT1TcAHw5gpejyemwRtdNyFKGBLc4qwA5gtw";
        "KT1FN5fcNNcgieGjzxbVEPWUpJGwZEpzNGA8";
        "KT1Um7ieBEytZtumecLqGeL56iY6BuWoBgio";
        "KT1QuofAgnsWffHzLA7D78rxytJruGHDe7XG";
        "KT1CSKPf2jeLpMmrgKquN2bCjBTkAcAdRVDy";
        "KT1D5NmtDtgCwPxYNb2ZK2But6dhNLs1T1bV";
        "KT1VvXEpeBpreAVpfp4V8ZujqWu2gVykwXBJ";
        "KT1TzamC1SCj68ia2E4q2GWZeT24yRHvUZay";
        "KT1LZFMGrdnPjRLsCZ1aEDUAF5myA5Eo4rQe";
        "KT1PDAELuX7CypUHinUgFgGFskKs7ytwh5Vw";
        "KT19xDbLsvQKnp9xqfDNPWJbKJJmV93dHDUa";
        "KT1Cz7TyVFvHxXpxLS57RFePrhTGisUpPhvD";
        "KT1LQ99RfGcmFe98PiBcGXuyjBkWzAcoXXhW";
        "KT1Gow8VzXZx3Akn5kvjACqnjnyYBxQpzSKr";
        "KT1DnfT4hfikoMY3uiPE9mQV4y3Xweramb2k";
        "KT1FuFDZGdw86p6krdBUKoZfEMkcUmezqX5o";
        "KT1SLWhfqPtQq7f4zLomh8BNgDeprF9B6d2M";
        "KT1THsDNgHtN56ew9VVCAUWnqPC81pqAxCEp";
        "KT1CM1g1o9RKDdtDKgcBWE59X2KgTc2TcYtC";
        "KT1W148mcjmfvr9J2RvWcGHxsAFApq9mcfgT";
        "KT1HvwFnXteMbphi7mfPDhCWkZSDvXEz8iyv";
        "KT1RUT25eGgo9KKWXfLhj1xYjghAY1iZ2don";
        "KT1EWLAQGPMF2uhtVRPaCH2vtFVN36Njdr6z";
        "KT1WPEis2WhAc2FciM2tZVn8qe6pCBe9HkDp";
        "KT1Msatnmdy24sQt6knzpALs4tvHfSPPduA2";
        "KT1A56dh8ivKNvLiLVkjYPyudmnY2Ti5Sba3";
        "KT1KRyTaxCAM3YRquifEe29BDbUKNhJ6hdtx";
        "KT1FL3C6t9Lyfskyb6rQrCRQTnf7M9t587VM";
        "KT1Q1kfbvzteafLvnGz92DGvkdypXfTGfEA3"
      ]; |}.

Definition expruqNpURkmjQk5RGHjLrnS1U3DZnEsQCvQQNLSpN1powRmJeQgoJ : t :=
  {|
    t.legacy_script_hash :=
      Script_expr_hash.of_b58check_exn
        "expruqNpURkmjQk5RGHjLrnS1U3DZnEsQCvQQNLSpN1powRmJeQgoJ";
    t.patched_code :=
      bin_expr_exn
        "02000001d405000764085e036c055f036d0000000325646f046c000000082564656661756c7405010765035d036e050202000001a403210316072e02000000930743036a00000313020000001e020000000403190325072c020000000002000000090200000004034f0327020000000b051f02000000020321034c03170316031e0354034802000000490319033c072c020000002a034807430368010000001b4f6e6c7920746865206f776e65722063616e206f7065726174652e03420327020000000f034f0326051f0200000002031703420200000101051f0200000006031703210317034202000000c303170321053d036d0200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f02000000020320055507640563036e076407650563036e0563036a0764036a076407650563036e0563036a036e020000002f072f020000002307430368010000001842616420636f6e747261637420696e2073746f7261676521032702000000000313053e036a03480346034205330764036a076407650563036e0563036a036e05440563036e034d031b0342034c0316034c0200000012020000000d03210316051f02000000020317051f0200000004034c03420342";
    t.addresses := [ "KT1CjfCztmRpsyUee1nLa9Wcpfr7vgwqRZmk" ]; |}.

Definition expruwujdJkc5y4iPzr83Sd3KrJhzxSUb67JdCZmXNKiTTNvEkMrRU : t :=
  {|
    t.legacy_script_hash :=
      Script_expr_hash.of_b58check_exn
        "expruwujdJkc5y4iPzr83Sd3KrJhzxSUb67JdCZmXNKiTTNvEkMrRU";
    t.patched_code :=
      bin_expr_exn
        "0200000cd705000764085e036c055f036d0000000325646f065f055f055f0362000000082564656661756c7405010765035d036e05020200000ca103210316072e02000000930743036a00000313020000001e020000000403190325072c020000000002000000090200000004034f0327020000000b051f02000000020321034c03170316031e0354034802000000490319033c072c020000002a034807430368010000001b4f6e6c7920746865206f776e65722063616e206f7065726174652e03420327020000000f034f0326051f0200000002031703420200000bfe051f020000000603170321031703420200000bc00321051f0200000002031703160743076507650765036203620765036207650362076503620362055f076507650362036207650362076503620765036203620707070707070000000007070000070700000707000000bf0302000000000200000019051f020000001004210000000a40706172616d65746572034c05520200000a3404580000002a405f706f696e74636f6c6f725f6f6c645f70745f6f6c645f636f6c6f725f6c6973745f736c6173685f33051f020000000203210342032104160000000b40706f696e74636f6c6f72072d02000002270200000014051f020000000b042100000005407461696c034c072d02000001d00200000014051f020000000b042100000005407461696c034c072d02000001510200000014051f020000000b042100000005407461696c034c072d020000001607430368010000000b57726f6e6720706f696e740327020000010b042100000002406e072d02000000e10200000014051f020000000b042100000005407461696c034c072d020000001607430368010000000b57726f6e6720706f696e740327020000009b042100000002406e03300200000039051f0200000030051f0200000027051f020000001e051f0200000015051f020000000c04210000000640636f6c6f72034c034c034c034c034c0342020000004a051f0200000041051f0200000038051f020000002f051f0200000026051f020000001d051f0200000014051f020000000b0421000000054068656164034c034c034c034c034c034c034c0342051f020000000403200320020000001607430368010000000b57726f6e672072616e67650327051f020000000403200320020000004f0743035b00010200000015051f020000000c04210000000640636f6c6f72034c03420200000026051f020000001d051f0200000014051f020000000b0421000000054068656164034c034c034c0342051f02000000040320032002000000270743035b00010200000014051f020000000b0421000000054068656164034c0342053d03620342051f020000000403200320020000002007430765055f03620765055f0362035b0707020000000007070200000000000104580000000f405f7074325f70636f6c6f72325f6e0321020000001003170416000000084070636f6c6f7232072d020000028f0200000012051f020000000904210000000340746c034c072d02000002320200000012051f020000000904210000000340746c034c072d02000001b30200000012051f020000000904210000000340746c034c072d02000001000200000012051f020000000904210000000340746c034c072d020000001607430368010000000b57726f6e6720636f6c6f72032702000000bc04210000000240610200000023051f020000001a051f0200000011051f02000000080421000000024062034c034c034c03420200000035051f020000002c051f0200000023051f020000001a051f0200000011051f02000000080421000000024067034c034c034c034c034c03420200000047051f020000003e051f0200000035051f020000002c051f0200000023051f020000001a051f0200000011051f02000000080421000000024072034c034c034c034c034c034c034c0342051f02000000040320032002000000850743036200bf030200000011051f02000000080421000000024062034c03420200000023051f020000001a051f0200000011051f02000000080421000000024067034c034c034c03420200000035051f020000002c051f0200000023051f020000001a051f0200000011051f02000000080421000000024072034c034c034c034c034c0342051f02000000040320032002000000510743036200bf0307430362000003420200000011051f02000000080421000000024067034c03420200000023051f020000001a051f0200000011051f02000000080421000000024072034c034c034c0342051f020000000403200320020000002f0743036200bf03074303620000034207430362000003420200000011051f02000000080421000000024072034c0342051f0200000004032003200200000024020000000b051f02000000020321034c0317031604170000000a406f6c645f636f6c6f720458000000074070636f6c6f720200000014051f020000000b051f02000000020321034c034c0317041700000005406c697374020000001d051f0200000014051f020000000b051f02000000020321034c034c034c03170316041600000007406f6c645f707403420200000014051f020000000b051f02000000020321034c034c0416000000044070743203420200000014051f020000000b051f02000000020321034c034c020000000a0317041700000002406e034207430359030a0534020000031604580000001540746d705f73686172705f315f736c6173685f333504210000000c40746d705f73686172705f310321041600000002406e020000000b051f02000000020321034c020000000403170317041600000007406f6c645f70740200000014051f020000000b051f02000000020321034c034c020000000403170317041700000005406c697374020000003a051f0200000031051f0200000028051f020000001f051f0200000016051f020000000d0421000000074070636f6c6f72034c034c034c034c034c0200000026051f020000001d051f0200000014051f020000000b051f02000000020321034c034c034c034c020000000c031704160000000440707432072d02000000ef0200000012051f020000000904210000000340746c034c072d020000007c0200000012051f020000000904210000000340746c034c072d020000001c07430368010000001157726f6e6720636f6f7264696e617465730327020000003204210000000240790200000023051f020000001a051f0200000011051f02000000080421000000024078034c034c034c0342051f02000000040320032002000000450200000026051f020000001d051f0200000014051f020000000b051f02000000020321034c034c034c034c03170200000011051f02000000080421000000024078034c0342051f02000000040320032002000000520200000014051f020000000b051f02000000020321034c034c03170743036200010200000026051f020000001d051f0200000014051f020000000b051f02000000020321034c034c034c034c0316031203420458000000034070740200000027051f0200000020051f0200000019051f0200000012051f020000000b051f020000000403200320044200000003407074041b00000005406c697374034c0342053d036203420743035b00010200000014051f020000000b051f02000000020321034c034c034b03420743035b00000200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f020000000203200319032a034203210316051f02000000020317045800000015405f5f6e5f5f7074325f6f6c645f70745f6c6973740200000014051f020000000d051f02000000060320032003200321020000000403170317041700000005406c6973740200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f020000000203200200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f02000000020320020000000403170317041600000007406f6c645f70740342034204580000000f405f5f70745f706172616d65746572051f02000000020320020000000b051f02000000020321034c0555055f07650765036203620765036207650362076503620362020000002e072f020000002207430368010000001742616420636f6e747261637420696e2073746f726167650327020000000003130200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f0200000002032004170000000a40706172616d65746572044d00000003406f70034c053d036d0200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f02000000020320031b0342034c0316034c0200000012020000000d03210316051f02000000020317051f0200000004034c03420342";
    t.addresses := [ "KT1MHDHRLugz3A4qP6KqZDpa7FFmZfcJauV4" ]; |}.

Definition expruZKjVy3JbWcJmjtnvMGvRamkDhMgM3urGGdne3pkN9VKgK7VnD : t :=
  {|
    t.legacy_script_hash :=
      Script_expr_hash.of_b58check_exn
        "expruZKjVy3JbWcJmjtnvMGvRamkDhMgM3urGGdne3pkN9VKgK7VnD";
    t.patched_code :=
      bin_expr_exn
        "0200001dc9050007640764045d0000000d257365745f64656c6567617465046c000000102572656d6f76655f64656c65676174650864046c00000010255f4c69715f656e7472795f6d61696e0764046200000013255f4c69715f656e7472795f73656c6c4f75740764046a00000014255f4c69715f656e7472795f77697468647261770764046c00000013255f4c69715f656e7472795f6465706f7369740865046a000000062573656c6c500765046a000000052562757950046a0000000d25657874726142616c616e6365000000253a707269636555706461746520255f4c69715f656e7472795f757064617465507269636573000000122564656661756c74203a5f656e747269657305010765035d08650860036e0362000000092562616c616e6365730765046800000005256e616d6507650468000000072573796d626f6c076504620000000925646563696d616c73076504620000000c25746f74616c537570706c790765046a0000000825696e42616b65720765046e00000006256f776e65720765046a00000009256275795072696365046a0000000a2573656c6c5072696365000000083a73746f7261676505020200001c1503210316072e02000000b10743036a00000313020000001e020000000403190325072c020000000002000000090200000004034f0327020000000b051f02000000020321034c03170316031e0354034802000000670319033c072c020000002a034807430368010000001b4f6e6c7920746865206f776e65722063616e206f7065726174652e03420327020000002d051f02000000060317053d036d072e02000000080346034e031b0342020000000c0320053e035d034e031b03420200001b54051f020000000603170321031703420200001b160321051f02000000020317031604210000000a40706172616d65746572072e020000055404580000000c406e6f705f736c6173685f330200000025051f020000001c0200000017051f020000000e0421000000084073746f72616765034c034c042100000006407374617465020000001d0317031703170317031703170317041600000009256275795072696365074303620080897a0313043a00000007406d6963726f730322072f020000001507430368010000000a42616420616d6f756e74032702000004a5044800000005406164647204210000000540616464720555036c072f020000003a07430368010000002f43616e6e6f7420757365207468697320636f6e74726163742066726f6d206e6f6e20756e697420636f6e74726163740327020000043a0200000024051f020000001b0200000016051f020000000d04210000000740616d6f756e74034c034c04160000000740746f6b656e73020000003f051f02000000360200000031051f02000000280200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c034c034c03210416000000092562616c616e636573034c03170321041600000005256e616d65034c031703210416000000072573796d626f6c034c0317032104160000000925646563696d616c73034c03170317020000004e051f02000000450200000040051f02000000370200000032051f02000000290200000024051f020000001b0200000016051f020000000d04210000000740746f6b656e73034c034c034c034c034c0200000093051f020000008a0200000085051f020000007c0200000077051f020000006e0200000069051f0200000060020000005b051f0200000052020000004d051f0200000044020000003f051f02000000360200000031051f02000000280200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c034c034c034c034c034c034c034c034c020000001a031703170317031704160000000c25746f74616c537570706c79031204420000000c25746f74616c537570706c79034c04420000000925646563696d616c73034c0442000000072573796d626f6c034c044200000005256e616d65034c04420000000d407331202562616c616e6365730317020000004d051f0200000044020000003f051f02000000360200000031051f02000000280200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c034c034c034c0416000000092562616c616e636573020000005b051f0200000052020000004d051f0200000044020000003f051f02000000360200000031051f02000000280200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c034c034c034c034c0416000000092562616c616e636573020000004c051f0200000043020000003e051f02000000350200000030051f02000000270200000022051f02000000190200000014051f020000000b0421000000054061646472034c034c034c034c034c0329072f0200000006074303620000020000000004580000000540686176650200000032051f02000000290200000024051f020000001b0200000016051f020000000d04210000000740746f6b656e73034c034c034c0312020000004c051f0200000043020000003e051f02000000350200000030051f02000000270200000022051f02000000190200000014051f020000000b0421000000054061646472034c034c034c034c034c051f02000000020346051f0200000019051f0200000012051f020000000b051f020000000403200320035004420000000d407332202562616c616e636573053d036d0342051f020000000403200320051f020000000403200320020000158e072e02000008d004580000001040616d6f756e745f736c6173685f31340200000025051f020000001c0200000017051f020000000e0421000000084073746f72616765034c034c0743036a0080c0a8ca9a3a0743036a0080897a0200000032051f02000000290200000024051f020000001b0200000016051f020000000d04210000000740616d6f756e74034c034c034c043a00000005407a616d740322072f020000001507430368010000000a62616420616d6f756e740327020000080d04480000000540616464720743036a0000041300000009407478416d6f756e740319033c072c020000003207430368010000002763616e6e6f742062757920616e642073656c6c20696e2073616d65207472616e73616374696f6e032702000007a00200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c0416000000092562616c616e6365730200000014051f020000000b0421000000054061646472034c0329072f0200000006074303620000020000000004580000000540686176650421000000054068617665020000004e051f02000000450200000040051f02000000370200000032051f02000000290200000024051f020000001b0200000016051f020000000d04210000000740616d6f756e74034c034c034c034c034c0319032a072c020000003507430368010000002a546865206164647265737320646f6573206e6f7420686176652074686174206d7563682073746f726564032702000006850200000014051f020000000b0421000000054061646472034c0555036c072f02000000480200000014051f020000000b0421000000054061646472034c07430368010000002243616e6e6f74207265636f76657220626f6f6c20636f6e74726163742066726f6d3a034203270200000614020000004e051f02000000450200000040051f02000000370200000032051f02000000290200000024051f020000001b0200000016051f020000000d04210000000740616d6f756e74034c034c034c034c034c020000004d051f0200000044020000003f051f02000000360200000031051f02000000280200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c034c034c034c020000001a031703170317031704160000000c25746f74616c537570706c79034b03210311034c0328072c020000051c0200000013051f020000000a04210000000440647374034c020000005b051f0200000052020000004d051f0200000044020000003f051f02000000360200000031051f02000000280200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c034c034c034c034c020000001e031703170317031703170317031704170000000a2573656c6c50726963650200000051051f02000000480200000043051f020000003a0200000035051f020000002c0200000027051f020000001e0200000019051f0200000010020000000b051f02000000020321034c034c034c034c034c034c04160000000a406e6f6e4d6963726f73043a0000000740746f53656e64034f044d00000003406f70020000006a051f0200000061020000005c051f0200000053020000004e051f02000000450200000040051f02000000370200000032051f02000000290200000024051f020000001b0200000016051f020000000d04210000000740616d6f756e74034c034c034c034c034c034c034c020000003e051f02000000350200000030051f02000000270200000022051f02000000190200000014051f020000000b0421000000054068617665034c034c034c034c034b03210311034c0328072c020000031b0200000069051f0200000060020000005b051f0200000052020000004d051f0200000044020000003f051f02000000360200000031051f02000000280200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c034c034c034c034c034c03210416000000092562616c616e636573034c03170321041600000005256e616d65034c031703210416000000072573796d626f6c034c0317032104160000000925646563696d616c73034c03170317020000006d051f0200000064020000005f051f02000000560200000051051f02000000480200000043051f020000003a0200000035051f020000002c0200000027051f020000001e0200000019051f020000001004210000000a406e6577537570706c79034c034c034c034c034c034c034c04420000000c25746f74616c537570706c79034c04420000000925646563696d616c73034c0442000000072573796d626f6c034c044200000005256e616d65034c04420000000d407331202562616c616e63657303170200000077051f020000006e0200000069051f0200000060020000005b051f0200000052020000004d051f0200000044020000003f051f02000000360200000031051f02000000280200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c034c034c034c034c034c034c0416000000092562616c616e6365730200000028051f020000001f020000001a051f020000001104210000000b406e657742616c616e6365034c034c0200000076051f020000006d0200000068051f020000005f020000005a051f0200000051020000004c051f0200000043020000003e051f02000000350200000030051f02000000270200000022051f02000000190200000014051f020000000b0421000000054061646472034c034c034c034c034c034c034c034c051f02000000020346051f0200000017051f0200000010051f0200000009051f02000000020320035004420000000d407332202562616c616e636573053d036d0200000019051f0200000010020000000b051f02000000020321034c034c031b0342020000001507430368010000000a62616420616d6f756e740327051f020000000403200320020000001507430368010000000a62616420616d6f756e740327051f02000000020320051f02000000020320051f020000000403200320051f0200000004032003200200000cb2072e020000034f04580000000d40616d745f736c6173685f33330200000025051f020000001c0200000017051f020000000e0421000000084073746f72616765034c034c0743035d0100000024747a314c42454b5861785162643547747a62633141544377633370707075383161574763041e0000000540646573740200000021051f02000000180200000013051f020000000a04210000000440616d74034c034c034f044d00000003406f700200000015051f020000000c042100000006407374617465034c0200000018031703170317031703170317041600000006256f776e657204470000000540616464720319033c072c02000000220743036801000000174f6e6c79206f776e65722063616e207769746864726177032702000002280200000015051f020000000c042100000006407374617465034c03210416000000092562616c616e636573034c03170321041600000005256e616d65034c031703210416000000072573796d626f6c034c0317032104160000000925646563696d616c73034c0317032104160000000c25746f74616c537570706c79034c031703170200000075051f020000006c0200000067051f020000005e0200000059051f0200000050020000004b051f0200000042020000003d051f0200000034020000002f051f02000000260200000021051f02000000180200000013051f020000000a04210000000440616d74034c034c034c034c034c034c034c034c0200000077051f020000006e0200000069051f0200000060020000005b051f0200000052020000004d051f0200000044020000003f051f02000000360200000031051f02000000280200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c034c034c034c034c034c034c02000000180317031703170317031704160000000825696e42616b6572031204420000000825696e42616b6572034c04420000000c25746f74616c537570706c79034c04420000000925646563696d616c73034c0442000000072573796d626f6c034c044200000005256e616d65034c04420000000d407331202562616c616e636573053d036d0200000020051f02000000170200000012051f0200000009042100000003406f70034c034c031b0342051f02000000060320032003200200000957072e020000024b04580000000d406e6f705f736c6173685f33390200000025051f020000001c0200000017051f020000000e0421000000084073746f72616765034c034c0421000000064073746174650200000018031703170317031703170317041600000006256f776e657204470000000540616464720319033c072c02000000210743036801000000164f6e6c79206f776e65722063616e206465706f7369740327020000019e04210000000640737461746503210416000000092562616c616e636573034c03170321041600000005256e616d65034c031703210416000000072573796d626f6c034c0317032104160000000925646563696d616c73034c0317032104160000000c25746f74616c537570706c79034c0317031704130000000740616d6f756e740200000069051f0200000060020000005b051f0200000052020000004d051f0200000044020000003f051f02000000360200000031051f02000000280200000023051f020000001a0200000015051f020000000c042100000006407374617465034c034c034c034c034c034c034c02000000180317031703170317031704160000000825696e42616b65720393072f020000001a07430368010000000f6e65676174697665206d7574657a210327020000000004420000000825696e42616b6572034c04420000000c25746f74616c537570706c79034c04420000000925646563696d616c73034c0442000000072573796d626f6c034c044200000005256e616d65034c04420000000d407331202562616c616e636573053d036d0342051f020000000403200320020000070004580000000e40696e666f5f736c6173685f34340200000025051f020000001c0200000017051f020000000e0421000000084073746f72616765034c034c04210000000640737461746503210416000000092562616c616e636573034c03170321041600000005256e616d65034c031703210416000000072573796d626f6c034c0317032104160000000925646563696d616c73034c0317032104160000000c25746f74616c537570706c79034c0317032104160000000825696e42616b6572034c03170321041600000006256f776e6572034c03170416000000092562757950726963650200000084051f020000007b0200000076051f020000006d0200000068051f020000005f020000005a051f0200000051020000004c051f0200000043020000003e051f02000000350200000030051f02000000270200000022051f02000000190200000014051f020000000b04210000000540696e666f034c034c034c034c034c034c034c034c034c0416000000062573656c6c50034c044200000014256275795072696365202573656c6c5072696365034c044200000006256f776e6572034c04420000000825696e42616b6572034c04420000000c25746f74616c537570706c79034c04420000000925646563696d616c73034c0442000000072573796d626f6c034c044200000005256e616d65034c04420000000d407331202562616c616e63657303210416000000092562616c616e636573034c03170321041600000005256e616d65034c031703210416000000072573796d626f6c034c0317032104160000000925646563696d616c73034c0317032104160000000c25746f74616c537570706c79034c0317032104160000000825696e42616b6572034c03170321041600000006256f776e6572034c031704170000000a2573656c6c50726963650200000084051f020000007b0200000076051f020000006d0200000068051f020000005f020000005a051f0200000051020000004c051f0200000043020000003e051f02000000350200000030051f02000000270200000022051f02000000190200000014051f020000000b04210000000540696e666f034c034c034c034c034c034c034c034c034c020000000d03170416000000052562757950044200000014256275795072696365202573656c6c5072696365034c044200000006256f776e6572034c04420000000825696e42616b6572034c04420000000c25746f74616c537570706c79034c04420000000925646563696d616c73034c0442000000072573796d626f6c034c044200000005256e616d65034c04420000000d407332202562616c616e6365730200000022051f02000000190200000014051f020000000b04210000000540696e666f034c034c0416000000062573656c6c500200000030051f02000000270200000022051f02000000190200000014051f020000000b04210000000540696e666f034c034c034c020000000d0317041600000005256275795003190337072c020000002b074303680100000020696e76616c69642070726963652c20656e61626c6573206172626974726167650327020000026f0200000015051f020000000c042100000006407374617465034c0200000018031703170317031703170317041600000006256f776e657204470000000540616464720319033c072c02000000230743036801000000184f6e6c79206f776e65722063616e20736574207072696365032702000001fa04210000000340733203210416000000092562616c616e636573034c03170321041600000005256e616d65034c031703210416000000072573796d626f6c034c0317032104160000000925646563696d616c73034c0317032104160000000c25746f74616c537570706c79034c031703170200000076051f020000006d0200000068051f020000005f020000005a051f0200000051020000004c051f0200000043020000003e051f02000000350200000030051f02000000270200000022051f02000000190200000014051f020000000b04210000000540696e666f034c034c034c034c034c034c034c034c0200000015031704170000000d25657874726142616c616e63650200000066051f020000005d0200000058051f020000004f020000004a051f0200000041020000003c051f0200000033020000002e051f02000000250200000020051f02000000170200000012051f0200000009042100000003407332034c034c034c034c034c034c034c02000000180317031703170317031704160000000825696e42616b6572031204420000000825696e42616b6572034c04420000000c25746f74616c537570706c79034c04420000000925646563696d616c73034c0442000000072573796d626f6c034c044200000005256e616d65034c04420000000d407333202562616c616e636573053d036d0342051f0200000006032003200320051f020000000403200320034c0316034c0200000012020000000d03210316051f02000000020317051f0200000004034c03420342";
    t.addresses := [ "KT1BvVxWM6cjFuJNet4R9m64VDCN2iMvjuGE" ]; |}.

Definition exprv98vtze1uwbDXdpb27R8RQabWZMZDXGNAwaAZwCg6WSvXu8fw3 : t :=
  {|
    t.legacy_script_hash :=
      Script_expr_hash.of_b58check_exn
        "exprv98vtze1uwbDXdpb27R8RQabWZMZDXGNAwaAZwCg6WSvXu8fw3";
    t.patched_code :=
      bin_expr_exn
        "0200000cd305000764085e036c055f036d0000000325646f065f055f055f0362000000082564656661756c7405010765035d036e05020200000c9d03210316072e02000000930743036a00000313020000001e020000000403190325072c020000000002000000090200000004034f0327020000000b051f02000000020321034c03170316031e0354034802000000490319033c072c020000002a034807430368010000001b4f6e6c7920746865206f776e65722063616e206f7065726174652e03420327020000000f034f0326051f0200000002031703420200000bfa051f020000000603170321031703420200000bbc0321051f0200000002031703160743076507650765036203620765036207650362076503620362055f076507650362036207650362076503620765036203620707070707070000000007070000070700000707000000bf0302000000000200000019051f020000001004210000000a40706172616d65746572034c05520200000a3004580000002a405f706f696e74636f6c6f725f6f6c645f70745f6f6c645f636f6c6f725f6c6973745f736c6173685f33051f020000000203210342032104160000000b40706f696e74636f6c6f72072d02000002270200000014051f020000000b042100000005407461696c034c072d02000001d00200000014051f020000000b042100000005407461696c034c072d02000001510200000014051f020000000b042100000005407461696c034c072d020000001607430368010000000b57726f6e6720706f696e740327020000010b042100000002406e072d02000000e10200000014051f020000000b042100000005407461696c034c072d020000001607430368010000000b57726f6e6720706f696e740327020000009b042100000002406e03300200000039051f0200000030051f0200000027051f020000001e051f0200000015051f020000000c04210000000640636f6c6f72034c034c034c034c034c0342020000004a051f0200000041051f0200000038051f020000002f051f0200000026051f020000001d051f0200000014051f020000000b0421000000054068656164034c034c034c034c034c034c034c0342051f020000000403200320020000001607430368010000000b57726f6e672072616e67650327051f020000000403200320020000004f0743035b00010200000015051f020000000c04210000000640636f6c6f72034c03420200000026051f020000001d051f0200000014051f020000000b0421000000054068656164034c034c034c0342051f02000000040320032002000000270743035b00010200000014051f020000000b0421000000054068656164034c0342053d03620342051f020000000403200320020000002007430765055f03620765055f0362035b0707020000000007070200000000000104580000000f405f7074325f70636f6c6f72325f6e0321020000001003170416000000084070636f6c6f7232072d020000028f0200000012051f020000000904210000000340746c034c072d02000002320200000012051f020000000904210000000340746c034c072d02000001b30200000012051f020000000904210000000340746c034c072d02000001000200000012051f020000000904210000000340746c034c072d020000001607430368010000000b57726f6e6720636f6c6f72032702000000bc04210000000240610200000023051f020000001a051f0200000011051f02000000080421000000024062034c034c034c03420200000035051f020000002c051f0200000023051f020000001a051f0200000011051f02000000080421000000024067034c034c034c034c034c03420200000047051f020000003e051f0200000035051f020000002c051f0200000023051f020000001a051f0200000011051f02000000080421000000024072034c034c034c034c034c034c034c0342051f02000000040320032002000000850743036200bf030200000011051f02000000080421000000024062034c03420200000023051f020000001a051f0200000011051f02000000080421000000024067034c034c034c03420200000035051f020000002c051f0200000023051f020000001a051f0200000011051f02000000080421000000024072034c034c034c034c034c0342051f02000000040320032002000000510743036200bf0307430362000003420200000011051f02000000080421000000024067034c03420200000023051f020000001a051f0200000011051f02000000080421000000024072034c034c034c0342051f020000000403200320020000002f0743036200bf03074303620000034207430362000003420200000011051f02000000080421000000024072034c0342051f0200000004032003200200000024020000000b051f02000000020321034c0317031604170000000a406f6c645f636f6c6f720458000000074070636f6c6f720200000014051f020000000b051f02000000020321034c034c0317041700000005406c697374020000001d051f0200000014051f020000000b051f02000000020321034c034c034c03170316041600000007406f6c645f707403420200000014051f020000000b051f02000000020321034c034c0416000000044070743203420200000014051f020000000b051f02000000020321034c034c020000000a0317041700000002406e034207430359030a0534020000031204580000001540746d705f73686172705f315f736c6173685f333504210000000c40746d705f73686172705f310321020000000403170317041600000007406f6c645f7074020000000b051f02000000020321034c020000000c031704160000000440707432072d02000000dd0200000012051f020000000904210000000340746c034c072d020000007c0200000012051f020000000904210000000340746c034c072d020000001c07430368010000001157726f6e6720636f6f7264696e617465730327020000003204210000000240790200000023051f020000001a051f0200000011051f02000000080421000000024078034c034c034c0342051f02000000040320032002000000330200000014051f020000000b051f02000000020321034c034c03170200000011051f02000000080421000000024078034c0342051f0200000004032003200200000029032103170743036200010200000014051f020000000b051f02000000020321034c034c031603120342051f020000000203200200000010051f0200000009051f020000000203200458000000034070740743035b00010200000014051f020000000b051f02000000020321034c034c041600000002406e044b00000002406e0200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f02000000020320020000000403170317041700000005406c697374020000001d051f0200000014051f020000000b051f02000000020321034c034c034c020000001d051f0200000014051f020000000b051f02000000020321034c034c034c0442000000094070745f636f6c6f72041b00000005406c6973740200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f020000000203200342053d03620342020000000b051f02000000020321034c03420743035b00000200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f020000000203200319032a034203210316051f020000000203170200000014051f020000000d051f0200000006032003200320045800000015405f5f6e5f5f7074325f6f6c645f70745f6c6973740321020000000403170317041700000005406c6973740200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f020000000203200200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f02000000020320020000000403170317041600000007406f6c645f707403420342051f0200000002032004580000000f405f5f70745f706172616d65746572020000000b051f02000000020321034c0555055f07650765036203620765036207650362076503620362020000002e072f020000002207430368010000001742616420636f6e747261637420696e2073746f726167650327020000000003130200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f0200000002032004170000000a40706172616d65746572044d00000003406f70034c053d036d0200000014051f020000000b051f02000000020321034c034c0200000017051f0200000010051f0200000009051f02000000020320031b0342034c0316034c0200000012020000000d03210316051f02000000020317051f0200000004034c03420342";
    t.addresses := [ "KT1PyX9b8WmShQjqNgDQsvxqj9UYdmHLr3xg" ]; |}.

Definition expru1ukk6ZqdA32rFYFG7j1eGjfsatbdUZWz8Mi1kXWZYRZm4FZVe : t :=
  {|
    t.legacy_script_hash :=
      Script_expr_hash.of_b58check_exn
        "expru1ukk6ZqdA32rFYFG7j1eGjfsatbdUZWz8Mi1kXWZYRZm4FZVe";
    t.patched_code :=
      bin_expr_exn
        (Pervasives.op_caret
          "0200002f0405000764076407640865046e000000083a7370656e646572076504620000000a3a616c6c6f77616e63650462000000113a63757272656e74416c6c6f77616e63650000000825617070726f766508650765046e000000063a6f776e657204620000000d3a6d696e4c71744d696e74656407650462000000133a6d6178546f6b656e734465706f7369746564046b000000093a646561646c696e650000000d256164644c6971756964697479076408650765046e000000063a6f776e65720765046e000000033a746f04620000000a3a6c71744275726e65640765046a000000103a6d696e58747a57697468647261776e07650462000000133a6d696e546f6b656e7357697468647261776e046b000000093a646561646c696e65000000102572656d6f76654c697175696469747907640865046e000000033a746f07650462000000103a6d696e546f6b656e73426f75676874046b000000093a646561646c696e650000000b2578747a546f546f6b656e08650765046e000000063a6f776e6572046e000000033a746f076504620000000b3a746f6b656e73536f6c640765046a0000000d3a6d696e58747a426f75676874046b000000093a646561646c696e650000000b25746f6b656e546f58747a0764076408650765046e000000153a6f7574707574446578746572436f6e747261637407650462000000103a6d696e546f6b656e73426f75676874046e000000063a6f776e65720765046e000000033a746f076504620000000b3a746f6b656e73536f6c64046b000000093a646561646c696e650000000d25746f6b656e546f546f6b656e0764045d0000001025757064617465546f6b656e506f6f6c04620000001825757064617465546f6b656e506f6f6c496e7465726e616c076408650563035d0359000000092573657442616b65720764046e0000000b257365744d616e61676572046c000000082564656661756c74050107650861046e000000063a6f776e657207650462000000083a62616c616e63650760046e000000083a7370656e64657204620000000a3a616c6c6f77616e636500000009256163636f756e7473076507650459000000183a73656c6649735570646174696e67546f6b656e506f6f6c076504590000000c3a667265657a6542616b65720462000000093a6c7174546f74616c07650765046e000000083a6d616e61676572046e0000000d3a746f6b656e41646472657373076504620000000a3a746f6b656e506f6f6c046a000000083a78747a506f6f6c05020200002b61055707650764076407640765036e07650362036207650765036e036207650362036b076407650765036e0765036e03620765036a07650362036b07640765036e07650362036b07650765036e036e076503620765036a036b0764076407650765036e07650362036e0765036e07650362036b0764035d0362076407650563035d03590764036e036c07650761036e076503620760036e036207650765035907650359036207650765036e036e07650362036a03210316051f02000000020317072e0200001e3d072e0200000b73072e02000001c1051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327051f02000000020321034c031603480329072f020000000e0723036e03620743036200000342020000000003210317071f0002020000000203210570000203160329072f02000000060743036200000200000000071f000202000000020321057000020317031703190325072c020000000002000000630743036801000000585468652063757272656e7420616c6c6f77616e636520706172616d65746572206d75737420657175616c207468652073656e64657227732063757272656e7420616c6c6f77616e636520666f7220746865206f776e65722e0327032103170570000203210316051f02000000060317031603460350051f020000000d0321051f020000000203160317034c0320034c0342051f020000000403210316034603480350051f020000000d0321051f020000000203170316034c03200342053d036d034202000009a6051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e03270200000000032103170317034003190337072c0200000000020000002807430368010000001d4e4f572069732067726561746572207468616e20646561646c696e652e032703210317031607430362000003190337072c0200000000020000003807430368010000002d6d6178546f6b656e734465706f7369746564206d7573742062652067726561746572207468616e207a65726f2e032703210316031707430362000003190337072c020000000002000000320743036801000000276d696e4c71744d696e746564206d7573742062652067726561746572207468616e207a65726f2e03270743036a000003130319032a072c0200000000020000002c074303680100000021416d6f756e74206d7573742062652067726561746572207468616e207a65726f2e0327051f02000000020321034c031703160317031703300325072c020000032f03130743036a0080897a03190332072c0200000000020000004f07430368010000004454686520696e697469616c206c697175696469747920616d6f756e74206d7573742062652067726561746572207468616e206f7220657175616c20746f20312058545a2e0327034c0313051f02000000060743036a00010322072f020000000b0743036801000000000327020000000203160321051f0200000071051f020000000403210317051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c03420342051f020000000d0321051f020000000203160317034c0320034c0342034c071f0002020000000203210570000203160316051f0200000004032103160329072f020000000e0723036e03620743036200000342020000000005700002051f020000000d0321051f020000000203170316034c03200342051f0200000004032103160346071f00030200000002032105700003031603160350051f020000000d0321051f020000000203170316034c032003420321031703170317031703130312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c034203210317031703170316071f00020200000002032105700002031703160312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342051f0200000011032103170316051f0200000004031603160321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a0000057000030349035405700005051f020000000203420342034d051f0200000004053d036d031b034202000004e6051f02000000020321034c0317031703170317051f02000000060743036a00010322072f020000000b0743036801000000000327020000000203160313051f02000000060743036a00010322072f020000000b0743036801000000000327020000000203160321071f000402000000020321057000040317031703170316033a071f00020200000002032105700002034c0322072f020000001507430368010000000a64697642795a65726f2e0327020000002703210316051f02000000020317034c03300325072c020000000002000000080743036200010312032107430362000003190337072c02000000000200000023074303680100000018746f6b656e734465706f7369746564206973207a65726f2e0327034c071f000402000000020321057000040317031603170317033a051f0200000002034c0322072f0200000002032702000000020316071f0002020000000203210570000203160317051f0200000002032103190332072c020000000002000000430743036801000000386c71744d696e746564206d7573742062652067726561746572207468616e206f7220657175616c20746f206d696e4c71744d696e7465642e0327051f0200000066051f02000000020321034c03170316051f0200000002032103190328072c0200000000020000003e074303680100000033746f6b656e734465706f73697465642069732067726561746572207468616e206d6178546f6b656e734465706f73697465642e0327071f00030200000002032105700003071f0003020000000203210570000303160316051f020000000203160329072f020000000e0723036e03620743036200000342020000000003210316071f000202000000020321057000020312051f020000000d0321051f020000000203170316034c032003420346071f0003020000000203210570000303160316051f020000000f051f020000000805700003032103160350051f020000000d0321051f020000000203170316034c0320034203210317031603170317057000020312051f020000000403210317051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c03420342051f020000000d0321051f020000000203160317034c0320034c03420321031703170317031703130312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c034203210317031703170316071f000202000000020321057000020312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342051f020000000b051f0200000004031603160321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a0000057000030349035405700005051f020000000203420342034d051f0200000004053d036d031b034202000012be072e020000090b051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000321031703170317034003190337072c0200000000020000002807430368010000001d4e4f572069732067726561746572207468616e20646561646c696e652e03270743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e03270321031703160743036a000003190337072c0200000000020000003507430368010000002a6d696e58747a57697468647261776e206d7573742062652067726561746572207468616e207a65726f2e0327032103170317031607430362000003190337072c0200000000020000003807430368010000002d6d696e546f6b656e7357697468647261776e206d7573742062652067726561746572207468616e207a65726f2e0327032103160317031707430362000003190337072c0200000000020000002f0743036801000000246c71744275726e6564206d7573742062652067726561746572207468616e207a65726f2e0327032103160316051f020000000d051f02000000020321034c03160329072f02000000220743036801000000176f776e657220686173206e6f206c69717569646974792e03270200000000034c0321031603170317071f00020200000002032105700002031603190328072c0200000000020000003507430368010000002a6c71744275726e65642069732067726561746572207468616e206f776e657227732062616c616e63652e0327032103160316034803190325072c0200000004034c03160200000132034c0321031703480329072f020000002a07430368010000001f73656e64657220686173206e6f20617070726f76616c2062616c616e63652e03270200000000051f0200000017034c0321031603170317051f02000000060743035b0000034b0321051f020000004b03190328072c0200000000020000003b07430368010000003073656e64657220617070726f76616c2062616c616e6365206973206c657373207468616e204c5154206275726e65642e03270311034605700002032103170570000203480350051f020000000d0321051f020000000203160317034c0320034c034203210316051f0200000043034605710001032103160316034c051f020000002e051f020000000b051f0200000004032103160350051f020000000d0321051f020000000203170316034c03200342051f02000000020321034c031603170317071f000302000000020321057000030317031703170317051f02000000060743036a00010322072f020000000b074303680100000000032702000000020316033a051f0200000017071f0002020000000203210570000203170316031703170322072f020000001507430368010000000a64697642795a65726f2e0327020000000203160743036a0001033a0321071f000302000000020321057000030317031603190332072c0200000000020000003507430368010000002a78747a57697468647261776e206973206c657373207468616e206d696e58747a57697468647261776e2e0327071f00020200000002032105700002031603170317051f0200000023071f0003020000000203210570000303210317031603170317034c0317031703170316033a0322072f020000001507430368010000000a64697642795a65726f2e0327020000000203160321071f0004020000000203210570000403170317031603190332072c0200000000020000003b074303680100000030746f6b656e7357697468647261776e206973206c657373207468616e206d696e546f6b656e7357697468647261776e2e0327071f0003020000000203210570000303160317031705700003034b03210743035b000003190332072c02000000020311020000000b0743036801000000000327057000040321071f0005020000000203210570000503160316051f020000000203160329072f020000000e0723036e03620743036200000342020000000005700002051f020000000d0321051f020000000203170316034c03200342051f0200000004032103160346071f00050200000002032105700005031603160350051f020000000d0321051f020000000203170316034c0320034203210317031603170317071f00040200000002032105700004031603170317034c034b03210743035b000003190332072c02000000020311020000000b0743036801000000000327051f020000000403210317051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c03420342051f020000000d0321051f020000000203160317034c0320034c034203210317031703170316071f00020200000002032105700002034c034b03210743035b000003190332072c02000000020311020000000"
          "b0743036801000000000327051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c034203210317031703170317071f00030200000002032105700003034c0393072f020000001a07430368010000000f6e65676174697665206d7574657a2103270200000000051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342071f000302000000020321057000030316031703160555036c072f020000000403170327020000000005700003034f034d051f020000005f051f020000000d051f02000000060316031703160321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a000005700003057000040342034903540342034d053d036d034c031b034c031b034202000009a7072e020000049c051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e03270200000000032103170317034003190337072c0200000000020000002807430368010000001d4e4f572069732067726561746572207468616e20646561646c696e652e03270743036a000003130319032a072c0200000000020000002c074303680100000021416d6f756e74206d7573742062652067726561746572207468616e207a65726f2e032703210317031607430362000003190337072c0200000000020000003507430368010000002a6d696e546f6b656e73426f75676874206d7573742062652067726561746572207468616e207a65726f2e0327051f020000004d032103170317031703170743036a000003190337072c0200000000020000002d07430368010000002278747a506f6f6c206d7573742062652067726561746572207468616e207a65726f2e0327051f020000004e0321031703170317031607430362000003190337072c0200000000020000002e074303680100000023746f6b656e506f6f6c206d7573742062652067726561746572207468616e207a65726f0327051f02000000020321034c0317031703170317051f02000000060743036a00010322072f020000000b0743036801000000000327020000000203160743036200a80f033a0313051f02000000060743036a00010322072f020000000b0743036801000000000327020000000203160321051f020000000b0743036200a50f033a03120743036200a50f033a071f000302000000020321057000030317031703170316033a0322072f020000001507430368010000000a64697642795a65726f2e0327020000000203160321051f0200000052051f020000000603210317031603190328072c0200000000020000003507430368010000002a746f6b656e73426f75676874206973206c657373207468616e206d696e546f6b656e73426f756768742e03270321071f000302000000020321057000030317031703170316034b03210743035b000003190332072c02000000020311020000000b0743036801000000000327051f020000000405700002051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c03420321031703170317031703130312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342051f020000000d051f02000000060316034903540321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a0000057000030570000505700005051f020000000203420342034d051f0200000004053d036d031b034202000004ff051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000321031703170317034003190337072c0200000000020000002807430368010000001d4e4f572069732067726561746572207468616e20646561646c696e652e03270743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327051f020000004d032103170317031703170743036a000003190337072c0200000000020000002d07430368010000002278747a506f6f6c206d7573742062652067726561746572207468616e207a65726f2e0327051f020000004e0321031703170317031607430362000003190337072c0200000000020000002e074303680100000023746f6b656e506f6f6c206d7573742062652067726561746572207468616e207a65726f032703210317031607430362000003190337072c0200000000020000001d074303680100000012746f6b656e73536f6c64206973207a65726f032703210317031703160743036a000003190337072c020000000002000000320743036801000000276d696e58747a426f75676874206d7573742062652067726561746572207468616e207a65726f2e03270321031703160743036200a50f033a071f0002020000000203210570000203170317031703160743036200a80f033a0312051f02000000020321034c031703160743036200a50f033a071f000302000000020321057000030317031703170317051f02000000060743036a00010322072f020000000b074303680100000000032702000000020316033a0322072f020000001507430368010000000a64697642795a65726f2e0327020000000203160743036a0001033a0321051f020000004e051f0200000008032103170317031603190328072c0200000000020000002f07430368010000002478747a426f75676874206973206c657373207468616e206d696e58747a426f756768742e0327051f0200000092034c03210317031703170316071f00020200000002032105700002031703160312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c03420321051f02000000ae051f020000000a03210317031703170317034c0393072f020000001a07430368010000000f6e65676174697665206d7574657a2103270200000000051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342071f00020200000002032105700002031603170555036c072f02000000020327020000000005700001034f034d051f020000006a051f0200000011032103170316051f0200000004031603160321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a0000057000030349035405700005051f020000000203420342034d053d036d05700002031b034c031b03420200000c59072e0200000867072e0200000517051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e03270321031703170317034003190337072c0200000000020000002807430368010000001d4e4f572069732067726561746572207468616e20646561646c696e652e0327032103170317031607430362000003190337072c0200000000020000001d074303680100000012746f6b656e73536f6c64206973207a65726f0327032103160317031607430362000003190337072c0200000000020000003507430368010000002a6d696e546f6b656e73426f75676874206d7573742062652067726561746572207468616e207a65726f2e0327051f020000004d032103170317031703170743036a000003190337072c0200000000020000002d07430368010000002278747a506f6f6c206d7573742062652067726561746572207468616e207a65726f2e0327051f020000004e0321031703170317031607430362000003190337072c0200000000020000002e074303680100000023746f6b656e506f6f6c206d7573742062652067726561746572207468616e207a65726f032703210317031703160743036200a50f033a071f0002020000000203210570000203170317031703160743036200a80f033a0312051f02000000020321034c0317031703160743036200a50f033a071f000302000000020321057000030317031703170317051f02000000060743036a00010322072f020000000b074303680100000000032702000000020316033a0322072f020000001507430368010000000a64697642795a65726f2e0327020000000203160743036a0001033a051f02000000020321034c031703170316071f0003020000000203210570000303170317031703160312051f020000000405700002051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c034203210317031703170317071f00020200000002032105700002034c0393072f020000001a07430368010000000f6e65676174697665206d7574657a2103270200000000051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342071f000202000000020321057000020316031606550765036e07650362036b0000000b2578747a546f546f6b656e072f020000000403170327020000000005700002071f00030200000002032105700003032103170316051f02000000190321031603170316051f0200000008032103170317031703420342034c0320034d034c051f0200000017034c0321031703170316051f02000000060316031703170321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a0000057000030349035405700005051f020000000203420342034d053d036d034c031b051f0200000002034c034c031b03420200000344072e02000001720743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327031e0354034803190325072c02000000000200000020074303680100000015756e73616665557064617465546f6b656e506f6f6c03270321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000321031707430359030a051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203170316034c032003420342051f020000000d0321051f020000000203160317034c0320034c03420321031703170316031706550765036e055a03620000000b2567657442616c616e6365072f02000000040317032702000000000743036a000004490000001825757064617465546f6b656e506f6f6c496e7465726e616c034903540342034d051f0200000004053d036d031b034202000001c60743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327051f02000000020321034c031703160316072c0200000000020000003207430368010000002744657874657220646964206e6f7420696e6974696174652074686973206f7065726174696f6e2e0327051f02000000020321034c0317031703160317034803190325072c0200000000020000004e0743036801000000435468652073656e646572206973206e6f742074686520746f6b656e20636f6e7472616374206173736f6369617465642077697468207468697320636f6e74726163742e0327051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c034203210317074303590303051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203170316034c032003420342051f020000000d0321051f020000000203160317034c0320034c0342053d036d034202000003e6072e02000001bd051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327051f02000000020321034c0317031703160316034803190325072c0200000000020000002e07430368010000002373656e646572206973206e6f742074686520636f6e7472616374206d616e616765722e0327051f02000000020321034c0317031603170316033f072c0200000000020000003d07430368010000003243616e6e6f74206368616e6765207468652062616b6572207768696c6520667265657a6542616b657220697320747275652e032703210316051f02000000020317034e051f0200000073051f020000000403210317051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c03420342051f020000000d0321051f020000000203160317034c0320034c0342053d036d031b0342020000021d072e0200000147051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327051f02000000020321034c0317031703160316034803190325072c0200000000020000002e07430368010000002373656e646572206973206e6f742074686520636f6e7472616374206d616e616765722e0327051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203170316034c032003420342034c0342051f020000000d0321051f020000000203160317034c0320034c0342053d036d034202000000ca03200321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000321031703170317031703130312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342053d036d0342");
    t.addresses :=
      [
        "KT1XTXBsEauzcv3uPvVXW92mVqrx99UGsb9T";
        "KT1Puc9St8wdNoGtLiD2WXaHbWU7styaxYhD";
        "KT19c8n5mWrqpxMcR3J687yssHxotj88nGhZ";
        "KT1DrJV8vhkdLEj76h1H9Q4irZDqAkMPo1Qf";
        "KT1D68BvUm9N1fcq6uaZnyZvmBkBvj9biyPu"
      ]; |}.

Definition exprubv5oQmAUP8BwktmDgMWqTizYDJVhzHhJESGZhJ2GkHESZ1VWg : t :=
  {|
    t.legacy_script_hash :=
      Script_expr_hash.of_b58check_exn
        "exprubv5oQmAUP8BwktmDgMWqTizYDJVhzHhJESGZhJ2GkHESZ1VWg";
    t.patched_code :=
      bin_expr_exn
        (Pervasives.op_caret
          "0200002c6905000764076407640865046e000000083a7370656e646572076504620000000a3a616c6c6f77616e63650462000000113a63757272656e74416c6c6f77616e63650000000825617070726f766508650765046e000000063a6f776e657204620000000d3a6d696e4c71744d696e74656407650462000000133a6d6178546f6b656e734465706f7369746564046b000000093a646561646c696e650000000d256164644c6971756964697479076408650765046e000000063a6f776e65720765046e000000033a746f04620000000a3a6c71744275726e65640765046a000000103a6d696e58747a57697468647261776e07650462000000133a6d696e546f6b656e7357697468647261776e046b000000093a646561646c696e65000000102572656d6f76654c697175696469747907640865046e000000033a746f07650462000000103a6d696e546f6b656e73426f75676874046b000000093a646561646c696e650000000b2578747a546f546f6b656e08650765046e000000063a6f776e6572046e000000033a746f076504620000000b3a746f6b656e73536f6c640765046a0000000d3a6d696e58747a426f75676874046b000000093a646561646c696e650000000b25746f6b656e546f58747a0764076408650765046e000000153a6f7574707574446578746572436f6e747261637407650462000000103a6d696e546f6b656e73426f75676874046e000000063a6f776e65720765046e000000033a746f076504620000000b3a746f6b656e73536f6c64046b000000093a646561646c696e650000000d25746f6b656e546f546f6b656e0764045d0000001025757064617465546f6b656e506f6f6c04620000001825757064617465546f6b656e506f6f6c496e7465726e616c076408650563035d0359000000092573657442616b65720764046e0000000b257365744d616e61676572046c000000082564656661756c74050107650861046e000000063a6f776e657207650462000000083a62616c616e63650760046e000000083a7370656e64657204620000000a3a616c6c6f77616e636500000009256163636f756e7473076507650459000000183a73656c6649735570646174696e67546f6b656e506f6f6c076504590000000c3a667265657a6542616b65720462000000093a6c7174546f74616c07650765046e000000083a6d616e61676572046e0000000d3a746f6b656e41646472657373076504620000000a3a746f6b656e506f6f6c046a000000083a78747a506f6f6c050202000028c6055707650764076407640765036e07650362036207650765036e036207650362036b076407650765036e0765036e03620765036a07650362036b07640765036e07650362036b07650765036e036e076503620765036a036b0764076407650765036e07650362036e0765036e07650362036b0764035d0362076407650563035d03590764036e036c07650761036e076503620760036e036207650765035907650359036207650765036e036e07650362036a03210316051f02000000020317072e0200001c86072e0200000b8d072e02000001c1051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327051f02000000020321034c031603480329072f020000000e0723036e03620743036200000342020000000003210317071f0002020000000203210570000203160329072f02000000060743036200000200000000071f000202000000020321057000020317031703190325072c020000000002000000630743036801000000585468652063757272656e7420616c6c6f77616e636520706172616d65746572206d75737420657175616c207468652073656e64657227732063757272656e7420616c6c6f77616e636520666f7220746865206f776e65722e0327032103170570000203210316051f02000000060317031603460350051f020000000d0321051f020000000203160317034c0320034c0342051f020000000403210316034603480350051f020000000d0321051f020000000203170316034c03200342053d036d034202000009c0051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e03270200000000032103170317034003190337072c0200000000020000002807430368010000001d4e4f572069732067726561746572207468616e20646561646c696e652e032703210317031607430362000003190337072c0200000000020000003807430368010000002d6d6178546f6b656e734465706f7369746564206d7573742062652067726561746572207468616e207a65726f2e032703210316031707430362000003190337072c020000000002000000320743036801000000276d696e4c71744d696e746564206d7573742062652067726561746572207468616e207a65726f2e032703130743036a000003190337072c0200000000020000004607430368010000003b54686520616d6f756e74206f662058545a2073656e7420746f20446578746572206d7573742062652067726561746572207468616e207a65726f2e0327051f02000000020321034c031703160317031703300325072c020000032f03130743036a0080897a03190332072c0200000000020000004f07430368010000004454686520696e697469616c206c697175696469747920616d6f756e74206d7573742062652067726561746572207468616e206f7220657175616c20746f20312058545a2e0327034c0313051f02000000060743036a00010322072f020000000b0743036801000000000327020000000203160321051f0200000071051f020000000403210317051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c03420342051f020000000d0321051f020000000203160317034c0320034c0342034c071f0002020000000203210570000203160316051f0200000004032103160329072f020000000e0723036e03620743036200000342020000000005700002051f020000000d0321051f020000000203170316034c03200342051f0200000004032103160346071f00030200000002032105700003031603160350051f020000000d0321051f020000000203170316034c032003420321031703170317031703130312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c034203210317031703170316071f00020200000002032105700002031703160312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342051f0200000011032103170316051f0200000004031603160321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a0000057000030349035405700005051f020000000203420342034d051f0200000004053d036d031b034202000004e6051f02000000020321034c0317031703170317051f02000000060743036a00010322072f020000000b0743036801000000000327020000000203160313051f02000000060743036a00010322072f020000000b0743036801000000000327020000000203160321071f000402000000020321057000040317031703170316033a071f00020200000002032105700002034c0322072f020000001507430368010000000a64697642795a65726f2e0327020000002703210316051f02000000020317034c03300325072c020000000002000000080743036200010312032107430362000003190337072c02000000000200000023074303680100000018746f6b656e734465706f7369746564206973207a65726f2e0327034c071f000402000000020321057000040317031603170317033a051f0200000002034c0322072f0200000002032702000000020316071f0002020000000203210570000203160317051f0200000002032103190332072c020000000002000000430743036801000000386c71744d696e746564206d7573742062652067726561746572207468616e206f7220657175616c20746f206d696e4c71744d696e7465642e0327051f0200000066051f02000000020321034c03170316051f0200000002032103190328072c0200000000020000003e074303680100000033746f6b656e734465706f73697465642069732067726561746572207468616e206d6178546f6b656e734465706f73697465642e0327071f00030200000002032105700003071f0003020000000203210570000303160316051f020000000203160329072f020000000e0723036e03620743036200000342020000000003210316071f000202000000020321057000020312051f020000000d0321051f020000000203170316034c032003420346071f0003020000000203210570000303160316051f020000000f051f020000000805700003032103160350051f020000000d0321051f020000000203170316034c0320034203210317031603170317057000020312051f020000000403210317051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c03420342051f020000000d0321051f020000000203160317034c0320034c03420321031703170317031703130312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c034203210317031703170316071f000202000000020321057000020312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342051f020000000b051f0200000004031603160321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a0000057000030349035405700005051f020000000203420342034d051f0200000004053d036d031b034202000010ed072e020000090b051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e03270321031703170317034003190337072c0200000000020000002807430368010000001d4e4f572069732067726561746572207468616e20646561646c696e652e03270321031703160743036a000003190337072c0200000000020000003507430368010000002a6d696e58747a57697468647261776e206d7573742062652067726561746572207468616e207a65726f2e0327032103170317031607430362000003190337072c0200000000020000003807430368010000002d6d696e546f6b656e7357697468647261776e206d7573742062652067726561746572207468616e207a65726f2e0327032103160317031707430362000003190337072c0200000000020000002f0743036801000000246c71744275726e6564206d7573742062652067726561746572207468616e207a65726f2e0327032103160316051f020000000d051f02000000020321034c03160329072f02000000220743036801000000176f776e657220686173206e6f206c69717569646974792e03270200000000034c0321031603170317071f00020200000002032105700002031603190328072c0200000000020000003507430368010000002a6c71744275726e65642069732067726561746572207468616e206f776e657227732062616c616e63652e0327032103160316034803190325072c0200000004034c03160200000132034c0321031703480329072f020000002a07430368010000001f73656e64657220686173206e6f20617070726f76616c2062616c616e63652e03270200000000051f0200000017034c0321031603170317051f02000000060743035b0000034b0321051f020000004b03190328072c0200000000020000003b07430368010000003073656e64657220617070726f76616c2062616c616e6365206973206c657373207468616e204c5154206275726e65642e03270311034605700002032103170570000203480350051f020000000d0321051f020000000203160317034c0320034c034203210316051f0200000043034605710001032103160316034c051f020000002e051f020000000b051f0200000004032103160350051f020000000d0321051f020000000203170316034c03200342051f02000000020321034c031603170317071f000302000000020321057000030317031703170317051f02000000060743036a00010322072f020000000b074303680100000000032702000000020316033a051f0200000017071f0002020000000203210570000203170316031703170322072f020000001507430368010000000a64697642795a65726f2e0327020000000203160743036a0001033a0321071f000302000000020321057000030317031603190332072c0200000000020000003507430368010000002a78747a57697468647261776e206973206c657373207468616e206d696e58747a57697468647261776e2e0327071f00020200000002032105700002031603170317051f0200000023071f0003020000000203210570000303210317031603170317034c0317031703170316033a0322072f020000001507430368010000000a64697642795a65726f2e0327020000000203160321071f0004020000000203210570000403170317031603190332072c0200000000020000003b074303680100000030746f6b656e7357697468647261776e206973206c657373207468616e206d696e546f6b656e7357697468647261776e2e0327071f0003020000000203210570000303160317031705700003034b03210743035b000003190332072c02000000020311020000000b0743036801000000000327057000040321071f0005020000000"
          "203210570000503160316051f020000000203160329072f020000000e0723036e03620743036200000342020000000005700002051f020000000d0321051f020000000203170316034c03200342051f0200000004032103160346071f00050200000002032105700005031603160350051f020000000d0321051f020000000203170316034c0320034203210317031603170317071f00040200000002032105700004031603170317034c034b03210743035b000003190332072c02000000020311020000000b0743036801000000000327051f020000000403210317051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c03420342051f020000000d0321051f020000000203160317034c0320034c034203210317031703170316071f00020200000002032105700002034c034b03210743035b000003190332072c02000000020311020000000b0743036801000000000327051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c034203210317031703170317071f00030200000002032105700003034c0393072f020000001a07430368010000000f6e65676174697665206d7574657a2103270200000000051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342071f000302000000020321057000030316031703160555036c072f020000000403170327020000000005700003034f034d051f020000005f051f020000000d051f02000000060316031703160321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a000005700003057000040342034903540342034d053d036d034c031b034c031b034202000007d6072e02000003af051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e03270200000000032103170317034003190337072c0200000000020000002807430368010000001d4e4f572069732067726561746572207468616e20646561646c696e652e032703210317031607430362000003190337072c0200000000020000003507430368010000002a6d696e546f6b656e73426f75676874206d7573742062652067726561746572207468616e207a65726f2e0327051f02000000020321034c0317031703170317051f02000000060743036a00010322072f020000000b0743036801000000000327020000000203160743036200a80f033a0313051f02000000060743036a00010322072f020000000b0743036801000000000327020000000203160321051f020000000b0743036200a50f033a03120743036200a50f033a071f000302000000020321057000030317031703170316033a0322072f020000001507430368010000000a64697642795a65726f2e0327020000000203160321051f0200000052051f020000000603210317031603190328072c0200000000020000003507430368010000002a746f6b656e73426f75676874206973206c657373207468616e206d696e546f6b656e73426f756768742e03270321071f000302000000020321057000030317031703170316034b03210743035b000003190332072c02000000020311020000000b0743036801000000000327051f020000000405700002051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c03420321031703170317031703130312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342051f020000000d051f02000000060316034903540321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a0000057000030570000505700005051f020000000203420342034d051f0200000004053d036d031b0342020000041b051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e032703210317031703160743036a000003190337072c020000000002000000320743036801000000276d696e58747a426f75676874206d7573742062652067726561746572207468616e207a65726f2e03270321031703170317034003190337072c0200000000020000002807430368010000001d4e4f572069732067726561746572207468616e20646561646c696e652e03270321031703160743036200a50f033a071f0002020000000203210570000203170317031703160743036200a80f033a0312051f02000000020321034c031703160743036200a50f033a071f000302000000020321057000030317031703170317051f02000000060743036a00010322072f020000000b074303680100000000032702000000020316033a0322072f020000001507430368010000000a64697642795a65726f2e0327020000000203160743036a0001033a0321051f020000004e051f0200000008032103170317031603190328072c0200000000020000002f07430368010000002478747a426f75676874206973206c657373207468616e206d696e58747a426f756768742e0327051f0200000092034c03210317031703170316071f00020200000002032105700002031703160312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c03420321051f02000000ae051f020000000a03210317031703170317034c0393072f020000001a07430368010000000f6e65676174697665206d7574657a2103270200000000051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342071f00020200000002032105700002031603170555036c072f02000000020327020000000005700001034f034d051f020000006a051f0200000011032103170316051f0200000004031603160321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a0000057000030349035405700005051f020000000203420342034d053d036d034c031b034c031b03420200000b75072e0200000783072e0200000433051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e03270321031703170317034003190337072c0200000000020000002807430368010000001d4e4f572069732067726561746572207468616e20646561646c696e652e0327032103160317031607430362000003190337072c0200000000020000003507430368010000002a6d696e546f6b656e73426f75676874206d7573742062652067726561746572207468616e207a65726f2e032703210317031703160743036200a50f033a071f0002020000000203210570000203170317031703160743036200a80f033a0312051f02000000020321034c0317031703160743036200a50f033a071f000302000000020321057000030317031703170317051f02000000060743036a00010322072f020000000b074303680100000000032702000000020316033a0322072f020000001507430368010000000a64697642795a65726f2e0327020000000203160743036a0001033a051f02000000020321034c031703170316071f0003020000000203210570000303170317031703160312051f020000000405700002051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c034203210317031703170317071f00020200000002032105700002034c0393072f020000001a07430368010000000f6e65676174697665206d7574657a2103270200000000051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342071f000202000000020321057000020316031606550765036e07650362036b0000000b2578747a546f546f6b656e072f020000000403170327020000000005700002071f00030200000002032105700003032103170316051f02000000190321031603170316051f0200000008032103170317031703420342034c0320034d034c051f0200000017034c0321031703170316051f02000000060316031703170321031703170316031706550765036e0765036e036200000009257472616e73666572072f02000000040317032702000000000743036a0000057000030349035405700005051f020000000203420342034d053d036d034c031b051f0200000002034c034c031b03420200000344072e02000001720743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327031e0354034803190325072c02000000000200000020074303680100000015756e73616665557064617465546f6b656e506f6f6c03270321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000321031707430359030a051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203170316034c032003420342051f020000000d0321051f020000000203160317034c0320034c03420321031703170316031706550765036e055a03620000000b2567657442616c616e6365072f02000000040317032702000000000743036a000004490000001825757064617465546f6b656e506f6f6c496e7465726e616c034903540342034d051f0200000004053d036d031b034202000001c60743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327051f02000000020321034c031703160316072c0200000000020000003207430368010000002744657874657220646964206e6f7420696e6974696174652074686973206f7065726174696f6e2e0327051f02000000020321034c0317031703160317034803190325072c0200000000020000004e0743036801000000435468652073656e646572206973206e6f742074686520746f6b656e20636f6e7472616374206173736f6369617465642077697468207468697320636f6e74726163742e0327051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c034203210317074303590303051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203170316034c032003420342051f020000000d0321051f020000000203160317034c0320034c0342053d036d034202000003e6072e02000001bd051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327051f02000000020321034c0317031703160316034803190325072c0200000000020000002e07430368010000002373656e646572206973206e6f742074686520636f6e7472616374206d616e616765722e0327051f02000000020321034c0317031603170316033f072c0200000000020000003d07430368010000003243616e6e6f74206368616e6765207468652062616b6572207768696c6520667265657a6542616b657220697320747275652e032703210316051f02000000020317034e051f0200000073051f020000000403210317051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316034c03200342034c03420342051f020000000d0321051f020000000203160317034c0320034c0342053d036d031b0342020000021d072e0200000147051f02000000410321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000743036a0000031303190325072c0200000000020000001f074303680100000014416d6f756e74206d757374206265207a65726f2e0327051f02000000020321034c0317031703160316034803190325072c0200000000020000002e07430368010000002373656e646572206973206e6f742074686520636f6e7472616374206d616e616765722e0327051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203170316051f020000000d0321051f020000000203170316034c032003420342034c0342051f020000000d0321051f020000000203160317034c0320034c0342053d036d034202000000ca03200321031703160316072c020000002d07430368010000002273656c6649735570646174696e67546f6b656e206d7573742062652066616c73652e032702000000000321031703170317031703130312051f020000000403210317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317051f020000000d0321051f020000000203160317034c0320034c0342034c0342034c0342051f020000000d0321051f020000000203160317034c0320034c0342053d036d0342");
    t.addresses := [ "KT1CT7S2b9hXNRxRrEcany9sak1qe4aaFAZJ" ]; |}.

Definition patches : list t :=
  [
    exprtgpMFzTtyg1STJqANLQsjsMXmkf8UuJTuczQh8GPtqfw18x6Lc;
    exprucjN3PgUnqQHFXQmemT44DjkacU35NrSSKyz18JSSjJB9vtUEw;
    expruqNpURkmjQk5RGHjLrnS1U3DZnEsQCvQQNLSpN1powRmJeQgoJ;
    expruwujdJkc5y4iPzr83Sd3KrJhzxSUb67JdCZmXNKiTTNvEkMrRU;
    expruZKjVy3JbWcJmjtnvMGvRamkDhMgM3urGGdne3pkN9VKgK7VnD;
    exprv98vtze1uwbDXdpb27R8RQabWZMZDXGNAwaAZwCg6WSvXu8fw3;
    expru1ukk6ZqdA32rFYFG7j1eGjfsatbdUZWz8Mi1kXWZYRZm4FZVe;
    exprubv5oQmAUP8BwktmDgMWqTizYDJVhzHhJESGZhJ2GkHESZ1VWg
  ].

Definition addresses_to_patch
  : list
    (string × Script_expr_hash.t ×
      Micheline.canonical Michelson_v1_primitives.prim) :=
  List.concat_map
    (fun (function_parameter : t) ⇒
      let '{|
        t.legacy_script_hash := legacy_script_hash;
          t.patched_code := patched_code;
          t.addresses := addresses
          |} := function_parameter in
      List.map (fun (addr : string) ⇒ (addr, legacy_script_hash, patched_code))
        addresses) patches.