Open enzoevers opened 1 year ago
KEVM-Foundry doesn't yet support automatically running the setUp
functions, so this test is actually expected to fail. You can see on the <k>
cell it is looking for a contract address that doesn't exist. We're working on this though. In the meantime, if you want to try out the proof you can move the setup code into the test, or call setUp
at the beginning of the test.
I expected it to be something with the creation of the Token contract indeed. Thanks for pointing this out. However, now it seems that the transaction went out of gas.
INFO 2023-02-22 13:40:38,359 pyk.ktool.kprove - Running: kprove out/specs/tokentest-testtransfer-spec.k --definition out/kompiled --spec-module TOKENTEST-TESTTRANSFER-SPEC --output json
[Error] Prover: backend terminated because the configuration cannot be
rewritten further. See output for more details.
INFO 2023-02-22 13:45:53,203 pyk.ktool.kprove - Timing [314.843]: kprove out/specs/tokentest-testtransfer-spec.k --definition out/kompiled --spec-module TOKENTEST-TESTTRANSFER-SPEC --output json
INFO 2023-02-22 13:45:53,203 pyk.ktool.kprove - Completed: kprove out/specs/tokentest-testtransfer-spec.k --definition out/kompiled --spec-module TOKENTEST-TESTTRANSFER-SPEC --output json
ERROR 2023-02-22 13:45:53,236 __main__ - Failed to prove claim: TokenTest-testTransfer
Result for TokenTest.testTransfer:
( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( #Ceil ( ( ( SetItem ( 1032069922050249630382865877677304880282300743300 ) -Set _TOUCHEDACCOUNTS_CELL:Set _TOUCHEDACCOUNTS_CELL:Set ) ) )
#And #Ceil ( ( ( SetItem ( 368263281805664599098893944405654396525700029268 ) SetItem ( 1032069922050249630382865877677304880282300743300 ) -Set _TOUCHEDACCOUNTS_CELL:Set ) ) ) ) )
#And #Ceil ( ( ( SetItem ( 368263281805664599098893944405654396525700029268 ) _TOUCHEDACCOUNTS_CELL:Set ) ) ) ) )
#And <generatedTop>
<foundry>
<kevm>
<k>
#halt
~> _CONTINUATION:K
</k>
<mode>
NORMAL
</mode>
<schedule>
LONDON
</schedule>
<ethereum>
<evm>
<output>
b""
</output>
<statusCode>
EVMC_OUT_OF_GAS
</statusCode>
<endPC>
316
</endPC>
<callStack>
.List
</callStack>
<touchedAccounts>
( ( ( ( SetItem ( 368263281805664599098893944405654396525700029268 ) SetItem ( 1032069922050249630382865877677304880282300743300 ) -Set _TOUCHEDACCOUNTS_CELL:Set ) ) _TOUCHEDACCOUNTS_CELL:Set ) )
</touchedAccounts>
<callState>
<program>
b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x00bW`\x005`\xe0\x1c\x80c\n\x92T\xe4\x14a\x00gW\x80c:v\x84c\x14a\x00qW\x80c\xbaAO\xa6\x14a\x00\xa9W\x80c\xdbg05\x14a\x00\xc1W\x80c\xf8\xcc\xbfG\x14a\x00\xd4W\x80c\xfav&\xd4\x14a\x00\xe7W[`\x00\x80\xfd[a\x00oa\x00\xf4V[\x00[a\x00\x8csq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[a\x00\xb1a\x02\x7fV[`@Q\x90\x15\x15\x81R` \x01a\x00\xa0V[a\x00oa\x00\xcf6`\x04a\n\xafV[a\x03\xaaV[`\x00Ta\x00\xb1\x90b\x01\x00\x00\x90\x04`\xff\x16\x81V[`\x00Ta\x00\xb1\x90`\xff\x16\x81V[`@Qa\x01\x00\x90a\n\x8bV[`@Q\x80\x91\x03\x90`\x00\xf0\x80\x15\x80\x15a\x01\x1cW=`\x00\x80>=`\x00\xfd[P`\x08\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x83\x16\x90\x81\x17\x90\x91U`\tT`@Qc@\xc1\x0f\x19`\xe0\x1b\x81R\x92\x16`\x04\x83\x01Rg\x8a\xc7#\x04\x89\xe8\x00\x00`$\x83\x01R\x90c@\xc1\x0f\x19\x90`D\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x01\x85W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x01\x99W=`\x00\x80>=`\x00\xfd[PP`\x08T`\nT`@Qc@\xc1\x0f\x19`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x91\x82\x16`\x04\x82\x01Rh\x01\x15\x8eF\t\x13\xd0\x00\x00`$\x82\x01R\x91\x16\x92Pc@\xc1\x0f\x19\x91P`D\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x01\xf5W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x02\tW=`\x00\x80>=`\x00\xfd[PP`\x08T`\x0bT`@Qc@\xc1\x0f\x19`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x91\x82\x16`\x04\x82\x01Rh\x01\xa0Ui\r\x9d\xb8\x00\x00`$\x82\x01R\x91\x16\x92Pc@\xc1\x0f\x19\x91P`D\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x02eW`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x02yW=`\x00\x80>=`\x00\xfd[PPPPV[`\x00\x80Ta\x01\x00\x90\x04`\xff\x16\x15a\x02\x9fWP`\x00Ta\x01\x00\x90\x04`\xff\x16\x90V[`\x00sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-;\x15a\x03\xa5W`@\x80Qsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-` \x82\x01\x81\x90Re\x19\x98Z[\x19Y`\xd2\x1b\x82\x84\x01R\x82Q\x80\x83\x03\x84\x01\x81R``\x83\x01\x90\x93R`\x00\x92\x90\x91a\x03-\x91\x7ff\x7f\x9dp\xcaA\x1dp\xea\xd5\r\x8d\\\"\x07\r\xaf\xc3j\xd7_=\xcf^r7\xb2*\xde\x9a\xec\xc4\x91`\x80\x01a\x0b\x1bV[`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\x03G\x91a\x0b?V[`\x00`@Q\x80\x83\x03\x81`\x00\x86Z\xf1\x91PP=\x80`\x00\x81\x14a\x03\x84W`@Q\x91P`\x1f\x19`?=\x01\x16\x82\x01`@R=\x82R=`\x00` \x84\x01>a\x03\x89V[``\x91P[P\x91PP\x80\x80` \x01\x90Q\x81\x01\x90a\x03\xa1\x91\x90a\x0bRV[\x91PP[\x91\x90PV[a\x03\xb2a\x00\xf4V[`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x85\x81\x16`\x04\x83\x01Rsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x92cLc\xe5b\x92\x85\x92\x90\x91\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x04\x1aW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x04>\x91\x90a\x0btV[`@Q`\x01`\x01`\xe0\x1b\x03\x19`\xe0\x85\x90\x1b\x16\x81R\x91\x11\x15`\x04\x82\x01R`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x04wW`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x04\x8bW=`\x00\x80>=`\x00\xfd[PP`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x87\x81\x16`\x04\x83\x01R`\x00\x94P\x90\x91\x16\x91Pcp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x04\xdcW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x05\x00\x91\x90a\x0btV[`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x86\x81\x16`\x04\x83\x01R\x92\x93P`\x00\x92\x90\x91\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x05PW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x05t\x91\x90a\x0btV[`@Qc\xcaf\x9f\xa7`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x87\x16`\x04\x82\x01R\x90\x91Psq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x90c\xcaf\x9f\xa7\x90`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x05\xccW`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x05\xe0W=`\x00\x80>=`\x00\xfd[PP`\x08T`@Qc\xa9\x05\x9c\xbb`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x88\x81\x16`\x04\x83\x01R`$\x82\x01\x88\x90R\x90\x91\x16\x92Pc\xa9\x05\x9c\xbb\x91P`D\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x062W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x06FW=`\x00\x80>=`\x00\xfd[PPPP\x83`\x01`\x01`\xa0\x1b\x03\x16\x85`\x01`\x01`\xa0\x1b\x03\x16\x03a\x07TW`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x87\x81\x16`\x04\x83\x01Ra\x06\xd9\x92\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x06\xafW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x06\xd3\x91\x90a\x0btV[\x83a\x08TV[`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x86\x81\x16`\x04\x83\x01Ra\x07O\x92\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x07%W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x07I\x91\x90a\x0btV[\x82a\x08TV[a\x08MV[`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x87\x81\x16`\x04\x83\x01Ra\x07\xd3\x92\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x07\xa0W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x07\xc4\x91\x90a\x0btV[a\x07\xce\x85\x85a\x0b\xa3V[a\x08TV[`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x86\x81\x16`\x04\x83\x01Ra\x08M\x92\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x08\x1fW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x08C\x91\x90a\x0btV[a\x07\xce\x85\x84a\x0b\xbcV[PPPPPV[\x80\x82\x14a\t{W\x7fA0O\xac\xd92=u\xb1\x1b\xcd\xd6\t\xcb8\xef\xff\xfd\xb0W\x10\xf7\xca\xf0\xe9\xb1lm\x9dp\x9fP`@Qa\x08\xc5\x90` \x80\x82R`\"\x90\x82\x01R\x7fError: a == b not satisfied [uin`@\x82\x01Rat]`\xf0\x1b``\x82\x01R`\x80\x01\x90V[`@Q\x80\x91\x03\x90\xa1`@\x80Q\x81\x81R`\n\x81\x83\x01Ri\x08\x08\x11^\x1c\x19X\xdd\x19Y`\xb2\x1b``\x82\x01R` \x81\x01\x83\x90R\x90Q\x7f\xb2\xde/\xbe\x80\x1a\r\xf6\xc0\xcb\xdd\xfdD\x8b\xa3\xc4\x1dH\xa0@\xca5\xc5l\x81\x96\xef\x0f\xca\xe7!\xa8\x91\x81\x90\x03`\x80\x01\x90\xa1`@\x80Q\x81\x81R`\n\x81\x83\x01Ri\x08\x08\x08\x08\x10X\xdd\x1dX[`\xb2\x1b``\x82\x01R` \x81\x01\x84\x90R\x90Q\x7f\xb2\xde/\xbe\x80\x1a\r\xf6\xc0\xcb\xdd\xfdD\x8b\xa3\xc4\x1dH\xa0@\xca5\xc5l\x81\x96\xef\x0f\xca\xe7!\xa8\x91\x81\x90\x03`\x80\x01\x90\xa1a\t{a\t\x7fV[PPV[sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-;\x15a\nzW`@\x80Qsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-` \x82\x01\x81\x90Re\x19\x98Z[\x19Y`\xd2\x1b\x92\x82\x01\x92\x90\x92R`\x01``\x82\x01R`\x00\x91\x90\x7fp\xca\x10\xbb\xd0\xdb\xfd\x90 \xa9\xf4\xb14\x02\xc1l\xb1 p^\r\x1c\n\xea\xb1\x0f\xa3S\xaeXo\xc4\x90`\x80\x01`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\n\x19\x92\x91` \x01a\x0b\x1bV[`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\n3\x91a\x0b?V[`\x00`@Q\x80\x83\x03\x81`\x00\x86Z\xf1\x91PP=\x80`\x00\x81\x14a\npW`@Q\x91P`\x1f\x19`?=\x01\x16\x82\x01`@R=\x82R=`\x00` \x84\x01>a\nuV[``\x91P[PPPP[`\x00\x80Ta\xff\x00\x19\x16a\x01\x00\x17\x90UV[a\x02\x9e\x80a\x0b\xd0\x839\x01\x90V[\x805`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x03\xa5W`\x00\x80\xfd[`\x00\x80`\x00``\x84\x86\x03\x12\x15a\n\xc4W`\x00\x80\xfd[a\n\xcd\x84a\n\x98V[\x92Pa\n\xdb` \x85\x01a\n\x98V[\x91P`@\x84\x015\x90P\x92P\x92P\x92V[`\x00\x81Q`\x00[\x81\x81\x10\x15a\x0b\fW` \x81\x85\x01\x81\x01Q\x86\x83\x01R\x01a\n\xf2V[P`\x00\x93\x01\x92\x83RP\x90\x91\x90PV[`\x01`\x01`\xe0\x1b\x03\x19\x83\x16\x81R`\x00a\x0b7`\x04\x83\x01\x84a\n\xebV[\x94\x93PPPPV[`\x00a\x0bK\x82\x84a\n\xebV[\x93\x92PPPV[`\x00` \x82\x84\x03\x12\x15a\x0bdW`\x00\x80\xfd[\x81Q\x80\x15\x15\x81\x14a\x0bKW`\x00\x80\xfd[`\x00` \x82\x84\x03\x12\x15a\x0b\x86W`\x00\x80\xfd[PQ\x91\x90PV[cNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[\x81\x81\x03\x81\x81\x11\x15a\x0b\xb6Wa\x0b\xb6a\x0b\x8dV[\x92\x91PPV[\x80\x82\x01\x80\x82\x11\x15a\x0b\xb6Wa\x0b\xb6a\x0b\x8dV\xfe`\xa0`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P3`\x80R`\x80Qa\x02oa\x00/`\x009`\x00`\xab\x01Ra\x02o`\x00\xf3\xfe`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x00AW`\x005`\xe0\x1c\x80c@\xc1\x0f\x19\x14a\x00FW\x80cp\xa0\x821\x14a\x00[W\x80c\xa9\x05\x9c\xbb\x14a\x00\x8dW[`\x00\x80\xfd[a\x00Ya\x00T6`\x04a\x01\xabV[a\x00\xa0V[\x00[a\x00{a\x00i6`\x04a\x01\xd5V[`\x00` \x81\x90R\x90\x81R`@\x90 T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[a\x00Ya\x00\x9b6`\x04a\x01\xabV[a\x01CV[3`\x01`\x01`\xa0\x1b\x03\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16\x14a\x01\x12W`@QbF\x1b\xcd`\xe5\x1b\x81R` `\x04\x82\x01R`\x13`$\x82\x01Rr\x13\xdb\x9b\x1eH\x1b\xdd\xdb\x99\\\x88\x18\xd8[\x88\x1bZ[\x9d`j\x1b`D\x82\x01R`d\x01`@Q\x80\x91\x03\x90\xfd[`\x01`\x01`\xa0\x1b\x03\x82\x16`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01:\x90\x84\x90a\x02\rV[\x90\x91UPPPPV[3`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01b\x90\x84\x90a\x02&V[\x90\x91UPP`\x01`\x01`\xa0\x1b\x03\x82\x16`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01:\x90\x84\x90a\x02\rV[\x805`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\xa6W`\x00\x80\xfd[\x91\x90PV[`\x00\x80`@\x83\x85\x03\x12\x15a\x01\xbeW`\x00\x80\xfd[a\x01\xc7\x83a\x01\x8fV[\x94` \x93\x90\x93\x015\x93PPPV[`\x00` \x82\x84\x03\x12\x15a\x01\xe7W`\x00\x80\xfd[a\x01\xf0\x82a\x01\x8fV[\x93\x92PPPV[cNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[\x80\x82\x01\x80\x82\x11\x15a\x02 Wa\x02 a\x01\xf7V[\x92\x91PPV[\x81\x81\x03\x81\x81\x11\x15a\x02 Wa\x02 a\x01\xf7V\xfe\xa2dipfsX\"\x12 \x12\xa7\xee\x81\x95r\x8a\xce4\x9c\xde\xc9\f\x1f\xe0'\x80n*uLb\xd7\x12\x8b\x07\xe01\\\xe7\x84\xf4dsolcC\x00\x08\x11\x003\xa2dipfsX\"\x12 \xee\xcd\x9c\x18\xdd;BG\xedVh\xbe\xa0\xda\x93\xc8\x890\xa2RT\xf5\x9e~-\xf0Crr\xd4\\KdsolcC\x00\x08\x11\x003"
</program>
<jumpDests>
( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( SetItem ( 16 ) SetItem ( 98 ) ) ) SetItem ( 103 ) ) ) SetItem ( 111 ) ) ) SetItem ( 113 ) ) ) SetItem ( 140 ) ) ) SetItem ( 160 ) ) ) SetItem ( 169 ) ) ) SetItem ( 177 ) ) ) SetItem ( 193 ) ) ) SetItem ( 207 ) ) ) SetItem ( 212 ) ) ) SetItem ( 231 ) ) ) SetItem ( 244 ) ) ) SetItem ( 284 ) ) ) SetItem ( 389 ) ) ) SetItem ( 409 ) ) ) SetItem ( 501 ) ) ) SetItem ( 521 ) ) ) SetItem ( 613 ) ) ) SetItem ( 633 ) ) ) SetItem ( 639 ) ) ) SetItem ( 671 ) ) ) SetItem ( 813 ) ) ) SetItem ( 839 ) ) ) SetItem ( 900 ) ) ) SetItem ( 905 ) ) ) SetItem ( 929 ) ) ) SetItem ( 933 ) ) ) SetItem ( 938 ) ) ) SetItem ( 946 ) ) ) SetItem ( 1050 ) ) ) SetItem ( 1086 ) ) ) SetItem ( 1143 ) ) ) SetItem ( 1163 ) ) ) SetItem ( 1244 ) ) ) SetItem ( 1280 ) ) ) SetItem ( 1360 ) ) ) SetItem ( 1396 ) ) ) SetItem ( 1484 ) ) ) SetItem ( 1504 ) ) ) SetItem ( 1586 ) ) ) SetItem ( 1606 ) ) ) SetItem ( 1711 ) ) ) SetItem ( 1747 ) ) ) SetItem ( 1753 ) ) ) SetItem ( 1829 ) ) ) SetItem ( 1865 ) ) ) SetItem ( 1871 ) ) ) SetItem ( 1876 ) ) ) SetItem ( 1952 ) ) ) SetItem ( 1988 ) ) ) SetItem ( 1998 ) ) ) SetItem ( 2003 ) ) ) SetItem ( 2079 ) ) ) SetItem ( 2115 ) ) ) SetItem ( 2125 ) ) ) SetItem ( 2132 ) ) ) SetItem ( 2245 ) ) ) SetItem ( 2427 ) ) ) SetItem ( 2431 ) ) ) SetItem ( 2585 ) ) ) SetItem ( 2611 ) ) ) SetItem ( 2672 ) ) ) SetItem ( 2677 ) ) ) SetItem ( 2682 ) ) ) SetItem ( 2699 ) ) ) SetItem ( 2712 ) ) ) SetItem ( 2735 ) ) ) SetItem ( 2756 ) ) ) SetItem ( 2765 ) ) ) SetItem ( 2779 ) ) ) SetItem ( 2795 ) ) ) SetItem ( 2802 ) ) ) SetItem ( 2828 ) ) ) SetItem ( 2843 ) ) ) SetItem ( 2871 ) ) ) SetItem ( 2879 ) ) ) SetItem ( 2891 ) ) ) SetItem ( 2898 ) ) ) SetItem ( 2916 ) ) ) SetItem ( 2932 ) ) ) SetItem ( 2950 ) ) ) SetItem ( 2957 ) ) ) SetItem ( 2979 ) ) ) SetItem ( 2998 ) ) ) SetItem ( 3004 ) ) ) SetItem ( 3040 ) ) ) SetItem ( 3087 ) ) ) SetItem ( 3136 ) ) ) SetItem ( 3141 ) ) ) SetItem ( 3155 ) ) ) SetItem ( 3160 ) ) ) SetItem ( 3162 ) ) ) SetItem ( 3176 ) ) ) SetItem ( 3194 ) ) ) SetItem ( 3212 ) ) ) SetItem ( 3226 ) ) ) SetItem ( 3231 ) ) ) SetItem ( 3345 ) ) ) SetItem ( 3385 ) ) ) SetItem ( 3394 ) ) ) SetItem ( 3425 ) ) ) SetItem ( 3470 ) ) ) SetItem ( 3493 ) ) ) SetItem ( 3498 ) ) ) SetItem ( 3517 ) ) ) SetItem ( 3526 ) ) ) SetItem ( 3540 ) ) ) SetItem ( 3558 ) ) ) SetItem ( 3567 ) ) ) SetItem ( 3574 ) ) ) SetItem ( 3596 ) ) ) SetItem ( 3615 ) ) ) SetItem ( 3621 ) ) ) SetItem ( 256 ) ) )
</jumpDests>
<id>
1032069922050249630382865877677304880282300743300
</id>
<callData>
b"\xdbg05" ++ #buf ( 32 , _VV0_from_3c5818c8:Int ) ++ #buf ( 32 , _VV1_to_3c5818c8:Int ) ++ #buf ( 32 , _VV2_amount_3c5818c8:Int )
</callData>
<callValue>
0
</callValue>
<wordStack>
368263281805664599098893944405654396525700029268 : 1461501637330902918203684832716283019655932542975 : 946 : _VV2_amount_3c5818c8:Int : _VV1_to_3c5818c8:Int : _VV0_from_3c5818c8:Int : 111 : 3680972853 : .WordStack
</wordStack>
<localMem>
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\xa0`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P3`\x80R`\x80Qa\x02oa\x00/`\x009`\x00`\xab\x01Ra\x02o`\x00\xf3\xfe`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x00AW`\x005`\xe0\x1c\x80c@\xc1\x0f\x19\x14a\x00FW\x80cp\xa0\x821\x14a\x00[W\x80c\xa9\x05\x9c\xbb\x14a\x00\x8dW[`\x00\x80\xfd[a\x00Ya\x00T6`\x04a\x01\xabV[a\x00\xa0V[\x00[a\x00{a\x00i6`\x04a\x01\xd5V[`\x00` \x81\x90R\x90\x81R`@\x90 T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[a\x00Ya\x00\x9b6`\x04a\x01\xabV[a\x01CV[3`\x01`\x01`\xa0\x1b\x03\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16\x14a\x01\x12W`@QbF\x1b\xcd`\xe5\x1b\x81R` `\x04\x82\x01R`\x13`$\x82\x01Rr\x13\xdb\x9b\x1eH\x1b\xdd\xdb\x99\\\x88\x18\xd8[\x88\x1bZ[\x9d`j\x1b`D\x82\x01R`d\x01`@Q\x80\x91\x03\x90\xfd[`\x01`\x01`\xa0\x1b\x03\x82\x16`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01:\x90\x84\x90a\x02\rV[\x90\x91UPPPPV[3`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01b\x90\x84\x90a\x02&V[\x90\x91UPP`\x01`\x01`\xa0\x1b\x03\x82\x16`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01:\x90\x84\x90a\x02\rV[\x805`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\xa6W`\x00\x80\xfd[\x91\x90PV[`\x00\x80`@\x83\x85\x03\x12\x15a\x01\xbeW`\x00\x80\xfd[a\x01\xc7\x83a\x01\x8fV[\x94` \x93\x90\x93\x015\x93PPPV[`\x00` \x82\x84\x03\x12\x15a\x01\xe7W`\x00\x80\xfd[a\x01\xf0\x82a\x01\x8fV[\x93\x92PPPV[cNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[\x80\x82\x01\x80\x82\x11\x15a\x02 Wa\x02 a\x01\xf7V[\x92\x91PPV[\x81\x81\x03\x81\x81\x11\x15a\x02 Wa\x02 a\x01\xf7V\xfe\xa2dipfsX\"\x12 \x12\xa7\xee\x81\x95r\x8a\xce4\x9c\xde\xc9\f\x1f\xe0'\x80n*uLb\xd7\x12\x8b\x07\xe01\\\xe7\x84\xf4dsolcC\x00\x08\x11\x003"
</localMem>
<pc>
316
</pc>
<gas>
9223372036854616137
</gas>
<memoryUsed>
25
</memoryUsed>
<callGas>
9079256848778887767
</callGas>
<static>
false
</static>
<callDepth>
0
</callDepth>
...
</callState>
<substate>
<refund>
( ( _REFUND_CELL:Int +Int Rsstore ( LONDON , 368263281805664599098893944405654396525700029268 |Int 115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int #lookup ( _ACCT_STORAGE:Map , 8 ) , #lookup ( _ACCT_STORAGE:Map , 8 ) , #lookup ( _DotVar3:Map , 8 ) ) ) )
</refund>
<accessedAccounts>
( ( SetItem ( 368263281805664599098893944405654396525700029268 ) SetItem ( 1032069922050249630382865877677304880282300743300 ) ) )
</accessedAccounts>
<accessedStorage>
( ( 1032069922050249630382865877677304880282300743300 |-> SetItem ( 8 ) ) )
</accessedStorage>
...
</substate>
...
</evm>
<network>
<activeAccounts>
( ( ( ( ( ( ( ( SetItem ( 120209876281281145568259943 ) SetItem ( 137122462167341575662000267002353578582749290296 ) ) ) SetItem ( 368263281805664599098893944405654396525700029268 ) ) ) SetItem ( 645326474426547203313410069153905908525362434349 ) ) ) SetItem ( 1032069922050249630382865877677304880282300743300 ) ) )
</activeAccounts>
<accounts>
( ( ( ( ( <account>
<acctID>
120209876281281145568259943
</acctID>
<balance>
0
</balance>
<code>
b""
</code>
<storage>
.Map
</storage>
<origStorage>
.Map
</origStorage>
<nonce>
0
</nonce>
</account>
<account>
<acctID>
137122462167341575662000267002353578582749290296
</acctID>
<balance>
0
</balance>
<code>
b""
</code>
<storage>
.Map
</storage>
<origStorage>
.Map
</origStorage>
<nonce>
0
</nonce>
</account> )
<account>
<acctID>
368263281805664599098893944405654396525700029268
</acctID>
<balance>
0
</balance>
<code>
b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x00AW`\x005`\xe0\x1c\x80c@\xc1\x0f\x19\x14a\x00FW\x80cp\xa0\x821\x14a\x00[W\x80c\xa9\x05\x9c\xbb\x14a\x00\x8dW[`\x00\x80\xfd[a\x00Ya\x00T6`\x04a\x01\xabV[a\x00\xa0V[\x00[a\x00{a\x00i6`\x04a\x01\xd5V[`\x00` \x81\x90R\x90\x81R`@\x90 T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[a\x00Ya\x00\x9b6`\x04a\x01\xabV[a\x01CV[3`\x01`\x01`\xa0\x1b\x03\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xb4\xc7\x9d\xab\x8f%\x9cz\xeen[*\xa7)\x82\x18d\"~\x84\x16\x14a\x01\x12W`@QbF\x1b\xcd`\xe5\x1b\x81R` `\x04\x82\x01R`\x13`$\x82\x01Rr\x13\xdb\x9b\x1eH\x1b\xdd\xdb\x99\\\x88\x18\xd8[\x88\x1bZ[\x9d`j\x1b`D\x82\x01R`d\x01`@Q\x80\x91\x03\x90\xfd[`\x01`\x01`\xa0\x1b\x03\x82\x16`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01:\x90\x84\x90a\x02\rV[\x90\x91UPPPPV[3`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01b\x90\x84\x90a\x02&V[\x90\x91UPP`\x01`\x01`\xa0\x1b\x03\x82\x16`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01:\x90\x84\x90a\x02\rV[\x805`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\xa6W`\x00\x80\xfd[\x91\x90PV[`\x00\x80`@\x83\x85\x03\x12\x15a\x01\xbeW`\x00\x80\xfd[a\x01\xc7\x83a\x01\x8fV[\x94` \x93\x90\x93\x015\x93PPPV[`\x00` \x82\x84\x03\x12\x15a\x01\xe7W`\x00\x80\xfd[a\x01\xf0\x82a\x01\x8fV[\x93\x92PPPV[cNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[\x80\x82\x01\x80\x82\x11\x15a\x02 Wa\x02 a\x01\xf7V[\x92\x91PPV[\x81\x81\x03\x81\x81\x11\x15a\x02 Wa\x02 a\x01\xf7V\xfe\xa2dipfsX\"\x12 \x12\xa7\xee\x81\x95r\x8a\xce4\x9c\xde\xc9\f\x1f\xe0'\x80n*uLb\xd7\x12\x8b\x07\xe01\\\xe7\x84\xf4dsolcC\x00\x08\x11\x003"
</code>
<storage>
.Map
</storage>
<origStorage>
.Map
</origStorage>
<nonce>
1
</nonce>
</account> )
<account>
<acctID>
645326474426547203313410069153905908525362434349
</acctID>
<balance>
0
</balance>
<code>
b"\x00"
</code>
<storage>
CHEATCODE_STORAGE:Map
</storage>
<origStorage>
.Map
</origStorage>
<nonce>
0
</nonce>
</account> )
<account>
<acctID>
1032069922050249630382865877677304880282300743300
</acctID>
<balance>
0
</balance>
<code>
b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x00bW`\x005`\xe0\x1c\x80c\n\x92T\xe4\x14a\x00gW\x80c:v\x84c\x14a\x00qW\x80c\xbaAO\xa6\x14a\x00\xa9W\x80c\xdbg05\x14a\x00\xc1W\x80c\xf8\xcc\xbfG\x14a\x00\xd4W\x80c\xfav&\xd4\x14a\x00\xe7W[`\x00\x80\xfd[a\x00oa\x00\xf4V[\x00[a\x00\x8csq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[a\x00\xb1a\x02\x7fV[`@Q\x90\x15\x15\x81R` \x01a\x00\xa0V[a\x00oa\x00\xcf6`\x04a\n\xafV[a\x03\xaaV[`\x00Ta\x00\xb1\x90b\x01\x00\x00\x90\x04`\xff\x16\x81V[`\x00Ta\x00\xb1\x90`\xff\x16\x81V[`@Qa\x01\x00\x90a\n\x8bV[`@Q\x80\x91\x03\x90`\x00\xf0\x80\x15\x80\x15a\x01\x1cW=`\x00\x80>=`\x00\xfd[P`\x08\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x83\x16\x90\x81\x17\x90\x91U`\tT`@Qc@\xc1\x0f\x19`\xe0\x1b\x81R\x92\x16`\x04\x83\x01Rg\x8a\xc7#\x04\x89\xe8\x00\x00`$\x83\x01R\x90c@\xc1\x0f\x19\x90`D\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x01\x85W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x01\x99W=`\x00\x80>=`\x00\xfd[PP`\x08T`\nT`@Qc@\xc1\x0f\x19`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x91\x82\x16`\x04\x82\x01Rh\x01\x15\x8eF\t\x13\xd0\x00\x00`$\x82\x01R\x91\x16\x92Pc@\xc1\x0f\x19\x91P`D\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x01\xf5W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x02\tW=`\x00\x80>=`\x00\xfd[PP`\x08T`\x0bT`@Qc@\xc1\x0f\x19`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x91\x82\x16`\x04\x82\x01Rh\x01\xa0Ui\r\x9d\xb8\x00\x00`$\x82\x01R\x91\x16\x92Pc@\xc1\x0f\x19\x91P`D\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x02eW`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x02yW=`\x00\x80>=`\x00\xfd[PPPPV[`\x00\x80Ta\x01\x00\x90\x04`\xff\x16\x15a\x02\x9fWP`\x00Ta\x01\x00\x90\x04`\xff\x16\x90V[`\x00sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-;\x15a\x03\xa5W`@\x80Qsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-` \x82\x01\x81\x90Re\x19\x98Z[\x19Y`\xd2\x1b\x82\x84\x01R\x82Q\x80\x83\x03\x84\x01\x81R``\x83\x01\x90\x93R`\x00\x92\x90\x91a\x03-\x91\x7ff\x7f\x9dp\xcaA\x1dp\xea\xd5\r\x8d\\\"\x07\r\xaf\xc3j\xd7_=\xcf^r7\xb2*\xde\x9a\xec\xc4\x91`\x80\x01a\x0b\x1bV[`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\x03G\x91a\x0b?V[`\x00`@Q\x80\x83\x03\x81`\x00\x86Z\xf1\x91PP=\x80`\x00\x81\x14a\x03\x84W`@Q\x91P`\x1f\x19`?=\x01\x16\x82\x01`@R=\x82R=`\x00` \x84\x01>a\x03\x89V[``\x91P[P\x91PP\x80\x80` \x01\x90Q\x81\x01\x90a\x03\xa1\x91\x90a\x0bRV[\x91PP[\x91\x90PV[a\x03\xb2a\x00\xf4V[`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x85\x81\x16`\x04\x83\x01Rsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x92cLc\xe5b\x92\x85\x92\x90\x91\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x04\x1aW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x04>\x91\x90a\x0btV[`@Q`\x01`\x01`\xe0\x1b\x03\x19`\xe0\x85\x90\x1b\x16\x81R\x91\x11\x15`\x04\x82\x01R`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x04wW`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x04\x8bW=`\x00\x80>=`\x00\xfd[PP`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x87\x81\x16`\x04\x83\x01R`\x00\x94P\x90\x91\x16\x91Pcp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x04\xdcW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x05\x00\x91\x90a\x0btV[`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x86\x81\x16`\x04\x83\x01R\x92\x93P`\x00\x92\x90\x91\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x05PW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x05t\x91\x90a\x0btV[`@Qc\xcaf\x9f\xa7`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x87\x16`\x04\x82\x01R\x90\x91Psq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x90c\xcaf\x9f\xa7\x90`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x05\xccW`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x05\xe0W=`\x00\x80>=`\x00\xfd[PP`\x08T`@Qc\xa9\x05\x9c\xbb`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x88\x81\x16`\x04\x83\x01R`$\x82\x01\x88\x90R\x90\x91\x16\x92Pc\xa9\x05\x9c\xbb\x91P`D\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x062W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x06FW=`\x00\x80>=`\x00\xfd[PPPP\x83`\x01`\x01`\xa0\x1b\x03\x16\x85`\x01`\x01`\xa0\x1b\x03\x16\x03a\x07TW`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x87\x81\x16`\x04\x83\x01Ra\x06\xd9\x92\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x06\xafW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x06\xd3\x91\x90a\x0btV[\x83a\x08TV[`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x86\x81\x16`\x04\x83\x01Ra\x07O\x92\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x07%W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x07I\x91\x90a\x0btV[\x82a\x08TV[a\x08MV[`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x87\x81\x16`\x04\x83\x01Ra\x07\xd3\x92\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x07\xa0W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x07\xc4\x91\x90a\x0btV[a\x07\xce\x85\x85a\x0b\xa3V[a\x08TV[`\x08T`@Qcp\xa0\x821`\xe0\x1b\x81R`\x01`\x01`\xa0\x1b\x03\x86\x81\x16`\x04\x83\x01Ra\x08M\x92\x16\x90cp\xa0\x821\x90`$\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x08\x1fW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x08C\x91\x90a\x0btV[a\x07\xce\x85\x84a\x0b\xbcV[PPPPPV[\x80\x82\x14a\t{W\x7fA0O\xac\xd92=u\xb1\x1b\xcd\xd6\t\xcb8\xef\xff\xfd\xb0W\x10\xf7\xca\xf0\xe9\xb1lm\x9dp\x9fP`@Qa\x08\xc5\x90` \x80\x82R`\"\x90\x82\x01R\x7fError: a == b not satisfied [uin`@\x82\x01Rat]`\xf0\x1b``\x82\x01R`\x80\x01\x90V[`@Q\x80\x91\x03\x90\xa1`@\x80Q\x81\x81R`\n\x81\x83\x01Ri\x08\x08\x11^\x1c\x19X\xdd\x19Y`\xb2\x1b``\x82\x01R` \x81\x01\x83\x90R\x90Q\x7f\xb2\xde/\xbe\x80\x1a\r\xf6\xc0\xcb\xdd\xfdD\x8b\xa3\xc4\x1dH\xa0@\xca5\xc5l\x81\x96\xef\x0f\xca\xe7!\xa8\x91\x81\x90\x03`\x80\x01\x90\xa1`@\x80Q\x81\x81R`\n\x81\x83\x01Ri\x08\x08\x08\x08\x10X\xdd\x1dX[`\xb2\x1b``\x82\x01R` \x81\x01\x84\x90R\x90Q\x7f\xb2\xde/\xbe\x80\x1a\r\xf6\xc0\xcb\xdd\xfdD\x8b\xa3\xc4\x1dH\xa0@\xca5\xc5l\x81\x96\xef\x0f\xca\xe7!\xa8\x91\x81\x90\x03`\x80\x01\x90\xa1a\t{a\t\x7fV[PPV[sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-;\x15a\nzW`@\x80Qsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-` \x82\x01\x81\x90Re\x19\x98Z[\x19Y`\xd2\x1b\x92\x82\x01\x92\x90\x92R`\x01``\x82\x01R`\x00\x91\x90\x7fp\xca\x10\xbb\xd0\xdb\xfd\x90 \xa9\xf4\xb14\x02\xc1l\xb1 p^\r\x1c\n\xea\xb1\x0f\xa3S\xaeXo\xc4\x90`\x80\x01`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\n\x19\x92\x91` \x01a\x0b\x1bV[`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\n3\x91a\x0b?V[`\x00`@Q\x80\x83\x03\x81`\x00\x86Z\xf1\x91PP=\x80`\x00\x81\x14a\npW`@Q\x91P`\x1f\x19`?=\x01\x16\x82\x01`@R=\x82R=`\x00` \x84\x01>a\nuV[``\x91P[PPPP[`\x00\x80Ta\xff\x00\x19\x16a\x01\x00\x17\x90UV[a\x02\x9e\x80a\x0b\xd0\x839\x01\x90V[\x805`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x03\xa5W`\x00\x80\xfd[`\x00\x80`\x00``\x84\x86\x03\x12\x15a\n\xc4W`\x00\x80\xfd[a\n\xcd\x84a\n\x98V[\x92Pa\n\xdb` \x85\x01a\n\x98V[\x91P`@\x84\x015\x90P\x92P\x92P\x92V[`\x00\x81Q`\x00[\x81\x81\x10\x15a\x0b\fW` \x81\x85\x01\x81\x01Q\x86\x83\x01R\x01a\n\xf2V[P`\x00\x93\x01\x92\x83RP\x90\x91\x90PV[`\x01`\x01`\xe0\x1b\x03\x19\x83\x16\x81R`\x00a\x0b7`\x04\x83\x01\x84a\n\xebV[\x94\x93PPPPV[`\x00a\x0bK\x82\x84a\n\xebV[\x93\x92PPPV[`\x00` \x82\x84\x03\x12\x15a\x0bdW`\x00\x80\xfd[\x81Q\x80\x15\x15\x81\x14a\x0bKW`\x00\x80\xfd[`\x00` \x82\x84\x03\x12\x15a\x0b\x86W`\x00\x80\xfd[PQ\x91\x90PV[cNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[\x81\x81\x03\x81\x81\x11\x15a\x0b\xb6Wa\x0b\xb6a\x0b\x8dV[\x92\x91PPV[\x80\x82\x01\x80\x82\x11\x15a\x0b\xb6Wa\x0b\xb6a\x0b\x8dV\xfe`\xa0`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P3`\x80R`\x80Qa\x02oa\x00/`\x009`\x00`\xab\x01Ra\x02o`\x00\xf3\xfe`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x00AW`\x005`\xe0\x1c\x80c@\xc1\x0f\x19\x14a\x00FW\x80cp\xa0\x821\x14a\x00[W\x80c\xa9\x05\x9c\xbb\x14a\x00\x8dW[`\x00\x80\xfd[a\x00Ya\x00T6`\x04a\x01\xabV[a\x00\xa0V[\x00[a\x00{a\x00i6`\x04a\x01\xd5V[`\x00` \x81\x90R\x90\x81R`@\x90 T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[a\x00Ya\x00\x9b6`\x04a\x01\xabV[a\x01CV[3`\x01`\x01`\xa0\x1b\x03\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16\x14a\x01\x12W`@QbF\x1b\xcd`\xe5\x1b\x81R` `\x04\x82\x01R`\x13`$\x82\x01Rr\x13\xdb\x9b\x1eH\x1b\xdd\xdb\x99\\\x88\x18\xd8[\x88\x1bZ[\x9d`j\x1b`D\x82\x01R`d\x01`@Q\x80\x91\x03\x90\xfd[`\x01`\x01`\xa0\x1b\x03\x82\x16`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01:\x90\x84\x90a\x02\rV[\x90\x91UPPPPV[3`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01b\x90\x84\x90a\x02&V[\x90\x91UPP`\x01`\x01`\xa0\x1b\x03\x82\x16`\x00\x90\x81R` \x81\x90R`@\x81 \x80T\x83\x92\x90a\x01:\x90\x84\x90a\x02\rV[\x805`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\xa6W`\x00\x80\xfd[\x91\x90PV[`\x00\x80`@\x83\x85\x03\x12\x15a\x01\xbeW`\x00\x80\xfd[a\x01\xc7\x83a\x01\x8fV[\x94` \x93\x90\x93\x015\x93PPPV[`\x00` \x82\x84\x03\x12\x15a\x01\xe7W`\x00\x80\xfd[a\x01\xf0\x82a\x01\x8fV[\x93\x92PPPV[cNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[\x80\x82\x01\x80\x82\x11\x15a\x02 Wa\x02 a\x01\xf7V[\x92\x91PPV[\x81\x81\x03\x81\x81\x11\x15a\x02 Wa\x02 a\x01\xf7V\xfe\xa2dipfsX\"\x12 \x12\xa7\xee\x81\x95r\x8a\xce4\x9c\xde\xc9\f\x1f\xe0'\x80n*uLb\xd7\x12\x8b\x07\xe01\\\xe7\x84\xf4dsolcC\x00\x08\x11\x003\xa2dipfsX\"\x12 \xee\xcd\x9c\x18\xdd;BG\xedVh\xbe\xa0\xda\x93\xc8\x890\xa2RT\xf5\x9e~-\xf0Crr\xd4\\KdsolcC\x00\x08\x11\x003"
</code>
<storage>
_ACCT_STORAGE:Map
</storage>
<origStorage>
_DotVar3:Map
</origStorage>
<nonce>
1
</nonce>
</account> )
_ACCOUNTS_INIT:AccountCellMap )
</accounts>
...
</network>
</ethereum>
...
</kevm>
...
</foundry>
...
</generatedTop> ) )
#And { 0 #Equals #lookup ( CHEATCODE_STORAGE:Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) } ) )
#And { false #Equals <acctID>
120209876281281145568259943
</acctID> in_keys ( _ACCOUNTS_INIT:AccountCellMap ) } ) )
#And { false #Equals <acctID>
137122462167341575662000267002353578582749290296
</acctID> in_keys ( _ACCOUNTS_INIT:AccountCellMap ) } ) )
#And { false #Equals <acctID>
368263281805664599098893944405654396525700029268
</acctID> in_keys ( _ACCOUNTS_INIT:AccountCellMap ) } ) )
#And { false #Equals <acctID>
645326474426547203313410069153905908525362434349
</acctID> in_keys ( _ACCOUNTS_INIT:AccountCellMap ) } ) )
#And { false #Equals <acctID>
1032069922050249630382865877677304880282300743300
</acctID> in_keys ( _ACCOUNTS_INIT:AccountCellMap ) } ) )
#And { true #Equals 0 <=Int _VV0_from_3c5818c8:Int } ) )
#And { true #Equals 0 <=Int _VV1_to_3c5818c8:Int } ) )
#And { true #Equals 0 <=Int _VV2_amount_3c5818c8:Int } ) )
#And { true #Equals 9223372036854616137 <Int Csstore ( LONDON , 368263281805664599098893944405654396525700029268 |Int 115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int #lookup ( _ACCT_STORAGE:Map , 8 ) , #lookup ( _ACCT_STORAGE:Map , 8 ) , #lookup ( _DotVar3:Map , 8 ) ) } ) )
#And { true #Equals _VV0_from_3c5818c8:Int <Int 1461501637330902918203684832716283019655932542976 } ) )
#And { true #Equals _VV1_to_3c5818c8:Int <Int 1461501637330902918203684832716283019655932542976 } ) )
#And { true #Equals _VV2_amount_3c5818c8:Int <Int 115792089237316195423570985008687907853269984665640564039457584007913129639936 } ) )
Failed to prove KCFGs: ['TokenTest.testTransfer']
5m22.653s 5m36.033s 0m14.021s python3 -m kevm_pyk foundry-prove out --profile --test TokenTest.testTransfer --definition /root/evm-semantics/.build/usr/lib/kevm/foundry -I /root/evm-semantics/.build/usr/lib/kevm/include/kframework -I /root/evm-semantics/.build/usr/lib/kevm/blockchain-k-plugin/include/kframework --verbose
So it seems that the generated gas amount is too little:
Default gas amount in ./foundry-demo/out/specs/tokentest-testtransfer-spec.k
...
<gas>
( 9223372036854775807 => ?_GAS_CELL_c89e25d9 )
</gas>
...
Changing this to:
<gas>
( 20000000000000000000 => ?_GAS_CELL_c89e25d9 )
</gas>
Now running kprove
results in the output below. It seems that the new gas amount was sufficient now? So it seems that the generated gas amount is not always sufficient.
$ kprove out/specs/tokentest-testtransfer-spec.k --definition out/kompiled --spec-module TOKENTEST-TESTTRANSFER-SPEC --output json
kore-exec: [285172538] Warning (WarnStuckClaimState):
The configuration's term unifies with the destination's term, but the implication check between the conditions has failed. Location: /foundry-demo/out/specs/tokentest-testtransfer-spec.k:9:159-292:126
Context:
(InfoReachability) while checking the implication
kore-exec: [285193313] Warning (WarnUnexploredBranches):
2 branches were still unexplored when the action failed.
{"format":"KAST","version":2,"term":{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#Ceil","params":[{"node":"KSort","name":"Set"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"Set:difference","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1032069922050249630382865877677304880282300743300","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_TOUCHEDACCOUNTS_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Set"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_TOUCHEDACCOUNTS_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Set"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Ceil","params":[{"node":"KSort","name":"Set"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"Set:difference","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1032069922050249630382865877677304880282300743300","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_TOUCHEDACCOUNTS_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Set"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Ceil","params":[{"node":"KSort","name":"Set"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_TOUCHEDACCOUNTS_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Set"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<generatedTop>","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<foundry>","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<kevm>","params":[]},"arity":5,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<k>","params":[]},"arity":1,"args":[{"node":"KSequence","arity":2,"items":[{"node":"KApply","label":{"node":"KLabel","name":"#halt_EVM_KItem","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_CONTINUATION","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"K"}}}}]}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<exit-code>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_EXITCODE_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<mode>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"NORMAL","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<schedule>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"LONDON_EVM","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<ethereum>","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<evm>","params":[]},"arity":12,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<output>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bytes"},"token":"b\"\"","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<statusCode>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"EVMC_OUT_OF_GAS_NETWORK_ExceptionalStatusCode","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<endPC>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"316","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<callStack>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":".List","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<interimStates>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_INTERIMSTATES_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"List"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<touchedAccounts>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"Set:difference","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1032069922050249630382865877677304880282300743300","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_TOUCHEDACCOUNTS_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Set"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_TOUCHEDACCOUNTS_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Set"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<callState>","params":[]},"arity":14,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<program>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bytes"},"token":"b\"`\\x80`@R4\\x80\\x15a\\x00\\x10W`\\x00\\x80\\xfd[P`\\x046\\x10a\\x00bW`\\x005`\\xe0\\x1c\\x80c\\n\\x92T\\xe4\\x14a\\x00gW\\x80c:v\\x84c\\x14a\\x00qW\\x80c\\xbaAO\\xa6\\x14a\\x00\\xa9W\\x80c\\xdbg05\\x14a\\x00\\xc1W\\x80c\\xf8\\xcc\\xbfG\\x14a\\x00\\xd4W\\x80c\\xfav&\\xd4\\x14a\\x00\\xe7W[`\\x00\\x80\\xfd[a\\x00oa\\x00\\xf4V[\\x00[a\\x00\\x8csq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-\\x81V[`@Q`\\x01`\\x01`\\xa0\\x1b\\x03\\x90\\x91\\x16\\x81R` \\x01[`@Q\\x80\\x91\\x03\\x90\\xf3[a\\x00\\xb1a\\x02\\x7fV[`@Q\\x90\\x15\\x15\\x81R` \\x01a\\x00\\xa0V[a\\x00oa\\x00\\xcf6`\\x04a\\n\\xafV[a\\x03\\xaaV[`\\x00Ta\\x00\\xb1\\x90b\\x01\\x00\\x00\\x90\\x04`\\xff\\x16\\x81V[`\\x00Ta\\x00\\xb1\\x90`\\xff\\x16\\x81V[`@Qa\\x01\\x00\\x90a\\n\\x8bV[`@Q\\x80\\x91\\x03\\x90`\\x00\\xf0\\x80\\x15\\x80\\x15a\\x01\\x1cW=`\\x00\\x80>=`\\x00\\xfd[P`\\x08\\x80T`\\x01`\\x01`\\xa0\\x1b\\x03\\x19\\x16`\\x01`\\x01`\\xa0\\x1b\\x03\\x92\\x83\\x16\\x90\\x81\\x17\\x90\\x91U`\\tT`@Qc@\\xc1\\x0f\\x19`\\xe0\\x1b\\x81R\\x92\\x16`\\x04\\x83\\x01Rg\\x8a\\xc7#\\x04\\x89\\xe8\\x00\\x00`$\\x83\\x01R\\x90c@\\xc1\\x0f\\x19\\x90`D\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x01\\x85W`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x01\\x99W=`\\x00\\x80>=`\\x00\\xfd[PP`\\x08T`\\nT`@Qc@\\xc1\\x0f\\x19`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x91\\x82\\x16`\\x04\\x82\\x01Rh\\x01\\x15\\x8eF\\t\\x13\\xd0\\x00\\x00`$\\x82\\x01R\\x91\\x16\\x92Pc@\\xc1\\x0f\\x19\\x91P`D\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x01\\xf5W`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x02\\tW=`\\x00\\x80>=`\\x00\\xfd[PP`\\x08T`\\x0bT`@Qc@\\xc1\\x0f\\x19`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x91\\x82\\x16`\\x04\\x82\\x01Rh\\x01\\xa0Ui\\r\\x9d\\xb8\\x00\\x00`$\\x82\\x01R\\x91\\x16\\x92Pc@\\xc1\\x0f\\x19\\x91P`D\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x02eW`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x02yW=`\\x00\\x80>=`\\x00\\xfd[PPPPV[`\\x00\\x80Ta\\x01\\x00\\x90\\x04`\\xff\\x16\\x15a\\x02\\x9fWP`\\x00Ta\\x01\\x00\\x90\\x04`\\xff\\x16\\x90V[`\\x00sq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-;\\x15a\\x03\\xa5W`@\\x80Qsq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-` \\x82\\x01\\x81\\x90Re\\x19\\x98Z[\\x19Y`\\xd2\\x1b\\x82\\x84\\x01R\\x82Q\\x80\\x83\\x03\\x84\\x01\\x81R``\\x83\\x01\\x90\\x93R`\\x00\\x92\\x90\\x91a\\x03-\\x91\\x7ff\\x7f\\x9dp\\xcaA\\x1dp\\xea\\xd5\\r\\x8d\\\\\\\"\\x07\\r\\xaf\\xc3j\\xd7_=\\xcf^r7\\xb2*\\xde\\x9a\\xec\\xc4\\x91`\\x80\\x01a\\x0b\\x1bV[`@\\x80Q`\\x1f\\x19\\x81\\x84\\x03\\x01\\x81R\\x90\\x82\\x90Ra\\x03G\\x91a\\x0b?V[`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x86Z\\xf1\\x91PP=\\x80`\\x00\\x81\\x14a\\x03\\x84W`@Q\\x91P`\\x1f\\x19`?=\\x01\\x16\\x82\\x01`@R=\\x82R=`\\x00` \\x84\\x01>a\\x03\\x89V[``\\x91P[P\\x91PP\\x80\\x80` \\x01\\x90Q\\x81\\x01\\x90a\\x03\\xa1\\x91\\x90a\\x0bRV[\\x91PP[\\x91\\x90PV[a\\x03\\xb2a\\x00\\xf4V[`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x85\\x81\\x16`\\x04\\x83\\x01Rsq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-\\x92cLc\\xe5b\\x92\\x85\\x92\\x90\\x91\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x04\\x1aW=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x04>\\x91\\x90a\\x0btV[`@Q`\\x01`\\x01`\\xe0\\x1b\\x03\\x19`\\xe0\\x85\\x90\\x1b\\x16\\x81R\\x91\\x11\\x15`\\x04\\x82\\x01R`$\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x04wW`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x04\\x8bW=`\\x00\\x80>=`\\x00\\xfd[PP`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x87\\x81\\x16`\\x04\\x83\\x01R`\\x00\\x94P\\x90\\x91\\x16\\x91Pcp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x04\\xdcW=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x05\\x00\\x91\\x90a\\x0btV[`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x86\\x81\\x16`\\x04\\x83\\x01R\\x92\\x93P`\\x00\\x92\\x90\\x91\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x05PW=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x05t\\x91\\x90a\\x0btV[`@Qc\\xcaf\\x9f\\xa7`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x87\\x16`\\x04\\x82\\x01R\\x90\\x91Psq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-\\x90c\\xcaf\\x9f\\xa7\\x90`$\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x05\\xccW`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x05\\xe0W=`\\x00\\x80>=`\\x00\\xfd[PP`\\x08T`@Qc\\xa9\\x05\\x9c\\xbb`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x88\\x81\\x16`\\x04\\x83\\x01R`$\\x82\\x01\\x88\\x90R\\x90\\x91\\x16\\x92Pc\\xa9\\x05\\x9c\\xbb\\x91P`D\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x062W`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x06FW=`\\x00\\x80>=`\\x00\\xfd[PPPP\\x83`\\x01`\\x01`\\xa0\\x1b\\x03\\x16\\x85`\\x01`\\x01`\\xa0\\x1b\\x03\\x16\\x03a\\x07TW`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x87\\x81\\x16`\\x04\\x83\\x01Ra\\x06\\xd9\\x92\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x06\\xafW=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x06\\xd3\\x91\\x90a\\x0btV[\\x83a\\x08TV[`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x86\\x81\\x16`\\x04\\x83\\x01Ra\\x07O\\x92\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x07%W=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x07I\\x91\\x90a\\x0btV[\\x82a\\x08TV[a\\x08MV[`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x87\\x81\\x16`\\x04\\x83\\x01Ra\\x07\\xd3\\x92\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x07\\xa0W=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x07\\xc4\\x91\\x90a\\x0btV[a\\x07\\xce\\x85\\x85a\\x0b\\xa3V[a\\x08TV[`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x86\\x81\\x16`\\x04\\x83\\x01Ra\\x08M\\x92\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x08\\x1fW=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x08C\\x91\\x90a\\x0btV[a\\x07\\xce\\x85\\x84a\\x0b\\xbcV[PPPPPV[\\x80\\x82\\x14a\\t{W\\x7fA0O\\xac\\xd92=u\\xb1\\x1b\\xcd\\xd6\\t\\xcb8\\xef\\xff\\xfd\\xb0W\\x10\\xf7\\xca\\xf0\\xe9\\xb1lm\\x9dp\\x9fP`@Qa\\x08\\xc5\\x90` \\x80\\x82R`\\\"\\x90\\x82\\x01R\\x7fError: a == b not satisfied [uin`@\\x82\\x01Rat]`\\xf0\\x1b``\\x82\\x01R`\\x80\\x01\\x90V[`@Q\\x80\\x91\\x03\\x90\\xa1`@\\x80Q\\x81\\x81R`\\n\\x81\\x83\\x01Ri\\x08\\x08\\x11^\\x1c\\x19X\\xdd\\x19Y`\\xb2\\x1b``\\x82\\x01R` \\x81\\x01\\x83\\x90R\\x90Q\\x7f\\xb2\\xde/\\xbe\\x80\\x1a\\r\\xf6\\xc0\\xcb\\xdd\\xfdD\\x8b\\xa3\\xc4\\x1dH\\xa0@\\xca5\\xc5l\\x81\\x96\\xef\\x0f\\xca\\xe7!\\xa8\\x91\\x81\\x90\\x03`\\x80\\x01\\x90\\xa1`@\\x80Q\\x81\\x81R`\\n\\x81\\x83\\x01Ri\\x08\\x08\\x08\\x08\\x10X\\xdd\\x1dX[`\\xb2\\x1b``\\x82\\x01R` \\x81\\x01\\x84\\x90R\\x90Q\\x7f\\xb2\\xde/\\xbe\\x80\\x1a\\r\\xf6\\xc0\\xcb\\xdd\\xfdD\\x8b\\xa3\\xc4\\x1dH\\xa0@\\xca5\\xc5l\\x81\\x96\\xef\\x0f\\xca\\xe7!\\xa8\\x91\\x81\\x90\\x03`\\x80\\x01\\x90\\xa1a\\t{a\\t\\x7fV[PPV[sq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-;\\x15a\\nzW`@\\x80Qsq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-` \\x82\\x01\\x81\\x90Re\\x19\\x98Z[\\x19Y`\\xd2\\x1b\\x92\\x82\\x01\\x92\\x90\\x92R`\\x01``\\x82\\x01R`\\x00\\x91\\x90\\x7fp\\xca\\x10\\xbb\\xd0\\xdb\\xfd\\x90 \\xa9\\xf4\\xb14\\x02\\xc1l\\xb1 p^\\r\\x1c\\n\\xea\\xb1\\x0f\\xa3S\\xaeXo\\xc4\\x90`\\x80\\x01`@\\x80Q`\\x1f\\x19\\x81\\x84\\x03\\x01\\x81R\\x90\\x82\\x90Ra\\n\\x19\\x92\\x91` \\x01a\\x0b\\x1bV[`@\\x80Q`\\x1f\\x19\\x81\\x84\\x03\\x01\\x81R\\x90\\x82\\x90Ra\\n3\\x91a\\x0b?V[`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x86Z\\xf1\\x91PP=\\x80`\\x00\\x81\\x14a\\npW`@Q\\x91P`\\x1f\\x19`?=\\x01\\x16\\x82\\x01`@R=\\x82R=`\\x00` \\x84\\x01>a\\nuV[``\\x91P[PPPP[`\\x00\\x80Ta\\xff\\x00\\x19\\x16a\\x01\\x00\\x17\\x90UV[a\\x02\\x9e\\x80a\\x0b\\xd0\\x839\\x01\\x90V[\\x805`\\x01`\\x01`\\xa0\\x1b\\x03\\x81\\x16\\x81\\x14a\\x03\\xa5W`\\x00\\x80\\xfd[`\\x00\\x80`\\x00``\\x84\\x86\\x03\\x12\\x15a\\n\\xc4W`\\x00\\x80\\xfd[a\\n\\xcd\\x84a\\n\\x98V[\\x92Pa\\n\\xdb` \\x85\\x01a\\n\\x98V[\\x91P`@\\x84\\x015\\x90P\\x92P\\x92P\\x92V[`\\x00\\x81Q`\\x00[\\x81\\x81\\x10\\x15a\\x0b\\fW` \\x81\\x85\\x01\\x81\\x01Q\\x86\\x83\\x01R\\x01a\\n\\xf2V[P`\\x00\\x93\\x01\\x92\\x83RP\\x90\\x91\\x90PV[`\\x01`\\x01`\\xe0\\x1b\\x03\\x19\\x83\\x16\\x81R`\\x00a\\x0b7`\\x04\\x83\\x01\\x84a\\n\\xebV[\\x94\\x93PPPPV[`\\x00a\\x0bK\\x82\\x84a\\n\\xebV[\\x93\\x92PPPV[`\\x00` \\x82\\x84\\x03\\x12\\x15a\\x0bdW`\\x00\\x80\\xfd[\\x81Q\\x80\\x15\\x15\\x81\\x14a\\x0bKW`\\x00\\x80\\xfd[`\\x00` \\x82\\x84\\x03\\x12\\x15a\\x0b\\x86W`\\x00\\x80\\xfd[PQ\\x91\\x90PV[cNH{q`\\xe0\\x1b`\\x00R`\\x11`\\x04R`$`\\x00\\xfd[\\x81\\x81\\x03\\x81\\x81\\x11\\x15a\\x0b\\xb6Wa\\x0b\\xb6a\\x0b\\x8dV[\\x92\\x91PPV[\\x80\\x82\\x01\\x80\\x82\\x11\\x15a\\x0b\\xb6Wa\\x0b\\xb6a\\x0b\\x8dV\\xfe`\\xa0`@R4\\x80\\x15a\\x00\\x10W`\\x00\\x80\\xfd[P3`\\x80R`\\x80Qa\\x02oa\\x00/`\\x009`\\x00`\\xab\\x01Ra\\x02o`\\x00\\xf3\\xfe`\\x80`@R4\\x80\\x15a\\x00\\x10W`\\x00\\x80\\xfd[P`\\x046\\x10a\\x00AW`\\x005`\\xe0\\x1c\\x80c@\\xc1\\x0f\\x19\\x14a\\x00FW\\x80cp\\xa0\\x821\\x14a\\x00[W\\x80c\\xa9\\x05\\x9c\\xbb\\x14a\\x00\\x8dW[`\\x00\\x80\\xfd[a\\x00Ya\\x00T6`\\x04a\\x01\\xabV[a\\x00\\xa0V[\\x00[a\\x00{a\\x00i6`\\x04a\\x01\\xd5V[`\\x00` \\x81\\x90R\\x90\\x81R`@\\x90 T\\x81V[`@Q\\x90\\x81R` \\x01`@Q\\x80\\x91\\x03\\x90\\xf3[a\\x00Ya\\x00\\x9b6`\\x04a\\x01\\xabV[a\\x01CV[3`\\x01`\\x01`\\xa0\\x1b\\x03\\x7f\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x16\\x14a\\x01\\x12W`@QbF\\x1b\\xcd`\\xe5\\x1b\\x81R` `\\x04\\x82\\x01R`\\x13`$\\x82\\x01Rr\\x13\\xdb\\x9b\\x1eH\\x1b\\xdd\\xdb\\x99\\\\\\x88\\x18\\xd8[\\x88\\x1bZ[\\x9d`j\\x1b`D\\x82\\x01R`d\\x01`@Q\\x80\\x91\\x03\\x90\\xfd[`\\x01`\\x01`\\xa0\\x1b\\x03\\x82\\x16`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01:\\x90\\x84\\x90a\\x02\\rV[\\x90\\x91UPPPPV[3`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01b\\x90\\x84\\x90a\\x02&V[\\x90\\x91UPP`\\x01`\\x01`\\xa0\\x1b\\x03\\x82\\x16`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01:\\x90\\x84\\x90a\\x02\\rV[\\x805`\\x01`\\x01`\\xa0\\x1b\\x03\\x81\\x16\\x81\\x14a\\x01\\xa6W`\\x00\\x80\\xfd[\\x91\\x90PV[`\\x00\\x80`@\\x83\\x85\\x03\\x12\\x15a\\x01\\xbeW`\\x00\\x80\\xfd[a\\x01\\xc7\\x83a\\x01\\x8fV[\\x94` \\x93\\x90\\x93\\x015\\x93PPPV[`\\x00` \\x82\\x84\\x03\\x12\\x15a\\x01\\xe7W`\\x00\\x80\\xfd[a\\x01\\xf0\\x82a\\x01\\x8fV[\\x93\\x92PPPV[cNH{q`\\xe0\\x1b`\\x00R`\\x11`\\x04R`$`\\x00\\xfd[\\x80\\x82\\x01\\x80\\x82\\x11\\x15a\\x02 Wa\\x02 a\\x01\\xf7V[\\x92\\x91PPV[\\x81\\x81\\x03\\x81\\x81\\x11\\x15a\\x02 Wa\\x02 a\\x01\\xf7V\\xfe\\xa2dipfsX\\\"\\x12 \\x12\\xa7\\xee\\x81\\x95r\\x8a\\xce4\\x9c\\xde\\xc9\\f\\x1f\\xe0'\\x80n*uLb\\xd7\\x12\\x8b\\x07\\xe01\\\\\\xe7\\x84\\xf4dsolcC\\x00\\x08\\x11\\x003\\xa2dipfsX\\\"\\x12 \\xee\\xcd\\x9c\\x18\\xdd;BG\\xedVh\\xbe\\xa0\\xda\\x93\\xc8\\x890\\xa2RT\\xf5\\x9e~-\\xf0Crr\\xd4\\\\KdsolcC\\x00\\x08\\x11\\x003\"","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<jumpDests>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"16","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"98","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"103","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"111","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"113","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"140","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"160","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"169","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"177","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"193","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"207","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"212","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"231","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"244","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"284","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"389","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"409","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"501","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"521","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"613","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"633","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"639","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"671","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"813","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"839","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"900","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"905","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"929","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"933","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"938","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"946","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1050","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1086","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1143","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1163","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1244","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1280","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1360","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1396","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1484","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1504","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1586","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1606","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1711","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1747","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1753","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1829","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1865","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1871","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1876","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1952","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1988","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1998","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2003","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2079","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2115","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2125","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2132","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2245","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2427","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2431","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2585","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2611","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2672","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2677","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2682","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2699","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2712","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2735","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2756","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2765","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2779","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2795","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2802","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2828","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2843","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2871","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2879","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2891","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2898","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2916","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2932","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2950","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2957","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2979","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"2998","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3004","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3040","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3087","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3136","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3141","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3155","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3160","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3162","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3176","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3194","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3212","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3226","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3231","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3345","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3385","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3394","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3425","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3470","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3493","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3498","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3517","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3526","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3540","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3558","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3567","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3574","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3596","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3615","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3621","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"256","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<id>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1032069922050249630382865877677304880282300743300","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<caller>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_CALLER_ID","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Account"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<callData>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_++__EVM-TYPES_ByteArray_ByteArray_ByteArray","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bytes"},"token":"b\"\\xdbg05\"","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_++__EVM-TYPES_ByteArray_ByteArray_ByteArray","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_++__EVM-TYPES_ByteArray_ByteArray_ByteArray","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"#buf(_,_)_BUF-SYNTAX_ByteArray_Int_Int","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"32","att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_VV0_from_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#buf(_,_)_BUF-SYNTAX_ByteArray_Int_Int","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"32","att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_VV1_to_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#buf(_,_)_BUF-SYNTAX_ByteArray_Int_Int","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"32","att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_VV2_amount_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<callValue>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<wordStack>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_:__EVM-TYPES_WordStack_Int_WordStack","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_:__EVM-TYPES_WordStack_Int_WordStack","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1461501637330902918203684832716283019655932542975","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_:__EVM-TYPES_WordStack_Int_WordStack","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"946","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_:__EVM-TYPES_WordStack_Int_WordStack","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_VV2_amount_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}},{"node":"KApply","label":{"node":"KLabel","name":"_:__EVM-TYPES_WordStack_Int_WordStack","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_VV1_to_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}},{"node":"KApply","label":{"node":"KLabel","name":"_:__EVM-TYPES_WordStack_Int_WordStack","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_VV0_from_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}},{"node":"KApply","label":{"node":"KLabel","name":"_:__EVM-TYPES_WordStack_Int_WordStack","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"111","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_:__EVM-TYPES_WordStack_Int_WordStack","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3680972853","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":".WordStack_EVM-TYPES_WordStack","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<localMem>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bytes"},"token":"b\"\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x80\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00`\\xa0`@R4\\x80\\x15a\\x00\\x10W`\\x00\\x80\\xfd[P3`\\x80R`\\x80Qa\\x02oa\\x00/`\\x009`\\x00`\\xab\\x01Ra\\x02o`\\x00\\xf3\\xfe`\\x80`@R4\\x80\\x15a\\x00\\x10W`\\x00\\x80\\xfd[P`\\x046\\x10a\\x00AW`\\x005`\\xe0\\x1c\\x80c@\\xc1\\x0f\\x19\\x14a\\x00FW\\x80cp\\xa0\\x821\\x14a\\x00[W\\x80c\\xa9\\x05\\x9c\\xbb\\x14a\\x00\\x8dW[`\\x00\\x80\\xfd[a\\x00Ya\\x00T6`\\x04a\\x01\\xabV[a\\x00\\xa0V[\\x00[a\\x00{a\\x00i6`\\x04a\\x01\\xd5V[`\\x00` \\x81\\x90R\\x90\\x81R`@\\x90 T\\x81V[`@Q\\x90\\x81R` \\x01`@Q\\x80\\x91\\x03\\x90\\xf3[a\\x00Ya\\x00\\x9b6`\\x04a\\x01\\xabV[a\\x01CV[3`\\x01`\\x01`\\xa0\\x1b\\x03\\x7f\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x16\\x14a\\x01\\x12W`@QbF\\x1b\\xcd`\\xe5\\x1b\\x81R` `\\x04\\x82\\x01R`\\x13`$\\x82\\x01Rr\\x13\\xdb\\x9b\\x1eH\\x1b\\xdd\\xdb\\x99\\\\\\x88\\x18\\xd8[\\x88\\x1bZ[\\x9d`j\\x1b`D\\x82\\x01R`d\\x01`@Q\\x80\\x91\\x03\\x90\\xfd[`\\x01`\\x01`\\xa0\\x1b\\x03\\x82\\x16`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01:\\x90\\x84\\x90a\\x02\\rV[\\x90\\x91UPPPPV[3`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01b\\x90\\x84\\x90a\\x02&V[\\x90\\x91UPP`\\x01`\\x01`\\xa0\\x1b\\x03\\x82\\x16`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01:\\x90\\x84\\x90a\\x02\\rV[\\x805`\\x01`\\x01`\\xa0\\x1b\\x03\\x81\\x16\\x81\\x14a\\x01\\xa6W`\\x00\\x80\\xfd[\\x91\\x90PV[`\\x00\\x80`@\\x83\\x85\\x03\\x12\\x15a\\x01\\xbeW`\\x00\\x80\\xfd[a\\x01\\xc7\\x83a\\x01\\x8fV[\\x94` \\x93\\x90\\x93\\x015\\x93PPPV[`\\x00` \\x82\\x84\\x03\\x12\\x15a\\x01\\xe7W`\\x00\\x80\\xfd[a\\x01\\xf0\\x82a\\x01\\x8fV[\\x93\\x92PPPV[cNH{q`\\xe0\\x1b`\\x00R`\\x11`\\x04R`$`\\x00\\xfd[\\x80\\x82\\x01\\x80\\x82\\x11\\x15a\\x02 Wa\\x02 a\\x01\\xf7V[\\x92\\x91PPV[\\x81\\x81\\x03\\x81\\x81\\x11\\x15a\\x02 Wa\\x02 a\\x01\\xf7V\\xfe\\xa2dipfsX\\\"\\x12 \\x12\\xa7\\xee\\x81\\x95r\\x8a\\xce4\\x9c\\xde\\xc9\\f\\x1f\\xe0'\\x80n*uLb\\xd7\\x12\\x8b\\x07\\xe01\\\\\\xe7\\x84\\xf4dsolcC\\x00\\x08\\x11\\x003\"","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<pc>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"316","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<gas>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"19999999999999840330","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<memoryUsed>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"25","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<callGas>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"19687499999999967832","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<static>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"false","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<callDepth>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<substate>","params":[]},"arity":5,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<selfDestruct>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_SELFDESTRUCT_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Set"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<log>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_LOG_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"List"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<refund>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_+Int_","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_REFUND_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}},{"node":"KApply","label":{"node":"KLabel","name":"Rsstore(_,_,_,_)_EVM_Int_Schedule_Int_Int_Int","params":[]},"arity":4,"args":[{"node":"KApply","label":{"node":"KLabel","name":"LONDON_EVM","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_|Int_","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_&Int_","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"115792089237316195423570985007226406215939081747436879206741300988257197096960","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#lookup(_,_)_EVM-TYPES_Int_Map_Int","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_ACCT_STORAGE","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Map"}}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"8","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#lookup(_,_)_EVM-TYPES_Int_Map_Int","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_ACCT_STORAGE","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Map"}}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"8","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#lookup(_,_)_EVM-TYPES_Int_Map_Int","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_DotVar3","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Map"}}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"8","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<accessedAccounts>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1032069922050249630382865877677304880282300743300","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<accessedStorage>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_|->_","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1032069922050249630382865877677304880282300743300","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"8","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<gasPrice>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_GASPRICE_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<origin>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_ORIGIN_ID","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Account"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<blockhashes>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_BLOCKHASHES_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"List"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<block>","params":[]},"arity":17,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<previousHash>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_PREVIOUSHASH_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<ommersHash>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_OMMERSHASH_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<coinbase>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_COINBASE_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<stateRoot>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_STATEROOT_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<transactionsRoot>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_TRANSACTIONSROOT_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<receiptsRoot>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_RECEIPTSROOT_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<logsBloom>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_LOGSBLOOM_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Bytes"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<difficulty>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_DIFFICULTY_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<number>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_NUMBER_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<gasLimit>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_GASLIMIT_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<gasUsed>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_GASUSED_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<timestamp>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_TIMESTAMP_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<extraData>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_EXTRADATA_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Bytes"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<mixHash>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_MIXHASH_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<blockNonce>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_BLOCKNONCE_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<baseFee>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_BASEFEE_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<ommerBlockHeaders>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_OMMERBLOCKHEADERS_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"JSON"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<network>","params":[]},"arity":6,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<chainID>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_CHAINID_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<activeAccounts>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_Set_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"120209876281281145568259943","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"137122462167341575662000267002353578582749290296","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"645326474426547203313410069153905908525362434349","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"SetItem","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1032069922050249630382865877677304880282300743300","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<accounts>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_AccountCellMap_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_AccountCellMap_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_AccountCellMap_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_AccountCellMap_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"_AccountCellMap_","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"AccountCellMapItem","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"120209876281281145568259943","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<account>","params":[]},"arity":6,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"120209876281281145568259943","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<balance>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<code>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bytes"},"token":"b\"\"","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<storage>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":".Map","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<origStorage>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":".Map","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<nonce>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"AccountCellMapItem","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"137122462167341575662000267002353578582749290296","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<account>","params":[]},"arity":6,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"137122462167341575662000267002353578582749290296","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<balance>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<code>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bytes"},"token":"b\"\"","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<storage>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":".Map","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<origStorage>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":".Map","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<nonce>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"AccountCellMapItem","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<account>","params":[]},"arity":6,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<balance>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<code>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bytes"},"token":"b\"`\\x80`@R4\\x80\\x15a\\x00\\x10W`\\x00\\x80\\xfd[P`\\x046\\x10a\\x00AW`\\x005`\\xe0\\x1c\\x80c@\\xc1\\x0f\\x19\\x14a\\x00FW\\x80cp\\xa0\\x821\\x14a\\x00[W\\x80c\\xa9\\x05\\x9c\\xbb\\x14a\\x00\\x8dW[`\\x00\\x80\\xfd[a\\x00Ya\\x00T6`\\x04a\\x01\\xabV[a\\x00\\xa0V[\\x00[a\\x00{a\\x00i6`\\x04a\\x01\\xd5V[`\\x00` \\x81\\x90R\\x90\\x81R`@\\x90 T\\x81V[`@Q\\x90\\x81R` \\x01`@Q\\x80\\x91\\x03\\x90\\xf3[a\\x00Ya\\x00\\x9b6`\\x04a\\x01\\xabV[a\\x01CV[3`\\x01`\\x01`\\xa0\\x1b\\x03\\x7f\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\xb4\\xc7\\x9d\\xab\\x8f%\\x9cz\\xeen[*\\xa7)\\x82\\x18d\\\"~\\x84\\x16\\x14a\\x01\\x12W`@QbF\\x1b\\xcd`\\xe5\\x1b\\x81R` `\\x04\\x82\\x01R`\\x13`$\\x82\\x01Rr\\x13\\xdb\\x9b\\x1eH\\x1b\\xdd\\xdb\\x99\\\\\\x88\\x18\\xd8[\\x88\\x1bZ[\\x9d`j\\x1b`D\\x82\\x01R`d\\x01`@Q\\x80\\x91\\x03\\x90\\xfd[`\\x01`\\x01`\\xa0\\x1b\\x03\\x82\\x16`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01:\\x90\\x84\\x90a\\x02\\rV[\\x90\\x91UPPPPV[3`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01b\\x90\\x84\\x90a\\x02&V[\\x90\\x91UPP`\\x01`\\x01`\\xa0\\x1b\\x03\\x82\\x16`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01:\\x90\\x84\\x90a\\x02\\rV[\\x805`\\x01`\\x01`\\xa0\\x1b\\x03\\x81\\x16\\x81\\x14a\\x01\\xa6W`\\x00\\x80\\xfd[\\x91\\x90PV[`\\x00\\x80`@\\x83\\x85\\x03\\x12\\x15a\\x01\\xbeW`\\x00\\x80\\xfd[a\\x01\\xc7\\x83a\\x01\\x8fV[\\x94` \\x93\\x90\\x93\\x015\\x93PPPV[`\\x00` \\x82\\x84\\x03\\x12\\x15a\\x01\\xe7W`\\x00\\x80\\xfd[a\\x01\\xf0\\x82a\\x01\\x8fV[\\x93\\x92PPPV[cNH{q`\\xe0\\x1b`\\x00R`\\x11`\\x04R`$`\\x00\\xfd[\\x80\\x82\\x01\\x80\\x82\\x11\\x15a\\x02 Wa\\x02 a\\x01\\xf7V[\\x92\\x91PPV[\\x81\\x81\\x03\\x81\\x81\\x11\\x15a\\x02 Wa\\x02 a\\x01\\xf7V\\xfe\\xa2dipfsX\\\"\\x12 \\x12\\xa7\\xee\\x81\\x95r\\x8a\\xce4\\x9c\\xde\\xc9\\f\\x1f\\xe0'\\x80n*uLb\\xd7\\x12\\x8b\\x07\\xe01\\\\\\xe7\\x84\\xf4dsolcC\\x00\\x08\\x11\\x003\"","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<storage>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":".Map","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<origStorage>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":".Map","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<nonce>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"AccountCellMapItem","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"645326474426547203313410069153905908525362434349","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<account>","params":[]},"arity":6,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"645326474426547203313410069153905908525362434349","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<balance>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<code>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bytes"},"token":"b\"\\x00\"","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<storage>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"CHEATCODE_STORAGE","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Map"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<origStorage>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":".Map","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<nonce>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"AccountCellMapItem","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1032069922050249630382865877677304880282300743300","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<account>","params":[]},"arity":6,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1032069922050249630382865877677304880282300743300","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<balance>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<code>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bytes"},"token":"b\"`\\x80`@R4\\x80\\x15a\\x00\\x10W`\\x00\\x80\\xfd[P`\\x046\\x10a\\x00bW`\\x005`\\xe0\\x1c\\x80c\\n\\x92T\\xe4\\x14a\\x00gW\\x80c:v\\x84c\\x14a\\x00qW\\x80c\\xbaAO\\xa6\\x14a\\x00\\xa9W\\x80c\\xdbg05\\x14a\\x00\\xc1W\\x80c\\xf8\\xcc\\xbfG\\x14a\\x00\\xd4W\\x80c\\xfav&\\xd4\\x14a\\x00\\xe7W[`\\x00\\x80\\xfd[a\\x00oa\\x00\\xf4V[\\x00[a\\x00\\x8csq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-\\x81V[`@Q`\\x01`\\x01`\\xa0\\x1b\\x03\\x90\\x91\\x16\\x81R` \\x01[`@Q\\x80\\x91\\x03\\x90\\xf3[a\\x00\\xb1a\\x02\\x7fV[`@Q\\x90\\x15\\x15\\x81R` \\x01a\\x00\\xa0V[a\\x00oa\\x00\\xcf6`\\x04a\\n\\xafV[a\\x03\\xaaV[`\\x00Ta\\x00\\xb1\\x90b\\x01\\x00\\x00\\x90\\x04`\\xff\\x16\\x81V[`\\x00Ta\\x00\\xb1\\x90`\\xff\\x16\\x81V[`@Qa\\x01\\x00\\x90a\\n\\x8bV[`@Q\\x80\\x91\\x03\\x90`\\x00\\xf0\\x80\\x15\\x80\\x15a\\x01\\x1cW=`\\x00\\x80>=`\\x00\\xfd[P`\\x08\\x80T`\\x01`\\x01`\\xa0\\x1b\\x03\\x19\\x16`\\x01`\\x01`\\xa0\\x1b\\x03\\x92\\x83\\x16\\x90\\x81\\x17\\x90\\x91U`\\tT`@Qc@\\xc1\\x0f\\x19`\\xe0\\x1b\\x81R\\x92\\x16`\\x04\\x83\\x01Rg\\x8a\\xc7#\\x04\\x89\\xe8\\x00\\x00`$\\x83\\x01R\\x90c@\\xc1\\x0f\\x19\\x90`D\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x01\\x85W`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x01\\x99W=`\\x00\\x80>=`\\x00\\xfd[PP`\\x08T`\\nT`@Qc@\\xc1\\x0f\\x19`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x91\\x82\\x16`\\x04\\x82\\x01Rh\\x01\\x15\\x8eF\\t\\x13\\xd0\\x00\\x00`$\\x82\\x01R\\x91\\x16\\x92Pc@\\xc1\\x0f\\x19\\x91P`D\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x01\\xf5W`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x02\\tW=`\\x00\\x80>=`\\x00\\xfd[PP`\\x08T`\\x0bT`@Qc@\\xc1\\x0f\\x19`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x91\\x82\\x16`\\x04\\x82\\x01Rh\\x01\\xa0Ui\\r\\x9d\\xb8\\x00\\x00`$\\x82\\x01R\\x91\\x16\\x92Pc@\\xc1\\x0f\\x19\\x91P`D\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x02eW`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x02yW=`\\x00\\x80>=`\\x00\\xfd[PPPPV[`\\x00\\x80Ta\\x01\\x00\\x90\\x04`\\xff\\x16\\x15a\\x02\\x9fWP`\\x00Ta\\x01\\x00\\x90\\x04`\\xff\\x16\\x90V[`\\x00sq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-;\\x15a\\x03\\xa5W`@\\x80Qsq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-` \\x82\\x01\\x81\\x90Re\\x19\\x98Z[\\x19Y`\\xd2\\x1b\\x82\\x84\\x01R\\x82Q\\x80\\x83\\x03\\x84\\x01\\x81R``\\x83\\x01\\x90\\x93R`\\x00\\x92\\x90\\x91a\\x03-\\x91\\x7ff\\x7f\\x9dp\\xcaA\\x1dp\\xea\\xd5\\r\\x8d\\\\\\\"\\x07\\r\\xaf\\xc3j\\xd7_=\\xcf^r7\\xb2*\\xde\\x9a\\xec\\xc4\\x91`\\x80\\x01a\\x0b\\x1bV[`@\\x80Q`\\x1f\\x19\\x81\\x84\\x03\\x01\\x81R\\x90\\x82\\x90Ra\\x03G\\x91a\\x0b?V[`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x86Z\\xf1\\x91PP=\\x80`\\x00\\x81\\x14a\\x03\\x84W`@Q\\x91P`\\x1f\\x19`?=\\x01\\x16\\x82\\x01`@R=\\x82R=`\\x00` \\x84\\x01>a\\x03\\x89V[``\\x91P[P\\x91PP\\x80\\x80` \\x01\\x90Q\\x81\\x01\\x90a\\x03\\xa1\\x91\\x90a\\x0bRV[\\x91PP[\\x91\\x90PV[a\\x03\\xb2a\\x00\\xf4V[`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x85\\x81\\x16`\\x04\\x83\\x01Rsq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-\\x92cLc\\xe5b\\x92\\x85\\x92\\x90\\x91\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x04\\x1aW=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x04>\\x91\\x90a\\x0btV[`@Q`\\x01`\\x01`\\xe0\\x1b\\x03\\x19`\\xe0\\x85\\x90\\x1b\\x16\\x81R\\x91\\x11\\x15`\\x04\\x82\\x01R`$\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x04wW`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x04\\x8bW=`\\x00\\x80>=`\\x00\\xfd[PP`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x87\\x81\\x16`\\x04\\x83\\x01R`\\x00\\x94P\\x90\\x91\\x16\\x91Pcp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x04\\xdcW=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x05\\x00\\x91\\x90a\\x0btV[`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x86\\x81\\x16`\\x04\\x83\\x01R\\x92\\x93P`\\x00\\x92\\x90\\x91\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x05PW=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x05t\\x91\\x90a\\x0btV[`@Qc\\xcaf\\x9f\\xa7`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x87\\x16`\\x04\\x82\\x01R\\x90\\x91Psq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-\\x90c\\xcaf\\x9f\\xa7\\x90`$\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x05\\xccW`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x05\\xe0W=`\\x00\\x80>=`\\x00\\xfd[PP`\\x08T`@Qc\\xa9\\x05\\x9c\\xbb`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x88\\x81\\x16`\\x04\\x83\\x01R`$\\x82\\x01\\x88\\x90R\\x90\\x91\\x16\\x92Pc\\xa9\\x05\\x9c\\xbb\\x91P`D\\x01`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x87\\x80;\\x15\\x80\\x15a\\x062W`\\x00\\x80\\xfd[PZ\\xf1\\x15\\x80\\x15a\\x06FW=`\\x00\\x80>=`\\x00\\xfd[PPPP\\x83`\\x01`\\x01`\\xa0\\x1b\\x03\\x16\\x85`\\x01`\\x01`\\xa0\\x1b\\x03\\x16\\x03a\\x07TW`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x87\\x81\\x16`\\x04\\x83\\x01Ra\\x06\\xd9\\x92\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x06\\xafW=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x06\\xd3\\x91\\x90a\\x0btV[\\x83a\\x08TV[`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x86\\x81\\x16`\\x04\\x83\\x01Ra\\x07O\\x92\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x07%W=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x07I\\x91\\x90a\\x0btV[\\x82a\\x08TV[a\\x08MV[`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x87\\x81\\x16`\\x04\\x83\\x01Ra\\x07\\xd3\\x92\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x07\\xa0W=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x07\\xc4\\x91\\x90a\\x0btV[a\\x07\\xce\\x85\\x85a\\x0b\\xa3V[a\\x08TV[`\\x08T`@Qcp\\xa0\\x821`\\xe0\\x1b\\x81R`\\x01`\\x01`\\xa0\\x1b\\x03\\x86\\x81\\x16`\\x04\\x83\\x01Ra\\x08M\\x92\\x16\\x90cp\\xa0\\x821\\x90`$\\x01` `@Q\\x80\\x83\\x03\\x81\\x86Z\\xfa\\x15\\x80\\x15a\\x08\\x1fW=`\\x00\\x80>=`\\x00\\xfd[PPPP`@Q=`\\x1f\\x19`\\x1f\\x82\\x01\\x16\\x82\\x01\\x80`@RP\\x81\\x01\\x90a\\x08C\\x91\\x90a\\x0btV[a\\x07\\xce\\x85\\x84a\\x0b\\xbcV[PPPPPV[\\x80\\x82\\x14a\\t{W\\x7fA0O\\xac\\xd92=u\\xb1\\x1b\\xcd\\xd6\\t\\xcb8\\xef\\xff\\xfd\\xb0W\\x10\\xf7\\xca\\xf0\\xe9\\xb1lm\\x9dp\\x9fP`@Qa\\x08\\xc5\\x90` \\x80\\x82R`\\\"\\x90\\x82\\x01R\\x7fError: a == b not satisfied [uin`@\\x82\\x01Rat]`\\xf0\\x1b``\\x82\\x01R`\\x80\\x01\\x90V[`@Q\\x80\\x91\\x03\\x90\\xa1`@\\x80Q\\x81\\x81R`\\n\\x81\\x83\\x01Ri\\x08\\x08\\x11^\\x1c\\x19X\\xdd\\x19Y`\\xb2\\x1b``\\x82\\x01R` \\x81\\x01\\x83\\x90R\\x90Q\\x7f\\xb2\\xde/\\xbe\\x80\\x1a\\r\\xf6\\xc0\\xcb\\xdd\\xfdD\\x8b\\xa3\\xc4\\x1dH\\xa0@\\xca5\\xc5l\\x81\\x96\\xef\\x0f\\xca\\xe7!\\xa8\\x91\\x81\\x90\\x03`\\x80\\x01\\x90\\xa1`@\\x80Q\\x81\\x81R`\\n\\x81\\x83\\x01Ri\\x08\\x08\\x08\\x08\\x10X\\xdd\\x1dX[`\\xb2\\x1b``\\x82\\x01R` \\x81\\x01\\x84\\x90R\\x90Q\\x7f\\xb2\\xde/\\xbe\\x80\\x1a\\r\\xf6\\xc0\\xcb\\xdd\\xfdD\\x8b\\xa3\\xc4\\x1dH\\xa0@\\xca5\\xc5l\\x81\\x96\\xef\\x0f\\xca\\xe7!\\xa8\\x91\\x81\\x90\\x03`\\x80\\x01\\x90\\xa1a\\t{a\\t\\x7fV[PPV[sq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-;\\x15a\\nzW`@\\x80Qsq\\tp\\x9e\\xcf\\xa9\\x1a\\x80bo\\xf3\\x98\\x9dh\\xf6\\x7f[\\x1d\\xd1-` \\x82\\x01\\x81\\x90Re\\x19\\x98Z[\\x19Y`\\xd2\\x1b\\x92\\x82\\x01\\x92\\x90\\x92R`\\x01``\\x82\\x01R`\\x00\\x91\\x90\\x7fp\\xca\\x10\\xbb\\xd0\\xdb\\xfd\\x90 \\xa9\\xf4\\xb14\\x02\\xc1l\\xb1 p^\\r\\x1c\\n\\xea\\xb1\\x0f\\xa3S\\xaeXo\\xc4\\x90`\\x80\\x01`@\\x80Q`\\x1f\\x19\\x81\\x84\\x03\\x01\\x81R\\x90\\x82\\x90Ra\\n\\x19\\x92\\x91` \\x01a\\x0b\\x1bV[`@\\x80Q`\\x1f\\x19\\x81\\x84\\x03\\x01\\x81R\\x90\\x82\\x90Ra\\n3\\x91a\\x0b?V[`\\x00`@Q\\x80\\x83\\x03\\x81`\\x00\\x86Z\\xf1\\x91PP=\\x80`\\x00\\x81\\x14a\\npW`@Q\\x91P`\\x1f\\x19`?=\\x01\\x16\\x82\\x01`@R=\\x82R=`\\x00` \\x84\\x01>a\\nuV[``\\x91P[PPPP[`\\x00\\x80Ta\\xff\\x00\\x19\\x16a\\x01\\x00\\x17\\x90UV[a\\x02\\x9e\\x80a\\x0b\\xd0\\x839\\x01\\x90V[\\x805`\\x01`\\x01`\\xa0\\x1b\\x03\\x81\\x16\\x81\\x14a\\x03\\xa5W`\\x00\\x80\\xfd[`\\x00\\x80`\\x00``\\x84\\x86\\x03\\x12\\x15a\\n\\xc4W`\\x00\\x80\\xfd[a\\n\\xcd\\x84a\\n\\x98V[\\x92Pa\\n\\xdb` \\x85\\x01a\\n\\x98V[\\x91P`@\\x84\\x015\\x90P\\x92P\\x92P\\x92V[`\\x00\\x81Q`\\x00[\\x81\\x81\\x10\\x15a\\x0b\\fW` \\x81\\x85\\x01\\x81\\x01Q\\x86\\x83\\x01R\\x01a\\n\\xf2V[P`\\x00\\x93\\x01\\x92\\x83RP\\x90\\x91\\x90PV[`\\x01`\\x01`\\xe0\\x1b\\x03\\x19\\x83\\x16\\x81R`\\x00a\\x0b7`\\x04\\x83\\x01\\x84a\\n\\xebV[\\x94\\x93PPPPV[`\\x00a\\x0bK\\x82\\x84a\\n\\xebV[\\x93\\x92PPPV[`\\x00` \\x82\\x84\\x03\\x12\\x15a\\x0bdW`\\x00\\x80\\xfd[\\x81Q\\x80\\x15\\x15\\x81\\x14a\\x0bKW`\\x00\\x80\\xfd[`\\x00` \\x82\\x84\\x03\\x12\\x15a\\x0b\\x86W`\\x00\\x80\\xfd[PQ\\x91\\x90PV[cNH{q`\\xe0\\x1b`\\x00R`\\x11`\\x04R`$`\\x00\\xfd[\\x81\\x81\\x03\\x81\\x81\\x11\\x15a\\x0b\\xb6Wa\\x0b\\xb6a\\x0b\\x8dV[\\x92\\x91PPV[\\x80\\x82\\x01\\x80\\x82\\x11\\x15a\\x0b\\xb6Wa\\x0b\\xb6a\\x0b\\x8dV\\xfe`\\xa0`@R4\\x80\\x15a\\x00\\x10W`\\x00\\x80\\xfd[P3`\\x80R`\\x80Qa\\x02oa\\x00/`\\x009`\\x00`\\xab\\x01Ra\\x02o`\\x00\\xf3\\xfe`\\x80`@R4\\x80\\x15a\\x00\\x10W`\\x00\\x80\\xfd[P`\\x046\\x10a\\x00AW`\\x005`\\xe0\\x1c\\x80c@\\xc1\\x0f\\x19\\x14a\\x00FW\\x80cp\\xa0\\x821\\x14a\\x00[W\\x80c\\xa9\\x05\\x9c\\xbb\\x14a\\x00\\x8dW[`\\x00\\x80\\xfd[a\\x00Ya\\x00T6`\\x04a\\x01\\xabV[a\\x00\\xa0V[\\x00[a\\x00{a\\x00i6`\\x04a\\x01\\xd5V[`\\x00` \\x81\\x90R\\x90\\x81R`@\\x90 T\\x81V[`@Q\\x90\\x81R` \\x01`@Q\\x80\\x91\\x03\\x90\\xf3[a\\x00Ya\\x00\\x9b6`\\x04a\\x01\\xabV[a\\x01CV[3`\\x01`\\x01`\\xa0\\x1b\\x03\\x7f\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x16\\x14a\\x01\\x12W`@QbF\\x1b\\xcd`\\xe5\\x1b\\x81R` `\\x04\\x82\\x01R`\\x13`$\\x82\\x01Rr\\x13\\xdb\\x9b\\x1eH\\x1b\\xdd\\xdb\\x99\\\\\\x88\\x18\\xd8[\\x88\\x1bZ[\\x9d`j\\x1b`D\\x82\\x01R`d\\x01`@Q\\x80\\x91\\x03\\x90\\xfd[`\\x01`\\x01`\\xa0\\x1b\\x03\\x82\\x16`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01:\\x90\\x84\\x90a\\x02\\rV[\\x90\\x91UPPPPV[3`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01b\\x90\\x84\\x90a\\x02&V[\\x90\\x91UPP`\\x01`\\x01`\\xa0\\x1b\\x03\\x82\\x16`\\x00\\x90\\x81R` \\x81\\x90R`@\\x81 \\x80T\\x83\\x92\\x90a\\x01:\\x90\\x84\\x90a\\x02\\rV[\\x805`\\x01`\\x01`\\xa0\\x1b\\x03\\x81\\x16\\x81\\x14a\\x01\\xa6W`\\x00\\x80\\xfd[\\x91\\x90PV[`\\x00\\x80`@\\x83\\x85\\x03\\x12\\x15a\\x01\\xbeW`\\x00\\x80\\xfd[a\\x01\\xc7\\x83a\\x01\\x8fV[\\x94` \\x93\\x90\\x93\\x015\\x93PPPV[`\\x00` \\x82\\x84\\x03\\x12\\x15a\\x01\\xe7W`\\x00\\x80\\xfd[a\\x01\\xf0\\x82a\\x01\\x8fV[\\x93\\x92PPPV[cNH{q`\\xe0\\x1b`\\x00R`\\x11`\\x04R`$`\\x00\\xfd[\\x80\\x82\\x01\\x80\\x82\\x11\\x15a\\x02 Wa\\x02 a\\x01\\xf7V[\\x92\\x91PPV[\\x81\\x81\\x03\\x81\\x81\\x11\\x15a\\x02 Wa\\x02 a\\x01\\xf7V\\xfe\\xa2dipfsX\\\"\\x12 \\x12\\xa7\\xee\\x81\\x95r\\x8a\\xce4\\x9c\\xde\\xc9\\f\\x1f\\xe0'\\x80n*uLb\\xd7\\x12\\x8b\\x07\\xe01\\\\\\xe7\\x84\\xf4dsolcC\\x00\\x08\\x11\\x003\\xa2dipfsX\\\"\\x12 \\xee\\xcd\\x9c\\x18\\xdd;BG\\xedVh\\xbe\\xa0\\xda\\x93\\xc8\\x890\\xa2RT\\xf5\\x9e~-\\xf0Crr\\xd4\\\\KdsolcC\\x00\\x08\\x11\\x003\"","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<storage>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_ACCT_STORAGE","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Map"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<origStorage>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_DotVar3","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Map"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<nonce>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_ACCOUNTS_INIT","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"AccountCellMap"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<txOrder>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_TXORDER_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"List"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<txPending>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_TXPENDING_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"List"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<messages>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_MESSAGES_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"MessageCellMap"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<cheatcodes>","params":[]},"arity":1,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<prank>","params":[]},"arity":6,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<prevCaller>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_PREVCALLER_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Account"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<prevOrigin>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_PREVORIGIN_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Account"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<newCaller>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_NEWCALLER_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Account"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<newOrigin>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_NEWORIGIN_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Account"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<depth>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_DEPTH_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<singleCall>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_SINGLECALL_CELL","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Bool"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"<generatedCounter>","params":[]},"arity":1,"args":[{"node":"KVariable","name":"_DotVar2","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Int"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#lookup(_,_)_EVM-TYPES_Int_Map_Int","params":[]},"arity":2,"args":[{"node":"KVariable","name":"CHEATCODE_STORAGE","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Map"}}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"46308022326495007027972728677917914892729792999299745830475596687180801507328","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"false","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"AccountCellMap:in_keys","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"120209876281281145568259943","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_ACCOUNTS_INIT","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"AccountCellMap"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"false","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"AccountCellMap:in_keys","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"137122462167341575662000267002353578582749290296","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_ACCOUNTS_INIT","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"AccountCellMap"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"false","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"AccountCellMap:in_keys","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_ACCOUNTS_INIT","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"AccountCellMap"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"false","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"AccountCellMap:in_keys","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"645326474426547203313410069153905908525362434349","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_ACCOUNTS_INIT","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"AccountCellMap"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"false","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"AccountCellMap:in_keys","params":[]},"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<acctID>","params":[]},"arity":1,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1032069922050249630382865877677304880282300743300","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_ACCOUNTS_INIT","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"AccountCellMap"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"true","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_<=Int_","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_VV0_from_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"true","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_<=Int_","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_VV1_to_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"true","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_<=Int_","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0","att":{"node":"KAtt","att":{}}},{"node":"KVariable","name":"_VV2_amount_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"true","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_<Int_","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"19999999999999840330","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"Csstore(_,_,_,_)_EVM_Int_Schedule_Int_Int_Int","params":[]},"arity":4,"args":[{"node":"KApply","label":{"node":"KLabel","name":"LONDON_EVM","params":[]},"arity":0,"args":[],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_|Int_","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"368263281805664599098893944405654396525700029268","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_&Int_","params":[]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"115792089237316195423570985007226406215939081747436879206741300988257197096960","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#lookup(_,_)_EVM-TYPES_Int_Map_Int","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_ACCT_STORAGE","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Map"}}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"8","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#lookup(_,_)_EVM-TYPES_Int_Map_Int","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_ACCT_STORAGE","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Map"}}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"8","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#lookup(_,_)_EVM-TYPES_Int_Map_Int","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_DotVar3","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Map"}}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"8","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"true","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_<Int_","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_VV0_from_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1461501637330902918203684832716283019655932542976","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"true","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_<Int_","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_VV1_to_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"1461501637330902918203684832716283019655932542976","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"Bool"},{"node":"KSort","name":"GeneratedTopCell"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Bool"},"token":"true","att":{"node":"KAtt","att":{}}},{"node":"KApply","label":{"node":"KLabel","name":"_<Int_","params":[]},"arity":2,"args":[{"node":"KVariable","name":"_VV2_amount_3c5818c8","att":{"node":"KAtt","att":{"org.kframework.kore.Sort":{"node":"KSort","name":"Int"}}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"115792089237316195423570985008687907853269984665640564039457584007913129639936","att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}],"att":{"node":"KAtt","att":{}}}}
[Error] Prover: backend terminated because the configuration cannot be
rewritten further. See output for more details.
You have probably also seen this. I'm just putting it here in case it could be helpful.
@enzoevers Thanks! We are aware of some issues with gas computations, and we're currently investigating which solution to implement. In the meantime, you can try to disable all gas checks using the infinite-gas
-branch from this PR: https://github.com/runtimeverification/evm-semantics/pull/1520
With this branch, you're basically telling KEVM, "Always assume I have enough gas".
So the final output means that execution has halted (there are no more rewrites) but there is still some condition that isn't met -- in my experience it usually means there is a branch that should have been pruned but wasn't. Could you run this and give us the output:
kevm foundry-show out TokenTest.testTransfer
@ehildenb also just made some significant updates to the instructions for running and exploring the execution of the prover, see this PR: https://github.com/runtimeverification/foundry-demo/pull/5/files
This explains how you can look for, in neater ways, what is failing.
Thank you for the tips. I will generate the output. But first I have to update my K/Kevm version (using kup). Currently I am using the last release of KEVM (v1.0.1-0539c0cc) but this doesn't have the foundry-show
command yet. So I will come back to this.
Thanks, please keep us in the loop! And feel free to ask any K questions not directly related to this on Discord, Matrix or Stack Overflow (links here: https://kframework.org/index.html)
Versions (in a docker container):
foundry-demo repo commit: 5aa1943
It was verified that the test itself passes with forge:
In
doit
simplify_init
was swapped due to the errorpython3 -m kevm_pyk: error: unrecognized arguments: --no-simplify-init
Note that the default test in
doit
(test=Examples.test_assert_bool_failing
) passes. So it seems that the k and foundry installation is correct?When adding
test=TokenTest.testTransfer
(and commenting out the other tests) in thedoit
file, an error in the process is given (see the first log below). The main problem I thought was related toWARNING 2023-02-03 07:10:28,496 kevm_pyk.solc_to_k - Could not find member 'storageLayout' while processing contract
. After adding--extra-output storageLayout
to theforge build
command indoit
this error is no longer shown, but the verification still fails (see the second log).Default (without
--extra-output storageLayout
):Using
--extra-output storageLayout
: