Browse chapters

Imports

import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.ValidityTail
import Mathlib.Tactic

Runtime cell-progression source for validity-row tails

The post-halted part of a Cook--Levin validity row contains, for every fixed stack, a runtime-height family of cell frames. Their three operands evolve simultaneously: right increases by six, left decreases by one, and blank increases by one fixed alphabet width.

This file begins the complete tail-family source with the irreducible runtime kernel. The loop count is represented by actual input ticks, while the three operand values occupy the three unary counters. Thus all four runtime values remain tape data and only the fixed blank stride occurs in finite control.

              noncomputable sectionopen StateTransitionnamespace CLRS.Chapter34.Turing.PolyBuilder

Exact ordered cell frames generated by the mixed increasing/decreasing runtime progression.

def affineCellProgressionFrames (blankStep : Nat) :
    Nat → Nat → Nat → Nat → List AffineCellFrame
  | 0, _, _, _ => []
  | count + 1, right, left, blank =>
      { right := right, left := left, blank := blank } ::
        affineCellProgressionFrames blankStep count
          (right + 6) (left - 1) (blank + blankStep)

Public one-step equation used when connecting the progression to the canonical arithmetic stack-cell family.

theorem affineCellProgressionFrames_succ
    (blankStep count right left blank : Nat) :
    affineCellProgressionFrames blankStep (count + 1) right left blank =
      { right := right, left := left, blank := blank } ::
        affineCellProgressionFrames blankStep count
          (right + 6) (left - 1) (blank + blankStep) := by
  rfl

Closed positional form of the three mixed arithmetic progressions.


theorem affineCellProgressionFrames_eq_ofFn
    (blankStep count right left blank : Nat) :
    affineCellProgressionFrames blankStep count right left blank =
      List.ofFn fun index : Fin count =>
        ({ right := right + 6 * index.val
           left := left - index.val
           blank := blank + blankStep * index.val } : AffineCellFrame) := by
  induction count generalizing right left blank with
  | zero => rfl
  | succ count ih =>
      rw [affineCellProgressionFrames, List.ofFn_succ]
      congr 1
      rw [ih]
      apply List.ofFn_inj.mpr
      funext index
      simp only [Fin.val_succ]
      simp only [AffineCellFrame.mk.injEq]
      constructor
      · ring
      constructor
      · omega
      · ring

Finite control of the loaded three-counter cell source.

inductive AffineCellProgressionSourceLabel (blankStep : Nat)
  | loop
  | emitRight | saveRight | pushRightTick | pushRightSeparator
  | restoreRight | restoreRightInc
  | emitLeft | saveLeft | pushLeftTick | pushLeftSeparator
  | restoreLeft | restoreLeftInc
  | emitBlank | saveBlank | pushBlankTick | pushBlankSeparator
  | restoreBlank | restoreBlankInc
  | addRight₁ | addRight₂ | addRight₃ | addRight₄ | addRight₅ | addRight₆
  | decLeft
  | addBlank (remaining : Fin (blankStep + 1))
  | resetTest
  | finish | invalid
deriving DecidableEq, Fintype

private def affineCellProgressionSourcePred {blankStep : Nat}
    (remaining : Fin (blankStep + 1)) (_hpositive : remaining.val ≠ 0) :
    Fin (blankStep + 1) :=
  ⟨remaining.val - 1, by omega⟩

Fixed reverse-output controller. The remaining runtime cell count is a literal tick stream terminated by frameEnd; the operand counters are loaded by the surrounding stack source.

def affineCellProgressionSourceRevProgram (blankStep : Nat) :
    Program UnaryFrameSym UnaryFrameSym where
  Label := AffineCellProgressionSourceLabel blankStep
  main := .loop
  op
    | .loop => .popInput .invalid fun
        | .tick => .emitRight
        | .frameEnd => .finish
        | .separator => .invalid
    | .emitRight => .dec₁ .pushRightSeparator .saveRight
    | .saveRight => .pushWork₁ .tick .pushRightTick
    | .pushRightTick => .pushOutput .tick .emitRight
    | .pushRightSeparator => .pushOutput .separator .restoreRight
    | .restoreRight => .popWork₁ .emitLeft fun
        | .tick => .restoreRightInc
        | _ => .emitLeft
    | .restoreRightInc => .inc₁ .restoreRight
    | .emitLeft => .dec₂ .pushLeftSeparator .saveLeft
    | .saveLeft => .pushWork₁ .tick .pushLeftTick
    | .pushLeftTick => .pushOutput .tick .emitLeft
    | .pushLeftSeparator => .pushOutput .separator .restoreLeft
    | .restoreLeft => .popWork₁ .emitBlank fun
        | .tick => .restoreLeftInc
        | _ => .emitBlank
    | .restoreLeftInc => .inc₂ .restoreLeft
    | .emitBlank => .dec₃ .pushBlankSeparator .saveBlank
    | .saveBlank => .pushWork₁ .tick .pushBlankTick
    | .pushBlankTick => .pushOutput .tick .emitBlank
    | .pushBlankSeparator => .pushOutput .separator .restoreBlank
    | .restoreBlank => .popWork₁ .addRight₁ fun
        | .tick => .restoreBlankInc
        | _ => .addRight₁
    | .restoreBlankInc => .inc₃ .restoreBlank
    | .addRight₁ => .inc₁ .addRight₂
    | .addRight₂ => .inc₁ .addRight₃
    | .addRight₃ => .inc₁ .addRight₄
    | .addRight₄ => .inc₁ .addRight₅
    | .addRight₅ => .inc₁ .addRight₆
    | .addRight₆ => .inc₁ .decLeft
    | .decLeft => .dec₂
        (.addBlank ⟨blankStep, by omega⟩)
        (.addBlank ⟨blankStep, by omega⟩)
    | .addBlank remaining =>
        if h : remaining.val = 0 then
          .inc₁ .resetTest
        else
          .inc₃ (.addBlank
            (affineCellProgressionSourcePred remaining h))
    | .resetTest => .dec₁ .loop .loop
    | .finish => .halt
    | .invalid => .halt

private def affineCellProgressionSourceCfg {blankStep : Nat}
    (label : AffineCellProgressionSourceLabel blankStep)
    (buffer₁ : Option UnaryFrameSym) (test : Bool)
    (input output work₁ : List UnaryFrameSym)
    (right left blank : List Unit) :
    BuilderCfg (affineCellProgressionSourceRevProgram blankStep) where
  label := some label
  buffer₁ := buffer₁
  buffer₂ := none
  test := test
  input := input
  output := output
  work₁ := work₁
  work₂ := []
  counter₁ := right
  counter₂ := left
  counter₃ := blank

Loaded entry: the three operand bases are counters and exactly count input ticks control the family loop.

def affineCellProgressionSourceLoadedCfg
    (blankStep count right left blank : Nat)
    (output : List UnaryFrameSym) :
    BuilderCfg (affineCellProgressionSourceRevProgram blankStep) :=
  affineCellProgressionSourceCfg .loop none false
    (List.replicate count .tick ++ [.frameEnd]) output []
    (List.replicate right ()) (List.replicate left ())
    (List.replicate blank ())

The loop test is irrelevant to the next cell, but is part of the exact configuration. An empty family preserves its incoming test; every productive family normalizes it to true before the next loop entry.

def affineCellProgressionSourceFinishTest : Nat → Bool → Bool
  | 0, test => test
  | _ + 1, _ => true

Public continuation after consuming the runtime cell-count sentinel.

def affineCellProgressionSourceFinishCfg
    (blankStep count right left blank : Nat)
    (output : List UnaryFrameSym) :
    BuilderCfg (affineCellProgressionSourceRevProgram blankStep) :=
  affineCellProgressionSourceCfg .finish (some .frameEnd)
    (affineCellProgressionSourceFinishTest count false) [] output []
    (List.replicate (right + 6 * count) ())
    (List.replicate (left - count) ())
    (List.replicate (blank + blankStep * count) ())

              private theorem tailCell_replicate_append_cons {α : Type}
    (value : α) (count : Nat) (tail : List α) :
    List.replicate count value ++ value :: tail =
      value :: (List.replicate count value ++ tail) := by
  induction count with
  | zero => rfl
  | succ count ih =>
      simp only [List.replicate_succ, List.cons_append]
      exact congrArg (List.cons value) ih

private theorem tailCell_emitRight_eval {blankStep : Nat} (value : Nat)
    (buffer₁ : Option UnaryFrameSym) (test : Bool)
    (input output work₁ : List UnaryFrameSym)
    (left blank : List Unit) :
    (flip Option.bind
      (step (affineCellProgressionSourceRevProgram blankStep)))^[3 * value + 1]
      (some (affineCellProgressionSourceCfg .emitRight buffer₁ test
        input output work₁ (List.replicate value ()) left blank)) =
      some (affineCellProgressionSourceCfg .pushRightSeparator buffer₁ false
        input (List.replicate value .tick ++ output)
        (List.replicate value .tick ++ work₁) [] left blank) := by
  induction value generalizing test output work₁ with
  | zero => rfl
  | succ value ih =>
      rw [show 3 * (value + 1) + 1 = (3 * value + 1) + 1 + 1 + 1 by
          omega,
        Function.iterate_succ_apply, Function.iterate_succ_apply,
        Function.iterate_succ_apply]
      change
        (flip Option.bind
          (step (affineCellProgressionSourceRevProgram blankStep)))^[3 * value + 1]
          (some (affineCellProgressionSourceCfg .emitRight buffer₁ true input
            (.tick :: output) (.tick :: work₁) (List.replicate value ())
            left blank)) = _
      simpa only [List.replicate_succ, tailCell_replicate_append_cons,
        List.cons_append] using ih true (.tick :: output) (.tick :: work₁)

private theorem tailCell_restoreRight_eval {blankStep : Nat} (value : Nat)
    (buffer₁ : Option UnaryFrameSym) (test : Bool)
    (input output : List UnaryFrameSym) (current left blank : List Unit) :
    (flip Option.bind
      (step (affineCellProgressionSourceRevProgram blankStep)))^[2 * value + 1]
      (some (affineCellProgressionSourceCfg .restoreRight buffer₁ test
        input output (List.replicate value .tick) current left blank)) =
      some (affineCellProgressionSourceCfg .emitLeft none test input output []
        (List.replicate value () ++ current) left blank) := by
  induction value generalizing buffer₁ current with
  | zero => rfl
  | succ value ih =>
      rw [show 2 * (value + 1) + 1 = (2 * value + 1) + 1 + 1 by omega,
        Function.iterate_succ_apply, Function.iterate_succ_apply]
      change
        (flip Option.bind
          (step (affineCellProgressionSourceRevProgram blankStep)))^[2 * value + 1]
          (some (affineCellProgressionSourceCfg .restoreRight (some .tick)
            test input output (List.replicate value .tick) (() :: current)
            left blank)) = _
      simpa only [List.replicate_succ, tailCell_replicate_append_cons,
        List.cons_append] using ih (some .tick) (() :: current)

private theorem tailCell_emitLeft_eval {blankStep : Nat} (value : Nat)
    (buffer₁ : Option UnaryFrameSym) (test : Bool)
    (input output work₁ : List UnaryFrameSym)
    (right blank : List Unit) :
    (flip Option.bind
      (step (affineCellProgressionSourceRevProgram blankStep)))^[3 * value + 1]
      (some (affineCellProgressionSourceCfg .emitLeft buffer₁ test input
        output work₁ right (List.replicate value ()) blank)) =
      some (affineCellProgressionSourceCfg .pushLeftSeparator buffer₁ false
        input (List.replicate value .tick ++ output)
        (List.replicate value .tick ++ work₁) right [] blank) := by
  induction value generalizing test output work₁ with
  | zero => rfl
  | succ value ih =>
      rw [show 3 * (value + 1) + 1 = (3 * value + 1) + 1 + 1 + 1 by
          omega,
        Function.iterate_succ_apply, Function.iterate_succ_apply,
        Function.iterate_succ_apply]
      change
        (flip Option.bind
          (step (affineCellProgressionSourceRevProgram blankStep)))^[3 * value + 1]
          (some (affineCellProgressionSourceCfg .emitLeft buffer₁ true input
            (.tick :: output) (.tick :: work₁) right
            (List.replicate value ()) blank)) = _
      simpa only [List.replicate_succ, tailCell_replicate_append_cons,
        List.cons_append] using ih true (.tick :: output) (.tick :: work₁)

private theorem tailCell_restoreLeft_eval {blankStep : Nat} (value : Nat)
    (buffer₁ : Option UnaryFrameSym) (test : Bool)
    (input output : List UnaryFrameSym) (right current blank : List Unit) :
    (flip Option.bind
      (step (affineCellProgressionSourceRevProgram blankStep)))^[2 * value + 1]
      (some (affineCellProgressionSourceCfg .restoreLeft buffer₁ test input
        output (List.replicate value .tick) right current blank)) =
      some (affineCellProgressionSourceCfg .emitBlank none test input output []
        right (List.replicate value () ++ current) blank) := by
  induction value generalizing buffer₁ current with
  | zero => rfl
  | succ value ih =>
      rw [show 2 * (value + 1) + 1 = (2 * value + 1) + 1 + 1 by omega,
        Function.iterate_succ_apply, Function.iterate_succ_apply]
      change
        (flip Option.bind
          (step (affineCellProgressionSourceRevProgram blankStep)))^[2 * value + 1]
          (some (affineCellProgressionSourceCfg .restoreLeft (some .tick)
            test input output (List.replicate value .tick) right
            (() :: current) blank)) = _
      simpa only [List.replicate_succ, tailCell_replicate_append_cons,
        List.cons_append] using ih (some .tick) (() :: current)

private theorem tailCell_emitBlank_eval {blankStep : Nat} (value : Nat)
    (buffer₁ : Option UnaryFrameSym) (test : Bool)
    (input output work₁ : List UnaryFrameSym)
    (right left : List Unit) :
    (flip Option.bind
      (step (affineCellProgressionSourceRevProgram blankStep)))^[3 * value + 1]
      (some (affineCellProgressionSourceCfg .emitBlank buffer₁ test input
        output work₁ right left (List.replicate value ()))) =
      some (affineCellProgressionSourceCfg .pushBlankSeparator buffer₁ false
        input (List.replicate value .tick ++ output)
        (List.replicate value .tick ++ work₁) right left []) := by
  induction value generalizing test output work₁ with
  | zero => rfl
  | succ value ih =>
      rw [show 3 * (value + 1) + 1 = (3 * value + 1) + 1 + 1 + 1 by
          omega,
        Function.iterate_succ_apply, Function.iterate_succ_apply,
        Function.iterate_succ_apply]
      change
        (flip Option.bind
          (step (affineCellProgressionSourceRevProgram blankStep)))^[3 * value + 1]
          (some (affineCellProgressionSourceCfg .emitBlank buffer₁ true input
            (.tick :: output) (.tick :: work₁) right left
            (List.replicate value ()))) = _
      simpa only [List.replicate_succ, tailCell_replicate_append_cons,
        List.cons_append] using ih true (.tick :: output) (.tick :: work₁)

private theorem tailCell_restoreBlank_eval {blankStep : Nat} (value : Nat)
    (buffer₁ : Option UnaryFrameSym) (test : Bool)
    (input output : List UnaryFrameSym) (right left current : List Unit) :
    (flip Option.bind
      (step (affineCellProgressionSourceRevProgram blankStep)))^[2 * value + 1]
      (some (affineCellProgressionSourceCfg .restoreBlank buffer₁ test input
        output (List.replicate value .tick) right left current)) =
      some (affineCellProgressionSourceCfg .addRight₁ none test input output []
        right left (List.replicate value () ++ current)) := by
  induction value generalizing buffer₁ current with
  | zero => rfl
  | succ value ih =>
      rw [show 2 * (value + 1) + 1 = (2 * value + 1) + 1 + 1 by omega,
        Function.iterate_succ_apply, Function.iterate_succ_apply]
      change
        (flip Option.bind
          (step (affineCellProgressionSourceRevProgram blankStep)))^[2 * value + 1]
          (some (affineCellProgressionSourceCfg .restoreBlank (some .tick)
            test input output (List.replicate value .tick) right left
            (() :: current))) = _
      simpa only [List.replicate_succ, tailCell_replicate_append_cons,
        List.cons_append] using ih (some .tick) (() :: current)

private theorem tailCell_addBlankFrom_eval (blankStep remaining : Nat)
    (hremaining : remaining < blankStep + 1) (test : Bool)
    (input output : List UnaryFrameSym) (right left blank : List Unit) :
    (flip Option.bind
      (step (affineCellProgressionSourceRevProgram blankStep)))^[remaining + 2]
      (some (affineCellProgressionSourceCfg
        (.addBlank ⟨remaining, hremaining⟩) none test input output []
        right left blank)) =
      some (affineCellProgressionSourceCfg .loop none true input output []
        right left (List.replicate remaining () ++ blank)) := by
  induction remaining generalizing blank test with
  | zero => rfl
  | succ remaining ih =>
      rw [show remaining + 1 + 2 = (remaining + 2) + 1 by omega,
        Function.iterate_succ_apply]
      change
        (flip Option.bind (step
          (affineCellProgressionSourceRevProgram blankStep)))^[remaining + 2]
          (some (affineCellProgressionSourceCfg
            (.addBlank ⟨remaining, by omega⟩) none test input output []
            right left (() :: blank))) = _
      have lifted := ih (by omega) test (() :: blank)
      simpa only [List.replicate_succ, tailCell_replicate_append_cons,
        List.cons_append] using liftedprivate theorem tailCell_addBlank_eval (blankStep : Nat) (test : Bool)
    (input output : List UnaryFrameSym) (right left blank : List Unit) :
    (flip Option.bind
      (step (affineCellProgressionSourceRevProgram blankStep)))^[blankStep + 2]
      (some (affineCellProgressionSourceCfg
        (.addBlank ⟨blankStep, by omega⟩) none test input output []
        right left blank)) =
      some (affineCellProgressionSourceCfg .loop none true input output []
        right left (List.replicate blankStep () ++ blank)) :=
  tailCell_addBlankFrom_eval blankStep blankStep (by omega) test
    input output right left blank

Exact productive cost of one cell frame, starting after the loop tick has been consumed and ending at the next loop test.

def affineCellProgressionSourceGroupSteps
    (blankStep right left blank : Nat) : Nat :=
  5 * (right + left + blank) + blankStep + 18



private def affineCellProgressionSource_runGroup
    (blankStep right left blank : Nat) (initialTest : Bool)
    (input output : List UnaryFrameSym) :
    EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep))
      (affineCellProgressionSourceCfg .emitRight (some .tick) initialTest
        input output [] (List.replicate right ())
        (List.replicate left ()) (List.replicate blank ()))
      (some (affineCellProgressionSourceCfg .loop none true input
        ((encodeAffineCellFrame
          { right := right, left := left, blank := blank }).reverse ++ output)
        [] (List.replicate (right + 6) ())
        (List.replicate (left - 1) ())
        (List.replicate (blank + blankStep) ())))
      (affineCellProgressionSourceGroupSteps
        blankStep right left blank) := by
  let afterRight := affineCellProgressionSourceCfg
    (blankStep := blankStep) .pushRightSeparator (some .tick) false input
    (List.replicate right .tick ++ output)
    (List.replicate right .tick) [] (List.replicate left ())
    (List.replicate blank ())
  let beforeRestoreRight := affineCellProgressionSourceCfg
    (blankStep := blankStep) .restoreRight (some .tick) false input
    (.separator :: (List.replicate right .tick ++ output))
    (List.replicate right .tick) [] (List.replicate left ())
    (List.replicate blank ())
  let beforeLeft := affineCellProgressionSourceCfg
    (blankStep := blankStep) .emitLeft none false input
    (.separator :: (List.replicate right .tick ++ output)) []
    (List.replicate right ()) (List.replicate left ())
    (List.replicate blank ())
  let afterLeft := affineCellProgressionSourceCfg
    (blankStep := blankStep) .pushLeftSeparator none false input
    (List.replicate left .tick ++
      .separator :: (List.replicate right .tick ++ output))
    (List.replicate left .tick) (List.replicate right ()) []
    (List.replicate blank ())
  let beforeRestoreLeft := affineCellProgressionSourceCfg
    (blankStep := blankStep) .restoreLeft none false input
    (.separator :: (List.replicate left .tick ++
      .separator :: (List.replicate right .tick ++ output)))
    (List.replicate left .tick) (List.replicate right ()) []
    (List.replicate blank ())
  let beforeBlank := affineCellProgressionSourceCfg
    (blankStep := blankStep) .emitBlank none false input
    (.separator :: (List.replicate left .tick ++
      .separator :: (List.replicate right .tick ++ output))) []
    (List.replicate right ()) (List.replicate left ())
    (List.replicate blank ())
  let afterBlank := affineCellProgressionSourceCfg
    (blankStep := blankStep) .pushBlankSeparator none false input
    (List.replicate blank .tick ++
      .separator :: (List.replicate left .tick ++
        .separator :: (List.replicate right .tick ++ output)))
    (List.replicate blank .tick) (List.replicate right ())
    (List.replicate left ()) []
  let beforeRestoreBlank := affineCellProgressionSourceCfg
    (blankStep := blankStep) .restoreBlank none false input
    (.separator :: (List.replicate blank .tick ++
      .separator :: (List.replicate left .tick ++
        .separator :: (List.replicate right .tick ++ output))))
    (List.replicate blank .tick) (List.replicate right ())
    (List.replicate left ()) []
  let beforeOffsets := affineCellProgressionSourceCfg
    (blankStep := blankStep) .addRight₁ none false input
    (.separator :: (List.replicate blank .tick ++
      .separator :: (List.replicate left .tick ++
        .separator :: (List.replicate right .tick ++ output)))) []
    (List.replicate right ()) (List.replicate left ())
    (List.replicate blank ())
  let beforeDecLeft := affineCellProgressionSourceCfg
    (blankStep := blankStep) .decLeft none false input
    (.separator :: (List.replicate blank .tick ++
      .separator :: (List.replicate left .tick ++
        .separator :: (List.replicate right .tick ++ output)))) []
    (() :: () :: () :: () :: () :: () :: List.replicate right ())
    (List.replicate left ())
    (List.replicate blank ())
  have hright : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep))
      (affineCellProgressionSourceCfg .emitRight (some .tick) initialTest
        input output [] (List.replicate right ())
        (List.replicate left ()) (List.replicate blank ()))
      (some afterRight) (3 * right + 1) := by
    refine ⟨⟨3 * right + 1, ?_⟩, le_rfl⟩
    simpa [afterRight] using tailCell_emitRight_eval
      (blankStep := blankStep) right (some .tick) initialTest input output []
      (List.replicate left ()) (List.replicate blank ())
  have hrightSep : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep)) afterRight
      (some beforeRestoreRight) 1 := ⟨⟨1, rfl⟩, le_rfl⟩
  have hrestoreRight : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep))
      beforeRestoreRight (some beforeLeft) (2 * right + 1) := by
    refine ⟨⟨2 * right + 1, ?_⟩, le_rfl⟩
    simpa [beforeRestoreRight, beforeLeft] using tailCell_restoreRight_eval
      (blankStep := blankStep) right (some .tick) false input
      (.separator :: (List.replicate right .tick ++ output)) []
      (List.replicate left ()) (List.replicate blank ())
  have hleft : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep)) beforeLeft
      (some afterLeft) (3 * left + 1) := by
    refine ⟨⟨3 * left + 1, ?_⟩, le_rfl⟩
    simpa [beforeLeft, afterLeft] using tailCell_emitLeft_eval
      (blankStep := blankStep) left none false input
      (.separator :: (List.replicate right .tick ++ output)) []
      (List.replicate right ()) (List.replicate blank ())
  have hleftSep : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep)) afterLeft
      (some beforeRestoreLeft) 1 := ⟨⟨1, rfl⟩, le_rfl⟩
  have hrestoreLeft : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep))
      beforeRestoreLeft (some beforeBlank) (2 * left + 1) := by
    refine ⟨⟨2 * left + 1, ?_⟩, le_rfl⟩
    simpa [beforeRestoreLeft, beforeBlank] using tailCell_restoreLeft_eval
      (blankStep := blankStep) left none false input
      (.separator :: (List.replicate left .tick ++
        .separator :: (List.replicate right .tick ++ output)))
      (List.replicate right ()) [] (List.replicate blank ())
  have hblank : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep)) beforeBlank
      (some afterBlank) (3 * blank + 1) := by
    refine ⟨⟨3 * blank + 1, ?_⟩, le_rfl⟩
    simpa [beforeBlank, afterBlank] using tailCell_emitBlank_eval
      (blankStep := blankStep) blank none false input
      (.separator :: (List.replicate left .tick ++
        .separator :: (List.replicate right .tick ++ output))) []
      (List.replicate right ()) (List.replicate left ())
  have hblankSep : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep)) afterBlank
      (some beforeRestoreBlank) 1 := ⟨⟨1, rfl⟩, le_rfl⟩
  have hrestoreBlank : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep))
      beforeRestoreBlank (some beforeOffsets) (2 * blank + 1) := by
    refine ⟨⟨2 * blank + 1, ?_⟩, le_rfl⟩
    simpa [beforeRestoreBlank, beforeOffsets] using tailCell_restoreBlank_eval
      (blankStep := blankStep) blank none false input
      (.separator :: (List.replicate blank .tick ++
        .separator :: (List.replicate left .tick ++
          .separator :: (List.replicate right .tick ++ output))))
      (List.replicate right ()) (List.replicate left ()) []
  have hoffsets : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep)) beforeOffsets
      (some beforeDecLeft) 6 := by
    refine ⟨⟨6, ?_⟩, le_rfl⟩
    change
      (flip Option.bind
        (step (affineCellProgressionSourceRevProgram blankStep)))^[6]
        (some beforeOffsets) = some beforeDecLeft
    simp only [show 6 = 1 + 1 + 1 + 1 + 1 + 1 by omega,
      Function.iterate_add_apply]
    rfl
  have hleftBlankOffset : EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep))
      beforeDecLeft
      (some (affineCellProgressionSourceCfg .loop none true input
        (.separator :: (List.replicate blank .tick ++
          .separator :: (List.replicate left .tick ++
            .separator :: (List.replicate right .tick ++ output)))) []
        (() :: () :: () :: () :: () :: () :: List.replicate right ())
        (List.replicate (left - 1) ())
        (List.replicate (blank + blankStep) ())))
      (blankStep + 3) := by
    cases left with
    | zero =>
        have hdec : EvalsToInTime
            (step (affineCellProgressionSourceRevProgram blankStep))
            beforeDecLeft
            (some (affineCellProgressionSourceCfg
              (.addBlank ⟨blankStep, by omega⟩) none false input
              (.separator :: (List.replicate blank .tick ++
                .separator :: (List.replicate 0 .tick ++
                  .separator :: (List.replicate right .tick ++ output)))) []
              (() :: () :: () :: () :: () :: () :: List.replicate right ()) []
              (List.replicate blank ()))) 1 := by
          refine ⟨⟨1, ?_⟩, le_rfl⟩
          rfl
        have hadd := tailCell_addBlank_eval blankStep false input
          (.separator :: (List.replicate blank .tick ++
            .separator :: (List.replicate 0 .tick ++
              .separator :: (List.replicate right .tick ++ output))))
          (() :: () :: () :: () :: () :: () :: List.replicate right ()) []
          (List.replicate blank ())
        let full := EvalsToInTime.trans
          (step (affineCellProgressionSourceRevProgram blankStep)) _ _ _ _ _
            hdec ⟨⟨blankStep + 2, hadd⟩, le_rfl⟩
        simpa only [List.replicate_zero, List.nil_append,
          List.replicate_append_replicate, Nat.zero_sub,
          show blankStep + blank = blank + blankStep by omega,
          show 1 + (blankStep + 2) = blankStep + 3 by omega] using full
    | succ left =>
        have hdec : EvalsToInTime
            (step (affineCellProgressionSourceRevProgram blankStep))
            beforeDecLeft
            (some (affineCellProgressionSourceCfg
              (.addBlank ⟨blankStep, by omega⟩) none true input
              (.separator :: (List.replicate blank .tick ++
                .separator :: (List.replicate (left + 1) .tick ++
                  .separator :: (List.replicate right .tick ++ output)))) []
              (() :: () :: () :: () :: () :: () :: List.replicate right ())
              (List.replicate left ())
              (List.replicate blank ()))) 1 := by
          refine ⟨⟨1, ?_⟩, le_rfl⟩
          rfl
        have hadd := tailCell_addBlank_eval blankStep true input
          (.separator :: (List.replicate blank .tick ++
            .separator :: (List.replicate (left + 1) .tick ++
              .separator :: (List.replicate right .tick ++ output))))
          (() :: () :: () :: () :: () :: () :: List.replicate right ())
          (List.replicate left ())
          (List.replicate blank ())
        let full := EvalsToInTime.trans
          (step (affineCellProgressionSourceRevProgram blankStep)) _ _ _ _ _
            hdec ⟨⟨blankStep + 2, hadd⟩, le_rfl⟩
        simpa only [List.replicate_append_replicate, Nat.add_sub_cancel,
          show blankStep + blank = blank + blankStep by omega,
          show 1 + (blankStep + 2) = blankStep + 3 by omega] using full
  let h₁ := EvalsToInTime.trans
    (step (affineCellProgressionSourceRevProgram blankStep)) _ 1 _ afterRight _
      hright hrightSep
  let h₂ := EvalsToInTime.trans
    (step (affineCellProgressionSourceRevProgram blankStep)) _ _ _
      beforeRestoreRight _ h₁ hrestoreRight
  let h₃ := EvalsToInTime.trans
    (step (affineCellProgressionSourceRevProgram blankStep)) _ _ _ beforeLeft _
      h₂ hleft
  let h₄ := EvalsToInTime.trans
    (step (affineCellProgressionSourceRevProgram blankStep)) _ 1 _ afterLeft _
      h₃ hleftSep
  let h₅ := EvalsToInTime.trans
    (step (affineCellProgressionSourceRevProgram blankStep)) _ _ _
      beforeRestoreLeft _ h₄ hrestoreLeft
  let h₆ := EvalsToInTime.trans
    (step (affineCellProgressionSourceRevProgram blankStep)) _ _ _ beforeBlank _
      h₅ hblank
  let h₇ := EvalsToInTime.trans
    (step (affineCellProgressionSourceRevProgram blankStep)) _ 1 _ afterBlank _
      h₆ hblankSep
  let h₈ := EvalsToInTime.trans
    (step (affineCellProgressionSourceRevProgram blankStep)) _ _ _
      beforeRestoreBlank _ h₇ hrestoreBlank
  let h₉ := EvalsToInTime.trans
    (step (affineCellProgressionSourceRevProgram blankStep)) _ 6 _
      beforeOffsets _ h₈ hoffsets
  let full := EvalsToInTime.trans
    (step (affineCellProgressionSourceRevProgram blankStep)) _ _ _
      beforeDecLeft _ h₉ hleftBlankOffset
  have hrightCounter :
      () :: () :: () :: () :: () :: () :: List.replicate right () =
        List.replicate (right + 6) () := by
    change List.replicate 6 () ++ List.replicate right () = _
    rw [List.replicate_append_replicate]
    congr 1
    omega
  rw [hrightCounter] at full
  convert full using 1
  · simp [encodeAffineCellFrame, encodeUnaryFrame, encodeUnaryFrameBlock,
      List.reverse_append, List.append_assoc]
  · simp [affineCellProgressionSourceGroupSteps]
    omega

Exact run time including one loop-input pop per cell and the final frameEnd pop.

def affineCellProgressionSourceSteps (blankStep : Nat) :
    Nat → Nat → Nat → Nat → Nat
  | 0, _, _, _ => 1
  | count + 1, right, left, blank =>
      1 + affineCellProgressionSourceGroupSteps blankStep right left blank +
        affineCellProgressionSourceSteps blankStep count
          (right + 6) (left - 1) (blank + blankStep)

A phase-sensitive bound that records the largest operand payload reached by the remaining mixed progression.


theorem affineCellProgressionSourceSteps_phase_le
    (blankStep count right left blank : Nat) :
    affineCellProgressionSourceSteps blankStep count right left blank ≤
      count *
        (5 * (right + left + blank + count * (6 + blankStep)) +
          blankStep + 19) + 1 := by
  induction count generalizing right left blank with
  | zero => simp [affineCellProgressionSourceSteps]
  | succ count ih =>
      simp only [affineCellProgressionSourceSteps]
      have hremaining := ih (right + 6) (left - 1) (blank + blankStep)
      have hleft : left - 1 ≤ left := Nat.sub_le left 1
      have hpayload :
          (right + 6) + (left - 1) + (blank + blankStep) +
              count * (6 + blankStep) ≤
            right + left + blank + (count + 1) * (6 + blankStep) := by
        nlinarith
      have hfactor :
          5 * ((right + 6) + (left - 1) + (blank + blankStep) +
              count * (6 + blankStep)) + blankStep + 19 ≤
            5 * (right + left + blank +
              (count + 1) * (6 + blankStep)) + blankStep + 19 := by
        omega
      calc
        1 + affineCellProgressionSourceGroupSteps blankStep right left blank +
            affineCellProgressionSourceSteps blankStep count
              (right + 6) (left - 1) (blank + blankStep) ≤
            1 + affineCellProgressionSourceGroupSteps blankStep right left blank +
              (count *
                (5 * ((right + 6) + (left - 1) + (blank + blankStep) +
                  count * (6 + blankStep)) + blankStep + 19) + 1) :=
          Nat.add_le_add_left hremaining _
        _ ≤ 1 + affineCellProgressionSourceGroupSteps blankStep right left blank +
              (count *
                (5 * (right + left + blank +
                  (count + 1) * (6 + blankStep)) + blankStep + 19) + 1) := by
          exact Nat.add_le_add_left
            (Nat.add_le_add_right (Nat.mul_le_mul_left count hfactor) 1) _
        _ ≤ (count + 1) *
              (5 * (right + left + blank +
                (count + 1) * (6 + blankStep)) + blankStep + 19) + 1 := by
          simp [affineCellProgressionSourceGroupSteps]
          nlinarith

Uniform quadratic runtime bound in the complete loaded unary payload. The fixed blank stride contributes only to the coefficient.


theorem affineCellProgressionSourceSteps_le
    (blankStep count right left blank : Nat) :
    affineCellProgressionSourceSteps blankStep count right left blank ≤
      60 * (blankStep + 1) *
        (count + right + left + blank + 1) ^ 2 := by
  let payload := count + right + left + blank + 1
  have hphase := affineCellProgressionSourceSteps_phase_le
    blankStep count right left blank
  have hpayload : 1 ≤ payload := by simp [payload]
  have hcount : count ≤ payload := by
    dsimp only [payload]
    omega
  have hbase : right + left + blank ≤ payload := by
    dsimp only [payload]
    omega
  have hstride : count * (6 + blankStep) ≤
      7 * (blankStep + 1) * payload := by
    have hmul := Nat.mul_le_mul_left (6 + blankStep) hcount
    nlinarith
  have hinside :
      right + left + blank + count * (6 + blankStep) ≤
        8 * (blankStep + 1) * payload := by
    nlinarith
  have hconstant : blankStep + 19 ≤
      19 * (blankStep + 1) * payload := by
    nlinarith
  have hfactor :
      5 * (right + left + blank + count * (6 + blankStep)) +
          blankStep + 19 ≤
        59 * (blankStep + 1) * payload := by
    nlinarith
  have hmain :
      count *
          (5 * (right + left + blank + count * (6 + blankStep)) +
            blankStep + 19) ≤
        59 * (blankStep + 1) * payload ^ 2 := by
    calc
      count *
          (5 * (right + left + blank + count * (6 + blankStep)) +
            blankStep + 19) ≤
          count * (59 * (blankStep + 1) * payload) :=
        Nat.mul_le_mul_left count hfactor
      _ ≤ 59 * (blankStep + 1) * payload ^ 2 := by
        have hmul := Nat.mul_le_mul_right
          (59 * (blankStep + 1) * payload) hcount
        nlinarith
  have hone : 1 ≤ (blankStep + 1) * payload ^ 2 := by
    nlinarith
  calc
    affineCellProgressionSourceSteps blankStep count right left blank ≤
        count *
          (5 * (right + left + blank + count * (6 + blankStep)) +
            blankStep + 19) + 1 := hphase
    _ ≤ 59 * (blankStep + 1) * payload ^ 2 +
          (blankStep + 1) * payload ^ 2 := Nat.add_le_add hmain hone
    _ = 60 * (blankStep + 1) * payload ^ 2 := by ring



private def affineCellProgressionSource_runFrom
    (blankStep count right left blank : Nat) (initialTest : Bool)
    (tail output : List UnaryFrameSym) :
    EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep))
      (affineCellProgressionSourceCfg .loop none initialTest
        (List.replicate count .tick ++ .frameEnd :: tail) output []
        (List.replicate right ()) (List.replicate left ())
        (List.replicate blank ()))
      (some (affineCellProgressionSourceCfg .finish (some .frameEnd)
        (affineCellProgressionSourceFinishTest count initialTest) tail
        ((encodeAffineCellFamily
          (affineCellProgressionFrames blankStep count
            right left blank)).reverse ++ output) []
        (List.replicate (right + 6 * count) ())
        (List.replicate (left - count) ())
        (List.replicate (blank + blankStep * count) ())))
      (affineCellProgressionSourceSteps blankStep count
        right left blank) := by
  induction count generalizing right left blank initialTest tail output with
  | zero =>
      refine ⟨⟨1, ?_⟩, le_rfl⟩
      rfl
  | succ count ih =>
      let restInput := List.replicate count UnaryFrameSym.tick ++
        UnaryFrameSym.frameEnd :: tail
      let loopAfterPop := affineCellProgressionSourceCfg
        (blankStep := blankStep) .emitRight (some .tick) initialTest
        restInput output []
        (List.replicate right ()) (List.replicate left ())
        (List.replicate blank ())
      have hpop : EvalsToInTime
          (step (affineCellProgressionSourceRevProgram blankStep))
          (affineCellProgressionSourceCfg .loop none initialTest
            (List.replicate (count + 1) .tick ++ .frameEnd :: tail) output []
            (List.replicate right ()) (List.replicate left ())
            (List.replicate blank ()))
          (some loopAfterPop) 1 := by
        refine ⟨⟨1, ?_⟩, le_rfl⟩
        rfl
      have hgroup := affineCellProgressionSource_runGroup
        blankStep right left blank initialTest restInput output
      have hrest := ih (right + 6) (left - 1) (blank + blankStep) true
        tail ((encodeAffineCellFrame
          { right := right, left := left, blank := blank }).reverse ++ output)
      let h₁ := EvalsToInTime.trans
        (step (affineCellProgressionSourceRevProgram blankStep)) _ _ _
          loopAfterPop _ hpop hgroup
      let full := EvalsToInTime.trans
        (step (affineCellProgressionSourceRevProgram blankStep)) _ _ _ _ _
          h₁ hrest
      convert full using 1
      · have hright : right + 6 * (count + 1) =
            right + 6 + 6 * count := by omega
        have hleft : left - (count + 1) = left - 1 - count := by omega
        have hblank : blank + blankStep * (count + 1) =
            blank + blankStep + blankStep * count := by ring
        have htest :
            affineCellProgressionSourceFinishTest (count + 1) initialTest =
              affineCellProgressionSourceFinishTest count true := by
          cases count <;> rfl
        simp [affineCellProgressionFrames, encodeAffineCellFamily,
          List.reverse_append, List.append_assoc, hright, hleft, hblank, htest]
      · simp [affineCellProgressionSourceSteps]
        omega

The fixed loaded controller emits exactly the reversed delimiter-bearing cell family and reaches a public continuation with all symbol work cleared.

def affineCellProgressionSource_runToFinish
    (blankStep count right left blank : Nat)
    (output : List UnaryFrameSym) :
    EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep))
      (affineCellProgressionSourceLoadedCfg blankStep count
        right left blank output)
      (some (affineCellProgressionSourceFinishCfg blankStep count
        right left blank
        ((encodeAffineCellFamily
          (affineCellProgressionFrames blankStep count
            right left blank)).reverse ++ output)))
      (affineCellProgressionSourceSteps blankStep count
        right left blank) := by
  simpa [affineCellProgressionSourceLoadedCfg,
    affineCellProgressionSourceFinishCfg] using
    affineCellProgressionSource_runFrom
      blankStep count right left blank false [] output

Contextual form of the loaded cell progression: the explicit sentinel is consumed while an arbitrary following invocation remains untouched.

def affineCellProgressionSource_runToFinishWithTail
    (blankStep count right left blank : Nat)
    (tail output : List UnaryFrameSym) :
    EvalsToInTime
      (step (affineCellProgressionSourceRevProgram blankStep))
      (affineCellProgressionSourceCfg .loop none false
        (List.replicate count .tick ++ .frameEnd :: tail) output []
        (List.replicate right ()) (List.replicate left ())
        (List.replicate blank ()))
      (some (affineCellProgressionSourceCfg .finish (some .frameEnd)
        (affineCellProgressionSourceFinishTest count false) tail
        ((encodeAffineCellFamily
          (affineCellProgressionFrames blankStep count
            right left blank)).reverse ++ output) []
        (List.replicate (right + 6 * count) ())
        (List.replicate (left - count) ())
        (List.replicate (blank + blankStep * count) ())))
      (affineCellProgressionSourceSteps blankStep count
        right left blank) :=
  affineCellProgressionSource_runFrom blankStep count right left blank false
    tail output

One complete loaded stack frame

Runtime operands for one stack mask followed by its mixed cell progression. The three cell bases are loaded counters at this contextual boundary; all remaining values occur in the explicit invocation stream.

structure AffineRuntimeStackSourceSeed where
  maskStart : Nat
  maskBase : Nat
  count : Nat
  cellRight : Nat
  cellLeft : Nat
  cellBlank : Nat
deriving DecidableEq, Repr

Complete stack frame denoted by one loaded runtime source seed.

def affineRuntimeStackSourceFrame (blankStep : Nat)
    (seed : AffineRuntimeStackSourceSeed) : AffineStackFrame :=
  { start := seed.maskStart
    base := seed.maskBase
    count := seed.count
    cells := affineCellProgressionFrames blankStep seed.count
      seed.cellRight seed.cellLeft seed.cellBlank }

Explicit source input: the canonical mask header, an internal boundary, and the runtime cell-count stream.

def encodeAffineRuntimeStackSourceInvocation
    (seed : AffineRuntimeStackSourceSeed) : List UnaryFrameSym :=
  encodeUnaryFrame [seed.count, seed.maskStart,
      seed.maskBase + seed.count] ++
    .frameEnd :: (List.replicate seed.count .tick ++ [.frameEnd])

Finite control connecting header copying, the mixed cell source, and the outer stack terminator.

inductive AffineRuntimeStackSourceLabel (blankStep : Nat)
  | copyHeader | pushHeader (symbol : UnaryFrameSym) | clearHeaderEnd
  | cells (label : AffineCellProgressionSourceLabel blankStep)
  | finish | invalid
deriving DecidableEq, Fintype

private def runtimeStackSourceRelabelOp {blankStep : Nat} :
    Op UnaryFrameSym UnaryFrameSym
        (AffineCellProgressionSourceLabel blankStep) →
      Op UnaryFrameSym UnaryFrameSym
        (AffineRuntimeStackSourceLabel blankStep)
  | .pushOutput symbol next => .pushOutput symbol (.cells next)
  | .pushWork₁ symbol next => .pushWork₁ symbol (.cells next)
  | .pushWork₂ symbol next => .pushWork₂ symbol (.cells next)
  | .moveInputWork₁ nextEmpty nextMoved =>
      .moveInputWork₁ (.cells nextEmpty) (fun symbol => .cells (nextMoved symbol))
  | .moveWork₁Input nextEmpty nextMoved =>
      .moveWork₁Input (.cells nextEmpty) (fun symbol => .cells (nextMoved symbol))
  | .moveInputWork₂ nextEmpty nextMoved =>
      .moveInputWork₂ (.cells nextEmpty) (fun symbol => .cells (nextMoved symbol))
  | .moveWork₂Input nextEmpty nextMoved =>
      .moveWork₂Input (.cells nextEmpty) (fun symbol => .cells (nextMoved symbol))
  | .moveWork₁Work₂ nextEmpty nextMoved =>
      .moveWork₁Work₂ (.cells nextEmpty) (fun symbol => .cells (nextMoved symbol))
  | .moveWork₂Work₁ nextEmpty nextMoved =>
      .moveWork₂Work₁ (.cells nextEmpty) (fun symbol => .cells (nextMoved symbol))
  | .copyInputWorks nextEmpty nextMoved =>
      .copyInputWorks (.cells nextEmpty) (fun symbol => .cells (nextMoved symbol))
  | .popInput nextEmpty nextMoved =>
      .popInput (.cells nextEmpty) (fun symbol => .cells (nextMoved symbol))
  | .popWork₁ nextEmpty nextMoved =>
      .popWork₁ (.cells nextEmpty) (fun symbol => .cells (nextMoved symbol))
  | .popWork₂ nextEmpty nextMoved =>
      .popWork₂ (.cells nextEmpty) (fun symbol => .cells (nextMoved symbol))
  | .inc₁ next => .inc₁ (.cells next)
  | .inc₂ next => .inc₂ (.cells next)
  | .inc₃ next => .inc₃ (.cells next)
  | .dec₁ nextZero nextSucc => .dec₁ (.cells nextZero) (.cells nextSucc)
  | .dec₂ nextZero nextSucc => .dec₂ (.cells nextZero) (.cells nextSucc)
  | .dec₃ nextZero nextSucc => .dec₃ (.cells nextZero) (.cells nextSucc)
  | .jump next => .jump (.cells next)
  | .halt => .halt

One fixed controller emits the complete delimiter-bearing stack frame without halting between its mask header and runtime cell family.

def affineRuntimeStackSourceRevProgram (blankStep : Nat) :
    Program UnaryFrameSym UnaryFrameSym where
  Label := AffineRuntimeStackSourceLabel blankStep
  main := .copyHeader
  op
    | .copyHeader => .popInput .invalid fun
        | .frameEnd => .clearHeaderEnd
        | symbol => .pushHeader symbol
    | .pushHeader symbol => .pushOutput symbol .copyHeader
    | .clearHeaderEnd => .popWork₁ (.cells .loop) (fun _ => .invalid)
    | .cells .finish => .pushOutput .frameEnd .finish
    | .cells label => runtimeStackSourceRelabelOp
        ((affineCellProgressionSourceRevProgram blankStep).op label)
    | .finish => .halt
    | .invalid => .halt

private def affineRuntimeStackSourceCfg {blankStep : Nat}
    (label : AffineRuntimeStackSourceLabel blankStep)
    (buffer₁ : Option UnaryFrameSym) (test : Bool)
    (input output work₁ : List UnaryFrameSym)
    (right left blank : List Unit) :
    BuilderCfg (affineRuntimeStackSourceRevProgram blankStep) where
  label := some label
  buffer₁ := buffer₁
  buffer₂ := none
  test := test
  input := input
  output := output
  work₁ := work₁
  work₂ := []
  counter₁ := right
  counter₂ := left
  counter₃ := blank

Clean contextual entry for one complete stack source.

def affineRuntimeStackSourceLoadedCfg (blankStep : Nat)
    (seed : AffineRuntimeStackSourceSeed) (output : List UnaryFrameSym) :
    BuilderCfg (affineRuntimeStackSourceRevProgram blankStep) :=
  affineRuntimeStackSourceCfg .copyHeader none false
    (encodeAffineRuntimeStackSourceInvocation seed) output []
    (List.replicate seed.cellRight ())
    (List.replicate seed.cellLeft ())
    (List.replicate seed.cellBlank ())

Public continuation after the complete stack frame has been emitted.

def affineRuntimeStackSourceFinishCfg (blankStep : Nat)
    (seed : AffineRuntimeStackSourceSeed) (output : List UnaryFrameSym) :
    BuilderCfg (affineRuntimeStackSourceRevProgram blankStep) :=
  affineRuntimeStackSourceCfg .finish (some .frameEnd)
    (affineCellProgressionSourceFinishTest seed.count false) [] output []
    (List.replicate (seed.cellRight + 6 * seed.count) ())
    (List.replicate (seed.cellLeft - seed.count) ())
    (List.replicate (seed.cellBlank + blankStep * seed.count) ())

Contextual entry preserving an arbitrary invocation after this stack.

def affineRuntimeStackSourceLoadedCfgWithTail (blankStep : Nat)
    (seed : AffineRuntimeStackSourceSeed) (tail output : List UnaryFrameSym) :
    BuilderCfg (affineRuntimeStackSourceRevProgram blankStep) :=
  affineRuntimeStackSourceCfg .copyHeader none false
    (encodeAffineRuntimeStackSourceInvocation seed ++ tail) output []
    (List.replicate seed.cellRight ())
    (List.replicate seed.cellLeft ())
    (List.replicate seed.cellBlank ())

Contextual continuation preserving the following invocation.

def affineRuntimeStackSourceFinishCfgWithTail (blankStep : Nat)
    (seed : AffineRuntimeStackSourceSeed) (tail output : List UnaryFrameSym) :
    BuilderCfg (affineRuntimeStackSourceRevProgram blankStep) :=
  affineRuntimeStackSourceCfg .finish (some .frameEnd)
    (affineCellProgressionSourceFinishTest seed.count false) tail output []
    (List.replicate (seed.cellRight + 6 * seed.count) ())
    (List.replicate (seed.cellLeft - seed.count) ())
    (List.replicate (seed.cellBlank + blankStep * seed.count) ())

              private def runtimeStackSourceRelabelCfg {blankStep : Nat}
    (c : BuilderCfg (affineCellProgressionSourceRevProgram blankStep)) :
    BuilderCfg (affineRuntimeStackSourceRevProgram blankStep) where
  label := c.label.map .cells
  buffer₁ := c.buffer₁
  buffer₂ := c.buffer₂
  test := c.test
  input := c.input
  output := c.output
  work₁ := c.work₁
  work₂ := c.work₂
  counter₁ := c.counter₁
  counter₂ := c.counter₂
  counter₃ := c.counter₃private theorem runtimeStackSourceRelabel_stepOp {blankStep : Nat}
    (op : Op UnaryFrameSym UnaryFrameSym
      (AffineCellProgressionSourceLabel blankStep))
    (c : BuilderCfg (affineCellProgressionSourceRevProgram blankStep)) :
    stepOp (runtimeStackSourceRelabelOp op)
        (runtimeStackSourceRelabelCfg c) =
      runtimeStackSourceRelabelCfg (stepOp op c) := by
  rcases c with
    ⟨label, buffer₁, buffer₂, test, input, output, work₁, work₂,
      counter₁, counter₂, counter₃⟩
  cases op <;>
    simp only [runtimeStackSourceRelabelOp, runtimeStackSourceRelabelCfg,
      stepOp] <;>
    first
    | rfl
    | split <;> rflprivate theorem affineRuntimeStackSource_op_cells {blankStep : Nat}
    (label : AffineCellProgressionSourceLabel blankStep)
    (hexit : label ≠ .finish) :
    (affineRuntimeStackSourceRevProgram blankStep).op (.cells label) =
      runtimeStackSourceRelabelOp
        ((affineCellProgressionSourceRevProgram blankStep).op label) := by
  cases label <;>
    simp_all [affineRuntimeStackSourceRevProgram]

private theorem affineRuntimeStackSource_lift_step {blankStep : Nat}
    (c : BuilderCfg (affineCellProgressionSourceRevProgram blankStep))
    (hexit : c.label ≠ some .finish) :
    step (affineRuntimeStackSourceRevProgram blankStep)
        (runtimeStackSourceRelabelCfg c) =
      Option.map runtimeStackSourceRelabelCfg
        (step (affineCellProgressionSourceRevProgram blankStep) c) := by
  unfold step
  rw [show (runtimeStackSourceRelabelCfg c).label = c.label.map .cells by rfl]
  cases hc : c.label with
  | none => rfl
  | some label =>
      have hlabelExit : label ≠ .finish := by
        intro h
        apply hexit
        simp [hc, h]
      simp only [Option.map_some]
      rw [affineRuntimeStackSource_op_cells label hlabelExit]
      exact congrArg some
        (runtimeStackSourceRelabel_stepOp
          ((affineCellProgressionSourceRevProgram blankStep).op label) c)

private theorem runtimeStackSource_iterate_bind_none {sigma : Type}
    (f : sigma → Option sigma) : ∀ n : Nat,
    (flip Option.bind f)^[n] none = none := by
  intro n
  induction n with
  | zero => rfl
  | succ n ih =>
      rw [Function.iterate_succ_apply]
      change (flip Option.bind f)^[n] none = none
      exact ih

private theorem affineRuntimeStackSource_haltExit_no_return
    {blankStep : Nat}
    (a b : BuilderCfg (affineCellProgressionSourceRevProgram blankStep))
    (ha : a.label = some .finish) (hb : b.label = some .finish) : ∀ n : Nat,
    (flip Option.bind
      (step (affineCellProgressionSourceRevProgram blankStep)))^[n]
        (step (affineCellProgressionSourceRevProgram blankStep) a) ≠ some b := by
  intro n
  let halted : BuilderCfg (affineCellProgressionSourceRevProgram blankStep) :=
    { a with label := none, buffer₁ := none, buffer₂ := none, test := false }
  have hstep : step (affineCellProgressionSourceRevProgram blankStep) a =
      some halted := by
    unfold step
    rw [ha]
    simp [affineCellProgressionSourceRevProgram, stepOp, halted]
  cases n with
  | zero =>
      rw [hstep]
      intro h
      have hlabel := congrArg (fun cfg => cfg.label) (Option.some.inj h)
      simp [halted, hb] at hlabel
  | succ n =>
      rw [hstep, Function.iterate_succ_apply]
      change (flip Option.bind
        (step (affineCellProgressionSourceRevProgram blankStep)))^[n]
          (step (affineCellProgressionSourceRevProgram blankStep) halted) ≠
            some b
      have hnone : step (affineCellProgressionSourceRevProgram blankStep)
          halted = none := rfl
      rw [hnone, runtimeStackSource_iterate_bind_none]
      simp

private theorem affineRuntimeStackSource_lift_iterations {blankStep : Nat}
    {a b : BuilderCfg (affineCellProgressionSourceRevProgram blankStep)}
    (hb : b.label = some .finish) : ∀ n : Nat,
    (flip Option.bind
      (step (affineCellProgressionSourceRevProgram blankStep)))^[n]
        (some a) = some b →
      (flip Option.bind
        (step (affineRuntimeStackSourceRevProgram blankStep)))^[n]
          (some (runtimeStackSourceRelabelCfg a)) =
            some (runtimeStackSourceRelabelCfg b) := by
  intro n
  induction n generalizing a with
  | zero =>
      intro h
      injection h with hab
      subst a
      rfl
  | succ n ih =>
      intro h
      rw [Function.iterate_succ_apply] at h ⊢
      change (flip Option.bind
        (step (affineCellProgressionSourceRevProgram blankStep)))^[n]
          (step (affineCellProgressionSourceRevProgram blankStep) a) =
            some b at h
      change (flip Option.bind
        (step (affineRuntimeStackSourceRevProgram blankStep)))^[n]
          (step (affineRuntimeStackSourceRevProgram blankStep)
            (runtimeStackSourceRelabelCfg a)) =
              some (runtimeStackSourceRelabelCfg b)
      have haexit : a.label ≠ some .finish := by
        intro ha
        exact affineRuntimeStackSource_haltExit_no_return a b ha hb n h
      cases hsource : step
          (affineCellProgressionSourceRevProgram blankStep) a with
      | none =>
          rw [hsource, runtimeStackSource_iterate_bind_none] at h
          contradiction
      | some c =>
          have hsim := affineRuntimeStackSource_lift_step a haexit
          rw [hsource] at hsim
          simp only [Option.map_some] at hsim
          rw [hsim]
          rw [hsource] at h
          exact ih h

private theorem unaryFrame_no_frameEnd (values : List Nat) :
    ∀ symbol ∈ encodeUnaryFrame values, symbol ≠ .frameEnd := by
  intro symbol hsymbol
  rw [encodeUnaryFrame, List.mem_flatMap] at hsymbol
  rcases hsymbol with ⟨value, _, hblock⟩
  simp [encodeUnaryFrameBlock] at hblock
  rcases hblock with ⟨_, rfl⟩ | rfl <;> simp

private def affineRuntimeStackSource_copy_run {blankStep : Nat}
    (header cellInput output : List UnaryFrameSym)
    (buffer₁ : Option UnaryFrameSym) (right left blank : Nat)
    (hheader : ∀ symbol ∈ header, symbol ≠ .frameEnd) :
    EvalsToInTime (step (affineRuntimeStackSourceRevProgram blankStep))
      (affineRuntimeStackSourceCfg .copyHeader buffer₁ false
        (header ++ .frameEnd :: cellInput) output []
        (List.replicate right ()) (List.replicate left ())
        (List.replicate blank ()))
      (some (runtimeStackSourceRelabelCfg
        (affineCellProgressionSourceCfg .loop none false cellInput
          (header.reverse ++ output) []
          (List.replicate right ()) (List.replicate left ())
          (List.replicate blank ()))))
      (2 * header.length + 2) := by
  induction header generalizing buffer₁ output with
  | nil =>
      refine ⟨⟨2, ?_⟩, le_rfl⟩
      rfl
  | cons symbol rest ih =>
      have hsymbol : symbol ≠ UnaryFrameSym.frameEnd :=
        hheader symbol (by simp)
      have hrest : ∀ item ∈ rest, item ≠ UnaryFrameSym.frameEnd := by
        intro item hitem
        exact hheader item (by simp [hitem])
      let afterHead := affineRuntimeStackSourceCfg
        (blankStep := blankStep) .copyHeader (some symbol) false
        (rest ++ .frameEnd :: cellInput) (symbol :: output) []
        (List.replicate right ()) (List.replicate left ())
        (List.replicate blank ())
      have hhead : EvalsToInTime
          (step (affineRuntimeStackSourceRevProgram blankStep))
          (affineRuntimeStackSourceCfg .copyHeader buffer₁ false
            ((symbol :: rest) ++ .frameEnd :: cellInput) output []
            (List.replicate right ()) (List.replicate left ())
            (List.replicate blank ()))
          (some afterHead) 2 := by
        cases symbol with
        | tick => exact ⟨⟨2, rfl⟩, le_rfl⟩
        | separator => exact ⟨⟨2, rfl⟩, le_rfl⟩
        | frameEnd => exact (hsymbol rfl).elim
      have htail := ih (symbol :: output) (some symbol) hrest
      let full := EvalsToInTime.trans
        (step (affineRuntimeStackSourceRevProgram blankStep)) _ _ _
          afterHead _ hhead htail
      convert full using 1
      · simp [List.reverse_cons, List.append_assoc]
      · simp only [List.length_cons]
        omegaprivate def affineRuntimeStackSource_cells_run (blankStep : Nat)
    (seed : AffineRuntimeStackSourceSeed)
    (tail output : List UnaryFrameSym) :
    EvalsToInTime (step (affineRuntimeStackSourceRevProgram blankStep))
      (runtimeStackSourceRelabelCfg
        (affineCellProgressionSourceCfg .loop none false
          (List.replicate seed.count .tick ++ .frameEnd :: tail) output []
          (List.replicate seed.cellRight ())
          (List.replicate seed.cellLeft ())
          (List.replicate seed.cellBlank ())))
      (some (runtimeStackSourceRelabelCfg
        (affineCellProgressionSourceCfg .finish (some .frameEnd)
          (affineCellProgressionSourceFinishTest seed.count false) tail
          ((encodeAffineCellFamily
            (affineCellProgressionFrames blankStep seed.count
              seed.cellRight seed.cellLeft seed.cellBlank)).reverse ++ output) []
          (List.replicate (seed.cellRight + 6 * seed.count) ())
          (List.replicate (seed.cellLeft - seed.count) ())
          (List.replicate
            (seed.cellBlank + blankStep * seed.count) ()))))
      (affineCellProgressionSourceSteps blankStep seed.count
        seed.cellRight seed.cellLeft seed.cellBlank) := by
  have sourceRun := affineCellProgressionSource_runToFinishWithTail blankStep
    seed.count seed.cellRight seed.cellLeft seed.cellBlank tail output
  refine ⟨⟨sourceRun.steps, ?_⟩, sourceRun.steps_le_m⟩
  exact affineRuntimeStackSource_lift_iterations rfl sourceRun.steps
    sourceRun.evals_in_steps

Exact runtime of one complete loaded stack source.

def affineRuntimeStackSourceSteps (blankStep : Nat)
    (seed : AffineRuntimeStackSourceSeed) : Nat :=
  2 * (encodeUnaryFrame [seed.count, seed.maskStart,
      seed.maskBase + seed.count]).length + 2 +
    affineCellProgressionSourceSteps blankStep seed.count
      seed.cellRight seed.cellLeft seed.cellBlank + 1

Contextual exact run preserving the invocation that follows this stack.

def affineRuntimeStackSource_runToFinishWithTail (blankStep : Nat)
    (seed : AffineRuntimeStackSourceSeed)
    (tail output : List UnaryFrameSym) :
    EvalsToInTime (step (affineRuntimeStackSourceRevProgram blankStep))
      (affineRuntimeStackSourceLoadedCfgWithTail blankStep seed tail output)
      (some (affineRuntimeStackSourceFinishCfgWithTail blankStep seed tail
        ((encodeAffineStackFrame
          (affineRuntimeStackSourceFrame blankStep seed)).reverse ++ output)))
      (affineRuntimeStackSourceSteps blankStep seed) := by
  let header := encodeUnaryFrame [seed.count, seed.maskStart,
    seed.maskBase + seed.count]
  have hcopy := affineRuntimeStackSource_copy_run
    (blankStep := blankStep) header
    (List.replicate seed.count .tick ++ .frameEnd :: tail) output none
    seed.cellRight seed.cellLeft seed.cellBlank
    (unaryFrame_no_frameEnd _)
  have hcells := affineRuntimeStackSource_cells_run blankStep seed tail
    (header.reverse ++ output)
  let h₁ := EvalsToInTime.trans
    (step (affineRuntimeStackSourceRevProgram blankStep)) _ _ _ _ _
      hcopy hcells
  have hend : EvalsToInTime
      (step (affineRuntimeStackSourceRevProgram blankStep))
      (runtimeStackSourceRelabelCfg
        (affineCellProgressionSourceCfg .finish (some .frameEnd)
          (affineCellProgressionSourceFinishTest seed.count false) tail
          ((encodeAffineCellFamily
            (affineCellProgressionFrames blankStep seed.count
              seed.cellRight seed.cellLeft seed.cellBlank)).reverse ++
                (header.reverse ++ output)) []
          (List.replicate (seed.cellRight + 6 * seed.count) ())
          (List.replicate (seed.cellLeft - seed.count) ())
          (List.replicate
            (seed.cellBlank + blankStep * seed.count) ())))
      (some (affineRuntimeStackSourceFinishCfgWithTail blankStep seed tail
        (.frameEnd ::
          (encodeAffineCellFamily
            (affineCellProgressionFrames blankStep seed.count
              seed.cellRight seed.cellLeft seed.cellBlank)).reverse ++
            (header.reverse ++ output)))) 1 := ⟨⟨1, rfl⟩, le_rfl⟩
  let full := EvalsToInTime.trans
    (step (affineRuntimeStackSourceRevProgram blankStep)) _ _ _ _ _ h₁ hend
  convert full using 1
  · simp [affineRuntimeStackSourceLoadedCfgWithTail,
      encodeAffineRuntimeStackSourceInvocation, header]
  · simp [affineRuntimeStackSourceFinishCfgWithTail,
      affineRuntimeStackSourceFrame, encodeAffineStackFrame, header,
      List.reverse_append, List.append_assoc]
  · simp [affineRuntimeStackSourceSteps, header]
    omega

The continuous loaded source emits the exact reversed encoding of one complete AffineStackFrame.

def affineRuntimeStackSource_runToFinish (blankStep : Nat)
    (seed : AffineRuntimeStackSourceSeed) (output : List UnaryFrameSym) :
    EvalsToInTime (step (affineRuntimeStackSourceRevProgram blankStep))
      (affineRuntimeStackSourceLoadedCfg blankStep seed output)
      (some (affineRuntimeStackSourceFinishCfg blankStep seed
        ((encodeAffineStackFrame
          (affineRuntimeStackSourceFrame blankStep seed)).reverse ++ output)))
      (affineRuntimeStackSourceSteps blankStep seed) := by
  simpa [affineRuntimeStackSourceLoadedCfg,
    affineRuntimeStackSourceFinishCfg,
    affineRuntimeStackSourceLoadedCfgWithTail,
    affineRuntimeStackSourceFinishCfgWithTail] using
      affineRuntimeStackSource_runToFinishWithTail blankStep seed [] output

Quadratic contextual runtime bound in the full stack-source payload.


theorem affineRuntimeStackSourceSteps_le (blankStep : Nat)
    (seed : AffineRuntimeStackSourceSeed) :
    affineRuntimeStackSourceSteps blankStep seed ≤
      70 * (blankStep + 1) *
        ((encodeUnaryFrame [seed.count, seed.maskStart,
            seed.maskBase + seed.count]).length + seed.count +
          seed.cellRight + seed.cellLeft + seed.cellBlank + 1) ^ 2 := by
  let headerLength := (encodeUnaryFrame [seed.count, seed.maskStart,
    seed.maskBase + seed.count]).length
  let payload := headerLength + seed.count + seed.cellRight +
    seed.cellLeft + seed.cellBlank + 1
  have hpayload : 1 ≤ payload := by simp [payload]
  have hheader : headerLength ≤ payload := by
    dsimp only [payload]
    omega
  have hcells := affineCellProgressionSourceSteps_le blankStep seed.count
    seed.cellRight seed.cellLeft seed.cellBlank
  have hcellPayload : seed.count + seed.cellRight + seed.cellLeft +
      seed.cellBlank + 1 ≤ payload := by
    dsimp only [payload]
    omega
  have hsquare : (seed.count + seed.cellRight + seed.cellLeft +
      seed.cellBlank + 1) ^ 2 ≤ payload ^ 2 := by nlinarith
  have hcells' : affineCellProgressionSourceSteps blankStep seed.count
      seed.cellRight seed.cellLeft seed.cellBlank ≤
        60 * (blankStep + 1) * payload ^ 2 :=
    hcells.trans (Nat.mul_le_mul_left (60 * (blankStep + 1)) hsquare)
  have hheader' : 2 * headerLength + 3 ≤
      10 * (blankStep + 1) * payload ^ 2 := by nlinarith
  calc
    affineRuntimeStackSourceSteps blankStep seed =
        (2 * headerLength + 3) +
          affineCellProgressionSourceSteps blankStep seed.count
            seed.cellRight seed.cellLeft seed.cellBlank := by
      simp [affineRuntimeStackSourceSteps, headerLength]
      omega
    _ ≤ 10 * (blankStep + 1) * payload ^ 2 +
          60 * (blankStep + 1) * payload ^ 2 :=
      Nat.add_le_add hheader' hcells'
    _ = 70 * (blankStep + 1) * payload ^ 2 := by ring

end CLRS.Chapter34.Turing.PolyBuilder