Cryptographic Boolean Functions in Lean

1.5. Finite-field representations🔗

Definition1.5.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 0
Used by 8
Reverse dependency previews
Preview
Theorem 1.5.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2absolute-tracepage-15fidelity-exact-direct-mathlib

Absolute trace (Carlet, p. 15). Let n>0, let K_n=\operatorname{GF}(2^n), and let \iota:\mathbb F_2\hookrightarrow K_n be the canonical embedding. The absolute trace is the \mathbb F_2-linear map \operatorname{Tr}_n:K_n\longrightarrow\mathbb F_2, \qquad \iota(\operatorname{Tr}_n(x)) =\sum_{i=0}^{n-1}x^{2^i}. The pairing (x,y)\mapsto\operatorname{Tr}_n(xy) is nondegenerate; hence \operatorname{Tr}_n is surjective. In particular, choose \tau\in K_n with \operatorname{Tr}_n(\tau)=1. For every f:K_n\to\mathbb F_2, define F_\tau(x)= \begin{cases} 0,&f(x)=0,\\ \tau,&f(x)=1. \end{cases} Then \operatorname{Tr}_n(F_\tau(x))=f(x) \qquad(x\in K_n).

Lean code for Definition1.5.1●10 declarations
  • abbrevdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    abbrev CryptBoolean.BinaryGaloisField (n : ℕ) : Type
    abbrev CryptBoolean.BinaryGaloisField (n : ℕ) :
  Type
    Mathlib's canonical field with `2^n` elements.
  • abbrevdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    abbrev CryptBoolean.FieldBooleanFunction (n : ℕ) : Type
    abbrev CryptBoolean.FieldBooleanFunction
  (n : ℕ) : Type
    A scalar Boolean function represented on the binary Galois field.
  • defdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    def CryptBoolean.absoluteTrace (n : ℕ) :
  CryptBoolean.BinaryGaloisField n →ₗ[FABL.𝔽₂] FABL.𝔽₂
    def CryptBoolean.absoluteTrace (n : ℕ) :
  CryptBoolean.BinaryGaloisField
      n →ₗ[FABL.𝔽₂]
    FABL.𝔽₂
    The absolute trace from `GF(2^n)` to `GF(2)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    theorem CryptBoolean.algebraMap_absoluteTrace_eq_sum_frobenius {n : ℕ}
  (hn : n ≠ 0) (x : CryptBoolean.BinaryGaloisField n) :
  (algebraMap FABL.𝔽₂ (CryptBoolean.BinaryGaloisField n))
      ((CryptBoolean.absoluteTrace n) x) =
    ∑ i ∈ Finset.range n, x ^ 2 ^ i
    theorem CryptBoolean.algebraMap_absoluteTrace_eq_sum_frobenius
  {n : ℕ} (hn : n ≠ 0)
  (x : CryptBoolean.BinaryGaloisField n) :
  (algebraMap FABL.𝔽₂
        (CryptBoolean.BinaryGaloisField
          n))
      ((CryptBoolean.absoluteTrace n) x) =
    ∑ i ∈ Finset.range n, x ^ 2 ^ i
    Mathlib's finite-field trace formula specializes to the absolute binary trace.
  • theoremdefined in Mathlib/RingTheory/Trace/Basic.lean
    complete
    theorem traceForm_nondegenerate.{u_4, u_5} (K : Type u_4) (L : Type u_5)
  [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
  [Algebra.IsSeparable K L] : (Algebra.traceForm K L).Nondegenerate
    theorem traceForm_nondegenerate.{u_4, u_5}
  (K : Type u_4) (L : Type u_5) [Field K]
  [Field L] [Algebra K L]
  [FiniteDimensional K L]
  [Algebra.IsSeparable K L] :
  (Algebra.traceForm K L).Nondegenerate
    Let $L/K$ be a finite extension of fields. If $L/K$ is separable,
then `traceForm` is nondegenerate.
  • theoremdefined in Mathlib/RingTheory/Trace/Basic.lean
    complete
    theorem Algebra.trace_surjective.{u_4, u_5} (K : Type u_4) (L : Type u_5)
  [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
  [Algebra.IsSeparable K L] : Function.Surjective ⇑(Algebra.trace K L)
    theorem Algebra.trace_surjective.{u_4, u_5}
  (K : Type u_4) (L : Type u_5) [Field K]
  [Field L] [Algebra K L]
  [FiniteDimensional K L]
  [Algebra.IsSeparable K L] :
  Function.Surjective ⇑(Algebra.trace K L)
  • theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    theorem CryptBoolean.exists_absoluteTrace_eq_one (n : ℕ) :
  ∃ traceOne, (CryptBoolean.absoluteTrace n) traceOne = 1
    theorem CryptBoolean.exists_absoluteTrace_eq_one
  (n : ℕ) :
  ∃ traceOne,
    (CryptBoolean.absoluteTrace n)
        traceOne =
      1
    Nondegeneracy of the finite-field trace supplies an element of absolute trace one.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    theorem CryptBoolean.absoluteTrace_surjective (n : ℕ) :
  Function.Surjective ⇑(CryptBoolean.absoluteTrace n)
    theorem CryptBoolean.absoluteTrace_surjective
  (n : ℕ) :
  Function.Surjective
    ⇑(CryptBoolean.absoluteTrace n)
    The absolute trace onto the binary prime field is surjective.
  • defdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    def CryptBoolean.traceLift {n : ℕ}
  (traceOne : CryptBoolean.BinaryGaloisField n)
  (f : CryptBoolean.FieldBooleanFunction n) :
  CryptBoolean.BinaryGaloisField n → CryptBoolean.BinaryGaloisField n
    def CryptBoolean.traceLift {n : ℕ}
  (traceOne :
    CryptBoolean.BinaryGaloisField n)
  (f :
    CryptBoolean.FieldBooleanFunction n) :
  CryptBoolean.BinaryGaloisField n →
    CryptBoolean.BinaryGaloisField n
    A field-valued lift selected by a trace-one element.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    theorem CryptBoolean.absoluteTrace_traceLift {n : ℕ}
  (traceOne : CryptBoolean.BinaryGaloisField n)
  (htraceOne : (CryptBoolean.absoluteTrace n) traceOne = 1)
  (f : CryptBoolean.FieldBooleanFunction n)
  (x : CryptBoolean.BinaryGaloisField n) :
  (CryptBoolean.absoluteTrace n) (CryptBoolean.traceLift traceOne f x) =
    f x
    theorem CryptBoolean.absoluteTrace_traceLift
  {n : ℕ}
  (traceOne :
    CryptBoolean.BinaryGaloisField n)
  (htraceOne :
    (CryptBoolean.absoluteTrace n)
        traceOne =
      1)
  (f :
    CryptBoolean.FieldBooleanFunction n)
  (x : CryptBoolean.BinaryGaloisField n) :
  (CryptBoolean.absoluteTrace n)
      (CryptBoolean.traceLift traceOne f
        x) =
    f x
    Every field-domain Boolean function is an absolute trace of a field-valued function.
Theorem1.5.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 0
Used by 3
Reverse dependency previews
Preview
Theorem 1.5.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2relation-4page-15fidelity-exact

Univariate representation (Carlet, Relation (4), p. 15). Let n>0 and K_n=\operatorname{GF}(2^n). For every function F:K_n\to K_n, there exists a unique polynomial P_F\in K_n[X] such that \deg P_F<2^n \qquad\text{and}\qquad P_F(x)=F(x)\quad\text{for every }x\in K_n. Equivalently, P_F(X)=\sum_{i=0}^{2^n-1}\delta_iX^i for uniquely determined coefficients \delta_i\in K_n.

Lean code for Theorem1.5.2●4 declarations
  • defdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    def CryptBoolean.univariateRepresentation {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  Polynomial (CryptBoolean.BinaryGaloisField n)
    def CryptBoolean.univariateRepresentation
  {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  Polynomial
    (CryptBoolean.BinaryGaloisField n)
    The canonical Lagrange polynomial representing a function on `GF(2^n)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    theorem CryptBoolean.eval_univariateRepresentation {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n → CryptBoolean.BinaryGaloisField n)
  (x : CryptBoolean.BinaryGaloisField n) :
  Polynomial.eval x (CryptBoolean.univariateRepresentation F) = F x
    theorem CryptBoolean.eval_univariateRepresentation
  {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n)
  (x : CryptBoolean.BinaryGaloisField n) :
  Polynomial.eval x
      (CryptBoolean.univariateRepresentation
        F) =
    F x
    The univariate representation evaluates to the original function.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    theorem CryptBoolean.degree_univariateRepresentation_lt_card {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  (CryptBoolean.univariateRepresentation F).degree <
    ↑(Nat.card (CryptBoolean.BinaryGaloisField n))
    theorem CryptBoolean.degree_univariateRepresentation_lt_card
  {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  (CryptBoolean.univariateRepresentation
        F).degree <
    ↑(Nat.card
        (CryptBoolean.BinaryGaloisField
          n))
    The canonical univariate representation has degree strictly below the field cardinality.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean
    complete
    theorem CryptBoolean.existsUnique_univariateRepresentation {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  ∃! P,
    P.degree < ↑(Nat.card (CryptBoolean.BinaryGaloisField n)) ∧
      ∀ (x : CryptBoolean.BinaryGaloisField n),
        Polynomial.eval x P = F x
    theorem CryptBoolean.existsUnique_univariateRepresentation
  {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  ∃! P,
    P.degree <
        ↑(Nat.card
            (CryptBoolean.BinaryGaloisField
              n)) ∧
      ∀
        (x :
          CryptBoolean.BinaryGaloisField
            n),
        Polynomial.eval x P = F x
    Carlet's unique univariate representation below degree `2^n`.

The polynomial P_F is obtained by finite Lagrange interpolation.

Theorem1.5.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.
uses 1
Used by 6
Reverse dependency previews
Preview
Theorem 4.2.10
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2finite-field-coordinatestrace-pairingfidelity-explicit-coordinate-representation

Coordinates from the trace pairing. Let n\ge0 and choose an \mathbb F_2-linear isomorphism \theta:V_n\xrightarrow{\sim}K_n. For every u\in V_n there is a unique b\in K_n such that u\mathbin\cdot x=\operatorname{Tr}_n\!\left(b\theta(x)\right) \qquad(x\in V_n).

Lean code for Theorem1.5.3●1 theorem
  • theoremdefined in CryptBoolean/Carlet/Chapter02/TracePairing.lean
    complete
    theorem CryptBoolean.existsUnique_tracePairingCoefficient {n : ℕ}
  (theta : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (u : FABL.F₂Cube n) :
  ∃! b,
    ∀ (x : FABL.F₂Cube n),
      FABL.f₂DotProduct u x =
        (CryptBoolean.absoluteTrace n) (b * theta x)
    theorem CryptBoolean.existsUnique_tracePairingCoefficient
  {n : ℕ}
  (theta :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (u : FABL.F₂Cube n) :
  ∃! b,
    ∀ (x : FABL.F₂Cube n),
      FABL.f₂DotProduct u x =
        (CryptBoolean.absoluteTrace n)
          (b * theta x)
    Every linear character of a binary cube has a unique coefficient under the finite-field
trace pairing transported by a linear equivalence.

This coordinate formula follows from the nondegeneracy of the trace pairing.

Theorem1.5.4
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.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Proposition 1.5.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2univariate-representationalgebraic-degreepage-17fidelity-exact

Univariate binary-degree formula (Carlet, p. 17). Let n>0, choose an \mathbb F_2-linear isomorphism \theta:V_n\xrightarrow{\sim}K_n, and let P_f(X)=\sum_{j=0}^{2^n-1}\delta_jX^j be the unique polynomial of degree less than 2^n representing the prime-field embedding of f\circ\theta^{-1}. Then \deg_{\mathrm{alg}}(f)=\max_{\delta_j\ne0}w_2(j), where the maximum is zero when P_f=0.

Lean code for Theorem1.5.4●3 declarations
  • defdefined in CryptBoolean/Carlet/Chapter02/FiniteFieldAlgebraicDegree.lean
    complete
    def CryptBoolean.binaryWeight (k : ℕ) : ℕ
    def CryptBoolean.binaryWeight (k : ℕ) : ℕ
    Carlet p. 17: the binary weight of an exponent is the Hamming weight of its base-two
expansion.
  • defdefined in CryptBoolean/Carlet/Chapter02/FiniteFieldAlgebraicDegree.lean
    complete
    def CryptBoolean.univariateBinaryDegree {n : ℕ}
  (P : Polynomial (CryptBoolean.BinaryGaloisField n)) : ℕ
    def CryptBoolean.univariateBinaryDegree
  {n : ℕ}
  (P :
    Polynomial
      (CryptBoolean.BinaryGaloisField
        n)) :
  ℕ
    Carlet p. 17: the binary degree of a univariate polynomial is the maximum binary weight
among the exponents of its nonzero coefficients.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteFieldAlgebraicDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_eq_univariateBinaryDegree {n : ℕ}
  (hn : n ≠ 0)
  (θ : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (f : FABL.F₂BooleanFunction n) :
  FABL.functionAlgebraicDegree f =
    CryptBoolean.univariateBinaryDegree
      (CryptBoolean.univariateRepresentation fun z =>
        (algebraMap FABL.𝔽₂ (CryptBoolean.BinaryGaloisField n))
          (f (θ.symm z)))
    theorem CryptBoolean.functionAlgebraicDegree_eq_univariateBinaryDegree
  {n : ℕ} (hn : n ≠ 0)
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (f : FABL.F₂BooleanFunction n) :
  FABL.functionAlgebraicDegree f =
    CryptBoolean.univariateBinaryDegree
      (CryptBoolean.univariateRepresentation
        fun z =>
        (algebraMap FABL.𝔽₂
            (CryptBoolean.BinaryGaloisField
              n))
          (f (θ.symm z)))
    Carlet p. 17: after any binary linear identification with `GF(2^n)`, coordinate ANF
degree equals the binary degree of the canonical bounded univariate representation.

Expanding the prime-field embedding in a K_n-valued ANF identifies its largest square-free monomial degree with the largest binary weight of an exponent carrying a nonzero coefficient.

Proposition1.5.5
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.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 4.2.10
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2proposition-3pages-17-18fidelity-exact

Proposition 3 (Carlet, pp. 17--18). Let n>0, let a\in K_n, choose an \mathbb F_2-linear isomorphism \theta:V_n\xrightarrow{\sim}K_n, and let k be represented by an integer 0\le k<2^n-1 modulo 2^n-1. If the Boolean function f_\theta(x)=\operatorname{Tr}_n\!\left(a\,\theta(x)^k\right) is not identically zero, then \deg_{\mathrm{alg}}(f_\theta)=w_2(k), where w_2(k) is the number of nonzero digits in the binary expansion of k.

Lean code for Proposition1.5.5●1 theorem
  • theoremdefined in CryptBoolean/Carlet/Chapter02/TraceMonomialDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_traceMonomial {n k : ℕ}
  (hn : 0 < n) (hk : k < 2 ^ n - 1)
  (θ : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n)
  (hfun : (fun x => (CryptBoolean.absoluteTrace n) (a * θ x ^ k)) ≠ 0) :
  (FABL.functionAlgebraicDegree fun x =>
      (CryptBoolean.absoluteTrace n) (a * θ x ^ k)) =
    CryptBoolean.binaryWeight k
    theorem CryptBoolean.functionAlgebraicDegree_traceMonomial
  {n k : ℕ} (hn : 0 < n)
  (hk : k < 2 ^ n - 1)
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n)
  (hfun :
    (fun x =>
        (CryptBoolean.absoluteTrace n)
          (a * θ x ^ k)) ≠
      0) :
  (FABL.functionAlgebraicDegree fun x =>
      (CryptBoolean.absoluteTrace n)
        (a * θ x ^ k)) =
    CryptBoolean.binaryWeight k
    Carlet Proposition 3: a nonzero trace monomial has algebraic degree equal to the
binary Hamming weight of its exponent.

The Frobenius-orbit polynomial agrees with the bounded univariate representation. Function nonzeroness makes its support nonempty, and every surviving orbit exponent is a cyclic binary shift of k.