diff --git a/.github/workflows/deploy-book.yaml b/.github/workflows/deploy-book.yaml index fd257b366..c940ef53e 100644 --- a/.github/workflows/deploy-book.yaml +++ b/.github/workflows/deploy-book.yaml @@ -1,8 +1,6 @@ name: Deploy Book on: - push: - branches: - - master + workflow_dispatch: # Enables manual triggering from GitHub UI only jobs: build-and-deploy: runs-on: ubuntu-latest diff --git a/doc/src/aliasing.md b/doc/src/aliasing.md index f318890a4..9a2c59455 100644 --- a/doc/src/aliasing.md +++ b/doc/src/aliasing.md @@ -10,10 +10,10 @@ contract A creates Token t0 := a0 Token t1 := a1 - transition transfer (uint256 value, address to) + transition transfer (uint256 _value, address to) updates - t0.balanceOf := t0.balanceOf[CALLER => t0.balanceOf[CALLER] - value] - t1.balanceOf := t1.balanceOf[to => t1.balanceOf[to] + value] + t0.balanceOf := t0.balanceOf[CALLER => t0.balanceOf[CALLER] - _value] + t1.balanceOf := t1.balanceOf[to => t1.balanceOf[to] + _value] ``` diff --git a/doc/src/constructors.md b/doc/src/constructors.md index 171d8c216..fcad46d49 100644 --- a/doc/src/constructors.md +++ b/doc/src/constructors.md @@ -46,7 +46,7 @@ The general shape of a constructor in act is: 2. **Precondition Block**: `iff ` - Specifies the necessary and sufficient condition for successful constructor execution. - - Must be present (use `iff true` if there are no preconditions). + - Can be omitted if there are no preconditions. 3. **Cases Block** (optional): - If present, there are multiple `case : creates ...` branches whose conditions are mutually exclusive and exhaustive. @@ -76,8 +76,6 @@ In the ERC20 example, the constructor is non-payable. Thus, it does not include ```act constructor(uint256 _totalSupply) -iff true - creates uint256 totalSupply := _totalSupply @@ -90,8 +88,6 @@ An artificial example of a *payable* constructor would be: ```act constructor () payable -iff true - case CALLVALUE > 0 : creates bool myFlag := true @@ -152,7 +148,7 @@ def __init__(t0: address, t1: address): ``` -As mentioned before, the `iff` block cannot be skipped even if the condition is trivial, in which case the user should write `iff true` as shown in the ERC20 example. +As mentioned before, the `iff` block can be skipped if the condition is trivial (i.e. `iff true`), as shown in the ERC20 example. ### `inRange` in Preconditions Whenever arithmetic operations are involved in the storage initialization, it is necessary to ensure that these operations do not overflow or underflow. This is done using the `inRange` expression ([Base Expressions](./store_type.md#base-expressions)), which checks whether a value fits within a specified type. In solidity these range checks are implicit, but in act they must be made explicit in the precondition block. @@ -165,6 +161,7 @@ For example, consider a constructor that initializes a balance by subtracting a constructor(uint256 initialAmount, uint256 deduction) iff inRange(uint256, initialAmount - deduction) + creates uint256 balance := initialAmount - deduction ``` diff --git a/doc/src/equiv.md b/doc/src/equiv.md index a29d1e612..329fac234 100644 --- a/doc/src/equiv.md +++ b/doc/src/equiv.md @@ -8,7 +8,7 @@ - [Running the ERC20 Example](#running-the-erc20-example) - [Expected Output for Successful Verification](#expected-output-for-successful-verification) - [When Verification Fails: Example with Broken ERC20](#when-verification-fails-example-with-broken-erc20) - - [Verifying Multiple Contracts with --json](#verifying-multiple-contracts-with---json) + - [Verifying Multiple Contracts with --sources](#verifying-multiple-contracts-with---sources) - [Additional Options](#additional-options) - [How it works](#how-it-works) - [Success nodes](#success-nodes) @@ -43,7 +43,7 @@ act equiv --spec --sol act equiv --spec --vy ``` -**3. Multi-contract projects:** (more info in [Multi-Contract Projects](#verifying-multiple-contracts-with---json)) +**3. Multi-contract projects:** (more info in [Multi-Contract Projects](#verifying-multiple-contracts-with---sources)) ```sh act equiv --json ``` diff --git a/doc/src/how_to.md b/doc/src/how_to.md index baf93ab03..03ff5fdfd 100644 --- a/doc/src/how_to.md +++ b/doc/src/how_to.md @@ -44,7 +44,7 @@ The general process of writing an act specification involves: We will use a running example, that was introduced in [Storage Updates are Partially Ordered](./transitions.md#storage-updates-are-partially-ordered), to illustrate the steps. Imagine we have the follwing solidity code declaring two contracts, which we want to specify in act: -*(code from [ordered_updates.sol](https://github.com/argotorg/act/blob/main/tests/hevm/pass/ordered_updates/ordered_updates.sol) double check link )* +*(code from [ordered_updates.sol](https://github.com/argotorg/act/blob/main/tests/hevm/pass/ordered_updates/ordered_updates.sol))* ```solidity pragma solidity >=0.8.0; @@ -97,9 +97,9 @@ contract Asset { Begin by analyzing your Solidity contract: - Identify the **contract name** and specify it in act using the `contract` keyword. -- Specify the **constructor**: Look for the constructor function and note its parameters. Specify it using the `constructor` keyword and copy the constructor parameters. If the parameter is `address` and is later cast to a contract type ``, use an annotated contract type `address`. If the constructor is payable in the source code, mark it as `payable` in act (`constructor payable()`). Leave the `iff` blank for now. +- Specify the **constructor**: Look for the constructor function and note its parameters. Specify it using the `constructor` keyword and copy the constructor parameters. If the parameter is `address` and is later cast to a contract type ``, use an annotated contract type `address`. If the constructor is payable in the source code, mark it as `payable` in act (`constructor () payable`). Leave the `iff` blank for now. - Identify all **state variables**. These become storage in act and will be initialized in the constructor. In solidity they are listed at the top of the contract. List them in the constructor's `creates` block: Specify the **type** and **name** of each storage variable. -- List all **external and public functions**. These become transitions. Also the getter functions for public state variables which are automatically generated by Solidity have to be listed as transitions. You have to name these getter functions the same as corresponding storage variables. Specify the transitions after the constructor using the `transition` keyword (respectively `transition payable` for payable ones), copy the parameters from the source code. If the parameter is `address` and is later cast to a contract type ``, use an annotated contract type `address`. If a function has a return value, specify its type after the parameter list using `: `. +- List all **external and public functions**. These become transitions. Also the getter functions for public state variables which are automatically generated by Solidity have to be listed as transitions. You have to name these getter functions the same as corresponding storage variables. Specify the transitions after the constructor using the `transition` keyword (respectively `transition () payable` for payable ones), copy the parameters from the source code. If the parameter is `address` and is later cast to a contract type ``, use an annotated contract type `address`. If a function has a return value, specify its type after the parameter list using `: `. What we would have at this point for our example: @@ -128,11 +128,11 @@ contract Asset constructor(uint256 _value) iff creates - uint256 value := + uint256 Value := Admins admins := mapping(address => uint256) balanceOf := -transition assetTransfer(uint256 amt, address to) +transition assetTransfer(uint256 amt, address to) : bool transition setAdmins(address new_admin1, address new_admin2) @@ -171,7 +171,7 @@ need to already be present in the Solidity implementation of the contract, not m -Our example specification would look like this after adding the preconditions. In practice one would fill on transition at a time. But for clarity we follow each step for the whole spec.: +Our example specification would look like this after adding the preconditions. In practice one would fill one transition at a time. But for clarity we follow each step for the whole spec. We also chose to explicitly fill all the `iff` blocks, even though most of them are trivial (`iff true`) in this example and could be omitted. ```act contract Admins @@ -200,11 +200,11 @@ contract Asset constructor(uint256 _value) iff true creates - uint256 value := + uint256 Value := Admins admins := mapping(address => uint256) balanceOf := -transition assetTransfer(uint256 amt, address to) +transition assetTransfer(uint256 amt, address to) : bool iff CALLER == admins.admin1 or CALLER == admins.admin2 inRange(uint256, balanceOf[THIS] - amt) THIS != to ==> inRange(uint256, balanceOf[to] + amt) @@ -222,7 +222,7 @@ transition balanceOf(address account) : uint256 iff true ``` -The only interesting precondition is in the `assetTransfer` transition, which corresponds to the `require` statement in the Solidity code and two `inRange` checks. The other transitions have trivial preconditions (`iff true`). +The only interesting precondition is in the `assetTransfer` transition, which corresponds to the `require` statement in the Solidity code and two `inRange` checks. Let us look closer into the `inRange` checks: - In the Solidity function `assetTransfer`, the line `balanceOf[address(this)] = balanceOf[address(this)] - amt;` performs a subtraction. To ensure that this subtraction does not underflow, we add the precondition `inRange(uint256, balanceOf[THIS] - amt)`. - If the previous line did not revert, the code proceeds to the line `balanceOf[to] = balanceOf[to] + amt;`, where it performs an addition. If `to` is different from `this`, this addition could overflow, otherwise (if `to == this`) it will just go back to its original value. @@ -260,7 +260,7 @@ After considering this step the specification of the running example only the tr ```act -transition assetTransfer(uint256 amt, address to) +transition assetTransfer(uint256 amt, address to) : bool iff CALLER == admins.admin1 or CALLER == admins.admin2 inRange(uint256, balanceOf[THIS] - amt) THIS != to ==> inRange(uint256, balanceOf[to] + amt) @@ -363,7 +363,7 @@ There is one **special case** about updates. If a contract uses an instance of **Guidelines:** - The syntax for updating a mapping is : `mapping_name := mapping_name[key1 => new_value1, key2 => new_value2]` -- All right-hand sides use **pre-state values** (e.g., `balanceOf[CALLER] - value` subtracts from the old balance) +- All right-hand sides use **pre-state values** (e.g., `balanceOf[CALLER] - _value` subtracts from the old balance) - Right-hand-sides of updates **cannot** be transition calls. Transition calls have to be inlined as described in step 3 and section [Inline Function Calls](#inline-function-calls) - If the contract's balance in Ether changes, update it using the special variable `BALANCE` - Every storage slot can be mentioned at most once per `case` block, except for the explained special case @@ -372,16 +372,16 @@ There is one **special case** about updates. If a contract uses an instance of ### Return values -For each transition where the signature specifies a return type, `returns ` has to be present for each `case` block. The returned expression can reference storage and parameters but always refers to the pre-state. +For each transition where the signature specifies a return type, `returns ` has to be present for each `case` block. The returned expression can reference storage and parameters but always refers to the pre-state. **Guidelines:** -- Use `returns expression` to specify the return value +- Use `returns ` to specify the return value - The return value can reference storage and parameters but always refers to the pre-state The final act specification of the Solidity code at the beginning of this page is the following: -*(also available as [ordered_updates.act](https://github.com/argotorg/act/blob/main/tests/hevm/pass/ordered_updates/ordered_updates.act) double check link )* +*(also available as [ordered_updates.act](https://github.com/argotorg/act/blob/main/tests/hevm/pass/ordered_updates/ordered_updates.act))* ```act contract Admins @@ -415,11 +415,12 @@ contract Asset constructor(uint256 _value) iff true creates - uint256 value := _value + uint256 Value := _value Admins admins := Admins(CALLER) mapping(address => uint256) balanceOf := [THIS => _value] + transition assetTransfer(uint256 amt, address to) : bool iff CALLER == admins.admin1 or CALLER == admins.admin2 @@ -433,8 +434,12 @@ updates THIS => balanceOf[THIS] - amt, to => balanceOf[to] + amt ] +returns true + case THIS == to +returns true + transition setAdmins(address new_admin1, address new_admin2) @@ -450,9 +455,9 @@ updates case not (CALLER == admins.admin1 or CALLER == admins.admin2) -transition value() : uint256 +transition Value() : uint256 iff true -returns value +returns Value transition balanceOf(address idx) : uint256 iff true @@ -526,7 +531,7 @@ contract Example { ```act // This is NOT valid act syntax transition updateBalance(uint256 amount) -iff true + updates balance := computeNewBalance(amount) // ❌ Function calls not allowed here ``` @@ -565,7 +570,7 @@ contract BranchingExample { ```act // This is NOT valid act syntax transition updateBalance(uint256 amount, bool addBonus) -iff true + updates balance := computeNewBalance(amount, addBonus) // ❌ Function call ``` diff --git a/doc/src/rocq.md b/doc/src/rocq.md index 3ab79394d..864849059 100644 --- a/doc/src/rocq.md +++ b/doc/src/rocq.md @@ -94,8 +94,8 @@ Theory.v - `-Q /path/to/act/lib ActLib` - Makes ActLib available (adjust path to your act installation) - List all `.v` files that should be compiled -**For the ERC20 example in the act repository:** -Add link. +**For the [ERC20 example](https://github.com/argotorg/act/tree/main/tests/rocq/ERC20) in the act repository:** + ```rocq-project -Q . ERC20 -Q ../../../lib ActLib @@ -115,7 +115,7 @@ verify: RocqMakefile MyContract.v make -f RocqMakefile MyContract.v: mycontract.act - act coq --file mycontract.act > MyContract.v + act rocq --file mycontract.act > MyContract.v RocqMakefile: _RocqProject rocq makefile -f _RocqProject -o RocqMakefile @@ -149,7 +149,7 @@ regenerate: clean MyContract.v verify Start with the basic structure: -```coq +```rocq Require Import MyContractDir.MyContract. Require Import ActLib.ActLib. @@ -498,7 +498,7 @@ Inductive transition (ENV : Env) (STATE : State) (NextAddr : address) (STATE' : -> transition ENV STATE NextAddr STATE' NextAddr' ``` -Since the Token contract does not refer to other contracts in its storage, the `transition` relation is essentially the same as the `Token_transition` relation. However, if a contract interacts with other contracts, the `transition` relation would need to account for those interactions as well. For instance, the Automated Market Maker contract [amm.act](https://github.com/argotorg/act/blob/main/tests/hevm/pass/multisource/amm/amm.act) stores two ERC20 Tokens in its storage, `token0` and `token1`. The state transitions can +Since the Token contract does not refer to other contracts in its storage, the `transition` relation is essentially the same as the `Token_transition` relation. However, if a contract interacts with other contracts, the `transition` relation would need to account for those interactions as well. For instance, the Automated Market Maker contract [amm.act](https://github.com/argotorg/act/blob/main/tests/rocq/amm/amm.act) stores two ERC20 Tokens in its storage, `token0` and `token1`. The state transitions can thus arise from calling the `Amm` contract's own transitions, or from calling transitions on either of the two stored Token contracts. The `transition` for `Amm` thus includes cases for the `Amm_Transition`, `Token_transition` for `token0`, and `Token_transition` for `token1` and has the following shape ```rocq Inductive transition (ENV : Env) (STATE : State) (NextAddr : address) (STATE' : State) (NextAddr' : address) : Prop := @@ -581,7 +581,7 @@ You are then welcome to use this lemma in the proof of your properties. ## Proving properties using the act Rocq export Now that the state transition system is exported automatically, -one can use it to prove properties about the contract. In the [Theory.v](https://github.com/argotorg/act/blob/rewrite/tests/coq/ERC20/Theory.v) you can find a proof of the *sum of balances invariant*, stating that at any possible reachable state the sum of balances is the same, and equal to the total supply: +one can use it to prove properties about the contract. In the [Theory.v](https://github.com/argotorg/act/blob/main/tests/rocq/ERC20/Theory.v) you can find a proof of the *sum of balances invariant*, stating that at any possible reachable state the sum of balances is the same, and equal to the total supply: ``` Theorem Token_sumOfBalances_eq_totalSupply : forall STATE, reachable STATE -> diff --git a/doc/src/running_ex.md b/doc/src/running_ex.md index 4bc8b1de8..ad93495cf 100644 --- a/doc/src/running_ex.md +++ b/doc/src/running_ex.md @@ -56,22 +56,19 @@ An **act specification** describes the **externally observable behavior** of thi ## The Shape of an act Contract The translation of the code above into an act specification has the following top-level structure: -*(snippet from [erc20.act](https://github.com/argotorg/act/blob/main/tests/hevm/pass/multisource/erc20/erc20.act), headers only)* +*(snippet from [erc20.act](https://github.com/argotorg/act/blob/main/tests/hevm/pass/multisource/erc20/erc20.act), high-level structure only)* ```act,editable contract Token: constructor(uint256 _totalSupply) -iff true - ... creates uint256 totalSupply := _totalSupply mapping(address => uint) balanceOf := [CALLER => _totalSupply] mapping(address => mapping(address => uint)) allowance := [] transition transfer(uint256 value, address to) -iff true - ... +iff ... case CALLER != to: updates ... @@ -80,8 +77,7 @@ case CALLER == to: ... transition transferFrom(address from, address to, uint256 value) -iff true -... +iff ... ``` Even without understanding the details, several aspects are already visible: @@ -89,15 +85,15 @@ Even without understanding the details, several aspects are already visible: - Afterwards the constructor `contructor()` follows. - Lastly all smart contract functions are listed as transitions `transition ()` - Within the constructor and the transitions: - - The list of preconditions (the `iff` block) comes first and lists the necessary and sufficient conditions on when this operation succeeds. If the `iff` block is not satisfied, the corresponding function in Solidity/Vyper would revert. + - The list of preconditions (the `iff` block) comes first and lists the necessary and sufficient conditions on when this operation succeeds. If the `iff` block is not satisfied, the corresponding function in Solidity/Vyper would revert. If there are no preconditions, the `iff` block is omitted. - In the constructor the `creates` block is next. It lists all the storage a contract has and initializes it. As expected, it mirrors the Solidity/Vyper code closely. The `creates` block is the last block of the constructor. - Similar to `creates` for constructors works the `updates` block for transitions. It updates all the changes to the storage. Thereby, summarizing the effects a transition has on the storage. - - If there are any branches in the underlying Solidity/Vyper code, then act distinguishes what happens to the storage relative to a `case`. In the ERC20 example, that happens in line 14 and line 17: depending on whether the function caller `CALLER` is the same address as the one where the money is supposed to be transfered to, `to`, the storage is updated differently. + - If there are any branches in the underlying Solidity/Vyper code, then act distinguishes what happens to the storage relative to a `case`. In the ERC20 example, that happens in line 11 and line 14: depending on whether the function caller `CALLER` is the same address as the one where the money is supposed to be transfered to, `to`, the storage is updated differently. - act is aware of some Ethereum environment variables such as the caller of a function `CALLER` or the amount that was "paid" to a contract upon a function call `CALLVALUE`. In the next sections, we will build up the meaning of these pieces by incrementally refining the ERC20 specification. -Jump to [Running the ERC20 Example](./layout_tooling.md#running-the-erc20-example) if you want to try out running the ERC20 example with verification backends. +Jump to [Running the ERC20 Example](./equiv.md#running-the-erc20-example) if you want to try out running the ERC20 example with the equivalence checking backend. To explore the Rocq extraction of the ERC20 example, go to [act Export](./rocq.md#act-export).