Skip to content

BINIUS-347: stop computing wires the optimiser already dropped - #1908

Open
tcoratger wants to merge 1 commit into
binius-zk:mainfrom
tcoratger:thomascoratger/binius-347-stop-computing-wires-the-optimiser-already-dropped
Open

BINIUS-347: stop computing wires the optimiser already dropped#1908
tcoratger wants to merge 1 commit into
binius-zk:mainfrom
tcoratger:thomascoratger/binius-347-stop-computing-wires-the-optimiser-already-dropped

Conversation

@tcoratger

Copy link
Copy Markdown
Contributor

Closes BINIUS-347.

Two optimiser passes already delete redundant work from the constraints. The witness generator never heard about them, so every proof still computed values no constraint mentions. It does not any more — witness filling drops 21% on zklogin.

Also fixes a latent bug in the duplicate-collapsing pass that this change exposes.

The problem

Compiling a circuit produces two artifacts:

  • the constraints a proof checks,
  • the instructions that fill in the witness.

Two clean-up passes run before the constraints are emitted.
One collapses duplicated work, the other drops work nothing reads.

Both fed the constraints only.
The instruction stream never heard about either.

The committed statistics showed it in plain sight — gate count and instruction count equal to the digit:

keccak:  Number of gates: 22,189
         Number of evaluation instructions: 22,189

If anything were being skipped, those two numbers would differ.

The idea

Compute the dropped set once and hand it to both.

An assertion is the one exception.
It produces no value, so nothing reads it by definition.
Its instruction is the only thing that reports a failing witness, so it keeps running even when its constraint is redundant.

Worked example

t1 = a & b          <- read by t3
t2 = a & b          <- duplicate of t1
t3 = t1 ^ c         <- read by the assertion
t4 = a & c          <- nothing reads it
assert t3 == out

before:  constraints t1, t3, assert           -> 3
         instructions t1, t2, t3, t4, assert  -> 5

after:   constraints t1, t3, assert           -> 3   (unchanged)
         instructions t1, t3, assert          -> 3

A latent bug this exposes

The duplicate-collapsing pass rewrites every reader of a dropped value onto the surviving copy.
The early exit for hint gates sat before that rewrite rather than after it.

So a hint kept pointing at a wire whose defining gate no longer emits a constraint.

That is invisible today only because the dropped gate is still evaluated.
Stop evaluating it and the hint reads zero, and every circuit that divides or inverts fails to populate.

 for gate in gate_ids {
-    if matches!(graph.gate_data(gate).opcode, Opcode::Hint) { continue; }
-
     for wire in graph.gates[gate].wires.iter_mut() { /* canonicalise */ }
+
+    if matches!(graph.gate_data(gate).opcode, Opcode::Hint) { continue; }

Canonicalise every gate, then exclude hints from being collapse candidates.
That alone fixed 7 of the 12 remaining test failures, and has its own regression test.

What the existing tests revealed

Around forty tests build a circuit, leave the result neither asserted nor committed, then read an intermediate value back out of the witness.

Several passed for the wrong reason.
One asserts a sum and a carry are both zero, which any all-zero buffer satisfies, and its constraint check ran against a system holding no constraint about those wires.

Each now pins what it inspects, so the value is constrained rather than merely computed.

Soundness

Constraints, constants and the committed layout are untouched.
Only the instruction stream shrinks, and only by instructions writing values no constraint names.

The skipped set is closed under reading: any gate whose output a kept gate reads is itself kept, because the liveness pass marks the definer of every input of a live gate.

Scope

  • frontend: the dropped set is computed once and threaded into the evaluation form; the hint canonicalisation fix
  • circuits: test sites pin what they inspect; a point type gains a method to pin a curve point
  • examples: statistics snapshots refreshed, 11 of 13 changed

Verification

  • cargo check --workspace --all-targets — clean
  • clippy -p binius-frontend -p binius-circuits --all-targets --all-features -D warnings — clean
  • nightly fmt --all --check — clean
  • binius-frontend 159 tests, binius-circuits 320 tests — pass
  • all 13 circuit statistics snapshots re-blessed and re-checked

Benchmark

Instructions removed, from the snapshot diff:

circuit before after saved
blake3_compress 6,336 0 6,336 100.0%
zklogin 550,362 429,895 120,467 21.9%
ec_msm 246,270 226,510 19,760 8.0%
ethsign 252,550 232,559 19,991 7.9%
bitcoin_p2pkh 178,391 165,000 13,391 7.5%
bitcoin_headers 47,378 46,302 1,076 2.3%
hashsign 409,098 400,087 9,011 2.2%
blake3 7,624 7,520 104 1.4%
sha256 20,616 20,535 81 0.4%
keccak 22,189 22,107 82 0.4%
sha512 24,839 24,758 81 0.3%
total 1,765,653 1,575,273 190,380 10.8%

Wall time, measuring populate_wire_witness alone, with the two core files reverted in place for the baseline:

circuit before after change
sha256 354.91 us 354.10 us no change (p = 0.07)
zklogin 10.092 ms 7.9854 ms -20.9% (p = 0.00)

Time tracks instruction count almost exactly.

Hand-written hash gadgets are already tight, so they barely move.
The win is in large composed circuits, where redundancy accumulates in the seams between gadgets — and those are the circuits where witness generation costs real time.

blake3_compress reaching zero is not caused by this change: that example already had 0 AND constraints on main, since everything it computes is neither asserted nor committed. The change only makes its witness generation agree with its constraint system. Worth a follow-up to make that example prove something.

Benchmark source used to produce the timings

Not part of this change. Drop in as crates/examples/benches/witness_fill.rs, add a [[bench]] entry with harness = false, and run cargo bench --bench witness_fill -p binius-examples.

// Copyright 2026 The Binius Developers
//! Times witness filling alone, isolated from circuit construction and from the example's own
//! input preparation.
//!
//! Throwaway harness for measuring one change; not intended to be committed.

use binius_examples::{
	ExampleCircuit,
	circuits::{sha256::Sha256Example, zklogin::ZkLoginExample},
};
use binius_frontend::CircuitBuilder;
use clap::Parser;
use criterion::{Criterion, criterion_group, criterion_main};

/// Wraps an example's instance arguments so clap can supply their declared defaults.
#[derive(Parser)]
struct DefaultArgs<T: clap::Args> {
	#[command(flatten)]
	inner: T,
}

fn default_args<T: clap::Args>() -> T {
	DefaultArgs::<T>::parse_from(["bench"]).inner
}

/// Builds one example circuit, fills its inputs once, then times only the wire-witness pass.
fn bench_one<E: ExampleCircuit>(c: &mut Criterion, name: &str)
where
	E::Params: clap::Args,
	E::Instance: clap::Args + Clone,
{
	let mut builder = CircuitBuilder::new();
	let example = E::build(default_args::<E::Params>(), &mut builder).expect("circuit builds");
	let circuit = builder.build();

	// Input preparation is setup, not the measurement, so it happens once here.
	let mut filler = circuit.new_witness_filler();
	example
		.populate_witness(default_args::<E::Instance>(), &mut filler)
		.expect("inputs populate");

	// Filling is idempotent: it rewrites the constants and every derived value, leaving the
	// input rows alone. So one filler can be reused across iterations.
	circuit
		.populate_wire_witness(&mut filler)
		.expect("circuit is satisfiable");

	let mut group = c.benchmark_group("populate_wire_witness");
	group.bench_function(name, |b| {
		b.iter(|| circuit.populate_wire_witness(&mut filler).unwrap())
	});
	group.finish();
}

fn bench_witness_fill(c: &mut Criterion) {
	bench_one::<Sha256Example>(c, "sha256");
	bench_one::<ZkLoginExample>(c, "zklogin");
}

criterion_group!(benches, bench_witness_fill);
criterion_main!(benches);

🤖 Generated with Claude Code

Compiling a circuit produces two artifacts: the constraints a proof
checks, and the instructions that fill in the witness. Two clean-up
passes run before the constraints are emitted, one collapsing duplicated
work and one dropping work nothing reads. Both fed the constraints only,
so every proof still computed values no constraint mentions. The
committed statistics showed it: gate count and instruction count were
equal to the digit in every circuit.

The dropped set is now computed once and handed to both. Assertions are
the exception: one produces no value, so nothing reads it by definition,
and its instruction is what reports a failing witness.

This surfaces a bug in the duplicate-collapsing pass. It rewrites every
reader of a dropped value onto the surviving copy, but the early exit for
hint gates sat before that rewrite, so a hint kept pointing at a wire
whose defining gate no longer emits a constraint. That was invisible only
because the dropped gate was still evaluated. Canonicalising every gate's
wires before excluding hints from collapse fixes it.

Around forty tests built a circuit, left the result neither asserted nor
committed, then read an intermediate value. Several passed for the wrong
reason: one asserts a sum and carry are zero, which any all-zero buffer
satisfies. Each now pins what it inspects, so the value is constrained
rather than merely computed.

Constraints, constants and the committed layout are unchanged.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@tcoratger
tcoratger requested a review from jimpo as a code owner July 25, 2026 09:37

@jimpo jimpo left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, I don't think it's a good pattern to use force commit this much, even in the tests. It's really a hack to hint at better compilation, not something that should be so important.

The better pattern would be to make inout wires for the outputs and use assert_eq to bind the gate outputs to the inout wires. But it would be annoying to have to then separately compute the expected outputs just to assert_eq. Maybe we should add a mechanism like assign_inout, which takes an inout wire and a private wire, and copies the value to the inout and adds a linear constraint between them (with dst = inout wire).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants