sgl_loop_spec_r

import Definitions.Def_sgl_records_r

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

Unchanged from the original but for the carrier.  The loop machine itself is
the same `offsetLoop`; only the records feeding `loopState_spec_v` come from
the trajectory that keeps a margin.
-/

namespace SipserGacsLautemann

open Classical

variable {n states : Nat}

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 : RoundHaltingMR M xs B R)

set_option maxHeartbeats 1000000 in
/-- **The loop, at a stopping round.** -/
theorem offsetLoopMR_at (s₀ : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q)
    (h0 : s₀.idx = 0) (rounds : Nat) (hlt : rounds < R)
    (hbefore : ∀ i, i < rounds → oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i = false)
    (hfire : oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds = true ∨ rounds + 1 = R) :
    HaltsExactly (offsetLoop L gd M)
      (TypedConfiguration.inLoop () (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ 0))
      (loopCost (ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀) rounds + ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds)
      (oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds) := by
  obtain ⟨hhalt, htp, hrv, hgl⟩ := otrajMR_round L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ h0 rounds hlt
  have hstopB : (roundVerdict (((loopBody L gd M).step^[ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds])
        (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds)).state ||
      !guideLeft (((loopBody L gd M).step^[ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds])
        (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds)).state) = true := by
    rw [hrv, hgl]
    rcases hfire with h | h
    · rw [h]
      rfl
    · rw [decide_eq_false (by omega : ¬ rounds + 1 < R)]
      simp
  have hmain := TypedMachine.loopState_spec_v
    (fun _ : Unit => loopBody L gd M) (fun _ _ => ())
    (fun _ b => roundVerdict b || !(guideLeft b))
    (fun _ b => roundVerdict b) ()
    (fun _ : Nat => ()) (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀) (ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀) rounds
    (ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds) (decide (rounds + 1 < R))
    (fun i hi => offsetMR_record 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 (by omega) (hbefore i hi))
    hhalt hstopB
  have hmain' : HaltsExactly (offsetLoop L gd M)
      (TypedConfiguration.inLoop () (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ 0))
      (loopCost (ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀) rounds + ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds)
      (roundVerdict (((loopBody L gd M).step^[ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds])
        (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds)).state) := hmain
  rw [hrv] at hmain'
  exact hmain'

set_option maxHeartbeats 1000000 in
/-- **The scheduler.** -/
theorem offsetLoopMR_spec (s₀ : OStateM L gd xs Ls Rs Lclk Lg Rg R B Q)
    (h0 : s₀.idx = 0) (hR : 1 ≤ R) :
    ∃ rounds : Nat, rounds < R ∧
      HaltsExactly (offsetLoop L gd M)
        (TypedConfiguration.inLoop () (oconfigMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ 0))
        (loopCost (ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀) rounds + ocostMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds)
        (decide (∃ i, i < R ∧ oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i = true)) := by
  classical
  by_cases hacc : ∃ i, i < R ∧ oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i = true
  · obtain ⟨hlt, hans⟩ := Nat.find_spec hacc
    have hbef : ∀ i, i < Nat.find hacc → oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i = false := by
      intro i hi
      have hmin := Nat.find_min hacc hi
      have hiR : i < R := by omega
      cases hb : oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i with
      | false => rfl
      | true => exact absurd ⟨hiR, hb⟩ hmin
    have hloop := offsetLoopMR_at L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ h0 (Nat.find hacc) hlt hbef
      (Or.inl hans)
    rw [hans] at hloop
    refine ⟨Nat.find hacc, hlt, ?_⟩
    rw [decide_eq_true hacc]
    exact hloop
  · have hans : oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ (R - 1) = false := by
      cases hb : oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ (R - 1) with
      | false => rfl
      | true => exact absurd ⟨R - 1, by omega, hb⟩ hacc
    have hbef : ∀ i, i < R - 1 → oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i = false := by
      intro i hi
      cases hb : oansMR L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i with
      | false => rfl
      | true => exact absurd ⟨i, by omega, hb⟩ hacc
    have hloop := offsetLoopMR_at L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ h0 (R - 1) (by omega) hbef
      (Or.inr (by omega))
    rw [hans] at hloop
    refine ⟨R - 1, by omega, ?_⟩
    rw [decide_eq_false hacc]
    exact hloop

end

end SipserGacsLautemann