Code Representation #

Sample followed by pure with a function simplifies to uniform bind with pure. This is key for coupling proofs where we need the distribution over (result, heap).

source

theorem CatCrypt.Core.SPComp.sample_bind_pure_id (α : Type u_4) [Fintype α] [Nonempty α] (h : Heap) :

sample α h = (Prob.SDistr.uniform α).bind fun (a : α) => Prob.SDistr.pure (a, h)

Sample followed by pure of the sampled value simplifies to uniform bind. Special case where f is identity.

source

@[simp]

theorem CatCrypt.Core.SPComp.sample_prod_eq (A B : Type) [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] :

sample (A × B) = (sample A).bind fun (a : A) => (sample B).bind fun (b : B) => pure (a, b)

Sampling from a product type is equivalent to sampling each component independently.

Associativity and unit laws #

source

@[simp]

theorem CatCrypt.Core.SPComp.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : SPComp α) (f : α → SPComp β) (g : β → SPComp γ) :

(c.bind f).bind g = c.bind fun (a : α) => (f a).bind g

Bind associativity for SPComp

source

@[simp]

theorem CatCrypt.Core.SPComp.bind_pure {α : Type u_1} (c : SPComp α) :

c.bind pure = c

Right identity: bind with pure

source

@[simp]

theorem CatCrypt.Core.SPComp.pure_bind {α : Type u_1} {β : Type u_2} (a : α) (f : α → SPComp β) :

(pure a).bind f = f a

Left identity: pure then bind

source

@[simp]

theorem CatCrypt.Core.SPComp.bind_pure_left {α β : Type} (a : α) (f : α → SPComp β) :

pure a >>= f = f a

Bind.bind form of pure_bind. When a goal arrives with the typeclass-method Bind.bind (from Monad SPComp instance projection) rather than the prefix SPComp.bind, pure_bind's LHS pattern does not unify because the head symbols differ syntactically. This bridge lemma is a definitional rfl (the Monad instance defines bind := SPComp.bind) and is safe as @[simp]: confluent with pure_bind and monad_bind_eq.

source

@[simp]

theorem CatCrypt.Core.SPComp.hBind_pure_left {α β : Type} (a : α) (f : α → SPComp β) :

pure a >>= f = f a

HBind operator form (x >>= f) of pure_bind. Mirrors bind_pure_left for the bind operator. Safe as @[simp]: rfl-true and confluent.

Functorial map #

source

noncomputable def CatCrypt.Core.SPComp.map {α : Type u_1} {β : Type u_2} (f : α → β) (c : SPComp α) :

SPComp β

Functorial map for SPComp

Equations

CatCrypt.Core.SPComp.map f c = c.bind fun (a : α) => CatCrypt.Core.SPComp.pure (f a)

Instances For

source

@[simp]

theorem CatCrypt.Core.SPComp.map_id {α : Type u_1} (c : SPComp α) :

map id c = c

source

@[simp]

theorem CatCrypt.Core.SPComp.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) (c : SPComp α) :

map g (map f c) = map (g ∘ f) c

source

@[simp]

theorem CatCrypt.Core.SPComp.map_pure {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :

map f (pure a) = pure (f a)

Bijection on Uniform Sample #

source

theorem CatCrypt.Core.SPComp.sample_bind_pure_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (e : α ≃ β) (f : β → γ) :

((sample α).bind fun (a : α) => pure (f (e a))) = (sample β).bind fun (b : β) => pure (f b)

Applying a bijection inside a uniform sample doesn't change the distribution.

If e : α ≃ β is a bijection, then sampling a : α uniformly and returning f (e a) is the same as sampling b : β uniformly and returning f b. This lifts SDistr.uniform_bind_bij to SPComp.

source

theorem CatCrypt.Core.SPComp.sample_bind_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (e : α ≃ β) (k : β → SPComp γ) :

((sample α).bind fun (a : α) => k (e a)) = (sample β).bind k

Applying a bijection inside a uniform sample with arbitrary continuation.

Generalizes sample_bind_pure_equiv to non-pure continuations. If e : α ≃ β, then sample α >>= (k ∘ e) = sample β >>= k.

source

theorem CatCrypt.Core.SPComp.bind_sample_bijection {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (c : SPComp γ) (e : γ → α ≃ β) (k : γ → β → SPComp δ) :

(c.bind fun (x : γ) => (sample α).bind fun (a : α) => k x ((e x) a)) = c.bind fun (x : γ) => (sample β).bind fun (b : β) => k x b

Bijection cancellation in context: apply a context-dependent bijection inside bind c (fun x => sample >>= ...).

This handles the common ROM pattern where a key x determines a bijection e x : α ≃ β applied to a uniform sample.

Purity: Heap-Independent Computations #

source

def CatCrypt.Core.SPComp.IsPure {α : Type u_1} (c : SPComp α) :

Prop

A computation is pure if it doesn't depend on or modify the heap. Formally, there exists a sub-distribution d over values such that for every initial heap h, the computation returns (a, h) (unchanged heap) with probability d(a).

Equations

c.IsPure = ∃ (d : CatCrypt.Prob.SDistr α), ∀ (h : CatCrypt.Core.Heap), c h = d.bind fun (a : α) => CatCrypt.Prob.SDistr.pure (a, h)

Instances For

source

theorem CatCrypt.Core.SPComp.pure_isPure {α : Type u_1} (a : α) :

(pure a).IsPure

pure a is pure.

source

theorem CatCrypt.Core.SPComp.sample_isPure (α : Type u_4) [Fintype α] [Nonempty α] :

(sample α).IsPure

sample α is pure (doesn't touch the heap).

source

theorem CatCrypt.Core.SPComp.fail_isPure {α : Type u_1} :

fail.IsPure

fail is pure (doesn't touch the heap — it produces no results at all).

source

theorem CatCrypt.Core.SPComp.bind_isPure {α : Type u_1} {β : Type u_2} {c : SPComp α} {f : α → SPComp β} (hc : c.IsPure) (hf : ∀ (a : α), (f a).IsPure) :

(c.bind f).IsPure

Bind of pure computations is pure.

source

theorem CatCrypt.Core.SPComp.isPure_bind_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c₁ : SPComp α) (c₂ : SPComp β) (k : α → β → SPComp γ) (hc₁ : c₁.IsPure) (hc₂ : c₂.IsPure) :

(c₁.bind fun (a : α) => c₂.bind fun (b : β) => k a b) = c₂.bind fun (b : β) => c₁.bind fun (a : α) => k a b

Two pure computations commute in bind (Fubini for SPComp).

If c₁ and c₂ are both pure, then: c₁ >>= fun a => c₂ >>= fun b => k a b equals c₂ >>= fun b => c₁ >>= fun a => k a b

This is the key lemma for hybrid game decomposition in PKE security proofs.

source

theorem CatCrypt.Core.SPComp.isPure_bind_comm_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c₁ : SPComp α) (c₂ : SPComp β) (k : α → β → SPComp γ) (hc₁ : c₁.IsPure) :

(c₁.bind fun (a : α) => c₂.bind fun (b : β) => k a b) = c₂.bind fun (b : β) => c₁.bind fun (a : α) => k a b

One-sided commutativity: an IsPure computation can be commuted past ANY computation (not just another IsPure one).

This generalizes isPure_bind_comm by dropping the requirement that c₂ be IsPure. The proof uses SDistr.bind_comm (Fubini) at the distribution level, where c₁'s extracted distribution commutes with c₂ h for any heap h.