Add Kani proofs for MacroStateGuard pointer lifecycle (#313)#381
Draft
leynos wants to merge 1 commit into
Draft
Conversation
`MacroInstance::new` transmutes a `Captured` to `Captured<'static>`, and `MacroStateGuard` stores it as a `NonNull<Captured<'static>>` while being declared `Send + Sync`. Neither the pointer lifecycle nor the thread-safety markers had formal verification. Extract the raw-pointer dance into payload-agnostic helpers, `heap_leak_non_null` and `reclaim_heap_non_null`, which `MacroStateGuard::new` and its `Drop` now use verbatim. Add a `#[cfg(kani)]` module with four proofs: - `macro_state_guard_ptr_is_non_null` — the leaked pointer is non-null and dereferences to the stored value; - `macro_state_guard_drop_is_safe` — the Box → raw → Box round-trip neither leaks nor double-frees; - `macro_instance_is_send` / `macro_instance_is_sync` — compile-time assertions of the marker traits. `Captured`/`State` are too complex for Kani to construct, so the pointer proofs run the real helpers over a small Kani-constructible stand-in payload (the unsafe operations are independent of payload type beyond non-zero size). Register `cfg(kani)` in `Cargo.toml` so ordinary builds do not flag the gated module, extend the `MacroInstance::new` SAFETY comment to reference the proofs by name, and refresh the formal-verification section of the developers' guide. Verified locally with Kani 0.67.0: 4 harnesses, 0 failures.
Contributor
|
Important Review skippedDraft detected. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Plus Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
![codescene-delta-analysis[bot]](https://avatars.githubusercontent.com/in/53921?s=60&v=4){kind=small}
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
Closes #313
Adds the four Kani proofs requested as a follow-up to #288, verifying the unsafe pointer lifecycle and thread-safety markers behind manifest macro caching.
Changes
src/manifest/jinja_macros/cache.rs:Box::into_raw→NonNull::new_uncheckedandBox::from_rawdance into payload-agnostic helpersheap_leak_non_null/reclaim_heap_non_null, used verbatim byMacroStateGuard::newand itsDropso the proofs cover the real code;#[cfg(kani)]module withmacro_state_guard_ptr_is_non_null,macro_state_guard_drop_is_safe,macro_instance_is_send,macro_instance_is_sync;MacroInstance::newSAFETY comment to state the precondition and reference the proofs by name.Cargo.toml: registercfg(kani)under[lints.rust](unexpected_cfgscheck-cfg) so ordinary builds do not flag the gated proofs.docs/developers-guide.md: refresh the formal-verification section to record that the first proof harnesses now exist.Modelling note
Captured<'static>/Statecannot be constructed or unwound by Kani, so (as the issue permits) the pointer proofs exercise the real helpers over a small Kani-constructible stand-in payload; the verified unsafe operations are independent of the payload type beyond its being non-zero-sized. TheSend/Syncproofs assert the marker traits on the realMacroInstance.Validation
rg '#\[kani::proof\]' src/manifest/jinja_macros/cache.rs→ 4kani-smokevalidates independently).make check-fmt/make markdownlint/make lint/make test— pass (37 suites; proofs gated out of ordinary builds).🤖 Generated with Claude Code