Several fixes to KEVM prover

include/kframework/evm.md

@@ -1044,11 +1044,8 @@ The `JUMP*` family of operations affect the current program counter.
 
     syntax BinStackOp ::= "JUMPI"
  // -----------------------------
-    rule <k> JUMPI _DEST I => . ... </k>
-      requires I ==Int 0
-
-    rule <k> JUMPI  DEST I => JUMP DEST ... </k>
-      requires I =/=Int 0
+    rule [jumpi.false]: <k> JUMPI _DEST I => .         ... </k> requires I  ==Int 0
+    rule [jumpi.true]:  <k> JUMPI  DEST I => JUMP DEST ... </k> requires I =/=Int 0
 
     syntax InternalOp ::= "#endBasicBlock"
  // --------------------------------------

include/kframework/lemmas/lemmas.k

@@ -216,6 +216,7 @@ module LEMMAS-HASKELL [symbolic, kore]
     rule (X &Int Y) <Int Z      => true requires 0 <=Int X andBool 0 <=Int Y andBool (X <Int Z orBool Y <Int Z)          [simplification]
     rule (X |Int Y) <Int pow256 => true requires 0 <=Int X andBool 0 <=Int Y andBool X <Int pow256 andBool Y <Int pow256 [simplification]
 
+    rule notMaxUInt160 &Int X => 0 requires #rangeUInt(160, X) [simplification]
     rule maxUInt160 &Int (X |Int (notMaxUInt160 &Int Y:Int)) => X requires #rangeUInt(160, X) andBool 0 <=Int Y [simplification]
 
   // ########################

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.29"
+version = "1.0.30"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__main__.py

@@ -182,11 +182,12 @@ def exec_prove(
     md_selector: Optional[str] = None,
     claim_labels: Iterable[str] = (),
     exclude_claim_labels: Iterable[str] = (),
-    max_depth: int = 100,
+    max_depth: int = 1000,
     max_iterations: Optional[int] = None,
     workers: int = 1,
     simplify_init: bool = True,
     break_every_step: bool = False,
+    break_on_jumpi: bool = False,
     break_on_calls: bool = True,
     implication_every_block: bool = True,
     rpc_base_port: Optional[int] = None,
@@ -219,6 +220,7 @@ def exec_prove(
         max_iterations=max_iterations,
         workers=workers,
         break_every_step=break_every_step,
+        break_on_jumpi=break_on_jumpi,
         break_on_calls=break_on_calls,
         implication_every_block=implication_every_block,
         rpc_base_port=rpc_base_port,
@@ -268,14 +270,15 @@ def exec_view_kcfg(
 
 def exec_foundry_prove(
     foundry_out: Path,
-    max_depth: int = 100,
+    max_depth: int = 1000,
     max_iterations: Optional[int] = None,
     reinit: bool = False,
     tests: Iterable[str] = (),
     exclude_tests: Iterable[str] = (),
     workers: int = 1,
     simplify_init: bool = True,
     break_every_step: bool = False,
+    break_on_jumpi: bool = False,
     break_on_calls: bool = True,
     implication_every_block: bool = True,
     rpc_base_port: Optional[int] = None,
@@ -296,6 +299,7 @@ def exec_foundry_prove(
         workers=workers,
         simplify_init=simplify_init,
         break_every_step=break_every_step,
+        break_on_jumpi=break_on_jumpi,
         break_on_calls=break_on_calls,
         implication_every_block=implication_every_block,
         rpc_base_port=rpc_base_port,
@@ -481,6 +485,13 @@ def parse(s: str) -> List[T]:
         action='store_true',
         help='Store a node for every EVM opcode step (expensive).',
     )
+    explore_args.add_argument(
+        '--break-on-jumpi',
+        dest='break_on_jumpi',
+        default=False,
+        action='store_true',
+        help='Store a node for every EVM jump opcode.',
+    )
     explore_args.add_argument(
         '--break-on-calls',
         dest='break_on_calls',

kevm-pyk/src/kevm_pyk/foundry.py

@@ -186,14 +186,15 @@ def foundry_kompile(
 
 def foundry_prove(
     foundry_out: Path,
-    max_depth: int = 100,
+    max_depth: int = 1000,
     max_iterations: Optional[int] = None,
     reinit: bool = False,
     tests: Iterable[str] = (),
     exclude_tests: Iterable[str] = (),
     workers: int = 1,
     simplify_init: bool = True,
     break_every_step: bool = False,
+    break_on_jumpi: bool = False,
     break_on_calls: bool = True,
     implication_every_block: bool = True,
     rpc_base_port: Optional[int] = None,
@@ -255,15 +256,13 @@ def foundry_prove(
             method = [m for m in contract.methods if m.name == method_name][0]
             empty_config = foundry.definition.empty_config(GENERATED_TOP_CELL)
             kcfg = _method_to_cfg(empty_config, contract, method)
-            init_term = kcfg.get_unique_init().cterm.kast
-            target_term = kcfg.get_unique_target().cterm.kast
             _LOGGER.info(f'Expanding macros in initial state for test: {test}')
-            init_term = KDefinition__expand_macros(foundry.definition, init_term)
-            init_cterm = KEVM.add_invariant(CTerm(init_term))
-            _LOGGER.info(f'Expanding macros in target state for test: {test}')
-            target_term = KDefinition__expand_macros(foundry.definition, target_term)
-            target_cterm = KEVM.add_invariant(CTerm(target_term))
+            init_term = kcfg.get_unique_init().cterm.kast
+            init_cterm = CTerm(KDefinition__expand_macros(foundry.definition, init_term))
             kcfg.replace_node(kcfg.get_unique_init().id, init_cterm)
+            _LOGGER.info(f'Expanding macros in target state for test: {test}')
+            target_term = kcfg.get_unique_target().cterm.kast
+            target_cterm = CTerm(KDefinition__expand_macros(foundry.definition, target_term))
             kcfg.replace_node(kcfg.get_unique_target().id, target_cterm)
             if simplify_init:
                 with KCFGExplore(foundry, port=find_free_port(), bug_report=br) as kcfg_explore:
@@ -279,6 +278,7 @@ def foundry_prove(
         max_iterations=max_iterations,
         workers=workers,
         break_every_step=break_every_step,
+        break_on_jumpi=break_on_jumpi,
         break_on_calls=break_on_calls,
         implication_every_block=implication_every_block,
         rpc_base_port=rpc_base_port,

kevm-pyk/src/kevm_pyk/solc_to_k.py

@@ -69,7 +69,7 @@ def rule(self, contract: KInner, application_label: KLabel, contract_name: str)
                 args.append(KEVM.abi_type(input_type, KVariable(input_name)))
                 rp = _range_predicate(KVariable(input_name), input_type)
                 if rp is None:
-                    _LOGGER.warning(
+                    _LOGGER.info(
                         f'Unsupported ABI type for method {contract_name}.{prod_klabel.name}, will not generate calldata sugar: {input_type}'
                     )
                     return None
@@ -127,22 +127,22 @@ def _get_method_abi(_mname: str) -> Dict:
             _method_identifiers = contract_json['methodIdentifiers']
         else:
             _method_identifiers = []
-            _LOGGER.warning(f"Could not find member 'methodIdentifiers' while processing contract: {self.name}")
+            _LOGGER.info(f"Could not find member 'methodIdentifiers' while processing contract: {self.name}")
         for msig in _method_identifiers:
             mname = msig.split('(')[0]
             mid = int(_method_identifiers[msig], 16)
             _m = Contract.Method(mname, mid, _get_method_abi(mname), contract_name, self.sort_method)
             _methods.append(_m)
         self.methods = tuple(_methods)
         if 'storageLayout' not in contract_json or 'storage' not in contract_json['storageLayout']:
-            _LOGGER.warning(f"Could not find member 'storageLayout' while processing contract: {self.name}")
+            _LOGGER.info(f"Could not find member 'storageLayout' while processing contract: {self.name}")
             self.fields = FrozenDict({})
         else:
             _fields_list = [(_f['label'], int(_f['slot'])) for _f in contract_json['storageLayout']['storage']]
             _fields = {}
             for _l, _s in _fields_list:
                 if _l in _fields:
-                    _LOGGER.warning(f'Found duplicate field access key on contract {self.name}: {_l}')
+                    _LOGGER.info(f'Found duplicate field access key on contract {self.name}: {_l}')
                     continue
                 _fields[_l] = _s
             self.fields = FrozenDict(_fields)
@@ -343,7 +343,7 @@ def _evm_base_sort(type_label: str) -> KSort:
     if type_label == 'string':
         return KSort('String')
 
-    _LOGGER.warning(f'Using generic sort K for type: {type_label}')
+    _LOGGER.info(f'Using generic sort K for type: {type_label}')
     return KSort('K')
 
 
@@ -400,7 +400,7 @@ def _range_predicate(term: KInner, type_label: str) -> Optional[KInner]:
     if type_label == 'string':
         return TRUE
 
-    _LOGGER.warning(f'Unknown range predicate for type: {type_label}')
+    _LOGGER.info(f'Unknown range predicate for type: {type_label}')
     return None
 
 

kevm-pyk/src/kevm_pyk/utils.py

@@ -41,10 +41,11 @@ def parallel_kcfg_explore(
     kprove: KProve,
     proof_problems: Dict[str, KCFG],
     save_directory: Optional[Path] = None,
-    max_depth: int = 100,
+    max_depth: int = 1000,
     max_iterations: Optional[int] = None,
     workers: int = 1,
     break_every_step: bool = False,
+    break_on_jumpi: bool = False,
     break_on_calls: bool = True,
     implication_every_block: bool = False,
     rpc_base_port: Optional[int] = None,
@@ -57,6 +58,8 @@ def _call_rpc(packed_args: Tuple[str, KCFG, int]) -> bool:
         terminal_rules = ['EVM.halt']
         if break_every_step:
             terminal_rules.append('EVM.step')
+        if break_on_jumpi:
+            terminal_rules.extend(['EVM.jumpi.true', 'EVM.jumpi.false'])
         if break_on_calls:
             terminal_rules.extend(
                 [

package/version

@@ -1 +1 @@
-1.0.29
+1.0.30

tests/foundry/test/Simple.t.sol

@@ -47,4 +47,25 @@ contract AssertTest is Test {
             assert(false);
         }
     }
+
+    function sum_N(uint n) pure internal returns (uint) {
+        uint s = 0;
+        while (0 < n) {
+            s = s + n;
+            n = n - 1;
+        }
+        return s;
+    }
+
+    function test_sum_10() public returns (uint) {
+        return sum_N(10);
+    }
+
+    function test_sum_100() public returns (uint) {
+        return sum_N(100);
+    }
+
+    function test_sum_1000() public returns (uint) {
+        return sum_N(1000);
+    }
 }

tests/specs/benchmarks/verification.k

@@ -102,7 +102,7 @@ module VERIFICATION
     rule maxUInt256 &Int X => X requires #rangeUInt(256, X) [simplification]
 
     // 2^256 - 2^160 = 0xff..ff00..00 (96 1's followed by 160 0's)
-    rule 115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int ADDR => 0
+    rule notMaxUInt160 &Int ADDR => 0
       requires #rangeAddress(ADDR)
       [simplification]
 

tests/specs/functional/lemmas-spec.k

@@ -42,30 +42,34 @@ module LEMMAS-SPEC
        andBool #rangeUInt(256, Z) andBool Z ==Int #lookup(M, _KZ)
        andBool #rangeUInt(256, (X -Int Y) -Int Z)
 
-    claim [address-reprojection]: <k> runLemma(((maxUInt160 &Int ((368263281805664599098893944405654396525700029268 |Int (115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int)) modInt pow256)) modInt pow160))
+    claim [address-reprojection]: <k> runLemma(((maxUInt160 &Int ((368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)) modInt pow256)) modInt pow160))
                                    => doneLemma(368263281805664599098893944405654396525700029268) ... </k>
                                 requires #rangeUInt(256, X)
 
-    claim [address-reprojection-1]: <k> runLemma(0 <=Int (368263281805664599098893944405654396525700029268 |Int (115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int)))
+    claim [address-reprojection-1]: <k> runLemma(0 <=Int (368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)))
                                      => doneLemma(true) ... </k>
                                   requires #rangeUInt(256, X)
 
-    claim [address-reprojection-2]: <k> runLemma(0 <=Int (115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int))
+    claim [address-reprojection-2]: <k> runLemma(0 <=Int (notMaxUInt160 &Int X:Int))
                                      => doneLemma(true) ... </k>
                                   requires #rangeUInt(256, X)
 
-    claim [address-reprojection-4]: <k> runLemma((368263281805664599098893944405654396525700029268 |Int (115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int)) <Int pow256)
+    claim [address-reprojection-4]: <k> runLemma((368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)) <Int pow256)
                                      => doneLemma(true) ... </k>
                                   requires #rangeUInt(256, X)
 
-    claim [address-reprojection-5]: <k> runLemma((115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int) <Int pow256)
+    claim [address-reprojection-5]: <k> runLemma((notMaxUInt160 &Int X:Int) <Int pow256)
                                      => doneLemma(true) ... </k>
                                   requires #rangeUInt(256, X)
 
-    claim [address-reprojection-6]: <k> runLemma(maxUInt160 &Int (368263281805664599098893944405654396525700029268 |Int (115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int)))
+    claim [address-reprojection-6]: <k> runLemma(maxUInt160 &Int (368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)))
                                      => doneLemma(368263281805664599098893944405654396525700029268) ... </k>
                                   requires #rangeUInt(256, X)
 
+    claim [address-insertion-1]: <k> runLemma(368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int #lookup(ACCT_STORAGE:Map, 8)))
+                                  => doneLemma(368263281805664599098893944405654396525700029268) ... </k>
+                               requires #lookup(ACCT_STORAGE, 8) <Int pow160
+
  // Buffer write simplifications
  // ----------------------------
 

tests/specs/mcd/word-pack.k

@@ -117,16 +117,14 @@ module WORD-PACK-COMMON
     rule  UINT48_1             |Int (maskWordPackUInt48UInt48_2 &Int UINT48_UINT48) => #WordPackUInt48UInt48( UINT48_1 , (maskWordPackUInt48UInt48_2 &Int UINT48_UINT48) /Int pow48 ) requires #rangeUInt(96, UINT48_UINT48) andBool #rangeUInt(48, UINT48_1) [simplification]
     rule (UINT48_2 *Int pow48) |Int (maxUInt48                  &Int UINT48_UINT48) => #WordPackUInt48UInt48( maxUInt48 &Int UINT48_UINT48 , UINT48_2                               ) requires #rangeUInt(96, UINT48_UINT48) andBool #rangeUInt(48, UINT48_2) [simplification]
 
-    syntax Int ::= "maskWordPackAddrUInt48UInt48_1" [macro] // 0xFFFFFFFFFFFFFFFFFFFFFFFF0000000000000000000000000000000000000000
-                 | "maskWordPackAddrUInt48UInt48_2" [macro] // 0xFFFFFFFFFFFF000000000000FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
+    syntax Int ::= "maskWordPackAddrUInt48UInt48_2" [macro] // 0xFFFFFFFFFFFF000000000000FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
                  | "maskWordPackAddrUInt48UInt48_3" [macro] // 0x000000000000FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
  // -----------------------------------------------------------------------------------------------------------------------------
-    rule maskWordPackAddrUInt48UInt48_1 => 115792089237316195423570985007226406215939081747436879206741300988257197096960
     rule maskWordPackAddrUInt48UInt48_2 => 115792089237315784047431654708638870748305248246218003188207458632603225030655
     rule maskWordPackAddrUInt48UInt48_3 => 411376139330301510538742295639337626245683966408394965837152255
 
-    rule (ADDR |Int (maskWordPackAddrUInt48UInt48_1 &Int ADDR_UINT48_UINT48)) /Int pow160 => ADDR_UINT48_UINT48 /Int pow160 requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeAddress(ADDR) [simplification]
-    rule (ADDR |Int (maskWordPackAddrUInt48UInt48_1 &Int ADDR_UINT48_UINT48)) /Int pow208 => ADDR_UINT48_UINT48 /Int pow208 requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeAddress(ADDR) [simplification]
+    rule (ADDR |Int (notMaxUInt160 &Int ADDR_UINT48_UINT48)) /Int pow160 => ADDR_UINT48_UINT48 /Int pow160 requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeAddress(ADDR) [simplification]
+    rule (ADDR |Int (notMaxUInt160 &Int ADDR_UINT48_UINT48)) /Int pow208 => ADDR_UINT48_UINT48 /Int pow208 requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeAddress(ADDR) [simplification]
 
     rule (UINT48_2 *Int pow208) |Int (maskWordPackAddrUInt48UInt48_3 &Int ADDR_UINT48_UINT48) => #WordPackAddrUInt48UInt48(maxUInt160 &Int ADDR_UINT48_UINT48, maxUInt48 &Int (ADDR_UINT48_UINT48 /Int pow160), UINT48_2) requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeUInt(48, UINT48_2) [simplification]
     rule (UINT48_1 *Int pow160) |Int (maskWordPackAddrUInt48UInt48_2 &Int ADDR_UINT48_UINT48) => #WordPackAddrUInt48UInt48(maxUInt160 &Int ADDR_UINT48_UINT48, UINT48_1, maxUInt48 &Int (ADDR_UINT48_UINT48 /Int pow208)) requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeUInt(48, UINT48_1) [simplification]