Merge pull request #551 from ethereum/better-test-doc

Rename ds-test in our documentation to std-test + explain concrete starting state

doc/src/SUMMARY.md

@@ -5,14 +5,14 @@
 
 # Tutorials
 
-- [ds-test tutorial](./ds-test-tutorial.md)
+- [Forge std-test tutorial](./std-test-tutorial.md)
 - [Equivalence checking tutorial](./equivalence-checking-tutorial.md)
 - [Symbolic execution tutorial](./symbolic-execution-tutorial.md)
 <!-- [Discovering reachable assertion violations]() -->
 
 # Reference
 
-- [ds-test proving](./test.md)
+- [Forge test proving](./test.md)
 - [Symbolic unit execution](./symbolic.md)
 - [Equivalence checking](./equivalence.md)
 - [Concrete execution](./exec.md)

doc/src/install.md

@@ -41,7 +41,7 @@ Checking 1 function(s) in contract src/contract-pass.sol:MyContract
    [PASS] prove_pass(address,uint256)
 ```
 
-See [ds-test tutorial](./ds-test-tutorial.md) for details.
+See [Forge std-test tutorial](./std-test-tutorial.md) for details.
 
 Note that Foundry provides the solidity compiler, hence there is no need to
 install solidity separately.

doc/src/ds-test-tutorial.md → doc/src/std-test-tutorial.md

@@ -1,4 +1,4 @@
-# ds-test Tutorial
+# Forge std-test Usage Tutorial
 
 Test cases must be prepended with `prove_` and the testing contract must
 inherit from `Test` from [Forge's standard test
@@ -18,7 +18,7 @@ contract BadVaultTest is Test {
 }
 ```
 
-Once you have written such a test case, you need to compile with `forge build`
+Once you have written such a test case, you need to compile with `forge build --ast`
 (see [forge documentation](https://book.getfoundry.sh/forge/tests) for more
 details) and then:
 
@@ -134,6 +134,21 @@ rather than a `>` in the `if`. Notice that in this case, while hevm filled in
 the `address` to give a complete call, the address itself is irrelevant,
 although this is not explicitly mentioned.
 
+## Starting State is Always Concrete
+
+In `test` mode, hevm runs with the starting state set to concrete values. This
+means that with the solidity-generated default constructor of contracts, state
+variables will be zero, and arrays and mappings will be empty. If you need a
+different starting state, such as e.g. tokens already distributed to some
+addresses, you can set that up in the setup phase of your test. This can be
+done via the `beforeTestSetup` function, as documented in the [Foundry
+Book](https://book.getfoundry.sh/forge/writing-tests#before-test-setups).
+
+In case you need a symbolic starting state, see the [Symbolic execution
+tutorial](#symbolic-execution-tutorial). Note that if all you need is a
+symbolic calldata, then you don't need to run `hevm` in symbolic mode, you can
+simply run `hevm test` and hevm will provide you with a symbolic calldata.
+
 ## Test Cases that Must Always Revert
 
 Hevm assumes that a test case should not always revert. If you have such a test
@@ -195,7 +210,6 @@ Checking 1 function(s) in contract src/contract-allrevert-expected.sol:MyContrac
 
 Which is now the expected outcome.
 
-
 ## Supported Cheat Codes
 
 Since hevm is an EVM implementation mainly dedicated to testing and

doc/src/test.md

@@ -57,11 +57,11 @@ Available options:
                            reachability (default: 1) (default: 1)
 ```
 
-`hevm test` executes all solidity unit tests that make use of the `ds-test` assertion library
+`hevm test` executes all solidity unit tests that make use of the `std-test` assertion library
 (a.k.a [Foundry tests](https://book.getfoundry.sh/forge/forge-std)). It
 supports both foundry based (the default) and [dapptools](https://dapp.tools/) based projects.
 
 A more detailed introduction to symbolic unit tests with `hevm` can be found
-[here](https://fv.ethereum.org/2020/12/11/symbolic-execution-with-ds-test/). An
-overview of using ds-test for solidity testing can be found in the [foundry
+[here](https://fv.ethereum.org/2020/12/11/symbolic-execution-with-std-test/). An
+overview of using `std-test` for solidity testing can be found in the [foundry
 book](https://book.getfoundry.sh/forge/tests).

readme.md

@@ -3,7 +3,7 @@
 `hevm` is an implementation of the Ethereum virtual machine (EVM) made for
 symbolic execution, equivalence checking, and unit testing of smart contracts.
 `hevm` can symbolically execute smart contracts, run unit tests, and run
-arbitrary EVM code. It can run on state set up in a [`ds-test` testing
+arbitrary EVM code. It can run on state set up in a [Forge `std-test` testing
 harness](https://book.getfoundry.sh/forge/forge-std), or fetched on demand from
 live network using `rpc` calls.