R3 gate #88: lens_application_carrier_landed (T-Lens-Application-Surface)

INVARIANTS.md

@@ -347,6 +347,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/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)**. |
+| `src/v3/compiler/tests/integration/t_lens_application_carrier_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#88** `lens_application_carrier_landed` (**T-Lens-Application-Surface** Slice A; design lock `docs/design-lens-application-surface.md` §2; substrate `src/v3/std/lens_application.dag`). **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 harness; SG-0 census net +1 pairing is mechanically prepended via `scripts/ci-merge/sg0-pr-body-append.3125.txt` in CI (`.github/workflows/ci.yml`). **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `EnforcedApplication` / `IntrospectApplication` template arity and conj field sets on `generated_full_bootstrap_dag()` without this hand-Rust structural ratchet (same dissolution posture as `file_attachment_substrate_carrier_test.rs` / `timing_lens_substrate_carrier_test.rs`). **Interim ratchet:** `r3_gate_88_enforced_application_carrier_shape_locked` + `r3_gate_88_introspect_application_carrier_shape_locked`. |
 
 ### SG-0 hand-authored compiler non-test paths (`EXPECTED_HAND_AUTHORED_NON_TEST`)
 

docs/r3-program-plan.md

@@ -312,9 +312,9 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 85 | `forall_exists_quantifier_substrate_landed` | substrate-shape | T-Tests-As-Data-Completeness | **DECLARED** — Carriers landed: `Quantifier { ForAll, Exists }`, `QuantifiedTestClaim`, `SuiteClaim` in `src/v3/std/verification.dag` via PR #2647 (vivid-dove-106 / #2613 / Cluster M Phase 1a); bootstrap snapshots regenerated by `regen_bootstrap`; `m1_5_verification_test.rs` references the new types as a hand-written integration ratchet. **CONSUMER_LANDED not claimed**: per §1.7 P2 vs taxonomy + row #17 precedent, INVARIANTS §P2 requires a **generated** consumer of the declared surface; SuiteClaim wrapper migration of `TestSuite.claims` (Phase 1 follow-on per design §6 line 344) + V Mgr #87 (#2609) generated/runner consumer must land before CONSUMER_LANDED, then PASSING. | ForAll / Exists quantifier substrate |
 | 86 | `program_generator_carrier_landed` | substrate-shape | T-Tests-As-Data-Completeness | **CONSUMER_LANDED + PASSING** — `ProgramGenerator` + `ProgramShape` carriers landed in `src/v3/std/verification.dag`; generated bootstrap snapshots refreshed by `regen_bootstrap`. **Refined shape PASSING preserved in-place** (PR #3040, merge 7c2936150): `GeneratedFromDag.manifest_entries: List<GeneratedManifestEntry>` (sum-variant `PendingFact | ResolvedFact` per Director msg_3b99a90f) replaces the prior `generated_paths: List<Path>` shape; `t_pb_b_1_dag_runner_test::r1c_d_pb_census_gates_suite_evaluates_through_runner` continues green under the refined carrier. | ProgramGenerator substrate carrier; follow-on quantified-claim consumer wiring remains under #85/#84 |
 | 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` |
+| 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>` + `EnforceableLens<Output, Budget>` 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 (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 |
 | 91 | `enforce_violation_routing_landed` | structural-fold | T-Lens-Application-Surface | DECLARED — substrate routing surface landed PR #2145 (`DiagnosticSeverity = Error` + `EnforcedApplication.diagnostic_severity` + `LensEnforcement.violates`); CONSUMER_LANDED requires the fold-pass consumer per design doc §10 step 2 — deferred to Slice B | 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 (consumer-disabled hot-fix-2026-05-12)** (Original consumer landing: PR #2340 — `t_las_complexity_contract_demo.dag` + `t_las_complexity_contract_compile_error_test.rs`. **2026-05-12 hot-fix housekeeping**: consumer-disabled via PR #2723 `#[ignore]` cut (cold-CI wall-time reduction; gate #92 was 14s wall on cold CI). PASSING evidence preserved in-tree at `t_las_complexity_contract_compile_error_test.rs` under `#[ignore]` marker; re-enables when T-LAS rebuild dispatch lands OnceLock/cached_compile/shared-fixture amortization. Rebuild ownership routing: pending Director surface — no standing T-LAS Mgr seat at present per PB Mgr → Director internal-message dispatch (warm-dove-618 → zesty-bear-812; not a GitHub comment thread) + gunbc#846 operator greenlight + PR #2725 §6 Cluster F ownership-gap.) | `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 |

scripts/ci-merge/sg0-pr-body-append.3125.txt

@@ -0,0 +1,2 @@
+SG-0 hand-path delta: +1
+SG-0 pairing: (c) T-LAS Slice A substrate dispatch tracked docs/briefs/r3-v-t-lens-application-surface-execution-split-worker.md (§Execution slice A — gates #88–#91 incl. lens_application_carrier_landed)

src/v3/compiler/tests/integration.rs

@@ -231,6 +231,8 @@ mod t_impossiblebugs_unenumerated_effects_test;
 mod t_las_complexity_contract_compile_error_test;
 #[path = "integration/t_las_crdt_cost_basis_demo_test.rs"]
 mod t_las_crdt_cost_basis_demo_test;
+#[path = "integration/t_lens_application_carrier_test.rs"]
+mod t_lens_application_carrier_test;
 #[path = "integration/t_pb_b_1_dag_runner_test.rs"]
 mod t_pb_b_1_dag_runner_test;
 #[path = "integration/tc1_substrate_lens_eta_equivalence_deferred_test.rs"]

src/v3/compiler/tests/integration/sg0_census_test.rs

@@ -726,6 +726,9 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[
     "src/v3/compiler/tests/integration/t_impossiblebugs_unenumerated_effects_test.rs",
     "src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs",
     "src/v3/compiler/tests/integration/t_las_crdt_cost_basis_demo_test.rs",
+    // §1.8 gate #88 (`lens_application_carrier_landed`): bootstrap field / arity locks for
+    // `EnforcedApplication` + `IntrospectApplication` in `src/v3/std/lens_application.dag`.
+    "src/v3/compiler/tests/integration/t_lens_application_carrier_test.rs",
     // T-PB-B-1 `tests/dag` runner table; gate #74 + #87 cementing regen suites; R3 Cluster M #84
     // R1C-D/E runner receipts (co-located harness).
     //

src/v3/compiler/tests/integration/t_lens_application_carrier_test.rs

@@ -0,0 +1,74 @@
+//! **Layer:** integration
+//!
+//! §1.8 / R3 gate **`lens_application_carrier_landed` (#88)** — T-Lens-Application-Surface:
+//! `EnforcedApplication<Output, Budget, Projected>` and `IntrospectApplication<Output>` template
+//! declarations in `src/v3/std/lens_application.dag` stay structurally aligned with
+//! `docs/design-lens-application-surface.md` §2 (`../INVARIANTS.md` P2 / practice-5 sibling).
+//!
+//! Companion substrate (gate #89 `SectionRef`, gate #90 `LensEnforcement` / `EnforceableLens`) shares
+//! the same module; this harness pins only the two **top-level application** carriers for #88.
+
+use std::collections::HashSet;
+
+use v3_compiler::dag::{Dag, TypeConnective};
+use v3_compiler::generated_full_bootstrap_dag;
+
+fn conj_field_labels(dag: &Dag, name: &str) -> HashSet<String> {
+    let decl = dag
+        .declaration_by_name(name)
+        .unwrap_or_else(|| panic!("`{name}` missing from full bootstrap"));
+    match &decl.connective {
+        TypeConnective::Conj { children } => children.iter().map(|f| f.label.clone()).collect(),
+        other => panic!("`{name}` is not a Conj: {other:?}"),
+    }
+}
+
+#[test]
+fn r3_gate_88_enforced_application_carrier_shape_locked() {
+    let dag = generated_full_bootstrap_dag();
+    let enforced = dag
+        .declaration_by_name("EnforcedApplication")
+        .expect("EnforcedApplication missing from full bootstrap");
+    assert_eq!(
+        enforced.type_params.len(),
+        3,
+        "EnforcedApplication must carry Output, Budget, Projected parameters"
+    );
+
+    let labels = conj_field_labels(&dag, "EnforcedApplication");
+    let expected: HashSet<&str> = [
+        "enforceable_lens",
+        "section",
+        "budget",
+        "diagnostic_severity",
+        "span",
+    ]
+    .into_iter()
+    .collect();
+    let actual: HashSet<&str> = labels.iter().map(String::as_str).collect();
+    assert_eq!(
+        actual, expected,
+        "EnforcedApplication field set drifted from T-LAS Slice A design doc §2"
+    );
+}
+
+#[test]
+fn r3_gate_88_introspect_application_carrier_shape_locked() {
+    let dag = generated_full_bootstrap_dag();
+    let intro = dag
+        .declaration_by_name("IntrospectApplication")
+        .expect("IntrospectApplication missing from full bootstrap");
+    assert_eq!(
+        intro.type_params.len(),
+        1,
+        "IntrospectApplication must carry a single Output parameter"
+    );
+
+    let labels = conj_field_labels(&dag, "IntrospectApplication");
+    let expected: HashSet<&str> = ["lens", "section", "span"].into_iter().collect();
+    let actual: HashSet<&str> = labels.iter().map(String::as_str).collect();
+    assert_eq!(
+        actual, expected,
+        "IntrospectApplication field set drifted from T-LAS Slice A design doc §2"
+    );
+}