Module io 

Specification helpers for crate::mm::io.

The tracked VM I/O owner/view types live in crate::mm::io. This module only adds spec/proof impls for the exec reader/writer types.