ControlFunctional.lean

import FrontierDerivative.FrontierAllocator

/-!
# Control-functional visible frontiers

When every reachable visible control carries at most one stack, the control is
a canonical persistent-stack coordinate. This module constructs one stationary
slot per control and discharges the FPRD-T102 allocator laws. A collision at a
target control is safe precisely because control functionality proves that all
candidate target stacks are equal at the extended prefix.
-/

namespace FrontierDerivative.ControlFunctional

open FrontierDerivative
open PartialVisible
open RootSharing

universe uΓ

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

abbrev Active (s : Nat) := Fin s → Bool

/-- Every reachable control carries at most one concrete stack. -/
def ControlFunctional (V : PartialVisible.Machine Input (Fin s) Γ) : Prop :=
  ∀ w q z₁ z₂, V.Frontier w q z₁ → V.Frontier w q z₂ → z₁ = z₂

/-! ## Stationary source-operation candidates -/

/-- Translate one successful visible command into the corresponding
source-selecting stack operation. -/
def command (V : PartialVisible.Machine Input (Fin s) Γ)
    (a : Input) (tops : Fin s → Option Γ) (source : Fin s)
    (action : VisibleAction) : Option (Fin s × Derive s Γ) :=
  match action with
  | .call =>
      (V.call source a).map fun next => (next.1, .push source next.2)
  | .ret =>
      (V.ret source a (tops source)).map fun q => (q, .pop source)
  | .local =>
      (V.localStep source a).map fun q => (q, .keep source)

/-- An active source/action pair supplies this operation for the displayed
target control. -/
def Candidate (V : PartialVisible.Machine Input (Fin s) Γ)
    (active : Active s) (a : Input) (tops : Fin s → Option Γ)
    (target : Fin s) (op : Derive s Γ) : Prop :=
  ∃ source action,
    active source = true ∧ command V a tops source action = some (target, op)

/-- One stationary candidate for a target, when any exists. Classical choice
denotes an ordinary finite transition table when the carriers are finite. -/
noncomputable def chooseOp (V : PartialVisible.Machine Input (Fin s) Γ)
    (active : Active s) (a : Input) (tops : Fin s → Option Γ)
    (target : Fin s) : Option (Derive s Γ) := by
  classical
  exact if h : ∃ op, Candidate V active a tops target op then
    some (Classical.choose h)
  else
    none

theorem chooseOp_sound (V : PartialVisible.Machine Input (Fin s) Γ)
    (active : Active s) (a : Input) (tops : Fin s → Option Γ)
    (target : Fin s) {op : Derive s Γ}
    (h : chooseOp V active a tops target = some op) :
    Candidate V active a tops target op := by
  classical
  unfold chooseOp at h
  split at h
  next hexists =>
    simp only [Option.some.injEq] at h
    subst op
    exact Classical.choose_spec hexists
  next => contradiction

theorem chooseOp_complete (V : PartialVisible.Machine Input (Fin s) Γ)
    (active : Active s) (a : Input) (tops : Fin s → Option Γ)
    (target : Fin s) {op : Derive s Γ}
    (h : Candidate V active a tops target op) :
    ∃ selected, chooseOp V active a tops target = some selected := by
  classical
  unfold chooseOp
  split
  · exact ⟨_, rfl⟩
  · next hnone => exact False.elim (hnone ⟨op, h⟩)

/-- A command computed from the top vector performs the exact visible step on
the concrete source stack. -/
theorem command_sound (V : PartialVisible.Machine Input (Fin s) Γ)
    (c : RootSharingMachine.Config (Active s) Γ s) (a : Input)
    (source target : Fin s) (action : VisibleAction) (op : Derive s Γ)
    (hcommand : command V a (fun i => (c.stacks i).head?) source action =
      some (target, op)) :
    V.apply a action ⟨source, c.stacks source⟩ =
      some ⟨target, op.apply c.stacks⟩ := by
  cases action
  ·
      cases hcall : V.call source a with
      | none => simp [command, hcall] at hcommand
      | some next =>
          simp [command, hcall] at hcommand
          rcases hcommand with ⟨rfl, rfl⟩
          simp [PartialVisible.Machine.apply, hcall, Derive.apply]
  ·
      cases hret : V.ret source a (c.stacks source).head? with
      | none => simp [command, hret] at hcommand
      | some next =>
          simp [command, hret] at hcommand
          rcases hcommand with ⟨rfl, rfl⟩
          simp [PartialVisible.Machine.apply, hret, Derive.apply]
  ·
      cases hlocal : V.localStep source a with
      | none => simp [command, hlocal] at hcommand
      | some next =>
          simp [command, hlocal] at hcommand
          rcases hcommand with ⟨rfl, rfl⟩
          simp [PartialVisible.Machine.apply, hlocal, Derive.apply]

/-- Every genuine visible successor of an active source supplies a stationary
candidate whose source operation produces the same concrete stack. -/
theorem command_complete (V : PartialVisible.Machine Input (Fin s) Γ)
    (c : RootSharingMachine.Config (Active s) Γ s) (a : Input)
    (source target : Fin s) (action : VisibleAction) (z : List Γ)
    (happly : V.apply a action ⟨source, c.stacks source⟩ = some ⟨target, z⟩) :
    ∃ op,
      command V a (fun i => (c.stacks i).head?) source action =
        some (target, op) ∧
      op.apply c.stacks = z := by
  cases action
  ·
      cases hcall : V.call source a with
      | none => simp [PartialVisible.Machine.apply, hcall] at happly
      | some next =>
          simp [PartialVisible.Machine.apply, hcall] at happly
          rcases happly with ⟨rfl, rfl⟩
          exact ⟨Derive.push source next.2, by
            simp [command, hcall, Derive.apply]⟩
  ·
      cases hret : V.ret source a (c.stacks source).head? with
      | none => simp [PartialVisible.Machine.apply, hret] at happly
      | some next =>
          simp [PartialVisible.Machine.apply, hret] at happly
          rcases happly with ⟨rfl, rfl⟩
          exact ⟨Derive.pop source, by
            simp [command, hret, Derive.apply]⟩
  ·
      cases hlocal : V.localStep source a with
      | none => simp [PartialVisible.Machine.apply, hlocal] at happly
      | some next =>
          simp [PartialVisible.Machine.apply, hlocal] at happly
          rcases happly with ⟨rfl, rfl⟩
          exact ⟨Derive.keep source, by
            simp [command, hlocal, Derive.apply]⟩

/-- Candidate soundness against the exact concrete visible successor. -/
theorem candidate_sound (V : PartialVisible.Machine Input (Fin s) Γ)
    (c : RootSharingMachine.Config (Active s) Γ s) (a : Input)
    (target : Fin s) (op : Derive s Γ)
    (h : Candidate V c.ctrl a (fun i => (c.stacks i).head?) target op) :
    ∃ source action,
      c.ctrl source = true ∧
      V.apply a action ⟨source, c.stacks source⟩ =
        some ⟨target, op.apply c.stacks⟩ := by
  rcases h with ⟨source, action, hactive, hcommand⟩
  exact ⟨source, action, hactive,
    command_sound V c a source target action op hcommand⟩

/-- Candidate completeness against every genuine successor of an active
source configuration. -/
theorem candidate_complete (V : PartialVisible.Machine Input (Fin s) Γ)
    (c : RootSharingMachine.Config (Active s) Γ s) (a : Input)
    (source target : Fin s) (action : VisibleAction) (z : List Γ)
    (hactive : c.ctrl source = true)
    (happly : V.apply a action ⟨source, c.stacks source⟩ = some ⟨target, z⟩) :
    ∃ op,
      Candidate V c.ctrl a (fun i => (c.stacks i).head?) target op ∧
      op.apply c.stacks = z := by
  rcases command_complete V c a source target action z happly with
    ⟨op, hcommand, hop⟩
  exact ⟨op, ⟨source, action, hactive, hcommand⟩, hop⟩

/-! ## One-slot-per-control executor -/

def coordinates : FrontierAllocator.Coordinates (Active s) (Fin s) s where
  slotState := fun active q => if active q then some q else none

theorem rep_iff (c : RootSharingMachine.Config (Active s) Γ s)
    (q : Fin s) (z : List Γ) :
    coordinates.Rep c q z ↔ c.ctrl q = true ∧ c.stacks q = z := by
  classical
  constructor
  · rintro ⟨i, hstate, hstack⟩
    cases hactive : c.ctrl i with
    | false => simp [coordinates, hactive] at hstate
    | true =>
        simp [coordinates, hactive] at hstate
        subst q
        exact ⟨hactive, hstack⟩
  · rintro ⟨hactive, hstack⟩
    exact ⟨q, by simp [coordinates, hactive], hstack⟩

/-- Stationary one-slot-per-control executor. -/
noncomputable def executor (V : PartialVisible.Machine Input (Fin s) Γ) :
    RootSharingMachine.Machine Input (Active s) Γ s where
  init := fun q => decide (q = V.init)
  accept := fun active => decide (∃ q, active q = true ∧ V.accept q = true)
  step := fun active a tops =>
    let selected := fun q => chooseOp V active a tops q
    (fun q => (selected q).isSome,
      fun q => (selected q).getD (.keep V.init))

theorem executor_step_of_choice
    (V : PartialVisible.Machine Input (Fin s) Γ)
    (c : RootSharingMachine.Config (Active s) Γ s) (a : Input)
    (q : Fin s) (op : Derive s Γ)
    (h : chooseOp V c.ctrl a (fun i => (c.stacks i).head?) q = some op) :
    ((executor V).stepConfig c a).ctrl q = true ∧
      ((executor V).stepConfig c a).stacks q = op.apply c.stacks := by
  simp [executor, RootSharingMachine.Machine.stepConfig, h]

theorem executor_step_active_choice
    (V : PartialVisible.Machine Input (Fin s) Γ)
    (c : RootSharingMachine.Config (Active s) Γ s) (a : Input)
    (q : Fin s)
    (h : ((executor V).stepConfig c a).ctrl q = true) :
    ∃ op,
      chooseOp V c.ctrl a (fun i => (c.stacks i).head?) q = some op := by
  classical
  change
    (chooseOp V c.ctrl a (fun i => (c.stacks i).head?) q).isSome = true at h
  cases hop : chooseOp V c.ctrl a (fun i => (c.stacks i).head?) q with
  | none => simp [hop] at h
  | some op => exact ⟨op, rfl⟩

/-- A configuration is valid when it exactly represents some reachable source
frontier. This is a proof invariant, not data inspected by the executor. -/
def ReachableExact (V : PartialVisible.Machine Input (Fin s) Γ)
    (c : RootSharingMachine.Config (Active s) Γ s) : Prop :=
  ∃ w, ∀ q z, coordinates.Rep c q z ↔ V.Frontier w q z

/-! ## Exact allocation -/

theorem init_exact (V : PartialVisible.Machine Input (Fin s) Γ)
    (q : Fin s) (z : List Γ) :
    coordinates.Rep (executor V).initConfig q z ↔ V.Frontier [] q z := by
  classical
  rw [rep_iff]
  simp [executor, RootSharingMachine.Machine.initConfig,
    PartialVisible.Machine.Frontier, PartialVisible.Machine.run,
    PartialVisible.Machine.initConfig]

theorem readout_exact (V : PartialVisible.Machine Input (Fin s) Γ)
    (c : RootSharingMachine.Config (Active s) Γ s) :
    ((executor V).accept c.ctrl = true ↔
      ∃ q z, coordinates.Rep c q z ∧ V.accept q = true) := by
  classical
  simp only [executor, decide_eq_true_eq]
  constructor
  · rintro ⟨q, hactive, hfinal⟩
    exact ⟨q, c.stacks q, (rep_iff c q (c.stacks q)).2 ⟨hactive, rfl⟩,
      hfinal⟩
  · rintro ⟨q, z, hrep, hfinal⟩
    exact ⟨q, (rep_iff c q z).1 hrep |>.1, hfinal⟩

/-- Every represented output is a genuine one-letter successor of a
represented input. No functionality hypothesis is needed in this direction. -/
theorem step_rep_sound (V : PartialVisible.Machine Input (Fin s) Γ)
    (c : RootSharingMachine.Config (Active s) Γ s) (a : Input)
    (q : Fin s) (z : List Γ)
    (hrep : coordinates.Rep ((executor V).stepConfig c a) q z) :
    ∃ q0 z0, coordinates.Rep c q0 z0 ∧
      (⟨q, z⟩ : PartialVisible.Config (Fin s) Γ) ∈
        V.successors a ⟨q0, z0⟩ := by
  classical
  have hout := (rep_iff ((executor V).stepConfig c a) q z).1 hrep
  rcases executor_step_active_choice V c a q hout.1 with ⟨op, hchoice⟩
  have hstep := executor_step_of_choice V c a q op hchoice
  have hcand := chooseOp_sound V c.ctrl a
    (fun i => (c.stacks i).head?) q hchoice
  rcases candidate_sound V c a q op hcand with
    ⟨source, action, hactive, happly⟩
  refine ⟨source, c.stacks source,
    (rep_iff c source (c.stacks source)).2 ⟨hactive, rfl⟩, ?_⟩
  rw [PartialVisible.Machine.mem_successors_iff]
  refine ⟨action, ?_⟩
  have hopz : op.apply c.stacks = z := hstep.2.symm.trans hout.2
  simpa [hopz] using happly

/-- At an exactly represented reachable boundary, every genuine successor is
represented after one executor step. If the stationary choice picked another
candidate at the same target, control functionality identifies their stacks
at the extended prefix. -/
theorem step_rep_complete (V : PartialVisible.Machine Input (Fin s) Γ)
    (hfun : ControlFunctional V) (w : List Input)
    (c : RootSharingMachine.Config (Active s) Γ s)
    (hexact : ∀ q z, coordinates.Rep c q z ↔ V.Frontier w q z)
    (a : Input) (q : Fin s) (z : List Γ)
    (hsucc : ∃ q0 z0, coordinates.Rep c q0 z0 ∧
      (⟨q, z⟩ : PartialVisible.Config (Fin s) Γ) ∈
        V.successors a ⟨q0, z0⟩) :
    coordinates.Rep ((executor V).stepConfig c a) q z := by
  classical
  rcases hsucc with ⟨q0, z0, hrep0, hnext⟩
  have hslot0 := (rep_iff c q0 z0).1 hrep0
  rw [PartialVisible.Machine.mem_successors_iff] at hnext
  rcases hnext with ⟨action, happly⟩
  have happly' :
      V.apply a action ⟨q0, c.stacks q0⟩ = some ⟨q, z⟩ := by
    simpa [hslot0.2] using happly
  rcases candidate_complete V c a q0 q action z hslot0.1 happly' with
    ⟨op, hcand, hopz⟩
  rcases chooseOp_complete V c.ctrl a (fun i => (c.stacks i).head?) q hcand with
    ⟨selected, hselected⟩
  have hselectedStep := executor_step_of_choice V c a q selected hselected
  have hselectedCand := chooseOp_sound V c.ctrl a
    (fun i => (c.stacks i).head?) q hselected
  rcases candidate_sound V c a q selected hselectedCand with
    ⟨source, selectedAction, hsourceActive, hselectedApply⟩
  have hsourceRep : coordinates.Rep c source (c.stacks source) :=
    (rep_iff c source (c.stacks source)).2 ⟨hsourceActive, rfl⟩
  have hselectedFrontier :
      V.Frontier (w ++ [a]) q (selected.apply c.stacks) := by
    rw [PartialVisible.Machine.frontier_append]
    refine ⟨source, c.stacks source, (hexact _ _).1 hsourceRep, ?_⟩
    rw [PartialVisible.Machine.mem_successors_iff]
    exact ⟨selectedAction, hselectedApply⟩
  have hzFrontier : V.Frontier (w ++ [a]) q z := by
    rw [PartialVisible.Machine.frontier_append]
    exact ⟨q0, z0, (hexact _ _).1 hrep0,
      (PartialVisible.Machine.mem_successors_iff V a _ _).2
        ⟨action, happly⟩⟩
  have hsame : selected.apply c.stacks = z :=
    hfun (w ++ [a]) q _ _ hselectedFrontier hzFrontier
  exact (rep_iff ((executor V).stepConfig c a) q z).2
    ⟨hselectedStep.1, hselectedStep.2.trans hsame⟩

theorem step_rep_exact (V : PartialVisible.Machine Input (Fin s) Γ)
    (hfun : ControlFunctional V) (w : List Input)
    (c : RootSharingMachine.Config (Active s) Γ s)
    (hexact : ∀ q z, coordinates.Rep c q z ↔ V.Frontier w q z)
    (a : Input) (q : Fin s) (z : List Γ) :
    coordinates.Rep ((executor V).stepConfig c a) q z ↔
      ∃ q0 z0, coordinates.Rep c q0 z0 ∧
        (⟨q, z⟩ : PartialVisible.Config (Fin s) Γ) ∈
          V.successors a ⟨q0, z0⟩ := by
  constructor
  · exact step_rep_sound V c a q z
  · exact step_rep_complete V hfun w c hexact a q z

theorem init_valid (V : PartialVisible.Machine Input (Fin s) Γ) :
    ReachableExact V (executor V).initConfig := by
  exact ⟨[], init_exact V⟩

theorem step_valid (V : PartialVisible.Machine Input (Fin s) Γ)
    (hfun : ControlFunctional V)
    (c : RootSharingMachine.Config (Active s) Γ s) (a : Input)
    (hvalid : ReachableExact V c) :
    ReachableExact V ((executor V).stepConfig c a) := by
  rcases hvalid with ⟨w, hexact⟩
  refine ⟨w ++ [a], fun q z => ?_⟩
  rw [step_rep_exact V hfun w c hexact a q z]
  constructor
  · rintro ⟨q0, z0, hrep, hnext⟩
    exact (PartialVisible.Machine.frontier_append V w a q z).2
      ⟨q0, z0, (hexact _ _).1 hrep, hnext⟩
  · rintro hfrontier
    rcases (PartialVisible.Machine.frontier_append V w a q z).1 hfrontier with
      ⟨q0, z0, hfrontier0, hnext⟩
    exact ⟨q0, z0, (hexact _ _).2 hfrontier0, hnext⟩

/-- The canonical one-slot-per-control construction is a lawful T102
allocator. -/
noncomputable def allocator (V : PartialVisible.Machine Input (Fin s) Γ)
    (hfun : ControlFunctional V) :
    FrontierAllocator.Allocator V (executor V) where
  coordinates := coordinates
  valid := ReachableExact V
  init_valid := init_valid V
  step_valid := step_valid V hfun
  init_exact := init_exact V
  step_exact := by
    intro c a hvalid q z
    rcases hvalid with ⟨w, hexact⟩
    exact step_rep_exact V hfun w c hexact a q z
  readout_exact := by
    intro c _
    exact readout_exact V c

theorem decides (V : PartialVisible.Machine Input (Fin s) Γ)
    (hfun : ControlFunctional V) (w : List Input) :
    (executor V).decides w = true ↔ V.Accepts w :=
  (allocator V hfun).decides_projected w

/-- The existing T102/T101 chain compiles the canonical allocator without a
new scaffold construction. -/
theorem compiled_decides (V : PartialVisible.Machine Input (Fin s) Γ)
    (hfun : ControlFunctional V) (w : List Input) :
    (RootSharingMachine.compile (executor V)).decides w = true ↔ V.Accepts w :=
  (allocator V hfun).compiled_decides_projected w

#check candidate_sound
#check candidate_complete
#check step_rep_exact
#check allocator
#check compiled_decides

end FrontierDerivative.ControlFunctional