module Peras.Chain where

Voting

Vote

VotingWeight = ℕ

record Vote : Set where
  constructor MkVote
  field votingRound : RoundNumber
        creatorId   : PartyId
        proofM      : MembershipProof
        blockHash   : Hash Block
        signature   : Signature

  votingRound' : ℕ
  votingRound' = getRoundNumber votingRound

open Vote public

instance
  iVoteEq : Eq Vote
  iVoteEq ._==_ x y = votingRound x == votingRound y
                        && creatorId x == creatorId y
                        && proofM x == proofM y
                        && blockHash x == blockHash y
                        && signature x == signature y

record Postulates : Set₁ where
  field
    IsSlotLeader : PartyId → SlotNumber → LeadershipProof → Set
    IsCommitteeMember : PartyId → RoundNumber → MembershipProof → Set
    IsBlockSignature : Block → Signature → Set
    IsVoteSignature : Vote → Signature → Set

record Network : Set₁ where
  field
    Δ : ℕ

module _ ⦃ _ : Postulates ⦄
         where

  open Postulates ⦃...⦄

  ValidVote : Vote → Set
  ValidVote v =
    IsCommitteeMember
        (creatorId v)
        (votingRound v)
        (proofM v)
    × IsVoteSignature v (signature v)

Equivocation relation

Equivocal votes are multiple votes by the same party for the same round.

data _∻_ : Vote → Vote → Set where

  Equivocation : ∀ {v₁ v₂}
    → creatorId v₁ ≡ creatorId v₂
    → votingRound v₁ ≡ votingRound v₂
    → v₁ ≢ v₂
    → v₁ ∻ v₂

Chain

Chain = List Block

certsFromChain : Chain → List Certificate
certsFromChain = mapMaybe certificate

insertCert : Certificate → List Certificate → List Certificate
insertCert cert [] = cert ∷ []
insertCert cert (cert' ∷ certs) =
  if cert == cert'
  then cert' ∷ certs
  else cert' ∷ insertCert cert certs

{-# COMPILE AGDA2HS insertCert #-}

Chain prefix

data _⪯_ : Chain → Chain → Set where

  Prefix : ∀ {c₁ c₂ c₃ : Chain}
    → c₁ ++ c₃ ≡ c₂
    → c₁ ⪯ c₂

Chain pruning

prune : SlotNumber → Chain → Chain
prune (MkSlotNumber sl) = filter ((_≤? sl) ∘ slotNumber')

Chain weight

open Params ⦃...⦄

module _ ⦃ _ : Hashable Block ⦄
         where

  open Hashable ⦃...⦄

  ChainExtends : Hash Block → Certificate → Chain → Set
  ChainExtends h c =
    Any (λ block → (hash block ≡ blockRef c))
      ∘ Data.List.dropWhile (λ block' → ¬? (hash block' ≟-BlockHash h))

  ChainExtends? : (h : Hash Block) → (c : Certificate) → (chain : Chain) → Dec (ChainExtends h c chain)
  ChainExtends? h c =
    any? (λ block → (hash block ≟-BlockHash blockRef c))
      ∘ Data.List.dropWhile (λ block' → ¬? (hash block' ≟-BlockHash h))

  Extends : Hash Block → Certificate → List Chain → Set
  Extends h c = Any (ChainExtends h c)

  Extends? : (h : Hash Block) → (c : Certificate) → (chains : List Chain) → Dec (Extends h c chains)
  Extends? h c = any? (ChainExtends? h c)

module _ ⦃ _ : Hashable Block ⦄
         ⦃ _ : Params ⦄
         where

  open Hashable ⦃...⦄

  _PointsInto_ : Certificate → Chain → Set
  _PointsInto_ c = Any ((blockRef c ≡_) ∘ hash)

  _PointsInto?_ : ∀ (c : Certificate) → (ch : Chain) → Dec (c PointsInto ch)
  _PointsInto?_ c = any? ((blockRef c ≟-BlockHash_) ∘ hash)

  StartOfRound : SlotNumber → RoundNumber → Set
  StartOfRound (MkSlotNumber sl) (MkRoundNumber r) = sl ≡ r * U

  StartOfRound? : (sl : SlotNumber) → (r : RoundNumber) → Dec (StartOfRound sl r)
  StartOfRound? (MkSlotNumber sl) (MkRoundNumber r) = sl ≟ r * U

  rnd : ℕ → ⦃ _ : NonZero U ⦄ → ℕ
  rnd s = s / U

  v-round : SlotNumber → RoundNumber
  v-round (MkSlotNumber s) = MkRoundNumber (rnd s)

Chain weight

  ∥_∥_ : Chain → List Certificate → ℕ
  ∥ ch ∥ cts = ∣ ch ∣ + ∣ filter (_PointsInto? ch) cts ∣ * B

Chain validity

module _ ⦃ _ : Hashable Block ⦄
         ⦃ _ : Postulates ⦄
         ⦃ _ : Network ⦄

         where

  open Hashable ⦃...⦄
  open Postulates ⦃...⦄
  open Network ⦃...⦄

  data ValidChain : Chain → Set where

    Genesis : ValidChain []

    Cons : ∀ {c : Chain} {b : Block}
      → IsBlockSignature b (signature b)
      → IsSlotLeader (creatorId b) (slotNumber b) (leadershipProof b)
      → parentBlock b ≡ tipHash c
      → ValidChain c
      → ValidChain (b ∷ c)

-- | `foldl` does not exist in `Haskell.Prelude` so let's roll our own
-- but let's make it total.
foldl1Maybe : ∀ {a : Set} -> (a -> a -> a) -> List a -> Maybe a
foldl1Maybe f xs =
  foldl (λ m y -> Just (case m of λ where
                             Nothing -> y
                             (Just x)  -> f x y))
        Nothing xs

{-# COMPILE AGDA2HS foldl1Maybe #-}

prefix : List Block -> List Block -> List Block -> List Block
prefix acc (x ∷ xs) (y ∷ ys) =
  if x == y
   then prefix (x ∷ acc) xs ys
   else reverse acc
prefix acc _ _ = reverse acc

{-# COMPILE AGDA2HS prefix #-}

commonPrefix : List Chain -> List Block
commonPrefix chains =
  case listPrefix of λ where
     Nothing -> []
     (Just bs) -> reverse bs
   where
     listPrefix : Maybe (List Block)
     listPrefix = foldl1Maybe (prefix []) (map (λ l -> reverse l) chains)

{-# COMPILE AGDA2HS commonPrefix #-}
-->