Add accounts invariants (#2249)

* strenghten invariant

* Set Version: 1.0.411

* apply review suggestions

* Set Version: 1.0.412

* Set Version: 1.0.412

---------

Co-authored-by: devops <[email protected]>

Author: anvacaru

kevm-pyk/pyproject.toml

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

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.411'
+VERSION: Final = '1.0.412'

kevm-pyk/src/kevm_pyk/kevm.py

@@ -12,7 +12,7 @@
 from pyk.ktool.kprove import KProve
 from pyk.ktool.krun import KRun
 from pyk.prelude.kint import intToken, ltInt
-from pyk.prelude.ml import mlEqualsTrue
+from pyk.prelude.ml import mlEqualsFalse, mlEqualsTrue
 from pyk.prelude.string import stringToken
 from pyk.proof.reachability import APRBMCProof, APRProof
 from pyk.proof.show import APRBMCProofNodePrinter, APRProofNodePrinter
@@ -242,16 +242,39 @@ def short_info(self, cterm: CTerm) -> list[str]:
 
     @staticmethod
     def add_invariant(cterm: CTerm) -> CTerm:
+        def _add_account_invariant(account: KApply) -> list[KApply]:
+            _account_constraints = []
+            acct_id, balance, nonce = account.args[0], account.args[1], account.args[5]
+
+            if type(acct_id) is KApply and type(acct_id.args[0]) is KVariable:
+                _account_constraints.append(mlEqualsTrue(KEVM.range_address(acct_id.args[0])))
+                _account_constraints.append(
+                    mlEqualsFalse(KEVM.is_precompiled_account(acct_id.args[0], cterm.cell('SCHEDULE_CELL')))
+                )
+            if type(balance) is KApply and type(balance.args[0]) is KVariable:
+                _account_constraints.append(mlEqualsTrue(KEVM.range_uint(256, balance.args[0])))
+            if type(nonce) is KApply and type(nonce.args[0]) is KVariable:
+                _account_constraints.append(mlEqualsTrue(KEVM.range_nonce(nonce.args[0])))
+            return _account_constraints
+
         constraints = []
         word_stack = cterm.cell('WORDSTACK_CELL')
         if type(word_stack) is not KVariable:
             word_stack_items = flatten_label('_:__EVM-TYPES_WordStack_Int_WordStack', word_stack)
             for i in word_stack_items[:-1]:
                 constraints.append(mlEqualsTrue(KEVM.range_uint(256, i)))
 
-        gas_cell = cterm.cell('GAS_CELL')
-        if not (type(gas_cell) is KApply and gas_cell.label.name == 'infGas'):
-            constraints.append(mlEqualsTrue(KEVM.range_uint(256, gas_cell)))
+        accounts_cell = cterm.cell('ACCOUNTS_CELL')
+        if type(accounts_cell) is not KApply('.AccountCellMap'):
+            accounts = flatten_label('_AccountCellMap_', cterm.cell('ACCOUNTS_CELL'))
+            for wrapped_account in accounts:
+                if not (type(wrapped_account) is KApply and wrapped_account.label.name == 'AccountCellMapItem'):
+                    continue
+
+                account = wrapped_account.args[1]
+                if type(account) is KApply:
+                    constraints.extend(_add_account_invariant(account))
+
         constraints.append(mlEqualsTrue(KEVM.range_address(cterm.cell('ID_CELL'))))
         constraints.append(mlEqualsTrue(KEVM.range_address(cterm.cell('CALLER_CELL'))))
         constraints.append(mlEqualsTrue(KEVM.range_address(cterm.cell('ORIGIN_CELL'))))
@@ -315,6 +338,10 @@ def range_bool(i: KInner) -> KApply:
     def range_bytes(width: KInner, ba: KInner) -> KApply:
         return KApply('#rangeBytes(_,_)_WORD_Bool_Int_Int', [width, ba])
 
+    @staticmethod
+    def range_nonce(i: KInner) -> KApply:
+        return KApply('#rangeNonce(_)_WORD_Bool_Int', [i])
+
     @staticmethod
     def range_blocknum(ba: KInner) -> KApply:
         return KApply('#rangeBlockNum(_)_WORD_Bool_Int', [ba])
@@ -343,6 +370,10 @@ def bin_runtime(c: KInner) -> KApply:
     def init_bytecode(c: KInner) -> KApply:
         return KApply('initBytecode', [c])
 
+    @staticmethod
+    def is_precompiled_account(i: KInner, s: KInner) -> KApply:
+        return KApply('#isPrecompiledAccount(_,_)_EVM_Bool_Int_Schedule', [i, s])
+
     @staticmethod
     def hashed_location(compiler: str, base: KInner, offset: KInner, member_offset: int = 0) -> KApply:
         location = KApply(

package/version

@@ -1 +1 @@
-1.0.411
+1.0.412