From 5bda4f102b126484687d07b176d8fe3bf1eca510 Mon Sep 17 00:00:00 2001 From: Felipe705x Date: Thu, 23 Jul 2026 21:41:07 -0400 Subject: [PATCH 1/2] =?UTF-8?q?perf(typing):=20PathSummary=20=E2=80=94=20b?= =?UTF-8?q?oundary-pair=20path=20representation=20(spec+eval=20split)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Kills the exponential: `()-[]->()` ×16 against the LDBC SF0.1 schema went from ~23.3 s per check_query to ~33 ms, and the anon family now scales linearly (0.9 / 2.6 / 7.6 / 15.6 / 33.5 ms for N=1/2/4/8/16). Root cause was the inductive PathType carrying every interior node of every union arm and cloning the whole prefix per refined junction arm — width multiplied per hop by the compatible-schema-entry count. Memory was severe enough to push an 8 GiB box toward swap (peak RSS not instrumented). Design (spec + eval split, pending advisor review for full replacement): - path_type.rs is UNTOUCHED — it remains the paper's inductive definition (rules.md §4/§8), still pinned by lattice_proptest. - New src/typing/path_summary.rs: the checker's evaluation form. A path is summarized as zero-length arms (a node-descriptor set — first ≡ last) plus edge-bearing arms ((first,last) → min edge count). The two classes stay separate because they concatenate differently: a zero-length arm IS the junction and adopts the refined junction as its boundary. Width is bounded by |schema.nodes|²+|schema.nodes| regardless of pattern length. - checker.rs: TypecheckResult.path is now PathSummary; all construction and lattice call sites swapped 1:1. - tests/path_summary_hom_proptest.rs: pins the abstraction theorem — summarize(meet(p,q)) ≡ meet(summarize(p), summarize(q)) (same for union) over 2×512 random cases on star and labeled schemas, plus judgment agreement against a satisfiability-aware ("live") length reference. An earlier draft that min-merged zero- and positive-length arms of the same boundary was UNSOUND and caught by this proptest. Known, deliberate semantic delta (documented in the module): the spec type's len/is_empty are satisfiability-blind on dead arms, which made the repeat-length warning depend on HOW an inner pattern died (Zero → warned; Edge-over-Zero → silent). PathSummary implements the live semantics uniformly: a dead repeat-inner now always takes the warning branch, matching the old Zero case. No existing test observes the difference; verdicts and errors are unchanged across all suites (full sweep: 80 targets green). Measurement caveat: this run's small-case medians were taken on a loaded machine (user gaming); labeled-shape numbers (chain_16 ~317 us) look flat-to-better vs QW3 but fine deltas need a quiet re-baseline. North-star check/parse ratio column added to pattern_typecheck (currently ~5–30× on labeled shapes; target ≤1× via the stage-2 compiled-schema representation). Co-Authored-By: Claude Fable 5 --- src/bin/pattern_typecheck.rs | 79 ++++- src/typing/checker.rs | 35 +-- src/typing/mod.rs | 1 + src/typing/path_summary.rs | 282 ++++++++++++++++++ ..._summary_hom_proptest.proptest-regressions | 9 + tests/path_summary_hom_proptest.rs | 221 ++++++++++++++ 6 files changed, 602 insertions(+), 25 deletions(-) create mode 100644 src/typing/path_summary.rs create mode 100644 tests/path_summary_hom_proptest.proptest-regressions create mode 100644 tests/path_summary_hom_proptest.rs diff --git a/src/bin/pattern_typecheck.rs b/src/bin/pattern_typecheck.rs index de647d8..5f4585f 100644 --- a/src/bin/pattern_typecheck.rs +++ b/src/bin/pattern_typecheck.rs @@ -51,6 +51,32 @@ fn median_min_ns(mut v: Vec) -> (u128, u128) { (v[v.len() / 2], v[0]) } +/// Cold-compile timing: every sample runs against a schema whose refine +/// cache has never been used, so each check pays full misses (hash + +/// key/result clones + insert on top of the scan). This is the regime a +/// per-query cache would live in permanently — the honest upper bound on +/// the cache's overhead. Code/branch/data caches stay warm (that part is +/// shared with the steady-state protocol). Heavy cases are capped by the +/// same per-case budget. +fn time_case_cold(schema: &Schema, q: &Query) -> (u128, u128) { + let fresh = || Schema::from_parts((*schema.nodes).clone(), (*schema.edges).clone()); + // Pilot on one fresh schema. + let t = Instant::now(); + black_box(Typechecker::new(fresh()).check_query(black_box(q))); + let est = t.elapsed().as_nanos().max(1); + let iters = ((CASE_BUDGET_NS / est) as usize).clamp(3, 500); + // Pre-build outside the timed region. + let schemas: Vec = (0..iters).map(|_| fresh()).collect(); + let mut samples = Vec::with_capacity(iters); + for s in schemas { + let mut tc = Typechecker::new(s); + let t = Instant::now(); + black_box(tc.check_query(black_box(q))); + samples.push(t.elapsed().as_nanos()); + } + median_min_ns(samples) +} + /// Hot-loop timing with the established warmup + median protocol; falls /// back to batch timing when a case is too fast for per-call resolution. fn time_case(tc: &mut Typechecker, q: &Query) -> (u128, u128) { @@ -86,6 +112,23 @@ fn time_case(tc: &mut Typechecker, q: &Query) -> (u128, u128) { median_min_ns(samples) } +/// Median parse time of the case's query string — the north-star +/// yardstick: a fully optimized check should cost no more than parsing +/// the same input (both walk the same AST; parsing also allocates it). +fn time_parse(q: &str) -> u128 { + const P_ITERS: usize = 512; + for _ in 0..32 { + black_box(frogql::parser::parse_query(black_box(q)).expect("parse")); + } + let mut samples = Vec::with_capacity(P_ITERS); + for _ in 0..P_ITERS { + let t = Instant::now(); + black_box(frogql::parser::parse_query(black_box(q)).expect("parse")); + samples.push(t.elapsed().as_nanos()); + } + median_min_ns(samples).0 +} + // --- Generated scaling families (all expected `valid` on the LDBC schema) --- /// `(p0: Person)~[:knows]~(p1: Person)~...` — N undirected labeled hops. @@ -150,9 +193,12 @@ fn main() { let mut gdb: Option = None; let mut out: Option = None; let mut star_schema = false; + let mut cold = false; for arg in std::env::args().skip(1) { if arg == "--star-schema" { star_schema = true; + } else if arg == "--cold" { + cold = true; } else if gdb.is_none() { gdb = Some(arg); } else if out.is_none() { @@ -339,16 +385,25 @@ fn main() { got: String, med: u128, min: u128, + parse: u128, st: stats::TcStats, phases: [u128; 5], ok: bool, } println!( - "\n{:<26}{:<11}{:>7}{:>9}{:>13}{:>9}{:>7}{:>11}", - "case", "category", "exp", "got", "check_med_us", "refines", "hits", "edge_scan" + "\n{:<26}{:<11}{:>7}{:>9}{:>13}{:>10}{:>9}{:>7}{:>11}", + "case", + "category", + "exp", + "got", + "check_med_us", + "chk/parse", + "refines", + "hits", + "edge_scan" ); - println!("{}", "-".repeat(93)); + println!("{}", "-".repeat(103)); let mut rows: Vec = Vec::new(); let mut mismatches = 0usize; for (id, category, expected, q) in &cases { @@ -364,7 +419,12 @@ fn main() { "valid" }; - let (med, min) = time_case(&mut tc, &elaborated); + let (med, min) = if cold { + time_case_cold(&schema, &elaborated) + } else { + time_case(&mut tc, &elaborated) + }; + let parse = time_parse(q); // One un-timed run for the counter shape, one profiled run for the // phase split. Both after the timed loop so they cannot pollute it. @@ -387,12 +447,13 @@ fn main() { mismatches += 1; } println!( - "{:<26}{:<11}{:>7}{:>9}{:>13.3}{:>9}{:>7}{:>11}{}", + "{:<26}{:<11}{:>7}{:>9}{:>13.3}{:>10.2}{:>9}{:>7}{:>11}{}", id, category, expected, got, med as f64 / 1000.0, + med as f64 / parse.max(1) as f64, st.refine_calls, st.refine_cache_hits, st.edge_entries_scanned, @@ -405,17 +466,18 @@ fn main() { got: got.to_string(), med, min, + parse, st, phases, ok, }); } - println!("{}", "-".repeat(93)); + println!("{}", "-".repeat(103)); let mut f = File::create(&out).unwrap_or_else(|e| panic!("create {out}: {e}")); writeln!( f, - "case,category,expected,got,check_med_ns,check_min_ns,\ + "case,category,expected,got,check_med_ns,check_min_ns,parse_med_ns,\ refine_calls,refine_cache_hits,node_scanned,edge_scanned,refine_to_nodes,\ env_meets,env_unions,env_outer_joins,env_to_groups,pt_meets,\ phase_pattern_ns,phase_rep_ns,phase_group_by_ns,phase_returns_ns,phase_order_by_ns,\ @@ -425,13 +487,14 @@ fn main() { for r in &rows { writeln!( f, - "{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{}", + "{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{},{}", r.id, r.category, r.expected, r.got, r.med, r.min, + r.parse, r.st.refine_calls, r.st.refine_cache_hits, r.st.node_entries_scanned, diff --git a/src/typing/checker.rs b/src/typing/checker.rs index 6106c2e..a433491 100644 --- a/src/typing/checker.rs +++ b/src/typing/checker.rs @@ -15,7 +15,8 @@ use crate::syntax::query::{Aggregator, MatchStatement, Query, ReturnItem, SortKe use super::descriptor_type::DescriptorType; use super::label_type::LabelType; -use super::path_type::{EdgeDir, PathType}; +use super::path_summary::PathSummary; +use super::path_type::EdgeDir; use super::property_type::PropertyType; use super::simple_type::SimpleType; use super::type_environment::TypeEnvironment; @@ -40,16 +41,20 @@ pub struct PhaseProfile { } /// Result of type-checking a path pattern or query. +/// +/// `path` is the boundary-pair summary (`PathSummary`), the checker's +/// evaluation form of the paper's inductive path type — see +/// `path_summary.rs` for the correspondence. #[derive(Clone, Debug)] pub struct TypecheckResult { - pub path: PathType, + pub path: PathSummary, pub env: TypeEnvironment, pub ok: bool, pub empty: bool, } impl TypecheckResult { - fn new(path: PathType, env: TypeEnvironment) -> Self { + fn new(path: PathSummary, env: TypeEnvironment) -> Self { TypecheckResult { path, env, @@ -573,7 +578,7 @@ impl Typechecker { match node { PathPattern::Node(desc) => { let t = self.refine_pattern_node(desc); - let p = PathType::from_variable(&t, EdgeDir::Any); + let p = PathSummary::from_variable(&t, EdgeDir::Any); let env = create_context(desc, t); TypecheckResult::new(p, env) } @@ -600,7 +605,7 @@ impl Typechecker { self.warn_for_collapsed_bindings(&cm, &r1.env, &r2.env); - let p = PathType::meet(&self.schema, &r1.path, &r2.path); + let p = PathSummary::meet(&self.schema, &r1.path, &r2.path); TypecheckResult::new(p, cm) } @@ -625,7 +630,7 @@ impl Typechecker { self.warn_for_collapsed_bindings(&cm, &r1.env, &r2.env); let p = if r1.path.is_unsatisfiable() || r2.path.is_unsatisfiable() { - PathType::Zero + PathSummary::zero() } else { r1.path }; @@ -654,7 +659,7 @@ impl Typechecker { "Filter expression has type {}, which is not a boolean", t )); - TypecheckResult::new(PathType::Zero, r.env) + TypecheckResult::new(PathSummary::zero(), r.env) } else { r } @@ -664,7 +669,7 @@ impl Typechecker { let r1 = self.check_path_pattern(p1); let r2 = self.check_path_pattern(p2); TypecheckResult::new( - PathType::union(r1.path, r2.path), + PathSummary::union(r1.path, r2.path), TypeEnvironment::union(&r1.env, &r2.env), ) } @@ -727,7 +732,7 @@ impl Typechecker { fn check_edge(&mut self, dir: EdgeDir, desc: &Option) -> TypecheckResult { let t = self.refine_pattern_edge(dir, desc); - let p = PathType::from_variable(&t, dir); + let p = PathSummary::from_variable(&t, dir); let env = create_context(desc, t); TypecheckResult::new(p, env) } @@ -1075,7 +1080,7 @@ impl Typechecker { // from `outer` directly, so the only up-front clone is the one // pushed onto the ambient stack. let mut env: Option = None; - let mut path: Option = None; + let mut path: Option = None; // Make the outer environment available to the body's `Filter` // predicates so a correlated WHERE (e.g. `WHERE x IN NODES(path)`) // can reference outer-bound variables. The runtime evaluates such a @@ -1109,7 +1114,7 @@ impl Typechecker { } self.ambient_env.pop(); let env = env.unwrap_or_else(|| outer.clone()); - let path = path.unwrap_or(PathType::Zero); + let path = path.unwrap_or_else(PathSummary::zero); let mut r = TypecheckResult::new(path, env); r.empty = r.path.is_unsatisfiable() || r.env.is_empty(); r @@ -1228,12 +1233,8 @@ impl Typechecker { } /// p^0 = identity (default node path), p^1 = p, p^n = meet(p, p^(n-1)). - fn pow_path_type(&self, p: &PathType, n: u64) -> PathType { - match n { - 0 => PathType::default(), - 1 => p.clone(), - _ => PathType::meet(&self.schema, p, &self.pow_path_type(p, n - 1)), - } + fn pow_path_type(&self, p: &PathSummary, n: u64) -> PathSummary { + PathSummary::pow(&self.schema, p, n) } } diff --git a/src/typing/mod.rs b/src/typing/mod.rs index e7276e8..b77675e 100644 --- a/src/typing/mod.rs +++ b/src/typing/mod.rs @@ -3,6 +3,7 @@ pub mod descriptor_type; pub mod format; pub mod inference; pub mod label_type; +pub mod path_summary; pub mod path_type; pub mod property_type; pub mod simple_type; diff --git a/src/typing/path_summary.rs b/src/typing/path_summary.rs new file mode 100644 index 0000000..ff16711 --- /dev/null +++ b/src/typing/path_summary.rs @@ -0,0 +1,282 @@ +//! Boundary-pair summary of a path type — the checker's evaluation +//! representation. +//! +//! The inductive `PathType` (`path_type.rs`, the paper's definition) stores +//! every interior node of every union arm, and its `meet` clones the whole +//! prefix per refined junction arm. On patterns whose positions refine into +//! wide unions (unlabeled chains against a real schema) the tree grows +//! multiplicatively per hop — `()-[]->()` ×16 on LDBC SF0.1 measured ~23 s +//! per check (2026-07 baseline), with memory growth severe enough to push +//! an 8 GiB machine toward swap (peak RSS was not instrumented). +//! +//! The observation that fixes it: once a segment is met and pruned, its +//! interior nodes are never consulted again. Every judgment the checker +//! makes — `is_unsatisfiable` (the `guaranteed_empty` source), +//! `is_empty`/`len` (the repeat-length checks), and further concatenation +//! `meet`s (which only join the left's *last* node with the right's +//! *first*) — factors through the path's **boundary summary**: +//! +//! * `nodes` — the zero-length arms. A zero-length arm is a single node, +//! so first ≡ last and a descriptor set suffices. Kept separate from +//! `pairs` because zero-length arms concatenate differently: their node +//! IS the junction, so the refined junction becomes the exposed +//! boundary. +//! * `pairs` — the edge-bearing arms as `(first, last) → min edge count` +//! (≥ 1). Arms sharing a boundary are interchangeable under every +//! further operation except the length judgment, for which the minimum +//! is exactly what `len()` observes. +//! +//! Width is bounded by |schema.nodes|² + |schema.nodes| regardless of +//! pattern length, so concatenation cost is independent of chain position +//! and the exponential disappears. +//! +//! Correspondence with the spec type: `PathSummary` is the image of the +//! abstraction `summarize : PathType → PathSummary`, and the lattice +//! operations commute with it — +//! `summarize(meet(p, q)) = meet(summarize(p), summarize(q))` (same for +//! `union`) — with `is_unsatisfiable`/`is_empty`/`len` agreeing with the +//! satisfiability-aware ("live") reading of the spec type. Pinned by +//! `tests/path_summary_hom_proptest.rs`. One deliberate divergence: the +//! spec type's own `len`/`is_empty` are satisfiability-blind on dead arms +//! (`Edge{p1: Zero, ..}` counts as length 1), which made the repeat-length +//! warning fire or not depending on *how* an inner pattern died; the +//! summary implements the live semantics uniformly (a dead inner is +//! "empty", matching the old `Zero` branch). +//! +//! Invariant relied on (holds for every checker-reachable path): schema +//! entries carry non-empty descriptors, and `refine`/`refine_to_nodes` +//! outputs are meets of matching entries, so satisfiable arms never carry +//! empty descriptors — unsatisfiability always surfaces as the absence of +//! arms. + +use std::collections::{HashMap, HashSet}; + +use super::descriptor_type::DescriptorType; +use super::path_type::{EdgeDir, PathType}; +use super::variable_type::{Schema, VariableType}; + +/// Boundary summary: zero-length arms as a node-descriptor set, edge- +/// bearing arms as `(first, last) → min edge count`. Both empty ⇔ the +/// path is unsatisfiable (`PathType::Zero`). +#[derive(Debug, Clone, PartialEq, Eq, Default)] +pub struct PathSummary { + nodes: HashSet, + pairs: HashMap<(DescriptorType, DescriptorType), usize>, +} + +impl PathSummary { + /// Bottom — no satisfiable arm. Mirrors `PathType::Zero`. + pub fn zero() -> Self { + PathSummary::default() + } + + /// A single-node path. Mirrors `PathType::Node`. + pub fn node(desc: DescriptorType) -> Self { + let mut nodes = HashSet::with_capacity(1); + nodes.insert(desc); + PathSummary { + nodes, + pairs: HashMap::new(), + } + } + + /// Mirrors `PathType::default()`: the anonymous star node. + pub fn star_node() -> Self { + PathSummary::node(DescriptorType::star()) + } + + /// Mirrors `PathType::from_variable`: build from a (refined) variable + /// type and the direction the edge is observed at. + pub fn from_variable(t: &VariableType, dir: EdgeDir) -> Self { + match t { + VariableType::Node(d) => PathSummary::node(d.clone()), + VariableType::EdgeDirectional { left, right, .. } => { + directed_edge_pairs(left, right, dir) + } + // Undirected: both orientations regardless of dir (as the + // spec's `from_variable` does). + VariableType::EdgeNonDirectional { left, right, .. } => { + directed_edge_pairs(left, right, EdgeDir::Any) + } + VariableType::Union(t1, t2) => PathSummary::union( + PathSummary::from_variable(t1, dir), + PathSummary::from_variable(t2, dir), + ), + VariableType::Group(_) + | VariableType::Null + | VariableType::Path + | VariableType::Zero => PathSummary::zero(), + } + } + + /// Minimum edge count over live arms (0 when unsatisfiable, matching + /// `PathType::Zero::len()`). + pub fn len(&self) -> usize { + if !self.nodes.is_empty() { + return 0; + } + self.pairs.values().copied().min().unwrap_or(0) + } + + /// True when some live arm has no edges — or when there is no live + /// arm at all (mirrors the spec: both `Node` and `Zero` are empty). + pub fn is_empty(&self) -> bool { + !self.nodes.is_empty() || self.pairs.is_empty() + } + + /// Bottom check — no live arm remains. + pub fn is_unsatisfiable(&self) -> bool { + self.nodes.is_empty() && self.pairs.is_empty() + } + + fn insert_pair(&mut self, key: (DescriptorType, DescriptorType), len: usize) { + debug_assert!(len >= 1, "edge-bearing pair with zero length"); + self.pairs + .entry(key) + .and_modify(|l| *l = (*l).min(len)) + .or_insert(len); + } + + /// Least upper bound: arm-set union (min length per edge boundary). + /// Mirrors `PathType::union` (Zero is identity). + pub fn union(a: PathSummary, b: PathSummary) -> PathSummary { + let (mut big, small) = if a.nodes.len() + a.pairs.len() >= b.nodes.len() + b.pairs.len() { + (a, b) + } else { + (b, a) + }; + big.nodes.extend(small.nodes); + for (k, l) in small.pairs { + big.insert_pair(k, l); + } + big + } + + /// Greatest lower bound — path concatenation joining `a`'s last node + /// with `b`'s first node, exactly as `PathType::meet` does: the + /// junction descriptors are met and re-refined against the schema + /// (`refine_to_nodes`). A zero-length side's node IS the junction, so + /// it adopts the refined junction as its exposed boundary; a + /// positive-length side keeps its own outer boundary (the junction + /// becomes interior and is dropped). + pub fn meet(schema: &Schema, a: &PathSummary, b: &PathSummary) -> PathSummary { + super::stats::record_pathtype_meet(); + let mut out = PathSummary::zero(); + // The junction only depends on (a.last, b.first); memoize per + // call so w×w arm combos cost w distinct refinements. + let mut junctions: HashMap<(DescriptorType, DescriptorType), Vec> = + HashMap::new(); + let mut junction = |l1: &DescriptorType, f2: &DescriptorType| -> Vec { + junctions + .entry((l1.clone(), f2.clone())) + .or_insert_with(|| { + let met = VariableType::Node(DescriptorType::meet(l1, f2)); + VariableType::refine_to_nodes(schema, &met) + .into_iter() + .filter_map(|v| match v { + VariableType::Node(d) => Some(d), + _ => None, + }) + .collect() + }) + .clone() + }; + + // pairs × pairs: junction interior, outer boundaries survive. + for ((f1, l1), &len1) in &a.pairs { + for ((f2, l2), &len2) in &b.pairs { + if !junction(l1, f2).is_empty() { + out.insert_pair((f1.clone(), l2.clone()), len1 + len2); + } + } + } + // pairs × nodes: the zero-length right is the junction; the + // refined junction becomes the result's last boundary. + for ((f1, l1), &len1) in &a.pairs { + for d in &b.nodes { + for r in junction(l1, d) { + out.insert_pair((f1.clone(), r), len1); + } + } + } + // nodes × pairs: symmetric — refined junction becomes first. + for d in &a.nodes { + for ((f2, l2), &len2) in &b.pairs { + for r in junction(d, f2) { + out.insert_pair((r, l2.clone()), len2); + } + } + } + // nodes × nodes: both are the junction; result is the refined + // node itself. + for d1 in &a.nodes { + for d2 in &b.nodes { + for r in junction(d1, d2) { + out.nodes.insert(r); + } + } + } + out + } + + /// `p^0` = the identity node path, `p^n = meet(p, p^{n-1})`. Mirrors + /// the checker's `pow_path_type`. + pub fn pow(schema: &Schema, p: &PathSummary, n: u64) -> PathSummary { + match n { + 0 => PathSummary::star_node(), + 1 => p.clone(), + _ => PathSummary::meet(schema, p, &PathSummary::pow(schema, p, n - 1)), + } + } + + /// Abstraction function from the spec type. `Edge` exposes its `n2` + /// as the last boundary and discards the prefix's own last boundary + /// (it became interior when the edge was appended); a dead arm + /// (empty descriptor or `Zero` prefix) contributes nothing, giving + /// the live semantics documented above. + pub fn summarize(p: &PathType) -> PathSummary { + match p { + PathType::Zero => PathSummary::zero(), + PathType::Node(n) => { + if n.desc.is_empty() { + PathSummary::zero() + } else { + PathSummary::node(n.desc.clone()) + } + } + PathType::Edge(e) => { + if e.n2.desc.is_empty() { + return PathSummary::zero(); + } + let prefix = PathSummary::summarize(&e.p1); + let mut out = PathSummary::zero(); + for d in &prefix.nodes { + out.insert_pair((d.clone(), e.n2.desc.clone()), 1); + } + for ((f, _), &len) in &prefix.pairs { + out.insert_pair((f.clone(), e.n2.desc.clone()), len + 1); + } + out + } + PathType::Union(p1, p2) => { + PathSummary::union(PathSummary::summarize(p1), PathSummary::summarize(p2)) + } + } + } +} + +/// Mirrors `path_type.rs::directed_edge_to_path` in pair form. +fn directed_edge_pairs(left: &VariableType, right: &VariableType, dir: EdgeDir) -> PathSummary { + let (l, r) = match (left, right) { + (VariableType::Node(l), VariableType::Node(r)) => (l, r), + _ => return PathSummary::zero(), + }; + let mut out = PathSummary::zero(); + if matches!(dir, EdgeDir::Right | EdgeDir::Any | EdgeDir::None) { + out.insert_pair((l.clone(), r.clone()), 1); + } + if matches!(dir, EdgeDir::Left | EdgeDir::Any | EdgeDir::None) { + out.insert_pair((r.clone(), l.clone()), 1); + } + out +} diff --git a/tests/path_summary_hom_proptest.proptest-regressions b/tests/path_summary_hom_proptest.proptest-regressions new file mode 100644 index 0000000..0756ee0 --- /dev/null +++ b/tests/path_summary_hom_proptest.proptest-regressions @@ -0,0 +1,9 @@ +# Seeds for failure cases proptest has generated in the past. It is +# automatically read and these particular cases re-run before any +# novel cases are generated. +# +# It is recommended to check this file in to source control so that +# everyone who runs the test benefits from these saved cases. +cc e8a232a42f2f0a77594610ee83fabe10800c0e5c5efb354d3bcf9d951b6132ea # shrinks to p = Edge(EdgePathType { p1: Edge(EdgePathType { p1: Node(NodePathType { desc: DescriptorType { label: Star, props: Open({}) } }), n2: NodePathType { desc: DescriptorType { label: Star, props: Open({}) } } }), n2: NodePathType { desc: DescriptorType { label: Star, props: Open({"k1": Z}) } } }), q = Union(Edge(EdgePathType { p1: Node(NodePathType { desc: DescriptorType { label: Label("B"), props: Open({}) } }), n2: NodePathType { desc: DescriptorType { label: Label("B"), props: Open({}) } } }), Union(Node(NodePathType { desc: DescriptorType { label: Star, props: Open({}) } }), Node(NodePathType { desc: DescriptorType { label: Label("B"), props: Open({}) } }))) +cc 7a6c6f984f33966072c8aae6a4ce28b8dc9e5f9190b5fb608d8dcd0a4df5d34e # shrinks to p = Edge(EdgePathType { p1: Union(Edge(EdgePathType { p1: Node(NodePathType { desc: DescriptorType { label: Star, props: Open({}) } }), n2: NodePathType { desc: DescriptorType { label: Star, props: Open({}) } } }), Zero), n2: NodePathType { desc: DescriptorType { label: Star, props: Open({}) } } }), q = Node(NodePathType { desc: DescriptorType { label: Star, props: Open({}) } }) +cc 52450c19fe4aed9df352435e42c407bdfacb1910e60b5a4f2889fe0e0baa760c # shrinks to p = Union(Edge(EdgePathType { p1: Edge(EdgePathType { p1: Node(NodePathType { desc: DescriptorType { label: Star, props: Open({}) } }), n2: NodePathType { desc: DescriptorType { label: Star, props: Open({}) } } }), n2: NodePathType { desc: DescriptorType { label: Star, props: Open({}) } } }), Edge(EdgePathType { p1: Zero, n2: NodePathType { desc: DescriptorType { label: Star, props: Open({}) } } })), q = Node(NodePathType { desc: DescriptorType { label: Star, props: Open({}) } }) diff --git a/tests/path_summary_hom_proptest.rs b/tests/path_summary_hom_proptest.rs new file mode 100644 index 0000000..086c09f --- /dev/null +++ b/tests/path_summary_hom_proptest.rs @@ -0,0 +1,221 @@ +//! Abstraction-soundness suite for `PathSummary` (the checker's +//! evaluation representation) against the inductive `PathType` (the +//! paper's spec type, `rules.md` §4/§8). +//! +//! The claim pinned here is that `summarize : PathType → PathSummary` is a +//! lattice homomorphism on the checker-reachable domain: +//! +//! summarize(meet_S(p, q)) = meet_S(summarize(p), summarize(q)) +//! summarize(union(p, q)) = union(summarize(p), summarize(q)) +//! +//! and that the judgments the checker consumes factor through it: +//! `is_unsatisfiable` agrees everywhere on the domain, and +//! `is_empty` / `len` agree on satisfiable values (the spec type's length +//! functions are satisfiability-blind on dead arms — e.g. +//! `Edge{p1: Zero, ..}` reports len 1 — but the checker never holds such a +//! value: meets prune them and constructors cannot produce them). +//! +//! Domain restriction: descriptors are generated non-empty (no +//! `PropertyType::Zero`), matching the checker-reachable invariant +//! documented in `path_summary.rs`. + +use proptest::prelude::*; +use std::collections::BTreeMap; + +use frogql::typing::descriptor_type::DescriptorType; +use frogql::typing::label_type::LabelType; +use frogql::typing::path_summary::PathSummary; +use frogql::typing::path_type::{EdgePathType, NodePathType, PathType}; +use frogql::typing::property_type::PropertyType; +use frogql::typing::simple_type::SimpleType; +use frogql::typing::variable_type::{Schema, VariableType}; + +fn arb_label() -> impl Strategy { + prop_oneof![ + Just(LabelType::Star), + Just(LabelType::Label("A".into())), + Just(LabelType::Label("B".into())), + Just(LabelType::Label("C".into())), + ] +} + +fn arb_props() -> impl Strategy { + let kv = prop_oneof![ + Just(("k1".to_string(), SimpleType::Z)), + Just(("k2".to_string(), SimpleType::S)), + Just(("k3".to_string(), SimpleType::B)), + ]; + proptest::collection::vec(kv, 0..3) + .prop_map(|kvs| PropertyType::Open(kvs.into_iter().collect::>())) +} + +fn arb_desc() -> impl Strategy { + (arb_label(), arb_props()).prop_map(|(l, p)| DescriptorType::new(l, p)) +} + +// Domain-faithful generator: the checker only ever builds unions through +// the `PathType::union` smart constructor (which drops `Zero` arms and +// collapses exact duplicates) — `from_variable`, `meet`'s distribution, +// and `union_from_list` all route through it. Raw `Union(_, Zero)` trees +// are unreachable and sit outside the abstraction's domain (the spec +// `len`/`is_empty` are satisfiability-blind on such dead arms), so the +// generator composes unions the same way the checker does. +fn arb_path() -> impl Strategy { + let leaf = prop_oneof![ + 2 => arb_desc().prop_map(PathType::node), + 1 => Just(PathType::Zero), + ]; + leaf.prop_recursive(4, 24, 3, |inner| { + prop_oneof![ + (inner.clone(), arb_desc()).prop_map(|(p1, d)| PathType::Edge(EdgePathType { + p1: Box::new(p1), + n2: NodePathType::new(d), + })), + (inner.clone(), inner).prop_map(|(a, b)| PathType::union(a, b)), + ] + }) +} + +/// A small non-trivial schema: three labeled node types with props, and +/// directed A→B, B→C plus an undirected B~B edge entry. +fn labeled_schema() -> Schema { + let node = |l: &str, k: &str, t: SimpleType| { + VariableType::Node(DescriptorType::new( + LabelType::Label(l.into()), + PropertyType::Open([(k.to_string(), t)].into_iter().collect()), + )) + }; + let a = node("A", "k1", SimpleType::Z); + let b = node("B", "k2", SimpleType::S); + let c = node("C", "k3", SimpleType::B); + let edge = |desc_label: &str, l: &VariableType, r: &VariableType, directed: bool| { + let desc = DescriptorType::new( + LabelType::Label(desc_label.into()), + PropertyType::open_empty(), + ); + if directed { + VariableType::EdgeDirectional { + desc, + left: Box::new(l.clone()), + right: Box::new(r.clone()), + } + } else { + VariableType::EdgeNonDirectional { + desc, + left: Box::new(l.clone()), + right: Box::new(r.clone()), + } + } + }; + let edges = vec![ + edge("ab", &a, &b, true), + edge("bc", &b, &c, true), + edge("bb", &b, &b, false), + ]; + Schema::from_parts(vec![a, b, c], edges) +} + +/// Satisfiability-aware length on the spec type: minimum edge count over +/// *live* (satisfiable) arms, `None` when no arm survives. This is the +/// reference for `PathSummary::len`/`is_empty` — the spec type's own +/// `len()`/`is_empty()` are satisfiability-blind (they count dead arms +/// like `Edge{p1: Zero, ..}`), which made the old repeat-length warning +/// inconsistent: whether it fired for a dead inner depended on how the +/// inner died. The summary implements the live semantics uniformly. +fn live_len(p: &PathType) -> Option { + match p { + PathType::Zero => None, + PathType::Node(n) => { + if n.desc.is_empty() { + None + } else { + Some(0) + } + } + PathType::Edge(e) => { + if e.n2.desc.is_empty() { + None + } else { + live_len(&e.p1).map(|l| l + 1) + } + } + PathType::Union(a, b) => match (live_len(a), live_len(b)) { + (Some(x), Some(y)) => Some(x.min(y)), + (x, None) => x, + (None, y) => y, + }, + } +} + +fn hom_checks(schema: &Schema, p: &PathType, q: &PathType) -> Result<(), TestCaseError> { + let sp = PathSummary::summarize(p); + let sq = PathSummary::summarize(q); + + // Homomorphism: meet and union commute with summarize. + let spec_meet = PathSummary::summarize(&PathType::meet(schema, p, q)); + let eval_meet = PathSummary::meet(schema, &sp, &sq); + prop_assert_eq!( + spec_meet, + eval_meet, + "meet hom failed\n p={:?}\n q={:?}", + p, + q + ); + + let spec_union = PathSummary::summarize(&PathType::union(p.clone(), q.clone())); + let eval_union = PathSummary::union(sp.clone(), sq.clone()); + prop_assert_eq!( + spec_union, + eval_union, + "union hom failed\n p={:?}\n q={:?}", + p, + q + ); + + // Judgment agreement against the live reference. + let live = live_len(p); + prop_assert_eq!( + p.is_unsatisfiable(), + live.is_none(), + "spec unsat vs live: {:?}", + p + ); + prop_assert_eq!( + sp.is_unsatisfiable(), + live.is_none(), + "summary unsat: {:?}", + p + ); + prop_assert_eq!(sp.len(), live.unwrap_or(0), "summary len vs live: {:?}", p); + prop_assert_eq!( + sp.is_empty(), + live.map_or(true, |l| l == 0), + "summary is_empty vs live: {:?}", + p + ); + // On fully-live paths the blind and live semantics coincide, so the + // spec's own judgments agree too. + if live.is_some() && p.len() == live.unwrap() { + prop_assert_eq!( + p.is_empty(), + sp.is_empty(), + "is_empty on live path: {:?}", + p + ); + } + Ok(()) +} + +proptest! { + #![proptest_config(ProptestConfig::with_cases(512))] + + #[test] + fn hom_star_schema(p in arb_path(), q in arb_path()) { + hom_checks(&Schema::star(), &p, &q)?; + } + + #[test] + fn hom_labeled_schema(p in arb_path(), q in arb_path()) { + hom_checks(&labeled_schema(), &p, &q)?; + } +} From f038ac27fa84b63c1db617631f91a1f9f4e621ac Mon Sep 17 00:00:00 2001 From: Felipe705x Date: Thu, 23 Jul 2026 21:58:45 -0400 Subject: [PATCH 2/2] =?UTF-8?q?perf(typing):=20flat=20PathSummary=20arms?= =?UTF-8?q?=20=E2=80=94=20typical=20queries=20back=20to=20QW3-level?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Goal realignment (user directive): optimize for queries users actually type (1–4 hop labeled patterns, subqueries, OPTIONALs); the synthetic scaling families remain cliff guards only. The hash-based PathSummary regressed exactly those typical shapes by 25–50% (subq_exists 58→87 us, multi_optional 105→157 us vs the QW3 state): every operation allocated a HashMap/HashSet and hashing walks the ENTIRE rich descriptor (label + property BTreeMap) on every insert and lookup, while typical paths summarize to 1–3 arms. Arms now live in flat Vecs deduplicated by linear equality scan — an equality probe fails fast on the label, and the O(w²) scan is bounded by the schema (the ×16 unlabeled cliff guard stays ~24 ms, still ~970× better than the pre-PathSummary 23.3 s). Set semantics preserved via a manual order-insensitive PartialEq; the junction memo keys by pointer identity (a value-equal miss just recomputes). Idle-machine numbers vs QW3 (the previous typical-query optimum): - subq_exists 61.0 us (+5%) multi_optional 108.0 us (+3%) - union_2 31.8 us (+2%) union_8 146.0 us (+4%) - chain_1 14.9 us (+15%, ~2 us) repeat_1_3 15.5 us (+13%, ~2 us) - chain_4 55.5 us (−10%) chain_16 234 us (−33%) - anydir_8 129.7 us (−12%) anon_16 cliff guard: 24.1 ms Hom proptest (summarize ∘ meet ≡ meet ∘ summarize) and all suites green; full sweep 80 targets. Co-Authored-By: Claude Fable 5 --- src/typing/path_summary.rs | 142 ++++++++++++++++++++++++------------- 1 file changed, 91 insertions(+), 51 deletions(-) diff --git a/src/typing/path_summary.rs b/src/typing/path_summary.rs index ff16711..7bd96f6 100644 --- a/src/typing/path_summary.rs +++ b/src/typing/path_summary.rs @@ -21,8 +21,8 @@ //! `pairs` because zero-length arms concatenate differently: their node //! IS the junction, so the refined junction becomes the exposed //! boundary. -//! * `pairs` — the edge-bearing arms as `(first, last) → min edge count` -//! (≥ 1). Arms sharing a boundary are interchangeable under every +//! * `pairs` — the edge-bearing arms as `(first, last, min edge count)` +//! (count ≥ 1). Arms sharing a boundary are interchangeable under every //! further operation except the length judgment, for which the minimum //! is exactly what `len()` observes. //! @@ -30,6 +30,16 @@ //! pattern length, so concatenation cost is independent of chain position //! and the exponential disappears. //! +//! Representation note: arms live in flat `Vec`s deduplicated by linear +//! equality scan, NOT hash sets. Queries users actually type summarize to +//! 1–3 arms, where a hash structure loses twice: allocation/setup per +//! operation, and hashing must walk the *entire* rich descriptor +//! (label + property `BTreeMap`) on every insert and lookup, while an +//! equality probe fails fast on the label. The linear scan is O(w²) in +//! arm width, bounded by the schema as above; the synthetic unlabeled +//! families are cliff guards, not tuning targets. Set semantics are +//! preserved by a manual order-insensitive `PartialEq`. +//! //! Correspondence with the spec type: `PathSummary` is the image of the //! abstraction `summarize : PathType → PathSummary`, and the lattice //! operations commute with it — @@ -49,20 +59,36 @@ //! empty descriptors — unsatisfiability always surfaces as the absence of //! arms. -use std::collections::{HashMap, HashSet}; - use super::descriptor_type::DescriptorType; use super::path_type::{EdgeDir, PathType}; use super::variable_type::{Schema, VariableType}; /// Boundary summary: zero-length arms as a node-descriptor set, edge- -/// bearing arms as `(first, last) → min edge count`. Both empty ⇔ the -/// path is unsatisfiable (`PathType::Zero`). -#[derive(Debug, Clone, PartialEq, Eq, Default)] +/// bearing arms as `(first, last, min edge count)`. Both empty ⇔ the +/// path is unsatisfiable (`PathType::Zero`). Set semantics with `Vec` +/// storage — see the module's representation note. +#[derive(Debug, Clone, Default)] pub struct PathSummary { - nodes: HashSet, - pairs: HashMap<(DescriptorType, DescriptorType), usize>, + nodes: Vec, + pairs: Vec<(DescriptorType, DescriptorType, usize)>, +} + +/// Order-insensitive set equality (arm order is an artifact of +/// construction order, never meaningful). +impl PartialEq for PathSummary { + fn eq(&self, other: &Self) -> bool { + self.nodes.len() == other.nodes.len() + && self.pairs.len() == other.pairs.len() + && self.nodes.iter().all(|d| other.nodes.contains(d)) + && self.pairs.iter().all(|(f, l, n)| { + other + .pairs + .iter() + .any(|(f2, l2, n2)| f == f2 && l == l2 && n == n2) + }) + } } +impl Eq for PathSummary {} impl PathSummary { /// Bottom — no satisfiable arm. Mirrors `PathType::Zero`. @@ -72,11 +98,9 @@ impl PathSummary { /// A single-node path. Mirrors `PathType::Node`. pub fn node(desc: DescriptorType) -> Self { - let mut nodes = HashSet::with_capacity(1); - nodes.insert(desc); PathSummary { - nodes, - pairs: HashMap::new(), + nodes: vec![desc], + pairs: Vec::new(), } } @@ -115,7 +139,7 @@ impl PathSummary { if !self.nodes.is_empty() { return 0; } - self.pairs.values().copied().min().unwrap_or(0) + self.pairs.iter().map(|&(_, _, n)| n).min().unwrap_or(0) } /// True when some live arm has no edges — or when there is no live @@ -129,12 +153,21 @@ impl PathSummary { self.nodes.is_empty() && self.pairs.is_empty() } - fn insert_pair(&mut self, key: (DescriptorType, DescriptorType), len: usize) { + fn insert_node(&mut self, d: DescriptorType) { + if !self.nodes.contains(&d) { + self.nodes.push(d); + } + } + + fn insert_pair(&mut self, f: DescriptorType, l: DescriptorType, len: usize) { debug_assert!(len >= 1, "edge-bearing pair with zero length"); - self.pairs - .entry(key) - .and_modify(|l| *l = (*l).min(len)) - .or_insert(len); + for (f2, l2, n) in self.pairs.iter_mut() { + if *f2 == f && *l2 == l { + *n = (*n).min(len); + return; + } + } + self.pairs.push((f, l, len)); } /// Least upper bound: arm-set union (min length per edge boundary). @@ -145,9 +178,11 @@ impl PathSummary { } else { (b, a) }; - big.nodes.extend(small.nodes); - for (k, l) in small.pairs { - big.insert_pair(k, l); + for d in small.nodes { + big.insert_node(d); + } + for (f, l, n) in small.pairs { + big.insert_pair(f, l, n); } big } @@ -162,48 +197,53 @@ impl PathSummary { pub fn meet(schema: &Schema, a: &PathSummary, b: &PathSummary) -> PathSummary { super::stats::record_pathtype_meet(); let mut out = PathSummary::zero(); - // The junction only depends on (a.last, b.first); memoize per - // call so w×w arm combos cost w distinct refinements. - let mut junctions: HashMap<(DescriptorType, DescriptorType), Vec> = - HashMap::new(); + // The junction only depends on (a.last, b.first). Memoized by + // pointer identity of the operand descriptors — w×w arm combos + // cost w distinct refinements; a value-equal miss just recomputes. + let mut junctions: Vec<( + *const DescriptorType, + *const DescriptorType, + Vec, + )> = Vec::new(); let mut junction = |l1: &DescriptorType, f2: &DescriptorType| -> Vec { - junctions - .entry((l1.clone(), f2.clone())) - .or_insert_with(|| { - let met = VariableType::Node(DescriptorType::meet(l1, f2)); - VariableType::refine_to_nodes(schema, &met) - .into_iter() - .filter_map(|v| match v { - VariableType::Node(d) => Some(d), - _ => None, - }) - .collect() + let key = (l1 as *const _, f2 as *const _); + if let Some((_, _, rs)) = junctions.iter().find(|(p1, p2, _)| (*p1, *p2) == key) { + return rs.clone(); + } + let met = VariableType::Node(DescriptorType::meet(l1, f2)); + let rs: Vec = VariableType::refine_to_nodes(schema, &met) + .into_iter() + .filter_map(|v| match v { + VariableType::Node(d) => Some(d), + _ => None, }) - .clone() + .collect(); + junctions.push((key.0, key.1, rs.clone())); + rs }; // pairs × pairs: junction interior, outer boundaries survive. - for ((f1, l1), &len1) in &a.pairs { - for ((f2, l2), &len2) in &b.pairs { + for (f1, l1, len1) in &a.pairs { + for (f2, l2, len2) in &b.pairs { if !junction(l1, f2).is_empty() { - out.insert_pair((f1.clone(), l2.clone()), len1 + len2); + out.insert_pair(f1.clone(), l2.clone(), len1 + len2); } } } // pairs × nodes: the zero-length right is the junction; the // refined junction becomes the result's last boundary. - for ((f1, l1), &len1) in &a.pairs { + for (f1, l1, len1) in &a.pairs { for d in &b.nodes { for r in junction(l1, d) { - out.insert_pair((f1.clone(), r), len1); + out.insert_pair(f1.clone(), r, *len1); } } } // nodes × pairs: symmetric — refined junction becomes first. for d in &a.nodes { - for ((f2, l2), &len2) in &b.pairs { + for (f2, l2, len2) in &b.pairs { for r in junction(d, f2) { - out.insert_pair((r, l2.clone()), len2); + out.insert_pair(r, l2.clone(), *len2); } } } @@ -212,7 +252,7 @@ impl PathSummary { for d1 in &a.nodes { for d2 in &b.nodes { for r in junction(d1, d2) { - out.nodes.insert(r); + out.insert_node(r); } } } @@ -251,10 +291,10 @@ impl PathSummary { let prefix = PathSummary::summarize(&e.p1); let mut out = PathSummary::zero(); for d in &prefix.nodes { - out.insert_pair((d.clone(), e.n2.desc.clone()), 1); + out.insert_pair(d.clone(), e.n2.desc.clone(), 1); } - for ((f, _), &len) in &prefix.pairs { - out.insert_pair((f.clone(), e.n2.desc.clone()), len + 1); + for (f, _, len) in &prefix.pairs { + out.insert_pair(f.clone(), e.n2.desc.clone(), len + 1); } out } @@ -273,10 +313,10 @@ fn directed_edge_pairs(left: &VariableType, right: &VariableType, dir: EdgeDir) }; let mut out = PathSummary::zero(); if matches!(dir, EdgeDir::Right | EdgeDir::Any | EdgeDir::None) { - out.insert_pair((l.clone(), r.clone()), 1); + out.insert_pair(l.clone(), r.clone(), 1); } if matches!(dir, EdgeDir::Left | EdgeDir::Any | EdgeDir::None) { - out.insert_pair((r.clone(), l.clone()), 1); + out.insert_pair(r.clone(), l.clone(), 1); } out }