feat: expose the public PFunctor module surface

PolyFun.lean

@@ -193,6 +193,7 @@ public import PolyFun.PFunctor.Free.Resumption
 public import PolyFun.PFunctor.Free.Universal
 public import PolyFun.PFunctor.Handler
 public import PolyFun.PFunctor.Handler.Free
+public import PolyFun.PFunctor.Handler.Instrumentation
 public import PolyFun.PFunctor.Handler.Normalization
 public import PolyFun.PFunctor.Handler.Normalization.Attr
 public import PolyFun.PFunctor.Handler.Stateful

PolyFun/Interaction/Basic/Sampler.lean

@@ -74,6 +74,40 @@ def samplePath {m : Type w → Type w'} [Monad m] :
       let tr ← samplePath (rest x) (sampRest x)
       return ⟨x, tr⟩
 
+/-- Sampling a completed interaction returns its unique empty path. -/
+@[simp]
+theorem samplePath_done {m : Type w → Type w'} [Monad m]
+    (sampler : Sampler m .done) :
+    samplePath .done sampler = pure ⟨⟩ := by
+  rfl
+
+/-! The raw and `TypeTree`-facing node equations are both public so callers can
+rewrite without depending on which transparent representation Lean exposes. -/
+
+/-- Sampling a raw free-monad node first samples its head value and then its
+dependent tail path. -/
+@[simp]
+theorem samplePath_lift_bind {m : Type w → Type w'} [Monad m]
+    {X : Type w} (rest : X → TypeTree.{w})
+    (sampler : m X) (samplerRest : ∀ x, Sampler m (rest x)) :
+    samplePath (@PFunctor.FreeM.lift TypeTree.basePFunctor X >>= rest)
+        ⟨sampler, samplerRest⟩ = do
+      let x ← sampler
+      let tr ← samplePath (rest x) (samplerRest x)
+      return ⟨x, tr⟩ := by
+  rfl
+
+/-- Sampling a `TypeTree.node` first samples its head value and then its
+dependent tail path. -/
+theorem samplePath_node {m : Type w → Type w'} [Monad m]
+    {X : Type w} (rest : X → TypeTree.{w})
+    (sampler : m X) (samplerRest : ∀ x, Sampler m (rest x)) :
+    samplePath (TypeTree.node X rest) ⟨sampler, samplerRest⟩ = do
+      let x ← sampler
+      let tr ← samplePath (rest x) (samplerRest x)
+      return ⟨x, tr⟩ := by
+  rfl
+
 /--
 Combine a scheduler sampler with two per-branch samplers into a sampler
 for the binary-choice interleaving tree

PolyFun/Interaction/Concurrent/Fairness.lean

@@ -46,11 +46,23 @@ forever. -/
 def EventuallyAlways (P : Nat → Prop) : Prop :=
   ∃ N, ∀ n, N ≤ n → P n
 
+/-- Characterize eventual persistence by a cutoff after which the property
+holds at every later index. -/
+theorem eventuallyAlways_iff {P : Nat → Prop} :
+    EventuallyAlways P ↔ ∃ N, ∀ n, N ≤ n → P n :=
+  Iff.rfl
+
 /-- `InfinitelyOften P` means that `P` holds at arbitrarily late time
 indices. -/
 def InfinitelyOften (P : Nat → Prop) : Prop :=
   ∀ N, ∃ n, N ≤ n ∧ P n
 
+/-- Characterize infinite recurrence by the existence of a witness at or
+after every requested index. -/
+theorem infinitelyOften_iff {P : Nat → Prop} :
+    InfinitelyOften P ↔ ∀ N, ∃ n, N ≤ n ∧ P n :=
+  Iff.rfl
+
 theorem always_mono {P Q : Nat → Prop} (himp : ∀ n, P n → Q n) : Always P → Always Q :=
   fun hP n => himp n (hP n)
 

PolyFun/Interaction/Multiparty/Observation.lean

@@ -163,6 +163,7 @@ variable {X : Type u}
 
 Every `Observation X` refines `Observation.top X`.
 -/
+@[expose]
 protected def top (X : Type u) : Observation X := ⟨X, id⟩
 
 /--
@@ -187,6 +188,12 @@ observers using `k₂` learn. This is the natural ordering in which
 def Refines (k₁ k₂ : Observation X) : Prop :=
   ∃ f : k₂.1 → k₁.1, ∀ x, k₁.2 x = f (k₂.2 x)
 
+/-- Observation refinement holds exactly when the first observation factors
+through the second by an explicit map. -/
+theorem refines_iff {k₁ k₂ : Observation X} :
+    k₁.Refines k₂ ↔ ∃ f : k₂.1 → k₁.1, ∀ x, k₁.2 x = f (k₂.2 x) :=
+  Iff.rfl
+
 @[refl] theorem Refines.refl (k : Observation X) : k.Refines k :=
   ⟨id, fun _ => rfl⟩
 

PolyFun/Interaction/UC/OpenProcess.lean

@@ -657,6 +657,48 @@ def OpenNodeContext.boundaryTrace {Party : Type u} {Δ : PortBoundary} : (spec :
   | .node _ rest, ⟨node, next⟩, ⟨x, tr⟩ =>
       node.boundary.emit x * OpenNodeContext.boundaryTrace (rest x) (next x) tr
 
+/-- A completed open node contributes no boundary actions. -/
+@[simp]
+theorem OpenNodeContext.boundaryTrace_done {Party : Type u} {Δ : PortBoundary}
+    (semantics : Decoration (OpenNodeContext.{u, w} Party Δ)
+      (TypeTree.done : TypeTree.{w}))
+    (path : TypeTree.Path (TypeTree.done : TypeTree.{w})) :
+    OpenNodeContext.boundaryTrace (Party := Party) (Δ := Δ) TypeTree.done semantics path =
+      (1 : PFunctor.TraceList Δ.Out) := by
+  rfl
+
+/-! The raw and `TypeTree`-facing node equations are both public so callers can
+rewrite without depending on which transparent representation Lean exposes. -/
+
+/-- A raw free-monad node emits the head boundary action and continues along
+the chosen tail. -/
+@[simp]
+theorem OpenNodeContext.boundaryTrace_lift_bind {Party : Type u} {Δ : PortBoundary}
+    {X : Type w} (rest : X → TypeTree.{w})
+    (semantics : Decoration (OpenNodeContext.{u, w} Party Δ) (TypeTree.node X rest))
+    (x : X) (path : TypeTree.Path (rest x)) :
+    OpenNodeContext.boundaryTrace (Party := Party) (Δ := Δ)
+        (@PFunctor.FreeM.lift TypeTree.basePFunctor X >>= rest) semantics ⟨x, path⟩ =
+      semantics.1.boundary.emit x *
+        OpenNodeContext.boundaryTrace (Party := Party) (Δ := Δ)
+          (rest x) (semantics.2 x) path := by
+  rcases semantics with ⟨node, next⟩
+  rfl
+
+/-- A `TypeTree.node` emits the head boundary action and continues along the
+chosen tail. -/
+theorem OpenNodeContext.boundaryTrace_node {Party : Type u} {Δ : PortBoundary}
+    {X : Type w} (rest : X → TypeTree.{w})
+    (semantics : Decoration (OpenNodeContext.{u, w} Party Δ) (TypeTree.node X rest))
+    (x : X) (path : TypeTree.Path (rest x)) :
+    OpenNodeContext.boundaryTrace (Party := Party) (Δ := Δ)
+        (TypeTree.node X rest) semantics ⟨x, path⟩ =
+      semantics.1.boundary.emit x *
+        OpenNodeContext.boundaryTrace (Party := Party) (Δ := Δ)
+          (rest x) (semantics.2 x) path := by
+  rcases semantics with ⟨node, next⟩
+  rfl
+
 /--
 The open-world specialization of `StepOver`.
 
@@ -674,6 +716,12 @@ def boundaryTrace {Party : Type u} {Δ : PortBoundary} {P : Type v}
     (step : OpenStep Party Δ P) (tr : TypeTree.Path step.tree) : PFunctor.TraceList Δ.Out :=
   OpenNodeContext.boundaryTrace step.tree step.semantics tr
 
+/-- The boundary trace of an open step is the trace of its decorated interaction tree. -/
+theorem boundaryTrace_eq {Party : Type u} {Δ : PortBoundary} {P : Type v}
+    (step : OpenStep Party Δ P) (tr : TypeTree.Path step.tree) :
+    boundaryTrace step tr = OpenNodeContext.boundaryTrace step.tree step.semantics tr := by
+  rfl
+
 end OpenStep
 
 /--

PolyFun/PFunctor/Handler/Instrumentation.lean

@@ -0,0 +1,184 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma, Quang Dao
+-/
+
+module
+
+public import Mathlib.Control.Monad.Writer
+public import PolyFun.PFunctor.Handler
+
+/-!
+# Instrumenting Monadic Handlers
+
+This module provides effect-generic constructions for polynomial-functor
+handlers. `liftTarget` changes the target monad through `MonadLiftT`, while
+`preInsert` and `postInsert` add a side effect before or after each handled
+operation. The writer specializations record response-independent or
+response-dependent traces without depending on any oracle-specific API.
+-/
+
+public section
+
+universe u v w uA
+
+namespace PFunctor
+namespace Handler
+
+variable {P : PFunctor.{uA, u}}
+variable {m : Type u → Type v} {n : Type u → Type w}
+
+/-- Lift every operation of a handler into a new target monad. -/
+-- Keep this structural adapter transparent: dependent handler result types
+-- frequently need its pointwise reduction during elaboration.
+@[expose] def liftTarget (n : Type u → Type w) [MonadLiftT m n]
+    (handler : Handler m P) : Handler n P :=
+  fun operation => liftM (handler operation)
+
+@[simp]
+theorem liftTarget_apply (n : Type u → Type w) [MonadLiftT m n]
+    (handler : Handler m P) (operation : P.A) :
+    handler.liftTarget n operation = liftM (handler operation) :=
+  by rfl
+
+/-- Lifting a handler to its current target has no effect. -/
+@[simp]
+theorem liftTarget_self (handler : Handler m P) :
+    handler.liftTarget m = handler :=
+  by rfl
+
+/-- Run an effect before handling each operation.
+
+The inserted effect is sequenced before the underlying handler. Whether its
+effects remain observable if that handler subsequently fails depends on the
+target monad's transformer order; for example, `WriterT` over `Option` discards
+the log together with a failed result. The inserted effect's value is
+discarded. -/
+def preInsert [Monad n] [MonadLiftT m n] {α : Type u}
+    (handler : Handler m P) (before : P.A → n α) : Handler n P :=
+  fun operation => before operation *> liftM (handler operation)
+
+@[simp, grind =]
+theorem preInsert_apply [Monad n] [MonadLiftT m n] {α : Type u}
+    (handler : Handler m P) (before : P.A → n α) (operation : P.A) :
+    handler.preInsert before operation =
+      before operation *> liftM (handler operation) :=
+  by rfl
+
+/-- Run an effect after handling each operation.
+
+The inserted effect may depend on the response and is skipped if the
+underlying handler fails. Its result is discarded. -/
+def postInsert [Monad n] [MonadLiftT m n] {α : Type u}
+    (handler : Handler m P) (after : (operation : P.A) → P.B operation → n α) :
+    Handler n P :=
+  fun operation => do
+    let response ← liftM (handler operation)
+    let _ ← after operation response
+    return response
+
+@[simp, grind =]
+theorem postInsert_apply [Monad n] [MonadLiftT m n] {α : Type u}
+    (handler : Handler m P) (after : (operation : P.A) → P.B operation → n α)
+    (operation : P.A) :
+    handler.postInsert after operation = do
+      let response ← liftM (handler operation)
+      let _ ← after operation response
+      return response :=
+  by rfl
+
+/-! ## Writer traces -/
+
+variable [Monad m]
+
+/-- Record a response-independent trace before each handled operation. -/
+def withTraceBefore {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : P.A → ω) : Handler (WriterT ω m) P :=
+  handler.preInsert fun operation => tell (trace operation)
+
+@[simp, grind =]
+theorem withTraceBefore_apply {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : P.A → ω) (operation : P.A) :
+    handler.withTraceBefore trace operation = (do
+      tell (trace operation)
+      handler operation) :=
+  by rfl
+
+/-- Response-independent writer tracing is before-insertion of `tell`. -/
+theorem withTraceBefore_eq_preInsert {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : P.A → ω) :
+    handler.withTraceBefore trace =
+      handler.preInsert (fun operation => tell (trace operation)) := by
+  rfl
+
+/-- Record a response-dependent trace after each handled operation. -/
+def withTrace {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) :
+    Handler (WriterT ω m) P :=
+  handler.postInsert fun operation response => tell (trace operation response)
+
+@[simp, grind =]
+theorem withTrace_apply {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω)
+    (operation : P.A) :
+    handler.withTrace trace operation = do
+      let response ← handler operation
+      tell (trace operation response)
+      return response :=
+  by rfl
+
+/-- Response-dependent writer tracing is after-insertion of `tell`. -/
+theorem withTrace_eq_postInsert {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) :
+    handler.withTrace trace =
+      handler.postInsert (fun operation response => tell (trace operation response)) := by
+  rfl
+
+/-- Append-flavoured response-independent tracing. -/
+def withTraceAppendBefore {ω : Type u} [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : P.A → ω) : Handler (WriterT ω m) P :=
+  handler.preInsert fun operation => tell (trace operation)
+
+@[simp, grind =]
+theorem withTraceAppendBefore_apply {ω : Type u} [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : P.A → ω) (operation : P.A) :
+    handler.withTraceAppendBefore trace operation = (do
+      tell (trace operation)
+      handler operation) :=
+  by rfl
+
+/-- Append-flavoured before-tracing is before-insertion of `tell`. -/
+theorem withTraceAppendBefore_eq_preInsert {ω : Type u}
+    [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : P.A → ω) :
+    handler.withTraceAppendBefore trace =
+      handler.preInsert (fun operation => tell (trace operation)) := by
+  rfl
+
+/-- Append-flavoured response-dependent tracing. -/
+def withTraceAppend {ω : Type u} [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) :
+    Handler (WriterT ω m) P :=
+  handler.postInsert fun operation response => tell (trace operation response)
+
+@[simp, grind =]
+theorem withTraceAppend_apply {ω : Type u} [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω)
+    (operation : P.A) :
+    handler.withTraceAppend trace operation = do
+      let response ← handler operation
+      tell (trace operation response)
+      return response :=
+  by rfl
+
+/-- Append-flavoured after-tracing is after-insertion of `tell`. -/
+theorem withTraceAppend_eq_postInsert {ω : Type u}
+    [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) :
+    handler.withTraceAppend trace =
+      handler.postInsert (fun operation response => tell (trace operation response)) := by
+  rfl
+
+end Handler
+end PFunctor