Framing at the wp layer

WP.Frames op x F states that the program x commutes op F · into the postcondition of wp x. A WP built as the Lean.Order.PredTrans.frameClosure of a base wp frames every resource by construction.

The monadic counterpart, which builds a WPMonad from the frame closure of a base interpretation, is in Std.WP.Monad.Frame.

structure Std.WP.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.

• op_wp_le_wp_op (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.WP.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 suprema: 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.WP.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.PredTrans.frameClosure op (wpTrans x)).apply Q E)

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.WP.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 → Lean.Order.PredTrans Pred EPred Value), ∀ (x : Prog), wpTrans x = Lean.Order.PredTrans.frameClosure op (f x)) : Frames op x F

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

theorem Std.WP.WP.Frames.of_conjunctive {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x : Prog} [WPConjunctive x] {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.WP.WP.of_frameClosure {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] {R : Type t} (op : R → Pred → Pred) [∀ (r : R), Lean.Order.PreservesSup (op r)] (base : WP Prog Value Pred EPred) : WP Prog Value Pred EPred

Reinterpret a WP so its weakest precondition is the frameClosure of the base wp over a family of supremum-preserving resource operators op r.

Equations

• Std.WP.WP.of_frameClosure op base = { wpTrans := fun (x : Prog) => Lean.Order.PredTrans.frameClosure op (Std.WP.WP.wpTrans x), wp_trans_monotone := ⋯ }

theorem Std.WP.WP.of_frameClosure_le_wp_iff {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] {R : Type t} (op : R → Pred → Pred) [∀ (r : R), Lean.Order.PreservesSup (op r)] (base : WP Prog Value Pred EPred) (x : Prog) (Q : Value → Pred) (E : EPred) (pre : Pred) : Lean.Order.PartialOrder.rel pre (wp x Q E) ↔ ∀ (r : R), Lean.Order.PartialOrder.rel (op r pre) (wp x (fun (a : Value) => op r (Q a)) E)

Characterization of the WP.of_frameClosure weakest precondition: landing below it is landing below the base wp with every resource op r framed onto the pre- and postcondition.

theorem Std.WP.WP.le_wp_of_frameClosure_eq {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] {R : Type t} {op : R → Pred → Pred} [∀ (r : R), Lean.Order.PreservesSup (op r)] {base I : WP Prog Value Pred EPred} (heq : I = of_frameClosure op base) {x : Prog} {Q : Value → Pred} {E : EPred} {pre : Pred} (h : ∀ (r : R), Lean.Order.PartialOrder.rel (op r pre) (wp x (fun (a : Value) => op r (Q a)) E)) : Lean.Order.PartialOrder.rel pre (wp x Q E)

Introduction rule for the weakest precondition of a WP.of_frameClosure interpretation, selected by the witness equation heq: land below the base wp with every resource framed on.