Result: partial
Files: crates/nikaia-std/src/tools/bounds_walk.nika crates/nikaia-std/src/tools/lowered/bounds_walk.rs docs/specification/30-nikaia-tooling.md tests/compiler/tests/prove_loop_counter_bounds.nika tests/compiler/tests/bounds_expectation_guards_a_proof.nika tests/compiler/tests/prove_loop_counter_bounds.bounds tests/compiler/tests/prove_for_counts_its_turns.nika tests/compiler/tests/prove_for_counts_its_turns.stdout tests/compiler/tests/prove_for_counts_its_turns.bounds tests/compiler/tests/prove_for_counts_its_turns.loops.bounds tests/compiler/tests/prove_while_counter_relative.nika tests/compiler/tests/prove_while_counter_relative.stdout tests/compiler/tests/prove_while_counter_relative.bounds tests/compiler/tests/prove_while_counter_relative.loops.bounds
Commit: bounds walk: a loop counts its turns, and a counter is bounded by them (ADR-361 D13)
Body: bounding_turn_steps sums, per path of a turn (fall-through end or continue; break, return and throw end no turn), what each whole-number name the body changes only by n += c / n = n ± c adds; a name changed any other way (reset, product, call, inner loop, lambda, bound again, the loop’s binding, a while condition) gets none. Those sums are the induction step, so low*t <= n - n@ <= high*t is assumed at each head (bounding_turn_bounds, n@ a fresh name with the entry facts copied). A for over a..b gets 0 <= t, a + t < b and binding == a + t; over a collection t < len where the context counts the iterable (bounding_length). A while takes a name grown by exactly 1 on every path as t. The facts go into the body’s facts only (not past a break), at both settings, so under on every walk of the portfolio has them. prove_loop_counter_bounds.bounds and bounds_expectation_guards_a_proof’s embedded off report updated: a while’s s += 1 beside its step i += 1 (k, f’s j) is now proved at off too.
Part: #1053
Pushed: local 28acd94a009c8cfe7a25b0814514a80929dda5b9
Tests: prove_for_counts_its_turns (header “#1053 step 4 (ADR-361 D13): a for counts its turns, and a counter is bounded by them.”) and prove_while_counter_relative fail on the unfixed compiler (/home/user/nikaia-suite binary: ranged k += 1, whiles n += 1, twice s += 2 checked) and pass with the fix; soundness rows (unbounded start, u8 n += 2, reset, inner-loop growth, n * 2, u8 over an unknown range, u8 s += 2 in a while, uneven step) all stay checked at both settings; tests/compiler –both-settings: 474 passed, 1 failed (bounds_expectation_guards_a_proof, its embedded off report now rightly proved; updated, then passed alone through nikaia test –both-settings); cargo test -p nikaia –test it – prove bounds: 179 passed; lower-std fixpoint clean; fmt, clippy 1.97 clean, pre-push-check ok; clippy 1.99.1 not run (5.2 GB free disk). Figure (lower-std –bounds, proved.nika): off 1,520/2,646 indexes, 733/1,620 operations; on 1,552/2,646, 740/1,620; counter reason 579 off, 541 on (ecf435a: 542 on).
Gate: green
Deviation: step 1’s every, some and same are not proved: the walk does not learn the length of a for’s collection (the checker records std_lengths/sized_lengths only for .len() receivers), so only for over a range gets a turn limit today
Found: tools lowering (lower-std) of opt ?? other with both ref Block (let present = else_branch ?? then_branch, else_branch: ref Block?) writes nikaia_std::index::or(else_branch, || then_branch.into()) and rustc refuses it (Block: Copy, &Block: Into
