sgl_answer_m

import Definitions.Def_sgl_cost_m

/-!
# The scheduler's answer, over the margin-carrying trajectory

The recorded verdict is not literally the one a fresh appeal to the delegate
produces, so it is identified by uniqueness — the two rounds halt at the same
step, hence share a terminal state.
-/

namespace SipserGacsLautemann

open Classical

variable {n states : Nat}

/-- The delegate answers `ans m` at offset `m`, whatever debris sits behind
the blank margin. -/
def RoundUniformM (M : Machine 4 states) (xs : Fin 3 → List TapeSymbol)
    (B : Nat) (ans : Nat → Bool) : Prop :=
  ∀ (Ld : Fin 4 → List TapeSymbol) (m : Nat),
    (∀ j, ∃ L' : List TapeSymbol,
      Ld j = List.replicate B TapeSymbol.blank ++ L') →
    ∃ Tm : Nat, Tm ≤ B ∧
      (∀ t, t < Tm → M.result
        ((M.step^[t]) ⟨M.start, roundTapes Ld xs m⟩).state = none) ∧
      M.result ((M.step^[Tm]) ⟨M.start, roundTapes Ld xs m⟩).state =
        some (ans m)

theorem roundHaltingM_of_uniform {M : Machine 4 states}
    {xs : Fin 3 → List TapeSymbol} {B : Nat} {ans : Nat → Bool}
    (h : RoundUniformM M xs B ans) : RoundHaltingM M xs B := by
  intro Ld m hmar
  obtain ⟨Tm, hB, hlive, hhalt⟩ := h Ld m hmar
  exact ⟨Tm, ans m, hB, hlive, hhalt⟩

section

variable (L : RoundLayout n) (hL : L.Wf) (gd : Fin n)
  (hgc : gd ≠ L.clk) (hgd : ∀ j, gd ≠ L.dst j) (hgn : gd ≠ L.cnt)
  (hgs : ∀ i, gd ≠ L.src i) (hsc : ∀ i, L.src i ≠ L.clk)
  (hsn : ∀ i, L.src i ≠ L.cnt)
  (M : Machine 4 states)
  (xs Ls Rs : Fin 3 → List TapeSymbol) (Lclk Lg Rg : List TapeSymbol)
  (R B Q : Nat) (hxs : ∀ i, ∀ x ∈ xs i, x ≠ TapeSymbol.blank)
  (hQ : ∀ m j, m ≤ R → (roundContent xs m j).length ≤ Q)
  (hhalts : RoundHaltingM M xs B)

set_option maxHeartbeats 1000000 in
/-- **The recorded verdict is the delegate's answer.** -/
theorem ostepM_answer (ans : Nat → Bool) (hU : RoundUniformM M xs B ans)
    (t : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q) (i : Nat) (hti : t.idx = i)
    (hi : i < R) :
    (ostepM L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t).2.2.1 = ans i := by
  classical
  subst hti
  obtain ⟨Ld, hdst⟩ := t.hinv.dstFun
  obtain ⟨Tm, hTmB, hlive, hhalt⟩ := hU Ld t.idx
    (margin_of_dst L B t.tp t.clock t.hmargin Ld hdst)
  obtain ⟨cost, hcb, hhaltsB, hinv', hrv, hgl⟩ :=
    loopBody_spec L hL gd hgc hgd hgn hgs hsc hsn M t.tp xs Ls Rs Lclk Lg Rg
      R t.clock t.idx Tm Ld (ans t.idx) hxs t.hinv hi t.hA
      (roundContent_size xs R t.clock t.idx (le_of_lt hi) t.hsz t.hszR)
      hdst hlive hhalt
  obtain ⟨hrec, htp, hrv2, hgl2⟩ := ostepM_round L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t t.idx rfl hi
  have hcost : (ostepM L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts t).1 = cost := hrec.unique hhaltsB
  rw [← hrv2, hcost]
  exact hrv

theorem oansM_eq (ans : Nat → Bool) (hU : RoundUniformM M xs B ans)
    (s₀ : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q) (h0 : s₀.idx = 0)
    (i : Nat) (hi : i < R) :
    oansM L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i = ans i :=
  ostepM_answer L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts ans hU (otrajM L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i) i
    (otrajM_idx L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ h0 i (le_of_lt hi)) hi


end

end SipserGacsLautemann