Verifier is unsound for bad specs involving method calls with equi-imprecise preconditions; discussion in Conrad's paper

[jennalwise]

The issue and solutions are discussed in great detail by @conradz at this link: https://gist.github.com/conradz/c227622c3055878300e3d99e4935d2f9 And in her submitted POPL paper, this issue and solutions are discussed again (TODO: update with link once paper is public).

The solutions that I am implementing with pros and cons are:

Option 1: Implement returning the frame at method calls (which is computed already, just needs translated) in the backend to the frontend and the frontend uses that information to only pass what is not in the frame to the callee; this calculation would only happen when the precondition of the callee is equi-recursively imprecise but iso-recursively precise

• Pros:
  • Preserves iso-recursive interpretation of predicates in the backend
  • Optimistic static verification closer to OOPSLA20 paper than the next option
  • Proven sound
  • Implementing translation of the frame will help with implementing translation of separation checks
• Cons:
  • Harder to implement than the other option
  • Complicates run-time check implementation for OwnFields in frontends by requiring this special case
  • Increases run-time over head for passing permissions at method calls, but in a very specific case
  • Likely far more expensive than the other option (not 100% clear though)

Option 2: Consume all permissions at method calls, when the precondition is equi-recursively imprecise but iso-recursively precise all in the backend

• Pros:
  • Easy to implement
  • Keeps everything to the backend which makes frontend implementations cleaner
  • Likely less expensive at run-time (not 100% clear though)
• Cons:
  • Breaks iso-recursive precision interpretation in backend
  • Creates more run-time checks from assertions than would like; not as much optimization with statically available information as we would like
  • Breaks the semantics of ? as specified in [Wise et al. 2020] since no logically-consistent strengthening of the imprecise predicate allows it to include permissions allocated after its body is folded for the example where soundness is broken
  • Not proven sound

[jennalwise]

As a follow-up investigation, Option 2 does seem sound and adheres to the gradual guarantee as long as equi-imprecision introduces imprecision after consumption. The semantics are still not ideal.

Currently, I have implemented this solution (https://github.com/gradual-verification/silicon-gv/commit/b1a75b68c88b4bcbac8452d47bda33064d38c492) and I am in the process of testing it and then evaluating its performance.

[jennalwise]

Update for Option 2: The fix also must apply to loops as well as method calls (implemented here: https://github.com/gradual-verification/silicon-gv/commit/c0ae1054222d073edeea554360b96d656c257ff2). Basically, anywhere, where a frame off occurs during verification and code may be modified in the part not represented by the frame needs the fix for Option 2. I applied the fix only to loops and method calls. Any other consumes, such as at the end of method and loop bodies, at asserts, at field assignments, and in folds and unfolds do not require it and can be optimized.

It is possible to apply this functionality in these other places without issue; so it is okay to put the functionality in consume in general. Although, it doesn't make sense to apply it at unfolds, so a special case for that should be added. The only affect this would have is on un-optimizing folds and creating instances where static verification succeeds more often when folds and unfolds are missing at the cost of more run-time overhead (this is also at the cost of likely making it harder to see how to get to a full static solution with the full set of folds and unfolds).