Cryptographic Boolean Functions in Lean

1.5. Algebraic normal form🔗

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