CryptoWord Typeclass

Abstract interface for word types used in cryptographic constructions.

Overview

Currently Word = Bool is hardcoded in PRFPRG.lean. This typeclass provides an abstract interface so new constructions (like CBC mode) can be written generically while existing Bool-specific proofs remain untouched.

Main definitions

• SampleableType — base typeclass: Fintype + Nonempty + DecidableEq + Inhabited
• CryptoWord — extends SampleableType with involutive XOR (wxor)
• wxorEquiv — bijection from wxor_cancel
• rHoare_sample_wxor — coupling lemma for wxor

Main results

• advantage_zero_of_wxor — zero advantage for wxor-based games
• SampleableType Bool / CryptoWord Bool instances
• SampleableType (BitVec n) / CryptoWord (BitVec n) instances

Typeclass Hierarchy

class CatCrypt.Crypto.SampleableType (W : Type) : Type

Base class for types that can be uniformly sampled in CatCrypt games. Requires Fintype (for uniform distribution), Nonempty (distribution is well-defined), DecidableEq (for equality checks in games), and Inhabited (for default values in extraction bridges).

• fintype : Fintype W
• nonempty : Nonempty W
• deceq : DecidableEq W
• inhabited : Inhabited W

class CatCrypt.Crypto.CryptoWord (W : Type) extends CatCrypt.Crypto.SampleableType W : Type

Abstract word type for cryptographic constructions. Extends SampleableType with an involutive XOR operation, needed for one-time-pad style proofs (symmetric ratchet, PSK injection, etc.).

• fintype : Fintype W
• nonempty : Nonempty W
• deceq : DecidableEq W
• inhabited : Inhabited W
• wxor : W → W → W

  The XOR-like operation

• wxor_cancel (a b : W) : wxor (wxor a b) b = a

  wxor is involutive: wxor (wxor a b) b = a

• wxor_comm (a b : W) : wxor a b = wxor b a

  wxor is commutative

Bool Instances

@[implicit_reducible]

instance CatCrypt.Crypto.instSampleableTypeBool : SampleableType Bool

Equations

• CatCrypt.Crypto.instSampleableTypeBool = { fintype := Bool.fintype, nonempty := ⋯, deceq := instDecidableEqBool, inhabited := instInhabitedBool }

@[implicit_reducible]

instance CatCrypt.Crypto.instCryptoWordBool : CryptoWord Bool

Equations

• One or more equations did not get rendered due to their size.

theorem CatCrypt.Crypto.boolCryptoWord_wxor_eq_xor : CryptoWord.wxor = xor

For Bool, wxor is definitionally xor.

BitVec Instance

@[irreducible]

noncomputable instance CatCrypt.Crypto.instFintypeBitVec (n : ℕ) : Fintype (BitVec n)

Fintype instance for BitVec n via the bijection with Fin (2^n). Marked @[irreducible] to prevent kernel reduction of 2^n for large n (e.g., BitVec 256). The instance is still found by typeclass search.

Equations

• CatCrypt.Crypto.instFintypeBitVec n = Fintype.ofEquiv (Fin (2 ^ n)) { toFun := BitVec.ofFin, invFun := BitVec.toFin, left_inv := ⋯, right_inv := ⋯ }

@[irreducible]

noncomputable instance CatCrypt.Crypto.instSampleableTypeBitVec (n : ℕ) : SampleableType (BitVec n)

BitVec n is sampleable (finite, nonempty, decidable equality, inhabited).

Equations

• CatCrypt.Crypto.instSampleableTypeBitVec n = { fintype := CatCrypt.Crypto.instFintypeBitVec n, nonempty := ⋯, deceq := instDecidableEqBitVec, inhabited := BitVec.instInhabited }

@[irreducible]

noncomputable instance CatCrypt.Crypto.instCryptoWordBitVec (n : ℕ) : CryptoWord (BitVec n)

BitVec n forms a CryptoWord with wxor = XOR. This enables all CatCrypt security proofs to work at any bit width, including the concrete BitVec 256 level matching P-256 / SHA-256. Marked @[irreducible] to prevent kernel reduction for large n.

Equations

• CatCrypt.Crypto.instCryptoWordBitVec n = { toSampleableType := CatCrypt.Crypto.instSampleableTypeBitVec n, wxor := fun (a b : BitVec n) => a ^^^ b, wxor_cancel := ⋯, wxor_comm := ⋯ }

Derived Properties

theorem CatCrypt.Crypto.CryptoWord.wxor_left_cancel {W : Type} [CryptoWord W] (a b : W) : wxor a (wxor a b) = b

Left cancellation: wxor a (wxor a b) = b. Follows from wxor_cancel and wxor_comm.

XOR Equivalence (Bijection)

def CatCrypt.Crypto.wxorEquiv {W : Type} [CryptoWord W] (x : W) : W ≃ W

wxor with a fixed value is an equivalence (bijection). This is the CryptoWord analogue of boolXorBij from XorBij.lean.

Equations

• CatCrypt.Crypto.wxorEquiv x = { toFun := fun (k : W) => CatCrypt.Crypto.CryptoWord.wxor k x, invFun := fun (r : W) => CatCrypt.Crypto.CryptoWord.wxor r x, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CatCrypt.Crypto.wxorEquiv_apply {W : Type} [CryptoWord W] (x k : W) : (wxorEquiv x) k = CryptoWord.wxor k x

Coupling Lemma

theorem CatCrypt.Crypto.rHoare_sample_wxor {W : Type} [CryptoWord W] (m : W) : Relational.rHoare Relational.eqPre (do let k ← Core.SPComp.sample W Core.SPComp.pure (CryptoWord.wxor k m)) (Core.SPComp.sample W) Relational.eqPost

Sampling a key and applying wxor has the same distribution as sampling directly. CryptoWord analogue of rHoare_sample_xor.

Zero Advantage

theorem CatCrypt.Crypto.advantage_zero_of_wxor {W : Type} [CryptoWord W] (m : W) (A : W → Core.SPComp Bool) : AdvantageA (do let k ← Core.SPComp.sample W Core.SPComp.pure (CryptoWord.wxor k m)) (Core.SPComp.sample W) A = 0

Zero advantage for wxor-based games. CryptoWord analogue of advantage_zero_of_xor.