From c323d739dd0ac01ed205642abd13500d5b16b4aa Mon Sep 17 00:00:00 2001 From: Naftali Goldstein Date: Tue, 10 Mar 2026 16:11:43 +0200 Subject: [PATCH] add links block examples --- CLIFlags/README.md | 4 +- CVLByExample/LinksBlock/AdvancedLinking.conf | 13 ++ CVLByExample/LinksBlock/AdvancedLinking.spec | 136 ++++++++++++++++++ CVLByExample/LinksBlock/AdvancedRegistry.sol | 77 ++++++++++ CVLByExample/LinksBlock/BasicLinking.conf | 11 ++ CVLByExample/LinksBlock/BasicLinking.spec | 51 +++++++ CVLByExample/LinksBlock/BasicVault.sol | 36 +++++ CVLByExample/LinksBlock/ConfStyleLinking.conf | 14 ++ CVLByExample/LinksBlock/ConfStyleLinking.spec | 27 ++++ CVLByExample/LinksBlock/README.md | 69 +++++++++ CVLByExample/LinksBlock/Tokens.sol | 30 ++++ CVLByExample/README.md | 1 + 12 files changed, 467 insertions(+), 2 deletions(-) create mode 100644 CVLByExample/LinksBlock/AdvancedLinking.conf create mode 100644 CVLByExample/LinksBlock/AdvancedLinking.spec create mode 100644 CVLByExample/LinksBlock/AdvancedRegistry.sol create mode 100644 CVLByExample/LinksBlock/BasicLinking.conf create mode 100644 CVLByExample/LinksBlock/BasicLinking.spec create mode 100644 CVLByExample/LinksBlock/BasicVault.sol create mode 100644 CVLByExample/LinksBlock/ConfStyleLinking.conf create mode 100644 CVLByExample/LinksBlock/ConfStyleLinking.spec create mode 100644 CVLByExample/LinksBlock/README.md create mode 100644 CVLByExample/LinksBlock/Tokens.sol diff --git a/CLIFlags/README.md b/CLIFlags/README.md index 80de0286..78e6cf73 100644 --- a/CLIFlags/README.md +++ b/CLIFlags/README.md @@ -29,9 +29,9 @@ For more information about available CLI options go to: https://docs.certora.com | [--summary_recursion_limit](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#summary-recursion-limit) | | | [--optimistic_hashing](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-hashing) | | | [--hashing_length_bound](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#hashing-length-bound) | | -| [--link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#link) | [Liquidity Pool without linking](https://prover.certora.com/output/15800/e80f04180604458597fecc47c2b64e74?anonymousKey=b893bb90a8858acf903ba4aff1006af89a96d188) / [With linking](https://prover.certora.com/output/15800/f8f4b7a9180b49c1acdff4111a3c8e7a?anonymousKey=4a5b9ea156448922f7a1b4a25311d2b1e5c676ad) | +| [--link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#link) | [Liquidity Pool without linking](https://prover.certora.com/output/15800/e80f04180604458597fecc47c2b64e74?anonymousKey=b893bb90a8858acf903ba4aff1006af89a96d188) / [With linking](https://prover.certora.com/output/15800/f8f4b7a9180b49c1acdff4111a3c8e7a?anonymousKey=4a5b9ea156448922f7a1b4a25311d2b1e5c676ad). **Note**: The spec-based [`links { }` block](../CVLByExample/LinksBlock/) is now the preferred approach, supporting structs, arrays, mappings, and wildcards natively. | | [--address](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#address) | | -| [--struct_link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#struct-link) | | +| [--struct_link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#struct-link) | **Note**: The spec-based [`links { }` block](../CVLByExample/LinksBlock/) is now the preferred approach. | | --foundry_tests_mode | [Foundry integration example](https://prover.certora.com/output/15800/70e5d5141ce34e4eae0f9966b78b34d9?anonymousKey=40a3a0266ff277d769a873681b1fc7829b0b5c55) | | --auto_dispatcher | [True](https://prover.certora.com/output/15800/e803efce805b473e9347e6b1b47fd8ac?anonymousKey=8b01aeed7d78c9165d7f79df8639aa7da550f361)/[False](https://prover.certora.com/output/15800/d65194e18b1c442db1182d3266ec6638?anonymousKey=536d7d2b5bf3cb3d75a5a06c0a002fc68a9e76e1) | | [--split_rules](https://docs.certora.com/en/latest/docs/prover/cli/options.html#split-rules-rule-name-pattern) | Splitting the rule `permitFrontRun` from an ERC20 full spec run: [Instance only running `permitFrontRun`](https://prover.certora.com/output/15800/662059e5f478418c872504d1c922dcdf?anonymousKey=8da20e873559812bcba3c2045aad35e9e20f6fb7), [Instance running the rest of the rules](https://prover.certora.com/output/15800/6a7d370b3d894807bbbf73d2711c9da0?anonymousKey=149479f02f6bef7df0dcf2571b86c3066dbaa119) | diff --git a/CVLByExample/LinksBlock/AdvancedLinking.conf b/CVLByExample/LinksBlock/AdvancedLinking.conf new file mode 100644 index 00000000..bee48f49 --- /dev/null +++ b/CVLByExample/LinksBlock/AdvancedLinking.conf @@ -0,0 +1,13 @@ +{ + "files": [ + "AdvancedRegistry.sol", + "BasicVault.sol", + "Tokens.sol:TokenA", + "Tokens.sol:TokenB", + "Tokens.sol:TokenC", + "Tokens.sol:TokenD" + ], + "verify": "AdvancedRegistry:AdvancedLinking.spec", + "rule_sanity": "basic", + "msg": "Links block: advanced (wildcards, multi-target, mappings, nesting)" +} diff --git a/CVLByExample/LinksBlock/AdvancedLinking.spec b/CVLByExample/LinksBlock/AdvancedLinking.spec new file mode 100644 index 00000000..95f1e4c7 --- /dev/null +++ b/CVLByExample/LinksBlock/AdvancedLinking.spec @@ -0,0 +1,136 @@ +/// Advanced `links { }` block example: wildcards, multi-target dispatch, +/// mappings, nested containers, and struct arrays. +/// +/// Demonstrates capabilities that go beyond what the `--link` conf flag can do. + +using AdvancedRegistry as registry; +using TokenA as tokenA; +using TokenB as tokenB; +using TokenC as tokenC; +using TokenD as tokenD; + +links { + // Multi-target dispatch: the address resolves to one of the listed contracts + registry.multiTarget => [tokenA, tokenB]; + + // Wildcard dynamic array: all elements resolve to tokenA or tokenB + registry.dynamicTokens[_] => [tokenA, tokenB]; + + // Mapping with concrete key + wildcard precedence: + // Key 0 always resolves to tokenA; all other keys resolve to tokenB + registry.tokenMap[0] => tokenA; + registry.tokenMap[_] => tokenB; + + // Address-keyed mapping: contract alias used as the key + registry.addrMap[tokenA] => tokenC; + registry.addrMap[tokenB] => tokenD; + + // Wildcard + concrete precedence on array: + // Index 0 is always tokenC; all other indices are tokenA + registry.precedenceTokens[0] => tokenC; + registry.precedenceTokens[_] => tokenA; + + // bytes4-keyed mapping: to_bytes4(...) cast as the key + registry.bytes4Map[to_bytes4(0x12345678)] => tokenA; + registry.bytes4Map[to_bytes4(0xdeadbeef)] => tokenB; + + // Nested mapping: two-level indexing + registry.mapMap[0][0] => tokenC; + registry.mapMap[_][_] => [tokenA, tokenD]; + + // Struct in array: wildcard access to a struct field + registry.holderArray[_].token => [tokenA, tokenC]; +} + +methods { + function getMultiTargetValue() external returns (uint) envfree; + function getDynamicTokenValue(uint) external returns (uint) envfree; + function dynamicTokensLength() external returns (uint) envfree; + function getTokenMapValue(uint) external returns (uint) envfree; + function getAddrMapValue(address) external returns (uint) envfree; + function getPrecedenceValue(uint) external returns (uint) envfree; + function precedenceTokensLength() external returns (uint) envfree; + function getBytes4MapValue(bytes4) external returns (uint) envfree; + function getMapMapValue(uint, uint) external returns (uint) envfree; + function getHolderArrayValue(uint) external returns (uint) envfree; + function holderArrayLength() external returns (uint) envfree; +} + +/// Multi-target: value must be TokenA (1) or TokenB (2) +rule multiTargetDispatch { + uint val = getMultiTargetValue(); + assert val == 1 || val == 2; + assert registry.multiTarget == tokenA || registry.multiTarget == tokenB; +} + +/// Wildcard dynamic array: every element is TokenA or TokenB +rule wildcardDynamicArray { + uint i; + require dynamicTokensLength() > i; + uint val = getDynamicTokenValue(i); + assert val == 1 || val == 2; + assert registry.dynamicTokens[i] == tokenA || registry.dynamicTokens[i] == tokenB; +} + +/// Mapping with wildcard precedence: key 0 -> TokenA (1), all others -> TokenB (2) +rule mappingWithPrecedence { + // Concrete key takes priority + assert getTokenMapValue(0) == 1; + assert registry.tokenMap[0] == tokenA; + + // Wildcard applies to all other keys + uint key; + require key != 0; + assert getTokenMapValue(key) == 2; + assert registry.tokenMap[key] == tokenB; +} + +/// Address-keyed mapping: contract aliases as keys +rule addressKeyedMapping { + assert getAddrMapValue(tokenA) == 3; // tokenA -> tokenC (value 3) + assert getAddrMapValue(tokenB) == 4; // tokenB -> tokenD (value 4) + assert registry.addrMap[tokenA] == tokenC; + assert registry.addrMap[tokenB] == tokenD; +} + +/// Wildcard + concrete precedence on array: +/// Index 0 is tokenC (3), all others are tokenA (1) +rule arrayPrecedence { + require precedenceTokensLength() >= 2; + + assert getPrecedenceValue(0) == 3; + assert registry.precedenceTokens[0] == tokenC; + + assert getPrecedenceValue(1) == 1; + assert registry.precedenceTokens[1] == tokenA; +} + +/// bytes4-keyed mapping: to_bytes4 casts as keys +rule bytes4Mapping { + assert getBytes4MapValue(to_bytes4(0x12345678)) == 1; // tokenA + assert getBytes4MapValue(to_bytes4(0xdeadbeef)) == 2; // tokenB + assert registry.bytes4Map[to_bytes4(0x12345678)] == tokenA; + assert registry.bytes4Map[to_bytes4(0xdeadbeef)] == tokenB; +} + +/// Nested mapping: concrete [0][0] -> tokenC (3), +/// wildcard [_][_] -> tokenA (1) or tokenD (4) +rule nestedMapping { + // Concrete entry + assert getMapMapValue(0, 0) == 3; + + // Wildcard entries + uint i; uint j; + require i != 0 || j != 0; + uint val = getMapMapValue(i, j); + assert val == 1 || val == 4; +} + +/// Struct in array: wildcard links holderArray[_].token to tokenA or tokenC +rule structInArray { + uint i; + require holderArrayLength() > i; + uint val = getHolderArrayValue(i); + assert val == 1 || val == 3; + assert registry.holderArray[i].token == tokenA || registry.holderArray[i].token == tokenC; +} diff --git a/CVLByExample/LinksBlock/AdvancedRegistry.sol b/CVLByExample/LinksBlock/AdvancedRegistry.sol new file mode 100644 index 00000000..3b72f498 --- /dev/null +++ b/CVLByExample/LinksBlock/AdvancedRegistry.sol @@ -0,0 +1,77 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "./Tokens.sol"; +import {TokenHolder} from "./BasicVault.sol"; + +contract AdvancedRegistry { + // Multi-target dispatch: address could be one of several contracts + address public multiTarget; + + // Dynamic array + address[] public dynamicTokens; + + // Uint-keyed mapping + mapping(uint256 => address) public tokenMap; + + // Address-keyed mapping (contract alias can be used as key in spec) + mapping(address => address) public addrMap; + + // For wildcard + concrete precedence demo + address[] public precedenceTokens; + + // Bytes4-keyed mapping + mapping(bytes4 => address) public bytes4Map; + + // Nested mapping + mapping(uint256 => mapping(uint256 => address)) public mapMap; + + // Struct in array + TokenHolder[] public holderArray; + + // --- Accessor functions --- + + function getMultiTargetValue() external view returns (uint) { + return IToken(multiTarget).getValue(); + } + + function getDynamicTokenValue(uint i) external view returns (uint) { + return IToken(dynamicTokens[i]).getValue(); + } + + function dynamicTokensLength() external view returns (uint) { + return dynamicTokens.length; + } + + function getTokenMapValue(uint key) external view returns (uint) { + return IToken(tokenMap[key]).getValue(); + } + + function getAddrMapValue(address key) external view returns (uint) { + return IToken(addrMap[key]).getValue(); + } + + function getPrecedenceValue(uint i) external view returns (uint) { + return IToken(precedenceTokens[i]).getValue(); + } + + function precedenceTokensLength() external view returns (uint) { + return precedenceTokens.length; + } + + function getBytes4MapValue(bytes4 key) external view returns (uint) { + return IToken(bytes4Map[key]).getValue(); + } + + function getMapMapValue(uint i, uint j) external view returns (uint) { + return IToken(mapMap[i][j]).getValue(); + } + + function getHolderArrayValue(uint i) external view returns (uint) { + return IToken(holderArray[i].token).getValue(); + } + + function holderArrayLength() external view returns (uint) { + return holderArray.length; + } +} diff --git a/CVLByExample/LinksBlock/BasicLinking.conf b/CVLByExample/LinksBlock/BasicLinking.conf new file mode 100644 index 00000000..5f7ec01c --- /dev/null +++ b/CVLByExample/LinksBlock/BasicLinking.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "BasicVault.sol", + "Tokens.sol:TokenA", + "Tokens.sol:TokenB", + "Tokens.sol:TokenC" + ], + "verify": "BasicVault:BasicLinking.spec", + "rule_sanity": "basic", + "msg": "Links block: basic linking (scalar, immutable, struct, array)" +} diff --git a/CVLByExample/LinksBlock/BasicLinking.spec b/CVLByExample/LinksBlock/BasicLinking.spec new file mode 100644 index 00000000..96ac024d --- /dev/null +++ b/CVLByExample/LinksBlock/BasicLinking.spec @@ -0,0 +1,51 @@ +/// Basic `links { }` block example: scalar, immutable, struct, and static array linking. +/// +/// This spec demonstrates the new spec-based linking syntax, replacing the +/// `--link` and `--struct_link` conf flags. All linking is declared in the spec +/// alongside the rules that depend on it. + +using BasicVault as vault; +using TokenA as tokenA; +using TokenB as tokenB; +using TokenC as tokenC; + +links { + vault.primaryToken => tokenA; // scalar field + vault.immutableToken => tokenB; // immutable field + vault.holder.token => tokenC; // struct field (not possible with --link conf flag) + vault.fixedTokens[0] => tokenA; // static array element + vault.fixedTokens[1] => tokenB; +} + +methods { + function getPrimaryValue() external returns (uint) envfree; + function getImmutableValue() external returns (uint) envfree; + function getHolderValue() external returns (uint) envfree; + function getFixedTokenValue(uint) external returns (uint) envfree; +} + +/// Scalar field: primaryToken is linked to TokenA (value 1) +rule scalarLinked { + assert getPrimaryValue() == 1; + assert vault.primaryToken == tokenA; +} + +/// Immutable field: immutableToken is linked to TokenB (value 2) +rule immutableLinked { + assert getImmutableValue() == 2; + assert vault.immutableToken == tokenB; +} + +/// Struct field: holder.token is linked to TokenC (value 3) +rule structFieldLinked { + assert getHolderValue() == 3; + assert vault.holder.token == tokenC; +} + +/// Static array: fixedTokens[0] = TokenA (1), fixedTokens[1] = TokenB (2) +rule staticArrayLinked { + assert getFixedTokenValue(0) == 1; + assert getFixedTokenValue(1) == 2; + assert vault.fixedTokens[0] == tokenA; + assert vault.fixedTokens[1] == tokenB; +} diff --git a/CVLByExample/LinksBlock/BasicVault.sol b/CVLByExample/LinksBlock/BasicVault.sol new file mode 100644 index 00000000..bdf56ff8 --- /dev/null +++ b/CVLByExample/LinksBlock/BasicVault.sol @@ -0,0 +1,36 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "./Tokens.sol"; + +struct TokenHolder { + address token; + uint256 weight; +} + +contract BasicVault { + address public primaryToken; + address public immutable immutableToken; + TokenHolder public holder; + address[2] public fixedTokens; + + constructor(address _immutableToken) { + immutableToken = _immutableToken; + } + + function getPrimaryValue() external view returns (uint) { + return IToken(primaryToken).getValue(); + } + + function getImmutableValue() external view returns (uint) { + return IToken(immutableToken).getValue(); + } + + function getHolderValue() external view returns (uint) { + return IToken(holder.token).getValue(); + } + + function getFixedTokenValue(uint i) external view returns (uint) { + return IToken(fixedTokens[i]).getValue(); + } +} diff --git a/CVLByExample/LinksBlock/ConfStyleLinking.conf b/CVLByExample/LinksBlock/ConfStyleLinking.conf new file mode 100644 index 00000000..cee24c5f --- /dev/null +++ b/CVLByExample/LinksBlock/ConfStyleLinking.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "BasicVault.sol", + "Tokens.sol:TokenA", + "Tokens.sol:TokenB" + ], + "verify": "BasicVault:ConfStyleLinking.spec", + "link": [ + "BasicVault:primaryToken=TokenA", + "BasicVault:immutableToken=TokenB" + ], + "rule_sanity": "basic", + "msg": "Conf-style linking with --link flag (old approach)" +} diff --git a/CVLByExample/LinksBlock/ConfStyleLinking.spec b/CVLByExample/LinksBlock/ConfStyleLinking.spec new file mode 100644 index 00000000..f7b72d2f --- /dev/null +++ b/CVLByExample/LinksBlock/ConfStyleLinking.spec @@ -0,0 +1,27 @@ +/// Conf-style linking example: same contract, but linking is done via the +/// `--link` conf flag instead of a `links { }` block. +/// +/// Note: The `--link` conf flag can only link scalar and immutable fields. +/// Struct fields (like holder.token) and array elements require either +/// `--struct_link` or the new `links { }` block. + +using BasicVault as vault; +using TokenA as tokenA; +using TokenB as tokenB; + +methods { + function getPrimaryValue() external returns (uint) envfree; + function getImmutableValue() external returns (uint) envfree; +} + +/// Scalar field: primaryToken is linked to TokenA (value 1) via conf --link +rule scalarLinked { + assert getPrimaryValue() == 1; + assert vault.primaryToken == tokenA; +} + +/// Immutable field: immutableToken is linked to TokenB (value 2) via conf --link +rule immutableLinked { + assert getImmutableValue() == 2; + assert vault.immutableToken == tokenB; +} diff --git a/CVLByExample/LinksBlock/README.md b/CVLByExample/LinksBlock/README.md new file mode 100644 index 00000000..bad67be8 --- /dev/null +++ b/CVLByExample/LinksBlock/README.md @@ -0,0 +1,69 @@ +# Links Block Example + +## Overview + +The `links { }` block is a CVL feature for declaring contract linking directly in the spec file, replacing the `--link` and `--struct_link` conf flags. Linking tells the Prover which concrete contract an address field points to, enabling precise verification of multi-contract interactions. + +With the `links { }` block, linking declarations live alongside the rules that depend on them, and support advanced features like struct field linking, array/mapping indexing, wildcards, and multi-target dispatch. + +## Syntax Quick Reference + +| Pattern | Description | +| ------- | ----------- | +| `main.field => target` | Scalar or immutable field | +| `main.holder.token => target` | Struct field (dot notation) | +| `main.arr[0] => target` | Array element (concrete index) | +| `main.arr[_] => target` | Wildcard (all indices) | +| `main.arr[0] => targetA; main.arr[_] => targetB` | Concrete precedence (index 0 -> targetA, rest -> targetB) | +| `main.field => [targetA, targetB]` | Multi-target dispatch | +| `main.map[0] => target` | Mapping (concrete key) | +| `main.map[_] => target` | Mapping (wildcard key) | +| `main.map[to_bytes4(0x1234)] => target` | Typed key cast | +| `main.map[contractAlias] => target` | Contract alias as key | +| `main.map[0][0] => target` | Nested mapping/array | +| `main.arr[_].field => target` | Struct field in array | + +## Examples + +### 1. BasicLinking — Scalar, immutable, struct, static array + +Demonstrates the most common linking patterns using the new `links { }` syntax. + +**Command:** +```bash +certoraRun BasicLinking.conf +``` + +### 2. ConfStyleLinking — Comparison with old `--link` conf flag + +Same contract, but linking is done via the `--link` conf flag. Only scalar and immutable fields can be linked this way — struct fields and arrays require the `links { }` block. + +**Command:** +```bash +certoraRun ConfStyleLinking.conf +``` + +### 3. AdvancedLinking — Wildcards, multi-target, mappings, nesting + +Demonstrates advanced capabilities: +- **Multi-target dispatch**: `field => [tokenA, tokenB]` — the Prover considers both targets +- **Wildcard arrays**: `arr[_] => target` — all indices resolve to the target +- **Wildcard precedence**: concrete entries override wildcards at the same path +- **Address-keyed mappings**: contract aliases used as mapping keys +- **bytes4-keyed mappings**: `to_bytes4(...)` casts as keys +- **Nested mappings**: `map[i][j] => target` +- **Struct arrays**: `arr[_].field => target` + +**Command:** +```bash +certoraRun AdvancedLinking.conf +``` + +## Important Notes + +- The `links { }` block and `--link`/`--struct_link` conf flags are **mutually exclusive** per contract. You cannot use both for the same contract. +- For dynamic arrays with concrete element links, the compiler assumes `length > index` for each linked index. +- When both concrete and wildcard entries exist at the same path, concrete entries take precedence. +- Wildcard indices cannot be mixed with concrete indices in the same entry (e.g., `arr[0][_]` is not allowed — use all concrete or all wildcards). + +For a comprehensive guide on Certora Verification Language, refer to the [Certora Documentation](https://docs.certora.com). diff --git a/CVLByExample/LinksBlock/Tokens.sol b/CVLByExample/LinksBlock/Tokens.sol new file mode 100644 index 00000000..3757fb04 --- /dev/null +++ b/CVLByExample/LinksBlock/Tokens.sol @@ -0,0 +1,30 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +interface IToken { + function getValue() external view returns (uint); +} + +contract TokenA is IToken { + function getValue() external pure returns (uint) { + return 1; + } +} + +contract TokenB is IToken { + function getValue() external pure returns (uint) { + return 2; + } +} + +contract TokenC is IToken { + function getValue() external pure returns (uint) { + return 3; + } +} + +contract TokenD is IToken { + function getValue() external pure returns (uint) { + return 4; + } +} diff --git a/CVLByExample/README.md b/CVLByExample/README.md index 1aa9b4f7..b52b76a5 100644 --- a/CVLByExample/README.md +++ b/CVLByExample/README.md @@ -35,6 +35,7 @@ | **struct** | [struct return type](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L47),
`struct` in `methods` block: [struct parameter](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L23), [struct return type](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L19),
[returning a struct as a tuple](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L21),
`struct` in a `CVL` function: [struct parameter to a CVL function](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L36),
[struct return type of a CVL function](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L47), [returning struct as a tuple](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L53),
[assignment to struct](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L98), [Assigning struct to a tuple](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L77) | | **use** | `rule`: [with filters](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L32), [overriding imported filters](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L32),
[`invariant`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L10): [overriding imported `preserved`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L12), [builtin rule](https://github.com/Certora/Examples/blob/master/CVLByExample/Reentrancy/certora/spec/ViewReentrancy.spec#L1) | | **using** | [`using`](https://github.com/Certora/Examples/blob/master/DEFI/LiquidityPool/certora/specs/pool_link.spec#L14) | +| **links { }** | [Basic linking](CVLByExample/LinksBlock/BasicLinking.spec), [Advanced (wildcards, multi-target, nesting)](CVLByExample/LinksBlock/AdvancedLinking.spec), [Comparison with --link conf flag](CVLByExample/LinksBlock/ConfStyleLinking.spec) | | **withrevert** | [`withrevert`](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L44) | | **CVL Type** | [mathint](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L23), [method](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L83), [env](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L20) | | **ercecover** | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/Ecrecover/ecrecover.spec#L67) |