Support check for unconstrained allocation

[porcuquine]

Completely unconstrained allocations are a common source of programmer error, leading to soundness bugs, when writing circuits. This class of error can be completely detected at circuit-shape-synthesis-time.

Bellpepper already inherits (from bellperson/bellman) an error intended to signal this condition: https://github.com/lurk-lab/bellpepper/blob/542bf035ff544ef0bc4c69a010e76ca1ef19cb9b/crates/bellpepper-core/src/constraint_system.rs#L45-L47.

We should add support to check synthesized constraint systems for this — either at program run-time, or in tests. Ideally, this would be implemented such that there is no cost if the check is never performed.

Since there are legitimate reasons to allocate unconstrained values, we will need to add a new operation (say, AllocatedNum::alloc_unconstrained(…)), allowing circuit programmers to white-list such allocations. This will greatly improve clarity when this is actually desired, by forcing it to be declared explicitly.

When performing the optional check on a constraint system supporting it, unconstrained allocations that are declared as above should not result in an error. Conversely, declared unconstrained allocations that are in fact constrained should also result in an error. We will need a new error type for this.

The principle suggested here could be taken further, since constrained/unconstrained is a crude binary hammer. Consider that an AllocatedBit will be 'constrained' at the R1CS level, but may still represent a conceptually unconstrained allocation. Ideally, we could similarly catch such unconstrained (except for the booleanity constraint) AllocatedBits — with an equivalent whitelisted-allocation form.

Of course, this could get complicated and expensive. One possibility that might be viable in general is to include metadata during shape synthesis (when opting into a more expensive analysis mode) so that 'partial constraints' of the kind created by AllocatedBit on construction are recorded and can be ignored when attempting to determine whether a given variable has been fully constrained.

These checks should apply both to inputs and aux variables.

If we want this to be shared by many constraint systems, we might need some refactoring and common traits. In that case, Nova's ShapeCS, for example, should be considered.

---

The most obvious implementation approach would involve a set of all variables (or their indices), with variables removed from the set as they are encountered in (qualifying — if/when we implement that nuance) constraints. A bit field might be a reasonably performant way to instantiate the idea.

For example, a circuit with n constraints might have a field initialized to [0xFFu8; (n + 7) / 8]. Then as each constraint is encountered, the bit at position corresponding to its index is set to 0. If we also explicitly clear the bits corresponding to whitelisted vars, then any remaining non-zero bits correspond to unconstrained allocations which should be reported.

Or maybe that's overkill, and a simpler but heavier data structure will suffice.

---

As a final note, the existing error (which should be retained for compatibility by consumers who still use Groth16 with bellpepper) doesn't report which var was unconstrained — but it will be much more useful for debugging purposes to include it. So we may need a new error for this, as well as the constrained-but-whitelisted case (which should also report the offending variable).