Open leonardoalt opened 4 years ago
I think for it to be useful though we'd need constexpr
as well
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?
We need to ensure that the conditions do not have side-effects.
Current proposal: Add a debug flag to not codegen assert/require. Return error if flag is active but assert/require has side-effects.
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.
I think C++-style static_assert
as a new feature makes sense, but as @christianparpart mentioned we need #3157 to be fully useful.
@dddejan people already actively remove assert
s 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.
@axic it can be done without #3157 if side effects are not allowed
This was discussed during the Solidity Summit and the following options were proposed:
// This does NOT become part of the bytecode, by default.
static_assert(f(x+2 == g(x-3)))
/// @assert f(x+2) == g(x-3)
@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.
And introduce a compiler flag, which includes them in the generated bytecode.
+1
I like option 3:
[[assert f(x+2 == g(x-3))]]
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
+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.".
As discussed during the Solidity summit, I like the general idea.
Some comments
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. 0xfe
is already used for /0, out-of-bound access etc, it would help dynamic tools to be able to focus on another opcode.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):
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.
Some notes from today's design call.
Rust has two kinds assertions:
We were trying to identify the use cases addressed by this topic:
Sentiment from the call:
static_assert
would be confusing if it is not compile-time evaluated. It should only be introduced for constant expressions.debug_assert
as well, which is not included in the code based on a compiler flag.function debug_assert(bool){assert(bool);}
. Just change the body be empty for the release build.
- 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.
I made a simple utility that aspires to be a temporary solution for this issue https://github.com/hacker-DOM/sol-env
require
andassert
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
andstatic_assert
could be logical only, without code generation. One variation would to also generate code if compiled in debug mode (or similar).