noncomputable def f (q : ℕ) (n : ℕ) : Polynomial (ZMod q)

Equations

• f q n = Polynomial.X ^ 2 ^ n + 1

def ZMod.toInt (q : ℕ) (x : ZMod q) : ℤ

Equations

• ZMod.toInt q x = x.cast

def ZMod.toFin (q : ℕ) [Fact (q > 1)] (x : ZMod q) : Fin q

Equations

• ZMod.toFin q x = x.cast

@[simp]

theorem ZMod.toInt_inj (q : ℕ) [Fact (q > 1)] {x : ZMod q} {y : ZMod q} : ZMod.toInt q x = ZMod.toInt q y ↔ x = y

def ZMod.toInt_zero_iff_zero (q : ℕ) [Fact (q > 1)] (x : ZMod q) : x = 0 ↔ ZMod.toInt q x = 0

Equations

• ⋯ = ⋯

instance instNontrivialZMod_sSA (q : ℕ) [Fact (q > 1)] : Nontrivial (ZMod q)

Equations

• ⋯ = ⋯

theorem f_deg_eq (q : ℕ) [Fact (q > 1)] (n : ℕ) : (f q n).degree = 2 ^ n

Charaterizing f: f has degree 2^n

theorem f_monic (q : ℕ) [Fact (q > 1)] (n : ℕ) : (f q n).Monic

Charaterizing f: f is monic

@[reducible, inline]

abbrev R (q : ℕ) (n : ℕ) : Type

The basic ring of interest in this dialect is R q n which corresponds to the ring ℤ/qℤ[X]/(X^(2^n) + 1).

Equations

• R q n = (Polynomial (ZMod q) ⧸ Ideal.span {f q n})

@[reducible, inline]

abbrev R.fromPoly {q : ℕ} {n : ℕ} : Polynomial (ZMod q) →+* R q n

Canonical epimorphism / quotient map: ZMod q[X] ->*+ R q n

Equations

• R.fromPoly = Ideal.Quotient.mk (Ideal.span {f q n})

theorem R.surjective_fromPoly (q : ℕ) (n : ℕ) : Function.Surjective ⇑R.fromPoly

fromPoly, the canonical epi from ZMod q[X] →*+ R q n is surjective

theorem R.injective_representative' (q : ℕ) (n : ℕ) : Function.Injective (R.representative' q n)

theorem R.fromPoly_representatitive' (q : ℕ) (n : ℕ) (a : R q n) : R.fromPoly (R.representative' q n a) = a

A concrete version that shows that mapping into the ideal back from the representative produces the representative' NOTE: Lean times out if I use the abbreviation R.fromPoly for unclear reasons!

theorem R.fromPoly_representatitive'_toFun (q : ℕ) (n : ℕ) (a : R q n) : (↑↑R.fromPoly).toFun (R.representative' q n a) = a

noncomputable def R.representative (q : ℕ) (n : ℕ) : R q n → Polynomial (ZMod q)

The representative of a : R q n is the (unique) polynomial p : ZMod q[X] of degree < 2^n such that R.fromPoly p = a.

Equations

• R.representative q n x = R.representative' q n x %ₘ f q n

@[simp]

theorem R.fromPoly_kernel_eq_zero (q : ℕ) (n : ℕ) (x : Polynomial (ZMod q)) : R.fromPoly (f q n * x) = 0

@[simp]

theorem R.fromPoly_representative (q : ℕ) (n : ℕ) [Fact (q > 1)] (a : R q n) : R.fromPoly (R.representative q n a) = a

R.representative is in fact a representative of the equivalence class.

theorem R.fromPoly_rep'_eq_ideal (q : ℕ) (n : ℕ) (a : Polynomial (ZMod q)) : ∃ i ∈ Ideal.span {f q n}, R.representative' q n (R.fromPoly a) = a + i

Characterization theorem for any potential representative (in terms of ideals). For an a : (ZMod q)[X], the representative of its equivalence class is just a + i for some i ∈ (Ideal.span {f q n}).

theorem R.exists_representative_fromPoly_eq_mul_add (q : ℕ) (n : ℕ) (a : Polynomial (ZMod q)) : ∃ (k : Polynomial (ZMod q)), R.representative' q n (R.fromPoly a) = k * f q n + a

Characterization theorem for any potential representative (in terms of elements). For an a : (ZMod q)[X], the representative of its equivalence class is a concrete element of the form a + k * (f q n) for some k ∈ (ZMod q)[X].

theorem R.representatitive'_toFun_fromPoly_eq_element (q : ℕ) (n : ℕ) (a : Polynomial (ZMod q)) : ∃ (k : Polynomial (ZMod q)), R.representative' q n ((↑↑R.fromPoly).toFun a) = a + k * f q n

A theorem similar to R.fromPoly_rep'_eq_element but uses fromPoly.toFun to be more deterministic, as the toFun sometimes sneaks in due to coercions.

theorem R.representative'_zero_ideal (q : ℕ) (n : ℕ) : R.representative' q n 0 ∈ Ideal.span {f q n}

The representative of 0 wil live in the ideal of {f q n}. To show that such an element is a multiple of {f q n}, use Ideal.mem_span_singleton'

theorem R.representative'_zero_elem (q : ℕ) (n : ℕ) : ∃ (k : Polynomial (ZMod q)), R.representative' q n 0 = k * f q n

The representatiatve of 0 is a multiple of f q n.

theorem neg_modByMonic (q : ℕ) (p : Polynomial (ZMod q)) (mod : Polynomial (ZMod q)) : -p %ₘ mod = -(p %ₘ mod)

pushing and pulling negation through mod

@[simp]

theorem sub_modByMonic (q : ℕ) (a : Polynomial (ZMod q)) (b : Polynomial (ZMod q)) (mod : Polynomial (ZMod q)) : (a - b) %ₘ mod = a %ₘ mod - b %ₘ mod

%ₘ is a subtraction homomorphism (obviously)

theorem R.representative_zero (q : ℕ) (n : ℕ) [Fact (q > 1)] : R.representative q n 0 = 0

Representative of (0 : R) is (0 : Z/qZ[X])

theorem R.representative_fromPoly_toFun (q : ℕ) (n : ℕ) [Fact (q > 1)] (a : Polynomial (ZMod q)) : R.representative q n ((↑↑R.fromPoly).toFun a) = a %ₘ f q n

Characterization theorem for the representative. Taking the representative of the equivalence class of a polynomial a : (ZMod q)[X] is the same as taking the remainder of a modulo f q n.

theorem R.representative_fromPoly (q : ℕ) (n : ℕ) [Fact (q > 1)] (a : Polynomial (ZMod q)) : R.representative q n (R.fromPoly a) = a %ₘ f q n

@[simp]

theorem R.representative_add (q : ℕ) (n : ℕ) [Fact (q > 1)] (a : R q n) (b : R q n) : R.representative q n (a + b) = R.representative q n a + R.representative q n b

Representative is an additive homomorphism

@[simp]

theorem R.representative_mul (q : ℕ) (n : ℕ) [Fact (q > 1)] (a : R q n) (b : R q n) : R.representative q n (a * b) = R.representative q n a * R.representative q n b %ₘ f q n

Representative is an multiplicative homomorphism upto modulo

@[simp]

theorem R.representative_fromPoly_eq (q : ℕ) (n : ℕ) [Fact (q > 1)] (x : Polynomial (ZMod q)) (DEGREE : x.degree < (f q n).degree) : R.representative q n (R.fromPoly x) = x

Another characterization of the representative: if the degree of x is less than that of (f q n), then we recover the same polynomial.

theorem R.rep_degree_lt_n (q : ℕ) (n : ℕ) [Fact (q > 1)] (a : R q n) : (R.representative q n a).degree < 2 ^ n

The representative of a : R q n is the (unique) reperesntative with degree < 2^n.

theorem R.representative_degree_lt_f_degree (q : ℕ) (n : ℕ) [Fact (q > 1)] (a : R q n) : (R.representative q n a).degree < (f q n).degree

The representative a : R q n is the (unique) representative with degree less than degree of f.

noncomputable def R.repLength {q : ℕ} {n : ℕ} (a : R q n) : ℕ

Equations

• a.repLength = match (R.representative q n a).degree with | none => 0 | some d => d + 1

theorem R.repLength_leq_representative_degree_plus_1 {q : ℕ} {n : ℕ} (a : R q n) : a.repLength ≤ (R.representative q n a).natDegree + 1

theorem R.repLength_lt_n_plus_1 {q : ℕ} {n : ℕ} [Fact (q > 1)] (a : R q n) : a.repLength < 2 ^ n + 1

noncomputable def R.coeff {q : ℕ} {n : ℕ} (a : R q n) (i : ℕ) : ZMod q

This function gets the ith coefficient of the polynomial representative (with degree < 2^n) of an element a : R q n. Note that this is not invariant under the choice of representative.

Equations

• a.coeff i = (R.representative q n a).coeff i

noncomputable def R.monomial {q : ℕ} {n : ℕ} (c : ZMod q) (i : ℕ) : R q n

R.monomial i c is the equivalence class of the monomial c * X^i in R q n.

Equations

• R.monomial c i = R.fromPoly ((Polynomial.monomial i) c)

noncomputable def R.slice {q : ℕ} {n : ℕ} (a : R q n) (startIdx : ℕ) (endIdx : ℕ) : R q n

Given an equivalence class of polynomials a : R q n with representative p = p_0 + p_1 X + ... + p_{2^n - 1} X^{2^n - 1}, R.slice a startIdx endIdx yields the equivalence class of the polynomial `p_{startIdx}*X^{startIdx} + p_{startIdx + 1} X^{startIdx + 1} + ... + p_{endIdx

• 1} X^{endIdx - 1}` Note that this is not invariant under the choice of representative.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def R.leadingTerm {q : ℕ} {n : ℕ} (a : R q n) : R q n

Equations

• a.leadingTerm = match (R.representative q n a).degree with | none => 0 | some deg => R.monomial (a.coeff deg) deg

noncomputable def R.fromTensor {q : ℕ} {n : ℕ} (coeffs : List ℤ) : R q n

Equations

• R.fromTensor coeffs = List.foldl (fun (res : R q n) (x : ℕ × ℤ) => match x with | (i, c) => res + R.monomial (↑c) i) 0 coeffs.enum

theorem R.fromTensor_snoc (q : ℕ) (n : ℕ) (c : ℤ) (cs : List ℤ) : R.fromTensor (cs ++ [c]) = R.fromTensor cs + R.monomial (↑c) cs.length

noncomputable def R.fromTensor' {q : ℕ} (coeffs : List ℤ) : Polynomial (ZMod q)

A definition of fromTensor that operates on Z/qZ[X], to provide a relationship between R and Z/qZ[X] as the polynomial in R is built.

Equations

• R.fromTensor' coeffs = List.foldl (fun (res : Polynomial (ZMod q)) (x : ℕ × ℤ) => match x with | (i, c) => res + (Polynomial.monomial i) ↑c) 0 coeffs.enum

theorem R.fromTensor_eq_fromTensor'_fromPoly_aux {q : ℕ} {n : ℕ} {k : ℕ} (coeffs : List ℤ) (rp : R q n) (p : Polynomial (ZMod q)) (H : R.fromPoly p = rp) : List.foldl (fun (res : R q n) (x : ℕ × ℤ) => match x with | (i, c) => res + R.monomial (↑c) i) rp (List.enumFrom k coeffs) = R.fromPoly (List.foldl (fun (res : Polynomial (ZMod q)) (x : ℕ × ℤ) => match x with | (i, c) => res + (Polynomial.monomial i) ↑c) p (List.enumFrom k coeffs))

theorem R.fromTensor_eq_fromTensor'_fromPoly {q : ℕ} {n : ℕ} [Fact (q > 1)] {coeffs : List ℤ} : R.fromTensor coeffs = R.fromPoly (R.fromTensor' coeffs)

fromTensor = R.fromPoly ∘ fromTensor'. This permits reasoning about fromTensor directly on the polynomial ring.

noncomputable def R.fromTensorFinsupp (q : ℕ) (coeffs : List ℤ) : Polynomial (ZMod q)

an equivalent implementation of fromTensor that uses Finsupp to enable reasoning about values using mathlib's notions of support, coefficients, etc.

Equations

• R.fromTensorFinsupp q coeffs = { toFinsupp := (List.map Int.cast coeffs).toFinsupp }

theorem Polynomial.degree_toFinsupp {M : Type u_1} [Semiring M] [DecidableEq M] (xs : List M) : { toFinsupp := xs.toFinsupp }.degree ≤ ↑xs.length

theorem R.fromTensorFinsupp_degree (q : ℕ) (coeffs : List ℤ) : (R.fromTensorFinsupp q coeffs).degree ≤ ↑coeffs.length

degree of fromTensorFinsupp is at most the length of the coefficient list.

theorem R.fromTensorFinsupp_coeffs {q : ℕ} {i : ℕ} (coeffs : List ℤ) : (R.fromTensorFinsupp q coeffs).coeff i = ↑(coeffs.getD i 0)

the ith coefficient of fromTensorFinsupp is a coercion of the 'coeffs' into the right list.

theorem R.fromTensorFinsupp_concat_finsupp {q : ℕ} (c : ℤ) (cs : List ℤ) : R.fromTensorFinsupp q (cs ++ [c]) = R.fromTensorFinsupp q cs + { toFinsupp := Finsupp.single cs.length ↑c }

concatenating into a fromTensorFinsupp is the same as adding a ⟨Finsupp.single⟩.

theorem R.fromTensorFinsupp_concat_monomial {q : ℕ} (c : ℤ) (cs : List ℤ) : R.fromTensorFinsupp q (cs ++ [c]) = R.fromTensorFinsupp q cs + (Polynomial.monomial cs.length) ↑c

concatenating into a fromTensorFinsupp is the same as adding a monomial.

theorem R.fromTensor_eq_fromTensorFinsupp_fromPoly {q : ℕ} {n : ℕ} {coeffs : List ℤ} : R.fromTensor coeffs = R.fromPoly (R.fromTensorFinsupp q coeffs)

show that fromTensor is the same as fromPoly ∘ fromTensorFinsupp.

theorem coeff_modByMonic_degree_lt_f {q : ℕ} {n : ℕ} [Fact (q > 1)] {i : ℕ} (p : Polynomial (ZMod q)) (DEGREE : p.degree < (f q n).degree) : (p %ₘ f q n).coeff i = p.coeff i

coeff (p % f) = coeff p if the degree of p is less than the degree of f.

@[simp]

theorem R.coeff_fromPoly {q : ℕ} {n : ℕ} [Fact (q > 1)] (p : Polynomial (ZMod q)) : (R.fromPoly p).coeff = (p %ₘ f q n).coeff

The coefficient of fromPoly p is the coefficient of p modulo f q n.

theorem R.coeff_fromTensor {q : ℕ} {n : ℕ} [Fact (q > 1)] {i : ℕ} (tensor : List ℤ) (htensorlen : tensor.length < 2 ^ n) : (R.fromTensor tensor).coeff i = ↑(tensor.getD i 0)

The coefficient of fromTensor is the same as the values available in the tensor input.

theorem R.representative_fromTensor_eq_fromTensor' {q : ℕ} {n : ℕ} [Fact (q > 1)] (tensor : List ℤ) : R.representative q n (R.fromTensor tensor) = R.representative' q n ((Ideal.Quotient.mk (Ideal.span {f q n})) (R.fromTensor' tensor)) %ₘ f q n

noncomputable def R.toTensor {q : ℕ} {n : ℕ} (a : R q n) : List ℤ

Converts an element of R into a tensor (modeled as a List Int) with the representatives of the coefficients of the representative. The length of the list is the degree of the representative + 1.

Equations

• a.toTensor = List.map (fun (i : ℕ) => ZMod.toInt q (a.coeff i)) (List.range a.repLength)

theorem R.toTensor_length {q : ℕ} {n : ℕ} (a : R q n) : a.toTensor.length = a.repLength

The length of the tensor R.toTensor a equals a.repLength

noncomputable def R.toTensor' {q : ℕ} {n : ℕ} (a : R q n) : List ℤ

Converts an element of R into a tensor (modeled as a List Int) with the representatives of the coefficients of the representative. The length of the list is the degree of the generator polynomial f + 1.

Equations

• a.toTensor' = a.toTensor ++ List.replicate (2 ^ n - a.toTensor.length + 1) 0

def trimTensor (tensor : List ℤ) : List ℤ

Equations

• trimTensor tensor = (List.dropWhile (fun (x : ℤ) => decide (x = 0)) tensor.reverse).reverse

inductive Ty (q : ℕ) (n : ℕ) : Type

We define the base type of the representation, which encodes both natural numbers and elements in the ring R q n (which in FHE are sometimes called 'polynomials' in allusion to R.representative).

In this context, `Tensor is a 1-D tensor, which we model here as a list of integers.

• index: {q n : ℕ} → Ty q n
• integer: {q n : ℕ} → Ty q n
• tensor: {q n : ℕ} → Ty q n
• polynomialLike: {q n : ℕ} → Ty q n

instance instDecidableEqTy : {q n : ℕ} → DecidableEq (Ty q n)

Equations

• instDecidableEqTy = decEqTy✝

instance instReprTy : {q n : ℕ} → Repr (Ty q n)

Equations

• instReprTy = { reprPrec := reprTy✝ }

instance instInhabitedTy {q : ℕ} {n : ℕ} : Inhabited (Ty q n)

Equations

• instInhabitedTy = { default := Ty.index }

instance instTyDenoteTy {q : ℕ} {n : ℕ} : TyDenote (Ty q n)

Equations

• instTyDenoteTy = { toType := fun (x : Ty q n) => match x with | Ty.index => ℕ | Ty.integer => ℤ | Ty.tensor => List ℤ | Ty.polynomialLike => R q n }

inductive Op (q : ℕ) (n : ℕ) : Type

The operation type of the Poly dialect. Operations are parametrized by the two parameters p and n that characterize the ring R q n. We parametrize the entire type by these since it makes no sense to mix operations in different rings.

• add: {q n : ℕ} → Op q n
• sub: {q n : ℕ} → Op q n
• mul: {q n : ℕ} → Op q n
• mul_constant: {q n : ℕ} → Op q n
• leading_term: {q n : ℕ} → Op q n
• monomial: {q n : ℕ} → Op q n
• monomial_mul: {q n : ℕ} → Op q n
• from_tensor: {q n : ℕ} → Op q n
• to_tensor: {q n : ℕ} → Op q n
• const: {q n : ℕ} → R q n → Op q n
• const_int: {q n : ℕ} → ℤ → Op q n
• const_idx: {q n : ℕ} → ℕ → Op q n

@[reducible, inline]

abbrev FHE (q : ℕ) (n : ℕ) [Fact (q > 1)] : Dialect

FHE is the dialect for fully homomorphic encryption

Equations

• FHE q n = { Op := Op q n, Ty := Ty q n, m := Id }

@[reducible]

def Op.sig {q : ℕ} {n : ℕ} : Op q n → List (Ty q n)

Equations

• Op.add.sig = [Ty.polynomialLike, Ty.polynomialLike]
• Op.sub.sig = [Ty.polynomialLike, Ty.polynomialLike]
• Op.mul.sig = [Ty.polynomialLike, Ty.polynomialLike]
• Op.mul_constant.sig = [Ty.polynomialLike, Ty.integer]
• Op.leading_term.sig = [Ty.polynomialLike]
• Op.monomial.sig = [Ty.integer, Ty.index]
• Op.monomial_mul.sig = [Ty.polynomialLike, Ty.index]
• Op.from_tensor.sig = [Ty.tensor]
• Op.to_tensor.sig = [Ty.polynomialLike]
• (Op.const c).sig = []
• (Op.const_int c).sig = []
• (Op.const_idx i).sig = []

@[reducible]

def Op.outTy {q : ℕ} {n : ℕ} : Op q n → Ty q n

Equations

• Op.add.outTy = Ty.polynomialLike
• Op.sub.outTy = Ty.polynomialLike
• Op.mul.outTy = Ty.polynomialLike
• Op.mul_constant.outTy = Ty.polynomialLike
• Op.leading_term.outTy = Ty.polynomialLike
• Op.monomial.outTy = Ty.polynomialLike
• Op.monomial_mul.outTy = Ty.polynomialLike
• Op.from_tensor.outTy = Ty.polynomialLike
• (Op.const c).outTy = Ty.polynomialLike
• Op.to_tensor.outTy = Ty.tensor
• (Op.const_int c).outTy = Ty.integer
• (Op.const_idx i).outTy = Ty.index

@[reducible]

def Op.signature {q : ℕ} {n : ℕ} : Op q n → Signature (Ty q n)

Equations

• o.signature = { sig := o.sig, regSig := [], outTy := o.outTy, effectKind := EffectKind.pure }

instance instDialectSignatureFHE {q : ℕ} [Fact (q > 1)] {n : ℕ} : DialectSignature (FHE q n)

Equations

• instDialectSignatureFHE = { signature := Op.signature }

noncomputable instance instDialectDenoteFHE {q : ℕ} [Fact (q > 1)] {n : ℕ} : DialectDenote (FHE q n)

Equations

• One or more equations did not get rendered due to their size.