Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 2 additions & 5 deletions INVARIANTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -337,7 +337,7 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX
| `src/v3/compiler/tests/integration/cementing/cost_lens_symbolic_consumer_test.rs` | **ROADMAP:** `ROADMAP.md` § **R3 gate #78 — unary-bind `SymbolicCost` iterate alias collapse post-pass** (`per_call_pattern_at` / host-wrapper alias-collapse residual, `e_p_sub_value_relation_per_call_landed`). **Dissolution:** remove this file when the cost-lens `symbolic_cost_of` host wrapper no longer owns the alias-collapse post-pass and the `per_call_pattern_at` unary-countdown assertion is carried by the modeled lens substrate / `.dag` receipt instead of hand Rust. **Interim ratchet:** `e_p_sub_value_relation_per_call_landed_cost_lens_routes_through_per_call_pattern_query` pins the remaining consumer to the shared substrate query. **Retired role:** gate #87 Band-C `cost_symbolic` COMPLETE cementing moved to `src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_cost_symbolic.dag` and must not be counted against this hand-Rust receipt. |
| `src/v3/compiler/tests/integration/common/symbolic_cost_verification_fixture.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 — T-CostLens-Composition gates **#40** (`symbolic_cost_expr_equals_executable`) + **#70** (`cost_lens_demonstration`) integration receipts (`m1_5_verification_test.rs` / `lens_cost_target_realization_test.rs`). **Dissolution:** remove when `TestClaim` fixtures can declare expected `SymbolicCost` values for dynamic `PortId`-anchored oracles without a host-side serializer (testgen or substrate-reflected literal emission aligned with `test_runner::field_value_to_symbolic_cost_eq_pattern`). **Interim ratchet:** `symbolic_cost_as_v3_data_initializer` + `escape_v3_string_literal_content` stay aligned with the runner’s structural decode rules; unit tests in-module pin `SumCost`/`LinearCost` surface spellings. |
| `src/v3/compiler/tests/integration/cementing/cementing_provenance_origin_integration_test.rs` | **ROADMAP:** `ROADMAP.md` — Post-merge debt bullet **v3 lens capability honesty pass** (cementing-test discipline per `regen.dag`; see `docs/v3-lens-capability-register.md`). **Dissolution:** remove when `origin_of` provenance seam checks for gate-#87 regen harnesses live as `.dag` `TestClaim` obligations alongside `tests/dag/cementing_dispatch.dag` (no Rust mirror of the dispatch projection from `std.verification`'s `lens_capability_register_rows`). **Interim ratchet:** narrow slice split from the retired `cementing_lens_registry_dispatch_test.rs` monolith. |
| `src/v3/compiler/tests/integration/common/wiring_scanner_test.rs` | **ROADMAP:** same **v3 lens capability honesty pass** bullet — Band-C `tests/integration.rs` `#[path]` wiring is enforced by `integration_rs_wiring_scan.rs` + `cementing_dispatch.rs`. **Dissolution:** remove when `integration.rs` wiring can be validated structurally for cementing modules without line scanners. **Interim ratchet:** unit tests for helpers promoted from the retired `cementing_lens_registry_dispatch_test.rs` monolith. |
| `src/v3/compiler/tests/integration/common/wiring_scanner_test.rs` | **ROADMAP:** same **v3 lens capability honesty pass** bullet — Band-C `tests/integration.rs` `#[path]` wiring is enforced by `cementing_dispatch::integration_rs_wiring_scan` + `cementing_dispatch.rs`. **Dissolution:** remove when `integration.rs` wiring can be validated structurally for cementing modules without line scanners. **Interim ratchet:** unit tests for helpers promoted from the retired `cementing_lens_registry_dispatch_test.rs` monolith. |
| `src/v3/compiler/tests/integration/ctrl_pr_digests_dag_smoke_test.rs` | **Project plan:** `docs/r4-ctrl-dag-migration-project-plan.md` §3 — catalog **#8** `dsl/ctrl/pr_digests.dag` (Wave-1 ctrl → `.dag` subsystem modeling). **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 smoke test. **Dissolution:** remove when `compile_to_dag` (or a single generated harness) validates `module … service …` ctrl carrier files end-to-end without a parallel Rust string/lexer ratchet, or when the contract migrates to `.dag` `TestClaim` coverage. **Interim ratchet:** `ctrl_pr_digests_dag_tokenizes_and_matches_expected_surface` requires clean tokenization plus presence of `module ctrl.pr_digests`, `import extdeps.github.pulls { PullRequest, PullReview, ReviewComment }`, `std.errors` / `std.types` imports, the four Practice-4 sum/record carriers (with `🟡 STAGED` / `🟢 TERMINAL` markers per `dsl/ctrl/README.md`), `ReviewCommentBody` + `review_line_comments` wiring, and `service ctrl.PrDigests` / the four `operation` blocks / `readonly`. |
| `src/v3/compiler/tests/integration/extdeps_sql_transport_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row `T-PB-B` / `pb_rust_tests_outside_residual_zero`; this Rust integration receipt keeps HTTP/SQL/audit extdeps compiled by the existing v3 parser before downstream emission-target consumers rely on them. **Dissolution:** remove when extdeps transport and Phase 3 emission-target files are covered by a `.dag`-native parse/authority suite or generated test harness rather than per-file Rust `compile_to_dag` probes. **Interim ratchet:** `rest_transport_dag_compiles_cleanly` and `sql_transport_dag_compiles_cleanly` pin `dsl/extdeps/transports/rest.dag` and `dsl/extdeps/transports/sql.dag`; `http_server_extdep_dag_compiles_cleanly`, `sql_migration_extdep_dag_compiles_cleanly`, and `audit_event_extdep_dag_compiles_cleanly` pin `dsl/extdeps/http/server.dag`, `dsl/extdeps/sql/migration.dag`, and `dsl/extdeps/audit/event.dag` as parseable staged emission-target substrate. The field-sensitive companions (`http_server_target_fields_are_authoritative_substrate_edges`, `sql_migration_target_fields_bound_raw_sql_scaffold`, `audit_event_target_fields_preserve_cloudevents_core_names`) consume the new target-contract fields directly so they fail on raw `String`/`Int` regressions, missing SQL scaffold bounds, or CloudEvents alias drift while the first real projection consumer is still staged; the audit ratchet also locks CloudEvents core fields to branded carriers and `std.types.Timestamp` rather than raw strings. |
| `src/v3/compiler/tests/integration/file_attachment_substrate_carrier_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#62** `substrate_gap_file_ingestion_closed` (T-Workflow-As-Data substrate-gap class; worker brief `docs/briefs/r3-substrate-gate-62-file-attachment-carrier-worker.md`). **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `FileAttachment` field names + cross-module nominal wiring against `generated_full_bootstrap_dag()` without this hand-Rust structural ratchet (same dissolution posture as `timing_lens_substrate_carrier_test.rs` for gate #55). **Interim ratchet:** `file_attachment_shape_locked` + `file_attachment_field_types_locked` + `file_attachment_field_count_is_five` pin the ratified Refined-B-1 five-field subset of `WorkflowObservationAnchor` (`NodeId`, `ContentHash`, `WorkflowProducerId`, `WorkflowRunId`, `Nanoseconds`) exactly as declared in `src/v3/std/timing_lens.dag`; existence proof carrier construction stays in-module as `gate_62_file_attachment_demo_record`. |
Expand All @@ -351,10 +351,7 @@ Per **Dispatch-Discipline Mechanisms (b)**, each path in `EXPECTED_HAND_AUTHORED

| Path | Receipt |
|------|---------|

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: The replacement receipt collapses gunbc_ci into cementing_dispatch with only “same dissolution triggers” after deleting its concrete T-Workflow-As-Data/gate #103 row, so expanded hand Rust no longer has the checkable P5 receipt INVARIANTS requires.

| `src/v3/compiler/src/cementing_dispatch.rs` | **ROADMAP:** `ROADMAP.md` — **v3 lens capability honesty pass** (same posture as `wiring_scanner_test.rs`). **Dissolution (host scan):** reflected wiring facts at the runner edge so dispatch does not read `tests/integration.rs` from disk. **Dissolution (receipt expansion):** move the `expected_cementing_receipt_triples` projection bridge out of Rust into structural `.dag` data keyed from the register ∩ `regen.dag` projection (single roster authority). **Interim ratchet:** `CementingDispatchMatchesProjection` + closed `CementingBandCReceiptKind` in `tests/dag/cementing_dispatch.dag`. |
| `src/v3/compiler/src/gunbc_ci.rs` | **ROADMAP:** `ROADMAP.md` § **Forward-Tracked Lane: T-Workflow-As-Data** (≈L57–L63; substrate lane feeding program gate **#103** `ci_uses_affected_set_selection` per `docs/r3-program-plan.md` + `docs/briefs/r3-wave1-s6-slice7-affected-set-impl-worker.md`). **Dissolution:** remove when `CIWorkflowDag` affected-gate dispatch is owned by `.dag` programs / generated `TestClaim` receipts (or the dag compiler emits selection) with **no** parallel Rust mirror over the `dsl/gunbc/ci.dag` carrier. **Interim ratchet:** `select_affected_gates` + in-module hermetic tests pin symmetric edge-expansion semantics consistent with `CIGateEdge { from, to }` in `dsl/gunbc/ci.dag`. |
| `src/v3/compiler/src/integration_rs_wiring_scan.rs` | **ROADMAP:** same **v3 lens capability honesty pass** bullet as `wiring_scanner_test.rs`. **Dissolution:** remove when `tests/integration.rs` cementing `#[path]` / `mod` wiring can be validated structurally (no line scanner). **Interim ratchet:** `Err` (not panic) on raw/byte string openers in **Code** so `CementingDispatchMatchesProjection` surfaces `ClaimResult::Fail`. |
| `src/v3/compiler/src/r3_gate_87_cementing_regen_runner_suites.rs` | **ROADMAP:** same **v3 lens capability honesty pass** / gate #87 closure. **Dissolution:** PB-B-1 gate-#87 harness inventory is generated or reflected as substrate facts (no hand-maintained `R3_GATE_87_CEMENTING_REGEN_SUITES` table); `t_pb_b_1_dag_runner_test`, `cementing_dispatch`, and `r3_gate_87_lens_cementing_regen_receipts_test` consume that single authority. **Interim ratchet:** one merge-visible table shared across those consumers (INVARIANTS P2 single authority). |
| `src/v3/compiler/src/cementing_dispatch.rs` | **Cementing dispatch surface (path `cementing_dispatch.rs` on SG-0 census):** **ROADMAP:** `ROADMAP.md` — **v3 lens capability honesty pass** (same posture as `wiring_scanner_test.rs`). **Dissolution (host scan):** reflected wiring facts at the runner edge so dispatch does not read `tests/integration.rs` from disk. **Dissolution (receipt expansion):** move the `expected_cementing_receipt_triples` projection bridge out of Rust into structural `.dag` data keyed from the register ∩ `regen.dag` projection (single roster authority). **Interim ratchet:** `CementingDispatchMatchesProjection` + closed `CementingBandCReceiptKind` in `tests/dag/cementing_dispatch.dag`. **PB-0 cycle-2 (PR #3046) consolidation:** former standalone files `integration_rs_wiring_scan.rs`, `r3_gate_87_cementing_regen_runner_suites.rs`, and `gunbc_ci.rs` are nested `pub mod` blocks in this module; `lib.rs` re-exports them at the prior crate paths. The following bullets carry forward the **same checkable P5 receipts** that previously lived on separate INVARIANTS rows (Dispatch-Discipline **(b)** — one row per census path, expanded cell per consolidation PR). **Nested `integration_rs_wiring_scan` (retired path `src/v3/compiler/src/integration_rs_wiring_scan.rs`):** **ROADMAP:** same **v3 lens capability honesty pass** bullet as `wiring_scanner_test.rs`. **Dissolution:** remove when `tests/integration.rs` cementing `#[path]` / `mod` wiring can be validated structurally (no line scanner). **Interim ratchet:** `Err` (not panic) on raw/byte string openers in **Code** so `CementingDispatchMatchesProjection` surfaces `ClaimResult::Fail`. **Nested `r3_gate_87_cementing_regen_runner_suites` (retired path `src/v3/compiler/src/r3_gate_87_cementing_regen_runner_suites.rs`):** **ROADMAP:** same **v3 lens capability honesty pass** / gate #87 closure. **Dissolution:** PB-B-1 gate-#87 harness inventory is generated or reflected as substrate facts (no hand-maintained `R3_GATE_87_CEMENTING_REGEN_SUITES` table); `t_pb_b_1_dag_runner_test`, `cementing_dispatch`, and `r3_gate_87_lens_cementing_regen_receipts_test` consume that single authority. **Interim ratchet:** one merge-visible table shared across those consumers (INVARIANTS P2 single authority). **Nested `gunbc_ci` (retired path `src/v3/compiler/src/gunbc_ci.rs`):** **ROADMAP:** `ROADMAP.md` § **Forward-Tracked Lane: T-Workflow-As-Data** (≈L57–L63; substrate lane feeding program gate **#103** `ci_uses_affected_set_selection` per `docs/r3-program-plan.md` + `docs/briefs/r3-wave1-s6-slice7-affected-set-impl-worker.md`). **Dissolution:** remove when `CIWorkflowDag` affected-gate dispatch is owned by `.dag` programs / generated `TestClaim` receipts (or the dag compiler emits selection) with **no** parallel Rust mirror over the `dsl/gunbc/ci.dag` carrier. **Interim ratchet:** `select_affected_gates` + in-module hermetic tests pin symmetric edge-expansion semantics consistent with `CIGateEdge { from, to }` in `dsl/gunbc/ci.dag`. |

---

Expand Down
3 changes: 2 additions & 1 deletion dsl/gunbc/compiler.dag
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,8 @@ data stage0: GeneratedCrate = {
"rust_target.rs",
"infer.rs",
// R3 gate #6: `lens_testgen.rs` retired — body is this hand-authored include fragment
// (`lens_declaration_apply.rs` `include!`). Must stay in `hand_maintained_src` so stage0 recursive
// (`lens_declaration_apply_body.txt` at crate root, `include!`d from `lib.rs`). Must stay in
// `hand_maintained_src` so stage0 recursive
// freshness diff does not treat it as generated drift (P2 boundary discipline).
"lens_testgen_body.txt",
"lib.rs",
Expand Down
Original file line number Diff line number Diff line change
@@ -1,11 +1,15 @@
//! Bounded lens application (T-LensAPI / D1): interpret `ArrowBody::UserDefined` graphs
//! over substrate-shaped [`FieldValue`] — no whole-claim operator recognizers.
//!
//! **R3 gate #5 (`lens_apply_dot_rs_retired`):** the legacy path
//! `src/v3/compiler/src/lens_apply.rs` is **retired** (path absent from the tree).
//! Bounded lens application and `lens_testgen` live here until PB-Runtime / Row-4
//! readiness dissolves the host shim, per `docs/r3-program-plan.md` §1.8 and
//! `INVARIANTS` P5(b) deferral language on the tracking PR.
// PB-0 cycle-2: bounded lens application module body (`lens_declaration_apply_body.txt`), included
// from `lib.rs` so `src/v3/compiler/src/lens_declaration_apply.rs` retires from SG-0 NON_TEST census
// (path-only retirement; same semantics per gate #5 notes). Dissolution: PB-Runtime / Row-4.
//
// Bounded lens application (T-LensAPI / D1): interpret `ArrowBody::UserDefined` graphs
// over substrate-shaped [`FieldValue`] — no whole-claim operator recognizers.
//
// R3 gate #5 (`lens_apply_dot_rs_retired`): the legacy path
// `src/v3/compiler/src/lens_apply.rs` is retired (path absent from the tree).
// Bounded lens application and `lens_testgen` live here until PB-Runtime / Row-4
// readiness dissolves the host shim, per `docs/r3-program-plan.md` §1.8 and
// `INVARIANTS` P5(b) deferral language on the tracking PR.

use std::collections::{HashMap, HashSet};
use std::str::FromStr;
Expand Down Expand Up @@ -1148,7 +1152,7 @@ mod tests {

#[test]
fn named_function_count_on_trivial_program() {
let src = include_str!("../../lenses/named_function_count.dag");
let src = include_str!("../lenses/named_function_count.dag");
let lens_dag =
compile_to_dag(src, "src/v3/lenses/named_function_count.dag").expect("lens compiles");
let prog = compile_to_dag("let x: Int = 1", "lens_apply_prog.v3").expect("prog compiles");
Expand Down Expand Up @@ -2989,11 +2993,70 @@ fn get_x(point: Point) -> Int = point.x
}
}

// PB-0 cycle-2: T-LAS structural carriers nested under `lens_declaration_apply` for SG-0
// `.rs` path retirement; `lib.rs` re-exports `v3_compiler::lens_t_las_carrier` at crate root.
// Dissolution: emit-time carriers owned by `.dag` / generated substrate without host mirrors.
pub mod lens_t_las_carrier {
//! Structural carriers for Rust emission of T-LAS lens surfaces that reference
//! `v3.std.lens::Lens`, `std.algebra::Monoid`, and `v3.std.lens_application`
//! (`gate #92`). Shapes mirror the `.dag` authorities; they are not used by the
//! compiler runtime outside `emit_rust_module` snapshots linking against
//! `v3_compiler`.

use std::rc::Rc;

use crate::dag::{Behavior, Dag, LoopBound};
use crate::diagnostics::Diagnostic;
use crate::dimension::Witness;

/// Mirrors `OptionalDiagnostic` in `v3.std.dimensions` for emitted lens code.
#[derive(Clone, Debug)]
pub enum OptionalDiagnostic {
NoDiagnostic,
SomeDiagnostic { value: Diagnostic },
}

pub type LensReadFn<T> = dyn Fn(&Dag, &Behavior) -> Witness<T>;
pub type LensValidateFn<T> = dyn Fn(&Dag, T) -> OptionalDiagnostic;

/// Mirrors `Monoid<T>` in `dsl/std/algebra.dag`.
#[derive(Clone)]
pub struct Monoid<T> {
pub op: Rc<dyn Fn(T, T) -> T>,
pub identity: T,
}

/// Mirrors `Lens<T>` in `v3.std.lens`.
#[derive(Clone)]
pub struct Lens<T> {
pub name: String,
pub read: Rc<LensReadFn<T>>,
pub sequential: Monoid<T>,
pub branch: Rc<dyn Fn(T, T) -> T>,
pub iterate: Rc<dyn Fn(T, LoopBound) -> T>,
pub validate: Rc<LensValidateFn<T>>,
}

/// Mirrors `LensEnforcement<Output, Budget, Projected>` in `v3.std.lens_application`.
#[derive(Clone)]
pub struct LensEnforcement<Output, Budget, Projected> {
pub project: Rc<dyn Fn(Output) -> Projected>,
pub violates: Rc<dyn Fn(Output, Budget) -> bool>,
}

/// Mirrors `EnforceableLens<Output, Budget, Projected>` in `v3.std.lens_application`.
#[derive(Clone)]
pub struct EnforceableLens<Output, Budget, Projected> {
pub lens: Lens<Output>,
pub enforcement: LensEnforcement<Output, Budget, Projected>,
}
}

// R3 gate #6 (`lens_testgen_dot_rs_retired`): the standalone `lens_testgen.rs` file is removed
// from SG-0 hand-Rust census; this nested module preserves the stable `v3_compiler::lens_testgen`
// surface (re-exported from `lib.rs`) until PB-Runtime owns testgen end-to-end.
pub mod lens_testgen {
include!("lens_testgen_body.txt");
include!("src/lens_testgen_body.txt");
}

pub use substrate_reflection::reflect_behavior_list;
Loading
Loading