import Sal.ConditionedMRDTs.MRDT_Instances.SidedRGA.SidedRGA_FugueMax /-! # The FugueMax variant alphabet as a conditioned MRDT instance `SidedRGA.lean`'s capstone `sided_embed_ra_linearizable3` covers plain sided coordinates (`sBlock`); the FugueMax realization (`SidedRGA_FugueMax.lean`) writes records over the VARIANT alphabet of `Sal/MRDTs/RGA_Embed/SidedMax_ChainLex.lean`, R entries carry an immutable right-origin tag (`fwTag`) before the delta code, which is a different block format, so RA-linearizability for the FM datatype needs a separate proof, which this file gives. The route is the sided instance's, verbatim in structure: the state is the same canonical sorted list (`SState`, strictly descending by `sKey`), so the whole §2/§2½ list algebra of `SidedRGA.lean` (`ssorted_ext`, `sInsert`, `sMerge2`, `sMergeL`) is REUSED; what changes is the op alphabet (`FOp` carries a coordinate prefix and one `FMEntry`) and the key-injectivity discharge, which runs through the variant's unique decodability `fmCoordOf_inj`, this is where the FM format differs materially: the variant needs `TagsOK` (wellformed right-origin tags) alongside chain positivity, so the honesty contract `FMHonest` carries both. Convergence is otherwise insensitive to what the coordinates contain, exactly as expected: coordinates are injectively minted, immutable, and consumed only through `sKey` comparisons. Sections: §1 the datatype (`FMSig`) · §3 well-formed enumerations and fold-canonicity (`f_fold_canon`, the FM analogue of `s_fold_canon`) · §5 honest histories (`FMHonestCore`) · §6 the Join (`f_join_at`: the merge is its own linearization witness) · §7 the capstone `fuguemax_ra_linearizable3` · §7½ the bridge to the generation layer (`mFold_eq_fFold`: the display fold of `SidedRGA_FugueMax.lean` IS this signature's fold of the mapped enumeration, so fold-canonicity covers `mFold`-generated states) · §8 SPOTs (PASS+FAIL, hand-derived). -/ namespace Sal.ConditionedMRDTs open Sal.Emulation open Sal.EmbedRGA (OrderedPrefixCode keyLt sKey unaryCode keyLt_irrefl keyLt_asymm keyLt_trans keyLt_total FMEntry FMChain fmδ PosFMChain TagOK fmTagOK TagsOK fmBlock fmCoordOf fmCoordOf_append fmCoordOf_inj) set_option linter.unusedSectionVars false set_option linter.unusedVariables false /-! ## §1 The datatype -/ /-- FM ops: an insert names an element, a coordinate prefix (the parent chain's coordinate), and ONE FugueMax entry (`.R tag δ` or `.L δ`); a delete names an id. The tag is payload to the datatype: it is minted by the generation policy (`mGenInsAfter`) and stored blindly. -/ inductive FOp : Type where | ins (e : ℕ) (π : List ℕ) (ent : FMEntry) | del (x : ℕ) deriving DecidableEq /-- The coordinate an insert writes, a function of the op alone: the carried prefix + the entry's variant block (`fmBlock` composes the reversed right-origin tag and the complemented delta code on R, the sided L band on L). -/ def fCoord (Γ : OrderedPrefixCode) (o : Op FOp) : List ℕ := match o.2.2 with | .ins _ π ent => π ++ fmBlock Γ ent | .del _ => [] /-- Insert places the record at its sorted position (idempotent on a present id); delete removes the record wherever it sits. Same shape as the sided `sUpdate`, over the variant block. -/ def fUpdate (Γ : OrderedPrefixCode) (s : SState) (o : Op FOp) : SState := match o.2.2 with | .ins e π ent => if o.1 ∈ sIds s then s else sInsert (o.1, e, π ++ fmBlock Γ ent) s | .del x => s.filter (fun r => decide (r.1 ≠ x)) /-- The FugueMax embedded-chain RGA, parametric in the delta code. State, merge, query, and `rc` are the sided instance's verbatim (the state IS the same canonical sorted list); only the op alphabet and the block format differ. -/ def FMSig (Γ : OrderedPrefixCode) : ConditionedMRDTSig where State := SState dec_state := inferInstance init := [] AppOp := FOp dec_op := inferInstance Query := Unit Value := List ℕ update := fUpdate Γ merge := fun a b => sMergeL [] a b query := fun s _ => s.map (fun r => r.2.1) rc := fun _ _ => RcRes.Either mergeL := sMergeL merge_init_slice := fun _ _ => rfl Inv := fun _ => True applicable := fun _ _ => True theorem FMSig_core_update (Γ : OrderedPrefixCode) (s : SState) (o : Op FOp) : (FMSig Γ).toCRDTSig.update s o = fUpdate Γ s o := rfl theorem FMSig_rc_either (Γ : OrderedPrefixCode) (o₁ o₂ : Op FOp) : (FMSig Γ).toCRDTSig.rc o₁ o₂ = RcRes.Either := rfl /-! ## §3 Well-formed enumerations and fold-canonicity `f_fold_canon`: any two well-formed enumerations of one event set fold to the SAME state, the FM analogue of `s_fold_canon`, by `ssorted_ext` + the fold membership characterization. The tag rides along inertly: it is consumed by `fCoord` at record-creation time and never consulted again, which is why every proof below is the sided proof with `fCoord` substituted. -/ def fFold (Γ : OrderedPrefixCode) (ρ : List (Op FOp)) : SState := applySeq (FMSig Γ).toCRDTSig (FMSig Γ).init ρ theorem fFold_snoc (Γ : OrderedPrefixCode) (ρ : List (Op FOp)) (e : Op FOp) : fFold Γ (ρ ++ [e]) = fUpdate Γ (fFold Γ ρ) e := by unfold fFold applySeq rw [List.foldl_append] rfl def fIsIns (o : Op FOp) : Bool := match o.2.2 with | .ins _ _ _ => true | .del _ => false /-- The record an insert writes. -/ def fRecOf (Γ : OrderedPrefixCode) (o : Op FOp) : SRec := (o.1, (match o.2.2 with | .ins e _ _ => e | .del _ => 0), fCoord Γ o) def fInsIds (ρ : List (Op FOp)) : List ℕ := (ρ.filter (fun o => fIsIns o)).map Prod.fst def fDels (ρ : List (Op FOp)) : List ℕ := ρ.filterMap (fun o => match o.2.2 with | .del x => some x | .ins _ _ _ => none) theorem mem_fInsIds {ρ : List (Op FOp)} {t : ℕ} : t ∈ fInsIds ρ ↔ ∃ o ∈ ρ, fIsIns o = true ∧ o.1 = t := by simp only [fInsIds, List.mem_map, List.mem_filter] constructor · rintro ⟨o, ⟨hm, hi⟩, rfl⟩ exact ⟨o, hm, hi, rfl⟩ · rintro ⟨o, hm, hi, rfl⟩ exact ⟨o, ⟨hm, hi⟩, rfl⟩ theorem mem_fDels {ρ : List (Op FOp)} {x : ℕ} : x ∈ fDels ρ ↔ ∃ o ∈ ρ, o.2.2 = FOp.del x := by simp only [fDels, List.mem_filterMap] constructor · rintro ⟨o, hm, hsome⟩ refine ⟨o, hm, ?_⟩ cases hop : o.2.2 with | ins e π ent => rw [hop] at hsome; simp at hsome | del y => rw [hop] at hsome; simp at hsome; rw [hsome] · rintro ⟨o, hm, hdel⟩ exact ⟨o, hm, by rw [hdel]⟩ theorem fInsIds_append (ρ σ : List (Op FOp)) : fInsIds (ρ ++ σ) = fInsIds ρ ++ fInsIds σ := by simp [fInsIds, List.filter_append] theorem fDels_append (ρ σ : List (Op FOp)) : fDels (ρ ++ σ) = fDels ρ ++ fDels σ := by simp [fDels, List.filterMap_append] /-- Well-formed enumerations: insert ids are unique, nothing is deleted before its insert, and distinct inserts mint distinct keys (supplied on honest histories by FM chain-generation + variant unique decodability, `fmCoordOf_inj`). -/ structure FWf (Γ : OrderedPrefixCode) (ρ : List (Op FOp)) : Prop where ins_nodup : (fInsIds ρ).Nodup del_late : ∀ σ o τ, ρ = σ ++ o :: τ → fIsIns o = true → o.1 ∉ fDels σ keys_inj : ∀ o₁ ∈ ρ, ∀ o₂ ∈ ρ, fIsIns o₁ = true → fIsIns o₂ = true → o₁.1 ≠ o₂.1 → sKey (fCoord Γ o₁) ≠ sKey (fCoord Γ o₂) theorem FWf.prefix {Γ : OrderedPrefixCode} {ρ : List (Op FOp)} {e : Op FOp} (h : FWf Γ (ρ ++ [e])) : FWf Γ ρ where ins_nodup := by have := h.ins_nodup rw [fInsIds_append] at this exact this.of_append_left del_late := fun σ o τ heq hins => by refine h.del_late σ o (τ ++ [e]) ?_ hins rw [heq] simp keys_inj := fun o₁ h₁ o₂ h₂ => h.keys_inj o₁ (List.mem_append_left _ h₁) o₂ (List.mem_append_left _ h₂) /-- Record provenance, unconditioned: everything in a fold was written by some insert of the enumeration. -/ theorem f_fold_rec_sub (Γ : OrderedPrefixCode) : ∀ (ρ : List (Op FOp)) (r : SRec), r ∈ fFold Γ ρ → ∃ o ∈ ρ, fIsIns o = true ∧ r = fRecOf Γ o := by intro ρ induction ρ using List.reverseRecOn with | nil => intro r hr exact absurd hr (by simp [fFold, applySeq, FMSig]) | append_singleton ρ e ih => intro r hr rw [fFold_snoc] at hr obtain ⟨ts, rr, op⟩ := e cases op with | ins el π ent => simp only [fUpdate] at hr by_cases hmem : ts ∈ sIds (fFold Γ ρ) · rw [if_pos hmem] at hr obtain ⟨o, hm, hi, hrec⟩ := ih r hr exact ⟨o, List.mem_append_left _ hm, hi, hrec⟩ · rw [if_neg hmem] at hr rcases mem_sInsert.mp hr with hr' | rfl · obtain ⟨o, hm, hi, hrec⟩ := ih r hr' exact ⟨o, List.mem_append_left _ hm, hi, hrec⟩ · exact ⟨(ts, rr, .ins el π ent), List.mem_append_right _ (by simp), by simp [fIsIns], by simp [fRecOf, fCoord]⟩ | del x => simp only [fUpdate] at hr obtain ⟨o, hm, hi, hrec⟩ := ih r (List.mem_of_mem_filter hr) exact ⟨o, List.mem_append_left _ hm, hi, hrec⟩ /-- Under well-formedness the insert guard never fires: a fresh insert's id is not in the fold of its past. -/ theorem f_fold_guard_free {Γ : OrderedPrefixCode} {ρ : List (Op FOp)} {e : Op FOp} (hwf : FWf Γ (ρ ++ [e])) (hins : fIsIns e = true) : e.1 ∉ sIds (fFold Γ ρ) := by intro hmem obtain ⟨r, hr, hr1⟩ := List.mem_map.mp hmem obtain ⟨o, hm, hi, hrec⟩ := f_fold_rec_sub Γ ρ r hr have ho1 : o.1 = e.1 := by rw [hrec] at hr1; exact hr1 have h1 : e.1 ∈ fInsIds ρ := mem_fInsIds.mpr ⟨o, hm, hi, ho1⟩ have := hwf.ins_nodup rw [fInsIds_append] at this rcases List.nodup_append.mp this with ⟨-, -, hdisj⟩ have h2 : e.1 ∈ fInsIds [e] := by simp [fInsIds, hins] exact (hdisj e.1 h1 e.1 h2) rfl /-- Folds of well-formed enumerations are canonical (sorted). -/ theorem f_fold_sorted (Γ : OrderedPrefixCode) : ∀ {ρ : List (Op FOp)}, FWf Γ ρ → SSorted (fFold Γ ρ) := by intro ρ induction ρ using List.reverseRecOn with | nil => intro _ rw [show fFold Γ [] = [] from rfl] exact List.Pairwise.nil | append_singleton ρ e ih => intro hwf have hsorted := ih hwf.prefix rw [fFold_snoc] obtain ⟨ts, rr, op⟩ := e cases op with | del x => exact List.Pairwise.filter _ hsorted | ins el π ent => simp only [fUpdate] by_cases hmem : ts ∈ sIds (fFold Γ ρ) · rw [if_pos hmem]; exact hsorted · rw [if_neg hmem] apply sInsert_sorted hsorted intro x hx obtain ⟨o, hm, hi, hrec⟩ := f_fold_rec_sub Γ ρ x hx have hx1 : x.1 = o.1 := by rw [hrec]; rfl have hne : o.1 ≠ ts := by intro heq exact hmem (List.mem_map.mpr ⟨x, hx, by rw [hx1, heq]⟩) have hkey := hwf.keys_inj o (List.mem_append_left _ hm) (ts, rr, .ins el π ent) (List.mem_append_right _ (by simp)) hi (by simp [fIsIns]) hne rw [hrec] show sKey (fCoord Γ o) ≠ sKey (π ++ fmBlock Γ ent) simpa [fCoord] using hkey /-- **The fold membership characterization**: under well-formedness a record is in the fold iff its insert is in the enumeration and its id is never deleted, an ORDER-FREE description. -/ theorem f_fold_mem (Γ : OrderedPrefixCode) : ∀ {ρ : List (Op FOp)}, FWf Γ ρ → ∀ (r : SRec), (r ∈ fFold Γ ρ ↔ (∃ o ∈ ρ, fIsIns o = true ∧ r = fRecOf Γ o) ∧ r.1 ∉ fDels ρ) := by intro ρ induction ρ using List.reverseRecOn with | nil => intro _ r simp [show fFold Γ [] = [] from rfl] | append_singleton ρ e ih => intro hwf r have IH := ih hwf.prefix rw [fFold_snoc] obtain ⟨ts, rr, op⟩ := e cases op with | ins el π ent => simp only [fUpdate] rw [if_neg (f_fold_guard_free hwf (by simp [fIsIns]))] have hdels : fDels (ρ ++ [(ts, rr, FOp.ins el π ent)]) = fDels ρ := by rw [fDels_append] simp [fDels] rw [hdels, mem_sInsert] constructor · rintro (hr | rfl) · obtain ⟨⟨o, hm, hi, hrec⟩, hnd⟩ := (IH r).mp hr exact ⟨⟨o, List.mem_append_left _ hm, hi, hrec⟩, hnd⟩ · refine ⟨⟨(ts, rr, .ins el π ent), List.mem_append_right _ (by simp), by simp [fIsIns], by simp [fRecOf, fCoord]⟩, ?_⟩ show ts ∉ fDels ρ exact hwf.del_late ρ (ts, rr, .ins el π ent) [] rfl (by simp [fIsIns]) · rintro ⟨⟨o, hm, hi, hrec⟩, hnd⟩ rcases List.mem_append.mp hm with hm' | hm' · exact Or.inl ((IH r).mpr ⟨⟨o, hm', hi, hrec⟩, hnd⟩) · right have : o = (ts, rr, .ins el π ent) := List.mem_singleton.mp hm' rw [hrec, this] simp [fRecOf, fCoord] | del x => simp only [fUpdate] have hdels : fDels (ρ ++ [(ts, rr, FOp.del x)]) = fDels ρ ++ [x] := by rw [fDels_append] simp [fDels] rw [hdels] constructor · intro hr have hm := List.mem_of_mem_filter hr have hx := List.of_mem_filter hr simp only [decide_eq_true_eq] at hx obtain ⟨⟨o, hmo, hi, hrec⟩, hnd⟩ := (IH r).mp hm refine ⟨⟨o, List.mem_append_left _ hmo, hi, hrec⟩, ?_⟩ simp only [List.mem_append, List.mem_singleton] rintro (h | h) · exact hnd h · exact hx h · rintro ⟨⟨o, hm, hi, hrec⟩, hnd⟩ simp only [List.mem_append, List.mem_singleton] at hnd push_neg at hnd have hm' : o ∈ ρ := by rcases List.mem_append.mp hm with h | h · exact h · have : o = (ts, rr, .del x) := List.mem_singleton.mp h rw [this] at hi simp [fIsIns] at hi refine List.mem_filter.mpr ⟨(IH r).mpr ⟨⟨o, hm', hi, hrec⟩, hnd.1⟩, by simpa using hnd.2⟩ /-- **Fold-canonicity**, FM variant: well-formed enumerations of one event set fold to the SAME state. The state is a function of the event set, the property the queue-route Join hook cannot live without, and the reason the right-origin tag can be policy-minted: the datatype's canonical state never depends on enumeration order, whatever tags the ops carry. -/ theorem f_fold_canon (Γ : OrderedPrefixCode) {ρ ρ' : List (Op FOp)} (hwf : FWf Γ ρ) (hwf' : FWf Γ ρ') (hmem : ∀ o, o ∈ ρ ↔ o ∈ ρ') : fFold Γ ρ = fFold Γ ρ' := by apply ssorted_ext (f_fold_sorted Γ hwf) (f_fold_sorted Γ hwf') intro r rw [f_fold_mem Γ hwf r, f_fold_mem Γ hwf' r] constructor · rintro ⟨⟨o, hm, hi, hrec⟩, hnd⟩ refine ⟨⟨o, (hmem o).mp hm, hi, hrec⟩, fun hx => hnd ?_⟩ obtain ⟨o', hm', hdel⟩ := mem_fDels.mp hx exact mem_fDels.mpr ⟨o', (hmem o').mpr hm', hdel⟩ · rintro ⟨⟨o, hm, hi, hrec⟩, hnd⟩ refine ⟨⟨o, (hmem o).mpr hm, hi, hrec⟩, fun hx => hnd ?_⟩ obtain ⟨o', hm', hdel⟩ := mem_fDels.mp hx exact mem_fDels.mpr ⟨o', (hmem o').mp hm', hdel⟩ /-! ## §5 Honest histories, well-formedness of enumerations `FMHonestCore` is the FM analogue of the sided instance's honesty: every delete names an id its issuer had observed (a `vis`-prior insert), and inserts are chain-generated over the VARIANT alphabet, the mint is a positive, TAG-WELLFORMED FugueMax birth chain's coordinate whose deltas telescope to the id. `TagsOK` is the one clause the sided contract did not need: the variant's unique decodability (`fmCoordOf_inj`) consumes it, because tag decoding (`fwTag_cancel`) is only unambiguous on wellformed tags. The FugueMax generation layer supplies it for free (`SidedRGA_FugueMax.lean`'s `KInv.wf`). -/ /-- The one non-commuting shape: an insert and the delete of its id. Witnessed at the empty state. -/ theorem f_ins_del_not_comm (Γ : OrderedPrefixCode) (ts r el : ℕ) (π : List ℕ) (ent : FMEntry) (ts' r' : ℕ) : ¬ (FMSig Γ).toCRDTSig.commutes (ts, r, FOp.ins el π ent) (ts', r', FOp.del ts) := by intro h have h0 := h [] rw [FMSig_core_update, FMSig_core_update, FMSig_core_update, FMSig_core_update] at h0 simp only [fUpdate, sIds, sInsert, List.map_nil, List.not_mem_nil, if_false, List.filter_nil] at h0 simp at h0 /-- Honest histories. -/ structure FMHonestCore (Γ : OrderedPrefixCode) (C : Sal.Emulation.Configuration (FMSig Γ).toCRDTSig) : Prop where /-- Every delete's target was inserted `vis`-before it. -/ del_has_ins : ∀ e ∈ C.events, ∀ x : ℕ, e.2.2 = FOp.del x → ∃ a ∈ C.events, C.vis a e ∧ a.1 = x ∧ fIsIns a = true /-- Inserts are chain-generated: each mint is the coordinate of a positive tag-wellformed FugueMax birth chain whose deltas telescope to the id (so chains are injective on ids for free). -/ chain_gen : ∃ chainOf : ℕ → FMChain, ∀ o ∈ C.events, fIsIns o = true → PosFMChain (chainOf o.1) ∧ TagsOK (chainOf o.1) ∧ fCoord Γ o = fmCoordOf Γ (chainOf o.1) ∧ ((chainOf o.1).map fmδ).sum = o.1 /-- Honesty + backward closure: a delete's insert lies in the same closed event set, `vis`-before it. -/ theorem f_del_ins_mem {Γ : OrderedPrefixCode} {C : Sal.Emulation.Configuration (FMSig Γ).toCRDTSig} (hHon : FMHonestCore Γ C) {ev : Set (Op FOp)} (hin : ∀ a ∈ ev, a ∈ C.events) (hcl : ∀ a b, C.vis a b → ¬ (FMSig Γ).toCRDTSig.commutes a b → b ∈ ev → a ∈ ev) : ∀ d ∈ ev, ∀ x : ℕ, d.2.2 = FOp.del x → ∃ a ∈ ev, fIsIns a = true ∧ a.1 = x ∧ C.vis a d := by intro d hd x hdel obtain ⟨a, haev, hvis, hax, hains⟩ := hHon.del_has_ins d (hin d hd) x hdel have hncomm : ¬ (FMSig Γ).toCRDTSig.commutes a d := by obtain ⟨a1, a2, aop⟩ := a obtain ⟨d1, d2, dop⟩ := d simp only at hdel hax subst hdel cases aop with | del y => simp [fIsIns] at hains | ins el π ent => subst hax exact f_ins_del_not_comm Γ a1 a2 el π ent d1 d2 exact ⟨a, hcl a d hvis hncomm hd, hains, hax, hvis⟩ /-- **A `loOn`-respecting enumeration of a closed honest set is well-formed**, the bridge from the configuration layer to `FWf`, one honesty ingredient per field: timestamp uniqueness gives `ins_nodup`, delete-after-insert visibility gives `del_late`, chain generation + variant unique decodability give `keys_inj`. -/ theorem f_wf_of_enum {Γ : OrderedPrefixCode} {C : Sal.Emulation.Configuration (FMSig Γ).toCRDTSig} (hHon : FMHonestCore Γ C) {ev : Set (Op FOp)} {ρ : List (Op FOp)} (hin : ∀ a ∈ ev, a ∈ C.events) (hcl : ∀ a b, C.vis a b → ¬ (FMSig Γ).toCRDTSig.commutes a b → b ∈ ev → a ∈ ev) (hperm : listPermOf ρ ev) (hresp : respects ρ (loOn C ev)) : FWf Γ ρ where ins_nodup := by apply List.Nodup.map_on ?_ (hperm.1.filter _) intro o₁ h₁ o₂ h₂ hfst exact C.ts_unique (hin _ ((hperm.2 _).mp (List.mem_of_mem_filter h₁))) (hin _ ((hperm.2 _).mp (List.mem_of_mem_filter h₂))) hfst del_late := by intro σ o τ heq hins hdel obtain ⟨d, hdσ, hddel⟩ := mem_fDels.mp hdel have hdρ : d ∈ ρ := by rw [heq]; exact List.mem_append_left _ hdσ have hoρ : o ∈ ρ := by rw [heq]; exact List.mem_append_right _ List.mem_cons_self obtain ⟨a, haev, hains, hax, hvis⟩ := f_del_ins_mem hHon hin hcl d ((hperm.2 d).mp hdρ) o.1 hddel have hao : a = o := C.ts_unique (hin a haev) (hin o ((hperm.2 o).mp hoρ)) hax subst hao unfold respects at hresp rw [heq] at hresp have hcross := (List.pairwise_append.mp hresp).2.2 d hdσ a List.mem_cons_self apply hcross rw [loOn_iff_of_rc_either (FMSig_rc_either Γ)] refine ⟨hvis, ?_⟩ obtain ⟨a1, a2, aop⟩ := a obtain ⟨d1, d2, dop⟩ := d simp only at hddel subst hddel cases aop with | del y => simp [fIsIns] at hins | ins el π ent => exact f_ins_del_not_comm Γ a1 a2 el π ent d1 d2 keys_inj := by obtain ⟨chainOf, hch⟩ := hHon.chain_gen intro o₁ h₁ o₂ h₂ hi₁ hi₂ hne hkey obtain ⟨hp₁, ht₁, hc₁, hs₁⟩ := hch o₁ (hin _ ((hperm.2 _).mp h₁)) hi₁ obtain ⟨hp₂, ht₂, hc₂, hs₂⟩ := hch o₂ (hin _ ((hperm.2 _).mp h₂)) hi₂ apply hne have hc : fmCoordOf Γ (chainOf o₁.1) = fmCoordOf Γ (chainOf o₂.1) := by rw [← hc₁, ← hc₂] exact sKey_inj hkey have hchain := fmCoordOf_inj Γ hp₁ hp₂ ht₁ ht₂ hc calc o₁.1 = ((chainOf o₁.1).map fmδ).sum := hs₁.symm _ = ((chainOf o₂.1).map fmδ).sum := by rw [hchain] _ = o₂.1 := hs₂ /-! ## §6a The survival algebra The record-level membership of the ternary merge, characterized order-free against the union event set, the mathematical core of the Join. §6b turns it into `JoinLemma3At` by exhibiting the witness enumeration. All verbatim sided proofs: the merge never looks inside a coordinate. -/ theorem f_fold_id_mem (Γ : OrderedPrefixCode) {ρ : List (Op FOp)} (hwf : FWf Γ ρ) (t : ℕ) : t ∈ sIds (fFold Γ ρ) ↔ (∃ o ∈ ρ, fIsIns o = true ∧ o.1 = t) ∧ t ∉ fDels ρ := by constructor · intro h obtain ⟨r, hr, rfl⟩ := List.mem_map.mp h obtain ⟨⟨o, hm, hi, hrec⟩, hnd⟩ := (f_fold_mem Γ hwf r).mp hr exact ⟨⟨o, hm, hi, by rw [hrec]; rfl⟩, hnd⟩ · rintro ⟨⟨o, hm, hi, rfl⟩, hnd⟩ have hr : fRecOf Γ o ∈ fFold Γ ρ := (f_fold_mem Γ hwf _).mpr ⟨⟨o, hm, hi, rfl⟩, hnd⟩ exact List.mem_map.mpr ⟨fRecOf Γ o, hr, rfl⟩ /-- Distinct honest inserts mint distinct keys (the standalone form of `f_wf_of_enum`'s third discharge, for use at the merge site). -/ theorem f_keys_inj_events {Γ : OrderedPrefixCode} {C : Sal.Emulation.Configuration (FMSig Γ).toCRDTSig} (hHon : FMHonestCore Γ C) : ∀ o₁ ∈ C.events, ∀ o₂ ∈ C.events, fIsIns o₁ = true → fIsIns o₂ = true → o₁.1 ≠ o₂.1 → sKey (fCoord Γ o₁) ≠ sKey (fCoord Γ o₂) := by obtain ⟨chainOf, hch⟩ := hHon.chain_gen intro o₁ h₁ o₂ h₂ hi₁ hi₂ hne hkey obtain ⟨hp₁, ht₁, hc₁, hs₁⟩ := hch o₁ h₁ hi₁ obtain ⟨hp₂, ht₂, hc₂, hs₂⟩ := hch o₂ h₂ hi₂ apply hne have hc : fmCoordOf Γ (chainOf o₁.1) = fmCoordOf Γ (chainOf o₂.1) := by rw [← hc₁, ← hc₂] exact sKey_inj hkey have hchain := fmCoordOf_inj Γ hp₁ hp₂ ht₁ ht₂ hc calc o₁.1 = ((chainOf o₁.1).map fmδ).sum := hs₁.symm _ = ((chainOf o₂.1).map fmδ).sum := by rw [hchain] _ = o₂.1 := hs₂ /-- **The merge membership characterization.** At a join site (three canonical enumerations over an honest configuration), a record is in the ternary merge iff its insert is somewhere in the union and its id is deleted nowhere in the union, the union's order-free membership. OR-set survival, with honesty closing the one subtle corner (a branch-2 delete of a branch-1 survivor forces the insert into the LCA). -/ theorem f_mergeL_mem {Γ : OrderedPrefixCode} {C : Sal.Emulation.Configuration (FMSig Γ).toCRDTSig} (hHon : FMHonestCore Γ C) {ev₁ ev₂ : Set (Op FOp)} {ρ₀ ρ₁ ρ₂ : List (Op FOp)} (hin₁ : ∀ a ∈ ev₁, a ∈ C.events) (hin₂ : ∀ a ∈ ev₂, a ∈ C.events) (hcl₁ : ∀ a b, C.vis a b → ¬ (FMSig Γ).toCRDTSig.commutes a b → b ∈ ev₁ → a ∈ ev₁) (hcl₂ : ∀ a b, C.vis a b → ¬ (FMSig Γ).toCRDTSig.commutes a b → b ∈ ev₂ → a ∈ ev₂) (hp₀ : listPermOf ρ₀ (ev₁ ∩ ev₂)) (hp₁ : listPermOf ρ₁ ev₁) (hp₂ : listPermOf ρ₂ ev₂) (hwf₀ : FWf Γ ρ₀) (hwf₁ : FWf Γ ρ₁) (hwf₂ : FWf Γ ρ₂) (r : SRec) : r ∈ sMergeL (fFold Γ ρ₀) (fFold Γ ρ₁) (fFold Γ ρ₂) ↔ (∃ o, (o ∈ ev₁ ∨ o ∈ ev₂) ∧ fIsIns o = true ∧ r = fRecOf Γ o) ∧ (∀ d, (d ∈ ev₁ ∨ d ∈ ev₂) → d.2.2 ≠ FOp.del r.1) := by classical set s₀ := fFold Γ ρ₀ set s₁ := fFold Γ ρ₁ set s₂ := fFold Γ ρ₂ have hdels : ∀ {ρ : List (Op FOp)} {ev : Set (Op FOp)}, listPermOf ρ ev → ∀ {t : ℕ}, t ∈ fDels ρ ↔ ∃ d ∈ ev, d.2.2 = FOp.del t := by intro ρ ev hp t rw [mem_fDels] constructor · rintro ⟨d, hm, hdel⟩ exact ⟨d, (hp.2 d).mp hm, hdel⟩ · rintro ⟨d, hm, hdel⟩ exact ⟨d, (hp.2 d).mpr hm, hdel⟩ rw [show sMergeL s₀ s₁ s₂ = sMerge2 (s₁.filter (fun x => decide (x.1 ∈ sIds s₂ ∨ x.1 ∉ sIds s₀))) (s₂.filter (fun x => decide (x.1 ∉ sIds s₀ ∧ x.1 ∉ sIds s₁))) from rfl, mem_sMerge2] constructor · rintro (hr | hr) · -- branch-1 survivor have hm := List.mem_of_mem_filter hr have hcond := List.of_mem_filter hr simp only [decide_eq_true_eq] at hcond obtain ⟨⟨o, hoρ, hi, hrec⟩, hnd₁⟩ := (f_fold_mem Γ hwf₁ r).mp hm refine ⟨⟨o, Or.inl ((hp₁.2 o).mp hoρ), hi, hrec⟩, ?_⟩ rintro d (hd | hd) hdel · exact hnd₁ ((hdels hp₁).mpr ⟨d, hd, hdel⟩) · rcases hcond with hin2 | hout0 · have := ((f_fold_id_mem Γ hwf₂ r.1).mp hin2).2 exact this ((hdels hp₂).mpr ⟨d, hd, hdel⟩) · -- honest corner: the deleter's insert lands in the LCA obtain ⟨a, haev₂, hains, hax, -⟩ := f_del_ins_mem hHon hin₂ hcl₂ d hd r.1 hdel have hao : a = o := by apply C.ts_unique (hin₂ a haev₂) (hin₁ o ((hp₁.2 o).mp hoρ)) rw [hax, hrec]; rfl have ho₀ : o ∈ ev₁ ∩ ev₂ := ⟨(hp₁.2 o).mp hoρ, hao ▸ haev₂⟩ apply hout0 rw [f_fold_id_mem Γ hwf₀] refine ⟨⟨o, (hp₀.2 o).mpr ho₀, hi, by rw [hrec]; rfl⟩, ?_⟩ intro hdel0 obtain ⟨d', hd', hdel'⟩ := (hdels hp₀).mp hdel0 exact hnd₁ ((hdels hp₁).mpr ⟨d', hd'.1, hdel'⟩) · -- branch-2 news have hm := List.mem_of_mem_filter hr have hcond := List.of_mem_filter hr simp only [decide_eq_true_eq] at hcond obtain ⟨⟨o, hoρ, hi, hrec⟩, hnd₂⟩ := (f_fold_mem Γ hwf₂ r).mp hm refine ⟨⟨o, Or.inr ((hp₂.2 o).mp hoρ), hi, hrec⟩, ?_⟩ rintro d (hd | hd) hdel · -- a branch-1 delete would force the insert into the LCA, -- contradicting r.1 ∉ ids s₀ obtain ⟨a, haev₁, hains, hax, -⟩ := f_del_ins_mem hHon hin₁ hcl₁ d hd r.1 hdel have hao : a = o := by apply C.ts_unique (hin₁ a haev₁) (hin₂ o ((hp₂.2 o).mp hoρ)) rw [hax, hrec]; rfl have ho₀ : o ∈ ev₁ ∩ ev₂ := ⟨hao ▸ haev₁, (hp₂.2 o).mp hoρ⟩ apply hcond.1 rw [f_fold_id_mem Γ hwf₀] refine ⟨⟨o, (hp₀.2 o).mpr ho₀, hi, by rw [hrec]; rfl⟩, ?_⟩ intro hdel0 obtain ⟨d', hd', hdel'⟩ := (hdels hp₀).mp hdel0 exact hnd₂ ((hdels hp₂).mpr ⟨d', hd'.2, hdel'⟩) · exact hnd₂ ((hdels hp₂).mpr ⟨d, hd, hdel⟩) · rintro ⟨⟨o, hor, hi, hrec⟩, hnd⟩ by_cases ho₁ : o ∈ ev₁ · -- route through branch 1 left refine List.mem_filter.mpr ⟨?_, ?_⟩ · rw [f_fold_mem Γ hwf₁] refine ⟨⟨o, (hp₁.2 o).mpr ho₁, hi, hrec⟩, ?_⟩ intro hdel1 obtain ⟨d, hd, hdel⟩ := (hdels hp₁).mp hdel1 exact hnd d (Or.inl hd) hdel · simp only [decide_eq_true_eq] by_cases h0 : r.1 ∈ sIds s₀ · left obtain ⟨⟨o', ho'ρ, hi', ho'1⟩, -⟩ := (f_fold_id_mem Γ hwf₀ r.1).mp h0 have ho'₀ := (hp₀.2 o').mp ho'ρ rw [f_fold_id_mem Γ hwf₂] refine ⟨⟨o', (hp₂.2 o').mpr ho'₀.2, hi', ho'1⟩, ?_⟩ intro hdel2 obtain ⟨d, hd, hdel⟩ := (hdels hp₂).mp hdel2 exact hnd d (Or.inr hd) hdel · exact Or.inr h0 · -- o ∈ ev₂ only: route through branch 2 have ho₂ : o ∈ ev₂ := by rcases hor with h | h · exact absurd h ho₁ · exact h right refine List.mem_filter.mpr ⟨?_, ?_⟩ · rw [f_fold_mem Γ hwf₂] refine ⟨⟨o, (hp₂.2 o).mpr ho₂, hi, hrec⟩, ?_⟩ intro hdel2 obtain ⟨d, hd, hdel⟩ := (hdels hp₂).mp hdel2 exact hnd d (Or.inr hd) hdel · simp only [decide_eq_true_eq] have hnot : ∀ {ρ : List (Op FOp)} {ev : Set (Op FOp)}, listPermOf ρ ev → FWf Γ ρ → (∀ a ∈ ev, a ∈ C.events) → (∀ a ∈ ev, a ∈ ev₁) → r.1 ∉ sIds (fFold Γ ρ) := by intro ρ ev hp hwf hin hsub hmem obtain ⟨⟨o', ho'ρ, hi', ho'1⟩, -⟩ := (f_fold_id_mem Γ hwf r.1).mp hmem have ho'ev := (hp.2 o').mp ho'ρ have : o' = o := by apply C.ts_unique (hin o' ho'ev) (hin₂ o ho₂) rw [ho'1, hrec]; rfl exact ho₁ (this ▸ hsub o' ho'ev) exact ⟨hnot hp₀ hwf₀ (fun a ha => hin₁ a ha.1) (fun a ha => ha.1), hnot hp₁ hwf₁ hin₁ (fun a ha => ha)⟩ /-! ## §6b The Join: the merge is its own linearization witness Witness enumeration for the union: the LCA's enumeration, then branch one's delta (in branch order), then branch two's news. Its `respects` obligation falls to CLOSURE, and `loOn` is event-set independent under `rc = Either`, so within-block orders transfer verbatim. Sided proof, `f`-substituted. -/ open LabeledTS in theorem f_join_at {Γ : OrderedPrefixCode} {C : Sal.Emulation.Configuration (FMSig Γ).toCRDTSig} (hHon : FMHonestCore Γ C) : JoinLemma3At (FMSig Γ) C := by intro ev₁ ev₂ s₀ s₁ s₂ _htr _hir hin₁ hin₂ hcl₁ hcl₂ h₀ h₁ h₂ classical obtain ⟨ρ₀, hp₀, hr₀, hf₀⟩ := h₀ obtain ⟨ρ₁, hp₁, hr₁, hf₁⟩ := h₁ obtain ⟨ρ₂, hp₂, hr₂, hf₂⟩ := h₂ set ev₀ := ev₁ ∩ ev₂ with hev₀ have hin₀ : ∀ a ∈ ev₀, a ∈ C.events := fun a ha => hin₁ a ha.1 have hcl₀ : ∀ a b, C.vis a b → ¬ (FMSig Γ).toCRDTSig.commutes a b → b ∈ ev₀ → a ∈ ev₀ := fun a b hv hc hb => ⟨hcl₁ a b hv hc hb.1, hcl₂ a b hv hc hb.2⟩ have hinU : ∀ a ∈ ev₁ ∪ ev₂, a ∈ C.events := by rintro a (ha | ha) · exact hin₁ a ha · exact hin₂ a ha have hclU : ∀ a b, C.vis a b → ¬ (FMSig Γ).toCRDTSig.commutes a b → b ∈ ev₁ ∪ ev₂ → a ∈ ev₁ ∪ ev₂ := by rintro a b hv hc (hb | hb) · exact Or.inl (hcl₁ a b hv hc hb) · exact Or.inr (hcl₂ a b hv hc hb) have hwf₀ := f_wf_of_enum hHon hin₀ hcl₀ hp₀ hr₀ have hwf₁ := f_wf_of_enum hHon hin₁ hcl₁ hp₁ hr₁ have hwf₂ := f_wf_of_enum hHon hin₂ hcl₂ hp₂ hr₂ -- loOn is event-set independent under rc = Either have hloOn : ∀ (ev ev' : Set (Op FOp)) (x y : Op FOp), loOn C ev x y → loOn C ev' x y := by intro ev ev' x y h rw [loOn_iff_of_rc_either (FMSig_rc_either Γ)] at h ⊢ exact h -- the witness enumeration set δ₁ := ρ₁.filter (fun o => decide (o ∉ ev₀)) with hδ₁ set δ₂ := ρ₂.filter (fun o => decide (o ∉ ev₁)) with hδ₂ set ρᵤ := ρ₀ ++ (δ₁ ++ δ₂) with hρᵤ have hmemδ₁ : ∀ {o}, o ∈ δ₁ ↔ o ∈ ρ₁ ∧ o ∉ ev₀ := by intro o rw [hδ₁] simp [List.mem_filter] have hmemδ₂ : ∀ {o}, o ∈ δ₂ ↔ o ∈ ρ₂ ∧ o ∉ ev₁ := by intro o rw [hδ₂] simp [List.mem_filter] -- membership: ρᵤ enumerates the union have hmemU : ∀ o, o ∈ ρᵤ ↔ o ∈ ev₁ ∪ ev₂ := by intro o rw [hρᵤ] simp only [List.mem_append] constructor · rintro (h | h | h) · exact Or.inl ((hp₀.2 o).mp h).1 · exact Or.inl ((hp₁.2 o).mp (hmemδ₁.mp h).1) · exact Or.inr ((hp₂.2 o).mp (hmemδ₂.mp h).1) · rintro (h | h) · by_cases h0 : o ∈ ev₀ · exact Or.inl ((hp₀.2 o).mpr h0) · exact Or.inr (Or.inl (hmemδ₁.mpr ⟨(hp₁.2 o).mpr h, h0⟩)) · by_cases h1 : o ∈ ev₁ · by_cases h0 : o ∈ ev₀ · exact Or.inl ((hp₀.2 o).mpr h0) · exact Or.inr (Or.inl (hmemδ₁.mpr ⟨(hp₁.2 o).mpr h1, h0⟩)) · exact Or.inr (Or.inr (hmemδ₂.mpr ⟨(hp₂.2 o).mpr h, h1⟩)) -- nodup: blocks are nodup and pairwise set-separated have hndU : ρᵤ.Nodup := by rw [hρᵤ] rw [List.nodup_append] refine ⟨hp₀.1, ?_, ?_⟩ · rw [List.nodup_append] refine ⟨hp₁.1.filter _, hp₂.1.filter _, ?_⟩ intro a ha b hb hab subst hab exact (hmemδ₂.mp hb).2 ((hp₁.2 a).mp (hmemδ₁.mp ha).1) · intro a ha b hb hab subst hab have ha0 : a ∈ ev₀ := (hp₀.2 a).mp ha rcases List.mem_append.mp hb with h | h · exact (hmemδ₁.mp h).2 ha0 · exact (hmemδ₂.mp h).2 ha0.1 have hpU : listPermOf ρᵤ (ev₁ ∪ ev₂) := ⟨hndU, hmemU⟩ -- respects: within-blocks by transfer, cross-blocks by closure have hrU : respects ρᵤ (loOn C (ev₁ ∪ ev₂)) := by rw [hρᵤ] unfold respects at hr₀ hr₁ hr₂ ⊢ rw [List.pairwise_append] refine ⟨hr₀.imp (fun h hl => h (hloOn _ _ _ _ hl)), ?_, ?_⟩ · rw [List.pairwise_append] refine ⟨(hr₁.sublist List.filter_sublist).imp (fun h hl => h (hloOn _ _ _ _ hl)), (hr₂.sublist List.filter_sublist).imp (fun h hl => h (hloOn _ _ _ _ hl)), ?_⟩ -- cross δ₁ × δ₂: a loOn-later δ₂ event before a δ₁ event would be in ev₁ intro a ha b hb hl rw [loOn_iff_of_rc_either (FMSig_rc_either Γ)] at hl have hb1 : b ∈ ev₁ := hcl₁ b a hl.1 hl.2 ((hp₁.2 a).mp (hmemδ₁.mp ha).1) exact (hmemδ₂.mp hb).2 hb1 · -- cross ρ₀ × deltas: a loOn-later delta event before an LCA event -- would be in ev₀ intro a ha b hb hl rw [loOn_iff_of_rc_either (FMSig_rc_either Γ)] at hl have ha0 : a ∈ ev₀ := (hp₀.2 a).mp ha have hb0 : b ∈ ev₀ := hcl₀ b a hl.1 hl.2 ha0 rcases List.mem_append.mp hb with h | h · exact (hmemδ₁.mp h).2 hb0 · exact (hmemδ₂.mp h).2 hb0.1 have hwfU : FWf Γ ρᵤ := f_wf_of_enum hHon hinU hclU hpU hrU -- the fold of the witness IS the merge, by canonical-form extensionality refine ⟨ρᵤ, hpU, hrU, ?_⟩ show fFold Γ ρᵤ = (FMSig Γ).mergeL s₀ s₁ s₂ rw [← hf₀, ← hf₁, ← hf₂] show fFold Γ ρᵤ = sMergeL (fFold Γ ρ₀) (fFold Γ ρ₁) (fFold Γ ρ₂) -- cross-key-injectivity feeding the merge's sortedness have hdisj : ∀ x ∈ fFold Γ ρ₁, ∀ y ∈ fFold Γ ρ₂, sKey x.2.2 = sKey y.2.2 → x = y := by intro x hx y hy hkey obtain ⟨o₁, hm₁, hi₁, hrec₁⟩ := f_fold_rec_sub Γ ρ₁ x hx obtain ⟨o₂, hm₂, hi₂, hrec₂⟩ := f_fold_rec_sub Γ ρ₂ y hy have he₁ : o₁ ∈ C.events := hin₁ o₁ ((hp₁.2 o₁).mp hm₁) have he₂ : o₂ ∈ C.events := hin₂ o₂ ((hp₂.2 o₂).mp hm₂) have hkey' : sKey (fCoord Γ o₁) = sKey (fCoord Γ o₂) := by rw [hrec₁, hrec₂] at hkey exact hkey have hids : o₁.1 = o₂.1 := by by_contra hne exact f_keys_inj_events hHon o₁ he₁ o₂ he₂ hi₁ hi₂ hne hkey' have : o₁ = o₂ := C.ts_unique he₁ he₂ hids rw [hrec₁, hrec₂, this] apply ssorted_ext (f_fold_sorted Γ hwfU) (sMergeL_sorted (f_fold_sorted Γ hwf₁) (f_fold_sorted Γ hwf₂) hdisj) intro r rw [f_fold_mem Γ hwfU r, f_mergeL_mem hHon hin₁ hin₂ hcl₁ hcl₂ hp₀ hp₁ hp₂ hwf₀ hwf₁ hwf₂ r] constructor · rintro ⟨⟨o, hm, hi, hrec⟩, hnd⟩ have hor : o ∈ ev₁ ∨ o ∈ ev₂ := by rcases (hmemU o).mp hm with h | h · exact Or.inl h · exact Or.inr h refine ⟨⟨o, hor, hi, hrec⟩, ?_⟩ intro d hd hdel apply hnd apply mem_fDels.mpr refine ⟨d, (hmemU d).mpr ?_, hdel⟩ rcases hd with h | h · exact Or.inl h · exact Or.inr h · rintro ⟨⟨o, hor, hi, hrec⟩, hnd⟩ have hmU : o ∈ ev₁ ∪ ev₂ := by rcases hor with h | h · exact Or.inl h · exact Or.inr h refine ⟨⟨o, (hmemU o).mpr hmU, hi, hrec⟩, ?_⟩ intro hdel obtain ⟨d, hd, hdel'⟩ := mem_fDels.mp hdel rcases (hmemU d).mp hd with h | h · exact hnd d (Or.inl h) hdel' · exact hnd d (Or.inr h) hdel' /-! ## §7 Honest reachability and the capstone -/ /-- Honest histories at the ternary configuration: every delete names an id its issuer had observed (a `vis`-prior insert), and inserts are chain-generated over the variant alphabet (positive, tag-wellformed, telescoping). The FM datatype's `HonestDelivery`. -/ def FMHonest (Γ : OrderedPrefixCode) (C : Configuration (FMSig Γ)) : Prop := (∀ e ∈ C.events, ∀ x : ℕ, e.2.2 = FOp.del x → ∃ a ∈ C.events, C.vis a e ∧ a.1 = x ∧ fIsIns a = true) ∧ (∃ chainOf : ℕ → FMChain, ∀ o ∈ C.events, fIsIns o = true → PosFMChain (chainOf o.1) ∧ TagsOK (chainOf o.1) ∧ fCoord Γ o = fmCoordOf Γ (chainOf o.1) ∧ ((chainOf o.1).map fmδ).sum = o.1) theorem fmHonest_core {Γ : OrderedPrefixCode} {C : Configuration (FMSig Γ)} (h : FMHonest Γ C) : FMHonestCore Γ (Configuration.core C) where del_has_ins := by intro e he x hx rw [core_events] at he obtain ⟨a, ha, hv, hax, hai⟩ := h.1 e he x hx refine ⟨a, ?_, hv, hax, hai⟩ rw [core_events] exact ha chain_gen := by obtain ⟨chainOf, hch⟩ := h.2 refine ⟨chainOf, fun o ho hi => hch o ?_ hi⟩ rw [core_events] at ho exact ho /-- **Honest reachability**: LTS reachability where every step is taken from a configuration with an honest history, instantiating the generic `HonestReach`, exactly as the sided instance and the mergeable queue do. -/ def FMReach (Γ : OrderedPrefixCode) : Configuration (FMSig Γ) → Prop := HonestReach (FMSig Γ) (FMHonest Γ) trivial theorem fm_goodConfig3 {Γ : OrderedPrefixCode} {C : Configuration (FMSig Γ)} (hReach : FMReach Γ C) : GoodConfig3 C := goodConfig3_of_honest_reach (fun _ hHon => f_join_at (fmHonest_core hHon)) hReach /-- **The FugueMax variant datatype is RA-linearizable, per version, at every honestly reachable configuration**: the sided capstone re-instantiated for the FM-tagged coordinate format. The right-origin tags ops carry are payload to this theorem, exactly as sides were to the sided capstone. This separates the policy from the datatype: `mGenInsAfter` (the FugueMax mint of `SidedRGA_FugueMax.lean`) is a generation policy above this one verified kernel. Parametric in the delta code Γ. -/ theorem fuguemax_ra_linearizable3 {Γ : OrderedPrefixCode} {C : Configuration (FMSig Γ)} (hReach : FMReach Γ C) : IsRALinearizable3 C := isRALinearizable3_of_good (fm_goodConfig3 hReach) #print axioms fuguemax_ra_linearizable3 /-! ## §7½ The bridge to the generation layer `SidedRGA_FugueMax.lean`'s display fold `mFold` (over generation records `MRec`) IS this signature's fold of the mapped enumeration: an insert record denotes the `FOp.ins` carrying its chain's coordinate split as (prefix of all but the last entry, minted entry). So `f_fold_canon` covers the generation layer's states, and `MaxReach` configurations are runs of the verified datatype. -/ /-- The op a generation record denotes. The `.ins` arm splits the chain as (everything but the last entry, the minted entry); the empty-chain arm is degenerate (unreachable on honest knowledge: deltas telescope to a positive id). -/ def fOpOfM (Γ : OrderedPrefixCode) (g : MRec) : Op FOp := match g.op, g.chain.getLast? with | .ins _ _, some ent => (g.ts, g.rep, .ins g.ts (fmCoordOf Γ g.chain.dropLast) ent) | .ins _ _, none => (g.ts, g.rep, .ins g.ts [] (.L 0)) | .del x, _ => (g.ts, g.rep, .del x) /-- One step of the generation-layer fold is one step of the datatype. -/ theorem fUpdate_fOpOfM (Γ : OrderedPrefixCode) (s : SState) {g : MRec} (hch : mIsIns g = true → g.chain ≠ []) : fUpdate Γ s (fOpOfM Γ g) = mStep Γ s g := by cases hop : g.op with | del x => unfold fOpOfM mStep rw [hop] cases g.chain.getLast? <;> rfl | ins p sd => have hins : mIsIns g = true := by simp [mIsIns, hop] have hne := hch hins cases hlast : g.chain.getLast? with | none => exact absurd (List.getLast?_eq_none_iff.mp hlast) hne | some ent => obtain ⟨pre, hpre⟩ := List.getLast?_eq_some_iff.mp hlast have hcoord : fmCoordOf Γ g.chain.dropLast ++ fmBlock Γ ent = fmCoordOf Γ g.chain := by rw [hpre, List.dropLast_concat, fmCoordOf_append] simp [fmCoordOf] unfold fOpOfM mStep rw [hop, hlast] show (if g.ts ∈ sIds s then s else sInsert (g.ts, g.ts, fmCoordOf Γ g.chain.dropLast ++ fmBlock Γ ent) s) = (if g.ts ∈ sIds s then s else sInsert (g.ts, g.ts, fmCoordOf Γ g.chain) s) rw [hcoord] /-- **The generation-layer fold is the datatype fold**: on knowledges whose insert records carry nonempty chains (all honest ones), `mFold` is `fFold` of the mapped enumeration. -/ theorem mFold_eq_fFold (Γ : OrderedPrefixCode) : ∀ (K : KnowM), (∀ g ∈ K, mIsIns g = true → g.chain ≠ []) → mFold Γ K = fFold Γ (K.map (fOpOfM Γ)) := by intro K induction K using List.reverseRecOn with | nil => intro _; rfl | append_singleton K g ih => intro hch rw [List.map_append, List.map_singleton, mFold_snoc, fFold_snoc, ih (fun g' hg' => hch g' (List.mem_append_left _ hg')), fUpdate_fOpOfM Γ _ (hch g (List.mem_append_right _ (by simp)))] /-- Insert records of a `KInv`-satisfying knowledge carry nonempty chains (their deltas telescope to a positive id). -/ theorem kinv_chain_ne_nil {Γ : OrderedPrefixCode} {K : KnowM} (inv : KInv Γ K) : ∀ g ∈ K, mIsIns g = true → g.chain ≠ [] := by intro g hg hi hnil have hsum := (inv.wf g hg hi).2.2 rw [hnil] at hsum have hpos := inv.pos g hg simp at hsum omega /-- **Fold-canonicity for `mFold`**: two knowledges whose mapped enumerations are well-formed and enumerate the same events display the same state, the generation-layer face of `f_fold_canon`. -/ theorem m_fold_canon (Γ : OrderedPrefixCode) {K K' : KnowM} (hch : ∀ g ∈ K, mIsIns g = true → g.chain ≠ []) (hch' : ∀ g ∈ K', mIsIns g = true → g.chain ≠ []) (hwf : FWf Γ (K.map (fOpOfM Γ))) (hwf' : FWf Γ (K'.map (fOpOfM Γ))) (hmem : ∀ o, o ∈ K.map (fOpOfM Γ) ↔ o ∈ K'.map (fOpOfM Γ)) : mFold Γ K = mFold Γ K' := by rw [mFold_eq_fFold Γ K hch, mFold_eq_fFold Γ K' hch', f_fold_canon Γ hwf hwf' hmem] #print axioms f_fold_canon #print axioms mFold_eq_fFold #print axioms m_fold_canon /-! ## §8 SPOTs (PASS+FAIL, hand-derived) Unary code: `enc d = replicate d true ++ [false]`; `compl` negates; `symR : false ↦ 1, true ↦ 2`; `fw k = [(8-k)/3, (8-k)%3]` so `fw 0 = [2,2]`, `fw 1 = [2,1]`, `fw 2 = [2,0]`, `fw 3 = [1,2]`; `fmBlock (.R t d) = fwTag t ++ map symR (compl (enc d))`; `sKey c = c ++ [3]`; the state is sorted strictly DESCENDING by key. -/ namespace FugueMaxRALinSPOT /-! ### Same-tag R siblings: ascending delta, order-insensitive fold -/ def opA : Op FOp := (1, 0, FOp.ins 11 [] (.R [0] 1)) def opB : Op FOp := (2, 1, FOp.ins 22 [] (.R [0] 2)) def ρTie : List (Op FOp) := [opA, opB] /-- PASS, record-level: hand-derived coordinates. `coord opA = fwTag [0] ++ map symR (compl [t,f]) = [2,2] ++ [1,2]`; `coord opB = [2,2] ++ map symR [f,f,t] = [2,2,1,1,2]`. First key difference at index 3 (`2` vs `1`), so id 1 displays first. -/ theorem tie_fold : fFold unaryCode ρTie = [(1, 11, [2, 2, 1, 2]), (2, 22, [2, 2, 1, 1, 2])] := by native_decide /-- PASS: same-tag siblings ascend by delta, the display twin of the generation layer's `tie_display`. -/ theorem tie_ids : sIds (fFold unaryCode ρTie) = [1, 2] := by native_decide /-- FAIL pin: the descending order is NOT displayed. -/ theorem tie_ids_not_desc : sIds (fFold unaryCode ρTie) ≠ [2, 1] := by native_decide /-- FAIL pin: the fold is not constantly empty. -/ theorem tie_fold_ne_empty : fFold unaryCode ρTie ≠ [] := by native_decide /-- PASS: fold-canonicity made concrete, the reversed enumeration folds to the SAME state (the enumeration order is erased). -/ theorem tie_fold_order_erased : fFold unaryCode [opB, opA] = fFold unaryCode ρTie := by native_decide /-! ### The tag is decisive: it overrides ascending-id order -/ def opA2 : Op FOp := (2, 0, FOp.ins 22 [] (.R [0] 2)) /-- Right origin = `opA2` (tag = its key `[2,2,1,1,2,3]`), the FugueMax-critical shape: an R sibling anchored at a LIVE right origin. -/ def opB2 : Op FOp := (1, 1, FOp.ins 11 [] (.R [2, 2, 1, 1, 2, 3] 1)) /-- PASS: the end-tagged sibling (right origin `end`, display-later) precedes the live-origin sibling despite its LARGER id: `coord opA2 = [2,2,1,1,2]`; `coord opB2 = fwTag [2,2,1,1,2,3] ++ [1,2] = [2,0,2,0,2,1,2,1,2,0,1,2,1,2]`; first key difference at index 1 (`2` vs `0`). The tag overrides the id order. -/ theorem tag_decisive_ids : sIds (fFold unaryCode [opA2, opB2]) = [2, 1] := by native_decide /-- FAIL pin: the ascending-id (plain-Fugue tiebreak) order is NOT displayed, the pin that kills every re-banding without tags. -/ theorem tag_decisive_not_id_order : sIds (fFold unaryCode [opA2, opB2]) ≠ [1, 2] := by native_decide /-! ### Delete and merge -/ def ρDel : List (Op FOp) := ρTie ++ [(3, 0, FOp.del 1)] /-- PASS: delete removes exactly its target. -/ theorem del_ids : sIds (fFold unaryCode ρDel) = [2] := by native_decide /-- FAIL pin: the delete is not a no-op. -/ theorem del_not_noop : sIds (fFold unaryCode ρDel) ≠ [1, 2] := by native_decide /-- FAIL pin: the delete did not clobber the survivor. -/ theorem del_not_clobber : sIds (fFold unaryCode ρDel) ≠ [] := by native_decide /-- PASS: the ternary merge of the two singleton branches (empty LCA) is the canonical two-record state, hand-derived, same keys as `tie_fold`. -/ theorem merge_ids : sIds (sMergeL [] (fFold unaryCode [opA]) (fFold unaryCode [opB])) = [1, 2] := by native_decide /-- FAIL pin: the merge is not a projection of either input. -/ theorem merge_not_projection : sMergeL [] (fFold unaryCode [opA]) (fFold unaryCode [opB]) ≠ fFold unaryCode [opA] ∧ sMergeL [] (fFold unaryCode [opA]) (fFold unaryCode [opB]) ≠ fFold unaryCode [opB] := by native_decide end FugueMaxRALinSPOT #print axioms FugueMaxRALinSPOT.tie_fold #print axioms FugueMaxRALinSPOT.tag_decisive_ids end Sal.ConditionedMRDTs