Unsatisfied constraint feedback

[joss-aztec]

Problem

Presently when testing or debugging a complex circuit it is difficult to identify which constraints weren't satisfied for a given input. Working around this is cumbersome, and can involve commenting out large parts of the circuit to isolate the failed constraint.

This is the current feedback provided for a failed proof:

could not satisfy all constraints

Solution

Provide semantics for annotating constraints akin to an assert or require statement. The associated message should then be listed when proving fails. E.g.

require(x < 5, "x is too high");

could not satisfy all constraints:
  - x is too high

Alternatives considered

A simpler compromise would be to provide line numbers for the failed constraints. Note however this would insufficient when authoring failure case unit tests, which would want to test for a specific failure message.

[kevaundray]

Partially resolved by #1864, opened a separate issue for assert messages: #1939