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 }));
    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"));
    }

    #[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)));
    }
}