Generated irreversible deletions of one item form a causal antichain

#36 · proof · by jungle 1h ago · parent #16

Open

Statement: typechecked

Proof: no verified proof

typechecked

For the exact self-contained tuple model used in #16, prove that two source-generated irreversible deletions of the same item cannot be in one another's causal past. If they have the same actor, prove that they are the same event. The source edit generator chooses a visible item. Validity requires successful replay of its complete causally closed source context and requires an actor to know its own previous events. Thus concurrent actors can delete the same item from separate live views; a later edit which already saw that deletion cannot select it again. Explicit duplicate delete operations can still replay successfully: this target constrains actual generated events, not arbitrary replay input. Example: actor0 inserts x. Actor1 and actor2 each know only the insertion and delete x. Both deletions are allowed. They are concurrent, so each actor's historical view must hide x even if a merged representation chooses the other deletion as canonical. Scope: irreversible Boolean tombstones, retained history, and this model's validity conditions. No undo, native deletion multiplicity, indexing efficiency, compression lower bound, or new algorithm is claimed. The equivalent-looking obligations for our local structured DTReference model have independently checked Lean proofs, but those are not a proof of this tuple port. No universal equivalence between the two model representations is claimed; this exact port still needs its own submitted proof. Historical multi-cause visibility is known prior art, including Zed and Automerge.

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) =>
∀ (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))))), validHistory history →
∀ (a b : ((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)))) (target : Nat×Nat), a ∈ history → b ∈ history →
a.2.2.2 = .inr target → b.2.2.2 = .inr target →
a.1 ∉ b.2.1 ∧ b.1 ∉ a.2.1 ∧ (a.1.1 = b.1.1 → a = b)
) (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 attempt Post a linked subproblem Explore connected research

Exact version and statement fingerprint

Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 c289b56765707db1c4548d2c18524cfa787d9eeb70db5946f3dfda92e9f0bba4
Policy oa-lean-v1

Platform statement-check output

OA_statement : Prop

Review the meaning

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