act
act copied to clipboard
ethereum
Smart contract specification language
Features and bug fixes: - Adds support for environment values in the Coq backend (only CALLER atm) - Adds support for multiple updates to state variables - Bug fix in...
Act specs allow us to define various branching behaviours with the use of the `case` syntax. In order for properties proved against a spec involving cases to be sound, we...
The following spec errors out with: ``` *** Exception: Internal error: Type.typedExp. Expr: EPreEntry (AlexPn 246 15 11) "x" [] CallStack (from HasCallStack): error, called at Type.hs:311:29 in act-0.1.0.0-inplace-act-internal:Type ```...
The following currently typechecks: ``` constructor of C interface constructor(uint24 _x) creates uint24 x := _x behaviour increase of C interface increase(uint24 new_x) storage x => new_x behaviour increase of...
Currently rewrites and implication use the same syntax, which is a little confusing. It would be nice to change the rewrite arrow to `
Understanding the impact of rounding error in a smart contract is a critical task for secure development. There are two properties of interest: 1. The direction of the rounding error...
When I try to prove the following spec: ``` constructor of Simple interface constructor() creates mapping (uint=>uint) store := [] behaviour set of Simple interface set(uint x, uint y) storage...
If I attempt to prove the following spec: ``` constructor of Auth interface constructor() creates mapping (address => bool) wards := [] behaviour rely of Auth interface rely(address usr) iff...
[cff](https://github.com/defi-formal/cff) ([paper](https://eprint.iacr.org/2021/1147)), is a framework and toolchain that allows for the formal analysis of economic properties. It appears to be a remakrably powerful tool, quoting from the abstract: "it can...