hey everyone how's it going they already
started my clock so I'm just gonna start
- so we got talk today about CBC Casper
design philosophy it's mostly really
about design methodology and I'm gonna
walk you through some of the stuff that
goes on in CBC Casper land in terms of
the methodology that we use to develop
and define distributed systems protocols
I'm gonna talk about it first is like
what is carpi construction and I'm gonna
talk about domain theory and then like
this kind of defined in this stuff it's
gonna be kind of a trip it's gonna be
pretty cool and then I'll talk and I'll
give some examples are like actual CBC
design in CBC Casper and some of the you
know stuff that happens and to give you
a kind of a taste of the methodology and
[Music]
you know like the the kind of approach
that we have that kind of sets apart a
CBC Casper from you know other because
there's a protocol research and finally
you know the last bit of my talk I'll
just to remind you all that where the
resources are show you some new
resources and make some announcements so
let's talk about design methods in CBC
Casper the number one kind of like
design methodology in CBC Casper is the
correct by construction design a
protocol design methodology the idea
with correct right construction is that
like the process by which you decide
what program you write should guarantee
that that program has the properties
that you want like the very process that
you use to specify the protocol should
guarantee that the protocol has the
properties that you want so somehow like
the way you decide what like formats to
use or what like the protocol is in
terms of like the data and the behavior
you know that happens somehow like the
definitions don't come out of nowhere
and there's like a process by which
stuff gets defined and it's called you
know your first eyes are called correct
by construction if you know the process
that you use to define the thing somehow
is guarantees that
definition that comes out is correct
this is kind of as opposed to the trial
and error approach where you will like
try something and then analyze it and
then you might it might work am I not
you'll maybe get lucky and maybe and if
not they may you learn something and
just keep trying until maybe you'll find
something so this is very different
approach right because instead of like
we never really have the trial and error
we just have like a lot of time defining
stuff and then like once the definition
pops out it's like correct by
construction and so there's no like
error but in some way like you know it
takes us a lot longer to come out with a
full definition but when it when it pops
out you know we know it's correct by
construction and we don't worry at all
about mmm mistakes in the specification
in the same way so there's two basically
kinds of correct by construction
software design that I'm kind of aware
of one of them is you know you you
define like a a proof may be a type
system and some proofs over broad class
of four over calls or broad classic
programs and then you in your design
process choose your protocol your your
protocol to be part of that set so that
you know when you choose it that it's
gonna satisfy the theorem that you know
is is is inhabited by this much broader
set of protocols so if we have like a
you know family of protocols they all
satisfy a theorem and we like pick
protocols or construct them in a way to
guarantee that it part of the family
then we can in a correct by construction
way get a protocol that has that
property that you know the theorem shows
for the family and then the other kind
of approaches that the protocols are
specified in a way that actually
generates a proof of their correctness
so you know the you generate the
protocol and the proof like a new proof
for every proton and and they don't do
any of that it sounds hard and I've ever
heard of people doing it and like
programming languages and compilers but
it hasn't showed up for me yet so what I
do here is basically we we do is we
define large family
of protocols and we prove things about
them and then we and then we and then we
choose specific protocols out of them
which will there by virtue of being in
those families have these properties so
now we're gonna switch over to this very
related topic but going off into the
math deep end so domain theory is a
field of mathematics that studies it's a
you know a it studies the semantics of
programming languages but really the
reason why is super interesting to me
and it just invites really useful for
understanding the correct by
construction process is because it
provides us a language for talking about
partial definitions
you know incomplete definitions partial
protocol specifications and and and we
can understand what it means to have a
process of defining something as opposed
to just having something that's outright
fully defined as you might have in set
theory so like you know you should think
of domain theory as something that arose
out of people's feelings that set theory
was inadequate for dealing with programs
and the semantics of programs especially
recursive programs and like a lazy
evaluation mmm but I'm not an expert in
domain theory but there are some things
that I've learned from domain theory
that I find super useful for thinking
about a bunch of stuff including correct
by construction protocol design so
there's a really really you know kind of
core notation in in domain theory to use
this like and to define this thing
called undefined so this bottom notation
means undefined and it's like defined to
be the most undefined thing it is the
most undefined thing in this partial
order of defined admits like if I if I
say nothing about my protocol then like
I have left it completely undefined and
then somehow that's like the most
undefined that I could leave it and as
soon as I say stuff I it becomes more
defined and we could talk about in
reason formally about this order of
defined earnest and this process of
defining stuff and you know having a
certain stages a partial definition and
then getting in more and more
learn more defined protocols so if a is
a definition that can be reached from a
definition B by replacing an undefined
term and B with something that's defined
or something else then a is gonna be is
more defined than B so basically like if
I have a definition it's got some
undefined term in it and I can replace
it to get some other definition then
that other definition is more defined
than this like initial definition so I'm
gonna give some examples so here we go
you know bottom times bottom is more
defined than bottom because you can
replace bottom with bottom times bottom
and therefore you know you can define
something there's clearly under find
bottom to be this thing bottom times
bottom which is still not totally
defined but it's more defined than just
bottom you know bottom times empty set
is more defined than bottom times bottom
because you can replace bottom with
empty sets and get from bottom times
bottom to bottom times everything
what about empty set times bottom vs.
bottom bottom well you know you can
place the first bottom with an empty set
and so the thing on the left is more
defined than the thing on the right but
the next example is a little trickier
because it's not more defined than the
thing on the left sorry the empty set
times bottom is not more defined then
empty set times bottom times empty set
because you can't replace the bottom to
get empty set times bottom because
there's already in it empty set in that
position so you know basically what
we're doing is replacing the bottoms on
the right to see if we can get the thing
on the left and if we can't then it's
not more to fine then
and if it if we can then it is more to
find them so at the end of the day where
we kind of get is this picture this
partial order of the defined Earnest of
these terms so like bottom is the most
undefined bottom times bottom is a
little more defined these two terms left
and right there no more defined than
each other even though they have a term
that is in common I mean a term that if
both of them can define
that you know a term that inhabits both
of these partial definitions and so kind
of you know what we do in the correct by
construction process is we move from
less defined protocol specifications to
more defined protocol specifications we
have a kind of process of we say
something about the protocol that we
prove things about protocol so that
later when we continue to define the
protocol the things that we proved
continue to holds because all of the
later definitions are just a they're
just a refinement of the previous
definition you know so you know so the
the kind of theorems that we have for
less defined versions of the protocol
spec are going to hold for more defined
versions of the spec and this kind of
starts to make you feel why we have like
this correct by construction protocol
design because at some point we're gonna
have a partial spec and some proofs and
then there's no way for us to define
that spec more that will kill those
proofs so basically like our kind of
strategies to like deliberately give and
Peru or give partial specifications and
prove things about partial
specifications so that we can have a lot
of flexibility in our iteration and
design because we can continue to define
from that point in many different
directions without having to worry and
go back about you know verifying and
changing proofs that you know because of
the change in the protocol so like a lot
of the time when you have a protocol and
you make a change you're gonna have to
like change the proofs that you have
about protocol but if you instead has
some partial definition of the protocol
that you had two proofs from which you
could change and you can make your
change to your protocol by just read
continuing to define the protocol just
like in a different way from before then
you can you know not have this
additional proof obligation because you
just have proven it for a much broader
class of things which are kind of the
things that inhabit this less well
specified definition of the protocol so
let's so you know I think we can get a
lot of flexibility in design
because we because of this because of
this approach i so here is some actual
like partial order of defining this in
like some definitions that we have in
the casper cbc casper world so we have
this minimal cbc casper family of
protocols which is like the
specification it's like the easiest to
understand the smallest the few fewest
parts and we defined terms in that
specification to define like the binary
consensus for all the block chain
consensus protocol and other cuz it's
protocols that you've seen if you've
watched me present on cbc casper over
the years and so all of these protocols
these three protocols the binary
consensus protocol the integer and the
friendly ghost they're all more defined
than the minimal CBC casper
specification and they all satisfy the
same proof as the minimal CBC caste
respect and these these all therefore we
kind of benefit from that proof and we
don't need to look back much when we do
when we're defining forward from this
minimal CBC Casper family we don't need
to look back and ask about what that
proof will continue to be satisfied but
you know this this this family of
protocols actually has a full note
condition it requires that all the
messages all the nodes processes all the
justifications of all their messages and
so that's actually not super useful for
example for sharding and so we don't
actually want to have to define sharding
as a further definition of this
specification because it's a full it
requires it's full note condition and so
actually what we do instead is we have
like this other spec which is like this
like client spec which you know where
clients don't need to have all of the
just all of the resolve all the pointers
and all their messages and so we and we
define the started watching says
protocol spec as an instance of this
like CB light client CBC family
protocols which all satisfy the same
because that's a safety proof and
actually there's like a more abstract
family of protocols which is you know
considerably harder to communicate than
the minimal one but which is less
defined than both the light client
protocol and the minimal CBC Casper
protocol and so like if we with with
this kind of set up what we think what
this does is it gives us a little
roadmap of like starting from where like
what is defined and what properties do
you have and if you go downstream from
there and continue to find stuff you
know what would you get to benefit from
and so it can be really you know I think
this kind of notion of a disorder of
define Innes and of progressively giving
more and more defined protocol
specifications is very very very very
much what we're doing in correct by
construction protocol design because
we're engaged in the process of defining
something and we start we don't have a
full definition but we want to get to a
point where we do have a definition that
satisfies certain properties and we want
to know that the process that which we
follow will guarantee that we have those
properties and so you know which we try
to have it's kind of a disciplined
approach for getting them one step at a
time
and where we don't really have to look
back so but you know it's not always as
straightforward sometimes we have like
alternative choices of what how exactly
to define stuff and even to get the same
goal so it's you know I painted a pretty
simple picture but the reality is more
complex for example for validated
rotation the easy thing to do in terms
of the protocol specification and the
proof obligations is to just launch lots
of instances of these protocols that
have new validator sets and that really
can work in some cases but there are
also cases where we want to define
protocols that do validate a rotation in
a way that is outside of the minimal CBC
Casper framework
and whenever we do this kind of design
that's outside of the of the framework
we need to do we create new proof
obligations and so we sometimes have to
have a choice between you know do we do
we design things and way to take
advantage of existing proofs or do we
come up with a new system on a broader
family that
or that have other proofs and it's it's
it's tricky because like on the one hand
we want to benefit from other folks we
already have and we're gonna make any
new ones on the other hand when we have
when we can generalize stuff sometimes
we can generalize it a little bit and
not as much as we'd like and so if I
come up with a more general family of
protocols for doing validated rotation
for example like I haven't come up with
one that really does everything I want
and so there's there's there's there's
definitely it definitely isn't as simple
as like you know define as you go and
everything will be fine there's real
choices that we need to make and like in
the design process so one of the
decisions we've made for example is that
validator strategies are not part of the
specification I would like the core core
like the you know the core partial spec
is only for clients it's like not the
spec for miners or for people who make
messages as people for people who
receive them and and the reason why we
did this is because there's like kind of
it separates out the parts of the
protocol in a way that allows us to
tackle them separately and we can like
independent of when validators make
messages or how validators make messages
show consensus safety so we have this
big part of this the protocol of like
when do you know it's make messages
which is not defined in the course back
which both seems weird because you'd
expect that to be part of the consensus
protocol but it also is really nice
because there's nothing that there's no
way that that term could be defined in a
way that disrupts the proofs in the for
the like client protocol and so
validated strategies are not in the core
the core partial protocol spec and I and
that was like one of the decisions we
made and deaf I definitely don't regret
it at all we have a bunch of design
decisions that are motivated by economic
thinking but also at the same time we
leave incentives undefined until very
late in the game because the incentives
have to respond to the actual states of
the protocol and the actual and
you know the consensus protocol itself
and so you can't actually define the
incentives until the consensus protocol
is defined and so although we do a lot
of thinking economic thing in front and
we come up with a lot of disturb you
systems properties that we want based on
the economic thinking the and the the
the the definition is of the incentives
is left for later so you know we have
the the fault tolerance threshold is not
specified in the protocol there's like a
decision we made and like very like you
know like it was not an arbitrary
decision and was like was motivated by
like the design requirements that we
have and we have and this is and and
this is like an area where it's not in
the core reference spec but we have a
proof for how noes use would use it with
different fault tolerance thresholds and
so we can without changing the core spec
very much give proofs for a new kind of
use of the protocol so you know more
kind of weird proof tactics around you
know using multiple instances of this
like correct by construction core
protocols partial spec you know we have
preventing das will require like you
know that we bound the amount of work
required to process a message and that
people have throttling for the amount of
messages that they can receive and so
that is that's good that requires a new
constraint on consensus messages it
requires new strategies for the
validators none of this stuff is part of
the core protocol spec none of it is
part of the minimal you know core piece
of the like you know those like the
start of the correct by construction
process and all of that is kind of very
deliberate because the idea is that we
can define this stuff later
and it's more than fine because we
didn't screw it up by defining it
earlier so so the the the the other kind
of you know really cool thing about the
crack by construction approaches the
fact that you can iterate actually quite
quickly
without having because you don't have to
reason about much of the protocol when
you make changes you because you
literally could not define it it in a
way that screws it up and so we show you
some of the progress we've made in the
last little little few months on some of
the charting stuff so this is what came
out of the East Berlin hackathon we came
up with like a pair of shards one of
which kind of follows the other one
there's very it's very similar to the
traditional CBC cast burkas protocol in
the sense that like it's you know it's
really implemented
completely as just a definition and a
further definition that protocol by
giving the consensus values and the
estimators and the validators and their
weights and the fault on a threshold so
so so we did this binary so we said we
did this to two shard system and one
thing that we kind of have been wanting
to do for a while that finally kind of
got to implementing is you know I mean
just like a few months like there's a
really short order is shard rotation so
like here what we see is two shards that
are changing position one of them is the
route at first and then it changes and
then the other one is the route and then
it changes again and the other one is
the route so the purple blocks there are
route blocks the yellow blocks are child
locks and the roles of these shards and
the hierarchical census are changing and
this does not require that we reason
about consensus safety at all because
the the correct by construction process
kind of guarantees that I with no
thought because it's kind of upstream
from our definition process and so
relatively little work compared to
normally working Contessa's protocols we
define this like actually relatively
complex because it's protocol there like
this comes to consensus on you know the
state of two shards with locks that have
like two different positions and have
like a relatively complicated fork
choice role and here's like an the kind
of next kind of conclusion of that is
like oh look when we have two shards
that can send messages we can do routing
we can move shards around in two
positions we can move short
rounded more and then we have this you
know pretty cool sharding solution where
we have messages being routed around
cross yards and with like the atomicity
property that if your route isn't fully
completed then the block that started
that route will be orphaned so we have
like you know a really kind of strong
ability to iterate very quickly because
of the correct by construction approach
because we don't need to look back at
the previous guarantees we're not at
risk of disrupting them and so the you
know I'm never walking through this
again so this so so what's gonna happen
here is first the the route chart was
initially 0 now is switching to one
these messages are being routed from
chars 6 to 3 and back charged shard 0
and one switched from 0 1 to like 1 0
and then and then back and then shard 3
became a child to start for even though
it was previously a sibling and then
messages start to get routed through
shard for after that swap so it's really
kind of quite complicated we have like
routing tables and they're updating and
but we really didn't need to think about
consensus protocol is almost at all
whilst us find this thing so you know we
have thank you
so we have like methodology that lets us
define consensus protocols we've defined
a large number of consensus protocols or
partially defined a large number of
consensus protocols and you know and we
iterate while creating minimal proof
obligations and we are able to mix and
match kind of a lot and you know so I
recommend that you try out you know
correct by construction and we sorry I'm
looking at the wrong slide here got
ahead of myself that was the next slide
so we basically really rely on these
partial specifications and you know the
fact that it's not defined yet is
actually a huge asset for us the fact
that we leave things undefined until you
know the latest possible moment means
that we have as much flexibility as
possible to iterate without disrupting
our previous proofs so all right you
said all this yes it's it's great try it
correct by construction protocol design
it's awesome so now let's moving to the
like kind of announcement section of the
talk so that was that was like oh that
was pretty much all of the all of the
content so we have some a bunch of a
bunch of announcements of people like
you know contributing to a CBC Kasper
research this is a brog ham rock from
true level built a generative testing
for CBC caster protocols I'm gonna let
see if I can and then with this spoiler
alert so with this what this kind of
shows here is a the the red the red dots
are members of a clique which are
validators who see each other agree in a
way that they are actually finalizing
that block the blue one down there and
this is something you know related to
the way that finality works in in in
Casper and and and here we see like
multiple views of the protocol from the
point view for different validators
until one of them finds a decision on
this block namely finalizing you know
this this blue block and the the green
dots are the messages from the validator
whose view
and the red dots are the click which I
was like a group of validators who sees
each other agree in a certain way that
corresponds to a because that's a
signature that you know is like a
decision so so that's pretty cool stuff
you know that I mentioned the charting
proof of concept we've been working on
this but like I look significant like
rotating group of people since the
Berlin hackathon and actually before
that at the etherium ic3 workshop we
worked on the specification especially
want to give a shout out to Alex Keaton
off who in the last like you know week
and also during the East San Francisco
hackathon put in like heroic efforts to
get the grouting working and the shard
swapping I mean he's the first guy he's
the first person to prototype the cross
shard message routing bit jealous but
you know you should check out this
github repo and see if you like it and
it's not there's still loads of bugs but
there's you know it's definitely
interesting
Aditya who is probably somewhere here
has announced that he's implementing a
shortened client with like you know
they're in blocks and like you know very
like aetherium starting client and he
has a github repo and that Twitter
handle he should follow him for his work
we this is a exciting one we kind of
released a draft or are going to release
a draft I wrote these slides I thought
we'd have it released by now but we're
gonna release a draft today of oh wait
it is released my bad github calm slash
CBC Kasper and you can download a new
specification of the minimal CBC Kasper
of protocol states that is you know
extremely rigorous and pedantic with
extremely rigorous and pedantic proof of
the consensus safety result and example
protocols including the Friendly Ghost a
finality gadget a sharding with fixed
hierarchy and I'd like to thank the code
my co-author is Nate rush Aditya and
Georgio's and they're all here you you
should you can probably recognize them
from their faces
I put a GES face was on the previous
slide finally you know don't forget
about the prototype in the wiki at dairy
m / TVC - Casper these are like good
resources if you want to like dip your
toes and check it out
you know we're totally looking for help
of all kinds and we're getting better
and better at helping you help us as
they're like documentation and
definitions and stuff have laid
themselves out in a way where you can
you know come in and contribute in a way
where it's really clear how it
interfaces with everyone else's work and
where you know you won't be wasting your
time and you will be helping so you
don't reach out and thanks so much for
listening
I have time for one question it's okay
you don't need to ask a question I can
just go by everyone oh wait there's a
question sorry sorry sorry
do you have a microphone so what's the
deal there the microphones are at the
front you have to come come over to the
front
we got like 30 seconds you got to be
quick 10 second question 20 second
answer yeah can you hear me good what's
a good way of really understanding CBC
if you come from a math background yes
read this paper and anything anything
more sort of high-level just know the
paper is really good it's just that it's
set theory okay it's very accessible I
think okay
you
[Applause]
you