End of a clause in the detour walk to HAMPATH emitter, phase A: copying a reversed name onto two stacks

DefinitionEnd of a clause in the detour walk#✓fully proved

For booleans \(p_p\) and \(p_n\) (the flags recording whether the current clause contains the current variable positively, respectively negatively), the detour walk continues at the end of the clause at the label where the first positive detour site \(d_{1u}\) starts with passed bit \(p_n\) if \(p_p\) is true; otherwise, if \(p_n\) is true, at the label where the first negative detour site \(d_{3u}\) starts with passed bit false; and otherwise at the label that ends the clause.

def clEnd (pp pn : Bool) : Lab := if pp then .cpA .d1u pn else if pn then .cpA .d3u false else .dj

Uses 2 · Used by 4

Statement usesLabels of the HAMPATH emitter · Copy sites of the HAMPATH emitter

Used byThe HAMPATH emitter machine · One clause of the detour walk · One literal of the detour walk · The detour walk of a diamond in the HAMPATH emitter

DefinitionThe HAMPATH emitter machine#✓fully proved

The emitter is the multi-stack machine with the emitter's stacks (the output stack \(O\) holds bits, every other stack holds token symbols), the emitter's labels, and a boolean internal state. Below, moving the bit block of a stack \(A\) onto a stack \(B\) means popping \(A\) while its top is a name bit \(\mathrm{bit}(b)\) and pushing each popped bit onto \(B\) (as \(\mathrm{bit}(b)\), or as the bit \(b\) when \(B = O\)). Comparing \(F\) with \(V\) means popping both while their tops are equal name bits, pushing each such bit onto \(X\) and onto \(Y\), and ending with "equal" if both bit blocks end together and with "different", without popping, at the first mismatch. Draining \(A\), pushing on given stacks, means popping \(A\) until it is empty and pushing on each of those stacks one symbol per popped symbol. Every pushed symbol not otherwise named is the separator \(\mathrm{cl}\). A list of steps written for several labels in turn is done one label at a time, each label passing to the next.

Phase A. At \(\mathrm{a0}\): if \(T\) is empty, go to \(\mathrm{b0}\); if its top is \(\mathrm{cl}\), pop it, push \(\mathrm{cl}\) once on \(F\), once on \(C\) and three times on \(M\), and go to \(\mathrm{a0}\); otherwise pop it, push on \(F\) the polarity marker \(\mathrm{lit}(s)\), where \(s\) is true exactly when the popped symbol is \(\mathrm{lit}(\mathrm{true})\), and go to \(\mathrm{anm}\). At \(\mathrm{anm}\): move the bit block of \(T\) onto \(F\), then go to \(\mathrm{aw}(\mathrm{false})\). At \(\mathrm{aw}(f)\): go to \(\mathrm{ab}(f)\) if \(V\) is empty and to \(\mathrm{ac}(f)\) otherwise. At \(\mathrm{ac}(f)\): compare \(F\) with \(V\), then go to \(\mathrm{ar1}(\mathrm{true})\) if equal and to \(\mathrm{ar1}(f)\) if different. At \(\mathrm{ar1}(f)\), \(\mathrm{ar2}(f)\), \(\mathrm{amv}(f)\) in turn: move the bit block of \(X\) onto \(F\), of \(Y\) onto \(V\), and of \(V\) onto \(W\), then go to \(\mathrm{asep}(f)\). At \(\mathrm{asep}(f)\): pop \(V\), push \(\mathrm{cl}\) on \(W\) and go to \(\mathrm{aw}(f)\). At \(\mathrm{ab}(f)\): if \(W\) is empty, go to \(\mathrm{a0}\) if \(f\) is true, and otherwise push \(\mathrm{cl}\) on \(V\) and go to \(\mathrm{ad2}\); if the top of \(W\) is \(\mathrm{cl}\), pop it and push \(\mathrm{cl}\) on \(V\); otherwise pop it and push \(\mathrm{bit}(s)\) on \(V\), where \(s\) is true exactly when the popped symbol is \(\mathrm{bit}(\mathrm{true})\); in these last two cases go to \(\mathrm{ab}(f)\). At \(\mathrm{ad2}\): move the bit block of \(F\) onto \(X\) and go to \(\mathrm{ad3}\). At \(\mathrm{ad3}\): if the top of \(X\) is a name bit, pop it, push it on \(F\) and on \(V\) and go to \(\mathrm{ad3}\); otherwise go to \(\mathrm{a0}\).

Diamonds. At \(\mathrm{b0}\), \(\mathrm{b1}\) in turn: drain \(C\) pushing on \(P\) and \(Z\), then drain \(Z\) pushing on \(C\), then go to \(\mathrm{h0}\). At \(\mathrm{h0}\): go to \(\mathrm{z0}\) if \(V\) is empty and to \(\mathrm{h1}\) otherwise. At \(\mathrm{h1}, \dots, \mathrm{h5}\) in turn: drain \(P\) pushing on \(N\) and \(Z\), drain \(Z\) pushing on \(P\), drain \(M\) pushing on \(N\) and \(Z\), drain \(Z\) pushing on \(M\), and push \(\mathrm{cl}\) on \(N\), then go to \(\mathrm{cpA}(f_{1u}, \mathrm{false})\). At \(\mathrm{r0}\), \(\mathrm{r1}\), \(\mathrm{r2}\) in turn: drain \(P\) pushing on \(R\) and \(Z\), drain \(Z\) pushing on \(P\), and push \(\mathrm{cl}\) on \(R\), then go to \(\mathrm{r3}\). At \(\mathrm{r3}\): if \(M\) is empty go to \(\mathrm{r4}\), and otherwise pop it, push \(\mathrm{cl}\) on \(L\) and go to \(\mathrm{cpA}(w_{1u}, \mathrm{false})\). At \(\mathrm{r4}\): drain \(L\) pushing on \(M\) and go to \(\mathrm{e0}\). At \(\mathrm{wi}\): push \(\mathrm{cl}\) on \(R\) and go to \(\mathrm{r3}\). At \(\mathrm{e0}\), \(\mathrm{e1}\), \(\mathrm{e2}\) in turn: drain \(P\) pushing on \(D\) and \(Z\), drain \(Z\) pushing on \(P\), and push \(\mathrm{cl}\) twice on \(D\), then go to \(\mathrm{dw}(\mathrm{false}, \mathrm{false})\).

Detours. At \(\mathrm{dw}(p_p, p_n)\): if \(F\) is empty go to \(\mathrm{t0}\); if its top is \(\mathrm{cl}\), go to \(\mathrm{cpA}(d_{1u}, p_n)\) if \(p_p\) is true, else to \(\mathrm{cpA}(d_{3u}, \mathrm{false})\) if \(p_n\) is true, else to \(\mathrm{dj}\); otherwise go to \(\mathrm{dk}(p_p, p_n)\). At \(\mathrm{dk}(p_p, p_n)\): compare \(F\) with \(V\), then go to \(\mathrm{dr1}(p_p, p_n, \mathrm{true})\) if equal and to \(\mathrm{dr1}(p_p, p_n, \mathrm{false})\) if different. At \(\mathrm{dr1}\), \(\mathrm{dr2}\), \(\mathrm{dm}\) with parameters \((p_p, p_n, b)\) in turn: move the bit block of \(X\) onto \(F\), of \(Y\) onto \(V\), and of \(F\) onto \(T\), then go to \(\mathrm{dl}(p_p, p_n, b)\). At \(\mathrm{dl}(p_p, p_n, b)\): pop \(F\), push \(\mathrm{lit}(s)\) on \(T\), where \(s\) is true exactly when the popped symbol is \(\mathrm{lit}(\mathrm{true})\), and go to \(\mathrm{dw}(p_p \lor (b \land s), p_n \lor (b \land \lnot s))\). At \(\mathrm{dj}\): pop \(F\), push \(\mathrm{cl}\) once on \(T\), once on \(J\) and three times on \(D\), and go to \(\mathrm{dw}(\mathrm{false}, \mathrm{false})\). At \(\mathrm{t0}\): if \(T\) is empty go to \(\mathrm{t1}\); otherwise pop it, push on \(F\) the symbol \(\mathrm{cl}\) if the popped symbol is \(\mathrm{cl}\), \(\mathrm{bit}(b)\) if it is \(\mathrm{bit}(b)\), and otherwise \(\mathrm{lit}(s)\) with \(s\) true exactly when it is \(\mathrm{lit}(\mathrm{true})\), and go to \(\mathrm{t0}\). At \(\mathrm{t1}, \dots, \mathrm{t8}\) in turn: move the bit block of \(V\) onto \(G\), pop \(V\), drain \(P\) pushing nothing, drain \(N\) pushing on \(P\), push \(\mathrm{cl}\) on \(P\), and drain \(R\), \(J\) and \(D\) pushing nothing, then go to \(\mathrm{h0}\).

Output. At \(\mathrm{z0}\): move the bit block of \(Q\) onto \(O\) and go to \(\mathrm{z1}\). At \(\mathrm{z1}, \dots, \mathrm{z9}\) in turn: push false and then true on \(O\); drain \(P\) pushing true on \(O\) and \(\mathrm{cl}\) on \(Z\); drain \(Z\) pushing on \(P\); push false on \(O\); drain \(P\) pushing true on \(O\) and \(\mathrm{cl}\) on \(Z\); drain \(Z\) pushing on \(P\); push false on \(O\); drain \(C\) pushing true on \(O\) and \(\mathrm{cl}\) on \(Z\); and drain \(Z\) pushing on \(C\); then go to \(\mathrm{done}\). At \(\mathrm{done}\): halt.

Copy sites. For a copy site \(j\) and a bit \(b\): at \(\mathrm{cpA}(j, b)\), drain the stack of the counter that \(j\) reads, pushing \(\mathrm{bit}(\mathrm{true})\) on \(Q\) and \(\mathrm{cl}\) on \(Z\), and go to \(\mathrm{cpB}(j, b)\); at \(\mathrm{cpB}(j, b)\), drain \(Z\) pushing \(\mathrm{cl}\) on the stack of the counter that \(j\) reads, and go to \(\mathrm{post}(j, b)\); at \(\mathrm{post}(j, b)\), in one step push on \(Q\) one \(\mathrm{bit}(\mathrm{true})\) for each of the ones that \(j\) adds to its counter and then \(\mathrm{bit}(\mathrm{false})\), and go to the label that follows \(j\) for \(b\).

Cslib.Complexity.Karp.EmitHam.prog · 87 lines

def prog : Lab → TM2.Stmt Γ Lab Bool
  | .a0 => .peek .T (fun _ o => o.isNone) <| .branch id (.goto fun _ => .b0) <|
      .peek .T (fun _ o => o == some .cl) <| .branch id
        (.pop .T (fun s _ => s) <| .push .F (fun _ => Sym.cl) <| .push .C (fun _ => Sym.cl) <|
          pushList .M [Sym.cl, Sym.cl, Sym.cl] <| .goto fun _ => .a0)
        (.pop .T (fun _ o => o == some (.lit true)) <| .push .F (fun s => Sym.lit s) <|
          .goto fun _ => .anm)
  | .anm => moveB .T .F Sym.bit? Sym.bit .anm (.aw false)
  | .aw f => .peek .V (fun _ o => o.isNone) <| .branch id (.goto fun _ => .ab f)
      (.goto fun _ => .ac f)
  | .ac f => cmpB .F .V .X .Y Sym.bit? Sym.bit? Sym.bit Sym.bit (.ac f) (.ar1 true) (.ar1 f)
  | .ar1 f => moveB .X .F Sym.bit? Sym.bit (.ar1 f) (.ar2 f)
  | .ar2 f => moveB .Y .V Sym.bit? Sym.bit (.ar2 f) (.amv f)
  | .amv f => moveB .V .W Sym.bit? Sym.bit (.amv f) (.asep f)
  | .asep f => .pop .V (fun s _ => s) <| .push .W (fun _ => Sym.cl) <| .goto fun _ => .aw f
  | .ab f => .peek .W (fun _ o => o.isNone) <| .branch id
      (if f then .goto fun _ => .a0 else .push .V (fun _ => Sym.cl) <| .goto fun _ => .ad2) <|
      .peek .W (fun _ o => o == some .cl) <| .branch id
        (.pop .W (fun s _ => s) <| .push .V (fun _ => Sym.cl) <| .goto fun _ => .ab f)
        (.pop .W (fun _ o => o == some (.bit true)) <| .push .V (fun s => Sym.bit s) <|
          .goto fun _ => .ab f)
  | .ad2 => moveB .F .X Sym.bit? Sym.bit .ad2 .ad3
  | .ad3 => .peek .X (fun _ o => isBit Sym.bit? o) <| .branch id
      (.pop .X (fun _ o => bitOf Sym.bit? o) <| .push .F (fun s => Sym.bit s) <|
        .push .V (fun s => Sym.bit s) <| .goto fun _ => .ad3)
      (.goto fun _ => .a0)
  | .b0 => xfer .C [⟨.P, Sym.cl⟩, ⟨.Z, Sym.cl⟩] .b0 .b1
  | .b1 => xfer .Z [⟨.C, Sym.cl⟩] .b1 .h0
  | .h0 => .peek .V (fun _ o => o.isNone) <| .branch id (.goto fun _ => .z0)
      (.goto fun _ => .h1)
  | .h1 => xfer .P [⟨.N, Sym.cl⟩, ⟨.Z, Sym.cl⟩] .h1 .h2
  | .h2 => xfer .Z [⟨.P, Sym.cl⟩] .h2 .h3
  | .h3 => xfer .M [⟨.N, Sym.cl⟩, ⟨.Z, Sym.cl⟩] .h3 .h4
  | .h4 => xfer .Z [⟨.M, Sym.cl⟩] .h4 .h5
  | .h5 => .push .N (fun _ => Sym.cl) <| .goto fun _ => .cpA .f1u false
  | .r0 => xfer .P [⟨.R, Sym.cl⟩, ⟨.Z, Sym.cl⟩] .r0 .r1
  | .r1 => xfer .Z [⟨.P, Sym.cl⟩] .r1 .r2
  | .r2 => .push .R (fun _ => Sym.cl) <| .goto fun _ => .r3
  | .r3 => forHead .M .L Sym.cl (.cpA .w1u false) .r4
  | .r4 => xfer .L [⟨.M, Sym.cl⟩] .r4 .e0
  | .wi => .push .R (fun _ => Sym.cl) <| .goto fun _ => .r3
  | .e0 => xfer .P [⟨.D, Sym.cl⟩, ⟨.Z, Sym.cl⟩] .e0 .e1
  | .e1 => xfer .Z [⟨.P, Sym.cl⟩] .e1 .e2
  | .e2 => pushList .D [Sym.cl, Sym.cl] <| .goto fun _ => .dw false false
  | .dw pp pn => .peek .F (fun _ o => o.isNone) <| .branch id (.goto fun _ => .t0) <|
      .peek .F (fun _ o => o == some .cl) <| .branch id
        (.goto fun _ => clEnd pp pn) (.goto fun _ => .dk pp pn)
  | .dk pp pn => cmpB .F .V .X .Y Sym.bit? Sym.bit? Sym.bit Sym.bit (.dk pp pn)
      (.dr1 pp pn true) (.dr1 pp pn false)
  | .dr1 pp pn b => moveB .X .F Sym.bit? Sym.bit (.dr1 pp pn b) (.dr2 pp pn b)
  | .dr2 pp pn b => moveB .Y .V Sym.bit? Sym.bit (.dr2 pp pn b) (.dm pp pn b)
  | .dm pp pn b => moveB .F .T Sym.bit? Sym.bit (.dm pp pn b) (.dl pp pn b)
  | .dl pp pn b => .pop .F (fun _ o => o == some (.lit true)) <|
      .push .T (fun s => Sym.lit s) <| .goto fun s => .dw (pp || (b && s)) (pn || (b && !s))
  | .dj => .pop .F (fun s _ => s) <| .push .T (fun _ => Sym.cl) <|
      .push .J (fun _ => Sym.cl) <| pushList .D [Sym.cl, Sym.cl, Sym.cl] <|
        .goto fun _ => .dw false false
  | .t0 => .peek .T (fun _ o => o.isNone) <| .branch id (.goto fun _ => .t1) <|
      .peek .T (fun _ o => o == some .cl) <| .branch id
        (.pop .T (fun s _ => s) <| .push .F (fun _ => Sym.cl) <| .goto fun _ => .t0) <|
      .peek .T (fun _ o => isBit Sym.bit? o) <| .branch id
        (.pop .T (fun _ o => bitOf Sym.bit? o) <| .push .F (fun s => Sym.bit s) <|
          .goto fun _ => .t0)
        (.pop .T (fun _ o => o == some (.lit true)) <| .push .F (fun s => Sym.lit s) <|
          .goto fun _ => .t0)
  | .t1 => moveB .V .G Sym.bit? Sym.bit .t1 .t2
  | .t2 => .pop .V (fun s _ => s) <| .goto fun _ => .t3
  | .t3 => xfer .P [] .t3 .t4
  | .t4 => xfer .N [⟨.P, Sym.cl⟩] .t4 .t5
  | .t5 => .push .P (fun _ => Sym.cl) <| .goto fun _ => .t6
  | .t6 => xfer .R [] .t6 .t7
  | .t7 => xfer .J [] .t7 .t8
  | .t8 => xfer .D [] .t8 .h0
  | .z0 => moveB .Q .O Sym.bit? id .z0 .z1
  | .z1 => pushList .O [false, true] <| .goto fun _ => .z2
  | .z2 => xfer .P [⟨.O, true⟩, ⟨.Z, Sym.cl⟩] .z2 .z3
  | .z3 => xfer .Z [⟨.P, Sym.cl⟩] .z3 .z4
  | .z4 => .push .O (fun _ => false) <| .goto fun _ => .z5
  | .z5 => xfer .P [⟨.O, true⟩, ⟨.Z, Sym.cl⟩] .z5 .z6
  | .z6 => xfer .Z [⟨.P, Sym.cl⟩] .z6 .z7
  | .z7 => .push .O (fun _ => false) <| .goto fun _ => .z8
  | .z8 => xfer .C [⟨.O, true⟩, ⟨.Z, Sym.cl⟩] .z8 .z9
  | .z9 => xfer .Z [⟨.C, Sym.cl⟩] .z9 .done
  | .cpA j b => xfer j.src.k [⟨.Q, Sym.bit true⟩, ⟨.Z, Sym.cl⟩] (.cpA j b) (.cpB j b)
  | .cpB j b => xfer .Z [⟨j.src.k, j.src.unit⟩] (.cpB j b) (.post j b)
  | .post j b => emit .Q ((List.replicate j.ext true ++ [false]).map Sym.bit) (j.nxt b)
  | .done => .halt

Uses 21 · Used by 28

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Copy sites of the HAMPATH emitter · Extra ones of a copy site · Label after a HAMPATH copy site · Counter read by a copy site · Stack of a HAMPATH copy-site counter · Unit symbol of an emitter counter · End of a clause in the detour walk · Stack alphabets of the HAMPATH emitter · 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 · Bit-block comparison statement · Pushing a constant list · Loop head of a for loop over a counter · Bit test for the top of a stack · Bit-moving loop · Pushing a list of symbols onto one stack · Counter transfer loop

Used byHAMPATH emitter, phase A: moving the walk stack back onto the variable stack · HAMPATH emitter, phase A: copying a reversed name onto two stacks · HAMPATH emitter, phase A: searching the variable stack for a name · Running a chain of copy sites in the HAMPATH emitter · Comparing a name with the top entry of the variable stack · Copying a counter in the HAMPATH emitter · Run of a HAMPATH copy site · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One clause of the detour walk · Front of a diamond · One literal of the detour walk · The literals of a clause in the detour walk · Draining a counter · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · Moving the tokens back in the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · The diamonds · The row of a diamond in the HAMPATH emitter · The output phase of the HAMPATH emitter · Correctness and running time of the HAMPATH emitter · The HAMPATH emitter

DefinitionStart label of the HAMPATH emitter#✓fully proved

The emitter machine starts at the label \(a_0\), the first phase A label, which reads the next token.

def start : Lab := .a0

Uses 1 · Used by 2

Statement usesLabels of the HAMPATH emitter

Used byCorrectness and running time of the HAMPATH emitter · The HAMPATH emitter

StructureQuiescent states of the HAMPATH emitter#✓fully proved

A quiescent state consists of lists of token symbols \(t\), \(f\), \(v\), \(w\), \(g\), \(x\) (meant as the token stack, the tokens in reading order, the distinct variables, the other side of the variable walk, garbage, and the first comparison scratch stack), a list of bits \(o\) (the output stack), a list of bits \(q\) (the edge bits so far, in reading order), and natural numbers \(c\), \(c_3\), \(p\), \(n\), \(r\), \(l\), \(j\), \(d\) (meant as the clause count, three times it, the diamond top, the row end, the row vertex, the row loop index, the clause index and the detour vertex).

On the emitter's stacks such a state holds each counter as a unary stack of \(\mathrm{cl}\) symbols and the edge bits \(q\) on \(Q\) reversed, as name-bit symbols; the scratch stacks \(Y\) and \(Z\) are empty, and \(X\) is empty except while a new name is copied onto \(V\).

Cslib.Complexity.Karp.EmitHam.MS · 33 lines

structure MS where
  /-- The token stack. -/
  t : List Sym
  /-- The output stack. -/
  o : List Bool
  /-- The tokens in reading order. -/
  f : List Sym
  /-- The distinct variables. -/
  v : List Sym
  /-- The variable walk's other side. -/
  w : List Sym
  /-- The edge bits so far, in reading order. -/
  q : List Bool
  /-- Garbage. -/
  g : List Sym
  /-- The first comparison scratch stack. -/
  x : List Sym
  /-- The clause count. -/
  c : ℕ
  /-- Three times the clause count. -/
  mm : ℕ
  /-- The diamond top. -/
  p : ℕ
  /-- The row end. -/
  n : ℕ
  /-- The row vertex. -/
  r : ℕ
  /-- The row loop index. -/
  l : ℕ
  /-- The clause index. -/
  j : ℕ
  /-- The detour vertex. -/
  d : ℕ

Uses 1 · Used by 31

Statement usesStack alphabet of the SAT verifier

Used byHAMPATH emitter, phase A: moving the walk stack back onto the variable stack · HAMPATH emitter, phase A: copying a reversed name onto two stacks · Bits pushed by a copy site of the HAMPATH emitter · HAMPATH emitter, phase A: searching the variable stack for a name · Step count of a list of copy sites in the HAMPATH emitter · Running a chain of copy sites in the HAMPATH emitter · Comparing a name with the top entry of the variable stack · Run of a HAMPATH copy site · Stacks of a quiescent emitter state · Counter values of a quiescent emitter state · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One clause of the detour walk · Front of a diamond · The emitter state before the diamonds · One literal of the detour walk · The literals of a clause in the detour walk · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · Initial state of the HAMPATH emitter · Phase A of the HAMPATH emitter · Moving the tokens back in the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · The diamonds · The row of a diamond in the HAMPATH emitter · The output phase of the HAMPATH emitter · Correctness and running time of the HAMPATH emitter

DefinitionStacks of a quiescent emitter state#✓fully proved

In a quiescent state \(s\), the stacks \(T\), \(O\), \(F\), \(V\), \(W\), \(G\) and \(X\) hold the lists that \(s\) records for them; the stack \(Q\) holds the edge bits of \(s\) as bit symbols, reversed so that the last bit is on top; each counter stack \(C\), \(M\), \(P\), \(N\), \(R\), \(L\), \(J\), \(D\) holds as many copies of the symbol \(\mathrm{cl}\) as the value that \(s\) records for the corresponding counter (the clause count, the counter reserved for three times the clause count, the diamond top, the row end, the row vertex, the row loop index, the clause index and the detour vertex), with no relation imposed between these values; and the scratch stacks \(Y\) and \(Z\) are empty.

Cslib.Complexity.Karp.EmitHam.MS.stk · 18 lines

def MS.stk (s : MS) : ∀ k, List (Γ k)
  | .T => s.t
  | .O => s.o
  | .F => s.f
  | .V => s.v
  | .W => s.w
  | .Q => s.q.reverse.map Sym.bit
  | .G => s.g
  | .C => cnt Sym.cl s.c
  | .M => cnt Sym.cl s.mm
  | .P => cnt Sym.cl s.p
  | .N => cnt Sym.cl s.n
  | .R => cnt Sym.cl s.r
  | .L => cnt Sym.cl s.l
  | .J => cnt Sym.cl s.j
  | .D => cnt Sym.cl s.d
  | .X => s.x
  | .Y | .Z => []

Uses 5 · Used by 25

Statement usesStacks of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Unary counter

Used byHAMPATH emitter, phase A: moving the walk stack back onto the variable stack · HAMPATH emitter, phase A: copying a reversed name onto two stacks · HAMPATH emitter, phase A: searching the variable stack for a name · Running a chain of copy sites in the HAMPATH emitter · Comparing a name with the top entry of the variable stack · Run of a HAMPATH copy site · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One clause of the detour walk · Front of a diamond · One literal of the detour walk · The literals of a clause in the detour walk · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · Moving the tokens back in the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · The diamonds · The row of a diamond in the HAMPATH emitter · The output phase of the HAMPATH emitter · Correctness and running time of the HAMPATH emitter

DefinitionCounter values of a quiescent emitter state#✓fully proved

For a quiescent state \(s\), the value of the counters \(p\), \(n\), \(r\), \(j\), \(d\) is respectively the diamond top, the row end, the row vertex, the clause index and the detour vertex recorded in \(s\).

def MS.val (s : MS) : Src → ℕ
  | .p => s.p
  | .n => s.n
  | .r => s.r
  | .j => s.j
  | .d => s.d

Uses 2 · Used by 8

Statement usesQuiescent states of the HAMPATH emitter · Counters read by HAMPATH copy sites

Used byBits pushed by a copy site of the HAMPATH emitter · Step count of a list of copy sites in the HAMPATH emitter · Running a chain of copy sites in the HAMPATH emitter · Run of a HAMPATH copy site · One clause of the detour walk · Front of a diamond · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter

TheoremCopying a counter in the HAMPATH emitter#✓fully proved

Let \(a\), \(c\) and \(Z\) be three distinct stacks of the emitter machine (with \(Z\) its copy scratch stack), \(u\) a symbol of \(a\) and \(x\) a symbol of \(c\). Suppose the machine at label \(l_1\) pops \(a\) until it is empty, pushing \(x\) onto \(c\) and the clause separator \(\mathrm{cl}\) onto \(Z\) for each popped symbol, and then continues at \(l_2\); and at \(l_2\) pops \(Z\) until it is empty, pushing \(u\) onto \(a\) for each popped symbol, and then continues at \(l'\). If the stacks \(S\) hold exactly \(n\) copies of \(u\) on \(a\) and nothing on \(Z\), then for every flag \(v\) there is a flag \(v'\) such that the machine goes in exactly \(2n + 2\) steps from label \(l_1\) with flag \(v\) and stacks \(S\) to label \(l'\) with flag \(v'\) and the stacks \(S\) with \(n\) copies of \(x\) pushed onto \(c\).

theorem cp_run {a c : K} (ua : Γ a) (x : Γ c) (hca : c ≠ a) (haZ : a ≠ .Z) (hcZ : c ≠ .Z)
    {l₁ l₂ next : Lab} (h₁ : prog l₁ = xfer a [⟨c, x⟩, ⟨.Z, Sym.cl⟩] l₁ l₂)
    (h₂ : prog l₂ = xfer .Z [⟨a, ua⟩] l₂ next) (val : ℕ) (v : Bool) (S : ∀ k, List (Γ k))
    (hS : S a = cnt ua val) (hZ : S .Z = []) :
    ∃ v', Run prog (2 * val + 2) ⟨some l₁, v, S⟩
      ⟨some next, v', update S c (cnt x val ++ S c)⟩

Uses 11 · Used by 6

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · 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 usesAdding units to target stacks · Running a counter transfer

Used byRun of a HAMPATH copy site · Front of a diamond · Phase A of the HAMPATH emitter · The detours of a diamond · The row of a diamond in the HAMPATH emitter · The output phase of the HAMPATH emitter

DefinitionBits pushed by a copy site of the HAMPATH emitter#✓fully proved

For a quiescent state \(s\) of the HAMPATH emitter and a copy site \(j\), the atom of \(j\) in \(s\) is the list of \(c + e\) copies of true followed by one false, where \(c\) is the value in \(s\) of the counter that \(j\) copies and \(e \in \{0, 1\}\) is the number of extra ones that \(j\) adds.

def atom (s : MS) (j : Site) : List Bool := List.replicate (s.val j.src + j.ext) true ++ [false]

Uses 5 · Used by 5

Statement usesQuiescent states of the HAMPATH emitter · Counter values of a quiescent emitter state · Copy sites of the HAMPATH emitter · Extra ones of a copy site · Counter read by a copy site

Used byRunning a chain of copy sites in the HAMPATH emitter · Run of a HAMPATH copy site · One clause of the detour walk · Front of a diamond · The row loop of a diamond in the HAMPATH emitter

TheoremRun of a HAMPATH copy site#✓fully proved

Let \(j\) be a copy site, \(b\) and \(v\) bits and \(s\) a quiescent state of the HAMPATH emitter; let \(c\) be the value in \(s\) of the counter that \(j\) reads and \(e\) the number of ones that \(j\) adds to its counter. Started at label \(\mathrm{cpA}(j, b)\) with internal state \(v\) and the stacks of \(s\), the emitter runs in exactly \(2c + 3\) steps to the label that follows \(j\) for \(b\), with some internal state and the stacks of the quiescent state obtained from \(s\) by appending \(c + e\) copies of true followed by one false to its edge bits.

theorem site_run (j : Site) (b : Bool) (s : MS) (v : Bool) :
    ∃ v', Run prog (2 * s.val j.src + 3) ⟨some (.cpA j b), v, s.stk⟩
      ⟨some (j.nxt b), v', {s with q := s.q ++ atom s j}.stk⟩

Uses 22 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Counter values of a quiescent emitter state · Copy sites of the HAMPATH emitter · Label after a HAMPATH copy site · Counter read by a copy site · Bits pushed by a copy site of the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesExtra ones of a copy site · Counters read by HAMPATH copy sites · Stack of a HAMPATH copy-site counter · Unit symbol of an emitter counter · Copying a counter in the HAMPATH emitter · A single step executes the statement at the current label · Unary counter · Pushing a constant list · Pushing a list of symbols onto one stack

Used byRunning a chain of copy sites in the HAMPATH emitter

DefinitionCopy sites chained in the HAMPATH emitter#✓fully proved

Copy sites \(j_1, \dots, j_n\) are chained from label \(l_0\) to label \(l\) with passed bit \(b\) when \(l_0\) is the label at which \(j_1\) starts with passed bit \(b\), the label where each \(j_i\) with \(i < n\) continues with passed bit \(b\) is the label at which \(j_{i+1}\) starts with passed bit \(b\), and \(j_n\) continues at \(l\) with passed bit \(b\). The empty list of sites is chained from \(l_0\) to \(l\) exactly when \(l_0 = l\).

def Chain : List Site → Bool → Lab → Lab → Bool
  | [], _, l₀, l => l₀ == l
  | j :: js, b, l₀, l => l₀ == .cpA j b && Chain js b (j.nxt b) l

Uses 3 · Used by 4

Statement usesLabels of the HAMPATH emitter · Copy sites of the HAMPATH emitter · Label after a HAMPATH copy site

Used byRunning a chain of copy sites in the HAMPATH emitter · One clause of the detour walk · Front of a diamond · The row loop of a diamond in the HAMPATH emitter

DefinitionStep count of a list of copy sites in the HAMPATH emitter#✓fully proved

For a quiescent state \(s\) and copy sites \(j_1, \dots, j_n\), the step count is \(\sum_{i=1}^{n} (2 v_i + 3)\), where \(v_i\) is the value in \(s\) of the counter that \(j_i\) copies.

def chainCost (s : MS) (js : List Site) : ℕ := (js.map fun j => 2 * s.val j.src + 3).sum

Uses 4 · Used by 4

Statement usesQuiescent states of the HAMPATH emitter · Counter values of a quiescent emitter state · Copy sites of the HAMPATH emitter · Counter read by a copy site

Used byRunning a chain of copy sites in the HAMPATH emitter · One clause of the detour walk · Front of a diamond · The row loop of a diamond in the HAMPATH emitter

TheoremRunning a chain of copy sites in the HAMPATH emitter#✓fully proved

Let \(j_1, \dots, j_n\) be copy sites chained from label \(l_0\) to label \(l\) with passed bit \(b\). Then for every quiescent state \(s\) and every flag \(v\) there is a flag \(v'\) such that the emitter machine goes, in exactly as many steps as the step count of \(j_1, \dots, j_n\) at \(s\), from label \(l_0\) with flag \(v\) and the stacks of \(s\) to label \(l\) with flag \(v'\) and the stacks of the state that differs from \(s\) only in that the atoms of \(j_1, \dots, j_n\) at \(s\), concatenated in this order, are appended to its edge bits.

theorem chain_run (js : List Site) : ∀ (s : MS) (b : Bool) (l₀ l : Lab),
    Chain js b l₀ l = true → ∀ v : Bool, ∃ v', Run prog (chainCost s js) ⟨some l₀, v, s.stk⟩
      ⟨some l, v', {s with q := s.q ++ (js.map (atom s)).flatten}.stk⟩

Uses 18 · Used by 3

Statement usesCopy sites chained in the HAMPATH emitter · Stacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Copy sites of the HAMPATH emitter · Bits pushed by a copy site of the HAMPATH emitter · Step count of a list of copy sites in the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesCounter values of a quiescent emitter state · Extra ones of a copy site · Label after a HAMPATH copy site · Counter read by a copy site · Counters read by HAMPATH copy sites · Run of a HAMPATH copy site

Used byOne clause of the detour walk · Front of a diamond · The row loop of a diamond in the HAMPATH emitter

TheoremA symbol that reads as a name bit is that bit#✓fully proved

For every symbol \(x\) of the stack alphabet of the SAT verifier and every bit \(b\), if \(x\) reads as the name bit \(b\), then \(x\) is the name-bit symbol for \(b\).

theorem bit_inv (x : Sym) (b : Bool) (h : Sym.bit? x = some b) : Sym.bit b = x

Uses 2 · Used by 1

Statement usesStack alphabet of the SAT verifier · Reading a symbol as a name bit

Used byComparing a name with the top entry of the variable stack

TheoremComparing a name with the top entry of the variable stack#✓fully proved

Let \(l_c\) be a label at which the emitter machine compares the bit blocks of the stacks \(F\) and \(V\), with scratch stacks \(X\) and \(Y\), going to \(r_1(b_T)\) if the blocks are equal and to \(r_1(b_F)\) otherwise. Suppose that for each bit \(b\) the machine at \(r_1(b)\) moves the bit block of \(X\) onto \(F\) and then continues at \(r_2(b)\), and at \(r_2(b)\) moves the bit block of \(Y\) onto \(V\) and then continues at \(n_x(b)\). Let \(s\) be a quiescent state whose stack \(F\) holds the bit symbols of a bit list \(u\) followed by a list \(A\), whose stack \(V\) holds the bit symbols of a bit list \(w\) followed by a list \(B\), where neither \(A\) nor \(B\) starts with a bit symbol, and whose stack \(X\) is empty. Then for every flag \(v\) there is a flag \(v'\) such that the machine goes in at most \(3 |w| + 3\) steps from label \(l_c\) with flag \(v\) and the stacks of \(s\) to label \(n_x(b_T)\) if \(u = w\) and to \(n_x(b_F)\) otherwise, with flag \(v'\) and again the stacks of \(s\).

theorem cmpR_run {lc : Lab} {r1 r2 nx : Bool → Lab} {bT bF : Bool}
    (hc : prog lc = cmpB .F .V .X .Y Sym.bit? Sym.bit? Sym.bit Sym.bit lc (r1 bT) (r1 bF))
    (h1 : ∀ b, prog (r1 b) = moveB .X .F Sym.bit? Sym.bit (r1 b) (r2 b))
    (h2 : ∀ b, prog (r2 b) = moveB .Y .V Sym.bit? Sym.bit (r2 b) (nx b))
    (s : MS) (v : Bool) (u w : List Bool) (A B : List Sym) (hA : A.head?.bind Sym.bit? = none)
    (hB : B.head?.bind Sym.bit? = none) (hf : s.f = u.map Sym.bit ++ A)
    (hv : s.v = w.map Sym.bit ++ B) (hx : s.x = []) :
    ∃ v', RunLe prog (3 * w.length + 3) ⟨some lc, v, s.stk⟩
      ⟨some (nx (if u = w then bT else bF)), v', s.stk⟩

Uses 18 · Used by 2

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Flag bit of a machine state · Runs within a step budget · Bit-block comparison statement · Bit-moving loop

Proof usesA symbol that reads as a name bit is that bit · Four pairwise distinct stacks · Bit blocks · Exact-length runs of a TM2 machine · Correctness of the bit-block comparison · Restoring a stack after a comparison

Used byHAMPATH emitter, phase A: searching the variable stack for a name · One literal of the detour walk

AbbreviationName of a variable in the HAMPATH emitter#✓fully proved

The name of a variable \(x \in \mathbb{N}\) is the list of name-bit symbols \(\mathrm{bit}(b_0), \dots, \mathrm{bit}(b_{k-1})\), where \(b_0 \cdots b_{k-1}\) is the binary encoding of \(x\), least significant bit first (the empty list for \(x = 0\)).

abbrev name (x : ℕ) : List Sym := (encodeNat x).map Sym.bit

Uses 1 · Used by 14

Statement usesStack alphabet of the SAT verifier

Used byHAMPATH emitter, phase A: searching the variable stack for a name · Variable stack of the HAMPATH emitter · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One clause of the detour walk · One literal of the detour walk · The literals of a clause in the detour walk · The detour walk of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · The diamonds

DefinitionVariable stack of the HAMPATH emitter#✓fully proved

For a list \(x_1, \dots, x_k\) of variables (natural numbers), the variable stack is the list of symbols obtained by concatenating, for \(i = 1, \dots, k\) in order, the name bits of \(x_i\) followed by the separator symbol \(\mathrm{cl}\). With the head of the list on top, \(x_1\) is the top entry and each name sits above its separator.

def vstk (vs : List ℕ) : List Sym := vs.flatMap fun x => name x ++ [Sym.cl]

Uses 2 · Used by 9

Statement usesName of a variable in the HAMPATH emitter · Stack alphabet of the SAT verifier

Used byHAMPATH emitter, phase A: searching the variable stack for a name · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · The emitter state before the diamonds · Phase A of the HAMPATH emitter · One diamond · The diamonds

DefinitionVariable-stack symbols of the HAMPATH emitter#✓fully proved

A token symbol is a variable-stack symbol when it is a name bit \(\mathrm{bit}(b)\) for some bit \(b\) or the separator \(\mathrm{cl}\); the polarity markers, the value markers and the dead marker are not.

def isVS : Sym → Bool
  | .bit _ | .cl => true
  | _ => false

Uses 1 · Used by 2

Statement usesStack alphabet of the SAT verifier

Used byHAMPATH emitter, phase A: moving the walk stack back onto the variable stack · HAMPATH emitter, phase A: one literal

TheoremHAMPATH emitter, phase A: moving the walk stack back onto the variable stack#✓fully proved

Let \(f\) be a Boolean, let \(L\) be a list of symbols each of which is a name bit or the separator \(\mathrm{cl}\), and let \(s\) be a quiescent state of the HAMPATH emitter whose stack \(W\) is \(L\). Then for every value \(v\) of the machine's Boolean variable there is a value \(v'\) such that the emitter goes in exactly \(|L|\) steps from label \(\mathrm{ab}(f)\), variable \(v\) and the stacks of \(s\) to label \(\mathrm{ab}(f)\), variable \(v'\) and the stacks of the state obtained from \(s\) by emptying \(W\) and replacing \(V\) by the reverse of \(L\) followed by the old contents of \(V\).

theorem ab_run (f : Bool) : ∀ (L : List Sym), (∀ x ∈ L, isVS x = true) → ∀ (s : MS) (v : Bool),
    s.w = L → ∃ v', Run prog L.length ⟨some (.ab f), v, s.stk⟩
      ⟨some (.ab f), v', {s with w := [], v := L.reverse ++ s.v}.stk⟩

Uses 10 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Variable-stack symbols of the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · 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 byHAMPATH emitter, phase A: one literal

TheoremHAMPATH emitter, phase A: searching the variable stack for a name#✓fully proved

For \(y \in \mathbb{N}\) write \(\mathrm{name}(y)\) for the canonical binary encoding of \(y\) as name-bit symbols, and for a list \(\mathit{vs}\) of naturals write \(\mathrm{vstk}(\mathit{vs})\) for the variable stack: the names of the entries of \(\mathit{vs}\), each followed by the separator \(\mathrm{cl}\). Let \(x \in \mathbb{N}\) and let \(A\) be a list of symbols that is empty or does not start with a name bit. Then for every list \(\mathit{vs}\) of naturals, every Boolean \(f\), every quiescent state \(s\) of the HAMPATH emitter whose stack \(F\) is \(\mathrm{name}(x)\) followed by \(A\), whose stack \(V\) is \(\mathrm{vstk}(\mathit{vs})\) and whose stack \(X\) is empty, and every value \(v\) of the machine's Boolean variable, writing \(g\) for the Boolean that is true exactly when \(f\) is true or \(x\) occurs in \(\mathit{vs}\), there is a value \(v'\) such that the emitter goes in at most \(6|\mathrm{vstk}(\mathit{vs})| + 1\) steps from label \(\mathrm{aw}(f)\), variable \(v\) and the stacks of \(s\) to label \(\mathrm{ab}(g)\), variable \(v'\) and the stacks of the state obtained from \(s\) by emptying \(V\) and replacing \(W\) by the reverse of \(\mathrm{vstk}(\mathit{vs})\) followed by the old contents of \(W\).

theorem aw_run (x : ℕ) (A : List Sym) (hA : A.head?.bind Sym.bit? = none) :
    ∀ (vs : List ℕ) (f : Bool) (s : MS) (v : Bool), s.f = name x ++ A → s.v = vstk vs →
      s.x = [] →
      ∃ v', RunLe prog (6 * (vstk vs).length + 1) ⟨some (.aw f), v, s.stk⟩
        ⟨some (.ab (f || decide (x ∈ vs))), v',
          {s with v := [], w := (vstk vs).reverse ++ s.w}.stk⟩

Uses 18 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Name of a variable in the HAMPATH emitter · The HAMPATH emitter machine · Variable stack of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Runs within a step budget

Proof usesComparing a name with the top entry of the variable stack · The binary code of natural numbers is injective · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Running the bit-moving loop

Used byHAMPATH emitter, phase A: one literal

TheoremHAMPATH emitter, phase A: copying a reversed name onto two stacks#✓fully proved

Let \(u\) be a list of bits and let \(s\) be a quiescent state of the HAMPATH emitter whose stack \(X\) holds \(u\) as name-bit symbols. Then for every value \(v\) of the machine's Boolean variable there is a value \(v'\) such that the emitter goes in exactly \(|u| + 1\) steps from label \(\mathrm{ad3}\), variable \(v\) and the stacks of \(s\) to label \(\mathrm{a0}\), variable \(v'\) and the stacks of the state obtained from \(s\) by emptying \(X\) and replacing each of \(F\) and \(V\) by the reverse of \(u\) (as name-bit symbols) followed by its old contents.

theorem ad3_run : ∀ (u : List Bool) (s : MS) (v : Bool), s.x = u.map Sym.bit →
    ∃ v', Run prog (u.length + 1) ⟨some .ad3, v, s.stk⟩ ⟨some .a0, v',
      { s with
        x := [], f := (u.map Sym.bit).reverse ++ s.f, v := (u.map Sym.bit).reverse ++ s.v }.stk⟩

Uses 11 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesReading a symbol as a name bit · A single step executes the statement at the current label · Bit on top of a stack

Used byHAMPATH emitter, phase A: one literal

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.