Proof composability on Hylé

When our first grantee, Matteo, finished building his provable play-by-email game engine, we asked him what his favorite part of building with Hylé was. He didn’t hesitate before answering: « It’s proof composability. This makes my life so much easier! »

In this blog post, we’ll explain why building provable apps is still hard today and how proof composability, as enabled by Hylé, saves developers a lot of time and effort.

Creating provable apps is hard!

Most applications require multiple pieces of information, and proofs are the condition for settling the actions in their transaction. These actions are interdependent, which means proofs have to reference each other.

In this post, we’ll take the example of a second-hand concert ticket application (TicketApp). A successful money transfer (on MoneyApp) is needed to deliver the ticket from the seller to the buyer. Both of them are provable apps, which means they use zero-knowledge proofs to settle their state.

This flow includes two stateful applications with a dependency linking them:

• TicketApp needs the successful execution of MoneyApp: the money must have been successfully transferred for the ticket to be issued.
• The money transfer must not happen if TicketApp fails, so you can’t do one and then the other.

With these atomic transactions, we either want both apps to settle to their final state (if both proofs are valid) or neither if one or more proofs fail to settle.

Recursive proofs

The way most zero-knowledge systems deal with this currently is by recursing proofs.

The process goes as follows:

1. MoneyApp generates a proof of transfer.
2. MoneyApp sends the proof of transfer to TicketApp.
3. TicketApp verifies the transfer proof, which means TicketApp includes a verifier compatible with MoneyApp’s proofs.
4. If valid, TicketApp sends both the TicketApp and the MoneyApp proofs to the blockchain for settlement.

It works, sure… as long as the applications are written with a technology that provides verifiers for all other zkApp technologies.

If MoneyApp is a provable app using Risc0, and TicketApp is in Cairo, as a developer, you’ll need to use a RISC Zero verifier in Cairo. Your contract dependencies depend entirely on which verifiers are available and where. The complexity grows fast: with two languages, you need two verifiers, but with 3 of them, you’re up to 9 different verifiers to check everything.

Not only that but if any of the programs changes, you need to update your entire stack!

For each of these proofs, the recursion means that the time to prove will increase exponentially. The dependencies between the programs will also block it: if TicketApp needs the MoneyApp proof before it is executed, the total waiting time is MoneyApp proof gen + TicketApp proof gen.

The slowest proof will bottleneck everything: all the others need confirmation of this one to start running.

This is simply not a sustainable solution for provable app development. 

The solution: proof composability

Hylé’s system, based on native proof verification, enables proof composability.

In the case above, we were injecting proofs into contracts and verifying them inside the contracts. Hylé verifies them natively outside of the contract.

In that case, TicketApp refers to a representation of a successful MoneyApp execution. This representation is checked at the contract execution without involving proof verification. 

This representation consists of:

• the app (MoneyApp)
• the function (transfer)
• its parameters (User A, User B, 10)
• a claim on the result (true).

TicketApp inputs

To make our TicketApp transaction valid, we need two assertions to be true:

1. MoneyApp has successfully registered a transfer from the buyer to the seller.
2. TicketApp has successfully sent the ticket from the seller to the buyer.

On Hylé, both of these assertions are the inputs you’ll provide to both TicketApp and MoneyApp for your transaction.

MoneyApp::transfer(10, A, B) == true
TicketApp::get(A) == ticket

Each will generate a proof if the execution is valid.

Combining the inputs

As a developer, you can:

1. inject the whole list of claims as inputs;
2. add an index to tell the contract where to locate its input;
3. use the claim list to assert whatever you need in the transaction about other contract calls.

TicketApp looks like this: 

TicketApp includes a check to confirm that the inputs include a valid claim on a transfer call in MoneyApp. Nothing gets executed.

Why we do this

As we’ve shown, the TicketApp contract now asserts the presence of the correct claim on MoneyApp it needs for its execution.

But that’s not enough: for the whole transaction to be valid, MoneyApp must also generate a proof asserting the transfer was done correctly, which will match the claim in TicketApp.

So, the MoneyApp claim is used twice:

1. in TicketApp, to ensure the claim matches the needs (a successful transfer from A to B);
2. in MoneyApp, as an input, to execute the actual money transfer and generate proof of the transaction.

This allows for several fail safes:

• If the claim is wrong, it does not fulfill TicketApp’s requirements: TicketApp fails.
• If the claim is well defined but can’t be executed (e.g., the buyer doesn’t have enough money), the MoneyApp can’t generate its proof of successful execution: MoneyApp fails.

Once all this is done, the proofs are sent to Hylé atomically and simultaneously. Since they are in a single transaction, this guarantees that the money transfer and the ticket delivery happen simultaneously and both app states are settled.

Programs don’t depend on respective proofs: they can be run simultaneously despite their mutual dependencies and achieve a proving time equal to the slowest proving time of all transaction contracts rather than compounding them.

You have full flexibility: the user can interact with both apps, or MoneyApp can lead the transaction and many other cases. In this diagram of the whole process, we’ve chosen to have the user ask for a ticket from TicketApp, who will act on their behalf when interacting with MoneyApp and lead the cross-contract composition.

With Hylé’s native proof composability, you can save time and effort building your provable apps as a developer. 

You don’t need to find the correct verifier anymore to link all of your proofs together: batch them in a single transaction and let us prove everything natively and simultaneously!

You can also choose whichever provable language you prefer, whether it’s out of personal comfort or because you want each language to do what it does best. Now, you can combine SP1 to prove a Rust app and Noir for client-side proving without any hassle!

If this sounds exciting and you’d like to build with Hylé, you can check out our documentation (our devnet is live!) and our grants program!

This post's main author is Alex C.