Issue #478: ADR-270 D24-D26: the logic layer as a package any package may ask, also at build time

Open and answer this issue on GitHub.

blocked · opened 2026-10-06 · updated 2026-10-06 · 1 comment

How it came up

While deciding the NULL rule for dsl … -> T (#477, ADR-299 D18), the question was how a really good driver finds out that a column cannot be NULL. For example:

WHERE (email IS NOT NULL OR age > 30) AND age <= 30

Here email is never NULL, but only via age > 30 ∧ age ≤ 30 ⇒ false. That is linear integer arithmetic with ∧ ∨ ¬, which nikaia-logic answers.

The encoding:

• one 0/1 variable n_c per nullable column;
• W(p) for “p is true” and F(p) for “p is false”, following SQL’s three-valued logic;
• the facts are W(where), and the goal is n_c = 0.

What was checked:

• ADR-270 D1 already decided that the logic layer and solvers are a Nikaia package that depends on nothing but std, so that another language or tool can feed it.
• Today it is the Rust crate crates/nikaia-logic, used only by prove.rs. A driver cannot reach it, and as a Rust crate it may not run at build time (ADR-321 D9).

Decision (owner)

The three points, in ADR-270 and Part III 14.2:

• D24 — The logic layer is a package any package may depend on, also while it is built (ADR-321 D2, D8, no exception). Public: terms, queries, answers, verify. Not public: solvers, representation, strategy.
• D25 — A build-time query is not an entry of nikaia.proofs. It gets the reference solver’s answer under a budget counted in work, the same on every machine. unknown proves nothing; in a driver, the column stays nullable.
• D26 — A package with its own version, not std::logic.

Still open:

• whether a grammar may call its package’s functions and Nikaia dependencies while it runs (ADR-321 §6), which a driver needs first;
• the package’s name in use.

To build

Prerequisite: ADR-270 D8 step 2, the reference solver in Nikaia.

1. Package boundary:
   • Mark the public surface: term building (Arena, Term, TermId), Query, the answer, verify.
   • Keep the solvers (FourierMotzkin, the later CDCL(T) core) private to the package.
2. Budget:
   • The reference solver takes a budget in units of work and returns unknown when it is spent.
   • The answer depends only on the query and the budget. Test: the same query gives byte-identical answers at 1 and N threads.
3. Build time:
   • A package that depends on it calls it from a comptime.
   • Test: a comptime that proves x > 30 ∧ x ≤ 30 ⇒ false builds and records nothing in nikaia.proofs.
   • Test: the ledger of the logic package derives sync and touches = [] (ADR-321 D8), so NK1152 does not fire.
4. Determinism:
   • Part III 13.5’s guarantee holds with the package’s version in nikaia.lock.
   • Test: --locked passes with such a comptime and an unchanged lock.
5. Later, with ADR-321 §6 decided: the sqlite driver (#117) uses it for WHERE nullability:
   • W/F encoding as above;
   • unknown means nullable;
   • tests for the OR/AND example and for a LEFT JOIN.

Comments

keywan-ghadami, 2026-10-06

The prerequisite is decided: ADR-321 D13 lets a grammar call its own package’s functions and its Nikaia dependencies, so a driver can ask the logic package. Build: #479.

---

Generated by Claude Code

Back to Open Issues