Higher level goal: Striving to eliminate non-standard models of `dss`

The reachability proofs of dss.md can be thought of as axiomatically defining the theory k-dss that is the dapp that is MCD. We are working with two standard models (we expect) to model this theory, [dss solidity]((https://github.com/makerdao/dss/) and dss solidity assembly.

To try to quantify and strive towards as much coverage as possible, or to try to quantize the extent to which k-dss defines MCD, it is helpful to consider what would be "non-standard" models of k-dss. In other words, what EVM bytecode could we imagine that might pass the test and still have unintended behavior?
Three obvious tasks remaining to make k-dss more of an exhaustive spec are https://github.com/dapphub/k-dss/issues/24, https://github.com/dapphub/k-dss/issues/12 and https://github.com/dapphub/k-dss/issues/16.

I think we could turn this into a really fun reverse bug bounty game

Start with dss.md and the three remaining tasks linked in issues 24, 12, and 16. Compare the standard Solidity and Solidity-assembly models, then investigate candidate non-standard EVM bytecode behaviors that could pass the k-dss tests; done means documenting or addressing such gaps toward a more exhaustive specification.