open-standards/proof/proof-rs/crates/proof-receipt/src/lib.rs

//! The Proof receipt (SPEC §6).
//!
//! A verified proof seals as a signed record of *what it cost*: the goal it
//! discharged, the tier that closed it, the joules spent (with `wasted_uj` and
//! the frontier-only `baseline_uj`), the honest energy provenance, and the
//! statement's spec-grounding. Receipts seal as **JCR-1** envelopes — the
//! family's shared signed-receipt format (canonical det-CBOR + COSE_Sign1/EdDSA)
//! — so a Proof receipt verifies with the same tooling as a Map, Sandbox, or
//! Joule Code receipt.
//!
//! The receipt attests the **proof**, not the specification: a goal whose
//! `spec_grounding` is `Ungrounded` says, in the signed artifact itself, that
//! the statement was never validated against intent.

use ed25519_dalek::SigningKey;
use proof_cascade::CascadeResult;
use serde_json::{json, Value};

pub mod jcr1;

/// Errors from projecting, sealing, or verifying a receipt.
#[derive(Debug, thiserror::Error)]
pub enum ReceiptError {
    /// A receipt was requested for a goal that was not proved.
    #[error("cannot seal a receipt for an unproved goal")]
    NotProved,
    /// The envelope payload did not match this result's canonical core.
    #[error("envelope payload does not match the result")]
    PayloadMismatch,
    #[error(transparent)]
    Jcr1(#[from] jcr1::Jcr1Error),
}

/// Project a cascade result to JCR-1 wire JSON — the `proof/1` profile of the
/// family's receipt format (SPEC §6). The signed core is a flat uint/text map;
/// fields that don't apply (e.g. `closed_by` for an unproved goal) are omitted.
pub fn to_jcr1_wire(r: &CascadeResult, steward: &str) -> Value {
    let mut obj = serde_json::Map::new();
    obj.insert("proof_receipt".into(), json!("proof/1"));
    obj.insert("goal_id".into(), json!(r.goal_id));
    obj.insert("verdict".into(), json!(if r.proved { "proved" } else { "unproved" }));
    if let Some(t) = r.closed_by {
        obj.insert("closed_by".into(), json!(t.wire_tag()));
    }
    if let Some(a) = r.artifact {
        obj.insert("artifact".into(), json!(a.to_hex()));
    }
    obj.insert("total_uj".into(), json!(r.total_uj));
    obj.insert("wasted_uj".into(), json!(r.wasted_uj));
    obj.insert("baseline_uj".into(), json!(r.baseline_uj));
    obj.insert("energy_provenance".into(), json!(r.provenance.jcr1_label()));
    obj.insert("spec_grounding".into(), json!(r.grounding.label()));
    obj.insert("from_cache".into(), json!(if r.from_cache { 1 } else { 0 }));
    // The declared ceiling, when there was one. Omitted otherwise, so a receipt
    // from an unbounded run canonicalizes to exactly the bytes it always did and
    // every previously sealed receipt and published vector still verifies.
    //
    // On a proved receipt this upgrades the claim from "this proof cost N" to
    // "this proof was obtained under a declared budget of C and cost N" — the
    // difference between reporting a cost and honouring a limit.
    if let Some(c) = r.ceiling_uj {
        obj.insert("ceiling_uj".into(), json!(c));
    }
    // Whether the rung that CLOSED the goal discharges nothing (SPEC §5.2).
    //
    // §5.2 requires a relying party to check this before acting on a proof, but
    // until now it lived only on the in-process result — so anyone holding just
    // the receipt, which is the whole point of sealing one, could not perform
    // the check the spec asks of them. A stand-in-closed receipt is honestly
    // signed and substantively empty; without this field nothing in the bytes
    // says so, and `closed_by` does not: it names a TIER, and the same tag
    // covers a real decision procedure on one ladder and a stand-in on another.
    //
    // Emitted only when true, so a receipt closed by a real solver
    // canonicalizes to exactly the bytes it always did and every such receipt
    // sealed before this field existed still verifies unchanged. The cost falls
    // entirely on receipts that were making an unearned claim.
    if r.closed_by_stub {
        obj.insert("closed_by_stub".into(), json!(1));
    }
    obj.insert("steward".into(), json!(steward));
    Value::Object(obj)
}

/// The canonical signed-core bytes (JCR-1 det-CBOR) for a result.
pub fn signed_core(r: &CascadeResult, steward: &str) -> Result<Vec<u8>, ReceiptError> {
    Ok(jcr1::signed_core_bytes(&to_jcr1_wire(r, steward))?)
}

/// Seal a *proved* result into a JCR-1 COSE_Sign1 envelope. Refuses to seal a
/// receipt for an unproved goal.
pub fn seal(r: &CascadeResult, key: &SigningKey, steward: &str) -> Result<Vec<u8>, ReceiptError> {
    if !r.proved {
        return Err(ReceiptError::NotProved);
    }
    let core = signed_core(r, steward)?;
    Ok(jcr1::cose_sign1_envelope(&core, key, steward))
}

/// Verify a JCR-1 envelope against a steward key and confirm its payload is
/// exactly this result's canonical signed core.
pub fn verify(
    r: &CascadeResult,
    envelope: &[u8],
    steward: &str,
    pubkey: &[u8; 32],
) -> Result<(), ReceiptError> {
    let payload = jcr1::verify_cose_sign1(envelope, steward, pubkey)?;
    if payload != signed_core(r, steward)? {
        return Err(ReceiptError::PayloadMismatch);
    }
    Ok(())
}

#[cfg(test)]
mod tests {
    use super::*;
    use proof_cascade::{ProofCache, Router};
    use proof_schema::{GoalKind, ProofGoal};
    use proof_solvers::reference_ladder;

    fn prove_one(stmt: &str, kind: GoalKind) -> CascadeResult {
        let router = Router::new(reference_ladder());
        let mut cache = ProofCache::new();
        router.prove(&ProofGoal::new(stmt, "lean4", kind), &mut cache)
    }

    #[test]
    fn proved_receipt_seals_and_verifies() {
        let r = prove_one("x = x", GoalKind::Trivial);
        let sk = SigningKey::from_bytes(&[7u8; 32]);
        let steward = "did:example:prover1";
        let env = seal(&r, &sk, steward).unwrap();
        assert!(verify(&r, &env, steward, &sk.verifying_key().to_bytes()).is_ok());
        // A different steward must not verify.
        assert!(verify(&r, &env, "did:example:other", &sk.verifying_key().to_bytes()).is_err());
    }

    #[test]
    fn wire_records_grounding_and_energy_fields() {
        let r = prove_one("dec", GoalKind::Decidable);
        let wire = to_jcr1_wire(&r, "did:example:p");
        let o = wire.as_object().unwrap();
        assert_eq!(o["proof_receipt"], json!("proof/1"));
        assert_eq!(o["verdict"], json!("proved"));
        assert_eq!(o["closed_by"], json!("T1"));
        assert_eq!(o["spec_grounding"], json!("Ungrounded")); // honest by default
        assert!(o.contains_key("baseline_uj") && o.contains_key("wasted_uj"));
    }

    /// A stand-in-closed receipt says so in the bytes a third party receives.
    ///
    /// SPEC §5.2 requires a relying party to check whether the closing rung
    /// discharged anything; §6.1 puts the marker in the signed core so they can
    /// do it holding only the artifact. Without this the pack ships a receipt
    /// asserting an open conjecture is proved, with nothing to qualify it.
    #[test]
    fn a_stand_in_closed_receipt_declares_itself_on_the_wire() {
        let r = prove_one("open conjecture", GoalKind::Hard);
        assert!(r.proved && r.closed_by_stub, "fixture must be stub-closed");
        let wire = to_jcr1_wire(&r, "did:example:p");
        assert_eq!(
            wire.as_object().unwrap().get("closed_by_stub"),
            Some(&json!(1)),
            "a receipt closed by a rung that discharges nothing must say so"
        );
    }

    /// ...and the field is free for an honest proof.
    ///
    /// Omit-when-false is what makes this revision non-breaking: a receipt
    /// closed by a real decision procedure canonicalizes to exactly the bytes it
    /// did before the field existed, so every one sealed earlier still verifies.
    /// The byte cost falls only on receipts making an unearned claim.
    #[test]
    fn a_real_closed_receipt_is_byte_identical_to_before_the_field() {
        use proof_solvers::real_ladder;
        let router = Router::new(real_ladder());
        let mut cache = ProofCache::new();
        let r = router.prove(
            &ProofGoal::new("a | ~a", "prop", GoalKind::Trivial),
            &mut cache,
        );
        assert!(r.proved && !r.closed_by_stub, "fixture must be closed by a real rung");

        let wire = to_jcr1_wire(&r, "did:example:p");
        assert!(
            wire.as_object().unwrap().get("closed_by_stub").is_none(),
            "the field must be absent, not false — an emitted 0 would change the bytes"
        );

        // Pin it at the level that actually matters: the canonical core is what
        // gets signed and content-addressed, so compare bytes, not just the map.
        let core = signed_core(&r, "did:example:p").unwrap();
        let mut expected = to_jcr1_wire(&r, "did:example:p");
        expected.as_object_mut().unwrap().remove("closed_by_stub");
        assert_eq!(core, jcr1::signed_core_bytes(&expected).unwrap());
    }

    #[test]
    fn unproved_goal_cannot_be_sealed() {
        // No solver in the reference ladder is unable to close General/Hard, so
        // build an explicitly unproved result by hand.
        let mut r = prove_one("x = x", GoalKind::Trivial);
        r.proved = false;
        r.closed_by = None;
        let sk = SigningKey::from_bytes(&[7u8; 32]);
        assert!(matches!(seal(&r, &sk, "s"), Err(ReceiptError::NotProved)));
    }
}