Evolution of `sym_n`

[shigoel]

sym_aggregate still aggregates the effects when the final state is reached, is that right? I meant aggregation of the effects in the middle of a long simulation (e.g., suppose we need to simulate 200 instructions and we'd like to aggregate the effects every 20 instructions -- we can invoke something like sym_n 20 at s0; sym_aggregate at s20). Would simp_all really be needed then (ref.: #133 (comment)) ? Could simp with axHyps at <h_s20> or some such not work?

Also, discussion for the future:

Another thing that is worth considering is having pre- and post-processing hooks in sym_n so that we can insert our own tactic blocks before and after the simulation of each instruction (e.g., tactics preceding the invocation of sym_n 1 at ... in the AbsVCGTandem proof). Can the while bit of sym_n can help with some of that already?

_Originally posted by @shigoel in #133 (comment)

[shigoel]

Closing: @alexkeizer discovered that intermediate aggregation is slow (#210). We'll work on other sym_n enhancements later when our use informs the design.