From ba80a5389cfe1554c1f150634cb894c60e9467b1 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 12 May 2026 20:33:25 +0000 Subject: [PATCH 1/3] T-Tier3-Dissolution gate #2: narrow trivial-constructor mirror retirement MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit R3 §1.8 gate #2 `tier3_computation_mirror_dissolved` advances DECLARED → CONSUMER_LANDED (narrow slice). Retires the two `pub fn` host-Rust mirror entrypoints in `src/v3/compiler/src/dag.rs` `mod computation` whose Rust definition added no information beyond direct variant construction: - `pub fn tree_size_bound(param) -> SizeBound` — trivial constructor for `SizeBound::TreeSize { param }`; sole external caller was the parity ratchet, which now constructs the variant directly. - `pub fn forever_iteration_bound() -> i64` — returned the `i64::MAX` literal; inlined at its single internal call site in `constant_bound_value` (`SizeBound::Forever` → `Some(i64::MAX)`). Mirrors the gate #1 (`termination_lattice_rust_mirror_dissolved`) string ratchet style with a new fail-closed reintroduction guard `tier3_computation_mirror_trivial_constructors_dissolved` in `src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs`, greping the live `dag.rs` source for the retired `pub fn` signatures. `src/v3/std/computation.dag` remains the single authority; the `computation_lowering_functions_preserve_std_body_spans` ratchet keeps the bootstrap body spans for both names pinned at `ArrowBody::Unparsed`. Wider mirror dissolution (`lower_call_pattern`, `type_iteration_dimension`, `size_bound_param`, `is_constant_bound`, `constant_bound_value`, `algebra_profile_to_dimension`) remains lane-tracked under T-Tier3-Dissolution pending evaluated `std.computation` block bodies. Brief: docs/briefs/r3-wave1-pb1-tier3-gate2-computation-mirror-worker.md Authority: docs/r3-structure.md §Acceptance; docs/r3-program-plan.md §1.8 row #2 SG-0 hand-path delta: none (no `sg0_census_test.rs` movement). Perf-budget audit-trail: none (`tier3_mirror_perf.rs` references `lower_call_pattern`/`type_iteration_dimension` only; retired entrypoints were not benched — no `tier3_baseline.json` recapture required per `docs/audit/c1-tier3-baseline-capture-procedure.md`). Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/r3-program-plan.md | 2 +- src/v3/compiler/src/dag.rs | 22 +++++------- .../m2_substrate_inhabitance_test.rs | 36 ++++++++++++++++--- 3 files changed, 41 insertions(+), 19 deletions(-) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index e633b4f023b..379f17c3ab6 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -225,7 +225,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap | # | Gate ID | Family | Owner Lane | Status | Notes | |---|---|---|---|---|---| | 1 | `tier3_termination_mirror_dissolved` | state-check | T-Tier3-Dissolution | **CONSUMER_LANDED + PASSING** (2026-05-12 — public `DescentEvidence` lattice-operation mirror helpers retired from `src/v3/compiler/src/dag.rs`; ratchet `termination_lattice_rust_mirror_dissolved` keeps the Rust mirror dissolved while `src/v3/std/termination.dag` remains the authority; Phase-1 `bench_termination_mirror` registration and frozen baseline row removed) | r3-structure.md §Acceptance | -| 2 | `tier3_computation_mirror_dissolved` | state-check | T-Tier3-Dissolution | DECLARED | r3-structure.md §Acceptance | +| 2 | `tier3_computation_mirror_dissolved` | state-check | T-Tier3-Dissolution | **CONSUMER_LANDED** (2026-05-12 — narrow trivial-constructor slice: `pub fn tree_size_bound` and `pub fn forever_iteration_bound` retired from `src/v3/compiler/src/dag.rs` `mod computation`; ratchet `tier3_computation_mirror_trivial_constructors_dissolved` in `m2_substrate_inhabitance_test.rs` forbids reintroduction; `Forever` constant inlined as `i64::MAX` in `constant_bound_value`. Wider mirror dissolution — `lower_call_pattern`, `type_iteration_dimension`, `size_bound_param`, `is_constant_bound`, `constant_bound_value`, `algebra_profile_to_dimension` — remains pending evaluated `std.computation` block bodies and stays tracked under T-Tier3-Dissolution.) | r3-structure.md §Acceptance | | 3 | `tier3_induction_mirror_dissolved` | state-check | T-Tier3-Dissolution | **CONSUMER_LANDED** (PR #2678 squash 2026-05-11 — merry-wolf-735 T-Tier3 induction mirror retirement; scope-verified per R-7 vs C1 Phase-1 baseline now landed via PR #2702) | r3-structure.md §Acceptance | | 4 | `tier3_effect_carrier_mirror_dissolved` | state-check | T-Tier3-Dissolution | **CONSUMER_LANDED + PASSING** (PR #2679 squash `6897445b` 2026-05-11 — warm-ibex-579 retired `workflow_idempotency.rs`, co-located Lane 2b idempotency projection in `dag/effects.rs` with P5/P2 receipts + bootstrap `ArrowBody::Unparsed` ratchet test) | r3-structure.md §Acceptance | | 5 | `lens_apply_dot_rs_retired` | state-check | T-LensProducer-Retirement | DECLARED | gated on PB-Runtime interpreter-as-data | diff --git a/src/v3/compiler/src/dag.rs b/src/v3/compiler/src/dag.rs index 5c0089fe16a..c6f9a07a294 100644 --- a/src/v3/compiler/src/dag.rs +++ b/src/v3/compiler/src/dag.rs @@ -119,10 +119,6 @@ mod computation { Forever, } - pub fn tree_size_bound(param: String) -> SizeBound { - SizeBound::TreeSize { param } - } - /// 🟡 SCAFFOLD — `CallPattern` coproduct (`docs/modeling-discipline.md` §4). /// /// Authority: `src/v3/std/computation.dag`. Peano shrink payloads are proof-grade (terminal @@ -270,17 +266,16 @@ mod computation { ) } - /// Signed `Int` top iterate count (`i64::MAX`) for [`SizeBound::Forever`] / `repeat(max_int)`. - pub fn forever_iteration_bound() -> i64 { - i64::MAX - } - /// `None` when `bound` is not constant (`ExplicitCount*` / `Forever` only). + /// + /// `Forever` materializes as signed-`Int` top (`i64::MAX`) per `std.computation` + /// `repeat(max_int)`; the prior `forever_iteration_bound()` Rust mirror was retired + /// (Tier3 gate #2 narrow slice — see `tier3_computation_mirror_trivial_constructors_dissolved`). pub fn constant_bound_value(bound: &SizeBound) -> Option { match bound { SizeBound::ExplicitCountZero => Some(0), SizeBound::ExplicitCountPositive { steps } => Some(positive_descent_count(steps)), - SizeBound::Forever => Some(forever_iteration_bound()), + SizeBound::Forever => Some(i64::MAX), _ => None, } } @@ -339,10 +334,9 @@ mod effects; mod ports; pub use computation::{ - algebra_profile_to_dimension, constant_bound_value, forever_iteration_bound, is_constant_bound, - lower_call_pattern, size_bound_param, tree_size_bound, type_iteration_dimension, - AlgebraProfile, CallPattern, IterationDimension, IterationPrimitive, LoweringTarget, - ShrinkFactor, SizeBound, + algebra_profile_to_dimension, constant_bound_value, is_constant_bound, lower_call_pattern, + size_bound_param, type_iteration_dimension, AlgebraProfile, CallPattern, IterationDimension, + IterationPrimitive, LoweringTarget, ShrinkFactor, SizeBound, }; pub use effects::{ diff --git a/src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs b/src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs index b0aebe0313f..036568f9479 100644 --- a/src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs +++ b/src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs @@ -4,9 +4,9 @@ use v3_compiler::compile_to_dag; use v3_compiler::dag::{ algebra_profile_to_dimension, constant_bound_value, is_constant_bound, literal_bits_int, lower_call_pattern, per_call_descent_evidence, per_call_pattern_at, positive_amount_from_i64, - size_bound_param, tree_size_bound, type_iteration_dimension, AlgebraProfile, ArrowBody, - AtomPayload, CallPattern, CardinalityBound, DescentEvidence, FieldMap, FieldValue, Interval, - IntervalWidth, IterationDimension, IterationPrimitive, LoweringTarget, PositiveDescentAmount, + size_bound_param, type_iteration_dimension, AlgebraProfile, ArrowBody, AtomPayload, + CallPattern, CardinalityBound, DescentEvidence, FieldMap, FieldValue, Interval, IntervalWidth, + IterationDimension, IterationPrimitive, LoweringTarget, PositiveDescentAmount, PositiveIntervalWidth, ProportionalDivisor, ShrinkFactor, SizeBound, SubValueRelation, TypeConnective, ValueBody, }; @@ -514,6 +514,32 @@ fn termination_lattice_rust_mirror_dissolved() { } } +#[test] +fn tier3_computation_mirror_trivial_constructors_dissolved() { + // Gate `tier3_computation_mirror_dissolved` (R3 §1.8 gate #2, narrow slice): + // the trivial host-Rust mirror entrypoints for `std.computation` declarations + // whose Rust definition added no information beyond direct variant construction + // (`tree_size_bound` returned `SizeBound::TreeSize { param }`; + // `forever_iteration_bound` returned the `i64::MAX` literal) have been retired + // from `src/v3/compiler/src/dag.rs`. `src/v3/std/computation.dag` remains the + // single authority for these names and their bootstrap body spans stay pinned + // by `computation_lowering_functions_preserve_std_body_spans`. + // + // Wider mirror dissolution (`lower_call_pattern`, `type_iteration_dimension`, + // `size_bound_param`, `is_constant_bound`, `constant_bound_value`, + // `algebra_profile_to_dimension`) requires evaluated `std.computation` block + // bodies and stays tracked in the T-Tier3-Dissolution lane; this ratchet + // forbids only reintroduction of the trivial-constructor mirrors above. + let dag_rs = include_str!("../../src/dag.rs"); + for forbidden in ["pub fn tree_size_bound", "pub fn forever_iteration_bound"] { + assert!( + !dag_rs.contains(forbidden), + "`dag.rs` must not export trivial `std.computation` mirror helper `{forbidden}`; \ + `src/v3/std/computation.dag` is the authority (R3 gate #2 narrow slice)" + ); + } +} + #[test] fn e_p_per_call_descent_evidence_side_table_reads_recursive_call() { let dag = compile_to_dag( @@ -1740,7 +1766,9 @@ fn computation_lowering_rust_mirror_matches_dag_authority() { #[test] fn computation_size_bound_helpers_match_dag_authority() { - let tree = tree_size_bound(String::from("node")); + let tree = SizeBound::TreeSize { + param: String::from("node"), + }; let collection = SizeBound::CollectionSize { param: String::from("items"), }; From cef134aa5d638aef2248b930450c975a65080586 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 12 May 2026 20:47:01 +0000 Subject: [PATCH 2/3] =?UTF-8?q?docs(r3):=20sweep=20=C2=A71.7=20Status-at-H?= =?UTF-8?q?EAD=20paragraph=20=E2=80=94=20tier3=20mirror=20gates=20no=20lon?= =?UTF-8?q?ger=20uniformly=20DECLARED?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex non-blocking review on PR #2789 flagged the §1.7 paragraph at `docs/r3-program-plan.md:144` still asserting `tier3_*_mirror_dissolved` gates "remain DECLARED at HEAD" while §1.8 row-level Status has advanced: - #1 (`tier3_termination_mirror_dissolved`) — CONSUMER_LANDED + PASSING - #4 (`tier3_effect_carrier_mirror_dissolved`) — CONSUMER_LANDED + PASSING - #3 (`tier3_induction_mirror_dissolved`) — CONSUMER_LANDED - #2 (`tier3_computation_mirror_dissolved`) — CONSUMER_LANDED (this PR, narrow trivial-constructor slice) Replace the stale uniform-DECLARED claim with the per-row Status summary and reaffirm the §1.8 ledger as the home-of-record. No gate semantics change; doc consistency sweep only. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/r3-program-plan.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 379f17c3ab6..7e07b5db597 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -141,7 +141,7 @@ Per openai-pro meta-review on PR #1808 sha `cf249389` ([#issuecomment-4384405832 **INVARIANTS §P2 vs this taxonomy:** Where a gate’s Pass condition is **substrate boundary discipline** (“landed” only when declaration + realization + **generated** consumer proof exist; INVARIANTS §P2), **CONSUMER_LANDED** in this ledger means that **generated** bar — a hand-written integration ratchet alone ratchets **DECLARED** substrate progress without claiming §P2 landed (see §1.8 **#17**). -**Status at HEAD**: per §1.8 canonical ledger Status column — most gates are **DECLARED**; `pb_self_compile_fixed_point` is a canonical CONSUMER_LANDED exemplar (R1 horizon Pass = current `verification.dag` + `test_runner` evaluation). **`method_template_projection_emit_shim_retirement_coherence` (§1.8 #97)**, **`omni_layers_share_one_node_tree` (§1.8 #28)**, and **`anthropic_wire_typed_serde_alignment` (§1.8 #29)** are **CONSUMER_LANDED + PASSING** via the integration tests / ratchets cited in the §1.8 ledger rows. **`numeric_abstract_carriers_landed` (§1.8 #17)** is **DECLARED** — carriers + lowering + hand-written ratchet are landed; **CONSUMER_LANDED** (§P2 sense: generated consumer proof) is **not** claimed until that generator exists. `tier3_*_mirror_dissolved` gates remain **DECLARED** at HEAD (T-Tier3-Dissolution lane work in flight per §3 lane status; consumer count / mirror-symbol count test not yet authored). Per-gate status updates flow through §1.8 ledger as Mgrs land consumer infrastructure per their lane scope; all 16 NEW gates added 2026-05-06 in PR #1808 are DECLARED-only. +**Status at HEAD**: per §1.8 canonical ledger Status column — most gates are **DECLARED**; `pb_self_compile_fixed_point` is a canonical CONSUMER_LANDED exemplar (R1 horizon Pass = current `verification.dag` + `test_runner` evaluation). **`method_template_projection_emit_shim_retirement_coherence` (§1.8 #97)**, **`omni_layers_share_one_node_tree` (§1.8 #28)**, and **`anthropic_wire_typed_serde_alignment` (§1.8 #29)** are **CONSUMER_LANDED + PASSING** via the integration tests / ratchets cited in the §1.8 ledger rows. **`numeric_abstract_carriers_landed` (§1.8 #17)** is **DECLARED** — carriers + lowering + hand-written ratchet are landed; **CONSUMER_LANDED** (§P2 sense: generated consumer proof) is **not** claimed until that generator exists. `tier3_*_mirror_dissolved` gates are advancing through T-Tier3-Dissolution per §1.8 row-level Status: **#1** `tier3_termination_mirror_dissolved` and **#4** `tier3_effect_carrier_mirror_dissolved` are **CONSUMER_LANDED + PASSING** at HEAD; **#2** `tier3_computation_mirror_dissolved` and **#3** `tier3_induction_mirror_dissolved` are **CONSUMER_LANDED** (narrow-slice receipts per their §1.8 Notes — wider mirror dissolution remains lane-tracked pending evaluated `std.termination` / `std.computation` / `std.induction` block bodies). Per-gate Status flows through the §1.8 ledger as Mgrs land further dissolution slices. Per-gate status updates flow through §1.8 ledger as Mgrs land consumer infrastructure per their lane scope; all 16 NEW gates added 2026-05-06 in PR #1808 are DECLARED-only. **R3 close criteria implies CONSUMER_LANDED for all R3-load-bearing §1.8 gates** (103 enumerated **minus** **#11** canvas-deferred per Director (a)-disposition 2026-05-09 = **102 R3-load-bearing**; #81/#82/#95 carve-promoted-IN-R3 per Director ratification 2026-05-09 c#4412330468; +6 T-WAD FULL R3 gates #98–#103 per Director (b) ledger-sync disposition msg_2a68a4b5 — see §1.5 above): declarations alone don't satisfy `r3_debt_paydown_zero_remaining` or the substrate-gap-class closures or the demonstration principle. Per Brian directive `feedback_no_textual_enforcement_bridges` + Director poke-hole 2026-05-06 finding 1.1 (demo-gate minimum bar) — closure requires runtime-executable verification, not document-level claims. From fcb3f1d555e2c400fff2c6d9c2b7a43f67669c92 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 12 May 2026 20:53:39 +0000 Subject: [PATCH 3/3] =?UTF-8?q?docs(r3):=20qualify=20trailing=20'DECLARED-?= =?UTF-8?q?only'=20clause=20in=20=C2=A71.7=20Status-at-HEAD?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit cursor/composer-2 APPROVE_WITH_COMMENTS on PR #2789 flagged a residual contradiction in the same §1.7 Status-at-HEAD paragraph: after the per-row tier3 mirror-gate summary, the closing clause still read "all 16 NEW gates added 2026-05-06 in PR #1808 are DECLARED-only" which now contradicts the per-row Status it just stated (INVARIANTS P1 "Documentation Describes Live State"). Also collapse the duplicate "Per-gate Status flows…" sentence pair into a single attribution and reaffirm §1.8 as home-of-record. The 16-gates clause is reframed as a point-in-time fact ("were DECLARED-only at that time"), with the ledger named as the authoritative current-Status surface. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/r3-program-plan.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 7e07b5db597..b1cdfeb9618 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -141,7 +141,7 @@ Per openai-pro meta-review on PR #1808 sha `cf249389` ([#issuecomment-4384405832 **INVARIANTS §P2 vs this taxonomy:** Where a gate’s Pass condition is **substrate boundary discipline** (“landed” only when declaration + realization + **generated** consumer proof exist; INVARIANTS §P2), **CONSUMER_LANDED** in this ledger means that **generated** bar — a hand-written integration ratchet alone ratchets **DECLARED** substrate progress without claiming §P2 landed (see §1.8 **#17**). -**Status at HEAD**: per §1.8 canonical ledger Status column — most gates are **DECLARED**; `pb_self_compile_fixed_point` is a canonical CONSUMER_LANDED exemplar (R1 horizon Pass = current `verification.dag` + `test_runner` evaluation). **`method_template_projection_emit_shim_retirement_coherence` (§1.8 #97)**, **`omni_layers_share_one_node_tree` (§1.8 #28)**, and **`anthropic_wire_typed_serde_alignment` (§1.8 #29)** are **CONSUMER_LANDED + PASSING** via the integration tests / ratchets cited in the §1.8 ledger rows. **`numeric_abstract_carriers_landed` (§1.8 #17)** is **DECLARED** — carriers + lowering + hand-written ratchet are landed; **CONSUMER_LANDED** (§P2 sense: generated consumer proof) is **not** claimed until that generator exists. `tier3_*_mirror_dissolved` gates are advancing through T-Tier3-Dissolution per §1.8 row-level Status: **#1** `tier3_termination_mirror_dissolved` and **#4** `tier3_effect_carrier_mirror_dissolved` are **CONSUMER_LANDED + PASSING** at HEAD; **#2** `tier3_computation_mirror_dissolved` and **#3** `tier3_induction_mirror_dissolved` are **CONSUMER_LANDED** (narrow-slice receipts per their §1.8 Notes — wider mirror dissolution remains lane-tracked pending evaluated `std.termination` / `std.computation` / `std.induction` block bodies). Per-gate Status flows through the §1.8 ledger as Mgrs land further dissolution slices. Per-gate status updates flow through §1.8 ledger as Mgrs land consumer infrastructure per their lane scope; all 16 NEW gates added 2026-05-06 in PR #1808 are DECLARED-only. +**Status at HEAD**: per §1.8 canonical ledger Status column — most gates are **DECLARED**; `pb_self_compile_fixed_point` is a canonical CONSUMER_LANDED exemplar (R1 horizon Pass = current `verification.dag` + `test_runner` evaluation). **`method_template_projection_emit_shim_retirement_coherence` (§1.8 #97)**, **`omni_layers_share_one_node_tree` (§1.8 #28)**, and **`anthropic_wire_typed_serde_alignment` (§1.8 #29)** are **CONSUMER_LANDED + PASSING** via the integration tests / ratchets cited in the §1.8 ledger rows. **`numeric_abstract_carriers_landed` (§1.8 #17)** is **DECLARED** — carriers + lowering + hand-written ratchet are landed; **CONSUMER_LANDED** (§P2 sense: generated consumer proof) is **not** claimed until that generator exists. `tier3_*_mirror_dissolved` gates are advancing through T-Tier3-Dissolution per §1.8 row-level Status: **#1** `tier3_termination_mirror_dissolved` and **#4** `tier3_effect_carrier_mirror_dissolved` are **CONSUMER_LANDED + PASSING** at HEAD; **#2** `tier3_computation_mirror_dissolved` and **#3** `tier3_induction_mirror_dissolved` are **CONSUMER_LANDED** (narrow-slice receipts per their §1.8 Notes — wider mirror dissolution remains lane-tracked pending evaluated `std.termination` / `std.computation` / `std.induction` block bodies). Per-gate status updates flow through the §1.8 ledger as Mgrs land consumer infrastructure per their lane scope; the 16 NEW gates added 2026-05-06 in PR #1808 were DECLARED-only at that time — current Status for each row is the §1.8 ledger value, not this paragraph. **R3 close criteria implies CONSUMER_LANDED for all R3-load-bearing §1.8 gates** (103 enumerated **minus** **#11** canvas-deferred per Director (a)-disposition 2026-05-09 = **102 R3-load-bearing**; #81/#82/#95 carve-promoted-IN-R3 per Director ratification 2026-05-09 c#4412330468; +6 T-WAD FULL R3 gates #98–#103 per Director (b) ledger-sync disposition msg_2a68a4b5 — see §1.5 above): declarations alone don't satisfy `r3_debt_paydown_zero_remaining` or the substrate-gap-class closures or the demonstration principle. Per Brian directive `feedback_no_textual_enforcement_bridges` + Director poke-hole 2026-05-06 finding 1.1 (demo-gate minimum bar) — closure requires runtime-executable verification, not document-level claims.