►
From YouTube: Andrei Marinica, Elrond – Integrating WebAssembly execution into own blockchain Elrond
Description
Speaker: Andrei Marinica, core developer at Elrond Network
Topic: Integrating WebAssembly execution into own blockchain Elrond
Elrond Network https://linktr.ee/elrond
Wasm in Web3 workshop:
https://avive.github.io/wasm_on_the_blockchain_2021/#/
A
A
So
with
that,
I
will
begin
this
is
the
advan
web
assembly
story.
I
will
talk
about
four
main
things.
I
will
first
give
an
overview
of
what
everyone
is
and
what
we
do
at
elrond.
Then
I
will
talk
a
little
bit
about
how
our
smart
contract
architecture
is,
how
we
think
of
smart
contracts
and
from
a
very,
very
high
level
perspective,
and
then
I
will
go
dive
a
little
bit
deeper
into
how
we
execute
them
and
how
we
really
integrated
web
assembly
into
our
stack
and,
of
course,
the
last
thing.
A
I'll
have
a
really
short
slide,
but
very
very
important
about
how
we
verify
the
correctness
of
what
we
build
and
what
our
developers
build.
So
without
further
ado,
what
is
elrond
adron
is
a
very,
very
scalable
layer,
1
blockchain
protocol,
which
many
of
you
might
have
heard
of.
We
do
state
charting
and
proof
of
stake.
A
A
We
have
a
six
second
latency
block
and
very
very
cheap
transactions,
but
even
more
important
than
that
we
have
the
iron's
money
and
d5
app,
which
is
called
maya,
which
is
a
it's.
A
phone
is
a
smartphone
application
that
allows
anybody
with
a
smartphone
access
to
the
world
of
defined
world
of
crypto,
and
so
far
it's
been
having
quite
some
success.
And
last
but
not
least,
we
have
quite
some
interesting
token
economics.
A
A
Our
main
innovations
there's
a
few
pillars
that
make
everyone
what
it
is
and
that
brought
us
where
we
are
today.
The
most
important
one
is
adaptive
stage,
starting
it's
our
flavor
of
proof-of-stake
sharding.
There
are
three
types
of
of
blockchain
charting
and
we
do
all
three
of
them.
One
is
a
state,
so
each
chart
has
completely
separate
state
from
the
other.
The
other
one
is
transactions,
so
each
chart
processes
its
own
transactions,
independent
of
the
others
and
yeah.
A
What
the
the
third
one
is
network
sharding
in
which
the
networks
ins
themselves,
don't
communicate
too
much
so
as
to
optimize
the
throughput.
Currently
we
have
one
meta
chain
and
three
execution
charts,
but
in
principle
we
can-
and
we
can
have
more
of
those.
If
there
is
demand
or
fewer.
You
know,
as
as
the
demand
fluctuates,
we
can
adapt
our
number
of
shards.
A
Then
the
second
pillar
is
secure
proof
of
stake.
This
is
again.
This
is
a
special
flavor
of
proof
of
stake.
It's
based
on
a
byzantine
fault,
tolerance
like
a
consensus
mechanism
which
samples
a
consensus
group
with
every
round,
and
we
have
validators
randomly
shuffled
between
shards,
so
that
shard
takeovers
are
very
difficult
and
we
also
have
an
unbiasable
randomness
source,
which
can
be
very
useful
for
certain
types
of
contracts.
A
Then
we
have
smart
accounts
now,
smart
accounts.
Basically,
any
account
on
l1
is
a
smart
account.
User
accounts
and
smart
contracts
are
not
that
different
in
that
they
both
have
an
individual
data
tree
where
their
storage.
Now,
of
course,
a
user
cannot
write
anything
they
want
in
their
own
storage,
but
this
storage
can
be
used
by
the
protocol
to
enable
all
kinds
of
cool
functionality.
A
A
Okay,
now
a
little
bit
about
how
the
last
two
or
three
years
have
been
a
few
highlights,
we've
had
the
main
at
launch
a
little
more
than
a
year
ago
it
was
late
july,
so
the
mainnet
has
been
online
for
a
year
now
and
without
interruptions.
That
is
which
we
are
very
very
proud
of,
and
also
in
january,
we
had
our
meijer
launch.
A
My
organ
is
our
smartphone
app,
which
enables
anybody
to
connect
to
blockchain
it's
very
friendly
and
we're
preparing
we're
in
our
final
preparations
to
launch
our
first
decentralized
exchange
on
called
the
meyer
decks,
which
will
be
soon
hopefully
very
soon,
there's
more
about
the
roadmap
and
the
projects
we
do
on
our
website.
There
will
be
a
launch
pad.
There
will
be
an
nft
marketplace,
a
lot
of
cool
stuff
coming,
but
this
is
just
like
the
major
major
things.
A
Each
smart
contract
lives
in
a
shard
and
they
all
have
their
own
data
trees,
and
then
they
rely
on
the
protocol
to
resolve
the
cross.
Chart
calls
now,
as
you
can
imagine,
there's
cross
chart
calls
from
users
to
smart
contracts,
but
there's
also
cross-chart
calls
from
smart
contracts
to
other
smart
contracts.
A
A
We
do
it,
but
rarely
what
we
prefer
to
do
is
working
with
so-called
asynchronous
calls.
Now
these
synchronous
calls
are
shard
agnostic,
which
means
the
developer,
doesn't
care
and
shouldn't
care
and
shouldn't
even
know
whether
or
not
the
two
contracts
are
in
the
same
chart
or
not.
Remember.
I
said
we
have
adaptive
stage
sharding,
so
at
some
point
the
shot
might
split
into
two.
So
we
don't
even
know.
Maybe
today
the
contracts
are
in
the
same
chart,
but
maybe
on
another
day
the
contracts
end
up
in
two
different
shards.
A
So
this
is
why
it's
important
that
we
have
a
mechanism
that
works
in
both
cases
identically.
It
consumes
the
same
amount
of
gas,
even
though,
of
course
doing
things
cross
chart
is
usually
a
bit
slower,
and
we
also
can't
have
the
answer.
So
if
you
want
to
interrogate
another
contract,
which
is
another
sorry
in
another
shard,
of
course,
you
can't
have
your
answer
immediately,
because
the
data
is
not
there
now.
What
happens?
Is
you
create
this
kind
of
transactions
the
other
chart?
A
And
then
you
wait
and
maybe
one
two
more
blocks
down
the
line.
You
will
get
back
the
result
in
what
we
call
a
callback
transaction.
So
you
get
the
answer
a
bit
later
and
this
is
not
atomic.
Unfortunately,
so
the
developer
has
to
handle
the
rollback
explicitly
in
case
of
failure
or
commit
things
that
can
only
be
committed
when
there's
confirmation
that
the
other
transaction
also
happened,
and
I
have
a
nice
diagram
here
now
this
I
have
to
caution.
You
is
the
absolute
simplest.
A
The
absolute
simplest
cross
chart
transaction
from
a
smart
country
to
another
smart
contract.
Of
course,
there's
a
lot
more
complex
scenarios
that
can
be
had,
but
yeah
in
this
most
simplest
form.
You
have
a
user.
The
user
is
calling
a
smart
contract,
of
course,
as
part
of
of
a
decentralized
application
and
contract
a
needs,
something
done
in
contract
b,
which
is
perhaps
in
another
chart.
Perhaps
not
so
what
happens?
Is
contract
a
sends?
A
This
asynchronous
call
to
contract
b
and
then
contract
b
does
its
thing
and
contract
b
sends
the
reply
back.
This
happens
automatically,
so
the
developer
doesn't
have
to
do
that.
The
protocol
always
sends
a
call
back
back
and
if
contract
b
ran
successfully
then
contract
a
will
know
this
and
we'll
get
the
answer
and
we'll
be
able
to
commit
stuff,
and
if
contract
b
failed,
then
contract
a
will
be
notified,
that
hey
contract
b
failed,
and
maybe
you
want
to
roll
back
some
stuff
and
so
forth.
A
So
this
is
in
a
nutshell,
how
it
works.
It's
conceptually,
not
very
complicated,
but
you
know,
as
the
scenarios
become
more
and
more
complex,
so
does
the
system
now
the
second
so
to
say,
complications.
Second,
innovation
is
that
smart
contracts
have
to
interact
with
esct
tokens,
so
I
mentioned
est
tokens
earlier.
A
This
is
very
important
in
a
shorter
deck
architecture.
Just
imagine
what
would
mean
to
run
an
erc20
in
a
sharded
architecture.
You
might
be
in
a
in
a
shard
and
your
token
might
be
in
another
shard.
So
it
would
take
a
lot
of
time
for
you
even
to
do
the
most
basic
stuff
with
your
token,
because
you
wouldn't
have
direct
access
to
it.
In
this
way,
we
make
sure
that
every
user
has
direct
access
at
all
times
to
their
tokens,
because
their
tokens
are
in
their
account
they're,
not
in
a
smart
contract.
A
A
They
carry
additional
information
which
again
I'll
come
back
to
a
bit
later
and
another
cool
thing
that
we've
had
for
a
month
or
two
is.
We
can
transfer
multiple
tokens
at
once,
so
in
the
same
transaction
you
can
actually
send
multiple
tokens,
which
is
cool
from
user
to
user,
but
it's
especially
cool
if
you
want
to
interact
with,
for
instance,
so
with
decentralized
exchange
where
you
might
want
to
swap
two
tokens,
so
you
might
want
to
send
them
both
at
once,
and
then
you
get
two
tokens
in
return
right.
A
But
let's
say
you
run
a
multitude
of
smart
contracts
that
communicate
with
each
other
across
shards,
and
you
want
to
share
some
information
between
them.
Another
way
you
can
share
information
between
them.
You
can
have
them
exchange
these
tokens,
which
might
not
be
valuable.
They
might
be.
You
know
they
might
not
be.
You
know
the
kind
of
tokens
that
I
don't
know
you
would
collect
like
nfts
or
keep.
A
How
do
we
split
depths
into
multiple
shards,
multiple
contracts,
so
that
people
don't
have
to
interact
with
the
monolithic
smart
contract
in
one
chart,
but
that
they
they
can
have
their
own
their
own
smart
contract
in
their
own
chart?
So
everything
was
a
bit
faster
right
now.
I
will
go
a
little
bit
deeper,
so
this
was
a
an
overview
of
the
main
challenges
of
the
main
things
we
had
to
to
deal
with,
and
now
I
go
a
little
bit
deeper
into
how
we
execute
smart
contracts.
A
This
is
where
it
gets,
maybe
a
little
more
technical,
but
don't
be
scared
I'll.
Try
to
explain
everything
in
plain
terms
too.
So,
first
things.
First
from
the
get-go,
we
thought
how
cool
it
would
be
to
have
more
than
one
vm.
So
what
we
did
was
we
built
a
vm
adapter
which
allows
plugging
in
any
number
of
vms.
A
Basically
any
piece
of
software
that
you
know
satisfies
the
that
interface
can
be
a
vm,
but
of
course,
vms
are
not
plug
and
play
things
they're
part
of
the
consensus,
so
you
need
a
a
system-wide
upgrade
to
change
the
available
vms.
However,
this
is
possible,
and
even
though
right
now,
we
only
have
one
vm,
it's
called
r1
is
the
lron
vm.
It
has
multiple
versions.
We
had
to
do
this
to
mitigate
some
of
the
backwards
compatibility
issues
that
we
either
had
or
might
have
had.
A
So
currently
we
use
it
for
yeah.
It's
a
form
of
versioning
so
that
older
contracts
can
still
run,
even
if
we
change
some
of
the
some
of
the
vm
characteristics
and,
of
course,
each
smart
contract
points
to
its
own
vm.
So
each
smart
contract
knows
which
vm
it
runs
on.
So
it
has
a
specific
vm
and
vm
version
of
somewhere
on
the
blockchain
stored
into
it.
But
enough
of
that,
let's
dive
right
in
into
the
lrnv
and
the
r1
vm,
so
the
story
of
this
started.
A
Actually
in
2019
we
had
some
attempts
to
port.
I
think
a
vm
called
yell
vm
to
lrond.
This
is
a
formally
specified
dialect
of
llvm,
which
is
very
cool
and
we
actually
got
it
to
work
on
the
first
testnet.
We
had
a
prototype
of
it
and
we
actually
had
a
very,
very
cool
game
which
is
called.
It
was
called
crypto
bubbles.
It
was
very
addictive
and
made
us
spend
a
lot
of
time
instead
of
working
playing
the
game.
A
I
will
admit
that,
unfortunately,
it's
not
online,
it's
not
live
anymore,
but
the
main
but
yeah,
maybe
we'll-
maybe
we'll
revive
it
at
some
point
in
the
future.
Who
knows
if
there's
enough
demand
for
it?
The
only
problem
was
this
yellow
vm
as
cool
as
it
was.
It
was
kind
of
slow.
It
was
interpreter
based
we
couldn't
get
to.
A
A
A
A
We
also
get
a
local
caching
of
smart
contract
binaries.
Since
this
compilation
this
just
in
time,
compilation
can
can
take
quite
a
little
bit
of
time.
So
we
try
to
optimize
this.
Like
this,
we
have
configurable
per
op
code
metering.
We
used
a
prototype
actually
and
what
we're
running
on
is
actually
a
fork
of
wasmer.
That
has
a
few
small
modifications
that
we
needed
and
we
also
use
runtime
breakpoints,
which
we
use.
A
A
That
is
basically
the
main
piece
of
software
of
the
blockchain.
That
is
the
protocol.
It
does
all
the
magic
it
makes.
The
blockchain
exist.
On
top
of
it.
We
have
the
adapter
that
we
talked
about.
This
adapter
allows
connecting
various
vms,
which
we
have,
I
think,
yeah
one
or
two.
As
I
mentioned
before,
on
top,
we
have
our
l1vm,
which
is
called
r1,
and
this
vm
is,
you
know
the
main
focus
of
my
talk.
A
A
So
there's
a
lot
of
magic,
actually
there's
a
lot
of
code
in
it
to
ensure
that
the
correct
communication
between
the
charts
between
the
contracts
can
happen.
On
top
of
that,
we
have
our
smart
contracts
and
smart
contracts.
Of
course
they
are
web
assembly
contracts.
So
whenever
we
commit
something
to
the
blockchain,
we
commit
a
webassembly
binary.
A
That's
it,
but
of
course
we
don't
want
to
write
directly
webassembly
by
hand,
although
it
is
possible
and
it's
okay
to
write,
but
you
know
for
your
everyday
developers,
you
what
you
want
to
have
a
nice
high-level
language
built
on
it
and
the
language
that
we've
invested
most
in
is
rust.
We
have
a
rust
framework
that
we've
been
working
on
for
a
year
and
a
half
or
two,
I
think,
which
offers
all
kinds
of
features.
You
will
see
a
small
screenshot
of
it.
We
also
offer
a
very
minimal
cnc,
plus
plus
frameworks.
A
Now
you
can
write
smart
contracts
for
l1
in
cnc
plus
plus.
We
actually
do
it
all
the
time,
but
we
mostly
do
it
for
testing
to
test
our
own
framework
and
not
so
much
for
general
contact
development.
For
that
we
recommend
rust.
Of
course,
in
the
future,
we
plan
on
expanding
this
list
of
languages,
but
yeah
that
takes
time,
and
it
just
made
more
sense
to
focus
on
one
for
now
now.
A
A
A
Now
then
r1
takes
these
inputs
and
it
can
do
one
of
two
things.
If
it's
a
new
contract,
it
doesn't
know
anything
about,
it
will
just
send
the
wasm
contract
by
code
to
a
single
pass
streaming
compiler.
This
compiler
will
create
an
executable
and
the
executable
will
be
run
now
if
r1
has
seen
this
contract
before
it
loads
it
from
the
cache.
So
it
goes
faster
than
like
this,
and
then
the
executable
will
run
the
smart
contract.
It
also
has
metering
injected
into
it,
and
then
contract
has
access
to
an
environment.
A
It's
the
environment
interface
which,
where
we
provide
a
multitude
of
methods
that
contracts
can
use
to
interact
with
the
blockchain.
Like
give
me
the
arguments,
these
are
my
results
load,
something
from
storage,
write,
something
to
storage,
et
cetera.
We
have.
We
have
loads
of
those
okay
and
now
I
will
go
a
bit
deeper
into
what
these
kind
of
primitive.
What
this
kind
of
this
ei
is
for
a
smart
contract.
A
We
actually
provide
a
quite
a
comprehensive
library,
basically
baked
into
the
vm,
and
the
reason
for
this
is
we
figured
very
soon
along
the
way
that
smart
contract
size
is
critical
and
it's
critical
for
two
reasons.
Now,
of
course,
we
don't.
We
want
to
have
as
little
data
as
we
can
in
the
blockchain
and,
of
course,
every
smart
contract
is
stored
on
the
blockchain.
A
So
if
I
have
a
very
big
contract,
this
will
inflate
a
lot
the
size
of
our
blockchain,
which
we
don't
want,
because
we
we
want
people
to
be
able
to
run
nodes
on
on
machines
that
are
as
small
as
possible,
make
it
as
accessible
to
to
everyone,
but
there's
another
side
to
it.
It's
the
fact
that
a
lot
of
the
times
you
have
to
compile
these
these
wasm
bytecodes
to
machine
code,
and
this
takes
time
for
us
for
a
big
contract.
It
might
be
80
or
90
of
your
transactions.
A
We
don't
want
that.
You
want
small,
very,
very
small
contracts,
so
the
compilation
is
fast
even
with
cashing.
You
still
want
it
to
be
as
fast
as
possible,
so
we
we
made
ourselves
this
goal
of
having
very
small
smart
contracts,
no
larger
than
a
few
kilobytes
inside
size,
which
we're
every
day
struggling
to
get
better
at.
We
started,
for
instance,
with
certain
contracts
had
100
kilobytes
and
we
reduced
them
to
maybe
30
or
40..
We
have
also
a
few
countries
that
are
smaller
than
one
kilobyte
inside.
A
We
have
an
erc
20,
which
we
use
for
benchmark,
which
we
managed
to
reduce
down
to
3.5
kilobytes
in
size,
which
is
very,
very
small,
but
how?
How
were
we
able
to
achieve
this-
and
this
comes
here-
comes
the
trick
that
we
use
now
you
could
think
of
it
as
a
pre-compile,
although
it's
more
like
something
baked
directly
into
the
into
the
framework
we
have
these
mathematical
and
crypto
operations
that
we
offer
for
smart
contracts
to
use
directly
from
the
vm
now
for
crypto.
A
A
The
idea
is
that
we
want
smart
contracts
to
only
contain
the
business
logic,
very,
very
minimal,
only
the
how
only
the
what
and
not
the
how
and
let
the
vm
do
everything
else
and
in
a
very
optimized
manner.
So
how
it
works
is
the
vm
has.
This
kind
of
heap
is
a
structure
where
you
have
a
handle
and
with
a
handle
you
get
access
to
a
number
or
a
string
of
bytes,
so
there
was
memory,
doesn't
have
to
hold
them,
and
these
types
are
as
follows.
A
So
our
first
type
that
we
played
around
with
was
bigind
now,
of
course,
smart
contracts,
work
with
with
balances,
for
instance,
and
on
lron
the
balances
are
not
floating
points.
Okay,
because
you
want
you
want
a
comma,
you
want
a
decimal,
but
we
don't
use
floating
point
because
it
would
be
too
unstable.
We
use
fixed
point,
and
so
basically,
every
time
you
send
one
eagle
to
somebody
else
in
the
blockchain
you're
actually
sending
a
one
followed
by
eighteen.
A
Zeros
of
you
know
the
most,
the
smallest
unit,
which
is,
I
don't
know
a
tiny
eagle
way
or
something
so
from
the
get-go.
The
even
the
most
simple
contracts
need
to
work
with
really
big
numbers.
So
we
thought
why
not
just
bake
a
big
end
library
directly
into
the
vm,
since
it's
so
fundamental
to
running
all
contracts
which
we
did
now
there's
another
difference
that
is
between
evm
and
what
we
did.
Evm
usually
works.
A
lot
with
256
bit.
A
We
use
we
use
them
for
all
kinds
of
stuff
to
concatenate,
like
error
messages
to
concatenate
keys
for
storage,
everything
we
do
with
them.
We
also
have
an
electric
curve
object
which
we
use
for
cryptography
and
we're
developing
a
big
float
so
yeah,
maybe
in
a
month
or
two.
If
everything
goes
well,
there
will
be
access
to
big
clothes
too,
in
smart
contracts
and
I'll
just
go
over
on
a
very,
very
simple
example
of
how
a
smart
contract
would
work
with
this.
This
is
actually
what
happens
every
day
on
our
blockchain.
A
So
these
numbers
don't
actually
ever
get
loaded
in
wasm.
The
contract
doesn't
never
see
them.
It
just
tells
the
vm
hey
do
this
with
these
numbers.
So
this
is
a
very
simple
example
from
a
very
simple
contract:
it's
called
an
adder
contract.
It
just
has
in
storage
a
value,
and
then
you
can
increment
it.
That's
it
very,
very
simple,
but
this
value
is
a
big
end.
So
how
would
you
go
about
it?
A
The
contract
basically
asks
at
the
very
beginning,
the
framework,
hey,
I'm
expecting
one
argument,
and
this
should
be
a
big
end,
just
load
this
argument
for
me
and
then
the
vm
says
sure:
okay
and
here's
your
handle
for
it.
This
is
handle
zero
and
the
contract
never
sees
the
number
just
get
the
handle.
A
Then,
okay,
I
have
this
value
in
storage.
Let's
read
this
and
then
the
vm
gives
it
the
other
value
at
handle.
One
and
the
contract
says.
Okay,
sure
just
add
these
two
numbers
together
and
okay.
The
vm
adds
them
behind
the
scenes
and
says:
okay,
so
I'll
put
the
result
in
handle
too
and
then
the
contract
says,
save
this
to
storage
and
maybe
also
return
this,
and
you
have
a
very,
very
small
transaction,
a
small
function
that
got
executed.
A
You
managed
to
interact
with
the
storage.
You
managed
to
receive
arguments,
you
managed
to
deserialize
them,
you
didn't
have
to
worry
about
visualizing
them
or
serializing
them
back
and
you
during
this
entire
time.
The
contract
didn't
see
the
numbers
even
once
it
only
told
the
vm
what
to
do
with
them.
So
this
is
how
we
get
really
really
small,
really
very
small
contracts.
A
Okay,
now
here's
some
benchmarks,
the
latest
one,
is
the
erc20
benchmark.
Now
again
we
don't
have
erc20s,
but
we
use
the
erc
kind
of
smart
contract
for
benchmark
because
it's
so
standard
because
everybody
knows
how
it
looks
like
and
what
it
does.
So
we
managed
to
shrink
it
down
to
3.5
kilobytes
in
size
and
half
a
minute.
Half
a
millisecond
per
transfer.
It's
pretty
fast.
There
will
be
more
benchmarks
in
the
picture.
We
have
a
bit
of
an
older
comparison,
but
actually
the
elder
numbers.
A
A
I
don't
know
if
we're
the
fastest
or
in
the
top,
but
I
presume
we're
in
the
top
there's.
I
hope
that
at
some
point
we
will
have
a
more
comprehensive
array
of
benchmarks
that
everybody
can
do,
and
so
we
can
compare
with
each
other.
But
that's
not
necessarily
the
point.
The
point
is
that
it's
fast
and
that
it
works
so
there
it
goes
now.
A
So
it's
it's
pretty
amazing
of
that,
and
we
tried
to
use
it
as
much
as
we
could
to
use
its
magic
as
much
as
we
could,
and
here
we
see
an
example
of
the
example
like
of
the
smart
contract.
I
talked
about
earlier,
the
one
with
number
there
which
you
can
increment
and,
as
you
can
see
nowhere
do
you
have
to
specify-
or
you
have
to
think
of
the
fact
that
this
this
big
hint
type
is
actually
not
in
memory
somewhere
else
and
you
can
even
write.
A
You
have
operators
on
it
like
run
like
plus
equals
stuff
like
that,
and
you
don't
care
in
this
whole
example.
You
basically
have
deserialization
of
a
big
number.
You
have
reading
from
storage,
you
have
writing
to
storage,
but
you
don't
actually
have
to
worry
about
it
very
much,
because
the
framework
does
a
lot
for
you
and
actually
the
most
of
the
work
that
the
framework
does.
A
There's
a
lot
of
money
being
lost
every
week
to
solve
the
software
bugs
so
we're
not
taking
this
lightly.
Quite
the
opposite.
We've
built
an
entire
stack
of
tools
that
we
use
now,
of
course.
First
of
all,
we
we
did
the
some
high-level
stuff.
So
there's
a
component
which
is
in
rust
only
that
mocks.
Everything
amongst
the
vm
marks
everything,
but
you
can
write
a
unit
test
and
you
can
write
integration
tests
in
high
level
rust
and
the
cool
thing.
A
Is
you
get
a
debugger
and
you
can
get
some
high
level
coverage
which
we,
where
we
didn't
yet
managed
to
to
do
running
running
the
web
assembly?
So
everything
you
see
in
the
in
on
at
the
first
point
that
is
not
involving
web
assemblies,
so
with
everything
mocked,
then
the
most
important
tool
that
we
use
for
testing
smart
contracts
is
called
mandos.
A
A
So
we
started
building
some
fuzzers
and
which
was
a
great
idea
because
we
were
able
to
much
more
aggressively
test
and
we
discovered
a
lot
of
bugs
like
this.
Well,
not
many,
but
the
bugs
that
we
found
would
have
been
very,
very
difficult
to
find
otherwise.
And
the
nice
thing
is
that
the
fathers
that
we've
built
are
actually
integrated
with
mondo,
so
they
they
can
use
bits
of
pre-written
scenarios,
pre-written
tests
and
then
mix
and
merge
them.
A
A
So
this
is
quite
nice
and
we
use
it
a
lot
and
then
the
last
two
things
I
want
to
talk
about
are
based
on
our
collaboration
with
runtime
verification,
which
is
a
very
cool
company
that
does
a
lot
of
very
cool
products,
especially
they
do
formal
modeling
of
software,
which
is
a
very
difficult
but
very
very
rewarding
field,
and
there's
two
actually
there's
right
now.
There's
two
projects
we're
running
with
them:
they
might
get
merged
at
some
point,
so
one
of
them
is
a
k
framework.
A
Full
implementation
of
our
vm
now,
for
those
who
don't
know
okay
framework
is,
is
a
framework
that
allows
one
to
define
languages
in
a
formal
way
and
is
very
good
at
that.
There's
many
technologies
out
there
that
allow
people
to
define
formal
specifications
but
k
framework
is
especially
good
at
defining
languages
and
they
already
had
so
when
we
started
they
already
had
an
implementation
of
chaosm.
A
So
I
think
ricard
had
a
presentation
about
it.
Two
years
ago,
at
this
very
very
conference
and
yeah
we're
working
with
them
to
integrate
that
and
also
formally
model
the
non-wasm
part
of
our
vm.
So
the
you
know,
synchronous
calls
and
whatnot
bring
them
together
and
then
run
smart
contracts
using
this.
This
formal
formally
defined
version
of
the
vm.
So
this
is
executable,
which
means
you
can
actually
execute
smart
contracts
on
the
k
framework
implementation.
A
But
it's
much
more
than
that.
You
can
also
prove
things
about
smart
contracts.
You
can
run
all
kinds
of
tools
like
coverage,
fuzzers,
all
kinds
of
things,
which
is
very
cool,
the
other
project
that
we
have
with
them.
We,
we
have
the
our
multi-stick
contract.
This
is
a
contract
that
allows
to
have
multiple
signers
on
a
transaction
and
we
had
it
modeled
and
verified
also
in
k
framework
and
its
soundness
was
proven.
A
It's
I
think
the
final
output
of
this
effort
should
come
out
this
month,
or
so
so
it's
actually
very
close
to
the
end,
and
we
also
and
yeah.
It
actually
found
some
very
subtle
bugs
so
it
I
guess
it
was
worth
it
and
we're
also
thinking
about
integrating
the
two.
So
that's
also
gonna
be
something
very
interesting
to
look
out
for
to
having
very
high
level
proofs
about
smart
contracts,
but
also
an
executable
sort
of
representation
of
everything
that
is
going
on
on
the
blockchain.