From 7419a70396acc613d2c065a40fdecf680f556f08 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 14 May 2026 18:04:09 +0000 Subject: [PATCH 1/4] =?UTF-8?q?test(T-LAS):=20CI=20ratchet=20for=20=C2=A71?= =?UTF-8?q?.8=20gate=20#88=20lens=20application=20carriers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Integration tests lock EnforcedApplication (3 typarams, 5 fields) and IntrospectApplication (1 typaram, 3 fields) on generated_full_bootstrap_dag - SG-0: register new hand-authored test module (sorted after t_las_*) - r3-program-plan: note harness on row #88; align row #90 with Projected PR checklist (census net +1): include in PR body verbatim: SG-0 hand-path delta: +1 SG-0 pairing: (c) substrate dispatch receipts docs/briefs/r3-substrate-t-las-demo-complexity-contract-compile-error-worker.md Co-authored-by: Cursor --- docs/r3-program-plan.md | 4 +- src/v3/compiler/tests/integration.rs | 2 + .../tests/integration/sg0_census_test.rs | 3 + .../t_lens_application_carrier_test.rs | 74 +++++++++++++++++++ 4 files changed, 81 insertions(+), 2 deletions(-) create mode 100644 src/v3/compiler/tests/integration/t_lens_application_carrier_test.rs diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 0c60aaa28e2..4859f048e6a 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/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 69c5ad7e6d5..7cbe59b1ccc 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -229,6 +229,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 0f73d914170..f06e5df764c 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -718,6 +718,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" + ); +} From 469dfb27cad20cdea3ba8303b2756e1f16abb615 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 14 May 2026 18:20:16 +0000 Subject: [PATCH 2/4] ci: prepend SG-0 PR-body pairing for census +1 (#3125) PR #3125 edits sg0_census_test.rs (+1 EXPECTED_HAND_AUTHORED_TEST) but the GitHub PR description lacked required SG-0 hand-path delta + pairing, failing the CI job. ci.yml merges scripts/ci-merge/sg0-pr-body-append..txt before the discipline gate. Co-authored-by: Cursor --- scripts/ci-merge/sg0-pr-body-append.3125.txt | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 scripts/ci-merge/sg0-pr-body-append.3125.txt 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..703a2fac1b8 --- /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 gate #88 substrate dispatch receipts docs/briefs/r3-substrate-t-las-demo-complexity-contract-compile-error-worker.md From f02f34ca2ae836808a69f982230f1d25dd33114e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 14 May 2026 18:25:21 +0000 Subject: [PATCH 3/4] docs(INVARIANTS): P5 receipt for t_lens_application_carrier_test (gate #88) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Register the new EXPECTED_HAND_AUTHORED_TEST path in §SG-0 hand-authored integration test receipts per Dispatch-Discipline Mechanism (b). Co-authored-by: Cursor --- INVARIANTS.md | 1 + 1 file changed, 1 insertion(+) diff --git a/INVARIANTS.md b/INVARIANTS.md index 6bf9e09065c..5e79657e0d9 100644 --- a/INVARIANTS.md +++ b/INVARIANTS.md @@ -344,6 +344,7 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX | `src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs` | **ROADMAP:** `ROADMAP.md` — **Tier-3 perf-budget Phase-1 hand-Rust mirror benches** / T-Tier3-Dissolution paired-dispatch (`docs/briefs/r3-pb-t-tier3-consumer-slice-worker.md`). **Plan:** `docs/r3-program-plan.md` §1.8 gate **#2** `tier3_computation_mirror_dissolved` (state-check; **CONSUMER_LANDED** = §1.7 executable-consumer sense, not INVARIANTS §P2 generated-consumer — see plan §1.7 “State-check …” paragraph). **Dissolution:** retire remaining Tier3 host mirrors per `docs/r3-structure.md` §Acceptance as Evaluator-backed std bodies land. **Interim ratchet (P5 Mechanism (b)):** `tier3_computation_mirror_trivial_constructors_dissolved` (PR #2789 narrow slice) + `tier3_computation_mirror_kernel_algebra_profile_substrate_authority` with brace-bounded `dag.rs` scan asserting `type_iteration_dimension` delegates through `BOOTSTRAPPED_DAG.kernel_algebra_profile` (forbid parallel hand-maintained type→profile tables); sibling Tier3 rows in this file carry the same lane receipts. | | `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`) From 60200afb9767d2421a811cf2bff86aa2882755ea Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 14 May 2026 18:40:25 +0000 Subject: [PATCH 4/4] =?UTF-8?q?ci:=20align=20SG-0=20pairing=20#3125=20brie?= =?UTF-8?q?f=20with=20Slice=20A=20gates=20#88=E2=80=93#91?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pairing cited gate #92 demo brief; executor brief r3-v-t-lens-application-surface- execution-split-worker.md owns §1.8 gates #88–#91 incl. lens_application_carrier_landed. Co-authored-by: Cursor --- scripts/ci-merge/sg0-pr-body-append.3125.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/ci-merge/sg0-pr-body-append.3125.txt b/scripts/ci-merge/sg0-pr-body-append.3125.txt index 703a2fac1b8..98558e0147f 100644 --- a/scripts/ci-merge/sg0-pr-body-append.3125.txt +++ b/scripts/ci-merge/sg0-pr-body-append.3125.txt @@ -1,2 +1,2 @@ SG-0 hand-path delta: +1 -SG-0 pairing: (c) T-LAS Slice A gate #88 substrate dispatch receipts docs/briefs/r3-substrate-t-las-demo-complexity-contract-compile-error-worker.md +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)