[feliperodri]

First PR of the series that RFC #5111 proposes for aliasing checks (-Z aliasing-checks). It adds the monitor, the functions that apply Tree Borrows' rules at the one memory byte the checks track, and a Verus proof that they implement those rules. Nothing calls the monitor yet: the next PR adds the MIR instrumentation that does.

Why on its own: the monitor is where the subtle rules are (conflicted Reserved, protectors, interior mutability, wildcard accesses), and it has no dependency on a CBMC release, unlike the instrumentation. It is easier to check against Miri's rules here than inside the compiler pass.

What to look at:

• The specification in library/kani_core/verus/aliasing_monitor.rs (local_step, foreign_step, retag_node, wild_access, return_spec, ...). It is the trusted part: the proof shows that the code implements it, not that it is Tree Borrows. Each rule cites the Miri code it transcribes (tree_borrows/perms.rs, tree.rs). The next PR checks it a second way, by running Miri's own borrow tests under both tools.
• The bit-level encoding, described at the top of library/kani_core/src/aliasing_monitor.rs: up to 64 tags, each with its ancestors and permission as bit masks.
• The new CI workflow, which downloads a pinned Verus release and runs the proof (about 3 minutes) when these files change.

Risk: none for users. The macro isn't expanded anywhere yet; the only change to the build is mod aliasing_monitor; in kani_core.

Where I'd like input:

• Is a CI job that depends on a pinned Verus release acceptable? It only runs when the monitor or its proof changes.
• Would you rather expand the macro now, so that every Kani library build compiles it? That catches breakage from toolchain upgrades earlier, at the cost of unused functions in the library until the next PR.

Testing:

• Verus 0.2026.10.04.426d8b0: verification results:: 163 verified, 0 errors. The proof uses no assume, admit or external_body.
• cargo build-dev, cargo clippy -p kani_core -- -D warnings and kani-fmt --check pass. The Intrinsics tests of the kani suite (177) pass; the full regression suite has not been run on this branch.

[Copilot]

Warning

Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.

Copilot review overview

2 open issues

• This workflow claims to run only when the monitor/proof changes, but merge_group has no path… · New
• The workflow downloads and executes a prebuilt tool archive without integrity verification beyond… · New

What changed in this PR

Adds the Tree Borrows “aliasing monitor” transition core to kani_core, alongside a Verus specification/proof that the implementation refines that spec, plus CI wiring to run the proof on relevant changes.

Changes:

• Introduces kani_aliasing_monitor! implementation (state + transition functions) in library/kani_core/src/aliasing_monitor.rs.
• Adds a large Verus spec/proof harness (library/kani_core/verus/aliasing_monitor.rs) and documentation (library/kani_core/verus/README.md).
• Adds a GitHub Actions workflow to download a pinned Verus release and run the proof on changes.

File	Description
library/​kani_core/​verus/​aliasing_monitor.rs	New Verus spec + proofs, includes and verifies the monitor implementation.
library/​kani_core/​verus/​README.md	Documents how to run the proof and what is/ isn’t proved.
library/​kani_core/​src/​lib.rs	Compiles in the new aliasing monitor module.
library/​kani_core/​src/​aliasing_monitor.rs	Adds the monitor implementation and Verus-only contracts/proof hooks.
.github/​workflows/​verus.yml	Adds CI job to run the Verus proof when monitor/proof changes.

_{Review effort: Lite}