Skip to content

Instantly share code, notes, and snippets.

@MrChico
Created June 20, 2018 20:28
Show Gist options
  • Save MrChico/9e401e90c8302b4368878fcc8ffc9e0f to your computer and use it in GitHub Desktop.
Save MrChico/9e401e90c8302b4368878fcc8ffc9e0f to your computer and use it in GitHub Desktop.
{
"format":"KAST",
"version":1,
"term":{
"node":"KApply",
"label":"<generatedTop>",
"variable":false,
"arity":6,
"args":[
{
"node":"KApply",
"label":"<k>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"#exceptional? [ PUSH ( 1 , 64 ) ] ~> #load [ PUSH ( 1 , 64 ) ] ~> #exec [ PUSH ( 1 , 64 ) ] ~> #pc [ PUSH ( 1 , 64 ) ] ~> #execute"
}
]
},
{
"node":"KApply",
"label":"<exit-code>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"Int",
"token":"1"
}
]
},
{
"node":"KApply",
"label":"<mode>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"NORMAL"
}
]
},
{
"node":"KApply",
"label":"<schedule>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"BYZANTIUM"
}
]
},
{
"node":"KApply",
"label":"<analysis>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":".Map"
}
]
},
{
"node":"KApply",
"label":"<ethereum>",
"variable":false,
"arity":2,
"args":[
{
"node":"KApply",
"label":"<evm>",
"variable":false,
"arity":26,
"args":[
{
"node":"KApply",
"label":"<output>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1079._1227:WordStack"
}
]
},
{
"node":"KApply",
"label":"<statusCode>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1080._1228:StatusCode"
}
]
},
{
"node":"KApply",
"label":"<callStack>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1081._1229:List"
}
]
},
{
"node":"KApply",
"label":"<interimStates>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1082._1230:List"
}
]
},
{
"node":"KApply",
"label":"<touchedAccounts>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1083._1231:Set"
}
]
},
{
"node":"KApply",
"label":"<callState>",
"variable":false,
"arity":14,
"args":[
{
"node":"KApply",
"label":"<program>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"0 |-> PUSH ( 1 , 128 )\n2 |-> PUSH ( 1 , 64 )\n4 |-> MSTORE\n5 |-> PUSH ( 1 , 4 )\n7 |-> CALLDATASIZE\n8 |-> LT\n9 |-> PUSH ( 1 , 63 )\n11 |-> JUMPI\n12 |-> PUSH ( 1 , 0 )\n14 |-> CALLDATALOAD\n15 |-> PUSH ( 29 , 26959946667150639794667015087019630673637144422540572481103610249216 )\n45 |-> SWAP ( 1 )\n46 |-> DIV\n47 |-> PUSH ( 4 , 4294967295 )\n52 |-> AND\n53 |-> DUP ( 1 )\n54 |-> PUSH ( 4 , 1997931255 )\n59 |-> EQ\n60 |-> PUSH ( 1 , 68 )\n62 |-> JUMPI\n63 |-> JUMPDEST\n64 |-> PUSH ( 1 , 0 )\n66 |-> DUP ( 1 )\n67 |-> REVERT\n68 |-> JUMPDEST\n69 |-> CALLVALUE\n70 |-> DUP ( 1 )\n71 |-> ISZERO\n72 |-> PUSH ( 1 , 79 )\n74 |-> JUMPI\n75 |-> PUSH ( 1 , 0 )\n77 |-> DUP ( 1 )\n78 |-> REVERT\n79 |-> JUMPDEST\n80 |-> POP\n81 |-> PUSH ( 1 , 118 )\n83 |-> PUSH ( 1 , 4 )\n85 |-> DUP ( 1 )\n86 |-> CALLDATASIZE\n87 |-> SUB\n88 |-> DUP ( 2 )\n89 |-> ADD\n90 |-> SWAP ( 1 )\n91 |-> DUP ( 1 )\n92 |-> DUP ( 1 )\n93 |-> CALLDATALOAD\n94 |-> SWAP ( 1 )\n95 |-> PUSH ( 1 , 32 )\n97 |-> ADD\n98 |-> SWAP ( 1 )\n99 |-> SWAP ( 3 )\n100 |-> SWAP ( 2 )\n101 |-> SWAP ( 1 )\n102 |-> DUP ( 1 )\n103 |-> CALLDATALOAD\n104 |-> SWAP ( 1 )\n105 |-> PUSH ( 1 , 32 )\n107 |-> ADD\n108 |-> SWAP ( 1 )\n109 |-> SWAP ( 3 )\n110 |-> SWAP ( 2 )\n111 |-> SWAP ( 1 )\n112 |-> POP\n113 |-> POP\n114 |-> POP\n115 |-> PUSH ( 1 , 140 )\n117 |-> JUMP\n118 |-> JUMPDEST\n119 |-> PUSH ( 1 , 64 )\n121 |-> MLOAD\n122 |-> DUP ( 1 )\n123 |-> DUP ( 3 )\n124 |-> DUP ( 2 )\n125 |-> MSTORE\n126 |-> PUSH ( 1 , 32 )\n128 |-> ADD\n129 |-> SWAP ( 2 )\n130 |-> POP\n131 |-> POP\n132 |-> PUSH ( 1 , 64 )\n134 |-> MLOAD\n135 |-> DUP ( 1 )\n136 |-> SWAP ( 2 )\n137 |-> SUB\n138 |-> SWAP ( 1 )\n139 |-> RETURN\n140 |-> JUMPDEST\n141 |-> PUSH ( 1 , 0 )\n143 |-> DUP ( 3 )\n144 |-> DUP ( 3 )\n145 |-> DUP ( 5 )\n146 |-> ADD\n147 |-> SWAP ( 2 )\n148 |-> POP\n149 |-> DUP ( 2 )\n150 |-> LT\n151 |-> ISZERO\n152 |-> ISZERO\n153 |-> ISZERO\n154 |-> PUSH ( 1 , 161 )\n156 |-> JUMPI\n157 |-> PUSH ( 1 , 0 )\n159 |-> DUP ( 1 )\n160 |-> REVERT\n161 |-> JUMPDEST\n162 |-> SWAP ( 3 )\n163 |-> SWAP ( 2 )\n164 |-> POP\n165 |-> POP\n166 |-> JUMP\n167 |-> STOP\n168 |-> LOG ( 1 )\n169 |-> PUSH ( 6 , 108278179835992 )\n176 |-> SHA3\n177 |-> LOG ( 3 )\n178 |-> ADD\n179 |-> UNDEFINED ( 33 )\n180 |-> PUSH ( 5 , 69781312742 )\n186 |-> GAS\n187 |-> AND\n188 |-> MSTORE8\n189 |-> RETURNDATASIZE\n190 |-> UNDEFINED ( 29 )\n191 |-> UNDEFINED ( 199 )\n192 |-> UNDEFINED ( 230 )\n193 |-> SLT\n194 |-> PUSH ( 14 , 2115412185022989223725417212049535 )\n209 |-> STOP\n210 |-> UNDEFINED ( 41 )"
}
]
},
{
"node":"KApply",
"label":"<programBytes>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"96 : 128 : 96 : 64 : 82 : 96 : 4 : 54 : 16 : 96 : 63 : 87 : 96 : 0 : 53 : 124 : 1 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 144 : 4 : 99 : 255 : 255 : 255 : 255 : 22 : 128 : 99 : 119 : 22 : 2 : 247 : 20 : 96 : 68 : 87 : 91 : 96 : 0 : 128 : 253 : 91 : 52 : 128 : 21 : 96 : 79 : 87 : 96 : 0 : 128 : 253 : 91 : 80 : 96 : 118 : 96 : 4 : 128 : 54 : 3 : 129 : 1 : 144 : 128 : 128 : 53 : 144 : 96 : 32 : 1 : 144 : 146 : 145 : 144 : 128 : 53 : 144 : 96 : 32 : 1 : 144 : 146 : 145 : 144 : 80 : 80 : 80 : 96 : 140 : 86 : 91 : 96 : 64 : 81 : 128 : 130 : 129 : 82 : 96 : 32 : 1 : 145 : 80 : 80 : 96 : 64 : 81 : 128 : 145 : 3 : 144 : 243 : 91 : 96 : 0 : 130 : 130 : 132 : 1 : 145 : 80 : 129 : 16 : 21 : 21 : 21 : 96 : 161 : 87 : 96 : 0 : 128 : 253 : 91 : 146 : 145 : 80 : 80 : 86 : 0 : 161 : 101 : 98 : 122 : 122 : 114 : 48 : 88 : 32 : 163 : 1 : 33 : 100 : 16 : 63 : 74 : 84 : 230 : 90 : 22 : 83 : 61 : 29 : 199 : 230 : 18 : 109 : 104 : 76 : 65 : 107 : 2 : 107 : 163 : 155 : 168 : 49 : 44 : 58 : 120 : 127 : 0 : 41 : .WordStack"
}
]
},
{
"node":"KApply",
"label":"<id>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"ACCT_ID._1223:Int"
}
]
},
{
"node":"KApply",
"label":"<caller>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"CALLER_ID._1269:Int"
}
]
},
{
"node":"KApply",
"label":"<callData>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"119 : 22 : 2 : 247 : nthbyteof ( X._1225:Int , 0 , 32 ) : nthbyteof ( X._1225:Int , 1 , 32 ) : nthbyteof ( X._1225:Int , 2 , 32 ) : nthbyteof ( X._1225:Int , 3 , 32 ) : nthbyteof ( X._1225:Int , 4 , 32 ) : nthbyteof ( X._1225:Int , 5 , 32 ) : nthbyteof ( X._1225:Int , 6 , 32 ) : nthbyteof ( X._1225:Int , 7 , 32 ) : nthbyteof ( X._1225:Int , 8 , 32 ) : nthbyteof ( X._1225:Int , 9 , 32 ) : nthbyteof ( X._1225:Int , 10 , 32 ) : nthbyteof ( X._1225:Int , 11 , 32 ) : nthbyteof ( X._1225:Int , 12 , 32 ) : nthbyteof ( X._1225:Int , 13 , 32 ) : nthbyteof ( X._1225:Int , 14 , 32 ) : nthbyteof ( X._1225:Int , 15 , 32 ) : nthbyteof ( X._1225:Int , 16 , 32 ) : nthbyteof ( X._1225:Int , 17 , 32 ) : nthbyteof ( X._1225:Int , 18 , 32 ) : nthbyteof ( X._1225:Int , 19 , 32 ) : nthbyteof ( X._1225:Int , 20 , 32 ) : nthbyteof ( X._1225:Int , 21 , 32 ) : nthbyteof ( X._1225:Int , 22 , 32 ) : nthbyteof ( X._1225:Int , 23 , 32 ) : nthbyteof ( X._1225:Int , 24 , 32 ) : nthbyteof ( X._1225:Int , 25 , 32 ) : nthbyteof ( X._1225:Int , 26 , 32 ) : nthbyteof ( X._1225:Int , 27 , 32 ) : nthbyteof ( X._1225:Int , 28 , 32 ) : nthbyteof ( X._1225:Int , 29 , 32 ) : nthbyteof ( X._1225:Int , 30 , 32 ) : nthbyteof ( X._1225:Int , 31 , 32 ) : nthbyteof ( Y._1226:Int , 0 , 32 ) : nthbyteof ( Y._1226:Int , 1 , 32 ) : nthbyteof ( Y._1226:Int , 2 , 32 ) : nthbyteof ( Y._1226:Int , 3 , 32 ) : nthbyteof ( Y._1226:Int , 4 , 32 ) : nthbyteof ( Y._1226:Int , 5 , 32 ) : nthbyteof ( Y._1226:Int , 6 , 32 ) : nthbyteof ( Y._1226:Int , 7 , 32 ) : nthbyteof ( Y._1226:Int , 8 , 32 ) : nthbyteof ( Y._1226:Int , 9 , 32 ) : nthbyteof ( Y._1226:Int , 10 , 32 ) : nthbyteof ( Y._1226:Int , 11 , 32 ) : nthbyteof ( Y._1226:Int , 12 , 32 ) : nthbyteof ( Y._1226:Int , 13 , 32 ) : nthbyteof ( Y._1226:Int , 14 , 32 ) : nthbyteof ( Y._1226:Int , 15 , 32 ) : nthbyteof ( Y._1226:Int , 16 , 32 ) : nthbyteof ( Y._1226:Int , 17 , 32 ) : nthbyteof ( Y._1226:Int , 18 , 32 ) : nthbyteof ( Y._1226:Int , 19 , 32 ) : nthbyteof ( Y._1226:Int , 20 , 32 ) : nthbyteof ( Y._1226:Int , 21 , 32 ) : nthbyteof ( Y._1226:Int , 22 , 32 ) : nthbyteof ( Y._1226:Int , 23 , 32 ) : nthbyteof ( Y._1226:Int , 24 , 32 ) : nthbyteof ( Y._1226:Int , 25 , 32 ) : nthbyteof ( Y._1226:Int , 26 , 32 ) : nthbyteof ( Y._1226:Int , 27 , 32 ) : nthbyteof ( Y._1226:Int , 28 , 32 ) : nthbyteof ( Y._1226:Int , 29 , 32 ) : nthbyteof ( Y._1226:Int , 30 , 32 ) : nthbyteof ( Y._1226:Int , 31 , 32 ) : .WordStack"
}
]
},
{
"node":"KApply",
"label":"<callValue>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"0"
}
]
},
{
"node":"KApply",
"label":"<wordStack>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"128 : .WordStack"
}
]
},
{
"node":"KApply",
"label":"<localMem>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":".Map"
}
]
},
{
"node":"KApply",
"label":"<pc>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"2"
}
]
},
{
"node":"KApply",
"label":"<gas>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"G._1224:Int -Int 3"
}
]
},
{
"node":"KApply",
"label":"<memoryUsed>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"0"
}
]
},
{
"node":"KApply",
"label":"<previousGas>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"G._1224:Int"
}
]
},
{
"node":"KApply",
"label":"<static>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"false"
}
]
},
{
"node":"KApply",
"label":"<callDepth>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1092._1240:Int"
}
]
}
]
},
{
"node":"KApply",
"label":"<substate>",
"variable":false,
"arity":3,
"args":[
{
"node":"KApply",
"label":"<selfDestruct>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1093._1241:Set"
}
]
},
{
"node":"KApply",
"label":"<log>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1094._1242:List"
}
]
},
{
"node":"KApply",
"label":"<refund>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1095._1243:Int"
}
]
}
]
},
{
"node":"KApply",
"label":"<gasPrice>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1096._1244:Int"
}
]
},
{
"node":"KApply",
"label":"<origin>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"ORIGIN_ID._1221:Int"
}
]
},
{
"node":"KApply",
"label":"<previousHash>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1097._1245:Int"
}
]
},
{
"node":"KApply",
"label":"<ommersHash>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1098._1246:Int"
}
]
},
{
"node":"KApply",
"label":"<coinbase>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1099._1247:Int"
}
]
},
{
"node":"KApply",
"label":"<stateRoot>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1100._1248:Int"
}
]
},
{
"node":"KApply",
"label":"<transactionsRoot>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1101._1249:Int"
}
]
},
{
"node":"KApply",
"label":"<receiptsRoot>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1102._1250:Int"
}
]
},
{
"node":"KApply",
"label":"<logsBloom>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1103._1251:WordStack"
}
]
},
{
"node":"KApply",
"label":"<difficulty>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1104._1252:Int"
}
]
},
{
"node":"KApply",
"label":"<number>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1105._1253:Int"
}
]
},
{
"node":"KApply",
"label":"<gasLimit>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1106._1254:Int"
}
]
},
{
"node":"KApply",
"label":"<gasUsed>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1107._1255:Int"
}
]
},
{
"node":"KApply",
"label":"<timestamp>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1108._1256:Int"
}
]
},
{
"node":"KApply",
"label":"<extraData>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1109._1257:WordStack"
}
]
},
{
"node":"KApply",
"label":"<mixHash>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1110._1258:Int"
}
]
},
{
"node":"KApply",
"label":"<blockNonce>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1111._1259:Int"
}
]
},
{
"node":"KApply",
"label":"<ommerBlockHeaders>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1112._1260:JSON"
}
]
},
{
"node":"KApply",
"label":"<blockhash>",
"variable":false,
"arity":1,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"_1113._1261:List"
}
]
}
]
},
{
"node":"KApply",
"label":"<network>",
"variable":false,
"arity":5,
"args":[
{
"node":"KToken",
"sort":"K",
"token":"<activeAccounts>\n SetItem ( ACCT_ID._1223:Int )\n _1114._1262:Set\n</activeAccounts>"
},
{
"node":"KToken",
"sort":"K",
"token":"<accounts>\n <acctID>\n ACCT_ID._1223:Int\n </acctID> |-> <account>\n <acctID>\n ACCT_ID._1223:Int\n </acctID>\n <balance>\n _1115._1263:Int\n </balance>\n <code>\n 96 : 128 : 96 : 64 : 82 : 96 : 4 : 54 : 16 : 96 : 63 : 87 : 96 : 0 : 53 : 124 : 1 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 144 : 4 : 99 : 255 : 255 : 255 : 255 : 22 : 128 : 99 : 119 : 22 : 2 : 247 : 20 : 96 : 68 : 87 : 91 : 96 : 0 : 128 : 253 : 91 : 52 : 128 : 21 : 96 : 79 : 87 : 96 : 0 : 128 : 253 : 91 : 80 : 96 : 118 : 96 : 4 : 128 : 54 : 3 : 129 : 1 : 144 : 128 : 128 : 53 : 144 : 96 : 32 : 1 : 144 : 146 : 145 : 144 : 128 : 53 : 144 : 96 : 32 : 1 : 144 : 146 : 145 : 144 : 80 : 80 : 80 : 96 : 140 : 86 : 91 : 96 : 64 : 81 : 128 : 130 : 129 : 82 : 96 : 32 : 1 : 145 : 80 : 80 : 96 : 64 : 81 : 128 : 145 : 3 : 144 : 243 : 91 : 96 : 0 : 130 : 130 : 132 : 1 : 145 : 80 : 129 : 16 : 21 : 21 : 21 : 96 : 161 : 87 : 96 : 0 : 128 : 253 : 91 : 146 : 145 : 80 : 80 : 86 : 0 : 161 : 101 : 98 : 122 : 122 : 114 : 48 : 88 : 32 : 163 : 1 : 33 : 100 : 16 : 63 : 74 : 84 : 230 : 90 : 22 : 83 : 61 : 29 : 199 : 230 : 18 : 109 : 104 : 76 : 65 : 107 : 2 : 107 : 163 : 155 : 168 : 49 : 44 : 58 : 120 : 127 : 0 : 41 : .WordStack\n </code>\n <storage>\n _1116._1264:Map\n </storage>\n <nonce>\n _1117._1265:Int\n </nonce>\n </account>\n DotVar1._1222:Map\n</accounts>"
},
{
"node":"KToken",
"sort":"K",
"token":"<txOrder>\n _1118._1266:List\n</txOrder>"
},
{
"node":"KToken",
"sort":"K",
"token":"<txPending>\n _1119._1267:List\n</txPending>"
},
{
"node":"KToken",
"sort":"K",
"token":"<messages>\n _1120._1268:Map\n</messages>"
}
]
}
]
}
]
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment