pub const BLAST_BUDGET_NODES: u128 = 8_000_000;Expand description
How many ProofExpr nodes we are willing to materialise for ONE bit-blasted obligation.
A ProofExpr node costs ~100 bytes once its Box is counted, so this ceiling is ~200 MB of
formula. It is calibrated from the measured blast of the RDU demo corpus’s ALU bodies (the
Eq(placed grid, body datapath) obligation at the certified 8-bit bound):
| obligation | gates in the DAG | nodes in the tree |
|---|---|---|
8-bit MAC PE (MatmulTiles) | 851 | 107 247 |
mix (2 inputs, 4 cells) | 1 041 | 10 631 |
| fib, 1 doubling block | 75 | 75 |
| fib, 2 doubling blocks | 1 235 | 65 363 |
| fib, 3 doubling blocks | 13 591 | 354 787 747 |
| fib, 4 doubling blocks | 122 515 | 50 957 299 143 |
fib, 6 — the demo fib.lg | 9 350 207 | 102 116 468 174 507 |
★ AND THE RECONFIG OBLIGATION, WHICH THE FIRST CALIBRATION MISSED:
| obligation | gates in the DAG | nodes in the tree |
|---|---|---|
certify_config_table, 3 islands at width 8 | 8 600 | 173 430 |
certify_config_table, 5 islands at width 8 | 167 366 | 2 767 042 |
That second row is why this constant is 8 000 000 and not 2 000 000. The ceiling was first chosen
from the ALU bodies ALONE, and certify_config_table blasts a much larger obligation on the same
ceiling — a time-mux of every island against one of them, growing SUPERLINEARLY in the island count
(three islands cost 173 k, five cost 2.77 M). At 2 000 000 a long-standing proof
(fabric_whole_program_lock) began failing, which is what a ceiling calibrated from one workload
does to another.
So the budget clears the widest obligation that certifies today (the 5-island reconfig, 2.77 M) by
~2.9× and still refuses the third doubling block (3.5 × 10^8) by ~44×. There is deliberately no
ceiling that “just fits” a multiply chain: each doubling block multiplies the encoding by ~70, so
past the knee the only honest answer is a refusal BY NAME, and the band between a legitimate
obligation and a runaway is five orders of magnitude wide. The DAG is priced first
(BlastSize), so a refusal costs the DAG, never the tree. bitblast_budget_lock re-measures
every row of both tables, against the REAL corpus rather than a smaller stand-in.