Experiment with unassume for mutex analysis

[sim642]

This is a quick proof-of-concept for an idea I had a while ago: unassume for variable protection in mutex analysis. It is the first example of a non–value-domain unassume operator.

To do so, this also implements the custom protected_by YAML witness entry type from our COOP 2023 talk, including generation and validation. On test 13/01 it reduces evals 23 → 19, so it conceptually seems to work (even in a trivial case!). But this needs more evaluation to see its potential.

TODO

• [ ] Add (cram?) tests.
• [ ] Experiment on larger (pthread) programs.
• [ ] Add location_mutex entry type as well.