diff --git a/INVARIANTS.md b/INVARIANTS.md index 4484a9c137f..72477b54ad3 100644 --- a/INVARIANTS.md +++ b/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>` 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` 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)**. | diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 0f1feda93fa..290a9567ccc 100644 --- a/docs/r3-program-plan.md +++ 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` + `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 + 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` + 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` + `EnforceableLens` 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 | diff --git a/docs/v3-lens-capability-register.md b/docs/v3-lens-capability-register.md index 0d31e6affe2..a6ecae5ae58 100644 --- a/docs/v3-lens-capability-register.md +++ b/docs/v3-lens-capability-register.md @@ -38,7 +38,7 @@ A lens is only "done" when **both** axes are at their strongest grade for the sc | Lens | Structural | Behavioral | v2 counterpart | v3 output | What v2 has that v3 drops | |---|---|---|---|---|---| | `complexity.dag` | TERMINAL | COMPLETE | `src/v2/complexity.dag` (5488L) | `v3.std.lookup::Lookup = Miss \| Hit(ComplexitySummary)` per port (generated consumer: `src/v3/compiler/src/lens_cost_generated.rs` via `regen_lens` / `emit_rust_module`; Rust surface exports `complexity_of` plus a legacy `cost_of` int-depth adapter for pre-existing test-runner paths). `ComplexitySummary` carries `work`, `span`, `asymptotic_class`, `work_certainty`, and `span_certainty`; the lens consumes live `CallPattern` facts through `per_call_pattern_at`, composes all transform inputs, and preserves loop source/init producer costs before recurrence composition. | N/A — behavioral-completion substrate landed in #2220: symbolic work/span costs, SizeVariable display names, certainty, asymptotic classification, and recurrence consumption are present; frozen-oracle cementing for the published `ComplexitySummary` carrier is the temporary Rust receipt at `src/v3/compiler/tests/integration/cementing/complexity_lens_behavioral_completion.rs` until `.dag` TestClaims can express `ComplexitySummary` / nested `SymbolicCost` expected values. | -| `cost.dag` | TERMINAL | COMPLETE | v2 `CostExpr` (embedded in `complexity.dag`) | `v3.std.lookup::Lookup = Miss \| Hit(SymbolicCost)` per port (generated consumer: `src/v3/compiler/src/lens_cost_symbolic_generated.rs` via `regen_lens` / `emit_rust_module`; Rust surface re-exports `SymbolicCostLookup` as a type alias for `Lookup`); E-C stages `std.computation::CallPattern` / `LoweringTarget`; E-I stages `std.induction::SubValueRelation` / `CostBound`; E-P provides the side-table `v3_compiler::dag::per_call_descent_evidence` producer and `per_call_pattern_at` query; E-M method carrier parity is closed by structural subsumption. `Dimension` wiring is executable through `v3_compiler::analyze_symbolic_cost_dimension`, which returns `DimensionReport` over the same generated `symbolic_cost_of` authority. **T-CostLens-Composition alpha/epsilon disposition** remains separate: §1.8 gates **#38** `coercion_cost_equals_complexity_by_construction` + **#39** `no_coercion_cost_dimension` are structurally satisfied by construction; gates **#37** / **#40** / **#70** cover target-realization composition and executable predicate/demo receipts outside this target-agnostic abstract-cost lens. | N/A for gate #80 scope — `SizeVariable` carries value identity by `source_port` with presentation-only `display_name`; recursive `CallPattern` consumption, happy-path `DimensionReport::DimensionOk` composition over `symbolic_cost_of`, and same-source frozen projection cementing are pinned by `src/v3/compiler/tests/integration/cementing/cost_lens_symbolic_consumer_test.rs`. Target-specific concrete realization composition remains tracked by T-CostLens-Composition gates #37/#40/#70, not as a behavioral gap in `cost.dag`'s abstract `SymbolicCost` lens. | +| `cost.dag` | TERMINAL | COMPLETE | v2 `CostExpr` (embedded in `complexity.dag`) | `v3.std.lookup::Lookup = Miss \| Hit(SymbolicCost)` per port (generated consumer: `src/v3/compiler/src/cost_symbolic_lens_generated.rs` via `regen_lens` / `emit_rust_module`; Rust surface re-exports `SymbolicCostLookup` as a type alias for `Lookup`); E-C stages `std.computation::CallPattern` / `LoweringTarget`; E-I stages `std.induction::SubValueRelation` / `CostBound`; E-P provides the side-table `v3_compiler::dag::per_call_descent_evidence` producer and `per_call_pattern_at` query; E-M method carrier parity is closed by structural subsumption. `Dimension` wiring is executable through `v3_compiler::analyze_symbolic_cost_dimension`, which returns `DimensionReport` over the same generated `symbolic_cost_of` authority. **T-CostLens-Composition alpha/epsilon disposition** remains separate: §1.8 gates **#38** `coercion_cost_equals_complexity_by_construction` + **#39** `no_coercion_cost_dimension` are structurally satisfied by construction; gates **#37** / **#40** / **#70** cover target-realization composition and executable predicate/demo receipts outside this target-agnostic abstract-cost lens. | N/A for gate #80 scope — `SizeVariable` carries value identity by `source_port` with presentation-only `display_name`; recursive `CallPattern` consumption, happy-path `DimensionReport::DimensionOk` composition over `symbolic_cost_of`, and same-source frozen projection cementing are pinned by `src/v3/compiler/tests/integration/cementing/cost_lens_symbolic_consumer_test.rs`. Target-specific concrete realization composition remains tracked by T-CostLens-Composition gates #37/#40/#70, not as a behavioral gap in `cost.dag`'s abstract `SymbolicCost` lens. | | `cost_target_realization.dag` | TERMINAL | **N/A** | None (v3-native; ε path consumer of `declaration_by_name` substrate accessor introduced by Slice 1a.0 / PR #2194) | Per-category meta-type `Declaration?` resolvers — `type_realization_meta(d)` / `callable_realization_meta(d)` / `operator_realization_meta(d)` / `behavior_realization_meta(d)` / `type_instantiation_realization_meta(d)` / `pattern_realization_meta(d)` (six total, covering all `*Realization` carriers in `src/v3/std/emit_model.dag`) — using `declaration_by_name` for name-keyed lookup. Slice 1a.1 of T-CostLens-Composition follow-on (#2141 ε scope per gunbc#2181 ratification): minimum-viable consumer-proof per INVARIANTS P2 closure of codex BLOCKING surfaced post-merge on Slice 1a.0. Slice 1a.2 adds Rust-side `v3_compiler::realization_cost::RealizationCostTable`, which filters realization declarations by `meta_tag`, requires `ValueBody.Structural.fields`, matches the active `language`, and extracts typed `target` / `op` keys plus `cost: Int`. Generated consumer: `src/v3/compiler/src/lens_cost_target_realization_generated.rs`. | N/A — ε path consumer-evidence-only; not a v2 mirror. ε composition (abstract `SymbolicCost` × per-target realization-cost) deferred to Slice 1a.3+. | | `effect_enumeration.dag` | TERMINAL | **PARTIAL** | None (v3-native) | `EffectEnumerationReport { facts, coverage_gaps, redundant_reads, transaction }` currently derived from `Dag.nodes` / `Behavior` callable-signature shape; generated consumer target: `src/v3/compiler/src/lens_effect_enumeration_generated.rs` via `regen_lens` / `emit_rust_module` | The file carries the F-β.2 Operation/resource-threading design canvas, but the live body still does not consume grounded `Operation` rows or algebra inhabitance witnesses. Gate #87 pins the current structural-effect report shape with `src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_effect_enumeration.dag` plus the Rust receipt in `src/v3/compiler/tests/integration/r3_gate_87_lens_cementing_regen_receipts_test.rs`; behavioral completion remains blocked until the live lens derives effect sets from `Operation.callable` resource threads and classifies kind from declared inhabitance. | | `idempotency.dag` | TERMINAL | **COMPLETE** | None (v3-native) | `WorkflowIdempotencyReport` via `lane2_workflow_at` + `std.effects::lane2_workflow_idempotency_report` | — (behavioral authority for the `WorkflowEffect` walk is `lane2_workflow_idempotency_report` in `src/v3/std/effects.dag`. `workflow_idempotency.rs` is still **parallel staging** for native `Dag` entry — same projection, hand mirror until an explicit dissolution removes it or routes through generated-only code; INVARIANTS P2 cleanup, not “two competing semantics.”) | diff --git a/scripts/ci-merge/sg0-pr-body-append.3129.txt b/scripts/ci-merge/sg0-pr-body-append.3129.txt new file mode 100644 index 00000000000..d6849de5e5a --- /dev/null +++ b/scripts/ci-merge/sg0-pr-body-append.3129.txt @@ -0,0 +1,3 @@ +SG-0 hand-path delta: +1 + +SG-0 pairing: (c) Net add is one `EXPECTED_HAND_AUTHORED_TEST` row for R3 gate #90 (`lens_enforcement_carrier_landed`) integration receipt (`r3_gate_90_lens_enforcement_carrier_landed_test.rs`). Dispatch evidence for T-LAS substrate sequencing: gunbc#3129 (this PR). diff --git a/src/v3/compiler/build.rs b/src/v3/compiler/build.rs index 8a22d46a99b..8a14f47a3dd 100644 --- a/src/v3/compiler/build.rs +++ b/src/v3/compiler/build.rs @@ -675,7 +675,7 @@ fn main() { "src/v3/compiler/src/diagnostics_generated.rs", "src/v3/compiler/src/infer_helpers_generated.rs", "src/v3/compiler/src/complexity_lens_generated.rs", - "src/v3/compiler/src/lens_cost_symbolic_generated.rs", + "src/v3/compiler/src/cost_symbolic_lens_generated.rs", "src/v3/compiler/src/lens_cost_target_realization_generated.rs", "src/v3/compiler/src/lens_effect_enumeration_generated.rs", "src/v3/compiler/src/lens_parallelism_generated.rs", diff --git a/src/v3/compiler/regen.dag b/src/v3/compiler/regen.dag index d7c08d73c11..6c41f2136c0 100644 --- a/src/v3/compiler/regen.dag +++ b/src/v3/compiler/regen.dag @@ -51,7 +51,7 @@ data lens_cost_entry: LensRegistryEntry = { data lens_cost_symbolic_entry: LensRegistryEntry = { name: "cost_symbolic" lens_file: "src/v3/lenses/cost.dag" - generated_file: "src/v3/compiler/src/lens_cost_symbolic_generated.rs" + generated_file: "src/v3/compiler/src/cost_symbolic_lens_generated.rs" } data lens_cost_target_realization_entry: LensRegistryEntry = { diff --git a/src/v3/compiler/src/bootstrap_generated.rs b/src/v3/compiler/src/bootstrap_generated.rs index 2893da78d91..6f73a974adb 100644 --- a/src/v3/compiler/src/bootstrap_generated.rs +++ b/src/v3/compiler/src/bootstrap_generated.rs @@ -65918,7 +65918,7 @@ fn bootstrapped_fixture_dag_declarations() -> Vec { ( "generated_file".to_string(), FieldValue::Literal(LiteralBits::String( - "src/v3/compiler/src/lens_cost_symbolic_generated.rs".to_string(), + "src/v3/compiler/src/cost_symbolic_lens_generated.rs".to_string(), )), ), ], diff --git a/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs b/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs index a8b950d44a6..ceb94d341da 100644 --- a/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs +++ b/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs @@ -44946,7 +44946,7 @@ fn bootstrapped_fixture_without_parse_surface_dag_declarations() -> Vec Lookup, + p1: Behavior, +) -> Witness { + match p0 { + Lookup::Hit(c) => Witness::Inhabits((c).clone()), + Lookup::Miss => Witness::Violates { + reason: String::from("symbolic_cost_of: missing SymbolicCost for behavior result port"), + at: (p1).clone(), + }, + } +} +pub fn cost_lens_read(p0: &Dag, p1: Behavior) -> Witness { + witness_from_symbolic_cost_lookup( + &(symbolic_cost_of(p0, &(behavior_result_port(&p1)))), + (p1).clone(), + ) +} +pub fn cost_lens_sequential_op(p0: SymbolicCost, p1: SymbolicCost) -> SymbolicCost { + sequential((p0).clone(), (p1).clone()) +} +pub fn cost_lens_branch_op(p0: SymbolicCost, p1: SymbolicCost) -> SymbolicCost { + dominant((p0).clone(), (p1).clone()) +} +pub fn cost_lens_iterate_op(p0: SymbolicCost, p1: &LoopBound) -> SymbolicCost { + match p1 { + LoopBound::Cardinality { count: payload } => iterate( + SymbolicCost::LinearCost { + _0: SizeVariable { + source_port: *payload, + display_name: None, + }, + }, + (p0).clone(), + ), + LoopBound::Descent { + cluster: __payload_cluster, + measure: __payload_measure, + } => iterate( + SymbolicCost::LinearCost { + _0: SizeVariable { + source_port: *__payload_measure, + display_name: None, + }, + }, + (p0).clone(), + ), + } +} +pub fn cost_lens_validate(p0: &Dag, p1: &SymbolicCost) -> OptionalDiagnostic { + OptionalDiagnostic::NoDiagnostic +} +pub fn cost_enforcement_project(p0: SymbolicCost) -> SymbolicCost { + p0 +} +pub fn cost_enforcement_violates(p0: SymbolicCost, p1: SymbolicCost) -> bool { + if dominates(&p0, (p1).clone()) { + if dominates(&p1, (p0).clone()) { + (0 == 1) + } else { + (0 == 0) + } + } else { + (0 == 1) + } +} diff --git a/src/v3/compiler/src/dimension.rs b/src/v3/compiler/src/dimension.rs index effad821e6d..5ebb6678644 100644 --- a/src/v3/compiler/src/dimension.rs +++ b/src/v3/compiler/src/dimension.rs @@ -249,7 +249,7 @@ pub fn analyze_symbolic_cost_dimension( /// /// **Lens-spine, not body-evaluator-driven.** This entrypoint does /// **not** depend on `eval_node` / `evaluate_body` at all — the -/// symbolic-cost lens (`lens_cost_symbolic_generated.rs`) walks the +/// symbolic-cost lens (`cost_symbolic_lens_generated.rs`) walks the /// program DAG structurally and produces `SymbolicCostLookup::Hit(cost)` /// for every reachable behavior including `Loop`. Even now that /// `eval_node` dispatches `Behavior::Loop` (E5 landed), this wrapper diff --git a/src/v3/compiler/src/lib.rs b/src/v3/compiler/src/lib.rs index 326f551bea5..a088c146427 100644 --- a/src/v3/compiler/src/lib.rs +++ b/src/v3/compiler/src/lib.rs @@ -4506,7 +4506,7 @@ pub mod lens_cost { /// Symbolic-cost lens (Lane 2 Stage 2d / DB-7). Authority lives in /// `src/v3/lenses/cost.dag`; the Rust projection is auto-emitted -/// into `src/v3/compiler/src/lens_cost_symbolic_generated.rs` and +/// into `src/v3/compiler/src/cost_symbolic_lens_generated.rs` and /// re-exported so callers use `v3_compiler::lens_cost_symbolic::*`. /// /// The `SymbolicCost` + `SizeVariable` carriers live in @@ -4524,13 +4524,18 @@ pub mod lens_cost_symbolic { unused_variables, clippy::clone_on_copy, clippy::collapsible_else_if, - clippy::deref_addrof + clippy::deref_addrof, + clippy::eq_op )] mod generated { use crate::dag::*; use crate::diagnostics::*; + use crate::lens_t_las_carrier::{ + EnforceableLens, Lens, LensEnforcement, Monoid, OptionalDiagnostic, + }; + use crate::Witness; - include!("lens_cost_symbolic_generated.rs"); + include!("cost_symbolic_lens_generated.rs"); } pub use generated::{ @@ -5219,6 +5224,7 @@ pub mod lens_parallelism { generated::loop_iteration_parallel_emission_indicator(dag, workflow_root) } } + // Surface pipeline for this crate (not workspace-root `src/tokenize.rs` / `src/parse.rs`): // `tokenize.dag` → `regen_tokenize` → `tokenize_generated.rs`, // `parse_parser_body.txt` → `regen_parse` → `parse_generated.rs` (`parse` module), diff --git a/src/v3/compiler/tests/dag/t_r1c_d_pb_census_gates.dag b/src/v3/compiler/tests/dag/t_r1c_d_pb_census_gates.dag index 3978070d56a..08da51ad224 100644 --- a/src/v3/compiler/tests/dag/t_r1c_d_pb_census_gates.dag +++ b/src/v3/compiler/tests/dag/t_r1c_d_pb_census_gates.dag @@ -149,7 +149,7 @@ data pb_test_file_generated_from_dag_gate: TestClaim = { PendingFact { output_path: "src/v3/compiler/src/enforced_lens_application_generated.rs" }, PendingFact { output_path: "src/v3/compiler/src/infer_helpers_generated.rs" }, PendingFact { output_path: "src/v3/compiler/src/int_literal_ranges_generated.rs" }, - PendingFact { output_path: "src/v3/compiler/src/lens_cost_symbolic_generated.rs" }, + PendingFact { output_path: "src/v3/compiler/src/cost_symbolic_lens_generated.rs" }, PendingFact { output_path: "src/v3/compiler/src/lens_cost_target_realization_generated.rs" }, PendingFact { output_path: "src/v3/compiler/src/lens_effect_enumeration_generated.rs" }, PendingFact { output_path: "src/v3/compiler/src/lens_parallelism_generated.rs" }, diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index e35505d7850..8b15a4757e4 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -193,6 +193,8 @@ mod r3_gate_60_phase2_width_nat_parser_test; mod r3_gate_62_file_ingestion_negative_bridge_audit_test; #[path = "integration/r3_gate_87_lens_cementing_regen_receipts_test.rs"] mod r3_gate_87_lens_cementing_regen_receipts_test; +#[path = "integration/r3_gate_90_lens_enforcement_carrier_landed_test.rs"] +mod r3_gate_90_lens_enforcement_carrier_landed_test; #[path = "integration/r3_lens_producer_retirement_executable_witness_test.rs"] mod r3_lens_producer_retirement_executable_witness_test; #[path = "integration/r3_pb_runtime_evaluator_corpus_seed_test.rs"] diff --git a/src/v3/compiler/tests/integration/cementing/cost_lens_symbolic_consumer_test.rs b/src/v3/compiler/tests/integration/cementing/cost_lens_symbolic_consumer_test.rs index eeab9c6266e..aecaba75f71 100644 --- a/src/v3/compiler/tests/integration/cementing/cost_lens_symbolic_consumer_test.rs +++ b/src/v3/compiler/tests/integration/cementing/cost_lens_symbolic_consumer_test.rs @@ -1,7 +1,7 @@ //! **Layer:** integration //! //! Band-C cementing for the generated `symbolic_cost_of` consumer in -//! `src/v3/lenses/cost.dag` (`regen_lens` → `lens_cost_symbolic_generated.rs`). +//! `src/v3/lenses/cost.dag` (`regen_lens` → `cost_symbolic_lens_generated.rs`). //! //! Residual gate #78 Rust receipt for the generated symbolic-cost consumer. //! Gate #80 Band-C cementing for `cost_symbolic` now lives in diff --git a/src/v3/compiler/tests/integration/lane2_stage_2d_symbolic_cost_test.rs b/src/v3/compiler/tests/integration/lane2_stage_2d_symbolic_cost_test.rs index b2eaa3346af..04215576432 100644 --- a/src/v3/compiler/tests/integration/lane2_stage_2d_symbolic_cost_test.rs +++ b/src/v3/compiler/tests/integration/lane2_stage_2d_symbolic_cost_test.rs @@ -2,7 +2,7 @@ #![allow(clippy::needless_borrows_for_generic_args)] // // Authority: `src/v3/lenses/cost.dag` (projection: -// `src/v3/compiler/src/lens_cost_symbolic_generated.rs`). +// `src/v3/compiler/src/cost_symbolic_lens_generated.rs`). // // These tests pin the per-Behavior lowering contract DB-7 specifies // — every Behavior variant produces an honest asymptotic bound, and @@ -970,11 +970,11 @@ budgeted_test! { cost_generated_module_matches_checked_in_snapshot, { let fresh = emit_lens_module(); - let checked_in = include_str!("../../src/lens_cost_symbolic_generated.rs"); + let checked_in = include_str!("../../src/cost_symbolic_lens_generated.rs"); assert_eq!( fresh.trim(), checked_in.trim(), - "checked-in `lens_cost_symbolic_generated.rs` is stale; run `cargo run -p v3-compiler --bin regen_lens -- --lens cost_symbolic`" + "checked-in `cost_symbolic_lens_generated.rs` is stale; run `cargo run -p v3-compiler --bin regen_lens -- --lens cost_symbolic`" ); } } diff --git a/src/v3/compiler/tests/integration/r3_gate_90_lens_enforcement_carrier_landed_test.rs b/src/v3/compiler/tests/integration/r3_gate_90_lens_enforcement_carrier_landed_test.rs new file mode 100644 index 00000000000..2416221a760 --- /dev/null +++ b/src/v3/compiler/tests/integration/r3_gate_90_lens_enforcement_carrier_landed_test.rs @@ -0,0 +1,90 @@ +//! **Layer:** integration +//! +//! R3 §1.8 gate #90 (`lens_enforcement_carrier_landed`) — T-Lens-Application-Surface +//! Slice B receipt: canonical `LensEnforcement` + `EnforceableLens` **data** rows +//! co-located with each `Lens` producer where LAS packaging lands today: +//! complexity (`complexity.dag`), symbolic cost (`cost.dag`), timing (`timing_lens.dag`). +//! Stage 2e parallelism (`parallelism.dag`) defers its LAS enforcement packaging — +//! `import lenses.parallelism { analyze_parallelism }` is not yet resolver-clean for a sibling +//! LAS module without merging regen emit paths (tracked with Cluster F #81 / gate #95 sequencing). +//! +//! **Bootstrap vs lens authorities:** `generated_full_bootstrap_dag()` concatenates `src/v3/std` +//! (among others), not `src/v3/lenses/`. `timing_lens.dag` therefore pins against full bootstrap; +//! `complexity.dag` / `cost.dag` are compiled standalone via `cached_compile_to_dag` like other +//! lens-library receipts. + +use crate::common::cached_compile_to_dag; +use v3_compiler::dag::{Dag, ValueBody}; +use v3_compiler::generated_full_bootstrap_dag; + +#[test] +fn r3_gate_90_timing_lens_enforcement_carrier_bundle_locked() { + let boot = generated_full_bootstrap_dag(); + assert_lens_enforcement_bundle(&boot, "timing_lens.dag", "timing_enforcement"); +} + +#[test] +fn r3_gate_90_complexity_lens_enforcement_carrier_bundle_locked() { + let complexity = cached_compile_to_dag( + include_str!("../../../lenses/complexity.dag"), + "src/v3/lenses/complexity.dag", + ); + assert_lens_enforcement_bundle(&complexity, "complexity.dag", "complexity_enforcement"); +} + +#[test] +fn r3_gate_90_cost_lens_enforcement_carrier_bundle_locked() { + let cost = cached_compile_to_dag( + include_str!("../../../lenses/cost.dag"), + "src/v3/lenses/cost.dag", + ); + assert_lens_enforcement_bundle(&cost, "cost.dag", "cost_enforcement"); +} + +fn assert_lens_enforcement_bundle(dag: &Dag, stem_suffix: &str, enforcement: &str) { + let enforce = dag + .declaration_by_name(enforcement) + .unwrap_or_else(|| panic!("DAG missing `{enforcement}` data row")); + assert!( + enforce.span.file.ends_with(stem_suffix), + "`{enforcement}` must remain authored in `*{stem_suffix}`; got {:?}", + enforce.span.file + ); + let fields = match enforce.value_body.as_ref() { + Some(ValueBody::Structural { fields }) => fields, + other => panic!( + "`{enforcement}` must carry a structural `data` body in compiled DAG; got {other:?}" + ), + }; + let labels: Vec<&str> = fields.iter().map(|(l, _)| l.as_str()).collect(); + assert_eq!( + labels, + vec!["project", "violates"], + "`{enforcement}` must instantiate `LensEnforcement` with project + violates" + ); + + let enforceable = enforcement + .strip_suffix("_enforcement") + .unwrap_or(enforcement); + let enforceable = format!("{enforceable}_enforceable"); + let bundle = dag.declaration_by_name(&enforceable).unwrap_or_else(|| { + panic!("DAG missing `{enforceable}` data row (paired with `{enforcement}`)") + }); + assert!( + bundle.span.file.ends_with(stem_suffix), + "`{enforceable}` must remain authored in `*{stem_suffix}`; got {:?}", + bundle.span.file + ); + let bundle_fields = match bundle.value_body.as_ref() { + Some(ValueBody::Structural { fields }) => fields, + other => panic!( + "`{enforceable}` must carry a structural `data` body in compiled DAG; got {other:?}" + ), + }; + let bundle_labels: Vec<&str> = bundle_fields.iter().map(|(l, _)| l.as_str()).collect(); + assert_eq!( + bundle_labels, + vec!["lens", "enforcement"], + "`{enforceable}` must instantiate `EnforceableLens`" + ); +} diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index 8dc4b676d11..ccda0af25cc 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -689,6 +689,9 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[ // paired with `tests/dag/t_r3_gate_87_cementing_regen_*.dag` + `t_pb_b_1_dag_runner_test` // until strict modules can freeze full `LensOutputEquals` carriers (M1(2.8)). "src/v3/compiler/tests/integration/r3_gate_87_lens_cementing_regen_receipts_test.rs", + // R3 gate #90 (`lens_enforcement_carrier_landed`): bootstrap pins per-lens + // `LensEnforcement` / `EnforceableLens` substrate rows (T-LAS Slice B). + "src/v3/compiler/tests/integration/r3_gate_90_lens_enforcement_carrier_landed_test.rs", // R3 gate #66 (`lens_producer_retirement_executable_witness`): focused receipt // that the `.dag` PB census claim executes through `TestRunner` and reports // the live lens-producer residual count while Row-4 / Item 4 retirement diff --git a/src/v3/compiler/tests/integration/sg6_hand_authored_census_test.rs b/src/v3/compiler/tests/integration/sg6_hand_authored_census_test.rs index 17d355eb04c..9f15ad8a6a6 100644 --- a/src/v3/compiler/tests/integration/sg6_hand_authored_census_test.rs +++ b/src/v3/compiler/tests/integration/sg6_hand_authored_census_test.rs @@ -337,7 +337,7 @@ fn sg6_regen_dag_registry_triples_are_pinned() { ( "cost_symbolic", "src/v3/lenses/cost.dag", - "src/v3/compiler/src/lens_cost_symbolic_generated.rs", + "src/v3/compiler/src/cost_symbolic_lens_generated.rs", ), ( "cost_target_realization", diff --git a/src/v3/compiler/tests/integration/t_las_crdt_cost_basis_demo_test.rs b/src/v3/compiler/tests/integration/t_las_crdt_cost_basis_demo_test.rs index 4a7ab1abfc6..2bd0e79f4b0 100644 --- a/src/v3/compiler/tests/integration/t_las_crdt_cost_basis_demo_test.rs +++ b/src/v3/compiler/tests/integration/t_las_crdt_cost_basis_demo_test.rs @@ -24,7 +24,7 @@ //! **`SectionRef::DeclarationScope`** / workflow `DeclarationId`, `PerWrite`, //! **`LogCost(merge_replicas_port)`**, bind **`span`**) **after** verifying that port //! appears in **`LogCost` in [`compute_symbolic_costs`]** (fail-closed vs fabricated basis). -//! The `.dag` carrier remains the type definitions in `lenses.cost` (`lens_cost_symbolic_generated.rs`). +//! The `.dag` carrier remains the type definitions in `lenses.cost` (`cost_symbolic_lens_generated.rs`). //! (2) **Full symbolic-cost lens table** //! ([`compute_symbolic_costs`]): some port still **`Hit`s `LogCost(merge_replicas_port)`** //! from divide lowering inside `crdt_merge_step` — the per-write O(log replicas) diff --git a/src/v3/lenses/cost.dag b/src/v3/lenses/cost.dag index 1d7894351f7..28090a7f800 100644 --- a/src/v3/lenses/cost.dag +++ b/src/v3/lenses/cost.dag @@ -58,13 +58,15 @@ module lenses.cost import std.list { List, empty, fold, cons } import std.substrate { - Dag, Behavior, BranchPath, LoopNode, NodeId, PortId, node, + Dag, Behavior, BranchPath, LoopNode, LoopBound, NodeId, PortId, node, TransformNode, TransformTarget, OperatorKind, ArithmeticOp } import std.algebra { MethodContract, CostShape, + Monoid, SymbolicCost, + dominates, unnamed_size_variable, sequential, iterate, @@ -87,7 +89,9 @@ import std.computation { } import v3.std.lookup { Lookup } import v3.std.substrate { SourceSpan } -import v3.std.lens_application { SectionRef } +import v3.std.dimensions { Witness, OptionalDiagnostic } +import v3.std.lens { Lens } +import v3.std.lens_application { SectionRef, LensEnforcement, EnforceableLens } // Cost-lens-owned user cost basis (T-User-Authored-Cost-Basis-Discipline audit: // `docs/audit/t-user-authored-cost-basis-discipline-worked-examples.md`). @@ -491,6 +495,84 @@ fn lookup_cost(acc: List, port_id: PortId) -> Lookup` + canonical enforcement (gate #90) ── +// +// Thin substrate packaging over the existing `symbolic_cost_of` / +// `compute_symbolic_costs` authority — **no parallel cost algebra**. Composition +// hooks reuse `std.algebra::{sequential,iterate}` / local `dominant` exactly as +// the Behavior fold does; Q-Lens-Target-Context / LoopBound-measure refinements +// remain tracked under gunbc#2175 without blocking enforcement landing. +fn witness_from_symbolic_cost_lookup(s: Lookup, at: Behavior) -> Witness = + match s { + Hit(c) => Inhabits(c) + Miss => + Violates { + reason: "symbolic_cost_of: missing SymbolicCost for behavior result port" + at: at + } + } + +fn cost_lens_read(d: Dag, b: Behavior) -> Witness = + witness_from_symbolic_cost_lookup(symbolic_cost_of(d, behavior_result_port(b)), b) + +fn cost_lens_sequential_op(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost = + sequential(a, b) + +fn cost_lens_branch_op(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost = + dominant(a, b) + +fn cost_lens_iterate_op(body: SymbolicCost, bound: LoopBound) -> SymbolicCost = + match bound { + Cardinality(payload) => + iterate( + LinearCost(unnamed_size_variable(payload.count)), + body + ) + Descent(payload) => + iterate( + LinearCost(unnamed_size_variable(payload.measure)), + body + ) + } + +fn cost_lens_validate(d: Dag, c: SymbolicCost) -> OptionalDiagnostic = + NoDiagnostic + +fn cost_enforcement_project(c: SymbolicCost) -> SymbolicCost = + c + +// Strict excess in the `SymbolicCost` dominance lattice (mirrors +// `complexity_enforcement_violates` orientation vs `asymptotic_dominates`). +fn cost_enforcement_violates(observed: SymbolicCost, declared: SymbolicCost) -> Bool = + if dominates(observed, declared) then + if dominates(declared, observed) then 0 == 1 else 0 == 0 + else + 0 == 1 + +data cost_lens_monoid: Monoid = { + op: cost_lens_sequential_op + identity: ConstantCost(0) +} + +data cost_lens: Lens = { + name: "symbolic_cost" + read: cost_lens_read + sequential: cost_lens_monoid + branch: cost_lens_branch_op + iterate: cost_lens_iterate_op + validate: cost_lens_validate +} + +data cost_enforcement: LensEnforcement = { + project: cost_enforcement_project + violates: cost_enforcement_violates +} + +data cost_enforceable: EnforceableLens = { + lens: cost_lens + enforcement: cost_enforcement +} + // ── T-CostLens-Composition α-narrow disposition (gunb-ai/gunbc#2141) ─ // // **Director-ratified α (narrow)** at gunbc#828 #issuecomment-4400772335 @@ -519,11 +601,10 @@ fn lookup_cost(acc: List, port_id: PortId) -> Lookup` row at HEAD — see the -// "Cost dimension data declaration / forward Lens boundary" section -// below ("do not author `data cost_lens`"); the existing scaffolding -// is the bespoke `compute_symbolic_costs(d: Dag)` Behavior fold, -// NOT a `Lens` instance. +// 1. ~~No `data cost_lens` row~~ — **superseded at HEAD**: T-LAS Slice B +// (`gate #90 lens_enforcement_carrier_landed`) lands `cost_lens` / +// `cost_enforceable` as thin packaging over `symbolic_cost_of` above. +// Target-context / richer iterate semantics remain under gunbc#2175. // 2. `Lens.read: fn(Dag, Behavior) -> Witness` carries no // target-context — Q-Lens-Target-Context PROPOSAL territory. // 3. Behavior→primitive-identity is structurally tractable via @@ -628,4 +709,5 @@ fn lookup_cost(acc: List, port_id: PortId) -> Lookup(m: Map, key: key) -> value? { // `std.substrate` — same split as `SymbolicCost` in `std.algebra`, keeps // this module free of declaration-identity imports); // - `src/v3/compiler/src/complexity_lens_generated.rs` and -// `src/v3/compiler/src/lens_cost_symbolic_generated.rs` — `regen_lens` / +// `src/v3/compiler/src/cost_symbolic_lens_generated.rs` — `regen_lens` / // `emit_rust_module` output; the compiler includes these modules and // pattern-matches `Lookup` at the lens boundary; // - `src/v3/spec/rust.dag` — `rust_lookup_instantiation` projects the carrier