If you modify a segment which contains a math symbol definition or $f statement, the definition of the math symbol is re-added, which currently bumps the version number even if it wasn't changed, causing all segments which use that symbol to be re-evaluated. We can instead detect re-adding exactly the same definition and keep the version the same for that slot. This happens for labels as well, but with current usage patterns there are no cross-segment dependencies on the label index.
Our symbol records track the in-segment index for $c$v$f statements, so adding new statements before one of those three types within a segment will invalidate the index even with the previous fixed.
$c and $v positions are used by scopeck to determine if the definitions are in scope. Since we don't need to track intra-segment dependencies anyway (scopeck runs at a segment granularity, and probably always will), this can be interpreted as only using the segment ID part of the address, and we could make the version number coarser. (Diagnostics will require additional work.)
$f positions are used as above, and also we need to sort by them in order to correctly determine hypothesis order. We could use an order-maintenance structure for this, or punt.
If scopeck runs on a segment, all statements in that segment will have their frame version bumped, resulting in unnecessary re-verifications. We can avoid that using comparisons as for the math symbol case above.
scopeck currently embeds the statement address of the final statement and all hypotheses in the generated frame. This was intended as a measure to support EXPLICIT format, but it also means that adding new statements to a segment will cause all later statements to appear to have changed. To fix this, we'll need an alternate approach for EXPLICIT; ideally nameck would generate Atoms for labels as well as math symbols, but that needs to be optimized if we are going to use it in one-shot mode.
verify currently runs at a segment granularity. Unlike scopeck, there is no computation shared between statements so there's much less reason to do a strict segment granularity; we could modify scopeck to output a list of changed frames when the change canary trips, and use that to detect which statements require reverification. Doing this without substantially worsening the worse case may be tricky.
$fstatement, the definition of the math symbol is re-added, which currently bumps the version number even if it wasn't changed, causing all segments which use that symbol to be re-evaluated. We can instead detect re-adding exactly the same definition and keep the version the same for that slot. This happens for labels as well, but with current usage patterns there are no cross-segment dependencies on the label index.$c$v$fstatements, so adding new statements before one of those three types within a segment will invalidate the index even with the previous fixed.$cand$vpositions are used by scopeck to determine if the definitions are in scope. Since we don't need to track intra-segment dependencies anyway (scopeck runs at a segment granularity, and probably always will), this can be interpreted as only using the segment ID part of the address, and we could make the version number coarser. (Diagnostics will require additional work.)$fpositions are used as above, and also we need to sort by them in order to correctly determine hypothesis order. We could use an order-maintenance structure for this, or punt.