-
Notifications
You must be signed in to change notification settings - Fork 5
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
ZIR-194: Fix and test BigInt type inference #45
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for walking me through the details!
Might want to add a couple notes to help clarify:
- where to look to cross-reference the test logic & the algorithm that encodes that logic
- the subtleties around normalization we discussed
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Awesome work. I love the new tests for the dialect, they're basically executable documentation! If you haven't already, it would probably be good to create an issue to track the Circom tests you turned off 😄
I'm going to wait for risc0/risc0#2413 to be approved before landing this, as otherwise we won't be able to bootstrap bigint into risc0 while this is landed and risc0/risc0#2413 is outstanding. |
There's an unsigned commit snuck in the middle, so I'm rebasing to get everything signed. |
de3875a
to
bcd6f2f
Compare
Fix mul coefficients used calculation
(they should produce the exact same shapes, so stick them in the same tests
(was previously using log2Ceil on an integer division, causing incorrect flooring prior to the ceiling)
This clarifies what it calculates, and in every case it's used that's what we want anyway
There's an edge case where the MulOp maxPos or maxNeg values could overflow 64 bits, which might cause the value to wrap to something that incorrectly passes BigInt type validation. Adjust this so the calculation stays large enough to fail validation, but doesn't overflow
4d75819
to
9e23be2
Compare
Make a number of fixes to BigInt dialect type inference. The bulk of the work is in the corresponding zirgen PR: risc0/zirgen#45.
This fixes a number of problems in the type inference for BigInts in calculating the number of coefficients, their maximum positive & negative values, and their minimum bits. It also adds lit tests verifying these properties. For the lit tests, I manually computed the output types without looking at the algorithms to give some redundancy.
Also adds a verifier to the BigInt type enforcing:
Makes the design decision that
minBits
should only be set if we know the number is positive, i.e. so that it is at least2^minBits
. Negative numbers don't count, even if we know they are large in absolute value.I also stuck a rename into this PR since this forces a rebuild of all the BigInt files anyway -- the existing
nondet_invmod
vsinv
vsModularInvOp
vsNondetInvModOp
was confusing even me, and since we're in integers there's no real need to specify it's a modular inverse: here's no other sensible multiplicative inverse. The new names arenondet_inv
(nondet) andinv
(checked) (and corresponding variants, e.g.NondetInvOp
andInvOp
).This could also be divided up as 3 PRs (one for BigInt type inference, one for the BigInt type verifier, and one for the renames of the inversion operations). I thought in this case it made more sense to unify them (in particular because that lets me make a single companion PR on the
risc0
repo), but if we want to split them it would be straightforward as the commits are fairly clearly separated.