Back to insights

Back to insights

Tutorial: Introduction to Formal Verification with Lean (Part 1)

Elena

Cryptography Engineer

Formal verification is a tool to verify correctness of (mathematical) statements. Where we use pen and paper to write a math proof, we could actually use a formal verification tool to write down the proof in code and get it machine-checked, to know for sure the proof is correct. Examples of these tools are Rocq (formally Coq), Isabelle and, the topic for this tutorial, Lean.

In this tutorial we'll write some simple statements about cryptography and their proofs in Lean. So this aims to be fun for cryptographic engineers who are new to formal verification or want to refresh it.

Specifically, we start at the very beginning of cryptography with the simple One-Time pad (OTP) protocol and show its correctness. This protocol was invented by Miller in 1882 (ref1, ref2) and later again in 1917 by Vernam (who is often credited):

  • Encryption (message m, key k) = m ⊕ k

  • Decryption (ciphertext c, key k) = c ⊕ k

Here, ⊕ is the XOR function. Message, key and ciphertext are all bitstrings of the same length.

OTP is often used in the beginning of learning cryptography, since it's a very simple protocol that gives us perfect security. This means, informally, that a ciphertext reveals nothing about the original plaintext. Claude Shannon, one of the pioneers of Information Security, introduced the concept of perfect security in 1949 and showed OTP is perfectly secure.

The goal for this tutorial is to port written mathematics (about cryptography) from a book to code in Lean. We use the book "A Graduate Course in Applied Cryptography" by Dan Boneh and Victor Shoup, which you can access for free. In this tutorial (part 1) we define the One-Time pad in Lean and show it works correctly, i.e. decryption after encryption returns the original message. In the next tutorial we'll show the OTP is perfectly secure.

This exercise is inspired by the repo VCV-io which contains formalized cryptography proofs and has a folder with examples of varying difficulty. Hopefully, after making some progress regarding the One-Time pad we'll be able to follow along with those examples.

Disclaimer: this is by no means intended to give best practices in Lean, but rather an introduction that might make sense to and be fun for cryptography people.

About Formal Verification in blockchain

You might have heard about formal verification efforts in the blockchain world recently, e.g. Zcash announced their development team Shielded Labs is aiming to formally verify the Orchard circuits after a critical bug was discovered. The lean Ethereum team that is working on the next set of proposed upgrades for Ethereum (a different "lean") aims to formally verify the zkVM they are building. Nethermind formally verified one of the chips in SP1 of Succinct with Lean last year.

In recent months, Vitalik and zkSecurity both published excellent blog posts about the topic. "The Final Form of Software Development" by Yoichi Hirai (zkSecurity) describes the workflow of having AI agents writing RISC-V assembly code accompanied by proofs in Lean for correctness of the code. And Vitalik's blog post talks about what formal verification is and how we can really use it to improve software and Ethereum specifically.

Formal verification can help us have more trust in the systems we use. However, it is not a "perfect" solution either; when writing proofs about systems, there is always a step in between the actual code written and the theorems we are proving. For example, the original code gets compiled and we don't know the exact implications, or we have to model the code that was written (which we can do incorrectly).

To learn more about the conext and pitfalls of formal verification for code and why it is still very valuable, I recommend this eposide of zkPodcast with Alexander Hicks, who leads the formal verification effort in lean Ethereum.

The Lean programming language & proof assistant

Lean was created in 2013 by Leonardo de Moura, then at Microsoft Research. It is a functional programming language and theorem prover.

It can be used by mathematicians to write down their axioms, lemma's and theorems and add proofs where needed. If the proof gets compiled by Lean, that means it's correct (assuming trust in the Lean compiler). The benefit, apart from checkeable proofs, is that it is easier to break up proofs into sub-proofs and collaborate. Furthermore, Lean can help you complete proofs by automatically searching and applying missing pieces.

However, Lean is also "just" a programming language. Specifically, it is a pure functional programming language, meaning its programs don't have side effects and functions are treated as first class values. We'll see more about the latter in the tutorial.

There are many great resources in order to get started with Lean. Here are a few:

(The reason I created this specific exercise even though so many great resources already exist, is the specific overlap with cryptography; VCV-io has amazing proofs for cryptography but is too advanced for beginners and doesn't have tutorials.)

Tutorial

Let's get started. The tutorial has 4 parts after we do a quick "Hello World!" (part 2 is the longest). Everything is in Lean 4 and the idea is for you to code along.

All code shown with line numbers is code that is needed for the final result. Code that has no line numbers is not yet completed or is just to check something and can be safely removed.

Finally, at the beginning of the subsections there is a small comment containing the new concepts shared in that section.

Hello world in Lean

  • the Lean InfoView

  • eval

You can download Lean locally, or use an online editor such as https://live.lean-lang.org/ which will look something like this (below). On the left side you'll write Lean and on the right side is the Lean Infoview with useful information and tips.

To make sure everything works fine, write something like

#eval 1+1
#eval 1+1
#eval 1+1

And verify that the outcome is shown in the InfoView on the right-hand side.

For the traditional "Hello World!", we can do either of the following:

#eval "Hello World!"
#eval String.append "Hello " "World!"
#eval String.append "Hello " (if 1 > 2 then "Lean!" else "World!")
#eval "Hello World!"
#eval String.append "Hello " "World!"
#eval String.append "Hello " (if 1 > 2 then "Lean!" else "World!")
#eval "Hello World!"
#eval String.append "Hello " "World!"
#eval String.append "Hello " (if 1 > 2 then "Lean!" else "World!")

Some properties of Lean:

  • Follows standard mathematical conventions: e.g. #eval 4 + 5 * 6 evaluates to 4+(5*6)=34

  • No parenthesis to hold function arguments, i.e in Lean you write f x instead of f(x)

  • Functions are first-class values in Lean, they get treated just like any value such as a number or a string

But let's not get ahead of ourselves; we'll learn each necessary Lean topic as we go.

What does the book say? I.e. what do we want to port to Lean?

We know more or less what we want to define, but the crux is that for using Lean we need clarity and precision. What exactly do we want to define and how exactly are we going to define it? This is why we use the Boneh & Shoup book, so the math we need is already written out and we only need to worry about translating it to Lean.

First, there is the definition of a Shannon cipher (2.1.1), which has 3 properties. The first two tell us what the encryption and decryption functions are and the last one is the correctness property, which says that decryption after encryption should return the original message.

The specific example we are interested in is the one-time pad, where encryption and decryption are simply XOR-ing:

A significant part of the tutorial will be dedicated to proving the properties of bit-wise exclusive-OR (XOR):

And finally, we can show one-time pad is a Shannon Cipher by proving it adheres to the correctness property:

For this first tutorial we'll do the following simple steps:

  1. Define bitstrings and the XOR function

  2. Prove necessary properties for XOR

    • commutativity

    • associativity

    • the identity element

    • self-inverse

  3. Define a Shannon Cipher, which has

    • an encryption function

    • a decryption function

    • the property that decryption "reverses" encryption (correctness)

  4. Show that a OTP, where encryption and decryption is XOR, is a Shannon Cipher

Ready for some fun? Let's begin.

Tutorial Part 1: Define a BitString and xor

The one-time pad will be defined over keys K, messages M and ciphertexts C which are all bit strings of the same length L; K:= M := C := {0,1}ᴸ.

In the definition of XOR we need addition modulo 2. So it will be helpful for us to see {0,1}ᴸ as ℤ₂ᴸ and use arithmetics over ℤ₂ in Lean.

Finite Fields

  • import libraries

  • Zmod n

First, import the finite field library ZMod from the mathematics library in Lean:

import Mathlib.Data.ZMod.Basic
import Mathlib.Data.ZMod.Basic
import Mathlib.Data.ZMod.Basic

In this predefined library ZMod n defines the integers modulo n, which comes with modular arithmetic pre-implemented. (You can read more about already implemented types by holding Cmd/Ctrl + clicking on them, e.g. checkout ZMod n.)

Tryout some simple modular arithmetic to get familiar with ZMod, for example 5 + 6 mod 7:

#eval (5: ZMod 7) + (6: ZMod 7)
#eval (5: ZMod 7) + (6: ZMod 7)
#eval (5: ZMod 7) + (6: ZMod 7)

Now we can define the domain of K, M, L by creating a new type that is a vector of elements from ZMod 2.

BitString definition

  • Vector

  • dependent type

  • check

A nice thing about Lean is that we don't have to fix bit string length L; we can just say L in ℕ, like we would in math. (Type "\N" to write ℕ in Lean.)

The predefined type Vector α n creates a vector of length n with elements of type α. So we can use Vector (ZMod 2) L for defining our custom type ℤ₂ᴸ:

def BitString (L: ℕ): Type := Vector (ZMod 2) L
def BitString (L: ℕ): Type := Vector (ZMod 2) L
def BitString (L: ℕ): Type := Vector (ZMod 2) L

This is a dependent type, which gives a different instantiation for different values L in ℕ. We can check it: (prefix a comment in Lean with --)

#check BitString 5 --BitString 5 : Type
#check BitString 5 --BitString 5 : Type
#check BitString 5 --BitString 5 : Type

Note that #eval won't work because there is nothing to evaluate, but #check displays the type of the expression, which in this case works fine.

XOR definition

  • implicit parameters

  • currying

  • lambda function

Now we define the function xor on input bit strings x = [x_1, …, x_L] and y = [y_1, …, y_L] to be [x_1 +₂ y_1, …, x_L +₂ y_L] if +₂ is addition modulo 2.

How can we define this in Lean? Think about the function signature in math: ℤ₂ᴸ × ℤ₂ᴸ → ℤ₂ᴸ. There are several options of how to do this (there are always many ways to achieve the same thing in Lean), we'll go with:

Here, parameter L is implicit. Now we need the "function body".
To easily iterate over the two input vectors and add them component-wise, we can use the predefined function zipWith available on vectors. Let's understand the type of zipWith:
def zipWith (f : α → β → φ) (as : Vector α n) (bs : Vector β n) : Vector φ n
def zipWith (f : α → β → φ) (as : Vector α n) (bs : Vector β n) : Vector φ n
def zipWith (f : α → β → φ) (as : Vector α n) (bs : Vector β n) : Vector φ n
It takes as arguments a function f and two vectors as and bs, and returns a vector of the same length as as and bs. Note that the types of the vector elements can be distinct (although it's not the case for xor).
The function type f : α → β → φ means: it takes an element of type α and an element of type β and it returns an element of type φ. In math we would write α × β → φ. The approach Lean uses is called currying; a function with multiple arguments is represented as a sequence of functions, each taking a single argument. This means you can do partial application and makes the code very flexible. So we can read f : α → β → φ as f : α → (β → φ), which shows that when you give it the first element of type α, you end up with a function β → φ to which you then give an element of type β and end up with an output of type φ.
So what zipWith does is walk over two vectors in parallel and performs operation f on the two current elements. In the case of xor we want it to walk over x and y and add them modulo 2.
def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  -- TODO define f
  Vector.zipWith f x y
def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  -- TODO define f
  Vector.zipWith f x y
def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  -- TODO define f
  Vector.zipWith f x y
The final piece of the puzzle is how to define the function f we want to pass to zipWith, knowing it needs to perform addition on the elements. We can use a lambda function, which can be written in a compact way like this: fun x => x + 1 (e.g. return the successor of a natural number).
Putting it together:
def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  Vector.zipWith (fun a b => a + b) x y
def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  Vector.zipWith (fun a b => a + b) x y
def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  Vector.zipWith (fun a b => a + b) x y
Note that this will work correctly, because the type of BitString has elements in ℤ₂ and thus addition will automatically be addition mod 2.
Tutorial Part 2: Prove properties of xor
Okay now the real fun begins!
Just for clarity, the content you should at least have now is:
import Mathlib.Data.ZMod.Basic

def BitString (L: ℕ): Type := Vector (ZMod 2) L

def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  Vector.zipWith (fun a b => a + b) x y
import Mathlib.Data.ZMod.Basic

def BitString (L: ℕ): Type := Vector (ZMod 2) L

def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  Vector.zipWith (fun a b => a + b) x y
import Mathlib.Data.ZMod.Basic

def BitString (L: ℕ): Type := Vector (ZMod 2) L

def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  Vector.zipWith (fun a b => a + b) x y
Or whatever equivalent version works for you! We'll add one more line; before the xor definition:
namespace BitString
namespace BitString
namespace BitString
This will make sure Lean does not get confused with a different already existing xor definition when we start proving things 😅
Continuing to follow the Boneh & Shoup book, we'll now prove the properties as mentioned in the definition of xor (Example 2.1), starting with commutativity:
Prove commutativity of xor; x ⊕ y = y ⊕ x
We start by proving commutativity for XOR, meaning x ⊕ y = y ⊕ x. This first property will take the most time to prove since it contains the first Lean proof of the tutorial. It's split up into 3 steps.
Define lemma for commutativity
  • goals in Lean
  • lemma definition
  • sorry
We'll define the commutativity property as a lemma and then prove it. As soon as you've written down the lemma, Lean will call it the "goal" of what is yet to be proven. Your task is to reduce the current goal into one or more smaller subgoals, which are closer to something you already know is true. Proving your statement then becomes a chain of reduction, similar to breaking up a programming problem into smaller subproblems.
The elements a lemma (or theorem) exist of in Lean:
lemma <name_lemma> <arguments_lemma> : <statement_lemma> := <proof>
lemma <name_lemma> <arguments_lemma> : <statement_lemma> := <proof>
lemma <name_lemma> <arguments_lemma> : <statement_lemma> := <proof>
In this case, the <arguments_lemma> consist of two BitStrings; x and y.
The <statement_lemma> should express the commutativity property we want to prove for x and y: xor x y = xor y x.
The name of the lemma depends on preference; I picked the elegantly short xor_comm_property. Note that for the BitStrings we need the implicit parameter L:
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    sorry -- This is the placeholder until you add the proof
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    sorry -- This is the placeholder until you add the proof
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    sorry -- This is the placeholder until you add the proof
The sorry placeholder is not a crazy invention of mine, this is really the Lean placeholder, which you could read as "sorry I haven't proven it yet".
Prove lemma commutativity: step 1
  • tactics, by
  • ⊢
  • Vector.ext
We'll build our proofs using tactics: instructions that help reduce the current goal. You'll have many different options of steps you can apply, for example:
  • rewrite goal into an equivalent form
  • split goal into several subgoals
  • close a goal when it matches something you already know to be true
We start by removing sorry and replacing it with by, which indicates we're going to prove this using tactics. This is useful, because Lean will help us by showing what our goal is and what progress we're making. It looks something like this:
In the InfoView, Lean says: the goal is to show that for L ∈ ℕ and x,y of type BitString L: x.xor y = y.xor x. (The goal is always preceded by ⊢.)
Onto the proof. What do we know? For every index i, if we calculate the corresponding element on both sides, they will be equal: (x.xor y)[i] = (y.xor x)[i] since (x[i] + y[i]) = (y[i] + x[i]) due to commutativity for addition in ℤ₂.
So if we can split up our goal into L subgoals, ranging over i, then the remaining goal becomes proving a single equality of the single element on both sides.
To achieve this splitting into L subgoals, we can use an extensionality lemma, which says: "2 things are the same if they are made up of the same things". This is a general type of lemma which applies for many types and for a vector it is accessible via Vector.ext (reference). We can use it as follows:
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
Now in the editor you can see the goal has changed to:
L : ℕ
x y : BitString L
⊢ ∀ (i : ℕ) (x_1 : i < L), (x.xor y)[i] = (y.xor x)[i]
L : ℕ
x y : BitString L
⊢ ∀ (i : ℕ) (x_1 : i < L), (x.xor y)[i] = (y.xor x)[i]
L : ℕ
x y : BitString L
⊢ ∀ (i : ℕ) (x_1 : i < L), (x.xor y)[i] = (y.xor x)[i]
So still we have L ∈ ℕ and x,y of type BitString L, but the goal has changed to: for all i ∈ ℕ with i < L: (x.xor y)[i] = (y.xor x)[i]. See the next step for what this really means and how we can continue the proof.
Prove lemma commutativity: step 2
  • intro
  • simp
In the pen-and-paper proof we could continue the proof by fixing an arbitrary i and prove equality for it. We might start by saying "let i ∈ with i < L", to then proceed proving the equality for that fixed i. In Lean this can be expressed as follows:
  1. First, fix the free variable i ∈ ℕ with intro i
  2. Then, make the assumption i < L with intro h_i_lt_L ("hypothesis i less than L")
intro strips the front of the goal and puts it into the local "context" of the proof. It either fixes a variable (as in 1) or assumes an additional hypothesis (as in 2).
You can write them consequently in a single line:
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
Now the goal is:
L : ℕ
x y : BitString L
i : ℕ
h_i_lt_L : i < L
⊢ (x.xor y)[i] = (y.xor x)[i]
L : ℕ
x y : BitString L
i : ℕ
h_i_lt_L : i < L
⊢ (x.xor y)[i] = (y.xor x)[i]
L : ℕ
x y : BitString L
i : ℕ
h_i_lt_L : i < L
⊢ (x.xor y)[i] = (y.xor x)[i]
The part before the goal ⊢ is everything that is in context; the variables we have fixed and the assumptions we have made. The goal is what we now have left to prove.
To finish the proof we'll use the tactic simp ("simplifier") to replace equal expressions. First, we can expand the definition of xor in x.xor y and y.xor x:
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
      simp[xor]
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
      simp[xor]
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
      simp[xor]
Now the goal is:
L : ℕ
x y : BitString L
i : ℕ
h_i_lt_L : i < L
⊢ x[i] + y[i] = y[i] + x[i]
L : ℕ
x y : BitString L
i : ℕ
h_i_lt_L : i < L
⊢ x[i] + y[i] = y[i] + x[i]
L : ℕ
x y : BitString L
i : ℕ
h_i_lt_L : i < L
⊢ x[i] + y[i] = y[i] + x[i]
And at this point we know this is true due to commutativity of addition in ℤ₂. This is an already proven property from ZMod which is called add_comm.
Add simp[add_comm] and voilà, we are done with our first proof!
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
      simp[xor]
      simp[add_comm]
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
      simp[xor]
      simp[add_comm]
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
      simp[xor]
      simp[add_comm]
Confirm on the right in the InfoView that there are no goals left 🫡
Just a few disclaimers before we move on. Is this the fastest, shortest, most elegant way of proving this property? No, no and probably no.
The goal here is to precisely understand every step we are doing. In practice, Lean solves many things automagically for us. However, for educational purposes, I think it is helpful to see and understand every substep, which is why I'm approaching it lengthy and mechanically. In addition, my goal is to understand how a pen-and-paper proof would translate to Lean, before I continue on to the auto-stuff. But feel free to make the proofs as short or as different as you like!
Prove xor_assoc_property of xor; x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z
  • auto-applying in simp
  • merging expressions in simp
Now that we know the general idea, the following proving steps will be much faster. In this step we show xor is associative, i.e. x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z. First, the lemma definition:
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z := 
  sorry
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z := 
  sorry
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z := 
  sorry
Once again, we'll prove this equality at the level of a random single entry for the left and right side, using Vector.ext:
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z := 
  by
    apply Vector.ext
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z := 
  by
    apply Vector.ext
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z := 
  by
    apply Vector.ext
The InfoView shows:
L : ℕ
x y z : BitString L
⊢ ∀ (i : ℕ) (x_1 : i < L), (x.xor (y.xor z))[i] = ((x.xor y).xor z)[i]
L : ℕ
x y z : BitString L
⊢ ∀ (i : ℕ) (x_1 : i < L), (x.xor (y.xor z))[i] = ((x.xor y).xor z)[i]
L : ℕ
x y z : BitString L
⊢ ∀ (i : ℕ) (x_1 : i < L), (x.xor (y.xor z))[i] = ((x.xor y).xor z)[i]
In the previous step we fixed variable i and introduced the hypothesis that i < L. However, here Lean can apply some magic and figure those parts out in simp. It doesn't only apply the rewrite you are passing it; it will browse through all available proven properties and tactics that might be applicable and automatically figure out what works.
So we can move on immediately to proving this equality:
(x.xor (y.xor z))[i] = ((x.xor y).xor z)[i]
(x.xor (y.xor z))[i] = ((x.xor y).xor z)[i]
(x.xor (y.xor z))[i] = ((x.xor y).xor z)[i]
Once again, expanding the definition of xor will bring us a step closer, write simp[xor] and confirm that the expansion into L subgoals is also automatically applied:
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z := 
  by
    apply Vector.ext
    simp[xor]
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z := 
  by
    apply Vector.ext
    simp[xor]
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z := 
  by
    apply Vector.ext
    simp[xor]
The goal per i has turned into:
x[i] + (y[i] + z[i]) = x[i] + y[i] + z[i]
x[i] + (y[i] + z[i]) = x[i] + y[i] + z[i]
x[i] + (y[i] + z[i]) = x[i] + y[i] + z[i]
At this point we can close the goal using the associativity for addition in ℤ₂ with add_assoc. Instead of writing a new line simp[add_assoc], we can merge it in the previous simp:
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z :=
  by
    apply Vector.ext
    simp[xor, add_assoc]
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z :=
  by
    apply Vector.ext
    simp[xor, add_assoc]
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z :=
  by
    apply Vector.ext
    simp[xor, add_assoc]
This closes the goal and therefore the associativity property for xor is proven.
Note that there is still a certain amount of Lean magic automatically being applied. Strictly speaking, x[i] + (y[i] + z[i]) = x[i] + y[i] + z[i] does not have the form a + b + c = a + (b + c) that is expected for add_assoc (notice the difference in parenthesis). Of course, we know that in this case it does mean the same, and I think we can accept Lean's magic, but further down we'll see that it means someone has defined this somewhere in a library we are depending on and that for our own definitions/proofs more strictness might be required.
Define identity element ID for XOR and prove correctness
  • Vector.replicate
  • Vector.ext usage with lambda function
The next thing we need is an identity element for xor. For such an element ID it should hold that for all x: x ⊕ ID = x.
Since xor equals addition in ℤ₂, the identity element should be a bit string with all 0, as addition with 0 mod 2 is identity as well.
How to make a BitString of zeroes of a length, for example L=5? We create a vector of length 5 filled with zeroes and cast it to a BitString (which is a vector with elements in ℤ₂):
#eval (Vector.replicate 5 0: BitString 5)
#eval (Vector.replicate 5 0: BitString 5)
#eval (Vector.replicate 5 0: BitString 5)
In the InfoView you can see this gives a BitString of length 5 filled with zeroes. Now we can generalize this idea for ID:
def BitString_ID {L: ℕ} : BitString L := Vector.replicate L 0
def BitString_ID {L: ℕ} : BitString L := Vector.replicate L 0
def BitString_ID {L: ℕ} : BitString L := Vector.replicate L 0
And we want to show the following property holds: for all x: x ⊕ ID = x.
lemma xor_show_identity {L: ℕ} (x: BitString L): xor x BitString_ID = x :=
    sorry
lemma xor_show_identity {L: ℕ} (x: BitString L): xor x BitString_ID = x :=
    sorry
lemma xor_show_identity {L: ℕ} (x: BitString L): xor x BitString_ID = x :=
    sorry
From the previous steps, we already know that this strategy will work:
  -- by
  --   apply Vector.ext
  --   intro i
  --   simp[xor, BitString_ID]
  -- by
  --   apply Vector.ext
  --   intro i
  --   simp[xor, BitString_ID]
  -- by
  --   apply Vector.ext
  --   intro i
  --   simp[xor, BitString_ID]
So let's tryout something slightly different. Once again we use Vector.ext, but calling it differently. This time we first look at the signature of Vector.ext itself (ref here, but I replaced n by L for clarity):
protected theorem ext {xs ys : Vector α L} (h : (i : Nat) → (_ : i < L) → xs[i] = ys[i]) : xs = ys := sorry
protected theorem ext {xs ys : Vector α L} (h : (i : Nat) → (_ : i < L) → xs[i] = ys[i]) : xs = ys := sorry
protected theorem ext {xs ys : Vector α L} (h : (i : Nat) → (_ : i < L) → xs[i] = ys[i]) : xs = ys := sorry
  • {xs ys : Vector α L} means that xs and ys are implicit types; Lean will deduce them.
  • (h : (i : Nat) → (_ : i < L) → xs[i] = ys[i]) is the argument we need to pass.
  • xs = ys is what holds.
Let's think about how we can pass h : (i : Nat) → (_ : i < L) → xs[i] = ys[i]. It takes two arguments; i and the proof that i < L for length L. The output should be the proof that xs[i] = ys[i]. We know that this proof can be given using simp[xor, BitString_ID].
To write the argument we can use a lambda function as we saw before. Putting it together, we can prove this property for identity as follows:
lemma xor_show_identity {L: ℕ} (x: BitString L): xor x BitString_ID = x :=
  Vector.ext fun i i_less_than_L => by simp [xor, BitString_ID]
lemma xor_show_identity {L: ℕ} (x: BitString L): xor x BitString_ID = x :=
  Vector.ext fun i i_less_than_L => by simp [xor, BitString_ID]
lemma xor_show_identity {L: ℕ} (x: BitString L): xor x BitString_ID = x :=
  Vector.ext fun i i_less_than_L => by simp [xor, BitString_ID]
Actually, because of Lean's magic we could also just use Vector.ext fun _ => by simp [xor, BitString_ID] and it will be figured out correctly as well.
Prove self-inverse of xor; x ⊕ x gives ID
  • exact?, exact
  • mpr
  • rfl
The final property we prove for xor is that each element is its own inverse: for all x: x ⊕ x = ID.
To get started, create the lemma signature and apply the techniques we saw above:
lemma xor_self_inverse {L: ℕ} (x: BitString L): xor x x = BitString_ID :=
  by
    apply Vector.ext
    intro i i_less_than_L
    simp[xor, BitString_ID]
lemma xor_self_inverse {L: ℕ} (x: BitString L): xor x x = BitString_ID :=
  by
    apply Vector.ext
    intro i i_less_than_L
    simp[xor, BitString_ID]
lemma xor_self_inverse {L: ℕ} (x: BitString L): xor x x = BitString_ID :=
  by
    apply Vector.ext
    intro i i_less_than_L
    simp[xor, BitString_ID]
This leaves us at the following point:
By expanding the definitions of xor and BitString_ID using simp[xor, BitString_ID] and narrowing down the goal to a subgoal per i using intro i and intro i_less_than_L, we now only need to show that for all i: x[i] + x[i] = 0.
In ℤ₂ we know this holds - but how do we write this down in Lean?
It turns out Lean is very helpful and apart from solving things automatically, it can also give us suggestions. Type on the next line of the proof: exact? and check the suggestion in the InfoView:
Let's first follow the advice and then understand what it does. Replace exact? by exact CharTwo.add_eq_zero.mpr rfl and confirm that it closes the goal 🎉
Now let's go through it step by step. From the name CharTwo.add_eq_zero we can guess that this applies the property of addition to itself equals zero in a ring of characteristic 2. You can always check the details by pressing Cmd/Ctrl and clicking on the name in the code. In this case the theorem says the following (ref):
theorem CharTwo.add_eq_zero {R : Type u_1} [Ring R] [CharP R 2]


theorem CharTwo.add_eq_zero {R : Type u_1} [Ring R] [CharP R 2]


theorem CharTwo.add_eq_zero {R : Type u_1} [Ring R] [CharP R 2]


The iff(↔) gives us 2 functions:
  • mp: from left to right (a + b = 0) → (a = b)
  • mpr: from right to left (a = b) → (a + b = 0)
Applied to the lemma we're working on, CharTwo.add_eq_zero.mpr says: given a proof that x[i] = x[i], it follows that x[i] + x[i] = 0.
The final thing we need is rfl which deems two things equal if they are equal by computation. In this case we can use it as a proof that x[i] = x[i] and together they prove the full goal:
lemma xor_self_inverse {L: ℕ} (x: BitString L): xor x x = BitString_ID := 
  by
    apply Vector.ext
    intro i i_less_than_L
    simp[xor, BitString_ID]
    exact CharTwo.add_eq_zero.mpr rfl
lemma xor_self_inverse {L: ℕ} (x: BitString L): xor x x = BitString_ID := 
  by
    apply Vector.ext
    intro i i_less_than_L
    simp[xor, BitString_ID]
    exact CharTwo.add_eq_zero.mpr rfl
lemma xor_self_inverse {L: ℕ} (x: BitString L): xor x x = BitString_ID := 
  by
    apply Vector.ext
    intro i i_less_than_L
    simp[xor, BitString_ID]
    exact CharTwo.add_eq_zero.mpr rfl
Tutorial Part 3: Define a Shannon cipher
  • Create a new type using structure
We're getting closer to the end of this tutorial. The final pieces are to define the Shannon cipher as per the book and then show that a One-Time pad is indeed a Shannon cipher.
First, let's recall the definition from the book we're following:
We need to introduce a new type which has:
  • an encryption function
  • a decryption function
  • a correctness property
For this, we'll be using a structure in Lean. This is just like a struct in other languages. For example, if we want to define a point with an x and y, both Floats:
structure Point where
  x : Float
  y : Float
structure Point where
  x : Float
  y : Float
structure Point where
  x : Float
  y : Float
How can we apply this to our case for a ShannonCipher? First of all, we need the definition to be for a certain message space M, key space K and ciphertext space C.
To make a structure generic for a type you can do:
structure Point (T: Type) where
  x : T
  y : T
structure Point (T: Type) where
  x : T
  y : T
structure Point (T: Type) where
  x : T
  y : T
So let's make a skeleton to fill out:
structure ShannonCipher (K M C: Type) where
  enc: sorry
  dec: sorry
  correctness: sorry
structure ShannonCipher (K M C: Type) where
  enc: sorry
  dec: sorry
  correctness: sorry
structure ShannonCipher (K M C: Type) where
  enc: sorry
  dec: sorry
  correctness: sorry
Note that this doesn't require K,M and C to have the same type. Writing (K M C: Type) is equivalent to (K: Type) (M: Type) (C: Type) which might indicate more clearly these are separate generic types.
Now we define what types the fields of ShannonCipher have. Encryption takes a key and a message and gives an output in the ciphertext space. The function signature in math is K × M → C. In Lean, this is expressed as K → M → C (recall the currying explanation from earlier).
The decryption function takes a key and a ciphertext and the output is in the message space. Let's add these pieces to the definition (write "\r" to get → in Lean):
structure ShannonCipher (K M C: Type) where
  enc: K → M → C
  dec: K → C → M
  correctness: sorry
structure ShannonCipher (K M C: Type) where
  enc: K → M → C
  dec: K → C → M
  correctness: sorry
structure ShannonCipher (K M C: Type) where
  enc: K → M → C
  dec: K → C → M
  correctness: sorry
Finally there is the definition of correctness. The book says this property is: 
∀ k ∈ K, m ∈ M: dec(k, enc(k,m)) = m
In Lean we can write this as (type "\forall" to get ∀ in Lean):
correctness: ∀ (k: K) (m: M), dec k (enc k m) = m
correctness: ∀ (k: K) (m: M), dec k (enc k m) = m
correctness: ∀ (k: K) (m: M), dec k (enc k m) = m
Lean can also derive the types for k and m. Thus the final definition can be:
structure ShannonCipher (K M C: Type) where
  enc: K → M → C
  dec: K → C → M
  correctness: ∀ k m, dec k (enc k m) = m
structure ShannonCipher (K M C: Type) where
  enc: K → M → C
  dec: K → C → M
  correctness: ∀ k m, dec k (enc k m) = m
structure ShannonCipher (K M C: Type) where
  enc: K → M → C
  dec: K → C → M
  correctness: ∀ k m, dec k (enc k m) = m
Double check we can instantiate ShannonCipher with 3 different types:
#check ShannonCipher Nat String Bool
#check ShannonCipher Nat String Bool
#check ShannonCipher Nat String Bool
Onto the final step!
Tutorial Part 4: Prove that One-Time pad is a ShannonCipher
  • create a value of a structure type
  • syntactic sugar for fun args =>
Finally, we are instantiating a One-Time pad as a ShannonCipher. To do this we need to:
  1. Pass the correct values for (K M C: Type).
  2. Define the enc/dec as applying xor.
  3. Prove the correctness property holds. We'll follow the proof as it's given in the book.
To create a value of a type defined with a structure, provide values for all of its fields. Following the structure example of the previous subsection Point; the point (0,0) can be defined as a value as follows (example from Functional Programming in Lean, ref):
structure Point where
  x : Float
  y : Float
  
def origin : Point := { x := 0.0, y := 0.0 }
structure Point where
  x : Float
  y : Float
  
def origin : Point := { x := 0.0, y := 0.0 }
structure Point where
  x : Float
  y : Float
  
def origin : Point := { x := 0.0, y := 0.0 }
In addition, if we used the generic version of Point (structure Point (T: Type) where ...) we need to add the type explicitly:
def origin : Point Float := { x := 0.0, y := 0.0 }
def origin : Point Float := { x := 0.0, y := 0.0 }
def origin : Point Float := { x := 0.0, y := 0.0 }
For the OTP we set K := M := C := {0,1}ᴸ, which is the type BitString (L: ℕ) that we defined earlier, so we can start the OTP like this:
def OneTimePad (L : ℕ) : ShannonCipher (BitString L) (BitString L) (BitString L) :=
  { 
    enc := sorry,
    dec := sorry,
    correctness := sorry 
  }
def OneTimePad (L : ℕ) : ShannonCipher (BitString L) (BitString L) (BitString L) :=
  { 
    enc := sorry,
    dec := sorry,
    correctness := sorry 
  }
def OneTimePad (L : ℕ) : ShannonCipher (BitString L) (BitString L) (BitString L) :=
  { 
    enc := sorry,
    dec := sorry,
    correctness := sorry 
  }
For the definition of enc and dec we can use lambda functions again:
enc := fun k m => xor k m
dec := fun k c => xor k c
enc := fun k m => xor k m
dec := fun k c => xor k c
enc := fun k m => xor k m
dec := fun k c => xor k c
In Lean you can express things in different ways, so we can use some syntactic sugar to express the above code slightly differently. fun args => can be replaced by bringing the arguments args to the left of :=:
enc k m := xor k m
dec k c := xor k c
enc k m := xor k m
dec k c := xor k c
enc k m := xor k m
dec k c := xor k c
The final step is the value of correctness, which should be a proof. We write the proof as stated in the book, recall from Example 2.1:
In order the following properties are applied:
  1. substitution of actual encryption function by xor
  2. substitution of actual decryption function by xor
  3. associativity of xor
  4. self inverse of xor
  5. addition with ID gives self
Start with the proof by replacing sorry with by and check what the Lean InfoView says the goal is:
def OneTimePad (L: ℕ ): ShannonCipher (BitString L) (BitString L) (BitString L) := 
{
  enc k m := xor k m
  dec k c := xor k c
  correctness := 
    by
}
def OneTimePad (L: ℕ ): ShannonCipher (BitString L) (BitString L) (BitString L) := 
{
  enc k m := xor k m
  dec k c := xor k c
  correctness := 
    by
}
def OneTimePad (L: ℕ ): ShannonCipher (BitString L) (BitString L) (BitString L) := 
{
  enc k m := xor k m
  dec k c := xor k c
  correctness := 
    by
}
It shows the goal ⊢ ∀ (k m : BitString L), k.xor (k.xor m) = m for L : ℕ:
This means Lean already did step 1 and 2. So we can directly apply associativity for xor by referencing the lemma that we proved for that property:
correctness := 
    by
      simp[xor_assoc_property]
correctness := 
    by
      simp[xor_assoc_property]
correctness := 
    by
      simp[xor_assoc_property]
This changes the goal to ∀ (k m : BitString L), (k.xor k).xor m = m. Now, apply step 4 using the lemma xor_self_inverse:
correctness := 
    by
      simp[xor_assoc_property]
      simp[xor_self_inverse]
correctness := 
    by
      simp[xor_assoc_property]
      simp[xor_self_inverse]
correctness := 
    by
      simp[xor_assoc_property]
      simp[xor_self_inverse]
The goal is now ∀ (k m : BitString L), BitString_ID.xor m = m. To apply step 5 of the proof we'd like to use the lemma xor_show_identity, but if you try that directly you'll see:
"simp made no progress" - Why? Well, we defined the property as xor x BitString_ID = x, while the current goal is BitString_ID.xor m = m. So while we know this is the same, strictly speaking we haven't shown this is the same. However, we have shown that xor x y = xor y x in the commutativity property with lemma xor_comm_property, so it will work fine if we apply that first.
Verify that the correctness property is proven:
correctness := 
    by
      simp[xor_assoc_property]
      simp[xor_self_inverse]
      simp[xor_comm_property]
      simp[xor_show_identity]
correctness := 
    by
      simp[xor_assoc_property]
      simp[xor_self_inverse]
      simp[xor_comm_property]
      simp[xor_show_identity]
correctness := 
    by
      simp[xor_assoc_property]
      simp[xor_self_inverse]
      simp[xor_comm_property]
      simp[xor_show_identity]
And this completes the definition of the One-Time Pad as a Shannon Cipher, following the book! Now we know (a little bit of) how to grab a cryptography book and implement the content in Lean. Isn't that super cool?
Okay we'll add one final thing to make it slightly cleaner and ready for part 2 of the tutorial where we will prove OTP is perfectly secure. (I'll start working on this soon™)
Recall that we addednamespace BitString before defining xor. This was to ensure Lean wouldn't interpret xor as the already implemented function and magically start solving things for us. The namespace creates a collection of whatever we defined in it. In this case, it makes sense for the BitString "collection" to contains xor, but not to contain ShannonCipher and the definition of OneTimePad.
Leaving it like this would mean that if we add a new file and want to reference the OTP definition, it'd be as BitString.OneTimePad. Not clean!
To solve it, add after the xor lemma's:
end BitString
end BitString
end BitString
Then, in order to use the previously defined functionality, add right before the OneTimePad definition:
open BitString
open BitString
open BitString
The full code then becomes:
import Mathlib.Data.ZMod.Basic

def BitString (L: ℕ): Type := Vector (ZMod 2) L

namespace BitString

def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  Vector.zipWith (fun a b => a + b) x y

-- commutativity
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
      simp[xor]
      simp[add_comm]

-- associativity
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z :=
  by
    apply Vector.ext
    simp[xor, add_assoc]

def BitString_ID {L: ℕ} : BitString L := Vector.replicate L 0

-- identity
lemma xor_show_identity {L: ℕ} (x: BitString L): xor x BitString_ID = x :=
  Vector.ext fun i i_less_than_L => by simp [xor, BitString_ID]

-- self-inverse
lemma xor_self_inverse {L: ℕ} (x: BitString L): xor x x = BitString_ID :=
  by
    apply Vector.ext
    intro i i_less_than_L
    simp[xor, BitString_ID]
    exact CharTwo.add_eq_zero.mpr rfl

end BitString

structure ShannonCipher (K M C: Type) where
  enc: K → M → C
  dec: K → C → M
  correctness: ∀ k m, dec k (enc k m) = m

open BitString

def OneTimePad (L: ℕ ): ShannonCipher (BitString L) (BitString L) (BitString L) :=
{
  enc k m := xor k m
  dec k c := xor k c
  correctness :=
    by
      simp[xor_assoc_property]
      simp[xor_self_inverse]
      simp[xor_comm_property]
      simp[xor_show_identity]
}
import Mathlib.Data.ZMod.Basic

def BitString (L: ℕ): Type := Vector (ZMod 2) L

namespace BitString

def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  Vector.zipWith (fun a b => a + b) x y

-- commutativity
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
      simp[xor]
      simp[add_comm]

-- associativity
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z :=
  by
    apply Vector.ext
    simp[xor, add_assoc]

def BitString_ID {L: ℕ} : BitString L := Vector.replicate L 0

-- identity
lemma xor_show_identity {L: ℕ} (x: BitString L): xor x BitString_ID = x :=
  Vector.ext fun i i_less_than_L => by simp [xor, BitString_ID]

-- self-inverse
lemma xor_self_inverse {L: ℕ} (x: BitString L): xor x x = BitString_ID :=
  by
    apply Vector.ext
    intro i i_less_than_L
    simp[xor, BitString_ID]
    exact CharTwo.add_eq_zero.mpr rfl

end BitString

structure ShannonCipher (K M C: Type) where
  enc: K → M → C
  dec: K → C → M
  correctness: ∀ k m, dec k (enc k m) = m

open BitString

def OneTimePad (L: ℕ ): ShannonCipher (BitString L) (BitString L) (BitString L) :=
{
  enc k m := xor k m
  dec k c := xor k c
  correctness :=
    by
      simp[xor_assoc_property]
      simp[xor_self_inverse]
      simp[xor_comm_property]
      simp[xor_show_identity]
}
import Mathlib.Data.ZMod.Basic

def BitString (L: ℕ): Type := Vector (ZMod 2) L

namespace BitString

def xor {L: ℕ} (x y: BitString L): (BitString L) :=
  Vector.zipWith (fun a b => a + b) x y

-- commutativity
lemma xor_comm_property {L: ℕ} (x y : BitString L) : xor x y = xor y x :=
    by
      apply Vector.ext
      intro i h_i_lt_L
      simp[xor]
      simp[add_comm]

-- associativity
lemma xor_assoc_property {L: ℕ} (x y z: BitString L) : xor x (xor y z) = xor (xor x y) z :=
  by
    apply Vector.ext
    simp[xor, add_assoc]

def BitString_ID {L: ℕ} : BitString L := Vector.replicate L 0

-- identity
lemma xor_show_identity {L: ℕ} (x: BitString L): xor x BitString_ID = x :=
  Vector.ext fun i i_less_than_L => by simp [xor, BitString_ID]

-- self-inverse
lemma xor_self_inverse {L: ℕ} (x: BitString L): xor x x = BitString_ID :=
  by
    apply Vector.ext
    intro i i_less_than_L
    simp[xor, BitString_ID]
    exact CharTwo.add_eq_zero.mpr rfl

end BitString

structure ShannonCipher (K M C: Type) where
  enc: K → M → C
  dec: K → C → M
  correctness: ∀ k m, dec k (enc k m) = m

open BitString

def OneTimePad (L: ℕ ): ShannonCipher (BitString L) (BitString L) (BitString L) :=
{
  enc k m := xor k m
  dec k c := xor k c
  correctness :=
    by
      simp[xor_assoc_property]
      simp[xor_self_inverse]
      simp[xor_comm_property]
      simp[xor_show_identity]
}
If you followed the tutorial, please let me know what you think and nudge me for part 2 via LinkedIn or Twitter.