Clean-up and Alignment of documentation

.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

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]
 
 ```
 

doc/src/constructors.md

@@ -46,7 +46,7 @@ The general shape of a constructor in act is:
 
 2. **Precondition Block**: `iff <condition>`
    - 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 <condition>: 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
 ```

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 <PATH_TO_SPEC> --sol <PATH_TO_SOL>
 act equiv --spec <PATH_TO_SPEC> --vy <PATH_TO_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 <PATH_TO_CONFIG_JSON>
 ```

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) <span style=color:red> double check link </span>)*
+*(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 `<ContractName>`, use an annotated contract type `address<ContractName>`. If the constructor is payable in the source code, mark it as `payable` in act (`constructor payable(<parameters>)`). 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 `<ContractName>`, use an annotated contract type `address<ContractName>`. If the constructor is payable in the source code, mark it as `payable` in act (`constructor (<parameters>) 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 `<ContractName>`, use an annotated contract type `address<ContractName>`. If a function has a return value, specify its type after the parameter list using `: <return_type>`.
+- 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 (<parameters>) payable` for payable ones), copy the parameters from the source code. If the parameter is `address` and is later cast to a contract type `<ContractName>`, use an annotated contract type `address<ContractName>`. If a function has a return value, specify its type after the parameter list using `: <return_type>`.
 
 What we would have at this point for our example:
 
@@ -128,11 +128,11 @@ contract Asset
 constructor(uint256 _value)
 iff <todo>
 creates
-    uint256 value := <todo>
+    uint256 Value := <todo>
     Admins admins := <todo>
     mapping(address => uint256) balanceOf := <todo>
 
-transition assetTransfer(uint256 amt, address to)
+transition assetTransfer(uint256 amt, address to) : bool
 <todo>
 
 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 := <todo>
+    uint256 Value := <todo>
     Admins admins := <todo>
     mapping(address => uint256) balanceOf := <todo>
 
-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
 <todo>
 ```
-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 <expr>` 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 <expression>` 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 <expression>` 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) <span style= color:red> double check link </span>)*
+*(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
 ```

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:**
-<span style="color:red">Add link.</span>
+**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 ->