bin_float Design

bin_float is the binary numerical core of floating 0.7.1. Its design has two simultaneous goals: preserve exact integer/dyadic semantics at arbitrary precision, and reproduce the declared IEEE 754-2019 behavior when a bounded BinaryContext is supplied. Public names are fixed by src/bin_float/pkg.generated.mbti; coefficient layouts, dispatch thresholds, and scratch storage remain implementation details.

Design Contract

The package separates three concerns that are often mixed in a floating-point implementation:

1. BinCoeff performs exact non-negative integer arithmetic.
2. BinFloat represents a dyadic value or an explicit special state.
3. BinaryContext applies a target precision, exponent range, rounding mode, tininess policy, and status flags to one operation.

This separation is the main correctness device. Kernel algorithms may change the cost of producing an exact coefficient, but only contextual finalization may change the represented floating-point result.

Representation And Invariants

A finite value denotes

(-1)^negative × coefficient × 2^exponent2

with an explicit working precision. A nonzero finite coefficient is odd because normalization removes powers of two and moves them into exponent2. The sign is stored independently, so positive and negative zero remain distinguishable. Infinity, quiet NaN, signaling NaN, and NaN payloads bypass the finite model and remain observable.

On non-JS targets, BinCoeff selects an inline 64/128-bit representation or a little-endian array of 32-bit limbs. The JavaScript target uses host bigint behind the same public contract. No caller can observe which storage form or coefficient algorithm was selected.

Standard Alignment

The IEEE-facing path follows a fixed operation pipeline:

operands + immutable BinaryContext
  -> classify NaN, infinity, zero, and invalid combinations
  -> compute an exact dyadic/rational result or certified enclosure
  -> round once in the requested direction
  -> apply exponent bounds and before/after-rounding tininess
  -> return value + BinaryFlags

BinaryInterchange is the only fixed-width encoding boundary. It decodes and encodes binary16, binary32, binary64, and binary128 without routing through a host Float or Double. Context arithmetic and interchange therefore share one value model while keeping format width explicit.

The conformance claim is deliberately narrower than the implementation. The pinned TestFloat matrix covers add, subtract, multiply, divide, and square root for the four interchange formats, five rounding directions, and both tininess policies. Pinned MPFR 4.2.2 data covers the documented square-root, integer- power, and elementary-function boundary. Passing these finite matrices does not claim every IEEE 754 operation or every real input.

Coefficient Algorithm Selection

Dispatch depends on operand size, shape, target, and algorithm preconditions; it is not a single size cutoff. For multiplication, n is the shorter operand length in 32-bit limbs and m is the longer length.

Decision	Condition	Selected path	Reason
Inline/schoolbook	n < 96	fixed-width or schoolbook	setup and allocation dominate at small sizes
Transform	n reaches the target NTT threshold and CRT bounds fit	two-prime Montgomery NTT + CRT	asymptotically lower work for large dense products
Oversized transform	a full transform does not fit but overlap is legal	overlap-add NTT	retain transform scaling without violating length bounds
Unbalanced	m > 2n after transform checks	block the longer operand	avoid padding a highly rectangular product
Large balanced	n reaches the target Toom-3 threshold	Toom-3	reduce recursive multiplication count
Medium balanced	otherwise	scratch-backed Karatsuba	lower asymptotic cost without transform setup

Squaring has its own schoolbook kernel and thresholds because cross terms are symmetric. The current crossover parameters are:

Target	Karatsuba	Toom-3 / NTT multiply	NTT square	recursive-square entry
native	96	2,048	768	512
LLVM	96	2,048	768	768
Wasm / Wasm-GC	96	4,096	3,072	768

These values are empirical policy, not semantic constants. Exact reconstruction bounds are checked before NTT selection; failure selects an exact integer fallback rather than accepting a transform result outside its proof range.

Division uses a similarly staged selector:

• inline or one-limb division for the smallest denominator;
• normalized Knuth division below 48 denominator limbs;
• Burnikel-Ziegler block division from 48 limbs;
• reciprocal Newton division from 1,024 limbs;
• a bounded high-product search for short near-equal quotients where applicable.

Every path returns quotient and remainder satisfying n = qd + r and 0 <= r < d. Square root uses fixed-width kernels through 512 bits and a divide-and-conquer path above that boundary. GCD uses Euclid on small inputs and Lehmer batching once leading-limb quotient prediction can amortize divisions.

Certified Elementary Functions

Elementary functions do not accept a repeated approximate value as evidence of correct rounding. A try_*_ctx function constructs directed lower and upper enclosures at a working precision, rounds both endpoints under the target context, and accepts the result only when both the value and flags agree.

Refinement begins with target precision plus guard bits, permits at most 12 attempts, and grows the working precision by max(32, work / 2). Failure to certify range reduction or the target rounding cell returns a structured ArithmeticError::CertificationFailure. The non-try convenience methods unwrap the same proof-producing path; they do not switch to an unchecked host transcendental function.

Optimization And Boundary Tuning

The switch boundaries are chosen by the unified Maremark benchmark hierarchy, not by asymptotic complexity alone. Measurements distinguish balanced, unbalanced, sparse, dense, and square shapes; target-specific policies are kept because allocation, integer lowering, and transform constants differ across native, LLVM, Wasm, Wasm-GC, and JavaScript.

An optimization is accepted only if it satisfies two independent conditions:

1. exact differential/property tests agree across the algorithms on and around every crossover; and
2. confirmatory measurements show a practical benefit under the repository's paired benchmark protocol.

This rule explains why the dispatcher retains simple algorithms below their measured crossover and why every advanced path has an exact fallback. A tuning decision may move a boundary, but it cannot move the numerical contract.

Complexity And Trade-offs

For balanced n-limb operands, schoolbook multiplication is O(n^2), Karatsuba is O(n^log2(3)), Toom-3 is O(n^log3(5)), and NTT convolution is approximately O(n log n) with larger constants and temporary storage. Burnikel-Ziegler and Newton division approach the multiplication cost at large sizes. Shape-aware dispatch and scratch arenas reduce allocation on hot paths, while immutable public values prevent temporary storage from escaping.

The implementation therefore optimizes expected cost subject to exactness, not exactness subject to speed. Thresholds, NTT primes, limb layout, and arena capacity may change in a patch release; normalized values, contextual rounding, flags, and interchange behavior may not change without an API/semantic change.

0.7.1 Semantic Preservation Proof

The optimization boundary is the exact coefficient or exact discarded-bit calculation. It does not cross the contextual finalizer. For far-exponent addition, binary_exact_top(c, e) orders exact magnitudes before alignment, and the split operation preserves the first discarded bit plus the sticky OR of all later bits. Those are precisely the inputs consumed by the existing rounding rule, so the fast path has the same rounded value and flags as the fully aligned path. Every advanced coefficient path retains an exact fallback when its proof precondition fails.

The semantic acceptance condition is observational equivalence at the BinFloat boundary: equal class, sign, coefficient/exponent, precision, rounding result, flags, and interchange bits. TestFloat, MPFR, boundary tests, and differential tests establish this condition for the declared matrices; Maremark only decides whether the private route is worth its setup cost.

Evidence Map

• API reference defines the callable 0.7.1 surface.
• Tutorial gives recommended construction and context flows.
• Conformance states the pinned TestFloat/MPFR claim and its exclusions.
• Performance records target-specific dispatch evidence and the immutable release comparison baseline.