@@ -115,12 +115,6 @@ The `runKontrolDeployment` function of [`KontrolDeployment`](./deployment/Kontro
...
@@ -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).
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 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.
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.
Note that the names of the addresses are automatically generated by the [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh) script.
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)
#### Add your test to [`run-kontrol.sh`](./scripts/run-kontrol.sh)
...
@@ -155,7 +148,6 @@ As described in [Execute Proofs](#execute-proofs), there's a `script` mode for s
...
@@ -155,7 +148,6 @@ As described in [Execute Proofs](#execute-proofs), there's a `script` mode for s
### Assumptions
### Assumptions
1. A critical invariant of the `KontrolDeployment.sol` contract is that it stays in sync with the original `Deploy.s.sol` contract.
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.
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.
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.