Open El-Ku opened 1 year ago
fubuloubu
commented
1 year ago We have the UNREACHABLE modifier for assert and revert statements, which injects the 0xFE opcode used by many FV tooling such as Symbolic Execution engines to detect invariant violations. It's a good safety measure, because even though you expect it never to be hit, if it does happen to be hit it will invoke a transaction abort
charles-cooper
commented
8 months ago i'm generally a fan of this proposal. the compiler would insert calls to __invariant__() at the exit of every mutable external function call (which is tedious and somewhat difficult to do by hand in the general case).
charles-cooper
commented
8 months ago tentatively approving this proposal, will look to add it in 0.4.1 or 0.4.2
Simple Summary
Introduce a special function for protocol level invariants. This function could be called automatically at the end of every function which makes external calls.
Motivation
The world of smart contracts is too complicated that its too scary to just rely on few audits and
battle-tested in timeclaims to trust a protocol. The users need something more tangible to give them the assurance that, no matter what kind of sorcery the blackhat will do, there are a few things he will be unable to achieve (readinvariants).Specification
The special function could be called
__invariants__for example.If the dev doesnt specify an invariant function it would be defaulted to this:
One point to be noted is that, it would be more useful if this function is used to specify more general invariants. When we focus to mitigate specific scenarios alone, there is a possibility for someone who could just think
outside the boxto come up with a different idea to rekt the protocol.This feature could be used to automatically pause the contract in case of an attack, which will give enough time for whitehats to mitigate the issue and rescue the funds.
Backwards Compatibility
n/a
Dependencies
n/a
References
n/a
Copyright
Copyright and related rights waived via CC0