Skip to content

N
nebula
Commit 31ac6d98 authored by Mark Tyneway's avatar Mark Tyneway
Browse files
Options

contracts-bedrock: generate invariant docs

parent ad928de2
Show whitespace changes
Inline Side-by-side
Showing with 9 additions and 9 deletions
packages/contracts-bedrock/invariant-docs/OptimismPortal.md
View file @ 31ac6d98
...@@ -19,6 +19,6 @@ This invariant asserts that there is no chain of calls that can be made that wil ...@@ -19,6 +19,6 @@ This invariant asserts that there is no chain of calls that can be made that wil
## Deposits of any value should always succeed unless `_to` = `address(0)` or `_isCreation` = `true`. ## Deposits of any value should always succeed unless `_to` = `address(0)` or `_isCreation` = `true`.
**Test:** [`FuzzOptimismPortal.sol#L41`](../contracts/echidna/FuzzOptimismPortal.sol#L41) **Test:** [`FuzzOptimismPortal.sol#L62`](../contracts/echidna/FuzzOptimismPortal.sol#L62)
All deposits, barring creation transactions and transactions sent to `address(0)`, should always succeed. All deposits, barring creation transactions and transactions sent to `address(0)`, should always succeed.
packages/contracts-bedrock/invariant-docs/ResourceMetering.md
View file @ 31ac6d98
# `ResourceMetering` Invariants # `ResourceMetering` Invariants
## The base fee should increase if the last block used more than the target amount of gas ## The base fee should increase if the last block used more than the target amount of gas
**Test:** [`FuzzResourceMetering.sol#L139`](../contracts/echidna/FuzzResourceMetering.sol#L139) **Test:** [`FuzzResourceMetering.sol#L160`](../contracts/echidna/FuzzResourceMetering.sol#L160)
If the last block used more than the target amount of gas (and there were no empty blocks in between), ensure this block's baseFee increased, but not by more than the max amount per block. If the last block used more than the target amount of gas (and there were no empty blocks in between), ensure this block's baseFee increased, but not by more than the max amount per block.
## The base fee should decrease if the last block used less than the target amount of gas ## The base fee should decrease if the last block used less than the target amount of gas
**Test:** [`FuzzResourceMetering.sol#L150`](../contracts/echidna/FuzzResourceMetering.sol#L150) **Test:** [`FuzzResourceMetering.sol#L171`](../contracts/echidna/FuzzResourceMetering.sol#L171)
If the previous block used less than the target amount of gas, the base fee should decrease, but not more than the max amount. If the previous block used less than the target amount of gas, the base fee should decrease, but not more than the max amount.
## A block's base fee should never be below `MINIMUM_BASE_FEE` ## A block's base fee should never be below `MINIMUM_BASE_FEE`
**Test:** [`FuzzResourceMetering.sol#L160`](../contracts/echidna/FuzzResourceMetering.sol#L160) **Test:** [`FuzzResourceMetering.sol#L181`](../contracts/echidna/FuzzResourceMetering.sol#L181)
This test asserts that a block's base fee can never drop below the `MINIMUM_BASE_FEE` threshold. This test asserts that a block's base fee can never drop below the `MINIMUM_BASE_FEE` threshold.
## A block can never consume more than `MAX_RESOURCE_LIMIT` gas. ## A block can never consume more than `MAX_RESOURCE_LIMIT` gas.
**Test:** [`FuzzResourceMetering.sol#L170`](../contracts/echidna/FuzzResourceMetering.sol#L170) **Test:** [`FuzzResourceMetering.sol#L191`](../contracts/echidna/FuzzResourceMetering.sol#L191)
This test asserts that a block can never consume more than the `MAX_RESOURCE_LIMIT` gas threshold. This test asserts that a block can never consume more than the `MAX_RESOURCE_LIMIT` gas threshold.
## The base fee can never be raised more than the max base fee change. ## The base fee can never be raised more than the max base fee change.
**Test:** [`FuzzResourceMetering.sol#L181`](../contracts/echidna/FuzzResourceMetering.sol#L181) **Test:** [`FuzzResourceMetering.sol#L202`](../contracts/echidna/FuzzResourceMetering.sol#L202)
After a block consumes more gas than the target gas, the base fee cannot be raised more than the maximum amount allowed. The max base fee change (per-block) is derived as follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR` After a block consumes more gas than the target gas, the base fee cannot be raised more than the maximum amount allowed. The max base fee change (per-block) is derived as follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR`
## The base fee can never be lowered more than the max base fee change. ## The base fee can never be lowered more than the max base fee change.
**Test:** [`FuzzResourceMetering.sol#L192`](../contracts/echidna/FuzzResourceMetering.sol#L192) **Test:** [`FuzzResourceMetering.sol#L213`](../contracts/echidna/FuzzResourceMetering.sol#L213)
After a block consumes less than the target gas, the base fee cannot be lowered more than the maximum amount allowed. The max base fee change (per-block) is derived as follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR` After a block consumes less than the target gas, the base fee cannot be lowered more than the maximum amount allowed. The max base fee change (per-block) is derived as follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR`
## The `maxBaseFeeChange` calculation over multiple blocks can never underflow. ## The `maxBaseFeeChange` calculation over multiple blocks can never underflow.
**Test:** [`FuzzResourceMetering.sol#L203`](../contracts/echidna/FuzzResourceMetering.sol#L203) **Test:** [`FuzzResourceMetering.sol#L224`](../contracts/echidna/FuzzResourceMetering.sol#L224)
When calculating the `maxBaseFeeChange` after multiple empty blocks, the calculation should never be allowed to underflow. When calculating the `maxBaseFeeChange` after multiple empty blocks, the calculation should never be allowed to underflow.
packages/contracts-bedrock/invariant-docs/SystemConfig.md
View file @ 31ac6d98
# `SystemConfig` Invariants # `SystemConfig` Invariants
## The gas limit of the `SystemConfig` contract can never be lower than the hard-coded lower bound. ## The gas limit of the `SystemConfig` contract can never be lower than the hard-coded lower bound.
**Test:** [`SystemConfig.t.sol#L39`](../contracts/test/invariants/SystemConfig.t.sol#L39) **Test:** [`SystemConfig.t.sol#L49`](../contracts/test/invariants/SystemConfig.t.sol#L49)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment