Correctness of the read machine for undirected connectivity

On the encoding of an instance I, the read machine Cslib.USTCON.Reader.machine halts with the output [true] if t is reachable from s and [false] otherwise (Cslib.USTCON.Reader.exists_run_eq). Correctness is claimed only on encodings of instances, as computability with respect to an encoding requires; recognising which bit strings are encodings is not formalised.

The proof follows the phases of the machine. The header is counted bit by bit, and the halvings of n give the depth and the walk length of Reingold's graph for a = Nat.size n. A walk starts at the vertex over the slot (s, s) with all labels zero, and each step evaluates the rotation map in place: the evaluation on slots written as pairs of numbers follows the evaluation on Fin n × Fin n (Cslib.RotationMap.iterate_reingoldEvalStep_mapVertex), whose step of the original graph is the rotation map of the regular rotation map of the instance (Cslib.USTCON.Reader.slotRotN_val), reading the adjacency matrix, so it computes the rotation map of Reingold's graph (Cslib.RotationMap.exists_iterate_reingoldEvalStep). The labels of the walk of the counter c are the digits of c in base 257 ^ 8, and every sequence of labels is the sequence of digits of some counter below (257 ^ 8) ^ T, so the machine accepts exactly when some walk of length T ends over a slot of t, which is reachability of t by Cslib.Reachability.Reingold.reachable_iff_exists_walk_of_le_two_pow.

Main results

• Cslib.USTCON.Reader.slotRotN_val: the step of the slot graph on pairs of numbers.
• Cslib.USTCON.Reader.exists_run_eq: the machine decides undirected connectivity.

References

• O. Reingold, Undirected connectivity in log-space

The step of the slot graph

def Cslib.USTCON.Reader.slotVal {n : ℕ} (v : Fin n × Fin n) : ℕ × ℕ

The slots of Fin n × Fin n as pairs of numbers.

theorem Cslib.USTCON.Reader.slotRotN_val (I : Complexity.USTCONInstance) (v : Fin I.n × Fin I.n) (b : Reachability.Reingold.Label) : slotRotN I.n (slotVal v) b (I.adj v.1 v.2) = Prod.map slotVal id ((Reachability.Reingold.input I.graph).rot (v, b))

The step of the slot graph on pairs of numbers: given the entry of the adjacency matrix at the slot, slotRotN is the rotation map of the regular rotation map of the instance, read through the values of the slots.

Runs without output

def Cslib.USTCON.Reader.Reaches (I : Complexity.USTCONInstance) (q q' : State) : Prop

q' is reached from q on the encoding of I, without output.

theorem Cslib.USTCON.Reader.Reaches.refl {I : Complexity.USTCONInstance} (q : State) : Reaches I q q

theorem Cslib.USTCON.Reader.Reaches.trans {I : Complexity.USTCONInstance} {q₁ q₂ q₃ : State} (h₁ : Reaches I q₁ q₂) (h₂ : Reaches I q₂ q₃) : Reaches I q₁ q₃

theorem Cslib.USTCON.Reader.readBit_of_addr {I : Complexity.USTCONInstance} {q : State} {A : ℕ} (h : addr q = some A) : machine.readBit I.encode q = I.encode.getD A false

The bit read at an address.

theorem Cslib.USTCON.Reader.readBit_of_addr_none {I : Complexity.USTCONInstance} {q : State} (h : addr q = none) : machine.readBit I.encode q = false

No bit is read without an address.

The header

def Cslib.USTCON.Reader.headerState (I : Complexity.USTCONInstance) : State

The state after the header: the number of vertices, the source and the target are counted, and the halvings start from the depth 524 and the walk length 136240.

Evaluating the rotation map

The walks

noncomputable def Cslib.USTCON.Reader.walkFrom (I : Complexity.USTCONInstance) {m : ℕ} : RotationMap.ReingoldVertex (Fin I.n × Fin I.n) Reachability.Reingold.Label m → ℕ → ℕ → RotationMap.ReingoldVertex (Fin I.n × Fin I.n) Reachability.Reingold.Label m

The walk in the m-th graph of Reingold's transformation of the instance from x along the labels of the digits of w, for j steps.

def Cslib.USTCON.Reader.Outputs (I : Complexity.USTCONInstance) (q : State) (b : Bool) : Prop

The machine halts from q with the output b appended to the output so far.

def Cslib.USTCON.Reader.Success (I : Complexity.USTCONInstance) (m T c : ℕ) : Prop

The walk of the counter c succeeds: it ends over a slot of t.

Every sequence of labels is a counter

The decision

theorem Cslib.USTCON.Reader.exists_run_eq (I : Complexity.USTCONInstance) : ∃ (k : ℕ), machine.halt (machine.run I.encode k).state = true ∧ (machine.run I.encode k).out = [decide (I ∈ Complexity.USTCON)]

The read machine decides undirected connectivity: on the encoding of an instance, it halts with the output [true] if t is reachable from s, and [false] otherwise.