Skip to content

ConstructorReferenceAdmission: refuse unlisted call edges to a sealed constructor - #7859

Merged
briansrls merged 7 commits into
mainfrom
session/tidy-fox-81
Aug 6, 2026
Merged

briansrls merged 7 commits into
mainfrom
session/tidy-fox-81

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session tidy-fox-81.
Pushing to session/tidy-fox-81 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

@briansrls
briansrls marked this pull request as ready for review August 5, 2026 16:53
@cursor

cursor Bot commented Aug 5, 2026

Copy link
Copy Markdown

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.

@gunbai-bot

gunbai-bot Bot commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

Response to review 48859 (claude-opus-4-7)

Verified each finding against 28181111c after rebase on main + regen.

1. admit_callers bypassed on the normal resolution path — CONFIRMED, not fixed in this PR.

lookup_func_sig still returns early from lookup_resolved_sig (04_lookup.dag ~81–88). The fn_admit_callers gate runs only inside func_sig_from_global_bare (census / whole-pool fallback). Imported callees that resolve via lookup_resolved_sig never hit the gate. This is a §5 fail-open relative to the PR title’s scope.

2. Method-call arm not gated — CONFIRMED, scoped omission.

Method dispatch does not route through lookup_func_sig; admit_callers on a callee reached only via foo.method() is not checked here. Intentional for this lookup-path experiment unless we extend infer’s call seams.

3. Silent drop of non-string admit_callers entries — PARTIALLY ADDRESSED.

02_parse.dag now refuses empty admit_callers lists at parse time. fn_admit_callers in 00_core.dag still maps via collect_decl_ref_coords_from_list (decl_ref-only); non-decl_ref children are dropped without a located refusal — review point still valid for malformed literals.

4. No enrolled witness on imported path — CONFIRMED.

No witness proves refusal when the callee resolves through lookup_resolved_sig.

Disposition: This PR rebases cleanly on main and regen is at fixed point (regen_verify_gate_passes). The lookup-only gate does not satisfy ConstructorReferenceAdmission on the ordinary import-resolution path. royal-crab-235 is landing the infer-time construction wall (constructor_call_admission_diags post func_decl_binding_for_call, caller_decl_coords on InferScope) on a separate horn-only branch — that is the path that closes finding 1 with enrolled witnesses. Recommend closing or superseding this PR once that horn PR is ready rather than stacking a second admission authority in lookup.

— sent from royal-crab-235

@gunbai-bot
gunbai-bot Bot force-pushed the session/tidy-fox-81 branch from c052050 to 2818111 Compare August 5, 2026 17:13
@gunbai-bot

gunbai-bot Bot commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

Response to review 48866 (composer-2.5 REQUEST_CHANGES)

All three findings are confirmed on this branch. This PR implements lookup-path admission only (func_sig_from_global_bare + module-path strings), which bypasses lookup_resolved_sig for explicit imports and does not parse decl_ref admit_callers entries.

Build fix in bb7e31e58 (missing fn_admit_callers import in emitted infer_lookup) unblocks CI compile, but does not close the semantic gaps above.

Disposition: Superseded by #7860, which lands infer-time ConstructorCallAdmissionRefused post func_decl_binding_for_call with decl_ref coords, enrolled witness, and the owner/properties fixes from review 48870. Recommend closing this PR rather than stacking a second admission authority in lookup.

— sent from royal-crab-235

@gunbai-bot

gunbai-bot Bot commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

Response to review 48882 (composer-2.5 REQUEST_CHANGES)

Verified against 03cba6c7d:

1. Wrong diagnostic variant in witness — FIXED in 03cba6c7d. compiler_tests.rs now matches ConstructorReferenceAdmissionViolation; ConstructorCallAdmissionRefused no longer appears in the tree. Same commit added the missing cli_run histogram arms that blocked build.

2. Hand-edited witness not in compiler_tests_rust.dag — CONFIRMED, not fixed here. constructor_call_admission_refuses_unlisted_cross_module_caller exists only in emitted compiler_tests.rs; there is no ct_constructor_call_admission_test() in compiler_tests_rust.dag. A stage0 regen would drop it. This is the §5 specification-without-execution gap the review names.

3. decl_ref admit_callers not parsed; positive control cannot pass — CONFIRMED, not fixed here. fn_admit_callers in 00_core.dag:950-955 still maps only expr_literal_string_optional children; decl_ref(...) becomes "" and is filtered, yielding an empty admitted list. Lookup-path enforcement (04_lookup.dag:167) then refuses all cross-module callers including caller_ok. The fixture does not exercise the intended admission path on this PR’s lookup-only design.

Disposition: Items 2–3 are structural to this branch’s approach. #7860 lands the conforming infer-time wall (ConstructorCallAdmissionRefused, decl_ref parsing in 02_parse.dag, ct_constructor_call_admission_test in compiler_tests_rust.dag, enrolled witness). Recommend closing #7859 rather than duplicating that work here.

— sent from royal-crab-235

@gunbai-bot

gunbai-bot Bot commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

Response to review 48894 (composer-2.5 REQUEST_CHANGES)

Re-verified on 03cba6c7d — all three findings confirmed, unchanged from review 48882:

1. Import path bypass (04_lookup.dag:81-88) — lookup_func_sig still returns FuncSigResolved from lookup_resolved_sig with no admit_callers check. Admission runs only in func_sig_from_global_bare (census fallback). The witness’s import mint_mod { mint } + bare mint(...) uses the normal parent-func_env resolution path, so unlisted callers are not refused on the path this PR’s title describes. §5 fail-open relative to stated scope.

2. decl_ref silently dropped (00_core.dag:953-955) — fn_admit_callers still maps only expr_literal_string_optional children; decl_ref(...) becomes "" and is filtered, yielding an empty admitted list while admit_callers remains present in source. Silent mis-modeling of authored DeclarationRef entries.

3. Witness not in emit authority (compiler_tests.rs vs compiler_tests_rust.dag:2328) — constructor_call_admission_refuses_unlisted_cross_module_caller exists only in hand-emitted compiler_tests.rs. compiler_tests_source() still ends at ct_sole_constructor_fieldless_witness_test() with no ct_constructor_call_admission_test(). Next stage0 regen drops the witness (§2 parallel representation / §5 specification-without-execution).

Why not fix on this PR: These are architectural to the lookup-only + module-path-string design. Repair requires infer-time enforcement post callee binding, decl_ref parsing in 02_parse.dag / collect_decl_ref_coords_from_list, and ct_constructor_call_admission_test() enrolled in compiler_tests_rust.dag — all landed on #7860 (ConstructorCallAdmissionRefused, 890828f42 owner/properties fixes). Closing #7859 is the correct disposition; duplicating #7860 here would fork the admission authority.

— sent from royal-crab-235

@gunbai-bot

gunbai-bot Bot commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

Response to review 48928 (composer-2.5 REQUEST_CHANGES)

Re-verified on 77accdb1f (includes ct_constructor_call_admission_test() enrollment from the regen_verify fix).

1. Import path bypass (04_lookup.dag:81-88 + 04_sigs.dag:144-163) — CONFIRMED, not fixable on this branch without redesign.

lookup_func_sig still returns FuncSigResolved straight from lookup_resolved_sig with no admit_callers gate. Admission runs only inside func_sig_from_global_bare when lookup is FuncSigUnresolved (census / global-bare fallback). The witness uses import mint_mod { mint } + bare mint(...), so both caller_ok and caller_bad resolve through parent func_env and never hit func_sig_from_global_bare. Infer’s FuncSigCallerNotAdmitted arm (04_infer.dag:2807-2808) is wired but unreachable for this fixture. §5 fail-open relative to the stated cross-module mint hole.

2. decl_ref roster not consumed (00_core.dag:950-955) — CONFIRMED.

fn_admit_callers still maps only expr_literal_string_optional children; decl_ref(module_path: "caller_ok", decl_name: "ok_call") becomes "" and is filtered, yielding an empty admitted list even when the global-bare path is hit. The witness syntax and lookup enforcement disagree on grain (module path strings vs DeclarationRef).

3. Witness emit authority — PARTIALLY ADDRESSED in 77accdb1f.

ct_constructor_call_admission_test() is now enrolled in compiler_tests_rust.dag (after ct_sole_constructor_test()), so stage0 regen retains constructor_call_admission_refuses_unlisted_cross_module_caller. That closes the parallel-representation / regen_verify gap named in review 48882. It does not close findings 1–2: the enrolled witness still does not exercise refused admission on the import-resolution path.

Disposition: Findings 1–2 are architectural to lookup-only + module-string admission. The conforming infer-time wall (ConstructorCallAdmissionRefused post func_decl_binding_for_call, decl_ref parsing, enrolled ct_constructor_call_admission_test) is on #7860 (CI green on session/royal-crab-235-horn-constructor-admission). Recommend closing #7859 rather than forking a second admission authority here.

— sent from royal-crab-235

@gunbai-bot

gunbai-bot Bot commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

Response to review 48965 (composer REQUEST_CHANGES)

Verified on head 2e35f4f65. All three findings are confirmed — no regression from the regen roster fix.

Finding 1 — import path bypass (04_lookup.dag:83)

Confirmed. lookup_func_sig still returns early from lookup_resolved_sig with no admission check:

fn lookup_func_sig(func_env: ResolvedFuncEnv, type_env: TypeEnv, name: String) -> FuncSigLookup {
  match lookup_resolved_sig(env: func_env, name: name) {
    FuncSigResolved { sig: sig } => FuncSigResolved { sig: sig }
    ...
    FuncSigUnresolved => func_sig_from_global_bare(type_env: type_env, name: name)
  }
}

The witness uses import mint_mod { mint } + bare mint(...), so both caller_ok and caller_bad resolve through func_env and never reach func_sig_from_global_bare. The production-stage-origin cross-module mint case stays unenforced on the normal import path (DESIGN §5 fail-open).

Finding 2 — selective-import / same-module branch (04_lookup.dag:136-163)

Confirmed. lookup_binding_by_name_local hits are wrapped with owner_module_path: type_env.module_path (:138), so they take the same-module branch at :155-163 and skip admission. The :165+ gate only runs for borrowed_census_decl global-bare hits. Enforcement is limited to unpooled census visibility, not explicit imports.

Finding 3 — decl_ref roster dropped (00_core.dag:950-955)

Confirmed. fn_admit_callers still maps only expr_literal_string_optional children; decl_ref(module_path: "caller_ok", decl_name: "ok_call") becomes "" and is filtered out. The witness oracle does not exercise std.decl_ref DeclarationRef identity, and module-grain matching at :167 does not use decl_name.

Why no further code on this PR

These are architectural limits of lookup-only admission, not fixable by extending the global-bare fallback. The intended fix is infer-time enforcement post callee binding (constructor_call_admission_diags after func_decl_binding_for_call), decl_ref parsing in fn_admit_callers, and scaffold-index + regen roster enrollment — landed on #7860 (session/royal-crab-235-horn-constructor-admission, CI green).

Recommendation: Close #7859 as superseded by #7860. This PR’s diagnostic/parse plumbing was a useful experiment; the review correctly blocks merge at lookup-only enforcement.

— sent from royal-crab-235

@gunbai-bot
gunbai-bot Bot force-pushed the session/tidy-fox-81 branch from 901e1c4 to 85e8a87 Compare August 5, 2026 20:25
Brian Searls and others added 7 commits August 5, 2026 21:59
Resolve SourceAnnotationRefused merge in 00_core and restore infer import
list after rebase; run regen to fixed point so CI regen_verify_gate passes.

Co-authored-by: Cursor <cursoragent@cursor.com>
Fixes build failure: emitted lookup calls fn_admit_callers without importing it.

Co-authored-by: Cursor <cursoragent@cursor.com>
Add cli_run histogram match arms for the new variant and align the
compiler_tests witness with ConstructorReferenceAdmissionViolation.

Co-authored-by: Cursor <cursoragent@cursor.com>
The hand-maintained compiler_tests.rs already carried
constructor_call_admission_refuses_unlisted_cross_module_caller but
compiler_tests_rust.dag did not emit it, so regen_verify_gate redded
with a stale compiler_tests.rs diff. Add ct_constructor_call_admission_test
so stage0 regen and the committed witness stay aligned.

Co-authored-by: Cursor <cursoragent@cursor.com>
Resolve merge conflicts by taking main's ConstructorCallAdmissionRefused
surface (#7860), updating lookup fn_admit_callers to decl_ref API, adding
FuncSigCallerNotAdmitted infer match arms, and regen stage0 emit.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot
gunbai-bot Bot force-pushed the session/tidy-fox-81 branch from 85e8a87 to 5b4e7f3 Compare August 5, 2026 22:12
@gunbai-bot

gunbai-bot Bot commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

Response to review 49098 (claude-opus-4-7 APPROVE)

Read the full stdout artifact — verdict only, no separate non-blocking remarks.

Disposition: No code change from this review. The branch already matches what review 49098 describes: FuncSigCallerNotAdmitted on the func_sig_from_global_bare census-fallback path, rendered as ConstructorCallAdmissionRefused, with exhaustive lookup_func_sig / func_sig_if_resolved matches and regen at fixed point (5b4e7f302).

Context (unchanged from prior reviews): infer-time admission is on main via gunbc#7860 (constructor_call_admission_diags post func_decl_binding_for_call with full decl_ref coords). This PR’s lookup layer is intentionally narrow — it does not gate lookup_resolved_sig success — so it supplements rather than replaces #7860. Closing vs keeping open remains an operator choice; review 49098 does not ask for further edits.

— sent from royal-crab-235

@gunbai-bot

gunbai-bot Bot commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

Response to review 49100 (composer-2.5 APPROVE)

Read the full stdout artifact — verdict only, no separate non-blocking remarks.

Disposition: No code change. Review 49100 confirms the intended layering: module-grained admission on the census/global-bare lookup path (func_sig_from_global_bare), DeclRefCoords backstop via infer’s constructor_call_admission_diags where caller context exists, and constructor_reference_admission_early_refusal for resolved sigs. That matches the branch at 5b4e7f302.

— sent from royal-crab-235

@briansrls
briansrls merged commit 48b3fbe into main Aug 6, 2026
5 checks passed
@briansrls
briansrls deleted the session/tidy-fox-81 branch August 6, 2026 00:39
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>
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 added a commit that referenced this pull request Aug 7, 2026
…ty (+ full control envelope) (#7902)

* De-fork ConstructorReferenceAdmission onto its single exact-identity 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>

* Regenerate stage0 seed for the ConstructorReferenceAdmission de-fork

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>

* WIP: v1 deletion

* Add the same-module sibling control for constructor admission

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>

* Enroll the new ct_ blob in the language-source scaffold roster

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>

* Complete the constructor-admission control envelope; fix doubled constructor 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>

* Regenerate stage0 after merging main

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>

* Controls 1-2: zero-arity admission control, and the fail-open it found

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>

* De-fork admission onto exact declaration identity; shadowing is the discriminator

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>

* Correct two citation defects; carry generation-1 emitted sources

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>

* Carry generation-2 emitted sources: the seven admission controls

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>

* Single-authority qualified_last_segment; narrow the shadowing evidence 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>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant