docs(r3): design-free-consequences — Lane 3 closure deliverable

docs/design-free-consequences.md

@@ -0,0 +1,157 @@
+# Design: Free Consequences
+
+**Status:** PROPOSAL - Lane 3 closure deliverable for
+T-Free-Consequences-Demonstration. This document records the guarantee framing;
+it does not introduce substrate facts, new `TestPredicate` variants, or new lens
+carriers.
+
+**User directive:** "what guarantees does the compiler ACTUALLY provide - i
+expect a small doc/testcases."
+
+The testcase half is the 10-gate suite in
+`src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag` and
+`src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag`. This
+document is the prose half: each consequence below is a structural guarantee
+only when its named lens inputs exist and produce witnesses. If a witness is
+missing, the compiler must fall back to the conservative behavior named by the
+gate; it must not infer a heuristic pass.
+
+The common discipline is `feedback_lenses_not_passes`: analyses are lenses over
+declared substrate physics, not ad hoc compiler passes. `docs/design-db18-workflow-effect-carrier.md`
+rejects deriving workflow shape heuristically inside each lens, and
+`docs/design-db20-lane2-stage2e-parallelism-lens.md` frames parallelism safety
+as operation-algebra physics rather than a lens-body guess.
+
+## 1. Auto-Parallelism
+
+**Lens algebra:** `Lens<Bind-Independence> * Lens<Effect-Commutativity> * Lens<Cost>`.
+
+The compiler may emit a parallel schedule for independent bind sequences only
+when three facts line up:
+
+- `Lens<Bind-Independence>` proves the binds have no dependency edge requiring
+  sequential order;
+- effect/commutativity evidence proves the operations commute or have no
+  observable conflict; and
+- `Lens<Cost>` proves parallelizing the work is meaningful rather than pure
+  ceremony.
+
+This is not a `DimensionReport<C>` consumer. Per the DB-3/DB-20 split, workflow
+parallelism is ordinary lens data rooted in DB-20's `WorkflowParallelismReport`.
+The current first-batch fixture keeps that distinction by using
+`LensOutputEquals` over `auto_parallelism_pending_lens`, with a dissolution
+comment pointing to `src/v3/lenses/parallelism.dag` once the real producer
+lands.
+
+**Testcase anchors:**
+
+- `auto_parallelism_independent_binds_emit_parallel`
+- `auto_parallelism_dependent_binds_emit_sequential`
+- `auto_parallelism_branch_arms_serialize`
+
+The first gate is the positive shape; the second and third are the safety
+shapes. Dependent binds and branch arms remain sequential unless the substrate
+can prove a parallel structure is legal.
+
+## 2. Auto-Loop-Parallelism
+
+**Lens algebra:** `Lens<Iteration-Independence> * Lens<Effect-Commutativity> * Lens<Cost>`.
+
+Loop iteration parallelism follows the same rule as bind parallelism, but the
+independence witness is per-iteration. The default is sequential. Parallel loop
+emission is opt-in through `Lens<Iteration-Independence>` and still needs the
+same effect/commutativity and cost witnesses. There is no heuristic "looks safe"
+loop parallelizer.
+
+This mirrors `Lens<Bind-Independence>` rather than creating a new dimension. The
+second-batch fixture therefore uses the same ordinary `LensOutputEquals` shape
+as auto-parallelism and explicitly keeps `LoopIterationEvidence` out of
+`DimensionReport<C>`. Its current scalar placeholder is intentionally
+mismatched (`0 != 1`), so the gates fail closed while still proving the ordinary
+lens-output path is expressible. The positive loop gate becomes substantive only
+when `src/v3/lenses/parallelism.dag` exposes the real DB-20
+`WorkflowParallelismReport` producer for `Lens<Iteration-Independence>`.
+
+**Testcase anchors:**
+
+- `auto_loop_parallelism_provable_independence_emits_parallel`
+- `auto_loop_parallelism_unproven_falls_back_sequential`
+- `auto_loop_parallelism_dependence_emits_sequential`
+
+Together these define the guarantee: provable iteration independence can emit a
+parallel loop; missing or negative evidence emits sequential code.
+
+## 3. Auto-Memoization
+
+**Lens algebra:** `Lens<Purity> * Lens<Cost>`.
+
+The compiler may memoize repeated work when the work is pure and the cost lens
+shows a useful repeated computation. Purity is load-bearing: a call that reads
+external mutable state, performs I/O, or depends on hidden runtime context is
+not eligible. Cost is also load-bearing: one-shot work does not receive
+memoization scaffolding just because it is pure.
+
+`docs/design-lens-framework.md` locks the `Lens.read` purity invariant:
+`Lens.read` is a pure function of declared `(Dag, Behavior)` inputs and may not
+depend on external mutable state. Runtime memoization of a lens fold is one
+instance of this same free consequence, not a separate "lens framework caching"
+feature.
+
+**Testcase anchors:**
+
+- `auto_memoization_repeated_pure_call_cached`
+- `auto_memoization_no_caching_for_one_shot`
+
+The first-batch fixture keeps these cost-related claims on
+`BinaryDimensionReportEquals` over paired `DimensionReport<C>` aliases, because
+this side of the lane consumes cost-shaped reports.
+
+## 4. Cross-Target Optimization
+
+**Lens algebra:** `Lens<Cost> * LanguageSpec`.
+
+The guarantee is not byte-identical output and not identical syntax across Rust,
+Python, and Go. Each target may choose target-native forms. The guarantee is
+that the cost and semantic relation is structurally preserved through the
+target's `LanguageSpec` facts.
+
+Constant folding is the minimal example: the folded subtree disappears in a
+target-specific way, but the symbolic cost reading changes by the same
+structural amount under each target's realization-cost table. The broader
+`cost_structurally_derived` gate states that emitted target cost is derived from
+the composition of `.dag` algebra-level cost and per-primitive realization cost,
+not runtime measurement or target-specific heuristic policy.
+
+**Testcase anchors:**
+
+- `cross_target_optimization_constant_fold_consistent`
+- `cross_target_optimization_cost_structurally_derived`
+
+Both second-batch gates use `BinaryDimensionReportEquals` because cost is a
+`DimensionReport<C>` consumer.
+
+## 5. Space-Bound CX
+
+Space-bound CX is a reference item in this lane, not a new derivation. The R1
+closure surface assigns the complexity-lens family to R1/T-LaneE authority:
+`ROADMAP.md` names `complexity_merge_sort_is_nlogn`,
+`complexity_merge_sort_v3_matches_v2_oracle`, and
+`lane_e_bundled_witness_host_emit_parity`; `docs/briefs/r1-closure-manager.md`
+records R1 closure by release acceptance; and
+`docs/thesis/r2-r3-thesis-mapping.md` maps "Space bound proofs from CX" to
+R1/T-LaneE complexity-lens gates.
+
+Lane 3 does not re-prove space bounds and does not claim a live space lens.
+`docs/thesis-validation-plan.md` still marks proven space bound per function as
+deferred, and `docs/briefs/r3-v-free-consequences-worker.md` explicitly keeps
+space-bound CX as status/reference only. The actual Lane 3 guarantee is that
+the other free consequences above stay structural and lens-derived; space-bound
+proofs remain governed by their R1/R2 authority until a modeled space lens
+exists.
+
+## Closure Shape
+
+T-Free-Consequences-Demonstration closes only when this document and the
+10-gate suite are both accepted. The gates are not heuristic demos: they pin the
+consumer shapes that must become substantive as the relevant `Lens<C>` producers
+and R2-Evaluator witness construction land.

docs/r3-structure.md

@@ -120,7 +120,7 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine-
 | **T-Bridge-Retirement** | M | **Verification (ledger only); retirement work distributed per bridge map** (Director-locked 2026-04-28: distribute-work-centralize-ledger discipline match — bridges retire in PB/Substrate territory; Verification owns the unified `bridge_retirement_ledger_zero` audit gate) | **Bridge distribution map** (5 named bridges): (1) `SourceSpan.file` participation checks → **Substrate** (typed identity surface); (2) `mark_bootstrap_secret_nominal_opacity()` → **Substrate** (Secret PR A continuation lineage); (3) canonical lens-name dispatch → **PB Manager** (lens-producer-retirement adjacent); (4) `include_str!` side channels (e.g., pipeline_authority.rs) → **PB Manager** (compiler-internal bootstrap); (5) `patch_lower_helpers_*` residual → **PB Manager** (Tier 2 retirement lineage; #1014 was first slice). **Net: 3 Substrate-owned + 3 PB-owned + 1 Verification-owned ledger.** Verification's `bridge_retirement_ledger_zero` audit gate verifies cross-program coordination/reporting cadence; the actual retirement work absorbs into existing Substrate / PB scopes without spawning a parallel manager | R2 substrate carriers (typed identity surfaces); per-bridge gates depend on the natural-owner program's prerequisites |
 | **T-CostLens-Composition** | M | **Substrate Manager (post-R2 continuation)** (Director-locked 2026-04-28: substrate-shape match — T-CostLens-Composition is substrate-authoring of cost facts (per-op algebra cost + per-primitive realization cost) + Lens<SymbolicCost> instance demonstration. Substrate authors; Verification asserts the gate. Different concerns shouldn't fold into one manager.) | Cost lens composes `.dag` algebra-level cost + target-primitive realization cost via the language spec; structural fold, not engine policy. **Instance of `Lens<C>`** (from R2-T-Substrate-Lens-Primitive) with `C = SymbolicCost`. Verifies "coercion cost = complexity" holds by construction. No "coercion cost" dimension. Per Modeling problem 8 in [`docs/design-emission-model.md`](design-emission-model.md). | R2-Evaluator (witness construction for cost claims) + **R2-T-Substrate-Lens-Primitive (the `Lens<C>` shape)** + R2-T-Substrate (per-operation cost on every algebra) + R2-T-Ground-LanguageSpec (per-primitive realization-cost declarations) |
 | **T-V2-Retirement** (NEW 2026-04-30) | S-M | **PB Manager (post-R2 continuation)** | v2 retirement is largely a *consequence* of T-FixedPoint + T-LensProducer-Retirement closing; pulling it into R3 is structurally cheap; the post-R3 framing was coordination convenience, not technical blocker. **Scope:** ~79 `.rs` files + ~32 `.dag` files in `src/v2/`; ~13 v2-using test files; legacy emit chain (`rust_method_template_contracts.dag` header note); dual `verification.dag` convergence (per `design-test-infra.md:14`). **Gates:** `v2_oracle_no_remaining_test_consumers` (no test references `src/v2/`); `v2_directory_deleted` (workspace member removed; bootstrap routes through PB-Runtime trampoline only). Rationale: user directive 2026-04-30 — *"nothing can be deferred past R3."* | T-FixedPoint + T-LensProducer-Retirement |
-| **T-Free-Consequences-Demonstration** (NEW 2026-04-30) | S-M | **Verification Manager** | Operationalizes thesis "free consequences" framing with structural test-claim suite. Per user directive 2026-04-30 — *"what guarantees does the compiler ACTUALLY provide - i expect a small doc/testcases."* **Deliverables:** (1) `docs/design-free-consequences.md` (~1-2 pages) per-consequence guarantee analysis grounded in 5 substrate behaviors + Lens<C> framework. Auto-parallelism = `Lens<Bind-Independence>·Lens<Cost>`; auto-memoization = `Lens<Purity>·Lens<Cost>` (subsumes lens-fold caching as one instance); cross-target opt = `Lens<Cost>·LanguageSpec`; space-bound CX = R1-closed reference. (2) **TestClaim suite (10 gates):** `auto_parallelism_independent_binds_emit_parallel`, `auto_parallelism_dependent_binds_emit_sequential`, `auto_parallelism_branch_arms_serialize`, `auto_loop_parallelism_provable_independence_emits_parallel`, `auto_loop_parallelism_unproven_falls_back_sequential`, `auto_loop_parallelism_dependence_emits_sequential`, `auto_memoization_repeated_pure_call_cached`, `auto_memoization_no_caching_for_one_shot`, `cross_target_optimization_constant_fold_consistent`, `cross_target_optimization_cost_structurally_derived`. **Loop-iteration parallelism design call (Director-ratified 2026-04-30):** sequential default + opt-in via `Lens<Iteration-Independence>` (zero-heuristic; same shape as `Lens<Bind-Independence>`); aligns with `feedback_lenses_not_passes`. | R2-Evaluator (witness construction); R2-T-Substrate-Lens-Primitive (`Lens<C>` shape); T-CostLens-Composition (cost-related claims) |
+| **T-Free-Consequences-Demonstration** (NEW 2026-04-30) | S-M | **Verification Manager** | Operationalizes thesis "free consequences" framing with structural test-claim suite. Per user directive 2026-04-30 — *"what guarantees does the compiler ACTUALLY provide - i expect a small doc/testcases."* **Deliverables:** (1) `docs/design-free-consequences.md` (~1-2 pages) per-consequence guarantee analysis grounded in 5 substrate behaviors + Lens<C> framework. Auto-parallelism = `Lens<Bind-Independence>·Lens<Effect-Commutativity>·Lens<Cost>`; auto-loop-parallelism = `Lens<Iteration-Independence>·Lens<Effect-Commutativity>·Lens<Cost>` (Director-ratified propagation: #828 c#4358522005 from PR #1391); auto-memoization = `Lens<Purity>·Lens<Cost>` (subsumes lens-fold caching as one instance); cross-target opt = `Lens<Cost>·LanguageSpec`; space-bound CX = R1-closed reference. (2) **TestClaim suite (10 gates):** `auto_parallelism_independent_binds_emit_parallel`, `auto_parallelism_dependent_binds_emit_sequential`, `auto_parallelism_branch_arms_serialize`, `auto_loop_parallelism_provable_independence_emits_parallel`, `auto_loop_parallelism_unproven_falls_back_sequential`, `auto_loop_parallelism_dependence_emits_sequential`, `auto_memoization_repeated_pure_call_cached`, `auto_memoization_no_caching_for_one_shot`, `cross_target_optimization_constant_fold_consistent`, `cross_target_optimization_cost_structurally_derived`. **Loop-iteration parallelism design call (Director-ratified 2026-04-30):** sequential default + opt-in via `Lens<Iteration-Independence>` (zero-heuristic; same shape as `Lens<Bind-Independence>`); aligns with `feedback_lenses_not_passes`. | R2-Evaluator (witness construction); R2-T-Substrate-Lens-Primitive (`Lens<C>` shape); T-CostLens-Composition (cost-related claims) |
 
 Critical path: **T-Verification-L4-L7-Direct → T-Verification-L5-Corpus** is the longest because Direct's corpus seeds Corpus's coverage suite. Other lanes parallel-dispatch after R2-Evaluator closes.
 

docs/thesis/r2-r3-thesis-mapping.md

@@ -107,12 +107,16 @@ Per THESIS §"Free consequences (fall out when Tiers 1-2 close)":
 
 | Claim | Disposition | Lane / gate | Evidence | Status |
 |---|---|---|---|---|
-| **Automatic parallelism from dependency graph** | post-R3 ecosystem | not gated on a release; emerges when Tier 1 + Tier 2 fully close | implicit in substrate; no demo lane | 🟡 implicit |
-| **Automatic memoization from purity + cost** | post-R3 ecosystem | same | same | 🟡 implicit |
+| **Automatic parallelism from dependency graph** | R3 | T-Free-Consequences-Demonstration / `auto_parallelism_*` + `auto_loop_parallelism_*` gates | `docs/design-free-consequences.md` + 6 parallelism TestClaims; `Lens<Bind-Independence>` / `Lens<Iteration-Independence>` + `Lens<Effect-Commutativity>` + `Lens<Cost>` | 🟡 R3 |
+| **Automatic memoization from purity + cost** | R3 | T-Free-Consequences-Demonstration / `auto_memoization_*` gates | `docs/design-free-consequences.md` + 2 memoization TestClaims; `Lens<Purity>` + `Lens<Cost>` | 🟡 R3 |
 | **Space bound proofs from CX** | R1 | T-LaneE complexity-lens gates | E-family carrier port | 🟡 R1 closure |
-| **Cross-language optimization from shared cost algebra** | post-R3 ecosystem | falls out when R3 closes; not a release gate | implicit | 🟡 implicit |
+| **Cross-language optimization from shared cost algebra** | R3 | T-Free-Consequences-Demonstration / `cross_target_optimization_*` gates | `docs/design-free-consequences.md` + 2 cross-target optimization TestClaims; `Lens<Cost>` + `LanguageSpec` | 🟡 R3 |
 
-**Note on "free consequences":** these are *consequences*, not gates. The thesis claim is that they fall out *because* Tier 1 + Tier 2 close — they're not separately deliverable. R3's L4-L7 verification harness is the structural test that they actually do fall out (not just claimed-to).
+**Note on "free consequences":** these are *consequences*, but the 2026-04-30
+R3 expansion operationalizes three of them as Lane 3 demonstration deliverables:
+`docs/design-free-consequences.md` plus the 10-gate TestClaim suite named in
+`docs/r3-structure.md`. Space-bound CX remains assigned to R1/T-LaneE authority
+and is referenced, not re-derived, by Lane 3.
 
 ## Disposition table — Omni-emission
 

src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag

@@ -31,10 +31,11 @@ data auto_loop_parallelism_program_input: ProgramInput = {}
 // real DB-20 `WorkflowParallelismReport` producer for `Lens<Iteration-Independence>`.
 // Keep this scalar path out of `DimensionReport<C>`; replace the placeholder
 // lens and expected value together when the structural parallelism producer
-// lands.
+// lands. The mismatch keeps the gate fail-closed while the real producer is
+// pending.
 fn auto_loop_parallelism_pending_lens(_d: Dag) -> Int = 0
 
-data auto_loop_parallelism_pending_expected: Int = 0
+data auto_loop_parallelism_pending_expected: Int = 1
 
 type constant_fold_observed_report = DimensionReport<CrossTargetOptimizationEvidence>
 type constant_fold_expected_report = DimensionReport<CrossTargetOptimizationEvidence>

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

@@ -51,10 +51,10 @@ fn r3_free_consequences_second_batch_reaches_expected_consumer_shapes() {
     for (idx, (result, expected_name)) in results.iter().zip(EXPECTED_CLAIMS).enumerate() {
         assert_eq!(result.claim_name, expected_name);
         if idx < 3 {
-            assert_eq!(
-                result.result,
-                ClaimResult::Pass,
-                "expected {expected_name} to exercise the ordinary loop-parallelism lens path"
+            assert!(
+                matches!(&result.result, ClaimResult::Fail(_)),
+                "expected {expected_name} to fail closed on the pending ordinary loop-parallelism lens, got {:?}",
+                result.result
             );
         } else {
             assert!(