deposit-spec.ini

; contract: https://github.com/axic/eth2-deposit-contract/blob/r1/deposit_contract.sol
; bytecode: https://github.com/axic/eth2-deposit-contract/blob/r1/deposit_contract.json
; gas analysis: https://docs.google.com/spreadsheets/d/16nH68f1yENUMQa3a5k4FfdvOvW3Eu37TKTFlmyS4s4o

[root]
; default
k: #execute => #halt
pc: 0 => ?_
word_stack: .WordStack => ?_
local_mem: .IMap => ?_
gas: #symGas({SCHEDULE}, G, {G0}, 0 => ?GAS_COST, 0, {MEMORY_USED})
memory_used: #symMem(0 => ?MEM_COST)
; no changes
call_data: _
log: _
refund: _
storage: _
orig_storage: _
balance: INIT_BALANCE
nonce: INIT_NONCE
code: {RUNTIME_CODE}
; ignore (potential) changes
output: _ => ?_
status_code: _ => ?_
; variables
comment:
schedule:       ISTANBUL
this:           THIS
msg_sender:     MSG_SENDER
call_value:     CALL_VALUE
call_depth:     CALL_DEPTH
active_accounts:
accounts:
requires:
    // conditions
    andBool #range(0 <= CALL_DEPTH < 1024)
    andBool #regularAddress({SCHEDULE}, THIS)
    // types
    andBool #rangeAddress(THIS)
    andBool #rangeAddress(MSG_SENDER)
    andBool #rangeUInt(256, CALL_VALUE)
    andBool #rangeUInt(256, INIT_BALANCE)
    andBool #rangeUInt(256, INIT_NONCE)
    andBool #isInf(G)
ensures:
attribute: [matching(#symGas,#symMem)]

;
; __init__
;

[init]
; for create
code: {INIT_CODE}
storage: .Map
orig_storage: .Map
G0: G0({SCHEDULE}, .WordStack, true)

[init-success]
status_code: _ => EVMC_SUCCESS
output: _ => #parseByteStack({RUNTIME_CODE})
storage: .Map => .Map
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES},  1) <- ?ZERO_HASHES_01 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES},  2) <- ?ZERO_HASHES_02 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES},  3) <- ?ZERO_HASHES_03 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES},  4) <- ?ZERO_HASHES_04 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES},  5) <- ?ZERO_HASHES_05 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES},  6) <- ?ZERO_HASHES_06 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES},  7) <- ?ZERO_HASHES_07 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES},  8) <- ?ZERO_HASHES_08 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES},  9) <- ?ZERO_HASHES_09 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 10) <- ?ZERO_HASHES_10 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 11) <- ?ZERO_HASHES_11 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 12) <- ?ZERO_HASHES_12 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 13) <- ?ZERO_HASHES_13 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 14) <- ?ZERO_HASHES_14 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 15) <- ?ZERO_HASHES_15 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 16) <- ?ZERO_HASHES_16 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 17) <- ?ZERO_HASHES_17 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 18) <- ?ZERO_HASHES_18 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 19) <- ?ZERO_HASHES_19 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 20) <- ?ZERO_HASHES_20 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 21) <- ?ZERO_HASHES_21 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 22) <- ?ZERO_HASHES_22 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 23) <- ?ZERO_HASHES_23 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 24) <- ?ZERO_HASHES_24 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 25) <- ?ZERO_HASHES_25 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 26) <- ?ZERO_HASHES_26 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 27) <- ?ZERO_HASHES_27 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 28) <- ?ZERO_HASHES_28 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 29) <- ?ZERO_HASHES_29 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 30) <- ?ZERO_HASHES_30 ]
    [ #hashedLocation({COMPILER}, {SLOT_ZERO_HASHES}, 31) <- ?ZERO_HASHES_31 ]
+ensures:
    andBool ?ZERO_HASHES_01 ==Int 111109925611824843164212799849330761292948257037696933205019304127221294824267
    andBool ?ZERO_HASHES_02 ==Int  99208582119974435635122834636860944394611999454454139265101248405002450066801
    andBool ?ZERO_HASHES_03 ==Int  90236482254272784387420235795439987838046297224132114184911355661882633139004
    andBool ?ZERO_HASHES_04 ==Int  37735605373063189145609870960383397519157271673603325697615186821228299686460
    andBool ?ZERO_HASHES_05 ==Int  71913990603354163933828411608472620759041242276514156984220416916786598645040
    andBool ?ZERO_HASHES_06 ==Int  97950246258348409692531222476457095756697573854283095464293321272902400876449
    andBool ?ZERO_HASHES_07 ==Int  61477539263323159367083172935543284935396148729545980766185719446310214598444
    andBool ?ZERO_HASHES_08 ==Int  17421805441306662828813938682339723858550903736451371212309658526853237682579
    andBool ?ZERO_HASHES_09 ==Int  36378541427962263534507524415416206454520492712868881526514165827410968138209
    andBool ?ZERO_HASHES_10 ==Int 115790397228362049466744952478840932980575707644826095658658722282297806219563
    andBool ?ZERO_HASHES_11 ==Int  49274280630555601797897865132281002146293805070798126028158380560236737348128
    andBool ?ZERO_HASHES_12 ==Int  83141414795720293663742362646790664571283415314047445910275483835985445429087
    andBool ?ZERO_HASHES_13 ==Int 101054748575760473813564301333136859612099677302306750615986031729334544803934
    andBool ?ZERO_HASHES_14 ==Int  82118745295487409076436877854822273376925616082029112448942904331137821783940
    andBool ?ZERO_HASHES_15 ==Int  96163225932810885736266036029917445088819617531019675867068430475668935471803
    andBool ?ZERO_HASHES_16 ==Int  65088336600655240038095685796880324455992690470134814168105519136673920265195
    andBool ?ZERO_HASHES_17 ==Int  63799769208876827738003032821893022143097474293424873737753651534389224801195
    andBool ?ZERO_HASHES_18 ==Int  67816509212607392382740074792956495608635882665724233434230291854030732195236
    andBool ?ZERO_HASHES_19 ==Int 112434921305070287559384313443636314384702132445424344431569901673819370811775
    andBool ?ZERO_HASHES_20 ==Int  93112230953615344385943808306254931967020084209711158834711445534019305401258
    andBool ?ZERO_HASHES_21 ==Int  62669181200805966564192421757819261985029837393920877947563891644048741760924
    andBool ?ZERO_HASHES_22 ==Int 115205076510789746548603599597779790746302978279183356048242913992201050263911
    andBool ?ZERO_HASHES_23 ==Int 104539113834876204786309677268196632426672930326563741131169818132455910346967
    andBool ?ZERO_HASHES_24 ==Int  22220639310854829338009213075933187018531271127936675242871245915956321995712
    andBool ?ZERO_HASHES_25 ==Int  15020270542076658589520891983882988038238976963402869888887748183344883676484
    andBool ?ZERO_HASHES_26 ==Int  44153847389689082926726920587762841378344527039658864594464812861203077687141
    andBool ?ZERO_HASHES_27 ==Int  56477553013929602061607210630309819251225478284985718139011950762099695862212
    andBool ?ZERO_HASHES_28 ==Int  59947690453143216863404114195220773987146401062580150977299285593826340359137
    andBool ?ZERO_HASHES_29 ==Int  61701827484336113174235061579227602710411934053193562355142130200675961312822
    andBool ?ZERO_HASHES_30 ==Int  82317687062382453000908156613654683080667757725396933779730835823850574461532
    andBool ?ZERO_HASHES_31 ==Int  68918648562210843738065282119278105929739692988049575047112145589597483221239
    // cross-check
    andBool ?ZERO_HASHES_01 ==Int #sha256(#buf(32,               0) ++ #buf(32,               0))
    andBool ?ZERO_HASHES_02 ==Int #sha256(#buf(32, ?ZERO_HASHES_01) ++ #buf(32, ?ZERO_HASHES_01))
    andBool ?ZERO_HASHES_03 ==Int #sha256(#buf(32, ?ZERO_HASHES_02) ++ #buf(32, ?ZERO_HASHES_02))
    andBool ?ZERO_HASHES_04 ==Int #sha256(#buf(32, ?ZERO_HASHES_03) ++ #buf(32, ?ZERO_HASHES_03))
    andBool ?ZERO_HASHES_05 ==Int #sha256(#buf(32, ?ZERO_HASHES_04) ++ #buf(32, ?ZERO_HASHES_04))
    andBool ?ZERO_HASHES_06 ==Int #sha256(#buf(32, ?ZERO_HASHES_05) ++ #buf(32, ?ZERO_HASHES_05))
    andBool ?ZERO_HASHES_07 ==Int #sha256(#buf(32, ?ZERO_HASHES_06) ++ #buf(32, ?ZERO_HASHES_06))
    andBool ?ZERO_HASHES_08 ==Int #sha256(#buf(32, ?ZERO_HASHES_07) ++ #buf(32, ?ZERO_HASHES_07))
    andBool ?ZERO_HASHES_09 ==Int #sha256(#buf(32, ?ZERO_HASHES_08) ++ #buf(32, ?ZERO_HASHES_08))
    andBool ?ZERO_HASHES_10 ==Int #sha256(#buf(32, ?ZERO_HASHES_09) ++ #buf(32, ?ZERO_HASHES_09))
    andBool ?ZERO_HASHES_11 ==Int #sha256(#buf(32, ?ZERO_HASHES_10) ++ #buf(32, ?ZERO_HASHES_10))
    andBool ?ZERO_HASHES_12 ==Int #sha256(#buf(32, ?ZERO_HASHES_11) ++ #buf(32, ?ZERO_HASHES_11))
    andBool ?ZERO_HASHES_13 ==Int #sha256(#buf(32, ?ZERO_HASHES_12) ++ #buf(32, ?ZERO_HASHES_12))
    andBool ?ZERO_HASHES_14 ==Int #sha256(#buf(32, ?ZERO_HASHES_13) ++ #buf(32, ?ZERO_HASHES_13))
    andBool ?ZERO_HASHES_15 ==Int #sha256(#buf(32, ?ZERO_HASHES_14) ++ #buf(32, ?ZERO_HASHES_14))
    andBool ?ZERO_HASHES_16 ==Int #sha256(#buf(32, ?ZERO_HASHES_15) ++ #buf(32, ?ZERO_HASHES_15))
    andBool ?ZERO_HASHES_17 ==Int #sha256(#buf(32, ?ZERO_HASHES_16) ++ #buf(32, ?ZERO_HASHES_16))
    andBool ?ZERO_HASHES_18 ==Int #sha256(#buf(32, ?ZERO_HASHES_17) ++ #buf(32, ?ZERO_HASHES_17))
    andBool ?ZERO_HASHES_19 ==Int #sha256(#buf(32, ?ZERO_HASHES_18) ++ #buf(32, ?ZERO_HASHES_18))
    andBool ?ZERO_HASHES_20 ==Int #sha256(#buf(32, ?ZERO_HASHES_19) ++ #buf(32, ?ZERO_HASHES_19))
    andBool ?ZERO_HASHES_21 ==Int #sha256(#buf(32, ?ZERO_HASHES_20) ++ #buf(32, ?ZERO_HASHES_20))
    andBool ?ZERO_HASHES_22 ==Int #sha256(#buf(32, ?ZERO_HASHES_21) ++ #buf(32, ?ZERO_HASHES_21))
    andBool ?ZERO_HASHES_23 ==Int #sha256(#buf(32, ?ZERO_HASHES_22) ++ #buf(32, ?ZERO_HASHES_22))
    andBool ?ZERO_HASHES_24 ==Int #sha256(#buf(32, ?ZERO_HASHES_23) ++ #buf(32, ?ZERO_HASHES_23))
    andBool ?ZERO_HASHES_25 ==Int #sha256(#buf(32, ?ZERO_HASHES_24) ++ #buf(32, ?ZERO_HASHES_24))
    andBool ?ZERO_HASHES_26 ==Int #sha256(#buf(32, ?ZERO_HASHES_25) ++ #buf(32, ?ZERO_HASHES_25))
    andBool ?ZERO_HASHES_27 ==Int #sha256(#buf(32, ?ZERO_HASHES_26) ++ #buf(32, ?ZERO_HASHES_26))
    andBool ?ZERO_HASHES_28 ==Int #sha256(#buf(32, ?ZERO_HASHES_27) ++ #buf(32, ?ZERO_HASHES_27))
    andBool ?ZERO_HASHES_29 ==Int #sha256(#buf(32, ?ZERO_HASHES_28) ++ #buf(32, ?ZERO_HASHES_28))
    andBool ?ZERO_HASHES_30 ==Int #sha256(#buf(32, ?ZERO_HASHES_29) ++ #buf(32, ?ZERO_HASHES_29))
    andBool ?ZERO_HASHES_31 ==Int #sha256(#buf(32, ?ZERO_HASHES_30) ++ #buf(32, ?ZERO_HASHES_30))
    // gas
    andBool ?GAS_COST ==Int 716470
    andBool ?MEM_COST ==Int 6358
refund: _ => ?_
+requires:
    // conditions
    andBool CALL_VALUE ==Int 0

[init-revert]
status_code: _ => EVMC_REVERT
+requires:
    // conditions
    andBool CALL_VALUE =/=Int 0

;
; get_deposit_root
;

[get_deposit_root]
; The term `#buf(EXTRA_CALL_DATA_SIZE, EXTRA_CALL_DATA)` models certain extra call-data added accidently or intentionally.
; This ensures that the function works correctly even in such a case.
call_data: #abiCallData("get_deposit_root", .TypedArgs) ++ #buf(EXTRA_CALL_DATA_SIZE, EXTRA_CALL_DATA)
+requires:
    // types
    andBool #rangeUInt(256, EXTRA_CALL_DATA_SIZE)
G0: G0({SCHEDULE}, #abiCallData("get_deposit_root", .TypedArgs), false)

[get_deposit_root-success]
status_code: _ => EVMC_SUCCESS
output: _ => #buf(32, #sha256(#buf(32, #node(32, {DEPOSIT_COUNT}, M)) ++ #toLittleEndian64({DEPOSIT_COUNT}) ++ #buf(24, 0)))
storage: M  /* constant function; no storage update */
+requires:
    // conditions
    andBool CALL_VALUE ==Int 0
    // types
    andBool isStorage(M)
+ensures:
    // gas
    andBool ?GAS_COST ==Int #itv(76849, 77169)
    andBool ?MEM_COST ==Int 3456
DEPOSIT_COUNT: select(M, #hashedLocation({COMPILER}, {SLOT_DEPOSIT_COUNT}, .IntList))

[get_deposit_root-success-loop]
_inherit_:
k: #execute
pc: 4305 /* loophead */
word_stack: (HEIGHT => HEIGHT +Int 1) : #size(HEIGHT => HEIGHT +Int 1, {DEPOSIT_COUNT}) : #node(HEIGHT => HEIGHT +Int 1, {DEPOSIT_COUNT}, M) : _ : _ : _ : .WordStack
local_mem: MEM => MEM
    [ {NEXT_FREE_ADDR} +Int  32 := #buf(32, ?_) ]
    [ {NEXT_FREE_ADDR} +Int  64 := #buf(32, ?_) ]
    [ {NEXT_FREE_ADDR}          := #buf(32, 64) ]
    [ 64                        := #buf(32, {NEXT_FREE_ADDR} +Int 96) ]
    [ {NEXT_FREE_ADDR} +Int  96 := #buf(32, ?_) ]
    [ {NEXT_FREE_ADDR} +Int 128 := #buf(32, ?_) ]
    [ {NEXT_FREE_ADDR} +Int 160 := selectRange(?_, ?_, 32) ]
storage: M
+requires:
    // conditions - invariants
    andBool HEIGHT <Int 32
    andBool {NEXT_FREE_ADDR} >=Int 128
    andBool {NEXT_FREE_ADDR} <=Int 4000
    // types
    andBool #rangeUInt(256, HEIGHT)
    andBool isStorage(M)
    andBool MU <=Int {NEXT_FREE_ADDR} +Int 96
ensures:
    // gas
    andBool ?GUSED_NEW >=Int GUSED +Int 2268
    andBool ?GUSED_NEW <=Int GUSED +Int 2278
gas: #symGas({SCHEDULE}, G, GBASE, GUSED => ?GUSED_NEW, 0, {MEMORY_USED})
memory_used: #symMem(MU => {NEXT_FREE_ADDR} +Int 192)
DEPOSIT_COUNT: select(M, #hashedLocation({COMPILER}, {SLOT_DEPOSIT_COUNT}, .IntList))
NEXT_FREE_ADDR: #asWord(selectRange(MEM, 64, 32))
attribute: [matching(#size,#node,#buf,selectRange,storeRange,#symGas,#symMem)]

[get_deposit_root-success-loop-trusted]
gas: #symGas({SCHEDULE}, G, GBASE, GUSED => GUSED +Int #itv(2268, 2278), 0, {MEMORY_USED})
ensures:
attribute: [trusted, matching(#size,#node,#symGas,#symMem)]

[get_deposit_root-revert]
status_code: _ => EVMC_REVERT
+requires:
    // conditions
    andBool CALL_VALUE =/=Int 0

;
; get_deposit_count
;

[get_deposit_count]
; The term `#buf(EXTRA_CALL_DATA_SIZE, EXTRA_CALL_DATA)` models certain extra call-data added accidently or intentionally.
; This ensures that the function works correctly even in such a case.
call_data: #abiCallData("get_deposit_count", .TypedArgs) ++ #buf(EXTRA_CALL_DATA_SIZE, EXTRA_CALL_DATA)
+requires:
    // types
    andBool #rangeUInt(256, EXTRA_CALL_DATA_SIZE)
G0: G0({SCHEDULE}, #abiCallData("get_deposit_count", .TypedArgs), false)

[get_deposit_count-success]
status_code: _ => EVMC_SUCCESS
output: _ => #encodeArgs(#bytes(#toLittleEndian64({DEPOSIT_COUNT}))) /* #buf(32, 32) ++ #buf(32, 8) ++ #toLittleEndian64(DEPOSIT_COUNT) ++ #buf(24, 0) */
storage: M  /* constant function; no storage update */
+requires:
    // conditions
    andBool CALL_VALUE ==Int 0
    // types
    andBool isStorage(M)
+ensures:
    // gas
    andBool ?GAS_COST ==Int 2187
    andBool ?MEM_COST ==Int 288
DEPOSIT_COUNT: select(M, #hashedLocation({COMPILER}, {SLOT_DEPOSIT_COUNT}, .IntList))

[get_deposit_count-revert]
status_code: _ => EVMC_REVERT
+requires:
    // conditions
    andBool CALL_VALUE =/=Int 0

;
; deposit
;

[deposit]
; #buf(32, 128) ++ #buf(32, 224) ++ #buf(32, 288) ++ #buf(32, DEPOSIT_DATA_ROOT) // header
; ++ #buf(32, 48) ++ #buf(48, PUBKEY) ++ #buf(16, 0)                             // pubkey + zero-padding
; ++ #buf(32, 32) ++ #buf(32, WITHDRAWAL_CREDENTIALS)                            // withdrawal_credentials
; ++ #buf(32, 96) ++ #buf(96, SIGNATURE)                                         // signature
call_data: #abiCallData("deposit", (
            #bytes(#buf({PUBKEY_LENGTH},                 PUBKEY)),
            #bytes(#buf({WITHDRAWAL_CREDENTIALS_LENGTH}, WITHDRAWAL_CREDENTIALS)),
            #bytes(#buf({SIGNATURE_LENGTH},              SIGNATURE)),
            #bytes32(DEPOSIT_DATA_ROOT) ))
storage: M
+requires:
    // ranges
    andBool #range(0 <= PUBKEY                 < 2 ^Int ({PUBKEY_LENGTH}                 *Int 8))
    andBool #range(0 <= WITHDRAWAL_CREDENTIALS < 2 ^Int ({WITHDRAWAL_CREDENTIALS_LENGTH} *Int 8))
    andBool #range(0 <= SIGNATURE              < 2 ^Int ({SIGNATURE_LENGTH}              *Int 8))
    andBool #rangeUInt(256, DEPOSIT_DATA_ROOT)
    // types
    andBool isStorage(M)
;
DEPOSIT_COUNT: select(M, #hashedLocation({COMPILER}, {SLOT_DEPOSIT_COUNT}, .IntList))
PUBKEY_LENGTH:                 48
WITHDRAWAL_CREDENTIALS_LENGTH: 32
SIGNATURE_LENGTH:              96
MAX_DEPOSIT_COUNT:  4294967295
GWEI_IN_WEI:        1000000000
DEPOSIT_AMOUNT: (CALL_VALUE /Int {GWEI_IN_WEI})
;
PUBKEY_ROOT: #sha256(#buf(48, PUBKEY) ++ #buf(16, 0))
TMP1: #sha256(#bufSeg(#buf(96, SIGNATURE), 0, 64))
TMP2: #sha256(#bufSeg(#buf(96, SIGNATURE), 64, 32) ++ #buf(32, 0))
SIGNATURE_ROOT: #sha256(#buf(32, {TMP1}) ++ #buf(32, {TMP2}))
TMP3: #sha256(#buf(32, {PUBKEY_ROOT}) ++ #buf(32, WITHDRAWAL_CREDENTIALS))
TMP4: #sha256(#toLittleEndian64({DEPOSIT_AMOUNT}) ++ #buf(24, 0) ++ #buf(32, {SIGNATURE_ROOT}))
NODE: #sha256(#buf(32, {TMP3}) ++ #buf(32, {TMP4}))
;
G0: #itv({G0_MIN}, {G0_MAX})
G0_MIN: G0({SCHEDULE}, #abiCallData("deposit", (
            #bytes(#buf({PUBKEY_LENGTH},                 0)),
            #bytes(#buf({WITHDRAWAL_CREDENTIALS_LENGTH}, 0)),
            #bytes(#buf({SIGNATURE_LENGTH},              0)),
            #bytes32(0) )), false)
G0_MAX: G0({SCHEDULE}, #abiCallData("deposit", (
            #bytes(#buf({PUBKEY_LENGTH},                 2 ^Int ({PUBKEY_LENGTH}                 *Int 8) -Int 1)),
            #bytes(#buf({WITHDRAWAL_CREDENTIALS_LENGTH}, 2 ^Int ({WITHDRAWAL_CREDENTIALS_LENGTH} *Int 8) -Int 1)),
            #bytes(#buf({SIGNATURE_LENGTH},              2 ^Int ({SIGNATURE_LENGTH}              *Int 8) -Int 1)),
            #bytes32(2 ^Int 256 -Int 1) )), false)

; #### `DepositData`
;
; ```python
; class DepositData(Container):
;     pubkey: BLSPubkey
;     withdrawal_credentials: Hash
;     amount: Gwei
;     signature: BLSSignature
; ```

;                                    ___________________________ node _________________________
;                                   /                                                          \
;                    __________ tmp3 ___________________                        ______________ tmp4 _______________
;                   /                                   \                      /                                   \
;           pubkey_root                       withdrawal_credentials       amount                        _____ signature_root __________
;           /       \                                                                                   /                               \
;   pubkey[0:32]  pubkey[32:48]++zero[0:16]                                                           tmp1                             tmp2
;                                                                                                  /       \                        /        \
;                                                                                       signature[0:32]  signature[32:64]  signature[64:96]  zero[0:32]

[deposit-success]
status_code: _ => EVMC_SUCCESS
storage: M => M
    [ #hashedLocation({COMPILER}, {SLOT_DEPOSIT_COUNT}, .IntList) <- {DEPOSIT_COUNT} +Int 1 ]
    [ #hashedLocation({COMPILER}, {SLOT_BRANCH}, ?HEIGHT) <- ?NODE ]
log: _:List ( .List => ListItem(#abiEventLog(THIS, "DepositEvent",
            #bytes(#buf({PUBKEY_LENGTH}, PUBKEY)),
            #bytes(#buf({WITHDRAWAL_CREDENTIALS_LENGTH}, WITHDRAWAL_CREDENTIALS)),
            #bytes(#toLittleEndian64({DEPOSIT_AMOUNT})),
            #bytes(#buf({SIGNATURE_LENGTH}, SIGNATURE)),
            #bytes(#toLittleEndian64({DEPOSIT_COUNT})) )))
+requires:
    // conditions
    andBool CALL_VALUE >=Int 10 ^Int 18
    andBool CALL_VALUE modInt {GWEI_IN_WEI} ==Int 0
    andBool {DEPOSIT_AMOUNT} <Int 2 ^Int 64
    andBool {NODE} ==Int DEPOSIT_DATA_ROOT
    andBool {DEPOSIT_COUNT} <Int {MAX_DEPOSIT_COUNT}
+ensures:
    andBool ?SIZE_00 ==Int {DEPOSIT_COUNT} +Int 1
    andBool ?SIZE_01 ==Int ?SIZE_00 /Int 2
    andBool ?SIZE_02 ==Int ?SIZE_01 /Int 2
    andBool ?SIZE_03 ==Int ?SIZE_02 /Int 2
    andBool ?SIZE_04 ==Int ?SIZE_03 /Int 2
    andBool ?SIZE_05 ==Int ?SIZE_04 /Int 2
    andBool ?SIZE_06 ==Int ?SIZE_05 /Int 2
    andBool ?SIZE_07 ==Int ?SIZE_06 /Int 2
    andBool ?SIZE_08 ==Int ?SIZE_07 /Int 2
    andBool ?SIZE_09 ==Int ?SIZE_08 /Int 2
    andBool ?SIZE_10 ==Int ?SIZE_09 /Int 2
    andBool ?SIZE_11 ==Int ?SIZE_10 /Int 2
    andBool ?SIZE_12 ==Int ?SIZE_11 /Int 2
    andBool ?SIZE_13 ==Int ?SIZE_12 /Int 2
    andBool ?SIZE_14 ==Int ?SIZE_13 /Int 2
    andBool ?SIZE_15 ==Int ?SIZE_14 /Int 2
    andBool ?SIZE_16 ==Int ?SIZE_15 /Int 2
    andBool ?SIZE_17 ==Int ?SIZE_16 /Int 2
    andBool ?SIZE_18 ==Int ?SIZE_17 /Int 2
    andBool ?SIZE_19 ==Int ?SIZE_18 /Int 2
    andBool ?SIZE_20 ==Int ?SIZE_19 /Int 2
    andBool ?SIZE_21 ==Int ?SIZE_20 /Int 2
    andBool ?SIZE_22 ==Int ?SIZE_21 /Int 2
    andBool ?SIZE_23 ==Int ?SIZE_22 /Int 2
    andBool ?SIZE_24 ==Int ?SIZE_23 /Int 2
    andBool ?SIZE_25 ==Int ?SIZE_24 /Int 2
    andBool ?SIZE_26 ==Int ?SIZE_25 /Int 2
    andBool ?SIZE_27 ==Int ?SIZE_26 /Int 2
    andBool ?SIZE_28 ==Int ?SIZE_27 /Int 2
    andBool ?SIZE_29 ==Int ?SIZE_28 /Int 2
    andBool ?SIZE_30 ==Int ?SIZE_29 /Int 2
    andBool ?SIZE_31 ==Int ?SIZE_30 /Int 2
    //
    andBool ?NODE_01 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH},  0))) ++ #buf(32, {NODE}))
    andBool ?NODE_02 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH},  1))) ++ #buf(32, ?NODE_01))
    andBool ?NODE_03 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH},  2))) ++ #buf(32, ?NODE_02))
    andBool ?NODE_04 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH},  3))) ++ #buf(32, ?NODE_03))
    andBool ?NODE_05 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH},  4))) ++ #buf(32, ?NODE_04))
    andBool ?NODE_06 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH},  5))) ++ #buf(32, ?NODE_05))
    andBool ?NODE_07 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH},  6))) ++ #buf(32, ?NODE_06))
    andBool ?NODE_08 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH},  7))) ++ #buf(32, ?NODE_07))
    andBool ?NODE_09 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH},  8))) ++ #buf(32, ?NODE_08))
    andBool ?NODE_10 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH},  9))) ++ #buf(32, ?NODE_09))
    andBool ?NODE_11 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 10))) ++ #buf(32, ?NODE_10))
    andBool ?NODE_12 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 11))) ++ #buf(32, ?NODE_11))
    andBool ?NODE_13 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 12))) ++ #buf(32, ?NODE_12))
    andBool ?NODE_14 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 13))) ++ #buf(32, ?NODE_13))
    andBool ?NODE_15 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 14))) ++ #buf(32, ?NODE_14))
    andBool ?NODE_16 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 15))) ++ #buf(32, ?NODE_15))
    andBool ?NODE_17 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 16))) ++ #buf(32, ?NODE_16))
    andBool ?NODE_18 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 17))) ++ #buf(32, ?NODE_17))
    andBool ?NODE_19 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 18))) ++ #buf(32, ?NODE_18))
    andBool ?NODE_20 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 19))) ++ #buf(32, ?NODE_19))
    andBool ?NODE_21 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 20))) ++ #buf(32, ?NODE_20))
    andBool ?NODE_22 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 21))) ++ #buf(32, ?NODE_21))
    andBool ?NODE_23 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 22))) ++ #buf(32, ?NODE_22))
    andBool ?NODE_24 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 23))) ++ #buf(32, ?NODE_23))
    andBool ?NODE_25 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 24))) ++ #buf(32, ?NODE_24))
    andBool ?NODE_26 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 25))) ++ #buf(32, ?NODE_25))
    andBool ?NODE_27 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 26))) ++ #buf(32, ?NODE_26))
    andBool ?NODE_28 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 27))) ++ #buf(32, ?NODE_27))
    andBool ?NODE_29 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 28))) ++ #buf(32, ?NODE_28))
    andBool ?NODE_30 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 29))) ++ #buf(32, ?NODE_29))
    andBool ?NODE_31 ==Int #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, 30))) ++ #buf(32, ?NODE_30))
    //
    andBool
          #if 1 &Int ?SIZE_00 ==Int 1 #then ?HEIGHT ==Int  0 andBool ?NODE ==Int {NODE}
    #else #if 1 &Int ?SIZE_01 ==Int 1 #then ?HEIGHT ==Int  1 andBool ?NODE ==Int ?NODE_01
    #else #if 1 &Int ?SIZE_02 ==Int 1 #then ?HEIGHT ==Int  2 andBool ?NODE ==Int ?NODE_02
    #else #if 1 &Int ?SIZE_03 ==Int 1 #then ?HEIGHT ==Int  3 andBool ?NODE ==Int ?NODE_03
    #else #if 1 &Int ?SIZE_04 ==Int 1 #then ?HEIGHT ==Int  4 andBool ?NODE ==Int ?NODE_04
    #else #if 1 &Int ?SIZE_05 ==Int 1 #then ?HEIGHT ==Int  5 andBool ?NODE ==Int ?NODE_05
    #else #if 1 &Int ?SIZE_06 ==Int 1 #then ?HEIGHT ==Int  6 andBool ?NODE ==Int ?NODE_06
    #else #if 1 &Int ?SIZE_07 ==Int 1 #then ?HEIGHT ==Int  7 andBool ?NODE ==Int ?NODE_07
    #else #if 1 &Int ?SIZE_08 ==Int 1 #then ?HEIGHT ==Int  8 andBool ?NODE ==Int ?NODE_08
    #else #if 1 &Int ?SIZE_09 ==Int 1 #then ?HEIGHT ==Int  9 andBool ?NODE ==Int ?NODE_09
    #else #if 1 &Int ?SIZE_10 ==Int 1 #then ?HEIGHT ==Int 10 andBool ?NODE ==Int ?NODE_10
    #else #if 1 &Int ?SIZE_11 ==Int 1 #then ?HEIGHT ==Int 11 andBool ?NODE ==Int ?NODE_11
    #else #if 1 &Int ?SIZE_12 ==Int 1 #then ?HEIGHT ==Int 12 andBool ?NODE ==Int ?NODE_12
    #else #if 1 &Int ?SIZE_13 ==Int 1 #then ?HEIGHT ==Int 13 andBool ?NODE ==Int ?NODE_13
    #else #if 1 &Int ?SIZE_14 ==Int 1 #then ?HEIGHT ==Int 14 andBool ?NODE ==Int ?NODE_14
    #else #if 1 &Int ?SIZE_15 ==Int 1 #then ?HEIGHT ==Int 15 andBool ?NODE ==Int ?NODE_15
    #else #if 1 &Int ?SIZE_16 ==Int 1 #then ?HEIGHT ==Int 16 andBool ?NODE ==Int ?NODE_16
    #else #if 1 &Int ?SIZE_17 ==Int 1 #then ?HEIGHT ==Int 17 andBool ?NODE ==Int ?NODE_17
    #else #if 1 &Int ?SIZE_18 ==Int 1 #then ?HEIGHT ==Int 18 andBool ?NODE ==Int ?NODE_18
    #else #if 1 &Int ?SIZE_19 ==Int 1 #then ?HEIGHT ==Int 19 andBool ?NODE ==Int ?NODE_19
    #else #if 1 &Int ?SIZE_20 ==Int 1 #then ?HEIGHT ==Int 20 andBool ?NODE ==Int ?NODE_20
    #else #if 1 &Int ?SIZE_21 ==Int 1 #then ?HEIGHT ==Int 21 andBool ?NODE ==Int ?NODE_21
    #else #if 1 &Int ?SIZE_22 ==Int 1 #then ?HEIGHT ==Int 22 andBool ?NODE ==Int ?NODE_22
    #else #if 1 &Int ?SIZE_23 ==Int 1 #then ?HEIGHT ==Int 23 andBool ?NODE ==Int ?NODE_23
    #else #if 1 &Int ?SIZE_24 ==Int 1 #then ?HEIGHT ==Int 24 andBool ?NODE ==Int ?NODE_24
    #else #if 1 &Int ?SIZE_25 ==Int 1 #then ?HEIGHT ==Int 25 andBool ?NODE ==Int ?NODE_25
    #else #if 1 &Int ?SIZE_26 ==Int 1 #then ?HEIGHT ==Int 26 andBool ?NODE ==Int ?NODE_26
    #else #if 1 &Int ?SIZE_27 ==Int 1 #then ?HEIGHT ==Int 27 andBool ?NODE ==Int ?NODE_27
    #else #if 1 &Int ?SIZE_28 ==Int 1 #then ?HEIGHT ==Int 28 andBool ?NODE ==Int ?NODE_28
    #else #if 1 &Int ?SIZE_29 ==Int 1 #then ?HEIGHT ==Int 29 andBool ?NODE ==Int ?NODE_29
    #else #if 1 &Int ?SIZE_30 ==Int 1 #then ?HEIGHT ==Int 30 andBool ?NODE ==Int ?NODE_30
    #else #if 1 &Int ?SIZE_31 ==Int 1 #then ?HEIGHT ==Int 31 andBool ?NODE ==Int ?NODE_31
    #else false #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi #fi
    // gas
    andBool ?GAS_COST_MIN >=Int 23252 andBool ?GAS_COST_MAX >=Int  61652 /* min/max diff = 38400 = (20000 - 800) * 2 */
    andBool ?GAS_COST_MIN <=Int 93529 andBool ?GAS_COST_MAX <=Int 131929 /* min/max diff = 38400 = (20000 - 800) * 2 */
    andBool ?MEM_COST >=Int 1024
    andBool ?MEM_COST <=Int 4000 /* = 1024 + 31 * 96 */
gas: #symGas({SCHEDULE}, G, {G0}, 0 => #itv(?GAS_COST_MIN, ?GAS_COST_MAX), 0, {MEMORY_USED})
refund: _ => ?_
attribute: [matching(store,#symGas,#symMem,#itv)]

[deposit-success-loop]
_inherit_:
k: #execute
pc: 4000 => 3950 /* loophead */
word_stack: (HEIGHT => HEIGHT +Int 1) : (SIZE => SIZE /Int 2) : (NODE => #sha256(#buf(32, select(M, #hashedLocation({COMPILER}, {SLOT_BRANCH}, HEIGHT))) ++ #buf(32, NODE))) : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack
local_mem: MEM => MEM
    [ {NEXT_FREE_ADDR} +Int  32 := #buf(32, ?_) ]
    [ {NEXT_FREE_ADDR} +Int  64 := #buf(32, ?_) ]
    [ {NEXT_FREE_ADDR}          := #buf(32, 64) ]
    [ 64                        := #buf(32, {NEXT_FREE_ADDR} +Int 96) ]
    [ {NEXT_FREE_ADDR} +Int  96 := #buf(32, ?_) ]
    [ {NEXT_FREE_ADDR} +Int 128 := #buf(32, ?_) ]
    [ {NEXT_FREE_ADDR} +Int 160 := selectRange(?_, ?_, 32) ]
storage: M
+requires:
    // conditions
    andBool 1 &Int SIZE =/=Int 1
    // conditions - invariants
    andBool HEIGHT <Int 32
    andBool {NEXT_FREE_ADDR} >=Int 928
    andBool {NEXT_FREE_ADDR} <=Int 5000
    // types
    andBool #rangeUInt(256, HEIGHT)
    andBool #rangeUInt(256, SIZE)
    andBool #rangeUInt(256, NODE)
    andBool isStorage(M)
    // gas conditions - invariants
    andBool MU <=Int {NEXT_FREE_ADDR} +Int 96
gas: #symGas({SCHEDULE}, G, GBASE, GUSED => GUSED +Int 2210, 0, {MEMORY_USED})
memory_used: #symMem(MU => {NEXT_FREE_ADDR} +Int 192)
NEXT_FREE_ADDR: #asWord(selectRange(MEM, 64, 32))
attribute: [matching(#buf,selectRange,storeRange,#symGas,#symMem)]

[deposit-success-loop-trusted]
attribute: [trusted, matching(#symGas,#symMem)]

[deposit-revert]
status_code: _ => EVMC_REVERT
log: _ => ?_
+requires:
    // conditions
    andBool notBool (
            CALL_VALUE >=Int 10 ^Int 18
    andBool CALL_VALUE modInt {GWEI_IN_WEI} ==Int 0
    andBool {DEPOSIT_AMOUNT} <Int 2 ^Int 64
    andBool {NODE} ==Int DEPOSIT_DATA_ROOT
    andBool {DEPOSIT_COUNT} <Int {MAX_DEPOSIT_COUNT}
    )
+ensures:
    // gas
    andBool ?GAS_COST >=Int   855
    andBool ?GAS_COST <=Int 20798
    andBool ?MEM_COST >=Int   260
    andBool ?MEM_COST <=Int  1092

[deposit-calldata-decoding]
_inherit_:
; arbitrary calldata including ill-formed one
call_data: #buf(CALL_DATA_SIZE, CALL_DATA)
+requires:
    // types
    andBool #rangeUInt(256, CALL_DATA_SIZE)
    // conditions
    andBool #asWord(#take(4, {CALL_DATA})) ==Int 579424536 /* 0x22895118 deposit */
    andBool CALL_DATA_SIZE >=Int 4
;
PUBKEY_OFFSET:                 #asWord({CALL_DATA}[   4 .. 32 ])
WITHDRAWAL_CREDENTIALS_OFFSET: #asWord({CALL_DATA}[  36 .. 32 ])
SIGNATURE_OFFSET:              #asWord({CALL_DATA}[  68 .. 32 ])
DEPOSIT_DATA_ROOT:             #asWord({CALL_DATA}[ 100 .. 32 ])
;
PUBKEY_SIZE:                 #asWord({CALL_DATA}[ 4 +Int {PUBKEY_OFFSET}                 .. 32 ])
WITHDRAWAL_CREDENTIALS_SIZE: #asWord({CALL_DATA}[ 4 +Int {WITHDRAWAL_CREDENTIALS_OFFSET} .. 32 ])
SIGNATURE_SIZE:              #asWord({CALL_DATA}[ 4 +Int {SIGNATURE_OFFSET}              .. 32 ])
;
PUBKEY_BEGIN:                 (4 +Int {PUBKEY_OFFSET}                 +Int 32)
WITHDRAWAL_CREDENTIALS_BEGIN: (4 +Int {WITHDRAWAL_CREDENTIALS_OFFSET} +Int 32)
SIGNATURE_BEGIN:              (4 +Int {SIGNATURE_OFFSET}              +Int 32)
;
PUBKEY_END:                 ({PUBKEY_BEGIN}                 +Int {PUBKEY_SIZE})
WITHDRAWAL_CREDENTIALS_END: ({WITHDRAWAL_CREDENTIALS_BEGIN} +Int {WITHDRAWAL_CREDENTIALS_SIZE})
SIGNATURE_END:              ({SIGNATURE_BEGIN}              +Int {SIGNATURE_SIZE})
;
G0: GBASE

[deposit-calldata-decoding-success]
k: #execute
pc: 0 => 772 /* tag_21: beginning of the actual function body */
word_stack: .WordStack => {DEPOSIT_DATA_ROOT} : {SIGNATURE_SIZE} : {SIGNATURE_BEGIN} : {WITHDRAWAL_CREDENTIALS_SIZE} : {WITHDRAWAL_CREDENTIALS_BEGIN} : {PUBKEY_SIZE} : {PUBKEY_BEGIN} : ?_ : ?_ : .WordStack
local_mem: .IMap => .IMap [ 64 := #buf(32, 128) ]
+requires:
    // conditions
    andBool CALL_DATA_SIZE >=Int 4 +Int 4 *Int 32
    //
    andBool {PUBKEY_OFFSET} <=Int 2 ^Int 32
    andBool {PUBKEY_SIZE}   <=Int 2 ^Int 32
    andBool {PUBKEY_BEGIN}  <=Int CALL_DATA_SIZE
    andBool {PUBKEY_END}    <=Int CALL_DATA_SIZE
    //
    andBool {WITHDRAWAL_CREDENTIALS_OFFSET} <=Int 2 ^Int 32
    andBool {WITHDRAWAL_CREDENTIALS_SIZE}   <=Int 2 ^Int 32
    andBool {WITHDRAWAL_CREDENTIALS_BEGIN}  <=Int CALL_DATA_SIZE
    andBool {WITHDRAWAL_CREDENTIALS_END}    <=Int CALL_DATA_SIZE
    //
    andBool {SIGNATURE_OFFSET} <=Int 2 ^Int 32
    andBool {SIGNATURE_SIZE}   <=Int 2 ^Int 32
    andBool {SIGNATURE_BEGIN}  <=Int CALL_DATA_SIZE
    andBool {SIGNATURE_END}    <=Int CALL_DATA_SIZE

[deposit-calldata-decoding-revert]
status_code: _ => EVMC_REVERT
+requires:
    // conditions
    andBool notBool (
            CALL_DATA_SIZE >=Int 4 +Int 4 *Int 32
    //
    andBool {PUBKEY_OFFSET} <=Int 2 ^Int 32
    andBool {PUBKEY_SIZE}   <=Int 2 ^Int 32
    andBool {PUBKEY_BEGIN}  <=Int CALL_DATA_SIZE
    andBool {PUBKEY_END}    <=Int CALL_DATA_SIZE
    //
    andBool {WITHDRAWAL_CREDENTIALS_OFFSET} <=Int 2 ^Int 32
    andBool {WITHDRAWAL_CREDENTIALS_SIZE}   <=Int 2 ^Int 32
    andBool {WITHDRAWAL_CREDENTIALS_BEGIN}  <=Int CALL_DATA_SIZE
    andBool {WITHDRAWAL_CREDENTIALS_END}    <=Int CALL_DATA_SIZE
    //
    andBool {SIGNATURE_OFFSET} <=Int 2 ^Int 32
    andBool {SIGNATURE_SIZE}   <=Int 2 ^Int 32
    andBool {SIGNATURE_BEGIN}  <=Int CALL_DATA_SIZE
    andBool {SIGNATURE_END}    <=Int CALL_DATA_SIZE
    )

;
; supportsInterface
;

[supportsInterface]
call_data: #buf(CALL_DATA_SIZE, CALL_DATA)
+requires:
    // types
    andBool #rangeUInt(256, CALL_DATA_SIZE)
    // conditions
    andBool #asWord(#take(4, {CALL_DATA})) ==Int 33540519 /* 0x01ffc9a7 supportsInterface */
    andBool CALL_DATA_SIZE >=Int 4
;
INTERFACE_ID: #asWord({CALL_DATA}[ 4 .. 4 ])
;
G0: #itv({G0_MIN}, {G0_MAX})
G0_MIN: G0({SCHEDULE}, #abiCallData("supportsInterface", #bytes4(0)), false)
G0_MAX: G0({SCHEDULE}, #abiCallData("supportsInterface", #bytes4(maxUInt32)), false)

[supportsInterface-success]
status_code: _ => EVMC_SUCCESS
output: _ => #encodeArgs(#bool(bool2Word({INTERFACE_ID} ==Int 33540519 /* 0x01ffc9a7 */ orBool {INTERFACE_ID} ==Int 2237925639 /* 0x85640907 */)))
+requires:
    // conditions
    andBool CALL_VALUE ==Int 0
    andBool CALL_DATA_SIZE >=Int 4 +Int 32
+ensures:
    // gas
    andBool ?GAS_COST >=Int 254 andBool ?GAS_COST <=Int 271
    andBool ?MEM_COST ==Int 160

[supportsInterface-revert]
status_code: _ => EVMC_REVERT
+requires:
    // conditions
    andBool notBool (
            CALL_VALUE ==Int 0
    andBool CALL_DATA_SIZE >=Int 4 +Int 32
    )

;
; revert cases
;

[revert]
status_code: _ => EVMC_REVERT
G0: GBASE

; Revert if the first four bytes are invalid (or not fully provided).
[revert-invalid_function_identifier]
call_data: #buf(CALL_DATA_SIZE, CALL_DATA)

[revert-invalid_function_identifier-lt_4]
+requires:
    // conditions
    andBool #range(0 <= CALL_DATA_SIZE < 4)

[revert-invalid_function_identifier-ge_4]
+requires:
    // conditions
    andBool #asWord(#bufSeg(#buf(CALL_DATA_SIZE, CALL_DATA), 0, 4)) =/=Int 33540519   /* 0x01ffc9a7 supportsInterface */
    andBool #asWord(#bufSeg(#buf(CALL_DATA_SIZE, CALL_DATA), 0, 4)) =/=Int 579424536  /* 0x22895118 deposit           */
    andBool #asWord(#bufSeg(#buf(CALL_DATA_SIZE, CALL_DATA), 0, 4)) =/=Int 1646252336 /* 0x621fd130 get_deposit_count */
    andBool #asWord(#bufSeg(#buf(CALL_DATA_SIZE, CALL_DATA), 0, 4)) =/=Int 3321006383 /* 0xc5f2892f get_deposit_root  */
    andBool CALL_DATA_SIZE >=Int 4

;
; globals
;

[pgm]
COMPILER: "StaticArray"
; storage slots
SLOT_BRANCH: 0
SLOT_DEPOSIT_COUNT: 32
SLOT_ZERO_HASHES: 33
; bytecode
RUNTIME_CODE: "0x{RUNTIME_CODE_BIN}"
INIT_CODE: "0x{INIT_CODE_BIN}"
RUNTIME_CODE_BIN: 60806040526004361061003f5760003560e01c806301ffc9a71461004457806322895118146100a4578063621fd130146101ba578063c5f2892f14610244575b600080fd5b34801561005057600080fd5b506100906004803603602081101561006757600080fd5b50357fffffffff000000000000000000000000000000000000000000000000000000001661026b565b604080519115158252519081900360200190f35b6101b8600480360360808110156100ba57600080fd5b8101906020810181356401000000008111156100d557600080fd5b8201836020820111156100e757600080fd5b8035906020019184600183028401116401000000008311171561010957600080fd5b91939092909160208101903564010000000081111561012757600080fd5b82018360208201111561013957600080fd5b8035906020019184600183028401116401000000008311171561015b57600080fd5b91939092909160208101903564010000000081111561017957600080fd5b82018360208201111561018b57600080fd5b803590602001918460018302840111640100000000831117156101ad57600080fd5b919350915035610304565b005b3480156101c657600080fd5b506101cf6110b5565b6040805160208082528351818301528351919283929083019185019080838360005b838110156102095781810151838201526020016101f1565b50505050905090810190601f1680156102365780820380516001836020036101000a031916815260200191505b509250505060405180910390f35b34801561025057600080fd5b506102596110c7565b60408051918252519081900360200190f35b60007fffffffff0000000000000000000000000000000000000000000000000000000082167f01ffc9a70000000000000000000000000000000000000000000000000000000014806102fe57507fffffffff0000000000000000000000000000000000000000000000000000000082167f8564090700000000000000000000000000000000000000000000000000000000145b92915050565b6030861461035d576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260268152602001806118056026913960400191505060405180910390fd5b602084146103b6576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252603681526020018061179c6036913960400191505060405180910390fd5b6060821461040f576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260298152602001806118786029913960400191505060405180910390fd5b670de0b6b3a7640000341015610470576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260268152602001806118526026913960400191505060405180910390fd5b633b9aca003406156104cd576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260338152602001806117d26033913960400191505060405180910390fd5b633b9aca00340467ffffffffffffffff811115610535576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252602781526020018061182b6027913960400191505060405180910390fd5b6060610540826114ba565b90507f649bbc62d0e31342afea4e5cd82d4049e7e1ee912fc0889aa790803be39038c589898989858a8a6105756020546114ba565b6040805160a0808252810189905290819060208201908201606083016080840160c085018e8e80828437600083820152601f017fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe01690910187810386528c815260200190508c8c808284376000838201819052601f9091017fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe01690920188810386528c5181528c51602091820193918e019250908190849084905b83811015610648578181015183820152602001610630565b50505050905090810190601f1680156106755780820380516001836020036101000a031916815260200191505b5086810383528881526020018989808284376000838201819052601f9091017fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0169092018881038452895181528951602091820193918b019250908190849084905b838110156106ef5781810151838201526020016106d7565b50505050905090810190601f16801561071c5780820380516001836020036101000a031916815260200191505b509d505050505050505050505050505060405180910390a1600060028a8a600060801b604051602001808484808284377fffffffffffffffffffffffffffffffff0000000000000000000000000000000090941691909301908152604080517ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0818403018152601090920190819052815191955093508392506020850191508083835b602083106107fc57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe090920191602091820191016107bf565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610859573d6000803e3d6000fd5b5050506040513d602081101561086e57600080fd5b5051905060006002806108846040848a8c6116fe565b6040516020018083838082843780830192505050925050506040516020818303038152906040526040518082805190602001908083835b602083106108f857805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe090920191602091820191016108bb565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610955573d6000803e3d6000fd5b5050506040513d602081101561096a57600080fd5b5051600261097b896040818d6116fe565b60405160009060200180848480828437919091019283525050604080518083038152602092830191829052805190945090925082918401908083835b602083106109f457805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe090920191602091820191016109b7565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610a51573d6000803e3d6000fd5b5050506040513d6020811015610a6657600080fd5b5051604080516020818101949094528082019290925280518083038201815260609092019081905281519192909182918401908083835b60208310610ada57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610a9d565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610b37573d6000803e3d6000fd5b5050506040513d6020811015610b4c57600080fd5b50516040805160208101858152929350600092600292839287928f928f92018383808284378083019250505093505050506040516020818303038152906040526040518082805190602001908083835b60208310610bd957805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610b9c565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610c36573d6000803e3d6000fd5b5050506040513d6020811015610c4b57600080fd5b50516040518651600291889160009188916020918201918291908601908083835b60208310610ca957805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610c6c565b6001836020036101000a0380198251168184511680821785525050505050509050018367ffffffffffffffff191667ffffffffffffffff1916815260180182815260200193505050506040516020818303038152906040526040518082805190602001908083835b60208310610d4e57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610d11565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610dab573d6000803e3d6000fd5b5050506040513d6020811015610dc057600080fd5b5051604080516020818101949094528082019290925280518083038201815260609092019081905281519192909182918401908083835b60208310610e3457805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610df7565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610e91573d6000803e3d6000fd5b5050506040513d6020811015610ea657600080fd5b50519050858114610f02576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260548152602001806117486054913960600191505060405180910390fd5b60205463ffffffff11610f60576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260218152602001806117276021913960400191505060405180910390fd5b602080546001019081905560005b60208110156110a9578160011660011415610fa0578260008260208110610f9157fe5b0155506110ac95505050505050565b600260008260208110610faf57fe5b01548460405160200180838152602001828152602001925050506040516020818303038152906040526040518082805190602001908083835b6020831061102557805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610fe8565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015611082573d6000803e3d6000fd5b5050506040513d602081101561109757600080fd5b50519250600282049150600101610f6e565b50fe5b50505050505050565b60606110c26020546114ba565b905090565b6020546000908190815b60208110156112f05781600116600114156111e6576002600082602081106110f557fe5b01548460405160200180838152602001828152602001925050506040516020818303038152906040526040518082805190602001908083835b6020831061116b57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0909201916020918201910161112e565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa1580156111c8573d6000803e3d6000fd5b5050506040513d60208110156111dd57600080fd5b505192506112e2565b600283602183602081106111f657fe5b015460405160200180838152602001828152602001925050506040516020818303038152906040526040518082805190602001908083835b6020831061126b57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0909201916020918201910161122e565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa1580156112c8573d6000803e3d6000fd5b5050506040513d60208110156112dd57600080fd5b505192505b6002820491506001016110d1565b506002826112ff6020546114ba565b600060401b6040516020018084815260200183805190602001908083835b6020831061135a57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0909201916020918201910161131d565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790527fffffffffffffffffffffffffffffffffffffffffffffffff000000000000000095909516920191825250604080518083037ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff8018152601890920190819052815191955093508392850191508083835b6020831061143f57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101611402565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa15801561149c573d6000803e3d6000fd5b5050506040513d60208110156114b157600080fd5b50519250505090565b60408051600880825281830190925260609160208201818036833701905050905060c082901b8060071a60f81b826000815181106114f457fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060061a60f81b8260018151811061153757fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060051a60f81b8260028151811061157a57fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060041a60f81b826003815181106115bd57fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060031a60f81b8260048151811061160057fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060021a60f81b8260058151811061164357fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060011a60f81b8260068151811061168657fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060001a60f81b826007815181106116c957fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a90535050919050565b6000808585111561170d578182fd5b83861115611719578182fd5b505082019391909203915056fe4465706f736974436f6e74726163743a206d65726b6c6520747265652066756c6c4465706f736974436f6e74726163743a207265636f6e7374727563746564204465706f7369744461746120646f6573206e6f74206d6174636820737570706c696564206465706f7369745f646174615f726f6f744465706f736974436f6e74726163743a20696e76616c6964207769746864726177616c5f63726564656e7469616c73206c656e6774684465706f736974436f6e74726163743a206465706f7369742076616c7565206e6f74206d756c7469706c65206f6620677765694465706f736974436f6e74726163743a20696e76616c6964207075626b6579206c656e6774684465706f736974436f6e74726163743a206465706f7369742076616c756520746f6f20686967684465706f736974436f6e74726163743a206465706f7369742076616c756520746f6f206c6f774465706f736974436f6e74726163743a20696e76616c6964207369676e6174757265206c656e677468a2646970667358221220dceca8706b29e917dacf25fceef95acac8d90d765ac926663ce4096195952b6164736f6c634300060b0033
INIT_CODE_BIN: 608060405234801561001057600080fd5b5060005b601f8110156101025760026021826020811061002c57fe5b01546021836020811061003b57fe5b015460405160200180838152602001828152602001925050506040516020818303038152906040526040518082805190602001908083835b602083106100925780518252601f199092019160209182019101610073565b51815160209384036101000a60001901801990921691161790526040519190930194509192505080830381855afa1580156100d1573d6000803e3d6000fd5b5050506040513d60208110156100e657600080fd5b5051602160018301602081106100f857fe5b0155600101610014565b506118d680620001136000396000f3fe60806040526004361061003f5760003560e01c806301ffc9a71461004457806322895118146100a4578063621fd130146101ba578063c5f2892f14610244575b600080fd5b34801561005057600080fd5b506100906004803603602081101561006757600080fd5b50357fffffffff000000000000000000000000000000000000000000000000000000001661026b565b604080519115158252519081900360200190f35b6101b8600480360360808110156100ba57600080fd5b8101906020810181356401000000008111156100d557600080fd5b8201836020820111156100e757600080fd5b8035906020019184600183028401116401000000008311171561010957600080fd5b91939092909160208101903564010000000081111561012757600080fd5b82018360208201111561013957600080fd5b8035906020019184600183028401116401000000008311171561015b57600080fd5b91939092909160208101903564010000000081111561017957600080fd5b82018360208201111561018b57600080fd5b803590602001918460018302840111640100000000831117156101ad57600080fd5b919350915035610304565b005b3480156101c657600080fd5b506101cf6110b5565b6040805160208082528351818301528351919283929083019185019080838360005b838110156102095781810151838201526020016101f1565b50505050905090810190601f1680156102365780820380516001836020036101000a031916815260200191505b509250505060405180910390f35b34801561025057600080fd5b506102596110c7565b60408051918252519081900360200190f35b60007fffffffff0000000000000000000000000000000000000000000000000000000082167f01ffc9a70000000000000000000000000000000000000000000000000000000014806102fe57507fffffffff0000000000000000000000000000000000000000000000000000000082167f8564090700000000000000000000000000000000000000000000000000000000145b92915050565b6030861461035d576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260268152602001806118056026913960400191505060405180910390fd5b602084146103b6576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252603681526020018061179c6036913960400191505060405180910390fd5b6060821461040f576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260298152602001806118786029913960400191505060405180910390fd5b670de0b6b3a7640000341015610470576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260268152602001806118526026913960400191505060405180910390fd5b633b9aca003406156104cd576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260338152602001806117d26033913960400191505060405180910390fd5b633b9aca00340467ffffffffffffffff811115610535576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252602781526020018061182b6027913960400191505060405180910390fd5b6060610540826114ba565b90507f649bbc62d0e31342afea4e5cd82d4049e7e1ee912fc0889aa790803be39038c589898989858a8a6105756020546114ba565b6040805160a0808252810189905290819060208201908201606083016080840160c085018e8e80828437600083820152601f017fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe01690910187810386528c815260200190508c8c808284376000838201819052601f9091017fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe01690920188810386528c5181528c51602091820193918e019250908190849084905b83811015610648578181015183820152602001610630565b50505050905090810190601f1680156106755780820380516001836020036101000a031916815260200191505b5086810383528881526020018989808284376000838201819052601f9091017fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0169092018881038452895181528951602091820193918b019250908190849084905b838110156106ef5781810151838201526020016106d7565b50505050905090810190601f16801561071c5780820380516001836020036101000a031916815260200191505b509d505050505050505050505050505060405180910390a1600060028a8a600060801b604051602001808484808284377fffffffffffffffffffffffffffffffff0000000000000000000000000000000090941691909301908152604080517ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0818403018152601090920190819052815191955093508392506020850191508083835b602083106107fc57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe090920191602091820191016107bf565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610859573d6000803e3d6000fd5b5050506040513d602081101561086e57600080fd5b5051905060006002806108846040848a8c6116fe565b6040516020018083838082843780830192505050925050506040516020818303038152906040526040518082805190602001908083835b602083106108f857805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe090920191602091820191016108bb565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610955573d6000803e3d6000fd5b5050506040513d602081101561096a57600080fd5b5051600261097b896040818d6116fe565b60405160009060200180848480828437919091019283525050604080518083038152602092830191829052805190945090925082918401908083835b602083106109f457805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe090920191602091820191016109b7565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610a51573d6000803e3d6000fd5b5050506040513d6020811015610a6657600080fd5b5051604080516020818101949094528082019290925280518083038201815260609092019081905281519192909182918401908083835b60208310610ada57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610a9d565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610b37573d6000803e3d6000fd5b5050506040513d6020811015610b4c57600080fd5b50516040805160208101858152929350600092600292839287928f928f92018383808284378083019250505093505050506040516020818303038152906040526040518082805190602001908083835b60208310610bd957805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610b9c565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610c36573d6000803e3d6000fd5b5050506040513d6020811015610c4b57600080fd5b50516040518651600291889160009188916020918201918291908601908083835b60208310610ca957805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610c6c565b6001836020036101000a0380198251168184511680821785525050505050509050018367ffffffffffffffff191667ffffffffffffffff1916815260180182815260200193505050506040516020818303038152906040526040518082805190602001908083835b60208310610d4e57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610d11565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610dab573d6000803e3d6000fd5b5050506040513d6020811015610dc057600080fd5b5051604080516020818101949094528082019290925280518083038201815260609092019081905281519192909182918401908083835b60208310610e3457805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610df7565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015610e91573d6000803e3d6000fd5b5050506040513d6020811015610ea657600080fd5b50519050858114610f02576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260548152602001806117486054913960600191505060405180910390fd5b60205463ffffffff11610f60576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260218152602001806117276021913960400191505060405180910390fd5b602080546001019081905560005b60208110156110a9578160011660011415610fa0578260008260208110610f9157fe5b0155506110ac95505050505050565b600260008260208110610faf57fe5b01548460405160200180838152602001828152602001925050506040516020818303038152906040526040518082805190602001908083835b6020831061102557805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101610fe8565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa158015611082573d6000803e3d6000fd5b5050506040513d602081101561109757600080fd5b50519250600282049150600101610f6e565b50fe5b50505050505050565b60606110c26020546114ba565b905090565b6020546000908190815b60208110156112f05781600116600114156111e6576002600082602081106110f557fe5b01548460405160200180838152602001828152602001925050506040516020818303038152906040526040518082805190602001908083835b6020831061116b57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0909201916020918201910161112e565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa1580156111c8573d6000803e3d6000fd5b5050506040513d60208110156111dd57600080fd5b505192506112e2565b600283602183602081106111f657fe5b015460405160200180838152602001828152602001925050506040516020818303038152906040526040518082805190602001908083835b6020831061126b57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0909201916020918201910161122e565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa1580156112c8573d6000803e3d6000fd5b5050506040513d60208110156112dd57600080fd5b505192505b6002820491506001016110d1565b506002826112ff6020546114ba565b600060401b6040516020018084815260200183805190602001908083835b6020831061135a57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0909201916020918201910161131d565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790527fffffffffffffffffffffffffffffffffffffffffffffffff000000000000000095909516920191825250604080518083037ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff8018152601890920190819052815191955093508392850191508083835b6020831061143f57805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09092019160209182019101611402565b51815160209384036101000a7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01801990921691161790526040519190930194509192505080830381855afa15801561149c573d6000803e3d6000fd5b5050506040513d60208110156114b157600080fd5b50519250505090565b60408051600880825281830190925260609160208201818036833701905050905060c082901b8060071a60f81b826000815181106114f457fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060061a60f81b8260018151811061153757fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060051a60f81b8260028151811061157a57fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060041a60f81b826003815181106115bd57fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060031a60f81b8260048151811061160057fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060021a60f81b8260058151811061164357fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060011a60f81b8260068151811061168657fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a9053508060001a60f81b826007815181106116c957fe5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a90535050919050565b6000808585111561170d578182fd5b83861115611719578182fd5b505082019391909203915056fe4465706f736974436f6e74726163743a206d65726b6c6520747265652066756c6c4465706f736974436f6e74726163743a207265636f6e7374727563746564204465706f7369744461746120646f6573206e6f74206d6174636820737570706c696564206465706f7369745f646174615f726f6f744465706f736974436f6e74726163743a20696e76616c6964207769746864726177616c5f63726564656e7469616c73206c656e6774684465706f736974436f6e74726163743a206465706f7369742076616c7565206e6f74206d756c7469706c65206f6620677765694465706f736974436f6e74726163743a20696e76616c6964207075626b6579206c656e6774684465706f736974436f6e74726163743a206465706f7369742076616c756520746f6f20686967684465706f736974436f6e74726163743a206465706f7369742076616c756520746f6f206c6f774465706f736974436f6e74726163743a20696e76616c6964207369676e6174757265206c656e677468a2646970667358221220dceca8706b29e917dacf25fceef95acac8d90d765ac926663ce4096195952b6164736f6c634300060b0033