open-standards/proof/conformance/v1/joulespec.toml

# JouleSpec applied to the proof standard.
#
# The first time this producer has measured a specification other than its own.
# Clauses are read from `../../SPEC.md` section 8 rather than copied here, so
# this manifest cannot drift from that document: reword an item and its
# obligation address moves, and the witness bound to the old wording stops
# applying.
#
# The three declared things are human judgements the standard refuses to guess
# (JouleSpec SPEC 2.6, 2.5, 8): which check stands for which obligation, where
# each check's expectation comes from, and which inputs it depends on.

workspace = "../../proof-rs"
steward = "did:key:joulespec-applied-proof"

[spec]
document = "../../SPEC.md"
section = "8. Conformance"
# This document writes its conformance items as a bulleted list with bold
# labels, which is a fact about the document rather than about this producer.
shape = "bulleted-bold-label"
# C1..C5 and C-neg. A floor, so a parser that matched fewer fails rather than
# reporting success over a shorter list.
expect_at_least = 6
intent = "The cheapest-sufficient prover routes, accounts and seals as section 8 requires."

[artifact]
dirs = ["crates"]
extensions = ["rs"]

[energy]
watts = 30.0
provenance = "estimator"

# ---------------------------------------------------------------------------
# C1 -- cheapest-sufficient routing
#
# The first mutation written here was aimed at `Tier::LADDER`, on the
# assumption that the router iterated it. It does not: that constant is read
# only by the monotonicity checks, and the router sorts the solvers it was
# handed. So the check passed with the constant reordered, and the harvester
# reported -- correctly -- that the check could not see its subject. The
# report was right and the manifest was wrong, which is the distinction the
# operator has to make and the producer cannot.
#
# Aimed at the sort, the same check fails at once.
[[evidence]]
clause = "C1"
check = "tests::trivial_closes_at_t0_no_waste"
anchor = "specification"
footprint = [
  "crates/proof-schema/src/lib.rs",
  "crates/proof-cascade/src/lib.rs",
]
[evidence.counter]
file = "crates/proof-cascade/src/lib.rs"
find = "        solvers.sort_by_key(|s| s.tier());"
replace = "        solvers.sort_by_key(|s| std::cmp::Reverse(s.tier()));"
breaks = "orders the router's rungs dearest-first, so a goal no longer closes at the cheapest tier that can discharge it"

# ---------------------------------------------------------------------------
# C2 -- disclosed escalation
[[evidence]]
clause = "C2"
check = "tests::escalation_discloses_waste"
anchor = "specification"
footprint = ["crates/proof-cascade/src/lib.rs"]
[evidence.counter]
file = "crates/proof-cascade/src/lib.rs"
find = "                    wasted_uj = wasted_uj.saturating_add(uj);"
replace = "                    wasted_uj = wasted_uj.saturating_add(0);"
breaks = "stops counting a failed cheaper attempt's joules as escalation waste"

# ---------------------------------------------------------------------------
# C3 -- energy honesty
[[evidence]]
clause = "C3"
check = "tests::ladder_is_cheapest_first_and_monotone"
anchor = "specification"
footprint = ["crates/proof-schema/src/lib.rs"]
[evidence.counter]
file = "crates/proof-schema/src/lib.rs"
find = """    pub const LADDER: [Tier; 4] = [
        Tier::Automation,
        Tier::Smt,"""
replace = """    pub const LADDER: [Tier; 4] = [
        Tier::Smt,
        Tier::Automation,"""
breaks = "breaks the ladder's strict monotonicity by putting a dearer rung first"

# ---------------------------------------------------------------------------
# C4 -- the flywheel
[[evidence]]
clause = "C4"
check = "tests::cache_is_the_flywheel"
anchor = "specification"
footprint = ["crates/proof-cascade/src/lib.rs"]
[evidence.counter]
file = "crates/proof-cascade/src/lib.rs"
find = """                total_uj: 0,
                wasted_uj: 0,"""
replace = """                total_uj: 1,
                wasted_uj: 0,"""
breaks = "charges a joule for a proof served from cache, so re-proving is no longer free"

# ---------------------------------------------------------------------------
# C5 -- the receipt
[[evidence]]
clause = "C5"
check = "jcr1::tests::envelope_rejects_wrong_steward"
anchor = "specification"
footprint = ["crates/proof-receipt/src/jcr1.rs"]
[evidence.counter]
file = "crates/proof-receipt/src/jcr1.rs"
find = "    if kid != expected_steward {"
replace = "    if false {"
breaks = "stops comparing the envelope's key id against the expected steward, so a wrong steward verifies"

# ---------------------------------------------------------------------------
# C-neg -- the negative pack
[[evidence]]
clause = "C-neg"
check = "tests::unproved_goal_cannot_be_sealed"
anchor = "specification"
footprint = ["crates/proof-receipt/src/lib.rs"]
[evidence.counter]
file = "crates/proof-receipt/src/lib.rs"
find = """    if !r.proved {
        return Err(ReceiptError::NotProved);
    }"""
replace = """    if false {
        return Err(ReceiptError::NotProved);
    }"""
breaks = "lets a receipt be sealed for a goal nothing proved"