0xbok

Change $a / b: (a \cdot b^{(p^{2-2})})$ % $p$ to $a / b: (a \cdot b^{(p^2-2)})$ % $p$

- manual review - invariants and invariant testing - formally verify?

- [ ] Readme file - [ ] ditto book

There is no documentation yet https://github.com/foundry-rs/book/issues/497, but here are some resources from foundry telegram: - See `testdata/fuzz/invariants`: https://github.com/foundry-rs/foundry/pull/1572/files#diff-da66ab1e15a3f7ae06235ce6c905ac28f2bd5fba8702f7c64a6a5114166b2d68 - https://github.com/maple-labs/revenue-distribution-token/tree/add-forge-invariants

echidna is not able to deploy the contract: ``` echidna-test --test-mode assertion --config src/test/echidna/echidna.config.yaml --contract DittoMachineEchidna src/test/echidna/DittoMachineEchidna.sol ``` ``` Analyzing contract: DittoMachineEchidna.sol:DittoMachineEchidna echidna-test: Deploying the contract 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 failed (revert, out-of-gas,...

Hardcoded gas limit can break on future gas cost change

4

https://github.com/ditto-lab/ditto/blob/2dd8b7f20a0f223160466a8d2953551a796c5306/src/DittoMachine.sol#L592

feat: spec for formal verification

3

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.

TODO - Tests to verify all these cases.