Hoare specifications for Tseitin literal buffers and emitters

This file gives the register-level contracts used by the streaming-controller induction. A BufferValues packages the values of all six unary registers; BufferValues.work realizes it as the concrete work-tape function. Every contract fixes a parked input tape, preserves the scratch register, and tracks the append-only output word exactly.

Time bounds are explicit structural sums of the already-proved register and emitter bounds. Keeping the composition overhead visible makes these theorems stable under later polynomial rounding.

Main results

• emitClauseTM_hoareTime_internal
• emitWideLinkTM_hoareTime_internal
• emitPendingTM_hoareTime_internal
• clearBuffersTM_hoareTime_internal
• rollWideBuffersTM_hoareTime_internal
• commitLiteralTM_hoareTime_internal
• closeClauseTM_hoareTime_internal

Six-register model

structure Complexity.SAT.ThreeSAT.Machine.BufferValues : Type

Values stored in the six fixed work registers of the streaming machine.

• fresh : ℕ

  First unused variable index.

• current : ℕ

  Variable index currently being decoded.

• a : ℕ

  First pending literal's variable index.

• b : ℕ

  Second pending literal's variable index.

• c : ℕ

  Third pending literal's variable index.

• scratch : ℕ

  Temporary register, zero between controller operations.

def Complexity.SAT.ThreeSAT.Machine.instDecidableEqBufferValues.decEq (x✝ x✝¹ : BufferValues) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instDecidableEqBufferValues : DecidableEq BufferValues

Equations

• Complexity.SAT.ThreeSAT.Machine.instDecidableEqBufferValues = Complexity.SAT.ThreeSAT.Machine.instDecidableEqBufferValues.decEq

def Complexity.SAT.ThreeSAT.Machine.BufferValues.work (v : BufferValues) (i : Fin workTapeCount) : Tape

Realize six values as the concrete fixed-layout unary-register tapes.

Equations

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

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.work_fresh (v : BufferValues) : v.work freshReg = TM.regTape v.fresh

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.work_current (v : BufferValues) : v.work currentReg = TM.regTape v.current

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.work_a (v : BufferValues) : v.work bufferAReg = TM.regTape v.a

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.work_b (v : BufferValues) : v.work bufferBReg = TM.regTape v.b

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.work_c (v : BufferValues) : v.work bufferCReg = TM.regTape v.c

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.work_scratch (v : BufferValues) : v.work scratchReg = TM.regTape v.scratch

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.work_parked (v : BufferValues) (i : Fin workTapeCount) : TM.Parked (v.work i)

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.update_fresh (v : BufferValues) (x : ℕ) : Function.update v.work freshReg (TM.regTape x) = { fresh := x, current := v.current, a := v.a, b := v.b, c := v.c, scratch := v.scratch }.work

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.update_current (v : BufferValues) (x : ℕ) : Function.update v.work currentReg (TM.regTape x) = { fresh := v.fresh, current := x, a := v.a, b := v.b, c := v.c, scratch := v.scratch }.work

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.update_a (v : BufferValues) (x : ℕ) : Function.update v.work bufferAReg (TM.regTape x) = { fresh := v.fresh, current := v.current, a := x, b := v.b, c := v.c, scratch := v.scratch }.work

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.update_b (v : BufferValues) (x : ℕ) : Function.update v.work bufferBReg (TM.regTape x) = { fresh := v.fresh, current := v.current, a := v.a, b := x, c := v.c, scratch := v.scratch }.work

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.update_c (v : BufferValues) (x : ℕ) : Function.update v.work bufferCReg (TM.regTape x) = { fresh := v.fresh, current := v.current, a := v.a, b := v.b, c := x, scratch := v.scratch }.work

def Complexity.SAT.ThreeSAT.Machine.BufferPred (inp : Tape) (v : BufferValues) (ys : List Bool) : TapePred workTapeCount

Standard Hoare predicate for a fixed input, six registers, and output accumulator.

Equations

• Complexity.SAT.ThreeSAT.Machine.BufferPred inp v ys = Complexity.TM.EmitPred inp v.work ys

Encoded output words and structural time bounds

def Complexity.SAT.ThreeSAT.Machine.literalBits (sign : Bool) (var : ℕ) : List Bool

Concrete encoded bits appended by emitLitTM for a literal.

Equations

• Complexity.SAT.ThreeSAT.Machine.literalBits sign var = [sign, sign] ++ List.replicate (2 * var) true ++ [false, true]

def Complexity.SAT.ThreeSAT.Machine.clauseBits (aSign : Bool) (a : ℕ) (bSign : Bool) (b : ℕ) (cSign : Bool) (c : ℕ) : List Bool

Concrete encoding of one three-literal clause, including its clause separator.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.literalTime (var : ℕ) : ℕ

Exact primitive bound for one literal emitter.

Equations

• Complexity.SAT.ThreeSAT.Machine.literalTime var = 3 * var + 9

def Complexity.SAT.ThreeSAT.Machine.clauseTime (a b c : ℕ) : ℕ

Structural bound for three literal emitters and a clause separator.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.copyTime (src dst : ℕ) : ℕ

Exact bound exposed by copyIntoTM_hoareTime.

Equations

• Complexity.SAT.ThreeSAT.Machine.copyTime src dst = 2 * dst + 4 + 1 + (src * (2 * (0 + src) + 4 + 2) + (src + 2))

def Complexity.SAT.ThreeSAT.Machine.unaryUpdateTime (v : ℕ) : ℕ

Primitive increment/clear bound for a unary register.

Equations

• Complexity.SAT.ThreeSAT.Machine.unaryUpdateTime v = 2 * v + 4

Clause emitters

theorem Complexity.SAT.ThreeSAT.Machine.emitClauseTM_hoareTime_internal (aSign bSign cSign : Bool) (aReg bReg cReg : Fin workTapeCount) (a b c : ℕ) (inp : Tape) (work : Fin workTapeCount → Tape) (ys : List Bool) (hinp : TM.Parked inp) (hwork : ∀ (i : Fin workTapeCount), TM.Parked (work i)) (ha : work aReg = TM.regTape a) (hb : work bReg = TM.regTape b) (hc : work cReg = TM.regTape c) : (emitClauseTM aSign aReg bSign bReg cSign cReg).HoareTime (TM.EmitPred inp work ys) (TM.EmitPred inp work (ys ++ clauseBits aSign a bSign b cSign c)) (clauseTime a b c)

Emit exactly one encoded three-literal clause, preserving every tape except for append-only output growth.

theorem Complexity.SAT.ThreeSAT.Machine.emitWideLinkTM_hoareTime_internal (aSign bSign : Bool) (v : BufferValues) (inp : Tape) (ys : List Bool) (hinp : TM.Parked inp) : (emitWideLinkTM aSign bSign).HoareTime (BufferPred inp v ys) (BufferPred inp v (ys ++ clauseBits aSign v.a bSign v.b true v.fresh)) (clauseTime v.a v.b v.fresh)

Specialized wide-link emitter (a ∨ b ∨ fresh).

Pending-clause emission

def Complexity.SAT.ThreeSAT.Machine.pendingBits (pending : PendingSigns) (v : BufferValues) : List Bool

Bits emitted when closing the pending finite-control clause shape.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Machine.pendingBits (Complexity.SAT.ThreeSAT.Machine.PendingSigns.one aSign) v = Complexity.SAT.ThreeSAT.Machine.clauseBits aSign v.a aSign v.a aSign v.a
• Complexity.SAT.ThreeSAT.Machine.pendingBits (Complexity.SAT.ThreeSAT.Machine.PendingSigns.two aSign bSign) v = Complexity.SAT.ThreeSAT.Machine.clauseBits aSign v.a bSign v.b bSign v.b
• Complexity.SAT.ThreeSAT.Machine.pendingBits (Complexity.SAT.ThreeSAT.Machine.PendingSigns.three aSign bSign cSign) v = Complexity.SAT.ThreeSAT.Machine.clauseBits aSign v.a bSign v.b cSign v.c

def Complexity.SAT.ThreeSAT.Machine.pendingTime (pending : PendingSigns) (v : BufferValues) : ℕ

Structural time bound for emitPendingTM.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Machine.pendingTime (Complexity.SAT.ThreeSAT.Machine.PendingSigns.one aSign) v = Complexity.SAT.ThreeSAT.Machine.clauseTime v.a v.a v.a
• Complexity.SAT.ThreeSAT.Machine.pendingTime (Complexity.SAT.ThreeSAT.Machine.PendingSigns.two aSign bSign) v = Complexity.SAT.ThreeSAT.Machine.clauseTime v.a v.b v.b
• Complexity.SAT.ThreeSAT.Machine.pendingTime (Complexity.SAT.ThreeSAT.Machine.PendingSigns.three aSign bSign cSign) v = Complexity.SAT.ThreeSAT.Machine.clauseTime v.a v.b v.c

theorem Complexity.SAT.ThreeSAT.Machine.emitPendingTM_hoareTime_internal (pending : PendingSigns) (v : BufferValues) (inp : Tape) (ys : List Bool) (hinp : TM.Parked inp) : (emitPendingTM pending).HoareTime (BufferPred inp v ys) (BufferPred inp v (ys ++ pendingBits pending v)) (pendingTime pending v)

Emit the exact-3 gadget selected by PendingSigns, leaving all registers unchanged.

Buffer clearing

def Complexity.SAT.ThreeSAT.Machine.BufferValues.cleared (v : BufferValues) : BufferValues

Register values after clearing the current literal and three buffers.

Equations

• v.cleared = { fresh := v.fresh, current := 0, a := 0, b := 0, c := 0, scratch := v.scratch }

def Complexity.SAT.ThreeSAT.Machine.clearBuffersTime (v : BufferValues) : ℕ

Structural time bound for clearBuffersTM.

Equations

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

theorem Complexity.SAT.ThreeSAT.Machine.clearBuffersTM_hoareTime_internal (v : BufferValues) (inp : Tape) (ys : List Bool) (hinp : TM.Parked inp) : clearBuffersTM.HoareTime (BufferPred inp v ys) (BufferPred inp v.cleared ys) (clearBuffersTime v)

Clear all literal registers, preserving fresh/scratch and output.

Wide-window rotation

def Complexity.SAT.ThreeSAT.Machine.BufferValues.rolled (v : BufferValues) : BufferValues

Register values after rotating (a,b,c,current,fresh) to (fresh,c,current,0,fresh+1).

Equations

• v.rolled = { fresh := v.fresh + 1, current := 0, a := v.fresh, b := v.c, c := v.current, scratch := v.scratch }

def Complexity.SAT.ThreeSAT.Machine.rollWideBuffersTime (v : BufferValues) : ℕ

Structural time bound for rollWideBuffersTM.

Equations

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

theorem Complexity.SAT.ThreeSAT.Machine.rollWideBuffersTM_hoareTime_internal (v : BufferValues) (inp : Tape) (ys : List Bool) (hinp : TM.Parked inp) : rollWideBuffersTM.HoareTime (BufferPred inp v ys) (BufferPred inp v.rolled ys) (rollWideBuffersTime v)

Rotate the three pending buffers after emitting a wide link.

Literal commit

def Complexity.SAT.ThreeSAT.Machine.BufferValues.committed (pending : PendingSigns) (v : BufferValues) : BufferValues

Register values after committing currentReg under a pending shape.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Machine.BufferValues.committed (Complexity.SAT.ThreeSAT.Machine.PendingSigns.three aSign bSign cSign) v = v.rolled

def Complexity.SAT.ThreeSAT.Machine.commitBits (pending : PendingSigns) (v : BufferValues) : List Bool

Bits emitted while committing a literal. Only the fourth-and-later case emits a completed wide link.

Equations

• Complexity.SAT.ThreeSAT.Machine.commitBits (Complexity.SAT.ThreeSAT.Machine.PendingSigns.three aSign bSign c) v = Complexity.SAT.ThreeSAT.Machine.clauseBits aSign v.a bSign v.b true v.fresh
• Complexity.SAT.ThreeSAT.Machine.commitBits pending v = []

def Complexity.SAT.ThreeSAT.Machine.commitLiteralTime (pending : PendingSigns) (v : BufferValues) : ℕ

Structural time bound for commitLiteralTM.

Equations

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

theorem Complexity.SAT.ThreeSAT.Machine.commitLiteralTM_hoareTime_internal (pending : PendingSigns) (v : BufferValues) (inp : Tape) (ys : List Bool) (hinp : TM.Parked inp) : (commitLiteralTM pending).HoareTime (BufferPred inp v ys) (BufferPred inp (BufferValues.committed pending v) (ys ++ commitBits pending v)) (commitLiteralTime pending v)

Commit the current decoded literal: buffer it when fewer than three are pending, or emit and roll a wide link otherwise.

Clause close

def Complexity.SAT.ThreeSAT.Machine.BufferValues.advanced (pending : PendingSigns) (v : BufferValues) : BufferValues

Fresh-register value after the empty-clause advance phase.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Machine.BufferValues.advanced pending v = v

def Complexity.SAT.ThreeSAT.Machine.BufferValues.closed (pending : PendingSigns) (v : BufferValues) : BufferValues

Final registers after closing and clearing a clause.

Equations

• Complexity.SAT.ThreeSAT.Machine.BufferValues.closed pending v = (Complexity.SAT.ThreeSAT.Machine.BufferValues.advanced pending v).cleared

def Complexity.SAT.ThreeSAT.Machine.advanceFreshTime (pending : PendingSigns) (v : BufferValues) : ℕ

Time for the fresh-advance phase selected by closeClauseTM.

Equations

• Complexity.SAT.ThreeSAT.Machine.advanceFreshTime Complexity.SAT.ThreeSAT.Machine.PendingSigns.zero v = Complexity.SAT.ThreeSAT.Machine.unaryUpdateTime v.fresh
• Complexity.SAT.ThreeSAT.Machine.advanceFreshTime pending v = 1

def Complexity.SAT.ThreeSAT.Machine.closeClauseTime (pending : PendingSigns) (v : BufferValues) : ℕ

Structural time bound for closing a clause.

Equations

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

theorem Complexity.SAT.ThreeSAT.Machine.closeClauseTM_hoareTime_internal (pending : PendingSigns) (v : BufferValues) (inp : Tape) (ys : List Bool) (hinp : TM.Parked inp) : (closeClauseTM pending).HoareTime (BufferPred inp v ys) (BufferPred inp (BufferValues.closed pending v) (ys ++ pendingBits pending v)) (closeClauseTime pending v)

Emit the pending clause, perform the empty-clause fresh increment when needed, and reset all literal buffers.