From 0a93a83e971fd58310f36c7c7956ac882d37695b Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Fri, 7 Aug 2026 15:31:54 +0200 Subject: [PATCH] ogar-elk: borrowed lens over the baked edge table `ogar-elk` runs after the bake. Joining -- resolving a CURIE, reconciling which source asserts what -- completes upstream, and the bake freezes the result into positions; this crate observes what the resulting spine entails. The module documentation now states that position. The previous text placed the crate before the bake, which does not match what it consumes. The shape follows from the position: an observation over a bake borrows what the bake already holds. - `Closure`, which owned a `HashMap>`, becomes `Spine<'a>`, a lens over a sorted `&'a [Subsumption]` -- the caller's projection of `Bake::triples` to its is_a edges. The bake already lays that adjacency out in sorted order, so the map was a second copy of it, and a second copy is a second thing that can disagree with the first. - `from_asserted(impl IntoIterator)` becomes `Spine::over(&[..])`. - `parents_of` is an equal-range binary search returning a subslice of the caller's data. `parents_are_a_borrowed_window_not_a_copy` asserts pointer identity against the source slice, so the borrowing is verified rather than documented. - `extended`, which cloned the whole map, becomes `with_overlay`, a second borrowed slice. Evaluating a candidate merge now costs a lens. Sortedness is a precondition of the search: an unsorted slice makes it miss parents, surfacing as `entails() == false` -- a wrong answer that looks like a legitimate one. `over` debug-asserts it (the bake emits sorted output); `try_over` validates in release builds and returns None rather than sorting a copy, since sorting would reintroduce ownership. Two scope notes are now in the documentation. The `HashSet` in `supers_of` is the traversal frontier, holding the answer being accumulated, not a copy of the edge table. And R3 is not redundant with `ogar_obo::BakeStats::is_a_cycles`: that field reports cycles within a single baked core, whereas R3 reports what an additional axiom set would introduce into a spine already baked. 10 tests pass (up from 8; adds the borrowed-window and sortedness cases), clippy clean. --- crates/ogar-elk/src/lib.rs | 449 +++++++++++++++++++++++-------------- 1 file changed, 278 insertions(+), 171 deletions(-) diff --git a/crates/ogar-elk/src/lib.rs b/crates/ogar-elk/src/lib.rs index 334a57a..bfd95b3 100644 --- a/crates/ogar-elk/src/lib.rs +++ b/crates/ogar-elk/src/lib.rs @@ -1,4 +1,4 @@ -//! `ogar-elk` — the EL subsumption closure as a **factfinder**. +//! `ogar-elk` — the EL subsumption closure as an **observation over the bake**. //! //! # What this is, and the two questions it answers //! @@ -6,9 +6,9 @@ //! [`ogar-ro`] (the predicate palette). Those two say what is *asserted*; this //! one says what *follows*. It answers exactly two questions: //! -//! 1. **Does `A ⊑ B` follow** from the asserted edges? ([`Closure::entails`]) +//! 1. **Does `A ⊑ B` follow** from the baked edges? ([`Spine::entails`]) //! 2. **Is adding a set of axioms sound** — does the merged closure introduce -//! an equivalence cycle that was not already there? ([`Closure::merge`]) +//! an equivalence cycle that was not already there? ([`Spine::merge`]) //! //! Nothing here is graded, ranked, scored or weighted. An EL entailment is a //! **fact**: it follows necessarily from the asserted set, or it does not. The @@ -18,29 +18,34 @@ //! [`ogar-obo`]: https://docs.rs/ogar-obo //! [`ogar-ro`]: https://docs.rs/ogar-ro //! -//! # Where this runs: BEFORE the bake, never after +//! # Where this runs: AFTER the bake, over what the bake already holds //! -//! **The joins are pre-bake.** Reconciling independently authored sources — -//! deciding which assertions corroborate, which enrich, and which contradict — -//! is exactly the work that must finish before anything is baked, because the -//! bake is what freezes the answer into positions. So this crate is a **stage**, -//! not a layer: it runs once, upstream, and then it is done. +//! **The joins are pre-bake.** Reconciling which source says what, resolving a +//! CURIE, deciding that two labels name one concept — all of that finishes +//! upstream, and the bake freezes the result into positions. This crate runs on +//! the far side of that line: it is the **observation** of what the baked spine +//! entails, not a stage that produces one. //! -//! Three consequences follow, and they are the whole design: +//! Which is why it **borrows and never owns**. A [`Spine`] is a lens over a +//! sorted slice the bake already emitted — `ogar_obo::Bake::triples` projected +//! to its `is_a` edges. Parents are found by [`slice::binary_search`] over that +//! slice and returned **as a subslice of it**; the crate allocates nothing that +//! mirrors the substrate. Building a `HashMap<_, Vec<_>>` here would be a +//! second copy of an adjacency the bake already laid out in order, and a second +//! copy is a second thing that can be wrong. //! -//! 1. **Types are legal here.** [`ClassAddr`] and [`Subsumption`] exist because -//! a join needs a key and a directed edge. They are pre-bake scaffolding. -//! **Nothing this crate defines survives the bake** — afterwards there are -//! only classes, and a class is resolved by position, not by a type declared -//! here. If one of these types ever appears in a post-bake read path, that is -//! the leak, and it is this doc that says so. -//! 2. **Nothing here is in the hot path**, so nothing here may pretend to be. -//! There is no serialization surface — not behind a feature, not optionally. -//! A join validator that could serialize its verdict would invite someone to -//! ship the verdict instead of the bake. -//! 3. **No file, no CURIE, no label.** Input is already-joined addressed edges. -//! Reaching back for the source document would put parsing inside the -//! validator and re-introduce the coupling the bake exists to remove. +//! The one allocation a walk does make is its **frontier** — the set of nodes +//! already visited. That is the algorithm's working set, bounded by the size of +//! the answer, and it is not a duplicate of the data. +//! +//! # The one precondition +//! +//! Edges must be **sorted by subclass**. The bake emits them that way (its ids +//! are sorted before rows are packed), so [`Spine::over`] takes that on trust +//! and checks it in debug builds. A caller holding a slice of uncertain +//! provenance uses [`Spine::try_over`], which verifies in release too — an +//! unsorted slice makes the binary search silently miss parents, which would +//! read as "not entailed" and is the one failure this crate must not have. //! //! # The fragment, stated precisely //! @@ -61,6 +66,11 @@ //! mechanical — and it is found at **any distance**, including cycles that close //! through a chain no pairwise comparison would think to check. //! +//! Note what R3 is NOT a duplicate of: `ogar_obo::BakeStats::is_a_cycles` +//! reports cycles **inside one** baked core. R3 asks what a *further* set of +//! axioms would do to a spine already baked — the question you can only ask +//! once you have the bake to ask it about. +//! //! # What is deliberately NOT here //! //! - **Existential restrictions** (`∃r.C`) @@ -77,25 +87,21 @@ //! **The concrete hazard that boundary guards:** without role composition, //! walking subsumption and part-of edges together derives FALSE ancestors. //! `A part_of B` and `B ⊑ C` does not give `A ⊑ C`. This crate cannot make that -//! mistake because it only ever ingests subsumptions — but a caller that feeds -//! it a mixed edge set can, so [`Closure::from_asserted`] takes subsumptions by -//! type rather than raw pairs. +//! mistake because it only ever reads subsumptions — but a caller that projects +//! a mixed edge set can, so [`Spine::over`] takes [`Subsumption`] by type rather +//! than raw pairs: the projection from the baked triple table has to name the +//! predicate it kept. #![forbid(unsafe_code)] -use std::collections::{HashMap, HashSet, VecDeque}; +use std::collections::{HashSet, VecDeque}; -/// The **join key** the pre-bake reconciliation uses: `(classid, identity)`. -/// -/// Not an ABI address, and deliberately not documented as one — it is the pair -/// the joiner has already agreed on for the two sides it is joining, which is -/// all a closure needs to index by. What a *baked* row carries is a matter of -/// position, resolved by the class, and this crate is finished long before that -/// question is asked. +/// The address a baked row carries: `(classid, identity)`. /// -/// Ordered and hashable so a closure can index by it without a side table. It -/// carries no namespace, no CURIE and no label — resolving those is the -/// caller's business and none of this crate's. +/// Read off the row's key by position — `classid` at `[0,4)`, the identity rail +/// in the V3 tail — never parsed and never resolved to a label. Ordered so a +/// slice of edges can be sorted and binary-searched; that ordering is the whole +/// access method. #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct ClassAddr { /// The row's classid. @@ -112,11 +118,12 @@ impl ClassAddr { } } -/// An asserted subsumption `sub ⊑ sup`. +/// A baked subsumption `sub ⊑ sup`. /// /// A distinct type rather than a `(ClassAddr, ClassAddr)` tuple, so a caller -/// cannot hand this crate a `part_of` edge by accident — see the crate doc's -/// false-ancestor hazard. +/// projecting the baked triple table cannot hand this crate a `part_of` edge by +/// accident — see the crate doc's false-ancestor hazard. `Ord` sorts by `sub` +/// first, which is the order [`Spine`] binary-searches in. #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct Subsumption { /// The subclass. @@ -136,46 +143,77 @@ impl Subsumption { /// How deep a transitivity walk may go before it stops. /// /// A guard, not a tuning knob. A well-formed subsumption spine is acyclic and -/// shallow, but this crate runs on real harvested data where a cycle would -/// otherwise spin forever — and [`Closure::equivalence_cycles`] exists precisely -/// because cycles DO occur. The cap is reported by [`Closure::depth_cap`] so a -/// caller can tell "not entailed" from "we stopped looking", which are different -/// answers and must not be conflated. +/// shallow, but this crate runs on real baked data where a cycle would otherwise +/// spin forever — and [`Spine::equivalence_cycles`] exists precisely because +/// cycles DO occur. The cap is reported by [`Spine::depth_cap`] so a caller can +/// tell "not entailed" from "we stopped looking", which are different answers +/// and must not be conflated. pub const DEFAULT_DEPTH_CAP: usize = 64; -/// The asserted subsumption graph, closed on demand. +/// A **lens** over baked subsumption edges — borrowed, never owned. /// -/// The closure is computed per query rather than materialised: a spine of N -/// classes has an O(N²) transitive closure but only O(N) asserted edges, and -/// almost every caller asks about a handful of classes. Materialising would -/// trade a cheap walk for an expensive table nobody reads in full. -#[derive(Debug, Clone, Default)] -pub struct Closure { - parents: HashMap>, +/// Holds two sorted slices: the `base` spine (what the bake emitted) and an +/// optional `overlay` (candidate axioms, for [`Self::merge`]). Both are borrowed +/// from the caller; adding an overlay allocates nothing, which is what makes +/// "what WOULD this merge do" cheap enough to ask before deciding. +/// +/// The closure is walked per query rather than materialised: a spine of N +/// classes has an O(N²) transitive closure but only O(N) baked edges, and almost +/// every caller asks about a handful of classes. Materialising would trade a +/// cheap walk over data that already exists for an expensive table nobody reads +/// in full. +#[derive(Debug, Clone, Copy)] +pub struct Spine<'a> { + base: &'a [Subsumption], + overlay: &'a [Subsumption], depth_cap: usize, } -impl Closure { - /// Build from asserted subsumptions. +impl<'a> Spine<'a> { + /// Lens over a slice of baked edges, **sorted by `sub`**. /// - /// Duplicate assertions are kept as asserted — deduplicating here would - /// silently change what [`Self::asserted_len`] reports, and a caller - /// counting its own input has a right to get its own number back. + /// The bake emits them sorted, so this takes it on trust and only checks in + /// debug builds. Use [`Self::try_over`] for a slice whose provenance you do + /// not control. #[must_use] - pub fn from_asserted(edges: impl IntoIterator) -> Self { - let mut parents: HashMap> = HashMap::new(); - for e in edges { - parents.entry(e.sub).or_default().push(e.sup); - } + pub fn over(edges: &'a [Subsumption]) -> Self { + debug_assert!(is_sorted(edges), "Spine::over: edges must be sorted by sub"); Self { - parents, + base: edges, + overlay: &[], depth_cap: DEFAULT_DEPTH_CAP, } } + /// Lens over a slice whose sortedness is **verified**, in release too. + /// + /// `None` means the slice is unsorted, which would make the binary search + /// miss parents and report "not entailed" for edges that are right there. + /// Returning `None` rather than sorting a copy is deliberate: sorting would + /// mean owning, and the caller who holds the real order should fix it. + #[must_use] + pub fn try_over(edges: &'a [Subsumption]) -> Option { + is_sorted(edges).then_some(Self { + base: edges, + overlay: &[], + depth_cap: DEFAULT_DEPTH_CAP, + }) + } + + /// A lens over `base ∪ overlay`, borrowing both. The overlay must be sorted + /// by `sub` on the same terms as the base. + #[must_use] + pub fn with_overlay(self, overlay: &'a [Subsumption]) -> Self { + debug_assert!( + is_sorted(overlay), + "Spine::with_overlay: overlay must be sorted by sub" + ); + Self { overlay, ..self } + } + /// Override the transitivity depth guard. #[must_use] - pub fn with_depth_cap(mut self, cap: usize) -> Self { + pub const fn with_depth_cap(mut self, cap: usize) -> Self { self.depth_cap = cap; self } @@ -187,21 +225,26 @@ impl Closure { self.depth_cap } - /// Number of asserted edges. + /// Number of edges in view (base + overlay). #[must_use] - pub fn asserted_len(&self) -> usize { - self.parents.values().map(Vec::len).sum() + pub const fn len(&self) -> usize { + self.base.len() + self.overlay.len() } - /// Whether any edge is asserted. + /// Whether any edge is in view. #[must_use] - pub fn is_empty(&self) -> bool { - self.parents.is_empty() + pub const fn is_empty(&self) -> bool { + self.base.is_empty() && self.overlay.is_empty() } - /// Classes with at least one asserted superclass. - pub fn subclasses(&self) -> impl Iterator + '_ { - self.parents.keys().copied() + /// The asserted parents of `c`, **as two subslices of the borrowed data**. + /// + /// This is the lookup the whole crate is built on: an equal-range binary + /// search by `sub`, returning a window into the caller's slice. Nothing is + /// copied, so a caller can hold the result as long as it holds the edges. + #[must_use] + pub fn parents_of(&self, c: ClassAddr) -> (&'a [Subsumption], &'a [Subsumption]) { + (equal_range(self.base, c), equal_range(self.overlay, c)) } /// **R1 + R2** — every superclass of `c`, transitively. @@ -209,6 +252,9 @@ impl Closure { /// Excludes `c` itself unless a cycle genuinely returns to it, which is the /// signal [`Self::equivalence_cycles`] reads. Breadth-first, so the walk /// terminates at `depth_cap` hops rather than at `depth_cap` nodes. + /// + /// The `HashSet` is the walk's frontier, not a copy of the spine: it holds + /// the answer, which is what the caller asked for. #[must_use] pub fn supers_of(&self, c: ClassAddr) -> HashSet { let mut seen = HashSet::new(); @@ -217,9 +263,10 @@ impl Closure { if depth >= self.depth_cap { continue; } - for &p in self.parents.get(&node).into_iter().flatten() { - if seen.insert(p) { - queue.push_back((p, depth + 1)); + let (a, b) = self.parents_of(node); + for e in a.iter().chain(b) { + if seen.insert(e.sup) { + queue.push_back((e.sup, depth + 1)); } } } @@ -229,52 +276,77 @@ impl Closure { /// **The first question: does `sub ⊑ sup` follow?** /// /// Reflexive per R1: every class subsumes itself, which is a fact even when - /// no edge is asserted for it. + /// no edge is baked for it. #[must_use] pub fn entails(&self, sub: ClassAddr, sup: ClassAddr) -> bool { sub == sup || self.supers_of(sub).contains(&sup) } + /// Every class with at least one baked parent, in sorted order and without + /// duplicates — the walk domain for [`Self::equivalence_cycles`]. + fn subclasses(&self) -> Vec { + let mut v: Vec = self + .base + .iter() + .chain(self.overlay) + .map(|e| e.sub) + .collect(); + v.sort_unstable(); + v.dedup(); + v + } + /// Classes that reach themselves — an equivalence cycle. /// /// Empty for a sound spine. A non-empty result is not automatically a bug: /// two classes an ontology models separately may be genuine synonyms. It IS /// always a finding, because a cycle makes the two mutually substitutable, /// and a consumer treating one as more specific than the other is then - /// relying on something the asserted set does not support. + /// relying on something the baked set does not support. #[must_use] pub fn equivalence_cycles(&self) -> Vec { - let mut out: Vec = self - .parents - .keys() - .copied() + self.subclasses() + .into_iter() .filter(|&c| self.supers_of(c).contains(&c)) - .collect(); - out.sort_unstable(); - out + .collect() } } -/// What merging a set of axioms into an existing closure would do. +/// Sorted-by-`sub` check. Cheap enough to run in debug on every construction. +fn is_sorted(edges: &[Subsumption]) -> bool { + edges.windows(2).all(|w| w[0].sub <= w[1].sub) +} + +/// The window of `edges` whose `sub == c` — an equal-range binary search. /// -/// Returned by [`Closure::merge`] **without mutating** the closure: a caller -/// decides whether to accept the merge after seeing the verdict, which is the -/// only order that makes the verdict useful. +/// Returns a subslice of the input, which is the point: a parent lookup costs a +/// `log n` probe and yields a borrowed view, never an allocation. +fn equal_range(edges: &[Subsumption], c: ClassAddr) -> &[Subsumption] { + let lo = edges.partition_point(|e| e.sub < c); + let hi = edges.partition_point(|e| e.sub <= c); + &edges[lo..hi] +} + +/// What merging a set of axioms into a baked spine would do. +/// +/// Returned by [`Spine::merge`] **without applying anything** — a caller decides +/// whether to accept the merge after seeing the verdict, which is the only order +/// that makes the verdict useful. Nothing is mutated because nothing is owned. #[derive(Debug, Clone, PartialEq, Eq, Default)] pub struct MergeVerdict { - /// Axioms the closure already entailed. These corroborate the existing set - /// and add nothing — the strongest possible outcome for an axiom, and the - /// one that carries no risk. + /// Axioms the baked spine already entailed. These corroborate it and add + /// nothing — the strongest possible outcome for an axiom, and the one that + /// carries no risk. pub corroborating: Vec, - /// Axioms the closure did NOT entail, and which introduce no cycle. New - /// structure the existing set was silent about — **enrichment**, not - /// conflict. Silence is not disagreement. + /// Axioms the spine did NOT entail, and which introduce no cycle. New + /// structure the bake was silent about — **enrichment**, not conflict. + /// Silence is not disagreement. pub enriching: Vec, /// Classes drawn into an equivalence cycle BY this merge. Empty means the /// merge is sound over this fragment. pub introduced_cycles: Vec, - /// Cycles that were already present before the merge — reported so the - /// merge cannot be blamed for them. + /// Cycles already present in the bake — reported so the merge cannot be + /// blamed for them. pub pre_existing_cycles: Vec, } @@ -298,13 +370,16 @@ impl MergeVerdict { } } -impl Closure { +impl Spine<'_> { /// **The second question: is adding `axioms` sound?** /// - /// Splits them into corroborating and enriching, then closes the union and - /// reports any equivalence cycle the merge introduced. The receiver is - /// untouched; apply the merge yourself with [`Self::extended`] once the - /// verdict is acceptable. + /// Splits them into corroborating and enriching, then observes the spine + /// **with the enriching ones overlaid** and reports any equivalence cycle + /// that appears. The overlay is borrowed, so the "what would happen" + /// question costs a second lens and no copy of the spine. + /// + /// `axioms` must be sorted by `sub` — same precondition as the base, for + /// the same reason. #[must_use] pub fn merge(&self, axioms: &[Subsumption]) -> MergeVerdict { let pre: HashSet = self.equivalence_cycles().into_iter().collect(); @@ -319,10 +394,21 @@ impl Closure { } } - // Only the enriching axioms can change the closure, so only they are - // merged for the cycle check. Including the corroborating ones would - // cost a larger walk to reach an identical answer. - let merged = self.extended(&enriching); + // Only the enriching axioms can change what follows, so only they are + // overlaid for the cycle check. Including the corroborating ones would + // cost a wider walk to reach an identical answer. + // + // The overlay must be sorted on its own terms — `axioms` being sorted + // does not survive the filter's re-collection into a new Vec in general, + // so it is re-sorted here rather than assumed. + let mut overlay = enriching.clone(); + overlay.sort_unstable(); + let merged = Spine { + base: self.base, + overlay: &overlay, + depth_cap: self.depth_cap, + }; + let mut introduced: Vec = merged .equivalence_cycles() .into_iter() @@ -340,20 +426,6 @@ impl Closure { pre_existing_cycles: pre_existing, } } - - /// A copy with `axioms` added. Pairs with [`Self::merge`]: check first, - /// then extend. - #[must_use] - pub fn extended(&self, axioms: &[Subsumption]) -> Closure { - let mut parents = self.parents.clone(); - for ax in axioms { - parents.entry(ax.sub).or_default().push(ax.sup); - } - Closure { - parents, - depth_cap: self.depth_cap, - } - } } #[cfg(test)] @@ -370,55 +442,84 @@ mod tests { Subsumption::new(c(a), c(b)) } - /// R1 + R2: transitivity derives what is not asserted, and reflexivity - /// holds for a class with no edges at all. + /// Baked edges arrive sorted; the tests mirror that rather than pretending + /// the lens sorts for them. + fn baked(mut e: Vec) -> Vec { + e.sort_unstable(); + e + } + + /// R1 + R2: transitivity derives what is not baked, and reflexivity holds + /// for a class with no edges at all. /// /// The anti-vacuity half is `!entails(1, 9)`: without it, an `entails` that /// returned `true` unconditionally would pass every positive assertion here. #[test] fn transitivity_derives_and_reflexivity_holds() { - let cl = Closure::from_asserted([sub(1, 2), sub(2, 3), sub(3, 4)]); - assert!(cl.entails(c(1), c(2)), "asserted"); - assert!(cl.entails(c(1), c(4)), "derived through two hops"); - assert!(cl.entails(c(7), c(7)), "reflexive even with no edges"); + let e = baked(vec![sub(1, 2), sub(2, 3), sub(3, 4)]); + let s = Spine::over(&e); + assert!(s.entails(c(1), c(2)), "baked"); + assert!(s.entails(c(1), c(4)), "derived through two hops"); + assert!(s.entails(c(7), c(7)), "reflexive even with no edges"); + assert!(!s.entails(c(1), c(9)), "must NOT entail an unrelated class"); + assert!(!s.entails(c(4), c(1)), "and must not run the wrong way"); + } + + /// The lens borrows: a parent lookup hands back a window into the caller's + /// own slice, and multiple parents land in one contiguous run. + #[test] + fn parents_are_a_borrowed_window_not_a_copy() { + let e = baked(vec![sub(1, 2), sub(1, 3), sub(4, 5)]); + let s = Spine::over(&e); + let (base, overlay) = s.parents_of(c(1)); + assert_eq!(base.len(), 2, "both parents in one equal-range window"); + assert!(overlay.is_empty(), "no overlay in view"); assert!( - !cl.entails(c(1), c(9)), - "must NOT entail an unrelated class" + std::ptr::eq(base.as_ptr(), e.as_ptr()), + "the window points INTO the caller's slice — nothing was copied" ); - assert!(!cl.entails(c(4), c(1)), "and must not run the wrong way"); + assert!(s.parents_of(c(9)).0.is_empty(), "an absent class has none"); + } + + /// An unsorted slice is refused rather than silently mis-searched, and a + /// sorted one is accepted — the discriminating pair. + #[test] + fn try_over_refuses_unsorted_and_accepts_sorted() { + let bad = vec![sub(5, 6), sub(1, 2)]; + assert!(Spine::try_over(&bad).is_none(), "unsorted must be refused"); + let good = baked(bad); + assert!(Spine::try_over(&good).is_some(), "sorted must be accepted"); } /// The depth cap is a real limit and is REPORTED, so "not entailed" stays /// distinguishable from "we stopped looking". - /// - /// Both directions are asserted: at cap 2 the far end is unreachable, at - /// the default it is reachable. A cap that did nothing would fail the first - /// assertion; one that clamped everything would fail the second. #[test] fn the_depth_cap_binds_and_is_visible() { - let chain: Vec = (1..10).map(|i| sub(i, i + 1)).collect(); - let shallow = Closure::from_asserted(chain.clone()).with_depth_cap(2); + let e = baked((1..10).map(|i| sub(i, i + 1)).collect()); + let shallow = Spine::over(&e).with_depth_cap(2); assert_eq!(shallow.depth_cap(), 2); assert!(!shallow.entails(c(1), c(10)), "beyond the cap"); assert!(shallow.entails(c(1), c(3)), "within the cap"); - let deep = Closure::from_asserted(chain); - assert!(deep.entails(c(1), c(10)), "reachable at the default cap"); + assert!( + Spine::over(&e).entails(c(1), c(10)), + "reachable at the default cap" + ); } - /// A sound spine has no cycles; a two-way assertion produces one. + /// A sound spine has no cycles; a two-way edge produces one. /// /// The can-stay-silent half uses a NON-trivial acyclic graph — an empty - /// closure would prove only that emptiness has no cycles. + /// spine would prove only that emptiness has no cycles. #[test] fn cycles_are_detected_and_absent_when_they_should_be() { - let acyclic = Closure::from_asserted([sub(1, 2), sub(2, 3), sub(1, 3), sub(4, 3)]); + let ok = baked(vec![sub(1, 2), sub(2, 3), sub(1, 3), sub(4, 3)]); assert!( - acyclic.equivalence_cycles().is_empty(), + Spine::over(&ok).equivalence_cycles().is_empty(), "a real acyclic spine reports no cycle" ); - let cyclic = Closure::from_asserted([sub(1, 2), sub(2, 1)]); + let bad = baked(vec![sub(1, 2), sub(2, 1)]); assert_eq!( - cyclic.equivalence_cycles(), + Spine::over(&bad).equivalence_cycles(), vec![c(1), c(2)], "both ends of the equivalence are named" ); @@ -428,43 +529,48 @@ mod tests { /// makes this a reasoner rather than a pairwise check. #[test] fn a_cycle_through_a_long_chain_is_found() { - let mut axioms: Vec = (1..8).map(|i| sub(i, i + 1)).collect(); - axioms.push(sub(8, 1)); // closes 1 → 8 → 1 - let cl = Closure::from_asserted(axioms); - assert_eq!(cl.equivalence_cycles().len(), 8, "every class on the ring"); + let mut v: Vec = (1..8).map(|i| sub(i, i + 1)).collect(); + v.push(sub(8, 1)); // closes 1 → 8 → 1 + let e = baked(v); + assert_eq!( + Spine::over(&e).equivalence_cycles().len(), + 8, + "every class on the ring" + ); } /// **The merge verdict discriminates all three outcomes.** A verdict that /// answered one class for everything would carry no information. #[test] fn merge_splits_corroborating_enriching_and_conflicting() { - let base = Closure::from_asserted([sub(1, 2), sub(2, 3)]); + let e = baked(vec![sub(1, 2), sub(2, 3)]); + let s = Spine::over(&e); // Corroborating: already derivable through 1 ⊑ 2 ⊑ 3. - let v = base.merge(&[sub(1, 3)]); + let v = s.merge(&[sub(1, 3)]); assert_eq!(v.corroborating.len(), 1); assert!(v.enriching.is_empty()); assert!(v.is_sound()); - // Enriching: the base is SILENT about 4, not opposed to it. - let v = base.merge(&[sub(4, 3)]); + // Enriching: the bake is SILENT about 4, not opposed to it. + let v = s.merge(&[sub(4, 3)]); assert!(v.corroborating.is_empty()); assert_eq!(v.enriching.len(), 1); assert!(v.is_sound(), "silence is not disagreement"); - // Conflicting: the base says 1 ⊑ 3; the reverse closes a cycle. - let v = base.merge(&[sub(3, 1)]); + // Conflicting: the bake says 1 ⊑ 3; the reverse closes a cycle. + let v = s.merge(&[sub(3, 1)]); assert!(!v.is_sound(), "a direction conflict must NOT read as sound"); assert_eq!(v.introduced_cycles, vec![c(1), c(2), c(3)]); - assert!(v.pre_existing_cycles.is_empty(), "the base was clean"); + assert!(v.pre_existing_cycles.is_empty(), "the bake was clean"); } /// Pre-existing cycles are never blamed on the merge — the control that /// makes `introduced_cycles` mean what it says. #[test] fn a_pre_existing_cycle_is_not_attributed_to_the_merge() { - let dirty = Closure::from_asserted([sub(1, 2), sub(2, 1)]); - let v = dirty.merge(&[sub(5, 6)]); + let e = baked(vec![sub(1, 2), sub(2, 1)]); + let v = Spine::over(&e).merge(&[sub(5, 6)]); assert_eq!(v.pre_existing_cycles, vec![c(1), c(2)]); assert!( v.introduced_cycles.is_empty(), @@ -473,19 +579,19 @@ mod tests { assert!(v.is_sound()); } - /// `merge` does not mutate; `extended` does. Checking first and applying - /// after is the only order in which a verdict is useful. + /// `merge` observes; the overlay applies. The base slice is untouched by + /// either, because the lens never had write access to begin with. #[test] - fn merge_inspects_and_extended_applies() { - let base = Closure::from_asserted([sub(1, 2)]); - let before = base.asserted_len(); - let v = base.merge(&[sub(2, 3)]); - assert_eq!(base.asserted_len(), before, "merge left the closure alone"); - assert!(!base.entails(c(1), c(3))); - let applied = base.extended(&v.enriching); + fn merge_observes_and_the_overlay_applies() { + let e = baked(vec![sub(1, 2)]); + let s = Spine::over(&e); + let v = s.merge(&[sub(2, 3)]); + assert_eq!(e.len(), 1, "the baked slice was not written to"); + assert!(!s.entails(c(1), c(3)), "and the lens still sees only the bake"); + let extra = baked(v.enriching.clone()); assert!( - applied.entails(c(1), c(3)), - "and extended really applies it" + s.with_overlay(&extra).entails(c(1), c(3)), + "overlaying really applies it" ); } @@ -494,11 +600,12 @@ mod tests { #[test] fn identity_alone_does_not_make_two_classes_the_same() { let other = 0x0302_0000; - let cl = Closure::from_asserted([Subsumption::new( + let e = baked(vec![Subsumption::new( ClassAddr::new(NS, 1), ClassAddr::new(NS, 2), )]); - assert!(!cl.entails(ClassAddr::new(other, 1), ClassAddr::new(NS, 2))); - assert!(cl.entails(ClassAddr::new(NS, 1), ClassAddr::new(NS, 2))); + let s = Spine::over(&e); + assert!(!s.entails(ClassAddr::new(other, 1), ClassAddr::new(NS, 2))); + assert!(s.entails(ClassAddr::new(NS, 1), ClassAddr::new(NS, 2))); } }