Add load events that except to read a certain byte

We add a new type of event which is like a relaxed load that expects
to read a certain value, causing it to act like an "assertion".

For this to work, we now require the From-Read axiom to be enabled
when we encode the memory axioms with our symbolic memory::Refinement
checking algorithm. This further increases the precision of the program
that appears on the RHS of the refinement check. This is particularly
useful for modelling purposes when we want to precisely describe the
happens-before ordering that can lead to a concurrency-related bug.

The new "assertion events" can be also used to model more precisely
mutually exclusive control flow such as if-then-else statements.