Skip to content

Conversation

@Forostovec
Copy link

The problem:
We only checked the Boolean value of the sum of the operation flags (is_add + is_sub + is_mul + is_div), rather than each flag individually. This allowed the prover to set a non-strict one-hot set of flags: for example, to make is_add = a, is_sub = 1 - a when is_real = 1, that is, to activate two flags at once in a linear combination, which violates the semantics of “exactly one operation performed” and could simultaneously attach several when(...) constraints on the same in1/in2/out.

The solution:
Explicitly assert the Boolean value of each flag and separately check that the sum of the flags is Boolean. As a result, in a real string, exactly one flag is equal to 1, while in padding, all flags are equal to 0; the behavior now corresponds to the intended one-hot logic.

@tamirhemo
Copy link
Contributor

Thanks for the PR! if you have multiple values that are non zero the constraint will actually fail because of the multiple assertions on the input below. Your version does make it a bit more explicit. We could consider this change when making the next major version upgrade.

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