test-kontrol: optimize the doc (ethereum-optimism#12065)

* optimize the doc

* small fix

* reomve outdated content

packages/contracts-bedrock/test/kontrol/README.md

@@ -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.
@@ -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)
 
@@ -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.