Support low-level circuit formats for circuit compilers and optimisers

[HarryR]

In order to benefit from a wider range of tools and broaden horizons I think it's a good idea to support netlist formats - or formats that are easily parsable and usable as a zkSNARK circuit.

The ISCAS89 format is widely supported and similar to the Pinocchio output format.

Example files:

• https://github.com/squillero/itc99-poli/blob/master/i99t/b14/b14.bench
• http://web.eecs.umich.edu/~jhayes/iscas.restore/c2670/c2670.isc

Example tools:

• https://users.ics.aalto.fi/tjunttil/bcsat/
• http://www.cprover.org/ebmc/
• https://gitlab.com/securityengineering/CBMC-GC-2
• http://people.eecs.berkeley.edu/~alanmi/abc/abc.htm and https://github.com/berkeley-abc/abc - Convert AIGER, BLIF, BLIF-MV, PLA, Verilog to ISCAS (bench) format

However, CBMC-GC-2 is the most interesting, as it's specifically designed for MPC - converting a subset of C into ISCAS style gates.

CBMC-GC example format: https://gitlab.com/securityengineering/CBMC-GC-2/blob/master/examples/tutorial_addition/output.gate.txt

SFDL / SHDL example: https://github.com/tastyproject/tasty/blob/master/tasty/circuit/circuits/BNP08_FairplayMP2.1/Millionaires.sfdl.shdl

Other examples:

• https://www.sciencedirect.com/science/article/abs/pii/S2214212617306749
• http://www.cs.huji.ac.il/project/Fairplay/Fairplay/Fairplay.pdf (CBMC-GC can output to this format)
• https://thomaschneider.de/FairplayPF/
• http://www.cs.huji.ac.il/project/Fairplay/FairplayMP/SFDL2.0.pdf
• https://github.com/FaiplayMP/FairplayMP
• https://github.com/tastyproject/tasty
• https://github.com/encryptogroup/tasty
• https://github.com/esonghori/TinyGarble

Potential high level languages:

• xjsnark (custom high-level language)
• Pinocchio (C subset)
• Fairplay (custom high-level language)
  • https://github.com/ciphron/sfdl_to_scdl
• SCDL
  • https://github.com/ciphron/scdl/blob/master/scdl.pdf
• CBMC-GC (C subset)
• TinyGarble (Verilog)
• Python
  • https://github.com/ciphron/scdf
• Pequin

Potential low-level languages:

• Simple Circuit Description Language (from Verilog via TinyGarble)
  • http://ciphron.netsoc.ie/projects/scdl.html
• jsnark / Pinocchio output format (work-in-progress)
• CBMC-GC output format

[HarryR]

I am giving up on Pinocchio, it's interesting as a quaint proof of concept, but has little further value.

However, further work should be done to support the Pinocchio style circuit format used by jsnark and xjsnark as they'e far more promising.

Furthermore, I'm working on a translated from SHDL (compiled from SFDL via the FairPlay compiler)

And working on integrating CBMC-GC-2

[HarryR]

https://practice-project.eu/downloads/publications/D22.1-State-of-the-art-analysis-PU-V1.1.pdf provides a good overview of different high-level languages and compilers for secure function evaluation.

[HarryR]

Other interesting projects:

• https://github.com/kyroy/VerifiableStatementCompiler
• https://github.com/lightning-li/blockchain-knife/blob/4e0a5049d7b989d5ede4947abfee04908506a85a/zksnark/code_to_r1cs.py
• https://github.com/pepper-project/pepper/blob/de725f298ae04f50dd9c481aab8eb5774e2116d4/compiler/backend/zcc_parser.py
• https://github.com/ntfc/cf-homomorphic-mac/tree/0d8dfeea76e97376c92bca63a4a5183aa6447fe3/src

[HarryR]

https://github.com/ZcashFoundation/GrantProposals-2018Q2/issues/33 is also related and contains many relevant resources