`Links` Block 

The links block allows you to declare contract linking directly in your CVL specification, replacing the link and struct_link conf file attributes. 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 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.

Syntax 

The syntax for the links block is given by the following EBNF grammar:

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 Identifiers for the id production, and Expressions for the number production.

The first id in a link_path is the contract alias (introduced via a using statement), and the second id is the name of a storage variable in that contract.

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 link conf file attribute.

Given a contract with a storage variable token of type address (or a contract type like IERC20):

contract Pool {
    IERC20 public token;
}

You can link it in your spec:

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 Dispatch 

When a storage location could resolve to one of several contracts, you can specify a list of possible targets using square brackets:

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:

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 Field Linking 

To link an address field inside a struct, use dot notation to navigate into the struct. This replaces the struct_link CLI flag.

contract Main {
    struct TokenHolder {
        IERC20 token;
    }
    TokenHolder public holder;
}

links {
    main.holder.token => tokenImpl;
}

This works with arbitrarily nested structs:

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 

You can link elements of both static and dynamic arrays using index notation.

Static arrays 

contract Main {
    IERC20[3] public fixedTokens;
}

links {
    main.fixedTokens[0] => tokenA;
    main.fixedTokens[1] => tokenB;
    main.fixedTokens[2] => tokenC;
}

Dynamic arrays 

contract Main {
    IERC20[] public tokens;
}

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 

You can link entries of mappings by specifying the key in square brackets.

Numeric keys 

links {
    main.tokenMap[0] => tokenA;
    main.tokenMap[1] => tokenB;
}

Byte cast keys 

For mappings with bytesN keys, use the to_bytesN(...) cast:

links {
    main.bytes4Map[to_bytes4(0x12345678)] => tokenA;
}

Contract alias keys 

For mappings with address keys, you can use a contract alias as the key:

links {
    main.addrMap[tokenA] => tokenC;
}

Here, the address of the tokenA contract instance is used as the mapping key.

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):

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:

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 Structures 

The links block supports arbitrary nesting of structs, arrays, and mappings:

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 variables can also be linked:

links {
    main.immutableToken => tokenB;
    main.immutableTokenMulti => [tokenA, tokenC];
}

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 link / struct_link CLI flags are mutually exclusive for the same contract. You cannot use both in the same verification run.

Migrating from CLI Flags 

If you are currently using --link or --struct_link, you can migrate to the links block as follows (assuming using statements have defined pool and tokenImpl):

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.