Open Grant Proposal: Lurk-FVM Integration

[johnchandlerburnham]

Open Grant Proposal: FVM Integration of Lurk zkSNARK Language and Applications

*Name of Project: Yatima*

Proposal Category: app-dev

Proposer: @johnchandlerburnham

Technical Sponsor: @porcuquine

Do you agree to open source all work you do on behalf of this RFP and dual-license under MIT, APACHE2, or GPL licenses?: Yes

Project Description

We are planning to integrate Lurk, a programming language for Turing-complete recursive zkSNARKs, with the Filecoin Virtual Machine as a user actor. This will enable zero-knowledge proofs written in Lurk to be verified natively on Filecoin, enabling us to then implement simple examples of zero-knowledge applications such as proofs of membership, private tokens, WASM or EVM state rollups.

We will also show a novel application of Lurk based on Yatima's previous Open Grant, called a zero knowledge type certificate (zkTC), which allows for succinct cryptographic verification that a specific program or data value correctly validates against a given type. With the Yatima project, Lurk zkTCs can be used to verify arbitrary formal proofs written in the Lean Theorem Prover. Finally, we will use Lurk zkTCs to create a demonstration of a on-chain marketplace where parties can trustlessly buy and sell verifiably correct typed programs and data.

Given the security requirements of this work, we will additionally use the Lean Theorem Prover to formally model many components of the Lurk and FVM stack. Bugs in the Lurk verifier or the FVM implementation have a high potential cost, and formal verification is a powerful tool for improving software correctness. Furthermore, these Lean security proofs can themselves then be verified via Lurk zkTCs on FVM, allowing the system to self-validate to some degree.

Value

The value of this project will be to allow users of Filecoin to create and interact with actors or smart contracts which can use Lurk to enhance their scalability or their expressiveness. Additionally, Lurk's generality allows for new kinds of applications of zero-knowledge proofs, such as zkTC concept explained above. We believe that zkTCs on FVM will make Filecoin the platform of choice for many formal verification use-cases, particularly involving the Lean Theorem Prover.

Deliverables

The deliverables for this project will be:

• A minimal lurk-verify rust crate factored out from the primary lurk-rs repository which implements a WASM compatible Lurk zero-knowledge proof verifier. (Milestone 1)
• A lurk-actor FVM user-actor implementation which exposes functions from lurk-verify (Milestone 1) Various formal proofs of components of the Lurk and FVM system, including modeling of Lurk's Nova backend. (Milestone 2)
• Functionality for generating Lurk proofs of WASM and EVM execution. (Milestone 3)
• A domain specific language in Lean for writing formally verified FVM contracts (Milestone 3)
• Various examples of simple applications enabled by Lurk-FVM (Milestone 4)

The final capstone deliverable will be the demonstration of a trustless proof marketplace (described further in Milestone 5)

Development Roadmap

Milestone 1: Lurk Verifier as an FVM Actor

Duration: 10 weeks, 4 people

The goal of this Milestone is to produce a proof-of-concept that shows Lurk may be integrated with FVM as a user actor. The FVM roadmap has user-actor deployment scheduled for Q1 '23, but likely this feature will be available on the Wallaby testnet much earlier.

• Milestone 1.1: A minimal lurk-verify rust crate factored out from the primary lurk-rs repository, specifically for the Lurk verifier
• Milestone 1.2: Ensure lurk-verify compiles to WASM
• Milestone 1.3: Implement a lurk-actor FVM user actor which exposes lurk-verify functions as an API.
• Milestone 1.4: Deploy lurk-actor to the Wallaby test-net, or to Filecoin main-net, if possible.

Milestone 2: Formal Modeling of Lurk in Lean

Duration: 10 weeks, 4 people

The goal of this milestone is to begin to build infrastructure in Lean which matches the functionality of lurk-verify and lurk-rs to lay the groundwork for formal proofs in Lean 4 about Lurk. This milestone does not aim to fully formally verify the entirety of Lurk, but does intend to write proofs where practicable, and to lay a solid foundation for more comprehensive verification in future.

• Milestone 2.1: Implement BabySNARK, Groth '16 in Lean 4, based loosely on Bolton Bailey's Formal Snarks Project in Lean 3. This is not strictly needed for lurk-verify, but is extremely useful for building knowledge of how to model these kinds of problems in Lean 4.
• Milestone 2.2: Implement Nova in Lean 4
• Milestone 2.3: Produce soundness proofs in Lean 4 for BabySNARK, Groth '16 and Nova, insofar as is practical given the current state of mathlib4.
• Milestone 2.4: Model Lurk's abstract syntax tree, and write a parser in Lean 4
• Milestone 2.5: Port the Serde library to Lean 4, and implement Lurk's IPLD content-addressing format
• Milestone 2.6: Port components of the bellperson library to Lean 4, specifically relating to the Nova proving system.

Milestone 3: Formal Modeling of FVM in Lean

Duration: 10 weeks, 4 people

The goal of this milestone is to facilitate writing formally verified Filecoin actors in Lean.

• Milestone 3.1: Specialize Yatima's prior WASM interpreter in Lean 4 to FVM
• Milestone 3.2: Write an interpreter in Lean 4 for the Ethereum Virtual Machine
• Milestone 3.3: Write a domain specific language in Lean 4 for writing Filecoin user actors
• Milestone 3.4: Extend the DSL from 1.4 with useful features for providing formal proofs about actors, such as e.g. proving properties about side-effects, function signatures, or arithmetic errors, etc.

Milestone 4: Filecoin User Actors using Lurk

Duration: 10 weeks, 6 people

Using the tools developed in the previous milestones, we will write several example contracts showcasing the use cases of the Lurk-FVM stack. In particular, we would like to demonstrate a minimal example of how Lurk can be used to implement state-machine roll-ups, which could greatly enhance FVM's scalability.

• Milestone 4.1: Write a typed functional commitment actor (tyfcomm) containing the CID of some Lean 4 function f which takes input type A and returns output type B, as well as a Lurk zkTC that f : A -> B). Once deployed, the actor will expose an endpoint such that a user can upload a Lurk proof that passing a value x of type A to f produces the value y of type B (i.e. f x == y and y : B). This minimal example allows for public point-wise validation of f, without requiring recomputation of f.

• Milestone 4.2: Explore a variation of the tyfcomm actor called tySaaScomm from Milestone 4.1 with f as a private input and x known. This extends tyfcomm to a multiparty setting, where the originator of the actor keeps the function f secret, and users request that the originator apply f to certain inputs they provide. This allows, in principle, the originator to efficiently operate a private on-chain Software-as-a-Service system.

• Milestone 4.2: Explore a variation of the tyfcomm actor called tyDaaScomm, where instead of committing to a function f : A -> B, we commit to secret data x : A, and then expose an API that allows user to request that the actor originator apply given functions f : A -> B to the committed x : A.

• Milestone 4.3: Specialize the tyfcomm actor for producing proofs where f refers the WASM.lean or EVM.lean interpreter. In principle, this will allow for single state machine transitions of FVM actors to be "rolled-up" into a Lurk proof

• Milestone 4.4: Write an actor for chaining multiple iterations of the tyfcomm actor, where f is a state machine f : S -> A -> (S, B).

• Milestone 4.5: Specialize the chaining tyfcomm actor to WASM.lean or EVM.lean, enabling chaining roll-ups. This Milestone aims to provide a minimal proof-of-concept for zk-rollups on FVM, but further work will be needed for a production-ready product, particularly around actor interaction.

Milestone 5: A Trustless Proof Marketplace

Duration: 10 weeks, 6 people.

Implement a minimum viable proof marketplace on FVM. As a rough sketch, this marketplace will have the following features:

• Users can place bids that they will pay k FIL for a Lean expression x that typechecks against a known type A. These bids are held by the marketplace directly.
• Different bids for the same type A pool together.
• Opening a new pool incurs a fee paid by the user to the marketplace, contributing to an existing pool incurs a smaller fee.
• Pools can be claimed by submitting a Lean expression x along with a Lurk proof that x : A. The marketplace then verifies the proof, and releases the funds if it is valid.

These features may change substantially based on technical requirements, but the essential principle is a notion of incorporating Filecoin as an economic incentive layer on top of the kinds of contracts outlined in Milestone 4.

• Milestone 5.1. Implement marketplace according to the following rough outline above.
• Milestone 5.2: Publish whitepaper detailing theory and operation the marketplace.
• Milestone 5.3: Explore extensions of the minimum viable marketplace, including non-custody transactions, sell-side offers, etc.

Total Budget Requested

Communicated to the team via Google Doc.

Maintenance and Upgrade Plans

Yatima Inc. is a well-funded seed-stage startup building a verifiable computing platform on top of Filecoin. The trustless proof marketplace, described above, is a key piece of infrastructure required by our platform. We also expect a varied ecosystems of data marketplaces to spring up on Filecoin, similar to how, for example, Uniswap catalyzed an entire industry of decentralized exchanges on the Ethereum platform.

Team Members

• @arthurpaulino
• @cognivore
• @DanielRrr
• @gabriel-barrett
• @ixahedron
• @johnchandlerburnham
• @mpenciak
• @rish987
• @samuelburnham
• @winston-h-zhang

CVs provided via email

Team Website

https://github.com/yatima-inc/

Relevant Experience

Our team has extensive experience at the intersection of formal proofs, zero-knowledge cryptography, and blockchain technologies. We have contributed to the Lean Theorem Prover, the Lurk Language, as well as to Filecoin infrastructure such as the IPLD and Multiformats libraries. Our previous Filecoin Open Grant is here: https://github.com/filecoin-project/devgrants/issues/369, and our previous W3F grant is here: https://github.com/w3f/Grants-Program/blob/master/applications/yatima.md

Team code repositories

• https://github.com/yatima-inc/yatima-langhttps://github.com/yatima-inc/Lurk.lean
• https://github.com/yatima-inc/ZKSnark.lean
• https://github.com/yatima-inc/Serde.lean
• https://github.com/yatima-inc/Ipld.lean
• https://github.com/yatima-inc/Lurk.lean

[ErinOCon]

Hi @johnchandlerburnham, thank you for your proposal! This grant has been approved. We will continue discussing next steps by email.

[Stebalien]

What features would you need to improve SNARK verification performance?

• Any specific syscalls (precompiles)? Builtin elliptic curve operations?
• SIMD support?

[samuelburnham]

At this stage, we're not sure what would be needed to improve performance on the FVM side. The plan is to create a minimal Lurk/Nova verifier compiled to wasm32-unknown-unknown without focusing on optimization yet, so there shouldn't be any need for SIMD support, floats, I/O, or syscalls. Definitely worth thinking about in the long term though!

[ineffectualproperty]

Hey @Stebalien - Based off recent profiling of the Nova compressedSNARK verify method, ~70-80% off the time is spent in multi-scalar multiplication (MSM) over the Pasta curves. A first target for improved verification performance would be a MSM precompile for the Pasta curves. Other elliptic curve operations (e.g. Add, Mul) may also be useful, and perhaps even hashing precompiles, but I don't have great insight today into the next bottleneck after MSM. The Ethereum EIP for the BLS12-381 precompiles (https://eips.ethereum.org/EIPS/eip-2537#proposed-addresses-table) may be a good starting point for a future FIP if this seems like a good direction to go.

[oberstet]

+1 for MSM as a hard wired performance primitive. using EIPs for precompiles to steal from: yeah, makes sense - if only rgd the attention to detail eg specifying behavior (a precompile MUST behave exactly the same under all inputs, conditions and in all client implementations .. the Filecoin FVM, any other FVM, any hardware implementation ..) and ABI (the EVM precompiles are via a VM bytecode and addresses etc, and this stuff must again be precise down to the single bit) ...