Graph reachability

DefinitionEncoding of a PATH instance#✓fully proved

Writing \(1\) for true and \(0\) for false, the instance with source \(s\), target \(t\) and the digraph given by \(n\) and the edge list \(E\) is encoded as \(s\) ones, a zero, \(t\) ones, a zero, then \(n\) ones and a zero, followed, for each pair \((u, v)\) of \(E\) in order, by \(u\) ones, a zero, \(v\) ones and a zero.

def encodeP (s t n : ℕ) (es : List (ℕ × ℕ)) : List Bool :=
  List.replicate s true ++ false :: (List.replicate t true ++ false :: Karp.encodeE n es)

Uses 1 · Used by 16

Statement usesBit-string encoding of a graph

Used byThe HAMPATH problem · A fixed HAMPATH no-instance · Sipser's HAMPATH instance of a CNF formula · The verifier on an encoded instance and witness · What the HAMPATH verifier accepts · Length of an encoded PATH instance · HAMPATH is verified with quadratic-size witnesses · HAMPATH on an encoded instance · HAMPATH rejects the fixed no-instance · SAT ≤ HAMPATH preserves membership · Correctness and running time of the Hamiltonian path verifier · Decoding inverts the PATH instance encoding · The PATH instance parser succeeds exactly on encodings · The PATH instance encoding is injective · The PATH problem · The marking algorithm decides PATH

DefinitionDecoding a PATH instance#✓fully proved

Writing \(1\) for true and \(0\) for false, a bit string \(x\) is parsed by reading a unary number \(s\) (a run of ones ended by a zero), then a unary number \(t\) from the rest, then a graph from what remains: a unary number \(n\) followed by pairs \((u, v)\) of unary numbers until the input ends. The result is \((s, t, n, E)\), with \(E\) the list of these pairs in order; there is no result unless the input ends right after \(n\) or right after a complete pair.

def decodeP (x : List Bool) : Option (ℕ × ℕ × ℕ × List (ℕ × ℕ)) :=
  match readUnaryLength x with
  | none => none
  | some (s, r) =>
      match readUnaryLength r with
      | none => none
      | some (t, r') => (Karp.decodeE r').map fun p => (s, t, p.1, p.2)

Uses 2 · Used by 13

Statement usesDecoding a graph · Reading a unary length prefix

Used byThe HAMPATH verifier · The verifier on an encoded instance and witness · What the HAMPATH verifier accepts · Instances that do not decode are rejected · Witnesses that do not decode are rejected · Correctness and running time of the Hamiltonian path verifier · Decoding inverts the PATH instance encoding · The PATH instance parser succeeds exactly on encodings · The PATH instance encoding is injective · The marking algorithm for PATH · The marking algorithm reads the mark of the target · The marking algorithm decides PATH · Running time and output of the marking machine

DefinitionArcs of the PATH digraph#✓fully proved

For \(n \in \mathbb{N}\) and a list \(E\) of pairs of natural numbers, there is an arc from \(u\) to \(v\) when the pair \((u, v)\) occurs in \(E\), \(u < n\) and \(v < n\); listed pairs with an end at least \(n\) give no arc.

def arc (n : ℕ) (es : List (ℕ × ℕ)) (u v : ℕ) : Prop := (u, v) ∈ es ∧ u < n ∧ v < n

Used by 22

Used byHamiltonian paths · Checking a vertex list against the arcs · The Hamiltonian path check is correct · Hamiltonian paths of Sipser's graph have normal detours · Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs · HAMPATH is verified with quadratic-size witnesses · A clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · A Hamiltonian path visits every vertex · The machine's walk is the check · Consecutive vertices of the contracted path are joined by arcs · A satisfying choice gives a Hamiltonian path · Backward direction of SAT ≤ HAMPATH for paths with normal detours · Every vertex of the contracted path except its end has a successor · Every top but the last is followed by an end of its row · HAMPATH rejects the fixed no-instance · Entering a row and leaving it at once is impossible · A row entered at one end is run to the other end · The PATH problem · The marking algorithm decides PATH · The final marks are exactly the reachable vertices

DefinitionThe PATH problem#✓fully proved

PATH is the decision problem that accepts a bit string \(x\) exactly when \(x\) is the encoding of some instance \((s, t, n, E)\) with \(s < n\), \(t < n\) and a sequence \(s = v_0, v_1, \dots, v_k = t\) with \(k \ge 0\) such that each \((v_i, v_{i+1})\) is an arc, that is, a pair listed in \(E\) with both ends below \(n\).

noncomputable def pathDec : MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  decide (∃ s t n es, encodeP s t n es = x ∧ s < n ∧ t < n ∧
    Relation.ReflTransGen (arc n es) s t)

Uses 3 · Used by 2

Statement usesArcs of the PATH digraph · Encoding of a PATH instance · Decision problems

Used byThe marking algorithm decides PATH · PATH ∈ P

DefinitionInitial marks#✓fully proved

For \(n, s \in \mathbb{N}\), the initial marks are the list of \(n\) booleans whose entry at position \(i < n\) is true exactly when \(i = s\); all entries are false when \(s \ge n\).

def initMarks (n s : ℕ) : List Bool := (List.range n).map (· == s)

Used by 8

Used byThe initial marks mark exactly the source, if it is a vertex · The final marks have one entry per vertex · Repeated passes reach a fixpoint · The marking algorithm reads the mark of the target · Reach marks · The final marks are exactly the reachable vertices · Running time and output of the marking machine · Initial marks by setting one entry

DefinitionOne marking pass#✓fully proved

Given \(n \in \mathbb{N}\), an edge list \(E\) and a list \(m\) of booleans (the marks), the pass scans the pairs \((u, v)\) of \(E\) in order and, whenever \(u < n\), \(v < n\) and position \(u\) of the current marks is true, sets position \(v\) to true. A position beyond the end of the list counts as false and setting it changes nothing. Marks set earlier in the pass are seen by later pairs.

def markPass (n : ℕ) : List (ℕ × ℕ) → List Bool → List Bool
  | [], m => m
  | (u, v) :: es, m =>
      markPass n es (if u < n ∧ v < n ∧ m.getD u false = true then m.set v true else m)

Used by 16

Used byThe edge loop of a pass · Marks survive repeated passes · Repeated marking passes preserve the length · A marking pass preserves the length · The final marks have one entry per vertex · A pass marks the heads of arcs with marked tails · A pass either changes nothing or adds a mark · Marks persist through a pass · Repeated passes reach a fixpoint · A pass sets no mark when none is set · Soundness of a pass · The pass loop of the marking machine · The marking algorithm reads the mark of the target · Reach marks · The final marks are exactly the reachable vertices · Running time and output of the marking machine

DefinitionReach marks#✓fully proved

For \(n, s \in \mathbb{N}\) and an edge list \(E\), the reach marks are obtained from the initial marks of \(s\) among \(0, \dots, n - 1\) by applying the marking pass over \(E\) with bound \(n\) exactly \(n\) times.

def reachMarks (n s : ℕ) (es : List (ℕ × ℕ)) : List Bool := (markPass n es)^[n] (initMarks n s)

Uses 2 · Used by 7

Statement usesInitial marks · One marking pass

Used byThe final marks have one entry per vertex · Repeated passes reach a fixpoint · The marking algorithm for PATH · The marking algorithm reads the mark of the target · The marking algorithm decides PATH · The final marks are exactly the reachable vertices · Running time and output of the marking machine

DefinitionThe marking algorithm for PATH#✓fully proved

On a bit string \(x\), the check decodes \(x\) as a PATH instance. If decoding fails it returns false; if it yields \((s, t, n, E)\) it returns true exactly when \(s < n\), \(t < n\) and position \(t\) of the marks after \(n\) marking passes from \(s\) over \(E\) is true.

def pathCheck (x : List Bool) : Bool :=
  match decodeP x with
  | some (s, t, n, es) => decide (s < n) && decide (t < n) && (reachMarks n s es).getD t false
  | none => false

Uses 2 · Used by 5

Statement usesDecoding a PATH instance · Reach marks

Used byThe marking algorithm is polynomial-time · The marking algorithm reads the mark of the target · The marking algorithm decides PATH · PATH ∈ P · Running time and output of the marking machine

TheoremDecoding inverts the PATH instance encoding#✓fully proved

For natural numbers \(s, t, n\) and a list \(E\) of pairs of natural numbers, the PATH instance parser applied to the PATH instance encoding of \((s, t, n, E)\) succeeds and returns \((s, t, n, E)\).

@[simp] theorem decodeP_encodeP (s t n : ℕ) (es : List (ℕ × ℕ)) :
    decodeP (encodeP s t n es) = some (s, t, n, es)

Uses 6 · Used by 5

Statement usesDecoding a PATH instance · Encoding of a PATH instance

Proof usesDecoding a graph · Graph decoding inverts graph encoding · Bit-string encoding of a graph · Reading a unary length prefix

Used byThe verifier on an encoded instance and witness · What the HAMPATH verifier accepts · The PATH instance parser succeeds exactly on encodings · The PATH instance encoding is injective · The marking algorithm decides PATH

TheoremThe PATH instance parser succeeds exactly on encodings#✓fully proved

For a bit string \(x\), natural numbers \(s, t, n\) and a list \(E\) of pairs of natural numbers, the PATH instance parser applied to \(x\) succeeds with result \((s, t, n, E)\) if and only if \(x\) is the PATH instance encoding of \((s, t, n, E)\).

theorem decodeP_eq_some {x : List Bool} {s t n : ℕ} {es : List (ℕ × ℕ)} :
    decodeP x = some (s, t, n, es) ↔ encodeP s t n es = x

Uses 7 · Used by 2

Statement usesDecoding a PATH instance · Encoding of a PATH instance

Proof usesDecoding a graph · Bit-string encoding of a graph · Graph decoding succeeds only on encodings · Decoding inverts the PATH instance encoding · Reading a unary length prefix

Used byWhat the HAMPATH verifier accepts · The marking algorithm decides PATH

TheoremThe PATH instance encoding is injective#✓fully proved

Let \(s, t, n, s', t', n'\) be natural numbers and \(E, E'\) lists of pairs of natural numbers. If the PATH instance encodings of \((s, t, n, E)\) and \((s', t', n', E')\) are equal, then \(s = s'\), \(t = t'\), \(n = n'\) and \(E = E'\).

theorem encodeP_inj {s t n s' t' n' : ℕ} {es es' : List (ℕ × ℕ)}
    (h : encodeP s t n es = encodeP s' t' n' es') : s = s' ∧ t = t' ∧ n = n' ∧ es = es'

Uses 3 · Used by 2

Statement usesEncoding of a PATH instance

Proof usesDecoding a PATH instance · Decoding inverts the PATH instance encoding

Used byHAMPATH on an encoded instance · The marking algorithm decides PATH

TheoremSetting an entry of a boolean list to true#✓fully proved

Let \(m\) be a list of booleans and \(v, w\) natural numbers, and read a position at or beyond the end of a list as \(\mathrm{false}\). Set the entry of \(m\) at position \(w\) to \(\mathrm{true}\), leaving \(m\) unchanged if \(w\) is not less than the length of \(m\). Then position \(v\) of the result holds \(\mathrm{true}\) if and only if position \(v\) of \(m\) holds \(\mathrm{true}\), or \(v = w\) and \(w\) is less than the length of \(m\).

theorem getD_set_true {m : List Bool} {w v : ℕ} :
    (m.set w true).getD v false = true ↔ m.getD v false = true ∨ (v = w ∧ w < m.length)

Used by 3

Used byA pass marks the heads of arcs with marked tails · Marks persist through a pass · Soundness of a pass

TheoremThe initial marks mark exactly the source, if it is a vertex#✓fully proved

Let \(n, s, v\) be natural numbers, and read a position at or beyond the end of a list as \(\mathrm{false}\). Position \(v\) of the initial marks for \(n\) vertices and source \(s\) holds \(\mathrm{true}\) if and only if \(v < n\) and \(v = s\).

theorem initMarks_getD {n s v : ℕ} : (initMarks n s).getD v false = true ↔ v < n ∧ v = s

Uses 1 · Used by 1

Statement usesInitial marks

Used byThe final marks are exactly the reachable vertices

TheoremA marking pass preserves the length#✓fully proved

Let \(n\) be a natural number, \(E\) a list of pairs of natural numbers and \(m\) a list of booleans. A marking pass over \(E\) for \(n\) vertices, applied to \(m\), gives a list of the same length as \(m\).

theorem length_markPass (n : ℕ) :
    ∀ (es : List (ℕ × ℕ)) (m : List Bool), (markPass n es m).length = m.length

Uses 1 · Used by 3

Statement usesOne marking pass

Used byRepeated marking passes preserve the length · A pass either changes nothing or adds a mark · The pass loop of the marking machine

TheoremMarks persist through a pass#✓fully proved

Let \(n, v \in \mathbb{N}\), let \(E\) be a list of pairs of natural numbers and let \(m\) be a list of booleans. If \(v < |m|\) and the \(v\)-th entry of \(m\) (counting from \(0\)) is true, then the same holds for the result of the marking pass of \(E\) with bound \(n\) on \(m\).

theorem markPass_mono (n : ℕ) {v : ℕ} : ∀ (es : List (ℕ × ℕ)) {m : List Bool},
    m.getD v false = true → (markPass n es m).getD v false = true

Uses 2 · Used by 3

Statement usesOne marking pass

Proof usesSetting an entry of a boolean list to true

Used byMarks survive repeated passes · A pass marks the heads of arcs with marked tails · A pass either changes nothing or adds a mark

TheoremSoundness of a pass#✓fully proved

Let \(n \in \mathbb{N}\), let \(P\) be a property of natural numbers and let \(E\) be a list of pairs of natural numbers such that \(P(u)\) implies \(P(v)\) whenever \((u, v) \in E\), \(u < n\) and \(v < n\). If \(m\) is a list of booleans such that \(P(v)\) holds for every \(v < |m|\) whose entry in \(m\) is true, then \(P(v)\) holds for every \(v\) whose entry is true in the result of the marking pass of \(E\) with bound \(n\) on \(m\).

theorem markPass_sound {n : ℕ} {P : ℕ → Prop} : ∀ (es : List (ℕ × ℕ)),
    (∀ u v, (u, v) ∈ es → u < n → v < n → P u → P v) → ∀ {m : List Bool},
    (∀ v, m.getD v false = true → P v) → ∀ v, (markPass n es m).getD v false = true → P v

Uses 2 · Used by 1

Statement usesOne marking pass

Proof usesSetting an entry of a boolean list to true

Used byThe final marks are exactly the reachable vertices

TheoremA pass marks the heads of arcs with marked tails#✓fully proved

Let \(n \in \mathbb{N}\), let \(E\) be a list of pairs of natural numbers and let \(m\) be a list of booleans, where \(m\) marks \(w\) when \(w < |m|\) and the \(w\)-th entry of \(m\) (counting from \(0\)) is true. If \((u, v) \in E\) with \(u < n\) and \(v < n\), \(v < |m|\) and \(m\) marks \(u\), then the result of the marking pass of \(E\) with bound \(n\) on \(m\) marks \(v\).

theorem markPass_closed {n u v : ℕ} (hu : u < n) (hv : v < n) :
    ∀ {es : List (ℕ × ℕ)} {m : List Bool}, (u, v) ∈ es → v < m.length →
      m.getD u false = true → (markPass n es m).getD v false = true

Uses 3 · Used by 1

Statement usesOne marking pass

Proof usesSetting an entry of a boolean list to true · Marks persist through a pass

Used byThe final marks are exactly the reachable vertices

TheoremCounting true entries of pointwise dominated boolean lists#✓fully proved

Let \(l_1\) and \(l_2\) be lists of booleans of the same length such that every position holding \(\mathrm{true}\) in \(l_1\) also holds \(\mathrm{true}\) in \(l_2\). Then \(l_1\) has at most as many \(\mathrm{true}\) entries as \(l_2\), and strictly fewer if \(l_1 \ne l_2\).

theorem count_lt_of_getD_imp : ∀ {l₁ l₂ : List Bool}, l₁.length = l₂.length →
    (∀ i, l₁.getD i false = true → l₂.getD i false = true) →
    l₁.count true ≤ l₂.count true ∧ (l₁ ≠ l₂ → l₁.count true < l₂.count true)

Used by 1

Used byA pass either changes nothing or adds a mark

TheoremA pass either changes nothing or adds a mark#✓fully proved

For every \(n \in \mathbb{N}\), every list \(E\) of pairs of natural numbers and every list \(m\) of booleans, let \(m'\) be the result of the marking pass of \(E\) with bound \(n\) on \(m\). Then \(m' = m\), or \(m'\) has strictly more entries equal to true than \(m\).

theorem markPass_eq_or_count_lt (n : ℕ) (es : List (ℕ × ℕ)) (m : List Bool) :
    markPass n es m = m ∨ m.count true < (markPass n es m).count true

Uses 4 · Used by 1

Statement usesOne marking pass

Proof usesCounting true entries of pointwise dominated boolean lists · A marking pass preserves the length · Marks persist through a pass

Used byRepeated passes reach a fixpoint

TheoremRepeated marking passes preserve the length#✓fully proved

Let \(n\) be a natural number, \(E\) a list of pairs of natural numbers and \(m\) a list of booleans. For every natural number \(k\), applying \(k\) marking passes over \(E\) for \(n\) vertices to \(m\) gives a list of the same length as \(m\).

theorem length_iterate_markPass (n : ℕ) (es : List (ℕ × ℕ)) (m : List Bool) :
    ∀ k, ((markPass n es)^[k] m).length = m.length

Uses 2 · Used by 3

Statement usesOne marking pass

Proof usesA marking pass preserves the length

Used byThe final marks have one entry per vertex · Repeated passes reach a fixpoint · The marking algorithm reads the mark of the target

TheoremMarks survive repeated passes#✓fully proved

Let \(n\) and \(v\) be natural numbers, \(E\) a list of pairs of natural numbers and \(m\) a list of booleans whose position \(v\) holds \(\mathrm{true}\) (positions at or beyond the end read as \(\mathrm{false}\)). Then for every natural number \(k\), position \(v\) still holds \(\mathrm{true}\) after \(k\) marking passes over \(E\) for \(n\) vertices, starting from \(m\).

theorem iterate_markPass_mono (n : ℕ) (es : List (ℕ × ℕ)) {m : List Bool} {v : ℕ}
    (h : m.getD v false = true) : ∀ k, ((markPass n es)^[k] m).getD v false = true

Uses 2 · Used by 1

Statement usesOne marking pass

Proof usesMarks persist through a pass

Used byThe final marks are exactly the reachable vertices

TheoremThe final marks have one entry per vertex#✓fully proved

For natural numbers \(n, s\) and a list \(E\) of pairs of natural numbers, the marks after \(n\) marking passes over \(E\) for \(n\) vertices, starting from the initial marks for source \(s\), form a list of length \(n\).

theorem length_reachMarks (n s : ℕ) (es : List (ℕ × ℕ)) : (reachMarks n s es).length = n

Uses 4 · Used by 1

Statement usesReach marks

Proof usesInitial marks · Repeated marking passes preserve the length · One marking pass

Used byThe final marks are exactly the reachable vertices

TheoremRepeated passes reach a fixpoint#✓fully proved

Let \(n, s \in \mathbb{N}\) with \(s < n\) and let \(E\) be a list of pairs of natural numbers. Let \(r\) be the list obtained from the initial marks (only \(s\) marked among \(0, \dots, n - 1\)) by \(n\) marking passes of \(E\) with bound \(n\). Then one more marking pass of \(E\) with bound \(n\) leaves \(r\) unchanged.

Each pass that changes the marks adds at least one mark, the initial marks contain one mark, and there are at most \(n\) marks.

theorem markPass_reachMarks {n s : ℕ} (es : List (ℕ × ℕ)) (hs : s < n) :
    markPass n es (reachMarks n s es) = reachMarks n s es

Uses 5 · Used by 1

Statement usesOne marking pass · Reach marks

Proof usesInitial marks · Repeated marking passes preserve the length · A pass either changes nothing or adds a mark

Used byThe final marks are exactly the reachable vertices

TheoremThe final marks are exactly the reachable vertices#✓fully proved

Let \(n, s, t \in \mathbb{N}\) with \(s < n\) and \(t < n\), and let \(E\) be a list of pairs of natural numbers. Start from the marks on \(0, \dots, n - 1\) in which only \(s\) is marked and apply \(n\) marking passes of \(E\) with bound \(n\). Then \(t\) is marked if and only if \(t\) is reachable from \(s\) in zero or more steps along the arcs of \(E\) below \(n\), the pairs \((u, v) \in E\) with \(u < n\) and \(v < n\).

theorem reachMarks_getD_iff {n s t : ℕ} (es : List (ℕ × ℕ)) (hs : s < n) (ht : t < n) :
    (reachMarks n s es).getD t false = true ↔ Relation.ReflTransGen (arc n es) s t

Uses 10 · Used by 1

Statement usesArcs of the PATH digraph · Reach marks

Proof usesInitial marks · The initial marks mark exactly the source, if it is a vertex · Marks survive repeated passes · The final marks have one entry per vertex · One marking pass · A pass marks the heads of arcs with marked tails · Repeated passes reach a fixpoint · Soundness of a pass

Used byThe marking algorithm decides PATH

TheoremThe marking algorithm decides PATH#✓fully proved

For every bit string \(x\), the marking algorithm returns the same answer on \(x\) as the decision problem PATH.

theorem pathDec_eq_pathCheck (x : List Bool) : pathDec x = pathCheck x

Uses 10 · Used by 1

Statement usesThe marking algorithm for PATH · The PATH problem

Proof usesArcs of the PATH digraph · Decoding a PATH instance · Decoding inverts the PATH instance encoding · The PATH instance parser succeeds exactly on encodings · Encoding of a PATH instance · The PATH instance encoding is injective · Reach marks · The final marks are exactly the reachable vertices

Used byPATH ∈ P

InductiveStacks of the PATH marking machine#✓fully proved

The PATH marking machine, run on an instance with source \(s\), target \(t\) and \(n\) vertices, has eleven stacks: the input stack \(X\), the output stack \(O\), the stack \(E\) of the edge bits (reversed between passes), the junk stack \(J\), the counters \(S\), \(T\) and \(N\) for \(s\), \(t\) and \(n\) (\(N\) counts the passes left), the counters \(U\) and \(V\) for the endpoints \(u\) and \(v\) of an arc, the mark stack \(M\) (with the mark of vertex \(0\) on top) and the stack \(P\) of parked marks.

inductive K | X | O | E | J | S | T | N | U | V | M | P
  deriving DecidableEq

Used by 25

Used byThe edge loop of a pass · Agreement off a set of stacks · The frame of a read · The marking algorithm is polynomial-time · The pass loop of the marking machine · The marking machine as a host component · The marking machine for PATH · The unary read instruction · Reading a cut-off unary number · Reading a unary number · Reading the mark of a vertex · Frames are reflexive · Restoring the parked marks · Running time and output of the marking machine · Mark-setting step · Walking to a vertex and setting its mark · Effect of the mark-setting step · A walk step with an exhausted counter · Statements of the PATH marking machine · Frames compose · Stack alphabets of the PATH marking machine · Updating a framed stack preserves the frame · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine · Walk step of the PATH marking machine

DefinitionStack alphabets of the PATH marking machine#✓fully proved

The output stack \(O\) of the PATH marking machine holds Booleans, and every other stack holds symbols of the SAT verifier's symbol alphabet.

@[reducible] def Γ : K → Type
  | .O => Bool
  | _ => Sym

Uses 2 · Used by 24

Statement usesStacks of the PATH marking machine · Stack alphabet of the SAT verifier

Used byThe edge loop of a pass · Agreement off a set of stacks · The frame of a read · The marking algorithm is polynomial-time · The pass loop of the marking machine · The marking machine as a host component · The marking machine for PATH · The unary read instruction · Reading a cut-off unary number · Reading a unary number · Reading the mark of a vertex · Frames are reflexive · Restoring the parked marks · Running time and output of the marking machine · Mark-setting step · Walking to a vertex and setting its mark · Effect of the mark-setting step · A walk step with an exhausted counter · Statements of the PATH marking machine · Frames compose · Updating a framed stack preserves the frame · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine · Walk step of the PATH marking machine

InductiveLabels of the PATH marking machine#✓fully proved

For an instance with source \(s\), target \(t\), \(n\) vertices and arcs \((u, v)\), the labels of the PATH marking machine are \(\mathsf{rdS}\), \(\mathsf{rdT}\) and \(\mathsf{rdN}\) (read \(s\), \(t\) and \(n\)); \(\mathsf{val0}\), \(\mathsf{valU}\) and \(\mathsf{valV}\) (validate the edge list: at a pair, inside \(u\), inside \(v\)); \(\mathsf{goS}\) and \(\mathsf{backS}\) (walk to \(s\) and set its mark, then restore); \(\mathsf{pass}\) (the pass loop), \(\mathsf{ld}\) (reload the edges) and \(\mathsf{edge}\) (the edge loop); \(\mathsf{rdU}\) and \(\mathsf{rdV}\) (read \(u\) and \(v\)); \(\mathsf{go1}\) and, for each bit \(b\), \(\mathsf{back1}(b)\) (walk to \(u\), then restore holding its mark \(b\)); \(\mathsf{go2}\) and \(\mathsf{back2}\) (walk to \(v\) and set its mark, then restore); \(\mathsf{drV}\) (drain the counter stack \(V\)); \(\mathsf{goT}\) (walk to \(t\) and answer); \(\mathsf{bad}\) (answer false); and \(\mathsf{done}\) (halt).

inductive Lab | rdS | rdT | rdN | val0 | valU | valV | goS | backS | pass | ld | edge | rdU | rdV
  | go1 | back1 (b : Bool) | go2 | back2 | drV | goT | bad | done
  deriving DecidableEq

Used by 20

Used byThe edge loop of a pass · The marking algorithm is polynomial-time · The pass loop of the marking machine · The marking machine as a host component · The marking machine for PATH · The unary read instruction · Reading a cut-off unary number · Reading a unary number · Reading the mark of a vertex · Restoring the parked marks · Running time and output of the marking machine · Mark-setting step · Walking to a vertex and setting its mark · Start label of the PATH marking machine · Effect of the mark-setting step · A walk step with an exhausted counter · Statements of the PATH marking machine · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine · Walk step of the PATH marking machine

AbbreviationStatements of the PATH marking machine#✓fully proved

The statements of the multi-stack Turing machine (TM2) model whose stacks carry the stack alphabets \(\Gamma\) of the marking machine, whose labels are the labels of the marking machine, and whose internal state is a boolean.

abbrev Stmt := TM2.Stmt Γ Lab Bool

Uses 3 · Used by 14

Statement usesStacks of the PATH marking machine · Labels of the PATH marking machine · Stack alphabets of the PATH marking machine

Used byThe edge loop of a pass · The marking machine for PATH · The unary read instruction · Reading a cut-off unary number · Reading a unary number · Reading the mark of a vertex · Restoring the parked marks · Running time and output of the marking machine · Mark-setting step · Walking to a vertex and setting its mark · A walk step with an exhausted counter · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine · Walk step of the PATH marking machine

AbbreviationThe counter unit of the PATH marking machine#✓fully proved

The unit symbol of the counters of the PATH marking machine is the clause-end symbol \(\mathrm{cl}\) of the SAT verifier's symbol alphabet.

abbrev one : Sym := .cl

Uses 1 · Used by 5

Statement usesStack alphabet of the SAT verifier

Used byThe edge loop of a pass · The pass loop of the marking machine · The marking machine for PATH · Reading the mark of a vertex · Running time and output of the marking machine

DefinitionThe unary read instruction#✓fully proved

Given a stack \(d\), an encoding \(g\) of bits as symbols of \(d\), a list \(ps\) of stack–symbol pairs and labels \(\ell\) and \(\ell'\), the instruction of the marking machine that jumps to bad if \(X\) is empty, and otherwise pops the top of \(X\) as a bit \(b\) (a symbol that is not a bit counts as false) and pushes \(g(b)\) on \(d\); then, if \(b\) is true, it pushes \(a\) on \(q\) for each pair \((q, a)\) of \(ps\), in order, and jumps to \(\ell\), and if \(b\) is false it jumps to \(\ell'\). Run at its own label \(\ell\), it reads a unary number off \(X\).

def readS (d : K) (g : Bool → Γ d) (ps : List (Σ k, Γ k)) (self next : Lab) : Stmt :=
  .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .bad) <|
    .pop .X (fun _ o => bitOf Sym.bit? o) <| .push d g <| .branch id
      (pushAll ps (.goto fun _ => self)) (.goto fun _ => next)

Uses 8 · Used by 3

Statement usesStacks of the PATH marking machine · Labels of the PATH marking machine · Statements of the PATH marking machine · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack · Pushing symbols onto several stacks

Used byThe marking machine for PATH · Reading a cut-off unary number · Reading a unary number

DefinitionWalk step of the PATH marking machine#✓fully proved

Given a counter stack \(c\), a label \(\ell\) and a final statement \(f\), the walk step pops the top of \(c\). If \(c\) was nonempty, it goes to \(\ell\) after moving the top mark of the marks stack \(M\), if there is one, onto the parked stack \(P\): the mark is popped, read as a bit (a symbol that is not a bit reads as false), and pushed on \(P\) as that bit. If \(c\) was empty, it runs \(f\).

def walkS (c : K) (self : Lab) (fin : Stmt) : Stmt :=
  .pop c (fun _ o => o.isSome) <| .branch id
    (.peek .M (fun _ o => o.isNone) <| .branch id (.goto fun _ => self) <|
      .pop .M (fun _ o => bitOf Sym.bit? o) <| .push .P (fun b => .bit b) <|
        .goto fun _ => self)
    fin

Uses 7 · Used by 6

Statement usesStacks of the PATH marking machine · Labels of the PATH marking machine · Statements of the PATH marking machine · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byThe marking machine for PATH · Reading the mark of a vertex · Running time and output of the marking machine · Walking to a vertex and setting its mark · A walk step with an exhausted counter · Walking along the marks of the PATH marking machine

DefinitionMark-setting step#✓fully proved

For a label \(\ell\), the statement of the marking machine that pops the top cell of the mark stack \(M\) and, if there was one, pushes the set mark (the bit true) onto \(M\) in its place; in either case it then goes to \(\ell\).

def setS (next : Lab) : Stmt :=
  .pop .M (fun _ o => o.isSome) <| .branch id
    (.push .M (fun _ => .bit true) <| .goto fun _ => next) (.goto fun _ => next)

Uses 5 · Used by 3

Statement usesStacks of the PATH marking machine · Labels of the PATH marking machine · Statements of the PATH marking machine · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier

Used byThe marking machine for PATH · Walking to a vertex and setting its mark · Effect of the mark-setting step

DefinitionThe marking machine for PATH#✓fully proved

The multi-stack machine program whose input lies on the stack \(X\) and whose answer is pushed on the Boolean stack \(O\). To read a unary number off \(X\) onto a stack \(d\), it pops a bit off \(X\) and pushes it on \(d\), repeating while the bit is true and moving on after the first false bit; an empty \(X\) jumps to bad. To walk along a counter \(c\), it pops units off \(c\) one at a time, each time moving the top mark of \(M\) (if there is one) onto \(P\), until \(c\) is empty. To restore, it moves the bits on top of \(P\) back onto \(M\) one at a time.

At rdS, rdT and rdN it reads \(s\), \(t\) and \(n\) in turn off \(X\) onto \(J\), pushing a counter unit on \(S\), \(T\) or \(N\) respectively for each true bit, and at rdN also a cleared mark on \(M\); then it goes to val0. At val0 it goes to goS if \(X\) is empty, and otherwise reads two unary numbers off \(X\) onto \(E\) (at valU and valV) and returns to val0. At goS it walks along \(S\) and then sets the top mark of \(M\) (if any); at backS it restores and goes to pass. At pass it pops a unit off \(N\) and goes to ld, or to goT if \(N\) is empty. At ld it moves the bits on top of \(E\) onto \(X\), then goes to edge. At edge it goes to pass if \(X\) is empty, and otherwise reads \(u\) and \(v\) off \(X\) onto \(E\) (at rdU and rdV), pushing a counter unit on \(U\), respectively \(V\), for each true bit, and then goes to go1. At go1 it walks along \(U\) and reads the top mark \(b\) of \(M\) (false if there is none); at back1 b it restores and goes to go2 if \(b\) is true and to drV otherwise. At go2 it walks along \(V\) and sets the top mark of \(M\) (if any); at back2 it restores and goes to edge. At drV it empties \(V\) and goes to edge. At goT it walks along \(T\), pushes the top mark of \(M\) (false if there is none) on \(O\) and goes to done. At bad it pushes false on \(O\) and goes to done. At done it halts.

Cslib.Complexity.Path.Machine.prog · 25 lines

def prog : Lab → Stmt
  | .rdS => readS .J Sym.bit [⟨.S, one⟩] .rdS .rdT
  | .rdT => readS .J Sym.bit [⟨.T, one⟩] .rdT .rdN
  | .rdN => readS .J Sym.bit [⟨.N, one⟩, ⟨.M, .bit false⟩] .rdN .val0
  | .val0 => .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .goS)
      (.goto fun _ => .valU)
  | .valU => readS .E Sym.bit [] .valU .valV
  | .valV => readS .E Sym.bit [] .valV .val0
  | .goS => walkS .S .goS (setS .backS)
  | .backS => moveB .P .M Sym.bit? Sym.bit .backS .pass
  | .pass => decr .N .goT .ld
  | .ld => moveB .E .X Sym.bit? Sym.bit .ld .edge
  | .edge => .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .pass)
      (.goto fun _ => .rdU)
  | .rdU => readS .E Sym.bit [⟨.U, one⟩] .rdU .rdV
  | .rdV => readS .E Sym.bit [⟨.V, one⟩] .rdV .go1
  | .go1 => walkS .U .go1 (.peek .M (fun _ o => bitOf Sym.bit? o) <| .goto fun b => .back1 b)
  | .back1 b => moveB .P .M Sym.bit? Sym.bit (.back1 b) (if b then .go2 else .drV)
  | .go2 => walkS .V .go2 (setS .back2)
  | .back2 => moveB .P .M Sym.bit? Sym.bit .back2 .edge
  | .drV => xfer .V [] .drV .edge
  | .goT => walkS .T .goT <| .peek .M (fun _ o => bitOf Sym.bit? o) <| .push .O id <|
      .goto fun _ => .done
  | .bad => .push .O (fun _ => false) <| .goto fun _ => .done
  | .done => .halt

Uses 15 · Used by 12

Statement usesStacks of the PATH marking machine · Labels of the PATH marking machine · Statements of the PATH marking machine · The counter unit of the PATH marking machine · The unary read instruction · Mark-setting step · Walk step of the PATH marking machine · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Flag bit of a machine state · Bit on top of a stack · Decrement · Bit-moving loop · Counter transfer loop

Used byThe edge loop of a pass · The marking algorithm is polynomial-time · The pass loop of the marking machine · The marking machine as a host component · Reading a cut-off unary number · Reading a unary number · Reading the mark of a vertex · Restoring the parked marks · Running time and output of the marking machine · Walking to a vertex and setting its mark · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine

DefinitionStart label of the PATH marking machine#✓fully proved

The marking machine for PATH starts at the label that reads the source vertex \(s\), in unary, off the input.

def start : Lab := .rdS

Uses 1 · Used by 2

Statement usesLabels of the PATH marking machine

Used byThe marking algorithm is polynomial-time · Running time and output of the marking machine

DefinitionSetting the first mark#✓fully proved

For a list of booleans, the list obtained by setting its first entry: the empty list is left unchanged, and a list \(b :: r\) with first entry \(b\) and remaining entries \(r\) becomes \(\mathrm{true} :: r\).

def setHead : List Bool → List Bool
  | [] => []
  | _ :: r => true :: r

Used by 3

Used byWalking to a vertex and setting its mark · Effect of the mark-setting step · Setting an entry by splitting the list

TheoremSetting an entry by splitting the list#✓fully proved

For every list \(m\) of booleans and every natural number \(j\), the first \(j\) entries of \(m\) followed by the remaining entries with their first entry set to true (the empty list stays empty) equal \(m\) with entry \(j\) set to true (which is \(m\) itself when \(j \ge |m|\)).

theorem take_append_setHead : ∀ (m : List Bool) (j : ℕ),
    m.take j ++ setHead (m.drop j) = m.set j true

Uses 1 · Used by 1

Statement usesSetting the first mark

Used byWalking to a vertex and setting its mark

TheoremReading the mark of vertex \(j\)#✓fully proved

Let \(m\) be a list of Boolean marks and \(j\) a natural number. Drop the first \(j\) marks of \(m\) and write the rest as bit symbols; reading the top symbol as a bit, with false when there is no top symbol, gives the entry of \(m\) at position \(j\) (counting from \(0\)), or false when \(j\) is at least the length of \(m\).

theorem bitOf_drop (m : List Bool) (j : ℕ) :
    bitOf Sym.bit? ((m.drop j).map Sym.bit).head? = m.getD j false

Uses 3 · Used by 2

Statement usesStack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byReading the mark of a vertex · Running time and output of the marking machine

TheoremOut-of-range arcs need no guard#✓fully proved

Let \(m\) be a list of \(n\) Boolean marks and let \(u\), \(v\) be natural numbers; write \(m_u\) for the entry of \(m\) at position \(u\) (counting from \(0\)), taken to be false when \(u \ge n\). If \(u < n\), \(v < n\) and \(m_u\) is true, set position \(v\) of \(m\) to true, and otherwise keep \(m\); the result is the same as setting position \(v\) of \(m\) to true when \(m_u\) is true and keeping \(m\) otherwise.

Setting a position \(v \ge n\) leaves the list unchanged, so the machine, which reads the mark of \(u\) and then sets the mark of \(v\), ignores an arc with an end past the last vertex, as the marking algorithm does.

theorem arc_eq {n u v : ℕ} {m : List Bool} (h : m.length = n) :
    (if u < n ∧ v < n ∧ m.getD u false = true then m.set v true else m) =
      if m.getD u false = true then m.set v true else m

Used by 1

Used byThe edge loop of a pass

TheoremInitial marks by setting one entry#✓fully proved

For all natural numbers \(n\) and \(s\), setting entry \(s\) of the list of \(n\) copies of false to true (which changes nothing when \(s \ge n\)) gives the initial marks of \(n\) vertices from \(s\): the list of length \(n\) whose entry \(i\) is true exactly when \(i = s\).

theorem set_replicate (n s : ℕ) : (List.replicate n false).set s true = initMarks n s

Uses 1 · Used by 2

Statement usesInitial marks

Used byThe marking algorithm reads the mark of the target · Running time and output of the marking machine

TheoremA cleared mark or nothing reads as cleared#✓fully proved

For every decidable proposition \(p\), the optional mark that is a cleared mark (false) when \(p\) holds and absent otherwise, read with default false, is false.

theorem getD_ite (p : Prop) [Decidable p] :
    (if p then some false else none).getD false = false

Used by 2

Used byA pass sets no mark when none is set · The marking algorithm reads the mark of the target

TheoremA pass sets no mark when none is set#✓fully proved

For all natural numbers \(n\) and \(k\) and every list \(es\) of arcs of natural numbers, one pass of the marking algorithm with \(n\) vertices over \(es\) (Mark Pass) maps the list of \(k\) cleared marks to itself.

theorem markPass_replicate (n k : ℕ) : ∀ es : List (ℕ × ℕ),
    markPass n es (List.replicate k false) = List.replicate k false

Uses 2 · Used by 1

Statement usesOne marking pass

Proof usesA cleared mark or nothing reads as cleared

Used byThe marking algorithm reads the mark of the target

TheoremThe marking algorithm reads the mark of the target#✓fully proved

If a bit string \(x\) parses as a PATH instance with source \(s\), target \(t\), \(n\) vertices and edge list \(es\), then the marking algorithm on \(x\) returns the mark of \(t\) in the reach marks of \(s\) (the marks after \(n\) marking passes over \(es\), starting from the marks on \(0, \dots, n - 1\) with only \(s\) marked, and none if \(s \ge n\)), where a vertex \(t \ge n\) counts as unmarked.

So the checks \(s < n\) and \(t < n\) of the marking algorithm are implied: a vertex \(t \ge n\) has no mark, and for \(s \ge n\) every mark stays cleared.

theorem pathCheck_eq {x : List Bool} {s t n : ℕ} {es : List (ℕ × ℕ)}
    (h : decodeP x = some (s, t, n, es)) : pathCheck x = (reachMarks n s es).getD t false

Uses 9 · Used by 1

Statement usesDecoding a PATH instance · The marking algorithm for PATH · Reach marks

Proof usesA cleared mark or nothing reads as cleared · A pass sets no mark when none is set · Initial marks by setting one entry · Initial marks · Repeated marking passes preserve the length · One marking pass

Used byRunning time and output of the marking machine

DefinitionAgreement off a set of stacks#✓fully proved

For a list \(A\) of stacks of the marking machine and two contents \(S\), \(S'\) of its stacks, \(S'\) agrees with \(S\) off \(A\) when every stack not in \(A\) holds the same list in \(S'\) as in \(S\).

def Fr (A : List K) (S S' : ∀ k, List (Γ k)) : Prop := ∀ q, q ∉ A → S' q = S q

Uses 2 · Used by 12

Statement usesStacks of the PATH marking machine · Stack alphabets of the PATH marking machine

Used byThe edge loop of a pass · The frame of a read · The pass loop of the marking machine · Reading the mark of a vertex · Frames are reflexive · Restoring the parked marks · Running time and output of the marking machine · Walking to a vertex and setting its mark · Frames compose · Updating a framed stack preserves the frame · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine

TheoremFrames are reflexive#✓fully proved

For every list \(A\) of stacks of the marking machine and every assignment \(S\) of contents to its stacks, \(S\) agrees with itself off \(A\).

theorem Fr.refl (A : List K) (S : ∀ k, List (Γ k)) : Fr A S S

Uses 3 · Used by 4

Statement usesAgreement off a set of stacks · Stacks of the PATH marking machine · Stack alphabets of the PATH marking machine

Used byThe edge loop of a pass · The pass loop of the marking machine · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine

TheoremFrames compose#✓fully proved

Let \(A\), \(B\), \(C\) be lists of stacks such that every stack in \(A\) or in \(B\) is in \(C\). If stacks \(S_2\) agree with \(S_1\) on every stack outside \(A\), and \(S_3\) agree with \(S_2\) on every stack outside \(B\), then \(S_3\) agree with \(S_1\) on every stack outside \(C\).

theorem Fr.trans {A B C : List K} {S₁ S₂ S₃ : ∀ k, List (Γ k)} (h₁ : Fr A S₁ S₂)
    (h₂ : Fr B S₂ S₃) (hA : ∀ q ∈ A, q ∈ C) (hB : ∀ q ∈ B, q ∈ C) : Fr C S₁ S₃

Uses 3 · Used by 6

Statement usesAgreement off a set of stacks · Stacks of the PATH marking machine · Stack alphabets of the PATH marking machine

Used byThe edge loop of a pass · The pass loop of the marking machine · Reading the mark of a vertex · Walking to a vertex and setting its mark · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine

TheoremUpdating a framed stack preserves the frame#✓fully proved

Let \(A\) be a list of stacks of the PATH marking machine, and let \(S\) and \(S'\) be stack contents such that \(S'\) agrees with \(S\) on every stack outside \(A\). Then for every stack \(k \in A\) and every list \(l\) over the alphabet of \(k\), the contents obtained from \(S'\) by replacing stack \(k\) with \(l\) still agree with \(S\) on every stack outside \(A\).

theorem Fr.upd {A : List K} {S S' : ∀ k, List (Γ k)} (h : Fr A S S') {k : K} (hk : k ∈ A)
    (l : List (Γ k)) : Fr A S (update S' k l)

Uses 3 · Used by 3

Statement usesAgreement off a set of stacks · Stacks of the PATH marking machine · Stack alphabets of the PATH marking machine

Used byThe edge loop of a pass · Walking to a vertex and setting its mark · Walking along the marks of the PATH marking machine

TheoremThe frame of a read#✓fully proved

Let \(d\) be a stack of the marking machine, \(ps\) a list of pairs of a stack and a symbol, \(i\) a natural number, and \(S\), \(S'\) two contents of the stacks. Suppose every stack \(q\) other than the input \(X\) and \(d\) holds in \(S'\) the list it holds in \(S\) with \(i\) further copies of the symbol of the first entry for \(q\) in \(ps\) pushed on top (and unchanged if \(ps\) has no entry for \(q\)). Then \(S'\) agrees with \(S\) on every stack other than \(X\), \(d\) and the stacks that have an entry in \(ps\).

theorem fr_addU {d : K} {ps : List (Σ k, Γ k)} {i : ℕ} {S S' : ∀ k, List (Γ k)}
    (h : ∀ q, q ≠ .X → q ≠ d → S' q = addU ps i S q) : Fr (.X :: d :: ps.keys) S S'

Uses 5 · Used by 3

Statement usesAgreement off a set of stacks · Stacks of the PATH marking machine · Stack alphabets of the PATH marking machine · Adding units to target stacks

Proof usesUnary counter

Used byThe edge loop of a pass · Running time and output of the marking machine · Validation phase of the PATH marking machine

TheoremReading a unary number#✓fully proved

Let \(d\) be a stack other than \(X\), let \(g\) encode bits as symbols of \(d\), and let \(ps\) be a list of stack–symbol pairs whose stacks are distinct and differ from \(X\) and \(d\). Suppose the instruction of the marking machine at a label \(\ell\) is the unary read off \(X\) onto \(d\) through \(g\) that pushes \(ps\) for each true bit, repeats at \(\ell\) and continues at \(\ell'\). If \(X\) holds, as bit symbols, \(k\) true bits, then a false bit, then a bit list \(r\), then in exactly \(k + 1\) steps the machine goes from \(\ell\), with any flag, to \(\ell'\); afterwards \(X\) holds \(r\), \(d\) has received \(k\) copies of \(g(\mathrm{true})\) and then \(g(\mathrm{false})\) on top, each stack \(q\) with a pair \((q, a)\) in \(ps\) has received \(k\) copies of \(a\) on top, and every other stack is unchanged.

theorem readS_some {d : K} {g : Bool → Γ d} {ps : List (Σ k, Γ k)} {self next : Lab}
    (hp : prog self = readS d g ps self next) (hdX : d ≠ .X) (hps : ps.NodupKeys)
    (hX : K.X ∉ ps.keys) (hd : d ∉ ps.keys) :
    ∀ (k : ℕ) (r : List Bool) (v : Bool) (St : ∀ k, List (Γ k)),
      St .X = (List.replicate k true ++ false :: r).map Sym.bit →
      ∃ v' S', Run prog (k + 1) ⟨some self, v, St⟩ ⟨some next, v', S'⟩ ∧
        S' .X = r.map Sym.bit ∧ S' d = g false :: (cnt (g true) k ++ St d) ∧
        ∀ q, q ≠ .X → q ≠ d → S' q = addU ps k St q

Uses 13 · Used by 3

Statement usesStacks of the PATH marking machine · Labels of the PATH marking machine · Statements of the PATH marking machine · The marking machine for PATH · The unary read instruction · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Adding units to target stacks · Unary counter

Proof usesReading a symbol as a name bit · A single step executes the statement at the current label · Pushing symbols onto several stacks

Used byThe edge loop of a pass · Running time and output of the marking machine · Validation phase of the PATH marking machine

TheoremReading a cut-off unary number#✓fully proved

Let \(d\) be a stack other than \(X\) and \(O\), let \(g\) encode bits as symbols of \(d\), and let \(ps\) be a list of stack–symbol pairs whose stacks are distinct and differ from \(X\) and \(O\). Suppose the instruction of the marking machine at a label \(\ell\) is the unary read off \(X\) onto \(d\) through \(g\) that pushes \(ps\) for each true bit, repeats at \(\ell\) and continues at \(\ell'\). If a bit list \(l\) has no unary length prefix (every bit of \(l\) is true) and \(X\) holds \(l\) as bit symbols, then from \(\ell\), with any flag, the machine reaches the label bad within \(|l| + 1\) steps, leaving the output stack \(O\) unchanged.

theorem readS_none {d : K} {g : Bool → Γ d} {ps : List (Σ k, Γ k)} {self next : Lab}
    (hp : prog self = readS d g ps self next) (hdX : d ≠ .X) (hps : ps.NodupKeys)
    (hX : K.X ∉ ps.keys) (hdO : d ≠ .O) (hO : K.O ∉ ps.keys) :
    ∀ (l : List Bool) (v : Bool) (St : ∀ k, List (Γ k)), readUnaryLength l = none →
      St .X = l.map Sym.bit →
      ∃ v' S', RunLe prog (l.length + 1) ⟨some self, v, St⟩ ⟨some .bad, v', S'⟩ ∧
        S' .O = St .O

Uses 16 · Used by 2

Statement usesStacks of the PATH marking machine · Labels of the PATH marking machine · Statements of the PATH marking machine · The marking machine for PATH · The unary read instruction · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier · Reading a unary length prefix · Runs within a step budget

Proof usesReading a symbol as a name bit · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Bit on top of a stack · Unary counter · Pushing symbols onto several stacks

Used byRunning time and output of the marking machine · Validation phase of the PATH marking machine

TheoremRestoring the parked marks#✓fully proved

Suppose the instruction of the marking machine at a label \(\ell\) moves the bits on top of \(P\) onto \(M\) one at a time, repeating at \(\ell\) and continuing at \(\ell'\) once \(P\) is empty or its top is not a bit. If \(P\) holds the reverse of a bit list \(p\) and \(M\) holds a bit list \(q\), both as bit symbols, then in exactly \(|p| + 1\) steps the machine goes from \(\ell\), with any flag, to \(\ell'\), leaving \(P\) empty, \(M\) holding \(p\) followed by \(q\), and every other stack unchanged.

theorem restore_run {self next : Lab} (hp : prog self = moveB .P .M Sym.bit? Sym.bit self next)
    (pre post : List Bool) (v : Bool) (St : ∀ k, List (Γ k))
    (hP : St .P = pre.reverse.map Sym.bit) (hM : St .M = post.map Sym.bit) :
    ∃ v' S', Run prog (pre.length + 1) ⟨some self, v, St⟩ ⟨some next, v', S'⟩ ∧ S' .P = [] ∧
      S' .M = (pre ++ post).map Sym.bit ∧ Fr [.P, .M] St S'

Uses 12 · Used by 2

Statement usesAgreement off a set of stacks · Stacks of the PATH marking machine · Labels of the PATH marking machine · Statements of the PATH marking machine · The marking machine for PATH · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Flag bit of a machine state · Exact-length runs of a TM2 machine · Bit-moving loop

Proof usesRunning the bit-moving loop

Used byReading the mark of a vertex · Walking to a vertex and setting its mark

TheoremA walk step with an exhausted counter#✓fully proved

Let \(c\) be a stack, \(\mathit{self}\) a label, \(\mathit{fin}\) a statement and \(S\) stacks in which \(c\) is empty. For every internal state \(v\), executing from \(v\) and \(S\) the walk step counted by \(c\) that loops at \(\mathit{self}\) and finishes with \(\mathit{fin}\) gives the same result as executing \(\mathit{fin}\) from internal state false and the same stacks \(S\).

theorem stepAux_walkS_nil {c : K} {self : Lab} {fin : Stmt} {S : ∀ k, List (Γ k)}
    (hc : S c = []) (v : Bool) : TM2.stepAux (walkS c self fin) v S = TM2.stepAux fin false S

Uses 8 · Used by 3

Statement usesStacks of the PATH marking machine · Labels of the PATH marking machine · Statements of the PATH marking machine · Walk step of the PATH marking machine · Stack alphabets of the PATH marking machine

Proof usesStack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byReading the mark of a vertex · Running time and output of the marking machine · Walking to a vertex and setting its mark

TheoremWalking along the marks of the PATH marking machine#✓fully proved

Let \(c\) be a stack other than the marks stack \(M\) and the parked stack \(P\), let \(u\) be a symbol of the alphabet of \(c\), and let \(\ell\) be a label at which the program is the walk step counted by \(c\) that returns to \(\ell\) (with some final statement). Let \(j\) be a natural number, \(p\) and \(q\) lists of bits, \(v\) a Boolean, and \(S\) stack contents in which \(c\) holds exactly \(j\) copies of \(u\), \(M\) holds \(q\) as bit symbols, and \(P\) holds the reverse of \(p\) as bit symbols. Then there are a Boolean \(v'\) and stack contents \(S'\) such that the machine goes in exactly \(j\) steps from label \(\ell\) with state \(v\) and stacks \(S\) to label \(\ell\) with state \(v'\) and stacks \(S'\), where \(c\) is empty in \(S'\), \(M\) holds \(q\) with its first \(j\) entries dropped, \(P\) holds the reverse of the concatenation of \(p\) with the first \(j\) entries of \(q\), all as bit symbols, and \(S'\) agrees with \(S\) on every stack other than \(c\), \(M\) and \(P\).

theorem walk_run {c : K} {self : Lab} {fin : Stmt} (hp : prog self = walkS c self fin)
    (hcM : c ≠ .M) (hcP : c ≠ .P) (u : Γ c) : ∀ (j : ℕ) (pre post : List Bool) (v : Bool)
    (St : ∀ k, List (Γ k)), St c = cnt u j → St .M = post.map Sym.bit →
    St .P = pre.reverse.map Sym.bit →
    ∃ v' S', Run prog j ⟨some self, v, St⟩ ⟨some self, v', S'⟩ ∧ S' c = [] ∧
      S' .M = (post.drop j).map Sym.bit ∧ S' .P = (pre ++ post.take j).reverse.map Sym.bit ∧
      Fr [c, .M, .P] St S'

Uses 16 · Used by 3

Statement usesAgreement off a set of stacks · Stacks of the PATH marking machine · Labels of the PATH marking machine · Statements of the PATH marking machine · The marking machine for PATH · Walk step of the PATH marking machine · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesFrames are reflexive · Frames compose · Updating a framed stack preserves the frame · Reading a symbol as a name bit · A single step executes the statement at the current label · Bit on top of a stack

Used byReading the mark of a vertex · Running time and output of the marking machine · Walking to a vertex and setting its mark

TheoremEffect of the mark-setting step#✓fully proved

Let \(\ell\) be a label, \(v\) an internal state and \(S\) stacks whose mark stack \(M\) holds the bits of a list \(l\) of booleans. Executing the mark-setting step to \(\ell\) from internal state \(v\) and stacks \(S\) ends at label \(\ell\) with some internal state and the stacks \(S\) with \(M\) replaced by the bits of \(l\) with its first entry set to true (the empty list stays empty); every other stack is unchanged.

theorem stepAux_setS (next : Lab) (l : List Bool) (v : Bool) (S : ∀ k, List (Γ k))
    (hM : S .M = l.map Sym.bit) : ∃ v', TM2.stepAux (setS next) v S =
      ⟨some next, v', update S .M ((setHead l).map Sym.bit)⟩

Uses 6 · Used by 1

Statement usesStacks of the PATH marking machine · Labels of the PATH marking machine · Setting the first mark · Mark-setting step · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier

Used byWalking to a vertex and setting its mark

TheoremWalking to a vertex and setting its mark#✓fully proved

Let \(c\) be a stack other than the mark stack \(M\) and the parking stack \(P\), and let \(\mathit{self}\), \(\mathit{back}\), \(\mathit{next}\) be labels such that the marking machine at \(\mathit{self}\) is the walk step counted by \(c\) that loops at \(\mathit{self}\) and finishes with the mark-setting step to \(\mathit{back}\), and at \(\mathit{back}\) it moves the bit block of \(P\) onto \(M\), looping at \(\mathit{back}\) and then going to \(\mathit{next}\). Let \(S\) be stacks in which \(c\) holds the counter value \(j\) (for some unit symbol), \(M\) holds the bits of a list \(m\) of booleans, and \(P\) is empty. Then from label \(\mathit{self}\) with stacks \(S\) and any internal state, the machine reaches label \(\mathit{next}\) in at most \(2j + 2\) steps, with some internal state and stacks \(S'\) such that \(c\) and \(P\) are empty, \(M\) holds the bits of \(m\) with entry \(j\) set to true (unchanged when \(j \ge |m|\)), and \(S'\) agrees with \(S\) on every stack other than \(c\), \(M\) and \(P\).

theorem setW_run {c : K} {self back next : Lab} (hp : prog self = walkS c self (setS back))
    (hb : prog back = moveB .P .M Sym.bit? Sym.bit back next) (hcM : c ≠ .M) (hcP : c ≠ .P)
    (u : Γ c) (j : ℕ) (m : List Bool) (v : Bool) (St : ∀ k, List (Γ k)) (hc : St c = cnt u j)
    (hM : St .M = m.map Sym.bit) (hP : St .P = []) :
    ∃ v' S', RunLe prog (2 * j + 2) ⟨some self, v, St⟩ ⟨some next, v', S'⟩ ∧ S' c = [] ∧
      S' .M = (m.set j true).map Sym.bit ∧ S' .P = [] ∧ Fr [c, .M, .P] St S'

Uses 24 · Used by 2

Statement usesAgreement off a set of stacks · Stacks of the PATH marking machine · Labels of the PATH marking machine · Statements of the PATH marking machine · The marking machine for PATH · Mark-setting step · Walk step of the PATH marking machine · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Flag bit of a machine state · Runs within a step budget · Unary counter · Bit-moving loop

Proof usesFrames compose · Updating a framed stack preserves the frame · Restoring the parked marks · Setting the first mark · Effect of the mark-setting step · A walk step with an exhausted counter · Setting an entry by splitting the list · Walking along the marks of the PATH marking machine · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byThe edge loop of a pass · Running time and output of the marking machine

TheoremReading the mark of a vertex#✓fully proved

Let \(u \in \mathbb{N}\) and let \(m\) be a list of marks. Start the marking machine at the label go1, with any flag, from stacks on which \(U\) holds \(u\) counter units, \(M\) holds \(m\) as bit symbols and \(P\) is empty. Then within \(2u + 2\) steps it reaches go2 if the mark of vertex \(u\) in \(m\) is set and drV otherwise (a vertex past the end of \(m\) counts as unmarked), with \(U\) and \(P\) empty, \(M\) holding \(m\) again, and every other stack unchanged.

theorem readW_run (u : ℕ) (m : List Bool) (v : Bool) (St : ∀ k, List (Γ k))
    (hU : St .U = cnt one u) (hM : St .M = m.map Sym.bit) (hP : St .P = []) :
    ∃ v' S', RunLe prog (2 * u + 2) ⟨some .go1, v, St⟩
      ⟨some (if m.getD u false then .go2 else .drV), v', S'⟩ ∧ S' .U = [] ∧
      S' .M = m.map Sym.bit ∧ S' .P = [] ∧ Fr [.U, .M, .P] St S'

Uses 20 · Used by 1

Statement usesAgreement off a set of stacks · Stacks of the PATH marking machine · Labels of the PATH marking machine · The counter unit of the PATH marking machine · The marking machine for PATH · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier · Runs within a step budget · Unary counter

Proof usesFrames compose · Statements of the PATH marking machine · Reading the mark of vertex \(j\) · Restoring the parked marks · A walk step with an exhausted counter · Walk step of the PATH marking machine · Walking along the marks of the PATH marking machine · Reading a symbol as a name bit · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack

Used byThe edge loop of a pass

TheoremValidation phase of the PATH marking machine#✓fully proved

Let \(w\) be a list of bits, \(v\) a Boolean and \(S\) stack contents whose input stack \(X\) holds \(w\) as bit symbols. Then there are a Boolean \(v'\) and stack contents \(S'\) such that, in at most \(2|w| + 1\) steps, the machine goes from the validation label (at a pair) with state \(v\) and stacks \(S\) to state \(v'\) and stacks \(S'\) at the label that walks to the source vertex if \(w\) decodes as an edge list, and at the label that answers false otherwise. The output stack \(O\) of \(S'\) equals that of \(S\). Moreover, if \(w\) decodes as an edge list, then \(X\) is empty in \(S'\), the edge stack \(E\) of \(S'\) is the reverse of \(w\) as bit symbols followed by the old contents of \(E\), and \(S'\) agrees with \(S\) on every stack other than \(X\) and \(E\).

theorem val_run : ∀ (w : List Bool) (v : Bool) (St : ∀ k, List (Γ k)),
    St .X = w.map Sym.bit →
    ∃ v' S', RunLe prog (2 * w.length + 1) ⟨some .val0, v, St⟩
      ⟨some (if (decodeEs w).isSome then .goS else .bad), v', S'⟩ ∧ S' .O = St .O ∧
      ((decodeEs w).isSome → S' .X = [] ∧ S' .E = w.reverse.map Sym.bit ++ St .E ∧
        Fr [.X, .E] St S')

Uses 23 · Used by 1

Statement usesEdge-list decoder · Agreement off a set of stacks · Stacks of the PATH marking machine · Labels of the PATH marking machine · The marking machine for PATH · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesDecoding the empty input · The edge-list decoder fails on a cut-off first number · Decoding fails on a dangling half-pair · Decoding one pair, then the rest · Frames are reflexive · Frames compose · Statements of the PATH marking machine · The frame of a read · Reading a cut-off unary number · Reading a unary number · Reading a unary length prefix · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Unary counter

Used byRunning time and output of the marking machine

TheoremThe edge loop of a pass#✓fully proved

Let \(n\) be a natural number, \(es\) a list of arcs \((u, w)\) of natural numbers and \(m\) a list of \(n\) Boolean marks. Encode an arc \((u, w)\) by \(u\) ones, a zero, \(w\) ones and a zero, and \(es\) by the concatenation of the codes of its arcs; let \(\ell\) be the length of this code. Suppose the marking machine is at the edge-loop label, in any internal state, with stacks \(S\) such that the input stack \(X\) holds the code of \(es\) and the mark stack \(M\) holds \(m\) (vertex \(0\) on top), as bit symbols, and the parked-mark stack \(P\) and the arc counters \(U\) and \(V\) are empty. Then within \(4\ell + 1\) steps it reaches the pass-loop label with stacks \(S'\) in which \(X\) is empty, the edge stack \(E\) holds the code of \(es\) in reverse order on top of its contents in \(S\), \(M\) holds the marks that one pass of the marking algorithm with \(n\) vertices over \(es\) (Mark Pass) produces from \(m\), and \(P\), \(U\), \(V\) are empty; every stack other than \(X\), \(E\), \(M\), \(U\), \(V\) and \(P\) holds the same list in \(S'\) as in \(S\).

theorem edges_run (n : ℕ) : ∀ (es : List (ℕ × ℕ)) (m : List Bool) (v : Bool)
    (St : ∀ k, List (Γ k)), m.length = n → St .X = (edgeBits es).map Sym.bit →
    St .M = m.map Sym.bit → St .P = [] → St .U = [] → St .V = [] →
    ∃ v' S', RunLe prog (4 * (edgeBits es).length + 1) ⟨some .edge, v, St⟩
      ⟨some .pass, v', S'⟩ ∧ S' .X = [] ∧ S' .E = (edgeBits es).reverse.map Sym.bit ++ St .E ∧
      S' .M = (markPass n es m).map Sym.bit ∧ S' .P = [] ∧ S' .U = [] ∧ S' .V = [] ∧
      Fr [.X, .E, .M, .U, .V, .P] St S'

Uses 25 · Used by 1

Statement usesBit encoding of an edge list · Agreement off a set of stacks · Stacks of the PATH marking machine · Labels of the PATH marking machine · The marking machine for PATH · Stack alphabets of the PATH marking machine · One marking pass · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesFrames are reflexive · Frames compose · Updating a framed stack preserves the frame · Statements of the PATH marking machine · Out-of-range arcs need no guard · The frame of a read · The counter unit of the PATH marking machine · Reading a unary number · Reading the mark of a vertex · Walking to a vertex and setting its mark · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Unary counter · Running a counter transfer

Used byThe pass loop of the marking machine

TheoremThe pass loop of the marking machine#✓fully proved

Let \(n, k \in \mathbb{N}\), let \(es\) be a list of pairs of natural numbers with edge bits \(b\), and let \(m\) be a list of \(n\) marks. Start the marking machine at the label pass, with any flag, from stacks on which \(N\) holds \(k\) counter units, \(X\), \(P\), \(U\) and \(V\) are empty, \(E\) holds the reverse of \(b\) and \(M\) holds \(m\), both as bit symbols. Then within \(k(5|b| + 3) + 1\) steps the machine reaches the label goT, with \(M\) holding \(p^k(m)\) as bit symbols, where \(p\) is one marking pass over \(es\) on \(n\) vertices, with \(P\) empty, and with every stack other than \(N\), \(X\), \(E\), \(M\), \(U\), \(V\) and \(P\) unchanged.

theorem passes_run (n : ℕ) (es : List (ℕ × ℕ)) : ∀ (k : ℕ) (m : List Bool) (v : Bool)
    (St : ∀ k, List (Γ k)), m.length = n → St .N = cnt one k → St .X = [] →
    St .E = (edgeBits es).reverse.map Sym.bit → St .M = m.map Sym.bit → St .P = [] →
    St .U = [] → St .V = [] →
    ∃ v' S', RunLe prog (k * (5 * (edgeBits es).length + 3) + 1) ⟨some .pass, v, St⟩
      ⟨some .goT, v', S'⟩ ∧ S' .M = ((markPass n es)^[k] m).map Sym.bit ∧ S' .P = [] ∧
      Fr [.N, .X, .E, .M, .U, .V, .P] St S'

Uses 21 · Used by 1

Statement usesBit encoding of an edge list · Agreement off a set of stacks · Stacks of the PATH marking machine · Labels of the PATH marking machine · The counter unit of the PATH marking machine · The marking machine for PATH · Stack alphabets of the PATH marking machine · One marking pass · Stack alphabet of the SAT verifier · Runs within a step budget · Unary counter

Proof usesFrames are reflexive · Frames compose · The edge loop of a pass · A marking pass preserves the length · Reading a symbol as a name bit · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Decrement · Running the bit-moving loop

Used byRunning time and output of the marking machine

TheoremRunning time and output of the marking machine#✓fully proved

For every bit string \(x\), the marking machine started at its start label, with any flag, with \(x\) on the input stack \(X\) as bit symbols and every other stack empty, reaches the label done within \(8(|x| + 1)^4\) steps, with the output stack \(O\) holding exactly one entry: the answer of the marking algorithm on \(x\).

theorem run (x : List Bool) (v : Bool) (St : ∀ k, List (Γ k))
    (hX : St .X = x.map Sym.bit) (h0 : ∀ k, k ≠ .X → St k = []) :
    ∃ v' S', RunLe prog (8 * (x.length + 1) ^ 4) ⟨some start, v, St⟩ ⟨some .done, v', S'⟩ ∧
      S' .O = [pathCheck x]

Uses 39 · Used by 1

Statement usesStacks of the PATH marking machine · Labels of the PATH marking machine · The marking machine for PATH · Start label of the PATH marking machine · Stack alphabets of the PATH marking machine · The marking algorithm for PATH · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesDecoding a graph · Edge-list decoder · Decoding the bits of an edge list · Bit encoding of an edge list · The edge-list decoder succeeds only on edge bits · Agreement off a set of stacks · Statements of the PATH marking machine · Reading the mark of vertex \(j\) · The frame of a read · The counter unit of the PATH marking machine · The pass loop of the marking machine · The marking algorithm reads the mark of the target · Reading a cut-off unary number · Reading a unary number · Walking to a vertex and setting its mark · Initial marks by setting one entry · A walk step with an exhausted counter · Validation phase of the PATH marking machine · Walk step of the PATH marking machine · Walking along the marks of the PATH marking machine · Decoding a PATH instance · Initial marks · One marking pass · Reach marks · Reading a symbol as a name bit · Reading a unary length prefix · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Bit on top of a stack · Unary counter

Used byThe marking algorithm is polynomial-time

AbbreviationThe marking machine as a host component#✓fully proved

The component machine whose stack indices, stack alphabets, labels and program are those of the marking machine, with its eleven stacks listed once each, in the order: input, output, edge bits, junk, the counters for the source, the target and the number of vertices, the counters for the two ends of an arc, the marks and the parked marks.

abbrev pathComp : Host.Comp where
  K := Machine.K
  Γ := Machine.Γ
  L := Machine.Lab
  prog := Machine.prog
  ks := [.X, .O, .E, .J, .S, .T, .N, .U, .V, .M, .P]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide

Uses 6 · Used by 1

Statement usesComponent machine · Stacks of the PATH marking machine · Labels of the PATH marking machine · The marking machine for PATH · Stack alphabets of the PATH marking machine · Stack alphabet of the SAT verifier

Used byThe marking algorithm is polynomial-time

TheoremThe marking algorithm is polynomial-time#✓fully proved

The marking algorithm for PATH, as a function from bit strings to booleans, is computable in polynomial time by a Turing machine with respect to the canonical bitstring encodings of lists of booleans and of booleans.

theorem isPolyTime_pathCheck : IsPolyTime pathCheck

Uses 22 · Used by 1

Statement usesThe marking algorithm for PATH · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions

Proof usesComponent machine · Decider host · Stacks of the PATH marking machine · Labels of the PATH marking machine · The marking machine for PATH · Running time and output of the marking machine · Start label of the PATH marking machine · Stack alphabets of the PATH marking machine · The marking machine as a host component · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Runs within a step budget

Used byPATH ∈ P

TheoremPATH ∈ P#✓fully proved

PATH ∈ P (Sipser, Theorem 7.14). The decision problem PATH belongs to the class P of decision problems decidable in polynomial time. Here PATH accepts a bit string exactly when it encodes natural numbers \(s\), \(t\), \(n\) and a list \(E\) of pairs of natural numbers such that \(s < n\), \(t < n\) and \(t\) is reachable from \(s\) in zero or more steps along the arcs of \(E\) below \(n\), the pairs \((u, v) \in E\) with \(u < n\) and \(v < n\).

theorem pathDec_mem_P : pathDec ∈ P

Uses 16

Statement usesThe PATH problem · Complexity classes · Decision problems · The complexity class P

Proof usesThe marking algorithm is polynomial-time · The marking algorithm for PATH · The marking algorithm decides PATH · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions

63 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.