Blocks

Signatures on objects

Signed Objects

We may sign hashable objects, such as votes, messages, etc.

record Signed (A : Type) : Type where
  constructor _signed-by_
  field datum     : A
        node      : Pid

  signature :  ⦃ _ : Digestable A ⦄ → Signature
  signature = sign (node ∙sk) datum

SignedShare = Signed

Threshold signatures

BlockId = Hash

record ThresholdSig (A : Type) : Type where
  field payload       : A
        shares        : List Pid
        .uniqueShares : Unique shares
        .quorum       : IsMajority shares

-- If we follow the paper to the letter shares should be a list of (A × Pid)
-- such that all elements have payload as first component.
-- Morally a Share = Pid × A

Quorum Certificates

QC = ThresholdSig (BlockId × Round)
     -- missing property: let (bid , r) = qc .payload.
     -- then ∀ b → blockId b ≡ bid → b ∙round ≡ r
     -- This condition was added to the connects-to predicate.

QCs = List QC

qcPayload : QC → PayloadQC
qcPayload qc = let bid , r = qc .payload in
  (bid , r , qc .shares)

qcPayload-inj : Injective≡ qcPayload
qcPayload-inj eq with refl , refl ← Prod.,-injective eq = refl

instance
  Digestable-QC : Digestable QC
  Digestable-QC = λ where
    .digest     → digest ∘ qcPayload
    .digest-inj → qcPayload-inj ∘ digest-inj

rqcPayload : Round × QC → ℕ × PayloadQC
rqcPayload = map₂ qcPayload

rqcPayload-inj : Injective≡ rqcPayload
rqcPayload-inj eq with refl , refl ← Prod.,-injective eq = refl

instance
  Digestable-ℕ×QC : Digestable (Round × QC)
  Digestable-ℕ×QC = λ where
    .digest     → digest ∘ rqcPayload
    .digest-inj → rqcPayload-inj ∘ digest-inj

QC order

Quorum certificates are ordered by round.

The following function returns the higher of two QCs.

qc ≤qc qc′ = qc ∙round ≤ qc′ ∙round
qc <qc qc′ = qc ∙round < qc′ ∙round

_≤qc?_ = Decidable² _≤qc_ ∋ dec²
_<qc?_ = Decidable² _<qc_ ∋ dec²

qc ⊔qc qc′ = if ¿ qc ≤qc qc′ ¿ᵇ then qc′ else qc

QC Property

In every qc there is an honest vote share.

qc⇒hp : ∀ (qc : QC) →
    ─────────────────────────────────
    ∃ λ p → p ∈ qc .shares × Honest p
qc⇒hp qc = satisfied′ $ honestFromMajority (getUnique qc) (getQuorum qc)

Timeout Certificates

-- TimeoutEvidence comes from timeout messages
TimeoutEvidence = Signed (Round × QC)

record TC : Type where
  field
    roundTC : Round
    tes     : List TimeoutEvidence
    -- NB: should we only keep the highest QC?
    --     possibly a compressed TC' after gathering timeouts

    .quorumTC : IsMajority tes
    .uniqueTC : UniqueBy node tes
    -- ^ each piece of TimeoutEvidence should be signed by a different replica.
    .allRound : All (λ te → te ∙round       ≡ roundTC) tes
    .qcBound  : All (λ te → te ∙qcTE ∙round < roundTC) tes

TCs = List TC

PayloadTE = Pid × PayloadQC

opaque
  tePayload : TimeoutEvidence → PayloadTE
  tePayload ((r , qc) signed-by p) = p , qcPayload qc

  tePayloads-inj : ∀ {tes tes′} →
    ∙ All (λ te → te ∙round ≡ r) tes
    ∙ All (λ te → te ∙round ≡ r) tes′
    ∙ map tePayload tes ≡ map tePayload tes′
      ──────────────────────────────────────
      tes ≡ tes′
  tePayloads-inj {tes = []}    []          []           refl = refl
  tePayloads-inj {tes = _ ∷ _} (refl ∷ r≡) (refl ∷ r≡′) tes≡
    with refl , tes≡ ← L.∷-injective tes≡
    = cong₂ _∷_ refl $ tePayloads-inj r≡ r≡′ tes≡

  tcPayload : TC → PayloadTC
  tcPayload tc = tc .roundTC , map tePayload (tc .tes)

  tcPayload-inj : Injective≡ tcPayload
  tcPayload-inj {tc}{tc′} tc≡
    with refl , tes≡ ← Prod.,-injective tc≡
    with refl ← tePayloads-inj (getAllRound tc) (getAllRound tc′) tes≡
    = refl

instance
  Digestable-TC : Digestable TC
  Digestable-TC = λ where
    .digest     → digest ∘ tcPayload
    .digest-inj → tcPayload-inj ∘ digest-inj

Blocks

record Block : Type where
  constructor ⟨_,_,_,_⟩
  field
    blockQC : QC
    blockTC : Maybe TC
    round   : Round
    txs     : List Transaction

SBlock = Signed Block

Genesis and Genesis QC

Chain = List Block

genesis : Chain
genesis = []

genesisId = genesis ♯

qc₀ : QC
qc₀ = record
  { payload      = genesisId , 
  ; shares       = allPids
  ; uniqueShares = L.Unique.tabulate⁺ {f = id} id
  ; quorum       = allPidsMajority
  }

instance
  HasBlockId-Chain = HasBlockId Chain ∋ λ where
    ._∙blockId []      → genesisId
    ._∙blockId (b ∷ _) → b ∙blockId
  HasRound-Chain = HasRound Chain ∋ λ where
    ._∙round []      → 
    ._∙round (b ∷ _) → b ∙round

highestQC : TC → QC
highestQC tc = maxNE (qcs⁺ tc)

ValidBlock : Block → Type
ValidBlock b = b ∙round > b .blockQC ∙round

record _-connects-to-_ (b : Block) (ch : Chain) : Type where
  constructor connects∶
  field idMatch       : (b .blockQC) ∙blockId ≡ ch ∙blockId
        roundMatch    : (b .blockQC) ∙round   ≡ ch ∙round
        roundAdvances : ValidBlock b -- TODO: move to Block
open _-connects-to-_ public