v2 body lowering: an as-cast's target type refuses (type_annotation_not_carried, at T) instead of being dropped

[gunbai-bot]

A cast x as Q in a v2 body was Accepted with Q declared nowhere. Body lowering dropped the cast's target type before resolve (gunbc.recurring_failure_mode as_cast_has_no_lowered_form), which is silent wrongness and forbidden by DESIGN §5. This PR makes body lowering refuse the cast instead: reason body_lowering_reason_type_annotation_not_carried, the one reason #12248 introduced for a type the lowering can't carry, located at the authored target type. It does not model the cast. Carrying it is the named restoration trigger, filed as a child work item under this lane.

What changed

• v2.compiler.body_lowering_fold body_lower_postfix_expr: a postfix chain carrying an as-suffix (dag_grammar_postfix_as_suffix_expr) refuses at its type expression. Every arm below it used to answer the primary or chain and drop the suffix.
• body_lower_arm_operand_resolved_read: a cast is OperandRefRefused at Q, so the operand reader can't answer x as Q with x in arm positions.
• v2.test.claim.body_cast_target_refusal, new. A cast in tail, let value, named call argument, if arm and match arm position each refuses with the exact reason, located at Q. The anchor spells Q and carries no let/=/fn token (btar_refused_at_authored_q). Positive control: the same body without the cast accepts.
• v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal an_as_cast_operand_refuses_at_normalize: re-pointed from operator_operand_unread to type_annotation_not_carried. The postfix is folded before the operator reader sees the operand, so the same file now refuses for the more exact reason. It still refuses at normalize.
• as_cast_has_no_lowered_form rung, updated honestly: below the floor on the value route becomes mitigated on every route. Its evidence cites the new controls.
• The new producers are enrolled in floor_cross_claim_pure_producers_warm, as v2 body lowering: a let type annotation it cannot carry refuses instead of being dropped #12248 did.

Evidence (exact head 168890f88d9; the .dag bodies of the controls and mutant runs are identical to 359e317b233, where they ran)

Local gunbc built from this tree (CARGO_TARGET_DIR=/cargo-target/quick-dove-780), run through a scratch driver that ANDs the claims:

• Controls: 11111111, all green. That's the five cast refusals, uncast-accepts, and v2 body lowering: a let type annotation it cannot carry refuses instead of being dropped #12248's btar_let_annotation_refuses / btar_unannotated_let_accepts. The re-pointed cav witness and its two neighbours (a_parenthesised_call_operand_resolves, a_caret_symbol_operand_refuses_at_normalize) are 111.
• Mutant (restore the drop: body_lower_postfix_cast_target_optional forced Absent): 00011100. All five cast controls go red; uncast-accepts and v2 body lowering: a let type annotation it cannot carry refuses instead of being dropped #12248's two stay green. Same result before and after the merge onto main's OperandRefRead refactor.
• Nothing else of the floor was run locally; CI runs it.

Census: modules that newly refuse (measured)

Instrument: v2.compiler.reference_conservation_census reference_conservation_census_for_paths, over the 321-path population (reference_conservation_stratified_sample_paths plus the six of #12194). Arm pair before 620ecb0a50f / after 4c9f8d326d3, each built and run from its own clone on srv1 (run by neat-boar-16). The after arm's lowering is identical to this head's except for the OperandRefRead merge. 315 of 321 paths measured in both arms; 6 are unmeasured in both, so the diff covers the 315 common paths.

68 newly refuse, 9 have fewer drops, and none changed unmeasured. Each goes from conserved>0, refused=0 to conserved=0, refused=1: every body-lowering refusal is fatal at module grain, so the whole module refuses, not just the cast. Shape, by grep over the 68: 44 have casts only in data rows, dominantly "literal" as NonEmptyStr. 24 have casts in fn bodies, dominantly name as String. Specimen, measured locally on both trees: dag/gunbc/systemctl_status_read.dag goes from refused=0 conserved=41 dropped=15 to refused=1 conserved=0 dropped=97 (unit as String in an argv list).

Required gate: no required claim takes any of the 68 through v2 body lowering.

• Required lanes resolve through the seed's compile_to_resolved (Strict).
• The v2 native route is off the merge path under the declared drop v2_native_route_off_the_merge_path.
• I checked each of the 68 by path and module name against every claim and workflow source. The only v2-route reader is this census itself, an observation. extdeps.uri is read by v2.test.manual.coproduct_reflection_conformance through the host decl_facts_at seam, not body lowering. dag/extdeps/tools/id.dag appears in effect_plan_bash_materialize only as an operation-locus string.
• So this is a loud refusal on an off-gate route, not a §4b(3) drop on a gated one. The 68 were Accepted only because their cast types were dropped.

The 68

• dag/extdeps/cloud/gcp/adc_document.dag
• dag/extdeps/docker/hub.dag
• dag/extdeps/linux/mlx5_core.dag
• dag/extdeps/ollama/gpu_support.dag
• dag/extdeps/tools/id.dag
• dag/gunbc/claim_unwind_seed_growth.dag
• dag/gunbc/closure_edge_demand_seed_growth.dag
• dag/gunbc/cursor_sdk_provider_standing.dag
• dag/gunbc/evaluation_budget_consequence_emit.dag
• dag/gunbc/fabric/fabric_executor_class.dag
• dag/gunbc/floor/floor_cost_debt_edit_seed_growth.dag
• dag/gunbc/git_use_census/roadmap_publication_pull_create.dag
• dag/gunbc/guarantee_stall/external_model_scope_live_cover_stall.dag
• dag/gunbc/instruments/fabric_ci_evidence_projection_fixture.dag
• dag/gunbc/live_deploy/deployed_tree_report.dag
• dag/gunbc/namespace/namespace_structural_observation_bridge_seed_growth.dag
• dag/gunbc/recurring_failure_mode/a_bare_type_name_binds_the_wrong_declaration.dag
• dag/gunbc/recurring_failure_mode/a_control_that_shares_its_derivation_with_its_subject.dag
• dag/gunbc/recurring_failure_mode/a_payload_admits_a_variant_its_producer_never_makes.dag
• dag/gunbc/recurring_failure_mode/a_result_filter_admits_only_anticipated_failures.dag
• dag/gunbc/recurring_failure_mode/ad_hoc_hardware_probe_produces_no_receipt.dag
• dag/gunbc/recurring_failure_mode/an_unreached_entry_body_is_never_typechecked.dag
• dag/gunbc/recurring_failure_mode/binder_renaming_changes_variant_field_lookup.dag
• dag/gunbc/recurring_failure_mode/claim_edit_changes_execution_policy_outside_reported_cost_delta.dag
• dag/gunbc/recurring_failure_mode/constructor_equality_consumes_the_branch_brace.dag
• dag/gunbc/recurring_failure_mode/declared_return_disagrees_with_the_generic_it_returns.dag
• dag/gunbc/recurring_failure_mode/dollar_dollar_in_a_subshell_writes_the_invoking_shell.dag
• dag/gunbc/recurring_failure_mode/enforcement_exhibits_the_shape_it_refuses.dag
• dag/gunbc/recurring_failure_mode/fabric_object_identity_is_a_structural_locator.dag
• dag/gunbc/recurring_failure_mode/git_execution_bypasses_direct_import_policy.dag
• dag/gunbc/recurring_failure_mode/identity_absent_graph_traversal.dag
• dag/gunbc/recurring_failure_mode/kind_carried_but_its_fields_stay_optional.dag
• dag/gunbc/recurring_failure_mode/mandatory_gate_refuses_the_corpus_it_is_mandatory_on.dag
• dag/gunbc/recurring_failure_mode/mistyped_body_radiates_nonlocal_diagnostics.dag
• dag/gunbc/recurring_failure_mode/one_refusal_two_destinations.dag
• dag/gunbc/recurring_failure_mode/prose_repealed_by_the_change_that_wrote_it.dag
• dag/gunbc/recurring_failure_mode/receipt_subject_surface_outlives_its_own_production_time.dag
• dag/gunbc/recurring_failure_mode/repair_job_red_is_attributed_to_the_content_it_repaired.dag
• dag/gunbc/recurring_failure_mode/restored_bytes_reviewed_as_authorship.dag
• dag/gunbc/recurring_failure_mode/shape_predicate_reads_only_the_head_so_a_container_passes_as_its_element.dag
• dag/gunbc/recurring_failure_mode/supervisor_liveness_consumed_as_participation.dag
• dag/gunbc/recurring_failure_mode/transport_mock_success_independent_of_request.dag
• dag/gunbc/recurring_failure_mode/unhandled_state_falls_to_the_not_yet_arm.dag
• dag/gunbc/recurring_failure_mode/verified_candidate_installed_as_a_subset_before_rebuild.dag
• dag/gunbc/required_lane_resolution_census_seed_growth.dag
• dag/gunbc/roadmap/roadmap_site_surface_witness.dag
• dag/gunbc/rung_drop/concat_binary_signature_exempt_from_arg_binding.dag
• dag/gunbc/rung_drop/floor_cost_high_cpu_withheld.dag
• dag/gunbc/rung_drop/heal_healed_head_executed_verdict_without_human.dag
• dag/gunbc/rung_drop/native_lane_closure_walk_unkeyed_membership.dag
• dag/gunbc/rung_drop/source_root_ingest_gate_rung_drop.dag
• dag/gunbc/rung_drop/v2_native_route_off_the_merge_path.dag
• dag/gunbc/runner/runner_registration_labels.dag
• dag/gunbc/spark/pinned_base_env_classification.dag
• dag/gunbc/systemctl_status_read.dag
• dag/test/claim/advertising_interface_witness_test.dag
• dag/test/claim/auth/approval_gate_witness_test.dag
• dag/test/claim/branded_list_first_optional_witness_test.dag
• dag/test/claim/codex_package_delivery_wet_witness_test.dag
• dag/test/claim/fleet/fleet_cap_observation_witness_test.dag
• dag/test/claim/gate_receipt_witness_test.dag
• dag/test/claim/os_install_actuator_selection_witness_test.dag
• dag/test/claim/runner/runner_connectivity_repair_plan_witness_test.dag
• dag/test/claim/runner_jit_admission_witness_test.dag
• dag/test/claim/serving/router_realization_witness_test.dag
• dag/test/claim/spark/spark_secret_access_ensure_witness_test.dag
• dag/test/claim/srv3/srv3_unobservable_probe_refuses_witness_test.dag
• dag/extdeps/uri.dag

Restoration trigger (the capability)

A typed cast node carried through lowering, resolve, infer and translate/eval, under the distinct unauthorable v2.std.type_binder <cast-target> label. It is not <type-annotation>: a cast is a runtime coercion, a let annotation a static ascription, and one label for both would be a §3 meaning fork.

• e as T lowers to Transform[coerce, e] plus <cast-target> -> T.
• Resolve binds T in type role through the shared type-role frame; an undeclared T refuses at T.
• Infer admits the crossing through v2.std.coercion, not std.coercion dag_cast_rules. That table is v1's side of the unjoined fork rostered as coercion_two_algebras_answer_one_question_stall, and this PR doesn't touch the join.
• Translate/eval realize the cast or refuse typed, on every route, returning all 68.
• Needs a coercion CanonicalOperation in v2.std.compilers.target_model plus the v2.std.node PositionalPlusOneNamedEdges rule, which lands with the let-annotation carrier.

🤖 Generated with Claude Code

[gunbai-bot]

emit-build red at 168890f was a real type error in this PR. The self-host emit failed rustc with E0308: OperandRefRefused { diagnostics } wants NonEmptyDiagnostics, and the new arm passed a bare Diagnostic. The interpreter route admitted it, which is why the local controls were green. Fixed at a3d324b by wrapping with diagnostics_singleton, as the neighbouring OperatorExpressionRefused does. Controls re-run locally on a3d324b: 11111111, and the cav trio 111. The mutant result in the body is unchanged by this fix, which touches only the refused arm's diagnostic wrapper. The evidence head is now a3d324b.

[gunbai-bot]

Merge artifacts fixed at b0068bb. floor_pure_producer_share carried #12248's five btar_* rows twice, which review 71387 on #12315 noticed and loyal-crab-333 relayed. It also silently dropped main's wildcard_arm_resolve.wc_outcomes row. The file is now main's plus only the six bctr_* rows, and main is merged in. The PR diff is 5 files: the fold, the new test, the re-pointed cav witness, the RFM row and that roster.

— sent from quick-dove-780

[gunbai-bot]

Closed as superseded by #12315, merged at 696a77d per neat-boar-16's landing ruling. #12315 contained this refusal and retired it in the same squash by carrying the cast as a typed node, so the refusal never needed to land on its own. This PR's census (68 of 315 newly refusing, pair 620ecb0 / 4c9f8d3), its controls and its mutant stay here as the record of the silent drop that #12315 closed.

— sent from quick-dove-780