File refinement_predicate_enforced_only_where_the_value_is_a_literal; enroll the seam census

dag/gunbc/recurring_failure_mode/refinement_predicate_enforced_only_where_the_value_is_a_literal.dag

@@ -0,0 +1,21 @@
+module gunbc.recurring_failure_mode.refinement_predicate_enforced_only_where_the_value_is_a_literal
+
+import std.types { NonEmptyStr }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data refinement_predicate_enforced_only_where_the_value_is_a_literal: RecurringFailureMode = RecurringFailureMode {
+  identity: "refinement_predicate_enforced_only_where_the_value_is_a_literal" as NonEmptyStr,
+  receipts: [
+    "SUBJECT: a value that violates the predicate of a `where`-refined type, at a position declared to hold that type. std.types declares NonEmptyStr = String where non_empty, and PathSegment, GlobSegment, LogicalTime and a dozen branded ids as NonEmptyStr where brand(...). THE WALL IS A PROPERTY OF THE SPELLING AT THE SITE, NOT OF THE REFINEMENT: enforcement lives in v1.compiler.infer where_refinement_mismatch_diags, reached from infer_expr through with_expected_where_refinement_diags at every position that threads an expected type -- but where_refinement_diags_for_predicate DECIDES ONLY WHEN THE VALUE IS A LITERAL. Every non-deciding arm emits WhereRefinementUnenforced, and all six of its reasons are advisory by policy (v1.std.core is_where_refinement_unenforced_advisory_reason -> SeverityNonError / GateAdvisoryTypecheck). So the refinement is a comment everywhere a value is not written out at the seam. This is the floor obligation that values inhabit declared types (DESIGN 4b, the floor first), broken for every non-literal value rather than for one argument shape -- which is what separates it from its neighbour refined_alias_argument_exempt_from_declared_type_inhabitance, a class about the FORMAL being a record.",
+    "CENSUS, MEASURED BY EXECUTION ACROSS THREE ROUTES ON ONE BINARY, 2026-09-14, main 74627165a69. R1 INTERPRETATION, `gunbc run`: a blank element in a List<String> reaching a List<NonEmptyStr> parameter, and `\"../../etc\" as PathSegment`, both run to exit 0 with no refusal (the gunbc-private#124 trigger, reproduced). R2 THE FIXTURE HARNESS, compile_dag_diagnostic_census, which its own carrier note scopes to the v1 pipeline to the RUST RENDER TARGET on a synthetic single module. R3 EMISSION, `gunbc compile --target rust|python|go`: exits 0, and the refinement is ERASED -- emitted Rust is `pub fn take(xs: Rc<Vec<String>>)` and `fn hostile_segment(raw: String) -> NonEmptyStr { raw.clone() }`, NonEmptyStr a bare String alias, PathSegment not surviving as a distinct name, no constructor and no check; python and go the same. The NonEmptyVec/NonEmptyBTreeSet wrappers that DO validate are for non-empty COLLECTIONS and never touch `String where non_empty`. THE POSITIVE CONTROL HOLDS AND IS WHAT MAKES THE ZEROS OBSERVATIONS: on R2 a blank LITERAL refuses with a blocking TypeMismatch at all seven literal seams -- data binding, cast, function return, let, record field, list literal, call argument.",
+    "WHAT ADMITS, on R2, each measured as a differential against a control identical but for the hostile term. ADVISORY-ONLY (one WhereRefinementUnenforced, nothing blocking): call argument through a String parameter, with or without a cast; function return; let binding; record field; match payload; Map value; an element cast inside a list literal. SILENT -- zero blocking AND zero advisory, no diagnostic of any severity: (a) A LIST ELEMENT THROUGH A FUNCTION-PARAMETER BOUNDARY, the #124 shape, whether or not an `as` cast is written; (b) AN ALIAS-MEDIATED POSITION. (b) is the sharpest cell and was not predicted: `data v: PathSegment = \"\" as PathSegment` REFUSES, and the identical construction through a one-line local alias, `type Seg = PathSegment` then `data v: Seg = \"\" as Seg`, is admitted in silence. One alias line defeats the only wall this class has. THE ALIAS HOLE IS WIDER THAN THE CAST FORM, first measured by fierce-moth-238 and re-run by this lane on the same R2 route: `type Seg = NonEmptyStr` then `fn f() -> Seg { \"\" }` is silent while the direct `fn f() -> NonEmptyStr { \"\" }` refuses, so the plain alias edge drops the predicate with no cast, brand or data binding; a List<String> let returned as List<NonEmptyStr>, or fed to a List<PathSegment> parameter, is silent too. The same lane reports, by execution on R1 and not re-run here, that the interpreter carries no predicate arm: blank, .. and a/b elements and an LF-bearing String cast as PathSegment reach their consumers with zero diagnostics, beside an interpreter positive control where take(xs: [\"\"]) refuses at resolve.",
+    "THE PATHSEGMENT HALF IS WORSE AND IT IS NOT A SEAM PROBLEM. `brand` is on the compiler's DEFERRED predicate list (v1.compiler.infer where_refinement_is_deferred_predicate), so PathSegment contributes NO decidable predicate of its own and inherits only `non_empty` transitively. The law std.types path_segment_safety_note calls 'the law, held once' lives in path_segment_is_safe, an ordinary runtime fn that NO SEAM CONSULTS. Measured on R2: of the characters that note names -- `.` `..` `/` `\\` CR LF NUL -- ZERO are refused at any seam, on any route, in any spelling, INCLUDING as a bare literal, which is the one place every other predicate in this corpus does refuse. `\"..\" as PathSegment` and `\"a/b\" as PathSegment` compile clean. The blank is the sole refusal and only because non_empty reached it. GlobSegment is identical.",
+    "BRAND FORGERY, the consequence that ranks. gunbc.merge_admission_subject WalkAttemptId and gunbc.fleet_known_hosts_anchor FleetSshAttemptIdentity are both `PathSegment where brand(...)`, and both modules state in their own prose that their validating fn is 'the only constructor' and 'REFUSES rather than sanitizing'. BOTH STATEMENTS ARE TRUE ABOUT THE FUNCTIONS AND FALSE ABOUT THE TYPES: a refined alias has no constructor to seal, so sole-constructor admission never applies to it. Measured: a foreign module writing `\"../../etc\" as WalkAttemptId` or `\"a/b\" as FleetSshAttemptIdentity` -- carrying exactly the characters those functions exist to refuse, into ids that are concatenated into <root>/.gunbc/merge-admission/<attempt_id>/ and into the known-hosts anchor path -- adds ZERO blocking diagnostics.",
+    "PRODUCTION CONSUMERS, INCLUDING A CORRECTION TO THIS LANE'S FIRST READING, which claimed PathSegment had exactly two producers, the branded walk_attempt_id and fleet_ssh_attempt_identity, both calling path_segment_is_safe. That counted brands and missed the unbranded carrier: std.types FilePathParts has `segments: List<PathSegment>`, and extdeps.rust.cargo cargo_target_source_path and rust_module_candidate_paths build it from a bare caller String (`concat(name, \".rs\")`, and `[\"src\", stem, \"mod.rs\"]`) at the admitted list-element seam with no path_segment_is_safe, so a stem of \"..\" yields src/../mod.rs with no refusal. Found by the parallel census lane fierce-moth-238 and confirmed by grep: both fns' ONLY caller is test.claim.cargo_target_path_witness_test, so it is a third, unguarded producer and NOT a live production hazard. The FilePathParts renderers that join on / (v2.extdeps.languages.bash_orch_if bash_relative_parts_text / bash_absolute_parts_text, extdeps.linux.proc_self_cgroup proc_self_cgroup_mount_root_text) receive only literal segments in production (v2.workflow.ci_floor_peak_emit). GlobSegment has ZERO consumers. extdeps.uri_path PathSegmentTokensResult / MalformedPathSegment are a different name, not this type.",
+    "ENROLLED FORM: three probes under dag/test/probe/ -- refinement_seam_admission_probe, path_segment_predicate_admission_probe, branded_path_segment_forgery_probe -- each a module that RESOLVES TODAY, which is the finding. test.claim.refinement_seam_enforcement_witness reads each off the tree and hands it to compile_dag_diagnostic_census paired with a control that is the same module with every hostile term made safe, so the shared closure cancels and the delta is the hostile term alone; the carrier's own rule forbids reading a total over an importing fixture. It asserts the literal wall at delta 1 FIRST -- without that the zeros would be indistinguishable from a harness that cannot refuse, which DESIGN 4b calls a permanently-green decoration -- then asserts the admissions at delta 0. Those zero assertions are the tripwires: each goes red the day its seam starts refusing, and the probe is then rewritten to expect the refusal rather than retiring (DESIGN 4b(4)).",
+    "RUNG FOUND AT AND CURRENT RUNG: silent wrongness, OUTSIDE the ladder, and that is the MINIMUM across all three in-scope routes, which is the rung (DESIGN 4b(1)). Citing the literal wall would be inflation twice over: it is mechanically preventable at best, and the alias receipt shows it defeated by one line. CEILING: structurally guaranteed (3), not impossible (4). non_empty and path_segment_is_safe are total decidable functions of a fully-modeled String, and the compiler already computes the first -- decidable_where_string_predicate_holds runs non_empty today -- so the judgment is not the missing piece; what is missing is that it is attempted only for literals, and that brand carries no predicate to a value's provenance. (4) is out of reach while these are refined ALIASES, because an alias has no constructor to seal, which is why the ceiling stops at (3) rather than at unwritability.",
+    "NEXT-RUNG TRIGGER, capability grain: the refinement judgment decides a value's predicate from its PROVENANCE rather than from its spelling at the seam -- a value whose origin does not establish the predicate is refused at a refined position, at every seam that threads an expected type, with alias-mediated and list-element positions judged exactly as the direct spelling is. Sufficient for flipping every zero-delta assertion in test.claim.refinement_seam_enforcement_witness to expect refusals. NOT satisfied by: widening the literal arm to more literal shapes; promoting WhereRefinementUnenforced from advisory to blocking, which refuses correct code rather than judging it; or adding a predicate to brand() alone, which leaves every non-branded refinement where it is. A SEPARATE AND SMALLER TRIGGER CLOSES THE FORGERY HALF ALONE, and it is worth naming because it does not touch a load-bearing stage: each branded path-segment id becomes a sealed sole_constructor record whose only mint runs path_segment_is_safe, at which point the two prose 'only constructor' claims become walls. That closes forgery for those brands and closes nothing else.",
+    "WHERE THE FIX LIVES, FLAGGED AND NOT STARTED per the census lane's brief: v1.compiler.infer (where_refinement_diags_for_predicate, where_refinement_mismatch_diags) and the disposition policy in v1.std.core -- the v1 seed's inference stage, which DESIGN names as load-bearing, and which is semantics-frozen under gunbc.v1_maintenance_standing so a change there must pass its PURPOSE admission test. READ, NOT MEASURED, and labelled as a code reading rather than a receipt: src/v2/compiler/04_infer.dag carries no where-refinement predicate judgment of any kind, so on the v2 route the wall is not weak but ABSENT, and the question for the fix lane is whether it is BUILT there rather than repaired in the seed. Probing the v2 route by execution is the first step of that lane, not a claim this row makes.",
+  ],
+  evidence: [],
+}