cert_atlas.defects
The defect taxonomy — every way a certificate can be wrong while looking right.
Each defect is a named, reproducible mutation applied to a valid artifact. The atlas exists because verifiers are usually tested on artifacts they accept. What matters is what they reject, and nobody publishes a corpus of near-miss forgeries.
Every entry records: what was mutated, why a naive verifier might miss it, and which check is supposed to catch it. A defect nobody's verifier catches is more interesting than one everybody catches, so the atlas keeps both.
CERT =
'certificate'
RECEIPT =
'receipt'
SEAL =
'seal'
SEQ =
'sequential'
@dataclass(frozen=True)
class
Defect:
One labelled way of being wrong.
DEFECTS: Dict[str, Defect] =
{'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'])}
def
summary() -> Dict[str, int]: