add links block examples

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

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)"
+}

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;
+}

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;
+    }
+}

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)"
+}

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;
+}

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();
+    }
+}

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)"
+}

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;
+}