[ngngardner]

Adds a fixed-decimal number writer, spec-first. The services ported from Python format numbers with '%.1f' / format(x, '.2f') and were hand-rolling the rounding on number text (qbt queue-cleanup has its own half-to-even round.go).

def num.fixed(raw: String, places: Nat) -> Maybe<&2, String>

It takes a number's text, which is what as_num reads, and not a Json. That way a caller can format a number it holds as text too, and as_num composes with it in a Maybe bind. It answers None when the text is not a JSON number (num.ok). The export is in main.bend, the logic is in the new pure module src/fixed.bend, and the README usage section documents it. places is a Nat, as Python's precision is.

Reference behaviour and the float caveat

The result is IEEE 754 roundTiesToEven applied to the exact decimal value of the text. That is Python's format(Decimal(s).quantize(Decimal(10) ** -n, ROUND_HALF_EVEN), 'f'). On every input whose decimal value is exactly a binary double, it is also Python's '%.Nf' % float(s). Python's '%.Nf' rounds the nearest double, not the text, so the two differ in three ways. SPEC.md lists all three:

• The double falls on the other side of a boundary. 2.675 to 2 places is 2.68 here and 2.67 in Python. 0.15 to 1 place is 0.2 here and 0.1 in Python. 0.45 is 0.4 here and 0.5 in Python. 0.0005 to 3 places is 0.000 here and 0.001 in Python. 9.995 to 2 places is 10.00 here and 9.99 in Python. 0.049999999999999999999 to 1 place is 0.0 here and 0.1 in Python.
• More than 17 significant digits. 1e23 to 0 places is 1 followed by 23 zeros here and 99999999999999991611392 in Python. 123456789012345678.5 to 0 places is 123456789012345678 here and 123456789012345680 in Python.
• Outside the double range. 1e400 is written out in full here and is inf in Python. 1e-400 agrees: it is 0.00.

Exact values agree with Python: 0.125, 2.5 to 0 places is 2, and 0.5 is 0. Negative zero is kept as Python and C's printf keep it: -0.04 to 1 place is -0.0, and -0 to 2 places is -0.00. With 0 places there is no point, so '%.0f' % 2.5 is 2.

Cost: the exponent is read as a Nat and the point moves one place per step, so time and memory grow with the exponent's value. 1e999999999 asks for a billion digits. A caller formatting untrusted numbers should bound the exponent first. SPEC.md's prose says so.

Rows (new group JSON-FIX, interface family)

ID	Level	Status	Requirement (short)
JSON-FIX-1	Proved	proved	num.fixed(s, n) is None when num.ok(s) is false, and Some{F.text(s, n)} when it is true
JSON-FIX-2	Proved	proved	- followed by s is written as - followed by the unsigned text of s. A text that does not start with - (the empty text too) is written unsigned. The minus is kept even when every digit rounds to 0
JSON-FIX-3	Proved	proved	The text is cut at the first e/E, then the mantissa at the first .. The exponent's sign is applied (- makes it negative, + is dropped) and its digits are read most significant first. The point moves k places right or left, one carry per step, with a 0 when a side runs out. A move right then left gives the same digits back, and so does left then right
JSON-FIX-4	Proved	proved	Exactly n fraction digits are kept, padded with 0s. The kept digits go up by one when the first dropped digit is above 5, or when it is 5 and a later dropped digit is nonzero, or when it is a tie and the last kept digit is odd. No kept digit at all counts as an even 0. A carry turns 9s into 0s and may add a new leading 1
JSON-FIX-5	Proved	proved	The integer part is every digit before the last n, with leading 0s dropped (0 if none is left), then . and the last n digits when n ≥ 1, and no point when n = 0

Laws (53, all quantified and tagged; LAWS.bend --- fixed decimals ---)

• JSON-FIX-1: fixed_none and fixed_some (direct).
• JSON-FIX-2: text_minus, text_plain and text_empty (direct).
• JSON-FIX-3:
  • unsigned_steps states the decomposition: split, move, round, write.
  • Cut laws: parts_exp and parts_plain, under the hypothesis no_e(mant); mant_dot and mant_int, under no_dot(int). The proofs go by induction through the new lemmas fx_cut_e_hit, fx_cut_e_none, fx_cut_dot_hit and fx_cut_dot_none.
  • Exponent sign: esign_minus, esign_plus and esign_digits.
  • Reading the exponent: place_parts, nat_start and nat_end. nat_snoc says that one more digit gives 10 × the value + d, by induction, which is what makes the reading positional.
  • Moving the point: move_right, move_left, ups_zero, ups_succ, downs_zero, downs_succ, up_digit, up_zero, down_digit and down_zero. up_down and down_up are frame laws: a move and its inverse give the same digits back.
• JSON-FIX-4:
  • round_cut states the decomposition.
  • Padding: pad_width says exactly n digits are kept, a frame law proved by induction. Also pad_none, pad_digit and pad_past.
  • The rounding decision: up_exact, up_below, up_above, up_past_half, up_tie (the half-to-even rule on the last kept digit) and up_tie_none.
  • The sticky digits: nonzero_zeros says all-zero dropped digits are not past half. nonzero_digit says one nonzero digit anywhere is past half. Both are by induction.
  • The carry: bump_up, bump_down, inc_digit and inc_nine. inc_nines says all 9s become 0s plus a 1, by induction.
• JSON-FIX-5: write_parts, point_none, point_some, trim_zero and trim_lead. trim_zeros says only zeros, or no digits, are written 0, by induction.

Many of these laws are step equations whose proof is a single rewrite on the hypothesis, or {==}. Together they pin every step of the algorithm in the order the text is read, as SYS-TIME does in ezsys. The non-definitional ones are nat_snoc, pad_width, nonzero_zeros, nonzero_digit, inc_nines, trim_zeros, up_down, down_up and the cut laws. They are proved by induction.

Trust boundary

Unchanged. No Trusted row was added. This is new behavior, so no released guarantee changes.

Gate (bend 2.0.38, bolt and ez 1.5.0 from the flake)

• With the laws written and no proofs yet, bend PROOF.bend reported 53 TODOs. With the proofs in place it prints ALL PROOFS CHECK (about 5 s).

• bolt on the whole tree reports 0 errors and 2 warnings. Both warnings are the existing L001s on lex.run and print.maybe, the same as on main. trace is at error, and the 5 rows agree with the tags.

• nix flake check passes: proofs, lint, scale and bench-compare.

• Planted bugs: I planted one bug per row group, confirmed the gate failed, and restored the code:

  Row	Planted bug	Law that fails
  FIX-1	non-numbers answer Some{""}	fixed_none
  FIX-2	the minus is dropped	text_minus
  FIX-3	a move right pads with 1	up_zero
  FIX-3	e+ makes the exponent negative	esign_plus
  FIX-4	a tie rounds to odd	up_tie
  FIX-4	inc adds 2	inc_digit
  FIX-4	nonzero is inverted	nonzero_zeros
  FIX-5	trim writes the empty text for zeros	trim_zeros
  FIX-5	, instead of .	point_some

Differential test against Python (driver not committed)

The driver is a compiled C-lane binary that calls num.fixed on each case. I ran 4 seeds of 751 cases each, 3004 checks in all. Each seed had 500 random JSON numbers, biased toward 5 ties, with signs, fractions, e/E/+/- exponents up to 2 digits and 0 to 8 places. Each seed also had 47 edge texts × 5 place counts, and 16 invalid texts ("", 01, 1., .5, +1, 1e, NaN, ' 1', …). The JS lane was spot-checked on the README examples.

• Against Decimal(s).quantize(10**-n, ROUND_HALF_EVEN), and None for the invalid texts: 0 mismatches.
• Against '%.Nf' % float(s) there were 291 mismatches across the 4 runs, and every one falls in one of the three classes above:
  • 20 were the double-range class: 1e400 gave inf in Python.
  • 219 were the more-than-17-digits class. These were integers past a double's precision, such as 1e23, 45432.875e25 or 5E+49.
  • 52 were the boundary class. Some were ties in the text that the double moved off the tie, such as 2.675, 0.15, -71.350, 1548.7455 and 0.650. Others were near-ties on the other side, such as 0.0005, 9.995 and 0.049999999999999999999.

🤖 Generated with Claude Code