# JouleSpec applied to its own reference implementation.
#
# The clauses are the conformance items of SPEC.md §7, read from the published
# document rather than copied here, so the manifest cannot drift from the
# specification: reword an item and its obligation address moves, and every
# witness bound to the old wording stops applying (SPEC §4.2).
#
# Three things below are human judgements the standard refuses to guess:
#
#   * which check stands for which obligation -- the mapping from prose to
#     code, which is the same act as formalizing a clause (SPEC §2.6);
#   * each check's `anchor` -- where its expected values come from, which the
#     author of the check knows and nobody else can see (SPEC §2.5);
#   * each check's `footprint` -- the inputs whose change could change the
#     outcome, since a harness that cannot observe its own reads must not
#     guess (SPEC §8).
#
# Each `counter` is a one-occurrence edit that SHOULD make the check fail. If
# it does not, the harvester reports a finding and the clause stays at E2: a
# check that passes while its subject is broken is an oracle that cannot fail.
#
# The keys are single-byte seeds so published vectors are reproducible by
# anyone. They are not secrets and a deployment must pass its own.

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

[spec]
document = "../../SPEC.md"
section = "7. Conformance"
expect_at_least = 11
# `shape` is deliberately not declared here. Omitting it selects the numbered
# conformance list this family's specifications use, which is what this
# manifest was written against -- so this file also stands as the check that a
# manifest predating the declared shape keeps every obligation address it had.
intent = """
The joulespec/1 reference implementation does what SPEC.md §7 says it does, \
and each claim is evidenced by a check demonstrated capable of failing.\
"""

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

# No meter is wired, so energy is wall-clock times a declared draw and is
# graded `estimator`. A measured backend is the listed contributing ask; until
# one exists the figure says what it is.
[energy]
watts = 30.0
provenance = "estimator"

# ── C1 — Addressing ───────────────────────────────────────────────────────
[[evidence]]
clause = "C1"
check = "spec::tests::relabelling_a_clause_moves_no_obligation"
anchor = "specification"
footprint = ["crates/joulespec-core/src/spec.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/spec.rs"
find = 'let doc = json!({ "kind": self.kind.label(), "text": self.text });'
replace = 'let doc = json!({ "label": self.label, "kind": self.kind.label(), "text": self.text });'
breaks = "puts the label back into the obligation address"

[[evidence]]
clause = "C1"
check = "spec::tests::rewording_a_clause_moves_its_obligation"
anchor = "specification"
footprint = ["crates/joulespec-core/src/spec.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/spec.rs"
find = 'let doc = json!({ "kind": self.kind.label(), "text": self.text });'
replace = 'let doc = json!({ "kind": self.kind.label(), "text": "" });'
breaks = "drops the text from the obligation address"

# ── C2 — Validation ───────────────────────────────────────────────────────
[[evidence]]
clause = "C2"
check = "spec::tests::two_clauses_stating_one_obligation_are_refused"
anchor = "specification"
footprint = ["crates/joulespec-core/src/spec.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/spec.rs"
find = "return Err(Error::DuplicateObligation(first, clause.label.clone()));"
replace = "let _ = first;"
breaks = "stops refusing two clauses that state one obligation"

# ── C3 — Signatures ───────────────────────────────────────────────────────
[[evidence]]
clause = "C3"
check = "spec::tests::a_tampered_clause_breaks_the_signature"
anchor = "specification"
footprint = ["crates/joulespec-core/src/spec.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/spec.rs"
find = """        key.verify(&pre, &Signature::from_bytes(&sig)).map_err(|_| Error::BadSignature)?;
        self.spec.spec_id()"""
replace = """        let _ = (&pre, &sig, &key);
        self.spec.spec_id()"""
breaks = "stops verifying the specification signature at all"

# ── C4 — The ladder ───────────────────────────────────────────────────────
[[evidence]]
clause = "C4"
check = "evidence::tests::a_proof_reaches_e4_only_when_grounded_and_shown_non_vacuous"
anchor = "specification"
footprint = ["crates/joulespec-core/src/evidence.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/evidence.rs"
find = "if grounded && vacuity.is_refuted() { Grade::Proved } else { Grade::Exercised }"
replace = "if grounded { Grade::Proved } else { Grade::Exercised }"
breaks = "lets a possibly-vacuous proof reach E4"

[[evidence]]
clause = "C4"
check = "evidence::tests::a_self_review_is_the_citation_again"
anchor = "specification"
footprint = ["crates/joulespec-core/src/evidence.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/evidence.rs"
find = "if reviewer == author { Grade::Cited } else { Grade::Reviewed }"
replace = "{ let _ = (reviewer, author); Grade::Reviewed }"
breaks = "stops computing independence from key disjointness"

# ── C5 — Evaluation ───────────────────────────────────────────────────────
[[evidence]]
clause = "C5"
check = "conform::tests::a_specification_is_graded_by_its_weakest_owed_obligation"
anchor = "specification"
footprint = ["crates/joulespec-core/src/conform.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = "    graded.into_iter().min().unwrap_or(None)"
replace = "    graded.into_iter().max().unwrap_or(None)"
breaks = "takes the strongest owed obligation instead of the weakest"

[[evidence]]
clause = "C5"
check = "conform::tests::evaluation_is_deterministic_under_witness_reordering"
anchor = "specification"
footprint = ["crates/joulespec-core/src/conform.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = "grade > current || (grade == current && &witness_id < best)"
replace = "grade >= current"
breaks = "breaks ties by input order instead of by address"

# ── C6 — Drift ────────────────────────────────────────────────────────────
[[evidence]]
clause = "C6"
check = "drift::tests::rewording_one_clause_invalidates_exactly_that_clauses_evidence"
anchor = "specification"
footprint = ["crates/joulespec-core/src/drift.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/drift.rs"
find = ".chain(self.reworded.iter().map(|r| r.was.clone()))"
replace = ".chain(std::iter::empty::<Obligation>())"
breaks = "stops counting a reworded clause's old obligation as invalidated"

[[evidence]]
clause = "C6"
check = "drift::tests::reusing_a_freed_label_is_an_addition_not_a_rewording"
anchor = "specification"
footprint = ["crates/joulespec-core/src/drift.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/drift.rs"
find = "Some(was) if !to_by_obligation.contains_key(was) => reworded.push(Reword {"
replace = "Some(was) => reworded.push(Reword {"
breaks = "mistakes a reused label for a rewording"

# ── C7 — Cost ─────────────────────────────────────────────────────────────
[[evidence]]
clause = "C7"
check = "conform::tests::an_aggregate_is_graded_by_the_weakest_figure_that_fed_it"
anchor = "specification"
footprint = [
  "crates/joulespec-core/src/lib.rs",
  "crates/joulespec-core/src/conform.rs",
]
[evidence.counter]
file = "crates/joulespec-core/src/lib.rs"
find = "    it.into_iter().min()"
replace = "    it.into_iter().max()"
breaks = "grades an aggregate by its best figure instead of its worst"

[[evidence]]
clause = "C7"
check = "conform::tests::a_ratio_with_no_work_is_absent_rather_than_zero"
anchor = "specification"
footprint = ["crates/joulespec-core/src/conform.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = """    if total == 0 {
        return None;
    }"""
replace = """    if total == 0 {
        return Some(0);
    }"""
breaks = "reports a ratio of nothing as zero rather than absent"

# ── C8 — Receipts ─────────────────────────────────────────────────────────
[[evidence]]
clause = "C8"
check = "receipt::tests::an_ungraded_specification_omits_the_grade_rather_than_sealing_a_floor"
anchor = "specification"
footprint = ["crates/joulespec-core/src/receipt.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/receipt.rs"
find = """    if let Some(grade) = conformance.grade {
        map.insert("grade".into(), json!(grade.code()));
    }"""
replace = """    map.insert("grade".into(), json!(conformance.grade.map_or("E0", Grade::code)));"""
breaks = "seals a floor grade where none was established"

[[evidence]]
clause = "C8"
check = "receipt::tests::a_receipt_is_byte_identical_for_identical_evidence"
anchor = "specification"
footprint = ["crates/joulespec-core/src/receipt.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/receipt.rs"
find = 'map.insert("steward".into(), json!(steward));'
replace = 'map.insert("steward".into(), json!(format!("{steward}{:?}", std::time::Instant::now())));'
breaks = "makes a receipt depend on when it was sealed rather than on its evidence"

# ── C9 — Footprints ───────────────────────────────────────────────────────
[[evidence]]
clause = "C9"
check = "evidence::tests::the_footprint_is_part_of_what_the_signature_covers"
anchor = "specification"
footprint = ["crates/joulespec-core/src/evidence.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/evidence.rs"
find = '"footprint": self.footprint.iter().map(Address::as_str).collect::<Vec<_>>(),'
replace = '"footprint": Vec::<&str>::new(),'
breaks = "leaves the footprint out of what the signature covers"

[[evidence]]
clause = "C9"
check = "evidence::tests::a_narrowed_witness_survives_a_change_it_did_not_depend_on"
anchor = "specification"
footprint = ["crates/joulespec-core/src/evidence.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/evidence.rs"
find = "self.footprint.iter().all(|a| state.parts.contains(a))"
replace = "self.footprint.iter().all(|a| a == &state.address)"
breaks = "matches footprint members against the whole-state address rather than its parts"

# Added after a harvest finding: the entry above narrows to one footprint
# member, and on a one-element footprint `all` and `any` are the same
# function, so the conjunction itself went unchecked.
[[evidence]]
clause = "C9"
check = "evidence::tests::a_witness_needs_every_footprint_member_not_merely_one"
anchor = "specification"
footprint = ["crates/joulespec-core/src/evidence.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/evidence.rs"
find = "self.footprint.iter().all(|a| state.parts.contains(a))"
replace = "self.footprint.iter().any(|a| state.parts.contains(a))"
breaks = "keeps a witness alive when only some of its footprint survives"

[[evidence]]
clause = "C9"
check = "evidence::tests::a_footprint_that_cannot_be_checked_is_stale"
anchor = "specification"
footprint = ["crates/joulespec-core/src/evidence.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/evidence.rs"
find = "        self.footprint.iter().all(|a| state.parts.contains(a))"
replace = "        state.parts.is_empty() || self.footprint.iter().all(|a| state.parts.contains(a))"
breaks = "assumes a state it cannot enumerate satisfies every footprint"

# ── C10 — Demonstrated failure ────────────────────────────────────────────
[[evidence]]
clause = "C10"
check = "evidence::tests::an_unstated_anchor_caps_a_falsifiable_check_at_e2"
anchor = "specification"
footprint = ["crates/joulespec-core/src/evidence.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/evidence.rs"
find = "                if anchor.is_stated() { Grade::Falsifiable } else { Grade::Exercised }"
replace = "                { let _ = anchor; Grade::Falsifiable }"
breaks = "lets a check with no stated anchor reach E3"

[[evidence]]
clause = "C10"
check = "evidence::tests::every_rung_above_e2_rests_on_a_demonstrated_failure"
anchor = "specification"
footprint = ["crates/joulespec-core/src/evidence.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/evidence.rs"
find = "            Self::Exercised { .. } => Grade::Exercised,"
replace = "            Self::Exercised { .. } => Grade::Falsifiable,"
breaks = "promotes a merely passing check to E3"

# ── C11 — Attestation ─────────────────────────────────────────────────────
[[evidence]]
clause = "C11"
check = "conform::tests::with_no_work_supplied_independence_is_absent_not_assumed"
anchor = "specification"
footprint = ["crates/joulespec-core/src/conform.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = """        let attestation = if implementers.is_empty() {
            None"""
replace = """        let attestation = if implementers.is_empty() {
            Some(Attestation::Independent)"""
breaks = "assumes independence where no implementer is known"

[[evidence]]
clause = "C11"
check = "conform::tests::agreement_among_implementers_alone_is_not_reproduction"
anchor = "specification"
footprint = ["crates/joulespec-core/src/conform.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = """        let any_independent =
            !implementers.is_empty() && authors.iter().any(|a| !implementers.contains(a));
        if any_independent {"""
replace = """        let any_independent = !implementers.is_empty();
        if any_independent {"""
breaks = "calls agreement among implementers reproduction"

# A proof, not a check. C7 says ratios are integer parts-per-million; the two
# checks above cover the provenance rule and the absent-not-zero rule, and
# neither covers whether the arithmetic on the way to the ratio is defined at
# all. That is the half sampling cannot reach: the inputs that break it are a
# `part` above roughly u64::MAX / 1_000_000, which no hand-written case picks.
#
# Measured on this workspace: the mutation below is invisible to the entire
# test suite and refuted by the prover in a fraction of a second. That gap is
# the reason the ladder has a rung above E3.
#
# The grounding is `declared`, so this witness is graded `E2` and not `E4`
# (SPEC §2.6). Nobody independent of its author has confirmed that the
# statement below says what C7 says, and recording the proof at its real rung
# is the point of having the axis.
[[evidence]]
clause = "C7"
check = "proofs::the_ratio_rule_is_total_over_every_input"
anchor = "specification"
footprint = [
  "crates/joulespec-core/src/conform.rs",
  "crates/joulespec-core/src/proofs.rs",
]
[evidence.formalization]
package = "joulespec-core"
grounding = "declared"
budget_seconds = 300
statement = """
For all part, rest : u64 --- every arithmetic operation performed by
conform::ppm(part, rest) is defined: none overflows and none divides by zero.
Discharged over the whole input domain by the checker's arithmetic checks,
with reachability covers for the absent case, the computed case, the
overflowing-whole case, and a part large enough to overflow the scale in 64
bits.

The companion statement --- that the quotient is bounded by the scale --- is
deliberately not made here. It requires the solver to reason about the output
bits of a 128-bit division and did not converge; see the README.
"""
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = "    Some(((u128::from(part) * 1_000_000) / u128::from(total)) as u64)"
replace = "    Some((part * 1_000_000) / total)"
breaks = "computes the scale in 64 bits, where a large part overflows it"

# A second proof, on the property an adversary has the clearest incentive to
# break. The statement is about `cap` itself -- the function the evaluator
# calls -- so the counter-artifact below is an edit to the artifact, not to a
# copy of the rule living inside the harness.
[[evidence]]
clause = "C5"
check = "proofs::widening_a_set_can_only_lower_its_cap"
anchor = "specification"
footprint = [
  "crates/joulespec-core/src/conform.rs",
  "crates/joulespec-core/src/proofs.rs",
]
[evidence.formalization]
package = "joulespec-core"
grounding = "declared"
budget_seconds = 300
statement = """
For every set of at most four graded figures and one added figure ---
conform::cap(set) is None whenever any member is None; otherwise it is Some(b)
for some b belonging to the set, and cap(set + extra) <= b; and cap can empty
only because the added figure was itself absent. Discharged over every
combination of ladder rungs and absences a set of that size admits, with
reachability covers for the strictly-lower, unchanged, emptied and
already-empty cases.
"""
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = "    graded.into_iter().min().unwrap_or(None)"
replace = "    graded.into_iter().max().unwrap_or(None)"
breaks = "caps a set by its best figure instead of its worst"