module Peras.SmallStep where
The small-step semantics of the Ouroboros Peras protocol define the evolution of the global state of the system modelling honest and adversarial parties. The number of parties is fixed during the execution of the protocol and the list of parties has to be provided as a module parameter. In addition the model is parameterized by the lotteries (for slot leadership and voting committee membership) as well as the type of the block tree. Furthermore adversarial parties share generic, adversarial state.
References:
The parameters for the Peras protocol and hash functions are defined as instance arguments of the module.
module _ ⦃ _ : Hashable Block ⦄
⦃ _ : Hashable (List Tx) ⦄
⦃ _ : Params ⦄
⦃ _ : Network ⦄
⦃ _ : Postulates ⦄
where
The block tree, resp. the validity of the chain is defined with respect
of the parameters.
open Hashable ⦃...⦄ open Params ⦃...⦄ open Network ⦃...⦄ open Postulates ⦃...⦄
data Message : Type where
ChainMsg : {c : Chain} → ValidChain c → Message
VoteMsg : {v : Vote} → ValidVote v → Message
Messages can be delayed by a number of slots
Delay = Fin (suc (suc Δ)) pattern 𝟘 = fzero pattern 𝟙 = fsuc fzero pattern 𝟚 = fsuc (fsuc fzero)Messages are put into an envelope and assigned to a party. The message can be delayed.
record Envelope : Type where
constructor ⦅_,_,_,_⦆
field
partyId : PartyId
honesty : Honesty partyId
message : Message
delay : Delay
open Envelope
record IsTreeType {T : Type}
(tree₀ : T)
(addChain : T → {c : Chain} → ValidChain c → T)
(chains : T → List Chain)
(preferredChain : T → Chain)
(addVote : T → {v : Vote} → ValidVote v → T)
(votes : T → List Vote)
(certs : T → List Certificate)
(cert₀ : Certificate)
: Type₁ where
field
Properties that must hold with respect to chains, certificates and
votes.
instantiated :
preferredChain tree₀ ≡ []
instantiated-certs :
certs tree₀ ≡ cert₀ ∷ []
instantiated-votes :
votes tree₀ ≡ []
extendable-chain : ∀ (t : T) {c : Chain} (vc : ValidChain c)
→ certs (addChain t vc) ≡ H.foldr insertCert (certs t) (certsFromChain c)
valid : ∀ (t : T)
→ ValidChain (preferredChain t)
optimal : ∀ (c : Chain) (t : T)
→ let
b = preferredChain t
cts = certs t
in
ValidChain c
→ c ∈ chains t
→ ∥ c ∥ cts ≤ ∥ b ∥ cts
self-contained : ∀ (t : T)
→ preferredChain t ∈ chains t
{-
valid-votes : ∀ (t : T)
→ All ValidVote (votes t)
-}
unique-votes : ∀ (t : T) {v : Vote} (vv : ValidVote v)
→ let vs = votes t
in
v ∈ vs
→ vs ≡ votes (addVote t vv)
no-equivocations : ∀ (t : T) {v : Vote} (vv : ValidVote v)
→ let vs = votes t
in
Any (v ∻_) vs
→ vs ≡ votes (addVote t vv)
quorum-cert : ∀ (t : T) (b : Block) (r : ℕ)
→ length (filter (λ {v →
(getRoundNumber (votingRound v) ≟ r)
×-dec (blockHash v ≟-BlockHash hash b)}
) (votes t)) ≥ τ
→ Any (λ {c →
(getRoundNumber (round c) ≡ r)
× (blockRef c ≡ hash b) }) (certs t)
In addition to chains the block-tree manages votes and certificates as
well. The block-tree type is defined as follows:
record TreeType (T : Type) : Type₁ where
field
tree₀ : T
addChain : T → {c : Chain} → ValidChain c → T
chains : T → List Chain
preferredChain : T → Chain
addVote : T → {v : Vote} → ValidVote v → T
votes : T → List Vote
certs : T → List Certificate
cert₀ : Certificate
cert₀ = MkCertificate (MkRoundNumber 0) (MkHash emptyBS)
field
is-TreeType : IsTreeType
tree₀ addChain chains preferredChain
addVote votes certs cert₀
latestCertOnChain : T → Certificate
latestCertOnChain =
latestCert cert₀ ∘ L.mapMaybe certificate ∘ preferredChain
latestCertSeen : T → Certificate
latestCertSeen = latestCert cert₀ ∘ certs
hasCert : RoundNumber → T → Type
hasCert (MkRoundNumber r) = Any ((r ≡_) ∘ roundNumber) ∘ certs
hasCert? : (r : RoundNumber) (t : T) → Dec (hasCert r t)
hasCert? (MkRoundNumber r) = any? ((r ≟_) ∘ roundNumber) ∘ certs
hasVote : RoundNumber → T → Type
hasVote (MkRoundNumber r) = Any ((r ≡_) ∘ votingRound') ∘ votes
hasVote? : (r : RoundNumber) (t : T) → Dec (hasVote r t)
hasVote? (MkRoundNumber r) = any? ((r ≟_) ∘ votingRound') ∘ votes
allBlocks : T → List Block
allBlocks = concat ∘ chains
In order to define the semantics the following parameters are required additionally:
module Semantics
{T : Type} {blockTree : TreeType T}
{S : Type} {adversarialState₀ : S}
{txSelection : SlotNumber → PartyId → List Tx}
{parties : Parties} -- TODO: use parties from blockTrees
-- i.e. allow dynamic participation
where
open TreeType blockTree
private
instance
Default-T : Default T
Default-T .def = tree₀
Updating the block-tree upon receiving a message for vote and block messages.
data _[_]→_ : T → Message → T → Type where
VoteReceived : ∀ {v vv t} →
────────────────────────────
t [ VoteMsg {v} vv ]→ addVote t vv
ChainReceived : ∀ {c vc t} →
──────────────────────────────
t [ ChainMsg {c} vc ]→ addChain t vc
When does a party vote in a round? The protocol expects regular voting, i.e. if in the previous round a quorum has been achieved or that voting resumes after a cool-down phase.
BlockSelection' : SlotNumber → Chain → Hash Block
BlockSelection' (MkSlotNumber s) =
tipHash ∘ filter (λ {b → (slotNumber' b) + L ≤? s})
BlockSelection : SlotNumber → T → Hash Block
BlockSelection s = BlockSelection' s ∘ preferredChain
VotingRule-1A : RoundNumber → T → Type
VotingRule-1A (MkRoundNumber r) t = r ≡ suc (roundNumber (latestCertSeen t))
VR-1B: The extends the block certified by cert-r−1,
VotingRule-1B : SlotNumber → T → Type
VotingRule-1B s t = Extends (BlockSelection s t) (latestCertSeen t) (chains t)
VR-1: Both VR-1A and VR-1B hold
VotingRule-1 : SlotNumber → T → Type
VotingRule-1 s t =
VotingRule-1A (v-round s) t
× VotingRule-1B s t
VR-2A: The last certificate a party has seen is from a round at least R
rounds back
VotingRule-2A : RoundNumber → T → Type
VotingRule-2A (MkRoundNumber r) t = r ≥ roundNumber (latestCertSeen t) + R
VR-2B: The last certificate included in a party’s current chain is from
a round exactly c⋆K rounds ago for some c : ℕ, c ≥ 0
VotingRule-2B : RoundNumber → T → Type
VotingRule-2B (MkRoundNumber r) t =
r > roundNumber (latestCertOnChain t)
× r mod K ≡ (roundNumber (latestCertOnChain t)) mod K
VR-2: Both VR-2A and VR-2B hold
VotingRule-2 : RoundNumber → T → Type
VotingRule-2 r t =
VotingRule-2A r t
× VotingRule-2B r t
If either VR-1A and VR-1B or VR-2A and VR-2B hold, voting is expected
VotingRule : SlotNumber → T → Type
VotingRule s t =
VotingRule-1 s t
⊎ VotingRule-2 (v-round s) t
The small-step semantics rely on a global state, which consists of the following fields:
record State : Type where
constructor ⟦_,_,_,_,_⟧
field
clock : SlotNumber
blockTrees : AssocList PartyId T
messages : List Envelope
history : List Message
adversarialState : S
blockTrees' : List T
blockTrees' = map proj₂ blockTrees
v-rnd : RoundNumber
v-rnd = v-round clock
v-rnd' : ℕ
v-rnd' = getRoundNumber v-rnd
Fetched : State → Type
Fetched = All (λ { z → delay z ≢ 𝟘 }) ∘ messages
where open State
Predicate for a global state stating that the current slot is the last
slot of a voting round.
LastSlotInRound : State → Type
LastSlotInRound M =
suc (rnd (getSlotNumber clock)) ≡ rnd (suc (getSlotNumber clock))
where open State M
LastSlotInRound? : (s : State) → Dec (LastSlotInRound s)
LastSlotInRound? M =
suc (rnd (getSlotNumber clock)) ≟ rnd (suc (getSlotNumber clock))
where open State M
Predicate for a global state stating that the next slot will be in a new
voting round.
NextSlotInSameRound : State → Type
NextSlotInSameRound M =
rnd (getSlotNumber clock) ≡ rnd (suc (getSlotNumber clock))
where open State M
NextSlotInSameRound? : (s : State) → Dec (NextSlotInSameRound s)
NextSlotInSameRound? M =
rnd (getSlotNumber clock) ≟ rnd (suc (getSlotNumber clock))
where open State M
Ticking the global clock increments the slot number and decrements the
delay of all the messages in the message buffer.
tick : State → State
tick M =
record M
{ clock = next clock
; messages =
map (λ where e → record e { delay = pred (delay e) })
messages
}
where open State M
Updating the global state inserting the updated block-tree for a given
party, adding messages to the message buffer for the other parties and
appending the history
_,_,_,_⇑_ : Message → Delay → PartyId → T → State → State
m , d , p , l ⇑ M =
record M
{ blockTrees = set p l blockTrees
; messages =
map (uncurry ⦅_,_, m , d ⦆)
(filter (¬? ∘ (p ≟_) ∘ proj₁) parties)
++ messages
; history = m ∷ history
}
where open State M
add_to_diffuse_ : (Message × Delay × PartyId) → T → State → State
add (m@(ChainMsg x) , d , p) to t diffuse M = m , d , p , addChain t x ⇑ M
add (m@(VoteMsg x) , d , p) to t diffuse M = m , d , p , addVote t x ⇑ M
A party receives messages from the global state by fetching messages assigned to the party, updating the local block tree and putting the local state back into the global state.
data _⊢_[_]⇀_ : {p : PartyId} → Honesty p → State → Message → State → Type
where
An honest party consumes a message from the global message buffer and
updates the local state
honest : ∀ {p} {t t′} {m} {N} → let open State N in
blockTrees ⁉ p ≡ just t
→ (m∈ms : ⦅ p , Honest , m , 𝟘 ⦆ ∈ messages)
→ t [ m ]→ t′
---------------------------------------------
→ Honest {p} ⊢
N [ m ]⇀ record N
{ blockTrees = set p t′ blockTrees
; messages = messages ─ m∈ms
}
An adversarial party might delay a message
corrupt : ∀ {p} {as} {m} {N} → let open State N in
(m∈ms : ⦅ p , Corrupt , m , 𝟘 ⦆ ∈ messages)
----------------------------------------------
→ Corrupt {p} ⊢
N [ m ]⇀ record N
{ messages = m∈ms ∷ˡ= ⦅ p , Corrupt , m , 𝟙 ⦆
; adversarialState = as
}
createVote : SlotNumber → PartyId → MembershipProof → Signature → Hash Block → Vote
createVote s p prf sig hb =
record
{ votingRound = v-round s
; creatorId = p
; proofM = prf
; blockHash = hb
; signature = sig
}
A party can vote for a block, if * the current slot is the first slot in a voting round * the party is a member of the voting committee * the chain is not in a cool-down phase
Voting updates the party’s local state and for all other parties a message is added to be consumed immediately. infix 2 _⊢_⇉_
data _⊢_⇉_ : {p : PartyId} → Honesty p → State → State → Type where
honest : ∀ {p} {t} {M} {π} {σ} {b}
→ let
open State
s = clock M
r = v-round s
v = createVote s p π σ b
in
BlockSelection s t ≡ b
→ blockTrees M ⁉ p ≡ just t
→ (sig : IsVoteSignature v σ)
→ StartOfRound s r
→ (mem : IsCommitteeMember p r π)
→ VotingRule s t
----------------------------------------------
→ Honest {p} ⊢
M ⇉ add (VoteMsg (mem , sig) , 𝟘 , p) to t
diffuse M
Rather than creating a delayed vote, an adversary can honestly create it and delay the message.
Certificates are conditionally added to a block. The following function determines if there needs to be a certificate provided for a given voting round and a local block-tree. The conditions are as follows
needCert : RoundNumber → T → Maybe Certificate
needCert (MkRoundNumber r) t =
let
cert⋆ = latestCertOnChain t
cert′ = latestCertSeen t
in
if not (any (λ {c → ⌊ roundNumber c + 2 ≟ r ⌋}) (certs t)) -- (a)
∧ (r ≤ᵇ A + roundNumber cert′) -- (b)
∧ (roundNumber cert⋆ <ᵇ roundNumber cert′) -- (c)
then just cert′
else nothing
Helper function for creating a block
createBlock : SlotNumber → PartyId → LeadershipProof → Signature → T → Block
createBlock s p π σ t =
record
{ slotNumber = s
; creatorId = p
; parentBlock =
let open IsTreeType
in tipHash (preferredChain t)
; certificate =
let r = v-round s
in needCert r t
; leadershipProof = π
; bodyHash =
let txs = txSelection s p
in blockHash
record
{ blockHash = hash txs
; payload = txs
}
; signature = σ
}
A party can create a new block by adding it to the local block tree and diffuse the block creation messages to the other parties. Block creation is possible, if as in Praos
infix 2 _⊢_↷_
data _⊢_↷_ : {p : PartyId} → Honesty p → State → State → Type where
honest : ∀ {p} {t} {M} {π} {σ}
→ let
open State
s = clock M
b = createBlock s p π σ t
pref = preferredChain t
in
blockTrees M ⁉ p ≡ just t
→ (vc : ValidChain (b ∷ pref))
----------------------------
→ Honest {p} ⊢
M ↷ add (
ChainMsg vc
, 𝟘
, p) to t
diffuse M
variable
M N O : State
p : PartyId
h : Honesty p
The relation allows
data _↝_ : State → State → Type where
Fetch : ∀ {m} →
∙ h ⊢ M [ m ]⇀ N
──────────────
M ↝ N
CreateVote :
∙ Fetched M
∙ h ⊢ M ⇉ N
─────────
M ↝ N
CreateBlock :
∙ Fetched M
∙ h ⊢ M ↷ N
─────────
M ↝ N
NextSlot :
∙ Fetched M
──────────
M ↝ tick M
infix 2 _↝⋆_
infixr 2 _↣_
infix 3 ∎
data _↝⋆_ : State → State → Type where
∎ : M ↝⋆ M
_↣_ : M ↝ N → N ↝⋆ O → M ↝⋆ O
infixr 2 _++'_
_++'_ :
M ↝⋆ N
→ N ↝⋆ O
→ M ↝⋆ O
∎ ++' M↝⋆O = M↝⋆O
(M↝M₁ ↣ M₁↝⋆N) ++' N↝⋆O = M↝M₁ ↣ M₁↝⋆N ++' N↝⋆O
open Semantics public