Better Call Dev

​x
 
parameter (or (bytes %default) (unit %other));
storage nat;
code { CAR ;
       IF_LEFT
         { PUSH nat 0 ;
           PUSH nat 0 ;
           DIG 2 ;
           PAIR ;
           PAIR ;
           { LEFT nat ;
             LOOP_LEFT { UNPAIR ;
                         UNPAIR ;
                         PUSH nat 0 ;
                         SWAP ;
                         DUP ;
                         DUG 2 ;
                         SIZE ;
                         COMPARE ;
                         EQ ;
                         IF
                           { DROP 3 ; PUSH string "BYTES_LENGTH_ZERO" ; FAILWITH }
                           { DUP ;
                             SIZE ;
                             DUP 3 ;
                             COMPARE ;
                             LT ;
                             IF
                               { DUP ;
                                 PUSH nat 1 ;
                                 DUP 4 ;
                                 SLICE ;
                                 IF_NONE { PUSH string "SLICE" ; FAILWITH } {} ;
                                 EMPTY_MAP bytes nat ;
                                 PUSH nat 255 ;
                                 SOME ;
                                 PUSH bytes 0xff ;
                                 UPDATE ;
                                 PUSH nat 254 ;
                                 SOME ;
                                 PUSH bytes 0xfe ;
                                 UPDATE ;
                                 PUSH nat 253 ;
                                 SOME ;
                                 PUSH bytes 0xfd ;
                                 UPDATE ;
                                 PUSH nat 252 ;
                                 SOME ;
                                 PUSH bytes 0xfc ;
                                 UPDATE ;
                                 PUSH nat 251 ;
                                 SOME ;
                                 PUSH bytes 0xfb ;
                                 UPDATE ;
                                 PUSH nat 250 ;
                                 SOME ;
                                 PUSH bytes 0xfa ;
                                 UPDATE ;
                                 PUSH nat 249 ;
                                 SOME ;
                                 PUSH bytes 0xf9 ;
                                 UPDATE ;
                                 PUSH nat 248 ;
                                 SOME ;
                                 PUSH bytes 0xf8 ;
                                 UPDATE ;
                                 PUSH nat 247 ;
                                 SOME ;
                                 PUSH bytes 0xf7 ;
                                 UPDATE ;
                                 PUSH nat 246 ;
                                 SOME ;
                                 PUSH bytes 0xf6 ;
                                 UPDATE ;
                                 PUSH nat 245 ;
                                 SOME ;
                                 PUSH bytes 0xf5 ;
                                 UPDATE ;
                                 PUSH nat 244 ;
                                 SOME ;
                                 PUSH bytes 0xf4 ;
                                 UPDATE ;
                                 PUSH nat 243 ;
                                 SOME ;
                                 PUSH bytes 0xf3 ;
                                 UPDATE ;
                                 PUSH nat 242 ;
                                 SOME ;
                                 PUSH bytes 0xf2 ;
                                 UPDATE ;
                                 PUSH nat 241 ;
                                 SOME ;
                                 PUSH bytes 0xf1 ;
                                 UPDATE ;
                                 PUSH nat 240 ;
                                 SOME ;
                                 PUSH bytes 0xf0 ;
                                 UPDATE ;
                                 PUSH nat 239 ;
                                 SOME ;
                                 PUSH bytes 0xef ;
                                 UPDATE ;
                                 PUSH nat 238 ;
                                 SOME ;
                                 PUSH bytes 0xee ;
                                 UPDATE ;
                                 PUSH nat 237 ;
                                 SOME ;
                                 PUSH bytes 0xed ;
                                 UPDATE ;
                                 PUSH nat 236 ;
                                 SOME ;
                                 PUSH bytes 0xec ;
                                 UPDATE ;
                                 PUSH nat 235 ;
                                 SOME ;
                                 PUSH bytes 0xeb ;
                                 UPDATE ;
                                 PUSH nat 234 ;
                                 SOME ;
                                 PUSH bytes 0xea ;
                                 UPDATE ;
                                 PUSH nat 233 ;
                                 SOME ;
                                 PUSH bytes 0xe9 ;
                                 UPDATE ;
                                 PUSH nat 232 ;
                                 SOME ;
                                 PUSH bytes 0xe8 ;
                                 UPDATE ;
                                 PUSH nat 231 ;
                                 SOME ;
                                 PUSH bytes 0xe7 ;
                                 UPDATE ;
                                 PUSH nat 230 ;
                                 SOME ;
                                 PUSH bytes 0xe6 ;
                                 UPDATE ;
                                 PUSH nat 229 ;
                                 SOME ;
                                 PUSH bytes 0xe5 ;
                                 UPDATE ;
                                 PUSH nat 228 ;
                                 SOME ;
                                 PUSH bytes 0xe4 ;
                                 UPDATE ;
                                 PUSH nat 227 ;
                                 SOME ;
                                 PUSH bytes 0xe3 ;
                                 UPDATE ;
                                 PUSH nat 226 ;
                                 SOME ;
                                 PUSH bytes 0xe2 ;
                                 UPDATE ;
                                 PUSH nat 225 ;
                                 SOME ;
                                 PUSH bytes 0xe1 ;
                                 UPDATE ;
                                 PUSH nat 224 ;
                                 SOME ;
                                 PUSH bytes 0xe0 ;
                                 UPDATE ;
                                 PUSH nat 223 ;
                                 SOME ;
                                 PUSH bytes 0xdf ;
                                 UPDATE ;
                                 PUSH nat 222 ;
                                 SOME ;
                                 PUSH bytes 0xde ;
                                 UPDATE ;
                                 PUSH nat 221 ;
                                 SOME ;
                                 PUSH bytes 0xdd ;
                                 UPDATE ;
                                 PUSH nat 220 ;
                                 SOME ;
                                 PUSH bytes 0xdc ;
                                 UPDATE ;
                                 PUSH nat 219 ;
                                 SOME ;
                                 PUSH bytes 0xdb ;
                                 UPDATE ;
                                 PUSH nat 218 ;
                                 SOME ;
                                 PUSH bytes 0xda ;
                                 UPDATE ;
                                 PUSH nat 217 ;
                                 SOME ;
                                 PUSH bytes 0xd9 ;
                                 UPDATE ;
                                 PUSH nat 216 ;
                                 SOME ;
                                 PUSH bytes 0xd8 ;
                                 UPDATE ;
                                 PUSH nat 215 ;
                                 SOME ;
                                 PUSH bytes 0xd7 ;
                                 UPDATE ;
                                 PUSH nat 214 ;
                                 SOME ;
                                 PUSH bytes 0xd6 ;
                                 UPDATE ;
                                 PUSH nat 213 ;
                                 SOME ;
                                 PUSH bytes 0xd5 ;
                                 UPDATE ;
                                 PUSH nat 212 ;
                                 SOME ;
                                 PUSH bytes 0xd4 ;
                                 UPDATE ;
                                 PUSH nat 211 ;
                                 SOME ;
                                 PUSH bytes 0xd3 ;
                                 UPDATE ;
                                 PUSH nat 210 ;
                                 SOME ;
                                 PUSH bytes 0xd2 ;
                                 UPDATE ;
                                 PUSH nat 209 ;
                                 SOME ;
                                 PUSH bytes 0xd1 ;
                                 UPDATE ;
                                 PUSH nat 208 ;
                                 SOME ;
                                 PUSH bytes 0xd0 ;
                                 UPDATE ;
                                 PUSH nat 207 ;
                                 SOME ;
                                 PUSH bytes 0xcf ;
                                 UPDATE ;
                                 PUSH nat 206 ;
                                 SOME ;
                                 PUSH bytes 0xce ;
                                 UPDATE ;
                                 PUSH nat 205 ;
                                 SOME ;
                                 PUSH bytes 0xcd ;
                                 UPDATE ;
                                 PUSH nat 204 ;
                                 SOME ;
                                 PUSH bytes 0xcc ;
                                 UPDATE ;
                                 PUSH nat 203 ;
                                 SOME ;
                                 PUSH bytes 0xcb ;
                                 UPDATE ;
                                 PUSH nat 202 ;
                                 SOME ;
                                 PUSH bytes 0xca ;
                                 UPDATE ;
                                 PUSH nat 201 ;
                                 SOME ;
                                 PUSH bytes 0xc9 ;
                                 UPDATE ;
                                 PUSH nat 200 ;
                                 SOME ;
                                 PUSH bytes 0xc8 ;
                                 UPDATE ;
                                 PUSH nat 199 ;
                                 SOME ;
                                 PUSH bytes 0xc7 ;
                                 UPDATE ;
                                 PUSH nat 198 ;
                                 SOME ;
                                 PUSH bytes 0xc6 ;
                                 UPDATE ;
                                 PUSH nat 197 ;
                                 SOME ;
                                 PUSH bytes 0xc5 ;
                                 UPDATE ;
                                 PUSH nat 196 ;
                                 SOME ;
                                 PUSH bytes 0xc4 ;
                                 UPDATE ;
                                 PUSH nat 195 ;
                                 SOME ;
                                 PUSH bytes 0xc3 ;
                                 UPDATE ;
                                 PUSH nat 194 ;
                                 SOME ;
                                 PUSH bytes 0xc2 ;
                                 UPDATE ;
                                 PUSH nat 193 ;
                                 SOME ;
                                 PUSH bytes 0xc1 ;
                                 UPDATE ;
                                 PUSH nat 192 ;
                                 SOME ;
                                 PUSH bytes 0xc0 ;
                                 UPDATE ;
                                 PUSH nat 191 ;
                                 SOME ;
                                 PUSH bytes 0xbf ;
                                 UPDATE ;
                                 PUSH nat 190 ;
                                 SOME ;
                                 PUSH bytes 0xbe ;
                                 UPDATE ;
                                 PUSH nat 189 ;
                                 SOME ;
                                 PUSH bytes 0xbd ;
                                 UPDATE ;
                                 PUSH nat 188 ;
                                 SOME ;
                                 PUSH bytes 0xbc ;
                                 UPDATE ;
                                 PUSH nat 187 ;
                                 SOME ;
                                 PUSH bytes 0xbb ;
                                 UPDATE ;
                                 PUSH nat 186 ;
                                 SOME ;
                                 PUSH bytes 0xba ;
                                 UPDATE ;
                                 PUSH nat 185 ;
                                 SOME ;
                                 PUSH bytes 0xb9 ;
                                 UPDATE ;
                                 PUSH nat 184 ;
                                 SOME ;
                                 PUSH bytes 0xb8 ;
                                 UPDATE ;
                                 PUSH nat 183 ;
                                 SOME ;
                                 PUSH bytes 0xb7 ;
                                 UPDATE ;
                                 PUSH nat 182 ;
                                 SOME ;
                                 PUSH bytes 0xb6 ;
                                 UPDATE ;
                                 PUSH nat 181 ;
                                 SOME ;
                                 PUSH bytes 0xb5 ;
                                 UPDATE ;
                                 PUSH nat 180 ;
                                 SOME ;
                                 PUSH bytes 0xb4 ;
                                 UPDATE ;
                                 PUSH nat 179 ;
                                 SOME ;
                                 PUSH bytes 0xb3 ;
                                 UPDATE ;
                                 PUSH nat 178 ;
                                 SOME ;
                                 PUSH bytes 0xb2 ;
                                 UPDATE ;
                                 PUSH nat 177 ;
                                 SOME ;
                                 PUSH bytes 0xb1 ;
                                 UPDATE ;
                                 PUSH nat 176 ;
                                 SOME ;
                                 PUSH bytes 0xb0 ;
                                 UPDATE ;
                                 PUSH nat 175 ;
                                 SOME ;
                                 PUSH bytes 0xaf ;
                                 UPDATE ;
                                 PUSH nat 174 ;
                                 SOME ;
                                 PUSH bytes 0xae ;
                                 UPDATE ;
                                 PUSH nat 173 ;
                                 SOME ;
                                 PUSH bytes 0xad ;
                                 UPDATE ;
                                 PUSH nat 172 ;
                                 SOME ;
                                 PUSH bytes 0xac ;
                                 UPDATE ;
                                 PUSH nat 171 ;
                                 SOME ;
                                 PUSH bytes 0xab ;
                                 UPDATE ;
                                 PUSH nat 170 ;
                                 SOME ;
                                 PUSH bytes 0xaa ;
                                 UPDATE ;
                                 PUSH nat 169 ;
                                 SOME ;
                                 PUSH bytes 0xa9 ;
                                 UPDATE ;
                                 PUSH nat 168 ;
                                 SOME ;
                                 PUSH bytes 0xa8 ;
                                 UPDATE ;
                                 PUSH nat 167 ;
                                 SOME ;
                                 PUSH bytes 0xa7 ;
                                 UPDATE ;
                                 PUSH nat 166 ;
                                 SOME ;
                                 PUSH bytes 0xa6 ;
                                 UPDATE ;
                                 PUSH nat 165 ;
                                 SOME ;
                                 PUSH bytes 0xa5 ;
                                 UPDATE ;
                                 PUSH nat 164 ;
                                 SOME ;
                                 PUSH bytes 0xa4 ;
                                 UPDATE ;
                                 PUSH nat 163 ;
                                 SOME ;
                                 PUSH bytes 0xa3 ;
                                 UPDATE ;
                                 PUSH nat 162 ;
                                 SOME ;
                                 PUSH bytes 0xa2 ;
                                 UPDATE ;
                                 PUSH nat 161 ;
                                 SOME ;
                                 PUSH bytes 0xa1 ;
                                 UPDATE ;
                                 PUSH nat 160 ;
                                 SOME ;
                                 PUSH bytes 0xa0 ;
                                 UPDATE ;
                                 PUSH nat 159 ;
                                 SOME ;
                                 PUSH bytes 0x9f ;
                                 UPDATE ;
                                 PUSH nat 158 ;
                                 SOME ;
                                 PUSH bytes 0x9e ;
                                 UPDATE ;
                                 PUSH nat 157 ;
                                 SOME ;
                                 PUSH bytes 0x9d ;
                                 UPDATE ;
                                 PUSH nat 156 ;
                                 SOME ;
                                 PUSH bytes 0x9c ;
                                 UPDATE ;
                                 PUSH nat 155 ;
                                 SOME ;
                                 PUSH bytes 0x9b ;
                                 UPDATE ;
                                 PUSH nat 154 ;
                                 SOME ;
                                 PUSH bytes 0x9a ;
                                 UPDATE ;
                                 PUSH nat 153 ;
                                 SOME ;
                                 PUSH bytes 0x99 ;
                                 UPDATE ;
                                 PUSH nat 152 ;
                                 SOME ;
                                 PUSH bytes 0x98 ;
                                 UPDATE ;
                                 PUSH nat 151 ;
                                 SOME ;
                                 PUSH bytes 0x97 ;
                                 UPDATE ;
                                 PUSH nat 150 ;
                                 SOME ;
                                 PUSH bytes 0x96 ;
                                 UPDATE ;
                                 PUSH nat 149 ;
                                 SOME ;
                                 PUSH bytes 0x95 ;
                                 UPDATE ;
                                 PUSH nat 148 ;
                                 SOME ;
                                 PUSH bytes 0x94 ;
                                 UPDATE ;
                                 PUSH nat 147 ;
                                 SOME ;
                                 PUSH bytes 0x93 ;
                                 UPDATE ;
                                 PUSH nat 146 ;
                                 SOME ;
                                 PUSH bytes 0x92 ;
                                 UPDATE ;
                                 PUSH nat 145 ;
                                 SOME ;
                                 PUSH bytes 0x91 ;
                                 UPDATE ;
                                 PUSH nat 144 ;
                                 SOME ;
                                 PUSH bytes 0x90 ;
                                 UPDATE ;
                                 PUSH nat 143 ;
                                 SOME ;
                                 PUSH bytes 0x8f ;
                                 UPDATE ;
                                 PUSH nat 142 ;
                                 SOME ;
                                 PUSH bytes 0x8e ;
                                 UPDATE ;
                                 PUSH nat 141 ;
                                 SOME ;
                                 PUSH bytes 0x8d ;
                                 UPDATE ;
                                 PUSH nat 140 ;
                                 SOME ;
                                 PUSH bytes 0x8c ;
                                 UPDATE ;
                                 PUSH nat 139 ;
                                 SOME ;
                                 PUSH bytes 0x8b ;
                                 UPDATE ;
                                 PUSH nat 138 ;
                                 SOME ;
                                 PUSH bytes 0x8a ;
                                 UPDATE ;
                                 PUSH nat 137 ;
                                 SOME ;
                                 PUSH bytes 0x89 ;
                                 UPDATE ;
                                 PUSH nat 136 ;
                                 SOME ;
                                 PUSH bytes 0x88 ;
                                 UPDATE ;
                                 PUSH nat 135 ;
                                 SOME ;
                                 PUSH bytes 0x87 ;
                                 UPDATE ;
                                 PUSH nat 134 ;
                                 SOME ;
                                 PUSH bytes 0x86 ;
                                 UPDATE ;
                                 PUSH nat 133 ;
                                 SOME ;
                                 PUSH bytes 0x85 ;
                                 UPDATE ;
                                 PUSH nat 132 ;
                                 SOME ;
                                 PUSH bytes 0x84 ;
                                 UPDATE ;
                                 PUSH nat 131 ;
                                 SOME ;
                                 PUSH bytes 0x83 ;
                                 UPDATE ;
                                 PUSH nat 130 ;
                                 SOME ;
                                 PUSH bytes 0x82 ;
                                 UPDATE ;
                                 PUSH nat 129 ;
                                 SOME ;
                                 PUSH bytes 0x81 ;
                                 UPDATE ;
                                 PUSH nat 128 ;
                                 SOME ;
                                 PUSH bytes 0x80 ;
                                 UPDATE ;
                                 PUSH nat 127 ;
                                 SOME ;
                                 PUSH bytes 0x7f ;
                                 UPDATE ;
                                 PUSH nat 126 ;
                                 SOME ;
                                 PUSH bytes 0x7e ;
                                 UPDATE ;
                                 PUSH nat 125 ;
                                 SOME ;
                                 PUSH bytes 0x7d ;
                                 UPDATE ;
                                 PUSH nat 124 ;
                                 SOME ;
                                 PUSH bytes 0x7c ;
                                 UPDATE ;
                                 PUSH nat 123 ;
                                 SOME ;
                                 PUSH bytes 0x7b ;
                                 UPDATE ;
                                 PUSH nat 122 ;
                                 SOME ;
                                 PUSH bytes 0x7a ;
                                 UPDATE ;
                                 PUSH nat 121 ;
                                 SOME ;
                                 PUSH bytes 0x79 ;
                                 UPDATE ;
                                 PUSH nat 120 ;
                                 SOME ;
                                 PUSH bytes 0x78 ;
                                 UPDATE ;
                                 PUSH nat 119 ;
                                 SOME ;
                                 PUSH bytes 0x77 ;
                                 UPDATE ;
                                 PUSH nat 118 ;
                                 SOME ;
                                 PUSH bytes 0x76 ;
                                 UPDATE ;
                                 PUSH nat 117 ;
                                 SOME ;
                                 PUSH bytes 0x75 ;
                                 UPDATE ;
                                 PUSH nat 116 ;
                                 SOME ;
                                 PUSH bytes 0x74 ;
                                 UPDATE ;
                                 PUSH nat 115 ;
                                 SOME ;
                                 PUSH bytes 0x73 ;
                                 UPDATE ;
                                 PUSH nat 114 ;
                                 SOME ;
                                 PUSH bytes 0x72 ;
                                 UPDATE ;
                                 PUSH nat 113 ;
                                 SOME ;
                                 PUSH bytes 0x71 ;
                                 UPDATE ;
                                 PUSH nat 112 ;
                                 SOME ;
                                 PUSH bytes 0x70 ;
                                 UPDATE ;
                                 PUSH nat 111 ;
                                 SOME ;
                                 PUSH bytes 0x6f ;
                                 UPDATE ;
                                 PUSH nat 110 ;
                                 SOME ;
                                 PUSH bytes 0x6e ;
                                 UPDATE ;
                                 PUSH nat 109 ;
                                 SOME ;
                                 PUSH bytes 0x6d ;
                                 UPDATE ;
                                 PUSH nat 108 ;
                                 SOME ;
                                 PUSH bytes 0x6c ;
                                 UPDATE ;
                                 PUSH nat 107 ;
                                 SOME ;
                                 PUSH bytes 0x6b ;
                                 UPDATE ;
                                 PUSH nat 106 ;
                                 SOME ;
                                 PUSH bytes 0x6a ;
                                 UPDATE ;
                                 PUSH nat 105 ;
                                 SOME ;
                                 PUSH bytes 0x69 ;
                                 UPDATE ;
                                 PUSH nat 104 ;
                                 SOME ;
                                 PUSH bytes 0x68 ;
                                 UPDATE ;
                                 PUSH nat 103 ;
                                 SOME ;
                                 PUSH bytes 0x67 ;
                                 UPDATE ;
                                 PUSH nat 102 ;
                                 SOME ;
                                 PUSH bytes 0x66 ;
                                 UPDATE ;
                                 PUSH nat 101 ;
                                 SOME ;
                                 PUSH bytes 0x65 ;
                                 UPDATE ;
                                 PUSH nat 100 ;
                                 SOME ;
                                 PUSH bytes 0x64 ;
                                 UPDATE ;
                                 PUSH nat 99 ;
                                 SOME ;
                                 PUSH bytes 0x63 ;
                                 UPDATE ;
                                 PUSH nat 98 ;
                                 SOME ;
                                 PUSH bytes 0x62 ;
                                 UPDATE ;
                                 PUSH nat 97 ;
                                 SOME ;
                                 PUSH bytes 0x61 ;
                                 UPDATE ;
                                 PUSH nat 96 ;
                                 SOME ;
                                 PUSH bytes 0x60 ;
                                 UPDATE ;
                                 PUSH nat 95 ;
                                 SOME ;
                                 PUSH bytes 0x5f ;
                                 UPDATE ;
                                 PUSH nat 94 ;
                                 SOME ;
                                 PUSH bytes 0x5e ;
                                 UPDATE ;
                                 PUSH nat 93 ;
                                 SOME ;
                                 PUSH bytes 0x5d ;
                                 UPDATE ;
                                 PUSH nat 92 ;
                                 SOME ;
                                 PUSH bytes 0x5c ;
                                 UPDATE ;
                                 PUSH nat 91 ;
                                 SOME ;
                                 PUSH bytes 0x5b ;
                                 UPDATE ;
                                 PUSH nat 90 ;
                                 SOME ;
                                 PUSH bytes 0x5a ;
                                 UPDATE ;
                                 PUSH nat 89 ;
                                 SOME ;
                                 PUSH bytes 0x59 ;
                                 UPDATE ;
                                 PUSH nat 88 ;
                                 SOME ;
                                 PUSH bytes 0x58 ;
                                 UPDATE ;
                                 PUSH nat 87 ;
                                 SOME ;
                                 PUSH bytes 0x57 ;
                                 UPDATE ;
                                 PUSH nat 86 ;
                                 SOME ;
                                 PUSH bytes 0x56 ;
                                 UPDATE ;
                                 PUSH nat 85 ;
                                 SOME ;
                                 PUSH bytes 0x55 ;
                                 UPDATE ;
                                 PUSH nat 84 ;
                                 SOME ;
                                 PUSH bytes 0x54 ;
                                 UPDATE ;
                                 PUSH nat 83 ;
                                 SOME ;
                                 PUSH bytes 0x53 ;
                                 UPDATE ;
                                 PUSH nat 82 ;
                                 SOME ;
                                 PUSH bytes 0x52 ;
                                 UPDATE ;
                                 PUSH nat 81 ;
                                 SOME ;
                                 PUSH bytes 0x51 ;
                                 UPDATE ;
                                 PUSH nat 80 ;
                                 SOME ;
                                 PUSH bytes 0x50 ;
                                 UPDATE ;
                                 PUSH nat 79 ;
                                 SOME ;
                                 PUSH bytes 0x4f ;
                                 UPDATE ;
                                 PUSH nat 78 ;
                                 SOME ;
                                 PUSH bytes 0x4e ;
                                 UPDATE ;
                                 PUSH nat 77 ;
                                 SOME ;
                                 PUSH bytes 0x4d ;
                                 UPDATE ;
                                 PUSH nat 76 ;
                                 SOME ;
                                 PUSH bytes 0x4c ;
                                 UPDATE ;
                                 PUSH nat 75 ;
                                 SOME ;
                                 PUSH bytes 0x4b ;
                                 UPDATE ;
                                 PUSH nat 74 ;
                                 SOME ;
                                 PUSH bytes 0x4a ;
                                 UPDATE ;
                                 PUSH nat 73 ;
                                 SOME ;
                                 PUSH bytes 0x49 ;
                                 UPDATE ;
                                 PUSH nat 72 ;
                                 SOME ;
                                 PUSH bytes 0x48 ;
                                 UPDATE ;
                                 PUSH nat 71 ;
                                 SOME ;
                                 PUSH bytes 0x47 ;
                                 UPDATE ;
                                 PUSH nat 70 ;
                                 SOME ;
                                 PUSH bytes 0x46 ;
                                 UPDATE ;
                                 PUSH nat 69 ;
                                 SOME ;
                                 PUSH bytes 0x45 ;
                                 UPDATE ;
                                 PUSH nat 68 ;
                                 SOME ;
                                 PUSH bytes 0x44 ;
                                 UPDATE ;
                                 PUSH nat 67 ;
                                 SOME ;
                                 PUSH bytes 0x43 ;
                                 UPDATE ;
                                 PUSH nat 66 ;
                                 SOME ;
                                 PUSH bytes 0x42 ;
                                 UPDATE ;
                                 PUSH nat 65 ;
                                 SOME ;
                                 PUSH bytes 0x41 ;
                                 UPDATE ;
                                 PUSH nat 64 ;
                                 SOME ;
                                 PUSH bytes 0x40 ;
                                 UPDATE ;
                                 PUSH nat 63 ;
                                 SOME ;
                                 PUSH bytes 0x3f ;
                                 UPDATE ;
                                 PUSH nat 62 ;
                                 SOME ;
                                 PUSH bytes 0x3e ;
                                 UPDATE ;
                                 PUSH nat 61 ;
                                 SOME ;
                                 PUSH bytes 0x3d ;
                                 UPDATE ;
                                 PUSH nat 60 ;
                                 SOME ;
                                 PUSH bytes 0x3c ;
                                 UPDATE ;
                                 PUSH nat 59 ;
                                 SOME ;
                                 PUSH bytes 0x3b ;
                                 UPDATE ;
                                 PUSH nat 58 ;
                                 SOME ;
                                 PUSH bytes 0x3a ;
                                 UPDATE ;
                                 PUSH nat 57 ;
                                 SOME ;
                                 PUSH bytes 0x39 ;
                                 UPDATE ;
                                 PUSH nat 56 ;
                                 SOME ;
                                 PUSH bytes 0x38 ;
                                 UPDATE ;
                                 PUSH nat 55 ;
                                 SOME ;
                                 PUSH bytes 0x37 ;
                                 UPDATE ;
                                 PUSH nat 54 ;
                                 SOME ;
                                 PUSH bytes 0x36 ;
                                 UPDATE ;
                                 PUSH nat 53 ;
                                 SOME ;
                                 PUSH bytes 0x35 ;
                                 UPDATE ;
                                 PUSH nat 52 ;
                                 SOME ;
                                 PUSH bytes 0x34 ;
                                 UPDATE ;
                                 PUSH nat 51 ;
                                 SOME ;
                                 PUSH bytes 0x33 ;
                                 UPDATE ;
                                 PUSH nat 50 ;
                                 SOME ;
                                 PUSH bytes 0x32 ;
                                 UPDATE ;
                                 PUSH nat 49 ;
                                 SOME ;
                                 PUSH bytes 0x31 ;
                                 UPDATE ;
                                 PUSH nat 48 ;
                                 SOME ;
                                 PUSH bytes 0x30 ;
                                 UPDATE ;
                                 PUSH nat 47 ;
                                 SOME ;
                                 PUSH bytes 0x2f ;
                                 UPDATE ;
                                 PUSH nat 46 ;
                                 SOME ;
                                 PUSH bytes 0x2e ;
                                 UPDATE ;
                                 PUSH nat 45 ;
                                 SOME ;
                                 PUSH bytes 0x2d ;
                                 UPDATE ;
                                 PUSH nat 44 ;
                                 SOME ;
                                 PUSH bytes 0x2c ;
                                 UPDATE ;
                                 PUSH nat 43 ;
                                 SOME ;
                                 PUSH bytes 0x2b ;
                                 UPDATE ;
                                 PUSH nat 42 ;
                                 SOME ;
                                 PUSH bytes 0x2a ;
                                 UPDATE ;
                                 PUSH nat 41 ;
                                 SOME ;
                                 PUSH bytes 0x29 ;
                                 UPDATE ;
                                 PUSH nat 40 ;
                                 SOME ;
                                 PUSH bytes 0x28 ;
                                 UPDATE ;
                                 PUSH nat 39 ;
                                 SOME ;
                                 PUSH bytes 0x27 ;
                                 UPDATE ;
                                 PUSH nat 38 ;
                                 SOME ;
                                 PUSH bytes 0x26 ;
                                 UPDATE ;
                                 PUSH nat 37 ;
                                 SOME ;
                                 PUSH bytes 0x25 ;
                                 UPDATE ;
                                 PUSH nat 36 ;
                                 SOME ;
                                 PUSH bytes 0x24 ;
                                 UPDATE ;
                                 PUSH nat 35 ;
                                 SOME ;
                                 PUSH bytes 0x23 ;
                                 UPDATE ;
                                 PUSH nat 34 ;
                                 SOME ;
                                 PUSH bytes 0x22 ;
                                 UPDATE ;
                                 PUSH nat 33 ;
                                 SOME ;
                                 PUSH bytes 0x21 ;
                                 UPDATE ;
                                 PUSH nat 32 ;
                                 SOME ;
                                 PUSH bytes 0x20 ;
                                 UPDATE ;
                                 PUSH nat 31 ;
                                 SOME ;
                                 PUSH bytes 0x1f ;
                                 UPDATE ;
                                 PUSH nat 30 ;
                                 SOME ;
                                 PUSH bytes 0x1e ;
                                 UPDATE ;
                                 PUSH nat 29 ;
                                 SOME ;
                                 PUSH bytes 0x1d ;
                                 UPDATE ;
                                 PUSH nat 28 ;
                                 SOME ;
                                 PUSH bytes 0x1c ;
                                 UPDATE ;
                                 PUSH nat 27 ;
                                 SOME ;
                                 PUSH bytes 0x1b ;
                                 UPDATE ;
                                 PUSH nat 26 ;
                                 SOME ;
                                 PUSH bytes 0x1a ;
                                 UPDATE ;
                                 PUSH nat 25 ;
                                 SOME ;
                                 PUSH bytes 0x19 ;
                                 UPDATE ;
                                 PUSH nat 24 ;
                                 SOME ;
                                 PUSH bytes 0x18 ;
                                 UPDATE ;
                                 PUSH nat 23 ;
                                 SOME ;
                                 PUSH bytes 0x17 ;
                                 UPDATE ;
                                 PUSH nat 22 ;
                                 SOME ;
                                 PUSH bytes 0x16 ;
                                 UPDATE ;
                                 PUSH nat 21 ;
                                 SOME ;
                                 PUSH bytes 0x15 ;
                                 UPDATE ;
                                 PUSH nat 20 ;
                                 SOME ;
                                 PUSH bytes 0x14 ;
                                 UPDATE ;
                                 PUSH nat 19 ;
                                 SOME ;
                                 PUSH bytes 0x13 ;
                                 UPDATE ;
                                 PUSH nat 18 ;
                                 SOME ;
                                 PUSH bytes 0x12 ;
                                 UPDATE ;
                                 PUSH nat 17 ;
                                 SOME ;
                                 PUSH bytes 0x11 ;
                                 UPDATE ;
                                 PUSH nat 16 ;
                                 SOME ;
                                 PUSH bytes 0x10 ;
                                 UPDATE ;
                                 PUSH nat 15 ;
                                 SOME ;
                                 PUSH bytes 0x0f ;
                                 UPDATE ;
                                 PUSH nat 14 ;
                                 SOME ;
                                 PUSH bytes 0x0e ;
                                 UPDATE ;
                                 PUSH nat 13 ;
                                 SOME ;
                                 PUSH bytes 0x0d ;
                                 UPDATE ;
                                 PUSH nat 12 ;
                                 SOME ;
                                 PUSH bytes 0x0c ;
                                 UPDATE ;
                                 PUSH nat 11 ;
                                 SOME ;
                                 PUSH bytes 0x0b ;
                                 UPDATE ;
                                 PUSH nat 10 ;
                                 SOME ;
                                 PUSH bytes 0x0a ;
                                 UPDATE ;
                                 PUSH nat 9 ;
                                 SOME ;
                                 PUSH bytes 0x09 ;
                                 UPDATE ;
                                 PUSH nat 8 ;
                                 SOME ;
                                 PUSH bytes 0x08 ;
                                 UPDATE ;
                                 PUSH nat 7 ;
                                 SOME ;
                                 PUSH bytes 0x07 ;
                                 UPDATE ;
                                 PUSH nat 6 ;
                                 SOME ;
                                 PUSH bytes 0x06 ;
                                 UPDATE ;
                                 PUSH nat 5 ;
                                 SOME ;
                                 PUSH bytes 0x05 ;
                                 UPDATE ;
                                 PUSH nat 4 ;
                                 SOME ;
                                 PUSH bytes 0x04 ;
                                 UPDATE ;
                                 PUSH nat 3 ;
                                 SOME ;
                                 PUSH bytes 0x03 ;
                                 UPDATE ;
                                 PUSH nat 2 ;
                                 SOME ;
                                 PUSH bytes 0x02 ;
                                 UPDATE ;
                                 PUSH nat 1 ;
                                 SOME ;
                                 PUSH bytes 0x01 ;
                                 UPDATE ;
                                 PUSH nat 0 ;
                                 SOME ;
                                 PUSH bytes 0x00 ;
                                 UPDATE ;
                                 SWAP ;
                                 GET ;
                                 IF_NONE
                                   { DROP 3 ;
                                     PUSH string "UNDEFINED_BYTES_IN_MAP" ;
                                     FAILWITH }
                                   { PUSH nat 256 ;
                                     DIG 4 ;
                                     MUL ;
                                     ADD ;
                                     PUSH nat 1 ;
                                     DIG 3 ;
                                     ADD ;
                                     DIG 2 ;
                                     PAIR ;
                                     PAIR ;
                                     LEFT nat } }
                               { DROP 2 ; RIGHT (pair (pair bytes nat) nat) } } } } }
         { DROP ; PUSH nat 0 } ;
       NIL operation ;
       PAIR }