Anchored at 31216a8f. Companion to #121, which takes the first step; this issue records the design argument behind it and two further proposals it opens up. Nothing here is scheduled — it is written to be argued with.
The observation
Emulates' composition theorems are derived from strict structure of the theory. Observation is a relation on T.Closed only:
structure Observation (T : OpenTheory.{u}) where
rel : T.Closed → T.Closed → Prop
equiv : Equivalence relBecause it lives only at the ground level, every proof that moves a component across the system/context divide has to route through an equality of closed systems — close_par_left, close_wire_left, plug_comm — and those come from HasPlugWireFactor. The concrete process model has none of them on the nose, which is why Emulates.lean says its composition theorems "do not apply to it directly."
But look at what those theorems prove:
theorem par_compose (h₁ : Emulates real₁ ideal₁ Obs) (h₂ : Emulates real₂ ideal₂ Obs) :
Emulates (T.par real₁ real₂) (T.par ideal₁ ideal₂) Obs
theorem wire_left (h₁ : Emulates real₁ ideal₁ Obs) (W₂ : ...) :
Emulates (T.wire real₁ W₂) (T.wire ideal₁ W₂) ObsRead fun Δ W₁ W₂ => Emulates W₁ W₂ Obs as a family indexed by boundary, and these are precisely the parallel and sequential closure conditions one would assume of an abstract indistinguishability relation — Definition III.3 of ePrint 2026/1605, which then derives the dummy-adversary theorem, closure under both compositions, and universal composition from them and nothing else.
So we derive what that treatment assumes, and pay for it with a strictness requirement our own flagship model does not meet. That is the whole diagnosis.
Proposal 1 — make Observation a boundary-indexed family
Generalize from a relation on T.Closed to a family ∀ Δ, T.Obj Δ → T.Obj Δ → Prop closed under the two conditions above, with the closed-system relation recovered at Δ = empty.
The pull is that closure becomes something a model can satisfy semantically — by an argument about what its observation can see — rather than structurally, by exhibiting equalities its composites do not satisfy. It also removes the current asymmetry where Emulates is defined by quantifying over plugs but the thing being quantified is only comparable at the ground level.
#121 is the first, non-breaking move in this direction: it keeps Observation as-is but makes the closure laws an interface (Observation.RespectsPlugComm, Observation.RespectsFactorization) that a model can satisfy however it likes. Whether to go the rest of the way is the open question. Costs worth weighing: Emulates and UCSecure both change shape, and the free syntax models currently get everything for free from strictness.
Proposal 2 — a sub-theory of allowed real-world systems
The categorical treatment has one parameter, D_real ⊆ D_bd, that says which systems may appear in a real-world protocol. It carries two things at once: the corruption model (restrict the generators and you get static, or honest-but-curious, or fully corruptible) and the efficiency restriction.
We currently spread that across unrelated mechanisms. CorruptionModel is a first-class bundle — genuinely richer than a generator restriction, since MomentaryCorruption expresses compromise-and-refresh that static UC cannot state at all — and efficiency has no representation in this repo whatsoever. Downstream in VCVio it exists only as an opaque predicate isPPT : Adv → Prop on an opaque index type, which no composition proof consumes.
The proposal is to ask whether an "allowed systems" sub-theory is the right shared slot for both. Two things make it attractive: it would give the corruption model a categorical reading it currently lacks, and it would give efficiency somewhere to live that composition theorems could actually quantify over. The interesting research question runs the other way — a generator restriction cannot express momentary corruption, so if the answer is "corruption is an effect channel, not a subcategory," that is a finding worth writing down.
Proposal 3 — decide which scheduler is canonical
Scheduling currently enters at three unrelated places:
schedulerSampler : m (ULift Bool), baked into openTheory and threaded identically into par, wire, and plugOpenProcess.stepSampler, internal to each system- downstream, VCVio's
SchedulerPair, which parameterizes the semantics rather than the system — and whose process half is currently unreachable, since processSemanticsAsync takes only the env scheduler
Because there is no single answer to "who chooses the interleaving," OpenProcessActivationEquiv ends up as something to route around rather than a principled quotient, and the fairness vocabulary in VCVio's AsyncSecurity.lean (WeakFair, StrongFair, Ticketed) has nothing to attach to — it is stated over a free infinite-run object with no theorem connecting it to runStepsAsync or to any induced distribution.
Picking one canonical entry point is a prerequisite for the fairness layer meaning anything, and would decide whether activation equivalence is the right quotient or merely the convenient one.
Non-goals
No cryptographic content in PolyFun — probability stays downstream, per the scope boundary in AGENTS.md. No dynamic party creation or dynamic sessions; the categorical treatment above is for static systems only and its own conclusion calls full UC "a difficult question." No attempt to unify with Broadbent–Karvonen's categorical composable cryptography, which is a different theory that neither subsumes nor is subsumed by it.
Anchored at
31216a8f. Companion to #121, which takes the first step; this issue records the design argument behind it and two further proposals it opens up. Nothing here is scheduled — it is written to be argued with.The observation
Emulates' composition theorems are derived from strict structure of the theory.Observationis a relation onT.Closedonly:Because it lives only at the ground level, every proof that moves a component across the system/context divide has to route through an equality of closed systems —
close_par_left,close_wire_left,plug_comm— and those come fromHasPlugWireFactor. The concrete process model has none of them on the nose, which is whyEmulates.leansays its composition theorems "do not apply to it directly."But look at what those theorems prove:
Read
fun Δ W₁ W₂ => Emulates W₁ W₂ Obsas a family indexed by boundary, and these are precisely the parallel and sequential closure conditions one would assume of an abstract indistinguishability relation — Definition III.3 of ePrint 2026/1605, which then derives the dummy-adversary theorem, closure under both compositions, and universal composition from them and nothing else.So we derive what that treatment assumes, and pay for it with a strictness requirement our own flagship model does not meet. That is the whole diagnosis.
Proposal 1 — make
Observationa boundary-indexed familyGeneralize from a relation on
T.Closedto a family∀ Δ, T.Obj Δ → T.Obj Δ → Propclosed under the two conditions above, with the closed-system relation recovered atΔ = empty.The pull is that closure becomes something a model can satisfy semantically — by an argument about what its observation can see — rather than structurally, by exhibiting equalities its composites do not satisfy. It also removes the current asymmetry where
Emulatesis defined by quantifying over plugs but the thing being quantified is only comparable at the ground level.#121 is the first, non-breaking move in this direction: it keeps
Observationas-is but makes the closure laws an interface (Observation.RespectsPlugComm,Observation.RespectsFactorization) that a model can satisfy however it likes. Whether to go the rest of the way is the open question. Costs worth weighing:EmulatesandUCSecureboth change shape, and the free syntax models currently get everything for free from strictness.Proposal 2 — a sub-theory of allowed real-world systems
The categorical treatment has one parameter,
D_real ⊆ D_bd, that says which systems may appear in a real-world protocol. It carries two things at once: the corruption model (restrict the generators and you get static, or honest-but-curious, or fully corruptible) and the efficiency restriction.We currently spread that across unrelated mechanisms.
CorruptionModelis a first-class bundle — genuinely richer than a generator restriction, sinceMomentaryCorruptionexpresses compromise-and-refresh that static UC cannot state at all — and efficiency has no representation in this repo whatsoever. Downstream in VCVio it exists only as an opaque predicateisPPT : Adv → Propon an opaque index type, which no composition proof consumes.The proposal is to ask whether an "allowed systems" sub-theory is the right shared slot for both. Two things make it attractive: it would give the corruption model a categorical reading it currently lacks, and it would give efficiency somewhere to live that composition theorems could actually quantify over. The interesting research question runs the other way — a generator restriction cannot express momentary corruption, so if the answer is "corruption is an effect channel, not a subcategory," that is a finding worth writing down.
Proposal 3 — decide which scheduler is canonical
Scheduling currently enters at three unrelated places:
schedulerSampler : m (ULift Bool), baked intoopenTheoryand threaded identically intopar,wire, andplugOpenProcess.stepSampler, internal to each systemSchedulerPair, which parameterizes the semantics rather than the system — and whose process half is currently unreachable, sinceprocessSemanticsAsynctakes only the env schedulerBecause there is no single answer to "who chooses the interleaving,"
OpenProcessActivationEquivends up as something to route around rather than a principled quotient, and the fairness vocabulary in VCVio'sAsyncSecurity.lean(WeakFair,StrongFair,Ticketed) has nothing to attach to — it is stated over a free infinite-run object with no theorem connecting it torunStepsAsyncor to any induced distribution.Picking one canonical entry point is a prerequisite for the fairness layer meaning anything, and would decide whether activation equivalence is the right quotient or merely the convenient one.
Non-goals
No cryptographic content in PolyFun — probability stays downstream, per the scope boundary in
AGENTS.md. No dynamic party creation or dynamic sessions; the categorical treatment above is for static systems only and its own conclusion calls full UC "a difficult question." No attempt to unify with Broadbent–Karvonen's categorical composable cryptography, which is a different theory that neither subsumes nor is subsumed by it.