Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

maint(ct): remove Kontrol interfaces #12178

Merged
merged 1 commit into from
Sep 27, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 18 additions & 16 deletions packages/contracts-bedrock/scripts/checks/check-interfaces.sh
Original file line number Diff line number Diff line change
Expand Up @@ -45,29 +45,31 @@ EXCLUDE_CONTRACTS=(
"ISchemaResolver"
"ISchemaRegistry"

# Kontrol
"KontrolCheatsBase"
# TODO: Interfaces that need to be fixed are below this line
# ----------------------------------------------------------

# TODO: Interfaces that need to be fixed
"IOptimismSuperchainERC20"
"IOptimismMintableERC721"
"IOptimismMintableERC20"
"ILegacyMintableERC20"
# Inlined interface, needs to be replaced.
"IInitializable"

# Missing various functions.
"IPreimageOracle"
"ICrossL2Inbox"
"IL2ToL2CrossDomainMessenger"
"ILegacyMintableERC20"
"IOptimismMintableERC20"
"IOptimismMintableERC721"
"IOptimismSuperchainERC20"

# Doesn't start with "I"
"MintableAndBurnable"
"KontrolCheatsBase"

# Currently inherit from interface, needs to be fixed.
"IWETH"
"IDelayedWETH"
"IResolvedDelegateProxy"
"IL2ToL2CrossDomainMessenger"
"ICrossL2Inbox"

# TODO: Kontrol interfaces that need to be removed
"IL1ERC721Bridge"
"IL1StandardBridge"
"IL1CrossDomainMessenger"
"ISuperchainConfig"
"IOptimismPortal"
# Solidity complains about receive but contract doens't have it.
"IResolvedDelegateProxy"
)

# Find all JSON files in the forge-artifacts folder
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,16 @@ import { IOptimismPortal } from "src/L1/interfaces/IOptimismPortal.sol";
import { ISystemConfig } from "src/L1/interfaces/ISystemConfig.sol";

interface IL1CrossDomainMessenger is ICrossDomainMessenger {
function PORTAL() external view returns (address);
function PORTAL() external view returns (IOptimismPortal);
function initialize(
ISuperchainConfig _superchainConfig,
IOptimismPortal _portal,
ISystemConfig _systemConfig
)
external;
function portal() external view returns (address);
function superchainConfig() external view returns (address);
function systemConfig() external view returns (address);
function portal() external view returns (IOptimismPortal);
function superchainConfig() external view returns (ISuperchainConfig);
function systemConfig() external view returns (ISystemConfig);
function version() external view returns (string memory);

function __constructor__() external;
Expand Down
15 changes: 6 additions & 9 deletions packages/contracts-bedrock/test/kontrol/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -122,23 +122,19 @@ The next step is to include tests for the newly included state updates in [`Depl

It might be necessary to set some of the existing tests from [`test`](../L1) as virtual because they can't be executed as is. See [`DeploymentSummary.t.sol`](deployment/DeploymentSummary.t.sol) for more concrete examples.

#### Add function signatures to [`KontrolInterfaces`](./proofs/interfaces/KontrolInterfaces.sol)

So far we've got all the state updates ready to be added to the initial configuration of each proof, but we cannot yet write any proof about the function. We still need to add the relevant signatures into `KontrolInterfaces`. The reason for having `KontrolInterfaces` instead of using directly the contracts is to reduce the amount of compiled contracts by Kontrol.
In the future there might interfaces for all contracts under `contracts-bedrock`, which would imply the removal of `KontrolInterfaces`.

#### Write the proof

Write your proof in a `.k.sol` file in the [`proofs`](./proofs/) folder, which is the `test` directory used by the `kprove` profile to run the proofs (see [Deployment Summary Process](#deployment-summary-process)). The name of the new proofs should start with `prove` (or `check`) instead of `test` to avoid `forge test` running them. The reason for this is that if Kontrol cheatcodes (see [Kontrol's own cheatcodes](https://github.com/runtimeverification/kontrol-cheatcodes/blob/master/src/KontrolCheats.sol)) are used in a test, it will not be runnable by `forge`. Currently, none of the tests are using custom Kontrol cheatcodes, but this is something to bear in mind.

To reference the correct addresses for writing the tests, first import the signatures as in this example:

```solidity
import {
IOptimismPortal as OptimismPortal,
ISuperchainConfig as SuperchainConfig
} from "./interfaces/KontrolInterfaces.sol";
import { IOptimismPortal as OptimismPortal } from "src/L1/interfaces/IOptimismPortal.sol";
import { ISuperchainConfig as SuperchainConfig } from "src/L1/interfaces/ISuperchainConfig.sol";
```

Declare the correspondent variables and cast the correct signatures to the correct addresses:

```solidity
OptimismPortal optimismPortal;
SuperchainConfig superchainConfig;
Expand All @@ -148,6 +144,7 @@ function setUp() public {
superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
}
```

Note that the names of the addresses come from [`DeploymentSummary.t.sol`](deployment/DeploymentSummary.t.sol) and are automatically generated by the [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh) script.

#### Add your test to [`run-kontrol.sh`](./scripts/run-kontrol.sh)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,8 @@ pragma solidity ^0.8.13;

import { DeploymentSummary } from "./utils/DeploymentSummary.sol";
import { KontrolUtils } from "./utils/KontrolUtils.sol";
import {
IL1CrossDomainMessenger as L1CrossDomainMessenger,
ISuperchainConfig as SuperchainConfig
} from "./interfaces/KontrolInterfaces.sol";
import { IL1CrossDomainMessenger as L1CrossDomainMessenger } from "src/L1/interfaces/IL1CrossDomainMessenger.sol";
import { ISuperchainConfig as SuperchainConfig } from "src/L1/interfaces/ISuperchainConfig.sol";

contract L1CrossDomainMessengerKontrol is DeploymentSummary, KontrolUtils {
L1CrossDomainMessenger l1CrossDomainMessenger;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,9 @@ pragma solidity ^0.8.13;
import { DeploymentSummary } from "./utils/DeploymentSummary.sol";
import { KontrolUtils } from "./utils/KontrolUtils.sol";
import { Types } from "src/libraries/Types.sol";
import {
IL1ERC721Bridge as L1ERC721Bridge,
IL1CrossDomainMessenger as CrossDomainMessenger,
ISuperchainConfig as SuperchainConfig
} from "./interfaces/KontrolInterfaces.sol";
import { IL1ERC721Bridge as L1ERC721Bridge } from "src/L1/interfaces/IL1ERC721Bridge.sol";
import { ISuperchainConfig as SuperchainConfig } from "src/L1/interfaces/ISuperchainConfig.sol";
import { ICrossDomainMessenger as CrossDomainMessenger } from "src/universal/interfaces/ICrossDomainMessenger.sol";

contract L1ERC721BridgeKontrol is DeploymentSummary, KontrolUtils {
L1ERC721Bridge l1ERC721Bridge;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,9 @@ pragma solidity ^0.8.13;
import { DeploymentSummary } from "./utils/DeploymentSummary.sol";
import { KontrolUtils } from "./utils/KontrolUtils.sol";
import { Types } from "src/libraries/Types.sol";
import {
IL1StandardBridge as L1StandardBridge,
IL1CrossDomainMessenger as CrossDomainMessenger,
ISuperchainConfig as SuperchainConfig
} from "./interfaces/KontrolInterfaces.sol";
import { IL1StandardBridge as L1StandardBridge } from "src/L1/interfaces/IL1StandardBridge.sol";
import { ISuperchainConfig as SuperchainConfig } from "src/L1/interfaces/ISuperchainConfig.sol";
import { ICrossDomainMessenger as CrossDomainMessenger } from "src/universal/interfaces/ICrossDomainMessenger.sol";

contract L1StandardBridgeKontrol is DeploymentSummary, KontrolUtils {
L1StandardBridge l1standardBridge;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,8 @@ pragma solidity ^0.8.13;
import { DeploymentSummary } from "./utils/DeploymentSummary.sol";
import { KontrolUtils } from "./utils/KontrolUtils.sol";
import { Types } from "src/libraries/Types.sol";
import {
IOptimismPortal as OptimismPortal,
ISuperchainConfig as SuperchainConfig
} from "./interfaces/KontrolInterfaces.sol";
import { IOptimismPortal as OptimismPortal } from "src/L1/interfaces/IOptimismPortal.sol";
import { ISuperchainConfig as SuperchainConfig } from "src/L1/interfaces/ISuperchainConfig.sol";
import "src/libraries/PortalErrors.sol";

contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,8 @@ pragma solidity ^0.8.13;
import { DeploymentSummaryFaultProofs } from "./utils/DeploymentSummaryFaultProofs.sol";
import { KontrolUtils } from "./utils/KontrolUtils.sol";
import { Types } from "src/libraries/Types.sol";
import {
IOptimismPortal as OptimismPortal,
ISuperchainConfig as SuperchainConfig
} from "./interfaces/KontrolInterfaces.sol";
import { IOptimismPortal as OptimismPortal } from "src/L1/interfaces/IOptimismPortal.sol";
import { ISuperchainConfig as SuperchainConfig } from "src/L1/interfaces/ISuperchainConfig.sol";
import "src/libraries/PortalErrors.sol";

contract OptimismPortal2Kontrol is DeploymentSummaryFaultProofs, KontrolUtils {
Expand Down

This file was deleted.