Repository navigation
Buses and tags: correctness fixes, tests, documentation and release metadata for circomlib_buses - #149
Merged
Conversation
This was referenced Sep 18, 2026
OBrezhniev
force-pushed
the
fix/circomlib_buses_review
branch
from
September 29, 2026 18:39
b85175e to
7198ad7
Compare
Num2Bin and Num2BinNeg tagged their output bus {unique} unconditionally,
but instantiated AliasCheck only when n == maxbits(). For n > maxbits()
no alias check was emitted, so the constraints lc1 === in plus the
binariness checks admit several distinct bit vectors for the same value:
with n = 255 the bits of p and the bits of 0 both satisfy them. The tag
was therefore a claim the template did not enforce, and Bin2Num requires
that tag.
Assert n <= maxbits() so the oversized case is rejected at compile time,
and use >= in the alias-check condition so it is not the sole guard.
Constraint counts are unchanged for every accepted n (Num2Bin(254) is
still 507 non-linear constraints); Num2Bin(255) now fails to compile.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
MinValueCheck asserts ct >= 1 because CompConstant(_, ct-1) wraps ct = 0 to p-1, but MinMaxValueCheck has the same ct1-1 expression and was left without the guard. It does not always fail loudly: when nbits(ct2) is maxbits(), CompConstant's own assert passes and the template compiles into res1 === 1 with res1 = (in > p-1), which no input can satisfy. MinMaxValueCheck(0, 2**253) built 760 constraints and rejected every witness rather than reporting the bad parameter. Add the same assert MinValueCheck already has. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The comparison operand aux is tagged maxbit = nbits(2 * n), but the comparator was instantiated as LessEqThan(n), mixing the bound n with the bit width it needs. LessEqThan asserts in.maxbit <= n, so whenever nbits(2 * n) > n the template failed to compile: MaxAbsValueTagCheck(1) and MaxAbsValueTagCheck(2) both hit that assert. Instantiate it with needed_bits instead. Both now compile, and witness generation confirms the accepted set is exactly [-n, n] for n = 1, 2 and 5, with the first value outside the range rejected on either side. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… uses nsegments divided by 246 while every other part of the template treats a segment as 249 bits: nseg is 249, nlastsegment subtracts (nsegments-1)*249 and the inputs are read as e[s*249+i]. Over-counting the segments makes nlastsegment zero or negative, so the template failed to compile for n in 247..249, 493..498 and 747, with "Out of bounds exception" or "The size of the array is expected to be a usize". The 246 in the old comment guarded the segment size, which bounds the accumulator; that size is 249 here regardless of this divisor, which only decides how many segments are allocated. Dividing by 249 makes the count agree with the rest of the template. (n-1)\246 and (n-1)\249 differ only where the old form was already broken, so this is not a re-segmentation: over n in 1..12, 100, 245..255, 300, 492..500, 600, 747 and 750, every width that compiled before produces a byte-identical R1CS, and the seven that failed now compile. Their output matches babyjub.mulPointEscalar for k = 2**(n-1) - 12345. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
circuits/smt/smthash_mimc.circom includes ../mimc.circom, which this branch deleted, so the file can no longer compile. No circuit or test includes it; an include-graph scan over all 78 .circom files found it to be the only unresolved include. Removing it completes the MiMC removal already recorded in CHANGES.txt. circuits/bits.circom is included by nothing and defines a second nbits(), which is not a copy of the canonical one in bitify.circom: it returns 0 for input 0 where bitify returns 1, and it lacks the negative and overflow handling. Including both in one compilation unit is a hard error, T2008 Duplicated callable symbol, so the file is a trap rather than an unused helper. Every nbits() caller already resolves through bitify.circom. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The file had no direct coverage: only BinaryCheckArray and MaxbitCheckArray were reached, and then only incidentally through other templates' test wrappers. MinMaxValueCheck was exercised once, by babypbk_test, with ct1 = 1. Cover all eight templates with four wrapper circuits and one suite: values inside the bounds are accepted and returned unchanged, the bounds themselves are accepted, and values outside them make the constraints unsatisfiable. The wrappers assert the tag values too, since a tag is a compile time property and cannot be read from the witness. MaxAbsValueTagCheck is instantiated at n = 1 and n = 2, the widths where nbits(2 * n) exceeds n, and MinValueCheck(0) and MinMaxValueCheck(0, _) are checked to be rejected by the compiler, so the suite covers the two bugs fixed in ec01941 and dfb35d8. Checked against mutants: dropping the ct1 assert, restoring LessEqThan(n), widening MaxbitCheck to Num2Bits(n+1) and removing the MaxValueCheck upper bound each fail the suite. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
bitify_test.circom and eddsapedersen_old_test.circom compiled but no test file referenced them, so neither ever ran, and poseidon_old.circom had no test circuit at all. Between them, eddsapedersen_old.circom and poseidon_old.circom had no coverage whatsoever, the second despite a fix to its include recorded in CHANGES.txt. - bitify.js drives bitify_test.circom: Num2Bits(30) and Bits2Num(30) round trip, the largest 30 bit value is accepted, and 2**30 and p-1 are not. The wrapper now also outputs the bits, because its own in === aux2 constraint makes the round trip pass even when Num2Bits stops constraining lc1, so without the bits the test pinned nothing about the decomposition itself. - poseidonold.js drives two new wrappers for poseidon_old.circom, the unoptimized formulation, against the results already pinned for poseidon.circom in poseidoncircuit.js. Pointing its include at poseidon_constants.circom fails all four cases, so the test covers the include fix. - eddsapedersen.js now drives the old verifier with the same signature as the current one, and both get a tampered message case. The file had a single passing test, so wiring the old circuit up without a negative case would not have shown that either verifier constrains anything. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
circuits/README.md came from master untouched, so it still listed compconstant, eddsa, eddsamimc, eddsamimcsponge, mimc, mimcsponge, multiplexer and sign as if they existed, pointed at the old top level escalarmul paths, and described every surviving template by its pre-bus signature. Filling it in was not the answer either. Of its 76 template entries, 5 had a description and the rest were bare DESCRIPTION / SCHEMA / INPUT / OUTPUT / BENCHMARKS / EXAMPLE placeholders, 830 lines of which roughly 93% was empty scaffolding. Meanwhile this branch documents each template where it is defined, in a comment giving its inputs, its outputs and the tags on both, which is both richer than the README ever was and cannot drift from the code. So the file now says where the specifications are and indexes what exists: the tags and what each asserts, the buses, which files need BN254 and which work over any prime, and every file with the templates it provides. Checked mechanically, every template, function and bus named resolves to a definition, and every template defined is named. Nothing accurate was lost: the only prose in the old file was a writeup of BabyAdd, which babyjub.circom now carries in fuller form. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
main.circom declared inputs a and b but wired a into both operands, so the example hashed (a, a) and b never reached the witness. circom said as much, reporting "private inputs: 2 (1 belong to witness)", which now reads "private inputs: 2". The circuit is an example with its own main component rather than a library template, and test/circuits/sha256_2_test.circom is the same circuit wired correctly, so nothing depended on the old behaviour. Against Node's crypto for the 54 byte encoding the template uses, the output now matches sha256(a, b) for (1, 2), (3, 7) and (5, 5), and differs from sha256(a, a) wherever a and b differ. Constraint counts are unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Num2Bits_strict, Bits2Num_strict and Num2BitsNeg had no coverage. Num2BitsNeg in particular was changed on this branch, in 8a071de, while its binnum twin Num2BinNeg was the one that got the tests. Two wrappers and three suites: - Bits2Num_strict is fed bits directly, so the alias check can be exercised: the bits of values below p recompose to those values, and the bits of p itself and 254 ones are rejected. Removing that AliasCheck fails both cases, which settles the "Maybe remove?" left beside it: it is load bearing. - Num2BitsNeg is covered at n = 8, where 2**n is well below the prime and the result is plainly 2**n - in, and at n = 254, where 2**n reduces and the template negates against the reduced value instead. Reverting 8a071de fails the in = 0 case. One limit worth recording: Num2Bits_strict derives its bits from a field element that is already reduced, so its AliasCheck cannot fire on an honestly generated witness, and removing it leaves the suite green. Catching that needs a crafted witness rather than calculateWitness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD
Comments only, apart from one trailing comment removed from a line of code. Constraint counts are unchanged and the suite still passes. - Bits2Num_strict said its input was maxbits() + 1 bits, and its example claimed that, for p = 11, the bits of 11 recompose to 2. They do not recompose to anything: the AliasCheck rejects them, which is the point of the template. Replaced with an example of each outcome, and dropped the "Maybe remove?" beside that AliasCheck, since removing it fails two cases in test/bitify.js. - MontgomeryBabyCheck had no docstring, the only template in its file without one. Added, including the relationship to BabyCheck. - Bits2Point_Strict, Point2Bits_Strict and EdDSAPedersenVerifier still described 256 bit arrays. They take and return BinaryPoint(254) buses, which hold 255 bits. All three now say so, and EdDSAPedersenVerifier also records that S is a scalar rather than a point and only borrows the bus to carry 255 bits. - The three of them now also state the obligation that came with the bus: a BinaryPoint has no bit 254, so code converting a 256 bit wire encoding into one has to reject a non-zero bit 254 itself, or two encodings map to the same key. The circuit cannot check a signal it does not have, and nothing said whose job it was. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD
…mplete The header comment shared by babyjub.circom and montgomery.circom said that a = 168700 is not a square in the BN254 scalar field and that the curve is therefore a quadratic twist of x'^2 + y'^2 = 1 + d'*x'^2*y'^2. It has this backwards. sqrt(168700) exists: 7214280148105020021932206872019688659210616427216992810330019057549499971851 and squares back to 168700, so the map (x, y) -> (sqrt(a)*x, y) given there is an isomorphism, not a twist. Checked four ways: Euler's criterion, the Jacobi symbol by quadratic reciprocity, the product of Legendre symbols over the factorisation 2^2 * 5^2 * 7 * 241, and ffjavascript's F.sqrt. The map and the constant d' were already right; d' is d/a and matches the stated value exactly. The same fact settles a question the library never wrote down. d = 168696 is a non-square, so a is a square and d is not, and by the Bernstein-Lange criterion the twisted Edwards addition law is complete on this curve: neither denominator of BabyAdd can vanish for points on the curve. BabyAdd is therefore correct for any two points, including equal ones and the identity, which is why BabyDbl is BabyAdd(pin, pin). Recorded in its docstring, together with the contrast to MontgomeryAdd, whose law is incomplete. Verified against babyjub.addPoint for P + P, P + (-P), identity + identity, P + identity and (0,-1) + (0,-1). Comments only. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD
The previous CHANGES.txt named the removed files, the CompConstant parameter change, the EdDSAVerifier rename and a version requirement. It did not say that the move to buses and tags changes the interface of nearly every template. Measured against master with a parser over every template's ports at both refs (scratchpad/breaking_inventory.py): of 100 templates, 13 are removed, 31 have their ports reshaped (coordinate pairs and out[2] became Point buses, SMT state became a bus), 46 keep their ports but now require tags on 110 inputs, and 10 are untouched. Every fact in the old file is kept; the new one adds the full lists by class, the fixes on this branch, a known issue, and a migration section with before/after snippets for includes, buses, tags and the 255-bit point encoding. Two removals the old file did not mention are now listed: the non-strict Bits2Point() and Point2Bits(), and smt/smthash_mimc.circom. The version requirement is corrected. The old file said 2.1.5; buses were introduced in circom 2.2.0 (RELEASES.md, October 7, 2024), so that is the floor. The pragma lines in the sources are inconsistent and all below it: most say 2.1.5, seven SMT files say 2.1.9, four say 2.0.0. A pragma is a minimum the compiler checks against its own version, so none of them stops circom 2.1.x from failing on the bus syntax. The same wrong figure was in circuits/README.md, written earlier on this branch; fixed here. The pragmas themselves are left as they are: harmonising them, and the major version bump this release needs, are recorded as decisions in the review notes. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD
The move off hardcoded 254, (p-1)/2 and 252 to maxbits(), nbits() and -1 \ 2 made the bit-level templates usable on primes other than BN254: aliascheck, bitify, binnum, comparators (Sign and CompConstant included), tags-managing, binsum, binsub, gates, the muxes and Switcher. CHANGES.txt and circuits/README.md now say so, backed by compiling probe circuits for each group with circom -p bn128, bls12381 and goldilocks: AliasCheck takes 254, 255 and 64 inputs respectively and constraint counts scale with it. The curve templates, Pedersen and the EdDSA verifiers stay BN254-only, because they embed the Baby Jubjub curve or its subgroup order. Poseidon needs a warning rather than a tick. poseidon.circom and poseidon_old.circom say "any prime field", and Poseidon(2) does compile for all three primes with the same 243 constraints, but the round constants were generated for the 254-bit BN254 prime and the round numbers chosen for its security level. For another prime the constants are reduced modulo it and the circuit computes a function nobody has specified or analysed. Both documents now say to treat Poseidon, and the SMT circuits built on it, as BN254-only. The header comment in the two source files still makes the broad claim; changing upstream's wording is left for review. Also replaces the last hardcoded "254 bits" in bitify.circom, in the Num2Bits_strict docstring, with maxbits(). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD
poseidon.circom and poseidon_old.circom opened with "The templates and functions in this file are general and work for any prime field". The round structure is, and Poseidon(2) compiles for bn128, bls12381 and goldilocks with the same 243 constraints. But the round constants in poseidon_constants*.circom were generated by the grain script for the 254-bit BN254 prime, and the round numbers were chosen for that field's security level. Compiled for another prime the constants are reduced modulo it and the circuit computes a function with no specification and no security analysis, which the old header invited. Both headers now say the templates only work for bn128, in the form the curve files use, and explain what is field-agnostic and what is not. CHANGES.txt and circuits/README.md, which had described the old wording, are updated to match. Comments only; constraint counts unchanged (poseidon3_test and poseidon_old3_test 243, smtverifier10_test 4092). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD
The changelog documents a breaking release: 13 templates removed, 77 of the 87 remaining changing their interface, every include path under escalarmul/ moved, and a compiler floor of 2.2.0. That is a major version, and as the interfaces are still under review (seven side branches, two questions for upstream) it is a pre-release for now. npm version premajor --preid alpha, without npm's own commit and tag, so package.json and package-lock.json move together from 2.0.5 to 3.0.0-alpha.0. CHANGES.txt names the version instead of asking for one. Not in this commit: enforcing the circom floor from package.json and pinning the version CI installs, the remaining items under S8. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD
MinValueCheck(ct) tagged its output minvalue = ct after checking CompConstant(maxbits(), ct-1) on bits from a plain Num2Bits(maxbits()). That comparison is on the integer the bits encode, and without an alias check the bits do not determine the value: for x < 2**maxbits() - p the bits of x + p also satisfy Num2Bits(maxbits())(x). Modelling the template's exact constraints with prover-chosen bits, in = 0 with the bits of 0 + p was accepted and tagged minvalue = 7; with the honest bits of 0 it was rejected, which is why no test noticed. Adding the alias check rejects the aliased bits. This is the same root cause as the Sign issue on fix/aliascheck-unique-tag. The ">=" direction is the one an aliased decomposition helps: making a small value look large. The other value checks are unaffected: MaxValueCheck is monotone in the other direction, and MinMaxValueCheck uses nbits(ct2) bits, which can only reach maxbits() for ct2 >= 2**253, where the aliased bits then fail the upper bound because x + p > ct2 for any ct2 < p. BabyPbk requires both minvalue and maxvalue and the library's own wrapper obtains them from MinMaxValueCheck, so it was not exposed; a caller combining MinValueCheck with a separate MaxValueCheck would have been. MinValueCheck now decomposes with Num2Bits_strict, which includes the alias check: 253 constraints more per instantiation. Existing tests keep their expectations (7 and q-1 accepted, 6 and 0 rejected). The vulnerability itself is only demonstrable with a crafted witness, not through calculateWitness; the model used is scratchpad/mv/model.circom in the session notes. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD
OBrezhniev
force-pushed
the
fix/circomlib_buses_review
branch
from
September 29, 2026 20:08
7198ad7 to
d5f158d
Compare
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.
Review of the
circomlib_busesbranch: correctness fixes, tests, documentation and release metadata for the move to buses and tags. 22 commits on top ofcircomlib_busesat5013906; every commit is verified individually and the full suite passes at every step (118 tests at the tip, up from 82 on the base). Nothing here changes the design of the bus/tag conversion itself; design alternatives are in the stacked PRs listed at the end so each can be reviewed on its own.Correctness fixes
d5f158dMinValueCheck(ct)comparedCompConstant(maxbits(), ct-1)on bits from a plainNum2Bits(maxbits()), with no alias check, so for anyx < 2^254 − pthe bits ofx + psatisfied the decomposition and passed the comparison:in = 0could be tagged{minvalue = ct}. Now decomposes withNum2Bits_strict(+253 constraints per instantiation).MaxValueCheckandMinMaxValueCheckwere not affected (their upper bound rejects the aliased bits), nor wasBabyPbk, which takes its tags fromMinMaxValueCheck; a caller usingMinValueCheckalone was. Was #156; merged here after an independent security review flagged it.daa7618Num2Bin/Num2BinNeggranted{unique}for n >maxbits()with no alias check, so two bit vectors could stand for one value. Now asserted. Upstream has questioned this form ("take into account the tags"); the alternative — aNum2Bin_strictsplit likebitify's — is open for discussion.dba6a9fMinMaxValueCheck(0, ct2)compiled into an unsatisfiable circuit (ct1 - 1wrapped top - 1). Now rejected at compile time, asMinValueCheck(0)already was.aa13fd0MaxAbsValueTagCheck(n)passed the bound where a bit width was needed; failed to compile for n = 1, 2. Witness generation confirms the accepted set is exactly[-n, n].3d3f7b3EscalarMulFix(n)failed to compile for n = 247–249, 493–498, 747: the segment count used 246 while the segment size was 249. Byte-identical R1CS for every width that compiled before; outputs matchbabyjub.mulPointEscalarat the newly working widths.d8347fasha256/main.circomwired inputainto both operands ofSha256_2.ce59ecdsmt/smthash_mimc.circom(included the deletedmimc.circom; nothing used it) andbits.circom(a second, differentnbits(); including both was a hard error).Tests
tags-managing.circomhad no direct coverage (94f98f1, 16 cases, mutation-checked);Num2Bits_strict,Bits2Num_strict,Num2BitsNeghad none (2866183);bitify_test.circomandeddsapedersen_old_test.circomexisted but no test ran them, andposeidon_old.circomhad no test at all (c58bac1). The Pedersen EdDSA verifier gets tampered-signature cases. Where a test could not catch a regression, the commit message says so and why.Documentation
circuits/README.mdrewritten as an index (6bcc4ca): the previous file was 830 lines of which ~93% were emptyDESCRIPTION / SCHEMA / …placeholders, and it documented eight templates that no longer exist.f051627):Bits2Num_strict(input size, an example that the alias check rejects),MontgomeryBabyCheck(none),Bits2Point_Strict/Point2Bits_Strict/EdDSAPedersenVerifier(still described 256-bit arrays). The encoding obligation that moved to the caller withBinaryPoint(254)— check bit 254 is 0 — is now stated where it applies.babyjub.circom/montgomery.circomheader saida = 168700is not a square and the curve a quadratic twist. It is a square (sqrt(168700) = 7214280148105020021932206872019688659210616427216992810330019057549499971851), the map is an isomorphism, and by Bernstein–Lange the Edwards law is complete on Baby Jubjub;BabyAdd's docstring now says so (0042c0b).CHANGES.txtrewritten from a measured inventory of what breaks (f97ec42): of 100 templates inmaster, 13 removed, 31 with ports reshaped, 46 with the same ports but tags now required on 110 inputs, 10 untouched. Includes a migration section. Field generality documented and verified by compiling the generalised templates forbn128,bls12381andgoldilocks(3222441).One upstream wording this branch overwrites — please read as deliberate
Poseidon headers (
f9ac87a).poseidon.circomandposeidon_old.circomsaid "work for any prime field". The round structure does compile for other primes, but the constants were generated for BN254 and the round numbers chosen for its security level; compiled elsewhere the result is an unspecified function. The headers now say BN254-only and why.Release metadata
3.0.0-alpha.0(536e456): a breaking release by the inventory above, pre-release while the stacked PRs are open. Not done here: enforcing the circom floor frompackage.jsonand pinning the version CI installs (test.ymlinstallslatest).The
pragma circomlines are deliberately left exactly as they are oncircomlib_buses(2.0.0 / 2.1.0 / 2.1.5 / 2.1.9 by file);CHANGES.txtstates the real requirement, 2.2.0, and why. Whether to raise the pragmas is upstream's call.Stacked PRs
Each is based on this branch and shows only its own change. Two are mutually exclusive alternatives; the rest are independent. Full suite passes on every one. (#156, the
MinValueCheckfix, was one of these and is now merged into this branch, see the first row above.)AliasCheckgrantsunique,Signrequires it{binary}Point2Bits_Strictrequiresbabyedwardsbabysubgrouptag,EscalarMulAnyrequires itMontgomeryAdd(+11–17%)xdistincttag (+14)Num2BitsNeg/Num2BinNegrefuse n ≥ maxbits()Two questions for upstream without a PR: whether EdDSA should reject torsion-carrying public keys outright rather than cofactor-clear them, and whether
babyedwardsshould imply subgroup membership (it should not, for that reason).🤖 Generated with Claude Code
https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD