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 : Set 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 : Set where
constructor ⦅_,_,_,_⦆
field
partyId : PartyId
honesty : Honesty partyId
message : Message
delay : Delay
open Envelope
record IsTreeType {T : Set}
(tree₀ : T)
(addChain : T → {c : Chain} → ValidChain c → T)
(chains : T → List Chain) -- TODO: use Set instead of List
(preferredChain : T → Chain)
(addVote : T → {v : Vote} → ValidVote v → T)
(votes : T → List Vote) -- TODO: use Set instead of List
(certs : T → List Certificate) -- TODO: use Set instead of List
(cert₀ : Certificate)
: Set₁ 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-votes : ∀ (t : T) {v : Vote} (vv : ValidVote v)
→ v ∈ votes (addVote t vv)
extendable-chain : ∀ (t : T) {c : Chain} (vc : ValidChain c)
→ certs (addChain t vc) ≡ foldr insertCert (certs t) (certsFromChain c)
self-contained-certs : ∀ (t : T) {c : Chain}
→ c ∈ chains t
→ certs t ≡ foldr insertCert (certs t) (certsFromChain c)
valid : ∀ (t : T)
→ ValidChain (preferredChain t)
optimal : ∀ (c : Chain) (t : T)
→ c ∈ chains t
→ weight c (certs t) ≤ weight (preferredChain t) (certs t)
self-contained : ∀ (t : T)
→ preferredChain t ∈ chains t
{-
-- TODO: use Set instead of List for votes
unique-votes : ∀ (t : T) {v : Vote} (vv : ValidVote v)
→ v ∈ votes t
→ votes t ≡ votes (addVote t vv)
-- TODO: use Set with `equivocation` as equivalence relation for votes
no-equivocations : ∀ (t : T) {v : Vote} (vv : ValidVote v)
→ Any (v ∻_) (votes t)
→ votes t ≡ votes (addVote t vv)
-}
quorum-cert : ∀ (t : T) (b : Block) (r : Nat)
→ L.length
(filter (λ {v →
(getRoundNumber (votingRound v) == r)
&& (blockHash v == 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 : Set) : Set₁ 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
is-TreeType : IsTreeType
tree₀ addChain chains preferredChain
addVote votes certs cert₀
latestCertOnChain : T → Certificate
latestCertOnChain =
latestCert cert₀ ∘ mapMaybe certificate ∘ preferredChain
latestCertSeen : T → Certificate
latestCertSeen = latestCert cert₀ ∘ certs
hasCert : RoundNumber → T → Set
hasCert (MkRoundNumber r) t = Any (λ c → r ≡ roundNumber c) (certs t)
hasVote : RoundNumber → T → Set
hasVote (MkRoundNumber r) t = Any (λ v → r ≡ votingRound' v) (votes t)
allBlocks : T → List Block
allBlocks = concat ∘ chains
postulate -- TODO: any t is constructed based on tree₀
-- using addVote, addChain and tree₀
-- contains cert₀ (see instantiated-certs above)
latestCertSeen∈certs : ∀ t → latestCertSeen t ∈ certs t
In order to define the semantics the following parameters are required additionally:
module Semantics {T : Set} {blockTree : TreeType T} {S : Set} {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 chain messages.
data _[_]→_ : T → Message → T → Set 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
cert-r−1 for round
r−1
VotingRule-1A : RoundNumber → T → Set
VotingRule-1A r t = r ≡ nextRound (round (latestCertSeen t))
VR-1B: The extends the block certified by cert-r−1,
VotingRule-1B : SlotNumber → T → Set
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 → Set
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 → Set
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 → Set
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 → Set
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 → Set
VotingRule s t =
Either
(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 : Set where
constructor ⟦_,_,_,_,_⟧
field
clock : SlotNumber
blockTrees : AssocList PartyId T
messages : List Envelope
history : List Message
adversarialState : S
v-rnd : RoundNumber
v-rnd = v-round clock
v-rnd' : Nat
v-rnd' = getRoundNumber v-rnd
Fetched : State → Set
Fetched s = All (λ { z → delay z ≢ 𝟘 }) (messages s)
where open State
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 = Data.Fin.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 → (PartyId → Delay) → State → State
m , fᵈ ⇑ M =
record M
{ messages =
map (λ (p ,ᵖ h) → ⦅ p , h , m , fᵈ p ⦆) parties
++ messages
; history = m ∷ history
}
where open State M
delay_by_update_ : Message → (PartyId → Delay) → State → State
delay m@(ChainMsg x) by fᵈ update M = m , fᵈ ⇑ M
delay m@(VoteMsg x) by fᵈ update M = m , fᵈ ⇑ 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 → Set
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 → Set 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
→ (fᵈ : PartyId → Delay)
----------------------------------------------
→ Honest {p} ⊢
M ⇉ delay VoteMsg (mem , sig) by fᵈ
update 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 = tipHash (preferredChain t)
; certificate = needCert (v-round s) t
; leadershipProof = π
; bodyHash = hash (txSelection s p)
; 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 → Set 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))
→ (fᵈ : PartyId → Delay)
----------------------------
→ Honest {p} ⊢
M ↷ delay ChainMsg vc by fᵈ
update M
variable
M N O : State
p : PartyId
h : Honesty p
The relation allows
data _↝_ : State → State → Set 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 → Set 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