module Peras.Block where

PartyId

PartyId = ℕ  -- FIXME: Data.Fin ?

Party

record Party : Set where
  constructor MkParty
  field pid : PartyId
        pkey : VerificationKey

open Party public

instance
  iPartyEq : Eq Party
  iPartyEq .Haskell._==_ x y = pid x Haskell.== pid y && pkey x Haskell.== pkey y

Honesty of a party

data Honesty : PartyId → Set where

  Honest : ∀ {p : PartyId}
    → Honesty p

  Corrupt : ∀ {p : PartyId}
    → Honesty p

PartyTup = ∃[ p ] (Honesty p)
Parties = List PartyTup

postulate
  Honest≢Corrupt : ∀ {p₁ p₂} {h₁ : Honesty p₁} {h₂ : Honesty p₂}
    → h₁ ≡ Honest
    → h₂ ≡ Corrupt
    → p₁ ≢ p₂

isHonest : ∀ {p : PartyId} → Honesty p → Bool
isHonest {p} Honest = true
isHonest {p} Corrupt = false

Transactions

Tx = ⊤

Block and Certificate

In addition to a Praos block, there is an optional field for the included certificate. Note: What we name Block is actually a block Header, we use BlockBody to contain the payload.

A Peras Certificate represents an aggregated quorum of votes for a specific block at a specific round. Such a certificate is supposed to be self-contained and verifiable by any node.

record Block : Set
record BlockBody : Set
record Certificate : Set

Payload = List Tx

record Certificate where
  constructor MkCertificate
  field round : RoundNumber
        blockRef : Hash Block

  roundNumber : ℕ
  roundNumber = getRoundNumber round

open Certificate public

latestCert : Certificate → List Certificate → Certificate
latestCert c = maximumBy c (comparing round)

record Block where
  constructor MkBlock
  field slotNumber : SlotNumber
        creatorId : PartyId
        parentBlock : Hash Block
        certificate : Maybe Certificate
        leadershipProof : LeadershipProof
        signature : Signature
        bodyHash : Hash Payload

  slotNumber' : ℕ
  slotNumber' = getSlotNumber slotNumber

open Block public

_≟-BlockHash_ : DecidableEquality (Hash Block)
(MkHash b₁) ≟-BlockHash (MkHash b₂) with b₁ ≟-BS b₂
... | yes p = yes (cong MkHash p)
... | no ¬p =  no (¬p ∘ cong hashBytes)

record BlockBody where
  constructor MkBlockBody
  field blockHash : Hash Payload
        payload : Payload

open BlockBody public

data HonestBlock : Block → Set where

  HonestParty : ∀ {p : PartyId} {h : Honesty p} {b : Block}
    → creatorId b ≡ p
    → h ≡ Honest {p}
    → HonestBlock b

instance
  iCertificateEq : Eq Certificate
  iCertificateEq ._==_ x y = round x == round y && blockRef x == blockRef y

instance
  iBlockEq : Eq Block
  iBlockEq ._==_ x y = slotNumber x == slotNumber y
                         && creatorId x == creatorId y
                         && parentBlock x == parentBlock y
                         && leadershipProof x == leadershipProof y
                         && certificate x == certificate y
                         && signature x == signature y
                         && bodyHash x == bodyHash y
                         -- FIXME: In principle, we only need to check equality of the signatures.

instance
  iBlockBodyEq : Eq BlockBody
  iBlockBodyEq ._==_ x y = blockHash x == blockHash y && payload x == payload y

module _ {a : Set} ⦃ _ : Hashable a ⦄
  where

  open Hashable ⦃...⦄

  tipHash : List a → Hash a
  tipHash Data.List.[] = MkHash emptyBS
  tipHash (x Data.List.∷ _) = hash x

{-# COMPILE AGDA2HS tipHash #-}

private
  open Hashable

  instance
    hashBlock : Hashable Block
    hashBlock .hash = MkHash ∘ bytesS ∘ signature