- Most turns: the brief’s plan for D1, “add
n <= 2^63 - 1 beside the floor”, cannot prove i + 1, because bounding_fits only states goals up to 2^62 (#444). Finding that out took about 8 turns: I wrote the edit, read the solver’s overflow handling, then found bounding_relatives and reverted. Second was step 2’s probe. My two-file nikaia check --bounds project looked like a failed fix, but that path checks a file alone (bounds_report::report). That cost about 5 turns.
- Could have been handed to me: the 2^62 goal cap and
bounding_relatives, the mechanism that already proves i + 1 under i < n for an i64 n. Also where another file’s types live in the checker: CheckWorld::parts_beside, collect_types_beside skipping non-generic structs, and fields_of reading world.own.types. And that nikaia check --bounds on a project file does not pass the files beside it.
- Checks:
- Ran: probe 1 on the old and new binaries;
lower-std --bounds --asserts at both settings, before and after (needed for step 3, and the diff showed no proof lost); the 5 bounds programs --both-settings; it -- bounds prove; the lib bounds and check filters; fmt; clippy 1.97 and 1.99.1; pre-push-check; the fixpoint.
- Wasted: the lib
bounds filter (it matched 0 tests), the multi-file CLI probe (wrong path), and one test run that failed because a scratch project had no src/.
- One change: a brief whose decision states a numeric fact should say how the walk can use it: here, the goal cap (
solvable(), 2^62) and the relative-goal route. Or it should give the expected way to build it (“a length is an i64 for bounding_relatives”) instead of “add n <= 2^63 - 1 to the floors”. Second, builder-facts should note that nikaia check --bounds checks each file alone, and that only lower-std --bounds checks a file with the package beside it.
This site is open source.
Improve this page.
