-------------------------------- MODULE GHOSTDAGOrdering --------------------------------
\* TLA+ Specification for GHOSTDAG Ordering Determinism
\*
\* This specification formally verifies that the GHOSTDAG algorithm produces
\* a deterministic total ordering of blocks given the same DAG structure,
\* regardless of the order in which blocks are received.
\*
\* Key Property: Two honest nodes with the same DAG view will compute
\* the same blue set, selected parent chain, and block ordering.
\*
\* Author: Synor Team
\* Date: January 2026

EXTENDS Integers, Sequences, FiniteSets, TLC

CONSTANTS
    K,              \* K parameter (anticone size bound for blue blocks)
    MAX_BLOCKS,     \* Maximum blocks in simulation
    GENESIS         \* Genesis block hash

VARIABLES
    dag,            \* DAG structure: block -> {parent blocks}
    blue_set,       \* Set of blue blocks
    blue_score,     \* Mapping: block -> blue score
    selected_parent,\* Mapping: block -> selected parent
    chain           \* Selected parent chain (sequence)

\* Type invariant
TypeOK ==
    /\ dag \in [SUBSET Nat -> SUBSET Nat]
    /\ blue_set \subseteq DOMAIN dag
    /\ blue_score \in [DOMAIN dag -> Nat]
    /\ selected_parent \in [DOMAIN dag \ {GENESIS} -> DOMAIN dag]
    /\ chain \in Seq(DOMAIN dag)

\* Helper: Get all ancestors of a block
RECURSIVE Ancestors(_, _)
Ancestors(block, d) ==
    IF block = GENESIS THEN {GENESIS}
    ELSE LET parents == d[block]
         IN parents \cup UNION {Ancestors(p, d) : p \in parents}

\* Helper: Get past (ancestors including self)
Past(block, d) == {block} \cup Ancestors(block, d)

\* Helper: Get anticone of block B relative to block A
\* Anticone(A, B) = blocks in Past(B) that are not in Past(A) and A is not in their past
Anticone(blockA, blockB, d) ==
    LET pastA == Past(blockA, d)
        pastB == Past(blockB, d)
    IN {b \in pastB : b \notin pastA /\ blockA \notin Past(b, d)}

\* GHOSTDAG: Compute blue set for a new block
\* A block is blue if its anticone (relative to virtual) contains at most K blue blocks
ComputeBlueSet(new_block, d, current_blue) ==
    LET anticone == Anticone(new_block, new_block, d) \cap current_blue
    IN IF Cardinality(anticone) <= K
       THEN current_blue \cup {new_block}
       ELSE current_blue

\* Compute blue score (number of blue blocks in past)
ComputeBlueScore(block, d, bs) ==
    Cardinality(Past(block, d) \cap bs)

\* Select parent with highest blue score
SelectParent(block, d, scores) ==
    LET parents == d[block]
    IN CHOOSE p \in parents : \A q \in parents : scores[p] >= scores[q]

\* CRITICAL INVARIANT: Ordering is deterministic
\* Given the same DAG, all nodes compute the same ordering
OrderingDeterminism ==
    \* For any two blocks A and B, their relative order is determined solely by:
    \* 1. Blue scores (higher = earlier in virtual order)
    \* 2. If tied, by hash (deterministic tiebreaker)
    \A a, b \in DOMAIN dag :
        a # b =>
            (blue_score[a] > blue_score[b] => \* a comes before b in ordering
                \A i, j \in 1..Len(chain) :
                    chain[i] = a /\ chain[j] = b => i < j)

\* Initial state: Only genesis block
Init ==
    /\ dag = [b \in {GENESIS} |-> {}]
    /\ blue_set = {GENESIS}
    /\ blue_score = [b \in {GENESIS} |-> 0]
    /\ selected_parent = [b \in {} |-> GENESIS]  \* Empty function
    /\ chain = <<GENESIS>>

\* Add a new block to the DAG
AddBlock(new_block, parents) ==
    /\ new_block \notin DOMAIN dag
    /\ parents \subseteq DOMAIN dag
    /\ parents # {}
    /\ LET new_dag == [b \in DOMAIN dag \cup {new_block} |->
                         IF b = new_block THEN parents ELSE dag[b]]
           new_blue == ComputeBlueSet(new_block, new_dag, blue_set)
           new_scores == [b \in DOMAIN new_dag |->
                           ComputeBlueScore(b, new_dag, new_blue)]
           new_sel_parent == SelectParent(new_block, new_dag, new_scores)
       IN /\ dag' = new_dag
          /\ blue_set' = new_blue
          /\ blue_score' = new_scores
          /\ selected_parent' = [b \in DOMAIN selected_parent \cup {new_block} |->
                                   IF b = new_block THEN new_sel_parent
                                   ELSE selected_parent[b]]
          /\ chain' = \* Rebuild chain to tip
                      LET RECURSIVE BuildChain(_, _)
                          BuildChain(blk, acc) ==
                              IF blk = GENESIS THEN Append(acc, GENESIS)
                              ELSE BuildChain(selected_parent'[blk], Append(acc, blk))
                      IN BuildChain(new_block, <<>>)

\* Next state relation
Next ==
    \E new_block \in Nat, parents \in SUBSET (DOMAIN dag) :
        /\ Cardinality(DOMAIN dag) < MAX_BLOCKS
        /\ AddBlock(new_block, parents)

\* Specification
Spec == Init /\ [][Next]_<<dag, blue_set, blue_score, selected_parent, chain>>

\* Safety properties

\* Blue set is monotonic (blocks stay blue once blue)
BlueMonotonic ==
    [][blue_set \subseteq blue_set']_blue_set

\* Chain extends (never shrinks except on reorg)
ChainGrows ==
    [][Len(chain') >= Len(chain) \/ \E i \in 1..Len(chain) : chain[i] # chain'[i]]_chain

\* Selected parent chain is connected
ChainConnected ==
    \A i \in 1..(Len(chain)-1) :
        chain[i] \in dag[chain[i+1]]

\* All properties
AllInvariants ==
    /\ TypeOK
    /\ OrderingDeterminism
    /\ ChainConnected

THEOREM Spec => []AllInvariants

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