Float investigation — multiplication work, source form, and demand

This continues the rounded-pipeline investigation. The lazy Haskell reducer is the established performance baseline, not an assumed bottleneck. Neither reducer nor production compiler/library code changed here. LSB-first remains a control/candidate, not a frozen public float encoding.

Questions

• Does recursive source form, rather than arithmetic work, explain much of the multiplication cost?
• Can useful significand invariants avoid computation?
• Which apparent improvements preserve the partial-input behavior of existing lib/math/native.tri arithmetic?
• Is there a concrete compiler investigation lead, rather than a blanket assumption that its output is inefficient?

Two bounded experiments answer parts of these questions. Neither instrumented reduction counts nor a strict surrogate evaluator was used. Timing, cumulative allocation, compiled-tree structure, and demand probes are distinct observations.

1. Multiplication alternatives

Workers: bench/float-multiply.tri. Harness: test/float_multiply.py.

Variant	Change relative to native natural multiplication
native	Existing local-recursive binary Horner multiplication
hoisted	Same recurrence, explicit top-level recursive operand parameter
topBit	Return multiplicand at the highest canonical multiplier bit
fused	Specialize a + 2*p: emit the low bit and add the remaining tails
positive	Additionally omit zero-normalizing shifts; positive multiplicand required
accumulate	Low-to-high shifted-factor accumulator
karatsuba	One 26-bit split, three native leaf products and recombination
mux	Native recurrence with a different full-adder Boolean expression
adaptive	Count set bits and choose the sparser operand as multiplier

Each variant was measured with three consumers:

• full exact product;
• the generic 53-bit rounding pipeline;
• a normalized-53-bit-input pipeline that knows the product is 105 or 106 bits and determines its rounding shift from a fixed bit rather than computing width.

The latter invariant is an explicit internal contract, not a replacement for arbitrary natural multiplication. Positive specialization likewise is not validated on zero multiplicands.

Correctness and demand

The general corpus has 360 input pairs (small exhaustive values, power/limb boundaries up to 106 bits, and random inputs). Exact and generic-rounded workers are checked in batches. The positive variant excludes zero multiplicands. The bounded-width workers have another 73 normalized-input pairs. There are 180 finite-value validation invocations, 27 separate demand probes, and 540 checked measured invocations across 108 workload groups.

Demand probes ask whether multiplying a partially defined input by zero, one, or two permits a known output to be observed. For example, let:

a = Fork True (diverging computation)

The existing N.multiply can return the low bit of a * 1 (1), or of a * 2 (0), without inspecting that divergent tail. These are numeral-shaped partial inputs, not complete finite numeric values.

Karatsuba and adaptive scheduling failed the latter two probes within the three-second limit; their zero-right probes succeeded. Source inspection explains the additional demand: popcount scheduling inspects the operand, and the Karatsuba recombination/subtractions require information beyond the requested low bit. A timeout is recorded as bounded experimental evidence, not itself a proof of divergence. Both passed their complete finite-value arithmetic checks.

The other variants passed these three probes. This is not proof of general demand equivalence: the second experiment below finds a difference those probes missed in the mux adder.

Results

Medians for batches of eight normalized 53-bit pairs, full exact products:

Variant	Random ms / allocated MB	Dense ms / allocated MB
native	53.84 / 413.62	100.27 / 812.03
hoisted	53.31 / 414.60	105.23 / 813.09
topBit	53.88 / 417.61	104.48 / 816.11
fused	56.91 / 410.69	107.99 / 800.89
positive	54.81 / 407.88	101.76 / 799.33
accumulate	92.53 / 612.59	133.26 / 1023.05
karatsuba	60.85 / 420.61	101.85 / 722.73
mux	57.09 / 384.05	91.66 / 713.63
adaptive	46.88 / 379.08	109.45 / 825.92

No convincing allocation improvement comes from hoisting recursion alone. Removing the highest-bit work or specializing shifts also buys little here. The accumulator is worse on these random/dense inputs. One-level Karatsuba is not a universal win at this precision; this does not establish its crossover point or rule out other splits/recursive strategies.

Operand shape matters greatly. With a sparse left operand, native took 45.11 ms / 373.40 MB and adaptive took 4.87 ms / 22.25 MB. With a sparse right operand, native already took 3.26 ms / 14.74 MB, while adaptive took 3.61 ms / 22.11 MB. The recurrence performs additions according to multiplier bits; swapping operands can avoid arithmetic work, but determining whether to swap adds work and changes partial-input demand.

Known product width removes a modest amount of allocation: random native rounded output was 406.91 MB versus 394.73 MB with the known-width consumer. Wall medians were 63.83 and 64.30 ms, so this run does not establish a timing win. Exact product allocation was 413.62 MB: asking for a rounded answer does not necessarily force every bit of the exact intermediate product. The lazy consumer matters, even when source code denotes an exact product first.

Compiler and runtime observations

The inspected source_compile, source_core, and source_stable files match the shipped compiler's accepted source hashes. The stable backend deliberately restricts constructor folding and binder-independent pruning; arbitrary closed computations and eta rewrites are not automatically safe in this language.

Compiled reachable DAG sizes for native/hoisted were 537/533 nodes, with distinct structural fingerprints. These sizes characterize stored function trees, not runtime reductions. Similar arithmetic cost despite different recursive source form gives no justification for a general lambda-lifting/compiler rewrite.

The run also records GC elapsed time and live bytes after complete forcing. For random native exact products, sampled GC elapsed time was 4.45 ms of the 53.84 ms interval. This is not a decomposition of every runtime cost, but it does not support calling GC pauses the sole dominant expense. Post-force live bytes were about 94 KB despite 414 MB of cumulative allocation. That is an endpoint snapshot, not peak residency, and includes host state. Negative live deltas simply mean earlier reachable inputs/workers became collectible. These observations do not establish that laziness itself is the problem.

Full data: bench/float-multiply-results.json; raw run: /tmp/tricu-float-multiply-measured.

2. Isolate the adder and inspect Boolean demand

Workers: bench/float-adders.tri. Harness: test/float_adders.py.

The native full-adder carry is equivalent on total Booleans to:

(a && b) || (carry && (a || b))

The first mux rewrite used:

if a then (b || carry) else (b && carry)

With a = False, carry = False, and unknown/divergent b, the native expression produces False without inspecting b. The rewritten expression inspects b first. The corrected order is:

if a then (b || carry) else (carry && b)

This is not a theoretical concern only. On the actual sum trees, the probe

head (tail (add 2 (Fork (diverging computation) 1)))

asks for bit 1 of either 4 or 5. The answer is 0 in either case. Native returns it; the original mux exceeded the three-second limit; both corrected variants return it. Interestingly, a probe skipping to bit 2 succeeds even for the original mux: that later carry can become known independently. Demand is consumer-specific, not simply “this function is strict.”

test/float_adders_demand_test.py additionally checks all 27 assignments of False/True/bottom to the full-adder's three Boolean inputs. Native and corrected carry functions agree on that flat domain; the sum expressions also agree. This supplements real tricu tests, not a proof about arbitrary intensional tree contexts or all partial numeral computations.

Source-form control

The corrected ordered version binds neg = not carry once. The inline version writes not carry in each of two mutually exclusive branches instead. The carry operand order is identical. Only one of those negations is needed in any evaluation of the result bit, so there is no obvious dynamic sharing benefit from this particular binding.

This creates a narrow source-form comparison, not a recommendation to remove all let bindings. Shared computations elsewhere can be essential.

Validation and results

There are 324 addition pairs for each full/low-bit/next-bit consumer and each of four variants. Five actual partial-input probes are run per variant. Only the original mux's unknown-low/bit-1 probe times out; all others return expected values. The run has 280 measured invocations across 56 groups, plus independent product checks. Every complete finite result is checked against Python integers.

Medians for batches of 16, random inputs:

Worker	53-bit full add ms / MB	106-bit full add ms / MB	53-bit exact products ms / MB
native	6.30 / 30.05	12.01 / 59.62	142.76 / 818.13
original mux	6.07 / 27.78	11.29 / 55.16	137.64 / 758.89
ordered mux	6.27 / 27.88	11.20 / 55.37	138.55 / 760.18
inline ordered mux	5.67 / 24.94	9.75 / 49.49	119.60 / 679.95

In the random multiplication batch, the corrected inline variant reduces allocation by about 17% relative to native. Relative to the ordered bound version, about 11% of allocation disappears from this source-form change. The product recurrence is otherwise unchanged. Carry-pattern additions with a small second operand show much less separation; many operations take existing successor/empty-operand paths rather than the full-adder path.

Compiled DAG sizes were native 430, original/ordered mux 444, inline 412. Here source size/shape and measured work move together, but static DAG node count is not a general cost metric: the first experiment already showed its limitations.

All variants were also measured with only the low or next result bit demanded. Their small timings are dominated enough by sampling overhead that the full results and targeted bottom probes provide stronger evidence than tiny timing rankings.

Full data: bench/float-adder-results.json; raw run: /tmp/tricu-float-adders-measured.

Interpretation and next questions

The subsequent stable binding/abstraction investigation now reproduces emitted trees with an independent finite model, attributes the extra abstraction work, and includes nonnumeric sharing, captured-closure, and eta-observation counterexamples. No production compiler changes were made.

• The strongest wins so far come from requesting less arithmetic work or expressing an inner operation more cheaply, not replacing the reducer.
• A mathematically correct rewrite can still have the wrong demand. Numeric differential tests alone missed the first mux counterexample.
• The ordered-inline adder is a credible compiler investigation lead: why does this exclusive-branch binding produce more runtime work? Before any compiler change, isolate the lowering, characterize when inlining is safe, and test sharing/demand/structural-observation consequences outside arithmetic.
• Sparse-operand scheduling remains a possible explicit finite-input strategy, not a transparent rewrite of partial-input multiplication.
• Full binary64 semantics, correctly rounded division, bounded exponent alignment, and public value invariants remain open. These benchmarks have not committed the representation or established a general compiler optimization.

Reproduce

Both measurement harnesses use fresh processes, one capability, a 2 GiB heap limit, explicit time budgets, shuffled workload order, and five repetitions with the first excluded. Timing includes invocation through sharing-aware full forcing before rendering, including profiling collection overhead. Inputs are supplied at runtime, not compiled as constant answers. Allocation is cumulative, not peak/live memory. Separate runs use different deterministic corpora; compare variants within a run rather than treating their absolute times as identical jobs.

HOST=$(nix build .# --no-link --print-out-paths)/bin/tricu
python3 test/float_adders_demand_test.py
python3 test/float_multiply.py "$HOST" \
  --directory /tmp/float-multiply-new --size 8 --repeats 5
python3 test/float_adders.py "$HOST" \
  --directory /tmp/float-adders-new --size 16 --repeats 5

Use fresh output directories and normal assertion settings. Reports preserve source/compiler/runtime hashes and demand-failure diagnostics. No production encoding, compiler, reducer, or math API was changed.