Skip to content

Commit d90f164

Browse files
yveshauseryveshauser
committed
Initial sketch of PoS-NSB small step semantics
1 parent 1df74e6 commit d90f164

5 files changed

Lines changed: 138 additions & 101 deletions

File tree

‎src/Peras/Block.agda‎

Lines changed: 9 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,4 @@
11
module Peras.Block where
2-
{-
3-
{-# LANGUAGE DerivingStrategies #-}
4-
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
5-
module Peras.Block where
6-
7-
import Data.Word (Word64)
8-
import Peras.Crypto (Hash, LeadershipProof, Signature, VerificationKey)
9-
import Data.Set (Set)
10-
import Data.ByteString (ByteString)
11-
-}
122

133
open import Level
144
open import Agda.Builtin.Word
@@ -22,27 +12,26 @@ open import Peras.Crypto
2212
record PartyId : Set where
2313
constructor mkPartyId
2414
field vkey : VerificationKey
25-
-- deriving newtype (Eq, Show, Ord)
2615

2716
record Tx : Set where
2817
field tx : ByteString
29-
-- deriving newtype (Eq, Show)
3018

19+
Slot = Word64
3120

3221
record Block : Set where
33-
field slotNumber : Word64
34-
blockHeight : Word64
22+
field slotNumber : Slot
23+
-- blockHeight : Word64
3524
creatorId : PartyId
3625
parentBlock : Hash
3726
includedVotes : set HashO
3827
leadershipProof : LeadershipProof
3928
payload : List Tx
4029
signature : Signature
41-
-- deriving stock (Eq, Show)
4230

43-
postulate blEq : Relation.Binary.Rel Block zero
44-
blLt : Relation.Binary.Rel Block zero
45-
blIs : Relation.Binary.IsStrictTotalOrder blEq blLt
31+
postulate
32+
blEq : Relation.Binary.Rel Block zero
33+
blLt : Relation.Binary.Rel Block zero
34+
blIs : Relation.Binary.IsStrictTotalOrder blEq blLt
4635

4736
BlockO : StrictTotalOrder zero zero zero
4837
BlockO = record {
@@ -51,5 +40,6 @@ BlockO = record {
5140
_<_ = blLt ;
5241
isStrictTotalOrder = blIs }
5342

54-
postulate isValidBlock : Block -> Bool
43+
postulate
44+
isValidBlock : Block -> Bool
5545

‎src/Peras/Chain.agda‎

Lines changed: 116 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -1,34 +1,21 @@
1-
{-
2-
3-
{-# LANGUAGE DerivingStrategies #-}
4-
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
5-
6-
-}
7-
8-
91
module Peras.Chain where
102

11-
{-
12-
import Data.ByteString (ByteString)
13-
import Data.Set (Set)
14-
import Data.Word (Word64)
15-
import Peras.Block (Block, PartyId (..))
16-
import Peras.Crypto (MembershipProof, Signature, isCommitteeMember, verify)
17-
-}
18-
193
open import Agda.Builtin.Word
204
open import Data.Bool
5+
open import Data.List as List using (List; all; foldr)
216
open import Level
227
open import Data.Tree.AVL.Sets renaming (⟨Set⟩ to set)
8+
open import Relation.Unary using (Pred)
239
open import Relation.Binary using (StrictTotalOrder)
2410

11+
import Relation.Binary.PropositionalEquality as Eq
12+
open Eq using (_≡_; refl; cong; sym)
13+
2514
open import Peras.Crypto
2615
open import Peras.Block
2716

2817
record RoundNumber : Set where
2918
field roundNumber : Word64
30-
-- deriving newtype (Eq, Show, Ord)
31-
3219

3320
record Vote msg : Set where
3421
constructor vote
@@ -37,11 +24,11 @@ record Vote msg : Set where
3724
committeeMembershipProof : MembershipProof
3825
blockHash : msg
3926
signature : Signature
40-
-- deriving stock (Eq, Show, Ord)
4127

42-
postulate vblEq : Relation.Binary.Rel (Vote Block) zero
43-
vblLt : Relation.Binary.Rel (Vote Block) zero
44-
vblIs : Relation.Binary.IsStrictTotalOrder vblEq vblLt
28+
postulate
29+
vblEq : Relation.Binary.Rel (Vote Block) zero
30+
vblLt : Relation.Binary.Rel (Vote Block) zero
31+
vblIs : Relation.Binary.IsStrictTotalOrder vblEq vblLt
4532

4633
VoteBlockO : StrictTotalOrder zero zero zero
4734
VoteBlockO = record {
@@ -53,7 +40,8 @@ VoteBlockO = record {
5340
toSignable : ∀{msg} → Vote msg -> ByteString
5441
toSignable _ = emptyBS -- const ""
5542

56-
postulate makeVote : ∀{msg} → RoundNumber -> PartyId -> msg -> Vote msg
43+
postulate
44+
makeVote : ∀{msg} → RoundNumber -> PartyId -> msg -> Vote msg
5745

5846
-- | A vote is valid if the committee-membership proof and the signature are valid.
5947

@@ -65,13 +53,11 @@ isValid v@(vote _ (mkPartyId vkey) committeeMembershipProof _ signature) =
6553
record Chain : Set where
6654
constructor chain
6755
field blocks : set BlockO
68-
tip : Block
69-
-- ^ The tip of this chain, must be a member of `blocks`.
70-
votes : set VoteBlockO
71-
-- ^ The set of "pending" votes, eg. which have not been included in
72-
-- a `Block`.
56+
tip : Block -- The tip of this chain, must be a member of `blocks`
57+
votes : set VoteBlockO -- The set of "pending" votes, eg. which have not been included in a `Block`.
58+
59+
7360

74-
-- deriving stock (Eq, Show)
7561

7662
-- | Chain validity
7763
--
@@ -89,5 +75,105 @@ record Chain : Set where
8975
-- TODO: expressing those conditions directly would be very expensive,
9076
-- it's more efficient to enforce them whenever the chain is extended.
9177

92-
postulate isValidChain : Chain -> Bool
9378

79+
postulate
80+
verifyLeadershipProof : Block → Bool
81+
82+
properlyLinked : Chain → Bool
83+
decreasingSlots : Chain → Bool
84+
85+
correctBlocks : Chain → Bool
86+
correctBlocks (chain blocks _ _) =
87+
let bs = toList BlockO blocks
88+
in all verifyLeadershipProof bs
89+
90+
postulate
91+
isValidChain : Chain -> Bool
92+
93+
94+
{-
95+
Formalizing Nakamoto-Style Proof of Stake
96+
Søren Eller Thomsen and Bas Spitters
97+
-}
98+
99+
-- progress
100+
101+
data Progress : Set where
102+
103+
Ready : Progress
104+
Delivered : Progress
105+
Baked : Progress
106+
107+
record Message : Set where
108+
constructor mkMessage
109+
field
110+
msg : ByteString
111+
112+
-- global state
113+
114+
record GlobalState : Set where
115+
constructor ⟪_,_,_,_⟫
116+
field
117+
slot : Slot
118+
progress : Progress
119+
messages : List Message
120+
execution-order : List PartyId
121+
122+
open GlobalState
123+
124+
postulate
125+
party_bake_step_world : PartyId → GlobalState → GlobalState
126+
party_rcv_step_world : PartyId → GlobalState → GlobalState
127+
incrementSlot : Slot → Slot
128+
permParties : List PartyId → List PartyId
129+
permMessages : List Message → List Message
130+
131+
data _↝_ : GlobalState → GlobalState → Set where
132+
133+
Deliver : ∀ {s ms ps}
134+
→ ⟪ s , Ready , ms , ps ⟫ ↝
135+
let gs = List.foldr party_rcv_step_world ⟪ s , Ready , ms , ps ⟫ ps
136+
in record gs { progress = Delivered }
137+
138+
Bake : ∀ {s ms ps}
139+
→ ⟪ s , Delivered , ms , ps ⟫ ↝
140+
let gs = List.foldr party_bake_step_world ⟪ s , Delivered , ms , ps ⟫ ps
141+
in record gs { progress = Delivered }
142+
143+
NextRound : ∀ {s ms ps}
144+
→ ⟪ s , Baked , ms , ps ⟫ ↝ ⟪ incrementSlot s , Ready , ms , ps ⟫
145+
146+
PermParties : ∀ {s p ms ps}
147+
→ ⟪ s , p , ms , ps ⟫ ↝ ⟪ s , p , ms , permParties ps ⟫
148+
149+
PermMsgs : ∀ {s p ms ps}
150+
→ ⟪ s , p , ms , ps ⟫ ↝ ⟪ s , p , permMessages ms , ps ⟫
151+
152+
-- reflexive, transitive closure (which is big-step in the paper)
153+
154+
infix 2 _↝⋆_
155+
infixr 2 _↝⟨_⟩_
156+
infix 3 _∎
157+
158+
data _↝⋆_ : GlobalState → GlobalState → Set where
159+
160+
_∎ : ∀ M
161+
-------
162+
→ M ↝⋆ M
163+
164+
_↝⟨_⟩_ : ∀ L {M N}
165+
→ L ↝ M
166+
→ M ↝⋆ N
167+
------
168+
→ L ↝⋆ N
169+
170+
{-
171+
-- knowledge propagation
172+
lemma_1 : ∀ (N₀ N₁ N₂ : GlobalState)
173+
→ (p₁ p₂ : PartyId)
174+
→ Nₒ ↝⋆ N₁
175+
→ N₁ ↝⋆ N₂
176+
→ progress N₁ ≡ Ready
177+
→ progress N₂ ≡ Delivered
178+
→ allBlocks t₁ ⊂ allBlocks t₂
179+
-}

‎src/Peras/Crypto.agda‎

Lines changed: 8 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1,34 +1,27 @@
1-
{-
2-
3-
{-# LANGUAGE DerivingStrategies #-}
4-
{-# LANGUAGE DuplicateRecordFields #-}
5-
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
6-
71
-- | Cryptographic primitives types and functions used to implement /Peras/ protocol.
82
--
93
-- We don't use real cryptography here, just a bunch of newtypes and
104
-- simple functions that represent various cryptographic operations
115
-- one can do when running the protocol
12-
13-
-}
146
module Peras.Crypto where
157

168
open import Level
179
open import Relation.Binary using (StrictTotalOrder)
1810
open import Data.Unit
1911
open import Data.Bool
2012

21-
postulate ByteString : Set
22-
emptyBS : ByteString
23-
_isInfixOf_ : ByteString → ByteString → Bool
13+
postulate
14+
ByteString : Set
15+
emptyBS : ByteString
16+
_isInfixOf_ : ByteString → ByteString → Bool
2417

2518
record Hash : Set where
2619
field hash : ByteString
27-
-- deriving newtype (Eq, Show)
2820

29-
postulate hsEq : Relation.Binary.Rel Hash zero
30-
postulate hsLt : Relation.Binary.Rel Hash zero
31-
postulate hsIs : Relation.Binary.IsStrictTotalOrder hsEq hsLt
21+
postulate
22+
hsEq : Relation.Binary.Rel Hash zero
23+
hsLt : Relation.Binary.Rel Hash zero
24+
hsIs : Relation.Binary.IsStrictTotalOrder hsEq hsLt
3225

3326
HashO : StrictTotalOrder zero zero zero
3427
HashO = record {
@@ -37,35 +30,25 @@ HashO = record {
3730
_<_ = hsLt ;
3831
isStrictTotalOrder = hsIs }
3932

40-
4133
-- should use normal VRF algorithm like leadership membership
4234
record MembershipProof : Set where
4335
constructor membershipProof
4436
field proof : ByteString
45-
-- deriving newtype (Eq, Show, Ord)
46-
47-
4837

4938
record LeadershipProof : Set where
5039
field proof : ByteString
51-
-- deriving newtype (Eq, Show)
5240

5341
{-
5442
-- use KES-based signatures which weighs about 600 bytes (could be
5543
-- down to 400)
5644
-}
5745

58-
5946
record Signature : Set where
6047
field signature : ByteString
61-
-- deriving newtype (Eq, Show, Ord)
62-
6348

6449
record VerificationKey : Set where
6550
constructor verificationKey
6651
field verKey : ByteString
67-
-- deriving newtype (Eq, Show, Ord)
68-
6952

7053
-- | a fake membership "proof" is simply a concatenation of all the
7154
-- members' verification keys.

‎src/Peras/Message.agda‎

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,8 @@
1-
{-
2-
{-# LANGUAGE DuplicateRecordFields #-}
3-
{-# LANGUAGE DerivingStrategies #-}
4-
-}
51
module Peras.Message where
62

7-
-- import Peras.Chain (RoundNumber, Vote)
8-
open import Peras.Chain
3+
open import Peras.Chain using (RoundNumber; Vote)
94

105
data Message msg : Set where
116
VoteFor : RoundNumber → msg → Message msg
127
NewVote : Vote msg → Message msg
138
NewChain : msg → Message msg
14-
-- deriving stock (Eq, Show)

‎src/Peras/Nakamoto.agda‎

Lines changed: 4 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,6 @@
1-
{-
2-
{-# LANGUAGE DerivingStrategies #-}
3-
{-# LANGUAGE LambdaCase #-}
4-
-}
5-
61
-- | The Nakamoto layer of the Peras protocol.
72
module Peras.Nakamoto where
83

9-
{-
10-
import Data.Map (Map)
11-
import Data.Set (Set)
12-
import Data.Word (Word64)
13-
import Peras.Block (Block (..), PartyId, isValidBlock)
14-
import Peras.Chain (Vote)
15-
import Peras.Message (Message (..))
16-
-}
17-
184
open import Agda.Builtin.Word
195
open import Level
206
open import Data.Tree.AVL.Sets renaming (⟨Set⟩ to set)
@@ -29,7 +15,6 @@ record ConsensusConfig : Set where
2915
field partyId : PartyId
3016
roundLength : Word64
3117
cooldownPeriod : Word64
32-
-- deriving stock (Eq, Show)
3318

3419
-- | Compute the weight of a (tip of) a chain w.r.t to a set of
3520
-- pending votes.
@@ -47,9 +32,10 @@ chainWeight ConsensusConfig{roundLength} Block{blockHeight, slotNumber} pendingV
4732
in undefined
4833
-}
4934

50-
postulate wEq : Relation.Binary.Rel Word64 zero
51-
wLt : Relation.Binary.Rel Word64 zero
52-
wIs : Relation.Binary.IsStrictTotalOrder wEq wLt
35+
postulate
36+
wEq : Relation.Binary.Rel Word64 zero
37+
wLt : Relation.Binary.Rel Word64 zero
38+
wIs : Relation.Binary.IsStrictTotalOrder wEq wLt
5339

5440
WordO : StrictTotalOrder zero zero zero
5541
WordO = record {
@@ -64,12 +50,10 @@ record ConsensusState : Set where
6450
field currentChain : Block
6551
seenChains : set BlockO
6652
votesReceived : Map WordO (Map BlockO (set VoteBlockO))
67-
-- deriving stock (Eq, Show)
6853

6954
data Decision : Set where
7055
Tally : Vote Block → Decision
7156
Seen : Block → Decision
72-
-- deriving stock (Eq, Show)
7357

7458
{-
7559
nakamotoLayer :: ConsensusConfig -> ConsensusState -> Message Block -> Decision

0 commit comments

Comments
 (0)