Documentation

Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial

Shamir Secret Sharing: Polynomial Utilities #

This file contains the Shamir-specific polynomial and interpolation utilities used to prove correctness and privacy of the public scheme construction.

source
noncomputable def Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.tailPolynomial {F : Type u_1} [Field F] (n : ℕ) (coeffs : Fin n → F) :
Polynomial F

The tail polynomial determined by the first n coefficients.

Equations
Instances For
    source
    @[simp]
    theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.tailPolynomial_coeff {F : Type u_1} [Field F] (n : ℕ) (coeffs : Fin n → F) (i : Fin n) :
    (tailPolynomial n coeffs).coeff ↑i = coeffs i
    source
    theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.tailPolynomial_degree_lt {F : Type u_1} [Field F] (n : ℕ) (coeffs : Fin n → F) :
    (tailPolynomial n coeffs).degree < ↑n

    tailPolynomial n coeffs has degree < n by construction.

    source
    theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.tailPolynomial_add {F : Type u_1} [Field F] (n : ℕ) (a b : Fin n → F) :
    tailPolynomial n (a + b) = tailPolynomial n a + tailPolynomial n b

    tailPolynomial is additive in its coefficient vector.

    source
    noncomputable def Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.sharingPolynomial {F : Type u_1} [Field F] (secretValue : F) (tail : Polynomial F) :
    Polynomial F

    The standard Shamir sharing polynomial s + X * q(X).

    Equations
    Instances For
      source
      @[simp]
      theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.sharingPolynomial_eval {F : Type u_1} [Field F] (secretValue x : F) (tail : Polynomial F) :
      Polynomial.eval x (sharingPolynomial secretValue tail) = secretValue + x * Polynomial.eval x tail
      source
      theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.coeff_zero_sharingPolynomial {F : Type u_1} [Field F] (secretValue : F) (tail : Polynomial F) :
      (sharingPolynomial secretValue tail).coeff 0 = secretValue
      source
      theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.constantCoeff_sharingPolynomial {F : Type u_1} [Field F] (secretValue : F) (tail : Polynomial F) :
      Polynomial.constantCoeff (sharingPolynomial secretValue tail) = secretValue
      source
      theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.natDegree_sharingPolynomial_le {F : Type u_1} [Field F] (secretValue : F) (tail : Polynomial F) {n : ℕ} (hdeg : tail.degree < ↑n) :
      (sharingPolynomial secretValue tail).natDegree ≤ n

      If the tail polynomial has degree < n, then the sharing polynomial has natural degree at most n.

      source
      theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.degree_sharingPolynomial_lt_succ {F : Type u_1} [Field F] (secretValue : F) (tail : Polynomial F) {n : ℕ} (hdeg : tail.degree < ↑n) :
      (sharingPolynomial secretValue tail).degree < ↑n + 1

      If the tail polynomial has degree < n, then the sharing polynomial has degree < n + 1.

      source
      theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.degree_sharingPolynomial_tailPolynomial_lt_succ {F : Type u_1} [Field F] (secretValue : F) (n : ℕ) (coeffs : Fin n → F) :
      (sharingPolynomial secretValue (tailPolynomial n coeffs)).degree < ↑n + 1

      The coefficient-vector version of degree_sharingPolynomial_lt_succ.

      source
      noncomputable def Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.reconstruct {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] (x σ : ι → F) :
      F

      Reconstruct the secret from finitely indexed share values by interpolating the unique low-degree polynomial that matches them.

      Equations
      Instances For
        source
        theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.reconstruct_eq_constantCoeff_of_eval_eq {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] {x : ι → F} {p : Polynomial F} (hx : Function.Injective x) (hdeg : p.degree < ↑(Fintype.card ι)) :
        (reconstruct x fun (i : ι) => Polynomial.eval (x i) p) = Polynomial.constantCoeff p

        Reconstruction recovers the constant coefficient of any low-degree polynomial from its values at distinct points.

        source
        theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.reconstruct_sharingPolynomial_eq_secret {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] {x : ι → F} {secretValue : F} {tail : Polynomial F} (hx : Function.Injective x) (hdeg : (sharingPolynomial secretValue tail).degree < ↑(Fintype.card ι)) :
        (reconstruct x fun (i : ι) => Polynomial.eval (x i) (sharingPolynomial secretValue tail)) = secretValue

        Reconstruction succeeds on the values of a Shamir sharing polynomial once the finite index type is large enough.