AztecProtocol
Confusion in constant-nonconstant branch of bigfield `assert_equal`
@zac-williamson left a TODO saying "wtf" here. Someone should follow up with this.
Interesting, I ran into the same problem with eccvm, I had to call self_reduce to make sure the non-constant value is not in the relaxed form because otherwise an assert equal that should be passing was failing. The assert equal was a check in sumcheck between a constant 0 and a non-constant 0
Discussed this with @Rumata888. TLDR: We think its best to keep the current code as it is.
So to assert a bigfield element $a$ is equal to bigfield element $b$, we need to check: $$(a - b) = 0 \textsf{ mod }p \implies (a - b) = q \cdot p$$ for some $q \in [0, 2^L)$ (i.e., $q$ is some positive integer that fits in a limb). When both $a, b$ are witnesses we check this equality using bigfield multiplication gate.
However, when $b$ is a circuit constant, we shouldn't need to perform any multiplication (ideally we should be able to check such an assertion without any additional gates). In that case we check $a_i - b_i = 0 \quad i \in {0,1,2,3 }$ for all its binary basis limbs and for the prime basis limb: $a_{\textsf{prime}} - b_{\textsf{prime}} = 0$.
Note that all of these constraints would only change the additive constants of $a$ and would not add any extra gates (as expected). One problem with these constraints is that these checks could lead to an honest prover being unable to generate satisfiable constraint(s).
Consider the case: $a = k \cdot p + m$ and $b = m \in [0, p)$. Note that $a = b \textsf{ mod }p$ so assert_equal should return true but the above condition(s) would not satisfy (limb-wise equality) and the prover would not be able to generate a proof. We would run into such a situation only if $a$ is unreduced (since bigfield witnesses are allowed to overflow).
Ideally the fix for this should be a boolean flag that is set to true when a bigfield witness is reduced. So whenever we run into this function, we always assert that the witness is reduced. However, adding this flag at this stage is likely to be risky (we might miss setting this flag in some places). So its best to leave it as is. I've expanded the existing comment to explain this. For now I am closing this issue, but link to this will remain in the codebase as a NOTE.
(Also, note that $b$ being a circuit constant can never exceed the modulus $p$ by design, but I am still adding a static assertion to check its always less than $p$.)
