Cryptographic Boolean Functions in Lean

1.2. Algebraic normal form🔗

Definition1.2.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 1used by 1✓L∃∀N
Tagscarletchapter-2relation-1pages-9-12fidelity-exact-with-zero-convention

Algebraic normal form (Carlet, Relation (1), p. 9). Let [n]=\{1,\ldots,n\}. For coefficients c=(c_S)_{S\subseteq[n]} in \mathbb F_2, set x^S=\prod_{i\in S}x_i, \qquad \operatorname{ANF}_c(x) =\bigoplus_{S\subseteq[n]}c_Sx^S. The coefficient support and algebraic degree are \operatorname{supp}_{\mathrm{ANF}}(c) =\{S\subseteq[n]:c_S\ne0\}, \qquad \deg(c)=\max\{|S|:c_S\ne0\}, with \deg(0)=0. For all coefficient families c,d, \operatorname{ANF}_{c+d}=\operatorname{ANF}_c+\operatorname{ANF}_d, \qquad \deg(c)\le n.

Lean code for Definition1.2.1●10 declarations
  • abbrevdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    abbrev FABL.ANFCoefficients (n : ℕ) : Type
    abbrev FABL.ANFCoefficients (n : ℕ) : Type
    A square-free algebraic normal form coefficient family over coordinate subsets.
  • defdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    def FABL.anfMonomial {n : ℕ} (S : Finset (Fin n)) (x : FABL.F₂Cube n) :
  FABL.𝔽₂
    def FABL.anfMonomial {n : ℕ}
  (S : Finset (Fin n))
  (x : FABL.F₂Cube n) : FABL.𝔽₂
    The square-free monomial `∏ᵢ∈S xᵢ` over `𝔽₂`.
  • defdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    def FABL.anfEval {n : ℕ} (c : FABL.ANFCoefficients n) (x : FABL.F₂Cube n) :
  FABL.𝔽₂
    def FABL.anfEval {n : ℕ}
  (c : FABL.ANFCoefficients n)
  (x : FABL.F₂Cube n) : FABL.𝔽₂
    Evaluation of a square-free algebraic normal form.
  • defdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    def FABL.anfSupport {n : ℕ} (c : FABL.ANFCoefficients n) :
  Finset (Finset (Fin n))
    def FABL.anfSupport {n : ℕ}
  (c : FABL.ANFCoefficients n) :
  Finset (Finset (Fin n))
    The nonzero coefficient support of an algebraic normal form.
  • defdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    def FABL.algebraicDegree {n : ℕ} (c : FABL.ANFCoefficients n) : ℕ
    def FABL.algebraicDegree {n : ℕ}
  (c : FABL.ANFCoefficients n) : ℕ
    The algebraic degree of an ANF coefficient family, with degree zero for the zero family.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.mem_anfSupport {n : ℕ} (c : FABL.ANFCoefficients n)
  (S : Finset (Fin n)) : S ∈ FABL.anfSupport c ↔ c S ≠ 0
    theorem FABL.mem_anfSupport {n : ℕ}
  (c : FABL.ANFCoefficients n)
  (S : Finset (Fin n)) :
  S ∈ FABL.anfSupport c ↔ c S ≠ 0
    Membership in ANF support is nonvanishing of the coefficient.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.anfMonomial_empty {n : ℕ} (x : FABL.F₂Cube n) :
  FABL.anfMonomial ∅ x = 1
    theorem FABL.anfMonomial_empty {n : ℕ}
  (x : FABL.F₂Cube n) :
  FABL.anfMonomial ∅ x = 1
    The empty ANF monomial evaluates to one.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.anfEval_zero {n : ℕ} (x : FABL.F₂Cube n) :
  FABL.anfEval (fun x => 0) x = 0
    theorem FABL.anfEval_zero {n : ℕ}
  (x : FABL.F₂Cube n) :
  FABL.anfEval (fun x => 0) x = 0
    The zero coefficient family evaluates to the zero Boolean function.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.anfEval_add {n : ℕ} (c d : FABL.ANFCoefficients n)
  (x : FABL.F₂Cube n) :
  FABL.anfEval (fun S => c S + d S) x =
    FABL.anfEval c x + FABL.anfEval d x
    theorem FABL.anfEval_add {n : ℕ}
  (c d : FABL.ANFCoefficients n)
  (x : FABL.F₂Cube n) :
  FABL.anfEval (fun S => c S + d S) x =
    FABL.anfEval c x + FABL.anfEval d x
    ANF evaluation is additive in the coefficient family.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/ANF.lean
    complete
    theorem FABL.algebraicDegree_le_dimension {n : ℕ} (c : FABL.ANFCoefficients n) :
  FABL.algebraicDegree c ≤ n
    theorem FABL.algebraicDegree_le_dimension {n : ℕ}
  (c : FABL.ANFCoefficients n) :
  FABL.algebraicDegree c ≤ n
    Algebraic degree is bounded by the ambient dimension.