car-verify 0.50.0

//! Attempt ledger — failure as a first-class, queryable object.
//!
//! CAR already records what happened. `car_memgine::trajectory::Trajectory`
//! keeps `(proposal, trace, outcome)` tuples on disk, the event log keeps the
//! action stream, and `car_bench`'s self-harness clusters failures to drive
//! harness evolution. What none of them answer is the question a planner needs
//! *before* it proposes:
//!
//! > Have we already tried an equivalent approach under equivalent assumptions,
//! > and if so, has anything changed that would make it worth trying again?
//!
//! Without that, a long-running agent rediscovers the same dead end every time
//! its context turns over. Negative results are the cheapest evidence the
//! system will ever have and the only kind it currently throws away.
//!
//! This module makes an [`Attempt`] a structured record — approach, the
//! assumptions it rested on, how it ended, and, when it failed, *what would
//! have to change* for a retry to be worthwhile — and makes [`AttemptLedger`]
//! answer the question above with [`AttemptLedger::consult`].
//!
//! # What it decides, and what it does not
//!
//! Matching is a decision procedure over the labels it is handed: two attempts
//! are equivalent when their normalised `approach` strings are equal and their
//! assumption *sets* are equal. That is exact, total, and deterministic.
//!
//! It emphatically does **not** decide semantic equivalence. "Retry the upload
//! with backoff" and "upload again, waiting longer each time" are one approach
//! to a reader and two to this module. Naming is the caller's job, and a caller
//! that generates a fresh label per attempt gets a ledger that never matches
//! anything — [`AttemptLedger::consult`] will honestly return
//! [`AttemptAdvice::Untried`] every time. Embedding-based clustering is a
//! deliberate non-goal here: it would make the crate's cheapest, most
//! predictable check depend on a model, and this crate has no model in it.
//!
//! The second boundary is [`Attempt::retry_when`]. The recorder declares which
//! assumptions the failure actually depended on; the ledger takes that
//! declaration at face value. A recorder that declares wrongly gets advice that
//! is wrong in the same direction, and no amount of analysis here would catch
//! it. [`AttemptAdvice::SimilarFailure`] exists precisely so that "the recorder
//! said nothing about what would unblock this" is reported as its own answer
//! rather than being rounded to either a hard block or a clean slate.
//!
//! # Advisory, not a gate
//!
//! Nothing here rejects anything. The ledger informs a planner's search; a
//! [`AttemptAdvice::KnownFailure`] is a strong reason to pick a different
//! branch, not a prohibition. Blocking belongs to `car-engine`'s admission
//! gates and to [`crate::verifier`], which have the authority model for it.
//! Keeping this advisory is what lets it be stored, replayed, and shared across
//! sessions without becoming a way to permanently wedge an agent.
//!
//! # Verified exclusions
//!
//! Not every recorded failure carries the same weight. A failure backed by a
//! verifier with the authority to decide has *foreclosed* a route; a failure
//! backed by nothing, or by an advisory opinion, is a note about one bad
//! afternoon. [`Attempt::verdicts`] carries the [`VerifierVerdict`]s that
//! decided the outcome, and [`Attempt::is_verified_exclusion`] distinguishes the
//! two — mirroring [`crate::verifier::admit`], where an advisory failure
//! records without rejecting.
//!
//! That distinction is what makes a retained failure *citable*. A route
//! abandoned on evidence and a route abandoned on vibes are indistinguishable
//! in the artifact, so a system that treats them alike cannot tell a pivot from
//! a rationalisation. [`AttemptLedger::verified_exclusions`] enumerates the
//! citable ones, which is the input a future contract amendment names as its
//! justification for changing the objective.

use crate::verifier::VerifierVerdict;
use serde::{Deserialize, Serialize};
use std::collections::BTreeSet;

/// Why an attempt failed, coarsely enough to be worth matching on.
///
/// The classes are chosen so that a planner can tell "this route is wrong" from
/// "this route was fine and the world got in the way" — the distinction that
/// decides whether retrying is pointless or merely premature.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum FailureClass {
    /// A precondition did not hold — the plan was infeasible from the state it
    /// started in.
    Precondition,
    /// Policy, permission, or the intent gate refused it. Retrying without a
    /// policy change is pointless by construction.
    Policy,
    /// A tool ran and returned an error.
    ToolError,
    /// A tool or the loop exceeded its time bound.
    Timeout,
    /// A cost, token, or iteration budget was exhausted. Says nothing about
    /// whether the approach was sound.
    Budget,
    /// A verifier rejected the result — the work was done and found wrong.
    Verification,
    /// The loop ran to completion without the goal condition holding.
    GoalUnmet,
    /// Anything else. Present so a caller is never forced to mis-classify;
    /// a ledger full of `Unknown` is a signal the recorder needs attention.
    Unknown,
}

impl FailureClass {
    /// Stable lowercase label, matching the serde representation.
    ///
    /// Matched exhaustively on purpose (project convention #2): a new class
    /// must fail to compile here rather than silently acquire a label.
    pub const fn as_str(&self) -> &'static str {
        match self {
            FailureClass::Precondition => "precondition",
            FailureClass::Policy => "policy",
            FailureClass::ToolError => "tool_error",
            FailureClass::Timeout => "timeout",
            FailureClass::Budget => "budget",
            FailureClass::Verification => "verification",
            FailureClass::GoalUnmet => "goal_unmet",
            FailureClass::Unknown => "unknown",
        }
    }
}

/// How an attempt ended.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
#[serde(tag = "outcome", rename_all = "snake_case")]
pub enum AttemptOutcome {
    /// The approach worked.
    Succeeded,
    /// The approach did not work.
    Failed {
        /// Why, coarsely.
        class: FailureClass,
        /// Why, in prose — the error text, the failing verifier, the unmet
        /// precondition.
        #[serde(default)]
        detail: String,
    },
}

impl AttemptOutcome {
    /// Convenience constructor for the common failing case.
    pub fn failed(class: FailureClass, detail: impl Into<String>) -> Self {
        AttemptOutcome::Failed {
            class,
            detail: detail.into(),
        }
    }

    /// Whether this outcome is a failure.
    pub const fn is_failure(&self) -> bool {
        matches!(self, AttemptOutcome::Failed { .. })
    }
}

/// One recorded attempt at a sub-goal.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub struct Attempt {
    /// Stable identity of this record, for citation in advice and logs.
    pub id: String,
    /// The strategy tried, as a caller-chosen label. Compared after
    /// normalisation (trimmed, lowercased, inner whitespace collapsed), so
    /// incidental formatting does not fork the ledger — but see the module
    /// docs: this is not semantic matching.
    pub approach: String,
    /// What was believed true when the approach was chosen. Compared as a set,
    /// so ordering and duplicates do not matter.
    #[serde(default)]
    pub assumptions: Vec<String>,
    /// How it ended.
    pub outcome: AttemptOutcome,
    /// References to supporting material — a trajectory id, a log path, an
    /// error artifact. Opaque to this module.
    #[serde(default)]
    pub evidence: Vec<String>,
    /// The verifier verdicts that decided this outcome.
    ///
    /// A failure carrying a [`crate::VerifierOutcome::Fail`] from a verifier
    /// whose authority can decide is a **verified exclusion** — the route is
    /// foreclosed on evidence, and citable as such. A failure carrying nothing,
    /// or only advisory opinions, is retained but not citable. See
    /// [`Attempt::is_verified_exclusion`].
    ///
    /// Distinct from `evidence`, which is opaque references; these are
    /// structured verdicts that fold into a
    /// [`VerificationEvidence`](crate::VerificationEvidence) bundle via
    /// [`VerifierVerdict::to_check_record`].
    #[serde(default)]
    pub verdicts: Vec<VerifierVerdict>,
    /// Assumptions whose change would make a retry worthwhile.
    ///
    /// The recorder's declaration of what the failure actually depended on.
    /// Empty means no claim was made, which
    /// [`AttemptLedger::consult`] reports as
    /// [`AttemptAdvice::SimilarFailure`] rather than guessing. Ignored on a
    /// [`AttemptOutcome::Succeeded`] record.
    #[serde(default)]
    pub retry_when: Vec<String>,
}

impl Attempt {
    /// A failed attempt with no declared retry condition.
    pub fn failure(
        id: impl Into<String>,
        approach: impl Into<String>,
        assumptions: impl IntoIterator<Item = String>,
        class: FailureClass,
        detail: impl Into<String>,
    ) -> Self {
        Self {
            id: id.into(),
            approach: approach.into(),
            assumptions: assumptions.into_iter().collect(),
            outcome: AttemptOutcome::failed(class, detail),
            evidence: Vec::new(),
            verdicts: Vec::new(),
            retry_when: Vec::new(),
        }
    }

    /// A successful attempt.
    pub fn success(
        id: impl Into<String>,
        approach: impl Into<String>,
        assumptions: impl IntoIterator<Item = String>,
    ) -> Self {
        Self {
            id: id.into(),
            approach: approach.into(),
            assumptions: assumptions.into_iter().collect(),
            outcome: AttemptOutcome::Succeeded,
            evidence: Vec::new(),
            verdicts: Vec::new(),
            retry_when: Vec::new(),
        }
    }

    /// Declare which assumptions would unblock a retry.
    pub fn retry_when(mut self, keys: impl IntoIterator<Item = String>) -> Self {
        self.retry_when = keys.into_iter().collect();
        self
    }

    /// Attach supporting-material references.
    pub fn with_evidence(mut self, refs: impl IntoIterator<Item = String>) -> Self {
        self.evidence = refs.into_iter().collect();
        self
    }

    /// Attach the verifier verdicts that decided this outcome.
    pub fn with_verdicts(mut self, verdicts: impl IntoIterator<Item = VerifierVerdict>) -> Self {
        self.verdicts = verdicts.into_iter().collect();
        self
    }

    /// Whether this attempt forecloses its route **on evidence**.
    ///
    /// True when the attempt failed *and* at least one attached verdict is a
    /// failure from a verifier whose authority can decide
    /// ([`crate::VerifierAuthority::can_satisfy`]). An advisory failure — a
    /// model judge, a linter, a similarity score — does not foreclose a route,
    /// exactly as it does not reject in [`crate::verifier::admit`].
    ///
    /// This is the predicate that separates a citable exclusion from an
    /// anecdote. A pivot justified by a non-verified failure is
    /// indistinguishable from a rationalisation, so callers building a case for
    /// changing an objective should cite only attempts that satisfy this.
    pub fn is_verified_exclusion(&self) -> bool {
        self.outcome.is_failure()
            && self.verdicts.iter().any(|v| {
                v.outcome == crate::VerifierOutcome::Fail && v.verifier.authority.can_satisfy()
            })
    }

    /// The assumption set, normalised for comparison.
    fn assumption_set(&self) -> BTreeSet<String> {
        self.assumptions.iter().map(|a| normalize(a)).collect()
    }
}

/// A route foreclosed on evidence — the citable unit a contract amendment names
/// when justifying a change of objective.
///
/// Borrowed from the ledger rather than cloned: an exclusion is a *view* of a
/// retained attempt, and copying it would invite a caller to build a parallel
/// record that can drift from the ledger it came from.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Exclusion<'a> {
    /// The retained attempt.
    pub attempt: &'a Attempt,
    /// Its failure class, lifted for convenience.
    pub class: FailureClass,
    /// The deciding verdicts — those that failed with authority to decide.
    /// Advisory verdicts attached to the same attempt are deliberately omitted;
    /// they are visible on `attempt.verdicts` if a caller wants them.
    pub deciding: Vec<&'a VerifierVerdict>,
}

/// Trim, lowercase, and collapse inner whitespace, so that incidental
/// formatting does not fork the ledger.
fn normalize(s: &str) -> String {
    s.split_whitespace()
        .collect::<Vec<_>>()
        .join(" ")
        .to_lowercase()
}

/// What the ledger has to say about a proposed approach.
///
/// The variants are ordered by how much they should move a planner: a
/// [`AttemptAdvice::KnownSuccess`] or [`AttemptAdvice::KnownFailure`] is a
/// decided answer for the exact situation asked about, whereas
/// [`AttemptAdvice::SimilarFailure`] is a caution and
/// [`AttemptAdvice::RetryUnblocked`] is an invitation.
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(tag = "advice", rename_all = "snake_case")]
pub enum AttemptAdvice {
    /// Nothing in the ledger matches this approach. No information either way.
    Untried,
    /// This exact approach, under this exact assumption set, has succeeded
    /// before.
    KnownSuccess {
        /// The matching record's id.
        attempt_id: String,
    },
    /// This exact approach, under this exact assumption set, has failed before
    /// and nothing has changed.
    ///
    /// The strongest "pick a different branch" signal the ledger produces.
    KnownFailure {
        /// The most recently recorded matching failure.
        attempt_id: String,
        /// Its class.
        class: FailureClass,
        /// Its detail text.
        detail: String,
        /// Whether that failure is a [verified
        /// exclusion](Attempt::is_verified_exclusion) — foreclosed on evidence
        /// rather than merely recorded.
        ///
        /// A planner should weight these very differently. `verified: false`
        /// means "we tried this and it did not work, and nothing checked why";
        /// `verified: true` means a verifier with authority to decide said no.
        verified: bool,
        /// How many recorded failures match exactly. Repetition is itself
        /// evidence — a planner circling a dead end shows up here as a rising
        /// count.
        occurrences: usize,
    },
    /// This approach failed before, and an assumption the recorder named in
    /// [`Attempt::retry_when`] has since changed. Worth trying again.
    RetryUnblocked {
        /// The failure this clears.
        attempt_id: String,
        /// The declared assumptions that differ now, sorted.
        changed: Vec<String>,
    },
    /// This approach failed before under *different* assumptions, and the
    /// recorder declared no retry condition.
    ///
    /// Deliberately distinct from [`AttemptAdvice::KnownFailure`]: the ledger
    /// has relevant history but no basis for deciding whether the difference
    /// matters. A planner may proceed; it should weight this against the cost
    /// of the attempt.
    SimilarFailure {
        /// The most recently recorded failure of the same approach.
        attempt_id: String,
        /// Its class.
        class: FailureClass,
        /// Assumptions that differ between then and now, sorted.
        differing: Vec<String>,
    },
}

/// An append-only record of what has been tried.
///
/// Pure and in-memory; persistence is the caller's. The natural durable home is
/// alongside `car_memgine`'s trajectory store, which already writes append-only
/// JSONL and already holds the traces an [`Attempt::evidence`] entry would cite
/// — but keeping the decision procedure here means a planner can consult a
/// ledger it assembled from any source, including one replayed from an oplog.
#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct AttemptLedger {
    /// Records in insertion order. Later records take precedence in advice,
    /// which is what makes the ledger reflect the most recent knowledge.
    attempts: Vec<Attempt>,
}

impl AttemptLedger {
    /// An empty ledger.
    pub fn new() -> Self {
        Self::default()
    }

    /// Build a ledger from existing records, preserving their order.
    pub fn from_attempts(attempts: impl IntoIterator<Item = Attempt>) -> Self {
        Self {
            attempts: attempts.into_iter().collect(),
        }
    }

    /// Append a record.
    pub fn record(&mut self, attempt: Attempt) {
        self.attempts.push(attempt);
    }

    /// Every record, in insertion order.
    pub fn attempts(&self) -> &[Attempt] {
        &self.attempts
    }

    /// How many records the ledger holds.
    pub fn len(&self) -> usize {
        self.attempts.len()
    }

    /// Whether the ledger is empty.
    pub fn is_empty(&self) -> bool {
        self.attempts.is_empty()
    }

    /// Every route foreclosed on evidence, in insertion order.
    ///
    /// These are the failures a caller may legitimately *cite* — when
    /// justifying a pivot, when explaining why a branch was abandoned, or when
    /// assembling the record that a reviewer inspects. Failures that were
    /// merely recorded, or that carry only advisory verdicts, are excluded;
    /// they remain in [`AttemptLedger::attempts`] and still steer
    /// [`AttemptLedger::consult`], but they are not evidence.
    ///
    /// The distinction is the whole point. A pivot backed by "we tried and it
    /// felt wrong" and a pivot backed by a failing verifier read identically
    /// once written into prose, so the ledger keeps them apart in the data.
    pub fn verified_exclusions(&self) -> Vec<Exclusion<'_>> {
        self.attempts
            .iter()
            .filter(|a| a.is_verified_exclusion())
            .map(|a| Exclusion {
                attempt: a,
                class: match &a.outcome {
                    AttemptOutcome::Failed { class, .. } => *class,
                    // Unreachable: is_verified_exclusion() requires a failure.
                    // Exhaustive rather than a wildcard so a new variant fails
                    // to compile here.
                    AttemptOutcome::Succeeded => FailureClass::Unknown,
                },
                deciding: a
                    .verdicts
                    .iter()
                    .filter(|v| {
                        v.outcome == crate::VerifierOutcome::Fail
                            && v.verifier.authority.can_satisfy()
                    })
                    .collect(),
            })
            .collect()
    }

    /// Ask what is known about trying `approach` under `assumptions`.
    ///
    /// A decision procedure over the recorded labels — total, deterministic,
    /// and order-stable. Resolution, in precedence order:
    ///
    /// 1. **Exact match** (same normalised approach, same assumption set).
    ///    The most recent such record decides: success →
    ///    [`AttemptAdvice::KnownSuccess`], failure →
    ///    [`AttemptAdvice::KnownFailure`] carrying the count of exact-match
    ///    failures. Precedence goes to the most recent record because the
    ///    ledger is a history, not a tally: an approach that failed twice and
    ///    then succeeded is available, and reporting it as a known failure
    ///    would strand the planner on stale evidence.
    /// 2. **Declared retry condition satisfied** — same approach, and an
    ///    assumption the recorder named in [`Attempt::retry_when`] differs
    ///    between then and now → [`AttemptAdvice::RetryUnblocked`].
    /// 3. **Same approach, different assumptions, nothing declared** →
    ///    [`AttemptAdvice::SimilarFailure`].
    /// 4. **No match** → [`AttemptAdvice::Untried`].
    ///
    /// Only failures are considered at steps 2 and 3; a success under different
    /// assumptions is not evidence that the approach works under these, and
    /// reporting it as though it were is the error this whole module exists to
    /// prevent in the other direction.
    ///
    /// # Examples
    ///
    /// ```
    /// use car_verify::{Attempt, AttemptAdvice, AttemptLedger, FailureClass};
    ///
    /// let mut ledger = AttemptLedger::new();
    /// ledger.record(
    ///     Attempt::failure("a1", "retry upload with backoff",
    ///                      ["endpoint is v1".into(), "token is valid".into()],
    ///                      FailureClass::ToolError, "503 from the endpoint")
    ///         .retry_when(["endpoint is v1".into()]),
    /// );
    ///
    /// // Same assumptions — a decided dead end.
    /// assert!(matches!(
    ///     ledger.consult("retry upload with backoff", ["endpoint is v1", "token is valid"]),
    ///     AttemptAdvice::KnownFailure { .. }
    /// ));
    ///
    /// // The declared retry condition changed — worth trying again.
    /// assert!(matches!(
    ///     ledger.consult("retry upload with backoff", ["endpoint is v2", "token is valid"]),
    ///     AttemptAdvice::RetryUnblocked { .. }
    /// ));
    ///
    /// // An approach never recorded is reported honestly, not guessed at.
    /// assert_eq!(
    ///     ledger.consult("upload via the batch api", ["endpoint is v1"]),
    ///     AttemptAdvice::Untried
    /// );
    /// ```
    pub fn consult<'a>(
        &self,
        approach: &str,
        assumptions: impl IntoIterator<Item = &'a str>,
    ) -> AttemptAdvice {
        let approach_key = normalize(approach);
        let now: BTreeSet<String> = assumptions.into_iter().map(normalize).collect();

        let same_approach: Vec<&Attempt> = self
            .attempts
            .iter()
            .filter(|a| normalize(&a.approach) == approach_key)
            .collect();
        if same_approach.is_empty() {
            return AttemptAdvice::Untried;
        }

        // 1. Exact match — most recent record decides.
        let exact: Vec<&&Attempt> = same_approach
            .iter()
            .filter(|a| a.assumption_set() == now)
            .collect();
        if let Some(latest) = exact.last() {
            return match &latest.outcome {
                AttemptOutcome::Succeeded => AttemptAdvice::KnownSuccess {
                    attempt_id: latest.id.clone(),
                },
                AttemptOutcome::Failed { class, detail } => AttemptAdvice::KnownFailure {
                    attempt_id: latest.id.clone(),
                    class: *class,
                    detail: detail.clone(),
                    verified: latest.is_verified_exclusion(),
                    occurrences: exact.iter().filter(|a| a.outcome.is_failure()).count(),
                },
            };
        }

        // 2 & 3 consider prior failures only, most recent first.
        let failures: Vec<&&Attempt> = same_approach
            .iter()
            .filter(|a| a.outcome.is_failure())
            .collect();

        // 2. A declared retry condition has changed.
        for prior in failures.iter().rev() {
            let then = prior.assumption_set();
            let changed: Vec<String> = prior
                .retry_when
                .iter()
                .map(|k| normalize(k))
                .filter(|k| then.contains(k) != now.contains(k))
                .collect::<BTreeSet<_>>()
                .into_iter()
                .collect();
            if !changed.is_empty() {
                return AttemptAdvice::RetryUnblocked {
                    attempt_id: prior.id.clone(),
                    changed,
                };
            }
        }

        // 3. Relevant history, no basis to decide.
        if let Some(prior) = failures.last() {
            let then = prior.assumption_set();
            let differing: Vec<String> = then.symmetric_difference(&now).cloned().collect();
            let class = match &prior.outcome {
                AttemptOutcome::Failed { class, .. } => *class,
                // Unreachable: `failures` is filtered to failures. Kept as an
                // exhaustive match rather than a wildcard so a new
                // `AttemptOutcome` variant fails to compile here.
                AttemptOutcome::Succeeded => FailureClass::Unknown,
            };
            return AttemptAdvice::SimilarFailure {
                attempt_id: prior.id.clone(),
                class,
                differing,
            };
        }

        AttemptAdvice::Untried
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    fn assumptions(items: &[&str]) -> Vec<String> {
        items.iter().map(|s| s.to_string()).collect()
    }

    fn ledger_with_one_failure() -> AttemptLedger {
        AttemptLedger::from_attempts([Attempt::failure(
            "a1",
            "retry upload with backoff",
            assumptions(&["endpoint is v1", "token is valid"]),
            FailureClass::ToolError,
            "503 from the upload endpoint",
        )])
    }

    #[test]
    fn empty_ledger_reports_untried() {
        let l = AttemptLedger::new();
        assert!(l.is_empty());
        assert_eq!(l.consult("anything", ["x"]), AttemptAdvice::Untried);
    }

    #[test]
    fn exact_match_reports_known_failure_with_its_class_and_detail() {
        let l = ledger_with_one_failure();
        let advice = l.consult(
            "retry upload with backoff",
            ["endpoint is v1", "token is valid"],
        );
        match advice {
            AttemptAdvice::KnownFailure {
                attempt_id,
                class,
                detail,
                verified,
                occurrences,
            } => {
                assert_eq!(attempt_id, "a1");
                assert_eq!(class, FailureClass::ToolError);
                assert_eq!(detail, "503 from the upload endpoint");
                assert!(!verified, "no verdicts attached, so not citable");
                assert_eq!(occurrences, 1);
            }
            other => panic!("expected KnownFailure, got {other:?}"),
        }
    }

    #[test]
    fn assumption_order_and_duplicates_do_not_matter() {
        let l = ledger_with_one_failure();
        let advice = l.consult(
            "retry upload with backoff",
            ["token is valid", "endpoint is v1", "token is valid"],
        );
        assert!(matches!(advice, AttemptAdvice::KnownFailure { .. }));
    }

    #[test]
    fn approach_matching_ignores_case_and_incidental_whitespace() {
        let l = ledger_with_one_failure();
        let advice = l.consult(
            "  Retry  Upload   With Backoff ",
            ["endpoint is v1", "token is valid"],
        );
        assert!(matches!(advice, AttemptAdvice::KnownFailure { .. }));
    }

    #[test]
    fn a_different_approach_is_untried() {
        let l = ledger_with_one_failure();
        assert_eq!(
            l.consult("upload via the batch api", ["endpoint is v1"]),
            AttemptAdvice::Untried
        );
    }

    #[test]
    fn repeated_identical_failures_raise_the_occurrence_count() {
        let mut l = ledger_with_one_failure();
        l.record(Attempt::failure(
            "a2",
            "retry upload with backoff",
            assumptions(&["endpoint is v1", "token is valid"]),
            FailureClass::ToolError,
            "503 again",
        ));
        match l.consult(
            "retry upload with backoff",
            ["endpoint is v1", "token is valid"],
        ) {
            AttemptAdvice::KnownFailure {
                attempt_id,
                occurrences,
                detail,
                ..
            } => {
                assert_eq!(occurrences, 2);
                // Most recent record decides the cited detail.
                assert_eq!(attempt_id, "a2");
                assert_eq!(detail, "503 again");
            }
            other => panic!("expected KnownFailure, got {other:?}"),
        }
    }

    #[test]
    fn a_later_success_supersedes_earlier_failures() {
        // The ledger is a history, not a tally.
        let mut l = ledger_with_one_failure();
        l.record(Attempt::success(
            "a2",
            "retry upload with backoff",
            assumptions(&["endpoint is v1", "token is valid"]),
        ));
        assert_eq!(
            l.consult(
                "retry upload with backoff",
                ["endpoint is v1", "token is valid"]
            ),
            AttemptAdvice::KnownSuccess {
                attempt_id: "a2".into()
            }
        );
    }

    #[test]
    fn declared_retry_condition_unblocks_when_it_changes() {
        let l = AttemptLedger::from_attempts([Attempt::failure(
            "a1",
            "retry upload with backoff",
            assumptions(&["endpoint is v1", "token is valid"]),
            FailureClass::ToolError,
            "503",
        )
        .retry_when(assumptions(&["endpoint is v1"]))]);

        match l.consult(
            "retry upload with backoff",
            ["endpoint is v2", "token is valid"],
        ) {
            AttemptAdvice::RetryUnblocked {
                attempt_id,
                changed,
            } => {
                assert_eq!(attempt_id, "a1");
                assert_eq!(changed, vec!["endpoint is v1".to_string()]);
            }
            other => panic!("expected RetryUnblocked, got {other:?}"),
        }
    }

    #[test]
    fn a_declared_condition_that_did_not_change_does_not_unblock() {
        // "token is valid" is still held; the declared condition is unchanged,
        // so the differing assumption is reported as a caution instead.
        let l = AttemptLedger::from_attempts([Attempt::failure(
            "a1",
            "retry upload with backoff",
            assumptions(&["endpoint is v1", "token is valid"]),
            FailureClass::Policy,
            "denied",
        )
        .retry_when(assumptions(&["token is valid"]))]);

        match l.consult(
            "retry upload with backoff",
            ["endpoint is v1", "token is valid", "region is eu"],
        ) {
            AttemptAdvice::SimilarFailure {
                attempt_id,
                class,
                differing,
            } => {
                assert_eq!(attempt_id, "a1");
                assert_eq!(class, FailureClass::Policy);
                assert_eq!(differing, vec!["region is eu".to_string()]);
            }
            other => panic!("expected SimilarFailure, got {other:?}"),
        }
    }

    #[test]
    fn exact_match_outranks_a_retry_condition() {
        // Same approach recorded twice: once matching the query exactly, once
        // with a declared unblock. The exact match is the more specific
        // evidence and must win.
        let l = AttemptLedger::from_attempts([
            Attempt::failure(
                "a1",
                "flush the cache",
                assumptions(&["lock held"]),
                FailureClass::Timeout,
                "timed out",
            )
            .retry_when(assumptions(&["lock held"])),
            Attempt::failure(
                "a2",
                "flush the cache",
                assumptions(&["lock free"]),
                FailureClass::Timeout,
                "timed out again",
            ),
        ]);
        match l.consult("flush the cache", ["lock free"]) {
            AttemptAdvice::KnownFailure { attempt_id, .. } => assert_eq!(attempt_id, "a2"),
            other => panic!("expected KnownFailure, got {other:?}"),
        }
    }

    #[test]
    fn no_declared_condition_yields_similar_failure_not_a_hard_block() {
        let l = ledger_with_one_failure();
        match l.consult(
            "retry upload with backoff",
            ["endpoint is v2", "token is valid"],
        ) {
            AttemptAdvice::SimilarFailure { differing, .. } => {
                assert_eq!(
                    differing,
                    vec!["endpoint is v1".to_string(), "endpoint is v2".to_string()]
                );
            }
            other => panic!("expected SimilarFailure, got {other:?}"),
        }
    }

    #[test]
    fn a_success_under_different_assumptions_is_not_evidence_for_these() {
        let l = AttemptLedger::from_attempts([Attempt::success(
            "a1",
            "flush the cache",
            assumptions(&["lock free"]),
        )]);
        // Relevant history exists, but only a success under other assumptions.
        // Nothing to say — not KnownSuccess.
        assert_eq!(
            l.consult("flush the cache", ["lock held"]),
            AttemptAdvice::Untried
        );
    }

    #[test]
    fn empty_assumption_sets_match_each_other() {
        let l = AttemptLedger::from_attempts([Attempt::failure(
            "a1",
            "just try it",
            [],
            FailureClass::GoalUnmet,
            "no",
        )]);
        let empty: [&str; 0] = [];
        assert!(matches!(
            l.consult("just try it", empty),
            AttemptAdvice::KnownFailure { .. }
        ));
    }

    #[test]
    fn consult_is_deterministic() {
        let l = ledger_with_one_failure();
        let first = l.consult(
            "retry upload with backoff",
            ["token is valid", "endpoint is v1"],
        );
        let second = l.consult(
            "retry upload with backoff",
            ["endpoint is v1", "token is valid"],
        );
        assert_eq!(first, second);
    }

    #[test]
    fn evidence_references_round_trip() {
        let a = Attempt::failure("a1", "x", [], FailureClass::Unknown, "y")
            .with_evidence(assumptions(&["trajectory:abc", "log:/tmp/run.jsonl"]));
        let json = serde_json::to_string(&a).unwrap();
        let back: Attempt = serde_json::from_str(&json).unwrap();
        assert_eq!(back, a);
        assert_eq!(back.evidence.len(), 2);
    }

    #[test]
    fn ledger_round_trips_through_serde() {
        let mut l = ledger_with_one_failure();
        l.record(Attempt::success("a2", "other", assumptions(&["k"])));
        let json = serde_json::to_string(&l).unwrap();
        let back: AttemptLedger = serde_json::from_str(&json).unwrap();
        assert_eq!(back.len(), 2);
        assert_eq!(back.attempts()[1].id, "a2");
    }

    // --- The join with `crate::verifier`: verified exclusions ---

    fn binding_fail() -> VerifierVerdict {
        VerifierVerdict::fail(
            crate::VerifierDescriptor::binding("counterexample_check", "proof"),
            "24-vertex witness disproves the reduction",
        )
    }

    fn advisory_fail() -> VerifierVerdict {
        let mut d = crate::VerifierDescriptor::binding("model_judge", "proof");
        d.authority = crate::VerifierAuthority::Advisory;
        d.tier = crate::EvidenceTier::Heuristic;
        VerifierVerdict::fail(d, "seems wrong")
    }

    #[test]
    fn a_failure_with_a_binding_failing_verdict_is_a_verified_exclusion() {
        let a = Attempt::failure("a1", "reduce via P13", [], FailureClass::Verification, "no")
            .with_verdicts([binding_fail()]);
        assert!(a.is_verified_exclusion());
    }

    #[test]
    fn a_bare_failure_is_not_a_verified_exclusion() {
        let a = Attempt::failure("a1", "reduce via P13", [], FailureClass::Verification, "no");
        assert!(!a.is_verified_exclusion());
    }

    #[test]
    fn an_advisory_failure_does_not_foreclose_a_route() {
        // Mirrors `admit`: an advisory failure records without rejecting.
        let a = Attempt::failure("a1", "reduce via P13", [], FailureClass::Verification, "no")
            .with_verdicts([advisory_fail()]);
        assert!(!a.is_verified_exclusion());
    }

    #[test]
    fn a_success_is_never_an_exclusion_even_carrying_a_failed_verdict() {
        let a = Attempt::success("a1", "reduce via P13", []).with_verdicts([binding_fail()]);
        assert!(!a.is_verified_exclusion());
    }

    #[test]
    fn verified_exclusions_lists_only_citable_failures() {
        let l = AttemptLedger::from_attempts([
            Attempt::failure("a1", "route one", [], FailureClass::Verification, "no")
                .with_verdicts([binding_fail()]),
            Attempt::failure("a2", "route two", [], FailureClass::ToolError, "503"),
            Attempt::failure("a3", "route three", [], FailureClass::Verification, "no")
                .with_verdicts([advisory_fail()]),
            Attempt::success("a4", "route four", []),
        ]);

        let ex = l.verified_exclusions();
        assert_eq!(ex.len(), 1);
        assert_eq!(ex[0].attempt.id, "a1");
        assert_eq!(ex[0].class, FailureClass::Verification);
        assert_eq!(ex[0].deciding.len(), 1);
        assert_eq!(ex[0].deciding[0].verifier.id, "counterexample_check");
    }

    #[test]
    fn deciding_omits_advisory_verdicts_on_the_same_attempt() {
        let l = AttemptLedger::from_attempts([Attempt::failure(
            "a1",
            "route one",
            [],
            FailureClass::Verification,
            "no",
        )
        .with_verdicts([advisory_fail(), binding_fail()])]);

        let ex = l.verified_exclusions();
        assert_eq!(
            ex[0].deciding.len(),
            1,
            "advisory verdict leaked into deciding"
        );
        assert_eq!(ex[0].attempt.verdicts.len(), 2, "both stay on the attempt");
    }

    #[test]
    fn consult_reports_whether_a_known_failure_is_verified() {
        let mut l = AttemptLedger::from_attempts([Attempt::failure(
            "a1",
            "route one",
            [],
            FailureClass::Verification,
            "no",
        )]);
        let empty: [&str; 0] = [];
        match l.consult("route one", empty) {
            AttemptAdvice::KnownFailure { verified, .. } => assert!(!verified),
            other => panic!("expected KnownFailure, got {other:?}"),
        }

        // A later, verified attempt at the same route supersedes it.
        l.record(
            Attempt::failure("a2", "route one", [], FailureClass::Verification, "no")
                .with_verdicts([binding_fail()]),
        );
        match l.consult("route one", empty) {
            AttemptAdvice::KnownFailure {
                verified,
                attempt_id,
                occurrences,
                ..
            } => {
                assert!(verified);
                assert_eq!(attempt_id, "a2");
                assert_eq!(occurrences, 2);
            }
            other => panic!("expected KnownFailure, got {other:?}"),
        }
    }

    #[test]
    fn verdicts_on_an_attempt_fold_into_check_records() {
        // The join in the other direction: a retained failure's verdicts enter
        // the same evidence vocabulary as any built-in check.
        let a = Attempt::failure("a1", "route one", [], FailureClass::Verification, "no")
            .with_verdicts([binding_fail()]);
        let records: Vec<_> = a.verdicts.iter().map(|v| v.to_check_record()).collect();
        assert_eq!(records.len(), 1);
        assert_eq!(records[0].name, "counterexample_check");
        assert_eq!(records[0].findings, 1);
        assert!(records[0].ran);
    }

    #[test]
    fn verdicts_round_trip_through_serde() {
        let a = Attempt::failure("a1", "route one", [], FailureClass::Verification, "no")
            .with_verdicts([binding_fail()]);
        let back: Attempt = serde_json::from_str(&serde_json::to_string(&a).unwrap()).unwrap();
        assert_eq!(back, a);
        assert!(back.is_verified_exclusion());
    }

    #[test]
    fn an_attempt_without_verdicts_still_deserializes_from_older_records() {
        // `verdicts` is #[serde(default)] — a ledger written before the join
        // must still load.
        let json = r#"{"id":"a1","approach":"x","assumptions":[],
                       "outcome":{"outcome":"failed","class":"tool_error","detail":"503"}}"#;
        let a: Attempt = serde_json::from_str(json).unwrap();
        assert!(a.verdicts.is_empty());
        assert!(!a.is_verified_exclusion());
    }

    #[test]
    fn failure_class_labels_match_serde_representation() {
        for class in [
            FailureClass::Precondition,
            FailureClass::Policy,
            FailureClass::ToolError,
            FailureClass::Timeout,
            FailureClass::Budget,
            FailureClass::Verification,
            FailureClass::GoalUnmet,
            FailureClass::Unknown,
        ] {
            assert_eq!(
                serde_json::to_value(class).unwrap(),
                serde_json::json!(class.as_str())
            );
        }
    }
}