"Full debug" constraints

[OlivierBBB]

It is currently not possible, AFAIK, to specify constraints that are "full debug" e.g.

(defconstraint    sanity-check-constraints    (:guard    (bla))
                  (begin
                    (debug    (is-binary    (shorthand-1)))
                    (debug    (is-binary    (shorthand-2)))
                    (debug    (vanishes!    (shorthand-3)))
                    (debug    (eq!          (shorthand-4)
                                            (shorthand-5)))
                    ))

The above (or similar) will produce e.g.

Error: compiling hub/constraints/instruction-handling/call/precompiles/common/generalities.lisp

Caused by:
    0: at line 56: (begin...
    1: expected at least 1 argument, but received 0
make: *** [zkevm.bin] Error 1

There is a workaround in the form of adding, e.g.

                  (begin
                    (vanishes!    0)
                    ...

Question: We discussed this back in the day and what I recall is that this is a safety feature, maybe to prevent constraints being quietly ignored. On the other hand it would seem interesting to allow for this feature (or something similar), e.g. by having a (debug-constraint ...) or (sanity-check ...) primitive that sets everything in debug mode by default.

• Is there any interest in this feature
• Is it easily doable ?

[DavePearce]

Hey Olivier,

(debug-constraint ...)

This is what I call a "property assertion". A property which we expect to be true for any valid trace, but which is not translated into actual constraints. The CorsetVerifier supports these as does the go-corset tool. So, there is definitely interest from my side, as these properties are things which can be e.g. checked using formal verification (and also testing).