More Precise Location for Verus?

[yizhou7]

One thing that came up in a discussion with @jialin-li is that, we currently can only figure out which procedure is unstable in Verus. Given a procedure $P$, it is not clear if the instability is because of:

• an assertion in $P$
• post-condition of $P$
• pre-condition of a call in $P$

This might be a nice to have feature?

[parno]

Might be nice in the long term, but it seems like a difficult task, since Verus (typically) only generates a single query per function that incorporates all of the above. You could potentially break down the query into smaller pieces, but then you've perturbed the goal query, which may lead to confusing results; it seems quite likely that the instability of the whole may not be measurable by studying the instability of the parts.