Simplify handling of user command failures in the transaction snark

[mrmr1993]

The current testnet uncovered a bug in one of the edge cases around handling user command failures, where we mispredicted a failure and generated an incorrect witness for the transaction snark. It would be good to simplify this handling.

The idea in brief:

• consume a User_command_status.Failure.t option as part of the proof
  • this is already generated by the transaction logic, so we can just plug it in
• if there is no failure, ensure that all of the checks succeed
• if there is a failure, ensure that that failure matches in the snark
  • for all other failure checks, we allow them to either pass or fail
  • this will remove the awkward prediction logic that we currently do to work out each possible check's state in advance

The truth table we want to match is (impossible fields, where a failure is predicted but the 'any failure' bit is not also set, are marked with an X)

Predicted failure (P)	Actual failure (A)	Any failure (S)	May build proof
0	0	0	1
0	0	1	1
0	1	0	0
0	1	1	1
1	0	0	X
1	0	1	0
1	1	0	X
1	1	1	1

Modelling as a rank-1 constraint, we get

(aP + bA + cS + d) * (eP + fA + gS + h) = (wP + xA + yS + z)

Substituting in our desired values

P=0, A=0, S=0 => d * h = z
P=0, A=0, S=1 => (c + d) * (g + h) = (y + z)
P=0, A=1, S=1 => (b + c + d) * (f + g + h) = (x + y + z)
P=1, A=1, S=1 => (a + b + c + d) * (e + f + g + h) = (w + x + y + z)

P=0, A=1, S=0 => (b + d) * (f + h) != (x + z)
P=1, A=0, S=1 => (a + c + d) * (e + g + h) != (w + y + z)

The trivial solution (including a constant term, which can probably be erased, but leaving in the interest of writing this up quickly) is to set all the constants on the left-hand side to 1, which gives

1*1 = z => z = 1
2*2 = y + z = > y = 4-1 = 3
3*3 = x + y + z => x = 9-4 = 5
4*4 = w + x + y + z => w = 16-9 = 7

2*2 != x + z = 5+1 = 6
3*3 != w + y + z = 7+3+1 = 11

By using this constraint instead of our current setup, we can use the system above where we only have to correctly predict that there are no failure conditions, or identify a single failing condition. The logic here is fairly trivial, but hopefully will save us any future headaches about pre-guessing the state of all failures in the snark for given transactions.

[mrmr1993]

Plugging in as above, but with d = h = 0, we get similar with the constant terms erased:

0*0 = z => z = 0
1*1 = y + z = > y = 1-0 = 1
2*2 = x + y + z => x = 4-1 = 3
3*3 = w + x + y + z => w = 9-4 = 5

1*1 != x + z = 3+0 = 3
2*2 != w + y + z = 5+1+0 = 6

This gives us a rank-1 constraint that we can drop in:

(P + A + S) * (P + A + S) = (5P + 3A + S)