SAT verifier TMs

Machine-level implementation of the deterministic SAT verifier, in the SAT.VerifierTM namespace (recently renamed from a namespace that shadowed TM). Building blocks, in dependency order:

• a deterministic checker for the witness-length side-condition |α| ≤ |z| + 1 (satLengthCheckTM and its retargeted variants);
• a streaming evaluator satEvalOnInputTM for a SAT-encoded CNF against a staged assignment tape, together with its pure semantic model (SatEvalSemState, satEvalSemStep, satEvalSemRun, satEvalSemBits);
• the three-work-tape machine verifyPairTM, which computes the Boolean reference verifier SAT.verifyPair and hence decides pairLang Witness within the quadratic budget verifyPairTMTime (verifyPairTM_decidesInTime).

The pure model is tied to the reference verifier by verifyPairSem and verifyPairSem_eq_verifyPair, so membership in pairLang Witness — the paired witness language underlying SAT.language ∈ NP — is characterized both semantically and at the machine level.

inductive Complexity.SAT.VerifierTM.SatLengthCheckPhase : Type

Control states for the SAT witness-length checker.

• init : SatLengthCheckPhase

  Initial state: step off the left marker before scanning.

• scan : SatLengthCheckPhase

  Scanning state: consume one counter mark per input bit.

• done : SatLengthCheckPhase

  Halt state: the verdict has been written to the output tape.

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instDecidableEqSatLengthCheckPhase : DecidableEq SatLengthCheckPhase

Equations

• Complexity.SAT.VerifierTM.instDecidableEqSatLengthCheckPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instFintypeSatLengthCheckPhase : Fintype SatLengthCheckPhase

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.VerifierTM.satLengthCheckTM : TM 1

Deterministic checker for |input| ≤ B, where B is given as a unary counter on work tape 0. The machine scans one input bit per counter mark, accepts when the input ends, and rejects if the counter is exhausted first.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.VerifierTM.satLengthCheckTime (n : ℕ) : ℕ

A convenient linear upper bound for the length checker.

Equations

• Complexity.SAT.VerifierTM.satLengthCheckTime n = n + 2

theorem Complexity.SAT.VerifierTM.satLengthCheckTM_started_hoareTime (B : ℕ) (α : List Bool) : satLengthCheckTM.HoareTime (fun (inp : Tape) (work : Fin 1 → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool α)).move Dir3.right ∧ (work ⟨0, ⋯⟩).HasUnaryCounter B ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (_work : Fin 1 → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool α)).cells ∧ out.cells 1 = if α.length ≤ B then Γ.one else Γ.zero) (satLengthCheckTime α.length)

Started-tape correctness for the witness-length checker. The input tape is already positioned at cell 1, the counter tape stores a unary bound B, and the output tape is the started blank tape. The machine halts with output 1 iff |α| ≤ B.

theorem Complexity.SAT.VerifierTM.retargetInput_satLengthCheckTM_started_hoareTime (B : ℕ) (α : List Bool) : satLengthCheckTM.retargetInput.HoareTime (fun (_inp : Tape) (work : Fin (1 + 1) → Tape) (out : Tape) => work ⟨1, ⋯⟩ = (Tape.init (List.map Γ.ofBool α)).move Dir3.right ∧ (work ⟨0, ⋯⟩).HasUnaryCounter B ∧ (work ⟨0, ⋯⟩).cells 0 = Γ.start ∧ (∀ j ≥ 1, (work ⟨0, ⋯⟩).cells j ≠ Γ.start) ∧ out = (Tape.init []).move Dir3.right) (fun (_inp : Tape) (work : Fin (1 + 1) → Tape) (out : Tape) => (work ⟨1, ⋯⟩).cells = (Tape.init (List.map Γ.ofBool α)).cells ∧ out.cells 1 = if α.length ≤ B then Γ.one else Γ.zero) (satLengthCheckTime α.length)

Virtual-input/work-tape version of satLengthCheckTM_started_hoareTime. The last work tape supplies the witness bits, work tape 0 supplies a unary counter bound, and the output tape receives 1 iff the witness length is at most that bound. The counter tape precondition includes the structural no-▷ invariant required by retargetInput.

def Complexity.SAT.VerifierTM.satCounter3TM : TM 3

Three-work-tape counter builder obtained by retargeting the input of inputLengthPlusOneCounterTM to work tape 2. Tape 0 stores the unary counter, tape 1 is preserved, and tape 2 provides the formula bits.

Equations

• Complexity.SAT.VerifierTM.satCounter3TM = (Complexity.TM.inputLengthPlusOneCounterTM ⟨0, Complexity.SAT.VerifierTM.satCounter3TM._proof_1⟩).retargetInput

theorem Complexity.SAT.VerifierTM.satCounter3TM_started_hoareTime (z α : List Bool) : satCounter3TM.HoareTime (fun (_inp : Tape) (work : Fin 3 → Tape) (out : Tape) => work ⟨2, ⋯⟩ = (Tape.init (List.map Γ.ofBool z)).move Dir3.right ∧ work ⟨0, ⋯⟩ = (Tape.init []).move Dir3.right ∧ work ⟨1, ⋯⟩ = (Tape.init (List.map Γ.ofBool α)).move Dir3.right ∧ out = (Tape.init []).move Dir3.right) (fun (_inp : Tape) (work : Fin 3 → Tape) (out : Tape) => (work ⟨2, ⋯⟩).cells = (Tape.init (List.map Γ.ofBool z)).cells ∧ (work ⟨2, ⋯⟩).head = z.length + 1 ∧ work ⟨1, ⋯⟩ = (Tape.init (List.map Γ.ofBool α)).move Dir3.right ∧ (work ⟨0, ⋯⟩).HasUnaryCounter (z.length + 1) ∧ (work ⟨0, ⋯⟩).cells 0 = Γ.start ∧ (∀ j ≥ 1, (work ⟨0, ⋯⟩).cells j ≠ Γ.start) ∧ out = (Tape.init []).move Dir3.right) (TM.inputLengthPlusOneCounterTime z.length)

Build the unary counter |z| + 1 on tape 0 from staged formula tape 2 while preserving the staged witness on tape 1 and leaving the output tape in the started blank configuration.

theorem Complexity.SAT.VerifierTM.satCounter3TM_started_stableInput_hoareTime (z α : List Bool) : satCounter3TM.HoareTime (fun (inp : Tape) (work : Fin 3 → Tape) (out : Tape) => inp.read ≠ Γ.start ∧ work ⟨2, ⋯⟩ = (Tape.init (List.map Γ.ofBool z)).move Dir3.right ∧ work ⟨0, ⋯⟩ = (Tape.init []).move Dir3.right ∧ work ⟨1, ⋯⟩ = (Tape.init (List.map Γ.ofBool α)).move Dir3.right ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin 3 → Tape) (out : Tape) => inp.read ≠ Γ.start ∧ (work ⟨2, ⋯⟩).cells = (Tape.init (List.map Γ.ofBool z)).cells ∧ (work ⟨2, ⋯⟩).head = z.length + 1 ∧ work ⟨1, ⋯⟩ = (Tape.init (List.map Γ.ofBool α)).move Dir3.right ∧ (work ⟨0, ⋯⟩).HasUnaryCounter (z.length + 1) ∧ (work ⟨0, ⋯⟩).cells 0 = Γ.start ∧ (∀ j ≥ 1, (work ⟨0, ⋯⟩).cells j ≠ Γ.start) ∧ out = (Tape.init []).move Dir3.right) (TM.inputLengthPlusOneCounterTime z.length)

Richer started-tape wrapper for satCounter3TM that also records that the real input tape remains stable when it starts past ▷.

def Complexity.SAT.VerifierTM.satLengthCheckPassiveTM : TM 2

A two-work-tape version of the SAT witness-length checker. Work tape 0 stores the unary bound, while work tape 1 is preserved exactly.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.VerifierTM.satLengthCheckPassiveTM_started_hoareTime (B : ℕ) (α β : List Bool) : satLengthCheckPassiveTM.HoareTime (fun (inp : Tape) (work : Fin 2 → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool α)).move Dir3.right ∧ (work ⟨0, ⋯⟩).HasUnaryCounter B ∧ work ⟨1, ⋯⟩ = (Tape.init (List.map Γ.ofBool β)).move Dir3.right ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin 2 → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool α)).cells ∧ work ⟨1, ⋯⟩ = (Tape.init (List.map Γ.ofBool β)).move Dir3.right ∧ out.cells 1 = if α.length ≤ B then Γ.one else Γ.zero) (satLengthCheckTime α.length)

Started-tape correctness for satLengthCheckPassiveTM: the machine checks |α| ≤ B while leaving work tape 1 unchanged.

def Complexity.SAT.VerifierTM.satLengthCheck3TM : TM 3

Three-work-tape length checker obtained by retargeting the input of satLengthCheckPassiveTM to work tape 2. Tape 0 stores the unary bound, tape 1 is preserved, and tape 2 provides the witness bits.

Equations

• Complexity.SAT.VerifierTM.satLengthCheck3TM = Complexity.SAT.VerifierTM.satLengthCheckPassiveTM.retargetInput

theorem Complexity.SAT.VerifierTM.satLengthCheck3TM_started_hoareTime (B : ℕ) (α β : List Bool) : satLengthCheck3TM.HoareTime (fun (_inp : Tape) (work : Fin 3 → Tape) (out : Tape) => work ⟨2, ⋯⟩ = (Tape.init (List.map Γ.ofBool α)).move Dir3.right ∧ (work ⟨0, ⋯⟩).HasUnaryCounter B ∧ work ⟨1, ⋯⟩ = (Tape.init (List.map Γ.ofBool β)).move Dir3.right ∧ (work ⟨0, ⋯⟩).cells 0 = Γ.start ∧ (∀ j ≥ 1, (work ⟨0, ⋯⟩).cells j ≠ Γ.start) ∧ out = (Tape.init []).move Dir3.right) (fun (_inp : Tape) (work : Fin 3 → Tape) (out : Tape) => work ⟨1, ⋯⟩ = (Tape.init (List.map Γ.ofBool β)).move Dir3.right ∧ (work ⟨2, ⋯⟩).cells = (Tape.init (List.map Γ.ofBool α)).cells ∧ out.cells 1 = if α.length ≤ B then Γ.one else Γ.zero) (satLengthCheckTime α.length)

Virtual-input/work-tape version of satLengthCheckPassiveTM: work tape 2 supplies the witness bits, work tape 0 supplies the unary bound, and work tape 1 is preserved exactly.

def Complexity.SAT.VerifierTM.satWitnessLengthTailTM : TM 3

Tail of the SAT witness-length verifier after the witness has been copied to tape 2: rewind tapes 1 and 2, then run satLengthCheck3TM.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.VerifierTM.satWitnessLengthTailTime (αLen : ℕ) : ℕ

Time bound for satWitnessLengthTailTM.

Equations

• Complexity.SAT.VerifierTM.satWitnessLengthTailTime αLen = αLen + 1 + 2 + 1 + (αLen + 1 + 2) + 1 + Complexity.SAT.VerifierTM.satLengthCheckTime αLen

inductive Complexity.SAT.VerifierTM.SatEvalMode : Type

Parser/evaluator mode for the deterministic CNF evaluator.

boundary cnf clause empty means the machine is between raw literals. cnf is the value of all completed clauses so far, clause is the disjunction accumulated for the current clause, and empty records whether the current clause has no completed literals. inLit ... sign means a raw literal has started with sign bit sign; each following raw bit must be true, and the assignment work-tape head tracks the current unary variable index.

• boundary (cnf clause empty : Bool) : SatEvalMode

  Between raw literals: cnf is the conjunction of completed clauses, clause the disjunction so far, empty whether the clause has no literals.

• inLit (cnf clause empty sign : Bool) : SatEvalMode

  Inside a raw literal with sign bit sign; the assignment head tracks the unary variable index.

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instDecidableEqSatEvalMode : DecidableEq SatEvalMode

Equations

• Complexity.SAT.VerifierTM.instDecidableEqSatEvalMode = Complexity.SAT.VerifierTM.instDecidableEqSatEvalMode.decEq

def Complexity.SAT.VerifierTM.instDecidableEqSatEvalMode.decEq (x✝ x✝¹ : SatEvalMode) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instReprSatEvalMode : Repr SatEvalMode

Equations

• Complexity.SAT.VerifierTM.instReprSatEvalMode = { reprPrec := Complexity.SAT.VerifierTM.instReprSatEvalMode.repr }

def Complexity.SAT.VerifierTM.instReprSatEvalMode.repr : SatEvalMode → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instFintypeSatEvalMode : Fintype SatEvalMode

Equations

• One or more equations did not get rendered due to their size.

inductive Complexity.SAT.VerifierTM.SatEvalPhase : Type

Control states for the streaming CNF evaluator. The input tape supplies the SAT encoding z; work tape 0 supplies the assignment α.

• readFirst (mode : SatEvalMode) : SatEvalPhase

  Reading the first bit of a doubled-bit token in mode mode.

• readSecond (mode : SatEvalMode) (first : Bool) : SatEvalPhase

  Reading the second bit of a token whose first bit was first.

• rewindAlpha (mode : SatEvalMode) : SatEvalPhase

  Rewinding the assignment tape to its left marker before continuing in mode mode.

• done : SatEvalPhase

  Halt state: the verdict has been written to the output tape.

def Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq (x✝ x✝¹ : SatEvalPhase) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq (Complexity.SAT.VerifierTM.SatEvalPhase.readFirst mode) (Complexity.SAT.VerifierTM.SatEvalPhase.readSecond mode_1 first) = isFalse ⋯
• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq (Complexity.SAT.VerifierTM.SatEvalPhase.readFirst mode) (Complexity.SAT.VerifierTM.SatEvalPhase.rewindAlpha mode_1) = isFalse ⋯
• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq (Complexity.SAT.VerifierTM.SatEvalPhase.readFirst mode) Complexity.SAT.VerifierTM.SatEvalPhase.done = isFalse ⋯
• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq (Complexity.SAT.VerifierTM.SatEvalPhase.readSecond mode first) Complexity.SAT.VerifierTM.SatEvalPhase.done = isFalse ⋯
• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq (Complexity.SAT.VerifierTM.SatEvalPhase.rewindAlpha mode) (Complexity.SAT.VerifierTM.SatEvalPhase.readFirst mode_1) = isFalse ⋯
• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq (Complexity.SAT.VerifierTM.SatEvalPhase.rewindAlpha mode) Complexity.SAT.VerifierTM.SatEvalPhase.done = isFalse ⋯
• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq Complexity.SAT.VerifierTM.SatEvalPhase.done (Complexity.SAT.VerifierTM.SatEvalPhase.readFirst mode) = isFalse ⋯
• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq Complexity.SAT.VerifierTM.SatEvalPhase.done (Complexity.SAT.VerifierTM.SatEvalPhase.readSecond mode first) = isFalse ⋯
• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq Complexity.SAT.VerifierTM.SatEvalPhase.done (Complexity.SAT.VerifierTM.SatEvalPhase.rewindAlpha mode) = isFalse ⋯
• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq Complexity.SAT.VerifierTM.SatEvalPhase.done Complexity.SAT.VerifierTM.SatEvalPhase.done = isTrue ⋯

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase : DecidableEq SatEvalPhase

Equations

• Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase = Complexity.SAT.VerifierTM.instDecidableEqSatEvalPhase.decEq

def Complexity.SAT.VerifierTM.instReprSatEvalPhase.repr : SatEvalPhase → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instReprSatEvalPhase : Repr SatEvalPhase

Equations

• Complexity.SAT.VerifierTM.instReprSatEvalPhase = { reprPrec := Complexity.SAT.VerifierTM.instReprSatEvalPhase.repr }

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instFintypeSatEvalPhase : Fintype SatEvalPhase

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.VerifierTM.satEvalOnInputTM : TM 1

Deterministic evaluator for a SAT-encoded CNF on the input tape and an assignment on work tape 0.

The evaluator tokenizes the input in two-bit groups. It rejects odd-length inputs and malformed raw literals, treats assignment positions beyond α as false by reading blanks, and writes the Boolean value of the decoded CNF to output cell 1. The formal correctness theorem is the next layer; this definition is the concrete finite-state machine that theorem targets.

Equations

• One or more equations did not get rendered due to their size.

inductive Complexity.SAT.VerifierTM.SatEvalSemState : Type

Pure parser/evaluator state for the streaming CNF evaluator, abstracting the machine mode SatEvalMode: either at a token boundary (tracking the CNF-so-far, clause-so-far, and clause-emptiness Booleans) or inLit scanning a raw literal with its sign and unary variable counter var.

• boundary (cnf clause empty : Bool) : SatEvalSemState

  Between tokens: cnf is the conjunction of completed clauses, clause the disjunction so far, empty whether the clause has no literals.

• inLit (cnf clause empty sign : Bool) (var : ℕ) : SatEvalSemState

  Inside a raw literal with sign bit sign and unary variable counter var.

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instDecidableEqSatEvalSemState : DecidableEq SatEvalSemState

Equations

• Complexity.SAT.VerifierTM.instDecidableEqSatEvalSemState = Complexity.SAT.VerifierTM.instDecidableEqSatEvalSemState.decEq

def Complexity.SAT.VerifierTM.instDecidableEqSatEvalSemState.decEq (x✝ x✝¹ : SatEvalSemState) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instReprSatEvalSemState : Repr SatEvalSemState

Equations

• Complexity.SAT.VerifierTM.instReprSatEvalSemState = { reprPrec := Complexity.SAT.VerifierTM.instReprSatEvalSemState.repr }

def Complexity.SAT.VerifierTM.instReprSatEvalSemState.repr : SatEvalSemState → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.VerifierTM.SatEvalSemState.finish : SatEvalSemState → Bool

End-of-input result: at a boundary the value is cnf && empty (the CNF so far, provided the trailing clause is empty, i.e. the last token was #); ending inside a literal is malformed and yields false.

Equations

• (Complexity.SAT.VerifierTM.SatEvalSemState.boundary a a_1 a_2).finish = (a && a_2)
• (Complexity.SAT.VerifierTM.SatEvalSemState.inLit a a_1 a_2 a_3 a_4).finish = false

def Complexity.SAT.VerifierTM.satEvalSemStep (α : Assignment) : SatEvalSemState → EncToken → Option SatEvalSemState

One-token transition of the pure evaluator under assignment α: none on malformed input (a separator with no literal, or a false bit inside a literal body); otherwise the updated SatEvalSemState, folding a completed literal's value into the clause accumulator at each litSep.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.VerifierTM.satEvalSemStep α (Complexity.SAT.VerifierTM.SatEvalSemState.boundary cnf clause empty) Complexity.SAT.EncToken.litSep = none
• Complexity.SAT.VerifierTM.satEvalSemStep α (Complexity.SAT.VerifierTM.SatEvalSemState.inLit cnf clause empty sign var) Complexity.SAT.EncToken.clauseSep = none

def Complexity.SAT.VerifierTM.satEvalSemRun (α : Assignment) : List EncToken → SatEvalSemState → Bool

Run the pure evaluator over a token stream from a given state: fold satEvalSemStep over the tokens, returning false on any malformed step and SatEvalSemState.finish at the end of input.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.VerifierTM.satEvalSemRun α [] x✝ = x✝.finish

def Complexity.SAT.VerifierTM.satEvalSemBits (α z : List Bool) : Bool

Bit-level pure evaluator: tokenize z (rejecting odd-length inputs) and run satEvalSemRun from the initial state .boundary true false true. Equals CNF.eval α on the decoded CNF by satEvalSemBits_eq_decode_eval.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.VerifierTM.satEvalOnInputTime (zLen αLen : ℕ) : ℕ

Coarse polynomial budget for the split-input evaluator. Rewinding the assignment after each completed literal gives a quadratic upper bound once α.length ≤ z.length + 1; this standalone bound keeps both lengths explicit.

Equations

• Complexity.SAT.VerifierTM.satEvalOnInputTime zLen αLen = (zLen + 1) * (αLen + 3) + 2

@[simp]

theorem Complexity.SAT.VerifierTM.Clause.eval_singleton (α : Assignment) (ℓ : Lit) : Clause.eval α [ℓ] = Lit.eval α ℓ

A singleton clause evaluates to the value of its unique literal.

theorem Complexity.SAT.VerifierTM.satEvalSemBits_eq_decode_eval (α z : List Bool) : satEvalSemBits α z = match CNF.decode? z with | none => false | some φ => CNF.eval α φ

Correctness of the pure evaluator: satEvalSemBits α z is false when z fails to decode as a CNF, and otherwise is CNF.eval α of the decoded formula.

def Complexity.SAT.VerifierTM.verifyPairSem (w : List Bool) : Bool

Pure semantic model of the paired SAT verifier: unpair w into (z, α), check the witness-length bound |α| ≤ |z| + 1, and evaluate the encoded CNF z under α via satEvalSemBits; false on malformed pairs.

Equations

• Complexity.SAT.VerifierTM.verifyPairSem w = match Complexity.unpair? w with | none => false | some (z, α) => decide (α.length ≤ z.length + 1) && Complexity.SAT.VerifierTM.satEvalSemBits α z

theorem Complexity.SAT.VerifierTM.verifyPairSem_eq_verifyPair (w : List Bool) : verifyPairSem w = verifyPair w

The pure semantic model agrees with the reference Boolean verifier SAT.verifyPair on every input.

theorem Complexity.SAT.VerifierTM.verifyPairSem_eq_true_iff_mem_pairLang (w : List Bool) : verifyPairSem w = true ↔ w ∈ pairLang Witness

verifyPairSem accepts exactly the members of the paired witness language pairLang Witness.

theorem Complexity.SAT.VerifierTM.pairLang_witness_eq_verifyPairSemLang : pairLang Witness = {w : List Bool | verifyPairSem w = true}

Set-level restatement: pairLang Witness is the language accepted by the pure semantic verifier verifyPairSem.

inductive Complexity.SAT.VerifierTM.VerifyPairPhase : Type

Control states for the deterministic paired SAT verifier.

Work-tape layout:

• tape 0: decoded formula encoding z,
• tape 1: decoded assignment α,
• tape 2: a unary counter initially holding |z| + 1, consumed while copying α.

The machine first validates and splits the outer pair z α encoding, checks the SAT witness length bound during the split, rewinds the staged z and α tapes, and then runs the same streaming CNF evaluator as satEvalOnInputTM against the staged work tapes.

• init : VerifyPairPhase

  Initial state: step off the left markers.

• initCounter : VerifyPairPhase

  Write the extra leading counter tally before the split scan.

• splitScan : VerifyPairPhase

  Split scan: expecting the first bit of a doubled input bit or of the separator 01.

• splitAfterFalse : VerifyPairPhase

  Split scan after a first false: a false completes a doubled bit, a true completes the separator.

• splitAfterTrue : VerifyPairPhase

  Split scan after a first true: only a second true is valid.

• rewindCounterForAlpha : VerifyPairPhase

  Rewind the counter tape before copying the assignment.

• copyAlpha : VerifyPairPhase

  Copy the assignment suffix to work tape 1, consuming counter tallies to enforce the witness-length bound.

• rewindFormula : VerifyPairPhase

  Rewind the staged formula tape to its left marker.

• rewindAssignment : VerifyPairPhase

  Rewind the staged assignment tape to its left marker.

• evalReadFirst (mode : SatEvalMode) : VerifyPairPhase

  Evaluator phase mirroring SatEvalPhase.readFirst.

• evalReadSecond (mode : SatEvalMode) (first : Bool) : VerifyPairPhase

  Evaluator phase mirroring SatEvalPhase.readSecond.

• evalRewindAlpha (mode : SatEvalMode) : VerifyPairPhase

  Evaluator phase mirroring SatEvalPhase.rewindAlpha.

• done : VerifyPairPhase

  Halt state: the verdict has been written to the output tape.

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instDecidableEqVerifyPairPhase : DecidableEq VerifyPairPhase

Equations

• Complexity.SAT.VerifierTM.instDecidableEqVerifyPairPhase = Complexity.SAT.VerifierTM.instDecidableEqVerifyPairPhase.decEq

def Complexity.SAT.VerifierTM.instDecidableEqVerifyPairPhase.decEq (x✝ x✝¹ : VerifyPairPhase) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instReprVerifyPairPhase : Repr VerifyPairPhase

Equations

• Complexity.SAT.VerifierTM.instReprVerifyPairPhase = { reprPrec := Complexity.SAT.VerifierTM.instReprVerifyPairPhase.repr }

def Complexity.SAT.VerifierTM.instReprVerifyPairPhase.repr : VerifyPairPhase → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.SAT.VerifierTM.instFintypeVerifyPairPhase : Fintype VerifyPairPhase

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.VerifierTM.verifyPairTM : TM 3

Deterministic three-work-tape verifier for the Boolean function SAT.verifyPair.

This is the machine-level verifier construction. The polynomial budget below is proved quadratic, and the end-to-end tape simulation below shows that this split/length/evaluation pipeline writes 1 exactly when verifyPair w = true.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.VerifierTM.verifyPairTMTime (n : ℕ) : ℕ

Coarse polynomial budget for verifyPairTM. The split/length prefix is linear, and the staged evaluator is quadratic in the input length because each literal may rewind the assignment tape.

Equations

• Complexity.SAT.VerifierTM.verifyPairTMTime n = (n + 3) * (n + 3) + 6 * n + 20

theorem Complexity.SAT.VerifierTM.verifyPairTMTime_bigO_quadratic : BigO verifyPairTMTime fun (x : ℕ) => x ^ 2

The verifier's time budget verifyPairTMTime is O(n²).

theorem Complexity.SAT.VerifierTM.verifyPairTMTime_polynomial : ∃ (d : ℕ), BigO verifyPairTMTime fun (x : ℕ) => x ^ d

The verifier's time budget is polynomially bounded (witnessed by degree 2), the form needed for polynomial-time verifier packaging.

theorem Complexity.SAT.VerifierTM.verifyPairTM_decidesInTime : verifyPairTM.DecidesInTime (pairLang Witness) verifyPairTMTime

Combine. verifyPairTM decides pairLang Witness within the quadratic budget verifyPairTMTime.