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