On Thu, Oct 10, 2024 at 3:52 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > On Thu, 2024-10-10 at 15:40 -0700, Eduard Zingerman wrote: > > > I think this would bring significant speedup. > > Not sure it would completely fix the issue at hand, > > as mark_chain_precision() walks like 100 instructions back on each > > iteration of the loop, but it might be a step in the right direction. > > In theory, we can do mark_chain_precision() lazily: > - mark that certain registers need precision for an instruction; > - wait till next checkpoint is created; > - do the walk for marked registers. > > This should be simpler to implement on top of what Andrii suggests. Indeed it can wait until the next new_state, since when the next iteration of the loop starts the sl->state are guaranteed to be some olderstates. Though the verifier may have done multiple loop iteration traversals, but it's still in 'cur' state, so states_equal(env, &sl->state, cur...) should still be correct.
