sgl_delegate_ok

import Definitions.Def_sgl_offset_input
import Definitions.Def_sgl_first_halt

/-!
# The delegate's obligations, discharged

This is where the whole debris argument pays off.  A machine's correctness is
given on clean `Tape.ofBits` tapes; the round runs it on tapes that carry a
blank margin and then debris.  Locality says the two are indistinguishable for
as many steps as the margin is wide, and the delegate's own time bound is that
many.  So the answer the round reads is the answer the machine was specified to
give.
-/

namespace SipserGacsLautemann

variable {states : Nat}

set_option maxHeartbeats 1000000 in
/-- **The delegate answers uniformly behind a margin.** -/
theorem roundUniformM_of_correct (M : Machine 4 states)
    (input : Fin 3 → List Bool) (P : (Fin 4 → List Bool) → Prop)
    [DecidablePred P] (T : Nat → Nat) (B : Nat)
    (hcorrect : ∀ inp : Fin 4 → List Bool,
      (M.acceptsWithin inp (T (totalInputLength inp)) ↔ P inp) ∧
      (M.rejectsWithin inp (T (totalInputLength inp)) ↔ ¬ P inp))
    (hTB : ∀ m, T (totalInputLength (offsetInput input m)) ≤ B) :
    RoundUniformM M (fun i => (input i).map TapeSymbol.bit) B
      (fun m => decide (P (offsetInput input m))) := by
  classical
  intro Ld m hmar
  set inp := offsetInput input m with hinp
  set t := T (totalInputLength inp) with ht
  set v := decide (P inp) with hv
  -- the machine's verdict on clean tapes
  have hclean : M.result ((M.step^[t])
      ⟨M.start, fun j => Tape.ofBits (inp j)⟩).state = some v := by
    have hrun : (M.step^[t]) ⟨M.start, fun j => Tape.ofBits (inp j)⟩ =
        M.run inp t := by
      rw [Machine.run_eq_iterate]
      rfl
    rw [hrun]
    by_cases hP : P inp
    · have := (hcorrect inp).1.mpr hP
      rw [hv, decide_eq_true hP]
      exact this
    · have := (hcorrect inp).2.mpr hP
      rw [hv, decide_eq_false hP]
      exact this
  obtain ⟨Tm, hTmt, hlive, hhalt⟩ :=
    Machine.firstHalt M ⟨M.start, fun j => Tape.ofBits (inp j)⟩ t v hclean
  -- the round's tapes agree with the clean ones
  have hagree : ∀ j, TapeAgree (B + 1) (Tape.ofBits (inp j))
      (roundTapes Ld (fun i => (input i).map TapeSymbol.bit) m j) := by
    intro j
    obtain ⟨L', hL'⟩ := hmar j
    have hcells : Tape.ofBits (inp j) =
        cellsTape [] (roundContent (fun i => (input i).map TapeSymbol.bit)
          m j) := by
      rw [ofBits_cellsTape, roundContent_offsetInput]
    rw [hcells]
    exact (roundTapes_agree B Ld (fun i => (input i).map TapeSymbol.bit) m j
      L' hL').symm
  have hTBm : t ≤ B := by
    have h := hTB m
    rw [← hinp, ← ht] at h
    exact h
  have hle : Tm ≤ B + 1 := by omega
  obtain ⟨hlive', hhalt'⟩ := halts_agree M
    (fun j => Tape.ofBits (inp j))
    (roundTapes Ld (fun i => (input i).map TapeSymbol.bit) m)
    (B + 1) Tm v hle hagree hlive hhalt
  exact ⟨Tm, by omega, hlive', hhalt'⟩

end SipserGacsLautemann