Cryptographic Boolean Functions in Lean

1. Generalities on Boolean functions🔗

Chapter 2 develops scalar Boolean-function representations and the relation between Fourier and Walsh transforms. All page and result references in this chapter point to Claude Carlet's Boolean Functions for Cryptography and Error Correcting Codes. Write V_n=\mathbb F_2^n, f_\chi(x)=(-1)^{f(x)}, and \chi_a(x)=(-1)^{a\mathbin\cdot x} throughout.

Carlet's raw Walsh transform and the normalized Fourier coefficient satisfy W_f(a)=2^n\widetilde{f_\chi}(a).

The chapter includes Proposition 5's numerical-normal-form integrality criterion, Carlet's full raw Poisson summation formula, affine invariance, recovery from restrictions, and the spectral-support bounds. It also includes the coordinate formula relating univariate binary exponent weight to ANF degree, Proposition 3 on trace-monomial degree, and the representation of binary coordinates by the trace pairing.

  1. 1.1. Boolean functions and support
  2. 1.2. Algebraic normal form
  3. 1.3. Algebraic normal form existence and uniqueness
  4. 1.4. Algebraic degree, distance, and affine functions
  5. 1.5. Finite-field representations
  6. 1.6. Numerical normal form
  7. 1.7. Walsh transform
  8. 1.8. Fourier operations and subspaces
  9. 1.9. Walsh inversion and Parseval
  10. 1.10. Derivatives and autocorrelation
  11. 1.11. Fourier support