Iris Library Best Practices
We should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered form. Other aspects are not mentioned; @Blaisorblade pointed out that it is non-obvious that specs should not contain own but instead wrap those things in their own definitions that depend on libG instead of inG.