Completed child calls of the Tseitin streaming controller

This module combines the tape-level Hoare contracts for register operations with the controller's child-trace embeddings. Each theorem starts at a scheduled child call, runs that child to completion, takes the single return step, and exposes the resulting first-bit read state together with the exact buffer/output postcondition.

def Complexity.SAT.ThreeSAT.Machine.ControllerReadPred (mode : StreamMode) (pred : TapePred workTapeCount) (c : Cfg workTapeCount validEmitterTM.Q) : Prop

A controller configuration is ready to read the next token in mode, and its tapes satisfy pred.

Equations

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

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_increment_call_internal (mode : StreamMode) (v : BufferValues) (inp : Tape) (ys : List Bool) (hinp : TM.Parked inp) {actualInput out : Tape} {work : Fin workTapeCount → Tape} (hpre : BufferPred inp v ys actualInput work out) : ∃ (c' : Cfg workTapeCount validEmitterTM.Q), ∃ t ≤ unaryUpdateTime v.current + 1, validEmitterTM.reachesIn t (controllerIncrementCfg mode { state := (TM.incRegTM currentReg).qstart, input := actualInput, work := work, output := out }) c' ∧ ControllerReadPred mode (BufferPred inp { fresh := v.fresh, current := v.current + 1, a := v.a, b := v.b, c := v.c, scratch := v.scratch } ys) c'

Run a scheduled current-register increment and return to the saved literal mode.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_commit_call_internal (pending : PendingSigns) (sign : Bool) (v : BufferValues) (inp : Tape) (ys : List Bool) (hinp : TM.Parked inp) {actualInput out : Tape} {work : Fin workTapeCount → Tape} (hpre : BufferPred inp v ys actualInput work out) : ∃ (c' : Cfg workTapeCount validEmitterTM.Q), ∃ t ≤ commitLiteralTime pending v + 1, validEmitterTM.reachesIn t (controllerCommitCfg pending sign { state := (commitLiteralTM pending).qstart, input := actualInput, work := work, output := out }) c' ∧ ControllerReadPred (StreamMode.boundary (pending.push sign)) (BufferPred inp (BufferValues.committed pending v) (ys ++ commitBits pending v)) c'

Run a scheduled literal commit and return to the updated boundary mode.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_close_call_internal (pending : PendingSigns) (v : BufferValues) (inp : Tape) (ys : List Bool) (hinp : TM.Parked inp) {actualInput out : Tape} {work : Fin workTapeCount → Tape} (hpre : BufferPred inp v ys actualInput work out) : ∃ (c' : Cfg workTapeCount validEmitterTM.Q), ∃ t ≤ closeClauseTime pending v + 1, validEmitterTM.reachesIn t (controllerCloseCfg pending { state := (closeClauseTM pending).qstart, input := actualInput, work := work, output := out }) c' ∧ ControllerReadPred (StreamMode.boundary PendingSigns.zero) (BufferPred inp (BufferValues.closed pending v) (ys ++ pendingBits pending v)) c'

Run a scheduled clause close and return to the empty boundary mode.