BINIUS-247: deduplicate the circuit interpreters via a shared execution-context trait#1753
Open
tcoratger wants to merge 2 commits into
Open
BINIUS-247: deduplicate the circuit interpreters via a shared execution-context trait#1753tcoratger wants to merge 2 commits into
tcoratger wants to merge 2 commits into
Conversation
…on-context trait The single-instance and batched circuit interpreters ran the same bytecode through the same ~40-opcode dispatch, every operation handler, and the same bytecode readers. All of it was written twice, differing only in where a decoded instruction reads and writes: one value vector versus one column per instance. Changing an opcode meant editing both copies identically or the two provers would silently disagree. Name the one thing that differs behind a small trait over the execution context: how many instances, read register r of instance i, write register r of instance i, note an assertion failure for instance i. Write the opcode logic once, as "for each instance, apply the operation". The single-instance interpreter becomes the degenerate case of one instance; the batched one is the many-column case. Both interpreters are now thin wrappers over the shared executor. Pure refactor, no behavior change: the assertion messages and blamed-instance index are byte-identical, and the batched-equals-single equivalence test is untouched and still passes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The exec module is private, so a private ancestor already gates external reachability; per CONTRIBUTING, prefer plain pub over pub(crate) in that case. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
Author
Just fixed the comment |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of BINIUS-247 — the second checklist item ("deduplicate
BatchInterpreterand the single-instanceInterpretervia a shared trait over the eval/execution context"). That issue has several bullet points; this is one of several PRs and does not close it.Merges the two circuit interpreters into one shared executor. Pure refactor — no behavior change.
The problem
A circuit is a little bytecode program:
ANDtwo words, shift one right by 7, assert two are equal. Something has to run it to fill in every wire value.There were two runners doing exactly that:
They did the same thing opcode for opcode. The ~40-branch dispatch, every operation handler, and the bytecode readers all existed twice — differing only in where a decoded instruction reads and writes.
That is a maintenance trap: touch one opcode and you must edit both copies identically, or the batched prover silently disagrees with the single-instance one.
The idea
Look at what actually differs between the two. It is tiny:
The operation logic is identical. Only "where do I read/write" differs.
So put that one difference behind a small trait over the execution context:
rof instancei?rof instancei?i?Then write the opcode logic once, as "for each instance
i, apply the operation". The single-instance interpreter is just the case where there is one instance.Per opcode
Take
AND dst, src1, src2.n_instances() == 1, so the loop runs once and reads/writes the lone value vector. The0..1loop inlines away.n_instances()is the column count, so the loop covers every instance.Same source line, both behaviors — chosen purely by which context is handed in.
The change
Soundness / behavior preservation
This is a pure refactor; two details are load-bearing and were kept identical:
The batched-machine-code path is unchanged (same monomorphization). The single-instance path gains a
0..1loop that the compiler elides.Scope
crates/frontend/src/compiler/eval_form/exec.rs— the shared trait and executor.interpreter.rsandbatch_interpreter.rsreduced to wrappers;mod.rsregisters the new module.Verification
cargo check -p binius-frontend --all-targets— cleancargo clippy -p binius-frontend --all-targets— cleancargo +nightly fmt --all -- --check— cleancargo test -p binius-frontend— 161 + 2 pass, including the batched-equals-single equivalence test and the assertion-path testscargo test -p binius-m4-prover value_table2— 9 pass (real-circuit batch witness generation, parallel stripes, failure diagnostics)Note:
cargo check --workspace --all-targetsfails onevaluate_batched_parallel(a rayon feature-unification quirk withinto_par_strides). This reproduces on a cleanmainand is unrelated to this change, so it is left alone here.🤖 Generated with Claude Code