provide KEVMSummarizer to sammarize rules for all the instruction rules

kevm-pyk/.gitignore

@@ -1,3 +1,5 @@
 /dist/
 __pycache__/
 .coverage
+proofs/
+summaries/

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
 
 

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.',

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,

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
+```

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

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) <Int #stackNeeded(OP)
-    rule #stackOverflow (WS, OP) => #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 <k> #ecadd(P1, P2) => #end EVMC_PRECOMPILE_FAILURE ... </k>
-      requires notBool isValidPoint(P1) orBool notBool isValidPoint(P2)
-    rule <k> #ecadd(P1, P2) => #end EVMC_SUCCESS ... </k> <output> _ => #point(BN128Add(P1, P2)) </output>
-      requires isValidPoint(P1) andBool isValidPoint(P2)
+      requires notBool isValidPointWrapper(P1) orBool notBool isValidPointWrapper(P2)
+    rule <k> #ecadd(P1, P2) => #end EVMC_SUCCESS ... </k> <output> _ => #point(BN128AddWrapper(P1, P2)) </output>
+      requires isValidPointWrapper(P1) andBool isValidPointWrapper(P2)
 
     syntax PrecompiledOp ::= "ECMUL"
  // --------------------------------
@@ -1930,9 +1932,9 @@ Precompiled Contracts
     syntax InternalOp ::= #ecmul(G1Point, Int) [symbol(#ecmul)]
  // -----------------------------------------------------------
     rule <k> #ecmul(P, _S) => #end EVMC_PRECOMPILE_FAILURE ... </k>
-      requires notBool isValidPoint(P)
-    rule <k> #ecmul(P,  S) => #end EVMC_SUCCESS ... </k> <output> _ => #point(BN128Mul(P, S)) </output>
-      requires isValidPoint(P)
+      requires notBool isValidPointWrapper(P)
+    rule <k> #ecmul(P,  S) => #end EVMC_SUCCESS ... </k> <output> _ => #point(BN128MulWrapper(P, S)) </output>
+      requires isValidPointWrapper(P)
 
     syntax Bytes ::= #point ( G1Point ) [symbol(#point), function]
  // --------------------------------------------------------------
@@ -1952,19 +1954,19 @@ Precompiled Contracts
     rule <k> (.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) ... </k>
       requires I =/=Int LEN
     rule <k> #ecpairing(A, B, LEN, _, LEN) => #end EVMC_SUCCESS ... </k>
-         <output> _ => #padToWidth(32, #asByteStack(bool2Word(BN128AtePairing(A, B)))) </output>
+         <output> _ => #padToWidth(32, #asByteStack(bool2Word(BN128AtePairingWrapper(A, B)))) </output>
 
     syntax InternalOp ::= "#checkPoint"
  // -----------------------------------
     rule <k> (#checkPoint => .K) ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) ... </k>
-      requires isValidPoint(AK) andBool isValidPoint(BK)
+      requires isValidPointWrapper(AK) andBool isValidPointWrapper(BK)
     rule <k> #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #end EVMC_PRECOMPILE_FAILURE ... </k>
-      requires notBool isValidPoint(AK) orBool notBool isValidPoint(BK)
+      requires notBool isValidPointWrapper(AK) orBool notBool isValidPointWrapper(BK)
 
     syntax PrecompiledOp ::= "BLAKE2F"
  // ----------------------------------
     rule <k> BLAKE2F => #end EVMC_SUCCESS ... </k>
-         <output> _ => #parseByteStack( Blake2Compress( DATA ) ) </output>
+         <output> _ => #parseByteStack( Blake2CompressWrapper( DATA ) ) </output>
          <callData> DATA </callData>
       requires lengthBytes( DATA ) ==Int 213
        andBool DATA[212] <=Int 1

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md

@@ -263,5 +263,8 @@ module GAS-SIMPLIFICATION [symbolic]
     imports BOOL
 
     rule A <Gas B => false requires B <=Gas A [simplification]
+    rule notBool (A <=Gas B) => B <Gas A [simplification]
+    rule notBool (A <Gas B) => B <=Gas A [simplification]
 endmodule
 ```
+

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 <Int A -Int B andBool 0 <=Int C [simplification]
 
+  // ###########################################################################
+  // log
+  // ###########################################################################
+
+    rule #Ceil ( log2Int ( X:Int ) ) => { true #Equals X >Int 0 } [simplification]
 endmodule

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]

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]
 ```