Issue #650: Prover and diagnostics: a guard does not prove a claim on an unannotated len(); underline over comments; --asserts omits derived contracts

Open and answer this issue on GitHub.

compiler, ready · opened 2026-10-18 · updated 2026-10-18 · 0 comments

Found while writing the website’s assert examples (2026-10-18, binary built from 0.0.1012). Each was reproduced with target/release/nikaia; none is shown on the site.

1. A guard does not prove a claim about an unannotated length (bug). let n = out.stdout.len() over process::run(..)’s output, then return if n != 41 (or if n != 41 { …; return }), then assert(n == 41): still NK1202. With let n: int = out.stdout.len() the claim is proved; let n = word.len() on a main String parameter is proved too. Part III 14.2 / ADR-269 D6: after the guard, the claim is proved. Test: both spellings proved.
2. The underline of NK1207 and NK1202 runs over a trailing // comment, and NK1207 marks the whole println(...) instead of the call share(1, 0) that breaks the precondition. Test: the span is the call.
3. NK1202’s summary says “1 type error”; it is a proof finding.
4. nikaia check --asserts lists only written asserts: a derived precondition (one carried back from a callee, Part III 14.2) and postconditions are not listed. Decide in the build whether the report should list them (Part III 14.2 says --asserts names each claim’s state); if it needs the owner, set decision.
5. Minor: build --asserts and build diagnostics print absolute paths, where check prints the path as given.

Back to Open Issues