ditto feat: spec for formal verification

Since our contract is small, we should be able to use formal verification to prove correctness (Certora).

Don't have much experience in this, but I can take a look.

Mar 10 '22 17:03 0xbok

We can explore manticore https://github.com/trailofbits/manticore https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/manticore

May 25 '22 18:05 0xbok

started on manticore.

Oct 04 '22 14:10 0xbok

@calvbore i think before we explore these tools, it would be good to have some specs we want to test against. Few thing we should formally verify:

Linked list manipulation is correct.
Oracle updates are correct.
Each ERC20 token in DittoMachine's balance can be claimed eventually, i.e., tokens are not permanently locked in the contract.
NFT transfer to DittoMachine never locks NFT in the contract, is always sold to protoId.
Dissolve works correctly.

We should think of how to translate them into sensible rules.

Oct 04 '22 14:10 0xbok