We will post more updates when the proof is complete! 🎄

To that end, we state that if the circuit runs until the end on a witness, then it must be the encoding with field elements of a Keccak computation.

Frequent intermediate operations are showing that arrays hold boolean field elements, as well as manipulations of limbs of binary integers.

We verify these logical tricks by brute-forcing all the possible values for the booleans, as there are only up to five or six such booleans for each formula.

The main property we show is that the circuit is deterministic (no under-constraints).

Then we write our proofs, trying to be careful to follow the organization of the original code, by verifying each loop independently and composing their behavior in a second step.

A few logical tricks are used in the definition of Keccak to replace some XOR operations by equivalent additions.

We might choose to refine those choices later, once we better understand the bottlenecks in the proofs.

Our base definitions are in github.com/formal-land/...

For now, we use rather simple data structures. For example, for field elements with use explicit Z elements with a modulo "p" operation, "p" being supposed as a prime number.

For arrays, we use the total function of their indices, returning a default value when out of bounds

It is important to keep the original structure of the code, with explicit loops, in order to keep the number of equations small.

It will be simpler to reason about loops rather than a larger number of equations. In addition, the loops are rather simple here in terms of invariants.

The Rust source code is available at github.com/Plonky3/Plon...

For now, we translate it by hand to the corresponding constraints in Rocq in the Garden project github.com/formal-land/...

We will ensure later with "coq-of-rust" that it corresponds to the original implementation.

The Keccak hash function, one of the most frequently used hash primitives in the Ethereum protocol, is implemented here efficiently using zero-knowledge constraints.

This amounts to encoding boolean operations like XOR or shift using equations over polynomials of integers modulo a prime number.

The blog post: formal.land/blog/2025/07...

Happy to discuss the proof strategy/choices of representation!

The link: formal.land/blog/2025/07...

formal.land/blog/2025/07...

It differs from what we were doing before, which was generating a typed and executable Rocq version, but without making explicit the non-aliasing and with a quite verbose version, making it difficult to use for the proofs.

1. Continue to verify a functional definition for the rest if the EVM instructions.

2. Show that this functional definition is equivalent to a semantics for the EVM in Rocq. There is at least one such project that we could show as equivalent to a reference implementation.

For the rest of the instructions, we have a typed representation in Rocq generated with the help of "coq-of-rust". However, we do not have a clear idiomatic and functional definition like for the instruction ADD.

From there, we can go in two directions:

Finally, we update the top of the stack with the result of "Impl_Uint.wrapping_add" applied to the two top elements!

We first try to consume a "VERYLOW" amount of gas. If it fails, we return the "OutOfGas" error message.

Otherwise, we pop one element from the stack and ask for a reference to the next one. If there are not enough elements, we return "StackUnderflow".

In our functional specification, the first line:

Output.Success tt

says that there can be no runtime failures (no panics!), assuming none of the provided methods panic. This is an important safety property.

The rest describes how the ADD instruction behaves.

One of the difficulties here is that the code is very abstract. The types of the stack or gas field are not defined, nor are the functions to manipulate them. Instead, they are provided as trait implementations.

We need to specify them somehow to say they admit a functional specification.