feat(uc): sampler-level coherence shapes and the scheduled theory's laws

PolyFun.lean

@@ -125,6 +125,7 @@ public import PolyFun.Interaction.UC.OpenProcessCoherence
 public import PolyFun.Interaction.UC.OpenProcessFactorization
 public import PolyFun.Interaction.UC.OpenProcessInterleave
 public import PolyFun.Interaction.UC.OpenProcessModel
+public import PolyFun.Interaction.UC.OpenProcessSamplerCoherence
 public import PolyFun.Interaction.UC.OpenProcessSamplerEquiv
 public import PolyFun.Interaction.UC.OpenProcessSamplerFactorization
 public import PolyFun.Interaction.UC.OpenSyntax.AtomSubTheory

PolyFun/Interaction/UC/OpenProcessCoherence.lean

@@ -43,6 +43,7 @@ namespace Interaction
 namespace UC
 
 open Concurrent
+open PFunctor.FreeM.Displayed (Decoration)
 
 variable {m : Type w → Type w'} {Party : Type u}
 
@@ -133,6 +134,107 @@ theorem isSilentStep_interleave_right_iff {Δ₁ Δ₂ Δ : PortBoundary}
 
 end OpenProcess
 
+/-! ## Branches of a composite step -/
+
+namespace OpenProcess
+
+variable {Δ₁ Δ₂ Δ Δ' : PortBoundary}
+  (p₁ : OpenProcess.{u, v, w, w'} m Party Δ₁) (p₂ : OpenProcess.{u, v, w, w'} m Party Δ₂)
+  (f₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁)
+    (OpenNodeContext.{u, w} Party Δ))
+  (f₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂)
+    (OpenNodeContext.{u, w} Party Δ))
+  (c : OpenNodeContext.{u, w} Party Δ (ULift.{w, 0} Bool)) (σ : m (ULift.{w, 0} Bool))
+  (g : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ)
+    (OpenNodeContext.{u, w} Party Δ'))
+  (s₁ : p₁.Proc) (s₂ : p₂.Proc)
+
+/-- A left-scheduled composite step is silent when the scheduler node is and
+the re-decorated component step is. -/
+theorem isSilentStep_interleave_left_iff_decoration (tr : (p₁.step s₁).tree.Path) :
+    IsSilentStep (p₁.interleave p₂ f₁ f₂ c σ) (s₁, s₂) ⟨⟨true⟩, tr⟩ ↔
+      c.boundary.isActivated = false ∧
+        IsSilentDecoration (Decoration.map f₁ _ (p₁.step s₁).semantics) tr := by
+  simp only [IsSilentStep, OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep,
+    PFunctor.DynSystem.expose_mk', IsSilentDecoration]
+
+/-- A right-scheduled composite step is silent when the scheduler node is and
+the re-decorated component step is. -/
+theorem isSilentStep_interleave_right_iff_decoration (tr : (p₂.step s₂).tree.Path) :
+    IsSilentStep (p₁.interleave p₂ f₁ f₂ c σ) (s₁, s₂) ⟨⟨false⟩, tr⟩ ↔
+      c.boundary.isActivated = false ∧
+        IsSilentDecoration (Decoration.map f₂ _ (p₂.step s₂).semantics) tr := by
+  simp only [IsSilentStep, OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep,
+    PFunctor.DynSystem.expose_mk', IsSilentDecoration]
+
+/-- Silence of the left branch of a re-decorated composite step. -/
+theorem isSilentDecoration_map_interleave_left (tr : (p₁.step s₁).tree.Path) :
+    IsSilentDecoration
+        (Decoration.map g _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics)
+        ⟨⟨true⟩, tr⟩ ↔
+      (g _ c).boundary.isActivated = false ∧
+        IsSilentDecoration (Decoration.map g _ (Decoration.map f₁ _ (p₁.step s₁).semantics))
+          tr := by
+  simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep,
+    PFunctor.DynSystem.expose_mk', OpenNodeContext.decoration_map_node, IsSilentDecoration]
+
+/-- Silence of the right branch of a re-decorated composite step. -/
+theorem isSilentDecoration_map_interleave_right (tr : (p₂.step s₂).tree.Path) :
+    IsSilentDecoration
+        (Decoration.map g _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics)
+        ⟨⟨false⟩, tr⟩ ↔
+      (g _ c).boundary.isActivated = false ∧
+        IsSilentDecoration (Decoration.map g _ (Decoration.map f₂ _ (p₂.step s₂).semantics))
+          tr := by
+  simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep,
+    PFunctor.DynSystem.expose_mk', OpenNodeContext.decoration_map_node, IsSilentDecoration]
+
+/-- The boundary trace of a left-scheduled composite step. -/
+theorem boundaryTrace_interleave_left (tr : (p₁.step s₁).tree.Path) :
+    OpenNodeContext.boundaryTrace _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics
+        ⟨⟨true⟩, tr⟩ =
+      c.boundary.emit ⟨true⟩ *
+        OpenNodeContext.boundaryTrace _ (Decoration.map f₁ _ (p₁.step s₁).semantics) tr := by
+  simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep,
+    PFunctor.DynSystem.expose_mk']
+  exact OpenNodeContext.boundaryTrace_node _ _ _ _
+
+/-- The boundary trace of a right-scheduled composite step. -/
+theorem boundaryTrace_interleave_right (tr : (p₂.step s₂).tree.Path) :
+    OpenNodeContext.boundaryTrace _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics
+        ⟨⟨false⟩, tr⟩ =
+      c.boundary.emit ⟨false⟩ *
+        OpenNodeContext.boundaryTrace _ (Decoration.map f₂ _ (p₂.step s₂).semantics) tr := by
+  simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep,
+    PFunctor.DynSystem.expose_mk']
+  exact OpenNodeContext.boundaryTrace_node _ _ _ _
+
+/-- The boundary trace of the left branch of a re-decorated composite step. -/
+theorem boundaryTrace_map_interleave_left (tr : (p₁.step s₁).tree.Path) :
+    OpenNodeContext.boundaryTrace _
+        (Decoration.map g _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics)
+        ⟨⟨true⟩, tr⟩ =
+      (g _ c).boundary.emit ⟨true⟩ *
+        OpenNodeContext.boundaryTrace _
+          (Decoration.map g _ (Decoration.map f₁ _ (p₁.step s₁).semantics)) tr := by
+  simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep,
+    PFunctor.DynSystem.expose_mk', OpenNodeContext.decoration_map_node]
+  exact OpenNodeContext.boundaryTrace_node _ _ _ _
+
+/-- The boundary trace of the right branch of a re-decorated composite step. -/
+theorem boundaryTrace_map_interleave_right (tr : (p₂.step s₂).tree.Path) :
+    OpenNodeContext.boundaryTrace _
+        (Decoration.map g _ ((p₁.interleave p₂ f₁ f₂ c σ).step (s₁, s₂)).semantics)
+        ⟨⟨false⟩, tr⟩ =
+      (g _ c).boundary.emit ⟨false⟩ *
+        OpenNodeContext.boundaryTrace _
+          (Decoration.map g _ (Decoration.map f₂ _ (p₂.step s₂).semantics)) tr := by
+  simp only [OpenProcess.interleave, ProcessOver.interleave, ProcessOver.ofStep,
+    PFunctor.DynSystem.expose_mk', OpenNodeContext.decoration_map_node]
+  exact OpenNodeContext.boundaryTrace_node _ _ _ _
+
+end OpenProcess
+
 /-! ## The three coherence shapes -/
 
 section Shapes

PolyFun/Interaction/UC/OpenProcessFactorization.lean

@@ -7,6 +7,7 @@ Authors: Devon Tuma
 module
 
 public import PolyFun.Interaction.UC.OpenProcessModel
+public import PolyFun.Interaction.UC.OpenProcessSamplerCoherence
 
 /-!
 # Plug factorization for the process model, up to activation equivalence
@@ -41,8 +42,9 @@ with the context, and the inner pair is commuted under
 composite under `OpenProcess.interleave_congr_left`.
 
 `OpenProcessFactorization.sourceSchedule`, `leftSchedule`, and `rightSchedule`
-record the scheduler truth tables of the two sides; the sampler-aware laws
-consume them.
+record the scheduler truth tables of the two sides, indexed by the leaf type
+`OpenProcessFactorization.Leaf` of `OpenProcessSamplerCoherence`; the
+sampler-aware laws consume them.
 -/
 
 public section
@@ -63,14 +65,6 @@ variable (schedulerSampler : m (ULift.{w, 0} Bool))
 
 namespace OpenProcessFactorization
 
-/-- The component selected after flattening either side of a plug
-factorization. -/
-inductive Leaf where
-  | first
-  | second
-  | context
-  deriving DecidableEq, Repr
-
 /-- Scheduler choices on the source shape `plug (compose W₁ W₂) K`.
 The outer choice is listed first; the inner choice is present only when the
 composite is selected. -/

PolyFun/Interaction/UC/OpenProcessInterleave.lean

@@ -47,6 +47,7 @@ namespace Interaction
 namespace UC
 
 open Concurrent
+open PFunctor.FreeM.Displayed (Decoration)
 
 /-! ## Activation-preserving context homs -/
 
@@ -106,6 +107,182 @@ theorem preservesActivation_close (Δ : PortBoundary) :
   intro X ons
   simp [OpenNodeContext.close, BoundaryAction.closed]
 
+/-! ## Internal nodes and trace relabelling
+
+The sampler-level coherence theorems compare boundary traces, so they need two
+finer pieces of data about a hom than activation preservation: whether a node
+is fully internal after the hom, and how the hom acts on emitted traces. -/
+
+/-- A node that is neither activated nor emits anything: the boundary action
+of a scheduler node after any of the theory's boundary adaptations. -/
+@[expose]
+def IsInternalNode {Δ : PortBoundary} {X : Type w} (c : OpenNodeContext.{u, w} Party Δ X) :
+    Prop :=
+  c.boundary = BoundaryAction.internal Δ X
+
+theorem IsInternalNode.isActivated {Δ : PortBoundary} {X : Type w}
+    {c : OpenNodeContext.{u, w} Party Δ X} (hc : IsInternalNode c) :
+    c.boundary.isActivated = false := by
+  rw [hc]; rfl
+
+theorem IsInternalNode.emit {Δ : PortBoundary} {X : Type w}
+    {c : OpenNodeContext.{u, w} Party Δ X} (hc : IsInternalNode c) (x : X) :
+    c.boundary.emit x = 1 := by
+  rw [hc]; rfl
+
+theorem IsInternalNode.map {Δ₁ Δ₂ : PortBoundary} {X : Type w}
+    {c : OpenNodeContext.{u, w} Party Δ₁ X} (hc : IsInternalNode c) (φ : PortBoundary.Hom Δ₁ Δ₂) :
+    IsInternalNode (OpenNodeContext.map Party φ X c) := by
+  unfold IsInternalNode at hc ⊢
+  simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, hc, BoundaryAction.mapBoundary,
+    BoundaryAction.internal]
+
+theorem IsInternalNode.inlTensor {Δ₁ : PortBoundary} (Δ₂ : PortBoundary) {X : Type w}
+    {c : OpenNodeContext.{u, w} Party Δ₁ X} (hc : IsInternalNode c) :
+    IsInternalNode (OpenNodeContext.inlTensor Party Δ₁ Δ₂ X c) := by
+  unfold IsInternalNode at hc ⊢
+  simp [OpenNodeContext.inlTensor, hc, BoundaryAction.embedInlTensor, BoundaryAction.internal]
+
+theorem IsInternalNode.inrTensor (Δ₁ : PortBoundary) {Δ₂ : PortBoundary} {X : Type w}
+    {c : OpenNodeContext.{u, w} Party Δ₂ X} (hc : IsInternalNode c) :
+    IsInternalNode (OpenNodeContext.inrTensor Party Δ₁ Δ₂ X c) := by
+  unfold IsInternalNode at hc ⊢
+  simp [OpenNodeContext.inrTensor, hc, BoundaryAction.embedInrTensor, BoundaryAction.internal]
+
+theorem IsInternalNode.wireLeft {Δ₁ Γ : PortBoundary} (Δ₂ : PortBoundary) {X : Type w}
+    {c : OpenNodeContext.{u, w} Party (PortBoundary.tensor Δ₁ Γ) X} (hc : IsInternalNode c) :
+    IsInternalNode (OpenNodeContext.wireLeft Party Δ₁ Γ Δ₂ X c) := by
+  unfold IsInternalNode at hc ⊢
+  simp [OpenNodeContext.wireLeft, hc, BoundaryAction.wireLeft, BoundaryAction.internal]
+
+theorem IsInternalNode.wireRight (Δ₁ : PortBoundary) {Γ Δ₂ : PortBoundary} {X : Type w}
+    {c : OpenNodeContext.{u, w} Party (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂) X}
+    (hc : IsInternalNode c) :
+    IsInternalNode (OpenNodeContext.wireRight Party Δ₁ Γ Δ₂ X c) := by
+  unfold IsInternalNode at hc ⊢
+  simp [OpenNodeContext.wireRight, hc, BoundaryAction.wireRight, BoundaryAction.internal]
+
+theorem IsInternalNode.close {Δ : PortBoundary} {X : Type w}
+    {c : OpenNodeContext.{u, w} Party Δ X} (hc : IsInternalNode c) :
+    IsInternalNode (OpenNodeContext.close Party Δ X c) := by
+  unfold IsInternalNode at hc ⊢
+  simp [OpenNodeContext.close, hc, BoundaryAction.closed, BoundaryAction.internal]
+
+/-- A hom **emits along** a partial relabelling `g` of output packets when it
+acts on every node's emitted trace by `g`. All of the theory's boundary
+adaptations do. -/
+@[expose]
+def EmitsAlong {Δ₁ Δ₂ : PortBoundary}
+    (h : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁)
+      (OpenNodeContext.{u, w} Party Δ₂))
+    (g : PFunctor.Idx Δ₁.Out → Option (PFunctor.Idx Δ₂.Out)) : Prop :=
+  ∀ (X : Type w) (ons : OpenNodeContext Party Δ₁ X),
+    (h X ons).boundary.emit = PFunctor.Trace.mapPartial g ons.boundary.emit
+
+theorem emitsAlong_id (Δ : PortBoundary) :
+    EmitsAlong (TypeTree.Node.ContextHom.id (OpenNodeContext.{u, w} Party Δ))
+      (fun i => some i) := by
+  intro X ons
+  simp [TypeTree.Node.ContextHom.id]
+
+theorem EmitsAlong.comp {Δ₁ Δ₂ Δ₃ : PortBoundary}
+    {h₂ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂)
+      (OpenNodeContext.{u, w} Party Δ₃)}
+    {h₁ : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁)
+      (OpenNodeContext.{u, w} Party Δ₂)}
+    {g₂ : PFunctor.Idx Δ₂.Out → Option (PFunctor.Idx Δ₃.Out)}
+    {g₁ : PFunctor.Idx Δ₁.Out → Option (PFunctor.Idx Δ₂.Out)}
+    (hh₂ : EmitsAlong h₂ g₂) (hh₁ : EmitsAlong h₁ g₁) :
+    EmitsAlong (TypeTree.Node.ContextHom.comp h₂ h₁) (fun i => (g₁ i).bind g₂) := by
+  intro X ons
+  change (h₂ X (h₁ X ons)).boundary.emit = _
+  rw [hh₂, hh₁, PFunctor.Trace.mapPartial_comp]
+
+theorem emitsAlong_map {Δ₁ Δ₂ : PortBoundary} (φ : PortBoundary.Hom Δ₁ Δ₂) :
+    EmitsAlong (OpenNodeContext.map.{u, w} Party φ)
+      (fun i => some (PFunctor.Chart.mapIdx φ.onOut i)) := by
+  intro X ons
+  simp [OpenNodeContext.map, OpenNodeProfile.mapBoundary, BoundaryAction.mapBoundary,
+    PFunctor.Trace.mapChart]
+
+theorem emitsAlong_inlTensor (Δ₁ Δ₂ : PortBoundary) :
+    EmitsAlong (OpenNodeContext.inlTensor.{u, w} Party Δ₁ Δ₂)
+      (fun i => some (PFunctor.Chart.mapIdx (Interface.Hom.inl Δ₁.Out Δ₂.Out) i)) := by
+  intro X ons
+  simp [OpenNodeContext.inlTensor, BoundaryAction.embedInlTensor, PFunctor.Trace.mapChart]
+
+theorem emitsAlong_inrTensor (Δ₁ Δ₂ : PortBoundary) :
+    EmitsAlong (OpenNodeContext.inrTensor.{u, w} Party Δ₁ Δ₂)
+      (fun i => some (PFunctor.Chart.mapIdx (Interface.Hom.inr Δ₁.Out Δ₂.Out) i)) := by
+  intro X ons
+  simp [OpenNodeContext.inrTensor, BoundaryAction.embedInrTensor, PFunctor.Trace.mapChart]
+
+theorem emitsAlong_wireLeft (Δ₁ Γ Δ₂ : PortBoundary) :
+    EmitsAlong (OpenNodeContext.wireLeft.{u, w} Party Δ₁ Γ Δ₂)
+      (fun
+        | ⟨Sum.inl a₁, m⟩ => some ⟨Sum.inl a₁, m⟩
+        | ⟨Sum.inr _, _⟩ => none) := by
+  intro X ons
+  simp only [OpenNodeContext.wireLeft, BoundaryAction.wireLeft]
+  exact congrArg (fun g => PFunctor.Trace.mapPartial g _)
+    (funext fun i => by rcases i with ⟨(_ | _), _⟩ <;> rfl)
+
+theorem emitsAlong_wireRight (Δ₁ Γ Δ₂ : PortBoundary) :
+    EmitsAlong (OpenNodeContext.wireRight.{u, w} Party Δ₁ Γ Δ₂)
+      (fun
+        | ⟨Sum.inl _, _⟩ => none
+        | ⟨Sum.inr a₂, m⟩ => some ⟨Sum.inr a₂, m⟩) := by
+  intro X ons
+  simp only [OpenNodeContext.wireRight, BoundaryAction.wireRight]
+  exact congrArg (fun g => PFunctor.Trace.mapPartial g _)
+    (funext fun i => by rcases i with ⟨(_ | _), _⟩ <;> rfl)
+
+theorem emitsAlong_close (Δ : PortBoundary) :
+    EmitsAlong (OpenNodeContext.close.{u, w} Party Δ) (fun _ => none) := by
+  intro X ons
+  funext x
+  simp only [OpenNodeContext.close, BoundaryAction.closed, PFunctor.Trace.mapPartial_apply]
+  exact (List.filterMap_eq_nil_iff.mpr fun _ _ => rfl).symm
+
+/-- Re-decorating a node applies the hom at the node and recursively below. -/
+theorem decoration_map_node {Δ₁ Δ₂ : PortBoundary}
+    (h : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁)
+      (OpenNodeContext.{u, w} Party Δ₂))
+    {X : Type w} (rest : X → TypeTree.{w})
+    (d : Decoration (OpenNodeContext.{u, w} Party Δ₁) (TypeTree.node X rest)) :
+    Decoration.map h (TypeTree.node X rest) d =
+      ⟨h X d.1, fun x => Decoration.map h (rest x) (d.2 x)⟩ :=
+  rfl
+
+/-- Re-decorating twice is re-decorating along the composite. -/
+theorem decoration_map_map {Δ₁ Δ₂ Δ₃ : PortBoundary}
+    (g : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₂)
+      (OpenNodeContext.{u, w} Party Δ₃))
+    (f : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁)
+      (OpenNodeContext.{u, w} Party Δ₂))
+    (spec : TypeTree.{w}) (d : Decoration (OpenNodeContext.{u, w} Party Δ₁) spec) :
+    Decoration.map g spec (Decoration.map f spec d) =
+      Decoration.map (TypeTree.Node.ContextHom.comp g f) spec d :=
+  TypeTree.Decoration.map_comp g f spec d
+
+/-- Boundary traces after a hom that emits along `g` are the `g`-relabelled
+traces. -/
+theorem boundaryTrace_map_of_emitsAlong {Δ₁ Δ₂ : PortBoundary}
+    {h : TypeTree.Node.ContextHom (OpenNodeContext.{u, w} Party Δ₁)
+      (OpenNodeContext.{u, w} Party Δ₂)}
+    {g : PFunctor.Idx Δ₁.Out → Option (PFunctor.Idx Δ₂.Out)} (hg : EmitsAlong h g) :
+    ∀ {spec : TypeTree.{w}} (d : Decoration (OpenNodeContext.{u, w} Party Δ₁) spec)
+      (tr : spec.Path),
+      boundaryTrace spec (Decoration.map h spec d) tr =
+        PFunctor.TraceList.mapPartial g (boundaryTrace spec d tr)
+  | .done, _, _ => by
+    rw [boundaryTrace_done, boundaryTrace_done, PFunctor.TraceList.mapPartial_one]
+  | .node _ rest, d, ⟨x, tr⟩ => by
+    rw [decoration_map_node, boundaryTrace_node, boundaryTrace_node,
+      boundaryTrace_map_of_emitsAlong hg (d.2 x) tr, hg, PFunctor.TraceList.mapPartial_mul]
+    rfl
+
+
 end OpenNodeContext
 
 namespace OpenProcess