►
From YouTube: Verus - Verified Rust for low-level systems code by Andrea Lattuada - Rust Zürisee June 2023
Description
Rust programmers care about the correctness of their code and, while the Rust type system and its memory safety are excellent foundations, they aren’t sufficient to ensure correctness. “Full functional verification" of code is an alternative (or a complement) to tests that uses formal methods to prove that the behaviour of a complex program corresponds to a desired specification, i.e. to prove that the program is "correct".
We are building our new tool, Verus, to efficiently verify full functional correctness of low-level systems code written in a safe Rust dialect that supports expressing specifications and proofs. In this talk I'll introduce the basics of functional verification, the verification technique used by Verus, and I'll demonstrate how the tool, with the programmer's help, can ensure that programs are bug-free (or how it catches bugs, if they are any).
Slides: https://github.com/rust-zurichsee/meetups/tree/master/2023-06-08_miri-simd-hir
Guillaume's Blog: https://andrea.lattuada.me/
Would you like to chat or give a talk? Join us in our Matrix room:
https://matrix.to/#/#rust-zuerisee:matrix.coredump.ch
Support the Zürich community: https://estada.ch/support-my-work/
Chapters:
00:00 Introduction
01:19 Examples
38:40 Questions
A
A
A
B
B
B
B
It
was
testing
a
very
specific
case
and
I
didn't
catch
the
edge
case,
which
is
now
like
huge
for
this,
for
this
example,
but
you
can
imagine
you
can
think
about
some
some
cases
in
which
you
maybe
didn't
think
about
the
test
case
that
could
have
caught
the
issue.
So
you
know
you
could
go
and
write
another
test
and
and
run
it
and
now.
Finally,
we
get
the
test
failing
because
we
swapped
DNA
over
here
right.
B
So
you
yes
and
that's
how
test
driven
development
has
been
working
and
it
works
very
well.
One
needs
to
be
attentive
in
writing
the
tests
that
will
catch
edge
cases
or
like
unexpected
Behavior.
So
here
the
way
a
road
test
3
is
a
bit
different.
Instead
of
writing
the
return
value
that
we
expect
exactly
I
wrote
the
property
I
want
the
return
value
to
have
so
I'm
saying
the
return
value
here
should
be
either
of
the
two
arguments
and
should
be
the
greater
one
of
the
two.
B
C
B
Know
I
can
I
can
fix
the
bug
and
we're
going
to
get
this
The
Test
passing
hopefully
right.
So
the
point
I
wanted
to
make
here
is
you
have
to
write
a
test
which
tests
can
the
various
points
in
the
input
space
of
this
function.
But
you
mean
you
never
know,
really
that
you've
caught
all
the
possible
issues
and
bugs,
and
because
you,
you
can't
possibly
know
that
you
tested
for
all
the
cases
so
we're
gonna
now
move
into.
B
I
can
that
I
can
run
with
the
command
virus,
and
what
I
did
here
was
take
the
max
function
from
before
and
then
right
an
assertion,
and
this,
as
you
can
see
here,
it
doesn't
have
the
bank
it's
it's
a
bit
of
a
different
syntactic
construct
but
I'm
keeping
the
property
that
we
wanted
right.
We
want
to
say
that
that
property
is
valid
for
the
return
value
and
the
error
message
we
get
from
various
is
different.
It's
not
a
panic.
We
actually
never
run
the
code
here.
B
What
we
got
here
is
two
messages
that
say
that
this
assertion
failed,
but
first
doesn't
run
the
code.
What
verse
does
is
it
statically
checks
every
possible
way
to
that?
The
program
this
Pro
this
program
could
run
and
checks
whether
these
assertions
are
true
in
every
possible
case
now
you're
going
to
say
well,
this
is
not
going
to
work,
because
this
function
is
bugged
and
I'm
going
to
actually
take
the
opportunity
here
for
a
second
to
introduce
you
to
another
Concept
in
veros,
which
is
despite
me,
fixing
the
function
right
now.
B
The
tool
is
still
not
believing
still
telling
me
well,
this
assertions
are
not
gonna
are
not
true.
The
reason
for
that
is
that
various,
for
various
reasons
is
a
modular,
so
it
requires
you
to
provide
a
specification
for
every
function
that
you're
trying
to
verify,
and
so
what
I
did
here
was
just
to
move
those
assertions
into
this
insurance
clause
and
we're
saying
for
this
function.
We
want
the
return
value
to
be
either
of
the
inputs
and
the
greater
or
the
two
ones.
B
So
now,
if
I
run
various
on
this
program,
we
got
a
new
error
message
which
says:
fill
this
post
condition
here
and
it's
pointing
into
exactly
where
the
problem
is
and
that's
happening
at
the
end
of
the
function
body.
There's
only
one
return
here,
so
this
is
easy,
so,
as
you
can
imagine,
we
can
go
ahead
and
fix
this
run
it
again
and
now.
Finally,
Varys
is
happy
with
our
program.
Saying
functions
verify
so,
interestingly,
once
we
have
done
this
conceptually,
we
don't
need
to
write
any
tests.
Anymore.
B
Verus
has
just
proven
that
for
every
possible
A
and
B
that
you
could
pass
to
this
function,
these
Insurance
Clauses
will
will
hold.
So
we
know
that
there
isn't
a
possible
input
that
would
break
the
behavior
of
this
function.
Obviously
this
is
fairly
trivial.
You
can
imagine
a
more
complicated,
also
feel
free
to
stop
me
if
anything
is
unclear
or
if
you're
like.
What's
what
what's
that
or
if
you
want
me
to
try
something,
please
please
ask
I'm
happy
to
try
things
out.
Things.
Might
break
but
that's
the
fun
of
it
so
cool.
B
So
this
is
a
verification.
The
promise
of
verification
is
this
mathematical
guarantee
this
static,
guarantee
that
conceptually
we've
tested
the
function
for
every
possible
input
or
tested
the
program
for
every
possible
cool,
so
why
we
do
y
valves?
Why
am
I
talking
to
you
about
the
stolen?
Why
we've
been
developing
it?
The
context
is
that
of
all
of
the
people
on
the
first
slide
that
you
saw
a
lot
of
them
have
been
thinking
about
verifying
system
software
as
a
way
to
have
strong
correctness
guarantees.
B
This
is
kind
of
the
same
goall
as
testing,
but
hopefully
stronger
and
and
as
usual,
like
avoiding
data
loss
and
availability
of
my
consequences,
but
also
if
we
want
to
be
able
to
use
these
techniques
in
the
real
world,
we
need
to
be
able
to
use
the
verification
process
as
part
of
regular
development.
We
need
to
be
able
to
build
up
the
program
while
we
verify
it
and
then
keep
this
verification
going
and
also
once
we've
constructed
the
program.
B
Why
why
virus
again
again
we're
looking
at
languages
that
we
want
to
use
for
verifying
system
software
and,
if
you're
not
familiar
with
the
area,
there
is
more
and
more
interested
in
space,
and
this
is
moving
in
different
ways
from
Academia
to
Industry.
There's
now
verified
projects
and
teams
in
various
in
various
companies,
but
there's
a
spectrum
of
things
you
could
use,
and
there
is
things
that
are
easy
to
verify,
because
they're
more
like
math
and
we
are
going
to
do
math
to
try
and
improve
properties
of
our
programs.
B
And
there
are
things
like
closer
to
computers.
So,
like
the
the
produce,
the
whose
code
is
closer
to
what
you
end
up
running
on
the
actual
on
the
actual
computer,
which
is
something
that
systems
people
often
want
like
they
want
the
control.
They
don't
want
to
write,
sometimes
a
functional
program
because
they
don't
have
enough
control.
B
B
That's
it
that's
right,
so
it's
in
some
ways
a
functional
programming
language,
and
it
has
things
that
functional
programming
languages
have
at
for
a
long
time,
such
as
the
red
data
types
pattern
matching
and
restricted
side
effects.
So
we
think
of
rust
as
a
very
good
language
for
this
and
to
reinforce
this
and
I'm
not
going
to
belabor
the
point
you're
probably
familiar.
B
You
know,
rust
enforces
single
ownership
by
default,
using
What's
called
the
Rios,
linear
type
system
or
fine
type
system,
depending
on
your
interpretation,
and
the
demonstration
here
is
just
a
tree
data
structure.
We
have
a
left
and
a
right
node
at
each
node,
and
one
we're
going
to
try
and
do
here-
is
to
assign
the
right
child
of
left
to
also
be
the
left
child
on
the
right,
which
is
clearly
illegal
and
Ross
would
reject
us
right.
So
we
have
this
guarantee
that
everything
is
owned
uniquely
so
again.
B
This
is
why
we
we
like
rust
for
this
before
this
goal:
Ras
lineage
type
system,
trucks,
ownership
and
prevents
what's
called
aliased
mutable
references,
which
means
that
what
we
get
from
from
Russ
regularly
is
data
races
and
users
to
create
all
the
nice
properties
you're
familiar
with.
But
in
addition,
we
have
noticed
that
aliasing
is
a
challenge
when
doing
functional
verification,
so
the
kind
of
technique
to
do
development
as
I've
shown
before
and
when
you
do
a
functional
verification
of
imperative
code.
It's
often
required
to
that.
B
B
So
again,
this
should
be
obvious.
Rust
prevents
Alias,
mutable
references,
and
here
we
I'm
going
to
start
with
an
example
that
goes
into
why
it's
useful
for
verification.
So
we
have
this
structural
structure
count
as
a
balance,
so
we're
function,
transfer
that
takes
two
accounts,
source
and
destination
and
an
amount
to
transfer
between
them.
B
B
So
that's
why
rust
now
why
Varys
so
again,
the
goal
is
to
make
verification,
formal
verification,
practical
for
writing
system
software,
and
we
started
with
some
of
the
folks
on
the
first
slide,
using
a
tool
called
Daphne,
which
is
a
and
the
c-sharp
alike,
with
integrated
verification
tools
and
then
because
we
encountered
all
of
these
issues.
Thinking
about
how
to
reason
about
aliasing
when
writing
proofs
in
Daphne
we've
integrated
the
linear
type
system
into
Daphne,
so
it
kind
of
made
definitely
look
a
little
bit
more
like
rust.
B
It
was
a
fairly
straightforward,
linear
type
system,
but
it
indicated
that
that
would
have
improved
verification
experience
significantly,
and
so
we
started
to
think
well
we're
trying
to
make
definitely
look
like
rust.
Why
not
try
to
make
rust
look
like
Daphne,
which
is
tool
that
we
really
liked
in
terms
of
the
feature
it
provides
for
verification
I,
unfortunately,
can't
really
talk
about
more
Daphne
here,
but
you
can
look
it
up.
It's
a
really
interesting
language.
So
that's
how
various
came
to
be
virus
is
our
smt-based
intrinsic
verification
tool
of
safe
rust
code.
B
There's
a
few
caveats
I'm
going
to
get
to
all
of
them.
Also
there's
words
that
maybe
you've
not
seen
before
what
does
intrinsic
verification
mean.
That's
actually
something
that
I
was
already
talking
about
earlier,
which
is
if
we
go
back
to
our
example,
and
we
try
to
verify
it.
You
may
know
what
to
expect.
You
may
know
what
may
happen
here.
B
We
haven't
provided
a
specification
for
the
transfer
function,
and
so
varus
can't
really
tell
what's
going
to
happen
when
we
call
transfer
here
and
also
varus
is
worried
about
the
fact
that
we
might
overflow
here
and
there
so
virus
is
also
checking
that
no
panics
will
happen
and
the
way
we
fix
this
to
start
is
by
adding
a
what's
called
a
precondition.
So
we're
going
to
say
the
original
balance
before
we
call
the
function.
This
is
what
old
overage
says
should
be
greater
than
the
amount
we
don't.
B
We
shouldn't
be
able
to
withdraw
more
money
than
there
is
available
in
the
academy
amount
in
the
account
and
also
if
we
are
depositing
into
the
destination
account
we
shouldn't
overflow
E64
Max.
Now,
if
we
run
virus
again
here,
we
noticed
that
the
two
first
errors,
the
two
possible
already
underflow
and
overflows-
are
gone
because
now
Varys
looks
just
at
the
body
of
this
function
and
says:
well,
if
we
know
these
two
things,
then
these
two
cannot
possibly
overflow
yep.
C
D
B
B
Mean
great
question
so
we're
going
to
get
to
that
in
a
few
minutes,
but
I
can
mention
now
that
exactly
mean.
That
means
that
this
function
is
something
that
we
intend
to
execute.
So
it's
program
code
that
we
intend
to
actually
compile
and
execute
it's
going
to
be
other
code
that
we
don't
intend
to
compile
next
good,
but
I'll
get
to
that
in
a
second
and
while
I'm
talking
about
this,
you
may
have
noticed
that
the
syntax
looks
different.
B
So
now
we
were
saying
that
you
know
these
two
assertions
down
here
still
failing,
even
though
they
should
pass
and
what
we
can
do
to
fix.
That
is,
you
know,
make
sure
that
we
modularly
describe
what
the
transfer
function
does,
because
virus
is
only
going
to
rely
on
the
specification
to
determine
what
happens
when
we
call
the
function
and
then
we're
just
going
to
verify
the
two
functions
separately.
B
So
if
we
make
that
change
that
the
ensures
and
say
like
this
is
the
behavior
we
expect
now,
the
virus
can
verify
the
problem
and
I
want
to
stress
once
again
that
we're
not
running
the
program
but
there's
a
joking
verification
that
people
essentially
never
run
their
programs
except
like
two
days
before
the
deadline,
if
you're
in
Academia
and
but
we
still
get
so
in
theory.
If
virus
is
correct,
there
is
no
way
that
this
program
will
go
wrong,
and
so
in
some
ways
you
wouldn't
need
to
write
any
tests.
B
There
are
caveats
to
this.
Obviously
great,
so
that's
interesting
verification.
So
a
whole
logic
specification
is
a
description
of
what
happens
before
and
after
you
call
a
function.
For
example,
I
said
smt
based
as
well,
which
is
one
of
the
possible
techniques
you
can
do
verification
of
software.
There
is
more
manual
techniques
where
you
kind
of
write
the
proof
steps
by
hand,
but,
as
you
can
see
here,
this
program,
a
bit
simple
verifies
automatically
and
the
way
we
do
this
is
by
leveraging
an
smt
solver.
B
So
you
may
be
familiar
with
sat,
which
is
a
Boolean
satisfiability,
which
means
you
have
an
expression
and
you're
asking
yourself.
There
exists
an
assignment
of
X
and
Y
such
that.
That
expression
is
true
and
you
could
do
this
by
hand
or
you
could
grab
Z3,
which
is
a
very
powerful
and
often
used.
Smt,
solver
and
Z3
will
tell
you.
This
expression
is
true.
B
If,
for
example,
X
is
false
and
Y
is
true,
you
can
try,
but
what
we're
going
to
do
actually
is
go
and
look
at
that
program
and
actually
run
Z3
on
it.
So
you
get
an
idea
of
what
it
looks
like.
So
what
I
did
here
is
just
write
that
expression
from
before
from
the
slide
in
syntax,
that
c3a
understands
and
it's
kind
of
this
list
like
syntax
and
then
what
I'm
saying
is
check,
sat,
which
means
does
the
does
an
assignment
exist
and
we're
getting
the
response
to
sat.
B
Yes,
there
is,
and
get
model
means
tell
me
what
that
assignment,
what
one
of
that
those
assignments
could
be,
and
here
it's
saying
why
is
true
and
X
is
false,
which
is
what
we
expected
from
before
cool,
so
there's
an
extension
to
sat,
which
is
what
the
three
implements,
which
is
smt,
satisfiability
modular
theories,
meaning
that
we're
going
to
generalize
such
to
formulas.
That
include
other
theories,
so
real
numbers,
integers
data
structures
and
quantifiers,
which
turn
out
very
to
be
very
useful
when
doing
program
verification.
B
So,
for
example,
here
we're
going
to
say
we
could
say
that
for
all
A
and
B
A
times
b
equals
B
times
a,
and
we
should
be
able
to
prove
that
so
innocent
based
verification.
What
we
do
is
we
start
from
the
program,
so
here
I'm
going
to
try
to
explain
to
you
in
two
minutes
how
virus
works
at
a
very,
very
high
level,
so
we're
going
to
start
with
the
program
and
we
initially
wrote
this
test
by
hand
right.
B
But
what
I've
been
saying
is
we
don't
really
want
to
like
pick
two
x
and
y's?
We
want
to
say
what
happens
for
any
possible
A
and
B,
which
is
how
which
would
be
defined
by
the
insurance
clause.
And
now
what
we're
going
to
do
is
encode
things
like
this.
So
what
we
want
to
prove
is
that
for
all
A's,
A
and
B's,
the
max
of
A
and
B
is
a
or
b.
So
it's
one
of
the
two
initial
values.
B
This
is
just
kind
of
a
logic
encoding
of
this
expression
and
that
it's
greater
than
both
right.
So
what
we're
going
to
do
is
just
turn
that
for
all
into
a
not
exist,
not
which
is
a
valid
transformation
and
Z3
is
excellent.
At
figuring
out,
this
exist
part,
so
we
essentially
use
the
three
kind
of
the
other
way
around
we're
asking
it.
B
Can
you
prove
that
such
an
assignment
does
not
exist,
and
if
it
can
prove
it,
then
it
must
be
that
for
all
A
and
B,
that
expression
is
true,
and
so,
if
Z3
says,
sat
or
unknown,
so
there
exists
an
assignment
of
variables.
That
falsify
is
what
we
were
trying
to
prove.
Then
we
failed
and
if
it
says
unsat,
it
means
that
this
we
can
prove
that
there
is
no
assignment
to
A
and
B.
That
could
falsify
our
post
condition.
B
In
practice,
we
can
actually
prove
a
lot
of
useful
programs,
but
there
is
this
issue
that
sometimes
Z3
just
goes
off
and
Spins
and
never
returns,
and
we
know
we
need
to
figure
out
how
to
kind
of
deal
with
that
all
right.
So
when
using
a
tool
like
smt,
we
get
these
automatic
proofs
that
we
were
seeing
before
for
free,
at
least
at
this
level
of
complexity.
B
But
that
comes
with
the
fact
that
we
need
to
make
sure
to
use
this
Z3
tool
properly
to
extract
as
much
performance
out
of
this.
If
you
say
you're
seeing
that
like
it
takes
us
a
very
short
time
to
get
a
response,
but
that's
a
a
very
explicit
design
goal
for
varus
of
of
getting
a
verification
results
back
quickly
in
an
amount
of
time
that
resembles
how
it
would
like.
B
Look
like
just
you
know:
cargo
check
something
right:
it
takes
longer
for
more
complex
functions,
sometimes
significantly
longer,
but
that's
very
much
our
focus
and
we
achieve
this
by
prioritizing
efficient
encoding
to
smt
queries.
So
the
way
we
encode
the
program
in
virus
and
here
I
think
it's
interesting
to
actually
look
like
at
almost
what
the
verification
query
that
we
pass
to.
The
Z3
looks
like
for
this
program.
So
I
did
a
tiny
bit
of
editing
here
to
just
simplify
things
a
bit.
B
There
is
a
bunch
of
Prelude
to
them
and
I'm
going
to
talk
about
here.
They
just
ignore
this.
It's
fine!
It's
it's
the
same
for
it's
almost
the
same
for
every
for
every
function,
but
I
didn't
want
to
you
know,
be
dishonest
and
delete
a
bunch
of
stuff.
So
this
is
not
exactly
the
spin
I
think
I
deleted
like
seven
or
eight
lines
that
are
not
critical
for
doing
verification
here,
but
this
is
the
encoding,
basically
in
Z3
of
our
Max
function.
B
So
we
are
saying
see
the
knot
from
before
we
were
proving
that
exists,
not
something,
and
so
that's
exactly
where
it
shows
up.
Our
assumption
is
how
the
function
looks
like
so
we're
doing.
You
know
if
a
greater
than
b
b
a
and
then
what
we're
trying
to
prove
is
the
post
condition
from
before,
and
we
can
just
run
Z3
on
this
and
if
I
write
it
correctly,
we're
getting
unknown
here,
which
says,
which
means
definitely
sorry
various
kind
of
prove
that
the
program
is
wrong.
B
It
cannot
also
kind
of
prove
that
the
program
is
correct.
It's
saying-
and
this
is
incompleteness
so
meaning
that
virus
is
not
able
to
determine
all
the
time
which
one
of
the
two
is
the
case,
and
this
is
and
sorry
a
rather
Z3.
In
this
case,
however,
we
generally
just
treat
unknown
as
a
verification
failure
we're
just
saying
telling
the
user
we
would
be.
B
You
know
putting
up
to
the
user,
that
message
saying
that
the
surgeon
fails
or
that
post
condition
fails
and
then
the
user
has
to
come
back
and
give
us
a
bit
more
information
to
to
prove
their
program.
Okay.
So
now
this
is
unknown,
because
it's
a
simple
program
that
we
expect
Z3
to
probably
verify
correctly
automatically.
B
But
the
program
is
wrong
because
it's
the
same
bug
as
before
so
I'm,
just
gonna,
you
know
fix
stuff,
as
so,
this
kind
of
this
equivalent
of
fixing
the
function
definition
and
now
we're
getting
unsut
and,
as
a
reminder,
ansat
means
proof.
So
we've
just
proven
that
for
every
possible
assignment
to
A
and
B,
that
program
will
always
return
something.
That's
the
satisfies
our
specification
cool,
so
I've
shown
you
smaller
examples.
B
So
far,
I
want
to
get
once
into
what
it
looks
like
to
verify
something
a
bit
more
complex
and
the
example
here
is
the
you
know:
iterative
implementation
of
Fibonacci.
So
what
we're
doing
here
is
just
just
wrote
the
code,
the
executable
code,
that
we
want
exactly
is
back
here
again
because
that's
the
code
we
actually
want
to
execute.
B
However,
we
need
to
be
able
to
say
what
correct
means
in
this
context
and
what
we're
going
to
try
to
do
is
say.
Well,
we
need
to
make
sure
for
this
function,
we'll
need
to
make
sure
that
Fibonacci,
the
return
value
in
fact
fits
into
a
u64.
Otherwise,
it's
not
gonna
We're,
not
gonna,
be
able
to
return
it.
So
we
need
to
call
it
with
an
end
that
for
which
people
will
fit
and
the
insurer
says
the
result
is
the
fee
above
that
number.
But
what
that?
What
does
that
mean?
Well
in
Paris?
B
We
have
this
other
part
of
the
language
which
is
essentially
a
functional
language,
functional
mathematical
language,
which
now
is
marked
spec.
That
lets
us
describe
the
intended
behavior
of
the
program
in
a
more
abstract
mathematical
way.
So
this
is
the
you
know,
definition
of
fibo,
that
you
would
expect
mathematically
and
then
fibo
fitsu
64
is
just
that.
B
So
let
me
run
virus
on
E,
fibo
1.,
and
what
we're
saying
is
inverse
is
saying:
okay,
not
quite
this
was
conditioned.
We
can
approve,
and
this
might
overflow.
So
here
is
where
we
have
specified
the
function
fully.
We
think
but
smt
the
Z3
is
not
is
behaving
in
such
a
way
to
avoid
you
know,
spinning
a
fun
controllably,
and
so
it
holds
back
in
trying
out
potential
proofs,
and
so
we
need
to
guide
it
a
little
bit
and
the
way
we
do,
that
is
by
writing
proof
functions.
B
So
here
I
mean
I'm
not
going
to
go
into
how
we
got
here,
but
we're
gonna
say
we're.
Gonna
need
to
know
as
a
theorem
that
Fibonacci
is
monotonic
and
inverse.
Theorem
is
just
a
function
with
a
keyword
proof
in
front,
and
this
is
saying
for
I
less
than
J,
then
fibo
of
I
is
less
or
equal
to
V,
both
J,
and
we
need
to
also
prove
that
this
function
terminates,
but
that
doesn't
really
matter
here,
I'm
not
going
to
guarantee
to
like
how
the
proof
exactly
works.
B
B
You
know
in
inductive
cases
to
prove
this
current
case
and
but
again,
I'm
not
gonna,
go
into
exactly
the
details
of
the
proof
and
if
we
try
and
run
virus
on
this
so
because
we
don't
get
an
error,
there
is
actually
can
prove.
The
view
is
tonic
Lemma.
We
just
aren't
using
it
yet
the
way
we
get
to
use
it
is
first,
we
need
to
add
an
invariant.
B
B
B
A
B
We
just
do
whatever
Russ
does,
so
all
of
this
code
gets
passed
on
to
after
transformation.
It
actually
doesn't
look
that
it's
different
after
transformation
just
looks
like
rust,
and
we
just
rely
on
the
rust
type
Checker,
which
is
one
of
the
big
benefits
of
building
a
tool
on
top
of
rust,
is
that
we
have
access
to
all
of
that
type
system
and
all
those
features
from
the
type
system.
B
Assume,
oh
great,
so
like
how
technically
so
yeah
the
different
tools
do
different
things.
What
we
do
is
we
take
hir
and
use
that
to
generate
the
queries
like
there's
a
few
layers
of
transformation,
but
basically
we'll
get
we
start
from
there
and
and
then
we
at
some
point
run
the
Border
Checker
I'm,
going
to
get
to
exactly
the
fact
that
we
don't
always
run
the
motorcycle
with
all
right.
Thank
you,
yeah
thanks
great
question.
B
So
great
so
this
is,
you
know.
This
big
energy
function
is
now
verified
for
any
n
that
fits
into
u64
to
actually
compute
fibo
cool.
So
this
is
all
of
the
code
in
that
proof,
and
I'm
gonna
highlight
some
of
it
and
get
back
to
your
question
before
so
this
is
exact
code.
Mostly,
this
is
the
code
we
actually
want
to
run.
B
This
is
proof
code,
so
this
code
that
we
used
to
explain
to
varus
and
to
Z3
why
our
program
is
correct
and
this
is
spec
code.
So
this
is
how
are
this,
this
high
level
mathematical
language
kind
of
functional
language?
In
fact,
this
allows
mutation,
for
example,
that
lets
us
specify
what
our
program
should
do
and
lets
us
talk
about.
Some
properties
of
the
program.
What's
important
here
is
that
spec
and
proof
mode
code
are
ghost
ghost,
meaning
that
all
of
this
code
will
not
appear
in
the
final
in
the
final
binary.
B
So
the
interesting
thing
in
Varys
is
that
we
treat
this
is
not
quite
exactly
accurate,
but
it's
I
think
a
decent
approximation,
which
is
that
we
have
three
modes
of
code
that
we've
seen
and
we
only
type
check
spec
code.
We
don't
borrow
check
it,
which
means
that
you
actually
can
violate
some
of
rust's.
You
know
restrictions
on
on
aliasing
in
Spec
mode
code,
but
that's
sound
because
spec
mode
code
is
just
a
functional
language.
B
Proof
mode
code
is
treated
as
regular
rust,
but
we
erase
it
before
we
get
to
compilation,
and
so
that
lets
us
express
some
proofs
and
I'm
going
to
show
you
a
quick
example
in
a
second
and
then
exact
mode
code
is
just
regular,
rust
program.
We
want
to
run
that
program,
we're
just
going
to
compile
it
border
check
it
first
then
compile
it
Okay.
So,
as
mentioned
the
rust
type
system,
something
relies
on
for
its
correctness.
We
do
rely
on
the
fact
that
you
know.
B
B
You
get
to
do
aliasing
in
there.
If
you
do
it
right
and
various
allows
access
to
this.
Some
other
set
of
Primitives
that
we
wrote
that
are
like
pointers,
raw
pointers,
for
example,
that
let
us
interact
with
these
regular,
normally
unsafe
features
in
a
safe
way,
because
the
verifier
is
checking
some
of
the
assumptions
and
here's
an
example.
This
is
a
bit
involved,
so
I'm
just
gonna
try
and
go
over
the
concepts,
but
what's
Happening
Here
is
we
have
a
transfer
permission.
B
Function
is
just
saying
this
is
some
ghost
state
that
we
use
to
describe
the
program
that
we're
going
to
transfer
away,
store
copy
of
pointer,
just
stores
a
copy
of
the
pointer?
We
pass
it
to
so
think
of
pptr
as
just
a
star
mute
u64,
but
our
version
that's
conditionally
safe,
and
things
like
pptr
put
is
like
assigning
to
five.
But
there
is
this
additional
argument
here
which
I'll
get
to
in
a
second
and
then
take
is
essentially
like
PPR
assigned
to
null.
B
So
what
we
are
saying
here
is
we're
gonna
allocate
a
new
pointer.
It's
going
to
point
to
nothing.
Then
we're
gonna
give
a
copy
of
that
pointer
to
somebody
else.
The
pointer
is
just
copyable,
that's
fine!
We
know
that
it
doesn't
contain
anything.
Then
we're
gonna
store
a
value
of
five,
and
that
should
be
worrying
to
you.
We
just
gave
a
copy
of
somebody
to
somebody
else
that
somebody
else
may
spawn
a
thread
and
going
right
into
it.
B
That's
not
great
that
would
that
could
be
a
data
race
and
that
could
be
undefined
Behavior.
However,
we
get
to
do
this
safely
here,
because
we
have
this
tracked
permission,
which
is
a
go
system,
some
abstract
representation
of
the
fact
that
we
can
access
the
pointer
and
that's
treated
like
a
regular,
rust
type
so
linearly.
B
So
you
don't
get
to
Alias
it
and
because
we
are
still
holding
on
to
the
permission,
then
we
know
that
we
are
the
only
ones
we
would
possibly
be
doing
this
operation
at
this
point
and
then
once
we
do
that,
then
we
know
that
the
contain
value
is
5..
Then
we
try
to
transfer
the
permission
elsewhere,
because
we
first
with
some
more
complex
proof
around
it,
which
I'm
not
going
to
be
able
to
show
we're
going
to
say.
Somebody
else
now
gets
to
write
here,
but
this
is
totally
a
ghost
operation.
B
Now
this
program,
I'm
showing
is
actually
broken
because
after
we've
transferred
the
permission,
we
should
not
be
able
to
set
a
pointer
to
null
because
that
could
again
be
a
data
race,
right,
yeah,
and
so
here
the
cool
thing
is
that
we
get
to
rely
on
Rust
borrow
Checker
to
check
our
proof.
So
this
is
some
high
level,
more
complex
proof
and
access
permissions,
which
is
kind
of
a
separation
logic.
Inspired
for
those
of
you
familiar,
but
we
have
this
nice
interface.
B
Okay
so-
and
this
is
why
we
have
this
proof
mode-
which
is
this
program
this
this
style
of
code-
that
is
borrow,
checked
but
isn't
then
compiled,
and
all
of
these
those
are
all
the
fragments
that
are
in
fact
proof
mode
here
and
as
a
reminder,
those
are
ghosts
they
go
away.
So
we
don't
we're
not
spending
any
runtime
resources
on
transferring
there's
permission.
The
alternative
here
would
be
at
runtime.
We
transfer
an
owned,
you
know
box
elsewhere,
but
that
wouldn't
require
a
channel
and
then
that
transfer
the
transfer
explicitly
here.
B
If
we
can
set
up
a
protocol
around
this
to
control
how
this
permission
is
transferred
correctly
abstractly,
then
we
get
to
do
it
without
any
runtime
cost.
Okay.
So,
generally
speaking,
we
are
designing
varus
as
a
pragmatic
toolbox
for
verification
we've
seen
that
we
want
to
encode
it
to
smt
queries
efficiently,
so
we
get
good
verification
performance.
B
So
if
you
want
to
reason
about
a
concurrent
program
programs,
we
have
techniques
to
do
that,
and
this
is
based
primarily
on
work
done
at
CMU
by
travisans
and
hydrofox,
and
what
I
wanted
to
like
showcase
here
is
like
how
does
it
look
like
if
you
want
to
use
a
different
prover
here,
we're
going
to
try
to
prove
some
property
that
the?
If
we
divide
X
by
y,
then
the
result
is
smaller.
B
The
cost
is
still
high,
but
we
believe
we're
bringing
the
cost
down
as
a
community,
and
so
it's
starting
to
make
sense
in
the
industry
to
verify
some
systems,
some
kind
of
high
value
systems,
and
hopefully
that
will
continue.
The
cost
will
continue
to
go
down
so
that
more
people
can
use
tools
like
this,
but
as
researchers,
we
want
to
prove
that
varus
works
or
is
use
usable
at
some
level,
and
so
we
have
been
working
on
and
folks
in
a
different
institutions
have
been
working
on
different
projects
around
using
varus
to
verify
different
things.
B
So
the
project
verifying
the
correctness
of
kubernetes
controllers,
there's
a
project
led
by
Matthias
who's
in
the
room
on
verifying
the
page
table
code
for
an
operating
system,
kernel
and
More
in
general.
How
to
verify
an
operating
system
with
techniques
like
this
and
there's
more
that
we're
working
on
and
needs
to
come
from
a
bunch
of
institutions
so
very
quickly.
B
B
Why
would
you
want
to
write
code
that
doesn't
appear
in
the
in
the
binary,
and
so
we
have
been
working
with
a
bunch
of
folks
in
the
community
Folks
at
dth
from
brusty
and
Xavier
working
on
cruso,
which
is
another
verification
tool
to
add
support
for
ghost
code
to
the
rust,
compiler
and
we'll
be
making
some
progress
here.
Great
so
talked
about
birds
versus
our
toolbox
for
system
verification.
B
All
of
these
people
on
the
slides
have
worked
on
varus,
and
these
are
these.
People
are
not
in
any
specific
order,
so
versus
an
open
source
project
which
spans
a
bunch
of
different
institutions.
I
want
to
highlight,
because
we
are
a
tth
that
the
first
you
know,
few
tens
of
tons
of
lines
maybe
were
written
by
Chris,
hoblitzel
Microsoft
and
me
while
I
was
a
dth,
so
I
want
to
acknowledge
GTH
for
that
and
but
the
a
lot
of
these
people
have
it
input
even
early
on
on
the
design
of
the
tool.
B
So,
if
you're
interested
try,
the
guide
tried
Varys,
we
have
this
thanks
to
Folks
at
CMU.
We
have
this
cool
wrestling
play
wrestling
alike
over
there.
There's
a
paper
if
you're
academically
minded
and
if
you
have
questions
you're
trying
to
tools
things,
don't
work,
get
in
touch
either
on
GitHub,
just
open
an
issue
or
shoot
me.
An
email
and
yeah
I.
Think
with
that
yeah.
F
B
So
go
sell,
is
the
Branded
Lifetime
right
nice
so
go
sell?
Let
me
say
this
correctly.
Hopefully,
so
ghost
cell
has
this
technique
where
the
permission
is
encoded
as
a
branded
lifetime.
Essentially,
and
then
you
move
around
the
permission
and
that's
mainly
encoded
just
in
the
rust
type
system.
That
means
that
you
don't
get
to
use
the
tools,
reasoning
to
determine
how
you
can
move
around
the
permission.
So
using
this
be
vague.
B
I'm
happy
to
you
know
be
more
precise
later,
but
with
with
varus
we
get
to
so
things
like
pptr
put,
has
preconditions
that
are
checked
by
the
smt
solder.
So
we
get
a
lot
more
flexibility
on
how
we
transfer
the
permissions.
We
can
combine
permissions
into
like
a
linear
hash
set,
for
example,
like
leaner
goes.shet,
and
then
you
get
them
out
when
you
need
them
things
like
this,
so
we
get
to
rely
on
on
the
smt
solver.
In
addition
to
having
the
syntactic
element,
that
kind
of
proves
your
ownership
yeah
thanks.
F
E
So
yeah
to
add
to
that
the
one
way
to
think
about
it
is
the
hard
part
with
separating
the
permissions
from
the
data
is
to
still
know
which
permission
is
for
which
data
which
ghost
cell
does
with
this
branded
lifetime
trick,
which
is
super
tricky
and
unigonomic,
and
everything.
But
it's
the
amazing
thing
it
works
in
the
rust
compiler.
E
B
D
D
My
question
is
about
practicality,
so,
let's
say
in
the
practicality
spectrum
of
which
kind
of
programs.
Can
you
verify
with
that?
For
example,
can
you
verify
like
sorting
algorithms
yeah,
which
I
think
you
know
there
are
a
lot
of
even
newer
algorithms
that
are
more
optimized
or
whatever,
but
are
they
correct,
yeah.
B
Sorry
is
there
more
to
the
question
great
great
question,
so
yeah
you
can
verify
things
like
algorithms.
In
fact,
the
state
alert
is
pretty
good
at
verifying
individual
algorithms,
especially
if
they
don't
have
side
effects.
So
if
they're
kind
of
do
I
mean
this
is
not
a
sorting
algorithm
I
think
we
have
a
sorting
algorithm
example
somewhere,
but
I
just
had
this.
B
The
state
of
the
art
is
multiple
thousands
of
lines
for
programs
like
so
the
largest
projects.
I
know
of
are
well.
One
of
ours
in
Daphne
was
very
better
KV,
which
is
a
verified
key
value
store,
which
I
think
is
about
5000
lines
of
source.
There's
projects
in
using
the
Cog,
prover
I
think
Daisy.
Nfs
is
one
of
them
is
a
file
system
which
is
a
verified
file.
It's
a
completely
different
technique,
but
I
think
of
maybe
comparable
scale
and
I
know
that
there
is
a
wave
which
is
a
verified.
B
It's
not
fully
like
it's
not
for
functional
correctness.
The
wave
is
a
runtime
for
webassembly
and
it
doesn't
they
don't
verify
my
understanding.
Is
they
don't
verify
that
it
runs
webassembly
correctly,
but
they
do
verify
that
the
runtime
will
not
do
anything,
but
it's
not
supposed
to
so
webassembly
is
supposed
to
be,
you
know
sandboxed,
and
so
they
verify
the
sandboxing
property,
and
so
the
scale
we
are
at
now
is
multiple
thousands
of
lives
of
code.
B
Multiple.
You
know
PhD
years
of
effort
that
hopefully
where
we
are
trying
to
like
improve
on.
So,
in
fact
the
verified
page
table
project
I
think
was
successful
in
that
sense,
because
we
got
very
good
verification
time.
So
the
iteration
time
was
good.
You
can
ask
materials
how
frustrating
it
was
afterwards
and
and
it's
it's
a
sizable
program
with
very
complex
interaction
with
the
system.
So
you
know,
space
table
is
writing
to
like
the
page
table
memory
or
whatever
good
question.
B
We
could
have
a
separate
API
that
does
not
make
the
Assumption
the
advantage
of
allocation
failure
is
that
in
Rust
regularly
I
think
it
just
crashes,
which
is
not
ideal
for
a
verified
program,
but
not
the
worst
outcome,
because
you're
not
going
to
do
anything
horribly
wrong.
One
interesting
thing
about
at
least
this
kind
of
techniques
is
you're
still
proving
partial
correctness
anyway,
which
means
you're
not
going
to
actually
prove
that
the
program
will
terminate
so
a
program
can
just
also
spin
forever
and
be
considered
correct.
B
There
are
techniques
to
also
address
that,
but
so
there
are
limits,
but
for
sure
allocation
is
something
that
currently,
we
assume
to
always
succeed,
and
if
we
want
complete
Summers
from
that
aspect,
we
should
probably
also
check
every
allocation
and
assume
that
again
handle
and
the
user
would
have
to
handle
the
case
of
the
panic
in
practice.
Many
systems
just
make
that
assumption
anyways
and
it's
a
pragmatic
choice,
but
for
some
environments
you
will
need
something
else.
Does
the
answer
Yeah
question?
Thank
you.
B
B
We
focus
on
correctness,
so
the
concurrent
program
results
in
the
correct
sorry
produces
the
correct
result
and
there
are
no
data
races.
There
are
no
concurrency
others,
so
we're
focusing
on
that
aspect
and
a
verified
program
inverse
using
the
concurrency
verification
techniques
could
very
well
still
be
deadlock.
Otherwise,
good
question.
H
And
so
far
examples
that
I
saw
they
seem
like
to
verify
within
a
body
of
the
function.
If
things
are
what
about
across
the
calls
like
in
the
continuation
style
or
you
know,
you
sometimes
execute
a
bit,
then
the
data
goes
somewhere
else
come
back
and
you
continue,
and
you
would
like
to
verify
that
the
whole
flow
is
correct.
Right
and
yeah.
B
Yeah
great
question:
so,
if
it's
you
know
just
a
regular
function,
call
like
we
were
doing
for
I.
Think
here
you
know
the
transfer
function.
What
happens
is
that
we
do
this
module
verification
approach.
Where
you
talk
about
what
the
transfer
function
does
and
then
that
lets
you
thread
that
knowledge
through
the
transfer
function,
call
I,
think
you're,
also
asking
things
about
like
a
continuation,
passing
style
or
like
as
async
essentially,
and
we
haven't
looked
into
async.
B
But,
generally
speaking,
this
style
of
tools
requires
you
to
build
up
your
verification
using
this
module
style.
So
every
function
will
carry
a
specification
inside
what
it
does
abstractly
and
you
can
abstract
quite
a
bit.
Fortunately,
and
then,
if
you
have
big
programs
and
complex
programs,
the
technique
that
Varys
optimizes
for
is
a
state
machine
refinement
which
is
using
the
kind
of
iron
Fleet
style.
B
B
A
A
B
Yeah
great
so,
let's
see
I
I,
don't
know,
I
think
there's
an
interesting
answer
here,
but
it's
maybe
it
may
be
long.
Whoever
asked
this
please
get
in
touch.
So,
let's
see,
if
I
can
make
it
quick,
so
linear
types
I,
we
think,
is
a
very
convenient
interface
for
the
kind
of
the
cell
person.
Writing.
But
there's
been
a
lot
of
success
using
inspiration,
logic,
which
is
a
style
of
type
system
in
which
the
values
can
be
used
multiple
times
in
certain
ways.
B
So
you
get
to
take
a
values,
split
it
up
and
then
give
fractions
to
everybody.
So
there's
definitely
overlap
there,
where
our
techniques
are
very
much
inspired
by
those
the
relationship
with
Idris
I,
really
don't
remember
much
of
Iris
I
looked
at
it
at
some
point,
so
I'm
not
sure
but
yeah.
If
you're
interested
in
more
just
get
in
touch.
Hopefully
that's
satisfying
enough.