From d6014904a285d6c307d33fc3a7a05f2caf09570c Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Sat, 8 Aug 2026 13:29:08 -0500 Subject: [PATCH 1/5] refactor(interaction): let the observation carry the UC factorization laws The UC composition theorems previously required `OpenTheory.HasPlugWireFactor`, a strict compact-closed structure that the process-backed `openTheory` cannot supply: every binary composition prepends a scheduler node, so regrouping one is a delay bisimulation rather than an identity. State the same motions as properties of the observation instead, through `Observation.RespectsPlugComm` and `Observation.RespectsFactorization`. Strict coherence is the degenerate case, so the free syntax models are unaffected, and a model that can only offer a scheduling-insensitive observation now participates: `Emulates.plug_right` and `Emulates.plug_compose` apply to `openTheory` for the first time. Co-Authored-By: Claude Opus 5 --- PolyFun.lean | 1 + PolyFun/Interaction/UC/Emulates.lean | 226 +++++++++++------- .../Interaction/UC/OpenProcessEmulates.lean | 103 ++++++++ .../UC/EmulatesFactorizationExamples.lean | 109 +++++++++ docs/wiki/interaction.md | 3 +- docs/wiki/repo-map.md | 5 + 6 files changed, 365 insertions(+), 82 deletions(-) create mode 100644 PolyFun/Interaction/UC/OpenProcessEmulates.lean create mode 100644 PolyFunTest/Interaction/UC/EmulatesFactorizationExamples.lean diff --git a/PolyFun.lean b/PolyFun.lean index 55153ac..6a12dd1 100644 --- a/PolyFun.lean +++ b/PolyFun.lean @@ -109,6 +109,7 @@ public import PolyFun.Interaction.UC.MachineId public import PolyFun.Interaction.UC.MomentaryCorruption public import PolyFun.Interaction.UC.Notation public import PolyFun.Interaction.UC.OpenProcess +public import PolyFun.Interaction.UC.OpenProcessEmulates public import PolyFun.Interaction.UC.OpenProcessModel public import PolyFun.Interaction.UC.OpenSyntax.Expr public import PolyFun.Interaction.UC.OpenSyntax.Interp diff --git a/PolyFun/Interaction/UC/Emulates.lean b/PolyFun/Interaction/UC/Emulates.lean index 8b583aa..910752c 100644 --- a/PolyFun/Interaction/UC/Emulates.lean +++ b/PolyFun/Interaction/UC/Emulates.lean @@ -55,10 +55,27 @@ isos, asymptotic computational indistinguishability) supply their own * `Emulates.plug_compose`: both protocol and environment emulation compose to yield observational equivalence of the closed systems. -These rely on structural factorization lemmas -(`close_par_left`, `close_par_right`, `close_wire_left`, -`close_wire_right`, `plug_comm`) that capture monoidal coherence -identities, derived from the `CompactClosed` axioms. +These take their structural input from the observation rather than from the +theory, through two classes: + +* `Observation.RespectsPlugComm Obs` says `Obs` cannot see a closed system's + two halves exchanging roles. `plug_right` and `plug_compose` need only this. +* `Observation.RespectsFactorization Obs` extends it with the `Obs.rel` + readings of `close_par_left`, `close_par_right`, `close_wire_left`, and + `close_wire_right`, and is what the `par` and `wire` theorems need. + +A theory with strict compact-closed structure satisfies both for *every* +observation, via `respectsFactorization_of_hasPlugWireFactor`, so the free +models (`Expr.theory`, `Interp.theory`) are unaffected. Stating the laws on +the observation is what lets a model whose coherences hold only up to a +quotient — the process-backed `openTheory`, whose composites differ by +scheduler nodes — participate at all. + +Note that `Emulates · · Obs`, read as a family indexed by boundary, is itself +closed under exactly these motions: `par_compose` and `wire_left` are the +parallel and sequential closure conditions one would assume of an abstract +indistinguishability relation. The classes make that closure the interface +instead of a consequence. ## Design note: why `Observation` requires a full `Equivalence` @@ -168,49 +185,6 @@ theorem plug_invariance {Δ : PortBoundary} {Obs : Observation T} {real ideal : (h : Emulates real ideal Obs) (K : T.Plug Δ) : Obs.rel (T.close real K) (T.close ideal K) := h.compare K -/-! ### Composition up to a plug-commutation observation - -The `plug`-composition theorems below (`plug_right`, `plug_compose`) are stated -for theories with the full compact-closed `HasPlugWireFactor` structure, which -provides `plug_comm` as a strict equality. The concrete process model -`openTheory` is *not* `HasPlugWireFactor` on the nose — its coherences hold only -up to coarse activation equivalence — so those theorems do not apply to it -directly. - -The `_of_observes_plug_comm` variants replace the strict-equality dependency with a single -hypothesis: that `plug` commutes *up to the observation `Obs`*. The -`HasPlugWireFactor` versions are the special case where `Obs`-commutation is -`plug_comm` composed with reflexivity. A concrete model must supply an -observation that retains the events its security statement intends to expose; -a scheduler-only structural relation is not sufficient by itself. -/ - -/-- `Obs.rel`-relative `plug_right`: given that `plug` commutes up to the -observation `Obs`, replacing the plug (environment) while keeping the protocol -`W` fixed preserves the observation. No compact-closed structure is required. -/ -theorem plug_right_of_observes_plug_comm {Δ : PortBoundary} {Obs : Observation T} - (hcomm : ∀ (W : T.Obj Δ) (K : T.Obj (PortBoundary.swap Δ)), - Obs.rel (T.plug W K) (T.plug K W)) - (W : T.Obj Δ) {K₁ K₂ : T.Obj (PortBoundary.swap Δ)} (hK : Emulates K₁ K₂ Obs) : - Obs.rel (T.close W K₁) (T.close W K₂) := - Obs.equiv.trans (hcomm W K₁) - (Obs.equiv.trans (hK.compare W) (Obs.equiv.symm (hcomm W K₂))) - -/-- `Obs.rel`-relative **UC `plug`-composition**: if the protocol emulates its -ideal and the environment emulates its ideal, and `plug` commutes up to the -observation `Obs`, then the closed real-world execution is `Obs`-related to the -closed ideal-world execution. The proof is the standard hybrid through -`T.close ideal K_real`: `plug_invariance` (same environment, different protocol, -needs no structure) then `plug_right_of_observes_plug_comm` (same protocol, different -environment). -/ -theorem plug_compose_of_observes_plug_comm {Δ : PortBoundary} {Obs : Observation T} - (hcomm : ∀ (W : T.Obj Δ) (K : T.Obj (PortBoundary.swap Δ)), - Obs.rel (T.plug W K) (T.plug K W)) - {real ideal : T.Obj Δ} {K_real K_ideal : T.Obj (PortBoundary.swap Δ)} - (hProt : Emulates real ideal Obs) (hEnv : Emulates K_real K_ideal Obs) : - Obs.rel (T.close real K_real) (T.close ideal K_ideal) := - Obs.equiv.trans (hProt.plug_invariance K_real) - (plug_right_of_observes_plug_comm hcomm ideal hEnv) - end Emulates /-! ## Structural factorization of `close` under composition -/ @@ -365,31 +339,116 @@ theorem OpenTheory.plug_comm {Δ : PortBoundary} (W : T.Obj Δ) (K : T.Obj (Port end Factorization +/-! ## Observation-level factorization laws + +The composition theorems below all move a component across the divide between +the system under test and its context. In a theory with strict compact-closed +structure that motion is an equality — `close_par_left` and its siblings — so +the theorems can rewrite with it. The concrete process model `openTheory` does +not have those equalities on the nose: every binary composition prepends a +scheduler node, so regrouping one is a delay bisimulation rather than an +identity. + +The classes here name the same motions as properties of the *observation* +instead of the theory. A model that cannot offer strict coherence can still +offer an observation coarse enough not to see the regrouping, and then earns +the full composition suite. Strict coherence is the degenerate case, recorded +by `respectsFactorization_of_hasPlugWireFactor`, so nothing that holds today +is lost. + +Splitting the laws across two classes follows the same principle as the +`IsMonoidal → IsTraced → IsCompactClosed` chain in `OpenTheory`: a model +declares exactly the strength it can honestly satisfy. `RespectsPlugComm` +alone already supports `Emulates.plug_right` and `Emulates.plug_compose`. +-/ + +/-- +`Obs.RespectsPlugComm` states that `Obs` cannot distinguish a closed system +from the same system with the roles of its two halves exchanged. + +This is the weaker of the two layers, and the one a scheduler-quotienting +observation can supply without any monoidal coherence. It is exactly what +`Emulates.plug_right` and `Emulates.plug_compose` consume. +-/ +class Observation.RespectsPlugComm {T : OpenTheory.{u}} (Obs : Observation T) : Prop where + /-- Exchanging a system with its context is invisible to `Obs`. -/ + plug_comm : ∀ {Δ : PortBoundary} (W : T.Obj Δ) (K : T.Obj (PortBoundary.swap Δ)), + Obs.rel (T.plug W K) (T.plug K W) + +/-- +`Obs.RespectsFactorization` states that `Obs` additionally cannot see one +component of a `par` or `wire` composite being absorbed into the context. + +These are the `Obs.rel` readings of `close_par_left`, `close_par_right`, +`close_wire_left`, and `close_wire_right`. Together with the inherited +`plug_comm` they are the whole structural input to the UC composition +theorems, which is why the theorems below take this class rather than +`OpenTheory.HasPlugWireFactor`. + +Deliberately *not* an extension of `OpenTheory.IsCompactClosed`: the concrete +process model has neither a `HasUnit` nor a `HasIdWire` instance, and +requiring them here would put the class out of its reach for no gain. +-/ +class Observation.RespectsFactorization {T : OpenTheory.{u}} (Obs : Observation T) : Prop + extends Obs.RespectsPlugComm where + /-- Absorbing the right component of a `par` into the context is invisible + to `Obs`. -/ + close_par_left : ∀ {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) + (K : T.Plug (PortBoundary.tensor Δ₁ Δ₂)), + Obs.rel (T.close (T.par W₁ W₂) K) (T.close W₁ (T.parContextLeft W₂ K)) + /-- Absorbing the left component of a `par` into the context is invisible + to `Obs`. -/ + close_par_right : ∀ {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) + (K : T.Plug (PortBoundary.tensor Δ₁ Δ₂)), + Obs.rel (T.close (T.par W₁ W₂) K) (T.close W₂ (T.parContextRight W₁ K)) + /-- Absorbing the right factor of a `wire` into the context is invisible to + `Obs`. -/ + close_wire_left : ∀ {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)) + (W₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)) + (K : T.Plug (PortBoundary.tensor Δ₁ Δ₂)), + Obs.rel (T.close (T.wire W₁ W₂) K) (T.close W₁ (T.wireContextLeft W₂ K)) + /-- Absorbing the left factor of a `wire` into the context is invisible to + `Obs`. -/ + close_wire_right : ∀ {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)) + (W₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)) + (K : T.Plug (PortBoundary.tensor Δ₁ Δ₂)), + Obs.rel (T.close (T.wire W₁ W₂) K) (T.close W₂ (T.wireContextRight W₁ K)) + +/-- Every observation over a theory with strict plug/wire factorization +respects that factorization, since each law holds as an equality and `Obs.rel` +is reflexive. This keeps the free syntax models on the full composition +suite. -/ +instance respectsFactorization_of_hasPlugWireFactor [OpenTheory.HasPlugWireFactor T] + (Obs : Observation T) : Obs.RespectsFactorization where + plug_comm W K := by rw [OpenTheory.plug_comm]; exact Obs.equiv.refl _ + close_par_left W₁ W₂ K := by rw [OpenTheory.close_par_left]; exact Obs.equiv.refl _ + close_par_right W₁ W₂ K := by rw [OpenTheory.close_par_right]; exact Obs.equiv.refl _ + close_wire_left W₁ W₂ K := by rw [OpenTheory.close_wire_left]; exact Obs.equiv.refl _ + close_wire_right W₁ W₂ K := by rw [OpenTheory.close_wire_right]; exact Obs.equiv.refl _ + /-! ## UC composition theorems -/ namespace Emulates -variable [OpenTheory.HasPlugWireFactor T] - /-- Replacing the left component of a parallel composition preserves emulation, with the right component and environment held fixed. -/ -theorem par_left {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} {real₁ ideal₁ : T.Obj Δ₁} - (h₁ : Emulates real₁ ideal₁ Obs) (W₂ : T.Obj Δ₂) : +theorem par_left {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} [Obs.RespectsFactorization] + {real₁ ideal₁ : T.Obj Δ₁} (h₁ : Emulates real₁ ideal₁ Obs) (W₂ : T.Obj Δ₂) : Emulates (T.par real₁ W₂) (T.par ideal₁ W₂) Obs := - ⟨fun K => by - rw [OpenTheory.close_par_left real₁ W₂ K, - OpenTheory.close_par_left ideal₁ W₂ K] - exact h₁.compare _⟩ + ⟨fun K => Obs.equiv.trans + (Observation.RespectsFactorization.close_par_left real₁ W₂ K) + (Obs.equiv.trans (h₁.compare _) + (Obs.equiv.symm (Observation.RespectsFactorization.close_par_left ideal₁ W₂ K)))⟩ /-- Replacing the right component of a parallel composition preserves emulation, with the left component and environment held fixed. -/ -theorem par_right {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} (W₁ : T.Obj Δ₁) - {real₂ ideal₂ : T.Obj Δ₂} (h₂ : Emulates real₂ ideal₂ Obs) : +theorem par_right {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} [Obs.RespectsFactorization] + (W₁ : T.Obj Δ₁) {real₂ ideal₂ : T.Obj Δ₂} (h₂ : Emulates real₂ ideal₂ Obs) : Emulates (T.par W₁ real₂) (T.par W₁ ideal₂) Obs := - ⟨fun K => by - rw [OpenTheory.close_par_right W₁ real₂ K, - OpenTheory.close_par_right W₁ ideal₂ K] - exact h₂.compare _⟩ + ⟨fun K => Obs.equiv.trans + (Observation.RespectsFactorization.close_par_right W₁ real₂ K) + (Obs.equiv.trans (h₂.compare _) + (Obs.equiv.symm (Observation.RespectsFactorization.close_par_right W₁ ideal₂ K)))⟩ /-- **UC composition theorem for `par`**: if each component emulates its ideal, then their parallel composition emulates the parallel composition @@ -398,34 +457,35 @@ of ideals. The proof uses a hybrid argument through `T.par ideal₁ real₂`, with each step reducing to emulation of a single component via `close_par_left` / `close_par_right`. -/ -theorem par_compose {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} {real₁ ideal₁ : T.Obj Δ₁} +theorem par_compose {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} [Obs.RespectsFactorization] + {real₁ ideal₁ : T.Obj Δ₁} {real₂ ideal₂ : T.Obj Δ₂} (h₁ : Emulates real₁ ideal₁ Obs) (h₂ : Emulates real₂ ideal₂ Obs) : Emulates (T.par real₁ real₂) (T.par ideal₁ ideal₂) Obs := Emulates.trans (par_left h₁ real₂) (par_right ideal₁ h₂) /-- Replacing the left factor of a wiring preserves emulation. -/ -theorem wire_left {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} +theorem wire_left {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} [Obs.RespectsFactorization] {real₁ ideal₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)} (h₁ : Emulates real₁ ideal₁ Obs) (W₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)) : Emulates (T.wire real₁ W₂) (T.wire ideal₁ W₂) Obs := - ⟨fun K => by - rw [OpenTheory.close_wire_left real₁ W₂ K, - OpenTheory.close_wire_left ideal₁ W₂ K] - exact h₁.compare _⟩ + ⟨fun K => Obs.equiv.trans + (Observation.RespectsFactorization.close_wire_left real₁ W₂ K) + (Obs.equiv.trans (h₁.compare _) + (Obs.equiv.symm (Observation.RespectsFactorization.close_wire_left ideal₁ W₂ K)))⟩ /-- Replacing the right factor of a wiring preserves emulation. -/ -theorem wire_right {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} +theorem wire_right {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} [Obs.RespectsFactorization] (W₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)) {real₂ ideal₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} (h₂ : Emulates real₂ ideal₂ Obs) : Emulates (T.wire W₁ real₂) (T.wire W₁ ideal₂) Obs := - ⟨fun K => by - rw [OpenTheory.close_wire_right W₁ real₂ K, - OpenTheory.close_wire_right W₁ ideal₂ K] - exact h₂.compare _⟩ + ⟨fun K => Obs.equiv.trans + (Observation.RespectsFactorization.close_wire_right W₁ real₂ K) + (Obs.equiv.trans (h₂.compare _) + (Obs.equiv.symm (Observation.RespectsFactorization.close_wire_right W₁ ideal₂ K)))⟩ /-- **UC composition theorem for `wire`**: if each factor emulates its ideal, then their wired composition emulates the wired ideal. -/ -theorem wire_compose {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} +theorem wire_compose {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} [Obs.RespectsFactorization] {real₁ ideal₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)} {real₂ ideal₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} (h₁ : Emulates real₁ ideal₁ Obs) (h₂ : Emulates real₂ ideal₂ Obs) : @@ -434,13 +494,16 @@ theorem wire_compose {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} /-- Replacing the plug (environment) while keeping the protocol fixed preserves observational equivalence, using `plug_comm` to swap -the protocol/environment roles. -/ -theorem plug_right {Δ : PortBoundary} {Obs : Observation T} (W : T.Obj Δ) - {K₁ K₂ : T.Obj (PortBoundary.swap Δ)} (hK : Emulates K₁ K₂ Obs) : - Obs.rel (T.close W K₁) (T.close W K₂) := by - simp only [OpenTheory.close, OpenTheory.plug_comm W K₁, - OpenTheory.plug_comm W K₂] - exact hK.compare W +the protocol/environment roles. + +Only `RespectsPlugComm` is needed: no factorization of `par` or `wire` is +involved. -/ +theorem plug_right {Δ : PortBoundary} {Obs : Observation T} [Obs.RespectsPlugComm] + (W : T.Obj Δ) {K₁ K₂ : T.Obj (PortBoundary.swap Δ)} (hK : Emulates K₁ K₂ Obs) : + Obs.rel (T.close W K₁) (T.close W K₂) := + Obs.equiv.trans (Observation.RespectsPlugComm.plug_comm W K₁) + (Obs.equiv.trans (hK.compare W) + (Obs.equiv.symm (Observation.RespectsPlugComm.plug_comm W K₂))) /-- **UC composition theorem for `plug`**: if the protocol emulates its ideal and the environment emulates its ideal, then the closed real-world @@ -450,7 +513,8 @@ execution. The proof uses a hybrid through `T.close ideal K_real`: step 1 is `plug_invariance` (same environment, different protocol) and step 2 is `plug_right` (same protocol, different environment). -/ -theorem plug_compose {Δ : PortBoundary} {Obs : Observation T} {real ideal : T.Obj Δ} +theorem plug_compose {Δ : PortBoundary} {Obs : Observation T} [Obs.RespectsPlugComm] + {real ideal : T.Obj Δ} {K_real K_ideal : T.Obj (PortBoundary.swap Δ)} (hProt : Emulates real ideal Obs) (hEnv : Emulates K_real K_ideal Obs) : Obs.rel (T.close real K_real) (T.close ideal K_ideal) := Obs.equiv.trans diff --git a/PolyFun/Interaction/UC/OpenProcessEmulates.lean b/PolyFun/Interaction/UC/OpenProcessEmulates.lean new file mode 100644 index 0000000..da14dfa --- /dev/null +++ b/PolyFun/Interaction/UC/OpenProcessEmulates.lean @@ -0,0 +1,103 @@ +/- +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.Emulates +public import PolyFun.Interaction.UC.OpenProcessModel + +/-! +# Observations on the process model that ignore scheduling + +`Emulates`' composition theorems take their structural input from the +observation, through `Observation.RespectsPlugComm` and +`Observation.RespectsFactorization`. This file supplies those instances for +the process-backed `openTheory`, which cannot supply the strict +`OpenTheory.HasPlugWireFactor` structure: every binary composition prepends a +scheduler node, so regrouping one is a delay bisimulation rather than an +identity. + +## The shape of the bridge + +`OpenProcessActivationEquiv` is *not* promoted to an observation here, and +must not be. It labels a step only by whether some party was activated, +discarding packet identity and `stepSampler` effects, so a security statement +made against it would say almost nothing. Its role is the opposite one: it is +an upper bound on how fine a scheduling-insensitive observation may be. + +`Observation.IsSchedulingInsensitive` records that bound — an observation +satisfies it when activation-equivalent closed systems are already related. +A concrete security observation (packet-aware, sampler-aware, supplied +downstream where probability lives) is expected to satisfy it because the +scheduler nodes introduced by composition are internal, hence never activated, +and so should be invisible to any reasonable notion of what a network does. + +## Main definitions + +* `Observation.IsSchedulingInsensitive Obs`: activation-equivalent closed + processes are `Obs`-related. +* `respectsPlugComm_of_isSchedulingInsensitive`: such an observation respects + plug commutation, so `Emulates.plug_right` and `Emulates.plug_compose` apply + to `openTheory`. + +## What is still missing + +`Observation.RespectsFactorization` needs the `par` and `wire` factorization +laws, and those have no activation-equivalence counterpart yet: of the three +`OpenTheory.HasPlugWireFactor` fields only `plug_eq_wire` is covered, by +`openTheory_plug_eq_wire_activation_equiv`, while `plug_par_left` and +`plug_wire_left` are unproved for this model (as are all three `IsTraced` +laws, which would be the categorical route to them). Until they exist the +process model supports the `plug` half of the composition suite but not the +`par` and `wire` half. +-/ + +public section + +universe u v w w' + +namespace Interaction +namespace UC + +variable {Party : Type u} {m : Type w → Type w'} {schedulerSampler : m (ULift.{w, 0} Bool)} + +/-- +`Obs.IsSchedulingInsensitive` states that the observation `Obs` cannot +distinguish closed processes that differ only in activation-preserving +scheduling structure. + +This is a *bound* on an observation, never a definition of one: +`OpenProcessActivationEquiv` retains no packet or action identity and ignores +`stepSampler`, so it is far too coarse to serve as a security observation on +its own. What the class says is that whatever `Obs` does measure, it does not +measure the internal scheduler nodes that `par`, `wire`, and `plug` introduce +— which is exactly the licence needed to transport the model's coherence laws +from activation equivalence to `Obs`. +-/ +class Observation.IsSchedulingInsensitive + (Obs : Observation (openTheory.{u, v, w, w'} Party m schedulerSampler)) : Prop where + /-- Activation-equivalent closed processes are related by `Obs`. -/ + rel_of_activationEquiv : + ∀ {p q : (openTheory.{u, v, w, w'} Party m schedulerSampler).Closed}, + OpenProcessActivationEquiv p q → Obs.rel p q + +/-- +A scheduling-insensitive observation on the process model respects plug +commutation, because `openTheory_plug_comm_activation_equiv` already provides +the law up to activation equivalence. + +This is what makes `Emulates.plug_right` and `Emulates.plug_compose` +applicable to `openTheory`. +-/ +instance respectsPlugComm_of_isSchedulingInsensitive + (Obs : Observation (openTheory.{u, v, w, w'} Party m schedulerSampler)) + [Observation.IsSchedulingInsensitive Obs] : Obs.RespectsPlugComm where + plug_comm W K := + Observation.IsSchedulingInsensitive.rel_of_activationEquiv + (openTheory_plug_comm_activation_equiv Party m schedulerSampler W K) + +end UC +end Interaction diff --git a/PolyFunTest/Interaction/UC/EmulatesFactorizationExamples.lean b/PolyFunTest/Interaction/UC/EmulatesFactorizationExamples.lean new file mode 100644 index 0000000..aed9d0f --- /dev/null +++ b/PolyFunTest/Interaction/UC/EmulatesFactorizationExamples.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ + +module + +import all PolyFun.Interaction.UC.Emulates +public import PolyFun.Interaction.UC.Emulates +public import PolyFun.Interaction.UC.OpenProcessEmulates +public import PolyFun.Interaction.UC.OpenSyntax.Expr + +/-! +# Observation-level factorization examples + +Regression checks that the UC composition theorems still reach the free +syntax models through `respectsFactorization_of_hasPlugWireFactor`, and that +the process-backed `openTheory` now reaches the `plug` half of the suite +through `Observation.IsSchedulingInsensitive`. +-/ + +@[expose] public section + +universe u v w w' + +namespace Interaction.UC.EmulatesFactorizationExamples + +/-! ### Free syntax models keep the full suite -/ + +section FreeModel + +variable {Atom : PortBoundary → Type u} (Obs : Observation (OpenSyntax.Expr.theory Atom)) + +/-- Strict plug/wire factorization gives every observation the factorization +laws, so instance synthesis needs no help on the free model. -/ +example : Obs.RespectsFactorization := inferInstance + +/-- The weaker plug-commutation layer is likewise available. -/ +example : Obs.RespectsPlugComm := inferInstance + +/-- Parallel composition of emulations still typechecks on the free model. -/ +example {Δ₁ Δ₂ : PortBoundary} + {real₁ ideal₁ : (OpenSyntax.Expr.theory Atom).Obj Δ₁} + {real₂ ideal₂ : (OpenSyntax.Expr.theory Atom).Obj Δ₂} + (h₁ : Emulates real₁ ideal₁ Obs) (h₂ : Emulates real₂ ideal₂ Obs) : + Emulates ((OpenSyntax.Expr.theory Atom).par real₁ real₂) + ((OpenSyntax.Expr.theory Atom).par ideal₁ ideal₂) Obs := + Emulates.par_compose h₁ h₂ + +/-- Wired composition of emulations still typechecks on the free model. -/ +example {Δ₁ Γ Δ₂ : PortBoundary} + {real₁ ideal₁ : (OpenSyntax.Expr.theory Atom).Obj (PortBoundary.tensor Δ₁ Γ)} + {real₂ ideal₂ : + (OpenSyntax.Expr.theory Atom).Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} + (h₁ : Emulates real₁ ideal₁ Obs) (h₂ : Emulates real₂ ideal₂ Obs) : + Emulates ((OpenSyntax.Expr.theory Atom).wire real₁ real₂) + ((OpenSyntax.Expr.theory Atom).wire ideal₁ ideal₂) Obs := + Emulates.wire_compose h₁ h₂ + +/-- Closing against emulating environments still typechecks on the free +model. -/ +example {Δ : PortBoundary} + {real ideal : (OpenSyntax.Expr.theory Atom).Obj Δ} + {K_real K_ideal : (OpenSyntax.Expr.theory Atom).Obj (PortBoundary.swap Δ)} + (hProt : Emulates real ideal Obs) (hEnv : Emulates K_real K_ideal Obs) : + Obs.rel ((OpenSyntax.Expr.theory Atom).close real K_real) + ((OpenSyntax.Expr.theory Atom).close ideal K_ideal) := + Emulates.plug_compose hProt hEnv + +end FreeModel + +/-! ### The process model reaches the `plug` half -/ + +section ProcessModel + +variable {Party : Type u} {m : Type w → Type w'} {schedulerSampler : m (ULift.{w, 0} Bool)} + (Obs : Observation (openTheory.{u, v, w, w'} Party m schedulerSampler)) + [Observation.IsSchedulingInsensitive Obs] + +/-- A scheduling-insensitive observation on the process model respects plug +commutation, without any `OpenTheory.HasPlugWireFactor` instance — which +`openTheory` does not have. -/ +example : Obs.RespectsPlugComm := inferInstance + +/-- Consequently `Emulates.plug_compose` applies to the process model. This is +the statement that was previously out of reach: the composition theorems were +gated on strict compact-closed structure that `openTheory` cannot supply. -/ +example {Δ : PortBoundary} + {real ideal : (openTheory.{u, v, w, w'} Party m schedulerSampler).Obj Δ} + {K_real K_ideal : + (openTheory.{u, v, w, w'} Party m schedulerSampler).Obj (PortBoundary.swap Δ)} + (hProt : Emulates real ideal Obs) (hEnv : Emulates K_real K_ideal Obs) : + Obs.rel ((openTheory.{u, v, w, w'} Party m schedulerSampler).close real K_real) + ((openTheory.{u, v, w, w'} Party m schedulerSampler).close ideal K_ideal) := + Emulates.plug_compose hProt hEnv + +/-- Replacing the environment alone likewise applies. -/ +example {Δ : PortBoundary} + (W : (openTheory.{u, v, w, w'} Party m schedulerSampler).Obj Δ) + {K₁ K₂ : (openTheory.{u, v, w, w'} Party m schedulerSampler).Obj (PortBoundary.swap Δ)} + (hK : Emulates K₁ K₂ Obs) : + Obs.rel ((openTheory.{u, v, w, w'} Party m schedulerSampler).close W K₁) + ((openTheory.{u, v, w, w'} Party m schedulerSampler).close W K₂) := + Emulates.plug_right W hK + +end ProcessModel + +end Interaction.UC.EmulatesFactorizationExamples diff --git a/docs/wiki/interaction.md b/docs/wiki/interaction.md index 890275f..f86f851 100644 --- a/docs/wiki/interaction.md +++ b/docs/wiki/interaction.md @@ -649,7 +649,8 @@ import PolyFun.Interaction.UC.OpenProcessModel | `OpenSyntax/Expr.lean` | `Expr` (quotient of `Raw`), granular `OpenTheory` lawfulness instances, `Expr.toInterp` | | `OpenProcess.lean` | `BoundaryAction`, `OpenNodeProfile`, `OpenNodeContext` (with polynomial-product bridge `productView` and structural `boundaryTrace`), `OpenProcess m Party Δ` (monad-parametric, with intrinsic `stepSampler`), `toProcess`, `OpenProcessActivationEquiv` | | `OpenProcessModel.lean` | `openTheory m Party schedulerSampler` (concrete model threading `TypeTree.Sampler` through `map` / `par` / `wire` / `plug`), `IsLawful`, monoidal / CC laws up to `OpenProcessActivationEquiv` | -| `Emulates.lean` | `Observation`, `Emulates`, `UCSecure`. Contextual emulation and UC security stated abstractly over an `Observation` (an equivalence relation on closed systems), with no probability monad and no concrete security predicate. | +| `Emulates.lean` | `Observation`, `Emulates`, `UCSecure`. Contextual emulation and UC security stated abstractly over an `Observation` (an equivalence relation on closed systems), with no probability monad and no concrete security predicate. Composition takes its structural input from the observation via `Observation.RespectsPlugComm` / `Observation.RespectsFactorization`; strict `HasPlugWireFactor` theories satisfy both automatically. | +| `OpenProcessEmulates.lean` | `Observation.IsSchedulingInsensitive` (an observation that cannot see activation-preserving scheduling structure) and the `RespectsPlugComm` instance it yields for `openTheory`, transporting `openTheory_plug_comm_activation_equiv` onto the abstract composition theorems | | `Notation.lean` | UC notation helpers (`∥`, `⊞`, `⊠`, `⊗ᵇ`, `ᵛ`); see [`notation.md`](notation.md) | | `MachineId.lean` | machine identifiers | | `EnvAction.lean` | environment actions, parametric over an arbitrary monad `m` (no probability dependency) | diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md index 0be98fe..c8de943 100644 --- a/docs/wiki/repo-map.md +++ b/docs/wiki/repo-map.md @@ -183,6 +183,11 @@ Interaction/{Concurrent, Basic} -> Interaction/UC/{Interface, Emulates, MachineId, EnvAction, EnvOpenProcess, CorruptionModel, MomentaryCorruption, Leakage} + +Interaction/UC/{Emulates, OpenProcessModel} -> Interaction/UC/OpenProcessEmulates + (Emulates is model-agnostic and must not reach OpenProcess; the bridge that + equips the concrete openTheory with observation-level composition laws + therefore sits above both) ``` `PolyFun.lean` is a generated umbrella import file, not a hand-maintained From 7281722d54e7f850543356547944affc62691332 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Tue, 11 Aug 2026 21:29:09 -0500 Subject: [PATCH 2/5] feat(interaction): allowed-systems sub-theories and relativized emulation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds `SubTheory T`, a boundary-indexed membership predicate on `T.Obj` carrying closure under `map`, `par`, and `wire`, with `plug` closure and containment of the structural generators split off as mixins. This is the allowed-systems parameter a UC development fixes before stating security: instantiable at a corruption discipline, at a resource bound, or at their meet. `EmulatesWithin` cuts the plug quantifier of `Emulates` down to a sub-theory and restates the composition suite against it. Each theorem gains exactly one hypothesis — the untouched component must itself be allowed — because the residual context handed to the inductive step is built from that component. `OpenSyntax/AtomSubTheory.lean` instantiates the machinery on the free model, where a sub-theory generated by allowed atoms transfers along interpretation into any target sub-theory accepting those atoms. Purely additive: no existing declaration changes, and relativizing to `SubTheory.top` recovers the unrelativized judgments verbatim. Co-Authored-By: Claude Opus 5 --- AGENTS.md | 7 +- PolyFun.lean | 3 + PolyFun/Interaction/UC/EmulatesWithin.lean | 333 ++++++++++++++++ .../UC/OpenSyntax/AtomSubTheory.lean | 208 ++++++++++ PolyFun/Interaction/UC/SubTheory.lean | 355 ++++++++++++++++++ .../Interaction/UC/SubTheoryExamples.lean | 231 ++++++++++++ docs/wiki/interaction.md | 3 + docs/wiki/repo-map.md | 8 + 8 files changed, 1146 insertions(+), 2 deletions(-) create mode 100644 PolyFun/Interaction/UC/EmulatesWithin.lean create mode 100644 PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean create mode 100644 PolyFun/Interaction/UC/SubTheory.lean create mode 100644 PolyFunTest/Interaction/UC/SubTheoryExamples.lean diff --git a/AGENTS.md b/AGENTS.md index 3bac8b2..33e270d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -74,8 +74,11 @@ 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 - (computational equivalence, asymptotic security) live in VCVio. + actions, leakage, and allowed-systems sub-theories (`SubTheory`, a + boundary-indexed membership predicate closed under the operations, + with emulation relativized to it). *Generic only* — security-flavored + UC layers (computational equivalence, asymptotic security) live in + VCVio, as do the resource measures a sub-theory gets instantiated at. - `PolyFun/Control/`: monad and comonad infrastructure transitively required by the above (coalgebra, comonad, free / freecont monad algebra, monad iter / hom, lawful re-exports). diff --git a/PolyFun.lean b/PolyFun.lean index 6a12dd1..047bb68 100644 --- a/PolyFun.lean +++ b/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 @@ -111,10 +112,12 @@ public import PolyFun.Interaction.UC.Notation public import PolyFun.Interaction.UC.OpenProcess public import PolyFun.Interaction.UC.OpenProcessEmulates 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 diff --git a/PolyFun/Interaction/UC/EmulatesWithin.lean b/PolyFun/Interaction/UC/EmulatesWithin.lean new file mode 100644 index 0000000..bb19957 --- /dev/null +++ b/PolyFun/Interaction/UC/EmulatesWithin.lean @@ -0,0 +1,333 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ + +module + +import all PolyFun.Interaction.UC.Emulates +public import PolyFun.Interaction.UC.Emulates +public import PolyFun.Interaction.UC.SubTheory + +/-! +# Emulation relative to an allowed class of contexts + +`Emulates real ideal Obs` quantifies over *every* plug. That is the right +judgment when the observation itself already encodes whatever restriction one +wants on the environment, and the wrong one as soon as the restriction is a +property of systems rather than of the relation — an efficiency bound being +the standard example. + +`EmulatesWithin D real ideal Obs` restricts that quantifier to the plugs +allowed by a `SubTheory D`. + +## Main definitions + +* `SubTheory.mem_parContextLeft` and its three siblings: the residual context + formed by absorbing one component of a composite into the plug stays inside + `D`. These are the only new facts the whole file needs, and they hold + because the four context-formers of `Emulates` are `map`/`wire` composites. +* `EmulatesWithin D real ideal Obs`, and the composition suite relativized to + it. +* `UCSecureWithin`, whose simulator carries the additional obligation of + mapping allowed contexts to allowed contexts. + +## What relativizing costs, and why that is the point + +Each composition theorem gains one hypothesis: the component being held fixed +must itself be allowed. `par_left` needs `D.mem W₂` because the plug it hands +to `h₁` is built from `W₂`. So the side condition that a categorical account +of UC imposes by fiat — that the map exhibiting an emulation lies in the +allowed sub-category — is here *derived* from the shape of the factorization +argument. There is nowhere else it could come from and nowhere else it could +go. + +Instantiating `D` at `SubTheory.top` discards every such hypothesis and +recovers `Emulates` exactly (`emulatesWithin_top_iff`), so nothing in this +file weakens what the unrelativized suite already proves. + +## Relation to the simulator + +`UCSecureWithin` is where the relativization pays for itself most visibly. +Its first conjunct says the simulator sends allowed contexts to allowed +contexts. Under an efficiency instantiation that reads "the simulator is +efficient", which is exactly the obligation simulation-based mechanizations +normally leave to the metatheory. +-/ + +public section + +universe u + +namespace Interaction +namespace UC + +variable {T : OpenTheory.{u}} + +/-! ## Residual contexts stay allowed -/ + +namespace SubTheory + +/-- Absorbing the right component of a `par` into an allowed plug yields an +allowed plug, since `parContextLeft` is a `wire` followed by a `map`. -/ +theorem mem_parContextLeft {D : SubTheory T} {Δ₁ Δ₂ : PortBoundary} {W₂ : T.Obj Δ₂} + {K : T.Plug (PortBoundary.tensor Δ₁ Δ₂)} (hK : D.mem K) (hW₂ : D.mem W₂) : + D.mem (T.parContextLeft W₂ K) := + D.mem_map _ (D.mem_wire hK (D.mem_map _ hW₂)) + +/-- Absorbing the left component of a `par` into an allowed plug yields an +allowed plug. -/ +theorem mem_parContextRight {D : SubTheory T} {Δ₁ Δ₂ : PortBoundary} {W₁ : T.Obj Δ₁} + {K : T.Plug (PortBoundary.tensor Δ₁ Δ₂)} (hK : D.mem K) (hW₁ : D.mem W₁) : + D.mem (T.parContextRight W₁ K) := + D.mem_map _ (D.mem_wire (D.mem_map _ hK) (D.mem_map _ hW₁)) + +/-- Absorbing the right factor of a `wire` into an allowed plug yields an +allowed plug. -/ +theorem mem_wireContextLeft {D : SubTheory T} {Δ₁ Γ Δ₂ : PortBoundary} + {W₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} + {K : T.Plug (PortBoundary.tensor Δ₁ Δ₂)} (hK : D.mem K) (hW₂ : D.mem W₂) : + D.mem (T.wireContextLeft W₂ K) := + D.mem_wire hK (D.mem_map _ hW₂) + +/-- Absorbing the left factor of a `wire` into an allowed plug yields an +allowed plug. -/ +theorem mem_wireContextRight {D : SubTheory T} {Δ₁ Γ Δ₂ : PortBoundary} + {W₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)} + {K : T.Plug (PortBoundary.tensor Δ₁ Δ₂)} (hK : D.mem K) (hW₁ : D.mem W₁) : + D.mem (T.wireContextRight W₁ K) := + D.mem_map _ (D.mem_wire (D.mem_map _ hK) hW₁) + +end SubTheory + +/-! ## The relativized emulation judgment -/ + +/-- +`EmulatesWithin D real ideal Obs` says `real` emulates `ideal` against every +context that the sub-theory `D` allows. + +This is `Emulates` with its plug quantifier cut down to `D`. Since `D` shrinks +the set of distinguishers, the judgment is *antitone* in `D` +(`EmulatesWithin.mono`): a smaller allowed class is a weaker security claim. +-/ +structure EmulatesWithin (D : SubTheory T) {Δ : PortBoundary} (real ideal : T.Obj Δ) + (Obs : Observation T) : Prop where + /-- Every allowed context sees `real` and `ideal` as `Obs`-related. -/ + compare : ∀ K : T.Plug Δ, D.mem K → Obs.rel (T.close real K) (T.close ideal K) + +namespace EmulatesWithin + +/-- Every open system emulates itself relative to any allowed class. -/ +theorem refl (D : SubTheory T) {Δ : PortBoundary} (Obs : Observation T) (W : T.Obj Δ) : + EmulatesWithin D W W Obs := + ⟨fun _ _ => Obs.equiv.refl _⟩ + +/-- Relativized emulation is symmetric. -/ +theorem symm {D : SubTheory T} {Δ : PortBoundary} {Obs : Observation T} {W₁ W₂ : T.Obj Δ} + (h : EmulatesWithin D W₁ W₂ Obs) : EmulatesWithin D W₂ W₁ Obs := + ⟨fun K hK => Obs.equiv.symm (h.compare K hK)⟩ + +/-- Relativized emulation composes transitively. -/ +theorem trans {D : SubTheory T} {Δ : PortBoundary} {Obs : Observation T} {W₁ W₂ W₃ : T.Obj Δ} + (h₁₂ : EmulatesWithin D W₁ W₂ Obs) (h₂₃ : EmulatesWithin D W₂ W₃ Obs) : + EmulatesWithin D W₁ W₃ Obs := + ⟨fun K hK => Obs.equiv.trans (h₁₂.compare K hK) (h₂₃.compare K hK)⟩ + +/-- +Shrinking the allowed class weakens the judgment. + +Read the other way: a security claim proved against a large class of contexts +holds against every smaller one, which is what makes an efficiency +instantiation a *relaxation* of the unrestricted statement rather than a +different claim. +-/ +theorem mono {D₁ D₂ : SubTheory T} (hD : D₁ ≤ D₂) {Δ : PortBoundary} {Obs : Observation T} + {real ideal : T.Obj Δ} (h : EmulatesWithin D₂ real ideal Obs) : + EmulatesWithin D₁ real ideal Obs := + ⟨fun K hK => h.compare K (hD K hK)⟩ + +/-- Adapting both sides along the same boundary morphism preserves relativized +emulation. The adapted context is allowed because `D` is closed under `map`. -/ +theorem map_invariance [OpenTheory.IsLawfulPlug T] {D : SubTheory T} {Δ₁ Δ₂ : PortBoundary} + {Obs : Observation T} (f : PortBoundary.Hom Δ₁ Δ₂) {real ideal : T.Obj Δ₁} + (h : EmulatesWithin D real ideal Obs) : + EmulatesWithin D (T.map f real) (T.map f ideal) Obs := + ⟨fun K hK => by + simp only [OpenTheory.close, + OpenTheory.map_plug f real K, OpenTheory.map_plug f ideal K] + exact h.compare _ (D.mem_map _ hK)⟩ + +end EmulatesWithin + +/-! ## Reconciliation with the unrelativized judgment -/ + +/-- An unrestricted emulation is an emulation relative to any allowed class: +restricting the contexts can only discard obligations. -/ +theorem Emulates.toEmulatesWithin (D : SubTheory T) {Δ : PortBoundary} {Obs : Observation T} + {real ideal : T.Obj Δ} (h : Emulates real ideal Obs) : EmulatesWithin D real ideal Obs := + ⟨fun K _ => h.compare K⟩ + +/-- +Relativizing to the class that allows everything is a no-op. + +This is the machine-checked form of the claim that this file is a +conservative extension: every theorem below specializes at +`SubTheory.top` to the corresponding theorem about `Emulates`. +-/ +theorem emulatesWithin_top_iff {Δ : PortBoundary} {Obs : Observation T} + {real ideal : T.Obj Δ} : + EmulatesWithin (SubTheory.top T) real ideal Obs ↔ Emulates real ideal Obs := + ⟨fun h => ⟨fun K => h.compare K trivial⟩, fun h => ⟨fun K _ => h.compare K⟩⟩ + +/-! ## Relativized UC composition theorems -/ + +namespace EmulatesWithin + +/-- +Replacing the left component of a parallel composition preserves relativized +emulation. + +The new hypothesis `hW₂` is the one the abstract theory imposes as a +convention: the untouched component must itself be an allowed system. It is +needed here because the plug handed to `h₁` is built by absorbing `W₂` into +the ambient context. +-/ +theorem par_left {D : SubTheory T} {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} + [Obs.RespectsFactorization] {real₁ ideal₁ : T.Obj Δ₁} + (h₁ : EmulatesWithin D real₁ ideal₁ Obs) {W₂ : T.Obj Δ₂} (hW₂ : D.mem W₂) : + EmulatesWithin D (T.par real₁ W₂) (T.par ideal₁ W₂) Obs := + ⟨fun K hK => Obs.equiv.trans + (Observation.RespectsFactorization.close_par_left real₁ W₂ K) + (Obs.equiv.trans (h₁.compare _ (SubTheory.mem_parContextLeft hK hW₂)) + (Obs.equiv.symm (Observation.RespectsFactorization.close_par_left ideal₁ W₂ K)))⟩ + +/-- Replacing the right component of a parallel composition preserves +relativized emulation. -/ +theorem par_right {D : SubTheory T} {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} + [Obs.RespectsFactorization] {W₁ : T.Obj Δ₁} (hW₁ : D.mem W₁) + {real₂ ideal₂ : T.Obj Δ₂} (h₂ : EmulatesWithin D real₂ ideal₂ Obs) : + EmulatesWithin D (T.par W₁ real₂) (T.par W₁ ideal₂) Obs := + ⟨fun K hK => Obs.equiv.trans + (Observation.RespectsFactorization.close_par_right W₁ real₂ K) + (Obs.equiv.trans (h₂.compare _ (SubTheory.mem_parContextRight hK hW₁)) + (Obs.equiv.symm (Observation.RespectsFactorization.close_par_right W₁ ideal₂ K)))⟩ + +/-- +**Relativized UC composition theorem for `par`.** + +Both ideal components must be allowed: the hybrid argument passes through +`T.par ideal₁ real₂`, and each leg absorbs the *other* component into the +context. +-/ +theorem par_compose {D : SubTheory T} {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} + [Obs.RespectsFactorization] {real₁ ideal₁ : T.Obj Δ₁} {real₂ ideal₂ : T.Obj Δ₂} + (h₁ : EmulatesWithin D real₁ ideal₁ Obs) (h₂ : EmulatesWithin D real₂ ideal₂ Obs) + (hReal₂ : D.mem real₂) (hIdeal₁ : D.mem ideal₁) : + EmulatesWithin D (T.par real₁ real₂) (T.par ideal₁ ideal₂) Obs := + EmulatesWithin.trans (par_left h₁ hReal₂) (par_right hIdeal₁ h₂) + +/-- Replacing the left factor of a wiring preserves relativized emulation. -/ +theorem wire_left {D : SubTheory T} {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} + [Obs.RespectsFactorization] {real₁ ideal₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)} + (h₁ : EmulatesWithin D real₁ ideal₁ Obs) + {W₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} (hW₂ : D.mem W₂) : + EmulatesWithin D (T.wire real₁ W₂) (T.wire ideal₁ W₂) Obs := + ⟨fun K hK => Obs.equiv.trans + (Observation.RespectsFactorization.close_wire_left real₁ W₂ K) + (Obs.equiv.trans (h₁.compare _ (SubTheory.mem_wireContextLeft hK hW₂)) + (Obs.equiv.symm (Observation.RespectsFactorization.close_wire_left ideal₁ W₂ K)))⟩ + +/-- Replacing the right factor of a wiring preserves relativized emulation. -/ +theorem wire_right {D : SubTheory T} {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} + [Obs.RespectsFactorization] {W₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)} (hW₁ : D.mem W₁) + {real₂ ideal₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} + (h₂ : EmulatesWithin D real₂ ideal₂ Obs) : + EmulatesWithin D (T.wire W₁ real₂) (T.wire W₁ ideal₂) Obs := + ⟨fun K hK => Obs.equiv.trans + (Observation.RespectsFactorization.close_wire_right W₁ real₂ K) + (Obs.equiv.trans (h₂.compare _ (SubTheory.mem_wireContextRight hK hW₁)) + (Obs.equiv.symm (Observation.RespectsFactorization.close_wire_right W₁ ideal₂ K)))⟩ + +/-- **Relativized UC composition theorem for `wire`.** -/ +theorem wire_compose {D : SubTheory T} {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} + [Obs.RespectsFactorization] {real₁ ideal₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)} + {real₂ ideal₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} + (h₁ : EmulatesWithin D real₁ ideal₁ Obs) (h₂ : EmulatesWithin D real₂ ideal₂ Obs) + (hReal₂ : D.mem real₂) (hIdeal₁ : D.mem ideal₁) : + EmulatesWithin D (T.wire real₁ real₂) (T.wire ideal₁ ideal₂) Obs := + EmulatesWithin.trans (wire_left h₁ hReal₂) (wire_right hIdeal₁ h₂) + +/-- +Replacing the plug while keeping the system fixed preserves observational +equivalence, provided the fixed system is itself allowed — it becomes the +context after `plug_comm` exchanges the two roles. +-/ +theorem plug_right {D : SubTheory T} {Δ : PortBoundary} {Obs : Observation T} + [Obs.RespectsPlugComm] {W : T.Obj Δ} (hW : D.mem W) {K₁ K₂ : T.Plug Δ} + (hK : EmulatesWithin D K₁ K₂ Obs) : Obs.rel (T.close W K₁) (T.close W K₂) := + Obs.equiv.trans (Observation.RespectsPlugComm.plug_comm W K₁) + (Obs.equiv.trans (hK.compare W hW) + (Obs.equiv.symm (Observation.RespectsPlugComm.plug_comm W K₂))) + +/-- +**Relativized UC composition theorem for `plug`.** + +The hybrid runs through `T.close ideal K_real`, so the real context must be +allowed for the first leg and the ideal system must be allowed for the second, +where it plays the role of the context. +-/ +theorem plug_compose {D : SubTheory T} {Δ : PortBoundary} {Obs : Observation T} + [Obs.RespectsPlugComm] {real ideal : T.Obj Δ} {K_real K_ideal : T.Plug Δ} + (hProt : EmulatesWithin D real ideal Obs) (hEnv : EmulatesWithin D K_real K_ideal Obs) + (hKreal : D.mem K_real) (hIdeal : D.mem ideal) : + Obs.rel (T.close real K_real) (T.close ideal K_ideal) := + Obs.equiv.trans (hProt.compare K_real hKreal) (plug_right hIdeal hEnv) + +end EmulatesWithin + +/-! ## Relativized UC security -/ + +/-- +`UCSecureWithin D protocol ideal Obs SimSpace simulate` is UC security with an +existential simulator, relative to the allowed class `D`. + +Two things change relative to `UCSecure`. The context quantifier is cut down +to `D`, and the simulator acquires an obligation: it must send allowed +contexts to allowed contexts. Under a resource-bounded instantiation of `D` +the second conjunct is the statement that the simulator is itself efficient — +an obligation that is normally discharged informally, if at all. +-/ +def UCSecureWithin (D : SubTheory T) {Δ : PortBoundary} (protocol ideal : T.Obj Δ) + (Obs : Observation T) (SimSpace : Type*) (simulate : SimSpace → T.Plug Δ → T.Plug Δ) : Prop := + ∃ s : SimSpace, + (∀ K : T.Plug Δ, D.mem K → D.mem (simulate s K)) ∧ + (∀ K : T.Plug Δ, D.mem K → Obs.rel (T.close protocol K) (T.close ideal (simulate s K))) + +/-- Relativized emulation implies relativized UC security with the identity +simulator, which trivially preserves the allowed class. -/ +theorem EmulatesWithin.toUCSecureWithin {D : SubTheory T} {Δ : PortBoundary} + {protocol ideal : T.Obj Δ} {Obs : Observation T} + (h : EmulatesWithin D protocol ideal Obs) : + UCSecureWithin D protocol ideal Obs PUnit (fun _ K => K) := + ⟨⟨⟩, fun _ hK => hK, h.compare⟩ + +/-- Relativized UC security with identity simulation recovers relativized +emulation. -/ +theorem UCSecureWithin.toEmulatesWithin_id {D : SubTheory T} {Δ : PortBoundary} + {protocol ideal : T.Obj Δ} {Obs : Observation T} + (hSec : UCSecureWithin D protocol ideal Obs PUnit (fun _ K => K)) : + EmulatesWithin D protocol ideal Obs := + let ⟨_, _, h⟩ := hSec; ⟨h⟩ + +/-- Relativizing UC security to the class that allows everything recovers +`UCSecure`. -/ +theorem ucSecureWithin_top_iff {Δ : PortBoundary} {protocol ideal : T.Obj Δ} + {Obs : Observation T} {SimSpace : Type*} {simulate : SimSpace → T.Plug Δ → T.Plug Δ} : + UCSecureWithin (SubTheory.top T) protocol ideal Obs SimSpace simulate ↔ + UCSecure protocol ideal Obs SimSpace simulate := + ⟨fun ⟨s, _, h⟩ => ⟨s, fun K => h K trivial⟩, + fun ⟨s, h⟩ => ⟨s, fun _ _ => trivial, fun K _ => h K⟩⟩ + +end UC +end Interaction diff --git a/PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean b/PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean new file mode 100644 index 0000000..04ab207 --- /dev/null +++ b/PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean @@ -0,0 +1,208 @@ +/- +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, so the natural sub-theories +of `Expr.theory Atom` are the ones cut out by a predicate on atoms: fix which +primitive components a protocol may use, and take everything wired together +from them. + +`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`. + +Read `D` as "implementable within a fixed resource discipline" and the +statement becomes *a network of implementable components is implementable* — +the closure property that composable-security frameworks assume of their +machine model, discharged here as an induction over five constructors. The +work is not in the induction; it is in `D`'s closure fields, which is exactly +where it belongs. + +## 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 not decidable and not +extensional. `atomSubTheory A` contains every expression that *can* be +assembled from allowed atoms, and an expression equal in `Expr` to such an +assembly is one. That is the right notion here — an implementability claim +should not depend on which representative one writes down. +-/ + +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 closure fields, so the theorem +holds for any notion of "allowed" whatsoever — a corruption discipline, a +resource bound, or their intersection. + +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 diff --git a/PolyFun/Interaction/UC/SubTheory.lean b/PolyFun/Interaction/UC/SubTheory.lean new file mode 100644 index 0000000..9711c80 --- /dev/null +++ b/PolyFun/Interaction/UC/SubTheory.lean @@ -0,0 +1,355 @@ +/- +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.OpenTheory + +/-! +# Sub-theories: which open systems a model allows + +An `OpenTheory` says how open systems may be combined. It does not say which +open systems one is *allowed* to build. Every UC-style development needs that +second notion: a corruption model is a restriction on the machines a real +protocol may use, and an efficiency requirement is a restriction on the +machines anyone may use at all. + +`SubTheory T` is that notion. It is a boundary-indexed membership predicate +on `T.Obj` together with proofs that membership survives the theory's +operations. Nothing here mentions corruption, probability, or cost: those are +instantiations, and the point of the abstraction is that they are the *same* +instantiation mechanism. + +## Main definitions + +* `SubTheory T` bundles `mem` with closure under `map`, `par`, and `wire`. +* `SubTheory.IsPlugClosed D` adds closure under `plug`. It is a separate class + rather than a field because a theory with strict plug/wire factorization + gets it for free (`isPlugClosed_of_hasPlugWireFactor`), while the concrete + process model — which has no such factorization — must earn it. +* `SubTheory.IsStructural D` says `D` contains the structural generators, the + unit and the identity wires. +* `SubTheory.top`, `SubTheory.inf`, and the order `≤`. `top` allows + everything, so every statement relativized to `top` is the unrelativized + statement. `inf` is how independent restrictions — a corruption model and an + efficiency class — combine into one allowed-systems predicate. +* `SubTheory.generated G` is the smallest sub-theory containing the generators + `G`, and `SubTheory.generated_le` is its induction principle. + +## Why the closure fields are the interesting part + +Read `mem` as "is implementable within some fixed resource discipline". Then +`mem_par` and `mem_wire` say that a network of implementable systems is itself +implementable — the property that composable-security frameworks normally +assume outright about their machine model, because it is stated globally over +networks and there is no finite obligation to discharge. Here the network is +built from four operations, so the assumption *is* four closure fields. That +is the whole reason to make the allowed class a first-class object rather than +a side condition. + +`generated` and `generated_le` are the other half of the same idea. A protocol +class defined by its generators is a `generated` sub-theory, so proving every +member of it implementable reduces to proving the generators implementable and +supplying the closure fields once. + +## Design notes + +`mem` is a `Prop`, not data. A resource-bounded instantiation carries its +witness *inside* the proposition (`∃ a bound in the class, …`), exactly as +`StepClass.Hom` does one level down in `PolyFun/Realizability/`; making +membership proof-relevant would make `EmulatesWithin` proof-relevant too, +which is wrong. + +`SubTheory` is deliberately the `OpenTheory`-level sibling of +`PFunctor.StepClass`: a bundled predicate plus its closure proofs, passed +explicitly rather than synthesized, with the optional structure split into +mixins and an order along which results transport. The two are meant to meet +at an instantiation of `mem` in terms of realizability, not to share code. +-/ + +public section + +universe u + +namespace Interaction +namespace UC + +variable {T : OpenTheory.{u}} + +/-- +`SubTheory T` picks out, at every boundary, which open systems of `T` are +allowed, subject to those systems being closed under the theory's composition +operations. + +This is the formal counterpart of the nested sub-categories a UC development +fixes before stating any security property: one parameter naming the class of +systems a real protocol may be assembled from. + +Closure under `plug` is *not* a field; see `SubTheory.IsPlugClosed`. +-/ +structure SubTheory (T : OpenTheory.{u}) where + /-- Which open systems at boundary `Δ` the sub-theory allows. -/ + mem : ∀ {Δ : PortBoundary}, T.Obj Δ → Prop + /-- Allowed systems remain allowed under boundary adaptation. Adaptation + changes only how a system presents its boundary, so no restriction worth + the name can be broken by it. -/ + mem_map : ∀ {Δ₁ Δ₂ : PortBoundary} {W : T.Obj Δ₁} (φ : PortBoundary.Hom Δ₁ Δ₂), + mem W → mem (T.map φ W) + /-- Allowed systems are closed under parallel composition. -/ + mem_par : ∀ {Δ₁ Δ₂ : PortBoundary} {W₁ : T.Obj Δ₁} {W₂ : T.Obj Δ₂}, + mem W₁ → mem W₂ → mem (T.par W₁ W₂) + /-- Allowed systems are closed under wiring one shared boundary. -/ + mem_wire : ∀ {Δ₁ Γ Δ₂ : PortBoundary} {W₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)} + {W₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)}, + mem W₁ → mem W₂ → mem (T.wire W₁ W₂) + +namespace SubTheory + +/-- Allowed systems remain allowed under transport along a boundary +equivalence. -/ +theorem mem_mapEquiv {D : SubTheory T} {Δ₁ Δ₂ : PortBoundary} + (e : PortBoundary.Equiv Δ₁ Δ₂) {W : T.Obj Δ₁} (hW : D.mem W) : + D.mem (T.mapEquiv e W) := + D.mem_map e.toHom hW + +/-! ### Closure under total closure -/ + +/-- +`D.IsPlugClosed` states that plugging an allowed system against an allowed +context yields an allowed closed system. + +This is a mixin rather than a `SubTheory` field for the same reason +`Observation.RespectsPlugComm` is split out of +`Observation.RespectsFactorization`: a theory whose `plug` factors through +`wire` gets it for free (`isPlugClosed_of_hasPlugWireFactor`), whereas the +process-backed `openTheory` — which instantiates only `OpenTheory.IsLawful` +— has to prove it directly. Splitting lets each model declare exactly the +strength it can honestly satisfy. +-/ +class IsPlugClosed {T : OpenTheory.{u}} (D : SubTheory T) : Prop where + /-- Closing an allowed system against an allowed context stays allowed. -/ + mem_plug : ∀ {Δ : PortBoundary} {W : T.Obj Δ} {K : T.Obj (PortBoundary.swap Δ)}, + D.mem W → D.mem K → D.mem (T.plug W K) + +/-- In a theory with strict plug/wire factorization, `plug` is a composite of +`map` and `wire`, so every sub-theory is automatically plug-closed. This is +what keeps the free syntax models on the full relativized suite. -/ +instance isPlugClosed_of_hasPlugWireFactor [OpenTheory.HasPlugWireFactor T] + (D : SubTheory T) : D.IsPlugClosed where + mem_plug hW hK := by + rw [OpenTheory.plug_eq_wire] + exact D.mem_map _ (D.mem_wire (D.mem_map _ hW) (D.mem_map _ hK)) + +/-- `close` is `plug` under the contextual-equivalence reading, so it inherits +closure verbatim. -/ +theorem mem_close {D : SubTheory T} [D.IsPlugClosed] {Δ : PortBoundary} + {W : T.Obj Δ} {K : T.Plug Δ} (hW : D.mem W) (hK : D.mem K) : + D.mem (T.close W K) := + IsPlugClosed.mem_plug hW hK + +/-! ### Containing the structural generators -/ + +/-- +`D.IsStructural` states that `D` contains the two pieces of structure a +compact-closed theory supplies on its own: the unit and the identity wire at +every boundary. + +These are the wires of a string diagram rather than machines in it, so any +class of systems meant to be closed under rewiring must contain them. It is a +class, and separate from `SubTheory`, because a theory need not have the +structure at all: `openTheory` has neither `OpenTheory.HasUnit` nor +`OpenTheory.HasIdWire` registered. +-/ +class IsStructural {T : OpenTheory.{u}} [OpenTheory.HasUnit T] [OpenTheory.HasIdWire T] + (D : SubTheory T) : Prop where + /-- The monoidal unit is allowed. -/ + mem_unit : D.mem (OpenTheory.HasUnit.unit (T := T)) + /-- Every identity wire is allowed. -/ + mem_idWire : ∀ Γ : PortBoundary, D.mem (OpenTheory.HasIdWire.idWire (T := T) Γ) + +/-! ### Order, top, and meet -/ + +/-- +`D₁ ≤ D₂` says every system `D₁` allows is also allowed by `D₂`. + +Relativized security statements are *antitone* in this order: allowing fewer +contexts is a weaker demand on the protocol. See `EmulatesWithin.mono`. +-/ +@[expose] +def le (D₁ D₂ : SubTheory T) : Prop := + ∀ {Δ : PortBoundary} (W : T.Obj Δ), D₁.mem W → D₂.mem W + +instance : LE (SubTheory T) := ⟨SubTheory.le⟩ + +/-- Build an inclusion of sub-theories from pointwise membership transfer. -/ +theorem le_of_mem {D₁ D₂ : SubTheory T} + (h : ∀ {Δ : PortBoundary} (W : T.Obj Δ), D₁.mem W → D₂.mem W) : D₁ ≤ D₂ := h + +theorem le_refl (D : SubTheory T) : D ≤ D := fun _ hW => hW + +theorem le_trans {D₁ D₂ D₃ : SubTheory T} (h₁₂ : D₁ ≤ D₂) (h₂₃ : D₂ ≤ D₃) : D₁ ≤ D₃ := + fun W hW => h₂₃ W (h₁₂ W hW) + +/-- Transfer membership upward along the order. -/ +theorem mem_of_le {D₁ D₂ : SubTheory T} (h : D₁ ≤ D₂) {Δ : PortBoundary} {W : T.Obj Δ} + (hW : D₁.mem W) : D₂.mem W := + h W hW + +/-- +The sub-theory allowing everything. + +Relativizing to `top` is a no-op: `EmulatesWithin.emulatesWithin_top_iff` +shows the relativized emulation judgment collapses to `Emulates`. This is what +makes the whole layer a conservative extension. +-/ +@[expose] +def top (T : OpenTheory.{u}) : SubTheory T where + mem := fun _ => True + mem_map _ _ := trivial + mem_par _ _ := trivial + mem_wire _ _ := trivial + +instance isPlugClosed_top (T : OpenTheory.{u}) : (top T).IsPlugClosed where + mem_plug _ _ := trivial + +instance isStructural_top (T : OpenTheory.{u}) [OpenTheory.HasUnit T] [OpenTheory.HasIdWire T] : + (top T).IsStructural where + mem_unit := trivial + mem_idWire _ := trivial + +theorem le_top (D : SubTheory T) : D ≤ top T := fun _ _ => trivial + +@[simp] +theorem top_mem {Δ : PortBoundary} (W : T.Obj Δ) : (top T).mem W := trivial + +/-- +The intersection of two sub-theories. + +This is how independent restrictions combine. A corruption model and a +resource bound are two unrelated reasons to disallow a system; their meet is +the class of systems allowed for both reasons, and it is a sub-theory because +each closure field holds componentwise. +-/ +@[expose] +def inf (D₁ D₂ : SubTheory T) : SubTheory T where + mem W := D₁.mem W ∧ D₂.mem W + mem_map φ h := ⟨D₁.mem_map φ h.1, D₂.mem_map φ h.2⟩ + mem_par h₁ h₂ := ⟨D₁.mem_par h₁.1 h₂.1, D₂.mem_par h₁.2 h₂.2⟩ + mem_wire h₁ h₂ := ⟨D₁.mem_wire h₁.1 h₂.1, D₂.mem_wire h₁.2 h₂.2⟩ + +instance isPlugClosed_inf (D₁ D₂ : SubTheory T) [D₁.IsPlugClosed] [D₂.IsPlugClosed] : + (inf D₁ D₂).IsPlugClosed where + mem_plug h₁ h₂ := ⟨IsPlugClosed.mem_plug h₁.1 h₂.1, IsPlugClosed.mem_plug h₁.2 h₂.2⟩ + +instance isStructural_inf [OpenTheory.HasUnit T] [OpenTheory.HasIdWire T] + (D₁ D₂ : SubTheory T) [D₁.IsStructural] [D₂.IsStructural] : (inf D₁ D₂).IsStructural where + mem_unit := ⟨IsStructural.mem_unit, IsStructural.mem_unit⟩ + mem_idWire Γ := ⟨IsStructural.mem_idWire Γ, IsStructural.mem_idWire Γ⟩ + +@[simp] +theorem inf_mem {D₁ D₂ : SubTheory T} {Δ : PortBoundary} {W : T.Obj Δ} : + (inf D₁ D₂).mem W ↔ D₁.mem W ∧ D₂.mem W := + Iff.rfl + +theorem inf_le_left (D₁ D₂ : SubTheory T) : inf D₁ D₂ ≤ D₁ := fun _ h => h.1 + +theorem inf_le_right (D₁ D₂ : SubTheory T) : inf D₁ D₂ ≤ D₂ := fun _ h => h.2 + +theorem le_inf {D D₁ D₂ : SubTheory T} (h₁ : D ≤ D₁) (h₂ : D ≤ D₂) : D ≤ inf D₁ D₂ := + fun W hW => ⟨h₁ W hW, h₂ W hW⟩ + +/-! ### The sub-theory generated by a set of generators -/ + +/-- +`Generated T G W` says `W` can be assembled from generators satisfying `G` +using only the operations of `T`. + +This is the inductive counterpart of "the smallest sub-theory containing `G`", +and it is the shape a protocol class actually takes in practice: one names the +allowed building blocks and takes everything wired together from them. + +The `plug` constructor is included, so `SubTheory.generated G` is plug-closed +unconditionally — no factorization law is needed to build a closed system, only +to take one apart. +-/ +inductive Generated (T : OpenTheory.{u}) (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) : + {Δ : PortBoundary} → T.Obj Δ → Prop where + /-- A generator is generated. -/ + | base {Δ : PortBoundary} {W : T.Obj Δ} : G Δ W → Generated T G W + /-- Boundary adaptation of a generated system is generated. -/ + | map {Δ₁ Δ₂ : PortBoundary} {W : T.Obj Δ₁} (φ : PortBoundary.Hom Δ₁ Δ₂) : + Generated T G W → Generated T G (T.map φ W) + /-- A parallel composite of generated systems is generated. -/ + | par {Δ₁ Δ₂ : PortBoundary} {W₁ : T.Obj Δ₁} {W₂ : T.Obj Δ₂} : + Generated T G W₁ → Generated T G W₂ → Generated T G (T.par W₁ W₂) + /-- A wiring of generated systems is generated. -/ + | wire {Δ₁ Γ Δ₂ : PortBoundary} {W₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)} + {W₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} : + Generated T G W₁ → Generated T G W₂ → Generated T G (T.wire W₁ W₂) + /-- Plugging generated systems together is generated. -/ + | plug {Δ : PortBoundary} {W : T.Obj Δ} {K : T.Obj (PortBoundary.swap Δ)} : + Generated T G W → Generated T G K → Generated T G (T.plug W K) + +/-- +The smallest sub-theory whose members include every generator satisfying `G`. + +Its closure fields are literally the constructors of `Generated`. + +The generator predicate takes its boundary *explicitly*, unlike +`SubTheory.mem`. A predicate whose leading argument is implicit gets its +implicits inserted eagerly when it is passed as an argument, which leaves the +boundary as an unsolvable metavariable at every use site; `mem` escapes this +only because it is a projection applied to a known `SubTheory`. +-/ +@[expose] +def generated (T : OpenTheory.{u}) (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) : SubTheory T where + mem W := Generated T G W + mem_map φ h := .map φ h + mem_par h₁ h₂ := .par h₁ h₂ + mem_wire h₁ h₂ := .wire h₁ h₂ + +instance isPlugClosed_generated (T : OpenTheory.{u}) + (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) : (generated T G).IsPlugClosed where + mem_plug h₁ h₂ := .plug h₁ h₂ + +/-- Every generator belongs to the sub-theory it generates. -/ +theorem mem_generated_of_gen (T : OpenTheory.{u}) (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) + {Δ : PortBoundary} (W : T.Obj Δ) (hW : G Δ W) : (generated T G).mem W := + .base hW + +/-- +**The induction principle for generated sub-theories.** + +If every generator is allowed by `D`, then everything assembled from +generators is allowed by `D`. Contrapositively, this is the only way a +generated class can fail a property closed under the operations: one of its +generators must already fail it. + +Instantiating `D` at a resource-bounded class turns the usual "a network of +efficient machines is efficient" assumption into a finite obligation — the +generators, plus the four closure fields carried by `D` itself. +-/ +theorem generated_le {G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop} (D : SubTheory T) + [D.IsPlugClosed] (hG : ∀ (Δ : PortBoundary) (W : T.Obj Δ), G Δ W → D.mem W) : + generated T G ≤ D := by + intro Δ W hW + induction hW with + | base hg => exact hG _ _ hg + | map _ _ ih => exact D.mem_map _ ih + | par _ _ ih₁ ih₂ => exact D.mem_par ih₁ ih₂ + | wire _ _ ih₁ ih₂ => exact D.mem_wire ih₁ ih₂ + | plug _ _ ih₁ ih₂ => exact IsPlugClosed.mem_plug ih₁ ih₂ + +/-- The generated sub-theory is monotone in its generators. -/ +theorem generated_mono {G₁ G₂ : ∀ (Δ : PortBoundary), T.Obj Δ → Prop} + (h : ∀ (Δ : PortBoundary) (W : T.Obj Δ), G₁ Δ W → G₂ Δ W) : + generated T G₁ ≤ generated T G₂ := + generated_le _ fun Δ W hW => Generated.base (h Δ W hW) + +end SubTheory + +end UC +end Interaction diff --git a/PolyFunTest/Interaction/UC/SubTheoryExamples.lean b/PolyFunTest/Interaction/UC/SubTheoryExamples.lean new file mode 100644 index 0000000..f9e45fb --- /dev/null +++ b/PolyFunTest/Interaction/UC/SubTheoryExamples.lean @@ -0,0 +1,231 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ + +module + +import all PolyFun.Interaction.UC.EmulatesWithin +public import PolyFun.Interaction.UC.EmulatesWithin +public import PolyFun.Interaction.UC.OpenProcessEmulates +public import PolyFun.Interaction.UC.OpenSyntax.AtomSubTheory + +/-! +# Sub-theory examples + +Checks that the allowed-systems layer behaves as intended: + +* the lattice operations synthesize their mixins, +* relativizing to `SubTheory.top` recovers the unrelativized judgments, +* the relativized composition suite elaborates on both the free syntax model + and the process-backed `openTheory`, +* a sub-theory generated by allowed atoms transfers along interpretation, and +* the unrelativized suite is untouched. +-/ + +@[expose] public section + +universe u v w w' + +namespace Interaction.UC.SubTheoryExamples + +/-! ### Lattice structure and mixin synthesis -/ + +section Lattice + +variable {T : OpenTheory.{u}} (D D₁ D₂ : SubTheory T) + +/-- The class allowing everything is plug-closed without any assumption on the +theory. -/ +example : (SubTheory.top T).IsPlugClosed := inferInstance + +/-- A meet of plug-closed classes is plug-closed. -/ +example [D₁.IsPlugClosed] [D₂.IsPlugClosed] : (SubTheory.inf D₁ D₂).IsPlugClosed := inferInstance + +/-- A generated class is plug-closed unconditionally: building a closed system +needs no factorization law. -/ +example (G : ∀ Δ : PortBoundary, T.Obj Δ → Prop) : + (SubTheory.generated T G).IsPlugClosed := inferInstance + +/-- Strict plug/wire factorization gives *every* sub-theory plug-closure, so +instance synthesis needs no help on a compact-closed theory. -/ +example {S : OpenTheory.{u}} [OpenTheory.HasPlugWireFactor S] (E : SubTheory S) : + E.IsPlugClosed := inferInstance + +/-- Meets are lower bounds. -/ +example : SubTheory.inf D₁ D₂ ≤ D₁ := SubTheory.inf_le_left D₁ D₂ + +/-- Everything is below the top class. -/ +example : D ≤ SubTheory.top T := SubTheory.le_top D + +end Lattice + +/-! ### Relativizing to `top` is a no-op -/ + +section Conservativity + +variable {T : OpenTheory.{u}} {Δ : PortBoundary} {Obs : Observation T} {real ideal : T.Obj Δ} + +/-- Emulation against every allowed context, where everything is allowed, is +emulation. -/ +example : EmulatesWithin (SubTheory.top T) real ideal Obs ↔ Emulates real ideal Obs := + emulatesWithin_top_iff + +/-- UC security relativized to the top class is UC security. -/ +example {SimSpace : Type*} {simulate : SimSpace → T.Plug Δ → T.Plug Δ} : + UCSecureWithin (SubTheory.top T) real ideal Obs SimSpace simulate ↔ + UCSecure real ideal Obs SimSpace simulate := + ucSecureWithin_top_iff + +/-- Any unrelativized emulation weakens to any allowed class. -/ +example (D : SubTheory T) (h : Emulates real ideal Obs) : EmulatesWithin D real ideal Obs := + h.toEmulatesWithin D + +end Conservativity + +/-! ### The relativized composition suite on the free syntax model -/ + +section FreeModel + +variable {Atom : PortBoundary → Type u} {Obs : Observation (OpenSyntax.Expr.theory Atom)} + {D : SubTheory (OpenSyntax.Expr.theory Atom)} + +/-- Parallel composition, relativized. Both untouched components must be +allowed — the hypotheses a categorical account of UC imposes by convention. -/ +example {Δ₁ Δ₂ : PortBoundary} + {real₁ ideal₁ : (OpenSyntax.Expr.theory Atom).Obj Δ₁} + {real₂ ideal₂ : (OpenSyntax.Expr.theory Atom).Obj Δ₂} + (h₁ : EmulatesWithin D real₁ ideal₁ Obs) (h₂ : EmulatesWithin D real₂ ideal₂ Obs) + (hReal₂ : D.mem real₂) (hIdeal₁ : D.mem ideal₁) : + EmulatesWithin D ((OpenSyntax.Expr.theory Atom).par real₁ real₂) + ((OpenSyntax.Expr.theory Atom).par ideal₁ ideal₂) Obs := + EmulatesWithin.par_compose h₁ h₂ hReal₂ hIdeal₁ + +/-- Wired composition, relativized. -/ +example {Δ₁ Γ Δ₂ : PortBoundary} + {real₁ ideal₁ : (OpenSyntax.Expr.theory Atom).Obj (PortBoundary.tensor Δ₁ Γ)} + {real₂ ideal₂ : + (OpenSyntax.Expr.theory Atom).Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} + (h₁ : EmulatesWithin D real₁ ideal₁ Obs) (h₂ : EmulatesWithin D real₂ ideal₂ Obs) + (hReal₂ : D.mem real₂) (hIdeal₁ : D.mem ideal₁) : + EmulatesWithin D ((OpenSyntax.Expr.theory Atom).wire real₁ real₂) + ((OpenSyntax.Expr.theory Atom).wire ideal₁ ideal₂) Obs := + EmulatesWithin.wire_compose h₁ h₂ hReal₂ hIdeal₁ + +/-- **No-regression canary.** The unrelativized suite is unchanged and still +reaches the free model by synthesis alone. -/ +example {Δ₁ Δ₂ : PortBoundary} + {real₁ ideal₁ : (OpenSyntax.Expr.theory Atom).Obj Δ₁} + {real₂ ideal₂ : (OpenSyntax.Expr.theory Atom).Obj Δ₂} + (h₁ : Emulates real₁ ideal₁ Obs) (h₂ : Emulates real₂ ideal₂ Obs) : + Emulates ((OpenSyntax.Expr.theory Atom).par real₁ real₂) + ((OpenSyntax.Expr.theory Atom).par ideal₁ ideal₂) Obs := + Emulates.par_compose h₁ h₂ + +end FreeModel + +/-! ### The relativized `plug` theorem on the process model + +`openTheory` has no strict factorization, so it reaches these through +`Observation.IsSchedulingInsensitive` rather than +`OpenTheory.HasPlugWireFactor`. -/ + +section ProcessModel + +variable (Party : Type u) (m : Type w → Type w') [Monad m] + (schedulerSampler : m (ULift.{w, 0} Bool)) + (Obs : Observation (openTheory.{u, v, w, w'} Party m schedulerSampler)) + [Observation.IsSchedulingInsensitive Obs] + (D : SubTheory (openTheory.{u, v, w, w'} Party m schedulerSampler)) + +example {Δ : PortBoundary} + {real ideal : (openTheory.{u, v, w, w'} Party m schedulerSampler).Obj Δ} + {K_real K_ideal : (openTheory.{u, v, w, w'} Party m schedulerSampler).Plug Δ} + (hProt : EmulatesWithin D real ideal Obs) (hEnv : EmulatesWithin D K_real K_ideal Obs) + (hKreal : D.mem K_real) (hIdeal : D.mem ideal) : + Obs.rel ((openTheory.{u, v, w, w'} Party m schedulerSampler).close real K_real) + ((openTheory.{u, v, w, w'} Party m schedulerSampler).close ideal K_ideal) := + EmulatesWithin.plug_compose hProt hEnv hKreal hIdeal + +end ProcessModel + +/-! ### A generated sub-theory over a toy signature -/ + +section Atoms + +/-- A two-generator signature: one component we are willing to use and one we +are not. -/ +inductive ToyAtom : PortBoundary → Type where + /-- An allowed primitive component at boundary `Δ`. -/ + | good (Δ : PortBoundary) : ToyAtom Δ + /-- A forbidden primitive component at boundary `Δ`. -/ + | bad (Δ : PortBoundary) : ToyAtom Δ + +/-- The allowed-atom predicate: `good` yes, `bad` no. -/ +def toyAllowed : ∀ {Δ : PortBoundary}, ToyAtom Δ → Prop + | _, .good _ => True + | _, .bad _ => False + +/-- Abbreviation for the syntactic theory over the toy signature. -/ +abbrev ToyTheory : OpenTheory.{1} := OpenSyntax.Expr.theory ToyAtom + +/-- The generated class is structural: it contains the unit and every identity +wire, found by synthesis. -/ +example : (OpenSyntax.atomSubTheory ToyAtom toyAllowed).IsStructural := inferInstance + +/-- An allowed atom is an allowed system. -/ +example (Δ : PortBoundary) : + (OpenSyntax.atomSubTheory ToyAtom toyAllowed).mem + (OpenSyntax.Expr.atom (ToyAtom.good Δ)) := + OpenSyntax.atomSubTheory.mem_atom ToyAtom toyAllowed trivial + +/-- A network of allowed atoms is allowed. This is the closure the whole +layer exists to supply. -/ +example (Δ₁ Δ₂ : PortBoundary) : + (OpenSyntax.atomSubTheory ToyAtom toyAllowed).mem + (ToyTheory.par (OpenSyntax.Expr.atom (ToyAtom.good Δ₁)) + (OpenSyntax.Expr.atom (ToyAtom.good Δ₂))) := + (OpenSyntax.atomSubTheory ToyAtom toyAllowed).mem_par + (OpenSyntax.atomSubTheory.mem_atom ToyAtom toyAllowed trivial) + (OpenSyntax.atomSubTheory.mem_atom ToyAtom toyAllowed trivial) + +/-- Plugging an allowed system against an allowed context stays allowed. -/ +example (Δ : PortBoundary) : + (OpenSyntax.atomSubTheory ToyAtom toyAllowed).mem + (ToyTheory.plug (OpenSyntax.Expr.atom (ToyAtom.good Δ)) + (OpenSyntax.Expr.atom (ToyAtom.good (PortBoundary.swap Δ)))) := + SubTheory.IsPlugClosed.mem_plug + (OpenSyntax.atomSubTheory.mem_atom ToyAtom toyAllowed trivial) + (OpenSyntax.atomSubTheory.mem_atom ToyAtom toyAllowed trivial) + +/-- The forbidden atom really is forbidden. -/ +example (Δ : PortBoundary) : ¬ toyAllowed (ToyAtom.bad Δ) := id + +/-- Allowing strictly more atoms gives a larger class. -/ +example : OpenSyntax.atomSubTheory ToyAtom toyAllowed ≤ + OpenSyntax.atomSubTheory ToyAtom (fun _ => True) := + OpenSyntax.atomSubTheory.mono ToyAtom fun _ _ => trivial + +/-- **The transfer theorem.** Interpreting a network of allowed atoms into any +target class that accepts the allowed atoms lands inside that class. Taken at +the identity interpretation, it says the generated class is closed under +everything the theory can build. -/ +example {Δ : PortBoundary} {e : OpenSyntax.Expr ToyAtom Δ} + (he : (OpenSyntax.atomSubTheory ToyAtom toyAllowed).mem e) : + (OpenSyntax.atomSubTheory ToyAtom toyAllowed).mem + (e.interpret ToyTheory OpenSyntax.Expr.atom) := + OpenSyntax.mem_interpret_of_atoms ToyAtom toyAllowed + (OpenSyntax.atomSubTheory ToyAtom toyAllowed) OpenSyntax.Expr.atom + (fun _ ha => OpenSyntax.atomSubTheory.mem_atom ToyAtom toyAllowed ha) he + +/-- The same statement as an inclusion of sub-theories. -/ +example : OpenSyntax.atomSubTheory ToyAtom toyAllowed ≤ + OpenSyntax.interpretSubTheory ToyAtom + (OpenSyntax.atomSubTheory ToyAtom toyAllowed) OpenSyntax.Expr.atom := + OpenSyntax.atomSubTheory_le_interpretSubTheory ToyAtom toyAllowed _ _ + fun _ ha => OpenSyntax.atomSubTheory.mem_atom ToyAtom toyAllowed ha + +end Atoms + +end Interaction.UC.SubTheoryExamples diff --git a/docs/wiki/interaction.md b/docs/wiki/interaction.md index f86f851..6573a8c 100644 --- a/docs/wiki/interaction.md +++ b/docs/wiki/interaction.md @@ -649,8 +649,11 @@ import PolyFun.Interaction.UC.OpenProcessModel | `OpenSyntax/Expr.lean` | `Expr` (quotient of `Raw`), granular `OpenTheory` lawfulness instances, `Expr.toInterp` | | `OpenProcess.lean` | `BoundaryAction`, `OpenNodeProfile`, `OpenNodeContext` (with polynomial-product bridge `productView` and structural `boundaryTrace`), `OpenProcess m Party Δ` (monad-parametric, with intrinsic `stepSampler`), `toProcess`, `OpenProcessActivationEquiv` | | `OpenProcessModel.lean` | `openTheory m Party schedulerSampler` (concrete model threading `TypeTree.Sampler` through `map` / `par` / `wire` / `plug`), `IsLawful`, monoidal / CC laws up to `OpenProcessActivationEquiv` | +| `SubTheory.lean` | `SubTheory` (a boundary-indexed membership predicate on `T.Obj` closed under `map` / `par` / `wire`), the `IsPlugClosed` and `IsStructural` mixins, the order `≤` with `top` and `inf`, and `SubTheory.generated` with its induction principle `generated_le`. The allowed-systems parameter a UC development fixes before stating security; instantiable at a corruption discipline, a resource bound, or their meet. No cost or probability content. | | `Emulates.lean` | `Observation`, `Emulates`, `UCSecure`. Contextual emulation and UC security stated abstractly over an `Observation` (an equivalence relation on closed systems), with no probability monad and no concrete security predicate. Composition takes its structural input from the observation via `Observation.RespectsPlugComm` / `Observation.RespectsFactorization`; strict `HasPlugWireFactor` theories satisfy both automatically. | +| `EmulatesWithin.lean` | `EmulatesWithin` (emulation quantified only over `SubTheory`-allowed plugs) and the composition suite relativized to it, plus `UCSecureWithin`, whose simulator must map allowed contexts to allowed contexts. Each theorem gains one hypothesis — the untouched component must itself be allowed — because the residual context is built from it. `emulatesWithin_top_iff` shows the layer is a conservative extension. | | `OpenProcessEmulates.lean` | `Observation.IsSchedulingInsensitive` (an observation that cannot see activation-preserving scheduling structure) and the `RespectsPlugComm` instance it yields for `openTheory`, transporting `openTheory_plug_comm_activation_equiv` onto the abstract composition theorems | +| `OpenSyntax/AtomSubTheory.lean` | `AllowedGen` / `atomSubTheory` (the sub-theory of `Expr.theory` generated by an allowed set of atoms, plus the identity wires), the pullback `interpretSubTheory`, and `mem_interpret_of_atoms`: if every allowed atom interprets into a target sub-theory, so does every network built from them. | | `Notation.lean` | UC notation helpers (`∥`, `⊞`, `⊠`, `⊗ᵇ`, `ᵛ`); see [`notation.md`](notation.md) | | `MachineId.lean` | machine identifiers | | `EnvAction.lean` | environment actions, parametric over an arbitrary monad `m` (no probability dependency) | diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md index c8de943..68db1a0 100644 --- a/docs/wiki/repo-map.md +++ b/docs/wiki/repo-map.md @@ -184,6 +184,14 @@ Interaction/{Concurrent, Basic} -> Interaction/UC/{Interface, EnvOpenProcess, CorruptionModel, MomentaryCorruption, Leakage} +Interaction/UC/OpenTheory -> Interaction/UC/SubTheory +Interaction/UC/{Emulates, SubTheory} -> Interaction/UC/EmulatesWithin +Interaction/UC/{OpenSyntax/Expr, SubTheory} + -> Interaction/UC/OpenSyntax/AtomSubTheory + (SubTheory is the allowed-systems predicate and depends on the algebra + alone; the residual-context lemmas that relativized emulation needs live + with EmulatesWithin because the context-formers are defined in Emulates) + Interaction/UC/{Emulates, OpenProcessModel} -> Interaction/UC/OpenProcessEmulates (Emulates is model-agnostic and must not reach OpenProcess; the bridge that equips the concrete openTheory with observation-level composition laws From 3cf72f884c35d7fd9adb9e9425986c2f78490878 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Tue, 11 Aug 2026 21:31:44 -0500 Subject: [PATCH 3/5] docs(wiki): record the implicit-binder and @[expose] traps from this work Both cost real iterations while building the sub-theory layer and are not specific to it: a predicate whose leading argument is implicit cannot be passed as an argument, and a `def` downstream proofs compute with needs `@[expose]` even inside a `public section`. Co-Authored-By: Claude Opus 5 --- docs/wiki/gotchas.md | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/docs/wiki/gotchas.md b/docs/wiki/gotchas.md index 52a76ef..8393ee4 100644 --- a/docs/wiki/gotchas.md +++ b/docs/wiki/gotchas.md @@ -89,6 +89,37 @@ non-standard instances. `do_pure_bind`, `do_bind_pure`, `do_bind_assoc`, `do_bind_pure_comp`, `do_map_bind`, `do_bind_map_left`. All are `@[simp]`. +### 8e. A predicate whose leading argument is implicit cannot be passed as an argument + +A parameter of type `∀ {Δ : PortBoundary}, F Δ → Prop` looks like the right +way to write a boundary-indexed predicate, and it works fine as a *structure +field* (`SubTheory.mem`, because `D.mem W` is a projection applied to a known +`D`). It breaks as soon as such a predicate is **passed** somewhere: a term +whose type starts with an implicit binder has that binder inserted eagerly, so +the argument arrives eta-expanded as `fun {Δ} ↦ P (Δ := ?m)` and `?m` is never +solved. Symptoms are "don't know how to synthesize implicit argument", motives +printed with doubled binders (`fun {Δ} {Δ} ↦ ...`), and +`Internal error in mkElimApp` from `induction`. + +**Fix**: make the index explicit in anything that gets passed — +`∀ (Δ : PortBoundary), F Δ → Prop`. See `SubTheory.generated`'s generator +argument in +[`PolyFun/Interaction/UC/SubTheory.lean`](../../PolyFun/Interaction/UC/SubTheory.lean). +The same applies to the carrier of an indexed family: `Atom` in +`AllowedGen` / `atomSubTheory` is explicit because solving +`?Atom ?Δ ≡ Atom Δ` is not a first-order problem. + +### 8f. `@[expose]` defs, or downstream modules cannot unfold them + +Under the module system a `def` in a `public section` still has an opaque +body outside its own file unless it is `@[expose]`. A definition that +downstream proofs are meant to *compute with* — a lattice element like +`SubTheory.top`, an order like `SubTheory.le`, a generated construction — +must carry the attribute, or the first cross-module `exact`/`rfl` against it +fails with an unhelpful type mismatch. Lean warns when the attribute is +redundant (instances are exposed by default), so add it and delete what it +flags rather than guessing. + ## Proof Patterns ### 8b. Keep one canonical concrete-step relation type From bd89f06b714206e1a262d7955ff2324e8fb9bb83 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Wed, 12 Aug 2026 21:19:27 -0600 Subject: [PATCH 4/5] fix(uc): clarify subtheory contracts --- AGENTS.md | 12 +- PolyFun/Interaction/UC/EmulatesWithin.lean | 54 ++--- .../UC/OpenSyntax/AtomSubTheory.lean | 29 ++- PolyFun/Interaction/UC/SubTheory.lean | 184 ++++++++++++------ .../Interaction/UC/SubTheoryExamples.lean | 143 +++++++++++++- docs/wiki/interaction.md | 6 +- docs/wiki/repo-map.md | 8 +- 7 files changed, 319 insertions(+), 117 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 33e270d..89140a4 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -74,11 +74,13 @@ and depend on this library. interleaving, observation. - `UC/`: open-process / open-theory layer, structural composition (interfaces, par, wire, plug), corruption models, environment - actions, leakage, and allowed-systems sub-theories (`SubTheory`, a - boundary-indexed membership predicate closed under the operations, - with emulation relativized to it). *Generic only* — security-flavored - UC layers (computational equivalence, asymptotic security) live in - VCVio, as do the resource measures a sub-theory gets instantiated at. + 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 algebra, monad iter / hom, lawful re-exports). diff --git a/PolyFun/Interaction/UC/EmulatesWithin.lean b/PolyFun/Interaction/UC/EmulatesWithin.lean index bb19957..d89e3de 100644 --- a/PolyFun/Interaction/UC/EmulatesWithin.lean +++ b/PolyFun/Interaction/UC/EmulatesWithin.lean @@ -13,14 +13,12 @@ public import PolyFun.Interaction.UC.SubTheory /-! # Emulation relative to an allowed class of contexts -`Emulates real ideal Obs` quantifies over *every* plug. That is the right -judgment when the observation itself already encodes whatever restriction one -wants on the environment, and the wrong one as soon as the restriction is a -property of systems rather than of the relation — an efficiency bound being -the standard example. +`Emulates real ideal Obs` quantifies over *every* plug. `EmulatesWithin D real ideal Obs` restricts that quantifier to the plugs -allowed by a `SubTheory D`. +allowed by a `SubTheory D`. It does not assert that `real` or `ideal` belongs +to `D`; those are separate protocol-membership obligations when a development +needs them. ## Main definitions @@ -30,8 +28,9 @@ allowed by a `SubTheory D`. because the four context-formers of `Emulates` are `map`/`wire` composites. * `EmulatesWithin D real ideal Obs`, and the composition suite relativized to it. -* `UCSecureWithin`, whose simulator carries the additional obligation of - mapping allowed contexts to allowed contexts. +* `SubTheory.PreservesAllowedness`, the exact closure obligation on a context + transformer. +* `UCSecureWithin`, whose simulator must preserve allowedness. ## What relativizing costs, and why that is the point @@ -47,13 +46,13 @@ Instantiating `D` at `SubTheory.top` discards every such hypothesis and recovers `Emulates` exactly (`emulatesWithin_top_iff`), so nothing in this file weakens what the unrelativized suite already proves. -## Relation to the simulator +## What simulator preservation says -`UCSecureWithin` is where the relativization pays for itself most visibly. -Its first conjunct says the simulator sends allowed contexts to allowed -contexts. Under an efficiency instantiation that reads "the simulator is -efficient", which is exactly the obligation simulation-based mechanizations -normally leave to the metatheory. +The first conjunct of `UCSecureWithin` says only that the selected simulator +sends `D`-allowed contexts to `D`-allowed contexts. It does not supply an +algorithm, a resource bound, a realizability witness, or an efficiency proof. +Such a reading requires a separate bridge from `D.mem` to the relevant +operational or cost model. -/ public section @@ -69,6 +68,12 @@ variable {T : OpenTheory.{u}} namespace SubTheory +/-- A context transformer preserves membership in the allowed class `D`. -/ +@[expose] +def PreservesAllowedness (D : SubTheory T) {Δ : PortBoundary} + (transform : T.Plug Δ → T.Plug Δ) : Prop := + ∀ K : T.Plug Δ, D.mem K → D.mem (transform K) + /-- Absorbing the right component of a `par` into an allowed plug yields an allowed plug, since `parContextLeft` is a `wire` followed by a `map`. -/ theorem mem_parContextLeft {D : SubTheory T} {Δ₁ Δ₂ : PortBoundary} {W₂ : T.Obj Δ₂} @@ -137,10 +142,8 @@ theorem trans {D : SubTheory T} {Δ : PortBoundary} {Obs : Observation T} {W₁ /-- Shrinking the allowed class weakens the judgment. -Read the other way: a security claim proved against a large class of contexts -holds against every smaller one, which is what makes an efficiency -instantiation a *relaxation* of the unrestricted statement rather than a -different claim. +Read the other way: a claim proved against a large class of contexts holds +against every smaller one. -/ theorem mono {D₁ D₂ : SubTheory T} (hD : D₁ ≤ D₂) {Δ : PortBoundary} {Obs : Observation T} {real ideal : T.Obj Δ} (h : EmulatesWithin D₂ real ideal Obs) : @@ -216,9 +219,9 @@ theorem par_right {D : SubTheory T} {Δ₁ Δ₂ : PortBoundary} {Obs : Observat /-- **Relativized UC composition theorem for `par`.** -Both ideal components must be allowed: the hybrid argument passes through -`T.par ideal₁ real₂`, and each leg absorbs the *other* component into the -context. +The real right component and ideal left component must be allowed: the hybrid +argument passes through `T.par ideal₁ real₂`, and each leg absorbs the other +component into the context. -/ theorem par_compose {D : SubTheory T} {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} [Obs.RespectsFactorization] {real₁ ideal₁ : T.Obj Δ₁} {real₂ ideal₂ : T.Obj Δ₂} @@ -293,15 +296,14 @@ end EmulatesWithin existential simulator, relative to the allowed class `D`. Two things change relative to `UCSecure`. The context quantifier is cut down -to `D`, and the simulator acquires an obligation: it must send allowed -contexts to allowed contexts. Under a resource-bounded instantiation of `D` -the second conjunct is the statement that the simulator is itself efficient — -an obligation that is normally discharged informally, if at all. +to `D`, and the selected simulator must satisfy +`SubTheory.PreservesAllowedness D`. Neither protocol membership nor simulator +realizability or efficiency follows from this definition. -/ def UCSecureWithin (D : SubTheory T) {Δ : PortBoundary} (protocol ideal : T.Obj Δ) (Obs : Observation T) (SimSpace : Type*) (simulate : SimSpace → T.Plug Δ → T.Plug Δ) : Prop := ∃ s : SimSpace, - (∀ K : T.Plug Δ, D.mem K → D.mem (simulate s K)) ∧ + D.PreservesAllowedness (simulate s) ∧ (∀ K : T.Plug Δ, D.mem K → Obs.rel (T.close protocol K) (T.close ideal (simulate s K))) /-- Relativized emulation implies relativized UC security with the identity diff --git a/PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean b/PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean index 04ab207..964c008 100644 --- a/PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean +++ b/PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean @@ -12,10 +12,9 @@ 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, so the natural sub-theories -of `Expr.theory Atom` are the ones cut out by a predicate on atoms: fix which -primitive components a protocol may use, and take everything wired together -from them. +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 @@ -27,12 +26,9 @@ components and so are always allowed. allowed atom interprets into a target sub-theory `D`, then every syntactic system built from allowed atoms interprets into `D`. -Read `D` as "implementable within a fixed resource discipline" and the -statement becomes *a network of implementable components is implementable* — -the closure property that composable-security frameworks assume of their -machine model, discharged here as an induction over five constructors. The -work is not in the induction; it is in `D`'s closure fields, which is exactly -where it belongs. +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 @@ -43,11 +39,9 @@ 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 not decidable and not -extensional. `atomSubTheory A` contains every expression that *can* be -assembled from allowed atoms, and an expression equal in `Expr` to such an -assembly is one. That is the right notion here — an implementability claim -should not depend on which representative one writes down. +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 @@ -169,9 +163,8 @@ instance isStructural_interpretSubTheory (Atom : PortBoundary → Type u) {T : O 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 closure fields, so the theorem -holds for any notion of "allowed" whatsoever — a corruption discipline, a -resource bound, or their intersection. +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 diff --git a/PolyFun/Interaction/UC/SubTheory.lean b/PolyFun/Interaction/UC/SubTheory.lean index 9711c80..e61fb2b 100644 --- a/PolyFun/Interaction/UC/SubTheory.lean +++ b/PolyFun/Interaction/UC/SubTheory.lean @@ -12,16 +12,14 @@ public import PolyFun.Interaction.UC.OpenTheory # Sub-theories: which open systems a model allows An `OpenTheory` says how open systems may be combined. It does not say which -open systems one is *allowed* to build. Every UC-style development needs that -second notion: a corruption model is a restriction on the machines a real -protocol may use, and an efficiency requirement is a restriction on the -machines anyone may use at all. +open systems belong to a chosen class. `SubTheory T` supplies that second, +purely structural notion. `SubTheory T` is that notion. It is a boundary-indexed membership predicate on `T.Obj` together with proofs that membership survives the theory's -operations. Nothing here mentions corruption, probability, or cost: those are -instantiations, and the point of the abstraction is that they are the *same* -instantiation mechanism. +operations. Nothing here defines corruption, protocol membership, probability, +cost, or realizability. A later bridge may instantiate `mem` with one of those +notions after proving the required closure laws. ## Main definitions @@ -32,42 +30,39 @@ instantiation mechanism. process model — which has no such factorization — must earn it. * `SubTheory.IsStructural D` says `D` contains the structural generators, the unit and the identity wires. -* `SubTheory.top`, `SubTheory.inf`, and the order `≤`. `top` allows +* The standard `PartialOrder`, `OrderTop`, and `SemilatticeInf` API. `top` allows everything, so every statement relativized to `top` is the unrelativized - statement. `inf` is how independent restrictions — a corruption model and an - efficiency class — combine into one allowed-systems predicate. + statement. `inf` combines independent composition-closed restrictions. * `SubTheory.generated G` is the smallest sub-theory containing the generators `G`, and `SubTheory.generated_le` is its induction principle. +* `SubTheory.plugGenerated G` is the smallest plug-closed sub-theory containing + `G`, with induction principle `SubTheory.plugGenerated_le`. ## Why the closure fields are the interesting part -Read `mem` as "is implementable within some fixed resource discipline". Then -`mem_par` and `mem_wire` say that a network of implementable systems is itself -implementable — the property that composable-security frameworks normally -assume outright about their machine model, because it is stated globally over -networks and there is no finite obligation to discharge. Here the network is -built from four operations, so the assumption *is* four closure fields. That -is the whole reason to make the allowed class a first-class object rather than -a side condition. +For any intended reading of `mem`, the closure fields state exactly what the +formal object proves: membership survives `map`, `par`, and `wire`. Plug closure +is an additional mixin. The abstraction does not itself justify a resource, +efficiency, corruption, or realizability interpretation. `generated` and `generated_le` are the other half of the same idea. A protocol class defined by its generators is a `generated` sub-theory, so proving every -member of it implementable reduces to proving the generators implementable and -supplying the closure fields once. +member satisfies another sub-theory reduces to checking the generators. ## Design notes -`mem` is a `Prop`, not data. A resource-bounded instantiation carries its -witness *inside* the proposition (`∃ a bound in the class, …`), exactly as -`StepClass.Hom` does one level down in `PolyFun/Realizability/`; making -membership proof-relevant would make `EmulatesWithin` proof-relevant too, -which is wrong. - -`SubTheory` is deliberately the `OpenTheory`-level sibling of -`PFunctor.StepClass`: a bundled predicate plus its closure proofs, passed -explicitly rather than synthesized, with the optional structure split into -mixins and an order along which results transport. The two are meant to meet -at an instantiation of `mem` in terms of realizability, not to share code. +`mem` is a `Prop`, not data, so relativized judgments remain proof-irrelevant. +Resource witnesses, if introduced later, belong inside the proposition or in +a separate realizability layer. + +The proposed `PFunctor.StepClass` and realizability layer are planned in +PolyFun PR #113; they are not dependencies of this module. A future bridge may +relate those classes to `SubTheory.mem` after their closure laws are available. + +`SubTheory` is also separate from `Interaction.UC.CorruptionModel`, which +describes corruption events, states, and environment actions. Relating a +corruption model to a class of allowed closing contexts or protocol systems is +future work and requires an explicit bridge. -/ public section @@ -84,9 +79,9 @@ variable {T : OpenTheory.{u}} allowed, subject to those systems being closed under the theory's composition operations. -This is the formal counterpart of the nested sub-categories a UC development -fixes before stating any security property: one parameter naming the class of -systems a real protocol may be assembled from. +The same structure can describe allowed closing contexts or another +composition-closed class. A judgment using `D` determines which role `D` plays; +membership of real and ideal protocols is not part of this structure. Closure under `plug` is *not* a field; see `SubTheory.IsPlugClosed`. -/ @@ -193,6 +188,16 @@ theorem le_refl (D : SubTheory T) : D ≤ D := fun _ hW => hW theorem le_trans {D₁ D₂ D₃ : SubTheory T} (h₁₂ : D₁ ≤ D₂) (h₂₃ : D₂ ≤ D₃) : D₁ ≤ D₃ := fun W hW => h₂₃ W (h₁₂ W hW) +/-- Two sub-theories are equal when they allow exactly the same systems. -/ +@[ext] +theorem ext {D₁ D₂ : SubTheory T} + (h : ∀ {Δ : PortBoundary} (W : T.Obj Δ), D₁.mem W ↔ D₂.mem W) : D₁ = D₂ := by + cases D₁ + cases D₂ + congr + funext Δ W + exact propext (h W) + /-- Transfer membership upward along the order. -/ theorem mem_of_le {D₁ D₂ : SubTheory T} (h : D₁ ≤ D₂) {Δ : PortBoundary} {W : T.Obj Δ} (hW : D₁.mem W) : D₂.mem W := @@ -222,16 +227,17 @@ instance isStructural_top (T : OpenTheory.{u}) [OpenTheory.HasUnit T] [OpenTheor theorem le_top (D : SubTheory T) : D ≤ top T := fun _ _ => trivial +instance : Top (SubTheory T) := ⟨top T⟩ + +instance : OrderTop (SubTheory T) where + le_top := le_top + @[simp] theorem top_mem {Δ : PortBoundary} (W : T.Obj Δ) : (top T).mem W := trivial /-- -The intersection of two sub-theories. - -This is how independent restrictions combine. A corruption model and a -resource bound are two unrelated reasons to disallow a system; their meet is -the class of systems allowed for both reasons, and it is a sub-theory because -each closure field holds componentwise. +The intersection of two sub-theories. It combines independent +composition-closed restrictions componentwise. -/ @[expose] def inf (D₁ D₂ : SubTheory T) : SubTheory T where @@ -261,19 +267,27 @@ theorem inf_le_right (D₁ D₂ : SubTheory T) : inf D₁ D₂ ≤ D₂ := fun _ theorem le_inf {D D₁ D₂ : SubTheory T} (h₁ : D ≤ D₁) (h₂ : D ≤ D₂) : D ≤ inf D₁ D₂ := fun W hW => ⟨h₁ W hW, h₂ W hW⟩ +instance : SemilatticeInf (SubTheory T) where + le_refl := le_refl + le_trans _ _ _ := le_trans + le_antisymm _ _ h₁₂ h₂₁ := ext fun W => ⟨h₁₂ W, h₂₁ W⟩ + inf := inf + inf_le_left := inf_le_left + inf_le_right := inf_le_right + le_inf := fun D D₁ D₂ => le_inf (D := D) (D₁ := D₁) (D₂ := D₂) + /-! ### The sub-theory generated by a set of generators -/ /-- `Generated T G W` says `W` can be assembled from generators satisfying `G` -using only the operations of `T`. +using the three operations required by `SubTheory`: `map`, `par`, and `wire`. This is the inductive counterpart of "the smallest sub-theory containing `G`", and it is the shape a protocol class actually takes in practice: one names the allowed building blocks and takes everything wired together from them. -The `plug` constructor is included, so `SubTheory.generated G` is plug-closed -unconditionally — no factorization law is needed to build a closed system, only -to take one apart. +This construction does not add `plug` closure. See `PlugGenerated` and +`plugGenerated` for the least plug-closed variant. -/ inductive Generated (T : OpenTheory.{u}) (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) : {Δ : PortBoundary} → T.Obj Δ → Prop where @@ -289,9 +303,6 @@ inductive Generated (T : OpenTheory.{u}) (G : ∀ (Δ : PortBoundary), T.Obj Δ | wire {Δ₁ Γ Δ₂ : PortBoundary} {W₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)} {W₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} : Generated T G W₁ → Generated T G W₂ → Generated T G (T.wire W₁ W₂) - /-- Plugging generated systems together is generated. -/ - | plug {Δ : PortBoundary} {W : T.Obj Δ} {K : T.Obj (PortBoundary.swap Δ)} : - Generated T G W → Generated T G K → Generated T G (T.plug W K) /-- The smallest sub-theory whose members include every generator satisfying `G`. @@ -311,10 +322,6 @@ def generated (T : OpenTheory.{u}) (G : ∀ (Δ : PortBoundary), T.Obj Δ → Pr mem_par h₁ h₂ := .par h₁ h₂ mem_wire h₁ h₂ := .wire h₁ h₂ -instance isPlugClosed_generated (T : OpenTheory.{u}) - (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) : (generated T G).IsPlugClosed where - mem_plug h₁ h₂ := .plug h₁ h₂ - /-- Every generator belongs to the sub-theory it generates. -/ theorem mem_generated_of_gen (T : OpenTheory.{u}) (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) {Δ : PortBoundary} (W : T.Obj Δ) (hW : G Δ W) : (generated T G).mem W := @@ -328,12 +335,12 @@ generators is allowed by `D`. Contrapositively, this is the only way a generated class can fail a property closed under the operations: one of its generators must already fail it. -Instantiating `D` at a resource-bounded class turns the usual "a network of -efficient machines is efficient" assumption into a finite obligation — the -generators, plus the four closure fields carried by `D` itself. +The statement uses exactly the closure fields carried by `D`; it does not +require plug closure because `generated` has the same map/par/wire signature as +`SubTheory`. -/ theorem generated_le {G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop} (D : SubTheory T) - [D.IsPlugClosed] (hG : ∀ (Δ : PortBoundary) (W : T.Obj Δ), G Δ W → D.mem W) : + (hG : ∀ (Δ : PortBoundary) (W : T.Obj Δ), G Δ W → D.mem W) : generated T G ≤ D := by intro Δ W hW induction hW with @@ -341,7 +348,6 @@ theorem generated_le {G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop} (D : SubTh | map _ _ ih => exact D.mem_map _ ih | par _ _ ih₁ ih₂ => exact D.mem_par ih₁ ih₂ | wire _ _ ih₁ ih₂ => exact D.mem_wire ih₁ ih₂ - | plug _ _ ih₁ ih₂ => exact IsPlugClosed.mem_plug ih₁ ih₂ /-- The generated sub-theory is monotone in its generators. -/ theorem generated_mono {G₁ G₂ : ∀ (Δ : PortBoundary), T.Obj Δ → Prop} @@ -349,6 +355,72 @@ theorem generated_mono {G₁ G₂ : ∀ (Δ : PortBoundary), T.Obj Δ → Prop} generated T G₁ ≤ generated T G₂ := generated_le _ fun Δ W hW => Generated.base (h Δ W hW) +/-! ### The plug-closed sub-theory generated by a set of generators -/ + +/-- +`PlugGenerated T G W` says `W` can be assembled from `G` using `map`, `par`, +`wire`, and `plug`. It is the inductive membership predicate for the least +plug-closed sub-theory containing `G`. +-/ +inductive PlugGenerated (T : OpenTheory.{u}) + (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) : + {Δ : PortBoundary} → T.Obj Δ → Prop where + /-- A generator belongs to the plug-closed generated class. -/ + | base {Δ : PortBoundary} {W : T.Obj Δ} : G Δ W → PlugGenerated T G W + /-- Boundary adaptation preserves plug-closed generated membership. -/ + | map {Δ₁ Δ₂ : PortBoundary} {W : T.Obj Δ₁} (φ : PortBoundary.Hom Δ₁ Δ₂) : + PlugGenerated T G W → PlugGenerated T G (T.map φ W) + /-- Parallel composition preserves plug-closed generated membership. -/ + | par {Δ₁ Δ₂ : PortBoundary} {W₁ : T.Obj Δ₁} {W₂ : T.Obj Δ₂} : + PlugGenerated T G W₁ → PlugGenerated T G W₂ → PlugGenerated T G (T.par W₁ W₂) + /-- Wiring preserves plug-closed generated membership. -/ + | wire {Δ₁ Γ Δ₂ : PortBoundary} {W₁ : T.Obj (PortBoundary.tensor Δ₁ Γ)} + {W₂ : T.Obj (PortBoundary.tensor (PortBoundary.swap Γ) Δ₂)} : + PlugGenerated T G W₁ → PlugGenerated T G W₂ → PlugGenerated T G (T.wire W₁ W₂) + /-- Plugging preserves plug-closed generated membership. -/ + | plug {Δ : PortBoundary} {W : T.Obj Δ} {K : T.Obj (PortBoundary.swap Δ)} : + PlugGenerated T G W → PlugGenerated T G K → PlugGenerated T G (T.plug W K) + +/-- The least plug-closed sub-theory containing every generator satisfying `G`. -/ +@[expose] +def plugGenerated (T : OpenTheory.{u}) + (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) : SubTheory T where + mem W := PlugGenerated T G W + mem_map φ h := .map φ h + mem_par h₁ h₂ := .par h₁ h₂ + mem_wire h₁ h₂ := .wire h₁ h₂ + +instance isPlugClosed_plugGenerated (T : OpenTheory.{u}) + (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) : (plugGenerated T G).IsPlugClosed where + mem_plug h₁ h₂ := .plug h₁ h₂ + +/-- Every generator belongs to the plug-closed sub-theory it generates. -/ +theorem mem_plugGenerated_of_gen (T : OpenTheory.{u}) + (G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop) {Δ : PortBoundary} + (W : T.Obj Δ) (hW : G Δ W) : (plugGenerated T G).mem W := + .base hW + +/-- +The universal property of `plugGenerated`: every plug-closed sub-theory that +contains `G` contains the entire plug-closed generated class. +-/ +theorem plugGenerated_le {G : ∀ (Δ : PortBoundary), T.Obj Δ → Prop} (D : SubTheory T) + [D.IsPlugClosed] (hG : ∀ (Δ : PortBoundary) (W : T.Obj Δ), G Δ W → D.mem W) : + plugGenerated T G ≤ D := by + intro Δ W hW + induction hW with + | base hg => exact hG _ _ hg + | map _ _ ih => exact D.mem_map _ ih + | par _ _ ih₁ ih₂ => exact D.mem_par ih₁ ih₂ + | wire _ _ ih₁ ih₂ => exact D.mem_wire ih₁ ih₂ + | plug _ _ ih₁ ih₂ => exact IsPlugClosed.mem_plug ih₁ ih₂ + +/-- Plug-closed generation is monotone in its generators. -/ +theorem plugGenerated_mono {G₁ G₂ : ∀ (Δ : PortBoundary), T.Obj Δ → Prop} + (h : ∀ (Δ : PortBoundary) (W : T.Obj Δ), G₁ Δ W → G₂ Δ W) : + plugGenerated T G₁ ≤ plugGenerated T G₂ := + plugGenerated_le _ fun Δ W hW => PlugGenerated.base (h Δ W hW) + end SubTheory end UC diff --git a/PolyFunTest/Interaction/UC/SubTheoryExamples.lean b/PolyFunTest/Interaction/UC/SubTheoryExamples.lean index f9e45fb..1349f07 100644 --- a/PolyFunTest/Interaction/UC/SubTheoryExamples.lean +++ b/PolyFunTest/Interaction/UC/SubTheoryExamples.lean @@ -16,7 +16,7 @@ public import PolyFun.Interaction.UC.OpenSyntax.AtomSubTheory Checks that the allowed-systems layer behaves as intended: -* the lattice operations synthesize their mixins, +* the standard order operations and mixins synthesize, * relativizing to `SubTheory.top` recovers the unrelativized judgments, * the relativized composition suite elaborates on both the free syntax model and the process-backed `openTheory`, @@ -36,6 +36,14 @@ section Lattice variable {T : OpenTheory.{u}} (D D₁ D₂ : SubTheory T) +example : PartialOrder (SubTheory T) := inferInstance + +example : Top (SubTheory T) := inferInstance + +example : OrderTop (SubTheory T) := inferInstance + +example : SemilatticeInf (SubTheory T) := inferInstance + /-- The class allowing everything is plug-closed without any assumption on the theory. -/ example : (SubTheory.top T).IsPlugClosed := inferInstance @@ -43,10 +51,9 @@ example : (SubTheory.top T).IsPlugClosed := inferInstance /-- A meet of plug-closed classes is plug-closed. -/ example [D₁.IsPlugClosed] [D₂.IsPlugClosed] : (SubTheory.inf D₁ D₂).IsPlugClosed := inferInstance -/-- A generated class is plug-closed unconditionally: building a closed system -needs no factorization law. -/ +/-- Plug-closed generation is plug-closed without a factorization law. -/ example (G : ∀ Δ : PortBoundary, T.Obj Δ → Prop) : - (SubTheory.generated T G).IsPlugClosed := inferInstance + (SubTheory.plugGenerated T G).IsPlugClosed := inferInstance /-- Strict plug/wire factorization gives *every* sub-theory plug-closure, so instance synthesis needs no help on a compact-closed theory. -/ @@ -59,6 +66,15 @@ example : SubTheory.inf D₁ D₂ ≤ D₁ := SubTheory.inf_le_left D₁ D₂ /-- Everything is below the top class. -/ example : D ≤ SubTheory.top T := SubTheory.le_top D +/-- Standard notation reduces to the named constructions. -/ +example : (⊤ : SubTheory T) = SubTheory.top T := rfl + +example : D₁ ⊓ D₂ = SubTheory.inf D₁ D₂ := rfl + +/-- Mutual inclusion determines a sub-theory extensionally. -/ +example (h₁₂ : D₁ ≤ D₂) (h₂₁ : D₂ ≤ D₁) : D₁ = D₂ := + SubTheory.ext fun W => ⟨h₁₂ W, h₂₁ W⟩ + end Lattice /-! ### Relativizing to `top` is a no-op -/ @@ -170,6 +186,83 @@ def toyAllowed : ∀ {Δ : PortBoundary}, ToyAtom Δ → Prop /-- Abbreviation for the syntactic theory over the toy signature. -/ abbrev ToyTheory : OpenTheory.{1} := OpenSyntax.Expr.theory ToyAtom +/-- A quotient-respecting semantics that counts forbidden atoms. All boundary +operations preserve or add counts, so the open-theory equations preserve the +result. -/ +structure AtomCountObj (Δ : PortBoundary) where + count : Nat + +abbrev atomCountTheory : OpenTheory where + Obj := AtomCountObj + map := fun _ n => ⟨n.count⟩ + par := fun n₁ n₂ => ⟨n₁.count + n₂.count⟩ + wire := fun n₁ n₂ => ⟨n₁.count + n₂.count⟩ + plug := fun n₁ n₂ => ⟨n₁.count + n₂.count⟩ + +instance : OpenTheory.HasPlugWireFactor atomCountTheory where + map_id := by intro _ W; cases W; rfl + map_comp := by intro _ _ _ _ _ W; cases W; rfl + map_par := by intro _ _ _ _ _ _ W₁ W₂; cases W₁; cases W₂; rfl + map_wire := by intro _ _ _ _ _ _ _ W₁ W₂; cases W₁; cases W₂; rfl + map_plug := by intro _ _ _ W K; cases W; cases K; rfl + unit := ⟨0⟩ + par_assoc := by + intro _ _ _ W₁ W₂ W₃ + cases W₁; cases W₂; cases W₃ + simp [atomCountTheory, Nat.add_assoc] + par_comm := by + intro _ _ W₁ W₂ + cases W₁; cases W₂ + simp [atomCountTheory, Nat.add_comm] + par_leftUnit := by intro _ W; cases W; simp [atomCountTheory] + par_rightUnit := by intro _ W; cases W; simp [atomCountTheory] + wire_assoc := by + intro _ _ _ _ W₁ W₂ W₃ + cases W₁; cases W₂; cases W₃ + simp [atomCountTheory, Nat.add_assoc] + wire_par_superpose := by + intro _ _ _ _ W₁ W₂ W₃ + cases W₁; cases W₂; cases W₃ + simp [atomCountTheory, Nat.add_assoc] + wire_comm := by + intro _ _ _ W₁ W₂ + cases W₁; cases W₂ + simp [atomCountTheory, Nat.add_comm] + idWire := fun _ => ⟨0⟩ + wire_idWire := by intro _ _ W; cases W; simp [atomCountTheory] + wire_idWire_right := by intro _ _ W; cases W; simp [atomCountTheory] + unit_eq := rfl + plug_eq_wire := by intro _ W K; cases W; cases K; rfl + plug_par_left := by + intro _ _ W₁ W₂ K + cases W₁; cases W₂; cases K + simp [atomCountTheory, Nat.add_comm, Nat.add_left_comm] + plug_wire_left := by + intro _ _ _ W₁ W₂ K + cases W₁; cases W₂; cases K + simp [atomCountTheory, Nat.add_comm, Nat.add_left_comm] + +/-- Interpret allowed atoms as zero and forbidden atoms as one. -/ +def atomCount : ∀ {Δ : PortBoundary}, ToyAtom Δ → atomCountTheory.Obj Δ + | _, .good _ => ⟨0⟩ + | _, .bad _ => ⟨1⟩ + +/-- The zero-count sub-theory of the counting semantics. -/ +def zeroCountSubTheory : SubTheory atomCountTheory where + mem n := n.count = 0 + mem_map _ h := h + mem_par h₁ h₂ := by simp [h₁, h₂] + mem_wire h₁ h₂ := by simp [h₁, h₂] + +instance : zeroCountSubTheory.IsStructural where + mem_unit := rfl + mem_idWire _ := rfl + +/-- Every atom accepted by `toyAllowed` has zero forbidden-atom count. -/ +theorem atomCount_eq_zero_of_allowed {Δ : PortBoundary} (a : ToyAtom Δ) + (ha : toyAllowed a) : zeroCountSubTheory.mem (atomCount a) := by + cases a <;> simp_all [toyAllowed, atomCount, zeroCountSubTheory] + /-- The generated class is structural: it contains the unit and every identity wire, found by synthesis. -/ example : (OpenSyntax.atomSubTheory ToyAtom toyAllowed).IsStructural := inferInstance @@ -199,14 +292,52 @@ example (Δ : PortBoundary) : (OpenSyntax.atomSubTheory.mem_atom ToyAtom toyAllowed trivial) (OpenSyntax.atomSubTheory.mem_atom ToyAtom toyAllowed trivial) -/-- The forbidden atom really is forbidden. -/ -example (Δ : PortBoundary) : ¬ toyAllowed (ToyAtom.bad Δ) := id +/-- The forbidden atom is absent from the quotiented generated sub-theory, not +only from the predicate on raw generators. -/ +example (Δ : PortBoundary) : + ¬(OpenSyntax.atomSubTheory ToyAtom toyAllowed).mem + (OpenSyntax.Expr.atom (ToyAtom.bad Δ)) := by + intro h + have hCount := OpenSyntax.mem_interpret_of_atoms ToyAtom toyAllowed + zeroCountSubTheory atomCount atomCount_eq_zero_of_allowed h + simp [zeroCountSubTheory, atomCount] at hCount /-- Allowing strictly more atoms gives a larger class. -/ example : OpenSyntax.atomSubTheory ToyAtom toyAllowed ≤ OpenSyntax.atomSubTheory ToyAtom (fun _ => True) := OpenSyntax.atomSubTheory.mono ToyAtom fun _ _ => trivial +/-! ### Restricted-context and simulator canaries -/ + +/-- Antitonicity is exercised on a class that excludes `ToyAtom.bad`, rather +than only on `SubTheory.top`. -/ +example {Δ : PortBoundary} {Obs : Observation ToyTheory} {real ideal : ToyTheory.Obj Δ} + (h : EmulatesWithin (OpenSyntax.atomSubTheory ToyAtom (fun _ => True)) real ideal Obs) : + EmulatesWithin (OpenSyntax.atomSubTheory ToyAtom toyAllowed) real ideal Obs := + h.mono (OpenSyntax.atomSubTheory.mono ToyAtom fun _ _ => trivial) + +/-- Identity simulation preserves a genuinely restricted allowed class. -/ +example {Δ : PortBoundary} : + (OpenSyntax.atomSubTheory ToyAtom toyAllowed).PreservesAllowedness + (Δ := Δ) (fun K => K) := + fun _ hK => hK + +/-- A simulator that replaces every allowed context with a forbidden atom does +not preserve allowedness. -/ +example : + ¬(OpenSyntax.atomSubTheory ToyAtom toyAllowed).PreservesAllowedness + (Δ := PortBoundary.empty) + (fun _ => OpenSyntax.Expr.atom (ToyAtom.bad PortBoundary.empty)) := by + intro h + exact (show ¬(OpenSyntax.atomSubTheory ToyAtom toyAllowed).mem + (OpenSyntax.Expr.atom (ToyAtom.bad PortBoundary.empty)) by + intro hBad + have hCount := OpenSyntax.mem_interpret_of_atoms ToyAtom toyAllowed + zeroCountSubTheory atomCount atomCount_eq_zero_of_allowed hBad + simp [zeroCountSubTheory, atomCount] at hCount) + (h (OpenSyntax.Expr.atom (ToyAtom.good PortBoundary.empty)) + (OpenSyntax.atomSubTheory.mem_atom ToyAtom toyAllowed trivial)) + /-- **The transfer theorem.** Interpreting a network of allowed atoms into any target class that accepts the allowed atoms lands inside that class. Taken at the identity interpretation, it says the generated class is closed under diff --git a/docs/wiki/interaction.md b/docs/wiki/interaction.md index 6573a8c..24a5710 100644 --- a/docs/wiki/interaction.md +++ b/docs/wiki/interaction.md @@ -649,11 +649,11 @@ import PolyFun.Interaction.UC.OpenProcessModel | `OpenSyntax/Expr.lean` | `Expr` (quotient of `Raw`), granular `OpenTheory` lawfulness instances, `Expr.toInterp` | | `OpenProcess.lean` | `BoundaryAction`, `OpenNodeProfile`, `OpenNodeContext` (with polynomial-product bridge `productView` and structural `boundaryTrace`), `OpenProcess m Party Δ` (monad-parametric, with intrinsic `stepSampler`), `toProcess`, `OpenProcessActivationEquiv` | | `OpenProcessModel.lean` | `openTheory m Party schedulerSampler` (concrete model threading `TypeTree.Sampler` through `map` / `par` / `wire` / `plug`), `IsLawful`, monoidal / CC laws up to `OpenProcessActivationEquiv` | -| `SubTheory.lean` | `SubTheory` (a boundary-indexed membership predicate on `T.Obj` closed under `map` / `par` / `wire`), the `IsPlugClosed` and `IsStructural` mixins, the order `≤` with `top` and `inf`, and `SubTheory.generated` with its induction principle `generated_le`. The allowed-systems parameter a UC development fixes before stating security; instantiable at a corruption discipline, a resource bound, or their meet. No cost or probability content. | +| `SubTheory.lean` | `SubTheory` (a boundary-indexed membership predicate on `T.Obj` closed under `map` / `par` / `wire`), the `IsPlugClosed` and `IsStructural` mixins, standard `PartialOrder` / `OrderTop` / `SemilatticeInf` instances, ordinary `generated`, and the separately named least plug-closed construction `plugGenerated`. This is structural membership only: resource, efficiency, realizability, protocol-class, and corruption readings require explicit bridges. The proposed `StepClass` / realizability bridge is planned in PR #113 and is not in this stack. | | `Emulates.lean` | `Observation`, `Emulates`, `UCSecure`. Contextual emulation and UC security stated abstractly over an `Observation` (an equivalence relation on closed systems), with no probability monad and no concrete security predicate. Composition takes its structural input from the observation via `Observation.RespectsPlugComm` / `Observation.RespectsFactorization`; strict `HasPlugWireFactor` theories satisfy both automatically. | -| `EmulatesWithin.lean` | `EmulatesWithin` (emulation quantified only over `SubTheory`-allowed plugs) and the composition suite relativized to it, plus `UCSecureWithin`, whose simulator must map allowed contexts to allowed contexts. Each theorem gains one hypothesis — the untouched component must itself be allowed — because the residual context is built from it. `emulatesWithin_top_iff` shows the layer is a conservative extension. | +| `EmulatesWithin.lean` | `EmulatesWithin` (emulation quantified only over `SubTheory`-allowed closing contexts) and its relativized composition suite, plus `UCSecureWithin` and `SubTheory.PreservesAllowedness`. The latter says only that the chosen simulator maps allowed contexts to allowed contexts; it does not prove simulator realizability or efficiency. Real/ideal protocol membership is also separate. Each composition theorem requests the precise component membership needed to build its residual context. `emulatesWithin_top_iff` shows the layer is a conservative extension. | | `OpenProcessEmulates.lean` | `Observation.IsSchedulingInsensitive` (an observation that cannot see activation-preserving scheduling structure) and the `RespectsPlugComm` instance it yields for `openTheory`, transporting `openTheory_plug_comm_activation_equiv` onto the abstract composition theorems | -| `OpenSyntax/AtomSubTheory.lean` | `AllowedGen` / `atomSubTheory` (the sub-theory of `Expr.theory` generated by an allowed set of atoms, plus the identity wires), the pullback `interpretSubTheory`, and `mem_interpret_of_atoms`: if every allowed atom interprets into a target sub-theory, so does every network built from them. | +| `OpenSyntax/AtomSubTheory.lean` | `AllowedGen` / `atomSubTheory` (the least map/par/wire-closed sub-theory of quotiented `Expr.theory` generated by an allowed set of atoms plus identity wires), the pullback `interpretSubTheory`, and `mem_interpret_of_atoms`: if every allowed atom interprets into a target sub-theory, so does every generated expression. Quotient equality preserves membership; membership is not generally decidable. | | `Notation.lean` | UC notation helpers (`∥`, `⊞`, `⊠`, `⊗ᵇ`, `ᵛ`); see [`notation.md`](notation.md) | | `MachineId.lean` | machine identifiers | | `EnvAction.lean` | environment actions, parametric over an arbitrary monad `m` (no probability dependency) | diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md index 68db1a0..e3d484c 100644 --- a/docs/wiki/repo-map.md +++ b/docs/wiki/repo-map.md @@ -188,9 +188,11 @@ Interaction/UC/OpenTheory -> Interaction/UC/SubTheory Interaction/UC/{Emulates, SubTheory} -> Interaction/UC/EmulatesWithin Interaction/UC/{OpenSyntax/Expr, SubTheory} -> Interaction/UC/OpenSyntax/AtomSubTheory - (SubTheory is the allowed-systems predicate and depends on the algebra - alone; the residual-context lemmas that relativized emulation needs live - with EmulatesWithin because the context-formers are defined in Emulates) + (SubTheory is a structural membership predicate and depends on the algebra + alone; EmulatesWithin uses it specifically for allowed closing contexts. + Protocol membership, resource and realizability claims, and links to + CorruptionModel require separate bridges. The residual-context lemmas live + with EmulatesWithin because the context-formers are defined in Emulates.) Interaction/UC/{Emulates, OpenProcessModel} -> Interaction/UC/OpenProcessEmulates (Emulates is model-agnostic and must not reach OpenProcess; the bridge that From c72aa500aa9acd79460594c47052c70df3cdc825 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Thu, 13 Aug 2026 15:49:22 -0500 Subject: [PATCH 5/5] fix(uc): state the process-model plug example on RespectsPlugComm `Observation.IsSchedulingInsensitive` requires an observation to identify everything `OpenProcessActivationEquiv` identifies, and that relation erases packet identity and `stepSampler`. No packet- or sampler-aware observation can inhabit it, so it is not a route by which a security observation reaches the composition suite. State the process-model example on `Obs.RespectsPlugComm` directly, which is what `EmulatesWithin.plug_compose` actually consumes, and drop the docstring's reference to an open pull request. Co-Authored-By: Claude Opus 5 (1M context) --- PolyFun/Interaction/UC/SubTheory.lean | 6 +++--- PolyFunTest/Interaction/UC/SubTheoryExamples.lean | 12 +++++++----- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/PolyFun/Interaction/UC/SubTheory.lean b/PolyFun/Interaction/UC/SubTheory.lean index e61fb2b..c30cf11 100644 --- a/PolyFun/Interaction/UC/SubTheory.lean +++ b/PolyFun/Interaction/UC/SubTheory.lean @@ -55,9 +55,9 @@ member satisfies another sub-theory reduces to checking the generators. Resource witnesses, if introduced later, belong inside the proposition or in a separate realizability layer. -The proposed `PFunctor.StepClass` and realizability layer are planned in -PolyFun PR #113; they are not dependencies of this module. A future bridge may -relate those classes to `SubTheory.mem` after their closure laws are available. +Nothing in this module depends on a realizability layer. Should one exist, a +bridge relating its admissibility classes to `SubTheory.mem` would need those +classes' own closure laws first. `SubTheory` is also separate from `Interaction.UC.CorruptionModel`, which describes corruption events, states, and environment actions. Relating a diff --git a/PolyFunTest/Interaction/UC/SubTheoryExamples.lean b/PolyFunTest/Interaction/UC/SubTheoryExamples.lean index 1349f07..e5d9a17 100644 --- a/PolyFunTest/Interaction/UC/SubTheoryExamples.lean +++ b/PolyFunTest/Interaction/UC/SubTheoryExamples.lean @@ -8,7 +8,7 @@ module import all PolyFun.Interaction.UC.EmulatesWithin public import PolyFun.Interaction.UC.EmulatesWithin -public import PolyFun.Interaction.UC.OpenProcessEmulates +public import PolyFun.Interaction.UC.OpenProcessModel public import PolyFun.Interaction.UC.OpenSyntax.AtomSubTheory /-! @@ -143,16 +143,18 @@ end FreeModel /-! ### The relativized `plug` theorem on the process model -`openTheory` has no strict factorization, so it reaches these through -`Observation.IsSchedulingInsensitive` rather than -`OpenTheory.HasPlugWireFactor`. -/ +`openTheory` has no `OpenTheory.HasPlugWireFactor` instance, so it cannot reach +the relativized `plug` theorem by strict factorization. It reaches it from +`Observation.RespectsPlugComm` alone, however that class is earned — which is +the point of stating the structural input on the observation rather than on the +theory. -/ section ProcessModel variable (Party : Type u) (m : Type w → Type w') [Monad m] (schedulerSampler : m (ULift.{w, 0} Bool)) (Obs : Observation (openTheory.{u, v, w, w'} Party m schedulerSampler)) - [Observation.IsSchedulingInsensitive Obs] + [Obs.RespectsPlugComm] (D : SubTheory (openTheory.{u, v, w, w'} Party m schedulerSampler)) example {Δ : PortBoundary}