Messages

Messages

-- r-cur, current QC_high , when QC-high.r = r-cur - 1 then TC = nothing else TC.r = r-1
TimeoutMessage = TimeoutEvidence × Maybe TC
Proposal       = Signed Block
VoteShare      = SignedShare (BlockId × Round)
TCMessage      = {- Signed -} TC

instance
  HasRound-VS = HasRound VoteShare      ∋ λ where ._∙round →  proj₂  ∘ datum
  HasRound-TM = HasRound TimeoutMessage ∋ λ where ._∙round → _∙round ∘ proj₁

  HasBlockId-VS = HasBlockId VoteShare ∋ λ where ._∙blockId → proj₁ ∘ datum

data Message : Type where
  Propose  : Proposal       → Message
  Vote     : VoteShare      → Message
  TCFormed : TCMessage      → Message
  Timeout  : TimeoutMessage → Message

Messages   = List Message
VoteShares = List VoteShare

data _qc∈-Message_ (qc : QC) : Message → Type where
  qc∈-Propose :
    qc ≡ sb ∙qc
    ─────────────────────────
    qc qc∈-Message Propose sb

  qc∈-ProposeTC :
    ∙ sb ∙tc? ≡ just tc
    ∙ qc ∈₁ qcs⁺ tc
      ─────────────────────────
      qc qc∈-Message Propose sb

  qc∈-TCFormed :
    qc ∈₁ qcs⁺ tc
    ──────────────────────────
    qc qc∈-Message TCFormed tc

  qc∈-Timeout : ∀{tm} →
    qc ≡ (tm .proj₁) ∙qcTE
    ─────────────────────────
    qc qc∈-Message Timeout tm

  qc∈-TimeoutTC : ∀{tm} →
    ∙ tm .proj₂ ≡ just tc
    ∙ qc ∈₁ qcs⁺ tc
      ─────────────────────────
      qc qc∈-Message Timeout tm

data _tc∈-Message_ (tc : TC) : Message → Type where
  tc∈-Propose :
    sb ∙tc? ≡ just tc
    ─────────────────────────
    tc tc∈-Message Propose sb

  tc∈-TCFormed :
    ──────────────────────────
    tc tc∈-Message TCFormed tc

  tc∈-Timeout : ∀{tm} →
    tm .proj₂ ≡ just tc
    ─────────────────────────
    tc tc∈-Message Timeout tm

IsTimeoutForRound : Round → Message → Type
IsTimeoutForRound r (Timeout (te , _)) = te ∙round ≡ r
IsTimeoutForRound r _ = ⊥

VotesFor : Block → Message → Type
VotesFor b = λ where
  (Vote vs) → vs ∙blockId ≡ b ∙blockId
  _ → ⊥

Envelopes

Envelopes add a recipient to a message (recipient = just p), or are a broadcast message (recipient = nothing).

record Envelope : Type where
   constructor [_?∣_⟩
   field recipient : Maybe Pid
         content   : Message