.svg){kind=icon}
Now hiring!
•
INTMAX is a zkRollup layer for Ethereum transfers that focuses on scalability and privacy. It comes with a mathematical specification of the underlying INTMAX2 protocol as well as pen-and-paper proofs of key security properties that the protocol observes.
The process of formalisation (also known as mechanisation) denotes the encoding of pen-and-paper mathematical concepts (in our case, the above-mentioned protocol description) in silico.
Lean is a state-of-the-art interactive theorem prover or proof assistant. One can think of proof assistants as environments specialised for formalisation of mathematics, with which users interact by means of a highly expressive programming language, and within which they can state and prove properties of interest about their formalisations (in our case, security properties of the INTMAX2 protocol).
The past contains numerous examples of how exploits can lead to disastrous consequences, such as loss of funds. Therefore, it is critical for blockchain-related protocols to have the strongest available assurances of correctness and security. With that in mind, pen-and-paper proofs do not suffice: the underlying mathematics is highly complex, the proofs are often lengthy, and important details can be easily overlooked or swept under the rug as trivial, even by the most experienced mathematicians. Proof assistants, on the other hand, machine-check every step of the formalisation, leaving no details unattended and ensuring that every accepted definition is well-formed and that every accepted proof is correct.
The project took us approximately fourteen weeks to complete. The first seven weeks were spent encoding into Lean the concepts described in the paper. This, expectedly, required interaction with the client to fix some minor inconsistencies and clarify certain aspects that were described in natural language only. It took us two more weeks to formalise the pen-and-paper proofs present, and the rest of time was spent on fully fleshing out in Lean some hand-waved parts that we spotted during the formalisation. While some of these turned out to be fairly tricky, there were ultimately no errors found in the over-arching reasoning. This experience highlights both the clarity and design capabilities of the protocol developers as well as the benefits of formalisation in bringing every single detail to the surface and providing the strongest correctness guarantees possible.
Throughout the formalisation, we did our best to maintain a clear correspondence with the paper, which we highlight in the body of the blog. There are, however, some minor deviations, with the two requiring a closer look being the following:
We start off by showing in pedagogical detail how the mathematical concepts from the INTMAX paper transfer to Lean, focusing in particular on the high-level correspondence between the formalisation and the pen-and-paper protocol description and the similarities and differences between reasoning in Lean and the way mathematicians normally reason about abstract concepts. In the next section, we will examine how Lean proofs correspond to pen-and-paper proofs, highlighting how well Lean spots missing steps in proof arguments and the results that had to be proven in addition to those explicitly articulated in the INTMAX paper. The full formalisation is available on GitHub, and consists of roughly 5000 lines of what we believe is reasonably optimised and terse Lean code. To the definitions!
The protocol describes a way of transferring tokens by modelling interactions between users and the rollup contract. The interface is simple; a user can submit deposit, transfer or withdrawal requests. We start by describing blocks, which can, expectedly, be either deposit, transfer, or withdrawal blocks. Let K1 and K2 respectively denote disjoint sets of L1 and L2 accounts, K denote the union of K1 and K2, V denote a lattice-ordered Abelian group (onward: an l-group) of values, and let the + subscript denote non-negativity. The three types of blocks are then defined as follows (for simplicity, we delay some of the details regarding transfer blocks for the time being):
This pen-and-paper definition is formalised in the dependent type theory (DTT) of Lean as follows:
.svg)
.svg)
.svg)
.svg)
.svg)
.svg){kind=icon}
.svg)
.svg)
.svg)
.svg)
.svg)
.svg)
.svg)
.svg)
inductive Block (K₁ K₂ : Type) (C Sigma : Type) (V : Type) [PreWithZero V] where
| deposit (recipient : K₂) (amount : V₊)
| transfer (aggregator : K₁) (extradata : ExtraDataT)
(commitment : C) (senders : List K₂)
(sigma : Sigma)
| withdrawal (withdrawals : K₁ → V₊)
While proof assistants in general have progressed substantially over the years, they will never be able to check whether or not mechanised definitions are exactly equivalent to their corresponding pen-and-paper definitions, which are ‘authoritative’ by nature. In that context, maintaining eyeball closeness is simply the easiest way of convincing humans of said equivalence, which is essential for any formalisation.
Another point worth mentioning is how we treat additional requirements (that is, side conditions) on sets/types, which are commonplace in pen-and-paper mathematics, in a DTT proof assistant. Two such side conditions, for example, regarding the above definition of blocks, are that V should be an l-group and that the amount in deposit blocks must be non-negative (captured on paper by the (sub-)type V+). In principle, there are two approaches of handling this:
and our experience with both DTT and Lean shows that one needs to strike a balance between the two, weighing eyeball closeness on the one hand and minimisation of proof effort on the other. For example, we would like to have the ₊ notation to match the paper, and therefore we need to incorporate the concept of non-negativity, which could easily be derived from the more general requirement that V is an l-group. However, characterising an l-group in Lean is both fairly verbose (it is given in full in the section on transition functions further below) and could potentially introduce numerous additional proof obligations to be discharged wherever blocks are used. Moreover, the remaining l-group properties are not relevant for this particular definition. For these reasons, we require a less complex algebraic structure on V, PreWithZero, which can be extended to an l-group and which allows us to define just the non-negative subtype of a given type, NonNeg, together with the ₊ shorthand:
class abbrev PreWithZero (α : Type) := Preorder α, Zero α
def NonNeg (α : Type) [PreWithZero α] := { a : α // 0 ≤ a }
postfix:max "₊" => NonNeg
As blocks conceptually describe transactions, let us next take a look at what transactions are and how they are extracted from blocks. A transaction can informally be viewed as a triple comprising a sender, a recipient and the value that is sent. In the INTMAX paper, transactions $T$ are defined as $T \subseteq \overline{K}^2 \times \mathit{Maybe}(V_+)$, where:
Option/Maybe type used ubiquitously in programming;
but they also come with a validity condition: a transaction, $((s, r), ov)$ is valid if and only if the sender does not equal the recipient, i.e. $s \neq r$, and if the transaction originates from the source account, it always sends a value, i.e. $s = \mathit{Source} \Rightarrow ov \neq \bot$. We can see that this pen-on-paper definition of a transaction as a slightly constrained triple comprising a sender, receiver, and an optional value, corresponds to our above-stated intuition.
The validity condition, unsurprisingly, falls under the above-mentioned side-condition consideration. To maintain eyeball closeness with the paper and also to mitigate certain notational complexities (specifically, carrying around the validity hypothesis whenever a transaction is needed), we bake this condition into the dependent type of transactions. We do so by first carving out the non-dependent portion into an auxiliary type T':
abbrev Τ' (K₁ K₂ V : Type) [PreWithZero V] := Kbar K₁ K₂ × Kbar K₁ K₂ × Option V₊
then defining the validity predicate on values of this type
def isValid (τ : Τ' K₁ K₂ V) :=
match τ with | (s, r, v) => s ≠ r ∧ (s matches .Source → v.isSome)
and then adding the predicate as a side condition of the transaction dependent type, thus obtaining the full transaction type T:
abbrev Τ (K₁ K₂ V : Type) [PreWithZero V] := { τ : Τ' K₁ K₂ V // τ.isValid }
Now that we know what blocks and transactions are, the next step is how to extract the latter from the former. We focus on the case of transfer blocks, which is the most interesting one; deposit and withdrawal blocks are handled fairly straightforwardly in comparison. The pen-and-paper declaration of the associated function is as follows:
A dictionary $\mathit{Dict}(A, B)$ denotes, in essence, a partial function $A \rightharpoonup B$, but is termed as such because of an associated notion of authenticated dictionary schemes, which are a key component of the main security result and which are defined shortly.
Balance proofs carry certain cryptographically relevant data, the full meaning of which we gloss over here (the interested reader can find all of the details in the INTMAX2 paper), but which is modelled faithfully in Lean. The paper defines balance proofs as follows:
abbrev BalanceProof (K₁ K₂ : Type) [Finite K₁] [Finite K₂]
(C Pi V : Type) [PreWithZero V] : Type :=
Dict (C × K₂) ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V)
An authenticated dictionary scheme (AD-scheme) over a key set $K$ and value set $M$ consists of two sets:
and two algorithms:
Further, an AD-scheme should satisfy two important properties, called correctness and binding, defined as follows.
An AD-scheme is correct if for all dictionaries $D \in \mathit{Dict}(K, M)$, with $(C, \pi) \leftarrow \mathsf{Commit}(D)$, it holds that $\mathit{Verify}(\pi_k, k, D_k, C) = \mathit{True}$ for all keys $k \in K$ in the domain of $D$.
An authenticated dictionary scheme is binding if it is computationally infeasible to find a commitment $C \in \mathcal{C}$, a key $k \in K$, values $m_1, m_2 \in M$ and lookup proofs $\pi_1, \pi_2 \in \Pi_l$ such that
which, if we squint hard enough, resembles finding a hash collision.
The corresponding Lean definition of AD-schemes is as follows:
class ADScheme (K : Type)
(M : Type)
(C Pi : Type) where
Commit : Dict K M → CommitT C K Pi
Verify : Pi → K → M → C → Bool
correct_keys_eq : ∀ {dict : Dict K M}, (Commit dict).keys = dict.keys
correct_consistent :
∀ {dict : Dict K M} {key : K} (h : key ∈ dict.keys),
Verify (Commit dict)[key] key dict[key] (Commit dict).commitment = true
binding : ComputationallyInfeasible <|
∃ (c : C) (k : K) (m₁ m₂ : M) (π₁ π₂ : Pi),
Verify π₁ k m₁ c = true ∧ Verify π₂ k m₂ c = true ∧ m₁ ≠ m₂
where the following aspects are worth highlighting:
CommitT to represent the product $\mathcal{C} \times Dict(K, \Pi)$, allowing us mimic the $\pi_k$ way of accessing a key using the syntax $\pi[k]$;correct_keys_eq and correct_consistent, allowing us to use the former in order to show in the latter that the access (Commit dict)[key] is valid, i.e. returns a value, rather than a $\bot$ (or Option.none in our particular case);ComputationallyInfeasible predicate to represent the notion of computational infeasibility, which is ostensibly the most delicate part of the formalisation and requires a dedicated discussion.
ComputationallyInfeasible and the associated axiom
The main security theorem of the paper relies on proving that breaking the binding property is computationally infeasible, meaning that a polynomially bounded adversary has only a negligible probability of breaking it, or, equivalently, that an adversary is able to efficiently find a hash collision. Fully formalising computational infeasibility requires reasoning about probability theory and/or complexity theory, for neither of which there currently exists a sufficient foundation in Lean. While building that foundation is within our capability in principle and, in fact, we plan to build part of it in our (hopefully) future work on formalising and automating Probabilistic Relational Hoare Logic (PRHL) reasoning, this would constitute a massive multi-month or even a year-long effort. With these limitations in place, there are several approaches that one could take, of which we outline two.
In particular, our approach is to define the ComputationallyInfeasible predicate and associated axiom as follows:
opaque ComputationallyInfeasible (p : Prop) : Prop := p
axiom computationallyInfeasible_axiom : ∀ {p : Prop},
ComputationallyInfeasible p → ¬p
By doing so, we abstract the probabilistic and complexity aspects of the standard definition into impossibility. This, however, does not hold in general. For example, we could stipulate that it is not possible to find a hash collision for some hash function, but if we happened to know two distinct values for which the hash function does return the same output, we could use these values to derive a contradiction and prove false, from which we could then prove anything. This must not happen in the formalisation, and we protect against this by
ComputationallyInfeasible definition opaque, so that it cannot be unfolded and then misused, either automatically or manually;computationallyInfeasible_axiom axiom as part of its automated reasoning; andAlternatively, we could have formulated a CollisionFinder algorithm, which efficiently tries to finds a hash collision given a list of requests, and proven that breaking the security properties of the protocol amounts to CollisionFinder actually finding a collision. While this would side-step the probabilistic aspect, the efficiency of the algorithm would still have to be proven on paper. Also, the security property itself would be phrased slightly differently, as a disjunction, which would require careful in-proof checks that we always end up, so to speak, in the correct disjunct.
With respect to the rest of this blog post, the reader should take away from this section that, conceptually, the authenticated dictionary scheme equips our balance proofs with the binding property, effectively promoting them into cryptographically secure partial maps that are needed to withdraw funds from the rollup.
We now finally get back to what it means to extract transactions from a transfer block. To that end, the paper states the following:
Note that up to this point we have primarily described data, but now we need to describe functionality. The corresponding Lean implementation is as follows:
def TransactionsInBlock_transfer
(π : BalanceProof K₁ K₂ C Pi V)
(b : { b : Block K₁ K₂ C Sigma V // b.isTransferBlock }) :
List (Τ K₁ K₂ V) :=
match h : b.1 with
| .transfer _ _ commitment S _ =>
let senderRecipient : Finset (K₂ × Key K₁ K₂) :=
{ (k₂, k) | (k₂ : K₂) (k : Key K₁ K₂) (_h : k₂ ≠ₖ k) }
let sorted : List (K₂ × Key K₁ K₂) := senderRecipient.sort Key.lexLe
let v (s : K₂) (r : Key K₁ K₂) : Option V₊ :=
if s ∉ S
then .some 0
else
if h : (commitment, s) ∈ π.keys
then let (_, t) := π[(commitment, s)]
t r
else .none
sorted.attach.map λ ⟨(s, r), h⟩ ↦ ⟨(s, r, v s r), by valid⟩
| .deposit .. | .withdrawal .. => by aesop
Once again, we follow the paper sentence-by-sentence, trying to maintain eyeball closeness:
let senderRecipient : Finset (K₂ × Key K₁ K₂) :=
{ (k₂, k) | (k₂ : K₂) (k : Key K₁ K₂) (_h : k₂ ≠ₖ k) }
let sorted : List (K₂ × Key K₁ K₂) := senderRecipient.sort Key.lexLe
sorted.attach.map λ ⟨(s, r), h⟩ ↦ ⟨(s, r, v s r), by valid⟩
Let us take a moment here to appreciate the somewhat unexpected guest appearance of by valid. Recall that we use a dependent subtype to define what a transaction T is. As such, whenever we create a transaction (here, (s, r, v s r)), Lean is forcing us to prove its validity. Considering that we often require such proofs, we have defined an automation procedure valid to save time throughout the formalisation process. This can be thought of as us teaching Lean how to prove properties specifically with regards to validity of triples. It is important to note that valid and similar procedures that we define generate proofs that are then checked by Lean; in other words, they do not expand the trust base of the formalisation.
let v (s : K₂) (r : Key K₁ K₂) : Option V₊ :=
if s ∉ S
then .some 0
else
if h : (commitment, s) ∈ π.keys
then let (_, t) := π[(commitment, s)]
t r
else .none
Here, if we squint a bit, we can see that besides a little bit of verification with respect to $\pi$, the function v pretty much just queries the conceptual map that the balance proof represents — note that we query $\pi$ first at sender (π[(commitment, s)]) and then at recipient (t r). And just like this, we obtain a sequence of triples representing transactions.
As mentioned before, extracting transactions from deposit and withdrawal blocks follows a similar pattern and is comparatively simpler. The paper then goes on to state:
which translates to the following Lean definition for extracting transactions from any type of block:
def TransactionsInBlock (π : BalanceProof K₁ K₂ C Pi V)
(b : Block K₁ K₂ C Sigma V) : List (Τ K₁ K₂ V) :=
match h : b with
| .deposit .. => TransactionsInBlock_deposit ↪b
| .transfer .. => TransactionsInBlock_transfer π ↪b
| .withdrawal .. => TransactionsInBlock_withdrawal ↪b
Having the ability to extract transactions from a single block lends itself to an easy generalisation to multiple blocks in sequence. In the paper, this is described as follows:
We extract the transactions from each block and concatenate the lists of partial transactions:
which translates straightforwardly to Lean as follows:
def TransactionsInBlocks (π : BalanceProof K₁ K₂ C Pi V)
(bs : List (Block K₁ K₂ C Sigma V)) : List (Τ K₁ K₂ V) :=
(bs.map (TransactionsInBlock π)).flatten
Transactions, in turn, influence the balances of accounts, that is, the state of balances, denoted by S. This state is mathematically almost just a simple map from accounts to balances (K \to V). However, the paper says that:
and for this we use the same trick as we did with transactions, that is, splitting off the non-dependent part:
abbrev S' (K₁ K₂ V : Type) := Kbar K₁ K₂ → V
encoding the value-dependent part in a predicate:
def isValid (s : S' K₁ K₂ V) := ∀ k : Kbar K₁ K₂, k matches .Source ∨ 0 ≤ s k
and finishing off the definition by bundling isValid with S' to obtain S:
abbrev S (K₁ K₂ V : Type) [Nonnegative V] := { s : S' K₁ K₂ V // s.isValid }
As an aside, note that we use ≤ with flipped arguments rather than ≥ in the definition of isValid. This style is simply more idiomatic in Lean, in that many properties of orderings across various libraries are articulated in terms of ‘less than’, rather than ‘greater than’.
Reflecting on the definition, we can observe that the only account with allowed negative balance is the special $Source$ account. This is because it conceptually represents the sum of all deposits and attempted withdrawals, and in fact, we will be stating important security properties in terms of attackers being unable to withdraw funds in a manner that would leave the rollup with a negative balance.
The next natural step is to understand how transactions influence the underlying rollup state, which is explained by the transaction function. The paper starts by defining it for complete transactions (that is, transactions with a non-$\bot$ known value to transact with) as follows:
Intuitively, $(e_r - e_s)_k$ decides whether we add funds (when $k = r$), subtract funds (when $k = s$), or do nothing (otherwise). Furthermore, $v\ \wedge\ b_s$ should be understood as ‘the minimum between the amount one wants to transfer and the amount they have available’. Therefore, one can at most drain their account completely regardless of how much they attempt to transact.
This is the point at which we need to equip $V$ with its full structure, telling Lean that it is, in fact an l-group. This is done as follows:
variable {V : Type} [Lattice V] [AddCommGroup V]
[CovariantClass V V (· + ·) (· ≤ ·)]
[CovariantClass V V (Function.swap (· + ·)) (· ≤ ·)]
relying on Lean’s typeclass resolution mechanism (the “stuff” enclosed in []) to implicitly equip types with structure, and using variable to implicitly universally quantify subsequent statements. The Lattice and AddCommGroup should be self-explanatory, whereas CovariantClass _ _ f R expresses the idea that $R\ a\ b \rightarrow R\ (f\ x\ a)\ (f\ x\ b)$ , for any $x\ a\ b$.
With this in place, we define $e$ as follows:
def e (i : Kbar K₁ K₂) : Kbar K₁ K₂ → ℤ := λ j ↦ if i = j then 1 else 0
followed by v':
def v' (v : V₊) (b : S K₁ K₂ V) (s : Kbar K₁ K₂) : V₊ :=
match h : s with
| .Source => v
| .key _ => ⟨v ⊓ b s, by simp [h]⟩
and finally, by fc:
def fc (τcXb : Τc K₁ K₂ V × S K₁ K₂ V) : S K₁ K₂ V :=
⟨λ k : Kbar K₁ K₂ ↦
match τcXb with
| ⟨⟨⟨⟨s, r, v⟩, _⟩, hτ⟩, b⟩ =>
let v' := v' (v.get hτ) b s
b k + (e r - e s) k • v',
by rintro (k | _) <;>
aesop (add unsafe apply le_add_of_le_of_nonneg)
⟩
Most of the formalisation mirrors the math definition quite closely. However, there is a little bit of additional clutter. For example, in the definition of v', we are paying the price for the dependent type V_+ by needing to prove that v ⊓ b s is nonnegative using by simp [h]. Next, we have let v' := v' (v.get hτ) b s , which applies v' and convinces Lean that v is not \bot by virtue of the transaction being complete. Finally, we have a proof that the resulting state continues to be isValid:
by rintro (k | _) <;>
aesop (add unsafe apply le_add_of_le_of_nonneg)
which is not exceedingly trivial, but the formalisation is set up by ourselves in a manner such that the aesop proof tactic is able to discharge it. One can think of tactics as algorithms for generating proofs, and aesop is the most general and extensible such tactic in Lean—we will discuss some of the other tactics shortly, once we get to the more complex proofs. This definition also illustrates how discrepancies between papers and their formalisations arise more often because we need to prove additional things rather than us needing to define additional things. In other words, we often simply need to convince Lean of miscellaneous facts that humans tend to gloss over because they are obvious (for some definition of obvious).
To conclude the definition, we need to know what to do for incomplete transactions, in which the value is $\bot$. The way this is done in the paper relies on a preorder relation over $T$ and $S$, the details of which are ultimately not interesting. Before doing that, however, the paper first equips $\overline{K}^2$ with the discrete preorder, which is defined in Lean as:
instance : Preorder (Kbar K₁ K₂) := discretePreorder
Note that we declare this to be an instance, which registers the definition with the typeclass resolution mechanism. This, in turn, allows us to access it for the type Kbar K₁ K₂ implicitly in all subsequent statements. Once the orderings on all of the relevant objects have been put in place, the transaction function is defined as follows:
Then, for all complete transactions $((s,r),v) \in T_c$ and for all $b \in S$ and $k \in \overline{K}$, we define
In Lean, we have the following definition of f:
def f (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) : S K₁ K₂ V :=
⟨
λ k ↦
have : InfSet V := infV b T k
⨅ x : boundedBelow b T, fc x.1 k,
by rintro (k | k)
· unfold iInf sInf infV; simp
rw [if_pos V'_eq_range.symm]
simp
· simp
⟩
where we see that, once again, a bit of proving is necessary to show that the resulting state isValid. While there exists a number of underlying technicalities (such as infV b T k, which shows the existence of the infimum—this is required as the underlying lattice is not complete), the reader can still observe the following correspondence with the paper definition:
x : boundedBelow b T corresponds to the indexing set of the infimum, and x.1 corresponds to the pair $(t’, b’)$;fc x.1 corresponds to $f_c(t',b')$, and therefore fc x.1 k denotes the value of $f_c$ at $k$.
The penultimate step is to define the iterative extension of $f$, denoted by $f^*$ in the paper, and described with a raaaaaaather lengthy description:
which translates to Lean exceptionally straightforwardly, as this is, in fact, the well-known folding pattern from functional programming:
def fStar (Ts : List (Τ K₁ K₂ V)) (s₀ : S K₁ K₂ V) : S K₁ K₂ V :=
Ts.foldl f s₀
Now that we know how transactions influence the rollup state, we are ready to define the balance function, which takes us from a sequence of blocks and an initial state where all balances are zero to a final state that accumulates the changes from all of the transactions extracted from the blocks. The balance function is given in the paper as follows:
whereas in Lean, we have:
def Bal (π : BalanceProof K₁ K₂ C Pi V)
(bs : List (Block K₁ K₂ C Sigma V)) : S K₁ K₂ V :=
fStar (TransactionsInBlocks π bs) (.initial K₁ K₂ V)
The only thing of minor note here is that we use .initial instead of 0 to represent the state where all accounts have a zero-balance. Conceptually, the Bal function computes the balances available to accounts and is an important building block for the operation of INTMAX2.
With all of these definitions in place, we can now state and prove the primary security invariant of the INTMAX2 protocol. Before doing so, however, we take a look at one of many important properties of the balance function to demonstrate how Lean helps us identify and fill the gaps that are often found in pen-and-paper proofs.
The property of Bal that we will be taking a look at is referred to in the paper (somewhat uniformatively, à la Bach’s “Fugue in [note name] [mode]”) as lemma 3 and is stated as follows:
For all balance proofs $\pi \in \Pi$ and block lists $B_* \in B^*$ we have
which translates to Lean as:
lemma lemma3 : Bal π bs .Source ≤ 0
and which tells us that the special $Source$ account always carries non-positive balance. This might seem counter-intuitive, but ultimately makes sense as deposits decrease this value and withdrawals increase it; this is merely a technical detail that is of little consequence and we could, in theory, define these the other way around. The proof then goes as follows:
We start by noticing that the transition function for complete transactions $f_c$ preserves the sum of account balances, i.e.
which translates to Lean as:
lemma sum_fc_eq_sum : ∑ (k : Kbar K₁ K₂), fc (Tc, b) k = ∑ (k : Kbar K₁ K₂), b k
The paper then continues with another statement without actually proving this equality. While omitting proofs is common practice in pen-and-paper mathematics and, more often than not, aids understanding by skipping uninteresting technical details, it does also carry the risk of overlooking an important subtlety that makes the statement false. Alternatively, even if a property is true, its proof might be genuinely tricky without the author foreseeing all of the details of its proof. Be that as it may, Lean enforces that everything is proven up to the very last detail imaginable and, assuming we trust Lean’s kernel, rejects all invalid proofs.
As such, we cannot continue without proving sum_fc_eq_sum. Luckily, the proof is not difficult:
unfold fc
simp [Finset.sum_add_distrib, add_right_eq_self, ←Finset.sum_smul]
and should be read as follows: “The property holds from the definition of fc, from the general simplification lemmas and from the lemmas given between the brackets”.
Lean offers various styles of constructing proofs and there are numerous tradeoffs to consider when proving statements, some of which are human-readability, terseness, ease of construction, robustness to changes to the statement and even proving time, that is, how long are we willing to wait for a proof search procedure to succeed. Considering that this proof is reasonably simple (to the point that the pen-and-paper version does not even do it), we choose a very terse and somehow opaque tactic proof, only giving an outline in terms of relevant lemmas. The paper then continues:
This implies the following fact about the transition function for partial transactions $f$
In Lean, we formalise this as:
lemma sum_f_le_sum : ∑ (k : Kbar K₁ K₂), f b T k ≤ ∑ (k : Kbar K₁ K₂), b k
Once again, the paper does not give a proof, but Lean is adamant on getting one. As this one is somewhat involved yet not very insightful, we are omitting it from the blog. The paper continues:
Then, it follows by induction that we have
or, in Lean:
lemma sum_fStar_le_zero : ∑ (k : Kbar K₁ K₂),
fStar Tstar (S.initial K₁ K₂ V) k ≤ 0 :=
sum_fStar_le_zero_aux (by simp)
The paper is not clear on how to prove this beyond ‘by induction’, and Lean will certainly not let this slide. The above proof does not provide much insight on its own either, other than effectively deferring to a proof of sum_fStar_le_zero_aux, which is a slightly more general property:
private lemma sum_fStar_le_zero_aux (h : ∑ (k : Kbar K₁ K₂), b k ≤ 0) :
∑ (k : Kbar K₁ K₂), fStar Tstar b k ≤ 0
that replaces the initial state with any state b for which h holds. The proof of this statement is then by induction on the structure of the list of transactions as follows:
simp [fStar]
induction Tstar generalizing b with
| nil => aesop
| cons _ _ ih => exact ih (le_trans sum_f_le_sum h)
First, we simplify the definition of fStar. Then, we do induction on the list of transactions Tstar and generalize the inductive hypothesis for all states b. The base case, i.e. nil, is trivial and we can automate it with aesop. The inductive step holds from the inductive hypothesis, transitivity of ≤ and from the lemma sum_f_le_sum. We choose this style of proof as it keeps the code clean, as it allows us to split the statement into two easier-to-prove lemmas.
Once the paper establishes all of these minor facts, it concludes the proof by stating:
which is the statement of the lemma.
This translates so beautifully into Lean that we omit the code to not repeat the above - Lean is now very happy about the proof and confirms that the property holds. As it happens, we only had to conjure a couple of reasonably sized sub-proofs to appease its insistence on checking every single step of every single proof down to the last detail.
There are many more important properties of the balance function needed to prove the main security result, such as lemma 4 and lemma 5. The translation of the proof of the former into Lean is interesting because there is some friction with sets being represented as types. The proof of the latter, on the other hand, was omitted and was therefore written down in Lean by us. With all of this in place, we can formulate and prove the security statement.
Let us first take a look at how the paper states the main security result. It first defines the Attack game 1 as follows:
The security property is then:
The rollup contract is secure if winning Attack game 1 is at least as hard as breaking either the binding property of the authenticated dictionary scheme, or finding a collision of the hash function H.
and from all of this one can conceptually understand how the attack game is defined more formally as follows:
We split this definition into two parts in Lean: we have the attackGame, which encodes 1 and 2, and adversaryWon, which represents 3. The statement of the theorem is then as follows:
theorem theorem1 : ¬adversaryWon (attackGame requests)
At a glance, this does not correspond exactly to ‘the attacker either loses the attack game, or breaks the authenticated dictionary scheme, or finds a hash collision’: this discrepancy is a side effect of the way we model computational infeasibility, which effectively converts the last two disjuncts into false, as these scenarios cannot occur within our model. In the end, the statement says that it is impossible to win the attack game.
Normally, we try to maintain a strong correspondence between Lean proofs and their pen-and-paper counterparts, analogously to what we have done for definitions and statements of properties. This gives us additional confidence that our mechanised model matches the corresponding mathematical model by virtue of us being able to replicate the exact same logical steps. Note that this need not come across as ‘eyeball closeness’, depending on what methodology of proof construction is chosen. Nonetheless, we make sure that the ‘intended’ logical step was taken.
As explained in the introduction, we derived the formal behaviour of the rollup from its description in natural language, as this was the only one available. Furthermore, the proof of theorem 1 relied and continues to rely on intuitive understanding of certain unstated properties of this formal description. As such, in order to maintain the correspondence between the pen-and-paper and the Lean proof here, we essentially force the structure of our proof to align in a way such that every logical step taken in the paper is also explicitly carried out in the Lean proof, even if this might not be the most straightforward way to prove the property given the specifics of our model.
Please note that for the purposes of this exposition, we will not give the full Lean proof nor shall we use the exact phrasing that is in the actual formalisation. We encourage the interested reader to consult the proof in the Github repostiory. The pen-and-paper proof starts us off with:
While this is a perfectly good way to start the pen-and-paper proof, it glosses over the fact that technically speaking, a request does not necessarily end up being turned into its corresponding block should it fail verification. There are several ways to address this, but for the sake of making sure we can replicate the step above, we first prove that the attack game plays out the same regardless of the validity of requests. In other words, we define an auxiliary function normalise that filters requests and only keeps valid ones. We then prove that for all sequences of requests, attackGame requests = attackGame (normalise requests). We can use this property to ‘align’ requests with their corresponding blocks, which allows us to have the following Lean code:
let Bstar := attackGameR requests [] -- (1)
let I := (List.finRange n).filter (Bstar[·].isWithdrawalBlock) -- (2)
let πproofs := (I.attach.map getπ).map Prod.snd -- (3)
The proof continues with:
The resulting contract balance can be computed by adding all deposited amounts and subtracting all withdrawn amounts:
where
and
stating this very authoritatively, almost makes it seem as though a proof is not needed. Lean disagrees. This is one of the the intuitive properties we alluded to that are not shown to follow from the formal description of the rollup contract in the paper. The corresponding Lean is essentially using the lemma:
lemma computeBalance_eq_sum : computeBalance σ = computeBalanceSum σ
where computeBalance comes from the formal description of the rollup contract, that is, adversaryWon is defined in its terms, and computeBalanceSum is the description above. This lemma is then used in the proofs to establish this equality in the following way
rw [computeBalance_eq_sum] at contra
The proof goes on by saying:
We now have two possibilities, either the balance proofs $(\pi_i)_{i \in I}$ have a join in $\Pi$ or they don't.
by_cases eq : ∃ join : BalanceProof K₁ K₂ C Pi V, IsLUB {π | π ∈ πproofs} join
followed by:
Suppose they have a join $\pi \in \Pi$. Then we have
Considering we have all of the lemmas above, we make sure to explicitly use them in sequence to copy the outline given in the paper. The are two points worth making here:
include isπ in the theorem to make this discrepancy transparent. This was our approach as there initially was no formal model for the rollup contract, and this was ‘just another property observed by the natural language description’. Due to the limited duration of the engagement, we did not have the time to perfectly reconcile the definitions.The proof then goes on to examine the remaining scenario, as follows:
'Now, suppose the balance proofs $(\pi_i)_{i \in I}$ do not have a join in $\Pi$.’
which is simply the second case in the proof, as the by_cases above split the proof into two, then
Let $i_k$ be the $k$-th index in $I$ (so that $I = \{i_1,i_2,\dots,i_{m}\}$, where $m = |I|$).
which we get for free, given the representation that we use for $I$, and then
which translates to Lean as:
let πs' := List.Ico 0 (πs.length + 1) |>.map λ i ↦ mergeR'' (πproofs.take i) .initial
where mergeR'' is the recursive procedure for merging balance proofs; an interesting side node here is that a small mistake was unearthed during the formalisation where the pen-and-paper proof did not consider the case where no withdrawals have been sent, thus making the recursive merge ill-defined. The full specifics of merging balance proofs are essential for the proof but not for the intents and purposes of this blog. However, it is worth keeping in mind that merging two balance proofs yields a new balance proof that is isomorphic to the least upper bound of the merged proofs \pi_1 and \pi_2 if and only if \pi_1 is compatible with \pi_2, for some definition of ‘compatible’. This fact is denoted as Proposition 6 in the paper and will become relevant shortly.
The proof then continues:
Clearly, these merged balance proofs are valid, since each of the original balance proofs is valid (otherwise they wouldn’t be accepted by the rollup contract), and since the merge of two valid balance proofs is again valid.
and, as you can imagine by now, ‘clearly’ is not quite enough to convince Lean, and so with an inductive proof that the recursive merge procedure preserves validity (valid_mergeR''), we end up with:
have hπs' : ∀ π ∈ πs', π.Verify (M := (C × K₁ × ExtraDataT)) := by
simp [πs', πproofs]; intros n hn
exact valid_mergeR'' (by simp; omega) (λ _ hx ↦ validπs hx)
The proof then goes on to claim the following:
Now, Proposition 6 gives us that we can merge two compatible balance proof into a new balance proof which is isomorphic to their least upper bound. However, the proof that this recursive merging procedure also computes the least upper bound of several merged balance proofs is missing and is one of the most involved and trickiest proofs in the entire formalisation and constitutes the main inductive argument of the part of the proof with a non-existent infimum. Intuitively, the tricky part here is that the intermediate merged balance proofs need not necessarily, in the general case, constitute a valid least upper bound. We invite the interested reader to start with the prop6_general property and trace all the machinery necessary to prove that this indeed holds. With that property in place, this fact is proven trivially
have : IsLUB {π | π ∈ πproofs} (mergeR'' πproofs .initial) := by
apply prop6_general
-- trivial
and the rest of the proof aligns beautifully as follows:
It then follows from Proposition 6 that there is a key $(C, s) \in \mathsf{AD}.C \times K_2$ such that$\pi'_{k-1}(C,s) \not\simeq \pi{i_k}(C,s)$.
have eq₁ : ∃ key : {k : C × K₂ // π₁! k ≠ .none ∧ π₂! k ≠ .none},
¬(((π₁! key.1) ≅ (π₂! key.1))) :=
-- trivial
obtain ⟨⟨π, salt⟩, t⟩ := (πs'[i-1]'(by omega) key).get prf
obtain ⟨⟨π', salt'⟩, t'⟩ := (πproofs[i-1]'(by simp [hm.symm, m]; omega) key).get prf'
have tneq : t ≠ t' := by -- trivial
Also, since both balance proofs are valid, as remarked earlier, we have
and
have π₁valid : AD.Verify π s (H _ (t, salt)) c := by -- proof omitted
have π₂valid : AD.Verify π' s (H _ (t', salt')) c := by -- proof omitted
by_cases hashEq : H (ω := (C × K₁ × ExtraDataT)) (t, salt) = H _ (t', salt')
meaning that we have found a hash collision
have : Function.Injective (H (ω := (C × K₁ × ExtraDataT))) :=
Function.injective_of_CryptInjective (inj := Hinj) -- AXIOMATISED
have : (t, salt) = (t', salt') := this hashEq
injection this; contradiction
have binding := AD.binding
apply computationallyInfeasible_axiom at binding -- AXIOMATISED
-- trivial
Importantly, note that when it comes to the computational infeasibility axiom, with which we have to deal with extremely carefully, we make its use explicit and delay it until the very last possible moment in the proof.
And that is that. Lean finally relents, giving us the no goals message for the proof. Thus, we can conclude that the attacker cannot, in fact, win the attack game, subject to the following assumptions:
computationallyInfeasible_axiom, which we know to be inconsistent, has not been misused; and
Shiny.
.svg)
The simplest solutions to the hardest
problems in blockchain
Nethermind © 2024
