//! Aether Claim ledger — Rust side (read/index for Eidos CS2, write-on-invalidate for CS3).
//!
//! Language-neutral contract: `<project>/.aether/schema/claim.schema.json`. This crate
//! mirrors it. Eidos uses it to INDEX claims (CS2) and flip them `proven -> stale` (CS3).
//! It is an OVERLAY: it must never be a dependency of the frozen `eidos-core`.

use std::fs;
use std::path::{Path, PathBuf};
use std::str::FromStr;

use serde::{Deserialize, Serialize};

pub mod file_store;
pub mod store;

pub use file_store::{FileClaimStore, fold};
pub use store::{ClaimFilter, ClaimStore, EventKind, LedgerEvent, StoreError};

#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "lowercase")]
pub enum ClaimStatus {
    Proposed,
    Proven,
    Stale,
    Contradicted,
    Revoked,
}

impl ClaimStatus {
    /// The on-disk/wire label (matches the schema enum and the serde rename).
    pub fn as_str(self) -> &'static str {
        match self {
            ClaimStatus::Proposed => "proposed",
            ClaimStatus::Proven => "proven",
            ClaimStatus::Stale => "stale",
            ClaimStatus::Contradicted => "contradicted",
            ClaimStatus::Revoked => "revoked",
        }
    }

    /// The legal status transitions — the canonical matrix from the seam doc's
    /// LEGAL TRANSITIONS section (both langs MUST agree; pinned by the conformance
    /// fixture `tests/fixtures/transitions/transitions.json`):
    /// `proposed→proven`, `proven→{stale,contradicted}`, `stale→{proven,contradicted}`,
    /// `contradicted→proven`, and `*→revoked`. Everything else is rejected so the
    /// ledger can never record an impossible state change. The last two stale/
    /// contradicted edges are the freshness + self-healing lifecycle (added 2026-06-15:
    /// `stale→contradicted` = reverify failed; `contradicted→proven` = repaired).
    pub fn can_transition_to(self, to: ClaimStatus) -> bool {
        use ClaimStatus::*;
        matches!(
            (self, to),
            (Proposed, Proven)
                | (Proven, Stale)
                | (Proven, Contradicted)
                | (Stale, Proven)
                | (Stale, Contradicted)
                | (Contradicted, Proven)
                | (_, Revoked)
        )
    }
}

impl FromStr for ClaimStatus {
    type Err = String;

    fn from_str(s: &str) -> Result<Self, Self::Err> {
        match s {
            "proposed" => Ok(ClaimStatus::Proposed),
            "proven" => Ok(ClaimStatus::Proven),
            "stale" => Ok(ClaimStatus::Stale),
            "contradicted" => Ok(ClaimStatus::Contradicted),
            "revoked" => Ok(ClaimStatus::Revoked),
            other => Err(format!("unknown claim status: {other}")),
        }
    }
}

/// The kind of a claim. `capability` is the original v1 kind; `health` is minted by
/// Nym (codebase memory) for structural-decay claims. The enum (not a bare `String`)
/// is the H3-lite contract guard.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum ClaimKind {
    Capability,
    Health,
}

impl ClaimKind {
    pub fn as_str(self) -> &'static str {
        match self {
            ClaimKind::Capability => "capability",
            ClaimKind::Health => "health",
        }
    }
}

#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(deny_unknown_fields)]
pub struct EvidenceRef {
    pub kind: String,
    #[serde(rename = "ref")]
    pub reference: String,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub span: Option<String>,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(deny_unknown_fields)]
pub struct ReverifyAction {
    pub argv: Vec<String>,
    #[serde(default)]
    pub expect_exit: i32,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(deny_unknown_fields)]
pub struct Claim {
    pub id: String,
    pub kind: ClaimKind,
    pub subject: String,
    pub statement: String,
    pub status: ClaimStatus,
    #[serde(default)]
    pub evidence_refs: Vec<EvidenceRef>,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub verifier_ref: Option<String>,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub reverify_action: Option<ReverifyAction>,
    #[serde(default)]
    pub invalidated_by: Vec<String>,
    pub created_at: String,
    pub updated_at: String,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub last_verified_at: Option<String>,
}

pub fn aether_dir(project_root: &Path) -> PathBuf {
    project_root.join(".aether")
}

pub fn claims_dir(project_root: &Path) -> PathBuf {
    aether_dir(project_root).join("claims")
}

/// Load every claim under `<project>/.aether/claims/*.json` (sorted, malformed files skipped).
pub fn load_all(project_root: &Path) -> std::io::Result<Vec<Claim>> {
    let dir = claims_dir(project_root);
    let mut out = Vec::new();
    if !dir.exists() {
        return Ok(out);
    }
    let mut paths: Vec<PathBuf> = fs::read_dir(&dir)?
        .filter_map(|e| e.ok().map(|e| e.path()))
        .filter(|p| p.extension().map(|x| x == "json").unwrap_or(false))
        .collect();
    paths.sort();
    for p in paths {
        let txt = fs::read_to_string(&p)?;
        if let Ok(c) = serde_json::from_str::<Claim>(&txt) {
            out.push(c);
        }
    }
    Ok(out)
}

/// Load every claim **folded fresh from the ledger** — the freshness-correct counterpart to
/// [`load_all`] (which returns the raw, possibly-stale `claims/*.json` cache files). This is what
/// the `health`/`vitals` claim breakdown must read: an `invalidate` appends `proven -> stale` to
/// the ledger without rewriting the cache, so counting [`load_all`] would report `proven` for a
/// claim the ledger has already moved to `stale` — the same divergence [`status`]/[`ground_claims`]
/// avoid by folding. Use this anywhere a count must match the read surface.
pub fn load_folded(project_root: &Path) -> std::io::Result<Vec<Claim>> {
    use store::ClaimStore;
    FileClaimStore::new(project_root)
        .list(None)
        .map_err(store_io)
}

pub fn read_claim(project_root: &Path, id: &str) -> std::io::Result<Claim> {
    let p = claims_dir(project_root).join(format!("{id}.json"));
    let txt = fs::read_to_string(p)?;
    serde_json::from_str(&txt).map_err(|e| std::io::Error::new(std::io::ErrorKind::InvalidData, e))
}

/// Persist a claim's current state **atomically** (temp → fsync → rename — never a
/// truncate-in-place `fs::write` on the target, which is the F2 torn-file bug).
/// Timestamps are the caller's responsibility (no time dep in this crate yet).
pub fn write_claim(project_root: &Path, claim: &Claim) -> std::io::Result<PathBuf> {
    let dir = claims_dir(project_root);
    fs::create_dir_all(&dir)?;
    let p = dir.join(format!("{}.json", claim.id));
    let txt = serde_json::to_string_pretty(claim)
        .map_err(|e| std::io::Error::new(std::io::ErrorKind::InvalidData, e))?;
    file_store::atomic_write(&p, format!("{txt}\n").as_bytes())?;
    Ok(p)
}

/// A flat, serializable read-view of a claim — the unit the CS2 read surface (MCP `claims_status`
/// and `eidos claims status`) reports: `id · subject · status · verifier_ref · evidence`.
#[derive(Debug, Clone, Serialize)]
pub struct ClaimSummary {
    pub id: String,
    pub subject: String,
    pub statement: String,
    pub status: ClaimStatus,
    #[serde(skip_serializing_if = "Option::is_none")]
    pub verifier_ref: Option<String>,
    /// Evidence receipts as `"kind:ref"` strings (the grounding-law justifications).
    pub evidence: Vec<String>,
}

impl ClaimSummary {
    pub fn of(c: &Claim) -> Self {
        ClaimSummary {
            id: c.id.clone(),
            subject: c.subject.clone(),
            statement: c.statement.clone(),
            status: c.status,
            verifier_ref: c.verifier_ref.clone(),
            evidence: c
                .evidence_refs
                .iter()
                .map(|e| format!("{}:{}", e.kind, e.reference))
                .collect(),
        }
    }
}

/// True if `query` selects this claim — by exact id/subject, or as a loose substring of either.
/// Lets `eidos claims status skill.using-eidos` (the subject) and the full claim id both work.
fn matches_subject(c: &Claim, query: &str) -> bool {
    c.subject == query || c.id == query || c.subject.contains(query) || c.id.contains(query)
}

/// Near-zero-signal words dropped from both the query and a claim's match surface so they can't be
/// the sole reason a subject query matches. The first row is the structural claim/subject scaffolding
/// (every capability id is `claim.capability.<x>`, every subject `skill.<x>`); the rest mirror the
/// engine's English stopword list. Kept here (not imported) so the overlay never depends on frozen
/// `eidos-core`. SORTED so [`is_claim_stop`] can binary-search it.
const CLAIM_STOP: &[&str] = &[
    "a",
    "an",
    "and",
    "are",
    "as",
    "at",
    "be",
    "but",
    "by",
    "can",
    "capability",
    "claim",
    "did",
    "do",
    "does",
    "for",
    "from",
    "had",
    "has",
    "have",
    "health",
    "how",
    "i",
    "in",
    "is",
    "it",
    "its",
    "me",
    "my",
    "need",
    "of",
    "on",
    "or",
    "our",
    "should",
    "skill",
    "so",
    "that",
    "the",
    "their",
    "them",
    "then",
    "there",
    "these",
    "this",
    "those",
    "to",
    "up",
    "us",
    "was",
    "we",
    "were",
    "what",
    "when",
    "where",
    "which",
    "will",
    "with",
    "would",
    "you",
    "your",
];

fn is_claim_stop(t: &str) -> bool {
    CLAIM_STOP.binary_search(&t).is_ok()
}

/// Lowercase alphanumeric tokens of `s`, minus stop/scaffolding words — the deterministic,
/// no-ML match surface for the ground-time claim overlay. Splits on word boundaries so a hyphenated
/// subject (`skill.using-eidos`) yields `using` + `eidos` and matches a query like "using-eidos".
fn claim_terms(s: &str) -> std::collections::BTreeSet<String> {
    s.to_lowercase()
        .split(|c: char| !c.is_alphanumeric())
        .filter(|t| t.chars().count() > 1 && !is_claim_stop(t))
        .map(str::to_string)
        .collect()
}

/// CS2 ground-overlay: the capability-claims whose subject / id / statement lexically overlap
/// `query`, ranked by overlap count (desc) then id (asc, for a stable order), capped at `limit`.
/// This is what lets `ground("is using-eidos proven")` surface `claim.capability.using-eidos`
/// with its status + evidence receipts ALONGSIDE the code/doc hits — the grounding-law answer to
/// "what do we believe about `<subject>`, and what's the proof?". Empty when nothing overlaps
/// (the brain being honest, not broken). Reuses the read engine's spirit, not frozen core.
pub fn ground_claims(
    project_root: &Path,
    query: &str,
    limit: usize,
) -> std::io::Result<Vec<ClaimSummary>> {
    let q = claim_terms(query);
    if q.is_empty() {
        return Ok(Vec::new());
    }
    // Fold-on-read here too, so grounding never surfaces a claim as `proven` after the ledger
    // has moved it to `stale`/`contradicted` (same divergence the read surface must not show).
    let mut scored: Vec<(usize, Claim)> = FileClaimStore::new(project_root)
        .list(None)
        .map_err(store_io)?
        .into_iter()
        .filter_map(|c| {
            let mut hay = claim_terms(&c.subject);
            hay.extend(claim_terms(&c.id));
            hay.extend(claim_terms(&c.statement));
            let overlap = q.iter().filter(|t| hay.contains(*t)).count();
            (overlap > 0).then_some((overlap, c))
        })
        .collect();
    scored.sort_by(|a, b| b.0.cmp(&a.0).then_with(|| a.1.id.cmp(&b.1.id)));
    Ok(scored
        .into_iter()
        .take(limit)
        .map(|(_, c)| ClaimSummary::of(&c))
        .collect())
}

/// CS2 read surface: load the claims under `<project>/.aether/claims/`, optionally filtered to a
/// subject (or claim id), and return their summaries. The grounding-law answer to
/// "is `<subject>` proven, and what's the receipt?".
pub fn status(project_root: &Path, subject: Option<&str>) -> std::io::Result<Vec<ClaimSummary>> {
    // Fold the ledger (via the store), NOT a raw `load_all`: the read surface must report what the
    // ledger says, not a derived-cache file that an `invalidate` may have left as a stale `proven`.
    let claims = FileClaimStore::new(project_root)
        .list(None)
        .map_err(store_io)?;
    Ok(claims
        .iter()
        .filter(|c| subject.is_none_or(|s| matches_subject(c, s)))
        .map(ClaimSummary::of)
        .collect())
}

/// Tally claims by status label — the `health` claim-count breakdown.
pub fn count_by_status(claims: &[Claim]) -> std::collections::BTreeMap<String, usize> {
    let mut counts = std::collections::BTreeMap::new();
    for c in claims {
        *counts.entry(c.status.as_str().to_string()).or_default() += 1;
    }
    counts
}

/// Walk UP from `start` to the nearest ancestor that contains a `.aether/` directory — the Aether
/// project root. Lets the read surface find claims from any subdirectory (the LSP/git model).
pub fn find_root(start: &Path) -> Option<PathBuf> {
    start
        .ancestors()
        .find(|d| d.join(".aether").is_dir())
        .map(|d| d.to_path_buf())
}

// ── CS3: freshness = justification propagation ──────────────────────────────────────────────────

/// One `proven -> stale` transition produced by [`invalidate`].
#[derive(Debug, Clone, Serialize)]
pub struct Invalidation {
    pub claim_id: String,
    pub from: ClaimStatus,
    pub to: ClaimStatus,
    /// The changed path that retracted the justification.
    pub changed: String,
}

/// The evidence paths a claim's truth depends on: its derived `invalidated_by` set, or (when that
/// is empty) the `file`/`check`/`test` evidence refs. Changing one of these retracts a justification.
pub fn watched_paths(c: &Claim) -> Vec<String> {
    if !c.invalidated_by.is_empty() {
        return c.invalidated_by.clone();
    }
    c.evidence_refs
        .iter()
        .filter(|e| matches!(e.kind.as_str(), "file" | "check" | "test"))
        .map(|e| e.reference.clone())
        .collect()
}

fn path_components(s: &str) -> Vec<&str> {
    s.split(['/', '\\'])
        .filter(|c| !c.is_empty() && *c != ".")
        .collect()
}

/// Component-wise suffix match: true when one path is a trailing-component run of the other. This
/// tolerates absolute vs project-relative vs bare-suffix forms without the `ab.md`~`b.md` false hit
/// that naive `ends_with` on strings would give.
fn paths_overlap(a: &str, b: &str) -> bool {
    let (a, b) = (path_components(a), path_components(b));
    let (short, long) = if a.len() <= b.len() {
        (&a, &b)
    } else {
        (&b, &a)
    };
    !short.is_empty() && long[long.len() - short.len()..] == short[..]
}

pub fn ledger_path(project_root: &Path) -> PathBuf {
    aether_dir(project_root).join("ledger.jsonl")
}

/// Append one JSONL event to `<project>/.aether/ledger.jsonl` (the append-only spine).
pub fn append_ledger(project_root: &Path, event: &serde_json::Value) -> std::io::Result<()> {
    use std::io::Write;
    fs::create_dir_all(aether_dir(project_root))?;
    let line = serde_json::to_string(event)
        .map_err(|e| std::io::Error::new(std::io::ErrorKind::InvalidData, e))?;
    let mut f = fs::OpenOptions::new()
        .create(true)
        .append(true)
        .open(ledger_path(project_root))?;
    writeln!(f, "{line}")
}

/// CS3 — freshness by justification propagation. Flip every **proven** claim whose watched evidence
/// touches one of `changed` to `stale`, persist it (bumping `updated_at` to `now`), and append a
/// `claim_invalidated` event to the ledger. Only trusted (`proven`) claims can go stale; unrelated
/// changes are no-ops. `now` is an RFC3339 stamp from the caller — the crate stays time-free.
/// Returns what was flipped (empty ⇒ nothing trusted depended on those files). This is
/// reason-maintenance, NOT a timer.
pub fn invalidate(
    project_root: &Path,
    changed: &[String],
    now: &str,
) -> std::io::Result<Vec<Invalidation>> {
    let now = now.to_string();
    let store = FileClaimStore::with_clock(project_root, move || now.clone());
    // Append-only: the ledger gets the `proven -> stale` event; the `claims/*.json` cache is NOT
    // rewritten here (that stays the explicit `materialize()` path). Correctness for readers comes
    // from folding on read — see `status` / `ground_claims`.
    invalidate_with_store(&store, changed).map_err(store_io)
}

/// Collapse a [`StoreError`] into `io::Error` for the `io`-typed public read/write helpers.
fn store_io(e: StoreError) -> std::io::Error {
    match e {
        StoreError::Io(io) => io,
        other => std::io::Error::other(other.to_string()),
    }
}

/// The seam version of [`invalidate`]: compute the affected **proven** claims and
/// flip each `proven → stale` through `store.transition` — ONE append-only call per
/// flip. No direct `write_claim`/`append_ledger`; the store owns validate + append,
/// and readers fold the ledger. This is the H1 single-most-important line in code:
/// Eidos never mutates a `claims/*.json` file as a primary write.
pub fn invalidate_with_store(
    store: &dyn ClaimStore,
    changed: &[String],
) -> Result<Vec<Invalidation>, StoreError> {
    let proven = store.list(Some(ClaimFilter {
        status: Some(ClaimStatus::Proven),
        ..Default::default()
    }))?;
    let mut out = Vec::new();
    for claim in proven {
        let watched = watched_paths(&claim);
        let Some(hit) = changed
            .iter()
            .find(|c| watched.iter().any(|w| paths_overlap(c, w)))
        else {
            continue;
        };
        store.transition(&claim.id, ClaimStatus::Stale, "eidos:invalidate", Some(hit))?;
        out.push(Invalidation {
            claim_id: claim.id,
            from: ClaimStatus::Proven,
            to: ClaimStatus::Stale,
            changed: hit.clone(),
        });
    }
    Ok(out)
}

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

    const EXAMPLE: &str = r#"{
        "id": "claim.capability.example",
        "kind": "capability",
        "subject": "skill.example",
        "statement": "x",
        "status": "proposed",
        "evidence_refs": [{"kind": "file", "ref": "a.md"}],
        "verifier_ref": null,
        "invalidated_by": ["a.md"],
        "created_at": "2026-06-15T00:00:00Z",
        "updated_at": "2026-06-15T00:00:00Z",
        "last_verified_at": null
    }"#;

    #[test]
    fn parses_the_contract() {
        let c: Claim = serde_json::from_str(EXAMPLE).unwrap();
        assert_eq!(c.status, ClaimStatus::Proposed);
        assert_eq!(c.evidence_refs.len(), 1);
        assert_eq!(c.evidence_refs[0].reference, "a.md");
    }

    #[test]
    fn round_trips_through_disk() {
        let tmp = std::env::temp_dir().join(format!("aether-cs0-{}", std::process::id()));
        let mut c: Claim = serde_json::from_str(EXAMPLE).unwrap();
        c.status = ClaimStatus::Stale; // CS3 will do exactly this
        write_claim(&tmp, &c).unwrap();
        let back = read_claim(&tmp, &c.id).unwrap();
        assert_eq!(back.status, ClaimStatus::Stale);
        assert_eq!(load_all(&tmp).unwrap().len(), 1);
        let _ = fs::remove_dir_all(&tmp);
    }

    /// The committed fixture project: `<crate>/tests/fixtures/pi` holds a `.aether/claims/` dir
    /// with the real dogfood capability-claims (using-eidos = proven, telos-gated = proposed).
    fn fixture_root() -> PathBuf {
        PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("tests/fixtures/pi")
    }

    // CS2 RED: before the index existed, the read surface could not answer "is using-eidos proven?"
    // from `.aether/claims/`. `status()` is that surface — it reports id · subject · status ·
    // verifier_ref · evidence for a subject (or all claims when no subject is given).
    #[test]
    fn status_reports_a_capability_claim_from_the_ledger() {
        let summaries = status(&fixture_root(), Some("skill.using-eidos")).unwrap();
        assert_eq!(
            summaries.len(),
            1,
            "subject filter should isolate the one claim"
        );
        let s = &summaries[0];
        assert_eq!(s.id, "claim.capability.using-eidos");
        assert_eq!(s.subject, "skill.using-eidos");
        assert_eq!(s.status, ClaimStatus::Proven);
        assert_eq!(
            s.verifier_ref.as_deref(),
            Some("telos:cs1-prove-using-eidos")
        );
        // evidence receipts are surfaced, not just the verdict (the grounding law).
        assert!(
            s.evidence
                .iter()
                .any(|e| e.contains("skills/using-eidos/SKILL.md"))
        );
    }

    // CS2 ground-overlay RED: a natural-language *subject* query ("can we trust using-eidos")
    // must surface the capability-claim + its status + receipt — the grounding-law answer
    // "what do we believe about <subject>, and what's the proof?". Before `ground_claims`,
    // ground returned only code/doc hits; the claim ledger was invisible to a query.
    #[test]
    fn ground_surfaces_matching_claim_for_a_subject_query() {
        let hits = ground_claims(&fixture_root(), "can we trust using-eidos", 5).unwrap();
        assert!(
            !hits.is_empty(),
            "a subject query must surface the matching claim"
        );
        let top = &hits[0];
        assert_eq!(top.id, "claim.capability.using-eidos");
        assert_eq!(top.status, ClaimStatus::Proven);
        // the receipt rides along, not just the verdict (the grounding law).
        assert!(
            top.evidence
                .iter()
                .any(|e| e.contains("skills/using-eidos/SKILL.md")),
            "evidence receipt surfaced: {:?}",
            top.evidence
        );
        // …and "is using-eidos proven" lands the same claim.
        let q2 = ground_claims(&fixture_root(), "is using-eidos proven", 5).unwrap();
        assert_eq!(
            q2.first().map(|c| c.id.as_str()),
            Some("claim.capability.using-eidos")
        );
    }

    // Precision: a query about an unrelated subject must NOT drag in the using-eidos claim,
    // and the structural id words (skill/claim/capability) must not be the sole match.
    // `is_claim_stop` binary-searches CLAIM_STOP, so the table MUST stay sorted.
    #[test]
    fn claim_stop_table_is_sorted() {
        assert!(
            CLAIM_STOP.windows(2).all(|w| w[0] < w[1]),
            "CLAIM_STOP must be sorted+unique"
        );
    }

    #[test]
    fn ground_claims_does_not_match_unrelated_subjects() {
        let none = ground_claims(&fixture_root(), "render an html graph of the brain", 5).unwrap();
        assert!(
            !none.iter().any(|c| c.id == "claim.capability.using-eidos"),
            "an unrelated subject query must not surface using-eidos: {none:?}"
        );
        // the bare structural word "capability" must not match every claim.
        let structural = ground_claims(&fixture_root(), "capability", 5).unwrap();
        assert!(
            structural.is_empty(),
            "structural id scaffolding must not match: {structural:?}"
        );
    }

    #[test]
    fn status_lists_all_claims_when_no_subject() {
        let all = status(&fixture_root(), None).unwrap();
        assert_eq!(all.len(), 2, "fixture has two capability-claims");
    }

    // health extension: claim counts broken down by status.
    #[test]
    fn counts_claims_by_status() {
        let claims = load_all(&fixture_root()).unwrap();
        let counts = count_by_status(&claims);
        assert_eq!(counts.get("proven"), Some(&1));
        assert_eq!(counts.get("proposed"), Some(&1));
        assert_eq!(counts.get("stale"), None);
    }

    #[test]
    fn find_root_walks_up_to_the_aether_dir() {
        let deep = fixture_root().join(".aether/claims");
        assert_eq!(find_root(&deep), Some(fixture_root()));
        assert_eq!(find_root(Path::new("/")), None);
    }

    /// Stand up a throwaway project with one PROVEN claim watching `skills/using-eidos/SKILL.md`.
    fn proven_in_tmp(tag: &str) -> (PathBuf, Claim) {
        let tmp = std::env::temp_dir().join(format!("aether-{tag}-{}", std::process::id()));
        let _ = fs::remove_dir_all(&tmp);
        let mut c: Claim = serde_json::from_str(EXAMPLE).unwrap();
        c.status = ClaimStatus::Proven;
        c.invalidated_by = vec!["skills/using-eidos/SKILL.md".into()];
        write_claim(&tmp, &c).unwrap();
        (tmp, c)
    }

    // H0a/H1 RED: `invalidate` is now APPEND-ONLY. Touching a file in a proven claim's
    // evidence must (1) leave `claims/<id>.json` BYTE-UNCHANGED — no truncate-in-place
    // direct write — (2) append exactly one `claim_invalidated` ledger line, and (3) the
    // claim must FOLD to `stale` on read. Before this work, invalidate rewrote the file.
    #[test]
    fn invalidate_appends_and_leaves_claim_file_byte_unchanged() {
        let (tmp, c) = proven_in_tmp("h0a-append");
        let claim_path = claims_dir(&tmp).join(format!("{}.json", c.id));
        let before = fs::read(&claim_path).unwrap();
        assert_eq!(
            read_claim(&tmp, &c.id).unwrap().status,
            ClaimStatus::Proven,
            "RED state"
        );

        let flipped = invalidate(
            &tmp,
            &["skills/using-eidos/SKILL.md".to_string()],
            "2026-06-15T12:00:00Z",
        )
        .unwrap();
        assert_eq!(flipped.len(), 1);
        assert_eq!(flipped[0].from, ClaimStatus::Proven);
        assert_eq!(flipped[0].to, ClaimStatus::Stale);

        // (1) the claim file is byte-identical — invalidate never wrote it.
        let after = fs::read(&claim_path).unwrap();
        assert_eq!(
            before, after,
            "invalidate must NOT mutate claims/<id>.json (append-only)"
        );

        // (2) exactly one claim_invalidated line was appended.
        let ledger = fs::read_to_string(ledger_path(&tmp)).unwrap();
        assert_eq!(
            ledger
                .lines()
                .filter(|l| l.contains("\"event\":\"claim_invalidated\""))
                .count(),
            1,
            "exactly one claim_invalidated event appended: {ledger}"
        );
        assert!(
            ledger.contains("\"to\":\"stale\""),
            "event records the transition: {ledger}"
        );

        // (3) reading folds the ledger over the (proven) file → stale.
        let store = FileClaimStore::new(&tmp);
        assert_eq!(
            store.read(&c.id).unwrap().status,
            ClaimStatus::Stale,
            "folds to stale"
        );
        let _ = fs::remove_dir_all(&tmp);
    }

    /// The shared cross-language convergence fixture (copied verbatim from
    /// `~/.pi/.aether/conformance/ledger-fold/`). `materialize()` over this ledger
    /// MUST reproduce `expected-claims.json` exactly — the contract between the Rust
    /// and Python folds (a `claim_proven` payload then a `claim_invalidated`: status
    /// `stale`, `updated_at` bumped, `last_verified_at` PRESERVED, content unchanged).
    #[test]
    fn materialize_reproduces_ledger_fold_fixture() {
        let fixture = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("tests/fixtures/ledger-fold");
        let tmp = std::env::temp_dir().join(format!("aether-foldfix-{}", std::process::id()));
        let _ = fs::remove_dir_all(&tmp);
        fs::create_dir_all(aether_dir(&tmp)).unwrap();
        fs::copy(fixture.join("ledger.jsonl"), ledger_path(&tmp)).unwrap();

        let store = FileClaimStore::new(&tmp);
        let materialized = store.materialize().unwrap();

        let expected: serde_json::Value = serde_json::from_str(
            &fs::read_to_string(fixture.join("expected-claims.json")).unwrap(),
        )
        .unwrap();
        let got = serde_json::to_value(&materialized).unwrap();
        assert_eq!(
            got, expected,
            "fold must reproduce the conformance fixture exactly"
        );

        // …and the cache file written to disk agrees.
        let written = read_claim(&tmp, "claim.capability.foldtest").unwrap();
        assert_eq!(written.status, ClaimStatus::Stale);
        assert_eq!(written.updated_at, "2026-06-15T01:00:00Z");
        assert_eq!(
            written.last_verified_at.as_deref(),
            Some("2026-06-15T00:00:00Z")
        );
        let _ = fs::remove_dir_all(&tmp);
    }

    /// `claims/` is a pure derived cache: delete it, materialize, identical result (F1).
    #[test]
    fn claims_cache_is_rebuildable_from_the_ledger_alone() {
        let fixture = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("tests/fixtures/ledger-fold");
        let tmp = std::env::temp_dir().join(format!("aether-rebuild-{}", std::process::id()));
        let _ = fs::remove_dir_all(&tmp);
        fs::create_dir_all(aether_dir(&tmp)).unwrap();
        fs::copy(fixture.join("ledger.jsonl"), ledger_path(&tmp)).unwrap();

        let store = FileClaimStore::new(&tmp);
        let first = serde_json::to_value(store.materialize().unwrap()).unwrap();
        fs::remove_dir_all(claims_dir(&tmp)).unwrap();
        let second = serde_json::to_value(store.materialize().unwrap()).unwrap();
        assert_eq!(
            first, second,
            "materialize is deterministic from the ledger alone"
        );
        let _ = fs::remove_dir_all(&tmp);
    }

    /// Illegal transitions are rejected before anything is appended.
    #[test]
    fn transition_rejects_illegal_status_changes() {
        let (tmp, c) = proven_in_tmp("h0a-illegal");
        let store = FileClaimStore::new(&tmp);
        // proven → proposed is not a legal edge.
        let err = store.transition(&c.id, ClaimStatus::Proposed, "test", None);
        assert!(
            matches!(err, Err(StoreError::InvalidTransition { .. })),
            "got {err:?}"
        );
        // the ledger must not have grown.
        assert!(
            !ledger_path(&tmp).exists(),
            "rejected transition appends nothing"
        );
        let _ = fs::remove_dir_all(&tmp);
    }

    /// CROSS-LANGUAGE CONFORMANCE: `can_transition_to` MUST match the canonical
    /// matrix in `~/.pi/.aether/conformance/transitions/transitions.json` (vendored)
    /// for ALL status pairs. Veris enforces the identical set in Python — drift here
    /// is a silently-diverging state machine. Source of truth: the seam doc's
    /// LEGAL TRANSITIONS section.
    #[test]
    fn transition_matrix_matches_the_conformance_fixture() {
        let fixture = PathBuf::from(env!("CARGO_MANIFEST_DIR"))
            .join("tests/fixtures/transitions/transitions.json");
        let v: serde_json::Value =
            serde_json::from_str(&fs::read_to_string(&fixture).unwrap()).unwrap();

        let statuses: Vec<ClaimStatus> = v["statuses"]
            .as_array()
            .unwrap()
            .iter()
            .map(|s| s.as_str().unwrap().parse().unwrap())
            .collect();
        let legal: std::collections::HashSet<(String, String)> = v["legal"]
            .as_array()
            .unwrap()
            .iter()
            .map(|p| {
                let a = p[0].as_str().unwrap().to_string();
                let b = p[1].as_str().unwrap().to_string();
                (a, b)
            })
            .collect();

        // every status pair: our matrix must agree with the fixture's legal set.
        for &from in &statuses {
            for &to in &statuses {
                let expected =
                    legal.contains(&(from.as_str().to_string(), to.as_str().to_string()));
                assert_eq!(
                    from.can_transition_to(to),
                    expected,
                    "transition {} -> {} should be {}",
                    from.as_str(),
                    to.as_str(),
                    if expected { "LEGAL" } else { "illegal" }
                );
            }
        }

        // spot-check the two edges added 2026-06-15 (the reason this brick exists).
        assert!(ClaimStatus::Stale.can_transition_to(ClaimStatus::Contradicted));
        assert!(ClaimStatus::Contradicted.can_transition_to(ClaimStatus::Proven));
    }

    // Freshness is justification propagation, not a blunt timer: unrelated changes leave the claim
    // proven, and only TRUSTED (proven) claims can go stale.
    #[test]
    fn invalidate_ignores_unrelated_changes() {
        let (tmp, c) = proven_in_tmp("cs3b");
        let flipped =
            invalidate(&tmp, &["src/main.rs".to_string()], "2026-06-15T12:00:00Z").unwrap();
        assert!(
            flipped.is_empty(),
            "an unrelated file must not retract the justification"
        );
        assert_eq!(read_claim(&tmp, &c.id).unwrap().status, ClaimStatus::Proven);
        // no spurious ledger file/event
        assert!(
            !ledger_path(&tmp).exists()
                || !fs::read_to_string(ledger_path(&tmp))
                    .unwrap()
                    .contains("claim_invalidated")
        );
        let _ = fs::remove_dir_all(&tmp);
    }

    #[test]
    fn watched_paths_falls_back_to_evidence_when_invalidated_by_empty() {
        let mut c: Claim = serde_json::from_str(EXAMPLE).unwrap();
        c.invalidated_by.clear();
        c.evidence_refs = vec![
            EvidenceRef {
                kind: "file".into(),
                reference: "x.md".into(),
                span: None,
            },
            EvidenceRef {
                kind: "telos_task".into(),
                reference: "t.yaml".into(),
                span: None,
            },
        ];
        let w = watched_paths(&c);
        assert_eq!(
            w,
            vec!["x.md".to_string()],
            "telos_task refs are not watched files"
        );
    }
}
