[Decider] Cyclers

Deciders
2

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.

2 Likes