Proof composition and cross-contract calls

To understand the concept of proof composability on Hylé, we recommend you read this blog post. This page focuses on demonstrating how to use proof composition in your code.

What is proof composition?

Proof composition happens when two contracts depend on each other. Proof composability is the fact that Hylé allows you to manage this while keeping their proofs independent.

Most zero-knowledge systems deal with cross-contract calls by enforcing recursive proof verification:

Program A verifies proof of correct execution of Program B;
Program B verifies proof of correct execution of Program A.

Hylé allows you to assume, in Program A, that Program B has been successfully executed, by verifying that claim. If you batch both blobs in the same operation, we verify both natively outside of the contract; the whole operation fails if one proof fails to verify.

Writing a cross-contract call

Your program does not need to verify the execution of another program directly. Instead, it uses a representation of the called contracts.

This representation consists of:

the app
the function
the function's parameters
a claim on the results.

Claims can look like this: MoneyApp::transfer(10, A, B) == true or TicketApp::get(A) == ticket.

Follow these steps:

Inject claims: add all the claims as inputs to the blob.
Index claims: provide an index to tell the contract where to locate its input.
Assert claims: use the claim list to validate the required conditions for the blob.

How Hylé settles multiple proofs

When you submit multiple proofs to Hylé:

Proof generation is parallelized: proving times do not compound since proofs do not depend on each other.
Proof verification is asynchronous thanks to pipelined proving. As soon as one proof is ready, it can be verified on Hylé, even if the other proofs aren't ready yet.
Once all proofs related to the transaction are verified, the transaction is settled on Hylé. If one proof verification fails, then the entire operation fails.