Observation Oracle for Side-Channel Leakage Modeling

This file defines an observation oracle that emits side-channel events during computation, enabling formal reasoning about leakage properties such as constant-time execution and distributional trace independence.

The API has two layers:

Layer 1 (generic, HasQuery-based): observation as a monad capability. Any monad m with HasQuery (ObsSpec Ev) m can emit observation events. Two canonical HasQuery instances are provided: obsDiscard (silently drops events) and obsAccumulate (accumulates events in a WriterT ω m layer).

Layer 2 (simulateQ-based): for reinterpreting concrete OracleComp (spec + ObsSpec Ev) α values. The definitions eraseObs and runObs are parameterized by a base oracle implementation base : QueryImpl spec m, so they work for any target monad, not just OracleComp spec.

Main Definitions

• ObsSpec Ev: oracle spec where each event type Ev maps to a PUnit response.
• observe: emit an observation event, generic over any [HasQuery (ObsSpec Ev) m].
• HasQuery.obsDiscard: HasQuery (ObsSpec Ev) m instance that discards events.
• HasQuery.obsAccumulate: HasQuery (ObsSpec Ev) (WriterT ω m) instance that accumulates.
• eraseObs: strip observation queries via simulateQ, parameterized by base implementation.
• runObs: execute observed computation with trace accumulation, parameterized by base.

Main Results

• fst_map_runObs: erasure theorem — projecting away the trace recovers eraseObs.
• probFailure_runObs: observations do not change failure probability ([HasEvalSPMF m]).
• NeverFail_runObs_iff: NeverFail is preserved by observation ([HasEvalSPMF m]).

Observation Spec

@[reducible, inline]

abbrev ObsSpec (Ev : Type u) : OracleSpec Ev

Oracle spec for observation events: each event maps to a PUnit response. Observation queries carry no computational payload and exist purely for side-channel instrumentation.

Layer 1: Generic HasQuery-Based Observation

def observe {Ev : Type u} {m : Type u → Type u_1} [HasQuery (ObsSpec Ev) m] (e : Ev) : m PUnit.{u + 1}

Emit an observation event into any monad with observation query capability.

@[reducible]

def HasQuery.obsDiscard {Ev : Type u} {m : Type u → Type u_1} [Monad m] : HasQuery (ObsSpec Ev) m

HasQuery instance that silently discards all observation events. Use this to erase observations without changing the computation's behavior.

@[reducible]

def HasQuery.obsAccumulate {Ev ω : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] (encode : Ev → ω) : HasQuery (ObsSpec Ev) (WriterT ω m)

HasQuery instance that accumulates observation events in a WriterT ω m layer. Each event e is encoded as encode e and accumulated via tell.

Layer 2: SimulateQ-Based Erasure and Trace Collection

def eraseObsImpl {ι : Type u} {spec : OracleSpec ι} {Ev : Type u} {m : Type u → Type u_1} [Monad m] (base : QueryImpl spec m) : QueryImpl (spec + ObsSpec Ev) m

Oracle implementation that handles spec + ObsSpec Ev by forwarding base queries to base and discarding observation events. Parameterized by the base implementation so it works for any target monad, not just OracleComp spec.

@[simp]

theorem eraseObsImpl_inl {ι : Type u} {spec : OracleSpec ι} {Ev : Type u} {m : Type u → Type u_1} [Monad m] (base : QueryImpl spec m) (t : ι) : eraseObsImpl base (Sum.inl t) = base t

@[simp]

theorem eraseObsImpl_inr {ι : Type u} {spec : OracleSpec ι} {Ev : Type u} {m : Type u → Type u_1} [Monad m] (base : QueryImpl spec m) (e : Ev) : eraseObsImpl base (Sum.inr e) = pure PUnit.unit

def eraseObs {ι : Type u} {spec : OracleSpec ι} {Ev α : Type u} {m : Type u → Type u_1} [Monad m] (base : QueryImpl spec m) (oa : OracleComp (spec + ObsSpec Ev) α) : m α

Strip observation queries from a computation, retaining only the base oracle queries. All observe calls become no-ops; the functional behavior of the computation is preserved.

@[simp]

theorem eraseObs_pure {ι : Type u} {spec : OracleSpec ι} {Ev α : Type u} {m : Type u → Type u_1} [Monad m] (base : QueryImpl spec m) (x : α) : eraseObs base (pure x) = pure x

@[simp]

theorem eraseObs_bind {ι : Type u} {spec : OracleSpec ι} {Ev α β : Type u} {m : Type u → Type u_1} [Monad m] [LawfulMonad m] (base : QueryImpl spec m) (oa : OracleComp (spec + ObsSpec Ev) α) (ob : α → OracleComp (spec + ObsSpec Ev) β) : eraseObs base (oa >>= ob) = do let x ← eraseObs base oa eraseObs base (ob x)

Running Observed Computations

def obsCostFn {ι : Type u} {spec : OracleSpec ι} {Ev ω : Type u} [Monoid ω] (encode : Ev → ω) : (spec + ObsSpec Ev).Domain → ω

Cost function for observation: base queries cost 1 (the monoid identity, so no trace contribution), observation events cost encode e.

def runObs {ι : Type u} {spec : OracleSpec ι} {Ev ω α : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] (base : QueryImpl spec m) (encode : Ev → ω) (oa : OracleComp (spec + ObsSpec Ev) α) : m (α × ω)

Execute an observed computation, producing the result paired with the accumulated observation trace. Parameterized by a base oracle implementation base : QueryImpl spec m, so this works for any target monad.

@[simp]

theorem runObs_pure {ι : Type u} {spec : OracleSpec ι} {Ev ω α : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] (base : QueryImpl spec m) (encode : Ev → ω) (x : α) : runObs base encode (pure x) = pure (x, 1)

theorem fst_map_runObs {ι : Type u} {spec : OracleSpec ι} {Ev ω α : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] (base : QueryImpl spec m) (encode : Ev → ω) (oa : OracleComp (spec + ObsSpec Ev) α) : (fun (z : α × ω) => z.1) <$> runObs base encode oa = eraseObs base oa

Erasure theorem: projecting away the observation trace recovers the erased computation.

theorem probFailure_runObs {ι : Type u} {spec : OracleSpec ι} {Ev ω α : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] [HasEvalSPMF m] (base : QueryImpl spec m) (encode : Ev → ω) (oa : OracleComp (spec + ObsSpec Ev) α) : Pr[⊥ | runObs base encode oa] = Pr[⊥ | eraseObs base oa]

Failure preservation: observations do not change the probability of failure.

theorem NeverFail_runObs_iff {ι : Type u} {spec : OracleSpec ι} {Ev ω α : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] [HasEvalSPMF m] (base : QueryImpl spec m) (encode : Ev → ω) (oa : OracleComp (spec + ObsSpec Ev) α) : NeverFail (runObs base encode oa) ↔ NeverFail (eraseObs base oa)

NeverFail is preserved by observation.

EvalDist Bridge for runObs

These lemmas connect the result-marginal distribution of runObs to the distribution of eraseObs, enabling direct probability-level reasoning about traces without needing to manually simplify the traced computation into its concrete form.

theorem evalDist_fst_runObs {ι : Type u} {spec : OracleSpec ι} {Ev ω α : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] [HasEvalSPMF m] (base : QueryImpl spec m) (encode : Ev → ω) (oa : OracleComp (spec + ObsSpec Ev) α) : evalDist ((fun (z : α × ω) => z.1) <$> runObs base encode oa) = evalDist (eraseObs base oa)

theorem probOutput_fst_runObs {ι : Type u} {spec : OracleSpec ι} {Ev ω α : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] [HasEvalSPMF m] (base : QueryImpl spec m) (encode : Ev → ω) (oa : OracleComp (spec + ObsSpec Ev) α) (x : α) : Pr[= x | (fun (z : α × ω) => z.1) <$> runObs base encode oa] = Pr[= x | eraseObs base oa]

theorem support_fst_runObs {ι : Type u} {spec : OracleSpec ι} {Ev ω α : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] [HasEvalSPMF m] (base : QueryImpl spec m) (encode : Ev → ω) (oa : OracleComp (spec + ObsSpec Ev) α) : support ((fun (z : α × ω) => z.1) <$> runObs base encode oa) = support (eraseObs base oa)

Structural Lemmas for runObs

@[simp]

theorem runObs_bind {ι : Type u} {spec : OracleSpec ι} {Ev ω α β : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] (base : QueryImpl spec m) (encode : Ev → ω) (oa : OracleComp (spec + ObsSpec Ev) α) (ob : α → OracleComp (spec + ObsSpec Ev) β) : runObs base encode (oa >>= ob) = do let __discr ← runObs base encode oa match __discr with | (a, w₁) => do let __discr ← runObs base encode (ob a) match __discr with | (b, w₂) => pure (b, w₁ * w₂)

@[simp]

theorem runObs_map {ι : Type u} {spec : OracleSpec ι} {Ev ω α β : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] (base : QueryImpl spec m) (encode : Ev → ω) (oa : OracleComp (spec + ObsSpec Ev) α) (f : α → β) : runObs base encode (f <$> oa) = Prod.map f id <$> runObs base encode oa

@[simp]

theorem runObs_liftM_query_inl {ι : Type u} {spec : OracleSpec ι} {Ev ω : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] (base : QueryImpl spec m) (encode : Ev → ω) (t : spec.Domain) : runObs base encode (liftM (OracleQuery.query t)) = (fun (x : spec.Range t) => (x, 1)) <$> base t

runObs on a single base-spec query lifted into spec + ObsSpec Ev: the trace is 1.

@[simp]

theorem runObs_liftComp {ι : Type u} {spec : OracleSpec ι} {Ev ω α : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] (base : QueryImpl spec m) (encode : Ev → ω) (oa : OracleComp spec α) : runObs base encode (liftM oa) = (fun (x : α) => (x, 1)) <$> simulateQ base oa

runObs on a lifted base-spec computation: the trace is 1 (monoid identity).

@[simp]

theorem runObs_observe {ι : Type u} {spec : OracleSpec ι} {Ev ω : Type u} {m : Type u → Type u_1} [Monad m] [Monoid ω] [LawfulMonad m] (base : QueryImpl spec m) (encode : Ev → ω) (e : Ev) : runObs base encode (observe e) = pure (PUnit.unit, encode e)

runObs on observe e: the result is PUnit.unit with trace encode e.