Skip to content

R3 gate #1: tier3 termination mirror dissolved #2589

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
briansrls wants to merge 1 commit into from
Closed

R3 gate #1: tier3 termination mirror dissolved #2589

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
21 changes: 6 additions & 15 deletions src/v3/compiler/benches/tier3_mirror_perf.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,31 +1,23 @@
//! Phase 1 — hand-Rust Tier-3 mirror timing (C1 perf-budget worker toward
//! `tier3_mirror_dissolution_perf_within_budget`).
//!
//! Maps 1:1 to the four mirror dissolution slices in
//! `docs/briefs/r3-pb-tier3-perf-budget-worker.md` (termination / computation /
//! induction / effect-carrier). See that brief for thresholds (≤2× median,
//! ≤5× p99) and Phase 1 / Phase 2 split.
//! Maps to the remaining mirror dissolution slices in
//! `docs/briefs/r3-pb-tier3-perf-budget-worker.md` (computation /
//! induction / effect-carrier). The termination mirror bench retired with
//! `tier3_termination_mirror_dissolved`.

@briansrls briansrls May 10, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

BLOCKING: Retiring the termination bench before tier3_baseline.json exists makes the relative perf-budget gate unrecoverable per the perf brief STOP condition, so INVARIANTS P2/P5 require keeping the bench until the termination baseline row is captured.

//!
//! **Frozen baseline** (`tier3_baseline.json`, deliverable 0c): not committed by
//! this skeleton. Capture median + p99 (ns) per group on the canonical CI
//! machine after this bench is stable, then commit JSON per the worker brief.

use criterion::{black_box, criterion_group, criterion_main, Criterion};
use v3_compiler::dag::{
lower_call_pattern, merge_evidence, positive_amount_from_i64, positive_descent_count,
type_iteration_dimension, CallPattern, DescentEvidence,
lower_call_pattern, positive_amount_from_i64, positive_descent_count, type_iteration_dimension,
CallPattern,
};
use v3_compiler::dag::{EffectShape, IdempotentShape, OperationEffect, WorkflowEffect};
use v3_compiler::lane2_workflow_idempotency_report;

fn bench_termination_mirror(c: &mut Criterion) {
let a = DescentEvidence::Strict;
let b = DescentEvidence::NonIncreasing;
c.bench_function("tier3_termination_merge_evidence", |bencher| {
bencher.iter(|| black_box(merge_evidence(black_box(a), black_box(b))));
});
}

fn bench_computation_mirror(c: &mut Criterion) {
let steps = positive_amount_from_i64(32).expect("fixture Peano depth");
c.bench_function("tier3_computation_positive_descent_count", |bencher| {
Expand Down Expand Up @@ -70,7 +62,6 @@ fn bench_effect_carrier_mirror(c: &mut Criterion) {

criterion_group!(
tier3_mirror_phase1,
bench_termination_mirror,
bench_computation_mirror,
bench_induction_mirror,
bench_effect_carrier_mirror
Expand Down
78 changes: 1 addition & 77 deletions src/v3/compiler/src/dag.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1020,84 +1020,8 @@ pub struct ProofEdge {
pub evidence: Vec<DescentEvidence>,
}

pub fn evidence_rank(evidence: DescentEvidence) -> i64 {
match evidence {
DescentEvidence::Strict => 2,
DescentEvidence::NonIncreasing => 1,
DescentEvidence::DescentUnknown => 0,
}
}

pub fn merge_evidence(a: DescentEvidence, b: DescentEvidence) -> DescentEvidence {
match a {
DescentEvidence::Strict => match b {
DescentEvidence::Strict => DescentEvidence::Strict,
DescentEvidence::NonIncreasing => DescentEvidence::NonIncreasing,
DescentEvidence::DescentUnknown => DescentEvidence::DescentUnknown,
},
DescentEvidence::NonIncreasing => match b {
DescentEvidence::Strict => DescentEvidence::NonIncreasing,
DescentEvidence::NonIncreasing => DescentEvidence::NonIncreasing,
DescentEvidence::DescentUnknown => DescentEvidence::DescentUnknown,
},
DescentEvidence::DescentUnknown => DescentEvidence::DescentUnknown,
}
}

pub fn join_evidence(a: DescentEvidence, b: DescentEvidence) -> DescentEvidence {
match a {
DescentEvidence::DescentUnknown => b,
DescentEvidence::NonIncreasing => match b {
DescentEvidence::Strict => DescentEvidence::Strict,
DescentEvidence::NonIncreasing => DescentEvidence::NonIncreasing,
DescentEvidence::DescentUnknown => DescentEvidence::NonIncreasing,
},
DescentEvidence::Strict => DescentEvidence::Strict,
}
}

/// Legacy E-T helper name retained for carrier API parity.
///
/// Fail-closed behavior means no unary helper may fabricate `Strict` from
/// weaker evidence; strict promotion requires a separate structural witness.
///
/// P5 bridge: identifier suggests promotion; this mirror is identity on the
/// three `DescentEvidence` variants today (same fail-closed contract as
/// `std.termination`). Dissolution: rename to e.g. `evidence_passthrough_preserving_strict`
/// and/or remove `v2.compiler.complexity` call sites when parser progress threads
/// `Strict` at the witness site.
pub fn promote_to_strict(evidence: DescentEvidence) -> DescentEvidence {
evidence
}

pub fn optional_evidence_meet(
a: Option<DescentEvidence>,
b: Option<DescentEvidence>,
) -> Option<DescentEvidence> {
match a {
None => b,
Some(va) => match b {
None => a,
Some(vb) => Some(merge_evidence(va, vb)),
},
}
}

pub fn map_evidence_merge_at(
mut base: HashMap<String, DescentEvidence>,
key: String,
new_val: DescentEvidence,
) -> HashMap<String, DescentEvidence> {
let merged = match base.get(&key).copied() {
Some(existing) => merge_evidence(existing, new_val),
None => new_val,
};
base.insert(key, merged);
base
}

// Continuation: Rust execution mirror for `src/v3/std/computation.dag` (Lane E-C).
// Same staging contract as the termination mirror above (`ArrowBody::Unparsed` std bodies).
// The termination lattice mirror has dissolved; computation still waits on evaluated std bodies.

@briansrls briansrls May 10, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

BLOCKING: This claims the termination lattice mirror is dissolved, but the PR only removes the Rust helpers while the std termination bodies remain preserved as ArrowBody::Unparsed, so INVARIANTS P5 / T-Tier3-Dissolution require an Evaluator-backed .dag consumer receipt before deletion counts as dissolution.

// `m2_substrate_inhabitance_test::{computation_*}` pins carrier shape + lowering helpers.

/// 🟡 SCAFFOLD — `SizeBound` coproduct (`docs/modeling-discipline.md` §4).
Expand Down
64 changes: 19 additions & 45 deletions src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,10 @@
use std::collections::{HashMap, HashSet};

Check failure on line 1 in src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs

View workflow job for this annotation

GitHub Actions / v3 

unused import: `HashMap`

use v3_compiler::compile_to_dag;
use v3_compiler::dag::{

Check warning on line 4 in src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs

View workflow job for this annotation

GitHub Actions / fmt 

Diff in /home/runner/work/gunbc/gunbc/src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs
algebra_profile_to_dimension, constant_bound_value, evidence_rank, is_constant_bound,
join_evidence, literal_bits_int, lower_call_pattern, map_evidence_merge_at, merge_evidence,
optional_evidence_meet, per_call_descent_evidence, per_call_pattern_at,
positive_amount_from_i64, promote_to_strict, size_bound_param,
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,
sub_value_relation_to_call_pattern, tree_size_bound, type_iteration_dimension, AlgebraProfile,
ArrowBody, AtomPayload, CallPattern, CardinalityBound, DescentEvidence, FieldMap, FieldValue,
Interval, IntervalWidth, IterationDimension, IterationPrimitive, LoweringTarget,
Expand Down Expand Up @@ -493,48 +492,23 @@
}

#[test]
fn termination_lattice_rust_mirror_matches_dag_authority() {
use DescentEvidence::{DescentUnknown, NonIncreasing, Strict};

assert_eq!(evidence_rank(Strict), 2);
assert_eq!(evidence_rank(NonIncreasing), 1);
assert_eq!(evidence_rank(DescentUnknown), 0);

for evidence in [Strict, NonIncreasing, DescentUnknown] {
assert_eq!(merge_evidence(Strict, evidence), evidence);
assert_eq!(merge_evidence(evidence, Strict), evidence);
assert_eq!(join_evidence(DescentUnknown, evidence), evidence);
assert_eq!(join_evidence(evidence, DescentUnknown), evidence);
}

assert_eq!(merge_evidence(Strict, Strict), Strict);
assert_eq!(merge_evidence(Strict, NonIncreasing), NonIncreasing);
assert_eq!(merge_evidence(NonIncreasing, NonIncreasing), NonIncreasing);
assert_eq!(
merge_evidence(NonIncreasing, DescentUnknown),
DescentUnknown
);

assert_eq!(join_evidence(NonIncreasing, Strict), Strict);
assert_eq!(join_evidence(NonIncreasing, NonIncreasing), NonIncreasing);
assert_eq!(join_evidence(Strict, DescentUnknown), Strict);
fn termination_lattice_rust_mirror_dissolved() {
let dag_rs = include_str!("../../src/dag.rs");

assert_eq!(promote_to_strict(NonIncreasing), NonIncreasing);
assert_eq!(promote_to_strict(Strict), Strict);
assert_eq!(promote_to_strict(DescentUnknown), DescentUnknown);

assert_eq!(optional_evidence_meet(None, Some(Strict)), Some(Strict));
assert_eq!(
optional_evidence_meet(Some(Strict), Some(NonIncreasing)),
Some(NonIncreasing)
);

let mut base = HashMap::new();
base.insert(String::from("n"), Strict);
let merged = map_evidence_merge_at(base, String::from("n"), NonIncreasing);
assert_eq!(merged.get("n"), Some(&NonIncreasing));
let inserted = map_evidence_merge_at(merged, String::from("m"), Strict);
assert_eq!(inserted.get("m"), Some(&Strict));
for helper in [
"evidence_rank",
"merge_evidence",
"join_evidence",
"promote_to_strict",
"optional_evidence_meet",
"map_evidence_merge_at",
] {
assert!(
!dag_rs.contains(&format!("pub fn {helper}")),
"`dag.rs` must not carry a hand-Rust `{helper}` lattice mirror; \
`src/v3/std/termination.dag` is the authority"
);
}
}

#[test]
Expand Down
20 changes: 10 additions & 10 deletions src/v3/compiler/tests/integration/sg0_census_test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -211,16 +211,16 @@ const EXPECTED_HAND_AUTHORED_NON_TEST: &[&str] = &[
// `tier3_mirror_dissolution_perf_within_budget` per
// `docs/briefs/r3-pb-tier3-perf-budget-worker.md` deliverable 0b
// (parent brief #1331; readiness matrix #1358; this PR #1362).
// Intentionally hand-authored: it measures live public mirror
// entrypoints (`merge_evidence`, `positive_descent_count`,
// `lower_call_pattern`, `type_iteration_dimension`,
// `lane2_workflow_idempotency_report`) before T-Tier3-Dissolution
// retires them — generated output cannot exist yet because the
// measurement target is the not-yet-dissolved Rust code.
// Dissolution trigger: deletes alongside the mirror-dissolution PRs
// per parent brief §"Phase 1 deliverables" — the bench harness has
// no role post-Phase-1; only the frozen `tier3_baseline.json` data
// survives.
// Intentionally hand-authored: it measures the remaining live public
// mirror entrypoints (`positive_descent_count`, `lower_call_pattern`,
// `type_iteration_dimension`, `lane2_workflow_idempotency_report`)
// before T-Tier3-Dissolution retires them — generated output cannot
// exist yet because the measurement target is the not-yet-dissolved
// Rust code. The termination entrypoint retired with
// `tier3_termination_mirror_dissolved`.
// Dissolution trigger: deletes alongside the remaining mirror-dissolution
// PRs per parent brief §"Phase 1 deliverables" — the bench harness has no
// role post-Phase-1; only the frozen `tier3_baseline.json` data survives.
"src/v3/compiler/benches/tier3_mirror_perf.rs",
"src/v3/compiler/build.rs",
// R3 row 85 / PB #1560 Gap 4 build-step shim: invokes
Expand Down
Loading