Result: done
Files: crates/nikaia-std/src/tools/bounds_walk.nika crates/nikaia-std/src/tools/check_collect.nika crates/nikaia-std/src/tools/check_decls.nika crates/nikaia-std/src/tools/check_state.nika crates/nikaia-std/src/tools/lowered/bounds_walk.rs crates/nikaia-std/src/tools/lowered/check_collect.rs crates/nikaia-std/src/tools/lowered/check_decls.rs crates/nikaia-std/src/tools/lowered/check_state.rs crates/nikaia/src/check/core.rs docs/formal-verification.md docs/specification/30-nikaia-tooling.md tests/compiler/tests/length_of_zero_size_elements.nika tests/compiler/tests/length_of_zero_size_elements.stdout tests/compiler/tests/length_of_zero_size_elements.bounds tests/compiler/tests/length_of_zero_size_elements.loops.bounds
Commit: prover: every length is an i64 (ADR-385 D1), and another file’s struct takes space
Body: D1: bounding_length_named (bounds_walk.nika) enters every length the walk reads into walk.typed as an i64, so bounding_relatives states a goal against it as against an i64 parameter: i < xs.len() proves i + 1 <= xs.len(), and a for’s counter, below its turn count t < xs.len() (D13), the same. A fact n <= 2^63 - 1 was not added: the walk’s goals stop at 2^62 (#444), so a constant fact could not prove i + 1 and its 2^63 constant risks the solver’s overflow; the relative goal is the same fact, read as the type. Step 2, cause confirmed: collect_types_beside (check_collect.nika) records another file’s struct only when generic, and named_takes_space (check_decls.nika) read only self.structs, so a list of CxHandled (cexport_model.nika) was unsized in cexport.nika. New CheckState::parts_beside, the package’s CheckWorld::parts_beside copied in collect_types, read by named_takes_space after this file’s structs and enums (a struct takes space where a field does, an enum where a payload does). Shown by emit_entry.nika:153 args.len() + k (Vec[FnArg], Vec[ConfigParam], both another file’s) now proved, which needs two lengths below 2^60. Not reached: nikaia check --bounds on one file of a multi-file project checks it alone (bounds_report::report -> check::check, no files beside it), so there another file’s struct stays unsized. Figures, lower-std --bounds --asserts + scripts/proved.nika, before -> after: off 1,544/2,677 indexes, operations 840 -> 923/1,633 (51.4 -> 56.5 %), counters a loop changes 476 -> 396, left at run time 1,929 -> 1,846; prove-through-loops:on indexes 1,576/2,677, operations 846 -> 929 (51.8 -> 56.9 %), counters 439 -> 359, left 1,891 -> 1,808. No proof lost at either setting (report diff). formal-verification.md §2 takes today’s figures (measured on 9bdbd5a plus this change); Part III’s optimization paragraph says every length and a for’s turns are at most 2^63 - 1. No existing .bounds changed.
Part: #1053
Tests: length_of_zero_size_elements (new): passes at both settings; on the unfixed binary (pre-change target/fast/nikaia) its .bounds and .loops.bounds fail (index += 1, k += 1 checked); prove_for_counts_its_turns, prove_in_loop_assert_bounds, prove_loop_counter_bounds, prove_while_counter_relative (every program with a bounds file) pass –both-settings; cexport.nika :179 and :188 proved in lower-std --bounds (loops on), :182 too; lib bounds (0 match, 89 filtered) and lib check 1 passed; it bounds prove 179 passed; fmt, clippy 1.97 and 1.99.1 clean; lower-std fixpoint unchanged; pre-push-check green
Gate: green
Deviation: none
Found: none
Needs: none
Changelog: Every length is at most 2^63 - 1 for a proof, so i < xs.len() proves i + 1 and a for’s counter is proved for every element type, and a list of a struct another file declares is bounded below 2^60 as one of the file’s own (ADR-385 D1, #1053).
Owner: none
Disk freed: /home/user/nikaia-clippy-new removed after clippy 1.99.1; target/nikaia-project-tests 3.5G, / 9.1G free; new entry over 100 MB: run-bundle/3f8b93b88f7f213d 344 MB
Rs2nika: none
Pushed: local ae09d7752b79f75146d5bb09d6fba4dc41779d26
