Possible Bug: Miss constraint

[autoDetector]

Vulnerable File: circuits/aes-gcm/ghash_gmul.circom
commit: 65f823fc5606fca74440fb0de939ae07a3c39a80

Wrong reduction condition in Mulx

For the right-shift GHASH algorithm, the reduction by the irreducible polynomial must be conditioned on the LSB of V before the shift, not the MSB. Your Mulx uses mux.s <== blockRightShift.msb, which applies the 0xE1 reduction when the MSB is 1. This yields a different field multiplication than GHASH (x^128 + x^7 + x^2 + x + 1) and will accept invalid values if this is used to verify AES-GCM/GMAC computations.
Fix: drive the selector with the pre-shift LSB of V; i.e., use lsb(V) as the condition when doing a right shift with R = 0xE1 in the most significant byte. Alternatively, switch to the left-shift variant with MSB gating and R = 0x87 at the least-significant byte.