static_assert

[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.