Created
January 13, 2024 23:14
-
-
Save erangaeb/fca2db617e0863ca4f2cf95cfa243247 to your computer and use it in GitHub Desktop.
tla+
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
--------------------------- MODULE BlockchainTransactions --------------------------- | |
EXTENDS Integers, Sequences, TLC | |
(*-- Constants used in the specification --*) | |
CONSTANT Clients, KafkaNodes, SmartContracts, StorageNodes, CacheNodes, LokkaServices | |
(*-- The set of all possible transactions --*) | |
VARIABLE transactions, messageBroker, blockchainStorage, distributedCache, blocks | |
(* -- Define the initial state of the blockchain system --*) | |
Init == | |
/\ transactions = << >> \* Initially, no transactions are submitted | |
/\ messageBroker = << >> \* Kafka starts with no messages | |
/\ blockchainStorage = << >> \* No transactions executed and stored yet | |
/\ distributedCache = {} \* Cache starts empty | |
/\ blocks = << >> \* No blocks created yet | |
(*-- Clients submit transactions to the API --*) | |
SubmitTransaction(t) == | |
/\ t \notin transactions | |
/\ transactions' = Append(transactions, t) | |
/\ UNCHANGED <<messageBroker, blockchainStorage, distributedCache, blocks>> | |
(*-- API publishes transactions to Kafka --*) | |
PublishToKafka == | |
/\ transactions /= << >> | |
/\ messageBroker' = transactions \* Kafka orders the transactions | |
/\ transactions' = << >> | |
/\ UNCHANGED <<blockchainStorage, distributedCache, blocks>> | |
(*-- Smart contracts stream and execute transactions --*) | |
ExecuteTransactions == | |
/\ messageBroker /= << >> | |
/\ LET t == Head(messageBroker) | |
sc == CHOOSE s \in SmartContracts: TRUE \* Choose any smart contract node | |
IN | |
/\ ~IsDoubleSpend(t) | |
/\ blockchainStorage' = Append(blockchainStorage, t) | |
/\ messageBroker' = Tail(messageBroker) | |
/\ distributedCache' = distributedCache \union {t} | |
/\ UNCHANGED blocks | |
(*-- Check if a transaction is a double spend --*) | |
IsDoubleSpend(t) == | |
t \in distributedCache | |
(*-- Cassandra replicates state updates to other blockchain nodes --*) | |
ReplicateState == | |
/\ blockchainStorage /= << >> | |
/\ LET t == Head(blockchainStorage) | |
sn == CHOOSE s \in StorageNodes: TRUE \* Choose any storage node | |
IN | |
/\ blockchainStorage' = Tail(blockchainStorage) \* State update replicated | |
/\ UNCHANGED <<transactions, messageBroker, distributedCache, blocks>> | |
(*-- Lokka service creates blocks with transaction IDs in the cache --*) | |
CreateBlocks == | |
/\ distributedCache /= {} | |
/\ LET t == CHOOSE x \in distributedCache: TRUE \* Choose any transaction in cache | |
ls == CHOOSE l \in LokkaServices: TRUE \* Choose any Lokka service | |
IN | |
/\ blocks' = Append(blocks, t) | |
/\ distributedCache' = distributedCache \ {t} | |
/\ UNCHANGED <<transactions, messageBroker, blockchainStorage>> | |
(*-- Define the next state based on possible actions --*) | |
Next == | |
\/ \E t \in DOMAIN transactions: SubmitTransaction(t) | |
\/ PublishToKafka | |
\/ ExecuteTransactions | |
\/ ReplicateState | |
\/ CreateBlocks | |
(*-- Specify safety properties --*) | |
Consistency == \A t \in DOMAIN transactions: ~IsDoubleSpend(t) | |
(*-- Specification combines initial state and next state relation --*) | |
Spec == Init /\ [][Next]_<<transactions, messageBroker, blockchainStorage, distributedCache, blocks>> | |
(*-- What TLC should check --*) | |
INVARIANTS Consistency | |
====================================================================================== |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment