State-Separating Proofs: Packages

A Package I E σ exposes an export oracle interface E while internally querying an import interface I, maintaining private state of type σ initialized to init. The handler impl runs a single export query inside StateT σ (OracleComp I).

This is the basic data type for the SSP layer. It corresponds to SSProve's package, but using VCVio's OracleSpec for interfaces, OracleComp as the underlying free monad, and a per-package functional StateT instead of a shared heap. Disjointness of state between two parallel packages is then a structural property of the product state σ₁ × σ₂.

The two basic operations live in this file:

• Package.id — identity package on E, with no internal state.
• Package.run — evaluate a closed package (with no imports) against an external "adversary" computation that queries the package's exports.

Composition of packages (sequential link and parallel par) and the bridge to probability distributions live in sibling files VCVio.SSP.Composition and VCVio.SSP.Advantage.

Universe layout

A Package I E σ lets the indices ιᵢ and ιₑ of the import / export specs live in independent universes (uᵢ, uₑ), and similarly the import / export ranges live in independent universes (vᵢ for I.Range, v for E.Range). The state σ and the result type α of any computation run against the package both live in Type v (i.e. the same universe as the export ranges); this constraint is forced by simulateQ operating on StateT σ (OracleComp I) (E.Range x). The import range universe vᵢ is unconstrained: an OracleComp I can produce values in Type v regardless of where I.Range lives.

structure VCVio.SSP.Package {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} (I : OracleSpec ιᵢ) (E : OracleSpec ιₑ) (σ : Type v) : Type (max (max (max uᵢ uₑ) v) vᵢ)

A package exposes the export interface E while internally querying the import interface I, maintaining a private state of type σ.

The handler impl interprets each export query as a stateful OracleComp I computation. The field init is the initial state.

Universe parameters: the index universes uᵢ, uₑ for the import and export specs are independent, as are the range universes vᵢ (for I) and v (for E). The state σ lives in the same universe v as the export ranges, since the handler must produce values of type StateT σ (OracleComp I) (E.Range x).

• init : σ

  Initial value of the package's private state.

• impl : QueryImpl E (StateT σ (OracleComp I))

  Implementation of each export query as a stateful OracleComp I computation.

def VCVio.SSP.Package.id {ιₑ : Type uₑ} (E : OracleSpec ιₑ) : Package E E PUnit.{v + 1}

The identity package on E: each export query is forwarded as the corresponding import query, with no private state.

Marked protected to prevent this name from shadowing _root_.id inside namespace Package; outside the namespace it is always written Package.id.

@[simp]

theorem VCVio.SSP.Package.id_init {ιₑ : Type uₑ} (E : OracleSpec ιₑ) : (Package.id E).init = PUnit.unit

@[simp]

theorem VCVio.SSP.Package.id_impl {ιₑ : Type uₑ} (E : OracleSpec ιₑ) (t : E.Domain) : (Package.id E).impl t = liftM (liftM (OracleQuery.query t))

def VCVio.SSP.Package.ofStateless {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} (h : QueryImpl E (OracleComp I)) : Package I E PUnit.{v + 1}

A purely stateless package built from a QueryImpl E (OracleComp I). The internal state is PUnit and the handler ignores it.

@[simp]

theorem VCVio.SSP.Package.ofStateless_impl {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} (h : QueryImpl E (OracleComp I)) (x : E.Domain) : (ofStateless h).impl x = QueryImpl.liftTarget (StateT PUnit.{v + 1} (OracleComp I)) h x

@[simp]

theorem VCVio.SSP.Package.ofStateless_init {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} (h : QueryImpl E (OracleComp I)) : (ofStateless h).init = PUnit.unit

def VCVio.SSP.Package.run {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α : Type v} (P : Package I E σ) (A : OracleComp E α) : OracleComp I α

Run a package against an "adversary" computation A that queries the package's exports.

The result is an OracleComp I computation in the package's import interface. Most commonly I is a sampling-only spec like unifSpec, in which case the result is a ProbComp (see VCVio.SSP.Advantage). The package's final state is discarded; use runState to keep it.

def VCVio.SSP.Package.runState {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α : Type v} (P : Package I E σ) (A : OracleComp E α) : OracleComp I (α × σ)

Variant of run that keeps the package's final state.

@[simp]

theorem VCVio.SSP.Package.runState_ofStateless {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {α : Type v} (h : QueryImpl E (OracleComp I)) (A : OracleComp E α) : (ofStateless h).runState A = (fun (x : α) => (x, PUnit.unit)) <$> simulateQ h A

@[simp]

theorem VCVio.SSP.Package.run_ofStateless {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {α : Type v} (h : QueryImpl E (OracleComp I)) (A : OracleComp E α) : (ofStateless h).run A = simulateQ h A

@[simp]

theorem VCVio.SSP.Package.run_pure {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α : Type v} (P : Package I E σ) (x : α) : P.run (pure x) = pure x

@[simp]

theorem VCVio.SSP.Package.runState_pure {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α : Type v} (P : Package I E σ) (x : α) : P.runState (pure x) = pure (x, P.init)

@[simp]

theorem VCVio.SSP.Package.runState_bind {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α β : Type v} (P : Package I E σ) (A : OracleComp E α) (f : α → OracleComp E β) : P.runState (A >>= f) = do let x ← P.runState A match x with | (a, s) => (simulateQ P.impl (f a)).run s

Universe-polymorphism sanity checks

The examples below exercise the four independent universe parameters of Package. They are purely typechecking tests: they ensure that the import / export index universes (uᵢ, uₑ) and the import / export range universes (vᵢ, v) all remain independent of each other.