docs: properties for invariant testing

[0xteddybear]

I'm not quite sure how to go about specifying the invariants for supERC20, since:

• the ethereum-optimism/optimism repo in packages/contracts-bedrock already has invariant tests, but written in foundry
• invariants are programatically generated from the @Custom:invariant tags in code, and we're gonna write invariant defs before their test code

any feedback is welcome ✨

[0xDiscotech]

Suggested change

	| 4 | sum of total supply across all chains is always `<=` to `convert()`ed amount | | |
	| 4 | sum of total supply across all chains is always `<=` to `convert()`-ed and `mint()`-ed amount | | |

[0xteddybear]

I'm not sure I follow you on this one, what mint() are you referring to?

with this property I'm trying to describe the high-level behaviour of the whole system, where the only place where tokens can be minted should be inside convert

I guess we could also define a separate 'Valid State' property local to the supERC20 where we check total supply is the sum of all mints, if we don't get that for free by including ToB ERC20 properties

[0xDiscotech]

I'm referring to the OptimismSuperchainERC20#mint function, that is only callable by the standard bridge on the L1 -> L2 flow.
Should we take that into consideration when defining the total amount of the token invariant?

[0xDiscotech]

Suggested change

	| 0 | calls to sendERC20 succeed as long as caller has enough balance | | |
	| 0 | calls to `sendERC20` succeed as long as caller has enough balance | | |

[0xDiscotech]

Suggested change

	| 1 | sendERC20 decreases the token's totalSupply in the source chain | | |
	| 2 | relayERC20 increases the token's totalSupply in the destination chain | | |
	| 3 | only calls to `convert()` can increase the total supply across chains | | |
	| 1 | `sendERC20` decreases the token's total supply in the source chain | | |
	| 2 | `relayERC20` increases the token's total supply in the destination chain | | |
	| 3 | only calls to `convert()` and `mint()` can increase the total supply across chains | | |

[0xDiscotech]

The invariant wouldn't be something like

Suggested change

	| 6 | supERC20 token address does not depend on chainID | | |
	| 6 | supERC20 token addresses are the same in all the different chains | | |

?

[0xteddybear]

I believe this is currently clearer to map to a halmos proof, like so:

check_addressDoesNotDependOnChainId(remote, name, symbol, decimals, chainId1, chainID2){
  vm.assume(chainId1 != chainId2);
  assertEq(factory.deploy(remote, name, symbol, chainId1),  factory.deploy(remote, name, symbol, chainId2));
}

wdyt? it certainly feels math-ier

[0xDiscotech]

ah perfect, if that's simpler for halmos let's keep like that