Exit labels of the counter comparisons to The edge scan of the Hamiltonian path verifier

DefinitionExit labels of the counter comparisons#✓fully proved

The label the verifier goes to after comparing two counters, where \(a\) is the current vertex, \(b\) the previous one, \(c\) the number of vertices seen, \(n\) the number of vertices and \(s\), \(t\) the two ends: after comparing \(a\) with \(n\) it goes to the head-or-edge dispatch if \(a < n\); after comparing \(a\) with \(s\) it goes to the repeat scan if \(a = s\); after comparing \(c\) with \(n\) it goes to the nonzero-count check if \(c = n\); after comparing \(b\) with \(t\) it goes to the accept label if \(b = t\); in every other case it goes to the reject label.

def cout : CI → Ordering → Lab
  | .an, .lt => .hd
  | .as, .eq => .nd
  | .cn, .eq => .fin
  | .bt, .eq => .yes
  | _, _ => .no

Uses 2 · Used by 7

Statement usesCounter comparisons of the HAMPATH verifier · Labels of the Hamiltonian path verifier

Used byRun of a HAMPATH-verifier counter comparison · Outcome of the HAMPATH verifier's vertex-range comparison · Outcome of a HAMPATH-verifier equality comparison · The Hamiltonian path verifier machine · Running the head-or-edge check · Running the vertex loop · One vertex step of the Hamiltonian-path verifier

DefinitionThe Hamiltonian path verifier machine#✓fully proved

The verifier is the program of the multi-stack machine with the stacks and labels of the Hamiltonian path verifier, every stack over the alphabet \(\mathrm{Sym}\), and a Boolean internal variable, given below label by label. Write \(\mathrm{bit}(x)\) for the bit symbol of a boolean \(x\). Write \((a, n)\), \((a, s)\), \((c, n)\) and \((b, t)\) for the four counter comparisons, and \(\alpha(i)\) and \(\beta(i)\) for the first and the second counter of comparison \(i\). Every unary reader, unary mover, bit-moving loop and transfer below has the label it sits at as its own label; the bit-moving loops read bit symbols as bits and every other symbol as a marker, and push \(\mathrm{bit}(x)\) for a bit \(x\). The transfer from a stack \(k\) onto a list of stacks with next label \(m\) pops \(k\); if it popped a symbol, it pushes \(\mathrm{bit}(\mathrm{true})\) onto each listed stack and returns to its own label, and otherwise it goes to \(m\). An emptiness test of a stack "to \(e\), else \(e'\)" goes to \(e\) if the stack is empty and to \(e'\) otherwise. A transfer also stores in the Boolean variable whether its pop found a symbol, and an emptiness test stores there whether the stack is empty.

• \(\mathsf{rdS}\), \(\mathsf{rdT}\), \(\mathsf{rdN}\): the unary reader from \(X\) onto \(S\), \(T\), \(N\) respectively, with next labels \(\mathsf{rdT}\), \(\mathsf{rdN}\), \(\mathsf{vE}\) respectively.
• \(\mathsf{vE}\): the emptiness test of \(X\) to \(\mathsf{vEb}\), else \(\mathsf{vEU}\). \(\mathsf{vEU}\) and \(\mathsf{vEV}\): the unary mover from \(X\) to \(E\), with next labels \(\mathsf{vEV}\) and \(\mathsf{vE}\) respectively. \(\mathsf{vEb}\): the bit-moving loop from \(E\) to \(X\) with next label \(\mathsf{vW}\).
• \(\mathsf{vW}\): the emptiness test of \(W\) to \(\mathsf{vWb}\), else \(\mathsf{vWU}\). \(\mathsf{vWU}\): the unary mover from \(W\) to \(Z\) with next label \(\mathsf{vW}\). \(\mathsf{vWb}\): the bit-moving loop from \(Z\) to \(W\) with next label \(\mathsf{loop}\).
• \(\mathsf{loop}\): the emptiness test of \(W\) to \(\mathsf{cmp}(c, n)\), else \(\mathsf{rdA}\). \(\mathsf{rdA}\): the unary reader from \(W\) onto \(A\) with next label \(\mathsf{cmp}(a, n)\). \(\mathsf{hd}\): the emptiness test of \(C\) to \(\mathsf{cmp}(a, s)\), else \(\mathsf{scan}\).
• For each comparison \(i\), \(\mathsf{cmp}(i)\) is one round of counter comparison of \(\alpha(i)\) and \(\beta(i)\), with scratch stacks \(R\) (for \(\alpha(i)\)) and \(Q\) (for \(\beta(i)\)), both units \(\mathrm{bit}(\mathrm{true})\), own label \(\mathsf{cmp}(i)\), and \(\mathsf{cr}(i, <)\), \(\mathsf{cr}(i, =)\), \(\mathsf{cr}(i, >)\) as its labels \(\mathit{lt}\), \(\mathit{eq}\) and \(\mathit{gt}\). For each ordering \(o\), \(\mathsf{cr}(i, o)\) is the transfer from \(R\) onto \(\alpha(i)\) with next label \(\mathsf{crb}(i, o)\), and \(\mathsf{crb}(i, o)\) is the transfer from \(Q\) onto \(\beta(i)\) whose next label is the exit label of the counter comparison \(i\) with outcome \(o\).
• \(\mathsf{scan}\): the emptiness test of \(X\) to \(\mathsf{no}\), else \(\mathsf{ceU}(\mathrm{true})\). For each boolean \(\mathit{ok}\): \(\mathsf{ceU}(\mathit{ok})\) is the step of the unary comparison loop with source \(X\), save stack \(E\), counter \(B\), label families \(\mathsf{ceU}\) and \(\mathsf{rsU}\), and verdict \(\mathit{ok}\); \(\mathsf{rsU}(\mathit{ok})\) is the transfer from \(R\) onto \(B\) with next label \(\mathsf{ceV}(\mathit{ok})\); \(\mathsf{ceV}(\mathit{ok})\) is the step of the unary comparison loop with source \(X\), save stack \(E\), counter \(A\), label families \(\mathsf{ceV}\) and \(\mathsf{rsV}\), and verdict \(\mathit{ok}\); and \(\mathsf{rsV}(\mathit{ok})\) is the transfer from \(R\) onto \(A\) with next label \(\mathsf{scB}\) if \(\mathit{ok}\) is true and \(\mathsf{scan}\) otherwise. \(\mathsf{scB}\): the bit-moving loop from \(E\) to \(X\) with next label \(\mathsf{nd}\).
• \(\mathsf{nd}\): the emptiness test of \(W\) to \(\mathsf{ndB}\), else \(\mathsf{cbN}(\mathrm{true})\). For each boolean \(\mathit{ok}\): \(\mathsf{cbN}(\mathit{ok})\) is the step of the unary comparison loop with source \(W\), save stack \(Z\), counter \(A\), label families \(\mathsf{cbN}\) and \(\mathsf{rsN}\), and verdict \(\mathit{ok}\); and \(\mathsf{rsN}(\mathit{ok})\) is the transfer from \(R\) onto \(A\) with next label \(\mathsf{no}\) if \(\mathit{ok}\) is true and \(\mathsf{nd}\) otherwise. \(\mathsf{ndB}\): the bit-moving loop from \(Z\) to \(W\) with next label \(\mathsf{incC}\).
• \(\mathsf{fin}\): the emptiness test of \(C\) to \(\mathsf{no}\), else \(\mathsf{cmp}(b, t)\). \(\mathsf{incC}\): the counter increment pushing \(\mathrm{bit}(\mathrm{true})\) onto \(C\) and going to \(\mathsf{dB}\). \(\mathsf{dB}\): the transfer from \(B\) onto no stack (it drains \(B\)) with next label \(\mathsf{mA}\). \(\mathsf{mA}\): the transfer from \(A\) onto \(B\) with next label \(\mathsf{loop}\).
• \(\mathsf{yes}\) and \(\mathsf{no}\): halt.

The verifier parses and validates the input and the witness, then walks the vertices.

Cslib.Complexity.Karp.HamVerify.prog · 34 lines

def prog : Lab → TM2.Stmt (fun _ : K => Sym) Lab Bool
  | .rdS => readU .X .S .rdS .rdT
  | .rdT => readU .X .T .rdT .rdN
  | .rdN => readU .X .N .rdN .vE
  | .vE => ifE .X .vEb .vEU
  | .vEU => skipU .X .E .vEU .vEV
  | .vEV => skipU .X .E .vEV .vE
  | .vEb => moveB .E .X Sym.bit? Sym.bit .vEb .vW
  | .vW => ifE .W .vWb .vWU
  | .vWU => skipU .W .Z .vWU .vW
  | .vWb => moveB .Z .W Sym.bit? Sym.bit .vWb .loop
  | .loop => ifE .W (.cmp .cn) .rdA
  | .rdA => readU .W .A .rdA (.cmp .an)
  | .hd => ifE .C (.cmp .as) .scan
  | .cmp i => cmpStep (ca i) (cb i) .R .Q (Sym.bit true) (Sym.bit true) (.cmp i) (.cr i .lt)
      (.cr i .eq) (.cr i .gt)
  | .cr i o => xfer .R [⟨ca i, Sym.bit true⟩] (.cr i o) (.crb i o)
  | .crb i o => xfer .Q [⟨cb i, Sym.bit true⟩] (.crb i o) (cout i o)
  | .scan => ifE .X .no (.ceU true)
  | .ceU ok => cbS .X .E .B .ceU .rsU ok
  | .rsU ok => xfer .R [⟨.B, Sym.bit true⟩] (.rsU ok) (.ceV ok)
  | .ceV ok => cbS .X .E .A .ceV .rsV ok
  | .rsV ok => xfer .R [⟨.A, Sym.bit true⟩] (.rsV ok) (if ok then .scB else .scan)
  | .scB => moveB .E .X Sym.bit? Sym.bit .scB .nd
  | .nd => ifE .W .ndB (.cbN true)
  | .cbN ok => cbS .W .Z .A .cbN .rsN ok
  | .rsN ok => xfer .R [⟨.A, Sym.bit true⟩] (.rsN ok) (if ok then .no else .nd)
  | .ndB => moveB .Z .W Sym.bit? Sym.bit .ndB .incC
  | .fin => ifE .C .no (.cmp .bt)
  | .incC => incr .C (Sym.bit true) .dB
  | .dB => xfer .B [] .dB .mA
  | .mA => xfer .A [⟨.B, Sym.bit true⟩] .mA .loop
  | .yes => .halt
  | .no => .halt

Uses 17 · Used by 21

Statement usesCounter comparisons of the HAMPATH verifier · Stacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · First counter of a HAMPATH-verifier comparison · Second counter of a HAMPATH-verifier comparison · Step of the HAMPATH verifier's unary comparison loop · Exit labels of the counter comparisons · Emptiness test · The unary reader of the Hamiltonian path verifier · The unary mover of the Hamiltonian path verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Flag bit of a machine state · One round of counter comparison · Counter increment · Bit-moving loop · Counter transfer loop

Used byRun of the HAMPATH verifier's unary comparison loop · Run of a HAMPATH-verifier counter comparison · HAMPATH-verifier unary comparison with the counter restored · One step of the emptiness test · Moving a stack of bits · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The unary reader of the Hamiltonian path verifier reads a terminated number · The edge scan of the Hamiltonian path verifier · The unary mover of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier moves a terminated number · A single step of the Hamiltonian-path verifier · The edge-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier · HAMPATH is in NP · The HAMPATH verifier as a host component · Running the head-or-edge check · Running the vertex loop · The repeat scan of the Hamiltonian path verifier · Correctness and running time of the Hamiltonian path verifier · One vertex step of the Hamiltonian-path verifier · The rest of a vertex step in the Hamiltonian-path verifier

DefinitionStart label of the Hamiltonian-path verifier#✓fully proved

The verifier starts at the label \(\mathsf{rdS}\), where it reads the first unary number of the input stack \(X\) (the start vertex \(s\)) onto the counter stack \(S\).

def start : Lab := .rdS

Uses 1 · Used by 2

Statement usesLabels of the Hamiltonian path verifier

Used byHAMPATH is in NP · Correctness and running time of the Hamiltonian path verifier

TheoremInterleaved stack updates in the Hamiltonian-path verifier#✓fully proved

Let \(a \ne b\) be two stacks of the verifier, \(S\) an assignment of a list of symbols to each stack, and \(p, p', t, t'\) lists of symbols. Setting \(a\) to \(p\), then \(b\) to \(t\), then \(a\) to \(p'\), then \(b\) to \(t'\) in \(S\) gives the same assignment as setting \(a\) to \(p'\) and then \(b\) to \(t'\).

theorem update_update_update_update {a b : K} (hab : a ≠ b) (S : ∀ _ : K, List Sym)
    (p p' t t' : List Sym) :
    update (update (update (update S a p) b t) a p') b t' = update (update S a p') b t'

Uses 2 · Used by 4

Statement usesStacks of the Hamiltonian path verifier · Stack alphabet of the SAT verifier

Used byThe unary reader of the Hamiltonian path verifier reads a terminated number · The unary mover of the Hamiltonian path verifier moves a terminated number · The edge-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier

TheoremA single step of the Hamiltonian-path verifier#✓fully proved

Let \(l, l'\) be labels, \(v\) a flag value and \(S, S'\) assignments of a list of symbols to each stack. If executing the verifier's statement at \(l\) with flag \(v\) and stacks \(S\) jumps to the label \(l'\) and leaves the stacks \(S'\), then the verifier goes in exactly one step from label \(l\), flag \(v\) and stacks \(S\) to label \(l'\) and stacks \(S'\), with some flag value.

theorem step1 {l l' : Lab} {v : Bool} {S S' : ∀ _ : K, List Sym}
    (h : (TM2.stepAux (prog l) v S).l = some l') (h' : (TM2.stepAux (prog l) v S).stk = S') :
    ∃ v', Run prog 1 ⟨some l, v, S⟩ ⟨some l', v', S'⟩

Uses 6 · Used by 6

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The Hamiltonian path verifier machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label

Used byRun of the HAMPATH verifier's unary comparison loop · One step of the emptiness test · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The unary reader of the Hamiltonian path verifier reads a terminated number · The unary mover of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier moves a terminated number

TheoremOne step of the emptiness test#✓fully proved

If the verifier's instruction at label \(l\) is the emptiness test of stack \(k\) with targets \(e\) and \(ne\), then from label \(l\), in any internal state and on any stacks, exactly one step of the verifier leads to label \(e\) if stack \(k\) is empty and to label \(ne\) otherwise, in some internal state and with the stacks unchanged.

theorem ifE_run {l e ne : Lab} {k : K} (hp : prog l = ifE k e ne) (v : Bool)
    (St : ∀ _ : K, List Sym) :
    ∃ v', Run prog 1 ⟨some l, v, St⟩ ⟨some (if St k = [] then e else ne), v', St⟩

Uses 7 · Used by 6

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Emptiness test · The Hamiltonian path verifier machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesA single step of the Hamiltonian-path verifier

Used byThe edge scan of the Hamiltonian path verifier · The edge-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier · Running the head-or-edge check · Running the vertex loop · The repeat scan of the Hamiltonian path verifier

TheoremThe unary reader of the Hamiltonian path verifier reads a terminated number#✓fully proved

Let \(\mathsf{src} \ne c\) be stacks and \(\ell\), \(m\) labels such that the verifier's statement at \(\ell\) is the unary reader from \(\mathsf{src}\) onto \(c\) with own label \(\ell\) and next label \(m\). Let \(k, j\) be natural numbers and \(r\) a bit list, and suppose that \(\mathsf{src}\) holds \(k\) copies of true, then false, then \(r\) (as bit symbols, first bit on top) and that \(c\) holds \(j\) copies of the bit true. Then from label \(\ell\), with either value of the Boolean variable, the verifier reaches label \(m\) in exactly \(k + 1\) steps, with \(\mathsf{src}\) holding the bits of \(r\), \(c\) holding \(k + j\) copies of the bit true, and every other stack unchanged.

theorem readU_run {src c : K} {self next : Lab} (hp : prog self = readU src c self next)
    (hc : c ≠ src) : ∀ (k j : ℕ) (r : List Bool) (v : Bool) (St : ∀ _ : K, List Sym),
      St src = (List.replicate k true ++ false :: r).map Sym.bit → St c = cnt (Sym.bit true) j →
      ∃ v', Run prog (k + 1) ⟨some self, v, St⟩ ⟨some next, v',
        update (update St src (r.map Sym.bit)) c (cnt (Sym.bit true) (k + j))⟩

Uses 10 · Used by 2

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The Hamiltonian path verifier machine · The unary reader of the Hamiltonian path verifier · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesA single step of the Hamiltonian-path verifier · Interleaved stack updates in the Hamiltonian-path verifier · Reading a symbol as a name bit

Used byCorrectness and running time of the Hamiltonian path verifier · One vertex step of the Hamiltonian-path verifier

TheoremThe unary reader of the Hamiltonian path verifier rejects an unterminated number#✓fully proved

Let \(\mathsf{src} \ne c\) be stacks and \(\ell\), \(m\) labels such that the verifier's statement at \(\ell\) is the unary reader from \(\mathsf{src}\) onto \(c\) with own label \(\ell\) and next label \(m\). Let \(l\) be a bit list from which no unary length can be read (that is, \(l\) contains no false), and suppose that \(\mathsf{src}\) holds the bits of \(l\) (as bit symbols, first bit on top). Then from label \(\ell\), with either value of the Boolean variable and any contents of the other stacks, the verifier reaches label \(\mathrm{no}\) within \(|l| + 1\) steps.

theorem readU_none {src c : K} {self next : Lab} (hp : prog self = readU src c self next)
    (hc : c ≠ src) : ∀ (l : List Bool) (v : Bool) (St : ∀ _ : K, List Sym),
      readUnaryLength l = none → St src = l.map Sym.bit →
      ∃ v' S', RunLe prog (l.length + 1) ⟨some self, v, St⟩ ⟨some .no, v', S'⟩

Uses 12 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The Hamiltonian path verifier machine · The unary reader of the Hamiltonian path verifier · Stack alphabet of the SAT verifier · Reading a unary length prefix · Runs within a step budget

Proof usesA single step of the Hamiltonian-path verifier · 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 byCorrectness and running time of the Hamiltonian path verifier

TheoremExtending a reversed unary block#✓fully proved

For \(a \in \mathbb{N}\), let \(\beta_a\) be the list of symbols obtained by mapping the bit symbol over the reversal of the unary block of \(a\) (\(a\) copies of true followed by one false), that is, the bit symbol of false followed by \(a\) bit symbols of true. Then for every list \(L\) of symbols, \(\beta_a\) followed by the bit symbol of true and then \(L\) equals \(\beta_{a+1}\) followed by \(L\).

theorem blk_succ (a : ℕ) (L : List Sym) :
    (List.replicate a true ++ [false]).reverse.map Sym.bit ++ Sym.bit true :: L =
      (List.replicate (a + 1) true ++ [false]).reverse.map Sym.bit ++ L

Uses 1 · Used by 2

Statement usesStack alphabet of the SAT verifier

Used byRun of the HAMPATH verifier's unary comparison loop · The unary mover of the Hamiltonian path verifier moves a terminated number

TheoremThe unary mover of the Hamiltonian path verifier moves a terminated number#✓fully proved

Let \(\mathsf{src} \ne \mathsf{dst}\) be stacks and \(\ell\), \(m\) labels such that the verifier's statement at \(\ell\) is the unary mover from \(\mathsf{src}\) to \(\mathsf{dst}\) with own label \(\ell\) and next label \(m\). Let \(k\) be a natural number and \(r\) a bit list, and suppose that \(\mathsf{src}\) holds \(k\) copies of true, then false, then \(r\) (as bit symbols, first bit on top). Then from label \(\ell\), with either value of the Boolean variable, the verifier reaches label \(m\) in exactly \(k + 1\) steps, with \(\mathsf{src}\) holding the bits of \(r\), with \(\mathsf{dst}\) holding the bit false followed by \(k\) copies of the bit true on top of its previous contents, and with every other stack unchanged.

theorem skipU_run {src dst : K} {self next : Lab} (hp : prog self = skipU src dst self next)
    (hd : dst ≠ src) : ∀ (k : ℕ) (r : List Bool) (v : Bool) (St : ∀ _ : K, List Sym),
      St src = (List.replicate k true ++ false :: r).map Sym.bit →
      ∃ v', Run prog (k + 1) ⟨some self, v, St⟩ ⟨some next, v',
        update (update St src (r.map Sym.bit)) dst
          ((List.replicate k true ++ [false]).reverse.map Sym.bit ++ St dst)⟩

Uses 10 · Used by 2

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The Hamiltonian path verifier machine · The unary mover of the Hamiltonian path verifier · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesExtending a reversed unary block · A single step of the Hamiltonian-path verifier · Interleaved stack updates in the Hamiltonian-path verifier · Reading a symbol as a name bit

Used byThe edge-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier

TheoremThe unary mover of the Hamiltonian path verifier rejects an unterminated number#✓fully proved

Let \(\mathsf{src} \ne \mathsf{dst}\) be stacks and \(\ell\), \(m\) labels such that the verifier's statement at \(\ell\) is the unary mover from \(\mathsf{src}\) to \(\mathsf{dst}\) with own label \(\ell\) and next label \(m\). Let \(l\) be a bit list from which no unary length can be read (that is, \(l\) contains no false), and suppose that \(\mathsf{src}\) holds the bits of \(l\) (as bit symbols, first bit on top). Then from label \(\ell\), with either value of the Boolean variable and any contents of the other stacks, the verifier reaches label \(\mathrm{no}\) within \(|l| + 1\) steps.

theorem skipU_none {src dst : K} {self next : Lab} (hp : prog self = skipU src dst self next)
    (hd : dst ≠ src) : ∀ (l : List Bool) (v : Bool) (St : ∀ _ : K, List Sym),
      readUnaryLength l = none → St src = l.map Sym.bit →
      ∃ v' S', RunLe prog (l.length + 1) ⟨some self, v, St⟩ ⟨some .no, v', S'⟩

Uses 12 · Used by 2

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The Hamiltonian path verifier machine · The unary mover of the Hamiltonian path verifier · Stack alphabet of the SAT verifier · Reading a unary length prefix · Runs within a step budget

Proof usesA single step of the Hamiltonian-path verifier · 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-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier

TheoremMoving a stack of bits#✓fully proved

Suppose the verifier's instruction at label \(p\) is the bit-moving loop from a stack \(a\) to a different stack \(b\), continuing at label \(p'\) when done. If stack \(a\) holds exactly the bits of a list \(l\), then from label \(p\) in any internal state the verifier takes exactly \(|l| + 1\) steps to reach label \(p'\), in some internal state, with stack \(a\) empty, stack \(b\) holding the bits of \(l\) in reverse order followed by its old contents, and every other stack unchanged.

theorem mv_run {self next : Lab} {a b : K} (hp : prog self = moveB a b Sym.bit? Sym.bit self next)
    (hab : a ≠ b) (l : List Bool) (v : Bool) (St : ∀ _ : K, List Sym)
    (ha : St a = l.map Sym.bit) :
    ∃ v', Run prog (l.length + 1) ⟨some self, v, St⟩
      ⟨some next, v', update (update St a []) b ((l.map Sym.bit).reverse ++ St b)⟩

Uses 9 · Used by 3

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The Hamiltonian path verifier 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 byThe edge scan of the Hamiltonian path verifier · The repeat scan of the Hamiltonian path verifier · Correctness and running time of the Hamiltonian path verifier

TheoremRun of a HAMPATH-verifier counter comparison#✓fully proved

Let \(i\) be one of the four counter comparisons of the HAMPATH verifier, with first counter \(\mathrm{ca}(i)\) and second counter \(\mathrm{cb}(i)\), and let \(m, n \in \mathbb{N}\). Suppose the stacks \(\sigma\) hold \(m\) units (bit symbols of true) on \(\mathrm{ca}(i)\), \(n\) units on \(\mathrm{cb}(i)\), and nothing on the scratch stacks \(R\) and \(Q\). Then for every flag \(v\) the verifier goes, in at most \(3 \min(m, n) + 4\) steps, from label \(\mathrm{cmp}(i)\) with flag \(v\) and stacks \(\sigma\) to the label \(\mathrm{cout}(i, o)\) that comparison \(i\) picks on the ordering \(o = \mathrm{compare}(m, n) \in \{\mathrm{lt}, \mathrm{eq}, \mathrm{gt}\}\) of \(m\) and \(n\), with flag false and the same stacks \(\sigma\).

theorem cmpI_run (i : CI) (m n : ℕ) (v : Bool) (St : ∀ _ : K, List Sym)
    (ha : St (ca i) = cnt (Sym.bit true) m) (hb : St (cb i) = cnt (Sym.bit true) n)
    (hR : St .R = []) (hQ : St .Q = []) :
    RunLe prog (3 * min m n + 4) ⟨some (.cmp i), v, St⟩ ⟨some (cout i (compare m n)), false, St⟩

Uses 13 · Used by 3

Statement usesCounter comparisons of the HAMPATH verifier · Stacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · First counter of a HAMPATH-verifier comparison · Second counter of a HAMPATH-verifier comparison · Exit labels of the counter comparisons · The Hamiltonian path verifier machine · Stack alphabet of the SAT verifier · Runs within a step budget · Unary counter

Proof usesFlag bit of a machine state · Exact-length runs of a TM2 machine · Non-destructive comparison of two counters

Used byRunning the head-or-edge check · Running the vertex loop · One vertex step of the Hamiltonian-path verifier

TheoremOutcome of the HAMPATH verifier's vertex-range comparison#✓fully proved

For all \(m, n \in \mathbb{N}\), the label that the comparison of the current vertex with the vertex count picks on the ordering \(\mathrm{compare}(m, n)\) of \(m\) and \(n\) is the head-or-edge dispatch label \(\mathrm{hd}\) if \(m < n\), and the reject label \(\mathrm{no}\) otherwise.

theorem cout_an (m n : ℕ) : cout .an (compare m n) = if m < n then .hd else .no

Uses 3 · Used by 1

Statement usesCounter comparisons of the HAMPATH verifier · Labels of the Hamiltonian path verifier · Exit labels of the counter comparisons

Used byOne vertex step of the Hamiltonian-path verifier

TheoremOutcome of a HAMPATH-verifier equality comparison#✓fully proved

Write \(\mathrm{cout}(i, o)\) for the label that counter comparison \(i\) of the HAMPATH verifier picks on the ordering \(o \in \{\mathrm{lt}, \mathrm{eq}, \mathrm{gt}\}\). Let \(i\) be a counter comparison and \(l\) a label such that \(\mathrm{cout}(i, \mathrm{eq}) = l\) and \(\mathrm{cout}(i, o)\) is the reject label \(\mathrm{no}\) for every ordering \(o \ne \mathrm{eq}\). Then for all \(m, n \in \mathbb{N}\), the label \(\mathrm{cout}(i, \mathrm{compare}(m, n))\) on the ordering of \(m\) and \(n\) is \(l\) if \(m = n\) and \(\mathrm{no}\) otherwise.

theorem cout_eq (i : CI) (l : Lab) (hl : cout i .eq = l) (hne : ∀ o, o ≠ .eq → cout i o = .no)
    (m n : ℕ) : cout i (compare m n) = if m = n then l else .no

Uses 3 · Used by 2

Statement usesCounter comparisons of the HAMPATH verifier · Labels of the Hamiltonian path verifier · Exit labels of the counter comparisons

Used byRunning the head-or-edge check · Running the vertex loop

TheoremRun of the HAMPATH verifier's unary comparison loop#✓fully proved

Let \(\mathit{src}\), \(\mathit{sv}\), \(c\) and the scratch stack \(R\) be four distinct stacks of the HAMPATH verifier, and let \(\mathrm{cb}\) and \(\mathrm{fin}\) be families of labels indexed by booleans such that for every boolean \(\mathit{ok}\) the instruction at \(\mathrm{cb}(\mathit{ok})\) is the unary comparison step on \(\mathit{src}\), \(\mathit{sv}\), \(c\) with loop labels \(\mathrm{cb}\), exit labels \(\mathrm{fin}\) and verdict \(\mathit{ok}\). Write \(1\) and \(0\) for the bit symbols of true and false, \(1^k\) for \(k\) copies of \(1\), and \(\bar r\) for the list of bit symbols of a list of booleans \(r\); stacks are listed from the top. Then for all \(a, u, j \in \mathbb{N}\), every boolean \(\mathit{ok}\), every list of booleans \(r\), every flag \(v\) and all stack contents \(\sigma\) with \(\sigma(\mathit{src}) = 1^a\,0\,\bar r\), \(\sigma(c) = 1^u\) and \(\sigma(R) = 1^j\), the verifier runs in exactly \(a + 1\) steps from label \(\mathrm{cb}(\mathit{ok})\) with flag \(v\) and stacks \(\sigma\) to label \(\mathrm{fin}(b)\), where \(b\) is true exactly when \(\mathit{ok}\) is true and \(a = u\), with some flag and some stacks \(\sigma'\) such that \(\sigma'(\mathit{src}) = \bar r\), \(\sigma'(\mathit{sv}) = 0\,1^a\,\sigma(\mathit{sv})\), \(\sigma'(c) = 1^{\max(u - a, 0)}\), \(\sigma'(R) = 1^{\min(a, u) + j}\), and \(\sigma'(k) = \sigma(k)\) for every other stack \(k\).

theorem cb_run {src sv c : K} {cb fin : Bool → Lab}
    (hp : ∀ ok, prog (cb ok) = cbS src sv c cb fin ok) (h1 : sv ≠ src) (h2 : c ≠ src)
    (h3 : K.R ≠ src) (h4 : c ≠ sv) (h5 : K.R ≠ sv) (h6 : K.R ≠ c) :
    ∀ (a u j : ℕ) (ok : Bool) (r : List Bool) (v : Bool) (St : ∀ _ : K, List Sym),
      St src = (List.replicate a true ++ false :: r).map Sym.bit → St c = cnt (Sym.bit true) u →
      St .R = cnt (Sym.bit true) j →
      ∃ v' S', Run prog (a + 1) ⟨some (cb ok), v, St⟩
        ⟨some (fin (ok && decide (a = u))), v', S'⟩ ∧ S' src = r.map Sym.bit ∧
        S' sv = (List.replicate a true ++ [false]).reverse.map Sym.bit ++ St sv ∧
        S' c = cnt (Sym.bit true) (u - a) ∧ S' .R = cnt (Sym.bit true) (min a u + j) ∧
        ∀ k, k ≠ src → k ≠ sv → k ≠ c → k ≠ .R → S' k = St k

Uses 10 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Step of the HAMPATH verifier's unary comparison loop · The Hamiltonian path verifier machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesExtending a reversed unary block · A single step of the Hamiltonian-path verifier · Reading a symbol as a name bit

Used byHAMPATH-verifier unary comparison with the counter restored

TheoremHAMPATH-verifier unary comparison with the counter restored#✓fully proved

Let \(\mathit{src}\), \(\mathit{sv}\), \(c\) and the scratch stack \(R\) be four distinct stacks of the HAMPATH verifier, and let \(\mathrm{cb}\), \(\mathrm{rs}\) and \(\mathrm{nx}\) be families of labels indexed by booleans such that for every boolean \(\mathit{ok}\) the instruction at \(\mathrm{cb}(\mathit{ok})\) is the unary comparison step on \(\mathit{src}\), \(\mathit{sv}\), \(c\) with loop labels \(\mathrm{cb}\), exit labels \(\mathrm{rs}\) and verdict \(\mathit{ok}\), and the instruction at \(\mathrm{rs}(\mathit{ok})\) is the transfer loop that pops \(R\) until it is empty, pushing one unit (the bit symbol of true) on \(c\) per symbol popped, and then goes to \(\mathrm{nx}(\mathit{ok})\). Write \(1\) and \(0\) for the bit symbols of true and false, \(1^k\) for \(k\) copies of \(1\), and \(\bar r\) for the list of bit symbols of a list of booleans \(r\); stacks are listed from the top. Let \(a, u \in \mathbb{N}\), let \(\mathit{ok}\) be a boolean, \(r\) a list of booleans, \(v\) a flag, and \(\sigma\) stack contents with \(\sigma(\mathit{src}) = 1^a\,0\,\bar r\), \(\sigma(c) = 1^u\) and \(\sigma(R)\) empty. Then the verifier runs in exactly \((a + 1) + (\min(a, u) + 1)\) steps from label \(\mathrm{cb}(\mathit{ok})\) with flag \(v\) and stacks \(\sigma\) to label \(\mathrm{nx}(b)\), where \(b\) is true exactly when \(\mathit{ok}\) is true and \(a = u\), with some flag and with the stacks of \(\sigma\) except that \(\mathit{src}\) now holds \(\bar r\) and \(\mathit{sv}\) holds \(0\,1^a\) followed by \(\sigma(\mathit{sv})\).

theorem cmpN_run {src sv c : K} {cb rs nx : Bool → Lab}
    (hp : ∀ ok, prog (cb ok) = cbS src sv c cb rs ok)
    (hr : ∀ ok, prog (rs ok) = xfer .R [⟨c, Sym.bit true⟩] (rs ok) (nx ok))
    (h1 : sv ≠ src) (h2 : c ≠ src) (h3 : K.R ≠ src) (h4 : c ≠ sv) (h5 : K.R ≠ sv)
    (h6 : K.R ≠ c) (a u : ℕ) (ok : Bool) (r : List Bool) (v : Bool) (St : ∀ _ : K, List Sym)
    (hs : St src = (List.replicate a true ++ false :: r).map Sym.bit)
    (hc : St c = cnt (Sym.bit true) u) (hR : St .R = []) :
    ∃ v', Run prog (a + 1 + (min a u + 1)) ⟨some (cb ok), v, St⟩
      ⟨some (nx (ok && decide (a = u))), v', update (update St src (r.map Sym.bit)) sv
        ((List.replicate a true ++ [false]).reverse.map Sym.bit ++ St sv)⟩

Uses 12 · Used by 2

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Step of the HAMPATH verifier's unary comparison loop · The Hamiltonian path verifier machine · Stack alphabet of the SAT verifier · Flag bit of a machine state · Exact-length runs of a TM2 machine · Unary counter · Counter transfer loop

Proof usesRun of the HAMPATH verifier's unary comparison loop · Adding units to target stacks · Running a counter transfer

Used byThe edge scan of the Hamiltonian path verifier · The repeat scan of the Hamiltonian path verifier

TheoremThe edge-list check of the Hamiltonian-path verifier#✓fully proved

Let \(r\) and \(acc\) be bit lists, and let the stacks \(St\) hold \(r\) on the input stack \(X\) and the reverse of \(acc\) on the save stack \(E\). Started at the label \(\mathsf{vE}\) with any flag value, the verifier reaches within at most \(2|r| + 1\) steps the label \(\mathsf{vEb}\) if \(r\) decodes as an edge list (a sequence of pairs of unary numbers, each a block of ones ended by a zero) and the label \(\mathsf{no}\) otherwise. When \(r\) decodes, the final stacks are \(St\) with \(X\) emptied and \(E\) holding the reverse of the concatenation of \(acc\) and \(r\) (that is, \(r\) reversed on top of \(acc\) reversed), all other stacks unchanged.

theorem valE_run : ∀ (r acc : List Bool) (v : Bool) (St : ∀ _ : K, List Sym),
    St .X = r.map Sym.bit → St .E = acc.reverse.map Sym.bit →
    ∃ v' S', RunLe prog (2 * r.length + 1) ⟨some .vE, v, St⟩
      ⟨some (if (Karp.decodeEs r).isSome then .vEb else .no), v', S'⟩ ∧
      ((Karp.decodeEs r).isSome →
        S' = update (update St .X []) .E ((acc ++ r).reverse.map Sym.bit))

Uses 16 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The Hamiltonian path verifier machine · Edge-list decoder · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesOne step of the emptiness test · The unary mover of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier moves a terminated number · Interleaved stack updates in the Hamiltonian-path verifier · Decoding 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 · Reading a unary length prefix · Exact-length runs of a TM2 machine

Used byCorrectness and running time of the Hamiltonian path verifier

TheoremThe witness check of the Hamiltonian-path verifier#✓fully proved

Let \(w\) and \(acc\) be bit lists, and let the stacks \(St\) hold \(w\) on the witness stack \(W\) and the reverse of \(acc\) on the save stack \(Z\). Started at the label \(\mathsf{vW}\) with any flag value, the verifier reaches within at most \(2|w| + 1\) steps the label \(\mathsf{vWb}\) if \(w\) decodes as a vertex list (a sequence of unary numbers, each a block of ones ended by a zero) and the label \(\mathsf{no}\) otherwise. When \(w\) decodes, the final stacks are \(St\) with \(W\) emptied and \(Z\) holding the reverse of the concatenation of \(acc\) and \(w\) (that is, \(w\) reversed on top of \(acc\) reversed), all other stacks unchanged.

theorem valW_run : ∀ (w acc : List Bool) (v : Bool) (St : ∀ _ : K, List Sym),
    St .W = w.map Sym.bit → St .Z = acc.reverse.map Sym.bit →
    ∃ v' S', RunLe prog (2 * w.length + 1) ⟨some .vW, v, St⟩
      ⟨some (if (decodeW w).isSome then .vWb else .no), v', S'⟩ ∧
      ((decodeW w).isSome → S' = update (update St .W []) .Z ((acc ++ w).reverse.map Sym.bit))

Uses 15 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Witness decoder · The Hamiltonian path verifier machine · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesDecoding the empty witness · Witness decoding fails on a cut-off first number · Decoding peels off the first number · One step of the emptiness test · The unary mover of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier moves a terminated number · Interleaved stack updates in the Hamiltonian-path verifier · Reading a unary length prefix · Exact-length runs of a TM2 machine

Used byCorrectness and running time of the Hamiltonian path verifier

TheoremThe edge scan of the Hamiltonian path verifier#✓fully proved

For a list \(e\) of pairs of natural numbers write \(\mathrm{bits}(e)\) for its edge-list encoding, in which each pair \((u, u')\) contributes \(u\) copies of true, then false, then \(u'\) copies of true, then false. Let \(a, b\) be natural numbers and \(r\), \(d\) lists of pairs of natural numbers. Suppose that the verifier's stacks hold, as bit symbols with the first bit on top, \(\mathrm{bits}(r)\) on \(\mathsf{X}\), \(\mathrm{bits}(d)\) in reverse order on \(\mathsf{E}\), \(a\) copies of the bit true on \(\mathsf{A}\), \(b\) copies of the bit true on \(\mathsf{B}\), and nothing on \(\mathsf{R}\), the other stacks being arbitrary. Started at label \(\mathrm{scan}\) with either value of its Boolean variable, the verifier reaches, within \(4|\mathrm{bits}(r)| + |\mathrm{bits}(d)| + 2\) steps, the label \(\mathrm{nd}\) if \((b, a)\) is one of the pairs of \(r\) and the label \(\mathrm{no}\) otherwise. In the first case its stacks are then the initial ones except that \(\mathsf{X}\) holds the encoding \(\mathrm{bits}\) of the list \(d\) followed by \(r\), and \(\mathsf{E}\) is empty.

theorem scan_run (a b : ℕ) : ∀ (rest done : List (ℕ × ℕ)) (v : Bool) (St : ∀ _ : K, List Sym),
    St .X = (Karp.edgeBits rest).map Sym.bit → St .E = (Karp.edgeBits done).reverse.map Sym.bit →
    St .A = cnt (Sym.bit true) a → St .B = cnt (Sym.bit true) b → St .R = [] →
    ∃ v' S', RunLe prog (4 * (Karp.edgeBits rest).length + (Karp.edgeBits done).length + 2)
      ⟨some .scan, v, St⟩ ⟨some (if (b, a) ∈ rest then .nd else .no), v', S'⟩ ∧
      ((b, a) ∈ rest →
        S' = update (update St .X ((Karp.edgeBits (done ++ rest)).map Sym.bit)) .E [])

Uses 13 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The Hamiltonian path verifier machine · Bit encoding of an edge list · Stack alphabet of the SAT verifier · Runs within a step budget · Unary counter

Proof usesHAMPATH-verifier unary comparison with the counter restored · Bits of concatenated edge lists · Bits of an edge list, first edge first · One step of the emptiness test · Moving a stack of bits · Exact-length runs of a TM2 machine

Used byRunning the head-or-edge check

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.