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
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
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.