NatSpec for formal specifications

JoranHonig commented 3 years ago

Abstract

Diligence released Scribble (a specification language for Solidity smart contracts) around one month ago. In short; Scribble is a specification language and runtime verification tool. You can write Scribble annotations, and automatically test them with existing unit tests or automated testing tools. Finally, Scribble might see integrations with formal verifiers in the future. To write Scribble annotations, you currently need to prefix annotations with ///. Using NatSpec to standardise specification language annotations is an interesting option. The goal of this issue is to start a discussion around using NatSpec for formal specifications.

Motivation

As mentioned in the abstract above. Scribble currently requires you to write custom docstrings like:

///  <annotation>
function example() {}

/// if_succeeds {:msg "result is positive"} $result > 0;
function positive() returns (uint) {}

Unfortunately, this adds yet another code commenting and documentation standard. Alternatively, we might extend NatSpec, allowing users to write their specifications as NatSpec comments.

An example NatSpec + Scribble annotation.

// @spec if_succeeds {:msg "result is positive"} $result > 0;
function positive() returns (uint) {}

Additionally, formal specifications have a documenting function, which makes them an excellent addition to the documentation options already in NatSpec.

Discussion Points

How can NatSpec support multiple specification languages?

Some examples:

// @spec[scribble] if_succeeds {:msg "result is positive"} $result > 0;
function positive() returns (uint) {}
// @scribble if_succeeds {:msg "result is positive"} $result > 0;
function positive() returns (uint) {}

JoranHonig commented 3 years ago

👋 I hope this is the right place to start a discussion like this! If not, let me know where I should move!

leonardoalt commented 3 years ago

I like the idea. I also see that different tools will probably have different expressivity/operators/etc, so tagging which tool/language it's related to sounds like a good start. One other idea could be to try to have a common subset which can be represented by Solidity expressions, and those could be used to express pre/post conditions. This would not include a common desire that cannot be represented in Solidity, sum over mapping, for example.

summoning @hajduakos @dddejan who might be interested

JoranHonig commented 3 years ago

One other idea could be to try to have a common subset which can be represented by Solidity expressions, and those could be used to express pre/post conditions.

What would this look like? Something like the following?

// @spec-post a + b == result;

This would not include a common desire that cannot be represented in Solidity, sum over mapping, for example.

I think this is a really important point you're making. People will very likely want to use more than just this common subset, and start to use other languages in addition to the common one. I think you'd lose most benefits when proofs for specs in the common subset require annotations in other languages.

That said, providing a common language so people don't have to write specifications multiple times is definately something to think about. It's actually something we're hoping Scribble might provide. To achieve that we're planning to implement & support backends for commonly used verification tools.

@cd1m0 and @wuestholz are two of the masterminds behind Scribble & might have some useful input on this discussion too!

GNSPS commented 3 years ago

I think this is a very good topic for the next Solidity community call! 😊

dddejan commented 3 years ago

I agree with the general direction here. Unifying spec approaches would be a big positive for developers and would simplify development.

Some quick thoughts from me.

Most spec extensions can be framed in the form that @JoranHonig proposed, i.e.

/// @spec[tool] spec_type spec_message? spec_expression

The spec_type and spec_message can be fairly flexible. The most important thing would be the expression language. I think the minimal spec_expression needs to support is:

pure Solidity expressions (variables in scope, return variable, state variables, arithmetic, ...);
above includes function calls that can be inlined as expressions (getters, ...);
a way to introduce fresh variables;
tool-specific expressions of the form tool.f(x, y), where the extension functions would be typechecked flexibly.

Above would, I think, cover all the spec needs I've seen. If the compiler could check these for conformance, provide type-checking, and inline costexpr functions that would be amazing.

For example (random syntax):

/// @spec[tool] invariant "fixed supply" tool.sum(balances) == 100
/// @spec[tool] invariant "lucky" tool.exists{address a}(balances[a] == 42)
/// @spec invariant value() > 0
contract A {
   map(address=>uint) balances;
   int x;
   function value() public view returns (int) { return x + 52; } 
}

Note: An important thing that we're trying to figure out at the moment is what to do with specification under inheritance. At the moment Solidity inherits natspec tags under some conditions. For example, for overridden functions tags are inherited even if function variables and return value are renamed (I think).

hrkrshnn commented 3 years ago

Maybe relevant: https://github.com/ethereum/solidity/issues/8802

JoranHonig commented 3 years ago

@dddejan the specifcation types you name align with what we're thinking & building into Scribble 👍. (except for the tool-specific expressions, Scribble doesn't consider different backends yet)

Above would, I think, cover all the spec needs I've seen. If the compiler could check these for conformance, provide type-checking, and inline costexpr functions that would be amazing.

We are planning on building some specification re-use features like allowing people to define predicates. One possibility is to write these re-usable structures in separate libraries. I'm not sure that this should be part NatSpec (it's probably out of scope for NatSpec). I'm raising it here though because it would complicate having the compiler do type checking or other complex logic on specifications.

franzihei commented 3 years ago

Hello everybody! I just sent out an invite via email to hopefully all of you to discuss this topic on a call. The proposed time is this week Wednesday, 27th of January, 4:30PM CET (Berlin time).

The Google meet link is in the invite and I can additionally share it in this issue before the meeting if needed. :)

chriseth commented 3 years ago

I think type-checking the expressions from the compiler is an important feature, but I'm a bit worried about custom constructs like sums over mappings. Could it be a solution to require a free function (that is otherwise not used or would always panic when called) to exist that would match? Maybe not in general.... We would also have to define "before" and "after" variants of variables.

leonardoalt commented 3 years ago

Could it be a solution to require a free function (that is otherwise not used or would always panic when called) to exist that would match? Maybe not in general....

The problem is that that's just one function. Different tools will probably give different capabilities, so I think we shouldn't add sum of mappings as a common thing.

hajduakos commented 3 years ago

I also like the general direction, I think #5421 and #4991 are also related.

From our side (solc-verify) I agree with the points of @dddejan . I also agree with @chriseth that the hard part is having compiler support (e.g., parsing, type checking) for the tool specific extensions. Looking at tools like solc-verify, VeriSol, VerX, etc., there is definitely interest for such extensions. @leonardoalt also raised a good point that it's not just a single or a few functions, a general solution is needed.

In solc-verify, we currently add such extensions as magic functions, with special names (e.g., __verifier_sum). This is of course just a workaround until there is a better solution. On the downside, this requires modifications in the compiler (to add these variables) and with some low probability, these functions can be in conflict with existing functions. Also, we are having trouble with polymorphism: we cannot define a function with the same name for different types. For example, to express a "before" version of the variables, we wanted to define a function __verifier_old(...), but we had to define a separate one for different types (e.g., __verifier_old_address(...)).

An other approach (that for example VeriSol uses) is to define such extensions in an interface, which needs to be included. However, such approaches influence the actual code and also the compiled binary (unless the compiler knows about them and optimizes them away), which might not be desirable. In my opinion, the compiled binary should be exactly the same for a contract with/without specs.

Having some common format for specifications (with some compiler support) could resolve the above issues.

dddejan commented 3 years ago

I think type-checking the expressions from the compiler is an important feature, but I'm a bit worried about custom constructs like sums over mappings. Could it be a solution to require a free function (that is otherwise not used or would always panic when called) to exist that would match? Maybe not in general.... We would also have to define "before" and "after" variants of variables.

As @hajduakos mentioned, not having access to "flexible" typing brings unnecessary verbosity, and even makes some constructs impossible. Verbosity really kills a spec language, nobody likes to read/write specs that are longer than the code itself.

The sum is a good example even for basic cases. For a mapping, its return type depends on the value type of the mapping (uint8, uint256, ...). To support all these types we'd have to define free functions per type, with different names. The sum relatively simple in this regard because the number of return types is finite (numeric types).

The old function is even more interesting, because it applies to arbitrary types, and its return value is of that type. Therefore we cannot predefine these as free functions apart from the basic solidity types. This seems like a very hard problem, i.e., how to "typecheck" tool.old(balances)[msg.sender].

Another great example is the equality function. In specs, we often need to state that two data structures (struct, array, mapping, mapping of structs, ...) are equal by value (regardless of whether in memory or storage). In this case declaring the equality functions ahead of time is impossible because they depend on the user defined datatypes. Example: tool.eq(balances, tool.old(balances)).

I use "flexible" because I don't have a good proposal towards a solution. I am not a big fan of adding more complexity to the language so I really don't want to suggest anything resembling templates in the language (although it might be necessary).

chriseth commented 3 years ago

If everything is flexible, what kind of type checking do you expect the compiler to perform? Also, some notations use things like x'old and x'new, if we are flexible, we should probably also support things like that - I would prefer this because strictly, old and new should not actually have access to the name of its argument but only to its value.

dddejan commented 3 years ago

If everything is flexible, what kind of type checking do you expect the compiler to perform?

That's a good question. Our main goal by using the compiler for parsing the specs is to make sure that we have the expressions that correspond exactly to the semantics of Solidity that that version of the compiler is using. Having the compiler cover Solidiy expression (parse, resolve names and types) is already a huge benefit for us (we don't worry about name resolution, operator precedence, casting, ...). The typechecking that I imagined would treat all unspecified types as free and propagate accordingly. We are fine with this kind of imprecision because the tools can eventually close all the free types themselves.

For example, what I would have in mind for tool.old(balances)[msg.sender] > 0:

msg.sender is typed according to Solidity
balances is typed according to Solidity
tool.old is a spec function and can take any arguments (tool will check)
tool.old(balances) is undefined (tool will check)
tool.old(balances)[msg.sender] typechecks and resolves to an udefined type (tool will check)
tool.old(balances)[msg.sender] > 0 typechecks and resolve to bool type (tool will check)

It's a bit handwavy, I know, but that's my intuition. I am not a PL person so I don't know if something like this makes sense, or has been done before.

cd1m0 commented 3 years ago

Hi All. Great points about the tension between type-checking specs, and placing undue burden/complication on the compiler. What about the following 3 rough directions about how much the compiler type-checks:

Not at all. The compiler simply exposes specs in the AST, and its up to each individual tool to type-check its own specs. This way we don't unnecessarily burden the compiler, but the tools still get the benefit of parsing.
The compiler only type-checks SMTChecker compatible specs, and leaves the rest to the tools.
Each tool is required to provide an 'interface specification'. As people pointed out, the interface spec must support parametric polymorphism. So specs would be typechecked in an extension to Solidity - Solidity+Parametric Polymorphism+Bounded Quantification. So for example tool X can provide the following interface for the compiler to type-check its tool-specific functions:

tool.old <T> :: (T) => T
tool.sum <T extends numbers> :: (T[]) => T
tool.sum <K, V extends numbers> :: (mapping(K=>V)) => V

This would add a bunch of complication to the type-checking code, just to support specs. Also we would have to add some additional subtyping rules to make this useful (e.g. int8 <: int16 <:... int256 <: numbers).

JoranHonig commented 3 years ago

This discussion is growing more extensive than I initially expected 😄

There seem to be three topics:

Introduce a NatSpec tag so specifications can live as NatSpec docstrings
Offloading specification sanity checks (syntax & type) to the compiler
Developing a common language that multiple tools use as a backend

I think we've gone very deep into topic 2, but think that nr. 3 is potentially beneficial:

While developing a common language that can essentially be extended by different tools does bring its benefits:

Compiler can do certain checks (syntax, type)
Developers would only need to learn one language + the specific functions used by the tools that they want to use

We'd still be missing out on one of the most important benefits that a common language can bring. Namely that you only have to write specifications once, instead of for every tool out there. If developers need to write annotations specific to a tool (because they need to use constructs like tool.sum), they will still have to duplicate their effort for each tool they want to use. Furthermore, slight semantic divergences between tools can result in a lot of confusion. (Consider, for example, tools treating invariants as either strong or weak).

A single common specification language (without tool-specific constructs) would potentially have a much-improved developer experience. Different backends could interpret or translate these specifications so that developers can apply different verification technique. An example of a similar framework/ spec-language is ACSL and frama-c.

The problem is that that's just one function. Different tools will probably give different capabilities, so I think we shouldn't add sum of mappings as a common thing.

@leonardoalt does raise a good point here. We might take a similar approach to frama-c. As I understand it, frama-c backends selectively support language features. For example, I believe the runtime assertion checking backend doesn't support frame conditions. While this doesn't solve every problem, it moves the problem of figuring out semantic divergences between backends (or tools) away from the developer. Which I think is a positive aspect. You also get the benefit of a single common language:

Developers only need to learn one language
Everything can be type-checked/ consistency checked
You can re-use specifications between backends

leonardoalt commented 3 years ago

@JoranHonig while I agree with you, I'm not very optimistic that we can practically achieve that. IMO the common language would be pre/post conditions, old/new vars, inductive invariants, + whatever the compiler is able to type check.

Also summoning @MrChico @xwvvvvwx

leonardoalt commented 3 years ago

As an extension of my comment above, I would suggest that if a subset of tools has a common set of features/language that is not common to all tools they could agree on an extension, give it a name, and publish it somewhere. This somewhere could be a common place where all extensions are explained, for instance the natspec docs (just an idea). Users can apply that extension as @spec[sum] ... and know which tools would support that.

JoranHonig commented 3 years ago

@leonardoalt I was thinking something similar 😅, but you type quicker than me 😂

I was thinking it would also be possible to think about something like "dialects". These would specify common groups of specification language features (such as sum).

This would fit perfectly with the tool that we're working on right now (scribble). Which isn't meant to have just the one backend ( runtime assertion checking ). A way to think about Scribble could be as such a dialect.

hajduakos commented 3 years ago

@JoranHonig I agree that having a single specification language has many benefits, but it is really hard to draw the line. I believe that pure Solidity expressions are good for some toy examples, but anything practical actually requires more. As @leonardoalt mentioned, it would be nice to have pre/postconditions, old/new vars, sums, etc. Furthermore, if we want to leverage multiple backends for the same code, then it is not enough to standardize the specification expressions themselves, we also need to come up with a common subset of specification types. For example, the if_succeeds <expression> construct of Scribble seem to roughly correspond to the postcondition <expression> construct of solc-verify.

Dialects are a good idea, but considering these different kinds of specs, I'm a bit concerned that each tool will still need something really tool specific. So in the end, the number of dialects might end up being equivalent to the number of tools and developers cannot really benefit from multiple backends.

Nevertheless, some steps towards standardization or a common subset of specs would be great.

leonardoalt commented 3 years ago

@hajduakos I agree what each tool will probably need their own precise dialect, but I'd say there are still common subsets that many tools would agree with, and I think sum is a good example for that.

hajduakos commented 3 years ago

@leonardoalt I agree. I think for the expressions it should be more straightforward. I'm more concerned about the specification kinds. For example, Scribble has if_succeeds, ..., solc-verify has precondition, postcondition, invriant, ... In some cases this is just a matter of naming and they can be matched. But there might be some subtle differences.

JoranHonig commented 3 years ago

But there might be some subtle differences.

Right, that seems like one of the primary challenges in a universal/ common language.

My thinking was that there is nothing stopping multiple tools from adhering to the same common dialect. In such a scenario tool developers (for future tools) would be able to prevent those subtile differences, as they can decide to stick to the common interpretation.

There are caveats though; Sometimes a tool might want to intentionally divert from a particular dialect. Sometimes a tool might want additional language features not present in a dialect. ...

dddejan commented 3 years ago

I think it might be wise to put aside advanced features and dialects for the moment (even the sum) and focus on the core expression language.

The main obstacle to specification and verification doesn't seem to be what we can verify, but rather the lack of users that are willing to write specs for the contracts. The benefit of having even a core set of specification expressions supported by the compiler would be tremendous in this regard. If the users could be exposed to specification elements in Solidity docs, complemented with IDE support for writing specs (through direct compiler support), the spec-writing community would grow and give a much larger boost for developing the general spec approach. I live to see the day when people upload a contract with a standard spec to Etherscan.

We basically all agree on the core language: contract and loop invariants, some kind of pre- and post-condititions, and some way to reference old values (old).

A good guiding principle for the core language might be to only include things that could potentially be "executed" by the compiler: turned into require/assert statements. For example, only allowing old on primitive types so that one could remember the value in a ghost variable. With sufficient work this could also be done for sum but wold take much more work so I would skip it for now. By framing it this way semantics are clear and there is no need to discuss tool differences (which btw I think don't really exist).

I would leave it to compiler developers to come up with the actual syntax, verification people can adopt their tools. Anything past that is getting researchy and is bound to take a while.

franzihei commented 3 years ago

Just dropping the meeting link here as well for out meeting in 5 mins! --> https://meet.google.com/oye-bduq-nkc

GNSPS commented 3 years ago

I'm running ~5 mins late! But Joran and Valentin will be there from the start! 😊 🙏

On Wed, Jan 27, 2021 at 15:25:35, Franziska Heintel < notifications@github.com > wrote:

Just dropping the meeting link here as well for out meeting in 5 mins! --> https:/ / meet. google. com/ oye-bduq-nkc ( https://meet.google.com/oye-bduq-nkc )

— You are receiving this because you commented. Reply to this email directly, view it on GitHub ( https://github.com/ethereum/solidity/issues/10825#issuecomment-768361674 ) , or unsubscribe ( https://github.com/notifications/unsubscribe-auth/AA6SSFO6T6RMKSK4PEDSUKDS4AV67ANCNFSM4WKPMRTA ).

axic commented 3 years ago

While not strictly related, the discussion in #8146 also touched upon syntax for invariants. So did #8433. (Seems like we have at least four issues discussing it.)

leonardoalt commented 3 years ago

Completely agree with @dddejan

axic commented 3 years ago

Based on today's call, it seems that the benefit of having a natspec tag is the visibility to users, and it is parsed and exposed by the compiler. These tags are however only exposed separately to the AST.

It appears it would be useful to a) extend the natspec output or have a separate output which links it to AST ids b) include all comments (and potentially parsed natspec additionally?) in the AST output

As mentioned earlier we are talking about various distinct features here:

Have very apparent place in the source for users to write specs in
Have the compiler do the parsing for tools
Have the compiler validate (some of) the contents of the specs
Have a common specification language

I think:

1 and 2 is achieved by having a natspec tag and exposing it nicely in the AST.
3 seems to be depending on 4), otherwise it will become very messy. Parsing expressions could be achieved via #1272.
4 seems to be a long term goal.

leonardoalt commented 3 years ago

Decision on call (which included most people in this issue): We'll use natspec and start with the very minimal, that is @spec, dialect, property. The syntax is yet to be defined, but suggestions were:

// @spec[dialect] property
// @spec dialect property
other ideas?

Thanks for the call everyone!

axic commented 3 years ago

I actually think @spec[dialect] stands out much better, but not sure about its compatibility within the wider natspec ecosystem.

axic commented 3 years ago

Furthermore some concerns were expressed regarding natspec tags:

@chriseth mentioned having custom tags (#8802) has the risk that people could prefix general tags by mistake, and nothing would pick it up. I imagine external tools (such as linters) could be extended to deal with it.
once we have the generic @spec tag, which is type-checked by the compiler, it must follow the same versioning regime as the compiler itself. It seems arriving at such a common subset will take quite a bit.
the @spec[dialect] or @spec dialect might be too verbose. In my opinion this actually could be beneficial by encouraging a quicker adoption of the common subset so that users can go with @spec. Or potentially we could see specific tags like @invariant.

franzihei commented 3 years ago

Long form, hacky notes of today's meeting can be found here. Thanks everybody for joining!

dddejan commented 3 years ago

@chriseth mentioned having custom tags (#8802) has the risk that people could prefix general tags by mistake, and nothing would pick it up. I imagine external tools (such as linters) could be extended to deal with it.

This is an extremely important issue! I have "proved" things several times with our tool by mistyping the spec tags only to find out later that it is all broken.

axic commented 3 years ago

Considering the current sentiment for @custom:<tag> in #8802, should we consider to use @spec:<dialect> here?

Or would that mean tools would be happy to go with @custom:<freetext> for the experimentation phase and revisit the @spec option when there is a baseline spec language agreed?

If the preference is to have @spec <dialect> <freetext>, does that mean the compiler has to verify this format, i.e. the dialect is an alphanumeric string without whitespace, and there is some actual content in the spec tag after it? Would that also mean non-dialect specs are not supported in this format?

cd1m0 commented 3 years ago

I am ok with @spec:<dialect>. Its nice to have uniformity in syntax.

Question: Can the <freetext> have line breaks in it?

In audits we often found predicates grew quite large, so we allowed line breaks in the Scribble syntax to make them readable. We denote the end of a Scribble annotation with ;.

chriseth commented 3 years ago

Line breaks should be OK, I think they are contracted to regular whitespace.

axic commented 3 years ago

As a heads up, in 0.8.2 we introduced the @custom:<name> tag and the AST output contains the natspec tags in the documentation field. It can be used to experiment with the dialect proposed in this issue. Please let us know how you get along using this feature, so we can come up with a spec language and perhaps introduce a specific tag for it later.

github-actions[bot] commented 1 year ago

This issue has been marked as stale due to inactivity for the last 90 days. It will be automatically closed in 7 days.

github-actions[bot] commented 1 year ago

Hi everyone! This issue has been automatically closed due to inactivity. If you think this issue is still relevant in the latest Solidity version and you have something to contribute, feel free to reopen. However, unless the issue is a concrete proposal that can be implemented, we recommend starting a language discussion on the forum instead.

ethereum / solidity