1606776394
## Formal Verification - Add TLA+ specs for UTXO conservation (formal/tla/UTXOConservation.tla) - Add TLA+ specs for GHOSTDAG ordering (formal/tla/GHOSTDAGOrdering.tla) - Add mathematical proof of DAA convergence (formal/proofs/) - Document Kani verification approach (formal/kani/) ## Bug Bounty Program - Add SECURITY.md with vulnerability disclosure process - Add docs/BUG_BOUNTY.md with $500-$100,000 reward tiers - Define scope, rules, and response SLA ## Web Wallet Dilithium3 WASM Integration - Build WASM module via Docker (498KB optimized) - Add wasm-crypto.ts lazy loader for Dilithium3 - Add createHybridSignatureLocal() for full client-side signing - Add createHybridSignatureSmart() for auto-mode selection - Add Dockerfile.wasm and build scripts ## Security Review ($0 Approach) - Add .github/workflows/security.yml CI workflow - Add deny.toml for cargo-deny license/security checks - Add Dockerfile.security for audit container - Add scripts/security-audit.sh for local audits - Configure cargo-audit, cargo-deny, cargo-geiger, gitleaks
123 lines
4.6 KiB
Text
123 lines
4.6 KiB
Text
-------------------------------- 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
|
|
|
|
================================================================================
|