.svg){kind=icon}
Now hiring!
•
%20verifier_%20Nethermind!%20(1).png)
The Formal Verification team at Nethermind joined forces with MatterLabs to formally verify the honesty of ZKsync's on-chain zk-verifier using EasyCrypt. This is a first-of-its-kind effort that showcases the applicability of formal verification in the broader zk ecosystem, with Nethermind leading the charge.
Read on for a full account. Or just get in touch right now to see what we can do about verifying your zk verifier.
In recent years, zero-knowledge (zk) proofs have emerged as a transformative technology in bringing Ethereum closer to its goal of achieving scalability and privacy. The key to their usefulness lies in their ability to allow one party (the prover) to demonstrate succinctly to another party (the verifier) that a given statement holds. In addition, there exists a fundamental asymmetry between the work required of the prover and the verifier: while the prover requires significant computational power to generate a proof, the verifier can quickly and efficiently check whether or not a proof is correct.
In the context of Ethereum, zk rollups leverage this ability and asymmetry by having:
where the semantics of transactions is commonly encoded as a set of arithmetic constraints over a finite field and is referred to as a zk circuit. In this way, zk rollups not only increase overall Ethereum scalability by reducing their on-chain storage and compute, but also, in an ideal world, do not allow for invalid state updates. However, there are three main issues that could make our world less than ideal: incorrect zk circuits; malicious provers; and malicious verifiers.
While recognising the importance of having correct zk circuits as well as the continuous and growing effort from the community that is going into their verification, we focus here on understanding the potential impact of the remaining two issues, as well as what it would mean to ensure correctness and security of the associated proof infrastructure components.
Before doing so, however, we define what it means for a zk verifier/prover implementation to be honest, as this notion underpins a number of relevant security properties below. In essence, a verifier implementation is honest if it:
and a prover implementation is honest if it:
The reader would be correct to note that honesty, by this definition, corresponds to the more generally used notion of functional correctness.
Impact of incorrectness of the prover or the verifier. On the one hand, if the verifier is honest but the prover is malicious, the worst-case scenario would involve liveness failures, but not safety failures. In particular, a malicious prover would not be able to generate a valid proof for an invalid computation, as the underlying cryptographic assumptions make this computationally infeasible. While liveness issues would admittedly be disruptive to the rollup operations, they could not, for example, result in funds being stolen or transactions being forged.
On the other hand, a malicious verifier could accept invalid proofs (for example, those generated by a malicious prover) as valid, potentially leading to catastrophic security breaches of the rollup.
Costs and benefits of formally establishing correctness. Provers are required to perform complex mathematical operations, use a variety of performance optimisations, and apply protocol-specific logic. This impacts the size of their codebase, which can easily reach tens if not hundreds of thousands of lines of code, making formal correctness assessments highly challenging. Moreover, there appears to be a shift in the Ethereum ecosystem towards decentralised provers, which cannot be trusted in principle as they could run on potentially untrusted custom hardware with potentially modified versions of the prover protocol/software.
In contrast, zk verifiers:
We believe that these combined facts make zk verifiers the appropriate first target for formal verification, a point previously recognised and advocated for by Firsov and Livshits [4].
When it comes to the prover and the verifier, and assuming circuit correctness, the essential properties that need to hold are the following:
In the work of Bellare and Goldreich [1], it is shown that soundness (1) can be derived from knowledge soundness (4), a result recently mechanised by Firsov and Unruh [2]. Further, Attema, Fehr, and Kloss [3] have shown that (4) can itself be derived from an additional property, termed special soundness. The work done in [2] has demonstrated how proofs of special soundness can be mechanised for some interactive versions of simple protocols, such as the Fiat-Shamir, Schnorr, and Blum protocols.
In considering which tools to use for this effort and stopping short of building our own, we were guided by the two must-have capabilities:
which left us with only one choice: the EasyCrypt interactive framework for proving security properties of cryptographic constructions and protocols. The key advantage of EasyCrypt over other available tools are its built-in specialised logics for reasoning about probabilistic programs and program equivalence, which are essential for proving the complex cryptographic properties that underpin the zk paradigm. In more technical terms, EasyCrypt comes with a primitive formalisation of probabilistic Relational Hoare Logic (pRHL), which is a dedicated cryptography-oriented program logic, together with an advanced tactic language for associated reasoning and integration with state-of-the-art SMT solvers.
The only aspect that EasyCrypt did not readily provide was the ability to reason about Yul programs. To that end, we extended it with a model of the subset of Yul required to execute the verifier by implementing the required Yul instructions, guided by our Yul formalisation in Lean, which underpins our Clear framework. In this way, we have created a reusable infrastructure for verification of zk verifiers written in Yul, while also giving a more general pathway for what it would mean to use EasyCrypt to prove zk verifiers written in other languages.
We have proven that the actual on-chain implementation of the ZKsync zk verifier in Yul is honest. We have achieved this by showing that this implementation behaves in the same way an honest verifier would. In more technical terms, we have established a bi-simulation between the implementation and an abstract model of an honest verifier. This abstract model is written in pseudo code manipulating field and group elements and has eyeball equivalence with the honest verifier definitions from the PLONK/plookup papers [5, 6].
This effort took us roughly 2.5 months to execute, including the learning curve of EasyCrypt and the creation of the Yul model.
This project was time-scoped with the sole goal of proving verifier honesty. Given our experience, we have high confidence that we would able to prove most of the remaining properties and look forward to putting this to a practical test—for the moment, let us explain what would need to be done for each.
When it comes to special soundness (from which knowledge soundness and soundness follow), there already exists a pen-and-paper proof for a slightly less complex version of the ZKsync verifier (for more details, see [2, 3]). In addition, special soundness proofs have already been done in EasyCrypt for less complex verifiers and there already exists a comprehensive library of supporting lemmas and theorems [2], including a derivation of knowledge soundness and soundness from special soundness.
When it comes to completeness, we would need to additionally create a abstract model of the honest prover in EasyCrypt and then use it together with the abstract model of the honest verifier in the proof.
Finally, we believe that proving prover honesty is out of reach at the moment because the prover is substantially larger than the 1710 lines of Yul of the verifier, and is also written in Rust, C++, and Cuda, the semantics of each of which is much more complex than that of Yul and would require a considerable EasyCrypt encoding effort.
We have many exciting plans in store and services to offer to interested clients! For example, with support by the creators of EasyCrypt, we will soon be submitting a grant to the Ethereum Foundation to embed pRHL in Lean, with the ultimate goal of creating a dedicated, fully foundational EasyCrypt-like tool for zk reasoning.
We are very much looking forward to pushing the boundaries of the field by formally verifying as many security properties for as many real-world zk verifiers as possible. We firmly believe that sooner rather than later, and with the right approach and support from the community, verified zk verifiers will be a matter of course rather than outcomes of isolated efforts. Please do get in touch with us if you would like to strengthen your zk frameworks with the strongest correctness guarantees available on the market!
In the remainder of the blog, and for the interested specialist reader, we delve deeper into the most salient technical details of our project.
Having established the importance of formally verifying zk verifiers and our choice of EasyCrypt as the verification framework, we now give more detail on the specifics of our approach. In particular, we focus on:
A key requirement for analysing correctness of ZKsync’s on-chain verifier was to extend EasyCrypt with a formal model of the appropriate subset of Yul primitive operations (primops). Specifically, the verifier only uses the following primops, which significantly simplified our modelling effort:
.svg)
.svg)
.svg)
.svg)
.svg)
.svg){kind=icon}
.svg)
.svg)
.svg)
.svg)
.svg)
.svg)
.svg)
.svg)
mload, mstore, mstore8;revert;add, sub, mulmod, addmod, eq, gt, shl, shr, iszero, and;callvalue, staticcall;calldataload, calldatasize;gas, pop.In addition to these, we needed to model the four precompiled contracts that the verifier uses—modular exponentiation (modexp 0x05) and three elliptic-curve operations: addition (ecAdd 0x06), multiplication (ecMul 0x07) and pairing (ecPairing 0x08).
In this blog, we cover the most important aspects of the modelling; the full development is available here. In particular, we focus on the memory and revert operations:
module Primops = {
var memory : mem
var reverted : bool
...
proc mload(idx : uint256) : uint256 = {
return (PurePrimops.mload memory idx);
}
proc mstore(idx : uint256, val : uint256): unit = {
memory <- PurePrimops.mstore memory idx val;
}
proc mstore8(idx : uint256, val : uint256) : unit = {
memory <- PurePrimops.mstore8 memory idx val;
}
proc revert(x : uint256, y : uint256) : unit = {
reverted <- true;
}
...
}
EasyCrypt structures imperative programs using modules, which appear similar to those in typical imperative programming languages, but serve a different purpose: to encapsulate state and enable reasoning about programs with global variables. We represent the EVM state that we are interested as global variables within a module called Primops. Here, we highlight: the memory, which is of the type (uint256, uint8) map, denoted by mem (meaning that it is a map from 256-bit words to bytes); and reverted, which is a Boolean indicator of whether or not a revert has happened.
The Ethereum Virtual Machine (EVM) employs a memory architecture indexed by 256-bit words, but storing data as bytes—we model this precisely by using the above-mentioned mem type. This type, under the hood, uses the SmtMap built-in EasyCrypt data structure, which is the primary tool for reasoning about key-value relationships in EasyCrypt. While this structure cannot be executed directly (as the model is non-constructive), it provides a robust framework for reasoning about memory updates, access patterns, and behaviours through the rich set of provided lemmas.
Observe that the three memory operations in Primops amount to calling their pure counterparts from the PurePrimops/MemoryMap theories (we elide store as it is too verbose):
theory PurePrimops.
import MemoryMap.
...
abbrev mload = load.
abbrev mstore = store.
abbrev mstore8 = store8.
...
end PurePrimops.
theory MemoryMap.
op load (memory: mem) (idx: uint256): uint256 =
W32u8.pack32_t (W32u8.Pack.init
(fun (i: int) => memory.[idx + W256.of_int (31 - i)]))
op store8 (memory: mem) (idx val: uint256): mem =
memory.[idx<-W8.of_int (W256.to_uint val)]
...
end MemoryMap.
and then updating the state accordingly. EasyCrypt theories can be seen as libraries of related axioms, operations, and results. We create this separation of functionality (that is, the actual lookup or memory update) and side effect (that is, the global state update) in order to be able to reason cleanly and straightforwardly about the former without having to consider the latter.
The verifier rejects proofs by reverting, and for this reason we need to model the revert semantics, which is done straightforwardly as shown above, by updating the reverted global variable (initially set to false) to true. Importantly, only the revert primop can modify the reverted flag.
The only function calls performed by the verifier are static calls to the above-mentioned precompiled functions. For this reason, we model these directly inside the staticcall method.
We do not model gas reasoning in this project, and work under the assumption that there exists sufficient gas for the verifier to operate. This is sound as we only consider partial correctness, that is, executions that either terminate successfully or that revert due to the proof being incorrect.
Finally, it is important to note that we have used a modified Solidity compiler, developed by Igor Zhirkov from Matter Labs, which directly creates EasyCrypt modules that are based on our Yul model instead of producing standard Yul code.
A natural question to ask is how we should convince ourselves that our EasyCrypt Yul model accurately reflects the Yul semantics. A direct comparison would be challenging, as EasyCrypt has no formal semantics. We also cannot run tests from the Ethereum official conformance test suite (which acts as the de facto standard for ensuring correctness of EVM implementations), as we do not cover all of the primops but also, more importantly, because our EasyCrypt model is non-executable.
What we can do, however, as all of the primops have a (relatively) simple semantics, is to perform a basic eyeball sanity check, relating the model primop implementation to its natural-language semantics. For example, the description of the mulmod operator in the Ethereum yellow paper is, in essence, as follows:
mulmod takes 3 parameters:
1. a : first value to multiply (256-bit unsigned integer)
2. b : second value to multiply (256-bit unsigned integer)
3. n : denominator (256-bit unsigned integer)
and returns:
1. (a * b) % n: The (256-bit unsigned integer) result of the multiplication
followed by a modulo. If the denominator is 0, the result
will be 0.
Note: All intermediate calculations are not subject to the 2^256 modulo.
whereas our mulmod implementation in EasyCrypt is as follows
op mulmod(a b n : uint256) : uint256 =
let a_int = W256.to_uint a in
let b_int = W256.to_uint b in
let n_int = W256.to_uint n in
W256.of_int ((a_int * b_int) %% n_int)
where W256.to_uint and W256.of_int, respectively, convert an EasyCrypt 256-bit word to an EasyCrypt integer and vice versa, with the latter working modulo 2256. The correspondence between the two is immediate, observing further that the casting from W256 to uint (which is an arbitrary-precision integer) ensures that the natural language note is respected.
In addition to this, we state and prove fundamental properties about the primops that we modelled. For example, we use the following test and lemma to prove that an mload correctly recovers a previously mstored value:
function writeReadTest(addr, value) -> r {
mstore(addr, value)
let _1 := mload(addr)
r := _1
}
lemma writeReadTest_correctness:
forall (address value: uint256),
phoare [YulTest.writeReadTest : arg = (address, value) ==> res = value] = 1%r.
proof. (* ... *) qed.
Specifically, the writeReadTest function first stores a given value at a given address in memory and then and returns the result of reading the same address. The writeReadTest_correctness lemma then states, using Probabilistic Hoare Logic (in which specifications have the form phoare [P:Q] = x%r, which have the standard partial correctness meaning of Hoare Logic, except that the post-condition Q is reached with probability x (where %r denotes that x is a real number)) that the returned value equals the originally passed-in value with probability 1 (that is, always). The full proof is available in the repository.
Another example comes in the form of the modTest function and the modTest_correctness lemma, which aim at verifying the interaction between sub, mulmod and addmod.
function modTest(m) -> r {
let mv := sub(m, 1)
let o := mulmod(mv, mv, m)
let z := addmod(o, mv, m)
r := z
}
lemma modTest_correctness:
forall (m : uint256)
phoare [YulTest.mod_test : arg = m /\ W256.one < m ==> res = W256.zero] = 1%r.
proof. (* ... *) qed.
This lemma states that, for all inputs $m > 1$, the modTest function returns zero with probability 1. The proof, elided above but present in the repository, progresses as follows:
1. Simplifying the expression for o, we obtain that:
2. Using the lemma mul_add_mod_eq, which states that:
and the fact that m > 1, we obtain that:
3. Finally, simplifying the expression for z, we trivially obtain:
By doing the basic eyeball sanity checks and proving various properties about the implemented primops and their relationships, we gain sufficient confidence to claim that our partial Yul model in EasyCrypt is correct. We believe that further confidence could be gained by connecting this work with existing and future efforts (including our research) to formalise the Yul semantics.
When it comes to establishing honesty of the verifier implementation, we follow a structured, multi-phase strategy. In particular, we verify equivalence between progressively abstracted specifications of the verifier, starting from the Yul code generated by the modified Solidity compiler. These abstractions, written as EasyCrypt procedures themselves, allow us to reason about the verifier properties at different levels—from low-level operations (for example, EVM memory, reverts and 256-bit words) to high-level cryptographic specifications that involve finite fields and groups on elliptic curves. Each phase verifies that the corresponding specification still accurately reflects the behaviour of the program/specification from the previous level, creating a chain of equivalence from the extracted code to the high-level cryptographic reasoning. Every function in the verifier goes through a three-phase verification: low-, middle-, and high-level.
Some value, while a revert returns None. Furthermore, the focus shifts to arithmetic correctness, and at the middle-level all numbers are modelled as integers and the equivalence proof shows that all the uint256 representations from the low-level do not overflow. This mid-level abstraction leaves behind the low-level complexities of memory, state management, and machine words. This representation allows for direct reasoning about the logical correctness of the arithmetic, making it easier to verify critical properties like overflow safety and expected behaviour under valid or invalid inputs.Let us next examine each phase in detail, using a function from the verifier that is representative of the key challenges and outcomes.
Our running example is the evaluateLagrangePolyOutOfDomain function, which computes the $i^{th}$ term of a Lagrange polynomial:
and which is implemented in the ZKsync verifier as follows:
function evaluateLagrangePolyOutOfDomain(polyNum, at) -> res {
let omegaPower := 1
if polyNum {
omegaPower := modexp(OMEGA, polyNum)
}
res := addmod(modexp(at, DOMAIN_SIZE), sub(R_MOD, 1), R_MOD)
// Vanishing polynomial can not be zero at point `at`
if iszero(res) {
revertWithMessage(28, "invalid vanishing polynomial")
}
res := mulmod(res, omegaPower, R_MOD)
let denominator := addmod(at, sub(R_MOD, omegaPower), R_MOD)
denominator := mulmod(denominator, DOMAIN_SIZE, R_MOD)
denominator := modexp(denominator, sub(R_MOD, 2))
res := mulmod(res, denominator, R_MOD)
}
The relationship between the implementation and the above formula is as follows:
polyNum;at;OMEGA;DOMAIN_SIZE;R_MOD, which is the size of the field, also denoted by $R$ (hence the use of the addmod, mulmod, and modexp functions, the last of which performs % R_MOD implicitly after the exponentiation, rather than having it passed in as a parameter); and
The not-particularly-readable code below is the extracted version of evaluateLagrangePolyOutOfDomain into EasyCrypt using our modified solidity compiler.
proc usr_evaluateLagrangePolyOutOfDomain(usr_polyNum : uint256, usr_at : uint256): uint256 = {
var usr_res, usr_omegaPower, _1, tmp266, _2, _3, _4, _5, _6, tmp267, _7, _8, _9, tmp268, _10, usr_denominator, _11, _12, tmp269;
usr_omegaPower <- (W256.of_int 1);
if ((bool_of_uint256 usr_polyNum))
{
_1 <- (W256.of_int 13446667982376394161563610564587413125564757801019538732601045199901075958935);
tmp266 <@ usr_modexp(_1, usr_polyNum);
usr_omegaPower <- tmp266;
}
_2 <- (W256.of_int 21888242871839275222246405745257275088548364400416034343698204186575808495617);
_3 <- (W256.of_int 1);
_4 <- (_2 - _3);
_5 <- (W256.of_int 67108864);
tmp267 <@ usr_modexp(usr_at, _5);
_6 <- tmp267;
usr_res <- (PurePrimops.addmod _6 _4 _2);
_7 <- (PurePrimops.iszero usr_res);
if ((bool_of_uint256 _7))
{
_8 <- (W256.of_int STRING (*invalid vanishing polynomial*));
_9 <- (W256.of_int 28);
tmp268 <@ usr_revertWithMessage(_9, _8);
}
usr_res <- (PurePrimops.mulmod usr_res usr_omegaPower _2);
_10 <- (_2 - usr_omegaPower);
usr_denominator <- (PurePrimops.addmod usr_at _10 _2);
usr_denominator <- (PurePrimops.mulmod usr_denominator _5 _2);
_11 <- (W256.of_int 2);
_12 <- (_2 - _11);
tmp269 <@ usr_modexp(usr_denominator, _12);
usr_denominator <- tmp269;
usr_res <- (PurePrimops.mulmod usr_res usr_denominator _2);
return usr_res;
}
Before comparing the extracted and original code, let us clarify for the reader some of the details of the EasyCrypt syntax and semantics, even though they have close resemblance to other imperative languages:
var keyword;<-) and another for its imperative (impure) subset (<@);bool_of_uint256 to cast an uint256 into an EasyCrypt boolean;PurePrimops come from our Yul EasyCrypt model;usr_ either come from the verifier or the precompiled contracts (such as modexp), which are compiled separately into EasyCrypt.With this in mind, we turn to the extracted code, but only to see that the Solidity compiler does not do the best job in preserving the original Yul as it has optimisations that cannot be turned off, such as the introduction of temporary variables and the unfolding of constants. From this code, we observe that, for example:
OMEGA = 13446667982376394161563610564587413125564757801019538732601045199901075958935;RMOD = 21888242871839275222246405745257275088548364400416034343698204186575808495617; andDOMAIN_SIZE = 67108864.
To somewhat recover the original program structure, we introduce the first, low-level, specification:
proc low(polyNum: uint256, at: uint256): uint256 = {
var ret, omegaPower, tmp267, _10, denominator;
omegaPower <- (W256.of_int 1);
if ((bool_of_uint256 polyNum))
{
omegaPower <@ Modexp.low(OMEGA, polyNum);
}
tmp267 <@ Modexp.low(at, DOMAIN_SIZE);
ret <- (PurePrimops.addmod tmp267 (R_MOD - W256.one) R_MOD);
if ((bool_of_uint256 (PurePrimops.iszero ret)))
{
RevertWithMessage.low(W256.of_int 28, W256.of_int STRING);
}
ret <- (PurePrimops.mulmod ret omegaPower R_MOD);
_10 <- (R_MOD - omegaPower);
denominator <- (PurePrimops.addmod at _10 R_MOD);
denominator <- (PurePrimops.mulmod denominator DOMAIN_SIZE R_MOD);
denominator <@ Modexp.low(denominator, (R_MOD - (W256.of_int 2)));
ret <- (PurePrimops.mulmod ret denominator R_MOD);
return ret;
}
This transformation is a simple: we reintroduce constants, eliminate unnecessary temporary variables and use low specifications of dependent procedures (in this case Modexp.low) With this specification in place, we can prove our first program equivalence between usr_evaluateLagrangePolyOutOfDomain and low:
lemma evaluateLagrangePolyOutOfDomain_extracted_equiv_low:
equiv [
usr_evaluateLagrangePolyOutOfDomain ~ EvaluateLagrangePolyOutOfDomain.low :
={arg, glob EvaluateLagrangePolyOutOfDomain} ==>
={res, glob EvaluateLagrangePolyOutOfDomain}
].
Let us unpack this statement in detail. First of all, we are introducing a new lemma called evaluateLagrangePolyOutOfDomain_extracted_equiv_low that we can use later in other proofs. In EasyCrypt, one can prove various properties about cryptographic programs, one of which is program equivalence. This is expressed by the syntax equiv [p1 ~ p2 : S ==> R], where:
p1 and p2 are the procedures to be checked for equivalence;S is the pre-condition;R is the post-condition; andarg, res and glob are special EasyCrypt variables that hold, respectively, the procedure arguments, the procedure return value, and the global variables of a given module.Also, note that writing ={a} is syntactic sugar for a{1} = a{2}, where the {1/2} indexing denotes to which program a variable belongs. With this in mind, and going back to our lemma, what we prove is that the extracted Lagrange function and its low-level specification are equivalent, that is, that if given the same arguments (={arg}) and starting from the same initial global state (={glob EvaluateLagrangePolyOutOfDomain}), they return the same result (={res}) and have the same final global state.
The next step is to lift the specification to the mid-level, where, as discussed above, we abstract away any machine representation (memory and reverts), focusing on integer arithmetic correctness and, more importantly, checking for the absence of over and underflow. For our running example of the Lagrange function, the mid-level specification is as follows:
proc mid(polyNum: int, at: int): int option = {
var r, omegaPolyNum, atDomainSize, zd1, num, den, inv;
omegaPolyNum <- (Constants.OMEGA ^ polyNum) %% Constants.R;
atDomainSize <- (at ^ Constants.DOMAIN_SIZE) %% Constants.R;
zd1 <- (atDomainSize - 1) %% Constants.R;
if (zd1 = 0) {
r <- None;
} else {
num <- (omegaPolyNum * zd1) %% Constants.R;
den <- (Constants.DOMAIN_SIZE * (at - omegaPolyNum)) %% Constants.R;
inv <- (den ^ (Constants.R - 2)) %% Constants.R;
r <- Some ((num * inv) %% Constants.R);
}
return r;
}
and we can see how it makes the reasoning more abstract in the following ways:
addmod tmp267 (R_MOD - W256.one) R_MOD has become (atDomainSize - 1) % R (doing the same for division requires some further finite-field properties, which come into play at the high level);Modexp.low(a, b)are replaced with pure assignments using its return value, $a^{b} \mod R$; andNone if a revert has occurred).The lemma that states the equivalence between the low-level and mid-level specifications is as follows:
lemma evaluateLagrangePolyOutOfDomain_low_equiv_mid
(poly256 at256: uint256) (memory: mem):
equiv [
EvaluateLagrangePolyOutOfDomain.low ~ EvaluateLagrangePolyOutOfDomain.mid :
arg{1} = (poly256, at256) /\
arg{2} = (to_uint poly256, to_uint at256) /\
!Primops.reverted{1} /\ Primops.memory{1} = memory
==>
( ((to_uint at256) ^ Constants.DOMAIN_SIZE - 1) %% Constants.R <> 0 /\
!Primops.reverted{1} /\
res{2} = Some (to_uint res{1}) ) /\
0 <= to_uint res{1} < Constants.R /\
( exists (v1 v2 v3: uint256),
Primops.memory{1} = lagrange_memory_footprint memory v1 v2 v3 )
\/
( ((to_uint at256) ^ Constants.DOMAIN_SIZE - 1) %% Constants.R = 0 /\
Primops.reverted{1} /\
res{2} = None) )
].
and is substantially more interesting than its extraction-level-to-low-level predecessor. On the syntactic level, we observe that this lemma has three parameters—poly256, at256, and memory—and this is because:
uint256 to int): this we specify by destructing the low-level arguments (arg{1} = (poly256, at256)) and then connecting them to the mid-level arguments (arg{2} = (W256.to_uint poly256, W256.to_uint at256));memory variable;Semantically, the pre-condition, in addition to the above observations, tells us that we are not in a revert state. The post-condition then tells us that either:
!Primops.reverted{1} for the low-level and res{2} = Some (...) for the mid-level);res{2} = Some (to_uint res{1})) and belong to the appropriate field (0 <= to_uint res{1} < Constants.R), noting that R_MOD = Constants.R);exists (v1 v2 v3: uint256), Primops.memory{1} = lagrange_memory_footprint memory v1 v2 v3)); orNote: To keep the proving process, which EasyCrypt performs line-by-line, as simple as possible we prove the equivalence between the low- and mid-level specifications using an in-between specification,mid', available here, in which the impure calls toModexp.lowfrom the low-level spec still persist as calls toModexp.mid, but asModexp.midliterally only returns $a^{b} \mod R$, the equivalence proof betweenmid'andmidis obtained trivially.
Below we have the high-level, and final, specification for the Lagrange function. Its structure is very similar to the mid-level one: the only difference comes from the transition from modular integer arithmetic to high-level cryptographic primitives, such as finite fields and groups on elliptic curves.
proc high(polyNum: int, at: FieldR.F): FieldR.F option = {
var r, omegaPolyNum, atDomainSize, zd1;
omegaPolyNum <- Constants.OMEGAFr ^ polyNum;
atDomainSize <- at ^ Constants.DOMAIN_SIZE;
zd1 <- atDomainSize - (FieldR.inF 1);
if (zd1 = FieldR.zero) {
r <- None;
} else {
r <- Some ((omegaPolyNum * zd1) * ((Constants.DOMAIN_SIZEFr * (at - omegaPolyNum)) ^ (-1)));
}
return r;
}
Observe that the mid-level constants are now represented as field elements through Constants.OMEGAFr and Constants.DOMAIN_SIZEFr, and also that all arithmetic operations—addition, subtraction, multiplication, and exponentiation—are defined over FieldR. The most evident improvement is in the handling of division: what was previously expressed as den ^ (Constants.R - 2) %% Constants.R is now written much more elegantly as den ^ (-1). The equivalence between these two representations was formally proven using finite-field properties from the EasyCrypt field library.
The lemma below states the equivalence between middle and high-level specifications:
lemma evaluateLagrangePolyOutOfDomain_mid_equiv_high
(polyInt: int) (atF: FieldR.F):
equiv [
EvaluateLagrangePolyOutOfDomain.mid ~ EvaluateLagrangePolyOutOfDomain.high :
arg{1} = (polyInt, FieldR.asint atF) /\
arg{2} = (polyInt, atF) /\
0 <= polyInt
==>
omap FieldR.inF res{1} = res{2} /\
omap FieldR.asint res{2} = res{1} /\
(res{2} <> None <=> atF ^ Constants.DOMAIN_SIZE - FieldR.one <> FieldR.zero)
].
and can be summarised as: if both programs receives the same input, they return the same result, and that result is None if and only if $z^N \equiv 1 ~mod~R$.
With all of these lemmas in place, we can prove by transitivity that the extracted code from the function evaluateLagrangePolyOutOfDomain conforms with the high-level specification.
The main outcome of the project is a theorem stating that the main entry point of the verifier smart-contract—the verify() method—conforms to a specification that precisely matches the PLONK [5] and plookup [6] papers. We have written the spec so that the correspondence between the two is evident, and invite the reader to confirm that the expressions landing into the final pairing invocation are precisely those outlined in the aforementioned protocols.
.svg)
The simplest solutions to the hardest
problems in blockchain
Nethermind © 2025
