Simultaneous encodings for range and next/previous larger/smaller value queries
Established nearest-smaller encoding prior art. Abstract and publisher results excerpt inspected; not independently reproduced.
Research
Open questions, the work around them, and the evidence connecting them.
Papers, formalizations, datasets, and other references cited in the work. Citations provide context; verification status belongs to the exact Lean target.
On Succinct Representations of Binary Trees
Established Cartesian/RMQ/tree-navigation theory. Abstract and selected sections inspected; not independently reproduced.
Weidner position-strings: exact base52 digit encoder and parser
src/position_source.ts stringifyBase52 and parseBase52
The Lean digit definitions port the exact ASCII branches: digit<26 maps to 65+digit, otherwise 71+digit; parser subtracts 71 at code>=97, otherwise 65. Target #38 proves one valid digit round trip and strict order, not the full variable-length codec or native JS refinement.
Weidner sparse-array-rled: compact tombstones and count/index correspondence
SparseArray serialization, present entries and count/index conversion; SparseString; SparseIndices
Supports separate future proofs of RLE serialization round trip, visible-rank/index conversion and equivalence to an uncompressed sparse array. Used by list-positions; no balance/performance proof or native-code correctness claimed.
Weidner uniquely dense total order prototype
UniquelyDenseTotalOrder interface; tree/string Fugue variants
Makes allocation-between and uniqueness explicit as an abstract data-type contract. README warns the prototype was minimally tested and points to Collabs/position-strings for published versions. This is source evidence, not a machine proof.
Weidner: versioned collaborative documents — diff as undo and replay
Versioning model and operations for switching versions
Design proposal for common-root operation histories, merging and version changes by undo/replay. A candidate for linking patch inversion/composition to CRDT history, not an existing verified implementation.
Weidner: text editing without CRDTs or OT — revised relationship to Fugue
Decentralized Collaboration; correction dated 8/9/26; Articulated persistence
The updated post says depth-first topological order gives behavior similar to Fugue, retracting equivalence. Lamport timestamp ordering corresponds to RGA/causal trees. Keep each ordering and server reconciliation model distinct.
Weidner Articulated: stable element IDs and bulk allocation
ElementIdGenerator.generateAfter; IdList and IdListSimple implementations
Proof candidates include disjoint allocated ID intervals, lookup/visible-index correspondence through tombstones, serialization and reconciliation. ID uniqueness and counter range must be explicit; tests/fuzzing do not constitute formal verification.
Weidner and Almeida: oblivious observed-reset embeddable counter
Algorithm 1; Theorem 4.1; Proposition 4.2
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.
Weidner et al.: for-each applies to prior and concurrent insertions
Appendix A: Theorems A.1-A.2 and Corollary A.3
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.
Collabs number demo: concrete semidirect message transformation
CNumber.action case 3; AddComponent; MultComponent
The demo transforms lower-priority message arguments by multiplication. It also includes min/max/add transformations and JavaScript Number arithmetic, which the integer Lean target does not cover.
Weidner, Miller and Meiklejohn: composing op-based CRDTs with semidirect products
Add/multiply example; Theorem 3.4
The paper proves the general operational construction. The Hunchroom Lean module verifies only the concrete unbounded-integer reordering and multiply-action laws, including arbitrary history permutation.
Weidner and Kleppmann: Fugue strong-list correctness; FugueMax maximal non-interleaving
Theorem 1; Definition 4; Lemmas 7-8; Theorems 9-10
Human proofs establish strong-list semantics for Fugue and maximal non-interleaving for FugueMax, including a semantic uniqueness result. They are future Lean obligations, not established by the conditional path-order lemma.
Weidner list-positions: structured positions and lexicographic serialization
src/order/lexicographic_string.ts; internals/README.md
Structured bunch IDs, inner indices and parent metadata are serialized using escaped ID delimiters and lex-sequence. Internal documentation identifies Fugue and rare backward interleaving, so it should not be equated with the stronger FugueMax guarantee.
Weidner lex-sequence: inverse, order, prefix freedom and length obligations
src/index.ts first, last, successor, sequence, sequenceInvSafe; README About/Misc
A compact, promising next formalization: exact inverse and successor, numeric/lexicographic order, prefix freedom and digit-length bound. Uses Number, Math.log and Math.pow; an unbounded Nat port would need a separate JavaScript safety refinement.
Weidner: position strings for collaborative lists and text
Position allocation; relation to Fugue; efficiency discussion
Primary explanation of the construction. Treat ordering, uniqueness, non-interleaving and logarithmic growth as separate obligations. The local Lean results are new supporting mechanizations, not a reproduced author proof.
Weidner position-strings: tree-path encoding and prefix-free label conditions
algorithm.md encoding conditions (i), (ii); src/position_source.ts stringifyBase52, parseBase52, nextOddValueSeq
Supports the suffix-stability and run-separation model. The code alphabet is ported separately; neither the full label language nor createBetween is verified by those targets.
Parent exact tuple model and causal projection question
Same indexOf, scan, insert, apply, generate, replay, and validity functions; removed only unused reconstruction definitions.
Verified string search: Imperative-HOL KMP returns the first match or proves absence
thys/Knuth_Morris_Pratt/KMP.thy; kmp_impl_correct; kmp_impl_correct'
kmp_impl_correct preserves the pattern/text arrays and returns None exactly when no match exists, or Some i at the first matching offset. Useful for string/rope search and diff anchoring; it neither proves diff minimality nor correspondence to an arbitrary production search routine. The inspected theorem is functional correctness, not a formal runtime bound.
Coq dependent finger trees and ropes: typed measure invariants, with unfinished wrappers
DependentFingerTree.v; DependentFingerTree.app; split_tree; RopeModule.get
The dependent app type returns a tree whose index is the combined measure; split_tree packages its specification in a dependent result. RopeModule.v implements strings as measured chunks. Caveat: wrapper size lemmas are admitted and the sequence specialization declares an extra axiom. Treat this as qualified source evidence, not a fully audited or reproduced library.
Isabelle finger trees: concatenation, measured splitting and list refinement
thys/Finger-Trees/FingerTree.thy; app_correct; app_list; splitTree_invpres; splitTree_correct; foldl_correct
A complete external functional model for rope-like measured sequences: concatenation denotes list append; split preserves invariants and reconstructs contents at the predicate boundary; fold agrees with list fold. No formal logarithmic-time bound or refinement to a production rope library is claimed. The Hunchroom chunked-sequence model only extracts reference obligations.
Coq tree-command inversion: every successful command has an undo
TreeOt.v; tree_ip1; treeInv
tree_ip1 proves tree_interp (tree_inv op) result = Some source after successful execution; includes subtree edits. This provides a concrete structural instance of the inverse contract used by the Hunchroom replay theorem. TreeOt.v is completed; the separate rich-text extension has admitted proofs and is excluded.
VeriFx sequence OT: C1 proof obligations and C2 counterexamples
examples/OT Verification/src/main/verifx/org/verifx/otproofs/OT.vfx; OT.C1; OT.C2; Ressel.C1_inserts/C1_deletes/C1_mix1/C1_mix2; Ressel.C2 (expected refutation)
OT.vfx defines application-order equality C1 and transformation-path equality C2. ResselTest.scala and ImineTest.scala expect C1 cases to prove but C2 to be rejected. This is valuable negative evidence: pairwise transformation correctness does not establish three-operation consistency. Tests inspected, not executed here.
Coq operational transformation for trees: successful transformed operations commute
TreeOt.v; tree_c1; treeOT
tree_c1 is completed with Qed and proves equal successful results of the two transformed execution orders. TreeOt.v dependencies inspected without admitted proofs found. RichText.v contains active admit/Admitted occurrences, so the rich-text extension and whole repository must not be called fully verified. C1 alone is not a C2 or network SEC proof.
Replicated tree moves: executable hash-map algorithm refines the abstract model
proof/Move_Code.thy; executable_apply_ops_simulates; executable_apply_ops_acyclic; executable_apply_ops_commutes
This proof connects executable Isabelle definitions to abstract operations. Its commutation theorem gives equal logs and equal lookups, not identical concrete memory layouts. The README explicitly says the separate hand-optimized evaluation implementation is not verified; only the Isabelle-generated implementation has this correspondence.
VeriFx CRDT portfolio: merge laws, delta counters and corrected-map counterexamples
examples/CRDT Verification/src/main/verifx/org/verifx/crdtproofs/lemmas/CvRDTProof.vfx; CvRDTProof.is_a_CvRDT; mergeCommutative; mergeIdempotent; mergeAssociative; KMapFixed.putDelCommute
GCounter and delta-counter source plus the CRDT proof tests inspected. The tests expect KMap put/delete commutation to be refuted and KMapFixed laws to be proved: the artifact includes failures as well as successes. These are SMT obligations and declared test expectations, not a replayed proof run or a Lean certificate of this target.
Replicated tree moves: commutation, unique parents, acyclicity and SEC
proof/Move_SEC.thy; Move.apply_ops_commutes; Move_Acyclic.apply_ops_acyclic; concurrent_operations_commute; sec: strong_eventual_consistency
Move.thy and Move_Acyclic.thy establish structural safety alongside convergence. Move_SEC.thy instantiates the AFP strong_eventual_consistency locale. These tree-move results are substantially richer than the posted grow-only-set target, and need their own formal targets to claim exact Hunchroom verification.
OpSets: RGA specification refinement and non-interleaving of insertion runs
thys/OpSets/Interleaving.thy; no_interleaving; missing_start_no_insertion; RGA.rga_meets_spec
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.
Diamond Types insertion scan
Motivation for preserving exact origins and record identity; no formal Rust refinement.
Angiuli, Morehouse, Licata and Harper: Homotopical Patch Theory
Higher inductive patch theory; expanded paper
Foundational account connecting patch operations, invertibility and equations between edit histories using homotopy type theory. Useful for choosing future patch algebra obligations. Classified here as a paper-level theoretical source: no complete runnable machine-checked development was located or reproduced. It does not prove this Option-based sequential replay target.