meithecatte / busycoq

Busy Beaver deciders backed by Coq proof

BusyCoq

Verified implementations of Busy Beaver deciders. The computation is split into two parts:

• First, an untrusted decider, written in Rust, tries to decide whether each machine halts. When it succeeds, it generates a certificate.
• Then, a verifier, proven correct in Coq and extracted to OCaml, checks each certificate and makes sure that it is correct. A Coq theorem guarantees that if the verifier accepts a certificate, then the corresponding machine doesn't halt.

Implemented deciders

• Cyclers
• Translated Cyclers
• Backwards Reasoning
• Bouncers

Individual machines

Apart from deciders, the repository includes manual proofs for some machines considered hard to decide automatically. At the moment, these include:

• Skelet #1 (due to the nature of the proof, the final computation is done by an extracted OCaml program)
• Skelet #10
• Skelet #15
• Skelet #26 (proof contributed by Jason Yuen; I am not aware of the informal argument being outlined anywhere)
• Skelet #33 (proof contributed by Jason Yuen)
• Skelet #34
• Skelet #35
• the five "cubic-finned" machines analyzed by Justin Blanchard (bbchallenge indices 7763480, 8120967, 10756090, 11017998, and 11018487).

Running the deciders

Place the seed database at seed.dat in the root of the repository. Make sure you have Rust, Coq and OCaml installed. Then,

cd beaver
cargo build --release
time target/release/beaver decide ../seed.dat ../certs.dat
cd ../verify
make
time ./verify ../seed.dat ../certs.dat ../decided.dat

A binary file listing the database indices of all successfully decided machines will be generated at decided.dat.

Results

Cyclers:
  11229238 Decided
         0 OutOfSpace
   3092791 OutOfTime
         0 Halted
  74342035 NotApplicable
Translated Cyclers:
  73860624 Decided
         0 OutOfSpace
    481411 OutOfTime
         0 Halted
   3092791 NotApplicable
Backwards Reasoning:
   2035576 Decided
    979028 OutOfSpace
    559598 OutOfTime
Bouncers:
   1406032 Decided
     23433 OutOfSpace
    109161 OutOfTime
         0 Halted

    132594 Undecided

real	2m11.670s
user	25m32.012s
sys	0m3.364s

Here are some results from an earlier run with higher limits (50M steps, 64k tape cells) on the Translated Cyclers decider:

chikara:~/dev/busycoq/beaver$ \time target/release/beaver decide
Cyclers:
  11229238 Decided
         0 OutOfSpace
   3092791 OutOfTime
         0 Halted
  74342035 NotApplicable
Translated Cyclers:
  73861173 Decided
    138452 OutOfSpace
    342410 OutOfTime
         0 Halted
   3092791 NotApplicable
10784.09user 136.66system 15:12.51elapsed 1196%CPU (0avgtext+0avgdata 10180maxresident)k
0inputs+2794536outputs (0major+2590minor)pagefaults 0swaps
chikara:~/dev/busycoq/verify$ \time ./verify
79.89user 0.41system 1:20.32elapsed 99%CPU (0avgtext+0avgdata 124288maxresident)k
0inputs+664776outputs (0major+30600minor)pagefaults 0swaps