//! 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))
//! `
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