feat(interaction): allowed-systems sub-theories and relativized emulation

AGENTS.md

@@ -74,7 +74,12 @@ and depend on this library.
     interleaving, observation.
   - `UC/`: open-process / open-theory layer, structural composition
     (interfaces, par, wire, plug), corruption models, environment
-    actions, leakage. *Generic only* — security-flavored UC layers
+    actions, leakage, and composition-closed sub-theories (`SubTheory`, a
+    boundary-indexed membership predicate, with contextual emulation
+    relativized to its allowed closing contexts). This relativization does not
+    assert real/ideal protocol membership, resource bounds, simulator
+    realizability, or a connection to `CorruptionModel`; those require explicit
+    downstream bridges. *Generic only* — security-flavored UC layers
     (computational equivalence, asymptotic security) live in VCVio.
 - `PolyFun/Control/`: monad and comonad infrastructure transitively
   required by the above (coalgebra, comonad, free / freecont monad

PolyFun.lean

@@ -101,6 +101,7 @@ public import PolyFun.Interaction.TwoParty.Swap
 public import PolyFun.Interaction.TwoParty.Syntax
 public import PolyFun.Interaction.UC.CorruptionModel
 public import PolyFun.Interaction.UC.Emulates
+public import PolyFun.Interaction.UC.EmulatesWithin
 public import PolyFun.Interaction.UC.EnvAction
 public import PolyFun.Interaction.UC.EnvOpenProcess
 public import PolyFun.Interaction.UC.Interface
@@ -110,10 +111,12 @@ public import PolyFun.Interaction.UC.MomentaryCorruption
 public import PolyFun.Interaction.UC.Notation
 public import PolyFun.Interaction.UC.OpenProcess
 public import PolyFun.Interaction.UC.OpenProcessModel
+public import PolyFun.Interaction.UC.OpenSyntax.AtomSubTheory
 public import PolyFun.Interaction.UC.OpenSyntax.Expr
 public import PolyFun.Interaction.UC.OpenSyntax.Interp
 public import PolyFun.Interaction.UC.OpenSyntax.Raw
 public import PolyFun.Interaction.UC.OpenTheory
+public import PolyFun.Interaction.UC.SubTheory
 public import PolyFun.Logic.HEq
 public import PolyFun.PFunctor.Adjunctions
 public import PolyFun.PFunctor.Basic

PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean

@@ -0,0 +1,201 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+
+module
+
+public import PolyFun.Interaction.UC.OpenSyntax.Expr
+public import PolyFun.Interaction.UC.SubTheory
+
+/-!
+# Sub-theories of the free open theory, generated by allowed atoms
+
+The free model is already presented by generators. A predicate on atoms gives
+a canonical sub-theory of `Expr.theory Atom`: fix which primitive components
+may be used, then close them under `map`, `par`, and `wire`.
+
+`atomSubTheory A` is that sub-theory. Its generators are the atoms satisfying
+`A` together with the identity wires, which are structure rather than
+components and so are always allowed.
+
+## The transfer theorem
+
+`mem_interpret_of_atoms` is the reason this file exists. It says: if every
+allowed atom interprets into a target sub-theory `D`, then every syntactic
+system built from allowed atoms interprets into `D`.
+
+The result is purely structural. Any resource, corruption, or realizability
+interpretation of `D.mem` requires a separate bridge establishing that
+interpretation and its closure laws.
+
+## Why this needs no reasoning about the quotient
+
+`Expr` is a quotient of `Raw` by the open-theory equations, so a predicate
+defined by structural recursion on `Raw` would have to be shown invariant
+under all twenty-odd equations. `SubTheory.generated` sidesteps that entirely:
+it is defined by the *operations of the theory*, which act on the quotient
+already, so `atomSubTheory` is well-defined by construction and its induction
+principle is `SubTheory.generated_le`.
+
+A consequence worth stating: membership is extensional on the quotient but is
+not generally decidable. `atomSubTheory A` contains every expression that can
+be assembled from allowed atoms, and equality in `Expr` preserves membership.
+-/
+
+public section
+
+universe u v
+
+namespace Interaction
+namespace UC
+namespace OpenSyntax
+
+/--
+The generators of a syntactic sub-theory: the atoms allowed by `A`, together
+with the identity wires.
+
+Identity wires are included unconditionally because they are the wires of the
+diagram rather than components in it. A class of protocols closed under
+rewiring must contain them, and no restriction on primitive components can
+sensibly forbid them.
+
+`Atom` is an explicit parameter here and in `atomSubTheory`: it cannot be
+recovered from the type of `A`, since solving `?Atom ?Δ ≡ Atom Δ` is not a
+first-order problem.
+-/
+inductive AllowedGen (Atom : PortBoundary → Type u)
+    (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop) :
+    ∀ (Δ : PortBoundary), Expr Atom Δ → Prop where
+  /-- An allowed atom is a generator. -/
+  | atom {Δ : PortBoundary} {a : Atom Δ} : A a → AllowedGen Atom A Δ (Expr.atom a)
+  /-- Every identity wire is a generator. -/
+  | idWire (Γ : PortBoundary) :
+      AllowedGen Atom A (PortBoundary.tensor (PortBoundary.swap Γ) Γ) (Expr.idWire Γ)
+
+/--
+The sub-theory of `Expr.theory Atom` generated by the atoms satisfying `A`.
+
+This is the formal counterpart of "the protocols one is allowed to write":
+a choice of primitive components, closed under the composition operations.
+-/
+@[expose]
+def atomSubTheory (Atom : PortBoundary → Type u)
+    (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop) : SubTheory (Expr.theory Atom) :=
+  SubTheory.generated (Expr.theory Atom) (AllowedGen Atom A)
+
+namespace atomSubTheory
+
+/-- An allowed atom is an allowed system. -/
+theorem mem_atom (Atom : PortBoundary → Type u) (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop)
+    {Δ : PortBoundary} {a : Atom Δ} (ha : A a) :
+    (atomSubTheory Atom A).mem (Expr.atom a) :=
+  SubTheory.Generated.base (AllowedGen.atom ha)
+
+/-- Identity wires are always allowed. -/
+theorem mem_idWire (Atom : PortBoundary → Type u) (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop)
+    (Γ : PortBoundary) : (atomSubTheory Atom A).mem (Expr.idWire Γ) :=
+  SubTheory.Generated.base (AllowedGen.idWire Γ)
+
+instance isStructural (Atom : PortBoundary → Type u)
+    (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop) : (atomSubTheory Atom A).IsStructural where
+  mem_unit :=
+    -- `Expr.unit` is `idWire` on the empty boundary pushed through a unitor.
+    SubTheory.Generated.map
+      (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom
+      (mem_idWire Atom A PortBoundary.empty)
+  mem_idWire Γ := mem_idWire Atom A Γ
+
+/-- Allowing more atoms yields a larger sub-theory. -/
+theorem mono (Atom : PortBoundary → Type u)
+    {A₁ A₂ : ∀ {Δ : PortBoundary}, Atom Δ → Prop}
+    (h : ∀ {Δ : PortBoundary} (a : Atom Δ), A₁ a → A₂ a) :
+    atomSubTheory Atom A₁ ≤ atomSubTheory Atom A₂ :=
+  SubTheory.generated_mono fun _ _ hg => by
+    cases hg with
+    | atom ha => exact AllowedGen.atom (h _ ha)
+    | idWire Γ => exact AllowedGen.idWire Γ
+
+end atomSubTheory
+
+/--
+The pullback of a sub-theory of `T` along an interpretation of atoms.
+
+An expression is allowed exactly when its interpretation is. This is a
+sub-theory because `Expr.interpret` commutes with every operation, so each
+closure field is the target's closure field transported across one rewrite.
+
+It exists so that the transfer theorem below can be an application of
+`SubTheory.generated_le` rather than a fresh induction: the induction was
+done once, in the induction principle.
+-/
+@[expose]
+def interpretSubTheory (Atom : PortBoundary → Type u) {T : OpenTheory.{v}}
+    [OpenTheory.HasPlugWireFactor T] (D : SubTheory T)
+    (interp : ∀ {Δ : PortBoundary}, Atom Δ → T.Obj Δ) : SubTheory (Expr.theory Atom) where
+  mem e := D.mem (e.interpret T interp)
+  mem_map φ h := by simpa only [Expr.interpret_map] using D.mem_map φ h
+  mem_par h₁ h₂ := by simpa only [Expr.interpret_par] using D.mem_par h₁ h₂
+  mem_wire h₁ h₂ := by simpa only [Expr.interpret_wire] using D.mem_wire h₁ h₂
+
+instance isPlugClosed_interpretSubTheory (Atom : PortBoundary → Type u) {T : OpenTheory.{v}}
+    [OpenTheory.HasPlugWireFactor T] (D : SubTheory T)
+    (interp : ∀ {Δ : PortBoundary}, Atom Δ → T.Obj Δ) :
+    (interpretSubTheory Atom D interp).IsPlugClosed where
+  mem_plug h₁ h₂ := by
+    simpa only [Expr.interpret_plug] using SubTheory.IsPlugClosed.mem_plug h₁ h₂
+
+instance isStructural_interpretSubTheory (Atom : PortBoundary → Type u) {T : OpenTheory.{v}}
+    [OpenTheory.HasPlugWireFactor T] (D : SubTheory T) [D.IsStructural]
+    (interp : ∀ {Δ : PortBoundary}, Atom Δ → T.Obj Δ) :
+    (interpretSubTheory Atom D interp).IsStructural where
+  mem_unit := by
+    change D.mem ((Expr.unit : Expr Atom PortBoundary.empty).interpret T interp)
+    rw [Expr.interpret_unit]
+    exact SubTheory.IsStructural.mem_unit
+  -- `Expr.interpret_idWire` is `rfl`, so this case is definitional.
+  mem_idWire Γ := SubTheory.IsStructural.mem_idWire (D := D) Γ
+
+/--
+**Transfer of allowedness along interpretation.**
+
+If every atom allowed by `A` interprets into the target sub-theory `D`, then
+every expression built from allowed atoms interprets into `D`.
+
+Nothing about the target is used beyond its structural and closure fields. Any
+stronger interpretation of target membership is external to this theorem.
+
+This is the structural form of the assumption that a network of admissible
+machines is admissible: instead of a global claim about networks, one supplies
+the generators (`hA`) and the closure fields carried by `D` itself.
+-/
+theorem mem_interpret_of_atoms (Atom : PortBoundary → Type u)
+    (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop)
+    {T : OpenTheory.{v}} [OpenTheory.HasPlugWireFactor T] (D : SubTheory T) [D.IsStructural]
+    (interp : ∀ {Δ : PortBoundary}, Atom Δ → T.Obj Δ)
+    (hA : ∀ {Δ : PortBoundary} (a : Atom Δ), A a → D.mem (interp a))
+    {Δ : PortBoundary} {e : Expr Atom Δ} (he : (atomSubTheory Atom A).mem e) :
+    D.mem (e.interpret T interp) :=
+  SubTheory.mem_of_le
+    (SubTheory.generated_le (interpretSubTheory Atom D interp) fun _ _ hg => by
+      -- Both `Expr.interpret_atom` and `Expr.interpret_idWire` hold by `rfl`,
+      -- so each generator case is discharged definitionally.
+      cases hg with
+      | atom ha => exact hA _ ha
+      | idWire Γ => exact SubTheory.IsStructural.mem_idWire (D := D) Γ)
+    he
+
+/-- The whole allowed class transfers at once: `atomSubTheory` sits inside the
+pullback of any target sub-theory that accepts the allowed atoms. -/
+theorem atomSubTheory_le_interpretSubTheory (Atom : PortBoundary → Type u)
+    (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop)
+    {T : OpenTheory.{v}} [OpenTheory.HasPlugWireFactor T] (D : SubTheory T) [D.IsStructural]
+    (interp : ∀ {Δ : PortBoundary}, Atom Δ → T.Obj Δ)
+    (hA : ∀ {Δ : PortBoundary} (a : Atom Δ), A a → D.mem (interp a)) :
+    atomSubTheory Atom A ≤ interpretSubTheory Atom D interp :=
+  fun _ he => mem_interpret_of_atoms Atom A D interp hA he
+
+end OpenSyntax
+end UC
+end Interaction