v2 no longer treats source identity as semantic grounding (P0: protect the replacement compiler)

[gunbai-bot]

P0 — protect the replacement compiler: v2 no longer treats source identity as semantic grounding

Closes the second P0 lane of the compiler-static-failure-closure finding (v2-semantic-grounding-wall, first half). The target sentence: stop v2 from treating source identity as semantic grounding.

What was actually wrong — measured, not inferred

v2's infer dispatched on n.kind with a wildcard _ arm covering nine of the closed vocabulary's twelve node kinds (6 connectives + 6 behaviors; only Branch, Match, Loop had a real derivation). That arm called solve_constraints with:

• candidate set [policy.graph.root] — the source node, alone;
• the constraint-satisfaction predicate, whose rule is algebra == source_facts && candidate == source_facts, with algebra bound to the root.

So the witness search reduced to root == root and always succeeded. The grounding it minted carried the source node as its own structural evidence, and it was then stamped ^constraint_property_being_canonical.

The part that makes this more than a mislabelled stamp:

fn inferred_facts_resolved_type(facts: InferredFacts) -> Node {
  facts.grounding.witness.structural.evidence
}

Structural evidence is the node's resolved type. So every literal, binding, type and operation in v2 was typed as itself, and every consumer that asked "what type is this node?" got the expression back.

Measured on main @ a589c5f0179 by execution (throwaway probe, not landed):

probe	main
infer accepts a bare ComputationNode{Value} leaf	accepted
infer accepts a bare TypeNode{Conj} leaf	accepted
canonical_grounding_for_node(Conj) evidence == source	true
canonical_grounding_for_node(Disj) evidence == source	true

canonical_grounding_for_node is the reader 06_translate.coerce_grounded_node funnels through, so the source node was being coerced toward the target as if it were its own derived type. Atom and ComputationNode happened to be screened out by algebra_ref_is_grounded, but that is a shape check on the connective, not a derivation check — which is exactly why Conj/Disj walked through it.

In 05_eval, inferred_facts_for_eval and the inhabitance / canonical acceptance witnesses all called canonical_grounding_admits_infer_facts, which checked well-formedness and the two property stamps — every one of them true by construction on the fabricated path. Both witnesses were therefore vacuously Holds for every node, and they are the same predicate called twice (a §2 duplicate).

The wall

1. Single construction authority (v2.std.constraints). canonical_grounding_from_derived_type(node, derived_type) is now the only way the compiler mints a grounding, and it refuses derived_type == node with a typed, located ^grounding_evidence_is_source. The three real derivations already complied — infer_branch_canonical_grounding passed the unified arm type — and the claim fixtures already passed a real i64 type node, so the intended contract was already encoded in the corpus; only the fabrication violated it.

2. Typed frontier carrier. InferredFacts.grounding is now

type NodeGrounding
  = DerivedGrounding { grounding: CanonicalGrounding }
  | GroundingNotDerived { node: Node }

so inferred structure is distinct from source structure and candidate == source is no longer even expressible as a grounding. infer_node_facts no longer calls solve_constraints at all; the descent proof is still derived (it is a real judgment) and the grounding is the frontier.

3. Total dispatch, no wildcard. infer_gather_fold_init now enumerates all twelve kinds. A thirteenth kind cannot be added without deciding, at that site, whether it derives its type or joins the counted frontier — the decision cannot be defaulted into by omission.

4. Consumers refuse instead of silently consuming. canonical_grounding_for_node, inferred_facts_resolved_type/_algebra_ref/_canonical_witness (now Witness-returning), eval's acceptance witnesses, and the branch/match/loop operand-type reads all refuse a frontier node, typed and located. The branch-operand fallback that returned the operand node as its own type is gone — that was the path by which the fabrication entered arm unification, where "types match" was really "expression nodes are identical".

5. Counted, with a dissolution trigger. Every frontier node emits ^infer_grounding_not_derived on the Accepted path, so the deficit's frequency is observable and prioritizable rather than zeroed by construction (§5). Dissolves kind-by-kind as derivation rules land.

6. The residue is stated, not covered. CanonicalGrounding is a structural record, so a module can still write one field-by-field without the authority. I first added evidence != node to canonical_grounding_admits_infer_facts as a read-path backstop and withdrew it — see below. A witness asserts the residue explicitly rather than leaving the wall's edge to optimism.

solve_constraints itself is untouched. dag/gunbc/plans/solve_higher_order_design.dag names it the structural-solve authority to be extended, never forked; DESIGN already records that it "closes only a singleton scaffold". This PR stops infer from reading a tautology as a derivation; it does not fork or delete the authority.

Witnesses — src/v2/test/claim/infer_self_grounding_wall_test.dag

Eight, green by execution, asserted in both directions:

• construction authority refuses self-evidence / accepts a real derived type;
• the hand-built self-grounding residue is asserted as admitted (the wall's stated edge);
• Conj and Disj groundings are refused where main returned evidence == source;
• a frontier node has no resolved type;
• the frontier is counted on the Accepted path.

Discriminating against main, not merely green: wall_conj_grounding_no_longer_returns_source_as_its_own_type is the direct inverse of a throwaway probe that passed on main (measured, not inferred), and compile_eval_bool_via_compile_entry_refuses_underived_holds inverts a witness that was green on main.

Existing derivation coverage stays green — branch_infer_test (4/4, including the arm-mismatch and cond-not-bool REDs), loop_infer_iteration_test (5/5, including four refusal controls), bind_demand_driven_eval_test (6/6), and the full compile_eval_thesis_proof_test (6/6).

Two witnesses fail under a plain --hermetic claim_batch invocation — auth_declared_but_unwired_witness_keystone_holds and bootstrap_witness_keystone_holds, both no mock_response for operation IsExecutable. Verified by execution to fail identically on pristine a589c5f0179: pre-existing, and an artifact of that harness mode rather than a regression.

Two corrections CI forced, recorded rather than quietly absorbed

The evidence != node backstop was withdrawn. It read as free, but it is a proxy for "was this grounding derived?" — which the NodeGrounding carrier already answers exactly. Proxies are the disease being treated here: algebra_ref_is_grounded is a shape test on the connective, which is exactly why Conj/Disj walked through it. It also false-positived: v2_evaluator's bool fixture uses one atom as both the evaluand and the runtime value's primitive_type, so resolved == algebra there is that fixture's coherent encoding of "this atom denotes Bool", not a fabrication. Keeping the conjunct would have meant rewriting a thesis-proof fixture so a check went green — the inversion DESIGN §5 names explicitly. The wall stays where it is exact.

compile_eval_bool_via_compile_entry_holds now asserts a refusal. It goes through the real infer (the other thesis witnesses supply facts via compile_inferred), and it passed on main only because the fabrication made eval's resolved_type check compare v2_eval_bool_literal_pin against itself — the equality held because both sides were the same node, not because a type was derived. v2 has no derivation rule for TypeNode{Atom}, so it now refuses with ^infer_grounding_not_derived, typed and located; the witness is renamed to say so and carries a dissolution trigger. The compile→eval thesis is unchanged and still proven by compile_eval_bool_reaches_node_value_holds / isolate_t1; what is no longer claimed is that v2 can infer those facts itself.

Finding surfaced, deliberately not fixed here

v2.compiler.translate translate_projection_absent_coerce_from_grounding_or_evidence has two Rejected { diagnostics: _ } arms that discard the diagnostics and fall through to translate_type_fold_init(node) — the refusal is swallowed, uncounted, and translation proceeds structurally. That is a pre-existing §5 absorbing fallback, not introduced here, but this PR makes it more reachable: Conj/Disj used to take the Accepted arm and coerce the source node as its own type, and now take the Rejected arm instead. Strictly less wrong (no fabricated type reaches coercion) but still not a refusal.

Not fixed in this PR because deciding what translate should do for a node with no derived type is its own decision with its own blast radius across the emit corpus, in a load-bearing file. Named here so it is tracked rather than absorbed.

A second finding, surfaced the expensive way

Four CI cycles on this PR failed heal_generated_artifacts with cannot apply Div to Variant and Variant — no file, no line, no string. It read as a semantic consequence of the wall. It was not. It was prose I wrote in this PR:

...which is precisely why TypeNode{Conj}/{Disj} self-groundings walked through it...

inside a data ... : String. {...} in a .dag string literal is an interpolation, so {Conj} and {Disj} parsed as coproduct Variant expressions with the / between them as division. The note compiled clean and failed only when the interpreter reached an operator it could not apply.

Located by execution, not inspection: instrumenting the interpreter's ExprBinOp arm to print its locus gave 04_infer.dag:10694..10697 → line 334. The instrumentation is reverted and is not part of this PR.

Recorded because it is squarely an instance of the class this lane exists to close — statically decidable (the corpus already ships the \{ escape), compiles clean, fails at interpretation, and the diagnostic names neither the file nor the string. Not fixed here; the fix belongs with whoever owns lexer diagnostics, and it is one more entry for the parent's prevalence map.

Scope — what this PR does NOT do

• Target realization is not addressed. The lane's other half — "require target realization before validate_then_compile can return an executable result", ExecutableNode<Target> / BehaviorRealization<Target> — is untouched and still open.
• No derivation rules were added. Nine kinds still have no semantic derivation; this PR makes that state honest and counted rather than fabricated. The frontier is a declared implementation frontier under §7's typed-frontier discipline, not a claim that inference is complete.
• The v1-side lanes (method existence, application contracts, declared-type conformance, primitive realization authority) are separate work.