{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"c289b56765707db1c4548d2c18524cfa787d9eeb70db5946f3dfda92e9f0bba4","problem":{"id":36,"title":"Generated irreversible deletions of one item form a causal antichain","description":"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.\n\nThe 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.\n\nExample: 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.\n\nScope: 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.","statement":"(fun (indexOf : (Nat×Nat)→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option Nat) =>\n(fun (leftAfter : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>\n(fun (rightBefore : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>\n(fun (idBefore : (Nat×Nat)→(Nat×Nat)→Bool) =>\n(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) =>\n(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))) =>\n(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))) =>\n(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))) =>\n(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))) =>\n(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))) =>\n(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))) =>\n(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)) =>\n(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) =>\n(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) =>\n∀ (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 →\n∀ (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 →\na.2.2.2 = .inr target → b.2.2.2 = .inr target →\na.1 ∉ b.2.1 ∧ b.1 ∉ a.2.1 ∧ (a.1.1 = b.1.1 → a = b)\n) (fun history =>\nList.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)\n(fun event _ rest pre => validExtension pre event ∧ rest (pre ++ [event])) history [])\n) (fun pre event =>\nevent.1 ∉ ids pre ∧\n(∀ id ∈ event.2.1, id ∈ ids pre) ∧\n(∀ previous ∈ pre, previous.1 ∈ event.2.1→∀ id ∈ previous.2.1, id ∈ event.2.1) ∧\n(∀ previous ∈ pre, previous.1.1 = event.1.1→previous.1.2 < event.1.2 ∧ previous.1 ∈ event.2.1) ∧\n∃ sourceState,\nreplay (pre.filter (fun previous => event.2.1.any (fun id => id == previous.1))) = .ok sourceState ∧\ngenerate sourceState event.1 event.2.2.1 = .ok event.2.2.2)\n) (fun history => history.map (fun event => event.1))\n) (fun history =>\nreplayOps (history.map (fun event => event.2.2.2)) [])\n) (fun ops start =>\nops.foldl (fun prior op => prior.bind (fun state => apply state op)) (.ok start))\n) (fun state fresh edit =>\nmatch edit with\n| .inl (pos, label, payload) => do\nif (visible state).length < pos then throw 4\n(fun (left : Option (Nat×Nat)) => do\nlet start ← leftAfter state left\nreturn .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))\n| .inr pos => match (visible state)[pos]? with\n| none => .error 4\n| some item => .ok (.inr item.1.1))\n) (fun state => state.filter (fun item => !item.2))\n) (fun state op =>\nmatch op with\n| .inl ins => insert state ins\n| .inr target =>\nif (indexOf target state).isSome then\n.ok (state.map fun item => if item.1.1 = target then (item.1, true) else item)\nelse .error 3)\n) (fun state ins => do\nif (indexOf ins.1 state).isSome then throw 1\nlet left ← leftAfter state ins.2.2.2.1\nlet right ← rightBefore state ins.2.2.2.2\nif right < left then throw 2\nlet dest ← scan state ins left right state.length left false left\nreturn state.take dest ++ [(ins, false)] ++ state.drop dest)\n) (fun state ins left right fuel =>\nNat.rec\n(fun i scanning back =>\nif right ≤ i then .ok (if scanning then back else i) else .error 5)\n(fun _ recur i scanning back => do\nif right ≤ i then return if scanning then back else i\nlet other ← match state[i]? with\n| none => .error 4\n| some item => .ok item\nif other.1.2.2.2.1 = ins.2.2.2.1 then\nif other.1.2.2.2.2 = ins.2.2.2.2 then\nif idBefore ins.1 other.1.1 then return if scanning then back else i\nelse recur (i + 1) false back\nelse\nlet otherRight ← rightBefore state other.1.2.2.2.2\nif otherRight < right then recur (i + 1) true (if scanning then back else i)\nelse recur (i + 1) false back\nelse\nlet otherLeft ← leftAfter state other.1.2.2.2.1\nif otherLeft < left then return if scanning then back else i\nelse recur (i + 1) scanning back)\nfuel)\n) (fun a b =>\na.1 < b.1 || (a.1 == b.1 && a.2 < b.2))\n) (fun state origin =>\nmatch origin with\n| none => .ok state.length\n| some id => match indexOf id state with\n| none => .error 0\n| some i => .ok i)\n) (fun state origin =>\nmatch origin with\n| none => .ok 0\n| some id => match indexOf id state with\n| none => .error 0\n| some i => .ok (i + 1))\n) (fun id state =>\nList.rec none (fun item _ tail => if item.1.1 = id then some 0 else tail.map Nat.succ) state)","profile":"core","module_pins":[],"module_context":[],"scope":{"obligations":[],"assumptions":[],"cost_metric":"","model_scope":"","implementation":"","correspondence":"","limitations":[]}},"source":"import Init\n\ndef OA_statement : Prop := ((fun (indexOf : (Nat×Nat)→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option Nat) =>\n(fun (leftAfter : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>\n(fun (rightBefore : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>\n(fun (idBefore : (Nat×Nat)→(Nat×Nat)→Bool) =>\n(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) =>\n(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))) =>\n(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))) =>\n(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))) =>\n(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))) =>\n(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))) =>\n(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))) =>\n(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)) =>\n(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) =>\n(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) =>\n∀ (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 →\n∀ (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 →\na.2.2.2 = .inr target → b.2.2.2 = .inr target →\na.1 ∉ b.2.1 ∧ b.1 ∉ a.2.1 ∧ (a.1.1 = b.1.1 → a = b)\n) (fun history =>\nList.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)\n(fun event _ rest pre => validExtension pre event ∧ rest (pre ++ [event])) history [])\n) (fun pre event =>\nevent.1 ∉ ids pre ∧\n(∀ id ∈ event.2.1, id ∈ ids pre) ∧\n(∀ previous ∈ pre, previous.1 ∈ event.2.1→∀ id ∈ previous.2.1, id ∈ event.2.1) ∧\n(∀ previous ∈ pre, previous.1.1 = event.1.1→previous.1.2 < event.1.2 ∧ previous.1 ∈ event.2.1) ∧\n∃ sourceState,\nreplay (pre.filter (fun previous => event.2.1.any (fun id => id == previous.1))) = .ok sourceState ∧\ngenerate sourceState event.1 event.2.2.1 = .ok event.2.2.2)\n) (fun history => history.map (fun event => event.1))\n) (fun history =>\nreplayOps (history.map (fun event => event.2.2.2)) [])\n) (fun ops start =>\nops.foldl (fun prior op => prior.bind (fun state => apply state op)) (.ok start))\n) (fun state fresh edit =>\nmatch edit with\n| .inl (pos, label, payload) => do\nif (visible state).length < pos then throw 4\n(fun (left : Option (Nat×Nat)) => do\nlet start ← leftAfter state left\nreturn .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))\n| .inr pos => match (visible state)[pos]? with\n| none => .error 4\n| some item => .ok (.inr item.1.1))\n) (fun state => state.filter (fun item => !item.2))\n) (fun state op =>\nmatch op with\n| .inl ins => insert state ins\n| .inr target =>\nif (indexOf target state).isSome then\n.ok (state.map fun item => if item.1.1 = target then (item.1, true) else item)\nelse .error 3)\n) (fun state ins => do\nif (indexOf ins.1 state).isSome then throw 1\nlet left ← leftAfter state ins.2.2.2.1\nlet right ← rightBefore state ins.2.2.2.2\nif right < left then throw 2\nlet dest ← scan state ins left right state.length left false left\nreturn state.take dest ++ [(ins, false)] ++ state.drop dest)\n) (fun state ins left right fuel =>\nNat.rec\n(fun i scanning back =>\nif right ≤ i then .ok (if scanning then back else i) else .error 5)\n(fun _ recur i scanning back => do\nif right ≤ i then return if scanning then back else i\nlet other ← match state[i]? with\n| none => .error 4\n| some item => .ok item\nif other.1.2.2.2.1 = ins.2.2.2.1 then\nif other.1.2.2.2.2 = ins.2.2.2.2 then\nif idBefore ins.1 other.1.1 then return if scanning then back else i\nelse recur (i + 1) false back\nelse\nlet otherRight ← rightBefore state other.1.2.2.2.2\nif otherRight < right then recur (i + 1) true (if scanning then back else i)\nelse recur (i + 1) false back\nelse\nlet otherLeft ← leftAfter state other.1.2.2.2.1\nif otherLeft < left then return if scanning then back else i\nelse recur (i + 1) scanning back)\nfuel)\n) (fun a b =>\na.1 < b.1 || (a.1 == b.1 && a.2 < b.2))\n) (fun state origin =>\nmatch origin with\n| none => .ok state.length\n| some id => match indexOf id state with\n| none => .error 0\n| some i => .ok i)\n) (fun state origin =>\nmatch origin with\n| none => .ok 0\n| some id => match indexOf id state with\n| none => .error 0\n| some i => .ok (i + 1))\n) (fun id state =>\nList.rec none (fun item _ tail => if item.1.1 = id then some 0 else tail.map Nat.succ) state))\n\n#check OA_statement\n","proof":null}