Nikaia
Menu
v0.0.1343pre-alpha GitHub

Issue #1104: Claim (b): the certificate checker (logic_lia, logic_alethe, logic_search) and the two tools panics at zero unproved checks

Open and answer this issue on GitHub.

ready · opened 2026-10-31 · updated 2026-10-31 · 0 comments

agent: builder model: opus max_turns: 120 budget_usd: 25 — Facts: Where things live, Traps already met, Commands

Part of #1053 (claim (b)), its step 5 and the panics. docs/formal-verification.md §3 item 5 and §6: the certificate checker, the trusted kernel, is the first file brought to zero unproved checks. Not briefed yet; do after ADR-385 D2 (the issue for p13) and #388’s fill case, which free part of its sites.

Figure (2026-10-31, lower-std --bounds --asserts, loops on)

Unproved sites: logic_lia.nika 54, logic_alethe.nika 21, logic_search.nika 18 (lg_verify, lg_follow, lg_replay, lg_replayed; the Farkas and rounding steps in logic_lia.nika). Mostly list elements used as indexes (held[place], needed[from]: certificate data), lists filled pairwise (#388), parameters.

To build

  1. Re-measure the three files (target/fast/nikaia lower-std --bounds --asserts --optimization prove-through-loops:on > R, then scripts/proved.nika -- R) and sort their sites by form.
  2. An index read out of certificate data: a guard that rejects a malformed certificate (throw/false result, not a stop) where the data comes from outside the checker; an assert precondition where every caller proves it (e.g. assert(at == made.len())), checked by --asserts.
  3. The two panic( calls in the tools (check_walked.nika :121, emit_grammar.nika :225): each a claim proved unreachable or a throw.
  4. A prover gap met on the way is not written around (CLAUDE.md, A missing form stops the work): report it, Needs: architect decision.
  5. Done when the three files and the panics read 0 unproved in the figure; docs/formal-verification.md §2/§4 updated (“the proof kernel is free of run-time errors” only then).

Tests: each changed function keeps its it/tests/compiler tests passing; a new guard gets a tests/compiler program feeding a malformed certificate, if one can reach it from Nikaia; otherwise say so.

Rules

As in docs/briefs/common.part. Edits tools/*.nika: re-lower (lower-std), never stage lowered/project_members.rs, check docs/briefs/batch.txt does not hold these files.

Generated by Claude Code

Back to Open Issues