Evaluation Semantics for ReaderT

This file provides monad homomorphisms for evaluating ReaderT ρ m computations by fixing the environment parameter.

Unlike StateT, ReaderT evaluation at a fixed environment is a valid monad homomorphism because the environment is read-only and doesn't change during computation.

Main definitions

• ReaderT.evalAt ρ0: Monad homomorphism ReaderT ρ m →ᵐ m by evaluation at ρ0
• HasEvalSPMF.readerAt ρ0: Lift HasEvalSPMF m through ReaderT at fixed ρ0
• HasEvalPMF.readerAt ρ0: Lift HasEvalPMF m through ReaderT at fixed ρ0

Design notes

We do NOT provide global HasEvalSPMF (ReaderT ρ m) instances because there's no canonical choice of environment. Instead, users explicitly provide the environment when constructing the evaluation homomorphism.

For cryptographic games with random oracles, the typical pattern is:

1. Generate oracle table with some distribution
2. Use readerAt to evaluate the protocol at that table
3. Compose with the table distribution to get overall game probability

def ReaderT.evalAt {ρ : Type u} {m : Type u → Type v} [Monad m] (ρ0 : ρ) : ReaderT ρ m →ᵐ m

Evaluate a ReaderT computation at a fixed environment ρ0. This is a monad homomorphism because ReaderT is read-only.

@[simp]

theorem ReaderT.evalAt_apply {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (ρ0 : ρ) (mx : ReaderT ρ m α) : (fun {α : Type u} (x : ReaderT ρ m α) => (evalAt ρ0).toFun α x) mx = mx ρ0

@[simp]

theorem ReaderT.evalAt_pure {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (ρ0 : ρ) (x : α) : (fun {α : Type u} (x : ReaderT ρ m α) => (evalAt ρ0).toFun α x) (pure x) = pure x

@[simp]

theorem ReaderT.evalAt_bind {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (ρ0 : ρ) (mx : ReaderT ρ m α) (f : α → ReaderT ρ m β) : (fun {α : Type u} (x : ReaderT ρ m α) => (evalAt ρ0).toFun α x) (mx >>= f) = do let x ← (fun {α : Type u} (x : ReaderT ρ m α) => (evalAt ρ0).toFun α x) mx (fun {α : Type u} (x : ReaderT ρ m α) => (evalAt ρ0).toFun α x) (f x)

noncomputable def HasEvalSPMF.readerAt {ρ : Type u} {m : Type u → Type v} [Monad m] (ρ0 : ρ) [HasEvalSPMF m] : ReaderT ρ m →ᵐ SPMF

Lift HasEvalSPMF m to a homomorphism ReaderT ρ m →ᵐ SPMF by fixing ρ0.

This allows evaluating reader computations to sub-probability distributions when the base monad m has such an evaluation.

noncomputable def HasEvalPMF.readerAt {ρ : Type u} {m : Type u → Type v} [Monad m] (ρ0 : ρ) [HasEvalPMF m] : ReaderT ρ m →ᵐ PMF

Lift HasEvalPMF m to a homomorphism ReaderT ρ m →ᵐ PMF by fixing ρ0.

This allows evaluating reader computations to probability distributions when the base monad m has such an evaluation.

@[simp]

theorem ReaderT.evalSPMF_pure {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (ρ0 : ρ) (x : α) : (fun {α : Type u} (x : ReaderT ρ m α) => (HasEvalSPMF.readerAt ρ0).toFun α x) (pure x) = (fun {α : Type u} (x : m α) => HasEvalSPMF.toSPMF.toFun α x) (pure x)

Evaluating pure x at any environment gives the same result as pure x in the base monad.

@[simp]

theorem ReaderT.evalSPMF_bind {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} [HasEvalSPMF m] (ρ0 : ρ) (mx : ReaderT ρ m α) (f : α → ReaderT ρ m β) : (fun {α : Type u} (x : ReaderT ρ m α) => (HasEvalSPMF.readerAt ρ0).toFun α x) (mx >>= f) = do let x ← (fun {α : Type u} (x : ReaderT ρ m α) => (HasEvalSPMF.readerAt ρ0).toFun α x) mx (fun {α : Type u} (x : ReaderT ρ m α) => (HasEvalSPMF.readerAt ρ0).toFun α x) (f x)

Evaluating a bind distributes through the monad homomorphism.

@[simp]

theorem ReaderT.evalPMF_pure {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalPMF m] (ρ0 : ρ) (x : α) : (fun {α : Type u} (x : ReaderT ρ m α) => (HasEvalPMF.readerAt ρ0).toFun α x) (pure x) = (fun {α : Type u} (x : m α) => HasEvalPMF.toPMF.toFun α x) (pure x)

@[simp]

theorem ReaderT.evalPMF_bind {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} [HasEvalPMF m] (ρ0 : ρ) (mx : ReaderT ρ m α) (f : α → ReaderT ρ m β) : (fun {α : Type u} (x : ReaderT ρ m α) => (HasEvalPMF.readerAt ρ0).toFun α x) (mx >>= f) = do let x ← (fun {α : Type u} (x : ReaderT ρ m α) => (HasEvalPMF.readerAt ρ0).toFun α x) mx (fun {α : Type u} (x : ReaderT ρ m α) => (HasEvalPMF.readerAt ρ0).toFun α x) (f x)

Optional: Instances with canonical environments

If you have a canonical choice of environment (e.g., via [Inhabited ρ]), you can uncomment these to get automatic HasEvalSPMF/PMF instances.

However, for most cryptographic use cases, it's better to keep the environment explicit and use the readerAt homomorphisms directly.

noncomputable instance [HasEvalSPMF m] [Inhabited ρ] :
    HasEvalSPMF (ReaderT ρ m) where
  toSPMF := HasEvalSPMF.readerAt (m := m) default

noncomputable instance [HasEvalPMF m] [Inhabited ρ] :
    HasEvalPMF (ReaderT ρ m) where
  toPMF := HasEvalPMF.readerAt (m := m) default