Generalize lookups to set inclusion constraints

[vlasin]

After the discussion in #252, we arrived at the idea that ArithmeticCircuit is an intermediate representation of the computation that should allow an unrestricted ability to create polynomial, lookup, and fold constraints. If a particular proving system (e.g., Plonk) does not support a certain type of constraints, we convert them to the supported form during the protocol setup computation.

Given the above, we want to generalize the current lookup constraints to the inclusion checks:

$$ (x_1, \dots, x_{k}) \in T $$

Translating this to Haskell, we probably want T to be represented by Map and the tuple of variables to be a functor. We do not restrict the number of such sets T to be used in the same ArithmeticCircuit.

• Refactor ArithmeticCircuit type, replacing acRange field
• Refactor MonadCircuit and its instances

[TurtlePU]

during the protocol setup computation

Are we sure about this? Conversion will need access to quite low-level circuit APIs, doing this on the compilation stage seemed most reasonable.

Also this would help to keep protocol code dedicated to cryptography stuff only

[vlasin]

Well, I believe the conversion to the proof protocol format is a separate step. The workflow probably should go like this:

1. Compile the function to the IR of ArithmeticCircuit
2. Post-compile optimization (as a general rule, we want to optimize as we go, but it might not be always possible)
3. Convert to a proof protocol format
4. Protocol-specific optimizations (?)

So, we can wrap all 4 steps in a compile function whose output is a prepared setup of a specific protocol. But we should also have "internal" compile that only produces "ArithmeticCircuit". The latter, for example, is useful in IVC.

[TurtlePU]

To fix it in text somewhere: the current problem is that we have to describe $T$ effectively in order to be able to use it as a key in some "acLookup" map.

For compact lookup table descriptions, I propose to use the following GADT:

-- | @LookupTable a f@ is a type of compact lookup table descriptions using ideas from relational algebra.
-- @a@ is a base field type, @f@ is a functor such that @f a@ is a type whose subset this lookup table describes.
data LookupTable a f where
  -- | @Ranges@ describes a set of disjoint intervals on the base field.
  Ranges :: Set (a, a) -> LookupTable a Par1
  -- | @Product t u@ is a cartesian product of tables @t@ and @u@.
  Product :: LookupTable a f -> LookupTable a g -> LookupTable a (f :*: g)
  -- | @Plot f x@ is a plot of a function @f@ with @x@ as a domain.
  Plot :: FunctionId (f a -> g a) -> LookupTable a f -> LookupTable a (f :*: g)

Now, on the topic of function ids. I didn't find any way to easily serialize a Haskell function (maybe @zlonast can help?), so for now I came up with the following addition to the MonadCircuit interface:

class Monad m => MonadCircuit v a w m where
  ...
  registerFunction :: (forall x. ResidueField a x => f x -> g x) -> m (FunctionId (f a -> g a))

This uses the same trick as vertex generation -- choose x to be a MerkleHash and you would get the id which you can use to also store the function inside the circuit.

P.S. Note that if we had some simpler technique to get some kind of function ids / some similar DSL for description of functions, we could let f be just a type instead of a functor.

P.P.S. I mean we could go with foreign function pointers, but I don't know whether this would work ok