feat(detection-core): foundation contract package (trace, verdict, coverage, provenance)

.kiro/specs/detection-core/brief.md

@@ -0,0 +1,95 @@
+# Brief: detection-core
+
+## Problem
+
+Detection in this project is specified as a set of per-family, per-arm runners (prover,
+hunter, hook, proof arm). Corrections patch one arm and do not compose: v1→v2 retunes
+transferred 0/17 on untouched cases, and the 2026-10-30 admission run returned NO-GO
+(0/12 pairs, in-family 0/3, 9/12 pilot repositories with zero framework recognition).
+Learned components have nothing constraining them, so DSPy fitted a shape shortcut
+(deletion count separates reversed fixes at 0.90). The root cause: the core security
+object — one deterministic, checkable artifact per change that makes a defect claim
+provable (with witness) and a non-claim bounded (with coverage) — was implicit, never
+specified.
+
+## Current State
+
+- The ordered trace exists for one family: `access-control-prover` implements entry →
+  hops → operation → witnesses → dominance → three-way judgment, with digests and the
+  Req 12 admission workflow (dev pool + untouched admission pool). 13.3's four-arm run
+  proved attribution works around the trace (analyzer_only −246 unguarded).
+- Measured ceilings of the chain: entry recognition (9/12 pilot repos unrecognized),
+  call resolution (11.9% complete), guard dominance coarseness, 120s pre-push budget
+  (whole-repo CPGs do not fit: libpng 446s, 637-file PMPro does not load).
+- `valid-detection-benchmark` provides the measurement instrument; `detection-quality.md`
+  (steering, 2026-10-30) holds standing rules and pre-registered stop conditions.
+
+## Desired Outcome
+
+One specified core object — the security trace — with a contract that every detection arm,
+fact pack, and consumer reuses: given a push (base, head) within a fixed budget, output
+proven defect claims (each with its witness) plus explicit coverage of what was not
+decided, on repositories never seen. No fitted component ever sees pool labels.
+
+## Approach
+
+Specify the trace as the core: scope (change regions, hard budget) → recognize (counted
+entry/operation coverage) → resolve (every call in one completeness bucket) → trace
+(entry → hops → operation → witnesses → dominance → judgment → digests) → verdict (proven
+claim | bounded silence). Models are bounded to residuals: zero-shot judge on the trace,
+hunter proposes trust boundaries, proof arm demonstrates (only BLOCK evidence). Admission
+on an untouched population gates the trace itself.
+
+## Scope
+
+- **In**: trace schema and witness algebra; three-way judgment; budget/scoping contract;
+  coverage accounting (funnel, resolution buckets, named incompleteness reasons); digest
+  and provenance fields; admission-gate contract (Req 12 workflow generalized); the
+  anti-shortcut rule for any fitted component (reversed-pair probes, per-repo holdout,
+  untouched-population admission); re-parenting map of existing specs onto the core.
+- **Out**: new vulnerability families; per-framework fact content (that is fact-pack work,
+  e.g. recognition-coverage table task 7.1 in valid-detection-benchmark); the pre-push
+  transaction itself (pre-push-safety-net consumes the core); engine internals.
+
+## Boundary Candidates
+
+- Core trace object and verdict contract (this spec).
+- Fact packs: per-family recognition/operation/guard facts, admission-gated (extension
+  point, starting with access_control from access-control-prover).
+- Consumers: pre-push-safety-net (push transaction), search-with-proof (BLOCK evidence),
+  hunter-learning-loop (proposal lane only).
+
+## Out of Boundary
+
+- The pre-push hook transaction and rollout policy.
+- New detection families beyond what the trace contract enables.
+- Fitted models of any kind in the core path.
+- Engine/CPG internals (contributor-scan owns those).
+
+## Upstream / Downstream
+
+- **Upstream**: `valid-detection-benchmark` (measurement instrument, dev + admission
+  pools), `access-control-prover` (trace implemented for access_control), steering
+  `detection-quality.md` (standing rules and stop conditions).
+- **Downstream**: `pre-push-safety-net` (M-series milestones), `search-with-proof`,
+  `hunter-learning-loop`, future fact-pack specs per family/ecosystem.
+
+## Existing Spec Touchpoints
+
+- **Extends**: `access-control-prover` — its trace schema, judgment vocabulary and
+  admission workflow become the core contract, generalized across families.
+- **Adjacent**: `pre-push-safety-net`, `search-with-proof`, `hunter-learning-loop`,
+  `valid-detection-benchmark`, `contributor-scan` — consumers/instruments; must not
+  duplicate the trace contract.
+
+## Constraints
+
+- Pool measures, never trains: no fitted prompt/threshold/model on pool labels
+  (detection-quality.md rules 4-5, 13-proposal).
+- Fixed measurement schema: population + freeze digests, judgment vocabulary, rates with
+  n and Wilson 95%, coverage, instrument failures, runtime.
+- Budget is measured, not static: per-change reply time and complexity are recorded, and
+  the budget is derived from the measured distribution per workload class (sample, percentile,
+  hardware disclosed); scoping to the change is part of the core contract.
+- Instrument rule: prove nonzero input reads before interpreting any zero.
+- Plain English in all documents; standard metrics only.

.kiro/specs/detection-core/design.md

@@ -0,0 +1,228 @@
+# Design Document: detection-core
+
+## Overview
+
+**Purpose:** detection-core specifies the single security object every detection arm reuses:
+the canonical trace with its verdict, coverage, budget, provenance, and admission contracts.
+It extracts what `access-control-prover` already implements for one family into a
+family-agnostic contract, so arms, fact packs, and consumers stop maintaining parallel
+runner contracts.
+
+**Users:** spec authors and implementers of detection arms (prover, hunter, push hook,
+proof arm) consume the contract; the maintainer reads admission GO/NO-GO over it.
+
+**Impact:** replaces per-arm envelopes with one contract; existing behavior stays
+byte-identical per consumer during migration (the 2026-10-30 admission suite is the
+regression gate).
+
+### Goals
+- One canonical trace schema and three-way verdict vocabulary shared by all arms (Req 1, 2, 5).
+- Coverage accounting that makes every zero explainable (Req 3); instrument rule enforced at core level.
+- A measured, per-workload-class time budget instead of a static constant (Req 4).
+- Provenance digests on every analysis, with refusal on mismatch (Req 6).
+- A generalized admission gate over untouched populations (Req 7), no fitting on labels with
+  reversed-pair probes (Req 8), models bounded to residuals (Req 9), families as fact packs
+  with scope disclosure (Req 10), consumer contracts (Req 11), fixed measurement schema (Req 12).
+
+### Non-Goals
+- New vulnerability families or their fact content.
+- The pre-push transaction itself (pre-push-safety-net consumes this core).
+- Fitted models anywhere in the core path.
+- Engine/graph internals (contributor-scan).
+
+## Boundary Commitments
+
+### This Spec Owns
+- The canonical trace schema (entry, hops, operation, witnesses, guards, judgment, completeness, digests) and its deterministic serialization.
+- The verdict contract: proven claim (witness attached) vs bounded silence (coverage reason attached); indeterminate never converts to clean.
+- Coverage accounting schema (entry recognition, per-call resolution buckets, unchecked reasons) and the zero-byte instrument refusal.
+- The measured-budget contract: complexity features recorded per change, per-workload-class budget derivation published with sample/percentile/hardware, configurable budget.
+- Provenance stamping (analyzer/fact/acquisition/configuration/population/input digests) and refusal on digest mismatch.
+- The generalized admission contract: consume-only manifest validation, paired scoring, gates, GO/NO-GO report schema, family-scope disclosure.
+- The fact-pack admission contract (reviewed facts, provenance stamping, family tag).
+- The consumer interface for the pre-push transaction and the proof layer.
+
+### Out of Boundary
+- Pre-push hook transaction, rollout policy, capability registry (pre-push-safety-net).
+- Family fact content (fact-pack specs, starting from access-control-prover's rulesets).
+- Hunter/proposer internals and proof-arm internals (they consume the contract).
+- Engine/CPG internals (contributor-scan).
+
+### Allowed Dependencies
+- `valid-detection-benchmark` pools and freeze artifacts (read-only; never label-tuned).
+- Existing prover implementation as the first contract implementation.
+- Steering rules in `detection-quality.md` (no fitting on pool labels; instrument rule; stop conditions).
+
+### Revalidation Triggers
+- Trace schema or verdict vocabulary changes → every arm and consumer re-validates.
+- Admission report schema changes → every admission gate re-runs.
+- Budget derivation method changes → new baseline under Req 12 (not a trend).
+- Fact-pack admission contract changes → all fact packs re-reviewed.
+
+## Architecture
+
+### Existing Architecture Analysis
+Today each arm owns its envelope: `prover_arm.py` (records + summarize), `development_runner.py`
+(bundle + funnel + gates), `arm_regression.py` (arm records), `admission_run.py` (manifest +
+paired scoring). The trace itself (`Trace`, `ProverResult`) exists in the prover. The gap is
+the missing shared contract layer, not missing analysis code.
+
+### Architecture Pattern & Boundary Map
+
+Pattern: **thin core contract package; existing implementations adopt it incrementally**
+(hybrid option C from research.md). The core owns contracts only — no analysis logic.
+
+```mermaid
+flowchart LR
+  subgraph CORE[detection-core contract package]
+    T[trace schema + verdict]
+    C[coverage accounting]
+    B[measured budget]
+    P[provenance digests]
+    A[admission contract]
+    F[fact-pack contract]
+  end
+  subgraph ARMS[arms / fact packs]
+    PR[access-control-prover arm]
+    FP[family fact packs]
+    HU[hunter proposal lane]
+  end
+  subgraph CONSUMERS[consumers]
+    PP[pre-push-safety-net]
+    PR2[search-with-proof]
+    BM[valid-detection-benchmark]
+  end
+  ARMS --> CORE
+  CORE --> CONSUMERS
+  BM -. measures .-> CORE
+```
+
+### Technology Stack
+
+| Layer | Choice | Role | Notes |
+|---|---|---|---|
+| Core contract | Python, frozen dataclasses + canonical JSON | trace/verdict/coverage/budget/admission schemas | mirrors existing Trace.record() conventions |
+| Runners | existing benchmark runners | adopt core contracts incrementally | behavior byte-identical per consumer |
+| Tests | pytest | contract conformance per consumer | admission suite is the regression gate |
+
+## File Structure Plan
+
+### Directory Structure
+```
+src/openultrasast/core/          # NEW: the contract package (no analysis logic)
+├── __init__.py                  # public contract exports
+├── trace.py                     # canonical trace schema, deterministic serialization (Req 1, 2)
+├── verdict.py                   # proven-claim vs bounded-silence contract (Req 5)
+├── coverage.py                  # entry/resolution/unchecked accounting + zero-byte refusal (Req 3)
+├── budget.py                    # measured budget: complexity features, per-class derivation (Req 4)
+├── provenance.py                # digest stamping + mismatch refusal (Req 6)
+├── admission.py                 # manifest validation, paired scoring, gates, GO/NO-GO schema (Req 7, 10)
+├── probes.py                    # reversed-pair / holdout probes for fitted components (Req 8)
+└── factpack.py                  # family fact-pack admission contract (Req 10)
+tests/test_core_trace.py         # conformance tests per contract module
+tests/test_core_admission.py
+tests/test_core_budget.py
+```
+
+### Modified Files
+- `src/openultrasast/hunt/prover.py`, `semantic/obligations/trace.py` — implement/re-export
+  the core trace contract for access_control (Req 1, 2, 5); behavior unchanged.
+- `benchmarks/valid/prover_admission.py`, `admission_scoring.py`, `admission_run.py` — become
+  thin consumers of `core/admission.py` (Req 7); existing refusal order and report schema preserved.
+- `benchmarks/valid/development_runner.py`, `arm_regression.py`, `prover_arm.py` — adopt
+  `core/coverage.py`, `core/budget.py`, `core/provenance.py` (Req 3, 4, 6, 11, 12).
+- `benchmarks/valid/run_manifests.py` — bundle digests feed `core/provenance.py` (Req 6).
+
+## System Flows
+
+```mermaid
+sequenceDiagram
+  participant PP as pre-push transaction
+  participant CORE as detection-core
+  participant ARM as arm (prover/fact pack)
+  participant BM as benchmark pools
+  PP->>CORE: push (base, head), budget class
+  CORE->>CORE: scope change regions (Req 4)
+  CORE->>ARM: analyze scoped regions
+  ARM-->>CORE: trace + coverage + complexity + seconds
+  CORE->>CORE: stamp digests, derive budget check (Req 4, 6)
+  CORE-->>PP: verdict (proven claims with witnesses | bounded silence)
+  BM-->>CORE: dev pool + untouched admission pool
+  CORE->>CORE: admission gate: manifest, pairs, criteria -> GO/NO-GO (Req 7)
+```
+
+## Requirements Traceability
+
+| Req | Summary | Components | Contracts |
+|---|---|---|---|
+| 1 | canonical trace | core/trace.py | Trace schema, deterministic record() |
+| 2 | three-way judgment | core/trace.py, core/verdict.py | Judgment enum; indeterminate-never-clean rule |
+| 3 | coverage accounting | core/coverage.py | funnel + resolution buckets + zero-byte refusal |
+| 4 | measured budget | core/budget.py | complexity features; per-class derivation; gate names derivation |
+| 5 | verdict contract | core/verdict.py | proven claim w/ witness; bounded silence w/ reason |
+| 6 | provenance | core/provenance.py | digest stamping; mismatch refusal |
+| 7 | admission gate | core/admission.py | consume-only manifest; paired scoring; GO/NO-GO |
+| 8 | no fitting on labels | core/probes.py + admission | reversed-pair probes; holdout; no pool-label tuning |
+| 9 | bounded models | core/verdict.py contract | zero-shot judge over trace; BLOCK only via proof |
+| 10 | fact packs | core/factpack.py + admission family tag | reviewed facts, provenance, family-scope in reports |
+| 11 | consumer contract | core/__init__.py | push-consumer and proof-consumer interfaces |
+| 12 | measurement schema | core/admission.py report schema | digests, vocabulary, rates+n+Wilson, coverage, instrument, runtime |
+
+## Components and Interfaces
+
+| Component | Intent | Req | Key contracts |
+|---|---|---|---|
+| core/trace.py | canonical trace + judgment | 1, 2 | `TraceRecord.record() -> canonical JSON` |
+| core/verdict.py | verdict contract | 5, 9 | `Verdict = ProvenClaim(witness, location) | BoundedSilence(reason)` |
+| core/coverage.py | coverage accounting | 3 | `Coverage{entry_recognition, resolution_buckets, unchecked_reasons}` |
+| core/budget.py | measured budget | 4 | `Complexity{regions, calls, changed_bytes}`; `derive_budget(samples, percentile, hardware) -> Budget` |
+| core/provenance.py | digests | 6 | `stamp(bundle, population, change) -> digests`; mismatch raises |
+| core/admission.py | admission gate | 7, 10, 12 | `validate_manifest` (consume-only), `admission_report(...) -> GO/NO-GO` |
+| core/probes.py | anti-shortcut probes | 8 | `reversed_pair_probe(component, fix, reversed_fix)` |
+| core/factpack.py | family packs | 10 | `admit_fact_pack(facts, review) -> stamped pack` |
+
+## Data Models
+
+- **TraceRecord**: entry identity; hops (each with call-target completeness); operation
+  (kind, resource, authority); witnesses (provenance + match relations); guards (effects);
+  completeness reasons; judgment; digests. Canonical JSON, sorted keys (existing convention).
+- **Verdict**: `ProvenClaim{trace_ref, witness, path, line, family}` or
+  `BoundedSilence{path, reason, coverage}`. Never a bare "clean".
+- **Coverage**: entry points + frameworks recognized; per-call exactly one of
+  complete/incomplete/unresolved; unchecked operations with named reasons.
+- **BudgetSample**: change complexity + measured seconds; **Budget**: per-class percentile
+  derivation with n and hardware disclosed; configurable, never a single constant.
+
+## Error Handling
+- Zero-byte or unreadable input → instrument failure; the run is invalid, never clean (Req 3).
+- Digest mismatch → refuse the result (Req 6).
+- Manifest unreviewed / label-exposing / acquisition-changed / spent → ordered refusal, no fallback (Req 7).
+- Budget exceeded → gate failure naming change, elapsed time, and the derivation exceeded (Req 4).
+- Indeterminate evidence → indeterminate verdict with reasons; never converted (Req 2).
+
+## Testing Strategy
+- Unit: trace serialization determinism; verdict rules; coverage bucket exclusivity; budget
+  derivation (fixed samples → fixed budget); digest refusal; manifest refusal order.
+- Contract conformance: prover's existing Trace satisfies core/trace.py; admission suite
+  output byte-identical before/after adoption (regression gate).
+- Probes: reversed-pair probe catches a shape-only component (deletion-count control).
+- Measurement: admission suite re-run on the pilot pool must reproduce the 2026-10-30
+  NO-GO numbers exactly (instrument check).
+
+## Performance & Scalability
+- Budget is measured (Req 4): fit the complexity→reply-time relation on the dev (483) and
+  pilot (264) record sets as measurement only; publish per-class budgets (n, percentile,
+  hardware). The static 120s remains as a provisional default until the first derivation
+  is published; changing it starts a new baseline (Req 12).
+
+## Security Considerations
+- Label isolation: the core never reads pool/admission labels except through the validated
+  admission path; forbidden markers enforced at manifest validation (Req 7, 8).
+- Repository identity masked in shared summaries (existing convention preserved).
+
+## Migration Strategy
+1. Create `core/` contract package mirroring existing shapes (no behavior change).
+2. Prover re-exports core types; conformance tests prove equivalence.
+3. Runners adopt coverage/budget/provenance one at a time; admission suite re-run after each.
+4. Admission modules become thin consumers of core/admission.py; 2026-10-30 NO-GO reproduced.
+5. Fact-pack contract adopted by ruleset loader; family-scope appears in reports.

.kiro/specs/detection-core/requirements.md

@@ -0,0 +1,140 @@
+# Requirements Document
+
+## Project Description (Input)
+
+**Who has the problem:** the maintainer of OpenUltraSAST. Every detection arm built so far
+(prover, hunter, push hook, proof arm) is corrected link by link, and corrections do not
+compose — v1→v2 retunes transferred 0/17 on untouched cases, and the 2026-10-30 admission
+run on the untouched pilot population returned NO-GO (0/12 pairs, in-family 0/3, 9/12
+repositories with zero framework recognition).
+
+**Current situation:** detection is specified as per-family, per-arm runners around an
+implicit core. The ordered trace exists for one family (access-control-prover), learned
+components fit pool shortcuts (deletion count separates reversed fixes at 0.90), and
+misses concentrate in unmeasured links: entry recognition, call resolution (11.9%
+complete), guard dominance, and the 120s pre-push budget.
+
+**What should change:** one specified core object — the security trace — with a contract
+every arm, fact pack, and consumer reuses: given a push (base, head) within a fixed budget,
+output proven defect claims (each with its witness) plus explicit coverage of what was not
+decided, on repositories never seen. Models are bounded to residuals; admission on an
+untouched population gates the trace itself; no fitted component ever sees pool labels.
+
+## Requirements
+
+### Requirement 1: Canonical trace object
+The detection core shall define one canonical trace object per analyzed change as the
+shared security object for all detection arms.
+1. When a change is analyzed, the detection core shall produce a canonical trace carrying
+   entry identity, ordered hops with call-target completeness, operation kind with resource
+   and authority, witnesses with provenance and match relations, guard effects, completeness
+   reasons, a final judgment, and the input digests of the analysis.
+2. The detection core shall serialize every trace deterministically, so that identical
+   inputs produce byte-identical traces.
+
+### Requirement 2: Three-way judgment vocabulary
+The detection core shall judge every analyzed operation as exactly one of unguarded,
+discharged, or indeterminate.
+1. The detection core shall never convert an indeterminate judgment into a clean
+   (discharged or unguarded-free) result.
+2. When evidence for a judgment is incomplete, the detection core shall return
+   indeterminate with the named incompleteness reasons.
+
+### Requirement 3: Coverage accounting
+The detection core shall account for every input it did or did not use, so a zero result is
+never indistinguishable from an unread input.
+1. When a change is analyzed, the detection core shall report entry-recognition coverage,
+   per-call resolution outcomes with exactly one outcome bucket per call, and named
+   reasons for every unchecked operation.
+2. If any input file is read as zero bytes, the detection core shall fail the run as an
+   instrument failure rather than reporting a clean result.
+
+### Requirement 4: Measured budget and change scoping
+The detection core shall derive its time budget from measurement, not from a fixed constant.
+1. When a change is analyzed, the detection core shall measure and record reply time and
+   change complexity (changed regions, call count, changed size) for every change.
+2. The detection core shall derive the per-change budget from the measured distribution
+   (sample count, percentile, reference workload and hardware disclosed) and shall publish
+   that derivation under the fixed measurement schema; the budget shall be configurable per
+   workload class, never a single static constant.
+3. When a change exceeds the measured budget, the detection core shall fail the budget gate
+   naming the change, the elapsed time, and the budget derivation exceeded.
+4. While a push is analyzed, the detection core shall limit analysis to regions affected by
+   the change and shall record the scope it used.
+
+### Requirement 5: Verdict contract
+The detection core shall distinguish proven defect claims from bounded silence.
+1. When the detection core reports a defect, the claim shall carry its witness evidence and
+   an exact location tied to the change.
+2. When the detection core cannot decide a site, it shall report that site as undecided
+   with its coverage reason, and shall never present an undecided site as a clean result.
+
+### Requirement 6: Provenance and digests
+The detection core shall stamp every trace and verdict with the identities of its inputs.
+1. The detection core shall record, for every analysis, the analyzer revision, fact-set
+   digest, acquisition-record digest, configuration digest, population digest, and
+   per-change input digest.
+2. If any recorded digest cannot be re-derived from the named inputs, the detection core
+   shall refuse the result rather than accept it.
+
+### Requirement 7: Admission gate contract
+The detection core shall gate any generalization claim on an untouched population.
+1. When an arm is proposed for pre-push use, the detection core shall require a reviewed
+   manifest naming the frozen analyzer, facts, acquisition, configuration, and an untouched
+   admission population before any admission label is opened.
+2. The detection core shall consume admission manifests without producing, mutating, or
+   re-labeling them, and shall refuse manifests that are unreviewed, label-exposing,
+   acquisition-changed, or spent.
+3. When admission evidence is scored, the detection core shall report paired
+   vulnerable/fixed behavior, ordinary false alarms, and every gate (budget, instrument,
+   pre-registered criteria) as an evidence-backed GO or NO-GO.
+
+### Requirement 8: No fitting on evaluation labels
+The detection core shall not allow any fitted component to train on evaluation labels.
+1. The detection core shall prohibit tuned prompts, thresholds, or fitted models whose
+   training data includes pool or admission labels.
+2. When a fitted component is proposed, the detection core shall require it to pass
+   reversed-pair probes (a fix and its reversed fix shall not be separable by the
+   component's decision features), per-repository holdout, and admission on an untouched
+   population before any claim is made.
+
+### Requirement 9: Bounded role for models
+The detection core shall bound every model to residual questions over the trace.
+1. Where a model judges a trace, the detection core shall present the deterministic trace
+   and require the judgment to be zero-shot over that trace.
+2. The detection core shall not allow a model to propose-and-adjudicate the same claim, and
+   shall reserve blocking verdicts for demonstrated proofs with a differential witness.
+
+### Requirement 10: Family fact packs as the extension point
+The detection core shall admit new vulnerability families only as fact packs over the core
+trace contract.
+1. When a new family is added, the detection core shall require the family's entry,
+   operation, and guard knowledge as reviewed fact packs stamped into the trace's
+   provenance, without changing the trace schema or judgment vocabulary.
+2. The detection core shall report, per arm, the vulnerability families the arm claims, so
+   admission and rollout numbers are never read across families the arm does not cover.
+
+### Requirement 11: Consumer and re-parenting contract
+The detection core shall be the single contract that existing detection specs reuse.
+1. The detection core shall define the interface through which the pre-push transaction
+   consumes traces and verdicts within its deadline.
+2. The detection core shall define the interface through which proof-based blocking evidence
+   attaches to a trace verdict.
+3. When an existing arm's behavior is described, the detection core shall require that
+   description to be expressed over the core contract rather than as a separate runner
+   contract.
+
+### Requirement 12: Fixed measurement schema
+The detection core shall require one fixed measurement schema for every detection number.
+1. When any detection result is reported, the detection core shall require population and
+   freeze digests, judgment vocabulary, every rate with its sample count and uncertainty
+   interval, coverage, instrument failures, and runtime.
+2. When a measurement changes population or judgment vocabulary, the detection core shall
+   treat the result as a new baseline and shall not present it as a trend against the
+   previous baseline.
+
+## Out of Scope
+- The pre-push hook transaction, rollout policy, and capability registry (pre-push-safety-net).
+- New vulnerability families and their fact content (fact-pack specs).
+- Fitted models of any kind in the core path.
+- Engine and graph internals (contributor-scan).

.kiro/specs/detection-core/research.md

@@ -0,0 +1,53 @@
+# Research Log: detection-core
+
+## Gap analysis (2026-10-30)
+
+### Current-state inventory (from codebase exploration)
+
+The security trace already exists for one family (access_control) in the prover:
+`Trace`/`PathRecord`/`ProverResult` (`src/openultrasast/hunt/prover.py`,
+`semantic/obligations/trace.py`), three-way judgment (`PairJudgment`,
+`semantic/obligations/judgment.py`), coverage counters (`Coverage`, `stage_funnel`,
+resolution buckets in `semantic/obligations/resolution.py`), digest stamping
+(`benchmarks/valid/run_manifests.py` `AnalyzerBundle`, `_input_digest`/`_population_digest`
+in `arm_regression.py`), and the admission workflow (`benchmarks/valid/prover_admission.py`,
+`admission_scoring.py`, `admission_run.py`).
+
+### Requirement-to-asset map
+
+| Req | Existing asset | Status |
+|---|---|---|
+| 1 trace object | `Trace`/`ProverResult` in prover | Exists, access_control-only; needs family-agnostic core contract |
+| 2 three-way judgment | `PairJudgment`, `judgment.py` | Exists; promote to core vocabulary |
+| 3 coverage accounting | `Coverage`, `stage_funnel`, resolution buckets | Exists; zero-byte refusal lives only in runners |
+| 4 measured budget | static `BUDGET_SECONDS = 120.0` in runners; per-change `seconds` recorded | **Gap**: budget is a constant; complexity features not recorded; no per-class derivation. Evidence: dev pool 20/483 overruns (max 240s) vs pilot max 7.7s |
+| 5 verdict contract | findings carry witness; indeterminate handling in prover | Exists; needs core-level contract (proven vs bounded silence) |
+| 6 digests/provenance | `AnalyzerBundle`, input/population digests | Exists; stamping rule must become core-level |
+| 7 admission gate | `prover_admission.py`/`admission_scoring.py`/`admission_run.py` | Exists for one arm; needs family-agnostic generalization |
+| 8 no fitting on labels | steering rule only (detection-quality.md) | **Gap**: no reversed-pair probe harness exists |
+| 9 bounded model role | zero-shot judge measured 2026-10-28 (nearly inert, safe) | Policy; core must state the boundary contract |
+| 10 fact packs | `ruleset/obligations/*.toml`, `fact_init.py` | Exists per language; needs family-pack admission + scope tagging |
+| 11 consumer contract | each runner has its own envelope (`prover_arm.run/summarize`, push.admission.defects) | **Gap**: no shared core interface |
+| 12 measurement schema | `score.rate`, `summarize_*` | Partial; vocabulary/digest fields not unified |
+
+### Implementation approach options
+
+- **A. Extend in place**: grow the prover modules into the core. Minimal new files, but
+  bloats family-specific code and keeps the "one arm = one contract" problem.
+- **B. New core module, prover reimplemented**: clean contract, but discards measured,
+  reviewer-approved code (risk of regression in the 34.8%-recall strict lane).
+- **C. Hybrid (recommended)**: new thin core-contract package that the prover's existing
+  types implement, and the runners consume incrementally. Contract extracted, behavior
+  preserved; migration is per-consumer, each step reviewable.
+
+### Effort / risk
+- Effort: M-L (contract extraction across ~6 runner modules plus core package).
+- Risk: Medium — contract extraction touches measured code paths; mitigated by keeping
+  existing behavior byte-identical per consumer during migration and re-running the
+  admission suite as the regression gate.
+
+### Research needed (carried to design)
+- Measured-budget model: which complexity features predict reply time on the two pools
+  (dev 483 changes with seconds; pilot 264). Carry the 13.3/13.4 record sets as the fitting
+  data — measurement only, never training a detector on them.
+- Reversed-pair probe harness for Req 8: fix/reversed-fix pairs exist in the pools.

.kiro/specs/detection-core/spec.json

@@ -0,0 +1,22 @@
+{
+  "feature_name": "detection-core",
+  "created_at": "2026-10-30T13:55:30Z",
+  "updated_at": "2026-10-30T13:55:30Z",
+  "language": "en",
+  "phase": "tasks-generated",
+  "approvals": {
+    "requirements": {
+      "generated": true,
+      "approved": true
+    },
+    "design": {
+      "generated": true,
+      "approved": true
+    },
+    "tasks": {
+      "generated": true,
+      "approved": false
+    }
+  },
+  "ready_for_implementation": false
+}

.kiro/specs/detection-core/tasks.md

@@ -0,0 +1,135 @@
+# Implementation Plan
+
+_Requirement IDs use N.M where N is the requirement number in requirements.md and M is its acceptance criterion._
+
+## Task constraints
+
+- Complexity: McCabe at most 10 per touched function, at most 50 logical lines per function and 400 per new module.
+- The core contract package owns contracts only; no analysis logic moves into it.
+- Every migration step keeps existing behavior byte-identical; the 2026-10-30 admission suite is the regression gate.
+- Instrument rule: prove nonzero input reads before interpreting any zero.
+- Pool measures, never trains: no fitted component reads pool or admission labels.
+
+- [ ] 1. Foundation: core contract package skeleton
+- [x] 1.1 (P) Canonical trace schema in the core package with deterministic serialization
+  - Define the trace record (entry, hops with call-target completeness, operation, witnesses, guards, completeness reasons, judgment, digests) as a frozen, family-agnostic contract.
+  - Done when a fixed trace serializes to byte-identical canonical output on repeat runs and a conformance test pins the schema.
+  - _Requirements: 1.1, 1.2_
+  - _Boundary: core trace contract_
+- [x] 1.2 (P) Three-way verdict vocabulary and verdict contract
+  - Define unguarded/discharged/indeterminate, the proven-claim-with-witness vs bounded-silence verdict, and the rule that indeterminate never converts to clean.
+  - Done when unit tests cover all three judgments, the conversion refusal, and zero-shot-judge-over-trace as the only model role on verdicts.
+  - _Requirements: 2.1, 2.2, 5.1, 5.2, 9.1_
+  - _Boundary: core verdict contract_
+- [x] 1.3 (P) Coverage accounting schema with instrument refusal
+  - Define entry-recognition coverage, exactly-one-bucket-per-call resolution outcomes, named unchecked reasons, and zero-byte/unreadable input as an instrument failure at core level.
+  - Done when a zero-byte read fails the run in a unit test and the bucket exclusivity is pinned.
+  - _Requirements: 3.1, 3.2_
+  - _Boundary: core coverage contract_
+- [x] 1.4 (P) Provenance digest stamping with mismatch refusal
+  - Define the analyzer/fact/acquisition/configuration/population/input digest stamping and refusal when any digest cannot be re-derived.
+  - Done when a mismatched digest is refused in a unit test.
+  - _Requirements: 6.1, 6.2_
+  - _Boundary: core provenance contract_
+
+- [ ] 2. Measured budget replaces the static gate
+- [ ] 2.1 Record per-change complexity and reply time
+  - Extend runner records with complexity features (changed regions, call count, changed bytes) alongside the already-recorded seconds.
+  - Done when dev-pool records carry all complexity fields and seconds.
+  - _Requirements: 4.1, 12.1_
+  - _Boundary: runner records_
+  - _Depends: 1.3_
+- [ ] 2.2 Derive per-workload-class budgets from measurement
+  - Fit complexity to reply time on the dev (483-change) and pilot (264-change) record sets as measurement only; publish per-class budgets with n, percentile, and hardware; make the budget configurable per class, demoting the static constant to provisional default.
+  - Done when the derivation table (class, n, percentile, hardware, budget) is published under the fixed measurement schema and a new-baseline note records the change.
+  - _Requirements: 4.2, 12.1, 12.2_
+  - _Boundary: core budget contract_
+  - _Depends: 2.1_
+- [ ] 2.3 Budget gate and scoping record
+  - Gate failures name the change, elapsed time, and the derivation exceeded; the analyzed scope (change regions) is recorded per run.
+  - Done when an over-budget fixture fails with all three fields and the scope is present in the record.
+  - _Requirements: 4.3, 4.4_
+  - _Boundary: core budget contract_
+  - _Depends: 2.2_
+
+- [ ] 3. Prover arm adopts the core contract
+- [ ] 3.1 Prover trace implements the core schema
+  - Re-export/implement the core trace contract in the access_control arm without behavior change.
+  - Done when a conformance test proves the prover's trace satisfies the core schema field-for-field.
+  - _Requirements: 1.1, 1.2, 2.1_
+  - _Boundary: prover arm_
+  - _Depends: 1.1, 1.2_
+- [ ] 3.2 Prover verdict and coverage over the core contract
+  - Emit verdicts and coverage through the core contracts; existing strict-lane behavior stays byte-identical.
+  - Done when the keyword regression and prover suites pass unchanged after adoption.
+  - _Requirements: 3.1, 5.1, 5.2_
+  - _Boundary: prover arm_
+  - _Depends: 3.1, 1.3_
+
+- [ ] 4. Generalized admission contract
+- [ ] 4.1 (P) Consume-only manifest validation generalized into the core
+  - Move the ordered refusal chain (malformed, producer, unreviewed, label-isolated, label-exposure, acquisition-changed, spent) into the core admission contract; the benchmark validator becomes a thin wrapper.
+  - Done when all refusal branches pass unit tests through the core contract.
+  - _Requirements: 7.1, 7.2_
+  - _Boundary: core admission contract_
+  - _Depends: 1.4_
+- [ ] 4.2 Paired scoring and GO/NO-GO report schema with family scope
+  - Generalize paired vulnerable/fixed scoring, ordinary false alarms, gates, and the report schema into the core; add the claimed-families field.
+  - Done when the report schema includes family scope and every rate carries n and Wilson 95.
+  - _Requirements: 7.3, 10.2, 12.1_
+  - _Boundary: core admission contract_
+  - _Depends: 1.2, 4.1_
+- [ ] 4.3 Admission suite reproduces the 2026-10-30 NO-GO
+  - Re-run the pilot admission through the core contract and reproduce 0/12 pairs, 0.83 flagged/100, 0 instrument failures, NO-GO exactly.
+  - Done when the reproduced report matches the committed 2026-10-30 report field-for-field.
+  - _Requirements: 7.3, 12.1_
+  - _Boundary: admission measurement_
+  - _Depends: 4.2, 3.2_
+
+- [ ] 5. Anti-shortcut probes for any fitted component
+- [ ] 5.1 (P) Reversed-pair probe harness
+  - Build the fix/reversed-fix probe; the deletion-count shape feature must fail it (control test).
+  - Done when the control probe fails a shape-only component and passes a relation-based one.
+  - _Requirements: 8.1, 8.2_
+  - _Boundary: core probes_
+  - _Depends: 1.2_
+- [ ] 5.2 Fitted-component gate
+  - Require per-repository holdout and untouched-population admission before any fitted component makes a claim; BLOCK reserved for demonstrated proofs.
+  - Done when a fitted component without admission evidence is refused by the gate in a test.
+  - _Requirements: 8.2, 9.2_
+  - _Boundary: core probes + admission_
+  - _Depends: 4.1, 5.1_
+
+- [ ] 6. Fact packs and consumer interfaces
+- [ ] 6.1 Fact-pack admission contract
+  - Ruleset loader admits family fact packs only with review evidence and provenance stamping; packs carry their family tag.
+  - Done when an unreviewed pack is refused and a reviewed pack stamps provenance in a test.
+  - _Requirements: 10.1_
+  - _Boundary: fact-pack contract_
+  - _Depends: 1.4_
+- [ ] 6.2 Consumer interfaces for push and proof
+  - Define the interfaces through which the pre-push transaction consumes traces/verdicts within its deadline and the proof layer attaches demonstrated evidence to a verdict; existing arms express behavior over the core contract.
+  - Done when both interfaces are exercised by conformance tests from a mock consumer.
+  - _Requirements: 9.2, 11.1, 11.2, 11.3_
+  - _Boundary: core consumer contracts_
+  - _Depends: 1.2, 3.2_
+- [ ] 6.3 Runners adopt core coverage, budget, provenance incrementally
+  - Migrate development_runner, arm_regression, prover_arm, run_manifests onto the core contracts one at a time, re-running the regression suite after each.
+  - Done when all runners consume the core contracts and the keyword regression passes at the pre-migration count plus new tests.
+  - _Requirements: 3.1, 4.1, 4.3, 6.1, 11.3, 12.1_
+  - _Boundary: benchmark runners_
+  - _Depends: 2.3, 3.2, 6.2_
+
+- [ ] 7. Validation
+- [ ] 7.1 Fixed measurement schema enforced in reports
+  - Every report carries population/freeze digests, judgment vocabulary, rates with n and Wilson 95, coverage, instrument failures, runtime; vocabulary/population change starts a new baseline.
+  - Done when a schema-validation test rejects a report missing any field and accepts the 2026-10-30 report.
+  - _Requirements: 12.1, 12.2_
+  - _Boundary: measurement schema_
+  - _Depends: 4.2, 6.3_
+- [ ] 7.2 End-to-end: one push through core to verdict to admission report
+  - Run one dev-pool push end-to-end: scope, recognize, resolve, trace, verdict, digests, admission report on the dev pool.
+  - Done when the E2E test produces a verdict with witness or bounded silence plus a complete report.
+  - _Requirements: 5.1, 5.2, 7.3, 11.1_
+  - _Boundary: end-to-end integration_
+  - _Depends: 6.3, 7.1_

src/openultrasast/core/__init__.py

@@ -0,0 +1,28 @@
+"""Detection core: the shared security-trace contract package.
+
+Owns contracts only -- no analysis logic. Arms implement the trace contract;
+runners and consumers adopt coverage, budget, provenance, and admission contracts.
+"""
+
+from openultrasast.core.coverage import Coverage, InstrumentFailure, ResolutionOutcome, check_reads
+from openultrasast.core.provenance import ProvenanceMismatch, stamp, verify_stamp
+from openultrasast.core.trace import Guard, Hop, TraceRecord, Witness
+from openultrasast.core.verdict import BoundedSilence, Judgment, ProvenClaim, as_clean
+
+__all__ = [
+    "BoundedSilence",
+    "Coverage",
+    "Guard",
+    "Hop",
+    "InstrumentFailure",
+    "Judgment",
+    "ProvenClaim",
+    "ProvenanceMismatch",
+    "ResolutionOutcome",
+    "TraceRecord",
+    "Witness",
+    "as_clean",
+    "check_reads",
+    "stamp",
+    "verify_stamp",
+]

src/openultrasast/core/coverage.py

@@ -0,0 +1,57 @@
+"""Coverage accounting for the detection core (Req 3).
+
+Every input is accounted for: entry recognition, exactly one resolution bucket per
+call, named reasons for unchecked operations. A zero-byte or unreadable input is an
+instrument failure -- a zero from an unread input is a failed run, never a clean one.
+"""
+
+from __future__ import annotations
+
+import enum
+from collections.abc import Mapping
+from dataclasses import dataclass, field
+
+
+class InstrumentFailure(ValueError):
+    """The run's input was not read; any result from it is invalid."""
+
+
+class ResolutionOutcome(enum.Enum):
+    """Exactly one bucket per call (Req 3.1)."""
+
+    COMPLETE = "complete"
+    INCOMPLETE = "incomplete"
+    UNRESOLVED = "unresolved"
+
+
+@dataclass(frozen=True)
+class Coverage:
+    """Coverage of one analyzed change."""
+
+    entry_points: int
+    frameworks_recognised: dict[str, int] = field(default_factory=dict)
+    calls: int = 0
+    complete: int = 0
+    incomplete: int = 0
+    unresolved: int = 0
+    unchecked_reasons: dict[str, int] = field(default_factory=dict)
+
+    def validate(self) -> None:
+        """Refuse coverage where calls lack exactly one resolution bucket."""
+        buckets = (self.complete, self.incomplete, self.unresolved)
+        if min(buckets) < 0:
+            raise ValueError(f"negative resolution bucket in {buckets}")
+        if sum(buckets) != self.calls:
+            raise ValueError(
+                f"resolution buckets ({self.complete}+{self.incomplete}+{self.unresolved}) must equal the call count ({self.calls})"
+            )
+
+
+def check_reads(reads: Mapping[str, int]) -> None:
+    """Fail the run when any tracked input was read as zero bytes (Req 3.2)."""
+    zero = sorted(path for path, size in reads.items() if size <= 0)
+    if zero:
+        raise InstrumentFailure(f"zero-byte read of tracked input: {', '.join(zero)}")
+
+
+__all__ = ["Coverage", "InstrumentFailure", "ResolutionOutcome", "check_reads"]

src/openultrasast/core/provenance.py

@@ -0,0 +1,62 @@
+"""Provenance digest stamping for the detection core (Req 6).
+
+Every analysis is stamped with the analyzer revision, fact-set, acquisition-record,
+configuration, population, and per-change input digests. A result whose digests
+cannot be re-derived from the named inputs is refused, never accepted.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+from collections.abc import Mapping
+from typing import Any
+
+
+class ProvenanceMismatch(ValueError):
+    """A recorded digest does not match the re-derived input identity."""
+
+
+_DIGEST_FIELDS = (
+    "analyzer_revision",
+    "fact_set_digest",
+    "acquisition_record_digest",
+    "configuration_digest",
+    "population_digest",
+    "input_digest",
+)
+
+
+def _input_digest(change_id: str, population_digest: str) -> str:
+    payload = json.dumps([population_digest, change_id], sort_keys=True, separators=(",", ":"))
+    return hashlib.sha256(payload.encode()).hexdigest()[:12]
+
+
+def stamp(
+    *,
+    analyzer_revision: str,
+    fact_set_digest: str,
+    acquisition_record_digest: str,
+    configuration_digest: str,
+    population_digest: str,
+    change_id: str,
+) -> dict[str, str]:
+    """The provenance stamp of one analysis (Req 6.1)."""
+    return {
+        "analyzer_revision": analyzer_revision,
+        "fact_set_digest": fact_set_digest,
+        "acquisition_record_digest": acquisition_record_digest,
+        "configuration_digest": configuration_digest,
+        "population_digest": population_digest,
+        "input_digest": _input_digest(change_id, population_digest),
+    }
+
+
+def verify_stamp(recorded: Mapping[str, Any], rederived: Mapping[str, Any]) -> None:
+    """Refuse when any digest cannot be re-derived (Req 6.2)."""
+    for field_name in _DIGEST_FIELDS:
+        if recorded.get(field_name) != rederived.get(field_name):
+            raise ProvenanceMismatch(f"{field_name}: recorded {recorded.get(field_name)!r} != rederived {rederived.get(field_name)!r}")
+
+
+__all__ = ["ProvenanceMismatch", "stamp", "verify_stamp"]

src/openultrasast/core/trace.py

@@ -0,0 +1,74 @@
+"""Canonical trace schema for the detection core (Req 1).
+
+One family-agnostic trace record per analyzed change, serialized deterministically:
+identical inputs produce byte-identical canonical output. The access-control
+prover's trace is the first implementation of this contract.
+"""
+
+from __future__ import annotations
+
+import json
+from dataclasses import asdict, dataclass, field
+from typing import Any
+
+from openultrasast.core.verdict import Judgment
+
+
+def _canonical_bytes(payload: dict[str, Any]) -> bytes:
+    return json.dumps(payload, sort_keys=True, separators=(",", ":"), ensure_ascii=False).encode()
+
+
+@dataclass(frozen=True)
+class Hop:
+    """One ordered hop with its call-target completeness."""
+
+    function: str
+    call_line: int | None
+    complete: bool
+
+
+@dataclass(frozen=True)
+class Witness:
+    """Evidence for or against a guard, with provenance and match relation."""
+
+    kind: str
+    provenance: str
+    relation: str
+
+
+@dataclass(frozen=True)
+class Guard:
+    """A guard effect observed on a path (kind plus effect)."""
+
+    kind: str
+    effect: str
+
+
+@dataclass(frozen=True)
+class TraceRecord:
+    """The canonical security trace: entry, hops, operation, witnesses, guards, judgment, digests."""
+
+    entry: str
+    hops: tuple[Hop, ...]
+    operation_kind: str
+    resource: str
+    authority: str
+    witnesses: tuple[Witness, ...] = ()
+    guards: tuple[Guard, ...] = ()
+    completeness_reasons: tuple[str, ...] = ()
+    judgment: Judgment = Judgment.INDETERMINATE
+    digests: dict[str, str] = field(default_factory=dict)
+
+    def record(self) -> dict[str, Any]:
+        """JSON-ready dict with sorted keys; enums encode as their value strings."""
+        payload: dict[str, Any] = asdict(self)
+        payload["judgment"] = self.judgment.value
+        record: dict[str, Any] = json.loads(json.dumps(payload, sort_keys=True))
+        return record
+
+    def canonical(self) -> bytes:
+        """Deterministic byte serialization (Req 1.2)."""
+        return _canonical_bytes(self.record())
+
+
+__all__ = ["Hop", "TraceRecord", "Witness"]

src/openultrasast/core/verdict.py

@@ -0,0 +1,51 @@
+"""Verdict vocabulary and verdict contract for the detection core (Req 2, 5, 9).
+
+Every analyzed operation is judged as exactly one of unguarded, discharged, or
+indeterminate. A verdict is either a proven claim (witness attached, exact
+location) or a bounded silence (coverage reason attached). Indeterminate never
+converts to clean, and models may only judge residuals zero-shot over a trace.
+"""
+
+from __future__ import annotations
+
+import enum
+from dataclasses import dataclass
+from typing import Any
+
+
+class Judgment(enum.Enum):
+    """The three-way judgment vocabulary; value strings are the wire format."""
+
+    UNGUARDED = "unguarded"
+    DISCHARGED = "discharged"
+    INDETERMINATE = "indeterminate"
+
+
+@dataclass(frozen=True)
+class ProvenClaim:
+    """A defect claim carrying its witness and exact location (Req 5.1)."""
+
+    trace_id: str
+    witness: str
+    path: str
+    line: int
+    family: str
+
+
+@dataclass(frozen=True)
+class BoundedSilence:
+    """An undecided site with its coverage reason; never a clean result (Req 5.2)."""
+
+    path: str
+    reason: str
+    coverage: dict[str, Any]
+
+
+def as_clean(judgment: Judgment) -> Judgment:
+    """Return a clean judgment, refusing to convert indeterminate (Req 2.1)."""
+    if judgment is Judgment.INDETERMINATE:
+        raise ValueError("indeterminate never converts to a clean judgment")
+    return judgment
+
+
+__all__ = ["BoundedSilence", "Judgment", "ProvenClaim", "as_clean"]

tests/test_core_contract.py

@@ -0,0 +1,132 @@
+"""Core contract conformance tests for detection-core tasks 1.1-1.4 (Reqs 1, 2, 3, 5, 6, 9)."""
+
+import sys
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parents[1]))
+
+from openultrasast.core.coverage import Coverage, InstrumentFailure, check_reads  # noqa: E402
+from openultrasast.core.provenance import ProvenanceMismatch, stamp, verify_stamp  # noqa: E402
+from openultrasast.core.trace import Guard, Hop, TraceRecord, Witness  # noqa: E402
+from openultrasast.core.verdict import BoundedSilence, Judgment, ProvenClaim, as_clean  # noqa: E402
+
+
+def _trace() -> TraceRecord:
+    return TraceRecord(
+        entry="src/app.py::handler",
+        hops=(Hop(function="handler", call_line=10, complete=True),),
+        operation_kind="protected_read",
+        resource="credentials",
+        authority="admin",
+        witnesses=(Witness(kind="guard", provenance="fact:checkPermission", relation="all_paths"),),
+        guards=(Guard(kind="permission_check", effect="branches"),),
+        completeness_reasons=(),
+        judgment=Judgment.UNGUARDED,
+        digests={"input": "abc123"},
+    )
+
+
+def test_trace_serializes_byte_identical_on_repeat() -> None:
+    first = _trace().canonical()
+    second = _trace().canonical()
+    assert first == second
+    assert isinstance(first, bytes)
+
+
+def test_trace_record_pins_schema_fields() -> None:
+    record = _trace().record()
+    for field in (
+        "entry",
+        "hops",
+        "operation_kind",
+        "resource",
+        "authority",
+        "witnesses",
+        "guards",
+        "completeness_reasons",
+        "judgment",
+        "digests",
+    ):
+        assert field in record
+    assert record["judgment"] == "unguarded"
+
+
+def test_judgment_vocabulary_is_exactly_three_way() -> None:
+    assert {j.value for j in Judgment} == {"unguarded", "discharged", "indeterminate"}
+
+
+def test_indeterminate_never_converts_to_clean() -> None:
+    assert as_clean(Judgment.DISCHARGED) == Judgment.DISCHARGED
+    try:
+        as_clean(Judgment.INDETERMINATE)
+        raise AssertionError("indeterminate must never convert to clean")
+    except ValueError:
+        pass
+
+
+def test_proven_claim_requires_witness_and_location() -> None:
+    claim = ProvenClaim(trace_id="t1", witness="w1", path="src/app.py", line=10, family="access_control")
+    assert claim.family == "access_control"
+    silence = BoundedSilence(path="src/app.py", reason="unreached", coverage={"entry_points": 0})
+    assert silence.reason == "unreached"
+
+
+def test_coverage_requires_exactly_one_bucket_per_call() -> None:
+    good = Coverage(entry_points=2, frameworks_recognised={"jenkins": 1}, calls=3, complete=1, incomplete=1, unresolved=1)
+    good.validate()
+    bad = Coverage(entry_points=1, frameworks_recognised={}, calls=3, complete=2, incomplete=1, unresolved=1)
+    try:
+        bad.validate()
+        raise AssertionError("two buckets for one call must be refused")
+    except ValueError:
+        pass
+    negative = Coverage(entry_points=1, frameworks_recognised={}, calls=3, complete=-1, incomplete=2, unresolved=2)
+    try:
+        negative.validate()
+        raise AssertionError("negative bucket counts must be refused")
+    except ValueError:
+        pass
+
+
+def test_verdict_contract_exposes_no_model_role_path() -> None:
+    import openultrasast.core.verdict as verdict_module
+
+    public = verdict_module.__all__
+    assert not any("model" in name.lower() or "judge" in name.lower() for name in public), (
+        "the verdict contract must expose no model/judge path; models judge residuals zero-shot over a trace only"
+    )
+
+
+def test_zero_byte_read_is_instrument_failure() -> None:
+    try:
+        check_reads({"src/app.py": 0, "src/lib.py": 12})
+        raise AssertionError("zero-byte read must fail the run")
+    except InstrumentFailure:
+        pass
+    check_reads({"src/app.py": 5})
+
+
+def test_provenance_stamp_and_mismatch_refusal() -> None:
+    record = stamp(
+        analyzer_revision="d063167",
+        fact_set_digest="3eb5bf699434",
+        acquisition_record_digest="none",
+        configuration_digest="095b5a4905ad",
+        population_digest="c866c0e812c0",
+        change_id="case-1",
+    )
+    assert set(record) == {
+        "analyzer_revision",
+        "fact_set_digest",
+        "acquisition_record_digest",
+        "configuration_digest",
+        "population_digest",
+        "input_digest",
+    }
+    verify_stamp(record, record.copy())
+    tampered = {**record, "fact_set_digest": "ffffffffffff"}
+    try:
+        verify_stamp(tampered, record)
+        raise AssertionError("mismatched digest must be refused")
+    except ProvenanceMismatch:
+        pass