Home Edition #2

Proposal: Leo: A Programming Language for Formally Verified, Zero-Knowledge Applications Discussion Notes

Moderator: Eran Tromer
Presenters: Howard Wu & Collin Chin

Authors:

  • Collin Chin
  • Howard Wu
  • Raymond Chu
  • Alessandro Coglio
  • Eric McCarthy
  • Eric Smith

To be presented on 2021-04-19.

Resources:

Real-time notes

Note taker: Daira Hopwood

Motivation:

Decentralised applications have scalability issues due to everyone reexecuting all transactions.

Time-sharing resources across all parties.

Limited execution environments are being used to improve throughput.

History of all state-transitions must be executed by all parties causes privacy issues.

Lack of privacy also enables front-running attacks against consensus.

ZKPs enable prover to prove known state-execution was performed correctly without publicly disclosing contents.

Challenges:

DApps have weak guarantees of correctness and safety.

Require specialised expertise to represent executions.

Solution:

Leo is formally verified programming language for zero-knowledge applications. It is composable, decidable and universal.

Leo has 3 primary stages. Code -> Parser -> AST -> Conversion -> …

Focus on Type Inference.

Type inference: automatically detects types of an expression in a formal language.

Formal definition of Leo language, aimed at producing a verifying compiler that proves semantic equivalence between input and output programs

Using ACL2 to verify each stage, using a formal model of the phase. There might be nondeterminism in the specification of the phase.

Compose the stage proofs to obtain an end-to-end proof.

Adding more optimization phases. Proofs are composable for modularity of the compiler.

Leo is implemented in Rust, 65000+ LoC, 12 contributors

Formally verified in ACL2, open-sourcing this soon.

70+ page language specification.

Also built tooling and frameworks, including Leo Playground. Will be released tomorrow.

Aleo Studio - IDE for writing zk applications.

Aleo package manager, with collaborative features.

https://leo-lang.org
https://paper.leo-lang.org
https://github.com/AleoHQ/leo

Discussion

Does it support nondeterminism?

  • Currently no. There have been discussions.
  • The current assumption is that a Leo circuit is compiled to a noninteractive proof system. Could also execute in the clear to produce a witness.

Is the scope of Leo just specifying a circuit? Does it include precomputation?

  • Specifying and executing a deterministic circuit.
  • Want to expand proof systems and curves.

Own implementation of proof system and curves?

  • own impl of Groth16 with BLS12-377

Supporting zkInterface?

  • Trying to optimize size of serialized representation.
  • PFCS = prime field constraint system, generalization of R1CS.
  • Need deterministic conversion to R1CS.

Eran: proposed extensions to zkInterface coming from SIEVE programme.

  • SIEVE IR, two syntaxes one based on zkInterface. Other might support PLONK-like custom-gate features, loops, branches, etc.

Francois Garillot: rationale for Hindley-Milner, relation to e.g. Noir?

  • need strong types with modular proof
  • biggest differentiating factor is formal verification
  • heavy lift is to remove assumptions in IR to make proving easier.

Francois: Why standardize specific language? What is required of the IR to enable more general standard that would enable formal verification?

  • Only the last stage depends on the circuit model. We want to formally verify the entire stack.

Francois: need to abstract in order to standardize. Otherwise we are standardizing precisely Leo.
Eran: drill more into what zkInterface should provide to support what Leo needs.

  • Extract what we had in early versions (baked in Groth16 and BLS12-377) to a separate repo.

Daira: comparison with CirC? (https://eprint.iacr.org/2020/1586)

  • SMT solver approach looks to be more elegant
  • Some language barrier (CirC implemented in Haskell, Rust version is coming up)
  • core library functionality could use CirC.

Kev: relation to ACIR (unlimited fan-in gates and black-box functions)

  • One aspect that makes our IR nice is that we use an ASG (abstract semantic graph) which enables outputting ASTs that can be converted to any IR.
  • Optimizations are standard PL fare.

Kev: rationale for Hindley-Milner?

  • not polymorphic, just inspired by H-M
  • not clear whether Leo will have polymorphic types
  • standardizing type systems for zk is an interesting problem

Alessandro: Verifying Leo programs against higher-level specifications is indeed of interest. But no work on that yet — focusing on the compilation process.

Stephane Graham-Langrand on Terminology: In the formal methods community, the name “Leo” is already taken as the name of a well-established Theorem Prover. Is the name set in stone? :-) It’s going to be confusing while interacting with the FM community…

Eran: standardizing language aspects (syntax and semantics that are quite opinionated) would be an uphill battle.

Proposed standards-oriented action

  1. Work with zkIntrface WG to discuss compilation targets and requisite extensions to zkInterface for representing structure, succinctness, etc.
  2. PFCS
  3. other components were mentioned that could be reused?

Telegram group for discussion: invite link here
Formal specification doc: link here

Select a repo