proofs/tla/DAGEVM.tla

---------------------------- MODULE DAGEVM ----------------------------
(*
 * TLA+ Specification of DAG-EVM Consensus
 *
 * Source: lux/evmgpu/dag/vertex.go         (EVMVertex)
 *         lux/evmgpu/dag/conflicts.go      (Conflicts predicate)
 *         lux/evmgpu/dag/executor.go       (topo-order applicator)
 *         lux/evm/core/parallel/blockstm.go (read/write-set tracking)
 *         lux/consensus/engine/dag/        (nebula finality)
 *         lux/consensus/protocol/horizon/  (antichain predicates)
 *
 * Protocol summary:
 *   DAG-EVM lifts Block-STM (Gelashvili et al., 2022) from a
 *   per-block scheduling discipline to full consensus-level ordering.
 *
 *   Each vertex batches a set of EVM transactions whose read/write sets
 *   have been pre-computed by speculative parallel execution. Vertices
 *   reference parents in the DAG, and the nebula finality mode finalises
 *   antichain cuts via quasar certificates.
 *
 *   The conflict rule is:
 *     conflicts(v1, v2) ==
 *         (v1.reads \cap v2.writes) # {} \/
 *         (v1.writes \cap v2.reads) # {} \/
 *         (v1.writes \cap v2.writes) # {}
 *
 *   BuildVertex guarantees that any two vertices emitted into the same
 *   antichain are pairwise non-conflicting. Conflicts flow along DAG
 *   edges (ancestor/descendant), never between siblings.
 *
 * Key properties (checked with TLC):
 *   Safety    : No two conflicting vertices are both accepted in the
 *               same antichain rank.
 *   Serializ. : Every reachable accepted set has a linear extension
 *               that produces the same final state as the DAG
 *               topological order.
 *   NoDblSpend: No storage key is written by two finalised antichain
 *               siblings.
 *   Liveness  : If a non-empty mempool exists, eventually a vertex is
 *               proposed and finalised.
 *
 * Go-to-TLA+ mapping:
 *   Vertex                       -> vertex records in `accepted`
 *   BuildVertex                  -> Propose action
 *   Conflicts                    -> Conflicts operator
 *   horizon.ComputeFrontier      -> Antichain operator
 *   nebula.Finalize              -> Finalize action
 *   quasar cert                  -> finality flag in Finalize
 *)

EXTENDS Integers, FiniteSets, Sequences, TLC

\* --------------------------------------------------------------------------
\* CONSTANTS
\* --------------------------------------------------------------------------

CONSTANTS
    Keys,           \* Set of storage keys (StorageKey = uint256 keccak slot)
    MaxVertices,    \* Bound on DAG size for model checking
    MaxTxsPerVertex \* Bound on batch size

ASSUME Cardinality(Keys) > 0
ASSUME MaxVertices \in Nat \ {0}
ASSUME MaxTxsPerVertex \in Nat \ {0}

\* --------------------------------------------------------------------------
\* TYPES
\* --------------------------------------------------------------------------

\* A vertex record:
\*   id      \in Nat                     unique identifier
\*   reads   \subseteq Keys              read set
\*   writes  \subseteq Keys              write set
\*   parents \subseteq {vertex ids}      DAG parents
\*   rank    \in Nat                     topological rank

VertexId == 1..MaxVertices

\* Ranks are layered as 1 + maxParentRank starting at 1, and a chain of
\* accepted vertices is bounded by MaxVertices, so every reachable rank lies
\* in 1..MaxVertices. Bounding the field here keeps Vertex a FINITE set; with
\* `rank : Nat` it was infinite and TLC could not enumerate `\E v \in Vertex`
\* in the Next relation ("can't enumerate the value of the rank field: Nat").
RankRange == 1..MaxVertices

Vertex ==
  [ id      : VertexId,
    reads   : SUBSET Keys,
    writes  : SUBSET Keys,
    parents : SUBSET VertexId,
    rank    : RankRange ]

\* --------------------------------------------------------------------------
\* VARIABLES
\* --------------------------------------------------------------------------

VARIABLES
    accepted,      \* Set of accepted vertex records (persistent)
    finalRank,     \* Highest rank for which the antichain is quasar-final
    mempool        \* Set of pending (reads, writes) tx batches awaiting propose

vars == <<accepted, finalRank, mempool>>

\* --------------------------------------------------------------------------
\* HELPERS
\* --------------------------------------------------------------------------

Conflicts(v1, v2) ==
    (v1.reads  \cap v2.writes) # {} \/
    (v1.writes \cap v2.reads)  # {} \/
    (v1.writes \cap v2.writes) # {}

\* The set of accepted vertices at a given rank.
Antichain(r) == { v \in accepted : v.rank = r }

\* The frontier: ranks whose antichains have been proposed but not yet finalised.
\* In the Go code this is horizon.ComputeFrontier().
Frontier == { v.rank : v \in accepted } \ { r \in Nat : r <= finalRank }

\* --------------------------------------------------------------------------
\* INVARIANT (structural well-formedness)
\* --------------------------------------------------------------------------

TypeOK ==
    /\ accepted \subseteq Vertex
    /\ finalRank \in Nat
    /\ mempool \subseteq ([reads: SUBSET Keys, writes: SUBSET Keys])

\* --------------------------------------------------------------------------
\* INITIAL STATE
\* --------------------------------------------------------------------------

Init ==
    /\ accepted = {}
    /\ finalRank = 0
    \* mempool is an abstract placeholder for pending tx batches; the abstracted
    \* Propose action draws arbitrary well-formed vertices directly and never
    \* reads mempool, so it stays UNCHANGED throughout. The previous
    \* `mempool \in SUBSET ([reads: SUBSET Keys, writes: SUBSET Keys])`
    \* forced TLC to enumerate 2^(2^|Keys| * 2^|Keys|) initial states (2^64 for
    \* 3 keys) before the cardinality filter could apply, stalling the checker.
    \* Initialising it to {} keeps Init tractable without weakening any property
    \* (no action depends on mempool's contents).
    /\ mempool = {}

\* --------------------------------------------------------------------------
\* ACTIONS
\* --------------------------------------------------------------------------

\* Propose a new vertex from the mempool.
\* Invariant enforced by BuildVertex: the new vertex does not conflict with
\* any other accepted vertex at the same rank.
Propose(newV) ==
    /\ newV \in Vertex
    /\ newV.id \notin { v.id : v \in accepted }
    /\ Cardinality(accepted) < MaxVertices
    \* Parents must already be accepted (DAG closure).
    /\ \A p \in newV.parents : \E v \in accepted : v.id = p
    \* Rank is one more than the max parent rank (Kahn layering).
    /\ newV.rank =
         IF newV.parents = {} THEN 1
         ELSE 1 + CHOOSE maxR \in { v.rank : v \in {x \in accepted : x.id \in newV.parents} } :
                      \A v \in accepted :
                        v.id \in newV.parents => v.rank <= maxR
    \* CRITICAL: no conflict with accepted siblings at the same rank.
    /\ \A v \in accepted : v.rank = newV.rank => ~Conflicts(v, newV)
    /\ accepted' = accepted \cup {newV}
    /\ UNCHANGED <<finalRank, mempool>>

\* Finalize the lowest unfinalised rank (nebula + quasar).
Finalize ==
    /\ finalRank + 1 \in { v.rank : v \in accepted }
    \* All sibling vertices at this rank are accepted (antichain complete).
    /\ \A v \in Antichain(finalRank + 1) :
         \A w \in Antichain(finalRank + 1) : v # w => ~Conflicts(v, w)
    /\ finalRank' = finalRank + 1
    /\ UNCHANGED <<accepted, mempool>>

Next ==
    \/ \E v \in Vertex : Propose(v)
    \/ Finalize

Spec == Init /\ [][Next]_vars /\ WF_vars(Finalize)

\* --------------------------------------------------------------------------
\* PROPERTIES
\* --------------------------------------------------------------------------

\* Safety: no two vertices in the same antichain conflict.
Safety ==
    \A v1, v2 \in accepted :
        (v1.id # v2.id /\ v1.rank = v2.rank) => ~Conflicts(v1, v2)

\* No double spend: at most one finalised vertex writes each key per rank.
NoDoubleSpend ==
    \A r \in 1..finalRank :
        \A k \in Keys :
            Cardinality({ v \in Antichain(r) : k \in v.writes }) <= 1

\* Serializability witness: a topological order of accepted vertices that
\* respects parent -> child precedence always exists (implicit in DAG
\* acyclicity + rank layering).
Serializability ==
    \A v, w \in accepted :
        w.id \in v.parents => w.rank < v.rank

\* Liveness: every accepted vertex is eventually finalised, assuming its
\* antichain stops accepting new siblings.
\*
\* We quantify over the FINITE set of possible ranks (1..MaxVertices) rather
\* than over the type Vertex. Vertex has a `rank : Nat` field, so it is an
\* infinite set; TLC cannot enumerate `\A v \in Vertex` inside a temporal
\* (~>) formula ("can't enumerate the value of the rank field: Nat"). Ranks
\* are layered 1 + maxParentRank and bounded by the vertex count, so every
\* rank that can ever appear lies in 1..MaxVertices. "Every accepted vertex's
\* rank is eventually finalised" is exactly "every populated rank is
\* eventually <= finalRank", which is finite and TLC-checkable.
Liveness ==
    \A r \in 1..MaxVertices :
        (\E v \in accepted : v.rank = r) ~> (finalRank >= r)

\* Conflict-flow-along-edges invariant (the BuildVertex contract).
\* Only DISTINCT vertices are compared: every vertex trivially "conflicts"
\* with itself (its write set intersects itself), so without the v1.id # v2.id
\* guard the implication degenerates to TRUE => (r # r) = FALSE on the very
\* first accepted vertex. The sibling invariant Safety already guards this way.
ConflictsAlongEdges ==
    \A v1, v2 \in accepted :
        (v1.id # v2.id /\ Conflicts(v1, v2)) => v1.rank # v2.rank

================================================================================