[Codegen#68] Structural under-coverage sweep: what every requirement promises that none of its acceptance criteria can falsify #68

quire coverage can only check the acceptance criteria a requirement chooses to write. A requirement can report 100% backed while half its Outputs section has no criterion at all. This is a full sweep of every requirement document's Behavior, Outputs and Inputs against its own Acceptance Criteria table, at the tree b9b632a plus the codegen#55/#56/#57 remediation.

Line numbers are as read; the three requirements edited in that pass (FR-008, FR-015, FR-017) are as edited.

Cross-cutting patterns, worst first

1. Terminal-state and error-code vocabularies are the largest systematic gap. backend-unavailable, io-failed and inconclusive (interface-001:77, 82-84); unchanged/published/unknown (FR-005:34-35); the ten FR-003 Kani refusal codes (interface-001:160); FR-013's NameCollision to UnsupportedClause path (FR-013:62-64); and the unsupported terminal state on UnsupportedClauseKind, UnsupportedRelation, EmptyPopulation and UnsupportedCampaignConstraint — every one named in prose and asserted by no criterion anywhere.
2. Per-artifact attestation cardinality is stated in FR-001, FR-003, FR-013 and interface-001 and asserted by no criterion in any of them.
3. Architectural negatives are consistently promised in Behavior and consistently absent from criteria: "no private wire structures", "does not implement a coverage engine", "shall not use adapt_to_proptest", "no generic runner". FR-006-AC-6/AC-7 and FR-008-CON-1/CON-2 are the only counterexamples.
4. Five criteria are effectively unfalsifiable: FR-002-AC-3, FR-005-AC-3, FR-013-AC-5, NFR-002-AC-4, NFR-002-AC-5. Two are disjunctive escape hatches: FR-007-AC-4, FR-016-AC-4. One cites a verification that does not exist: FR-004-AC-9 ("Test (TC-006; proposed next slice)").

Per requirement

StR-001 — "without hiding unsupported semantics, vacuity, rejection, assumptions, or tool identity" (:16-17): VC-1 covers identity only, VC-2 requirement identity and corpus agreement; rejection and assumptions reach no StR observable (FR-002-AC-1 and FR-003-AC-1/AC-4 cover them downstream). "coverage artifacts" (:15) omitted from VC-2 entirely. VC-1's "complete … identities" has no enumeration in this document. Both VCs are Demonstration-only, so the requirement carries no testable criterion of its own.

FR-001 — "shall not emit a scalar-valued oracle" (:45), no criterion. Rejection of every numeric arithmetic and negation node (:48-51), no FR-001 criterion. Probe columns one-based with exclusive end (:55), no criterion anywhere. "Dropped or duplicate regions cannot redefine that count" (:56-57), no criterion. Attestation-context minimality (:58-60), no criterion. Source revision, dirty state and lowering-implementation digest (:61), no criterion names the last two. The 1,048,576-byte threshold (:62), no criterion states it. Filename components ≤ 255 bytes (:63-64), no criterion. The four architectural negatives at :69-71, no criterion and no inspection item. "not a fabricated executable CLI invocation" (:82-83), no criterion. Artifact-count preflight and incremental byte enforcement (:84-86), no criterion. "Publication is a separate explicit call" (:86), no criterion. The package API versus the low-level single-clause API (:22-25), no criterion distinguishes them. Customer type bindings (:25), no criterion exercises them. Per-artifact attestation cardinality (:31-32), no criterion. FR-001-AC-4 bundles four distinct claims (construct, obligation, name collision, bounded resource) under one verification, so a pass on one masks the others.

FR-002 — pre-state snapshot before invocation and post-state check after (:29-30), no criterion, here or anywhere (FR-011:36-37 puts the subject harness out of its slice). Generated harnesses owning the four-step ordering (:33-35), no criterion. The rejection-rate numerator and denominator (:31-32) have no owner at all: FR-011-AC-4 covers the bound-strategy summary and FR-011:97-98 leaves the harness summary unchanged. Structured diagnostic for unsupported constraint forms (:36), no criterion. "shall not silently fall back to filtering" (:37), reached only by the unfalsifiable AC-3. Zero rejected floor declaring a total precondition (:40-41), no criterion. Policy over a report carrying preexisting counts (:46-47), no criterion. Determinism, attestation and no-partial-bundle for harness and strategy (:54-55), no criterion. StatePinned and NoEvent strategies (:23-24) are mentioned in no criterion of any requirement, and interface-001:143 places them out of the bound slice, so they are entirely unverified. Execution points (:20), no criterion varies one.

FR-003 — overflow policy and per-binding source span in the graph (:41-43), no criterion. Multi-value ordered tuple result binding (:46-47), no criterion (AC-6 covers one value, AC-7 none). "SHALL NOT accept a caller override" (:50-51): AC-5's "without clamping or approximation" would not fail on an honoured override. The ensures-side domain requirement on a bounded-integer post-state result (:52-53) has no criterion; AC-5 is scoped to subject arguments. "Model-domain assumptions SHALL appear separately … rather than as completed dependency proofs" (:57-58): AC-4 lists both artefacts and never asserts the separation, so a graph recording a model-domain assumption as a completed edge passes. Post-state data in a precondition (:67) is absent from AC-3's refusal list. The framing region (:69-70) is inspected by no criterion. The four separately inspectable regions (:30-31), no criterion. Schema validation of the proof graph (:32), no criterion — contrast FR-013-AC-3, which does assert it for the attestation. Per-artifact attestation cardinality (:35-36), no criterion. No FR-003 criterion names any of the ten refusal codes, and none asserts that a wrong Kani version yields backend-unavailable.

FR-004 — "without implementing instrumentation, profile merging, or a coverage engine" (:40-41), no criterion and no inspection item. Partial intersection and unterminated final span (:56-57), no criterion (AC-5 names summary-only). inconsistent is a fifth outcome beside AC-3's four (:57) and no criterion asserts it is produced. The count-contradiction rule (:58-62), no criterion. The two prohibited combinations at :64-66, no criterion. Parent traversal, backslash aliases and source-root stripping (:71-72), no criterion (AC-5 names only path-ambiguous). Of the retained identities at :73-75, toolchain/target/optimization profile, LLVM export format version, generated-report schema identity and exact requirement revision are covered by no criterion. The qualified producer profile (:76-78) pins cargo-llvm-cov 0.9.0 and export 3.0.1 and no criterion pins either, so a build accepting 0.8.0 passes. The cargo_llvm_cov.version/manifest_path cross-check (:79-80), no criterion. "shall not manufacture" an exception owner (:84-85), no criterion. The 16 MiB bound, not_emitted and the null-versus-zero distinction (:103-111), no criterion.

FR-005 — the whole of :33-36 is uncovered: noncanonical path rejection before mutation, distinguishing missing ownership inputs from I/O inspection failures, and reporting unchanged/published/unknown. AC-1 covers only "no partial published bundle". "The CLI shall never edit developer-owned source regions" (:32): AC-1 covers the failed-generation case only. "shall cite completed conformance evidence without closing the human claim" (:38), half-covered by NFR-002-AC-4. Backend selection (:25), no criterion varies it. The diagnostic's content and terminal state (:28), no criterion. Every FR-005 criterion is library-level while interface-001:60-64 marks cli_generate unimplemented, so the requirement's title obligation has no falsifiable criterion. AC-3 is a verbatim restatement of behavior :37 with no named register or format.

FR-006 — "Exactly one Make target shall run producers" (:44), no criterion. "Every consumer of a producer result shall refuse to create that result" (:45) — the stated core of the design — no criterion. Naming the target that makes an absent result (:46), no criterion. Unreadable result as environment error (:48), no criterion. Declared command equals executed command (:49), no criterion. Unobserved tool version not defaulted (:50-51), no criterion. The internal-mirror prohibition (:52-53), no criterion; AC-1 covers only the incompatible-version half. Manual-dispatch-only CI (:54), no criterion. AC-6's census omits identity framework, retention store and audit store from :23-24's list. Of the codegen.generation-conformance/v1 fields (:35-38), no criterion constrains any of the four contents nor the check-count floor. Row-per-upstream cardinality (:39), no criterion. The MSRV message stream (:40), no criterion. Per-obligation attestation cardinality and byte provenance (:41-42), no criterion. Bookkeeping: criteria run 1,2,3,5,6,7 — AC-4 is withdrawn and explained at :74-83, but the gap is silent in the table.

FR-007 — the requirement's central claim has no criterion: "compare native runtime, executable oracle, generated strategy, and Kani outcomes using their exact typed classifications" (:73-75). AC-2 covers artifact production, AC-4 only counterexample replay; FR-005-AC-4 is far coarser. The seven retained identities at :57-62 are enumerated by no criterion. The object-reference failure modes (:66-69) and collection failure modes (:69-72), including their no-graph-harness and no-strategy-assumption consequences, have no criterion. "without approximating it through another semantic family" (:72-74), no criterion. Capability disposition (:31-32), no criterion. FR-007-CON-3's Validation says "Test" and names no test case, and no criterion asserts it. AC-4 is disjunctive: an implementation that always returns "unavailable" satisfies it. AC-5's verification is "Inspection (TC-023)" — an inspection criterion pointing at a test case.

FR-008 — "shall not accept a caller-supplied range" (:72), no criterion. The unsupported terminal state on UnsupportedClauseKind and UnsupportedRelation (:97-98), no criterion. The UnsupportedRelation span locus (:105-106) has no criterion; AC-3 asserts a span only for UnsupportedClause. Span absence for EmptyPopulation and UnsupportedCampaignConstraint (:107-108), no criterion here or in FR-009/FR-010. "every new refusal as a variant of the existing StrategyErrorCode" (:109-110), no criterion. The shared-domain rule (:111-113) is untested at its only failure point: no criterion exercises a clause whose operands carry unequal IntegerTypes. The Input census row (:61-62) is produced by no criterion — AC-1 exercises State only, as does FR-013.

FR-009 — "at most two inclusive intervals intersected with the domain" (:38-39) and the domain-minus-one-point construction (:45-46) are both unfalsifiable: AC-2 constrains the resulting set extensionally, so any correct implementation passes regardless of structure. EmptyPopulation's terminal state (:56), no criterion. "shall not claim that a case satisfies any clause other than the requested one" (:59), no criterion and no defined observable.

FR-010 — coincident literal and domain unrepresentable entries listed separately (:62-63), no criterion. Representability tested only for would-be out-of-domain values, per read (:57-59), no criterion. The three per-entry fields of the unrepresentable array (:32-33), no criterion. UnsupportedCampaignConstraint's terminal state (:64-66), no criterion.

FR-011 — the verdict-construction rule at :63-66 has no criterion at all: not the use of construct_verdict, not the identity fields, not the four serialized execution-point names (initialization, handler, pre, post). An output vocabulary of four values with zero criteria. The invariant observation's clause kind (:60-62), no criterion. The runtime failure detail (:67-69), no criterion. accepted and failed counting (:70-72), no criterion reads either. The identity-mismatch path and "record nothing further" (:73-74), no criterion. "shall not use adapt_to_proptest" (:75-78), no criterion — a runner using it while producing correct counts passes everything. Where the rate accessors appear (:97-98), no criterion. ConformanceMismatch ordering against the ceiling check and the never-Failed claim (:101-102), no criterion.

FR-012 — AC-1 restates behavior :40-42 as a property of the walk the test performs rather than of the value tree, so a tree that misbehaves on an early complicate is never visited. "minimal" (:31) is defined nowhere and AC-3 pins one fixture, so minimality is not a falsifiable general property.

FR-013 — the "current" observation name for an input declaration (:79-80) has no criterion anywhere; AC-1 exercises "pre" and "post" on a State declaration, as do FR-008-AC-1/AC-2. The NameCollision to UnsupportedClause path (:62-64), no criterion. --backend none (:71), no criterion. Derivation of field identifiers from the oracle's parameter names (:61-62) is not falsified — AC-1 reads through the constants and passes under any self-consistent naming. Per-artifact cardinality and the obligation id (:53-54), no criterion. AC-5 is satisfied by the interface prose existing and cannot go red.

FR-014 — of the claim-map entry at :67-72, semantic type, "the bounds its parameters were checked against" (distinct from bounds), and "either the generated symbol or the typed refusal" are covered by no criterion. The five bound-form member tables (:54-60) are "defined by this generator, not by V2" and no criterion constrains any member count or order. "checks every descriptor parameter … against the node's reachable bounded_domain nodes" (:44-48): AC-10 asserts refusal for one unequal parameter and no criterion establishes coverage over all five families. The caller-supplied Meter (:77-81), no criterion. The scalar tag profile used for lowering (:73-76), no criterion.

FR-015 — after codegen#56 the remaining gaps are two. "One Kani harness per obligation kind and claim" (:37-38): AC-1 covers one contract's four kinds and no criterion covers the per-claim cardinality, so two postconditions of one contract yielding two harnesses is unasserted. The frame kind appears in the Behavior list and in ObligationKind and is unreachable from the merged IR, which TC-025 records as Blocked — correct, but it means AC-1's "four kinds" is verified over three.

FR-016 — the FR-333 method-result envelope (:36-38), no criterion. AC-4 is a disjunctive escape hatch: an implementation collapsing every disagreement into "unavailable" passes. Otherwise the best-covered requirement in the set. Zero implementation, honestly marked.

FR-017 — written in this pass with criteria for each Behavior clause. Two Behavior clauses are deliberately uncovered and named in its Open items: no wall-clock budget (#58) and prose-parsed verdicts (#59).

NFR-001 — "every supported backend and declared platform profile" (:23): neither the criteria, the metric table, nor the Verification section enumerates a single platform, so the criterion cannot be shown unmet. Metric method golden-approval-testing (:34) against AC-1 "Test (TC-001)", and metric method inspection (:36) against AC-3 "Test (TC-002)" — the declared measurement method and the criterion's verification method disagree in both rows. TC-001's randomized input order (:48) has no criterion; AC-1 says only "Identical pinned inputs".

NFR-002 — AC-4 is a verbatim restatement of statement :19 with no defined census, token list or output population; contrast FR-006-AC-7, which defines its census precisely. AC-5 is a claim about the documentation's own honesty and no system behavior can falsify it; its cited verification at :96-98 verifies something narrower. Metric method negative-abuse-testing (:36) against AC-3 "Test (TC-003)". Scope names proof graphs and reports (:23) and no criterion exercises either for the six identity fields. No criterion anywhere validates a generated artifact against its own versioned schema (interface-001:108); FR-013-AC-3 validates the attestation schema only. The Qualification Integrity numbers at :50-77 are asserted by no criterion and no test, so a regression in them is undetectable.

NFR-004 — the metric bounds census size "per admitted clause" (:46) while AC-2 bounds it "for every admitted fixture in TC-019" (:53), so a 21-case census on a clause TC-019 does not contain falsifies nothing. The ResidualExclusion exclusion boundary (:28-29) has no criterion.

interface-001 — the document has no acceptance criteria table at all: 200 lines of YAML contract. Everything below is listed because no other requirement's criteria reach it. backend-unavailable, io-failed and inconclusive (:77, :82-84), produced by no criterion. The four attestation results (:91), none asserted present or absent. The whole of write_bundle_atomic (:49) — ownership marker matching, missing-input versus io_failed, failed rollback reporting unknown and preserving staging, post-commit cleanup reporting published — untouched by FR-005's four criteria. observed_at's frozen source-commit time (:94), no criterion. The UNKNOWN-attested-command-is-not-runnable sentinel (:95), no criterion. The ten not_carried fields (:96-102), no criterion asserts their absence; FR-006-AC-7 covers a different population. archive_build's unavailable-and-dirty marking (:107), no criterion. oracle_slice.schemas (:108), no criterion. The missing-documentation lint on generated crate roots (:124), no criterion. The harness/strategy source limit (:125) and naming scheme (:126), no criterion. kani_slice.subject_boundary (:158), no criterion. compatibility.licensing AGPL-3.0-or-later (:194), no criterion — NFR-002-AC-2 covers emitted Rust SPDX only. compatibility.publication (:195), no criterion. Both open_design_gates prohibitions (:196-199), no criterion.

Also checked and found honest

• spec/test-matrix.md:16 marks FR-001-AC-5 ✅ Covered citing TC-001, TC-006, and :23 marks FR-003-AC-2 ✅ Covered citing TC-007, TC-014. TC-006 and TC-007 are indeed 🚧 Planned in the same file's Test Case Summary — but each row also cites a ✅ Covered test case (TC-001 and TC-014), so neither green row rests on a planned test case alone. The matrix says so explicitly for the second: "the FR-003 portion of TC-007 is already covered by TC-014 without promoting TC-007 overall."
• FR-016 and TC-026 have zero implementation and both rows say 🚧 Planned. Verified and left alone.