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

[mohammad jalali <jalaliofficial@xxxxxxxxx>]

-------------------------------- 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.                                    *)
  (*************************************************************************)

On Saturday, January 8, 2022 at 9:23:44 PM UTC+3:30 hwa...@xxxxxxxxx wrote:

What have you tried?

On 1/8/2022 6:05 AM, mohammad jalali wrote:

Please send me the algorithm code

--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/82dcf6fd-d6bf-473f-89de-06aea1156831n%40googlegroups.com.

-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/47c862f6-da8e-41bd-b909-933f5dffd3ebn%40googlegroups.com.