Result: done
Files: crates/nikaia-std/src/tools/prover_state.nika crates/nikaia-std/src/tools/prover_walk.nika crates/nikaia-std/src/tools/lowered.rs crates/nikaia-std/src/tools/lowered/prover_state.rs crates/nikaia-std/src/tools/lowered/prover_walk.rs crates/nikaia/tests/it/prove_through_loops.rs crates/nikaia/tests/it/unsafe_follows_switches.rs tests/compiler/tests/prove_argument_lengths.nika tests/compiler/tests/prove_argument_lengths.stdout tests/compiler/tests/prove_argument_lengths_refused.nika tests/compiler/tests/prove_argument_lengths_refused.stderr
Commit: prover: Bytes(x), a bound [v; n] and a literal or repeat passed as an argument have their length
Body: A new length_given (prover_state.nika) gives the length term of a list literal (its items), a repeat (its count, by lin_term), a name the scope follows, and Bytes(x) (x’s, unless a local shadows Bytes). precondition_call takes it for every argument, where only a name was read before; prover_let (immutable) and prover_mutable_list share the new prover_list_length for a repeat and Bytes(x), which records nothing where the term mentions the bound name or its length (let v = Bytes(v)). The two it programs build their bytes as the brief says ([59; 40]; resize then index writes), and bounds_report/lowered drop the --unproved-claims warn 302275e added, since the calls are now proved. g([1, 2, 3]) against >= 40 is NK1207 (false at the call), with two NK1300s in prove_argument_lengths_refused.stderr.
Fixes: #1084
Tests: prove_argument_lengths (7 calls proved) and prove_argument_lengths_refused: run on the unfixed binary (/home/user/nikaia-suite) both refused the proved rows (NK1300, g 2 calls, h 4 calls); tests/compiler –both-settings 498 passed; it prove_through_loops unsafe_follows_switches 11 passed (warn removed); it prove bounds asserts 182 passed; lower-std fixpoint unchanged; clippy 1.97 and 1.99.1, fmt, pre-push-check green
Gate: green
Deviation: no .bounds/.loops.bounds for prove_argument_lengths: the program has no index or operation, and the bounds report lists no precondition, so they would be one empty header line; the proof shows in the program building (NK1300 otherwise). The soundness rows “x a parameter” and “[59; k] with k a parameter” stand in main with unknown lengths (k = xs[2]): in a function of their own the call is carried back to its entry (D20) and never refused (see Found)
Found: a precondition carried back to a function’s entry (D20) is not refused at a call that does not prove it: fn hb(x: Vec[u8]) -> i64 { return h(x) } with h asserting b.len() >= 4, called as hb(u) with u.resize(xs[2], 0): check --asserts says “proved at every call”, the build passes, and the run stops with “precondition of hb: x.len() >= 4” (unfixed binary too; p8’s NK1300 rule does not reach carried preconditions)
Needs: none
Changelog: The prover knows the length of Bytes(x) (x’s), of a bound [v; n] (let as well as let mut), and of a list literal or repeat passed straight to a function, so a length precondition these plainly meet is proved (#1084).
Owner: none
Disk freed: /home/user/nikaia-clippy-new removed after clippy 1.99.1; target/nikaia-project-tests 3.4G, / 9.9G free; new entry over 100 MB: run-bundle/3f8b93b88f7f213d 287 MB
Rs2nika: none
Pushed: local 76c216ed33ddc7ac2ecbb2400073bb4c19b1dc77
