doc: start working on doc

doc/src/equiv.md

@@ -1,51 +1,76 @@
 # Checking equivalence with EVM bytecode
 
 EVM bytecode can be formally verified to implement an Act spec. This
-means that each successful behavior of the bytecode should be covered
+means that each successful end state of the bytecode should be covered
 by the Act spect. To check equivalence the Act spec is translated to
-Expr, the intermediate representation of HEVM, and the EVM bytecode is
-symbolically executed to obtain its Expr representation. Then
-equivalence can be checked with the equivalence checker of HEVM.
+`Expr`, the intermediate representation of hevm, and the EVM bytecode
+is symbolically executed to obtain its `Expr` representation. Then
+equivalence can be checked with the equivalence checker of hevm.
 
-The Expr representation of an Act program is a list of *Success*
-nodes, that contain the possible successful results of the
-computation. The Expr representation of the EVM bytecode can also be
+The `Expr` representation of an Act program is a list of *Success*
+nodes, that contain all possible results of the
+computation.
+%
+The `Expr` representation of the EVM bytecode can also be
 flattened to a list of result nodes from which we only keep the
 successful executions, filtering out failed and partial execution
 paths. An informative warning will be thrown when partial executions
 are encountered.
 
-A success node in Expr, `Success cond res storage`, is a leaf in the
-Expr tree representation and contains the path conditions, `cond` that
-lead to the leaf, the result buffer `res`, and the end state
-`storage`.
+A success node in `Expr`, `Success cond res storage`, is a leaf in the
+`Expr` tree representation and contains the path conditions, `cond`
+that lead to the leaf, the result buffer `res`, and the end final
+storage `storage`.
 
 
-## Equivalence checks 
-To check equivalence between the two Expr representations the
-following checks are performed. 
+
+
+## Equivalence checks
+For each constructor and behavior in the Act spec
+we perform the following
+
+1. translate it to its `Expr` representation
+2. find the corresponing bahavior in the bytecode, by doing symbolic
+execution using the calldata the corresponds to the desired
+behavior. This will return an `Expr` list of end states that
+corresponds to this constructor/behaviour.
+
+Then for each behaviour we check the following.
 
 ### Result equivalence
-The two list of `Success` nodes are checked for equivalence using
-the HEVM equivalence checker. For each pair of nodes in the two lists,
-we check that for all inputs that satisfy the combined path conditions the
-result and final storage the same. 
+The two list of `Success` nodes are checked for equivalence using the
+HEVM equivalence checker. For each pair of nodes in the two lists, we
+check that for all inputs that satisfy the path conditions of both
+lists the result and final state (return and storage) must be the
+same.
 
 ### Input space equivalence
-Since the input space of the two lists is not necessarily exhaustive,
-some inputs may lead to failed execution paths that are not
-present in the list. We therefore need to check that the input space of the two
-lists are the same. That is, there must not be inputs that satisfy
-some path condition in the first list but not the second and vice verse. 
+We also need to check that the path conditions that may lead to this
+behavior are the same in both list.
+That is, there must not be inputs that satisfy
+some path condition in the first list but not the second and vice verse.
 
-Say that the Act program has the Expr representation 
+Say that the Act program has the Expr representation
 `[Success c1 r1 s1, ..., Success cn rn sn`
-and the the EVM bytecode has the Expr representation 
+and the the EVM bytecode has the Expr representation
 `[Success c1' r1' s1', ..., Success cn' rn' sn'`
 
-then we need to check that `c1 \/ .. \/ cn <-> c1' \/ .. \/ cn'` that
-is, we require that `c1 \/ .. \/ cn /\ ~ (c1' \/ .. \/ cn')` and `c1'
+then we need to check that `c1 \/ .. \/ cn <-> c1' \/ .. \/ cn'`.
+We require therefore require that `c1 \/ .. \/ cn /\ ~ (c1' \/ .. \/ cn')` and `c1'
 \/ .. \/ cn' /\ ~ (c1 \/ .. \/ cn)` are both unsatisfiable.
 
-### Exhaustiveness checks for bytecode
-TODO
+### Result equivalence
+The two list of `Success` nodes are checked for equivalence using the
+HEVM equivalence checker. For each pair of nodes in thedekfunction selector
+different from those present in Act is unsatisfiable.  If these
+assertions were satisfiable, then it must be that there is a function
+in the bytecode that produces successful end states in it is not
+covered by the spec.
+
+
+## Multiple contracts
+If the contract creates and interacts with other contracts, then
+equivalence checking becaumes more compilated.
+
+
+### Contructors

doc/src/introduction.md

@@ -1,8 +1,8 @@
 # Introduction
 
-Act is a high level specification language for evm programs. The core aim is to allow for easy
+Act is a high level specification language for EVM programs. The core aim is to allow for easy
 refinement. We want to make it as easy as possible for development teams to define a high level
-specification, which can then either be used "upwards" to prove higher level properties or
+specification, which can then be used "upwards" to prove higher level properties or
 "downwards" to demonstrate that an implementation in EVM bytecode conforms to the spec.
 
 Act currently integrates with the following tools:

doc/src/language.md

@@ -39,9 +39,9 @@ As an example consider the specification of overflow safe addition:
 
 ```act
 behaviour add of SafeMath
-interface add(uint x, uint y)
+interface add(uint256 x, uint256 y)
 
-iff in range uint
+iff in range uint256
 
    x + y
 
@@ -67,15 +67,15 @@ constructor of A
 
 A constructor section consists of the following fields:
 
-### interface
+### Interface
 
 Specifying the arguments the constructor takes.
 Example:
 ```act
 interface constructor(address _owner)
 ```
 
-### iff (optional)
+### Iff (optional)
 
 The conditions that must be satisfied in order for the contract to be created.
 These must be necessary and sufficient conditions, in the sense that if any
@@ -89,7 +89,7 @@ CALLER == _owner
 ```
 
 
-### creates
+### Creates
 Defines the storage layout of the contract.
 
 Example:
@@ -139,15 +139,15 @@ behaviour of A
 and consists of the following fields:
 
 
-### interface
+### Interface
 
 Specifying which method the behaviour refers to.
 Example:
 ```act
 interface transfer(address to, uint value)
 ```
 
-### iff (optional)
+### Iff (optional)
 
 The conditions that must be satisfied in order for the transition to apply.
 These must be necessary and sufficient conditions, in the sense that if any
@@ -161,7 +161,7 @@ iff
   CALLVALUE == 0
 ```
 
-### state updates and returns
+### State updates and returns
 
 Each behaviour must specify the state changes that happens a result of
 a valid call to the method, and its return argument, if any.
@@ -180,7 +180,7 @@ storage
 returns post(balanceOf[CALLER])
 ```
 
-### cases
+### Cases
 
 State updates and returns can be split between a number of cases, as in:
 
@@ -198,7 +198,12 @@ case to =/= CALLER:
    returns post(balanceOf[CALLER])
 ```
 
-Note that currently, either a `storage` or `returns` section, or both is required in every spec.
+Note that either a `storage` or `returns` section, or both is required in every spec.
+
+
+Cases must be both nonoverlappig and exhaustive. This is ensured
+during typechecking using an SMT solver. 
+
 
 ### Ensures (optional)
 
@@ -246,8 +251,8 @@ storage
 
 ## Range predicates
 Often, to accurately specify a contract, we need to assume that
-arithmetic operations do not overflow. This is done with built-in
-*in-range* predicates. For example, in the iff conditions of a
+arithmetic operations do not overflow. This is done with a built-in
+*inRange* predicates. For example, in the iff conditions of a
 constructor of behaviour we can write
 
 
@@ -267,8 +272,8 @@ CALLER =/= x => inRange(uint256, (a + b) - c)
 ```
 
 
-To conveniently pack many in range predicates together Act provides an
-alternative form of iff conditions
+To conveniently pack many *inRange* predicates together Act provides
+an alternative form of iff conditions:
 
 ```
 iff
@@ -278,3 +283,12 @@ iff in range uint256
    (a + b) - c
    d - e
 ```
+
+### Semantics
+The semantics of the *inRange* predicate is that the final expression,
+as well ass **all of the subexpressions** must be in the required range. 
+
+For example, the above example `inRange(uint256, (a + b) - c)`, means
+that `a`, `b`, `a + b`, and `(a + b) - c` stay withing the range of a
+`uint256`.
+