State-Separating Proofs: Composition

This file defines the two basic composition operators on Packages and proves the program-level reduction lemmas relating their simulateQ and run to nested calls.

• Package.link — sequential composition. Given an outer package importing M and exporting E, and an inner package importing I and exporting M, produce a single package importing I and exporting E, with state σ₁ × σ₂.
• Package.par — parallel composition. Given two packages with disjoint export and import interfaces, combine them into a single package on the disjoint sums I₁ + I₂ and E₁ + E₂, with state σ₁ × σ₂.
• Package.simulateQ_link_run, Package.run_link, Package.run_link_ofStateless — the unbundled and bundled program-equivalence forms of the SSP "reduction lemma" for link.

These correspond to SSProve's link and par. Disjointness of the two state factors is structural: each side's handler can only modify its own factor, so non-interference is a type-level fact rather than a separation predicate that needs to be proved.

Universe layout

All five "module" universes (the indices uᵢ, uₘ, uₑ and the import-range universe vᵢ) are independent. Both packages on either side of link must agree on the universe v of their export ranges and state, since link's product state lives in Type v. Likewise par requires the import ranges of p₁ and p₂ to share a universe (so + for OracleSpec typechecks), and similarly for the export ranges.

Sequential composition (link)

def VCVio.SSP.Package.link {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ σ₂ : Type v} (outer : Package M E σ₁) (inner : Package I M σ₂) : Package I E (σ₁ × σ₂)

Sequential composition of two packages: outer ∘ inner.

The outer package exports E and imports M. The inner package exports M and imports I. The composite exports E and imports I, with state σ₁ × σ₂ (outer state on the left, inner state on the right). Each export query of the composite runs the outer handler in state σ₁, then re-interprets every import-query in M it issues by running the inner handler in state σ₂.

@[simp]

theorem VCVio.SSP.Package.link_init {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ σ₂ : Type v} (outer : Package M E σ₁) (inner : Package I M σ₂) : (outer.link inner).init = (outer.init, inner.init)

@[simp]

theorem VCVio.SSP.Package.link_id_init {ιₑ : Type uₑ} {E : OracleSpec ιₑ} {σ₁ : Type v} {ι : Type uₘ} (M' : OracleSpec ι) (P : Package M' E σ₁) : (P.link (Package.id M')).init = (P.init, PUnit.unit)

Sanity check: linking with the identity package on the right keeps the outer state, with a PUnit placeholder on the right. The full state-isomorphism σ × PUnit ≃ σ is left to follow-up files; this lemma only requires the Package's import / export range universes to agree with the identity package's range universe.

link reduction lemmas

theorem VCVio.SSP.Package.simulateQ_link_run {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ σ₂ α : Type v} (P : Package M E σ₁) (Q : Package I M σ₂) (A : OracleComp E α) (s₁ : σ₁) (s₂ : σ₂) : (simulateQ (P.link Q).impl A).run (s₁, s₂) = VCVio.SSP.Package.linkReshape✝ <$> (simulateQ Q.impl ((simulateQ P.impl A).run s₁)).run s₂

Structural fact: running (P.link Q).impl is the same as nesting the simulations, threaded through both states. This is the unbundled form from which the SSP reduction lemma follows.

Statement: (simulateQ (P.link Q).impl A).run (s₁, s₂) = reshape <$> (simulateQ Q.impl ((simulateQ P.impl A).run s₁)).run s₂.

theorem VCVio.SSP.Package.run_link {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ σ₂ α : Type v} (P : Package M E σ₁) (Q : Package I M σ₂) (A : OracleComp E α) : (P.link Q).run A = Prod.fst <$> (simulateQ Q.impl ((simulateQ P.impl A).run P.init)).run' Q.init

The SSP reduction lemma in its program-equivalence form: linking the outer reduction package P to game Q and running against adversary A produces the same OracleComp output distribution as running Q against simulateQ P.impl A (the "outer-shifted" adversary).

This is the analogue of SSProve's swap_link_left / link_assoc-driven move that turns A ∘ (P ∘ Q) into (A ∘ P) ∘ Q at the level of distributions.

theorem VCVio.SSP.Package.run_link_left_ofStateless {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₂ α : Type v} (hP : QueryImpl E (OracleComp M)) (Q : Package I M σ₂) (A : OracleComp E α) : ((ofStateless hP).link Q).run A = Prod.fst <$> (simulateQ Q.impl (simulateQ hP A)).run Q.init

Specialization of run_link when only the outer (left) package is stateless. The PUnit factor on the outer side collapses, leaving only the inner package's state to thread.

This is the key reduction lemma for SSP-style proofs where the reduction package is stateless but the underlying game package carries non-trivial state (such as a lazily sampled secret key or a cached oracle output).

Not marked @[simp]: the data premise hP : QueryImpl E (OracleComp M) cannot be pattern- matched on, so a @[simp] tag here would loop with run_link. Use explicitly.

@[simp]

theorem VCVio.SSP.Package.run_link_ofStateless {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {α : Type v} (hP : QueryImpl E (OracleComp M)) (hQ : QueryImpl M (OracleComp I)) (A : OracleComp E α) : ((ofStateless hP).link (ofStateless hQ)).run A = simulateQ hQ (simulateQ hP A)

Specialization of run_link for two stateless packages. The link of two ofStateless packages reduces to nested simulateQ calls without any state to thread.

Parallel composition (par)

The two summed specs in par must share the import range universe and the export range universe (otherwise the disjoint sums I₁ + I₂ and E₁ + E₂ cannot share a single OracleSpec type). To keep par mostly universe polymorphic, we additionally collapse the import and export range universes to the same v; this matches the typing pattern induced by liftComp from OracleComp Iᵢ into OracleComp (I₁ + I₂). The index universes remain independent.

def VCVio.SSP.Package.par {σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} (p₁ : Package I₁ E₁ σ₁) (p₂ : Package I₂ E₂ σ₂) : Package (I₁ + I₂) (E₁ + E₂) (σ₁ × σ₂)

Parallel composition of two packages.

Given p₁ exporting E₁ and importing I₁, and p₂ exporting E₂ and importing I₂, the parallel composite exports the disjoint sum E₁ + E₂ and imports the disjoint sum I₁ + I₂. Each side's handler is lifted along the obvious OracleComp Iᵢ ⊂ₒ OracleComp (I₁ + I₂) and the resulting state is the product σ₁ × σ₂.

State separation is automatic: each side's handler can only access its own state component, so modifications to the other side are behaviorally invisible. This is the structural-typing counterpart of SSProve's fseparate side-condition.

We do not use QueryImpl.prodStateT here because of awkward universe unification through OracleSpec sums; the body is the same up to the obvious lifts.

@[simp]

theorem VCVio.SSP.Package.par_init {σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} (p₁ : Package I₁ E₁ σ₁) (p₂ : Package I₂ E₂ σ₂) : (p₁.par p₂).init = (p₁.init, p₂.init)

Universe-polymorphism sanity checks for link and par