diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index a494d03bef..46c8f64f67 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -639,7 +639,7 @@ def exec_summarize(options: ProveOptions) -> None: proof_dir = Path(__file__).parent / 'proofs' save_directory = Path(__file__).parent / 'summaries' summarizer = KEVMSummarizer(proof_dir, save_directory) - proof = summarizer.build_spec('STOP') + proof = summarizer.build_spec('ADD') summarizer.explore(proof) summarizer.summarize(proof) # summarizer.analyze_proof(proof_dir / 'STOP_SPEC') 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 5708f1ae4b..d86781e3e4 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1886,9 +1886,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) + requires notBool isValidPointWrapper(P1) orBool notBool isValidPointWrapper(P2) rule #ecadd(P1, P2) => #end EVMC_SUCCESS ... _ => #point(BN128Add(P1, P2)) - requires isValidPoint(P1) andBool isValidPoint(P2) + requires isValidPointWrapper(P1) andBool isValidPointWrapper(P2) syntax PrecompiledOp ::= "ECMUL" // -------------------------------- @@ -1898,9 +1898,9 @@ Precompiled Contracts syntax InternalOp ::= #ecmul(G1Point, Int) [symbol(#ecmul)] // ----------------------------------------------------------- rule #ecmul(P, _S) => #end EVMC_PRECOMPILE_FAILURE ... - requires notBool isValidPoint(P) + requires notBool isValidPointWrapper(P) rule #ecmul(P, S) => #end EVMC_SUCCESS ... _ => #point(BN128Mul(P, S)) - requires isValidPoint(P) + requires isValidPointWrapper(P) syntax Bytes ::= #point ( G1Point ) [symbol(#point), function] // -------------------------------------------------------------- @@ -1925,9 +1925,9 @@ Precompiled Contracts 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" // ---------------------------------- 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 13a582cb6c..b0f994b895 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,16 @@ module SERIALIZATION Address/Hash Helpers -------------------- +- `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 diff --git a/kevm-pyk/src/kevm_pyk/summaries/ADD_SPEC/nohup.out b/kevm-pyk/src/kevm_pyk/summaries/ADD_SPEC/nohup.out new file mode 100644 index 0000000000..6d3d3e6472 --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/summaries/ADD_SPEC/nohup.out @@ -0,0 +1,671 @@ +   INFO 2025-01-09 07:20:22,497 pyk.kast.outer - Loading JSON definition: /home/zhaoji/.cache/kdist-9ffc41e/evm-semantics/haskell/compiled.json +INFO 2025-01-09 07:20:22,581 pyk.kast.outer - Converting JSON definition to Kast: /home/zhaoji/.cache/kdist-9ffc41e/evm-semantics/haskell/compiled.json +INFO 2025-01-09 07:20:22,990 pyk.utils - Making directory: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/kcfg +INFO 2025-01-09 07:20:22,990 pyk.utils - Making directory: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/kcfg/nodes +INFO 2025-01-09 07:20:22,994 pyk.kore.rpc - Starting KoreServer: kore-rpc-booster /home/zhaoji/.cache/kdist-9ffc41e/evm-semantics/haskell/definition.kore --module EDSL --server-port 0 --llvm-backend-library /home/zhaoji/.cache/kdist-9ffc41e/evm-semantics/haskell/llvm-library/interpreter.so --interim-simplification 25 +INFO 2025-01-09 07:20:23,000 pyk.kore.rpc - [PID=666580][stde] [proxy] Loading definition from /home/zhaoji/.cache/kdist-9ffc41e/evm-semantics/haskell/definition.kore, main module "EDSL" +INFO 2025-01-09 07:20:24,002 pyk.kore.rpc - [PID=666580][stde] [kore][info] Reading the input file TimeSpec {sec = 0, nsec = 24159631} +INFO 2025-01-09 07:20:25,003 pyk.kore.rpc - [PID=666580][stde] [kore][info] Parsing the file TimeSpec {sec = 0, nsec = 110} +INFO 2025-01-09 07:20:26,004 pyk.kore.rpc - [PID=666580][stde] [kore][info] Verifying the definition TimeSpec {sec = 0, nsec = 230} +INFO 2025-01-09 07:20:27,005 pyk.kore.rpc - [PID=666580][stde] [kore][info] Executing TimeSpec {sec = 0, nsec = 707814144} +INFO 2025-01-09 07:20:27,005 pyk.kore.rpc - [PID=666580][stde] [kore][info] Reading the input file TimeSpec {sec = 0, nsec = 24515185} +INFO 2025-01-09 07:20:27,005 pyk.kore.rpc - [PID=666580][stde] [kore][info] Parsing the file TimeSpec {sec = 0, nsec = 120} +INFO 2025-01-09 07:20:27,673 pyk.kore.rpc - KoreServer started: 0.0.0.0:39309, pid=666580 +INFO 2025-01-09 07:20:27,673 pyk.kore.rpc - Connecting to host: localhost:39309 +INFO 2025-01-09 07:20:27,674 pyk.kore.rpc - Connected to host: localhost:39309 +INFO 2025-01-09 07:20:27,674 kevm_pyk.utils - Computing definedness constraint for initial node: ADD_SPEC +INFO 2025-01-09 07:20:27,687 pyk.kore.rpc - Sending request to localhost:39309: 139792892662480-001 - simplify +INFO 2025-01-09 07:20:28,006 pyk.kore.rpc - [PID=666580][stde] [proxy] Processing request 139792892662480-001 +INFO 2025-01-09 07:20:28,006 pyk.kore.rpc - [PID=666580][stde] [kore][info] Verifying the definition TimeSpec {sec = 0, nsec = 210} +INFO 2025-01-09 07:20:28,006 pyk.kore.rpc - [PID=666580][stde] [proxy] Starting RPC server +INFO 2025-01-09 07:20:28,232 pyk.kore.rpc - Received response from localhost:39309: 139792892662480-001 - simplify +INFO 2025-01-09 07:20:28,245 pyk.kore.rpc - Sending request to localhost:39309: 139792892662480-002 - simplify +INFO 2025-01-09 07:20:28,780 pyk.kore.rpc - Received response from localhost:39309: 139792892662480-002 - simplify +INFO 2025-01-09 07:20:28,781 kevm_pyk.utils - Simplifying initial and target node: ADD_SPEC +INFO 2025-01-09 07:20:28,790 pyk.kore.rpc - Sending request to localhost:39309: 139792892662480-003 - simplify +INFO 2025-01-09 07:20:29,007 pyk.kore.rpc - [PID=666580][stde] [proxy] Processing request 139792892662480-002 +INFO 2025-01-09 07:20:29,007 pyk.kore.rpc - [PID=666580][stde] [proxy] Processing request 139792892662480-003 +INFO 2025-01-09 07:20:29,415 pyk.kore.rpc - Received response from localhost:39309: 139792892662480-003 - simplify +INFO 2025-01-09 07:20:29,422 pyk.kore.rpc - Sending request to localhost:39309: 139792892662480-004 - simplify +INFO 2025-01-09 07:20:29,963 pyk.kore.rpc - Received response from localhost:39309: 139792892662480-004 - simplify +INFO 2025-01-09 07:20:29,967 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:20:29,968 pyk.kore.rpc - Connecting to host: localhost:39309 +INFO 2025-01-09 07:20:29,968 pyk.kore.rpc - Connected to host: localhost:39309 +INFO 2025-01-09 07:20:29,968 pyk.proof.proof - [ZJH] prover type: +INFO 2025-01-09 07:20:29,968 pyk.proof.reachability - [ZJH] init proof +INFO 2025-01-09 07:20:29,971 pyk.kore.rpc - Sending request to localhost:39309: 139792900265744-001 - add-module +INFO 2025-01-09 07:20:30,008 pyk.kore.rpc - [PID=666580][stde] [proxy] Processing request 139792900265744-001 +INFO 2025-01-09 07:20:30,008 pyk.kore.rpc - [PID=666580][stde] [proxy] Processing request 139792892662480-004 +INFO 2025-01-09 07:20:30,766 pyk.kore.rpc - Received response from localhost:39309: 139792900265744-001 - add-module +INFO 2025-01-09 07:20:30,781 pyk.kore.rpc - Sending request to localhost:39309: 139792900265744-002 - add-module +INFO 2025-01-09 07:20:31,009 pyk.kore.rpc - [PID=666580][stde] [proxy] Processing request 139792900265744-002 +INFO 2025-01-09 07:20:31,573 pyk.kore.rpc - Received response from localhost:39309: 139792900265744-002 - add-module +INFO 2025-01-09 07:20:31,573 pyk.proof.reachability - [ZJH] pending: [1] +INFO 2025-01-09 07:20:31,574 pyk.proof.reachability - [ZJH] node_id: 1 +INFO 2025-01-09 07:20:31,574 pyk.proof.reachability - [ZJH] is_terminal: False +INFO 2025-01-09 07:20:31,574 pyk.proof.reachability - [ZJH] node_id: 2 +INFO 2025-01-09 07:20:31,575 pyk.proof.reachability - [ZJH] is_terminal: False +INFO 2025-01-09 07:20:31,575 pyk.proof.reachability - [ZJH] pending: [1] +INFO 2025-01-09 07:20:31,575 pyk.proof.proof - [ZJH] proof initialized +INFO 2025-01-09 07:20:31,575 pyk.proof.proof - [ZJH] pending: [1] +INFO 2025-01-09 07:20:31,575 pyk.proof.reachability - Before appending step: 1 +INFO 2025-01-09 07:20:31,576 pyk.kore.rpc - Connecting to host: localhost:39309 +INFO 2025-01-09 07:20:31,576 pyk.proof.proof - Submitted steps for proof: ADD_SPEC +INFO 2025-01-09 07:20:31,576 pyk.kore.rpc - Connected to host: localhost:39309 +INFO 2025-01-09 07:20:31,606 pyk.kore.rpc - Sending request to localhost:39309: 139792891217104-001 - implies +INFO 2025-01-09 07:20:32,047 pyk.kore.rpc - [PID=666580][stde] [proxy] Processing request 139792891217104-001 +INFO 2025-01-09 07:20:32,204 pyk.kore.rpc - Received response from localhost:39309: 139792891217104-001 - implies +INFO 2025-01-09 07:20:32,211 pyk.kore.rpc - Sending request to localhost:39309: 139792891217104-002 - execute +INFO 2025-01-09 07:20:33,049 pyk.kore.rpc - [PID=666580][stde] [proxy] Processing request 139792891217104-002 +INFO 2025-01-09 07:20:36,398 pyk.kore.rpc - Received response from localhost:39309: 139792891217104-002 - execute +INFO 2025-01-09 07:20:36,483 pyk.kcfg.kcfg - Extending current KCFG with the following: 4 branches: 1 --> [3, 4, 5, 6]: ['#sizeWordStack ( WS:WordStack , 0 ) <=Int 1023 andBool #if _USEGAS_CELL:Bool #then Gverylow < _SCHEDULE_CELL:Schedule > <=Gas _GAS_CELL:Gas #else true #fi andBool _WORDSTACK_CELL:WordStack ==K W0:Int : W1:Int : WS:WordStack', '#sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024', 'notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) +Int -1 >Int 1024 andBool notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) +INFO 2025-01-09 07:55:53,169 pyk.proof.reachability - [ZJH] init proof +INFO 2025-01-09 07:55:53,175 pyk.kore.rpc - Sending request to localhost:38421: 139736914874320-001 - add-module +INFO 2025-01-09 07:55:53,312 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736914874320-001 +INFO 2025-01-09 07:55:53,312 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736914875792-004 +INFO 2025-01-09 07:55:53,984 pyk.kore.rpc - Received response from localhost:38421: 139736914874320-001 - add-module +INFO 2025-01-09 07:55:54,011 pyk.kore.rpc - Sending request to localhost:38421: 139736914874320-002 - add-module +INFO 2025-01-09 07:55:54,313 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736914874320-002 +INFO 2025-01-09 07:55:54,826 pyk.kore.rpc - Received response from localhost:38421: 139736914874320-002 - add-module +INFO 2025-01-09 07:55:54,826 pyk.proof.reachability - [ZJH] pending: [1] +INFO 2025-01-09 07:55:54,826 pyk.proof.reachability - [ZJH] node_id: 1 +INFO 2025-01-09 07:55:54,827 pyk.proof.reachability - [ZJH] is_terminal: False +INFO 2025-01-09 07:55:54,827 pyk.proof.reachability - [ZJH] node_id: 2 +INFO 2025-01-09 07:55:54,827 pyk.proof.reachability - [ZJH] is_terminal: False +INFO 2025-01-09 07:55:54,827 pyk.proof.reachability - [ZJH] pending: [1] +INFO 2025-01-09 07:55:54,827 pyk.proof.proof - [ZJH] proof initialized +INFO 2025-01-09 07:55:54,827 pyk.proof.proof - [ZJH] pending: [1] +INFO 2025-01-09 07:55:54,827 pyk.proof.reachability - Before appending step: 1 +INFO 2025-01-09 07:55:54,828 pyk.kore.rpc - Connecting to host: localhost:38421 +INFO 2025-01-09 07:55:54,828 pyk.proof.proof - Submitted steps for proof: ADD_SPEC +INFO 2025-01-09 07:55:54,828 pyk.kore.rpc - Connected to host: localhost:38421 +INFO 2025-01-09 07:55:54,857 pyk.kore.rpc - Sending request to localhost:38421: 139736913433104-001 - implies +INFO 2025-01-09 07:55:55,314 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913433104-001 +INFO 2025-01-09 07:55:55,521 pyk.kore.rpc - Received response from localhost:38421: 139736913433104-001 - implies +INFO 2025-01-09 07:55:55,581 pyk.kore.rpc - Sending request to localhost:38421: 139736913433104-002 - execute +INFO 2025-01-09 07:55:56,315 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913433104-002 +INFO 2025-01-09 07:55:59,855 pyk.kore.rpc - Received response from localhost:38421: 139736913433104-002 - execute +INFO 2025-01-09 07:55:59,890 pyk.kcfg.kcfg - Extending current KCFG with the following: 4 branches: 1 --> [3, 4, 5, 6]: ['#sizeWordStack ( WS:WordStack , 0 ) <=Int 1023 andBool #if _USEGAS_CELL:Bool #then Gverylow < _SCHEDULE_CELL:Schedule > <=Gas _GAS_CELL:Gas #else true #fi andBool _WORDSTACK_CELL:WordStack ==K W0:Int : W1:Int : WS:WordStack', '#sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024', 'notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) +Int -1 >Int 1024 andBool notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) 7 +INFO 2025-01-09 07:56:04,922 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:04,924 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:04,924 pyk.proof.reachability - Before appending step: 4 +INFO 2025-01-09 07:56:04,924 pyk.proof.reachability - Before appending step: 5 +INFO 2025-01-09 07:56:04,924 pyk.proof.reachability - Before appending step: 7 +INFO 2025-01-09 07:56:04,956 pyk.kore.rpc - Sending request to localhost:38421: 139736912899408-003 - implies +INFO 2025-01-09 07:56:04,958 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912899408-003 +INFO 2025-01-09 07:56:05,588 pyk.kore.rpc - Received response from localhost:38421: 139736912899408-003 - implies +INFO 2025-01-09 07:56:05,596 pyk.kore.rpc - Sending request to localhost:38421: 139736912899408-004 - execute +INFO 2025-01-09 07:56:05,959 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912899408-004 +INFO 2025-01-09 07:56:08,109 pyk.kore.rpc - Received response from localhost:38421: 139736912821648-002 - execute +INFO 2025-01-09 07:56:08,137 pyk.kcfg.kcfg - Extending current KCFG with the following: basic block at depth 2: 4 --> 8 +INFO 2025-01-09 07:56:08,137 pyk.kore.rpc - Received response from localhost:38421: 139736912904080-002 - execute +INFO 2025-01-09 07:56:08,162 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:08,164 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:08,164 pyk.proof.reachability - Before appending step: 5 +INFO 2025-01-09 07:56:08,164 pyk.proof.reachability - Before appending step: 7 +INFO 2025-01-09 07:56:08,164 pyk.proof.reachability - Before appending step: 8 +INFO 2025-01-09 07:56:08,165 pyk.kcfg.kcfg - Extending current KCFG with the following: basic block at depth 2: 5 --> 9 +INFO 2025-01-09 07:56:08,171 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:08,172 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:08,172 pyk.proof.reachability - Before appending step: 7 +INFO 2025-01-09 07:56:08,172 pyk.proof.reachability - Before appending step: 8 +INFO 2025-01-09 07:56:08,173 pyk.proof.reachability - Before appending step: 9 +INFO 2025-01-09 07:56:08,174 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:08,175 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:08,176 pyk.proof.reachability - Before appending step: 7 +INFO 2025-01-09 07:56:08,176 pyk.proof.reachability - Before appending step: 9 +INFO 2025-01-09 07:56:08,177 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:08,178 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:08,178 pyk.proof.reachability - Before appending step: 7 +INFO 2025-01-09 07:56:09,293 pyk.kore.rpc - Received response from localhost:38421: 139736912899408-004 - execute +INFO 2025-01-09 07:56:09,303 pyk.kcfg.kcfg - Extending current KCFG with the following: 2 non-deterministic branches: 7 --> [10, 11] +INFO 2025-01-09 07:56:09,303 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:09,306 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:09,306 pyk.proof.reachability - Before appending step: 10 +INFO 2025-01-09 07:56:09,306 pyk.proof.reachability - Before appending step: 11 +INFO 2025-01-09 07:56:09,368 pyk.kore.rpc - Sending request to localhost:38421: 139736912904080-003 - implies +INFO 2025-01-09 07:56:09,369 pyk.kore.rpc - Sending request to localhost:38421: 139736912821648-003 - implies +INFO 2025-01-09 07:56:09,374 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912904080-003 +INFO 2025-01-09 07:56:09,374 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912821648-003 +INFO 2025-01-09 07:56:09,997 pyk.kore.rpc - Received response from localhost:38421: 139736912821648-003 - implies +INFO 2025-01-09 07:56:10,006 pyk.kore.rpc - Sending request to localhost:38421: 139736912821648-004 - execute +INFO 2025-01-09 07:56:10,110 pyk.kore.rpc - Received response from localhost:38421: 139736912904080-003 - implies +INFO 2025-01-09 07:56:10,196 pyk.kore.rpc - Sending request to localhost:38421: 139736912904080-004 - execute +INFO 2025-01-09 07:56:10,375 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912821648-004 +INFO 2025-01-09 07:56:10,375 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912904080-004 +INFO 2025-01-09 07:56:13,140 pyk.kore.rpc - Received response from localhost:38421: 139736912821648-004 - execute +INFO 2025-01-09 07:56:13,157 pyk.kcfg.kcfg - Extending current KCFG with the following: 2 branches: 10 --> [12, 13]: ['_USEGAS_CELL:Bool', 'notBool _USEGAS_CELL:Bool'] +INFO 2025-01-09 07:56:13,158 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:13,160 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:13,161 pyk.proof.reachability - Before appending step: 11 +INFO 2025-01-09 07:56:13,161 pyk.proof.reachability - Before appending step: 12 +INFO 2025-01-09 07:56:13,161 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:13,224 pyk.kore.rpc - Sending request to localhost:38421: 139736912899408-005 - implies +INFO 2025-01-09 07:56:13,225 pyk.kore.rpc - Sending request to localhost:38421: 139736912821648-005 - implies +INFO 2025-01-09 07:56:13,228 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912899408-005 +INFO 2025-01-09 07:56:13,900 pyk.kore.rpc - Received response from localhost:38421: 139736912899408-005 - implies +INFO 2025-01-09 07:56:13,909 pyk.kore.rpc - Sending request to localhost:38421: 139736912899408-006 - execute +INFO 2025-01-09 07:56:13,920 pyk.kore.rpc - Received response from localhost:38421: 139736912821648-005 - implies +INFO 2025-01-09 07:56:13,929 pyk.kore.rpc - Sending request to localhost:38421: 139736912821648-006 - execute +INFO 2025-01-09 07:56:14,039 pyk.kore.rpc - Received response from localhost:38421: 139736912904080-004 - execute +INFO 2025-01-09 07:56:14,049 pyk.kcfg.kcfg - Extending current KCFG with the following: 2 non-deterministic branches: 11 --> [14, 15] +INFO 2025-01-09 07:56:14,050 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:14,053 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:14,053 pyk.proof.reachability - Before appending step: 12 +INFO 2025-01-09 07:56:14,053 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:14,053 pyk.proof.reachability - Before appending step: 14 +INFO 2025-01-09 07:56:14,053 pyk.proof.reachability - Before appending step: 15 +INFO 2025-01-09 07:56:14,059 pyk.kore.rpc - Connecting to host: localhost:38421 +INFO 2025-01-09 07:56:14,084 pyk.kore.rpc - Connected to host: localhost:38421 +INFO 2025-01-09 07:56:14,086 pyk.kore.rpc - Sending request to localhost:38421: 139736912904080-005 - implies +INFO 2025-01-09 07:56:14,119 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-001 - implies +INFO 2025-01-09 07:56:14,229 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912904080-005 +INFO 2025-01-09 07:56:14,229 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-001 +INFO 2025-01-09 07:56:14,229 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912821648-005 +INFO 2025-01-09 07:56:14,229 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912899408-006 +INFO 2025-01-09 07:56:14,229 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912821648-006 +INFO 2025-01-09 07:56:14,770 pyk.kore.rpc - Received response from localhost:38421: 139736912904080-005 - implies +INFO 2025-01-09 07:56:14,779 pyk.kore.rpc - Sending request to localhost:38421: 139736912904080-006 - execute +INFO 2025-01-09 07:56:14,809 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-001 - implies +INFO 2025-01-09 07:56:14,818 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-002 - execute +INFO 2025-01-09 07:56:15,230 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912904080-006 +INFO 2025-01-09 07:56:15,230 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-002 +INFO 2025-01-09 07:56:18,418 pyk.kore.rpc - Received response from localhost:38421: 139736912904080-006 - execute +INFO 2025-01-09 07:56:18,438 pyk.kcfg.kcfg - Extending current KCFG with the following: 2 branches: 14 --> [16, 17]: ['_USEGAS_CELL:Bool', 'notBool _USEGAS_CELL:Bool'] +INFO 2025-01-09 07:56:18,438 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:18,441 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:18,441 pyk.proof.reachability - Before appending step: 12 +INFO 2025-01-09 07:56:18,442 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:18,442 pyk.proof.reachability - Before appending step: 15 +INFO 2025-01-09 07:56:18,442 pyk.proof.reachability - Before appending step: 16 +INFO 2025-01-09 07:56:18,442 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:18,448 pyk.kore.rpc - Connecting to host: localhost:38421 +INFO 2025-01-09 07:56:18,469 pyk.kore.rpc - Connected to host: localhost:38421 +INFO 2025-01-09 07:56:18,481 pyk.kore.rpc - Sending request to localhost:38421: 139736912904080-007 - implies +INFO 2025-01-09 07:56:18,491 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912904080-007 +INFO 2025-01-09 07:56:18,509 pyk.kore.rpc - Sending request to localhost:38421: 139736911122064-001 - implies +INFO 2025-01-09 07:56:19,288 pyk.kore.rpc - Received response from localhost:38421: 139736912904080-007 - implies +INFO 2025-01-09 07:56:19,297 pyk.kore.rpc - Sending request to localhost:38421: 139736912904080-008 - execute +INFO 2025-01-09 07:56:19,302 pyk.kore.rpc - Received response from localhost:38421: 139736911122064-001 - implies +INFO 2025-01-09 07:56:19,311 pyk.kore.rpc - Sending request to localhost:38421: 139736911122064-002 - execute +INFO 2025-01-09 07:56:19,491 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736911122064-002 +INFO 2025-01-09 07:56:19,492 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736911122064-001 +INFO 2025-01-09 07:56:19,492 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912904080-008 +INFO 2025-01-09 07:56:19,695 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-002 - execute +INFO 2025-01-09 07:56:19,707 pyk.kcfg.kcfg - Extending current KCFG with the following: 2 non-deterministic branches: 15 --> [18, 19] +INFO 2025-01-09 07:56:19,707 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:19,711 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:19,711 pyk.proof.reachability - Before appending step: 12 +INFO 2025-01-09 07:56:19,711 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:19,711 pyk.proof.reachability - Before appending step: 16 +INFO 2025-01-09 07:56:19,711 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:19,712 pyk.proof.reachability - Before appending step: 18 +INFO 2025-01-09 07:56:19,712 pyk.proof.reachability - Before appending step: 19 +INFO 2025-01-09 07:56:19,718 pyk.kore.rpc - Connecting to host: localhost:38421 +INFO 2025-01-09 07:56:19,744 pyk.kore.rpc - Connected to host: localhost:38421 +INFO 2025-01-09 07:56:19,746 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-003 - implies +INFO 2025-01-09 07:56:19,780 pyk.kore.rpc - Sending request to localhost:38421: 139736912761552-001 - implies +INFO 2025-01-09 07:56:19,982 pyk.kore.rpc - Received response from localhost:38421: 139736912899408-006 - execute +INFO 2025-01-09 07:56:19,996 pyk.proof.reachability - Caching next step for edge starting from 12 +INFO 2025-01-09 07:56:19,997 pyk.kcfg.kcfg - Extending current KCFG with the following: basic block at depth 4: 12 --> 20 +INFO 2025-01-09 07:56:19,998 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:20,001 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:20,001 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:20,001 pyk.proof.reachability - Before appending step: 16 +INFO 2025-01-09 07:56:20,002 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:20,002 pyk.proof.reachability - Before appending step: 18 +INFO 2025-01-09 07:56:20,002 pyk.proof.reachability - Before appending step: 19 +INFO 2025-01-09 07:56:20,002 pyk.proof.reachability - Before appending step: 20 +INFO 2025-01-09 07:56:20,035 pyk.kore.rpc - Sending request to localhost:38421: 139736912899408-007 - implies +INFO 2025-01-09 07:56:20,492 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-003 +INFO 2025-01-09 07:56:20,493 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912761552-001 +INFO 2025-01-09 07:56:20,493 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912899408-007 +INFO 2025-01-09 07:56:20,709 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-003 - implies +INFO 2025-01-09 07:56:20,719 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-004 - execute +INFO 2025-01-09 07:56:20,898 pyk.kore.rpc - Received response from localhost:38421: 139736912761552-001 - implies +INFO 2025-01-09 07:56:20,908 pyk.kore.rpc - Sending request to localhost:38421: 139736912761552-002 - execute +INFO 2025-01-09 07:56:21,021 pyk.kore.rpc - Received response from localhost:38421: 139736912899408-007 - implies +INFO 2025-01-09 07:56:21,024 pyk.proof.reachability - Using cached step for edge 12 --> 20 +INFO 2025-01-09 07:56:21,027 pyk.kcfg.kcfg - Extending current KCFG with the following: 3 non-deterministic branches: 20 --> [21, 22, 23] +INFO 2025-01-09 07:56:21,027 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:21,031 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:21,032 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:21,032 pyk.proof.reachability - Before appending step: 16 +INFO 2025-01-09 07:56:21,032 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:21,032 pyk.proof.reachability - Before appending step: 18 +INFO 2025-01-09 07:56:21,033 pyk.proof.reachability - Before appending step: 19 +INFO 2025-01-09 07:56:21,033 pyk.proof.reachability - Before appending step: 21 +INFO 2025-01-09 07:56:21,033 pyk.proof.reachability - Before appending step: 22 +INFO 2025-01-09 07:56:21,033 pyk.proof.reachability - Before appending step: 23 +INFO 2025-01-09 07:56:21,047 pyk.kore.rpc - Connecting to host: localhost:38421 +INFO 2025-01-09 07:56:21,047 pyk.kore.rpc - Connected to host: localhost:38421 +INFO 2025-01-09 07:56:21,205 pyk.kore.rpc - Sending request to localhost:38421: 139736912899408-008 - implies +INFO 2025-01-09 07:56:21,207 pyk.kore.rpc - Sending request to localhost:38421: 139736912872848-001 - implies +INFO 2025-01-09 07:56:21,496 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-004 +INFO 2025-01-09 07:56:21,496 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912899408-008 +INFO 2025-01-09 07:56:21,496 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912761552-002 +INFO 2025-01-09 07:56:21,496 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912872848-001 +INFO 2025-01-09 07:56:22,337 pyk.kore.rpc - Received response from localhost:38421: 139736912899408-008 - implies +INFO 2025-01-09 07:56:22,347 pyk.kore.rpc - Sending request to localhost:38421: 139736912899408-009 - execute +INFO 2025-01-09 07:56:22,386 pyk.kore.rpc - Received response from localhost:38421: 139736912872848-001 - implies +INFO 2025-01-09 07:56:22,396 pyk.kore.rpc - Sending request to localhost:38421: 139736912872848-002 - execute +INFO 2025-01-09 07:56:22,497 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912899408-009 +INFO 2025-01-09 07:56:22,497 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912872848-002 +INFO 2025-01-09 07:56:26,131 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-004 - execute +INFO 2025-01-09 07:56:26,157 pyk.kcfg.kcfg - Extending current KCFG with the following: 2 branches: 18 --> [24, 25]: ['_USEGAS_CELL:Bool', 'notBool _USEGAS_CELL:Bool'] +INFO 2025-01-09 07:56:26,184 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-005 - implies +INFO 2025-01-09 07:56:26,184 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:26,188 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:26,189 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:26,189 pyk.proof.reachability - Before appending step: 16 +INFO 2025-01-09 07:56:26,189 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:26,190 pyk.proof.reachability - Before appending step: 19 +INFO 2025-01-09 07:56:26,190 pyk.proof.reachability - Before appending step: 21 +INFO 2025-01-09 07:56:26,190 pyk.proof.reachability - Before appending step: 22 +INFO 2025-01-09 07:56:26,190 pyk.proof.reachability - Before appending step: 23 +INFO 2025-01-09 07:56:26,191 pyk.proof.reachability - Before appending step: 24 +INFO 2025-01-09 07:56:26,191 pyk.proof.reachability - Before appending step: 25 +INFO 2025-01-09 07:56:26,222 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-005 +INFO 2025-01-09 07:56:27,617 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-005 - implies +INFO 2025-01-09 07:56:27,628 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-006 - execute +INFO 2025-01-09 07:56:27,635 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-006 +INFO 2025-01-09 07:56:27,735 pyk.kore.rpc - Received response from localhost:38421: 139736912761552-002 - execute +INFO 2025-01-09 07:56:27,753 pyk.kcfg.kcfg - Extending current KCFG with the following: 2 non-deterministic branches: 19 --> [26, 27] +INFO 2025-01-09 07:56:27,759 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:27,780 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:27,780 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:27,780 pyk.proof.reachability - Before appending step: 16 +INFO 2025-01-09 07:56:27,781 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:27,781 pyk.proof.reachability - Before appending step: 21 +INFO 2025-01-09 07:56:27,781 pyk.proof.reachability - Before appending step: 22 +INFO 2025-01-09 07:56:27,781 pyk.proof.reachability - Before appending step: 23 +INFO 2025-01-09 07:56:27,782 pyk.proof.reachability - Before appending step: 24 +INFO 2025-01-09 07:56:27,782 pyk.proof.reachability - Before appending step: 25 +INFO 2025-01-09 07:56:27,782 pyk.proof.reachability - Before appending step: 26 +INFO 2025-01-09 07:56:27,783 pyk.proof.reachability - Before appending step: 27 +INFO 2025-01-09 07:56:27,792 pyk.kore.rpc - Sending request to localhost:38421: 139736912761552-003 - implies +INFO 2025-01-09 07:56:28,696 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912761552-003 +INFO 2025-01-09 07:56:28,706 pyk.kore.rpc - Received response from localhost:38421: 139736912904080-008 - execute +INFO 2025-01-09 07:56:28,721 pyk.proof.reachability - Caching next step for edge starting from 16 +INFO 2025-01-09 07:56:28,728 pyk.kcfg.kcfg - Extending current KCFG with the following: basic block at depth 4: 16 --> 28 +INFO 2025-01-09 07:56:28,728 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:28,732 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:28,732 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:28,733 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:28,733 pyk.proof.reachability - Before appending step: 21 +INFO 2025-01-09 07:56:28,733 pyk.proof.reachability - Before appending step: 22 +INFO 2025-01-09 07:56:28,734 pyk.proof.reachability - Before appending step: 23 +INFO 2025-01-09 07:56:28,734 pyk.proof.reachability - Before appending step: 24 +INFO 2025-01-09 07:56:28,735 pyk.proof.reachability - Before appending step: 25 +INFO 2025-01-09 07:56:28,735 pyk.proof.reachability - Before appending step: 26 +INFO 2025-01-09 07:56:28,735 pyk.proof.reachability - Before appending step: 27 +INFO 2025-01-09 07:56:28,736 pyk.proof.reachability - Before appending step: 28 +INFO 2025-01-09 07:56:28,765 pyk.kore.rpc - Sending request to localhost:38421: 139736912904080-009 - implies +INFO 2025-01-09 07:56:28,907 pyk.kore.rpc - Received response from localhost:38421: 139736912761552-003 - implies +INFO 2025-01-09 07:56:28,917 pyk.kore.rpc - Sending request to localhost:38421: 139736912761552-004 - execute +INFO 2025-01-09 07:56:29,699 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912761552-004 +INFO 2025-01-09 07:56:29,699 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912904080-009 +INFO 2025-01-09 07:56:29,963 pyk.kore.rpc - Received response from localhost:38421: 139736912904080-009 - implies +INFO 2025-01-09 07:56:29,973 pyk.kore.rpc - Sending request to localhost:38421: 139736912904080-010 - execute +INFO 2025-01-09 07:56:30,701 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912904080-010 +INFO 2025-01-09 07:56:31,411 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-006 - execute +INFO 2025-01-09 07:56:31,420 pyk.kcfg.kcfg - Extending current KCFG with the following: stuck node: 23 +INFO 2025-01-09 07:56:31,431 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:31,435 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:31,435 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:31,436 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:31,436 pyk.proof.reachability - Before appending step: 21 +INFO 2025-01-09 07:56:31,436 pyk.proof.reachability - Before appending step: 22 +INFO 2025-01-09 07:56:31,437 pyk.proof.reachability - Before appending step: 24 +INFO 2025-01-09 07:56:31,437 pyk.proof.reachability - Before appending step: 25 +INFO 2025-01-09 07:56:31,437 pyk.proof.reachability - Before appending step: 26 +INFO 2025-01-09 07:56:31,438 pyk.proof.reachability - Before appending step: 27 +INFO 2025-01-09 07:56:31,438 pyk.proof.reachability - Before appending step: 28 +INFO 2025-01-09 07:56:31,459 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-007 - implies +INFO 2025-01-09 07:56:31,705 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-007 +INFO 2025-01-09 07:56:32,530 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-007 - implies +INFO 2025-01-09 07:56:32,540 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-008 - execute +INFO 2025-01-09 07:56:32,714 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-008 +INFO 2025-01-09 07:56:36,174 pyk.kore.rpc - Received response from localhost:38421: 139736912872848-002 - execute +INFO 2025-01-09 07:56:36,205 pyk.proof.reachability - Caching next step for edge starting from 22 +INFO 2025-01-09 07:56:36,212 pyk.kcfg.kcfg - Extending current KCFG with the following: basic block at depth 4: 22 --> 29 +INFO 2025-01-09 07:56:36,212 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:36,216 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:36,216 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:36,216 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:36,217 pyk.proof.reachability - Before appending step: 21 +INFO 2025-01-09 07:56:36,217 pyk.proof.reachability - Before appending step: 24 +INFO 2025-01-09 07:56:36,217 pyk.proof.reachability - Before appending step: 25 +INFO 2025-01-09 07:56:36,218 pyk.proof.reachability - Before appending step: 26 +INFO 2025-01-09 07:56:36,218 pyk.proof.reachability - Before appending step: 27 +INFO 2025-01-09 07:56:36,219 pyk.proof.reachability - Before appending step: 28 +INFO 2025-01-09 07:56:36,219 pyk.proof.reachability - Before appending step: 29 +INFO 2025-01-09 07:56:36,251 pyk.kore.rpc - Sending request to localhost:38421: 139736912872848-003 - implies +INFO 2025-01-09 07:56:36,265 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912872848-003 +INFO 2025-01-09 07:56:37,338 pyk.kore.rpc - Received response from localhost:38421: 139736912872848-003 - implies +INFO 2025-01-09 07:56:37,348 pyk.kore.rpc - Sending request to localhost:38421: 139736912872848-004 - execute +INFO 2025-01-09 07:56:37,350 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912872848-004 +INFO 2025-01-09 07:56:38,330 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-008 - execute +INFO 2025-01-09 07:56:38,351 pyk.kcfg.kcfg - Extending current KCFG with the following: 2 branches: 26 --> [30, 31]: ['_USEGAS_CELL:Bool', 'notBool _USEGAS_CELL:Bool'] +INFO 2025-01-09 07:56:38,351 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:38,356 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:38,356 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:38,357 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:38,357 pyk.proof.reachability - Before appending step: 21 +INFO 2025-01-09 07:56:38,357 pyk.proof.reachability - Before appending step: 24 +INFO 2025-01-09 07:56:38,358 pyk.proof.reachability - Before appending step: 25 +INFO 2025-01-09 07:56:38,363 pyk.proof.reachability - Before appending step: 27 +INFO 2025-01-09 07:56:38,370 pyk.proof.reachability - Before appending step: 28 +INFO 2025-01-09 07:56:38,375 pyk.proof.reachability - Before appending step: 29 +INFO 2025-01-09 07:56:38,381 pyk.proof.reachability - Before appending step: 30 +INFO 2025-01-09 07:56:38,387 pyk.proof.reachability - Before appending step: 31 +INFO 2025-01-09 07:56:38,389 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-009 - implies +INFO 2025-01-09 07:56:38,393 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-009 +INFO 2025-01-09 07:56:38,420 pyk.kore.rpc - Received response from localhost:38421: 139736912761552-004 - execute +INFO 2025-01-09 07:56:38,536 pyk.proof.reachability - Caching next step for edge starting from 24 +INFO 2025-01-09 07:56:38,542 pyk.kcfg.kcfg - Extending current KCFG with the following: basic block at depth 4: 24 --> 32 +INFO 2025-01-09 07:56:38,558 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:38,574 pyk.kore.rpc - Sending request to localhost:38421: 139736912761552-005 - implies +INFO 2025-01-09 07:56:38,577 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:38,578 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:38,578 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:38,578 pyk.proof.reachability - Before appending step: 21 +INFO 2025-01-09 07:56:38,579 pyk.proof.reachability - Before appending step: 25 +INFO 2025-01-09 07:56:38,579 pyk.proof.reachability - Before appending step: 27 +INFO 2025-01-09 07:56:38,580 pyk.proof.reachability - Before appending step: 28 +INFO 2025-01-09 07:56:38,580 pyk.proof.reachability - Before appending step: 29 +INFO 2025-01-09 07:56:38,580 pyk.proof.reachability - Before appending step: 30 +INFO 2025-01-09 07:56:38,581 pyk.proof.reachability - Before appending step: 31 +INFO 2025-01-09 07:56:38,581 pyk.proof.reachability - Before appending step: 32 +INFO 2025-01-09 07:56:38,583 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:38,587 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:38,587 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:38,588 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:38,588 pyk.proof.reachability - Before appending step: 21 +INFO 2025-01-09 07:56:38,588 pyk.proof.reachability - Before appending step: 25 +INFO 2025-01-09 07:56:38,589 pyk.proof.reachability - Before appending step: 27 +INFO 2025-01-09 07:56:38,589 pyk.proof.reachability - Before appending step: 28 +INFO 2025-01-09 07:56:38,589 pyk.proof.reachability - Before appending step: 30 +INFO 2025-01-09 07:56:38,590 pyk.proof.reachability - Before appending step: 31 +INFO 2025-01-09 07:56:38,590 pyk.proof.reachability - Before appending step: 32 +INFO 2025-01-09 07:56:39,405 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912761552-005 +INFO 2025-01-09 07:56:39,452 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-009 - implies +INFO 2025-01-09 07:56:39,455 pyk.proof.reachability - Using cached step for edge 16 --> 28 +INFO 2025-01-09 07:56:39,463 pyk.kcfg.kcfg - Extending current KCFG with the following: 3 non-deterministic branches: 28 --> [33, 34, 35] +INFO 2025-01-09 07:56:39,478 pyk.proof.reachability - Wrote proof data for ADD_SPEC: /home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/proofs/ADD_SPEC/proof.json +INFO 2025-01-09 07:56:39,495 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-010 - implies +INFO 2025-01-09 07:56:39,500 pyk.proof.reachability - Before appending step: 3 +INFO 2025-01-09 07:56:39,500 pyk.proof.reachability - Before appending step: 13 +INFO 2025-01-09 07:56:39,501 pyk.proof.reachability - Before appending step: 17 +INFO 2025-01-09 07:56:39,501 pyk.proof.reachability - Before appending step: 21 +INFO 2025-01-09 07:56:39,501 pyk.proof.reachability - Before appending step: 25 +INFO 2025-01-09 07:56:39,502 pyk.proof.reachability - Before appending step: 27 +INFO 2025-01-09 07:56:39,502 pyk.proof.reachability - Before appending step: 30 +INFO 2025-01-09 07:56:39,503 pyk.proof.reachability - Before appending step: 31 +INFO 2025-01-09 07:56:39,503 pyk.proof.reachability - Before appending step: 32 +INFO 2025-01-09 07:56:39,504 pyk.proof.reachability - Before appending step: 33 +INFO 2025-01-09 07:56:39,504 pyk.proof.reachability - Before appending step: 34 +INFO 2025-01-09 07:56:39,505 pyk.proof.reachability - Before appending step: 35 +INFO 2025-01-09 07:56:39,616 pyk.kore.rpc - Received response from localhost:38421: 139736912761552-005 - implies +INFO 2025-01-09 07:56:39,627 pyk.kore.rpc - Sending request to localhost:38421: 139736912761552-006 - execute +INFO 2025-01-09 07:56:40,406 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912761552-006 +INFO 2025-01-09 07:56:40,406 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-010 +INFO 2025-01-09 07:56:40,885 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-010 - implies +INFO 2025-01-09 07:56:40,896 pyk.kore.rpc - Sending request to localhost:38421: 139736913677584-011 - execute +INFO 2025-01-09 07:56:41,408 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736913677584-011 +INFO 2025-01-09 07:56:42,874 pyk.kore.rpc - Received response from localhost:38421: 139736912872848-004 - execute +INFO 2025-01-09 07:56:42,915 pyk.kore.rpc - Sending request to localhost:38421: 139736912872848-005 - implies +INFO 2025-01-09 07:56:42,926 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912872848-005 +INFO 2025-01-09 07:56:43,950 pyk.kore.rpc - Received response from localhost:38421: 139736912872848-005 - implies +INFO 2025-01-09 07:56:43,953 pyk.proof.reachability - Using cached step for edge 24 --> 32 +INFO 2025-01-09 07:56:43,987 pyk.kore.rpc - Sending request to localhost:38421: 139736912872848-006 - implies +INFO 2025-01-09 07:56:44,007 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912872848-006 +INFO 2025-01-09 07:56:45,045 pyk.kore.rpc - Received response from localhost:38421: 139736912872848-006 - implies +INFO 2025-01-09 07:56:45,055 pyk.kore.rpc - Sending request to localhost:38421: 139736912872848-007 - execute +INFO 2025-01-09 07:56:45,063 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912872848-007 +INFO 2025-01-09 07:56:50,043 pyk.kore.rpc - Received response from localhost:38421: 139736912761552-006 - execute +INFO 2025-01-09 07:56:50,060 pyk.proof.reachability - Caching next step for edge starting from 30 +INFO 2025-01-09 07:56:50,093 pyk.kore.rpc - Sending request to localhost:38421: 139736912761552-007 - implies +INFO 2025-01-09 07:56:50,097 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912761552-007 +INFO 2025-01-09 07:56:51,395 pyk.kore.rpc - Received response from localhost:38421: 139736912761552-007 - implies +INFO 2025-01-09 07:56:51,405 pyk.kore.rpc - Sending request to localhost:38421: 139736912761552-008 - execute +INFO 2025-01-09 07:56:51,407 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912761552-008 +INFO 2025-01-09 07:57:06,261 pyk.kore.rpc - Received response from localhost:38421: 139736912761552-008 - execute +INFO 2025-01-09 07:57:06,297 pyk.proof.reachability - Caching next step for edge starting from 34 +INFO 2025-01-09 07:57:06,331 pyk.kore.rpc - Sending request to localhost:38421: 139736912761552-009 - implies +INFO 2025-01-09 07:57:06,335 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912761552-009 +INFO 2025-01-09 07:57:07,567 pyk.kore.rpc - Received response from localhost:38421: 139736912761552-009 - implies +INFO 2025-01-09 07:57:07,578 pyk.kore.rpc - Sending request to localhost:38421: 139736912761552-010 - execute +INFO 2025-01-09 07:57:07,581 pyk.kore.rpc - [PID=692183][stde] [proxy] Processing request 139736912761552-010 +INFO 2025-01-09 07:57:11,673 pyk.kore.rpc - Received response from localhost:38421: 139736912761552-010 - execute +INFO 2025-01-09 07:57:17,194 pyk.kore.rpc - Received response from localhost:38421: 139736913433104-004 - execute +INFO 2025-01-09 07:57:36,321 pyk.kore.rpc - Received response from localhost:38421: 139736912821648-006 - execute +INFO 2025-01-09 07:57:38,675 pyk.kore.rpc - Received response from localhost:38421: 139736912899408-009 - execute +INFO 2025-01-09 07:57:44,964 pyk.kore.rpc - Received response from localhost:38421: 139736911122064-002 - execute +INFO 2025-01-09 07:57:54,298 pyk.kore.rpc - Received response from localhost:38421: 139736913677584-011 - execute +INFO 2025-01-09 07:57:54,678 pyk.kore.rpc - Received response from localhost:38421: 139736912904080-010 - execute +INFO 2025-01-09 07:57:56,677 pyk.kore.rpc - Received response from localhost:38421: 139736912872848-007 - execute +ERROR 2025-01-09 07:57:56,677 kevm_pyk.utils - Proof crashed: ADD_SPEC +{ false #Equals #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) +Int -1 >Int 1024 } +#And { false #Equals #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024 } +#And { false #Equals #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) _K_CELL:K +│ pc: _PC_CELL:Int +│ callDepth: _CALLDEPTH_CELL:Int +│ statusCode: _STATUSCODE_CELL:StatusCode +┃ +┃ (branch) +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023 +┃ ┃ _WORDSTACK_CELL:WordStack ==K ( W0:Int : ( W1:Int : WS:WordStack ) ) +┃ ┃ #if _USEGAS_CELL:Bool #then Gverylow < _SCHEDULE_CELL:Schedule > <=Gas _GAS_CELL:Gas #else true #fi +┃ │ +┃ └─ 3 (leaf, pending) +┃ k: #next [ ADD ] ~> _K_CELL:K +┃ pc: _PC_CELL:Int +┃ callDepth: _CALLDEPTH_CELL:Int +┃ statusCode: _STATUSCODE_CELL:StatusCode +┃ +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) _K_CELL:K +┃ │ pc: _PC_CELL:Int +┃ │ callDepth: _CALLDEPTH_CELL:Int +┃ │ statusCode: _STATUSCODE_CELL:StatusCode +┃ │ +┃ │ (2 steps) +┃ └─ 8 (leaf, terminal) +┃ k: #halt ~> _K_CELL:K +┃ pc: _PC_CELL:Int +┃ callDepth: _CALLDEPTH_CELL:Int +┃ statusCode: EVMC_STACK_UNDERFLOW +┃ +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ ( #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) +Int -1 ) >Int 1024 +┃ │ +┃ ├─ 5 +┃ │ k: #next [ ADD ] ~> _K_CELL:K +┃ │ pc: _PC_CELL:Int +┃ │ callDepth: _CALLDEPTH_CELL:Int +┃ │ statusCode: _STATUSCODE_CELL:StatusCode +┃ │ +┃ │ (2 steps) +┃ └─ 9 (leaf, terminal) +┃ k: #halt ~> _K_CELL:K +┃ pc: _PC_CELL:Int +┃ callDepth: _CALLDEPTH_CELL:Int +┃ statusCode: EVMC_STACK_OVERFLOW +┃ +┗━━┓ subst: .Subst + ┃ constraint: + ┃ ( notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024 ) + │ + ├─ 6 + │ k: #next [ ADD ] ~> _K_CELL:K + │ pc: _PC_CELL:Int + │ callDepth: _CALLDEPTH_CELL:Int + │ statusCode: _STATUSCODE_CELL:StatusCode + │ + │ (2 steps) + ├─ 7 + │ k: #exec [ ADD ] ~> #pc [ ADD ] ~> _K_CELL:K + │ pc: _PC_CELL:Int + │ callDepth: _CALLDEPTH_CELL:Int + │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┃ (1 step) + ┣━━┓ + ┃ │ + ┃ ├─ 10 (split) + ┃ │ k: #gas [ ADD , ADD W0:Int W1:Int ] ~> ADD W0:Int W1:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ │ pc: _PC_CELL:Int + ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┃ (branch) + ┃ ┣━━┓ subst: .Subst + ┃ ┃ ┃ constraint: + ┃ ┃ ┃ _USEGAS_CELL:Bool + ┃ ┃ │ + ┃ ┃ ├─ 12 + ┃ ┃ │ k: #gas [ ADD , ADD W0:Int W1:Int ] ~> ADD W0:Int W1:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ │ + ┃ ┃ │ (4 steps) + ┃ ┃ ├─ 20 + ┃ ┃ │ k: Gverylow < _SCHEDULE_CELL:Schedule > ~> #deductGas ~> #access [ ADD , ADD W0:Int ... + ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ + ┃ ┃ ┃ (1 step) + ┃ ┃ ┣━━┓ + ┃ ┃ ┃ │ + ┃ ┃ ┃ └─ 21 (leaf, pending) + ┃ ┃ ┃ k: #access [ ADD , ADD W0:Int W1:Int ] ~> ADD W0:Int W1:Int ~> #pc [ ADD ] ~> _K_CE ... + ┃ ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ + ┃ ┃ ┣━━┓ + ┃ ┃ ┃ │ + ┃ ┃ ┃ ├─ 22 + ┃ ┃ ┃ │ k: #end EVMC_OUT_OF_GAS ~> #access [ ADD , ADD W0:Int W1:Int ] ~> ADD W0:Int W1:Int ... + ┃ ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ │ + ┃ ┃ ┃ │ (4 steps) + ┃ ┃ ┃ └─ 29 (leaf, terminal) + ┃ ┃ ┃ k: #halt ~> _K_CELL:K + ┃ ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ ┃ statusCode: EVMC_OUT_OF_GAS + ┃ ┃ ┃ + ┃ ┃ ┗━━┓ + ┃ ┃ │ + ┃ ┃ └─ 23 (stuck, leaf) + ┃ ┃ k: Gverylow < _SCHEDULE_CELL:Schedule > ~> #deductGas ~> #access [ ADD , ADD W0:Int ... + ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┗━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ ( notBool _USEGAS_CELL:Bool ) + ┃ │ + ┃ └─ 13 (leaf, pending) + ┃ k: #gas [ ADD , ADD W0:Int W1:Int ] ~> ADD W0:Int W1:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ pc: _PC_CELL:Int + ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┗━━┓ + │ + ├─ 11 + │ k: #exec [ ADD ] ~> #pc [ ADD ] ~> _K_CELL:K + │ pc: _PC_CELL:Int + │ callDepth: _CALLDEPTH_CELL:Int + │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┃ (1 step) + ┣━━┓ + ┃ │ + ┃ ├─ 14 (split) + ┃ │ k: #gas [ ADD , ADD W0:Int W2:Int ] ~> ADD W0:Int W2:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ │ pc: _PC_CELL:Int + ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┃ (branch) + ┃ ┣━━┓ subst: .Subst + ┃ ┃ ┃ constraint: + ┃ ┃ ┃ _USEGAS_CELL:Bool + ┃ ┃ │ + ┃ ┃ ├─ 16 + ┃ ┃ │ k: #gas [ ADD , ADD W0:Int W2:Int ] ~> ADD W0:Int W2:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ │ + ┃ ┃ │ (4 steps) + ┃ ┃ ├─ 28 + ┃ ┃ │ k: Gverylow < _SCHEDULE_CELL:Schedule > ~> #deductGas ~> #access [ ADD , ADD W0:Int ... + ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ + ┃ ┃ ┃ (1 step) + ┃ ┃ ┣━━┓ + ┃ ┃ ┃ │ + ┃ ┃ ┃ └─ 33 (leaf, pending) + ┃ ┃ ┃ k: #access [ ADD , ADD W0:Int W2:Int ] ~> ADD W0:Int W2:Int ~> #pc [ ADD ] ~> _K_CE ... + ┃ ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ + ┃ ┃ ┣━━┓ + ┃ ┃ ┃ │ + ┃ ┃ ┃ └─ 34 (leaf, pending) + ┃ ┃ ┃ k: #end EVMC_OUT_OF_GAS ~> #access [ ADD , ADD W0:Int W2:Int ] ~> ADD W0:Int W2:Int ... + ┃ ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ + ┃ ┃ ┗━━┓ + ┃ ┃ │ + ┃ ┃ └─ 35 (leaf, pending) + ┃ ┃ k: Gverylow < _SCHEDULE_CELL:Schedule > ~> #deductGas ~> #access [ ADD , ADD W0:Int ... + ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┗━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ ( notBool _USEGAS_CELL:Bool ) + ┃ │ + ┃ └─ 17 (leaf, pending) + ┃ k: #gas [ ADD , ADD W0:Int W2:Int ] ~> ADD W0:Int W2:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ pc: _PC_CELL:Int + ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┗━━┓ + │ + ├─ 15 + │ k: #exec [ ADD ] ~> #pc [ ADD ] ~> _K_CELL:K + │ pc: _PC_CELL:Int + │ callDepth: _CALLDEPTH_CELL:Int + │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┃ (1 step) + ┣━━┓ + ┃ │ + ┃ ├─ 18 (split) + ┃ │ k: #gas [ ADD , ADD W0:Int W3:Int ] ~> ADD W0:Int W3:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ │ pc: _PC_CELL:Int + ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┃ (branch) + ┃ ┣━━┓ subst: .Subst + ┃ ┃ ┃ constraint: + ┃ ┃ ┃ _USEGAS_CELL:Bool + ┃ ┃ │ + ┃ ┃ ├─ 24 + ┃ ┃ │ k: #gas [ ADD , ADD W0:Int W3:Int ] ~> ADD W0:Int W3:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ │ + ┃ ┃ │ (4 steps) + ┃ ┃ └─ 32 (leaf, pending) + ┃ ┃ k: Gverylow < _SCHEDULE_CELL:Schedule > ~> #deductGas ~> #access [ ADD , ADD W0:Int ... + ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┗━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ ( notBool _USEGAS_CELL:Bool ) + ┃ │ + ┃ └─ 25 (leaf, pending) + ┃ k: #gas [ ADD , ADD W0:Int W3:Int ] ~> ADD W0:Int W3:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ pc: _PC_CELL:Int + ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┗━━┓ + │ + ├─ 19 + │ k: #exec [ ADD ] ~> #pc [ ADD ] ~> _K_CELL:K + │ pc: _PC_CELL:Int + │ callDepth: _CALLDEPTH_CELL:Int + │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┃ (1 step) + ┣━━┓ + ┃ │ + ┃ ├─ 26 (split) + ┃ │ k: #gas [ ADD , ADD W0:Int W4:Int ] ~> ADD W0:Int W4:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ │ pc: _PC_CELL:Int + ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┃ (branch) + ┃ ┣━━┓ subst: .Subst + ┃ ┃ ┃ constraint: + ┃ ┃ ┃ _USEGAS_CELL:Bool + ┃ ┃ │ + ┃ ┃ └─ 30 (leaf, pending) + ┃ ┃ k: #gas [ ADD , ADD W0:Int W4:Int ] ~> ADD W0:Int W4:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┗━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ ( notBool _USEGAS_CELL:Bool ) + ┃ │ + ┃ └─ 31 (leaf, pending) + ┃ k: #gas [ ADD , ADD W0:Int W4:Int ] ~> ADD W0:Int W4:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ pc: _PC_CELL:Int + ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┗━━┓ + │ + └─ 27 (leaf, pending) + k: #exec [ ADD ] ~> #pc [ ADD ] ~> _K_CELL:K + pc: _PC_CELL:Int + callDepth: _CALLDEPTH_CELL:Int + statusCode: _STATUSCODE_CELL:StatusCode + + +┌─ 2 (root, leaf, target) +│ k: _K_CELL:K +│ pc: ?_FINAL_PC_CELL:Int +│ callDepth: ?_FINAL_CALLDEPTH_CELL:Int +│ statusCode: ?_FINAL_STATUSCODE_CELL:StatusCode + + +Node 1: + + + + + #next [ ADD ] + ~> _K_CELL:K + + ... + + ... + + + + +Node 2: + +... + + + +Node 3: + +( + + + #next [ ADD ] + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + _USEGAS_CELL:Bool + + + + + + _WORDSTACK_CELL:WordStack + + + _GAS_CELL:Gas + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023 } +#And ( { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W1:Int : WS:WordStack ) ) } +#And { true #Equals #if _USEGAS_CELL:Bool #then Gverylow < _SCHEDULE_CELL:Schedule > <=Gas _GAS_CELL:Gas #else true #fi } ) ) ) + + + +Node 4: + +( + + + #next [ ADD ] + ~> _K_CELL:K + + + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + ... + +#And { true #Equals #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) + + + #next [ ADD ] + ~> _K_CELL:K + + + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + ... + +#And { true #Equals ( #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) +Int -1 ) >Int 1024 } ) + + + +Node 6: + +( + + + #next [ ADD ] + ~> _K_CELL:K + + + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { false #Equals #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024 } ) ) + + + +Node 7: + +( + + + #exec [ ADD ] + ~> #pc [ ADD ] + ~> _K_CELL:K + + + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals ( notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024 ) } ) ) + + + +Node 8: + +( + + + #halt + ~> _K_CELL:K + + + + + EVMC_STACK_UNDERFLOW + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + ... + +#And { true #Equals #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) + + + #halt + ~> _K_CELL:K + + + + + EVMC_STACK_OVERFLOW + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + ... + +#And { true #Equals ( #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) +Int -1 ) >Int 1024 } ) + + + +Node 10: + +( + + + #gas [ ADD , ADD W0:Int W1:Int ] + ~> ADD W0:Int W1:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + + + + WS:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals ( notBool #sizeWordStack ( WS:WordStack , 2 ) Int 1024 ) } ) ) ) + + + +Node 11: + +( + + + #exec [ ADD ] + ~> #pc [ ADD ] + ~> _K_CELL:K + + + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals ( notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024 ) } +#And #Not ( #Exists W0:Int . #Exists W1:Int . #Exists WS:WordStack . { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W1:Int : WS:WordStack ) ) } ) ) ) ) + + + +Node 12: + +( + + + #gas [ ADD , ADD W0:Int W1:Int ] + ~> ADD W0:Int W1:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _USEGAS_CELL:Bool + + + + + + WS:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { _USEGAS_CELL:Bool #Equals true } +#And ( { true #Equals ( notBool #sizeWordStack ( WS:WordStack , 2 ) Int 1024 ) } ) ) ) ) + + + +Node 13: + +( + + + #gas [ ADD , ADD W0:Int W1:Int ] + ~> ADD W0:Int W1:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _USEGAS_CELL:Bool + + + + + + WS:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { _USEGAS_CELL:Bool #Equals false } +#And ( { true #Equals ( notBool #sizeWordStack ( WS:WordStack , 2 ) Int 1024 ) } ) ) ) ) + + + +Node 14: + +( + + + #gas [ ADD , ADD W0:Int W2:Int ] + ~> ADD W0:Int W2:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + + + + WS0:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals ( notBool #sizeWordStack ( WS0:WordStack , 2 ) Int 1024 ) } +#And #Not ( ( { W1:Int #Equals W2:Int } +#And { WS:WordStack #Equals WS0:WordStack } ) ) ) ) ) ) + + + +Node 15: + +( + + + #exec [ ADD ] + ~> #pc [ ADD ] + ~> _K_CELL:K + + + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals ( notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024 ) } +#And ( #Not ( #Exists W0:Int . { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W1:Int : WS:WordStack ) ) } ) +#And #Not ( #Exists W0:Int . #Exists W2:Int . #Exists WS0:WordStack . { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W2:Int : WS0:WordStack ) ) } ) ) ) ) ) + + + +Node 16: + +( + + + #gas [ ADD , ADD W0:Int W2:Int ] + ~> ADD W0:Int W2:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _USEGAS_CELL:Bool + + + + + + WS0:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { _USEGAS_CELL:Bool #Equals true } +#And ( { true #Equals ( notBool #sizeWordStack ( WS0:WordStack , 2 ) Int 1024 ) } +#And #Not ( ( { W1:Int #Equals W2:Int } +#And { WS:WordStack #Equals WS0:WordStack } ) ) ) ) ) ) ) + + + +Node 17: + +( + + + #gas [ ADD , ADD W0:Int W2:Int ] + ~> ADD W0:Int W2:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _USEGAS_CELL:Bool + + + + + + WS0:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { _USEGAS_CELL:Bool #Equals false } +#And ( { true #Equals ( notBool #sizeWordStack ( WS0:WordStack , 2 ) Int 1024 ) } +#And #Not ( ( { W1:Int #Equals W2:Int } +#And { WS:WordStack #Equals WS0:WordStack } ) ) ) ) ) ) ) + + + +Node 18: + +( + + + #gas [ ADD , ADD W0:Int W3:Int ] + ~> ADD W0:Int W3:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + + + + WS1:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals ( notBool #sizeWordStack ( WS1:WordStack , 2 ) Int 1024 ) } +#And ( #Not ( ( { W1:Int #Equals W3:Int } +#And { WS:WordStack #Equals WS1:WordStack } ) ) +#And #Not ( ( { W2:Int #Equals W3:Int } +#And { WS0:WordStack #Equals WS1:WordStack } ) ) ) ) ) ) ) + + + +Node 19: + +( + + + #exec [ ADD ] + ~> #pc [ ADD ] + ~> _K_CELL:K + + + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals ( notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024 ) } +#And ( #Not ( #Exists W0:Int . { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W1:Int : WS:WordStack ) ) } ) +#And ( #Not ( #Exists W0:Int . { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W2:Int : WS0:WordStack ) ) } ) +#And #Not ( #Exists W0:Int . #Exists W3:Int . #Exists WS1:WordStack . { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W3:Int : WS1:WordStack ) ) } ) ) ) ) ) ) + + + +Node 20: + +( + + + Gverylow < _SCHEDULE_CELL:Schedule > + ~> #deductGas + ~> #access [ ADD , ADD W0:Int W1:Int ] + ~> ADD W0:Int W1:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + true + + + + + + WS:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals _USEGAS_CELL:Bool } +#And ( { true #Equals ( notBool #sizeWordStack ( WS:WordStack , 2 ) Int 1024 ) } ) ) ) ) + + + +Node 21: + +( + + + #access [ ADD , ADD W0:Int W1:Int ] + ~> ADD W0:Int W1:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + true + + + + + + WS:WordStack + + + _GAS_CELL:Gas -Gas Gverylow < _SCHEDULE_CELL:Schedule > + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals _USEGAS_CELL:Bool } +#And ( { true #Equals ( notBool #sizeWordStack ( WS:WordStack , 2 ) <=Gas _GAS_CELL:Gas } +#And { true #Equals ( notBool ( #sizeWordStack ( WS:WordStack , 2 ) +Int -1 ) >Int 1024 ) } ) ) ) ) ) + + + +Node 22: + +( + + + #end EVMC_OUT_OF_GAS + ~> #access [ ADD , ADD W0:Int W1:Int ] + ~> ADD W0:Int W1:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + true + + + + + + WS:WordStack + + + _GAS_CELL:Gas + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals _USEGAS_CELL:Bool } +#And ( { true #Equals ( notBool #sizeWordStack ( WS:WordStack , 2 ) } +#And { true #Equals ( notBool ( #sizeWordStack ( WS:WordStack , 2 ) +Int -1 ) >Int 1024 ) } ) ) ) ) ) + + + +Node 23: + +( + + + Gverylow < _SCHEDULE_CELL:Schedule > + ~> #deductGas + ~> #access [ ADD , ADD W0:Int W1:Int ] + ~> ADD W0:Int W1:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + true + + + + + + WS:WordStack + + + _GAS_CELL:Gas + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals _USEGAS_CELL:Bool } +#And ( { true #Equals ( notBool #sizeWordStack ( WS:WordStack , 2 ) Int 1024 ) } +#And ( { true #Equals ( notBool _GAS_CELL:Gas ) } +#And { true #Equals ( notBool Gverylow < _SCHEDULE_CELL:Schedule > <=Gas _GAS_CELL:Gas ) } ) ) ) ) ) ) + + + +Node 24: + +( + + + #gas [ ADD , ADD W0:Int W3:Int ] + ~> ADD W0:Int W3:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _USEGAS_CELL:Bool + + + + + + WS1:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { _USEGAS_CELL:Bool #Equals true } +#And ( { true #Equals ( notBool #sizeWordStack ( WS1:WordStack , 2 ) Int 1024 ) } +#And ( #Not ( ( { W1:Int #Equals W3:Int } +#And { WS:WordStack #Equals WS1:WordStack } ) ) +#And #Not ( ( { W2:Int #Equals W3:Int } +#And { WS0:WordStack #Equals WS1:WordStack } ) ) ) ) ) ) ) ) + + + +Node 25: + +( + + + #gas [ ADD , ADD W0:Int W3:Int ] + ~> ADD W0:Int W3:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _USEGAS_CELL:Bool + + + + + + WS1:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { _USEGAS_CELL:Bool #Equals false } +#And ( { true #Equals ( notBool #sizeWordStack ( WS1:WordStack , 2 ) Int 1024 ) } +#And ( #Not ( ( { W1:Int #Equals W3:Int } +#And { WS:WordStack #Equals WS1:WordStack } ) ) +#And #Not ( ( { W2:Int #Equals W3:Int } +#And { WS0:WordStack #Equals WS1:WordStack } ) ) ) ) ) ) ) ) + + + +Node 26: + +( + + + #gas [ ADD , ADD W0:Int W4:Int ] + ~> ADD W0:Int W4:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + + + + WS2:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals ( notBool #sizeWordStack ( WS2:WordStack , 2 ) Int 1024 ) } +#And ( #Not ( ( { W1:Int #Equals W4:Int } +#And { WS:WordStack #Equals WS2:WordStack } ) ) +#And ( #Not ( ( { W2:Int #Equals W4:Int } +#And { WS0:WordStack #Equals WS2:WordStack } ) ) +#And #Not ( ( { W3:Int #Equals W4:Int } +#And { WS1:WordStack #Equals WS2:WordStack } ) ) ) ) ) ) ) ) + + + +Node 27: + +( + + + #exec [ ADD ] + ~> #pc [ ADD ] + ~> _K_CELL:K + + + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals ( notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024 ) } +#And ( #Not ( #Exists W0:Int . { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W1:Int : WS:WordStack ) ) } ) +#And ( #Not ( #Exists W0:Int . { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W2:Int : WS0:WordStack ) ) } ) +#And ( #Not ( #Exists W0:Int . { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W3:Int : WS1:WordStack ) ) } ) +#And #Not ( #Exists W0:Int . #Exists W4:Int . #Exists WS2:WordStack . { _WORDSTACK_CELL:WordStack #Equals ( W0:Int : ( W4:Int : WS2:WordStack ) ) } ) ) ) ) ) ) ) + + + +Node 28: + +( + + + Gverylow < _SCHEDULE_CELL:Schedule > + ~> #deductGas + ~> #access [ ADD , ADD W0:Int W2:Int ] + ~> ADD W0:Int W2:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + true + + + + + + WS0:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals _USEGAS_CELL:Bool } +#And ( { true #Equals ( notBool #sizeWordStack ( WS0:WordStack , 2 ) Int 1024 ) } +#And #Not ( ( { W1:Int #Equals W2:Int } +#And { WS:WordStack #Equals WS0:WordStack } ) ) ) ) ) ) ) + + + +Node 29: + +( + + + #halt + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + true + + + + + EVMC_OUT_OF_GAS + + + + WS:WordStack + + + _GAS_CELL:Gas + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals _USEGAS_CELL:Bool } +#And ( { true #Equals ( notBool #sizeWordStack ( WS:WordStack , 2 ) } +#And { true #Equals ( notBool ( #sizeWordStack ( WS:WordStack , 2 ) +Int -1 ) >Int 1024 ) } ) ) ) ) ) + + + +Node 30: + +( + + + #gas [ ADD , ADD W0:Int W4:Int ] + ~> ADD W0:Int W4:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _USEGAS_CELL:Bool + + + + + + WS2:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { _USEGAS_CELL:Bool #Equals true } +#And ( { true #Equals ( notBool #sizeWordStack ( WS2:WordStack , 2 ) Int 1024 ) } +#And ( #Not ( ( { W1:Int #Equals W4:Int } +#And { WS:WordStack #Equals WS2:WordStack } ) ) +#And ( #Not ( ( { W2:Int #Equals W4:Int } +#And { WS0:WordStack #Equals WS2:WordStack } ) ) +#And #Not ( ( { W3:Int #Equals W4:Int } +#And { WS1:WordStack #Equals WS2:WordStack } ) ) ) ) ) ) ) ) ) + + + +Node 31: + +( + + + #gas [ ADD , ADD W0:Int W4:Int ] + ~> ADD W0:Int W4:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _USEGAS_CELL:Bool + + + + + + WS2:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { _USEGAS_CELL:Bool #Equals false } +#And ( { true #Equals ( notBool #sizeWordStack ( WS2:WordStack , 2 ) Int 1024 ) } +#And ( #Not ( ( { W1:Int #Equals W4:Int } +#And { WS:WordStack #Equals WS2:WordStack } ) ) +#And ( #Not ( ( { W2:Int #Equals W4:Int } +#And { WS0:WordStack #Equals WS2:WordStack } ) ) +#And #Not ( ( { W3:Int #Equals W4:Int } +#And { WS1:WordStack #Equals WS2:WordStack } ) ) ) ) ) ) ) ) ) + + + +Node 32: + +( + + + Gverylow < _SCHEDULE_CELL:Schedule > + ~> #deductGas + ~> #access [ ADD , ADD W0:Int W3:Int ] + ~> ADD W0:Int W3:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + true + + + + + + WS1:WordStack + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals _USEGAS_CELL:Bool } +#And ( { true #Equals ( notBool #sizeWordStack ( WS1:WordStack , 2 ) Int 1024 ) } +#And ( #Not ( ( { W1:Int #Equals W3:Int } +#And { WS:WordStack #Equals WS1:WordStack } ) ) +#And #Not ( ( { W2:Int #Equals W3:Int } +#And { WS0:WordStack #Equals WS1:WordStack } ) ) ) ) ) ) ) ) + + + +Node 33: + +( + + + #access [ ADD , ADD W0:Int W2:Int ] + ~> ADD W0:Int W2:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + true + + + + + + WS0:WordStack + + + _GAS_CELL:Gas -Gas Gverylow < _SCHEDULE_CELL:Schedule > + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals _USEGAS_CELL:Bool } +#And ( { true #Equals ( notBool #sizeWordStack ( WS0:WordStack , 2 ) <=Gas _GAS_CELL:Gas } +#And ( { true #Equals ( notBool ( #sizeWordStack ( WS0:WordStack , 2 ) +Int -1 ) >Int 1024 ) } +#And #Not ( ( { W1:Int #Equals W2:Int } +#And { WS:WordStack #Equals WS0:WordStack } ) ) ) ) ) ) ) ) + + + +Node 34: + +( + + + #end EVMC_OUT_OF_GAS + ~> #access [ ADD , ADD W0:Int W2:Int ] + ~> ADD W0:Int W2:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + true + + + + + + WS0:WordStack + + + _GAS_CELL:Gas + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals _USEGAS_CELL:Bool } +#And ( { true #Equals ( notBool #sizeWordStack ( WS0:WordStack , 2 ) } +#And ( { true #Equals ( notBool ( #sizeWordStack ( WS0:WordStack , 2 ) +Int -1 ) >Int 1024 ) } +#And #Not ( ( { W1:Int #Equals W2:Int } +#And { WS:WordStack #Equals WS0:WordStack } ) ) ) ) ) ) ) ) + + + +Node 35: + +( + + + Gverylow < _SCHEDULE_CELL:Schedule > + ~> #deductGas + ~> #access [ ADD , ADD W0:Int W2:Int ] + ~> ADD W0:Int W2:Int + ~> #pc [ ADD ] + ~> _K_CELL:K + + + _SCHEDULE_CELL:Schedule + + + true + + + + + + WS0:WordStack + + + _GAS_CELL:Gas + + ... + + ... + + ... + + ... + + ... + +#And ( { true #Equals _USEGAS_CELL:Bool } +#And ( { true #Equals ( notBool #sizeWordStack ( WS0:WordStack , 2 ) Int 1024 ) } +#And ( { true #Equals ( notBool _GAS_CELL:Gas ) } +#And ( { true #Equals ( notBool Gverylow < _SCHEDULE_CELL:Schedule > <=Gas _GAS_CELL:Gas ) } +#And #Not ( ( { W1:Int #Equals W2:Int } +#And { WS:WordStack #Equals WS0:WordStack } ) ) ) ) ) ) ) ) ) + + + diff --git a/kevm-pyk/src/kevm_pyk/summaries/ADD_SPEC/summary.md b/kevm-pyk/src/kevm_pyk/summaries/ADD_SPEC/summary.md new file mode 100644 index 0000000000..b16994b515 --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/summaries/ADD_SPEC/summary.md @@ -0,0 +1,543 @@ + +┌─ 1 (root, split, init) +│ k: #next [ ADD ] ~> _K_CELL:K +│ pc: _PC_CELL:Int +│ callDepth: _CALLDEPTH_CELL:Int +│ statusCode: _STATUSCODE_CELL:StatusCode +┃ +┃ (branch) +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023 +┃ ┃ _WORDSTACK_CELL:WordStack ==K ( W0:Int : ( W1:Int : WS:WordStack ) ) +┃ ┃ #if _USEGAS_CELL:Bool #then Gverylow < _SCHEDULE_CELL:Schedule > <=Gas _GAS_CELL:Gas #else true #fi +┃ │ +┃ └─ 3 (leaf, pending) +┃ k: #next [ ADD ] ~> _K_CELL:K +┃ pc: _PC_CELL:Int +┃ callDepth: _CALLDEPTH_CELL:Int +┃ statusCode: _STATUSCODE_CELL:StatusCode +┃ +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) _K_CELL:K +┃ │ pc: _PC_CELL:Int +┃ │ callDepth: _CALLDEPTH_CELL:Int +┃ │ statusCode: _STATUSCODE_CELL:StatusCode +┃ │ +┃ │ (2 steps) +┃ └─ 8 (leaf, terminal) +┃ k: #halt ~> _K_CELL:K +┃ pc: _PC_CELL:Int +┃ callDepth: _CALLDEPTH_CELL:Int +┃ statusCode: EVMC_STACK_UNDERFLOW +┃ +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ ( #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) +Int -1 ) >Int 1024 +┃ │ +┃ ├─ 5 +┃ │ k: #next [ ADD ] ~> _K_CELL:K +┃ │ pc: _PC_CELL:Int +┃ │ callDepth: _CALLDEPTH_CELL:Int +┃ │ statusCode: _STATUSCODE_CELL:StatusCode +┃ │ +┃ │ (2 steps) +┃ └─ 9 (leaf, terminal) +┃ k: #halt ~> _K_CELL:K +┃ pc: _PC_CELL:Int +┃ callDepth: _CALLDEPTH_CELL:Int +┃ statusCode: EVMC_STACK_OVERFLOW +┃ +┗━━┓ subst: .Subst + ┃ constraint: + ┃ ( notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024 ) + │ + ├─ 6 + │ k: #next [ ADD ] ~> _K_CELL:K + │ pc: _PC_CELL:Int + │ callDepth: _CALLDEPTH_CELL:Int + │ statusCode: _STATUSCODE_CELL:StatusCode + │ + │ (2 steps) + ├─ 7 + │ k: #exec [ ADD ] ~> #pc [ ADD ] ~> _K_CELL:K + │ pc: _PC_CELL:Int + │ callDepth: _CALLDEPTH_CELL:Int + │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┃ (1 step) + ┣━━┓ + ┃ │ + ┃ ├─ 10 (split) + ┃ │ k: #gas [ ADD , ADD W0:Int W1:Int ] ~> ADD W0:Int W1:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ │ pc: _PC_CELL:Int + ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┃ (branch) + ┃ ┣━━┓ subst: .Subst + ┃ ┃ ┃ constraint: + ┃ ┃ ┃ _USEGAS_CELL:Bool + ┃ ┃ │ + ┃ ┃ ├─ 12 + ┃ ┃ │ k: #gas [ ADD , ADD W0:Int W1:Int ] ~> ADD W0:Int W1:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ │ + ┃ ┃ │ (4 steps) + ┃ ┃ ├─ 20 + ┃ ┃ │ k: Gverylow < _SCHEDULE_CELL:Schedule > ~> #deductGas ~> #access [ ADD , ADD W0:Int ... + ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ + ┃ ┃ ┃ (1 step) + ┃ ┃ ┣━━┓ + ┃ ┃ ┃ │ + ┃ ┃ ┃ └─ 21 (leaf, pending) + ┃ ┃ ┃ k: #access [ ADD , ADD W0:Int W1:Int ] ~> ADD W0:Int W1:Int ~> #pc [ ADD ] ~> _K_CE ... + ┃ ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ + ┃ ┃ ┣━━┓ + ┃ ┃ ┃ │ + ┃ ┃ ┃ ├─ 22 + ┃ ┃ ┃ │ k: #end EVMC_OUT_OF_GAS ~> #access [ ADD , ADD W0:Int W1:Int ] ~> ADD W0:Int W1:Int ... + ┃ ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ │ + ┃ ┃ ┃ │ (4 steps) + ┃ ┃ ┃ └─ 29 (leaf, terminal) + ┃ ┃ ┃ k: #halt ~> _K_CELL:K + ┃ ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ ┃ statusCode: EVMC_OUT_OF_GAS + ┃ ┃ ┃ + ┃ ┃ ┗━━┓ + ┃ ┃ │ + ┃ ┃ └─ 23 (stuck, leaf) + ┃ ┃ k: Gverylow < _SCHEDULE_CELL:Schedule > ~> #deductGas ~> #access [ ADD , ADD W0:Int ... + ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┗━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ ( notBool _USEGAS_CELL:Bool ) + ┃ │ + ┃ └─ 13 (leaf, pending) + ┃ k: #gas [ ADD , ADD W0:Int W1:Int ] ~> ADD W0:Int W1:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ pc: _PC_CELL:Int + ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┗━━┓ + │ + ├─ 11 + │ k: #exec [ ADD ] ~> #pc [ ADD ] ~> _K_CELL:K + │ pc: _PC_CELL:Int + │ callDepth: _CALLDEPTH_CELL:Int + │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┃ (1 step) + ┣━━┓ + ┃ │ + ┃ ├─ 14 (split) + ┃ │ k: #gas [ ADD , ADD W0:Int W2:Int ] ~> ADD W0:Int W2:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ │ pc: _PC_CELL:Int + ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┃ (branch) + ┃ ┣━━┓ subst: .Subst + ┃ ┃ ┃ constraint: + ┃ ┃ ┃ _USEGAS_CELL:Bool + ┃ ┃ │ + ┃ ┃ ├─ 16 + ┃ ┃ │ k: #gas [ ADD , ADD W0:Int W2:Int ] ~> ADD W0:Int W2:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ │ + ┃ ┃ │ (4 steps) + ┃ ┃ ├─ 28 + ┃ ┃ │ k: Gverylow < _SCHEDULE_CELL:Schedule > ~> #deductGas ~> #access [ ADD , ADD W0:Int ... + ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ + ┃ ┃ ┃ (1 step) + ┃ ┃ ┣━━┓ + ┃ ┃ ┃ │ + ┃ ┃ ┃ └─ 33 (leaf, pending) + ┃ ┃ ┃ k: #access [ ADD , ADD W0:Int W2:Int ] ~> ADD W0:Int W2:Int ~> #pc [ ADD ] ~> _K_CE ... + ┃ ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ + ┃ ┃ ┣━━┓ + ┃ ┃ ┃ │ + ┃ ┃ ┃ └─ 34 (leaf, pending) + ┃ ┃ ┃ k: #end EVMC_OUT_OF_GAS ~> #access [ ADD , ADD W0:Int W2:Int ] ~> ADD W0:Int W2:Int ... + ┃ ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ ┃ + ┃ ┃ ┗━━┓ + ┃ ┃ │ + ┃ ┃ └─ 35 (leaf, pending) + ┃ ┃ k: Gverylow < _SCHEDULE_CELL:Schedule > ~> #deductGas ~> #access [ ADD , ADD W0:Int ... + ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┗━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ ( notBool _USEGAS_CELL:Bool ) + ┃ │ + ┃ └─ 17 (leaf, pending) + ┃ k: #gas [ ADD , ADD W0:Int W2:Int ] ~> ADD W0:Int W2:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ pc: _PC_CELL:Int + ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┗━━┓ + │ + ├─ 15 + │ k: #exec [ ADD ] ~> #pc [ ADD ] ~> _K_CELL:K + │ pc: _PC_CELL:Int + │ callDepth: _CALLDEPTH_CELL:Int + │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┃ (1 step) + ┣━━┓ + ┃ │ + ┃ ├─ 18 (split) + ┃ │ k: #gas [ ADD , ADD W0:Int W3:Int ] ~> ADD W0:Int W3:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ │ pc: _PC_CELL:Int + ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┃ (branch) + ┃ ┣━━┓ subst: .Subst + ┃ ┃ ┃ constraint: + ┃ ┃ ┃ _USEGAS_CELL:Bool + ┃ ┃ │ + ┃ ┃ ├─ 24 + ┃ ┃ │ k: #gas [ ADD , ADD W0:Int W3:Int ] ~> ADD W0:Int W3:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ ┃ │ pc: _PC_CELL:Int + ┃ ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ │ + ┃ ┃ │ (4 steps) + ┃ ┃ └─ 32 (leaf, pending) + ┃ ┃ k: Gverylow < _SCHEDULE_CELL:Schedule > ~> #deductGas ~> #access [ ADD , ADD W0:Int ... + ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┗━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ ( notBool _USEGAS_CELL:Bool ) + ┃ │ + ┃ └─ 25 (leaf, pending) + ┃ k: #gas [ ADD , ADD W0:Int W3:Int ] ~> ADD W0:Int W3:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ pc: _PC_CELL:Int + ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┗━━┓ + │ + ├─ 19 + │ k: #exec [ ADD ] ~> #pc [ ADD ] ~> _K_CELL:K + │ pc: _PC_CELL:Int + │ callDepth: _CALLDEPTH_CELL:Int + │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┃ (1 step) + ┣━━┓ + ┃ │ + ┃ ├─ 26 (split) + ┃ │ k: #gas [ ADD , ADD W0:Int W4:Int ] ~> ADD W0:Int W4:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ │ pc: _PC_CELL:Int + ┃ │ callDepth: _CALLDEPTH_CELL:Int + ┃ │ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┃ (branch) + ┃ ┣━━┓ subst: .Subst + ┃ ┃ ┃ constraint: + ┃ ┃ ┃ _USEGAS_CELL:Bool + ┃ ┃ │ + ┃ ┃ └─ 30 (leaf, pending) + ┃ ┃ k: #gas [ ADD , ADD W0:Int W4:Int ] ~> ADD W0:Int W4:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ ┃ pc: _PC_CELL:Int + ┃ ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ ┃ + ┃ ┗━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ ( notBool _USEGAS_CELL:Bool ) + ┃ │ + ┃ └─ 31 (leaf, pending) + ┃ k: #gas [ ADD , ADD W0:Int W4:Int ] ~> ADD W0:Int W4:Int ~> #pc [ ADD ] ~> _K_CELL: ... + ┃ pc: _PC_CELL:Int + ┃ callDepth: _CALLDEPTH_CELL:Int + ┃ statusCode: _STATUSCODE_CELL:StatusCode + ┃ + ┗━━┓ + │ + └─ 27 (leaf, pending) + k: #exec [ ADD ] ~> #pc [ ADD ] ~> _K_CELL:K + pc: _PC_CELL:Int + callDepth: _CALLDEPTH_CELL:Int + statusCode: _STATUSCODE_CELL:StatusCode + + +┌─ 2 (root, leaf, target) +│ k: _K_CELL:K +│ pc: ?_FINAL_PC_CELL:Int +│ callDepth: ?_FINAL_CALLDEPTH_CELL:Int +│ statusCode: ?_FINAL_STATUSCODE_CELL:StatusCode + + + +module SUMMARY-ADD-SPEC + + + rule [BASIC-BLOCK-6-TO-7]: + + ( #next [ ADD ] ~> .K => #exec [ ADD ] + ~> #pc [ ADD ] ) + ~> __K_CELL + + + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + requires ( ( notBool #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) Int 1024 ) + )) + [priority(20), label(BASIC-BLOCK-6-TO-7)] + + rule [BASIC-BLOCK-4-TO-8]: + + ( #next [ ADD ] => #halt ) + ~> __K_CELL + + + + + ( __STATUSCODE_CELL => EVMC_STACK_UNDERFLOW ) + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + requires #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) + + ( #next [ ADD ] => #halt ) + ~> __K_CELL + + + + + ( __STATUSCODE_CELL => EVMC_STACK_OVERFLOW ) + + + + _WORDSTACK_CELL:WordStack + + ... + + ... + + ... + + ... + + requires ( #sizeWordStack ( _WORDSTACK_CELL:WordStack , 0 ) +Int -1 ) >Int 1024 + [priority(20), label(BASIC-BLOCK-5-TO-9)] + + rule [BASIC-BLOCK-12-TO-20]: + + ( #gas [ ADD , ADD W0:Int W1:Int ] ~> .K => Gverylow < _SCHEDULE_CELL:Schedule > + ~> #deductGas + ~> #access [ ADD , ADD W0:Int W1:Int ] ) + ~> ADD W0:Int W1:Int + ~> #pc [ ADD ] + ~> __K_CELL + + + _SCHEDULE_CELL:Schedule + + + ( _USEGAS_CELL:Bool => true ) + + + + + + WS:WordStack + + ... + + ... + + ... + + ... + + requires ( _USEGAS_CELL:Bool + andBool ( ( notBool #sizeWordStack ( WS:WordStack , 2 ) Int 1024 ) + )))) + [priority(20), label(BASIC-BLOCK-12-TO-20)] + + rule [BASIC-BLOCK-16-TO-28]: + + ( #gas [ ADD , ADD W0:Int W2:Int ] ~> .K => Gverylow < _SCHEDULE_CELL:Schedule > + ~> #deductGas + ~> #access [ ADD , ADD W0:Int W2:Int ] ) + ~> ADD W0:Int W2:Int + ~> #pc [ ADD ] + ~> __K_CELL + + + _SCHEDULE_CELL:Schedule + + + ( _USEGAS_CELL:Bool => true ) + + + + + + WS0:WordStack + + ... + + ... + + ... + + ... + + requires ( _USEGAS_CELL:Bool + andBool ( ( notBool #sizeWordStack ( WS0:WordStack , 2 ) Int 1024 ) + andBool ( ( notBool ( _W1 ==Int W2:Int andBool _WS ==K WS0:WordStack ) ) + ))))) + [priority(20), label(BASIC-BLOCK-16-TO-28)] + + rule [BASIC-BLOCK-22-TO-29]: + + ( #end EVMC_OUT_OF_GAS + ~> #access [ ADD , ADD W0:Int W1:Int ] + ~> ADD W0:Int W1:Int + ~> #pc [ ADD ] => #halt ~> .K ) + ~> __K_CELL + + + _SCHEDULE_CELL:Schedule + + + true + + + + + ( __STATUSCODE_CELL => EVMC_OUT_OF_GAS ) + + + + WS:WordStack + + + _GAS_CELL:Gas + + ... + + ... + + ... + + ... + + requires ( __USEGAS_CELL + andBool ( ( notBool #sizeWordStack ( WS:WordStack , 2 ) + andBool ( ( notBool ( #sizeWordStack ( WS:WordStack , 2 ) +Int -1 ) >Int 1024 ) + ))))) + [priority(20), label(BASIC-BLOCK-22-TO-29)] + + rule [BASIC-BLOCK-24-TO-32]: + + ( #gas [ ADD , ADD W0:Int W3:Int ] ~> .K => Gverylow < _SCHEDULE_CELL:Schedule > + ~> #deductGas + ~> #access [ ADD , ADD W0:Int W3:Int ] ) + ~> ADD W0:Int W3:Int + ~> #pc [ ADD ] + ~> __K_CELL + + + _SCHEDULE_CELL:Schedule + + + ( _USEGAS_CELL:Bool => true ) + + + + + + WS1:WordStack + + ... + + ... + + ... + + ... + + requires ( _USEGAS_CELL:Bool + andBool ( ( notBool #sizeWordStack ( WS1:WordStack , 2 ) Int 1024 ) + andBool ( ( notBool ( _W1 ==Int W3:Int andBool _WS ==K WS1:WordStack ) ) + andBool ( ( notBool ( _W2 ==Int W3:Int andBool _WS0 ==K WS1:WordStack ) ) + )))))) + [priority(20), label(BASIC-BLOCK-24-TO-32)] + +endmodule