v2: refinement-obligation carrier + discharge after infer; root-first cut of every infer caller

[gunbai-bot]

What

This PR adds a refinement-obligation carrier and a discharge step between infer and everything downstream. It then cuts every infer caller over to the new return type, root-first. This is the carrier-plus-discharge PR ruled by neat-boar-16 for node adhoc-032c89dc-138. It is the first of three:

1. This PR: the carrier, the discharge step, and the caller cut.
2. Grounding PR: where-predicates become declarations that resolve binds to (adhoc-46630399-82b).
3. Producer PR: infer records an obligation for a literal cast into a refinement ("abc" as NonEmptyStr). That flips bcn_cast_into_a_refinement_refuses_at_infer and clears the 44 NonEmptyStr census modules.

• v2.compiler.inferred_tree
  • RefinementObligation { site, application, target }. application is the closed predicate(operand) node, which infer itself infers, because the evaluator needs an inferred fact for every node it evaluates and discharge may not mint one.
  • ObligatedInferredTree { root, facts, obligations }. It has no InferredTree field. InferredTree gains no obligations field.
  • Pre-discharge readers read the obligated form's fields directly; no accessor functions are added.
• v2.compiler.infer: infer now returns Outcome<ObligatedInferredTree>.
• New v2.compiler.refinement_discharge:
  • discharge_refinement_obligations evaluates each obligation through the existing evaluator (v2.compiler.eval, via eval); there is no second evaluator. It maps the result to one of three outcomes and never widens:
    • the evaluator's own true value admits the crossing;
    • any other value refuses refinement_predicate_violated, located at the cast site;
    • an evaluator refusal becomes refinement_obligation_undischargeable, located at the site, with the evaluator's diagnostics carried behind it.
  • Zero obligations re-wrap the tree and evaluate nothing.
  • infer_and_discharge is the pipeline composition that production callers take.
• The dependency direction stays infer → eval. Discharge imports eval, and eval imports infer, so there is no cycle. This was compiled clean from 00_compile, 03_ingest and the discharge module.

No producer yet (a declared frontier, not dangling code)

No producer records an obligation yet, so every tree currently discharges with nothing to evaluate. The carrier is still consumed now: infer's signature produces it, and compile, 03_ingest, the self-host emitters and the workflow stages discharge it. Its named next consumer is the literal-cast producer (PR 3 above).

Rung, stated honestly

The property is that an obligation infer recorded cannot reach emission undischarged. The wall holds only where a consumer's parameter is typed InferredTree:

• Unwrapped: rung 3, on the compile path only.
  • gunbc compile refuses fn f(t: ObligatedInferredTree) -> InferredTree { t } with a blocking TypeMismatch. That is the compile-clean gate's path, and it is how the root-first cut surfaced its refusals: 4 in 00_compile, 15 test files and the production sites.
  • No enrolled fixture. compile_dag_diagnostic_census, which every guarantee-probe fixture runs through, reports 0 TypeMismatch for this bypass and for its green control alike. A fixture there cannot go red, so none is added. The path disagreement has been reported to neat-boar-16.
  • v2 infer does not decide this inhabitance yet. It reports inhabitance_undecidable_formal_unresolved.
• Through Outcome/Optional: silent hole, even on the compile path. Outcome<ObligatedInferredTree> passes as Outcome<InferredTree> with 0 blocking errors. This is the rostered generic-instantiation hole (gunbc.guarantee_probe_corpus floor_generic_instantiation_hole_probe).
• Through .root: not covered. A consumer taking a plain Node can read .root from the obligated form and emit a subtree. The type wall cannot see this. Two test sites did exactly that and now discharge (see dispositions below).
• Hand-built InferredTree fixtures stay legitimate supplied inputs under the DESIGN §3 witness rule. They record no obligation.

So the wall is mitigated by the site-by-site dispositions below, not guaranteed by construction.

Dispositions: all 42 infer call sites, read one by one

The compile refusals were not a complete census. At least 11 sites handed infer's Outcome on through an Outcome<InferredTree> signature and compiled silently, and 2 more read .root and emitted from it. So every site was read.

Discharge (hands the tree on to emit, translate, eval or a gate, so it takes infer_and_discharge):

• Production:
  • v2.compiler.compile (×3)
  • v2.compiler.ingest (×2: the source-model bridge and cross_language_compile)
  • self_host.candidate_generation (×4), self_host.compiler_closure_emit, self_host.closure_emission, self_host.direct_rust_door_fixture
  • workflow.realization_attempt, workflow.dag_acceptance
• Tests that refused:
  • infer_self_grounding_wall (2; its other 3 sites are verdict-only and stay on infer), translate_underived_refusal (3), stage0_production_target
  • inhabitant_neutralization (4), inhabitant_neutralization_e2e_witness (2)
  • ingest_bridge (2), cross_language_add_python_to_typescript (2)
  • infer_atom_grounding_rules (2), infer_product_introduction (2)
  • emit_host_classical_not_ingested_equals_eval (3; its other 2 sites are verdict-only and stay on infer), accumulator_copy_compile_gate, self_host_module_emit_derisk
  • infer_transform_binary_infix_witness and its helpers, pipeline.stage_bridge (3)
• Tests that were silent through Outcome<InferredTree>:
  • loop_infer_iteration, branch_infer, infer_ground_add, infer_emit_compile_anchor, infer_bounded_lattice_completeness_anchor
• Tests that were silent through .root, then emit:
  • rust_module_emission_population, int_literal_form_unwired_located

Pre-discharge read (reads infer's own verdict or facts, never hands the tree on):

• Production: self_host.candidate_generation_stage_verdicts. It records infer's own stage verdict, and its emission path goes through candidate_generation, which discharges.
• Tests:
  • body_cast_node, claim_pipeline.infer_test, parser_completeness_frontier
  • branch_infer_if_then_else, branch_infer_fail_open_audit, match_infer_fail_open_audit
  • data_decl_lowering_grounding, infer_application_argument_inhabitance_witness
  • infer_list_introduction, type_param_binder_frame

Source of truth: v2.compiler.infer itself.

Three test files carry no imports and resolve from the ambient pool: loop_infer_iteration, branch_infer and infer_emit_compile_anchor. They resolve infer_and_discharge the same way they already resolved infer, so adding an import was not needed.

Floor fixes after the first run

• 5 verdict-only sites reverted to infer. My first cut converted whole files mechanically. A site whose Accepted arm binds _ reads only infer's verdict and must not discharge; that is the pre-discharge-read disposition. Affected: infer_self_grounding_wall (3 sites) and emit_host_classical_not_ingested_equals_eval (2 sites, including ingested_classical_not_real_infer_holds, which the first floor run failed on cost).
• v2.test.manual.ingest_bridge ingest_identity_coercion_accepts_source_present_in_authored_roster enrolled expected-red.
  • It is red on main: false at merge base 21f4d0c and at origin/main b1b7aea, same seed, infer_algebra_ref_ungrounded from canonical_grounding_for_node. It is also red with v2 infer: arrow elimination + body/declared-return check; one Int, one Bool value type #12379 applied.
  • This PR's required edit to its file pulled it into the floor's changed-population selection for the first time.
  • Per-row reason and capability trigger are at v2.workflow.floor_expected_red floor_expected_red_chunk_emitted_add_algebra_ref_ungrounded.

Evidence

v2.test.claim.refinement_discharge:

• (1) rdt_an_unevaluable_application_refuses_undischargeable_whatever_its_body. The application is real and inferred by infer.
  • v2 infer leaves a Bool-returning application GroundingNotDerived, so the evaluator refuses it. Discharge reports refinement_obligation_undischargeable at the site for both a true body and a false body.
  • Landing on the same arm for both bodies is the discriminator: it shows discharge is not answering from anything but the evaluator.
• (2) rdt_zero_obligations_discharge_to_the_same_tree. The identity, and today's only cost path.

Frontier. Row (1) flips when infer has an arrow-elimination rule: an application derives its callee's declared return type, with the body checked against it (node adhoc-3fbf72e5-2b4, dispatched). Only then does a where-predicate application ground so that v2.compiler.eval can evaluate it. (Corrected: an earlier statement that infer already derives Int applications was wrong. It derives no application, Int included. Only Int add and casts derive.) At that point a true body admits and a false body refuses refinement_predicate_violated. That is the holds/violated pair the ruling asked for.

The effectful-predicate case is covered by the same arm. With no effect handler bound, the evaluator refuses any effect operation. There is no separate effect analysis here.

Floor cost

Floor cost, before and after. Measured by required-floor run 36279207012 at eefd917 (job 108507699514):

• Whole run: 547 planned, 533 passed, 9 known reds held, 0 failed, 0 over the cost requirement.
  • For comparison, main-based v2 infer: bind a parameter by its enclosing Arrow, so x:Pos as Pos admits #12373's run 36271105114 had 536 planned and 0 over cost.
  • The first run of this PR had 1 over cost. That was a verdict-only site wrongly routed through discharge, reverted above.
• The zero-obligation path, measured directly: rdt_zero_obligations_discharge_to_the_same_tree observed 60 ms CPU against its 302 ms budget, for infer plus discharge of a one-application tree. rdt_an_unevaluable_application_refuses_undischargeable_whatever_its_body observed 91 ms.
• Not available: a paired infer-only vs infer_and_discharge step count for one identity on main and here. The floor logs per-claim steps only for shared-fill claims, and no main run selected the converted claims.
  • Structurally, zero-obligation discharge is one record construction plus one Empty match arm. It performs no evaluation.

🤖 Generated with Claude Code