![](https://i.imgur.com/WeIvTiX.png =150x) **Home Edition** # Discussion notes #9.2: zkInterface, a Tool for Zero Knowledge Interoperability Presenter: Aurelien Nicolas and Eran Tromer Authors: - Daniel Benarroch - Kobi Gurkan - Ron Kahat - Aurel Nicolas - Eran Tromer To be presented on 2020-05-18. Resources: * [Latest PDF version](https://docs.zkproof.org/pages/standards/accepted-workshop3/proposal-zkinterface.pdf) * [Miro Whiteboard](https://zkproof.org/workshop3-board) * [SoK Working Group](https://community.zkproof.org/g/WG_ZKINTERFACE) * [Additional related links](https://hackmd.io/@HtwXZr-PTFCniCs7fWFSmQ/B1AwbdI_8) ---- ## Real-time notes _Note taker: <mary maller>_. > Others are welcome to augment/annotate using notes. Add your name. ---OtherName Problem statement: Want to separate the backends and front ends of designing zero-knowledge proofs to allow for more modular constructions: Decide on instance and witness formats Witness reduction techniques to variable assignments gadgets interoperability. Require interoperatbility across frontend frameworks and PL. Gadgets should be usable by different frontends and backends. Ideally avoid high overhead. Expose details of the backends interface. Ideally support numerous styles of constraint systems. Where we are right now: zkinterface currently R1CS how are messages serialised. Recommendations for implementation Some adapters Demo: zokrates and bulletproofs Some adapters already exist Current proposal: beyond R1CS e.g. arithmetic and boolean circuites, custom gates, uniformity multi-part proofs deployment and execution more adapters Out of scope: SNARK-adjacent primitives e.g. accumulate and prove, commit and prove Backend interoperability: curve, scheme, bit pattern Programming language and frontend Typing New use case: DARPA SIEVE: Make zk useful for more complicated statements e.g. proving security of an implementation DARPA are funding many groups to produce front ends and backends Require us to accomodate backends other than QAP/ R1CS Suggested flow (simple case): We have a front end that knows about a statement, and a backend that knows about cryptography communicate by sending messages 2 phases: 1 describe circuit, 2 generate witness + proof Suggested flow (complicated case): Front ends to communicate Want to allow gadgets as input to a larger constraint system Have a front end, gadgets and a backend front end sends constraint system and assignment front end can ask gadget to generate constraints and assigments for certain tasks Message format: Memory layout format Supports highly optimised settings Need: Other constraint system styles: arithmetic/boolean circuits bounded fan-in, maybe smaller fields native to garbled circuits and MPC schemes could make an automatic converter multipart proofs i.e. two different proving systems combined together polynomial constraints and custom gates arithmetic representations can exploit uniformity in circuits using low-degree polynomials allow fallbacks to go back to r1cs if helpful for interoperability QUESTIONS: Riad: Should the front end be responsible for choosing the assignment? Might there be some other computation? Eran: Don't know current system that can talk in terms of variable assignments. Bundling instance reduction and witness reduction into the same thing. Daira: Want to preserve information about circuit so that you know which custom gate to use. Don't want to compile the high level gadget too early so that the backend has to undo and optimise. Eran: This is why we need to maintain some generality. Muthu: For really large statements memory will be the bottleneck and you want something on the fly. Have you thought about this with respect to the interface? For smaller statements you want to optimise and tailor make your system. How do you do both. Aurel: A streaming mode is supported, where you can send your witness chunks a piece at a time. We are more concerned about large statements, but the format is compact. Muthu: It seems you are restricting the way in which the front end and back end communicate. Is the way in which you are doing this restricted? Eran: We are optimising to make it as easy as possible to do a clean split. We are looking for some spot close to the bare metal where you have stripped the semantics already, but preserved enough for the backend to exploit uniformity. Easy for R1CS, might be difficult for more complicated settings. Muthu: MPC has struggled with these problems in garbled circuits. We may be missing some tricks. Eran: Gadget libraries. MPC don't even have these. Daira: An interopable interface will never have the same performance as something specialised but that's okay because we're making the technology open to more people. Eran: Because we allow composition of gadgets, it would be possible for someone to write highly optimised gadgets that could be used in more complicated languages. Doesn't help with high level techniques, but gets us halfway there. PRESENTATION: Need multipart proofs: Might use multiple schemes for proving a larger statement. Want to concatenate proofs Need to specify public inputs to each proofs, and must be some shared wires. Legosnark is relevant. Easy way to make it scalable is to design subproofs. Not succinct, but very scalable. Need packaging and execution: How to execute diverse implementations? How do they communicate? Ideally something like docker. Encourage all designers to support this mode. We would like to automate as much as possible to make it usable and testable. Flexible deployment: experiment messages sent in files, or as a buffer move towards automation of comments Using zkInterface today: You can use it and contribute. github.com/QED-it/zkinterface DISCUSSION: Benedikt: At some point there is always a trade-off between usability and performance. Do you think this is inherent. Eran: Depends on the language in the backend. In R1CS we have been fortunate. The richer we go, the harder it is to convey all the power without loosing interoperability. It's a moving target because the best native languages change depending on the state-of-the-art. I'm optimistic that there are good abstractions to be found. Benedikt: Do you think it's important for cryptographers to aim for R1CS natively. Daira: I don't think that constraint should be imposed on proof systems. Eran: An adapter would be nice, although it might make benchmarking unfair. Risks misguiding developers to optimising for the wrong thing so should be a bit weary. Daniel: I think the real overhead would come if someone wanted to use a R1CS frontend and a backend optimised for a different frontend. Daira: Guestimate factor of 6 overhead if have custom gates. Eran: Would be great if people could experiment with R1CS frontends while using a very different backend. Benedikt: Any comments on the GKR setting which tends to be quite different? Daniel: What languages would people like to see in a standard? What would make zkinterface more useful? Daira: Ariel's proposal was to specify polynomials that make custom gates. Not the right level of abstraction for an interopable system as it would be very difficult for a compiler to use that. Benedikt: There is a growing set of proof systems, polynomial commitments, crypto is all in polycommit and front-end may be described by e.g. a PCP. Daira: Doesn't help in this situation. THe problem is that a proof system that is partly universal means you have to fix some things about the metacircuit and then get the front end compiler to understand what you have done. Even if different systems are compiled in the same way, it may not be in a way that is useful to the frontend. Benedikt: Seems like an interesting next candidate. Daira: There are only a few things that we need to heavily optimise because hash-functions and ECC comes up everywhere and tends to be the bottleneck. Benedikt: Is there a goal towards a useable front end for R1CS. More higher level languages. Daira: As long as the more general thing is not the bottleneck in your circuit then you're fine. Riad: Proposed specification is intended to be a diognostic type thing. Should support any language in the front end. Great, but a lot of the higher level semantic information is lost, and the compiling outputs are done forever. Lost something, but maybe that's okay. Maybe there is room in this format for some meta-information about which semantic piece corresponds to which output. Daira: I think we can use the interactivity. Front end can ask back-end "What can you do efficiently", and not compile those bits in the same way. Jamie: Automatically vectorising was replaced with gpu's. Coming back-now, and asking "does the backend support this operation", if not do this. Both branches equivalent, but allow the code to make choices at compile time. Seems like a similar scenario. Great to pass function calls down layers. Daira: This conditional code ends up being in libraries so it's okay in practice. Jamie: Typically yes. Benedikt: Join the working group. https://community.zkproof.org/g/WG_ZKINTERFACE Riad: In certain cases formal verification, attempting to make things better can be hampered by having a gross mismatch between higher and lower level semantics. There are people that know a lot about this. We should ask them which constructs in a low level language are dangerous. Izaak: It's a lot easier to give formal semantics to functional programming languages or something that looks like one, something non-deterministic. With something as low level as constraint1 + constraint2 it becomes more difficult to describe semantics. Riad: Proving "this compiler always correctly compiles from this language to that language". Would that be problematic? ---- Charter Ideas Goals: - Milestones: - ---- ## Discussion topics _Suggestions welcome! Please append at the end, and the moderators will incorporate into the schedule._ ~15 minutes each, by default. * Feedback on the current design? * Have you used it? * What did/didn’t you like? * Beyond R1CS * What constraint-system styles are most urgently needed? * Good conventions/examples to follow? * Concrete deployment scenarios * Execution environment and packaging requirements? (e.g., binaries vs. WebAssembly) * Connections to PL and formal verification * What other tools can benefit from being combined with many frontends? * Analysis, verification, optimizers, …?