Streaming controller for the CNF-to-3CNF reduction machine

validEmitterTM is the concrete valid-input controller for the buffer and emission layer. It reads the already-validated input in two-bit tokens, keeps literal signs and the number of pending literals in finite control, and stores all unbounded variable indices in unary work registers.

The controller invokes three families of child machines:

• incRegTM currentReg for every unary body bit;
• commitLiteralTM pending at a literal separator;
• closeClauseTM pending at a clause separator.

The latter two child-state types depend on pending, so the controller state uses sigma types. Each child is run to its halt state before the controller resumes reading at the next input token. reductionTM installs this controller in the validation-first total assembly from Machine.Defs.

This file defines the machine. Its simulation invariant and polynomial-time accounting live in proof-only internal modules and are exposed publicly by Complexitylib.SAT.Tseitin.Machine.

Controller state

inductive Complexity.SAT.ThreeSAT.Machine.StreamMode : Type

Parser mode after tokenization. A literal sign is retained in finite control while its unary variable body accumulates in currentReg.

• boundary (pending : PendingSigns) : StreamMode
• literal (pending : PendingSigns) (sign : Bool) : StreamMode

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instDecidableEqStreamMode : DecidableEq StreamMode

Equations

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

def Complexity.SAT.ThreeSAT.Machine.instDecidableEqStreamMode.decEq (x✝ x✝¹ : StreamMode) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instFintypeStreamMode : Fintype StreamMode

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instReprStreamMode : Repr StreamMode

Equations

• Complexity.SAT.ThreeSAT.Machine.instReprStreamMode = { reprPrec := Complexity.SAT.ThreeSAT.Machine.instReprStreamMode.repr }

def Complexity.SAT.ThreeSAT.Machine.instReprStreamMode.repr : StreamMode → ℕ → Std.Format

Equations

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

inductive Complexity.SAT.ThreeSAT.Machine.ReadPhase : Type

The controller alternates between the first and second bit of each token.

• first (mode : StreamMode) : ReadPhase
• second (mode : StreamMode) (firstBit : Bool) : ReadPhase

def Complexity.SAT.ThreeSAT.Machine.instDecidableEqReadPhase.decEq (x✝ x✝¹ : ReadPhase) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instDecidableEqReadPhase : DecidableEq ReadPhase

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instFintypeReadPhase : Fintype ReadPhase

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instReprReadPhase : Repr ReadPhase

Equations

• Complexity.SAT.ThreeSAT.Machine.instReprReadPhase = { reprPrec := Complexity.SAT.ThreeSAT.Machine.instReprReadPhase.repr }

def Complexity.SAT.ThreeSAT.Machine.instReprReadPhase.repr : ReadPhase → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Complexity.SAT.ThreeSAT.Machine.IncrementCall : Type

State of an in-progress unary-register increment, paired with the parser mode to restore when the child machine halts.

Equations

• Complexity.SAT.ThreeSAT.Machine.IncrementCall = (Complexity.SAT.ThreeSAT.Machine.StreamMode × (Complexity.TM.incRegTM Complexity.SAT.ThreeSAT.Machine.currentReg).Q)

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.incrementCallDecidableEq : DecidableEq IncrementCall

Equations

• Complexity.SAT.ThreeSAT.Machine.incrementCallDecidableEq = id inferInstance

@[reducible, inline]

abbrev Complexity.SAT.ThreeSAT.Machine.CommitCall : Type

State of an in-progress literal commit. The child state type depends on the pending-sign shape selected at the call site.

Equations

• Complexity.SAT.ThreeSAT.Machine.CommitCall = ((pending : Complexity.SAT.ThreeSAT.Machine.PendingSigns) × Bool × (Complexity.SAT.ThreeSAT.Machine.commitLiteralTM pending).Q)

@[implicit_reducible]

def Complexity.SAT.ThreeSAT.Machine.commitStateDecidableEq (pending : PendingSigns) : DecidableEq (commitLiteralTM pending).Q

Equality decision for the pending-dependent commit child state.

Equations

• Complexity.SAT.ThreeSAT.Machine.commitStateDecidableEq pending = (Complexity.SAT.ThreeSAT.Machine.commitLiteralTM pending).decEq

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.commitCallDecidableEq : DecidableEq CommitCall

Equations

• Complexity.SAT.ThreeSAT.Machine.commitCallDecidableEq = id inferInstance

@[reducible, inline]

abbrev Complexity.SAT.ThreeSAT.Machine.CloseCall : Type

State of an in-progress clause close.

Equations

• Complexity.SAT.ThreeSAT.Machine.CloseCall = ((pending : Complexity.SAT.ThreeSAT.Machine.PendingSigns) × (Complexity.SAT.ThreeSAT.Machine.closeClauseTM pending).Q)

@[implicit_reducible]

def Complexity.SAT.ThreeSAT.Machine.closeStateDecidableEq (pending : PendingSigns) : DecidableEq (closeClauseTM pending).Q

Equality decision for the pending-dependent clause-close child state.

Equations

• Complexity.SAT.ThreeSAT.Machine.closeStateDecidableEq pending = (Complexity.SAT.ThreeSAT.Machine.closeClauseTM pending).decEq

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.closeCallDecidableEq : DecidableEq CloseCall

Equations

• Complexity.SAT.ThreeSAT.Machine.closeCallDecidableEq = id inferInstance

@[reducible, inline]

abbrev Complexity.SAT.ThreeSAT.Machine.ControllerQ : Type

Finite controller states: reading, one of three dependent child calls, or the unique halt state.

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instDecidableEqControllerQ : DecidableEq ControllerQ

Equations

• Complexity.SAT.ThreeSAT.Machine.instDecidableEqControllerQ a b = instDecidableEqSum a b

def Complexity.SAT.ThreeSAT.Machine.controllerRead (phase : ReadPhase) : ControllerQ

Inject a read phase into the controller state.

Equations

• Complexity.SAT.ThreeSAT.Machine.controllerRead phase = Sum.inl phase

def Complexity.SAT.ThreeSAT.Machine.controllerIncrement (mode : StreamMode) (q : (TM.incRegTM currentReg).Q) : ControllerQ

Inject an increment child state into the controller state.

Equations

• Complexity.SAT.ThreeSAT.Machine.controllerIncrement mode q = Sum.inr (Sum.inl (mode, q))

def Complexity.SAT.ThreeSAT.Machine.controllerCommit (pending : PendingSigns) (sign : Bool) (q : (commitLiteralTM pending).Q) : ControllerQ

Inject a pending-dependent commit child state into the controller state.

Equations

• Complexity.SAT.ThreeSAT.Machine.controllerCommit pending sign q = Sum.inr (Sum.inr (Sum.inl ⟨pending, (sign, q)⟩))

def Complexity.SAT.ThreeSAT.Machine.controllerClose (pending : PendingSigns) (q : (closeClauseTM pending).Q) : ControllerQ

Inject a pending-dependent clause-close child state.

Equations

• Complexity.SAT.ThreeSAT.Machine.controllerClose pending q = Sum.inr (Sum.inr (Sum.inr (Sum.inl ⟨pending, q⟩)))

def Complexity.SAT.ThreeSAT.Machine.controllerDone : ControllerQ

The unique controller halt state.

Equations

• Complexity.SAT.ThreeSAT.Machine.controllerDone = Sum.inr (Sum.inr (Sum.inr (Sum.inr ())))

def Complexity.SAT.ThreeSAT.Machine.scheduleToken (mode : StreamMode) (token : EncToken) : ControllerQ

Schedule the operation denoted by a complete token. Invalid cases halt; they are unreachable after the preceding successful validation pass.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Machine.scheduleToken (Complexity.SAT.ThreeSAT.Machine.StreamMode.boundary pending) Complexity.SAT.EncToken.litSep = Complexity.SAT.ThreeSAT.Machine.controllerDone

Concrete controller

def Complexity.SAT.ThreeSAT.Machine.validEmitterTM : TM workTapeCount

Stream over a validated concrete CNF encoding and emit its exact-3 Tseitin transformation. The input must begin at cell one, freshReg must hold the first fresh variable, all literal buffers must be zero registers, and the output must be an empty append-only accumulator.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.reductionTM : TM workTapeCount

Final concrete machine for the total encoded reduction. It initializes the fresh counter, validates before emission, clears the validator verdict on the selected branch, runs validEmitterTM on valid inputs, and emits the fixed fallback on malformed inputs.

Equations

• Complexity.SAT.ThreeSAT.Machine.reductionTM = Complexity.SAT.ThreeSAT.Machine.reductionTMWith Complexity.SAT.ThreeSAT.Machine.validEmitterTM