Poseidon2 constraints do not determine outputs

[matthiasgoergens]

See the code in #1304 and run this test:

cargo test --package mozak-circuits --lib -- poseidon2::stark::tests::poseidon2_constraints --exact --nocapture

Our Poseidon2 constraints can't tell whether the prover gave you the canonical byte representation of the digest or not. I'm not sure whether that's a problem.

To elaborate:

1. hash(a) == hash(b) implies a == b.
2. but a == b does not imply hash(a) == hash(b).

In our system so far we are only relying on property (1). But property (2) not holding is very counterintuitive and might catch unaware users off guard.

[codeblooded1729]

Here is one way we can go about ensuring canonical representation. Let $(l_{low}, l_{high})$ be representation of $l$ with $32$ bit limbs.
let $p = 2^{64} - 2^{32} + 1$ be goldilocks prime.
Idea is that if $2^{32} l_{high} + l_{low} \ge p \iff l_{high} = 2^{32} - 1 \land l_{low} > 0$
So $l$ is in canonical form means that either $l_{high} < 2^{32} - 1$ or $l_{low} = 0$.
To ensure the first constraint, we can have additional column to store the inverse of gap, say $gap_{inv}$
The final constraint would be
$$(1 - (2^{32} - 1 - l_{high})gap_{inv})l_{low} = 0$$