Repository navigation
Generate bounded Kani contracts and proof dependencies - #25
Conversation
|
Exact-head review request: Please perform an independent full code review and gap analysis of this exact head, including semantic mutation of Kani dependency readiness, unsupported constructs, executable-oracle parity, and attestation identity. Confirm that Agent B harness/vacuity commits are absent. Post an explicit exact-SHA landing verdict and do not dispatch hosted CI. If the branch moves, re-review is required. |
Independent exact-head review — PR #25Head reviewed: Prior review status: this is the first review of this PR. Agent B isolation — confirmed. Verdict⛔ Changes requested — 5 high / 10 medium / 5 low. The generation logic is careful and, in several places, better than the program average. But the central question the lens asks — can a downstream consumer mistake a generated-but-unproven artifact for a discharged proof? — the answer at this head is yes, and it is reachable through the field a consumer would actually filter on. Separately, three retained assurance documents now assert a fact the tree contradicts, and HighK25-01 — the Kani proof attestations carry
|
| Claimed class | Implemented at | Fixture |
|---|---|---|
| Unsupported backend version | kani.rs:522 |
✅ :409 |
| Invalid path/identity | kani.rs:536-537, :631 |
✅ :415 |
| Invalid attestation context | kani.rs:552 |
✅ :423 |
| Invalid unwind | kani.rs:545 |
✅ :430 |
| Invalid dependency combination | kani.rs:570-614 |
✅ :437 |
| Unsupported binding | kani.rs:667 |
✅ :463 |
| Duplicate dependency identity / collision with root | kani.rs:563 |
❌ none |
| Precondition clause == postcondition clause | kani.rs:529 |
❌ none |
| Non-Boolean root | via map_clause_diagnostics, kani.rs:793 |
❌ none |
Staging is correct where fixtures exist — each was traced against validate_request's ordering and every one is valid to all preceding stages and dies at the stage it claims. Two weaknesses: the subject-path case at :415 asserts only code == InvalidIdentity, which validate_plain_identity(proof_id, …) also returns, so the assertion does not discriminate which validator fired — diagnostic.path ("subject_path") is the discriminating field and is not asserted. And map_clause_diagnostics is the only path that populates KaniDiagnostic::generation_code (kani.rs:802); with no non-Boolean-root or unsupported-expression fixture, that field is never non-None in any test.
K25-10 — attestation_diagnostic is unreachable and discards the code the struct has a field for
src/kani.rs:809-819
generated_output_attestation returns Err on exactly two conditions: !attestation_context_is_valid(context) (oracle.rs:1024) and serialization failure. The first is already rejected by validate_request at kani.rs:552 before generation begins; the second cannot occur for these plain structs. So both arms are unreachable. Worse, the reachable-in-principle arm collapses everything to SerializationFailed:
let kani_code = match code {
GenerationErrorCode::InvalidAttestationContext => KaniErrorCode::InvalidAttestationContext,
_ => KaniErrorCode::SerializationFailed, // src/kani.rs:812
};and single_diagnostic sets generation_code: None (kani.rs:826), discarding the upstream code — while its sibling map_clause_diagnostics preserves it. A swallowed error class beside a preserving one, on a path nothing can reach.
K25-11 — duplicate stub/assumption paths are not rejected, despite the error code's own doc saying they are
src/kani.rs:142, :559-569, :594-606
KaniErrorCode::InvalidIdentity is documented as "A proof, subject, assumption, or stub identity is invalid or duplicated." Only dependency.proof_id is deduplicated (:563). Two Stubbed dependencies with distinct proof_ids and the same original_path validate, and the generator emits two conflicting #[kani::stub(same, a)] / #[kani::stub(same, b)] attributes. original_path == replacement_path (self-stub) is likewise unchecked. Both are Kani-time errors at best; the generator should fail closed here, and its own doc says it does.
K25-12 — cargo test now hard-requires cargo-kani 0.67.0; the CI workflow installs it nowhere
.github/workflows/ci.yml:28-29 · tests/kani_generation.rs:578-587
pinned_kani_executes_the_generated_contract_proof fails loudly if cargo kani --version is absent or not exactly cargo-kani 0.67.0 — which is the right behaviour and matches tests/common/mod.rs's stated policy that a missing prerequisite is a failure, never a skip. But the hosted workflow's Test step is cargo test with no cargo-kani installation anywhere in the job. Dispatching CI at this head would go red on a missing tool rather than on a defect. (The quoin half of this is pre-existing — the workflow installs quoin in the later "Validate specification" step — so Test is already red on main for that reason. Neither is declared.) No CI was dispatched during this review, per the program rule.
To close: add a cargo-kani 0.67.0 install step before Test, or split the Kani suite behind an explicit job, and record the CI prerequisite in spec/evidence/suites.md beside SUITE-008.
K25-13 — the derived input/state binding is discarded into comments; a swapped subject signature proves the wrong statement
src/kani.rs:643-702 · src/kani.rs:356-364
derive_binding does real work — it rejects everything outside one Boolean input plus pre/post state, with a correct _ => fall-through at :667 and no early return. Then KaniBinding { input_name, state_name } is consumed at exactly two places: // input-binding: {} and // state-binding: {} (kani.rs:357-358). The generated call is positional and fixed:
fn call_subject(input: bool, pre_state: bool) -> bool {
<subject_path>(input, pre_state) // src/kani.rs:363
}subject_path is validated only as a syntactic syn::Path (kani.rs:631). A customer function declared fn subject(pre_state: bool, input: bool) type-checks, verifies, and proves a statement about the wrong argument assignment. The two names that could catch this are computed and then written to a comment. Per technique 1, the framing block has no read site: git grep input-binding finds only the emission.
(Credit where due: the argument-order risk in predicate_arguments was traced and is sound — dependency_parameters produces the parameter order for both generate_boolean_oracle's signature (oracle.rs:443-448) and the Kani call site (kani.rs:704-728), from the same call on the same expression, so positional agreement holds by construction.)
K25-14 — kani_implementation_digest() has no independent re-derivation test, breaking an established repo convention
src/kani.rs:897-919 · tests/oracle_generation.rs:100-121, :399-402
The repo has a good pattern: expected_implementation_digest() in tests/oracle_generation.rs:100 re-lists the nine hashed inputs independently, so adding a file to one side and not the other fails. This PR introduces a second, different configuration digest over a different seven-file set — and provides no equivalent test. git grep configuration_digest -- tests finds only the oracle assertion. Deleting kani.rs:474 and substituting generator_implementation_digest() breaks nothing.
Consequence for consumers: within one bundle, tool.identity and tool.version are identical across all attestations while tool.configuration_digest now takes two values, and nothing in the record says which subset each covers.
K25-15 — an empty dependency census yields ready vacuously, with nothing recording that a census was taken
src/kani.rs:766-768 · schemas/kani-proof-graph-v1.schema.json:42-44
dependency_readiness(&[]) falls through both any(...) predicates — both vacuously false over an empty slice — and returns Ready. The schema places no minItems on dependencies. A caller that passed &[] because it could not enumerate dependencies is indistinguishable from one whose proof genuinely has none, and the field is documented as "Complete caller-owned dependency census" (kani.rs:130) with nothing requiring the caller to assert completeness. This is the empty-set vacuity pattern recurring across the program, and no test asserts the empty case at all — fixture_bundle(&[]) is used at :471, :557 and :606 but its readiness is never read.
Low
- K25-16 —
schemas/generated-rust-kani-v1.schema.jsonis nine unanchored substring patterns, every one satisfied by the fixed template and none of them structural. A file containing only the marker comments validates. It has no negative probe (contrast the good one for the proof graph attests/kani_generation.rs:396-401), yet its digest is bound into both attestations as--output-schema-digest(src/kani.rs:485), so a consumer told "this validates against schema X" is told very little. - K25-17 —
kani_bundle_is_deterministic_schema_valid_and_stable_rust_compiles(tests/kani_generation.rs:315-330) runscargo checkwithout--cfg kani. The entire framing/binding/contract/harness module is behind#[cfg(kani)](src/kani.rs:351), so that step type-checks only the two embedded oracle functions. Real coverage of the module comes from the Kani test alone. The test name overstates. - K25-18 —
KaniErrorCode::ResourceLimitExceeded → GenerationTerminalState::Unsupported(src/kani.rs:172-174) conflates "out of budget" with "out of scope". Under the governing principle these are different answers;Inconclusiveis the honest one. - K25-19 — the census arithmetic comment at
tests/shared_assurance.rs:1494-1500("this head 30 … added 0 … 45 − 15 + 0 = 30") is stale by +4 at this head (2 schemas, 1 src, 1 tests). Theinspected >= 27floor still holds, so nothing fails — but this file's own prose says every figure was re-derived rather than inherited. - K25-20 — SUITE-008 is registered in
spec/evidence/suites.md:19but feeds nothing intoscripts/assurance_chain.py'sINPUTS(:58-61); its only record is a terminal transcript.suites.md:47-53states this ("local pre-review evidence"), so it is a declared gap, not a hidden one.
Proof-state table
For a generated Kani artifact at this head. "Representable" = the artifact set has a slot for it; "distinguishable" = a consumer reading the retained record can tell it from a discharged proof.
| State | Representable in artifact | Distinguishable in record | Mistakable for discharged |
|---|---|---|---|
| Generated, not run | Yes — proofExecutionState: "not_run", kani.rs:418 |
Partly. Distinguishable in the graph. In the two ProofAttestationV1 bodies it is argv element n while result reads passed. |
Yes — K25-01 |
| Proved (Kani ran, SUCCESSFUL, non-vacuous) | No — schema pins proofExecutionState to const: "not_run"; no result intake exists |
n/a | n/a |
| Refuted (Kani ran, FAILURE) | No — same | n/a | n/a |
| Unwind bound insufficient | No. Kani's unwinding assertions are on (no --no-unwinding-checks in adapter_options, kani.rs:771-791), so a run would report FAILURE — but there is no field for the outcome, and as a dependency it must be forced into passed/failed/missing (K25-07) |
No | Via a dependency reported passed |
| Vacuous / unsatisfiable assumptions | No. No kani::cover, no vacuity marker. Every Assumed edge is either a no-op or wholly vacuum-inducing (K25-05) |
No | Yes — a vacuous Kani run exits 0 |
| Kani unavailable | No. Generation never probes for Kani, yet emits --backend cargo-kani --backend-version 0.67.0 --backend-executable-sha256 <caller hex> (K25-06) |
No | Yes |
| Unsupported construct (generation refused) | Yes, and well — KaniDiagnostic { code, terminal_state, generation_code, path }, no partial bundle |
Yes — typed code + typed terminal state, machine-readable | No |
| Dependency missing / failed | Yes — readiness: "incomplete" |
Yes in the graph; no consumer acts on it (K25-03) | Not directly, but unenforced |
The last two rows are where this PR is genuinely strong. The first six are the gap.
Issue #2 acceptance
| Deliverable / criterion | Status | Deciding line |
|---|---|---|
| Generate requires, ensures, proof harnesses from the same clauses as executable oracles | Met | src/kani.rs:280-298 reuses generate_boolean_oracle output verbatim; tests/kani_generation.rs:504-573 asserts byte-containment of the executable oracle in the Kani source across all five Boolean operators |
| Emit framing, binding, contract portions distinctly | Partial | src/kani.rs:355-382 emits BEGIN/END framing|binding|contract|proof harness. The framing block is three comment lines whose values have no read site (K25-13) |
| Record every stubbed or assumed edge in a proof dependency graph | Met | src/kani.rs:730-748 + the bijection assertion at tests/kani_generation.rs:386-394 (matches(source_site).count() == 1) — a genuine, load-bearing check |
| Isolate unstable Kani syntax behind a backend/version adapter | Met | KANI_ADAPTER_PROFILE (:25), exact-version gate (:522-528), option vector confined to adapter_options (:771) |
| AC-1 A proof cannot be counted complete while a required dependency is missing or failed | Not met | src/kani.rs:750-769 computes it, but the state is caller-asserted with no binding (K25-03), the precedence that enforces it is untested (K25-04), and no consumer reads readiness at all |
| AC-2 Generated Kani and executable-oracle semantics agree on the shared bounded corpus | Met | tests/kani_generation.rs:504-573. Agreement by construction (identical bytes) is the strongest available form |
| AC-3 Unsupported constructs are explicit diagnostics | Partial | Structured, typed, machine-readable (KaniDiagnostic, :183-196) — genuinely good. But three claimed rejection classes have no fixture (K25-09) and three error codes are unreachable (K25-10) |
| AC-4 Kani toolchain/version/options captured in evidence | Partial | Version, adapter profile, options, unwind, solver all land in the graph and argv. backend_executable_sha256 is shape-checked only and binds to nothing real (K25-06) |
| Workflow gate: spec + matrix updated, review complete, plan delta, gap analysis, retained evidence | Partial | FR-003/TC-003/TC-005/TC-007 pre-existed; interface-001, test-matrix, suites.md, MP-001, plan tasks all updated. planning/REV-008/REV-009 filed but REV-008 collides (K25-08). Retained evidence: SUITE-008 feeds no evidence store (K25-20) |
PR-body claims checked
| Claim | Result |
|---|---|
| Generates Kani 0.67.0 contracts/harnesses from the validated Boolean semantics used by executable oracles | Verified — src/kani.rs:280-298, tests/kani_generation.rs:504-573 |
Emits distinct contract, binding, framing, harness, dependency-graph and shared ProofAttestationV1 artifacts |
Verified, with the framing caveat in K25-13 |
| Derives ready/conditional/incomplete from the complete sorted dependency census | Partly contradicted — sorting verified (kani.rs:746, order-independence asserted at tests/kani_generation.rs:377-381, genuinely good). "Complete" is unenforced: &[] yields ready (K25-15) and passed is unverified (K25-03) |
| Records proof execution as not run during generation | Verified in the graph; contradicted in the attestations. Traced to all five write sites (kani.rs:235, :418, :469; schema :36; test :279, :304). In the graph it is a const-pinned field. In the two attestation bodies it is argv text beside result: passed (K25-01) |
| Rejects unsupported syntax, invalid dependency/path combinations, duplicate identities, invalid attestations, non-Boolean roots "with structured diagnostics" | Diagnostics: verified structured — typed code, typed terminal_state, stable path, prose confined to message which is explicitly not machine identity (kani.rs:195). Coverage: partly contradicted — 3 of 6 classes untested (K25-09) |
| Binds tool/version/options, assumptions, source identity, graph identity and artifact digests | Mixed. Genuinely bound: the rust artifact digest reaches the attestation transitively (rust.sha256 → graph.sourceArtifactSha256 → graph.sha256 → request_identity → input_digest → attestation_id, kani.rs:419-445) — a correct chain, and options has a real read site (passed to cargo kani at tests/kani_generation.rs:616). Not bound: backend_executable_sha256 (K25-06), dependency state (K25-03), configuration_digest (K25-14) |
| 33 Rust tests, actual cargo-kani 0.67.0 execution, Rust 1.75, clippy/fmt/rustdoc, 9/9 conformance rows, 14 scenarios / 6 controls / 8 probes, 56/56 Quire documents | Unverifiable read-only. Two structural notes: (a) the conformance producer does not import generate_kani_bundle — examples/generation_conformance.rs:36-41 — so "9/9 rows" is unchanged from main and covers zero Kani cases; (b) the assurance-chain green is compatible with K25-02's sealed false statement, so it is not evidence against it |
| "Honest limitations": strict coverage red, no rows claimed | Verified. Every FR-003 and TC-003/005/007 row is still 🚧 Planned (spec/test-matrix.md:17-20, :73-77). No row status was promoted anywhere in the diff. This is accurately stated |
What is genuinely right
Several things here are above the program's average and belong on the record so they are not lost in a rework.
- The
source_sitebijection is a real check.assert_eq!(bundle.rust.contents.matches(source_site).count(), 1)(tests/kani_generation.rs:391) ties every graph edge to exactly one marker in the generated source. Deleting an emission or a graph entry fails it. This is what a binding assertion should look like. - The proof-graph schema mutation probe is correct.
tests/kani_generation.rs:396-401laundersdependencies[0].stateto"passed"and asserts the validator rejects it. TheoneOfwas checked by hand:kindisconst-distinct across the three branches, so at most one can match, and the laundered instance matches zero. The schema is load-bearing and the probe proves it. - Order-independence is asserted, not assumed.
tests/kani_generation.rs:377-381regenerates with a reversed census and asserts bundle equality. That is the right way to pin determinism. - Semantic parity by construction. Embedding the exact oracle bytes rather than re-interpreting the predicate is the correct answer to FND-501, and it makes AC-2 true by construction rather than by sampling.
syn::parse_fileon the generated source (src/kani.rs:400) plussyn::parse_str::<syn::Path>on every caller-supplied path (:631) is a sound injection defense. Whatsyn::Pathadmits was enumerated — turbofish, qualified segments — and nothing escapes an argument position or a comment.- Diagnostics are properly typed.
code+terminal_state+ optional preservedgeneration_code+ stablepath, withmessageexplicitly documented as not machine identity. This is the shape the lens asks for, and this repo already had it right for oracles. tests/common/mod.rs's no-skip policy is honoured. Missing quoin and missing cargo-kani both panic with an explanation. The Kani tests seal through the real Quoin CLI rather than a local copy of the schema.- No matrix row was promoted. The temptation to move an FR-003 row to ✅ on the strength of a local green was available and was not taken, and
MP-001/suites.mdexplain why in the prose. That restraint is the right instinct and it is what makes the K25-02 finding a fixable oversight rather than a pattern. - The
oracle.rsrefactor is non-regressive. Every field of the newGeneratedAttestationSpecwas checked against the values the old code passed; existing slices emit identical bytes.
Make execution-control class — carried note only
This PR touches neither Makefile nor tests/shared_assurance.rs, so nothing here changes the guard. Carrying the corrected figure: quire-contract-codegen holds the strongest guard in the program at 7 of 18 spellings (Rust directive scan at tests/shared_assurance.rs covering global SHELL under five operators, override/export prefixes, global .IGNORE/.SILENT/.ONESHELL/.SHELLFLAGS, recipe - prefixes, and any include/-include/sinclude). Not covered: duplicate target rules, target-scoped/pattern-scoped/static-pattern SHELL and .SHELLFLAGS, $(eval …), define … endef, backslash continuation, computed names, !=, +=, .DEFAULT, MAKE :=. tl-parse and tl-mltl now have no guard. Prior evidence (execution, tl-syntax): .SHELLFLAGS := -c true made make ci exit 0 in ~0.1s with every command printed and none executed. Tracked as #14.
Merge signal
Not mergeable at 8ccc8e63cbd59158510bd6720854b625e9e34643. The same account authors and reviews this repository, so a GitHub APPROVE is unavailable; this comment is the merge signal and it is withheld.
Note on merge order with PR #26: both branch from 0f4df41 and edit seven of the same files, including two paragraphs whose contents directly contradict each other (spec/test-matrix.md and plan/.../Task-006-parity.md on whether atomic publication exists). #26's review recommends landing #26 first and rebasing this branch; whichever order is chosen, the rebased head must be re-reviewed for those prose hunks specifically. K25-08's REV-008 collision with PR #23 must be resolved before this lands regardless.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WDww4TaMhjT6b7U7rzsDPR # Conflicts: # plan/PLAN-001-codegen-v01/plan.md # plan/PLAN-001-codegen-v01/tasks/Task-005-backends.md # plan/PLAN-001-codegen-v01/tasks/Task-006-parity.md # spec/evidence/suites.md # spec/test-matrix.md # src/lib.rs # src/oracle.rs
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WDww4TaMhjT6b7U7rzsDPR # Conflicts: # plan/PLAN-001-codegen-v01/tasks/Task-005-backends.md # spec/interface/interface-001-codegen-api.md
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WDww4TaMhjT6b7U7rzsDPR # Conflicts: # Cargo.lock # Cargo.toml # plan/PLAN-001-codegen-v01/plan.md # plan/PLAN-001-codegen-v01/tasks/Task-005-backends.md # plan/PLAN-001-codegen-v01/tasks/Task-006-parity.md # spec/assurance/MP-001-codegen-measurements.md # spec/evidence/suites.md # spec/functional/FR-001-deterministic-oracles.md # spec/functional/FR-004-vacuity-evidence.md # spec/interface/interface-001-codegen-api.md # spec/test-matrix.md # spec/test/TC-006-vacuity.md # src/harness.rs # src/lib.rs # src/oracle.rs # src/publication.rs # src/vacuity.rs
1 participant
Scope
This is the isolated Agent A Kani slice based directly on current main. It contains none of Agent B's harness or vacuity commits.
Exact head and local verification
Head:
8ccc8e63cbd59158510bd6720854b625e9e34643Full local
make cipasses at this exact SHA:Honest limitations
Strict Quire coverage remains red because semantic rows await independent review and unrelated Inspection/Analysis rows lack a released shared discharge artifact. This PR does not claim those rows. Hosted CI remains manual-dispatch only and was not dispatched.
Refs #2.