►
Description
Nous allons présenter des résultats préliminaires tirés de notre travail actuel portant sur la spécification et la vérification de chaincodes Hyperledger Fabric.
La méthodologie proposée consiste en l'utilisation de l'outil Why3 [1] (ainsi que de son langage dédié WhyML et de solveurs SMT tiers) afin de spécifier, implémenter et prouver des chaincodes.
L'outil Why3 permet ensuite d'extraire un chaincode dans le langage OCaml. Enfin, nous avons développé OCaml-chaincode-shim [2] pour rendre ces chaincodes OCaml exécutables sur un noeud HLF.
Nous démontrerons l'application de cette méthodologie sur un scénario de développement sans code d'un superviseur de workflow (qui pourrait être un composant critique au sein d'un système de tracabilité d'une chaîne logistique industrielle).
Ce scénario débute par la spécification abstraite du workflow à l'aide d'un formalisme graphique (comparable à [3]) et se termine par le déploiement d'un chaincode formellement vérifié sur un testnet HLF.
fabric-chaincode-ocaml: https://github.com/hyperledger-labs/fabric-chaincode-ocaml
----
Hyperledger – Open Source Blockchain Technologies
Hyperledger is an open source community focused on developing a suite of stable frameworks, tools and libraries for enterprise-grade blockchain deployments.
It serves as a neutral home for various distributed ledger frameworks including Hyperledger Besu, Fabric, Sawtooth, Indy, as well as tools like Hyperledger Avalon, Cactus and libraries like Hyperledger Aries, Ursa. Learn more about Hyperledger projects: https://www.hyperledger.org/use
Discord: https://discord.gg/rVCn4j7UFd
Case Studies: https://www.hyperledger.org/learn/case-studies
Training & Certification: https://www.hyperledger.org/learn/training
Tutorials: https://www.hyperledger.org/use/tutorials
Webinars: https://www.hyperledger.org/learn/webinars
Events: https://www.hyperledger.org/events
Vendor Directory: https://www.hyperledger.org/use/vendor-directory
Subscribe to the Hyperledger Newsletter: https://www.hyperledger.org/newsletter
Follow-us on Twitter @Hyperledger
Learn about Hyperledger Membership: https://www.hyperledger.org/about/join
#Hyperledger #Blockchain
License
Creative Commons Attribution license (reuse allowed)
A
A
B
So
first
of
all,
I
will
describe
the
framework
of
our
work
and
we
will
in
particular
talk
about
the
use
of
cincode
hipalager
manufactures
in
the
nuclear
sector,
as
well
as
the
application
of
a
formal
method
at
the
level
of
this
code
chain.
And,
secondly,
I
will
give
you
an
overview
of
the
steps
that
make
up
our
proven
generation
of
chencodile
manager
manufactures
and
which
therefore
meet
our
needs.
ns
and
in
a
second
part
of
the
presentation.
A
C
A
B
Ok
and
therefore
d,
first
a
little
bit
of
context
on
our
work,.
Therefore,
the
Development
Research
division
of
DF
to
identify
the
need
to
be
able
to
administer
and
trace
the
evidence
of
industrial
operations
in
a
more
secure
and
more
transparent
way
within
the
framework
of
the
nuclear
sector,
and
they
have
therefore
initiated
a
DLT
project,.
Therefore,
decentralized,
register
technology
to
control
and
monitor
the
smooth
running
of
these
industrial
procedures,,
which
therefore
makes
it
a
critical
system
for
many
In,
our
respects,
therefore,.
B
We
are
used
to
classifying
the
criticality
of
a
system
in
the
event
of
categories
and,
in
the
case
of
our
system,,
a
failure
or
an
erroneous
behavior
would
not
threaten
the
life
of
people
or
would
not
cause
a
sudden
stop
to
the
def
activities.
On
the
other
hand,
a
defection
of
the
system
could
harm
the
image
of
the
company
to
the
confidence
that
these
partners
and
its
customers
have
in
it,
and
it
could
also
give
rise
to
a
leak
of
sensitive
information.
B
So
we
understand,
therefore,
it
is
necessary
to
provide
solid
guarantees
as
to
the
proper
execution
of
this
system,,
which
will
therefore
make
the
operators
and
subcontractors
of
these
industrial
operations
interact,,
but
also
the
regulators,,
the
authorities
who
will
control
and
audit
the
evidence,.
Thus
monitoring
the
smooth
running
of
these
operations,
therefore,
know
that
the
idea
of
boosting
exchanges
in
the
nuclear
sector
and
therefore
of
approaching
more
transparency
and
confidence
vis-à-vis
regulators
has
already
been
explored
by.
Therefore,
the
Finnish
and
Australian
operators.
B
B
It
also
allows
the
confidentiality
of
smart
contracts
and
the
use
of
a
system,
so
brave
data
collection,
which
therefore
makes
it
possible
to
secure
the
data,
which
is
that
passes
through
Smart
contracts
and
that's
three
functions.
These
therefore
provide
fairly
substantial
guarantees
that
respond
to
the
critical
aspect
of
securing
the
data
that
we
need
and
with
regard
to
the
critical
aspect
of
the
proper
functioning
of
the
business
application
and
therefore
of
the
code
strings
that
we
want
to
develop
there.
B
B
B
Our
approach
resumes,
it
is
four
levels
of
formal
correction
and,
in
particular,
the
correct
generation,
from
a
graphic
specification
of
which
here
is
an
example.
Then
it
is
not
an
industrial
operation
e,
but
therefore
from
the
tiramisu
recipe,
a
little
simplified
and
represented
with
our
formalism
of
specifications,
and
here
we
are
therefore
trying
to
specify
the
order
which
must
be
respected
between
the
different
tasks
and
to
carry
out.
B
Therefore,
there
is
a
sometimes
strict
and
therefore
sequential
order,
but
also
looser
at
certain
places
in
the
recipe
at
certain
times,
such
as
in
the
smallest
dotted
box,
where
we
want
to
perform
two
tasks
in
any
order,.
Also
note
that
each
action
carried
out
will
correspond
to
a
method
check
code
which
will
therefore
encode
this
procedure.
B
So
once
this
graphic
specification
has
been
carried
out,
there
are
several
steps
which
are
necessary
before
obtaining
an
executable
and
exploitable
cheat
code
on
the
hyper
Ledger
blockchain
manufactures
and
in
our
system,
therefore,
of
industrial
consortium.
So
we
must
first
generate
a
logical
specification
and
an
implementation
on
average,
so
which
is
the
language
dedicated
to
the
tool,
w
hite
3
that
we
use
and
this
tool.
Therefore,
white
3,
therefore
of
deductive
verification
will
allow
us
to
prove
the
implementation
compared
to
the
generated
specification.
B
So
there
you
have
an
example
of
the
average
function
where
we
have
expressed
in
addition
to
the
function.
A
precondition,
therefore
express
at
the
level
of
require,
therefore,
which
must
be
true
when
calling
this
function
and
a
condition
which
defined
it.
How
the
result
is
therefore
the
what
must
be
true
at
the
exit
of
this
function.
B
Once
this
presentation
is
finished
by
the
way,
yes,
sorry,
you
will
have
the
opportunity
to
attend
a
tutorial
that
François
has
prepared
for
you,
and
you
will
also
be
able
to
experiment
tool.
3
yourself
on
this
occasion
from
our
implementation
could
tool.
White
3
makes
it
possible
to
extract
a
camel
code
correct
by
construction,
which
is
executable
for
it,.
B
So,
first
of
all,
we
have
the
call
for
publication,
which
is
carried
out.
Therefore,
by
the
journal,
a
submission,
the
submission
of
the
paper
by
the
scientist.
Then
we
has
a
first
review
which
is
carried
out
and
which
gives
its
agreement
for
the
publication,
but
in
this
case,
in
the
present
case,
another
review
which
is
carried
out
but
which
it
does
not
give
its
approval
and
therefore.
B
In
fact
asks
the
scientists
forgiveness
for
republishing
a
new
version
to
resubmit,
a
new
version
of
his
paper
and
therefore
in
scenario.
Both
the
following
two
reviews
are
correct:
accept
the
pu
blication,
which
it
is
therefore
carried
out
by
the
journal,
and
therefore
this
formalism
therefore
includes
a
notion
of
rendezvous.
Therefore
symbolized
by
the
plus
symbol
and
a
notion
of
interruption
symbolized
by.
Therefore
this
minus
symbol
and
knowing
that
the
transition
taken
by
the
review
action.
B
It
is
not
so
easy
to
express
all
the
possible
properties
such
as
the
one
that
one
would
like
to
be
able
to
express
in
temporal
logic,,
for
example,
and
so
here
I
am
talking
to
you
about
a
property
of
your
own
that
we
want.
We
would
like
to
express-
because
we
may
wish
to
want
to
test
the
specification,
because
the
implementation
will
be
proven
with
respect
to
this
specification,
but
the
specification
itself
can
be
subject
to
design
flaws.
B
B
B
C
Thank
you
Julien,
so
the
chyme,
as
in
the
other
cases
for
the
other
languages
.
In
fact
it
fits
all
at
the
end
of
the
chain.
So
at
the
very
top
we
have
the
horror
order.
Like
that
usual
we
were
already
losing
factory
and
he
will
choose
only
what
is
milk
the
transactions
and
then
the
endorsers
they
will
execute
them
and
for
that
hyper
manages.
Factory.
C
Ique
has
chosen
to
put
the
check
codes
in
docker
images
which
allows
the
use
of
many
different
languages
,
whether
on
the
left,
JavaScript
Java
and
therefore
what
had
already
been
presented
there,
the
last
and
there
so
with
the
camel
it's
the
wants
to
do
a
bit
the
same
thing
and
in
fact
the
the
sleeper
communicates
with
the
rather
classic
network
protocol
chyme
the
patient
us,
as
in
the
case
of
askle.
For
the
moment,
we
are
doing
the
case
where
we
is
in
development
mode.
C
If
in
development
mode,
we
can
make
sure
when
we
to
iterate
a
little
faster,
make
sure
to
put
the
ensorcer
in
development
mode
and
are
there,
the
Chimps
can
directly
connect
to
the
ensorcer
so
as
to
be
able
to
quickly
create
new
versions
of
a
Chen
code
and
immediately
execute
a
recompier
reexecute.
It's
not
the
endorser
that
generates
that
compiles
the
jenkod
in
the
core
image.
So
it's
something
we
would
like
to
do
in
the
future.
We
we'll
see,
but
it's
still
a
bit
complicated.
C
So
the
shim,
in
fact,
is
based.
Communication
is
based
on
grpc,
which
is
a
fairly
common
friend
and
therefore
it's
a
we
used
the
C
library,
which
is
also
used
by
the
others
in
other
languages.
and
above
this
library
we
put
a
stop
at
the
camel
that
we
called
grpc,
which
allows
to
link
to
the
functions
of
C
functionalities
and
in
fact
the
whole
protocol
is
described.
The
data,
the
format
of
the
data
d
protocol
exchanges
are
defined
in
proto
beef,
a
beef
post.
C
C
Protoba
manufactures
proto
and
directly
from
camel
protocoline
We
can
generate
the
protocol
in
ecamel
manufactures
protocol
and
with
this
one
and
on
the
other
side,
I
have
a
pc
protocol
plugin,
which
allows
to
link
that
to
the
protocol
to
the
real
execution
of
the
protocol.
But
we
can
no
longer
necessarily
write
a
library
called
factory
Chen
coaching
and
which
allows
to
describe
a
check
code
in
then.
Here
is
the
example
of
a
toy
of
a
hollowers.
C
So
at
the
start
we
say
to
open
the
library
manufactures
a
China
family
which
allows
access
to
the
functionalities.
We
have
a
part,
we
define
each
method.
So,
for
example,
here
we
have
a
query
where
we
are
going
to
be
able
to
retrieve
with
a
get
step
the
value
in
the
Ledger
for
a
given
argument
of
the
value,
and
then
we
return
it
directly
because
it
is
really
a
recovered
toy
example.
We
return
and
the
other
side.
C
And
finally,
we
have
the
last
part,
the
third
part.
It's
a
bit
of
a
code
that
we
can
from
the
boiler
plate.
We
can
recover
directly,
so
maybe
we
will
be
able
it
generate
it
or
automatically.
In
any
case
there
we
can
see
that
we
go
each
time
we
retrieve.
We
have
a
new
request
which
is
made,
so
it
is
the
1
which
is
at
the
level
of
1
vogue.
C
C
That's
fast
to
also
do
Shen
code
and
that's
true
that
it
is
good
for
hyper.
The
players
manufacture
very
practical.
They
have
made
sure
not
to
be
tied
to
a
single
training
language,
but
to
leave
it
the
second
freedom,
so
we
have
there
are
a
lot
of.
We
could
not
have
been
possible
if
we
hadn't
had
the
skelchim
which
had
been
defined
because
it
made
it
possible
to
have
a
slightly
simpler
diagram
and
which
made
it
possible
because
certain
parts
of
the
protocol
were
not
well
defined.
C
C
But
good
protoboeuf
does
not
describe
everything.
For
example,
there
is
in
some
cases
we
have
certain
data
for
which
we
have
different
types
of
messages
which
can
be
for
different
messages.
The
data
are
a
little
different,
those
which
are
accessible,
and
that
is
not
said
in
the
beef
post.
A
lot
of
things
are
implicit
but
good.
It
is
enough
to
read
another
China
to
have
the
answers
on
what
to
use
when
and
finally,
in
what
is
not
yet
implemented.
C
So,
in
fact,
it
was
just
to
show
an
example,
so
it's
true
that
it's
just
a
script,
but
it's
really
not
going
to
be
very
long,
but
in
done
we
have
a
first
script
and
that's
something
that
was
quite
practical
useful
to
do
for
afterwards,
which
allows
us
to
directly
download
the
code
from
the
page
to
the
factory
to
compile
all
the
programs.
We
need
like
during
horror
the
the
worst
then
to
launch
a
horror
order,
then
to
launch
a
worst
and
well.
There
is
a
bit
of
time
between.
C
So
there
we
are
going
to
create
the
transaction
query
a
to
ask
to
run
and
on
the
other
terminal,
which
is
on
the
right.
There
we
see
the
chencode
to
the
camel
that
we
are
asking
to
execute.
It
therefore
connects
there.
You
can
see
at
the
top
right
127
001
7502.
It
is
on
this
port
there,
which
is
the.
C
And
so
when
it
starts,
they
get
rich,
it
waits,
and
so
there
it
will
wait
until
we
have
made
the
request,
on
the
other
side
down
to
execute
it
and
there
when
we
executed
it.
The
transaction
was
received
by
the
shink
code,
the
transaction
id
number
which
quoted
x
id
and
it
was
executed.
We
sent
back
said.
That
was
the
response.
It
was
90
and
indeed
we
have
on
the
left
well
90,
which
indeed
appears
very
simple
as
by
contract,
but
here
we
can
modify
the
value
in
a
and
put
the
value
40
we
rerun.
C
C
B
And
therefore
presented
to
you
the
initially,
therefore,
the
stages
of
our
certified
generation
of
ginkod
hyper
Ledger
manufactures,
therefore,
which
implements
procedures
but
but
in
our
use
case.
Therefore,
industrial
operations
within
the
framework
of
the
nuclear
firm
and
then
François
has
therefore
presented
to
you
a
shim,
therefore
implementing
in
no
Mel
and.
B
C
Any
and
so
right
after
I
will
present
to
you,
so
it's
in
fact
just
a
little
tutorial
on
proving
this
is
Smart
contract.
That
looks
a
bit
more
like
smart
contracts.
Solidity
in
why
3,
but
it's
to
show
you
a
bit
how
you
can
use
white
3
and
in
fact
you
can
do
it
directly
in
your
browser.
So
that's
enough
here
is
nothing
to
install.
C
C
There
you
see
it's
a
so
one
on
a
web
page
there
of
the
reach
project
so
to
manage
in
a
European
project
made
for
help
r
companies
startups
to
be
able
to
use
tools
to
secure
and
have
more
confidence
in
data
in
services
that
offered
data.
So
it's
a
European
project
which
is
a
bit
special
because
it's
European
projects
where
there
are
a
startups
can
apply
for
a
vision
startup
for
companies
influence
but
can
apply
for
funding.
C
So
there
are
multiple
times
in
during
the
course
of
the
project,
so
I
believe
that
's
three
four
times
where
companies
can
propose
a
project
say
what
would
they
like
to
use?
And
at
that
time
they
can
receive
some
money
to
have
time
to
try
these
tools
and
also
to
be
able
to
discuss
with
the
people
who
make
the
tools
to
more
easily
use
them.
There
also
has
access
to
big
data
infrastructures,
the
Big
Data
fast
action,
so
in
any
case,
I
advise
you
to
go.
C
C
This
is
just
the
number,
no
proof
that
the
prover,
which
is
called
AlterGo
and
which
is
also
directly
initiated
in
Javascript,
all
that
in
fact
it
really
executes
in
your
bronzer
but
really
locally,
it's
all
in
Javascript
and
therefore
there
in
this
code
we
have
a
certain
number
of
mod
theories,
the
which
define
the
the
modeling
that
we
have
done
of
soliditine.
For
example,
there
we
have
the
wet
integers
256
of
solidity,
which
are
instants.
Here
we
have
the
addresses.
C
C
It's
just
that
it's
not
the
default,
the
mappings,
where
there
is
always
a
lot
of
mapping
in
solidity
for
often
from
address
to
values
,
but
it
can
be
many
other
things,
and
so
there
at
the
very
bottom.
We
really
have
the
code
of
the
one
we
want
to
use
and
in
fact
everything
above
that
actually
leaves
it.
25
lines
are
reusable
for
different
if
we
wanted
to
prove
different
Smart
contracts.
Indeed,
the
Smart
contracts,
it
is
not
written
in
solidity,
we
have.
What
we
can
do
is
the
extract.
C
So
the
code
could
be
said
to
seems
simple
to
write.
We
will
already
do
that.
The
sender
will
remove
the
number
of
tokens
from
it
and
the
receiver.
We
will
add
the
number
of
tokens
to
it
and
if
we
actually
launch
there,
it
tells
us
that
it
can't
prove
it.
That
n
can't
find
it
makes
big
maths,
but
simply
by
keeping
in
the
interface.
C
In
the
interface
of
the
stocks,
we
can
also
access
counter-examples.
We
do
not
have
the
opportunity,
but
in
fact
here
it
tells
us
we
have
a
problem.
We
have
a
ban
overflow,
possibly
a
inside.
It's
not
sure,
but
tells
us
I
can't
prove
that
there
is
one
we
can
look
and
there
we
see
that
we
are
done
when
we
subtract
num
token.
It
is
quite
possible
that
we
arrive
below
zero
so
as
it
is
256
factories.
In
fact,
there
is
a
semantics
in
solidity
or
it
is
wrapant,
so
it
should
give
us
something.
C
It
should
pass
a
very
large
value.
However,
we
preferred
to
choose
that
it
is
no.
We
wanted
a
semantics
a
little
stricter
than
that,
so
which
is
still
valid
with
the
way
in
which
it
is
executed.
We
say
to
ourselves,
but
we
say
that
it
is
an
error
to
pass
to
try
to
obtain
the
value
of
doing
d
'use
this
modulo
the
fact
that
it
will
be
really
and
therefore
there
what
to
do,
but
it
is
necessary
to
try.
C
We
will
have
to
prevent
the
fact
of
doing
this
calculation.
When
we
are,
we
pass,
it
is
possible
to
pass
to
something
negative.
So
in
fact
we
have
put
back
a
little
the
same
thing
as
the
require
which
had
in
solidity,
because
it
is
necessary
really
that
it
makes
an
error
finally,
but
a
horror,
a
little
which
is
directly
treated
so
there
we
could
say
note.
C
A
C
Here
and
so
there
he
says
this
expression,
it
returns
exceptions
which
are
not
recorded,
because
indeed
the
7th
exception
this
requoyeuse
function.
In
fact,
it
stops
the
flow
of
the
program.
It's
it
's
like
a
it
actually
resets
in
case
of
the
EVM,
is
that
it
addresses
that
cancels
the
transaction,
but
that
we
wanted
to
make
it
quite
clear
because
in
fact
we
do
not
necessarily
know
there
can
be
a
very
low
call
that
will
cancel
the
execution
and
therefore,
what
we
wanted
to
do.
C
C
In
any
case
there,
in
fact,
there
is
almost
exactly
what
I
had
been
able
to
write
before
and
there
when
we
launch,
we
see
that
it
tells
us
there
is
well.
There
was
j.
I
was
able
to
prove
that
here
there
is
no
integration
and
that
the
excess
and
the
requoyeur
makes
who
is
there.
In
fact,
we
stop
the
transaction
only
in
this
case
than
in
the
case
where
the
balance
is
more
strictly
that
the
requoyeur
is
in
fact
the
opposite
since
there,
in
fact,
we
wanted
it
to
be
inferior
and
the
balance.
C
So
there
we
have
the
negation.
Why
is
it
that
there
we
still
cannot
prove
the
last
case,
which
is
this
this
this
one
and
in
fact
it
's
this
one.
We
often
think
about
it.
In
fact,
when
there
is
a
tutorial,
the
first
solidity
forgiveness
tutorial.
There
are
several
or
more
versions,
because
people
have
corrected
each
time,
small
problems,
and
there
this
one
remained
for
quite
a
long
time,
because
in
fact
there
too
we
can
have.
It
is
if
the
balance
re
receiver
has
too
many
tokens.
C
What
I
had
put
before,
and
so
there
when
we
actually
launch
there,
it
tells
us
that
this
one
is
good,
but
this
one,
in
fact,
when
we
did
the
calculation
he
says
well,
no,
there
is
the
same
overflow
possible.
So
we
must
not.
We
can
not
test
in
this
way
that
we
are
not
too
big,
in
fact,
to
test
that
we
are
not
too
tall.
In
fact,
we
must
pass
it
from
a
On
the
other
hand.
You
have
to
do
the
subtraction,
and
it's
true
that
it's
all
the
same
right
away.
C
It
becomes
complicated
because
even
to
do
the
tests
to
test
that
you're
in
the
right
that
you're
doing
things
correctly,
you
have
to
be
careful
because
it's
also
quite
difficult,
but
that's
good.
Now
we
have
everything
that
has
been
tested.
In
fact,
if
we
can
see
that
in
what
I
recovered,
we
had
to
add
here.
Another
reason
why
we
could
stop
the
transaction.
It
was
that
the
balance
plus
the
number
of
tokens
was
greater
than
256
max
and
there
we
have
the
right
to
do
the
addition,
because
here
it
is
calculations
which
are
mathematical.
C
It
is,
we
have
all
of
the
double
tailor
integers,
whereas
here
we
were
only
allowed
one
256
integers,
and
so
that's
an
advantage.
It's
how
you
can
read
exactly
what
you
want
and
not
have
to
do
some
gymnastics
intellectual
so
that
the
to
postpone
the
tests
a
little
to
so
there.
We
can
see
that
it
is
all
the
same,
the
interest
of
having
these
specs
also
at
this
place.
C
C
The
the
balance
which
is
here,
in
fact
we
does
a
transfer,,
that
is
to
say
that
we
did
not
lose
tokens
or
we
did
not
recover.
We
did
not
create
tokens,
because
here
we
could
have
removed
this
line
there
and
like
that,
we
would
have
created
tokers
with
this
function
and
it
's
something
that
we
don't
necessarily
have,
which
would
be
a
mistake.
Finally,
it's
we
had
attacks
like
the
DAO,
where
it's
a
bit
like
that
or
suddenly
the
we
had
too
much
fine
money
money.
C
Here,
in
fact,
we
had
an
initial
number
of
tokens
and
what
we
ask
if
we
have
an
invariant
and
this
invariant
since
we
minimize
it
here
at
the
level
of
T,
it
is
a
Variant.
It
is
that
the
sum
of
the
balance,
the
sum
has
been
defined
not
necessarily
easily
we
can
do
it
once
must
always
be
equal
to
the
initial
value.
C
There
we
must
show
that
it
is
invariant
is
at
least
verified
by
one
by
one,
by
unit
by
a
value
initial,
for
example.
Finally,
for
the
values
that
exist
and
therefore,
if
we
take
and
if
we
say
that
we
always
have
zero
and
we
initialize
with
this
map,
which
always
has
which
is
worth
0
everywhere.
At
that
moment,
we
are
done
this
part
there,
wake
up
and
just
by
doing
that,
in
fact,.
It
tears
us
away.
C
C
In
for
C
the
hada,
in
this
case,
we
start
from
the
C
of
the
Ada,
and
we
generate
either
logical
formulas
or
code
like
that
yeah
3.
Here
the
example
is
more
an
example
for
smart
contra,
but
on
the
site
from
White
3.
There
are
plenty
of
other
examples
with
plenty
of
other
different
algorithms
and
that's
it.
The
power
of
the
tool.
A
It's
true
that
there
suddenly
it
was
the
case
of
a
solidity
code,
because
your
familiarity
like
that,
but
it
would
work
a
little
the
same
way
for
hyper
Ledger.
In
fact,
it
had
in
particular
for
implement
the
Shym
there
in
fact
specify
the
primitives
for
interaction
with
the
hyperager
blockchain,
what
the
famous
get
state
and
putstate
we
were
talking
about
earlier.
Moreover,
perhaps
we
can
talk
about
it
a
little
bit.
It
was
a
little
a
bit
specific
to
hyper
Ledger
that
we
talked
about
François.
Yes,.
C
C
C
At
that
time
makes
it
the
when
we
do
guestets,
if
we
have
done
a
whim
before
having
done
a
get
7.
In
fact,
we
do
not
obtain
the
value
that
we
have
in
the
whim.
That's
something
it's
probably
to
optimize
good,
it's
a
technical
choice
that
has
been
done,
but
this
is
where
the
proof
can
be
quite
interesting,
because
it
is
something
that
is
not
necessarily
natural
and
in
our
modeling.
We
have
made
sure
that
when
we
go
for
a
get
step,
we
always
obtain
the
value
from
the
beginning.
A
C
Fact
to
increase,
it
is
simply
because,
in
fact
it
is
the
number
of
stages
of
proof
and
simply
it
there
are
some
proofs
I'm
struggling.
The
last
proof.
I
think
there
needs
a
little
more
proof
steps
and,
in
fact,
the
tool
that
the
solver
tool
behind
AlterGo
actually
stops
at
the
end.
100
no
proof
go
and
say:
well,
sorry,
I
can't
prove
it.
But
in
fact,
when
we
tell
him
go
ahead,
you
have
900
no
more
proof.
He
manages
to
prove
it.
He
has,
he
finds
the
he
can
prove
it.
C
A
C
We
limit
when
we
step
on
it
me
often
I
limit
myself
to
5
seconds
to
launch
for
each
proof.
So
often
things
are
not
proven
in
5
seconds,
or
we
can
help
them
with
additional
assertions.
So
it's
in
fact
we
cut
the
proof
into
smallest
piece
is
sometimes
it
can
mean
that
it's
not
proven
ble
and
when
we
have
counter-examples
it
could
tell
us
why.
C
Indeed,
it
is
not
probable
to
show
you
an
example
of
execution
which
indeed
does
not
verify
the
property,
and
this
is
where
sometimes
it
requires
a
little
more
d
experience,
because
that's
when
there
is
something
that
is
not
proven.
Why
is
it
going
to
be
proven,
knowing
which
invariant
to
add
it
is
that
it
still
requires
a
bit,
but
the
tools
also
with
abstract
interpretation,
which
started
to
have
in
white
3?
It
can
help
us
simplify
as
much
as
possible
warm.