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.