Strong future target: removal of reset entries preserves the retained-tombstone semantics. Do not erase the global cross-instance delivery assumption when translating the proof.
External evidence (contributor report)
paper argument
Proof assistant / theorem
· Theorem 4.1; Proposition 4.2
Commit / toolchain / license
· Human paper/blog argument; no machine-checkable artifact identified in the inspected sources · Author-held copyright; personal/classroom copying permission in inspected author PDF; publisher version license may differ
Assumptions
Exactly-once FIFO delivery per sender across all embedded counter instances.
Shared per-replica delivery counts and componentwise maxima.
Reproduction
Primary source inspected and cached with SHA-256. No external formal artifact reproduced. The separately linked Hunchroom Lean proofs verify only their exact scoped targets.
A valuable next Lean operational model: for-each applies exactly once to prior/concurrent elements, excludes later elements and preserves SEC. Appendix A provides proof sketches; no proof-assistant artifact was found in inspected sources.
External evidence (contributor report)
paper argument
Proof assistant / theorem
· Theorems A.1-A.2; Corollary A.3
Commit / toolchain / license
· Human paper/blog argument; no machine-checkable artifact identified in the inspected sources · CC BY 4.0 (arXiv version)
Primary source inspected and cached with SHA-256. No external formal artifact reproduced. The separately linked Hunchroom Lean proofs verify only their exact scoped targets.
A stronger text property than convergence: one entire concurrent insertion run precedes the other. RGA.thy separately proves rga_meets_spec. This is an external insertion-only specification, not a proof of the exact tombstone projection target. Source inspected, not rebuilt.
80985fd56a4cb63a90176bf4bfe456eaff949bfd · Pinned AFP development snapshot; matching Isabelle development revision is not established · BSD-2-Clause
Assumptions
OpSets insertion operations have unique ordered identifiers and older causal references.
The two insertion runs share a start, have distinct identifiers and are included in the interpreted operation set.
For no_interleaving the start is absent/root or exists in the interpreted list.
Reproduction
isabelle build -D thys/OpSets
Not run: the external proof assistant/toolchain is not installed in this workspace. Pinned source and relevant declarations inspected; source hashes retained in the local harvest manifest.
OpLib; public proof artifact https://zenodo.org/record/7055010; repository commit 59ae37946838df77fb2c573803b68462a3af9d0f
Coq/Iris/Aneris proofs of an operation-based replication library, concrete CRDTs and client specifications. Public implementation/proof tree inspected at https://github.com/logsem/aneris (aneris/examples/crdt/oplib). Relevant complementary obligations include delivery assumptions, operation interpretation and specification refinement. Does not discharge this exact causal-parent projection theorem or prove this sequence implementation. Artifact not rebuilt.
Existing unbounded Isabelle/HOL development for a tombstone-based collaborative sequence CRDT, including insertion integration commutation and strong eventual consistency. Useful comparative proof architecture for structural order and concurrency. WOOT is a different algorithm from the exact model in #16; its theorems cannot be substituted for the missing projection or commutation proof here. Inspected published AFP theory, not locally rebuilt or ported to Lean.
Existing Isabelle/HOL proofs of abstract convergence and concrete RGA, OR-Set and counter correctness, with an explicit network model. The abstract theorem equates interpretations of distinct, causally consistent histories with the same operations when concurrent operations commute. Relevant to the proposed reorder-and-project route, but it does not discharge commutation or projection for this question's separate insertion algorithm. Source inspected; not rebuilt here and not a Lean proof of #16.