►
Description
Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on Swarm, IPFS and more.
https://archive.devcon.org/archive/watch/6/building-secure-contracts-use-echidna-like-a-pro/
In this workshop, attendees will gain hands-on experience with Echidna - an open-source smart contract fuzzer - to build secure smart contracts. Echidna has been used in many professional audits, and fuzzing is a key component to increasing the contracts’ security. Attendees will learn how to define and write invariants and how to use Echidna efficiently. By the end of the session, they will know how to integrate property testing into their development process and write more secure code.
Speaker(s): Josselin Feist, Gustavo Grieco
Track: Security
Keywords: fuzzing,vulnerability,testing
Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/
Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/
A
A
A
Okay,
okay,
so
who
are
we
so
Gustavo
Greco
and
myself,
Rosner
Feist?
We
are
both
security
researcher
at
trail
of
Beats.
If
you
don't
know
us,
we
are
a
company
where
we
specialize
in
high
hand
security
technology.
We
have
expertive
in
blockchain,
but
also
another
topic.
For
example,
we
do
a
lot
of
cloud
native
application
or
we
do
a
lot
of
cryptography
with
like
weaker
stuff,
and
so
something
that
I
think
differs
from
other
company
is
that
we
spend
a
lot
of
time
trying
to
apply
research
and
program
analysis
into
like
our
daily
job.
A
As
a
result,
we
have
built
a
lot
of
Open
Source
tool.
You
might
know
slitter,
which
is
a
static
analyzer
for
solidity,
a
kidnap.
We
are
going
to
talk
about
it
today,
but
we
have
a
lot
of
other
tools,
for
example
tiller,
which
is
a
static
analyzer
for
algorand
armana,
which
is
static,
analyzer
for
KO
and
so
on.
A
A
I'm,
assuming
everyone
here
is
familiar
with
unit
tests.
You
should
use
any
test
and
they
are
good
usually
to
cover
that
the
system
is
working
as
expected
in
the
happy
path,
something
that
we
have
learned
over.
Our
audit
and
I
know.
Those
analysis
that
we
have
done
is
that
there
is
no
correlation
between
the
quality
and
the
quantity
of
the
unit
test
and
the
likelihood
of
having
high
severity
vulnerability.
And
this
is,
we
actually
have
an
academic
paper
on
this,
where
we
have
looked
over.
A
Like
all
the
audits
we
have
done-
and
this
is
a
correlation
that
we
have
not
found
and
the
reason
why
our
intuition
tell
us
that
when
you
are
going
to
write
unit
test,
you
are
going
to
try
to
cover
happy
path,
things
that
are
supposed
to
do
in
the
correct
execution,
while
vulnerability
usually
lies
in
the
edge
CAD.
In
the
things
that
you
haven't
considered.
A
An
example
of
a
unit
test,
the
second
technique
that
you
can
use
is
manual
webview,
so
you
can
go
line
by
line
and
try
to
understand
what
the
code
is
supposed
to
do.
What
is
actually
doing
and
if
there
is
like
a
difference
between
both
doing
manual
review,
requires
specific
set
of
skills.
It's
time
consuming
it's
it's
it's
kind
of
difficult
to
do.
Usually
you
are
going
to
go
through
a
security
company
to
do
a
security
assessment
to
have
people
that
have
this
specific
set
of
skills.
A
The
next
technique
that
you
can
use
is
using
a
fully
automated
tool.
These
are
like
the
two
that
are
going
to
find
some
of
the
common
bugs
you're
just
going
to
click
on
the
button,
and
the
tool
is
going
to
tell
you
there
is
this
type
of
work
or
not.
For
example,
you
might
know
Theta,
which
is
our
static
analyzer
for
solidity.
This
type
of
techniques
might
give
you
forth
running,
but
they're
also
really
powerful,
because
I
might
cut.
You
know
like
a
critical
bugs
you,
oh
yeah,
okay,.
A
Okay,
so
first
Rita,
like
the
best
technique,
is
spend
one
hour
like
the
first
time.
You
try
it.
There
is
a
triage
mode.
So
once
you
have
triage
like
the
ways
you
as
I
won't
show
up
like
in
the
next
execution,
and
if
it
takes
you
like
one
hour
and
at
the
end
of
the
day,
you
might
be
able
to
catch
critical
vulnerability.
I
would
say
it's
worth
going
for
the
first
result
and
look
we
are.
A
We
have
like
a
list
of
trophy
for
Twitter
that
demonstrates
that
we
have
found
a
lot
of
like
actual
bug
using
it
so
yeah.
There
is
like
a
false
positive
pass
for
for
false
alarm,
but
it's
not
going
to
take
you
so
much
time
and
it's
going
to
provide
you
value.
For
example,
we
have
a
git
abduction
with
Filter,
when
you
can
connect
it
to
GitHub
on
every
pull
request
commitment,
depending
on
how
you
are
going
to
configure
it.
It's
going
to
run
if
to
see
if
you
are
introducing
new
new
vulnerability,
yeah.
A
Okay.
The
last
technique
that
you
can
use
is
using
semi-automated
analysis,
so
these
are
going
to
be
tools
for
which
you
are
going
to
provide
some
information
for
which
you
are
going
to
have
a
human
intervention,
to
explain
to
the
tool
what
you
are
looking
for,
and
this
is
a
bit
more
difficult
to
use
because
it
requires
like
this
interaction
from
you
know,
from
the
user.
A
So
what
is
property-based
texting
to
understand
how
it
works?
I
have
to
introduce
fuzzing.
So
first
thing
is
a
standard
program
analysis
technique
that
is
used
a
lot
in
traditional
security.
The
idea
is,
basically,
you
provide
a
one-time
input
to
the
program
and
you
try
to
see.
What's
what's
going
to
happen,
you
try
to
stress
this
with
random
input,
the
most
trivial
further
that
you
convert.
A
A
However,
most
of
the
traditional
feather
are
going
to
look
for
memory
corruption
for
crash
in
the
program.
We
don't
have
a
lot
of
memory,
corruption
on
solidity.
There
are
some,
but
they
are
not
that
common.
What
we
are
going
to
try
to
look
for
is
a
property
of
the
system
that
can
be
broken,
and
this
is
why
we
call
it
property
based
testing.
Basically,
the
way
it
works
is
that
the
user
is
going
to
define
invariants.
A
The
further
is
going
to
explore.
One
Dome
is
a
program,
and
it's
going
to
try
to
save
the
invariant
odd
or
not.
You
can
think
of
you
of
feeling
really
as
like
unit
tests
on
steroid
well
with
unit
test.
You
try
one
specific
value
with
the
program,
while
first
thing
is
just
going
to
try
randomly
a
lot
of
different
value.
A
A
So
I'll
talk
also
about
ekina,
so
echina
is
our
further
for
smart
contract
interpensers.
We
have
been
using
it
for
like
four
or
five
years.
Even
now.
In
all
our
audits,
you
can
see
a
list
of
match
your
code
base
actually
using
and
I've
integrated
Echidna
in
their
process
for
Aquino.
We
are
focusing
on
the
you
know,
ease
of
fuse,
so
the
invariant
are
going
to
be
describing
solidity.
We
have
a
GitHub
action
similar
to
slitter
and
we
support
all
the
compilation
of
framework.
A
Okay,
I
was
talking
about
invariant,
so
let's
say
you
have
a
token.
You
have
a
Neo
C20
token.
It
has
you
know
a
balance.
You
can
transfer
token.
What
would
be
an
invariance
an
environment
could
be
that
if
you
have
a
total
Supply,
no
user
in
the
system
should
have
not
talking
to
the
total
Supply
right.
If
you
have
10
million
of
token,
if
a
user
of
20
million
yeah
something
is
wrong.
A
The
way
it
works
is
that
you're
going
to
take
the
contract
in
solidity,
you're
going
to
Define
invariants,
which
are
going
to
describe
what
you
are
trying
to
check.
One
way
to
do
that
is
to
create
functions
that
are
called
echina
underscore
some
name.
This
function
should
work
on
a
Boolean
is
a
Boolean,
is
true
the
property
or
if
the
Boolean
is
false
or
the
property
is
broken,
you
give
both
to
Akin.
Now
Akinator
is
going
to
explore
one
Dominator
program
and
it's
going
to
try
to
see
if
it
hurts
foreign
for
you.
A
So
we
have
we're
going
to
have
a
couple
of
theory
of
exercise
where
you're
going
to
try
to
apply
again
now
and
to
Define
some
invariant
on
the
system.
You
can
go
on
this
repo
or
you
can
scan
the
QR
code
to
object
repo
check
out
the
Defcon
branch
and
open
the
first
exercise
if
you
have
any
problem
to
install
Akin
now,
if
you
have
any
question,
let
us
know.
B
We
also
welcome
everyone
who
is
not
into
the
exercises
just
to
see,
even
even
if
you're
already
know
how
to
do
how
to
do
testing
or
even
if
you,
if
you
use
fasting
every
day,
it's
it's
totally
fine.
We
will
happy
to
take
any
questions
simple
or
more
advanced
about
how
Echidna
work,
so
please
feel
free
to
to
do
it.
A
Okay,
so
the
question
was:
what
are
the
benefits
of
using
Echidna
other
Foundry,
so
first
I
think
echina
has
more
features
than
friendly.
At
the
moment
they
were
developing
Foundry.
For
like
six
months,
we
have
been
using
a
canine
like
four
years.
We
support
any
compilation
framework.
So
let's
say
you
are
using
r
dot
because
you
want
to
do
integration
test
and
you
need
some
complex
setup
using
like
typescript
or
whatever.
If
you
move
to
Foundry
you're
going
to
have
issue,
because
it's
more
difficult
to
you
know
create
this
type
of
test.
A
A
Here
we
are,
like
you
know,
agnostic
to
the
compilation
framework.
In
that
sense,
we
have
we're
going
to
talk
about
that
later.
We
also
have
like
a
couple
of
advanced
features
that
the
others
I
don't
have.
For
example,
something
that
you
can
do
with
echina
is
that,
instead
of
trying
to
find
in
there
that
are
broken,
you
can
look
for
functions
that
consume
most
of
the
gas.
So
you
can
list
the
further
one
and
give
you
a
summary
of
okay.
C
A
Okay,
that's
a
really
good
question
and
even
in
like
traditional
Feathering,
you
know
like
if
you
go
like
in
the
literature
of
whole
feather
or
benchmark,
I
would
say
that
most
of
the
benchmarks
are
poor
or
one
of
the
issues
that
when
someone
does
a
benchmark
to
you,
know
benchmark
their
own
tool,
there's
a
bias
all
right,
so
we
we
have
Benchmark.
We
have
our
own
Benchmark
to
try
to
see.
B
Yeah,
it's
it's
also
an
open
question.
What
is
your
benchmarking
like
if
you,
if
you
are
if
you're
saying
well,
this
is
faster
than
this
sort
of
thing,
but
it
could
be
executing
just
always
the
same
thing
like
you
know,
calling
a
constant
function
over
and
over
again
is
going
to
be
faster
than
calling
some
deep,
deep
part
in
the
in
the
call.
On
top
of
that,
you
have
like
bugs
what
about
like
finding
bars,
how
much
bugs
you
found,
and
there
is.
B
There-
are
a
couple
of
academic
papers
saying
that
some
people
like
to
compare
this,
but
you
have
a
like,
like
a
plot
saying
how
many
Bucks
you
found,
and
let's
say
that
one
faster
is
better
than
the
other,
but
you
don't
know
if
the
next
hour,
you
will
have
a
a
peak
saying.
Well,
these
found
a
lot
of
things.
So
there
are
all
the
things
that
you
can
do,
so
you
can
use
coverage,
but
also
coverage
is
not
going
to
give
you
like
it's
not
going
to
be
the
the
ultimate
answer.
B
So
it's
it's
still
a
debate.
How
long
you
should
run
faster
for
a
benchmark
or
even
for
you
know,
testing
something?
It's
also
a
debate.
What
you,
what
we
should
use
for
benchmarking,
should
we
use
like
complex,
defy
applications
like,
but
how
many
of
them
we
have
like
10
or
20?
We
don't
have
thousands
of
different
device.
So
it's
it's!
We.
We
definitely
are
interested
in
a
deeper
discussion
on
how
to
have
a
good
band
merch
set
for
for
touring.
A
And
we
have
the
same
problem,
for
example
with
Rita.
Well,
how
do
we
Benchmark
it?
Our
static
analyzer
provide
good
weather
and
it's
tough.
We
usually
tend
to
have
a
practical
approach
in
the
sense
that,
if
the
truth
provide
value
during
our
audit,
if
it
helps
us,
you
know
to
find
bugs-
and
we
make
us
faster.
B
B
A
It's
it's
only
for
first
thing:
we
have
another
tool
for
symbolic
execution,
which
is
called
Mantika,
however,
and
something
actually
we're
going
to
discuss
later,
I
think
in
practice,
any
formal
base
method
approach
is
going
to
have
a
lower
return
on
investment
at
further.
If
you
have
two
weeks
three
weeks
to
work
on
a
project,
you
know-
and
you
want
to
invest
some
resource
to
increase
your
confidence
in
the
project.
First
thing
is
the
best
solution.
Yes,.
B
If
you,
if
you,
if
you
have
a
test
case,
that
is
not
that
is
not
working,
please
let
us
know,
and
we
can
try
to
to
see
it,
but
in
practice
it
seems
like
some
of
the
typical
use
cases
for
symbolic
execution
in
which
you
have
constant
Magic
values
to
to
look
for.
They
can
be
replaced
by
constant
mining
extraction.
A
B
No,
you
you,
you,
you,
you
have
to
open
your
terminal
and
a
kidnap
will
deploy.
The
sort
of
unit
is
still
installed
the
tool
and
when
you
put
like
equipment,
you
cannot
test
some
contract,
it
will
compile
it
running
inside
the
simulated
blockchain
and
give
you
the
answer.
So
you
don't
need
to
connect
into
something.
B
B
So
so
over
there
you
said
like
if
you're
using
Mac,
you
can
do
that
that
or
you
can
download
okay
yeah,
okay,
yeah,
so
I
wanted
to
highlight
one
one
little
feature
that
we
are
testing
on
Echidna,
that
is,
that
is
also
used
in
fasting,
but
instead
of
testing
a
property
where
we
are
doing
minimization
or
maximization
of
some
value.
So
this
is
an
a
new
thing
that
we
are
that
we
are
testing.
It
is
not
property
based
testing,
but
it's
it's
something.
It's
something
that
we
are
trying
that
we
are
trying
to
push.
B
So
if
you
want
to
know
if
a
user
is
it's
capable
of
extracting
tokens
from
your
system
without
you
to
realize
you
can
use
that
feature
just
saying:
Hey
Echidna.
Can
you
maximize
this
balance
of
this
account?
So
it
will
try
to
generate
you
the
maximum
sequence.
So
it's
it's!
It's
a
little
bit
outside
this,
but
it's
something
that
we
wanted
to
mention.
A
Okay,
so
our
Target
here
is
a
token.
It
has
a
transfer
function
like
a
classic
Crosshair
function.
You
enable
it
from
a
possible
contract
which
is
like
a
basic
possible
system,
and
what
we
want
to
try
to
do
here
is
to
create
the
invariants,
such
as
no
user
should
have
a
balance
above
the
total
Supply
test.
The
tokens
where
we
are
going
to
do
it
is
that
we
are
going
to
inherit
the
token
or
Target
we
are
going
to
create
the
contract
test.
Token.
A
We
are
going
to
initialize
the
balance
of
the
colors
of
the
first
user
to
10
000,
and
this
is
an
initialization,
so
you
are
creating
a
token.
There
is
10
000
in
one
address,
and
no.
The
invariant
is
simply
that
no
user,
so
the
user
should
not
have
more
than
10
000.
Okay,
again,
you
deploy
a
token
10
000
token
to
one
user.
This
user
should
never
have
like
20
000
token
all
right,
and
if
you
want
this
with
a
kidnap,
a
Kina
is
going
to
tell
you
that
this
invariant
is
property.
A
A
This
was
compiled
with
solidity
0.7.
So
there
is
no
overflow
and
underflow
protection.
So
there
was
an
underflow
problem
here,
where,
if
you
try
to
send
more
more
tokens
that
you
have
a
new
balance,
the
balance
is
going
to
render
flow,
and
you
know
you
have
a
really
large
balance.
Something
which
is
interesting
here
is
that
we
Define
the
invariance.
You
know
without
looking
at
the
code
without
looking
at
the
function,
we
were
not
looking.
Is
there
any
issue
in
the
transfer
function?
A
A
Okay,
so,
okay,
so
the
question
is:
does
it
execute
a
specific
function
or
how
does
it
know
which
function
to
curve
the
answer
that
is
going
to
call
everything?
So
in
this
token,
if
you
look
at
like
the
word
source
code,
you
have
a
transfer
function,
possible
function
and
like
some
additional
function,
so
the
federal
is
just
going
to
call
everything
and
everything,
external
or
public,
like
everything
that
a
user
can
call.
A
Okay,
the
question
is,
if
you
have
a
very
large
token
or
very
large
contract,
you
have
a
lot
of
function,
so
here
you
can
take
different
approach
either
you
want
a
keynote
to
call
everything
and
you
just
do
nothing
and
you
let
it
now
when
which
might
work?
No,
it
depends
on
what
it
is.
If
you
know
that
some
functions
are
more
important
and
you
want
to
Target,
you
can
change
in
the
configuration
configuration
file
of
echina
and
tell
him
call
only
this
function
or
don't
call
this
function.
A
E
A
Okay,
so
the
question
is:
can
you
have
like
a
better
log,
because
obviously
this
is
like
a
simple
example
and
when
you
do
want
them,
you
know
exploration.
You
might
call
a
lot
of
functions
that
are
not
necessary
for
what
you
are
trying
to
to
call
right,
and
the
answer
is
yes,
so
Echidna
does
what
we
call
shrinking,
where
once
it
found
a
way
to
break
the
invariant,
it's
going
to
try
to
reduce
the
choice.
A
Target
so
you're
going
to
try
to
have
an
invariant.
On
the
same
token,
the
first
invariant
was
that
no
user
should
have
a
balance
above
total
Supply
here,
as
we
kind
of
hinted
before
now.
This
is
a
possible
system,
so
it's
a
system
where
the
owner
can
pause
or
unpause
the
system
and
what
we
want
to
verify
the
environment
we
want
to
have
is
that
if
there
is
nowhere
now
and
the
system
is
pause,
can
someone
unpose
a
system,
and
this
is
what
we're
going
to
try.
A
And
what
we
want
to
check
is
that
if
we
drop
the
ownership
and
we
pause
the
system,
is
it
possible
to
unpause
it?
So
here
we
have
a
bit
of
initialization
to
do
what,
because
we
want
to
drop
the
ownership
and
we
want
to
put
the
system.
We
are
doing
this
in
the
Constructor,
so
we
are
calling
pause
and
oh
no
from
now
on
the
system
as
a
contract
is
deployed,
it's
pause.
There
is
no.
A
No,
the
invariant
is
then,
just
if
the
variable
that
you
know
tracks
the
possible
state
of
the
system
is
true,
and
this
should
hard
work.
You
pause,
no
ownership,
it
should
be
always
post
and
I
cannot
tells
us
that
it
actually
failed
and
the
reason
for
that.
So
this
is
kind
of
like
an
old
bug
that
were
really
frequent
and
common.
A
In
old
version
of
solidity,
there
was
no
constrictor
keywords
and
where
you
were
doing
the
Constructor
that
you
needed
to
have
the
function
name,
which
was
a
match
with
the
contract
name,
and
here
you
have
the
contract,
ownership
and
a
function
owner,
and
because
of
that,
the
functional
is
a
public
function
and
anyone
can
call
it
and
become
the
owner.
This
does
not
work
anymore
with
more.
You
know
modern
version
of
solidity,
but
the
type
of
bug
that
we
are
finding
a
bit
more
a
bit
too
much
in
the
past.
A
Something
which
is
interesting
again
is
that
you
know
we
did
not
look
at
the
ownership
contract.
We
did
not
look
like
at
the
implementation
itself.
We
just
Define
an
invariant
and
without
the
one
of
the
further
one-
and
you
found
the
environment
for
us,
so
now
bring
the
question
on
how
to
define
it.
Okay,
foreign.
A
Okay,
so
the
question
is:
is
defining
invariant
part
of
the
auditor?
You
know
work,
yes
like
we
are
using
a
Kinder
in
our
audit
and
during
our
audit
we
are
going
to
Define
invariant
and
something
we
are
going
to
do
that
we
are
going
to
discuss
with
the
developer,
because
the
developers
know
you
know
better
than
us
what
the
system
is
supposed
to
do.
A
So
we
are
going
to
have
this
collaboration
with
them
to
understand
what
the
system
is
supposed
to
do
and
to
Define
this
variants,
foreign,
how
to
define
invariance,
because
you
know
like
if
you
have
bad
invariance,
it
doesn't
matter
what
you
are
doing.
You
know
if
you
are
using
further,
if
you
are
using
like
formal
method,
if
your
invariant
are
not
good
you're,
just
going
to
check
for
some
things
that
you
know
doesn't
matter.
A
A
Start
simple
start
with
invariants
that
you
know
you
know
are
true
start
with
things
that
are
not
working
once
you
have
5
or
10
simple
invariants,
buy
them
in
solidity
and
when
the
further
on
top
of
them,
if
the
invariant
are
all
holding,
then
you
can
go
back
to
thinking
about
the
event
of
the
system
and
you
know
go
more
deeper
into
into
the
environment
themselves.
If
something
is
broken,
then
look
if
the
invariant
is
incorrect
or
if
there
is
an
actual
bug
and
iterates
go
over.
B
A
Okay,
how
to
use
it
with
other
contract,
so
you
can
just
in
the
Constructor,
deploy
the
contract,
something
that
we
are
not
going
to
cover
here,
but
we
have
a
tool
which
is
called
itino,
which
is
basically
going
to
take
your
unit
test.
Take
like
your
suite
and
we
play
them
in
Echidna.
So,
for
example,
if
you
have
like
a
complex
integration
with
like
you
know,
you
are
deploying
in
your
unit
test
10
different
contracts.
B
F
So
there
is
case
was
we
have
a
special
I'm
from
gearbox
protocol
and
we
work
on
composable
Leverage
and
we
have
adapters
because
we
just
provide
leverage
for
some
other
contracts.
So
when
you
combine
gearbox
with
uni,
swap
you
get
immediately
margin
trading
and
in
this
case
it
has
adapters
and
these
adapters
incorrectly
Parts
path
to
make
check
after
uni
swap.
However,
they
integrated
and
may
call
to
existing
uni,
Swap
and
guy
who
were
on
immuneify
problem.
F
He
write
a
small
test
and
this
test
show
us
that
if
you
really
add
some
additional
part
of
call
data,
it
could
be
interpreted
incorrectly.
So
we
have
two
different
ones.
Our
system
could
be
fooled
check,
not
Z
balance,
which
should
be
checked,
and
in
this
case
it
was
a
fault
of
the
system
and
the
funds
could
be
drained
and
in
this
case
I
think
we
could
find
some
fuzzing
testing
to
really
provide
any
information.
F
But
this
test
should
work
with
uni
swap
because
we
behave
in
different
way
and
we
shouldn't
cover
that,
because
we
run
with
mocks
and
MOX,
of
course,
was
created
with
the
same
bug.
So
MOX
was
okay,
but
real
implementation.
Total
different
and
I
definitely
believe
that
fuzzing
should
found
this
mistakes.
Yeah.
B
Yeah
definitely
definitely
when
you
are
creating
a
mock,
you
are
assuming
how
everything
works,
and
if
your
assumption
is
not
precise
enough
it
will
it
will.
You
won't
be
able
to
detect
something
and
we
as
an
Auditors,
it's
it's
common,
that
we
have
to
audit
contracts
that
will
interact
with
other
other
contract,
let's
say
compound.
So
when
we
go
into
compound,
we
have
all
the
documentation
and
says
well
compound
word
like
this
or
like
that.
B
When
we
look
at
the
code
and
see
some
things
are
not
documented
and
we
go
back
into
the
developers
and
look
look
if
you're.
If
your
contract
is
doing
this
so
that
it
will
revert
and
you're
not
testing
for
that.
So
it's
when
you,
when
you
are
using
a
third
party
contract,
you
are
importing
the
risk
so
either
either
you
have
really
good
tests
or
you
even
make
sure
that
you
understand
everything.
Otherwise
it
will
be
difficult
to
catch
the,
but.
A
Yeah
I
think
this
type
of
work
can
be
found
with
fuzzing
like
the
most
like.
The
difficulty
is
going
to
find
initialization
that
makes
sense,
and
then
that
makes
sense.
That's
why
that's
why
you
know
we
are
kind
of
in
putting
like
the
infances
onto
defining
environment,
because
this
is
like
the
key
component
of
this
technique.
Yeah.
F
In
terms
in
terms
of
speed,
is
it
okay
to
put
all
deployment
script
into
Constructor
because
of
course,
if
you
deploy
such
a
huge
system
and
you
deploy
some
contracts
from
external
repositories
like
uni,
Swap
and
so
on,
it
requires
time
and
of
course,
when
you
want
to
test
million
operation,
if
you
redeploy
each
time
holds
the
system,
it
could
require
hours
or
days.
I
know.
B
Yeah,
so
so
so,
when
you
use
Echidna,
you
deploys
only
once
and
then
the
when
your
test
finish,
it
will
go
back
to
the
states
after
the
contract
is
deployed.
There's
no
need
to
redeploy
it,
and
that
is
why
we
have
we.
We
ask
the
developer
to
have
fixed
amount
of
parameters
in
the
deployment
right
on
the
on
the
on
the
Constructor.
Otherwise
we
will
know
what
what
we
should
deploy.
Yeah
I
think
there
is
a
question
over
there
also.
C
I'm
just
wondering,
as
you
once
you've
kind
of
defined
your
invariance
and
I.
Imagine
you
guys
in
your
audits,
you
you
run
through
these
and
basically
I'm,
not
trying
to
understand
when
you
guys
have
confidence
that,
yes,
the
this
is
a
good
invariance
from
and
and
if
there
are
any
metrics
that
you
guys
use
internally
like
I,
see
it's
outputting
Unique
instructions
and
unique
code
hashes
those
sorts
of
things
that
give
you
confidence
in
in
what
you've
done.
A
So
in
practice
you
know
you
can
look
at
the
coverage,
but
usually
coverage
is
not
a
good
indicator
and
In
fairness,
like
you
know,
when
we
do
that
we
do
this
in
a
time
box
manner.
So
we
have
two
or
three
weeks
to
do
it
and
we're
going
to
do
our
best
in
two
or
three
weeks.
That's
the
best
that
we
can
do
yeah.
B
It's
it's
it's.
We
there
is
no
Silver
Bullet
for
this
it.
We
when
we
do
a
report,
we
list
the
invariance
that
we
test.
So
it's
it's
clear
what
what
we
tested
and
what
and
everything
else
was
was
not
tested
with
all.
So
we
will
perhaps
did
Manual
review
or
use
all
the
techniques
like
Slither
to
check
some
some
other
things
but
yeah.
B
Unfortunately,
there
is
no
good
way
to
to
Define
this,
but
perhaps
I
I
personally
think
that
talking
with
the
developer
early
on
the
invariance,
it's
a
really
good
thing.
It's
usually
the
case
that
we
think
an
in
barrient.
Let's
say
that
some
some
value
cannot
be
zero
and
we
go
into
the
into
the
client
and
says:
is
this
an
invariant?
We
don't
know
because
we
have
not
designed
the
system
and
they
don't
know,
and
if
they
don't
know,
that's
that's
an
issue
right.
We
should.
A
G
A
Way.
Okay,
so
this
is
a
really
good
question
and,
in
my
opinion,
the
best
tool
to
find
way
on
Transit
is
static
analysis.
So
the
question
is
more
to
find
which
technique
you
should
apply
for
which
problem
and
for
things
like
Korean
transition,
static
analysis
is
just
going
to
be
better.
You
can
use
further.
You
can
create
like
random
callback
and
things
like
that,
but
in
practice,
static
analysis
is
just
going
to
outperform
any
further
this
work.
A
A
F
One
more
question:
what's
your
addition,
for
example,
we
have
a
complex
system
and
we
want
to
make
a
classical
fuzzing
with
the
kidnap,
and
it
seems
that
to
really
cover
many
cases,
it
requires
a
lot
of
computational
power.
So
maybe
can
you
advise
some
cloud
provider
or
how
to
do
to
run
it,
maybe
for
a
week
with
very
powerful
computer
to
get
something
achievable
because
of
course,
this
pretty
simple
contracts
could
be
found
on
my
MacBook.
But
if
we
go
a
little
bit
further
many
contracts,
many
setups,
maybe
it
requires
more
computational
power.
A
B
B
So
the
second
thing
is:
every
we
have
a
python
companion
tool
called
in
a
parade
that
will
run
echina
in
any
number
of
any
number
of
concurrent
instances.
So
you
can
run
10
at
a
time,
but
we're
not
only
going
to
run
it
10
of
the
time,
but
we
are
going
to
randomly
Shuffle
parameters
because
in
some
cases
there
are
some.
B
There
are
some
issues
that
can
be
easily
found
with,
let's
say
three
or
ten
transactions
and
some
other
issues
are
going
to
be
more
easily
found
with
two
200
transactions
in
a
in
a
in
a
row
right.
So
what
we
do
is
we
run
the
tool
in
different
with
different
random
parameters
and
in
different,
let's
say
Generations,
so
we
run
we
run
akina
for
an
hour
10
times.
Then
we
save
the
Corpus
and
you
can
get
you.
B
You
can
see
all
the
all
the
all
the
code
that
was
covered
and
then
we
started
again
but
taking
the
the
the
output
of
the
previous
generation,
so
you
iterate
over
and
over
again,
so
you
can
see
how
your
code
is
explored
right
or,
if
there's
some
part
of
the
code
that
is
not
explored
with
10
different
instances.
You
can
go
back
and
say
no
I
need
I
need
to
change
this
because
it
doesn't
depend
on
the
on
the
actual
execution.
So
we
can.
We
can
give
you
the
link
for
that.
A
Okay,
so
yeah
like
it's
really
about
spending
time
and
thinking
about
our
invariants,
and
it's
not
simple
like
it's.
The
first
invariant
that
you
are
writing
leads
to
a
bugs.
There
is
something
wrong
about
your
approach.
You
should
not
have
like
simple
invariants
that
you
know
are
going
to
work
the
system
so
we'll
start
simple
and
iterate
over
them.
A
Okay,
to
give
you
some
example,
let's
say
you
have
a
now
with
magic
libraries.
What
environment
can
you
have?
You
can
have
commutative
properties?
A
plus
b
is
equal
to
B,
plus
a
you
can
have
identity.
A
one
multiplied
by
two
should
be
true
our
inverse.
If
you
add
something
by
its
opposite,
it
should
be
zero.
This
is
not
always
true
right,
but
depending
of
what
you
are
building,
this
might
be
like
the
type
of
property
you
are
looking
for
for
token.
We
already
talked
about
the
first
one.
A
No
no
user
should
have
a
balance
above
total
Supply.
Let's
say
you
want
to
look
at
the
transfer
function
and
patsync
transfer
function.
What
does
it
do?
I'm
transferring
token
to
someone
so
at
the
end,
my
balance
should
have
decreased
by
the
amount
and
the
receiver
should
have
see
its
balance
increased
by
the
amount.
And,
let's
say
you
try
to
write
something
like
that
once
you
might
quickly
realized
that
what
happened
if
the
destination
is
myself.
So
if
I
transfer
token
to
myself,
my
balance
is
not
going
to
increase
or
decrease
quite
awfully.
A
So
this
is
an
example
where
you
might
try
to
Define
an
invariance
on
transfer.
It
might
seem
simple.
You
might
write
like
the
the
thing
in
solidity
and
if
you
do,
that
again
is
going
to
tell
you
that
there
is
an
edge
case
where,
if
you
transfer
to
yourself
like
the
event,
is
going
to
be
to
be
broken
and
in
this
example,
if
you
go
through
this,
it's
not
the
code,
which
is
bad.
It's
an
invariant.
That
was
bad.
A
Something
else
which
is
also
important
to
to
consider
is
patterning.
First,
reverting,
for
example,
an
environment
you
can
have.
Is
that
if
you
don't
have
enough
phones,
the
transfer
function
to
the
revert
or
a
return
first,
depending
on
how
you
implemented
the
token,
once
you
have
this
list
of
invariants,
usually
you
can
split
invariant
into
two
categories.
A
Function
level,
invariant
system
level,
invariant
function
over
invariant
are
usually
stateless.
They
are
things
that
you
can
just
you
know,
look
at
a
specific
function
and
try
to
see
if
it
holds
so
it
may
take.
You
know.
Environment
I
mentioned
are
stateless
and
our
functional
leveling
variants.
Here
you
can
craft
simple
scenario.
Just
by
calling
the
specific
function,
then
you
have
system
level.
In
there
system
level
environments
are
usually
more
complex,
but
they're
also
more
powerful,
and
here
you
are
stateful.
A
You
are
going
to
change
the
state
of
the
contract
and
you
are
going
to
try
to
see
the
environment
no
matter
the
state,
and
here
is
why
it's
important
that
echina
is
calling
all
the
different
function,
because
it's
actually
what
you
want
to
try
the
balance
being
below
or
equal
to.
The
total
Supply
is
an
example
of
a
system
level.
Invariant.
A
One
thing
that
you
can
use
is
a
different
modern
incidence
of
calling
Akinator
underscore
something
we
support
a
session.
So
you
can
just
create
function,
put
assertion
and
try
to
see
if
it
holds
a
SIM
for
system
level
environment,
as
we
kind
of
already
like
discuss.
It
might
be
more
complex
depending
on
the
initialization
of
your
system.
B
All
right,
so,
let's,
let's
see
this
particular
piece
of
code,
let's
take
half
a
minute
to
read
it:
it's
it's
basically
a
buy
function
that
will
call
an
internal
function
valid
by.
So
what
we
are
going
to
do
is
we're
going
to
think
what
are
the
type
of
invariants
that
we
can
have
here
and
what
what
is,
what
will
they
are
going
to
test
and
what
type
of
guarantees
we're
going
to
get
from
this?
So,
let's,
let's
take
a
few
few
seconds
for
this
foreign?
B
Okay,
so
the
question
is
testing
timestamp
dependent.
So
it's
clearly
not
not
the
case
here
for
timestamp
depending
code,
a
kid
now
when
it
runs
it
automatically
increase
either
the
block
number
or
the
block
timestamp
inside
some
range
right,
because
it
it
happens
that
some
code
will
fail
when
the
timestamp
is
increased
into
a
really
really
large
number,
but
yeah
100
years
or
like
the
end
of
the
universe.
B
F
The
first
one
we
can
understand
that
how
much
token
how
many
tokens
we
can
get
as
a
result
follows
our
expectation
when
we're
sending
message
value
because,
as
you
can
see,
it's
a
hard-coded
rate
is
around
10.
So
basically
it's
a
pretty
simple
formula:
we
can
change
different
values
we
put
into
the
function.
We
have
totally
prediction
how
much
we
can
get
and
then
we
can
try
to
verify
that
it
works.
B
Yes,
exactly
so,
the
the
property
is
related
with
the
amount
that
we
can
get
even
the
number
of
weight
that
is
sent
so
yeah
we
can
so.
The
first
thing
is
this:
this
code
will
depend
on
the
state.
We
don't
have
the
mean
function,
so
we
don't
know
what
is
what
is
inside,
where
we
have
the
valid
buy
function.
That
is
actually
abstracting
the
thing
that
we
want
to
that.
We
want
to
test,
so
we
will
start
with
valid
by
which
is
a
pure
stateless
function.
B
Yes,
so
we
were
thinking
about
invariance
here
related
with
the
amount
that
we
can
get
so
this
is.
These
are
very
simple
without
going
into
specific.
This
is
a
very
simple
invariant.
If
the
amount,
if
the
Wayside
in
C
is
zero,
then
the
user
should
receive
no
tokens
at
all
right.
So
so
that's
it's!
It's
even
simple
and
thinking
how
how
much
well
I
a
user
should
receive,
but
it's
a
Concrete
case
and
it's
it's
kind
of
a
corner
case,
so
it's
it
can
be
important
to
test
all
right.
B
So
how
we
can
test
this.
So
there
are
a
couple
of
way
to
test
it.
This
is
this
is
one
so
we
we
can
write
a
function
that
will
take
one
parameter
so
again,
I
will
put
any
any
number
there.
However,
we're
going
to
restrict
the
number
the
input
of
this
function
to
be
non-zero,
then
we're
going
to
execute
valid
by
and
then
we
want
to
know
if
echina
can
reach.
He
can
reach
the
the
statement
after
that,
because
valid
by
Will
revert.
B
And
so
perhaps
you're
wondering
what?
If
what
if
the
ceremony
is
zero,
then
clearly,
this
code
will
not
do
anything
interesting,
so
she
was
just
is
going
to
revert
when
you're
writing
tests
you
need
to
so
you
can
put
any
any
amount
of
requires
or
preconditions
or
people
usually
call
it.
However,
if
you
put,
if
the
preconditions
are
too
restrictive
and
your
your
function
reverts
most
of
the
time,
it
means
like
you're
not
going
to
get
value
from
the
execution,
so
every
execution
reverted
in
a
test
in
an
invariant.
B
B
So
it's
not
a
big
deal,
but
if
you
have,
if
you
put
a
lot
of
requires
that
only
a
very
small
small
amount
of
values
well
satisfied
and
it
will
be
difficult
to
get
randomly
or
even
even
with
the
with
the
techniques
that
we
use,
you
will
need
a
slightly
different
approach,
but
yeah
we
will.
We
will
then
go
later
into
that,
so
any
any
questions.
B
B
B
It's
another
thing
and
fasting
techniques
are
going
to
sample,
let's
say
randomly
from
the
from
the
input
or
with
hubs
right
it's
in
the
case
of
Echidna,
since
we
are
going
to
compile
this
code
and
it
will
run
through
or
static
analyzer,
we
will
detect
some
interesting
values
in
this
case
10,
for
instance,
10
10
is
an
interesting
value
there,
it's
a
it's
a
constant
and
it's
going
to
be
used
somewhere.
So
definitely
we
want
to.
We
want
to
test
with
that
constant
okay.
B
So,
let's
see
what
happens
if
we,
if
you,
if
you
run
so
this
is
so
kinda
will
run
a
number
of
transactions.
It
will
eventually
detect
that
assernal
free
token
has
an
assertion
failure.
However,
this
is
going
to
be
in
a
context
of
100
of
transactions,
random
transactions
that
perhaps
will
do
something
that
is
completely
unrelated.
But
what
we'll
do
is
input
minimization
input.
Minimization
is
a
very
old
technique
referred
to
testing,
in
which
you
have
a
list
of
bytes.
That
affects
a
bug.
B
You
want
to
remove
that
bytes
one
by
one
or
in
some
random
way,
in
order
to
get
a
a
list
of
bytes
that
will
still
trigger
the
bug,
but
it's
going
to
be
minimal
or
or
either
local
or
a
global
minimal,
depending
on
the
type
of
tool
that
you're
that
yours.
So
in
this
case
we
can,
a
kidnap
will
try
to
minimize
any
any
parameter.
Here.
We
have
only
one
parameter
and
the
parameter
is
actually
is
actually
going
to
be
useful
triggering
about.
B
If
we
have
more
parameters,
they
are
going
to
be
minimized
towards
zero.
So
if
you
have
units,
then
it
will
be
reduced
until
zero.
So
zero
is
the
simplest
value.
This
is
arbitrary,
defined
on
the
on
the
code.
You
can
you
you
can
change
it
if
you
want,
and
but
in
this
case
the
parameter
cannot
be
zero,
because
if
it's
zero,
the
the
test
will
pass
right.
B
So
in
this
case
the
minimal
amount
is,
is
one
it's
not
guaranteed.
That
you
will
always
get
this
smallest
set
list
of
transactions
to
trigger.
This
is
an
an
MP,
complete
problem.
It
cannot
be
solved
on
on
linear
time,
so
it's
it's
all
going
to
be
always
a
sample,
but
in
in
practice
even
randomly
sampling,
removing
transactions
or
reducing
the
complexity
of
each
value
will
will
give
you
good
answers
all
right,
so
a
little
bit
about
ekina
apis,
maybe.
A
Issue
here
is
that,
if
you
send
one
desire
token,
what's
going
to
happen,
is
that
you
do
one
divided
by
10
and
1
divided
by
10
is
0
because
you
are
winding
down
and
other
results.
The
required
amount
to
be
sent
is
zero.
So
if
you
ask
any
number
of
tokens
below
10,
you
are
going
to
get
them
for
free,
and
this
is
again
again
an
example
where
we
Define
an
invariant.
We
don't
actually
look
at
the
formula.
We
are
not
looking
at
how
this
formula
works.
A
B
E
E
B
Yeah,
if
I
understand
it
correctly,
so
this
this
could
be
an
internal
part,
and
you
can
have
like
a
lot
of
code
that
put
like
gets
the
value
from
them
from
the
message
value
and
then
do
something
else
you
can
do
that
yeah
I
mean
I
mean
is
this
depends
on
on
your
code.
Here
we
are
testing
an
internal
function
right
using.
E
B
F
What
I'm
really
wondering,
because
we
talk
about
this
error,
whoever
tokens
less
than
is
so
way
less
than
it's
so
small
amount
and
the
same
problem
which
could
be
here
is
Overflow
if
I
provide
a
huge
amount
of
ease,
because
we
have
a
multiplication
to
decimals,
it
could
be
done
on
the
other
side.
We
all
of
us
know
that
the
quantity
of
s
is
limited.
F
You
can't
even
take
a
flash
loan
and
get
more
ease
than
it
produce.
So
what
is
the
best
practice?
Follow
this
formal
execution
when
you
write
fuzzing
tests
or
take
some
real
examples
as
limitations
as
there
is
no
match
as
zeroom
as
it
exists
at
the
moment,
and
we
know
it's
a
deflation,
so
we
can
simply
assume
that
in
the
future
nobody
could
take
so
much
to
get
overflow
here.
Yeah.
B
Yeah
exactly
so
yeah
this
is
is
an
interesting
question
and
it
goes
into
the
fact
that
what
are
your
assumptions
on
the
test
right,
if
you,
if
your
assumptions
are
like
I,
have
this
token,
with
this
limited
Supply
that
should
never
go
over
something,
then
you,
you
can
just
say,
I
require
that
that
the
value
sign
cannot
be
more
than
the
total
supply
of
something
right.
But
in
the
case
of
interest,
is
a
bit
more
tricky
and
and
in
fact,
in
in
Echidna,
what
we
do
is
we
have.
B
We
have
externally
on
accounts
that
are
simulated.
We
loaded
with
eater
every
at
every
transaction,
because
you
can
have
a
very
large
amount
of
feature.
You
can
take
a
flat
loan.
You,
you
probably
cannot
have
as
enough
eater
to
overflow
you
into
256,
because
that
will
be
a
real
issue
for
the
AVM
in
in
itself,
but
we
can.
We
can
Define
in
the
Kinder
config,
which
is
the
maximum
amount
of
value
that
we
send
per
transaction
right.
B
So
if
you
put
like
I,
don't
care
if
the
attacker
has
more
than
than
10
000
liter,
because
that
will
mean
that
they
can
do
other
things,
then
Echidna
will
happily
take
that
limit
and
will
never
put
something
more.
However,
it's
still
the
case
that
over
several
number
of
transactions,
the
accumulate
number
of
features
can
go
over
that
that
barrier.
So
you
should,
you
should
be
careful.
A
So
either
you
start
where
the
invariant
has
really
limited,
Twitter
like
really
with
chain
one,
and
you
try
to
see
if
it
hurts.
If
it's
working
with
like
a
you
know
like
with
one
meter:
okay,
it's
already
working,
so
you
can
continue
like
this.
If
it's
not
breaking,
then
you
can
increase
this
with
time
from
time
to
time
or
you
can
take
the
opposite
approach.
If
you
define
an
invariant
where
the
threshold
is
really
large,
it's
working
because
it's
really
large
and
then
you
decrease
this
result.
B
The
if
we
start
with
very
large
values
we
we
could
have
false
positives,
but
and
if
we
start
with
very
small
values,
we
can
have
a
false
negative,
but
which
are
the
ones
that
are
going
to
cause
you
more
trouble.
That
is
something
to
to
think
about
it,
because
if
you
miss
one's
false
positive,
your
your
protocol
can
be,
you
know,
destroyed,
and
if
you
miss
one
one
false
negative,
then
it's
okay,
all
right.
I
A
B
Yes,
there
are
some.
There
are
some
techniques.
I
can
show
you
a
little
bit
after
a
few
lines
of
the
code
of
Akinator
that
shows
all
limitations.
We
have
mutation,
interesting
mutations
on
list
of
transactions
in
which
we
Shuffle.
We
do.
We
do
like
splice
as
well,
so
we
take
a
list,
a
list
of
Interest
transaction
and
another
one
and
we
splice
it
on
a
random
position.
So
there
are
a
couple
of
fun
things
to
to
look
at,
but
yeah
I
think
we
should
move
on
a
little
bit
all
right.
B
So
as
I
was
saying,
we
have
this
failing.
Even
if
you
don't
understand
what
was
what
is
the
failure?
Well,
that
is,
that
is
a
different.
There
is
a
different
Beast.
Sometimes
you
you,
you,
have
you
put
your
your
your
invariant
and
your
invariant
feels,
and
then
you
start
the
journey
to
understand
why
it
fits
so
that's
we
are
not
going
to
talk
about
that.
You.
Some
people
like
to
re-u,
run
We
Run,
The
failure
into
a
unit
test
to
make
sure
step
by
step.
B
What
is
what
is
going
on,
but
yeah?
That's
that's
a
completely
different
type
of
Beast
that
is
related
with
what
happened
after
and
how
we
can
fix
how
we
can
fixation
all
right
so
a
little
bit
about
ekin
apis.
This
is
a
topic
that
it's
it's.
It's
still
an
open
debate
in
some
in
some
cases.
So
what
are
the
best
way
to
test
to
create
properties?
So
Echidna
supports
a
couple
different
ones:
it's
about
Boolean
properties
in
which
a
function
is
executed
and
then
it
will.
B
It
should
return
a
Boolean,
true
or
false,
and
if
the
function
reverts
for
any
reason,
that
is
the
same
as
returning
false
right.
So
if
we
go
back
a
little
bit,
we
can
see
over
there
error
and
recognize
op
code
that
is
going.
That
is
related
with
the
assertion.
Failure
this.
That
is
how,
on
version
of
solidity,
used
to
have
this
assertion
failures.
But
if
you
use
Boolean,
you
will
just
say
return
false
right,
so
you
know
exactly
how
how
everybody
fail
or
it
could
be
a
revert.
B
So
you
you
say
over
there
you
see
over
there.
It
revert
okay,
so
either
you
do
Boolean
properties,
which
are
the
classic
way
to
define
invariants,
and
these
come
from
some
some
real
old
techniques,
in
particular,
quick
check,
which
is
which
is
a
property
based
testing
tool
for
Haskell
and
then
a
couple
of
other
languages,
which
was
an
inspiration
for
for
for
this.
Then
you
have
assertion
failure
so
every
time
you
see
every
time
the
the
assertion
is
called
with
false.
That
is,
that
will
fail.
B
B
So
there
is
testing
modes
in
the
in
the
in
a
repository,
so
we
can,
you
can
go
there
and
it's
explained
a
little
bit
more.
This
is
very
high
level
overview,
so
yeah
yeah
yeah,
so
so
so
yeah
again,
that's
something
returnable
Boolean,
it's
easy
to
Define,
no
side
effects,
that's
that
that
is
so
interesting.
When
you
use
Boolean
properties,
all
the
side
effects
will
be
reverted
before
the
execution
of
the
actual
invariant
right.
B
B
It
will
also
be
easy
to
see
on
the
code
coverage
if
it's
not
if
it's
not
covered
or
or
not.
However,
some
code,
especially
some
old
piece
of
solitary
code,
it's
going
to
have
assertion
as
required,
and
that
is
a
really
bad
thing
you
should
not
be
doing
it
use
require
if
you
want
to,
if
you
want
to
actually
have
a
precondition
in
your
call
and
use
assertion
for
for
testing,
okay
yeah
and
finally,
we
have
the
The
Foundry
and
up
compatibility.
The
only
thing.
B
Well,
the
thing
that
we
don't
support
is
pranks.
So
we
don't
like
to
prank
people.
So
we
don't,
we
don't
support
pranks.
However,
we
support
some
of
the
some
of
the
havm
yeah,
the
havm,
the
original
ones
cheat
codes.
You
should
be
careful
using
it.
We
we
know
that
there
are
some
catch
with
that,
especially
related
with
what
the
solid
compiler
expects
and
what
you're
doing
in
your
in
your
transaction.
B
B
If,
if
the
community
agrees
that
we
need
a
specific
cheat
code
or
we
need
to
avoid
some
specific
chicken,
then
we
are
open
to
discuss
it
all
right,
so
exercise
four
we're
going
to
deal
with
one
of
the
one
of
the
exercise
for
dumb
vulnerable
defy.
So
how
many
of
you
know
this
amazing
CTF,
yeah,
sorry,
you
you.
A
B
B
Echina
will
only
target
a
specific
contract
that
you
can
put
in
on
on
your
command
line,
or
if
you
have
only
one
contract,
you
will
use
the
first
one
right,
but
there
is
something
called
multi-avi
that
would
call
every
every
contract
that
is
deployed
after
the
Constructor
that
you
have
Avi
right.
So
if
you
deploy
something
in
bike
in
by
code
directly
and
you
don't
have
Avi
in
the
won't
be
able
to
call
it
because
it
doesn't
know
what
is
what
is
there?
B
But
if
you,
if
you
deployed
a
couple
of
tokens
and
several
contracts
and
you
use
multi,
API
Echidna
will
call
any
function
in
any
deploy
contract
after
after
the
the
end
of
the
Constructor.
So
we
will
need
these
in
order
to
deal
with
the
next
example,
because
sometimes
the
the
the
the
debug
that
you
want
to
detect
it
doesn't
depend
on
the
state
of
one
contract.
B
It
depends
on
the
state
of
many
contracts,
and
in
that
case
you
can,
you
can
be
surprised
by
the
fact
that
changing
the
state
in
another
contract
can
break
your
your
property,
and
definitely
we
want
to
avoid
that
Okay.
So
again,
how
many
of
you
know
about
them
vulnerable,
defy,
okay,
a
good
number,
and
did
you
actually
well?
This
is
these.
Are
the
first
exercise,
the
first,
the
first
two
so
I
hope
that
people
know.
B
B
A
A
I
can
allow
you
to
take
a
Flash
run
for
a
fee,
and
you
have
a
second
contract,
which
is
a
user
contract
that
is
going
to
interact
with
a
pool
and
the
contract
is
going
to
be.
The
user
contract
is
going
to
be
deployed
with
some
fund
inside
and
the
girl
is
going
to
try
to
see
if
it's
possible,
for
this
specific
contract
from
the
user
to
be
joined.
B
We
we
want
you
to
review
the
the
the
exercise.
If
you
have
already
did
it,
it
requires
you
to
send
some
some
some
some
number
of
transactions.
So
in
this
case
we
are
going
to
prepare
everything
for
a
kidnap
to
ReDiscover
this
without
telling
it
what
is
what
how
how
it
can
be
sold,
so
we
will
need
two
things.
We
will
need
to
initialize
the
the
code
to
have
too
much
what
the
what
the
initialization
is.
It's
is
actually
showing
us.
B
Let's
see,
okay,
so
this
is
the
The
Flash
loan,
the
part
of
the
or
the
flash
loan.
So
the
the
interesting
part
about
this
is
we
don't
have
to
care
about
specific
details
in
the
code
we
want
to.
We
want
to
give
a
kid
now,
the
same
scenario
that
we
have
on
the
on
the
actual
Challenge,
and
we
want
to
know
if
it
can
actually
find
a
way
to
drain
the
contract
so
yeah
we
can.
We
can
see
how
the
reciprocal
function
works
here,
but
yeah.
B
A
B
There
there
is
an
alternative
way
to
do
it,
but
the
solidity
approach
is
is
easier
to
to
avoid
because
well,
the
other
tool
is
called
atino
that
can
replay
this
in
a
simulated
blockchain
like
ganache
and
then
send
it
to
the
to
the
tool.
So
in
that
case
you
don't
need
to
replace
on
solidity
manually,
but
you
are
still
I
still
know
still
need
to
know.
Where
is
everything
deployed
right?
So
if
you
want
to
interact
with
the
pool
you
need
to
know,
where
is
which
is
the
address
of
the
pool?
A
B
So
yeah
the
the
previous
exercises
are
on
the
easy
side.
This
is
a
bit
more
difficult,
but
still
shouldn't
require
more
than
a
few
lines,
so
yeah.
But
please
let
us
know
if
you,
if
you
need
some
some
hints
there
are
some
hints
in
in
one
of
the
one
of
the
branches
in
the
hint
Branch,
but
yeah
Heather.
I
B
G
Yeah
I
have
kind
of
high
level
questions,
so
I'm
trying
to
think
about
what
the
limitations
are
in
terms
of
expressing
properties
as
invariance
right.
So,
for
example,
let's
say
we
have
a
temporal
property
that
we
want
to
express
like
we
have
a
wallet
contract
and
we
want
to
be
able
to
say
that
any
user
who
deposits
their
money
is
eventually
able
to
withdraw
it.
Is
that
just
like
a
fundamental
limitation
of
Echidna,
or
is
there
a
way
to
so?
If
you
can.
B
So
the
notion
of
eventually
it's
you,
you
need
to
have
some
definition
on
the
or
on
the
blockchain
right.
So
eventually
cannot
mean
like
in
100
years
right.
So
if
you,
if
you
find
say
I,
will
only
allow
increment
of
time
up
to
some
limit.
Yes,
you
can,
you
can
call
it
as
a
bounded
version
of
that
property,
but
you
cannot.
You
cannot
use
it
as
a
theoretical
thing.
B
Like
you
know,
I
have
a
state
which
I
don't
know
what
it
is
and
then
I
will
transition
to
another
state
which
I
don't
know
which
what
it
is,
and
in
that
case
you
will
need
to
know
if
the
original
state
was
actually
possible
and
and
things
like
that,
so
it
kind
of
works
on
on
a
concrete
on
on
concrete
States.
So
you
always
have
concrete
data
and
you
need
to
put
like
boundaries
on
the
things
that
you
that
you
can
do.
B
G
B
You
you
will,
you
will
do
something
like
this.
You
will
put
a
function
that
says
and
and
you
will
need
a
state
to
track
down
like
you,
you
do
a
deposit
and
you
will
need
a
user
to
eventually
receive
something
right,
so
you
will
need
to
have
a
state
that
tracks
deposit
like
a
mapping
right
and
you
have
a
function.
That
is
your
invariant.
So
if
and
then
you
receive
the
address
of
a
user
and
you
check
in
the
mapping.
B
It
so
yeah,
you
will
you
so
if
the
if
the
property
that
you
are
testing
requires
to
add
State,
yes,
you
will
need
to
add
whatever
state
is
needed,
it
won't
be
able
to
track
state
outside
right.
The
only
thing
that
will
be
tracked
outside
is
the
increment
between
between
the
different
blocks,
for
instance,
so
that
that
will
be
tracked
outside
a
new
Aquino
will
show
you
from
in
between
this
transactions,
and
this
transaction
I
have
10
blocks
that
will
be
tracked
outside,
but
everything
else.
B
Let's
say
that
you
have
three
parameters
and
you
need
a
deposit
that
has
that
has
digital
parameter
in
in
in
the
Sim
in
the
same
number
or
in
numbers
in
which
in
which
are
difficult
to
find.
You
can
have
this
piece
of
code,
but
it's
important
to
let
the
kidnap
to
explore
freely,
at
the
same
time
that
you
are
allowing
information.
B
But
at
the
same
time
you
want
to
allow
the
tool
to
explore
things
that
you
don't
expect,
because
if
you
just
restrict
says,
I
only
expect
users
to
do
these
type
of
deposits,
then
you
can.
You
can
be
surprised
later,
because
there
there
is
a
way
to
break
your
your
property
using
things
that
you
don't
expect.
A
And
it
comes
down
to
the
previous
question:
where
either
you
start
with
a
lot
of
requirements
and
a
lot
of
you
know
restriction
in
what
you
are
trying
to
explore
and
if
it
odds
you
are
going
to
remove
some
of
the
restriction
or
you
start
this
opposing
Direction.
You
don't
have
any
restriction
and
you
know
you
go
more
and
more
restricted.
B
B
B
E
B
So
we
don't
actually
need
to
follow
exactly
what
the
exercise
says
about
draining
completely
the
contract.
If
we
have
one
transaction
that
allows
you
to
reduce
the
balance
of
the
receiver,
then
then
it's
then
something
is
wrong
and
definitely
it
will.
It
will
eventually
be
drained
so
yeah
so
quickly.
If
you
run
it,
you
will
see
something
like
this
in
which
well,
the
deflection
has
a
has
a
parameter.
That
is
the
the
borrower
and
we
can
control
this
to
in
order
to
reduce
the
amount
of
balance
all
right.
A
Yeah
we're
the
second
exercise
on
them
ruinable
D5,
but
we
are
running
out
of
time.
This
idea
was
the
same.
We
are
defining
an
initialization
which
was
a
bit
more
complex
and
if
you
go
through
this
exercise
with
something
a
bit
more
specific
is
that
there
is
a
callback
from
the
contract
to
the
caller.
So
on
the
Kindle
test,
you
need
to
have
like
also
the
Callback
to
implement
the
flashlight,
but
yeah.
A
A
This
funnel
might
be
a
bit
better
for
simple
tests
and
for,
like
you
know,
ease
of
useful
like
the
first
invariant,
because
they
are
integrated
within
the
compilation
framework,
but
in
the
long
run
they
might
not
be
as
powerful
as
a
Kinder.
Simply
because
we
have
you
know
user
Kinder
for
a
couple
of
years
and
we
have
tuned
it.
You
know
where
that
it
provides
the
best
value
that
we
can
do.
I'll
get
finished,
okay,
sorry,
yeah,
okay,
so
I
hope
you
enjoyed
the
workshop.
A
J
Yes,
I'm
gonna
present
you
storage
proofs
and
explain
why
they're
cool
how
to
work
with
them.
Why
you
need
to
link
to
work
with
them
and
yeah
a
bunch
of
other
things?
Why
is
it
even
possible
all
the
complexities
behind
the
trade-offs
and
so
on?
So
a
few
words
about
storage
Crews?
Why
I
really
believe
that
they
are
cool,
especially
nowadays
so
might
as
this
is
that
ethereum
is
pretty
sharded
nowadays
and
with
storage
truth,
we
can
essentially
read
the
state
in
a
almost
synchronous
manner,
which
is
a
pretty
pretty
nice
thing
to
do.
J
Given
the
circumstances
yeah
and
maybe
also,
let
me
explain,
why-
is
it
even
possible?
So
story
is
essentially
this
idea
that
the
entire
state
is
committed
in
a
cryptographic
manner,
using
some
data
structure
like
Miracle
trees,
Marco
Patricia,
trees
and
so
on
and
yeah.
We
can
essentially
verify
any
specific
piece
of
State
at
any
point
in
time
on
any
domain,
which
is
pretty
nice
and
does
introduce
additional
trust
assumptions.
J
You
just
rely
on
the
security
of
like
the
base
chain,
so
yeah,
that's,
like
storage
proofs
tldr,
where
they're
cool
now
a
bit
of
like
sponsored
section
of
sponsored
sections.
So
what
we're
doing
at
harvardus,
so
our
like
goal
is
to
make
smart
contracts
sell
for
in
a
way
by
providing
access
to
historical
state.
J
We
like
I,
said,
might
as
this
is
that
ethereum
is
pretty
short
that
nowadays
we
want
to
unchart
it
by
using
storage
proofs,
and
we
want
to
enable
synchronous
data
reads
because
today
we
do
not
have
really
nice
ways
to
make
synchronous
data
access
without
introducing
New,
State
new
trust
assumptions,
so
yeah,
that's
we
do
and
how
we
achieve
that.
We
achieve
that
by
using
obviously
storage
proofs,
we
use
snark,
Starks
and
NPC
I
will
get
why
we
even
use
all
this
tooling,
but
first
a
few
words
about
storage
rules.
J
What
these
are
and
and
so
on.
It's
so
tricky.
Actually
I
I
need
to
be
multitasking,
okay.
So
what
we're
gonna
cover
in
today's
Workshop?
So
all
the
basics
required
to
like
understand
properly
this
primitive,
how
to
like
work
with
it.
How
you
can
generate
these
proofs,
why
they're
pretty
useful
and
how
actually
you
can
access
this
commitments?
I'll
get
later,
what
we
call
the
commitment
in
a
process
manner
and
how
we
make
smart
contracts
software
and
enable
historical
data
reads
cool.
J
J
Just
a
very
quick
reminder:
I
hope
it
will
take
less
than
a
minute
like
generalized
blockchain
Anatomy,
how
I
ethereum
header
looks
like
why
ethereum
they're,
not
like
pretty
on
only
like
ethereum
focused,
however
I
think
that,
for
the
sake
of
this
Workshop,
it's
the
best
to
like
present
on
this
concrete
example,
Miracle
trees,
explain
me
like
on
five
I
will
just
quickly
explain
the
idea,
how
it
works
and
what
is
America
Patricia
tree
without
really
going
too
much
into
digitals
yeah.
Finally,
no,
not.
Finally,
the
anatomy,
the
ethereum
state.
J
It's
pretty
important
to
like
deal
with
this
with
this
primitive
and
finally,
how
to
deal
with
the
storage
layout
cool,
so
touching
function.
Essential.
Is
this
idea,
essentially
it's
this
idea
that
I
can
have
a
function
that
takes
some
input
of
any
size
and
it
always
always
return
an
output
of
a
fixed
size
and
now
what's
also
important.
There
is
no
input.
There
are
no
two
inputs
that
will
generate
the
same
output
and
you
cannot
reverse
the
hashing
function.
J
So
it
means
that,
given
the
output,
you
don't
know
what
is
the
input,
and
this
is
not
what
we
call
like
Collision
resistance,
pretty
useful,
primitive,
like
used
in
blockchains,
I,
will
and
I.
Think
that's
that's
pretty
much.
What
I
assume
that
everyone
is
like
familiar
with
like
yeah?
Okay?
Why
is
it
important.
J
So
generalized
blockchain
Anatomy,
so
why
we
call
it
a
chain
because
we
have
a
bunch
of
blocks
mined
together
like
linked
together,
because
each
block
contains
the
reference
the
parent
hash
and
the
previous
header
contains
the
reference
of
the
parent
hash,
which
is
pretty
cool,
and
let
me
remind
what
the
hash,
the
parent
hash
or
the
block
hash
of
on
ethereum
is
it's
essentially
the
hash
of
the
header
pretty
important
to
deal
with
this
Primitives
and
make
smart
contracts
software
so
accessing
six
Oracle
state.
Do
you
just
keep
that
in
mind?
J
Let's
get
to
the
next
part,
so
no
I
think
I'm
missing
one
slide.
No,
it's
the
correct
one!
Okay!
So
this
is
an
ethereum
block
header,
as
I
said,
we're
gonna
go
through
the
example
of
ethereum,
concretely,
so
a
bit
of
anatomy
so
to
access
State.
Obviously
we
need
the
state
route.
What
is
the
state
route
is
the
root
of
the
miracle
Patricia
tree
of
the
ethereum
state.
We
also
have
the
transactions
rule,
which
is
pretty
useful.
J
If
you
want
to
access
historical
transactions
like
their
entire
body
and
receive
truth,
so
it's
really
useful
to
access
any
events.
Logs
and
and
so
on,
and
all
of
these
are
like
root
of
the
American
Patricia
tree
America
Patricia,
3's,
America
3,
just
think
of
it
in
that
way,
and
most
importantly,
we
have
the
parent
hash
and
with
the
parent
hash,
we
can
in
a
way
go
go
backwards.
J
I
think
that's
it.
Let's
get
to
Miracle
tree.
So
essentially
it's
this
idea
that
I
can
take
whatever
amount
of
data
and
I
can
commit
it
in
a
cryptographic
manner
by
using
this
data
structure.
So
on
the
left
side,
we
see
a
standard
Merkle
tree.
So
essentially
all
the
data
goes
to
the
bottom
and
we
essentially
hash
it.
You
know
what
the
hashing
function
is.
Then
we
combine
these
two
hashes
together
with
hashtag.
J
We
keep
doing
that
until
we
get
to
essentially
one
hush,
and
this
is
what
we
call
the
root
mark
up
to
three
shot:
three
modified
Miracle,
Patricia
2,
to
be
exactly
the
data
structure
that
we
use
in
ethereum.
What
you
see
here,
I
hope
you
see
on
the
top.
We
have
the
state
route
and
essentially
the
state
route
is
the
root
of
this
tree
and
now
how
it
works
and
how
you
should
think
of
this
of
this.
It's
a
pretty
complex
data
structure.
J
I,
don't
want
you
to
bother
with
it
today,
but
essentially
we
have
three
types
of
like
notes:
we
have
Leaf
nodes,
extension
notes
and
Branch
notes,
so
Leaf
nodes
contain
data.
Branch
nodes
contain
data
and
extension
nodes
like
on
the
high
level,
just
help
us
to
like
sort
of
navigate
in
that
tree,
but
to
be
honest,
to
deal
with
storage
truth,
you
don't
really
need
to
understand
this
part,
but
to
like
build
on
the
low
level
as
we
do.
Obviously,
we
need
to.
J
We
need
to
do
pretty
pretty
a
lot
with
that
with
that
part,
okay,
so
ethereum
State.
How
is
it
constructed
most
important
takeaway?
It's
a
two
level
structure,
so
I
mentioned
that
the
state
route
is
the
commitment
of
the
entire
state,
but
it's
not
really
true,
because
ethereum
is
a
does
it
still.
Okay,
it
works.
It's
it's
account
based
and
essentially,
the
state
route
is
the
commitment
of
all
the
accounts
that
exist
on
ethereum
and
what
an
account
is
made
of
it's
made
of
a
balance
like
the.
J
If
balance,
it's
announced,
transaction
counter
storage
route,
the
storage
route
is
like
the
root
of
another
America
Patricia
tree,
and
this
America
Patricia
3
contains
the
key
value
database
that
holds
like
the
mapping
from
storage
key
to
its
actual
value.
And
finally,
we
have
the
code,
it's
essentially
the
hash
of
the
of
the
bytecode
so
main
takeaway.
First,
we
access
accounts
and
once
we
have
the
account
storage
root,
we
can
access.
Is
it's
it's
the
okay
cool?
J
So
to
sum
it
up
like
the
background,
so
main
takeaways,
given
the
block
stay
true
to
you,
can
recreate
any
any
state
for
this
specific
block
on
this
network
and
given
an
initial
trusted
blockage,
you
can
essentially
recreate
all
the
previous
headers,
which
is
pretty
pretty
cool
and
important
to
get
the
ideas
that
I
will
explain
like
pretty
soon.
Okay.
So,
as
it's
gonna
be
a
workshop,
it's
a
short
one.
So
I
won't
let
you
code,
but
I
will
show
you
some
concrete
examples.
J
J
So
first
of
all,
the
question
that
we
need
to
answer
to
ourselves
is
how
does
Polygon
commit
to
ethereum
L1,
because
if
we
want
to,
like,
let's
say,
prove
the
ownership
of
a
lens
profile
on
optimism,
we
need
to
know
the
state
route
of
polygon,
but
there
is
material
one
in
the
middle.
So
how
do
we
actually
access
this
on
each
terminal?
One
primarily
so
polygon
is
a
commitment
commit
commit
chain
and
it
commits
to
to
ethereum
a
bunch
of
things
every
some
amount
of
time
and
essentially
on
L1.
J
We
do
not
validate
the
entire
State
transition,
but
we
just
verify
the
consensus
of
polygon
and
this
checkpoints
how
they
call
it
essentially
contain
State
routes,
and
so
I
mean
not
directly,
but
we
can
access
them
and
let's
get
to
this
to
this
part,
so
this
is
taken
from
polygons
documentation
and
this
is
how
a
checkpoint
looks
like.
So,
as
you
can
see,
the
checkpoint
is
made
of
a
proposal
so
who
proposed
The,
Block,
start
lock
and
block.
Give
me
a
second
I'll
get
to
this
and,
most
importantly,
we
have
the
root
question.
J
So
the
root
hush
is
essentially
a
Merkle
tree,
not
America
Patricia
tree
that
contains
all
the
headers
and
which
headers
the
headers
in
the
range
of
start
block
and
end
block
cool.
So
now,
if
we
get
back
to
the
previous
part,
we
can
essentially
prove
with
this
commitment
that
we
know
the
valid
state
route
of
polygon.
J
J
So
number
one
we
go
to
the
contracts,
we
see
a
contract,
we
go
for
it
and
we
see
that.
Essentially,
there
is
a
bunch
of
logic
on
top
of
this
erc721.
This
is
like
the
basic
erc71.
As
you
can
see,
it's
an
abstract
contract
and
it's
slightly
modified
instead
of
having
like
a
standard
mapping
from
like
token
ID
to
its
owner.
We
have
like
token
ID
to
token
data
token
data
is
a
struct.
Distract
is
32
bytes
in
total,
20
bytes
is
the
actual
owner,
and
the
remaining
12
bytes
represent
one.
J
The
token
was
minted:
okay,
but
how
do
I
actually
prove
it?
Oh
and
also
very
important
thing
when
dealing
with
storage
layout,
we
have
something
that
is
called
like
slot
indices,
so
each
variable
has
a
given
slot
like
in
the
some
sort
of
meta
layout.
I
call
it
like
that
it's
from
the
right
way
anyways
this
mapping.
It
has
like
the
slot
index
too.
I
will
get
to
this
part
in
a
second.
J
Why
it's
two
and
we
have
a
mapping
from
token
ID,
so
you
win
to
32
bytes
of
data
represented
as
a
structure
just
think
of
it.
As
some
bytes,
okay,
so
I
guess
most
of
you
use
heart
hot,
so
I'm
gonna
present
on
on
hard
Hut.
There
is
a
very,
very
cool
tool
to
deal
with:
storage
layouts.
It's
called
obviously
hard
hot
storage
layout.
This
is
how
you
install
it.
It's
literally
yarn
install
hardcode
storage
layout.
You
add
one
comment
to
your
heart:
config.
J
You
write
a
new
script
that
contains
literally
eight
lines
of
code.
You
run
the
script
and
you
get
this
weird
table
and
what
does
it?
What
does
it
really
tell
you
and
oh,
and
by
the
way
why
this
tool
is
pretty
useful?
As
you
see,
this
contract
is
abstract,
so
some
other
contracts,
then
does
it
still
yeah.
Some
countries
can
inherit
from
it
and
obviously
why
we
inherit
the
storage
layout.
I
mean
this.
J
Does
this
in
synthesis
can
can
get
more
trickier
because
it
also
okay,
so
that's
it's
pretty
hard
to
coordinate
like
one
hand
with
another
hand,
even
though
I'm
Italian,
okay,
anyways
yeah.
We
know
this
slot
in
the
in
the
index
and
that's
how
we
get
it.
We
have
a
column
that
is
called
storage
slot
and,
as
you
see
underscore
token,
data
is
marked
as
two
and
that's
it
okay.
But
what
do
we
do
with
it?
How
do
we
get
this
storage
key
and
yeah?
That's
that's
it.
Let
me
check
the
time.
J
J
How
do
we
get
the
storage
key?
We
essentially
do
this
operation,
so
we
concatenate
the
slot.
I
mean
the
key
in
the
mapping
which
is
35.94,
because
this
is
the
token
ID.
As
you
know,
we
have
a
mapping
from
token
ID
to
token
data.
Token
data
contains
the
old
okay,
so
we
concatenate
this
with
the
storage
index.
We
hash
it
all
together.
J
This
is
the
storage
key
that
we
have
if
you're
interested
how
to
deal
with
it
for
like
more
complex
mappings
and
like
layouts
back
the
solidity
documentation,
it's
explained
pretty
well
so
now
that's
to
make
sure
we
got
the
proper
storage
key,
let's
just
check
it.
How
we
can
check
it
super
easy.
Let's
just
make
a
one,
liter
PC
call
to
get
this
storage
at
some
specific
key.
Please,
if
get
storage
at
so
the
parameters
we
want
to
access.
The
storage
of
what
of
the
lens
Hub
lens
cap
is
a
contract.
J
J
And
we
know
that
it's
32
bytes
of
data,
where
we
have
20
and
12.,
so,
let's
split
it
into
12
and
20
bytes,
and
what
we
have
is
some
number
like.
You
can
see
Zero
x,
a
lot
of
zeros,
then
62
till
D,
and
this
looks
like
a
small
number.
So
apparently
it
is
a
timestamp
and
the
second
part
is
like
35
7
and
it's
literally
our
address.
So
we
got
it
correct.
J
We
have
the
proper
storage
key
cool
foreign,
but
how
do
we
actually
get
to
storage
proofs,
so
blurb
standardized
method
in
like
the
Json
or
PC
standard
for
ethereum
clients,
and
this
method
is
called
eth,
get
proof
which
essentially,
given
the
contract
address
so
I'm,
better
call.
It
account
address
in
this
specific
case,
allows
us
to
generate
a
state
proof
and
the
last
argument
I
mean
the
sorry.
The
second
argument
is
an
array
that
contains
all
this
Storage
storage
keys
that
we
want
to
prove.
J
There
is
another
argument
which
is
0x1a:
it's
essentially
the
block
number
for
which
we
prove
the
state
yeah.
Let's
call
this
method,
oh
by
the
way
you
might
have
a
question:
how
do
we
deal
with
this
method
on
non-evm
chains
because,
for
example,
on
some
specific
Roll-Ups,
this
method
is
like
not
supported?
Actually,
it's
not
a
big
deal,
because,
if
you
think
of
it,
we
just
need
the
database
and
on
top
of
this
database
we
can
literally
build
this
method.
We
just
need
to
know
how
the
storage
is
constructed.
J
Okay,
this
is
the
proof,
it
looks
scary.
It
is
scary.
This
entire
object
is
four
kilobytes
of
data,
and
now
I
mentioned
before
that
the
state
is
like
a
two
level
structure.
First,
we
have
a
proof
for
the
account
itself
and
then
we
have
the
proof
for
the
storage
I
mean
for
the
actual
storage
slot.
It
is
scary,
it's
meant
to
be
scary.
One
proof
is
like
more
or
less
600
bytes
700
bytes.
It
really
depends
like
bigger.
The
storage
is
than
bigger.
The
proof
is,
and
also
more
accounts
we
have
than
bigger.
J
The
account
proof
is,
so
that's
a
lot
of
cool
data.
If,
if
you
can
imagine
you
can
imagine
and
yeah,
that's
that's
pretty
bad.
Why?
Because
we
need
to
pause
this
proof
on
the
Chain,
so
it's
a
lot
of
cool
data,
but
okay,
let's,
let's
try
what's
going
to
be
the
cost
on
like
an
evm
chain,
that's
the
cost!
It's
like
600k
of
gas!
That's
a
lot
that
kills
almost
every
single
application
that
you
want
to
build
on
top
of
this
nice
primitive.
J
So
it's
pretty
bad,
and
why
is
it
that
bad,
so
I
explained
on
the
high
level
what
Merkel
trees
are
America
Patricia
trees
are
on
ethereum,
we
use
Marco,
Patricia
trees,
and
essentially
there
is
a
trade-off
that
when
using
Miracle
Patricia
trees,
the
proof
is
a
slightly
bigger.
It's
like
harder
to
decode
it,
because
actually
we
need
to
do
some
a
bit
of
decoding
there,
but
we
need
to
do
less
hashing.
J
So
this
is
a
trade-off,
but
depending
where
we
actually
verify
this
proof,
it
might
be
more
feasible
to
verify
like
prove
that
is
based
on
record
Patricia
trees
or
Miracle
trees.
Okay,
but
there
is
a
solution
and
the
solution
is
what,
if
we
snarkify
such
such
a
proof-
and
we
verify
this
proof
inside
the
Stark-
why
is
it
cool?
Because
we
can
like
let's
say
that
I'm
gonna
verify
this
proof
inside
the
craft
craft,
16
circuit
and
yeah,
the
verification
costs
more
or
less
like
210k
gas.
J
The
proof
is
like
way
less
than
600
bytes.
So
it's
good
so
essentially
get
rid
of
the
cold
data,
because
the
proof
itself
can
be
the
private
input
to
the
Circuit
yeah.
We
can
like
use
multiple
proving
system
depending
on
the
on
the
actual
use
case
and
now.
Why
is
it
like
very,
very
cool?
So,
first
of
all,
it
removes
call
data
second
model.
J
It
allows
us
to
deal
with
very
UNH
unfriendly
hashing
functions
or
the
evm
is
the
ones
that
we
don't
have
pre-compiled
for,
like
let's
say
Peterson,
so
it
might
be
like
super
expensive
to
verify
such
a
proof
on
the
evm,
because,
first
of
all,
that's
a
lot
of
cool
data
and
the
hashing
function
is
pretty
like
unfriendly.
But
what?
If
we
can
like,
do
it
inside
the
snark
and
just
verify
snark
and
yeah?
So
another
benefits?
This
really
really
helps
in
obstructing
the
way.
J
How
we
verify
this
proofs,
because
you
don't
need
to
have
like
one
generalized
verifier
for
each
type
of
of
proof,
but
you
can
essentially
obstruct
it
behind
behind
the
behind
the
snark,
which
is,
which
is
great.
These
numbers
were
taken
from
a
very
nice
article,
written
by
a16z,
like
a
bunch
of
a
few
a
few
months
ago.
J
J
So
I
mentioned
that
we
always
need
the
state
route,
but
because
all
of
these
systems
have
a
native
messaging
system,
we
can
send
the
small
commitments
like,
for
example,
the
blockage
to
like
L1.
Usually
it
goes
off-road
one
and
and
yeah
we
can
like
enroll
it
or
send
the
state
through
directly
and
also
we
don't
need
to
rely
on
messaging,
but
we
can,
for
example,
rely
on
the
fact
that
polygon
is
like
a
commit
chain
and
all
these
Roll-Ups
like
commit
from
time
to
time,
they're
like
batches
and
and
so
on.
J
So
if,
let's
say
polygon
commits
another,
one
I
can
send
this
commitment,
then
to
start
and
I'm
starting
to
do
their
actual
verification
cool.
So
now,
how
do
we
actually
do
that?
So,
let's
break
the
entire
flow
into
like
smallest
pieces.
So
the
flow
is
the
following:
we
need
to
have
access
to
the
commitment
which
is
either
a
block,
hush
or
a
state
route,
and
again
we
can
get
it
or
I
either
by
sending
a
message
relying
on
the
fact
that
is
this
chain
commit.
So
in
a
sense
it's
still
a
message.
J
We
can
relate
in
an
optimistic
manner
or
we
can
go
even
more
crazy
and
verify
the
entire
consensus.
Okay.
So
this
is
Step
number
one.
We
need
to
get
the
commitment
step
number
two.
We
need
to
somehow
access
the
state
route,
so
the
commitments
of
the
state
from
like
a
previous
block
or
the
actual
blog,
because
keep
in
mind
that
these
commitments
are
only
block
hashes
and
with
block
hashes.
We
can
recreate
headers,
but
we
cannot
access
the
state
okay.
So
once
we
have
the
state
route,
we
obviously
need
to
verify
this
state
storage
groups.
J
J
So
approach
number
one
messaging,
so
I
can
send
the
message
from
let's
say:
optimism
to
Eternal
one
I
can
get
the
optical
I
can
get
the
blockers
by
just
calling
the
proper
op
code
and
and
I
get
it
take
some
time,
but
still
I
get
it.
This
is
approach
number
one.
So
we
rely
on
the
built-in
messaging
system,
which
is
I,
think
Fair,
because
the
security
of
it
is
equal
to
the
security
of
the
roll
up
and
if
you're
deploying
an
application
of
the
scroll
up,
it's
a
fair
assumption
to
do
so.
J
Yeah
it
doesn't.
Oh,
they
don't
know
about
the
downsides,
so
the
message
must
be
delivered,
so
it
introduces
a
significant
delay,
especially
when
dealing
with
the
withdrawal
period
in
the
in
in
the
middle,
and
it
requires
we.
It
requires
interacting
with
multiple
layers.
So,
first
you
need
to
send
a
message
and
then
actually
you
need
to
consume
it.
So
it's
it's
not
ideal,
but
the
trust
assumptions
are
pretty
occasional.
J
Another
approach,
consensus,
validation
by
the
way
this
like
Gremlin,
is
supposed
to
verify
a
bunch
of
BLS
signatures.
I
I
hope
it's
self-explanatory.
Okay,
so
maybe
a
few
a
bit
of
an
intro
right
now
we
have
POS
as
the
native
like
consensus,
algorithm
on
ethereum,
which
is
pretty
great
because
verifying
the
consensus
is
finally
doable
because,
before
like
verifying
the
hashing
function,
eth
hash,
which
was
used
for
proof
of
work,
was
very
memory
intense,
so
not
possible
to
do
inside
the
snark
on
chain
directly.
So
it
was
almost
impossible
to
do
so.
J
So
now
we
also
have
this
Workshop
called
lmd
ghost,
which
is
implementable,
but
doing
all
of
this,
like
directly,
is
pretty
expensive.
So
we
need
to
ideally
wrap
inside
the
snark,
but
there
is
another
downside.
So
a
few
words
about
the
trust
assumptions
you
well,
you
verify
the
consensus
directly.
So
it's
it's
fine.
He
do
you
introduce
any
trust
assumptions,
not
really,
but
the
biggest
downside
that
generating
the
proof
actually
takes
some
time.
J
So,
to
be
honest,
this
approach
is
feasible,
but
comparing
to
messaging
like
quite
often
is
like
almost
the
same,
and
you
pay
a
lot
of
improving
time
and
requires
like
having
more
advanced
infrastructure.
Okay
last
approach
that
we
actually
use
is
something
that
we
call
like
an
optimistic
relator
based
on
NPC
MPC
stands
for
multi-party
computation.
Maybe
before
I
explain
how
it
works,
let
me
explain
the
the
image
I
hope
it's
self-explanatory,
so
it's
an
NPC
protocol.
We
have
multiple
parties,
it's
multiple
parties
attached
something.
J
J
But
it
comes
with
a
few
downsides
because
while
we
introduce
some
trust
assumptions,
but
still
it's
okay,
okay,
how
does
it
work
so
it
works
in
a
way
that
we
have
a
bunch
of
off
chain
actors
who
essentially
make
this
calls
and
it
works
more
or
less
like
a
multi-seek.
But
the
reason
why
we
have
NPC
is
because
more
validators
you
have
than
obviously
more
Securities
but
more
validators.
You
have
in
it
like
standard
multi-sig
approach.
You
have
more
signatures
so
more
in
a
way
decentralized.
J
It
is
then
it's
more
expensive
to
verify,
because
you
need
to
verify
multiple
signatures
and
you
need
to
like
pause
the
signatures.
It's
a
lot
of
cool
data.
Such
approach
is
not
feasible
on
chains.
Oracle
data
is
expensive,
so
at
one
optimistic,
rollups
and
yeah
okay.
So
how
does
it
work?
What
is
actually
NPC
part
doing?
The
MPC
part
is
very
simple:
it's
essentially
signing
over
like
a
specific
curve.
Some
specific
payload
and
the
payload
is
the
commitment
itself,
and
that's
it
okay.
J
So
this
is
how
we
actually
attest,
but
now
how
why
this
approach
is
called
optimistic
and
why
it's
still
secure.
So,
first
of
all,
we
just
posted
some
something
on
the
actual
L2
and,
as
you
may
know,
we
can
send
messages
from
L1
to
L2,
and
such
a
message
can
contain
like
the
proper
commitment.
So
essentially,
even
if
the
validator
set
will
lie,
L1
will
never
lie,
so
you
can
just
challenge
such
a
message
and
now
to
participate
in
verifying
this
validators.
J
It's
super
easy
because
literally
two
RP
sequels
one
call
is
gonna
check
the
actual
commitment
on
the
actual
chain
and
the
other
one
checks
like
what
is
the
claimed
Commitment?
If
you
disagree,
you
just
send
a
message:
it
costs
roughly
60
K
of
gas
and
that's
it.
Everyone
can
do
that
and
again,
the
fraud
proving
window
is
pretty
short,
because
it's
essentially
how
long
it
will
take
to
generate
like
the
proof
of
consensus,
if
it's
possible
or
how
long
does
it
take
to
deliver
the
message
and
what
is
pretty
cool
in
this
approach?
J
It's
not
gas
intensive.
We
verify
just
one
signature.
So
that's
about
this
approach.
Let's
make
a
recap
and
let's
identify
the
trade-offs,
so
we
have
three
approaches.
The
first
one
is
messaging.
The
second
one
is
validating
the
consensus
and
the
third
one
is
having
this
optimistic
layer.
So
I
categorize
it
in
four
categories.
The
first
one
is
latency.
The
second
one
is
the
gas
cost.
The
third
one
is
trust
and
the
last
one
is:
what
is
the
off-ching
computation
overhead?
Why
do
I
even
list
it?
J
Because
if
we
do
some
sort
of
proving,
then
obviously
it
takes
time,
because
we
need
to
generate
the
proof
so
messaging
in
terms
of
latency?
We
are
quite
sad
because
well,
the
message
needs
to
get
delivered.
So
once
the
message
gets
delivered
to
some
specific
L2,
L1
will
be
able
to
generate
already
new
block.
So
we
don't
have
like
access
to
the
newest
values
in
terms
of
gas
cost.
It's
not
bad,
but
it's
not
perfect,
because
we
need
to
interact
with
two
chains
at
the
same
time.
J
J
Option
computation
overhead
we're
very
happy,
because
there
is
no
computation
to
do
off-chain,
verifying
the
consensus.
So
in
terms
of
latency,
we
are
side
because
we
need
to
generate
the
proof
that
we've
done
it.
It
takes
a
bit
of
time
in
terms
of
gas
cost
we
are
I
would
say
sad
because
we
need
to
verify
the
actual
ZK
proof
which
is
way
more
expensive
than
just
consuming
a
message
or
verifying
a
signature.
In
terms
of
trust,
we
are
happy
because
we
verify
the
consensus
itself
and
computation
overhead.
J
It's
significant
right,
because
we
need
to
generate
the
proof,
Final
Approach,
this
optimistic
layer,
so
in
terms
of
latency
we're
happy,
because
we
simply
make
a
claim
and
we
post
it
on
the
other
chain.
That's
it
gas
cost.
We're
very
happy
because
the
well,
we
just
verify
a
signature
in
terms
of
trust.
Well,
we
are
not
that
happy,
but
also
not
that
sad
at
the
same
time,
because
it
still
can
be
challenged
in
an
optimistic
manner
using
a
fraud
proof
computation
option,
computation
overhead
are
pretty
happy
because
we
participate
like
an
MPC
protocol.
J
J
Okay,
accessing
the
headers
I
hope
it's
self-explanatory,
because
we
literally
unroll
something
from
The
Trusted
input
and
The.
Trusted
input
is
again
a
block
hush
for
a
specific
block
X,
and
if
you
follow
the
initial
slides,
that's
essentially
each
block.
We
given
a
blockage,
you
can
recreate
the
block
header
and
knowing
the
block
header,
we
can
access
the
parent
question
by
knowing
the
parent
hash.
You
can
recreate
the
previous
block
header
to
essentially
go
to
the
Genesis
block.
J
So,
given
this
very
small
input,
we
can
essentially
unroll
the
state
or
whatever
was
present
on
the
chain
from
this
block
till
the
Journey's
block.
Okay,
so,
as
I
said,
I'm
gonna
explain
everything
on
on
the
example
of
ethereum
and
today
all
the
block
headers
together,
are
like
roughly
seven
gigabytes
of
data.
J
So
it's
quite
a
lot
but
okay.
This
is
how
we
actually
do
that
this
is
the
high
level
concept
and
what
are
the
approaches
so
the
first
one
we
call
it
like
on-train
accumulation.
So
essentially
we
do
this
procedure,
this
computation
directly
on
the
Chain,
so
we
provide
all
these
properly
encoded
block
headers
inside
the
call
data
and
the
blockers
that
we
might
receive
as
like
The
Trusted
input
by
sending
a
message
relaying
it
in
optimistic
manner
or
validating
the
consensus
and
yeah
like
recursively,
go
through
all
these
headers
and
and
verify
them.
J
But
there
are
many
many
downsides
because,
first
of
all,
it's
very
cool
data
intensive,
it's
very
computational
intensive
and
now
we
can
store
all
these
headers
on
the
actual
chain.
But
you
know
even
storing
on
an
L2.
Storing
7
gigabytes
of
data
is
still
a
significant
cost,
because
the
state
on
an
L2
is
reflected
as
call
data
on
L1,
so
it's
still
expensive
either
way.
But
the
cool
thing
is
that
I
have
direct
access
to
like
State
router
or
anything
that
I
want
to
access.
J
Next
approach
is
unchain
compression,
so
we
can
still
use
the
same
approaches
previously
so
literally
unroll
it
and
process
this
seven
gigabytes
of
data,
but
instead
of
like
storing,
then
we
can
just
update
the
miracle
tree.
It's
a
nice
approach,
but
comes
again
with
a
few
dump
sites.
It's
very
computationally
intense,
because
if
we
have
like
millions
of
headers,
we
need
to
perform
millions
of
hashes
on
the
Chain.
That's
that's
expensive,
but
at
least
we
we
save
on
on
storing
data
and
also
we
need
to
update
the
miracle
tree,
which
is
which
is
another
cost.
J
Last
downside
is
that
we
need
to
index
all
the
headers
that
have
been
processed.
Why
we
need
to
index
them
because,
if
I
want
to
up
the
access,
a
specific
block,
header
I,
need
to
provide
a
miracle
tab
because,
as
we
update
the
miracle
3-
and
we
just
store
the
root
in
the
contract
itself,
then
I
need
to
know
the
path
right.
So
I
need
to
index
the
data
and
essentially
once
I
it's
the
moment
that
I
want
to
access
it.
I
need
to
provide
the
miracle
path.
J
This
approach
is
okay,
it's
I,
wouldn't
say
way
better
than
the
previous
one,
but
it's
way
cheaper
last
approach.
So
there
is
a
very
cool,
primitive
called
Merkel
mountain
ranges,
love
it,
and
the
idea
is:
let's
do
the
same-
that
we
do
previously
inside
this
Arc.
So
we
can
provide
this
tremendous
amount
of
data
as
a
private
input
to
the
circuit
and
essentially
do
the
same
computation
like
unrolling
inside
this
record
itself,
and
now
we
have
a
public
input,
which
is
the
blockage,
so
essentially
the
commitment
from
which
we
unroll
it.
J
So
the
trusted
input,
the
public
input-
can
be
literally
asserted
when
we
do
the
on-train
verification
and
why
we
unroll
it.
We
can
accumulate
inside
the
miracle
tree
or
American.
Mountain
range.
Why
American
mountain
range
is
is
cool
because
well,
let's
imagine
that
you
want
to
have
like
seven
gigabytes
of
data
processing.
One
star
like
the
proving
time
is
going
to
be
horrible,
and
why
would
you
even
like
prove
this
commitment
for
like
the
entire
history
like?
Do
you
really
need
that?
J
Probably
not
so,
let's
chunk
it
like
into
smaller
pieces
and
Miracle
mountain
ranges
are
pretty
cool,
primitive
that
allow
to
do
this.
To
do
to
do
this,
to
give
you
like
a
bit
of
intuition,
how
how
does
it
work,
it's
essential,
think
of
it
as
a
tree
of
trees
yeah.
So
once
we
do
all
this
proving
like
of
chain,
we
simply
verify
the
proof
on
chain,
as
you
know,
like
refine.
The
proof
is
is
way
cheaper
than
doing
this
directly
on
the
chain,
and
still
we
just
provide
a
miracle
path
and
that's
it.
J
We
essentially
have
access
to
any
sort
of
data
we
want.
Let's
do
a
recap
again,
so
approach
number
one
on
the
accumulation
on
chain
compression
of
chain
compression
three
categories:
prover,
overhead
gas,
cost
storage
cost.
Actually,
gas
costs
should
be
computational
cost.
Okay,
so
prover
overhead
on-chain
accumulation.
Do
we
prove
anything?
Well,
not
really.
So
we
are
happy
answering
compression
well.
J
We
still
like
need
to
update
the
miracle
tree.
I
think.
Actually
there
is.
There
is
an
issue
here,
so
I'll
just
skip
this
part
after
in
compression
you're.
Very,
very
sad
because
well,
we
need
to
prove
actually
significant
computation,
so
the
proving
time
is
significant.
Okay,
now,
in
terms
of
gas
cause,
the
third
approach
is
horrible,
because
it
just
costs
a
lot,
because
we
do
the
entire
computation
engine
compression.
J
Well
we're
a
bit
happy
because
we
just
do
a
bit
of
computation,
but
still
it's
a
lot
of
cool
data,
a
lot
of
computation,
but
at
least
not
so
much
storage,
storage
cost.
Oh
sorry,
gas
cost
in
the
second
approach,
while
we
just
verify
approved
so
it's
cool,
okay
storage
cost
for
the
first
approach.
Well,
seven
gigabytes
of
data:
it
is
horrible,
so
we
are
very
set
on
chain
compression,
sorry,
storage
cost
for
launching
compression.
We
just
the
root
of
the
miracle
tree.
J
So
we
are
happy
and
in
the
second
case,
we're
even
more
happy
because
we
again
we
just
essentially
keep
updating
a
tree
and
we
don't
even
need
to
post
a
lot
post
a
lot
of
cool
data,
because
the
cool
data
we
passed
is
literally
just
the
proof,
so
we're
very,
very
happy
but
again
I.
Don't
want
to
say
that
all
of
the
one
of
these
approaches
is
the
best
one,
because,
as
you
see,
there
are
trade-offs
and
yeah.
So
this
part
is
actually
pretty
easy.
J
So,
as
you
know,
as
you
may
notice
here,
I
was
explaining,
like
the
second
step
when
it
comes
to
two
linguist
storage
proofs,
and
now
there
is
the
the
last
part
which
is
essentially
verifying
the
proof
itself.
So
approach
number
one
is
verifying
the
proof
directly
on
the
Chain
approach.
Number
two:
let's
verify
the
proving
side
the
star
can
then
verify
the
Stark
approach.
Number
three:
let's
verify
multiple
proofs
inside
the
snark
and
then
verify
the
snark.
J
We
can
aggregate
multiple
sharks
together
and
so
on,
but
obviously
there
are
some
trade-offs,
especially
when
it
comes
to
proving
time
and
yeah.
So
now
why
the
first
approach
is
feasible
on
on
ZK
rollups,
for
example,
on
structural
data
is
very
cheap
and
what
we
want
to
avoid
in
this
specific
processes
called
Data.
So
this
approach
is,
for
example,
feasible
on
starknet,
but,
for
example,
if
you
want
to
verify
like
a
proof
on
optimism
or
a
collate
is
very
expensive,
you
want
to
reduce
it
as
much
as
possible.
J
So
for
that
reason
you
might
want
to
use
a
snark.
And
finally,
if
you
have
like
many
slots
that
you
want
to
prove,
why
can't
you
just
verify
them
inside
one
snark,
you're
gonna
pay
improver
time,
but
you
just
present
one
proof
at
the
end.
So
this
approach
is
cheaper
is
the
cheapest
one,
but
only
if
you
have
multiple
actions
to
to
take
so
there
are
trade-offs.
J
So
let's
identify
them
categories,
approver,
overhead,
latency,
verification
cost.
So
verifying
the
proof
directly,
prover
overhead
doesn't
exist.
Latency
doesn't
exist
because
we
don't
need
to
prove
anything
verification
costs.
Well,
it
is
significant
because
we
need
to
post
School
data
and
we
need-
and
we
need
to
do
the
actual
computation
so
like
going
through
the
entire
path
and
each
step
in
the
path
is
one
hashing
function,
oh
and
also,
let
me
get
back
to
the
previous
slide.
I
forgot.
This
is
very
important.
Why
wrapping
inside
this
wrapping
inside
this
Arc
is
pretty
important.
J
If
you're
like
dealing
with
a
storage
layout
that
is
using
a
specific
hashing
function,
let's
say,
for
example,
Peterson
Peterson
is
not
available
like
on
on
the
evm
like
you
just
need
to
implement
it's,
not
the
pre-composed,
it's
gonna
be
costly,
but
if
you
do
inside
the
snork
and
Peterson
is
pretty
smart
friendly,
it's
not
friendly,
then
well,
it
just
verifies
in
our
control
one
and
you
abstract
it.
So
it's
going
to
be
way
way
way
cheaper.
But
again
there
are
trade-offs.
Let
me
get
back
to
this.
So
I
went
for
this.
J
The
normal
competition
3
star,
Cricket,
fight
proof
through
the
overhead
it
exists.
So
we
are
not
super
happy.
Latency
you're,
also
not
happy,
because
we
actually
need
to
spend
time
on
improving
this.
This
thing
verification
costs.
We
are
happy
because
well
we
we
just
verify
your
proof.
So
it's
fine
and
it's
an
artifying,
multiple
proofs,
the
prover
overhead,
is
still
there.
J
Okay,
went
through
quite
a
lot
of
things,
let's
put
this
all
together,
so,
let's
imagine
we
have
three
chains
and
we
want
to
have
interoperability
interoperability
between
them,
so
we
have
chain
Z,
chain,
X
and
chain
y,
so
it
all
starts
with
a
message:
AKA
commitment.
We
send
a
message
in
order
to
get
the
commitment.
So
let's
say
that
we
send
a
message
from
chain
Z
to
chain
X,
because
on
chain
X
we
want
to
access
the
the
state
of
changing.
J
So
what
do
we
do
once
we
have
the
commitment,
we
literally
recreate
all
the
headers
using
one
of
the
three
approaches,
and
once
we
recreate
it,
the
header
is
still
the
point
for
which
I
want
to
prove
the
storage.
I,
just
verify
a
proof
and
again
for
verifying
get
proof.
There
are
multiple
approaches,
but
now,
let's
say
that
on
chain
y
I
want
to
access
the
state
of
change
Z,
and
there
is
no
direct
communication
between
chain
Y
and
chain
Z.
J
J
We
don't
expect,
like
developers
to
deal
with
all
that
complexities,
choosing
the
right
approach
for
the
direct
thing
essentially
right
now,
our
apis
optimizes
cost
wise
soon,
we'll
be
able
to
optimize
latency,
wise
and
yeah,
and
essentially
that's
it
just
about
our
API
I,
highly
highly,
encourage
you
to
check
this
out
and
yeah
like
a
few
final
words
about
the
API.
It
acts
as
a
coordinator.
J
It
optimize
the
costs,
it
optimizes
the
cost,
because
we
can
batch
multiple
things
and
once
the
job
is
done,
we
get
a
notification
like
via
webhook
VIA,
an
event
like
whatever
you
want
so
essentially
you're.
Not
you
don't
need
to
be
like
a
infrastructure
maintainer
and
you
can
just
focus
on
essentially
building
on
top
of
this
primitive
and
I.
Think
that's
it
questions.
J
So
the
API
essentially
is
a
rest
API.
For
now
we
also
have
a
Json
interface.
We
have
option
function,
entry
points,
so
we
can
request
the
data
like
by
making
enough
jingle
like
calling
a
rest
API
or
like
calling
a
Json
or
PC
method
or,
if
you're,
a
smart
contracts
like
wants
to
access
this
data,
then
you
just
submit
an
event:
we're
gonna
catch
the
event
and
later
on,
like
after
a
bit
of
time,
fit
this
the
specific
data
inside
the
smart
contract.
J
So
we
have
like
a
bunch
of
interfaces
and
by
the
way,
speaking
of
like
the
off-train
entry
points,
once
the
entire
leg
work
is
done
on
our
site,
you
can
get
a
notification,
it
can
be
like
a
web
hook.
We
can
like
send
you
a
bit
of
information
like
using
a
websocket.
It
can
be
essentially
whatever
whatever
you
want.
J
J
Oh
yeah,
so
that's
actually
a
great
question.
So
different
chains
use
a
different
like
storage,
I
would
say
architecture
they
might
commit
to
America
Patricia
3,
Miracle,
3,
maybe
even
vertical
tree
and
obviously,
like
I,
said
having
a
generalized
verifier.
It's
like
pretty
it's
not
a
clean
approach,
so
we
essentially
abstract
it,
but
by
using
a
snark
and
inside
the
snark
itself,
we
just
do
the
proper
work
like
you
know.
J
You
go
for
the
for
the
tree
like
for
the
for
the
through
the
elements
of
the
proof,
and
then
we
can
like
use
a
specific
hashing
function.
So,
for
example,
now
Poseidon
is
Poseidon
is,
is,
is
pretty
popular,
I
think
that
scroll
uses,
Poseidon
and
also
SDK
sync
uses
Poseidon
on
the
avian
like
performing
Poseidon
will
be
pretty
expensive.
So
for
that
reason
you
cannot
verify
the
proof
directly,
but
what
you
can
do
you
can
do
the
entire
verification
inside
the
snark
and
then
on
the
one
you
don't
really
care
about.
J
J
J
J
Oh
yeah,
that's
that's
actually
a
good
question
because
I
think
I
went
super
technical,
so
actually
what
we
do
at
Herodotus
every
two
weeks
we
have
some
internal
hackathons
and
right
before
the
merge,
we
built
a
proof
of
concept
that
we
called
merge.
Swap
and
essentially
we
allowed
anyone
to
dump
their
proof
of
work
if
on
proof
of
stake
and
the
way
how
it
works.
J
Would
you
literally
build
the
bridge
on
top
of
this
technology
and
the
bridge
Works
in
a
way
that
you
can
lock
your
if
proof
of
work
inside
a
smart
contract
on
if
proof
of
under,
if
proof
of
work
chain,
you
can
prove
that
you've
done
it
on
ethereum
proof
of
stake.
You
can
once
you
the
proof
is
verified.
You
can
meet
the
erc20
token
and
you
can
do
whatever
you
want
with
this
token
and
then,
if
you
want
to
withdraw
back
to,
if
you're
in
proof
of
work,
you
just
burn
it.
J
You
prove
the
fact
that
you
burned
on
the
other
side
and
and
yeah.
That's
it
also
in
terms
of
other
use
cases.
I
think
that
cross-chain
collateralization
is
pretty
cool,
because
this
is
the
place
where
you
want
to
avoid
latency
as
much
as
possible,
and
you
want
to
be
asynchronous
as
much
as
possible
and
essentially
that's
that's
what
we
do
here,
because
our
latency
comes
only
from
from
the
proving
time
but
again
using
some
optimistic
approaches,
and
so
on
there
a
lot
of
things
we
can
do
cure
I
hope
it
answers
the
question.