Compile to Sunscreen FHE (BFV)

[cwgoes]

I had a nice chat with Ravital Solomon from Sunscreen.tech at EthDenver. They are building a compiler for the BFV FHE scheme (for now), which can be found here. As far as I understand from talking to Ravital and skimming the docs, Sunscreen solves problems orthogonal and complementary to the problems that VampIR and our compiler stack aim to solve - namely, their compiler takes a circuit, with add, multiply, and comparison operations (although with BFV it sounds like these may be expensive), and figures out how to choose all of the BFV-specific parameters in a way which makes sense for that circuit (sounds like this is a non-trivial problem), but they don't do any sort of higher-level compilation to circuits or optimisations of the circuit itself. Given that VampIR doesn't solve the FHE-specific parameter choice problems but does (along with Juvix) do all the higher-level compilation and circuit optimisations, it seems to me like they match up rather nicely.

In the long run, for practical feasibility the combination of a ZK proof system plus (possibly threshold) FHE would make sense for most applications, since ZKPs can handle the single-user private state much more cheaply (and they help out with some problems in just using FHE at all, such as verifiable re-encryption of data). Sunscreen does not yet implement any sort of BFV-compatible ZKP scheme, but it sounds like they're at least thinking about this problem, so we should also keep in touch about that.

For now, could we investigate what it would take for VampIR to support Sunscreen's compiler (and the BFV FHE scheme) as a backend? Just from looking at their interface, it seems like an integration would be pretty straightforward, although we'll also have to think about how this may change VampIR's interface (which at the moment assumes a ZKP system backend, e.g. prove & verify).