Test Constraints Rigorously

[aszepieniec]

One tiny oversight in the constraints constitutes a catastrophic security hole. It is imperative that the constrains be water-tight. This issue is about testing them to verify their correctness (soundness really).

Maybe some philosophy is in order: what other strategies are there that can help a) catch errors, and b) convince third parties of the code's correctness. Unit tests are obviously useful but can only get you so far.

Formal verification is an obvious candidate but seems like a rather extreme option for the quantity of work involved.

[jan-ferdinand]

I would argue that part of that effort is to make the code for the constraints more legible.

[Sword-Smith]

I definitely think the mathematical approach is the primary one: Having well-documented constraints defined.

Number two on that list could be a fuzzing: Make a pertubation in a specific column and check that the verifier fails. Do this in a loop over all columns.

[jan-ferdinand]

As @aszepieniec has pointed out, Gröbner basis analysis can help. Particularly, the constraints of all deterministic instructions (like add, but not divine) must have a single solution, which is easily verifiable given a Gröbner basis.