R3 gate #90: lens_enforcement_carrier_landed (T-Lens-Application-Surface)

INVARIANTS.md

@@ -348,6 +348,7 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX
 | `src/v3/compiler/tests/integration/no_coercion_cost_dimension_ratchet_test.rs` | **ROADMAP:** `ROADMAP.md` → `### Nine lanes` → **T-PB-B** / `pb_rust_tests_outside_residual_zero` (SG-0 `EXPECTED_HAND_AUTHORED_TEST` hand-authored integration census; same “Hand-Rust census” partition narrative as `ROADMAP.md` §Nine lanes / T-PB-B row in the lanes table). **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#39** `no_coercion_cost_dimension` (T-CostLens-Composition — host walk over `src/v3/{std,lenses,spec}/**/*.dag` forbidding standalone `CoercionCost` outside `//` comments). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` literal land in the same PR as the ratchet. **Dissolution:** remove when the same structural claim is carried by `.dag` `TestClaim` / generated harness without this host file walk. **Interim ratchet:** `no_coercion_cost_dimension_substrate_dag_has_no_coercion_cost_carrier_token` + `standalone_needle_tests` pin identifier-boundary matching. |
 | `src/v3/compiler/tests/integration/r3_gate_60_phase2_width_nat_parser_test.rs` | **ROADMAP:** `ROADMAP.md` — **`substrate_gap_parser_grammar_closed`** / R3 gate **#60** (Phase 2.1 parser slice: angle-only width nat in `<…>`, `TypeAngleArg` substrate split, `Compose<Algebra, MachineWidth<N>>` lowering with literal phantom width). **Dissolution:** remove when gate #60 parse/lower/routing receipts are carried by `.dag` `TestClaim` / generated harness without this hand-authored `compile_to_dag` + `parse_for_test` module (per `docs/audit/r3-gate-60-decomposition.md` follow-on slices). **Interim ratchet:** `gate_60_phase2_parse_accepts_algebra_angle_width_nat`, `gate_60_phase2_int_64_lowers_to_compose_int_machine_width_literal`, `gate_60_phase2_nat_8_lowers_via_uint_slot`, `gate_60_integer_routing_witness_accepts_literal_nat_machine_width`, `gate_60_bare_numeric_type_is_parse_rejected`, `gate_60_int_disallowed_width_fails_closed_without_malformed_template_args`. |
 | `src/v3/compiler/tests/integration/r3_gate_62_file_ingestion_negative_bridge_audit_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#62** `substrate_gap_file_ingestion_closed` supporting evidence (T-Workflow-As-Data substrate-gap class). **NOT a §Acceptance receipt**: §1.4/§4.3 require a positive `.dag` ingestion-via-`FileAttachment` demonstration, not absence-of-bridge evidence (operator BLOCKING 2026-05-14T19:13:37Z, THESIS/P1 modeling faithfulness). This row is a CI-visible negative-bridge audit only — it ratchets that no `.dag`/`.v3` program body under `dsl/` re-introduces `include_str!` while the workflow-substrate file-ingestion path is built out; program bodies are scanned with `//` line comments, `/* … */` block comments, and `"…"` / `` `…` `` string literals stripped so a doc-comment or label mentioning the bridge name does not trip the audit (`feedback_no_textual_enforcement_bridges`). **ROADMAP:** `ROADMAP.md` → `### Nine lanes` → **T-PB-B** / `pb_rust_tests_outside_residual_zero` — hand-Rust integration test held under the T-PB-B deferral lane until a `.dag` `TestClaim` / PB-B-1 runner can carry the predicate. **Dissolution:** remove when (a) a `.dag` `TestClaim` / PB-B-1 runner receipt asserts the same file-tree audit fail-closed without a host-side filesystem walker, OR (b) the gate flips PASSING via a positive ingestion-via-`FileAttachment` `.dag` program and the carrier-reachability ratchets alone carry the audit. **Interim ratchet:** `r3_gate_62_no_include_str_in_dsl` walks every `.dag`/`.v3` file under `dsl/` and fails with the offending paths if any reintroduce `include_str!` in a program body. |
+| `src/v3/compiler/tests/integration/r3_gate_90_lens_enforcement_carrier_landed_test.rs` | **ROADMAP:** `ROADMAP.md` → `### Nine lanes` → **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **Plan:** `docs/r3-program-plan.md` §1.8 gate **#90** `lens_enforcement_carrier_landed` (T-Lens-Application-Surface Slice B — canonical `LensEnforcement` / `EnforceableLens` **data** rows co-located with complexity (`complexity.dag`), symbolic cost (`cost.dag`), and timing (`timing_lens.dag`); Stage 2e parallelism LAS enforcement deferral honest under gates **#81/#95** / Cluster F sequencing). **Design:** `docs/design-lens-application-surface.md` (parametric carriers in `src/v3/std/lens_application.dag`). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` literal land in the same PR as the harness. **Dissolution:** remove when the same structural obligations (field labels on each bundled enforcement / enforceable pair + authority file co-location) are carried only by `.dag` `TestClaim` / generated runner receipts without this Rust integration harness. **Interim ratchet:** `r3_gate_90_timing_lens_enforcement_carrier_bundle_locked`, `r3_gate_90_complexity_lens_enforcement_carrier_bundle_locked`, and `r3_gate_90_cost_lens_enforcement_carrier_bundle_locked` pin `project`/`violates` on each `*_enforcement` and `lens`/`enforcement` on each `*_enforceable` (one lens authority per test); timing via `generated_full_bootstrap_dag()`, complexity/cost via `cached_compile_to_dag` because `src/v3/lenses/*.dag` stays outside the std bootstrap concat. **Co-receipt:** `scripts/ci-merge/sg0-pr-body-append.3129.txt` prepended in CI for SG-0 net-shrink +1 pairing on this census line. |
 | `src/v3/compiler/tests/integration/symbolic_cost_expr_equals_executable_ratchet_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#40** `symbolic_cost_expr_equals_executable` (T-CostLens-Composition). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + the matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the ratchet. **Dissolution:** remove when the `SymbolicCostExprEquals` executable-wiring invariant is asserted by a `.dag` `TestClaim` / generated harness over `src/v3/compiler/src/test_runner.rs` (or its modeled successor) without this hand-Rust `TestRunner`-driven ratchet — same dissolution posture as adjacent T-CostLens hand-Rust receipts (`m1_5_verification_test.rs` / `lens_cost_target_realization_test.rs` / `common/symbolic_cost_verification_fixture.rs`). **Interim ratchet:** behavior-driven via the `TestRunner` interface — `symbolic_cost_expr_equals_well_shaped_claim_passes_and_never_returns_not_yet_implemented` compiles a minimal `SymbolicCostExprEquals` `TestClaim`, runs it through `TestRunner::run_suite`, and asserts `ClaimResult::Pass` (forbidding both `NotYetImplemented(_)` — the dispatch-fallthrough shell gate #40 ratchets away from — and `Fail(_)` on the well-shaped path). Robust to dispatch reshaping, helper renames, and message-text edits (per codex `TESTING.md` behavior-first guidance). Typed-shape rejection / fail-closed coverage for the dedicated evaluator is covered separately by `m1_5_verification_test.rs::symbolic_cost_expr_equals_fail_closed_*` — not duplicated here. Wider pass + fail-closed receipts for the predicate stay anchored in `m1_5_verification_test.rs::symbolic_cost_expr_equals_{smoke_suite,countdown_demo_suite}_passes` + `symbolic_cost_expr_equals_fail_closed_*`. |
 | `src/v3/compiler/tests/integration/t_gate_106_show_correct_code_diagnostic_coverage_test.rs` | **ROADMAP:** `ROADMAP.md` → `### Nine lanes` → **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **Plan:** `docs/r3-program-plan.md` §1.8 gate **#106** `show_correct_code_diagnostic_coverage` — lanes **T-Tests-As-Data-Completeness** + Substrate canvas (`Correction` sum + mandatory substrate `Diagnostic.correction` at `src/v3/std/diagnostics.dag`; consumer locks over `generated_full_bootstrap_dag()` plus one typed live-correction roundtrip via `compile_to_dag` / `apply_correction_and_reparse`). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` literal land in the same PR as the harness. **Dissolution:** remove when §1.8 row #106 close obligations (substrate carrier checks + diagnostic-class roundtrip audit + zero-`DeferredCorrection` corpus tally per plan) are discharged via `.dag` `TestClaim` / generated harness without this Rust anchor. **Interim ratchet:** `gate_106_correction_*` / `gate_106_diagnostic_record_carries_mandatory_correction_field` / variant payload locks + `gate_106_type_mismatch_live_correction_roundtrip_recompiles_cleanly`. |
 | `src/v3/compiler/tests/integration/t_gate_58_apply_lens_self_application_test.rs` | **ROADMAP:** `ROADMAP.md` → `### Nine lanes` → **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **Plan:** `docs/r3-program-plan.md` §1.8 gate **#58** `apply_lens_self_application_demonstrated` — lane **T-Lens-Self-Application** (`EnforcedApplication<TimingMeasurement, TimingBudget, TimingEnforcementProjected>` bootstrap receipt over `gate_58_apply_lens_self_application_pass` + typed witness `gate_58_modeled_ci_timing_measurement` (`gate_58_ci_workflow_timing_row` with `workflow: modeled_gunbc_ci_workflow`) in `src/v3/std/t_ci_workflow_as_data_demo.dag`). **Dissolution:** remove when a `.dag` `TestClaim` / runner receipt asserts the same `generated_full_bootstrap_dag()` facts (empty bootstrap diagnostics + witness declarations) without this Rust harness. **Interim ratchet:** `apply_lens_self_application_demonstrated_bootstrap_receipt` + `gate_58_modeled_ci_timing_measurement` presence checks. **Co-receipt (same PR, P5 single surface):** expanded `src/v3/compiler/src/enforced_lens_application.rs` timing consumer + `src/v3/compiler/build.rs` default-rank std `STAGED_FILES` ordering from parsed `import v3.std.*` edges (Kahn topo among co-ranked files; single authority with module imports) are documented in `scripts/ci-merge/sg0-pr-body-append.2827.txt` (prepended to the PR body in CI) with explicit ROADMAP rows + dissolution triggers per INVARIANTS §P5 Mechanism **(b)**. |

docs/r3-program-plan.md

@@ -314,7 +314,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 87 | `lens_cementing_test_discipline_complete` | state-check | T-Tests-As-Data-Completeness | **CONSUMER_LANDED + PASSING** — PR #2639 per-`regen.dag` harness inventory + `t_pb_b_1_dag_runner_test::r3_gate_87_cementing_regen_lens_suites_pass_through_runner`; PR #2757 replaces behavior-bearing `Compiles` placeholders with `LensOutputEquals` / `DifferentialEquals` / `SymbolicCostExprEquals` receipts (plus Int projections where full carriers are not yet authorable); helper-only rows (`infer_helpers`, `lower_helpers`, `variant_payload`) remain explicit `Compiles` + paired Rust compile receipts per register **N/A** / partial scopes; `r3_gate_87_lens_cementing_regen_receipts_test` pins behavioral Rust contracts where `.dag` predicates stay intentionally narrower. | **§Acceptance:** `r3-structure.md` §"Acceptance" bullet for this gate names the `regen.dag` `LensRegistryEntry` enumeration surface (co-landed with this PR stack); PR #2639 + #2757 are the executable receipts against that bullet + `TESTING.md` Band-C. **§1.7:** PASSING here means exhaustive coverage of **that** §Acceptance corpus (registry rows), not a partial slice against some larger implicit canon; non-`regen` lenses stay on Band-C / register ratchets outside this gate id. |
 | 88 | `lens_application_carrier_landed` | substrate-shape | T-Lens-Application-Surface | CONSUMER_LANDED (Slice A receipt PR #2145) | EnforcedApplication + IntrospectApplication carriers in `src/v3/std/lens_application.dag`; CI structural ratchet `t_lens_application_carrier_test` (`r3_gate_88_*`) |
 | 89 | `section_ref_substrate_landed` | substrate-shape | T-Lens-Application-Surface | CONSUMER_LANDED (Slice A receipt PR #2145) | SectionRef disjoint sum (DeclarationScope / NodeScope) in `src/v3/std/lens_application.dag` |
-| 90 | `lens_enforcement_carrier_landed` | substrate-shape | T-Lens-Application-Surface | CONSUMER_LANDED (Slice A receipt PR #2145) | parametric `LensEnforcement<Output, Budget, Projected>` + `EnforceableLens<Output, Budget, Projected>` carriers in `src/v3/std/lens_application.dag`; per-lens data instances co-located with each lens land in Slice B |
+| 90 | `lens_enforcement_carrier_landed` | substrate-shape | T-Lens-Application-Surface | **CONSUMER_LANDED + PASSING** — parametric carriers landed PR #2145; Slice B `LensEnforcement` + `EnforceableLens` land for **complexity** (`complexity.dag`), **symbolic cost** (`cost.dag`), **timing** (`timing_lens.dag`); integration `r3_gate_90_lens_enforcement_carrier_landed_test` pins canonical bundle field shapes (full bootstrap for `timing_lens.dag`; standalone compile for `complexity.dag` / `cost.dag`, which are outside the std bootstrap concat). **Deferral (honest):** Stage 2e **parallelism** LAS enforcement (`Lens<ParallelismMode>` + bundled carrier) is blocked on resolver/regen packaging — sibling-module import of `analyze_parallelism` fails inference today and merging packaging into `parallelism.dag` perturbs the walker-only `regen_lens` emit snapshot; pairs with Cluster **F-γ** / gate **#81/#95** sequencing rather than a silent omission. | parametric `LensEnforcement<Output, Budget, Projected>` + `EnforceableLens<Output, Budget, Projected>` in `src/v3/std/lens_application.dag`; per-lens instances co-located with each lens |
 | 91 | `enforce_violation_routing_landed` | structural-fold | T-Lens-Application-Surface | **CONSUMER_LANDED + PASSING** — fold-pass consumer `check_enforced_lens_applications` walks `EnforcedApplication` declarations from `infer`, evaluates landed per-lens `violates` relations for complexity (`complexity_enforceable`) and timing (`timing_enforceable`), and routes budget violations through `EnforcedApplication.diagnostic_severity` via `enforced_violation_diagnostic`. Executable receipts: unit `enforce_violation_routing_landed_routes_error_severity_to_parse_error` pins `DiagnosticSeverity::Error` → `ParseError` routing and fail-closed malformed-severity tests; integration `complexity_violation_compile_error_demonstrated` and gate #58 timing enforcement receipts exercise the fold-pass consumer on lowered `EnforcedApplication` rows. | Enforce-mode violation routing through `DiagnosticSeverity` per design §3 + INVARIANTS C-8 |
 | 92 | `complexity_violation_compile_error_demonstrated` | demonstration | T-Lens-Application-Surface | **CONSUMER_LANDED + PASSING** — original consumer landing PR #2340 (`t_las_complexity_contract_demo.dag` + `t_las_complexity_contract_compile_error_test.rs`); hot-fix #2723 temporarily ignored the cold-CI receipt on 2026-05-12, but the live harness is active again at HEAD. Executable receipt: `cargo test -p v3-compiler --test integration complexity_violation_compile_error_demonstrated` asserts the lowered `EnforcedApplication` routes through `check_enforced_lens_applications` to a `ParseError` at the lens-application span when `complexity_of` exceeds the `ClassConstant` budget. | `EnforcedApplication` + `complexity_enforceable`; `complexity_of` > `ClassLog` ⇒ `ParseError` "lens enforcement violation" |
 | 93 | `crdt_cost_basis_demonstrated` | demonstration | T-Lens-Application-Surface | **CONSUMER_LANDED + PASSING for the interim symbolic-cost / carrier receipt** — gate #93 CRDT receipt materializes `CostBasisDeclaration { subject: DeclarationScope(my_crdt_field), kind: PerWrite, cost: LogCost(crdt_merge_step.replicas), span }` from lowered DAG facts via `try_build_per_write_log_cost_basis_declaration`; integration `t_las_crdt_cost_basis_demo_test.rs` pins the fixture compile, symbolic-cost lens-table `LogCost` witness, subject/span/kind/cost shape, per-op budget-vs-composed workflow distinction, unknown ceiling dominance, and fail-closed no-divide negative case. **Not full §4.2 closure**: authored `.dag` `CostBasisDeclaration` data rows and folding those rows into `compute_symbolic_costs` remain same-gate follow-on debt; parser lowering for surface `apply_lens(cost, …, Enforce { … })` still tracks through gate #91. | CRDT cost basis via apply_lens |