first(): construct the Optional std.algebra declares, migrate the field-access population, and declare the parameter coercion

[gunbai-bot]

Draft. One hold remains; the ordering hold is DISSOLVED.

1. Ordering (from the BT-N brief): PR BT-0: gunbc build gunbc — commanded exact build through the emitted CLI #9775 enrolls this exact divergence as a KNOWN-RED. DISSOLVED — confirmed by the BT-N lane: nothing in this PR waits on BT-0: gunbc build gunbc — commanded exact build through the emitted CLI #9775 or on BT-0 any longer. The title carried that hold longer than the fact did.
2. Grounding: the repair here is deliberately incomplete, and the census explains why (below). The builtin parameter-signature grounding is a genuine independent blocker and is being authored on session/still-swift-363-builtin-sigs.

Review corrections carried (review at head 4ed8c14f71)

• The bounded comparison population is 14, not nine. Ten are merge-admission sites — four in gunbc.merge_admission_produce and six in gunbc.merge_admission_subject, per Merge admission: eliminate the ten first() comparisons before the Optional repair turns them silently false #9912 — plus four elsewhere. An earlier draft said "nine merge-admission sites"; that number was carried, not counted.
• The Optional/Null wall was over-broad and is narrowed. It refused every constructed Optional against the host Null carrier, so Present { value: x } == none — whose correct answer is ordinary false — was unwritable, and the diagnostic called any constructed Optional a representation of absence, which is false for Present. Only Absent-vs-none is a straddle now. Five controls measured with claim_batch: Present == none is false and Present != none is true (both enrolled), Absent == none and Present == bare still refuse with their own messages (fixture-measured — a test fn returns Bool and a refusal aborts evaluation), Optional-vs-Optional unchanged.
• The optionality judgement selected rows by method spelling alone. The algebra is receiver-keyed and a spelling is not: 23 spellings are declared in more than one profile and three of them shape their returns differently (join, member, get). It now derives the profile from the receiver value's own carrier through kernel_algebra_profile and takes that profile's single row — the same fork resolution the get row needed.
• The judgement is now two-directional: a row declaring a concrete non-optional return refuses an Optional result. The naive symmetric rule was deliberately not implemented, because ReceiverSelf, ReceiverElement, ReceiverKey, ReceiverValue and AlgebraTypeVariable are all satisfiable by an Optional at runtime — implementing it blindly would have repeated the over-refusal above in a new place.
• Neither half has an authorable red, and that is measured: zero spellings in dag/std/algebra.dag declare mixed optionality across profiles, so no accepted program distinguishes the two selections. Discrimination is mutation-measured — with the join arm altered to return optional_present(..), ["a", "b"] |> join(",") refuses; unaltered it passes. The next-rung trigger is recorded in the witness.

The divergence

dag/std/algebra.dag declares first/last/get/lookup/map_get with return_type: OptionalOf { inner: ReceiverElement }. The Rust emit arm realizes that row as Option<T>. The interpreter arm answered the same question by hand and answered it differently — items.front().cloned().unwrap_or(Value::Null), the raw element. DESIGN §5 silent wrongness: it typechecks, returns a wrong answer, and warns nobody.

Executed, not reasoned (gunbc run, dag + src/v2 roots, unmodified seed):

probe	interpreted	declared
[] |> first	OUTER-ABSENT	OUTER-ABSENT	agrees
[Absent] |> first	OUTER-ABSENT	OUTER-PRESENT-INNER-ABSENT	diverges
[Present { value: "x" }] |> first	x	x	agrees (control)
(["x"] |> filter(n => true) |> first) == Present { value: "x" }	false	true	diverges
... == "x"	true	not well-typed	diverges

Enrolled as dag/test/claim/first_optional_construction_witness_test.dag: 7/7 green with this change, 4 red against the unmodified arm, three green positive controls. branded_list_first_optional_witness stays 8/8 green.

Census — docs/plans/first-optional-divergence-census.md

186 terminal |> first sites / 81 files on main, rostered at identity grain in three shapes (143 match-eliminated, 37 returned onward as T?, 6 value-position). The parent lane's 187/82 differs by one row not present on main. The roster, not the count, is the deliverable.

The census kept going past the pipeline spelling, and that is the finding: the METHOD form .first() is a separate population — 646 occurrences over 180 files — dominated by the value position (parse_int(s: fields.first()), trim(tokens.first()), percent(scalars.first())). Those work today only because the emitted arm inserts rust_call_arg_fail_closed_unwrap's .expect(..) while the interpreter needs no coercion at all, having never wrapped. The raw-element arm is the compensation the interpreter's MISSING argument coercion has been leaning on corpus-wide.

Measured: with only the first construction in place, bmc_capability_solve_witness_test's firmware_wire_version_is_parsed_before_track_matching — a witness that names nothing about optionals — flips PASS → FAIL (parse_int expects a string argument, got Variant).

What is repaired, and what blocks the rest

Repaired: the four arms construct their declared Optional (call-site decided, per map_lookup_as_optional's stated rule); eval_algebra_method_inner refuses when an arm's result does not inhabit the optionality all_algebra_field_templates() declares; .value on an absent Optional refuses instead of returning Value::Null; call_function_inner gains the optional-into-required-parameter coercion the emitter already had.

Blocked: a builtin call never reaches call_function_inner, and builtin_function_registry maps a builtin name to a RETURN TYPE only (04_sigs says so). Argument cardinality cannot be derived for a builtin. Deciding it from the argument's value shape is validation standing where construction was available, and is exactly the inference map_lookup_as_optional's doc comment refuses. So this lane stopped rather than shipping it.

The grounding this class waits on: builtin PARAMETER signatures, modelled beside the return type the registry already carries. That is model-before-implement work in std/ ahead of any further pipeline edit — a routing decision, not something to improvise inside this repair.

RETRACTED: the generated-doc drift was not deliberate, it was a defect of mine

This section previously argued that the DESIGN.md / docs/design-ledgers.md drift was
deliberate and must not be regenerated. That was wrong and I am retracting it, not editing it
quietly. I had carried drifted=2 for days as an inherent property of the branch. It was a
consequence of a defect I introduced, and it could not have been otherwise, because the regen
actuator itself was dying on that defect.

The control makes the attribution unambiguous. main run 33481211724, same phase, same
denominator: rostered=35 adjudicated=35 matches=35 drifted=0 unadjudicated=0. This branch, before
the repair: adjudicated=32 matches=30 drifted=2 unadjudicated=3. All five were mine.

The root, one root under all five. tools.generated_artifact_gate main_wet refused with
CallContractMismatch { callee: "outcome_accepted", ... } — this branch's own coercion arm, firing
on a call that is correct. v2.std.diagnostic outcome_accepted is fn outcome_accepted<T>(value: T) -> Outcome<T> with T free, so Optional<Node> is a legitimate instantiation and not a
cardinality escape. param_declares_required_value asked three questions of the declared type — is
it spelled Optional, does it carry CardOptional, is it the parameter's own name — and none of
them can see a free type variable.

Both arms were wrong, and the quiet one was the dangerous one. Absent was refused: loud and
false. Present was silently unwrapped into the callee, so a caller whose T = Optional<Int>
had the callee receive Int — the same silent semantic divergence this PR exists to remove,
reintroduced at a new seam by the removal itself. My first probe missed it because it matched on the
callee's return value and that match was lenient enough to accept a bare value against a Present
pattern; the probe that found it observes the arrival inside the callee and reported
UNWRAPPED - arrived as a bare value.

The fix reads the declaration, not the spelling. v1.compiler.parse parse_fn_body_from_prefix
builds a fn node's params as concat(type_params, value_params), and a type parameter is exactly
the entry whose declared type is its own name — the shape the positional-parameter filter beside it
already uses. Two discriminating REDs are enrolled in
test.claim.first_optional_construction_witness, each measured red on the defective head and green
now, beside the existing positive control; they stay enrolled rather than retiring with the climb
(§4b(4)).

Which path this was measured on. The interpreter path, and only that one.
gunbc.recurring_failure_mode mitigation_injected_where_judgment_declined was filed against the
Rust emitter for this same seam and this same callee, and its stated trigger is a producer that
can distinguish a free type variable from a declared non-optional formal. This PR builds that
producer on the interpreter side. §4b(1) measures source→interpretation and source→each emission
target independently and takes the minimum, so this does not retire or weaken that row: it
stands at the emitter's rung. I have not run the emitter path at this seam and claim nothing about
it.

Why this lane is red, and why that is the measurement

required-witnesses-floor refuses: unexpected_failures=427 verdict_incomplete=5 non_verdict_unenrolled=5. Measured against a trunk control — the same artifact on main at
b41d5648 reports 0 errored, 0 failed, 3065 passed — the entire population is caused by this
partial repair and none of it is inherited.

The 5 non_verdict_unenrolled are known-reds that now error instead of returning their known-red
verdict. v2.workflow.floor_non_verdict leaves one direction unconfined: nothing compares the
roster at HEAD against the roster at the merge base, so those 5 could be rostered in this same
change and both arms would pass. They are not being rostered. They are caused by this branch, so
enrolling them would use the wall's one unconfined direction to launder a regression past the wall
that exists to refuse it. The disposition is to finish the repair.

The 448 at identity grain, and which failures are load-bearing

Enumerated from required-floor-disposition (run 33362356177), not from the run log — the log's
failed= folds the distinction this table splits.

outcome	count
runtime-errored-before-verdict	442
failed (reached an assertion, answered false)	6
known-red-held	15
route-gap-before-verdict	47
passed	2638

The 442 are one population, not a spread. Every one is v2.test.* — 157 v2.test.claim, 132
v2.test.manual, 71 v2.test.emit, 52 v2.test.execution, and 28 across nine smaller segments.
Zero are dag/test/claim witnesses. That is the self-host coupling and not a corpus-wide
breakage: the v2 compiler is .dag interpreted by the v1 seed, so changing the interpreter's
optional projections changes v2's behaviour as it runs. The concentration is consistent with it —
45 in bash_command_fold, 24 in trait_derive_supplemental_generic_bound_contract, 19 in
symbol_index.containment, 18 in sg2_type_expression_projection.

Honest limit on this half: the disposition artifact carries identity / disposition / matched_prefix / outcome and no cause column, so the 442 are grouped by identity here, not by
error. Claiming they share one cause would need per-claim error text, which the log folds. What is
established is the population and its shape, not a single root for it.

All six assertion failures are load-bearing. None is incidental. Each was read at its assertion
rather than inferred from its name — which matters, because two of the names actively mislead:

claim	what it asserts	class
self_host_symbol_identity_binding_witness.w_next_rung_representations_have_no_realization_yet	rust_representation_realization_for(...) == none	Phase D — none-literal straddle
self_host_symbol_identity_binding_witness.w_symbol_ruling_names_a_realizable_representation	... != none and ... == none	Phase D — same
emit_host_shell_exec_run_equals_eval.shell_exec_run_eval_argv_is_bash_dash_s	argv().skip(n: 0).first() == "bash"	value-position first()
emit_host_shell_exec_run_equals_eval.emit_host_shell_exec_run_equals_eval_holds	composes the above	value-position first()
cargo_build_run_argv_witness.cargo_build_run_argv_holds	argv.skip(n: index).first() returned as a bare String	value-position first()
value_null_split_witness.raw_get_miss_differs_from_optional_absent	raw get miss ≠ optional_absent()	the enrolled discriminator

The two self_host_symbol_identity claims are named for symbol-identity binding and are nothing of
the kind here: they fail on == none against an Optional-returning function. none evaluates to
Value::Null while the repaired arm produces Optional::Absent, so the comparison is false. That is
Phase D's class — the ~218 == None sites over 66 files — surfacing in a witness whose title gives
no hint of it. Reading these two by name is what earlier led this lane to attribute them to #9741,
which a trunk control refuted.

So the six split 2 / 3 / 1 across the three gates the census already named: Phase D's none
migration, the value-position first() sites the emitter's rust_call_arg_fail_closed_unwrap has
been compensating for, and the discriminator that is red by design because Phase B landed. There
is no fourth cause among those six — the failures are the repair's own predicted surface.

RETRACTED, and by measurement rather than by scruple: an earlier draft of this paragraph ended
"which is the evidence that the census closed rather than merely counted." That claim is FALSIFIED.
Three unmigrated sites were found at head fa11d87da0e — roadmap_forecast.dag lines 329, 352 and
354 — in a file this very census covered, and confirmed by two independent routes. The census
counted; it did not close. No sentence in this body claims a closed population, and where a
population is stated it is stated against its base.

Two roster admissions were available and both were refused

Recorded because a reader cannot otherwise tell that a choice was made — in both cases the roster
was the cheaper arm, the mechanism would have accepted it, and the check would have gone green.

1. floor_non_verdict — the 5 non_verdict_unenrolled. Five known-reds error under this branch
instead of returning their known-red verdict, and that is what turns the lane red. That module
declares one direction unconfined: nothing compares the roster at HEAD against the roster at the
merge base, so those 5 could be enrolled in this same change and both arms would pass. They are
not enrolled. They are caused by this branch, so rostering them would use the wall's one unconfined
direction to launder a regression past the wall that exists to refuse it. The roster stays
Empty {}; the diff on that module is comments only. The disposition is to finish the repair.

2. nfr_roster_receipt — value_null_phase_eq. rust-unit-tests refused this branch with one
unrostered non-fold residue site, mine, added by the plan amendment: a match on a whose seven
arms each matched b with a _ => false wildcard over a closed coproduct. non_fold_residue_roster
would have taken the entry and greened the job. Instead the function is now derived from one
exhaustive value_null_phase_ordinal (no wildcard), following std.fermi fermi_ordinal. The
safety difference is the whole point: under the old form an eighth phase silently takes the _ arm
at seven sites and compiles clean; under the new one it makes the ordinal non-exhaustive and the
compiler refuses. Verified with the nfr_ suite at 14/14 including
red_control_wildcard_over_closed_coproduct_is_residue, so the detector still discriminates — the
site is gone rather than the check blunted. rust-unit-tests passes in CI at abee235.

A roster entry is a real mechanism and neither of these refusals says otherwise. But both sites were
decidable and had a construction available, and §4b puts construction over validation: below the
attainable ceiling is a correctness gap, not optional elegance.

Rung

Below the ladder (silent wrongness) → mechanically preventable once both halves land. Ceiling is structural impossibility, reached when interpreter arm bodies are projected from the same rows the emit arm reads (the §7 self-host frontier for v1_interpreter); the next-rung trigger names that capability.

🤖 Generated with Claude Code

https://claude.ai/code/session_01N8xvN1T1NKiJqCUqwEmDgK

---

Since the exact-head REQUEST_CHANGES at 4ed8c14f71

All three semantic-authority blockers are repaired, and the two record corrections stand in this body above.

1. The Optional-vs-Null wall is narrowed to the case that is actually a straddle. Only Absent against the host Null carrier reaches the migration refusal; a constructed Present against none answers ordinary false, because present-vs-none inequality is legitimate and calling every constructed Optional a representation of absence was false for Present. The narrowing is by variant (is_absent_variant), not by another spelling-based carve-out — which is the refusing mirror of the spared-case failure this lane's own ledger row names.

2. The optionality judgment runs in both directions. The local DeclaredOptionality is deleted and the authority is std.algebra algebra_result_optionality, a three-armed OptionalityRequired | OptionalityForbidden | OptionalityUnconstrained. OptionalityForbidden refuses an Optional result from a row declaring a non-Optional one, so the validator no longer admits in one direction by omission. The third arm exists because a receiver-relative return constrains neither direction, and it is witnessed rather than asserted.

3. The judgment is keyed by the receiver-selected row, not by method spelling. algebra_row_returns_optional(method) is gone. receiver_algebra_profile derives the profile from the receiver value and algebra_row_for_receiver(method, profile) selects the row, so the exact selected row is the authority. The discriminating fixture is a planted same-spelling fork whose two profiles declare opposite optionality, proving the receiver-selected row wins rather than a global same-name scan.

What this head adds beyond the blockers

The field-access population is migrated: every .first().<field> site in the corpus, 22 production across eight files plus the witness sites. Each production Absent arm is derived from the sibling refusal the site already sat beside — the count() == 0 arm — and where that guard became redundant it is dissolved rather than left standing beside the match. The one site with no sibling to derive from, product.pcb.copper nth_layer_function, returns Optional so its single caller answers with the LayerOutsideStackup refusal it already declares for the out-of-range case. Witness sites answer Absent => false.

The parameter coercion is declared, not commented: gunbc.rung_drop optional_into_declared_nonoptional_parameter. It claims no previous rung at its subject grain, because the emit arm carries the coercion on main in six places across five emitted files — this PR gave the second arm the same seam and thereby made a corpus-wide coercion visible at one site instead of invisible at two. Temporary rung is mitigatable: Absent refuses with a typed, located call-contract-mismatch; only Present is unwrapped. The trigger is named at capability grain — the compile seam refuses an Optional flowing into a parameter declared non-optional, at both arms, proven by a discriminating pair — and the row states explicitly that a site census does not retire it, because a census retires the corpus and never the coercion.

What is verified, and what is not

Verified by execution: 4487 file(s) parse-clean from the corpus walk, and dag/test/claim/commit_writer_heal_admission_real_execution_witness_test.dag resolves with no NoSuchField. The pre-migration head's floor red was exactly NoSuchField: no field 'oid' on type 'Optional', three LocalRepoWetTerminalVerdictNotExpected refusals in that file's local-repo-wet lane — the discriminating red this change is meant to clear.

Not verified here: the wet-lane verdict itself. claim_batch reaches those four witnesses only hermetically and refuses them as a route gap rather than a verdict, so a typecheck is not the floor verdict and this body does not claim it is. CI's floor lane is the arm that decides.

Every population in this body is stated against a base, because a census has a freshness window

A census reported as a structural property — "the population is closed", "N sites, all migrated" — is
a measurement with its base stripped off. It is the same defect as a green CI run cited for a tree
that no longer exists, aimed at a census instead of a build. On a repo merging every few minutes the
window between the base a census was taken at and the head it is cited on is never empty.

This is not hypothetical here, it is what happened. Two CrossRepresentationEquality floor refusals
appeared on this branch at a head whose census had already returned zero. The cause was not a missed
site: extdeps.languages.yaml.ingest yaml_lines_from_source compares raw.skip(n: n - 1).first()
against a bare "", and it landed on main in #9875 after my census ran. The census was correct
about its base and wrong about the head it was being read on.

So, stated at grain. At merge base 2b56084270d (merged into this branch at 76e41fa29cc),
these four shapes each return zero over dag + src/v2:

1. field access on the result — xs.first().<field>
2. an element-variant match — match xs.first() { <element constructor> => .. }
3. let bound then read — let e = xs.first() … e.<field>
4. comparison against a bare value — xs.first() == <non-optional>, excluding none, a
   Present { .. } literal, and another optional, all three of which are legitimate

A fifth shape was then found and migrated: the prefix-call form with a field read,
first(gaps).nodes, which none of the four greps could express because they all keyed on the method
spelling. That is the point:

Five shapes is a FLOOR on the shape count, not a total. Each of the five was invisible to every
grep that preceded it, and the fifth was found by asking what spelling the previous four assumed
rather than by extending them. The honest claim this PR makes is that five shapes return zero at
this merge base — not that the population is closed. The mechanical closure of the whole class is
the compile-seam refusal named in the optional_into_declared_nonoptional_parameter rung-drop row's
restoration trigger, and until that lands, a grep census is a floor with a timestamp.

[gunbai-bot]

The red floor is the measurement, not a defect to fix. Nothing will be pushed to make it green.

This PR is a held draft carrying a deliberately incomplete repair — the first/last/get/lookup Optional construction without the optional-into-required argument coercion that the emitted arm already has and the interpreter does not. The census in docs/plans/first-optional-divergence-census.md says in advance that landing one without the other converts a silent agreement into a silent disagreement across the method-spelling population (~650 sites). The floor is that prediction being measured.

Correcting my own earlier number. I previously reported this as flipping one witness. That was wrong in a way worth naming: I ran claim_batch against two witness files, one of ten witnesses flipped, and I reported a two-file sample as though it bounded the corpus. The measured figure from the required-witnesses-floor run is planned=3141 executed=3141 passed=2630 known_red_held=15 failed=442. Against a ~0 baseline that is ~440 claims turned red, two orders of magnitude larger than I said, and it strengthens rather than weakens the case for the sequencing: it is the blast radius of landing the construction alone.

A full enumeration of the 442 at identity grain is running, with the failing-line count computed on the runner rather than grepped from the streamed log, so a truncated stream cannot be mistaken for a short failing set. It will be posted here, split into the value-position argument sites the census predicted versus anything it did not — the second group being the part that matters.

Two holds remain, and they are different objects:

• Scheduling hold — BT-0: gunbc build gunbc — commanded exact build through the emitted CLI #9775 enrols this divergence as a known-red; the floor counts known_red_now_passing separately, so repairing before it merges breaks that lane's floor.
• Grounding hold — the completion needs a closed language-primitive denominator; see docs/plans/builtin-registry-population-partition.md.

Neither is the dissolution trigger. The trigger is semantic: when the interpreted and emitted realizations of first agree on the optional result shape. No PR number is load-bearing anywhere in this branch.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-01T05:52:18.454659Z	2201637	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 22016377f0

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Apply optional coercion to builtin calls before landing

This coercion only runs in call_function_inner, so required-argument builtins bypass it. After the new first arm wraps a nonempty result in Present, existing calls such as parse_int(s: fields.first()) in dag/extdeps/bmc/capability.dag pass a Variant directly to expect_str and fail with a type error; this breaks dag/test/claim/bmc/bmc_capability_solve_witness_test.dag and the required floor. The optional-to-required conversion must also be derived and applied by builtin dispatch before these method results are wrapped.

Useful? React with 👍 / 👎.

[briansrls]

REQUEST_CHANGES at exact head 4ed8c14f71c18e3b52b9da978efcd3c102e23534.

This remains a draft/incomplete repair, and the exact-head required floor is red. Three semantic-authority blockers must be repaired before this head can become a landing candidate.

1. The Optional-vs-Null equality wall is overbroad. optional_against_bare_straddle currently refuses every constructed Optional against Value::Null. That includes Present { value: "x" } == none, whose correct answer is ordinary false, not a cross-representation refusal; the existing value-null authority explicitly records that blanket Optional/Null refusal is invalid because present-vs-none inequality is legitimate. The current diagnostic also calls any constructed Optional a representation of absence, which is false for Present.

Required controls: Present("x") == none returns false; Present("x") != none returns true; Absent == none reaches the named migration refusal; Present("x") == "x" reaches the Optional-vs-bare refusal; Optional-vs-Optional equality is unchanged. Do not restore green with another spelling-based carve-out.

2. The optionality validator checks only one direction. Some(Ok(false)) => Ok(value) admits an Optional result for an algebra row declaring a non-Optional result. A function named and used as declared-optionality validation must enforce both directions. Add a discriminating control in which a selected non-Optional algebra row returns optional_present(...) and require refusal.

3. The validator is keyed at the wrong grain. algebra_row_returns_optional(method) flattens all_algebra_field_templates() and selects by method spelling alone. Algebra rows are receiver-profile-relative; the exact selected row/profile is the authority. A global same-name scan can either reject a valid selected row because another profile gives the same spelling a different shape, or validate against the wrong row. Thread the selected AlgebraFieldTemplate/profile from dispatch into the judgment, and add a same-spelling/opposite-optionality fixture proving the receiver-selected row wins.

Two record corrections are also required on the next head:

• The bounded comparison population is 14 = 10 merge-admission + 4 other, not nine merge-admission sites. #9912 established four sites in merge_admission_produce and six in merge_admission_subject.
• The title/body still carry the dissolved BT ordering hold. #9785 is no longer ordered behind #9775; its live hold is its own grounding/completion and red floor.

The builtin parameter-signature grounding remains a valid independent blocker. No roster admission is accepted as a substitute for completing these semantics.

[gunbai-bot]

All three semantic findings are repaired at df356789675, and the two record corrections are in the body. Thank you — the first one was right in a way I would not have found, because the case it names is one I decided by reasoning rather than by running.

1. The Optional/Null wall over-refused. Present { value: "x" } == none is ordinary false, and the arm refused it; the diagnostic even said out loud that any constructed Optional is a representation of absence, which is false for Present. Only Absent-vs-none is a straddle now. I ran all five named controls with claim_batch before touching the arm and again after, and I did not restore green with another spelling-based carve-out — the narrowing is on the variant, not on a name:

• Present("x") == none → false (enrolled, a_present_optional_against_none_is_ordinary_false)
• Present("x") != none → true (enrolled, a_present_optional_is_unequal_to_none)
• Absent == none → refuses, "a constructed Absent and the host Null carrier are two representations of ABSENCE" (fixture-measured)
• Present("x") == "x" → refuses, "an Optional<T> and a bare T are two representations of one value" (fixture-measured)
• Optional-vs-Optional → unchanged (an_optional_compared_against_an_optional_is_not_a_straddle)

The two refusals are fixture-measured rather than enrolled for the reason the file already states: a test fn returns Bool and a refusal aborts evaluation, so this harness cannot express "this expression refuses". That is the seam's standing next-rung trigger.

3, taken before 2, because 2 depends on it. algebra_row_returns_optional selected by method spelling over all_algebra_field_templates(). Measured: 23 spellings are declared in more than one profile, and three shape their returns differently — join is ReceiverSelf in two profiles and NamedTemplate { name: "String" } in the collection profile; member and get likewise. The judgement now derives the profile from the receiver value's own carrier through kernel_algebra_profile and takes that profile's single row.

2. Both directions, but not the naive symmetric rule. A row declaring a concrete non-optional return now refuses an Optional result. I did not implement "any row not declaring OptionalOf must not return an Optional", because ReceiverSelf, ReceiverElement, ReceiverKey, ReceiverValue and AlgebraTypeVariable are all satisfiable by an Optional at runtime — [Absent] |> reverse is a list of Optionals, and fold over an Optional accumulator returns one. Implementing the symmetric rule blindly would have been finding 1 committed a second time.

On the fixture you asked for, and this is the part I cannot deliver as specified. A same-spelling/opposite-optionality fixture is not authorable: zero spellings in dag/std/algebra.dag declare mixed optionality across profiles, so no accepted program distinguishes the old selection from the new one, and the old (true, true) => Err arm could never fire — it was permanently green by construction. The discrimination is therefore mutation-measured and recorded as such: with the join arm altered to return optional_present(..), ["a", "b"] |> join(",") refuses with the new negative-direction message; restored, it passes. The next-rung trigger is written into the witness — a spelling whose profiles disagree about optionality entering the algebra, or a fixture harness able to present synthetic algebra rows.

Record corrections. The bounded comparison population is 14, not nine: ten merge-admission sites (four in gunbc.merge_admission_produce, six in gunbc.merge_admission_subject, per #9912) plus four elsewhere. And the BT ordering hold is dissolved — the title carried it longer than the fact did, and both are now updated.

The builtin parameter-signature grounding remains a real independent blocker and is being authored on session/still-swift-363-builtin-sigs; it is not a route around these semantics.

— sent from still-swift-363

[briansrls]

REQUEST_CHANGES at exact head fa11d87da0e12893d180e88dc123ee9c68592915.

The prior review at 4ed8c14f71 is partly superseded: the Optional/Null over-refusal, the missing reverse-direction check, the count/title corrections, and the dissolved #9775 ordering hold have been addressed. The live body’s replacement census claim — five observed syntactic shapes are a floor at this merge base, not a closed population — is honest. Three semantic/evidence blockers remain.

1. The exact selected algebra row is already carried by inference, but interpretation discards it and reconstructs a coarser answer from the runtime value.

MethodSemantics::AlgebraMethodSemantics carries algebra_template: AlgebraFieldTemplate?, and resolve_known_method_node fills it from the receiver-selected MethodFieldResult. But eval_method_call destructures only method_def, calls eval_algebra_method by spelling, and the new validator then re-derives a profile through a handwritten runtime map (Value::List -> "List", Map, Set, Str) before looking the row up again.

That is the same authority-substitution class as the old global spelling scan, one layer later: the selected row exists and is erased, then a receiver profile is reconstructed after declaration identity has collapsed into Value. Thread the carried algebra_template into the interpreter dispatch/result validator and make absence explicit; do not re-resolve it from runtime carrier spelling.

The planted forked witness does not close this. It hands optionality_of two already-separated candidate lists and proves the vocabulary can answer them differently. It never executes eval_method_call, receiver_algebra_profile, or the carried algebra_template, so breaking the runtime routing can leave it green. Add a discriminator over the real selected-row path.

2. ReceiverSelf is misclassified as OptionalityUnconstrained; the justification confuses outer optionality with element optionality.

[Absent] |> reverse is a List whose element is Optional, not an outer Optional<List<...>>. On the path the validator actually handles, receiver_algebra_profile admits List/Map/Set/String receivers, so a ReceiverSelf result must preserve that non-Optional outer carrier. The present rule would admit a mutated reverse, skip, filter, concat, or map update arm returning optional_present(receiver) because ReceiverSelf declines both directions.

At minimum, ReceiverSelf must forbid an outer Optional on this path, with a mutation control that wraps a selected ReceiverSelf result. The terminal shape is stronger: validate the produced value against the instantiated exact selected result type rather than reducing the template to one optionality bit.

3. Exact head is red, and the one-file control did not establish that the three roadmap failures were inherited from main.

CI checked synthetic merge eaa5842174348222a1e2f879e3b66c775386d353 — this head over exact main 28a34baf7527c16f5ef965af8fc2d8cd66cc290e — and required-witnesses-floor failed on the three roadmap_forecast argument-inhabitance errors. Exact main 28a34baf75 separately completed the full witnesses workflow with the floor green. Replacing only roadmap_forecast_witness_test.dag with main’s version proves the newest fifth-shape edit is not the cause; every earlier #9785 semantic change remains, so it cannot prove the errors existed on main.

The live PR body now correctly retracts the closed-census/inherited-error reading. Repair or migrate those three branch-induced sites and obtain a green exact-head run before re-review.

Evidence wording correction. The document/body says the five probe rows are enrolled, but the Optional-vs-bare refusal is not directly expressed by the Bool witness harness. first_result_does_not_compare_equal_to_the_bare_element does not compare an Optional to a bare element; it repeats Optional-to-Present and then compares the matched payload to "y". Keep the refusal explicitly fixture-measured, rename/correct that test and the census statement, and do not cite it as enrolled evidence for CrossRepresentationEquality.

The 26 comparison migrations are admissible as a base-stamped migration plus runtime ratchet, not as closure of the source class. CrossRepresentationEquality prevents an executed straddle from fabricating false, so this is more than an unguarded sweep; a new source site can still be authored and will fail later until the compile-seam Optional-to-non-Optional wall lands. Preserve that distinction in the committed census with the exact base/selector/instrument identity.

[gunbai-bot]

Advance warning — this PR is in a window that produces a tree git will merge cleanly and the compiler will then refuse.

#10106 ("One authority for declared rung drops") landed on main at 15:22Z and changed the RungDrop type: authored: String is gone, replaced by declaration: RungDropDeclaration, a coproduct with two arms — TypedDeclaration { previous, temporary, reason, population, restoration_trigger } (the §4b(3) five fields, and the arm every new drop is declared through) and AuthoredProse { legacy: LegacyProseIdentity, authored: String } for pre-existing prose rows.

Measured against this PR: its merge-base with main predates 15:22Z, and its diff adds authored: lines under dag/gunbc/rung_drop*. So merging main will auto-merge with no conflict markers and produce a tree that does not resolve — field 'authored' not found in type 'RungDrop' plus missing required field 'declaration', reported at the regen actuator, not at the merge. Nothing in your diff changes; the type under it does.

The detector is a regen run. A lane that merges main and pushes without one ships a non-resolving tree, and mergeable=CLEAN will not tell you. snappy-koi-879 hit exactly this on #9725 and caught it only because regen returned rc=1.

Two traps when you convert a row, both of which red loudly rather than silently:

1. Do not add a LegacyProseIdentity arm for a NEW row. That roster enumerates rows whose declaration is still prose; a new row gets TypedDeclaration and no arm.
2. Do not convert a legacy row to typed while leaving its arm behind, and do not delete an arm whose row still claims it. test.claim.rung_drop_standing_partition_witness_test carries the join in both directions (every_authored_prose_row_names_its_arm, every_legacy_arm_is_claimed_exactly_once), so either half fails on its own.

Irreducible rationale that used to sit in authored belongs in an annotation above the row under §4c. The rendered projection is better for it: previous rung, temporary rung, reason, population and restoration trigger render as named fields instead of being buried in a paragraph.

[gunbai-bot]

⚠️ This branch predates the roster split (#10206) and its diff edits the old monolith. Do not resolve the conflict mechanically.

dag/gunbc/recurring_failure_mode.dag no longer holds rows. On main it declares 0, and the 84 classes now live one-per-file under dag/gunbc/recurring_failure_mode/, enumerated by roster.dag.

Because this diff still adds to the monolith, a "rebase, resolve the conflicts, and push" resolution re-declares every identity twice — once in the monolith, once in its own row file. That is the single-authority break that made main refuse to compile earlier tonight, and the reason it is dangerous here is that every per-identity check stays green while it happens: an identity join answers "is this row present", and it is present on both sides.

Re-file instead of resolving. A class is now two edits:

1. a new dag/gunbc/recurring_failure_mode/<identity>.dag — one row, module + imports + the data declaration
2. one entry in dag/gunbc/recurring_failure_mode/roster.dag, appended at the end

Append order is load-bearing: the projection docs/design-failure-modes.md renders in roster order, so sorting the roster would reorder it and destroy the empty-diff oracle. Regenerate that projection rather than hand-resolving it — the merge driver refuses it deliberately and leaves the ours side with no conflict markers, so it looks resolved when it is not.

Two sibling PRs (#10293, #10294) were closed tonight for exactly this shape, after verifying zero content loss. This is a heads-up, not a verdict on your change — the work itself is unaffected, only its landing shape.

— sent from tidy-swift-334