Phase-0 labels of the SAT verifier host to Program of the SAT verifier host

InductivePhase-0 labels of the SAT verifier host#✓fully proved

The five labels of phase 0 of the SAT verifier host: \(m_1\) and \(m_2\) move the formula bits \(x\) off the input (in two passes), \(\mathsf{sep}\) drops the separator, and \(m_3\) and \(m_4\) move the witness bits \(w\) (in two passes).

inductive P0 | m1 | m2 | sep | m3 | m4
  deriving DecidableEq

Used by 8

Used byHost labels as a sum type · Labels of the SAT verifier host · Program of the SAT verifier host · The tokenizer embeds in the SAT verifier host · Initial configuration of the SAT verifier machine · Phase 0 of the SAT verifier host · The SAT verifier machine · The TM2 SAT verifier

InductiveLabels of the SAT verifier host#✓fully proved

A label of the SAT verifier host is one of the following: a phase-0 label; a label of the tokenizer; a label of the 3-clause filter; a label of the clause-check driver or of the lookup embedded in it; a cleanup label carrying an answer bit; or an output label carrying an answer bit.

inductive HLab
  | ph (p : P0)
  | tok (l : Tokenizer.Lab)
  | flt (l : Karp.Filter3.Lab)
  | chk (l : Check.DLab ⊕ Lookup.Lab)
  | clean (ans : Bool)
  | fin (ans : Bool)
  deriving DecidableEq

Uses 5 · Used by 12

Statement usesLabels of the 3SAT clause-length filter · Driver labels of the clause check · Labels of the lookup machine · Phase-0 labels of the SAT verifier host · Labels of the SAT tokenizer

Used byDriver labels in the SAT host · Host labels as a sum type · Filter exits in the SAT verifier host · Program of the SAT verifier host · Tokenizer labels in the host machine · Cleanup of the SAT host · The tokenizer embeds in the SAT verifier host · Cleanup phase of the SAT verifier host · Initial configuration of the SAT verifier machine · Phase 0 of the SAT verifier host · The SAT verifier machine · The TM2 SAT verifier

DefinitionHost labels as a sum type#✓fully proved

Write \(P_0\) for the phase-0 labels, \(\Lambda_T\) for the tokenizer labels, \(\Lambda_F\) for the labels of the clause-length filter, and \(\Lambda_D\) and \(\Lambda_L\) for the labels of the clause-check driver and of the lookup. The host labels are in bijection with \(P_0 \sqcup \Lambda_T \sqcup \Lambda_F \sqcup (\Lambda_D \sqcup \Lambda_L) \sqcup \mathrm{Bool} \sqcup \mathrm{Bool}\): a phase-0 label \(p\), tokenizer label, filter label, or driver or lookup label goes to itself in its summand, a cleanup label with answer \(a\) goes to \(a\) in the first copy of \(\mathrm{Bool}\), and a final label with answer \(a\) goes to \(a\) in the second copy. The bijection gives the host labels their finiteness instance.

def HLab.equiv :
    HLab ≃ P0 ⊕ Tokenizer.Lab ⊕ Karp.Filter3.Lab ⊕ (Check.DLab ⊕ Lookup.Lab) ⊕ Bool ⊕ Bool where
  toFun
    | .ph p => .inl p | .tok l => .inr (.inl l) | .flt l => .inr (.inr (.inl l))
    | .chk l => .inr (.inr (.inr (.inl l))) | .clean a => .inr (.inr (.inr (.inr (.inl a))))
    | .fin a => .inr (.inr (.inr (.inr (.inr a))))
  invFun
    | .inl p => .ph p | .inr (.inl l) => .tok l | .inr (.inr (.inl l)) => .flt l
    | .inr (.inr (.inr (.inl l))) => .chk l | .inr (.inr (.inr (.inr (.inl a)))) => .clean a
    | .inr (.inr (.inr (.inr (.inr a)))) => .fin a
  left_inv x := by cases x <;> rfl
  right_inv x := by rcases x with p | l | l | l | a | a <;> rfl

Uses 6 · Used by 1

Statement usesLabels of the 3SAT clause-length filter · Driver labels of the clause check · Labels of the lookup machine · Labels of the SAT verifier host · Phase-0 labels of the SAT verifier host · Labels of the SAT tokenizer

Used byThe SAT verifier machine

DefinitionPlacement of the tokenizer's stacks in the host#✓fully proved

The stacks of the tokenizer (the formula bits \(X\), the witness bits \(W\), the token output \(T\), the table output \(B\), and the clause and literal counters \(CC\) and \(LC\)) are placed in the host machine by the map that sends each of them to the host stack of the same name.

def eT : Tokenizer.K → HK
  | .X => .X | .W => .W | .T => .T | .B => .B | .CC => .CC | .LC => .LC

Uses 2 · Used by 2

Statement usesStacks of the SAT verifier host · Stacks of the SAT tokenizer

Used byStack embedding of the tokenizer into the host · The TM2 SAT verifier

DefinitionStack embedding of the tokenizer into the host#✓fully proved

Every stack of the tokenizer has alphabet \(\mathrm{Sym}\). The tokenizer is embedded in the host machine by sending each of its stacks \(X\), \(W\), \(T\), \(B\), \(CC\), \(LC\) to the host stack of the same name (an injective map) and identifying the alphabet of each with that of its image, which is again \(\mathrm{Sym}\), by the identity.

def embT : SEmb (fun _ : Tokenizer.K => Sym) HΓ where
  e := eT
  inj a b h := by cases a <;> cases b <;> first | rfl | exact absurd h (by decide)
  ι k := match k with
    | .X => Equiv.refl Sym | .W => Equiv.refl Sym | .T => Equiv.refl Sym
    | .B => Equiv.refl Sym | .CC => Equiv.refl Sym | .LC => Equiv.refl Sym

Uses 6 · Used by 3

Statement usesStacks of the SAT verifier host · Stack alphabets of the SAT verifier host · Placement of the tokenizer's stacks in the host · Stack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Stack embedding

Used byProgram of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The TM2 SAT verifier

DefinitionPlacement of the lookup's stacks in the clause-check driver#✓fully proved

The stacks of the lookup (the query \(T\), the table \(B\), the stash \(S\), the scratch stacks \(A\) and \(C\), and the value \(V\)) are placed in the clause-check driver by the map that sends each of them to the driver stack of the same name.

def eL : Lookup.K → Check.K
  | .T => .T | .B => .B | .S => .S | .A => .A | .C => .C | .V => .V

Uses 2 · Used by 2

Statement usesStacks of the clause check · Stacks of the lookup machine

Used byStack embedding of the lookup into the clause-check driver · The embedded lookup meets the lookup contract

DefinitionStack embedding of the lookup into the clause-check driver#✓fully proved

Every stack of the lookup and of the clause-check driver has alphabet \(\mathrm{Sym}\). The lookup is embedded in the driver by sending each of its stacks \(T\), \(B\), \(S\), \(A\), \(C\), \(V\) to the driver stack of the same name (an injective map) and identifying the alphabets by the identity of \(\mathrm{Sym}\).

def embL : SEmb (fun _ : Lookup.K => Sym) (fun _ : Check.K => Sym) where
  e := eL
  inj a b h := by cases a <;> cases b <;> first | rfl | exact absurd h (by decide)
  ι _ := Equiv.refl Sym

Uses 5 · Used by 2

Statement usesStacks of the clause check · Stacks of the lookup machine · Placement of the lookup's stacks in the clause-check driver · Stack alphabet of the SAT verifier · Stack embedding

Used byThe embedded lookup program · The embedded lookup meets the lookup contract

DefinitionLookup labels in the clause-check driver#✓fully proved

The relabelling that places the lookup's labels among the driver's labels, whose label set consists of the driver's own labels together with the lookup's labels: the lookup's final label \(\mathsf{done}\) goes to the driver's return label \(\mathsf{ret}\), and every other lookup label \(l\) goes to the copy of \(l\) among the lookup's labels.

def φL (l : Lookup.Lab) : Check.DLab ⊕ Lookup.Lab := if l = .done then .inl .ret else .inr l

Uses 2 · Used by 2

Statement usesDriver labels of the clause check · Labels of the lookup machine

Used byThe embedded lookup program · The embedded lookup meets the lookup contract

DefinitionThe embedded lookup program#✓fully proved

The lookup sub-program of the clause-check driver: at each lookup label \(l\), it is the lookup program's statement at \(l\) with every stack operation moved to the driver's stack of the same name (the lookup's stacks \(T\), \(B\), \(S\), \(A\), \(C\), \(V\)) and every jump target relabelled by the lookup-label map, which sends \(\mathsf{done}\) to the driver's return label \(\mathsf{ret}\) and keeps every other label.

def lkH (l : Lookup.Lab) : Check.Stmt Lookup.Lab := mapS embL φL (Lookup.prog l)

Uses 10 · Used by 4

Statement usesDriver labels of the clause check · Stacks of the clause check · Clause-check statements · Stacks of the lookup machine · Labels of the lookup machine · The lookup program · Stack embedding of the lookup into the clause-check driver · Lookup labels in the clause-check driver · Stack alphabet of the SAT verifier · Translating a statement along a stack embedding

Used byProgram of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The embedded lookup meets the lookup contract · The TM2 SAT verifier

DefinitionDriver stacks in the SAT host#✓fully proved

The map from the stacks of the clause-check driver into the host stacks sends each driver stack to the host stack of the same name.

def eC : Check.K → HK
  | .T => .T | .B => .B | .S => .S | .A => .A | .C => .C | .V => .V | .P => .P | .F => .F

Uses 2 · Used by 1

Statement usesStacks of the clause check · Stacks of the SAT verifier host

Used byStack embedding of the clause-check driver into the host

DefinitionStack embedding of the clause-check driver into the host#✓fully proved

Every stack of the clause-check driver has alphabet \(\mathrm{Sym}\). The driver is embedded in the host machine by sending each of its stacks \(T\), \(B\), \(S\), \(A\), \(C\), \(V\), \(P\), \(F\) to the host stack of the same name (an injective map) and identifying the alphabet of each with that of its image, which is again \(\mathrm{Sym}\), by the identity.

def embC : SEmb (fun _ : Check.K => Sym) HΓ where
  e := eC
  inj a b h := by cases a <;> cases b <;> first | rfl | exact absurd h (by decide)
  ι k := match k with
    | .T => Equiv.refl Sym | .B => Equiv.refl Sym | .S => Equiv.refl Sym | .A => Equiv.refl Sym
    | .C => Equiv.refl Sym | .V => Equiv.refl Sym | .P => Equiv.refl Sym | .F => Equiv.refl Sym

Uses 6 · Used by 3

Statement usesStacks of the clause check · Stacks of the SAT verifier host · Stack alphabets of the SAT verifier host · Driver stacks in the SAT host · Stack alphabet of the SAT verifier · Stack embedding

Used byProgram of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The TM2 SAT verifier

DefinitionPlacement of the filter's stacks in the host#✓fully proved

The two stacks of the clause-length filter, the token stack \(T\) and the side stack \(U\), are placed in the host machine by the map that sends \(T\) to the host stack \(T\) and \(U\) to the host stack \(U\).

def eF : Karp.Filter3.K → HK
  | .T => .T | .U => .U

Uses 2 · Used by 2

Statement usesStacks of the 3SAT clause-length filter · Stacks of the SAT verifier host

Used byStack embedding of the clause-length filter into the host · The TM2 SAT verifier

DefinitionStack embedding of the clause-length filter into the host#✓fully proved

Both stacks of the clause-length filter have alphabet \(\mathrm{Sym}\). The filter is embedded in the host machine by sending its stacks \(T\) and \(U\) to the host stacks of the same names (an injective map) and identifying the alphabet of each with that of its image, which is again \(\mathrm{Sym}\), by the identity.

def embF : SEmb (fun _ : Karp.Filter3.K => Sym) HΓ where
  e := eF
  inj a b h := by cases a <;> cases b <;> first | rfl | exact absurd h (by decide)
  ι k := match k with | .T => Equiv.refl Sym | .U => Equiv.refl Sym

Uses 6 · Used by 3

Statement usesStacks of the 3SAT clause-length filter · Stacks of the SAT verifier host · Stack alphabets of the SAT verifier host · Placement of the filter's stacks in the host · Stack alphabet of the SAT verifier · Stack embedding

Used byProgram of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The TM2 SAT verifier

DefinitionFilter exits in the SAT verifier host#✓fully proved

The relabelling of the 3-clause filter's labels into the labels of the SAT verifier host sends the filter's exit label pass to the start label of the clause-check driver, its exit label fail to the cleanup label with answer false, and every other filter label \(l\) to the host's copy of \(l\) among its filter labels.

def φF : Karp.Filter3.Lab → HLab
  | .pass => .chk (.inl .start)
  | .fail => .clean false
  | l => .flt l

Uses 4 · Used by 3

Statement usesLabels of the 3SAT clause-length filter · Driver labels of the clause check · Labels of the lookup machine · Labels of the SAT verifier host

Used byProgram of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The TM2 SAT verifier

DefinitionTokenizer labels in the host machine#✓fully proved

The map from labels of the tokenizer to labels of the host SAT verifier sends the tokenizer's accepting label to the start label of the embedded clause-length filter, its rejecting label to the cleanup label with answer false, and every other label \(l\) to the host label that runs the tokenizer at \(l\).

def φT (l : Tokenizer.Lab) : HLab :=
  if l = .acc then .flt Karp.Filter3.start else if l = .rej then .clean false else .tok l

Uses 4 · Used by 3

Statement usesLabels of the 3SAT clause-length filter · Start label of the filter · Labels of the SAT verifier host · Labels of the SAT tokenizer

Used byProgram of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The TM2 SAT verifier

DefinitionDriver labels in the SAT host#✓fully proved

The map from the labels of the clause-check driver (its own labels and those of the lookup embedded in it) to the host labels sends the driver's label for the answer yes to the cleanup label with answer true, its label for the answer no to the cleanup label with answer false, and every other label \(l\) to the host label running the driver at \(l\).

def φC : Check.DLab ⊕ Lookup.Lab → HLab
  | .inl .yes => .clean true
  | .inl .no => .clean false
  | l => .chk l

Uses 3 · Used by 3

Statement usesDriver labels of the clause check · Labels of the lookup machine · Labels of the SAT verifier host

Used byProgram of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The TM2 SAT verifier

DefinitionReading a formula bit in the SAT host#✓fully proved

The input alphabet of the SAT host consists of the formula bits, the separator and the witness bits. This partial map sends a formula bit \(b\) to \(b\) and is undefined on the separator and on witness bits.

def dX : G → Option Bool
  | .inl b => some b
  | _ => none

Uses 1 · Used by 3

Statement usesInput alphabet of the SAT verifier host

Used byProgram of the SAT verifier host · The tokenizer embeds in the SAT verifier host · Phase 0 of the SAT verifier host

DefinitionReading a witness bit in the SAT host#✓fully proved

The input alphabet of the SAT host consists of the formula bits, the separator and the witness bits. This partial map sends a witness bit \(b\) to \(b\) and is undefined on formula bits and on the separator.

def dW : G → Option Bool
  | .inr (some b) => some b
  | _ => none

Uses 1 · Used by 3

Statement usesInput alphabet of the SAT verifier host

Used byProgram of the SAT verifier host · The tokenizer embeds in the SAT verifier host · Phase 0 of the SAT verifier host

DefinitionStacks emptied by the SAT verifier's cleanup#✓fully proved

The cleanup loop of the host SAT verifier empties the list of stacks made of the input stack followed by the work stacks \(X\), \(W\), \(T\), \(B\), \(S\), \(A\), \(C\), \(V\), \(P\), \(F\), \(CC\), \(LC\), \(X1\), \(W1\), \(U\), in that order: every host stack except the output stack.

def workKs : List HK := [.inp, .X, .W, .T, .B, .S, .A, .C, .V, .P, .F, .CC, .LC, .X1, .W1, .U]

Uses 1 · Used by 4

Statement usesStacks of the SAT verifier host

Used byProgram of the SAT verifier host · Cleanup of the SAT host · The tokenizer embeds in the SAT verifier host · The cleanup stacks are distinct

DefinitionProgram of the SAT verifier host#✓fully proved

For a value \(c\) of the 3SAT flag, the host program acts at each host label as follows. Here moving a bit block from one stack to another means repeatedly popping the top symbol of the first stack while it is a bit and pushing it, as a bit token, onto the second, and continuing at the next label once the top is not a bit or the stack is empty.

The phase-0 labels move the formula bits from the input stack onto a scratch stack, move them from there onto the formula stack, pop one symbol (on a pair encoding, the separator) from the input stack, move the certificate bits from the input stack onto a second scratch stack, and move them from there onto the certificate stack before going to the start label of the tokenizer. At a tokenizer label, a filter label or a driver label the host runs the program of the tokenizer, of the 3-clause filter with flag \(c\), or of the clause-check driver with its embedded lookup, on that component's stacks embedded in the host, with the component's labels renamed to host labels; the tokenizer's accept exit goes to the filter's start label, the filter's pass exit to the driver's start label, the driver's yes exit to the cleanup label with answer true, and the tokenizer's reject exit, the filter's fail exit and the driver's no exit to the cleanup label with answer false. At the cleanup label with answer \(b\) the host pops every stack other than the output stack once, repeats this while anything was popped, and then goes to the output label with answer \(b\), where it pushes \(b\) onto the output stack, sets its internal state to false and halts.

def hprog (cap : Bool) : HLab → TM2.Stmt HΓ HLab Bool
  | .ph .m1 => moveB (Γ := HΓ) HK.inp HK.X1 dX Sym.bit (.ph .m1) (.ph .m2)
  | .ph .m2 => moveB (Γ := HΓ) HK.X1 HK.X Sym.bit? Sym.bit (.ph .m2) (.ph .sep)
  | .ph .sep => .pop .inp (fun s _ => s) (.goto fun _ => .ph .m3)
  | .ph .m3 => moveB (Γ := HΓ) HK.inp HK.W1 dW Sym.bit (.ph .m3) (.ph .m4)
  | .ph .m4 => moveB (Γ := HΓ) HK.W1 HK.W Sym.bit? Sym.bit (.ph .m4) (.tok Tokenizer.start)
  | .tok l => mapS embT φT (Tokenizer.prog l)
  | .flt l => mapS embF φF (Karp.Filter3.prog cap l)
  | .chk l => mapS embC φC (Check.prog lkH Lookup.start l)
  | .clean ans => cleanS workKs (.clean ans) (.fin ans)
  | .fin ans => .push .out (fun _ => ans) (.load (fun _ => false) .halt)

Uses 32 · Used by 6

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Driver labels of the clause check · Stacks of the clause check · The clause-check driver with a lookup sub-program · Labels of the lookup machine · Start label of the lookup machine · Stacks of the SAT verifier host · Labels of the SAT verifier host · Stack alphabets of the SAT verifier host · Phase-0 labels of the SAT verifier host · Reading a witness bit in the SAT host · Reading a formula bit in the SAT host · Stack embedding of the clause-check driver into the host · Stack embedding of the clause-length filter into the host · Stack embedding of the tokenizer into the host · The embedded lookup program · Stacks emptied by the SAT verifier's cleanup · Driver labels in the SAT host · Filter exits in the SAT verifier host · Tokenizer labels in the host machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Start label of the SAT tokenizer · Translating a statement along a stack embedding · Flag bit of a machine state · Cleanup round · Bit-moving loop

Used byCleanup of the SAT host · The tokenizer embeds in the SAT verifier host · Cleanup phase of the SAT verifier host · Phase 0 of the SAT verifier host · The SAT verifier machine · The TM2 SAT verifier

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.