Issue #390: The default of --optimization, and whether its proofs belong in nikaia.proofs

Open and answer this issue on GitHub.

compiler, ready · opened 2026-10-03 · updated 2026-10-07 · 7 comments

Two questions ADR-271 §6 leaves open:

1. The default

• Today: remove-bounds-checks and remove-overflow-checks are off unless a build asks.
• Measured so far: aggressive costs about +3 % over the 46 standalone files and +16 ms on solver-kernels.nika (solver-workload.md §8.3).
• To decide: whether the default becomes basic, or aggressive, once the compile time is measured over the whole corpus, std included.

2. The proof file

• Today: the walk re-proves on every build, deterministically.
• The other path: ADR-270 D19–D23 put every solver answer into the committed nikaia.proofs.
• To decide: whether the walk’s queries go there too once the search may be nondeterministic, and what that means for the cache key (ADR-271 D1).

Comments

keywan-ghadami, 2026-10-04

State after the owner’s round (2026-10-04)

1. nikaia.proofs - decided: the walk’s proofs go into it. This does not wait for the solver’s search to become free. ADR-306 §6’s “when the solver’s search is free” is superseded.

2. The default - not decidable yet. The owner’s view: aggressive is dangerous today. A proved index is emitted through proven-index’s get_unchecked, so a wrong proof means undefined behaviour, where a wrong overflow proof only means a wrong value. The certificate checker (ADR-270 D5) covers the solver’s arithmetic, not whether the query the walk built says what the program does. The questions are now:

• Can the design let a build buy safety or performance with the prover’s depth or time, and how?
• Opt-in or opt-out?

A decision basis is being prepared first:

• what each kind of wrong proof costs, and which part of the chain is checked by what;
• how SPARK, Dafny, LLVM/HotSpot and Wuffs handle budgets and defaults;
• the design options for a depth/time setting, including what a time budget means for reproducibility now that the answers are recorded;
• opt-in against opt-out;
• the measurements still owed: compile time over the whole corpus with std, and sites proved per budget.

---

Generated by Claude Code

keywan-ghadami, 2026-10-04

Budget, as the owner decided in another session: the prover’s effort is a step budget, never time. Only the expensive steps are counted. That makes counting nearly free, and in any case cheaper than reading the clock. nikaia-logic’s Budget already has this shape: cases, where each case is one elimination, and bounds, the bounds one elimination may hold. It is not counted per operation.

What remains open for #390:

• how a build sets this budget, its depth;
• whether the setting can be given separately for index checks and overflow checks;
• opt-in or opt-out.

---

Generated by Claude Code

keywan-ghadami, 2026-10-04

What makes aggressive dangerous (owner, 2026-10-04). A wrong proof that removes a run-time check turns a defect into a bomb. Where the program would have stopped cleanly, it reads out of bounds through get_unchecked (undefined behaviour) or computes a silently wrong value through wrapping_*. A proof used to find errors is not dangerous: a wrong refutation is a visible build error, and --refuted-claims warn bypasses it.

So the decision basis treats the prover’s two uses separately:

1. Finding errors (refutation, ADR-269 D8): harmless if wrong, and it gains from more budget. It is a candidate for on by default.
2. Removing checks (ADR-306): needs its own decision, and ways to defuse the bomb:
   • a test build that keeps every proved check as an assertion reporting the compiler’s proof was wrong, so wrong proofs surface in CI;
   • index and overflow set separately (undefined behaviour against a wrong value);
   • checking the translation from program to query (translation validation, or differential runs at both levels).
3. Budget: counted in expensive steps only (decided). Open is how a build sets it.
4. Opt-in or opt-out for each use.
5. Measurements owed: compile time, and the sites proved and refuted per budget.

---

Generated by Claude Code

keywan-ghadami, 2026-10-04

Decision (owner, 2026-10-04)

Today’s problem: aggressive is one switch for two things. It means search harder and remove what was proved at once, and nothing lets a build set the budget. Checked in the code:

• prove.rs (written claims: requires, ensures, assert) always runs, and a refuted claim is an error (ADR-269 D8).
• bounds.rs (the checks nobody writes: index and overflow) runs only at aggressive. Its only effect is to remove checks: a check it could show can fail is not reported.
• Both use Budget::default() (1024 cases, 4096 bounds), and no switch reaches it.

Two switches for two things

1. How hard the compiler proves, e.g. --proving=LEVEL / [build] proving.

• The levels map to step budgets, counting expensive steps only (decided earlier).
• It governs both paths: written claims, and the checks nobody writes. bounds.rs therefore runs whatever the optimization.
• The answers go into nikaia.proofs (decided).
• More budget means more defects found at build time.

2. What happens to a proved check: --optimization=remove-bounds-checks and remove-overflow-checks, now on/off.

• It changes only what is emitted, never what is proved.
• Default off: a wrong proof that removes a check turns a defect into a bomb (get_unchecked, wrapping_*, and debug-assertions = false in the generated profile).
• Switching it re-proves nothing, so it causes no extra proving round and no second set of proofs.

A check nobody writes that is shown to fail is an error

Example: an index shown outside the list for a value the program reaches. The run-time check would only stop the program; it would not rescue it. So this is reported as a refused claim is, an error, with --refuted-claims warn as the bypass (ADR-269 D8).

• Only on a refutation, never on unknown. As prove.rs::refutes already demands, the model has to be checked, and the values have to be ones the program reaches; the facts are true but not all that is true. A refusal on a guess would refuse a correct program (Part III C.4).

To build

1. The proving option: command line and [build], levels mapped to a Budget. Pass it to prove.rs and to the walk. Add it to the cache key and to the nikaia.proofs key.
2. Run bounds.rs at every build, independent of --optimization, and record its answers in nikaia.proofs.
3. Reduce remove-bounds-checks / remove-overflow-checks to on/off. basic either becomes a proving level or goes; decide when building, and say which. Removal reads the recorded proofs.
4. A refuted implicit check is an error: a new code (or NK1202’s family), naming the value that fails, and honouring --refuted-claims warn.
5. Update ADR-306 and ADR-269 D8, and Part III 13.3’s [build] table.
6. Tests:
   • a provable index out of bounds is refused, and builds with warn;
   • an unknown index builds silently;
   • a higher proving level proves a site the default does not;
   • toggling removal re-proves nothing (no new nikaia.proofs entries);
   • removal off emits every check even where it is proved.
7. Measure: compile time over the whole corpus with std per proving level, and the sites proved and refuted per level. These numbers pick the default proving level.

---

Generated by Claude Code

keywan-ghadami, 2026-10-04

Written into the records in 8fd9b3f (0.0.451):

• ADR-306 D14-D16 say why;
• Part III 13.3 (optimization is on/off), the refuted-claims paragraph, --bounds and the NK1207 row say what;
• ADR-314 D4 now points at proving.

Step 5 of To build is done.

Still open: proving’s level names, budgets and default, which wait for step 7’s measurements, and whether D3’s walk without a solver stays a level (ADR-306 §6). Part III gets the proving option once those are decided.

---

Generated by Claude Code

keywan-ghadami, 2026-10-04

Steps 2 and 3 of To build are built in 97b883c (0.0.460).

• The walk runs at every build. It proves D3’s shape (a loop over the list’s own length) and every fact D4’s solver decides, whatever the build says. bounds::proven no longer takes a level. The emitter writes a proved check without it only where remove-bounds-checks:on or remove-overflow-checks:on.
• remove-*-checks are on/off. Both are off by default.
• basic goes as a word of the option. Its one shape is proved at every build. Whether a level without the solver is worth offering belongs to proving’s levels (ADR-306 §6), which step 7’s measurements decide. basic and aggressive are refused with the word they now are (on). ADR-306 has an as built note under D14.
• --bounds (#389) reports the same proofs at either setting, and says in its first line what this build writes.
• The full test suite ran with the walk at every build. The only failure was a regression of mine from #380, fixed in 2b2781b.

Still open:

1. The proving option and its budget. Levels and default wait for the measurements.
2. Recording the walk’s answers in nikaia.proofs.
3. A refuted implicit check becomes an error, with a model checked by evaluation.
4. Tests 1, 3 and 4 of step 6, which depend on the three items above.
5. The measurements of step 7.

---

Generated by Claude Code

keywan-ghadami, 2026-10-07

Step 7: sites proved and refuted per budget (measured on 0.0.634)

Method

• Corpus: every tracked .nika file (nikaia lower --no-cache), plus std’s self-hosted tools (nikaia lower-std).
• Patch, not committed:
  • proofs::search takes its Budget from an environment variable, with cases = N and bounds = 4·N (the default’s ratio, 1024/4096);
  • it logs every solver answer;
  • recorded answers in nikaia.proofs are ignored, so that every query is searched.
• Counted, not timed: each row counts solver answers, so it is exact and machine-independent.

Results

cases (bounds = 4×)	queries	proved	refuted	unknown: budget (cases / bounds)	unknown: no contradiction	unknown: overflow
1	984	52	18	484 / 419	2	9
4	989	489	287	63 / 122	19	9
16	995	664	303	0 / 0	19	9
64	995	664	303	0 / 0	19	9
256	995	664	303	0 / 0	19	9
1024 (today’s default)	995	664	303	0 / 0	19	9
4096	995	664	303	0 / 0	19	9
16384	995	664	303	0 / 0	19	9

There are 472 distinct queries; the same query is asked from several places. At budgets 1 and 4 the walk asks fewer follow-up queries, because earlier ones end unknown.

What it says

• From 16 cases up, the budget changes nothing on today’s corpus. No query reaches the limit. The 28 unknowns that remain are outside what more search can answer: no contradiction exists in the facts given (19), or a coefficient overflowed (9).
• Compile cost per level. Above 16 the search is deterministic and never stopped by the budget, so the work done is identical at every setting. A callgrind count per level would show the same solver instructions, so it was not taken. The budget is a cap, not an effort setting, as long as no query reaches it.
• Raising the budget therefore buys nothing today. It would only pay where the walk asks harder queries: more facts per function, nested loops, or quantities the prover reads today but does not combine.
• Lowering it is the only lever with an effect, and only below 16, where proofs are lost (664 → 489 at 4).

For the decision

The measurements do not separate any levels above 16, so they cannot choose a default among them. There are two honest readings:

1. No user-facing levels for now: keep Budget::default() and let nikaia.proofs carry the answers. A proving option then only matters once a program exists that reaches the limit.
2. Levels as caps for pathological programs: a low and a high cap. The default stays far above 16, because there is no measured cost to it.

Not measured: queries from programs that do not exist yet. The corpus has 995 queries; its hardest is answered within 16 cases.

The 303 refuted queries are what step 4 (a refuted implicit check is an error) would read. Most are the walk asking whether a check is needed in a case it then rules out another way. They are not 303 defects. Step 4 still has to tell a refutation the program reaches from one under incomplete facts, as the decision says.

The status stays ready: steps 1 and 4 remain to build. A level design waits for a program that reaches the budget, or for the owner to choose reading 1 or 2.

---

Generated by Claude Code

Back to Open Issues