hunch

Exact causal-parent projection for a tombstone-preserving list CRDT

Report a concern

#16 · proof · by jungle 4h ago

Open

Statement: typechecked

Meaning: awaiting independent review

Proof: no verified proof

complete

Can the exact structural state of an event's causal parents be reconstructed by filtering the final state of a successful list-CRDT replay and restoring the parent-context tombstone flags? The challenge is the supporting semantic lemma below, not a runtime claim. The parent history may omit concurrent events earlier in the serialization, so it need not be a serialization prefix. Preserving visible text alone is insufficient: deleted but known items can remain insertion anchors. Model and tuple notation • Id = Nat × Nat, interpreted as actor and sequence number. • Ins = Id × Id × Nat × Option Id × Option Id: ordering identity, immutable label, payload, left origin, right origin. • Item = Ins × Bool, with true meaning deleted. State = List Item, including tombstones. • Op = Sum Ins Id: insertion or deletion of an identity. • Edit = Sum (Nat × Id × Nat) Nat: insert at a visible position with a supplied label/payload, or delete at a visible position. • Event = Id × List Id × Edit × Op: event identity, explicit causal past, user edit, recorded generated operation. History = List Event. The statement contains the entire executable model using typed lambda applications, because the venue disallows custom definitions and local := bindings in statements. Names inside those applications are indexOf, leftAfter, rightBefore, idBefore, scan, insert, apply, visible, generate, replayOps, replay, ids, parentContext, validExtension, validHistory and reconstruct. Products associate to the right. None of these names is a theorem assumed as an axiom. Insertion scans the structural interval between the two origins, including deleted items, using actor/sequence ordering to break equal-origin ties. Delete marks the existing item and retains it. Edit generation chooses a visible left neighbor, then the immediate structural right neighbor, which may be deleted. Replay folds the recorded operations from empty state and propagates errors. Errors 0–5 denote missing origin, duplicate identity, invalid interval, missing delete target, position out of bounds and exhausted scan fuel. Valid history means every event has a fresh identity, refers only to earlier event identities, has a transitively closed past, includes previous events from the same actor with lower sequence numbers, and records precisely the operation generated from successfully replaying its own parent context. These assumptions do not assert the desired projection equation. Complete full-history replay success is a separate explicit premise. For each actual event, P is the history filtered by membership in that event's past. Reconstruct selects from the final structural state precisely those items whose insertion identities appear in P, preserving all immutable fields and their final relative order. It then restores each selected item's deleted flag using existence of a deletion of that identity in P. The requested conclusion is replay(P) = ok(reconstruct(P, finalState)). This Boolean deletion model does not model the native implementation's multiplicity counters. Attempt and remaining obstacle The empty-parent case has a direct Lean proof; a partial attempt is supplied separately. In our local project, we also have a proved serialization-prefix reconstruction theorem for the reference model. Neither settles non-prefix parents. A possible route is to stably move P to the front of the serialization, prove operation commutation/convergence and preservation of successful replay, and then apply prefix reconstruction. Establishing validity of the reordered history by assuming the desired projection would be circular. That missing step remains open here. Research motivation and limits We are exploring exact causal preparation for histories consisting of a linear source and concurrent remote edits. A useful eventual algorithm would answer identity-sensitive queries without walking every source version, with preprocessing, causal-context access, maintained order, tombstones, output and storage all charged. This challenge supplies only a semantic prerequisite. It proves no efficiency gain, memory bound, native refinement or new convergence result. It is plausibly an instance of established list-CRDT convergence reasoning. We welcome a proof or a counterexample under the exact stated model. Prepared by James Addison (jungle) with Codex, with a separate adversarial AI evaluator checking the local statement and tests. AI review is not an independent human statement review on this site. The platform's own Lean checker determines its displayed status. Port validation: the self-contained statement has been locally typechecked and source-reviewed, with finite Lean kernel controls. A universal port-equivalence theorem to the separately defined local project model is not claimed. The exact expression published here is the challenge.

Formal statement

(fun (indexOf : (Nat×Nat)→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option Nat) =>
(fun (leftAfter : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>
(fun (rightBefore : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>
(fun (idBefore : (Nat×Nat)→(Nat×Nat)→Bool) =>
(fun (scan : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))→Nat→Nat→Nat→Nat→Bool→Nat→Except Nat Nat) =>
(fun (insert : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (apply : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (visible : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (generate : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(Nat×Nat)→(Sum (Nat×(Nat×Nat)×Nat) Nat)→Except Nat (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))) =>
(fun (replayOps : List (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (replay : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (ids : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→List (Nat×Nat)) =>
(fun (validExtension : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))→Prop) =>
(fun (validHistory : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→Prop) =>
(fun (reconstruct : List (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (parentContext : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))→(List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))) =>
∀ (history : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))) (finalState : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))),
validHistory history→replay history = .ok finalState→∀ (event : ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))), event ∈ history→replay (parentContext history event) =
.ok (reconstruct ((parentContext history event).map (fun e => e.2.2.2)) finalState)
) (fun history event =>
history.filter (fun previous => event.2.1.any (fun id => id == previous.1)))
) (fun ops finalState =>
(fun (born dead : List (Nat×Nat)) =>
(finalState.filter (fun item => born.any (fun id => id == item.1.1))).map
(fun item => (item.1, dead.any (fun id => id == item.1.1))))
(ops.filterMap (fun op => match op with | .inl ins => some ins.1 | .inr _ => none))
(ops.filterMap (fun op => match op with | .inl _ => none | .inr target => some target)))
) (fun history =>
List.rec (fun _ : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))) => True)
(fun event _ rest pre => validExtension pre event ∧ rest (pre ++ [event])) history [])
) (fun pre event =>
event.1 ∉ ids pre ∧
(∀ id ∈ event.2.1, id ∈ ids pre) ∧
(∀ previous ∈ pre, previous.1 ∈ event.2.1→∀ id ∈ previous.2.1, id ∈ event.2.1) ∧
(∀ previous ∈ pre, previous.1.1 = event.1.1→previous.1.2 < event.1.2 ∧ previous.1 ∈ event.2.1) ∧
∃ sourceState,
replay (pre.filter (fun previous => event.2.1.any (fun id => id == previous.1))) = .ok sourceState ∧
generate sourceState event.1 event.2.2.1 = .ok event.2.2.2)
) (fun history => history.map (fun event => event.1))
) (fun history =>
replayOps (history.map (fun event => event.2.2.2)) [])
) (fun ops start =>
ops.foldl (fun prior op => prior.bind (fun state => apply state op)) (.ok start))
) (fun state fresh edit =>
match edit with
| .inl (pos, label, payload) => do
if (visible state).length < pos then throw 4
(fun (left : Option (Nat×Nat)) => do
let start ← leftAfter state left
return .inl (fresh, label, payload, left, (state[start]?).map (fun x => x.1.1))) (if pos = 0 then none else ((visible state)[pos - 1]?).map (fun x => x.1.1))
| .inr pos => match (visible state)[pos]? with
| none => .error 4
| some item => .ok (.inr item.1.1))
) (fun state => state.filter (fun item => !item.2))
) (fun state op =>
match op with
| .inl ins => insert state ins
| .inr target =>
if (indexOf target state).isSome then
.ok (state.map fun item => if item.1.1 = target then (item.1, true) else item)
else .error 3)
) (fun state ins => do
if (indexOf ins.1 state).isSome then throw 1
let left ← leftAfter state ins.2.2.2.1
let right ← rightBefore state ins.2.2.2.2
if right < left then throw 2
let dest ← scan state ins left right state.length left false left
return state.take dest ++ [(ins, false)] ++ state.drop dest)
) (fun state ins left right fuel =>
Nat.rec
(fun i scanning back =>
if right ≤ i then .ok (if scanning then back else i) else .error 5)
(fun _ recur i scanning back => do
if right ≤ i then return if scanning then back else i
let other ← match state[i]? with
| none => .error 4
| some item => .ok item
if other.1.2.2.2.1 = ins.2.2.2.1 then
if other.1.2.2.2.2 = ins.2.2.2.2 then
if idBefore ins.1 other.1.1 then return if scanning then back else i
else recur (i + 1) false back
else
let otherRight ← rightBefore state other.1.2.2.2.2
if otherRight < right then recur (i + 1) true (if scanning then back else i)
else recur (i + 1) false back
else
let otherLeft ← leftAfter state other.1.2.2.2.1
if otherLeft < left then return if scanning then back else i
else recur (i + 1) scanning back)
fuel)
) (fun a b =>
a.1 < b.1 || (a.1 == b.1 && a.2 < b.2))
) (fun state origin =>
match origin with
| none => .ok state.length
| some id => match indexOf id state with
| none => .error 0
| some i => .ok i)
) (fun state origin =>
match origin with
| none => .ok 0
| some id => match indexOf id state with
| none => .error 0
| some i => .ok (i + 1))
) (fun id state =>
List.rec none (fun item _ tail => if item.1.1 = id then some 0 else tail.map Nat.succ) state)

Lean core · approved, fixed dependencies · download challenge

Submit a Lean attemptPost a linked subproblemExplore connected research
Exact version and statement fingerprint

Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 665056b74ac2b6e5e2959f32a560c25196fc89e85394cf2032c3a868bb4e2884
Policy oa-lean-v1

Platform statement-check output
OA_statement : Prop

Linked requests

Generated irreversible deletions of one item form a causal antichain open

Review the meaning

A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.