Cost estimates for binary descriptor execution #
These engineering priors guide static candidate selection; they never affect semantics or refinement. The model follows the threshold selection used by GMP and the separation of planning from execution used by FFTW.
Generated-code inspection and benchmark calibration remain necessary because Lean's compiler, target architecture, and workload can move useful thresholds.
Coarse superlinear work estimate for exact significand arithmetic.
This is intentionally cheap to reduce at specialization time. It is an engineering feature, not an asymptotic-complexity theorem.
Instances For
Width- and operation-sensitive estimate for the generic kernel.
The constants are calibrated with benchmarks/scripts/format-comparison.sh, in units of
approximately 100 ns. Above 128 bits, fixed allocation costs dominate the measured range;
limb-count terms account for the remaining arbitrary-precision work.
Instances For
Estimate for a monomorphic binary32 or binary64 specialization.
The shared addition, multiplication, and division estimates use geometric means of measured
binary32 and binary64 costs, on the same approximately 100 ns scale as genericEstimate.
Instances For
Estimate for a reusable one-word kernel on a structurally eligible descriptor.
Tiny-format constants are calibrated against the same descriptor carrier as the table candidate. Wider-format estimates use measured binary16 and 24-bit costs.
Instances For
Estimate for a fixed-count native-limb kernel.
Instances For
Estimate for a kernel over a runtime-sized buffer of 32-bit limbs.
Measured addition and subtraction costs grow linearly in the limb count; multiplication and FMA include the quadratic schoolbook product. Both this kernel and the generic kernel allocate on every call. Their allocation estimates are equal, so selection compares the estimated times. Division and square root have no wide-limb kernel and receive the generic cost.
Instances For
Calibrated table-generation work per encoded result.
The small width bands capture the measured decrease in generator overhead per entry as a table gets larger. They depend only on encoded width and operation, never on a catalogued format name.
Instances For
Estimate for a dense byte table over all encoded operands.
One result occupies one byte because this candidate is only constructed when bitWidth ≤ 8.
The selector's memory policy independently rejects tables that are valid but too large.
execFloatBackendCalibration showed table construction to be approximately linear in the number
of encoded results for each operation. The operation-specific coefficient is therefore a more
accurate and more stable prior than multiplying by the public generic-kernel estimate: table
generation runs below the ExecFloat carrier boundary and has a different constant factor.