Flow-insensitive YAML witness invariants

[sim642]

This adds the generation of non-standard flow_insensitive_invariant entries to YAML witnesses. Base privatizations are extended to emit such invariants based on their internal unprotected/weak values.

TODO

• flow_insensitive_invariant checking validation? Too inefficient, would have to evaluate such invariant at every node in every context.
• Invariants from earlyglobs? Works automatically, because earlyglobs delegates to base privatization.
• Flow-insensitive invariants for singlethreaded non-earlyglobs?

[michael-schwarz]

Actually, does this account for modifications to the values of globals before multi-threaded mode is entered if earlyglobs is off?

[sim642]

No, and that's what the third task above would be about. That could be fixed by doing the earlyglobs side effects even when it's disabled, but still reading values from the local state in singlethreaded mode, such that the flow-insensitive invariant would be correct.

I don't want to introduce that extra complication right now though, because these flow-insensitive invariants aren't too useful for self-validation (we don't want to evaluate/unassume such expressions at every point, that would be hugely expensive). I'll restrict the generation of these to only when earlyglobs is enabled for now, because this PR also contains other fixes/refactorings to base's invariant generation that are still required for #833, etc.