Skip to content

Instantly share code, notes, and snippets.

@sockdrawermoney
Created September 27, 2024 15:51
Show Gist options
  • Save sockdrawermoney/21a55c3775dfef25c64c0e9a770b0774 to your computer and use it in GitHub Desktop.
Save sockdrawermoney/21a55c3775dfef25c64c0e9a770b0774 to your computer and use it in GitHub Desktop.

Kakarot ZK-EVM Code Walk-Through

This document is a transcript of a code walk-through session on the Kakarot ZK-EVM project. Participants include members of the Kakarot Labs team and other C4 community members. The session covers various topics related to Cairo, the EVM implementation, and interactions with StarkNet L2.

Summary

The session covered various aspects of implementing an EVM in Cairo and deploying it on StarkNet L2. Key topics included:

  • Differences between Cairo and Cairo Zero languages and their VMs.
  • Handling non-deterministic memory in CairoVM.
  • The use of hints in Cairo and their implications for the prover.
  • Interactions between EVM subcalls and transaction reverts in Cairo.
  • Potential vulnerabilities in StarkNet and Kakarot interactions.
  • Representation of large integers (u256) using felt in Cairo.
  • Resources for further learning, including video tutorials and documentation.

Resources discussed


Discussion on Cairo and CairoVM

jilt:

Is it the Cairo Python version?

clemlaflemme:

Python is a VM language, not a Cairo version. So any Cairo version runs either on Python or on whatever VM (Rust, TypeScript, Go).

Elias Tazartes:

There are two languages:

  • Cairo
  • Cairo Zero

There are two Cairo VMs that are able to interpret both languages:

  • CairoVM Python
  • CairoVM Rust

jilt:

The version with hints, I mean.

Elias:

Yep, this is it.


Execution Specifications

clemlaflemme:

For everything regarding standard EVM flow, the Ethereum Foundation's Execution Specs is a great resource.


Managing Non-Deterministic Memory

  • Elias: At the end of the call, you could do a 5-minute deep dive into understanding this idea of non-deterministic memory, @clemlaflemme. It's a new mental model for most people.
  • Elias: Note that CairoVM is a write-once VM—it can't have a native stack or native memory data structures, so we have to simulate them using dictionaries.
  • clemlaflemme: It's read-only.

Hints in Cairo

Elias:

Hints suggest to the prover to add some values to memory, but he is not forced to. Whereas Cairo code defines real constraints.

This is the same as succinct "unconstrained" blocks of Rust code vs. constrained code.

Example Use Case:

  • Compute sqrt(x), but sqrt is expensive in ZK.
  • Ask the prover to provide y = sqrt(x) inside a hint.
  • Then assert inside constrained code that y^2 = x.
  • The prover cannot lie, and we've saved compute.

Key Point:

  • Always think the prover is malicious.
  • Constrain him to ensure what you want to prove is proven, e.g., proper EVM flow.

Question from Franfran

Did you say that the prover may not execute the hints?

Elias:

Yes, hints suggest to the prover to add some values to memory, but he is not forced to.

clemlaflemme:

The hints are not part of the program.

Question from 3DOC

About the State copy you showed before, could you dive a little more into how the state is restored after a revert? Is it simply the new copy that is discarded, or is there something more?

clemlaflemme:

The new copy is (squashed and) discarded.

Question from Franfran

Do we have mutable references to avoid having to pass by value with your example of the EVM variable in Cairo 1?

Elias:

There exist two EVM instruction set implementations:

Note: Only Kakarot is in the scope (plus Cairo 1 helpers in SSJ).

Franfran:

Thanks!

Elias:

Maybe in some cool future, there'll be a competitive audit for SSJ :))) ~2025.


EVM Subcalls and Transaction Reverts

Elias:

If a subcall in spec-compliant EVM fails, the parent call may decide not to fail or fail (try/catch).

If a subcall in Cairo fails, currently the entire transaction reverts.


StarkNet and Kakarot Interactions

Elias:

As we finish this part of the presentation on "Interop Cairo vs. EVM," remember this EVM will live on StarkNet L2.

There might be some vulnerabilities regarding StarkNet and Kakarot interactions, not necessarily linked to the Ethereum Virtual Machine implementation per se.

Best to understand StarkNet flow and infrastructure:

Considerations:

  • Is the EVM following the spec (we do pass >95% Ethereum Foundation specification tests)?
  • Can an attacker steal funds from Kakarot users on StarkNet (by exploiting our EOA implementation, etc.)?
  • Can an attacker abuse our StarkNet ↔ EVM interop modules to pass malicious payloads?

Note: Kakarot is ownable, but key management isn't part of the scope of the audit.


Felt Representation and u256

Elias:

Remember, felt is the word size in Cairo; it is up to 252 bits.

So to represent a u256, we need two felts (represented as two u128s).

Question from 0xTheBlackPanther:

251 or 252?

Elias:

Almost 252, yep.

Further clarification from clemlaflemme:

0x800000000000011000000000000000000000000000000000000000000000001 from starkware.cairo.lang.cairo_constants import DEFAULT_PRIME.


Additional Resources

Elias suggests watching later:

Documentation on Hints:

Understanding Implicit Arguments:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment