sgl_traj_r

import Definitions.Def_sgl_traj_m

/-!
# The halting hypothesis, bounded by the round count

`RoundHaltingM` asks the delegate to halt within `B` at *every* offset, and no
fixed `B` can honour that: the offset is part of the input, and running time
grows with input.  The loop never asks beyond its own round count, so the
honest hypothesis stops there — and unlike its predecessor, this one is
dischargeable from a polynomial time bound.
-/

namespace SipserGacsLautemann

open Classical

variable {n states : Nat}

/-- The delegate halts within `B` on every round the loop can reach. -/
def RoundHaltingMR (M : Machine 4 states) (xs : Fin 3 → List TapeSymbol)
    (B R : Nat) : Prop :=
  ∀ (Ld : Fin 4 → List TapeSymbol) (m : Nat), m < R →
    (∀ j, ∃ L' : List TapeSymbol,
      Ld j = List.replicate B TapeSymbol.blank ++ L') →
    ∃ Tm : Nat, ∃ v : Bool, 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 v

set_option maxHeartbeats 1000000 in
/-- **One step of the trajectory, margin included.** -/
theorem ostep_existsMR (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 : RoundHaltingMR M xs B R)
    (s : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q) (hidx : s.idx < R) :
    ∃ p : Nat × Nat × Bool × OStateM L gd xs Ls Rs Lclk Lg Rg R B Q,
      p.1 ≤ 80 * s.clock + 13 * ((xs 0).length + (xs 1).length + (xs 2).length)
        + 13 * s.idx + p.2.1 + 178 ∧
      p.2.1 ≤ B ∧
      p.2.2.2.clock = s.clock + p.2.1 ∧
      p.2.2.2.idx = s.idx + 1 ∧
      HaltsExactly (loopBody L gd M) ((loopBody L gd M).startCfg s.tp) p.1
        (decide (s.idx + 1 < R)) ∧
      p.2.2.2.tp = (((loopBody L gd M).step^[p.1])
        ((loopBody L gd M).startCfg s.tp)).tape ∧
      roundVerdict (((loopBody L gd M).step^[p.1])
        ((loopBody L gd M).startCfg s.tp)).state = p.2.2.1 ∧
      guideLeft (((loopBody L gd M).step^[p.1])
        ((loopBody L gd M).startCfg s.tp)).state = decide (s.idx + 1 < R) := by
  classical
  obtain ⟨Ld, hdst⟩ := s.hinv.dstFun
  obtain ⟨Tm, v, hTmB, hlive, hhalt⟩ := hhalts Ld s.idx hidx
    (margin_of_dst L B s.tp s.clock s.hmargin Ld hdst)
  obtain ⟨cost, hcb, hhaltsB, hinv', hrv, hgl, hdstv⟩ :=
    loopBody_dst L hL gd hgc hgd hgn hgs hsc hsn M s.tp xs Ls Rs Lclk Lg Rg
      R s.clock s.idx Tm Ld v hxs s.hinv hidx s.hA
      (roundContent_size xs R s.clock s.idx (le_of_lt hidx) s.hsz s.hszR)
      hdst hlive hhalt
  have hmar : MarginAt L B
      ((((loopBody L gd M).step^[cost])
        ((loopBody L gd M).startCfg s.tp)).tape) (s.clock + Tm) := by
    intro j
    rw [hdstv j]
    refine delegate_leaves_skippable_blanks M
      ⟨M.start, roundTapes Ld xs s.idx⟩ j Tm Q
      ((s.clock + Tm) + (s.clock + Tm)) B ?_ ?_
    · rw [roundTapes_right_length]
      exact hQ s.idx j (le_of_lt hidx)
    · have := s.hszB
      omega
  refine ⟨⟨cost, Tm, v,
    { clock := s.clock + Tm
      idx := s.idx + 1
      tp := (((loopBody L gd M).step^[cost])
        ((loopBody L gd M).startCfg s.tp)).tape
      hA := by have := s.hA; omega
      hsz := by intro i; have := s.hsz i; omega
      hszR := by have := s.hszR; omega
      hszB := by have := s.hszB; omega
      hinv := hinv'
      hmargin := hmar }⟩, hcb, hTmB, rfl, rfl, hhaltsB, rfl, hrv, hgl⟩

end SipserGacsLautemann