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.

Sign up for GitHub

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

test-kontrol: optimize the doc #12065

Merged
merged 4 commits into from
Oct 24, 2024
+1 −9
Merged

test-kontrol: optimize the doc #12065

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
68d6f13
optimize the doc
rickck11 Sep 23, 2024
d1f4cac
small fix
rickck11 Oct 7, 2024
602553d
Resolved merge conflicts
rickck11 Oct 23, 2024
690383a
reomve outdated content
rickck11 Oct 23, 2024
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
10 changes: 1 addition & 9 deletions packages/contracts-bedrock/test/kontrol/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,12 +115,6 @@ The `runKontrolDeployment` function of [`KontrolDeployment`](./deployment/Kontro

Once new deployment steps have been added to `runKontrolDeployment` the state-diff files have to [be rebuilt](#build-deployment-summary).

#### Include existing tests on the new state-diff recorded bytecode

The next step is to include tests for the newly included state updates in [`DeploymentSummary.t.sol`](deployment/DeploymentSummary.t.sol). These tests inherit the tests from [`test`](../L1) of the contracts deployed by `runKontrolDeployment`. This ensures that deployment steps were implemented correctly and that the state updates are correct.

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.

#### 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.
Expand All @@ -143,8 +137,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.
Note that the names of the addresses 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 All @@ -155,7 +148,6 @@ As described in [Execute Proofs](#execute-proofs), there's a `script` mode for s
### Assumptions

1. A critical invariant of the `KontrolDeployment.sol` contract is that it stays in sync with the original `Deploy.s.sol` contract.
Currently, this is partly enforced by running some of the standard post-`setUp` deployment assertions in `DeploymentSummary.t.sol`.
A more rigorous approach may be to leverage the `ChainAssertions` library, but more investigation is required to determine if this is feasible without large changes to the deploy script.

2. Size of `bytes[]` arguments. In [`OptimismPortal.k.sol`](./proofs/OptimismPortal.k.sol), the `prove_proveWithdrawalTransaction_paused` proof is broken down into 11 different proofs, each corresponding to a different size of the `_withdrawalProof` argument, which is of type `bytes[]`. We execute the same logic for lengths of `_withdrawalProof` ranging from 0 to 10, setting the length of each symbolic `bytes` element to 600.
Expand Down