Repository navigation
De-fork ConstructorReferenceAdmission onto one exact-identity authority (+ full control envelope) - #7902
Merged
Conversation
…authority #7859 added a SECOND admission decision in 04_lookup.dag (FuncSigCallerNotAdmitted, module-grain) beside the exact DeclRefCoords decision 04_infer.dag already carried — one concept, two decision sites, at two different grains. DESIGN §3. Removes the lookup-side decision and its FuncSigLookup variant, deleting both translation arms in 04_infer.dag. The exact-identity check (constructor_call_admission_diags via decl_ref_coords_equal) is retained as the single authority. Also hoists constructor_reference_admission_early_refusal above the arity split so the refusal is not confined to the zero-arity branch. NOTE: this widens the wall to function-value references; that half is pending an operator ruling and is separable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
regen_stage0 wrote 133 files; exactly the three corresponding to the three edited .dag modules changed. Fixed point reached in one generation: rebuilding from the new seed and re-running --verify gives regen_divergence_count=0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The existing admission test only distinguishes MODULES: an unlisted caller in a different module is refused. Nothing exercised a caller sitting in the same module as the admitted one, which is the case that pins the surviving authority's grain. constructor_call_admission_refuses_same_module_unlisted_sibling compiles a caller_ok module holding both the admitted ok_call and an unadmitted sneak_call, and asserts the refusal names sneak_call and does not name ok_call. Green by execution: cargo test -p v1-compiler --release --lib constructor_call_admission 2 passed Deliberately NOT enrolled as a de-fork discriminator. The deleted module-grain check admitted this case, but 04_infer's exact check refused it anyway, so behavior is identical before and after the de-fork -- as it must be, since a de-fork that changed behavior would be a bug. The in-code comment says so rather than letting the name imply a stronger claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
compiler_tests_rust_blobs_are_all_rostered compares the count of `\nfn ct_` declarations in compiler_tests_rust.dag against the roster rows for carrier v1.compiler.compiler_tests_rust. Adding the same-module sibling control moved declared to 37 while rostered stayed 36. Adds the row AND its membership in language_source_scaffold_roster -- declaring the data row alone does not enroll it, since rostered_count_for folds over the list. Verified by execution (fresh claim_batch): PASS compiler_tests_rust_blobs_are_all_rostered Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 6, 2026
Answers the question this lane could not resolve earlier: the ConstructorReferenceAdmission de-fork is #7902 (defork-constructor-admission). #7859 CREATED the fork it removes, so #7859 is not the de-fork and the gate must never be inferred from main moving. #7902 changes src/v1/04_infer.dag, so any frontier measurement taken before it merges is stale by construction. Records the operator-ordered sequence on the closeout carrier: interrupted-run receipt, then the FrontierMeasurementProvenance coproduct (so the survey does not rewrite roster rows through the provenance-conflating constructor this branch documents), then #7902, then the authoritative survey. Records the retry environment ruling: the survey must run in a fresh job or runner whose real kill boundary is observable, not in a session envelope reporting cgroup 0::/ that an ancestor can kill invisibly. The 27 modules shard, every receipt carries the same exact subject, and a killed shard is RERUN -- never hand-reconciled, since reconciling a shard that ran against a different subject is what turns a partial survey into a fabricated one. Verified: zero own-file diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…tructor identity
Operator ruled the admission check stays ABOVE the arity guard: the authority is
ConstructorReferenceAdmission, not zero-arity-invocation admission, so an unlisted
caller must not be able to obtain a nonzero-arity constructor as a function value and
invoke it from somewhere else.
Adds the two controls that axis needs, both green by execution:
constructor_call_admission_refuses_unlisted_function_value_reference
sneak_ref unlisted, takes mint as a value without calling -> refuses
ok_call listed, takes mint as a value and calls it -> clean
use_plain ordinary non-sealed fn used as a value -> clean
The third is the negative control: a wall that refused every function value would
pass the first two and look correct.
constructor_call_admission_qualified_caller_reports_undoubled_identity
An unlisted caller reaching the constructor by qualified projection refuses, AND
the refusal carries the same constructor identity the imported path produces.
FIX FOUND BY THAT SECOND CONTROL: constructor_decl_name was the call-site spelling, so
a qualified call rendered as 'mint_mod.mint_mod.mint' -- the module prefix applied
twice. Now qualified_last_segment (the existing authority in 00_core.dag, already
imported here), not a new helper. Asserting only that the refusal fires would have
passed straight over this.
cargo test -p v1-compiler --release --lib constructor_call_admission
4 passed
Roster 39 == 39. Two generations regenerated (emitter, then the tests it emits).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…mission # Conflicts: # src/v1/stage0/src/v1_compiler_infer.rs
The merge conflicted only in the generated src/v1/stage0/src/v1_compiler_infer.rs; the .dag sources merged cleanly. Generated files are never hand-resolved -- resolved by regenerating from the merged sources. Fixed point verified: regen_divergence_count=0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 6, 2026
…t jobs, four-PR gate
Three operator rulings supersede what this branch previously recorded.
NAMED SUCCESSOR, corrected shape. The provenance carrier is
FrontierEvidenceProvenance, not FrontierMeasurementProvenance, and
ExecutionMeasured takes a TYPED subject and a TYPED receipt rather than
free-form fields:
ExecutionMeasured { subject: FrontierSurveySubject, receipt: FrontierProbeReceipt }
KnowledgeAttributed { source: DeclarationRef, dissolve_on: DeclarationRef }
OracleDerived { oracle: DeclarationRef }
The row constructor must CONSUME the variant, so a row cannot claim
execution-measured provenance without carrying the receipt that proves it. That
turns this branch's rung-inflation finding from a documented defect into an
unwritable one -- a constructor named execution_measured_* that accepts ordinary
caller-provided blocker fields is a name-level claim, not evidence.
EXECUTION MODEL: 27 INDEPENDENT JOBS, NOT ONE PROCESS. One pinned subject, 27
independent module jobs, one receipt artifact per module, one exact-subject
aggregator. This is designed directly out of the failure this receipt records:
the costly property of the six runs was not that they died but that each death
cost EVERYTHING -- the one-shot lost all 27 modules when module 1 was killed. A
killed job now yields one interrupted row, rerun independently, and twenty-six
completed rows survive the twenty-seventh being SIGKILLed. A monolithic process
must not be retried in the same opaque envelope: the ancestor killer is still
unobservable from inside, so the answer is a visible kill boundary, not a bigger
cap.
GATE IS FOUR MERGES, NOT ONE: #7908 (whole-tree compile zero), #7902 (de-fork,
now READY at 227d9cb with its eight-control admission envelope green and the
arity ruling applied), #7925 (all-seven stage0 partition crate compile gate),
then this receipt. No authoritative survey runs on a head carrying compiler
diagnostics or a duplicated admission authority.
Also records the required output shape, whose last line is load-bearing: blocker
groups by DETAILED cause, not high-level reason strings. The 14 modules sharing
parse_grammar_choice_overlap_residue must have their detailed causes separated,
because the next phase ranks by largest DETAILED group on the premise that one
root governs many.
The receipt gets a pointer to the execution model rather than a copy of it; the
carrier stays the single authority.
Verified: zero own-file diagnostics.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Adds the zero-arity half of the arity matrix the eight-control envelope requires. Control 1 (listed caller of a zero-arity sealed constructor succeeds) holds. Control 2 does not, and the reason is not this PR. Writing it exposed a fail-open that PREDATES the de-fork and lives in a different mechanism than the guard placement this PR moved: an unlisted caller may reference a zero-arity sealed constructor and receive no diagnostic at all, in both the bare-reference and explicit-call spellings. Proven by execution on two fixtures identical but for the constructor's arity -- one-arity refuses, zero-arity emits zero diagnostics. Root-cause lead (unconfirmed): infer_sigs builds the resolved signature env from `params |> count > 0 && body != none`, so a zero-arity declaration is never in func_env; admission resolves through the global-bare fallback, which carries a binding's resolved node rather than the declaration node, and fn_admit_callers reads admit_callers off n.properties. The property survives the parse for both arities (verified in the emitted artifact), so this is a lookup defect. Control 2 is quarantined as an executing known-red: the assertion is inverted so the probe greens on the defect and REDS the moment the wall holds, forcing whoever closes the hole to flip it into a permanent regression control. It is not evidence the wall is complete. A speculative fix to func_decl_binding_for_call was written, measured to have no effect, and reverted rather than carried. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 6, 2026
…ight controls green Operator pass found two status claims in the closeout note that had rotted since they were written. Neither touches the interruption receipt or the roster provenance rung-inflation finding, which are the value of this PR and are unchanged. HEAD AND STATE. The note named #7902 as READY (not draft) at head 227d9cb. It is now DRAFT by operator ruling at head 42b5d00. ENVELOPE. The note claimed all eight admission controls green by execution. They are not, and the gap is a real defect rather than an unwritten test: writing control 2 exposed a fail-open where an unlisted caller can reference or invoke a ZERO-ARITY sealed constructor with no admission diagnostic at all, in both the bare-reference and the explicit-call spelling, proven by execution on two fixtures identical but for constructor arity. #7902 carries it as an inverted known-red, and the operator has ruled it is closed inside #7902 rather than merged as a known-red. Accurate statement is seven of eight green with the eighth quarantined pending that fix, so the gate does not open on a claim of eight. Recorded with the consequence for this lane attached: a survey taken against a head where a zero-arity sealed constructor is reachable without admission measures the wrong tree. Dropped the trailing "arity ruling applied" clause rather than carrying it forward unverified. That is the point of this correction - a status claim restated in a second place is a claim that rots silently, which is the same defect class this PR exists to record, so the note now asserts only the status the gate actually depends on. Gate structure is unchanged and stays separated as landed last round: four merges gate the merge, the FrontierEvidenceProvenance coproduct is the fifth and gates the survey. Verified: zero own-file diagnostics; no stale 227d9cb or eight-control reference survives anywhere in the tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 7, 2026
…) + roster provenance rung-inflation finding (#7901) * WIP: Authoritative exact-head 27/27 frontier survey * Frontier survey: executed memory-refusal receipt + roster provenance finding The authoritative 27/27 exact-head survey DID NOT RUN. This lands the executed refusal, not a measurement, and carries no frontier counts. frontier_probe_emit_from_ingest is OOM-killed before emitting a receipt for any module: five invocations, five kills, zero receipts. One-shot over all 27 (killed during module 1 of 27), plus 03_normalize, 03_resolve and 01_tokenize individually at --source-root src/v2 + dag, plus 03_normalize at src/v2 alone. Host cgroup memory.max = 33578549248 (31.3 GiB). All five die at the same place: after the per-module probe begins, inside the interpreted evaluation, with the ingest closure already fully read. Instrument control, because exit 137 alone proves nothing: cgroup oom_kill incremented 1 through 5, one per killed run, in lockstep. A 15-second RSS sampler saw only ~2.6 GB because the climb happens between samples; that figure is an artifact, not the working set. Two hypotheses raised and REFUTED by execution before being reported as causes: (a) that the 10 never-measured modules are the memory-bound ones -- refuted by 01_tokenize, one of the 17 that DID measure at 9f978aa; (b) that the widened src/v2 + dag root set is the cause -- refuted by 03_normalize OOMing at src/v2 alone. Cause remains open. Regression vs host capacity is UNRESOLVED and not resolvable here: three builds of the probe at old head 9f978aa were all OOM-killed (jobs=15, jobs=1, debug). The single-job attempt is decisive -- one rustc process still exceeded the cap, so this host cannot cold-build v1-compiler at all, and the current-head build succeeded only via sccache. Reported, not chased, per operator direction; a probe trimmed to fit a box measures a different question. Consequence: 27/27 is unreachable by BOTH documented paths, since a single module in a fresh process exhausts the cap alone. Fanning the 27 across workers does not address a per-module failure. Second, independent finding (DESIGN 4b rung inflation in the roster carrier): knowledge_attributed_blocker_class_seed_retained_row has ZERO call sites repo-wide, while all 10 never-measured roster modules are authored through execution_measured_seed_retained_row, whose name asserts execution measurement. That constructor takes blocker, stage and reason as ordinary parameters, so it cannot distinguish measured from attributed -- the NAME asserts a provenance the TYPE does not carry. No roster row is edited here; frontier.dag is load-bearing and the construction fix (a provenance field) is flagged for routing. Recipe corrections found by execution: ctrl-build defaults to remote and BuildBuddy refuses a detached worktree, so the mandated detached worktree and the default build path are mutually exclusive and ctrl-build --local is required. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct the memory attribution: cgroup never hit its cap; both claims withdrawn An independent same-cap control cold-built v1-compiler at a 3.26 GiB peak with zero kills, refuting this receipt's earlier host-capacity claim. Re-reading my own counters refutes the other one. memory.max 33578549248 31.3 GiB memory.peak 9136902144 8.5 GiB high-water across EVERY run memory.events max 0 oom 0 oom_kill 10 max 0 means allocation NEVER reached memory.max; oom 0 means the CGROUP oom killer was never invoked; in cgroup v2 oom_kill also counts tasks reaped by a killer above this cgroup. The cgroup never exceeded 27% of its cap, so the kill decisions were made outside its limit entirely. WITHDRAWN (marked withdrawn in place, not deleted): - "the probe requires more than 31 GiB" -> memory.peak is 8.5 GiB - "this host cannot cold-build v1-compiler" -> refuted by the control Root error, named so it does not recur: oom_kill incrementing in lockstep is a sound control for "was this a kill" and worthless for "what hit the limit". memory.events max/oom and memory.peak answer that, and were available throughout. Not a leak either: memory.current was 391MB before the jobs=1 build with no cargo/rustc running, and memory.peak never moved. A retry under low host load survived to 3.5 minutes at ~2.0 GB, past every earlier run, then was killed anyway without raising memory.peak. Cause is not attributable from inside the container (/proc/self/cgroup is namespaced to 0::/); reported as an operator finding rather than guessed at. Consequently the lane is INTERRUPTED AND RETRYABLE, not blocked, and probe memory cost is UNMEASURED rather than high. Doc and carrier note renamed off "memory_refusal", which asserted the conclusion the evidence killed. Both recipe-defect predictions also refuted by execution: - no module collision: duplicate module in a third root does not refuse, tested both inside and outside target/ - target/-resident roots ARE indexed: an invalid .dag there fails the compile loudly (parse error naming the file, exit 101), so the emitted manifest will be read Only the ctrl-build --local defect survives. The vacuous-green property is recorded separately: partition-totality passes on an empty manifest, so it can never evidence that a survey ran. Verification: all three edited .dag modules compile with zero own-file diagnostics. Incidental and unrelated: 4 hard diagnostics in dag/extdeps/systems/nvidia.dag (SPARK-0, byte offsets, DESIGN 4c body-grain annotation refusal), present tree-wide and untouched by this branch. Rung-inflation finding is unaffected and unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Name #7902 as the gating branch and record the operator retry sequence Answers the question this lane could not resolve earlier: the ConstructorReferenceAdmission de-fork is #7902 (defork-constructor-admission). #7859 CREATED the fork it removes, so #7859 is not the de-fork and the gate must never be inferred from main moving. #7902 changes src/v1/04_infer.dag, so any frontier measurement taken before it merges is stale by construction. Records the operator-ordered sequence on the closeout carrier: interrupted-run receipt, then the FrontierMeasurementProvenance coproduct (so the survey does not rewrite roster rows through the provenance-conflating constructor this branch documents), then #7902, then the authoritative survey. Records the retry environment ruling: the survey must run in a fresh job or runner whose real kill boundary is observable, not in a session envelope reporting cgroup 0::/ that an ancestor can kill invisibly. The 27 modules shard, every receipt carries the same exact subject, and a killed shard is RERUN -- never hand-reconciled, since reconciling a shard that ran against a different subject is what turns a partial survey into a fabricated one. Verified: zero own-file diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Align the recipe and bind rows with the corrected reading (review 49553) Review found that commit c2edc86 corrected the survey carrier but left the LOCAL RECIPE text carrying the pre-correction reading -- a second, contradictory authority for the same facts, which is the DESIGN 3 single-authority violation this PR otherwise documents. Both findings verified against current code and both are real. gunbc.ci_layer_roots compiler_frontier_per_module_probe_exclusion_note: replaced "BLOCKED BY EXECUTED REFUSAL / OOM-killed / both paths unreachable / a single module exhausts the cap alone" with what the counters support -- runs interrupted, cause OPEN and not a demonstrated capacity limit (memory.events max 0, oom 0; memory.peak 8.5 GiB against a 31.3 GiB cap), probe memory cost UNMEASURED, "unreachable" NOT established, retry in a fresh job or runner with an observable kill boundary. The clause now points at frontier_probe_run_interruption_note rather than restating it, so there is one authority instead of two. gunbc.doc_graph_roots: dropped the "(memory refusal resolved)" parenthetical and "refusal receipt" wording from the bind dissolution; the trigger is the carrier's own -- the probe emits a receipt for at least one module. Swept the rest of the diff for the same staleness rather than fixing only what review cited, which surfaced two more the review did not mention: - the interruption note still opened "EXECUTED REFUSAL" and said frontier_probe_emit_from_ingest "is OOM-killed" - BOTH the note and the receipt said FIVE invocations; there were SIX. The low-host-load 01_tokenize retry -- the run that survived to 3.5 minutes at ~2.0 GB and is the strongest single piece of evidence against the capacity reading -- was described in prose but missing from the count and the table. An undercount in a receipt whose whole purpose is negative evidence is the same defect class review caught, so it is fixed here rather than left for a later reader to trip over. Verified: all three edited .dag modules compile with zero own-file diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Apply operator refinements: FrontierEvidenceProvenance, 27 independent jobs, four-PR gate Three operator rulings supersede what this branch previously recorded. NAMED SUCCESSOR, corrected shape. The provenance carrier is FrontierEvidenceProvenance, not FrontierMeasurementProvenance, and ExecutionMeasured takes a TYPED subject and a TYPED receipt rather than free-form fields: ExecutionMeasured { subject: FrontierSurveySubject, receipt: FrontierProbeReceipt } KnowledgeAttributed { source: DeclarationRef, dissolve_on: DeclarationRef } OracleDerived { oracle: DeclarationRef } The row constructor must CONSUME the variant, so a row cannot claim execution-measured provenance without carrying the receipt that proves it. That turns this branch's rung-inflation finding from a documented defect into an unwritable one -- a constructor named execution_measured_* that accepts ordinary caller-provided blocker fields is a name-level claim, not evidence. EXECUTION MODEL: 27 INDEPENDENT JOBS, NOT ONE PROCESS. One pinned subject, 27 independent module jobs, one receipt artifact per module, one exact-subject aggregator. This is designed directly out of the failure this receipt records: the costly property of the six runs was not that they died but that each death cost EVERYTHING -- the one-shot lost all 27 modules when module 1 was killed. A killed job now yields one interrupted row, rerun independently, and twenty-six completed rows survive the twenty-seventh being SIGKILLed. A monolithic process must not be retried in the same opaque envelope: the ancestor killer is still unobservable from inside, so the answer is a visible kill boundary, not a bigger cap. GATE IS FOUR MERGES, NOT ONE: #7908 (whole-tree compile zero), #7902 (de-fork, now READY at 227d9cb with its eight-control admission envelope green and the arity ruling applied), #7925 (all-seven stage0 partition crate compile gate), then this receipt. No authoritative survey runs on a head carrying compiler diagnostics or a duplicated admission authority. Also records the required output shape, whose last line is load-bearing: blocker groups by DETAILED cause, not high-level reason strings. The 14 modules sharing parse_grammar_choice_overlap_residue must have their detailed causes separated, because the next phase ranks by largest DETAILED group on the premise that one root governs many. The receipt gets a pointer to the execution model rather than a copy of it; the carrier stays the single authority. Verified: zero own-file diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix gate enumeration (five prerequisites, not four) and align dissolve-on with the doc bind Both findings in review 49609 verified against the tree and confirmed real. GATE ENUMERATION. The closeout note said "FOUR merges gate the authoritative survey" and "the gate opens after all four", then added a fifth prerequisite -- FrontierEvidenceProvenance -- in a later sentence of the same paragraph. Read as written, the four-merge list authorizes a survey run before provenance is structural, which would rewrite roster rows through the provenance-conflating constructor: precisely the rung inflation this receipt files. The note now says FIVE prerequisites and separates the two gates it was conflating -- the MERGE gate opens after the four merges, the SURVEY gate only after the fifth -- and states plainly that reading the four merges as the whole gate authorizes the defect. The duplicate provenance sentence downstream is deleted rather than left beside the corrected one, since two statements of one gate is how the disagreement arose in the first place. DISSOLVE-ON. frontier_probe_run_interruption_note dissolved on ONE condition (a probe receipt at a pinned subject) while the HandAuthoredDocBind for the same artifact requires TWO (receipt AND structural roster provenance). The bind is correct and the note was wrong: that bind carries frontier_roster_provenance_constructor_inflation_note as an additional work, so the weaker trigger would have deleted the receipt while the provenance finding it carries was still live -- a scaffold dissolving before its own trigger fires. The note now carries both conditions and names the bind as the single authority for when the doc deletes, so the two cannot drift apart again silently. Checked the md for a third copy: it states no dissolution, so there are exactly two authorities and they now agree. Verified: zero own-file diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct two stale #7902 status passages: DRAFT at 42b5d00, seven of eight controls green Operator pass found two status claims in the closeout note that had rotted since they were written. Neither touches the interruption receipt or the roster provenance rung-inflation finding, which are the value of this PR and are unchanged. HEAD AND STATE. The note named #7902 as READY (not draft) at head 227d9cb. It is now DRAFT by operator ruling at head 42b5d00. ENVELOPE. The note claimed all eight admission controls green by execution. They are not, and the gap is a real defect rather than an unwritten test: writing control 2 exposed a fail-open where an unlisted caller can reference or invoke a ZERO-ARITY sealed constructor with no admission diagnostic at all, in both the bare-reference and the explicit-call spelling, proven by execution on two fixtures identical but for constructor arity. #7902 carries it as an inverted known-red, and the operator has ruled it is closed inside #7902 rather than merged as a known-red. Accurate statement is seven of eight green with the eighth quarantined pending that fix, so the gate does not open on a claim of eight. Recorded with the consequence for this lane attached: a survey taken against a head where a zero-arity sealed constructor is reachable without admission measures the wrong tree. Dropped the trailing "arity ruling applied" clause rather than carrying it forward unverified. That is the point of this correction - a status claim restated in a second place is a claim that rots silently, which is the same defect class this PR exists to record, so the note now asserts only the status the gate actually depends on. Gate structure is unchanged and stays separated as landed last round: four merges gate the merge, the FrontierEvidenceProvenance coproduct is the fifth and gates the survey. Verified: zero own-file diagnostics; no stale 227d9cb or eight-control reference survives anywhere in the tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Replace the mutable gate status with a static admission contract Operator ruling, superseding the two status patches it follows. The defect was not that the sentences were wrong; it was that the note was acting as a MUTABLE BOARD, so every merge made it wrong again and the fix arrived as another hand-patch. Two rounds of that is the signal. REMOVED from the closeout note: the four-PR gate list, the de-fork's head SHA, its draft state, and the seven-of-eight control tally. No PR number, no SHA, no lifecycle state, no tally survives anywhere in the file. REPLACED WITH conditions on the tree, which stay true as heads move and changes land. The authoritative survey may start only when all four hold: whole-tree hard diagnostics equals zero; ConstructorReferenceAdmission has one authority and no known-red control; all seven partition crates are continuously checked; FrontierEvidenceProvenance is construction-enforced. Each is decidable against whatever head is current, and for which change carries which condition the reader is sent to the board rather than to a second copy of it here. Two conditions are spelled out because they are easy to under-read. Condition 2 is not discharged by a de-fork landing while a control stays inverted -- one authority AND no known-red are both required, since a partially admitted constructor authority means the survey measures a tree in which a sealed constructor is reachable without admission. Condition 4 is what stops the survey writing all 27 roster rows through the conflating constructor. Why the reasoning is kept rather than just the list: a receipt that restates mutable status is a claim asserted in a place that cannot check it, which is the same defect class frontier_roster_provenance_constructor_inflation_note files one layer down. Recording that connection is what stops the next author reintroducing a status line here. Also sharpened the successor so it cannot read as landed implementation: the contract now says condition 4 is a construction wall to be BUILT and that this receipt does not build it -- this receipt RECORDS the provenance defect, the separate FrontierEvidenceProvenance change FIXES it. The PR body carries the same correction, retitled proposed shape NOT landed here, with the closing line changed from asserting the finding is already unwritable to stating that the defect stands recorded and unfixed until that change lands. Substantive content is untouched: zero receipts means no frontier measurement, the run was interrupted rather than proven memory-bound, the visible cgroup never reached its own limit, the survey needs independent module jobs, and the existing constructor inflates knowledge-attributed rows to execution-measured. Verified by execution: zero own-file diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
marked this pull request as ready for review
August 7, 2026 05:04
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
…iscriminator The admission lookup returned a binding's resolved VALUE node in four of its five arms. A value node carries no admit_callers property, so fn_admit_callers found nothing and the wall admitted every caller of any name resolving through one of them. Zero-arity sealed constructors were the live population: an unlisted caller could reference or invoke one with no diagnostic in either spelling, while a one-arity name happened to resolve through the symbol index and refused correctly. Arity was a correlate of which path ran, never the distinguishing fact, so the repair is uniform rather than arity-specific. constructor_declaration_for_admission resolves the declaration by exact qualified name and returns a three-way ConstructorDeclarationLookup. The owner must be LOCATED, not guessed: only func_decl_owner_module and borrowed_census_decl positively assert that a declaration of this name lives in the module they name, so a name no locating authority claims is NotAdmissionBearingReference. Resolving against a guessed owner and treating the index miss as unrecoverable turned a wrong guess into a hard refusal -- measured on the whole tree that fabricated 11 refusals over three ordinary data declarations, none of them constructors. The unavailable arm is reserved for the genuinely anomalous case: a positively located declaration the index cannot produce, which refuses rather than falling back to a provenance-losing node. Admission decides a resolved declaration identity, not an identifier spelling. Hoisting the check above the ExprVar arm closed the fail-open and simultaneously refused a parameter named token, converting one section 5 violation into its mirror image. body_locals -- the corpus's existing shadowing authority -- is reused rather than a second notion of shadowing being minted beside it. Controls: listed/unlisted zero-arity bare reference and explicit call, qualified identity rendering, an ordinary nonsealed zero-arity function as the widening detector, and parameter/let shadowing. The inverted zero-arity quarantine that asserted the defect is flipped to a permanent regression control rather than retired. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Both defects are the DESIGN section 3 class -- a claim in a comment that a grep decides, sitting false while the mechanism it describes stays correct. extdeps_external_authority_anchor was described as "a homonym declared in two modules". It is declared under that one name in 459 modules across dag/extdeps -- a per-module anchor convention, not a two-way collision. The measurement the sentence supports (11 fabricated refusals over three ordinary data declarations) is unaffected, but the reason it matters is stronger than stated: a guessed owner picks one of 459 homes, so the index miss that follows says nothing whatever about admission. NotAnAdmissionBearingConstructor named nothing. No such symbol exists anywhere in the tree; the variant is NotAdmissionBearingReference. A fabricated symbol in a comment is worse than a stale line, because it reads as a citation and resolves to nothing. The other six symbols cited in these comment blocks were swept and all resolve. Also carries generation 1's emitted sources for the three changed .dag modules. This is an INTENTIONALLY INCOMPLETE generated head: compiler_tests.rs is not yet regenerated, because producing it requires evaluating the ct_* generator functions with a binary built from generation 1's output. The fixed point is therefore not reached and the drift gate is expected to red here. Comments cannot move emitted bytes (DESIGN section 4c), so the .dag correction above does not invalidate the emitted sources committed with it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Generation 1 rebuilt the generator (v1_compiler_compiler_tests_rust.rs); this is generation 2, where a binary built from that generator evaluates compiler_tests_source() and emits the controls themselves. One file changed, exactly as the fixed-point sequence predicts. CI's regen on srv4 reported the same single divergence independently before this ran. Until this commit the seven controls existed only as generator source and had never been compiled, let alone executed -- specification without execution, which is the trap the controls themselves exist to close. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e claim 04_lookup.dag carried a local qualified_last_segment_local beside v1.std.core's qualified_last_segment, which 04_infer.dag already uses -- two spellings of "qualified name -> declaration leaf" inside one compiler pipeline. There was no layering constraint to justify it: 04_lookup already imports v1.std.core, so the duplicate was gratuitous. Deleted in favour of the existing authority. The two were NOT identical implementations. The canonical routes through module_path_segments, which maps "" to the empty list; the local used raw split(name, "."). They converge on every input -- both answer "" for empty -- so there is no behaviour change, but that is luck rather than design, and two qualified-name splitters with different empty-case handling is exactly the shape that later renders one identity differently from the other. Also narrows an evidence claim in 04_infer.dag. The shadowing comment asserted body_locals covers fn parameters, let bindings, match binders and lambda parameters, while the executed controls prove only the first two. Match binders and lambda parameters do inherit the arm by construction, because it reads body_locals rather than enumerating forms -- but inheritance by construction is not execution, and stating four where two ran is rung inflation at comment grain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 7, 2026
6 tasks
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
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.
De-forks ConstructorReferenceAdmission onto one exact declaration-grain authority.
Root: declaration provenance was lost through
binding.resolvedThe admission lookup returned a binding's resolved value node in four of its five arms. A value node is the right subject for type inference and the wrong subject for declaration policy: it carries no
admit_callersproperty, sofn_admit_callersfound nothing, saw no admission list, and admitted every caller of any name resolving through one of those arms.Zero-arity sealed constructors were the live population — an unlisted caller could reference or invoke one with no diagnostic in either spelling. Arity was a correlate of which lookup path ran, never the distinguishing fact: a one-arity name happened to resolve through the symbol index and refused correctly. An earlier revision of this PR proposed a
params |> count > 0root cause; that hypothesis is refuted and the repair is uniform rather than arity-specific.Authority: one exact declaration-grain decision
constructor_declaration_for_admissionresolves the declaration by exact qualified name and returnsConstructorDeclarationLookup:Admission facts are read from the declaration node only. #7859's second, module-grain decision (
FuncSigCallerNotAdmittedonFuncSigLookup) is deleted along with both of its translation arms, leaving one post-resolution authority.Shadowing:
body_localsprecedes constructor lookupAdmission decides a resolved declaration identity, never an identifier spelling. Hoisting the check above the
ExprVararm closed the fail-open and simultaneously refused a parameter namedtoken— converting one DESIGN §5 violation into its mirror image.body_localsis the corpus's existing shadowing authority (call_locals_shadow_note), so it is reused rather than a second notion of shadowing being minted beside it.Negative state: located-and-missing refuses; unlocated stays ordinary
The owner must be located, not guessed. Only
func_decl_owner_moduleandborrowed_census_declpositively assert that a declaration of this name lives in the module they name. Resolving against a guessed owner and treating the index miss as unrecoverable turned a wrong guess into a hard refusal — measured on the whole tree, that fabricated 11 refusals over three ordinary data declarations (srv3_nbd_proxy_local_port,gnu_bash_subject_ref,extdeps_external_authority_anchor), none of them constructors.So a name no locating authority claims is
NotAdmissionBearingReference, and the unavailable arm is reserved for the genuinely anomalous case: a positively located declaration the index cannot produce, which refuses rather than falling back to a provenance-losing node. A fabricated refusal is a wrong answer exactly as a fabricated success is.Evidence
Generated control envelope — executed, not merely written. Denominators kept separate on purpose:
Covering: listed/unlisted zero-arity bare reference; listed/unlisted zero-arity explicit call; unlisted qualified call reporting an undoubled identity; listed/unlisted nonzero-arity function value; ordinary non-sealed function value; same-module listed/unlisted siblings; parameter shadowing;
letshadowing.The combination is what matters:
ordinaryis the widening detector — an implementation that satisfied the wall by refusing more things would pass the refusal controls and fail this one.Self-host fixed point. Three generations were required, and the sequence is itself the finding: generation 1 rebuilt the generator, generation 2 emitted the controls from it, generation 3 was clean. Confirmed independently on BuildBuddy at this exact head:
Until generation 2 landed, the seven controls existed only as generator source and had never been compiled, let alone executed.
Local Rust test attempt — stated as a differential receipt, because the ordinary/heavyweight partition does not exist in this tree and there is therefore no total denominator to claim a pass against:
The repository CI job does not execute those three scanners, so it is independent build/regeneration/floor evidence and is explicitly not claimed as coverage for them.
Single-authority cleanup
04_lookup.dagbriefly carried a localqualified_last_segment_localbesidev1.std.core'squalified_last_segment. There was no layering constraint —04_lookupalready importsv1.std.core— so the duplicate is deleted. The two were not identical implementations (canonical routes throughmodule_path_segments, which maps""to the empty list; the local used rawsplit); they converge on every input, but two qualified-name splitters with different empty-case handling is the shape that later renders one identity differently from the other.Scope — what this does NOT establish
admit_callershas no production population today; its live population is fixtures. This PR delivers the language capability and its exact-identity authority, not a production behavioural receipt.Declaration totality is not proven. A declaration carrying
admit_callersthat enters through a path neither locating authority represents would land inNotAdmissionBearingReferenceand bypass admission. That is bounded today only because no production constructor carriesadmit_callers. The named successor is a declaration-totality wall — an exact identity join between all declarations carrying nonemptyadmit_callersand all admission-indexed constructor declarations, reporting missing / extra / duplicate / ambiguous / unresolvable — and it must land before the first production admission-bearing constructor, not after.Shadowing evidence covers two binder forms, not four. The controls prove fn-parameter and
letshadowing. Match binders and lambda parameters inherit the arm by construction, because it readsbody_localsrather than enumerating forms — but inheritance by construction is not execution.