Safegcd iteration bound (checked with Candle ITP)

djb-candle.sh

#  New formally verified proof of #safegcd iteration bound:
#  https://cr.yp.to/2023/hull-light-20230416.sage (script for full
#  run+extras: https://cr.yp.to/2023/hull-light-howto-20230416.sh)
#  Advantages over previous formally verified proofs:
#  (1) covers all input sizes;
#  (2) finishes verifying in 10 minutes;
#  (3) smaller TCB (HOL Light).
#  https://twitter.com/hashbreaker/status/1647709221662646274#m

# assuming Debian or Ubuntu:
#sudo apt install opam wget sagemath -y

# Ubuntu 22.04 needs the --disable-sandboxing
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

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

# takes about 10 minutes
wget https://cr.yp.to/2023/hull-light-20230416.sage
time sage hull-light-20230416.sage > hull-light.ml
# 6.18s user 0.79s system 86% cpu 8.051 total
time ocaml -I "$(camlp5 -where)" camlp5o.cma -init hol.ml \
< hull-light.ml > hull-light.out
# 709.44s user 0.52s system 99% cpu 11:52.33 total

# stronger internal lemmas (optional), takes about 5 hours:
time sage hull-light-20230416.sage exact > hull-light-exact.ml
# 1255.09s user 2.71s system 99% cpu 21:00.10 total
time ocaml -I "$(camlp5 -where)" camlp5o.cma -init hol.ml \
< hull-light-exact.ml > hull-light-exact.out
# 17552.65s user 3.14s system 99% cpu 4:52:59.81 total

cd
git clone https://github.com/CakeML/candle
cd candle
./build-instructions.sh

{
  echo '#use "hol.ml";;'
  grep -v '\<Sys\>' ~/hol-light/hull-light.ml
  echo 'Runtime.abort();;'
} > chull-light.ml
cat chull-light.ml | time ./cake --candle &> chull-light.out
# 728.57s user 1.23s system 99% cpu 12:11.19 total
cat chull-light.ml | time env CML_HEAP_SIZE=8192 CML_STACK_SIZE=8192 \
  ./cake --candle &> chull-light.out
# 534.78s user 1.52s system 99% cpu 8:57.04 total

{
  echo '#use "hol.ml";;'
  grep -v '\<Sys\>' ~/hol-light/hull-light-exact.ml
  echo 'Runtime.abort();;'
} > chull-light-exact.ml
cat chull-light-exact.ml | time env CML_HEAP_SIZE=8192 CML_STACK_SIZE=8192 \
  ./cake --candle &> chull-light-exact.out
# 14213.69s user 14.59s system 99% cpu 3:57:33.98 total