Cryptographic Boolean Functions in Lean

1.1. Boolean functions, support, and Walsh transform🔗

Definition1.1.1
uses 0
Used by 6
Reverse dependency previews
Preview
Definition 1.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2pages-8-22fidelity-exact

Boolean and sign functions (Carlet, pp. 8 and 22). Fix n\ge 0 and write V_n=\mathbb F_2^n. An n-variable Boolean function is a map f:V_n\to\mathbb F_2. Its sign function is f_\chi:V_n\longrightarrow\{-1,1\}\subset\mathbb R, \qquad f_\chi(x)=(-1)^{f(x)}.

Lean code for Definition1.1.1●2 definitions
  • abbrevdefined in CryptBoolean/Bridge/FABL.lean
    complete
    abbrev CryptBoolean.BooleanFunction (n : ℕ) : Type
    abbrev CryptBoolean.BooleanFunction (n : ℕ) :
  Type
    Scalar cryptographic Boolean functions on the additive binary cube.
  • abbrevdefined in CryptBoolean/Bridge/FABL.lean
    complete
    abbrev CryptBoolean.realSignView {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  FABL.F₂Cube n → ℝ
    abbrev CryptBoolean.realSignView {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  FABL.F₂Cube n → ℝ
    The real sign view `(-1)^{f(x)}` of a bit-valued Boolean function.
Definition1.1.2
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 1.1.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2page-8fidelity-exact-with-mathlib-hamming-norm

Support and Hamming weight (Carlet, p. 8). For f:V_n\to\mathbb F_2, define \operatorname{supp}(f)=\{x\in V_n:f(x)=1\}, \qquad w_H(f)=|\operatorname{supp}(f)|.

Lean code for Definition1.1.2●4 declarations
  • defdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    def CryptBoolean.support {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  Finset (FABL.F₂Cube n)
    def CryptBoolean.support {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Finset (FABL.F₂Cube n)
    The support of a Boolean function, as the finite set on which it is one.
  • abbrevdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    abbrev CryptBoolean.hammingWeight {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℕ
    abbrev CryptBoolean.hammingWeight {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℕ
    The Hamming weight of a Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.mem_support {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) : x ∈ CryptBoolean.support f ↔ f x = 1
    theorem CryptBoolean.mem_support {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  x ∈ CryptBoolean.support f ↔ f x = 1
    The support predicate is extensionally the one-set of the Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.hammingWeight_eq_card_support {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.hammingWeight f = (CryptBoolean.support f).card
    theorem CryptBoolean.hammingWeight_eq_card_support
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.hammingWeight f =
    (CryptBoolean.support f).card
    On binary-valued functions, Mathlib's Hamming norm is the cardinality of the one-set.

Formalization note. The source-facing weight name is a reducible alias of Mathlib's hammingNorm; the associated bridge proves that it is exactly the cardinality displayed above.

Definition1.1.3
uses 1
Used by 3
Reverse dependency previews
Preview
Theorem 1.1.4
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.1.3●3 definitions
  • 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.
  • 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.1.4
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 1.2.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2normalization-bridgefidelity-explicit-bridge

Walsh normalization bridge. 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.1.4●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.

Formalization note. The normalized coefficient \widetilde{f_\chi}(a) is FABL's vectorFourierCoeff. The explicit equation above is the only identification made between Carlet's raw transform and FABL's normalized transform.

Theorem1.1.5
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 1✓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.1.5●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.