feat: support verus! blocks in Rust

.github/workflows/ci.yml

@@ -44,7 +44,7 @@ jobs:
         with:
           python-version: "3.13"
 
-      - run: uv sync --all-groups
+      - run: uv sync --locked --all-groups
 
       - run: uv tool install ty && ty check
 
@@ -65,20 +65,27 @@ jobs:
         with:
           python-version: ${{ matrix.python-version }}
 
-      - run: uv sync --all-groups
+      - run: uv sync --locked --all-groups
 
       - run: uv run pytest -q tests/
 
   package:
-    name: Package Smoke Test
-    runs-on: ubuntu-latest
+    name: Package Smoke Test (${{ matrix.os }})
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
     steps:
       - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v7.0.0
         with:
           persist-credentials: false
 
       - uses: astral-sh/setup-uv@11f9893b081a58869d3b5fccaea48c9e9e46f990  # v8.3.2
 
+      - uses: actions/setup-python@ece7cb06caefa5fff74198d8649806c4678c61a1  # v6.3.0
+        with:
+          python-version: "3.13"
+
       - run: uv build
       - run: uv venv /tmp/trailmark-wheel && uv pip install --python /tmp/trailmark-wheel dist/*.whl
       - run: /tmp/trailmark-wheel/bin/python tests/package_smoke.py tests/fixtures/kat

.github/workflows/mutation.yml

@@ -5,16 +5,17 @@ on:
     branches: [main]
   pull_request:
     branches: [main]
+  workflow_dispatch:
 
 concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: true
+  group: mutation-${{ github.event_name == 'pull_request' && github.ref || github.run_id }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
 
 permissions:
   contents: read
 
 jobs:
-  mutmut:
+  gremlins:
     name: Mutation Testing
     runs-on: ubuntu-latest
     steps:
@@ -28,11 +29,29 @@ jobs:
         with:
           python-version: "3.13"
 
-      - run: uv sync --all-groups
+      - run: uv sync --locked --all-groups
 
-      - name: Run mutation testing
-        run: uv run mutmut run
+      - name: Run reviewed mutation scope
+        if: github.event_name == 'pull_request'
+        run: uv run --locked python -m tests.run_mutations --reviewed --workers=4
 
-      - name: Show results
+      - name: Run full mutation campaign
+        if: github.event_name != 'pull_request'
+        run: uv run --locked python -m tests.run_mutations --workers=4
+
+      - name: Enforce reviewed Rust and Verus baseline
+        run: uv run --locked python -m tests.mutation_gate
+
+      - name: Record revision
         if: always()
-        run: uv run mutmut results
+        run: |
+          mkdir -p coverage/gremlins
+          git rev-parse HEAD > coverage/gremlins/revision.txt
+
+      - name: Upload mutation reports
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02  # v4.6.2
+        with:
+          name: mutation-report-${{ github.sha }}
+          path: coverage/gremlins/
+          if-no-files-found: error

.gitignore

@@ -12,4 +12,7 @@
 *.pyc
 mutants/
 src/trailmark/tree_sitter_custom/**/*.so
-src/trailmark/tree_sitter_custom/**/*.pyd
+src/trailmark/tree_sitter_custom/**/*.pyd
+.gremlins_cache/
+coverage/gremlins/
+.coverage.*

AGENTS.md

@@ -74,19 +74,16 @@ uv run pytest -q tests/
 ## Mutation Testing
 
 ```bash
-uv run mutmut run
-uv run mutmut results
+uv run python -m tests.run_mutations --reviewed --workers=4
+uv run python -m tests.mutation_gate
 ```
 
-### macOS Fork Safety
-
-mutmut uses `fork()` which segfaults with rustworkx on macOS. Set:
-
-```bash
-export OBJC_DISABLE_INITIALIZE_FORK_SAFETY=YES
-```
-
-This is not needed on Linux/CI (Ubuntu).
+The runner uses real pytest subprocesses and validates clean and instrumented
+baselines. It orders component unit tests first and retains all selected tests
+as fallback. Use it rather than invoking the pinned plugin directly. Omit
+`--reviewed` for a full repository campaign; CI runs that after merges
+and on manual dispatch. `--workers` already enables parallel execution.
+Do not enable `TRAILMARK_UPDATE_SNAPSHOTS` during CI or mutation testing.
 
 ## Adding Features
 

NOTICE

@@ -10,3 +10,8 @@ This product bundles the following third-party components:
   Copyright 2024 Decurity
   Licensed under the MIT License
   https://github.com/nicedrop/tree-sitter-circom
+
+- tree-sitter-verus grammar (src/trailmark/tree_sitter_custom/verus/)
+  Copyright (c) 2017 Maxim Sokolov
+  Licensed under the MIT License
+  https://github.com/secure-foundations/tree-sitter-verus

README.md

@@ -52,7 +52,7 @@
 | C# | `.cs` | methods, classes, interfaces, structs, enums, namespaces |
 | Java | `.java` | methods, classes, interfaces, enums |
 | Go | `.go` | functions, methods, structs, interfaces |
-| Rust | `.rs` | functions, structs, traits, enums, impl blocks |
+| Rust | `.rs` | functions, structs, traits, enums, impl blocks, `verus!` blocks |
 | Solidity | `.sol` | contracts, interfaces, libraries, functions, modifiers, structs, enums |
 | Cairo | `.cairo` | functions, traits, structs, enums, impl blocks, StarkNet contracts |
 | Circom | `.circom` | templates, functions, signals, components |
@@ -73,6 +73,24 @@
 | GraphQL | `.graphql`, `.gql` | object types, root operations, fields, enums |
 | SQL | `.sql` | schemas, tables, views, functions, procedures |
 
+The Rust parser extracts ordinary, `spec`, and `proof` functions with bodies
+from `verus! { ... }` blocks. The Verus grammar currently supports only
+brace-delimited blocks; `verus!(...)` and `verus![...]` are skipped with a warning.
+Inline modules retain qualified IDs (for example, `file.inner:function`), and
+methods retain their impl or trait owner. Each block is parsed independently;
+syntax errors produce a warning with the file and block location.
+Qualified invocations such as `vstd::prelude::verus!` are supported too.
+Local helper functions retain their enclosing function in their IDs (for example,
+`file:outer.inner`). Calls to these helpers and relative imports such as
+`use super::*` resolve to declarations present in the file.
+Repeated local names in different blocks receive a byte-offset suffix to keep
+their nodes distinct, and calls respect block scope.
+
+Trailmark does not expand arbitrary macros. Literal Verus invocations inside
+opaque macros or function bodies are skipped with a warning. Uninvoked
+`macro_rules!` definitions are not expanded. Function signatures without bodies
+and calls in `requires`/`ensures` clauses are not extracted.
+
 ```mermaid
 flowchart TD
     subgraph "Per-File Parsing"
@@ -219,8 +237,8 @@
     def verify(self, token: str) -> bool:
         return self._check_sig(token)
 
     def _check_sig(self, token: str) -> bool:
         ...
 
 def handle_request(req: Request) -> Response:
     auth = Auth()
@@ -271,6 +289,16 @@
 directory to the target machine. `HTTPS_PROXY` is also honored. The SQL grammar
 ships as the `tree-sitter-sql` wheel dependency and does not use that cache.
 
+The bundled Circom, Miden Assembly, and Verus grammars compile on first use.
+This requires a C compiler (`cc`), Python development headers, and write access
+to their installed grammar directories. Rust files without Verus blocks do not
+trigger compilation. If the Verus grammar cannot be built or loaded, Trailmark
+logs a warning, skips Verus blocks, and continues parsing ordinary Rust.
+The Verus binding cache includes the compiled source contents, Python ABI,
+platform, and compiler options. Changed inputs select a new binding; completed
+builds are published atomically. Compiler failures include the exit status and
+stderr in the warning.
+
 ## Usage
 
 ```bash
@@ -534,10 +562,39 @@
 # Tests
 uv run pytest -q tests/
 
-# Mutation testing (on macOS, set this env var to avoid rustworkx fork segfaults)
-OBJC_DISABLE_INITIALIZE_FORK_SAFETY=YES uv run mutmut run
+# Mutation testing with pytest-gremlins
+uv run python -m tests.run_mutations --reviewed --workers=4
+uv run python -m tests.mutation_gate
+
+# Full repository mutation campaign
+uv run python -m tests.run_mutations --workers=4
 ```
 
+Mutation reports are written to `coverage/gremlins/`. Pull requests mutate the
+Rust/Verus files named in `tests/mutation_baseline.json` and gate new and
+changed functions there. Full repository campaigns run on pushes to main
+and through the mutation workflow's manual trigger. Unchanged legacy functions
+are identified by source hashes and enter the gate automatically when edited.
+The gate rejects unreviewed survivors, missing tests/results, errors, and timeouts.
+Exceptions require a reason and a fingerprint of the function and mutation;
+changing that function requires reviewing its exceptions again.
+
+The runner pins pytest-gremlins 1.9.0 and uses real pytest subprocesses for every
+mutant, including fixtures and parametrized tests. Each mutant retains the full
+selected test suite: component unit tests run first, followed by the remaining
+tests, stopping at the first failure. Shared-helper mutants retain tests from
+every language. Tests stay in their existing files; `tests/mutation_order.py`
+defines the ordering, and unknown components retain collection order. The runner
+skips the redundant coverage pre-scan, checks the clean baseline and each distinct
+instrumented test ordering, and preserves package metadata and exact parameter
+IDs when loading mutated code.
+These compatibility measures address upstream runner and selection issues;
+their control tests must pass before upgrading the plugin.
+Snapshot updates (`TRAILMARK_UPDATE_SNAPSHOTS=1`) are disabled during CI and mutation
+runs. To focus a local campaign, pass `--targets` with comma-separated source
+paths, followed by the relevant test files. `--workers=4` already enables parallel
+execution. Use `--test-order=collection` to compare against pytest's original order.
+
 ## License
 
 Apache-2.0

pyproject.toml

@@ -30,10 +30,11 @@ trailmark = "trailmark.cli:main"
 [dependency-groups]
 dev = [
     "hypothesis>=6.150.0",
-    "mutmut>=3.4.0",
+    "pytest-gremlins==1.9.0",
     "pytest>=9.0",
     "pytest-cov>=7.0.0",
     "ruff>=0.15.0,<1.0",
+    "pytest-timeout>=2.4,<3",
 ]
 
 [tool.ruff]
@@ -52,7 +53,4 @@ select = [
 
 [tool.pytest.ini_options]
 testpaths = ["tests"]
-
-[tool.mutmut]
-paths_to_mutate = ["src/trailmark/"]
-pytest_add_cli_args_test_selection = ["tests/"]
+markers = ["mutation_infrastructure: validate the runner once in its clean baseline"]

src/trailmark/parsers/_common.py

@@ -165,6 +165,8 @@ def collect_body_info(
     branches: list[BranchInfo],
     exception_types: list[TypeRef],
     calls: list[tuple[str, Node]],
+    *,
+    skip_types: frozenset[str] = frozenset(),
 ) -> None:
     """Collect branches, exceptions, and calls from a function body.
 
@@ -174,6 +176,8 @@ def collect_body_info(
     stack: list[Node] = list(reversed(body.children))
     while stack:
         node = stack.pop()
+        if node.type in skip_types:
+            continue
         if node.type in branch_types:
             condition = _extract_condition_text(node)
             branches.append(
@@ -293,10 +297,15 @@ def add_contains_edge(
     )
 
 
-def extract_type_parameters(node: Node) -> tuple[TypeParameter, ...]:
+def extract_type_parameters(
+    node: Node, *, field_name: str | None = None
+) -> tuple[TypeParameter, ...]:
     """Best-effort extraction of generic parameter declarations."""
-    text = node_text(node)
-    raw = _generic_parameter_block(text)
+    if field_name is None:
+        raw = _generic_parameter_block(node_text(node))
+    else:
+        parameters = node.child_by_field_name(field_name)
+        raw = node_text(parameters)[1:-1] if parameters is not None else None
     if raw is None:
         return ()
     params = [_parse_type_parameter(part) for part in _split_top_level(raw)]