static_assert and static_require

[leonardoalt]

require and assert can be used to write formal specs into Solidity, but many people don't because they automatically lead to extra bytecode increasing gas costs.
static_require and static_assert could be logical only, without code generation.
One variation would to also generate code if compiled in debug mode (or similar).

[leonardoalt]

I think for it to be useful though we'd need constexpr as well

[christianparpart]

I think for it to be useful though we'd need constexpr as well

I'd not make it another syntax element but a compiler flag to not codegen on assert/require. This way in constexpr context (future) we could still use assert/require. What do you think?

[chriseth]

We need to ensure that the conditions do not have side-effects.

[leonardoalt]

Current proposal:
Add a debug flag to not codegen assert/require.
Return error if flag is active but assert/require has side-effects.

[dddejan]

Not generating code is scary.

We do this all the time in C and works as follows: add asserts, compile release without asserts, release to customer, wait, customer reports segfault, debug with assertions, fix code, repeat. I feel that this doesn't really fit on blockchain unless you trust formal methods 💯% (which I don't).

The danger is that if you allow people to save gas with a flag, they probably will. Also, doesn't require need to generate anyhow because it's used for argument checking.

[axic]

I think C++-style static_assert as a new feature makes sense, but as @christianparpart mentioned we need #3157 to be fully useful.

[leonardoalt]

@dddejan people already actively remove asserts from their code to save gas, so I don't think the flag would make it more dangerous there, and I agree with the workflow you described.

[leonardoalt]

@axic it can be done without #3157 if side effects are not allowed

[axic]

This was discussed during the Solidity Summit and the following options were proposed:

1. static_assert

// This does NOT become part of the bytecode, by default.
static_assert(f(x+2 == g(x-3)))

2. special comments with proper Solidity expressions

/// @assert f(x+2) == g(x-3)

3. non-comment annotations

@assert(f(x+2 == g(x-3)))
[[assert f(x+2 == g(x-3))]]

And introduce a compiler flag, which includes them in the generated bytecode.

Thanks for @hajduakos and @montyly for feedback.

[muellerberndt]

And introduce a compiler flag, which includes them in the generated bytecode.

+1

[leonardoalt]

I like option 3:
[[assert f(x+2 == g(x-3))]]

[leonardoalt]

Regardless of which option, I think the main question left is:
Compiler flag for bytecode generation or not?
In case no, how would tools that target bytecode know about those properties?

I am personally in favor of compiler flag

[hajduakos]

+1 for option 3, that could also be generalized to further specs. For example

[[invariant x == y]]
contract C {
  int x; int y;
  // ...
}

(or @invariant(x == y)).

This approach can also have better flexibility if verifiers want to have tool specific extensions. For example they could define custom annotations (or functions to be used in annotations). Similarly as Java or C# allows custom annotations/attributes. E.g., the former example could be expressed with some syntax saying "I want to define an annotation with name invariant that can be attached to nodes of type contract and would have an expression as argument.".

[montyly]

As discussed during the Solidity summit, I like the general idea.

Some comments

• If we add invariants at the contract/function level, we should define what it means; Is it going to be always-true invariant or invariant that must hold at the beginning/end of transactions, or something else? I think @leonardoalt mentioned that invariants would hold at the beginning/end of transactions during the summit.
• We should be careful with the wording and documentation on this feature. I like assert, but as assert() is already used by developers to do input filtering, we must be careful that no one will use it thinking that code will be generated. I think this is particularly true for static_assert, the options 2 and 3 are likely to be less confusing, but it's probably worth asking more people about it.
• I definitely think the compiler should be able to generate bytecode with an extra flag. Ideally, the compiler could take an optional flag to define the opcode used to trigger the invalid states. As 0xfe is already used for /0, out-of-bound access etc, it would help dynamic tools to be able to focus on another opcode.

[wuestholz]

I also like option 3.

About contract invariants: I think it's worth thinking carefully about where the checks should happen. In the literature on class/object invariants there are many different methodologies for checking invariants and not all of them are sound or easy to check at runtime. At MythX/Diligence, we are currently experimenting with an option that should be sound and quite easy to check at runtime (@cd1m0):

• Check at the end of the constructor.
• Check before external calls. (Shouldn't lead to many "false positives", since external calls should happen after state changes anyways to avoid reentrancy issues.)
• Check at the end of public/external functions.

All these check use assert-statements and no require-statements are used; when performing modular checking, one might want to assume/require the invariant at the beginning of functions to simplify the reasoning, but I think this should be optional.

Currently, we also disallow invariants that refer to the state of other contracts (that is, multi-contract invariants) since they are notoriously hard to check soundly and efficiently at runtime.

As mentioned earlier, we use regular assert for these check, but we also emit a special event (see https://medium.com/consensys-diligence/checking-custom-correctness-properties-of-smart-contracts-using-mythx-25cbac5d7852 for more details) to distinguish them from implicit assertions that are emitted by the compiler. I also like the option of using a separate opcode as suggested by @montyly.

[axic]

Some notes from today's design call.

Rust has two kinds assertions:

• assert!
• debug_assert!

We were trying to identify the use cases addressed by this topic:

1. People add many assertions to code during development, but remove many of them at deploy time to save gas.
2. Analysis tools could benefit from detecting these assertions.

Sentiment from the call:

1. Having a compiler flag to remove all asserts is a bad idea. There needs to be a way to select which ones to keep.
2. Introducing static_assert would be confusing if it is not compile-time evaluated. It should only be introduced for constant expressions.
3. Could follow Rust and have a debug_assert as well, which is not included in the code based on a compiler flag.
4. Could also implement this as a user defined function: function debug_assert(bool){assert(bool);}. Just change the body be empty for the release build.

[moodysalem]

• Having a compiler flag to remove all asserts is a bad idea. There needs to be a way to select which ones to keep.

Why though? The user chooses to turn that flag on. And anything that is expected to happen at runtime should be a require.

[hacker-DOM]

I made a simple utility that aspires to be a temporary solution for this issue https://github.com/hacker-DOM/sol-env