Deterministic Code Predicate

This file provides the IsDeterministic predicate for RawCode, identifying computations that never use sample or fail.

Main definitions

• IsDeterministic - Predicate: code never uses sample or fail
• DetCode - Bundled deterministic code with proof

Motivation

CatCrypt code is defined in terms of RawCode, which supports probabilistic sampling. However, many extracted programs (from hax) are purely deterministic: they only use ret, bind, get, and put. This predicate identifies such programs, enabling reasoning about determinism in cryptographic proofs.

IsDeterministic Predicate

A RawCode computation is deterministic if it never uses sample or fail. This is an inductive predicate that closely mirrors the structure of ValidCode but without the location constraints and without the sample/fail cases.

inductive CatCrypt.Deep.IsDeterministic {α : Type u} : RawCode α → Prop

A computation is deterministic if it only uses ret, bind, get, and put. No probabilistic sampling or failure is allowed.

• ret {α : Type u} (a : α) : IsDeterministic (RawCode.ret a)
• bind {α β : Type u} (c : RawCode α) (k : α → RawCode β) (hc : IsDeterministic c) (hk : ∀ (a : α), IsDeterministic (k a)) : IsDeterministic (c.bind k)
• get (ℓ : Core.Location) : IsDeterministic (RawCode.get ℓ)
• put (ℓ : Core.Location) (v : ℓ.ty) : IsDeterministic (RawCode.put ℓ v)

Properties of IsDeterministic

theorem CatCrypt.Deep.IsDeterministic.not_fail {α : Type u} : ¬IsDeterministic RawCode.fail

Deterministic code never starts with fail.

theorem CatCrypt.Deep.IsDeterministic.not_sample {T : Type u} [Fintype T] [Nonempty T] : ¬IsDeterministic (RawCode.sample T)

Deterministic code never starts with sample.

theorem CatCrypt.Deep.IsDeterministic.not_oracleCall {op : ℕ} {dom codom : Type u} {x : dom} : ¬IsDeterministic (RawCode.oracleCall op dom codom x)

Deterministic code never starts with oracleCall.

theorem CatCrypt.Deep.IsDeterministic.not_embed {α : Type u} {c : Core.SPComp α} : ¬IsDeterministic (RawCode.embed c)

Deterministic code never starts with embed — an embedded SPComp may be probabilistic, so we conservatively rule it out of the deterministic fragment.

theorem CatCrypt.Deep.IsDeterministic.of_bind_left {α β : Type u} {c : RawCode α} {k : α → RawCode β} (h : IsDeterministic (c.bind k)) : IsDeterministic c

If bind c k is deterministic, then c is deterministic.

theorem CatCrypt.Deep.IsDeterministic.of_bind_right {α β : Type u} {c : RawCode α} {k : α → RawCode β} (h : IsDeterministic (c.bind k)) (a : α) : IsDeterministic (k a)

If bind c k is deterministic, then k a is deterministic for all a.

theorem CatCrypt.Deep.IsDeterministic.nonempty {α : Type u} {c : RawCode α} (h : IsDeterministic c) : Nonempty α

Deterministic code has a nonempty return type. This follows because every deterministic code form produces a value: ret a has a, get returns ULift ℓ.ty (inhabited), put returns ULift Unit, and bind inherits from its continuation.

Combinators for Deterministic Code

Helper combinators that maintain the IsDeterministic predicate.

structure CatCrypt.Deep.DetCode (α : Type u) : Type (u + 1)

A deterministic computation bundled with its proof.

• code : RawCode α
• isDet : IsDeterministic self.code

def CatCrypt.Deep.DetCode.ret {α : Type u} (a : α) : DetCode α

Pure return is deterministic.

Equations

• CatCrypt.Deep.DetCode.ret a = { code := CatCrypt.Deep.RawCode.ret a, isDet := ⋯ }

def CatCrypt.Deep.DetCode.bind {α β : Type u} (x : DetCode α) (f : α → DetCode β) : DetCode β

Bind preserves determinism.

Equations

• x.bind f = { code := x.code.bind fun (a : α) => (f a).code, isDet := ⋯ }

def CatCrypt.Deep.DetCode.get (ℓ : Core.Location) : DetCode (ULift.{u_1, 0} ℓ.ty)

Get is deterministic.

Equations

• CatCrypt.Deep.DetCode.get ℓ = { code := CatCrypt.Deep.RawCode.get ℓ, isDet := ⋯ }

def CatCrypt.Deep.DetCode.put (ℓ : Core.Location) (v : ℓ.ty) : DetCode (ULift.{u_1, 0} Unit)

Put is deterministic.

Equations

• CatCrypt.Deep.DetCode.put ℓ v = { code := CatCrypt.Deep.RawCode.put ℓ v, isDet := ⋯ }