Skip to content

Unify fn and func on a single fn item form - #10850

Merged
gunbai-bot[bot] merged 44 commits into
mainfrom
session/cool-ibex-701
Sep 13, 2026
Merged

gunbai-bot[bot] merged 44 commits into
mainfrom
session/cool-ibex-701

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 8, 2026 •

Copy link
Copy Markdown
Contributor

What

.dag carried two item forms for one concept: fn (type parameters, no uses) and func (a uses row, no type parameters). That is a §3 fork — one concept, two names, differing only in which fields each could carry. This unifies on the single fn form by flipping has_uses: false -> true on its grammar row and deleting the func ItemForm and keyword, and rewrites every func declaration in the corpus to fn.

Evidence the fork was live: while this PR was open, main delivered four new func declarations, three at once carrying uses rows. Authors were selecting a spelling by which grammar fields it permitted, not by semantic kind.

Landed as one squash-merge so main never carries dual authority. The bootstrap constraint was measured, not assumed — the committed mirror IS the parser that reads .dag, so the mirror boot recipe (grammar row patch + parser delta replay, then the regen phase adjudicates) is what makes a one-round cut possible.

The semantic repair, and why it is the risky part

parse_fn_body_from_prefix built its node with a hardcoded uses: [] while the func path bound prefix.uses. Unifying without this fix would have SILENTLY DISCARDED every effect row: a dropped row still parses, and the stage0 mirrors project only compiler modules, which declare no uses — so both cheap oracles are structurally blind to it.

Its evidence is test.claim.generic_effectful_declaration_wall_witness_test, whose positive control returns net.id so the resource must be BOUND, and whose mutation bar is executed rather than asserted: restoring uses: [] on the success node reddens exactly that arm while the other two stay green. The recovery node is NOT covered (it carries body: none, so nothing can reference the resource) and the file says so.

The new refusal

Unifying makes <T> + uses newly grammatical, and no emitter plumbs type parameters through the effectful path. A typed located refusal sits at the single ingress where both facts are in scope. Moving it to the emission boundary is correct layering that would LOWER the rung today, because gunbc.rung_drop.emit_stage_blocking is standing and file_emission_target_is_modeled answers Rust=>true with Python, Go and Dag all false.

How this became landable

This PR was the specimen of gunbc.recurring_failure_mode.base_readability_gate_refuses_a_grammar_change: the wave-admission phase parsed base-revision declarations with the head parser, so a grammar change was refused NotEvaluated. The prerequisite (#10970, landed as ab898ba3edf) loads the base revision's own ParseEnvironment and reads the base under it when the environments differ. This PR is recut on that main and the required floor now reads, on this exact head:

namespace-wave-admission: the base and head parse environments differ (dag/extdeps/languages/dag/syntax.dag), so the baseline is read in full under the base's own grammar rather than reconstructed from untouched head records
namespace-wave-admission base=ab898ba3edf… head=981a15717c3… modules_compared=5666 modules_added=1 … deltas=0
namespace-wave-admission ADMITTED
required-floor: verdict=FloorClean

The failure-mode row stays enrolled as regression evidence per §4b(4).

Deliberately OUT of this PR (independent follow-ups): collapsing FuncItem into FnItem in the node model, and repairing uses rows that were authored against the old form.

Test plan

  • test.claim.generic_effectful_declaration_wall_witness_test — 3 arms, enrolled; mutation bar executed against v1_compiler_parse.rs.
  • Required lanes on this head: required-witnesses-build, required-witnesses-floor, heal-generated-artifacts, witnesses all SUCCESS; floor FloorClean, wave ADMITTED.
  • Corpus residual: zero .dag item declarations spell func.

🤖 Generated with Claude Code

https://claude.ai/code/session_01XjkfJ59JXcYnbtgTCH2Utn

gunbc-ci-auto-heal and others added 6 commits September 8, 2026 17:19
…p round 1 of 2)

Round 1 of the `func` keyword cut. It makes a compiler that accepts BOTH
spellings so that round 2 -- which rewrites the corpus and deletes `func` --
has something able to parse its own output. The seed's committed mirror is the
parser that reads .dag, so a single-commit cut is unbuildable: the old mirror
cannot parse `fn ... uses`, and it is the thing that would have to generate the
new mirror. Measured: 64 files refuse with "expected '=' or '{' after fn return
type", cascading to 3980 orphaned annotations.

Three edits, and the second is the load-bearing one:

- `fn`'s ItemForm row gains `has_uses: true`. This is the ONLY field that had to
  change. `fn` and `func` differ on four (type params, return_required, body
  kind, uses) and are incomparable in both directions, but the corpus decides
  each: 746 `fn` declarations carry type params and 0 `func` do; all 451 `func`
  declarations already carry a return type; and `fn`'s ExprBody accepts both
  `= expr` and `{ }`, strictly subsuming func's BlockBody.

- `parse_fn_body_from_prefix` threads `prefix.uses` into both its recovery and
  success nodes. It hardcoded `uses: []` while `parse_block_body_from_prefix`
  (today's `func` path) binds the row. Flipping has_uses WITHOUT this would have
  parsed every effect row and silently discarded it -- every effectful function
  reclassified FnItem and emitted pure, with a green compile. That is a silent
  wrong answer (DESIGN.md section 5), not a missing feature.

- The unified row makes `fn f<T>(..) uses net: Network` newly grammatical, and no
  emitter plumbs type parameters through the effectful path -- Rust, Python and
  Go each construct the resource-aware body directly. The refusal goes at
  `parse_fn_body_from_prefix`, the single ingress where both facts are in scope,
  so one typed located diagnostic covers all three targets. The pre-existing
  Rust `compile_error!` is a target-specific failure that would let `gunbc
  compile` claim success over an artifact designed to fail its target compiler.

`func` and its keyword are RETAINED here and deleted in round 2. The dual
authority exists only between two commits of one squash-merged PR, so main never
carries it.

Receipt: the .dag parse sweep over src/v1, dag and src/v2 reports 5232 file(s)
parse-clean on this commit, run against the UNCHANGED mirror -- i.e. the old
seed can compile round 1.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
The two mirrors CI named as drifted, regenerated from the round-1 .dag
authority: extdeps_languages_dag_syntax.rs and v1_compiler_parse.rs. Nothing
hand-edited -- these are the emitter's output, carried back from a remote
`claim_executor --required-regen` (planned=155 executed=155 adjudicated=155).

This is what makes round 1 a usable bootstrap step rather than a declaration:
the mirror IS the parser that reads .dag, so until it carries `has_uses: true`
and the threaded `prefix.uses`, no seed exists that can parse round 2's corpus.

Two notes for anyone reproducing this:

- A remote regen cannot install. `ctrl-build --remote` reconstructs the worktree
  without .git and uploads no artifacts, so the candidate tree stays on the
  runner. The drift here is 2 files / 2771 bytes, small enough to carry back as
  a patch through stdout; a large drift would need a different route.
- Regen panics on a BuildBuddy runner with `HostBudgetUnreadable` because no
  cgroup memory.high/memory.max binds the process. GUNBC_* is deliberately NOT
  forwarded by ctrl-build (those name host-sized values), so the budget must be
  set ON the runner from its own MemTotal rather than by defeating the allowlist.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
…effect fact (round 2 of 2)

`fn` and `func` were never a semantic distinction. `func`'s ENTIRE effect was
setting ItemForm.has_uses -- permission to parse a `uses` clause -- and the
keyword was then discarded: `item_kind` derives FuncItem from
`item.uses |> count > 0` and never consults the spelling. So a source-spelled
`func` with no `uses` was already reconstructed as an FnItem, and that was the
majority case: of 451 `func` declarations, 275 carried no `uses` row.

Round 1 made a compiler accepting both spellings. This round removes the
redundant one:

- 451 declaration heads rewritten `func` -> `fn`, plus 7 .dag programs embedded
  in STRING LITERALS (4 in data_reference_ambiguous_refusal_witness_test, 2 in
  workflow_default_field_projection_fold_witness_test, 1 in cli_run.rs). Deleting
  a keyword censes files parsed as .dag modules; it cannot cense a .dag program
  stored inside a string, so those needed finding by hand.
- The `func` ItemForm row and its `dag_keyword_set` entry are deleted. The
  deletion IS the census: `find_item_form` returns Absent and `parse_item`
  refuses, so any missed site fails loudly rather than silently.
- `func` removed from heads-only item-start recognition and the parser's
  refusal text.
- The dead grammar mirror deleted after an exact call census: parse_func_def
  (0 callers), parse_fn_def (0), parse_fn_after_kw (1, inside parse_fn_def, so
  dead transitively) and parse_block_item_after_kw (0). The live route is
  table-driven through parse_item_by_form, so these were a second, stale copy of
  a grammar the ItemForm table owns -- exactly the §3 fork the cut exists to end.
- bare_name_fork_lens renders FuncItem as "fn". After this round it would
  otherwise report a source declaration written `fn ... uses` as the now
  unwritable spelling `func`, preserving deleted syntax as a false observation.

NOT in this change, deliberately: FuncItem's deletion (the internal variant
survives, still derived from `uses`), the 275 candidate missing-`uses` rows, and
the pre-existing zero-argument inference loss. Three independent propositions.

Go, Swift and Wasm keep their own `func` -- that is their grammar, not ours.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
# Conflicts:
#	dag/gunbc/instruments/docs_projection_gate.dag
#	dag/gunbc/runner/runner_microvm_host_ready.dag
#	dag/gunbc/tools/bmc_onboard.dag
#	src/v1/stage0/src/v1_compiler_parse.rs
Emitter output for the round-2 authority, carried back from a remote
`--required-regen`. The mirror now carries the cut: no `func` ItemForm row, no
`func` in dag_keyword_set, and none of the four dead grammar-mirror functions
(parse_func_def, parse_fn_def, parse_fn_after_kw, parse_block_item_after_kw).

Receipt on the merged tree: the .dag parse sweep reports SWEEP_ERRORS=0. Before
the cut the same sweep refused 64 files with "expected '=' or '{' after fn
return type" and cascaded 3980 "source annotation names no subject" -- so that
second class was orphan damage from the first, not an independent defect, which
the pre-cut census could not distinguish.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
… gate class

Two DESIGN obligations the cut incurred and had not discharged.

1. ENROLLED EVIDENCE (section 4b(4)). The wall's positive and negative controls
   had only ever run as throwaway fixtures inside a remote dispatch, deleted in
   the same script -- they proved the wall fired once, on a machine that no
   longer exists, which establishes nothing about any later revision. They are
   now a committed witness with both arms passing.

   The refusal arm names the ParseError CLASS rather than asserting a bare
   false, per dag/test/retirement/model.dag: "A generic
   compile_dag_rust_emit_check false is explicitly insufficient: it cannot
   separate the expected refusal from a malformed fixture or an unrelated
   earlier failure."

   COVERAGE BOUND, written into the witness rather than left to be inferred
   from a green: these arms cover the WALL, not the sibling `prefix.uses`
   threading in the same change. That repair is invisible to both cheap
   oracles, measured: a discarded effect row still PARSES (sweep reports 0
   errors with the row dropped), and regen drift cannot see it either because
   the stage0 mirrors project only the compiler's own modules, which declare no
   `uses` -- the subject is outside that oracle's population entirely. Its
   executing evidence today is the floor (3550 claims, claims_failed=0). The
   next-rung trigger is recorded with the four measured obstacles that defeated
   the emit-level assertion, so it is not rediscovered from scratch.

2. A NEW FAILURE-MODE ROW. namespace-wave-admission reads the BASE revision
   with the HEAD compiler, so deleting a keyword makes all 140+ changed files
   unreadable at base -> NotEvaluated -> BLOCKING, while every other required
   signal is green.

   Filed as its own row rather than folded into
   fail_closed_gate_refuses_its_own_repair, whose recognition rule is a
   DEFECTIVE base that the head repairs. Here the base is HEALTHY under its own
   grammar and unreadable only under the head's; merging them would state
   "restores base health" as the rule and send a reader looking for a defect on
   main that does not exist.

   The finding beyond this PR: the gate's precondition that base and head share
   a language is unstated, so it surfaces as a red rather than as something
   readable in the gate; it is self-clearing only by landing, so holding cannot
   resolve it; and the repair that would satisfy it is the transitional alias
   section 3 delete-first forbids. A gate should not settle a language-design
   question by attrition. Ceiling: read the base with the base revision's own
   compiler.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
@gunbai-bot

gunbai-bot Bot commented Sep 8, 2026

Copy link
Copy Markdown
Contributor Author

CI state at daf0c07, since the red is expected and its only in-scope "fix" would defeat the change.

One blocking cause, unchanged across three runs:

namespace-wave-admission NotEvaluated — dag/extdeps/access/posix_effective_principal_read_op.dag
does not parse at the base revision (5 diagnostic(s)), so its base-side declarations cannot be read

The phase compares base-side and head-side declarations and parses the base revision with the head compiler. This PR deletes the func keyword, so all 140+ changed .dag files are unreadable at base. The 5 diagnostics are one refused declaration plus its orphaned annotations, and the same shape holds for every changed file. The base is not defective — main parses clean under main's own compiler; it is unreadable only under the head grammar.

Filed as its own class in this PR: gunbc.recurring_failure_mode.base_readability_gate_refuses_a_grammar_change, kept separate from fail_closed_gate_refuses_its_own_repair because that row's recognition rule is a defective base the head repairs, which is false here. It is self-clearing only by landing: once merged, every later PR has a post-cut base and the phase evaluates normally.

Not being "fixed" deliberately. The only edit that turns this phase green is keeping func as a transitional parse-only alias — the staged migration DESIGN §3 delete-first forbids and that the approving ruling rejected ("an alias plus deprecation diagnostic would preserve a second authority without buying a migration window"). Escalated to the operator instead; a gate should not settle a language-design question by attrition.

Every other required signal is green:

signal result
required-witnesses-build PASS
floor planned=3552 executed=3552 terminal=3552 passed=3483 claims_failed=0
.dag parse sweep (merged tree) 0 errors — was 64 refusals + 3980 orphaned annotations pre-cut
regen first_generation_equal=true
enrolled wall witness both arms pass in the required floor (planned 3550→3552, passed 3481→3483)

Known gaps, stated rather than implied: the identity-keyed before/after over the 451 rewritten declarations is not built; and the prefix.uses threading has no enrolled discriminating control — a discarded effect row still parses (sweep 0 errors with the row dropped) and regen drift cannot see it either, since stage0 mirrors project only the compiler's own modules, which declare no uses. Both are recorded in the witness with next-rung triggers.

A residual-func check is needed immediately before merge: main delivered new func declarations mid-flight once already (14, in the merge from main).

gunbc-ci-auto-heal and others added 8 commits September 8, 2026 23:39
…eaves

The phase compared base-side and head-side declarations by parsing BOTH with
the HEAD compiler. That precondition -- base and head share one grammar -- is
unstated, and this change breaks it: removing the `func` keyword makes every
file in its own diff unreadable at base, so the phase refused in proportion to
how thoroughly the change succeeded. It reported NotEvaluated, BLOCKING, with
every other required signal green.

Both repairs available inside the gate are worse than deleting it. Softening
the refusal to an empty base side is the empty-observation narrow that review
56449 already rejected on this exact function. Keeping `func` as a parse-only
transitional alias satisfies the gate and is the staged migration DESIGN §3
delete-first forbids -- a gate should not settle a language-design question by
attrition. Operator ruling: delete the behavior.

What goes with it is declared rather than absorbed. §4b(3) permits lowering a
rung only with previous rung, temporary rung, reason, bounded population and a
restoration trigger naming the CAPABILITY, so the drop is filed as a typed row,
gunbc.rung_drop.namespace_wave_admission_deleted: previously mechanically
preventable, now mitigatable, DeletedWithoutReplacement, population = the
subject-membership, closure and occurrence-binding deltas -- the third of which
has no remaining mechanism at all, because both sides resolve and nothing else
compares them. The trigger is the capability of reading a revision's
declarations under THAT revision's own grammar; a rebuilt gate without it
re-earns the identical refusal on the next grammar edit.

StageF0 is left OUTSTANDING with its reason rather than silently cleared, the
class stands in gunbc.recurring_failure_mode (its specimen is gone, the class is
not), and `git_stdout` is rehomed into behavioral_receipt_host rather than
deleted with its caller.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
# Conflicts:
#	dag/gunbc/namespace/namespace_wave_admission.dag
#	dag/gunbc/stage0/stage0_crate_layout_generated.dag
#	src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs
#	src/v1/stage0/src/gunbc_stage0_crate_layout_generated.rs
#	src/v1/stage0/src/namespace_wave_admission.rs
…the merge-resolved projections

The generated-artifact merge driver refused three crate-layout projections as
GeneratedArtifactConcurrentDivergence and left the ours side in the worktree
with no markers. Taking ours to unblock the merge dropped exactly what that
refusal predicts: main added `bootstrap_seed_retention_frontier_generated.rs`
to the emitted-file roster in the same window this branch removed
`namespace_wave_admission.rs` from it, so neither side's bytes are the
projection of the merged authorities. The union is restored here and the claim
is not that these bytes are hand-derived -- regen is the oracle and refused on
exactly this line (`emit missing generated file
bootstrap_seed_retention_frontier_generated.rs`), which is how the drop was
found rather than shipped.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
`head_index` existed only to hand the parse phase's declaration index to the
wave-admission phase without acquiring the corpus a second time. With that
phase gone the binding is written and never read, which rustc reports as two
errors under the `-D warnings` the required build lane runs -- so both required
jobs failed to build the instrument and refused with
`standing=measurement_unreached cause=instrument could not be built`.

A plain `cargo build` does not deny warnings, which is why the local check went
green over it. Verified with the command CI actually runs, read by its own exit
code rather than by a grep pattern over its output: `cargo clippy --all-targets
-- -D warnings`, CLIPPY_EXIT=0.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
Ledger-Repair-Judged: docs/design-rung-drops.md
Ledger-Rows-Repaired: docs/design-rung-drops.md namespace_wave_admission_deleted
…wall

The rostered-row-join phase refused with RosterMemberUnresolved on
`namespace_wave_admission_occurrence_grain_stall` and
`namespace_wave_admission_board_grain_stall`: both were declared inside the
module this branch deleted, and the roster still imported them. That is the
fail-closed census working -- the deletion is what made the dependents refuse
loudly.

They are deleted rather than rehomed. A §4b(2) stall says a class sits below its
ceiling and names what blocks the climb; with the wall gone there is no
mechanism to climb, so keeping the rows would report a stalled guarantee where
there is now no guarantee at all. The loss is not absorbed by their removal --
it is declared at gunbc.rung_drop.namespace_wave_admission_deleted, whose
population carries the occurrence-binding delta these rows were about and whose
restoration trigger names the same capability.

The roster's "five rows arrived late" annotation is corrected to three, since it
asserts a present fact. The identical sentence in
roster_re_enumerates_its_own_rows_stall is left alone: it recounts what that
join refused on its first execution, and a past event stays true.

Floor otherwise green on the prior head: planned=3551 executed=3551
claims_failed=0, with these two the only blockers.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
# Conflicts:
#	docs/design-rung-drops.md
#	src/v1/stage0/src/namespace_wave_admission.rs
# Conflicts:
#	dag/gunbc/repo/repo_ruleset.dag
@gunbai-bot

gunbai-bot Bot commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

Merge of fe83b41f48a (#10814, world_converge deleted at the root) delivered a new func declaration onto main after this branch cut the keyword — gunbc.repo.repo_ruleset verify. That is the mid-flight delivery this change has to expect: every branch authored against pre-cut main can add one, and the conflict only surfaced it here because #10814 rewrote the same hunk. Resolved by taking main's side whole (the world_converge replacement) and respelling the one declaration.

The same merge is the occasion for a residual this branch had not swept: three hand-rolled item-keyword rosters in cli_run.rs still listed "func "/"pub func " — decl_head, ITEM_KEYWORDS, FACT_CARDINALITY_ITEM_KEYWORDS (two of them fixed-arity [&str; 8], now 7). A census that counts a spelling the compiler refuses is a divergence between what the corpus says a declaration is and what the parser accepts, so the entries are removed rather than left inert. They rode in on the merge commit f639ee9f439 rather than a commit of their own; recording them here so the diff is not the only place they appear.

Verified with the command CI runs, read by its exit code: cargo clippy --all-targets -- -D warnings, CLIPPY_EXIT=0.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

HOLD at exact head f639ee9f439329a5dcf29ce558a0378561c13b36.

The core fn/func cut is directionally right: the modeled fn row now admits uses, parse_fn_body_from_prefix carries prefix.uses, the redundant item-form and dead parser mirrors are removed, the corpus spelling is rewritten, and the live source-facing projection no longer reports FuncItem as authored func.

There are three blocking issues:

  1. Restore namespace-wave-admission; do not pay for this grammar cut by deleting a required guarantee. This branch removes the required phase from required_ci_phase_roster, deletes its execution from claim_executor, deletes its implementation/tests and two guarantee-stall rows, and records a permanent rung drop because the HEAD parser cannot read base-side func declarations. That is a defect in cross-revision acquisition, not authorization to remove the adjudicator. Revert 039990d9f51a86bc72e444305df93e1620d9013e and the dependent cleanup/rung-drop work. Preserve NotEvaluated as refusing and preserve the deletion of the func alias. The repair is to obtain the base declaration index under the base revision's own grammar/compiler and feed a stable projection to the head adjudicator; land that as a prerequisite if it cannot remain single-subject here.

  2. The new positive witness does not witness the load-bearing prefix.uses repair. gew_plain_effectful declares uses net: GewNet2, but its body only returns x, and the assertion checks only that ParseError count is zero. Restoring the old uses: [] hardcode would still make this test green. Make the positive fixture consume the binding—for example return net.id—and assert zero total blocking diagnostics (or the exact emitted resource binding), so deleting the threading produces a RED. Also add a constructed legacy func declaration that must produce the parser refusal; the current pair tests generic+effects, not deletion of the old spelling.

  3. The generic-plus-uses wall is at the wrong semantic boundary as currently justified. parse_fn_body_from_prefix rejects the construct because the Rust/Python/Go effectful emitters do not plumb type parameters. That makes an emitter limitation part of the source grammar and also blocks interpreter/Dag paths before target selection. Keep the parser's one callable grammar and carry both facts; refuse at artifact/target emission before publishing success, unless this PR can establish that the language/interpreter itself cannot represent the combination independently of those three emitters.

The PR is also still draft with the placeholder title/body and its exact-head workflow is still in progress. Please update the summary/test plan after the substantive repairs and bring back a terminal exact-head run.

gunbc-ci-auto-heal and others added 3 commits September 9, 2026 02:50
Ledger-Repair-Judged: docs/design-rung-drops.md
Ledger-Rows-Repaired: docs/design-rung-drops.md floor_cut_falsifier_cadence
Ledger-Rows-Repaired: docs/design-rung-drops.md source_root_ingest_gate
Ledger-Rows-Repaired: docs/design-rung-drops.md harness_seat_ceiling_by_operator_policy
Ledger-Rows-Repaired: docs/design-rung-drops.md serving_cost_axes_asserted_unmeasured
Ledger-Rows-Repaired: docs/design-rung-drops.md serving_offer_identity_is_the_exporter_process
Ledger-Rows-Repaired: docs/design-rung-drops.md witness_deferral_freeze_forward_rule
Ledger-Rows-Repaired: docs/design-rung-drops.md deleted_cadence_reference
Ledger-Rows-Repaired: docs/design-rung-drops.md transitional_admission_exception
Review 5149145309 is right that the positive control proved nothing about the
repair it sits beside: the fixture declared `uses net: GewNet2`, never mentioned
`net`, and asserted only that the ParseError count was zero -- so restoring the
exact defect this branch fixes (a hardcoded `uses: []` where the deleted `func`
path bound `prefix.uses`) would have passed it unchanged. A discarded effect row
still parses.

The control now returns `net.id`, so the declared resource must be BOUND for the
fixture to compile, and it counts EVERY blocking class rather than ParseError
alone -- an unbound `net` is not a parse failure, so the old scoping was blind to
precisely the mutation the arm exists to catch. Counting every blocking row is
exact only because these fixtures import nothing; that is stated in the file,
since a census carries the whole compile's closure. A third arm was added for
the removed spelling: the sweep proves no `func` declaration REMAINS, which is a
different claim from the grammar REFUSING one.

THE BAR WAS EXECUTED, NOT ARGUED, AND IT HOLDS FOR ONE NODE OF TWO. Mutating the
success node reddens exactly this arm while the other two stay green; mutating
the recovery node reddens nothing, because that node carries `body: none` so no
expression can reference the resource and no compile census can see the row.
Recorded as uncovered rather than averaged into a pair that passes.

AND THE FIRST MUTATION ROUND WAS RUN IN THE WRONG TREE AND PASSED, which is worth
more than the fix: `compile_dag_diagnostic_census` is a host fold, so the fixture
is compiled by the SEED BINARY and a mutation of src/v1/02_parse.dag leaves this
witness green until regen installs it. The review's fix alone, verified the way
it was proposed, would have produced a false receipt.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
@gunbai-bot

gunbai-bot Bot commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

Dispositions on review 5149145309. Two of three are acted on; one is declined with its reason, and finding 2 turned up something worth more than the fix.

Finding 2 — ACCEPTED, and the verification as proposed would have been false

You are right that the control proved nothing about the repair beside it. Fixed as you describe: the control returns net.id so the resource must be BOUND, and it counts every blocking class rather than ParseError alone — an unbound net is not a parse failure, so the old scoping was blind to exactly the mutation the arm exists to catch. The total is exact only because these fixtures import nothing, which is now stated in the file. Third arm added for the removed spelling: the sweep proves no func declaration REMAINS; that is a different claim from the grammar REFUSING one.

The mutation bar was executed, and it holds for one node of two.

success node   uses: prefix.uses -> uses: []   =>  THIS ARM FAILS, other two PASS
recovery node  uses: prefix.uses -> uses: []   =>  ALL THREE PASS -- NOT COVERED

The recovery node carries body: none, so no expression in it can reference the resource and no compile census can separate a threaded row from a dropped one there. Recorded as uncovered rather than folded into a pair that passes.

And the first mutation round was run in the wrong tree and PASSED. compile_dag_diagnostic_census is a host fold in cli_run, so the fixture is compiled by the SEED BINARY, not by src/v1/02_parse.dag under interpretation — a .dag mutation leaves this witness green until regen installs it. Verified the way it was proposed, your fix would have produced a false receipt. The mutation belongs in v1_compiler_parse.rs, and the file now says so.

Finding 3 — the layering argument is correct; executing it today LOWERS the rung

Agreed on the principle, and emit_func_def is indeed selected inside the Rust emitter by is_effectful, so this is a realization fact sitting in the interface. What stops the move is measured, not stylistic:

  • gunbc.rung_drop.emit_stage_blocking is a STANDING declared drop: a blocking emit-stage diagnostic can sit on main indefinitely with no required phase that fails. A parse phase reaches a parse refusal; nothing required reaches an emit one.
  • The refusal surface does not exist for two of the three targets the diagnostic names — file_emission_target_is_modeled answers Rust => true, with Python, Go and Dag all false.
  • The Rust-side mechanism at that seam, emit_rust_item_refusal, emits compile_error! INTO the artifact, deferring the refusal to rustc — the fabricated-plausible-output failure this witness file already argues against.

So the choice is a §3 layer inversion that refuses loudly, against correct layering that refuses where nothing gates and, for two targets, cannot refuse at all. That second arm is a §4b(3) rung drop, and I am not taking it silently to buy layering purity for a construct the corpus contains zero instances of. Stated honestly as a cost rather than a virtue: the wall does make a coherent construct unwritable, and I have NOT established whether the interpreter would execute it. The condition that moves the refusal is emit_stage_blocking's own restoration trigger.

Finding 1 — declined, and the ruling you are looking for is in the session, not the commit

The deletion is not scope drift. The operator instructed it directly: "i would delete that behavior", and when offered three scopings chose deleting the whole phase. I raised the objection you are raising BEFORE doing it, which is why the choice was put to them at all.

You are right that main still carries the module and that the standing direction says repair, not delete — that is exactly why it was escalated rather than decided. You are also right about the repair shape, and it is not discarded: it is the restoration trigger of gunbc.rung_drop.namespace_wave_admission_deleted, verbatim — base-side declaration reading bound to the compiler of the revision being read.

Reverting would reverse an explicit operator decision on a reviewer's request, which is not mine to do. If the ruling should be revisited — land the revision-relative acquisition first and rebase this PR onto it — that is the operator's call, and I have flagged it to them rather than deciding either way myself.

@gunbai-bot gunbai-bot Bot changed the title fn vs func Unify fn and func on a single fn item form; delete the wave-admission phase the cut refused Sep 9, 2026
gunbc-ci-auto-heal and others added 7 commits September 9, 2026 03:27
# Conflicts:
#	dag/gunbc/namespace/namespace_wave_admission.dag
#	src/v1/stage0/src/namespace_wave_admission.rs
#	src/v1/stage0/tests/namespace_wave_admission.rs
# Conflicts:
#	dag/gunbc/namespace/namespace_wave_admission.dag
#	src/v1/stage0/src/namespace_wave_admission.rs
#	src/v1/stage0/tests/namespace_wave_admission.rs
`dag/gunbc/superseded_run_starvation_census.dag:696`, from #10742
(9b33fd6), was authored against pre-cut main and refused the parse phase
with `expected item declaration`. It carries no `uses` row, so the migration is
the keyword and nothing else.

This is the SECOND such delivery on this branch -- #10814 supplied the first,
in gunbc.repo.repo_ruleset -- and the two arrived by different routes: that one
surfaced as a merge conflict because it rewrote a hunk this branch had touched,
while this one merged cleanly and was caught only by the required parse sweep.
The sweep is what makes the class fail-closed rather than silent, and it is the
reason the corpus residual is checked immediately before merge rather than once
at the start: every branch authored against pre-cut main can add one, and the
window closes only when this lands.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YZZi3QsDvibJqy8k8PwzZ9
Ledger-Repair-Judged: docs/design-rung-drops.md
Ledger-Rows-Repaired: docs/design-rung-drops.md spark_serving_local_artifact_not_reproducible
Ledger-Rows-Repaired: docs/design-rung-drops.md spark_serving_fleet_global_configuration
# Conflicts:
#	.gitattributes
#	docs/design-rung-drops.md
#	src/v1/stage0/src/namespace_wave_admission.rs
Ledger-Repair-Judged: docs/design-rung-drops.md

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

HOLD at exact head e9dc3ebdbb3fa1f7114572e9570045dc0ba9eb67. Current ruling: REVERT the whole-phase deletion and land revision-relative acquisition first.

This supersedes the earlier instruction to “delete that behavior” to the extent it was implemented as deleting the entire namespace-wave-admission capability. Delete the defective behavior—reading BASE source with the HEAD grammar—not the independent required wall.

The core A work is approved. Main’s continuing delivery of production func … uses declarations strengthens the case that this is one concept with two field-gated spellings. The revised witness also resolves review finding 2: the positive arm now consumes net.id, counts all blocking diagnostics, has an executed mutation bar on the seed parser, and separately proves the removed func spelling refuses. I also withdraw finding 3 as a blocker for A: the generic-plus-uses parse wall preserves the pre-cut accepted-program set and is an honest temporary safety wall while emit-stage blocking remains below the required path. It must not be read as terminal semantics, but this PR need not build generic effectful emission.

The contested deletion is different. §3’s delete-first root is the obsolete func declaration form. namespace-wave-admission is not a second spelling or realization of that fact; it asks an independent safety question about subject-membership and binding motion. Its refusal is the deletion census working: it exposed one load-bearing assumption in a consumer. The next sentence of the doctrine says to fix surfaced dependents forward from first principles, and the atomicity clause is explicit that minimum Y must preserve every required refusal. A required merge wall is a gap-intolerant boundary. The fact that staging/freeze preserves its refusal is why that carve-out applies, not why it does not.

The declared §4b(3) drop makes the deletion honest rather than silent. That is good bookkeeping, and my earlier phrasing that the implementation simply contradicted the docs was too categorical. But permission to record a bounded safety regression is not evidence that deleting the capability is the preferred fix, nor does §3 make the gate obsolete. Recent #10871/#10889 arm churn does not change the question the wall answers or the four-member population this branch itself says becomes unguarded.

Required sequence:

  1. Revert 039990d9f51a86bc72e444305df93e1620d9013e and the dependent phase-removal cleanup: restore the required roster member, execution path, implementation, tests, milestones, and the two guarantee-stall rows; remove namespace_wave_admission_deleted once its restoration trigger is satisfied.
  2. Land a prerequisite that reads each revision with that revision’s own compiler and projects both sides into one stable declaration-index interchange shape: BASE source → BASE compiler → projection; HEAD source → HEAD compiler → the same projection; HEAD adjudicator compares them. Preserve NotEvaluated as refusing. Do not restore a func alias.
  3. Rebase the syntax cut onto that prerequisite. Its exact-head required run must show namespace-wave-admission Adjudicated, not absent and not NotEvaluated, followed by the residual func census and fixed-point receipts.

The newly filed base_readability_gate_refuses_a_grammar_change class is a valid finding; carry it with the prerequisite repair rather than using removal of its sole live specimen as the resolution.

Maintenance merges and respellings while waiting were appropriate and are not being read as work past the unresolved decision. The decision is now closed: preserve the wall; repair acquisition first; then land the one-spelling cut.

@gunbai-bot gunbai-bot Bot changed the title Unify fn and func on a single fn item form (BLOCKED on revision-relative base acquisition) Unify fn and func on a single fn item form Sep 13, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review September 13, 2026 14:36
@briansrls
briansrls dismissed stale reviews from themself September 13, 2026 14:40

Superseded by the exact-head LAND review on 3a05b6f. The phase was restored, revision-relative base acquisition landed as #10970, the discriminating uses witness and legacy-spelling refusal are enrolled, and the exact-head required run is green with namespace-wave-admission ADMITTED.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LAND @ 3a05b6fb4acab00cac18af6e1e60730bb32a4aaa.

The three earlier holds are satisfied and have been dismissed: namespace-wave-admission is restored; revision-relative base acquisition landed first as #10970 / ab898ba3edf16076654f9bfd6b7712fda3e28a70; the prefix.uses repair has an executed discriminating mutation bar; the removed func spelling refuses; and the exact-head required run is terminal SUCCESS across required-witnesses-build, required-witnesses-floor, heal-generated-artifacts, and witnesses. The floor reaches the differing-environment full-base route, reports namespace-wave-admission ADMITTED, and terminates FloorClean. The PR is ready and GitHub reports merge state CLEAN.

Scope remains the approved A cut: one fn item form with has_uses: true, deletion of the Dag func item form/keyword, corpus declaration-head rewrite, prefix.uses preservation, and the temporary typed generic-plus-effects refusal. FuncItem collapse and missing-uses repair remain separate follow-ups.

This authorizes enqueue only, with expectedHeadOid pinned to the full SHA above. It does not transfer to any new head and does not authorize a manual merge or native-review bypass. Because main has advanced since the pull-request run, the composed merge-group/queue run remains the final integration proof; any required-context red holds the landing.

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Sep 13, 2026
Merged via the queue into main with commit 5fe55d7 Sep 13, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/cool-ibex-701 branch September 13, 2026 15:29
gunbai-bot Bot pushed a commit that referenced this pull request Sep 13, 2026
Keep #11056 native-ancestry overlay; take main's unified fn item form.

Co-authored-by: Cursor <cursoragent@cursor.com>

# Conflicts:
#	dag/gunbc/seed_growth_admission.dag
gunbai-bot Bot pushed a commit that referenced this pull request Sep 13, 2026
main #10850 dropped the func keyword; this entry was the only added
func on the branch and would fail after a clean merge.

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls pushed a commit that referenced this pull request Sep 13, 2026
…rations

main 5fe55d7 landed gunbc#10850, which unifies fn and func on a single fn
item form corpus-wide: main carries zero `func` declarations. This branch carried
24, so the head was DIRTY rather than merely floor-red.

Resolution, mechanical: take this branch's side on the four conflicting files
(gcp_secret_access, secret_ref_credential, r2_permission_group_observe,
r2_token_mint_run), then func -> fn across every .dag file this branch touches.
NOTHING OF MAIN'S IS LOST: #10850 is the only main commit touching those four
files since 6e70be2, measured with git log 6e70be2..origin/main on that
path set. Prose references to `func` are left as main leaves them -- #10850
changed declaration syntax only, and a prose sweep belongs to that lane.

Verified before pushing: zero `^func` in dag/ and src/v2, zero unresolved paths,
cargo build -p v1-compiler --bin gunbc exit 0, and gunbc compile clean on
r2_token_mint_run, access_token_source and r2_mint_secret_access against the
merged tree.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015R9M9cY4iaqsqeaSDpT7g1
gunbai-bot Bot pushed a commit that referenced this pull request Sep 13, 2026
Review 65500, and it is right. The receipt said "THE TRIGGER THIS ROW SHOULD
CARRY" is a placement diagnostic that names the safe composition. That
REDEFINES the row's next-rung trigger DOWNWARD. The row already carries a
trigger at its STRUCTURALLY IMPOSSIBLE ceiling -- private material materialised
outside the public checkout, so auto-push cannot publish a tree it cannot see
-- and a diagnostic is rung 1: an operator-facing message can be ignored,
misread, or arrive after the copy, and it removes no constructor.

That is DESIGN 4b(3) grain, and the row's own text already forbids the move:
it rules that a brief instructing lanes to clone outside the worktree does not
discharge it. I quoted that neighbourhood and then proposed a better-worded
message as the trigger. The receipt now says so, because a ledger whose author
trips the class inside a receipt about that class is worth more than one that
reads as though the author only ever observed it.

KEPT, both measurements the review explicitly preserved:
  the compiler steer -- the panic names private_overlay/dag INSIDE the workspace
  and says nothing about where that layout is safe, while the safe recipe sits
  four lines below it in the same generated workflow;
  the worktree exclude result -- info/exclude is honoured only from
  --git-common-dir, never from --git-dir, so the obvious command writes to a
  file git does not read.

CHANGED: the diagnostic repair is now stated as mitigation ON THE WAY TO the
existing trigger, with "THIS ROW'S TRIGGER IS UNCHANGED" said outright so no
later reader mistakes this receipt for a narrowing.

Verified by execution on a matched-vintage binary: vintage control
(access_token_source.dag) EXIT 0 with ZERO parse refusals, and the edited row
compiles with 0 blocking errors. Main is merged in -- before it, the
post-#10850 binary refused this branch's pre-#10850 corpus, which is the same
instrument/subject vintage mismatch in the opposite direction.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UNzi2Ht3mXzngnKsdZnfH2
briansrls pushed a commit that referenced this pull request Sep 13, 2026
The merge from main brought #10850, which removed func as an item keyword;
the object store git realization, its wet witness and the exact-revision
reads still declared func items and no longer parsed.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Yb9agVcWYWzjhPsJ42XQAk
gunbai-bot Bot pushed a commit that referenced this pull request Sep 13, 2026
…5650)

The carrier defines the empty list as NEVER-LOOKED and a nonempty one as
RESEARCHED-AND-UNANSWERED. An empty list beside an obligation that narrates a
read is the meaning fork DESIGN section 3 names -- one name, two materially
different meanings -- and review 65650 states the consequence exactly: it hands
the WRONG REMEDY on ProviderRouteFactsIncomplete once earlier arms clear. It
sends a reader to go read a source for the first time when the published sources
are exhausted and the next step is asking the vendor. That is a fabricated
plausible output in section 5's sense: well-formed, typed, located, and wrong
about the world.

THE REVIEWS NAMED TWO SITES; THE MISMATCH IS ON FIVE. I audited every
construction against its own obligation rather than patching what was pointed
at, because fixing named instances of a class leaves the class:

  control_plane   []      -> six. "the documents read on 2026-09-12 ... say
                             nothing about where the service that administers
                             them runs".
  telemetry       2 of 6  -> six. Its obligation ENUMERATES all six by name.
  log_system      1 of 6  -> six. "no other document read on 2026-09-12 answers
                             it either" is a claim about the whole read set.
  spill           1 of 6  -> six. Same collective sentence.
  admin_access    1       -> 2. Its obligation reports consulting the locations
                             page and REJECTING it as answering a different
                             question. Consulted-and-did-not-answer is precisely
                             what this field records.

THE RULE, stated in the module so the next author does not have to infer it: a
path cites EXACTLY the documents its own obligation reports having read for it.
Nothing is cited because a document looks like it ought to have answered.

EXECUTED on a binary proven post-#10850 by a vintage control (0 parse refusals
on a file the older binary rejects). The runner refuses to map a Bool to an exit
code, so the verdict is read from the refusal text rather than from $?:
  the_same_route_admits_once_that_path_is_resolved                  true
  the_helsinki_route_refuses_on_durable_storage                     true
  one_unread_support_path_refuses_with_that_paths_obligation        true
  a_resolved_closure_with_an_unread_downstream_still_refuses        true
  every_hetzner_route_in_the_population_refuses                     true
  the_finland_subcontractor_the_route_cites_is_the_one_upstream_publishes  true
  a_resolving_reference_to_the_wrong_subcontractor_refuses          true
The first is the control: a refusal row is satisfied by ANY refusal reaching its
tag, so only the admit case can detect a posture that started refusing for a
different reason.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UNzi2Ht3mXzngnKsdZnfH2
gunbai-bot Bot pushed a commit that referenced this pull request Sep 14, 2026
… self-hosted runner

REFUSED at vivid-bee's thread on 4c23cca, one blocker, and it is real. The uploader
runs with always() over a shared /tmp glob; a self-hosted runner's /tmp survives across
attempts; an attempt that refuses EARLY writes no receipt of its own. So the uploader
could collect attempt N's orphan receipt and present it as attempt N+1's evidence -- and
an operator reads that receipt to decide WHICH LIVE CLOUDFLARE TOKEN TO REVOKE, so a
stale one names the wrong token.

That is this PR's own filed failure mode arriving from the other side: there a check was
correctly written and positioned after the irreversible effect; here an artifact is
correctly written and readable as belonging to a run that did not produce it. Both are a
receipt asserting what the execution does not establish.

THE DIRECTORY CARRIES THE ATTEMPT AND IS DECLARED ONCE. r2_mint_receipt_dir_root,
r2_mint_receipt_scope and r2_mint_receipt_dir_for live with r2_mint_receipt_path; the two
callers differ only in where the identity comes from -- the mint reads GITHUB_RUN_ID /
GITHUB_RUN_ATTEMPT on the runner, the emitter writes the workflow expressions -- and
neither spells a path. Same shape as the 66010 repair.

R2MintReceiptUnscoped is NAMED, not defaulted: a workflow run missing the identity writes
to the root, and because the uploader names an attempt directory that file is evidence for
NOTHING rather than evidence for the wrong attempt.

THE CONTROL THE REFUSAL ASKED FOR IS EXECUTED, not described: a stale receipt at the SAME
run id and the PREVIOUS attempt is a real receipt and lies outside this attempt's
directory (same-run-different-attempt is the sharp case -- a re-run is exactly when the old
file is still there); an unscoped receipt lies outside every attempt directory; and the
emitted glob pins the attempt while wildcarding only the bucket.

The emitted yaml CHANGED, 75775 -> 75839 bytes, which is the inverse of the 66010 check:
there byte-identity proved the derivation faithful, here a changed artifact proves the fix
reached the runner. Emitted path:
  /tmp/r2-mint-receipts/${{ github.run_id }}-${{ github.run_attempt }}/r2-*-object-write-mint-receipt.txt

Also restored `fn` on a new declaration I wrote as `func` out of habit; #10850 removed that
form hours ago.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015R9M9cY4iaqsqeaSDpT7g1
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