//! The **formally-verified fix tier** — the verification rung past build+test.
//!
//! `joule-fix`'s `run_once` discharges six *operational* gates (build, tests,
//! lint-delta, frame, diff). They answer "did this change break anything we
//! tested?" — not "is this change *correct*?". For a fix whose correctness is a
//! formal property, there is a stronger gate, and every piece to run it already
//! ships in this monorepo:
//!
//!   - `joulecontract-proof` — the vericoding bridge: a contract obligation that
//!     carries a formalization becomes a content-addressed proof goal.
//!   - `proof-solvers::real_ladder()` — a cheapest-sufficient cascade ending in
//!     a **real `z3`** SMT backend (assert the negation; `unsat` ⇒ valid).
//!   - the proof cascade meters every attempt in joules.
//!
//! This example wires them into a fix flow the harness does not yet run inline.
//! A settlement-netting function must satisfy one postcondition:
//!
//!     when debits == credits, the net is zero.
//!
//! Two candidate fixes arrive. The proof — not a test suite — decides which one
//! is correct, and the buggy one is *refused before it can ship*:
//!
//!   - candidate A (`net = debits + credits`): z3 finds a counter-model
//!     (debits = credits = 1 ⇒ net = 2 ≠ 0) → **Unproved** → the formal gate
//!     rejects the fix, with the wasted joules on record.
//!   - candidate B (`net = debits - credits`): z3 finds the negation `unsat` →
//!     the postcondition holds for *all* integers → **Proved** by the SMT rung,
//!     measured joules sealed.
//!
//! That is the rigor nobody in the remediation market has reached: a fix gated
//! by a machine-checked proof of its own postcondition, priced in joules. It is
//! honest by construction — where `z3` is absent both candidates come back
//! Unproved (never a fabricated pass), and the unformalized obligations are
//! demoted, never dropped.
//!
//! Run with:  `cargo run -p joule-code-remediate --example formal_fix`

use joulecontract_proof::{discharge, DischargeStatus, Formalization};
use joulecontract_schema::{Ceiling, Contract, ContentAddress, Rigor};
use proof_cascade::{ProofCache, Router};
use proof_schema::{GoalKind, SpecGrounding};
use proof_solvers::{z3_available, Propositional, Z3Smt};

// SOUNDNESS NOTE — why this example uses a decision-procedure ladder.
//
// This example originally exposed a soundness hole: against
// `proof_solvers::real_ladder()` = `[Propositional, Z3Smt, SmallModel,
// FrontierModel]`, candidate A (the bug) came back "PROVED by BigModel" at
// ~50 J. The cascade had no `Verdict::Refuted`, so `Z3Smt` collapsed z3's `sat`
// (a real counter-model) into `Unproved`; the router escalated it; and
// `FrontierModel` proves ANY goal unconditionally — so a disproof was
// fabricated into a proof.
//
// That is now fixed in the proof crate: `Verdict::Refuted` exists, `Z3Smt`
// emits it on `sat`, and the router HALTS on a refutation instead of escalating
// (regression test in proof-cascade). So `real_ladder()` no longer fabricates a
// proof of candidate A — it halts at `Z3Smt` with a refutation.
//
// We still use the decision-procedure ladder `[Propositional, Z3Smt]` here, on
// purpose: a formal *gate* must not depend on a model stand-in even for goals
// z3 returns `unknown` on (the stubs would still claim `proved` there). The
// gate's guarantee is "a decision procedure decided this", nothing weaker.

/// The contract over the netting function: one precondition, one postcondition
/// (the property the fix must honor), one frame. Same spec for both candidates
/// — only the fix's computed `net` differs.
fn netting_contract() -> Contract {
    Contract {
        joulecontract: "joulecontract/0.6".into(),
        subject: "settlement netting — net(debits, credits)".into(),
        rigor_target: Rigor::Jr2,
        pre: vec!["debits and credits are integers".into()],
        post: vec!["when debits == credits, the net is zero".into()],
        inv: vec![],
        frame: vec!["the settlement ledger row".into()],
        ceiling: Ceiling {
            enpi_joules: 10.0,
            unit: "joules/settlement".into(),
            enb_ref: ContentAddress::of_bytes(b"enb-settlement-2026"),
            derivation: None,
        },
        sector_equivalence: None,
        amends: None,
    }
}

/// An SMT-LIB2 goal: the candidate's computed `net`, the premise `debits ==
/// credits`, and the **negation** of the postcondition. `unsat` ⇒ no
/// counter-model exists ⇒ the postcondition is a theorem for that candidate.
fn postcondition_goal(net_definition: &str) -> String {
    format!(
        "(declare-const debits Int)\n\
         (declare-const credits Int)\n\
         (declare-const net Int)\n\
         (assert (= net {net_definition}))\n\
         (assert (= debits credits))\n\
         (assert (not (= net 0)))"
    )
}

/// Discharge the post-condition (obligation index 1: pre=0, post=1, frame=2)
/// for one candidate fix, and report the verdict + measured joules.
fn judge(label: &str, net_definition: &str) -> bool {
    let contract = netting_contract();
    let formalization = Formalization {
        obligation: 1, // the postcondition
        statement: postcondition_goal(net_definition),
        kind: GoalKind::Decidable,
        grounding: SpecGrounding::CrossChecked,
    };
    // A fresh cascade + cache per candidate so the joules reported are this
    // candidate's own proof work, not a cache hit from the other. The ladder is
    // decision-procedures only (see the SOUNDNESS NOTE at the top) — a formal
    // gate may not fall through to a model stand-in that fabricates a proof.
    let router = Router::new(vec![Box::new(Propositional), Box::new(Z3Smt)]);
    let mut cache = ProofCache::new();
    let d = discharge(&contract, &[formalization], &router, &mut cache)
        .expect("discharge runs (bookkeeping is well-formed)");

    let entry = &d.entries[1];
    println!("── candidate {label}:  net = {net_definition}");
    match &entry.status {
        DischargeStatus::Proved(result) => {
            println!(
                "   PROVED   by {:?} — postcondition holds for all integers   ({} µJ measured)",
                result.closed_by, result.total_uj
            );
            println!("   → formal gate ACCEPTS this fix.");
            true
        }
        DischargeStatus::Unproved(result) => {
            println!(
                "   UNPROVED — z3 found a counter-model; the postcondition can fail   ({} µJ measured)",
                result.total_uj
            );
            println!("   → formal gate REFUSES this fix (it would be reverted, never shipped).");
            false
        }
        DischargeStatus::Unformalized => {
            println!("   UNFORMALIZED — no proof goal supplied (recorded, never dropped).");
            false
        }
    }
}

fn main() {
    println!("formally-verified fix tier — settlement netting postcondition\n");
    println!("postcondition under proof:  debits == credits  ⇒  net == 0\n");

    if !z3_available() {
        println!(
            "note: `z3` is not on PATH — both candidates will come back UNPROVED.\n\
             That is the honesty rule, not a failure: the harness never fabricates\n\
             a proof it could not run. Install z3 to see the SMT rung discharge.\n"
        );
    }

    let buggy_ok = judge("A (the bug)", "(+ debits credits)");
    println!();
    let fixed_ok = judge("B (the fix)", "(- debits credits)");

    println!("\n── verdict");
    if z3_available() {
        assert!(!buggy_ok, "the buggy candidate must NOT pass the formal gate");
        assert!(fixed_ok, "the correct fix must pass the formal gate");
        println!(
            "the proof discriminated: candidate A refused, candidate B verified.\n\
             the shipped fix is gated by a machine-checked proof of its postcondition —\n\
             a rung above build+test, priced in measured joules. that is the tier the\n\
             remediation market has not reached."
        );
    } else {
        println!(
            "z3 absent: both candidates Unproved (honest). the gate refused the bug AND\n\
             the fix — refusing a correct fix you could not prove beats shipping an\n\
             unproven one. with z3 present, candidate B verifies and candidate A is refused."
        );
    }
}