Cryptographic Boolean Functions in Lean

1.3. Algebraic normal form existence and uniqueness🔗

Theorem1.3.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 1
Used by 11
Reverse dependency previews
Preview
Definition 1.4.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2proposition-1pages-10-11fidelity-exact

Existence and uniqueness of the ANF, and Proposition 1 (Carlet, pp. 10--11). For every f:V_n\to\mathbb F_2, there exists a unique family (c_S)_{S\subseteq[n]} such that f(x)=\bigoplus_{S\subseteq[n]}c_S\prod_{i\in S}x_i \qquad(x\in V_n). If \mathbf 1_T denotes the indicator vector of T\subseteq[n], then the coefficient of x^S is c_S =\bigoplus_{\substack{x\in V_n\\\operatorname{supp}(x)\subseteq S}}f(x) =\bigoplus_{T\subseteq S}f(\mathbf 1_T) \qquad(S\subseteq[n]).

Lean code for Theorem1.3.1●8 declarations
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.anfMonomial_f₂CubeOfFinset {n : ℕ} (S U : Finset (Fin n)) :
  FABL.anfMonomial S (FABL.f₂CubeOfFinset U) = if S ⊆ U then 1 else 0
    theorem FABL.anfMonomial_f₂CubeOfFinset {n : ℕ}
  (S U : Finset (Fin n)) :
  FABL.anfMonomial S
      (FABL.f₂CubeOfFinset U) =
    if S ⊆ U then 1 else 0
    The square-free monomial evaluated at a subset indicator is one exactly on subsets.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.anfEval_f₂CubeOfFinset {n : ℕ} (c : FABL.ANFCoefficients n)
  (U : Finset (Fin n)) :
  FABL.anfEval c (FABL.f₂CubeOfFinset U) = ∑ S ∈ U.powerset, c S
    theorem FABL.anfEval_f₂CubeOfFinset {n : ℕ}
  (c : FABL.ANFCoefficients n)
  (U : Finset (Fin n)) :
  FABL.anfEval c (FABL.f₂CubeOfFinset U) =
    ∑ S ∈ U.powerset, c S
    ANF evaluation at a subset indicator is the zeta partial sum over the powerset.
  • defdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    def FABL.anfCoeff {n : ℕ} (f : FABL.F₂BooleanFunction n) :
  FABL.ANFCoefficients n
    def FABL.anfCoeff {n : ℕ}
  (f : FABL.F₂BooleanFunction n) :
  FABL.ANFCoefficients n
    The canonical `𝔽₂` Möbius-inverse coefficient family of a Boolean function.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.anfEval_anfCoeff_f₂CubeOfFinset {n : ℕ}
  (f : FABL.F₂BooleanFunction n) (U : Finset (Fin n)) :
  FABL.anfEval (FABL.anfCoeff f) (FABL.f₂CubeOfFinset U) =
    f (FABL.f₂CubeOfFinset U)
    theorem FABL.anfEval_anfCoeff_f₂CubeOfFinset
  {n : ℕ} (f : FABL.F₂BooleanFunction n)
  (U : Finset (Fin n)) :
  FABL.anfEval (FABL.anfCoeff f)
      (FABL.f₂CubeOfFinset U) =
    f (FABL.f₂CubeOfFinset U)
    The canonical coefficients reproduce `f` at every subset indicator.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.anfEval_anfCoeff {n : ℕ} (f : FABL.F₂BooleanFunction n) :
  FABL.anfEval (FABL.anfCoeff f) = f
    theorem FABL.anfEval_anfCoeff {n : ℕ}
  (f : FABL.F₂BooleanFunction n) :
  FABL.anfEval (FABL.anfCoeff f) = f
    The canonical coefficient family evaluates to the original Boolean function.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.anfCoeff_unique_of_powerset_sum {n : ℕ}
  (c d : FABL.ANFCoefficients n)
  (h :
    ∀ (U : Finset (Fin n)),
      ∑ T ∈ U.powerset, c T = ∑ T ∈ U.powerset, d T) :
  c = d
    theorem FABL.anfCoeff_unique_of_powerset_sum
  {n : ℕ} (c d : FABL.ANFCoefficients n)
  (h :
    ∀ (U : Finset (Fin n)),
      ∑ T ∈ U.powerset, c T =
        ∑ T ∈ U.powerset, d T) :
  c = d
    Equal powerset partial sums force equal ANF coefficient families.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.anfEval_injective {n : ℕ} {c d : FABL.ANFCoefficients n}
  (h : FABL.anfEval c = FABL.anfEval d) : c = d
    theorem FABL.anfEval_injective {n : ℕ}
  {c d : FABL.ANFCoefficients n}
  (h : FABL.anfEval c = FABL.anfEval d) :
  c = d
    Coefficient families with equal ANF evaluation are equal.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.existsUnique_anfEval {n : ℕ} (f : FABL.F₂BooleanFunction n) :
  ∃! c, FABL.anfEval c = f
    theorem FABL.existsUnique_anfEval {n : ℕ}
  (f : FABL.F₂BooleanFunction n) :
  ∃! c, FABL.anfEval c = f
    Every Boolean function has a unique algebraic normal form.

Existence follows from the characteristic-two subset-lattice transform, while injectivity of its zeta sums gives uniqueness.