Bundled Lifts from ProbComp

This file packages the "public randomness" capability separately from denotational semantics.

Many crypto constructions need two orthogonal pieces of structure on their ambient monad m:

1. a way to observe computations probabilistically (SPMFSemantics / PMFSemantics)
2. a way to inject plain probabilistic sampling into m

This file packages the second capability as a bundled monad homomorphism ProbComp →ᵐ m, so it can be carried independently of whatever denotational semantics the construction uses. It also defines ProbCompRuntime, the common crypto-facing bundle that pairs public-randomness lifting with bundled SPMF semantics for an ambient monad.

structure ProbCompLift (m : Type → Type v) [Monad m] : Type (max 1 v)

Bundled way to lift plain probabilistic computations into an ambient monad m.

Intuitively, this is the capability "sample fresh public randomness inside m". We package it as a monad homomorphism so it composes lawfully with pure and bind.

• liftProbComp : ProbComp →ᵐ m

  Inject a plain ProbComp computation into m.

def ProbCompLift.ofMonadLift (m : Type → Type v) [Monad m] [MonadLiftT ProbComp m] [LawfulMonadLiftT ProbComp m] : ProbCompLift m

Build a bundled ProbCompLift from an existing lawful MonadLiftT ProbComp m instance.

def ProbCompLift.id : ProbCompLift ProbComp

The identity lift on ProbComp itself.

structure ProbCompRuntime (m : Type → Type v) [Monad m] : Type (max v (w + 1))

Common runtime bundle for crypto games in an ambient monad m.

This packages the two capabilities that security experiments usually need together:

1. SPMFSemantics m to observe the experiment as a Boolean subdistribution.
2. ProbCompLift m to sample fresh public randomness inside m.

The bundle is kept separate from the core scheme definitions so that executable scheme data does not become noncomputable merely by carrying denotational semantics.

• toSPMFSemantics : SPMFSemantics m

  Bundled subprobabilistic semantics for the ambient monad.

• toProbCompLift : ProbCompLift m

  Bundled injection of plain probabilistic sampling into the ambient monad.

def ProbCompRuntime.evalDist {m : Type → Type v} [Monad m] {α : Type} (runtime : ProbCompRuntime m) (mx : m α) : SPMF α

Observe an ambient computation as an SPMF using the runtime's bundled semantics.

def ProbCompRuntime.probFailure {m : Type → Type v} [Monad m] {α : Type} (runtime : ProbCompRuntime m) (mx : m α) : ENNReal

Failure probability of an ambient computation under the runtime's bundled semantics.

def ProbCompRuntime.liftProbComp {m : Type → Type v} [Monad m] (runtime : ProbCompRuntime m) : ProbComp →ᵐ m

Lift a plain ProbComp computation into the ambient monad using the runtime's public randomness capability.

noncomputable def ProbCompRuntime.probComp : ProbCompRuntime ProbComp

Canonical runtime for ProbComp itself.