Cryptographic Boolean Functions in Lean🔗

CryptBoolean is a formalization of cryptographic Boolean-function theory in Lean 4 and Mathlib. Its primary mathematical source is Claude Carlet's Boolean Functions for Cryptography and Error-Correcting Codes (Carlet, 2010).

The library develops algebraic representations, Walsh analysis, finite-field representations, Reed--Muller coding, and cryptographic criteria for scalar Boolean functions. Carlet's raw Walsh transform and the normalized Fourier coefficient are related throughout by the identity W_f(a)=2^n\widetilde{f_\chi}(a).

The nine chapters develop, in order, representations and the Fourier--Walsh relation, Reed--Muller coding, scalar cryptographic criteria, classes with constrained weights, Walsh spectra, and nonlinearities, bent functions, resilient functions, strict avalanche and propagation criteria, algebraic immune functions, and symmetric and rotation-symmetric functions.

The exposition begins with Carlet's Chapter 2. Thus Chapters 1--9 below correspond respectively to Carlet Chapters 2--10; source references retain Carlet's numbering.

Each entry states the mathematics with explicit domains, hypotheses, quantifiers, and conclusions. The graph below records the mathematical dependencies among these results.