Result: done
Files: crates/nikaia/src/main.rs crates/nikaia/src/sysroot.rs scripts/proved.nika docs/formal-verification.md
Commit: prover: lower-std --asserts prints each tools file’s claims, and the figure counts claims, panics and the checks left at run time
Body: nikaia lower-std --bounds --asserts prints each tools file’s --bounds block, then its check --asserts block (check_claims_report, read with refuses on: check_against refuses an unproved claim, ADR-380 D1); --asserts alone prints only the claim blocks; plain lower-std is unchanged. scripts/proved.nika sums the asserts in headers into a claims: line, counts panic( calls in crates/nikaia-std/src/tools/*.nika, skipping // comments and names such as a_panic( (read from the checkout’s root, like the report’s paths), and prints left at run time (unproved indexes + operations + unproved claims + panics). A report without --asserts says claims: not counted and leaves out that term. The brief expected 13 panics in 9 files; the count is 3 in 3: raw grep gives 16 in 9, but 10 are in comments and 3 are a_panic(, a method name. formal-verification.md §2 and §4 now carry the a784e6d figure at both settings.
Part: #1053
Tests: cargo test –profile fast -p nikaia –lib – sysroot:: bounds_report:: (8 passed); no test covers bounds_tools, so checked by hand on a784e6d: lower-std --bounds --asserts (247 asserts in blocks) then proved.nika prints “proved: 1543/2676 indexes (57.7 %), 840/1633 operations (51.4 %), 247 files, 0 refused” / “claims: 0 asserts, 0 proved (0 through a loop), 0 preconditions proved at every call, 0 not proved” / “panics: 3 in 3 files” / “left at run time: 1929”; with prove-through-loops:on 1575 (58.9 %), 846 (51.8 %), left 1891. --bounds alone gives “claims: not counted (run lower-std with –asserts)” and “left at run time: 1929 (indexes, operations and panics; …)”. A scratch sysroot copy (not the checkout) with 2 proved asserts and 1 precondition added gave “claims: 3 asserts, 2 proved (0 through a loop), 1 preconditions proved at every call, 0 not proved”; a synthetic header tested the not-proved and loop fields; an unproved assert gets the file refused (NK1300), as the build does. cargo fmt, clippy (1.97 and 1.99.1), pre-push-check.sh all clean
Gate: green
Deviation: none
Found: a view of a temporary in a let passes nikaia check but rustc refuses it (“Temporary value dropped while borrowed”, against ADR-278 D19 “a temporary is taken”); probe: use std::process / fn main() throws { let root = process::run("echo", ["hi"]).stdout.trim().to_string(); println(f"{root}/x") }, also without .to_string(); the lowering drops .to_string() and writes let root = process::run(..).await?.stdout.trim();. Also on the unfixed binary. proved.nika does not use that form: it reads the tools path relative to the checkout’s root.
Needs: none
Changelog: nikaia lower-std --asserts (with or without --bounds) prints each tools file’s --asserts report, so scripts/proved.nika can count the tools package’s claims beside its indexes and operations.
Owner: none
Disk freed: 655 MB (the clippy 1.99.1 target); target/nikaia-project-tests 3.5G, 9.0G free, no large entry from this run
Rs2nika: none
Pushed: local 4eef22762575794b50d78e7ca2030a2b65ded246
