diff --git a/Dockerfile b/Dockerfile index 78dc2cc053..97a3ea16a3 100644 --- a/Dockerfile +++ b/Dockerfile @@ -43,5 +43,18 @@ ADD --chown=user:user deps/k/haskell-backend/src/main/native/haskell-backend/kor RUN cd /home/user/.tmp-haskell \ && stack build --only-snapshot +ADD deps/k/pom.xml /home/user/.tmp-maven/ +ADD deps/k/ktree/pom.xml /home/user/.tmp-maven/ktree/ +ADD deps/k/llvm-backend/pom.xml /home/user/.tmp-maven/llvm-backend/ +ADD deps/k/llvm-backend/src/main/native/llvm-backend/matching/pom.xml /home/user/.tmp-maven/llvm-backend/src/main/native/llvm-backend/matching/ +ADD deps/k/haskell-backend/pom.xml /home/user/.tmp-maven/haskell-backend/ +ADD deps/k/ocaml-backend/pom.xml /home/user/.tmp-maven/ocaml-backend/ +ADD deps/k/kernel/pom.xml /home/user/.tmp-maven/kernel/ +ADD deps/k/java-backend/pom.xml /home/user/.tmp-maven/java-backend/ +ADD deps/k/k-distribution/pom.xml /home/user/.tmp-maven/k-distribution/ +ADD deps/k/kore/pom.xml /home/user/.tmp-maven/kore/ +RUN cd /home/user/.tmp-maven \ + && mvn dependency:go-offline + ENV LD_LIBRARY_PATH=/usr/local/lib ENV PATH=/home/user/.local/bin:/home/user/.cargo/bin:$PATH diff --git a/Makefile b/Makefile index 4cd718804d..abff96d1af 100644 --- a/Makefile +++ b/Makefile @@ -175,7 +175,7 @@ concrete_tangle:=.k:not(.node):not(.symbolic),.standalone,.concrete symbolic_tangle:=.k:not(.node):not(.concrete),.standalone,.symbolic node_tangle:=.k:not(.standalone):not(.symbolic),.node,.concrete -k_files=driver.k data.k network.k evm.k krypto.k edsl.k evm-node.k web3.k +k_files=driver.k data.k network.k evm.k krypto.k edsl.k evm-node.k web3.k asm.k EXTRA_K_FILES+=$(MAIN_DEFN_FILE).k ALL_K_FILES:=$(k_files) $(EXTRA_K_FILES) diff --git a/asm.md b/asm.md new file mode 100644 index 0000000000..456f102d78 --- /dev/null +++ b/asm.md @@ -0,0 +1,189 @@ +Ethereum Assembler +================== + +This file contains an assembler from EVM opcodes to byte strings. + +Note that due to the design of EVM, which depends on the binary representation of a smart contract, it is **not** the case that disassembling and then reassembling the same contract will yield the same sequence of bytes. +As a simple counterexample, consider the contract `0x60`. +Disassembling and then reassembling this contract will yield `0x6000`. + +As such, assembly is not considered part of the semantics of EVM, but is provided merely as a sample implementation to ease readability and make it easier to write inputs to the KEVM semantics. + +```k +module EVM-ASSEMBLY + imports EVM + + syntax OpCode ::= PUSH(Int, Int) [klabel(PUSHAsm)] + // -------------------------------------------------- + + syntax ByteArray ::= #asmOpCodes ( OpCodes ) [function] + // ------------------------------------------------------- +``` + +```{.k .symbolic} + syntax ByteArray ::= #asmOpCodes ( OpCodes, ByteArray ) [function, klabel(#asmOpCodesAux)] + // ------------------------------------------------------------------------------------------ + rule #asmOpCodes( OPS ) => #asmOpCodes(#revOps(OPS), .ByteArray) + + rule #asmOpCodes( PUSH(N, W) ; OCS, WS ) => #asmOpCodes(OCS, #asmOpCode(PUSH(N)) : {#padToWidth(N, #asByteStack(W)) ++ WS}:>WordStack) + rule #asmOpCodes( OP ; OCS, WS ) => #asmOpCodes(OCS, #asmOpCode(OP) : WS) requires PUSH(_, _) :/=K OP + rule #asmOpCodes( .OpCodes, WS ) => WS +``` + +```{.k .concrete} + syntax ByteArray ::= #asmOpCodes ( OpCodes, StringBuffer ) [function, klabel(#asmOpCodesAux)] + // --------------------------------------------------------------------------------------------- + rule #asmOpCodes( OPS ) => #asmOpCodes(OPS, .StringBuffer) + + rule #asmOpCodes( PUSH(N, W) ; OCS, SB ) => #asmOpCodes(OCS, (SB +String chrChar(#asmOpCode(PUSH(N)))) +String Bytes2String(Int2Bytes(N, W, BE))) + rule #asmOpCodes( OP ; OCS, SB ) => #asmOpCodes(OCS, SB +String chrChar(#asmOpCode(OP))) [owise] + rule #asmOpCodes( .OpCodes, SB ) => String2Bytes(StringBuffer2String(SB)) +``` + +```k + syntax Int ::= #asmOpCode ( OpCode ) [function] + // ----------------------------------------------- + rule #asmOpCode( STOP ) => 0 + rule #asmOpCode( ADD ) => 1 + rule #asmOpCode( MUL ) => 2 + rule #asmOpCode( SUB ) => 3 + rule #asmOpCode( DIV ) => 4 + rule #asmOpCode( SDIV ) => 5 + rule #asmOpCode( MOD ) => 6 + rule #asmOpCode( SMOD ) => 7 + rule #asmOpCode( ADDMOD ) => 8 + rule #asmOpCode( MULMOD ) => 9 + rule #asmOpCode( EXP ) => 10 + rule #asmOpCode( SIGNEXTEND ) => 11 + rule #asmOpCode( LT ) => 16 + rule #asmOpCode( GT ) => 17 + rule #asmOpCode( SLT ) => 18 + rule #asmOpCode( SGT ) => 19 + rule #asmOpCode( EQ ) => 20 + rule #asmOpCode( ISZERO ) => 21 + rule #asmOpCode( AND ) => 22 + rule #asmOpCode( EVMOR ) => 23 + rule #asmOpCode( XOR ) => 24 + rule #asmOpCode( NOT ) => 25 + rule #asmOpCode( BYTE ) => 26 + rule #asmOpCode( SHL ) => 27 + rule #asmOpCode( SHR ) => 28 + rule #asmOpCode( SAR ) => 29 + rule #asmOpCode( SHA3 ) => 32 + rule #asmOpCode( ADDRESS ) => 48 + rule #asmOpCode( BALANCE ) => 49 + rule #asmOpCode( ORIGIN ) => 50 + rule #asmOpCode( CALLER ) => 51 + rule #asmOpCode( CALLVALUE ) => 52 + rule #asmOpCode( CALLDATALOAD ) => 53 + rule #asmOpCode( CALLDATASIZE ) => 54 + rule #asmOpCode( CALLDATACOPY ) => 55 + rule #asmOpCode( CODESIZE ) => 56 + rule #asmOpCode( CODECOPY ) => 57 + rule #asmOpCode( GASPRICE ) => 58 + rule #asmOpCode( EXTCODESIZE ) => 59 + rule #asmOpCode( EXTCODECOPY ) => 60 + rule #asmOpCode( RETURNDATASIZE ) => 61 + rule #asmOpCode( RETURNDATACOPY ) => 62 + rule #asmOpCode( EXTCODEHASH ) => 63 + rule #asmOpCode( BLOCKHASH ) => 64 + rule #asmOpCode( COINBASE ) => 65 + rule #asmOpCode( TIMESTAMP ) => 66 + rule #asmOpCode( NUMBER ) => 67 + rule #asmOpCode( DIFFICULTY ) => 68 + rule #asmOpCode( GASLIMIT ) => 69 + rule #asmOpCode( POP ) => 80 + rule #asmOpCode( MLOAD ) => 81 + rule #asmOpCode( MSTORE ) => 82 + rule #asmOpCode( MSTORE8 ) => 83 + rule #asmOpCode( SLOAD ) => 84 + rule #asmOpCode( SSTORE ) => 85 + rule #asmOpCode( JUMP ) => 86 + rule #asmOpCode( JUMPI ) => 87 + rule #asmOpCode( PC ) => 88 + rule #asmOpCode( MSIZE ) => 89 + rule #asmOpCode( GAS ) => 90 + rule #asmOpCode( JUMPDEST ) => 91 + rule #asmOpCode( PUSH(1) ) => 96 + rule #asmOpCode( PUSH(2) ) => 97 + rule #asmOpCode( PUSH(3) ) => 98 + rule #asmOpCode( PUSH(4) ) => 99 + rule #asmOpCode( PUSH(5) ) => 100 + rule #asmOpCode( PUSH(6) ) => 101 + rule #asmOpCode( PUSH(7) ) => 102 + rule #asmOpCode( PUSH(8) ) => 103 + rule #asmOpCode( PUSH(9) ) => 104 + rule #asmOpCode( PUSH(10) ) => 105 + rule #asmOpCode( PUSH(11) ) => 106 + rule #asmOpCode( PUSH(12) ) => 107 + rule #asmOpCode( PUSH(13) ) => 108 + rule #asmOpCode( PUSH(14) ) => 109 + rule #asmOpCode( PUSH(15) ) => 110 + rule #asmOpCode( PUSH(16) ) => 111 + rule #asmOpCode( PUSH(17) ) => 112 + rule #asmOpCode( PUSH(18) ) => 113 + rule #asmOpCode( PUSH(19) ) => 114 + rule #asmOpCode( PUSH(20) ) => 115 + rule #asmOpCode( PUSH(21) ) => 116 + rule #asmOpCode( PUSH(22) ) => 117 + rule #asmOpCode( PUSH(23) ) => 118 + rule #asmOpCode( PUSH(24) ) => 119 + rule #asmOpCode( PUSH(25) ) => 120 + rule #asmOpCode( PUSH(26) ) => 121 + rule #asmOpCode( PUSH(27) ) => 122 + rule #asmOpCode( PUSH(28) ) => 123 + rule #asmOpCode( PUSH(29) ) => 124 + rule #asmOpCode( PUSH(30) ) => 125 + rule #asmOpCode( PUSH(31) ) => 126 + rule #asmOpCode( PUSH(32) ) => 127 + rule #asmOpCode( DUP(1) ) => 128 + rule #asmOpCode( DUP(2) ) => 129 + rule #asmOpCode( DUP(3) ) => 130 + rule #asmOpCode( DUP(4) ) => 131 + rule #asmOpCode( DUP(5) ) => 132 + rule #asmOpCode( DUP(6) ) => 133 + rule #asmOpCode( DUP(7) ) => 134 + rule #asmOpCode( DUP(8) ) => 135 + rule #asmOpCode( DUP(9) ) => 136 + rule #asmOpCode( DUP(10) ) => 137 + rule #asmOpCode( DUP(11) ) => 138 + rule #asmOpCode( DUP(12) ) => 139 + rule #asmOpCode( DUP(13) ) => 140 + rule #asmOpCode( DUP(14) ) => 141 + rule #asmOpCode( DUP(15) ) => 142 + rule #asmOpCode( DUP(16) ) => 143 + rule #asmOpCode( SWAP(1) ) => 144 + rule #asmOpCode( SWAP(2) ) => 145 + rule #asmOpCode( SWAP(3) ) => 146 + rule #asmOpCode( SWAP(4) ) => 147 + rule #asmOpCode( SWAP(5) ) => 148 + rule #asmOpCode( SWAP(6) ) => 149 + rule #asmOpCode( SWAP(7) ) => 150 + rule #asmOpCode( SWAP(8) ) => 151 + rule #asmOpCode( SWAP(9) ) => 152 + rule #asmOpCode( SWAP(10) ) => 153 + rule #asmOpCode( SWAP(11) ) => 154 + rule #asmOpCode( SWAP(12) ) => 155 + rule #asmOpCode( SWAP(13) ) => 156 + rule #asmOpCode( SWAP(14) ) => 157 + rule #asmOpCode( SWAP(15) ) => 158 + rule #asmOpCode( SWAP(16) ) => 159 + rule #asmOpCode( LOG(0) ) => 160 + rule #asmOpCode( LOG(1) ) => 161 + rule #asmOpCode( LOG(2) ) => 162 + rule #asmOpCode( LOG(3) ) => 163 + rule #asmOpCode( LOG(4) ) => 164 + rule #asmOpCode( CREATE ) => 240 + rule #asmOpCode( CALL ) => 241 + rule #asmOpCode( CALLCODE ) => 242 + rule #asmOpCode( RETURN ) => 243 + rule #asmOpCode( DELEGATECALL ) => 244 + rule #asmOpCode( CREATE2 ) => 245 + rule #asmOpCode( STATICCALL ) => 250 + rule #asmOpCode( REVERT ) => 253 + rule #asmOpCode( INVALID ) => 254 + rule #asmOpCode( SELFDESTRUCT ) => 255 + rule #asmOpCode( UNDEFINED(W) ) => W + +endmodule +``` diff --git a/deps/k b/deps/k index 824ffc8767..677104b8b9 160000 --- a/deps/k +++ b/deps/k @@ -1 +1 @@ -Subproject commit 824ffc8767fb61d63105acffa445e0fa54d205d7 +Subproject commit 677104b8b956b15ab59a1f6953a57aa77bfbd3ee diff --git a/driver.md b/driver.md index 7c5e132d80..1b316e5c9b 100644 --- a/driver.md +++ b/driver.md @@ -10,9 +10,11 @@ requires "evm-node.k" ```k requires "evm.k" +requires "asm.k" module ETHEREUM-SIMULATION imports EVM + imports EVM-ASSEMBLY ``` ```{.k .node} @@ -508,7 +510,7 @@ Here we load the environmental information. rule load "exec" : { "data" : ((DATA:String) => #parseByteStack(DATA)) } ... // ------------------------------------------------------------------------------------- rule load "exec" : { "data" : (DATA:ByteArray) } => . ... _ => DATA - rule load "exec" : { "code" : (CODE:OpCodes) } => . ... _ => #asMapOpCodes(CODE) + rule load "exec" : { "code" : (CODE:OpCodes) } => . ... _ => #asMapOpCodes(#dasmOpCodes(#asmOpCodes(CODE), SCHED)) _ => #asmOpCodes(CODE) SCHED rule load "exec" : { "code" : (CODE:ByteArray) } => . ... _ => #asMapOpCodes(#dasmOpCodes(CODE, SCHED)) _ => CODE SCHED ``` diff --git a/evm.md b/evm.md index c88aa7c96e..aefc51e019 100644 --- a/evm.md +++ b/evm.md @@ -336,7 +336,7 @@ The `#next [_]` operator initiates execution by: syntax Int ::= #stackNeeded ( OpCode ) [function] // ------------------------------------------------- - rule #stackNeeded(PUSH(_, _)) => 0 + rule #stackNeeded(PUSH(_)) => 0 rule #stackNeeded(IOP:InvalidOp) => 0 rule #stackNeeded(NOP:NullStackOp) => 0 rule #stackNeeded(UOP:UnStackOp) => 1 @@ -366,7 +366,7 @@ The `#next [_]` operator initiates execution by: rule #stackAdded(RETURN) => 0 rule #stackAdded(REVERT) => 0 rule #stackAdded(SELFDESTRUCT) => 0 - rule #stackAdded(PUSH(_,_)) => 1 + rule #stackAdded(PUSH(_)) => 1 rule #stackAdded(LOG(_)) => 0 rule #stackAdded(SWAP(N)) => N rule #stackAdded(DUP(N)) => N +Int 1 @@ -515,8 +515,8 @@ The arguments to `PUSH` must be skipped over (as they are inline), and the opcod syntax Int ::= #widthOp ( OpCode ) [function] // --------------------------------------------- - rule #widthOp(PUSH(N, _)) => 1 +Int N - rule #widthOp(OP) => 1 requires notBool isPushOp(OP) + rule #widthOp(PUSH(N)) => 1 +Int N + rule #widthOp(OP) => 1 requires notBool isPushOp(OP) ``` ### Substate Log @@ -831,9 +831,11 @@ Some operators don't calculate anything, they just push the stack around a bit. rule DUP(N) WS:WordStack => #setStack ((WS [ N -Int 1 ]) : WS) ... rule SWAP(N) (W0 : WS) => #setStack ((WS [ N -Int 1 ]) : (WS [ N -Int 1 := W0 ])) ... - syntax PushOp ::= PUSH ( Int , Int ) - // ------------------------------------ - rule PUSH(_, W) => W ~> #push ... + syntax PushOp ::= PUSH ( Int ) + // ------------------------------ + rule PUSH(N) => #asWord(PGM [ PCOUNT +Int 1 .. N ]) ~> #push ... + PCOUNT + PGM ``` ### Local Memory @@ -1224,8 +1226,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d ```k syntax InternalOp ::= "#checkCall" Int Int | "#call" Int Int Int Int Int ByteArray Bool - | "#callWithCode" Int Int Map ByteArray Int Int ByteArray Bool - | "#mkCall" Int Int Map ByteArray Int ByteArray Bool + | "#callWithCode" Int Int Int ByteArray Int Int ByteArray Bool + | "#mkCall" Int Int Int ByteArray Int ByteArray Bool // ---------------------------------------------------------------------------------- rule #checkCall ACCT VALUE => #refund GCALL ~> #pushCallStack ~> #pushWorldState @@ -1252,41 +1254,31 @@ The various `CALL*` (and other inter-contract control flow) operations will be d requires notBool (VALUE >Int BAL orBool CD >=Int 1024) rule #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC - => #callWithCode ACCTFROM ACCTTO (0 |-> #precompiled(ACCTCODE)) .ByteArray VALUE APPVALUE ARGS STATIC - ... - - SCHED - requires ACCTCODE in #precompiledAccounts(SCHED) - - rule #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC - => #callWithCode ACCTFROM ACCTTO #asMapOpCodes(#dasmOpCodes(CODE, SCHED)) CODE VALUE APPVALUE ARGS STATIC + => #callWithCode ACCTFROM ACCTTO ACCTCODE CODE VALUE APPVALUE ARGS STATIC ... - SCHED ACCTCODE CODE ... - requires notBool ACCTCODE in #precompiledAccounts(SCHED) rule #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC - => #callWithCode ACCTFROM ACCTTO .Map .ByteArray VALUE APPVALUE ARGS STATIC + => #callWithCode ACCTFROM ACCTTO ACCTCODE .ByteArray VALUE APPVALUE ARGS STATIC ... ACCTS - SCHED - requires notBool ACCTCODE in #precompiledAccounts(SCHED) andBool notBool ACCTCODE in ACCTS + requires notBool ACCTCODE in ACCTS - rule #callWithCode ACCTFROM ACCTTO CODE BYTES VALUE APPVALUE ARGS STATIC + rule #callWithCode ACCTFROM ACCTTO ACCTCODE BYTES VALUE APPVALUE ARGS STATIC => #pushCallStack ~> #pushWorldState ~> #transferFunds ACCTFROM ACCTTO VALUE - ~> #mkCall ACCTFROM ACCTTO CODE BYTES APPVALUE ARGS STATIC + ~> #mkCall ACCTFROM ACCTTO ACCTCODE BYTES APPVALUE ARGS STATIC ... - rule #mkCall ACCTFROM ACCTTO CODE BYTES APPVALUE ARGS STATIC:Bool - => #initVM ~> #execute + rule #mkCall ACCTFROM ACCTTO ACCTCODE BYTES APPVALUE ARGS STATIC:Bool + => #initVM ~> #precompiled?(ACCTCODE, SCHED) ~> #execute ... CD => CD +Int 1 @@ -1296,10 +1288,16 @@ The various `CALL*` (and other inter-contract control flow) operations will be d _ => GCALL GCALL => 0 _ => ACCTFROM - _ => CODE + _ => #asMapOpCodes(#dasmOpCodes(BYTES, SCHED)) _ => BYTES OLDSTATIC:Bool => OLDSTATIC orBool STATIC ... .Set => SetItem(ACCTFROM) SetItem(ACCTTO) ... + SCHED + + syntax InternalOp ::= "#precompiled?" "(" Int "," Schedule ")" + // -------------------------------------------------------------- + rule #precompiled?(ACCTCODE, SCHED) => #next [ #precompiled(ACCTCODE) ] ... requires ACCTCODE in #precompiledAccounts(SCHED) + rule #precompiled?(ACCTCODE, SCHED) => . ... requires notBool ACCTCODE in #precompiledAccounts(SCHED) syntax KItem ::= "#initVM" // -------------------------- @@ -1941,7 +1939,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, MLOAD _) => Gverylow < SCHED > ... rule #gasExec(SCHED, MSTORE _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, MSTORE8 _ _) => Gverylow < SCHED > ... - rule #gasExec(SCHED, PUSH(_, _)) => Gverylow < SCHED > ... + rule #gasExec(SCHED, PUSH(_)) => Gverylow < SCHED > ... rule #gasExec(SCHED, DUP(_) _) => Gverylow < SCHED > ... rule #gasExec(SCHED, SWAP(_) _) => Gverylow < SCHED > ... @@ -2373,8 +2371,11 @@ After interpreting the strings representing programs as a `WordStack`, it should - `#dasmOpCode` interperets a `Int` as an `OpCode`. ```k - syntax OpCodes ::= #dasmOpCodes ( ByteArray , Schedule ) [function] - // ----------------------------------------------------------------------------- + syntax Int ::= #widthOpCode ( Int ) [function] + syntax OpCodes ::= #dasmOpCodes ( ByteArray , Schedule ) [function] + // ------------------------------------------------------------------- + rule #widthOpCode(W) => W -Int 94 requires W >=Int 96 andBool W <=Int 127 + rule #widthOpCode(_) => 1 [owise] ``` ```{.k .symbolic} @@ -2383,13 +2384,7 @@ After interpreting the strings representing programs as a `WordStack`, it should rule #dasmOpCodes( WS, SCHED ) => #revOps(#dasmOpCodes(.OpCodes, WS, SCHED)) rule #dasmOpCodes( OPS, .WordStack, _ ) => OPS - rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(#dasmOpCode(W, SCHED) ; OPS, WS, SCHED) requires W >=Int 0 andBool W <=Int 95 - rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(#dasmOpCode(W, SCHED) ; OPS, WS, SCHED) requires W >=Int 165 andBool W <=Int 255 - rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(DUP(W -Int 127) ; OPS, WS, SCHED) requires W >=Int 128 andBool W <=Int 143 - rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(SWAP(W -Int 143) ; OPS, WS, SCHED) requires W >=Int 144 andBool W <=Int 159 - rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(LOG(W -Int 160) ; OPS, WS, SCHED) requires W >=Int 160 andBool W <=Int 164 - - rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(PUSH(W -Int 95, #asWord(#take(W -Int 95, WS))) ; OPS, #drop(W -Int 95, WS), SCHED) requires W >=Int 96 andBool W <=Int 127 + rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(#dasmOpCode(W, SCHED) ; OPS, #drop(#widthOpCode(W) -Int 1, WS), SCHED) ``` ```{.k .concrete} @@ -2398,13 +2393,7 @@ After interpreting the strings representing programs as a `WordStack`, it should rule #dasmOpCodes( WS, SCHED ) => #revOps(#dasmOpCodes(.OpCodes, WS, SCHED, 0, #sizeByteArray(WS))) rule #dasmOpCodes( OPS, _ , _ , I , J ) => OPS requires I >=Int J - rule #dasmOpCodes( OPS, WS, SCHED , I , J ) => #dasmOpCodes(#dasmOpCode(WS[I], SCHED) ; OPS, WS, SCHED, I +Int 1, J) requires WS[I] >=Int 0 andBool WS[I] <=Int 95 [owise] - rule #dasmOpCodes( OPS, WS, SCHED , I , J ) => #dasmOpCodes(#dasmOpCode(WS[I], SCHED) ; OPS, WS, SCHED, I +Int 1, J) requires WS[I] >=Int 165 andBool WS[I] <=Int 255 [owise] - rule #dasmOpCodes( OPS, WS, SCHED , I , J ) => #dasmOpCodes(DUP(WS[I] -Int 127) ; OPS, WS, SCHED, I +Int 1, J) requires WS[I] >=Int 128 andBool WS[I] <=Int 143 [owise] - rule #dasmOpCodes( OPS, WS, SCHED , I , J ) => #dasmOpCodes(SWAP(WS[I] -Int 143) ; OPS, WS, SCHED, I +Int 1, J) requires WS[I] >=Int 144 andBool WS[I] <=Int 159 [owise] - rule #dasmOpCodes( OPS, WS, SCHED , I , J ) => #dasmOpCodes(LOG(WS[I] -Int 160) ; OPS, WS, SCHED, I +Int 1, J) requires WS[I] >=Int 160 andBool WS[I] <=Int 164 [owise] - - rule #dasmOpCodes( OPS, WS, SCHED , I , J ) => #dasmOpCodes(PUSH(WS[I] -Int 95, #asWord(WS [ I +Int 1 .. WS[I] -Int 95 ])) ; OPS, WS, SCHED, I +Int WS[I] -Int 94, J) requires WS[I] >=Int 96 andBool WS[I] <=Int 127 [owise] + rule #dasmOpCodes( OPS, WS, SCHED , I , J ) => #dasmOpCodes(#dasmOpCode(WS[I], SCHED) ; OPS, WS, SCHED, I +Int #widthOpCode(WS[I]), J) [owise] ``` ```k @@ -2471,6 +2460,75 @@ After interpreting the strings representing programs as a `WordStack`, it should rule #dasmOpCode( 89, _ ) => MSIZE rule #dasmOpCode( 90, _ ) => GAS rule #dasmOpCode( 91, _ ) => JUMPDEST + rule #dasmOpCode( 96, _ ) => PUSH(1) + rule #dasmOpCode( 97, _ ) => PUSH(2) + rule #dasmOpCode( 98, _ ) => PUSH(3) + rule #dasmOpCode( 99, _ ) => PUSH(4) + rule #dasmOpCode( 100, _ ) => PUSH(5) + rule #dasmOpCode( 101, _ ) => PUSH(6) + rule #dasmOpCode( 102, _ ) => PUSH(7) + rule #dasmOpCode( 103, _ ) => PUSH(8) + rule #dasmOpCode( 104, _ ) => PUSH(9) + rule #dasmOpCode( 105, _ ) => PUSH(10) + rule #dasmOpCode( 106, _ ) => PUSH(11) + rule #dasmOpCode( 107, _ ) => PUSH(12) + rule #dasmOpCode( 108, _ ) => PUSH(13) + rule #dasmOpCode( 109, _ ) => PUSH(14) + rule #dasmOpCode( 110, _ ) => PUSH(15) + rule #dasmOpCode( 111, _ ) => PUSH(16) + rule #dasmOpCode( 112, _ ) => PUSH(17) + rule #dasmOpCode( 113, _ ) => PUSH(18) + rule #dasmOpCode( 114, _ ) => PUSH(19) + rule #dasmOpCode( 115, _ ) => PUSH(20) + rule #dasmOpCode( 116, _ ) => PUSH(21) + rule #dasmOpCode( 117, _ ) => PUSH(22) + rule #dasmOpCode( 118, _ ) => PUSH(23) + rule #dasmOpCode( 119, _ ) => PUSH(24) + rule #dasmOpCode( 120, _ ) => PUSH(25) + rule #dasmOpCode( 121, _ ) => PUSH(26) + rule #dasmOpCode( 122, _ ) => PUSH(27) + rule #dasmOpCode( 123, _ ) => PUSH(28) + rule #dasmOpCode( 124, _ ) => PUSH(29) + rule #dasmOpCode( 125, _ ) => PUSH(30) + rule #dasmOpCode( 126, _ ) => PUSH(31) + rule #dasmOpCode( 127, _ ) => PUSH(32) + rule #dasmOpCode( 128, _ ) => DUP(1) + rule #dasmOpCode( 129, _ ) => DUP(2) + rule #dasmOpCode( 130, _ ) => DUP(3) + rule #dasmOpCode( 131, _ ) => DUP(4) + rule #dasmOpCode( 132, _ ) => DUP(5) + rule #dasmOpCode( 133, _ ) => DUP(6) + rule #dasmOpCode( 134, _ ) => DUP(7) + rule #dasmOpCode( 135, _ ) => DUP(8) + rule #dasmOpCode( 136, _ ) => DUP(9) + rule #dasmOpCode( 137, _ ) => DUP(10) + rule #dasmOpCode( 138, _ ) => DUP(11) + rule #dasmOpCode( 139, _ ) => DUP(12) + rule #dasmOpCode( 140, _ ) => DUP(13) + rule #dasmOpCode( 141, _ ) => DUP(14) + rule #dasmOpCode( 142, _ ) => DUP(15) + rule #dasmOpCode( 143, _ ) => DUP(16) + rule #dasmOpCode( 144, _ ) => SWAP(1) + rule #dasmOpCode( 145, _ ) => SWAP(2) + rule #dasmOpCode( 146, _ ) => SWAP(3) + rule #dasmOpCode( 147, _ ) => SWAP(4) + rule #dasmOpCode( 148, _ ) => SWAP(5) + rule #dasmOpCode( 149, _ ) => SWAP(6) + rule #dasmOpCode( 150, _ ) => SWAP(7) + rule #dasmOpCode( 151, _ ) => SWAP(8) + rule #dasmOpCode( 152, _ ) => SWAP(9) + rule #dasmOpCode( 153, _ ) => SWAP(10) + rule #dasmOpCode( 154, _ ) => SWAP(11) + rule #dasmOpCode( 155, _ ) => SWAP(12) + rule #dasmOpCode( 156, _ ) => SWAP(13) + rule #dasmOpCode( 157, _ ) => SWAP(14) + rule #dasmOpCode( 158, _ ) => SWAP(15) + rule #dasmOpCode( 159, _ ) => SWAP(16) + rule #dasmOpCode( 160, _ ) => LOG(0) + rule #dasmOpCode( 161, _ ) => LOG(1) + rule #dasmOpCode( 162, _ ) => LOG(2) + rule #dasmOpCode( 163, _ ) => LOG(3) + rule #dasmOpCode( 164, _ ) => LOG(4) rule #dasmOpCode( 240, _ ) => CREATE rule #dasmOpCode( 241, _ ) => CALL rule #dasmOpCode( 242, _ ) => CALLCODE diff --git a/tests/interactive/search/branching-invalid.evm.search-expected b/tests/interactive/search/branching-invalid.evm.search-expected index 49cb885e8e..0334d0462b 100644 --- a/tests/interactive/search/branching-invalid.evm.search-expected +++ b/tests/interactive/search/branching-invalid.evm.search-expected @@ -65,19 +65,19 @@ #Equals - 0 |-> PUSH ( 1 , 3 ) - 2 |-> PUSH ( 1 , 4 ) + 0 |-> PUSH ( 1 ) + 2 |-> PUSH ( 1 ) 4 |-> ADD - 5 |-> PUSH ( 1 , 8 ) + 5 |-> PUSH ( 1 ) 7 |-> EQ - 8 |-> PUSH ( 1 , 12 ) + 8 |-> PUSH ( 1 ) 10 |-> JUMPI 11 |-> INVALID 12 |-> JUMPDEST 13 |-> STOP - .WordStack + 96 : 3 : 96 : 4 : 1 : 96 : 8 : 20 : 96 : 12 : 87 : 254 : 91 : 0 : .WordStack 0 diff --git a/tests/interactive/search/straight-line.evm.search-expected b/tests/interactive/search/straight-line.evm.search-expected index 6223ad8047..83f72d0ab2 100644 --- a/tests/interactive/search/straight-line.evm.search-expected +++ b/tests/interactive/search/straight-line.evm.search-expected @@ -65,13 +65,13 @@ #Equals - 0 |-> PUSH ( 32 , 3 ) - 33 |-> PUSH ( 32 , 4 ) + 0 |-> PUSH ( 32 ) + 33 |-> PUSH ( 32 ) 66 |-> ADD 67 |-> INVALID - .WordStack + 127 : 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 : 0 : 0 : 0 : 3 : 127 : 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 : 0 : 0 : 0 : 4 : 1 : 254 : .WordStack 0 diff --git a/tests/interactive/sumTo10.evm.parse-expected b/tests/interactive/sumTo10.evm.parse-expected index 823d6dd539..f5fca885b7 100644 --- a/tests/interactive/sumTo10.evm.parse-expected +++ b/tests/interactive/sumTo10.evm.parse-expected @@ -1,2 +1,2 @@ -`___ETHEREUM-SIMULATION`(`mkAcct__ETHEREUM-SIMULATION`(#token("7","Int")),`___ETHEREUM-SIMULATION`(`load__ETHEREUM-SIMULATION`(`_:__EVM-DATA`(#token("\"account\"","String"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("7","Int"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"balance\"","String"),#token("1000000000","Int")),`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"nonce\"","String"),#token("1","Int")),`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"code\"","String"),`.ByteArray_EVM-DATA`(.KList)),`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"storage\"","String"),`.Map`(.KList)),`.List{"_,__EVM-DATA"}`(.KList))))))),`.List{"_,__EVM-DATA"}`(.KList))))),`___ETHEREUM-SIMULATION`(`load__ETHEREUM-SIMULATION`(`_:__EVM-DATA`(#token("\"exec\"","String"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"address\"","String"),#token("7","Int")),`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"gas\"","String"),#token("100000","Int")),`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"code\"","String"),`_;__EVM`(`PUSH`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`PUSH`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`MSTORE_EVM`(.KList),`_;__EVM`(`PUSH`(#token("32","Int"),#token("10","Int")),`_;__EVM`(`PUSH`(#token("32","Int"),#token("32","Int")),`_;__EVM`(`MSTORE_EVM`(.KList),`_;__EVM`(`JUMPDEST_EVM`(.KList),`_;__EVM`(`PUSH`(#token("32","Int"),#token("32","Int")),`_;__EVM`(`MLOAD_EVM`(.KList),`_;__EVM`(`ISZERO_EVM`(.KList),`_;__EVM`(`PUSH`(#token("32","Int"),#token("411","Int")),`_;__EVM`(`JUMPI_EVM`(.KList),`_;__EVM`(`PUSH`(#token("32","Int"),#token("32","Int")),`_;__EVM`(`MLOAD_EVM`(.KList),`_;__EVM`(`DUP`(#token("1","Int")),`_;__EVM`(`PUSH`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`MLOAD_EVM`(.KList),`_;__EVM`(`ADD_EVM`(.KList),`_;__EVM`(`PUSH`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`MSTORE_EVM`(.KList),`_;__EVM`(`PUSH`(#token("32","Int"),#token("1","Int")),`_;__EVM`(`SWAP`(#token("1","Int")),`_;__EVM`(`SUB_EVM`(.KList),`_;__EVM`(`PUSH`(#token("32","Int"),#token("32","Int")),`_;__EVM`(`MSTORE_EVM`(.KList),`_;__EVM`(`PUSH`(#token("32","Int"),#token("134","Int")),`_;__EVM`(`JUMP_EVM`(.KList),`_;__EVM`(`JUMPDEST_EVM`(.KList),`_;__EVM`(`PUSH`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`MLOAD_EVM`(.KList),`_;__EVM`(`PUSH`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`SSTORE_EVM`(.KList),`.OpCodes_EVM`(.KList)))))))))))))))))))))))))))))))))),`.List{"_,__EVM-DATA"}`(.KList))))))),`___ETHEREUM-SIMULATION`(`start_ETHEREUM-SIMULATION`(.KList),`___ETHEREUM-SIMULATION`(`check__ETHEREUM-SIMULATION`(`_:__EVM-DATA`(#token("\"account\"","String"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("7","Int"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"storage\"","String"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"0x00\"","String"),#token("\"0x37\"","String")),`.List{"_,__EVM-DATA"}`(.KList)))),`.List{"_,__EVM-DATA"}`(.KList)))),`.List{"_,__EVM-DATA"}`(.KList))))),`___ETHEREUM-SIMULATION`(`failure__ETHEREUM-SIMULATION`(#token("\"Interactive sumTo10 test\"","String")),`___ETHEREUM-SIMULATION`(`success_ETHEREUM-SIMULATION`(.KList),`___ETHEREUM-SIMULATION`(`clear_ETHEREUM-SIMULATION`(.KList),`.EthereumSimulation_ETHEREUM-SIMULATION`(.KList))))))))) +`___ETHEREUM-SIMULATION`(`mkAcct__ETHEREUM-SIMULATION`(#token("7","Int")),`___ETHEREUM-SIMULATION`(`load__ETHEREUM-SIMULATION`(`_:__EVM-DATA`(#token("\"account\"","String"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("7","Int"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"balance\"","String"),#token("1000000000","Int")),`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"nonce\"","String"),#token("1","Int")),`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"code\"","String"),`.ByteArray_EVM-DATA`(.KList)),`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"storage\"","String"),`.Map`(.KList)),`.List{"_,__EVM-DATA"}`(.KList))))))),`.List{"_,__EVM-DATA"}`(.KList))))),`___ETHEREUM-SIMULATION`(`load__ETHEREUM-SIMULATION`(`_:__EVM-DATA`(#token("\"exec\"","String"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"address\"","String"),#token("7","Int")),`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"gas\"","String"),#token("100000","Int")),`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"code\"","String"),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`MSTORE_EVM`(.KList),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("10","Int")),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("32","Int")),`_;__EVM`(`MSTORE_EVM`(.KList),`_;__EVM`(`JUMPDEST_EVM`(.KList),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("32","Int")),`_;__EVM`(`MLOAD_EVM`(.KList),`_;__EVM`(`ISZERO_EVM`(.KList),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("411","Int")),`_;__EVM`(`JUMPI_EVM`(.KList),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("32","Int")),`_;__EVM`(`MLOAD_EVM`(.KList),`_;__EVM`(`DUP`(#token("1","Int")),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`MLOAD_EVM`(.KList),`_;__EVM`(`ADD_EVM`(.KList),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`MSTORE_EVM`(.KList),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("1","Int")),`_;__EVM`(`SWAP`(#token("1","Int")),`_;__EVM`(`SUB_EVM`(.KList),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("32","Int")),`_;__EVM`(`MSTORE_EVM`(.KList),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("134","Int")),`_;__EVM`(`JUMP_EVM`(.KList),`_;__EVM`(`JUMPDEST_EVM`(.KList),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`MLOAD_EVM`(.KList),`_;__EVM`(`PUSHAsm`(#token("32","Int"),#token("0","Int")),`_;__EVM`(`SSTORE_EVM`(.KList),`.OpCodes_EVM`(.KList)))))))))))))))))))))))))))))))))),`.List{"_,__EVM-DATA"}`(.KList))))))),`___ETHEREUM-SIMULATION`(`start_ETHEREUM-SIMULATION`(.KList),`___ETHEREUM-SIMULATION`(`check__ETHEREUM-SIMULATION`(`_:__EVM-DATA`(#token("\"account\"","String"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("7","Int"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"storage\"","String"),`{_}_EVM-DATA`(`_,__EVM-DATA`(`_:__EVM-DATA`(#token("\"0x00\"","String"),#token("\"0x37\"","String")),`.List{"_,__EVM-DATA"}`(.KList)))),`.List{"_,__EVM-DATA"}`(.KList)))),`.List{"_,__EVM-DATA"}`(.KList))))),`___ETHEREUM-SIMULATION`(`failure__ETHEREUM-SIMULATION`(#token("\"Interactive sumTo10 test\"","String")),`___ETHEREUM-SIMULATION`(`success_ETHEREUM-SIMULATION`(.KList),`___ETHEREUM-SIMULATION`(`clear_ETHEREUM-SIMULATION`(.KList),`.EthereumSimulation_ETHEREUM-SIMULATION`(.KList))))))))) diff --git a/tests/specs/examples/sum-to-n-spec.k b/tests/specs/examples/sum-to-n-spec.k index 0bbdd864e3..a394c85ef8 100644 --- a/tests/specs/examples/sum-to-n-spec.k +++ b/tests/specs/examples/sum-to-n-spec.k @@ -13,24 +13,25 @@ requires "../lemmas.k" module VERIFICATION imports EDSL imports LEMMAS + imports EVM-ASSEMBLY rule #sizeWordStack ( WS , N:Int ) => N +Int #sizeWordStack ( WS , 0 ) requires N =/=K 0 [lemma] - syntax Map ::= "sumTo" "(" Int ")" [function] - // --------------------------------------------- - rule sumTo(N) - => #asMapOpCodes( PUSH(1, 0) ; PUSH(32, N) // s = 0 ; n = N - ; JUMPDEST // label:loop - ; DUP(1) ; ISZERO ; PUSH(1, 52) ; JUMPI // if n == 0, jump to end - ; DUP(1) ; SWAP(2) ; ADD // s = s + n - ; SWAP(1) ; PUSH(1, 1) ; SWAP(1) ; SUB // n = n - 1 - ; PUSH(1, 35) ; JUMP // jump to loop - ; JUMPDEST // label:end - ; .OpCodes - ) [macro] + syntax ByteArray ::= "sumToN" [function] + // ---------------------------------------- + rule sumToN + => #asmOpCodes(PUSH(1, 0) ; SWAP(1) // s = 0 ; n = N + ; JUMPDEST // label:loop + ; DUP(1) ; ISZERO ; PUSH(1, 20) ; JUMPI // if n == 0, jump to end + ; DUP(1) ; SWAP(2) ; ADD // s = s + n + ; SWAP(1) ; PUSH(1, 1) ; SWAP(1) ; SUB // n = n - 1 + ; PUSH(1, 3) ; JUMP // jump to loop + ; JUMPDEST // label:end + ; .OpCodes + ) [macro] endmodule @@ -84,7 +85,8 @@ module SUM-TO-N-SPEC 0 .Map _ => _ - sumTo(N) + #asMapOpCodes(#dasmOpCodes(sumToN, DEFAULT)) + sumToN @@ -95,8 +97,8 @@ module SUM-TO-N-SPEC - 0 => 53 - WS => 0 : N *Int (N +Int 1) /Int 2 : WS + 0 => 21 + N : WS => 0 : N *Int (N +Int 1) /Int 2 : WS G => G -Int (52 *Int N +Int 27) requires N >=Int 0 @@ -120,7 +122,8 @@ module SUM-TO-N-SPEC 0 .Map _ => _ - sumTo(N) + #asMapOpCodes(#dasmOpCodes(sumToN, DEFAULT)) + sumToN @@ -134,7 +137,7 @@ module SUM-TO-N-SPEC - 35 => 53 + 3 => 21 G => G -Int (52 *Int I +Int 21) I : S : WS