MainnetController.conf

{
    "files": [
        "spark-alm-controller/src/MainnetController.sol",
        "spark-alm-controller/src/ALMProxy.sol",
        "spark-alm-controller/src/RateLimits.sol",
        "harness/CctpMock.sol",
        "harness/DaiUsdsMock.sol",
        "harness/PsmMock.sol",
        "harness/AllocatorVaultMock.sol",
        "harness/DaiMock.sol",
        "harness/UsdsMock.sol",
        "harness/UsdcMock.sol",
        "harness/SUsdsMock.sol",
        "harness/Auxiliar.sol"
    ],
    "solc": "solc-0.8.21",
    "solc_optimize": "200",
    "packages": [
        "forge-std/interfaces/=spark-alm-controller/lib/forge-std/src/interfaces",
        "openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts",
        "lib/openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts",
        "src=spark-alm-controller/src"
    ],
    "link": [
        "MainnetController:proxy=ALMProxy",
        "MainnetController:rateLimits=RateLimits",
        "MainnetController:cctp=CctpMock",
        "MainnetController:daiUsds=DaiUsdsMock",
        "MainnetController:psm=PsmMock",
        "MainnetController:vault=AllocatorVaultMock",
        "MainnetController:dai=DaiMock",
        "MainnetController:usds=UsdsMock",
        "MainnetController:usdc=UsdcMock",
        "MainnetController:susds=SUsdsMock"
    ],
    "verify": "MainnetController:MainnetController.spec",
    "rule_sanity": "basic",
    "multi_assert_check": true,
    "optimistic_loop": true,
    "prover_args": [
        "-enableABIAnalysis true"
    ],
    "parametric_contracts": ["MainnetController"],
    "smt_timeout": "7000",
    "build_cache": true,
    "msg": "MainnetController"
}