Cryptographic Boolean Functions in Lean

6.6. Counting resilient functions🔗

Theorem6.6.1

Group: Chapter 6: Resilient functions (38)

Group member previews

Preview

Theorem 6.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 6.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-7maiorana-mcfarlandcountingpage-129fidelity-corrected-r-two

Maiorana--McFarland counts (Carlet, p. 129). Let r>0 and s=n-r. The number of pairs (\varphi,g) in Relation (59) satisfying \varphi(y)\ne0 for every y is (2^{r+1}-2)^{2^s}. The number satisfying w_H(\varphi(y))>m for every y is \left( 2\sum_{i=m+1}^{r}\binom ri \right)^{2^{n-r}}. If r=1 or r\ge3, the first quantity is at most 2^{2^{n-1}}. At r=2 the printed bound is false and the strict reverse inequality holds.

Lean code for Theorem6.6.1●8 declarations

defdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandCounting.lean

complete

def CryptBoolean.pointwiseConstrainedGeneralMaioranaMcFarlandParametersEquiv
  {r s : ℕ} (P : FABL.F₂Cube r → Prop) :
  { p // ∀ (y : FABL.F₂Cube s), P (p.1 y) } ≃
    (FABL.F₂Cube s → { a // P a }) × CryptBoolean.BooleanFunction s

def CryptBoolean.pointwiseConstrainedGeneralMaioranaMcFarlandParametersEquiv
  {r s : ℕ} (P : FABL.F₂Cube r → Prop) :
  { p //
      ∀ (y : FABL.F₂Cube s), P (p.1 y) } ≃
    (FABL.F₂Cube s → { a // P a }) ×
      CryptBoolean.BooleanFunction s

A pointwise constraint on the frequency map is equivalent to choosing
one constrained frequency independently at every input, together with an
unconstrained Boolean offset.

theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.card_pointwiseConstrainedGeneralMaioranaMcFarlandParameters
  {r s : ℕ} (P : FABL.F₂Cube r → Prop) [DecidablePred P] :
  Fintype.card { p // ∀ (y : FABL.F₂Cube s), P (p.1 y) } =
    (2 * Fintype.card { a // P a }) ^ 2 ^ s

theorem CryptBoolean.card_pointwiseConstrainedGeneralMaioranaMcFarlandParameters
  {r s : ℕ} (P : FABL.F₂Cube r → Prop)
  [DecidablePred P] :
  Fintype.card
      { p //
        ∀ (y : FABL.F₂Cube s),
          P (p.1 y) } =
    (2 * Fintype.card { a // P a }) ^
      2 ^ s

The cardinality of pointwise-constrained Relation (59) construction data
is the corresponding one-fiber count, including the free offset bit, raised
to the number of inputs.

theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.card_nonzero_f₂Cube (r : ℕ) :
  Fintype.card { a // a ≠ 0 } = 2 ^ r - 1

theorem CryptBoolean.card_nonzero_f₂Cube (r : ℕ) :
  Fintype.card { a // a ≠ 0 } = 2 ^ r - 1

The punctured `r`-dimensional binary cube has `2^r - 1` elements.

theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.card_f₂Cube_weight_gt_eq_sum_choose (r m : ℕ) :
  Fintype.card { a // m < (FABL.f₂Support a).card } =
    ∑ i ∈ Finset.Icc (m + 1) r, r.choose i

theorem CryptBoolean.card_f₂Cube_weight_gt_eq_sum_choose
  (r m : ℕ) :
  Fintype.card
      { a //
        m < (FABL.f₂Support a).card } =
    ∑ i ∈ Finset.Icc (m + 1) r, r.choose i

The number of binary frequencies of weight greater than `m` is the upper
binomial tail.

theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.card_nonzeroGeneralMaioranaMcFarlandParameters (r s : ℕ) :
  Fintype.card { p // ∀ (y : FABL.F₂Cube s), p.1 y ≠ 0 } =
    (2 ^ (r + 1) - 2) ^ 2 ^ s

theorem CryptBoolean.card_nonzeroGeneralMaioranaMcFarlandParameters
  (r s : ℕ) :
  Fintype.card
      { p //
        ∀ (y : FABL.F₂Cube s),
          p.1 y ≠ 0 } =
    (2 ^ (r + 1) - 2) ^ 2 ^ s

The exact number of Relation (59) construction pairs whose frequency map
is nonzero at every input.

theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.card_highWeightGeneralMaioranaMcFarlandParameters
  (r s m : ℕ) :
  Fintype.card
      { p //
        ∀ (y : FABL.F₂Cube s), m < (FABL.f₂Support (p.1 y)).card } =
    (2 * ∑ i ∈ Finset.Icc (m + 1) r, r.choose i) ^ 2 ^ s

theorem CryptBoolean.card_highWeightGeneralMaioranaMcFarlandParameters
  (r s m : ℕ) :
  Fintype.card
      { p //
        ∀ (y : FABL.F₂Cube s),
          m <
            (FABL.f₂Support
                (p.1 y)).card } =
    (2 *
        ∑ i ∈ Finset.Icc (m + 1) r,
          r.choose i) ^
      2 ^ s

The exact number of Relation (59) construction pairs whose frequency-map
values all have weight greater than `m`.

theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.card_nonzeroGeneralMaioranaMcFarlandParameters_le (r s : ℕ)
  (hr : r = 1 ∨ 3 ≤ r) :
  Fintype.card { p // ∀ (y : FABL.F₂Cube s), p.1 y ≠ 0 } ≤
    2 ^ 2 ^ (r + s - 1)

theorem CryptBoolean.card_nonzeroGeneralMaioranaMcFarlandParameters_le
  (r s : ℕ) (hr : r = 1 ∨ 3 ≤ r) :
  Fintype.card
      { p //
        ∀ (y : FABL.F₂Cube s),
          p.1 y ≠ 0 } ≤
    2 ^ 2 ^ (r + s - 1)

Corrected form of Carlet's upper bound: for `r = 1` or `r ≥ 3`, the
number of everywhere-nonzero Relation (59) construction pairs is at most
`2^(2^(r+s-1))`.

theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandCounting.lean

complete

theorem CryptBoolean.card_nonzeroGeneralMaioranaMcFarlandParameters_sourceBound_lt_at_two
  (s : ℕ) :
  2 ^ 2 ^ (2 + s - 1) <
    Fintype.card { p // ∀ (y : FABL.F₂Cube s), p.1 y ≠ 0 }

theorem CryptBoolean.card_nonzeroGeneralMaioranaMcFarlandParameters_sourceBound_lt_at_two
  (s : ℕ) :
  2 ^ 2 ^ (2 + s - 1) <
    Fintype.card
      { p //
        ∀ (y : FABL.F₂Cube s), p.1 y ≠ 0 }

Source correction: at `r = 2`, Carlet's stated upper bound is reversed
strictly for every `s`; the smallest instance is already `6 > 4`.

Theorem6.6.2

Group: Chapter 6: Resilient functions (38)

Group member previews

Preview

Theorem 6.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 3.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-7resiliencycountingpage-129fidelity-exact

Naive counting bound (Carlet, p. 129). The number of m-resilient n-variable Boolean functions is at most 2^{\sum_{i=0}^{n-m-1}\binom ni}. The count is extensional and counts Boolean functions, with algebraic normal forms serving as their unique representation.

Lean code for Theorem6.6.2●2 theorems

theoremdefined in CryptBoolean/Carlet/Chapter07/NaiveCounting.lean

complete

theorem CryptBoolean.exists_eq_affineFunction_fullFrequency_of_isResilient_natPred
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hf : CryptBoolean.IsResilient (n - 1) f) :
  ∃ b, f = FABL.affineFunction b (FABL.f₂CubeOfFinset Finset.univ)

theorem CryptBoolean.exists_eq_affineFunction_fullFrequency_of_isResilient_natPred
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n)
  (hf :
    CryptBoolean.IsResilient (n - 1) f) :
  ∃ b,
    f =
      FABL.affineFunction b
        (FABL.f₂CubeOfFinset Finset.univ)

A highest-order resilient Boolean function is full parity or its
complement.

theoremdefined in CryptBoolean/Carlet/Chapter07/NaiveCounting.lean

complete

theorem CryptBoolean.natCard_isResilient_le_naiveBound (m n : ℕ) (hm : m < n) :
  Nat.card { f // CryptBoolean.IsResilient m f } ≤
    2 ^ ∑ i ∈ Finset.range (n - m - 1 + 1), n.choose i

theorem CryptBoolean.natCard_isResilient_le_naiveBound
  (m n : ℕ) (hm : m < n) :
  Nat.card
      { f //
        CryptBoolean.IsResilient m f } ≤
    2 ^
      ∑ i ∈ Finset.range (n - m - 1 + 1),
        n.choose i

Carlet's naive upper bound on the number of `m`-resilient
`n`-variable Boolean functions.