I had some trouble updating the proof of print_mults_sat_spec in extra/StateIOTrace.v. Either something is getting unfolded too much by the dependent induction earlier, or the monad change requires an extra proof of Proper for the setoid rewrite.

This is very helpful, thanks! I'll take a closer look at the proof you mention tomorrow.

Something about the switch to a record makes controlling unfolding a lot more annoying. I marked interp_state as simpl never as a cludgy fix but it also causes some issues.

The root cause of the failure is still mysterious to me but I managed to fix the proof. dependent induction does too much unfolding now. We want to keep interp_state handleIOState folded as long as possible, so I abstract it away with remember then revert the equation into the goal because dependent induction was still trying to use the equation to undo the remember.

when updating the tutorial, there seems to be a somewhat significant decision to make about whether the interp_asm and interp_imp functions should expose the stateT or produce an interface like the current one that returns a function that takes the state like they currently do.

I don't think I rely on the stateT abstraction in the tutorial, so try removing it from the result of interp_asm and interp_imp.