structure Std.Internal.Do.WP.Frames {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {R : Type t} (op : R → Pred → Pred) (x : Prog) (F : R) : Prop

x frames the resource F with respect to the operator op : R → Pred → Pred: op F · commutes into the postcondition of wp x for every postcondition.

For the meet op = (· ⊓ ·) with R = Pred and stateful Pred, this means running x preserves the state identified by F. Other operators take a simpler resource, e.g. a cost counter R = Nat.

• conj_wp_le_wp_conj (Q : Value → Pred) (E : EPred) : Lean.Order.PartialOrder.rel (op F (wp x Q E)) (wp x (fun (a : Value) => op F (Q a)) E)

  When x frames (op F ·), (op F ·) commutes into the postcondition of wp x.

theorem Std.Internal.Do.WP.Frames.op_wp_upperAdjoint_le_wp {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {R : Type t} (op : R → Pred → Pred) [∀ (r : R), Lean.Order.PreservesSup (op r)] {x : Prog} {F : R} (hframes : Frames op x F) (Q : Value → Pred) (E : EPred) : Lean.Order.PartialOrder.rel (op F (wp x (fun (a : Value) => Lean.Order.PreservesSup.upperAdjoint (op F) (Q a)) E)) (wp x Q E)

The framed spec vcgen applies for x, when each op r preserves Sup: framing x by F makes op F (wp x (fun a => PreservesSup.upperAdjoint (op F) (Q a))) a precondition for wp x Q.

theorem Std.Internal.Do.WP.Frames.le_frameClosure {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {R : Type t} (op : R → Pred → Pred) [∀ (r : R), Lean.Order.PreservesSup (op r)] {x : Prog} (hframes : ∀ (r : R), Frames op x r) {Q : Value → Pred} {E : EPred} {pre : Pred} (hpre : Lean.Order.PartialOrder.rel pre (wp x Q E)) : Lean.Order.PartialOrder.rel pre (Lean.Order.PreservesSup.frameClosure op (fun (Q : Value → Pred) => wp x Q E) Q)

PreservesSup.le_frameClosure at the wp layer: when x frames every resource r, landing below wp x Q E suffices to land below the frame closure of wp x · E.

theorem Std.Internal.Do.WP.Frames.of_frameClosure {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {R : Type t} (op : R → Pred → Pred) [∀ (r : R), Lean.Order.PreservesSup (op r)] (comp : R → R → R) (hact : ∀ (r r' : R) (a : Pred), op (comp r r') a = op r (op r' a)) {x : Prog} {F : R} (h : ∃ (f : Prog → EPred → (Value → Pred) → Pred), ∀ (x : Prog) (Q : Value → Pred) (E : EPred), wp x Q E = Lean.Order.PreservesSup.frameClosure op (f x E) Q) : Frames op x F

If wp is built as PreservesSup.frameClosure op over a base post-transformer f x E (the frame rule internalized into wp), then every program frames every resource F with respect to op.

theorem Std.Internal.Do.WP.Frames.of_wp_conjunctive {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] [WPConjunctive Prog Value Pred EPred] {x : Prog} {F : Pred} (h : ∀ (E : EPred), Lean.Order.PartialOrder.rel F (wp x (fun (x : Value) => F) E)) : Frames (fun (x1 x2 : Pred) => Lean.Order.meet x1 x2) x F

If wp x is conjunctive, then x frames (F ⊓ ·) when F holds before and after running x.

@[instance_reducible]

noncomputable def Std.Internal.Do.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 PreservesSup.frameClosure of the base wp over a family of Sup-preserving resource operators op r that act by comp with unit e. The resource frame rule then holds by construction (WP.Frames.of_frameClosure).

Equations

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