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
4 changes: 2 additions & 2 deletions docs/r3-program-plan.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 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.

Expand Down Expand Up @@ -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 |
Expand Down
22 changes: 8 additions & 14 deletions src/v3/compiler/src/dag.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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<i64> {
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,
}
}
Expand Down Expand Up @@ -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::{
Expand Down
36 changes: 32 additions & 4 deletions src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
};
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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"),
};
Expand Down
Loading