ReputationSystem.tla

---- MODULE ReputationSystem ----
\* ReputationSystem - TLA+ Formal Specification
\* Models reputation-weighted leader selection and voting
\* 
\* Verified Properties:
\* - MonotonicReputation: Scores never decrease improperly
\* - WeightedVoting: Vote power = reputation^2
\* - LeaderSelection: Highest-reputation node selected
\* - SlashingBounded: Penalties proportional and capped

EXTENDS Integers, Sequences, TLC, FiniteSets, Reals

CONSTANTS
    Nodes,              \* Set of validator node IDs
    InitialRep,         \* Starting reputation (e.g., 50)
    MaxSlashPenalty,    \* Maximum reputation loss from slashing (e.g., 10)
    MaxReputation       \* Cap on reputation (e.g., 100)

VARIABLES
    reputation,         \* Node -> Reputation score (0-100)
    votes,              \* Proposal -> (Node -> Vote)
    currentLeader,      \* Current epoch leader
    slashEvents,        \* Set of slashing records
    pohSequence         \* PoH timestamp counter

vars == <<reputation, votes, currentLeader, slashEvents, pohSequence>>

\* Vote choices
FOR == "FOR"
AGAINST == "AGAINST"
ABSTAIN == "ABSTAIN"

\* Slashing reasons
SLASH_MISSED_BLOCK == "MISSED_BLOCK"
SLASH_DOUBLE_SIGN == "DOUBLE_SIGN"
SLASH_INVALID_TX == "INVALID_TX"

----

\* Initial state
Init ==
    /\ reputation = [n \in Nodes |-> InitialRep]
    /\ votes = <<>>
    /\ currentLeader = CHOOSE n \in Nodes: TRUE  \* Arbitrary initial leader
    /\ slashEvents = {}
    /\ pohSequence = 0

----

\* UpdateReputation: Adjust node reputation score
UpdateReputation(nodeId, delta) ==
    /\ nodeId \in Nodes
    /\ LET newRep == reputation[nodeId] + delta
           clampedRep == IF newRep < 0 THEN 0
                         ELSE IF newRep > MaxReputation THEN MaxReputation
                         ELSE newRep
       IN
        /\ reputation' = [reputation EXCEPT ![nodeId] = clampedRep]
        /\ pohSequence' = pohSequence + 1
        /\ UNCHANGED <<votes, currentLeader, slashEvents>>

\* CastVote: Node casts weighted vote on proposal
CastVote(nodeId, proposalId, choice) ==
    /\ nodeId \in Nodes
    /\ choice \in {FOR, AGAINST, ABSTAIN}
    /\ reputation[nodeId] > 0  \* Only nodes with rep can vote
    /\ LET vote == [
                node |-> nodeId,
                proposal |-> proposalId,
                choice |-> choice,
                votePower |-> reputation[nodeId] * reputation[nodeId],  \* rep^2
                pohSeq |-> pohSequence
            ]
       IN
        /\ votes' = Append(votes, vote)
        /\ pohSequence' = pohSequence + 1
        /\ UNCHANGED <<reputation, currentLeader, slashEvents>>

\* SelectLeader: Choose leader for next epoch (highest reputation)
SelectLeader ==
    /\ LET eligibleNodes == {n \in Nodes: reputation[n] > 0}
           maxRep == CHOOSE r \in {reputation[n]: n \in eligibleNodes}:
                        \A n \in eligibleNodes: reputation[n] <= r
           leader == CHOOSE n \in eligibleNodes: reputation[n] = maxRep
       IN
        /\ currentLeader' = leader
        /\ pohSequence' = pohSequence + 1
        /\ UNCHANGED <<reputation, votes, slashEvents>>

\* SlashNode: Penalize node for misbehavior
SlashNode(nodeId, reason) ==
    /\ nodeId \in Nodes
    /\ reason \in {SLASH_MISSED_BLOCK, SLASH_DOUBLE_SIGN, SLASH_INVALID_TX}
    /\ LET penalty == CASE reason = SLASH_MISSED_BLOCK -> 1
                        [] reason = SLASH_DOUBLE_SIGN -> 5
                        [] reason = SLASH_INVALID_TX -> 3
           cappedPenalty == IF penalty > MaxSlashPenalty THEN MaxSlashPenalty ELSE penalty
           newRep == IF reputation[nodeId] - cappedPenalty < 0 THEN 0
                     ELSE reputation[nodeId] - cappedPenalty
           slashEvent == [
                node |-> nodeId,
                reason |-> reason,
                penalty |-> cappedPenalty,
                pohSeq |-> pohSequence
            ]
       IN
        /\ reputation' = [reputation EXCEPT ![nodeId] = newRep]
        /\ slashEvents' = slashEvents \cup {slashEvent}
        /\ pohSequence' = pohSequence + 1
        /\ UNCHANGED <<votes, currentLeader>>

\* RewardBlock: Reward node for producing block
RewardBlock(nodeId) ==
    /\ nodeId \in Nodes
    /\ UpdateReputation(nodeId, 1)  \* +1 reputation per block

----

\* Next state: All possible actions
Next ==
    \/ \E n \in Nodes, d \in -MaxSlashPenalty..5: UpdateReputation(n, d)
    \/ \E n \in Nodes, p \in {"prop1", "prop2"}, c \in {FOR, AGAINST, ABSTAIN}:
        CastVote(n, p, c)
    \/ SelectLeader
    \/ \E n \in Nodes, r \in {SLASH_MISSED_BLOCK, SLASH_DOUBLE_SIGN, SLASH_INVALID_TX}:
        SlashNode(n, r)
    \/ \E n \in Nodes: RewardBlock(n)

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

----

\* SAFETY PROPERTIES (Invariants)

TypeInvariant ==
    /\ \A n \in Nodes: reputation[n] >= 0
    /\ \A n \in Nodes: reputation[n] <= MaxReputation
    /\ currentLeader \in Nodes
    /\ pohSequence \in Nat

\* Property 1: Monotonic Reputation
\* Reputation never goes negative
MonotonicReputation ==
    \A n \in Nodes: reputation[n] >= 0

\* Property 2: Weighted Voting
\* Vote power equals reputation squared
WeightedVoting ==
    \A v \in DOMAIN votes:
        LET vote == votes[v]
        IN vote.votePower = vote.node \in Nodes =>
            reputation[vote.node] * reputation[vote.node]

\* Property 3: Leader Selection
\* Leader has highest reputation among active nodes
LeaderSelection ==
    LET eligibleNodes == {n \in Nodes: reputation[n] > 0}
    IN eligibleNodes # {} => 
        \A n \in eligibleNodes: reputation[currentLeader] >= reputation[n]

\* Property 4: Slashing Bounded
\* Penalties never exceed MaxSlashPenalty
SlashingBounded ==
    \A s \in slashEvents: s.penalty <= MaxSlashPenalty

\* Property 5: Reputation Cap
\* No node exceeds MaxReputation
ReputationCap ==
    \A n \in Nodes: reputation[n] <= MaxReputation

\* Property 6: Active Leader
\* Leader always has positive reputation
ActiveLeader ==
    reputation[currentLeader] > 0

====