Move specifications

Hello!

I’ve seen that recently Move got bunch of specification options. And I am wondering why and what for. From what I’ve understood spec{} blocks are not present in compiler’s byte code and are only used in move-prover.

Why do you need them? Is there a chance we’ll be able to use specifications to create function restrictions? Or are they some kind of tests for move modules? Is it possible that specifications will be used somewhere outside move-prover? Finally, what is their use case?

Also (since I’m working on Move’s syntax highlighting) has the decision on spec syntax been made? Is it possible that you’ll redesign it?

2 Likes

Specifications are logical properties that resources, modules, and functions are supposed to have. They NEVER affect the execution of programs. The Move Prover checks whether those properties are satisfied by the code in the Move modules.

The Move Prover is in a preliminary state and under very active development. I.e., anything can change, including the spec syntax, and a lot is going to. The prover is not fully functional, yet. The code, and test cases that show examples, is in github in language/libra/move-prover.

I don’t know how your syntax highlighter works, but, if possible, doing something extremely basic for spec blocks, so you don’t end up throwing away a lot of code, would be a good idea.

2 Likes

To add a bit more detail, the Move Prover extracts these specifications from the source code, but the proof is actually done on the generated bytecode. That has the advantage that we don’t have to trust the correctness of code generation. The bytecode is also less complex than the source language and (lately) hasn’t been changing as quickly, so it’s better from a software engineering perspective as well.

4 Likes

Just to add to what @dill has already said. I would assume that any syntax in the Move source language could change. In the next few months, that will go down will there probably only make smaller tweaks. But as far as the syntax for spec blocks, almost all of that syntax is temporary. We implemented it as a stopgap solution to push the Move Prover implementation forward. That syntax will likely be reworked fully sometime this year.

3 Likes

Are you going to use move-prover for checking newly-published modules? Or is it going to be local tool? Though it makes no sense if one can avoid move prover locally and publish compiled move source without specifications.

1 Like

I’ll try to follow these changes in my Move IDE. Currently Move feels like the best language for smart contracts development. I hope you use my extension! :laughing:

2 Likes

The Move prover is a tool for helping developers ensure the correctness of their own modules. Specs are not published on-chain, and the prover does not run on-chain (similar to module tests and the Move compiler). The Move whitepaper explains the reasoning behind this in a bit more detail in Section 3.4.

However, we plan to use the Move prover to gain confidence in the safety of all the Libra core modules and encourage the Move community to be the same. As the whitepaper explains:

Our longer-term goal is to promote a culture of correctness in which users will look to the formal
specification of a module to understand its functionality. Ideally, no Move programmer will be willing to interact with a module unless it has a comprehensive formal specification and has been verified to meet to that specification. However, achieving this goal will present several technical and social challenges. Verification tools should be precise and intuitive. Specifications must be modular and reusable, yet readable enough to serve as useful documentation of the module’s behavior.

2 Likes

I think I got the idea. Thanks for answer and for linking Whitepaper - I almost forgot about it.

1 Like

There are some imperative specs exist so it implies at least something like classical automated module testing which can be done (describing boundary conditions as specs) without Monte Carlo method. So this Boogie-style approach statically covers only bugs and boundaries which developer is aware for. Thus specs cannot mitigate whole classes of bugs “between the boundaries”. Especially malicious behavior of developer itself.
Am I right?

1 Like

Specifications in Move are not used for testing. Instead they are used for formal verification. One can think of formal verification as executing the Move program for all possible inputs (not just boundary values), and validating whether the conditions specified hold for all those inputs. Technically, this is done using some form of symbolic execution.

However, your observation is right that things which aren’t specified will also not be checked for. On the other hand, one can have rather simple yet powerful specifications. For example, the condition aborts_if false would state that under now circumstances and for all possible inputs, a function must not abort (no division by zero, no access to non-existing resources, etc.). The Move Prover can verify that this is in fact the case, and shows you the program points where it may abort if not.

6 Likes

Thank you for your email
As a libra developer, and with little knowledge of coding. I am confused with all the mail I’m receiving implying codes. With my different project I have in my country or the global economy I need some ideas related to the development of the different projects.

I wish to know what I can expect from the programmers in the community and will that be sufficient for the immediate.

Furthermore will I need to recrute programmers locally and create a team in order to develop the libra projects.

I have created a group on my FB page which numbers 250 persons worldwide awaiting libra launch.

I think that my query is becoming more and more pressant with the evolution of libra and the task need more and more personnel with diverse knowhow.

Thank you for your support,

Mardoche (Harold Marie)

:mauritius: Libra Mauritius.

1 Like

@dill hope it’s not too late! I’ve added spec syntax support to Move IDE! It was hard to separate scope blocks from other scopes so I ended up rewriting syntax to scope-based.

https://marketplace.visualstudio.com/items/damirka.move-ide/changelog

perfect post thank for sharing sirji