//! Two soundness regressions, pinned. Both were found by running the shipped
//! ladder on a real statement rather than by reading it, and each was masking
//! the other: the false refutation stopped the cascade before it could reach
//! the fabricating rung.
use proof_cascade::{ProofCache, Router};
use proof_schema::{GoalKind, ProofGoal, Solver, Verdict};

/// A goal that is not SMT-LIB must never come back **refuted**.
///
/// z3 reports a parse failure as `(error "...")` on stdout and then answers
/// `(check-sat)` anyway — against an assertion stack that is empty because
/// nothing parsed — and that answer is `sat`. Read as a verdict, "I could not
/// understand the goal" becomes "the goal is FALSE", and since a refutation is
/// terminal here, the cascade stops and reports a disproof of arbitrary prose.
#[test]
fn prose_is_never_refuted_by_the_smt_rung() {
    let solver = proof_solvers::Z3Smt;
    for stmt in [
        "every even integer greater than 2 is the sum of two primes",
        "the halting problem is decidable",
        "",
        "(((",
    ] {
        let a = solver.attempt(&ProofGoal::new(stmt, "c", GoalKind::Hard));
        assert!(
            !matches!(a.verdict, Verdict::Refuted { .. }),
            "{stmt:?} came back refuted — a parse failure is not a disproof"
        );
    }
}

/// A `sat` with no counter-model is not a refutation. A script that asserts
/// nothing is trivially satisfiable, so `sat` there means "no constraints", not
/// "here is a counter-example".
#[test]
fn a_refutation_must_carry_a_witness() {
    let a = proof_solvers::Z3Smt.attempt(&ProofGoal::new("(check-sat)", "c", GoalKind::Decidable));
    if let Verdict::Refuted { counter_model } = &a.verdict {
        panic!("empty assertion stack reported as refuted with model {counter_model:?}");
    }
}

/// A goal no real rung can decide. Used by both tests below, which are the two
/// halves of one guarantee.
fn open_conjecture() -> ProofGoal {
    ProofGoal::new(
        "every even integer greater than 2 is the sum of two primes",
        "demo",
        GoalKind::Hard,
    )
}

/// The reference stand-ins must admit what they are. The top rung returns
/// `Proved` for *any* goal, with the hash of the goal's own statement as the
/// "artifact" — the claim offered as its own evidence — and `seal()` will sign
/// that into a receipt that verifies. The receipt is not forged; it is honestly
/// signed and substantively empty, which is worse, because it verifies.
///
/// This exercises `reference_ladder()`. It used to exercise `real_ladder()`,
/// because the stand-ins sat on that ladder too — which is precisely the defect
/// since fixed: a solverless machine escalated past both real rungs into T3 and
/// proved everything. Detection was the right answer while the fabrication was
/// reachable in production; now it is prevented there and only has to be
/// detectable where stand-ins legitimately live. The companion test below pins
/// the other half.
#[test]
fn a_stand_in_proof_is_detectable_before_it_is_trusted() {
    let goal = open_conjecture();
    let r = Router::new(proof_solvers::reference_ladder());
    let mut cache = ProofCache::new();
    let res = r.prove(&goal, &mut cache);

    // It still "proves" it — that is the reference ladder's documented shape.
    assert!(res.proved);
    assert_eq!(res.closed_by, Some(proof_schema::Tier::BigModel));
    // The artifact is the goal restated as its own evidence.
    assert_eq!(
        res.artifact.map(|a| a.to_hex()),
        Some(proof_schema::ContentId::of_bytes(goal.statement.as_bytes()).to_hex())
    );

    // But a relying party can now refuse it, which is the point.
    assert!(res.closed_by_stub, "the closing solver was a stand-in");
    assert_eq!(
        res.require_substantive_proof(),
        Err("closed by a reference stand-in, which discharges nothing")
    );

    // And the cache must not launder it into an unmarked proof on the next hit.
    let again = r.prove(&goal, &mut cache);
    assert!(again.from_cache);
    assert!(again.closed_by_stub, "a cache hit must not strip the marker");
    assert!(again.require_substantive_proof().is_err());
}

/// The other half: on the real ladder that same goal is never closed at all.
///
/// Detection (above) is a relying party's last line of defence, and it only
/// works if the relying party remembers to call it. Not reaching a stand-in in
/// the first place is the guarantee that does not depend on anyone remembering.
/// A missing rung must yield a weaker claim, never a stronger one.
#[test]
fn the_real_ladder_never_reaches_a_stand_in() {
    let goal = open_conjecture();
    let r = Router::new(proof_solvers::real_ladder());
    let mut cache = ProofCache::new();
    let res = r.prove(&goal, &mut cache);

    assert!(
        !res.proved,
        "an open conjecture came back proved, closed by {:?}",
        res.closed_by
    );
    assert!(res.closed_by.is_none());
    assert!(
        !res.closed_by_stub,
        "nothing closed it, stand-in or otherwise"
    );
    assert_eq!(res.require_substantive_proof(), Err("not proved"));
    assert!(
        !res.attempts.iter().any(|a| matches!(
            a.tier,
            proof_schema::Tier::SmallModel | proof_schema::Tier::BigModel
        )),
        "a model stand-in ran on the real ladder"
    );
}

/// A real rung is not marked, so the check is not vacuous.
#[test]
fn a_real_solver_is_not_flagged() {
    assert!(!proof_solvers::Propositional.is_reference_stub());
    assert!(!proof_solvers::Z3Smt.is_reference_stub());
    assert!(proof_solvers::FrontierModel.is_reference_stub());

    let r = Router::new(vec![Box::new(proof_solvers::Propositional)]);
    let mut cache = ProofCache::new();
    let res = r.prove(&ProofGoal::new("a | ~a", "c", GoalKind::Trivial), &mut cache);
    assert!(res.proved, "the real propositional decider closes a tautology");
    assert!(!res.closed_by_stub);
    assert!(res.require_substantive_proof().is_ok());
}