[tlaplus] Implementing a simple 'proof of work' algorithm in tla+

• Date: Tue, 11 Jan 2022 09:53:26 -0800 (PST)
• Ironport-hdrordr: A9a23:6AXqnqzM5amjvdZW8TndKrPxY+skLtp133Aq2lEZdDV8acaYl9+jkbAyyHbP+XMssb8b6Kq90ci7MAzhHPFOkO8s1N2ZMDUOhlHYZb2KgbGSugEJ9UXFh6xgPYkJSdkwNDTbNyk3sS5jizPIUOrJ+bG8geCVbQ239QYicegSUdAg0+4bMHfmLqQVfng6OXNjLuvVl4F6TlObEBx9BKvLZQhmLo2zw6ytqHuBW29/O/cJ0njFsdrC0s+PL/Hs5GZvb9o5+8ZQzYGqqX2D2k0t3svLuCM16QXonuNrcaPau6p+7aG35/T9fQ+c9DpBb+5aKsu/VSgOzt1H8mxKrDDTmXcdFvU21HvVfmy8vBvq3E3qwF8Vmgrf4G7dhn2mqdfyRTIkB6N69M9kTic=

I wrote this code, what is wrong?

-------------------------------- MODULE POW --------------------------------

EXTENDS Integers

CONSTANT nodes
VARIABLES chain, blcks, last_block_id, status, status_changer

Block == [miner_id: nodes \union {"first"}, block_id: 0..3, prev_block_id: -1..3]

POWTypeOK ==
/\ blcks \subseteq Block
/\ chain \in [nodes -> SUBSET Block]
/\ last_block_id \in [nodes -> 0..3]
/\ status \in [nodes -> {"mined", "miner"}]
/\ status_changer \in [nodes -> {0, 1}]

----------------------------------------------------------------------------

POWInit ==
/\ blcks = {[miner_id |-> "first", block_id |-> 0, prev_block_id |-> -1]}
/\ chain = [n \in nodes |-> {[miner_id |-> "first", block_id |-> 0, prev_block_id |-> -1]}]
/\ last_block_id = [n \in nodes |-> 0]
/\ status = [ n \in nodes |-> "miner"]
/\ status_changer = [n \in nodes |-> 0]

----------------------------------------------------------------------------

MineABlock(n) ==
/\ status[n] = "miner"
/\ chain' = [chain EXCEPT ![n] = chain[n] \union {[miner_id |-> n, block_id |-> last_block_id[n] + 1,
prev_block_id |-> last_block_id[n]]}]
/\ blcks' = blcks \union {[miner_id |-> n, block_id |-> last_block_id[n] + 1, prev_block_id |-> last_block_id[n]]}
/\ last_block_id' = [last_block_id EXCEPT ![n] = last_block_id[n] + 1]
/\ status' = [status EXCEPT ![n] = "mined"]
/\ status_changer' = [status_changer EXCEPT ![n] = 1]

CommitABlock(n, r) ==
/\ status[n] = "mined"
/\ last_block_id[r] = last_block_id[n] - 1
/\ [miner_id |-> n, block_id |-> last_block_id[n], prev_block_id |-> last_block_id[n] - 1] \in blcks
/\ chain' = chain
/\ chain[r]' = chain[r] \union {[miner_id |-> n, block_id |-> last_block_id[n], prev_block_id |-> last_block_id[r]]}
/\ last_block_id' = [last_block_id EXCEPT ![r] = last_block_id[n]]
/\ status_changer' = [status_changer EXCEPT ![r] = 1]
/\ UNCHANGED <<blcks, status>>

IgnoreABlock(n, r) ==
/\ status[n] = "mined"
/\ [miner_id |-> n, block_id |-> last_block_id[n], prev_block_id |-> last_block_id[n] - 1] \in blcks
/\ status_changer' = [status_changer EXCEPT ![r] = 1]
/\ UNCHANGED <<chain, blcks, last_block_id, status>>

ChangeStatus(n) ==
/\ status_changer = [r \in nodes |-> 1]
/\ status' = [status EXCEPT ![n] = "miner"]
/\ status_changer' = [r \in nodes |-> 0]
/\ UNCHANGED <<blcks, chain, last_block_id>>

-----------------------------------------------------------------------------

POWNext == (\E n\in nodes:
\/ MineABlock(n) \/ ChangeStatus(n)
\/ (\A r \in nodes: CommitABlock(n, r) \/ IgnoreABlock(n, r)))

-----------------------------------------------------------------------------

POWSpec == POWInit /\ [][POWNext]_<<chain, blcks, last_block_id, status>>
(*************************************************************************)
(* The complete spec of the Proof-of-work Commit protocol.               *)
(*************************************************************************)

THEOREM POWSpec => []POWTypeOK
(*************************************************************************)
(* This theorem asserts that the type-correctness predicate POWTypeOK is *)
(* an invariant of the specification.                                    *)
(*************************************************************************)

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.