FrontierAllocator.lean

import FrontierDerivative.PartialVisible
import FrontierDerivative.RootSharingMachine

/-!
# Stationary allocation of forgotten-action frontiers

An allocator assigns the exact successful partial-visible frontier to a fixed
family of persistent stack slots. Its executor is precisely the
source-selecting machine compiled by FPRD-T101. The laws below expose the
stationary allocation obligation; they do not derive it from a per-prefix
cardinality bound.
-/

namespace FrontierDerivative.FrontierAllocator

universe u

variable {Input Q Ctrl : Type} {Γ : Type u} {s : Nat}

/-- Finite-control metadata saying which visible control, if any, each fixed
stack slot currently represents. Finiteness is imposed only at the external
LMR boundary. -/
structure Coordinates (Ctrl : Type) (Q : Type) (s : Nat) where
  slotState : Ctrl → Fin s → Option Q

namespace Coordinates

/-- Extensional frontier relation represented by one allocator configuration.
Inactive slots contribute nothing; duplicate active slots are harmless. -/
def Rep (D : Coordinates Ctrl Q s)
    (c : RootSharingMachine.Config Ctrl Γ s) (q : Q) (z : List Γ) : Prop :=
  ∃ i, D.slotState c.ctrl i = some q ∧ c.stacks i = z

end Coordinates

/--
One stationary exact allocation of a partial visible frontier.

`step_exact` is the unresolved resource obligation in FPRD-C02: the one fixed
source-selecting transition must allocate the complete successor frontier from
the represented current frontier at every reachable input boundary.
-/
structure Allocator (V : PartialVisible.Machine Input Q Γ)
    (E : RootSharingMachine.Machine Input Ctrl Γ s) where
  coordinates : Coordinates Ctrl Q s
  valid : RootSharingMachine.Config Ctrl Γ s → Prop
  init_valid : valid E.initConfig
  step_valid : ∀ c a, valid c → valid (E.stepConfig c a)
  init_exact : ∀ q z,
    coordinates.Rep E.initConfig q z ↔ V.Frontier [] q z
  step_exact : ∀ c a, valid c → ∀ q z,
    coordinates.Rep (E.stepConfig c a) q z ↔
      ∃ q0 z0, coordinates.Rep c q0 z0 ∧
        (⟨q, z⟩ : PartialVisible.Config Q Γ) ∈
          V.successors a ⟨q0, z0⟩
  readout_exact : ∀ c, valid c →
    (E.accept c.ctrl = true ↔
      ∃ q z, coordinates.Rep c q z ∧ V.accept q = true)

namespace Allocator

variable {V : PartialVisible.Machine Input Q Γ}
variable {E : RootSharingMachine.Machine Input Ctrl Γ s}

/-- The allocator invariant holds after every observed prefix. -/
theorem run_valid (K : Allocator V E) (w : List Input) :
    K.valid (E.run w) := by
  have hall : ∀ w : List Input, K.valid (E.run w) := by
    apply PartialVisible.list_snoc_induction
    · exact K.init_valid
    · intro u a ih
      rw [RootSharingMachine.Machine.run_append]
      exact K.step_valid (E.run u) a ih
  exact hall w

/-- The fixed slots denote exactly the successful forgotten-action frontier
after every prefix. -/
theorem run_exact (K : Allocator V E) (w : List Input) (q : Q)
    (z : List Γ) :
    K.coordinates.Rep (E.run w) q z ↔ V.Frontier w q z := by
  have hall : ∀ w : List Input, ∀ q z,
      K.coordinates.Rep (E.run w) q z ↔ V.Frontier w q z := by
    apply PartialVisible.list_snoc_induction
    · intro q z
      exact K.init_exact q z
    · intro u a ih q z
      rw [RootSharingMachine.Machine.run_append]
      rw [K.step_exact (E.run u) a (K.run_valid u)]
      rw [PartialVisible.Machine.frontier_append]
      constructor
      · rintro ⟨q0, z0, hrep, hnext⟩
        exact ⟨q0, z0, (ih q0 z0).1 hrep, hnext⟩
      · rintro ⟨q0, z0, hfrontier, hnext⟩
        exact ⟨q0, z0, (ih q0 z0).2 hfrontier, hnext⟩
  exact hall w q z

/-- The source-selecting executor decides exactly the projected visible
language, including the empty word. -/
theorem decides_projected (K : Allocator V E) (w : List Input) :
    E.decides w = true ↔ V.Accepts w := by
  change E.accept (E.run w).ctrl = true ↔ V.Accepts w
  rw [K.readout_exact (E.run w) (K.run_valid w)]
  rw [PartialVisible.Machine.Accepts]
  constructor
  · rintro ⟨q, z, hrep, hfinal⟩
    exact ⟨q, z, (K.run_exact w q z).1 hrep, hfinal⟩
  · rintro ⟨q, z, hfrontier, hfinal⟩
    exact ⟨q, z, (K.run_exact w q z).2 hfrontier, hfinal⟩

/-- FPRD-T101 compiles the stationary allocator without changing its
projected language. -/
theorem compiled_decides_projected (K : Allocator V E) (w : List Input) :
    (RootSharingMachine.compile E).decides w = true ↔ V.Accepts w := by
  rw [RootSharingMachine.compile_decides]
  exact K.decides_projected w

#check run_valid
#check run_exact
#check decides_projected
#check compiled_decides_projected

end Allocator

end FrontierDerivative.FrontierAllocator