From ef34367194e7fd18940d0b52ee7ed36cbb155dfa Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 9 Nov 2026 07:05:07 -0800 Subject: [PATCH] Expand ENABLED when applying EnabledGossip The draft soundness fix (https://github.com/tlaplus/tlapm/pull/314) exposes a completeness gap: coalescing assigns different opaque identifiers to the lemma's n,o and the goal's u,v. Expand ENABLED and the relevant definitions so ordinary first-order instantiation can discharge the step. The proof statement and assumptions remain unchanged. Unfolding definitions and expanding ENABLED preserve the TLA+ meaning of the obligation. Related: https://github.com/tlaplus/tlapm/issues/309 https://github.com/tlaplus/tlapm/pull/314 Co-authored-by: GPT-6.1 Sol Ultra Signed-off-by: Markus Alexander Kuppe --- specifications/FiniteMonotonic/CRDT_proof.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specifications/FiniteMonotonic/CRDT_proof.tla b/specifications/FiniteMonotonic/CRDT_proof.tla index 6961f8d0..246420ab 100644 --- a/specifications/FiniteMonotonic/CRDT_proof.tla +++ b/specifications/FiniteMonotonic/CRDT_proof.tla @@ -305,7 +305,7 @@ THEOREM OGLiveness == OGSpec => <>(\A n, o \in Node : counter[n] = counter[o]) => <> \E k \in 0 .. (m-1) : P(k) OBVIOUS <5>1. TypeOK /\ C(u,v) => ENABLED <>_vars - BY EnabledGossip + BY EnabledGossip, ExpandENABLED DEF Gossip, vars, C <5>2. /\ TypeOK /\ TypeOK' /\ Safety /\ Safety' /\ \E k \in 0 .. m : P(k) /\ <>_vars