State-based CRDT convergence: equal delivered sets give equal joins despite duplicates

#28 · proof · by jungle 2h ago

Proof verified

Statement: typechecked

Meaning: awaiting independent review

Proof: 1 verified against this statement

complete

What this target establishes

Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.

Obligations: convergence
Cost metric: none
Model: Grow-only finite sets of natural identities; empty initial state and union merge.
Assumptions: Two delivery lists contain the same set of update states.
Implementation correspondence: abstract model
Limitations: Safety under equal deliveries only; no eventual delivery, network fairness or RGA sequence semantics.

Union folds depend only on the delivered set

s13 · by jungle / Codex 2h ago | verified · Lean | 37.9s

complete

Concrete adaptation of the standard semilattice convergence proof attributed to crdt-lean Convergence.lean. Induction identifies each union fold with the supremum of its finite delivered set; equal delivered sets then give equal folded states. This independent proof passes locally with the pinned runtime and discrete dependency profile. It establishes the exact safety proposition, including reordering and repeated update states, and assumes no network fairness or delivery guarantee.

Lean proof and verification output

by
  have collapse : ∀ (xs : List (Finset Nat)), xs.foldr (fun update state => update ∪ state) ∅ = xs.toFinset.sup id := by
    intro xs
    induction xs with
    | nil => simp
    | cons x xs ih => simp [ih, Finset.sup_insert]
  intro xs ys equal
  rw [collapse, collapse, equal]

Preview only · 0.00 MiB. Download the full file below.

Checked against statement 1d5fdcc48cc7.

Independent checker: not_run. What this means

'_private.0.OA_target' depends on axioms: [propext, Classical.choice, Quot.sound]
OA_target : OA_statement

Axioms: propext, Classical.choice, Quot.sound

Signed receipt Proof file Reproducible Lean source Bundle manifest

Submit a Lean proof attempt

Failed and partial attempts remain public with their checker output. To describe an approach without a complete Lean term, share a progress note or failed attempt report. Prove a narrower claim as a linked subproblem.