search

FStarLang / steel

The Steel separation logic library for F*
Apache License 2.0
31 stars 5 forks source link

Returning terms in Neutral or Ghost; propagating effect annotations; joining computation types of branches #167

Closed nikswamy closed 9 months ago

nikswamy commented 9 months ago

This PR fixes issues #162, #151, and #77. The root causes of the issues are all intertwined.

  1. We now return pure terms in Neutral and ghost terms in stt_ghost, adding pure equality refinements in the postcondition. This removes the equality refinement types that we were adding on returned terms, which lead to issues like #77. Also, returning terms in their least effect also solves issue #151, allowing lemmas to be called in Ghost code.

  2. Adding this uncovered a problem in the way we were handling the inference of the opens annotation in atomic code. Two atomic computations can only be composed when they (are subsumed to) open the same invariants. Returning terms in Neutral in atomic contexts then requires applying this subsumption rule and figuring out which set of inames to subsume to becomes an issue---we can't simply use the opens annotation on the continuation, since this may reference names that are not in scope.

    So, to solve this, we now propagate effect annotations, notable EffectAnnotAtomic { opens } in the post_hint, and the checker is proven to respect such annotations: i.e., the result of the checker is always STT_Atomic _ opens when the effect annotation is set as above, and that opens index is guaranteed to be well-typed in the proper scope. Note, the observability flag of an atomic computation is always inferred, rather than set in the annotation. This is because although the top-level annotation may be, say, atomic, it is often the case that the tail of the computation is in some smaller effect, e.g., neutral or unobservable.

  3. Finally, bug #162 was uncovered by a failure in Pulse.Lib.InvList, which was failing due to the scoping issue described in 2. But, now, with the proper scopes enforced, and with a fix to take the join of the computed types, notably taking a join of their observabilities, in case the branches are all stt_atomic.

nikswamy commented 9 months ago

Some more description of how the effect annotations are propagated:

One interesting thing is how to propagate effect annotations into the body of with_invariant blocks.

Say you have with_invariant (i) { body }:

If the effect annotation is EffectAnnotAtomic { opens } then the body is checked with annotation EffectAnnotAtomic { remove_inv opens i } to ensure that i is not opened within body. The inferred effect of the whole term is then add_inv (remove_inv opens i) i and we check with an SMT query that this term is included in opens.

If the effect annotation is EffectAnnotSTT, i.e., the context is not annotated as atomic, then we first check the whole term with the annotation EffectAnnotAtomic { opens=all_inames }, i.e., the universe of all inames---the inferred type of the with_invariant i { body } term is then stt_atomic _ all_inames which we then promote to STT.