Checking only read permissions when asserting function preconditions

[marcoeilers]

Changes the meaning of permission amounts in functions:

• When checking function preconditions, concrete permission amounts are ignored; instead, we only distinguish between zero and any positive amounts. Thus, the following assertions all have the same meaning in a function precondition: acc(x.f, write) or acc(x.f, wildcard) or acc(x.f, 1/2) or acc(x.f, b ? write : 1/2) or acc(x.f) && acc(x.f) or acc(x.f, 2/1) all just require checking that a caller has some positive permission amount to x.f. The same is true for predicate permissions.
• However, we still distinguish between zero and positive amounts. Thus, acc(x.f, b ? write : none) is equivalent to acc(x.f, b ? 1/2 : none) and acc(x.f, b ? wildcard : none) but not to acc(x.f, write) or acc(x.f, none).
• As a result, inside a function, we can no longer assume non-aliasing based on permission amounts.
• Additionally, when verifying well-definedness of a function, again all permission amounts are ignored (with the exception of distinguishing between zero and something positive as stated before), so I can for example unfold a whole predicate inside a function whose precondition only asks for half that predicate.

The corresponding changes in Silver warn clients who rely on the current behavior, and we provide an alternative:

• Clients that used function applications to check for specific permission amounts can use the new asserting expression instead.
• Silver outputs warnings when concrete fractions are used anywhere inside a function, since they are always meaningless (but not wrong)
• acc(x.f, b ? wildcard : none) is now allowed only in functions (previously, any complex expressions involving wildcards were always forbidden).
• The old behavior can be enabled via the new --respectFunctionPrePermAmounts command line option

The implementation in Silicon should be more efficient than just substituting wildcards everywhere:

• The implementation in Silicon adds a new flag to the state that expresses whether only read permission should be asserted. In that mode, we also no longer remove permission from the heap when consuming permissions, and we produce chunks with the amount written in the program; we do not introduce additional wildcards anywhere.
• Additionally, assuming permission upper bounds is simply disabled inside functions.

[jcp19]

I did not notice any major problems. I have a question and a small suggestion to avoid warnings. To be clear I understand this, for the program

function f(x: Ref): Int
    requires acc(x,f, 2/3)
    requires acc(x,f, 2/3)
{ ... }

in the new interpretation, this is safe to call whenever we have any permission to x.f, and this precondition does not imply false, right?