feat: dialect to represent combinational circuits

[asraa]

Some programs may benefit from translation into a combinational circuit with logic gates that can then be optimized by tools (like Yosys).

These programs can eventually target FHE schemes that implement boolean logic / LUTs (such as TFHE).

In order to integrate combinational lgoic optimizations, we need a dialect or IR that can represent these programs, and then create passes that may invoke programs like ABC through Yosys to optimize gates.

The ops involved would be LUTs (perhaps with rewrite patterns that would be able to optimize these LUTs (related: google/fully-homomorphic-encryption#62 @johannesmono) or fix the LUTs to certain sizes) and boolean gates.

@j2kun

[asraa]

CIRCT has a comb dialect: https://circt.llvm.org/docs/Dialects/Comb/

[asraa]

WDYT about CIRCT as a dependency? IMO yes it's large, but I think it'd be great to re-use the existing comb dialect.

[j2kun]

I recall they were missing a LUT operation, but they seem to have added it recently: comb.truth_table (::circt::comb::TruthTableOp)

It is a big dependency... I'm just taking quick notes here to see what else they provide that would make the dependency worthwhile

• CombToArith and CombToLLVM passes, which don't seem particularly useful for us.
• A LowerComb pass with the single pattern TruthTableToMuxTree that seems designed to help with their ExportVerilog codegen that doesn't support LUTs (not sure why... we do it with shift operators).
• An analysis function that computes information about which bits are known to have specific values, which is currently only used in the icmp folder here
• Folders which seems to have the majority of the value as a bunch of canonicalizers, including:
  • Variadic operand flattening
  • Width narrowing
  • Constant folding
  • Canonicalizations for shift ops (shift by constant == extract bits + concat with zeroes), extract and concat and replicate interactions,
  • Some folds like this one that push ops involving constants to the op that created the non-constant operand
  • Check for duplicate idempotence
  • Basic equivalence folding for and/or/xor (none for the truth_table op, though)

The folding logic seems nice, but if we're planning to use an external optimizer, they don't provide us that much value since they would be unlikely to cover what the external optimizer doesn't cover.

IMO the two alternatives to consider are:

• Make a local clone of comb to avoid the dependency.
• Try to upstream comb into MLIR proper.

[j2kun]

I also noticed that the majority of their ops are variadic, and they take advantage of it by canonicalizing stuff like and(x, y, x) == and(x, y), and now I'm wondering what it would take to have such a canonicalization if you didn't have variadic ops. If And is commutative, maybe you'd use the commutative sorter upstream (but would that reorder arguments across ops if there are no intermediate uses of the values?). Or maybe traverse use-def chains to find out how x is used in earlier ops

[asraa]

CombToArith and CombToLLVM passes, which don't seem particularly useful for us.

They also have an ArithToComb, which would be pretty useful out of the box to us!

Make a local clone of comb to avoid the dependency.

So I have been successful at building just the Comb dialect (not the passes yet) using a custom BUILD file after cloning circt - so this is kind of the route I'm going.

We could also further simplify it, but if we're using the files as is, it's not too bad to filter for the relevant files and define our custom Bazel builds.

[j2kun]

Shruthi mentioned an interesting idea: would we have a use for the comb dialect besides CGGI? If not, and if CGGI is going to implement all the same binary gate + LUT ops as comb anyway, why not just translate the yosys output directly to CGGI?

[asraa]

Let's see, I was under the impression the Yosys pass would be used to optimize arithmetic circuits anyway using blackbox cells? (It can likely do that better than MLIR can). In that case, since the cells we chose for that would be reflected from the supported ops of the crypto dialect, perhaps that could really simplify it - the LUT/binary cell targets binary LWE / CGGI, while arithmetic targets other shortint schemes! We can frame the Yosys pass as an "optimize circuit for XYZ scheme" - and make it more like a lowering pass that performs optimizations rather than a rewrite. Makes sense? @code-perspective for feedback

EDIT: The one downside is that it would be nice to use the Yosys pass for other non-FHE things (like optmizing an MPC circuit) - the comb intermediate representation is nice for a non-opinionated representation. Something to consider...