diff --git a/INVARIANTS.md b/INVARIANTS.md index b1e0ab8d95b..78f7e5ebf08 100644 --- a/INVARIANTS.md +++ b/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>` 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` 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`) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 49bb7ae9bed..fe29a83cd78 100644 --- a/docs/r3-program-plan.md +++ b/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` (sum-variant `PendingFact | ResolvedFact` per Director msg_3b99a90f) replaces the prior `generated_paths: List` 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` + `EnforceableLens` 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` + `EnforceableLens` 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 | diff --git a/scripts/ci-merge/sg0-pr-body-append.3125.txt b/scripts/ci-merge/sg0-pr-body-append.3125.txt new file mode 100644 index 00000000000..98558e0147f --- /dev/null +++ b/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) diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 6fee76e5f54..f071a1a442a 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/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"] diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index 20534796500..3f809ce445f 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/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). // diff --git a/src/v3/compiler/tests/integration/t_lens_application_carrier_test.rs b/src/v3/compiler/tests/integration/t_lens_application_carrier_test.rs new file mode 100644 index 00000000000..a361812b256 --- /dev/null +++ b/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` and `IntrospectApplication` 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 { + 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" + ); +}