Bugfixes: R1CS lowering (includes a soundness bugfix) #124
Conversation
This file contains 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
Fixes 4 bugs in R1CS lowering: * division-by-zero in finite fields: previously, this always caused incompleteness. Now, the behavior depends on the CIRC_RELAXATION envvar: * CIRC_RELAXATION=incomplete: divide-by-0 causes incompletenes * CIRC_RELAXATION=nondet: divide-by-0 allows the output to take any value * CIRC_RELAXATION=det: divide-by-0 forces the output to 0 * bit-vector overshift: previously, this cause incompleteness. Now, we follow the semantics of SMT-LIB (the result saturates). * bit-vector udiv-by-zero: previously, the output value was an unconstrained bit-vector. Now, it is MAX (following SMT-LIB). * bit-vector comparisons: previously, the prover could lie, claiming that x < y when actually x >= y. All bit-vector comparisons are affected, including those in udiv and urem. * soundness bug!
alex-ozdemir
added a commit
that referenced
this pull request
Dec 20, 2022
This reverts commit 05b793d. Right now Z#'s represents field comparisons and remainders using 255-bit bit-vectors. Our field-blaster is not intended to be correct or sound for bit-vectors that are this wide. Previously, a bug in the field-blaster essentially allowed compilation and proving to succeed anyway. With the (reverted) bugfix, the field-blaster crashes. Ultimately, we want Z# to handle these operations using range-checks---not bit-vectors. So, I'm reverting the bugfix for now.
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.
Fixes 4 bugs in R1CS lowering: