Register invariant for the Tseitin streaming controller

This file connects the pure token transducer in ThreeSAT.Streaming to the finite control and six unary registers of validEmitterTM. It deliberately contains no execution simulation. The definitions here only say how a pure streaming state is represented:

• pending literals retain their signs in PendingSigns;
• the parser scan becomes a StreamMode;
• unbounded variable indices occupy freshReg, currentReg, and the three pending-literal registers;
• the scratch register is zero; and
• the output tape is an append-only TM.OutAcc containing the encoding of the already-emitted tokens.

The projection and parked-tape lemmas are the glue needed to instantiate the register-level Hoare specifications in Machine.Internal.BufferSpecs.

Main definitions

• PendingSigns.ofStreaming
• StreamMode.ofStreaming
• StreamMode.ofState
• BufferValues.ofStreaming
• StreamingStatePred

Finite-control representation

def Complexity.SAT.ThreeSAT.Machine.PendingSigns.ofStreaming : Streaming.Pending → PendingSigns

Forget the variable indices of a pure pending window, retaining exactly the signs kept by the machine controller.

Equations

• Complexity.SAT.ThreeSAT.Machine.PendingSigns.ofStreaming Complexity.SAT.ThreeSAT.Streaming.Pending.zero = Complexity.SAT.ThreeSAT.Machine.PendingSigns.zero
• Complexity.SAT.ThreeSAT.Machine.PendingSigns.ofStreaming (Complexity.SAT.ThreeSAT.Streaming.Pending.one a) = Complexity.SAT.ThreeSAT.Machine.PendingSigns.one a.sign
• Complexity.SAT.ThreeSAT.Machine.PendingSigns.ofStreaming (Complexity.SAT.ThreeSAT.Streaming.Pending.two a b) = Complexity.SAT.ThreeSAT.Machine.PendingSigns.two a.sign b.sign
• Complexity.SAT.ThreeSAT.Machine.PendingSigns.ofStreaming (Complexity.SAT.ThreeSAT.Streaming.Pending.three a b c) = Complexity.SAT.ThreeSAT.Machine.PendingSigns.three a.sign b.sign c.sign

def Complexity.SAT.ThreeSAT.Machine.StreamMode.ofStreaming (pending : Streaming.Pending) : Streaming.Scan → StreamMode

Convert a pure parser scan to its finite controller mode under the signs of the current pending window.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.StreamMode.ofState (st : Streaming.State) : StreamMode

Finite controller mode represented by a complete pure streaming state.

Equations

• Complexity.SAT.ThreeSAT.Machine.StreamMode.ofState st = Complexity.SAT.ThreeSAT.Machine.StreamMode.ofStreaming st.pending st.scan

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.StreamMode.ofState_mk (next : ℕ) (pending : Streaming.Pending) (scan : Streaming.Scan) (emitted : List EncToken) : ofState { next := next, pending := pending, scan := scan, emitted := emitted } = ofStreaming pending scan

theorem Complexity.SAT.ThreeSAT.Machine.PendingSigns.ofStreaming_pushLiteral (st : Streaming.State) (lit : Lit) : ofStreaming (Streaming.pushLiteral st lit).pending = (ofStreaming st.pending).push lit.sign

Sign control after a pure literal push agrees with PendingSigns.push.

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.StreamMode.ofState_pushLiteral (st : Streaming.State) (lit : Lit) : ofState (Streaming.pushLiteral st lit) = boundary ((PendingSigns.ofStreaming st.pending).push lit.sign)

A pure literal push returns the parser to the corresponding boundary mode.

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.StreamMode.ofState_closeClause (st : Streaming.State) : ofState (Streaming.closeClause st) = boundary PendingSigns.zero

Closing a pure clause resets both pending signs and parser mode.

Unary-register representation

def Complexity.SAT.ThreeSAT.Machine.streamingScanValue : Streaming.Scan → ℕ

Unary value stored in currentReg for a pure parser scan.

Equations

• Complexity.SAT.ThreeSAT.Machine.streamingScanValue Complexity.SAT.ThreeSAT.Streaming.Scan.boundary = 0
• Complexity.SAT.ThreeSAT.Machine.streamingScanValue (Complexity.SAT.ThreeSAT.Streaming.Scan.literal sign var) = var

def Complexity.SAT.ThreeSAT.Machine.streamingBufferA : Streaming.Pending → ℕ

Unary value stored in bufferAReg for a pending window.

Equations

• Complexity.SAT.ThreeSAT.Machine.streamingBufferA Complexity.SAT.ThreeSAT.Streaming.Pending.zero = 0
• Complexity.SAT.ThreeSAT.Machine.streamingBufferA (Complexity.SAT.ThreeSAT.Streaming.Pending.one a) = a.var
• Complexity.SAT.ThreeSAT.Machine.streamingBufferA (Complexity.SAT.ThreeSAT.Streaming.Pending.two a b) = a.var
• Complexity.SAT.ThreeSAT.Machine.streamingBufferA (Complexity.SAT.ThreeSAT.Streaming.Pending.three a b c) = a.var

def Complexity.SAT.ThreeSAT.Machine.streamingBufferB : Streaming.Pending → ℕ

Unary value stored in bufferBReg for a pending window.

Equations

• Complexity.SAT.ThreeSAT.Machine.streamingBufferB Complexity.SAT.ThreeSAT.Streaming.Pending.zero = 0
• Complexity.SAT.ThreeSAT.Machine.streamingBufferB (Complexity.SAT.ThreeSAT.Streaming.Pending.one a) = 0
• Complexity.SAT.ThreeSAT.Machine.streamingBufferB (Complexity.SAT.ThreeSAT.Streaming.Pending.two a b) = b.var
• Complexity.SAT.ThreeSAT.Machine.streamingBufferB (Complexity.SAT.ThreeSAT.Streaming.Pending.three a b c) = b.var

def Complexity.SAT.ThreeSAT.Machine.streamingBufferC : Streaming.Pending → ℕ

Unary value stored in bufferCReg for a pending window.

Equations

• Complexity.SAT.ThreeSAT.Machine.streamingBufferC Complexity.SAT.ThreeSAT.Streaming.Pending.zero = 0
• Complexity.SAT.ThreeSAT.Machine.streamingBufferC (Complexity.SAT.ThreeSAT.Streaming.Pending.one a) = 0
• Complexity.SAT.ThreeSAT.Machine.streamingBufferC (Complexity.SAT.ThreeSAT.Streaming.Pending.two a b) = 0
• Complexity.SAT.ThreeSAT.Machine.streamingBufferC (Complexity.SAT.ThreeSAT.Streaming.Pending.three a b c) = c.var

def Complexity.SAT.ThreeSAT.Machine.BufferValues.ofStreaming (st : Streaming.State) : BufferValues

Six unary-register values representing a pure streaming state.

Equations

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

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.ofStreaming_fresh (st : Streaming.State) : (ofStreaming st).fresh = st.next

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.ofStreaming_current (st : Streaming.State) : (ofStreaming st).current = streamingScanValue st.scan

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.ofStreaming_a (st : Streaming.State) : (ofStreaming st).a = streamingBufferA st.pending

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.ofStreaming_b (st : Streaming.State) : (ofStreaming st).b = streamingBufferB st.pending

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.ofStreaming_c (st : Streaming.State) : (ofStreaming st).c = streamingBufferC st.pending

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.ofStreaming_scratch (st : Streaming.State) : (ofStreaming st).scratch = 0

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.ofStreaming_work_parked (st : Streaming.State) (i : Fin workTapeCount) : TM.Parked ((ofStreaming st).work i)

Every register tape in the representation of a pure state is parked.

Complete tape predicate

def Complexity.SAT.ThreeSAT.Machine.StreamingStatePred (inp : Tape) (st : Streaming.State) : TapePred workTapeCount

Tape-level representation of a pure streaming state. The input tape is a fixed parked ghost for buffer operations; the work tapes are its six unary registers; and the output accumulator contains exactly the emitted tokens.

Equations

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

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.streamingStatePred_eq_bufferPred (inp : Tape) (st : Streaming.State) : StreamingStatePred inp st = BufferPred inp (BufferValues.ofStreaming st) (encodeTokens st.emitted)

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.input_eq {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) : actualInput = inp

Project the fixed input tape from the streaming-state predicate.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.work_eq {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) : work = (BufferValues.ofStreaming st).work

Project the six-register work-tape function.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.outAcc {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) : TM.OutAcc (encodeTokens st.emitted) out

Project the exact append-only encoded-token accumulator.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.input_parked {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) (hinp : TM.Parked inp) : TM.Parked actualInput

The represented input is parked whenever its fixed ghost is parked.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.work_parked {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) (i : Fin workTapeCount) : TM.Parked (work i)

Every represented work tape is parked.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.output_parked {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) : TM.Parked out

The represented output accumulator is parked.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.work_fresh {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) : work freshReg = TM.regTape st.next

Project the fresh-variable register.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.work_current {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) : work currentReg = TM.regTape (streamingScanValue st.scan)

Project the current-literal register.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.work_a {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) : work bufferAReg = TM.regTape (streamingBufferA st.pending)

Project the first pending-literal register.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.work_b {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) : work bufferBReg = TM.regTape (streamingBufferB st.pending)

Project the second pending-literal register.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.work_c {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) : work bufferCReg = TM.regTape (streamingBufferC st.pending)

Project the third pending-literal register.

theorem Complexity.SAT.ThreeSAT.Machine.StreamingStatePred.work_scratch {inp actualInput out : Tape} {st : Streaming.State} {work : Fin workTapeCount → Tape} (h : StreamingStatePred inp st actualInput work out) : work scratchReg = TM.regTape 0

Project the zero scratch register.