The optimization of caching the `_cached_subst` seems pretty unnecessary to me. As far as I can tell, it will only fire _if_ `_check_forget_pattern` is true, which should only happpen when we have `cheatcode_forget` at the top of the K cell, which only happens maybe once or twice a test? So we may set the cached result once, and use it once, but no more than that, in a given test. So it introduces state dependencies/synchronization between `can_take_custom_step` and `custom_step` for maybe less than a second of savings a single time in a proof.
Originally posted by @ehildenb in #899 (comment)