Typed-input specification for the Tseitin valid emitter

This module closes the concrete controller proof on a typed CNF encoding. The front-end register layout is identified with the pure streaming initial state, the full token stream is simulated at the global input-derived cap, and the one trailing-blank step halts validEmitterTM. The postcondition is the exact StreamingStatePred determined by CNF.to3Aux.

The structural specification uses controllerRunBudget; a second theorem rounds it to the library's explicit quartic envelope.

Main results

• validEmitterFinalState
• frontEndWork_eq_initialBufferValues_internal
• validEmitterTM_hoareTime_internal
• validEmitterTM_hoareTime_quartic_internal

def Complexity.SAT.ThreeSAT.Machine.validEmitterFinalState (phi : CNF) : Streaming.State

Exact pure streaming endpoint for a typed CNF input.

Equations

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

theorem Complexity.SAT.ThreeSAT.Machine.frontEndWork_eq_initialBufferValues_internal (z : List Bool) : frontEndWork z = (BufferValues.ofStreaming (Streaming.initial (z.length + 1))).work

The front-end unary registers are exactly the register representation of the pure streaming initial state.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_hoareTime_internal (phi : CNF) : validEmitterTM.HoareTime (validEmitterPre phi.encode) (StreamingStatePred (framedTokenInput phi.tokens []) (validEmitterFinalState phi)) (controllerRunBudget phi.encode.length)

On a typed CNF encoding, the concrete valid emitter halts with the exact register and output representation of the pure streaming endpoint.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_hoareTime_quartic_internal (phi : CNF) : validEmitterTM.HoareTime (validEmitterPre phi.encode) (StreamingStatePred (framedTokenInput phi.tokens []) (validEmitterFinalState phi)) (16384 * (phi.encode.length + 2) ^ 4)

Quartic-rounded typed-input specification for the concrete valid emitter.