Framing at the wp layer

WP.Frames op x F P states that the program x commutes op F · into the postcondition of wp x in every state that satisfies the guard P, with the exception channel framed by the FrameOp-derived companion. The guard P matters when the footprint of x depends on the state. For example, a write to the memory region [s.p, s.p + s.n) frames F s := s.mem a = v under the guard P s := a < s.p ∨ s.p + s.n ≤ a. A WP built as the Lean.Order.PredTrans.frameClosure of a base wp frames every resource under every guard.

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} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {R : Type t} (op : R → Pred → Pred) {opE : R → EPosts → EPosts} [Lean.Order.FrameOp op EPosts opE] (x : Prog) (F : R) (P : Pred) : Prop

The program x frames the resource F under the guard P: in a state that satisfies P, op F · commutes into the postcondition of wp x and the companion opE F · into the exception postcondition.

• op_wp_le_wp_op (Q : Value → Pred) (E : EPosts) : Lean.Order.PartialOrder.rel (Lean.Order.meet P (op F (wp x Q E))) (wp x (fun (a : Value) => op F (Q a)) (opE F E))

  Under P, op F and its companion commute into the postcondition pair of wp x.

theorem Std.WP.meet_op_wp_upperAdjoint_le_wp {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {R : Type t} {op : R → Pred → Pred} {opE : R → EPosts → EPosts} [Lean.Order.FrameOp op EPosts opE] {x : Prog} {F : R} {P : Pred} {Q : Value → Pred} {E : EPosts} (hframes : WP.Frames op x F P) : Lean.Order.PartialOrder.rel (Lean.Order.meet P (op F (wp x (fun (a : Value) => Lean.Order.PreservesSup.upperAdjoint (op F) (Q a)) (Lean.Order.PreservesSup.upperAdjoint (opE F) E)))) (wp x Q E)

theorem Std.WP.WP.frames_of_frameClosure {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {R : Type t} (op : R → Pred → Pred) {opE : R → EPosts → EPosts} [Lean.Order.FrameOp op EPosts opE] (comp : R → R → R) (hact : ∀ (r r' : R) (a : Pred), op (comp r r') a = op r (op r' a)) (hactE : ∀ (r r' : R) (E : EPosts), opE (comp r r') E = opE r (opE r' E)) {x : Prog} {F : R} {P : Pred} (h : ∃ (f : Prog → Lean.Order.PredTrans Pred EPosts Value), ∀ (x : Prog), trans x = Lean.Order.PredTrans.frameClosure op (f x)) : Frames op x F P

theorem Std.WP.WP.frames_of_conjunctive {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x : Prog} [WPConjunctive x] {opE : Pred → EPosts → EPosts} [Lean.Order.FrameOp Lean.Order.meet EPosts opE] {F P : Pred} (hF : Lean.Order.PartialOrder.rel (Lean.Order.meet P F) (wp x (fun (x : Value) => F) (opE F Lean.Order.top))) (hE : ∀ (E : EPosts), Lean.Order.PartialOrder.rel (Lean.Order.meet (opE F Lean.Order.top) E) (opE F E)) : Frames Lean.Order.meet x F P

@[instance_reducible]

noncomputable def Std.WP.WP.withFrameClosure {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] {R : Type t} (op : R → Pred → Pred) {opE : R → EPosts → EPosts} [Lean.Order.FrameOp op EPosts opE] (base : WP Prog Value Pred EPosts) : WP Prog Value Pred EPosts

Reinterpret a WP so its weakest precondition is the frameClosure of the base wp over a family of supremum-preserving resource operators op r and the FrameOp-derived exception-channel companion.

Equations

• Std.WP.WP.withFrameClosure op base = { trans := fun (x : Prog) => Lean.Order.PredTrans.frameClosure op (Std.WP.WP.trans x), trans_monotone := ⋯ }

theorem Std.WP.WP.withFrameClosure_le_wp_iff {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] {R : Type t} (op : R → Pred → Pred) {opE : R → EPosts → EPosts} [Lean.Order.FrameOp op EPosts opE] (base : WP Prog Value Pred EPosts) (x : Prog) (Q : Value → Pred) (E : EPosts) (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)) (opE r E))

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