[Applause]
but it doesn't matter because I've
waited for many minutes okay so we're
talking about later today I look like
about particularly something which is
difficult the obligatory machine now
when most people think of a virtual
machine they think of stacks and
registers and all these other things and
I got a incredibly advanced computer
scientist so I think I can make an
argument that this thing's a virtual
machine but usually when I say oh yeah
I'm can we do something else so actually
we're gonna be talking about today is
one particular subset called optimistic
semantics and basically the idea is
what's going on with this layer two and
how can we try to bring it under your
sort of more unified I'm well what's up
guys we're unified umbrella okay so what
are we gonna talk about today first
thing we're gonna do is we're gonna
spend some time bisecting what layer two
is today and sort of looking at how it
functions and what are the conversation
the next thing we're going to do is we
are going to take all the components
that we use in trying to describe layer
two and talk about how we should try to
use those to build the layer two
okay and the last thing here which pema
this is really an agenda point but it's
something that i want is i do not know
how to finish these slides okay so the
reason that this is like not a video
that is on our website or being posted
on our twitter is because of you guys
this means is that there's no point in
us having this here unless people ask
questions and engage okay so before I go
forward I'm not going to say no word
until I ask the question do you feel
like perfect you optimistic about like
audience participation
[Music]
to optimistic is like supply okay great
okay I let so let's gonna make this a
little bit so we have a later - later -
is popping you could even say it's a any
brilliant explosion okay it's under the
sex building I think to quote me about
my really big plan do very very simple
payment channels a bitcoin then we have
a lightning power come out in 2015 then
we started seeing more different state
channels design sprites virtual channels
generalize channels right we start
because a true bit that I and I come
from a background of plasma and plasma
is perhaps the most exciting but also
guilty printing huge amounts of diverse
designs and varying implementations this
is a place small selection of the code
plasma flavors that we have in the
classroom design world I mean even worse
I'll be company you other incredible
things happening we've got roll-ups the
optimistic flavor and the CK flavor no
cuz it's a commit chain which is
basically possible that is why cultures
possibly because they're not plasma our
maturity was in the room with another
better version of two of it right
there's lots and lots of exams use
coming about right so this is wonderful
as a research in this very exciting as a
user who wants we didn't get the big
simulator to this is very exciting but
it's not like all of these ideas are
totally unique right at the end of the
day most step or I'll go all around one
thing and that is this notion of
disputes right usually something happens
on the off main chain and then someone
claims something happen on the main
chain and then someone else disputes
them about it right
sort of the basis based things that
happens and what we see a lot of papers
completely reinvent this real right so
these are you know layer 2 protocol
admin and layer 2 protocol head plus one
this is like often sort of you know what
we get in this ingest of course you know
citations are very important and
everyone's standing on the shoulders of
giants
but everything uses disputes this is the
point ok I think I realized is that the
sort of meme of one helps you can rule
them all up and out outside view the
Bitcoin world because unfortunately only
lightning is really possible on Bitcoin
this is a lie this is just a plain line
ok what we see is the different layer
two designs are built for different
applications they're built for different
use cases so what we need to say see is
not one l2 the global but like you know
sand well Jesus shaking hands and
interoperating because the reality users
are going to want you some many such
applications the layers you can provide
but it's not going to be just one that
gives it to them that's not to say that
we're gonna have you know thousands
perhaps but it was probably on more than
one ok so I have not any questions now
something's composite off and they've
got the questions cuz I would agree with
this ain't hot tanks then gonna prove me
wrong there's only one L to rule them
all concert in all to death no okay good
that's what I do here so let's try to
understand a bit about what layer to
really is okay so like in a high-level I
think there's like four pretty distinct
things that go into layer two
okay four steps if you were so the one
thing that you do is you check the
blockchain see where
DEFCON so I'll say three check the
blockades to state see what's going on
right now right the next thing that you
do and this is the sort of layer apart
the second layer is you get some local
information and you look at it observe
it right the third thing that you do is
you make some kind of an assumption
right so this is usually of the form I
will dispute things and we'll be talking
about that a lot here but there's lots
of different assumptions you can name
then the last thing you do is you make
some prediction about future l2 state so
what I have you know two coins in a
channel what this means as I believe in
the future I will be able to withdraw
two coins from the channel it's not
really anything other than that okay
that's so like an example of this or
seychelles I see on check verify these
an n-channel which is usually doesn't
involve a multi-sig i see that i've only
size science of a certain state usually
the one with the highest nonce right and
you're sort of traditional aetherium
style and channel i make the assumption
that if someone tries to drop an older
state I'm gonna go in to bring that
state forward and dispute it and they
saw that loads through things I can make
an assumption based on that of course
something that I will be able to
withdraw according to the state s okay
does that make sense to everyone
questions comments concerns okay I'm
going to need questions at some point so
you guys good luck love okay great so we
have some fun you know some fun
formalizations that we can make around
this which are very reminiscent of like
things of the CBC future so here's the
interior watching right so here like the
universe or the
and based on that sit there's some
subset on the next blocks that come up
here right these are here and based on
the details of the um you know maybe you
can't unlearn money for example if you
set up the zero address it can't come
back but it can be sent to this your
address if it hasn't already so here's
somebody being burned and now you know
that these states are no longer possible
because this is the one that just got
mine right and so he beyond you know
consensus algorithm that we call a
theory in themselves and either is
progressing through this futurist cover
of the material right which is say sort
of borrowed from physics you know for
all that the mean is not giving that
goes into it and this is what we're
doing right so this is one thing that
happens what's the only thing that
happens the other thing that happens is
we have this local information write us
about our passing things around
signatures inclusion proofs we've got
local information to yeah it's off chain
right okay the last thing that we do is
we make some assumptions right so the
EDM set that says that some set of
future states are possible right this is
a pretty large set and what I do as
someone who's trying to make a
prediction about future el Tuesday is if
I make an additional assumption that is
not inherent to the EDM okay so here
imagine sort of to force of the botching
right so so imagine that we're at a
state right here and someone it
maliciously tries to withdraw some money
okay I will assume if I have a channel
talents and I'm trusting that I have a
channel balance that it's so put in the
future this thing will get disputed
right so what that means is basically
what entities I'm looking at any such
chain that where no disputes have
occurred and I say I don't believe that
this is going
happen it's an assumption it's an
additional quality of the statement and
it's an assumption that you make the
valid mistake right so we can find those
two things we did something like this
right you have the finalized box that we
saw before right behind me we have the
same as here in futures comes before but
now based on this layer right so these
things which are possible a part of
India are no longer possible according
to my assumptions because I believe that
I'm going to do something about them
that's usually the assumption right and
this is what we see and furthermore one
of the things that gives us the great
scalability I etherion is that these
this pump does not just restrict as
newbucks about it actually restricts as
messages are passed around so if I get a
new message and it tells me I can do a
new to speak this narrows in the code of
future states that I'm assuming are
possible so we can call this our
optimistic futures okay with me so far
yes not excellent questions I got a
question yes castle there you go
why can we assume that that's going to
be missed
it's content but lightning is that
someone doesn't have an outside
motivation not to result
correct say ah so that's a great
question and so you know extra protocol
incentives I talked a lot about even
later on and certainly in layer 2 and
they're not to bury a research and we
need to continue researching these
things in general however we we believe
this because we think that black chicks
are meant to be sensitive system so
usually in layer 2 we use the properties
that we're assuming that l1 fulfills to
make our assumptions sound reasonable so
you go through the work world right we
have this decentralized Network where
anyone can start you know bringing some
electricity to my nook and because
anyone of the world is going to do that
I have my fingers crossed that in the
next you know whatever the dispute
period as the blocks are at least one of
those people aren't had to be willing to
accept my transaction now that's not we
said that there aren't like important
nuances to be analysed here
so one one-line critical example of this
that we have to be careful about is what
if the dispute to keep my money safe
cost me more money than the dispute
itself cost me more money that this fees
can get you right so that happens we're
in trouble so we want to be careful and
design the protocols carefully so that
the the assumptions of makers reasonable
as possible and ask another question you
that was one nightmare over
that looks like it is not fit to be more
but in this Dominica oh what a swell a
segue what a segue is this mystery -
you're totally right so unfortunately we
can't just write a computer program that
does a four loop over all the future if
you're in states that are possible it
checks whether the analyzer assumptions
this is computationally infeasible right
so this is a great tool into when we
describe so far it's a great framework a
great model for describing how there are
two protocols that existant work but
you're right that it's not really useful
in constructing some sort of layer two
client that is like unified or magically
combined everything in one way because
this is a very very large set in fact
infinite now maybe with the gas limited
like the fact that there's only so many
bytes it's like actually kind of finite
but there's like way more atoms would
you know way more than atoms in the
universe worth of these things right
yeah so exactly right so what we've been
doing here is we've been looking at
later to write this framework that we
just talked about is a way that you look
at layer two systems it is not however
Granick that's useful in a building a
layer two systems right but so this is
what we really want to do right at the
end of the day research should be going
to fight motivated by actionable things
and what we really want is to be able to
build a layer two protocols in some
framework that extends beyond you know a
particular plasma researcher who has
intuitions for plasma does and a
particular channels regions researcher
has emissions for channels two and so on
and so forth
we want to try to unify this under one
sort of shared frame right so we want
like when I like to think about dispute
Legos right we want some way to
contextualize and instead of replacing
so like a plasma for example we're
feeling very guilty of this we have like
limo swaps and about
and you know the job isn't all these
things I think very very useful for us
as possible researchers to be able to
talk to each other but they're not good
what if you want to bring someone you
want bored because we have to teach them
all of this stuff right and what the
people who want to be fun to do
understand is like logic and math and
models rain so we want to be able to
push that and so that's what we sort of
the goal of what we're going to do here
today great question great question so
we want to be able to build things
because the space is just too large it's
basically infinite you know for all
intents and purposes right this is too
big to compute here we go I wish you'd
asked at once laminator on/off switch we
really wanted to put this slide earlier
but you're exactly right right so we
want something that is easier to cute
but we also want something that is
flexible enough to go the protocol right
so for example there's a layer 2
protocol that says I can burn all of my
money whenever I want and of course once
it's burnt you're never going to go back
from a B number this is a very useful
protocol right so we want somewhere in
the middle between the spectrum of just
like before leaping over alternative
boxes can be done without you know
magically infinite computer and
something that's actually useful so
that's what I'm gonna try to pull out
here today ok other questions other
questions all right so let's talk about
some hits
ok I pulled these from a couple of
different layer to sort of the science
and protocols so in the other right here
upper right here we have some
localization this wrote a paper called
note costly to commit chance very
similar to plasma so they have a whole
have this notion of local information
right it's the same thing that we were
talking about before a few slides back
on what we call the high logo they're
using that in their paper boom ok now
there's another there's another hint
that I'd like to share
which is from the generalized state
channels paper so great they work by the
counterfactual team which is now been
unified across almost all state channels
porphyria this is very safe there's a
for all here okay I like for alts and
you'll see I mean talk about for all's a
lot for the rest of these slides so
there's another hint for all so here's
one from my coworker my challenges this
world has no paper and there is no sir
no challenges right it seems like
decisions are primarily based on
challenges one person says one thing and
other challenges it with another and it
more advanced protocols we even have
several layers of challenges where maybe
one guy says one thing and another guy
challenges and then the guy respond the
first that responds again okay so here
are some sort of these these are what I
think are hints that will sort of lead
us to being able to construct something
very useful ok that makes sense
questions there ok everyone has a TOC
slide that talks all hi mind you one of
the word that I love from history which
on the island I guess I'll read it not
to insult you all without a little
Bachchan organizations have to move
existence it's group of in existence the
ability prove the message and see what
and all answer depends beside other
messages sunshine has not been published
yet so this is very often a property
that we see in our LG protocols
someone makes a challenge and there is a
possible response that could be made but
after some time out that response isn't
me and we take that as to say well this
must be the response doesn't exist
ok and so existence particularly is the
word here I want to pull out so we've
seen some challenges you've seen some
for all's and we've seen existence and
it turns out that there is something
that has a lot of those same words ok so
it's most first-order logic right this
is your answer Lawrence or not this is
her for all's and your exists so what
we're going to go through them in the
rest of this is we're
to look at this within the context of
layer two right so we looked at this for
a while and it was very interesting to
us as researchers that there were sort
of analogies here and we came up and
tried to come up with some designs for
how this could be sort of integrated
into altitude from fact in practice took
us to ultra it took us a while to hit
one that we thought was pretty solid but
a big big key moment that helped us
understand this was response I called
dialogical logic okay this is related to
the broader Kill Bill game semantics and
I started this talk by saying game
semantics right so dialogical logic is
an interpretation of these first order
logic sort of expressions and in
evaluating whether the truths are
possible by interpreting each expression
as a game and then interprets truth of
this expression as the existence of a
winning or losing strategy for the
equivalent game okay so this is very
interesting and just for context of
semantics it took me a long time to
figure out semantics methods are not
really you know I've never taken a
semantic score sir so semantics is like
meaning like so first-order logic like
there's actually lots of logics which
are sort of satisfied by the language
that uses for all and this ranking so
these are very important by the way so
remember the outside that a is like for
all of the I don't know line for those I
already knew the backwards to use exist
like this one just like inverted letters
what's up otherwise they so so it's
worth understanding that there are
different semantics okay
for the same sort of language of persona
logic okay so next I simply example this
is like classical logic is the one that
you learn in logic 101 is what I wants
mirror with and this is this you know
where you can prove something like true
or false right
there's also called intuitionistic logic
which in turn size does not it was like
philosophers arguing about logic it's
saying we don't like this thing called
the law of excluded middle so in
classical logic for any proposition P
you can say P or not P right you can end
them that that's decided to be true
sounds reasonable rights leads to true
or its false but apparently these
phosphor guys will have aluminum can
begin secured files like maybe something
not right and so intuitionistic logic is
like a version of logic which removes
the ability to say room or the R P or
not P ok so these are semantics
depending on how you interpret what the
language means these are called
semantics and so we one of one of these
for layer two so we're gonna call out
optimistic game semantics because
basically the way the layer to the
scales is you might give you an
optimistic property and assume that
everyone's going to play long and so the
blockchain has to process less
information for the total computation
that went into the state machine that
was running off chain of day that was
making these optimistic decisions okay
so that was a lot so I hope that we have
some questions at this point time
ah so that's them the rest of the
presentation give you a simple example
okay so illogical was it on this later
but in logic they're these things called
atomic predicate okay so it's very
simple atomic predicate slickness
right right like you know one equals two
is either true or false I think it's
false yes and so on and so forth so here
just gives another example of an atomic
try to hit okay verify signature okay
this is another example of an accredited
okay so in state channels what is a
state channel well you could build a
state channel out a multi-state and
thankfully the cleanest multi-sensor
this is likely going to be two channels
so here here's an example an intuition
for how we're going to bistec there's a
you can write a function to verify
multi-sig right this is a time try to
get that verifies a multi-sig so let's
say there's like some participants right
I'm gonna call these PT PS because I'm a
to get writing okay so let's say there's
like five participants right we can
write a verify right multi-sig
right which takes in the participants
right SIG's right a message being signed
right okay so this is another table of
atomic predator right I think that value
isn't your fault would it be nice if
it's something to redefine this thing we
could say for all P in participants
verify sick right okay so maybe
hopefully that's an instructive example
so the idea that we're trying to do here
is we're trying to pull out these sort
of very very like very large your
monstrosity Frankenstein layer to
solutions where we have to write a bunch
of custom things like this and try to
like convince them down into a
composition of these logical statements
okay so we want say for all to the P in
participants verifying the sync of that
individual P and so this allows you do
not like a verify sit and a verify
multi-city
you just write a verify see so they
hopefully that's hopefully time great
other questions the logic you talking
about is strategy a winning strategy
listen even for a game what does that
mean okay so I'll get into that and so
maybe I'll just try to provide an
intuition now because I'll have an
actual like game tree example soon but
what that means is we take the logical
expression and we convert it into a game
tree okay
I'm Tilly let me actually let me let me
go let me go on the side so here I wish
you to switch to this slide immediately
because this is within the answer in the
first question here are some intuitions
for lettuces
there does not exist
such that this is an example interesting
layer to eat and logical composition
right for a lot such that the signature
satisfies x and y right be honest this
is this logical connective and yet you
have to be really careful about there
does not exist a signature in systems
like this because there exists a
signature right there is some string
admits that's a valid signature
absolutely so this is a great question
and not to just illogical omniscience
this is the problem that we face so in
theory all Caesars is just in theory
late from a lot of perspective all hash
functions have an unlimited number of
preimages that satisfy the given hash
right so we're going to talk about how
to solve that problem and one of the
important future works that I hope will
take I can get out of someone in this
audience is to do a much better job
analyzing that than I can because I did
a big bad job and there's some minimal
approach to be able to get this thing
out there okay okay yes so we're very
careful about how we construct these
things but we're doing it in layer 2 is
anyway so it's really just thing that's
been careful about how we do it in layer
2 but again this is an important
distinction so even though even within
the sava logical interpretation right a
semantics there is a semantics for like
the love a bit like precise logical
expression that says that this is always
true because like all signatures exist
out there there's always a string in
place but we're going to provide a
semantics an interpretation the logic in
which this can sometimes be false namely
if I haven't said that signature to
anyone else so right I mean one of the
standard approaches is to talk about a
party having knowledge of a signature
correct right which is a different kind
of statement correct so so so there are
lots of approaches to knowledge so I I
went down a long rabbit hole on this and
cycled Kripke semantics which which
defines us in the worlds W you'll see
something borrowed from that here in
these slides
defines an accessibility relational way
to progress through world a world is
successful if it's in the
we want to talk about temporal logic to
do with time and and there's one for
knowledge as well and so on and so forth
um we're not going to give a rigorous
treatment of that here well we're going
to talk about today is just the first
step in sort of in sort of formalized
novell - which is let's just look at the
games let's just look at the games and
so we'll do a very simple crappy job of
the knowledge that is not rigorous and I
don't think you could prove hopefully
there's someone here or at DEFCON that I
will be able to talk to that knows more
about University's ability and these
computability assumptions that's gonna
be able to inform me much better than I
have I have so long I'm lucky enough to
see a few of those spaces in the crowd
and there's definitely more to speak -
so one of the one of the goals of this
work is to be able to pass that part off
to someone else who can do this much
better than I can't because I you know I
you know there's only so much time in a
day and I can't but I can
I can train home okay so other questions
excuse me I should not have done that
yet other questions again the goal is to
not go through these slides guys I'm
telling you guys what is the successful
stay here so ask for it ask away
okay but no questions so let's get into
it okay
so let's define this language Duncan
worked with okay it's very simple for
sort of language okay these sides are
called quantifiers okay this guy's for
all the upside down hanging inverted
angry - its mirror
you know this is your 4 L also known as
universal and complication this is for
ahlet's and sort of the universal this
is exist it's called the dual of Porto
is existential quantification so for all
right so we actually when we write this
in practice when you write something
like for all X in an X ok
I only write exist X in X right and then
we say this is like it such that another
like some T of X right some P of X now
they have notably in most logics the
these two parts the duals of each other
so not so this is this stuff is good we
are not by the way so not for all not is
the same thing as exists and not exist
that is the same thing as well ok so
that's just who she anyway so then we're
also going to use and ok so you're sort
of upside down V or you know I'm free to
be whatever is we've got the same
problems in Reverse upon a fire this is
your aunt
this is or not this is your war ok good
make sense yes yes ok excellent
ok so I'm going to briefly talk about
simplifications that we will use within
this language so there are these I
repeat over there that was a quiz
natural so P and P sub 0 and P sub 1 are
going to be our our summons for a
generic proposition okay so this is any
expression in this language which
evaluates to true or false
ok I think that means it's closed so
there's no variable floating around in
there all the grandmas or mobile pod and
it's well-formed ok you know you know
the street not not was nothing after it
is not well
composition it's just like this we're
vacuous statement that has no memory
tonight yeah okay
now along with with compositions we also
have formulas okay which accept as an
input some variable so for example x
equals 5 is an example of a P of X right
P of X you know that's re X greater than
5 and this example of a formula because
you can plug in different actions that
will be true or false and they're free
in X right in cents a room excellent
okay and I'm going to use a script
notation for P of T so this is a little
tricky but what we're doing here is
we're plugging in 2 for X okay so right
there any more consumers and I can
scream onstage but for example for the P
of X X greater than 5 P of X / 10 would
be 10 greater than 5 right which would
happen to be true right good make sense
make sense questions comments concerns
school education is just the particular
evaluation of PD where X is equal to
correct it's a particularly you plug in
in your summary actually it's very hard
to see fun yes okay okay well apologies
for that please shout out if you can't
see things and we will whiteboard them
where I will go out of full screen and
zoom in or whatever to make yes exactly
so in fact why don't I just no need to
do that
so P of X can you can you read that
maybe that's the same exact size oh okay
so we've got some peanuts if so to DMX
let's say P of X we've defined it with a
dot dot equals this thing is x5 then you
know P of X which directions they can
slash given X / 10 would you know would
be would be equivalent to 10 greater
than 5 okay so we have X is free here
and now 10 has been subsidence of
impress okay excellent excellent
[Music]
the very right absolutely yeah I'm sorry
it's this tough life or is this okay
yes well let's read let's read it out
loud so there's actually two there's
actually something just outlined in
Section two so are even today as a
batsman who the straining yes so this
expression read analysis for all X and X
so X look little X in big ax right so
this is the set the domain of
quantification few days okay and this
says there exists X in X such that P of
X okay right and so what we will see
right well one up seeing is we're going
to be we're gonna start building up
disputes or sentences for all X in P of
X so we also can say I have this X and
I'm playing not to P slash but you know
whatever the special cases they're that
they're kind of discouraged I just
okay okay other questions excellent and
how are we doing on time oh great I
don't think we'll finish it's been
touched
where do we get out here 3:15 no okay
let's call it 350 okay and then the last
thing that we're going to cover in this
language which remember we touched on
the floor you've got a target
proposition so if the other things too
small this is definitely small but it
was like what's a simple atomic
proposition in equals so actually that's
a bit of a lie equals is that it's like
really connected so really five equals
ten
that's an atomic proposition and
evaluates to false right but but things
worthy where both sides of the equals
are filled they come an atomic
proposition greater than there's no
example right less then there's another
table okay I know there's there's three
in particular which are very interesting
to us building layer two things which is
is this thing the hash tag image so it's
this little H the hash English to this
big age which basically is equivalent to
saying hash of blue H equals H right
these are the these are these are these
two atomic propositions
well we have lights turn off right
okay and otherwise verify signature
right so we're all familiar with
signatures in the Wild West of
cryptocurrency which is a very fun
actually you can build a signature of
the hash function it turns out Lamport
Leslie I'm quickly at night and the last
thing verify inclusion what they were to
verify inclusion of the thing ever
this of all the functions that are
evaluated to true or false the coming
position any function you can imagine so
I have only has it my intuitive answer
is yes and I think intuitively you
should think of this is no no actually
okay so no literally
the important thing is that it is free
of these logical connectives ok so if
you have some fans and some nonsense
ores or some quantifiers
this isn't so a and B where they are two
atomic propositions is not a prominent
that might be breaking it's possible I'm
not a super super deep logicians it's
possible or that that's broken but
that's how I think about it well the big
one that's that that is makes it an odd
proposition is the not happy for all it
exists right not having classification
that's that's that ends up being the big
one yeah great question great question
so anything that arrives at your Falls
as a composition an atomic proposition
is one that doesn't have many of these
these bad boys Americans these are sort
of indicators that there's more logical
structure beyond just some sort of
simple function evaluation the reason
for the consistent use of language we're
like I mean the atomic propositions like
is equals who is has payment for all
semenya instead of like that is valid
signature you have my very time
signature which stuff but it's certainly
my accent inside the Great Hall
so I dunno I should I should
paper to have more consistency there
yeah and I was actually the most
egregious I had to say the initially
reported breaches in consistency than
that
which is that I shouldn't have in the
parentheses here and you know signature
message punky and I should have you know
before inputs to verify between but
absolutely yeah so that is that my bad
my bad
but hopefully hopefully can see it the
point across yes are there quantifiers
you don't like because like if you're
considering like atomic binary values
those are like bullets like built it is
express like player I know with that
there exist age so that
and you're like saying like knowledge
you want to know the moment knowledge
people on fire yeah is that what you're
saying yeah so I this is why I decided
jam with you after this bi because
that's totally a dollar question so
there's like you can think of two layers
happening here okay so the layer that
we're going to covered mostly in all
these slides is the on shame layer okay
and there's there's a relationship to
option that's not as well defined off
chain is for on chain well we're doing
is we're just building the dispute games
that go on changes okay so what we're
gonna end up doing is going to try to
construct a contract that sort of
implements the ability to check the
truth or you know false evaluation of
these things so is there a more even
less classical logics than these ones my
knowledge or is your knowledge is
actually ends up being stuck want to
fire that that's absolutely right we're
gonna ignore that for now
well we'll treat that very simply block
will have something called computability
model it's not as well formed as has to
be like you know very very well
quantified but you're absolutely right
but for now for the intense purposes of
this all we're going to think about is
for all and exists and it should be
noted that there are many extensions
with semantics I'm going to come here
and so for instance the binary search
game which is the true that guys use
I've messed around with right here
that's and for all exist for all exist
but I'm not sure if it doesn't denote
its own on a fire or or we're connected
maybe do you want that okay other
questions before proceed
all right let's get to it so what we
want to do is we want to take these
expressions right things of you know the
performance under there and we want to
turn them into games okay this is our
goal we wanted to so these lateral
expressions we want to evaluate their
sort of truthiness whether they're true
or false in relation to some game okay
and eventually the goal is for this to
be a game played on chain it's going to
correspond to the dispute contract or
the deposit contract depending on what
layer 2 protocol developing mask so
we're good for now we're gonna talk
about two players we approve of key an
opponent oh okay that's not good and
summons a and B capital A and capital B
are going to be variable as representing
either the prover or their punt
so today is not equal to B but they
might be one of the other okay does that
make sense so very often we want to talk
about a player generically and we want
to talk about the the other player
generically some will call on a
microphone everyone do with that great
okay okay so these are the two people
that are playing this imaginary game and
this game again is our interpretation of
the logic it's what gives the semantics
the meaning to the logic that we're
gonna try to make him to player two
constructions through good great okay so
there's a game station
so a game stays a tuple of two things a
player remember a but he says either
this is either to prove the opponent but
we don't we don't care about this you at
this point we know this the defending
player okay
now the only thing here is the current
proposition you can also think of it as
the prophecies should be defended by the
defending player okay so this is a state
of the game okay so the game is
currently
in some position there's there's going
to be a defending player specify and in
current position specify right time to
just I'm good they're wrong
and what did I say here okay absolutely
say that somewhere is okay to the people
that that can't be
oh yeah so if you would speak we might
say that this games a just a sign that I
love this this is something that I found
in a lot of game semantics and logic so
an eighty science state is one in which
a is the defending player just just an
additional that I may or may not slip up
and use through the wrestlers
presentation okay that makes sense
everyone right pretty playful okay so
the next thing we gotta find now that we
know with the state of a game can be we
want to talk about how the state of a
game can progress right how does it move
through the iterations okay
the way that we're gonna do it
turn-based sequence of challenges okay
so this is gonna be one game state okay
and then something's gonna happen this
is to be the new game stand okay and
Sonny's gonna happen this is gonna be
the next game state okay okay that's
unreasonable everyone makes us right and
know that these are different
propositions okay so the I believe this
is p0 p1 and p2 right these are gonna be
different expressions make sense all
right
I always like we're between B what's
that always back and forth units always
but always turn this yeah always turn
this and one thing that's important to
illustrate here is that the semantics
and I'm going to find I know Sebastian
depending on me immediately after this
for saying a bunch of things that don't
reflect some of the nuances of things
like haqeeqat strategies
love you strange things in very
developing semantics but this is these
officials provided a this will be
sufficient to provide me some intuition
for why this is possible and what the
contract that we want to know what you
look like
alright so for our purposes for the
through the purposes a says something
these days now something else is not
something else something else and so on
yeah does that make sense
okay now we get the real meat and bones
okay this is like the bee's knees up
over to talk about here let's define the
rules from which a p0 goes to V V P 1 ok
so here are the rules rule number one
okay well first of all just talk about
how this table is ok so this is a game
state and now the opponents will be here
might might or might not have to make a
choice might have to make some provide
some input okay in this case they don't
and this is gonna be our new resulting
state ok so this is our this is our
thing if you love to pair up everything
to the right of zero and so we call
these challenge rules this is how the
games no progress in the steps make
sense okay so it's first shondrel it's
very very simple
this a is defending a statement of the
form of not P then B may challenge by
claiming P okay makes a lot of sense I
say that you know the the sky is not
blue and my opponent responds with well
in this kind of blue okay
makes sense
make more sense than they say it's B&V
said it's not because I say I have a
balance of 50 in peace if no he doesn't
great question so the reason that we
want to avoid that is because what we
want to do is we want to slowly take
these very complex expressions and
reduce them down so for example if a kid
say P and then you could say not P then
n could say Takaaki and then you could
say not not not T and then see if you
take not not P right and so all we're
doing is growing this leg logical
expression what we really wanted to make
the expression smaller because we want
to get down to something eventually that
we can evaluate on chain very easily so
that's a great question and intuitively
this makes sense because I plan a you
can play my game but what we want to do
is provide in such a way that these
games sort of reduce so the two lands of
the movies that great question great
question but here's the intuition is
there yeah I guess that the game can
transform in a way then if one person
says something the other person says
something else that disagrees so that's
exactly great intuition okay does this
rule makes sense
nice here's a final a a says p0 and p1
that I has a that that B has a choice D
may either XI 0 or 1 which is the left
of the a hat or the right of the end and
B says not P i okay so here's an example
of where not does get that bond
regularly produce me and into something
else right ok so hopefully that makes
sense it's very logical
today says the sky is blue and it is
raining then D they either say the sky
is not blue or it is not raining right
this is how this is how they respond and
so notably
everywhere to be here then the next then
this rule would apply right an a and B
are sort of switched out right but now
but now we would get these a over here
API over invited so this should give an
intuition for how these games are the
best right okay here's another one or
right so lord is something that are you
doing through the rapt estroux are the
right is true that it's true so what
happens in a cesspit 0 or P 1 then B has
to respond by saying not p 0 and not p 1
right so the only way for this statement
to sort of be false is if both of these
things are false because this is what
the order does is conjunction and
destruction there's thing like that any
budget right so does that make sense it
it's bigger ah this one is bigger so it
is bigger that's true but now it feeds
into this rule so right so so normally
like you know this this outcome has this
rule about it and this song is in that
this rule applied to it which will then
get that this rule applied to it so what
we'll find is that you've got this one
kind of looks a little bigger because
there's now two knots and a half as was
just one more eventually things will
would you stop will always get smaller
and smaller incisions around later
vision say that's a no he's not that you
didn't report our position yeah it's a
some intuitive reduction the goal is to
eventually around so we're just like
checking one signature right
so the verified multi-sig example that i
gave we want to say for all P plus the
participants right the great thing about
doing them all to see this way is you
can disprove the multiset not by
checking all the participants but by
simply providing the one that's not true
okay
and so this ends up being what happens a
lot in with being in layer two protocols
for example a plasma you make a rule
that says before all blocks less than
the line exiting from this condition is
satisfied would be very expensive and it
would break the scalability or system to
check all those blocks on chain but
instead you only check them into the
true ones that people decide to respond
to okay so here's here's a fun one okay
this is this one things maybe get a
little more hairier these are these are
pretty straightforward now we're gonna
throw in the two qualifiers the first
one we'll talk about is the existential
quantifier okay so there's a such fun
part let's just let's just read this
statement a is defending the proposition
there exists X such that P of X okay so
how do we respond to this the way that B
is a lot of respond to this is the same
uh-huh I disagreed for love of X not to
do this okay so this should make sense
so if I sing every day in the last year
there was a thing last year when it
rained okay so what else to response in
you know every day last year it did not
man okay
so hopefully hopefully that makes sense
it should be fairly intuitive and again
these are all very intuitive right we're
just providing a particular formulation
so that seems very obvious right there's
nothing very very hard what the
counterintuitive about these rules
okay so now we have the last one and as
well as the caption that you thought
that prior to the universal inspire and
this is this is oh this is a big one so
if a says 4 X P of X B may choose a
particular T and s and say not P of T
replaced in X or or if you replace the
protest ok so if a player a says it
rained every day last year player B can
say it did not rain on January 3rd of
last year right so the this seems very
important one is one of the things one
of the main things that gets us the
scalability of these solutions is that
oh the old we can evaluate whether
something is true for all of these
things with this dispute assumption by
simply only analyzing particular ones
that people are claiming it's not true
for so this is missing this is the
really between the meat and potatoes of
our scalability under this construction
yes could only be used to rules lead to
infinity challenges ah great question
all these will see different challenges
my gut says no I don't approve for you
so I won't say that absolutely but my
gut says no and I think that was I think
that would hold up and there's lots of
results so this is by the way I'm very
very close to stole this from this
dialogical logic things very very very
simplified logical logic and the
biological logic there are lots of
results that say that a shrimp I sub
antics that are very similar to the
structure and a few differences very
similar exactly correspond to things
like classical logic there's another
version that corresponds to
intuitionistic logic there's no that
corresponds to linear logic and all
these other in bubble I think there's
one for you dependent types because
gravity
types are also logic time
but I believe that there would be a
result I would say this rule introduced
and there would be a mention and when
you think about it they kind of make
sense these things are sort of getting
smaller and I don't see any place where
we would start looping through anything
sorry could you speak up over it sorry
new conditions need to thank wait they
so exists turns into a for all when a
floor off is not turning to exist of
world just gets rid of the four ball and
puts it not in front right so so so so
so maybe make I'll just do a profession
out okay so let's say someone says
exists X impacts and such that few
that's okay and let's say let's say it
says this and the next thing we would
have you would have be same for all X
and X you're next and I knew that a said
again they would pay particular team and
I would say not not of tuna
okay the particular images yeah so they
so the for all doesn't look back you to
exist so we're okay we're good we're
good
no internal loops as far as I can see
which the PT is not DT
than us so the middle one says let me
just read this off
he says a says there was a day last year
such that it rained B says for all days
last year it - not great day says it did
not not rain on January 12th of last
year okay the person that not not will
eventually resolve in the B st. not Pete
and then a sink as we respect it not not
reduces to Oh
screen height other questions like this
the challenge game below YouTube and
attracts like brings I believe someone
says that or all previous blogs the
statement April
and then the other guy said oh it
doesn't hold or below zero and they
never guy said no it closed for well
zero but the other guy said oh I
actually meant doesn't work for block
one that's great questions so just to
rehash that one can hear the question is
do we allow a sort of replays do we
allow to be allow if suddenly maybe some
guys those for all blocks some guy says
not for this block but really it was not
through this block and if we went back
through this block we might get stuck
down this wrong trail when the right
trail is over here so we have a contract
design that basically makes it so that a
and B B's prove apart really piano the
Rural Employment are like these sort of
imaginary players we replace that which
was one in which anybody can sort of
play on behalf of piano so we go is from
lunch string of plays to trees of plays
and so this allows you all 20 people to
these people all the blocks all in
parallel and it works out to a great
question great question others
cool okay so with that there's one last
thing to cover which is what the heck
happens at the end of this game right
that's the one thing that we haven't
gone over what the hell's going on as
the end game outcomes so the game's
gonna add when we have an atomic
proposition
so for example over here if we assume if
the P infinitive hog proposition the
next thing we get here was be saying not
P of this thing right and then we have a
saying P all right and now we don't know
how to reduce it any further
okay so when we can't reduce them any
further this is what the game is either
won or lost okay and it via the outcomes
that you assign is quite as you'd expect
if a is true so let's say the game
states of the economy we didn't say this
ba right so again because one player
either to prove the opponent we don't
know much but not the same as aim and
sum of atomic proposition names so I
have a little aid for this atom okay so
the game then if a is true right because
again atomic propositions have a truth
value associated with them if a is true
then P wins right therefore in business
but really be 10 men right because if
you were to actually play the game we
could make a mistake and lose ah
absolutely right so we'll talk about
that a little bit more later but for
right now all we're going to be doing is
talking about if the game had ended this
way
so what you're talking about is the
behavior of how people play the game so
if I say for all things last year I
could definitely lose the pea which day
I'll take if I pick the wrong day right
and this matters because you can't if
you actually play the game between two
players in a real system you can't go
back and say well a 1 therefore a must
have been right in the beginning that's
correct
so you so there actually are layer 2
designs that correspond to doing
precisely that and I actually think that
it's a pretty reasonable design so
it's too much of a sight trying to get
into that all now but there are cases in
which maybe you might want to be lenient
in that way it does give me some
advantages but it is a good point I mean
from a security standpoint you think the
fact that a that the fact that they won
the game doesn't establish that little a
was true in the beginning right so you
would need an additional argument about
incentives somehow absolutely so you
would have to get to any kind of
conclusion absolutely right
however if you make the assumption that
everybody knows that if any game plays
out that involves them in some way and
it's one than we assume all the possible
sub games they could have been played
out would have been one then that's okay
so there's nuance there and I know and I
know that essentially maps that you
can't go through multiple turns it's
only like really if a game was won all
possible challenges would have been lost
that's really the assumption that you
can make that other letters your
protocols make but it's not correct
right if you and I play chess and you
win right it doesn't mean that well it
could it doesn't me that I never had a
sure win position on the board it might
be that I actually had a winning
position I just missed it right so this
is the case however there are some where
this is a bit of a science so I'll try
to keep it relatively sure but there are
some cases in which you can make that
and particularly we're okay making the
deception if we tell you ahead of time
hey buddy your life depends on this
chess game because every other chess
game is you're playing next in the
future is gonna be dependent on whether
you
it's okay if I suffer because the game
came out that way but if everybody else
suffers because I messed up the game
very truth that's a design problem very
true so so so some of the major design
problems there we can tackle and the
ones that are sort of a you know
contextual subjective decisions you
might want to or not may want to make or
not make it your layer 2 protocol those
are choices that you can make yes oh is
it a game that you're playing a game on
the results of a game those already
played in which case like we already
know who won the chess games so now
you're planning gameplay
did you win the chess game around it but
even so if then won the chess game I
night he might mess up
then we play a game about who really won
the chess games if he makes a mistake I
could win the second game and convince
the room even though he deserves it
so like one claim one pain pain doesn't
mean the
it like the country it's not Monticello
right that's maybe an illuminating
example I think I think we're kind of
short because there's there's a whole
separate discussion what we're doing
right now is pretty separate from the
way that you implement a contract and so
one of the key things that you want to
do when you turn these semantics into
labor contract that you're writing out
blockchain is that if someone else makes
the wrong move and you know that they're
making the wrong move you can't let that
screw them over you have to be able to
sort of go like start and use up a new
game from a different point in the tree
where you make the move that you would
be this right and so there's a contract
design that allows you to do that but
anyway maybe I'll take you here because
this could be a very long discussion is
what I want to have but I also I said I
didn't want to get thrown aside a couple
more okay so does this make sense to
everyone you're defending some games and
you're defending some think if you're
defending something that's true you won
if you're defending something that's
false you've lost that make sense cool
excellent okay here we go okay so now we
have a game tree now we can make the
game tree so let's let's let's define
two atomic propositions path entity what
will they will then how will they be
assigned your thighs you guessed it
that's as falsity is true okay get it on
read this by the way it's possible some
pink enemies okay
it seems like we're gonna get great so
daintree for false more true so the game
always starts with the proofer I haven't
mentioned that yet but it's pretty
obvious the game is initiated by the
prover that's the one trying to prove it
so they made the first defense of the
thing being prudent okay so false or
true so P since false or true
now there's only one response according
the challengers though
which this is a not false and not true
right
so that is according to rule rule number
three here right right here
p0 uh not be 0 Anunnaki 1 right so false
portrait not false and not true right
make sense ok so now we have an right
and so they add P Naza choice
P can either say not on the left or not
to the right ok so let's say peaches is
I equals 0 aka the left now P is going
to say not the thing on the left which
is not not false okay and of course not
not falsely mikey is by not
false by own which is by false
Mikey right and so of course this day
Malcolm is going to be 1 by oh right so
the reason that it's one is because
Athens in the time proposition it's
false because P is defending a faucet on
proposition it's 1 by P so does that
does that side make sense yeah great
okay and of course the other side the
kids were one which is this tightly to
those big and someone says not call Sam
not true well you should obviously make
you know go ahead and say not true right
because that's true so yeah not not true
the same thing happens when you're the
sweetest is not true where's the truth
and that's what Mikey okay so for false
or true we have now taken this
expression this this expression in the
syntax just the language of first-order
logic and we've interpreted it as this
tree doesn't it says everyone is the one
here
awesome okay so that's great so now
we've defined a tree but we still
haven't answered the question
what does it mean for this thing to be
true or false we've interpreted this
expression as a tree now how do we look
at this tree and understand whether or
not the thing is actually true or false
right so that that's the next question
organized and the answer is going to be
strategies okay
so what is the traffic and I promise
we're almost through the good stuff
finally into protocols some plug all
right so so of course a strategy is a
subtree and actually may be able to skip
to the TLDR of the damn shot to you
which is a strategy for player a is we
start off with the big thing and they
look at all the possible challenges that
you can make right what's everything
that B could say if I said device if
player a said the first thing right so
for all the challenges we know winning
strategy says it says all the challenges
that he could have done a have a
response to that I have to be able to
deal with that case so you look at all
the challenges by B you speak my
specific powder challenge but that
should say so you specific pick a
specific kind of challenge and I'm
offline okay I think highlighter in
there it's a I promise you I said
hopefully I didn't present again oh baby
okay all right no worries my bless my
phone died we're gonna be good okay yes
so my strategy is when player a says
okay I'm playing a having a witness
what's my strategy here right okay my
strategy is I'm gonna look at all the
possible things that P could do I don't
know people what I'm gonna do in
response right and then for everything
that's done in response what are all the
things that they could do in response to
that and for each one of those I'm gonna
pick some
as well okay and so this defines a
strategy for player a right so for
example let's here yes
what's leg was that Polly six thanks a
lot I can fix it okay right and that's
when we repeat this process right so let
me let me just start the board because
maybe board as many this one here it's
on a high level what is the strategy
let's let's Li get a strategy for the
prover P okay so we have some some root
stage here I think this is you know P
you know whatever I'm not gonna write
out this thing probably examples right
but what is the strategy for the privity
a strategy is we look at all the
possible next nodes in the tree right so
these are all of the things that could
be played by oh okay so these are all
given form Oh something oh something
else something else right and so P has
to be every every single one of those
right so every everything that oh says
he's got an answer okay so what that
means is we're gonna pick one answer for
each of these that he's gonna play in
response right so these were played by
oh now these are played by people okay
so he said one thing he has to be able
to say okay here's all the things that
oh they say and here's what I mean to
say in response this is my strategy does
that make sense
it's what I am choosing to play in
response to anything possibly I can play
by my opponent and so again this
different people
for example imagine maybe you know maybe
maybe terminates terminates here and
this is like yeah but for this one
there's more stuff that could happen
right so these are all you know you know
counter counter counter claims by oh now
again he has to be able to nominate that
you need response these rules okay so in
effect will be debt is that you know
perhaps Oh couldn't make this decision
work you know this decision as well can
make these books but we want to pick
just one right so this this has to be
chosen
this has to be chose missus we chose
this has to be chosen this has been
chosen this has to be chosen assumptions
listen to these are on week and then all
possible plays by an opponent have to be
have to be a numerator does that make
sense this is a strategy anything like
what it does this is one gonna do
anything he does after that this is what
I'm gonna do right down to strategy
because this makes sense questions
comments concerns
all right well let's have it a strategy
so we just did the game true or false or
true okay and it turns out that stretch
is very easy to look at it turns out
that our strategy haha what a shocker is
one of these so normally this sub-tree
or this subtree on both strategies okay
the strategy here kids I've been pretty
easy because we've got a lot of knots
here we've got a lot of things where
there are main choices to be made
so in pieces this only has one response
so PE Husson but but but now for for for
most response a strategy for P has to be
to choose one or the other actions
America okay so let's say P's gonna
choose this action okay
now of course we have the response by oh
and then she chooses a response together
now there's not many branches here right
so it's very easy to see that he was
doing in this but this is a strategy
there's a basis everyone helped us with
this strategy is this interactive or not
interactive so the this so this this
without any highlights this tree here is
the full possible set of all
interactions okay so these games are
definitely interactive like they're
meant to be describing piano interacting
or challenging and Patrick childhood
kamikaze
right so this defines all the possible
actions okay a strategy for one player
defines the specific action that they
are going to take that they could take
in response to all possible actions by
the other one okay so every time we show
a strategy routine every time we have a
play by oh we didn't write one
particular response might be so it's my
strategy like shows which one I'm going
to do okay so realistically like oh
would not send that first one he would
just jump down to the last time he sends
an interaction and then people private
correct so realistically if you want to
make this an efficient smart contractor
you don't have a timeout through this
part this is more of this look so in
reality obviously not not always reduces
to not and not you know not not yeah not
as reduces to the thing and not not
always reason to the thing but and so
obviously personality test into one
dispute period in the actual smart
contract innovation well I will ignore
that for here because we're just trying
to get something from semantics that's
like that you know an equation you know
to take this like it in another example
is similar to how like tic-tac-toe is a
salt game and there is a strategy to
always win tic-tac-toe exactly right
exactly right yeah it's not like the the
first assertion ie I don't remember what
you call them but the first on the left
side is like setting up the keyboard
particular
exactly right exactly the next steps are
all the games but in our case the king
board is not a tic-tac-toe board
okay the board is AC is a logical
statement and the logical statement
progresses through each thing yes and
this is why for a layer 2 protocol you
would not play chess you would play
tic-tac-toe because we always want to
know that we have our money you don't
want to have to compute enactment when
you know I'm not infinite but a mass is
exactly right exactly right now so just
wouldn't be very useful in this room all
eyes just all been about maybe a I saw
up like all the games
there's some gamers that's awful we
wouldn't want to apply this ran into it
what's wrong
yeah so what you really have to
enumerate all strategies I just
enumerated and stop as soon as he finds
a winning strategy
definitely we do to have a securely I
chose another for all that Varitek me
you don't have to finally it just
absolutely right like one strategy that
leads to be out community tend to have
and then absolutely right to do to
continue so to have safety in a sense of
layer to what we want to say to say that
a protocol is safe in layer two is that
the winning strategy can always be found
by the person you know defending their
money that's what's taking this deposit
contract yes it's possible to be great
also the different possibilities because
if you have a graph that is huge like
wind up with like just beautiful seeing
also strategies and way to have a way to
set one over another because always we
take actress like maybe one little
country just take the best strategy ever
on this try China whatever so how do you
do that on the really complex set of
data so what we're not doing here is
proposing that all logical expressions
can be
as a different layer to gaming that is
meaningful most of the expressions that
we interpret with the semantics are not
gonna be meaningful they're gonna be on
safe protocols and I can be useful maybe
they're not gonna be able to move money
around or whatever the point is that we
can find some of them that do correspond
to the player to protocol so
particularly state channels plasmas
things like Troopa and optimistic
roll-up all of these things are very
simple games which do have continuing
strategies so like Carlos said you don't
you don't make chess out of this you
make tic-tac-toe something that is
playable right so this is what this is
what layer 2 protocols were developers
were doing when they invented state
channels they they didn't realize it but
they were finding these sequences of
expressions these challenges and
responses in which the client could like
have a chance at actually computing
what's going on yes could you do
something like turning a complete and
then do a problem that department
absolutely absolutely good so state
channels are gay example of this I can
play as a chess game in a state channel
but the dispute game is not going to be
about it is not going to be me fighting
my winning stretch the chess game it's
gonna be me fighting the winning
strategy for proving the highest signed
which we sign nods to the smart contract
and that's the channel stuff and the
chest that is a layer on top of that
exactly right exactly right yes it seems
like I'm being like finding the correct
finding if you have a winning strategy
for the for all it's got hard because
you have a like you need to find a team
absolutely right and so and so the for
all in practice there's two ways there's
two common ways to be able to compute
for all so one for all that we can do
keep for easily is if we say for all
things such that signed by me or such
that signed by me I know exactly
and I can enumerate that so that's a
nice for all another for all that we use
in plasma is for all blocks less than X
and now that we can numerate because we
doesn't go with the X X minus 1 X minus
2 to 0 so it's a finite set and so
absolutely there are tons of games here
that we come up with that are not
computable and are like very very hard
to reason about but some of them turn
out to be lazy protocols and so we think
that's pretty cool yeah
other questions great questions yes the
way each step like he's stepping the
trade felt it would have an extra pair
and in theory each stuff without that is
great in reality what you actually have
mr. Turing this is what this is was
mentioned earlier is only when there's a
choice to be made so particularly the
time that really ends up gift-getting
you would hop to a dimension time up is
when you got a needle for all or hand
and you have to make a choice see
they're not the left side and or not the
right side at the end but but but you
can doesn't you any pianist should
design the contracts on that expression
not got to you is automatically reduced
to T because this is the only possible
place so why play time on it can
automatically be reduced
yeah well in person like lost my I mean
do more if you sell but if like every
game has to share this day interior so
like from the start to the end that have
to be in this game can I have different
gifts
apparently yes so actually and so we
touched on this in the paper MVP is one
of the very interesting examples of
games that doesn't rate into this
magnetism planet not even new connected
to do it
the latke connected so to not be playing
inside baseball here plasma MVP these
are the original spec for plasma have
this thing called an exit cue and
basically there could be like
transactions forged and inserted by this
malicious music and the way that you
prove that they were forged or delicious
was you proved that the sum of all the
UT EXO's that led up to the forest once
was equal to the total amount deposited
into the contract and so this actually
seems to be like a summation operation
so we would need to define some sort of
MVP q observation operation so that has
to be done been done this because
there's a lot to do without that but
you're absolutely right that's it that's
a great example of more sort of game
than their activity yeah absolutely no
other questions
all right well I like him so keep them
coming okay we remember we okay okay
great so this is an example of a winning
strategy why is it winning because every
possible leaf every game outcome was one
Mikey so a winning strategy is it is one
in which all these branches was on the
way okay so if we go back here right
buddy we liberated the so for instance
tic-tac-toe has a lean strategy right
because we can numerate all the
responses by the button and then 1
pikmin particular play after that and so
on and so forth a narrow one so if these
are all one
and this is a winning strategy for
people because they've all been won
right
and so what this corresponds to in later
two world is the reason that I know I
have some money is because I know
whatever however some tries to dispute
me whatever they do I'm going to be able
to win that outcome okay and like this
is why I have some layer two states
because I know winning strategy that
proves that that state was internet so
we can sort of interpret the truth of
these expressions based on whether or
not there's a winning strategy in the
tree for that for the particular image
that corresponds the particular
expression make sense
nice other questions comments attorney
and so some interesting notes on this
one of the ways that you can understand
odd than not is it reverses the roles
right so we have that not expression P
right not paid because that not reverses
the week right reverses the roles
Marisa's so if someone trying to prove P
then it's like the opponent is trying to
prove a not be okay so this reverses the
roles so there's a winning strategy for
key then there's not one a strategy for
o and if there's a winning strategy for
oh there's not a winning strategy for P
so thankfully we've retired that at
least so what this means is that if P is
sort of true because of his winning
strategy then oh not people will be
false because now the other guy is the
opponent so there you have the winning
strategy is now the one who's gonna win
but he's now the opponent as opposed to
the proven so this is this is sort of
good we've recurred some intuitive
properties of other logics and other
semantics in which is singin a is true
staining the statement not a is false
right so we released with at least
recover time okay
I wanna pause for questions I don't have
this I'll do it once again okay great
but learn about photography okay so this
is saying that we've totally ignored up
to now and this is saying it does add
more complexity most of what we've gone
over here very very similar to existing
works in game semantics and biological
logic and these things the complex
nature that comes about is in layer two
protocols these the truth of a
particular composition changes off chain
so for example there's a game
corresponding to a channel and state
channel thinks it's right but basically
the claim that says uses this multiple
evolved multi signaling system
before that says I claim that this is
the valid state because I claim for of
all states higher than this for all the
knots is higher there does not exist a
multi-sig signed by everyone and so that
is what state channel is so let's say
that that's the end that's true at time
and X maybe at time X plus 1 we sign the
next knots well now this thing that is
false because this one is true here
right and so there's some notion in in
the layer tool that is subjective truth
it's not that it's not like true or
false which is obviously true right
click this is the expression true or
false duh that's true like oh no duh
true or false
right but the expression signature
exists or hash tree which exists that's
dependent on what the players know and
what they're allowed to play exactly
this this is the point that it's not the
facts it's not that what exists
abstractly changes the players knowledge
- right exactly right
so players knowledge about particular
data changes over time and this changes
the computability of what's going on
right so we have a yellow we have a
bottle for this right that this problem
is called logical or missions right and
so we have a problem for this and this
is that we have a solution for this
whether there's a problem beyond
solution there we go ok so I don't think
we'll play to you that it is nearly as
advanced as the rest of the massive
amounts of work that have gone into the
systemization of knowledge and
cryptographic knowledge and
computability it's not but it's enough
to be improved constant to demonstrate
that we can express layer 2 systems has
you know has logical expressions and so
unify them all under one framer ok so
the way we think about it is we define
subset W and this is like a set of the
worlds okay so one world it was that
might say Alice has a private key King
but she's not signed anything ok another
world like saying Alice's s is the
Viking king and she's signed message m
and sent it off to the opponent so the
opponent knows
how's the signature but only on the
message n right and so as we progressed
through these world that progression so
Alice when it started out not haven't
seen anything
and then at world zero and then a world
one she decided message M this is what
will allow us to change this thing
between true and false because in this
world it's not true for anything that
there exists a signature of my house in
this world it's true for a message that
there is a signature of my house
and so this progression through worlds
is what you actually do when you execute
a layer 2 protocol and you and you send
them ie roundoff chain into it'll make
sense so we can find this a little more
precisely by saying there's a
computability of computable subset ok so
we call these X hop ok and this is like
the segmentation but when you really
care about as a function it takes in the
current world and the which player it is
either either the approver of the
opponent and return some subset of the
total state which they contribute which
they are therefore the loud to play ok
so for example you know in a world where
Thomas has not seen anything
but cannot play your signature as a
challenge so if the world W here says
Alice has not signed anything
then executable is a subset of X which
does not include Alice's signature and
therefore you know exists such that
signed by house will end up being false
and of being false okay so tactus how do
we how did this has to affect the game
somehow so the way that we can affect
the semantics is we change the final
challenge rule right so we have this
five challengers rules before the
university lot fire for all it's not
changed it so instead of T and X we can
only pick tag team in the computable
subset of X in the current world by the
current player
is going to be providing the challenge
so this is a got a subset of the trees
so whereas before all the possible
things were known by the logic and
therefore all the possible things could
be played in history radical notion now
we might say we're in a particular w0
due to this set of worlds and in this
world you know you know maybe this was
false right but in this world it turns
out that oh can i play cannot play this
branch so we're good right so we still
have a winning strategy because in this
world this cannot be commutative it's
impossible to go to play it because it's
computers only finite and though that
only knows the things that it's
downloaded off and because Palace is not
signed any that has not signed the thing
and there were economic endowment from
the internet or cubed then this this
thing is inaccessible so we restrict
these observes theoretical game treaties
which would - only once which are
computable moves right only the only way
to play something is if your computer
can get in there and punch the numbers
and plate and now note of course that in
each will W there's a different game
tree right so maybe hit W 0 at maybe of
W 0 this was our final but maybe of W 1
now this is playable again right make
you know a reason X there we go ok so
maybe and maybe in this world it is
playable again right so it is playable
again well now this thing becomes false
because the strategy doesn't check out
right the strategy doesn't work because
this is laws ok and so what this means
is that as we progress through worlds
these propositions can go from being
true to the impulsive it's no longer
meaningful to interpret the truth of a
statement in a vacuum you have to
interpret it in the particular
computability world or whatever you want
to call it that corresponds to the state
of affairs right and so we
say that now there's a strategy that is
winning or losing even world done and
therefore we say that a logical
proposition is true or false in the
world w it's not in a vacuum it's not
the true or false on its own it's true
or false in the world w XS so in
practice the world W that you're going
to track you is for instance what am i
signing
yes so in this example what the party
can't compute is whether they would win
or lose if they went down that right
path or is it that they can't compute
they can't even compute what the choices
they know so what it is is they can't
compute the move therefore they can't
play it so the game trees so they don't
even know what there's some uses they
know what their set of moves is is one
of the computer can come up with right
so it's so it's so but they'd the but
all right so so for example more
importantly I know that my opponent can
never come up with my signature unless
I've given to them and that's the really
important one and so that allows me to
restrict the subject so you essentially
you're taking the original train you're
just pruning out that's exactly right
you're pruning out any moves which are
computationally infeasible to have been
played in the first place and this was
what removes the logical omniscience
problem and makes the extrude hang
subjectively so I have a set of moods
that I can if in the game might one of
the moves I could place to exhibit
Alice's signature on some string right
there's a set of strings of a certain
length that I know I can play it's not
that I it's not that I don't know that
that I am allowed to play that string of
bits it's just that I don't know that's
the string I should play in order to win
that I don't know that I can't figure
out the enormous number of moves that
available to me which of them is winning
okay so maybe I'm more loosely than I
should have thrown around allowed so
it's not really allowed it's really
capable right the game tree is
restricted because people are incapable
of playing moves that are not computable
by their computers so so it may be maybe
that maybe that refinement of learning
would help would help there
I mean looks like let's take this long
okay I'll take offline excellent okay
and now we can tell by the way okay we
all that tension other questions other
questions can when you look at me look
at the commercial this is this is very
reminiscent if you want to see what is
the set up winning strategies based on
that anyone up in a certain tree with
this basic basically what's the support
right so you could you could be
happening rolls over these right two to
two
- to see you know because of the path
that the path or the ones that are that
are that are not computable will give
you zero right right because there's no
support right but if you're if you're if
you're integrating the path of the world
WWI and you're dirty you're going we can
express it to paths that you can
actually because it's you can treat the
power series you can then Excel
exponentiate so that that's so now now
you actually now you'll actually have a
have a have a have a corresponding that
you can you can compute total total
total total values of census right
beautiful positive it goes I don't know
they apply but that sounds great so this
is talking out there that that's exactly
what I'm trying to do here is and make
up something that sounds legit enough
that you believe me the hell to it will
be supported by it but that you can
stick on your actual knowledge of
computability and cryptography because
mine is woefully inadequate to deal with
these sort of systemic problem actually
it's actually more okay what about me my
not sure about today okay absolutely so
let's check after yeah in general I'll
be around after everyone who wants to
come let's come talk about this stuff
okay it's like a very a very simple
computer ability model that you can
build which is one that we sort of deal
with in in the statement which may or
may not be of course the accurate at all
is maybe maybe the way that we define
our world and as we say that the world
is that the world and the set of worlds
is applied my three things a set of
public information I set of secret
information to P and a sort of secret
information
right and you maintain the rule whatever
the world is a particularly we say that
in all worlds it holds true that if some
act something's up some that said
element X is in the secret information
of a then it is not in the public
information okay so if a if a has to see
an information that is not in the public
information right and the further we say
the computable the computable moves that
can be played is the intersection of all
the possible groups with the public
information set so what this means
instead of X is in I I be secret then
therefore it's not in I public and
therefore it's not in this intersection
and it's not playable so this is a very
simple very rudimentary way to try to
restrict these game trees it's probably
has nothing to do like a you know maybe
when I said this was like universe of
composability and get it you know I get
an actual security model that
corresponds to crypto slapped on it this
is probably not it but it gives you a
good intuition for what's going on yes
that's the question
it's public but it is it or private yeah
so what is it right right so we'll say
the public the public information is
known by both parties that's why we're
calling it public right and so maybe
this isn't accurate to the meaning so
for example if we extend this to can't
party world on which there are many
different play people playing things
there's not one public set of
information there's a set of information
that I have downloaded and there's a set
of information that's secret to me that
I know that no one else is downloaded
but making the local information that is
public that I have downloaded is not is
not is not that downloaded by someone
else right so there's many more complex
models you can build
far more complex models and that's what
we need we need a better model this is a
very simple one that we can throw
together just to pull out the course or
elements of
other questions five minutes which I'm
pretty pleased because we're pretty much
there okay so a really simple example
with this very very very simple model
which again probably not accurate to the
computer science out there but it's
accurate enough to give us a layered you
can treat that actually corresponds to
what really is done on chained in
literature
so the preimage existence you know you
know sort of predicate is like the
simplest sort of rudimentary example of
what happens right so the game or
proposition is as follows there exists a
hash in you know the set of lights such
that is has privileged H and H naught
for some some fixed H naught is known
okay so this game has a different game
tree depending on whether or not H the
particularly you know a little H is
known it's in the moment information or
is not right so this is the game for
this game up there so we'll W in which H
naught is in pub then this game is true
this game is true right because the
premiere says there exists a chance the
purpose of this thing
then the abundance has no hope for all
age not is Hashmi image but because H
naught is in the public information he
may choose it is in the computable
subset so it may be played and so now
that the P naught is hatched village
Judas is that not decided image
purchases fish has been image and this
is true right so it's one by people so
in a world in which H naught is in the
public domain
then this proposition is interpreted as
true because this is a winning strategy
for that composition for the proven
however instead H naught is secret right
its secrets to the opponent then this
will not be true because this step which
we previously had is is not to be is not
computable
it's not possible random may be allowed
it's not possible because H naught is
not in peace it's not in the public
center information so you have to play
and no matter what the actual world is
right so maybe the rest of the elements
we said we might play some H prime or
some major private line but no matter
what happens there those are gonna be
false because of that they only inch
only this image not which is secret and
there we're not playable there's gonna
be the thing that gets us to a true
statement at the bottom a truly a true
game outcome okay
and so normally what this means is that
if we start out in this in this world in
which H not the secret to vote then this
proposition is false but its desired by
by the opponent oh may reveal that
preimage and in doing so it would change
the world that the world would know what
managed by my security would go back to
this one and it would now be true so
we've changed the truth so we started in
a world where the game where the thing
is false and we added a thing in which
the thing is true right and because we
can do that off chain and because we can
enforce these games on chain this is how
we get the scalability of player two
solutions wouldn't it be sort of cleaner
and easier to think about if you just
said Pino is H such that sure that might
that might be cleaner yeah absolutely
absolutely yeah
so this is a very simple thing you like
started together because point I want to
get across is these games were what
happened on to me
earlier twos and someone's you'll be
able to do the spring rehearsal yet
effectively yes your local public
information an example of our building
and Priya doesn't make the city
this may be necessarily true for all
participants just the party that
actually revealed to absolutely right
and that's why so far I've defined the
semantics as between two imaginary
players of group Republic where you're
absolutely right well we need to do to
like hit this with the universal
composability but you know at that you
know epic like formal proof you know for
all they are to model is we need to have
that we need to have a say you know a
distributed system like thank many many
people public shared information what
what has been published shared to anyone
was been publishers only some people and
when it's not the publisher aka is
private right so absolutely this is
lonely and if you think you know it or
know a good way to do it or how
something knows gonna do it come find
you
ah what is it useful for so-and-so as we
have exactly one minute to go
what is it useful for well here is a
state channel so the thing that we've
been doing all along to come upon state
channels and we've thought of as a
unique thing is actually simply this
expression okay so this is a pre-image
reveal stage channel so we imagine that
there's a set of hashes which are all
secret to the opponent in the beginning
and as we progress to your worlds we
selectively revealed each patch and by
associated a game of the form channel s2
a payout of the form s so that we pay
say s coins out to someone we can
actually associate money with this game
and by selectively revealing these three
images we selected they're paid at one
collector nomination through the
planning so that's a state journal okay
we can also do certain or aetherium
style change you know so here's our
multi sync that we had before there's a
multi sing as I'm the day before in a
theory of style channel as I claim for
this day there exists some obesity and
fourtner's does not exist the higher
snake such that there's an officer and
the state is indeed higher with a higher
knots right so there's that here's how
the music roll up
do you pick that exchange but just
remember this this is a roll of chain
computability model of care for roll ups
are really nice is that it is a chain
always makes data available so the
computability ball is much easier for
any information that's on the main chain
because it's always no it can't be in
this very great property and make sure
it very very very simple
graceful elegant distress of an elegant
thing because it's nice to learn
lastly it's plasma which is God awfully
complicated expression somebody and it's
the simplest possible construction I
think about them but I can tell you the
distant deep works is we got a paper
that talks more about opposition money
with this Allah we got to go thank you
very much
[Applause]