From the canonical pair encoding to the w # y form

13 fully proved

The canonical encoding of a pair of bit lists

DefinitionConverter encoding of the first component#✓fully proved

For a bit list \(x\), the bit list obtained by replacing every bit \(b\) of \(x\), in order, with the six bits true, true, true, \(b\), true, false.

def encFst (x : List Bool) : List Bool := x.flatMap fun b => [true, true, true, b, true, false]

Used by 5

Used byCanonical bit-list decoder · Run of the pair-to-canonical converter · Canonical encoding of a pair of bit lists · Polynomial-time conversion to the verifier's pair encoding · Full run of the pair-encoding converter

DefinitionConverter encoding of the second component#✓fully proved

For a bit list \(w\), the bit list obtained by replacing every bit \(b\) of \(w\), in order, with the three bits true, \(b\), false.

def encSnd (w : List Bool) : List Bool := w.flatMap fun b => [true, b, false]

Used by 7

Used byCanonical bit-list decoder · Polynomial-time decoder of the canonical bit-list encoding · Polynomial-time encoder to the canonical bit-list encoding · Run of the pair-to-canonical converter · Canonical encoding of a pair of bit lists · Polynomial-time conversion to the verifier's pair encoding · Full run of the pair-encoding converter

TheoremCanonical encoding of a pair of bit lists#✓fully proved

For bit lists \(x\) and \(w\), the canonical bitstring encoding of the pair \((x, w)\) is the concatenation of three parts: every bit \(b\) of \(x\), in order, written as the six bits true, true, true, \(b\), true, false; then a single false; then every bit \(b\) of \(w\), in order, written as the three bits true, \(b\), false.

theorem bitEncode_pair_eq (x w : List Bool) :
    (BitstringEncoding.toEncoding (α := List Bool × List Bool)).encode (x, w) =
      encFst x ++ false :: encSnd w

Uses 10 · Used by 2

Statement usesConverter encoding of the first component · Converter encoding of the second component · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Used byCanonical bit-list decoder · Polynomial-time conversion to the verifier's pair encoding

The machine

InductiveStacks of the pair-encoding converter#✓fully proved

The machine that rewrites the canonical encoding of a pair of bit lists into the verifier's input form has four stacks: the input stack, the output stack, and two stash stacks, one for each component of the pair.

inductive Stk | inp | out | fst | snd
  deriving DecidableEq

Used by 7

Used byPolynomial-time conversion to the verifier's pair encoding · Full run of the pair-encoding converter · Program of the pair-encoding converter · Runs of the pair-encoding converter · Stack contents of the pair-encoding converter · The pair-encoding converter machine · Stack alphabets of the pair-encoding converter

DefinitionStack alphabets of the pair-encoding converter#✓fully proved

The output stack of the converter has as its alphabet the verifier's work alphabet \(G = \{0,1\} \sqcup (\{0,1\} \cup \{\#\})\); the input stack and the two stash stacks have the bits \(\{0,1\}\) as their alphabet.

@[reducible] def Γ : Stk → Type
  | .out => Verifier.G
  | _ => Bool

Uses 2 · Used by 6

Statement usesStacks of the pair-encoding converter · Work alphabet of the dense-SAT verifier

Used byPolynomial-time conversion to the verifier's pair encoding · Full run of the pair-encoding converter · Program of the pair-encoding converter · Runs of the pair-encoding converter · Stack contents of the pair-encoding converter · The pair-encoding converter machine

InductiveLabels of the pair-encoding converter#✓fully proved

The five labels of the converter program: read the first component, read the second component, emit the second component, emit the separator, and emit the first component.

inductive Lab | readFst | readSnd | emitSnd | sep | emitFst
  deriving DecidableEq

Used by 5

Used byPolynomial-time conversion to the verifier's pair encoding · Full run of the pair-encoding converter · Program of the pair-encoding converter · Runs of the pair-encoding converter · The pair-encoding converter machine

AbbreviationState of the pair-encoding converter#✓fully proved

The internal state of the converter is an optional bit: either a bit or nothing. It records the last bit the program stored.

abbrev St := Option Bool

Used by 5

Used byPolynomial-time conversion to the verifier's pair encoding · Full run of the pair-encoding converter · Program of the pair-encoding converter · Runs of the pair-encoding converter · The pair-encoding converter machine

DefinitionProgram of the pair-encoding converter#✓fully proved

The program over the converter's four stacks, five labels and states (a bit or nothing). Each pop either stores the popped bit in the state (nothing if the stack is empty) or leaves the state unchanged, and each push of the stored bit uses false when the state holds nothing.

At read first: pop the input, storing; if the state is true, pop the input twice without storing, once storing and twice without storing, push the stored bit onto the first stash and go to read first; otherwise go to read second. At read second: pop the input, storing; if the state is true, pop the input once storing and once without storing, push the stored bit onto the second stash and go to read second; otherwise go to emit second. At emit second: pop the second stash, storing; if a bit was popped, push it onto the output as a right-tagged bit and go to emit second; otherwise go to separator. At separator: push the separator onto the output and go to emit first. At emit first: pop the first stash, storing; if a bit was popped, push it onto the output as a left-tagged bit and go to emit first; otherwise halt.

Cslib.Complexity.DenseSAT.Converter.prog · 21 lines

def prog : Lab → TM2.Stmt Γ Lab St
  | .readFst =>
      .pop .inp (fun _ o => o) <| .branch (fun s => s == some true)
        (.pop .inp (fun s _ => s) <| .pop .inp (fun s _ => s) <| .pop .inp (fun _ o => o) <|
          .pop .inp (fun s _ => s) <| .pop .inp (fun s _ => s) <|
          .push .fst (fun s => s.getD false) <| .goto fun _ => .readFst)
        (.goto fun _ => .readSnd)
  | .readSnd =>
      .pop .inp (fun _ o => o) <| .branch (fun s => s == some true)
        (.pop .inp (fun _ o => o) <| .pop .inp (fun s _ => s) <|
          .push .snd (fun s => s.getD false) <| .goto fun _ => .readSnd)
        (.goto fun _ => .emitSnd)
  | .emitSnd =>
      .pop .snd (fun _ o => o) <| .branch (fun s => s.isSome)
        (.push .out (fun s => .inr (some (s.getD false))) <| .goto fun _ => .emitSnd)
        (.goto fun _ => .sep)
  | .sep => .push .out (fun _ => .inr none) <| .goto fun _ => .emitFst
  | .emitFst =>
      .pop .fst (fun _ o => o) <| .branch (fun s => s.isSome)
        (.push .out (fun s => .inl (s.getD false)) <| .goto fun _ => .emitFst)
        .halt

Uses 4 · Used by 4

Statement usesLabels of the pair-encoding converter · State of the pair-encoding converter · Stacks of the pair-encoding converter · Stack alphabets of the pair-encoding converter

Used byPolynomial-time conversion to the verifier's pair encoding · Full run of the pair-encoding converter · Runs of the pair-encoding converter · The pair-encoding converter machine

DefinitionThe pair-encoding converter machine#✓fully proved

The converter is the finite multi-stack Turing machine whose stacks are the input stack, the output stack and the two stash stacks, with bits as the alphabet of every stack except the output stack, which holds the verifier's symbols. Its labels are the five phases (read the first component, read the second, emit the second, emit the separator, emit the first), and it starts in the phase that reads the first component. Its internal state is an optional bit (the last bit popped), initially empty, and it runs the converter program. Input is read from the input stack, which holds bits, and output is written to the output stack.

def tm : FinTM2 where
  K := Stk
  k₀ := .inp
  k₁ := .out
  Γ := Γ
  Λ := Lab
  main := .readFst
  σ := St
  initialState := none
  Γk₀Fin := (inferInstance : Fintype Bool)
  m := prog

Uses 5 · Used by 1

Statement usesLabels of the pair-encoding converter · State of the pair-encoding converter · Stacks of the pair-encoding converter · Program of the pair-encoding converter · Stack alphabets of the pair-encoding converter

Used byPolynomial-time conversion to the verifier's pair encoding

Configurations and runs

DefinitionStack contents of the pair-encoding converter#✓fully proved

For bit lists \(i\), \(a\), \(b\) and a list \(o\) of verifier symbols, the contents of the converter's four stacks with \(i\) on the input stack, \(o\) on the output stack, \(a\) on the first stash and \(b\) on the second stash.

def stk (i : List Bool) (o : List Verifier.G) (a b : List Bool) : ∀ k, List (Γ k)
  | .inp => i
  | .out => o
  | .fst => a
  | .snd => b

Uses 3 · Used by 2

Statement usesStacks of the pair-encoding converter · Stack alphabets of the pair-encoding converter · Work alphabet of the dense-SAT verifier

Used byPolynomial-time conversion to the verifier's pair encoding · Full run of the pair-encoding converter

AbbreviationRuns of the pair-encoding converter#✓fully proved

For \(n \in \mathbb{N}\) and configurations \(c\) and \(d\) of the converter, the statement that \(n\) steps of the converter program lead from \(c\) to \(d\).

abbrev Run (n : ℕ) (c d : TM2.Cfg Γ Lab St) : Prop := TM2Program.Run prog n c d

Uses 6 · Used by 1

Statement usesLabels of the pair-encoding converter · State of the pair-encoding converter · Stacks of the pair-encoding converter · Program of the pair-encoding converter · Stack alphabets of the pair-encoding converter · Exact-length runs of a TM2 machine

Used byFull run of the pair-encoding converter

TheoremFull run of the pair-encoding converter#✓fully proved

For bit lists \(x\) and \(w\), the converter program goes in exactly \(2|x| + 2|w| + 5\) steps from the configuration at the label read first, with no bit in the state, the input stack holding every bit \(b\) of \(x\) in order as the six bits true, true, true, \(b\), true, false, then a single false, then every bit \(b\) of \(w\) in order as the three bits true, \(b\), false, and the other three stacks empty, to the halted configuration with no bit in the state, the verifier's pair encoding of \((x, w)\) on the output stack and the other three stacks empty.

theorem convert_run (x w : List Bool) :
    Run (2 * x.length + 2 * w.length + 5)
      ⟨some .readFst, none, stk (encFst x ++ false :: encSnd w) [] [] []⟩
      ⟨none, none, stk [] (Verifier.pairEncode (x, w)) [] []⟩

Uses 13 · Used by 1

Statement usesLabels of the pair-encoding converter · Runs of the pair-encoding converter · State of the pair-encoding converter · Stacks of the pair-encoding converter · Converter encoding of the first component · Converter encoding of the second component · Stack contents of the pair-encoding converter · Stack alphabets of the pair-encoding converter · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Proof usesProgram of the pair-encoding converter · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byPolynomial-time conversion to the verifier's pair encoding

DefinitionPolynomial-time conversion to the verifier's pair encoding#✓fully proved

A polynomial-time computation of the identity map on pairs \((x, w)\) of bit lists, from the canonical bitstring encoding of \((x, w)\) to the verifier's pair encoding of \((x, w)\) (the bits of \(x\), the separator, then the bits of \(w\)), by the converter machine, with the bits and the verifier's symbols themselves as input and output alphabets and time bound \(n + 5\): started on the canonical encoding of \((x, w)\), a list of length \(n\), the converter halts within \(n + 5\) steps with no bit in its state, the verifier's pair encoding of \((x, w)\) on its output stack and every other stack empty.

Cslib.Complexity.DenseSAT.Converter.computable · 21 lines

noncomputable def computable :
    TM2ComputableInPolyTime (BitstringEncoding.toEncoding (α := List Bool × List Bool)).encode
      Verifier.pairEncode id where
  tm := tm
  inputAlphabet := Equiv.refl Bool
  outputAlphabet := Equiv.refl Verifier.G
  time := Polynomial.X + Polynomial.C 5
  outputsFun := fun p => by
    obtain ⟨x, w⟩ := p
    unfold TM2OutputsInTime
    refine { steps := 2 * x.length + 2 * w.length + 5, evals_in_steps := ?_, steps_le_m := ?_ }
    · change (flip bind (TM2.step prog))^[_] (some (initList tm _)) =
        Option.map (haltList tm) (some _)
      rw [bitEncode_pair_eq]
      erw [List.map_id, List.map_id, initList_tm, Option.map_some, haltList_tm]
      exact convert_run x w
    · rw [bitEncode_pair_eq]
      simp only [encFst, encSnd, List.length_append, List.length_cons, List.length_flatMap,
        Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C]
      simp only [List.map_const', List.sum_replicate, smul_eq_mul, List.length_nil]
      omega

Uses 21 · Used by 4

Statement usesLabels of the pair-encoding converter · State of the pair-encoding converter · Stacks of the pair-encoding converter · Canonical encoding of a pair of bit lists · Full run of the pair-encoding converter · Converter encoding of the first component · Converter encoding of the second component · Program of the pair-encoding converter · Stack contents of the pair-encoding converter · The pair-encoding converter machine · Stack alphabets of the pair-encoding converter · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Used byMapping the first component of a pair is polynomial-time · The dense certificate check runs in polynomial time · The SAT host's answer is polynomial-time · Verifier host, canonical form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.