module Peras.Block where

PartyId

PartyId = Nat

Party

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

open Party public

instance
  iPartyEq : Eq Party
  iPartyEq ._==_ x y = pid x == pid y && pkey x == 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

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
  pattern
  field round : RoundNumber
        blockRef : Hash Block

  roundNumber : Nat
  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' : Nat
  slotNumber' = getSlotNumber slotNumber

open Block public

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

open BlockBody public

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

eqCertificate-sound : ∀ {c₁ c₂ : Certificate} → (c₁ == c₂) ≡ True → c₁ ≡ c₂
eqCertificate-sound {MkCertificate round₁ blockRef₁} {MkCertificate round₂ blockRef₂} x
  = let l = &&-leftTrue (getRoundNumber round₁ == getRoundNumber round₂) _ x
        r = &&-rightTrue _ (eqBS (hashBytes blockRef₁) (hashBytes blockRef₂)) x
    in cong₂ MkCertificate (cong MkRoundNumber (eqℕ-sound l)) (MkHash-inj (lem-eqBS r))
  where
    eqℕ-sound : {n m : Nat} → (n == m) ≡ True → n ≡ m
    eqℕ-sound {zero}  {zero}   _  = refl
    eqℕ-sound {suc n} {suc m} prf = cong suc (eqℕ-sound prf)

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 [] = MkHash emptyBS
  tipHash (x ∷ _) = hash x

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

{-# COMPILE AGDA2HS tipHash #-}
{-# COMPILE AGDA2HS iCertificateEq #-}
{-# COMPILE AGDA2HS iBlockEq #-}
{-# COMPILE AGDA2HS iBlockBodyEq #-}
{-# COMPILE AGDA2HS hashBlock #-}