BoundedActionWindow.lean

import FrontierDerivative.LastActionRefinement

/-!
# Canonical bounded hidden-action windows

Successful traces are defined on the original partial visible machine. Their
last `k` hidden actions, newest first, form a canonical finite-shape control
refinement. If each such window class carries at most one stack per original
control, the refinement is control-functional and reaches the existing
compiler.
-/

namespace FrontierDerivative.BoundedActionWindow

open FiniteRefinement
open FiniteReindexing

universe uΓ

variable {Input Q : Type} {Γ : Type uΓ}

/-! ## Bounded action memory -/

/-- A newest-first list of at most `k` hidden visible actions. -/
def ActionWindow (k : Nat) := { actions : List VisibleAction // actions.length ≤ k }

/-- The action window at the empty-word boundary. -/
def emptyWindow (k : Nat) : ActionWindow k := ⟨[], Nat.zero_le k⟩

/-- Record the current action at the front and forget everything beyond the
fixed depth. -/
def pushWindow (k : Nat) (action : VisibleAction)
    (memory : ActionWindow k) : ActionWindow k :=
  ⟨(action :: memory.1).take k, by
    rw [List.length_take]
    exact Nat.min_le_left _ _⟩

/-- The exact bounded window of a chronological action trace. -/
def windowOf (k : Nat) (actions : List VisibleAction) : ActionWindow k :=
  actions.foldl (fun memory action => pushWindow k action memory)
    (emptyWindow k)

theorem windowOf_append (k : Nat) (actions : List VisibleAction)
    (action : VisibleAction) :
    windowOf k (actions ++ [action]) =
      pushWindow k action (windowOf k actions) := by
  simp [windowOf]

theorem pushWindow_zero (action : VisibleAction) (memory : ActionWindow 0) :
    pushWindow 0 action memory = emptyWindow 0 := by
  apply Subtype.ext
  rfl

theorem windowOf_zero (actions : List VisibleAction) :
    windowOf 0 actions = emptyWindow 0 := by
  apply Subtype.ext
  rcases windowOf 0 actions with ⟨memory, hmemory⟩
  dsimp
  cases memory with
  | nil => rfl
  | cons action rest => simp at hmemory

/-! ## Original traced semantics -/

/-- One successful hidden action per observed input round, retained in
chronological order. This relation belongs to the original machine. -/
inductive TracedReachable (V : PartialVisible.Machine Input Q Γ) :
    List Input → List VisibleAction → PartialVisible.Config Q Γ → Prop where
  | init : TracedReachable V [] [] V.initConfig
  | step {w : List Input} {actions : List VisibleAction}
      {c : PartialVisible.Config Q Γ} (a : Input) (action : VisibleAction)
      {c' : PartialVisible.Config Q Γ} :
      TracedReachable V w actions c →
      V.apply a action c = some c' →
      TracedReachable V (w ++ [a]) (actions ++ [action]) c'

/-- The original successful frontier classified by its exact last-`k` action
window. The refined machine does not occur in this definition. -/
def WindowFrontier (V : PartialVisible.Machine Input Q Γ) (k : Nat)
    (w : List Input) (memory : ActionWindow k) (q : Q) (z : List Γ) : Prop :=
  ∃ actions,
    TracedReachable V w actions ⟨q, z⟩ ∧
      windowOf k actions = memory

/-- For one fixed input prefix, target control, and bounded hidden-action
window, there is at most one resulting concrete stack. -/
def WindowSeparated (V : PartialVisible.Machine Input Q Γ) (k : Nat) : Prop :=
  ∀ w memory q z₁ z₂,
    WindowFrontier V k w memory q z₁ →
    WindowFrontier V k w memory q z₂ →
    z₁ = z₂

/-! ## Canonical machine -/

/-- Refine control by the bounded window of the successful hidden actions seen
so far. -/
def rememberWindow (V : PartialVisible.Machine Input Q Γ) (k : Nat) :
    PartialVisible.Machine Input (Q × ActionWindow k) Γ where
  call := fun state a =>
    (V.call state.1 a).map fun next =>
      ((next.1, pushWindow k .call state.2), next.2)
  ret := fun state a top =>
    (V.ret state.1 a top).map fun q =>
      (q, pushWindow k .ret state.2)
  localStep := fun state a =>
    (V.localStep state.1 a).map fun q =>
      (q, pushWindow k .local state.2)
  init := (V.init, emptyWindow k)
  accept := fun state => V.accept state.1

/-- A refined command is exactly the original same-round command, and its
target memory is exactly the current action pushed into the old window. -/
theorem rememberWindow_apply_iff
    (V : PartialVisible.Machine Input Q Γ) (k : Nat)
    (a : Input) (action : VisibleAction) (q q' : Q)
    (memory memory' : ActionWindow k) (z z' : List Γ) :
    (rememberWindow V k).apply a action ⟨(q, memory), z⟩ =
        some ⟨(q', memory'), z'⟩ ↔
      V.apply a action ⟨q, z⟩ = some ⟨q', z'⟩ ∧
        memory' = pushWindow k action memory := by
  cases action with
  | call =>
      cases hcommand : V.call q a with
      | none => simp [rememberWindow, PartialVisible.Machine.apply, hcommand]
      | some next =>
          rcases next with ⟨target, symbol⟩
          simp [rememberWindow, PartialVisible.Machine.apply, hcommand,
            eq_comm, and_assoc, and_left_comm, and_comm]
  | ret =>
      cases hcommand : V.ret q a z.head? with
      | none => simp [rememberWindow, PartialVisible.Machine.apply, hcommand]
      | some target =>
          simp [rememberWindow, PartialVisible.Machine.apply, hcommand,
            eq_comm, and_assoc, and_left_comm, and_comm]
  | «local» =>
      cases hcommand : V.localStep q a with
      | none => simp [rememberWindow, PartialVisible.Machine.apply, hcommand]
      | some target =>
          simp [rememberWindow, PartialVisible.Machine.apply, hcommand,
            eq_comm, and_assoc, and_left_comm, and_comm]

/-- Forgetting the bounded window is a lawful same-action, same-stack
refinement. -/
def rememberWindowRefinement (V : PartialVisible.Machine Input Q Γ) (k : Nat) :
    Refinement V (rememberWindow V k) where
  erase := Prod.fst
  init_eq := rfl
  accept_eq := by intro; rfl
  apply_sound := by
    intro a action state z state' z' h
    rcases state with ⟨q, memory⟩
    rcases state' with ⟨q', memory'⟩
    exact ((rememberWindow_apply_iff V k a action q q' memory memory' z z').1 h).1
  apply_complete := by
    intro a action state z q' z' h
    rcases state with ⟨q, memory⟩
    refine ⟨(q', pushWindow k action memory), ?_, rfl⟩
    exact (rememberWindow_apply_iff V k a action q q' memory
      (pushWindow k action memory) z z').2 ⟨h, rfl⟩

/-! ## Exact trace translations -/

/-- Every original successful trace lifts to the refined run with exactly its
folded action window. -/
theorem traced_to_remembered (V : PartialVisible.Machine Input Q Γ) (k : Nat)
    {w : List Input} {actions : List VisibleAction}
    {c : PartialVisible.Config Q Γ}
    (h : TracedReachable V w actions c) :
    (rememberWindow V k).TaggedReachable w
      ⟨(c.ctrl, windowOf k actions), c.stack⟩ := by
  induction h with
  | init => exact PartialVisible.Machine.TaggedReachable.init
  | step a action hprev happly ih =>
      apply PartialVisible.Machine.TaggedReachable.step a action ih
      rw [windowOf_append]
      exact (rememberWindow_apply_iff V k a action _ _ _ _ _ _).2
        ⟨happly, rfl⟩

/-- Every refined successful run erases to an original chronological trace,
and the stored memory is exactly that trace's bounded window. -/
theorem remembered_to_traced (V : PartialVisible.Machine Input Q Γ) (k : Nat)
    {w : List Input} {state : PartialVisible.Config (Q × ActionWindow k) Γ}
    (h : (rememberWindow V k).TaggedReachable w state) :
    ∃ actions,
      TracedReachable V w actions ⟨state.ctrl.1, state.stack⟩ ∧
        windowOf k actions = state.ctrl.2 := by
  induction h with
  | init => exact ⟨[], TracedReachable.init, rfl⟩
  | @step w state a action state' hprev happly ih =>
      rcases state with ⟨⟨q, memory⟩, z⟩
      rcases state' with ⟨⟨q', memory'⟩, z'⟩
      rcases ih with ⟨actions, htrace, hmemory⟩
      rcases (rememberWindow_apply_iff V k a action q q' memory memory' z z').1
        happly with ⟨horiginal, htarget⟩
      refine ⟨actions ++ [action],
        TracedReachable.step a action htrace horiginal, ?_⟩
      rw [windowOf_append, hmemory]
      exact htarget.symm

/-- The refined frontier is exactly the original traced frontier classified by
its stored action window, for every prefix including epsilon. -/
theorem frontier_window_iff (V : PartialVisible.Machine Input Q Γ) (k : Nat)
    (w : List Input) (memory : ActionWindow k) (q : Q) (z : List Γ) :
    (rememberWindow V k).Frontier w (q, memory) z ↔
      WindowFrontier V k w memory q z := by
  rw [PartialVisible.Machine.frontier_iff_tagged]
  constructor
  · intro h
    exact remembered_to_traced V k h
  · rintro ⟨actions, htrace, hmemory⟩
    have hrefined := traced_to_remembered V k htrace
    simpa [hmemory] using hrefined

/-! ## Separation and compilation -/

/-- Window separation on the original traced semantics makes the canonical
refined frontier control-functional. -/
theorem rememberWindow_controlFunctional
    (V : PartialVisible.Machine Input Q Γ) (k : Nat)
    (hsep : WindowSeparated V k) :
    ControlFunctionalOn (rememberWindow V k) := by
  intro w state z₁ z₂ h₁ h₂
  rcases state with ⟨q, memory⟩
  exact hsep w memory q z₁ z₂
    ((frontier_window_iff V k w memory q z₁).1 h₁)
    ((frontier_window_iff V k w memory q z₂).1 h₂)

/-- A supplied enumeration of the full bounded-window control carrier compiles
the original forgotten-action projection. -/
theorem compiled_decides_window {s : Nat}
    (V : PartialVisible.Machine Input Q Γ) (k : Nat)
    (hsep : WindowSeparated V k)
    (e : ControlEquiv (Q × ActionWindow k) (Fin s))
    (w : List Input) :
    (RootSharingMachine.compile
      (ControlFunctional.executor (rename (rememberWindow V k) e))).decides w =
        true ↔ V.Accepts w := by
  exact compiled_decides_original_via_equiv (rememberWindowRefinement V k) e
    (rememberWindow_controlFunctional V k hsep) w

#check TracedReachable
#check WindowFrontier
#check rememberWindowRefinement
#check frontier_window_iff
#check rememberWindow_controlFunctional
#check compiled_decides_window

end FrontierDerivative.BoundedActionWindow