feat(codegen): Kani harnesses for generated-code AADL contract preservation#224
Open
avrabe wants to merge 2 commits into
Open
feat(codegen): Kani harnesses for generated-code AADL contract preservation#224avrabe wants to merge 2 commits into
avrabe wants to merge 2 commits into
Conversation
…vation Add three #[kani::proof] harnesses in crates/spar-codegen/tests/kani_contracts.rs that prove each codegen pass preserves the AADL source contract (spar's Logika-equivalent strategy: machine-checked proofs on the generated-code path). - prove_thread_period_preserved: for any Period p in (0, 1_000_000_000] ns, the emitted dispatch-metadata string round-trips back to exactly p (no truncation, no off-by-one) - prove_port_direction_preserved: Out→In connections produce complementary WIT setter+getter pairs; same-direction connections never produce a complementary pair (AADL §9 directionality contract) - prove_access_right_preserved: Access_Rights = Read_Only never produces &mut in the generated access shim; Read_Write always does (type-level read-only enforcement) Wire-up: add kani-harnesses feature flag to spar-codegen/Cargo.toml; extend CI Kani job to run each harness explicitly; add REQ-KANI-CODEGEN-001 + TEST-KANI-CODEGEN to artifacts YAML. Co-Authored-By: Claude Opus 4.7 <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
This PR adds spar's Logika-equivalent strategy for generated-code correctness: instead of importing a new prover language, three Kani bounded model-checking harnesses give machine-checked proofs that each codegen pass preserves the source AADL contract.
prove_thread_period_preserved— for anyPeriod p ∈ (0, 1_000_000_000]ns, the emitted dispatch-metadata string round-trips back to exactlyp(no truncation, no off-by-one). Useskani::any()over the full nanosecond range;kani::assume(period_ns > 0 && period_ns <= MAX_PERIOD_NS).prove_port_direction_preserved—Outsource maps exclusively to a WIT setter;Insink to a getter; a well-formedOut→Inconnection always produces a complementary setter+getter pair; same-direction features never produce a complementary pair. Proves the AADL §9 directionality contract over all direction combinations.prove_access_right_preserved—Access_Rights = Read_Onlynever produces&mutin the generated access shim;Read_Writealways does. Proves read-only enforcement at the Rust type level.Wire-up
crates/spar-codegen/tests/kani_contracts.rs— three#[cfg(kani)] #[kani::proof]harnessescrates/spar-codegen/Cargo.toml—kani-harnessesfeature flag (no-op at runtime; enablescargo build -p spar-codegen --features kani-harnessesfor CI compilation gating).github/workflows/ci.yml— CI Kani job extended to run each harness by nameartifacts/requirements.yaml—REQ-KANI-CODEGEN-001(implemented, tags: codegen/kani/verification/v0100/safety)artifacts/verification.yaml—TEST-KANI-CODEGEN(passing, satisfiesREQ-KANI-CODEGEN-001)Design note
Kani cannot symbolically construct
SystemInstancevalues (they embedla_arena::Idxhandles requiring a live arena). Following the pattern established inkani_codegen.rsandkani_solver.rs, each harness models the pure functions the codegen calls and asserts the invariant that pass must satisfy. Any divergence between the Kani model and production would be caught by the existing unit + golden tests.Test plan
cargo build -p spar-codegen --features kani-harnesses— compiles cleancargo test -p spar-codegen— 19 unit tests pass, harness files load without errorcargo kani --tests -p spar-codegen --harness prove_thread_period_preserved(CI)cargo kani --tests -p spar-codegen --harness prove_port_direction_preserved(CI)cargo kani --tests -p spar-codegen --harness prove_access_right_preserved(CI)rivet validate— no new errors (pre-existing YAML parse issue at verification.yaml:1648 is unrelated)🤖 Generated with Claude Code