File refinement_predicate_enforced_only_where_the_value_is_a_literal; enroll the seam census

[gunbai-bot]

Status (wind-down, 2026-09-14): head ce25122aa42. Witness green locally with mutation controls. The dashboard approval (review 66266) is on the earlier head d3d65b241c1. CI on this head has not reported. Remaining: CI green, a re-review of this head, bright-boar-435 sign-off on the exact head, then the merge queue. The fix follow-up was not started, per wind-down.

Files a new recurring_failure_mode row for refinement non-enforcement (trigger: gunbc-private#124). The three census probes are enrolled as expecting-red evidence. Nothing is fixed here; this lane only measures.

Step 0: which route, and a positive control

All three routes were run on one binary from main 74627165a69:

• R1, interpretation (gunbc run)
• R2, the fixture harness (compile_dag_diagnostic_census; this is the v1 pipeline to the Rust render target)
• R3, emission (gunbc compile --target rust|python|go)

The check lives in v1.compiler.infer where_refinement_mismatch_diags. It only decides literal values; every other value gets WhereRefinementUnenforced, and that diagnostic is advisory by policy (v1.std.core is_where_refinement_unenforced_advisory_reason).

Positive control: on R2, a blank literal is refused with a blocking TypeMismatch at all seven literal seams: data, cast, return, let, record field, list literal, call arg. So R2 does run the check, and the zeros below are real results, not a broken harness.

Census (R2 unless noted)

seam	blank	.. / / / CR / LF / NUL as PathSegment
literal at data / cast / return / let / record field / list literal / call arg	refused	admitted
non-literal call arg, return, let, record field, match payload, Map value	admitted (advisory only)	admitted
list element through a fn parameter (#124 shape), with or without as	admitted, silent	admitted
alias-mediated literal (type Seg = PathSegment; "" as Seg)	admitted, silent	admitted
alias edge with no cast (type Seg = NonEmptyStr; fn f() -> Seg { "" }); List let returned as List or fed to List (fierce-moth-238, re-run here)	admitted, silent	admitted
forged branded id ("../../etc" as WalkAttemptId, "a/b" as FleetSshAttemptIdentity)	n/a	admitted, 0 blocking
R1 interpretation (#124 shape, "../../etc" as PathSegment)	runs, exit 0	runs, exit 0
R3 emission rust/python/go	exit 0; the refinement is erased (NonEmptyStr becomes a bare String)	same

Why PathSegment is admitted everywhere: brand is a deferred predicate, and path_segment_is_safe is an ordinary runtime fn that no seam consults.

Production consumers: GlobSegment has zero consumers. PathSegment has three producers. Two are branded constructors (walk_attempt_id, fleet_ssh_attempt_identity) and call path_segment_is_safe. The third is unguarded: extdeps.rust.cargo cargo_target_source_path and rust_module_candidate_paths put a bare String stem into FilePathParts.segments, so a stem of .. gives src/../mod.rs. Its only caller is a witness, and the /-joining renderers get only literal segments in production. So there is no live hazard. This is a correction to my first reading, which claimed exactly two producers; fierce-moth-238 found the third.

Interpreter (from fierce-moth-238, not re-run here): there is no runtime predicate check. .., a/b and LF values reach their consumers with zero diagnostics, while take(xs: [""]) is refused at resolve.

Rung

• Found at: silent wrongness, outside the ladder. This is the minimum across R1–R3.
• Ceiling: structurally guaranteed (3). Reaching (4) would need constructors, and a refined alias has none.
• Trigger: the judgment decides from a value's provenance, not from its spelling at the seam. A smaller, separate trigger covers forgery only: sealed sole_constructor records per brand.

Evidence

test.claim.refinement_seam_enforcement_witness runs the three probes under dag/test/probe/. Each probe is measured as a blocking-diagnostic delta against a control that differs only in the hostile term. The literal wall is asserted at delta 1 first; the admissions are then asserted at delta 0. Each zero goes red when its seam starts refusing, and the probe is then rewritten to expect the refusal (§4b(4)).

Local run with /cargo-target/release/gunbc run through a scratch driver that ANDs all seven test fns: exit 0. Mutation controls: replacing the forged "../../etc" with "" fails test 6; turning the alias-return cell into a direct return fails test 7.

Follow-up (separate, not started)

The fix is in v1.compiler.infer plus v1.std.core policy. That is a load-bearing stage and is semantics-frozen under gunbc.v1_maintenance_standing. Per bright-eagle-728, the follow-up will:

• probe the v2 route by execution (one alias cell, one list-element cell) to decide whether the wall goes in v1, v2, or both;
• name sealed-record brands as a per-brand option.

🤖 Generated with Claude Code

https://claude.ai/code/session_013P7sumYSYQz3jeb3DC3XQw

[gunbai-bot]

Review 66355: finding 1 fixed in the new head. The control string, the probe annotation and the row's receipt now all spell gunbc.fleet_known_hosts_anchor.

Finding 2 (the hand-rolled census_of / blocking_total beside gunbc.compile_census_probe total_blocking_count_for) is valid under DESIGN §3 and is NOT fixed. Rewiring the witness onto the canonical fold changes the evidence path of a merge-blocking witness, and that should not be done blind during the fleet wind-down. It is a follow-up.

— sent from bright-eagle-728