Given a word size W, construct an arithmetic circuit which verifies the bitwise AND operation on W-bit words. You may assume that W is a positive integer multiple of 8. Your circuit should work in practice when W = 8 and when W = 16. Your circuit should be over a finite field F such that |F| > 2^W. A word should be encoded as a single field element. The circuit verifies knowledge of words A, B such that A AND B = C for public input C.
You should follow the strategy outlined in the Arya paper (https://eprint.iacr.org/2018/380.pdf). Here's how that works. See page 25 of the paper for more detail.
You need a one-column lookup table, call it EvenBits, which contains the field element encodings of all words of length W which have zero at all odd bit positions. This lookup table will have 2^(W/2) rows.
You need to decompose A, B, and C into their even and odd bits. A_e, A_o, B_e, B_o, C_e, C_o are each field elements encoding words of size W with zero at all odd bit positions. The following constraints express that these are the decompositions of A, B, C into their even and odd bits:
A = A_e + 2A_o
B = B_e + 2B_o
C = C_e + 2C_o
A_e, A_o, B_e, B_o, C_e, C_o ∈ EvenBits
Additionally, we need variables O_o, O_e, E_o, E_e, and the following constraints which express that O = O_e + 2O_o and E = E_e + 2E_o each contain in their odd bits half of the bits of A AND B:
A_o + B_o = 2O_o + O_e
A_e + B_e = 2E_o + E_e
Given that these constraints hold, the following additional constraint expresses that C = A AND B:
C = 2O_o + E_o
Using this strategy, implement the circuit and property test it for W = 8 and W = 16.
This strategy can also be modified to compute XOR, simply by taking the even bits of O and E instead of the odd:
Given a word size W, construct an arithmetic circuit which verifies the bitwise AND operation on W-bit words. You may assume that W is a positive integer multiple of 8. Your circuit should work in practice when W = 8 and when W = 16. Your circuit should be over a finite field F such that |F| > 2^W. A word should be encoded as a single field element. The circuit verifies knowledge of words A, B such that A AND B = C for public input C.
You should follow the strategy outlined in the Arya paper (https://eprint.iacr.org/2018/380.pdf). Here's how that works. See page 25 of the paper for more detail.
You need a one-column lookup table, call it EvenBits, which contains the field element encodings of all words of length W which have zero at all odd bit positions. This lookup table will have 2^(W/2) rows.
You need to decompose A, B, and C into their even and odd bits. A_e, A_o, B_e, B_o, C_e, C_o are each field elements encoding words of size W with zero at all odd bit positions. The following constraints express that these are the decompositions of A, B, C into their even and odd bits:
A = A_e + 2A_o B = B_e + 2B_o C = C_e + 2C_o A_e, A_o, B_e, B_o, C_e, C_o ∈ EvenBits
Additionally, we need variables O_o, O_e, E_o, E_e, and the following constraints which express that O = O_e + 2O_o and E = E_e + 2E_o each contain in their odd bits half of the bits of A AND B:
A_o + B_o = 2O_o + O_e A_e + B_e = 2E_o + E_e
Given that these constraints hold, the following additional constraint expresses that C = A AND B:
C = 2O_o + E_o
Using this strategy, implement the circuit and property test it for W = 8 and W = 16.
This strategy can also be modified to compute XOR, simply by taking the even bits of O and E instead of the odd:
C = 2O_e + E_e