An external representation for non-generative, non-opaque records (allowing simple serialization and deserialization) is now specified in my latest commit (in the personal repo).
