sgl_loop_answer

import Definitions.Def_sgl_answer_m

/-!
# The scheduler's verdict and cost together

The two halves of the specification, joined: the loop halts with the
delegate's own answer to the bounded existential, inside the polynomial bound.
-/

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

set_option maxHeartbeats 1000000 in
/-- **The scheduler's verdict and cost, in the delegate's own terms.** -/
theorem offsetLoopM_answer (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)
    (hR : 1 ≤ R) :
    ∃ cost : Nat,
      cost ≤ (R + 1) * (80 * (s₀.clock + R * B)
        + 13 * ((xs 0).length + (xs 1).length + (xs 2).length)
        + 13 * R + B + 179) ∧
      HaltsExactly (offsetLoop L gd M)
        (TypedConfiguration.inLoop () (oconfigM L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ 0)) cost
        (decide (∃ i, i < R ∧ ans i = true)) := by
  classical
  obtain ⟨rounds, hlt, hloop⟩ := offsetLoopM_spec L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ h0 hR
  have hiff : (∃ i, 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 = true) ↔
      (∃ i, i < R ∧ ans i = true) := by
    constructor
    · rintro ⟨i, hi, hv⟩
      exact ⟨i, hi, by rw [← oansM_eq L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts ans hU s₀ h0 i hi]; exact hv⟩
    · rintro ⟨i, hi, hv⟩
      exact ⟨i, hi, by rw [oansM_eq L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts ans hU s₀ h0 i hi]; exact hv⟩
  rw [decide_eq_decide.mpr hiff] at hloop
  refine ⟨_, ?_, hloop⟩
  set K := 80 * (s₀.clock + R * B)
    + 13 * ((xs 0).length + (xs 1).length + (xs 2).length)
    + 13 * R + B + 178 with hK
  clear_value K
  have hall : ∀ i, i < rounds → ocostM L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ i ≤ K := by
    intro i hi
    rw [hK]
    exact ocostM_le 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)
  have h1 := loopCost_le_of hall
  have h2 := ocostM_le 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 h3 : rounds * (K + 1) ≤ R * (K + 1) :=
    Nat.mul_le_mul_right _ (by omega)
  rw [← hK] at h2
  calc loopCost (ocostM L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀) rounds + ocostM L hL gd hgc hgd hgn hgs hsc hsn M xs Ls Rs Lclk Lg Rg R B Q hxs hQ hhalts s₀ rounds
      ≤ rounds * (K + 1) + K := by omega
    _ ≤ R * (K + 1) + (K + 1) := by omega
    _ = (R + 1) * (K + 1) := (Nat.succ_mul R (K + 1)).symm
    _ = (R + 1) * (80 * (s₀.clock + R * B)
          + 13 * ((xs 0).length + (xs 1).length + (xs 2).length)
          + 13 * R + B + 179) := by rw [hK]

end

end SipserGacsLautemann