Functional Pearl: Folding Polynomials of Polynomials

Abstract

Polynomials are a central concept to many branches in mathematics and computer science. In particular, manipulation of polynomial expressions can be used to model a wide variety of computation. In this paper, we consider a simple recursive construction of multivariate polynomials over a base ring such as the integers or a (finite) field. We show that this construction allows inductive implementation of polynomial operations such as arithmetic, evaluation, substitution, etc. Furthermore, we can transform a polynomial expression into in a sequence of arithmetic expressions in the base ring and prove the correctness of this transformation in Agda. Combined with our recursive construction, this allows for compiling polynomial expressions over a tower of extension fields into scalar expressions over the ground field, for example. Such a technique is not only interesting in its own right but also finds plentiful application in research areas such as cryptography.

1 Introduction

A univariate polynomial over a base ring R is a finite sum of the form

$$\begin{aligned} a_nX^n+a_{n-1}X^{n-1}+\cdots +a_0, \end{aligned}$$

where $a_i\in R$ are the coefficients, and X is called an indeterminate. The set of univariate polynomials over R forms a ring, denoted as R[X]. We can allow two or more indeterminates $X_1,X_2,\ldots ,X_m$ and thus arrive at a multivariate polynomial, a finite sum of the form

$$\begin{aligned} \sum _{i}a_iX_1^{e_1^{(i)}}X_2^{e_2^{(i)}}\cdots X_m^{e_m^{(i)}}, \end{aligned}$$

where $a_i\in R$ are the coefficients, and the nonnegative integers $e_j^{(i)}$ are the exponents. The set of m-variate polynomials over R, denoted as $R[X_1,X_2,\ldots ,X_m]$, also forms a ring, referred to as a ring of polynomials.

Polynomials are a central concept to many branches in mathematics and computer science. In particular, manipulation of polynomial expressions can be used to model a wide variety of computation. For example, every element of an algebraic extension field F over a base field K can be identified as a polynomial over K, e.g., cf. Theorem 1.6, Chap. 5 of the (standard) textbook by Hungerford [6]. Addition in F is simply polynomial addition over K, whereas multiplication in F is polynomial multiplication modulo the defining polynomial of F over K. Let us use the familiar case of the complex numbers over the real numbers as a concrete example. The complex numbers can be obtained by adjoining to the real numbers a root i of the polynomial $X^2+1$. In this case, every complex number can be identified as a polynomial $a+bi$ for a, b real. The addition of $a_1+b_1i$ and $a_2+b_2i$ is simply $(a_1+a_2)+(b_1+b_2)i$, whereas the multiplication, $(a_1+b_1i)(a_2+b_2i)\bmod i^2+1=(a_1a_2-b_1b_2)+(a_1b_2+a_2b_1)i$.

In addition to arithmetic in an algebraic extension field, manipulation of polynomial expressions also finds rich application in cryptography in particular. A wide variety of cryptosystems can be implemented using polynomial expressions over a finite field or $\mathbb Z/n\mathbb Z$, the ring of integers modulo n. In elliptic curve cryptography [8], for example, we use the group structure of certain elliptic curves over finite fields to do cryptography, and the group laws are often given in polynomial expressions over finite fields. Another example is certain classes of post-quantum cryptosystems, i.e., those expected to survive large quantum computers’ attack. Among the most promising candidates, we have multivariate cryptosystems [3] and several particularly efficient lattice-based cryptosystems [4, 7], for which encryption and decryption operations can be carried out using polynomial expressions over finite fields or $\mathbb Z/n\mathbb Z$.

This pearl is initially motivated by our research in cryptography, where we often have to deal with multivariate polynomials over various base rings, as exemplified above. We also need to transform a polynomial expression into a sequence of arithmetic expressions over its base ring. This is useful for, e.g., software implementation of cryptosystems on microprocessors with no native hardware support for arithmetic operations with polynomials or integers of cryptographic sizes, which typically range from a few hundreds to a few thousands of bits. Again using multiplication of two complex numbers as an example, we would need a sequence of real arithmetic expressions for implementing $z=z_r+iz_i=(x_r+ix_i)\times (y_r+iy_i)=xy$:

$$\begin{aligned} t_1&\leftarrow x_r\times y_r ; \\ t_2&\leftarrow x_i\times y_i ; \\ t_3&\leftarrow x_r\times y_i ; \\ t_4&\leftarrow x_i\times y_r ; \\ z_r&\leftarrow t_1-t_2 ; \\ z_i&\leftarrow t_3+t_4 \text{. } \end{aligned}$$

Furthermore, we would like to have a precision that exceeds what our hardware can natively support. For example, let us assume that we have a machine with native support for an integer type $-R<x<R$. In this case, we split each variable $\zeta$ into a low part plus a high part: $\zeta =\zeta ^{(0)}+R\zeta ^{(1)}$, $-R<\zeta ^{(0)},\zeta ^{(1)}<R$. Now let us assume that our machine has a multiplication instruction $(c^{(0)},c^{(1)})\leftarrow a\times b$ such that $-R<a,b,c^{(0)},c^{(1)}<R$ and $ab=c^{(0)}+Rc^{(1)}$. For simplicity, let us further assume that our machine has n-ary addition instructions for $n=2,3,4$: $(c^{(0)},c^{(1)})\leftarrow a_1+\cdots +a_n$ such that $-R<a_1,\ldots ,a_n,c^{(0)},c^{(1)}<R$ and $a_1+\cdots +a_n=c^{(0)}+Rc^{(1)}$. We can then have a suboptimal yet straightforward implementation of, say, $t_1=t_1^{(0)}+Rt_1^{(1)}+R^2t_1^{(2)}+R^3t_1^{(3)}=(x_r^{(0)}+Rx_r^{(1)})\times (y_r^{(0)}+Ry_r^{(1)})=x_r\times y_r$ as follows.

$$\begin{aligned} \begin{array}{llll} (t_1^{(0)},s_1^{(1)}) &{}\leftarrow x_r^{(0)}\times y_r^{(0)}; &{}&{}// t_1^{(0)}+Rs_1^{(1)} \\ (s_2^{(0)},s_2^{(1)}) &{}\leftarrow x_r^{(0)}\times y_r^{(1)}; &{}&{}// Rs_2^{(0)}+R^2s_2^{(1)} \\ (s_3^{(0)},s_3^{(1)}) &{}\leftarrow x_r^{(1)}\times y_r^{(0)}; &{}&{}// Rs_3^{(0)}+R^2s_3^{(1)} \\ (s_4^{(0)},s_4^{(1)}) &{} \leftarrow x_r^{(1)}\times y_r^{(1)}; &{}&{}// R^2s_4^{(0)}+R^3s_4^{(1)} \\ (t_1^{(1)},s_5^{(1)}) &{} \leftarrow s_1^{(1)}+s_2^{(0)}+s_3^{(0)}; &{}&{}// Rt_1^{(1)}+R^2s_5^{(1)} \\ (t_1^{(2)},s_6^{(1)}) &{} \leftarrow s_2^{(1)}+s_3^{(1)}+s_4^{(0)}+s_5^{(1)}; &{}&{}// R^2t_1^{(2)}+R^3s_6^{(1)} \\ (t_1^{(3)},\_) &{} \leftarrow s_4^{(1)}+s_6^{(1)}\text{. } &{}&{}// R^3t_1^{(3)} \end{array} \end{aligned}$$

It might be surprising that, with the advance of compiler technology today, such programs are still mostly coded and optimized manually, sometimes in assembly language, for maximal efficiency. Naturally, we would like to automate this process as much as possible. Furthermore, with such security-critical applications, we would like to have machine-verified proofs that the transformation and optimizations are correct.

In attempting toward this goal, we have come up with this pearl. It is not yet practical but, we think, is neat and worth documenting. A key observation is that there is an isomorphism between multivariate polynomial ring $R[X_1,X_2\ldots ,X_m]$ and univariate polynomial ring $S[X_m]$ over the base ring $S=R[X_1,X_2,\ldots ,X_{m-1}]$, cf. Corollary 5.7, Chap. 3 of Hungerford [6]. This allows us to define a datatype $\mathsf {Poly}$ for univariate polynomials, and reuse it inductively to define multivariate polynomials — an $\mathsf {n}$-variate polynomial can be represented by $\mathsf {Poly}^{\mathsf {n}}$ ($\mathsf {Poly}$ applied $\mathsf {n}$ times). Most operations on the polynomials can be defined either in terms of the fold induced by $\mathsf {Poly}$, or by induction on $\mathsf {n}$, hence the title.

We explore the use of $\mathsf {Poly}^{\mathsf {n}}$ and its various implications in depth in Sect. 2. Then in Sect. 3, we present implementations of common polynomial operations such as evaluation, substitution, etc. We pay special attention to an operation $\mathsf {expand}$ and prove its correctness, since it is essential in transforming polynomial into scalar expressions. In Sect. 4, we show how to compile a polynomial function into an assembly program that computes it. We present a simple compilation, also defined in terms of fold, and prove its correctness, while leaving further optimization to future work. The formulation in this pearl have been implemented in both Haskell and Agda [9], the latter also used to verify our proofs. The code is available on line at https://github.com/petercommand/ExtFieldComp.

2 Univariate and Multivariate Polynomials

In this section, we present our representation for univariate and multivariate polynomials, as well as their semantics. The following Agda datatype denotes a univariate polynomial whose coefficients are of type $\mathsf {A}$:¹

where $\mathsf {Ind}$ denotes the indeterminate, $\mathsf {Lit}$ denotes a constant (of type $\mathsf {A}$), while $\mathsf {({:\!\!+})}$ and $\mathsf {(:\!\!\times )}$ respectively denote addition and multiplication. A polynomial $2 x^2 + 3x + 1$ can be represented by the following expression of type $\mathsf {Poly}$ $\mathbb {Z}$:

Notice that the type parameter $\mathsf {A}$ is abstracted over the type of coefficients. This allows us to represent polynomials whose coefficients have non-simple types — in particular, polynomials whose coefficients are themselves polynomials. Do not confuse this with the more conventional representation of arithmetic expressions:

where the literals are usually assigned a fixed type (in this example, $\mathsf {Int}$), and the type parameter is abstracted over variables $\mathsf {Var}$.

2.1 Univariate Polynomial and Its Semantics

In the categorical style outlined by Bird and de Moor [1], every regular datatype gives rise to a fold, also called a catamorphism. The type $\mathsf {Poly}$ induces a fold that, conventionally, takes four arguments, each replacing one of its four constructors. To facilitate our discussion later, we group the last two arguments together. The fold for $\mathsf {Poly}$ is thus given by:

where arguments $\mathsf {x}$, $\mathsf {f}$, $(\oplus )$, and $(\otimes )$ respectively replace constructors $\mathsf {Ind}$, $\mathsf {Lit}$, (:+), and $\mathsf {({:\!\!\times })}$.

Evaluation. To evaluate a polynomial of type $\mathsf {Poly}\;\mathsf {A}$, we have to know how to perform arithmetic operations for type $\mathsf {A}$. Define

the intention is that the tuple $\mathsf {Ring}\;\mathsf {A}$ defines addition, multiplication, zero, one, and negation for $\mathsf {A}$ (addition and multiplication are grouped together, for our convenience later). In our Haskell implementation, $\mathsf {Ring}$ is a type class for types whose addition and multiplication are defined. It can usually be inferred what instance of $\mathsf {Ring}$ to use. When proving properties about $\mathsf {foldP}$, however, it is clearer to make the construction of $\mathsf {Ring}$ instances explicit.

With the presence of $\mathsf {Ind}$, the semantics of $\mathsf {Poly}\;\mathsf {A}$ should be $\mathsf {A}\;\rightarrow \;\mathsf {A}$ — a function that takes the value of the indeterminate and returns a value. We define the following operation that lifts pointwise the addition and multiplication of some type $\mathsf {B}$ to $\mathsf {A}\; \rightarrow \;\mathsf {B}$:

where $\mathsf {const}\;\mathsf {x}\;\mathsf {y}\;\mathrel {=}\;\mathsf {x}$. The semantics of a univariate polynomial is thus given by:

where $\mathsf {id}\;\mathsf {x}\;\mathrel {=}\;\mathsf {x}$ and $\mathsf {fst}$ retrieves the left component of a pair.

2.2 Bivariate Polynomials

To represent polynomials with two indeterminates, one might extend $\mathsf {Poly}$ with a constructor $\mathsf {Ind'}$ in addition to $\mathsf {Ind}$. It turns out to be unnecessary — it is known that the bivariate polynomial ring R[X, Y] is isomorphic to R[X][Y] (modulo the operation $\mathsf {litDist}$, to be defined later). That is, a polynomial over base ring $\mathsf {A}$ with two indeterminates can be represented by $\mathsf {Poly}\;(\mathsf {Poly}\;\mathsf {A})$.

To understand the isomorphism, consider the following expression:

Note that to represent a literal $\mathsf {3}$, we have to write $\mathsf {Lit}\;(\mathsf {Lit}\;\mathsf {3})$, since the first $\mathsf {Lit}$ takes a $\mathsf {Poly}\;\mathsf {\mathbb {Z}}$ as its argument. To evaluate $\mathsf {e}$ using $\mathsf {sem}_{1}$, we have to define $\mathsf {Ring}\;(\mathsf {Poly}\;\mathsf {\mathbb {Z}})$. A natural choice is to connect two expressions using corresponding constructors:

With $\mathsf {ringP}$ defined, $\mathsf {sem}_{1}\;(\mathsf {ringP}\;\mathsf {r})\;\mathsf {e}$ has type $\mathsf {Poly}\;\mathsf {A}\;\mathsf {\rightarrow }\;\mathsf {Poly}\;\mathsf {A}$. Evaluating, for example $\mathsf {sem}_{1}\;(\mathsf {ringP}\;\mathsf {r})\;\mathsf {e}\;(\mathsf {Ind}\;{:\!\!+}\;\mathsf {Lit}\;\mathsf {1})$, yields

Note that $\mathsf {Lit}\;\mathsf {Ind}$ in $\mathsf {e}$ is replaced by the argument $\mathsf {Ind}\;{:\!\!+}\;\mathsf {Lit}\;\mathsf {1}$. Furthermore, one layer of $\mathsf {Lit}$ is removed, thus both $\mathsf {Lit}\;\mathsf {3}$ and $\mathsf {Ind}\;{:\!\!+}\;\mathsf {Lit}\;\mathsf {4}$ are exposed to the outermost level. The expression $\mathsf {e'}$ may then be evaluated by $\mathsf {sem}_{1}\;\mathsf {rng\mathbb {Z}}$, where $\mathsf {rng\mathbb {Z}}\;\!\!:\!\!\;\mathsf {Ring}\;\mathsf {\mathbb {Z}}$. The result is a natural number. In general, the function $\mathsf {sem}_{2}$ that evaluates $\mathsf {Poly}\;(\mathsf {Poly}\;\mathsf {A})$ can be defined by:

This is how $\mathsf {Poly}\;(\mathsf {Poly}\;\mathbb {{Z}})$ simulates bivariate polynomials: the two indeterminates are respectively represented by $\mathsf {Ind}$ and $\mathsf {Lit}\;\mathsf {Ind}$. During evaluation, $\mathsf {Ind}$ can be instantiated to an expression $\mathsf {arg}$ of type $\mathsf {Poly}\;\mathbb {Z}$, while $\mathsf {Lit}\;\mathsf {Ind}$ can be instantiated to a $\mathbb {Z}$. If $\mathsf {arg}$ contains $\mathsf {Ind}$, it refers to the next indeterminate.

What about expressions like $\mathsf {Lit}\;(\mathsf {Ind}\;{:\!\!+}\;\mathsf {Lit}\;\mathsf {4})$? One can see that its semantics is the same as $\mathsf {Lit}\;\mathsf {Ind}\;{:\!\!+}\;\mathsf {Lit}\;(\mathsf {Lit}\;\mathsf {4})$, the expression we get by pushing $\mathsf {Lit}$ to the leaves. In general, define the following function:

The function traverses through the given expression and, upon encountering a subtree $\mathsf {Lit}\;\mathsf {e}$, lifts $\mathsf {e}$ to $\mathsf {Poly}\;(\mathsf {Poly}\;\mathsf {A})$ while distributing $\mathsf {Lit}$ inwards $\mathsf {e}$. We can prove the following theorem:

Theorem 1

For all $\mathsf {e}\;\!\!:\!\!\;\mathsf {Poly}\;(\mathsf {Poly}\;\mathsf {A})$ and $\mathsf {r}\;\!\!:\!\!\;\mathsf {Ring}\;\mathsf {A}$, we have $\mathsf {sem}_{2}\;\mathsf {r}(\mathsf {litDist}\;\mathsf {e})\;\mathrel {=}\;\mathsf {sem}_{2}\;\mathsf {r}\;\mathsf {e}$.

2.3 Multivariate Polynomials

In general, as we have mentioned in Sect. 1, the multivariate polynomial $R[X_1,X_2\ldots ,X_m]$ is isomorphic to univariate polynomial ring $S[X_m]$ over the base ring $S=R[X_1,X_2,\ldots ,X_{m-1}]$ (modulo the distribution law of $\mathsf {Lit}$). That is, a polynomial over $\mathsf {A}$ with $\mathsf {n}$ indeterminates can be represented by $\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A}$, defined by

To define the semantics of $\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A}$, recall that, among its $\mathsf {n}$ indeterminates, the outermost indeterminate shall be instantiated to an expression of type $\mathsf {Poly}^{\mathsf {n-1}}\;\mathsf {A}$, the next indeterminate to $\mathsf {Poly}^{\mathsf {n-2}}\;\mathsf {A}$..., and the inner most indeterminate to $\mathsf {A}$, before yielding a value of type $\mathsf {A}$. Define

that is, $\mathsf {DChain}\;\mathsf {A}\;\mathsf {n}$ (the name standing for a “descending chain”) is a list of $\mathsf {n}$ elements, with the first having type $\mathsf {Poly}^{\mathsf {n-1}}\;\mathsf {A}$, the second $\mathsf {Poly}^{\mathsf {n-2}}\;\mathsf {A}$, and so on. The type $\mathsf {\top }$ denotes the “unit” type, inhabited by exactly one term $\mathsf {tt}$.

Given an implementation of $\mathsf {Ring}\;\mathsf {A}$, the semantics of $\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A}$ is a function $\mathsf {DChain}\;\mathsf {A}\;\mathsf {n}\;\!\rightarrow \!\;\mathsf {A}$, defined inductively as below:

where $\mathsf {ringP}^{\star }$ delivers the $\mathsf {Ring}\;(\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A})$ instance for all $\mathsf {n}$:

For $\mathsf {n}\;\mathsf {:=}\;\mathsf {2}$ and $\mathsf {3}$, for example, $\mathsf {sem}\;\mathsf {r}\;\mathsf {n}$ expands to:

Essentially, $\mathsf {sem}\;\mathsf {r}\;\mathsf {n}$ is $\mathsf {n}$-fold composition of $\mathsf {sem}_{1}\;(\mathsf {ringP}^i\;\mathsf {r})$, each interpreting one level of the given expression.

3 Operations on Polynomials

Having defined a representation for multivariate polynomials, we ought to demonstrate that this representation is feasible — that we can define most of the operations we want. In fact, it turns that most of them can be defined either in terms of $\mathsf {foldP}$ or by induction over the number of iterations $\mathsf {Poly}$ is applied.

3.1 Rotation

The first operation swaps the two outermost indeterminates of a $\mathsf {Poly}^{2}\;\mathsf {A}$, using $\mathsf {foldP}$. This function witnesses the isomorphism between $R[X_1,\ldots ,X_{m-1}][X_m]$ and $R[X_m,X_1,\ldots ,X_{m-2}][X_{m-1}]$. It is instructive comparing it with $\mathsf {litDist}$.

In $\mathsf {rotaPoly}_{2}$, the outermost $\mathsf {Ind}$ is replaced by $\mathsf {Lit}\;\mathsf {Ind}$. When encountering $\mathsf {Lit}\;\mathsf {e}$, the inner $\mathsf {e}$ is lifted to $\mathsf {Poly}^{2}\;\mathsf {A}$. The $\mathsf {Ind}$ inside $\mathsf {e}$ remains $\mathsf {Ind}$, which becomes the outermost indeterminate after lifting. Note that both $\mathsf {litDist}$ and $\mathsf {rotaPoly}_{2}$ apply to $\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A}$ for all $\mathsf {n}\;\mathsf {\geqslant }\;\mathsf {2}$, since $\mathsf {A}$ can be instantiated to a polynomial as well.

Consider $\mathsf {Poly}^{\mathsf {3}}\;\mathsf {A}$, a polynomial with (at least) three indeterminates. To “rotate” the three indeterminates, that is, turn $\mathsf {Lit}^{\mathsf {2}}\;\mathsf {Ind}$ to $\mathsf {Lit}\;\mathsf {Ind}$, $\mathsf {Lit}\;\mathsf {Ind}$ to $\mathsf {Ind}$, and $\mathsf {Ind}$ to $\mathsf {Lit}^{\mathsf {2}}\;\mathsf {Ind}$, we can define:

where $\mathsf {fmap}$ is the usual “functorial map” function for $\mathsf {Poly}$:

The first $\mathsf {rotaPoly}_{2}$ swaps the two outer indeterminates, while $\mathsf {fmap}\;\mathsf {rotaPoly}_{2}$ swaps the inner two. To rotate the outermost four indeterminates of a $\mathsf {Poly}^{\mathsf {4}}\;\mathsf {A}$, we may define:

In general, the following function rotates the first $\mathsf {n}$ indeterminates of the given polynomial:

Note that in the actual code we need to convince Agda that $\mathsf {Poly}^{\mathsf {n}}\;(\mathsf {Poly}\;\mathsf {A})$ is the same type as $\mathsf {Poly}\;(\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A})$ and use $\mathsf {subst}$ to coerce between the two types. We omit those details for clarity.

Given $\mathsf {m}$ and $\mathsf {n}$, $\mathsf {rotaOuter}\;\mathsf {n}\;\mathsf {m}$ compose $\mathsf {rotaPoly}\;\mathsf {n}$ with itself $\mathsf {m}$ times. Therefore, the outermost $\mathsf {n}$ indeterminates are rotated $\mathsf {m}$ times. It will be handy in Sect. 3.2.

3.2 Substitution

Substitution is another operation that one would expect. Given an expression $\mathsf {e}$, how do we substitute, for each occurrence of $\mathsf {Ind}$, another expression $\mathsf {e'}$, using operations we have defined? Noticing that the type of $\mathsf {sem}_{1}$ can be instantiated to $\mathsf {Poly}^{\mathsf {2}}\;\mathsf {A}\;\mathsf {\rightarrow }\;\mathsf {Poly}\;\mathsf {A}\;\mathsf {\rightarrow }\;\mathsf {Poly}\;\mathsf {A}$, we may lift $\mathsf {e}$ to $\mathsf {Poly}^{\mathsf {2}}\;\mathsf {A}$ by wrapping it with $\mathsf {Lit}$, do a $\mathsf {rotaPoly}_{2}$ to swap the $\mathsf {Ind}$ in $\mathsf {e}$ to the outermost position, and use $\mathsf {sem}_{1}$ to perform the substitution:

What about $\mathsf {e}\;\!\!:\!\!\;\mathsf {Poly}^{2}\;\mathsf {A}$? We may lift it to $\mathsf {Poly}^{\mathsf {4}}\;\mathsf {A}$, perform two $\mathsf {rotaPoly}_{4}$ to expose its two indeterminates, before using $\mathsf {sem}_{2}$:

Consider the general case with substituting the $\mathsf {n}$ indeterminates in $\mathsf {e}\;\!\!:\!\!\;\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A}$ for $\mathsf {n}$ expressions, each of type $\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A}$. Let $\mathsf {Vec}\;\mathsf {B}\;\mathsf {n}$ be the type of vectors (lists of fixed lengths) of length $\mathsf {n}$. A general $\mathsf {substitute}$ can be defined by:

where $\mathsf {liftPoly}\;\mathsf {n}\;\mathsf {m}$ (with $\mathsf {n}\;\!\leqslant \;\!\mathsf {m}$) lifts a $\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A}$ to $\mathsf {Poly}^{\mathsf {m}}\;\mathsf {A}$ by applying $\mathsf {Lit}$; $\mathsf {rotaOuter}\;(\mathsf {n}\;\mathsf {+}\;\mathsf {n})\;\mathsf {n}$, as defined in Sect. 3.1, composes $\mathsf {rotaPoly}\;(\mathsf {n+n})$ with itself $\mathsf {n}$ times, thereby moving the $\mathsf {n}$ original indeterminates of $\mathsf {e}$ to outermost positions; the function $\mathsf {toDChain}\;\!\!:\!\!\;\mathsf {\forall }\;\{\mathsf {A}\}\;\mathsf {n}\;\!\rightarrow \!\;\mathsf {Vec}\;\mathsf {A}\;\mathsf {n}\;\!\rightarrow \!\;\mathsf {DChain}\;\mathsf {A}\;\mathsf {n}$ converts a vector to a descending chain, informally,

finally, $\mathsf {sem}$ performs the substitution. Again, the actual code needs additional proof terms (to convince Agda that $\mathsf {n}\;\!\leqslant \;\!\mathsf {n+n}$) and type coercion (between $\mathsf {Poly}^{\mathsf {n}}\;(\mathsf {Poly}^{\mathsf {m}}\;\mathsf {A})$ and $\mathsf {Poly}^{\mathsf {m}+\mathsf {n}}\;\mathsf {A}$), which are omitted here.

3.3 Expansion

Expansion is an operation we put specific emphasis on, since it is useful when implementing cryptosystems on microprocessors with no native hardware support for arithmetic operations with polynomials or integers of cryptographic sizes. Let us use a simple yet specific example for further exposition: the polynomial expression over complex numbers $(3 + 2i) x^2 + (2 + i)x + 1$ can be represented by $\mathsf {Poly}\;({\mathbb R}\;\mathsf {\times }\;{\mathbb R})$, whose semantics is a function $({\mathbb R}\;\mathsf {\times }\;{\mathbb R})\;\!\!\rightarrow \!\;\!({\mathbb R}\;\mathsf {\times }\;{\mathbb R})$. Let x be $x_1 + x_2 i$, the polynomial can be expanded as below:

$$\begin{aligned}&(3 + 2i)(x_1 + x_2 i)^2 + (2 + i)(x_1 + x_2 i) + 1 \\ =~&(3 x^2_1 - 4 x_1 x_2 - 3 x^2_2) + (2 x^2_1 + 6 x_1 x_2 - 2 x^2_2) i + (2 x_1 - x_2) + (x_1 + 2 x_2) i + 1\\ =~&(3 x^2_1 + 2 x_1 - 4 x_1 x_2 - x_2 - 3 x^2_2 + 1) + (2 x^2_1 + x_1 + 6 x_1 x_2 + 2 x_2 - 2x^2_2) i \text{. } \end{aligned}$$

That is, a univariate polynomial over pairs, $\mathsf {Poly}\;({\mathbb R}\;\mathsf {\times }\;{\mathbb R})$, can be expanded to $(\mathsf {Poly}^{2}\;{\mathbb R}\;\mathsf {\times }\;\mathsf {Poly}^{2}\;{\mathbb R})$, a pair of bivariate expressions. The expansion depends on the definitions of addition and multiplication of complex numbers.

It might turn out that ${\mathbb R}$ is represented by a fixed number of machine words: ${\mathbb R}\;\!\!\mathrel {=}\;\!\!\mathsf {Word}^{\mathsf {n}}$. As mentioned before, in cryptosystems $\mathsf {n}$ could be hundreds. To compute the value of the polynomial, $\mathsf {Poly}\;\mathsf {Word}^{\mathsf {n}}$ can be further expanded to $(\mathsf {Poly}^{\mathsf {n}}\;\mathsf {Word})^\mathsf {n}$, this time using arithmetic operations defined for $\mathsf {Word}$. Now that each polynomial is defined over $\mathsf {Word}$, whose arithmetic operations are natively supported, we may compile the expressions, in ways discussed in Sect. 4, into a sequence of operations in assembly language. We also note that the roles played by the indeterminates x and i are of fundamental difference: x might just represent the input of the computation modelled by the polynomial expression, which will be substituted by some values at runtime, whereas i intends to model some internal (algebraic) structures and is never substituted throughout the whole computation.

Currently, such conversion and compilation are typically done by hand. We define expansion in this section and compilation in the next, as well as proving their correctness.

In general, a univariate polynomial over $\mathsf {n}$-vectors, $\mathsf {Poly}\;(\mathsf {Vec}\;\mathsf {A}\;\mathsf {n})$, can be expanded to a $\mathsf {n}$-vector of $\mathsf {n}$-variate polynomial, $\mathsf {Vec}\;(\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A})\;\mathsf {n}$. To formally define expansion we need some helper functions. Firstly, $\mathsf {genInd}\;\mathsf {n}$ generates a vector $\mathsf {Ind}\;\mathsf {{:}{:}}\;\mathsf {Lit}\;\mathsf {Ind}\;\mathsf {{:}{:}}\;\mathsf {...}\;\mathsf {Lit}^{\mathsf {n-1}}\;\mathsf {Ind}\;\mathsf {{:}{:}}\;[\,]$. It corresponds to expanding x to $(x_1 , x_2)$ in the previous example.

Secondly, $\mathsf {liftVal}\;\!\!:\!\!\;\mathsf {\forall }\;\{\mathsf {A}\}\;\mathsf {n}\;\mathsf {\rightarrow }\;\mathsf {A}\;\mathsf {\rightarrow }\;\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A}$ lifts $\mathsf {A}$ to $\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A}$ by $\mathsf {n}$ applications of $\mathsf {Lit}$. The definition is routine.

Expansion can now be defined by:

For the $\mathsf {Ind}$ case, one indeterminant is expanded to $\mathsf {n}$ using $\mathsf {genInd}$. For the $\mathsf {Lit}\;\mathsf {xs}$ case, $\mathsf {xs}\;\!\!:\!\!\;\mathsf {Vec}\;\mathsf {A}\;\mathsf {n}$ can be lifted to $\mathsf {Vec}\;(\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A})\;\mathsf {n}$ by $\mathsf {map}\;(\mathsf {liftVal}\;\mathsf {n})$. For addition and multiplication, we let $\mathsf {rv}$ decide how to combine vectors of expressions.

The function $\mathsf {expand}$ alone does not say much — all the complex work is done in $\mathsf {rv}\;\!\!:\!\!\;\mathsf {Ring}\;(\mathsf {Vec}\;(\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A})\;\mathsf {n})$. To generate $\mathsf {rv}$, we define the type of operations that, given arithmetic operators for $\mathsf {A}$, define ring instance for vectors of $\mathsf {A}$:

For example, $\mathsf {rComplex}$ lifts arithmetic operations on $\mathsf {A}$ to that of complex numbers over $\mathsf {A}$:

To expand a polynomial of complex numbers $\mathsf {Poly}\;(\mathsf {Vec}\;\mathsf {A}\;\mathsf {2})$, $\mathsf {expand}$ demands an instance of $\mathsf {Ring}\;(\mathsf {Vec}\;(\mathsf {Poly}^{\mathsf {2}}\;\mathsf {A})\;\mathsf {2})$. One may thus call $\mathsf {expand}\;\mathsf {2}\;(\mathsf {rComplex}\;(\mathsf {ringP}^2\;\mathsf {r})$, where $\mathsf {r}\;\!\!:\!\!\;\mathsf {Ring}\;\mathsf {A}$. That is, we use $\mathsf {rComplex}$ to combine a pair of polynomials, designating $(({:\!\!+})\;\mathsf {,}\;({:\!\!\times }))$ as addition and multiplication.

Correctness. Intuitively, $\mathsf {expand}$ is correct if the expanded polynomial evaluates to the same value as that of the original. To formally state the property, we have to properly supply all the needed ingredients. Consider $\mathsf {e}\;\!\!:\!\!\;\mathsf {Poly}\;(\mathsf {Vec}\;\mathsf {A}\;\mathsf {n})$ — a polynomial whose coefficients are vectors of length $\mathsf {n}$. Let $\mathsf {r}\;\!\!:\!\!\;\mathsf {Ring}\;\mathsf {A}$ define arithmetic operators for $\mathsf {A}$, and let $\mathsf {ringVec}\;\!\!:\!\!\;\mathsf {RingVec}\;\mathsf {n}$ define how arithmetic operators for elements are lifted to vectors. We say that $\mathsf {expand}$ is correct if, for all $\mathsf {xs}\;\!\!:\!\!\;\mathsf {Vec}\;\mathsf {A}\;\mathsf {n}$:

$$\begin{aligned} \mathsf {sem}_{1}\;(\mathsf {ringVec}\;\mathsf {r})\;\mathsf {e}\;\mathsf {xs}\;\mathrel {=}~&\mathsf {map}\;(\lambda \;\mathsf {e}\;\mathsf {\rightarrow }\;\mathsf {sem}\;\mathsf {r}\;\mathsf {n}\;\mathsf {e}\;(\mathsf {toDChain}\;\mathsf {xs})) \nonumber \\&\qquad (\mathsf {expand}\;\mathsf {n}\;(\mathsf {ringVec}\;(\mathsf {ringP}^{\star }\;\mathsf {r}\;\mathsf {n}))\;\mathsf {e}) \text{. } \end{aligned}$$

(1)

On the lefthand side, $\mathsf {e}$ is evaluated by $\mathsf {sem}_{1}$, using operators supplied by $\mathsf {ringVec}\;\mathsf {r}$. The value of the single indeterminant is $\mathsf {xs}\,\!\!:\!\!\,\mathsf {Vec}\;\mathsf {A}\;\mathsf {n}$, and the result also has type $\mathsf {Vec}\;\mathsf {A}\;\mathsf {n}$. On the righthand side, $\mathsf {e}$ is expanded to $\mathsf {Vec}\;(\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A})\;\mathsf {n}$, for which we need an instance of $\mathsf {Ring}\;(\mathsf {Vec}\;(\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A})\;\mathsf {n})$, generated by $\mathsf {ringVec}\;(\mathsf {ringP}^{\star }\;\mathsf {r}\;\mathsf {n})$. Each polynomial in the vector is then evaluated individually by $\mathsf {sem}\;\mathsf {r}\;\mathsf {n}$. The function $\mathsf {toDChain}$ converts a vector to a descending chain. The $\mathsf {n}$ elements in $\mathsf {xs}$ thus substitutes the $\mathsf {n}$ indeterminants of the expanded polynomial.

Interestingly, it turns out that $\mathsf {expand}$ is correct if $\mathsf {ringVec}$ is polymorphic — that is, the way it computes vectors out of vectors depends only on the shape of its inputs, regardless of the type and values of their elements.

Theorem 2

For all $\mathsf {n}$, $\mathsf {e}\;\!\!:\!\!\;\mathsf {Poly}\;(\mathsf {Vec}\;\mathsf {A}\;\mathsf {n})$, $\mathsf {xs}\;\!\!:\!\!\;\mathsf {Vec}\;\mathsf {A}\;\mathsf {n}$, $\mathsf {r}\;\!\!:\!\!\;\mathsf {Ring}\;\mathsf {A}$, and $\mathsf {ringVec}\;\!\!:\!\!\;\mathsf {RingVec}$, property (1) holds if $\mathsf {ringVec}$ is polymorphic.

Proof

Induction on $\mathsf {e}$. For the base cases we need two lemmas:

• for all $\mathsf {n}$, $\mathsf {x}$, $\mathsf {es}\;\!\!:\!\!\;\mathsf {DChain}\;\mathsf {A}\;\mathsf {n}$, and $\mathsf {r}$, we have $\mathsf {sem}\;\mathsf {r}\;\mathsf {n}\;(\mathsf {liftVal}\;\mathsf {n}\;\mathsf {x})\;\mathsf {es}\;\mathrel {=}\;\mathsf {x}$;

• for all $\mathsf {n}$, $\mathsf {xs}\;\!\!:\!\!\;\mathsf {Vec}\;\mathsf {A}\;\mathsf {n}$, and $\mathsf {r}\;\!\!:\!\!\;\mathsf {Ring}\;\mathsf {A}$, we have $\mathsf {map}\;(\lambda \;\mathsf {e}\;\mathsf {\rightarrow }\;\mathsf {sem}\;\mathsf {r}\;\mathsf {n}\;\mathsf {e}\;(\mathsf {toDChain}\;\mathsf {xs}))\;(\mathsf {genInd}\;\mathsf {n})\;\mathrel {=}\;\mathsf {xs}$.

The inductive case where $\mathsf {e}\;\mathsf {:=}\;\mathsf {e}_1\;{:\!\!+}\;\mathsf {e}_2$ eventually comes down to proving that (abbreviating $\lambda \;\mathsf {e}\;\mathsf {\rightarrow }\;\mathsf {sem}\;\mathsf {r}\;\mathsf {n}\;\mathsf {e}\;(\mathsf {toDChain}\;\mathsf {xs})$ to $\mathsf {sem'}$):

where $({+_\mathsf {VA}})\;\mathrel {=}\;\mathsf {fst}\;(\mathsf {fst}\;(\mathsf {ringVec}\;\mathsf {r}))$ defines addition on vectors of $\mathsf {A}$’s, and $({+_\mathsf {VP}})\;\mathrel {=}\;\mathsf {fst}\;(\mathsf {fst}\;(\mathsf {ringVec}\;(\mathsf {ringP}^{\star }\;\mathsf {r}\;\mathsf {n})))$ on vectors of polynomials. But this is implied by the free theorem of $\mathsf {ringVec}$. Specifically, $\mathsf {fst}\;\!\cdot \!\;\mathsf {fst}\;\!\cdot \!\;\mathsf {ringVec}$ has type

The free theorem it induces is

where $\mathsf {P}$ is given by:

The conclusion of the free theorem is exactly what we need, while proving the premise is routine. The case for $\mathsf {e}\;\mathsf {:=}\;\mathsf {e}_1\;{:\times }\;\mathsf {e}_2$ is similar.    $\square$

4 Compiling Polynomials

A potentially complex polynomial can be expanded, in several passes, to a vector of polynomial over $\mathsf {Word}$, which can be compiled separately. As we have mentioned, such compilation is useful for software implementation of cryptosystems. Furthermore, even for hardware implementation, such compilation can be useful, as we can break down a complicated polynomial expression into a sequence of simpler arithmetic operations in a smaller algebraic structure, reducing the design complexity.

We consider a simple imaginary machine with a heap, denoted by $\mathsf {Heap}$, that may abstractly be seen as mapping between memory addresses $\mathsf {Addr}$ and machine words $\mathsf {Word}$. Albeit its simplicity, we believe that such a model captures the essential aspects of a wide variety of hardware and software implementations. The operator $(\mathbin {!!})\;\!\!:\!\!\;\mathsf {Heap}\;\!\rightarrow \!\;\mathsf {Addr}\;\!\rightarrow \!\;\mathsf {Word}$ fetches the value stored in the given address, while $\mathsf {ringWord}\;\!\!:\!\!\;\mathsf {Ring}\;\mathsf {Word}$ defines how words are added and multiplied. The simple assembly language we consider consists of three instructions:

The command $\mathsf {Const}\;\mathsf {i}\;\mathsf {v}$ stores value $\mathsf {v}$ in address $\mathsf {i}$, $\mathsf {Add}\;\mathsf {i}\;\mathsf {j}\;\mathsf {k}$ fetches values stored in addresses $\mathsf {i}$ and $\mathsf {j}$ and stores their sum in address $\mathsf {k}$, and similarly with $\mathsf {Mul}$. Given a heap, executing an assembly program computes a new heap:

To compile a program we employ a monad $\mathsf {SSA}$, which support an operation $\mathsf {alloc}\;\!\!:\!\!\;\mathsf {SSA}\;\mathsf {Addr}$ that returns the address of an unused cell in the heap. A naive approach is to implement $\mathsf {SSA}$ by a state monad that keeps a counter of the highest address that is allocated, while $\mathsf {alloc}$ returns the current value of the counter before incrementing it — register allocation can be performed in a separate pass. To run a $\mathsf {SSA}$ monad we use a function $\mathsf {runSSA}\;\!\!:\!\!\;\mathsf {\forall }\;\{\mathsf {A}\;\mathsf {St}\}\;\mathsf {\rightarrow }\;\mathsf {St}\;\mathsf {\rightarrow }\;\mathsf {SSA}\;\mathsf {St}\;\mathsf {A}\;\mathsf {\rightarrow }\;(\mathsf {A}\;\mathsf {\times }\;\mathsf {St})$ that takes a state $\mathsf {St}$ and yields a pair containing the result and the new state.

Compilation of a polynomial yields $\mathsf {SSA}\;(\mathsf {Addr}\;\mathsf {\times }\;\mathsf {Ins})$, where the second component of the pair is an assembly program, and the first component is the address where the program, once run, stores the value of the polynomial. We define compilation of $\mathsf {Poly}^{\mathsf {n}}\;\mathsf {Word}$ by induction on $\mathsf {n}$. For the base case $\mathsf {Poly}^{\mathsf {0}}\;\mathsf {Word}\;\mathrel {=}\;\mathsf {Word}$, we simply allocate a new cell and store the given value there using $\mathsf {Const}$:

To compile a polynomial of type $\mathsf {Poly}^{\mathsf {n}}\;\mathsf {Word}$, we assume that the value of the $\mathsf {n}$ indeterminants are already computed and stored in the heap, the locations of which are stored in a vector of $\mathsf {n}$ addresses.

In the clause for $\mathsf {suc}\;\mathsf {n}$, $\mathsf {x}$ is the address storing the value for the outermost indeterminant. To compile $\mathsf {Ind}$, we simply return this address without generating any code. To compile $\mathsf {Lit}\;\mathsf {e}$ where $\mathsf {e}\;\!\!:\!\!\;\mathsf {Poly}^{\mathsf {n}}\;\mathsf {Word}$, we inductively call $\mathsf {compile}\;\mathsf {n}\;\mathsf {addr}$. The generated code is combined by $\mathsf {biOp}\;\mathsf {op}\;\mathsf {p}_1\;\mathsf {p}_2$, which runs $\mathsf {p}_1$ and $\mathsf {p}_2$ to obtain the compiled code, allocate a new address $\mathsf {dest}$, before generating a new instruction $\mathsf {op}\;\mathsf {dest}\;\mathsf {addr}_1\;\mathsf {addr}_2$:

The following function compiles a polynomial, runs the program, and retrieves the resulting value from the heap:

Correctness. Given a polynomial $\mathsf {e}$, by correctness we intuitively mean that the compiled program computes the value which $\mathsf {e}$ would be evaluated to. A formal statement of correctness is complicated by the fact that $\mathsf {e}\;\!\!:\!\!\;\mathsf {Poly}^{\mathsf {n}}\;\mathsf {A}$ expects, as arguments, $\mathsf {n}$ polynomials arranged as a descending chain, each of them expects arguments as well, and $\mathsf {ins}$ expects their values to be stored in the heap.

Given a heap $\mathsf {h}$, a chain $\mathsf {es}\;\!\!:\!\!\;\mathsf {DChain}\;\mathsf {Word}\;\mathsf {n}$, and a vector of addresses $\mathsf {rs}$, the predicate $\mathsf {Consistent}\;\mathsf {h}\;\mathsf {es}\;\mathsf {rs}$ holds if the values of each polynomial in $\mathsf {es}$ is stored in $\mathsf {h}$ at the corresponding address in $\mathsf {rs}$. The predicate can be expressed by the following $\mathsf {Agda}$ datatype:

Observe that in the definition of $(\mathsf {{:}{:}})$ the descending chain $\mathsf {es}$ is supplied to each invocation of $\mathsf {sem}$ to compute value of $\mathsf {e}$, before $\mathsf {e}$ itself is accumulated to $\mathsf {es}$.

The correctness of $\mathsf {compile}$ can be stated as:

The predicate $\mathsf {Consistent}\;\mathsf {h}\;\mathsf {es}\;\mathsf {rs}$ states that the values of the descending chain $\mathsf {es}$ are stored in the corresponding addresses $\mathsf {rs}$. The predicate $\mathsf {NoOverlap}\;\mathsf {r_{0}}\;\mathsf {rs}$ states that, if an $\mathsf {SSA}$ monad is run with starting address $\mathsf {r_{0}}$, all subsequent allocated addresses will not overlap with those in $\mathsf {rs}$. With the naive counter-based implementation of $\mathsf {SSA}$, $\mathsf {NoOverlap}\;\mathsf {r_{0}}\;\mathsf {rs}$ holds if $\mathsf {r_{0}}$ is larger than every element in $\mathsf {rs}$. The last line states that the polynomial $\mathsf {e}$ is compiled with argument addresses $\mathsf {es}$ and starting address $\mathsf {r_{0}}$, and the value the program computes should be the same as the semantics of $\mathsf {e}$, given the descending chain $\mathsf {es}$ as arguments.

With all the setting up, the property $\mathsf {compSem}\;\mathsf {n}\;\mathsf {e}$ can be proved by induction on $\mathsf {n}$ and $\mathsf {e}$.

5 Conclusions and Related Work

In dependently typed programming, a typical choice in implementing multivariate polynomials is to represent de Bruin indices using $\mathsf {Fin}\;\mathsf {n}$, the type having exactly $\mathsf {n}$ members. This is done in, for example, the $\mathsf {RingSolver}$ in the Agda standard library [5], among many. The tagless-final representation [2] is another alternative. In this paper, we have explored yet another alternative, chosen to see how far we can go in exploiting the isomorphism between $R[X_1,X_2\ldots ,X_m]$ and univariate polynomial ring $R[X_1,X_2,\ldots ,X_{m-1}][X_m]$. It turns out that we can go quite far — we managed to represent multivariate polynomials using univariate polynomials. Various operations on them can be defined inductively. In particular, we defined how a polynomial of vectors can be expanded to a vector of polynomials, and how a polynomial can be compiled to sequences of scalar-manipulating instructions like assembly-language programs. The correctness proofs of those operations also turn out to be straightforward inductions, once we figure out how to precisely express the correctness property.

We note that the current expansion formula is provided by the programmer. For example, in order to expand a complex polynomial expression into two real ones, the programmer needs to provide (in a $\mathsf {RingVec}$) the formula $(a_1+b_1i)(a_2+b_2i)\bmod i^2+1=(a_1a_2-b_1b_2)+(a_1b_2+a_2b_1)i$. We can see that the divisor polynomial of the modular relationship can actually give rise to an equational type in which $i^2+1=0$, or any pair of polynomials are considered “equal” if their difference is a multiple of the polynomial $i^2+1$. In the future, we would like to further automate the derivation of this formula, so the programmer will only need to give us the definition of the equational types under consideration. The $\mathsf {RingSolver}$ [5] manipulates equations into normal forms to solve them, and the solution can be used in Agda programs by reflection. It is interesting to explore whether a similar approach may work for our purpose.