Programmable Oracles

This file defines combinators for programming an oracle: forcing chosen query points to return chosen pre-decided values, with a bookkeeping flag tracking whether the programming has been used (the canonical "bad event" of the identical-until-bad pattern).

Main definitions

• OracleSpec.ProgrammingPolicy spec — partial function t ↦ Option (programmed answer).
• OracleSpec.ProgrammingPolicy.empty — the all-none policy (no programming).
• QueryImpl.withRedirect so redirect — replace every query with a user-supplied callback.
• QueryImpl.withProgramming so policy — wrap so in StateT (QueryCache × Bool) so that policy hits override the underlying impl, set the bad flag, and are cached for consistency.

Design notes

The state of withProgramming is (QueryCache × Bool):

• The QueryCache ensures consistent answering: re-querying a programmed point returns the same value (so the adversary cannot detect programming via repeat queries).
• The Bool flag is set the first time the policy fires on an uncached query — i.e. when the programming would be observable relative to standard caching semantics. This is the canonical bad event for the identical-until-bad bound coming in a follow-up PR.

The flag is monotone (bad_monotone): once set, it stays set throughout execution. With the empty policy, the flag stays false and the impl is structurally an extendState-lift of withCaching (withProgramming_empty_run_proj_eq).

Auxiliary tracker

QueryImpl.withCachingTrackingPolicy so policy is withCaching so lifted to StateT (QueryCache × Bool) m, with the bad flag set on the same cache-miss-and-policy-fire condition as withProgramming but without actually programming: the oracle is queried normally and the (fresh) value is cached. Its purpose is to be the relational bridge between withCaching (cache-side projection) and withProgramming (the "identical-until-bad" partner of withProgramming); see OracleComp.ProgramLogic.Relational.ProgrammingOracle for the actual TV-distance bound (tvDist_simulateQ_withCaching_withProgramming_le_probEvent_bad) and its programming_collision_bound{,_qP_qH_β} repackagings.

def OracleSpec.ProgrammingPolicy {ι : Type u} (spec : OracleSpec ι) : Type (max u u_1)

A programming policy: a partial assignment of programmed answers to oracle inputs.

policy t = some v means "force the oracle to return v when queried at t". policy t = none means "leave the oracle unchanged at t".

@[implicit_reducible]

instance OracleSpec.ProgrammingPolicy.instInhabited {ι : Type u} {spec : OracleSpec ι} : Inhabited spec.ProgrammingPolicy

@[reducible]

def OracleSpec.ProgrammingPolicy.empty {ι : Type u} {spec : OracleSpec ι} : spec.ProgrammingPolicy

The empty programming policy: no point is programmed. Specializing withProgramming to this policy recovers withCaching (modulo the auxiliary Bool flag).

@[simp]

theorem OracleSpec.ProgrammingPolicy.empty_apply {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : empty t = none

Redirect

def QueryImpl.withRedirect {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} (_so : QueryImpl spec m) (redirect : (t : spec.Domain) → m (spec.Range t)) : QueryImpl spec m

Redirect every oracle query to a user-supplied callback. The base impl so is discarded on every query, and redirect t : m (spec.Range t) is consulted instead.

withRedirect so redirect = redirect definitionally; the named wrapper exists to expose intent at call sites and to compose with withProgramming (which uses withRedirect internally for the "programmed branch" of each query).

@[simp]

theorem QueryImpl.withRedirect_apply {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} (so : QueryImpl spec m) (redirect : (t : spec.Domain) → m (spec.Range t)) (t : spec.Domain) : so.withRedirect redirect t = redirect t

Programming

def QueryImpl.withProgramming {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) (policy : spec.ProgrammingPolicy) : QueryImpl spec (StateT (spec.QueryCache × Bool) m)

Wrap a query implementation so to honor a programming policy.

State: StateT (spec.QueryCache × Bool) m.

• The QueryCache is consulted first; cache hits return the cached value (consistent answers on repeated queries).
• On a cache miss:
  • policy t = some v → return v, cache it, set the bad flag.
  • policy t = none → fall through to so t, cache the result, leave the flag untouched.

Specialising to policy = ProgrammingPolicy.empty recovers withCaching lifted via extendState; see withProgramming_empty_run_proj_eq.

@[simp]

theorem QueryImpl.withProgramming_apply {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) (policy : spec.ProgrammingPolicy) (t : spec.Domain) : so.withProgramming policy t = StateT.mk fun (s : spec.QueryCache × Bool) => match s.1 t with | some v => pure (v, s) | none => (fun (p : spec.Range t × Bool) => (p.1, s.1.cacheQuery t p.1, p.2)) <$> match policy t with | some v => pure (v, true) | none => (fun (u : spec.Range t) => (u, s.2)) <$> so t

Bad-flag monotonicity

theorem QueryImpl.withProgramming_bad_monotone {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSet m] (so : QueryImpl spec m) (policy : spec.ProgrammingPolicy) (t : spec.Domain) (cache : spec.QueryCache) (z : spec.Range t × spec.QueryCache × Bool) (hz : z ∈ support ((so.withProgramming policy t).run (cache, true))) : z.2.2 = true

The bad flag of withProgramming is monotone: once set, every query keeps it set.

theorem QueryImpl.PreservesInv.withProgramming_bad {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀] (so : QueryImpl spec₀ ProbComp) (policy : spec₀.ProgrammingPolicy) : (so.withProgramming policy).PreservesInv fun (s : spec₀.QueryCache × Bool) => s.2 = true

PreservesInv packaging of withProgramming_bad_monotone for ProbComp.

Tracker partner of withProgramming

def QueryImpl.withCachingTrackingPolicy {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) (policy : spec.ProgrammingPolicy) : QueryImpl spec (StateT (spec.QueryCache × Bool) m)

withCaching lifted to StateT (QueryCache × Bool) m with the bad flag set on exactly the same cache-miss-and-policy-fire condition as withProgramming, but without actually programming: the underlying oracle is queried normally and the fresh value u is cached.

This is the "identical-until-bad" partner of withProgramming: at every step they either

• produce the same (value, cache, bad) distribution (cache hit, or cache miss with no policy hit), or
• both produce a step whose output flags bad := true, with possibly different value/cache components on the bad branch.

That is the exact shape needed to apply the output-bad version of "identical until bad".

@[simp]

theorem QueryImpl.withCachingTrackingPolicy_apply {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) (policy : spec.ProgrammingPolicy) (t : spec.Domain) : so.withCachingTrackingPolicy policy t = StateT.mk fun (s : spec.QueryCache × Bool) => match s.1 t with | some v => pure (v, s) | none => (fun (p : spec.Range t × Bool) => (p.1, s.1.cacheQuery t p.1, p.2)) <$> (fun (u : spec.Range t) => (u, if (policy t).isSome = true then true else s.2)) <$> so t

theorem QueryImpl.withCachingTrackingPolicy_bad_monotone {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSet m] (so : QueryImpl spec m) (policy : spec.ProgrammingPolicy) (t : spec.Domain) (cache : spec.QueryCache) (z : spec.Range t × spec.QueryCache × Bool) (hz : z ∈ support ((so.withCachingTrackingPolicy policy t).run (cache, true))) : z.2.2 = true

The bad flag of withCachingTrackingPolicy is monotone: once set, every query keeps it set.

theorem QueryImpl.PreservesInv.withCachingTrackingPolicy_bad {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀] (so : QueryImpl spec₀ ProbComp) (policy : spec₀.ProgrammingPolicy) : (so.withCachingTrackingPolicy policy).PreservesInv fun (s : spec₀.QueryCache × Bool) => s.2 = true

PreservesInv packaging of withCachingTrackingPolicy_bad_monotone for ProbComp.

withProgramming empty ≡ withCaching (cache-side projection)

theorem OracleComp.ProgramLogic.Relational.withProgramming_empty_run_proj_eq {α ι : Type} [DecidableEq ι] {spec : OracleSpec ι} (so : QueryImpl spec ProbComp) (oa : OracleComp spec α) (cache : spec.QueryCache) (bad : Bool) : Prod.map id Prod.fst <$> (simulateQ (so.withProgramming OracleSpec.ProgrammingPolicy.empty) oa).run (cache, bad) = (simulateQ so.withCaching oa).run cache

Cache-side projection: running withProgramming so empty and projecting away the bad flag gives the same distribution as running so.withCaching directly.

This is the "specializes to caching" sanity check for withProgramming, witnessing that the empty policy adds no observable behavior beyond withCaching plus a trivial bookkeeping flag.

theorem OracleComp.ProgramLogic.Relational.withProgramming_empty_run'_eq {α ι : Type} [DecidableEq ι] {spec : OracleSpec ι} (so : QueryImpl spec ProbComp) (oa : OracleComp spec α) (cache : spec.QueryCache) (bad : Bool) : (simulateQ (so.withProgramming OracleSpec.ProgrammingPolicy.empty) oa).run' (cache, bad) = (simulateQ so.withCaching oa).run' cache

run' projection corollary of withProgramming_empty_run_proj_eq.

withCachingTrackingPolicy ≡ withCaching (cache-side projection)

theorem OracleComp.ProgramLogic.Relational.withCachingTrackingPolicy_run_proj_eq' {α ι ι' : Type} [DecidableEq ι] {spec : OracleSpec ι} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) (policy : spec.ProgrammingPolicy) (oa : OracleComp spec α) (cache : spec.QueryCache) (bad : Bool) : Prod.map id Prod.fst <$> (simulateQ (so.withCachingTrackingPolicy policy) oa).run (cache, bad) = (simulateQ so.withCaching oa).run cache

Cache-side projection (general spec'): running so.withCachingTrackingPolicy policy and projecting away the bad flag gives the same distribution as running so.withCaching directly, irrespective of the initial bad value or the policy used to compute the (discarded) tracking.

theorem OracleComp.ProgramLogic.Relational.withCachingTrackingPolicy_run'_eq' {α ι ι' : Type} [DecidableEq ι] {spec : OracleSpec ι} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) (policy : spec.ProgrammingPolicy) (oa : OracleComp spec α) (cache : spec.QueryCache) (bad : Bool) : (simulateQ (so.withCachingTrackingPolicy policy) oa).run' (cache, bad) = (simulateQ so.withCaching oa).run' cache

run' projection corollary of withCachingTrackingPolicy_run_proj_eq'.

theorem OracleComp.ProgramLogic.Relational.withCachingTrackingPolicy_run_proj_eq {α ι : Type} [DecidableEq ι] {spec : OracleSpec ι} (so : QueryImpl spec ProbComp) (policy : spec.ProgrammingPolicy) (oa : OracleComp spec α) (cache : spec.QueryCache) (bad : Bool) : Prod.map id Prod.fst <$> (simulateQ (so.withCachingTrackingPolicy policy) oa).run (cache, bad) = (simulateQ so.withCaching oa).run cache

ProbComp specialization of withCachingTrackingPolicy_run_proj_eq'.

theorem OracleComp.ProgramLogic.Relational.withCachingTrackingPolicy_run'_eq {α ι : Type} [DecidableEq ι] {spec : OracleSpec ι} (so : QueryImpl spec ProbComp) (policy : spec.ProgrammingPolicy) (oa : OracleComp spec α) (cache : spec.QueryCache) (bad : Bool) : (simulateQ (so.withCachingTrackingPolicy policy) oa).run' (cache, bad) = (simulateQ so.withCaching oa).run' cache

ProbComp specialization of withCachingTrackingPolicy_run'_eq'.

Forward query bounds for withCachingTrackingPolicy

The bad-flag overlay projects away to withCaching (via withCachingTrackingPolicy_run_proj_eq') and makes no underlying queries, so the withCaching bounds transfer directly.

theorem OracleComp.ProgramLogic.Relational.isTotalQueryBound_run_simulateQ_withCachingTrackingPolicy {α ι ι' : Type} [DecidableEq ι] {spec : OracleSpec ι} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) (policy : spec.ProgrammingPolicy) {oa : OracleComp spec α} {n : ℕ} (h : oa.IsTotalQueryBound n) (hstep : ∀ (t : spec.Domain), (so t).IsTotalQueryBound 1) (cache : spec.QueryCache) (bad : Bool) : ((simulateQ (so.withCachingTrackingPolicy policy) oa).run (cache, bad)).IsTotalQueryBound n

theorem OracleComp.ProgramLogic.Relational.isQueryBoundP_run_simulateQ_withCachingTrackingPolicy {α ι ι' : Type} [DecidableEq ι] {spec : OracleSpec ι} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) (policy : spec.ProgrammingPolicy) {oa : OracleComp spec α} {p : ι → Prop} [DecidablePred p] {q : ι' → Prop} [DecidablePred q] {n : ℕ} (h : oa.IsQueryBoundP p n) (hstep_p : ∀ (t : ι), p t → (so t).IsQueryBoundP q 1) (hstep_np : ∀ (t : ι), ¬p t → (so t).IsQueryBoundP q 0) (cache : spec.QueryCache) (bad : Bool) : ((simulateQ (so.withCachingTrackingPolicy policy) oa).run (cache, bad)).IsQueryBoundP q n

theorem OracleComp.ProgramLogic.Relational.isPerIndexQueryBound_run_simulateQ_withCachingTrackingPolicy {α ι : Type} [DecidableEq ι] {spec : OracleSpec ι} (so : QueryImpl spec (OracleComp spec)) (policy : spec.ProgrammingPolicy) {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) (hstep : ∀ (t : spec.Domain), (so t).IsPerIndexQueryBound (Function.update 0 t 1)) (cache : spec.QueryCache) (bad : Bool) : ((simulateQ (so.withCachingTrackingPolicy policy) oa).run (cache, bad)).IsPerIndexQueryBound qb

Forward query bounds for withProgramming

A wrapped step makes ≤ 1 underlying query (zero on a cache hit or programmed value, one on a true miss). Unlike withCachingTrackingPolicy, the policy can short-circuit on cache miss, so the proof case-splits on cache × policy rather than reusing the withCaching projection.

theorem OracleComp.ProgramLogic.Relational.isTotalQueryBound_run_simulateQ_withProgramming {α ι ι' : Type} [DecidableEq ι] {spec : OracleSpec ι} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) (policy : spec.ProgrammingPolicy) {oa : OracleComp spec α} {n : ℕ} (h : oa.IsTotalQueryBound n) (hstep : ∀ (t : spec.Domain), (so t).IsTotalQueryBound 1) (cache : spec.QueryCache) (bad : Bool) : ((simulateQ (so.withProgramming policy) oa).run (cache, bad)).IsTotalQueryBound n

theorem OracleComp.ProgramLogic.Relational.isQueryBoundP_run_simulateQ_withProgramming {α ι ι' : Type} [DecidableEq ι] {spec : OracleSpec ι} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) (policy : spec.ProgrammingPolicy) {oa : OracleComp spec α} {p : ι → Prop} [DecidablePred p] {q : ι' → Prop} [DecidablePred q] {n : ℕ} (h : oa.IsQueryBoundP p n) (hstep_p : ∀ (t : ι), p t → (so t).IsQueryBoundP q 1) (hstep_np : ∀ (t : ι), ¬p t → (so t).IsQueryBoundP q 0) (cache : spec.QueryCache) (bad : Bool) : ((simulateQ (so.withProgramming policy) oa).run (cache, bad)).IsQueryBoundP q n

theorem OracleComp.ProgramLogic.Relational.isPerIndexQueryBound_run_simulateQ_withProgramming {α ι : Type} [DecidableEq ι] {spec : OracleSpec ι} (so : QueryImpl spec (OracleComp spec)) (policy : spec.ProgrammingPolicy) {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) (hstep : ∀ (t : spec.Domain), (so t).IsPerIndexQueryBound (Function.update 0 t 1)) (cache : spec.QueryCache) (bad : Bool) : ((simulateQ (so.withProgramming policy) oa).run (cache, bad)).IsPerIndexQueryBound qb