AGENTS.md

Nibli

A Zero-Hallucination Symbolic Reasoning Engine.

Nibli is a deterministic theorem prover compiled to WebAssembly (WASI P2). It compiles nibli KR — the nibli knowledge-representation (KR) language, a human-readable predicate-call surface — into First-Order Logic and performs inference via demand-driven backward-chaining over an indexed fact store. Every conclusion is a formal derivation from the facts + rules you assert, under a closed-world + closed-domain assumption (compute-backend results are trusted as axioms); nothing is fabricated. A FALSE verdict means "not derivable," not "proved ¬P". (README's "What zero-hallucination means here" has the full scoping.)

Environment

OS: Ubuntu on WSL2. The agent is already running inside WSL in this repository.
Dev shell: Nix flake — all tools (rustc, cargo-component, wac, just, wasmtime) come from flake.nix
Enter dev shell: nix develop --extra-experimental-features nix-command --extra-experimental-features flakes
Run commands directly here: use the current Linux shell and Linux paths. For example: nix develop --extra-experimental-features nix-command --extra-experimental-features flakes --command just check.
Stay in WSL: do not wrap commands in cmd.exe, PowerShell, or wsl.exe. Use Linux-native tools here, including for document rendering and browser automation.

Build & Test

All commands must run inside the Nix dev shell. Use just as the primary task runner (see Justfile):

Command	What it does
`just run`	Full pipeline: clean WASM -> build nibli-pipeline component -> launch REPL (KR-only since THE DROP, 2026-07-13)
`just check`	Fast type-check all workspace crates (`cargo check --workspace`)
`just test`	Run all unit tests (`cargo test --lib -- --nocapture`, parallel — the old `--test-threads=1` constraint died with the thread-local dispatch/cache, now per-KB instance fields)
`just test-engine`	Run nibli-engine integration tests (full pipeline: parse → compile → reason)
`just test-nibli-kr`	Run nibli-kr (surface-syntax front-end) tests only — dev loop; `just test` already sweeps them into `ci`
`just test-alias-map`	Run nibli-lexicon's unit tests only — the committed-corpus tests (lookups, converted/compound entries, provenance bridge, reserved/place invariants, const-guard `#[test]` twins with offender lists, TODO ratchet) — dev loop; `just test` already sweeps them into `ci`
`just verify-nibli-kr-seam`	The KR→nibli-semantics seam-conformance gate — the KR front-end's independent oracle (it OUTLIVED THE DROP as designed) (`nibli-verify/tests/nibli_kr_seam_gate.rs` + the `nibli_kr_seam` generator module): 17 hand-verified FOL structural goldens (event decomposition, ∀-implication vs ∃-conjunction shapes, assertion/query connected-clause `$name` co-reference, converted-alias `owns_x1/x2` routing, the compound `computer_user` golden + its uncurated fail-closed negative, named-arg place routing, explicit Past→Present rule-literal mapping, standalone deontic wrapping, flat `equals`, prenex implication, `__abs_` opacity, exact-count-0, `?`-vs-`$x $x` independence), a 20-case fail-closed mixed tense×deontic matrix over assertion/query/antecedent/conclusion/NAF in both orders, the CONSTRUCT_INVENTORY acceptance sweep (every §3–§9 KR spelling compiles, per-section floors), KR-internal metamorphic relations (the O7 block-every ≡ prenex pin re-anchored KR≡KR + named≡positional + converted≡label-permuted + a 60-seed batch over three families: label permutation, `no`≡`exactly 0`, conjoined≡stacked clause bodies), and the re-homed `determinism_corpus_nibli_kr_native` leg. Single-mode (the committed corpus), never skips. Part of `ci`.
`just verify-alias-map`	Corpus differential gate (`nibli-verify/tests/alias_differential.rs`): the SHIPPED committed corpus's invariants — shape (sorted/unique/ident/reserved/place rules re-asserted with offender lists), provenance integrity (every swap names an existing canonical base of the same arity; `by_provenance` round-trips), compound integrity (relation = name with `+`→`_`, collision-free against atomic names), coverage floors (≥1,300 predicates, ≥3 compounds), PLUS a behavioral battery: for EVERY shipped entry, `name(A, B, …)` must compile canonically EQUAL to its twin — a plain entry to ITSELF under explicit `xN` labels (named ≡ positional routing), a converted entry to its CANONICAL BASE under the permuted labels (the cross-entry conversion oracle). Single-mode, never skips — arity agreement holds by construction (one committed table). Part of `ci`.
`just test-backend`	Run Python backend tests
`just test-host`	Run nibli-host host unit tests (trap classification, error/verdict formatting, arithmetic)
`just test-validate`	Run the `nibli-validate` batch reporter tests (ordinary assertion acceptance, outer exact-count rejection, opaque quoted-content acceptance)
`just test-formalize`	Run nibli-formalize native tests (agentic loop + history trim, the local gates incl. the render round-trip gate, the grounded-prompt guards — few-shots gate-valid + the assembled prompt embeds the pest grammar and the alias map, the semantic verification turn incl. the KR Genesis silent-mistranslation fixture, LLM request/response shapes). Part of `ci`.
`just test-ui`	Run nibli-ui's native tests — the shipped-examples guard (`shipped_examples_compile`): EVERY example KB line + preset query compiles through the nibli KR front-end (single-mode since the committed corpus — no vocab skips; line-count floor). nibli-ui is bin-only, so `just test` (`--lib`) skips it — this gates it in `ci`.
`just test-all`	Run every test suite (unit + integration + Python)
`just ci`	Fast native CI gate (fmt-check, clippy, all native test suites incl. `test-host` + `test-ui` + `test-formalize` + `verify-soundness` + `verify-alias-map` + `verify-nibli-kr-seam` + `verify-dict` + `verify-pins` + `verify-proofs`). No WASM build.
`just verify-soundness`	Differential soundness gate (Track A) — GREEN again since 2026-07-31 (the `utopia_asp_pins_agree_with_clingo` leg had been latently red since `e31de89` added `~($a = $b)` to utopia.nibli, masked by earlier `ci` legs failing first; fixed by mapping non-ground `equals` to clingo `==`/`!=`). Two oracles over KR-generated programs: (1) Vampire (classical FOL) over the Horn/NAF-free fragment — curated cases (incl. ground `=`-equality mapped to TPTP native `=`), a seeded batch of random Horn programs with mixed-in identity links (`NIBLI_VERIFY_RANDOM_COUNT`, default 200), the auto-extracted mappable slice of the `gdpr`/`ddi` corpora, and the Predilex taxonomy leg (`run_predilex_taxonomy`) — real-vocabulary rule programs from the vendored Predilex hypernym links, each Lojban lemma mapped through `by_provenance` to its English corpus name before the fail-closed KR pre-filter (39 checked, floor 35); (2) clingo (ASP/Datalog) over the stratified-NAF + closed-world fragment — a curated NAF corpus (incl. the real GDPR deontic-NAF erasure rule and `=`×NAF cases) + random stratified-NAF programs (`NIBLI_VERIFY_NAF_RANDOM_COUNT`, default 100). Ordinary-predicate tense flavors (`past`/`now`/`future`) are covered by both oracles via the flavorization pre-pass (`tense.rs`): bare rule literals stay Bare, while explicit wrappers declare same- or cross-flavor mappings, and every curated `tense_` case must reach its oracle rather than skip; this includes tense×NAF (a `past ~P` restrictor flavorizes to `not P__pu`; the flavor-aware `NegatedExistsGroup`), with curated + random tense×NAF legs (`NIBLI_VERIFY_TENSE_NAF_RANDOM_COUNT`, default 100); exact-count queries as `#count` aggregates (`NIBLI_VERIFY_COUNT_RANDOM_COUNT`, default 100). Plus (3) the non-stratified-rejection differential* (`strat_diff.rs`, `NIBLI_VERIFY_STRAT_RANDOM_COUNT`, default 300) with the post-rejection fresh-replay battery, (4) the retraction metamorphic differential (`retract_diff.rs`, `NIBLI_VERIFY_RETRACT_RANDOM_COUNT`, default 200) — retract ≡ never-asserted (ONE rebuild path since 2026-08-01: the incremental branch left retracted members in the quantifier domain; the battery's quantified + numeric rows are what caught it), and (5) the materialisation metamorphic differential (`materialize_diff.rs`, `NIBLI_VERIFY_MATERIALIZE_RANDOM_COUNT`, default 60 — fewer than the other differentials because the OFF side IS the slow path this optimisation removes, so each program costs ~3 s in a debug build; ~3 min for the leg) — saturated ≡ backward-chained: every generated stratified-NAF program runs on two fresh engines (materialisation ON and OFF) over an entity×predicate battery, and a DEFINITIVE verdict may never change; the only permitted difference is OFF non-definitive → ON definitive (the depth-bound completeness gain). The generator mixes in the shapes materialisation must REFUSE (`du` links, `past` facts, positive-cycle recursion), so a refusal that decayed into an approximation fails here. All three native-only, never skip. Needs `vampire` + `clingo` for oracles (1)+(2) (Nix shell; each side skips if its solver is absent). Part of `ci`.
`just verify-dict`	Dictionary-arity differential gate: the committed corpus's arities must COVER independent lower bounds derived from Predilex (CC0 thesaurus of sememes-as-predicates, vendored + SHA-pinned in `nibli-verify/vendor/predilex/`; the data rules live in `nibli-verify/src/predilex.rs`), keyed through the `by_provenance` gismu→English bridge. Predilex sememes are systematically coarser than Lojban place structures, so the sound invariant is a LOWER BOUND: an undercount (corpus arity < bound) flags a truncated place structure (its first run caught the `cusku` 3→4 override pin); overcounts pass as expected coarseness. `KNOWN_UNDERCOUNTS` allowlist (value-pinned, still-undercounting invariant) holds hand-verified lensisku definition-text gaps only. Single-mode, never skips: 132 checked, floor 120. Part of `ci`.
`just verify-pins`	KB-level behavioural pins (`nibli-pin`, native — no wasm, no fuel, seconds): guards EMERGENT engine properties a knowledge base depends on but cannot state. Chiefly the rights-floor stratification firewall — a KB asserts `entitled(every person, event { P() }).` and relies on the engine REFUSING any rule that punishes the absence of P; that refusal falls out of the `flatten_consequent` (descends the abstraction body → `P -> person` dep edge) vs `collect_ground_facts` (honours `__abs_` opacity → no actuality leaks) ASYMMETRY in nibli-reason, so a pin in a downstream repo would never fire on the refactor that breaks it. Pin files are `pins/*.nibli`: `:refuse <class> /needle/` and `:accept` are duals SCOPED TO THE NEXT STATEMENT (class matched on the `NibliError` variant, so a typo — a `Syntax` error — can never satisfy a `:refuse reasoning`), `? <query>` + a MANDATORY `# => <verdict>` annotation, and a per-file `:expect-pins <n>` anti-hollowing floor. `RESOURCE_EXCEEDED` is structurally unpinnable (fuel is a host budget the native engine does not enforce). EXIT CODES ARE DISTINCT: `1` = a pinned property regressed, `2` = the script/harness is broken (nothing was learned). Harness self-tests live in the bin (`cargo test -p nibli --bin nibli-pin`). Skips cleanly when `pins/` is empty. Part of `ci`.
`nibli-pin --strata --kb <file>`	Dump the engine's STRATIFICATION as stable TSV to stdout, then exit (runs no pins; needs `--kb`, takes no pin file). One row per predicate: `predicate <TAB> stratum <TAB> base\|derived <TAB> edges`, edges `+name`/`-name` for positive/negative (NAF). Exists so a CONSUMING project reads the engine's own stratification instead of re-deriving it — a book computing chapter order from a constitution was regexing `.nibli` text to rebuild the predicate graph, i.e. a second stratifier maintained by someone who cannot see this code, and numbers printed as "the engine computed this order" have to come from the engine that enforces it. Backed by `KnowledgeBase::stratification_report()` -> `Vec<StratumRow>` (public, native-only, no WIT change). Names are SURFACE relations: role predicates (`p_x1`) collapse onto their anchor, which is lossless because the anchor and its roles carry identical dependency sets and so always share a stratum (pinned by `strata_surface_projection_is_lossless` over four corpora). A surviving self-edge is GENUINE recursion, not a decomposition artifact. `event`/`__abs_v1_<digest>_<key>` (abstraction artifacts) and `equals` (the `=` builtin — `~($a = $b)` IS a negative edge that raises the reader's stratum) are LISTED, not hidden: silently dropping nodes is how re-derivations come to disagree. Rule heads absent from `pred_dep_graph` (a conditionless rule pushes no edges) are emitted at stratum 0 rather than vanishing. A fixture that fails to load yields harness errors and an EMPTY dump — partial numbers still look like numbers.
`nibli-pin --kb <fixture>`	TWO KINDS OF PIN. Mechanism pins guard the ENGINE: fixture INLINE (an edit elsewhere weakening it would silently weaken a nibli guarantee) — everything under `pins/` is this kind and is marked so in its header. Content pins guard a specific ARTIFACT (a constitution, policy, corpus): the artifact IS the subject, so the fixture must be the LIVE file, loaded with the repeatable `--kb` flag (`nibli-pin --kb constitution.nibli constitution.pins.nibli`) — inlining a content fixture is the failure mode, since the copy drifts and the pins start certifying fiction. Composition is a CLI flag rather than a `:load` directive on purpose: the pin language stays closed, and nothing in `pins/*.nibli` can reference a path outside the repo and break `ci`. Each pin file gets a FRESH engine (no leakage between files); a fixture that fails to load is exit 2 (harness), never exit 1 — if the fixture did not load, no pin ran, so no pinned property could have regressed.
`nibli-pin` `:accept-scoped`	`:accept` that PUTS THE KB BACK. A content file uses `:accept` as a CONTROL ("this rule must still load") and never wants the rule afterwards — but it stayed, so every query below ran against a WIDENED base. In the constitution suite four complement controls each concluded `prisoner`, so a query below them passed with the rule that should derive it deleted, and a `~false` control made a person with NO conviction answer TRUE (verified both ways: `prisoner(Quin)` TRUE under `:accept`, FALSE under `:accept-scoped`). `:refuse` never had this — a refused statement never enters the store — and that ASYMMETRY was the bug; ordering the file so controls came last was the only workaround. Compiles + stratifies, reports loadability as the pin verdict, then retracts. Retraction is the primitive rather than a bespoke undo, so it inherits `retract_diff.rs`'s pinned "retract ≡ never-asserted" (one rebuild path since 2026-08-01). Cannot scope `derived_only`/`admits` (one-way by design, they survive the rebuild replay) — refused as a harness error rather than silently no-op'd. A failed retraction is ALSO harness, not a finding: the KB is polluted and every pin below it is untrustworthy. Composes with `:defect`. Pinned by `pins/scoped-control.nibli`. NOT a blanket replacement for `:accept`: an accept is sometimes a PREMISE the file then queries (write a roster entry, ask what it derived), not a control. Scope one and the accept still passes — the QUERY BELOW flips, so it surfaces as a FINDING at exit 1 and reads as a design regression rather than a mis-edited pin file (measured downstream: 2 findings in one chapter file, 1 in another). The runner cannot distinguish them — "did the author want this rule afterwards" is not a property of the statement — so the file must say which it meant. Scoping controls is also NOT the same as a file not widening its own base: ordinary ground facts above a query stay resident.
`nibli-pin --allow-shell` / `:defect`	TWO KINDS OF PIN CONTENT. A pin usually encodes a GUARANTEE; sometimes it encodes a DEFECT the artifact currently HAS and a chapter argues about. Both are `? q.` + `# => V`, so a flip read identically while meaning opposite things. `:defect "<what flips it>"` marks the NEXT pin (orthogonal to `:accept`/`:refuse`, may precede one; reason MANDATORY — a bare marker cannot tell a reader what to do when it fires). A marked pin that still reproduces is COUNTED (summary gains `(N encode defects that still reproduce)`); one that stops reproducing is exit 3, "a pinned defect no longer reproduces", NOT a finding — the artifact improved, and calling that a regression trains readers to ignore the one message meaning "update the prose". Precedence: harness 2 > finding 1 > resolved 3. INERT when unused: output stays byte-identical, so a consuming suite that parses it need not change. A dangling `:defect`, or one marking a non-pin statement, is a harness error (silent no-op refused as everywhere else). `:require <shell>` runs a precondition for things that are ABSENCES and have no query ("nothing reads this predicate" — grep-shaped). GATED behind `--allow-shell` and refused loudly without it, preserving the closed-pin-language rule that nothing under `pins/` executes shell in `ci`; exit 127 is a BROKEN CHECK (harness), not a failing one.
`just verify-pins` (pin files)	`pins/closed-vocabulary.nibli` + `pins/closed-vocabulary-order.nibli` pin the CLOSED BASE VOCABULARY — `admits("<relation>")`, the DUAL of `derived_only`. `derived_only` says which relations may not be asserted; `admits` says which may, and without it any corpus name still entered fail-open, so a KB claiming its record has exactly N entries was claiming something unchecked. OPEN by default (v0.1 behaviour, opt-in closure); the FIRST declaration closes it; thereafter an unadmitted ground assertion is `NibliError::Reasoning` and ATOMIC. Ordering is enforced, not just documented: the `admits` block must precede every ordinary assertion, because a late one would silently GRANDFATHER everything above — the mirror of `derived_only`'s "comes too late", and the same class of false green. EXTENSIONAL only: a rule may still conclude outside the set. Both declaration relations are exempt (`admits("admits")` must be able to store itself). Live state is `admitted: HashSet<String>` on `KnowledgeBaseInner` — absent from `rebuild_inner`'s clear list (retraction replay cannot re-open) but CLEARED by `reset()`. Corpus entry uses the `zzmeta` synthetic-gismu pattern `derived_only` established. Programmatic twins: `declare_admitted`/`is_admitted`/`vocabulary_is_closed`/`admitted_relations`. NOT NIBLI_KR §14.1's `pred` — that v2 feature declares new vocabulary WITH places and replaces the dictionary; this is a whitelist over the shipped corpus.
`just verify-pins` (pin files)	`pins/converse-alias.nibli` pins the converse-alias spelling discipline. `bilga` shipped two spellings — `obliged(bound, duty)` and a CONVERTED alias whose arguments were exchanged — named `obligated`. In English those are the same participle, so nothing in the surface form told a hand-writer that one INVERTED the other: a constitution stating `obliged(Review, $x)` ("the review body owes a duty about this person") meant the opposite if written the other way, and only a hand-written two-pin discriminator stood between that and a green suite. Renamed to `obligated_by` (the `metabolized_by` precedent — `_by` is the corpus's own marker that arguments run the other way), so `obligated(...)` is now a COMPILE ERROR rather than a wrong answer. ~46 call sites migrated across `utopia`/`gdpr`/`readme`/`acceptance` corpora, engine tests, nibli-wasm, the UI example and the verify gates; provably verdict-preserving, since the swap/places are unchanged. The other three converse aliases (`owned`/`owns`, `permitted`/`permits`, `metabolized_by`/`cuts`) were already self-marking — each differs morphologically between passive and active — which is why `obligated`/`obliged` alone was a trap. All four alias TEMPLATES were also de-inverted (they had been copied from the base unpermuted); they are dead for rendering (a stored fact always carries the BASE relation, and `nibli-render`'s `TEMPLATE_OVERRIDES` wins anyway) but were a standing landmine.
`just verify-pins` (pin files)	`pins/temporal-order.nibli` pins order and duration WITHOUT numerals — asked for as a missing "primitive", but no primitive was needed: the committed corpus already carries `earlier`/`later` (arity-2 time-sequence ordering, gismu `purci`/`balvi`), `continue`/`cease` (gismu `ranji`/`sisti`) and `time` (arity 3, "the interval FROM x2 TO x3", gismu `temci`), none with a numeric place. What was missing is that this is GUARANTEED rather than incidental, which is what the pin file supplies. Transitivity is NOT built in (the KB states its own axioms; the closure rule bisects, so a chain longer than `max_chain_depth` still resolves) and asymmetry is NOT enforced (a KB derives it, the `utopia.nibli` `false` shape). "Not yet" is plain NAF over these relations (`~cease(Term, Custody)`) — reach for that rather than tense, since `~past P` is refused and the three flavours carry no ordering. The five entries were refined out of TODO-guessed labels in the same diff (`TODO_BASELINE` 1278 -> 1273). Also covered: `happen` (begins, gismu `cfari`), `end`, `concurrent` (during), `precede`. Honest boundary, in GUARANTEES §Time and Order: no clock, no interval arithmetic, no duration comparison the KB has not asserted itself — but a magnitude may be SYMBOLIC (`year(Term, Two).` compiles, `Two` opaque), so the "numerals are unavoidable" premise is only true of ARITHMETIC, not of stating a term.
`just verify-pins` (pin files)	`pins/numeric-comparison-boundary.nibli` pins the numeric-comparison boundary in BOTH directions, and records that the rule-position capability is DECIDED AGAINST rather than pending (2026-08-08). `greater`/`less`/`num_equal` straddle a seam decided by OPERANDS, not by name: `greater(20, 15)` is computed by a query and never stored, `greater(Alis, Bob)` ("taller than") is an ordinary relational fact. The refusal of the computed reading is pinned in all four asserted positions (ground fact, positive guard, negated guard, head) plus the variable-operand case, and the relational reading is pinned as still asserting, still answering, and still firing a rule — because a name-based ban would have taken it too. Why declined: `greater` has FOUR places, so diverting a comparison out of rule compilation is a GROUP-level rewrite across `typed_conditions` and `negated_exists_groups` (a `~greater` never enters `typed_conditions` at all), with `negated_condition_indices` and `register_rule`'s edge-rollback accounting to match; the ingress guard cannot be made position-aware where it runs (no `ImpliesNode` — a rule arrives as a quantified disjunction over a shared DAG); `materialize::project_rule` does NOT already refuse the shape (`Ineligible::ComputeCondition` fires only on FLAT conditions, and a decomposed comparison projects as an ordinary atom that would be seeded EMPTY and marked COMPLETE — unreachable only because the ingress guard exists, now noted in place); and NEITHER differential oracle can judge arithmetic (Vampire's path is FOF with numbers as `num_<n>` Herbrand constants, the ASP path renders them the same way, and teaching clingo integers is a GLOBAL rendering change whose half-measure — constants compared under a relational operator — is vacuously true by ASP-Core-2 term order, i.e. a WRONG oracle, not a skip). Re-open trigger, in GUARANTEES §Disclosed Sharp Edges: a differential oracle that can judge arithmetic. What the pin file deliberately CANNOT cover: the pin language has no find/count form, so verdict≡enumeration is pinned in Rust (`verdict_and_find_agree_for_every_comparison`, `numeric_threshold_verdict_and_find_agree`) and the header says so rather than letting a reader assume coverage.
`just verify-pins` (pin files)	`pins/derived-only.nibli` additionally pins EDB/IDB separation: `derived_only("<relation>").` closes a relation to DIRECT ASSERTION so it can only ever be concluded by a rule (without it a rule only ADDS a derivation path and never REMOVES assertability, so a KB that derives a credential cannot stop anyone asserting one). Spelled as an ordinary arity-1 ground fact — no grammar form, so it rides the store and buffer replay like any assertion and reaches native/wasmtime/v8 identically via `CoreSession::assert_text`. Intercepted in `nibli-reason::process_assertion`'s ground arm as `asserted_derived_only`, beside the `admits` closed-vocabulary check; refusal is `NibliError::Reasoning` and ATOMIC (the caller's `rebuild_inner` rollback). (The numeric-comparison guard is NOT its sibling any more: `validate_no_operational_comparisons` moved to `preflight_assertion_buffer`, which runs before id allocation, so a refused comparison burns no fact id.) Closes every SURFACE SPELLING, converted aliases included (`permitted` -> `permits`), since the check tests the COMPILED relation. Live state is `derived_only: HashSet<String>` on `KnowledgeBaseInner`: absent from `rebuild_inner`'s clear list (so it survives retraction replay) but CLEARED by `reset()` (it is KB content, not session config like `strict`). Programmatic twin: `KnowledgeBase::declare_derived` / `is_derived_only` / `derived_only_relations`.
`just verify-proofs`	Mechanized-proof gate (Track B): check the Lean 4 soundness proofs in `proofs/` (needs `lean`, provided by the Nix shell; skips if absent). Part of `ci`.
`just ci-wasm`	WASM behavioral gate: build the nibli-pipeline component + run the nibli-host smokes — all payloads KR (script, trap recovery, persist-replay, statement-split + buffer replay, query-only exact-count assertion atomicity, schema-v3 migration — a legacy `StoredAssertion::Text` row recompiles once on open to a `Buffer` row and fails closed non-destructively on a non-KR row, NAF note, `:debug`, collapse, backend-unavailable via `exponential`, query-only reference compute assertion (`exponential`/`logarithm` refused at ingress unregistered, atomically, no durable row), and the corpus-scoped registration contract (unknown registration/query and registered over-arity fail closed; a live stored fact blocks registration naming its id; registration succeeds after retraction; bare `:compute` reports the canonical registry), quiet, strict, existential-import, materialize — the last pins the saturation REPORT across the WIT boundary plus both opt-outs, and that verdicts are identical either way). Determinism legs: `smoke-host-determinism` (the pinned `determinism-corpus.nibli` through the Wasmtime component) and `verify-wasm-node` (the same corpus through the wasm32-unknown-unknown build under node/V8; skips cleanly if wasm-pack is absent). The native leg is `determinism_corpus_nibli_kr_native` (`verify-nibli-kr-seam`).
`just ci-all`	Comprehensive pre-push / pre-release gate: `ci` + `ci-wasm`
`just build-wasm`	Build single nibli-pipeline WASM component
`just build-host`	Build native Wasmtime host nibli-host (runner)
`just backend`	Start the Python reference compute backend (port 5555)
`just run-with-backend`	Build + run with `NIBLI_COMPUTE_ADDR=127.0.0.1:5555`
`just ui`	Launch the standalone Transparency Triad web UI (Dioxus, port 8080) — engine runs fully in-browser
`just build-ui`	Build the nibli-ui web bundle for release (`dx build --release` → `target/dx/nibli-ui/release/web/public/`) — a local preview / pre-merge sanity build; the PRODUCTION build runs in the external dhilipsiva.dev site repo (see `DEPLOY.md`)
`just fetch-dict`	Download the lensisku English dictionary to `dictionary-en.json` (public dump, no login) — ONLY the input of `just regen-lexicon`; never a build input (see Dictionary Data below)
`just regen-lexicon`	Run `tools/lexigen` over `dictionary-en.json`: drift report + new-entry candidates to scratch files — it NEVER rewrites committed corpus entries
`just import FILE [ARGS]`	Import an RDF Turtle / OWL file into a fresh KB via the `nibli-import` CLI (`--raw` skips OWL class handling, `--export` prints the round-trip view, `--query "<text>"` runs entailment checks — reaches only dictionary/alias-resolvable names, fail-closed; English/camelCase RDF predicates import as facts but await the v2 schema registry, NIBLI_KR §14.1). NOTE: just's variadic args lose shell quoting — run `./target/debug/nibli-import` directly for multi-word queries
`just bench-naf`	Timing for negation-as-failure evaluation: release-profile native bench over `utopia.nibli` — the worst NAF shape the shipped corpora contain (`false/1` is concluded by a 3-variable/15-conjunct rule and read under `~`). Legs: corpus load / `naf-true reward(Esa)` (no witness → the search is exhaustive) / `naf-false reward(Bela)` / a same-KB stored-fact `lookup` control, min/median/max over `NIBLI_BENCH_RUNS` runs (default 5), every verdict asserted every run. The source for any NAF latency figure — never hand-write timings. `NIBLI_MATERIALIZE=0` runs the OFF side in the SAME build, so the before/after is one measurement rather than two: naf-true 1039 ms → 0.3 ms, naf-false 1058 ms → under 0.1 ms (the positive-goal probe removed that leg's residual search), lookup 0.3 → under 0.1 ms
`just bench-book`	Timing pins for the book's quoted figures (Ch 13 latency numbers, Ch 19 GDPR sequence): release-profile native bench over `gdpr.nibli` — corpus load / lawful-basis query / full Ch-19 sequence (load + query + consent retraction + 2 re-queries), min/median/max over `NIBLI_BENCH_RUNS` runs (default 10), every verdict asserted every run. The source for any latency figure the book quotes — never hand-write timings
`just verify-book-refs`	Book-reference conformance gate (detection only): every WIT name, REPL command (`nibli-host` + `nibli` debug REPL), Rust struct field, and notation form the book quotes must match the repo (`book/tools/verify_book_refs.py`, per-claim report). EXPECTED red until the book reconciliation pass; wiring into `ci` is a book-repo decision after that. Skips when `book/` is absent
`just count-tests`	Derive the current test-suite counts (unit + native integration/bin targets). The source for any doc that needs a figure — never hand-write test counts (pre-commit checklist)
`just docs [site_url]`	Build the code-derived mdBook site (`mdbook/` → `mdbook/book/`). Default `site-url` from `book.toml` (`/docs/nibli/`); pass e.g. `/nibli/` for GitHub Pages. Not the Orange AVA manuscript. CI `docs` job builds default; `docs-pages.yml` deploys the mirror.
`just docs-pages-build`	`just docs /nibli/` — Pages base path
`just docs-serve`	Serve mdBook locally at http://127.0.0.1:3000
`just release-check`	Release-track consistency gate (R0 — decisions of record in `RELEASING.md`; v0.1.0 shipped 2026-08-03: tag + GitHub Release with component/host/validate artifacts, all 13 Tier A crates live on crates.io): `cargo metadata` + tomllib lint asserting lockstep versions (every member + `[workspace.package]` + every `[workspace.dependencies]` entry at one version), publish flags matching the Tier A/Z decision table (Tier Z + auth crates `publish = false`, Tier A publishable), required crates.io metadata (description/license/repository) on every publishable crate, and NO versionless normal/build path dep on a publishable crate (cargo publish rejects those; probe-tested). Internal DEV-deps are deliberately path-only — cargo strips versionless path dev-deps at publish, so they impose no publish-order constraint (a `workspace = true` dev-dep would be RETAINED and break `cargo publish -p nibli-kr` on unpublished nibli-semantics). The bench bins are REPO-ONLY behind the `bench-bins` feature (`required-features`; bench recipes pass it) — they `include_str!` repo-root corpora no package tarball can carry, which failed tarball verification. nibli-auth-py's wheel version is maturin-`dynamic` from Cargo.toml so it rides the lockstep. Native + offline; run before any tag or publish.
`just verify-doc-fences`	Doc-fence gate (docs Phase 5): every statement inside a ```nibli-kr fence — under `mdbook/src/*.md` AND in the repo-root specs — must compile through `NibliEngine::assert_text`, the same path as the REPL's `:load` and `nibli-validate`. A Rust test (`nibli-verify/tests/doc_fences.rs`) rather than a `nibli-validate` wrapper: `assert!` IS the gate, since nibli-validate always exits 0 (a reporter, not a gate), and the book-side precedent keys its results by statement TEXT — which collapses `animal(every dog).` where it appears in two different pages. CommonMark-shaped fence scanner (state machine over fence char + run length, so a hyphenated info string can never invert fence state); one statement per line, REJECTED not joined, because `:load` is line-oriented and a wrapped statement cannot be pasted; per-fence cumulative KB with `reset()` between fences; ALL failures collected, reported as file:line + statement + verbatim compiler error; PER-ROOT coverage floors (20/5 mdBook, 25/1 root — one shared floor would let a collapse in either hide behind the other's count) so a broken path fails loudly instead of checking nothing. DELIBERATELY in `ci`, not the `docs` CI job — that job is Nix + `mdbook build` with no Rust toolchain (~2 min) and the standing docs-job deferral protects exactly that. SCOPE: `mdbook/src` RECURSIVELY plus repo-root `.md` FLAT — the root walk must never descend, or it reaches the private `book/` manuscript and the generated `mdbook/book/`. The boundary is COMPILABLE EXAMPLE vs. METASYNTAX, carried by the info string, NOT tutorial vs. spec: the root specs were out of scope at first on the "red by construction" theory, but the failures were exactly two categories and both were MISLABELS — §5 notation (`pred(term, term, …)`) and §14's `pred` declarations, an explicit v2 feature that is a compile error today. Both now sit in ```text fences; every remaining spec fence is checked like any other (it caught `barks`, not a corpus name, in §6's binder-block example).
`just verify-grammar-parity`	Shipped-artifact parity (docs Phase 5): `grammars/nibli.tmLanguage.json`'s keyword alternation must equal `nibli_lexicon::RESERVED_WORDS` — set, ORDER (so the two files diff side by side), and the `\b` anchors (unanchored, an editor paints the `we` inside `wealth`). `grammars/README.md` always stated the invariant in prose and the pest twin was pinned inside nibli-kr, but the TextMate copy — a tracked, public artifact — was pinned by nothing, and NO recipe, CI job or test referenced `grammars/` at all. `include_str!` rather than a runtime read, so a moved or renamed grammar is a COMPILE error, never a silently-skipped gate; dependency-free extraction with each structural assumption its own assert.
`just release-prep X.Y.Z [DATE]`	Roll the tree to a new version (R3): section-scoped bump of `[workspace.package]` + every `[workspace.dependencies]` entry (edit count DERIVED from the parsed manifest, never hardcoded; line-scoped rather than a tomllib round-trip, which would discard the root manifest's decision-encoding comments), CHANGELOG `[Unreleased]` → `## [X.Y.Z] - DATE` with both link refs rewritten (fence-aware parser — a `##` inside a KR snippet is not a heading), then `cargo update --workspace` (never bare `cargo update` — that re-resolves every third-party dep and makes the release diff unreviewable). Never commits or tags. Refuses rather than faking idempotency: bad semver, non-increasing version, dirty tree, tag already local/remote, existing `## [X.Y.Z]` section, empty `[Unreleased]` (override `NIBLI_RELEASE_ALLOW_EMPTY=1`); a non-`main` branch WARNS only, because the hotfix path branches from the tag. Ends by calling `release-verify` as the last body statement — as a `just` dependency it would run BEFORE the body and verify the pre-bump tree.
`just release-verify X.Y.Z`	The release-moment gate (`release-check` + version-specific legs): workspace version, CHANGELOG section present/first-after-Unreleased/non-empty/dated, both link refs, every `Cargo.lock` member entry, `cargo metadata --locked`, and — only when `GITHUB_REF_TYPE == tag` — that the tag equals `vX.Y.Z` (gating on `GITHUB_REF_NAME` being non-empty instead would compare `main` and fail every branch push). Cargo-free enough for the release workflow's preflight. Never in `ci`: its answer is deliberately false on an ordinary commit.
`just release-publish X.Y.Z [dry]`	crates.io publish, safe to re-run. `cargo publish --workspace` hard-errors on an already-published version (`verify_unpublished` bails before uploading anything, so it is NOT a resume path); this probes the sparse index, then either exits 0 (all live), publishes `--workspace`, or resumes with `--exclude` per already-live crate — keeping cargo's own dependency ordering and index-propagation waits instead of re-implementing them in a per-crate loop. Bounded retry (90 s, re-probing each attempt) because cargo's per-wave index wait is a fixed, unstable-gated 60 s. A `dry` second arg SKIPS the preflight and always runs `--dry-run`, so a rehearsal at an already-published version still verify-BUILDS all 13 tarballs. Warns when a crate is absent from the index at every version (the crates.io NEW-crate bucket is burst-5-then-1/10min — publish new crates manually once first).
`just release-bins` / `release-dist V SLUG` / `release-wasm V` / `release-notes V`	Release artifacts. `release-bins` is `cargo build --release --locked -p nibli-host -p nibli` — never `--workspace` (links the cdylib component crates; WIT `@` export symbols break the linker) and never `--features bench-bins`. `release-dist` tars inside the matrix job because `actions/upload-artifact` does not preserve the executable bit. `release-wasm` needs cargo-component so it runs in the DEFAULT devshell, and owns the `nibli.wasm` → `nibli-pipeline-V.wasm` rename (the lib target is named `nibli`). `release-notes` extracts the CHANGELOG section + a generated asset table; the workflow passes it as `--notes-file`, never interpolated into a shell string.
`just clean`	`cargo clean`
`just fuzz-assert [SECS]`	Fuzz nibli-engine assert_text (full pipeline)
`just fuzz-query [SECS]`	Fuzz nibli-engine assert + query (stateful KB; split-half input: first half asserted, second half queried)
`just fuzz-nibli-kr [SECS]`	Fuzz the nibli KR front-end (parse → the single validating emit walk): any accepted input must compile through nibli-semantics WITHOUT a "corrupt AST buffer" rejection — a structurally invalid emitted buffer is a nibli-kr bug, surfaced as an oracle panic; the same oracle covers `parse_text`'s per-statement recovery buffer (rollback integrity) (plus the usual crash/leak detection)
`just fuzz-seed`	Seed `fuzz/corpus/` for the three targets from the shipped `.nibli` corpora + `nibli-kr/tests/acceptance.nibli`
`just fuzz-ci [SECS]`	Unattended fuzz gate: `fuzz-seed` + all three targets × SECS (default 120) each; non-zero on crash/OOM/leak. Runs as a parallel `fuzz` job in the GitHub workflow.
`just mutants [JOBS]`	Mutation-testing gate over the soundness paths (scope + per-mutant test set in `.cargo/mutants.toml`: nibli-reason/nibli-semantics/nibli-engine/nibli-kr suites per mutant — nibli-kr carries the shape_tests kill power). The recipe caps each process at 12 GiB virtual (`ulimit -v`) so a runaway-allocation mutant dies alone as a CATCH instead of OOMing the box; JOBS defaults to 3 (provably within the WSL cap), raise it with more RAM. Diffs survivors against `mutants-baseline.txt` (line:col-stripped): fails on any NEW survivor, prompts a shrink for killed ones. On-demand (~2.5 h full sweep at -j3), not in the per-push gate. Baseline (re-cut 2026-07-19) + stats in GUARANTEES.md; between re-cuts, verify soundness-path changes with `cargo mutants --in-diff`.

Important:

Always use cargo test --lib (NOT cargo test) — cdylib linker chokes on WIT export symbols containing @
- Exception: nibli-host is a normal bin (no cdylib/WIT export), so cargo test -p nibli-host (the test-host recipe, gated by ci) links fine; the @ issue only affects nibli-pipeline/the component crates.
ci is the fast native gate (no WASM build). The WASM component + nibli-host fuel/memory/trap-recovery behavior is gated by ci-wasm (the six smokes); run ci-all (= ci + ci-wasm) as the comprehensive pre-push gate.
Regenerate WIT bindings: cargo component build (bindings appear in each crate's src/bindings.rs)
- Note: full build fails on io-extras crate (#![feature] on stable). Bindings still generate successfully before the failure.
REPL uses reedline — does not work with piped stdin
The --lib unit sweep runs PARALLEL since 2026-07-18 — the old --test-threads=1 constraint is gone (the thread-local compute dispatch + predicate cache became per-KnowledgeBase instance fields, kb.rs). The integration/gate recipes (test-engine, known-failures, the nibli-verify gates) keep --test-threads=1 for their own reasons (fixed redb paths, oracle runs).

Lucy conversation memory

When the user wakes or addresses Lucy, load lucy-plugin/skills/lucy/SKILL.md and the wake skill. The checkout's CLI is target/debug/lucy (build with cargo build -p lucy-cli in the Nix shell if needed).

In a Lucy session, preserve complete user messages and assistant replies, including progress updates, with lucy record --json or lucy record --stdin. Keep the original text and source; summaries are additional records. Save interpreted facts and decisions with lucy claim --from MESSAGE_ID, so their contents remain attributed rather than becoming bare facts. The conversation KB is lucy/interactions.nibli; private conversations and their extractions stay in lucy/private-interactions.nibli. lucy transcript reads the complete records. Use lucy ask --conversations "<KR>" for conversation queries; it explicitly excludes the constitution and direct facts, avoiding the known slowdown of the combined KB as its domain grows. Older Markdown journals are imported as legacy entries, without inventing their missing verbatim messages. Hosted agents submit replies through the CLI; the prompt hook alone cannot capture assistant output.

Dictionary Data — the committed English corpus

Since the committed-corpus milestone (2026-07-17) the dictionary IS Rust source: nibli-lexicon/src/corpus/predicates.rs (a four-figure set of PredicateEntry rows, sorted, binary- searched) + src/corpus/compounds.rs (curated CompoundEntry seeds). There is exactly ONE build mode — no build.rs, no phf, no dictionary-en.json at build time, no FULL/FALLBACK split; local, CI, and deployed builds are identical and need no network.

Strongly typed: arity = places.len() and every place is NAMED in English (structural — an unnamed place is unrepresentable). Swap { with, base } types the converted→canonical link; CompoundEntry.relation is const-checked = name with +→_. A const _: () = validate_predicates(...) guard re-checks sorted/unique/ident/reserved/label/swap invariants on every compile (hand edits included), with #[test] twins that re-run the same logic with offender lists.
Refinement model: edit the committed file in place. Machine-guessed place names carry a greppable // TODO(corpus): guessed places … comment; a count ratchet (TODO_BASELINE in predicates.rs) forces conscious adjustment as rows are refined.
English-only input: gismu spellings never resolve (klama(…) is a compile error); the source gismu survives as provenance metadata via by_provenance(gismu) — the permanent bridge the Predilex gates and lexigen key through. Compounds (a+b) resolve only via committed CompoundEntries and emit their relation ident (computer_user); uncurated compounds fail closed (NIBLI_KR §5).
Regeneration: tools/lexigen (workspace bin, NEVER a build-dep) reads dictionary-en.json — the lensisku English bulk export, gitignored, fetched with just fetch-dict (public dump, no login) — and prints a drift report + new-entry candidates to scratch files (just regen-lexicon). It never rewrites existing entries, so refinements cannot be clobbered. The JSON is ONLY lexigen's input; the book's verify_book.py VOCAB check still reads it, skipping cleanly when absent.

Compute Backend

The nibli-host (runner) acts as a TCP client to an external compute backend server via JSON Lines protocol.

Env var: NIBLI_COMPUTE_ADDR=host:port — configures the backend address at startup
REPL command: :backend [host:port] — show or change backend address at runtime
Protocol: One JSON object per line, keyed on the ENGLISH relation name (the IR is Lojban-free since the predicate-name flip). Request: {"relation":"exponential","args":[{"type":"number","value":8.0},...]}. Response: {"result":true} or {"error":"..."}.
Fallback: Valid numeric product/sum/quotient calls are handled locally first. If their operands are not locally evaluable, the registered canonical corpus relation follows the same external-dispatch path as other registered corpus predicates. If that backend is unconfigured or errors, the query returns UNKNOWN (backend-unavailable).
- Tolerant equality (disclosed): product/sum/quotient compare the result with isclose (rel_tol 1e-9, abs_tol 0) — a deliberate float approximation so 0.3 = 0.1 + 0.2 is TRUE — in the single shared evaluator nibli-types/src/arithmetic.rs (nibli-reason guest + nibli-host host + nibli_backend.py all mirror it). The exact-equality predicate num_equal is EXACT == (nibli-reason/src/compute.rs). README's "Compute Backend" discloses this to users.
Lazy connection: TCP connects on first external dispatch, auto-reconnects on failure.
Proof-local compute (disclosed): built-in and external results decide only the current ComputeCheck; they are never inserted into fact_store/FactRecord, receive no id, do not appear in :facts, cannot be retracted, never change the domain, are not persisted/replayed, and trigger no forward chaining. Executable compute is query-only: assertion ingress rejects it in facts and every rule position before id allocation, except inside opaque quoted abstractions; the reference external names (exponential/logarithm) are rejected there registered or not. Text registration is post-compile routing over the committed corpus, not a vocabulary declaration: surface aliases/compounds normalize to their canonical IR relation, an unknown name is refused without guessing arity, and a live fact/rule referencing the canonical relation blocks registration (ids named), so registration order cannot strand a stored fact. Arbitrary compute names require an explicit raw ComputeNode through the native KnowledgeBase query API (or a future schema extension); the shipping component has no raw-buffer query export, so implementing its backend import alone cannot add a text name. Each top-level query recomputes or redispatches, with the same proof-local lifecycle for corpus KR and native raw IR; repeated identical external checks may share only a transient within-query memo so a trace cannot contradict its verdict. A backend error is uniformly UNKNOWN (backend-unavailable), even after an earlier query succeeded or despite a matching ordinary fact. A successful backend reply remains trusted evidence, so the backend is part of the TCB for that proof step. README's "What zero-hallucination means here" + "Compute Backend" and GUARANTEES §Compute Result Lifecycle disclose the contract.
External compute admission (decision 2026-08-05): the stock nibli-host / NibliEngine::enable_compute_backend path deliberately remains low-assurance plaintext, unauthenticated JSONL/TCP. This does not apply to in-process built-in arithmetic. The wire has no peer identity, confidentiality, integrity or request binding, version, freshness/replay, expiry/revocation, or audit receipt; any parseable Boolean received in stream order is trusted. Valid forged/stale/reordered replies are therefore not detectable. The stock CLI's address setting is routing, not policy. Native embedders may replace both callbacks with set_compute_dispatch, and component hosts may implement the WIT compute-backend import, but rejection collapses to UNKNOWN (backend-unavailable) and current proofs cannot carry policy metadata. Stock retries mean external handlers must be pure/idempotent. nibli-auth is unrelated to this transport.
Reference server: python/nibli_backend.py — handles product, sum, quotient, exponential, logarithm (all keyed on the canonical English relation name). Extend HANDLERS for additional corpus relations, or for arbitrary names reached by a native raw-IR caller; adding a handler alone does not extend KR vocabulary.

Architecture

Core component crates + runtime surfaces:

Crate	Name origin	Role	Key files
`nibli-semantics`	—	Flat AST buffer -> FOL logic IR -> flat WIT logic buffer; rejects a proposition carrying both temporal and deontic fields before IR emission	`semantic.rs`, `ir.rs`, `lib.rs` (flattener)
`nibli-reason`	—	FOL logic buffer -> backward-chaining assert/query, with QUERY-CONE-SCOPED STRATUM-ORDERED MATERIALISATION (`materialize.rs`): before backward chaining, only query-reachable cones that need NAF completeness are saturated bottom-up; purely positive roots stay lazy unless exact reasoning remains non-definitive, a depth-cut exact single-positive rule antecedent extends the same cumulative root union, and find/count still request complete positive roots. Unrelated eligible relations are never global startup work. Within a requested cone, both a NAF check and a positive `∃ev` goal become set-membership tests instead of proof attempts (the positive probe short-circuits `check_formula_holds_core`'s `ExistsNode` arm before candidate enumeration; PROOF-TRACED queries keep backward chaining — `positive_lookup` is lowered for their duration — because a lookup has no derivation and the trace contract assumes one). Unbound rule events are joined left-deep under accumulated role bindings; cheap grounded-index selectivity chooses the next event before its complete relation-scoped candidate set is generated. Rule-head Skolems retain grounded sibling dependencies and enumerate only unresolved dependencies; the global domain × registry pool remains the fallback only when no sound anchor exists. Needs the `∃ev` REGROUPING first — every `∀`-rule head carries a dependent Skolem for its event var, so the raw program is not function-free; `∃ev. rel(ev) ∧ rel_x1(ev,a1) ∧ …` projects to `rel(a1,…,aN)` (the same move `nibli-verify/src/asp.rs` makes for clingo, deliberately REIMPLEMENTED so the oracle stays independent of what it checks). Fail-closed: tense/deontic flavours, `du` equivalence classes, compute conditions, non-projectable `~` groups and non-range-restricted rules are all REFUSED and keep the ordinary path. `set_materialization` / `materialization_report`, cumulative over requested query cones until mutation and reaching every surface since the 0.7.0 WIT bump (`:materialize [on	off]`in nibli-host prints the report and toggles);`NIBLI_MATERIALIZE=0 `opts out at startup. ABSTRACTION referents (`entitled(every person, event { P() })`) project to the complete versioned` _abs_v1_ `marker RELATION NAME as an opaque constant — the tagged, length-delimited, alpha-canonical kind+body key is identity; the digest is recomputed from the key at assert/query ingress and is non-semantic, while malformed/unknown versions fail closed — admitted only while the referent fills at most one role slot; the typing relations (`event`,` _abs*`) are then explicitly REFUSED, never omitted, or` is_edb`would call them EDB and complete them over an empty extension. Safe because the abstraction body's event term is`sk_2(Unspecified)`, independent of the universal, so the body projects to a tuple about nobody and an entitlement cannot fabricate its actuality. A relation is completed only if every relation its rules read is ALSO complete — the eligibility closure covers unprojectable RULES, but a relation can become unusable later when` seed_edb`refuses its stored FACTS (a`past` fact, a role gap, an arity clash), and completing over that hole made a negated condition pass vacuously (a definitive wrong TRUE, caught by the ON/OFF differential)
`nibli-pipeline`	—	Glue: chains nibli-kr -> nibli-semantics -> nibli-reason as the ONE WASM component. KR-only since THE DROP; since the CoreSession extraction (2026-07-18) the session wraps `nibli_session::CoreSession` — WIT term/error conversion at the boundary only; interactive text inputs emit the §12 lint notes as verbose-gated `[Note: …]` guest-stdout echoes (the `[Skolem]` precedent — `NIBLI_QUIET=1` suppresses; the replay path never lints; the env reads live HERE, not in the core)	`lib.rs`
`nibli-host`	—	Native Wasmtime host, REPL, external compute backend TCP client. KR-only since THE DROP (`:load`/`--script` load any file as KR text)	`main.rs`
`nibli-engine`	—	Native in-process embedding of the pipeline (used by tests + the store layer; no Wasmtime). Wraps `nibli_session::CoreSession` (the sole text→AST seam) + the durable-store write-through (ids minted by the store; buffer replay is text-free)	`lib.rs`
`nibli-auth`	—	Built-in authorization: warm `Authorizer` over `nibli-session`, builtin `policy/auth-0.1.0.nibli`, decision cache, ephemeral context KR; API `can` / `allowed_fields` / `explain` (KR head `authorized`, not corpus `can`); `tls` for !Send multi-thread; optional features `axum` / `async-graphql` / `juniper`; demo `examples/auth-axum`	`lib.rs`, `tls.rs`, `policy/`
`nibli-auth-py`	—	PyO3 cdylib `nibli_auth_native` (maturin); pure Python package `python/nibli_auth` + FastAPI/DRF/… helpers; demo `examples/auth-fastapi`	`nibli-auth-py/`, `python/nibli_auth/`
`nibli-session`	—	The SHARED session core (2026-07-18): `CoreSession` = the ONE compile chain (`nibli_kr::parse_checked` → nibli-semantics → compute-marking) + compute-predicate registry + assert/query verbs that nibli-engine, nibli-pipeline, nibli-wasm, nibli-ui, and nibli-verify's `kompile` all wrap with only boundary conversion — native↔WASM agreement BY CONSTRUCTION (the old hand-mirrored `compile_text`/`compile_pipeline` copies are gone). Deliberately excludes linting, env reads, persistence, and dispatch wiring (per-surface boundary policy); free `compile_unmarked`/`compile_text` fns serve pre-mark/per-call-set consumers. Deps: nibli-kr + nibli-semantics + nibli-reason only (wasm-safe on every target)	`lib.rs`
`nibli-ui`	—	Standalone Dioxus web UI (browser, port 8080) — nibli-kr/nibli-semantics/nibli-reason compiled in, reasons fully in-browser; KR-only since THE DROP (preloaded examples and the Custom buffers all compile through nibli-kr). Optional client-side BYO-key LLM Formalize (Source→KB; "compile" stays reserved for the deterministic step): the agentic self-correcting loop (`nibli-formalize`) → the nibli-kr+nibli-semantics+round-trip gates (`GATE_ORDER` chips) → fresh-context semantic verification → feed errors back → retry, with a self-correction trace. The LLM client is single-sourced on `nibli_formalize::llm`; nibli-ui holds a thin `Settings { llm, max_attempts }` wrapper. Lint notes (§12 L1–L9) ride `nibli_protocol::LineResult::notes` (fresh `Linter` per query run — the stateless-KB model) and render as `[Note: …]` rows in the KB status bar. Native test: the `shipped_examples_compile` guard (`just test-ui`)	`main.rs`, `examples.rs`
`nibli-formalize`	translate (name predates THE DROP)	Agentic English→KR formalizer engine consumed by nibli-ui: a multi-turn LLM client (5 providers) with a `Chat` seam + wasm `HttpChat` transport; the local gates (`gates.rs`): `nibli_kr::parse_checked` + nibli-semantics + the render round-trip gate (`GateError::RoundTrip`: the candidate's canonical `nibli_kr::render` re-spelling must re-compile to the SAME `LogicBuffer` — nibli-kr's fixpoint contract as a per-candidate drift-catcher; native + wasm); the grammar+dictionary-grounded system prompt (`llm/system_prompt.rs`, assembled ONCE via `LazyLock` since the corpus is compile-time): the pest `nibli_kr::GRAMMAR` (in-sync by construction) + a distilled §4/§6/§7 semantics block + the FULL committed corpus as `- name(places…) — gloss` lines (no gismu — they no longer resolve) + the compound-entry section + the few-shots — pinned by two guards (the few-shots stay gate-valid; the assembled prompt embeds the grammar + ≥1,300 entry lines + the compound section); the `translate_agentic` loop (line-by-line KB validation, attempt cap, oscillation guard), and the semantic verification turn (`verify.rs`, int19h feedback): after the gates pass, a FRESH-context judge reads the overlay-free `nibli_render` back-translation of each KB line; MISMATCH retries as `GateError::Verification` — best-effort advisory. All logic native-tested (incl. the KR Genesis fixture); only the browser transport is wasm-only	`agent.rs`, `gates.rs`, `llm/`
`nibli-wasm`	—	wasm-bindgen wrapper exposing the in-browser pipeline (powers the live demo). KR-only since THE DROP; `set_language(&str)` and `back_translate` survive as DEPRECATED NO-OP echo shims (deployed-site JS compatibility — die at the site-migration milestone). Native tests load the `.nibli` corpora — every line must compile (single-mode since the committed corpus)	`lib.rs`
`nibli`	—	Native debug REPL, `nibli-validate`, and `nibli-pin` (the `verify-pins` KB-behavioural pin runner; harness self-tests live in the bin) tooling (KR-only since THE DROP; `--lang`/`NIBLI_LANG` retired — `verify-book` is expected red until the book migrates or pins `v0.1-lojban-final`)	`main.rs`, `src/bin/validate.rs`
`nibli-types`	—	Shared flat types used by every stage: `LogicBuffer`/`LogicNode` (the WIT-BOUNDARY types — the only data crossing the WASM component seam), `AstBuffer` (the INTERNAL nibli-kr→nibli-semantics interchange + render's input + the `validate_ast_buffer`-gated programmatic-build target — never crosses WASM; arguments are TYPED since the 2026-07-18 split — `Argument::Variable` (sigiled `$name`, validate-enforced) / `Marker` (`it`/`slot`/`?`) / `Pronoun` (14 variants, `as_str()` the single spelling authority) — no string-sniffed catch-all, §10 pro-arguments unrepresentable by construction), `NibliError`, and the single shared arithmetic evaluator (tolerant equality). The `LogicBuffer` IR is publicly specified in repo-root `LOGIC_IR.md` — keep that spec in sync when the IR or its emitted-shape invariants change	`ast.rs`, `logic.rs`, `error.rs`, `arithmetic.rs`
`nibli-lexicon`	—	The COMMITTED English corpus (see Dictionary Data below): `src/corpus/predicates.rs` (a four-figure set of sorted `PredicateEntry` rows — English name, `source_gismu` provenance, optional `Swap{with,base}`, NAMED places where `arity = places.len()`, gloss, template, tier) + `src/corpus/compounds.rs` (curated `CompoundEntry` seeds: `a+b` spelling → relation ident + committed places). No build.rs, no deps, ONE build mode; a compile-time `const _: ()` guard + `#[test]` twins enforce sorted/unique/ident/reserved/label/swap/compound invariants fail-closed. Functions-only API: `alias`/`compound`/`compound_by_relation`/`relation_places`/`get_arity`/`get_gloss`/`get_template`/`by_provenance`/`canonical_alias`; `src/reserved.rs` single-sources the nibli KR keyword list. Regenerated (report-only) by `tools/lexigen`	`src/corpus.rs`, `src/corpus/predicates.rs`, `src/corpus/compounds.rs`, `lib.rs`, `src/reserved.rs`
`nibli-kr`	—	The nibli KR surface-syntax front-end — the ONLY front-end since THE DROP; the v0.1 compat profile of `NIBLI_KR.md` is fully implemented, lint catalog included (`TODO.md` carries the rest of the nibli-KR program). Parses the predicate-call language (`goes(me, destination: some market).`) into the `AstBuffer` nibli-semantics consumes. Parser tech = pest: `src/nibli_kr.pest` is the EXECUTABLE grammar (normative NIBLI_KR §15 — grammar↔parser drift impossible by construction; keyword rules self-guarded and pinned against nibli-lexicon's reserved list by a conformance test). The FULL v0.1 grammar surface; the walker owns the §6/§7 errata as targeted positioned errors. `src/emit.rs` is THE SINGLE VALIDATING WALK (single-resolution merge 2026-07-17 — each word resolves exactly once, at the site that emits it): all the dictionary-driven fail-closed checks (name resolution — corpus name or committed `a+b` compound entry, else COMPILE ERROR (gismu never resolve); place checks, linked-args rules, `it`/`slot` position rules, Name↔pronoun collisions; error precedence pinned) + the lowering to the `AstBuffer` (entries→their ENGLISH canonical base name with `Converted` swaps, compounds→their relation ident as a plain Root, `$vars` preserved verbatim as the logic-variable sigil — no da/de/di pool, no 3-var cap, operators at sentence level; ALL block determiners lower since 2026-07-17: `exactly N [the]`/`every the` via `Sentence::Quantified` (seam-pinned equal to the term twins), `the X $v:` by let-binding substitution, block rel-clauses fold domain/matrix-side). `src/resolve.rs` is the lookup module both emit and lint share (`lookup`/`lookup_compound`/`label_index`). Public `nibli_kr::parse_checked` is the engine's sole text→AST seam; `parse_text` is the per-statement recovery variant (emit-with-rollback: a failing statement's partial nodes truncate back out, fuzz-oracled). `src/render.rs` is the inverse (AstBuffer→nibli KR; PARITY LAYER 1: zero wildcard arms + `__ast_parity_guard`, so a new AST variant breaks the build; §10 pro-arguments have NO AST form since the typed argument split — what stays representable-but-unspellable (pronoun-colliding Names, non-finite numbers) fails closed BY NAME; compound relations render back as their `a+b` spelling; rel-clause bodies with an implicit bound entity render with an injected `it` + place-sorted positional args); `tests/acceptance.nibli` (honest-generic §16) is pinned by render∘parse fixpoint tests. `src/lint.rs` is the §12 LINT CATALOG (L1–L9): a data-returning pass (`nibli_kr::lint::Linter`, stateful per session; `reset()` rides KB resets) — non-blocking `[Note: …]` compile notes; `parse_checked` stays note-free, surfaces opt in. `src/shape_tests/` is the KR-text-level shape regression suite (migrated 2026-07-18 from nibli-semantics per the flat-vs-surface discipline — asserts on the compiled `LogicBuffer` via seam-style structural helpers; dev-deps nibli-semantics)	`src/nibli_kr.pest`, `src/parser.rs`, `src/resolve.rs`, `src/emit.rs`, `src/render.rs`, `src/lint.rs`, `src/ast.rs`, `src/shape_tests/`
`nibli-protocol`	—	Shared wire-format proof-trace types: nibli-engine (native) serializes, nibli-ui/nibli-wasm (browser) deserialize	`lib.rs`
`nibli-store`	—	Persistent redb stores: `NibliStore` (durable fact registry — provenance, retraction tombstones, `:export`; schema v3 — `open` accepts v2 as migratable and `migrate_v2_text_rows` recompiles any legacy `StoredAssertion::Text` rows to `Buffer` fail-closed, `finalize_v3` restamps engine DBs) and `RedbFactStore` (the KB's typed write-through mirror, schema-versioned, fail-closed decode)	`lib.rs`, `typed_store.rs`
`nibli-render`	—	Shared English rendering of proofs/verdicts (the collapsed `[Why]` narrative; `DomainGloss` overlays are curated-UI-example-only — overlay→dictionary→generic fallback, never CLI/book)	`lib.rs`, `corpus_overlay.rs`
`nibli-import`	—	RDF Turtle / OWL import + fact export, wired as the `nibli-import` CLI (`just import <file.ttl>`; `--raw/--export/--query` flags — KR queries reach only dictionary/alias-resolvable names, fail-closed)	`lib.rs`, `rdf.rs`, `owl.rs`
`nibli-verify`	—	Differential SOUNDNESS gate (Track A), two oracles over KR-generated programs: exports the nibli-semantics FOL IR (`LogicBuffer`) and checks nibli's verdict against (1) Vampire over the Horn/NAF-free fragment (TPTP), and (2) clingo over the stratified-NAF + closed-world fragment (ASP — the translator regroups the event decomposition back to function-free surface Datalog). Plus (3) the KR→nibli-semantics seam gate (`nibli_kr_seam.rs` + `tests/nibli_kr_seam_gate.rs`, `just verify-nibli-kr-seam`) — the front-end oracle: hand-verified FOL structural goldens + the CONSTRUCT_INVENTORY acceptance sweep + KR-internal metamorphic relations (3 seeded families) + the determinism native leg. Plus (4) the corpus differential (`tests/alias_differential.rs`, `just verify-alias-map`) — the SHIPPED committed corpus's invariants (shape/provenance/swap/compound integrity, coverage floors, per-entry behavioral twins; single-mode) — arity agreement holds by construction (one committed table). Plus (5) the Predilex dictionary-arity differential (`predilex.rs`, `just verify-dict`). Plus (6) the stratification-rejection, (7) retraction metamorphic, and (8) materialisation metamorphic differentials (`strat_diff.rs`/`retract_diff.rs`/`materialize_diff.rs` — the last is saturated ≡ backward-chained, the gate standing between the NAF materialisation and its one unsound failure mode: an under-derived extension makes a missing tuple read as "not derivable", flipping a NAF FALSE to a definitive wrong TRUE). Not a runtime surface — a CI gate	`lib.rs`, `tptp.rs`, `asp.rs`, `filter.rs`, `oracle.rs`, `oracle_asp.rs`, `seam.rs` (buffer probes), `nibli_kr_battery.rs`, `nibli_kr_seam.rs`, `strat_diff.rs`, `retract_diff.rs`, `materialize_diff.rs`, `tense.rs`, `corpus.rs`, `corpus_naf.rs`
`python/`	—	Reference compute backend server (TCP + JSON Lines)	`nibli_backend.py`

Flavor-stack boundary: a single formula path may carry one temporal or one deontic wrapper, never both. The KR walker rejects mixed prefixes in either order; AST compilation/rendering rejects dual-field propositions; nibli-reason rejects any second raw-IR wrapper before mutation, query/find, proof construction, materialisation, or replay. The IR/WIT retains each individual node variant, so this contract does not change the component ABI. Separate rule literals may still carry different flavors.
Current component compute contract (clarified 2026-08-13 without an ABI change): text registration routes a canonical committed-corpus relation after fail-closed compilation; it declares neither vocabulary nor arity. The shipping WIT has no raw-buffer query export, so a host backend cannot add a text name. Arbitrary compute names are reachable today only through a native caller-built raw ComputeNode, or after a future schema/raw-query extension.
WIT interfaces: wit/world.wit defines only the SHIPPING component's boundary: logic-types (FOL IR), error-types, compute-backend (host import), engine (session export), authorizer (built-in auth session — logical auth v0.1). Package nibli:engine@0.11.0 (0.11.0 made register-compute-predicate fallible — refused while live stored facts or rules reference the name, blocking ids in the message; the reference external compute names are additionally query-only at assertion ingress regardless of registration — and added the compute-predicates getter backing the bare :compute report; 0.10.0 adds assertion/rule citations to proof facts and a distinct presupposed proof case, so an eager rule conclusion cannot cross the component boundary as a user-given fact and duplicate sources remain separately citable; 0.9.0 added the generated-witness origin and changed forall proof payloads from bare terms to origin-bearing witness bindings; 0.8.0 made set-existential-import fallible, added existential-import-enabled, and carried witness-origin through find/exists proofs plus existential-imported through count proofs; 0.7.0 added set-materialization + materialization-report; 0.6.0 added export authorizer wrapping native nibli-auth; 0.5.0 removed legacy assert-text-with-id with store schema-v3; earlier history: 0.2.0 set-language, 0.3.0 named-field proof-rule, 0.4.0 set-existential-import). cargo component build -p nibli-pipeline regenerates nibli-pipeline/src/bindings.rs (the ONLY crate with WIT bindings; nibli-kr/nibli-semantics/nibli-reason are plain Rust libs using nibli-types directly). The boundary types ARE nibli_types: [package.metadata.component.bindings] with remaps logic-types/error-types's ABI-matching types (everything except proof-rule/proof-step/proof-trace) onto the canonical enums, so nibli-pipeline carries only the one convert_proof_rule bridge, not a full mirror-conversion layer. The remap keys pin the interface version (nibli:engine/logic-types@0.11.0/…) — bump them with any WIT version change (all eleven, or bindings generation silently stops remapping onto nibli_types). Auth WIT methods use parameter name object (not resource — reserved WIT keyword) for the protected resource id.
WIT worlds: nibli-pipeline is the SOLE world — a single WASM component importing compute-backend, exporting nibli-pipeline, with nibli-kr/nibli-semantics/nibli-reason linked as internal Rust crate deps. (The legacy per-stage nibli-kr-component/nibli-semantics-component/nibli-reason-component worlds + nibli-kr/nibli-semantics/nibli-reason/ast-types interfaces were removed — they were never built and misled contributors into thinking a per-component architecture existed.)
Rust structs: NibliPipeline (the WASM component) is the only WIT-binding struct.
Boundary data: Flat index-based arrays (LogicBuffer for :debug/proof output, LogicalTerm args) with u32 indices cross the SINGLE host↔nibli-pipeline WASM boundary — no heap pointers. The internal nibli-kr→nibli-semantics→nibli-reason stages are Rust function calls (no WASM boundary), using nibli-types flat buffers directly.
Compute dispatch: nibli-reason uses injectable function pointers (nibli_reason::KnowledgeBase::set_compute_dispatch) instead of cfg-gated WIT imports. Lasna registers host-bridge functions at Session creation; native nibli-engine can opt in via enable_compute_backend, while nibli-ui/nibli-wasm leave external dispatch unwired. Valid numeric product/sum/quotient calls resolve locally first; any registered corpus call that cannot be evaluated locally requires external dispatch and yields UNKNOWN (backend-unavailable) when no backend works. A native explicit raw ComputeNode reaches the same dispatcher without text registration.

Canonical Runtime Surfaces

Use these assumptions when selecting entrypoints:

nibli-host is the canonical local/operator runtime for the theorem prover. It is the main single-node REPL and the default way to exercise the WASM-hosted pipeline. KR-only since THE DROP (the book capture harness must pin the v0.1-lojban-final tag until the book migrates).
- Strict mode: NIBLI_STRICT=1 (or :strict on|off at runtime) makes arity mismatches and integrity-constraint violations REJECT the offending fact and fail the assertion atomically, instead of the default permissive warn-and-insert (GUARANTEES §Predicate Validation / §Integrity Constraints). Plumbing pinned by the smoke-host-strict gate (in ci-wasm); rejection behavior pinned at the nibli-reason level.
- Existential-import mode: existential import is DEFAULT OFF (clean-core is the default): a description universal (animal(every dog).) mints no entity, so some is plain classical ∃. NIBLI_EXISTENTIAL_IMPORT=1 (or :existential-import on) explicitly enables the legacy xorlo profile. Its witness participates consistently in ∃/∀/find/exact-count/count_witnesses/aggregate; WitnessBinding and ExistsWitness carry WitnessOrigin, while CountResult.existential_imported discloses its share. The fallible setter transactionally rebuilds the live assertion registry and rolls back on replay failure; the getter reports the effective profile. Threaded KnowledgeBase→CoreSession→nibli-engine/nibli-wasm and through WIT 0.9.0→nibli-pipeline→nibli-host; host startup/toggles and the UI report the profile. Pinned by existential_import_profiles_are_algebraically_coherent_and_retractable, existential_import_profile_switch_rebuilds_loaded_rules_immediately, the reasoner provenance tests, wasm/UI profile tests, and smoke-host-existential-import in ci-wasm. The Vampire/clingo differentials remain clean-core; the import algebra has its own metamorphic battery.
- Exact counts are query-only in asserted position: exactly N and no compile to CountNode for query/proof evaluation over the current domain. Every assertion, assumption, and preassigned/replay ingress rejects that use before id/state mutation; there is no persistent cardinality-constraint assertion and exactly 0 is not a prohibition. Opaque abstraction bodies remain quoted content. Legacy persisted count rows fail replay without deletion. Formalize's KB gate rejects outer-KB counts while its compiler/round-trip gate still accepts the query IR.
- Quiet mode: NIBLI_QUIET=1 suppresses the per-assertion bookkeeping echoes — [Fact #N] … (host) plus [Skolem]/[Rule]/[Constraint] (guest; nibli-host forwards the flag into the component's WASI env, since nibli-pipeline::Session::new reads it to decide kb.set_verbose). The verdict, [Why], proof trace, [Find], [Note: …] (the §12 lint catalog — quiet-INDEPENDENT, a different producer), [Retract], and :facts output are unaffected. Opt-in — a live just run REPL stays verbose. The book's capture harness (book/tools/capture_book.py) sets it by default for clean transcripts; the smoke-host-quiet gate (in ci-wasm) pins both directions. (The short-lived [Domain] numeric-quantifier-domain echo, 2026-08-01, retired same-day with the numbers-join-the-domain semantics decision — asserted numbers are now checked, not skipped-and-announced; GUARANTEES §Disclosed Sharp Edges.)
nibli-ui is the canonical browser frontend — a standalone Dioxus app with the engine (nibli-kr→nibli-semantics→nibli-reason) compiled into the WASM bundle, KR-only since THE DROP. It reasons fully in-browser; there is no server. The one optional network call is the Source→KB Formalize (renamed from Translate 2026-07-12 — the LLM step is interpretive formalization behind gates; NEVER label it "Compile") — the agentic self-correcting loop in nibli-formalize (LLM client single-sourced on nibli_formalize::llm): a bring-your-own-key request sent directly from the browser to a user-chosen LLM (Anthropic/OpenAI/OpenRouter/Gemini/Custom), with the key held in tab memory only. Hosting: the site is rebuilt by the external dhilipsiva.dev repo, pinged by .github/workflows/redeploy-site.yml on push to main. Since the committed corpus the site build needs NO dictionary fetch — the full vocabulary is compiled in from the repo's committed tables (build_nibli.sh's fetch step is obsolete; see DEPLOY.md); just build-ui produces a local release bundle. See DEPLOY.md.
- Query model (state, don't ask): a query is an entailment check of a proposition — you state eats(Adam). ("Adam eats") and the engine returns TRUE/FALSE/UNKNOWN. There is no interrogative form. The "?" affix shown in the UI query box is a decorative reading cue: not part of query_text, never sent to the engine. Keep UI/docs/book copy phrased as "state a claim," never "ask a question."
- Example dropdown: the header offers preloaded KBs (nibli-ui/src/examples.rs — book case studies Syllogism/GDPR/Drug-interactions; corpora include_str!-ed from repo-root *.nibli files the engine's regression tests pin; every KB line + preset query additionally pinned by just test-ui). Selecting one is read-only (Formalize disabled) and turns the query box into a preset-query dropdown that auto-runs; default Custom (example == None) is the editable mode. The example signal lives in App and is rendered conditionally — Custom buffers are never overwritten. Keep Syllogism/GDPR/Drug name strings byte-stable vs book quotes (Ch 18/19/20). The book legal case study is GDPR only—do not document a utopia/constitutional companion as a book chapter.
nibli-wasm is the wasm-bindgen wrapper exposing the same in-browser pipeline to JS (powers the live demo at dhilipsiva.dev/nibli).
nibli-engine is an internal native embedding library, not a user-facing runtime surface.
nibli is developer tooling: a native direct-crate REPL and the nibli-validate binary used for validation/data-generation workflows. It is not the canonical production runtime.

Code Conventions

Native contradiction gates use check_contradictions_report() and require both violations and unresolved to be empty (is_clean()). The older check_contradictions() exposes findings only and cannot prove scan completion. The report includes derived positive counterparts and integrity/disjunctive antecedents through the ordinary evaluator; it preserves generated witness identity internally and reports undecided or unsupported checks. This scans represented constraints, not unrestricted FOL consistency. Explicit negations preserve temporal/deontic flavor; opaque abstraction bodies remain quoted.

Semantic-compiler tests use compile_one(predicates, arguments, proposition) helper returning (IrForm, SemanticCompiler)
resolve(&compiler, &spur) helper to get string from interner in tests
The Connective enum (And/Or/Iff/Xor) is used only at the sentence level (SentenceConnective::Afterthought) — the argument/predicate connective variants were removed (dead capacity no emitter produced)
via modals carry the target predicate directly (ModalTag, a single-field newtype over the tagged predicate id) — there is no fixed modal-tag table
Test discipline — flat vs surface (nibli-reason): nibli-reason's flat make_* test helpers hand-build bare LogicBuffers and skip nibli-semantics's event decomposition + transform_compute_nodes, so they match the shipped pipeline on verdicts but NOT on shape-dependent behavior (cwa_false/naf_dependent flags, the ComputeCheck step, witness/Skolem shape). For anything shape-dependent, build the buffer the real way via compile_surface("<kr text>") (a nibli-reason test helper = nibli_kr::parse_checked → nibli_semantics::compile_from_ast → transform_compute_nodes), or use the make_decomposed_* helpers, or write a nibli-engine integration test — never assert those on a bare flat buffer. nibli-reason/src/tests/flat_vs_surface.rs is a metamorphic guard that keeps every behavior class' flat verdict == the surface verdict; keep it green. (See the header comment in nibli-reason/src/tests.rs — the tests-module ROOT, which since the 2026-07-18 split holds the shared harness + hoisted cross-section helpers and declares the ~20 topical submodules under src/tests/; nibli-semantics' test module is likewise split under src/semantic/tests/.) The same discipline drove the 2026-07-18 migration of nibli-semantics' KR-expressible shape tests to the surface: they now live in nibli-kr/src/shape_tests/ — driven through nibli_kr::parse_checked → nibli_semantics::compile_from_ast and asserted on the public LogicBuffer via structural helpers (modeled on nibli-verify/src/seam.rs), not the interner-keyed internal IrForm. What stays hand-built under nibli-semantics/src/semantic/tests/ is exactly the set with no KR surface: the corrupt-buffer negative controls + direct-injection API tests (lib.rs), the internal-static white-box units, and the defense-in-depth guards whose inputs the KR parser/emitter rejects or cannot spell first (over-arity/collision/overflow place tags, mandatory-it firewall, unknown-word arity, WithArgs-at-proposition, CLL place-counter, n-ary identity, arity-1 via).

Codebase Exclusions

When analyzing or searching the codebase:

Exclude generated docs HTML — mdbook/book/ (mdBook output). Hand-authored docs source is mdbook/src/ (see Docs Conventions below). Do not import the private manuscript at book/.
Exclude docs/ folder if present — legacy/generated path only; never put mdBook source there.
Exclude **/bindings.rs — auto-generated by cargo component build, not hand-written
proofs/ is Lean 4, not Rust — the mechanized soundness proofs (Track B; proofs/README.md). Each .lean mirrors a Rust component and is kept in lock-step with an exhaustive Rust conformance test. Checked by just verify-proofs.

Docs Conventions

The decisions of record for the mdBook site (inherited from the retired DOCS_TODO.md, 2026-08-03 — docs Phases 0–5 all landed; hosting recipes are DEPLOY.md, release policy is RELEASING.md, the remaining open items are TODO.md):

Source is mdbook/src/, never mdbook/book/ (generated) and never a docs/ dir.
Content law: code-derived only. Every claim re-derives from code, tests, recipes, corpora, or the root engine specs. Never the private Orange AVA manuscript at book/ — rights are reserved, and no book/ path may appear in a docs diff.
Epistemic rule: never present aspirations as shipped (the same rule GUARANTEES and README hold themselves to). A page describing unbuilt work is a defect, not a preview.
Fence tags are nibli / nibli-kr, aligned with the editor track. A ```nibli-kr fence is a PROMISE that its statements compile — just verify-doc-fences enforces it across mdbook/src and the root specs, so metasyntax and unimplemented-v2 syntax must use ```text.
Build targets: just docs for the primary host (site-url=/docs/nibli/), and just docs /nibli/ (= docs-pages-build) for the GitHub Pages mirror. The primary at dhilipsiva.dev/docs/nibli/ is NOT live until the site repo copies the build — until then the canonical public URL is the mirror, dhilipsiva.github.io/nibli/.
Docs PR gate: just docs (the CI docs job). That job is deliberately Nix + mdbook build with NO Rust toolchain (~2 min) — keep Rust-dependent doc gates in ci.
API docs are docs.rs, linked from mdbook/src/api-index.md; conceptual docs live only on the primary/mirror.

Known Issues

cargo component build fails on io-extras crate — pre-existing, unrelated to our changes. Bindings generate before the failure.
rustc ICE in check_mod_deathness — RESOLVED: the wasmtime::component::bindgen! compiler panic was fixed in rustc 1.94.0 (the flake's pinned toolchain); nibli-engine's #![allow(dead_code)] workaround was removed 2026-07-17 (zero dead code surfaced).

Roadmap

The soundness-by-proof frontier is complete (P1–P4 gaps cleared; P5 done): Track A ships two differential gates — Vampire (classical FOL, Horn/NAF-free) and clingo (ASP, stratified-NAF

closed-world, incl. the GDPR deontic-NAF erasure rule) — and Track B ships six mechanized Lean 4 proofs of the soundness-critical core (combiner, stratification criterion, SCC decomposition, unifier, rule firing, and the capstone trace ⇒ perfect-model theorem), each bridged to the engine by a conformance test (proofs/README.md; just verify-soundness + just verify-proofs). The nibli KR v0.1 program is complete (2026-07-12): the language shipped as the default front-end on every surface, lint catalog included. THE PIVOT (2026-07-12, second decision round — TODO.md is the tracker): Lojban is DROPPED entirely — THE DROP landed 2026-07-13 (single surface; nibli-kr + the agentic Lojban translator live on in the donation repo, github.com/dhilipsiva/fanva; the last dual-front-end engine is tagged v0.1-lojban-final). The nibli KR rename and the total Lojban naming purge (crates, WIT package, vocabulary — only the word nibli survives) have landed, and — with the predicate-name bullet — the canonical predicate + variable namespace has flipped from gismu to English, so proof traces and all user-facing output contain no Lojban: content, arithmetic/comparison, equals (the du identity), something (zo'e), $var names, the abstraction type names, the pronoun constants (me/you/this/it_a… — with a fail-closed guard rejecting a capitalized Name like Me that would co-refer with a pronoun), and the L4 lint (converted-alias + compound English notes, metabolized_by ↦ cuts⟨x1↔x2⟩ / computer+user ↦ computer_user(user, computer, purpose)) are all English. The committed English corpus landed 2026-07-17: the dictionary is Rust source (one build mode, no JSON at build time, gismu never resolve, compounds fail closed via committed entries). The mechanical identifier refactor also landed 2026-07-17 — the last Lojban identifiers, test names, codename comments, and corpus headers went English (deliberate residuals: the source_gismu/by_provenance provenance API, the gismu string fixtures in nibli-reason's flat tests, and explicit-history notes), clearing the book's timing gate 4(b) — the book migration is unblocked. The remaining ceiling is adoption — chiefly a reproducible non-expert authoring study (round-trip fidelity + silent-mistranslation rate), which belongs to the book/UX track.

Research paper

The systems paper and reproducible experiment sources live in paper/. Enter the paper environment with nix develop --extra-experimental-features nix-command --extra-experimental-features flakes .#paper. Use just paper-check, paper-smoke, paper-evaluate, paper-build, and paper-package; see paper/README.md for the frozen baseline and separate output paths for new runs. Preserve recorded observations. The large frozen schedule is stored in Git as schedule.json.gz; analysis also accepts the plain JSON emitted by collection.

Pre-commit Checklist

Before every commit, always:

Update AGENTS.md — if required
Update README.md — if language coverage or reasoning capabilities changed
Never hand-write test counts (or other derivable figures) into docs. If a figure is needed, derive it at writing time with just count-tests — stale hard-coded counts in GUARANTEES.md were an audit finding; prefer floor phrases ("a four-figure suite") that survive growth
Then commit all code + doc changes together

FilesExpand file tree

AGENTS.md

Latest commit

History

AGENTS.md

File metadata and controls

Nibli

Environment

Build & Test

Lucy conversation memory

Dictionary Data — the committed English corpus

Compute Backend

Architecture

Canonical Runtime Surfaces

Code Conventions

Codebase Exclusions

Docs Conventions

Known Issues

Roadmap

Research paper

Pre-commit Checklist