►
From YouTube: crux-mir: Symbolic testing for Rust
Description
Aaron Tomb and Stuart Pernsteiner
A
Our
next
two
speakers-
well,
I
think
it's
going
to
be
stewart
who's
actually
going
to
be
speaking,
but
we,
the
two
names
on
the
presentation,
are
aaron
toom
and
stewart.
Parentsteiner
we're
talking
about
crux,
mirror
symbolic
testing
for
rust,
two
fun
facts:
they
both
work
at
gawa
and
also,
I
can't
find
anything
about
them
with
google.
So
there
you
have
it,
but
it
turned
out.
Stuart
did
email
me
later
that
stuart
worked
and
built
a
number
of
oh.
B
B
Now
it
claims
to
be
sharing
the
screen.
So
today,
I'm
going
to
be
talking
about
crux
mirror,
which
is
a
symbolic
testing
tool
for
rust,
code
and
kind
of
the
purpose
of
cruxmere
in
one
slide,
is
that
we
want
to
take
the
testing
workflow,
that
developers
are
already
familiar
with
and
extend
it
with
symbolic
execution
capabilities.
B
So
on
the
left,
you
have
kind
of
a
perfectly
ordinary
rust
test.
It
sets
up
some
input
values,
it
calls
a
function
on
those
inputs
and
it
has
an
assertion
to
check
that
the
output
of
the
function
satisfies
some
desired
condition
and
if
the
developer
writes
this
code
and
then
runs
cargo
test,
karger
will
build
in
on
their
test
and
tell
them
that
indeed,
on
this
particular
set
of
inputs,
the
function
is
doing.
The
right
thing
now
on
the
right
is
a
symbolic
test
for
use
with
cruxmere.
B
The
idea
here
is
that
this
should
be
kind
of
as
similar
as
possible
to
the
concrete
test
so
that
it's
using
things
that
developers
are
already
familiar
with,
and
in
this
case
there
are
kind
of
three
main
changes
right.
We
change
the
test
attribute
to
crux
test,
to
indicate
that
you
know
this
is
a
a
symbolic
test
for
use
with
crux
smear.
B
In
this
case,
we
only
care
about
y
values
that
are
at
least
400,
and
if
we
run
the
cargo
crux
test
command
on
on
this
code,
it
will
check
not
only
a
single
set
of
inputs,
but
all
possible
inputs
that
satisfy
those
assumptions
to
make
sure
that
the
function
behaves
properly
on
all
of
them
and
in
terms
of
the
kind
of
features
that
crux
mirror
supports.
At
the
moment
on
the
kind
of
rust
language
features
side
we
can
handle
generics,
traits
closures,
trait
objects
and
a
little
bit
of
unsafe
code.
B
B
I'm
next
going
to
get
into
specifically
like
what
kind
of
use
cases
this
is
built
for
since
that
informs
the
design
and
also
a
more
detailed
example
of
what
it
looks
like
to
use
the
tool.
Then
I'll
talk
in
about
the
kind
of
design
and
architecture
and
then,
finally,
how
we
went
about
supporting
some
particular
interesting
rust
features
like
generics,
the
standard
library
and
that
cargo
integration.
B
B
There
are
still
some
interesting
things
to
look
at
particularly
implementations
of
cryptographic,
algorithms.
This
was
kind
of
one
of
the
main
use
cases
of
the
symbolic
execution
engine
that
we're
building
on,
and
so
crux.
Spinner
also
supports
this
pretty
well,
and
we've
also
had
some
success.
Looking
at
like
serialization
deserialization
code,
where
you
want
to
verify
that,
if
you
serialize
and
deserialize,
you
don't
lose
any
data
or
that,
if
you
feed
you
know
possibly
garbage
data
into
your
deserializer,
it
will
fail
gracefully
and
return
an
error
code
instead
of
just
panicking.
B
B
We
particularly
looked
at
the
scalar
52
type,
which
is
their
implementation
of
modular
arithmetic.
They
want
to
do
you
know
addition
subtraction
multiplication,
modulo,
some
big
prime,
constant
l
and,
of
course
this
is
optimized
for
performance,
so
the
implementation
of
that
scalar,
52
type,
isn't
just
a
wrapper
around
some
big
number
library.
It's
doing
something!
Fancy
and
these
you
know,
arithmetic
operations
are
similarly,
you
know
kind
of
complicated.
B
So
the
question
here
is,
you
know:
can
we
verify
that
these
optimized
implementations
actually
correctly
implement
the
arithmetic
that
they
are
supposed
to
do
so?
The
way
that
we
verify
that
with
cruxmere?
Is
we
write
a
blog
test
that
looks
like
this
and
we,
oh?
I
was
gonna,
try
and
move
my
mouse
over
this,
but
my
mouse
disappears
when
I
move
it
over
the
presentation
so
never
mind.
So,
at
the
top
we
set
up
some
symbolic
input
values
a
and
b,
which
are
just
arbitrary,
scalar,
52
values.
B
B
B
B
The
rust
source
code
goes
into
mirror
json,
which
is
a
rust
c
wrapper,
mirror
json
builds
the
code
as
rusty
would
normally
do,
but
also
on
the
side
dumps
out
a
representation
of
the
mirror
for
all
of
the
functions
in
the
crate.
That
representation
of
the
mirror
is
what
gets
fed
into
the
crux
mirror
back.
End
crux:
mirror
translates
the
mirror
to
crucibles
internal
language
and
then
runs
symbolic
execution
on
it.
B
So
before
I
get
into
kind
of
the
details
of
the
rust
side
of
things,
I'm
going
to
talk
a
bit
about
kind
of
what
crucible
is
and
what
it
does.
So
the
crucible,
symbolic
execution
engine
is
built
on
top
of
the
creatively
named
crucible
language,
which
is
just
a
strongly
typed
imperative
language
that
is
designed
as
a
a
translation
target.
B
So
if
you
want
to
do
symbolic
execution
on
some
higher
level
language,
you
can
translate
it
into
crucible
and
then
run
the
crucible
symbolic
execution
engine
on
that
the
crucible
language
supports
as
primitive
types.
Basically,
the
types
you
would
see
supported
natively
in
smt
solvers,
so
booleans
bit
vectors,
smt
arrays
out
of
this
set
mirror
mostly
uses
booleans
and
bit
vectors,
since
those
are
kind
of
the
natural
translation
of
rust's
bool
type-
and
you
know
primitive,
integer
types,
you
can
also
compose
those
types
into
higher
level
types
such
as
structs
enums
vectors.
B
B
So
here
on
the
right,
you
know
we
start
with
x,
equals
zero
y
equals
one
then
branch
on
some
symbolic
value.
On
the
left
side.
We,
you
know
we
assign
x
to
five
on
the
right
side
we
reassign
y
instead
and
when
the
when
the
two
branches
rejoin,
then
the
final
in
the
final
state,
the
symbolic
expression
for
the
value
of
x,
has
this.
You
know
conditional
in
it.
If
the
symbolic
condition
was
true
at
the
point
of
the
branch,
then
x
is
now
five.
B
Otherwise
it
has
kept
its
old
value
of
zero
and
similarly
for
y
now,
maybe
a
little
more
interesting
is
how
we
handle
loops
and
the
way
we
handle
loops
is
we
don't
unroll
them
to
any
specific,
predetermined
bound?
We
just
keep
unrolling
until
we
can
prove
that
the
loop
doesn't
need
any
more
iterations.
B
So
here
on
the
right,
we
have
some
initial
state
where
n
is
a
symbolic
variable
and
we
have
an
assumption
stating
that
n
is
no
more
than
10.,
and
so,
as
we
go
around
this
loop,
you
know
each
time
it
reaches
the
branch
to
decide
if
it
should
continue,
looping
or
or
go
to
the
skip.
At
the
end,
it
queries
the
smt
solver
to
check
which
of
those
paths
are
feasible.
The
first
10
times
going
around
the
loop
is
still
feasible,
but
after
10
iterations
there
are
no
possible
inputs.
B
So
everything
I've
said
about
crucible,
so
far
is
kind
of
you
know
generic,
no
matter
what
source
language
you're
translating
down
to
crucible.
You
know
it
has
the
same
type
system.
It
uses
the
same
execution
strategy.
The
interesting
part
where
we
had
to
implement
a
crucible
extension
was
for
the
rust
memory
model.
You
know
how
do
you
represent
memory?
B
How
do
you
represent
references
in
particular,
and
so
the
memory
model
that
we're
using
in
crux
mirror
memory
is
a
collection
of
independent
objects
and
each
object
is
strongly
typed.
So
if
you
have,
for
example,
like
a
rust
variable,
whose
type
is
a
pair
of
i32s,
then
the
corresponding
that
corresponds
to
a
single
object
in
in
the
memory
model,
whose
type
is
a
crucible
struct
containing
two
fields
that
are
both
32-bit
vectors.
B
The
one
maybe
interesting
thing
about
this
particular
memory
model
is
that
all
of
the
object
layouts
are
kept
kind
of
abstract,
so
the
memory
model
does
not
reason
about
kind
of
field,
offsets
and
things
like
that.
So
in
rust,
how
do
we
handle
transmute
yeah?
We
don't
yeah.
So
in
rust,
you
can
have
a
struct
with
you
know
four
bytes
in
it,
and
you
can
do
some
reasoning
about.
Oh
this
field
is
at
offset
zero.
This
field
is
offset
one.
B
So
if
I
transmute
this
struct
to
a
u32,
you
know
I
can
have
kind
of
some
idea
of
what
I
will
get
out
of
that
conversion
and
in
crux
mirror
that
kind
of
conversion
is
just
not
supported
by
the
memory
model.
So,
of
course,
this
limits
our
ability
to
handle
a
lot
of
unsafe
code,
but
we
can
still
handle
you
know
most
safe
code,
just
fine
as
long
as
the
kind
of
underlying
library
calls
that
it's
making
are
supported,
and
also
this,
this
kind
of
simplifies
some
things.
B
B
We
just
sort
of
reject
code
that
that
tries
to
do
that,
and
we
have
some
ideas
on
how
we
could
support
transmutes
and
other
things
like
that,
but
it
would
be
kind
of
tricky
and
we
haven't
really
needed
it
yet
so,
just
to
finish
up
the
memory
model
topic,
the
representation
of
references
since
memory
has
this
sort
of
type
structure
to
it.
The
references
also
have
some
structure
to
them
right,
they're,
not
just
like
an
address
or
like
a
block
and
offset
number.
B
Instead,
they
consist
of
a
root
object,
a
reference
to
some
root
object
and
then
a
path
to
some
sub
element
within
that
object.
So
if
you
have
so,
you
might
have
a
reference
to
the
second
array
element
of
the
first
field
of
the
local
variable
x
and
their
x
is
your
root
object
and
the
the
field
and
index
parts
make
up
the
path
all
right,
so
that
is
it
for
crucible
and
the
kind
of
general
design
of
crux
mirror.
B
I'm
next
going
to
get
into
some
details
about
how
we
handle
generics,
how
we
handle
the
standard
library
in
unsafe
code
and
kind
of
a
bit
about
the
cargo
integration.
Assuming
I
have
time,
which
I
might
not
so
for
generics.
Our
initial
inclination
with
generics
was
to
say
well,
rust
has
generics
and
crucible
supports
generic.
B
So
you
know
here
we
have
the
peakable
struct.
It
takes
an
iterator
as
a
type
parameter
and
contains
an
instance
of
that
iterator
type
right
in
its
inner
field,
but
then
its
peaked
field,
references,
the
item,
type
of
that
iterator,
and
so
in
crucible.
You
know
it's
perfectly
happy
if
you
have
some
type
parameter
and
use
that
as
a
field
in
your
object,
but
here
we
have
kind
of
maybe
seemingly
unrelated
type
right.
This
this
item
type,
which
is
somehow
derived
from
the
iterator
type
and
crucible,
is
really
not
it's.
You
know.
B
Polymorphism
support
is
really
not
set
up
in
a
way
that
can
handle
that,
and
so
we
thought
about
like
how
can
we
you
know
what
kind
of
workarounds
can
we
do?
What
kind
of
extra
information
can
we
export,
alongside
the
mirror
code,
to
make
this
work
out?
But
what
we
eventually
concluded
is
that
really
trying
to
handle
this
on
the
crux
mirror
back
end
is:
would
probably
amount
to
just
duplicating
logic
and
duplicating
things
that
rust
c
already
knows
how
to
do
so.
B
If
you
use
s
of
bool
and
if
you
use
s
of
I
32
right
and
those
are
as
far
as
the
back
end
can
see
two
totally
independent
structs,
and
it
doesn't
really
have
to
reason
about
like
how
do
I
construct
a
concrete
type
from
from
this
generic
type
definition
and
so
on,
and
so
in
particular,
in
the
case
of
peekaboo.
You
know
this.
B
Has
you
know
that
you
know
the
back
end
as
far
as
it's
concerned,
right,
peekaboo,
foo
and
peekable
bar
are
just
two
totally
independent
structs.
It
doesn't
matter
that
you
know
the
peaked
field
for
the
first
one
uses
a
bull
and
the
peaked
field
for
the
second
one
uses
an
I-32,
because
they're
totally
unrelated
right
and
the
code
passed
to
the
back
end
has
no
generics
of
any
kind
left
in
it,
and
most
of
the
traits
have
been
erased
as
well.
B
I
guess
monomorphization
helps
here
as
well,
since
we
can
treat
you
know,
iterators
with
an
item
type
of
bool
as
a
totally
independent
trait
from
iterators
with
an
item
type
of
i32
and
again,
that's
you
know,
work
that
the
back
end
doesn't
have
to
doesn't
have
to
worry
about.
We
can
just
kind
of
query
rusty,
you
know,
hey,
can
you
do
this
substitution
of
this
trait
definition,
and
it
will
do
it?
B
I
guess
the
other
thing
is
we,
whenever
the
front
end
encounters
a
cast
from
some
concrete
type
to
some
trait
object
type,
it
annotates
that
cast
in
the
the
mirror
code
that
it
outputs
like
when
it
goes
to
serialize
the
mirror
for
that
cast
it
annotates
it
with
the
id
of
the
particular
vtable
instance.
That's
being
used
to
make
that
cast
possible.
B
B
So
in
summary,
you
know
we
are
monomorphizing,
basically
everything
that
can
possibly
be
monomorphized,
we're
doing
it
at
the
mirror
level,
so
we
get
kind
of
monomorphized
mirror
that
looks
you
know
almost
like
c,
except
using
rust
types
right,
but
it
has
no
generics
at
all
because
we're
doing
this
we're
kind
of
using
rust,
compiler
infrastructure
to
do
all
this
monomorphization
we
get
a
bunch
of
things.
Kind
of
for
free,
so
closures,
for
example,
right,
like
a
call
to
a
closure,
is
really
just
like
a
call
to
a
trait
method.
B
On
a
particular
you
know
funny
named
type,
and
if
we
can
handle
trait
methods
we
can
handle
closure
calls,
you
know
just
as
well,
it
did
need
some
special
handling
for
the
rustcall
avi,
that's
used
in
those
fun
and
related
closure
traits,
but
that
was
kind
of
the
main
work
that
we
had
to
do
in
the
back
end
to
support
this.
The
other
thing
is,
you
know,
as
rusty
started,
adding
things
like
you
know,
const
generics
and
specialization
it
turned
out.
B
We
had
to
do
almost
no
work
for
for
supporting
these,
because
you
know
when
we
monomorphized,
we
just
call
rusty's
internal
substitution
functions
when
the
rusty
developers
added
const
generics.
They,
you
know
added
cost
generic
support
to
their
substitution
functions
too,
and
so
we
got
all
that
all
that
support
totally
for
free
all
right.
The
next
bit
is
on
how
we
handle
the
standard
library
in
unsafe
code
and
specifically
the
way
I
the
reason
I
lumped
these
two
seemingly
unrelated
topics
together.
B
Is
that
our
main
motivation
for
adding
unsafe
code
support
is
to
support
the
standard
library?
We
would
really
like
to
not
have
to
write
specifications
or
patches
to
the
standard
library,
for
you
know
every
single
function
of
the
library
or
something
like
that.
We
really
want
to
just
if
we
can
support
the
lower
level
primitives,
which
don't
tend
to
really
change
and
just
be
able
to
directly
execute
the
higher
level
parts
of
the
standard
library
based
on
those
primitives.
B
B
That
doesn't
have
a
lifetime
on
it.
We
did
have
to
add
support
for
integer
to
pointer
cast
so
that
you
can
have
like
null
pointers
and
the
special
dangling
pointer.
That's
used
for
like
empty
slices,
and
things
like
that
and
implement
fat
pointer
to
thin
pointer
casts
and
a
bunch
of
intrinsics
which
are
on
the
next
slide.
B
The
things
we
kind
of,
notably
don't
support,
are
you
know,
unions,
transmute
and
casting
raw
pointers
to
a
pointer
to
a
different
type,
since
these
are
all
ways
of
reinterpreting
some
bytes
as
as
an
element
of
a
different
type
than
they
originally
were,
and
that's
something
that
our
memory
model
doesn't
handle.
At
the
moment
we
did
special
case
a
few
things
in
our
stub
for
transmute,
but
that's
it
and
we
don't
support
pointer
to
integer,
casts
kind
of
along
the
same
lines
right.
B
Our
memory
model
doesn't
have
a
notion
of
how
to
map
its
abstract
memory
down
to
kind
of
a
flat
byte
array
where
things
are
at
consistent
positions
relative
to
each
other
right.
So
we
just
don't
allow
pointer
to
integer
cast
at
all,
rather
than
trying
to
come
up
with
a
way
to
make
that
consistent
and
again
this
hasn't
been
an
issue.
So
far
on
the
code
that
we've
been
looking
at
since
we've
been
looking
at,
you
know
like
cryptographic,
code
and
things
like
that
where
people
try
to
avoid
unsafe
code
anyway.
B
So
as
long
as
we
can
handle,
what's
in
the
standard
library,
that's
sort
of
good
enough
for
what
we're
doing
so
far
so
low
level
pointer
offset.
We
do
support
pointer,
offset
pointer,
arithmetic
within
arrays
only
since
this
is
used
for
basically
in
slice
and
vect,
and
the
way
this
works
is,
if
you
have
a
pointer
to
an
element
of
a
a
crucible
vector
that
reference.
B
You
know
its
path
ends
with
this
is
index.
Zero
of
this
of
you
know
the
the
vector,
and
then
you
can
just
increment
or
decrement
that
index
and
as
long
as
you
don't
go
off
the
end
of
the
vector,
it's
all
okay,
we
also
implement
some
low-level
memory,
intrinsics,
so
mems
swap
you
know,
which
is
kind
of
the
primitive
behind
memory
place
which
gets
used
all
over
the
place.
Also
pointer,
read,
pointer,
right,
etc,
an
unsafe
cell,
which
is
actually
pretty
straightforward,
since
we
don't
actually
yeah.
B
I
guess
that's
not
really
all
that
important.
I
guess,
but
we
implemented
all
this
stuff
via
the
overrides
or
kind
of
which
kind
of
replaced
the
the
rust
definition
of
of
some
of
these
functions,
or
you
know
if
they're
intrinsic,
they
don't
have
a
definition
with
some
custom
haskell
code
that
interacts
with
the
the
crux
mirror
memory
model,
and
since
we
support
all
these
primitives,
we
avoid
needing
to
modify
the
higher
level
and
more
complex
code
that
builds
on
top
of
them.
B
So,
like
the
slice
library
we
have
a
pretty
like,
we
still
have
some
patches
to
the
slice
library
that
we
use
to
make
it
compatible
with
cruxmere,
but
they're,
not
all
that
many
lines
of
code,
and
so
every
time
we
update
to
a
new
version
of
rust.
We
have
to
port
this
to
the
new
version
of
the
standard
library.
B
B
This
is
about
vec,
but
I
am
running
out
of
time,
so
I'm
going
to
skip
it.
I
guess
the
only
interesting
thing
here
is.
We
have
to
replace
all
the
allocate
and
de-allocate
calls
since
we
require
you,
you
can't
just
allocate
a
bunch
of
bytes
and
decide
later
what
type
of
thing
you
want
to
put
in
there.
You
have
to
say
up
front
for
the
memory
model,
what
it
is,
what
type
of
things
you're
allocating
and
unfortunately,.
B
Going
to
skip
the
cargo
integration,
but
the
short
version
of
this
is
you
should
go.
Look
at
that
cargo
mirror
code
that
ralph
linked
previously
in
the
chat,
since
it
is
doing
almost
exactly
the
same
thing
as
what
crux
mirror
is
doing,
but
seems
to
be
probably
more
robust
and
looks
to
have
better
comments
than
than
our
code
does
right.
B
B
I
think
we're
using
a
similar
strategy
to
that
we're
looking
at
kind
of
all
possible
interleavings
of
a
particular
piece
of
code,
but
since
we're
also
in
this,
you
know
symbolic
execution
context.
We
can
look
at.
We
can
test
not
only
all
possible
interleavings
but
kind
of
all
possible
interleavings
times
all
possible
inputs
all
right.
So
I
think
that
is
it
for
for
crux,
mirror
I've
kind
of
given
you
the
overview
of
what
it
does
and
how
some
of
the
internals
are
put
together.
A
A
A
It's
rust-verify.zoolibchat.com
might
be
a
great
place
for
people
to
talk
either.
You
know
during
or
after
the
talk
and
maybe
after
the
workshop
ends,
so
we
can
keep
keep
working
on
this
stuff
together.
Apart
from
that,
let's
go
through
some
of
the
questions.
There
were
some
in
the
in
the
chat
that
I
didn't
that
I
wanted.
I
thought
might
be
good
to
follow
up
on
so,
for
example,
there's
a
question
whether
crux
mirror
is
doing
its
own
monomorphization.
B
What
we
are
doing
is
we
are,
I
guess
we
kind
of
are
doing
our
own
model
organization,
but
it's
not
very
complicated,
because
rusty
already
has
apis
for
doing
type
substitutions
on
all
sorts
of
its
internal
data
structures.
So
you
can
just
take
the
mirror
for
an
entire
function
and
say
substitute.
You
know
these
concrete
types
for
the
generics
of
that
function
and
it's
you
know
it's
one
line
of
code,
basically
yeah.
A
B
Bond,
yes,
we
do
not,
I
guess
right,
like
custom
dsts
right
where
you
have
like
a
struct,
where
the
last
field
is
a
slice
that
could
have
arbitrary
length.
We
do
not
support
those
at
the
moment
right.
This
would
this
this
needs
to
be
like
it
would
need
to
be
kind
of
a
weird
combination
of
like
a
crucible
struct
and
a
crucible
vector
type,
which
I
don't
think
we
really
thought
about
kind
of
how
to
do
that.
Quite
yet,.
D
B
C
So
I
could,
I
could
step
in
and
say
either
that
we
we're
not
doing
concolic
execution
right
now.
We've
we've
explored
that
possibility,
but
we
haven't
so
at
the
moment
we're
just
doing
purely
symbolic
execution,
so
we're
executing
over
all
possible
inputs
symbolically.
Does
that
answer
your
question?
Yes,
it
does.
Thank.
C
A
E
I
would
have
another
question
not
about
the
transparent
stuff,
so
you
mentioned
unsafe
cell
does.
Does
that
mean
you
support
interior
immutability,
like
programs
that
you
sell
and
stuff,
and
what
does
it
like?
How
how
good
are
the
servers
able
to
handle
code
that
actually
has
interesting
sharing
patterns.
A
I
guess
I
have
a
question.
I
have
one
last
question,
it's
kind
of
a
question
for
the
room
actually
as
much
for
herman
as
for
and
others,
but
I'm
curious
whether
you
know
one
thing
that
they
came
up
when
talking
in
the
mirai
discussion
was
then
the
problem
of
hitting
functions
where
you
don't
have
the
source
and
needing
sort
of
summaries
or
or
other
stuff
to
allow
people.
B
And
I
guess
I
can
say
real,
quick
like
on
the
cruxmere
side,
we
don't
usually
run
into
many
functions
where
we
don't
have
a
source
code.
Since
we
are
building
our
own
version
of
the
standard
library,
we
can
export
the
mirror
right.
You
know,
there's
a
problem
like
the
standard
library
is
normally
built.
Without
that
always
encode
mirror
flag,
but
there's
some
functions
in
there
that
don't
have
mirror,
but
since
we're
building
it
ourselves,
we
can
export
the
mirror
for
anything
we
want,
which
you
know
is
right.
E
Okay,
so
that
that's
pretty
much
exactly
what
also
happens
in
mary,
the
the
cargo
mirror
wrapper
builds
its
own
sand
library
with
a
bunch
of
dedicated
flags
in
particular
they
always
encode
my
flag,
so
that
inside
mary
is
exactly
the
same
situation
only
intrinsics
and
foreign
codes,
and
that
it's
not
terribly
like
I
mean
there
are
the
number
of
intrinsics
is
very
finite.
So
that's
not
as
long
as
you
don't
run
into
zindy.
So
that's
that's!
E
But
what
I
guess
could
be
interesting
is
that
it
seems
like
there
are
at
least
two,
if
not
more,
I've,
I've
clicked
through
the
crooks
crystal
christmas
report.
I've
not
found
the
cargo
wrapper,
but
it
seems
like
there
are
at
least
two,
if
not
more,
implementations,
of
like
a
thing
that
wraps
cargo
to
build
its
own
snare
library
and
with
a
special
flag
and
then
also
build
all
of
the
dependencies
of
the
local
crate
with
that
flag.
E
But
then
have
to
be
very
careful
to
not
build
truck
macros
with
that
flag,
because
then
they
will
fail,
depending
on
the
flags,
at
least
in
very.
If
you,
you
can't
actually
build.
Grundable
code
has
to
be
clearly
distinguished
from
the
from
the
analyze
code,
so
there
seems
to
be
a
lot
of
stuff
there
that
could,
in
principle,
be
shared
because
there's
the
same
problem
all
the
time.
It's
you
really
just.
E
What
all
you
need
is
please
build
that
crates
tree,
build
all
the
proc
macros
and
build
scripts
like
usual,
build
all
the
actual
target
code
in
a
way
that
I
can
analyze
it
and
run
it
through
my
custom
driver
and
we
solved
this
problem
in
memory,
and
it
was
a
lot
of
work
and
and-
and
it
was
probably
partially
or
completely
served
in
a
couple
other
instances
as
well.
So
this
seems
to
be
something
that
we
should
probably
work
on.
Sharing.
A
A
A
E
A
E
G
Last
week,
trying
to
implement
intrinsics
and
in
c
code
that
I
can
compile
to
lvm,
because
I'm
doing
verification
using
llvm
based
tools-
and
I
do
not
want
to
implement
x86
intrinsic
side
or
if
I
do
I'd
like
to
help
other
people
so
that
we
get
them
all
done
without
me.
Having
to
do
every
single
one
of
them
and
making
buggy
implementations.
F
Actually,
even
in
cases
where
we
don't
directly
use
it
so
often
when
we
see
intrinsics,
we
can
you
know.
Cbmc
will
have
some
support
for
that
operation
already,
but
for
sanity
checking
it'd
be
nice
to
be
able
to
admit
to
actually
verify
that
the
result
of
our
lowering
to
cvmc
is
the
same
as
the
result
of
a
pure
mirror
implementation.
E
E
But
there
are
quite
a
few
well
most
entrants,
except
that
mary
implements
you
couldn't
express
them
in
mirror.
They
are
just
proper
language
extensions,
so
mary
has
a
reference
implementation,
but
that's
written
in
rust
code
that
directly
operates
on
the
merry
interpreter
state.
So
that's
not
really,
and
then,
of
course,
like
crucible
would
need
one
that
instead
is
written
in
haskell
and
implements
on
the
crucible,
abstract,
state
and
leggy.
It's
not
clear
that
there
is
a
format
here
that
could
be
actually
shared
other
than
writing
in
english.
G
Well,
the
the
long
long
tail
is
those
semdy
instructions
so
kind
of
having
those
taken
care
of,
and
then
it's
like
yeah
you're
gonna
have
to
do
something
special
with
something
that's
about
kind
of
like
into
processor
communication,
or
you
know
synchronization
or
something,
but
at
least
having
the
the
boring
ones,
which
really
don't
do
anything
interesting.
You
know
having
those
taken
care
of
would
be
worthwhile.
E
E
We've
gotten
away
with
that
in
mary.
I
don't
know
exactly
why
actually
like
somehow
we
are
avoiding
the
code
that
calls
intrinsics.
I
don't
know
if
people
add
cfg
memory
hacks
to
their
code
or
or
I
don't
know,
we
are
running
this
library
test
suite
which
uses
zindy
for
things
when
it
can
and
it's
not
running
into
that
code
in
memory.
So
somehow
I
mean,
then
it's
clearly
not
verifying
that
part
of
the
code,
but
at
least
it
can
verify
all
the
higher
levels
of
the
stack
without
worrying
about
the
zimbabwe
stuff.