document links block

Author: naftali-g

docs/cvl/index.md

@@ -16,6 +16,7 @@ expr.md
 statements.md
 imports.md
 using.md
+linking.md
 methods.md
 rules.md
 builtin.md

docs/cvl/linking.md

@@ -0,0 +1,348 @@
+(linking)=
+`Links` Block
+===========
+
+The `links` block allows you to declare contract linking directly in your CVL
+specification, replacing the {ref}`--link` and {ref}`--struct_link` CLI flags.
+Each entry in the `links` block tells the Prover that a particular storage
+location holding an address should be resolved to a specific contract instance
+in the {term}`scene`.
+
+The `links` block supports linking simple scalar fields, struct fields, array
+elements, mapping entries, immutable variables, and arbitrary nesting of these.
+Entries can target a single contract or a list of possible contracts, and can
+use wildcard indices to cover all keys of a mapping or all elements of an array.
+
+```{contents}
+```
+
+Syntax
+------
+
+The syntax for the `links` block is given by the following [EBNF grammar](ebnf-syntax):
+
+```
+links_block   ::= "links" "{" { link_entry } "}"
+
+link_entry    ::= link_path "=>" id ";"
+               | link_path "=>" "[" id { "," id } "]" ";"
+
+link_path     ::= id "." id { link_segment }
+
+link_segment  ::= "." id
+               | "[" index_expr "]"
+
+index_expr    ::= number
+               | "to_bytes" number "(" number ")"
+               | id
+               | "_"
+```
+
+See {ref}`identifiers` for the `id` production, and {doc}`expr` for the
+`number` production.
+
+The first `id` in a `link_path` is the contract alias (introduced via a
+{ref}`using statement <using-stmt>`), and the second `id` is the name of a
+storage variable in that contract.
+
+
+(basic-linking)=
+Basic Linking
+-------------
+
+The simplest form of linking maps a storage variable that holds an address to a
+contract instance in the scene.  This is equivalent to using the {ref}`--link`
+CLI flag.
+
+Given a contract with a storage variable `token` of type `address` (or a
+contract type like `IERC20`):
+
+```solidity
+contract Pool {
+    IERC20 public token;
+}
+```
+
+You can link it in your spec:
+
+```cvl
+using Pool as pool;
+using TokenImpl as tokenImpl;
+
+links {
+    pool.token => tokenImpl;
+}
+```
+
+This is equivalent to passing `--link Pool:token=TokenImpl` on the command line
+or in the conf file.
+
+
+(multi-target-linking)=
+Multi-Target Dispatch
+---------------------
+
+When a storage location could resolve to one of several contracts, you can
+specify a list of possible targets using square brackets:
+
+```cvl
+links {
+    pool.token => [tokenA, tokenB];
+}
+```
+
+This tells the Prover that `pool.token` could be the address of either
+`tokenA` or `tokenB`, and it will consider both possibilities when resolving
+calls through that field.
+
+Multi-target entries are particularly useful when combined with array or mapping
+linking.  For example, to verify a contract that holds two tokens which may or
+may not be the same:
+
+```cvl
+links {
+    main.tokens[0] => tokenA;
+    main.tokens[1] => [tokenA, tokenB];
+}
+```
+
+This allows the Prover to explore both the case where both elements point to
+the same contract and the case where they point to different contracts.
+
+
+(struct-linking)=
+Struct Field Linking
+--------------------
+
+To link an address field inside a struct, use dot notation to navigate into the
+struct.  This replaces the {ref}`--struct_link` CLI flag.
+
+```solidity
+contract Main {
+    struct TokenHolder {
+        IERC20 token;
+    }
+    TokenHolder public holder;
+}
+```
+
+```cvl
+links {
+    main.holder.token => tokenImpl;
+}
+```
+
+This works with arbitrarily nested structs:
+
+```cvl
+links {
+    main.wrapper.inner.token => tokenImpl;
+}
+```
+
+Unlike `--struct_link`, the `links` block targets a specific storage variable
+and struct path, so there is no risk of accidentally linking the same field name
+across unrelated struct types.
+
+```{note}
+The `--struct_link` flag matches a field name across all structs in the contract,
+including struct values inside mappings and arrays.  For example, if a contract
+has `mapping(uint => MyStruct) myMapping` where `MyStruct` has an `address`
+field called `token`, then `--struct_link C:token=TokenA` would link the `token`
+field in every `MyStruct` value in the mapping.  The equivalent in the `links`
+block would be `c.myMapping[_].token => tokenA;`.
+```
+
+
+(array-linking)=
+Array Linking
+-------------
+
+You can link elements of both static and dynamic arrays using index notation.
+
+### Static arrays
+
+```solidity
+contract Main {
+    IERC20[3] public fixedTokens;
+}
+```
+
+```cvl
+links {
+    main.fixedTokens[0] => tokenA;
+    main.fixedTokens[1] => tokenB;
+    main.fixedTokens[2] => tokenC;
+}
+```
+
+### Dynamic arrays
+
+```solidity
+contract Main {
+    IERC20[] public tokens;
+}
+```
+
+```cvl
+links {
+    main.tokens[0] => tokenA;
+    main.tokens[1] => tokenB;
+}
+```
+
+```{note}
+For dynamic arrays with concrete index links, the linking is conditional on the
+array being long enough.  For example, linking `main.tokens[1] => tokenA`
+causes the Prover to assume `tokens.length > 1 => main.tokens[1] == tokenA`.
+If the array is shorter than the linked index, no assumption is made about that
+element.
+```
+
+
+(mapping-linking)=
+Mapping Linking
+---------------
+
+You can link entries of mappings by specifying the key in square brackets.
+
+### Numeric keys
+
+```cvl
+links {
+    main.tokenMap[0] => tokenA;
+    main.tokenMap[1] => tokenB;
+}
+```
+
+### Byte cast keys
+
+For mappings with `bytesN` keys, use the `to_bytesN(...)` cast:
+
+```cvl
+links {
+    main.bytes4Map[to_bytes4(0x12345678)] => tokenA;
+}
+```
+
+### Contract alias keys
+
+For mappings with `address` keys, you can use a contract alias as the key:
+
+```cvl
+links {
+    main.addrMap[tokenA] => tokenC;
+}
+```
+
+Here, the address of the `tokenA` contract instance is used as the mapping key.
+
+
+(wildcard-linking)=
+Wildcard Indices
+----------------
+
+Use `_` as a wildcard index to link all elements of an array or all entries of a
+mapping to the same target(s):
+
+```cvl
+links {
+    main.tokenMap[_] => tokenA;
+}
+```
+
+This means that for any key, the value of `tokenMap` is linked to `tokenA`.
+
+### Wildcard precedence
+
+When both concrete and wildcard entries exist for the same path, concrete
+entries take precedence.  For example:
+
+```cvl
+links {
+    main.tokens[0] => tokenB;
+    main.tokens[_] => tokenA;
+}
+```
+
+Here, `main.tokens[0]` resolves to `tokenB`, while all other indices resolve to
+`tokenA`.
+
+```{caution}
+You cannot mix concrete and wildcard indices in the same entry when there are
+multiple levels of indexing.  For example, `main.nested[0][_]` is not allowed.
+Each entry must use either all concrete indices or all wildcard indices.
+```
+
+
+(nested-linking)=
+Nested Structures
+-----------------
+
+The `links` block supports arbitrary nesting of structs, arrays, and mappings:
+
+```cvl
+links {
+    // Array element within a struct
+    main.arrayHolder.tokens[0] => tokenC;
+
+    // Struct within an array
+    main.structItems[0].token => tokenA;
+
+    // Struct value within a mapping
+    main.structMap[0].token => tokenC;
+}
+```
+
+
+(immutable-linking)=
+Immutable Linking
+-----------------
+
+Immutable variables can also be linked:
+
+```cvl
+links {
+    main.immutableToken => tokenB;
+    main.immutableTokenMulti => [tokenA, tokenC];
+}
+```
+
+
+(linking-requirements)=
+Requirements and Limitations
+----------------------------
+
+```{important}
+The `links` block requires storage layout information from the Solidity
+compiler.  This information is only available for contracts compiled with
+**Solidity version 0.5.13 or later**.
+```
+
+- Library contracts cannot be linked.
+- The `links` block and the {ref}`--link` / {ref}`--struct_link` CLI flags are
+  **mutually exclusive** for the same contract.  You cannot use both in the
+  same verification run.
+
+
+(linking-migration)=
+Migrating from CLI Flags
+-------------------------
+
+If you are currently using `--link` or `--struct_link`, you can migrate to the
+`links` block as follows:
+
+| CLI Flag | `links` Block Equivalent |
+| --- | --- |
+| `--link Pool:token=TokenImpl` | `pool.token => tokenImpl;` |
+| `--struct_link Pool:field=TokenImpl` | One entry per storage variable containing a struct with that field, using the full path. For example, `pool.holder.field => tokenImpl;` for a direct struct, or `pool.myMapping[_].field => tokenImpl;` for struct values inside a mapping or array. |
+
+The `links` block provides several advantages over the CLI flags:
+
+- **Type-checked:** The Prover validates that the paths and targets in the
+  `links` block are well-typed.
+- **Precise struct linking:** Unlike `--struct_link`, which applies to all
+  structs with a matching field name, the `links` block targets a specific
+  storage path.
+- **Richer linking:** Support for arrays, mappings, wildcards, and multi-target
+  dispatch that are not available through CLI flags.

docs/cvl/overview.md

@@ -16,6 +16,9 @@ A spec may contain any of the following:
  - **[Using statements](using):** Using statements allow a specification to reference
    multiple contracts.
 
+ - **[Links blocks](linking):** `links` blocks declare contract linking inline in the
+   spec, mapping storage variables holding addresses to specific contract instances.
+
  - **[Methods blocks](methods):** `methods` blocks contain information on how methods
    should be summarized by the Prover during verification.
 

docs/prover/cli/options.md

@@ -1966,6 +1966,13 @@ _Configuration file_
 ]
 ```
 
+```{note}
+You can also declare linking inline in your spec using a {ref}`links block <linking>`,
+which provides type checking, precise struct paths, and support for arrays,
+mappings, and wildcards.  The `links` block and `--link` flag cannot be used
+together for the same contract.
+```
+
 (--optimistic_contract_recursion)=
 ## `optimistic_contract_recursion`
 
@@ -2158,6 +2165,13 @@ struct ReserveTokens {
 ... then the `struct_link` setting above would result in the same fixed address values for `tokenA` and `tokenB` in instances of this struct, which is likely an unintended constraint. Similarly, structs that are values in a mapping or array will _all_ get the same address linkage.
 ````
 
+```{note}
+Consider using a {ref}`links block <linking>` in your spec instead of
+`--struct_link`.  The `links` block targets specific storage paths and avoids the
+ambiguity of matching all structs with the same field name.  The `links` block and
+`--struct_link` flag cannot be used together for the same contract.
+```
+
 
 Options for job metadata and dashboard filtering
 ================================================