Verifying leangoppa

D. J. Bernstein, 20230726

leangoppa-20230726 (browse, download) is a collection of computer-verified proofs regarding Goppa decoding. The proofs are written in the Lean language. This page explains how to run Lean to verify the proofs.

Prerequisites: Debian VM with at least 8GB free disk space. Probably adaptations of these instructions can work in other environments.

As root in the VM:

apt install git curl
adduser --disabled-password --gecos leangoppa leangoppa
su - leangoppa

All remaining steps are within the leangoppa account:

curl -sS -o elan-init.sh https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
sh elan-init.sh -y
source $HOME/.elan/env
wget https://cr.yp.to/2023/leangoppa-20230726.tar.gz
tar -xf leangoppa-20230726.tar.gz
cd leangoppa-20230726
time lake exe cache get
time lake build

The lake exe cache get takes roughly a minute depending on your network connection and CPU, and the lake build takes a few minutes depending on your CPU. There will be some Building lines (and timing information from time at the end); in case of failure, there will be further output. To see what a failure looks like, try commenting out a line in Goppadecoding/*.lean (by putting -- at the beginning of the line) and running lake build again.

Beware that Lean is a general-purpose programming language. Malicious code anywhere inside the Lean software or inside leangoppa can spoil verification, destroy files, etc. In other words, the proof verification relies on a large TCB.