Poseidon2 constraints do not determine outputs

[matthiasgoergens]

See the code in https://github.com/0xmozak/mozak-vm/pull/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$$