bitsToNat Properties

This file establishes that binary evaluation identifies length-n bit-vectors with the natural numbers below 2 ^ n. It also records consequences used by the Elligator string encoding.

Main results

• bitsToNat_lt_two_pow_n: the value of an n-bit vector is below 2 ^ n.
• bitsToNat_injective: binary evaluation is injective.
• bitsToFin_bijective: binary evaluation, with its range encoded in the codomain, is a bijection
• bitsToNat_surj: every natural number below 2 ^ n is represented by an n-bit vector.
• σ_injective: casting binary values into a prime field is injective on b-bit vectors.
• exists_σ_preimage_or_neg: every field element, up to sign, is represented by a bit-vector in S.

References

See [bernstein2013a], Section 3.4, Theorem 4.

theorem Elligator.Elligator1.bitsToNat_le_full_range {n : ℕ} (τ : Fin n → Bool) : bitsToNat τ ≤ ∑ i ∈ Finset.range n, 2 ^ i

theorem Elligator.Elligator1.bitsToNat_lt_two_pow_n {n : ℕ} (τ : Fin n → Bool) : bitsToNat τ < 2 ^ n

Every bit-vector of length n has binary value less than 2^n.

theorem Elligator.Elligator1.bitsToNat_le_q_sub_one_div_two {q : ℕ} (τ : ↥S) : bitsToNat ↑τ ≤ (q - 1) / 2

theorem Elligator.Elligator1.bitsToNat_succ {n : ℕ} (τ : Fin (n + 1) → Bool) : bitsToNat τ = (2 * bitsToNat fun (i : Fin n) => τ i.succ) + if τ 0 = true then 1 else 0

Splitting off the least significant bit gives the standard binary recurrence.

@[simp]

theorem Elligator.Elligator1.bitsToNat_cons_false {n : ℕ} (τ : Fin n → Bool) : bitsToNat (Fin.cons false τ) = 2 * bitsToNat τ

Prefixing a zero bit doubles the value of the remaining bits.

@[simp]

theorem Elligator.Elligator1.bitsToNat_cons_true {n : ℕ} (τ : Fin n → Bool) : bitsToNat (Fin.cons true τ) = 2 * bitsToNat τ + 1

Prefixing a one bit doubles the value of the remaining bits and adds one.

theorem Elligator.Elligator1.bitsToNat_injective {n : ℕ} : Function.Injective bitsToNat

bitsToNat is injective: distinct bit-vectors give distinct natural numbers.

theorem Elligator.Elligator1.bitsToNat_surj (n m : ℕ) (hm : m < 2 ^ n) : ∃ (τ : Fin n → Bool), bitsToNat τ = m

Every natural number less than 2^n is the binary value of some bit-vector.

This statement doesn't use Function.surjective since it is not viable to get hm into the ∀ m value.

theorem Elligator.Elligator1.natCast_injective_of_prime_card {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (q_prime : Prime q) (a b : ℕ) (ha : a < q) (hb : b < q) (h : ↑a = ↑b) : a = b

theorem Elligator.Elligator1.lower_half_neg_eq {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (hq : Prime q) {a b : ℕ} (ha : a ≤ (q - 1) / 2) (hb : b ≤ (q - 1) / 2) (heq : ↑a = -↑b) : a = b

theorem Elligator.Elligator1.σ_injective {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (q_prime : Prime q) (hq_mod : q % 4 = 3) : Function.Injective σ

theorem Elligator.Elligator1.exists_S_elem_of_le {q : ℕ} (hq_mod : q % 4 = 3) (n : ℕ) (hle : n ≤ (q - 1) / 2) : ∃ (τ : ↥S), bitsToNat ↑τ = n

theorem Elligator.Elligator1.exists_σ_preimage_or_neg {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (q_prime : Prime q) (hq_mod : q % 4 = 3) (t : F) : ∃ (τ : ↥S), σ ↑τ = t ∨ σ ↑τ = -t

Every field element has a representative in S up to sign. For prime q with q ≡ 3 (mod 4) and any t : F, there is a string τ ∈ S such that σ τ = t or σ τ = -t. This is the lower-half representative argument used to prove that the string encoding covers all of ϕ(F) in Theorem 4.