diff --git a/rust/candid/examples/subtype_bench.rs b/rust/candid/examples/subtype_bench.rs new file mode 100644 index 00000000..7c308be2 --- /dev/null +++ b/rust/candid/examples/subtype_bench.rs @@ -0,0 +1,127 @@ +//! Micro-benchmark for issue #603: quadratic subtype traversal. +//! +//! Builds deeply nested `vec` types and times `subtype` for growing depth. +//! Three workloads: +//! - widening : vec^d(nat) <: vec^d(int) -> succeeds (Nat <: Int at leaf) +//! - rejection : vec^d(nat) <: vec^d(text) -> fails at the leaf +//! - equal : vec^d(nat) <: vec^d(nat) -> succeeds, two separately allocated +//! but structurally equal trees, caught by the whole-type `==` fast path +//! - subtree : record{0: vec^d nat; 1: nat} <: record{0: vec^d nat} -> the +//! shared field is a separately allocated equal subtree, but the records +//! differ so the whole-type fast path cannot fire; it must be accepted by the +//! per-level memoized equality without walking the field into the guard (the +//! case a ptr_eq-only patch regressed; PR #780 review) +//! +//! BEFORE the fix, widening/rejection are O(depth^2) (the `t1 == t2` deep +//! structural compare runs at every recursion level). `equal` is O(depth) via +//! the whole-type short-circuit. `subtree` is the regression guard: it stays +//! O(depth) via the memoized per-level equality. +//! +//! Run: cargo run --release --example subtype_bench + +use candid::types::subtype::{subtype, Gamma}; +use candid::types::{Type, TypeEnv, TypeInner}; +use std::time::Instant; + +/// vec^depth(leaf), freshly allocated each call. +fn nest(depth: usize, leaf: TypeInner) -> Type { + let mut t: Type = leaf.into(); + for _ in 0..depth { + t = TypeInner::Vec(t).into(); + } + t +} + +/// `record { 0: vec^depth(leaf); extra... }`, with field ids 0, 1, 2, … +fn record(fields: Vec) -> Type { + use candid::types::internal::{Field, Label}; + use std::rc::Rc; + TypeInner::Record( + fields + .into_iter() + .enumerate() + .map(|(id, ty)| Field { + id: Rc::new(Label::Id(id as u32)), + ty, + }) + .collect(), + ) + .into() +} + +/// Median per-operation time in nanoseconds, over `runs` runs of `iters` ops. +fn bench(iters: u64, runs: usize, mut f: F) -> f64 { + let mut samples: Vec = Vec::with_capacity(runs); + for _ in 0..runs { + let start = Instant::now(); + for _ in 0..iters { + f(); + } + let elapsed = start.elapsed().as_nanos() as f64; + samples.push(elapsed / iters as f64); + } + samples.sort_by(|a, b| a.partial_cmp(b).unwrap()); + samples[samples.len() / 2] +} + +fn run_case(name: &str, t1: &Type, t2: &Type, expect_ok: bool, iters: u64, runs: usize) -> f64 { + let env = TypeEnv::new(); + // Sanity: confirm the subtype relation is what we expect, so a "fast" + // number is never fast because it short-circuited the wrong way. + let mut g: Gamma = Gamma::new(); + let ok = subtype(&mut g, &env, t1, t2).is_ok(); + assert_eq!(ok, expect_ok, "{name}: unexpected subtype result"); + bench(iters, runs, || { + let mut gamma: Gamma = Gamma::new(); + let _ = subtype(&mut gamma, &env, t1, t2); + }) +} + +fn main() { + let runs = 9; + let depths = [16usize, 32, 64, 128, 256, 384, 512]; + let env_leaf = TypeEnv::new(); + let _ = &env_leaf; + + println!("# subtype_bench (issue #603) median ns/op over {runs} runs"); + println!(); + for (name, build) in [ + ( + "widening vec^d(nat) <: vec^d(int)", + Box::new(|d: usize| (nest(d, TypeInner::Nat), nest(d, TypeInner::Int), true)) + as Box (Type, Type, bool)>, + ), + ( + "rejection vec^d(nat) <: vec^d(text)", + Box::new(|d: usize| (nest(d, TypeInner::Nat), nest(d, TypeInner::Text), false)), + ), + ( + "equal vec^d(nat) <: vec^d(nat)", + Box::new(|d: usize| (nest(d, TypeInner::Nat), nest(d, TypeInner::Nat), true)), + ), + ( + "subtree record{vec^d nat; nat} <: record{vec^d nat}", + Box::new(|d: usize| { + ( + record(vec![nest(d, TypeInner::Nat), TypeInner::Nat.into()]), + record(vec![nest(d, TypeInner::Nat)]), + true, + ) + }), + ), + ] { + println!("## {name}"); + println!("{:>6} | {:>14} | {:>14}", "depth", "ns/op", "ns/op/depth"); + println!("{:->6}-+-{:-<14}-+-{:-<14}", "", "", ""); + for &d in &depths { + let (t1, t2, ok) = build(d); + // Scale iterations so each run is a meaningful duration regardless + // of how fast the operation is; fewer iters for the slow BEFORE + // deep-nesting cases, more for the fast ones. + let iters: u64 = (2_000_000 / (d as u64 * d as u64 / 16 + 1)).clamp(200, 200_000); + let ns = run_case(name, &t1, &t2, ok, iters, runs); + println!("{d:>6} | {ns:>14.1} | {:>14.3}", ns / d as f64); + } + println!(); + } +} diff --git a/rust/candid/src/types/subtype.rs b/rust/candid/src/types/subtype.rs index 2498f699..c30ed3ee 100644 --- a/rust/candid/src/types/subtype.rs +++ b/rust/candid/src/types/subtype.rs @@ -5,11 +5,18 @@ use crate::types::TypeEnv; use crate::utils::RecursionDepth; use crate::{Error, Result}; use anyhow::Context; +use std::cell::RefCell; use std::collections::{HashMap, HashSet}; use std::fmt; pub type Gamma = HashSet<(Type, Type)>; +/// Pointer identity of a `Type`, used to key the structural-equality memo in +/// [`Assumptions`]. The `Type`s a key is taken from are pinned alive for the +/// life of the check (see `Assumptions::eq_pins`), so an address is never freed +/// and reused under a live key. +type TypePtr = *const TypeInner; + /// The `Gamma` of one check, together with the order its pairs were assumed in. /// /// A pair is assumed before it is proved, and any pair proved after it may have @@ -28,6 +35,12 @@ struct Assumptions<'a> { gamma: &'a mut Gamma, log: Vec<(Type, Type)>, refuted: Gamma, + /// Memo for `same_type`, keyed by the pointer identity of the two `Type`s. + /// Each entry's `Type`s are kept alive in `eq_pins`, so a cached verdict can + /// never be read for a different type that happens to reuse a freed address. + eq_memo: RefCell>, + /// Keeps every `Type` that `eq_memo` keys on alive for the whole check. + eq_pins: RefCell>, } impl<'a> Assumptions<'a> { @@ -36,9 +49,129 @@ impl<'a> Assumptions<'a> { gamma, log: Vec::new(), refuted: Gamma::new(), + eq_memo: RefCell::new(HashMap::new()), + eq_pins: RefCell::new(Vec::new()), } } + /// Reflexivity short-circuit used *inside* the subtype recursion, in place + /// of the deep structural `t1 == t2` (#603). + /// + /// `t1 == t2` on `Type` is a deep structural comparison (derived `PartialEq` + /// over `Rc`). The recursion reached it at *every* level, so a + /// mismatch deep inside an otherwise-identical tree was rediscovered by + /// re-comparing the surrounding structure at each level: O(depth^2) in the + /// nesting depth. + /// + /// This returns exactly what `t1 == t2` would — so it is a sound, + /// behaviour-preserving replacement for it — but memoizes by pointer + /// identity, so each subtree pair is compared at most once across the whole + /// check. The memo makes both directions linear: an equal subtree is + /// accepted after one comparison, and a mismatch deep in an otherwise-equal + /// tree is found once and then answered from the cache at every enclosing + /// level, instead of being rewalked. A first cut of this PR used a bare + /// `ptr_eq`/leaf check, which was O(1) but stopped detecting + /// separately-allocated equal composite subtrees; one whose parents differ + /// (so the entry-point whole-type `==` cannot fire) was then walked + /// level-by-level into the recursion guard, turning a valid check into a + /// "recursion limit exceeded" error (PR #780 review). Memoized deep equality + /// keeps the O(1)-amortized per level while restoring that acceptance. + fn same_type(&self, t1: &Type, t2: &Type, depth: &RecursionDepth) -> bool { + use TypeInner::*; + if std::rc::Rc::ptr_eq(&t1.0, &t2.0) { + return true; + } + let key: (TypePtr, TypePtr) = (std::rc::Rc::as_ptr(&t1.0), std::rc::Rc::as_ptr(&t2.0)); + if let Some(&cached) = self.eq_memo.borrow().get(&key) { + return cached; + } + // Recurse under the same stack guard as the structural subtype rules. This + // traversal descends one native frame per nesting level, so on a deeply + // nested equal subtree it could overflow the stack on its own — exactly + // what `RecursionDepth` prevents everywhere else here (PR #780 review). + // When the stack runs low, stop and report "not trivially equal" so the + // caller falls through to the guarded structural rules, which end the whole + // check with a graceful "Recursion limit exceeded" rather than aborting the + // process. The bail means "undetermined here", not "unequal", so the result + // below is cached only when no limit was hit in this subtree. + let Ok(_guard) = depth.guard() else { + return false; + }; + if depth.overflows() > 0 { + return false; + } + let result = match (t1.as_ref(), t2.as_ref()) { + // Composites that can form deep chains recurse through `same_type`, + // so each nested pair is memoized too; that is what keeps the whole + // traversal linear rather than quadratic. + (Opt(a), Opt(b)) | (Vec(a), Vec(b)) => self.same_type(a, b, depth), + (Record(f1), Record(f2)) | (Variant(f1), Variant(f2)) => { + f1.len() == f2.len() + && f1 + .iter() + .zip(f2.iter()) + .all(|(x, y)| x.id == y.id && self.same_type(&x.ty, &y.ty, depth)) + } + (Class(a1, r1), Class(a2, r2)) => { + a1.len() == a2.len() + && a1 + .iter() + .zip(a2.iter()) + .all(|(x, y)| self.same_type(x, y, depth)) + && self.same_type(r1, r2, depth) + } + // `Func` and `Service` also form arbitrarily deep chains — a function + // whose return is a function, a service whose method is such a + // function, and so on — and the subtype recursion reaches `same_type` + // at each level, so they must recurse through `same_type` too. Left to + // the derived `==` arm, a mismatch deep in an otherwise-equal chain + // would be re-walked in full at every enclosing level: the #603 + // quadratic, still live for these two until PR #780 review flagged it. + // The non-type metadata (`modes`, method names) holds no nested `Type`, + // so it is compared directly; child types go through `same_type`, so + // each nested pair is memoized and the traversal stays linear. + (Func(f1), Func(f2)) => { + f1.modes == f2.modes + && f1.args.len() == f2.args.len() + && f1.rets.len() == f2.rets.len() + && f1 + .args + .iter() + .zip(f2.args.iter()) + .all(|(x, y)| self.same_type(x, y, depth)) + && f1 + .rets + .iter() + .zip(f2.rets.iter()) + .all(|(x, y)| self.same_type(x, y, depth)) + } + (Service(m1), Service(m2)) => { + m1.len() == m2.len() + && m1 + .iter() + .zip(m2.iter()) + .all(|(x, y)| x.0 == y.0 && self.same_type(&x.1, &y.1, depth)) + } + // Leaves, the `Var`/`Knot` indirection nodes, and any cross-variant + // pair carry no deep-nesting chain to re-walk per level here, so the + // derived deep `==` settles them directly; its verdict is still cached + // by pointer below. + (a, b) => a == b, + }; + // Cache only a verdict reached without hitting the stack guard anywhere in + // this subtree; a bail above returns a bare `false` that must not be + // remembered as "unequal". + if depth.overflows() == 0 { + self.eq_memo.borrow_mut().insert(key, result); + // Pin both operands so their addresses stay valid (and unique) for + // every later cache hit on this key. + let mut pins = self.eq_pins.borrow_mut(); + pins.push(t1.clone()); + pins.push(t2.clone()); + } + result + } + /// Assume `t1 <: t2`. `None` if it is already assumed; otherwise the mark /// to `retract` it by. fn assume(&mut self, t1: &Type, t2: &Type) -> Option { @@ -90,6 +223,14 @@ pub fn subtype_with_config( t1: &Type, t2: &Type, ) -> Result<()> { + // One-shot deep equality: a wholly-equal pair is decided in a single linear + // pass here, so the common equal case never allocates the `Assumptions` + // state. Inside the recursion `Assumptions::same_type` is used, which is the + // same deep equality but memoized by pointer identity, so the per-level + // check is O(1)-amortized and the quadratic blow-up (#603) stays fixed. + if t1 == t2 { + return Ok(()); + } let mut gamma = Assumptions::new(gamma); let depth = RecursionDepth::new(); let res = subtype_(report, &mut gamma, env, t1, t2, &depth); @@ -231,6 +372,13 @@ pub fn subtype_check_all( t1: &Type, t2: &Type, ) -> Vec { + // One-shot deep equality fast path; see `subtype_with_config`. A fully-equal + // pair has no incompatibilities, and deciding it here avoids allocating the + // `Assumptions` state, while `Assumptions::same_type` handles each level of + // the partial-overlap cases. + if t1 == t2 { + return Vec::new(); + } let mut errors = Vec::new(); let mut gamma = Assumptions::new(gamma); let depth = RecursionDepth::new(); @@ -291,7 +439,7 @@ fn subtype_collect_( return; } use TypeInner::*; - if t1 == t2 { + if gamma.same_type(t1, t2, depth) { return; } // Handle Var/Knot (type variables / recursive types) @@ -654,7 +802,7 @@ fn subtype_( return Err(Error::msg("Recursion limit exceeded")); } use TypeInner::*; - if t1 == t2 { + if gamma.same_type(t1, t2, depth) { return Ok(()); } if matches!(t1.as_ref(), Var(_) | Knot(_)) || matches!(t2.as_ref(), Var(_) | Knot(_)) { @@ -990,3 +1138,267 @@ fn pp_args(args: &[crate::types::Type]) -> String { let _ = write!(&mut s, ")"); s } + +#[cfg(test)] +mod tests { + //! `Assumptions::same_type` is a memoized stand-in for the deep structural + //! `t1 == t2` it replaced inside the subtype recursion (#603). These tests + //! pin it to its oracle: for every pair it must return exactly what the + //! derived `==` returns, including for separately allocated but equal trees + //! (the case a `ptr_eq`-only check regressed; PR #780 review). + use super::*; + use crate::types::internal::{Function, Label}; + use std::rc::Rc; + + fn leaf(t: TypeInner) -> Type { + t.into() + } + /// `vec^depth(leaf)`, freshly allocated so no node is shared with any other + /// tree built the same way. + fn vec(depth: usize, l: TypeInner) -> Type { + let mut t: Type = l.into(); + for _ in 0..depth { + t = TypeInner::Vec(t).into(); + } + t + } + fn opt(t: Type) -> Type { + TypeInner::Opt(t).into() + } + fn rec(fields: Vec<(u32, Type)>) -> Type { + TypeInner::Record( + fields + .into_iter() + .map(|(id, ty)| Field { + id: Rc::new(Label::Id(id)), + ty, + }) + .collect(), + ) + .into() + } + fn variant(fields: Vec<(u32, Type)>) -> Type { + TypeInner::Variant( + fields + .into_iter() + .map(|(id, ty)| Field { + id: Rc::new(Label::Id(id)), + ty, + }) + .collect(), + ) + .into() + } + fn func(args: Vec, rets: Vec) -> Type { + TypeInner::Func(Function { + modes: vec![], + args, + rets, + }) + .into() + } + fn class(args: Vec, ret: Type) -> Type { + TypeInner::Class(args, ret).into() + } + fn service(ms: Vec<(&str, Type)>) -> Type { + TypeInner::Service(ms.into_iter().map(|(n, t)| (n.to_string(), t)).collect()).into() + } + + /// `same_type` must agree with the derived `==` in both directions. + fn assert_oracle(a: &Type, b: &Type) { + let mut g = Gamma::new(); + let asm = Assumptions::new(&mut g); + let depth = crate::utils::RecursionDepth::new(); + assert_eq!( + asm.same_type(a, b, &depth), + a == b, + "same_type disagreed with `==` on {a:?} vs {b:?}" + ); + assert_eq!( + asm.same_type(b, a, &depth), + b == a, + "same_type disagreed with `==` on {b:?} vs {a:?}" + ); + } + + #[test] + fn same_type_matches_eq_on_leaves_and_mismatched_variants() { + assert_oracle(&leaf(TypeInner::Nat), &leaf(TypeInner::Nat)); + assert_oracle(&leaf(TypeInner::Nat), &leaf(TypeInner::Int)); + assert_oracle(&leaf(TypeInner::Principal), &leaf(TypeInner::Principal)); + // Cross-variant pairs fall to the derived `==` arm and must be unequal. + assert_oracle(&opt(leaf(TypeInner::Nat)), &vec(1, TypeInner::Nat)); + assert_oracle(&vec(1, TypeInner::Nat), &leaf(TypeInner::Nat)); + assert_oracle( + &TypeInner::Var("a".into()).into(), + &TypeInner::Var("b".into()).into(), + ); + } + + #[test] + fn same_type_accepts_separately_allocated_equal_deep_subtrees() { + // The regression from PR #780: these share no allocation (ptr_eq is + // false at every level) yet are structurally equal, so `same_type` must + // still return true without being walked level by level. + let d = 400; + assert!(Rc::as_ptr(&vec(d, TypeInner::Nat).0) != Rc::as_ptr(&vec(d, TypeInner::Nat).0)); + assert_oracle(&vec(d, TypeInner::Nat), &vec(d, TypeInner::Nat)); + // ...and must still distinguish a deep leaf mismatch or a depth change. + assert_oracle(&vec(d, TypeInner::Nat), &vec(d, TypeInner::Int)); + assert_oracle(&vec(d, TypeInner::Nat), &vec(d - 1, TypeInner::Nat)); + } + + #[test] + fn same_type_matches_eq_on_records_and_variants() { + let r = || { + rec(vec![ + (0, vec(3, TypeInner::Nat)), + (1, leaf(TypeInner::Text)), + ]) + }; + assert_oracle(&r(), &r()); + // Reordered fields, a renamed field, an extra field, and a changed field + // type must each be unequal — exactly as the derived `==` sees them. + assert_oracle( + &r(), + &rec(vec![ + (1, leaf(TypeInner::Text)), + (0, vec(3, TypeInner::Nat)), + ]), + ); + assert_oracle( + &r(), + &rec(vec![ + (0, vec(3, TypeInner::Nat)), + (2, leaf(TypeInner::Text)), + ]), + ); + assert_oracle( + &r(), + &rec(vec![ + (0, vec(3, TypeInner::Nat)), + (1, leaf(TypeInner::Text)), + (2, leaf(TypeInner::Nat)), + ]), + ); + assert_oracle( + &r(), + &rec(vec![ + (0, vec(3, TypeInner::Int)), + (1, leaf(TypeInner::Text)), + ]), + ); + let v = || variant(vec![(0, leaf(TypeInner::Nat)), (1, leaf(TypeInner::Null))]); + assert_oracle(&v(), &v()); + assert_oracle( + &v(), + &variant(vec![ + (0, leaf(TypeInner::Nat)), + (1, leaf(TypeInner::Reserved)), + ]), + ); + // A record and a variant with identical fields are still different types. + assert_oracle( + &rec(vec![(0, leaf(TypeInner::Nat))]), + &variant(vec![(0, leaf(TypeInner::Nat))]), + ); + } + + #[test] + fn same_type_matches_eq_on_func_class_service() { + let f = || func(vec![vec(2, TypeInner::Nat)], vec![leaf(TypeInner::Bool)]); + assert_oracle(&f(), &f()); + assert_oracle( + &f(), + &func(vec![vec(2, TypeInner::Int)], vec![leaf(TypeInner::Bool)]), + ); + assert_oracle(&f(), &func(vec![vec(2, TypeInner::Nat)], vec![])); + + let s = || service(vec![("m", f()), ("n", leaf(TypeInner::Nat))]); + assert_oracle(&s(), &s()); + assert_oracle( + &s(), + &service(vec![("m", f()), ("other", leaf(TypeInner::Nat))]), + ); + + let c = || class(vec![vec(2, TypeInner::Nat), leaf(TypeInner::Bool)], s()); + assert_oracle(&c(), &c()); + assert_oracle(&c(), &class(vec![vec(2, TypeInner::Nat)], s())); + assert_oracle( + &c(), + &class(vec![vec(2, TypeInner::Nat), leaf(TypeInner::Bool)], f()), + ); + // A deeply nested leaf mismatch inside a class must still be caught. + assert_oracle( + &c(), + &class(vec![vec(2, TypeInner::Int), leaf(TypeInner::Bool)], s()), + ); + } + + #[test] + fn same_type_matches_eq_on_deep_func_and_service_chains() { + // `func () -> (func () -> (... leaf))` nested `d` deep, separately + // allocated at every level (ptr_eq false throughout). Before the + // dedicated `Func`/`Service` arms these fell to the derived `==`, which + // re-walked the whole tail at each recursion level (the #603 quadratic). + // The oracle pins that recursing through `same_type` still agrees with + // `==` in both the equal and the deep-mismatch case. + fn func_chain(d: usize, bottom: TypeInner) -> Type { + let mut t = leaf(bottom); + for _ in 0..d { + t = func(vec![], vec![t]); + } + t + } + fn service_chain(d: usize, bottom: TypeInner) -> Type { + let mut t = leaf(bottom); + for _ in 0..d { + t = service(vec![("m", t)]); + } + t + } + let d = 400; + assert_oracle( + &func_chain(d, TypeInner::Nat), + &func_chain(d, TypeInner::Nat), + ); + // One differing leaf at the bottom of an otherwise-identical chain. + assert_oracle( + &func_chain(d, TypeInner::Nat), + &func_chain(d, TypeInner::Int), + ); + assert_oracle( + &service_chain(d, TypeInner::Nat), + &service_chain(d, TypeInner::Nat), + ); + assert_oracle( + &service_chain(d, TypeInner::Nat), + &service_chain(d, TypeInner::Int), + ); + } + + #[test] + fn same_type_matches_eq_on_nested_composites() { + let big = || { + opt(rec(vec![ + (0, vec(5, TypeInner::Nat)), + (1, variant(vec![(7, opt(leaf(TypeInner::Text)))])), + ( + 2, + func(vec![leaf(TypeInner::Nat)], vec![vec(3, TypeInner::Bool)]), + ), + ])) + }; + assert_oracle(&big(), &big()); + // Change one leaf five levels down; `==` sees it, so `same_type` must too. + let other = opt(rec(vec![ + (0, vec(5, TypeInner::Int)), + (1, variant(vec![(7, opt(leaf(TypeInner::Text)))])), + ( + 2, + func(vec![leaf(TypeInner::Nat)], vec![vec(3, TypeInner::Bool)]), + ), + ])); + assert_oracle(&big(), &other); + } +} diff --git a/rust/candid/tests/subtype_equal_subtree.rs b/rust/candid/tests/subtype_equal_subtree.rs new file mode 100644 index 00000000..ce891d4b --- /dev/null +++ b/rust/candid/tests/subtype_equal_subtree.rs @@ -0,0 +1,201 @@ +//! A separately allocated but structurally equal subtree is reflexively a +//! subtype, so it must be accepted even when it is too deep to walk within the +//! recursion guard. +//! +//! De-quadratic subtype checking (#603) stopped running the deep `t1 == t2` at +//! every recursion level. A first cut detected equality only by pointer, which +//! missed separately allocated equal subtrees: one whose parents differ (so the +//! entry-point whole-type `==` cannot fire) was walked level by level into the +//! depth guard, turning a valid check into a "recursion limit exceeded" error +//! (PR #780 review). The per-level check is now a memoized deep equality, which +//! short-circuits such a subtree before it reaches the guard. +//! +//! The limit is reached at a depth that depends on the stack, not the types, so +//! each check runs on a thread with a fixed stack (as in +//! `subtype_recursion_limit.rs`) to make the depth predictable. + +use candid::types::internal::{Field, Label, Type, TypeInner}; +use candid::types::subtype::{subtype, subtype_check_all, Gamma, Incompatibility}; +use candid::types::TypeEnv; +use std::rc::Rc; + +const STACK_SIZE: usize = 1 << 20; + +/// Levels of headroom left between the measured recursion limit and the depth of +/// an *equal* subtree an acceptance test builds. `same_type` shares the +/// structural `RecursionDepth`, so verifying the subtree must fit under the same +/// limit *together with* the enclosing record (and, for the alias test, the `Var` +/// resolution) frames. Where the stack size can't be measured the guard is a flat +/// 512-level count with no byte slack, so this headroom is what keeps these +/// acceptance tests passing there as well (PR #780 review). The subtree is still +/// hundreds of levels deep, and the sanity check below pins the full limit. +const EQUAL_SUBTREE_HEADROOM: usize = 16; + +fn on_small_stack(f: impl FnOnce() -> T + Send + 'static) -> T { + std::thread::Builder::new() + .stack_size(STACK_SIZE) + .spawn(f) + .unwrap() + .join() + .unwrap() +} + +/// `vec^depth(leaf)`, freshly allocated so the trees share no node. +fn vec_chain(depth: usize, leaf: TypeInner) -> Type { + let mut t: Type = leaf.into(); + for _ in 0..depth { + t = TypeInner::Vec(t).into(); + } + t +} + +fn record(fields: Vec) -> Type { + TypeInner::Record( + fields + .into_iter() + .enumerate() + .map(|(id, ty)| Field { + id: Rc::new(Label::Id(id as u32)), + ty, + }) + .collect(), + ) + .into() +} + +fn var(name: &str) -> Type { + TypeInner::Var(name.to_string()).into() +} + +fn hit_limit(errors: &[Incompatibility]) -> bool { + errors.iter().any(|e| { + e.message + .to_lowercase() + .contains("recursion limit exceeded") + }) +} + +/// Shortest `vec^d(nat) <: vec^d(text)` that hits the limit on this thread: a +/// mismatched chain of this depth is walked straight into the guard, so it is a +/// depth at which an equal subtree would be too, were it not short-circuited. +fn shortest_overflowing_depth() -> usize { + let overflows = |d: usize| { + on_small_stack(move || { + let env = TypeEnv::new(); + hit_limit(&subtype_check_all( + &mut Gamma::new(), + &env, + &vec_chain(d, TypeInner::Nat), + &vec_chain(d, TypeInner::Text), + )) + }) + }; + let mut hi = 64; + while !overflows(hi) { + hi *= 2; + } + let mut lo = hi / 2 + 1; + while lo < hi { + let mid = (lo + hi) / 2; + if overflows(mid) { + hi = mid; + } else { + lo = mid + 1; + } + } + lo +} + +/// `record { 0: vec^d nat; 1: nat } <: record { 0: vec^d nat }` with the shared +/// field just under the recursion limit (a mismatched chain at the full depth is +/// confirmed to overflow first). The field is separately allocated but equal, and +/// the records differ, so the whole-type `==` fast path cannot fire; the equal +/// field must be accepted as reflexive, not driven into the guard. +#[test] +fn deep_equal_subtree_under_differing_parents_is_accepted() { + let d = shortest_overflowing_depth(); + on_small_stack(move || { + let env = TypeEnv::new(); + // Sanity: a mismatched chain of this depth really does reach the guard, + // so the structural recursion is being driven that deep here. + assert!( + hit_limit(&subtype_check_all( + &mut Gamma::new(), + &env, + &vec_chain(d, TypeInner::Nat), + &vec_chain(d, TypeInner::Text), + )), + "expected the mismatched chain at depth {d} to hit the limit" + ); + + // The equal subtree sits a little below that limit so verifying it, plus + // the enclosing record frame, stays within the shared guard even under the + // flat fallback count (see EQUAL_SUBTREE_HEADROOM). + let sub = d.saturating_sub(EQUAL_SUBTREE_HEADROOM); + let t1 = record(vec![vec_chain(sub, TypeInner::Nat), TypeInner::Nat.into()]); + let t2 = record(vec![vec_chain(sub, TypeInner::Nat)]); + assert!( + subtype(&mut Gamma::new(), &env, &t1, &t2).is_ok(), + "equal deep subtree under differing parents must be accepted" + ); + assert!( + subtype_check_all(&mut Gamma::new(), &env, &t1, &t2).is_empty(), + "equal deep subtree under differing parents must report no incompatibility" + ); + }); +} + +/// Stack-safety half of the PR #780 review: a subtree so deep that the memoized +/// equality check would itself run out of stack must fail *gracefully*, never +/// overflow the native stack and abort the process. `same_type` shares the +/// structural recursion's `RecursionDepth`, so once the stack runs low it stops +/// and defers to the guarded structural rules, which end the check with +/// "recursion limit exceeded". A multiple of the structural limit is used so the +/// equality check is driven well past its own (lighter-frame, so deeper) limit; +/// if it were unguarded this test would crash the process rather than fail. +#[test] +fn deep_equal_subtree_beyond_guard_fails_gracefully() { + let d = shortest_overflowing_depth().saturating_mul(16); + on_small_stack(move || { + let env = TypeEnv::new(); + let t1 = record(vec![vec_chain(d, TypeInner::Nat), TypeInner::Nat.into()]); + let t2 = record(vec![vec_chain(d, TypeInner::Nat)]); + assert!( + subtype(&mut Gamma::new(), &env, &t1, &t2).is_err(), + "a subtree too deep for the equality check to verify must fail gracefully, not crash" + ); + assert!( + hit_limit(&subtype_check_all(&mut Gamma::new(), &env, &t1, &t2)), + "the collector must report the recursion limit rather than overflow the stack" + ); + }); +} + +/// The same, but the equal subtree is reached through two different `Var` +/// aliases (`A` and `B`, each a separately allocated `vec^d nat`). The +/// entry-point `==` misses it because the aliases differ by name; after one +/// resolution step the per-level equality must still accept the resolved subtree +/// before it reaches the guard. +#[test] +fn equal_subtree_through_different_aliases_is_accepted() { + let d = shortest_overflowing_depth(); + on_small_stack(move || { + let mut env = TypeEnv::new(); + // Headroom for the record plus the two `Var` resolution frames, so the + // equality check of the resolved subtree fits under the shared guard even + // under the flat fallback count (see EQUAL_SUBTREE_HEADROOM). + let sub = d.saturating_sub(EQUAL_SUBTREE_HEADROOM); + env.0.insert("A".into(), vec_chain(sub, TypeInner::Nat)); + env.0.insert("B".into(), vec_chain(sub, TypeInner::Nat)); + let t1 = record(vec![var("A"), TypeInner::Nat.into()]); + let t2 = record(vec![var("B")]); + assert!( + subtype(&mut Gamma::new(), &env, &t1, &t2).is_ok(), + "equal subtree via different aliases must be accepted" + ); + assert!( + subtype_check_all(&mut Gamma::new(), &env, &t1, &t2).is_empty(), + "equal subtree via different aliases must report no incompatibility" + ); + }); +}