Add Kani tooling and local smoke targets (4.1.1)#305
Open
leynos wants to merge 3 commits into
Open
Conversation
Draft the approval-gated plan for roadmap item 4.1.1. Capture the Kani version-pin, installer-script, and local Make target workflow, along with validation, review, and rollback guidance.
Contributor
WalkthroughThis PR establishes Kani bounded model checker integration for Netsuke. It pins version 0.67.0, adds a Bash installer script, wires Make targets ( ChangesKani tooling integration
Suggested labels
Poem
Caution Pre-merge checks failedPlease resolve all errors before merging. Addressing warnings is optional.
❌ Failed checks (2 errors, 1 warning, 1 inconclusive)
✅ Passed checks (14 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
![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.
Pin the supported Kani verifier version and add the local installer script used by the formal-verification workflow.
Expose local Kani smoke and full-suite Make targets for the formal-verification workflow, document their use, and mark roadmap item 4.1.1 complete after validation.
Contributor
Reviewer's GuideAdds pinned Kani formal-verification tooling and opt-in Make targets, plus documentation and roadmap updates, to establish a repeatable local Kani smoke workflow without impacting existing CI/test paths. Sequence diagram for make formal-pr Kani smoke workflowsequenceDiagram
actor Developer
participant Make
participant cargo_kani
Developer->>Make: make formal-pr
Make->>Make: kani
Make->>cargo_kani: cargo kani --version
Flow diagram for scripts/install-kani.sh installation stepsflowchart TD
A[run scripts/install-kani.sh] --> B[require_command cargo]
B --> C[read tools/kani/VERSION]
C --> D[validate MAJOR.MINOR.PATCH]
D --> E[cargo install --locked kani-verifier --version <version>]
E --> F[cargo kani setup]
F --> G[cargo kani --version]
File-Level Changes
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Hey - I've found 2 issues
Prompt for AI Agents
Please address the comments from this code review:
## Individual Comments
### Comment 1
<location path="docs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.md" line_range="44" />
<code_context>
+- Keep Makefile additions consistent with the current target style: variables
+ near the top, `.PHONY` declarations, target descriptions using `##`, and
+ recipes that honour overrideable variables.
+- Preserve the existing OrthoConfig and localized CLI help surfaces. This
+ item adds developer tooling, not a user-facing Netsuke subcommand or flag.
+- If any Kani-specific Rust source is introduced later during implementation,
</code_context>
<issue_to_address>
**issue (typo):** Align "localized" with the stated en-GB-oxendict spelling ("localised").
This bullet references en-GB-oxendict spelling but uses the en-US form "localized"; please change it to "localised" for consistency with the documented style.
```suggestion
- Preserve the existing OrthoConfig and localised CLI help surfaces. This
```
</issue_to_address>
### Comment 2
<location path="docs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.md" line_range="276" />
<code_context>
+
+## Context and orientation
+
+Netsuke is a Rust build-system compiler. It reads a YAML `Netsukefile`, expands
+MiniJinja-controlled manifest logic, validates a static Intermediate
+Representation (IR), emits a deterministic Ninja file, and delegates execution
</code_context>
<issue_to_address>
**suggestion (review_instructions):** The acronym “YAML” is used without being expanded on first use.
Please expand YAML on first use, for example: “YAML Ain’t Markup Language (YAML) `Netsukefile`”. Later occurrences can use “YAML” alone.
<details>
<summary>Review instructions:</summary>
**Path patterns:** `**/*.md`
**Instructions:**
Define uncommon acronyms on first use.
</details>
</issue_to_address>Help me be more useful! Please click 👍 or 👎 on each comment and I'll use the feedback to improve your reviews.
| - Keep Makefile additions consistent with the current target style: variables | ||
| near the top, `.PHONY` declarations, target descriptions using `##`, and | ||
| recipes that honour overrideable variables. | ||
| - Preserve the existing OrthoConfig and localized CLI help surfaces. This |
Contributor
There was a problem hiding this comment.
issue (typo): Align "localized" with the stated en-GB-oxendict spelling ("localised").
This bullet references en-GB-oxendict spelling but uses the en-US form "localized"; please change it to "localised" for consistency with the documented style.
Suggested change
| - Preserve the existing OrthoConfig and localized CLI help surfaces. This | |
| - Preserve the existing OrthoConfig and localised CLI help surfaces. This |
|
|
||
| ## Context and orientation | ||
|
|
||
| Netsuke is a Rust build-system compiler. It reads a YAML `Netsukefile`, expands |
Contributor
There was a problem hiding this comment.
suggestion (review_instructions): The acronym “YAML” is used without being expanded on first use.
Please expand YAML on first use, for example: “YAML Ain’t Markup Language (YAML) Netsukefile”. Later occurrences can use “YAML” alone.
Review instructions:
Path patterns: **/*.md
Instructions:
Define uncommon acronyms on first use.
![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: b9e59e9e6b
ℹ️ 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".
| nixie --no-sandbox | ||
|
|
||
| kani: ## Run the Kani local smoke check | ||
| $(KANI) $(KANI_SMOKE_FLAGS) |
There was a problem hiding this comment.
When a developer or CI image already has cargo-kani installed at a different version, this target exits successfully because it only runs cargo kani --version and never compares that output with tools/kani/VERSION; formal-pr delegates to this target, so stale or newer Kani binaries can validate PRs despite the new pinned-version contract. Please have the smoke path read the version pin and fail on a mismatch, or route it through a script that performs that check.
Useful? React with 👍 / 👎.
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
This branch implements roadmap task (4.1.1), adding the pinned local Kani tooling contract for Netsuke's formal-verification workflow.
It adds
tools/kani/VERSION,scripts/install-kani.sh, and the localmake kani,make kani-full, andmake formal-prtargets. It also documents the developer workflow and marks the roadmap item complete after validation.Roadmap task: (4.1.1)
Execplan: docs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.md
Review walkthrough
tools/kani/VERSIONandscripts/install-kani.shfor the pinnedkani-verifierinstallation path.Makefilefor the opt-in Kani smoke, full-suite, and formal pull-request targets.docs/developers-guide.mdanddocs/roadmap.mdfor the developer workflow and completed roadmap checkboxes.Validation
scripts/install-kani.sh: passed, installedkani-verifier0.67.0 and rancargo kani setupmake kani: passedmake formal-pr: passedmake kani-full: passed; currently reports that no#[kani::proof]harnesses existmbake validate Makefile: passedmake check-fmt: passedmake lint: passedmake test: passedmake markdownlint: passedmake nixie: passedcoderabbit review --agent: passed with 0 findings on each milestone and final runNotes
make fmtwas attempted, but it still fails on pre-existing Markdown line-length and table issues in unrelated documentation. Formatter-only edits outside this branch's intended files were restored.Summary by Sourcery
Add pinned Kani formal-verification tooling and local make targets for smoke and full runs, along with developer documentation and roadmap updates.
New Features:
Enhancements:
Documentation: