[siracozmen01]

Problem

math.round of an f64 was floor(value + 0.5), and the addition is rounded before floor sees it:

• 0.49999999999999994, the f64 just under a half, answered 1;
• every odd whole number past 2^52 answered the even one above it, since adding a half to it rounds up to the next even number;
• round(-0.0) answered 0.0, losing the sign.

deterministic programs see these answers, on every machine alike.

Change

• lib/std/math.kest: round(f64) takes below = floor(value) and adds one when value - below >= 0.5. Outside (-1/2, 0) that subtraction is exact. Inside it, below is -1 and the subtraction rounds to at least a half only for values that are -1/2 or above, which is the documented rule. A half still goes up (round(2.5) is 3, round(-2.5) is -2). A whole number, an infinity and NaN answer themselves. round(f32) is unchanged: an f32 plus a half in f64 is exact.
• KEST_PROFILE_VERSION moves from kest-det 4 to kest-det 5, because a deterministic program observes the change. It is named everywhere the profile is: include/kest.h, the glossary, determinism.md, editions.md, getting-started.md, examples/slice/kest.project and tools/fuzz.c.
• docs/user/determinism.md has a new "Rounding" paragraph that states the rule.
• test/regress/roundnear.kest covers:
  • 0.49999999999999994 on both signs;
  • 2^52 - 1, 2^52 and -(2^52 + 1);
  • odd whole numbers past 2^52 on both signs, 2^53 - 1, and an odd one plus a half;
  • halves on both signs (0.5, 1.5, 2.5);
  • just either side of 2.5, and small values just under nought;
  • 1e300, both infinities and NaN;
  • f32 (0.49999997, 8388609 and halves);
  • the sign of nought: round(-0.0) is -0.0 and round(0.0) is 0.0.

BREAKING CHANGE: math.round of an f64 answers 0 for 0.49999999999999994, and an odd whole number past 2^52 answers itself, where both answered one more. round(-0.0) is -0.0 where it was 0.0. The determinism profile is kest-det 5.

Verification

• roundnear.kest answers 1 on main and 0 here. With the old floor(value + 0.5) put back into the built library, it answers 1 again.
• A model in exact rationals over 250,016 f64 values, chosen around halves, whole numbers, 2^52 and 2^53 and nought: the new rule disagreed with round-half-up 0 times and the old one 6,691 times.
• Built with clang-20: ctest --preset dev -j4 passes 21 of 21 (gate, regressions under every switch and compiled to C, conformance), as do tools/check-costs.sh and tools/check-c.sh over every example, library and bench file.
• test/conformance.trace is unchanged: no example's output moves.

Closes #258