[Feature-request]: NFT minting properties

[aviggiano]

Describe the desired feature or improvement

I am reviewing a smart contract that contains a very complex logic to mint NFTs with random rarities using Chainlink VRF. Just by reading the code it is hard to understand if it correctly implements the specification. It would be nice to have pre-built echidna properties to test invariants.

In my particular example, the invariants are rather commonplace to other NFT projects, which is why I believe these are generic enough to be applied to other smart contracts:

• max NFTs per wallet: no user can have more NFTs than the max
• max NFTs minted: total supply must not exceed the max
• max NFTs per project owner: the project owner cannot have more than the max
• NFT price (in Ether, but can be extended to ERC-20 too): minting an NFT must cost exactly the NFT price
• NFT rarity: the number of NFTs minted for a given rarity must match their assigned percentages, within an error margin
• whitelist: no user can mint NFTs if they are not on the whitelist
• etc

If you think this is useful I can work on these properties and submit a PR.