nibli_formalize/lib.rs
1//! # nibli-formalize — agentic English→KB formalizer engine
2//!
3//! An LLM formalizes English into the KB language (nibli KR — the nibli-kr
4//! crate); the output is validated by the real nibli compilers; any error is
5//! fed back into the conversation and the LLM retries until the KB text is
6//! valid (bounded by an attempt cap). This crate is the engine — the UI shell
7//! lives in `nibli-ui`, which surfaces it as the agentic "Formalize" mode
8//! ("compile" stays reserved for the deterministic KB→logic step; the LLM
9//! step is interpretive formalization behind gates).
10//!
11//! ## Validation gate (the "verify" firewall)
12//!
13//! A candidate must pass three deterministic gates before the loop accepts
14//! it: 1. **nibli-kr** — `nibli_kr::parse_checked` (grammar + fail-closed alias
15//! resolution) — local. 2. **nibli-semantics** — `nibli_semantics::compile_from_ast`
16//! (semantics/arity) — local. 3. **round-trip** — the candidate's canonical
17//! re-spelling (`nibli_kr::render`) must re-compile to the SAME `LogicBuffer`
18//! (nibli-kr's fixpoint contract as a per-candidate drift-catcher) — local,
19//! native + wasm.
20//!
21//! All gates are local, so the hot validation path makes no network call and
22//! the loop stays fully serverless. (The legacy Lojban chain — gerna + the
23//! wasm-only camxes gate — and the jbotci MCP tool loop retired with the
24//! Lojban front-end at THE DROP.)
25//!
26//! ## Testability
27//!
28//! The gates run on pure Rust nibli crates, so [`gates`] is
29//! native-`cargo test`-able (including the round-trip gate). The LLM
30//! `chat()` is abstracted behind a seam so the agent/provider logic tests
31//! with mocks on native, and only the concrete transport is wasm-only.
32
33pub mod agent;
34pub mod gates;
35pub mod llm;
36pub mod verify;