Specify LLVM vacuity and rejection analysis

[kreneskyp]

Begins #5 at its required specification-review gate. This PR contains no analyzer implementation and closes no FR-004 matrix row.

The proposed boundary:

• reuses cargo-llvm-cov 0.9.0 as the producer of LLVM coverage JSON export 2.0.1
• adds an explicit oracle_evaluation source-map role so zero consequent counts can distinguish vacuity from code that never ran
• reconstructs active spans from LLVM segment transitions rather than trusting file summaries
• distinguishes unexecuted, vacuous, partially_exercised, and exercised
• consumes the pinned runtime CampaignReport instead of a caller-owned counter lookalike
• retains campaign counts and test outcome independently of coverage classification
• binds exact paths, source-map/export digests, requirement revision, producer/format versions, report schema, and packaged ProofAttestationV1
• rejects malformed, summary-only, ambiguous, traversing, mismatched, or unsupported inputs without a partial bundle

The preimplementation review records FND-2001 through FND-2010 in planning/vacuity-preimplementation-review.md. It explicitly forbids a local coverage engine, evidence store, attestation schema, or verifier.

Local verification at 46285ad:

• Quire specification validation
• JSON schema syntax validation
• make ci

The full local gate passed on Rust 1.75 and the native toolchain, including shared Quoin/Quire assurance. No hosted CI was dispatched and no workflow file changed.

Independent specification review is requested for exact head 46285ad. Implementation remains blocked on that review.

[kreneskyp]

Independent specification review requested for exact head 46285ad. Please review the classification lattice, LLVM segment/path interpretation, runtime/source-map identity boundary, and all-or-nothing packaging before implementation begins. Full local make ci passed; no hosted CI ran.

[kreneskyp]

Specification review — PR #23

PR: #23 "Specify LLVM vacuity and rejection analysis" (draft, closes #5)
Reviewed head: 46285ad5da502f363782a22842d1bbb3c732db4e (branch contract-agent-b/codegen-5-vacuity)
Diffed against: merge base 0f4df413b21dba39ef62aca89ededc707aab7056 (== origin/main; the branch is one commit ahead, no divergence)
Nature: spec-only, with one exception noted below (S23-15). 8 files, +148/−20. No Makefile, no .github/, no src/, no tests/ change. No hosted CI was dispatched for this review; nothing was built, run, or edited.

Verdict: ⛔ Changes requested — 8 high / 9 medium / 3 low.
Draft status is justified. Do not un-draft. The PR asks the right question and the boundary it draws (LLVM is the producer, codegen validates/maps/classifies/packages) is the correct one. But the specification as written can be satisfied in full by an implementation that never fails, never records that it could not measure, and reports exercised for a clause whose consequent never ran. Under the DO-330 lens this is not ready to become an implementation contract.

---

Prior state

One comment on the PR (kreneskyp, 2026-09-02) requesting independent review of the classification lattice, segment/path interpretation, identity boundary and all-or-nothing packaging. No reviews. Nothing pending a reply. This is the first review on the PR, so there is no prior finding-ID scheme in review comments — the FND-2xxx IDs in planning/vacuity-preimplementation-review.md are the author's own self-review, not a reviewer scheme. This review uses S23-nn.

Issue #5 acceptance criteria against the diff:

#5 criterion	Where addressed	Verdict
"An implication whose antecedent is always false is reported as vacuous even when all calls return true"	spec/functional/FR-004-vacuity-evidence.md:60 (AC-1), :34-35	Addressed in text; see S23-02, S23-07
"Unexecuted control flow and vacuous satisfaction remain distinct findings"	FR-004:61 (AC-2), spec/interface/interface-001-codegen-api.md:101-102	Addressed in text; unfalsifiable against the current generator — S23-04
"A report cannot claim exercised coverage without observing the consequent region"	FR-004:62 (AC-3), interface-001:99, :104	Not met. interface-001:99's "intersects" rule permits exactly this — S23-07
"Coverage tool/version and source-map digests are retained"	FR-004:63 (AC-4), :50-51, interface-001:108	Partially. Retained set omits toolchain identity (S23-09) and AC-4 is verified by an unnamed "Inspection" (S23-16)
"Update or author the owning requirements and test matrix, complete review, and produce the plan delta before implementation"	FR-004, TM-001, planning/vacuity-preimplementation-review.md, plan/.../Task-005-backends.md:30-34	Structurally done

---

HIGH

S23-01 — Nothing in the spec makes a vacuous or unexecuted result a failure, anywhere

spec/functional/FR-004-vacuity-evidence.md:30-54; spec/interface/interface-001-codegen-api.md:37-40, :100-104

FR-004 specifies a classifier and a report. It never states that any classification is a failing verdict, and analyze_coverage has no CLI surface — interface-001:41-44 gives cli_generate a "stable exit status" and there is no corresponding coverage operation, so the analysis has no exit code at all. The only success signal is CoverageArtifactBundle vs CoverageDiagnosticSet, and per interface-001:109 the diagnostic set is produced only for malformed inputs, never for adverse findings.

Failure this permits: an implementation that satisfies every FR-004 behaviour bullet literally returns a well-formed CoverageArtifactBundle, with a sealed ProofAttestationV1 whose result is passed (MP-001:94-95 — "A bundle exists only when generation succeeded, so passed is the only honest answer"), for a run in which every analysed clause classified vacuous. spec/assurance/AP-001-codegen-release.md:38 names "vacuous satisfaction presented as exercised" as a material impact scenario; this spec produces the artifact that scenario needs and attaches a green attestation to it.

To close: state normatively which classifications are adverse, and require the analysis to yield a non-success outcome — distinct from invalid-input — when any analysed clause is vacuous, unexecuted, or partially_exercised, unless an explicit, retained, per-clause exception is supplied. Give the operation an exit-code surface, or say explicitly which existing gate consumes the report and fails on it.

S23-02 — The classification lattice is not a partition; the empty consequent set matches two rules at once

spec/interface/interface-001-codegen-api.md:100-104, against spec/functional/FR-004-vacuity-evidence.md:41-42

The lattice is four independent predicates with no stated precedence and no requirement that exactly one holds. For a clause with zero mapped implication_consequent regions and an observed oracle_evaluation:

• vacuous (:102, "no mapped implication consequent is observed") — true, vacuously, over the empty set;
• exercised (:104, "every mapped implication consequent is observed, or the evaluated clause contains no implication") — true, twice over.

FR-004:41-42 resolves this in prose ("vacuity shall not be inferred when there is no implication") and FND-2010 flags it as low, but the implementer's normative artifact is the interface contract, and it is self-contradictory there. There is also no acceptance criterion requiring that each analysed clause carries exactly one classification, that the four values are pairwise distinct in the report, or that partially_exercised is a retained distinct value — partially_exercised is pinned only in TC-006 prose (spec/test/TC-006-vacuity.md:33), never in an AC.

Failure this permits: first-match evaluation labels every implication-free clause vacuous; last-match labels it exercised. Both satisfy interface-001 as written.

To close: make the lattice a total, mutually exclusive function of (oracle_evaluation observed, mapped-consequent count, observed-consequent count) with the implication-free case as an explicit input condition rather than an or-clause; add an AC requiring exactly one classification per analysed clause and that all four values are demonstrated by TC-006.

S23-03 — No population floor, and the population is defined by the artifact it is supposed to guard

spec/interface/interface-001-codegen-api.md:97, :104; schemas/oracle-source-map-v1.schema.json:5-27

interface-001:97 requires "exactly one clause envelope and one oracle_evaluation region per analyzed clause". "Analyzed clause" is defined by the source map that is being analysed. Nothing anywhere requires the analysed clause set to equal the generated clause set, and nothing establishes a floor derived from an independent source (the IR package, the bundle manifest, the generated artifact inventory).

Worse: the schema has no way to declare that a clause is implication-bearing. Roles are a flat enum (:21) over a flat array; there is no per-clause expected-consequent count, and additionalProperties: false (:9) means one cannot be added without a schema change.

Failure this permits, concretely: a defect in the source-map emitter that drops implication_consequent regions turns every at-risk clause into "a clause with no implication consequents", which interface-001:104 classifies exercised. The population that would catch the bug is derived from the artifact the bug corrupted. This is the empty-set vacuity pattern this program has now hit in four-plus repos, and here it lands on the one analysis whose entire purpose is to detect vacuity. MP-001:46-47 already states the doctrine for the generation corpus — "a corpus can go green by getting smaller, and the floor is what stops that" — and the coverage slice declares no floor.

To close: require the source map to declare, per clause, whether the clause is implication-bearing and how many consequent regions it must carry, with that count derived from the IR/lowering plan rather than from the map; require the analyser to reject a source map whose clause set does not exactly cover the generated artifact inventory it is analysed against; add a census row (analysed clauses, implication-bearing clauses, mapped consequents) and a floor beneath which the run is not a measurement.

S23-04 — The oracle_evaluation region the whole design rests on has no owning requirement, no AC, no matrix row, and nothing emits it

schemas/oracle-source-map-v1.schema.json:21; spec/interface/interface-001-codegen-api.md:97; spec/functional/FR-001-deterministic-oracles.md:31; spec/test-matrix.md:21-22

The PR widens the source-map role enum and then requires (interface-001:97) that exactly one oracle_evaluation region exist per clause. But oracle_evaluation is a generator obligation, and FR-001 — which owns source-map emission — is untouched. FR-001:31 still says only "An implication consequent shall occupy its own coverable source region." No FR-001 acceptance criterion covers it, no TM-001 row binds it, and no test-case names it.

At the reviewed head src/oracle.rs:496-505 emits exactly two roles: one clause region spanning lines 1..EOF of the generated file, and one implication_consequent region per implication. Nothing emits oracle_evaluation. The schema change is permissive — it widens an enum, it does not require the new role — so the generator remains schema-conformant while producing maps the analyser must reject.

Failure this permits: FR-004-AC-2 ("a clause whose oracle-evaluation region was not observed is unexecuted, not vacuous") cannot be violated by any implementation, because no such region exists to be observed. It is a requirement no implementation can fail. Meanwhile, the only region an implementer has today is the whole-file clause region, which is "observed" by any coverage anywhere in the file — including the generated doc-comment header and the early return of a rejected precondition.

There is also no placement or disjointness constraint on oracle_evaluation: nothing forbids it from being the same lines as the consequent, or from spanning the whole function body. See S23-07 for why that matters.

To close: add the emission requirement to FR-001 with its own AC and TM-001 row; require oracle_evaluation in the schema (per-clause cardinality is not expressible in the current flat-array shape — see S23-03); state the placement constraint (dominates the antecedent evaluation, disjoint from every implication_consequent region of the same clause).

S23-05 — Test outcome and producer identity are caller-asserted, unverified, and use a vocabulary that has no "could not run"

spec/functional/FR-004-vacuity-evidence.md:22-24; spec/interface/interface-001-codegen-api.md:38, :106, :107

Two of the operation's inputs are free assertions by the caller:

1. Test outcome. interface-001:106 fixes the vocabulary as [passed, failed, aborted, not_computed]. aborted is not in the shared verification vocabulary — quire-contract-ir spec/program/PGM-01-governance.md:221-224 enumerates failed, skipped, unavailable, not-computed, inconclusive, partial, stale, suspect, vacuous, tampered, unsupported, unreadable. The coverage slice drops skipped, unavailable, inconclusive, partial, stale and suspect and invents a state that is in no vocabulary. AP-001:44 requires that "Unsupported, rejected, discarded, failed, inconclusive, unavailable, and differential states remain visible"; this operation cannot express unavailable.

   Nothing requires the outcome to be derived from producer bytes or to be consistent with the campaign counters. interface-001:107 forbids counts from upgrading the coverage classification but says nothing about the outcome. A caller may supply passed while CampaignCounts::failed() is 47.

   MP-001:94-96 already refuses exactly this pattern for the attestation result — "derived and not supplied… the deprecated envelope's caller-supplied result status permitted a cleanly generated artifact to carry rejected". The coverage slice re-introduces it.

2. Producer identity. interface-001:38 takes "producer identity" as a caller input, and FR-004:52-54 pins cargo-llvm-cov 0.9.0 / export 2.0.1 and rejects everything else "as unsupported". But the check is against the caller's declaration. planning/vacuity-preimplementation-review.md:21-22 explicitly notes that cargo-llvm-cov's export carries "its own root metadata, which separately identifies its own version and manifest path" — and the spec never requires the declared producer identity to be cross-checked against the export's own self-declaration. A caller declares 0.9.0 over bytes from anything.

To close: require the producer name/version to be read from the export's own root metadata and require the caller's declaration to agree with it or fail; replace the outcome vocabulary with the shared twelve (or a stated subset with a stated mapping), including skipped, unavailable and inconclusive; require the test outcome to be derived from the producer's own bytes, and require an outcome of passed with failed > 0 to be a rejected input.

S23-06 — All-or-nothing packaging means a failed or unrunnable analysis retains no record at all

spec/interface/interface-001-codegen-api.md:39, :68, :109; planning/vacuity-preimplementation-review.md:43-44; spec/assurance/MP-001-codegen-measurements.md:94-96

The design is deliberate and mostly right: no partial bundle. But the attestation is bound to the bundle (interface-001:39 — bundle or diagnostic set; FND-2008 — "the packaged ProofAttestationV1 result describes successful report generation"). interface-001:68 gives ProofAttestationV1.results as [passed, failed, unavailable, not_computed]. Under this spec, analyze_coverage can emit only passed: on success a bundle exists and MP-001:94-95 derives passed; on failure no bundle exists, therefore no attestation exists.

Failure this permits: a consumer counting retained attestations for PROOF-codegen-…-coverage sees zero for a run where the export was unreadable, and zero for a run that was never attempted. "The tool could not measure" and "the tool was not invoked" are byte-identical in the retained record. That is precisely the DO-330 condition this program exists to prevent, and CAC-001:47 already requires that "unavailable tools… produce explicit non-success diagnostics".

To close: require an attestation to be emitted for every invocation, with result ∈ {passed, failed, unavailable, not_computed} derived from the analysis outcome, retained alongside the diagnostic set when no bundle is produced. The all-or-nothing rule should govern the report, not the record of the attempt.

S23-07 — "A positive-count span intersects the region" licenses the exact false exercised this PR exists to prevent

spec/interface/interface-001-codegen-api.md:99; schemas/oracle-source-map-v1.schema.json:22-23

Two compounding problems in one sentence.

(a) Intersection, not containment. :99 says a mapped region is observed "when a positive-count, count-bearing, non-gap active span intersects it". LLVM's segment list flattens nested regions, so a correct reconstruction yields one count per point — but the spec does not say innermost, does not say contained within, and does not say what to do when several reconstructed spans overlap the region. An implementation that reconstructs the enclosing function's region (count > 0, spanning the whole body) and asks whether it intersects the consequent will answer yes for a consequent whose own count is zero. That is a false exercised on the single case the whole PR is about.

(b) Line granularity vs column granularity. LLVM segments are (line, column)-addressed. The source map carries only startLine/endLine (schemas/oracle-source-map-v1.schema.json:22-23), integers, with additionalProperties: false at :9 so columns cannot be added without a schema change. Any consequent sharing a source line with executed code — if a { b } on one line, a chained expression, a closing brace shared with a covered parent region — is indistinguishable at the granularity the map records. Nothing in the spec requires the generator to render consequents on lines exclusive of any other coverage region, and nothing states that the mapping is sound only under that condition.

Failure this permits: FR-004-AC-3 and issue #5's third acceptance criterion — "a report cannot claim exercised coverage without observing the consequent region" — are both satisfiable by an implementation that never observes the consequent region at all.

To close: state the segment-reconstruction rule normatively (the count at a point is the count of the last segment at or before it; a region is observed iff the count at its start point is positive and no zero-count segment opens strictly inside it); either add column fields to the source map, or add an explicit generator requirement that every implication_consequent and oracle_evaluation region occupies whole lines shared with no other mapped region, plus a TC-006 fixture in which the enclosing function has positive count and the consequent has zero.

S23-08 — Negative fixtures are not required to discriminate the validator they name

spec/test/TC-006-vacuity.md:24-28; spec/assurance/MP-001-codegen-measurements.md:64-72, against :86-92

TC-006 requires the rejection fixtures to be mutated "independently" across nine input classes, and MP-001's new block (:70-72) lists six mutation controls. Neither requires that a fixture for validator N be valid to every other validator, nor that the fixture stop rejecting when validator N alone is removed. Nor does the spec require the diagnostic set to be complete — FR-004:45-47 says only "shall fail without a partial report", singular, and interface-001:109 says "produce stable diagnostics" without requiring every applicable diagnostic. With validation order unspecified, a first-wins implementation is conformant.

Failure this permits: a nine-fixture rejection suite in which all nine die at the export-version check, every one asserting only "no bundle was returned". Deleting the path-traversal check, the digest check and the identity check leaves the suite green. Quoin's evidence schema cannot express which validator a fixture discriminates, so this is only pinnable in the spec text — and it isn't.

What makes this sharp rather than pedantic: MP-001 already states the rule, verbatim, twenty lines below the new block. MP-001:90-92 — "Each rule is probed on its own against a binding that is valid apart from the one field under test, with a control requiring the fully valid binding to be accepted; a single joint probe over several bad fields shows only that some rule fired." The coverage slice does not adopt it.

To close: require in TC-006 and MP-001 that each negative fixture be valid to every validator other than the one under test, that a positive control over the otherwise-identical valid input be observed to be accepted, and that removing the target validator alone makes the fixture pass. Require the diagnostic set to contain one diagnostic per violated rule, not the first.

---

MEDIUM

S23-09 — Toolchain, optimisation profile and target are neither inputs, checks, nor retained facts

spec/functional/FR-004-vacuity-evidence.md:22-24, :50-51; spec/interface/interface-001-codegen-api.md:108; spec/assurance/MP-001-codegen-measurements.md:64-67

The retained identity set is producer name/version, LLVM export format version, export digest, source-map digest, report schema identity, requirement revision. It omits the rustc/LLVM version, the optimisation and -C instrument-coverage profile, and the target triple — all of which determine the coverage region layout the line-based source map is matched against. llvm-cov export JSON does not carry the rustc version, so this must be a declared input; it is not in FR-004:22-24. The repo pins MSRV 1.75 (MP-001:61) and carries rust-toolchain.toml, so the values exist and are simply not bound.

Permits: a coverage export produced by a different compiler than the one that generated and instrumented the artifact, silently classified. Close: add compiler identity, profile and target triple to the declared inputs, require them to agree with the generation attestation's environment, and add them to the retained identity set.

S23-10 — unsupported and vacuous are used without declaring which vocabulary axis they belong to

spec/functional/FR-004-vacuity-evidence.md:54; spec/interface/interface-001-codegen-api.md:102; against spec/assurance/MP-001-codegen-measurements.md:239-242

FR-004:54 says non-qualified producers "shall fail as unsupported" — but this repo has three live vocabularies: the Interface-001 terminal states (interface-001:54), the shared twelve verification states (PGM-01:221-224), and now the coverage classification lattice. MP-001:239-242 warns about precisely this: "The generation corpus reaches an unsupported Interface-001 terminal state, which is a different vocabulary on a different axis and is not borrowed to fill the gap." MP-001:231-237 further records that this repository withdrew its unsupported demonstration in the shared vocabulary. vacuous has the same problem — it is simultaneously a shared verification state and, now, a coverage classification. Close: name the axis for each term at every use site, and state the mapping (or explicit non-mapping) between the coverage lattice and the shared twelve.

S23-11 — Coverage failures are not mapped onto the Interface-001 terminal states

spec/interface/interface-001-codegen-api.md:53-62, :109

interface-001:55-61 maps each terminal state to a lowering-specific meaning; io-failed is "reserved for atomic publication" and backend-unavailable "reserved for external backends". The coverage slice's nine invalid-input classes at :109 are never mapped onto any of them, and the coverage-specific case of an absent or unreadable export file appears nowhere at all — :109 covers malformed and summary-only, not missing. interface-001:62 ("no non-generated state may be converted into a complete artifact claim") therefore has nothing to bind for coverage. Close: extend implemented_mapping with the coverage cases, including absent/unreadable export and internal analyser failure, and give each a stable diagnostic code.

S23-12 — The revision identity that must "agree" crosses an integer/string boundary with no normalisation rule

schemas/oracle-source-map-v1.schema.json:25; spec/functional/FR-004-vacuity-evidence.md:45-46; spec/interface/interface-001-codegen-api.md:108

FR-004:45-46 requires source-map and runtime campaign requirement/revision identity to be equal. The source map's requirementRevision is {"type": "integer", "minimum": 1}. quire-contract-runtime's ContractIdentity.revision is RevisionId<'a>(&'a str) — src/identity.rs:38-41, :55-61 at origin/main 60749bc, documented as created "without allocation or normalization". The spec supplies no conversion. Permits: an implementation that compares only requirementId and silently drops the revision half of the check — which is FND-2004's whole subject. Close: state the normalisation (or change one side's type) and require TC-006 to fixture a revision-only mismatch that is rejected.

S23-13 — The report schema, the proof obligation, and the shared evidence binding are all named-but-absent

spec/functional/FR-004-vacuity-evidence.md:50-51; spec/interface/interface-001-codegen-api.md:95-109

Three loose ends:

• FR-004:51 and interface-001:108 require the report to retain a "generated-report schema identity", but no report schema document is added and schemas/ contains only generated-rust-oracle-v1 and oracle-source-map-v1. interface-001:79 already records this exact pathology for the harness and strategy slices ("no schema document exists for the identifier they name"). The program rule is that specs create all artifacts as discrete files — this one should ship schemas/coverage-report-v1.schema.json.
• The oracle slice declares PROOF-codegen-generated-rust-oracle / PROOF-codegen-oracle-source-map (interface-001:81) and the harness slice declares two more (:89). The coverage slice declares none, so the ProofAttestationV1 it must emit has no obligation_ids to carry.
• quire-contract-ir spec/program/STD-002-shared-assurance-governance.md:105 declares an accepted shared domain case property-proof-and-vacuity-results — the read site for this report in the shared intake chain. Neither FR-004, interface-001 nor MP-001 names it.

Note in mitigation: spec/evidence/suites.md and MP-001:226-229 correctly and explicitly decline to declare a suite or proof obligation for FR-004 while nothing exists — "a proof obligation whose subject does not exist is the most complete false green available". That honesty is right; the point here is that the identifiers the report must carry still need to be allocated in the spec.

S23-14 — REV-008 collides with an ID already allocated on a pushed branch, and the same file already exists elsewhere under a different ID

planning/vacuity-preimplementation-review.md:2

Scanned across every local and remote ref:

• REV-008 is already held by planning/kani-preimplementation-review.md on refs/remotes/origin/wave2-agent-b-kani-round1 (pushed) and on contract-agent-a/codegen-v01-completion.
• contract-agent-a/codegen-v01-completion already contains planning/vacuity-preimplementation-review.md as REV-010, plus planning/vacuity-gap-analysis.md as REV-011. Two agents have authored the same path for the same issue under two IDs.
• Highest allocation observed across all refs is REV-013.

This is the "scan remote branches before claiming an ID is free" rule: the working tree is not the global max. Close: reallocate to REV-014 or above, and reconcile with Agent A's REV-010 file before either merges — this is a guaranteed content conflict on one path, not just an ID clash.

S23-15 — A code-affecting artifact ships in a PR described as spec-only

schemas/oracle-source-map-v1.schema.json:21; src/oracle.rs:30; tests/shared_assurance.rs:1085-1105

The PR body states "This PR contains no analyzer implementation", which is true, but schemas/oracle-source-map-v1.schema.json is include_bytes!-ed into the crate at src/oracle.rs:30 and its SHA-256 is emitted as the source map's declared schema identity (tests/shared_assurance.rs:1084-1086 states this explicitly). Widening the role enum therefore changes the compiled binary and the schema identity every emitted source map declares — while the $id at :3 still reads oracle-source-map-v1.schema.json. Two documents now share one identity, and any previously sealed attestation binding that identity binds different bytes. Close: either bump to -v2 with an explicit migration note, or state in the spec why an in-place widening is identity-preserving and add the assertion that pins the schema digest to a declared value.

S23-16 — FR-004-AC-4, the only provenance criterion, has no binding

spec/functional/FR-004-vacuity-evidence.md:63; spec/test-matrix.md:22

AC-4 ("Coverage and source-map identities are present in every report") is verified by "Inspection", and TM-001:22 binds it to the literal string Inspection — not to a test case, an inspection procedure, a checklist, or a retained record. It is the one criterion carrying the DO-330 provenance obligation and the one criterion with no executable binding. It also does not require the identities to be correct, only present — a report with a hardcoded producer string satisfies it. Close: move AC-4 to TC-006 with an assertion over the retained report bytes, or name the inspection artifact and its record.

S23-17 — Coverage classification is decoupled from campaign accounting in both directions; nothing forbids exercised with zero cases run

spec/interface/interface-001-codegen-api.md:107, against :91

:107 says the runtime counts "are retained verbatim and never used to upgrade coverage classification" — correct, and FR-004-AC-6 pins it. But independence is stated symmetrically, so the counts are also never used to downgrade. The harness slice has an explicit "accepted-case floor" (interface-001:24, :91 — "requires at least one accepted case"); the coverage slice has none.

quire-contract-runtime src/accounting.rs was read at origin/main 60749bc to check the invariant interface-001:105 claims: record_kind at :43-54 increments accepted for both Passed and FailedPostcondition, and total() at :88-93 deliberately omits failed. The "failed-is-a-subset-of-accepted" claim is accurate — that part of the spec checks out.

Permits: an exercised classification with CampaignCounts::accepted() == 0, i.e. coverage attributable to a doctest, a const-eval, or another requirement's test run, with no case having been evaluated against this requirement at all. Close: require accepted > 0 for exercised or partially_exercised, and add a TC-006 fixture pairing positive coverage with an all-zero CampaignReport.

---

LOW

S23-18 — SpecReview heading omits the # CODE: Title form

planning/vacuity-preimplementation-review.md:10 reads # LLVM vacuity and rejection analysis preimplementation review; the program form is # REV-008: …. Consistent with the local siblings (planning/oracle-preimplementation-review.md:10, planning/harness-preimplementation-review.md:10), so this is repo-wide drift the PR extends rather than introduces — but it is drift.

S23-19 — Two SpecReview homes, two ID schemes, one duplicated ID

The repo keeps SpecReviews in both reviews/ (SR-001…SR-006) and planning/ (REV-001…), and planning/foundation-gap-analysis.md carries id: SR-001, which duplicates reviews/SR-001-shared-assurance-migration-code-review.md on main. Pre-existing; this PR adds to the ambiguous pile. Sibling crates are split too: quire-contract-{ir,runtime} and quire-analyze use top-level reviews/, while tl-syntax/tl-parse/tl-rewrite/tl-mltl use spec/reviews/. Worth one decision across the eight crates.

S23-20 — No usecase artifact, and FR-004 carries no stakeholder link

spec/functional/FR-004-vacuity-evidence.md:5-9 declares depends_on FR-001 and implements interface-001 but no satisfies StR-001. Consistent with FR-002/FR-003/FR-005/FR-006, which chain through FR-001 — only FR-001 links StR-001 directly. There is no spec/usecase/ directory in this repo or in any of the seven sibling crates (checked at each pushed origin/main). Recording as family-wide, not a defect this PR introduces; see FEEDBACK.

---

Silences table

Every condition under which the specified analysis cannot perform its check, what the spec obliges, and whether a passed/success outcome is excluded.

#	Condition	What the spec obliges	Is success excluded?
1	Coverage export never supplied / operation never invoked	FR-004:15 "When … are supplied" — a guard with no else branch	❌ No. The unsupplied case is unspecified; no record is produced
2	Export file absent or unreadable (producer never ran)	Nothing. interface-001:109 covers malformed and summary-only, not missing; io-failed is "reserved for atomic publication" (:60)	❌ No
3	Generated file absent from the export	interface-001:98 "exactly one … filename matching" → reject	✅ Yes
4	oracle_evaluation region absent from the source map	interface-001:97 requires exactly one → missing region → reject	✅ Yes — but nothing emits it (S23-04)
5	Region present, no LLVM segment covers it (optimised away, not instrumented)	Falls through to "not observed" → unexecuted	❌ No. unexecuted has no defined verdict (S23-01), and "could not measure" is reported as "did not run"
6	rustc/LLVM version differs from the artifact's compiler	Nothing — not an input, not checked, not retained	❌ No (S23-09)
7	Optimisation / -C instrument-coverage profile differs	Nothing	❌ No (S23-09)
8	Target triple differs / cross-compiled	Nothing — never mentioned	❌ No (S23-09)
9	cargo-llvm-cov ≠ 0.9.0 or export ≠ 2.0.1, per the caller's declaration	FR-004:54 "fail as unsupported"	✅ Yes — but on which axis is undefined (S23-10)
10	Producer identity is misdeclared by the caller	Nothing — declaration is never checked against the export's own root metadata	❌ No (S23-05)
11	Test did not run / was skipped / was unavailable	Vocabulary is [passed, failed, aborted, not_computed]; no rule binds which applies; skipped/unavailable/inconclusive are not expressible	❌ No (S23-05)
12	Test outcome contradicts the campaign counters (passed with failed > 0)	Nothing — interface-001:107 forbids upgrading classification, not inconsistency	❌ No (S23-05)
13	Campaign recorded zero cases (CampaignReport::new, never used)	Nothing — no accepted-case floor for this slice	❌ No (S23-17)
14	Source map covers only a subset of the generated clauses	Nothing — the analysed population is defined by the source map	❌ No (S23-03)
15	Clause has zero mapped consequents because the emitter dropped them	interface-001:104 classifies it exercised	❌ No — actively misreports (S23-03)
16	Attestation context invalid / digest mismatch / identity mismatch	interface-001:109 → diagnostics, no bundle	⚠️ Partial — the run fails, but no attestation is retained, so the failure and a non-invocation are indistinguishable (S23-06)
17	Analyser fails internally	inconclusive exists (interface-001:59) but is scoped to "internal syntax or serialization control failure" in lowering and is not mapped for coverage	❌ No (S23-11)
18	Any analysed clause classifies vacuous or partially_exercised	Report it. Nothing more	❌ No. The bundle is produced and its attestation derives passed (S23-01)

14 of 18 conditions do not exclude a success outcome. Under DO-330 §6 tool-operational-requirements terms, the specified tool can return "check performed, result acceptable" for a run in which it performed no check.

---

Traceability check

New/changed requirement	Matrix row	Binds to
FR-004:32-33 (consume, don't implement, a coverage engine)	none	Nothing. No AC. Asserted, unverifiable
FR-004:34-35 (vacuous definition)	test-matrix.md:21 → TC-006 via AC-1	TC-006, 🚧 Planned. No implementation, no fixture
FR-004:36-37 (unexecuted definition)	:21 via AC-2	TC-006. Unfalsifiable today — S23-04
FR-004:38-40 (partially_exercised)	:21 via AC-3	AC-3 does not name the value; pinned only in TC-006:33 prose — S23-02
FR-004:41-42 (implication-free clause)	none	No AC. Contradicted by interface-001:104 — S23-02
FR-004:43-44 (counts/outcome independent)	:21 via AC-6	TC-006. One-directional — S23-17
FR-004:45-47 (identity agreement, fail closed)	:21 via AC-5	TC-006. Type mismatch unresolved — S23-12
FR-004:48-49 (path normalisation, no traversal)	:21 via AC-5	TC-006. No staging rule — S23-08
FR-004:50-51 (retained identity set)	:22 → "Inspection"	Nothing. Not a test case, not a named procedure — S23-16
FR-004:52-54 (qualified profile; all else unsupported)	none	No AC. Checked against a caller assertion — S23-05
interface-001:97 (oracle_evaluation per clause)	none	No FR owns it, no AC, no row, nothing emits it — S23-04
interface-001:99 (segment semantics)	none directly	The soundness core of the analysis has no requirement and no AC — S23-07
interface-001:106 (test_outcomes vocabulary)	none	Not reconciled with PGM-01's twelve or with TC-012 — S23-05
interface-001:108 ("report schema identity")	:22 via AC-4	Names a schema document that does not exist — S23-13
MP-001:64-72 (coverage producer + mutation controls)	n/a (measurement policy)	Consistent with suites.md and MP-001:226-229 declining a suite. ✅ Correct
schemas/…:21 (oracle_evaluation role)	none	Widened enum; no producer, no consumer, no assertion — S23-04, S23-15

Six of sixteen new normative statements have no acceptance criterion. Two bind to the literal string Inspection. One binds to a nonexistent schema. Every TC-006-bound row is 🚧 Planned, which is honest and correctly stated at test-matrix.md:47 and MP-001:226-229.

---

What is right

Stating this so the rework is targeted rather than wholesale:

• The boundary is correct and consistently held: LLVM/cargo-llvm-cov produces, codegen validates/maps/classifies/packages, and FR-004:32-33, MP-001:66-68 and the review's Decision (planning/vacuity-preimplementation-review.md:49-53) all forbid a local coverage engine, evidence store, attestation schema or verifier. That is the right refusal.
• Separating producer version from LLVM export-format version (planning/vacuity-preimplementation-review.md:21-25) is a real distinction most specs collapse.
• Refusing to declare an FR-004 suite or proof obligation while nothing exists (spec/evidence/suites.md, MP-001:226-229) is exactly right: "a proof obligation whose subject does not exist is the most complete false green available."
• The failed ⊆ accepted invariant claimed at interface-001:105 is accurate against quire-contract-runtime/src/accounting.rs:43-54, :88-93 at origin/main 60749bc, and consuming the pinned CampaignReport rather than a caller lookalike is the right call.
• No domain= anywhere; internal links relative (FR-004:69); ecosystem refs ix://; no Mermaid; module keys unchanged.

---

Process feedback (recorded to the assurance-feedback log, not blocking)

1. Quoin's evidence schema cannot express which validator a negative fixture discriminates. S23-08 exists only because that fact is unrepresentable in evidence and therefore has to be pinned in prose in every spec, in every repo, forever. This repo has now written the rule twice by hand (MP-001:86-92 for attestation fields) and omitted it once (MP-001:64-72 for coverage). A discriminates: <validator-id> field on a negative evidence row, plus a required control: <row-id> naming the positive case, would make the omission mechanically detectable instead of a review finding.

2. The shared verification vocabulary has no machine-readable definition, so every repo re-types it and drifts. PGM-01's twelve states live as prose at quire-contract-ir/spec/program/PGM-01-governance.md:221-224. interface-001:106 in this PR introduces aborted, which is in no vocabulary, and drops skipped/unavailable/inconclusive, which are the three states the DO-330 posture most depends on. quire validate cannot catch this because there is nothing to validate against. A published enum — a schema or a quire-exported list — that specs can declare conformance to would turn S23-05 into a lint.

3. The TestMatrix structure permits a verification method (Inspection) in the Test Case column, which produces rows that bind to nothing. spec/test-matrix.md:19, 22, 26 all carry the literal string Inspection where a TC identifier belongs. A grep for coverage succeeds; the binding is empty. This is the "a tag that greps fine can still bind to nothing" pattern at the matrix level. Either Inspection should require a named inspection-record artifact ID, or the schema should reject a non-TC value in that column. Related and already tracked: the coverage selector expects Status while the TestMatrix structure requires Coverage Status (spec/test-matrix.md:35-39, upstream spec-artifacts-process#77), which means this matrix is not currently machine-checked at all.

Separately, and lower priority: no repo in this eight-crate family has a spec/usecase/ directory, though the program rule states every spec needs a usecase and a stakeholder. Either the rule does not apply to library crates and should say so, or eight repos are non-conformant and the cookiecutter should emit the artifact.

---

Recommendation

Do not un-draft. The eight highs are all closable in spec text plus one schema decision, and none of them requires implementation work to resolve. Priority order for the rework:

1. S23-01 — give the analysis a verdict. Without it nothing else matters.
2. S23-06 — emit an attestation on failure. unavailable must be reachable.
3. S23-07 — fix the segment/region observation rule and decide the column-granularity question.
4. S23-04 + S23-03 — give oracle_evaluation an owning requirement, and derive the population floor from something other than the source map.
5. S23-02, S23-05, S23-08 — partition the lattice, fix the outcome vocabulary, adopt the staging rule MP-001 already states.
6. S23-14 before anything else touches planning/ — the REV-008 collision and the duplicate planning/vacuity-preimplementation-review.md on Agent A's branch will conflict on merge regardless of this review's outcome.

Re-request review at the new exact head. Nothing was run, edited, or dispatched for this review; every citation above is read from 46285ad5da502f363782a22842d1bbb3c732db4e and from sibling repositories at their pushed origin/main heads (quire-contract-runtime 60749bc, quire-contract-ir 8ce5c2d, quire-analyze 5f37678, tl-syntax 4cb5787, tl-parse 1ba1cef, tl-rewrite e7411a4, tl-mltl 58f858e).

[kreneskyp]

Recovery checkpoint published at a953a203abe08e0e1bff573e0a45d7a11b83ca5f over 46285ad5da502f363782a22842d1bbb3c732db4e.

The bounded slice adds generated entry probes, an independent typed implication census, strict bounded LLVM parsing, and measured exercised/vacuous/partial/unexecuted classification. Missing/gap/partial mappings remain unavailable rather than becoming measured zero. Existing source-size guards remain; probe extraction is linear.

Real generated oracle controls establish LLVM JSON 3.0.1 with cargo-llvm-cov 0.9.0 and stable rustc 1.94.1. The earlier unqualified 2.0.1 assumption is explicitly corrected; unqualified versions remain unsupported. No tools were installed or silently substituted.

Final-head verification: all ten oracle and five primitive tests on stable; native coverage plus five primitives under Rust1.75.0. The preceding implementation commit also passed all fifteen on1.75.0. Clippy all-targets, formatting, spec validation and diff checks passed. Independent review reran seven focused tests including the pinned native coverage fixture and found no blocker in this slice.

FR004 remains planned: IR-owned complete population binding (#50), full package identity in maps, native campaign/run provenance, aggregate schema and consuming coverage gate are not yet implemented. No private binder, obsolete evidence framework, coverage attestation, or human sufficiency decision is introduced. REV014/015 preserve the preimplementation review and gap dispositions. Nonblocking review hardening remains: hoist the repeated root-prefix allocation outside the file loop.