Atom version-integrity redesign campaign - #100
Draft
nrdxp wants to merge 276 commits into
Draft
Conversation
Small grounded corrections across ADR-0007, no normative change:
- §6: the sibling constraint is a path-segment containment check with
normalization, not a raw string-prefix one (P=foo must not match
foobar) -- a publisher footgun the prefix wording left open.
- §4: [temporal-vector] is not 'the only non-section-anchor bracket'
(false; so are [verify-before-fetch], [k-derivation-signed-only]);
state the first log leaf MUST be a charter; drop the reified
'anchor = czd(charter)' phrasing.
- §3: head is the fifth pay.typ value but structurally distinct, not 'a
sixth category / seventh scope' (off-by-one wording).
- §2: note head is a pay.typ value yet structurally distinct (§3/§11).
- §7.5: ref^{commit} peels to the closure-commit but bypasses the fact
chain -- a consumer needing current trust status must walk the tags.
(adr-0007 full-review + s7 cosmetic batch: C5/C6/C7/C8, security-F5.)
ADR-0008 §2 used the charter-declared 'attesters' role (ADR-0007 §3, for in-log vouch anchoring) and §1 used the 'assertor' role (trust-model consumer-side admission) without stating they are different roles. Add a sentence: anchoring is valid placement; assertor admission is whether the verdict credits it -- a vouch can be validly anchored yet admitted by no consumer, and neither substitutes for the other. (adr-0007 full-review cosmetic: ADR-0008 attesters vs assertor.)
Sharpen the §7.4 leaf0 verification step: content_commitment is folded from the publish record's own signed declared content_hashes, so leaf0 is checkable from signed data in Phase A before any content is fetched; the bytes are separately re-derived against those same signed content_hashes at Phase B. Removes the ambiguity in 'recomputed'. (follow-up to the §7.4 B1 rewrite.)
Fold in nrd's evolved, authoritative framing of content_hash (T3): it is a Merkle root over the subject's LOADED CONTENT (bytes plus in-tree structure), computed by a supported, pluggable algorithm (eml's k-ary by default), EXPLICITLY independent of git's own object/tree hashing -- git is storage only, never the hasher, and its tree OID is never reused as the integrity root (that OID stays a checked cache, the tree field). Rationale stated in-doc: this decouples content integrity from any backend and its hash choice, and is what maps content_hash cleanly onto the composition model's content-addressed values. Also folds in the hash-agility / SHA-1 scoping note (security considerations, not a new MUST): content integrity is decoupled from the git object hash, so a SHA-1 collision cannot forge content; the residual SHA-1 exposure is confined to the position OIDs (upstream history pins), with blast radius on provenance/ordering, never content; mitigants (sha1dc, fail-closed ancestry, SHA-256 = zero residual). §8's F4 collision-bound claim is qualified accordingly and cross-references the note. A position-layer strong hash is recorded as noted-not-adopted future hardening; the normative position definition is unchanged. Glossary 'Atom (the unit)' synced to the same framing so the source-of-truth does not re-diverge from the ADR. (adr-0007 T3, refined by nrd 2026-07-22; security-considerations.)
The reconciliation verdict's amendment manifest listed trust-model.md (git-storage-format, atom-transactions, atom-backend-contract, trust-model, lock-file-schema); the freshen task list dropped it. Restore it to the 'Obligates amendment of' field -- the signature-anchoring and role-authorization semantics ADR-0007 §3/§13 lean on are trust-model territory, obligated to amend with the rest. (adr-0007 reconciliation verdict D2-2a.)
Elevate the §7.5 completeness delta-scan to a named hard invariant, [completeness-scan-mandatory], with the same standing as [verify-before-fetch]: on every resolution of a pub ref, a consumer MUST scan the record log from the fact-tag chain's last known leaf to the current tip for anything targeting this (label, version). Names the form of an obligation the prose already stated as a MUST (parity, not new normative content), and §10's Completeness bullet cites the bracket. (adr-0007 s7 W1 r2-F2.)
nrd ratified the 2026-07-22 freshen pass (the two adversarial review rounds' fixes plus the model/spec reconciliation). Drop the contingent qualifier; ADR-0007 is now ACCEPTED.
The surety thesis's core, machine-checked: genuineness is not record-determined, therefore it admits no evidence scheme -- the Thompson / Surety-Ceiling answer, for the atom system, as a direct instantiation of the already-proven EON/EALM determination gate (snapshot_characterization_determined). A separate lake package path-requiring EonEalm (the eml-bridge pattern). Compiles zero-sorry; #print axioms is [Context, Entry] (the two abstract model types, no classical axioms needed on this path); the non-determination witness enters as an explicit hypothesis, not an axiom.
Mechanize the structural surety ceiling in Lean: the classify biconditional over an inductive, acyclic-by-construction Artifact, the trust-surface / basis / Total definitions, and the ceiling theorems over them. This is the vouch-path layer. A non-seed atom whose Total verdict holds provably carries an admitted vouch in its assumption basis (total_carries_vouch_in_basis), and an atom whose establishment fails can never be Total (laundered_never_total). Grounds the classification prose in a machine-checked model, with the Alloy differentials as the companion check. Companion prose: docs/models/surety-of-source.md. Companion Alloy: docs/specs/alloy/surety_core.als, surety_classification.als.
Mechanize the forced generator's denotation: the partial map it computes, degeneracy as finite range, genuine as its complement, a proved extensionality lemma, and the laundering witness (a realizing yet degenerate generator). This is the object the ceiling's genuineness axis measures. It carries no computation model by design, so Rice-style undecidability (surety-of-source.md Theorem 1) enters as cited evidence, never as an internal decision the model pretends to make. Phase-1 groundwork for binding the ceiling's laundered shape to generator degeneracy. Companion prose: docs/models/surety-of-source.md section 8.
Bind the forced-generator model to the surety ceiling, closing the generator-grounding phase. The genuineness axis is now grounded in a real computational object, not an opaque predicate: - rcas_forces_established: classify reaches RCAS only through the vouch clause, with no generator premise — the ceiling is provably blind to degeneracy, so it cannot secretly decide the undecidable. - genuineness_underdetermined: a genuine and a degenerate generator realize the identical output, so observing an atom's bytes cannot distinguish honest from laundered — the concrete determination axis core. - unboundedDomain_byteInput: the non-vacuity of degeneracy transfers to arbitrary-length byte payloads, the faithful input type. A launderedShape-to-degenerate correspondence was sought and found false in both directions (documented in-file): degeneracy never enters classification, only the vouch does. Claim R (Rice on finite-range indices) is cited, not mechanized. Companion prose: docs/models/surety-of-source.md sections 8, 10.
The ceiling theorems total_carries_vouch_in_basis and laundered_never_total are universally quantified — true but worthless if their hypotheses are unsatisfiable. Exhibit a concrete Unit-typed instantiation proving they bite: - a non-seed atom that classifies RCAS, is Total, and whose basis contains an actual vouch, with the general theorem applied to it to reproduce the witness — it fires, not just "could"; - a non-seed laundered atom (establishment fails) that the laundered_never_total theorem shows is never Total. Both hypotheses are thus satisfiable and both conclusions fire on reachable configurations. Note the positive atom is Total via an empty trust surface; a witness with a non-empty base-bounded surface would exercise the characteristic case further.
The prior non-vacuity witness reached Total via an empty trust
surface — an atom trusting nothing beyond its own vouch. Add the
characteristic case the ceiling actually claims: Total via a
NON-EMPTY surface every member of which is a genesis seed, so the
irreducible trust is a real but base-bounded residue (T(a) =
{seed} subset base), not zero.
A genesis-seed leaf, cited as a build input, is never RCAS (leaves
classify trustImport unconditionally), so it survives the trust
surface filter while the atom itself is filtered out — leaving a
one-element all-seed surface. The general total_carries_vouch_in_
basis theorem is applied to it and still fires.
This closes the honest residue flagged on the empty-surface
witness: Total is demonstrated in its trust-bounded-to-a-known
base form, not only its zero-trust degenerate case.
Add section 11 to the surety-of-source model, reconciling the prose with the now-complete Lean 4 mechanization under docs/models/lean-surety/. Records what each of the six files proves, the decoupling finding (classification is vouch-decided, never degeneracy-decided — sharpened from prose to a type-level fact), the proven-vs-cited boundary (Theorem 1 / Rice is cited, not mechanized, by design), the two-premise assumption base, and one honest bound: the Lean corpus is not yet wired into CI. The mechanization gives unconditional, machine-checked teeth to claims the model and ADR-0008 already asserted; nothing normative changes.
Add a reviewer entry point for the Lean surety-ceiling corpus: a file-by-file guide with the actual theorem identifiers, build instructions, and — prominently — the cross-repo build prerequisite (the package path-requires the Cyphr EON/EALM Lean corpus, so both repos must be checked out as siblings). Points to surety-of-source.md §11 for the prose rather than duplicating it.
Correct the recursion-theoretic ground for "no certificate at any size retires the genuineness question." Plain Rice bounds decidability, not certifiability — and undecidable is not uncertifiable (the halting set is undecidable yet recursively enumerable, certified by a trace). What forecloses a certificate is failing to be recursively enumerable at all: finite-range degeneracy sits above that level of the arithmetical hierarchy (both it and its complement fail to be r.e.), and Rice-Shapiro's finite-subfunction criterion is what shows it. The permanent signed vouch is forced because certifiability itself is foreclosed, not because the check is merely hard.
docket's contract now requires a quadrant per genre (27f3a65); the composer applied the four values and validated them. Commit the config so the campaign's genre gate has a tracked artifact to bind.
ADR-0007 built one write-gated, project-owned log for every append at every scope (S7.1, S19). That is unimplementable against atom-transactions.md's own fact-kind-table, whose open- tier advisory fact requires admission from signers who hold no push access to the subject project's repository. ADR-0009 splits the plane by algebra: an ordered, append-only spine (genesis, amendment; the owner-set's one write gate) and a history-independent cloud (fact; any anchored role-holder, union-merged, no write gate). This dissolves the contradiction and matches Composition Model S6's own commutative, set-union law for anything fact-shaped, which the prior single-log design never honored for atom's own facts. Superseded in part, not wholesale: ADR-0007 S3's taxonomy and S19's write gate are replaced; every other subsection retains its content, inherited by citation, per the section-by-section map in the new document. A separate, named tension with ADR-0005 S2's action-identity framing is tracked as issue #101 and is not resolved by this change.
The initial draft derived ADR-0007's per-section fate from its own independent reading, missing the architect's authoritative N0b dispositions ruling, which this node's dispatch never named. Ten of twenty-one subsections split rather than surviving or moving wholesale; the initial table under-counted this and several individual claims were wrong. Corrected: S7.4's closure artifact (the embedded two-leaf eml tree) is deleted, not inherited — publish verification proves inclusion against the spine directly, with no materialized closure object. S10's completeness scan is retired outright, not narrowed to the spine. S13's interface-descriptor clause is superseded by the already-landed fact classification (interface manifests are facts). S11-S12's head mechanism loses two of its three roles outright; what attests recency is named as the one genuinely open residue rather than asserted as settled. S21's ref-format collision concern is resolved by the flat, content-addressed store keying, not left open. The supersession table now uses the ruling's own four-way disposition vocabulary (survives / moves to spec / split / superseded and deleted) instead of ad hoc language, and citations to sections whose content moves to specification no longer rest on that content as still-operative ADR material.
ADR-0009's "What changes, and what does not" table gives every ADR-0007 Decision subsection a fate; several rows mark specific spans superseded or deleted with no destination. Remove exactly those spans so ADR-0007 stops asserting mechanisms ADR-0009 already refuted, while every one of its 21 Decision subsections keeps content per ADR-0009's own "no subsection is deleted" rule. Removed: §3's facts-forever taxonomy paragraph (genesis-once reasoning kept); §7.4's closure artifact and §7.5's fact-tag chain in full; §10's completeness-scan bullet; §16's Tier-2 fail-closed clause; §19's every-append write-gate bullet; §21's ref-format paragraph (GC-by-reachability kept). Left unmade, per the coherence-halt rule: §13's package-atom mandatory-artifact bullet and §14's ancestry predicate are also marked superseded by the table but excising either breaks a surviving sentence's own grammatical subject; reported instead of authored around.
docs/ is gaining ~27 machine-readable claim blocks (fenced ```claim YAML naming a claim's kind and evaluator, per docket's MVP.md ss1.2). process_docs.py copied bodies verbatim, so every block would publish as an unstyled code fence: a bare normative statement with no sign of how strongly it is actually discharged, which reads as MORE authoritative than the source (issue #103). Renders instead, in process_docs.py ahead of link rewriting (a raw `cites: [a, b]` line would otherwise be walked by the markdown-link regex): kind and evaluator become visible badges, with the evaluator badge color-graded along its preference order (proof down to none) so discharge strength reads at a glance. Emitted as inline HTML rather than templated, because sukr's markdown backend (pulldown-cmark) passes HTML blocks through verbatim and has no shortcode mechanism to hook from the template layer. A block that fails the schema (unknown field, bad enum, missing required key) renders as a flagged error callout with its raw source shown, rather than vanishing or falling back to a plain code fence — silently dropping it would hide the exact defect the claim register exists to surface. `cites` render as plain text, not links: resolving a citation to a URL needs corpus-wide path knowledge that belongs to the quadrant/frontmatter derivation, not this surface. The parser is a small hand-rolled reader scoped to the claim schema's three flat keys, matching this file's existing no-dependency style rather than adding a YAML library for a closed three-field shape.
ADR-0009's spine/cloud split needs two new homes: the published object plus store-keying constraints, and the subject-scoped fact channel plus ingestion completeness. Neither existing spec covers the atom plane's own store (storage-model.md explicitly disclaims it). Kept minimal, per the claim-register campaign's D7 queue.
Adds the 7 new atom-plane invariants ADR-0009 introduces: the spine's chain-completeness and fold discipline, the cloud's terminal withdrawal and history-independent root, and the store-sufficiency and single-discovery-question bounds. Also corrects the reproducibility contract's equality, which design-of-record §7.4 identifies as wrongly keyed on action_id instead of req_digest — the old phrasing is left in place with a superseding note rather than rewritten, since the surrounding violation/adjudication prose (and trust-model.md's mirrored constraints) still need the same re-key, registered in §8 as owed follow-up.
lock-file-schema.md, trust-model.md, and atom-backend-contract.md gain the remaining 7 constraint claims from ADR-0009's queue. lock-file-schema.md's [sets] section gains lock-sets-three-fields and lock-pins-gating-facts, which supersede [lock-set-charter-head] and retire [lock-set-snapshot] outright (a cloud root is not a stable pin) — both old clauses get a SUPERSEDED annotation in place, and the example TOML is updated to the new three-field shape. Also adds manifest-test-params-separate, extending the existing manifest/lock boundary discussion. trust-model.md gains verdict-carries-basis and freshness-refusal- scoped as a new subsection extending the bare Verdict enum and the PolicyRule language. atom-backend-contract.md gains czd-oid-phantom-typed next to the existing [backend-seam-typed] it restates — graded none rather than type after checking atom-id/src/digest.rs, whose AtomDigest is a single untyped digest shared across Czd/OID/content-hash uses, not the disjoint sorts the design-of-record claims are already compiled.
ion-sad.md and atom-sad.md gain the 6 requirement claims from ADR-0009's queue. ion-sad.md: two-clients-one-store (§1.5), seven-operations (§2.6), plugin-seam-at-composite (§6.10 — a distinct plugin axis from §6.5's lock dependency-type plugins, kept separate rather than merged into it), blast-radius-visibility (§6.11), and closure-faults-user-loop (§6.12). atom-sad.md: store-format-public-contract (§6.9), scoped narrowly to cite only atom-model.md and ADR-0009 — the existing §6.6 "Store Keying" teaches the now-retired blake3(publish_czd) reduction and is flagged, not rewritten, since realigning it is separate, already- obligated work (ADR-0007's own amendment list).
The doc-link audit's fix (anchor-form prose links now satisfy docket's C5) removes the collision that forced dropping these at authoring time. Restores the 8 declarations, all as anchor-form links (same-file: #id; cross-file: relative-path#id) rather than the old bare-id form. - atom-model.md fold-inputs-on-spine depends spine-chain-complete: the claim restricts fold inputs to spine records specifically because the spine's chain-completeness is what makes that restriction buy anything; without it the scoping rule is hollow. - atom-model.md store-sufficiency depends spine-chain-complete, withdrawal-terminal: sufficiency is literally false if either gives out — a gappy spine can't ground authorization, and non-terminal withdrawal would need future facts to know present truth. - atom-model.md discover-one-question because store-sufficiency: the general law stands on its own; store-sufficiency is cited as a witnessing instance, not a precondition. - atom-store-format.md publish-inclusion-required depends spine-chain-complete: "included in the spine" only means something because the spine can't have silent gaps. - atom-store-format.md verification-no-discover depends discover-one-question: the claim's own term "discovery capability" is discover-one-question's definition. - atom-store-format.md fact-keyed-by-own-czd because store-keyed-by-czd: facts would still be self-keyed even absent the general flat-map law; it's the pattern, not a precondition. - fact-exchange.md fact-exchange-advertised-only and ingest-closure-complete, both because fact-exchange-subject- scoped: both properties (advertised-vs-held, closure-completeness) are stated relative to the subject-scoped channel but would still hold under a differently-shaped exchange. Verified: 0 C5 failures before and after (the collision meant no declared edges existed to fail); 27 claims still indexed; corpus- wide docket check unchanged at the 39 pre-existing docs/adr/** findings; doc-link audit clean on all three files.
process_docs.py hardcoded quadrant = "Explanation" into every document's frontmatter, contradicting docket.ncl's per-genre quadrant declarations (three of the four genres are "reference"). Derive the frontmatter value by matching each source path against docket.ncl's genre globs instead; a path matching zero or more than one genre now aborts the build rather than silently defaulting, since a silent default is exactly what produced the original defect.
process_docs.py's claim-block parser still accepted the retired `cites` field while the corpus (atom-store-format.md, fact-exchange.md, atom-model.md) is authored against docket's current schema (MVP.md §1.2), which split it into `depends` and `because`. Every real reference in those files rendered as a malformed claim block on the published site. Accept both new fields and render them on separate, labeled lines rather than merged, since a `depends` target vanishing breaks the claim while a `because` target vanishing only leaves it under-justified. `cites` is retired outright rather than kept as an alias: a parser that still took it would silently accept a stale document instead of flagging it, undermining the same unknown-field-is-an-error rule the parser already enforces elsewhere.
docs/glossary.md sits directly in docs/ and matched none of the four genre patterns, so the site build's per-source quadrant lookup hard-stopped on it rather than guess a quadrant. Genre is `reference` (a glossary is canonical lookup material) with `kinds = []`: the glossary defines terms rather than asserting normative rules, and today carries zero claim blocks and zero RFC-2119 keywords, so the empty kind list describes what the document is rather than restricting it. It also means a future normative keyword added to the glossary fails loudly instead of drifting in silently.
Calibration run for the corpus-wide registration pass: claim blocks for every bold-form definition in atom-backend-contract.md, graded against atom-conformance's dedicated GREEN/RED battery rather than the doc's own stale (still-"pending") Verification table. depends/ because stay empty per the registration effort's own phasing. Five claims (backend-store-injective, backend-ancestry-queryable, backend-refs-atomic-multi, backend-carriage-bit-perfect, backend-liveness-protection) grade `test`, each backed by a docket: marker beside its passing atom-conformance test. The remaining eleven grade `none`: some have no battery coverage at all, others have a passing mechanism test undercut by a named, current gap (a TOCTOU window, an unimplemented charter chain/ref layout, an untyped digest) that the claim's own text explicitly binds - grading them above `none` would assert a conformance the code does not yet have.
spine-chain-complete and spine-genesis-first are structural chain- integrity invariants shaped exactly like the sibling atom- transactions.md claims atom_structure.als already model-checks (genesis-once, unbroken prior-links) — a natural extension of that existing Alloy model, not new formal-methods work. fold-inputs-on- spine is a fold-function input-domain restriction a SpineRecord type enforces structurally. reproducibility-req-keyed is a clean fixed-req_digest-equality law, textbook property-test. metadata-partition-law and signature-anchoring-law are their own Proof Obligations section's audit obligations over a checkable inventory — a decorrelated reviewer enumerating and classifying a finite schema, not a single runtime test. runtime-declare-required, withdrawal-terminal, store-sufficiency, and discover-one-question are concrete behavioral claims (a closure-fault gate, a terminal-state check, airplane-mode operation) a fixture test discharges. proof-obligations-scope stays none: a scoping/definitional claim naming which obligations belong to this model, adding no checkable predicate of its own.
Twenty single-block none claims graded. Nineteen of twenty concrete
git-level behaviors (forbidden ref/commit shapes, ancestry-walk
discipline, fetch/transfer mechanics, chain traversal) a fixture
battery discharges directly (test); client-evaluates-not-replays is
an order-independence property (trust state must not depend on
chain traversal order) — property-test. refs-sole-mutable is the
git instantiation of the same whole-system negative graded review
in atom-backend-contract.md; kept consistent.
anchor-is-genesis and anchor-oldest-root stay none: both are
explicitly retired-rule prose ("(retired 2026-07-08 — superseded by
the charter amendment)") documenting a historical supersession, not
a live behavior — the operative Anchor := czd(charter_0) rule they
describe is independently checked elsewhere.
Twelve none claims in this file are NOT touched here and are not
among the sixty-six graded in this node — see the dispatch report
for the corpus defect that makes editing them unsafe (a vestigial
block trailing an immediately-following RETIRED heading silently
overrides the real claim's registered evaluator).
Sixty-six claims across five atom-layer documents now declare an evaluator. The question asked of each was what would check it, not how to make it pass — no tests were written and no markers wired, because the implementation these claims describe does not exist yet. Nine stayed undeclared with individual reasons, and those are the honest half. Two are retired-rule prose whose operative content is checked elsewhere; one names in its own text the untyped digest that keeps it ungraded, verified still true; one is definitional with no independent predicate to check. Grades follow the claim rather than its neighbours: property tests where a document's own testing strategy names generative testing, types where a Rust shape genuinely closes it, model-check where an Alloy model already checks the exact assertion.
The §6 retirement kept the original multi-tree derivation as plain own-voice prose, so the normative-prose scanner still fired on MAY/MUST/MUST NOT wording that is now dead decision history, not live requirements. Wrap the preserved derivation (the four paragraphs following "What follows through the rest of this section...") in a blockquote, matching the idiom §2's extension-metadata retirement already uses in this same document. The "Reversed" ruling and the "What is cut"/"What this costs" analysis stay as current-voice prose outside the quote — only the historical text moved.
Its last three misplaced requirements were not live rules — they sat inside the multi-tree derivation retired this afternoon, preserved as plain prose so a reader could see what the reversed decision actually said. The register's scanner is genre-agnostic and exempts only quoted and fenced text, so dead words kept reporting. Quoting them was the fix rather than rewording them. A retirement record earns its keep by showing the old decision in its own words, and paraphrasing the keywords away would have been a loss dressed as a correction. The boundary is where it should be: the retirement notice and the reversal reasoning stay in the document's current voice, and only the dead decision's own wording sits inside the quote. The document that began the day issuing twenty-seven requirements now issues none.
All 28 evaluator: none claims graded, none left unresolved.
model-check (8): the genesis-once/fork-detection family --
atom-genesis-and-facts, claim-owner-fact, charter-owner-fact,
charter-owner-fact-linear, identity-stability -- mirror the shape
already model-checked here (charter-fork-distinction, chain-
monotonicity, publish-claim-coherence, claim-charter-authorization):
consumer-side fail-closed divergence detection over a fold of
signed facts, an Alloy/TLA-natural extension, not new formal work.
property-test (4): charter-owner-threshold (once-crossed threshold
is a monotonic ratchet), backend-bit-perfect and atom-snapshot-
reproducible (canonical round-trip/determinism shapes), format-
unknown-field-tolerance (round-trip preservation through
serialize/deserialize).
type (3): charter-typ (matches claim-typ/publish-typ's literal-
discriminator grade), manifest-minimal (the Manifest trait
signature itself is the enforcement), owner-compatibility (an
owner-fact payload has no czd field to mutate).
test (10): concrete field-derivation and fixture-shaped MUST rules
(dig-is-atom-snapshot, path-is-subdir, anchor-resolvable,
atom-detached, fs-source-contract, publish-delegate-role), resolver/
decision-table behavior with golden vectors (amendment-field-
classification, fact-kind-table, fact-claim-owner-gated), and
composite-source-concurrent's concurrency-bound behavior. crypto-
layer-separation and no-cross-layer-crypto get test, not linter --
this corpus's evaluator contract (docket/contracts/claim.ncl) has no
linter rung; a Cargo.toml dependency audit is the closest valid grade.
review (2): format-version-discriminator and format-reserved-names
are prospective design principles for formats that don't exist yet;
their own text names the enforcement mechanism ("ordinary review of
new namespace/field/kind additions").
No claim was too vague to grade -- all 28 carry concrete MUST/SHOULD
mechanisms, none merely definitional.
All twenty-eight of its undeclared claims now name an evaluator, and none were found too vague to grade — every one carried a concrete mechanism, which is the first document today where the underwritten list came back empty. The grades were argued from each claim's own text rather than from its neighbours. Genesis-once and the owner-fact rules are model-checked because their own applications already are and they share a fork-detection shape; threshold permanence, byte-perfect round trips and snapshot reproducibility are property tests because they are monotonicity, round-trip and determinism in the canonical sense; two format rules stay review because they govern formats that do not exist yet and there is nothing to check today. One claim was graded at the harder rung deliberately: identity stability has a trivial immutability half and a substantive uniqueness half, and grading the easy half would have left the hard one uncovered.
14 of 27 atom-layer claims graded evaluator: model-check asserted Alloy coverage nothing in atom_structure.als or atom_backend_seam.als actually provides, independent of today's record-anchored-publishing redesign. Audited each against the models' own @docket tags, the run_model_check.sh categorization (several claims rest only on TLC configs now marked HISTORICAL/SUPERSEDED), and TLA+ invariant lists that already retire some of these by name (AtomIdPerSourceUnique, IdentityStability). Several of these were already self-documented elsewhere in the corpus as ungraded (atom-transactions.md's own Verification notes, and atom-sad.md's Alloy certification row) but the claim blocks were never updated to match. This closes that gap for the claims it names; no claim text, id, depends, or because edge changed, and the Alloy models themselves are untouched pending a separate repair pass.
Twenty-seven atom claims asserted that a model already checks them. Thirteen do. Fourteen did not, and now read none. None of the fourteen trace to today's redesign, which is what this audit was launched to find. They are older, and the corpus had already said so in prose while the machine-readable grade said otherwise: three claim blocks state in their own text that they are not machine-verified, the model-check script names three more that should read none, and two solver configs retire two invariants by name in their own comments. Four more were backed only by configs the script itself partitions as historical and superseded — regression cover on an abolished design. So the defect was never staleness. It was that prose and grade disagreed, and only the prose was kept true. A reader following the documentation would have known; a reader trusting the register would not.
evaluator: <v> read as coverage in a metric meant to track implementation progress, but a claim's design axis is a separate question nobody answered. For claims backed by a code-run evaluator (test, type, property-test), the design axis is absent (unanswered), not `none` (answered as unchecked) — so migrate to verification.implementation: <v> without asserting a design grade. 175 claims migrated by a mechanical script (.scratch/migrate.py, untracked) over the top-level `evaluator:` key inside ```claim fences only. docket check --json: 465 claims, 86 findings before and after; the finding set is identical modulo line-number shifts from the added `verification:` lines.
evaluator: none is the default for a claim with no code-run evaluator: the claim's implementation target exists and nothing checks it. Migrate to verification.implementation: none, per the same axis split as the previous commit — the head approved this default corpus-wide, so it applies uniformly rather than case by case. 223 claims migrated by the same mechanical script over the top-level `evaluator: none` key inside ```claim fences only. docket check --json: 465 claims, 86 findings before and after; the finding set is identical modulo line-number shifts. 67 claims (model-check/review/proof) are left in legacy `evaluator:` form — that judgment set belongs to a concurrent walk.
A claim's evaluator answered how strong the evidence is and never what the evidence was about. A model-check grade then read as coverage in a metric meant to track implementation progress, while no code had been run against the claim at all. The register grew a second axis to make that difference sayable; this moves the 398 claims that need no judgment to say it. Test, type and property-test evaluators run against code, so they become implementation targets. The design axis is left absent rather than none: whether a design-level checker should exist for a claim a test already covers is a separate question nobody has answered, and none would claim an answer. An evaluator of none becomes an implementation target of none: a claim nothing checks has an implementation nothing checks. The 67 model-check, review and proof claims keep their legacy field. Which axis each of them belongs to is a reading, not a rewrite, and the runner accepts both shapes while that reading is in progress.
The remaining 67 claims graded model-check, proof, or review carried that grade in a single evaluator: field, so the register's implementation-progress metric read them as covered. Twenty of them now say plainly that their design is model-checked and nothing checks their implementation; the other 47 split cleanly by which axis their one evaluator actually verifies. The per-claim mapping was decided outside this change and applied here as a mechanical transform.
An adversarial review of the axis assignment found five claims given an absent implementation key that should carry none. Absent asserts no program behaviour could ever falsify the claim; none says the target exists and nothing checks it. The first silently excuses a claim from ever being verified, so it must be earned. surety-theorem3a-forced-attributability names its own refutation surface as an implementation of the closure walk, and requires any conforming implementation to expose B(a) so the check is possible. It was given an absent key on document class without being read. metadata-partition-law carries normative obligations, and one of them -- the fact-append versus moved-tip-warning carve-out -- is called an open gap by a claim in layer-boundaries.md. Treating it as discharged contradicts the corpus. surety-establishment-vouch-required, surety-classify-law and surety-gate-fail-closed operationalize predicates that ADR-0008 restates as MUSTs on real verifiers. The review graded the last two uncertain; under uncertainty none is the correcting choice, because a wrong none is a visible gap and a wrong absent is silence.
Sixty-seven claims carried an evaluator that said how strong their evidence was and never what it was evidence about. Most of them were model-check or review, and both read as coverage in a metric meant to track implementation progress while no code had been run against them at all. Twenty now say plainly that their design is model-checked and their implementation is checked by nothing. Twenty-six say a human read the code and no tool does. Twenty-one carry no implementation target, because a program could not falsify them or because a separate claim already carries that half. The reading behind this was not a reading. Three attempts to classify these by prose each produced a complete table with no reported ambiguity and each was systematically wrong -- first crediting model evidence to the code axis, then stripping the code axis from claims describing a daemon nobody has written. What settled it was mechanical: a spec document states in its own header that it constrains implementation, a model document states properties no program can falsify, and the register's own because graph names which claims already have an implementation half. Exactly three do. An adversarial review then found five claims that rule had excused wrongly, each argued from its own text rather than its location, and they carry an implementation target of none. The asymmetry is the reason to prefer that under doubt: a wrong none is a gap somebody closes later, and a wrong absence is a claim quietly exempted from ever being checked.
docket flagged 5 normative-prose findings in ADR-0002: SHALL/SHOULD/ SHALL NOT in the ADR's own voice, illegal because docs/adr/**'s genre permits no claim kinds. The whole document is dead scope, not merely stale wording: ADR-0006 §3 removed the "optional legacy passthrough- snix executor" that Tiers 1, 2, and 4 survived ADR-0005 scoped to, so "ADR-0002's residual tiers lose their referent and the ADR is superseded wholesale" (ADR-0006's own supersession note). The document's status line already said this; its Decision-section notes did not — they still claimed Tiers 1/2/4 "hold," contradicting the header. Reworded every SHALL/SHOULD/SHALL NOT to past tense describing what was specified, and rewrote the two stale inline notes (Decision- section opener, Tier 3 heading) so they agree with the header instead of contradicting it. Nothing here restates the tiers as live requirements, matching the treatment ADR-0007 already received. normative-prose in this file: 5 -> 0.
docket flagged one normative-prose finding: "developers MAY provide scheduling hints" in the ADR's own voice, illegal because docs/adr/** permits no claim kinds. The sentence is not a protocol rule anyone must satisfy — it describes an optional developer affordance that eos-scheduler.md's own type already models as optional (`atom_metadata: Maybe<SchedulingMetadata>`, a Maybe is the type-level statement of "may be absent"). Nothing here needs an evaluator: a developer either supplies the tag or does not, and both are valid. Reworded "MAY provide" to "can provide" — same meaning, no BCP-14 claim implied. normative-prose in this file: 1 -> 0.
docket flagged one normative-prose finding: a struck-through "MAY exist as an optional legacy escape hatch" sentence, illegal because docs/adr/**'s genre permits no claim kinds — strikethrough markup isn't a citation, so the checker still reads it as own-voice prose. The sentence already carries its own supersession note (ADR-0006 §3 withdrew the passthrough-snix executor entirely) and was never a live permission to begin with: it describes an option that was considered and then struck out in the same document. Reworded "MAY exist" to "was considered" — past tense matching the withdrawal already stated around it. normative-prose in this file: 1 -> 0.
docket flagged 3 normative-prose findings in ADR-0008: MUST in the
ADR's own voice, illegal because docs/adr/**'s genre permits no claim
kinds. All three are duplicates by the ADR's own admission, not new
rules:
- Sec 2's opening MUST ("a source-class-vouch MUST be anchored") says
of itself that it "instantiates the signature-anchoring law rather
than adding to it" — it is trust-model.md's
[trust-anchored-input] applied to one more fact class. Reworded to
cite that claim instead of restating it.
- Sec 2's closing MUST ("consume only anchored, unretracted vouches")
bundles two things: the anchored half is the same
[trust-anchored-input] duplicate. The unretracted half was a real
gap — no existing claim excludes a retracted fact from acceptance,
even though every fact in the protocol is retractable
(ADR-0007 sec 3's `retracts` field) and trust-model.md's own
7-step acceptance procedure never checks it. Added
[trust-excludes-retracted] to trust-model.md to close that gap, and
cited both claims from the ADR instead of restating either.
- Sec 3's MUST ("make T(a) and B(a) available to policy") is
[verdict-carries-basis] under this ADR's own T(a)/B(a) notation —
"a verdict carries its trust surface, its assumption basis" is the
same obligation. Reworded to name the correspondence and cite it.
[trust-excludes-retracted] omits a because: cross-file citation to
ADR-0007 sec 3 deliberately: every existing cross-file because:/
depends: in this corpus already trips docket's C5 check (28 baseline
instances, a known corpus-wide gap in how C5 matches cross-file
citations against prose links, not something this pass owns), and a
same-file [trust-anchored-input] depends: plus prose citation says
everything the constraint needs without adding a 29th instance of a
pre-existing defect class.
normative-prose in ADR-0008: 3 -> 0. Claim count +1 (relocated
constraint, verification: implementation: none — nothing checks it
yet).
docket flagged 2 normative-prose findings in ADR-0003: MUST in the ADR's own voice, illegal because docs/adr/**'s genre permits no claim kinds. Both sat in a "### Invariants" section carrying claim-shaped [id] brackets that were never registered anywhere — eos-sad.md §1.5 independently restates the same two rules in its own prose, which is exactly the drift this defect class produces: the same requirement asserted twice, nowhere checked. Added §4.5 to layer-boundaries.md with both as proper constraints: [deployment-no-codepath-divergence] (structural: same trait interfaces/pipelines across modes, no mode-conditional business logic) fits this spec's existing structural-ownership domain directly. [deployment-mode-bisimilarity] (behavioral: identical outputs across modes) is its consequence, backed by publishing-stack-layers.md's coalgebraic bisimulation argument for embedded/daemon/remote engine equivalence — an informal, reviewed proof, not machine-checked, so verification: design: review, not model-check. Both implementation: none — the honest default for a freshly relocated constraint nothing yet enforces mechanically. ADR-0003 keeps the decision (independently-wireable component boundaries) and cites the spec for the two rules that decision depends on. The third bracketed paragraph ([deployment-composable-monolith]) carried no BCP-14 keyword and was folded into that decision prose rather than given its own claim — it describes what was built, not a rule to check. No cross-file because:/depends: on the two new claims: every existing cross-file citation in this corpus already trips docket's C5 check (a known, pre-existing corpus-wide gap, 28 baseline instances untouched by this pass), and prose citation to the model says what's needed without adding a new instance of it. normative-prose in this file: 2 -> 0.
An ADR records a decision and why it was taken. A spec carries the rules, each naming something that could falsify it. Several ADRs were written with rules inside them because at the time there was nowhere else to put the detail, and a rule written there is unreachable by the register: ADR paths permit no claims, so a MUST in one reads as binding while nothing can ever check it. Twelve such statements, and most were not gaps at all. Five belonged to an ADR whose subject a later decision removed outright, leaving its tiers without a referent; two restated rules the trust model already carried, in different notation; two were conversational uses of MAY and one was already struck through and withdrawn. Three were real. A verifier's obligation to exclude retracted vouches was stated nowhere else -- the acceptance procedure never checked retraction at all -- and two rules about deployment modes had no spec home, which is why a design document had independently restated them in prose. All three now sit in specs with an implementation target of none: the rule exists, nothing checks it yet, and the register can say so. Findings fall from 86 to 71 and no new one appears.
The audit that dropped 14 model-check grades never reached this claim, and it looked like the cheapest one to re-earn: the model it needs already exists and its CI gate is green. Checking that gate's non-vacuity before trusting it found the opposite: OID and Czd are separate top-level Alloy sigs with no extends/in relation, so their disjointness holds by declaration before any fact in the file is consulted (confirmed by probing the negation directly: no instance exists regardless of which facts are in force). oid_disjoint_from_ protocol_sorts and carrier_czd_seam therefore restate Alloy's own sig-partition typing, not a property of this model's domain — no mutation to the model's facts can ever make them fail. Grading backend-seam-typed model-check on that basis would have repeated exactly the defect the audit found. Left honestly ungraded (verification.design: none, stated explicitly rather than left absent) with the reason recorded at the claim block, in the two assertions' own comments, and in the stale Verification/Appendix A prose that still described the model as unbuilt after it had landed. The model's real, non-vacuous coverage is the ancestry-soundness obligation via ancestry_soundness, which this pass leaves untouched.
The 2026-08-23 audit dropped 14 unearned model-check grades to verification.implementation: none, but left the design axis absent rather than stating design: none — which reads as "this claim has no design target" when every one of these plainly does (all were model-check before the audit). Added design: none explicitly to all 13 atom-transactions.md and atom-model.md claims, and recorded why each stays there rather than getting re-earned. None was restored. Two genuinely new formal-model constructs (the owner-fact/fold mechanism ADR-0007 requires, and the ADR-0009 spine) have no model anywhere in this repository, and building either is new modeling scope the corpus's own comments already name as an architect's decision, not something to improvise here. The cheapest- looking fix for chain-monotonicity/anchor-immutable — restricting AtomCharter.tla's Next relation to its three genesis-only actions — was tried on paper and found to make both checks vacuous (no reachable state exercises the rollback/fork content either invariant is actually about, and anchor-immutable's guard was already vacuous by construction independent of that restriction). charter-ancestry's full temporal floor spans two models, neither of which carries the src field it would need. Each of these is recorded at its own claim and summarized once in a dated Verification note so a future reader does not have to re-derive it.
An audit found half the model-check grades unearned and dropped them rather than raising the models. This node asked whether the models could be raised. For all fourteen the answer is no, and each now carries the reason it stays down. Thirteen need constructs the corpus itself flags as unscheduled work: the owner-fact fold and genesis-once rejection have no model anywhere here, and both transaction models say so in their own comments. The cheapest-looking fix was attempted and rejected on evidence -- limiting the charter model to its genesis actions makes the rollback and fork invariants vacuous rather than checked, since no succession action remains to exercise them. The fourteenth looked free: an Alloy model exists and runs green. Its assertions cannot fail. The two sorts they separate are declared as distinct top-level sigs, so disjointness holds by Alloy's own typing before any fact is consulted, and no mutation to any fact can redden them. Restoring a grade on that would have reproduced the defect the audit was opened to remove. Separately, all fourteen had lost their design key entirely in the migration to two axes -- read as having no design target at all, when every one of them had been model-check before the audit. They now say design: none, which is the true statement: the target exists and nothing checks it.
The register knew which claims had something backing them and which only declared it, but nothing outside a one-claim-at-a-time run could see it. `docket report` emits that survey as markdown; wiring it ahead of the site build puts it on the published docs and keeps it from drifting from what the register measures. The page joins the other generated reference content rather than being committed, following what content/.gitignore already establishes. DOCKET overrides the binary for anyone whose PATH docket is not the register.
docket now emits dk-prefixed class names and data-* state on the claim verification page (a separate change on the docket side) but the page still rendered as a wall of headings — nothing selected the new structure. This adds the presentation half: a bordered card per claim, verification-axis pills coloured by state (backed/gap/ misleading), a numbered weakest-first section marker, and a summary figures grid, reusing the site's existing --bg/--fg/--border tokens and its three-mechanism theme wiring (OS preference, pinned data-theme, light-dark()) rather than inventing a parallel one. Three new tokens (pine/amber/alarm) are added through all three mechanisms for the verification-state colours the existing palette had no concept of.
The generated survey now emits structure -- a wrapper per claim, per section and for the summary, each carrying which backing tier it fell into and what its two verification axes declare. This is the site's half: what that structure looks like. A claim reads as a bordered card with a tier-coloured edge, its axes as pills whose colour says whether the axis is backed, an honest gap, or a grade with nothing behind it. Sections carry a numbered marker, which is information rather than ornament: the order is by weakness of evidence, and the number is the only thing that says so. The palette threads through the three theme mechanisms already here rather than adding a fourth, and reuses the existing tokens for everything except the three states the report needs to distinguish. The tier numeral is drawn from a data attribute rather than written into the heading text, because inline markup inside a section heading is currently dropped by the compiler. That is a defect elsewhere, and this avoids depending on its fix either way.
supply-chain-security.md still taught ownership transfer and key rotation as a "successor charter", a shape atom-transactions.md retired on 2026-08-05: genesis records are written once and never reissued, and every later change lands as a signed fact folded onto the charter's chain. The glossary fences the old phrasing and FAQ entry 5 already states the current model; this page was the last reader-facing surface teaching the retired mechanism.
Nix identified the right jobs -- version integrity, hermetic builds, distribution, storage -- but serves them all through one primitive: recompute it yourself. Recomputation is the most expensive possible verification, so its cost is the trust model itself, paid in compute, and cannot be optimized away from inside. Name that reading in the public prose: a compact statement in the README after the fixed-point argument, and a new Part 0 FAQ entry mapping each tool buried in Nix onto the layer that does its one job with the canonical primitive (signatures, content digests, corroborating builds), with the binary cache's hardcoded key as the tell. Entry 9 gains a tie-back so its two blockers read as instances of the same pattern.
atom-transactions.md retired charter succession outright on 2026-08-05 (genesis-once: facts are the only mutation channel, and a new charter is by definition a fork with its own identity), but two documents still taught succession in current voice. atom-sad.md glossed the anchor's immutability as "successor charters chain without changing it" and resolved git hash agility through an explicit successor charter; lock-file-schema.md's anchor field assigned hash-rewrite continuity to "a successor charter's explicit concern". Both now state the ruled model: the charter is written once, later change folds on as signed facts, a re-hash severs the in-protocol path to the anchor, and chartering the re-hashed history is a genuine fork — continuity between the two anchors is at most an out-of-band trust decision. The remaining successor-charter mentions in both files are deliberate: retired-constraint blocks, supersession markers, and the SAD's verification row recording the abolition itself.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Successor to #71 (MVP-M1: atom stabilization campaign), closed early per the comment on that PR. A from-scratch rework of the atom version-integrity model landed as ADR-0007 plus a companion explainer: charter, claim, and publish become permanent, genesis-once records per scope, with everything after genesis — ownership rotation, label transfer, yank/deprecation, multisig thresholds — expressed as
facts layered on top, never a mutation of the founding record. This replaces the charter/claim mutation-via-succession model #71's remaining layer-3/4 work was built against.Tracking issue: #68 (continuing, not split — this is a rare mid-campaign deviation, not a new initiative).
Status
Landed so far:
eml-backed, single-root canonicalized, MMR-derived — RFC 6962 was the starting point, since diverged)www/content/explanation/atom-version-integrity.md)site.tomlhost fixStill open, not yet scoped into a node DAG:
docs/models/atom-model.md/docs/architecture/atom-sad.md/ atom specsn2-charter-impl,n3-atom-charter-tla-rework,n3-owner-verification-impl,n3-store-charter-ingest,n3-registry-anchor-fix) against the new genesis-once model — this is what's expected to also resolve the CI failures noted when MVP-M1: atom stabilization campaign #71 closedeml::Storagetrait implementationThis PR stays a draft while the above gets scoped into an actual node DAG.