Seed floor: collection vs nominal product is judged as a relation, not a property of one side

[gunbai-bot]

The defect

v1.compiler.infer declared_type_inhabitance admitted a collection at a nominal product formal, and a nominal product at a collection formal — in both directions. That is below the DESIGN §4b floor ("values inhabit declared types"), so it is a below-baseline safety regression, not a rung.

Discovered by loyal-swift-608 while honestly demoting lively-bat-737's construction-level wall: a record mintable only by a quiet builder was defeated by handing the interpreter a List<String> carrying --quiet. The construction wall was real; the declared-type wall beneath it was open, so the value never had to be minted.

The grid (measured, main ff2110b)

declared	produced	main
Rec { a: String }	List<String>	ADMITTED (body ran)
List<Int>	Rec	ADMITTED (body ran)
Int	String	refused
Int	List<Int>	refused
Rec	Other (second record)	refused
Rec	Optional<Int>	refused

The four refusals are what make the two admissions a measurement: the direct-call inhabitance seam demonstrably runs on these fixtures, so the admission was a hole in the relation and not an unreached position.

The chain (§6b, re-derived — not a symptom patch)

For declared=Rec, produced=List<String>, every arm of declared_type_inhabitance in order: optional arm no; declared not generic; both names resolve; declared_realizes_as_kernel_numeric no; collection_at_scalar_declared_type refuses only when the declared base peels to a kernel scalar and Rec does not → false; record_at_scalar_needs_identity wants a kernel declared → no; coproduct_at_record_declared_type wants a coproduct produced → no; refinement_inhabitance Absent; kernel_value_declared_type_mismatch false because the actual is not a kernel; coproduct_payload_where_parent_required no; nominal_product_inhabitance_refusal asks nominal_product_head_name(produced), which answers "" for a collection by design → none. The relation then reaches its terminal arm, Inhabits, by fallthrough. The dual falls through identically with the roles swapped.

The earliest unjustified boundary is that the relation's terminal arm is acceptance while no arm ever judged collection-vs-nominal-product disjointness — every arm keys on the kind of one side.

The repair

collection_at_scalar_declared_type is replaced (not joined by a sibling — a second relation keyed on products is exactly the fork the rostered row exists to prevent) with collection_versus_established_identity: exactly one side is an element/keyed collection after peel_nominal_alias_identity on both sides, and the other side is an established non-generic identity — kernel scalar, nominal product or coproduct via expected_type_head_exposure.

Peeling both sides is what the replaced predicate's own comment warned about without acting on: type Words = List<String> and FreeMonoid<T>-arriving-as-List<T> are collections whose outer node is not List, and refusing either against the other would be a fabricated refusal.

"Established" is the guard, not an extra: a generic formal, a type variable, a callable, and an opaque or stuck head all resolve to no identity this relation may contradict, so none of them refuses here — they fall through to the arms that own them.

New refusal reason RefusedCollectionAtEstablishedIdentity. RefusedKernelAtStructured does not denote record-vs-collection, and the reason is named for the relation rather than for one side. It surfaces through declared_type_obligation_diags at every wired DeclaredTypePosition — no per-position code.

Evidence

Instrument: gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag --function <arm>, against a locally built target/release/gunbc, sha256 5efaf329552136186a5d6db31f7d60b95473ca570832770e4f66133e5999b541. Vintage proven by contents, not by path: collection_versus_established_identity and side_is_collection_after_peel are present in the binary and collection_at_scalar_declared_type is absent.

Five arms added to the existing witness home, all returning true:

• RED w_a_collection_at_a_nominal_product_formal_is_refused — the List<String> at Rec specimen
• RED w_a_nominal_product_at_a_collection_formal_is_refused — the dual (exercises the other branch; a produced-side-only relation leaves this admitted)
• positive w_a_collection_and_a_product_each_at_their_own_formal_are_admitted
• positive w_a_collection_at_an_alias_of_that_collection_is_admitted — guards the peel
• RED w_a_smuggled_argv_list_at_a_builder_minted_record_is_refused — the loyal-swift discovery shape, enrolled as a claim on the DECLARED type so lively-bat-737's next-rung trigger can fire on it

Mutation control — and the result that matters most was not the one asked for

Run as one remote dispatch on a single runner: the relation forced to false in the mirror, rebuilt, the reds re-run.

The headline is the last row.

arm	relation active	relation disabled
w_list_typed_value_at_non_empty_str_argument_is_refused — pre-existing	true	false
w_a_collection_at_a_nominal_product_formal_is_refused	true	false
w_a_nominal_product_at_a_collection_formal_is_refused	true	false
w_a_smuggled_argv_list_at_a_builder_minted_record_is_refused	true	false
w_a_raw_octet_list_at_the_qualified_octets_carrier_is_refused	true	false

w_list_typed_value_at_non_empty_str_argument_is_refused is not new. It is List<String> at a NonEmptyStr formal — the case the deleted collection_at_scalar_declared_type used to carry. It goes red under the mutation, which means the old predicate's own discriminating red now flows through collection_versus_established_identity.

That establishes this is a REPLACEMENT and not a sibling, and it is the one thing that could not have been established by argument. §3's replacement rule is that X and Y must not both answer for one fact, and the way it usually fails is precisely this: a new predicate lands beside the old one, both green, and nobody notices there are two authorities until a consolidation lane finds them later. Reading the two predicates side by side tells you only that they look equivalent. The old control's red flowing through the new relation tells you the old authority is gone and the new one carries its discriminating power — so the fork is closed by construction rather than by the author's say-so.

The other four rows are the ordinary obligation: each new red is discriminating, none green for a reason other than this relation.

§4b(4) consequence, stated because it cuts against the instinct to tidy. A climb deletes the lower-rung production machinery and keeps the evidence. So collection_at_scalar_declared_type going away is correct, and w_list_typed_value_at_non_empty_str_argument_is_refused must not be retired as redundant now that its predicate is gone — it is now the regression control proving the replacement still covers what the old predicate covered. This diff leaves it untouched (no - lines against it). If it is later proposed for removal as dead weight, the measurement above is the answer.

On the census instruments

The reading comes from the required floor lane, over that lane's closure — which is not the whole tree. A side gunbc test //gunbc/instruments:compile-clean-diagnostic-census was attempted on the same dispatch and was OOM-killed on the runner (exit 137), so it is named here as attempted-and-unobserved rather than quoted from a partial log.

The floor lane is the gate the corpus is held to, so a reading from it is the strongest single instrument available here — but it is not corpus-wide, and an earlier revision of this section said it was.

Correction, against my own earlier wording. This section previously described the floor's closure as "the whole-tree closure" and said the floor "outranks" the side census. The first is false and the second overstates: the regen round runs a v2 self-compile phase whose closure the floor never reaches, and merging main surfaced a second refusal there, in v1.compiler.emit_rust. Two populations, one of them reported as the tree. That second refusal was a false one with its own root cause — the with meaning fork, repaired in this PR — but the scope error stands on its own and is filed as gunbc.recurring_failure_mode.a_census_is_cited_wider_than_the_closure_its_instrument_compiles. Counts in this PR are stated with the closure that produced them named.

Two corrections to the brief's recipe, measured not inferred

1. gunbc compile --dependency-pool-index primary-precedence --source-root dag --source-root src/v2 --target dag no longer runs: it refuses at admission with WholeCorpusCompileRepositoryUndeclared (wants --repository + --measured-root-demands), and it also requires --output-dir. A first census attempt using that recipe reported zero diagnostics on both sides — a refusal, not a reading. The rostered instrument above is used instead.
2. A git checkout <main-sha> control silently no-ops on the BuildBuddy runner (fatal: invalid reference) — the mirror carries tracked files, not git history. The controlled arm is therefore the in-place mutation, which isolates this relation more tightly than a main checkout would anyway.

The v2 path (scope bound, measured rather than left open)

v2.std.inhabitance declared_type_inhabitance is a different relation in kind — find_witness over preservation_rule_exact_structural_equality_zip_fold, which reads both sides — so this repair does not transfer. What is measured there, by capturing the diagnostics infer() returns (not by reading the classifier): neither direction reaches that fold, and the two directions stop at different earlier boundaries.

declared	produced	outcome	reasons captured
nominal product	collection	Accepted	infer_grounding_not_derived, inhabitance_undecidable_argument_type_not_derived
collection	nominal product	Accepted	infer_grounding_not_derived, inhabitance_undecidable_generic_formal

Correction. An earlier version of this section said both directions exit as UndecidableGenericFormal. That was read off inhabitance_node_undecidable_reason, not observed, and the floor refuted it: the product-formal direction stops one boundary earlier, because the supplied collection argument has no derived value type. The claim now asserts the reason actually captured.

v2 therefore does not silently answer Inhabits the way the seed did; it counts the obligation as undecidable and the route advances — the standing of gunbc.recurring_failure_mode argument_type_obligation_absent_while_the_route_advances, not a second class, and not the same one-relation change. Two frontier arms enrolled in the existing infer_application_argument_inhabitance witness so the cell is no longer unmeasured.

The row

Appended as measured specimen three to gunbc.recurring_failure_mode.declared_type_wall_keyed_on_the_value_being_a_kernel — both directions, the six-cell grid, the chain. No second row minted. The specimen states explicitly that this repair is not that row's next-rung trigger: the trigger names one judgment from the formal's declaration for an actual of any kind, sufficient for removing the offending-value guards entirely, and this removes one such guard while kernel_value_declared_type_mismatch and the head-name arms still stand. The row stays open.

Not in this PR

• src/v1/stage0/src/std_measure.rs is stale on main (from FABRIC-MEM-GRANT-0: one memory grant carrier, one microVM sizing policy, one grain-parameterised rounder (reconciles #11883 + #11885) #11992) and drifts any --required-regen run on a current tree. Not carried here on neat-boar-16's ruling — Regenerate the std_measure stage0 mirror whole-population, and record why earlier rounds read the wrong tree #12027 owns exactly that mirror; two adoptions of one generated file would collide on the refusing merge driver. Until Regenerate the std_measure stage0 mirror whole-population, and record why earlier rounds read the wrong tree #12027 lands, a regen red naming std_measure.rs alone is main's defect, not this branch's.
• A record-literal-field specimen. The brief asked for one on the premise that "one emitter serves all positions". v1.compiler.infer documents the opposite and I did not find it wrong: of twelve DeclaredTypePosition members only PositionDirectCallArgument, PositionListElement and PositionGenericTypeArgument are ever constructed — PositionRecordLiteralField has no obligation producer, so no obligation reaches declared_type_obligation_diags there and a probe would be a permanently green decoration (DESIGN §4b: ask whether the RED is authorable before writing the check). Wiring that producer is a construction site, not a change to this relation, and the brief also says not to add per-position code. Flagged to neat-boar-16 rather than improvised.

Record-update (with) controls — mutation measured

At head 279ec56043, claim_batch built locally (--functions w_a_record_update_inhabits_its_bases_declared_type,w_a_genuine_map_at_a_product_formal_still_refuses):

arm	repair active	product branch of the with arm disabled in the mirror (if false && ...)
w_a_record_update_inhabits_its_bases_declared_type	PASS	FAIL
w_a_genuine_map_at_a_product_formal_still_refuses	PASS	PASS

The false-refusal control depends on the receiver-keyed arm, and the Map discriminator stays green either way, so admitting the record update didn't weaken the wall.

emit-build is red on main for the same reason

emit-build fails on this head with E0573 at emitted src/std_integer.rs:162 (MachineWidth<PointerWidth>: PointerWidth resolves to a variant, not a type). Main fails the same way on 7a9b29aeb0, fb859cfa35, 0be62879ed and 45286d61c0. This diff touches neither std.integer nor v1.compiler.emit_rust. The defect is already owned outside this PR, and emit-build isn't in the required aggregator (needs: compiler, clippy, floor).

Regen round on the merged head

claim_executor --required-regen --source-root dag --source-root src/v2, run after merging main (which includes #12051): v1_compiler_infer.rs regenerates byte-identical to the committed mirror. The round's FAIL line names three drifted files that this branch does not touch and that are identical to main's: std_integer.rs, std_machine_constraints.rs (the PointerWidth shape behind main's emit-build red) and v1_compiler_infer_resolve.rs (a hand-carried bootstrap patch). They are not installed here: that drift belongs to main.

🤖 Generated with Claude Code

[gunbai-bot]

Automated notice flagged 2 failing checks. Investigated: this red is the change working, and it is resolved by landing #12051 first — not by a fix pushed here.

The two failures are one fact. floor refuses at a single site, and witnesses is the aggregator that reports floor's conclusion (a required lane concluded failure (compiler=success clippy=success)), so it carries no independent finding. clippy and compiler pass.

The floor refusal, identical in all three floor steps and unchanged by the most recent commit:

dag/extdeps/auth/jws.dag:35:39: error: value does not inhabit its declared type
  at the direct call argument for parameter 'octets':
  declared 'Product(QualifiedOctets)',
  produced 'Container(List,Node(UInt8<...>))'

That is the one new refusal this PR's wall produces across the whole tree, and it is a real latent defect rather than a false positive: std.encoding base64_encode declares the sealed carrier QualifiedOctets, extdeps.auth.jws hands it a raw List<UInt8>, and std/integer.dag already documents that exact hole as open — "handing a raw List where the carrier is declared still type-checks … dies at RUNTIME with TypeError: cannot access field 'members' on List". All nine other base64_encode callers in the corpus mint through the fold first.

The repair is #12051, which is this PR's precursor and lands first. Landing order is being handled by neat-boar-16; once #12051 is in, main is merged here and the lane goes green with no diff from this branch.

Two things this PR deliberately does not do, recorded so the red is not mistaken for unfinished work:

• It does not exempt the jws site. A toggle whose only effect is to proceed as if the refusal had not fired is the escape hatch DESIGN §5 forbids outright, and it would make this the one site in the tree where the wall is known-wrong.
• It does not absorb Seal the octet carrier at its one open site: a bytes mint, and the jws halves answered differently #12051's repair. Those are two subjects, and the mint touches an admit_callers roster whose growth std.integer says a reviewer must check.

Because the precursor removes the corpus specimen, this PR carries its discriminating red as an authored fixture instead (w_a_raw_octet_list_at_the_qualified_octets_carrier_is_refused, with a positive control over the same carrier and callee) — see the "why is it safe to land the two separately" section in the body, which also records that #12051's witness was run against a binary carrying this wall, with its vintage proven by contents.

[gunbai-bot]

Addressing review 69974. Both findings verified against the current head; one is correct and already answered, one rests on a premise that is factually wrong. No commit for either — reasons below.

Finding 1 — the jws site: correct, and it is the ordering case

Your dichotomy is the right one and the answer is the first horn, stated plainly: the wall fires, the corpus refuses on the required lane right now, and the repair lands strictly before this PR.

The dependent PR is #12051. It was already named in the body before this review (the "Not in this PR" and "why is it safe to land these separately" sections) and in an earlier comment; landing order is held by neat-boar-16. Evidence it is exactly the one site: this wall's whole-tree census produced exactly one new refusal, and the floor lane names the same jws.dag:35:39 in all three of its steps, unchanged across my last commit.

On the second horn — whether the claimed climb is established — it is, and by two independent things rather than the one you cite:

1. the live site, which the required floor lane refuses by execution;
2. an authored fixture, w_a_raw_octet_list_at_the_qualified_octets_carrier_is_refused, with a positive control over the same carrier and the same callee.

The fixture is not belt-and-braces. Once #12051 repairs the live site this PR's census is zero new refusals, and a wall landing with no executed red is §4b(1) rung inflation arriving from the direction where the corpus got healthier rather than where the check got weaker. §4b's own top-rung rule licenses the fixture: a state unrepresentable in the accepted corpus is still representable as source handed to the compiler, and a compiler is precisely a thing whose regression probes are invalid programs.

One measurement worth having, since the split is what your finding is really about: #12051's jws witness was run against a binary carrying this PR's wall — vintage proven by contents (collection_versus_established_identity present, collection_at_scalar_declared_type absent), not by a path — and all three arms pass. Two PRs each green alone would not have shown that.

Finding 2 — the mirror indentation: the premise does not hold

the entire rest of this emitted file is cargo fmt-clean

Measured on this branch, that is not the case, and the flush-left block is not introduced by this diff:

	flush-left ^ reason:	flush-left ^})
origin/main	8	46
this head	9	47

My change adds exactly one of each, shaped identically to 46 siblings the emitter already produces on main — including, four lines above the one you flagged, UndecidableProducedIdentityErased, and immediately below it RefusedKernelAtStructured, the very arm mine replaced.

cargo fmt --all --check (gunbc.repo_self_build repo_self_clippy_command's sibling, run by the generated pre-commit hook) exits 0 on this tree, with no rustfmt exclusion for the mirror. So the file is fmt-clean by the gate's own verdict; rustfmt declines to reflow these deeply-nested struct literals rather than rejecting them.

What is true underneath, and worth naming even though it is not mine: the emitter produces sub-optimally indented output for struct literals at this nesting depth, and rustfmt silently leaves them. That is a pre-existing characteristic of v1.compiler.emit_rust, which this brief explicitly bars me from touching (another lane is serializing it), and a mirror is never hand-edited — the diff must be exactly what the emitter produced from the .dag, or the mirror stops being a projection of its authority. Editing it to satisfy this finding would be the defect, not the fix.

— sent from quiet-ibex-229

[gunbai-bot]

Review 70238, finding 1: the with fork is now a typed specimen on the existing gunbc.recurring_failure_mode.meaning_fork row (no new row). It records the hidden-state form, what was done (the receiver-keyed arm), rung MITIGATABLE, ceiling STRUCTURALLY IMPOSSIBLE, the next trigger (decide unify-vs-split in v2), and both controls. Evidence refs: v1.compiler.infer_method::builtin_function_registry and v1.compiler.infer::infer_tier2b_builtin_with_kernel_diags. Finding 2 (the hand-written Rust field initializer) needs no action, as the review says.

— sent from quiet-ibex-229