cert_atlas
cert-atlas — a labelled corpus of forged certificates, and a two-sided metric.
DEFECTS =
{'cert.forged_verdict': Defect(key='cert.forged_verdict', family='certificate', title='Recorded verdict flipped to ADMIT', why_it_looks_valid='Every other field is untouched and internally consistent; only the recorded outcome is a lie.', caught_by='Re-deriving the verdict from the per-locus data instead of reading it.', severity='soundness', tags=['verdict', 'trust-the-producer']), 'cert.mutated_intensity': Defect(key='cert.mutated_intensity', family='certificate', title='A locus intensity moved across the threshold, verdict left as ADMIT', why_it_looks_valid='The certificate still parses and its structure is intact.', caught_by='Re-deriving the per-locus classification.', severity='soundness', tags=['physics-input', 'verdict']), 'cert.inflated_photons': Defect(key='cert.inflated_photons', family='certificate', title='Photon count inflated to shrink the safety constant', why_it_looks_valid='A larger photon budget is a physically meaningful edit, so the number looks plausible in isolation.', caught_by='Recomputing K bit-identically from (kappa, safety, n_photons).', severity='soundness', tags=['derived-constant']), 'cert.tampered_kappa': Defect(key='cert.tampered_kappa', family='certificate', title='kappa perturbed so the stated budget no longer holds', why_it_looks_valid='kappa is an opaque constant most readers will not check.', caught_by='The erfc round-trip against the declared budget.', severity='soundness', tags=['derived-constant', 'transcendental']), 'cert.dropped_field': Defect(key='cert.dropped_field', family='certificate', title='A re-derived field deleted from the record to dodge comparison', why_it_looks_valid="Absence is easy to mistake for 'not applicable'.", caught_by='Comparing every re-derived field, treating a missing one as a mismatch.', severity='integrity', tags=['omission']), 'cert.vacuous': Defect(key='cert.vacuous', family='certificate', title='All certificates stripped; the bundle is empty but well-formed', why_it_looks_valid='An empty bundle is trivially internally consistent, so a pure format check reports success.', caught_by='Refusing a bundle that certifies nothing.', severity='vacuity', tags=['vacuity', 'the-quiet-one']), 'cert.self_consistent_forgery': Defect(key='cert.self_consistent_forgery', family='certificate', title='Physics inputs AND recorded verdict edited together, so they agree', why_it_looks_valid='Every internal check passes. The forger simply did the interval arithmetic correctly on fabricated inputs, so re-derivation reproduces exactly the verdict that was recorded.', caught_by='An out-of-band fingerprint ONLY. No amount of internal checking can distinguish this from a genuine certificate — which is why the reference verifier abstains (UNVERIFIED) rather than passing when no anchor is given.', severity='soundness', tags=['verdict', 'physics-input', 'requires-anchor', 'the-honest-limit']), 'cert.broken_manifest': Defect(key='cert.broken_manifest', family='certificate', title='A payload file edited after the manifest was written', why_it_looks_valid='The bundle metadata is untouched.', caught_by='Re-hashing every payload file against the manifest.', severity='integrity', tags=['payload']), 'cert.broken_merkle': Defect(key='cert.broken_merkle', family='certificate', title='Merkle root replaced', why_it_looks_valid='The root is an opaque hex string.', caught_by='Recomputing the root from the manifest.', severity='integrity', tags=['commitment']), 'cert.broken_outputs_commitment': Defect(key='cert.broken_outputs_commitment', family='certificate', title='A reported value edited without updating its commitment', why_it_looks_valid='The value is plausible and the rest of the bundle verifies.', caught_by='Recomputing the outputs commitment over the reported values.', severity='integrity', tags=['reported-values']), 'cert.noncanonical': Defect(key='cert.noncanonical', family='certificate', title='Bundle re-serialized with different byte formatting', why_it_looks_valid='Semantically identical JSON; only the bytes differ.', caught_by='A canonical-form round-trip, or a fingerprint obtained out of band.', severity='integrity', tags=['serialization']), 'receipt.unjustified_empty_clause': Defect(key='receipt.unjustified_empty_clause', family='receipt', title='Empty clause asserted with no derivation', why_it_looks_valid='A one-line proof of an unsatisfiable-looking formula.', caught_by='RUP-checking every lemma, including the empty one.', severity='soundness', tags=['drat', 'proof']), 'receipt.non_rup_lemma': Defect(key='receipt.non_rup_lemma', family='receipt', title='A lemma inserted that does not follow by unit propagation', why_it_looks_valid='The proof has the right shape and ends in a contradiction.', caught_by='Checking each lemma is RUP against the active clause set.', severity='soundness', tags=['drat', 'proof']), 'receipt.swapped_cnf': Defect(key='receipt.swapped_cnf', family='receipt', title='Formula replaced by a trivially unsatisfiable one', why_it_looks_valid='The proof genuinely refutes the formula presented — just not the formula that corresponds to the circuits.', caught_by='Committing the formula and the encoder identity, and checking both.', severity='soundness', tags=['encoding', 'the-subtle-one']), 'receipt.swapped_description': Defect(key='receipt.swapped_description', family='receipt', title='One circuit description swapped after the proof was made', why_it_looks_valid='Proof and formula are genuinely valid; only the claim about *what* was proven is false.', caught_by='Binding both descriptions into the commitment.', severity='soundness', tags=['binding']), 'receipt.forged_counterexample': Defect(key='receipt.forged_counterexample', family='receipt', title='Counterexample that does not satisfy the formula', why_it_looks_valid='A plausible-looking assignment over the right variables.', caught_by='Re-simulating the assignment against the committed formula.', severity='soundness', tags=['counterexample']), 'receipt.truncated_chain': Defect(key='receipt.truncated_chain', family='receipt', title='Trailing records removed from the hash chain', why_it_looks_valid='The surviving prefix is internally consistent.', caught_by='Requiring the chain to reach a terminal record.', severity='integrity', tags=['chain']), 'receipt.broken_chain_link': Defect(key='receipt.broken_chain_link', family='receipt', title="A record's predecessor digest altered", why_it_looks_valid='Individual records still parse.', caught_by='Recomputing each link.', severity='integrity', tags=['chain']), 'receipt.swapped_encoder': Defect(key='receipt.swapped_encoder', family='receipt', title='Encoder identity replaced with an untrusted one', why_it_looks_valid='The formula and proof are unchanged and valid.', caught_by='Committing the encoder identity so a substitution is visible.', severity='soundness', tags=['provenance']), 'seal.moved_threshold': Defect(key='seal.moved_threshold', family='seal', title='Acceptance threshold loosened after sealing', why_it_looks_valid='The specification is well-formed and the seal file exists.', caught_by='Recomputing the digest of the specification actually in force.', severity='soundness', tags=['preregistration']), 'seal.repointed_bound_seal': Defect(key='seal.repointed_bound_seal', family='seal', title='Specification doctored AND a matching seal minted', why_it_looks_valid='Specification and seal agree with each other perfectly.', caught_by='A binding that covers the result and the seal together.', severity='soundness', tags=['preregistration', 'the-hard-direction']), 'seal.altered_result': Defect(key='seal.altered_result', family='seal', title='Measured result edited after binding', why_it_looks_valid='The seal still matches the specification.', caught_by='Recomputing the binding over result and seal.', severity='soundness', tags=['preregistration']), 'seq.forged_undecided_as_equivalent': Defect(key='seq.forged_undecided_as_equivalent', family='sequential', title='An abstention relabelled as a proof of equivalence', why_it_looks_valid='Every obligation present carries a real, checkable proof. The base cases genuinely hold. Only the inductive step is missing, and the recorded verdict does not mention it.', caught_by='Re-deriving the argument rather than reading the verdict: with no step obligation discharged, EQUIVALENT does not follow, and the honest answer is UNDECIDED-AT-K.', severity='soundness', tags=['verdict', 'abstention', 'the-hardest-one']), 'seq.valid_proof_of_a_different_problem': Defect(key='seq.valid_proof_of_a_different_problem', family='sequential', title='A real proof, of a formula this design does not encode to', why_it_looks_valid='The DRAT checks. The formula is UNSAT. Everything about the obligation is internally impeccable — it is simply an obligation for different circuits.', caught_by='Re-encoding the obligation from the committed design and comparing bytes. A receipt that only commits the formula cannot catch this.', severity='soundness', tags=['encoder', 'physics-input']), 'seq.dropped_obligation': Defect(key='seq.dropped_obligation', family='sequential', title='An obligation claimed UNSAT but shipped without its proof', why_it_looks_valid='The receipt still lists the obligation and marks it discharged; only the proof body is empty.', caught_by='An UNSAT claim with no proof is a claim, and claims are not accepted.', severity='soundness', tags=['proof']), 'seq.edited_design': Defect(key='seq.edited_design', family='sequential', title='The design changed after the proofs were produced', why_it_looks_valid='Every proof still checks against the formula beside it.', caught_by='The design digest, and re-encoding: the formulas no longer correspond to the circuits now in the receipt.', severity='integrity', tags=['commitment']), 'seq.tampered_verdict': Defect(key='seq.tampered_verdict', family='sequential', title='A counterexample receipt relabelled EQUIVALENT', why_it_looks_valid='Nothing else was touched.', caught_by='The verdict is re-derived from the obligations, never read.', severity='soundness', tags=['verdict']), 'seq.broken_chain': Defect(key='seq.broken_chain', family='sequential', title='A record edited inside the hash chain', why_it_looks_valid='The payload is untouched and every proof still checks.', caught_by='Recomputing the chain digests.', severity='integrity', tags=['commitment'])}
@dataclass(frozen=True)
class
Defect:
One labelled way of being wrong.
def
summary() -> Dict[str, int]:
def
build(out_dir) -> dict:
Write the full atlas. Returns the index.
def
atlas_digest(out_dir) -> str:
Content digest over every file except the index itself.
ATLAS_VERSION =
'1.0.0'
def
score( atlas_dir, verifier: Callable[[str, dict], bool], *, families: Optional[List[str]] = None, jobs: int = 1) -> dict:
Run verifier over every case and compute the metric.
verifier returns True if it ACCEPTS the artifact. Exceptions count as a
rejection, since a verifier that crashes has not accepted anything.
jobs > 1 runs cases concurrently in threads. That is worth it only for a
verifier invoked as a subprocess, where the cost is interpreter startup and
the GIL is released while waiting — an in-process verifier gains nothing and
may lose. Results are assembled in index order regardless, so the score,
the row order and the missed list do not depend on scheduling.
def
command_verifier( argv_template: List[str], accept_returncode: int = 0, timeout: float = 30.0) -> Callable[[str, dict], bool]:
Adapt an external CLI to the scorer.
argv_template uses {path} as the placeholder, e.g.
["my-verifier", "--check", "{path}"]. Acceptance is signalled by exit code.
A verifier that hangs is scored as a rejection after timeout seconds
rather than blocking the run forever — an answer that never arrives is not an
acceptance.
def
format_report(res: dict, *, show_rows: bool = True) -> str:
def
load_index(atlas_dir) -> dict:
def
reference_verifier(path: str, case: dict) -> bool:
Accept iff the appropriate reference checker accepts.
What this atlas measures. Certificates are checked with
require_anchor=False — that is, on the artifact alone, with no
out-of-band fingerprint. That is deliberate: an anchor trivially detects any
byte-level change, so scoring with one would measure the hash function rather
than the checker. The interesting question is how much a verifier can catch
from the artifact by itself.
The consequence is stated openly: a self-consistent forgery — physics
inputs and recorded verdict edited together — is not detectable in this
track, by anyone, and the atlas contains such a case
(cert.self_consistent_forgery) to make that limit measurable rather than
merely asserted. Use anchored_reference_verifier() for the track where
it is caught.
def
anchored_reference_verifier(path: str, case: dict) -> bool:
Reference checker with the out-of-band anchor supplied.
The case carries expected_fingerprint — the fingerprint of the genuine
artifact, recorded before mutation. That stands in for a value a real user
obtains from a signed report or a separate channel.
def
accept_everything(path: str, case: dict) -> bool:
Negative control: the degenerate verifier that trusts everything.
def
reject_everything(path: str, case: dict) -> bool:
Negative control: the degenerate verifier that trusts nothing.
__version__ =
'1.0.0'
def
hf_export(atlas_dir, out_dir) -> dict:
Write JSONL shards plus a machine-readable schema.
JSONL rather than a JSON array: it streams, it diffs line-by-line in review, and it is what dataset loaders expect.
def
to_rows(atlas_dir) -> List[dict]: