Add deal framework for formal verification with release no-ops

AGENTS.md

@@ -583,6 +583,7 @@ To maintain a predictable and reliable codebase, follow these rules when handlin
 - **Version Bump**: Updated extension version to `0.6.0-beta`.
 
 ### Code Quality Improvements
+- **Formal Verification Setup**: Added the `deal` library and `crosshair-tool` to `pyproject.toml` dev dependencies. Introduced `plugin/framework/deal_compat.py` to provide safe, zero-overhead no-op decorators in release builds (detected via the absence of the `plugin/tests/` folder), allowing contract checking to be used exclusively during development/debug.
 - **Safe JSON Parsing**: Introduced `safe_json_loads()` utility in `plugin/framework/errors.py` to replace scattered `json.loads` fallbacks with try/except blocks.
 - **Document Cache Removal**: Commented out `DocumentCache` usage and removed cache invalidation calls to simplify document handling logic.
 - **Logging Enhancements**: Improved logging consistency across modules, ensuring all caught exceptions are properly logged with context.

plugin/contrib/deal/__init__.py

@@ -0,0 +1,76 @@
+"""
+**Deal** is a Python library for [design by contract][wiki] (DbC) programming.
+See [documentation] for more details.
+
+[wiki]: https://en.wikipedia.org/wiki/Design_by_contract
+[documentation]: https://deal.readthedocs.io/index.html
+"""
+from . import introspection
+from ._exceptions import (
+    ContractError, ExampleContractError, InvContractError, MarkerError,
+    NoMatchError, OfflineContractError, PostContractError, PreContractError,
+    RaisesContractError, ReasonContractError, SilentContractError,
+)
+from ._imports import activate, module_load
+from ._runtime import (
+    catch, chain, dispatch, ensure, example, has, implies,
+    inherit, inv, post, pre, pure, raises, reason, safe,
+)
+from ._schemes import Scheme
+from ._sphinx import autodoc
+from ._state import disable, enable, reset
+from ._testing import TestCase, cases
+
+
+__title__ = 'deal'
+__version__ = '4.24.6'
+__author__ = 'Gram (@orsinium)'
+__license__ = 'MIT'
+__all__ = [
+    'autodoc',
+    'cases',
+    'introspection',
+    'Scheme',
+    'TestCase',
+
+    # state
+    'disable',
+    'enable',
+    'reset',
+
+    # decorators
+    'chain',
+    'dispatch',
+    'ensure',
+    'example',
+    'has',
+    'inherit',
+    'inv',
+    'post',
+    'pre',
+    'raises',
+    'reason',
+
+    # aliases
+    'catch',
+    'implies',
+    'pure',
+    'safe',
+
+    # module level
+    'module_load',
+    'activate',
+
+    # exceptions
+    'ContractError',
+    'ExampleContractError',
+    'InvContractError',
+    'MarkerError',
+    'NoMatchError',
+    'OfflineContractError',
+    'PostContractError',
+    'PreContractError',
+    'RaisesContractError',
+    'ReasonContractError',
+    'SilentContractError',
+]

plugin/contrib/deal/__main__.py

@@ -0,0 +1,6 @@
+import sys
+
+from ._cli import main
+
+
+sys.exit(main(sys.argv[1:]))

plugin/contrib/deal/_cached_property.py

@@ -0,0 +1,24 @@
+from __future__ import annotations
+
+from typing import Any, Callable, Generic, TypeVar, overload
+
+
+T = TypeVar('T')
+
+
+class cached_property(Generic[T]):  # noqa: N801
+    def __init__(self, func: Callable[[Any], T]) -> None:
+        self.func = func
+
+    @overload
+    def __get__(self, instance: None, owner: type | None = ...) -> cached_property[T]:
+        pass
+
+    @overload
+    def __get__(self, instance, owner: type | None = ...) -> T:
+        pass
+
+    def __get__(self, obj, cls):
+        value = self.func(obj)
+        obj.__dict__[self.func.__name__] = value
+        return value

plugin/contrib/deal/_colors.py

@@ -0,0 +1,50 @@
+from __future__ import annotations
+
+from ._state import state
+
+
+try:
+    import pygments
+except ImportError:
+    pygments = None
+else:
+    from pygments.formatters import TerminalFormatter
+    from pygments.lexers import PythonLexer
+
+
+COLORS = dict(
+    red='\033[91m',
+    green='\033[92m',
+    yellow='\033[93m',
+    blue='\033[94m',
+    magenta='\033[95m',
+    end='\033[0m',
+)
+NOCOLORS = dict(
+    red='',
+    green='',
+    yellow='',
+    blue='',
+    magenta='',
+    end='',
+)
+
+
+def highlight(source: str) -> str:
+    if pygments is None:  # pragma: no cover
+        return source
+    source = pygments.highlight(
+        code=source,
+        lexer=PythonLexer(),
+        formatter=TerminalFormatter(),
+    )
+    return source.rstrip()
+
+
+def get_colors(args) -> dict[str, str]:
+    if not state.color:
+        return NOCOLORS
+    if args.nocolor:
+        state.color = False
+        return NOCOLORS
+    return COLORS

plugin/contrib/deal/_exceptions.py

@@ -0,0 +1,195 @@
+from __future__ import annotations
+
+import sys
+from pathlib import Path
+from types import TracebackType
+from typing import Any
+
+from ._cached_property import cached_property
+from ._colors import COLORS, NOCOLORS, highlight
+from ._source import get_validator_source
+from ._state import state
+
+
+ROOT = str(Path(__file__).parent)
+
+
+def exception_hook(etype: type[BaseException], value: BaseException, tb: TracebackType | None):
+    """Exception hook to remove deal from the traceback for ContractError.
+    """
+    if not issubclass(etype, ContractError):
+        return _excepthook(etype, value, tb)
+
+    # try to reduce traceback by removing `deal` part
+    patched_tb: TracebackType | None = tb
+    prev_tb = None
+    while patched_tb:
+        path = patched_tb.tb_frame.f_code.co_filename
+        if path.startswith(ROOT) and prev_tb is not None:
+            prev_tb.tb_next = None
+        prev_tb = patched_tb
+        patched_tb = patched_tb.tb_next
+    else:
+        # cannot find deal in the trace, leave it as is
+        patched_tb = tb
+
+    return _excepthook(etype, value, patched_tb)
+
+
+_excepthook = sys.excepthook
+sys.excepthook = exception_hook
+
+
+class ContractError(AssertionError):
+    """The base class for all errors raised by deal contracts.
+    """
+    message: str
+    errors: Any | None
+    validator: Any
+    params: dict[str, Any]
+    origin: object | None
+
+    def __init__(
+        self,
+        message: str = '',
+        errors=None,
+        validator=None,
+        params: dict[str, Any] | None = None,
+        origin: object | None = None,
+    ) -> None:
+        self.message = message
+        self.errors = errors
+        self.validator = validator
+        self.params = params or {}
+        self.origin = origin
+
+        args = []
+        if message:
+            args.append(message)
+        if errors:
+            args.append(errors)
+        super().__init__(*args)
+
+    @cached_property
+    def source(self) -> str:
+        """The raw unformatted source code of the validator.
+        """
+        if self.validator is None:
+            return ''
+        source = get_validator_source(self.validator)
+        if source:
+            return source
+        if hasattr(self.validator, '__name__'):  # pragma: no cover
+            return self.validator.__name__
+        return repr(self.validator)
+
+    @cached_property
+    def colored_source(self) -> str:
+        """The colored source code of the validator.
+        """
+        return highlight(self.source)
+
+    @cached_property
+    def variables(self) -> str:
+        """Formatted variables passed into the validator.
+        """
+        sep = ', '
+        colors = COLORS
+        if not state.color:
+            colors = NOCOLORS
+        tmpl = '{blue}{k}{end}={magenta}{v}{end}'
+        params = []
+        for k, v in self.params.items():
+            v = repr(v)
+            if len(v) > 20:
+                continue
+            params.append(tmpl.format(k=k, v=v, **colors))
+        return sep.join(params)
+
+    def __str__(self) -> str:
+        result = self.message
+        if not result and self.errors:
+            result = repr(self.errors)
+        if not result and self.source:
+            result = 'expected '
+            if state.color:
+                result += self.colored_source
+            else:
+                result += self.source
+        if self.variables:
+            result += f' (where {self.variables})'
+        return result
+
+
+class PreContractError(ContractError):
+    """The error raised by `deal.pre` for contract violation.
+    """
+
+
+class PostContractError(ContractError):
+    """The error raised by `deal.post` for contract violation.
+    """
+
+
+class InvContractError(ContractError):
+    """The error raised by `deal.inv` for contract violation.
+    """
+
+
+class ExampleContractError(ContractError):
+    """The error raised by `deal.example` for contract violation.
+
+    `deal.example` contracts are checked only during testing and linting,
+    not at runtime.
+    """
+
+
+class RaisesContractError(ContractError):
+    """The error raised by `deal.raises` for contract violation.
+    """
+
+
+class ReasonContractError(ContractError):
+    """The error raised by `deal.reason` for contract violation.
+    """
+
+
+class MarkerError(ContractError):
+    """The base class for errors raised by `deal.has` for contract violation.
+    """
+
+
+class OfflineContractError(MarkerError):
+    """The error raised by `deal.has` for networking markers violation.
+
+    The networking can be allowed by markers `io`, `network`, and `socket`.
+    """
+
+
+class SilentContractError(MarkerError):
+    """The error raised by `deal.has` for printing markers violation.
+
+    The printing can be allowed by markers `io`, `print`, `stdout`, and `stderr`.
+    """
+
+
+class NoMatchError(Exception):
+    """The error raised by `deal.dispatch` when there is no matching implementation.
+
+    "No matching implementation" means that all registered functions
+    raised `PreContractError`.
+    """
+    __module__ = 'deal'
+
+    def __init__(self, exceptions: tuple[PreContractError, ...]) -> None:
+        self.exceptions = exceptions
+
+    def __str__(self) -> str:
+        return '; '.join(str(e) for e in self.exceptions)
+
+
+# Patch module name to show in repr `deal` instead of `deal._exceptions`
+for cls in ContractError.__subclasses__():
+    cls.__module__ = 'deal'
+for cls in MarkerError.__subclasses__():
+    cls.__module__ = 'deal'