feat(foundation): Verus verification proofs for StaticVec#137
Merged
Conversation
…tes, configs Renames CrateId::Wrt/Wrtd to CrateId::Kiln/Kilnd, updates the wrt.resource_limits custom section to kiln.resource_limits, fixes GitHub URLs, disabled workflow files, platform templates, and config files (gitignore, cspell, CODEOWNERS, memory_budget example). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…bug traces Replace position-based lowered function registration (which caused cabi_realloc to be incorrectly intercepted as a WASI function) with call-time __canon_lower_ prefix dispatch. Add FuncRef instance_id tracking for cross-instance indirect calls. Remove 468 debug println!/eprintln! statements across runtime and component crates. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add SMT-backed deductive proofs that verify unbounded correctness properties of StaticVec<T, N> — the core bounded collection used throughout Kiln. Unlike Kani (bounded model checking), Verus proves properties for ALL possible inputs and ALL capacities N. Verified properties: - Capacity invariant (len <= N always holds) - Push/pop correctness and inverse relationship - Bounds-safe get() operation - Well-formedness preservation across all operations - Drop completeness The module is gated behind #[cfg(verus)] — zero impact on normal builds, zero runtime overhead. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
🔍 Build Diagnostics ReportSummary
🎯 Impact AnalysisIssues in Files You Modified
Cascading Issues (Your Changes Breaking Other Files)
✅ No Issues DetectedPerfect! Your changes don't introduce any new errors or warnings, and don't break any existing code. 📊 Full diagnostic data available in workflow artifacts 🔧 To reproduce locally: # Install cargo-kiln
cargo install --path cargo-kiln
# Analyze your changes
cargo-kiln build --output json --filter-severity error
cargo-kiln check --output json --filter-severity warning |
Replace "WASI Preview 2" with "WASI 0.2" across all occurrences, add CI badge. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…0 errors Update the Verus proof model to use proof-mode operations throughout, matching the verified pattern that passes rust_verify. Add Bazel integration via MODULE.bazel and BUILD.bazel targets. Key changes: - All operations (new, push, pop, clear) are proof fn, not exec fn, since the model exists purely for verification - Ghost fields use direct assignment in proof mode (no Ghost wrapper) - Arithmetic casts with `as usize` for proof-mode int→usize conversion - MODULE.bazel pins rules_verus with rust_verify direct invocation - BUILD.bazel defines verus_test target for CI integration - .gitignore updated for Bazel output directories Verified properties (all unbounded — proved for ALL inputs): 1. Capacity invariant: len <= N always maintained 2. Push correctness: appends exactly one element 3. Push-full rejection: returns Err without mutation 4. Pop correctness: returns last pushed element (LIFO) 5. Push-pop inverse: push(x); pop() restores original state 6. Get bounds safety: get(i) returns Some iff i < len 7. Clear correctness: empties vector, preserves well-formedness 8. Length bounded by capacity: core ASIL-D invariant Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
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
StaticVec<T, N>, proving unbounded correctness properties that Kani's bounded model checking cannot reachverus_proofs/module gated behind#[cfg(verus)]— zero impact on normal buildscfg(verus)to expected cfgs inCargo.tomlProperties proved (for ALL inputs, ALL N)
len <= Nafter pushFiles
kiln-foundation/src/verus_proofs/mod.rs— module declarationkiln-foundation/src/verus_proofs/static_vec_proofs.rs— Verus specs and proofskiln-foundation/src/lib.rs—#[cfg(verus)] pub mod verus_proofskiln-foundation/Cargo.toml—cfg(verus)in expected cfgsTest plan
cargo check -p kiln-foundationpasses (verus module gated)verus --crate-type lib static_vec_proofs.rsverifies all proofs (requires Verus binary)Related
🤖 Generated with Claude Code