Repository navigation
A matched format tag means "I understand this exact schema" - #8840
Merged
Merged
Conversation
added 3 commits
August 22, 2026 00:54
…ically A decoded SCM image supplies child order from a document nobody in this process authored, and insert_from_structure handed that order straight to content_hash_of_children, whose contract placed the canonical-order obligation on the caller. That obligation is undischargeable by a decoder: a hand-edited image listing `beta` before `alpha` minted an ObjectId under the fold of `beta, alpha` while the reconstructed node's own content_hash folds `alpha, beta`, so find_object(H1) could answer a node whose content_hash is H2. That is not a lossy round trip; it breaks the meaning of ObjectId = v2.std.node.Hash. content_hash_of_children now canonicalizes its own input, which makes the state unwritable rather than detectable (DESIGN section 5) and costs canonical callers nothing, since canonicalizing a canonical list is identity. The remaining caller obligation is the one that genuinely cannot be discharged here -- each hash must be that child's own content_hash -- and the comment now says only that. THE ORDERING RULE IS STATED ONCE. Every rule reads a label and the child count and never a child's target, so it generalizes over the carrier: one canonicalize_labeled_for_content_hash<T>, instantiated at Edge for canonicalize_node_for_content_hash and at LabeledChildHash here. An Edge-shaped copy with a hash-shaped copy beside it would be two authorities for one identity rule (section 3), agreeing exactly until one is edited and disagreeing as objects unreachable by the identity they were stored under. Six Edge-specific partition helpers collapse into the generic ones; connective_edge_discipline_for_children projects onto a count-taking form rather than duplicating the Atom rule. EVIDENCE. node_hash_protocol's 19 frozen-vector claims stay green, which is what establishes no identity changed for any existing caller. The new pair is a pair on purpose: canonicalizing everything would satisfy the named claim while destroying positional structure, where order IS the meaning. Mutation credential, executed -- remove only the canonicalize call inside content_hash_of_children: scm_image_permuted_named_children_reconstruct_the_canonical_identity FAIL scm_image_permuted_positional_children_are_a_different_identity PASS The named claim asserts the permuted insert derives the identity that content_hash derives for the assembled node, not merely that the two inserts agree with each other -- which any consistent wrong rule would satisfy. The projections are named top-level functions because an inline lambda in that argument position refuses with `no field 'label' on type 'T'`; the corpus already passes named functions this way (eq: string_eq), so this follows the existing route rather than respelling around the inference gap.
An unknown JSON member was silently ignored. That is not forward compatibility:
a writer states a fact, the reader discards it, the next re-encode deletes it,
and every operation in that sequence reports success. It is the
fabricated-plausible-output failure DESIGN section 5 forbids, arrived at by
omission -- nothing anywhere reports that a claim in the document was thrown
away.
So once the format tag matches, every JSON object in the document has a closed,
variant-specific member set, and anything else is a typed refusal. It does
foreclose additive evolution WITHIN a version, and that is the intended cost: a
schema that grows a member grows a new format tag, and a decoder that supports
both says so by admitting both tags. An open extension point, if one is ever
genuinely needed, is a declared member with declared namespacing and retention
rules -- never every unrecognized key promoted to one by default.
THE MEMBER SET IS CLOSED PER VARIANT, NOT OVER THE UNION. `identity` is required
on an atom and forbidden on every other connective, so "unexpected" has no
meaning until the variant is known -- the check runs after the tag is read and
before the variant is built, so a Conj carrying an identity refuses rather than
decoding into a node whose stated identity silently played no part in the node
that resulted. scm_image_identity_on_a_non_atom_kind_refuses is the claim a
union-shaped check would fail.
THE VOCABULARY IS PER LAYER, THE MECHANISM IS SHARED. image.dag owns
`unexpected_member_key`, which answers a context-free question -- which key is
not in this set -- and each layer names its own shapes
(ImageMemberContext / RepositoryMemberContext). Adding the repository's shapes to
image.dag's coproduct would have made the lower carrier enumerate a layer above
it; duplicating the fold in the envelope would have been a second authority for
one rule. Neither is necessary.
EVIDENCE, all executed. Six new image claims and three envelope claims, and the
controls are the load-bearing half:
same members in a different order -> loads (closed population is
not positional parsing)
an atom carrying its identity -> loads (so the refusals are not
"reject identity everywhere")
the encoder's own unmodified wire -> loads (so the decoder does not
refuse its own output)
The envelope claims add the extra member to the ENCODER'S OWN OUTPUT, so the
document is otherwise exactly what this decoder emits and the refusal can only be
the extra member. All three assert the CAUSE rather than the arm: a document
refusing for an unrelated reason would satisfy a bare refusal claim and prove
nothing about the member set.
The new RepositoryRefusal variant was caught by the compiler as a non-exhaustive
match in the witness rather than by review -- the closed coproduct doing its job.
Two structural corrections from review, both before the envelope format becomes durable. ENCODE AND DECODE HAVE DIFFERENT FAILURE POPULATIONS, SO THEY ARE DIFFERENT TYPES. One shared RepositoryRefusal made every total consumer of an ENCODE result state how it classifies RepositoryUnexpectedMember -- a decode-only fact an encoder cannot produce, since it receives a RepositoryEnvelope and never an input JSON object. The closed coproduct was doing its job and the carrier was lying to it: an exhaustiveness obligation is only as honest as the type it ranges over, and a union of two operations' failures forces each to handle the other's impossible states. The previous commit's witness had to add exactly that impossible arm, which is how it surfaced. The split also dissolves a conflation that predates the member sets. Both paths spelled their unresolved reference as String, and the two strings are different things: on encode the caller handed us an ObjectId the store or the commit list does not contain; on decode the DOCUMENT named an image-local position at which no object decoded. The encode side now carries the ObjectId directly, so the identity no longer round-trips through a hex key the caller would have to parse back. The decode side still spells its references as String, and that is declared in the carrier as a REMAINING conflation rather than quietly fixed halfway -- typing it properly means typing image.dag's whole reference vocabulary. THE CODEC IS NAMED FOR THE EXACT WIRE VERSION IT UNDERSTANDS. decode_repository now performs format dispatch and nothing else; decode_repository_v1 understands exactly v1 and is frozen once a v1 document exists anywhere. encode_repository is the separate question of which version we EMIT, delegating to encode_repository_v1. They are one implementation today, which is exactly why the names must differ now: the seam a v2 arrives through has to exist somewhere no author is tempted to just add the field to v1. THIS FABRICATES NO v2. No second arm, no enum member for a format that does not exist, no migration claim -- a synthetic second version would test an invented migration rather than the one the product eventually needs. What IS claimed stays exactly what the executed claims cover: v1's member populations are closed, an unknown format tag refuses, and valid v1 loads. The two-tag migration is a declared future obligation, not verified compatibility. All image, envelope and node-hash-protocol claims green.
Contributor
Author
|
Merge-order note: #8853 first. This branch is off a main whose witness floor is red — 16 failures, all I established the inheritance by execution: restoring main's version of the file this stack touches reproduced byte-identical failures. #8853 fixes the root (an occurrence payload declared where the carrier was required) and takes all 16 back to green. So a floor red here before #8853 lands is expected and is not this diff. Once #8853 is in, I'll merge main into this branch and confirm green rather than assume it. — sent from gentle-eagle-360 |
Contributor
Author
|
Same inherited root, and measured rather than inferred. Run #8853 (now 86/86. The 19 frozen node-hash vectors are in there deliberately — they are what establishes the canonicalization change carries no identity drift. The probe was applied to the working tree and reverted, so nothing is pushed here and this branch is still exactly what was reviewed. No fix is owed on this PR; the unblock is merging #8853. — sent from gentle-eagle-360 |
One conflict, in scm_image_witness_test.dag, and it was positional rather than substantive. Both #8838 (now on main) and this branch append a block to the end of the same file, so git conflicted on the append point. Main's side of the conflict region was EMPTY: this branch already carries main's node-identity-protocol block, picked up by the earlier merge at 058a2f7. Verified rather than assumed -- no test fn present on main is absent from this branch, checked by name at both HEAD and the resolved file, and the resolved file is byte-identical to this branch's version. 24 test fns, all of main's 18 among them. Merged rather than rebased, per the repo's merge policy. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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.
An unknown JSON member was silently ignored. That is not forward compatibility: a writer states a fact, the reader discards it, the next re-encode deletes it, and every operation in that sequence reports success. It is the fabricated-plausible-output failure §5 forbids, arrived at by omission — nothing anywhere reports that a claim in the document was thrown away.
Once the format tag matches, every JSON object now has a closed, variant-specific member set, and anything else is a typed refusal.
Stacked on #8838 (needs its
scm_image_witness_test.dagadditions); merge that first.Closed per variant, not over the union
identityis required on an atom and forbidden on every other connective, so "unexpected" has no meaning until the variant is known. The check runs after the tag is read and before the variant is built, so aConjcarrying anidentityrefuses rather than decoding into a node whose stated identity silently played no part in the node that resulted.scm_image_identity_on_a_non_atom_kind_refusesis the claim a union-shaped check would fail.Vocabulary per layer, mechanism shared
image.dagownsunexpected_member_key, which answers a context-free question — which key is not in this set — and each layer names its own shapes (ImageMemberContext/RepositoryMemberContext). Adding the repository's shapes toimage.dag's coproduct would have made the lower carrier enumerate a layer above it; duplicating the fold in the envelope would have been a second authority for one rule.The cost, stated
This forecloses additive evolution within a version, deliberately. A schema that grows a member grows a new format tag; a decoder supporting both says so by admitting both tags. An open extension point, if ever genuinely needed, is a declared member with declared namespacing and retention rules — never every unrecognized key promoted to one by default.
Evidence
Six new image claims, three envelope claims, all executed green alongside the existing 18 + 20. The controls are the load-bearing half:
identityidentityeverywhere"The envelope claims add the extra member to the encoder's own output, so the document is otherwise exactly what this decoder emits and the refusal can only be the extra member. All three assert the cause, not the arm — a document refusing for an unrelated reason would satisfy a bare refusal claim and prove nothing about the member set.
The new
RepositoryRefusalvariant was caught as a non-exhaustive match in the witness by the compiler rather than by review — the closed coproduct doing its job.— sent from gentle-eagle-360