5.8. On the number of bent functions🔗

Theorem5.8.1

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

Tagscarletchapter-6countingpage-97fidelity-exact

Number of Maiorana--McFarland functions (Carlet, p. 97). In dimension n=2m, the original Maiorana--McFarland class contains exactly (2^m)!\,2^{2^m} distinct bent functions.

Lean code for Theorem5.8.1●7 declarations

abbrevdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean

complete

abbrev CryptBoolean.MaioranaMcFarlandParameters (m : ℕ) : Type

abbrev CryptBoolean.MaioranaMcFarlandParameters
  (m : ℕ) : Type

The permutation and Boolean offset parameters of the original
Maiorana--McFarland construction.

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean

complete

def CryptBoolean.booleanMaioranaMcFarlandOfParameters {m : ℕ}
  (p : CryptBoolean.MaioranaMcFarlandParameters m) :
  CryptBoolean.BooleanFunction (m + m)

def CryptBoolean.booleanMaioranaMcFarlandOfParameters
  {m : ℕ}
  (p :
    CryptBoolean.MaioranaMcFarlandParameters
      m) :
  CryptBoolean.BooleanFunction (m + m)

The Boolean function determined by a Maiorana--McFarland parameter
pair.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.booleanMaioranaMcFarlandOfParameters_injective {m : ℕ} :
  Function.Injective CryptBoolean.booleanMaioranaMcFarlandOfParameters

theorem CryptBoolean.booleanMaioranaMcFarlandOfParameters_injective
  {m : ℕ} :
  Function.Injective
    CryptBoolean.booleanMaioranaMcFarlandOfParameters

The original Maiorana--McFarland parameterization is injective.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.card_maioranaMcFarlandParameters (m : ℕ) :
  Fintype.card (CryptBoolean.MaioranaMcFarlandParameters m) =
    (2 ^ m).factorial * 2 ^ 2 ^ m

theorem CryptBoolean.card_maioranaMcFarlandParameters
  (m : ℕ) :
  Fintype.card
      (CryptBoolean.MaioranaMcFarlandParameters
        m) =
    (2 ^ m).factorial * 2 ^ 2 ^ m

The original parameter space has
`(2^m)! * 2^(2^m)` elements.

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean

complete

def CryptBoolean.originalMaioranaMcFarlandClass (m : ℕ) :
  Finset (CryptBoolean.BooleanFunction (m + m))

def CryptBoolean.originalMaioranaMcFarlandClass
  (m : ℕ) :
  Finset
    (CryptBoolean.BooleanFunction (m + m))

The finite set of distinct functions in the original
Maiorana--McFarland class.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.card_originalMaioranaMcFarlandClass (m : ℕ) :
  (CryptBoolean.originalMaioranaMcFarlandClass m).card =
    (2 ^ m).factorial * 2 ^ 2 ^ m

theorem CryptBoolean.card_originalMaioranaMcFarlandClass
  (m : ℕ) :
  (CryptBoolean.originalMaioranaMcFarlandClass
        m).card =
    (2 ^ m).factorial * 2 ^ 2 ^ m

The original Maiorana--McFarland class contains exactly
`(2^m)! * 2^(2^m)` distinct functions.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.originalMaioranaMcFarlandClass_subset_bentFunctionFamily
  (m : ℕ) :
  CryptBoolean.originalMaioranaMcFarlandClass m ⊆
    CryptBoolean.bentFunctionFamily (m + m)

theorem CryptBoolean.originalMaioranaMcFarlandClass_subset_bentFunctionFamily
  (m : ℕ) :
  CryptBoolean.originalMaioranaMcFarlandClass
      m ⊆
    CryptBoolean.bentFunctionFamily
      (m + m)

The original Maiorana--McFarland class is a family of bent functions.

Theorem5.8.2

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Corollary 3.4.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-6countingpartial-spreadpage-97fidelity-exact-positive-half-dimension

Number of PS_{ap} functions (Carlet, p. 97). Let m\ge2. With field division defined at zero, the functions on \mathbb F_{2^m}\times\mathbb F_{2^m} of the form f_g(x,y)=g(x/y), where g:\mathbb F_{2^m}\to\mathbb F_2 is balanced, are distinct bent functions. Their number is \binom{2^m}{2^{m-1}}.

Lean code for Theorem5.8.2●8 declarations

abbrevdefined in CryptBoolean/Carlet/Chapter06/PSapCounting.lean

complete

abbrev CryptBoolean.PSapParameters (m : ℕ) : Type

abbrev CryptBoolean.PSapParameters (m : ℕ) : Type

The balanced Boolean parameters of the `PS_ap` construction.

theoremdefined in CryptBoolean/Carlet/Chapter06/PSapCounting.lean

complete

theorem CryptBoolean.card_psapParameters (m : ℕ) (hm : 0 < m) :
  Fintype.card (CryptBoolean.PSapParameters m) =
    (2 ^ m).choose (2 ^ (m - 1))

theorem CryptBoolean.card_psapParameters (m : ℕ)
  (hm : 0 < m) :
  Fintype.card
      (CryptBoolean.PSapParameters m) =
    (2 ^ m).choose (2 ^ (m - 1))

There are exactly `choose (2^m) (2^(m-1))` balanced Boolean parameters.

defdefined in CryptBoolean/Carlet/Chapter06/PSapCounting.lean

complete

def CryptBoolean.psapOfParameters {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (g : CryptBoolean.PSapParameters m) :
  CryptBoolean.FieldBooleanFunction (2 * m)

def CryptBoolean.psapOfParameters {m : ℕ}
  (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (g : CryptBoolean.PSapParameters m) :
  CryptBoolean.FieldBooleanFunction
    (2 * m)

The field-valued `PS_ap` function selected by a balanced Boolean
parameter and fixed quadratic-extension coordinates.

theoremdefined in CryptBoolean/Carlet/Chapter06/PSapCounting.lean

complete

theorem CryptBoolean.psapOfParameters_coordinate {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (g : CryptBoolean.PSapParameters m)
  (y' y : CryptBoolean.BinaryGaloisField m) :
  CryptBoolean.psapOfParameters hm iota omega homega theta g
      (iota y' + omega * iota y) =
    ↑g (theta.symm (y' / y))

theorem CryptBoolean.psapOfParameters_coordinate
  {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (g : CryptBoolean.PSapParameters m)
  (y' y :
    CryptBoolean.BinaryGaloisField m) :
  CryptBoolean.psapOfParameters hm iota
      omega homega theta g
      (iota y' + omega * iota y) =
    ↑g (theta.symm (y' / y))

Evaluation of a parametrized `PS_ap` function in quadratic-extension
coordinates.

theoremdefined in CryptBoolean/Carlet/Chapter06/PSapCounting.lean

complete

theorem CryptBoolean.psapOfParameters_injective {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m) :
  Function.Injective
    (CryptBoolean.psapOfParameters hm iota omega homega theta)

theorem CryptBoolean.psapOfParameters_injective
  {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m) :
  Function.Injective
    (CryptBoolean.psapOfParameters hm iota
      omega homega theta)

Distinct balanced parameters give distinct `PS_ap` functions.

defdefined in CryptBoolean/Carlet/Chapter06/PSapCounting.lean

complete

def CryptBoolean.psapClass {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m) :
  Finset (CryptBoolean.FieldBooleanFunction (2 * m))

def CryptBoolean.psapClass {m : ℕ}
  (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m) :
  Finset
    (CryptBoolean.FieldBooleanFunction
      (2 * m))

The finite `PS_ap` family in fixed quadratic-extension coordinates.

theoremdefined in CryptBoolean/Carlet/Chapter06/PSapCounting.lean

complete

theorem CryptBoolean.card_psapClass {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m) :
  (CryptBoolean.psapClass hm iota omega homega theta).card =
    (2 ^ m).choose (2 ^ (m - 1))

theorem CryptBoolean.card_psapClass {m : ℕ}
  (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m) :
  (CryptBoolean.psapClass hm iota omega
        homega theta).card =
    (2 ^ m).choose (2 ^ (m - 1))

Carlet's exact count for the `PS_ap` family.

theoremdefined in CryptBoolean/Carlet/Chapter06/PSapCounting.lean

complete

theorem CryptBoolean.isBent_psapOfParameters_comp_linearEquiv {m : ℕ}
  (hm : 2 ≤ m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (Theta :
    FABL.F₂Cube (2 * m) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (g : CryptBoolean.PSapParameters m) :
  CryptBoolean.IsBent
    (CryptBoolean.psapOfParameters ⋯ iota omega homega theta g ∘ ⇑Theta)

theorem CryptBoolean.isBent_psapOfParameters_comp_linearEquiv
  {m : ℕ} (hm : 2 ≤ m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (Theta :
    FABL.F₂Cube (2 * m) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (g : CryptBoolean.PSapParameters m) :
  CryptBoolean.IsBent
    (CryptBoolean.psapOfParameters ⋯ iota
        omega homega theta g ∘
      ⇑Theta)

Every balanced `PS_ap` parameter yields a bent function after any linear
choice of ambient binary coordinates.

Theorem5.8.3

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 2.1.6

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-6countingnaive-boundpage-97fidelity-exact

Naive upper bound for the number of bent functions (Carlet, p. 97). If n\ge4 is even, then the number B_n of bent functions on V_n satisfies B_n\le 2^{\sum_{i=0}^{n/2}\binom ni}.

Lean code for Theorem5.8.3●3 declarations

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean

complete

def CryptBoolean.bentFunctionFamily (n : ℕ) :
  Finset (CryptBoolean.BooleanFunction n)

def CryptBoolean.bentFunctionFamily (n : ℕ) :
  Finset (CryptBoolean.BooleanFunction n)

The finite family of all `n`-variable bent Boolean functions.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.mem_bentFunctionFamily_iff {n : ℕ}
  {f : CryptBoolean.BooleanFunction n} :
  f ∈ CryptBoolean.bentFunctionFamily n ↔ CryptBoolean.IsBent f

theorem CryptBoolean.mem_bentFunctionFamily_iff
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n} :
  f ∈ CryptBoolean.bentFunctionFamily n ↔
    CryptBoolean.IsBent f

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.card_bentFunctionFamily_le_naiveBound {n : ℕ}
  (_hnEven : Even n) (hn : 4 ≤ n) :
  (CryptBoolean.bentFunctionFamily n).card ≤
    2 ^ ∑ i ∈ Finset.range (n / 2 + 1), n.choose i

theorem CryptBoolean.card_bentFunctionFamily_le_naiveBound
  {n : ℕ} (_hnEven : Even n)
  (hn : 4 ≤ n) :
  (CryptBoolean.bentFunctionFamily
        n).card ≤
    2 ^
      ∑ i ∈ Finset.range (n / 2 + 1),
        n.choose i

Carlet's naive bound: in even dimension at least four, the number of
bent functions is at most the number of Boolean functions of degree at most
half the dimension.