Framing for a monadic wp #
WPMonad.of_frameClosure 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.of_frameClosure
{m : Type → Type}
[Monad m]
{P : Type u}
{E : Type z}
[Assertion P]
[Assertion E]
{R : Type}
(op : R → P → P)
[∀ (r : R), Lean.Order.PreservesSup (op r)]
{comp : R → R → R}
{e : R}
(hact : ∀ (r r' : R) (a : P), op (comp r r') a = op r (op r' a))
(hunit : ∀ (a : P), op e a = a)
(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.
The resource frame rule then holds by construction (WP.Frames.of_frameClosure).
A separation logic depends on this property: every frame op r passes through the wp of every
program. 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.