e0e9fa7831
Applying the producer to a second standard found something about the `E3` mechanism rather than about that standard. `map/conformance/v1/joulespec.toml` maps every conformance item of the map standard's §8 to a named check with a counter-artifact, and all of them reach `E3`. Four did immediately. The fifth did not, and the reason is the point. That standard's `verify_envelope` enforces its steward twice: once as the envelope's key identifier, and again because the steward sits inside the signed core the envelope commits to, so a wrong steward also fails the payload comparison. Disabling either check alone leaves the other standing, and the test keeps passing. The harvester reported that the check could not see its subject — true, and misleading, because the check is strong and the mutation was well aimed. Neither of the two readings the producer's own documentation offers fits. It is a third case: the artifact state in which the check should fail is not one edit away from the state in which it passes. So a counter-artifact may now declare several edits. They are applied before anything runs and reverted together, in reverse order, including on a panic; if any fails to apply, those already applied revert as the partial vector drops, so the tree is never left half-mutated. The witness's report records how many were applied, because a state several edits away is a different claim from one edit away and a reader should not have to open the manifest to tell. The single-edit form is unchanged and the proof standard's manifest, which uses it throughout, still reaches `E3`. SPEC §2.5 states the rule: nothing in the rung says the failing state is one edit away, and a conforming producer must accept several and record the count. The schema refuses a counter-artifact that declares both forms, or part of the single-edit form, or no edit at all: the first is ambiguous about what the artifact state is, and the others claim to be a counter-artifact while describing nothing. Co-Authored-By: Claude Opus 5 <[email protected]>
100 lines
3.8 KiB
TOML
100 lines
3.8 KiB
TOML
# JouleSpec applied to the map standard.
|
|
#
|
|
# Clauses are read from `../../SPEC.md` section 8 rather than copied here, so
|
|
# this manifest cannot drift from that document: reword a conformance item and
|
|
# its obligation address moves, and the witness bound to the old wording stops
|
|
# applying.
|
|
|
|
workspace = "../../map-rs"
|
|
steward = "did:key:joulespec-applied-map"
|
|
|
|
[spec]
|
|
document = "../../SPEC.md"
|
|
section = "8. Conformance"
|
|
shape = "bulleted-bold-label"
|
|
expect_at_least = 5
|
|
intent = "The 4D cell key, its signed range-requestable tilesets and its resolver behave as section 8 requires."
|
|
|
|
[artifact]
|
|
dirs = ["crates"]
|
|
extensions = ["rs"]
|
|
|
|
[energy]
|
|
watts = 30.0
|
|
provenance = "estimator"
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# C1 -- cell key
|
|
[[evidence]]
|
|
clause = "C1"
|
|
check = "published_cell_keys_re_address_to_their_recorded_ids"
|
|
anchor = "specification"
|
|
footprint = ["crates/map-schema/src/lib.rs"]
|
|
[evidence.counter]
|
|
file = "crates/map-schema/src/lib.rs"
|
|
find = " ContentId(*blake3::hash(bytes).as_bytes())"
|
|
replace = " ContentId(*blake3::hash(b\"\").as_bytes())"
|
|
breaks = "addresses every payload to the hash of nothing, so a published key no longer re-addresses to its recorded id"
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# C2 -- tileset directory
|
|
[[evidence]]
|
|
clause = "C2"
|
|
check = "tests::directory_sorts_and_coalesces_ranges"
|
|
anchor = "specification"
|
|
footprint = ["crates/map-schema/src/lib.rs"]
|
|
[evidence.counter]
|
|
file = "crates/map-schema/src/lib.rs"
|
|
find = " spans.sort_unstable();"
|
|
replace = " spans.reverse();"
|
|
breaks = "hands the range planner unsorted spans, so contiguous ones are no longer coalesced"
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# C3 -- manifest & revision
|
|
[[evidence]]
|
|
clause = "C3"
|
|
check = "tests::revision_chain_verifies_and_detects_break"
|
|
anchor = "specification"
|
|
footprint = ["crates/map-schema/src/lib.rs"]
|
|
[evidence.counter]
|
|
file = "crates/map-schema/src/lib.rs"
|
|
find = " if &self.body.prev_root != expected_prev {"
|
|
replace = " if false {"
|
|
breaks = "stops comparing a revision against the root it claims to follow, so a broken chain verifies"
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# C4 -- cascade
|
|
[[evidence]]
|
|
clause = "C4"
|
|
check = "tests::falls_back_to_floor_when_higher_tiers_absent"
|
|
anchor = "specification"
|
|
footprint = ["crates/map-cascade/src/lib.rs"]
|
|
[evidence.counter]
|
|
file = "crates/map-cascade/src/lib.rs"
|
|
find = " fell_back: tier.rank() < ceiling,"
|
|
replace = " fell_back: false,"
|
|
breaks = "reports a resolution that fell below the requested tier as though it had not"
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# C5 -- receipt
|
|
[[evidence]]
|
|
clause = "C5"
|
|
check = "tests::estimator_seal_verify_roundtrips"
|
|
anchor = "specification"
|
|
footprint = ["crates/map-receipt/src/jcr1.rs", "crates/map-receipt/src/lib.rs"]
|
|
# Two edits, because the steward is enforced twice: once as the envelope's key
|
|
# id, and again because it is inside the signed core the envelope commits to,
|
|
# so a wrong steward also fails the payload comparison. Either edit alone
|
|
# leaves the other defence standing and the check keeps passing -- which the
|
|
# harvester reports, truthfully, as a check that cannot see its subject. The
|
|
# check is strong; the artifact state simply is not one edit away.
|
|
[evidence.counter]
|
|
breaks = "stops enforcing the steward in both places it is checked, so a wrong steward verifies"
|
|
[[evidence.counter.edit]]
|
|
file = "crates/map-receipt/src/jcr1.rs"
|
|
find = " if kid != expected_steward {"
|
|
replace = " if false {"
|
|
[[evidence.counter.edit]]
|
|
file = "crates/map-receipt/src/lib.rs"
|
|
find = " if payload != self.signed_core(steward)? {"
|
|
replace = " if false {"
|