Consensys / corset

4 stars 10 forks source link

Resolving Typing Issues around `and!`, `or`, `any` and `all!` #83

Open DavePearce opened 1 month ago

DavePearce commented 1 month ago

These functions accept variadic arguments, and place requirements on them. Specifically, that summing any two arguments cannot result in 0 unless they are all 0. In real terms, this means they should be "small" in some sense (e.g. u1, u8, etc). Unfortunately, the lack of type information given for the arguments of this functions represents a potential pitfall. Specifically:

There is no syntax for adding type information on arguments for variadic functions.
Even if such syntax existed, its not clear what type should be used to ensure overflow is impossible.

The latter point is especially true with field agnosticity. That's because the size of fields (hence the chance of overflow) is much increased.

DavePearce commented 1 month ago

NOTE: some of these functions are not actually used within the zkEVM constraints and could be removed.

DavePearce commented 1 month ago

Note also that this compiles without warnings / errors:

(module test)
(defcolumns (A :binary@loob) (B :binary@loob))
(defconstraint test () (if (+ A 1) B))