//! The Proof conformance harness (SPEC §8).
//!
//! Every check is real — it exercises the reference library and asserts a
//! property the standard requires, returning `Ok(())` or a human-readable
//! failure. The classes:
//!
//! - **C1 — cheapest-sufficient routing:** each goal closes at the cheapest tier
//!   that can discharge it.
//! - **C2 — disclosed escalation:** `total_uj` accounts every attempt, and
//!   `wasted_uj` is exactly the joules of the cheaper attempts that failed first.
//! - **C3 — energy honesty:** the tier ladder is strictly monotone, and the
//!   batch is accounted against a frontier-only baseline (savings never negative).
//! - **C4 — the flywheel:** re-proving an identical goal costs zero new joules.
//! - **C5 — the receipt:** a proved result seals to a JCR-1 envelope and verifies;
//!   a wrong steward fails.
//! - **C-neg — negatives:** provenance coupling is enforced, an unproved goal
//!   cannot be sealed, a tampered envelope fails, and canonical CBOR rejects
//!   floats/bools.

use ed25519_dalek::SigningKey;
use proof_cascade::{ProofCache, Router};
use proof_schema::{canonical_cbor, Energy, GoalKind, ProofGoal, Provenance, Tier};
use proof_solvers::reference_ladder;

/// A single conformance check.
pub struct Check {
    pub id: &'static str,
    pub run: fn() -> Result<(), String>,
}

/// All checks, in order.
pub fn checks() -> Vec<Check> {
    vec![
        Check { id: "C1 cheapest-sufficient routing", run: c1_routing },
        Check { id: "C2 disclosed escalation", run: c2_escalation },
        Check { id: "C3 energy honesty + baseline", run: c3_energy },
        Check { id: "C4 the cache flywheel", run: c4_flywheel },
        Check { id: "C5 receipt seal + verify", run: c5_receipt },
        Check { id: "C6 joule ceiling", run: c6_ceiling },
        Check { id: "C-neg provenance coupling", run: cneg_provenance },
        Check { id: "C-neg unproved cannot seal", run: cneg_unproved },
        Check { id: "C-neg tampered envelope fails", run: cneg_tamper },
        Check { id: "C-neg canonical rejects floats", run: cneg_canonical },
    ]
}

fn router() -> Router {
    Router::new(reference_ladder())
}

fn c1_routing() -> Result<(), String> {
    let r = router();
    let mut cache = ProofCache::new();
    let cases = [
        ("x = x", GoalKind::Trivial, Tier::Automation),
        ("decidable", GoalKind::Decidable, Tier::Smt),
        ("needs search", GoalKind::General, Tier::SmallModel),
        ("open conjecture", GoalKind::Hard, Tier::BigModel),
    ];
    for (stmt, kind, want) in cases {
        let res = r.prove(&ProofGoal::new(stmt, "c", kind), &mut cache);
        if res.closed_by != Some(want) {
            return Err(format!("{stmt:?} closed at {:?}, want {want:?}", res.closed_by));
        }
    }
    Ok(())
}

/// **C6 — the joule ceiling (SPEC §5.1).** A declared ceiling must stop the
/// cascade *before* the rung it cannot afford, must leave a budget halt
/// distinguishable from a mathematical verdict, and must be sealed into the
/// receipt when a proof is obtained under one.
fn c6_ceiling() -> Result<(), String> {
    // The reference ladder closes `Hard` only at BigModel (50 J). A ceiling
    // that admits everything below it must refuse exactly that rung.
    let ceiling = Tier::Automation.nominal_uj()
        + Tier::Smt.nominal_uj()
        + Tier::SmallModel.nominal_uj()
        + 1;
    let r = Router::with_ceiling(reference_ladder(), ceiling);
    let mut cache = ProofCache::new();
    let res = r.prove(&ProofGoal::new("open conjecture", "c", GoalKind::Hard), &mut cache);

    if res.proved {
        return Err("a goal needing an unaffordable rung must not be proved".into());
    }
    if res.halted_at != Some(Tier::BigModel) {
        return Err(format!("halted_at = {:?}, want Some(BigModel)", res.halted_at));
    }
    if res.ceiling_uj != Some(ceiling) {
        return Err("the ceiling in force must be recorded on the result".into());
    }
    // The expensive rung must never have executed — enforcement is before the
    // spend, not after it.
    if res.attempts.iter().any(|a| a.tier == Tier::BigModel) {
        return Err("the refused rung executed anyway".into());
    }
    if res.total_uj > ceiling {
        return Err(format!("spent {} over a ceiling of {ceiling}", res.total_uj));
    }
    // A budget halt is not a refutation and not a decision.
    if res.refuted {
        return Err("a budget halt must not be reported as a refutation".into());
    }

    // Under a ceiling it CAN afford, the run proceeds and the receipt carries
    // the budget it was honoured under.
    let r = Router::with_ceiling(reference_ladder(), u64::MAX);
    let mut cache = ProofCache::new();
    let ok = r.prove(&ProofGoal::new("x = x", "c", GoalKind::Trivial), &mut cache);
    if !ok.proved || ok.halted_by_ceiling() {
        return Err("an affordable goal must still close".into());
    }
    let wire = proof_receipt::to_jcr1_wire(&ok, "did:example:steward");
    if wire.get("ceiling_uj").and_then(|v| v.as_u64()) != Some(u64::MAX) {
        return Err("a declared ceiling must be sealed into the receipt".into());
    }

    // And an unbounded run must omit the field entirely, so its receipt is
    // byte-identical to one sealed before §5.1 existed.
    let mut cache = ProofCache::new();
    let unbounded = router().prove(&ProofGoal::new("x = x", "c", GoalKind::Trivial), &mut cache);
    let wire = proof_receipt::to_jcr1_wire(&unbounded, "did:example:steward");
    if wire.get("ceiling_uj").is_some() {
        return Err("an unbounded run must omit ceiling_uj, not encode a null".into());
    }
    Ok(())
}

fn c2_escalation() -> Result<(), String> {
    let r = router();
    let mut cache = ProofCache::new();
    // Decidable: T0 (automation) runs and fails, T1 (smt) closes it.
    let res = r.prove(&ProofGoal::new("dec", "c", GoalKind::Decidable), &mut cache);
    let want_waste = Tier::Automation.nominal_uj();
    let want_total = Tier::Automation.nominal_uj() + Tier::Smt.nominal_uj();
    if res.wasted_uj != want_waste {
        return Err(format!("wasted_uj = {}, want {want_waste}", res.wasted_uj));
    }
    if res.total_uj != want_total {
        return Err(format!("total_uj = {}, want {want_total}", res.total_uj));
    }
    // total = sum of recorded attempts.
    let sum: u64 = res.attempts.iter().map(|a| a.uj).sum();
    if sum != res.total_uj {
        return Err(format!("attempts sum {sum} ≠ total_uj {}", res.total_uj));
    }
    Ok(())
}

fn c3_energy() -> Result<(), String> {
    for w in Tier::LADDER.windows(2) {
        if w[0].nominal_uj() >= w[1].nominal_uj() {
            return Err(format!("ladder not monotone at {:?}→{:?}", w[0], w[1]));
        }
    }
    let r = router();
    let mut cache = ProofCache::new();
    let mut s = proof_cascade::EnergySummary::default();
    for (stmt, kind) in [
        ("x=x", GoalKind::Trivial),
        ("dec", GoalKind::Decidable),
        ("hard", GoalKind::Hard),
    ] {
        s.record(&r.prove(&ProofGoal::new(stmt, "c", kind), &mut cache));
    }
    if s.baseline_uj != 3 * Tier::BigModel.nominal_uj() {
        return Err("baseline is not frontier-only over the batch".into());
    }
    if s.saved_uj() == 0 || s.energy_ratio_milli() <= 1000 {
        return Err("no savings versus frontier-only".into());
    }
    Ok(())
}

fn c4_flywheel() -> Result<(), String> {
    let r = router();
    let mut cache = ProofCache::new();
    let g = ProofGoal::new("dec", "c", GoalKind::Decidable);
    let first = r.prove(&g, &mut cache);
    let again = r.prove(&g, &mut cache);
    if !again.from_cache {
        return Err("second proof was not served from cache".into());
    }
    if again.total_uj != 0 {
        return Err(format!("cache hit cost {} uj, want 0", again.total_uj));
    }
    if again.closed_by != first.closed_by {
        return Err("cache hit changed the closing tier".into());
    }
    Ok(())
}

fn c5_receipt() -> Result<(), String> {
    let r = router();
    let mut cache = ProofCache::new();
    let res = r.prove(&ProofGoal::new("x = x", "c", GoalKind::Trivial), &mut cache);
    let sk = SigningKey::from_bytes(&[7u8; 32]);
    let steward = "did:example:prover";
    let env = proof_receipt::seal(&res, &sk, steward).map_err(|e| e.to_string())?;
    proof_receipt::verify(&res, &env, steward, &sk.verifying_key().to_bytes())
        .map_err(|e| format!("verify failed: {e}"))?;
    if proof_receipt::verify(&res, &env, "did:example:wrong", &sk.verifying_key().to_bytes()).is_ok() {
        return Err("verified under the wrong steward".into());
    }
    Ok(())
}

fn cneg_provenance() -> Result<(), String> {
    let bad_shunt = Energy { measured_uj: None, estimated_uj: 1, provenance: Provenance::HwShunt };
    if bad_shunt.check_provenance().is_ok() {
        return Err("HwShunt without a measured figure was accepted".into());
    }
    let bad_est = Energy { measured_uj: Some(1), estimated_uj: 1, provenance: Provenance::Estimator };
    if bad_est.check_provenance().is_ok() {
        return Err("Estimator carrying a measured figure was accepted".into());
    }
    Ok(())
}

fn cneg_unproved() -> Result<(), String> {
    let r = router();
    let mut cache = ProofCache::new();
    let mut res = r.prove(&ProofGoal::new("x = x", "c", GoalKind::Trivial), &mut cache);
    res.proved = false;
    res.closed_by = None;
    let sk = SigningKey::from_bytes(&[7u8; 32]);
    if proof_receipt::seal(&res, &sk, "s").is_ok() {
        return Err("an unproved goal was sealed into a receipt".into());
    }
    Ok(())
}

fn cneg_tamper() -> Result<(), String> {
    let r = router();
    let mut cache = ProofCache::new();
    let res = r.prove(&ProofGoal::new("x = x", "c", GoalKind::Trivial), &mut cache);
    let sk = SigningKey::from_bytes(&[7u8; 32]);
    let steward = "did:example:prover";
    let mut env = proof_receipt::seal(&res, &sk, steward).map_err(|e| e.to_string())?;
    // Flip a byte in the signature region (last byte) — must fail verification.
    if let Some(b) = env.last_mut() {
        *b ^= 0x01;
    }
    if proof_receipt::verify(&res, &env, steward, &sk.verifying_key().to_bytes()).is_ok() {
        return Err("a tampered envelope verified".into());
    }
    Ok(())
}

fn cneg_canonical() -> Result<(), String> {
    if canonical_cbor(&serde_json::json!({"x": 1.5})).is_ok() {
        return Err("canonical CBOR accepted a float".into());
    }
    if canonical_cbor(&serde_json::json!({"x": true})).is_ok() {
        return Err("canonical CBOR accepted a bool".into());
    }
    Ok(())
}

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

    #[test]
    fn all_checks_pass() {
        for c in checks() {
            (c.run)().unwrap_or_else(|e| panic!("{} failed: {e}", c.id));
        }
    }
}