Framing for a monadic wp

WPMonad.withFrameClosure reinterprets a WPMonad through the Lean.Order.PredTrans.frameClosure of its base weakest precondition, so that every program frames every resource.

@[instance_reducible]

noncomputable def Std.WP.WPMonad.withFrameClosure {m : Type → Type} [Monad m] {P : Type u} {E : Type z} [Assertion P] [Assertion E] {R : Type} (op : R → P → P) {opE : R → E → E} [Lean.Order.FrameOp op E opE] {comp : R → R → R} {e : R} (hact : ∀ (r r' : R) (a : P), op (comp r r') a = op r (op r' a)) (hactE : ∀ (r r' : R) (E' : E), opE (comp r r') E' = opE r (opE r' E')) (hunit : ∀ (a : P), op e a = a) (hunitE : ∀ (E' : E), opE e E' = E') (base : WPMonad m P E) : WPMonad m P E

Reinterpret a WPMonad m so its weakest precondition is the frameClosure of the base wp over a family of supremum-preserving resource operators op r that act by comp with unit e. Every program then frames every resource (WP.frames_of_frameClosure).

A separation logic depends on this property: every frame op r passes through the wp of every program in every state. A caller of a spec picks a frame and applies the frame rule for that frame.

Equations

• One or more equations did not get rendered due to their size.