Skip to main content

xlog_induce/
nary.rs

1//! Ordered n-ary rule-pattern layer for exact induction.
2//!
3//! Generalizes the four fixed 2-body binary topologies to rule patterns over
4//! heads of arity `>= 1` with bodies of up to `max_body_atoms` atoms, where
5//! every body-atom position binds either a head argument position or a
6//! bounded, canonically-numbered existential join variable. The shipped
7//! binary engine's templates are exactly four members of this space at
8//! `head_arity = 2`, two body atoms and one join variable — see
9//! [`canonical_binary_pattern`], which is the parity surface the general
10//! enumeration is tested against.
11//!
12//! This module is deliberately pure host-side: pattern types, canonical-form
13//! validation and deterministic enumeration. Scoring the patterns on device
14//! is a separate stage that consumes [`NaryRulePattern`] values as its rule
15//! templates.
16//!
17//! Three laws are enforced here rather than documented elsewhere:
18//!
19//! * **Canonical form (join-variable naming).** Join variables are numbered
20//!   densely in first-appearance order across the body read left to right,
21//!   so the ENUMERATOR never emits two patterns differing only by
22//!   join-variable renaming — it does not need to filter them.
23//!
24//!   Note the exact scope: canonicality is a property of what
25//!   [`enumerate_patterns`] EMITS, not of the type. [`NaryRulePattern`] has
26//!   public fields, so a caller can hand-build a non-canonical alpha-twin,
27//!   and the public flatten/score path will score it identically to its
28//!   canonical form. That is safe (the score is the same), but it means
29//!   alpha-duplicates are avoided by construction of the generator and
30//!   REJECTED by [`NaryRulePattern::validate`] — not made unrepresentable
31//!   by the type. Callers assembling patterns by hand own that obligation.
32//!
33//! * **Canonical form does NOT quotient atom order or multiplicity.**
34//!   `H :- A(x),B(x)` and `H :- B(x),A(x)` are distinct members, as are
35//!   `H :- A(x)` and `H :- A(x),A(x)`. Semantically identical bodies score
36//!   identically, tie perfectly in the reduction, can co-occupy top-K, and
37//!   inflate `total_scored`. This matches the shipped binary engine, whose
38//!   ordered `(topology, L, R)` grid likewise scores both orderings; a
39//!   sorted-body canonical form would be a behavior change, not a bug fix.
40//!
41//! * **No silent truncation.** The enumeration refuses with a typed error
42//!   when the pattern space exceeds `max_patterns`, and when the SEARCH
43//!   exceeds `max_traversal_nodes`; it never quietly caps. The two bounds
44//!   are separate because the first bounds output and the second bounds
45//!   work — a search that keeps nothing can still be enormous.
46
47use xlog_core::{Result, XlogError};
48
49/// A variable slot inside a body-atom binding pattern.
50#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
51pub enum PatternVar {
52    /// Bound to head argument position `i` (0-based, `< head_arity`).
53    Head(u8),
54    /// Bound to existential join variable `j` (0-based). Join variables are
55    /// canonical: `j` is dense in first-appearance order across the body.
56    Join(u8),
57}
58
59/// One body atom: a candidate-relation slot plus its ordered bindings.
60///
61/// `candidate_slot` indexes the request's candidate list (the same slot the
62/// binary engine calls `L`/`R` indices); the binding vector length is the
63/// atom's arity and must match the slot's declared relation arity.
64#[derive(Debug, Clone, PartialEq, Eq, Hash)]
65pub struct BodyAtomPattern {
66    pub candidate_slot: u32,
67    pub bindings: Vec<PatternVar>,
68}
69
70/// A canonical n-ary rule pattern: `H(h0..h{a-1}) :- body...`.
71#[derive(Debug, Clone, PartialEq, Eq, Hash)]
72pub struct NaryRulePattern {
73    pub head_arity: u8,
74    pub body: Vec<BodyAtomPattern>,
75}
76
77/// Enumeration bounds for one n-ary induction request.
78#[derive(Debug, Clone, Copy)]
79pub struct NaryEnumerationConfig {
80    /// Maximum number of body atoms per pattern (the binary engine uses 2).
81    pub max_body_atoms: u8,
82    /// Maximum distinct existential join variables per pattern (binary: 1).
83    pub max_join_vars: u8,
84    /// Hard ceiling on the enumerated pattern count. Exceeding it is a typed
85    /// refusal, never a silent cap.
86    ///
87    /// This bounds the OUTPUT. It does not bound the work: the search can
88    /// walk an exponential number of dead-end nodes without ever producing
89    /// a keepable pattern, so `max_traversal_nodes` bounds that separately.
90    pub max_patterns: u32,
91    /// Hard ceiling on SEARCH NODES visited during enumeration.
92    ///
93    /// Without it an in-contract request (small `max_patterns`, wide
94    /// candidate set) walks billions of nodes and returns an empty result,
95    /// because the pattern cap can only fire when a pattern is KEPT.
96    /// Exceeding this is the same kind of typed refusal.
97    pub max_traversal_nodes: u64,
98}
99
100impl NaryRulePattern {
101    /// Validate canonical form against a head arity, the candidate arity
102    /// table and the enumeration bounds.
103    ///
104    /// The checks, in refusal order:
105    /// 1. structural: nonzero head arity, nonempty body, body length bound;
106    /// 2. per-atom: known candidate slot, binding length == declared arity;
107    /// 3. variable legality: `Head(i) < head_arity`, join count bound;
108    /// 4. canonical join numbering (dense, first-appearance order);
109    /// 5. range restriction: every head position bound somewhere in the
110    ///    body — a head position no body atom touches cannot be scored by
111    ///    coverage and is refused as an unsafe variable rather than scored
112    ///    vacuously.
113    pub fn validate(&self, candidate_arities: &[u8], config: &NaryEnumerationConfig) -> Result<()> {
114        if self.head_arity == 0 {
115            return Err(XlogError::Type(
116                "nary pattern: head arity must be at least 1".into(),
117            ));
118        }
119        if self.body.is_empty() {
120            return Err(XlogError::Type(
121                "nary pattern: body must carry at least one atom".into(),
122            ));
123        }
124        if self.body.len() > config.max_body_atoms as usize {
125            return Err(XlogError::Type(format!(
126                "nary pattern: body has {} atoms but max_body_atoms is {}",
127                self.body.len(),
128                config.max_body_atoms
129            )));
130        }
131        let mut next_join: u8 = 0;
132        let mut head_bound = vec![false; self.head_arity as usize];
133        for (atom_index, atom) in self.body.iter().enumerate() {
134            let declared = candidate_arities
135                .get(atom.candidate_slot as usize)
136                .copied()
137                .ok_or_else(|| {
138                    XlogError::Type(format!(
139                        "nary pattern: body atom {atom_index} names candidate \
140                         slot {} but only {} candidates exist",
141                        atom.candidate_slot,
142                        candidate_arities.len()
143                    ))
144                })?;
145            if atom.bindings.len() != declared as usize {
146                return Err(XlogError::Type(format!(
147                    "nary pattern: body atom {atom_index} binds {} positions \
148                     but candidate slot {} declares arity {declared}",
149                    atom.bindings.len(),
150                    atom.candidate_slot
151                )));
152            }
153            for binding in &atom.bindings {
154                match *binding {
155                    PatternVar::Head(i) => {
156                        if i >= self.head_arity {
157                            return Err(XlogError::Type(format!(
158                                "nary pattern: head position {i} out of range \
159                                 for head arity {}",
160                                self.head_arity
161                            )));
162                        }
163                        head_bound[i as usize] = true;
164                    }
165                    PatternVar::Join(j) => {
166                        if j > next_join {
167                            return Err(XlogError::Type(format!(
168                                "nary pattern: join variable z{j} appears \
169                                 before z{} — join numbering must be dense in \
170                                 first-appearance order",
171                                j.saturating_sub(1)
172                            )));
173                        }
174                        if j == next_join {
175                            // checked: with max_join_vars = 255 a crafted
176                            // 256-join pattern would panic in debug and wrap
177                            // to 0 in release, after which the bound check
178                            // reads 0 > 255 and ACCEPTS the over-budget,
179                            // non-canonical pattern.
180                            next_join = next_join.checked_add(1).ok_or_else(|| {
181                                XlogError::Type(
182                                    "nary pattern: join variable count exceeds                                      the representable range"
183                                        .to_string(),
184                                )
185                            })?;
186                            if next_join > config.max_join_vars {
187                                return Err(XlogError::Type(format!(
188                                    "nary pattern: {} join variables exceed \
189                                     max_join_vars {}",
190                                    next_join, config.max_join_vars
191                                )));
192                            }
193                        }
194                    }
195                }
196            }
197        }
198        if let Some(unbound) = head_bound.iter().position(|bound| !bound) {
199            return Err(XlogError::UnsafeVariable(format!("h{unbound}")));
200        }
201        Ok(())
202    }
203}
204
205/// The four shipped binary topologies expressed as n-ary patterns.
206///
207/// This is the parity surface: scoring these four patterns for a pair of
208/// candidate slots must reproduce the binary engine's `(topology, L, R)`
209/// results exactly.
210pub fn canonical_binary_pattern(
211    topology: crate::types::Topology,
212    left_slot: u32,
213    right_slot: u32,
214) -> NaryRulePattern {
215    use crate::types::Topology;
216    use PatternVar::{Head, Join};
217    let (left, right) = match topology {
218        // H(X,Y) :- L(X,Z), R(Z,Y)
219        Topology::Chain => (vec![Head(0), Join(0)], vec![Join(0), Head(1)]),
220        // H(X,Y) :- L(X,Y), R(X,Y)
221        Topology::Star => (vec![Head(0), Head(1)], vec![Head(0), Head(1)]),
222        // H(X,Y) :- L(X,Z), R(X,Y)
223        Topology::Fanout => (vec![Head(0), Join(0)], vec![Head(0), Head(1)]),
224        // H(X,Y) :- L(X,Y), R(Z,Y)
225        Topology::Fanin => (vec![Head(0), Head(1)], vec![Join(0), Head(1)]),
226    };
227    NaryRulePattern {
228        head_arity: 2,
229        body: vec![
230            BodyAtomPattern {
231                candidate_slot: left_slot,
232                bindings: left,
233            },
234            BodyAtomPattern {
235                candidate_slot: right_slot,
236                bindings: right,
237            },
238        ],
239    }
240}
241
242/// Deterministically enumerate every well-formed canonical pattern.
243///
244/// Order is lexicographic in `(body_len, candidate slots, bindings)` with
245/// `Head(i)` ordered before `Join(j)` at each position, so two calls with the
246/// same inputs return identical vectors. Canonical join numbering is
247/// generated directly (a join slot may only introduce the next unused join
248/// index), so this function never produces an alpha-duplicate — it does
249/// not need to filter them. Callers that construct patterns by hand
250/// bypass that guarantee; `NaryRulePattern::validate` is what rejects a
251/// non-canonical one.
252///
253/// Refuses with a typed error the moment the pattern count would exceed
254/// `config.max_patterns`.
255pub fn enumerate_patterns(
256    head_arity: u8,
257    candidate_arities: &[u8],
258    config: &NaryEnumerationConfig,
259) -> Result<Vec<NaryRulePattern>> {
260    if head_arity == 0 {
261        return Err(XlogError::Type(
262            "nary enumeration: head arity must be at least 1".into(),
263        ));
264    }
265    if candidate_arities.is_empty() {
266        return Ok(Vec::new());
267    }
268    let mut patterns: Vec<NaryRulePattern> = Vec::new();
269    let mut body: Vec<BodyAtomPattern> = Vec::new();
270    let mut nodes: u64 = 0;
271    for body_len in 1..=config.max_body_atoms {
272        enumerate_bodies(
273            head_arity,
274            candidate_arities,
275            config,
276            body_len,
277            &mut body,
278            0,
279            &mut patterns,
280            &mut nodes,
281        )?;
282    }
283    Ok(patterns)
284}
285
286#[allow(clippy::too_many_arguments)]
287fn enumerate_bodies(
288    head_arity: u8,
289    candidate_arities: &[u8],
290    config: &NaryEnumerationConfig,
291    body_len: u8,
292    body: &mut Vec<BodyAtomPattern>,
293    joins_used: u8,
294    out: &mut Vec<NaryRulePattern>,
295    nodes: &mut u64,
296) -> Result<()> {
297    charge_node(config, nodes)?;
298    if body.len() == body_len as usize {
299        let candidate = NaryRulePattern {
300            head_arity,
301            body: body.clone(),
302        };
303        // Range restriction is the only law the canonical generator cannot
304        // guarantee positionally; everything else holds by construction.
305        let mut head_bound = vec![false; head_arity as usize];
306        for atom in &candidate.body {
307            for binding in &atom.bindings {
308                if let PatternVar::Head(i) = *binding {
309                    head_bound[i as usize] = true;
310                }
311            }
312        }
313        if head_bound.iter().all(|bound| *bound) {
314            if out.len() as u32 >= config.max_patterns {
315                return Err(XlogError::Execution(format!(
316                    "nary enumeration: pattern space exceeds max_patterns {} \
317                     (head_arity {head_arity}, {} candidates, max_body_atoms \
318                     {}, max_join_vars {}); raise the bound explicitly or \
319                     narrow the request — the engine never truncates silently",
320                    config.max_patterns,
321                    candidate_arities.len(),
322                    config.max_body_atoms,
323                    config.max_join_vars
324                )));
325            }
326            out.push(candidate);
327        }
328        return Ok(());
329    }
330    for slot in 0..candidate_arities.len() as u32 {
331        let arity = candidate_arities[slot as usize];
332        let mut bindings: Vec<PatternVar> = Vec::with_capacity(arity as usize);
333        enumerate_bindings(
334            head_arity,
335            candidate_arities,
336            config,
337            body_len,
338            body,
339            joins_used,
340            slot,
341            arity,
342            &mut bindings,
343            out,
344            nodes,
345        )?;
346    }
347    Ok(())
348}
349
350#[allow(clippy::too_many_arguments)]
351fn enumerate_bindings(
352    head_arity: u8,
353    candidate_arities: &[u8],
354    config: &NaryEnumerationConfig,
355    body_len: u8,
356    body: &mut Vec<BodyAtomPattern>,
357    joins_used: u8,
358    slot: u32,
359    arity: u8,
360    bindings: &mut Vec<PatternVar>,
361    out: &mut Vec<NaryRulePattern>,
362    nodes: &mut u64,
363) -> Result<()> {
364    charge_node(config, nodes)?;
365    if bindings.len() == arity as usize {
366        body.push(BodyAtomPattern {
367            candidate_slot: slot,
368            bindings: bindings.clone(),
369        });
370        let joins_now = joins_used.max(next_join_index(body));
371        enumerate_bodies(
372            head_arity,
373            candidate_arities,
374            config,
375            body_len,
376            body,
377            joins_now,
378            out,
379            nodes,
380        )?;
381        body.pop();
382        return Ok(());
383    }
384    for head in 0..head_arity {
385        bindings.push(PatternVar::Head(head));
386        enumerate_bindings(
387            head_arity,
388            candidate_arities,
389            config,
390            body_len,
391            body,
392            joins_used,
393            slot,
394            arity,
395            bindings,
396            out,
397            nodes,
398        )?;
399        bindings.pop();
400    }
401    // Canonical growth: a join slot may reuse any join already introduced or
402    // introduce exactly the next unused index, never a later one.
403    let introduced_so_far = joins_used.max(bindings_join_watermark(bindings, joins_used));
404    let reachable = introduced_so_far
405        .saturating_add(1)
406        .min(config.max_join_vars);
407    for join in 0..reachable {
408        bindings.push(PatternVar::Join(join));
409        enumerate_bindings(
410            head_arity,
411            candidate_arities,
412            config,
413            body_len,
414            body,
415            joins_used,
416            slot,
417            arity,
418            bindings,
419            out,
420            nodes,
421        )?;
422        bindings.pop();
423    }
424    Ok(())
425}
426
427/// Charge one search node against the traversal budget.
428///
429/// The pattern cap can only fire when a pattern is KEPT, so a request with
430/// a small `max_patterns` over a wide candidate set would otherwise walk an
431/// exponential dead-end space and return an empty result after minutes of
432/// work. Bounding nodes makes the refusal reachable on the SEARCH, not just
433/// on the output.
434fn charge_node(config: &NaryEnumerationConfig, nodes: &mut u64) -> Result<()> {
435    *nodes += 1;
436    if *nodes > config.max_traversal_nodes {
437        return Err(XlogError::Execution(format!(
438            "nary enumeration: search exceeded max_traversal_nodes {} \
439             (max_body_atoms {}, max_join_vars {}); the pattern space is \
440             larger than the work budget — narrow the request or raise the \
441             bound explicitly, the engine never truncates silently",
442            config.max_traversal_nodes, config.max_body_atoms, config.max_join_vars,
443        )));
444    }
445    Ok(())
446}
447
448/// Highest join index introduced anywhere in `body`, as a next-free counter.
449fn next_join_index(body: &[BodyAtomPattern]) -> u8 {
450    let mut next = 0u8;
451    for atom in body {
452        for binding in &atom.bindings {
453            if let PatternVar::Join(j) = *binding {
454                next = next.max(j + 1);
455            }
456        }
457    }
458    next
459}
460
461/// Highest join index introduced in the partial `bindings`, as a next-free
462/// counter floored at `joins_used` (joins introduced by earlier atoms).
463fn bindings_join_watermark(bindings: &[PatternVar], joins_used: u8) -> u8 {
464    let mut next = joins_used;
465    for binding in bindings {
466        if let PatternVar::Join(j) = *binding {
467            next = next.max(j + 1);
468        }
469    }
470    next
471}
472
473#[cfg(test)]
474mod tests {
475    use super::*;
476    use crate::types::Topology;
477
478    fn config(max_body_atoms: u8, max_join_vars: u8) -> NaryEnumerationConfig {
479        NaryEnumerationConfig {
480            max_body_atoms,
481            max_join_vars,
482            max_patterns: 1_000_000,
483            max_traversal_nodes: 1_000_000,
484        }
485    }
486
487    #[test]
488    fn canonical_binary_patterns_validate_and_match_templates() {
489        let arities = [2u8, 2u8];
490        let cfg = config(2, 1);
491        for topology in Topology::ALL {
492            let pattern = canonical_binary_pattern(topology, 0, 1);
493            pattern
494                .validate(&arities, &cfg)
495                .unwrap_or_else(|e| panic!("{topology:?} failed validation: {e}"));
496            assert_eq!(pattern.head_arity, 2);
497            assert_eq!(pattern.body.len(), 2);
498        }
499        // Chain joins through z on the inner positions - the exact shipped
500        // template H(X,Y) :- L(X,Z), R(Z,Y).
501        let chain = canonical_binary_pattern(Topology::Chain, 0, 1);
502        assert_eq!(
503            chain.body[0].bindings,
504            vec![PatternVar::Head(0), PatternVar::Join(0)]
505        );
506        assert_eq!(
507            chain.body[1].bindings,
508            vec![PatternVar::Join(0), PatternVar::Head(1)]
509        );
510    }
511
512    #[test]
513    fn enumeration_contains_all_four_binary_topologies() {
514        let arities = [2u8, 2u8];
515        let cfg = config(2, 1);
516        let patterns = enumerate_patterns(2, &arities, &cfg).expect("enumerate");
517        for topology in Topology::ALL {
518            let expected = canonical_binary_pattern(topology, 0, 1);
519            assert!(
520                patterns.contains(&expected),
521                "{topology:?} missing from the general enumeration"
522            );
523        }
524    }
525
526    #[test]
527    fn enumeration_is_deterministic_and_canonical() {
528        let arities = [2u8, 3u8];
529        let cfg = config(2, 2);
530        let first = enumerate_patterns(3, &arities, &cfg).expect("enumerate");
531        let second = enumerate_patterns(3, &arities, &cfg).expect("enumerate");
532        assert_eq!(first, second);
533        for pattern in &first {
534            pattern
535                .validate(&arities, &cfg)
536                .unwrap_or_else(|e| panic!("non-canonical pattern {pattern:?}: {e}"));
537        }
538    }
539
540    #[test]
541    fn enumeration_count_matches_hand_derivation() {
542        // head_arity=1, one arity-1 candidate, max_body=2, max_join=1.
543        // K=1: (H0) — a lone (J0) leaves the head unbound and is dropped.
544        // K=2: (H0,H0), (H0,J0), (J0,H0); (J0,J0) drops (head unbound),
545        // (J0,J1) is unreachable at max_join=1. Total = 4.
546        let arities = [1u8];
547        let cfg = config(2, 1);
548        let patterns = enumerate_patterns(1, &arities, &cfg).expect("enumerate");
549        assert_eq!(
550            patterns.len(),
551            4,
552            "hand-derived space changed: {patterns:#?}"
553        );
554    }
555
556    #[test]
557    fn validation_refuses_out_of_range_head_position() {
558        let pattern = NaryRulePattern {
559            head_arity: 2,
560            body: vec![BodyAtomPattern {
561                candidate_slot: 0,
562                bindings: vec![PatternVar::Head(2), PatternVar::Head(0)],
563            }],
564        };
565        let err = pattern.validate(&[2], &config(2, 1)).unwrap_err();
566        assert!(matches!(err, XlogError::Type(_)), "got {err:?}");
567    }
568
569    #[test]
570    fn validation_refuses_unbound_head_position_as_unsafe_variable() {
571        let pattern = NaryRulePattern {
572            head_arity: 2,
573            body: vec![BodyAtomPattern {
574                candidate_slot: 0,
575                bindings: vec![PatternVar::Head(0), PatternVar::Join(0)],
576            }],
577        };
578        let err = pattern.validate(&[2], &config(2, 1)).unwrap_err();
579        assert!(matches!(err, XlogError::UnsafeVariable(v) if v == "h1"));
580    }
581
582    #[test]
583    fn validation_refuses_non_dense_join_numbering() {
584        let pattern = NaryRulePattern {
585            head_arity: 1,
586            body: vec![BodyAtomPattern {
587                candidate_slot: 0,
588                bindings: vec![PatternVar::Head(0), PatternVar::Join(1)],
589            }],
590        };
591        let err = pattern.validate(&[2], &config(2, 2)).unwrap_err();
592        assert!(matches!(err, XlogError::Type(_)), "got {err:?}");
593    }
594
595    #[test]
596    fn validation_refuses_arity_mismatch_against_declared_candidate() {
597        let pattern = NaryRulePattern {
598            head_arity: 1,
599            body: vec![BodyAtomPattern {
600                candidate_slot: 0,
601                bindings: vec![PatternVar::Head(0)],
602            }],
603        };
604        let err = pattern.validate(&[3], &config(2, 1)).unwrap_err();
605        assert!(matches!(err, XlogError::Type(_)), "got {err:?}");
606    }
607
608    #[test]
609    fn pattern_space_guard_refuses_instead_of_truncating() {
610        let arities = [2u8, 2u8];
611        let cfg = NaryEnumerationConfig {
612            max_body_atoms: 2,
613            max_join_vars: 1,
614            max_patterns: 3,
615            max_traversal_nodes: 1_000_000,
616        };
617        let err = enumerate_patterns(2, &arities, &cfg).unwrap_err();
618        assert!(
619            matches!(err, XlogError::Execution(ref m) if m.contains("max_patterns")),
620            "got {err:?}"
621        );
622    }
623
624    #[test]
625    fn traversal_guard_fires_on_work_not_only_on_output() {
626        // The reviewer's probe: an IN-CONTRACT request whose pattern cap can
627        // never fire, because the search walks an enormous dead-end space
628        // without keeping anything. Before the node budget this returned
629        // Ok(empty) after millions of nodes; now it refuses.
630        let arities = [2u8; 8];
631        let cfg = NaryEnumerationConfig {
632            max_body_atoms: 8,
633            max_join_vars: 8,
634            max_patterns: 1,
635            max_traversal_nodes: 10_000,
636        };
637        let err = enumerate_patterns(8, &arities, &cfg).unwrap_err();
638        assert!(
639            matches!(
640                err,
641                XlogError::Execution(ref m) if m.contains("max_traversal_nodes")
642            ),
643            "got {err:?}"
644        );
645    }
646
647    #[test]
648    fn traversal_budget_does_not_refuse_a_bounded_request() {
649        // The guard must not fire on lawful small requests — a check that
650        // can fail in BOTH directions.
651        let arities = [2u8, 2u8];
652        let cfg = NaryEnumerationConfig {
653            max_body_atoms: 2,
654            max_join_vars: 1,
655            max_patterns: 1_000,
656            max_traversal_nodes: 1_000_000,
657        };
658        let patterns = enumerate_patterns(2, &arities, &cfg).expect("bounded request");
659        assert!(!patterns.is_empty());
660    }
661}