Given a possibly mutable (and therefore unhardened) record, return a corresponding state record that acts identically for normal gets and sets, but is implemented using accessors, so it will be recognized as a state record.
Given a possibly mutable (and therefore unhardened) record, return a corresponding state record that acts identically for normal gets and sets, but is implemented using accessors, so it will be recognized as a state record.