Specify LLVM vacuity and rejection analysis

plan/PLAN-001-codegen-v01/tasks/Task-005-backends.md

@@ -39,9 +39,16 @@ size guard. Correct the accounting unit and add a source-limit conformance case.
 The campaign-outcome producer integration remains a separate completion item; generated-crate
 execution supplies the focused campaign controls in this revision.
 
+Issue #5's reviewed spec is being repaired in a bounded coordinator-authorized slice: generated
+entry probes, a typed-IR implication census, strict LLVM reading, and measured classification
+primitives. Native fixtures use actual generator outputs. Aggregate analysis and coverage
+attestations await IR #50's bound population and a native producer/run-result contract; no private
+binding or counter model is introduced. REV-014 and REV-015 record the repair and residual work.
+
 ## Guards
 
 - Current `main` is the branch base; superseded bespoke-assurance PRs are not revived or restacked.
 - Unsupported state, constraint, or shrinking semantics fail with a structured diagnostic rather
   than falling back to an unreported filter.
-- Kani and vacuity work remain separate slices and do not broaden this issue #3 branch.
+- Kani remains a separate slice and is outside this recovery slice. Vacuity is partial and closes no
+  full FR-004 row.

planning/vacuity-preimplementation-review.md

@@ -0,0 +1,64 @@
+---
+id: REV-014
+title: "LLVM vacuity and rejection analysis preimplementation review"
+type: SpecReview
+analysis: gap-analysis
+scope: "issue #5 per-requirement vacuity and rejection evidence"
+review_set: subset
+---
+
+# LLVM vacuity and rejection analysis preimplementation review
+
+## Summary
+
+FR-004 cannot distinguish vacuity from code that never ran using the current source map alone. It
+marks the whole generated file as a clause and marks implication consequents, but it does not identify
+the executable region proving that the oracle was entered. The proposed slice adds that region and
+consumes LLVM JSON segments plus the accepted runtime campaign report. LLVM/cargo-llvm-cov remains
+the coverage producer; codegen only validates, maps, classifies, and packages the supplied facts.
+
+The external format boundary follows LLVM's documented `llvm-cov export` contract, which exports
+regions, functions, branches, expansions, and summaries in JSON, and cargo-llvm-cov's documented
+root metadata, which separately identifies its own version and manifest path. Tool version and LLVM
+export-format version are therefore retained as different fields. The initial qualified pair is
+cargo-llvm-cov 0.9.0 and LLVM coverage JSON export 3.0.1; other versions fail as unsupported rather
+than inheriting compatibility from a similar-looking tuple layout.
+
+Correction history: the original PR #23 proposed 2.0.1 without a native fixture. Recovery executed
+cargo-llvm-cov 0.9.0 with rustc 1.94.1 and observed export 3.0.1. The strict reader first refused that
+input, exposing the mismatch; the coordinator approved qualifying the measured 3.0.1 profile instead.
+Native tests now explicitly select Rust 1.94.1, separately from library MSRV testing on Rust 1.75.0.
+
+Primary format references:
+
+- [LLVM `llvm-cov export`](https://llvm.org/docs/CommandGuide/llvm-cov.html#export-command)
+- [cargo-llvm-cov JSON metadata](https://github.com/taiki-e/cargo-llvm-cov#additional-json-information)
+
+## Findings
+
+| ID | Severity | Summary | Refs |
+|---|---|---|---|
+| FND-2001 | high | Consequent count zero is ambiguous without proof that the owning oracle evaluation ran. Add exactly one `oracle_evaluation` region per clause; zero evaluation means unexecuted, while positive evaluation plus zero consequent means vacuous. | FR-004-AC-1, FR-004-AC-2 |
+| FND-2002 | high | File summaries and partial intersection can claim coverage without entry. Require one count-bearing, non-gap active span to contain the complete entry-token probe; retain measured zero separately from unavailable observation. | FR-004-AC-3 |
+| FND-2003 | high | Requirement aggregation can hide an unobserved nested or sibling implication. Report `partially_exercised` when only a proper subset of mapped consequents is observed; only complete observation is exercised. | FR-004-AC-3, TC-006 |
+| FND-2004 | high | A source map, runtime report, or coverage file from a different requirement/revision can produce a plausible false report. Recompute the source-map digest, require one identity throughout, and reject missing, duplicate, or ambiguous file/region matches. | FR-004-AC-4, FR-004-AC-5 |
+| FND-2005 | medium | LLVM segment tuples, export type/version, and full-versus-summary shape are an external schema boundary. Reject malformed tuples, unsupported formats, absent segments, and extra candidates rather than defaulting counts to zero. | FR-004-AC-5 |
+| FND-2006 | medium | Absolute and relative filenames can alias after ad hoc suffix matching, and `..` can escape a declared root. Strip one exact caller-declared root, normalize lexically, reject traversal, and require exactly one match. | FR-004-AC-5 |
+| FND-2007 | medium | Rejection, discard, failed-postcondition, and test status are evidence about the campaign, not substitutes for consequent execution. Consume the pinned runtime `CampaignReport` rather than a lookalike and preserve its four counters plus test outcome independently. | FR-004-AC-6 |
+| FND-2008 | high | Serialization success cannot attest coverage success. Bind native executable/run identities and expected IR population, and deny coverage discharge for adverse or unavailable analysis/execution. JSON metadata is only a cross-check, never producer provenance. | FR-004-AC-4, FR-004-AC-8 |
+| FND-2009 | medium | All-or-nothing success must not erase refusal evidence. Retain structured non-success outcomes and available input identities without inventing classifications or a passed coverage attestation. | interface-001 |
+| FND-2010 | low | Clauses without implications can be mislabeled vacuous merely because there is no consequent region. Such clauses are exercised when their evaluation region is observed and unexecuted otherwise; vacuity is inapplicable. | FR-004-AC-1, TC-006 |
+
+## Decision
+
+The original PR #23 review requires repair before aggregate implementation. The coordinator has
+authorized the bounded source-probe/LLVM-primitive slice and unambiguous spec corrections; REV-015
+records its review dispositions and open integration gates. Full analysis waits for IR #50 and
+native-run binding. Reuse source-map artifacts and the runtime's campaign accounting, then consume
+the shared Quoin/Quire chain without creating a local evidence framework. REV-014 replaces the
+colliding REV-008 identifier; it does not claim the unrelated Kani review.
+
+## Verdict
+
+**PARTIAL RECOVERY; INDEPENDENT REVIEW REQUIRED.** TC-006 and FR-004 remain planned until the bound
+contract, load-bearing aggregate negative controls and full integrated gates pass on an exact head.

reviews/SR-008-vacuity-recovery-gap-analysis.md

@@ -0,0 +1,72 @@
+---
+id: REV-015
+title: "Vacuity primitive recovery and remaining binding gaps"
+type: SpecReview
+analysis: gap-analysis
+scope: "PR #23 bounded source probes, LLVM parser and classification recovery"
+review_set: subset
+---
+
+# Vacuity primitive recovery and remaining binding gaps
+
+## Summary
+
+PR #23 at `46285ad5da502f363782a22842d1bbb3c732db4e` was specification-only. The recovery
+reproduces/adjudicates its review rather than treating every proposed fix as implementation authority.
+Only source probes, bounded LLVM reading, measured classification, native fixtures and unambiguous
+spec repairs are implemented. Bound aggregate analysis remains dependent on IR #50 and native
+producer/run-result ownership. Quoin owns retention/integrity; Quire owns static facts; attributed
+human decisions remain outside automatic coverage classification.
+
+The old `f553dca` implementation was inspected but not cherry-picked: it mixed a superseded local
+evidence framework with seven-state classification, suffix path matching, loose tuple shape,
+intersection/max-count inference and unbounded final spans. No old evidence is revived.
+
+## Findings
+
+| ID | Severity | Summary | Refs |
+|---|---|---|---|
+| FND-23001 | high | S23-01: Spec repaired: default deny for adverse/unavailable coverage or execution. Primitive emits no attestation. Aggregate outcome schema and consuming obligation gate remain open. | FR-004-AC-8 |
+| FND-23002 | high | S23-02: Repaired measured partition; implication-free positive entry is exercised, zero entry is unexecuted, unavailable observation has no classification. Native and synthetic controls exercise the distinction. | FR-004-AC-3 |
+| FND-23003 | high | S23-03: Generator independently counts typed implications on the clause envelope; primitive rejects census mismatch. Complete trusted package/clause population awaits IR-owned BoundPackage; public primitive arguments are not an authenticated census. | FR-004-AC-7 |
+| FND-23004 | high | S23-04: FR-001 now owns one function-entry token probe and every consequent entry probe, preserving exact expression line ranges. Actual generated Rust is instrumented in the native test. | FR-001-AC-5 |
+| FND-23005 | high | S23-05: Self-declared export version/manifest are checked but expressly do not authenticate a run. Native command/binary/profile/source/campaign/candidate binding remains open; no primitive claims it. | FR-004-AC-4 |
+| FND-23006 | high | S23-06: Spec requires structured non-success outcomes retaining available identities. Primitive diagnostics exist; aggregate outcome/report producer is not implemented. | FR-004-AC-5 |
+| FND-23007 | high | S23-07: Repaired: one count-bearing non-gap active span must contain the entire entry-token probe. Partial, gap, non-count and unterminated-span controls refuse observation, not invent zero. | FR-004-AC-3 |
+| FND-23008 | high | S23-08: Native generated controls plus independent malformed tuple/version/path/population/span tests are executable. Aggregate tampering/discharge controls remain planned and explicitly listed in TC-006. | TC-006 |
+
+Additional review dispositions: exact u64-to-canonical-decimal runtime revision normalization,
+outcome axes, native toolchain/target/profile and accounting consistency are now specified but await
+aggregate implementation. REV-008 collided with Kani work and is now REV-014. FR-004 gains its
+stakeholder relationship and one matrix row per criterion; these rows remain planned. The live
+source-map schema changes because this slice now implements the producer fields, not spec alone.
+Package identity is still absent from the historical generated source map and must be added when
+joining the public bound population; requirement/revision/clause alone is not cross-package binding.
+
+## Measured profile and implemented controls
+
+The original proposed LLVM format 2.0.1 was refused when the real producer emitted 3.0.1. The qualified
+fixture now explicitly runs cargo-llvm-cov 0.9.0 with Rust 1.94.1 on x86_64-unknown-linux-gnu/test profile.
+The reader accepts exactly that export-format/producer-metadata pair and refuses other versions.
+Library Rust 1.75.0 compatibility is separate from native coverage-tool qualification.
+
+Native fixtures call generated oracles for vacuous, implication-free exercised, sibling partial,
+unexecuted, nested partial and fully exercised cases. Synthetic controls cover exact tuple arity and
+types, coordinate order/zero, source-root boundary and normalized duplicates, traversal/backslash,
+missing segments, unavailable probes, partial overlap, gap/non-count and final-span refusal, census
+mismatch, contradictory entry/consequent observations and the raw 16 MiB size limit. Decoder limits
+also cap files and total segments with independent over-limit controls; no native evidence or full
+assurance receipt is minted by tests. The fixture selects `+stable` only after asserting the exact
+Rust 1.94.1 commit/version and preflighting installed LLVM tools; it does not install missing tools.
+
+## Remaining work and verdict
+
+Implement and independently review the IR-owned complete population join, full artifact/map semantic
+validation and digests, native runtime report binding, run/binary/profile/candidate provenance,
+versioned success/non-success analysis outcomes and the producer/consumer obligation gate. Tests must
+prove removing all clauses, one clause, an implication or evaluator cannot pass, and serialization of
+an adverse/unavailable result cannot discharge coverage. Failures must retain diagnostics rather than
+turn unavailable evaluation into implication-free success. No automatic human sufficiency decision.
+
+**PARTIAL; NOT FULL FR-004 COMPLETION.** No full matrix row, native campaign producer integration,
+shared receipt, independent review, or complete local CI pass is claimed by this document.

schemas/oracle-source-map-v1.schema.json

@@ -18,12 +18,25 @@
     ],
     "properties": {
       "artifactPath": {"type": "string", "minLength": 1},
-      "role": {"enum": ["clause", "implication_consequent"]},
+      "role": {"enum": ["clause", "oracle_evaluation", "implication_consequent"]},
       "startLine": {"type": "integer", "minimum": 1},
       "endLine": {"type": "integer", "minimum": 1},
       "requirementId": {"type": "string", "minLength": 1},
       "requirementRevision": {"type": "integer", "minimum": 1},
-      "clauseId": {"type": "string", "minLength": 1}
-    }
+      "clauseId": {"type": "string", "minLength": 1},
+      "expectedConsequents": {"type": "integer", "minimum": 0},
+      "probe": {
+        "type": "object", "additionalProperties": false,
+        "required": ["line", "startColumn", "endColumn"],
+        "properties": {
+          "line": {"type": "integer", "minimum": 1},
+          "startColumn": {"type": "integer", "minimum": 1},
+          "endColumn": {"type": "integer", "minimum": 2}
+        }
+      }
+    },
+    "if": {"properties": {"role": {"const": "clause"}}},
+    "then": {"required": ["expectedConsequents"], "not": {"required": ["probe"]}},
+    "else": {"required": ["probe"], "not": {"required": ["expectedConsequents"]}}
   }
 }

spec/assurance/MP-001-codegen-measurements.md

@@ -64,6 +64,16 @@ export. Quire exports; it never executes a producer.
 `rustup run 1.75.0 cargo check --locked --all-targets --message-format=json` is the MSRV build, whose
 verdict is read from cargo's own `build-finished` message rather than from its transcript.
 
+TC-006 will add a coverage producer only after FR-004's independent specification review. The
+qualified v0.1 producer is cargo-llvm-cov 0.9.0 invoked with `cargo llvm-cov --json`, whose output is
+LLVM's full JSON export format 2.0.1 with
+per-file segments; the analyzer consumes those retained bytes and never invokes LLVM, Cargo, Quire,
+or Quoin. The producer version and LLVM export-format version are separate facts. A positive
+measurement pairs a tool-produced export with exact source-map and runtime identities; mutation
+controls independently remove the evaluation hit, remove one of several consequent hits, replace the
+export with summary-only output, alter a source path, alter each digest, and mismatch the campaign
+revision. No FR-004 proof obligation or suite is declared until that producer and analyzer exist.
+
 Every generated artifact carries a proof-attestation body, and that body's conformance to the shared
 shape is measured rather than declared. `tests/oracle_generation.rs` fetches
 `proof-attestation-v1.schema.json` from `quoin change-assurance schema` — the bytes the sealing and

spec/functional/FR-001-deterministic-oracles.md

@@ -31,6 +31,11 @@ attestation with complete identity.
 - Generated signatures shall contain exactly the clause dependency set in deterministic order,
   preserving current, pre-state, and post-state observations in caller-facing parameter names.
 - An implication consequent shall occupy its own coverable source region.
+- Each oracle shall carry exactly one evaluation-entry probe on its function-entry line, disjoint
+  from every consequent region. Every consequent shall carry a single-line entry-token probe inside
+  its exact expression region. Probe columns are one-based byte offsets with an exclusive end.
+- The clause envelope shall declare its expected consequent count derived from the typed expression,
+  independent of the emitted region list. Dropped or duplicate regions cannot redefine that count.
 - The generator shall retain every input, schema, tool, backend, configuration, output, and digest identity;
   consuming packages shall supply only the sealed record digest and the candidate revision their
   attestations bind to.
@@ -48,6 +53,7 @@ attestation with complete identity.
 | FR-001-AC-2 | A differential corpus covering every supported operator compiles with only the runtime and matches an independent evaluator. | Test (TC-002) |
 | FR-001-AC-3 | Requirement IDs and revisions appear in symbols, failures, source maps, and attestations. | Test (TC-001) |
 | FR-001-AC-4 | No construct, obligation, name collision, or bounded-resource failure is silently dropped, approximated, or marked complete after a diagnostic. | Test (TC-003) |
+| FR-001-AC-5 | Every oracle map declares the typed-expression consequent census, one disjoint evaluation-entry probe, and an exact entry-token probe for every consequent; generated-oracle LLVM controls distinguish observed entry from zero consequent execution. | Test (TC-001, TC-006) |
 
 ## Dependencies