Record Verus and Stateright phase-1 boundary (4.1.3)#311
Open
leynos wants to merge 6 commits into
Open
Conversation
Contributor
SummaryThis pull request implements roadmap item 4.1.3 by formally recording the phase-1 scope boundary for Verus and Stateright formal verification tooling in Netsuke. The changes are documentation-only, with supporting workflow and build configuration updates to align with the documented scope. Key ChangesNew ExecPlan Document: Added
Documentation Updates:
Tooling Migration:
ValidationAll validation checks passed:
No changes to Rust code, Cargo manifests, CI workflows beyond uv setup, OrthoConfig, locale, or WalkthroughThis PR consolidates formal verification tool management by delegating Kani and Verus installation to ChangesProver Tool Delegation Infrastructure
Formal Verification Phase 1 Scope Boundaries
Documentation Standards and Code Guidance
Possibly related PRs
Suggested labels
Suggested reviewers
Caution Pre-merge checks failedPlease resolve all errors before merging. Addressing warnings is optional.
❌ Failed checks (2 errors, 2 warnings)
✅ Passed checks (16 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Contributor
Reviewer's GuideAdds a detailed, approval-gated ExecPlan document for roadmap item 4.1.3 that defines how to document and enforce the phase-1 boundary for Verus and Stateright, keeping them out of the mandatory tooling surface while preserving Kani as the only phase-1 formal verification gate. File-Level Changes
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
![codescene-delta-analysis[bot]](https://avatars.githubusercontent.com/in/53921?s=60&v=4){kind=small}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
lodyai
Bot
force-pushed
the
4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright
branch
from
f016add to
dbd1fa9
Compare
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Draft the approval-gated ExecPlan for roadmap item `4.1.3` so the implementation can record Verus as optional and proof-kernel-only while keeping Stateright deferred until Netsuke has stateful concurrent behaviour. Capture the expected documentation scope, validation gates, OrthoConfig boundary guardrails, Wyvern reconnaissance, and CodeRabbit rate-limit status.
Document the phase-1 formal-verification scope so Kani remains the supported gate, Verus stays optional and proof-kernel-only, and Stateright remains deferred until Netsuke has stateful concurrent behaviour to model.
Replace repository-local Kani shell scripts with the shared `rust-prover-tools` CLI pinned in the Makefile. Route Kani installation and version checks through `uv tool run`, add optional Verus install/run Make targets, and update the `kani-smoke` job to install `uv` before running `make install-kani`. Update the formal-verification docs and roadmap so contributor guidance points at the shared prover tooling instead of local scripts.
lodyai
Bot
force-pushed
the
4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright
branch
from
a960d02 to
2eff8cc
Compare
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Owner
Author
|
@coderabbitai Please investigate the cause of the following issue using codegraph exploration and research, identify a fix and provide an AI coding agent prompt for the fix: |
This comment was marked as resolved.
This comment was marked as resolved.
Remove `enable-cache: true` from the Kani smoke workflow uv setup. This job uses uv only as a tool installer, so the default `uv.lock` cache dependency glob is not applicable to this repository.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Replace the repository agent guidance with the updated AGENTS.md from the referenced memoryd branch so local agent rules stay in sync.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Replace the local documentation style guide with the latest version from the referenced memoryd main branch.
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 19f8eabe67
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| MDLINT ?= $(shell command -v markdownlint-cli2 2>/dev/null || printf '%s' "$$HOME/.bun/bin/markdownlint-cli2") | ||
| NIXIE ?= nixie | ||
| PROVER_TOOLS_SOURCE ?= git+https://github.com/leynos/rust-prover-tools@b07ef696f8373d54ae68e517d39d47a5d27a5bd5 | ||
| PROVER_TOOLS ?= uv tool run --from $(PROVER_TOOLS_SOURCE) prover-tools |
There was a problem hiding this comment.
The new PROVER_TOOLS command shells out to uv tool run --from git+https://... for both make install-kani and make kani, which means the formal-verification smoke path now depends on reaching GitHub at runtime. In any restricted or offline environment, make kani/make formal-pr can fail before invoking cargo kani, even when Kani is already installed, because the helper itself cannot be resolved. This introduces a reliability regression in CI and local validation compared with the previous repository-local scripts.
Useful? React with 👍 / 👎.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@AGENTS.md`:
- Line 294: Replace the British spelling "initialise" with the Oxford -ize form
"initialize" in the sentence containing "install global recorders or
subscribers. Applications should initialise" in AGENTS.md so the file follows
the en-GB-oxendict rule; update the single occurrence to "initialize" ensuring
the rest of the sentence and punctuation remain unchanged.
In
`@docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md`:
- Around line 37-40: The docs currently list a stale local install script
`scripts/install-kani.sh` in the preserved phase-1 contract; update the sentence
that enumerates the supported tooling to remove `scripts/install-kani.sh` and
replace it with the delegated CLI `make install-kani` so the line reads with
`tools/kani/VERSION`, `make install-kani`, and the `kani-smoke` CI job while
keeping `make kani`, `make kani-full`, and `make formal-pr` intact; ensure the
wording reflects delegation to `rust-prover-tools` rather than repository-local
shell scripts.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 49506a98-1498-4e1b-ac79-31436ec12094
📒 Files selected for processing (10)
.github/workflows/ci.ymlAGENTS.mdMakefiledocs/developers-guide.mddocs/documentation-style-guide.mddocs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.mddocs/formal-verification-methods-in-netsuke.mddocs/roadmap.mdscripts/check-kani-version.shscripts/install-kani.sh
💤 Files with no reviewable changes (2)
- scripts/check-kani-version.sh
- scripts/install-kani.sh
| user input, request IDs, paths with unbounded parameters, or raw error | ||
| strings into labels. | ||
| - Libraries may emit `metrics` and `tracing` instrumentation, but must not | ||
| install global recorders or subscribers. Applications should initialise |
Contributor
There was a problem hiding this comment.
Use Oxford -ize spelling in normative guidance.
Replace initialise with initialize to align with the repository’s en-GB-oxendict rule.
Triage: [type:spelling] [type:docstyle]
Suggested patch
- install global recorders or subscribers. Applications should initialise
+ install global recorders or subscribers. Applications should initializeAs per coding guidelines: “Use British English based on the Oxford English Dictionary locale en-GB-oxendict, including suffix -ize in words like 'realize' and 'organization'.”
🧰 Tools
🪛 LanguageTool
[style] ~294-~294: Would you like to use the Oxford spelling “initialize”? The spelling ‘initialise’ is also correct.
Context: ...ers or subscribers. Applications should initialise exporters/subscribers once, as early ...
(OXFORD_SPELLING_Z_NOT_S)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@AGENTS.md` at line 294, Replace the British spelling "initialise" with the
Oxford -ize form "initialize" in the sentence containing "install global
recorders or subscribers. Applications should initialise" in AGENTS.md so the
file follows the en-GB-oxendict rule; update the single occurrence to
"initialize" ensuring the rest of the sentence and punctuation remain unchanged.
Comment on lines
+37
to
+40
| - Preserve the existing Kani phase-1 contract from roadmap items `4.1.1` and | ||
| `4.1.2`: `make kani`, `make kani-full`, `make formal-pr`, | ||
| `tools/kani/VERSION`, `scripts/install-kani.sh`, and the `kani-smoke` CI job | ||
| remain the supported formal-verification tooling and gating surface. |
Contributor
There was a problem hiding this comment.
Remove stale scripts/install-kani.sh from the preserved phase-1 surface.
Update this constraint to match the current delegated Kani workflow and avoid documenting a legacy path that is no longer the supported contract.
Triage: [type:docstyle]
Patch
- Preserve the existing Kani phase-1 contract from roadmap items `4.1.1` and
`4.1.2`: `make kani`, `make kani-full`, `make formal-pr`,
- `tools/kani/VERSION`, `scripts/install-kani.sh`, and the `kani-smoke` CI job
+ `tools/kani/VERSION`, `make install-kani`, and the `kani-smoke` CI job
remain the supported formal-verification tooling and gating surface.Based on learnings: "Ensure Kani and Verus installation and execution are delegated to the rust-prover-tools CLI rather than repository-local shell scripts."
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In
`@docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md`
around lines 37 - 40, The docs currently list a stale local install script
`scripts/install-kani.sh` in the preserved phase-1 contract; update the sentence
that enumerates the supported tooling to remove `scripts/install-kani.sh` and
replace it with the delegated CLI `make install-kani` so the line reads with
`tools/kani/VERSION`, `make install-kani`, and the `kani-smoke` CI job while
keeping `make kani`, `make kani-full`, and `make formal-pr` intact; ensure the
wording reflects delegation to `rust-prover-tools` rather than repository-local
shell scripts.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
(4.1.3)by recording the phase-1 Verus and Stateright scope boundary.docs/formal-verification-methods-in-netsuke.mdto define Verus as optional and proof-kernel-only, with no phase-1 Cargo, Make, or CI surface.docs/developers-guide.mdwith the contributor-facing support boundary: Kani is supported and gated, Verus is optional, and Stateright is deferred.docs/roadmap.mditem4.1.3and its subitems done.docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md.Review Walkthrough
Start with
docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.mdfor the approved plan, implementation decisions, validation record, and scope notes. Then reviewdocs/formal-verification-methods-in-netsuke.mdfor the normative phase-1 boundary anddocs/developers-guide.mdfor contributor workflow guidance.Validation
make check-fmtmake lintmake testmake markdownlintmake nixiecoderabbit review --agentcompleted twice during implementation with zero findings.Notes
docs/users-guide.mdremains unchanged because no user-facing behaviour changed.make fmtwas attempted, butmdformat-alltried to rewrite unrelated Markdown files and then failed on pre-existing line-length findings outside this task. The formatter churn was restored, and all checking gates passed afterwards.References