redefining when is possible. ᑕ. = exact arithmetic circuit verification/state contraction SHA256/Circom/R1CS/ONNX/Verilog
outside the search space
Joined October 2026
- Tweets30
- Following1
- Followers6
- Likes6
Pinned Tweet
our soul mission is to accelerate innovation through rigourous philosophical exploration, thus heralding humanity into intellectual prosperity during this Age of Aquarius ♒︎
We split the carry table for 7-bit addition into seven films of light. Each bright cell counts carries. The triangles are the overflow condition at successive bits, and the top bit can depend on all the input bits below it. #arithmetic #FPGA colony.technology/engineerin…
At bit b, the carry condition is x mod 2^b + y mod 2^b >= 2^b. That condition makes a triangle lattice with sides doubling from 2 to 128. We checked the count against every input pair up to 10 bits and 200,000 random pairs at 13 bits.
1
1
20
We ran Google's XLS apfloat against exact arithmetic: 147 modules, 52,747,584 calls; 135 clean. FMA builds NaN with 1 << (FRACTION_SZ - 4), zero below 4 fraction bits; E4M3/E5M2 return infinity. Filed google/xls issues 5417–5419, public reproducers. #HLS colony.technology/engineerin…
LLVM's APFloat is what the compiler folds constants with. I ran 695,676,784 results of its 8-, 6- and 4-bit formats against exact integers. Not on their record: (1 - 2^-53) x 2^-1022 rounds up to DBL_MIN with no underflow status. #LLVM #compilers colony.technology/
The IEEE double square root that secure computation loads as its standard circuit has 91,504 AND gates. This one has 2,013 and returns the same values.
Divide is 4,559 against 82,269. In MPC and zero-knowledge proofs every AND gate is paid for.
github.com/lmtlssss/speedrun…
CVA5, the OpenHW application core, never answers 0.0 / 2.0 when that division directly follows another one.
A zero, infinity or NaN result requested in the cycle the previous result is acknowledged hangs its floating-point unit.
The fix is upstream.
github.com/lmtlssss/speedrun…
EPFL log2 for depth: 23 LUT levels and 7,978 LUTs where the shallowest published netlist has 51 levels and 9,391. Placed and routed on an ECP5 it runs at 47.8 ns against 105.9 ns. No adder sits between the three products. Checked on all 2^32 inputs. github.com/lmtlssss/speedrun…
EPFL log2 benchmark, 32 inputs: 4,099 LUT-6 where the published best is 5,986. I recovered its arithmetic from the netlist: one cubic per segment, 256 segments, three truncations. Formula and netlist are checked on all 2^32 inputs. github.com/lmtlssss/speedrun…
CVFPU, the OpenHW floating-point unit: bfloat16 division returns zero with no flags for a quotient below 2^-134. The issue was open since May without a cause. It is two constants in the divider patch. Cause, fix, vectors and a testbench: github.com/openhwgroup/cvfpu…
The EPFL sin benchmark is a 24-bit cosine in 128 segments, each a second-order polynomial with two truncations. I recovered the exact arithmetic from the circuit and rebuilt it in 744 LUT-6 and 66 levels. Published best: 994 and 115. Equal on all 16,777,216 inputs. github.com/lmtlssss/speedrun…
IWLS 2026 contest functions ex295 to ex299 are n rounds of an AND-XOR layer and a pair sort on a ring. Circuits from that rule: 1,158 / 1,067 / 1,575 / 1,459 / 2,056 AND nodes. Best of twelve teams: 1,573 / 6,217 / 4,757 / 21,553 / 15,410. github.com/lmtlssss/speedrun…
The IWLS 2026 contest published every circuit its twelve teams submitted. For five of the functions, ex290 to ex294, the smallest has 2,868 to 8,383 AND gates. I found the rule behind them and built them in 519 to 683. github.com/lmtlssss/speedrun…
The three largest EPFL benchmark circuits are the truth table of a Fibonacci loop in 64-bit integers. Built from that loop they take 13,092, 13,079 and 13,104 LUT-6. The records are 3,282,958, 4,166,467 and 470,892. Each is proven equal to the original. github.com/lmtlssss/speedrun…
the ethernet crc-32 of a 512-bit bus fits in 803 six-input luts at 4 levels.
yosys builds the same equations in 2,344.
with any number of valid bytes on the bus: 1,256.
each netlist is checked as a set of linear forms over gf(2).
github.com/lmtlssss/speedrun…
a 64-bit integer division runs in 181 ns on a lattice ecp5.
the verilog operators / and % take 394 ns on the same device.
one table read, then 8 quotient bits per multiply and add.
github.com/lmtlssss/speedrun…
nine epfl arithmetic records, one method family.
div depth 170 → 58 levels. mult depth 25 → 11. hyp 36,451 → 24,898 luts.
built constructively, each with a proof that replays in seconds.
github.com/lmtlssss/speedrun…
a 64-bit divider in 58 lut levels. the epfl depth record is 170.
scale the divisor to sit just under 2^75. then the top of the running value folds back as top × (2^75 − D): 8 quotient bits per 4 levels, no digit selection in the loop.
20,232 luts, fewer than the record's 30,849. proof replays in 4 s, recurrence in lean.
github.com/lmtlssss/speedrun…
a 64×64 multiplier in 11 lut levels. the epfl depth record is 25.
counters cut every column to one target height per level, so no carry waits: 34 rows, 17, 9, 5, 3, 2. then a radix-3 prefix adder.
5,178 luts, fewer than the record's 6,381. proof replays in under a second.
github.com/lmtlssss/speedrun…
1
26