Cryptographic Boolean Functions in Lean

1.1. Boolean functions and support🔗

Definition1.1.1
Group: Chapter 1: Generalities on Boolean functions (40)
Group member previews
Preview
Definition 1.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 7
Reverse dependency previews
Preview
Definition 1.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2pages-8-22fidelity-exact

Boolean and sign functions (Carlet, pp. 8 and 22). Fix n\ge 0 and write V_n=\mathbb F_2^n. An n-variable Boolean function is a map f:V_n\to\mathbb F_2. Its sign function is f_\chi:V_n\longrightarrow\{-1,1\}\subset\mathbb R, \qquad f_\chi(x)=(-1)^{f(x)}.

Lean code for Definition1.1.1●2 definitions
  • abbrevdefined in CryptBoolean/BooleanFunction.lean
    complete
    abbrev CryptBoolean.BooleanFunction (n : ℕ) : Type
    abbrev CryptBoolean.BooleanFunction (n : ℕ) :
  Type
    Scalar cryptographic Boolean functions on the additive binary cube.
  • abbrevdefined in CryptBoolean/BooleanFunction.lean
    complete
    abbrev CryptBoolean.realSignView {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  FABL.F₂Cube n → ℝ
    abbrev CryptBoolean.realSignView {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  FABL.F₂Cube n → ℝ
    The real sign view `(-1)^{f(x)}` of a bit-valued Boolean function.
Definition1.1.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 1
Used by 16
Reverse dependency previews
Preview
Definition 1.4.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2page-8fidelity-exact-with-mathlib-hamming-norm

Support and Hamming weight (Carlet, p. 8). For f:V_n\to\mathbb F_2, define \operatorname{supp}(f)=\{x\in V_n:f(x)=1\}, \qquad w_H(f)=|\operatorname{supp}(f)|.

Lean code for Definition1.1.2●4 declarations
  • abbrevdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    abbrev CryptBoolean.support {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  Finset (FABL.F₂Cube n)
    abbrev CryptBoolean.support {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Finset (FABL.F₂Cube n)
    The support of a Boolean function, as the finite set on which it is one.
  • abbrevdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    abbrev CryptBoolean.hammingWeight {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℕ
    abbrev CryptBoolean.hammingWeight {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℕ
    The Hamming weight of a Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.mem_support {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) : x ∈ CryptBoolean.support f ↔ f x = 1
    theorem CryptBoolean.mem_support {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  x ∈ CryptBoolean.support f ↔ f x = 1
    The support predicate is extensionally the one-set of the Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Foundations.lean
    complete
    theorem CryptBoolean.hammingWeight_eq_card_support {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.hammingWeight f = (CryptBoolean.support f).card
    theorem CryptBoolean.hammingWeight_eq_card_support
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.hammingWeight f =
    (CryptBoolean.support f).card
    On binary-valued functions, Mathlib's Hamming norm is the cardinality of the one-set.