pub const GATE_BUDGET_NODES: u64 = 2_000_000;Expand description
How large a SHARED GATE DAG the certificate path will pay to refute.
This is the ceiling that stays live once the obligation is built as a circuit rather than as a
tree. BLAST_BUDGET_NODES prices the ProofExpr TREE, which is the right question only for
a caller that materialises one; the gate path never does, so what it must bound is the number
of gates it allocates and Tseitin-encodes — both linear in the DAG. The RDU demo corpus’s
widest body (fib.lg’s six-block fast-doubling chain, 75 cells of chained 8-bit multiplies)
prices in the tens of thousands of gates once the grid and the spec are built as DAGs, so two
million is orders of magnitude of headroom over anything the product lowers today, and a body
past it is refused BY NAME in the time it takes to build the circuit — never by the allocator.
certifier_strength_lock re-measures both sides of that claim.