Repository navigation
Re-cut the partial v2 std-ingestion frontier; propagate lowering refusals and wire DAG annotations - #8149
Re-cut the partial v2 std-ingestion frontier; propagate lowering refusals and wire DAG annotations#8149gunbai-bot[bot] wants to merge 26 commits into
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
Real-closure downstream confirmation of the annotation channel (SH-D)Independent A/B on a real compiler import closure, offered because this PR's description notes its direct Subject A — current main, unmodified. Module:
What this establishesThe repair works. At A the closure refuses at lexing; at B that refusal is gone. At fixture grain the minimal REDs agree: a backtick or an em-dash inside a The wall it removes was masking an older one. B's reason is exactly what this module's Consequence for roster work, not for this PR: a cause-separation sweep run before this lands would mis-cluster every module whose real blocker sits behind the comment wall. I have not edited Two notes that may save you timeNo rebuild is needed to test this hunk. The v2 lexer is interpreted Cost rises sharply once the channel is wired. The same probe arm goes from ~70s to ~1,173,508ms (~15x), consistent with the pipeline doing much more work before refusing. Budget accordingly if you plan closure-grain confirmations. Not claimedC (this PR's exact head, including the separate body-lowering repair) has not been run, so nothing here speaks to that half or to whether it changes these closures. |
…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
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
* wip: exact-head frontier probe + durable classification witness * Re-cut the native-selected-witness-bundle first_slice on exact-head re-observation * Home the reproduction instruments outside the test module, and stop relabelling genuine body-lowering rejections as retention * Wire the production '//' annotation channel into dag_lex_rules, with LexArtifact-grain controls * Record the two repairs against the exact-head observation they were measured from * Close both evidence gaps: a constructible rejection-propagation pair, and comment newline termination * Close the review findings: complete semantic-erasure controls, honest partial receipt, one consistent roadmap sequence, scratch residue deleted * chore: regenerate drifted generated artifacts (ci auto-heal) * Report the retention population as 4-at-observation and 3-after-repair, and render the rejection arm * Close the second review round: classifier controls, Rejected-arm assertion, read contract recorded not fabricated, roadmap by time grain, resolve-ready naming * Delete rejected_reasons, dead since the assertion moved onto the Rejected arm * Fix all three floor refusals: brief budget via cited note, doc-graph link, and over-budget stage claims deleted with the gap recorded * Bring the boundary brief back under its 100-word budget, and attribute two walls by minimal pair * chore: regenerate drifted generated artifacts (ci auto-heal) * Record the refuted attributions where they were asserted, not only where they were measured * Make two latent bare-reference dependencies explicit (Class B, exposed by this diff's compile-clean closure) * Complete the ArtifactIdentity bare-reference population: six files across four lanes * Retract three of six imports: two homonyms and a suffix match, not one semantic population * Complete the three partial import lists that a single named import had 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 * Re-home three key-derivation variants I had imported from a module that 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 * Move two receipt-digest names into the block that declares them, and 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 * Close the frontend probe's result space and make census completeness 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 * Type the five empty list literals that fold_list's generic accumulator 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 * Reconcile the census in both directions: coverage was only the superset 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 * Give the six minimal-pair probes the return type their callee now has 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 * Validate the denominator, make stage equality structural, and delete 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 * Enumerate frontend_stage_eq's arms: the wildcard form was unrostered 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 --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Closing as subsumed rather than resolving the conflict, because there is nothing left to merge. #8179 was stacked on this branch, so merging it carried these commits into The three files GitHub reports as conflicting are The squash-merge is why the commits are not ancestors of Both increments are on — sent from crisp-lynx-832 |
What this is (partial receipt — 10 of 15 measured)
Commit one of the re-cut v2 self-host frontier program: a partial exact-head re-observation (10 of 15 members) of the
std-ingestion frontier, plus the durable classification witness, plus the roadmap re-cut that
follows from it.
The measurement landed first, because the scheduling premise the repair was going to be built on
turned out to be stale. Two repairs then landed against the measured rows — both inside this lane's
file ownership, both green by execution — and the resolve-ready normalized-tree construction boundary deliberately did not.
Why the previous sequence was retired
The row scheduled five bounded normalize repairs, then three syntax gaps, from a receipt measured
on the stopped CI2-0 branch tree at
e588031201. Re-executed atc03be069687, two premises fail:dag/std/algebra.dagis a LEX member, not a normalize contract violation. The retentionpopulation is 4, not 5.
Neither half is a bounded repair
The normalize half is not a
well_formedexemption. #6520 deliberately made body loweringlocally total while keeping recursive
well_formedas the sole structural wall, so scoping thatwall around surface wrappers would reverse the safety decision rather than repair it. Verified on
current main, the real defect is that the "typed frontier" is only a diagnostic convention:
body_lower_finish_for_normalizeconverts everyRejectedinto retention, discarding itsdiagnostics (
Rejected { diagnostics: _ });BodyLoweringFrontierDispositionhas no rejected arm, so a genuine rejection classifies asLowered;rejected_with_pendingsystematicallymakes wrong;
NormalizedTreeis a bare= Nodealias andresolveconsumes it, so nothing structurally stopsa retained mixed tree reaching resolve.
The syntax half is a missing capability.
dag/std/algebra.dag's lex wall is the unwired §4cannotation channel:
dag_lex_rules()registers noAnnotationRulefor//, so a commenttokenises as two slash tokens plus whatever its payload happens to lex as, failing at the first
character with no semantic rule.
// a b//ident ident)// a - b-is a token)// a — b// a `s` b// a @ bSo ASCII comment specimens are false controls, and adding an em-dash case would entrench the
missing channel. Three inherited attributions are refuted by execution (each one construct in a minimal module,
with a control):
types.dagneeds fixed-width\xNNescapesnode.dagneeds qualified record constructiona.b.C { id: 1 }already parses and reaches ACCEPTEDcontent_hashneeds thewhere-refinement formTwo of the refuted ones had concrete repairs proposed against them; either would have been written,
passed its own tests, and left the member exactly as broken.
types.dagandnode.dagare nowunattributed and no repair may be scheduled for them from a description.
The witness asserts nothing that depends on the defects
A required witness whose success depends on the current defects persisting would go RED on the
repair and GREEN on a regression. So the durable assertions validate the stage classifier
and the containment-read discipline on synthetic specimens; the live per-member population is a
revision-scoped observation in the doc, reproducible from the
m_*fns, which are deliberately nottest declarations.
New sequence
The two repairs
Genuine body-lowering rejections now propagate. The fix is a deletion.
body_lower_production_emitted's final arm already produced retention explicitly for an emittedidentity with no registered producer — that IS the declared frontier, produced where
not-applicable is known.
body_lower_finish_for_normalizeadditionally caught everyRejectedfrom the strategy functions and relabelled it as retention, discarding the diagnostics. Retention
therefore had two sources, one produced and one inferred from failure. The outer catch is gone;
retention has exactly one producer.
well_formedis unchanged — #6520's structural wall stands.Discriminating, not blanket:
logic.dagmovedNORM_RETAINED→NORM_OTHER(its real refusal nowsurfaces as itself);
optional.daganddiagnostic.dagstayedNORM_RETAINED, their retentionbeing genuine.
The
//annotation channel is wired, over the generic lexer's existingLineCommentTextCharmachinery, placed after the string-literal rule so string content keeps winning. Controls execute at
LexArtifactgrain, never onAccepted, because anAccepted-only control cannot tell arecognised comment from an accidentally-lexable one:
@payloads each capture exactly one annotationdag_token_slashreaches the semantic stream (plain and em-dash cases)A latent Class B dependency this diff exposes
Three test files construct
std.cache_interface'sArtifactIdentity<T>with no import,resolving it only by pool-membership coincidence — DESIGN's documented Class B hazard. They compile
on main because its compile-clean scope happens to supply the module. This diff touches the DAG
lexer, so its affected-set closure is much wider and does not, and they fail
unresolved type 'ArtifactIdentity'. The defect is pre-existing; the widened closure is what exposes it, and this PRcannot establish a compile-clean result without repairing it.
The three files are
hermetic_fixture_realization_test,realize_kernel_test, andreconcile_in_process_cache_test; each gets the one load-bearing import. It is not redundant —its absence is the compile failure — so it works with the import-deletion lane rather than
against it.
A first attempt at this census was wrong and is worth recording. A grep for
ArtifactIdentityreturned six files, and all six were "fixed". Three of those were false: two self-host witnesses use
a different declaration with the same short name (
v2.compiler.self_host.generation, a coproduct)which they already import, so the added import created two authorities for one name; and one Spark
witness matched only on the suffixes
RuntimeArtifactIdentity/ModelArtifactIdentity. Those threeimports are removed.
That error is the same failure class as the defect it was chasing: a name-level observation
standing where bound declaration identity is required. The permanent census owed to the
import-deletion lane must therefore operate on provider file and bound declaration, never on a
grep roster, with the structural condition: every accepted cross-file reference binding projects
its provider file into the compilation dependency closure, independently of unrelated pool
membership.
Not claimed
well_formedchange and no resolve-ready construction boundary.NormalizedTreeis still= Nodeandresolvestill consumes that alias, so retained cannot reach resolve holds only by propagation,not by construction. That is the next increment and it is not in this PR.
dag/std/algebra.dagis not re-confirmed after the lexer repair — the probe again exceededits budget, now doing strictly more work because it no longer stops at lex. The lex wall is
claimed closed on the minimal pairs, not on that member.
src/v2/std/node.dagisNOT RE-OBSERVED— the interpreted probe exceeded its 900s budget. Abudget interruption is not a verdict, and it is not discharged by copying the historical value.
src/v2/std/algebra.dagremains uncaptured and stays visibly on the board.supersession pointer to the new one.
types.dagremains at LEX with its cause unattributed, andnode.dag's member stage isunmeasured — neither may carry a scheduled repair.