diff --git a/kevm-pyk/.gitignore b/kevm-pyk/.gitignore index 98fe5a7f3d..700e92b34d 100644 --- a/kevm-pyk/.gitignore +++ b/kevm-pyk/.gitignore @@ -1,3 +1,5 @@ /dist/ __pycache__/ .coverage +proofs/ +summaries/ \ No newline at end of file diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 08deb9d0ea..d2bb615080 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -32,6 +32,8 @@ from pyk.proof.tui import APRProofViewer from pyk.utils import FrozenDict, hash_str, single +from kevm_pyk.summarizer import batch_summarize + from . import VERSION, config from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination from .gst_to_kore import SORT_ETHEREUM_SIMULATION, filter_gst_keys, gst_to_kore, kore_pgm_to_kore @@ -634,6 +636,10 @@ def exec_kast(options: KastOptions) -> None: print(output_text) +def exec_summarize(options: ProveOptions) -> None: + batch_summarize() + + # Helpers diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 5b0c32885b..a663d57c89 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -74,6 +74,8 @@ def generate_options(args: dict[str, Any]) -> LoggingOptions: return KastOptions(args) case 'run': return RunOptions(args) + case 'summarize': + return ProveOptions(args) case _: raise ValueError(f'Unrecognized command: {command}') @@ -99,6 +101,8 @@ def get_option_string_destination(command: str, option_string: str) -> str: option_string_destinations = KastOptions.from_option_string() case 'run': option_string_destinations = RunOptions.from_option_string() + case 'summarize': + option_string_destinations = ProveOptions.from_option_string() return option_string_destinations.get(option_string, option_string.replace('-', '_')) @@ -127,6 +131,8 @@ def func(par: str) -> str: option_types = KastOptions.get_argument_type() case 'run': option_types = RunOptions.get_argument_type() + case 'summarize': + option_types = ProveOptions.get_argument_type() return option_types.get(option_string, func) @@ -183,6 +189,23 @@ def _create_argument_parser() -> ArgumentParser: help='Maximum worker threads to use on a single proof to explore separate branches in parallel.', ) + command_parser.add_parser( + 'summarize', + help='Summarize an Opcode.', + parents=[ + kevm_cli_args.logging_args, + kevm_cli_args.parallel_args, + kevm_cli_args.k_args, + kevm_cli_args.kprove_args, + kevm_cli_args.rpc_args, + kevm_cli_args.bug_report_args, + kevm_cli_args.smt_args, + kevm_cli_args.explore_args, + # kevm_cli_args.spec_args, + config_args.config_args, + ], + ) + prune_args = command_parser.add_parser( 'prune', help='Remove a node and its successors from the proof state.', diff --git a/kevm-pyk/src/kevm_pyk/kdist/plugin.py b/kevm-pyk/src/kevm_pyk/kdist/plugin.py index 184679b4d4..7a0f4e88b3 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/plugin.py +++ b/kevm-pyk/src/kevm_pyk/kdist/plugin.py @@ -115,6 +115,14 @@ def context(self) -> dict[str, str]: 'syntax_module': 'EDSL', }, ), + 'summary': KEVMTarget( + { + 'target': KompileTarget.HASKELL, + 'main_file': config.EVM_SEMANTICS_DIR / 'edsl-sum.md', + 'main_module': 'EDSL', + 'syntax_module': 'EDSL', + }, + ), 'haskell-standalone': KEVMTarget( { 'target': KompileTarget.HASKELL, diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl-sum.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl-sum.md new file mode 100644 index 0000000000..2e225766b7 --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl-sum.md @@ -0,0 +1,35 @@ +eDSL High-Level Notations +========================= + +The eDSL high-level notations make the EVM specifications more succinct and closer to their high-level specifications. +The succinctness increases the readability, and the closeness helps "eye-ball validation" of the specification refinement. +The high-level notations are defined by translation to the corresponding EVM terms, and thus can be freely used with other EVM terms. +The notations are inspired by the production compilers of the smart contract languages like Solidity and Vyper, and their definition is derived by formalizing the corresponding translation made by the compilers. + +```k +requires "buf.md" +requires "hashed-locations.md" +requires "abi.md" +requires "gas.md" +requires "lemmas/lemmas.k" + +module EDSL + imports BUF + imports HASHED-LOCATIONS + imports SOLIDITY-FIELDS + imports EVM-ABI + imports INFINITE-GAS + imports BIN-RUNTIME + imports LEMMAS +endmodule + +module BIN-RUNTIME + imports EVM-ABI + + syntax Contract + syntax Bytes ::= #binRuntime ( Contract ) [alias, symbol(binRuntime) , function, no-evaluators] + | #initBytecode ( Contract ) [alias, symbol(initBytecode), function, no-evaluators] + // -------------------------------------------------------------------------------------------------- + +endmodule +``` diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md index fca29562ba..ce631b3183 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md @@ -12,6 +12,7 @@ requires "hashed-locations.md" requires "abi.md" requires "gas.md" requires "optimizations.md" +requires "lemmas/lemmas.k" module EDSL imports BUF @@ -21,6 +22,7 @@ module EDSL imports EVM-OPTIMIZATIONS imports INFINITE-GAS imports BIN-RUNTIME + imports LEMMAS endmodule module BIN-RUNTIME diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index b0effad7a7..e4b441ec39 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -11,12 +11,14 @@ This file only defines the local execution operations, the file `driver.md` will requires "data.md" requires "network.md" requires "gas.md" +requires "serialization.md" module EVM imports STRING imports EVM-DATA imports NETWORK imports GAS + imports SERIALIZATION ``` Configuration @@ -363,7 +365,7 @@ The `#next [_]` operator initiates execution by: | #stackOverflow ( WordStack , OpCode ) [symbol(#stackOverflow), macro] // --------------------------------------------------------------------------------------- rule #stackUnderflow(WS, OP:OpCode) => #sizeWordStack(WS) #sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024 + rule #stackOverflow (WS, OP) => (#stackDelta(OP) >Int 0) andBool (#sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024) syntax Int ::= #stackNeeded ( OpCode ) [symbol(#stackNeeded), function] // ----------------------------------------------------------------------- @@ -1918,9 +1920,9 @@ Precompiled Contracts syntax InternalOp ::= #ecadd(G1Point, G1Point) [symbol(#ecadd)] // --------------------------------------------------------------- rule #ecadd(P1, P2) => #end EVMC_PRECOMPILE_FAILURE ... - requires notBool isValidPoint(P1) orBool notBool isValidPoint(P2) - rule #ecadd(P1, P2) => #end EVMC_SUCCESS ... _ => #point(BN128Add(P1, P2)) - requires isValidPoint(P1) andBool isValidPoint(P2) + requires notBool isValidPointWrapper(P1) orBool notBool isValidPointWrapper(P2) + rule #ecadd(P1, P2) => #end EVMC_SUCCESS ... _ => #point(BN128AddWrapper(P1, P2)) + requires isValidPointWrapper(P1) andBool isValidPointWrapper(P2) syntax PrecompiledOp ::= "ECMUL" // -------------------------------- @@ -1930,9 +1932,9 @@ Precompiled Contracts syntax InternalOp ::= #ecmul(G1Point, Int) [symbol(#ecmul)] // ----------------------------------------------------------- rule #ecmul(P, _S) => #end EVMC_PRECOMPILE_FAILURE ... - requires notBool isValidPoint(P) - rule #ecmul(P, S) => #end EVMC_SUCCESS ... _ => #point(BN128Mul(P, S)) - requires isValidPoint(P) + requires notBool isValidPointWrapper(P) + rule #ecmul(P, S) => #end EVMC_SUCCESS ... _ => #point(BN128MulWrapper(P, S)) + requires isValidPointWrapper(P) syntax Bytes ::= #point ( G1Point ) [symbol(#point), function] // -------------------------------------------------------------- @@ -1952,19 +1954,19 @@ Precompiled Contracts rule (.K => #checkPoint) ~> #ecpairing((.List => ListItem((#asWord(#range(DATA, I, 32)), #asWord(#range(DATA, I +Int 32, 32))))) _, (.List => ListItem((#asWord(#range(DATA, I +Int 96, 32)) x #asWord(#range(DATA, I +Int 64, 32)) , #asWord(#range(DATA, I +Int 160, 32)) x #asWord(#range(DATA, I +Int 128, 32))))) _, I => I +Int 192, DATA, LEN) ... requires I =/=Int LEN rule #ecpairing(A, B, LEN, _, LEN) => #end EVMC_SUCCESS ... - _ => #padToWidth(32, #asByteStack(bool2Word(BN128AtePairing(A, B)))) + _ => #padToWidth(32, #asByteStack(bool2Word(BN128AtePairingWrapper(A, B)))) syntax InternalOp ::= "#checkPoint" // ----------------------------------- rule (#checkPoint => .K) ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) ... - requires isValidPoint(AK) andBool isValidPoint(BK) + requires isValidPointWrapper(AK) andBool isValidPointWrapper(BK) rule #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #end EVMC_PRECOMPILE_FAILURE ... - requires notBool isValidPoint(AK) orBool notBool isValidPoint(BK) + requires notBool isValidPointWrapper(AK) orBool notBool isValidPointWrapper(BK) syntax PrecompiledOp ::= "BLAKE2F" // ---------------------------------- rule BLAKE2F => #end EVMC_SUCCESS ... - _ => #parseByteStack( Blake2Compress( DATA ) ) + _ => #parseByteStack( Blake2CompressWrapper( DATA ) ) DATA requires lengthBytes( DATA ) ==Int 213 andBool DATA[212] <=Int 1 diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md index 3f345f8c81..acc5e7ca06 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md @@ -263,5 +263,8 @@ module GAS-SIMPLIFICATION [symbolic] imports BOOL rule A false requires B <=Gas A [simplification] + rule notBool (A <=Gas B) => B B <=Gas A [simplification] endmodule ``` + diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k index 265be3c071..c0a0671749 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k @@ -223,4 +223,9 @@ module INT-SIMPLIFICATION-COMMON rule A -Int B +Int C <=Int D => false requires D { true #Equals X >Int 0 } [simplification] endmodule diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 661fa1c143..221528a759 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -46,7 +46,7 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // Word Reasoning // ######################## - rule 0 <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma] + rule N <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma] // #newAddr range rule 0 <=Int #newAddr(_,_) => true [simplification] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md index f6ae417b26..de978fb230 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -18,6 +18,42 @@ module SERIALIZATION Address/Hash Helpers -------------------- +- `BN128AddWrapper` and `BN128MulWrapper` serve as wrappers around the `BN128Add` and `BN128Mul` in `KRYPTO`. + +```k + syntax G1Point ::= BN128AddWrapper ( G1Point , G1Point ) [symbol(BN128AddWrapper), function, total, smtlib(smt_krypto_bn128add)] + | BN128MulWrapper ( G1Point , Int ) [symbol(BN128MulWrapper), function, total, smtlib(smt_krypto_bn128mul)] + // ----------------------------------------------------------------------------------------------------------------------------------------- + rule [BN128AddWrapper]: BN128AddWrapper(G1, G2) => BN128Add(G1, G2) [concrete] + rule [BN128MulWrapper]: BN128MulWrapper(G1, I) => BN128Mul(G1, I) [concrete] +``` + +- `BN128AtePairing` serves as a wrapper around the `BN128AtePairing` in `KRYPTO`. + +```k + syntax Bool ::= BN128AtePairingWrapper ( List , List ) [symbol(BN128AtePairingWrapper), function, total, smtlib(smt_krypto_bn128ate)] + // ------------------------------------------------------------------------------------------------------------------------------------------------ + rule [BN128AtePairingWrapper]: BN128AtePairingWrapper(G1, G2) => BN128AtePairing(G1, G2) [concrete] +``` + +- `Blake2CompressWrapper` serves as a wrapper around the `Blake2Compress` in `KRYPTO`. + +```k + syntax String ::= Blake2CompressWrapper ( Bytes ) [symbol(Blake2CompressWrapper), function, total, smtlib(smt_krypto_blake2compress)] + // ------------------------------------------------------------------------------------------------------------------------------------ + rule [Blake2CompressWrapper]: Blake2CompressWrapper(BYTES) => Blake2Compress(BYTES) [concrete] +``` + +- `isValidPointWrapper` serves as a wrapper around the `isValidPoint` in `KRYPTO`. + +```k + syntax Bool ::= isValidPointWrapper ( G1Point ) [symbol(isValidPointWrapper), function, total, smtlib(smt_krypto_bn128valid)] + | isValidPointWrapper ( G2Point ) [symbol(isValidG2PointWrapper), function, total, smtlib(smt_krypto_bn128g2valid)] + // ----------------------------------------------------------------------------------------------------------------------------- + rule [isValidPointWrapper]: isValidPointWrapper(P:G1Point) => isValidPoint(P) [concrete] + rule [isValidG2PointWrapper]: isValidPointWrapper(P:G2Point) => isValidPoint(P) [concrete] +``` + - `keccak` serves as a wrapper around the `Keccak256` in `KRYPTO`. ```k @@ -33,6 +69,7 @@ Address/Hash Helpers | #newAddr ( Int , Int , Bytes ) [symbol(newAddrCreate2), function] // -------------------------------------------------------------------------------- rule [#newAddr]: #newAddr(ACCT, NONCE) => #addr(#parseHexWord(Keccak256(#rlpEncode([#addrBytes(ACCT), NONCE])))) [concrete] + rule [#newAddr-definedness]: #Ceil(#newAddr(@ACCT, @NONCE)) => #Ceil(@ACCT) #And #Ceil(@NONCE) [simplification] rule [#newAddrCreate2]: #newAddr(ACCT, SALT, INITCODE) => #addr(#parseHexWord(Keccak256(b"\xff" +Bytes #addrBytes(ACCT) +Bytes #wordBytes(SALT) +Bytes #parseByteStack(Keccak256(INITCODE))))) [concrete] ``` diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py new file mode 100644 index 0000000000..fd24f23e7a --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/summarizer.py @@ -0,0 +1,613 @@ +from __future__ import annotations + +import logging +import time +import traceback +from multiprocessing import Pool +from pathlib import Path +from typing import TYPE_CHECKING + +from pyk.cterm import CSubst, CTerm, CTermSymbolic, cterm_build_claim +from pyk.kast.inner import KApply, KSequence, KToken, KVariable, Subst +from pyk.kast.outer import KSort +from pyk.kcfg import KCFG, KCFGExplore +from pyk.kdist import kdist +from pyk.kore.rpc import KoreClient +from pyk.prelude.ml import mlEquals, mlEqualsFalse, mlNot +from pyk.proof import APRProof +from pyk.proof.show import APRProofShow +from pyk.utils import ensure_dir_path + +from kevm_pyk.kevm import KEVM, KEVMSemantics, kevm_node_printer +from kevm_pyk.utils import initialize_apr_proof, legacy_explore, run_prover + +if TYPE_CHECKING: + from pyk.kast.inner import KInner + +_LOGGER = logging.getLogger(__name__) + +OPCODES: dict[str, KApply] = { + 'STOP': KApply('STOP_EVM_NullStackOp'), + 'ADD': KApply('ADD_EVM_BinStackOp'), + 'MUL': KApply('MUL_EVM_BinStackOp'), + 'SUB': KApply('SUB_EVM_BinStackOp'), + 'DIV': KApply('DIV_EVM_BinStackOp'), + 'SDIV': KApply('SDIV_EVM_BinStackOp'), + 'MOD': KApply('MOD_EVM_BinStackOp'), + 'SMOD': KApply('SMOD_EVM_BinStackOp'), + 'ADDMOD': KApply('ADDMOD_EVM_TernStackOp'), + 'MULMOD': KApply('MULMOD_EVM_TernStackOp'), + 'EXP': KApply('EXP_EVM_BinStackOp'), + 'SIGNEXTEND': KApply('SIGNEXTEND_EVM_BinStackOp'), + 'LT': KApply('LT_EVM_BinStackOp'), + 'GT': KApply('GT_EVM_BinStackOp'), + 'SLT': KApply('SLT_EVM_BinStackOp'), + 'SGT': KApply('SGT_EVM_BinStackOp'), + 'EQ': KApply('EQ_EVM_BinStackOp'), + 'ISZERO': KApply('ISZERO_EVM_UnStackOp'), + 'AND': KApply('AND_EVM_BinStackOp'), + 'EVMOR': KApply('EVMOR_EVM_BinStackOp'), + 'XOR': KApply('XOR_EVM_BinStackOp'), + 'NOT': KApply('NOT_EVM_UnStackOp'), + 'BYTE': KApply('BYTE_EVM_BinStackOp'), + 'SHL': KApply('SHL_EVM_BinStackOp'), + 'SHR': KApply('SHR_EVM_BinStackOp'), + 'SAR': KApply('SAR_EVM_BinStackOp'), + 'SHA3': KApply('SHA3_EVM_BinStackOp'), + 'ADDRESS': KApply('ADDRESS_EVM_NullStackOp'), + 'BALANCE': KApply('BALANCE_EVM_UnStackOp'), + 'ORIGIN': KApply('ORIGIN_EVM_NullStackOp'), + 'CALLER': KApply('CALLER_EVM_NullStackOp'), + 'CALLVALUE': KApply('CALLVALUE_EVM_NullStackOp'), + 'CALLDATALOAD': KApply('CALLDATALOAD_EVM_UnStackOp'), + 'CALLDATASIZE': KApply('CALLDATASIZE_EVM_NullStackOp'), + 'CALLDATACOPY': KApply('CALLDATACOPY_EVM_TernStackOp'), + 'CODESIZE': KApply('CODESIZE_EVM_NullStackOp'), + 'CODECOPY': KApply('CODECOPY_EVM_TernStackOp'), + 'GASPRICE': KApply('GASPRICE_EVM_NullStackOp'), + 'EXTCODESIZE': KApply('EXTCODESIZE_EVM_UnStackOp'), + 'EXTCODECOPY': KApply('EXTCODECOPY_EVM_QuadStackOp'), + 'RETURNDATASIZE': KApply('RETURNDATASIZE_EVM_NullStackOp'), + 'RETURNDATACOPY': KApply('RETURNDATACOPY_EVM_TernStackOp'), + 'EXTCODEHASH': KApply('EXTCODEHASH_EVM_UnStackOp'), + 'BLOCKHASH': KApply('BLOCKHASH_EVM_UnStackOp'), + 'COINBASE': KApply('COINBASE_EVM_NullStackOp'), + 'TIMESTAMP': KApply('TIMESTAMP_EVM_NullStackOp'), + 'NUMBER': KApply('NUMBER_EVM_NullStackOp'), + 'PREVRANDAO': KApply('PREVRANDAO_EVM_NullStackOp'), + 'DIFFICULTY': KApply('DIFFICULTY_EVM_NullStackOp'), + 'GASLIMIT': KApply('GASLIMIT_EVM_NullStackOp'), + 'CHAINID': KApply('CHAINID_EVM_NullStackOp'), + 'SELFBALANCE': KApply('SELFBALANCE_EVM_NullStackOp'), + 'BASEFEE': KApply('BASEFEE_EVM_NullStackOp'), + 'POP': KApply('POP_EVM_UnStackOp'), + 'MLOAD': KApply('MLOAD_EVM_UnStackOp'), + 'MSTORE': KApply('MSTORE_EVM_BinStackOp'), + 'MSTORE8': KApply('MSTORE8_EVM_BinStackOp'), + 'SLOAD': KApply('SLOAD_EVM_UnStackOp'), + 'SSTORE': KApply('SSTORE_EVM_BinStackOp'), + 'JUMP': KApply('JUMP_EVM_UnStackOp'), + 'JUMPI': KApply('JUMPI_EVM_BinStackOp'), + 'PC': KApply('PC_EVM_NullStackOp'), + 'MSIZE': KApply('MSIZE_EVM_NullStackOp'), + 'GAS': KApply('GAS_EVM_NullStackOp'), + 'JUMPDEST': KApply('JUMPDEST_EVM_NullStackOp'), + 'TLOAD': KApply('TLOAD_EVM_UnStackOp'), + 'TSTORE': KApply('TSTORE_EVM_BinStackOp'), + 'MCOPY': KApply('MCOPY_EVM_TernStackOp'), + 'PUSHZERO': KApply('PUSHZERO_EVM_PushOp'), + 'PUSH': KApply('PUSH', KVariable('N', KSort('Int'))), + 'DUP': KApply('DUP', KVariable('N', KSort('Int'))), + 'SWAP': KApply('SWAP', KVariable('N', KSort('Int'))), + 'LOG': KApply('LOG', KVariable('N', KSort('Int'))), + 'CREATE': KApply('CREATE_EVM_TernStackOp'), + 'CALL': KApply('CALL_EVM_CallOp'), + 'CALLCODE': KApply('CALLCODE_EVM_CallOp'), + 'RETURN': KApply('RETURN_EVM_BinStackOp'), + 'DELEGATECALL': KApply('DELEGATECALL_EVM_CallSixOp'), + 'CREATE2': KApply('CREATE2_EVM_QuadStackOp'), + 'STATICCALL': KApply('STATICCALL_EVM_CallSixOp'), + 'REVERT': KApply('REVERT_EVM_BinStackOp'), + 'INVALID': KApply('INVALID_EVM_InvalidOp'), + 'SELFDESTRUCT': KApply('SELFDESTRUCT_EVM_UnStackOp'), + 'UNDEFINED': KApply('UNDEFINED(_)_EVM_InvalidOp_Int', KVariable('W', KSort('Int'))), + # OpCode Variable + # 'ALL': KVariable('OP_CODE', KSort('OpCode')) +} + + +OPCODES_SUMMARY_STATUS = { + 'STOP': 'PASSED, One rule? Several rules?', + 'ADD': 'PASSED, No underflow check in KCFG', + 'MUL': 'PASSED, No underflow check in KCFG', + 'SUB': 'PASSED, No underflow check in KCFG', + 'DIV': 'PASSED, No underflow check in KCFG', + 'SDIV': 'PASSED, No underflow check in KCFG', + 'MOD': 'PASSED, No underflow check in KCFG', + 'SMOD': 'PASSED, No underflow check in KCFG', + 'ADDMOD': 'PASSED, No underflow check in KCFG', + 'MULMOD': 'PASSED, No underflow check in KCFG', + 'EXP': 'PASSED, No underflow check in KCFG', + 'SIGNEXTEND': 'PASSED, No underflow check in KCFG', + 'LT': 'PASSED, No underflow check in KCFG', + 'GT': 'PASSED, No underflow check in KCFG', + 'SLT': 'PASSED, No underflow check in KCFG', + 'SGT': 'PASSED, No underflow check in KCFG', + 'EQ': 'PASSED, No underflow check in KCFG', + 'ISZERO': 'PASSED, No underflow check in KCFG', + 'AND': 'PASSED, No underflow check in KCFG', + 'EVMOR': 'PASSED, No underflow check in KCFG', + 'XOR': 'PASSED, No underflow check in KCFG', + 'NOT': 'PASSED, No underflow check in KCFG', + 'BYTE': 'PASSED, No underflow check in KCFG', + 'SHL': 'PASSED, No underflow check in KCFG', + 'SHR': 'PASSED, No underflow check in KCFG', + 'SAR': 'PASSED, No underflow check in KCFG', + 'SHA3': 'PASSED, No underflow check in KCFG', + 'ADDRESS': 'PASSED, No underflow check, no .Account', + 'BALANCE': 'PASSED, no underflow check, no gas usage', + 'ORIGIN': 'PASSED, no underflow check, no .Account in origin cell', + 'CALLER': 'PASSED, no underflow check, no gas usage', + 'CALLVALUE': 'PASSED, No underflow check in KCFG', + 'CALLDATALOAD': 'PASSED, No underflow check in KCFG', + 'CALLDATASIZE': 'PASSED, No underflow check in KCFG', + 'CALLDATACOPY': 'PASSED, No underflow check in KCFG', + 'CODESIZE': 'PASSED, No underflow check in KCFG', + 'CODECOPY': 'PASSED, No underflow check in KCFG', + 'GASPRICE': 'PASSED, No underflow check in KCFG', + 'EXTCODESIZE': 'PASSED, No underflow check, No gas usage', + 'EXTCODECOPY': 'PASSED, No underflow check, No gas usage', + 'RETURNDATASIZE': 'PASSED, No underflow check, No gas usage', + 'RETURNDATACOPY': 'PASSED, No underflow check in KCFG', + 'EXTCODEHASH': 'PASSED, No underflow check, No gas usage', + 'BLOCKHASH': 'PASSED, No underflow check in KCFG', + 'COINBASE': 'PASSED, No underflow check, No gas usage', + 'TIMESTAMP': 'PASSED, No underflow check in KCFG', + 'NUMBER': 'PASSED, No underflow check in KCFG', + 'PREVRANDAO': 'PASSED, No underflow check in KCFG', + 'DIFFICULTY': 'PASSED, No underflow check in KCFG', + 'GASLIMIT': 'PASSED, No underflow check in KCFG', + 'CHAINID': 'PASSED, No underflow check in KCFG', + 'SELFBALANCE': 'PASSED, No underflow check in KCFG', + 'BASEFEE': 'PASSED, No underflow check in KCFG', + 'POP': 'PASSED, No underflow check, no gas usage', + 'MLOAD': 'PASSED, No underflow check, no gas usage', + 'MSTORE': 'PASSED, No underflow check in KCFG', + 'MSTORE8': 'PASSED, No underflow check, no gas usage', + 'SLOAD': 'PASSED, No underflow check in KCFG', + 'SSTORE': 'PASSED, No underflow check in KCFG', + 'JUMP': 'PASSED, No underflow check, wierd ndbranch that looks like a split', + 'JUMPI': 'PASSED, no underflow check, no gas usage, weird ndbranch that looks like a split', + 'PC': 'PASSED, No underflow check in KCFG', + 'MSIZE': 'PASSED, No underflow check in KCFG, no gas usage', + 'GAS': 'PASSED, No underflow check in KCFG', + 'JUMPDEST': 'PASSED, No underflow check in KCFG', + 'TLOAD': 'PASSED, No underflow check, no gas usage', + 'TSTORE': 'PASSED, No underflow check, no gas usage, strange info about smt reason timeout', + 'MCOPY': 'PASSED, No underflow check in KCFG', + 'PUSHZERO': 'PASSED, No underflow check in KCFG', + 'PUSH': 'PASSED, No underflow check, no gas usage', + 'DUP': 'PASSED, No underflow check in KCFG', + 'SWAP': 'PASSED, No underflow check in KCFG', + 'LOG': 'PASSED, No underflow check, no gas usage', + 'CREATE': 'TODO, Proof crashed', + 'CALL': 'UNCHECKED', + 'CALLCODE': 'UNCHECKED', + 'RETURN': 'PASSED, no underflow check, no gas usage', + 'DELEGATECALL': 'UNCHECKED', + 'CREATE2': 'UNCHECKED', + 'STATICCALL': 'UNCHECKED', + 'REVERT': 'PASSED', + 'INVALID': 'PASSED', + 'SELFDESTRUCT': 'UNCHECKED', + 'UNDEFINED': 'PASSED', + 'ALL': 'TODICUSS, failed to summarize, the optimized rule applies one step to obtain the target, the failure process rules are applied to obtain the failure, we need to summarize these ndbranches and exclude these conditions from individual opcode spec', +} + + +NOT_USEGAS_OPCODES = [ + 'BALANCE', + 'EXTCODESIZE', + 'EXTCODECOPY', + 'CALLER', + 'RETURNDATASIZE', + 'EXTCODEHASH', + 'COINBASE', + 'SELFBALANCE', + 'POP', + 'MLOAD', + 'MSTORE8', + 'SLOAD', + 'SSTORE', + 'JUMP', + 'JUMPI', + 'MSIZE', + 'TLOAD', + 'TSTORE', + 'PUSH', + 'CREATE', + 'CALL', +] + +ACCOUNT_QUERIES_OPCODES = [ + 'BALANCE', + 'EXTCODESIZE', + 'EXTCODEHASH' 'EXTCODECOPY', +] + +ACCOUNT_STORAGE_OPCODES = ['SLOAD', 'SSTORE', 'TLOAD', 'TSTORE'] + + +def get_passed_opcodes() -> list[str]: + passed_opcodes = [] + for opcode in OPCODES_SUMMARY_STATUS: + if get_summary_status(opcode) == 'PASSED': + passed_opcodes.append(opcode) + return passed_opcodes + + +def get_summary_status(opcode: str) -> str: + assert opcode in OPCODES_SUMMARY_STATUS + return OPCODES_SUMMARY_STATUS[opcode].split(',')[0] + + +def word_stack(size_over: int) -> KInner: + def _word_stack_var(n: int) -> KInner: + return KVariable(f'W{n}', KSort('Int')) + + def _word_stack(w0: KInner, w1: KInner) -> KInner: + return KApply('_:__EVM-TYPES_WordStack_Int_WordStack', [w0, w1]) + + ws: KInner = KVariable('WS', KSort('WordStack')) + for i in reversed(range(size_over)): + ws = _word_stack(_word_stack_var(i), ws) + return ws + + +def get_todo_list() -> list[str]: + todo_list = [] + _LOGGER.info(f'Number of opcodes: {len(OPCODES)}') + for opcode in OPCODES: + if get_summary_status(opcode) != 'PASSED': + todo_list.append(opcode) + _LOGGER.info(f'Number of passed opcodes: {len(OPCODES)-len(todo_list)}') + _LOGGER.info(f'Number of todo opcodes: {len(todo_list)}') + _LOGGER.info(f'Todo opcodes: {todo_list}') + return todo_list + + +def stack_needed(opcode_id: str) -> list[int]: + """ + Return the stack size needed for the opcode, corresponding `#stackNeeded` in the semantics. + """ + opcode = OPCODES[opcode_id].label.name + if 'CallOp' in opcode: + return [7] + elif 'CallSixOp' in opcode: + return [6] + elif 'LOG' in opcode: + return list(range(5)) + elif 'SWAP' in opcode: + return list(range(1, 17)) + elif 'DUP' in opcode: + return list(range(1, 17)) + elif 'QuadStackOp' in opcode: + return [4] + elif 'TernStackOp' in opcode: + return [3] + elif 'BinStackOp' in opcode: + return [2] + elif 'UnStackOp' in opcode: + return [1] + return [0] + + +def accounts_cell(acct_id: str) -> tuple[KInner, KInner]: + """Return the accounts cell with constraints on the accounts.""" + acct_id_cell = KApply('', KVariable(acct_id, KSort('Int'))) + balance_cell = KApply('', KVariable('BALANCE_CELL', KSort('Int'))) + code_cell = KApply('', KVariable('CODE_CELL', KSort('AccountCode'))) + storage_cell = KApply('', KVariable('STORAGE_CELL', KSort('Map'))) + orig_storage_cell = KApply('', KVariable('ORIG_STORAGE_CELL', KSort('Map'))) + transient_storage_cell = KApply('', KVariable('TRANSIENT_STORAGE_CELL', KSort('Map'))) + nonce_cell = KApply('', KVariable('NONCE_CELL', KSort('Int'))) + account_cell = KApply( + '', + [ + acct_id_cell, + balance_cell, + code_cell, + storage_cell, + orig_storage_cell, + transient_storage_cell, + nonce_cell, + ], + ) + dot_account_var = KVariable('DotAccountVar', KSort('AccountCellMap')) + constraint = mlEqualsFalse( + KApply( + 'AccountCellMap:in_keys', + [ + KApply('', KVariable(acct_id, KSort('Int'))), + KVariable('DotAccountVar', KSort('AccountCellMap')), + ], + ) + ) + + return KApply('_AccountCellMap_', [account_cell, dot_account_var]), constraint + + +class KEVMSummarizer: + """ + A class for summarizing the instructions of the KEVM. + + 1. `build_spec` builds the proof to symbolically execute one abitrary opcode. + 2. `explore` runs the proof to get the KCFG. + 3. `summarize` minimizes the KCFG to get the summarized rules for opcodes. + """ + + _cterm_symbolic: CTermSymbolic + kevm: KEVM + proof_dir: Path + save_directory: Path + + def __init__(self, proof_dir: Path, save_directory: Path) -> None: + self.kevm = KEVM(kdist.get('evm-semantics.summary')) + self.proof_dir = proof_dir + self.save_directory = save_directory + + def build_stack_underflow_spec(self) -> APRProof | None: + """Build the specification to symbolically execute abitrary instruction with stack underflow.""" + # TODO: + return None + + def build_spec(self, opcode: KApply, stack_needed: int, id_str: str = '') -> APRProof: + """Build the specification to symbolically execute one abitrary instruction.""" + cterm = CTerm(self.kevm.definition.empty_config(KSort('GeneratedTopCell'))) + opcode_symbol = opcode.label.name.split('_')[0] + + # construct the initial substitution + _init_subst: dict[str, KInner] = {} + _init_constraints: list[KInner] = [] + next_opcode = KApply('#next[_]_EVM_InternalOp_MaybeOpCode', opcode) + _init_subst['K_CELL'] = KSequence([next_opcode, KVariable('K_CELL')]) # #next [ OPCODE ] ~> K_CELL + _init_subst['WORDSTACK_CELL'] = word_stack(stack_needed) # W0 : W1 : ... : Wn for not underflow + _init_subst['ID_CELL'] = KVariable('ID_CELL', KSort('Int')) # ID_CELL should be Int for ADDRESS, LOG. + # This is because #push doesn't handle `.Account`. And it's okay to be Int for other opcodes. + _init_subst['CALLER_CELL'] = KVariable('CALLER_CELL', KSort('Int')) # CALLER_CELL should be Int for CALLER. + _init_subst['ORIGIN_CELL'] = KVariable('ORIGIN_CELL', KSort('Int')) # ORIGIN_CELL should be Int for ORIGIN. + _init_subst['GAS_CELL'] = KEVM.inf_gas( + KVariable('GAS_CELL', KSort('Gas')) + ) # inf_gas to reduce the computation cost. + if opcode_symbol in NOT_USEGAS_OPCODES: + _init_subst['USEGAS_CELL'] = KToken('false', KSort('Bool')) # TODO: cannot usegas for these opcodes. + if opcode_symbol in ACCOUNT_QUERIES_OPCODES: + cell, constraint = accounts_cell('W0') + _init_subst['ACCOUNTS_CELL'] = cell + _init_constraints.append(constraint) + if opcode_symbol in ACCOUNT_STORAGE_OPCODES: + cell, constraint = accounts_cell('ID_CELL') + _init_subst['ACCOUNTS_CELL'] = cell + _init_constraints.append(constraint) + init_subst = CSubst(Subst(_init_subst), ()) + + # construct the final substitution + _final_subst: dict[str, KInner] = {vname: KVariable('FINAL_' + vname) for vname in cterm.free_vars} + _final_subst['K_CELL'] = KVariable('K_CELL') + if opcode_symbol == 'JUMP': + _final_subst['K_CELL'] = KSequence([KApply('#endBasicBlock_EVM_InternalOp'), KVariable('K_CELL')]) + final_subst = CSubst(Subst(_final_subst), ()) + + init_cterm = init_subst(cterm) + init_cterm = CTerm(init_cterm.config, _init_constraints + list(init_cterm.constraints)) + kclaim = cterm_build_claim(f'{opcode_symbol}{id_str}_{stack_needed}_SPEC', init_cterm, final_subst(cterm)) + proof = APRProof.from_claim(self.kevm.definition, kclaim[0], {}, self.proof_dir) + return proof + + def build_specs(self, opcode_symbol: str) -> list[APRProof]: + needs = stack_needed(opcode_symbol) + opcode = OPCODES[opcode_symbol] + proofs = [] + for need in needs: + if len(needs) > 1: + opcode = KApply(opcode.label.name, KToken(str(need), KSort('Int'))) + + if opcode_symbol == 'JUMPI': + proof = self.build_spec(opcode, need, id_str='_FALSE') + constraint = mlEquals(KVariable('W1', KSort('Int')), KToken('0', KSort('Int')), 'Int') + node1 = proof.kcfg.get_node(1) + assert isinstance(node1, KCFG.Node) + proof.kcfg.let_node(1, cterm=node1.cterm.add_constraint(constraint)) + proofs.append(proof) + + proof = self.build_spec(opcode, need, id_str='_TRUE') + _subst = {'K_CELL': KSequence([KApply('#endBasicBlock_EVM_InternalOp'), KVariable('K_CELL')])} + subst = CSubst(Subst(_subst), ()) + constraint = mlNot(mlEquals(KVariable('W1', KSort('Int')), KToken('0', KSort('Int')), 'Int')) + node1 = proof.kcfg.get_node(1) + assert isinstance(node1, KCFG.Node) + proof.kcfg.let_node(1, cterm=node1.cterm.add_constraint(constraint)) + node2 = proof.kcfg.get_node(2) + assert isinstance(node2, KCFG.Node) + proof.kcfg.let_node(2, cterm=subst(node2.cterm)) + proofs.append(proof) + elif opcode_symbol == 'LOG': + need += 2 + proof = self.build_spec(opcode, need) + proofs.append(proof) + else: + proof = self.build_spec(opcode, need) + proofs.append(proof) + return proofs + + def explore(self, proof: APRProof) -> bool: + """ + Execute the specification to explore the KCFG for all possible instructions. + """ + + # Construct the KCFGExplore + # Copy from kevm-pyk/src/kevm_pyk/__main__.py/exec_prove + # TODO: Make this process as an independent function to reuse； best to be in pyk. + + def _init_and_run_proof(proof: APRProof) -> tuple[bool, list[str]]: + with legacy_explore( + self.kevm, + kcfg_semantics=KEVMSemantics(allow_symbolic_program=True), + id=proof.id, + llvm_definition_dir=self.kevm.definition_dir / 'llvm-library', + bug_report=None, + kore_rpc_command=('kore-rpc-booster',), + smt_timeout=None, + smt_retry_limit=None, + log_succ_rewrites=True, + log_fail_rewrites=True, + fallback_on=None, + interim_simplification=25, + no_post_exec_simplify=False, + port=None, + haskell_threads=8, + ) as kcfg_explore: + + def create_kcfg_explore() -> KCFGExplore: + client = KoreClient( + 'localhost', + kcfg_explore.cterm_symbolic._kore_client.port, + bug_report=None, + bug_report_id=None, + dispatch=None, + ) + cterm_symbolic = CTermSymbolic( + client, + self.kevm.definition, + log_succ_rewrites=True, + log_fail_rewrites=True, + ) + return KCFGExplore( + cterm_symbolic, + kcfg_semantics=KEVMSemantics(allow_symbolic_program=True), + id=proof.id, + ) + + initialize_apr_proof(kcfg_explore.cterm_symbolic, proof) + proof.write_proof_data() + + start_time = time.time() + passed = run_prover( + proof, + create_kcfg_explore=create_kcfg_explore, + max_depth=1000, + max_iterations=None, + cut_point_rules=KEVMSemantics.cut_point_rules( + break_on_jumpi=False, + break_on_jump=False, + break_on_calls=False, + break_on_storage=False, + break_on_basic_blocks=False, + break_on_load_program=False, + ), + terminal_rules=KEVMSemantics.terminal_rules(False), + fail_fast=False, + fast_check_subsumption=False, + direct_subproof_rules=False, + max_frontier_parallel=8, + force_sequential=False, + assume_defined=False, + optimize_kcfg=False, + ) + end_time = time.time() + print(f'Proof timing {proof.id}: {end_time - start_time}s') + # failure_log = None + + node_printer = kevm_node_printer(self.kevm, proof) + proof_show = APRProofShow(self.kevm, node_printer=node_printer) + + res_lines = proof_show.show( + proof, + nodes=[node.id for node in proof.kcfg.nodes], + ) + + return passed, res_lines + + passed, res_lines = _init_and_run_proof(proof) + + ensure_dir_path(self.save_directory / proof.id) + with open(self.save_directory / proof.id / 'proof-result.txt', 'w') as f: + f.write(f'Proof {proof.id} Passed' if passed else f'Proof {proof.id} Failed') + f.write('\n') + for line in res_lines: + f.write(line) + f.write('\n') + return passed + + def summarize(self, proof: APRProof, merge: bool = False) -> None: + # TODO: may need customized way to generate summary rules, e.g., replacing infinite gas with finite gas. + proof.minimize_kcfg(KEVMSemantics(allow_symbolic_program=True), merge) + node_printer = kevm_node_printer(self.kevm, proof) + proof_show = APRProofShow(self.kevm, node_printer=node_printer) + ensure_dir_path(self.save_directory / proof.id) + with open(self.save_directory / proof.id / 'summary.md', 'w') as f: + for res_line in proof_show.show(proof, to_module=True): + f.write(res_line) + f.write('\n') + + def analyze_proof(self, proof_id: str, node_id: int) -> None: + proof = APRProof.read_proof_data(self.proof_dir, proof_id) + for successor in proof.kcfg.successors(node_id): + print('Type: ', type(successor)) + print('Source: ', successor.source.id) + if isinstance(successor, KCFG.Edge) or isinstance(successor, KCFG.NDBranch): + print('Rules: ', successor.rules) + print('Target: ', [target.id for target in successor.targets]) + + +def _process_opcode(opcode: str) -> None: + try: + summarize(opcode) + _LOGGER.info(f'Successfully processed opcode: {opcode}') + except Exception as e: + _LOGGER.error(f'Failed to process opcode {opcode}: {str(e)}') + _LOGGER.debug(traceback.format_exc()) + + +def batch_summarize(num_processes: int = 4) -> None: + """ + Parallelize the summarization of opcodes using multiple processes. + + Args: + num_processes: Number of parallel processes to use. Defaults to 4. + """ + + opcodes_to_process = OPCODES.keys() + passed_opcodes = get_passed_opcodes() + unpassed_opcodes = [opcode for opcode in opcodes_to_process if opcode not in passed_opcodes] + has_call_opcodes = [opcode for opcode in unpassed_opcodes if 'Call' in OPCODES[opcode].label.name] + no_call_opcodes = [opcode for opcode in unpassed_opcodes if 'Call' not in OPCODES[opcode].label.name] + + _LOGGER.info(f'Starting batch summarization of {len(unpassed_opcodes)} opcodes with {num_processes} processes') + + with Pool(processes=num_processes) as pool: + _LOGGER.info(f'Summarizing {len(no_call_opcodes)} opcodes without CALL') + pool.map(_process_opcode, no_call_opcodes) + _LOGGER.info(f'Summarizing {len(has_call_opcodes)} opcodes with CALL') + pool.map(_process_opcode, has_call_opcodes) + + _LOGGER.info('Batch summarization completed') + + +def summarize(opcode_symbol: str) -> tuple[KEVMSummarizer, list[APRProof]]: + proof_dir = Path(__file__).parent / 'proofs' + save_directory = Path(__file__).parent / 'summaries' + summarizer = KEVMSummarizer(proof_dir, save_directory) + proofs = summarizer.build_specs(opcode_symbol) + for proof in proofs: + summarizer.explore(proof) + summarizer.summarize(proof) + proof.write_proof_data() + return summarizer, proofs + + +def analyze_proof(opcode: str, node_id: int) -> None: + proof_dir = Path(__file__).parent / 'proofs' + save_directory = Path(__file__).parent / 'summaries' + summarizer = KEVMSummarizer(proof_dir, save_directory) + summarizer.analyze_proof(str(proof_dir / f'{opcode}_SPEC'), node_id) diff --git a/kevm-pyk/src/tests/integration/test_summarize.py b/kevm-pyk/src/tests/integration/test_summarize.py new file mode 100644 index 0000000000..559298f457 --- /dev/null +++ b/kevm-pyk/src/tests/integration/test_summarize.py @@ -0,0 +1,61 @@ +import pytest +from pyk.kast.outer import KRuleLike +from pyk.kcfg import KCFG + +from kevm_pyk.summarizer import OPCODES, OPCODES_SUMMARY_STATUS, get_summary_status, summarize + + +@pytest.mark.parametrize('opcode', OPCODES.keys()) +def test_summarize(opcode: str) -> None: + if get_summary_status(opcode) != 'PASSED': + pytest.skip(f'{opcode} status: {OPCODES_SUMMARY_STATUS[opcode]}') + + print(f'[{opcode}] selected') + summarizer, proofs = summarize(opcode) + print(f'[{opcode}] summarize finished') + print(f'[{opcode}] {len(proofs)} proofs generated') + + for proof in proofs: + claims: list[KRuleLike] = [] + + # no pending, failing, bounded nodes in the proof + for leaf in proof.kcfg.leaves: + assert not proof.is_pending(leaf.id) + assert not proof.kcfg.is_stuck(leaf.id) + assert not proof.kcfg.is_vacuous(leaf.id) + assert not proof.is_bounded(leaf.id) + print(f'[{opcode}] Node {leaf.id} is not pending, stuck, vacuous, or bounded') + + # only one successor from the initial node in the proof + successors = proof.kcfg.successors(proof.init) + assert len(successors) == 1 + successor = successors[0] + print(f'[{opcode}] Node {proof.init} has only one successor') + + # only one edge to the terminal node + if isinstance(successor, KCFG.Split): + targets = successor.targets + assert len(proof.kcfg.edges()) == len(targets) + print(f'[{opcode}] Split has {len(targets)} targets') + for target in targets: + successors = proof.kcfg.successors(target.id) + assert len(successors) == 1 + edge = successors[0] + assert isinstance(edge, KCFG.Edge) + assert proof.is_terminal(edge.target.id) or proof.kcfg.is_covered(edge.target.id) + claims.append(edge.to_rule(f'{opcode}-SUMMARY', claim=True)) + print(f'[{opcode}] Edge {edge.source.id} -> {edge.target.id} is terminal or covered') + else: + assert len(proof.kcfg.edges()) == 1 + assert isinstance(successor, KCFG.Edge) + assert proof.is_terminal(successor.target.id) or proof.kcfg.is_covered(successor.target.id) + claims.append(successor.to_rule(f'{opcode}-SUMMARY', claim=True)) + print(f'[{opcode}] Edge {successor.source.id} -> {successor.target.id} is terminal or covered') + + # # prove the correctness of the summary + # for claim in claims: + # print(f'[{opcode}] Proving claim {claim.att.get(Atts.LABEL)}') + # assert summarizer.explore( + # APRProof.from_claim(summarizer.kevm.definition, claim, {}, summarizer.proof_dir) + # ) + # print(f'[{opcode}] Claim {claim.att.get(Atts.LABEL)} proved') diff --git a/tests/ethereum-tests b/tests/ethereum-tests index c30599fb23..faf33b4714 160000 --- a/tests/ethereum-tests +++ b/tests/ethereum-tests @@ -1 +1 @@ -Subproject commit c30599fb23d0470301f68bc69188ef444dcbc861 +Subproject commit faf33b471465d3c6cdc3d04fbd690895f78d33f2