Repository navigation
Make the v2 frontend census typed and exactly reconciled - #8179
Merged
Merged
Conversation
…elabelling genuine body-lowering rejections as retention
…LexArtifact-grain controls
… and comment newline termination
… partial receipt, one consistent roadmap sequence, scratch residue deleted
…r, and render the rejection arm
…sion/crisp-lynx-832
…rtion, read contract recorded not fabricated, roadmap by time grain, resolve-ready naming
…link, and over-budget stage claims deleted with the gap recorded
…e two walls by minimal pair
…ere they were measured
…sion/crisp-lynx-832
…d by this diff's compile-clean closure)
…e semantic population
…d left half-bound The 13 witness failures at eff3eaa are caused by the repair, not exposed by it. All three modules were fully bare — every name resolved by pool-membership coincidence (DESIGN Class B). Naming ONE dependency changed the closure that gets assembled, and the extdeps catalog rows two of the witnesses read stopped resolving: `no such function: hermetic_fixture_file_facts`, etc. A partial import list is the worst of the two states: it neither binds the module's dependencies nor leaves the coincidence intact. So the repair is the whole list, and every symbol home below was verified at its declaration rather than by name search — std.cache_identity for the artifact kind ids and the receipt digest, std.cache_interface for the kernel types and route/write folds, extdeps.cache + extdeps.cache.types for the catalog projections, and the per-family extdeps realization modules for the rows themselves. realize_kernel_test stayed GREEN under the partial list its two siblings went red under, and is completed here anyway. Green under a bare reference is not evidence the reference is bound; it is evidence that this run's closure happened to contain it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DBBegUkJygQyr1zMHiv2eK
…at only re-imports them ContentAddressedByValue, HandAuthoredString and NativeInternalHash are declared on std.cache_interface KeyDerivationClass; extdeps.cache.types merely imports them at the top of its own file. I read those lines as declarations because a name-ranked search returned them, which is the third instance in this PR of the same failure — a name-level observation standing where a bound declaration was required, the exact class the PR's subject is about. Every one of the 54 imported names across the three files is now checked against a declaration form (col-0 type/fn/data, or a variant on its coproduct) rather than against an occurrence. StructuredArtifact is declared inline on `type ValueShape` and is correct as imported. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DBBegUkJygQyr1zMHiv2eK
…check the written file ExecutionReceiptDigest and execution_receipt_digest_of_value are declared on std.cache_identity; I wrote them into the std.cache_interface block. The previous commit's verification did not catch it because it checked a list of (name, intended module) pairs I held in mind, not the pairs the file actually contains — so it confirmed the homes I had already re-derived and said nothing about where the import statement put them. The check now parses the three files' import blocks and tests each (module, name) pair as written against a declaration in that module's source. 71 pairs, no remaining mismatch; the two StructuredArtifact flags are the checker's own blind spot for inline variant lists (`type ValueShape = RawBytes | StructuredArtifact | ...`), confirmed correct by direct read. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DBBegUkJygQyr1zMHiv2eK
…an identity join Increment 2 of the frontier lane, delivering the two structural halves and NOT the third. CLOSED RESULT SPACE. classify_source answered in String, so every consumer compared against a literal and a typo produced a verdict rather than a refusal. It now returns FrontendStage = LexRefused | ParseRefused | NormalizeGraftRefused | NormalizeRetained | NormalizeOther | NormalizeAccepted, with frontend_stage_label the single rendering authority. THE EMPTY-REASON-SET ARM IS GONE BECAUSE ITS INPUT IS. The classifier took List<Symbol> and had to answer NORM_REASON_SET_INVALID_EMPTY for the empty list. It now takes NonEmptyDiagnostics, whose head is not optional, so that input has no representation. The RED that fed it an empty list retires with the state rather than with the wall — the dissolution rule preserves a control when the invalid state stays writable, and this one cannot be authored at all without re-widening the parameter to admit the value it tests. Recorded in the file rather than left to be inferred from a deleted test. COMPLETENESS IS A JOIN. Fifteen hand-written m_* fns had no denominator: drop one and the remaining fourteen still answer, so 'all fifteen observed' only ever meant 'fifteen fns were present'. They are now rows on frontier_roster, and census_is_complete asks per roster label whether a matching observation exists. Three controls, including one that a count equality would pass — fifteen observations, none of them a roster member. NOT DELIVERED, and it is the increment's headline item: the live fifteen still cannot gate a PR. dag_grammar() construction alone exceeds the fast-lane budget before any member is read, so observe_roster stays a reproduction instrument in a non-test module and the durable claims run on synthetic specimens. The two stage-separation claims deleted last increment are still owed to the batched or realized instrument; what changed is that it now has a total verdict type and a denominator to join against. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DBBegUkJygQyr1zMHiv2eK
…r cannot infer compile-clean refused all five `empty: []` arguments: fold_list's empty parameter is the generic accumulator A, so a bare literal has no expected type to be a collection of. The corpus idiom is an explicit cast, used the same way in gunbc.package_delivery. Diagnostic returns to the witness import list — it was dropped as unused when the specimen helper stopped naming it, and the cast names it again. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DBBegUkJygQyr1zMHiv2eK
Contributor
Author
|
Flagging a coverage gap in this PR's approvals, against my own interest. Three reviews have now approved this PR, and all three describe The census increment itself — the This self-corrects when #8149 merges: this PR's diff then shrinks to the census work alone and a subsequent review would have to look at it. I am not restructuring the branches to force that sooner, but I would not treat the current 3 approvals as satisfying the two-approval bar for the new code. — sent from crisp-lynx-832 |
Contributor
Author
|
Correcting my comment above. A fourth review (cursor/composer-2.5) explicitly names the census work — "separates revision-scoped frontier observation from durable classifier/roster laws" — so it engaged with this PR's own increment rather than only the stacked #8149 half. My claim that the approvals covered none of the new code was wrong for that review. What still stands: the three earlier approvals do describe only #8149's changes, so the tally overstates coverage of the census work. What does not stand: the flat "has drawn no review". One review has looked at it. — sent from crisp-lynx-832 |
…et half census_is_complete asked, per roster label, whether SOME observation carried it. That is the covering direction alone, and I described it as an identity join, which it was not. A census of all fifteen members PLUS a stray sixteenth passed it, and so did one carrying a member twice — neither condition can make a per-label existence check fail. reconcile_census now joins both directions and at multiplicity, returning CensusReconciliation = CensusExact | CensusMissingMember | CensusDuplicateMember | CensusUnrosteredObservation with the offending label. The three failures are not one state: a missing member means coverage is short, an unrostered observation means the roster and instrument have drifted apart, and a duplicate silently doubles that member's contribution to every count_stage figure derived from the census. Collapsing them into one Bool is what would have made those figures unfalsifiable. census_is_complete is now DERIVED from the verdict rather than computed beside it, so there is no second Bool fold that could disagree with the coproduct. Four controls, two of which the previous version passed: the stray and the doubled census each contain every roster member. The notes claiming an identity join are corrected at the point of assertion rather than left for the next reader to discover. Found by a question from the planning side asking whether the census proved exact reconciliation or mere coverage. It proved coverage. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DBBegUkJygQyr1zMHiv2eK
classify_source returns FrontendStage; p_hex_escape and its five siblings still declared -> String, so every one of them was a type error waiting for the next compile-clean run. I changed the classifier's result type and updated its structured consumers without checking the six one-line probes at the bottom of the same file. Found by the planning side reading the file, not by me re-reading what I had edited. Also merges origin/main, which now carries #8177 — the rename of the OTHER ArtifactIdentity. That PR touches self_host_generation_identity_witness_test, self_host_promotion_admission_ witness_test and self_host/generation.dag: exactly the files I retracted imports from on #8149, and none of the three I kept. It confirms the homonym split rather than superseding those edits. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DBBegUkJygQyr1zMHiv2eK
…the unadmitted stage count Four repairs from an external review of the census increment. Three are defects I introduced. THE ROSTER WAS NEVER VALIDATED. reconcile_census checked observations against the roster and assumed the roster itself was sound. Two malformed rosters defeat that with CensusExact still reachable: a duplicated LABEL is satisfied by one observation counted once for BOTH rows, so fifteen rows with fourteen labels reconcile exactly against fourteen observations; a duplicated PATH under two labels is invisible at label grain entirely, and the live census would read one file twice and report it as two members. verify_roster now runs first and CensusExact is unreachable without FrontierRosterValid. It takes the rows rather than reading frontier_roster, because a validator that can only see the one live roster is unfalsifiable — it would report valid and nothing could establish it reports anything else. STAGE EQUALITY WAS THE RENDERER. frontend_stage_eq compared frontend_stage_label results, making presentation the semantic authority: a label rename would change which stages compare equal. Now structural; the pairwise-distinctness claim is about rendering only, which is what it should always have been. count_stage IS DELETED. It took the unreconciled population, so it would total a census missing a member, carrying a duplicate, or built on an invalid roster — the exact corruption the note beside it describes. It also had no consumer. Counting returns on a carrier only a reconciled census can construct, with the executing census that gives it a producer. The six manual probes now render through frontend_stage_label rather than returning FrontendStage. Their only consumer is a person invoking one by hand, so label text is the right interface; the typed vocabulary is for structured consumers. Four roster controls, including reordering, since row order is not a fact about the roster and must not become one about the verdict. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DBBegUkJygQyr1zMHiv2eK
gunbai-bot
Bot
changed the title
Contributor
Author
|
The
Merged — sent from crisp-lynx-832 |
…non-fold residue
The floor refused non_fold_residue_no_unrostered_or_stale. v2.lens.non_fold_residue counts a
match on a FUNCTION PARAMETER whose type is a closed coproduct and whose body carries a top-level
wildcard arm, in a non-test .dag. The structural equality I landed last push is exactly that
shape — `match b { LexRefused => true _ => false }`, six times — so making equality structural
introduced the residue in the same motion that removed the renderer from the equality path.
Both facts are real and the resolution is neither a roster row nor a revert: enumerate the arms.
All thirty-six positions are written out.
The verbosity is the point rather than a cost being tolerated. Under wildcards, adding a seventh
stage leaves this function compiling and quietly answering false for every comparison involving
it — the same silent-widening the lens exists to catch. Enumerated, the addition fails to
typecheck at all thirty-six positions, so a new stage cannot be introduced without deciding its
equality against every existing one.
Verified no match-on-parameter in the file carries a wildcard: the remaining ones scrutinise
let-bound values or closure parameters, which the census does not count and which cannot hide a
missing coproduct case.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DBBegUkJygQyr1zMHiv2eK
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.
Increment 2 of the v2 self-host frontier lane. Three delivered facts, one explicit non-delivery.
What lands
FrontendStagereplaces string verdicts.classify_sourceanswered inString, so everyconsumer compared against a literal and a typo produced a verdict rather than a refusal. The
result space is now closed:
LexRefused | ParseRefused | NormalizeGraftRefused | NormalizeRetained | NormalizeOther | NormalizeAccepted. Equality is structural;frontend_stage_labelis the sole renderer and deliberately not the comparison mechanism.Normalize refusal classification consumes
NonEmptyDiagnostics. The classifier tookList<Symbol>and had to answerNORM_REASON_SET_INVALID_EMPTYfor the empty list, because thatinput was constructible and mapping it to a real stage would render a missing observation as an
observed one.
NonEmptyDiagnostics.headis not optional, so that input has no representation andthe defending arm has no subject — a climb to structurally-impossible for that one class. The RED
that fed it an empty list retires with the state, not with the wall; it cannot be authored without
re-widening the parameter to admit the value it tests.
Census reconciliation checks roster and observations in both directions and at multiplicity.
The first version established coverage only — per roster label, does some observation exist — and
I wrongly called that an identity join. It accepted a stray sixteenth observation and a duplicated
member.
reconcile_censusnow returnsCensusExact | CensusRosterInvalid | CensusMissingMember | CensusDuplicateMember | CensusUnrosteredObservationcarrying the offending label, and the rosteris validated before the join: a duplicated label is satisfied by one observation counted once for
both rows, and a duplicated path under two labels would have the census read one file twice and
report it as two members.
census_is_completeis derived from the verdict rather than computedbeside it.
What does NOT land
The live 15-member census still does not execute as a required PR gate.
dag_grammar()construction alone measured over the five-second fast-lane budget before any member is read, so
observe_rosterremains a reproduction instrument in a non-test module and the durable claims runon synthetic specimens. Nothing here claims otherwise. The two stage-separation claims deleted in
the previous increment are still owed to that executing instrument; what changed is that it now
has a total verdict type and a validated denominator to join against.
There is no per-stage count:
count_stagetook the unreconciled population and had no consumer,so it was deleted rather than kept beside a note explaining how a duplicate corrupts exactly the
figures it produced.
Review note
This branch is stacked on #8149, so its diff against
maincurrently presents both increments.Several approvals here describe #8149's half rather than the census work — see the comments
below. Merge #8149 first; this PR's diff then reduces to the census files.