Resourceful invariants and associated libraries

[aseemr]

With @nikswamy.

The PR adds support for resourceful invariants, getting rid of the reliance on the monotonicity-related axioms in Pulse Core. The use of these axioms for implementing invariants in Pulse Core has been troublesome because of how it interacts with strong excluded middle (see FStarLang/FStar#2814). To get around these issues, Pulse Core had to accommodate a new point "Unobservable" in its effect hierarchy and prohibit ghost code from allocating or using invariants.

Summary

Extending the stratified heap model in Pulse, this PR adds a new compartment to the heap that maps a new kind of reference, iref, to vprops. The compartment is monotonic (as in no freeing/updating of irefs once allocated) and an assertion of the form inv i p represents the knowledge that iref i points to vprop p. This is a duplicable invariant resource that may be eliminated with a with_invariant combinator.

Building on this change in the memory model, the PR implements these resourceful invariants all the way up to the Pulse checker and associated libraries (e.g., locks, mutex, trade, pledge, etc.).

Changes

Pulse Core

Pulse semantics is now based on a preorder state monad, rather than a monotonic state monad.

Following are the new additions to Pulse Core:

val iref : Type0
val iname_of (i:iref) : GTot iname
val inv (i:iref) (p:vprop) : vprop
val new_invariant (p:vprop { is_big p }) : stt_ghost iref emp_inames (requires p) (ensures fun i -> inv i p)

The stt_ghost effect is also indexed with the set if inames to indicate that the computation may open these invariants. Due to the stratified nature of the underlying memory, new_invariant requires that p is "big". This essentially means that p should not be a (inv i p) assertion itself. The PR augments libraries with support to prove is_big for common vprops.

The Unobservable effect is no longer there in Pulse.

Pulse Checker

{ pre }
with_invariant i
  returns x:a
  ensures post
  opens is { e }

Pulse typechecks this as follows:

• It tries to find an assertion of the form inv i p, for some p, in pre (by traversing the pre, descending into separating conjuncts recursively). Suppose pre ~ inv i p ** pre'.
• It then tries to find inv i p, for same p as in the previous step, in post. Suppose post ~ inv i p ** post'
• It typechecks the body (e) with pre = p ** pre' and post = p ** post', opens set as is \ { i }, and expected type as a.
• It checks that ((is \ { i }) $\cup$ { i }) $\subseteq$ is.
• The final type of the combinator is C a is pre post, where C is allowed to be ghost or atomic.

The annotations (returns, ensures, opens) are either present on the with_invariant block itself, or come from post hint propagation (via bidirectional typechecking).

To support both ghost and atomic with_invariant blocks with the same syntax, the checker has a EffectAnnotAtomicOrGhost expected effect.

Pulse Libraries and Examples

The main change is that working with invariants now requires explicit invariant resources. With the new design, the libaries now have:

• Pulse.Lib.SpinLock, with storable and freeable locks. One caveat is that lock liveness predicates cannot themselves be stored in locks.
• Similar changes to Pulse.Lib.Mutex.
• inames indexed trades and pledges.
• invlist-based small Trades with a slightly different API.

[aseemr]

The new iref type and associated inv resource.

[aseemr]

Effect annotation used to check with_invariants blocks, in case a post hint is not already present.

[aseemr]

returns annotation on with_invariants contains an opens also (defaults to emp_inames if absent).

[aseemr]

A couple of examples.