RealtimeTransfer.lean

/-
The strict real-time transfer.

A deterministic ordinary single-head multitape machine that performs exactly
one global transition per arriving input symbol is encoded as a
letter-synchronous machine with `2 * m` stacks -- two per tape, by the zipper --
performing at most one action on each stack per symbol.  Composing with
`compile_correct` gives a single LMR scaffolding automaton, of degree `2 * m`
and distance `2`, that appends one node per input symbol and whose scaffold
decodes to the machine's tape contents after every prefix.

There is no `|x|`-advice tape and no post-input cleanup: acceptance is the
control state reached after the last symbol, on both sides.
-/

import FPRDTransfer.Compile
import FPRDTransfer.TapeZipper

namespace FPRD

variable {Sym Q T : Type} {m : Nat}

/-- A deterministic multitape machine with one head per tape, making exactly
one transition per arriving input symbol.  It sees only the scanned symbols. -/
structure MultiTapeMachine (Sym : Type) (Q : Type) (T : Type) (m : Nat) where
  blank : T
  step : Q → Sym → (Fin m → T) → Q × (Fin m → T × Move)
  init : Q
  accept : Q → Bool

/-- A multitape configuration. -/
structure TapeConfig (Q : Type) (T : Type) (m : Nat) where
  ctrl : Q
  tapes : Fin m → Tape T

namespace MultiTapeMachine

/-- The all-blank tape. -/
def initTape (b : T) : Tape T where
  left := []
  cur := b
  right := []

def stepConfig (N : MultiTapeMachine Sym Q T m) (c : TapeConfig Q T m) (x : Sym) :
    TapeConfig Q T m :=
  let r := N.step c.ctrl x (fun i => (c.tapes i).cur)
  { ctrl := r.1
    tapes := fun i => (c.tapes i).apply (r.2 i).1 N.blank (r.2 i).2 }

@[simp] theorem stepConfig_ctrl (N : MultiTapeMachine Sym Q T m) (c : TapeConfig Q T m)
    (x : Sym) :
    (N.stepConfig c x).ctrl = (N.step c.ctrl x (fun i => (c.tapes i).cur)).1 := rfl

@[simp] theorem stepConfig_tapes (N : MultiTapeMachine Sym Q T m) (c : TapeConfig Q T m)
    (x : Sym) (i : Fin m) :
    (N.stepConfig c x).tapes i =
      (c.tapes i).apply ((N.step c.ctrl x (fun i => (c.tapes i).cur)).2 i).1 N.blank
        ((N.step c.ctrl x (fun i => (c.tapes i).cur)).2 i).2 := rfl

def initConfig (N : MultiTapeMachine Sym Q T m) : TapeConfig Q T m where
  ctrl := N.init
  tapes := fun _ => initTape N.blank

def run (N : MultiTapeMachine Sym Q T m) (w : List Sym) : TapeConfig Q T m :=
  w.foldl N.stepConfig N.initConfig

def decides (N : MultiTapeMachine Sym Q T m) (w : List Sym) : Bool :=
  N.accept (N.run w).ctrl

end MultiTapeMachine

/-! ### Indexing the two stacks of each tape -/

/-- The stack holding the cells left of tape `i`'s head. -/
def leftIdx (i : Fin m) : Fin (2 * m) :=
  ⟨2 * i.val, by have := i.isLt; omega⟩

/-- The stack holding the cells right of tape `i`'s head. -/
def rightIdx (i : Fin m) : Fin (2 * m) :=
  ⟨2 * i.val + 1, by have := i.isLt; omega⟩

/-- Which tape a stack index belongs to. -/
def tapeOf (j : Fin (2 * m)) : Fin m :=
  ⟨j.val / 2, by have := j.isLt; omega⟩

/-- Whether a stack index is a tape's left stack. -/
def isLeftIdx (j : Fin (2 * m)) : Bool := j.val % 2 == 0

@[simp] theorem tapeOf_leftIdx (i : Fin m) : tapeOf (leftIdx i) = i := by
  apply Fin.ext
  simp only [tapeOf, leftIdx]
  omega

@[simp] theorem tapeOf_rightIdx (i : Fin m) : tapeOf (rightIdx i) = i := by
  apply Fin.ext
  simp only [tapeOf, rightIdx]
  omega

@[simp] theorem isLeftIdx_leftIdx (i : Fin m) : isLeftIdx (leftIdx i) = true := by
  have hmod : (leftIdx i).val % 2 = 0 := by simp only [leftIdx]; omega
  simp [isLeftIdx, hmod]

@[simp] theorem isLeftIdx_rightIdx (i : Fin m) : isLeftIdx (rightIdx i) = false := by
  have hmod : (rightIdx i).val % 2 = 1 := by simp only [rightIdx]; omega
  simp [isLeftIdx, hmod]

namespace MultiTapeMachine

/-- The stack action for one stack index, given this step's writes and moves. -/
def stackOp (writes : Fin m → T × Move) (j : Fin (2 * m)) : StackOp T :=
  if isLeftIdx j then Tape.leftOp (writes (tapeOf j)).1 (writes (tapeOf j)).2
  else Tape.rightOp (writes (tapeOf j)).1 (writes (tapeOf j)).2

@[simp] theorem stackOp_left (writes : Fin m → T × Move) (i : Fin m) :
    stackOp writes (leftIdx i) = Tape.leftOp (writes i).1 (writes i).2 := by
  simp [stackOp]

@[simp] theorem stackOp_right (writes : Fin m → T × Move) (i : Fin m) :
    stackOp writes (rightIdx i) = Tape.rightOp (writes i).1 (writes i).2 := by
  simp [stackOp]

/-- The next scanned symbol, computed from the finite control and the stack
tops only.  A blank appears exactly when the relevant stack is empty. -/
def nextCurEnc (b : T) (writes : Fin m → T × Move) (tops : Fin (2 * m) → Option T)
    (i : Fin m) : T :=
  match (writes i).2 with
  | .right => (tops (rightIdx i)).getD b
  | .left => (tops (leftIdx i)).getD b
  | .stay => (writes i).1

/-- The zipper encoding: `2 * m` stacks, the scanned symbols in the control. -/
def toStack (N : MultiTapeMachine Sym Q T m) :
    StackMachine Sym (Q × (Fin m → T)) T (2 * m) where
  step := fun qc x tops =>
    (((N.step qc.1 x qc.2).1, nextCurEnc N.blank (N.step qc.1 x qc.2).2 tops),
      stackOp (N.step qc.1 x qc.2).2)
  init := (N.init, fun _ => N.blank)
  accept := fun qc => N.accept qc.1

@[simp] theorem toStack_step_fst (N : MultiTapeMachine Sym Q T m)
    (qc : Q × (Fin m → T)) (x : Sym) (tops : Fin (2 * m) → Option T) :
    (N.toStack.step qc x tops).1 =
      ((N.step qc.1 x qc.2).1, nextCurEnc N.blank (N.step qc.1 x qc.2).2 tops) := rfl

@[simp] theorem toStack_step_snd (N : MultiTapeMachine Sym Q T m)
    (qc : Q × (Fin m → T)) (x : Sym) (tops : Fin (2 * m) → Option T) :
    (N.toStack.step qc x tops).2 = stackOp (N.step qc.1 x qc.2).2 := rfl

@[simp] theorem toStack_accept (N : MultiTapeMachine Sym Q T m) (qc : Q × (Fin m → T)) :
    N.toStack.accept qc = N.accept qc.1 := rfl

/-- The correspondence between a multitape configuration and the encoded
stack configuration. -/
structure TapeSim (N : MultiTapeMachine Sym Q T m) (c : TapeConfig Q T m)
    (d : Config (Q × (Fin m → T)) T (2 * m)) : Prop where
  ctrl : c.ctrl = d.ctrl.1
  cur : ∀ i, (c.tapes i).cur = d.ctrl.2 i
  left : ∀ i, d.stacks (leftIdx i) = (c.tapes i).left
  right : ∀ i, d.stacks (rightIdx i) = (c.tapes i).right

theorem tapeSim_init (N : MultiTapeMachine Sym Q T m) :
    N.TapeSim N.initConfig N.toStack.initConfig where
  ctrl := rfl
  cur := fun _ => rfl
  left := fun _ => rfl
  right := fun _ => rfl

theorem tapeSim_step (N : MultiTapeMachine Sym Q T m) {c : TapeConfig Q T m}
    {d : Config (Q × (Fin m → T)) T (2 * m)} (h : N.TapeSim c d) (x : Sym) :
    N.TapeSim (N.stepConfig c x) (N.toStack.stepConfig d x) := by
  have hq : d.ctrl.1 = c.ctrl := h.ctrl.symm
  have hcur : d.ctrl.2 = fun i => (c.tapes i).cur := (funext h.cur).symm
  refine { ctrl := ?_, cur := ?_, left := ?_, right := ?_ }
  · simp only [StackMachine.stepConfig_ctrl, toStack_step_fst, stepConfig_ctrl, hq, hcur]
  · intro i
    simp only [StackMachine.stepConfig_ctrl, toStack_step_fst, stepConfig_tapes, hq, hcur,
      Tape.apply_cur, Tape.nextCur_of_tops, nextCurEnc, h.left i, h.right i]
    cases ((N.step c.ctrl x fun i => (c.tapes i).cur).2 i).2 <;> rfl
  · intro i
    simp only [StackMachine.stepConfig_stacks, toStack_step_snd, stepConfig_tapes, hq, hcur,
      stackOp_left, Tape.apply_left, h.left i]
  · intro i
    simp only [StackMachine.stepConfig_stacks, toStack_step_snd, stepConfig_tapes, hq, hcur,
      stackOp_right, Tape.apply_right, h.right i]

theorem tapeSim_run (N : MultiTapeMachine Sym Q T m) :
    ∀ (w : List Sym) (c : TapeConfig Q T m) (d : Config (Q × (Fin m → T)) T (2 * m)),
      N.TapeSim c d →
      N.TapeSim (w.foldl N.stepConfig c) (w.foldl N.toStack.stepConfig d) := by
  intro w
  induction w with
  | nil => intro c d h; exact h
  | cons x w ih =>
    intro c d h
    simp only [List.foldl_cons]
    exact ih _ _ (tapeSim_step N h x)

/-- **Strict multitape transfer, stack level.** -/
theorem toStack_correct (N : MultiTapeMachine Sym Q T m) (w : List Sym) :
    N.TapeSim (N.run w) (N.toStack.run w) :=
  tapeSim_run N w N.initConfig N.toStack.initConfig (tapeSim_init N)

/-! ### The composed theorem -/

/-- **Strict real-time transfer.**  For every input word, the scaffolding
automaton compiled from a strict single-transition-per-symbol multitape machine
has the same control state, and its scaffold decodes at the top to exactly the
two zipper halves of every tape.

Degree is `2 * m`, distance is `2`, one node is appended per input symbol, and
acceptance is the final control state. -/
theorem realtime_transfer (N : MultiTapeMachine Sym Q T m) (w : List Sym) :
    (∀ i, decode ((compile N.toStack).run w).2 (leftIdx i)
        ((compile N.toStack).run w).2.top = ((N.run w).tapes i).left) ∧
    (∀ i, decode ((compile N.toStack).run w).2 (rightIdx i)
        ((compile N.toStack).run w).2.top = ((N.run w).tapes i).right) ∧
    (N.run w).ctrl = ((compile N.toStack).run w).1.1 := by
  have hs := toStack_correct N w
  refine ⟨fun i => ?_, fun i => ?_, ?_⟩
  · rw [compile_stacks N.toStack w (leftIdx i)]; exact hs.left i
  · rw [compile_stacks N.toStack w (rightIdx i)]; exact hs.right i
  · rw [← compile_ctrl N.toStack w]; exact hs.ctrl

/-- The compiled scaffolding automaton decides exactly the multitape machine's
language. -/
theorem realtime_transfer_decides (N : MultiTapeMachine Sym Q T m) (w : List Sym) :
    (compile N.toStack).decides w = N.decides w := by
  rw [compile_decides]
  show N.toStack.accept (N.toStack.run w).ctrl = N.accept (N.run w).ctrl
  rw [toStack_accept, ← (toStack_correct N w).ctrl]

/-! ### Reconstructing each source tape from the scaffold

`realtime_transfer` identifies the two decoded zipper halves.  The scanned
symbol is carried in the compiled finite control.  The definitions and
theorems below package those three facts as equality of `Tape` values and then
as agreement at every integer offset, including the blank-padded tails. -/

/-- Tape `i` reconstructed from the compiled scaffold and finite control after
reading `w`. -/
def scaffoldTape (N : MultiTapeMachine Sym Q T m) (w : List Sym) (i : Fin m) :
    Tape T where
  left :=
    decode ((compile N.toStack).run w).2 (leftIdx i) ((compile N.toStack).run w).2.top
  cur := ((compile N.toStack).run w).1.2 i
  right :=
    decode ((compile N.toStack).run w).2 (rightIdx i) ((compile N.toStack).run w).2.top

/-- The tape reconstructed from the compiled scaffold is exactly the source
machine's tape after every input word. -/
theorem realtime_transfer_tape (N : MultiTapeMachine Sym Q T m) (w : List Sym)
    (i : Fin m) : scaffoldTape N w i = (N.run w).tapes i := by
  have h := realtime_transfer N w
  have hcur : ((compile N.toStack).run w).1.2 i = ((N.run w).tapes i).cur := by
    rw [← compile_ctrl N.toStack w]
    exact ((toStack_correct N w).cur i).symm
  simp only [scaffoldTape, h.1 i, h.2.1 i, hcur]

/-- The reconstructed and source tapes agree at every integer offset from the
head, including offsets in their implicit blank tails. -/
theorem realtime_transfer_tape_contents (N : MultiTapeMachine Sym Q T m)
    (w : List Sym) (i : Fin m) (z : Int) :
    (scaffoldTape N w i).get N.blank z = ((N.run w).tapes i).get N.blank z := by
  rw [realtime_transfer_tape]

/-- The compiled automaton meets LMR's typing constraints: every named port
word has length at most the distance, and `SELF` is never used. -/
theorem realtime_transfer_wellFormed (N : MultiTapeMachine Sym Q T m) :
    (compile N.toStack).DistanceOk ∧ (compile N.toStack).SelfFree :=
  ⟨compile_distanceOk N.toStack, compile_selfFree N.toStack⟩

/-- The compiled automaton satisfies the structural constraints established
here and decides exactly the source machine's language. Finiteness enters only
when this operational theorem is composed with the scaffold-to-PEG theorem. -/
theorem realtime_transfer_wellFormed_decides (N : MultiTapeMachine Sym Q T m) :
    (compile N.toStack).DistanceOk ∧ (compile N.toStack).SelfFree ∧
      ∀ w : List Sym, (compile N.toStack).decides w = N.decides w :=
  ⟨compile_distanceOk _, compile_selfFree _, realtime_transfer_decides N⟩

end MultiTapeMachine

end FPRD