Cryptographic Boolean Functions in Lean

1.4. Derivatives and autocorrelation🔗

Definition1.4.1
uses 1used by 1✓L∃∀N
Tagscarletchapter-2definition-2page-27fidelity-exact

Definition 2 (Carlet, p. 27). Let f:V_n\to\mathbb F_2 and b\in V_n. The derivative of f in direction b is the Boolean function D_bf(x)=f(x)+f(x+b) \qquad(x\in V_n), where addition is in \mathbb F_2. Its sign function satisfies (D_bf)_\chi(x)=f_\chi(x)f_\chi(x+b).

Lean code for Definition1.4.1●2 declarations
  • defdefined in CryptBoolean/Carlet/Chapter02/Derivatives.lean
    complete
    def CryptBoolean.booleanDerivative {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.booleanDerivative {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction n
    Carlet Definition 2: the binary derivative in direction `b`.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Derivatives.lean
    complete
    theorem CryptBoolean.realSignView_booleanDerivative {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b x : FABL.F₂Cube n) :
  CryptBoolean.realSignView (CryptBoolean.booleanDerivative f b) x =
    CryptBoolean.realSignView f x * CryptBoolean.realSignView f (x + b)
    theorem CryptBoolean.realSignView_booleanDerivative
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b x : FABL.F₂Cube n) :
  CryptBoolean.realSignView
      (CryptBoolean.booleanDerivative f b)
      x =
    CryptBoolean.realSignView f x *
      CryptBoolean.realSignView f (x + b)
    The derivative sign is the product of the two translated function signs.
Definition1.4.2
Statement uses 2
Statement dependency previews
Preview
Definition 1.3.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-2relation-24page-27fidelity-exact

Autocorrelation (Carlet, Relations (24)--(25), p. 27). For f:V_n\to\mathbb F_2, define \Delta_f(b) =\sum_{x\in V_n}(-1)^{D_bf(x)} =\sum_{x\in V_n}f_\chi(x)f_\chi(x+b) =(f_\chi\otimes f_\chi)(b).

Lean code for Definition1.4.2●2 declarations
  • defdefined in CryptBoolean/Carlet/Chapter02/Derivatives.lean
    complete
    def CryptBoolean.autocorrelation {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) : ℝ
    def CryptBoolean.autocorrelation {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.F₂Cube n) : ℝ
    Carlet's autocorrelation value `Δ_f(b) = ∑ₓ (-1)^(D_b f(x))`.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Derivatives.lean
    complete
    theorem CryptBoolean.autocorrelation_eq_rawConvolution_realSignView {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) :
  CryptBoolean.autocorrelation f b =
    CryptBoolean.rawConvolution (CryptBoolean.realSignView f)
      (CryptBoolean.realSignView f) b
    theorem CryptBoolean.autocorrelation_eq_rawConvolution_realSignView
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.F₂Cube n) :
  CryptBoolean.autocorrelation f b =
    CryptBoolean.rawConvolution
      (CryptBoolean.realSignView f)
      (CryptBoolean.realSignView f) b
    Autocorrelation is the raw self-convolution of the sign view.
Theorem1.4.3
Statement uses 3
Statement dependency previews
Preview
Definition 1.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-2relation-25page-27fidelity-exact

Wiener--Khinchin identity (Carlet, Relation (25), p. 27). For every f:V_n\to\mathbb F_2 and u\in V_n, \widehat{\Delta_f}(u) =\sum_{b\in V_n}\Delta_f(b)(-1)^{u\mathbin\cdot b} =W_f(u)^2.

Lean code for Theorem1.4.3●1 theorem
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Derivatives.lean
    complete
    theorem CryptBoolean.rawFourierTransform_autocorrelation {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform (CryptBoolean.autocorrelation f) a =
    ↑(CryptBoolean.walshTransform f a) ^ 2
    theorem CryptBoolean.rawFourierTransform_autocorrelation
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (CryptBoolean.autocorrelation f) a =
    ↑(CryptBoolean.walshTransform f a) ^ 2
    Wiener--Khintchine: the raw transform of autocorrelation is the squared Walsh spectrum.
Corollary1.4.4
uses 1used by 0✓L∃∀N
Tagscarletchapter-2relation-26page-28fidelity-exact

Relation (26) (Carlet, p. 28). For every f:V_n\to\mathbb F_2, \sum_{b\in V_n}\Delta_f(b)=W_f(0)^2.

Lean code for Corollary1.4.4●1 theorem
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Derivatives.lean
    complete
    theorem CryptBoolean.sum_autocorrelation_eq_walshTransform_zero_sq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ b, CryptBoolean.autocorrelation f b =
    ↑(CryptBoolean.walshTransform f 0) ^ 2
    theorem CryptBoolean.sum_autocorrelation_eq_walshTransform_zero_sq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ b, CryptBoolean.autocorrelation f b =
    ↑(CryptBoolean.walshTransform f 0) ^ 2
    The total autocorrelation is the square of the zero-frequency Walsh value.