RejectingSink.lean

import FrontierDerivative.FrontierAllocator

/-!
# Pruning an absorbing rejecting sink from a total visible machine

The conventional total visible-machine presentation may send failed tagged
commands into a permanent rejecting sink. This module relates that presentation
to the successful partial frontier used by FPRD-T102.
-/

namespace FrontierDerivative

open VisibleAction

variable {Input Q Γ : Type}

/-- A designated nonaccepting control that no visible action can leave. -/
structure RejectingSink (V : VisibleMachine Input Q Γ) where
  sink : Q
  accept_sink : V.accept sink = false
  call_sink : ∀ a, (V.call sink a).1 = sink
  ret_sink : ∀ a top, V.ret sink a top = sink
  local_sink : ∀ a, V.localStep sink a = sink

namespace RejectingSink

/-! ## Total tagged execution -/

/-- Execute one total visible action on a concrete visible configuration. -/
def totalApply (V : VisibleMachine Input Q Γ) (a : Input)
    (action : VisibleAction) (c : PartialVisible.Config Q Γ) :
    PartialVisible.Config Q Γ :=
  match action with
  | .call =>
      let next := V.call c.ctrl a
      ⟨next.1, next.2 :: c.stack⟩
  | .ret => ⟨V.ret c.ctrl a c.stack.head?, c.stack.drop 1⟩
  | .local => ⟨V.localStep c.ctrl a, c.stack⟩

/-- Total tagged execution from an arbitrary visible configuration. -/
def totalRunFrom (V : VisibleMachine Input Q Γ)
    (c : PartialVisible.Config Q Γ)
    (tagged : List (Input × VisibleAction)) : PartialVisible.Config Q Γ :=
  tagged.foldl (fun c t => totalApply V t.1 t.2 c) c

/-- Total tagged execution from the blank initial visible configuration. -/
def totalRun (V : VisibleMachine Input Q Γ)
    (tagged : List (Input × VisibleAction)) : PartialVisible.Config Q Γ :=
  totalRunFrom V ⟨V.init, []⟩ tagged

theorem totalRunFrom_append (V : VisibleMachine Input Q Γ)
    (c : PartialVisible.Config Q Γ)
    (u v : List (Input × VisibleAction)) :
    totalRunFrom V c (u ++ v) =
      totalRunFrom V (totalRunFrom V c u) v := by
  simp [totalRunFrom, List.foldl_append]

theorem totalRun_append (V : VisibleMachine Input Q Γ)
    (tagged : List (Input × VisibleAction)) (a : Input)
    (action : VisibleAction) :
    totalRun V (tagged ++ [(a, action)]) =
      totalApply V a action (totalRun V tagged) := by
  simp [totalRun, totalRunFrom, List.foldl_append]

/-! ## Equality with the existing one-stack evaluator -/

/-- Forget the singleton stack index in the existing strict stack evaluator. -/
def stackProjection (c : FPRD.Config Q Γ 1) : PartialVisible.Config Q Γ :=
  ⟨c.ctrl, c.stacks 0⟩

/-- One existing tagged stack-machine step is exactly one total visible step. -/
theorem stackProjection_step (V : VisibleMachine Input Q Γ)
    (c : FPRD.Config Q Γ 1) (a : Input) (action : VisibleAction) :
    stackProjection (V.stackMachine.stepConfig c (a, action)) =
      totalApply V a action (stackProjection c) := by
  cases action <;>
    simp [stackProjection, VisibleMachine.stackMachine,
      FPRD.StackMachine.stepConfig, FPRD.StackOp.apply, totalApply]

theorem stackProjection_runFrom (V : VisibleMachine Input Q Γ)
    (c : FPRD.Config Q Γ 1)
    (tagged : List (Input × VisibleAction)) :
    stackProjection (tagged.foldl V.stackMachine.stepConfig c) =
      totalRunFrom V (stackProjection c) tagged := by
  induction tagged generalizing c with
  | nil => rfl
  | cons t tagged ih =>
      simp only [List.foldl_cons]
      rw [ih, stackProjection_step]
      rfl

/-- The existing total tagged machine and the direct visible evaluator have
exactly the same final control and stack for every tagged word. -/
theorem stackProjection_run (V : VisibleMachine Input Q Γ)
    (tagged : List (Input × VisibleAction)) :
    stackProjection (V.stackMachine.run tagged) = totalRun V tagged := by
  change stackProjection
      (tagged.foldl V.stackMachine.stepConfig V.stackMachine.initConfig) = _
  rw [stackProjection_runFrom]
  rfl

/-- The existing tagged-machine Boolean readout is exactly the direct total
visible readout. -/
theorem stackMachine_decides_eq_total (V : VisibleMachine Input Q Γ)
    (tagged : List (Input × VisibleAction)) :
    V.stackMachine.decides tagged = V.accept (totalRun V tagged).ctrl := by
  change V.accept (V.stackMachine.run tagged).ctrl = _
  have h := congrArg PartialVisible.Config.ctrl (stackProjection_run V tagged)
  change (V.stackMachine.run tagged).ctrl = (totalRun V tagged).ctrl at h
  rw [h]

/-! ## Pruning commands that enter the rejecting sink -/

/-- Discard exactly the commands whose total target control is the sink. -/
def prune [DecidableEq Q] {V : VisibleMachine Input Q Γ}
    (H : RejectingSink V) : PartialVisible.Machine Input Q Γ where
  call := fun q a =>
    let next := V.call q a
    if next.1 = H.sink then none else some next
  ret := fun q a top =>
    let next := V.ret q a top
    if next = H.sink then none else some next
  localStep := fun q a =>
    let next := V.localStep q a
    if next = H.sink then none else some next
  init := V.init
  accept := V.accept

/-- A total step whose target is not the sink is retained exactly. -/
theorem prune_apply_of_total_nonSink [DecidableEq Q]
    {V : VisibleMachine Input Q Γ} (H : RejectingSink V)
    (a : Input) (action : VisibleAction) (c : PartialVisible.Config Q Γ)
    (h : (totalApply V a action c).ctrl ≠ H.sink) :
    H.prune.apply a action c = some (totalApply V a action c) := by
  cases action <;>
    simp [prune, PartialVisible.Machine.apply, totalApply] at h ⊢ <;>
    exact h

/-- Every successful pruned step is exactly its underlying total step. -/
theorem totalApply_of_prune_apply [DecidableEq Q]
    {V : VisibleMachine Input Q Γ} (H : RejectingSink V)
    (a : Input) (action : VisibleAction) (c c' : PartialVisible.Config Q Γ)
    (h : H.prune.apply a action c = some c') :
    totalApply V a action c = c' := by
  cases action
  · simp [prune, PartialVisible.Machine.apply] at h
    rcases h with ⟨q', b, ⟨_, hnext⟩, hconfig⟩
    simp [totalApply, hnext]
    exact hconfig
  · simp [prune, PartialVisible.Machine.apply] at h
    rcases h with ⟨q', ⟨_, hnext⟩, hconfig⟩
    simp [totalApply, hnext]
    exact hconfig
  · simp [prune, PartialVisible.Machine.apply] at h
    rcases h with ⟨q', ⟨_, hnext⟩, hconfig⟩
    simp [totalApply, hnext]
    exact hconfig

/-- Once the total run is in the sink, every next control is still the sink.
The stack may nevertheless change. -/
theorem totalApply_of_sink {V : VisibleMachine Input Q Γ}
    (H : RejectingSink V) (c : PartialVisible.Config Q Γ)
    (hc : c.ctrl = H.sink) (a : Input) (action : VisibleAction) :
    (totalApply V a action c).ctrl = H.sink := by
  rcases c with ⟨q, z⟩
  change q = H.sink at hc
  subst q
  cases action <;>
    simp [totalApply, H.call_sink, H.ret_sink, H.local_sink]

/-- A final control with true readout cannot be the rejecting sink. -/
theorem accept_true_ne_sink {V : VisibleMachine Input Q Γ}
    (H : RejectingSink V) {q : Q} (h : V.accept q = true) :
    q ≠ H.sink := by
  intro hq
  subst q
  rw [H.accept_sink] at h
  contradiction

/-! ## Two-directional successful-run transfer -/

/-- Every successful pruned derivation is an exact total tagged run on an
explicit same-length annotation. -/
theorem prunedTagged_to_total [DecidableEq Q]
    {V : VisibleMachine Input Q Γ} (H : RejectingSink V)
    {w : List Input} {c : PartialVisible.Config Q Γ}
    (h : H.prune.TaggedReachable w c) :
    ∃ tagged : List (Input × VisibleAction),
      tagged.map Prod.fst = w ∧ totalRun V tagged = c := by
  induction h with
  | init => exact ⟨[], rfl, rfl⟩
  | step a action hprev happly ih =>
      rcases ih with ⟨tagged, hinputs, hrun⟩
      refine ⟨tagged ++ [(a, action)], ?_, ?_⟩
      · simp [hinputs]
      · rw [totalRun_append, hrun]
        exact H.totalApply_of_prune_apply a action _ _ happly

/-- A total tagged run that ends outside the absorbing sink never entered the
sink and therefore has an exact successful pruned derivation. -/
theorem totalNonSink_to_prunedTagged [DecidableEq Q]
    {V : VisibleMachine Input Q Γ} (H : RejectingSink V)
    (tagged : List (Input × VisibleAction))
    (hfinal : (totalRun V tagged).ctrl ≠ H.sink) :
    H.prune.TaggedReachable (tagged.map Prod.fst) (totalRun V tagged) := by
  have hall : ∀ tagged : List (Input × VisibleAction),
      (totalRun V tagged).ctrl ≠ H.sink →
        H.prune.TaggedReachable (tagged.map Prod.fst) (totalRun V tagged) := by
    apply PartialVisible.list_snoc_induction
    · intro _
      exact PartialVisible.Machine.TaggedReachable.init
    · intro u taggedAction ih hnext
      rcases taggedAction with ⟨a, action⟩
      have hprevious : (totalRun V u).ctrl ≠ H.sink := by
        intro hsink
        apply hnext
        rw [totalRun_append]
        exact H.totalApply_of_sink (totalRun V u) hsink a action
      have htarget :
          (totalApply V a action (totalRun V u)).ctrl ≠ H.sink := by
        simpa [totalRun_append] using hnext
      have hreach := ih hprevious
      have happly :=
        H.prune_apply_of_total_nonSink a action (totalRun V u) htarget
      have hstep := PartialVisible.Machine.TaggedReachable.step
        a action hreach happly
      simpa [List.map_append, totalRun_append] using hstep
  exact hall tagged hfinal

/-! ## Projected-language equality and allocator composition -/

/-- Removing the absorbing nonaccepting sink preserves exactly the
forgotten-action language, including at epsilon. -/
theorem projectAccepts_iff_pruned [DecidableEq Q]
    {V : VisibleMachine Input Q Γ} (H : RejectingSink V)
    (w : List Input) :
    ResolverCover.ProjectAccepts V w ↔ H.prune.Accepts w := by
  constructor
  · rintro ⟨tagged, hinputs, haccept⟩
    rw [stackMachine_decides_eq_total] at haccept
    have hreach := H.totalNonSink_to_prunedTagged tagged
      (H.accept_true_ne_sink haccept)
    rw [hinputs] at hreach
    apply (H.prune.accepts_iff_tagged w).2
    exact ⟨totalRun V tagged, hreach, haccept⟩
  · intro hpruned
    have htagged := (H.prune.accepts_iff_tagged w).1 hpruned
    rcases htagged with ⟨c, hreach, haccept⟩
    rcases H.prunedTagged_to_total hreach with
      ⟨tagged, hinputs, hrun⟩
    refine ⟨tagged, hinputs, ?_⟩
    rw [stackMachine_decides_eq_total, hrun]
    exact haccept

/-- Any stationary allocator for the pruned successful frontier decides the
original total projection after the existing T101 compilation. -/
theorem compiled_allocator_decides_total_projection [DecidableEq Q]
    {V : VisibleMachine Input Q Γ} (H : RejectingSink V)
    {Ctrl : Type} {s : Nat}
    {E : RootSharingMachine.Machine Input Ctrl Γ s}
    (K : FrontierAllocator.Allocator H.prune E) (w : List Input) :
    (RootSharingMachine.compile E).decides w = true ↔
      ResolverCover.ProjectAccepts V w := by
  rw [K.compiled_decides_projected]
  exact (H.projectAccepts_iff_pruned w).symm

#check totalRun_append
#check stackProjection_step
#check stackProjection_run
#check stackMachine_decides_eq_total
#check prune_apply_of_total_nonSink
#check totalApply_of_prune_apply
#check totalApply_of_sink
#check accept_true_ne_sink
#check prunedTagged_to_total
#check totalNonSink_to_prunedTagged
#check projectAccepts_iff_pruned
#check compiled_allocator_decides_total_projection

end RejectingSink

end FrontierDerivative