halo2_gadgets::poseidon: Fix loading of padding words.

[therealyingtong]

Previously, a padding word was first assigned to a fixed column
using assign_fixed(), then copied to the state advice column using
copy_advice(). However, since the prover ignores fixed assignments
during synthesis, the value passed to copy_advice is None.

This causes the odd-length input to pass the MockProver, but fail
in real proof generation with a Synthesis error.

[daira]

utACK

[parazyd]

Any plans to merge this?

[str4d]

This breaks compatibility with existing circuits, because the constants move from being assigned in the rc_b column to being assigned in the circuit-global constant space.

Instead, we should revert the change made in 65a89f0#diff-81e1b63d3841ada245a37c0d485d03d48fb2d477a946e5135ba4602eb0e7e6f4 and manually call assign_advice and constrain_equal, which would avoid this problem because we can pass Value::known into assign_advice.

[str4d]

Separately, @therealyingtong and I discussed in Office Hours how to fix this in general. The core problem is that AssignedCell::copy_advice (correctly) propagates Value::unknown, but assign_fixed isn't propagating the fact that it was called with Value::known to the AssignedCell it returns.

The simplest fix would be to always evaluate to inside assign_fixed, but that would result in significant proving performance regressions for existing circuits (as this bug in question meant that you just couldn't write circuits that way, i.e. it failed safe). Ideally we could use memoization to remember to until the first time we need to evaluate it, then evaluate once, and remember the result going forward. We tried that approach and ran into both interior mutability needs, and object safety / lifetime issues related to the RegionLayouter trait.

[daira]

Wouldn't it be sufficient just to make sure that the MockProver fails in the same way as the real prover?

[therealyingtong]

Force-pushed to revert 65a89f0.

[str4d]

ACK f4293c2. I confirmed that this does not change the Orchard circuit (as expected, because we still call assign_advice followed by constrain_equal with the same cell relationships).

[daira]

Post-hoc utACK f4293c2.

Nit: the message of the second commit is "Revert commit 65a89f0", but it is not a full reversion, it reverts just the change to load_input_word inside Pow5Chip::add_input. It's fine, but in general we should be careful that commit messages are accurate especially for circuit changes.