Cryptographic Boolean Functions in Lean

5.9. Characterization through the NNF🔗

Proposition5.9.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.
Statement uses 4
Statement dependency previews
Preview
Theorem 1.6.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6proposition-23numerical-normal-formsection-6-6-1page-98fidelity-exact

Proposition 23 (Carlet, p. 98). Let n\ge2 be even, and let f:V_n\to\mathbb F_2 have numerical normal form f(x)=\sum_{I\subseteq[n]}\lambda_Ix^I. Then f is bent if and only if both of the following conditions hold:

  1. for every I\subseteq[n] with n/2<|I|<n, 2^{|I|-n/2}\mid\lambda_I;

  2. for N=[n], \lambda_N\equiv2^{n/2-1}\pmod {2^{n/2}}.

Lean code for Proposition5.9.1●6 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/NNFCharacterization.lean
    complete
    def CryptBoolean.booleanNNFFourierCoeffInt {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (u : FABL.F₂Cube n) : ℤ
    def CryptBoolean.booleanNNFFourierCoeffInt
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube n) : ℤ
    The integral Fourier coefficient obtained from the integral numerical
normal form by Carlet Relation (30).
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NNFCharacterization.lean
    complete
    theorem CryptBoolean.booleanNNFFourierCoeffInt_cast {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (u : FABL.F₂Cube n) :
  ↑(CryptBoolean.booleanNNFFourierCoeffInt f u) =
    CryptBoolean.rawFourierTransform (FABL.booleanRealEmbedding f) u
    theorem CryptBoolean.booleanNNFFourierCoeffInt_cast
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube n) :
  ↑(CryptBoolean.booleanNNFFourierCoeffInt
        f u) =
    CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding f) u
    The integral NNF Fourier coefficient is the raw Fourier transform of the
zero-one embedding.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NNFCharacterization.lean
    complete
    theorem CryptBoolean.walshTransform_eq_indicator_sub_two_mul_booleanNNFFourierCoeffInt
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f u =
    (if u = 0 then 2 ^ n else 0) -
      2 * CryptBoolean.booleanNNFFourierCoeffInt f u
    theorem CryptBoolean.walshTransform_eq_indicator_sub_two_mul_booleanNNFFourierCoeffInt
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f u =
    (if u = 0 then 2 ^ n else 0) -
      2 *
        CryptBoolean.booleanNNFFourierCoeffInt
          f u
    The Walsh transform is the constant Fourier coefficient minus twice the
integral zero-one Fourier coefficient.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NNFCharacterization.lean
    complete
    theorem CryptBoolean.isBent_iff_forall_booleanNNFFourierCoeffInt_modeq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : Even n) (hnTwo : 2 ≤ n) :
  CryptBoolean.IsBent f ↔
    ∀ (u : FABL.F₂Cube n),
      CryptBoolean.booleanNNFFourierCoeffInt f u ≡ 2 ^ (n / 2 - 1) [ZMOD
        2 ^ (n / 2)]
    theorem CryptBoolean.isBent_iff_forall_booleanNNFFourierCoeffInt_modeq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Even n) (hnTwo : 2 ≤ n) :
  CryptBoolean.IsBent f ↔
    ∀ (u : FABL.F₂Cube n),
      CryptBoolean.booleanNNFFourierCoeffInt
          f u ≡
        2 ^ (n / 2 - 1) [ZMOD 2 ^ (n / 2)]
    Carlet Lemma 2 in the equivalent zero-one Fourier normalization.
  • defdefined in CryptBoolean/Carlet/Chapter06/NNFCharacterization.lean
    complete
    def CryptBoolean.SatisfiesBentNNFCoefficientConditions {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.SatisfiesBentNNFCoefficientConditions
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    The two divisibility conditions of Carlet Proposition 23.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NNFCharacterization.lean
    complete
    theorem CryptBoolean.isBent_iff_nnfCoefficientConditions {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : Even n) (hnTwo : 2 ≤ n) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.SatisfiesBentNNFCoefficientConditions f
    theorem CryptBoolean.isBent_iff_nnfCoefficientConditions
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Even n) (hnTwo : 2 ≤ n) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.SatisfiesBentNNFCoefficientConditions
      f
    Carlet Proposition 23: in even dimension at least two, a Boolean function
is bent exactly when its integral numerical normal form satisfies the stated
intermediate divisibility conditions and top-coefficient congruence.