[Decider] Cyclers

Cyclers: principle

The goal is to decide [Family] Cyclers.

The decider keeps in memory all configurations (i.e. memory tape + head position + machine state) seen during the execution of the machine and returns true if the same configuration is seen twice.

Decider examples and counterexamples

Decider code

https://github.com/bbchallenge/bbchallenge-deciders/tree/main/decider-cyclers

Decider tests

https://github.com/bbchallenge/bbchallenge-deciders/blob/main/decider-cyclers/main_test.go

Results

Subset of application

The decider was applied only on the first 14,322,029 machines of the seed database as they are the ones that exceeded the time limit of 47M steps. It is unlikely that a cycler would exceed the 12k space limit.

This corresponds to 14,322,029 machines tested.

Decider correctness

Proof available at https://github.com/bbchallenge/bbchallenge-proofs/blob/main/deciders/correctness-deciders.pdf.

I’ve created a second implementation of the Cyclers decider(*) in Dafny. Dafny (GitHub - dafny-lang/dafny: Dafny is a verification-aware programming language) is a “verification-aware programming language”. This means that it’s possible to not only write up an implementation, it is possible to ask Dafny to prove that the implementation is correct.

In addition to writing plain code, Dafny allows you to write specifications that describe the expected behavior of your code. The compiler then confirms that all of your specifications are correct. In this case, this culminates in writing:

// This method returns the nth TM state for a program, starting from the
// initial state.
function method machine_iter_n(program: Program, n: nat): MachineStep {
  machine_step_n(program, initial, n)
}

// By definition, a machine halts if there's a step such that at that point, it halts.
predicate program_eventually_halts(program: Program) {
  exists n :: n >= 0 && machine_iter_n(program, n).Halt?
}

predicate program_loops_forever(program: Program) {
  !program_eventually_halts(program)
}

method cyclers_decider(program: Program, time_limit: nat)
returns (finds_loop: bool)
ensures finds_loop ==> program_loops_forever(program) {
  ...
}

In particular, assuming the implementation of the single-step TM function machine_step_n can be trusted, this ensures that when cyclers_decider returns true, the corresponding TM really does halt. This means that bugs in the cyclers_decider function cannot cause false positives!

Differences

In this program, the configuration is described relative to the head of the machine, not relative to the starting position. That means that https://bbchallenge.org/59645887 is a cycler, not a translated cycler!

However, it will still be defeated by other translated cyclers like https://bbchallenge.org/15167997 since the configuration relative to the head of the machine grows without bound.

For this reason, I expect the resolved machines to be a strict superset of the existing cycler output, and a strict subset of the existing translated cycler output.

Decider code

Remaining Tasks
I’ve updated the file to include a basic test; it runs the current BB(5) candidate for 47_176_869 steps and confirms that it has not halted, and then runs for 47_176_870 steps and confirms that it has.

I still need to run the decider itself to confirm the results and make sure that there’s no bugs in the specification.

1 Like

That is fantastic thank you. This is the first effort for formally verifying code so far in bbchallenge.

Thank you for having started this trend!

Really cool. I assume that in order to trust the single-step TM function, a good unittest would be to verify that the 5 state champion, 1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA, does halt after 47,176,870 steps.