Weakest Preconditions Over the Free Monad

This file provides the extrinsic verification-condition substrate for FreeM P, in two coupled layers:

• Syntactic wp. An OpSpec P l assigns each operation a : P.A a predicate transformer (P.B a → l) → l over an ordered carrier l, saying what one call to a guarantees. FreeM.wpFold Φ folds these per-operation specs over a free tree, leaving the operations uninterpreted. Every monotone spec induces an ordered monad algebra OpSpec.toMAlgOrdered, so the whole MAlgOrdered.wp / Triple rule set applies; wp_toMAlgOrdered identifies the induced wp with wpFold.

• Semantic wp. FreeM.wpVia s is the weakest precondition of the program interpreted through a handler s : Handler m P into a monad carrying an ordered algebra. The soundness theorems wpFold_le_wpVia / wpFold_eq_wpVia say that per-operation specs that (under-)approximate the handler's wp give syntactic wps that (under-)approximate the semantic wp — the generic engine behind handler-specification reasoning.

The canonical Prop-carrier specs OpSpec.demonic ("every response") and OpSpec.angelic ("some response") recover the support-based judgments of PolyFun.PFunctor.Free.Support: wpFold_demonic_iff_allOutputs and wpFold_angelic_iff_someOutput identify their folds with AllOutputs and SomeOutput, so trivial-precondition ("always" / "never") triples and the syntactic wp theory agree.

Per-operation specifications

def PFunctor.OpSpec (P : PFunctor.{uA, uB}) (l : Type w) : Type (max uA uB w)

A per-operation predicate-transformer specification for the interface P over an ordered carrier l: at each position a, transform a postcondition on the directions of a into a precondition.

def PFunctor.OpSpec.Mono {P : PFunctor.{uA, uB}} {l : Type w} [Preorder l] (Φ : P.OpSpec l) : Prop

Monotonicity of a per-operation spec in its continuation.

def PFunctor.OpSpec.demonic (P : PFunctor.{uA, uB}) : P.OpSpec Prop

The demonic ("all responses") spec on the Prop carrier: a call to a guarantees only that every response satisfies the continuation.

def PFunctor.OpSpec.demonicUnder {P : PFunctor.{uA, uB}} (allows : (a : P.A) → P.B a → Prop) : P.OpSpec Prop

The demonic specification restricted to admitted responses: a call to a guarantees that every response satisfying allows a satisfies the continuation.

This specification is intentionally a partial-correctness condition. If no response is admitted at a position, its obligation is vacuous; progress or non-vacuity must be supplied separately by an operational layer.

def PFunctor.OpSpec.angelic (P : PFunctor.{uA, uB}) : P.OpSpec Prop

The angelic ("some response") spec on the Prop carrier: a call to a guarantees that some response satisfies the continuation.

def PFunctor.OpSpec.angelicUnder {P : PFunctor.{uA, uB}} (allows : (a : P.A) → P.B a → Prop) : P.OpSpec Prop

The angelic specification restricted to admitted responses: a call can continue along any response satisfying allows.

theorem PFunctor.OpSpec.demonic_mono {P : PFunctor.{uA, uB}} : (demonic P).Mono

theorem PFunctor.OpSpec.demonicUnder_mono {P : PFunctor.{uA, uB}} (allows : (a : P.A) → P.B a → Prop) : (demonicUnder allows).Mono

theorem PFunctor.OpSpec.angelic_mono {P : PFunctor.{uA, uB}} : (angelic P).Mono

theorem PFunctor.OpSpec.angelicUnder_mono {P : PFunctor.{uA, uB}} (allows : (a : P.A) → P.B a → Prop) : (angelicUnder allows).Mono

Syntactic weakest precondition

def PFunctor.FreeM.wpFold {P : PFunctor.{uA, uB}} {l : Type w} {α : Type v} (Φ : P.OpSpec l) : P.FreeM α → (α → l) → l

Fold a per-operation spec over a free tree: the syntactic weakest precondition of x for postcondition post, with operations uninterpreted.

@[simp]

theorem PFunctor.FreeM.wpFold_pure {P : PFunctor.{uA, uB}} {l : Type w} {α : Type v} (Φ : P.OpSpec l) (x : α) (post : α → l) : wpFold Φ (pure x) post = post x

theorem PFunctor.FreeM.wpFold_liftBind {P : PFunctor.{uA, uB}} {l : Type w} {α : Type v} (Φ : P.OpSpec l) (a : P.A) (r : P.B a → P.FreeM α) (post : α → l) : wpFold Φ (liftBind a r) post = Φ a fun (b : P.B a) => wpFold Φ (r b) post

@[simp]

theorem PFunctor.FreeM.wpFold_lift {P : PFunctor.{uA, uB}} {l : Type w} (Φ : P.OpSpec l) (a : P.A) (post : P.B a → l) : wpFold Φ (lift a) post = Φ a post

theorem PFunctor.FreeM.wpFold_bind' {P : PFunctor.{uA, uB}} {l : Type w} {X : Type uX} {Y : Type uY} (Φ : P.OpSpec l) (x : P.FreeM X) (f : X → P.FreeM Y) (post : Y → l) : wpFold Φ (x.bind f) post = wpFold Φ x fun (a : X) => wpFold Φ (f a) post

Weakest preconditions compose through sequencing across result universes.

theorem PFunctor.FreeM.wpFold_bind {P : PFunctor.{uA, uB}} {l : Type w} {α β : Type v} (Φ : P.OpSpec l) (x : P.FreeM α) (f : α → P.FreeM β) (post : β → l) : wpFold Φ (x >>= f) post = wpFold Φ x fun (a : α) => wpFold Φ (f a) post

The rest of the do fragment

wpFold is a fold, so every combinator do-notation elaborates to reduces to wpFold_bind and wpFold_pure; the equations below state the results directly so simp need not rediscover them.

@[simp]

theorem PFunctor.FreeM.wpFold_map {P : PFunctor.{uA, uB}} {l : Type w} {α β : Type v} (Φ : P.OpSpec l) (f : α → β) (x : P.FreeM α) (post : β → l) : wpFold Φ (f <$> x) post = wpFold Φ x fun (a : α) => post (f a)

@[simp]

theorem PFunctor.FreeM.wpFold_seq {P : PFunctor.{uA, uB}} {l : Type w} {α β : Type v} (Φ : P.OpSpec l) (f : P.FreeM (α → β)) (x : P.FreeM α) (post : β → l) : wpFold Φ (f <*> x) post = wpFold Φ f fun (g : α → β) => wpFold Φ x fun (a : α) => post (g a)

@[simp]

theorem PFunctor.FreeM.wpFold_seqLeft {P : PFunctor.{uA, uB}} {l : Type w} {α β : Type v} (Φ : P.OpSpec l) (x : P.FreeM α) (y : P.FreeM β) (post : α → l) : wpFold Φ (x <* y) post = wpFold Φ x fun (a : α) => wpFold Φ y fun (x : β) => post a

@[simp]

theorem PFunctor.FreeM.wpFold_seqRight {P : PFunctor.{uA, uB}} {l : Type w} {α β : Type v} (Φ : P.OpSpec l) (x : P.FreeM α) (y : P.FreeM β) (post : β → l) : wpFold Φ (x *> y) post = wpFold Φ x fun (x : α) => wpFold Φ y post

@[simp]

theorem PFunctor.FreeM.wpFold_ite {P : PFunctor.{uA, uB}} {l : Type w} {α : Type v} (Φ : P.OpSpec l) (c : Prop) [Decidable c] (x y : P.FreeM α) (post : α → l) : wpFold Φ (if c then x else y) post = if c then wpFold Φ x post else wpFold Φ y post

@[simp]

theorem PFunctor.FreeM.wpFold_dite {P : PFunctor.{uA, uB}} {l : Type w} {α : Type v} (Φ : P.OpSpec l) (c : Prop) [Decidable c] (x : c → P.FreeM α) (y : ¬c → P.FreeM α) (post : α → l) : wpFold Φ (if h : c then x h else y h) post = if h : c then wpFold Φ (x h) post else wpFold Φ (y h) post

@[simp]

theorem PFunctor.FreeM.wpFold_option_elim {P : PFunctor.{uA, uB}} {l : Type w} {α : Type v} {γ : Type uX} (Φ : P.OpSpec l) (o : Option γ) (x : P.FreeM α) (f : γ → P.FreeM α) (post : α → l) : wpFold Φ (o.elim x f) post = o.elim (wpFold Φ x post) fun (c : γ) => wpFold Φ (f c) post

@[simp]

theorem PFunctor.FreeM.wpFold_sum_elim {P : PFunctor.{uA, uB}} {l : Type w} {α : Type v} {γ : Type uX} {δ : Type uY} (Φ : P.OpSpec l) (s : γ ⊕ δ) (f : γ → P.FreeM α) (g : δ → P.FreeM α) (post : α → l) : wpFold Φ (Sum.elim f g s) post = Sum.elim (fun (c : γ) => wpFold Φ (f c) post) (fun (d : δ) => wpFold Φ (g d) post) s

theorem PFunctor.FreeM.wpFold_mono {P : PFunctor.{uA, uB}} {l : Type w} {α : Type v} [Preorder l] {Φ : P.OpSpec l} (hΦ : Φ.Mono) (x : P.FreeM α) {post post' : α → l} (h : ∀ (a : α), post a ≤ post' a) : wpFold Φ x post ≤ wpFold Φ x post'

Reachable outputs under an operationalization

def PFunctor.FreeM.reachableUnder {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (x : P.FreeM α) : Set α

Outputs reachable when each operation may return exactly the responses admitted by allows. This is the set view of the angelic predicate transformer, not a generic interpretation of MonadAttach.CanReturn.

def PFunctor.FreeM.reachable {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) : Set α

Structural reachability when every typed response is admitted.

@[simp]

theorem PFunctor.FreeM.reachableUnder_pure {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (result : α) : reachableUnder allows (pure result) = {result}

theorem PFunctor.FreeM.reachableUnder_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (position : P.A) (next : P.B position → P.FreeM α) : reachableUnder allows (liftBind position next) = ⋃ direction ∈ {direction : P.B position | allows position direction}, reachableUnder allows (next direction)

@[simp]

theorem PFunctor.FreeM.reachableUnder_lift {P : PFunctor.{uA, uB}} (allows : (a : P.A) → P.B a → Prop) (position : P.A) : reachableUnder allows (lift position) = {direction : P.B position | allows position direction}

theorem PFunctor.FreeM.wpFold_angelicUnder_iff_exists_reachable {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (x : P.FreeM α) (post : α → Prop) : wpFold (OpSpec.angelicUnder allows) x post ↔ ∃ result ∈ reachableUnder allows x, post result

The angelic fold is existential quantification over reachable outputs.

@[simp]

theorem PFunctor.FreeM.reachableUnder_bind {P : PFunctor.{uA, uB}} {α β : Type v} (allows : (a : P.A) → P.B a → Prop) (x : P.FreeM α) (next : α → P.FreeM β) : reachableUnder allows (x >>= next) = ⋃ result ∈ reachableUnder allows x, reachableUnder allows (next result)

@[simp]

theorem PFunctor.FreeM.reachableUnder_bind' {P : PFunctor.{uA, uB}} {X : Type uX} {Y : Type uY} (allows : (a : P.A) → P.B a → Prop) (program : P.FreeM X) (next : X → P.FreeM Y) : reachableUnder allows (program.bind next) = ⋃ result ∈ reachableUnder allows program, reachableUnder allows (next result)

Reachability through sequencing with independent result universes.

theorem PFunctor.FreeM.reachableUnder_mono {P : PFunctor.{uA, uB}} {α : Type v} {allows₁ allows₂ : (a : P.A) → P.B a → Prop} (h : ∀ (position : P.A) (direction : P.B position), allows₁ position direction → allows₂ position direction) (x : P.FreeM α) : reachableUnder allows₁ x ⊆ reachableUnder allows₂ x

@[simp]

theorem PFunctor.FreeM.reachableUnder_map {P : PFunctor.{uA, uB}} {X : Type uX} {Y : Type uY} (allows : (a : P.A) → P.B a → Prop) (function : X → Y) (program : P.FreeM X) : reachableUnder allows (map function program) = function '' reachableUnder allows program

Mapping leaf values maps the set of outputs reachable under the same responses.

theorem PFunctor.FreeM.reachableUnder_liftObj {P : PFunctor.{uA, uB}} {X : Type uX} (allows : (a : P.A) → P.B a → Prop) (object : ↑P X) : reachableUnder allows (liftObj object) = object.snd '' {direction : P.B object.fst | allows object.fst direction}

@[simp]

theorem PFunctor.FreeM.reachableUnder_functorMap {P : PFunctor.{uA, uB}} {α β : Type v} (allows : (a : P.A) → P.B a → Prop) (function : α → β) (program : P.FreeM α) : reachableUnder allows (function <$> program) = function '' reachableUnder allows program

Functor mapping preserves the admitted response policy and maps reachable results.

def PFunctor.FreeM.Path.AllowedUnder {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (x : P.FreeM α) : x.Path → Prop

A path is admitted when every direction on it is admitted at its operation.

@[simp]

theorem PFunctor.FreeM.Path.allowedUnder_pure {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (value : α) (path : (pure value).Path) : AllowedUnder allows (pure value) path

The terminal path has no response constraints.

theorem PFunctor.FreeM.Path.allowedUnder_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (position : P.A) (next : P.B position → P.FreeM α) (direction : P.B position) (path : (next direction).Path) : AllowedUnder allows (liftBind position next) ⟨direction, path⟩ ↔ allows position direction ∧ AllowedUnder allows (next direction) path

An admitted node path takes an admitted response and an admitted continuation path.

theorem PFunctor.FreeM.mem_reachableUnder_iff_exists_path {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (x : P.FreeM α) (result : α) : result ∈ reachableUnder allows x ↔ ∃ (path : x.Path), Path.AllowedUnder allows x path ∧ x.output path = result

Reachability is witnessed by an admitted root-to-leaf path.

theorem PFunctor.FreeM.reachableUnder_eq_liftM {P : PFunctor.{uA, uB}} {γ : Type uB} (allows : (a : P.A) → P.B a → Prop) (x : P.FreeM γ) : reachableUnder allows x = (FreeM.liftM (fun (position : P.A) => {direction : P.B position | allows position direction}) x).run

Running the powerset handler gives the same reachable outputs.

theorem PFunctor.FreeM.reachable_eq_support {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) : x.reachable = MonadAttach.support x

Full-response reachability agrees with the free tree's attachment predicate.

theorem PFunctor.FreeM.mem_reachable_iff_canReturn {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) (result : α) : result ∈ x.reachable ↔ MonadAttach.CanReturn x result

Admitted-response leaf contracts

def PFunctor.FreeM.LeavesSatisfyUnder {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (accept : α → Prop) : P.FreeM α → Prop

Every leaf reachable by choosing admitted responses satisfies accept.

This is the relation-restricted demonic weakest precondition, not a termination or progress assertion. In particular, a query with no admitted response satisfies every leaf contract vacuously.

@[simp]

theorem PFunctor.FreeM.leavesSatisfyUnder_pure {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (accept : α → Prop) (result : α) : LeavesSatisfyUnder allows accept (pure result) ↔ accept result

theorem PFunctor.FreeM.leavesSatisfyUnder_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (accept : α → Prop) (position : P.A) (next : P.B position → P.FreeM α) : LeavesSatisfyUnder allows accept (liftBind position next) ↔ ∀ (direction : P.B position), allows position direction → LeavesSatisfyUnder allows accept (next direction)

theorem PFunctor.FreeM.LeavesSatisfyUnder.mono {P : PFunctor.{uA, uB}} {α : Type v} {allows : (a : P.A) → P.B a → Prop} {accept accept' : α → Prop} (haccept : ∀ (result : α), accept result → accept' result) {program : P.FreeM α} (h : LeavesSatisfyUnder allows accept program) : LeavesSatisfyUnder allows accept' program

Weakening the required leaf predicate preserves whole-tree conformance.

theorem PFunctor.FreeM.leavesSatisfyUnder_map_iff {P : PFunctor.{uA, uB}} (allows : (a : P.A) → P.B a → Prop) {X : Type uX} {Y : Type uY} (accept : Y → Prop) (function : X → Y) (program : P.FreeM X) : LeavesSatisfyUnder allows accept (map function program) ↔ LeavesSatisfyUnder allows (accept ∘ function) program

Mapping a function changes only the predicate imposed on returned leaves.

theorem PFunctor.FreeM.leavesSatisfyUnder_bind_iff {P : PFunctor.{uA, uB}} (allows : (a : P.A) → P.B a → Prop) {X : Type uX} {Y : Type uY} (accept : Y → Prop) (program : P.FreeM X) (next : X → P.FreeM Y) : LeavesSatisfyUnder allows accept (program.bind next) ↔ LeavesSatisfyUnder allows (fun (result : X) => LeavesSatisfyUnder allows accept (next result)) program

Whole-tree result conformance composes through monadic sequencing.

theorem PFunctor.FreeM.leavesSatisfyUnder_iff_forall_reachable {P : PFunctor.{uA, uB}} {α : Type v} (allows : (a : P.A) → P.B a → Prop) (x : P.FreeM α) (post : α → Prop) : LeavesSatisfyUnder allows post x ↔ ∀ result ∈ reachableUnder allows x, post result

The relation-restricted demonic WP quantifies over the reachable outputs.

theorem PFunctor.FreeM.leavesSatisfyUnder_liftM {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type uB} (handler : (position : P.A) → Q.FreeM (P.B position)) (outerAllows : (position : P.A) → P.B position → Prop) (innerAllows : (position : Q.A) → Q.B position → Prop) (accept : α → Prop) (hhandler : ∀ (position : P.A), LeavesSatisfyUnder innerAllows (outerAllows position) (handler position)) (program : P.FreeM α) (hprogram : LeavesSatisfyUnder outerAllows accept program) : LeavesSatisfyUnder innerAllows accept (FreeM.liftM handler program)

Interpreting a finite free program through leaf-conforming free handlers preserves its admitted-response leaf contract.

Unlike the map and bind laws above, the program result type shares the source interface's direction universe. This is exactly the homogeneous result constraint of the upstream FreeM.liftM; the target interface's position and direction universes remain independent.

theorem PFunctor.FreeM.reachableUnder_liftM_subset {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type uB} (handler : (position : P.A) → Q.FreeM (P.B position)) (outerAllows : (position : P.A) → P.B position → Prop) (innerAllows : (position : Q.A) → Q.B position → Prop) (hhandler : ∀ (position : P.A), LeavesSatisfyUnder innerAllows (outerAllows position) (handler position)) (program : P.FreeM α) : reachableUnder innerAllows (FreeM.liftM handler program) ⊆ reachableUnder outerAllows program

A free handler whose admitted outputs respect the source response constraint cannot introduce new reachable results. This is the operational counterpart of leavesSatisfyUnder_liftM.

theorem PFunctor.FreeM.reachable_liftM_subset {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type uB} (handler : (position : P.A) → Q.FreeM (P.B position)) (program : P.FreeM α) : (FreeM.liftM handler program).reachable ⊆ program.reachable

Interpreting free operations by free programs cannot create new leaf values.

The induced ordered monad algebra

@[instance_reducible]

def PFunctor.OpSpec.toMAlgOrdered {P : PFunctor.{uA, uB}} {l : Type v} [CompleteLattice l] (Φ : P.OpSpec l) (hΦ : Φ.Mono) : MAlgOrdered P.FreeM l

Every monotone per-operation spec over a complete lattice induces an ordered monad algebra on FreeM P, giving the full MAlgOrdered.wp/Triple rule set for free.

theorem PFunctor.FreeM.wp_toMAlgOrdered {P : PFunctor.{uA, uB}} {α l : Type v} [CompleteLattice l] (Φ : P.OpSpec l) (hΦ : Φ.Mono) (x : P.FreeM α) (post : α → l) : MAlgOrdered.wp x post = wpFold Φ x post

The MAlgOrdered.wp induced by a per-operation spec is its syntactic fold.

Semantic weakest precondition through a handler

def PFunctor.FreeM.wpVia {P : PFunctor.{uA, uB}} {m : Type uB → Type w} [Monad m] {l : Type uB} [CompleteLattice l] [MAlgOrdered m l] {α : Type uB} (s : Handler m P) (x : P.FreeM α) (post : α → l) : l

The semantic weakest precondition of a free program interpreted through a handler into a monad carrying an ordered algebra.

@[simp]

theorem PFunctor.FreeM.wpVia_pure {P : PFunctor.{uA, uB}} {m : Type uB → Type w} [Monad m] [LawfulMonad m] {l : Type uB} [CompleteLattice l] [MAlgOrdered m l] {α : Type uB} (s : Handler m P) (x : α) (post : α → l) : wpVia s (pure x) post = post x

theorem PFunctor.FreeM.wpVia_bind {P : PFunctor.{uA, uB}} {m : Type uB → Type w} [Monad m] [LawfulMonad m] {l : Type uB} [CompleteLattice l] [MAlgOrdered m l] {α β : Type uB} (s : Handler m P) (x : P.FreeM α) (f : α → P.FreeM β) (post : β → l) : wpVia s (x >>= f) post = wpVia s x fun (a : α) => wpVia s (f a) post

theorem PFunctor.FreeM.wpVia_lift {P : PFunctor.{uA, uB}} {m : Type uB → Type w} [Monad m] [LawfulMonad m] {l : Type uB} [CompleteLattice l] [MAlgOrdered m l] (s : Handler m P) (a : P.A) (post : P.B a → l) : wpVia s (lift a) post = MAlgOrdered.wp (s a) post

The semantic precondition of a single operation is the handler's precondition.

theorem PFunctor.FreeM.wpFold_le_wpVia {P : PFunctor.{uA, uB}} {m : Type uB → Type w} [Monad m] [LawfulMonad m] {l : Type uB} [CompleteLattice l] [MAlgOrdered m l] {α : Type uB} {Φ : P.OpSpec l} (s : Handler m P) (h : ∀ (a : P.A) (k : P.B a → l), Φ a k ≤ MAlgOrdered.wp (s a) k) (x : P.FreeM α) (post : α → l) : wpFold Φ x post ≤ wpVia s x post

Soundness of per-operation specs against a handler: specs that lower-bound the handler's wp at every operation give a syntactic wp lower-bounding the semantic wp of the interpreted program.

theorem PFunctor.FreeM.wpFold_eq_wpVia {P : PFunctor.{uA, uB}} {m : Type uB → Type w} [Monad m] [LawfulMonad m] {l : Type uB} [CompleteLattice l] [MAlgOrdered m l] {α : Type uB} {Φ : P.OpSpec l} (s : Handler m P) (h : ∀ (a : P.A) (k : P.B a → l), Φ a k = MAlgOrdered.wp (s a) k) (x : P.FreeM α) (post : α → l) : wpFold Φ x post = wpVia s x post

Exact per-operation specs give the semantic wp exactly.

Coherence with the canonical support

theorem PFunctor.FreeM.leavesSatisfyUnder_all_iff_allOutputs {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) (post : α → Prop) : LeavesSatisfyUnder (fun (x : P.A) (x_1 : P.B x) => True) post x ↔ MonadAttach.AllOutputs post x

With every response admitted, the restricted leaf contract is the canonical all-outputs judgment.

theorem PFunctor.FreeM.wpFold_demonic_iff_allOutputs {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) (post : α → Prop) : wpFold (OpSpec.demonic P) x post ↔ MonadAttach.AllOutputs post x

The demonic fold is the "always" judgment over the canonical support.

theorem PFunctor.FreeM.wpFold_angelic_iff_someOutput {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) (post : α → Prop) : wpFold (OpSpec.angelic P) x post ↔ MonadAttach.SomeOutput post x

The angelic fold is the "some output" judgment over the canonical support.

theorem PFunctor.FreeM.wpFold_demonic_not_iff_noOutput {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) (post : α → Prop) : (wpFold (OpSpec.demonic P) x fun (a : α) => ¬post a) ↔ MonadAttach.NoOutput post x

The demonic fold of a negated postcondition is the "never" judgment.

Coherence with the interpreted program's support

The section above relates the syntactic fold to the support of the free tree. This one closes the other half: it relates the semantic wpVia to the support of the interpreted program, which is what a handler-specification consumer actually reasons about.

The carrier is Prop, so these live at the ground direction universe: MAlgOrdered m l forces l : Type uB, and Prop : Type 0.

theorem PFunctor.FreeM.wpVia_demonic_iff_allOutputs {Q : PFunctor.{uA, 0}} {n : Type → Type w} [Monad n] [LawfulMonad n] [MonadAttach n] [ExactMonadAttach n] {α : Type} (s : Handler n Q) (x : Q.FreeM α) (post : α → Prop) : wpVia s x post ↔ MonadAttach.AllOutputs post (FreeM.liftM s x)

The semantic keystone. wpVia is by definition the algebra's wp of the interpreted program, so under the demonic Prop algebra it is the "always" judgment on that program. One rewrite, but it is the step that turns every statement about wpVia into a statement about which outputs the interpreted program can actually return.

theorem PFunctor.FreeM.wpVia_angelic_iff_someOutput {Q : PFunctor.{uA, 0}} {n : Type → Type w} [Monad n] [LawfulMonad n] [MonadAttach n] [ExactMonadAttach n] {α : Type} (s : Handler n Q) (x : Q.FreeM α) (post : α → Prop) : wpVia s x post ↔ MonadAttach.SomeOutput post (FreeM.liftM s x)

The angelic companion.

theorem PFunctor.FreeM.allOutputs_liftM_of_wpFold {Q : PFunctor.{uA, 0}} {n : Type → Type w} [Monad n] [LawfulMonad n] [MonadAttach n] [ExactMonadAttach n] {α : Type} {Φ : Q.OpSpec Prop} (s : Handler n Q) (h : ∀ (a : Q.A) (k : Q.B a → Prop), Φ a k ≤ MAlgOrdered.wp (s a) k) (x : Q.FreeM α) (post : α → Prop) (hx : wpFold Φ x post) : MonadAttach.AllOutputs post (FreeM.liftM s x)

Specs discharge support facts about the interpreted program. Composing the keystone with wpFold_le_wpVia: a per-operation spec that under-approximates the handler's wp turns a syntactic fold into a guarantee about every output the handler can actually produce. This is the shape a handler-specification layer consumes.

theorem PFunctor.FreeM.allOutputs_liftM_of_allOutputs {Q : PFunctor.{uA, 0}} {n : Type → Type w} [Monad n] [LawfulMonad n] [MonadAttach n] [ExactMonadAttach n] {α : Type} (s : Handler n Q) (h : ∀ (a : Q.A) (k : Q.B a → Prop), (∀ (b : Q.B a), k b) → MAlgOrdered.wp (s a) k) (x : Q.FreeM α) (post : α → Prop) (hx : MonadAttach.AllOutputs post x) : MonadAttach.AllOutputs post (FreeM.liftM s x)

The demonic fold at the canonical spec already implies the interpreted guarantee, whenever the handler validates that spec. Specializes the previous theorem to OpSpec.demonic: the handler must establish every postcondition that holds for all typed responses. This constrains its outputs to the operation's response type; it does not claim that the handler can produce every response.