/**
 * The Evidence Ledger — the per-turn evidence snapshot the §5 soundness
 * predicate reads (SDD §G; v1.1 §7; Inv 7). Read + Action feed entries IN; the
 * Claims Kernel reads them OUT as the final output authority. This module owns
 * the entry SHAPE and the snapshot's resolution rules; it does NOT implement the
 * soundness predicate (`CLAIM_ALLOWED` — a separate kernel deliverable, SDD §Q.3)
 * and it does NOT enforce the `must_read_this_turn ⟹ sourceMode=="live"` rule
 * (that is Q3's soundness check — this module only RECORDS `sourceMode`
 * faithfully so Q3 can reject a cache-validated live read).
 *
 * **DISTINCT from `../ledger.ts`** (the Execution Ledger — hot-path replay/dedup
 * keyed by `intentHash`). That answers "has this intent already executed?"; this
 * is the per-turn evidence snapshot a claim is validated against. They share the
 * word "ledger" and nothing else — do not conflate or merge them.
 *
 * Transcribed VERBATIM from SDD §G / v1.1 §7 — the entry shape is not
 * re-derived, re-ordered semantically, or paraphrased (SDD zero-drift contract).
 * Pure & self-contained — no kernel-downstream import (SDD §R kernel purity:
 * `adjudicate → claustrum → ibatexas`, never backward); no clock/RNG/IO (the
 * `fetchedAt` timestamp is supplied BY the caller — Read/Action — not minted
 * here, so the ledger stays a deterministic data structure).
 */

import type { ClaimVerdict } from "./verdict.js";
import { sameValue } from "./value-equality.js";

// ─────────────────────────────────────────────────────────────────────────
// Ledger provenance vocabulary — SDD §G / v1.1 §7, verbatim
// ─────────────────────────────────────────────────────────────────────────

/**
 * The Read Kernel's per-entry PROVENANCE verdict as it lands in the ledger
 * (SDD §F "provenance: TRUSTED/UNTRUSTED_DATA"; SDD §G / v1.1 §7 entry shape):
 *
 *   "TRUSTED" | "UNTRUSTED_DATA"
 *
 * This is the Read-layer *trust* axis recorded ON a ledger entry — verbatim from
 * §G. It is DELIBERATELY NOT the payload-level `Taint` lattice in `../taint.ts`
 * (`SYSTEM | TRUSTED | UNTRUSTED`, the LLM-boundary payload-trust meet): §G names
 * exactly the two values `TRUSTED` / `UNTRUSTED_DATA`, and the SDD §A precedence
 * rule binds the build to the canon's vocabulary where they differ. An
 * `UNTRUSTED_DATA` entry may never be the *validating value* of any claim
 * (Inv 3) — but THAT gate is the soundness predicate's job (Q3); here the field
 * is only recorded faithfully.
 */
export type LedgerTaint = "TRUSTED" | "UNTRUSTED_DATA";

/**
 * The closed membership tuple for `LedgerTaint`, in spec order (SDD §G). Single
 * source of truth for the two members; `isLedgerTaint` narrows against it.
 */
export const LEDGER_TAINTS: readonly LedgerTaint[] = [
  "TRUSTED",
  "UNTRUSTED_DATA",
] as const;

/** Type guard: is `value` one of the exactly-two ledger taints (§G)? Pure. */
export function isLedgerTaint(value: unknown): value is LedgerTaint {
  return (
    typeof value === "string" &&
    (LEDGER_TAINTS as readonly string[]).includes(value)
  );
}

/**
 * The ORIGIN-trust axis recorded on a ledger entry (SDD §G / §J.3; v1.1 §7) — a
 * THREE-valued classification, DISTINCT from the read-layer two-valued
 * `LedgerTaint`:
 *
 *   "FIRST_PARTY" | "TRUSTED_THIRD_PARTY" | "UNTRUSTED_DATA"
 *
 * This is the value's ORIGIN trust, NOT the read-layer `taint`. The two axes are
 * deliberately separate (SDD §J.3 — "the origin axis is three-valued …, distinct
 * from the read-layer two-valued `taint`"): a value may be content-`TRUSTED`
 * (taint) yet originate from an `UNTRUSTED_DATA` ingress (origin), and both must
 * be recorded independently so neither can silently overwrite the other.
 *
 * It "survives persistence" (SDD §G C3; Inv 3): an `UNTRUSTED_DATA` ingress stays
 * `UNTRUSTED_DATA` across reads and never washes up to a trusted class; a
 * `TRUSTED_THIRD_PARTY` origin is NOT first-party. The provenance policies read
 * this axis (SDD §G):
 *
 *   - `first_party_only` ⟹ origin === `FIRST_PARTY` (a `TRUSTED_THIRD_PARTY`
 *     origin does NOT satisfy it → `REFUSED`).
 *   - `preserve`         ⟹ any NON-`UNTRUSTED_DATA` origin (so `FIRST_PARTY` or
 *     `TRUSTED_THIRD_PARTY`).
 *
 * **Absent/unlabeled ⟹ NOT first-party (fail-closed)** — only an explicit
 * first-party MINT may carry `FIRST_PARTY`; nothing is auto-promoted to it. This
 * is what makes `first_party_only` strictly STRONGER than `preserve` (the
 * de-vacuumed gate of soundness's C3): under the old 2-value origin the gate was
 * vacuous (every non-untrusted origin looked first-party); the third class
 * separates a trusted third party from a true first party.
 */
export type OriginProvenance =
  | "FIRST_PARTY"
  | "TRUSTED_THIRD_PARTY"
  | "UNTRUSTED_DATA";

/**
 * The closed membership tuple for `OriginProvenance`, in spec order (SDD §G —
 * trusted→untrusted). Single source of truth for the three members;
 * `isOriginProvenance` narrows against it.
 */
export const ORIGIN_PROVENANCES: readonly OriginProvenance[] = [
  "FIRST_PARTY",
  "TRUSTED_THIRD_PARTY",
  "UNTRUSTED_DATA",
] as const;

/**
 * Type guard: is `value` one of the exactly-three origin classes (§G)? Pure.
 * NOTE it REJECTS the read-layer-only `"TRUSTED"` — that is a `LedgerTaint`
 * member, not an origin class (the two axes are distinct, SDD §J.3).
 */
export function isOriginProvenance(value: unknown): value is OriginProvenance {
  return (
    typeof value === "string" &&
    (ORIGIN_PROVENANCES as readonly string[]).includes(value)
  );
}

/**
 * The freshness SOURCE mode recorded on a ledger entry (SDD §G / v1.1 §7):
 *
 *   "live" | "cache"
 *
 * A timestamped, faithfully-recorded distinction (H4): a value read live this
 * turn is `"live"`; one served from a cache is `"cache"`. `must_read_this_turn`
 * evidence REQUIRES `sourceMode == "live"` — but enforcing that is Q3's
 * soundness rule. Q2 only guarantees the distinction is *preserved* at read time
 * so cache can never masquerade as live (a cache row carries both
 * `sourceMode: "cache"` AND its own `fetchedAt`, never a fabricated live stamp).
 */
export type SourceMode = "live" | "cache";

/** The closed membership tuple for `SourceMode`, in spec order (§G). */
export const SOURCE_MODES: readonly SourceMode[] = ["live", "cache"] as const;

/** Type guard: is `value` one of the exactly-two source modes (§G)? Pure. */
export function isSourceMode(value: unknown): value is SourceMode {
  return (
    typeof value === "string" && (SOURCE_MODES as readonly string[]).includes(value)
  );
}

// ─────────────────────────────────────────────────────────────────────────
// Structural provenance — the deriveProvenance hook (Plan 1 Phase 4 / W6 seam)
// ─────────────────────────────────────────────────────────────────────────

/**
 * The INJECTED, PURE capability that DERIVES an entry's trust labels from its
 * SOURCE-OF-RECORD identity rather than letting the adapter SELF-DECLARE them
 * (Plan 1 Phase 4 / W6; same injection pattern as soundness `owns`). The intent:
 * by the time soundness reads `entry.taint`/`entry.originProvenance`, those labels
 * were derived from the source identity (connection identity / endpoint / table
 * origin), not stamped by a possibly-model-authored adapter.
 *
 * W6 SHIPS the HOOK + its application point (in `record`) + the null-provenance
 * default-deny; it does NOT ship the derivation LOGIC. Until W5 wires real source
 * descriptors, consumers pass no deriver and the self-declared labels are used
 * (then normalized fail-closed) — so the §11 TCB "Read adapters" row stays
 * TRUSTED, not VERIFIED, until W5 lands. Must be PURE (deterministic, no IO).
 */
export interface ProvenanceDeriver {
  readonly derive: (sourceOfRecord: unknown) => {
    readonly taint: LedgerTaint;
    readonly originProvenance: OriginProvenance;
  };
}

// ─────────────────────────────────────────────────────────────────────────
// Per-envelope dispatch result — SDD §G `dispatch?`; v1.1 §10 Inv 4 (H10/H11)
// ─────────────────────────────────────────────────────────────────────────

/**
 * One envelope's dispatch outcome (SDD §G `dispatch?: PerEnvelopeResult[]`; v1.1
 * §10 Inv 4 / H10 / H11). Defined minimally — Q2 only needs partial commits to
 * be *representable*, not to drive them.
 *
 * Inv 4: "Action-claim success is defined (verdict + dispatch + `result.success`;
 * settlement ≠ session); per-envelope results make partial commits representable."
 * An `action_outcome` claim's evidence is this turn's Action verdict + dispatch,
 * NOT a read — so when one Action fans out to several side-effecting envelopes,
 * each envelope's success is recorded SEPARATELY here. A turn in which envelope A
 * settled but envelope B failed is then representable as a `dispatch` array with
 * `success: true` / `success: false` members, rather than collapsing to a single
 * turn-wide boolean that would hide the partial commit.
 *
 * `settled` (settlement ≠ session, Inv 4): `success` is the dispatch result;
 * `settled` records whether the side effect durably committed downstream. The two
 * are kept distinct so a session-level ack can never masquerade as settlement.
 */
export interface PerEnvelopeResult {
  /** Stable identifier of the dispatched envelope (e.g. its intentHash). */
  readonly envelopeId: string;
  /** Whether THIS envelope's dispatch succeeded (`result.success`, Inv 4). */
  readonly success: boolean;
  /**
   * Whether the side effect durably SETTLED downstream (settlement ≠ session,
   * Inv 4). Optional: absent when settlement is not yet known/applicable; a
   * present `false` is distinct from absence, mirroring error ≠ absence.
   */
  readonly settled?: boolean;
}

// ─────────────────────────────────────────────────────────────────────────
// The ledger entry — SDD §G / v1.1 §7, EXACT shape
// ─────────────────────────────────────────────────────────────────────────

/**
 * One Evidence Ledger entry — the EXACT §G / v1.1 §7 shape:
 *
 * ```
 * { key, value, source,
 *   fetchedAt: <timestamp>,            // H4: a timestamp, NOT a boolean
 *   sourceMode: "live" | "cache",      // H4: must_read_this_turn REQUIRES "live"
 *   taint: "TRUSTED" | "UNTRUSTED_DATA",                                        // read-layer trust (2-value)
 *   originProvenance: "FIRST_PARTY" | "TRUSTED_THIRD_PARTY" | "UNTRUSTED_DATA", // C3 origin-trust (3-value); survives persistence
 *   dispatch?: PerEnvelopeResult[] }   // H10: per-envelope dispatch results
 * ```
 *
 * `fetchedAt` is a `number` epoch-millis TIMESTAMP, never a boolean (H4) — a
 * boolean would let a cache row claim "fresh: true" and masquerade as live; a
 * timestamp + `sourceMode` together make that impossible.
 */
export interface EvidenceEntry {
  /** The evidence key this entry binds (e.g. an `EvidenceRequirement.key`). */
  readonly key: string;
  /** The evidence value (opaque to the ledger; the claims kernel interprets it). */
  readonly value: unknown;
  /** Human/system-readable source descriptor (which read/action produced it). */
  readonly source: string;
  /**
   * When the evidence was fetched — epoch-millis TIMESTAMP, NOT a boolean (H4).
   * Supplied by the caller (Read/Action), so the ledger needs no clock and stays
   * deterministic; cache cannot masquerade as live because its stamp is its own.
   */
  readonly fetchedAt: number;
  /** `"live"` (read this turn) vs `"cache"` (served from cache) — H4, faithful. */
  readonly sourceMode: SourceMode;
  /** Read-layer trust of the value (SDD §G) — `TRUSTED` | `UNTRUSTED_DATA`. */
  readonly taint: LedgerTaint;
  /**
   * The provenance of the value's ORIGIN (SDD §G / §J.3; C3, Inv 3) — the
   * THREE-valued `OriginProvenance` axis (`FIRST_PARTY` | `TRUSTED_THIRD_PARTY` |
   * `UNTRUSTED_DATA`), DISTINCT from the 2-value read-layer `taint`. It survives
   * persistence: a row written from an `UNTRUSTED_DATA` ingress stays
   * `UNTRUSTED_DATA` across reads and never "washes" up to a trusted class; a
   * `TRUSTED_THIRD_PARTY` origin is NOT first-party. `first_party_only` requires
   * `FIRST_PARTY` here (a `TRUSTED_THIRD_PARTY` origin → `REFUSED`); `preserve`
   * requires only a non-`UNTRUSTED_DATA` origin. Absent/unlabeled ⟹ NOT
   * first-party (fail-closed) — only an explicit first-party mint earns
   * `FIRST_PARTY`.
   */
  readonly originProvenance: OriginProvenance;
  /**
   * Optional per-envelope dispatch results (H10) — present for `action_outcome`
   * evidence so partial commits are representable; absent for plain reads.
   */
  readonly dispatch?: readonly PerEnvelopeResult[];
}

/**
 * The input a writer (Read/Action) supplies to record an entry — the §G fields,
 * with `dispatch` optional, PLUS an OPTIONAL write-time-only `sourceOfRecord`
 * descriptor (W6). `sourceOfRecord` is consumed by an injected `ProvenanceDeriver`
 * at write time and is NEVER stored on the entry (the stored `EvidenceEntry` shape
 * stays the frozen §G shape). When no deriver is injected, `sourceOfRecord` is
 * ignored and the self-declared `taint`/`originProvenance` are used (then
 * normalized fail-closed).
 */
export type EvidenceEntryInput = EvidenceEntry & {
  readonly sourceOfRecord?: unknown;
};

/**
 * NULL-PROVENANCE DEFAULT-DENY write guard (Plan 1 Phase 4 / W6). Normalize an
 * entry's trust labels at the WRITE boundary so the ledger never stores a
 * structurally-typed-but-mislabeled row that could later VALIDATE:
 *
 *   - `taint` / `originProvenance` absent OR not a recognized member → coerced to
 *     `UNTRUSTED_DATA` (fail-closed default-deny — "no provenance" = denied, NEVER
 *     a silent trusted default). Because soundness REFUSES any `UNTRUSTED_DATA`
 *     origin/taint, a null-provenance entry can never be a validating value.
 *   - `sourceMode` absent OR not a recognized member → coerced to `"cache"` (not
 *     provably live → a `must_read_this_turn` requirement cannot validate from it).
 *
 * NEVER coerces UP to a trusted class. The write-time-only `sourceOfRecord` is
 * stripped (it is not part of the stored §G entry). Pure: deterministic; no
 * clock/RNG/IO. A valid entry passes through with its labels unchanged.
 */
export function normalizeEvidenceEntry(input: EvidenceEntryInput): EvidenceEntry {
  // Strip the write-time-only descriptor; it is not part of the stored §G shape.
  const { sourceOfRecord: _ignored, ...rest } = input;
  void _ignored;
  return {
    ...rest,
    // Fail-closed default-deny: anything not provably trusted is UNTRUSTED_DATA.
    taint: isLedgerTaint(rest.taint) ? rest.taint : "UNTRUSTED_DATA",
    originProvenance: isOriginProvenance(rest.originProvenance)
      ? rest.originProvenance
      : "UNTRUSTED_DATA",
    // Fail-closed: not provably live → cache.
    sourceMode: isSourceMode(rest.sourceMode) ? rest.sourceMode : "cache",
  };
}

// ─────────────────────────────────────────────────────────────────────────
// Read resolution — SDD §G / v1.1 §7; Inv 7 (error ≠ absence)
// ─────────────────────────────────────────────────────────────────────────

/**
 * The distinguishable STATES a key can be in within the snapshot (SDD §G; Inv 7).
 * These are NOT the claim verdict — they are the ledger's read-resolution states,
 * each of which the soundness predicate maps to a verdict. Four states, all
 * distinct (the Inv 7 demand "read-error ≠ read-absence"):
 *
 *   - `"present"`   — a single un-conflicted value was written; resolvable.
 *   - `"absent"`    — the key was never written this turn (a read ABSENCE).
 *   - `"error"`     — a read ERROR was recorded for the key (DISTINCT from absent).
 *   - `"conflict"`  — two+ writes to the key disagreed this turn (H3); the value
 *                     is poisoned and must resolve `UNKNOWN`, never last-write.
 *
 * `absent`, `error`, and `conflict` all resolve to a NON-CONCRETE verdict
 * (`UNKNOWN`-or-safer); only `present` exposes the concrete value to validation.
 * They remain SEPARATE states so callers (and audit) can tell them apart — an
 * error fails CLOSED loudly, an absence is honest ignorance (Inv 7).
 */
export type EvidenceState = "present" | "absent" | "error" | "conflict";

/**
 * The result of resolving a key against the snapshot (SDD §G; Inv 7). Carries
 * the distinguishable `state` AND the safe `verdict` floor:
 *
 *   - `present`  → `verdict: "VALIDATED"`-eligible; `value`/`entry` exposed. (The
 *                  ledger does NOT itself assert VALIDATED — that is the soundness
 *                  predicate; `present` only means "a concrete value is readable".
 *                  We surface `verdict: "UNKNOWN"` for non-present and leave the
 *                  present case's verdict to the caller by exposing `entry`.)
 *   - `absent`   → `verdict: "UNKNOWN"`, no `value`/`entry`.
 *   - `error`    → `verdict: "UNKNOWN"` (fail CLOSED), no `value`/`entry`.
 *   - `conflict` → `verdict: "UNKNOWN"` (H3 — never last-write-as-validated),
 *                  no `value`/`entry`.
 *
 * The KEY safety property (Inv 7 / H3): for every non-`present` state the
 * resolution NEVER carries a concrete `value` — a read error, an absence, and a
 * conflict are indistinguishable from "no concrete value" to a downstream
 * consumer that only inspects `value`, while `state` keeps them distinguishable
 * to one that cares.
 */
export interface EvidenceResolution {
  readonly key: string;
  /** The distinguishable ledger state (error ≠ absence ≠ conflict ≠ present). */
  readonly state: EvidenceState;
  /**
   * The safe verdict FLOOR the ledger guarantees for this key. `UNKNOWN` for
   * every non-`present` state (never a concrete value escapes as VALIDATED);
   * `present` resolutions leave the final VALIDATED/REFUSED to the soundness
   * predicate, so the ledger reports `UNKNOWN` here too and exposes `entry` —
   * the ledger is not the soundness authority and must not pre-empt it.
   */
  readonly verdict: Extract<ClaimVerdict, "UNKNOWN">;
  /**
   * The concrete value — ONLY present when `state === "present"`. Absent/error/
   * conflict states carry NO value (the Inv 7 / H3 safety floor). Use a presence
   * check on `entry`, not on `value === undefined` (a present value MAY be
   * `undefined` legitimately; the discriminator is `state`).
   */
  readonly entry?: EvidenceEntry;
}

// Internal stored cell — a key's accumulated state within ONE snapshot.
interface Cell {
  // The last entry written for a non-error, single-write key.
  readonly entry?: EvidenceEntry;
  // True once a read ERROR was recorded for this key (distinct from absence).
  readonly errored?: boolean;
  // The recorded error reason (audit), distinct from a missing value.
  readonly errorReason?: string;
  // True once two writes DISAGREED on this key this turn (H3 conflict).
  readonly conflicted?: boolean;
  // Count of value-writes seen (drives conflict detection independent of value).
  readonly writeCount: number;
}

/**
 * The Evidence Ledger (SDD §G / v1.1 §7) — a single PER-TURN SNAPSHOT. Construct
 * one per turn; Read + Action `record*` evidence into it; the Claims Kernel
 * `resolve`s keys out of it. Every mutation advances a monotonic `version` token
 * that identifies the snapshot's revision.
 *
 * NOT a cache across turns: a new turn => a new `EvidenceLedger`. The snapshot
 * boundary is what makes "two reads of the same key in one turn" (H3) and
 * "must_read_this_turn" (H4) well-defined.
 *
 * Pure data structure: no clock, RNG, or IO. `fetchedAt` timestamps arrive from
 * callers; the version token is a deterministic in-memory counter.
 */
export class EvidenceLedger {
  // Monotonic snapshot revision; advances on EVERY mutation. Starts at 0 (empty
  // snapshot), so the first write yields version 1. Never decreases, never
  // resets within a ledger instance.
  #version = 0;

  // A stable identifier for THIS snapshot instance — lets a resolution name the
  // snapshot it came from (the "identifies the snapshot" half of AC1). The pair
  // (snapshotId, version) uniquely names a point-in-time revision.
  readonly #snapshotId: string;

  readonly #cells = new Map<string, Cell>();

  // OPTIONAL injected structural-provenance hook (W6). When present, an entry that
  // carries a `sourceOfRecord` has its trust labels DERIVED from that descriptor at
  // write time, overriding the adapter's self-declared labels. Absent ⟹ the
  // self-declared labels are used (then normalized fail-closed).
  readonly #deriver?: ProvenanceDeriver;

  /**
   * @param snapshotId Optional caller-supplied snapshot identity (e.g. a turn
   *   id). When omitted, a deterministic per-instance counter id is used so the
   *   ledger needs no RNG; distinct instances still get distinct ids.
   * @param deriver Optional structural-provenance hook (W6). When supplied, a
   *   recorded entry's `sourceOfRecord` is mapped to its trust labels at write
   *   time. The kernel ships the seam; the derivation logic is W5 (adapter-side).
   */
  constructor(snapshotId?: string, deriver?: ProvenanceDeriver) {
    this.#snapshotId = snapshotId ?? `snapshot-${EvidenceLedger.#nextId()}`;
    this.#deriver = deriver;
  }

  // Deterministic, monotonic instance-id source (no RNG). Module-private.
  static #idCounter = 0;
  static #nextId(): number {
    EvidenceLedger.#idCounter += 1;
    return EvidenceLedger.#idCounter;
  }

  /** The current monotonic version/sequence token of this snapshot (AC1). */
  get version(): number {
    return this.#version;
  }

  /** The stable identity of this snapshot instance (AC1 — identifies snapshot). */
  get snapshotId(): string {
    return this.#snapshotId;
  }

  /**
   * Record an evidence entry for a key (Read/Action write path). Advances the
   * version token monotonically.
   *
   * **Same-key conflict → UNKNOWN (H3):** a SECOND write to a key whose stored
   * value DIFFERS from the new one raises the key's `conflicted` flag (and keeps
   * last-write-wins for the stored `entry`, per §G "last-write-wins **and** a
   * conflict flag"). A subsequent `resolve` of a conflicted key yields
   * `UNKNOWN`, never the last-written value as a validated concrete. A repeated
   * write of the SAME value does not conflict (idempotent re-read).
   *
   * Writing over a previously-errored key is itself a conflict-class event: an
   * error and a value disagree about whether the read succeeded, so the key is
   * marked conflicted (the safest interpretation — never silently let a later
   * value erase a recorded error).
   */
  record(input: EvidenceEntryInput): void {
    // ── W6 structural-provenance hook: when a deriver is injected AND the write
    // carries a `sourceOfRecord`, DERIVE the trust labels from the source identity,
    // overriding the adapter's self-declared `taint`/`originProvenance`. Then the
    // null-provenance default-deny normalizer runs over the result (so a deriver
    // that returns an invalid label still fails closed).
    const derived =
      this.#deriver !== undefined && input.sourceOfRecord !== undefined
        ? { ...input, ...this.#deriver.derive(input.sourceOfRecord) }
        : input;
    const entry = normalizeEvidenceEntry(derived);
    const prior = this.#cells.get(entry.key);
    this.#version += 1;

    if (prior === undefined) {
      this.#cells.set(entry.key, { entry, writeCount: 1 });
      return;
    }

    // A value-write after a recorded error (or vice versa) is a disagreement
    // about whether the read succeeded — conflict, fail closed.
    const conflictsWithError = prior.errored === true;
    // Two value-writes that DISAGREE on the value are a conflict (H3). Equal
    // values are an idempotent re-read and do NOT conflict.
    const disagrees =
      prior.entry !== undefined && !sameValue(prior.entry.value, entry.value);

    this.#cells.set(entry.key, {
      // last-write-wins for the stored entry (§G), even on conflict.
      entry,
      conflicted: prior.conflicted === true || conflictsWithError || disagrees,
      // An error flag is sticky across a later value-write (the disagreement is
      // preserved as a conflict above; we no longer claim a clean error state).
      writeCount: prior.writeCount + 1,
    });
  }

  /**
   * Record a read ERROR for a key (Read fail-closed path — Inv 7). This is a
   * DISTINCT state from absence: an errored key resolves `UNKNOWN`-or-safer, but
   * its resolution `state` is `"error"`, not `"absent"`. Advances the version.
   *
   * Recording an error after a value-write (or vice versa) marks the key
   * `conflicted` — the two disagree about whether the read succeeded; fail
   * closed rather than letting either win silently.
   */
  recordError(key: string, reason: string): void {
    const prior = this.#cells.get(key);
    this.#version += 1;

    if (prior === undefined) {
      this.#cells.set(key, { errored: true, errorReason: reason, writeCount: 0 });
      return;
    }

    // An error after a value-write disagrees with that value → conflict.
    const conflictsWithValue = prior.entry !== undefined;
    this.#cells.set(key, {
      ...prior,
      errored: true,
      errorReason: reason,
      conflicted: prior.conflicted === true || conflictsWithValue,
    });
  }

  /**
   * Resolve a key against the snapshot (Claims Kernel read path; SDD §G; Inv 7;
   * H3). Returns the distinguishable `state` AND a safe verdict floor:
   *
   *   - never written      → `{ state: "absent",   verdict: "UNKNOWN" }`
   *   - error recorded     → `{ state: "error",    verdict: "UNKNOWN" }`
   *   - conflicting writes → `{ state: "conflict", verdict: "UNKNOWN" }`
   *   - clean single write → `{ state: "present",  verdict: "UNKNOWN", entry }`
   *
   * For EVERY non-`present` state, NO concrete `value`/`entry` is exposed — a
   * read error, an absence, and a conflict are all "no concrete value" to a
   * consumer reading `entry`, while `state` keeps them distinct (Inv 7 / H3).
   * `present` exposes the entry but still reports `verdict: "UNKNOWN"` because
   * the ledger is NOT the soundness authority — VALIDATED is the predicate's call.
   */
  resolve(key: string): EvidenceResolution {
    const cell = this.#cells.get(key);

    // Absence — the key was never written this turn (Inv 7: distinct from error).
    if (cell === undefined) {
      return { key, state: "absent", verdict: "UNKNOWN" };
    }

    // Conflict takes precedence (H3): a poisoned key never exposes a value, even
    // though last-write-wins kept an `entry`. Checked before `error`/`present`.
    if (cell.conflicted === true) {
      return { key, state: "conflict", verdict: "UNKNOWN" };
    }

    // Error (Inv 7) — distinct state from absence; fail closed, no value.
    if (cell.errored === true) {
      return { key, state: "error", verdict: "UNKNOWN" };
    }

    // Present — a single, un-conflicted, non-error value. Expose the entry; the
    // verdict floor stays UNKNOWN (soundness, not the ledger, decides VALIDATED).
    if (cell.entry !== undefined) {
      return { key, state: "present", verdict: "UNKNOWN", entry: cell.entry };
    }

    // Defensive: a cell with neither entry, error, nor conflict is an absence.
    return { key, state: "absent", verdict: "UNKNOWN" };
  }

  /**
   * Resolve a key AGAINST its declared FALSIFIERS — the CROSS-KEY conflict gate
   * (Plan 1 Phase 4 / W6; the runtime arm of the falsifier-completeness gate).
   *
   * DISTINCT from the same-key last-write-wins conflict above (`record`/H3): that
   * detects two writes to the SAME key disagreeing. THIS detects a DIFFERENT key —
   * a declared FALSIFIER — being PRESENT, which CONTRADICTS the claim the resolved
   * key backs (e.g. STORE_OPEN_NOW's key is falsified by a present ScheduleOverride
   * key; PAYMENT_STATUS=paid is falsified by a present refund/chargeback key). The
   * mere PRESENCE of any falsifier key (a value that fired this turn) poisons the
   * resolved key → `conflict` → `UNKNOWN`, exactly like a same-key conflict.
   *
   * Demote-only & fail-closed: if the base key is not `present`, its own
   * (absent/error/conflict) resolution is returned unchanged (a falsifier cannot
   * UPGRADE a non-present key). If the base key is `present` AND any falsifier key is
   * `present` (a live contradiction) OR `error`/`conflict` (its read could NOT be
   * determined this turn — we cannot prove the falsifier did NOT fire), the result is
   * downgraded to `conflict` → `UNKNOWN` (F6). This is SYMMETRIC with the base-key
   * axis, which already demotes to UNKNOWN on error/conflict: a declared falsifier
   * that errored poisons exactly the claim it guards (e.g. PAYMENT_STATUS=paid while
   * the refund/chargeback falsifier read errored — a refund may have occurred but
   * could not be read, so `paid` must NOT keep rendering). Only an `absent` falsifier
   * key does NOT fire — successfully determining no falsifier is present is the normal
   * happy path (e.g. no refund exists). Demote-only: UNKNOWN, never REFUSED, never a
   * promotion. Pure: read-only.
   *
   * This is the cross-key COMPANION to the soundness falsifier-completeness CAP:
   * the CAP (soundness.ts) forces UNKNOWN-only until a type DECLARES its falsifiers;
   * this gate makes a DECLARED falsifier's actual presence drive the backed key to
   * UNKNOWN. NO integrity-ranked auto-resolution (inv.16): a contradiction is never
   * silently resolved by ranking the falsifier vs the value — it is always UNKNOWN.
   */
  resolveAgainstFalsifiers(
    key: string,
    falsifierKeys: readonly string[],
  ): EvidenceResolution {
    const base = this.resolve(key);
    // A falsifier can only DEMOTE a present key; a non-present key keeps its state.
    if (base.state !== "present") return base;
    for (const fk of falsifierKeys) {
      // F6 — fail-closed & SYMMETRIC with the base-key axis. A falsifier key that is
      // `present` (a live contradiction) OR `error`/`conflict` (its read could not be
      // determined — we cannot prove it did NOT fire) poisons the base → conflict →
      // UNKNOWN. Only `absent` (provably no falsifier present) lets the base stand.
      if (this.resolve(fk).state !== "absent") {
        return { key, state: "conflict", verdict: "UNKNOWN" };
      }
    }
    return base;
  }

  /** Is `key` resolvable to a concrete, un-conflicted, non-error value? */
  has(key: string): boolean {
    return this.resolve(key).state === "present";
  }

  /** The recorded error reason for an errored key, else `undefined` (audit). */
  errorReason(key: string): string | undefined {
    const cell = this.#cells.get(key);
    return cell?.errored === true ? cell.errorReason : undefined;
  }

  /** The keys recorded in this snapshot (any state). Stable insertion order. */
  keys(): readonly string[] {
    return [...this.#cells.keys()];
  }

  /**
   * Capture the SOURCE-VERSION TOKEN of this snapshot at a point in time (W6
   * render-time freshness re-check). The pair `(snapshotId, version)` uniquely
   * names a revision; capture it at VALIDATE time and re-check it at RENDER time
   * via {@link isSnapshotFresh} so a claim validated against revision N is never
   * rendered after the ledger mutated to revision N+1 (a TOCTOU between validate
   * and render). Pure.
   */
  snapshotToken(): SnapshotToken {
    return { snapshotId: this.#snapshotId, version: this.#version };
  }
}

// ─────────────────────────────────────────────────────────────────────────
// Render-time freshness re-check — the source-version token (Plan 1 Phase 4 / W6)
// ─────────────────────────────────────────────────────────────────────────

/**
 * The SOURCE-VERSION token of an Evidence Ledger snapshot (W6). `(snapshotId,
 * version)` uniquely names a point-in-time revision; a render-time re-check
 * compares the token captured at VALIDATE time against the ledger at RENDER time.
 */
export interface SnapshotToken {
  readonly snapshotId: string;
  readonly version: number;
}

/**
 * Render-time freshness re-check (W6): is `ledger` still at the EXACT revision the
 * `token` named? `true` IFF same snapshot identity AND unchanged `version`. A
 * FALSE means the ledger mutated between validate and render — the validated claim
 * set is STALE and must NOT be rendered (re-validate or ESCALATE). Fail-closed: a
 * token from a DIFFERENT snapshot is never "fresh". Pure: read-only.
 */
export function isSnapshotFresh(token: SnapshotToken, ledger: EvidenceLedger): boolean {
  return (
    token.snapshotId === ledger.snapshotId && token.version === ledger.version
  );
}

// ─────────────────────────────────────────────────────────────────────────
// Cross-key conflict table (Plan 1 Phase 4 / W6) — the falsifier runtime arm
// ─────────────────────────────────────────────────────────────────────────

/**
 * One CROSS-KEY conflict declaration (W6): the evidence `key` is FALSIFIED when
 * `falsifierKey` is present this turn. DISTINCT from the same-key last-write-wins
 * conflict (two writes to ONE key disagreeing); this names a DIFFERENT key whose
 * presence contradicts `key` (STORE_OPEN_NOW ← a ScheduleOverride; PAYMENT_STATUS
 * ← a refund/chargeback). The companion declaration of a type's `falsifiers[]`.
 */
export interface CrossKeyConflict {
  readonly key: string;
  readonly falsifierKey: string;
}

/**
 * Detect which keys in `table` are FALSIFIED in this `ledger` (W6 cross-key gate).
 * A key is falsified iff it is itself `present` AND at least one of its declared
 * falsifier keys FIRES this turn. A falsifier FIRES when its state is NOT `absent`:
 * `present` (a live contradiction) OR `error`/`conflict` (its read could not be
 * determined — we cannot prove the falsifier did NOT fire). Only an `absent`
 * falsifier (provably not present) lets the base key stand. Returns the distinct
 * falsified keys (the set a caller must resolve to `UNKNOWN`).
 *
 * SYMMETRIC with — and a table-of-pairs wrapper over — the per-key
 * `EvidenceLedger.resolveAgainstFalsifiers` (F6): both demote on `present`/`error`/
 * `conflict` and stand only on `absent`, fail-closed and symmetric with the base-key
 * axis (which already demotes to UNKNOWN on error/conflict). Pure: read-only over the
 * ledger; demote-only; NO integrity-ranked auto-resolution (inv.16) — a fired
 * falsifier always poisons the key to UNKNOWN, never silently resolved by ranking.
 */
export function detectCrossKeyConflicts(
  ledger: EvidenceLedger,
  table: readonly CrossKeyConflict[],
): readonly string[] {
  const falsified = new Set<string>();
  for (const { key, falsifierKey } of table) {
    if (falsified.has(key)) continue;
    // The falsifier FIRES unless it is provably `absent` (mirror of the F6 fix in
    // resolveAgainstFalsifiers): present OR error OR conflict all poison the base key.
    if (
      ledger.resolve(key).state === "present" &&
      ledger.resolve(falsifierKey).state !== "absent"
    ) {
      falsified.add(key);
    }
  }
  return [...falsified];
}

// ─────────────────────────────────────────────────────────────────────────
// Value equality — drives H3 conflict detection. The conservative, fail-closed
// `sameValue` (idempotent re-read vs DISAGREEMENT) is the SINGLE canonical
// implementation in `./value-equality.ts`, shared verbatim with the P2
// same-type value-conflict gate so the two determinism-critical decisions can
// never silently diverge. Imported above; not redefined here.
// ─────────────────────────────────────────────────────────────────────────