Greetings! I noticed that there isn’t very much formal verification in this project, so I decided to apply some Coq.
Writing a Cyclers decider seemed like a good starting point, so here it is: GitHub - meithecatte/busycoq: Busy Beaver deciders backed by Coq proof
I decided to approach this with an architecture of untrusted decider written in Rust + a verifier proven correct checking certificates produced by the decider.
Needless to say, the results match the index list linked upthread.
Within the Coq development, I define Turing machines in two ways:
- through small-step semantics, using abstract infinite lists to represent the tape: TM.v
- as an executable function: Compute.v
Of course, both definitions have been proven equivalent. The main reason for this apparent duplication is to make the proof easier, but it also has the nice aspect that each definition gives more reason to trust the other one.
The main correctness theorem can be found in Cyclers.v:
Theorem verify_cycler_correct : forall tm n k,
verify_cycler tm n k = true -> ~ halts tm c0.