document address function calls

docs/cvl/expr.md

@@ -108,7 +108,7 @@ Struct Comparison
 CVL supports equality comparison of structs under the following restrictions:
 
  * The structs must be of the same type.
- * The structs (or any nested structs) don't contain dynamic arrays. (`string` and `bytes` can be part of the struct) 
+ * The structs (or any nested structs) don't contain dynamic arrays. (`string` and `bytes` can be part of the struct)
  * There's no support for comparison for structs fetched using direct-storage-access.
 
 Two structs will be evaluated as equal if and only if all the fields are equal.
@@ -349,9 +349,9 @@ There are many kinds of function-like things that can be called from CVL:
 There are several additional features that can be used when calling contract
 functions (including calling them through {ref}`method variables <method-type>`).
 
-The method name can optionally be prefixed by a contract name.  If a contract is
-not explicitly named, the method will be called with `currentContract` as the
-receiver.
+The method name can optionally be prefixed by a contract name (introduced via a
+{ref}`using statement <using-stmt>`). If a contract is not explicitly named, the
+method will be called with `currentContract` as the receiver.
 
 It is possible for multiple contract methods to match the method call.  This can
 happen in two ways:
@@ -365,6 +365,15 @@ while verifying the rule, and will provide a separate verification report for
 each checked method.  Rules that use this feature are referred to as
 {term}`parametric rule`s.
 
+Another possible way to have the Prover consider options for a function is by
+prefixing the function name with an `address` typed variable. In this case the
+Prover will consider every possible contract in the scene that implements a
+function that matches the signature provided by the call (if no such function
+exists in the scene the prover will fail with an error). If there are no
+relevant constraints on the `address` variable the prover may also consider the
+case that its value does not match any contract in the scene and in this case
+the Prover will consider this a violation of the rule.
+
 (with-revert)=
 After the function name, but before the arguments, you can write an optional
 method tag, one of `@norevert` or `@withrevert`.
@@ -568,7 +577,7 @@ contract WithImmutables {
     return myImmutAddr;
   }
 }
-``` 
+```
 
 We can access both `myImmutAddr` and `myImmutBool` directly from CVL
 like this:
@@ -589,7 +598,7 @@ rule accessPublicImmut {
 }
 ```
 
-The advantages of direct immutable access is that there is no need to 
+The advantages of direct immutable access is that there is no need to
 declare `envfree` methods for the public immutables, and even more importantly, nor is there a need to harness contracts in order to
 expose the private immutables.