Checking only read permissions when asserting function preconditions

[marcoeilers]

Carbon implementation of the changes described here: viperproject/silicon#877

In the Carbon implementation

• 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