we add a flag to the permission module's state that expresses whether we should consume concrete permission amounts, the default behavior, or just assert read permission without changing the mask,
the flag is set when verifying a function and when exhaling a function precondition,
to avoid assuming non-aliasing from permission amounts when verifying a function, we change the axiom that limits field permissions to one to be conditional on a new global flag, and assume this flag is true only when verifying predicates or methods
Carbon implementation of the changes described here: https://github.com/viperproject/silicon/pull/877
In the Carbon implementation