Verifying lightgoppa

D. J. Bernstein, 20230811

lightgoppa-20230811 is a collection of computer-verified proofs regarding Goppa decoding. The proofs are written in the HOL Light language. (For comparison, leangoppa-20230726 has essentially the same theorems with proofs written in the Lean language.) This page explains how to run HOL Light to verify the proofs.

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

As root in the VM:

apt install git opam wget -y
adduser --disabled-password --gecos lightgoppa lightgoppa
su - lightgoppa

All remaining steps are within the lightgoppa account:

time opam init -a --disable-sandboxing
time opam switch create 4.05.0
eval `opam env`
time opam pin add camlp5 7.10 -y
time opam install num camlp-streams ocamlfind -y

git clone https://github.com/jrh13/hol-light
cd hol-light
git checkout 29b3e114f5c166584f4fbcfd1e1f9b13a25b7349
make

wget https://cr.yp.to/2023/lightgoppa-20230811.ml
time ocaml -I `camlp5 -where` camlp5o.cma -init hol.ml \
< lightgoppa-20230811.ml > lightgoppa-20230811.out
grep Error lightgoppa-20230811.out

These commands normally produce 40778 lines of output in lightgoppa-20230811.out, including copies of all definitions and proven theorems. The first 80% of the lines are from various HOL Light libraries. The main lightgoppa-20230811 theorem statements are collected at the end. If you comment out a random proof line in lightgoppa-20230811.ml (by putting (* before the line and *) after) then you should end up seeing “Error” in lightgoppa-20230811.out rather than the desired theorems.

On a dual EPYC 7742 server running at 2.245GHz, the timed commands above were observed to take 21 seconds, 307 seconds, 68 seconds, 143 seconds, and 1165 seconds respectively. This server has 128 cores, but most of the time was spent on single-core processing.

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