Coq-BB5 Formal Verification Project

The proof is parallelized by splitting the TNF tree into several subtrees, each contained in a separate Coq file. The original root represents completely undefined Turing machines and has 8 children.

To optimize proof search, you can leverage symmetry: the four roots using direction L do not need to be searched directly; instead, their computation can be symmetrized to use direction R.

Root Distribution:

• TNF_Root_1.v: explores 0RA---_------_------_------_------
• TNF_Root_2.v: explores 1RA---_------_------_------_------
• TNF_Root_3.v: explores 0RB---_------_------_------_------
• TNF_Root_4.v: explores 1RB---_------_------_------_------. This root is further expanded into 12 children located in the TNF_Root_4/ subfolder.

Leaf Nodes: Files in the TNF_Root_4/ directory marked with _leaf (e.g., TNF_Root_4/TNF_Root_4_3_leaf.v) represent nonhalting children of root_4. These are terminal nodes in the overall TNF tree and do not yield additional subtrees.

The proof for BB(4) = 107 works by enumerating 4-state Turing machines in Tree Normal Form (TNF) and passing them through a pipeline of deciders.

Core Components

• Statement & Theorem: BB4_Statement.v contains the main definitions and theorem, while BB4_Theorem.v is the entry point.
• TNF Enumeration: BB4_TNF_Enumeration.v implements the algorithm that visits machines in a tree structure. It ignores machines whose first head move is Left (due to symmetry) but includes both machines starting with 0 and 1 to simplify the proof.
• Decider Pipeline: Machines are processed by a subset of the BB(5) pipeline (defined in BB4_Deciders_Pipeline.v):
  1. Loops: ../BB5/Deciders/Decider_Loop.v
  2. n-gram Closed Position Set (n-gram CPS): ../BB5/Deciders/Decider_NGramCPS.v
  3. Repeated Word List (RepWL): ../BB5/Deciders/Decider_RepWL.v

Each decider is implemented and proven correct in Coq, ensuring that if they output HALT or NONHALT, the result is mathematically sound.

The system uses two inductive types, WF1 and WF2, to track the valid configuration states of the counter. This ensures that certain invalid states (like a list containing only even numbers in specific positions) are unreachable.

• WF1: A basic configuration where all elements in the list (except potentially the last) are non-zero.
• WF2: A more complex configuration used during specific transitions. It requires elements to be even, a specific odd element y, and non-zero elements in the remainder of the list zs, ending with [O; O].

Transitions between WF1 and WF2 are managed by the pre-conditions of the Increment, Halve, Zero, and Overflow operations to maintain system invariants.

Inductive WF1: (nat*(list nat))->Prop :=
| WF1_intro x xs y:
  Forall Nonzero xs ->
  WF1 (x,xs ++ [y]).

Inductive WF2: (nat*(list nat))->Prop :=
| WF2_intro x xs y zs:
  Forall Nonzero xs ->
  Forall Even xs ->
  Odd y ->
  Forall Nonzero zs ->
  WF2 (x,xs ++ y :: zs ++ [O; O])

The proof follows a specific logical structure involving Tree Normal Form (TNF) enumeration and a pipeline of deciders:

1. TNF Enumeration

The proof enumerates 2-state machines in Tree Normal Form (TNF). The algorithm (BB2_TNF_Enumeration.v) works as follows:

• If a machine halts (meets an undefined transition), the algorithm visits a new subtree of machines representing all possible ways to fill that undefined transition.
• If a machine does not halt, it is treated as a leaf in the TNF tree.
• The enumeration ignores machines whose first head move is Left (due to symmetry) but includes machines starting by writing either 0 or 1 to maintain a simpler proof.

2. Decider Pipeline

Each enumerated machine is passed through a pipeline of deciders (BB2_Deciders_Pipeline.v) to determine if it halts or not. The deciders are programmed and proven correct in Coq. The pipeline for BB(2) includes:

• Loops: See ../BB5/Deciders/Decider_Loop.v.
• n-gram Closed Position Set (n-gram CPS): See ../BB5/Deciders/Decider_NGramCPS.v.

3. Key Files

• BB2_Statement.v: Contains main definitions and the BB(2) = 6 theorem statement.
• BB2_Theorem.v: The entry point of the proof.
• BB2_Deciders_Generic.v: Defines the IDs for the deciders.