//! Proof schema (SPEC §2–§4) — the content-addressed proof obligation, the
//! cheapest-sufficient tier ladder, the honest energy model, and the `Solver`
//! trait every backend implements.
//!
//! The standard is vendor-neutral: a *goal* is content-addressed, a *solver* is
//! anything that can attempt one at a declared tier, and a closed goal carries
//! the joules it cost with an honest provenance tag. Correctness is never traded
//! for energy — a solver returns `Proved` only when a verifier would accept the
//! artifact.

use serde::{Deserialize, Serialize};

mod cbor;
pub use cbor::canonical_cbor;

/// Errors from canonical serialization / content addressing.
#[derive(Debug, thiserror::Error)]
pub enum SchemaError {
    /// A value contained a type the canonical encoding forbids (float, bool,
    /// null, or a non-uint number).
    #[error("disallowed type in canonical encoding: {0}")]
    DisallowedType(&'static str),
}

/// `blake3` content address of any canonically-serialized value (SPEC §3).
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize)]
pub struct ContentId(pub [u8; 32]);

impl ContentId {
    /// `blake3(canonical_cbor(value))` — the content address of any serializable.
    pub fn of<T: Serialize>(value: &T) -> Result<Self, SchemaError> {
        Ok(Self::of_bytes(&canonical_cbor(value)?))
    }
    /// `blake3(bytes)` — the content address of a raw payload.
    pub fn of_bytes(bytes: &[u8]) -> Self {
        ContentId(*blake3::hash(bytes).as_bytes())
    }
    /// Lowercase hex, the wire form used in receipts.
    pub fn to_hex(self) -> String {
        hex::encode(self.0)
    }
}

/// The solver tiers, cheapest first (SPEC §4). Energy rises by orders of
/// magnitude per rung; the router sends each goal to the cheapest one that can
/// close it and escalates only on failure.
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
pub enum Tier {
    /// T0 — deterministic automation (proof-language tactics): ~free CPU.
    Automation,
    /// T1 — SMT / decision procedures: cheap CPU.
    Smt,
    /// T2 — a small distilled in-domain prover: model, but small.
    SmallModel,
    /// T3 — a frontier reasoning model: the last resort, the most expensive rung.
    BigModel,
}

impl Tier {
    /// The four tiers in cheapest-first order — the canonical ladder.
    pub const LADDER: [Tier; 4] = [
        Tier::Automation,
        Tier::Smt,
        Tier::SmallModel,
        Tier::BigModel,
    ];

    /// The wire tag used in receipts and vectors (`T0`..`T3`).
    pub fn wire_tag(self) -> &'static str {
        match self {
            Tier::Automation => "T0",
            Tier::Smt => "T1",
            Tier::SmallModel => "T2",
            Tier::BigModel => "T3",
        }
    }

    /// A short human label (`T0:automation`, …).
    pub fn label(self) -> &'static str {
        match self {
            Tier::Automation => "T0:automation",
            Tier::Smt => "T1:smt",
            Tier::SmallModel => "T2:small-model",
            Tier::BigModel => "T3:big-model",
        }
    }

    /// The reference per-tier energy estimator, microjoules (non-normative,
    /// SPEC §5). The standard is that the figure is *reported and honestly
    /// tagged* — not this constant. Each rung is ~100× the one below.
    pub fn nominal_uj(self) -> u64 {
        match self {
            Tier::Automation => 50,       // ~free deterministic CPU
            Tier::Smt => 5_000,           // cheap decision procedure
            Tier::SmallModel => 500_000,  // a small model forward pass
            Tier::BigModel => 50_000_000, // a frontier model, the last resort
        }
    }
}

/// How honest an energy reading is (SPEC §5) — the family's provenance model.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub enum Provenance {
    /// Read from a hardware energy interface: a shunt or power meter, the SMC,
    /// or a vendor energy counter (RAPL, NVML, Apple IOReport, ...). Requires a
    /// present `measured_uj`.
    ///
    /// A vendor counter's reading is a hardware reading; what it lacks is
    /// independent provenance, not accuracy. It is subject to the liveness
    /// requirement of SPEC §5: a reading from a vendor energy counter (RAPL,
    /// NVML, Apple IOReport, ...) MAY be graded as a hardware reading only
    /// while the counter is demonstrably live for the domain the figure
    /// claims: the implementation MUST have observed the counter covering that
    /// domain advance under load (for Apple IOReport: the CPU energy rail
    /// itself advancing in at least 5 sample intervals, in at least 4 of every
    /// 5, over at least 300 ms while the probing thread burns CPU). A counter
    /// that is present but not live - frozen, or republished in lumps - MUST
    /// NOT produce a hardware-graded figure; the implementation falls back to
    /// its estimator or reports the work unmetered, and SHOULD record why.
    HwShunt,
    /// Computed from a model calibrated on the host or against a reading (e.g.
    /// wall time × a power the host measured). `measured_uj` may be absent.
    ModelBased,
    /// A figure nothing calibrated: a coarse constant, or a model run at a
    /// default or assumed parameter (e.g. wall time × a default power).
    /// `measured_uj` MUST be absent.
    Estimator,
}

impl Provenance {
    /// The JCR-1 wire label, shared across the family's receipts.
    pub fn jcr1_label(self) -> &'static str {
        match self {
            Provenance::HwShunt => "HwShunt",
            Provenance::ModelBased => "ModelBased",
            Provenance::Estimator => "Estimator",
        }
    }
}

/// A two-part energy reading, all integer microjoules (SPEC §5).
#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct Energy {
    /// Present ONLY when obtained from a hardware interface.
    pub measured_uj: Option<u64>,
    /// Always present.
    pub estimated_uj: u64,
    pub provenance: Provenance,
}

impl Energy {
    /// A model-based reading (e.g. measured wall time × a power the host
    /// calibrated). No hardware shunt, so `measured_uj` stays absent. A model
    /// at a power nothing calibrated is an estimate: [`Energy::estimator`].
    pub fn modeled(uj: u64) -> Self {
        Energy {
            measured_uj: None,
            estimated_uj: uj,
            provenance: Provenance::ModelBased,
        }
    }
    /// An estimate of `uj`: a figure nothing calibrated (e.g. measured wall
    /// time × a default power). `measured_uj` stays absent.
    pub fn estimator(uj: u64) -> Self {
        Energy {
            measured_uj: None,
            estimated_uj: uj,
            provenance: Provenance::Estimator,
        }
    }
    /// The estimator of last resort: a coarse per-tier constant.
    pub fn estimate_tier(tier: Tier) -> Self {
        Energy {
            measured_uj: None,
            estimated_uj: tier.nominal_uj(),
            provenance: Provenance::Estimator,
        }
    }
    /// A true hardware reading. For a vendor energy counter, only while it is
    /// live for the domain the figure claims ([`Provenance::HwShunt`]).
    pub fn measured(uj: u64) -> Self {
        Energy {
            measured_uj: Some(uj),
            estimated_uj: uj,
            provenance: Provenance::HwShunt,
        }
    }
    /// The figure to account with: the hardware reading if present, else the estimate.
    pub fn uj(&self) -> u64 {
        self.measured_uj.unwrap_or(self.estimated_uj)
    }
    /// Enforce the provenance ↔ measured coupling (SPEC §5): `HwShunt` requires
    /// `measured_uj`; `Estimator` forbids it.
    pub fn check_provenance(&self) -> Result<(), SchemaError> {
        match (self.provenance, self.measured_uj) {
            (Provenance::HwShunt, None) => {
                Err(SchemaError::DisallowedType("HwShunt without measured"))
            }
            (Provenance::Estimator, Some(_)) => {
                Err(SchemaError::DisallowedType("Estimator with measured"))
            }
            _ => Ok(()),
        }
    }
}

/// A coarse hint about a goal's difficulty — informs (does not bind) routing.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub enum GoalKind {
    /// Closes by normalization (`x = x`).
    Trivial,
    /// Linear/decidable arithmetic.
    Arithmetic,
    /// Decidable by an SMT theory.
    Decidable,
    /// Needs learned proof search.
    General,
    /// Open / research-grade.
    Hard,
}

/// Whether a goal's *statement* has been validated against intent (SPEC §2).
/// A receipt attests the **proof**; this says whether the thing proved is the
/// thing meant. A verified proof of the wrong specification is worthless, and a
/// prover MUST NEVER upgrade this on its own.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub enum SpecGrounding {
    /// The statement was not validated against intent (the default).
    Ungrounded,
    /// A human reviewed the statement against intent.
    HumanReviewed,
    /// The statement was cross-checked against an independent encoding.
    CrossChecked,
}

impl SpecGrounding {
    pub fn label(self) -> &'static str {
        match self {
            SpecGrounding::Ungrounded => "Ungrounded",
            SpecGrounding::HumanReviewed => "HumanReviewed",
            SpecGrounding::CrossChecked => "CrossChecked",
        }
    }
}

/// A proof obligation (SPEC §2). Content-addressed by `H(statement‖context)`,
/// so an identical goal has one identity across the system and the cache.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct ProofGoal {
    pub statement: String,
    pub context: String,
    pub kind: GoalKind,
    /// Free-text statement of intent (what the statement is meant to encode).
    pub intent: String,
    pub grounding: SpecGrounding,
}

impl ProofGoal {
    /// A new goal, `Ungrounded` by default.
    pub fn new(statement: impl Into<String>, context: impl Into<String>, kind: GoalKind) -> Self {
        ProofGoal {
            statement: statement.into(),
            context: context.into(),
            kind,
            intent: String::new(),
            grounding: SpecGrounding::Ungrounded,
        }
    }
    /// Attach intent and a (necessarily human/cross-checked) grounding.
    pub fn grounded(mut self, intent: impl Into<String>, grounding: SpecGrounding) -> Self {
        self.intent = intent.into();
        self.grounding = grounding;
        self
    }
    /// The content id `H(statement‖0x00‖context)` — the goal's stable identity.
    pub fn id(&self) -> ContentId {
        let mut buf = Vec::with_capacity(self.statement.len() + self.context.len() + 1);
        buf.extend_from_slice(self.statement.as_bytes());
        buf.push(0);
        buf.extend_from_slice(self.context.as_bytes());
        ContentId::of_bytes(&buf)
    }
}

/// The outcome of an attempt (SPEC §4). `Proved` carries the content id of the
/// (verifier-accepted) artifact.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub enum Verdict {
    Proved { artifact: ContentId },
    /// The solver **decided the goal false** — it found a concrete counter-model
    /// (e.g. `z3` returned `sat` on the negated claim). This is a *decision*,
    /// not a failure to decide: the cascade MUST halt on it and never escalate a
    /// disproof to a weaker rung (a model stand-in would otherwise fabricate a
    /// "proof" of a refuted goal). `counter_model` carries the witness when the
    /// solver surfaced one, else empty.
    Refuted { counter_model: String },
    Unproved,
    Error,
}

impl Verdict {
    pub fn is_proved(&self) -> bool {
        matches!(self, Verdict::Proved { .. })
    }
    /// A definitive disproof — a counter-model was found. Distinct from
    /// `Unproved` ("no rung could close it"); a refutation is a decision the
    /// router must not escalate.
    pub fn is_refuted(&self) -> bool {
        matches!(self, Verdict::Refuted { .. })
    }
    /// The wire tag used in receipts (`proved` / `refuted` / `unproved` / `error`).
    pub fn wire_tag(&self) -> &'static str {
        match self {
            Verdict::Proved { .. } => "proved",
            Verdict::Refuted { .. } => "refuted",
            Verdict::Unproved => "unproved",
            Verdict::Error => "error",
        }
    }
}

/// One solver's attempt on a goal: the verdict and what it cost.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct Attempt {
    pub tier: Tier,
    pub verdict: Verdict,
    pub energy: Energy,
}

/// A solver at a declared tier (SPEC §4). The reference solvers gate on
/// [`GoalKind`]; a real one runs the tool and reports what actually happened. A
/// solver returns `Proved` ONLY when a verifier would accept the artifact.
pub trait Solver {
    /// The tier this solver occupies on the ladder.
    fn tier(&self) -> Tier;
    /// Attempt the goal, reporting the verdict and the energy spent.
    fn attempt(&self, goal: &ProofGoal) -> Attempt;

    /// Whether this solver is a **reference stand-in** rather than a real
    /// decision procedure — it returns a verdict to exercise the ladder, and
    /// discharges nothing.
    ///
    /// Defaults to `false`, which is the wrong-way-round default for safety and
    /// deliberately so: a stand-in that forgets to declare itself is the
    /// dangerous case, so the trait cannot be relied on alone — the reference
    /// stand-ins in `proof-solvers` all override it, and a new one MUST.
    ///
    /// Because that default cannot be trusted on its own, the real ladders do
    /// not rely on it to stay clean: they are built from decision procedures
    /// only, and `ladder_is_sound` in `proof-solvers` pins both their membership
    /// and their exact tiers — so a stand-in that forgot to override this still
    /// cannot slip into a ladder whose verdict is read as evidence.
    ///
    /// `Provenance` qualifies the *energy* of an attempt and `SpecGrounding`
    /// qualifies its *intent*; neither says anything about whether a verdict was
    /// earned. This does.
    fn is_reference_stub(&self) -> bool {
        false
    }
}

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

    #[test]
    fn ladder_is_cheapest_first_and_monotone() {
        assert_eq!(Tier::LADDER.len(), 4);
        for w in Tier::LADDER.windows(2) {
            assert!(w[0].nominal_uj() < w[1].nominal_uj());
            assert!(w[0] < w[1]);
        }
    }

    #[test]
    fn goal_id_is_stable_and_distinguishes_context() {
        let a = ProofGoal::new("x = x", "lean4", GoalKind::Trivial);
        let b = ProofGoal::new("x = x", "lean4", GoalKind::Trivial);
        let c = ProofGoal::new("x = x", "coq", GoalKind::Trivial);
        assert_eq!(a.id(), b.id());
        assert_ne!(a.id(), c.id());
        // Grounding/intent do not change identity — the statement does.
        assert_eq!(
            a.id(),
            a.clone()
                .grounded("x equals itself", SpecGrounding::HumanReviewed)
                .id()
        );
    }

    #[test]
    fn provenance_coupling_is_enforced() {
        assert!(Energy::modeled(10).check_provenance().is_ok());
        assert!(Energy::estimate_tier(Tier::Smt).check_provenance().is_ok());
        assert!(Energy::measured(10).check_provenance().is_ok());
        let bad = Energy {
            measured_uj: None,
            estimated_uj: 1,
            provenance: Provenance::HwShunt,
        };
        assert!(bad.check_provenance().is_err());
        let bad2 = Energy {
            measured_uj: Some(1),
            estimated_uj: 1,
            provenance: Provenance::Estimator,
        };
        assert!(bad2.check_provenance().is_err());
    }

    #[test]
    fn default_grounding_is_ungrounded() {
        assert_eq!(
            ProofGoal::new("p", "c", GoalKind::Trivial).grounding,
            SpecGrounding::Ungrounded
        );
    }
}