support natspec preconditions

.github/workflows/test-pr.yml

@@ -63,6 +63,7 @@ jobs:
       - name: 'Build Kontrol'
         run: |
             docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` natspec.llvm'
       - name: 'Run profiling'
         run: |
           PROF_ARGS='--numprocesses=8'
@@ -89,6 +90,7 @@ jobs:
       - name: 'Build Kontrol'
         run: |
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` natspec.llvm'
       - name: 'Run integration tests'
         run: |
           TEST_ARGS='-vv --force-sequential -k "not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end)" --numprocesses=3'
@@ -115,6 +117,7 @@ jobs:
       - name: 'Build Kontrol'
         run: |
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` natspec.llvm'
       - name: 'Run CSE and Minimize tests'
         run: |
           TEST_ARGS='--numprocesses=5 --force-sequential -vv -k "test_kontrol_cse or test_foundry_minimize_proof"'
@@ -141,6 +144,7 @@ jobs:
       - name: 'Build Kontrol'
         run: |
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` natspec.llvm'
       - name: 'Run end-to-end tests'
         run: |
           TEST_ARGS='--numprocesses=6 -vv --force-sequential -k "test_kontrol_end_to_end"'

pyproject.toml

@@ -19,12 +19,16 @@ dependencies = [
 name = "Runtime Verification, Inc."
 email = "[email protected]"
 
+[tool.hatch.build.targets.wheel]
+packages = ["src/kontrol", "src/natspec"]
+
 [project.scripts]
 kontrol = "kontrol.__main__:main"
 kontrol-kdist = "pyk.kdist.__main__:main"
 
 [project.entry-points.kdist]
 kontrol = "kontrol.kdist.plugin"
+natspec = "natspec.kdist.plugin"
 
 [dependency-groups]
 dev = [

src/kontrol/prove.py

@@ -15,7 +15,7 @@
 from kevm_pyk.utils import KDefinition__expand_macros, abstract_cell_vars, run_prover
 from multiprocess.pool import Pool  # type: ignore
 from pyk.cterm import CTerm, CTermSymbolic
-from pyk.kast.inner import KApply, KSequence, KSort, KVariable, Subst
+from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
 from pyk.kast.manip import flatten_label, free_vars, set_cell
 from pyk.kast.prelude.bytes import bytesToken
 from pyk.kast.prelude.collections import list_empty, map_empty, map_item, set_empty
@@ -34,6 +34,9 @@
 from pyk.utils import hash_str, run_process_2, unique
 from rich.progress import Progress, SpinnerColumn, TaskID, TextColumn, TimeElapsedColumn
 
+from natspec.natspec import Natspec
+from natspec.utils import GLOBAL_VARIABLES_TO_CELL_NAMES, HEX_LITERAL, ID, NATSPEC_TO_K_OPERATORS
+
 from .foundry import Foundry, KontrolSemantics, foundry_to_xml
 from .options import ConfigType
 from .solc_to_k import Contract, decode_kinner_output
@@ -1065,6 +1068,13 @@ def _init_cterm(
     for constraint in storage_constraints:
         init_cterm = init_cterm.add_constraint(constraint)
 
+    if type(method) is Contract.Method:
+        natspec_preconditions = _create_precondition_constraints(method, init_cterm)
+
+        for precondition in natspec_preconditions:
+            _LOGGER.info(f'Adding NatSpec precondition: {foundry.kevm.pretty_print(mlEqualsTrue(precondition))}')
+            init_cterm = init_cterm.add_constraint(mlEqualsTrue(precondition))
+
     non_cheatcode_contract_ids = []
     if not (config_type == ConfigType.TEST_CONFIG or active_simbolik):
         non_cheatcode_contract_ids = [Foundry.symbolic_contract_id(contract_name), 'CALLER_ID', 'ORIGIN_ID']
@@ -1486,3 +1496,59 @@ def _interpret_proof_failure(
         log = failure_log.print_with_additional_info(status_codes, output_values) + Foundry.help_info()
         for line in log:
             print(replace_k_words(line))
+
+
+def _create_precondition_constraints(method: Contract.Method, init_cterm: CTerm) -> list[KApply]:
+    precondition_constraints: list[KApply] = []
+
+    if method.preconditions is not None:
+        natspec = Natspec(kdist.get('natspec.llvm'))
+        for p in method.preconditions:
+            kinner = natspec.decode(input=p.precondition)
+            if type(kinner) is KApply:
+                kontrol_precondition = _kontrol_kast_from_natspec(kinner, method, init_cterm)
+                precondition_constraints.append(kontrol_precondition)
+
+    return precondition_constraints
+
+
+def _kontrol_kast_from_natspec(term: KApply, method: Contract.Method, init_cterm: CTerm) -> KApply:
+    """Convert a KApply representing a Precondition defined using the Natspec-Grammar a Kontrol KApply.
+
+    Replace symbol sorts and Id elements with KVariables.
+    """
+    symbol = NATSPEC_TO_K_OPERATORS[term.label]
+    args: list[KInner] = []
+    for arg in term.args:
+        if type(arg) is KApply:
+            # Check for predefined `block` or `msg` value.
+            global_variable = get_global_variable(arg, init_cterm)
+            if global_variable:
+                args.append(global_variable)
+            else:
+                args.append(_kontrol_kast_from_natspec(arg, method, init_cterm))
+        if type(arg) is KToken:
+            if arg.sort == ID:
+                # If it's an ID token, ensure it's either a function parameter or a storage variable
+                function_arg = method.find_arg(arg.token)
+                if function_arg:
+                    args.append(KVariable(function_arg))
+                    continue
+                # TODO: For storage address:
+                #  - identify storage slot
+                #  - identify contract address
+                _LOGGER.warning(f'NatSpec precondition: Unknown Id sort element: {arg.token}')
+            elif arg.sort == HEX_LITERAL:
+                args.append(token(int(arg.token, 16)))
+            elif arg.sort in [KSort('Int'), KSort('Bool')]:
+                args.append(arg)
+            _LOGGER.warning(f'NatSpec precondition: unknown token: {arg.token}')
+    return KApply(symbol, args)
+
+
+def get_global_variable(term: KApply, init_cterm: CTerm) -> KInner | None:
+    """Checks if a KAst term is a Solidity global variable and return the cell value from init_cterm if so."""
+    cell_name = GLOBAL_VARIABLES_TO_CELL_NAMES.get(term)
+    if cell_name is None:
+        return None
+    return init_cterm.cell(cell_name)

src/kontrol/solc_to_k.py

@@ -342,6 +342,32 @@ def parse_devdoc(tag: str, devdoc: dict | None) -> dict:
     return natspecs
 
 
+def parse_annotations(
+    devdoc: str | None, method: Contract.Method | Contract.Constructor
+) -> tuple[Precondition, ...] | None:
+    """
+    Parse developer documentation (devdoc) to extract user-provided preconditions.
+
+    Returns a tuple of Precondition objects, each representing a single precondition and a method to which it belongs.
+    """
+
+    if devdoc is None:
+        return None
+
+    preconditions: list[Precondition] = []
+    for precondition in devdoc.split(','):
+        # Trim whitespace and skip if empty
+        precondition = precondition.strip()
+        if not precondition:
+            continue
+
+        # Create a Precondition object and add it to the list
+        new_precondition = Precondition(precondition, method)
+        preconditions.append(new_precondition)
+
+    return tuple(preconditions)
+
+
 class StorageField(NamedTuple):
     label: str
     data_type: str
@@ -350,6 +376,19 @@ class StorageField(NamedTuple):
     linked_interface: str | None
 
 
+@dataclass
+class Precondition:
+    precondition: str
+    method: Contract.Method | Contract.Constructor
+
+    def __init__(self, precondition: str, method: Contract.Method | Contract.Constructor):
+        """
+        Initializes a new instance of the Precondition class.
+        """
+        self.precondition = precondition
+        self.method = method
+
+
 @dataclass
 class Contract:
     @dataclass
@@ -361,6 +400,7 @@ class Constructor:
         contract_storage_digest: str
         payable: bool
         signature: str
+        preconditions: tuple[Precondition, ...] | None
 
         def __init__(
             self,
@@ -476,6 +516,7 @@ class Method:
         ast: dict | None
         natspec_values: dict | None
         function_calls: tuple[str, ...] | None
+        preconditions: tuple[Precondition, ...] | None
 
         def __init__(
             self,
@@ -506,6 +547,9 @@ def __init__(
             natspec_tags = ['custom:kontrol-array-length-equals', 'custom:kontrol-bytes-length-equals']
             self.natspec_values = {tag.split(':')[1]: parse_devdoc(tag, devdoc) for tag in natspec_tags}
             self.inputs = tuple(inputs_from_abi(abi['inputs'], self.natspec_values))
+            self.preconditions = (
+                parse_annotations(devdoc.get('custom:kontrol-precondition', None), self) if devdoc is not None else None
+            )
             self.function_calls = tuple(function_calls) if function_calls is not None else None
 
         @property
@@ -571,6 +615,13 @@ def arg_types(self) -> tuple[str, ...]:
                     arg_types.extend([sub_input.type for sub_input in input.flattened()])
             return tuple(arg_types)
 
+        def find_arg(self, name: str) -> str | None:
+            try:
+                idx = single([i.idx for i in self.inputs if i.name == name])
+                return self.arg_names[idx]
+            except ValueError:
+                return None
+
         def up_to_date(self, digest_file: Path) -> bool:
             digest_dict = _read_digest_file(digest_file)
             return digest_dict.get('methods', {}).get(self.qualified_name, {}).get('method', '') == self.digest

src/natspec/kdist/natspec-grammar.md

@@ -0,0 +1,60 @@
+Solidity Natspec Grammar
+------------------------
+
+
+ TODO:
+ ----
+ 1. add support for bitwise operators
+
+```k
+module NATSPEC-SYNTAX
+    imports INT-SYNTAX
+    imports BOOL-SYNTAX
+    imports ID-SYNTAX
+
+    // Literals
+    syntax HexLiteral ::= r"0x[0-9a-fA-F]+" [token, symbol(SolidityHexLiteral)]
+ // ---------------------------------------------------------------------------
+
+    syntax Access ::= Id
+                    | Access "[" Exp "]" [symbol(SolidityIndexAccess)]
+                    | Access "." Id      [symbol(SolidityFieldAccess)]
+ // ------------------------------------------------------------------
+
+    syntax Exp ::= Int | Bool | HexLiteral | Access
+                 | "(" Exp ")"                   [bracket]
+                 // Unary operators (high precedence)
+                 > "!" Exp                       [symbol(SolidityNegation)]
+                 // Power (right associative)
+                 > right:
+                   Exp "**" Exp                  [symbol(SolidityPower)]
+                 // Multiplicative
+                 > left:
+                   Exp "*" Exp                   [symbol(SolidityMultiplication)]
+                 | Exp "/" Exp                   [symbol(SolidityDivision)]
+                 | Exp "%" Exp                   [symbol(SolidityModulo)]
+                 // Additive
+                 > left:
+                   Exp "+" Exp                   [symbol(SolidityAddition)]
+                 | Exp "-" Exp                   [symbol(SoliditySubtraction)]
+                 // Relational
+                 > non-assoc:
+                   Exp "<" Exp                   [symbol(SolidityLT)]
+                 | Exp ">" Exp                   [symbol(SolidityGT)]
+                 | Exp "<=" Exp                  [symbol(SolidityLE)]
+                 | Exp ">=" Exp                  [symbol(SolidityGE)]
+                 // Equality
+                 > non-assoc:
+                   Exp "==" Exp                  [symbol(SolidityEq)]
+                 | Exp "!=" Exp                  [symbol(SolidityNeq)]
+                 // Logical AND
+                 > left:
+                   Exp "&&" Exp                  [symbol(SolidityConjunction)]
+                 // Logical OR
+                 > left:
+                   Exp "||" Exp                  [symbol(SolidityDisjunction)]
+endmodule
+
+module NATSPEC
+endmodule
+```

src/natspec/kdist/plugin.py

@@ -0,0 +1,59 @@
+from __future__ import annotations
+
+import shutil
+from typing import TYPE_CHECKING
+
+from pyk.kbuild.utils import k_version
+from pyk.kdist.api import Target
+from pyk.ktool.kompile import PykBackend, kompile
+
+if TYPE_CHECKING:
+    from collections.abc import Callable, Mapping
+    from typing import Any, Final
+    from pathlib import Path
+
+from .utils import KSRC_DIR
+
+
+class SourceTarget(Target):
+
+    def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
+        shutil.copy(KSRC_DIR / 'natspec-grammar.md', output_dir / 'natspec-grammar.md')
+
+    def source(self) -> tuple[Path, ...]:
+        return (KSRC_DIR,)
+
+
+class KompileTarget(Target):
+    _kompile_args: Callable[[Path], Mapping[str, Any]]
+
+    def __init__(self, kompile_args: Callable[[Path], Mapping[str, Any]]):
+        self._kompile_args = kompile_args
+
+    def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
+        kompile_args = self._kompile_args(deps['natspec.source'])
+        kompile(output_dir=output_dir, verbose=verbose, **kompile_args)
+
+    def context(self) -> dict[str, str]:
+        return {'k-version': k_version().text}
+
+    def deps(self) -> tuple[str]:
+        return ('natspec.source',)
+
+
+__TARGETS__: Final = {
+    'source': SourceTarget(),
+    'llvm': KompileTarget(
+        lambda src_dir: {
+            'backend': PykBackend.LLVM,
+            'main_file': src_dir / 'natspec-grammar.md',
+            'main_module': 'NATSPEC',
+            'syntax_module': 'NATSPEC-SYNTAX',
+            'md_selector': 'k',
+            'warnings_to_errors': True,
+            'gen_glr_bison_parser': True,
+            'opt_level': 3,
+            'ccopts': ['-g'],
+        },
+    ),
+}

src/natspec/kdist/utils.py

@@ -0,0 +1,10 @@
+from __future__ import annotations
+
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from typing import Final
+
+
+KSRC_DIR: Final = Path(__file__).parent.resolve(strict=True)