Skip to main content

nibli_semantics/
lib.rs

1//! nibli-semantics: flat AST buffer → FOL logic buffer. An internal
2//! Rust pipeline stage of the single `nibli-pipeline` WASM component (NOT a standalone
3//! WIT component). Compiles nibli-kr's
4//! flat AST buffer into a flat First-Order Logic buffer via the [`SemanticCompiler`],
5//! then flattens the tree-structured [`IrForm`] IR into the WIT-compatible
6//! index-based [`LogicBuffer`].
7//!
8//! The flattener expands `Biconditional` and `Xor` IR nodes into primitive
9//! `And`/`Or`/`Not` nodes (sharing sub-tree indices for zero-cost duplication).
10
11/// Predicate-arity facade over the committed English corpus.
12pub mod dictionary;
13/// First-Order Logic IR types (`IrTerm`, `IrForm`).
14pub mod ir;
15/// Semantic compiler: AST → FOL logic form tree.
16pub mod semantic;
17
18use ir::{IrForm, IrTerm};
19use nibli_types::ast as flat_ast;
20use nibli_types::error::NibliError;
21use nibli_types::logic::{LogicBuffer, LogicNode, LogicalTerm};
22use semantic::SemanticCompiler;
23
24/// Structural validation of an [`flat_ast::AstBuffer`] at the PUBLIC compile
25/// boundary — a MECHANISM, not call-site discipline (the same pattern as the
26/// assert-boundary groundness drop): every index reachable from `roots` must be
27/// in bounds, and reference chains must be acyclic. The recursive compiler
28/// would otherwise PANIC on an out-of-bounds index or overflow the stack on a
29/// reference cycle — both crash classes for a hand-built/corrupt buffer (the
30/// nibli-kr emitter produces valid buffers by construction; this guards the
31/// programmatic path). Sharing (a DAG) is legal — only true cycles reject.
32/// Iterative DFS, so an adversarially deep buffer cannot overflow the
33/// validator itself.
34fn validate_ast_buffer(ast: &flat_ast::AstBuffer) -> Result<(), NibliError> {
35    use flat_ast::{Argument, ModalTag, Predicate, Sentence};
36
37    #[derive(Clone, Copy, PartialEq)]
38    enum Kind {
39        Sel,
40        Sum,
41        Sen,
42    }
43    #[derive(Clone, Copy, PartialEq)]
44    enum State {
45        White,
46        Grey,
47        Black,
48    }
49    let err = |kind: &str, idx: u32, len: usize| {
50        NibliError::Semantic(format!(
51            "corrupt AST buffer: {kind} index {idx} out of bounds (len {len}) — \
52             rejecting the whole buffer (fail closed)"
53        ))
54    };
55    let cycle_err = |kind: &str, idx: u32| {
56        NibliError::Semantic(format!(
57            "corrupt AST buffer: {kind} index {idx} participates in a reference \
58             cycle — rejecting the whole buffer (fail closed)"
59        ))
60    };
61
62    // Typed-split invariant: a `Variable` payload carries its `$` sigil —
63    // variable identity IS the sigiled interned string (the IR-layer
64    // free-variable closure and scope-marker passes key on the prefix). A
65    // sigil-less payload can only come from a hand-built buffer; it would
66    // compile as a variable those passes ignore (a free-variable leak) and a
67    // pronoun-spelled one would re-render as a reparse-flipping pronoun.
68    for (i, argument) in ast.arguments.iter().enumerate() {
69        if let Argument::Variable(v) = argument {
70            if !v.starts_with('$') {
71                return Err(NibliError::Semantic(format!(
72                    "corrupt AST buffer: argument index {i} is a Variable \
73                     without its `$` sigil ({v:?}) — rejecting the whole \
74                     buffer (fail closed)"
75                )));
76            }
77        }
78    }
79
80    // Child references of one node: (kind, index) pairs.
81    let children = |kind: Kind, idx: u32| -> Vec<(Kind, u32)> {
82        match kind {
83            Kind::Sel => match &ast.predicates[idx as usize] {
84                Predicate::Root(_) => vec![],
85                Predicate::Pair((m, h)) => vec![(Kind::Sel, *m), (Kind::Sel, *h)],
86                Predicate::Converted((_, i)) | Predicate::Negated(i) | Predicate::Grouped(i) => {
87                    vec![(Kind::Sel, *i)]
88                }
89                Predicate::WithArgs((core, args)) => {
90                    let mut v = vec![(Kind::Sel, *core)];
91                    v.extend(args.iter().map(|a| (Kind::Sum, *a)));
92                    v
93                }
94                Predicate::Abstraction((_, s)) => vec![(Kind::Sen, *s)],
95            },
96            Kind::Sum => match &ast.arguments[idx as usize] {
97                Argument::Variable(_)
98                | Argument::Marker(_)
99                | Argument::Pronoun(_)
100                | Argument::Name(_)
101                | Argument::QuotedLiteral(_)
102                | Argument::Unspecified
103                | Argument::Number(_) => vec![],
104                Argument::Description((_, s)) | Argument::QuantifiedDescription((_, _, s)) => {
105                    vec![(Kind::Sel, *s)]
106                }
107                Argument::Tagged((_, i)) => vec![(Kind::Sum, *i)],
108                Argument::ModalTagged((modal, i)) => {
109                    let mut v = vec![(Kind::Sum, *i)];
110                    let ModalTag(s) = modal;
111                    v.push((Kind::Sel, *s));
112                    v
113                }
114                Argument::Restricted((i, clause)) => {
115                    vec![(Kind::Sum, *i), (Kind::Sen, clause.body_sentence)]
116                }
117            },
118            Kind::Sen => match &ast.sentences[idx as usize] {
119                Sentence::Simple(b) => {
120                    let mut v = vec![(Kind::Sel, b.relation)];
121                    v.extend(b.terms.iter().map(|t| (Kind::Sum, *t)));
122                    v
123                }
124                Sentence::Connected((_, l, r)) => vec![(Kind::Sen, *l), (Kind::Sen, *r)],
125                Sentence::Prenex((_, body)) => vec![(Kind::Sen, *body)],
126                Sentence::Quantified((_, _, restr, clause, body)) => {
127                    let mut v = vec![(Kind::Sel, *restr)];
128                    if let Some(c) = clause {
129                        v.push((Kind::Sen, *c));
130                    }
131                    v.push((Kind::Sen, *body));
132                    v
133                }
134            },
135        }
136    };
137    let meta = |kind: Kind| -> (&'static str, usize) {
138        match kind {
139            Kind::Sel => ("predicate", ast.predicates.len()),
140            Kind::Sum => ("argument", ast.arguments.len()),
141            Kind::Sen => ("sentence", ast.sentences.len()),
142        }
143    };
144
145    let mut states = [
146        vec![State::White; ast.predicates.len()],
147        vec![State::White; ast.arguments.len()],
148        vec![State::White; ast.sentences.len()],
149    ];
150    let slot = |k: Kind| match k {
151        Kind::Sel => 0usize,
152        Kind::Sum => 1,
153        Kind::Sen => 2,
154    };
155
156    // Explicit-stack DFS with enter/exit markers (three-color cycle detection).
157    let mut stack: Vec<(Kind, u32, bool)> = Vec::new();
158    for &root in &ast.roots {
159        if root as usize >= ast.sentences.len() {
160            return Err(err("root sentence", root, ast.sentences.len()));
161        }
162        stack.push((Kind::Sen, root, false));
163        while let Some((k, i, exited)) = stack.pop() {
164            if exited {
165                states[slot(k)][i as usize] = State::Black;
166                continue;
167            }
168            match states[slot(k)][i as usize] {
169                State::Black => continue,
170                // Re-entered while still in progress: only a descendant of the
171                // node itself can pop its Enter marker before its Exit marker.
172                State::Grey => return Err(cycle_err(meta(k).0, i)),
173                State::White => {}
174            }
175            states[slot(k)][i as usize] = State::Grey;
176            stack.push((k, i, true));
177            for (ck, ci) in children(k, i) {
178                let (name, len) = meta(ck);
179                if ci as usize >= len {
180                    return Err(err(name, ci, len));
181                }
182                match states[slot(ck)][ci as usize] {
183                    State::Grey => return Err(cycle_err(name, ci)),
184                    State::Black => {}
185                    State::White => stack.push((ck, ci, false)),
186                }
187            }
188        }
189    }
190    Ok(())
191}
192
193/// Core compilation: nibli-kr AST buffer → FOL logic buffer.
194/// Used by both the native API and the WIT export path.
195fn compile_ast(ast: &flat_ast::AstBuffer) -> Result<LogicBuffer, NibliError> {
196    validate_ast_buffer(ast)?;
197    let mut compiler = SemanticCompiler::new();
198    let mut logic_forms = Vec::with_capacity(ast.roots.len());
199
200    // Only compile top-level (root) sentences.
201    // Rel clause bodies live in ast.sentences but are referenced
202    // by index from Argument::Restricted — they are NOT roots.
203    for &root_idx in ast.roots.iter() {
204        logic_forms.push(compiler.compile_sentence(
205            root_idx,
206            &ast.predicates,
207            &ast.arguments,
208            &ast.sentences,
209        ));
210    }
211
212    // Check for semantic errors accumulated during compilation.
213    if let Some(err) = compiler.errors.first() {
214        return Err(NibliError::Semantic(err.clone()));
215    }
216
217    let mut nodes = Vec::new();
218    let mut roots = Vec::with_capacity(logic_forms.len());
219
220    for form in logic_forms {
221        let root_id = flatten_form(&form, &mut nodes, &compiler.interner);
222        roots.push(root_id);
223    }
224
225    Ok(LogicBuffer { nodes, roots })
226}
227
228/// Recursively flatten a [`IrForm`] tree into the flat `nodes` array.
229///
230/// Returns the index of the root node in the array. String interning keys
231/// are resolved to `String` at this boundary for WIT serialization.
232/// `Biconditional` and `Xor` are expanded into primitive `And`/`Or`/`Not`.
233fn flatten_form(form: &IrForm, nodes: &mut Vec<LogicNode>, interner: &lasso::Rodeo) -> u32 {
234    match form {
235        IrForm::Predicate { relation, args } => {
236            let wit_args = args
237                .iter()
238                .map(|a| match a {
239                    IrTerm::Variable(v) => LogicalTerm::Variable(interner.resolve(v).to_string()),
240                    IrTerm::Constant(c) => LogicalTerm::Constant(interner.resolve(c).to_string()),
241                    IrTerm::Description(d) => {
242                        LogicalTerm::Description(interner.resolve(d).to_string())
243                    }
244                    IrTerm::Unspecified => LogicalTerm::Unspecified,
245                    IrTerm::Number(n) => LogicalTerm::Number(*n),
246                })
247                .collect();
248
249            let id = nodes.len() as u32;
250            nodes.push(LogicNode::Predicate((
251                interner.resolve(relation).to_string(),
252                wit_args,
253            )));
254            id
255        }
256        IrForm::And(left, right) => {
257            let l_id = flatten_form(left, nodes, interner);
258            let r_id = flatten_form(right, nodes, interner);
259            let id = nodes.len() as u32;
260            nodes.push(LogicNode::AndNode((l_id, r_id)));
261            id
262        }
263        IrForm::Or(left, right) => {
264            let l_id = flatten_form(left, nodes, interner);
265            let r_id = flatten_form(right, nodes, interner);
266            let id = nodes.len() as u32;
267            nodes.push(LogicNode::OrNode((l_id, r_id)));
268            id
269        }
270        IrForm::Not(inner) => {
271            let inner_id = flatten_form(inner, nodes, interner);
272            let id = nodes.len() as u32;
273            nodes.push(LogicNode::NotNode(inner_id));
274            id
275        }
276        IrForm::Exists(v, body) => {
277            let b_id = flatten_form(body, nodes, interner);
278            let id = nodes.len() as u32;
279            nodes.push(LogicNode::ExistsNode((
280                interner.resolve(v).to_string(),
281                b_id,
282            )));
283            id
284        }
285        IrForm::ForAll(v, body) => {
286            let b_id = flatten_form(body, nodes, interner);
287            let id = nodes.len() as u32;
288            nodes.push(LogicNode::ForAllNode((
289                interner.resolve(v).to_string(),
290                b_id,
291            )));
292            id
293        }
294        IrForm::Past(inner) => {
295            let inner_id = flatten_form(inner, nodes, interner);
296            let id = nodes.len() as u32;
297            nodes.push(LogicNode::PastNode(inner_id));
298            id
299        }
300        IrForm::Present(inner) => {
301            let inner_id = flatten_form(inner, nodes, interner);
302            let id = nodes.len() as u32;
303            nodes.push(LogicNode::PresentNode(inner_id));
304            id
305        }
306        IrForm::Future(inner) => {
307            let inner_id = flatten_form(inner, nodes, interner);
308            let id = nodes.len() as u32;
309            nodes.push(LogicNode::FutureNode(inner_id));
310            id
311        }
312        IrForm::Obligatory(inner) => {
313            let inner_id = flatten_form(inner, nodes, interner);
314            let id = nodes.len() as u32;
315            nodes.push(LogicNode::ObligatoryNode(inner_id));
316            id
317        }
318        IrForm::Permitted(inner) => {
319            let inner_id = flatten_form(inner, nodes, interner);
320            let id = nodes.len() as u32;
321            nodes.push(LogicNode::PermittedNode(inner_id));
322            id
323        }
324        IrForm::Count { var, count, body } => {
325            let b_id = flatten_form(body, nodes, interner);
326            let id = nodes.len() as u32;
327            nodes.push(LogicNode::CountNode((
328                interner.resolve(var).to_string(),
329                *count,
330                b_id,
331            )));
332            id
333        }
334        IrForm::Biconditional(left, right) => {
335            // Expand A ↔ B to (¬A ∨ B) ∧ (¬B ∨ A) using shared sub-tree indices
336            let l_id = flatten_form(left, nodes, interner);
337            let r_id = flatten_form(right, nodes, interner);
338            let not_l = nodes.len() as u32;
339            nodes.push(LogicNode::NotNode(l_id));
340            let not_r = nodes.len() as u32;
341            nodes.push(LogicNode::NotNode(r_id));
342            let impl1 = nodes.len() as u32;
343            nodes.push(LogicNode::OrNode((not_l, r_id)));
344            let impl2 = nodes.len() as u32;
345            nodes.push(LogicNode::OrNode((not_r, l_id)));
346            let id = nodes.len() as u32;
347            nodes.push(LogicNode::AndNode((impl1, impl2)));
348            id
349        }
350        IrForm::Xor(left, right) => {
351            // Expand A ⊕ B to (A ∨ B) ∧ ¬(A ∧ B) using shared sub-tree indices
352            let l_id = flatten_form(left, nodes, interner);
353            let r_id = flatten_form(right, nodes, interner);
354            let or_id = nodes.len() as u32;
355            nodes.push(LogicNode::OrNode((l_id, r_id)));
356            let and_id = nodes.len() as u32;
357            nodes.push(LogicNode::AndNode((l_id, r_id)));
358            let not_and = nodes.len() as u32;
359            nodes.push(LogicNode::NotNode(and_id));
360            let id = nodes.len() as u32;
361            nodes.push(LogicNode::AndNode((or_id, not_and)));
362            id
363        }
364    }
365}
366
367/// Compile a nibli-kr-produced AST buffer into a logic buffer.
368/// Primary API for all callers (nibli-pipeline, nibli-engine).
369pub fn compile_from_ast(ast: flat_ast::AstBuffer) -> Result<LogicBuffer, NibliError> {
370    compile_ast(&ast)
371}
372
373/// Compile a directly-injected ground fact `(relation, args)` into the SAME
374/// event-decomposed, arity-padded FOL shape that a surface assertion of
375/// `relation` produces — so injected facts are matched by surface text queries
376/// (`la .adam. cu gerku` matches `:assert gerku adam`), not just by raw-FOL or
377/// same-shape direct facts.
378///
379/// Used by the trusted programmatic injection APIs (nibli-engine
380/// `assert_fact_direct`, nibli-pipeline's WIT `assert-fact`, the REPL `:assert`). Mirrors
381/// `apply_predicate`'s `Predicate::Root` arm so the stored shape is identical
382/// to text assertion, under the INJECTED-ARITY POLICY
383/// (`LexiconSchema::injected_arity`): a known relation pads to its corpus
384/// arity and FAILS CLOSED on over-arity; an unknown relation takes the
385/// caller's argument count as ground truth (no arity-2 guess, no silent
386/// truncation). The identity relation is the one exception — it stays a
387/// FLAT 2-arg predicate (NOT event-decomposed, n-ary fails closed), because
388/// nibli-reason's union-find equality interception only fires on
389/// `relations::IDENTITY` at arity 2.
390pub fn compile_injected_fact(
391    relation: &str,
392    args: &[LogicalTerm],
393) -> Result<LogicBuffer, NibliError> {
394    let mut compiler = SemanticCompiler::new();
395    let ir_args: Vec<IrTerm> = args
396        .iter()
397        .map(|t| wit_term_to_ir(t, &mut compiler.interner))
398        .collect();
399
400    let form = if relation == nibli_types::relations::IDENTITY {
401        if ir_args.len() > 2 {
402            return Err(NibliError::Semantic(format!(
403                "the identity relation is 2-place, but {} arguments were supplied; \
404                 n-ary identity is unsupported (mirrors the text path's reject)",
405                ir_args.len()
406            )));
407        }
408        let fitted = SemanticCompiler::fit_args(&ir_args, 2);
409        IrForm::Predicate {
410            relation: compiler
411                .interner
412                .get_or_intern(nibli_types::relations::IDENTITY),
413            args: fitted,
414        }
415    } else {
416        let arity = crate::dictionary::LexiconSchema::injected_arity(relation, ir_args.len())
417            .map_err(NibliError::Semantic)?;
418        let fitted = SemanticCompiler::fit_args(&ir_args, arity);
419        compiler.event_decompose(relation, &fitted)
420    };
421
422    let mut nodes = Vec::new();
423    let root = flatten_form(&form, &mut nodes, &compiler.interner);
424    Ok(LogicBuffer {
425        nodes,
426        roots: vec![root],
427    })
428}
429
430/// Convert a flat WIT `LogicalTerm` to the interned nibli-semantics IR `IrTerm`
431/// (the inverse of `flatten_form`'s Predicate arm).
432fn wit_term_to_ir(term: &LogicalTerm, interner: &mut lasso::Rodeo) -> IrTerm {
433    match term {
434        LogicalTerm::Variable(v) => IrTerm::Variable(interner.get_or_intern(v)),
435        LogicalTerm::Constant(c) => IrTerm::Constant(interner.get_or_intern(c)),
436        LogicalTerm::Description(d) => IrTerm::Description(interner.get_or_intern(d)),
437        LogicalTerm::Unspecified => IrTerm::Unspecified,
438        LogicalTerm::Number(n) => IrTerm::Number(*n),
439    }
440}
441
442#[cfg(test)]
443mod ast_buffer_validation_tests {
444    //! Negative controls for the compile-boundary AST validation: a hand-built
445    //! corrupt buffer must be REJECTED with a Semantic error — never a slice
446    //! panic (out-of-bounds index) or a stack overflow (reference cycle).
447    use super::compile_from_ast;
448    use nibli_types::ast::*;
449
450    fn bare_proposition(relation: u32, terms: Vec<u32>) -> Sentence {
451        let x1_present = !terms.is_empty();
452        Sentence::Simple(Proposition {
453            relation,
454            terms,
455            x1_present,
456            negated: false,
457            tense: None,
458            deontic: None,
459        })
460    }
461
462    fn expect_corrupt(ast: AstBuffer, what: &str) {
463        match compile_from_ast(ast) {
464            Err(nibli_types::error::NibliError::Semantic(msg)) => assert!(
465                msg.contains("corrupt AST buffer"),
466                "{what}: expected the corrupt-buffer rejection, got: {msg}"
467            ),
468            other => panic!("{what}: expected Err(Semantic(corrupt ...)), got {other:?}"),
469        }
470    }
471
472    #[test]
473    fn oob_root_sentence_rejected() {
474        expect_corrupt(
475            AstBuffer {
476                predicates: vec![],
477                arguments: vec![],
478                sentences: vec![],
479                roots: vec![0],
480            },
481            "root index into empty sentences",
482        );
483    }
484
485    #[test]
486    fn oob_proposition_relation_rejected() {
487        expect_corrupt(
488            AstBuffer {
489                predicates: vec![],
490                arguments: vec![],
491                sentences: vec![bare_proposition(7, vec![])],
492                roots: vec![0],
493            },
494            "proposition relation predicate index",
495        );
496    }
497
498    #[test]
499    fn oob_proposition_term_rejected() {
500        expect_corrupt(
501            AstBuffer {
502                predicates: vec![Predicate::Root("gerku".to_string())],
503                arguments: vec![],
504                sentences: vec![bare_proposition(0, vec![3])],
505                roots: vec![0],
506            },
507            "proposition head term argument index",
508        );
509    }
510
511    #[test]
512    fn oob_nested_pair_arm_rejected() {
513        expect_corrupt(
514            AstBuffer {
515                predicates: vec![
516                    Predicate::Pair((1, 99)),
517                    Predicate::Root("sutra".to_string()),
518                ],
519                arguments: vec![],
520                sentences: vec![bare_proposition(0, vec![])],
521                roots: vec![0],
522            },
523            "pair head predicate index",
524        );
525    }
526
527    #[test]
528    fn oob_rel_clause_sentence_rejected() {
529        expect_corrupt(
530            AstBuffer {
531                predicates: vec![Predicate::Root("gerku".to_string())],
532                arguments: vec![
533                    Argument::Name("adam".to_string()),
534                    Argument::Restricted((
535                        0,
536                        RelClause {
537                            kind: RelClauseKind::Restrictive,
538                            body_sentence: 42,
539                        },
540                    )),
541                ],
542                sentences: vec![bare_proposition(0, vec![1])],
543                roots: vec![0],
544            },
545            "relative-clause body sentence index",
546        );
547    }
548
549    #[test]
550    fn sentence_self_cycle_rejected() {
551        // Prenex whose body is ITSELF: the recursive compiler would overflow
552        // the stack — same crash class as an OOB panic, same rejection.
553        expect_corrupt(
554            AstBuffer {
555                predicates: vec![],
556                arguments: vec![],
557                sentences: vec![Sentence::Prenex((vec!["da".to_string()], 0))],
558                roots: vec![0],
559            },
560            "prenex self-cycle",
561        );
562    }
563
564    #[test]
565    fn cross_array_cycle_rejected() {
566        // predicate 0 = Abstraction -> sentence 0, whose proposition relation = predicate 0.
567        expect_corrupt(
568            AstBuffer {
569                predicates: vec![Predicate::Abstraction((AbstractionKind::Event, 0))],
570                arguments: vec![],
571                sentences: vec![bare_proposition(0, vec![])],
572                roots: vec![0],
573            },
574            "abstraction/proposition cross-array cycle",
575        );
576    }
577
578    #[test]
579    fn shared_subterm_dag_still_compiles() {
580        // Sharing is NOT a cycle: the same argument referenced twice must compile.
581        let ast = AstBuffer {
582            predicates: vec![Predicate::Root("batci".to_string())],
583            arguments: vec![Argument::Name("adam".to_string())],
584            sentences: vec![bare_proposition(0, vec![0, 0])],
585            roots: vec![0],
586        };
587        compile_from_ast(ast).expect("a shared (DAG) subterm is legal");
588    }
589
590    #[test]
591    fn sigil_less_variable_rejected() {
592        // Typed-split invariant: `Variable` carries its `$` sigil. A hand-built
593        // sigil-less payload would compile as a variable the IR-layer `$`-keyed
594        // passes ignore (a free-variable leak the old string design could not
595        // express), and a pronoun-spelled one ("me") would re-render as a
596        // reparse-flipping pronoun — both crash classes of the same corruption.
597        for payload in ["me", "da"] {
598            expect_corrupt(
599                AstBuffer {
600                    predicates: vec![Predicate::Root("gerku".to_string())],
601                    arguments: vec![Argument::Variable(payload.to_string())],
602                    sentences: vec![bare_proposition(0, vec![0])],
603                    roots: vec![0],
604                },
605                "sigil-less Variable payload",
606            );
607        }
608    }
609}
610
611#[cfg(test)]
612mod injected_fact_tests {
613    use super::*;
614
615    fn role_count(buf: &LogicBuffer, relation: &str) -> usize {
616        buf.nodes
617            .iter()
618            .filter(|n| {
619                matches!(n, LogicNode::Predicate((r, _))
620                    if r.starts_with(relation) && r.contains("_x"))
621            })
622            .count()
623    }
624
625    #[test]
626    fn unknown_relation_takes_the_callers_arity() {
627        // No arity-2 guess: a 3-arg unknown fact keeps 3 roles…
628        let args = vec![
629            LogicalTerm::Constant("a".into()),
630            LogicalTerm::Constant("b".into()),
631            LogicalTerm::Constant("c".into()),
632        ];
633        let buf = compile_injected_fact("zzz_unknown_rel", &args).unwrap();
634        assert_eq!(role_count(&buf, "zzz_unknown_rel"), 3);
635        // …and a 1-arg one mints no phantom x2(Unspecified).
636        let buf = compile_injected_fact("zzz_unknown_rel", &args[..1]).unwrap();
637        assert_eq!(role_count(&buf, "zzz_unknown_rel"), 1);
638    }
639
640    #[test]
641    fn known_relation_over_arity_fails_closed() {
642        // `product` has corpus arity 3 — a 4th argument must ERROR, never
643        // silently truncate (the pre-policy behavior).
644        let args: Vec<LogicalTerm> = (0..4).map(|n| LogicalTerm::Number(n as f64)).collect();
645        let e = compile_injected_fact("product", &args).unwrap_err();
646        let msg = format!("{e}");
647        assert!(
648            msg.contains("arity 3") && msg.contains("4 arguments"),
649            "{msg}"
650        );
651        // Under-arity still pads to the corpus arity (omitted places).
652        let buf = compile_injected_fact("product", &args[..2]).unwrap();
653        assert_eq!(role_count(&buf, "product"), 3);
654    }
655
656    #[test]
657    fn identity_over_arity_fails_closed() {
658        let args: Vec<LogicalTerm> = (0..3).map(|n| LogicalTerm::Number(n as f64)).collect();
659        let e = compile_injected_fact(nibli_types::relations::IDENTITY, &args).unwrap_err();
660        assert!(format!("{e}").contains("n-ary identity is unsupported"));
661    }
662}