4.1. Affine functions
Affine Walsh spectrum (Carlet, Section 5.1, p. 68). Let n\ge0, let
a,u\in V_n, and let \epsilon\in\mathbb F_2. For
\ell(x)=a\mathbin\cdot x+\epsilon,
the unnormalized Walsh transform satisfies
W_\ell(u)=
\begin{cases}
2^n(-1)^\epsilon,&u=a,\\
0,&u\ne a.
\end{cases}
Lean code for Theorem4.1.1●1 theorem
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter05/Affine.leancomplete
theorem CryptBoolean.walshTransform_affineFunction {n : ℕ} (b : FABL.𝔽₂) (a u : FABL.F₂Cube n) : CryptBoolean.walshTransform (FABL.affineFunction b a) u = if u = a then CryptBoolean.bitSignInt b * 2 ^ n else 0
theorem CryptBoolean.walshTransform_affineFunction {n : ℕ} (b : FABL.𝔽₂) (a u : FABL.F₂Cube n) : CryptBoolean.walshTransform (FABL.affineFunction b a) u = if u = a then CryptBoolean.bitSignInt b * 2 ^ n else 0
The raw Walsh transform of an affine Boolean function is supported at its linear part.
Maiorana--McFarland functions (Carlet, Section 5.1, p. 68).
Fix a decomposition V_{r+s}=V_r\times V_s. A Boolean function
f:V_r\times V_s\to\mathbb F_2 is a Maiorana--McFarland function when,
for every y\in V_s, the function
x\mapsto f(x,y) is affine. Equivalently, the truth table of f is the
concatenation, indexed by y, of affine truth tables on V_r.
Lean code for Definition4.1.2●1 definition
Associated Lean declarations
-
CryptBoolean.IsMaioranaMcFarland[complete]
-
CryptBoolean.IsMaioranaMcFarland[complete]
-
defdefined in CryptBoolean/Carlet/Chapter05/Affine.leancomplete
def CryptBoolean.IsMaioranaMcFarland {r s : ℕ} (f : CryptBoolean.BooleanFunction (r + s)) : Prop
def CryptBoolean.IsMaioranaMcFarland {r s : ℕ} (f : CryptBoolean.BooleanFunction (r + s)) : Prop
Carlet's Chapter 5 Maiorana--McFarland functions: each restriction to the first block is affine.
Carlet uses this Chapter 5 name for concatenations of affine restrictions. Section 6.4 later specializes the construction to a class of bent functions.