//! Vericoding a contract, end to end: declare obligations, formalize the ones
//! that have a formal meaning, discharge them through the JouleProof cascade,
//! and print the per-obligation ledger with measured joules.
//!
//! Run: `cargo run -p joulecontract-proof --example vericode`
//! (needs `z3` on PATH for the SMT rung; without it the postcondition shows
//! Unproved rather than a fabricated pass — the standard never fakes a proof.)

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

fn main() {
    // A real unit of work and what it must honor.
    let contract = Contract {
        joulecontract: "joulecontract/0.6".into(),
        subject: "settlement batch writer".into(),
        rigor_target: Rigor::Jr2,
        pre: vec!["the input batch is well-formed".into()],
        post: vec!["if debits equal credits, the net settlement is zero".into()],
        inv: vec![],
        frame: vec!["ledger table".into()],
        ceiling: Ceiling {
            enpi_joules: 10.0,
            unit: "joules/batch".into(),
            enb_ref: ContentAddress::of_bytes(b"enb-2026"),
            derivation: None,
        },
        sector_equivalence: None,
        amends: None,
    };

    // Formalize the postcondition (index 1: pre=0, post=1, frame=2). Its
    // negation being unsat means the property holds for all integers.
    let post = Formalization {
        obligation: 1,
        statement: "(declare-const debits Int)\n\
                     (declare-const credits Int)\n\
                     (declare-const net Int)\n\
                     (assert (= net (- debits credits)))\n\
                     (assert (= debits credits))\n\
                     (assert (not (= net 0)))"
            .into(),
        kind: GoalKind::Decidable,
        grounding: SpecGrounding::CrossChecked,
    };

    let router = Router::new(real_ladder());
    let mut cache = ProofCache::new();
    let report = discharge(&contract, &[post], &router, &mut cache).unwrap();

    println!("contract: {}", report.contract);
    if !z3_available() {
        println!("(z3 not found on PATH — the SMT obligation will show Unproved, never faked)\n");
    }
    for entry in &report.entries {
        let status = match &entry.status {
            DischargeStatus::Proved(r) => {
                format!("PROVED at {:?} · {} µJ", r.closed_by.unwrap(), r.total_uj)
            }
            DischargeStatus::Unproved(r) => format!("UNPROVED · {} µJ burned", r.total_uj),
            DischargeStatus::Unformalized => "UNFORMALIZED (binds, undischargeable by proof)".into(),
        };
        println!("  [{}] {:?}: {}\n        → {}", entry.index, entry.obligation.kind, entry.obligation.text, status);
    }
    println!(
        "\n{} proved · {} unproved · {} unformalized · {} µJ total · discharged={}",
        report.proved, report.unproved, report.unformalized, report.total_uj, report.discharged()
    );
}