►
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 HLF.
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.
We will show some preliminary results of our ongoing work to enable formal specification and verification of HLF chaincode.
The proposed methodology consists in using the tool Why3 [1] (and its underneath language WhyML, and third-party SMT solvers) to specify, implement and prove the chaincodes.
The tool Why3 then extracts an OCaml chaincode. Finally, we developped OCaml-chaincode-shim [2] to make OCaml chaincodes executable by an HLF peer.
We will demonstrate the application of this methodology on a no code development scenario of a workflow supervisor (that could be a critical component of an industrial supply chain traceability system).
This scenario starts with an abstract specification of the workflow in a graphical formalism (in the vein of [3]) and ends with a formally verified chaincode living in a HLF testnet.
[1] : Filliâtre, J. C., & Paskevich, A. (2013, March). Why3—where programs meet provers. In European symposium on programming (pp. 125-128). Springer, Berlin, Heidelberg.
[2] : https://github.com/hyperledger-labs/fabric-chaincode-ocaml
[3] : Bistarelli, S., Faloci, F., & Mori, P. (2021, November). *. chain: automatic coding of smart contracts and user interfaces for supply chains. In 2021 Third International Conference on Blockchain Computing and Applications (BCCA) (pp. 164-171). IEEE.
----
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
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
formal
method
at
the
level
of
this
code
chain
and
in
a
second
time.
I
will
give
you
an
overview
of
the
steps
that
make
up
our
proven
generation
of
chain
Cody
manager
manufactures
and
which
therefore
meets
our
needs
and
in
a
second
of
presentation.
A
C
A
B
Ok
and
so
first
a
little
little
context
on
our
work,.
Therefore,
the
Development
Research
division
of
DF
identified
the
need
to
be
able
to
administer
and
trace
the
evidence
of
industrial
operations
in
a
more
secure
and
more
transparent
manner
within
the
framework
of
the
nuclear
sector,
and
they
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
in
several
respects.
B
So
we
has
the
habit
of
classifying
the
criticality
of
a
system
in
case
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
stop
to
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
could
also
give
rise
to
a
leak
of
sensitive
information.
So
we
understand,
therefore,
it
is
necessary
to
provide
solid
guarantees.
B
As
for
the
proper
execution
of
this
system,
which
will
therefore
make
interact
the
operators,
as
well
as
the
subcontractors
of
these
industrial
operations,
but
also
the
regulators,
the
authorities
who
will
control
and
audit
the
evidence
data
by
monitoring
the
smooth
running
of
these
operations
so
know
that
the
idea
of
boosting
exchanges
in
the
nuclear
sector
and
therefore
of
approaching
greater
transparency
and
confidence
vis-à-vis
regulators
was
already
explored
by.
Therefore,
the
Finnish
and
Australian
operators.
B
Therefore,
through
the
papers
that
we
show
that
we
quote
pardons
and
therefore
in
our
system,
we
have
decided
to
use
the
blockchain
ipager
manufactures
in
order
to
allow
these
different
actors
to
be
able
to
interact
in
a
way
on
the
transparent,
by
using
a
chencode
to
encode
or
transcribe.
The
business
application
of
each
desired
industrial
operation.
B
B
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
a
question
of
an
industrial
operation
but
therefore
of
the
receipt
head
of
the
tiramisu,
a
little
simplified
and
represented
with
our
formalism
of
specifications.
B
And
here,
therefore,
we
seek
to
specify
the
order
which
must
be
respected
between
the
different
tasks
and
to
carry
out.
Therefore,
there
is
a
sometimes
strict
and
therefore
sequential
order,
but
also
looser
at
certain
at
certain
places
in
the
recipe
certain
times,
such
as
in
the
smallest
dotted
box,
where
you
want
to
perform
two
tasks
in
any
order,.
Also
note
that
each
action
performed
will
correspond
to
a
check
code
method
which
will
encode
so
this
procedure.
B
So
once
this
graphic
specification
has
been
made,
there
are
several
steps
that
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
average
implementation
so
which
is
the
language
dedicated
to
the
white
3
tool
that
we
use
ons,
and
this
therefore
white
3,
therefore
deductive
verification
tool
will
allow
us
to
prove
the
implementation
in
relation
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
so
express
at
the
level
of
require,
so
which
must
be
true
when
calling
this
function
and
a
pose
condition
which
defined
it.
How
the
result
is
so
the
what
must
be
true
when
exiting
this
function.
B
Once
this
presentation
is
finished
d
elsewhere,
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
experience
tool.
3
yourself
on
this
occasion
from
our
implementation
could
tool.
White
3
allows
you
to
extract
a
code
from
the
camel
correct
by
construction,
which
is
executable
for
it,.
B
So,
first
of
all,
there
is
the
call
for
publication,
which
is
carried
out.
Therefore,
by
the
journal,
a
submission,
the
submission
of
the
paper
by
the
scientist.
Then
there
is
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
for
forgiveness
to
republish
a
new
version
of
resubmit,
a
new
version
of
his
paper
and
therefore
in
scenario.
Both
the
following
two
reviews
are
correct:
accept
the
publication
who
she
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
So
we
then
come
to
the
generation
of
code
to
starting
from
the
constraints
expressed
in
this
graphic
specification
and
where
we
go
where
we
have,
where
we
produce
both
sorry,
the
logical
specification
and
the
implementation
in
the
Wemmel
language,
which
is
therefore
the
language
dedicated
to
white
3
tools.
And
we
can
thus
prove
the
implementation
compared
to
the
specification
in
an
automatic
way
using
to
prove,
therefore,
in
our
case,
AlterGo,
HVAC,
Cat
and
Z3,
and
therefore
what
requires
well,
obviously,
proof
engineering
and
a
certain
experience
of
the
tool.
B
However,
however,
it
is
not
so
easy
to
express
all
the
possible
properties
like
the
one
that
one
would
like,
for
example,
to
be
able
to
express
in
temporal
logic
and
therefore,
here
I
tell
you
speaks
to
you
of
a
property
that
we
want
that.
We
would
like
to
express-
because
we
may
wish
to
want
to
test
the
specification,
because
the
implementation
will
be
proven
against
this
specification,
but
the
specification
itself
may
be
subject
to
defects
in
design.
B
Therefore,
knowing
that
it
is
not,
it
is
not
a
question
of
the
skeleton
it
the
knowing
that
it
is
only
in
the
generated
code.
Therefore,
the
workflow,
that
of
the
skeleton
of
the
Genk
code,
therefore,
from
the
which
is
generated
at
From,
the
graphic
specifications
speciation,
it
is
quite
possible
to
also
add
functionalities.
B
From
Wemmel
a
camel
code,
and
therefore
in
the
Wii
email
code
we
have,
there
is
no
implementation
of
the
functionalities
which
are
present
in
the
shim
they
are.
We
must
therefore
make
a
code
with
holes
where
we
simply
declare
the
functions
so
that
we
will
tell
him
that
they
will
be
available
in
the
film
in
no
Mel,
and
we
will
therefore
be
able
to
do
a
mapping
during
this
extraction
step
here.
C
Thank
you
Julien,
so
the
chyme,
as
in
the
other
cases
for
the
other
languages
.
In
fact
it
is
placed
at
the
very
end
of
chain.
Then
at
the
very
top.
We
have
the
horror
order.
Like
that
usual
we
can
talk
about
kind
manufactures
and
he
will
choose
what
is
milk,
the
transactions
and
then
the
endorsers.
C
They
will
execute
them
and
for
that
hyper
manages
manufactures
to
choose
d
e,
put
the
checkots
in
docker
images,
which
makes
it
possible
to
use
many
different
languages
,
whether
on
the
left,
JavaScript
Java
and
therefore
what
had
already
been
presented
there,
the
last
ones
and
there
therefore
with
camel
it's
the
wants
to
do
a
bit
the
same
thing
and
in
fact
the
endorcer
communicates
with
the
fairly
classic
network
protocol
shim
the
patient
us,
as
in
the
case
of
askle.
For
the
moment,
we
are
doing
the
case
where
we
are
in
development
mode.
C
If
in
development
mode,
we
can
make
sure
when
we
to
iterate
a
little
faster,
make
sure
to
put
the
endorcer
in
development
mode
and
are
there,
the
Chimps
can
connect
directly
to
the
endorneur,
so
that
new
versions
can
be
quickly
created
of
a
Chen
code
and
immediately
executed
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'll
see,
but
it's
e
still
a
little
complicated.
C
So
the
shim,
in
fact,
is
based.
Communication
is
based
on
grpc,
which
is
a
fairly
common
friend,
and
therefore
it
is
a
we
used,
the
C
library,
which
is
also
used
by
others
in
other
languages
and
above
this
library
we
put
a
stop
at
the
camel
that
we
called
grpc,
which
makes
it
possible
to
link
to
the
functions
of
C
functionalities
and
in
fact
the
whole
protocol
is
described.
The
data,
the
format
of
the
protocol
exchange
data
are
defined
in
beef
proto,
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
which
is
called
factory
Chen
coaching
and
which
allows
to
describe
a
check
code
in
so
here.
It
is
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
question
where
we
will
be
able
to
recover
with
a
step,
get
the
value
in
the
Ledger
for
a
given
argument
of
the
value,
and
then
we
return
it
directly
because
it's
really
a
recovered
toy
example.
We
return
and
the
other
side.
We
have
another
method
which
allows
to
change
the
values,
so
that
is
directly
linked
to
the
head
boost
command.
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
could
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
level
1
vogue.
We
retrieve
the
function,
the
arguments
we
look
at
which
function.
C
C
That's
fast
to
also
do
Shen
code,
and
it's
true
that
it's
well
for
hyper.
The
players
make
very
practical.
They
made
sure
not
to
be
tied
to
a
single
training
language,
but
leave
it
the
second
freedom,
so
we
have,
there
are
a
lot
of
we
would
have.
This
work
could
not
have
been
possible
if
we
didn't
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
some
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
so
autof.
So
a
lot
of
things
are
implicit,
but
hey
just
read
another
China
to
have
the
answers
on
what
to
use
when
and
finally,
in
what
is
not
yet
implemented.
C
We
have
the
States
which
are
not
yet
implemented
for
a
little
more
complex
queries
on
the
keys,
and
we
also
have
parallelism
or
in
any
case
manage
several
requests
at
the
same
time,
which
are
not
completely
processed
yet
I
can
just
show
you
very
quickly
a
little.
The
execution
that
we
can
have
on
I
will
take
the.
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
fact
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
all
the
programs
that
we
need,
as
when
horror,
the
the
the
worst
then
to
launch
a
horror
order,
then
to
launch
a
worst
and
well.
There
are
a
few
times
between.
C
We
wait
for
each
application
to
finish
working,
so
it
takes
30
seconds,
but
if
I
jump
directly,
when
the
we
arrive
at
this
moment
there,
in
fact
there
we
arrive
in
a
tarp
like
that,
we
put
ourselves
where
we
already
have
all
the
commands
which
have
been
compiled,
which
are
accessible,
for
example,
there
at
the
worse
command
and
therefore
the
worse
command.
It
is
a
command
which
makes
it
possible
to
to
execute,
to
send
a
request,
a
transaction
to
create
a
transaction.
C
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
at
the
bottom,
for
the
'executes
and
there
when
we
executed
it,
the
transaction
was
received
by
the
shink
code,
the
transaction
id
number
that
was
quoting
and
it
was
executed.
We
returned
said
that
was
the
response.
It
was
90
and
in
indeed
we
have
on
the
left
well
90,
which
indeed
appears
very
simple
as
by
contract,
but
here
we
can
instead
modify
the
value
in
a
and
put
the
value.
C
B
And
therefore
presented
to
you
the
initially,
therefore,
the
stages
of
our
certified
generation
of
ginkod
hyper
manufactures,
therefore,
which
implements
procedures
but
but
in
our
use
case.
Therefore,
industrial
operations
within
the
framework
of
the
nuclear
firm
and
then
therefore
François
presented
you
with
a
chime,
therefore
implemented
in
any
Mel
and.
B
C
Any
and
so
right
after
I
will
just
present
a
little
tutorial
on
proving
this,
it's
Smart
contracts,.
It
looks
a
little
more
like
smart
contracts.
Solidity
en.
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
at
a
European
project,
made
to
help
start-up
companies
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
startups
can
ask
for
a
startup
vision
for
companies
influence
but
can
apply
for
funding.
C
So
there
are
multiple
times
in
over
the
course
of
the
project,
so
I
believe
it's
three
four
times
where
companies
can
come
up
with
a
project
say
what
would
they
like
to
use
and
to
that
time
they
can
receive
a
little
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
is
also
access
to
big
data
infrastructures,
the
Big
Data
fast
action,
so
in
any
case,
I
advise
you
to
go.
C
C
C
This
is
just
the
number
of
proof,
steps
that
the
prover
called
AlterGo
and
which
is
directly
initiated
also
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
module
theories
which
define
the
modeling
that
we
have
done
of
soliditine
by
ex
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
we
want
to
use,
and
in
fact
everything
above,
which
makes
it
in
fact,
leaving
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.
C
So
the
code,
we
could
say
that
it
seems
simple
to
write
to
us.
We
are
already
going
to
make
the
sender
remove
the
number
of
tokens
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.
It
can't
find
it
so
it
makes
big
mathematical
forms,
but
simply
by
keeping
in
the.
C
Interface
in
the
stocks
interface,
we
can
also
access
counter-examples.
We
don't
have
the
opportunity,
but
in
fact
here
it
tells
us
we
have
a
problem.
We
have
a
ban
overflow,
possibly
an
integration,
it's
not
sure,
but
he
tells
us
I
can't
prove
that
there
are.
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
has
a
semantics
in
solidity
or
it's
wrapant,
so
it
should
give
us
something.
C
C
We
say
to
ourselves,
but
we
say
that
it
is
an
error
to
pass
to
try
to
obtain
the
value
of
doing,
to
use
this
modulo
the
fact
that
it
will
really
be
and
therefore
there
what
it
is
necessary
to
do,
but
it
is
necessary
to
try
it
is
going
to
be
necessary
to
prevent
the
fact
of
making
this
calculation
when
we
are,
we
pass.
We
are
possible
to
pass
to
something
negative,
so
in
fact
we
put
back
the
same
thing
as
the
require
which
had
in
solidity
because
it
really
has
to
make
an
error.
C
A
C
C
It
is,
it
addresses
it
cancels
the
transaction,
but
that
we
wanted
to
make
it
quite
clear,
because
in
fact
we
don't
necessarily
know
there
can
be
a
very
low
call
that
will
cancel
the
execution,
and
so
what
we
wanted
to
do
was
reuse
the
exception
system
of
White
3
and
there
in
fact,
we're
really
going
to
write
it's
a
little
too
trendy,
we'll
see
in
another
case
where
this
redundancy
is
useful,
or
here
we're
going
to
say
that
require
fail.
A.
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
I
was
able
to
prove
that
here
there
is
no
integration
and
that
the
excess
and
the
requoyeur
does.
Who
is
there?
In
fact,
we
stop
the
transaction
only
in
this
case
that,
in
the
case
where
the
balance
is
more
strictly
than
the
requoyeur,
it
is
in
fact
the
opposite
since
there,
in
fact,
we
wanted
that
either
lower
and
the
balance.
C
So
there
we
have
the
negation.
Why
don't
we
still
manage
to
prove
the
last
case?
Which
is
this
one
and
in
fact
it
is
on
this
one?
We
often
think
about
it.
In
fact,
when
there
is
a
tutorial,
the
first
tutorial
of
ipadjo
factory
of
forgiveness
of
solidity,
there
are
several
versions,
because
people
have
corrected
small
problems
each
time
and
there
this
one
remained
for
quite
a
long
time,
because
in
fact
there
too
we
can
have.
It
is
if
the
balance
the
receiver
has
too
many
tokens.
C
What
I
had
put
before,
and
so
when
we
actually
launch
there,
it
tells
us
that
this
one
is
good,
but
this
one.
In
fact,
when
we've
done
the
calculation
he
says
well,
no,
there
is
the
same
overflow
possible.
So
we
must
not.
We
cannot
test
in
this
way
that
we
are
not
too
tall,
in
fact,
to
test
that
we
are
not
too
tall.
In
fact,
we
must
to
pass
on
the
other
side.
It
is
necessary
to
make
the
subtraction,
and
it
is
true
that
it
is
nevertheless
me
right
away.
C
C
In
fact,
if
we
can
see
that
in
what
I
recovered,
we
had
to
add
here
that
another
reason
for
which
we
could
stop
the
transaction
was
that
the
balance
plus
the
number
of
tokens
was
bigger
than
a
256
max
and
there
we
have
the
right
to
do
the
addition,
because
here
it's
calculations
that
are
mathematical.
It's
we
have
all
the
integers
of
bitrary
tailors,
whereas
here
we
had
the
right
that
to
integers
a
256,
and
so
that's
an
advantage.
C
It's
how
we
can
read
exactly
what
we
wanted
and
not
have
to
do
some
intellectual
gymnastics
so
that
the
to
put
the
tests
back
a
little
so
there
we
can
see
that
'it
is
nevertheless
the
interest
to
have
these
specs.
Also
at
this
place,
so
there
we
arrive
at
the
garlic.
We
were
able
to
prove
at
least
that
the
execution
and
was
going
correctly
or
with
and
that
we
have
no
integer
overflow
and
we
can
see
a
little.
What
are
the
cases
of
reset?
C
The
balance,
which
is
here
in
fact,
we
are
indeed
making
a
transfer,,
that
is
to
say
that
we
have
not
lost
any
tokens
where
we
did
not
recover.
We
did
not
create
tokens,
because
here
we
could
have
removed
this
line
there,
and
that
way
we
would
have
created
tokers
with
this
function,
and
it
is
something
that
we
do
not
have.
Obviously,
that
would
be
a
mistake.
C
Here,
in
fact,
we
had
an
initial
number
of
token
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
doing
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
an
initial
value,
for
example.
Finally,
for
the
values
that
exist
and
therefore,
if
we
take
and
if
we
says
that
we
always
have
zero
and
we
initialize
with
this
map,
which
always
has
the
value
of
0
everywhere.
At
that
moment,
we
did.
This
part
there
waking
up
and
just
by
doing
that,
in
fact,
there
it
tore
us.
C
C
Also
for
C
the
hada
in
this
case
we
start
from
C
from
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
White
3
site.
There
are
plenty
of
other
examples
with
plenty
of
others.
Different
algorithms,
and
here
is
the
power
of
the
tool.
A
It
is
true
that
suddenly
it
was
the
case
of
d'
a
solid
code,
because
your
familiarity
like
that,
but
it
would
work
a
bit
the
same
way
for
hyper
Ledger.
In
fact,
he
had
in
particular
to
implement
the
Shym
there
in
fact
specify
the
primitives
for
interaction
with
the
hyperager
blockchain,
what
the
famous
get
state
and
putstate
which
we
were
talking
about
earlier.
Moreover,
maybe
we
can
talk
about
it
a
little
bit.
It
was
a
little
bit
specific
to
hyper
Ledger,
which
we
had
talked
about
François.
Yes,.
C
C
C
At
that
time
makes
it
the
when
we
make
guestets,
if
we
made
a
whim
before
making
a
get
7.
In
fact,
we
don't
get
the
value
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
q
ue
it
is
something
that
is
not
necessarily
natural
and
in
our
modeling.
We
have
made
sure
that
when
we
go
to
a
get
step,
we
always
obtain
the
value
of
the
beginning.
A
C
It's
simply
because,
in
fact,
it's
the
number
of
stages
of
evidence
and
simply
there
is
certain
evidence.
I
look
at
the
last
evidence.
I
believe
there
is
need
a
little
more
proof,
steps
and,
in
fact,
the
tool
that
the
solver
tool
behind
AlterGo
actually
stops
after
100
proof
steps
and
goes
to
say.
Well,
sorry,
I
can't
prove
it,
but
in
fact,
when
we
tell
him
go
ahead,
you
have
900
more
steps
of
proof.
He
manages
to
prove
it.
He
has,
he
finds
the
he
can
prove
it.
C
A
C
Is
limited
when
you
walk
on
the
road
me
often
I
limit
myself
to
5
seconds
to
launch
for
each
prove.
So
often
the
things
are
not
proven
in
5
seconds
either.
We
can
help
them
with
additional
assertions,
so
it
is
in
fact
we
cut
the
proof
into
smaller
pieces,
or
sometimes
it
can
mean
that
it
is
not
provable
and
when
we
have
counter-
examples
that
could
tell
us
why.
C
Indeed
it
is
p
you're
likely
to
show
you
a
runtime
example
that
indeed
doesn't
verify
the
property
and
that's
where
sometimes
it
takes
a
bit
more
experience,
because
that's
when
there's
something
that's
not
proven.
Why
is
that
that
he
will
prove
to
know
which
invariant
to
add
it
is
that
it
still
requires
a
bit,
but
the
tools
also
with
abstract
interpretation,
which
began
to
be
available
in
white
3.
It
can
help
us
to
simplify
as
much
as
possible
to
the
lukewarm
that.