Output-emission subroutines

Building blocks for machines that compute string functions (ComputesInTime): the output tape is treated as an append-only accumulator, written left to right. The central predicate OutAcc ys out says the output tape holds exactly the bits ys (after the ▷ at cell 0) with the head parked on the first blank, ready to append; emitters have Hoare specs of the shape

{OutAcc ys ∧ …} emit {OutAcc (ys ++ w) ∧ …}

which compose by seqTM along List.append associativity. The final bridge to ComputesInTime is OutAcc.hasOutput.

This layer is the foundation for the Cook–Levin reduction emitter (docs/A5-ReductionEmitter.md).

Main definitions

• TM.OutAcc — the output-accumulator predicate
• TM.bumpTM — entry adapter: bump every head from ▷ to cell 1
• TM.emitBitsTM — append a fixed word to the output
• TM.emitUnaryTM — append a register's value as a doubled-unary run
• TM.emitLitTM — append one encoded literal (sign bits, unary body, terminator)

Main results

• TM.OutAcc.hasOutput — accumulated output is HasOutput
• TM.OutAcc.eq — the accumulated word uniquely determines its output tape
• TM.outAcc_append_bit — one writeAndMove _ .right extends the accumulator
• TM.emitBitsTM_reachesIn_frame — exact emission with a complete input/work frame
• TM.emitBitsTM_hoareTime — emitBitsTM w appends w in |w| steps, preserving the input and work tapes
• TM.emitBitsTM_isTransducer — fixed-word emission never moves output left

def Complexity.TM.OutAcc (ys : List Bool) (out : Tape) : Prop

Output accumulator. The output tape holds exactly the bits ys (cells 1..|ys|, after the ▷ at cell 0), all cells beyond are blank, and the head is parked on the first blank — ready to append.

Equations

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

theorem Complexity.TM.OutAcc.head_eq {ys : List Bool} {out : Tape} (h : OutAcc ys out) : out.head = ys.length + 1

The accumulator head sits just past the |ys| stored bits, at cell |ys| + 1.

theorem Complexity.TM.OutAcc.read_blank {ys : List Bool} {out : Tape} (h : OutAcc ys out) : out.read = Γ.blank

The accumulator reads the first blank.

theorem Complexity.TM.OutAcc.parked {ys : List Bool} {out : Tape} (h : OutAcc ys out) : Parked out

An accumulator tape is parked (bits and blanks are never ▷).

theorem Complexity.TM.OutAcc.hasOutput {ys : List Bool} {out : Tape} (h : OutAcc ys out) : out.HasOutput ys

The bridge to ComputesInTime: an accumulated output HasOutput its bits.

theorem Complexity.TM.OutAcc.eq {ys : List Bool} {first second : Tape} (hfirst : OutAcc ys first) (hsecond : OutAcc ys second) : first = second

An output accumulator is uniquely determined by its accumulated word.

theorem Complexity.TM.outAcc_nil_init : OutAcc [] { head := 1, cells := (Tape.init []).cells }

The empty accumulator: a blank output tape with the head bumped to cell 1.

theorem Complexity.TM.outAcc_append_bit {ys : List Bool} {out : Tape} (h : OutAcc ys out) (b : Bool) : OutAcc (ys ++ [b]) (out.writeAndMove (Γ.ofBool b) Dir3.right)

Appending one bit. Writing Γ.ofBool b at the accumulator head and moving right extends the accumulator by b.

inductive Complexity.TM.BumpPhase : Type

The two states of bumpTM: go (initial, about to bump every head right) and done (halted).

• go : BumpPhase
• done : BumpPhase

@[instance_reducible]

instance Complexity.TM.instDecidableEqBumpPhase : DecidableEq BumpPhase

Equations

• Complexity.TM.instDecidableEqBumpPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.TM.instFintypeBumpPhase : Fintype BumpPhase

BumpPhase is a finite type, as required for TM state spaces.

Equations

• Complexity.TM.instFintypeBumpPhase = { elems := {Complexity.TM.BumpPhase.go, Complexity.TM.BumpPhase.done}, complete := ⋯ }

def Complexity.TM.bumpTM {n : ℕ} : TM n

Entry adapter: one step moving every head from ▷ (cell 0, the initial configuration) to cell 1, establishing the parked discipline: blank work tapes become zero registers and the blank output becomes the empty accumulator.

Equations

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

theorem Complexity.TM.parked_init_input (x : List Bool) : Parked { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells }

The input tape of the initial configuration, bumped to cell 1, is parked.

theorem Complexity.TM.bumpTM_hoareTime {n : ℕ} (x : List Bool) : bumpTM.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (∀ (i : Fin n), work i = Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } ∧ (∀ (i : Fin n), IsReg 0 (work i)) ∧ OutAcc [] out) 1

bumpTM Hoare specification. From the initial configuration's tapes, one step establishes: parked input (cells intact), zero registers on all work tapes, and the empty output accumulator.

def Complexity.TM.emitBitsTM {n : ℕ} (w : List Bool) : TM n

Append the fixed word w to the output and halt. State k = number of bits already emitted; each step writes bit k and moves the output head right; input and work tapes are parked and untouched.

Equations

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

theorem Complexity.TM.emitBitsTM_reachesIn_frame {n : ℕ} (w : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hout₀ : OutAcc ys out₀) : ∃ (c' : Cfg n (emitBitsTM w).Q), (emitBitsTM w).reachesIn w.length { state := (emitBitsTM w).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (emitBitsTM w).halted c' ∧ c'.input = inp₀ ∧ c'.work = work₀ ∧ OutAcc (ys ++ w) c'.output

Exact fixed-word emission appends w, preserves the complete input/work frame, and reaches the halt state in exactly |w| steps.

theorem Complexity.TM.emitBitsTM_isTransducer {n : ℕ} (w : List Bool) : (emitBitsTM w).IsTransducer

Fixed-word emission satisfies the one-way-output transducer discipline.

theorem Complexity.TM.emitBitsTM_hoareTime {n : ℕ} (w : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) : (emitBitsTM w).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ OutAcc ys out) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ OutAcc (ys ++ w) out) w.length

emitBitsTM Hoare specification. Appends the word w to the output accumulator in |w| steps, leaving the (parked) input and work tapes literally unchanged. Ghost-parametrized by the initial tapes for seqTM composition.

inductive Complexity.TM.EmitUnaryPhase : Type

The states of emitUnaryTM: emitA/emitB alternate to emit two trues per register mark, back rewinds the register head to ▷, park steps it to cell 1, and done halts.

• emitA : EmitUnaryPhase
• emitB : EmitUnaryPhase
• back : EmitUnaryPhase
• park : EmitUnaryPhase
• done : EmitUnaryPhase

@[instance_reducible]

instance Complexity.TM.instDecidableEqEmitUnaryPhase : DecidableEq EmitUnaryPhase

Equations

• Complexity.TM.instDecidableEqEmitUnaryPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.TM.instFintypeEmitUnaryPhase : Fintype EmitUnaryPhase

EmitUnaryPhase is a finite type, as required for TM state spaces.

Equations

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

def Complexity.TM.emitUnaryTM {n : ℕ} (r : Fin n) : TM n

Append 2v trues to the output, where v is the value of register r (the doubled-unary body doubleBits (Unary.encode v) of a literal's variable index), restoring the register exactly. The head sweeps right over the register's marks emitting two trues per mark (emitA/emitB), then rewinds to cell 1 (back/park).

Equations

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

theorem Complexity.TM.emitUnaryTM_hoareTime {n : ℕ} (r : Fin n) (v : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), i ≠ r → Parked (work₀ i)) (hreg : IsReg v (work₀ r)) : (emitUnaryTM r).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ OutAcc ys out) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ OutAcc (ys ++ List.replicate (2 * v) true) out) (3 * v + 3)

emitUnaryTM Hoare specification. Appends 2v trues (the doubled unary body of a literal with variable index v) to the output accumulator in 3v + 3 steps, restoring all tapes exactly: the scanned register r included.

def Complexity.TM.EmitPred {n : ℕ} (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) : TapePred n

The standard emit-spec shape: ghost-fixed input and work tapes, output accumulator holding ys.

Equations

• Complexity.TM.EmitPred inp₀ work₀ ys inp work out = (inp = inp₀ ∧ work = work₀ ∧ Complexity.TM.OutAcc ys out)

theorem Complexity.TM.emitPred_transition {n : ℕ} {inp₀ : Tape} {work₀ : Fin n → Tape} (hinp₀ : Parked inp₀) (hworkAll : ∀ (i : Fin n), Parked (work₀ i)) (ys : List Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) : EmitPred inp₀ work₀ ys inp work out → EmitPred inp₀ work₀ ys (transitionInput inp) (fun (i : Fin n) => transitionTape (work i)) (transitionTape out)

Emit-spec states pass through combinator phase boundaries unchanged: parked ghosts and the accumulator are fixed points of transitionTape / transitionInput. The h_trans obligation of seqTM_hoareTime for any two composed emitters.

def Complexity.TM.emitLitTM {n : ℕ} (s : Bool) (r : Fin n) : TM n

Append one encoded literal with sign s and variable index read from register r: the bits [s, s] ++ (2v trues) ++ [false, true] (= doubleBits (Lit.encodeRaw ⟨s, v⟩) ++ [false, true], the form literals take inside Clause.encode).

Equations

• Complexity.TM.emitLitTM s r = (Complexity.TM.emitBitsTM [s, s]).seqTM ((Complexity.TM.emitUnaryTM r).seqTM (Complexity.TM.emitBitsTM [false, true]))

theorem Complexity.TM.emitLitTM_hoareTime {n : ℕ} (s : Bool) (r : Fin n) (v : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), i ≠ r → Parked (work₀ i)) (hreg : IsReg v (work₀ r)) : (emitLitTM s r).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ work₀ (ys ++ ([s, s] ++ List.replicate (2 * v) true ++ [false, true]))) (3 * v + 9)

emitLitTM Hoare specification. Appends the encoded literal in 3v + 9 steps, preserving the input and work tapes (the scanned register included). The first seqTM-composed emitter spec; later emitters chain the same way.