Skip to content

Commit

Permalink
maint(ct): remove Kontrol interfaces (#12178)
Browse files Browse the repository at this point in the history
We no longer need these interfaces now that we have the actual
interfaces.
  • Loading branch information
smartcontracts authored Sep 27, 2024
1 parent b1dfd74 commit 5eaac1d
Show file tree
Hide file tree
Showing 9 changed files with 40 additions and 134 deletions.
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.

0 comments on commit 5eaac1d

Please sign in to comment.