diff --git a/AGENTS.md b/AGENTS.md index fbd0068..9a6aedd 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -74,7 +74,12 @@ and depend on this library. interleaving, observation. - `UC/`: open-process / open-theory layer, structural composition (interfaces, par, wire, plug), corruption models, environment - actions, leakage. *Generic only* — security-flavored UC layers + actions, leakage, and composition-closed sub-theories (`SubTheory`, a + boundary-indexed membership predicate, with contextual emulation + relativized to its allowed closing contexts). This relativization does not + assert real/ideal protocol membership, resource bounds, simulator + realizability, or a connection to `CorruptionModel`; those require explicit + downstream bridges. *Generic only* — security-flavored UC layers (computational equivalence, asymptotic security) live in VCVio. - `PolyFun/Control/`: monad and comonad infrastructure transitively required by the above (coalgebra, comonad, free / freecont monad diff --git a/PolyFun.lean b/PolyFun.lean index 52a346d..93e3853 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 @@ -110,10 +111,12 @@ public import PolyFun.Interaction.UC.MomentaryCorruption public import PolyFun.Interaction.UC.Notation public import PolyFun.Interaction.UC.OpenProcess public import PolyFun.Interaction.UC.OpenProcessModel +public import PolyFun.Interaction.UC.OpenSyntax.AtomSubTheory public import PolyFun.Interaction.UC.OpenSyntax.Expr public import PolyFun.Interaction.UC.OpenSyntax.Interp public import PolyFun.Interaction.UC.OpenSyntax.Raw public import PolyFun.Interaction.UC.OpenTheory +public import PolyFun.Interaction.UC.SubTheory public import PolyFun.Logic.HEq public import PolyFun.PFunctor.Adjunctions public import PolyFun.PFunctor.Basic diff --git a/PolyFun/Interaction/UC/EmulatesWithin.lean b/PolyFun/Interaction/UC/EmulatesWithin.lean new file mode 100644 index 0000000..d89e3de --- /dev/null +++ b/PolyFun/Interaction/UC/EmulatesWithin.lean @@ -0,0 +1,335 @@ +/- +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. + +`EmulatesWithin D real ideal Obs` restricts that quantifier to the plugs +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 + +* `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. +* `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 + +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. + +## What simulator preservation says + +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 + +universe u + +namespace Interaction +namespace UC + +variable {T : OpenTheory.{u}} + +/-! ## Residual contexts stay allowed -/ + +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 Δ₂} + {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 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) : + 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`.** + +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 Δ₂} + (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 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, + 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 +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..964c008 --- /dev/null +++ b/PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean @@ -0,0 +1,201 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ + +module + +public import PolyFun.Interaction.UC.OpenSyntax.Expr +public import PolyFun.Interaction.UC.SubTheory + +/-! +# Sub-theories of the free open theory, generated by allowed atoms + +The free model is already presented by generators. A predicate on atoms gives +a canonical sub-theory of `Expr.theory Atom`: fix which primitive components +may be used, then close them under `map`, `par`, and `wire`. + +`atomSubTheory A` is that sub-theory. Its generators are the atoms satisfying +`A` together with the identity wires, which are structure rather than +components and so are always allowed. + +## The transfer theorem + +`mem_interpret_of_atoms` is the reason this file exists. It says: if every +allowed atom interprets into a target sub-theory `D`, then every syntactic +system built from allowed atoms interprets into `D`. + +The result is purely structural. Any resource, corruption, or realizability +interpretation of `D.mem` requires a separate bridge establishing that +interpretation and its closure laws. + +## Why this needs no reasoning about the quotient + +`Expr` is a quotient of `Raw` by the open-theory equations, so a predicate +defined by structural recursion on `Raw` would have to be shown invariant +under all twenty-odd equations. `SubTheory.generated` sidesteps that entirely: +it is defined by the *operations of the theory*, which act on the quotient +already, so `atomSubTheory` is well-defined by construction and its induction +principle is `SubTheory.generated_le`. + +A consequence worth stating: membership is extensional on the quotient but is +not generally decidable. `atomSubTheory A` contains every expression that can +be assembled from allowed atoms, and equality in `Expr` preserves membership. +-/ + +public section + +universe u v + +namespace Interaction +namespace UC +namespace OpenSyntax + +/-- +The generators of a syntactic sub-theory: the atoms allowed by `A`, together +with the identity wires. + +Identity wires are included unconditionally because they are the wires of the +diagram rather than components in it. A class of protocols closed under +rewiring must contain them, and no restriction on primitive components can +sensibly forbid them. + +`Atom` is an explicit parameter here and in `atomSubTheory`: it cannot be +recovered from the type of `A`, since solving `?Atom ?Δ ≡ Atom Δ` is not a +first-order problem. +-/ +inductive AllowedGen (Atom : PortBoundary → Type u) + (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop) : + ∀ (Δ : PortBoundary), Expr Atom Δ → Prop where + /-- An allowed atom is a generator. -/ + | atom {Δ : PortBoundary} {a : Atom Δ} : A a → AllowedGen Atom A Δ (Expr.atom a) + /-- Every identity wire is a generator. -/ + | idWire (Γ : PortBoundary) : + AllowedGen Atom A (PortBoundary.tensor (PortBoundary.swap Γ) Γ) (Expr.idWire Γ) + +/-- +The sub-theory of `Expr.theory Atom` generated by the atoms satisfying `A`. + +This is the formal counterpart of "the protocols one is allowed to write": +a choice of primitive components, closed under the composition operations. +-/ +@[expose] +def atomSubTheory (Atom : PortBoundary → Type u) + (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop) : SubTheory (Expr.theory Atom) := + SubTheory.generated (Expr.theory Atom) (AllowedGen Atom A) + +namespace atomSubTheory + +/-- An allowed atom is an allowed system. -/ +theorem mem_atom (Atom : PortBoundary → Type u) (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop) + {Δ : PortBoundary} {a : Atom Δ} (ha : A a) : + (atomSubTheory Atom A).mem (Expr.atom a) := + SubTheory.Generated.base (AllowedGen.atom ha) + +/-- Identity wires are always allowed. -/ +theorem mem_idWire (Atom : PortBoundary → Type u) (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop) + (Γ : PortBoundary) : (atomSubTheory Atom A).mem (Expr.idWire Γ) := + SubTheory.Generated.base (AllowedGen.idWire Γ) + +instance isStructural (Atom : PortBoundary → Type u) + (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop) : (atomSubTheory Atom A).IsStructural where + mem_unit := + -- `Expr.unit` is `idWire` on the empty boundary pushed through a unitor. + SubTheory.Generated.map + (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom + (mem_idWire Atom A PortBoundary.empty) + mem_idWire Γ := mem_idWire Atom A Γ + +/-- Allowing more atoms yields a larger sub-theory. -/ +theorem mono (Atom : PortBoundary → Type u) + {A₁ A₂ : ∀ {Δ : PortBoundary}, Atom Δ → Prop} + (h : ∀ {Δ : PortBoundary} (a : Atom Δ), A₁ a → A₂ a) : + atomSubTheory Atom A₁ ≤ atomSubTheory Atom A₂ := + SubTheory.generated_mono fun _ _ hg => by + cases hg with + | atom ha => exact AllowedGen.atom (h _ ha) + | idWire Γ => exact AllowedGen.idWire Γ + +end atomSubTheory + +/-- +The pullback of a sub-theory of `T` along an interpretation of atoms. + +An expression is allowed exactly when its interpretation is. This is a +sub-theory because `Expr.interpret` commutes with every operation, so each +closure field is the target's closure field transported across one rewrite. + +It exists so that the transfer theorem below can be an application of +`SubTheory.generated_le` rather than a fresh induction: the induction was +done once, in the induction principle. +-/ +@[expose] +def interpretSubTheory (Atom : PortBoundary → Type u) {T : OpenTheory.{v}} + [OpenTheory.HasPlugWireFactor T] (D : SubTheory T) + (interp : ∀ {Δ : PortBoundary}, Atom Δ → T.Obj Δ) : SubTheory (Expr.theory Atom) where + mem e := D.mem (e.interpret T interp) + mem_map φ h := by simpa only [Expr.interpret_map] using D.mem_map φ h + mem_par h₁ h₂ := by simpa only [Expr.interpret_par] using D.mem_par h₁ h₂ + mem_wire h₁ h₂ := by simpa only [Expr.interpret_wire] using D.mem_wire h₁ h₂ + +instance isPlugClosed_interpretSubTheory (Atom : PortBoundary → Type u) {T : OpenTheory.{v}} + [OpenTheory.HasPlugWireFactor T] (D : SubTheory T) + (interp : ∀ {Δ : PortBoundary}, Atom Δ → T.Obj Δ) : + (interpretSubTheory Atom D interp).IsPlugClosed where + mem_plug h₁ h₂ := by + simpa only [Expr.interpret_plug] using SubTheory.IsPlugClosed.mem_plug h₁ h₂ + +instance isStructural_interpretSubTheory (Atom : PortBoundary → Type u) {T : OpenTheory.{v}} + [OpenTheory.HasPlugWireFactor T] (D : SubTheory T) [D.IsStructural] + (interp : ∀ {Δ : PortBoundary}, Atom Δ → T.Obj Δ) : + (interpretSubTheory Atom D interp).IsStructural where + mem_unit := by + change D.mem ((Expr.unit : Expr Atom PortBoundary.empty).interpret T interp) + rw [Expr.interpret_unit] + exact SubTheory.IsStructural.mem_unit + -- `Expr.interpret_idWire` is `rfl`, so this case is definitional. + mem_idWire Γ := SubTheory.IsStructural.mem_idWire (D := D) Γ + +/-- +**Transfer of allowedness along interpretation.** + +If every atom allowed by `A` interprets into the target sub-theory `D`, then +every expression built from allowed atoms interprets into `D`. + +Nothing about the target is used beyond its structural and closure fields. Any +stronger interpretation of target membership is external to this theorem. + +This is the structural form of the assumption that a network of admissible +machines is admissible: instead of a global claim about networks, one supplies +the generators (`hA`) and the closure fields carried by `D` itself. +-/ +theorem mem_interpret_of_atoms (Atom : PortBoundary → Type u) + (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop) + {T : OpenTheory.{v}} [OpenTheory.HasPlugWireFactor T] (D : SubTheory T) [D.IsStructural] + (interp : ∀ {Δ : PortBoundary}, Atom Δ → T.Obj Δ) + (hA : ∀ {Δ : PortBoundary} (a : Atom Δ), A a → D.mem (interp a)) + {Δ : PortBoundary} {e : Expr Atom Δ} (he : (atomSubTheory Atom A).mem e) : + D.mem (e.interpret T interp) := + SubTheory.mem_of_le + (SubTheory.generated_le (interpretSubTheory Atom D interp) fun _ _ hg => by + -- Both `Expr.interpret_atom` and `Expr.interpret_idWire` hold by `rfl`, + -- so each generator case is discharged definitionally. + cases hg with + | atom ha => exact hA _ ha + | idWire Γ => exact SubTheory.IsStructural.mem_idWire (D := D) Γ) + he + +/-- The whole allowed class transfers at once: `atomSubTheory` sits inside the +pullback of any target sub-theory that accepts the allowed atoms. -/ +theorem atomSubTheory_le_interpretSubTheory (Atom : PortBoundary → Type u) + (A : ∀ {Δ : PortBoundary}, Atom Δ → Prop) + {T : OpenTheory.{v}} [OpenTheory.HasPlugWireFactor T] (D : SubTheory T) [D.IsStructural] + (interp : ∀ {Δ : PortBoundary}, Atom Δ → T.Obj Δ) + (hA : ∀ {Δ : PortBoundary} (a : Atom Δ), A a → D.mem (interp a)) : + atomSubTheory Atom A ≤ interpretSubTheory Atom D interp := + fun _ he => mem_interpret_of_atoms Atom A D interp hA he + +end OpenSyntax +end UC +end Interaction diff --git a/PolyFun/Interaction/UC/SubTheory.lean b/PolyFun/Interaction/UC/SubTheory.lean new file mode 100644 index 0000000..c30cf11 --- /dev/null +++ b/PolyFun/Interaction/UC/SubTheory.lean @@ -0,0 +1,427 @@ +/- +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 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 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 + +* `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. +* The standard `PartialOrder`, `OrderTop`, and `SemilatticeInf` API. `top` allows + everything, so every statement relativized to `top` is the unrelativized + 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 + +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 satisfies another sub-theory reduces to checking the generators. + +## Design notes + +`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. + +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 +corruption model to a class of allowed closing contexts or protocol systems is +future work and requires an explicit bridge. +-/ + +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. + +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`. +-/ +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) + +/-- 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 := + 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 + +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. It combines independent +composition-closed restrictions 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⟩ + +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 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. + +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 + /-- 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₂) + +/-- +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₂ + +/-- 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. + +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) + (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₂ + +/-- 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) + +/-! ### 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 +end Interaction diff --git a/PolyFunTest/Interaction/UC/SubTheoryExamples.lean b/PolyFunTest/Interaction/UC/SubTheoryExamples.lean new file mode 100644 index 0000000..e5d9a17 --- /dev/null +++ b/PolyFunTest/Interaction/UC/SubTheoryExamples.lean @@ -0,0 +1,364 @@ +/- +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.OpenProcessModel +public import PolyFun.Interaction.UC.OpenSyntax.AtomSubTheory + +/-! +# Sub-theory examples + +Checks that the allowed-systems layer behaves as intended: + +* 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`, +* 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) + +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 + +/-- A meet of plug-closed classes is plug-closed. -/ +example [D₁.IsPlugClosed] [D₂.IsPlugClosed] : (SubTheory.inf D₁ D₂).IsPlugClosed := inferInstance + +/-- Plug-closed generation is plug-closed without a factorization law. -/ +example (G : ∀ Δ : PortBoundary, T.Obj Δ → Prop) : + (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. -/ +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 + +/-- 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 -/ + +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 `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)) + [Obs.RespectsPlugComm] + (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 + +/-- 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 + +/-- 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 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 +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/gotchas.md b/docs/wiki/gotchas.md index 76ed1b3..fd74b68 100644 --- a/docs/wiki/gotchas.md +++ b/docs/wiki/gotchas.md @@ -118,6 +118,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 diff --git a/docs/wiki/interaction.md b/docs/wiki/interaction.md index 1fb8ebe..98d9a9c 100644 --- a/docs/wiki/interaction.md +++ b/docs/wiki/interaction.md @@ -649,7 +649,10 @@ 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, 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. | | `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 exact structural input from the observation via `Observation.RespectsPlugComm` / `Observation.RespectsFactorization`; strict `HasPlugWireFactor` theories satisfy both automatically. Process-backed security observations must prove these laws without erasing security-visible packet, action, or sampler data. | +| `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. | +| `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 bef981c..28d62e7 100644 --- a/docs/wiki/repo-map.md +++ b/docs/wiki/repo-map.md @@ -184,6 +184,16 @@ Interaction/{Concurrent, Basic} -> Interaction/UC/{Interface, Emulates, MachineId, EnvAction, 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 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.) ``` `PolyFun.lean` is a generated umbrella import file, not a hand-maintained