import Sal.ConditionedMRDTs.MRDT_Instances.SidedRGA.SidedRGA_Intent

/-!
# Sequential-spec soundness: the sided embedded-chain RGA

Tier 3 (`EmbedRGA_SeqSpec.lean`) at the sided instance: the naive
TWO-SIDED text buffer. Entries are `(id, element)` pairs plus a root
SENTINEL entry (id 0) kept in the buffer so both insert directions have a
splice point: `ins … a R` splices immediately AFTER `a`'s entry, `ins … a
L` immediately BEFORE it, `del x` filters; the read drops the sentinel.
Because the sentinel is always present, the front insert is not a special
case: the anchor `a = 0` IS the sentinel.

The heart is the pair of **sided adjacency lemmas** at the kernel order
(`schainBefore_snocR_iff`, `schainBefore_snocL_iff`): a fresh R-extension
of an anchor displays immediately after it (its delta beats every
existing R-continuation, by sum-telescoping against the fresh stamp, and
the anchor's L-descendants sit on the other side), and a fresh
L-extension displays immediately before it (the L band is mirrored, so
the newest L-child hugs the node from above). The rooted fold `sRFold`
(the canonical state seeded with the sentinel record) makes both lemmas
apply uniformly, root anchor included: the sentinel's chain is `[]`.

Capstone: `sided_seq_sound`, under the datatype's own sequential
discipline `sSeqOK` (monotone insert stamps + `sApplicable` at each
fold), the rooted canonical state IS the two-sided buffer program, record
for record; `sided_seq_read` drops the sentinel on both sides.
-/

namespace Sal.ConditionedMRDTs

open Sal.Emulation
open Sal.EmbedRGA (OrderedPrefixCode keyLt sKey sBlock Side SChain
  PosSChain sidedCoordOf sidedCoordOf_append sidedCoordOf_inj unaryCode
  schainBefore schainBefore_inv sEntryBefore keyLt_total keyLt_irrefl
  keyLt_asymm sdisplay_iff_schainBefore)

set_option linter.unusedSectionVars false

/-! ## §A  The naive two-sided buffer -/

/-- The user-visible projection of a record: `(id, element)`. -/
def sProj (r : SRec) : ℕ × ℕ := (r.1, r.2.1)

/-- The sentinel record: id 0, the empty coordinate (the virtual root's
key `[3]` sits exactly between the root's L-region and R-region). -/
def rootRec : SRec := (0, 0, [])

/-- Splice `p` immediately after the entry with id `a`. -/
def sInsAfter (a : ℕ) (p : ℕ × ℕ) : List (ℕ × ℕ) → List (ℕ × ℕ)
  | [] => []
  | q :: qs => if q.1 = a then q :: p :: qs else q :: sInsAfter a p qs

/-- Splice `p` immediately before the entry with id `a`. -/
def sInsBefore (a : ℕ) (p : ℕ × ℕ) : List (ℕ × ℕ) → List (ℕ × ℕ)
  | [] => []
  | q :: qs => if q.1 = a then p :: q :: qs else q :: sInsBefore a p qs

/-- The naive two-sided buffer program. -/
def sSpecStep (S : List (ℕ × ℕ)) (o : Op SOp) : List (ℕ × ℕ) :=
  match o.2.2 with
  | .ins el _ a sd =>
      match sd with
      | Side.R => sInsAfter a (o.1, el) S
      | Side.L => sInsBefore a (o.1, el) S
  | .del x => S.filter (fun p => decide (p.1 ≠ x))

def sSpecFold (ρ : List (Op SOp)) : List (ℕ × ℕ) :=
  ρ.foldl sSpecStep [(0, 0)]

theorem sSpecFold_snoc (ρ : List (Op SOp)) (o : Op SOp) :
    sSpecFold (ρ ++ [o]) = sSpecStep (sSpecFold ρ) o := by
  unfold sSpecFold
  rw [List.foldl_append]
  rfl

/-! ## §B  The rooted fold -/

/-- The canonical state seeded with the sentinel. -/
def sRFold (Γ : OrderedPrefixCode) (ρ : List (Op SOp)) : SState :=
  ρ.foldl (sUpdate Γ) [rootRec]

theorem sRFold_snoc (Γ : OrderedPrefixCode) (ρ : List (Op SOp))
    (o : Op SOp) : sRFold Γ (ρ ++ [o]) = sUpdate Γ (sRFold Γ ρ) o := by
  unfold sRFold
  rw [List.foldl_append]
  rfl

/-! ## §C  Sequential honesty -/

/-- Sequential honesty: stamps exceed all previous insert stamps
(Lamport), and every op is applicable at the current (unrooted) fold,
the instance's own §8 issuer guard, specialized to a linear history. -/
def sSeqOK (Γ : OrderedPrefixCode) (ρ : List (Op SOp)) : Prop :=
  ∀ (σ : List (Op SOp)) (o : Op SOp) (τ : List (Op SOp)),
    ρ = σ ++ o :: τ →
    (∀ x ∈ sInsIds σ, x < o.1) ∧ sApplicable o (sFold Γ σ)

theorem sSeqOK_prefix {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    {o : Op SOp} (h : sSeqOK Γ (ρ ++ [o])) : sSeqOK Γ ρ := by
  intro σ o' τ heq
  exact h σ o' (τ ++ [o]) (by rw [heq]; simp)

/-! ## §D  Chains for every insert of the history -/

/-- Every insert of a sequentially honest history mints a positive sided
chain's coordinate whose deltas telescope to its (positive) id. -/
theorem s_seq_chains {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    (hOK : sSeqOK Γ ρ) :
    ∀ o ∈ ρ, sIsIns o = true →
      ∃ ch, PosSChain ch ∧ ((ch.map Prod.snd).sum = o.1) ∧ 1 ≤ o.1 ∧
        sCoord Γ o = sidedCoordOf Γ ch := by
  induction ρ using List.reverseRecOn with
  | nil =>
      intro o ho
      simp at ho
  | append_singleton ρ o' ih =>
      intro o ho hins
      rcases List.mem_append.mp ho with h | h
      · exact ih (sSeqOK_prefix hOK) o h hins
      · simp at h
        subst h
        obtain ⟨ts, r, op⟩ := o
        cases op with
        | del x => simp [sIsIns] at hins
        | ins el π a sd =>
            have happ := (hOK ρ (ts, r, .ins el π a sd) [] (by simp)).2
            simp only [sApplicable] at happ
            obtain ⟨hat, hcase⟩ := happ
            have hat' : a < ts := hat
            have hts1 : (1:ℕ) ≤ ts :=
              Nat.lt_of_le_of_lt (Nat.zero_le a) hat'
            rcases hcase with ⟨rfl, rfl⟩ | ⟨el', hmem⟩
            · refine ⟨[(sd, ts)], ?_, by simp, hts1, ?_⟩
              · intro e he
                simp at he
                rw [he]
                show 1 ≤ ts
                exact hts1
              · show [] ++ sBlock Γ (sd, ts - 0) = _
                simp [sidedCoordOf]
            · obtain ⟨aop, haρ, hai, hae⟩ :=
                s_fold_rec_sub Γ ρ (a, el', π) hmem
              have hπ : π = sCoord Γ aop :=
                congrArg (fun q : SRec => q.2.2) hae
              have ha1 : aop.1 = a := (congrArg Prod.fst hae).symm
              obtain ⟨cha, hpos, hsum, -, hcoord⟩ :=
                ih (sSeqOK_prefix hOK) aop haρ hai
              refine ⟨cha ++ [(sd, ts - a)], ?_, ?_, hts1, ?_⟩
              · intro e he
                rcases List.mem_append.mp he with h' | h'
                · exact hpos e h'
                · simp at h'
                  rw [h']
                  show 1 ≤ ts - a
                  exact Nat.le_sub_of_add_le (Nat.add_comm 1 a ▸ hat')
              · rw [List.map_append, List.sum_append, hsum, ha1]
                simp
                exact Nat.add_sub_cancel' (Nat.le_of_lt hat')
              · show π ++ sBlock Γ (sd, ts - a) = _
                rw [sidedCoordOf_append, hπ, hcoord]
                simp [sidedCoordOf]

/-! ## §D′  Well-formedness from sequential honesty -/

theorem sInsIds_lt_of_seqOK {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    {o : Op SOp} (hOK : sSeqOK Γ (ρ ++ [o])) :
    ∀ x ∈ sInsIds ρ, x < o.1 :=
  (hOK ρ o [] (by simp)).1

theorem sWf_of_seqOK {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    (hOK : sSeqOK Γ ρ) : SWf Γ ρ := by
  constructor
  case ins_nodup =>
      induction ρ using List.reverseRecOn with
      | nil => simp [sInsIds]
      | append_singleton ρ o ih =>
          rw [sInsIds_append, List.nodup_append]
          refine ⟨ih (sSeqOK_prefix hOK), ?_, ?_⟩
          · cases o' : o.2.2 <;> simp [sInsIds, sIsIns, o']
          · intro a ha b hb
            have hlt := sInsIds_lt_of_seqOK hOK a ha
            have hb1 : b = o.1 := by
              simp only [sInsIds, List.mem_map, List.mem_filter] at hb
              obtain ⟨o', ⟨ho', -⟩, rfl⟩ := hb
              simp at ho'
              rw [ho']
            omega
  case del_late =>
      intro σ o τ heq hins hdel
      obtain ⟨d, hd, hddel⟩ := mem_sDels.mp hdel
      obtain ⟨σ₁, σ₂, rfl⟩ := List.append_of_mem hd
      have happ := (hOK σ₁ d (σ₂ ++ o :: τ) (by rw [heq]; simp)).2
      obtain ⟨ts, rr, dop2⟩ := d
      cases dop2 with
      | ins el π a sd => simp at hddel
      | del x =>
          simp only [sApplicable] at happ
          simp only at hddel
          injection hddel with hx
          subst hx
          obtain ⟨rec, hrec, hrx⟩ := List.mem_map.mp happ
          obtain ⟨iop, hiρ, hii, hie⟩ := s_fold_rec_sub Γ σ₁ rec hrec
          have hix : iop.1 = o.1 → False := by
            intro hcontra
            have hmem : o.1 ∈ sInsIds (σ₁ ++ (ts, rr, SOp.del o.1) :: σ₂) := by
              rw [show σ₁ ++ (ts, rr, SOp.del o.1) :: σ₂ =
                  (σ₁ ++ [(ts, rr, SOp.del o.1)]) ++ σ₂ from by simp,
                sInsIds_append, sInsIds_append]
              exact List.mem_append_left _ (List.mem_append_left _
                (mem_sInsIds.mpr ⟨iop, hiρ, hii, hcontra⟩))
            have := (hOK (σ₁ ++ (ts, rr, SOp.del o.1) :: σ₂) o τ
              (by simp [heq])).1 o.1 hmem
            omega
          apply hix
          rw [hie] at hrx
          exact hrx
  case keys_inj =>
      intro o₁ h₁ o₂ h₂ hi₁ hi₂ hne hkey
      obtain ⟨ch₁, hp₁, hs₁, -, hc₁⟩ := s_seq_chains hOK o₁ h₁ hi₁
      obtain ⟨ch₂, hp₂, hs₂, -, hc₂⟩ := s_seq_chains hOK o₂ h₂ hi₂
      rw [hc₁, hc₂] at hkey
      have hco := sKey_inj hkey
      have hch := sidedCoordOf_inj Γ hp₁ hp₂ hco
      rw [← hs₁, ← hs₂, hch] at hne
      exact hne rfl

/-! ## §E  Rooted-fold structure -/

/-- Chain package for a live record of the unrooted fold. -/
theorem s_fold_chain {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    (hOK : sSeqOK Γ ρ) {rec : SRec} (hrec : rec ∈ sFold Γ ρ) :
    ∃ ch, PosSChain ch ∧ ((ch.map Prod.snd).sum = rec.1) ∧
      rec.2.2 = sidedCoordOf Γ ch := by
  obtain ⟨iop, hiρ, hii, hie⟩ := s_fold_rec_sub Γ ρ rec hrec
  obtain ⟨ch, h1, h2, -, h4⟩ := s_seq_chains hOK iop hiρ hii
  have e1 : rec.1 = iop.1 := by rw [hie]; rfl
  have e2 : rec.2.2 = sCoord Γ iop := by rw [hie]; rfl
  exact ⟨ch, h1, by rw [e1]; exact h2, by rw [e2]; exact h4⟩

theorem s_fold_id_pos {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    (hOK : sSeqOK Γ ρ) {rec : SRec} (hrec : rec ∈ sFold Γ ρ) :
    1 ≤ rec.1 := by
  obtain ⟨iop, hiρ, hii, hie⟩ := s_fold_rec_sub Γ ρ rec hrec
  obtain ⟨-, -, -, h3, -⟩ := s_seq_chains hOK iop hiρ hii
  have e1 : rec.1 = iop.1 := by rw [hie]; rfl
  rw [e1]
  exact h3

/-- **The rooted fold is the unrooted fold plus the sentinel**, the
membership bridge. -/
theorem sr_fold_iff {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    (hOK : sSeqOK Γ ρ) :
    ∀ r : SRec, r ∈ sRFold Γ ρ ↔ r = rootRec ∨ r ∈ sFold Γ ρ := by
  induction ρ using List.reverseRecOn with
  | nil =>
      intro r
      show r ∈ [rootRec] ↔ _
      rw [show sFold Γ [] = [] from rfl]
      simp
  | append_singleton ρ o ih =>
      intro r
      have hOK' := sSeqOK_prefix hOK
      have IH := ih hOK'
      rw [sRFold_snoc, sFold_snoc]
      obtain ⟨ts, rr, op⟩ := o
      cases op with
      | ins el π a sd =>
          have happ := (hOK ρ (ts, rr, .ins el π a sd) [] (by simp)).2
          simp only [sApplicable] at happ
          have hat : a < ts := happ.1
          have hts1 : (1:ℕ) ≤ ts :=
            Nat.lt_of_le_of_lt (Nat.zero_le a) hat
          have hfreshU : ts ∉ sIds (sFold Γ ρ) :=
            s_fold_guard_free (sWf_of_seqOK hOK) (by simp [sIsIns])
          have hfreshR : ts ∉ sIds (sRFold Γ ρ) := by
            intro hmem
            obtain ⟨rec, hrec, hr1⟩ := List.mem_map.mp hmem
            rcases (IH rec).mp hrec with rfl | hrec'
            · have h0 : (0:ℕ) = ts := hr1
              rw [← h0] at hts1
              exact absurd hts1 (by decide)
            · exact hfreshU (List.mem_map.mpr ⟨rec, hrec', hr1⟩)
          show r ∈ sUpdate Γ (sRFold Γ ρ) (ts, rr, .ins el π a sd) ↔
            r = rootRec ∨ r ∈ sUpdate Γ (sFold Γ ρ) (ts, rr, .ins el π a sd)
          simp only [sUpdate]
          rw [if_neg hfreshR, if_neg hfreshU, mem_sInsert, mem_sInsert, IH r]
          tauto
      | del x =>
          have happ := (hOK ρ (ts, rr, .del x) [] (by simp)).2
          simp only [sApplicable] at happ
          have hx0 : x ≠ 0 := by
            intro h0
            obtain ⟨rec, hrec, hr1⟩ := List.mem_map.mp happ
            have h1 := s_fold_id_pos hOK' hrec
            rw [hr1, h0] at h1
            exact absurd h1 (by decide)
          show r ∈ sUpdate Γ (sRFold Γ ρ) (ts, rr, .del x) ↔
            r = rootRec ∨ r ∈ sUpdate Γ (sFold Γ ρ) (ts, rr, .del x)
          simp only [sUpdate]
          constructor
          · intro hr
            have hm := List.mem_of_mem_filter hr
            have hxne := List.of_mem_filter hr
            simp only [decide_eq_true_eq] at hxne
            rcases (IH r).mp hm with rfl | hm'
            · exact Or.inl rfl
            · exact Or.inr (List.mem_filter.mpr ⟨hm', by simpa using hxne⟩)
          · intro hr
            rcases hr with rfl | hr'
            · refine List.mem_filter.mpr
                ⟨(IH rootRec).mpr (Or.inl rfl), ?_⟩
              show decide (rootRec.1 ≠ x) = true
              simp only [rootRec, decide_eq_true_eq]
              exact fun h => hx0 h.symm
            · have hm := List.mem_of_mem_filter hr'
              have hxne := List.of_mem_filter hr'
              exact List.mem_filter.mpr ⟨(IH r).mpr (Or.inr hm), hxne⟩

/-- Chain package on the rooted fold: the sentinel carries the empty
chain. -/
theorem sr_fold_chain {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    (hOK : sSeqOK Γ ρ) {rec : SRec} (hrec : rec ∈ sRFold Γ ρ) :
    ∃ ch, PosSChain ch ∧ ((ch.map Prod.snd).sum = rec.1) ∧
      rec.2.2 = sidedCoordOf Γ ch := by
  rcases (sr_fold_iff hOK rec).mp hrec with rfl | h
  · exact ⟨[], by intro e he; simp at he, rfl, rfl⟩
  · exact s_fold_chain hOK h

/-- Rooted ids sit below a fresh op's stamp. -/
theorem sr_fold_id_lt {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    {o : Op SOp} (hOK : sSeqOK Γ (ρ ++ [o])) (hts1 : 1 ≤ o.1)
    {rec : SRec} (hrec : rec ∈ sRFold Γ ρ) : rec.1 < o.1 := by
  rcases (sr_fold_iff (sSeqOK_prefix hOK) rec).mp hrec with rfl | hrec'
  · show (0:ℕ) < o.1
    exact hts1
  · obtain ⟨iop, hiρ, hii, hie⟩ := s_fold_rec_sub Γ ρ rec hrec'
    have h1 := sInsIds_lt_of_seqOK hOK iop.1
      (mem_sInsIds.mpr ⟨iop, hiρ, hii, rfl⟩)
    have e1 : rec.1 = iop.1 := by rw [hie]; rfl
    rw [e1]
    exact h1

theorem sr_fold_sorted {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    (hOK : sSeqOK Γ ρ) : SSorted (sRFold Γ ρ) := by
  induction ρ using List.reverseRecOn with
  | nil => exact List.pairwise_singleton _ _
  | append_singleton ρ o ih =>
      have hOK' := sSeqOK_prefix hOK
      rw [sRFold_snoc]
      obtain ⟨ts, rr, op⟩ := o
      cases op with
      | del x => exact List.Pairwise.filter _ (ih hOK')
      | ins el π a sd =>
          apply sUpdate_sorted (ih hOK')
          intro x hx hkey
          obtain ⟨chx, hpx, hsx, hcx⟩ := sr_fold_chain hOK' hx
          obtain ⟨cho, hpo, hso, hts1, hco⟩ := s_seq_chains hOK
            (ts, rr, .ins el π a sd)
            (List.mem_append_right _ (by simp)) (by simp [sIsIns])
          have hxlt : x.1 < ts := sr_fold_id_lt hOK
            (show (1:ℕ) ≤ ts from hts1) hx
          rw [hcx, hco] at hkey
          have hch := sidedCoordOf_inj Γ hpx hpo (sKey_inj hkey)
          rw [hch, hso] at hsx
          have hsx' : ts = x.1 := hsx
          rw [hsx'] at hxlt
          exact absurd hxlt (Nat.lt_irrefl _)

theorem sr_fold_fst_inj {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    (hOK : sSeqOK Γ ρ) :
    ∀ r ∈ sRFold Γ ρ, ∀ r' ∈ sRFold Γ ρ, r.1 = r'.1 → r = r' := by
  intro r hr r' hr' hfst
  rcases (sr_fold_iff hOK r).mp hr with rfl | h
  · rcases (sr_fold_iff hOK r').mp hr' with rfl | h'
    · rfl
    · exfalso
      have := s_fold_id_pos hOK h'
      have h0 : (0:ℕ) = r'.1 := hfst
      omega
  · rcases (sr_fold_iff hOK r').mp hr' with rfl | h'
    · exfalso
      have := s_fold_id_pos hOK h
      have h0 : r.1 = (0:ℕ) := hfst
      omega
    · obtain ⟨o, ho, hi, hrec⟩ := s_fold_rec_sub Γ ρ r h
      obtain ⟨o', ho', hi', hrec'⟩ := s_fold_rec_sub Γ ρ r' h'
      have h1 : o.1 = o'.1 := by
        have e1 : r.1 = o.1 := by rw [hrec]; rfl
        have e2 : r'.1 = o'.1 := by rw [hrec']; rfl
        rw [← e1, ← e2, hfst]
      have : o = o' := by
        have hinj := List.inj_on_of_nodup_map
          (f := Prod.fst) (l := ρ.filter (fun o => sIsIns o))
          (sWf_of_seqOK hOK).ins_nodup
        exact hinj (List.mem_filter.mpr ⟨ho, hi⟩)
          (List.mem_filter.mpr ⟨ho', hi'⟩) h1
      rw [hrec, hrec', this]

/-! ## §F  The two sided adjacency lemmas (the heart) -/

/-- **R-adjacency**: appending a fresh R entry whose delta beats every
existing R-continuation of the anchor changes no display verdict against
the anchor, the newcomer sits immediately after it. -/
theorem schainBefore_snocR_iff {ca cr : SChain} {δ : ℕ}
    (hne : cr ≠ ca)
    (hmax : ∀ d rest, cr = ca ++ (Side.R, d) :: rest → d < δ) :
    schainBefore cr (ca ++ [(Side.R, δ)]) ↔ schainBefore cr ca := by
  constructor
  · intro h
    rcases schainBefore_inv h with ⟨d, rest, heq⟩ | ⟨d, rest, heq⟩ |
      ⟨q, e1, e2, t1, t2, hlt, hu, hv⟩
    · -- cr extends the newcomer on the L side: refuted by freshness
      exfalso
      have := hmax δ ((Side.L, d) :: rest) (by rw [heq]; simp)
      omega
    · -- ca ++ [(R,δ)] = cr ++ (R,d) :: rest
      rcases List.eq_nil_or_concat rest with rfl | ⟨rest', lst, rfl⟩
      · have hinj := List.append_inj' heq rfl
        exact absurd hinj.1.symm hne
      · simp only [List.concat_eq_append] at heq
        rw [show cr ++ (Side.R, d) :: (rest' ++ [lst])
            = (cr ++ (Side.R, d) :: rest') ++ [lst] from by simp] at heq
        obtain ⟨hca, -⟩ := List.append_inj' heq rfl
        rw [hca]
        exact schainBefore.extR cr d rest'
    · rcases List.eq_nil_or_concat t2 with rfl | ⟨t2', lst, rfl⟩
      · -- the divergence is at the snoc position
        have h2 : q ++ [e2] = ca ++ [(Side.R, δ)] := hv.symm
        obtain ⟨rfl, he⟩ := List.append_inj' h2 rfl
        injection he with he1
        subst he1
        obtain ⟨s1, d1⟩ := e1
        cases s1 with
        | R =>
            exfalso
            have hd := hmax d1 t1 hu
            have hδd : δ < d1 := hlt
            omega
        | L =>
            rw [hu]
            exact schainBefore.extL q d1 t1
      · simp only [List.concat_eq_append] at hv
        rw [show q ++ e2 :: (t2' ++ [lst]) = (q ++ e2 :: t2') ++ [lst]
            from by simp] at hv
        obtain ⟨hca, -⟩ := List.append_inj' hv rfl
        rw [hu, hca]
        exact schainBefore.diverge q e1 e2 t1 t2' hlt
  · intro h
    rcases schainBefore_inv h with ⟨d, rest, heq⟩ | ⟨d, rest, heq⟩ |
      ⟨q, e1, e2, t1, t2, hlt, hu, hv⟩
    · rw [heq, show ca ++ [(Side.R, δ)] = ca ++ (Side.R, δ) :: []
        from rfl]
      exact schainBefore.diverge ca (Side.L, d) (Side.R, δ) rest []
        trivial
    · rw [heq, List.append_assoc]
      exact schainBefore.extR cr d (rest ++ [(Side.R, δ)])
    · rw [hu, hv, List.append_assoc]
      exact schainBefore.diverge q e1 e2 t1 (t2 ++ [(Side.R, δ)]) hlt

/-- **L-adjacency**: appending a fresh L entry whose delta beats every
existing L-continuation of the anchor changes no display verdict against
the anchor, the newcomer sits immediately before it (the L band is
mirrored: the newest L-child hugs the node). -/
theorem schainBefore_snocL_iff {ca cr : SChain} {δ : ℕ}
    (hne : cr ≠ ca)
    (hmax : ∀ d rest, cr = ca ++ (Side.L, d) :: rest → d < δ) :
    schainBefore (ca ++ [(Side.L, δ)]) cr ↔ schainBefore ca cr := by
  constructor
  · intro h
    rcases schainBefore_inv h with ⟨d, rest, heq⟩ | ⟨d, rest, heq⟩ |
      ⟨q, e1, e2, t1, t2, hlt, hu, hv⟩
    · -- ca ++ [(L,δ)] = cr ++ (L,d) :: rest
      rcases List.eq_nil_or_concat rest with rfl | ⟨rest', lst, rfl⟩
      · have hinj := List.append_inj' heq rfl
        exact absurd hinj.1.symm hne
      · simp only [List.concat_eq_append] at heq
        rw [show cr ++ (Side.L, d) :: (rest' ++ [lst])
            = (cr ++ (Side.L, d) :: rest') ++ [lst] from by simp] at heq
        obtain ⟨hca, -⟩ := List.append_inj' heq rfl
        rw [hca]
        exact schainBefore.extL cr d rest'
    · -- cr extends the newcomer on the R side: refuted by freshness
      exfalso
      have := hmax δ ((Side.R, d) :: rest) (by rw [heq]; simp)
      omega
    · rcases List.eq_nil_or_concat t1 with rfl | ⟨t1', lst, rfl⟩
      · have h2 : q ++ [e1] = ca ++ [(Side.L, δ)] := hu.symm
        obtain ⟨rfl, he⟩ := List.append_inj' h2 rfl
        injection he with he1
        subst he1
        obtain ⟨s2, d2⟩ := e2
        cases s2 with
        | R =>
            rw [hv]
            exact schainBefore.extR q d2 t2
        | L =>
            exfalso
            have hd := hmax d2 t2 hv
            have hδd : δ < d2 := hlt
            omega
      · simp only [List.concat_eq_append] at hu
        rw [show q ++ e1 :: (t1' ++ [lst]) = (q ++ e1 :: t1') ++ [lst]
            from by simp] at hu
        obtain ⟨hca, -⟩ := List.append_inj' hu rfl
        rw [hv, hca]
        exact schainBefore.diverge q e1 e2 t1' t2 hlt
  · intro h
    rcases schainBefore_inv h with ⟨d, rest, heq⟩ | ⟨d, rest, heq⟩ |
      ⟨q, e1, e2, t1, t2, hlt, hu, hv⟩
    · rw [heq, List.append_assoc]
      exact schainBefore.extL cr d (rest ++ [(Side.L, δ)])
    · rw [heq, show ca ++ [(Side.L, δ)] = ca ++ (Side.L, δ) :: []
        from rfl]
      exact schainBefore.diverge ca (Side.L, δ) (Side.R, d) [] rest
        trivial
    · rw [hu, hv, List.append_assoc]
      exact schainBefore.diverge q e1 e2 (t1 ++ [(Side.L, δ)]) t2 hlt

#print axioms schainBefore_snocR_iff
#print axioms schainBefore_snocL_iff

/-! ## §G  Placement: sorted insert = splice at the anchor -/

theorem sInsert_all_lt {nr : SRec} : ∀ {s : SState},
    (∀ y ∈ s, keyLt (sKey y.2.2) (sKey nr.2.2) = true) →
    sInsert nr s = nr :: s
  | [], _ => rfl
  | x :: xs, h => by
      unfold sInsert
      rw [if_pos (h x List.mem_cons_self)]

/-- **R-placement**: when the newcomer's key sits exactly between the
anchor's and everything after it, the sorted insert IS the
splice-after-anchor, under projection. -/
theorem sInsert_map_insAfter {a : ℕ} {nr : SRec} :
    ∀ {s : SState} {ar : SRec}, SSorted s → ar ∈ s → ar.1 = a →
    (∀ r ∈ s, ∀ r' ∈ s, r.1 = r'.1 → r = r') →
    (∀ r ∈ s, sKey r.2.2 ≠ sKey nr.2.2) →
    (∀ r ∈ s, (keyLt (sKey nr.2.2) (sKey r.2.2) = true ↔
      (r = ar ∨ keyLt (sKey ar.2.2) (sKey r.2.2) = true))) →
    (sInsert nr s).map sProj = sInsAfter a (sProj nr) (s.map sProj) := by
  intro s
  induction s with
  | nil =>
      intro ar _ har
      exact absurd har (by simp)
  | cons x xs ih =>
      intro ar hsort har hara hinj hkeyne hiff
      by_cases hx : keyLt (sKey x.2.2) (sKey nr.2.2) = true
      · exfalso
        have hnx : ¬ (keyLt (sKey nr.2.2) (sKey x.2.2) = true) := by
          rw [keyLt_asymm hx]
          exact fun h => Bool.noConfusion h
        have hnor : ¬ (x = ar ∨ keyLt (sKey ar.2.2) (sKey x.2.2) = true) :=
          fun h => hnx ((hiff x List.mem_cons_self).mpr h)
        rcases List.mem_cons.mp har with heq | harx
        · exact hnor (Or.inl heq.symm)
        · exact hnor (Or.inr ((List.pairwise_cons.mp hsort).1 ar harx))
      · have hstep : sInsert nr (x :: xs) = x :: sInsert nr xs := by
          show (if keyLt (sKey x.2.2) (sKey nr.2.2) = true
            then nr :: x :: xs else x :: sInsert nr xs)
            = x :: sInsert nr xs
          rw [if_neg hx]
        rw [hstep]
        have hxk : keyLt (sKey nr.2.2) (sKey x.2.2) = true := by
          rcases keyLt_total (hkeyne x List.mem_cons_self) with h | h
          · exact absurd h hx
          · exact h
        rcases (hiff x List.mem_cons_self).mp hxk with heq | hax
        · have hall : ∀ y ∈ xs,
              keyLt (sKey y.2.2) (sKey nr.2.2) = true := by
            intro y hy
            have hyx := (List.pairwise_cons.mp hsort).1 y hy
            have hyne : y ≠ x := by
              rintro rfl
              rw [keyLt_irrefl] at hyx
              exact Bool.noConfusion hyx
            have hrfalse :
                ¬ (y = ar ∨ keyLt (sKey ar.2.2) (sKey y.2.2) = true) := by
              rintro (rfl | hcontra)
              · exact hyne heq.symm
              · rw [← heq, keyLt_asymm hyx] at hcontra
                exact Bool.noConfusion hcontra
            have hnn : ¬ (keyLt (sKey nr.2.2) (sKey y.2.2) = true) :=
              fun h => hrfalse ((hiff y (List.mem_cons_of_mem _ hy)).mp h)
            rcases keyLt_total
              (hkeyne y (List.mem_cons_of_mem _ hy)) with h | h
            · exact h
            · exact absurd h hnn
          rw [sInsert_all_lt hall, List.map_cons]
          show sProj x :: sProj nr :: xs.map sProj =
            if (sProj x).1 = a then sProj x :: sProj nr :: xs.map sProj
            else sProj x :: sInsAfter a (sProj nr) (xs.map sProj)
          rw [if_pos (show (sProj x).1 = a from by
            show x.1 = a
            rw [heq, hara])]
        · have hxa : x.1 ≠ a := by
            intro hcontra
            have hxar : x = ar :=
              hinj x List.mem_cons_self ar har (by rw [hcontra, hara])
            rw [hxar, keyLt_irrefl] at hax
            exact Bool.noConfusion hax
          have harx : ar ∈ xs := by
            rcases List.mem_cons.mp har with heq2 | h
            · exact absurd (show x.1 = a from by rw [← heq2]; exact hara)
                hxa
            · exact h
          rw [List.map_cons, List.map_cons]
          show sProj x :: (sInsert nr xs).map sProj =
            if (sProj x).1 = a then
              sProj x :: sProj nr :: xs.map sProj
            else sProj x :: sInsAfter a (sProj nr) (xs.map sProj)
          rw [if_neg (show ¬ (sProj x).1 = a from hxa)]
          rw [ih (List.pairwise_cons.mp hsort).2 harx hara
            (fun r hr r' hr' => hinj r (List.mem_cons_of_mem _ hr)
              r' (List.mem_cons_of_mem _ hr'))
            (fun r hr => hkeyne r (List.mem_cons_of_mem _ hr))
            (fun r hr => hiff r (List.mem_cons_of_mem _ hr))]

/-- **L-placement**: when everything displaying after the newcomer is
exactly the anchor and what follows it, the sorted insert IS the
splice-before-anchor, under projection. -/
theorem sInsert_map_insBefore {a : ℕ} {nr : SRec} :
    ∀ {s : SState} {ar : SRec}, SSorted s → ar ∈ s → ar.1 = a →
    (∀ r ∈ s, ∀ r' ∈ s, r.1 = r'.1 → r = r') →
    (∀ r ∈ s, (keyLt (sKey r.2.2) (sKey nr.2.2) = true ↔
      (r = ar ∨ keyLt (sKey r.2.2) (sKey ar.2.2) = true))) →
    (sInsert nr s).map sProj = sInsBefore a (sProj nr) (s.map sProj) := by
  intro s
  induction s with
  | nil =>
      intro ar _ har
      exact absurd har (by simp)
  | cons x xs ih =>
      intro ar hsort har hara hinj hiff
      by_cases hx : keyLt (sKey x.2.2) (sKey nr.2.2) = true
      · -- the head displays after the newcomer: it must be the anchor
        have hxar : x = ar := by
          rcases (hiff x List.mem_cons_self).mp hx with h | h
          · exact h
          · exfalso
            rcases List.mem_cons.mp har with heq | harx
            · rw [← heq, keyLt_irrefl] at h
              exact Bool.noConfusion h
            · have hhead := (List.pairwise_cons.mp hsort).1 ar harx
              rw [keyLt_asymm hhead] at h
              exact Bool.noConfusion h
        have hstep : sInsert nr (x :: xs) = nr :: x :: xs := by
          show (if keyLt (sKey x.2.2) (sKey nr.2.2) = true
            then nr :: x :: xs else x :: sInsert nr xs)
            = nr :: x :: xs
          rw [if_pos hx]
        rw [hstep]
        show sProj nr :: sProj x :: xs.map sProj =
          if (sProj x).1 = a then sProj nr :: sProj x :: xs.map sProj
          else sProj x :: sInsBefore a (sProj nr) (xs.map sProj)
        rw [if_pos (show (sProj x).1 = a from by
          show x.1 = a
          rw [hxar, hara])]
      · have hxne : x ≠ ar :=
          fun heq => hx ((hiff x List.mem_cons_self).mpr (Or.inl heq))
        have harx : ar ∈ xs := by
          rcases List.mem_cons.mp har with heq2 | h
          · exact absurd heq2.symm hxne
          · exact h
        have hxa : x.1 ≠ a := by
          intro hcontra
          exact hxne (hinj x List.mem_cons_self ar
            (List.mem_cons_of_mem _ harx) (by rw [hcontra, hara]))
        have hstep : sInsert nr (x :: xs) = x :: sInsert nr xs := by
          show (if keyLt (sKey x.2.2) (sKey nr.2.2) = true
            then nr :: x :: xs else x :: sInsert nr xs)
            = x :: sInsert nr xs
          rw [if_neg hx]
        rw [hstep, List.map_cons, List.map_cons]
        show sProj x :: (sInsert nr xs).map sProj =
          if (sProj x).1 = a then
            sProj nr :: sProj x :: xs.map sProj
          else sProj x :: sInsBefore a (sProj nr) (xs.map sProj)
        rw [if_neg (show ¬ (sProj x).1 = a from hxa)]
        rw [ih (List.pairwise_cons.mp hsort).2 harx hara
          (fun r hr r' hr' => hinj r (List.mem_cons_of_mem _ hr)
            r' (List.mem_cons_of_mem _ hr'))
          (fun r hr => hiff r (List.mem_cons_of_mem _ hr))]

/-! ## §H  Deletion commutes with projection -/

theorem map_sProj_filter (s : SState) (x : ℕ) :
    (s.filter (fun r => decide (r.1 ≠ x))).map sProj =
      (s.map sProj).filter (fun p => decide (p.1 ≠ x)) := by
  induction s with
  | nil => rfl
  | cons r rs ih =>
      simp only [ne_eq, decide_not] at ih
      by_cases h : r.1 = x
      · simp [h, sProj, ih]
      · simp [h, sProj, ih]

/-! ## §I  The capstone -/

/-- **The sided embedded-chain RGA, sequentially = the naive two-sided
buffer.** Under the datatype's own sequential discipline the rooted
canonical state IS the buffer program, record for record: an R insert
splices immediately after its anchor, an L insert immediately before it
(the two adjacency lemmas), a delete filters. -/
theorem sided_seq_sound {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    (hOK : sSeqOK Γ ρ) :
    (sRFold Γ ρ).map sProj = sSpecFold ρ := by
  induction ρ using List.reverseRecOn with
  | nil => rfl
  | append_singleton ρ o ih =>
      have hOK' := sSeqOK_prefix hOK
      have IH := ih hOK'
      rw [sRFold_snoc, sSpecFold_snoc]
      obtain ⟨ts, rr, op⟩ := o
      cases op with
      | del x =>
          show ((sRFold Γ ρ).filter (fun r => decide (r.1 ≠ x))).map sProj
            = _
          rw [map_sProj_filter, IH]
          rfl
      | ins el π a sd =>
          have happ := (hOK ρ (ts, rr, .ins el π a sd) [] (by simp)).2
          simp only [sApplicable] at happ
          obtain ⟨hat, hcase⟩ := happ
          have hat' : a < ts := hat
          have hts1 : (1:ℕ) ≤ ts :=
            Nat.lt_of_le_of_lt (Nat.zero_le a) hat'
          have hsort := sr_fold_sorted hOK'
          have hinj := sr_fold_fst_inj hOK'
          have hfresh : (ts, rr, SOp.ins el π a sd).1
              ∉ sIds (sRFold Γ ρ) := by
            intro hmem
            obtain ⟨rec, hrec, hr1⟩ := List.mem_map.mp hmem
            have h1 : rec.1 < ts := sr_fold_id_lt hOK hts1 hrec
            rw [hr1] at h1
            exact absurd h1 (Nat.lt_irrefl _)
          -- the anchor package: the sentinel serves the root anchor
          obtain ⟨ar, cha, harm, hara, har2, hpa, hsa⟩ :
              ∃ (ar : SRec) (cha : SChain), ar ∈ sRFold Γ ρ ∧ ar.1 = a ∧
                ar.2.2 = π ∧ PosSChain cha ∧
                ((cha.map Prod.snd).sum = a ∧
                  π = sidedCoordOf Γ cha) := by
            rcases hcase with ⟨rfl, rfl⟩ | ⟨el', hmem⟩
            · exact ⟨rootRec, [],
                (sr_fold_iff hOK' rootRec).mpr (Or.inl rfl),
                rfl, rfl, by intro e he; simp at he, rfl, rfl⟩
            · obtain ⟨ch, hp, hs, hc⟩ := s_fold_chain hOK' hmem
              exact ⟨(a, el', π), ch,
                (sr_fold_iff hOK' _).mpr (Or.inr hmem), rfl, rfl, hp,
                hs, hc⟩
          obtain ⟨hsa, hπeq⟩ := hsa
          have harc : ar.2.2 = sidedCoordOf Γ cha := by rw [har2, hπeq]
          have hδpos : 1 ≤ ts - a :=
            Nat.le_sub_of_add_le (Nat.add_comm 1 a ▸ hat')
          have hcoordnew : π ++ sBlock Γ (sd, ts - a)
              = sidedCoordOf Γ (cha ++ [(sd, ts - a)]) := by
            rw [sidedCoordOf_append, hπeq]
            simp [sidedCoordOf]
          have hpos_new : PosSChain (cha ++ [(sd, ts - a)]) := by
            intro e he
            rcases List.mem_append.mp he with h | h
            · exact hpa e h
            · simp at h
              rw [h]
              exact hδpos
          have hsum_new : ((cha ++ [(sd, ts - a)]).map Prod.snd).sum
              = ts := by
            rw [List.map_append, List.sum_append, hsa]
            simp
            exact Nat.add_sub_cancel' (Nat.le_of_lt hat')
          have hcane : cha ≠ cha ++ [(sd, ts - a)] := by
            intro hcontra
            have := congrArg List.length hcontra
            simp at this
          have hkeyne : ∀ rec ∈ sRFold Γ ρ, sKey rec.2.2 ≠
              sKey (((ts : ℕ), el, π ++ sBlock Γ (sd, ts - a))
                : SRec).2.2 := by
            intro rec hrec hcontra
            obtain ⟨chr, hpr, hsr, hcr⟩ := sr_fold_chain hOK' hrec
            have hrlt : rec.1 < ts := sr_fold_id_lt hOK hts1 hrec
            rw [hcr, show (((ts : ℕ), el, π ++ sBlock Γ (sd, ts - a))
                : SRec).2.2 = sidedCoordOf Γ (cha ++ [(sd, ts - a)])
                from hcoordnew] at hcontra
            have h1 := sidedCoordOf_inj Γ hpr hpos_new
              (sKey_inj hcontra)
            rw [h1, hsum_new] at hsr
            rw [hsr] at hrlt
            exact absurd hrlt (Nat.lt_irrefl _)
          show (sUpdate Γ (sRFold Γ ρ) (ts, rr, SOp.ins el π a sd)).map
            sProj = _
          simp only [sUpdate]
          rw [if_neg hfresh]
          -- per-record facts for the divergence analysis
          have hrecfacts : ∀ rec ∈ sRFold Γ ρ, rec ≠ ar →
              ∃ chr, PosSChain chr ∧ rec.2.2 = sidedCoordOf Γ chr ∧
                chr ≠ cha ∧ chr ≠ cha ++ [(sd, ts - a)] ∧
                (∀ sd' d rest, chr = cha ++ (sd', d) :: rest →
                  d < ts - a) := by
            intro rec hrec hreq
            obtain ⟨chr, hpr, hsr, hcr⟩ := sr_fold_chain hOK' hrec
            have hrlt : rec.1 < ts := sr_fold_id_lt hOK hts1 hrec
            have hra : rec.1 ≠ a := by
              intro hcontra
              exact hreq (hinj rec hrec ar harm (by rw [hcontra, hara]))
            refine ⟨chr, hpr, hcr, ?_, ?_, ?_⟩
            · intro hcontra
              apply hra
              rw [← hsr, hcontra, hsa]
            · intro hcontra
              rw [hcontra, hsum_new] at hsr
              rw [hsr] at hrlt
              exact absurd hrlt (Nat.lt_irrefl _)
            · intro sd' d rest hcontra
              have h2 := congrArg (fun l => (l.map Prod.snd).sum) hcontra
              simp only [List.map_append, List.sum_append, List.map_cons,
                List.sum_cons] at h2
              rw [hsa, hsr] at h2
              have h3 : a + d ≤ rec.1 := by
                rw [h2]
                omega
              have h4 : a + d < ts := Nat.lt_of_le_of_lt h3 hrlt
              exact Nat.lt_sub_of_add_lt (by rw [Nat.add_comm]; exact h4)
          cases sd with
          | R =>
              have hiff : ∀ rec ∈ sRFold Γ ρ,
                  (keyLt (sKey (((ts : ℕ), el,
                      π ++ sBlock Γ (Side.R, ts - a)) : SRec).2.2)
                    (sKey rec.2.2) = true ↔
                    (rec = ar ∨ keyLt (sKey ar.2.2)
                      (sKey rec.2.2) = true)) := by
                intro rec hrec
                by_cases hreq : rec = ar
                · subst hreq
                  constructor
                  · intro _
                    exact Or.inl rfl
                  · intro _
                    rw [show (((ts : ℕ), el,
                        π ++ sBlock Γ (Side.R, ts - a)) : SRec).2.2
                        = sidedCoordOf Γ (cha ++ [(Side.R, ts - a)])
                        from hcoordnew, harc]
                    exact (sdisplay_iff_schainBefore Γ hpa hpos_new
                      hcane).mpr (schainBefore.extR cha (ts - a) [])
                · obtain ⟨chr, hpr, hcr, hchne, hchne2, hmax⟩ :=
                    hrecfacts rec hrec hreq
                  rw [show (((ts : ℕ), el,
                      π ++ sBlock Γ (Side.R, ts - a)) : SRec).2.2
                      = sidedCoordOf Γ (cha ++ [(Side.R, ts - a)])
                      from hcoordnew, harc,
                    show rec.2.2 = sidedCoordOf Γ chr from hcr,
                    sdisplay_iff_schainBefore Γ hpr hpos_new hchne2,
                    or_iff_right hreq,
                    sdisplay_iff_schainBefore Γ hpr hpa hchne]
                  exact schainBefore_snocR_iff hchne
                    (fun d rest h => hmax Side.R d rest h)
              rw [sInsert_map_insAfter hsort harm hara hinj hkeyne hiff,
                IH]
              rfl
          | L =>
              have hiff : ∀ rec ∈ sRFold Γ ρ,
                  (keyLt (sKey rec.2.2)
                    (sKey (((ts : ℕ), el,
                      π ++ sBlock Γ (Side.L, ts - a)) : SRec).2.2)
                      = true ↔
                    (rec = ar ∨ keyLt (sKey rec.2.2)
                      (sKey ar.2.2) = true)) := by
                intro rec hrec
                by_cases hreq : rec = ar
                · subst hreq
                  constructor
                  · intro _
                    exact Or.inl rfl
                  · intro _
                    rw [show (((ts : ℕ), el,
                        π ++ sBlock Γ (Side.L, ts - a)) : SRec).2.2
                        = sidedCoordOf Γ (cha ++ [(Side.L, ts - a)])
                        from hcoordnew, harc]
                    exact (sdisplay_iff_schainBefore Γ hpos_new hpa
                      (Ne.symm hcane)).mpr
                      (schainBefore.extL cha (ts - a) [])
                · obtain ⟨chr, hpr, hcr, hchne, hchne2, hmax⟩ :=
                    hrecfacts rec hrec hreq
                  rw [show (((ts : ℕ), el,
                      π ++ sBlock Γ (Side.L, ts - a)) : SRec).2.2
                      = sidedCoordOf Γ (cha ++ [(Side.L, ts - a)])
                      from hcoordnew, harc,
                    show rec.2.2 = sidedCoordOf Γ chr from hcr,
                    sdisplay_iff_schainBefore Γ hpos_new hpr
                      (Ne.symm hchne2),
                    or_iff_right hreq,
                    sdisplay_iff_schainBefore Γ hpa hpr (Ne.symm hchne)]
                  exact schainBefore_snocL_iff hchne
                    (fun d rest h => hmax Side.L d rest h)
              rw [sInsert_map_insBefore hsort harm hara hinj hiff, IH]
              rfl

#print axioms sided_seq_sound

/-- The read corollary: dropping the sentinel on both sides, the
unrooted read IS the buffer program's read. -/
theorem sided_seq_read {Γ : OrderedPrefixCode} {ρ : List (Op SOp)}
    (hOK : sSeqOK Γ ρ) :
    (sFold Γ ρ).map sProj
      = (sSpecFold ρ).filter (fun p => decide (p.1 ≠ 0)) := by
  rw [← sided_seq_sound hOK, ← map_sProj_filter]
  congr 1
  apply ssorted_ext (s_fold_sorted Γ (sWf_of_seqOK hOK))
    (List.Pairwise.filter _ (sr_fold_sorted hOK))
  intro r
  rw [List.mem_filter]
  constructor
  · intro h
    refine ⟨(sr_fold_iff hOK r).mpr (Or.inr h), ?_⟩
    have h1 := s_fold_id_pos hOK h
    simp only [decide_eq_true_eq]
    intro h0
    rw [h0] at h1
    exact absurd h1 (by decide)
  · rintro ⟨hm, hne⟩
    rcases (sr_fold_iff hOK r).mp hm with rfl | h
    · simp [rootRec] at hne
    · exact h

#print axioms sided_seq_read

/-! ## §J  SPOTs (PASS+FAIL, hand-derived)

The L19 trace's buffer replay reproduces the datatype's own display, and
a genuinely sequential two-sided trace with a delete exercises both
splice directions plus the filter. -/

namespace SidedSeqSPOT

open SidedSPOT (cOf ch1 ch10 ch30 opsL19)

/-- PASS: the two-sided buffer program replays the L19 trace to exactly
the datatype's own display (sentinel first; elements = ids). The L19
trace is a MERGED two-replica history, not a sequential one, the buffer
program still reproduces the fold on it. -/
theorem l19_spec_replay :
    sSpecFold opsL19 = [(0, 0), (50, 50), (30, 30), (10, 10), (61, 61),
      (41, 41), (21, 21), (1, 1)] := by native_decide

/-- PASS: the rooted fold projects to the same buffer, on the same
trace. -/
theorem l19_fold_eq_spec :
    (sRFold unaryCode opsL19).map sProj = sSpecFold opsL19 := by
  native_decide

/-- FAIL pin: the interleaved order is NOT what the buffer program
produces. -/
theorem l19_spec_not_interleaved :
    sSpecFold opsL19 ≠ [(0, 0), (61, 61), (50, 50), (41, 41), (30, 30),
      (21, 21), (10, 10), (1, 1)] := by native_decide

/-- A genuinely sequential (monotone-stamp, applicable-at-every-fold)
two-sided trace: backward-type 10, 30, 50 to the left of 1,
forward-type 61, 70 to its right, then delete 30. -/
def ch61 : SChain := ch1 ++ [(Side.R, 60)]

def opsTwoSided : List (Op SOp) :=
  [ (1, 0, .ins 1 [] 0 Side.R)
  , (10, 0, .ins 10 (cOf ch1) 1 Side.L)
  , (30, 0, .ins 30 (cOf ch10) 10 Side.L)
  , (50, 0, .ins 50 (cOf ch30) 30 Side.L)
  , (61, 0, .ins 61 (cOf ch1) 1 Side.R)
  , (70, 0, .ins 70 (cOf ch61) 61 Side.R)
  , (80, 0, .del 30) ]

/-- PASS: fold = spec, hand-derived on both sides:
`[0, 50, 10, 1, 61, 70]`. -/
theorem two_sided_fold_eq_spec :
    (sRFold unaryCode opsTwoSided).map sProj = sSpecFold opsTwoSided := by
  native_decide

/-- PASS: the shared value, pinned. -/
theorem two_sided_display :
    sSpecFold opsTwoSided = [(0, 0), (50, 50), (10, 10), (1, 1),
      (61, 61), (70, 70)] := by native_decide

/-- FAIL pin: dropping the sentinel breaks the buffer equation shape. -/
theorem two_sided_not_unrooted :
    sSpecFold opsTwoSided ≠ [(50, 50), (10, 10), (1, 1),
      (61, 61), (70, 70)] := by native_decide

end SidedSeqSPOT

#print axioms SidedSeqSPOT.two_sided_fold_eq_spec

end Sal.ConditionedMRDTs
