We are consider a three-point lattice of Ghost < Unobservable < Atomic and indexing a new Pulse computation type with these labels as follows:
type label = Ghost | Unobservable | Atomic
val stpoly (a:Type) (_:inames) (_:label) (pre:vprop) (post: a -> vprop)
The bind for stpoly behaves like a graded monad on this label.
st_poly a _ Atomic _ _ can be promoted to stt unconditionally.
st_poly a _ (Ghost| Unobservable) _ _ can be promoted to Atomic if a is non-informative.
new_invariant is Unobservable.
with_invariant both is always at least in Unobservable (never Ghost), but may be Atomic if its body is.
Ghost (and only it) is also treated as an erasable effect, meaning that it composes with FStar.Ghost.
The distinction between Ghost/Atomic should be obvious.
The need for Unobservable comes up because we want to prevent the use of ghost axioms to create invariants, as in FStar issue FStarLang/FStar#2814
Reflecting a conversation with @mtzguido
We are consider a three-point lattice of Ghost < Unobservable < Atomic and indexing a new Pulse computation type with these labels as follows:
The bind for stpoly behaves like a graded monad on this label.
st_poly a _ Atomic _ _can be promoted to stt unconditionally.st_poly a _ (Ghost| Unobservable) _ _can be promoted to Atomic if a is non-informative.new_invariantis Unobservable.with_invariantboth is always at least in Unobservable (never Ghost), but may be Atomic if its body is. Ghost (and only it) is also treated as an erasable effect, meaning that it composes with FStar.Ghost.The distinction between Ghost/Atomic should be obvious. The need for Unobservable comes up because we want to prevent the use of ghost axioms to create invariants, as in FStar issue FStarLang/FStar#2814