Blocks

record Block : Type where
  constructor ⟨_,_,_⟩
  field parentHash : Hash
        epoch      : Epoch
        payload    : List Transaction

Signed Blocks

These blocks are the ones that are transmitted in messages.

record SignedBlock : Type where
  constructor _signed-by_
  field block     : Block
        node      : Pid

  --We assume the signature is correct.
  --Otherwise we have to add a property that signatures are valid
  -- or at least that they are determined by the block and pid,
  -- in order to be able to say that it is enough to compare node and block.
  signature : Signature
  signature = sign (node ∙sk) block

signBlock : Pid → Block → SignedBlock
signBlock pid b = b signed-by pid