Cryptographic Boolean Functions in Lean

1.7. Walsh transform🔗

Definition1.7.1
Group: Chapter 1: Generalities on Boolean functions (40)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 23
Reverse dependency previews
Preview
Theorem 1.7.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2pages-22-23fidelity-exact

Walsh transform (Carlet, pp. 22--23). Let f:V_n\to\mathbb F_2. The Walsh transform of f is the unnormalized Fourier transform of its sign function: W_f(a)=\sum_{x\in V_n}(-1)^{f(x)+a\mathbin\cdot x} =\sum_{x\in V_n}f_\chi(x)(-1)^{a\mathbin\cdot x} \qquad(a\in V_n).

Lean code for Definition1.7.1●5 declarations
  • defdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    def CryptBoolean.bitSignInt (b : FABL.𝔽₂) : ℤ
    def CryptBoolean.bitSignInt (b : FABL.𝔽₂) : ℤ
    The integer sign `(-1)^b` used in Carlet's raw Walsh sums.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.bitSignInt_add (a b : FABL.𝔽₂) :
  CryptBoolean.bitSignInt (a + b) =
    CryptBoolean.bitSignInt a * CryptBoolean.bitSignInt b
    theorem CryptBoolean.bitSignInt_add
  (a b : FABL.𝔽₂) :
  CryptBoolean.bitSignInt (a + b) =
    CryptBoolean.bitSignInt a *
      CryptBoolean.bitSignInt b
    The integer sign encoding sends binary addition to multiplication.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.bitSignInt_injective :
  Function.Injective CryptBoolean.bitSignInt
    theorem CryptBoolean.bitSignInt_injective :
  Function.Injective
    CryptBoolean.bitSignInt
    The integer sign encoding distinguishes the two binary values.
  • defdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    def CryptBoolean.walshTerm {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (a x : FABL.F₂Cube n) : ℤ
    def CryptBoolean.walshTerm {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a x : FABL.F₂Cube n) : ℤ
    The summand `(-1)^{f(x)+a·x}` in Carlet's Walsh transform.
  • defdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    def CryptBoolean.walshTransform {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) : ℤ
    def CryptBoolean.walshTransform {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) : ℤ
    Carlet's unnormalized integer Walsh transform.
Theorem1.7.2
Group: Chapter 1: Generalities on Boolean functions (40)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 1.9.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2walsh-normalizationfidelity-explicit-scaling-identity

Normalization of the Walsh transform. For f:V_n\to\mathbb F_2 and a\in V_n, let \widetilde{f_\chi}(a) =2^{-n}\sum_{x\in V_n}f_\chi(x)(-1)^{a\mathbin\cdot x}. Then, after embedding the integer W_f(a) in \mathbb R, W_f(a)=2^n\widetilde{f_\chi}(a).

Lean code for Theorem1.7.2●4 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.card_f₂Cube (n : ℕ) : Fintype.card (FABL.F₂Cube n) = 2 ^ n
    theorem CryptBoolean.card_f₂Cube (n : ℕ) :
  Fintype.card (FABL.F₂Cube n) = 2 ^ n
    The binary cube has cardinality `2^n`.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.walshTerm_cast_eq_realSignView_mul_character {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a x : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTerm f a x) =
    CryptBoolean.realSignView f x * (FABL.vectorWalshCharacter a) x
    theorem CryptBoolean.walshTerm_cast_eq_realSignView_mul_character
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a x : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTerm f a x) =
    CryptBoolean.realSignView f x *
      (FABL.vectorWalshCharacter a) x
    The real cast of a raw Walsh summand is the product of the encoded function and character.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.walshTransform_cast_eq_sum_realSignView_mul_character
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f a) =
    ∑ x, CryptBoolean.realSignView f x * (FABL.vectorWalshCharacter a) x
    theorem CryptBoolean.walshTransform_cast_eq_sum_realSignView_mul_character
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f a) =
    ∑ x,
      CryptBoolean.realSignView f x *
        (FABL.vectorWalshCharacter a) x
    Carlet's raw Walsh sum equals the unnormalized character-correlation sum.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.walshTransform_eq_two_pow_mul_vectorFourierCoeff {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f a) =
    2 ^ n * FABL.vectorFourierCoeff (CryptBoolean.realSignView f) a
    theorem CryptBoolean.walshTransform_eq_two_pow_mul_vectorFourierCoeff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f a) =
    2 ^ n *
      FABL.vectorFourierCoeff
        (CryptBoolean.realSignView f) a
    Carlet's raw Walsh transform is `2^n` times FABL's normalized Fourier coefficient.
Theorem1.7.3
Group: Chapter 1: Generalities on Boolean functions (40)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 17
Reverse dependency previews
Preview
Theorem 2.1.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2relation-13page-23fidelity-exact

Zero-frequency identity (Carlet, Relation (13), p. 23). For every f:V_n\to\mathbb F_2, W_f(0)=2^n-2w_H(f). Consequently, f\text{ is balanced} \quad\Longleftrightarrow\quad W_f(0)=0. When n>0, these conditions are also equivalent to w_H(f)=2^{n-1}.

Lean code for Theorem1.7.3●6 declarations
  • defdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    def CryptBoolean.IsBalanced {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  Prop
    def CryptBoolean.IsBalanced {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    A Boolean function is balanced when exactly half of the binary cube is in its support.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.bitSignInt_eq_if_one (b : FABL.𝔽₂) :
  CryptBoolean.bitSignInt b = if b = 1 then -1 else 1
    theorem CryptBoolean.bitSignInt_eq_if_one
  (b : FABL.𝔽₂) :
  CryptBoolean.bitSignInt b =
    if b = 1 then -1 else 1
    The integer sign encoding is `-1` at one and `1` at zero.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.walshTerm_zero {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  CryptBoolean.walshTerm f 0 x = CryptBoolean.bitSignInt (f x)
    theorem CryptBoolean.walshTerm_zero {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  CryptBoolean.walshTerm f 0 x =
    CryptBoolean.bitSignInt (f x)
    At zero frequency the Walsh summand is just the sign of the function value.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.walshTransform_zero_eq_card_sub_two_weight {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.walshTransform f 0 =
    ↑(Fintype.card (FABL.F₂Cube n)) -
      2 * ↑(CryptBoolean.hammingWeight f)
    theorem CryptBoolean.walshTransform_zero_eq_card_sub_two_weight
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.walshTransform f 0 =
    ↑(Fintype.card (FABL.F₂Cube n)) -
      2 * ↑(CryptBoolean.hammingWeight f)
    The zero-frequency Walsh value is support complement size minus support size.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.walshTransform_zero_eq_two_pow_sub_two_weight {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.walshTransform f 0 =
    2 ^ n - 2 * ↑(CryptBoolean.hammingWeight f)
    theorem CryptBoolean.walshTransform_zero_eq_two_pow_sub_two_weight
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.walshTransform f 0 =
    2 ^ n -
      2 * ↑(CryptBoolean.hammingWeight f)
    The zero-frequency Walsh value is `2^n - 2 wt(f)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.isBalanced_iff_walshTransform_zero_eq_zero {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBalanced f ↔ CryptBoolean.walshTransform f 0 = 0
    theorem CryptBoolean.isBalanced_iff_walshTransform_zero_eq_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBalanced f ↔
    CryptBoolean.walshTransform f 0 = 0
    A Boolean function is balanced exactly when the zero-frequency Walsh coefficient vanishes.