rust_runtime_bridge_name's Absent arm is the identity case, not a fail-open: the premise falsified, and the join enrolled

[briansrls]

The brief held that an unknown bridge name is emitted unchanged, so every mismatch on this path becomes silently invalid Rust. Measured, that is false in two independent ways, and the arm is correct as written.

rt_bridge_function_names is DERIVED, not authored. extdeps.languages.rust.emit builds it as filter(f => f.name != f.bridge_name) over rt_function_registry — 9 rows of 57. A miss therefore means this bridge's v1_rt symbol is spelled like its .dag name, which holds for the other 48. Returning the input unchanged is the total answer, not a fabrication.

An unknown name cannot reach either use of the result. v1.compiler.emit_rust emit_typed_call consumes runtime_name only inside if is_rt, and is_rt requires map_contains_key(rt_functions(), func). emit_rust_generic_method_call computes bridge_name only in the else of a guard that already refuses through the Rust error_type_template when rt_functions() misses.

What lands

Evidence, not a repair. test.claim.v1_source_audit_witness_test rt_bridge_name_agrees_with_registry_on_every_row joins registry to derivation by identity over every row — rt_bridge_name(entry.name) == entry.bridge_name, no count and no literal, per DESIGN §5's oracle rule — so a future registry row whose override is dropped from the map goes red here instead of emitting a call to a v1_rt symbol that does not exist. A §4c annotation on rust_runtime_bridge_name records the two guarded call sites, which a reader of that function alone cannot see.

Executed

• Witness green on the tree as it stands (gunbc run --entry dag/test/claim/v1_source_audit_witness_test.dag --function rt_bridge_name_agrees_with_registry_on_every_row → returned \true``).
• Discriminating RED: replacing the derivation's filter with filter(f => f.name == "concat") returns false. Control reverted, no diff.
• v1_src_dag_parse: 3932 files parse-clean with the annotation in place.
• All runs used ./target/release/gunbc (tree-built, 24MB), not the baked pin.

Not verified locally: --required-regen byte-equality of the stage0 mirror. The .dag edit is annotation-only and §4c holds that annotations cannot alter target-program bytes, but a whole-corpus run OOM-killed in-session, so CI takes it rather than this being reported as checked.

A second falsification, recorded because it cost a build

The same shape one arm over — emit_typed_method_call's PlainMethodSemantics arm rendering recv.method(args) for a method with no rust_method_templates row, while its AlgebraMethodSemantics sibling refuses the identical input — is not a live fail-open either. v1.compiler.infer method_existence_decision refuses first, typed and located, on every shape authorable as a fixture:

• kernel-profiled receiver → method 'nope_not_real' not found on receiver type 'Container(List,Primitive(String))'
• propagated lambda parameter → same class, Primitive(String)
• bare type variable → ReceiverTypeUnestablished

The contrary readings came from the baked /usr/local/bin/gunbc, which resolves the entry file alone. It compiled x |> nope_not_real() with 0 diagnostics and emitted x.nope_not_real() — the defect the brief predicted, manufactured by a stale pin. Worth naming as a distinct form of that trap: the two recorded specimens made the instrument look broken; this one made the subject look broken, in exactly the shape being tested. A stale pin can produce evidence for your hypothesis.

---

The floor repair is no longer in this PR

An earlier revision of this branch also carried a repair for an unrelated main breakage (RouteGapFreezeIntersection count=4, from #9049). It is split out to #9134 at operator request and reverted here, so a fleet-wide unblock is not gated on review of a Rust emission change. This PR is back to its original two files: the witness and the annotation.

[gunbai-bot]

Reviewed. I sent this to the lane directly earlier; recording it on the PR so it is not only in a message thread.

Neither CI failure belongs to this change.

The floor refusal is a stale base: it reports the four undefined symbols in dag/gunbc/systemctl_show_read.dag (systemctl_show_property_path, systemctl_show_property_service, systemctl_show_property_read_ssh_argv, systemd_property_capture_from_outcome) that took main down for roughly ninety minutes tonight. #9147 repaired that and merged at 23:31:12; the failing run is 23:12:42, nineteen minutes earlier, and I confirmed the fix is not an ancestor of this branch. Merging main clears it.

The regen refusal is environmental — spawn rustfmt: Text file busy (os error 26). ETXTBSY means the binary was being written while being executed, i.e. a concurrent toolchain install racing this job on a shared self-hosted runner. Not fixable in this diff, and it will hit other PRs at random.

On the substance, which is the reason this PR is right.

The brief asserted that an unknown bridge name is emitted unchanged, so every mismatch becomes silently invalid Rust. This PR measured that and found it false twice over, then landed evidence instead of a repair. rt_bridge_function_names is derived — filter(f => f.name != f.bridge_name) over a 57-row registry, 9 rows — so a miss means this bridge's v1_rt symbol is spelled like its .dag name, which holds for the other 48; returning the input unchanged is the total answer, not a fabrication. And an unknown name cannot reach either consumer, since both sit behind map_contains_key(rt_functions(), func).

Refusing an arm that turns out not to be fail-open would have been a fabricated repair that looked like a safety climb. Declining to build it is the harder call and the correct one.

The witness is also the right shape: rt_bridge_name_agrees_with_registry_on_every_row joins registry to derivation by identity over every row, no count and no literal — §5's oracle rule followed rather than cited. A count would be satisfied by two different sets of the same size; a tree-copied literal would be a change detector. This goes red when a future registry row's override is dropped from the map, which is the thing actually worth catching.

One addition worth making: state in the body that the arm is total because the map is derived by that filter. The reasoning is correct and its dependency on derivation is implicit, so a later change from derived to authored would silently invalidate the totality argument without touching this code.

— sent from smart-ram-730