Better docs

[msooseth]

Description

This is an ongoing effort to improve documentation.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[aviggiano]

Great update

I find it a bit curious that there is a circular reference between foundry and hevm. The docs from one cite the other. Not sure if there's a way out

[zoep]

Maybe add an # Overview header and itemize the following three sections

[msooseth]

Actually, good idea -- but somehow mdbook doesn't allow a header above the first line I think? When I change it to:

# Overview

- [Getting Started](./getting-started.md)
- [Quick Installation](./install.md)
- [When to Use](./when-to-use.md)

The Overview does not appear :S Even if I remove the # in front it still doesn't want to appear. Dunno what's best to do.

[msooseth]

Great update

I find it a bit curious that there is a circular reference between foundry and hevm. The docs from one cite the other. Not sure if there's a way out

Thanks for your help!! Yeah, not sure there is an out, but I think it's also OK. Not perfect, but maybe an OK start. I will probably improve things as time goes on, hopefully I'll find a way to deal with that as well :) Thanks again for your help,

Mate

[zoep]

I wound't say that symbolic execution is a testing approach (also it is not claimed in the referenced wikipedia link).

[msooseth]

Ooops, thanks for catching this! I always thought that fuzzing is kind of an automation of exploratory testing, but that does sound bogus. I fixed it to:

Fuzzing tests usually have a set of (sometimes implicit) pre- and
postconditions, but the actual action (e.g. function call) is performed by an
external entity, the fuzzer. For C/C++ fuzzing, the implicit postcondition is
often e.g. that the system does not throw a segmentation fault. For EVM
bytecode, postconditions need to be explicit. Let's see an example:

What do you think?

[zoep]

I find the discussion about testing a bit diverting, especially since nothing is said about the methodology of symbolic execution.

It would be nice if we can highlight that in testing examines inputs one by one, whereas symbolic execution analyzes entire program paths.

[msooseth]

Actually, really good point. I have no idea why I went on a tangent here, it was unnecessary. Thanks for that. I have now replaced it with:

In the cryptocurrency world, it is exceedingly easy to lose a [lot of
assets](https://chainsec.io/defi-hacks/) due to bugs. While fuzz testing can
help find potential issues with digital contracts, it is a tool that can only
execute the program concretely, one execution at a time. In contrast, Symbolic
Execution can execute all potential values in a decision path "in one go",
creating a symbolic expression out of a path, and checking whether it
can trigger a fault. Hence, Symbolic Execution tends to be more efficient at
finding bugs than fuzzing when the bugs are rare, or explicitly (i.e.
maliciously) hidden. Symbolic Execution can also _prove_ that no postcondition
can be violated, increasing the overall confidence in the contract. Note, however,
that Symbolic Execution does not automatically generate postconditions for
well-known bug classes like static code analysis tools do. Instead, these
postconditions, and their sometimes associated preconditions, need to
be explicitly written.

Let me know what you think!

[zoep]

Maybe also mention other errors as well (overflows etc.)

[msooseth]

Added overflow, good point! I don't know if I wanna put too many here, but maybe we can have a section in when-to-use.md ?

[zoep]

This is a great improvement of the docs! Thank you! I only had a couple of nits to point out.