-------------------------------- MODULE UTXOConservation --------------------------------
\* TLA+ Specification for Synor UTXO Conservation Invariant
\*
\* This specification formally verifies that the total value of all UTXOs
\* is conserved across all valid state transitions, ensuring no money is
\* created or destroyed outside of coinbase rewards.
\*
\* Author: Synor Team
\* Date: January 2026

EXTENDS Integers, Sequences, FiniteSets, TLC

CONSTANTS
    MAX_SUPPLY,         \* Maximum total supply (21M * 10^8 sompi)
    COINBASE_REWARD,    \* Block reward amount
    MAX_TX_INPUTS,      \* Maximum inputs per transaction
    MAX_TX_OUTPUTS,     \* Maximum outputs per transaction
    NULL_HASH           \* Represents zero hash for coinbase

VARIABLES
    utxo_set,           \* Set of all unspent transaction outputs
    total_minted,       \* Total amount minted (coinbase rewards)
    block_height        \* Current block height

\* Type invariant: All UTXOs are valid records
TypeOK ==
    /\ utxo_set \subseteq [outpoint: Nat \X Nat, amount: 0..MAX_SUPPLY, is_coinbase: BOOLEAN]
    /\ total_minted \in 0..MAX_SUPPLY
    /\ block_height \in Nat

\* Helper: Sum of all UTXO amounts
TotalUTXOValue ==
    LET amounts == {u.amount : u \in utxo_set}
    IN IF amounts = {} THEN 0 ELSE SumSet(amounts)

\* CRITICAL INVARIANT: Total UTXO value equals total minted
\* This ensures no value is created or destroyed
ConservationInvariant ==
    TotalUTXOValue = total_minted

\* Initial state: Genesis with no UTXOs
Init ==
    /\ utxo_set = {}
    /\ total_minted = 0
    /\ block_height = 0

\* Add coinbase transaction (only way to create new coins)
MintCoinbase(reward, outpoint) ==
    /\ reward <= COINBASE_REWARD
    /\ total_minted + reward <= MAX_SUPPLY
    /\ utxo_set' = utxo_set \cup {[outpoint |-> outpoint, amount |-> reward, is_coinbase |-> TRUE]}
    /\ total_minted' = total_minted + reward
    /\ block_height' = block_height + 1

\* Process a regular transaction
\* Inputs must exist in UTXO set, outputs created, conservation maintained
ProcessTransaction(inputs, outputs) ==
    /\ Cardinality(inputs) <= MAX_TX_INPUTS
    /\ Cardinality(outputs) <= MAX_TX_OUTPUTS
    /\ \A i \in inputs : i \in {u.outpoint : u \in utxo_set}
    /\ LET input_utxos == {u \in utxo_set : u.outpoint \in inputs}
           input_sum == SumSet({u.amount : u \in input_utxos})
           output_sum == SumSet({o.amount : o \in outputs})
       IN /\ output_sum <= input_sum  \* Outputs cannot exceed inputs (fee is difference)
          /\ utxo_set' = (utxo_set \ input_utxos) \cup
                         {[outpoint |-> o.outpoint, amount |-> o.amount, is_coinbase |-> FALSE] : o \in outputs}
          /\ total_minted' = total_minted - (input_sum - output_sum)  \* Fee is "destroyed"
          /\ UNCHANGED block_height

\* Alternative model: Fee goes to miner (more accurate)
ProcessTransactionWithFee(inputs, outputs, miner_outpoint) ==
    /\ Cardinality(inputs) <= MAX_TX_INPUTS
    /\ Cardinality(outputs) <= MAX_TX_OUTPUTS
    /\ \A i \in inputs : i \in {u.outpoint : u \in utxo_set}
    /\ LET input_utxos == {u \in utxo_set : u.outpoint \in inputs}
           input_sum == SumSet({u.amount : u \in input_utxos})
           output_sum == SumSet({o.amount : o \in outputs})
           fee == input_sum - output_sum
       IN /\ output_sum <= input_sum
          /\ utxo_set' = (utxo_set \ input_utxos) \cup
                         {[outpoint |-> o.outpoint, amount |-> o.amount, is_coinbase |-> FALSE] : o \in outputs} \cup
                         {[outpoint |-> miner_outpoint, amount |-> fee, is_coinbase |-> FALSE]}
          /\ UNCHANGED <<total_minted, block_height>>

\* Next state relation
Next ==
    \/ \E reward \in 1..COINBASE_REWARD, op \in Nat \X Nat :
         MintCoinbase(reward, op)
    \/ \E inputs \in SUBSET (Nat \X Nat), outputs \in SUBSET [outpoint: Nat \X Nat, amount: Nat] :
         ProcessTransaction(inputs, outputs)

\* Liveness: Eventually blocks are produced
Liveness ==
    <>[](block_height > block_height)

\* Safety: Conservation always holds
Safety == []ConservationInvariant

\* Full specification
Spec == Init /\ [][Next]_<<utxo_set, total_minted, block_height>> /\ Liveness

\* Theorems to verify
THEOREM Spec => Safety
THEOREM Spec => []TypeOK

\* Additional properties

\* No double-spend: Each UTXO can only be spent once
NoDoubleSpend ==
    \A u1, u2 \in utxo_set : u1.outpoint = u2.outpoint => u1 = u2

\* Total supply never exceeds maximum
SupplyBounded ==
    total_minted <= MAX_SUPPLY

\* All invariants
AllInvariants ==
    /\ TypeOK
    /\ ConservationInvariant
    /\ NoDoubleSpend
    /\ SupplyBounded

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