Skip to content
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

Implement bitwise And and Or in terms of XOR #544

Open
matthiasgoergens opened this issue Nov 4, 2024 · 0 comments
Open

Implement bitwise And and Or in terms of XOR #544

matthiasgoergens opened this issue Nov 4, 2024 · 0 comments

Comments

@matthiasgoergens
Copy link
Collaborator

Currently we have separate lookup tables for all three logical operations. But we can implement all three operations in terms of one of them, eg XOR.

From https://github.com/0xmozak/mozak-vm/blob/main/circuits/src/cpu/bitwise.rs

 //! This module implements constraints for bitwise operations, AND, OR, and XOR.
 //! We assume XOR is implemented directly as a cross-table lookup.
 //! AND and OR are implemented as a combination of XOR and field element
 //! arithmetic.
 //!
 //!
 //! We use two basic identities to implement AND, and OR:
 //! `
 //!  a | b = (a ^ b) + (a & b)
 //!  a + b = (a ^ b) + 2 * (a & b)
 //! `
 //! The identities might seem a bit mysterious at first, but contemplating
 //! a half-adder circuit should make them clear.
 //! Note that these identities work for any `u32` numbers `a` and `b`.
 //!
 //! Re-arranging and substituting yields:
 //! `
 //!  x & y := (x + y - (x ^ y)) / 2
 //!  x | y := (x + y + (x ^ y)) / 2
 //! `
 //! Or, without division:
 //! `
 //!  2 * (x & y) := (x + y - (x ^ y))
 //!  2 * (x | y) := (x + y + (x ^ y))
 //! `
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

No branches or pull requests

1 participant