# Formal Verification of the Sumcheck Protocol

Azucena Garvía Bosshard<EMAIL_ADDRESS>Independent
Researcher† Jonathan Bootle<EMAIL_ADDRESS>IBM Research Europe – Zurich
Christoph Sprenger<EMAIL_ADDRESS>ETH Zurich $\dagger$ Work done while
at ETH Zurich

###### Abstract

The sumcheck protocol, introduced in 1992, is an interactive proof which is a
key component of many probabilistic proof systems in computational complexity
theory and cryptography, some of which have been deployed. However, none of
these proof systems based on the sumcheck protocol enjoy a formally-verified
security analysis. In this paper, we make progress in this direction by
providing a formally verified security analysis of the sumcheck protocol using
the interactive theorem prover Isabelle/HOL. We follow a general and modular
approach.

First, we give a general formalization of public-coin interactive proofs. We
then define a _generalized sumcheck protocol_ for which we axiomatize the
underlying mathematical structure and we establish its soundness and
completeness. Finally, we prove that these axioms hold for multivariate
polynomials, the original setting of the sumcheck protocol. Our modular
analysis facilitates formal verification of sumcheck instances based on
different mathematical structures with little effort, by simply proving that
these structures satisfy the axioms. Moreover, the analysis supports the
development and formal verification of future cryptographic protocols using
the sumcheck protocol as a building block.

###### Index Terms:

sumcheck protocol, formal verification, interactive proofs, Isabelle

##  I Introduction

Probabilistic proof systems are protocols in which a powerful but untrusted
prover can convince a verifier that a given statement is true. They differ
from traditional mathematical proofs by incorporating interaction, randomness
and cryptographic assumptions. As a result, they offer benefits such as fast
verification and zero-knowledge properties.

Early research into interactive proofs [1, 2] produced complexity theoretic
results such as $\mathsf{IP}=\mathsf{PSPACE}$. Today, probabilistic proof
systems enjoy a high degree of adoption and are increasingly deployed in
applications such as verifiable computation, electronic voting, and
cryptocurrencies.

Errors in analysis. Unfortunately, the designs and deployments of
probabilistic proof systems often contain errors:

  * •

The analysis of the proof system [3] for integer commitments contained errors,
later addressed in [4];

  * •

The public setup information of the proof system [5] contained extra
information which made the proof system insecure. This affected the ZCash
cryptocurrency [6];

  * •

A significant gap in the security proof of [7] was found and fixed using three
different methods in [8, 9, 10].

  * •

The proof system described in [11] states a cheating probability lower than
its actual value. A proper analysis was given in [12, 13].

  * •

The description of the Fiat-Shamir transformation in [14] neglects to hash
certain values, which leads to the vulnerability described in [15]. This
affected multiple implementations of proof systems [16, 17, 18, 19, 20].

Other researchers have raised concerns about errors in cryptographic analyses
in general [21, 22]. As probabilistic proofs have become increasingly popular,
their security analyses demand greater care and scrutiny.

Formal verification of probabilistic proof systems. In order to remedy these
issues, researchers are starting to turn to machine-checkable security
analyses using formal verification techniques. Existing formal verification
work falls into two categories: formal verification of non-interactive proof
systems, such as that of [23] by [24, 25], and constant-round interactive
proof systems, including Sigma protocols [26], protocols using the “MPC-in-
the-head” paradigm of [27] in [28, 29], and particular signature schemes [30,
31].

However, despite this growing body of work, interactive proof systems with a
non-constant number of rounds have not yet been addressed. This category
contains a large number of protocols, including proof systems based on the GKR
protocol [32] for uniform circuits, proof systems for NP [33], “split-and-
fold” proof systems such as [34, 14], as well as protocols with optimal prover
complexity [35, 36, 37, 38] and interesting streaming properties [39, 40, 8,
41]. Note that while e.g. [26] does consider sequential composition of Sigma
protocols, leading to a multi-round protocol, many of the protocols cited
above have a significantly more complicated recursive structure.

In fact, the multi-round protocols cited above are all based on a single
protocol: the sumcheck protocol. Each protocol makes direct use of the
sumcheck protocol, or its algebraic [42] or combinatorial [43]
generalizations, as a subroutine. Moreover, the streaming properties of [40,
8, 41] are directly linked to those of the sumcheck protocol.

The sumcheck protocol. As the name suggests, the goal of the sumcheck protocol
is to check that the evaluation of a sum corresponds to a certain value. More
specifically, the verifier V’s objective is to use the prover P to confirm
that

$\isaid{v}=\sum_{(x_{1},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}}}\isaid{p}(x_{1},\ldots,x_{\isaid{n}})\enspace,$
(1)

where H is a subset of some field $\mathbb{F}$, p is a polynomial of arity n
over $\mathbb{F}$, and $\isaid{v}\in\mathbb{F}$. The protocol has n rounds of
interaction between the prover and the verifier, and a recursive structure
whereby statements about polynomials with arity n are reduced to statements
about polynomials with smaller arity, repeatedly, until arity $0$ is reached.

As well as being used in many practical probabilistic proof systems, the
sumcheck protocol and its generalizations are also a core component of many
complexity-theoretic results, like $\mathsf{coNP}\subseteq\mathsf{IP}$,
$\mathsf{PSPACE}=\mathsf{IP}$ [44, 45], and results on
$\mathsf{PPAD}$-hardness [46, 47, 48]. It is also one of few interactive proof
systems that can be made non-interactive via the Fiat-Shamir transformation
without relying on heuristics like the random oracle model [49].

Given the versatility of the sumcheck protocol, it is clear that its formal
analysis is highly desirable and constitutes the first step towards analysing
a great many probabilistic proofs with unique and interesting properties.

###  I-A Our Work

We provide a formally verified security analysis of the sumcheck protocol
[50]. We start with generic definitions of (recursive, multi-round) public-
coin interactive proofs and the associated soundness and completeness
properties, which we refer to as security properties. Our definition is
parameterized by prover and verifier functions and reduces the size of the
problem instance in each recursive call. We then formalize a _generalized
sumcheck protocol_ that abstracts from the concrete mathematical structure of
polynomials and we provide machine-checkable mathematical proofs of its
security properties in Isabelle/HOL. Our proofs thus cover an entire protocol
family of which the concrete sumcheck protocol is a special case. We also show
that the protocol and its properties are an instance of our generic
definitions for public-coin interactive proofs. More precisely, our analysis
proceeds in two steps.

In the first step, we axiomatize the key properties of polynomials required by
the protocol, formalize the generalized sumcheck protocol based on these
axioms, and prove its security. We have made an effort to make the the axioms
as weak as possible to ensure their wide applicability. For example, we make
only minimal assumptions about the polynomials’ algebraic structure, namely,
that they form a commutative monoid over a finite support set. For the
inductive proofs to succeed, the soundness and completeness theorems required
several generalizations of the statements usually found in less formal
accounts. For example, in the generalized soundness statement, the assumptions
about the polynomial’s arity and degree must be generalized to ensure that the
induction hypothesis is applicable.

In a second step, we show that concrete multivariate polynomials satisfy our
axioms. We do this based on an existing (concrete) formalization of
multivariate polynomials in Isabelle [51], which we extend with additional
definitions and results, e.g., about polynomial instantiation and the number
of a polynomial’s roots. This establishes the axioms’ consistency and
specializes the security proofs to the concrete protocol instance.

###  I-B Our Contributions

Our main contributions are as follows.

  * •

We define and formalize a generalized version of the sumcheck protocol and
prove its soundness and completeness. We then instantiate this protocol with
multivariate polynomials. To the best of our knowledge, this is the first
machine-checkable security analysis for probabilistic proof systems with an
input-size-dependent number of rounds.

  * •

Our general and modular analysis has several benefits. First, it simplifies
proofs by decoupling the reasoning about the protocol from reasoning about
concrete polynomial representations. Second, our general results can be used
to obtain security proofs of sumcheck protocol variants [52, 42] relying on
different but similar mathematical structures, such as, for example, rings or
modules instead of finite fields. This can be achieved with minimal effort by
proving that these structures satisfy the required axioms, with some minor
changes. Finally, our work paves the way for the future analysis of the many
aforementioned protocols which use the sumcheck protocol as a subroutine.

###  I-C Related Work

Bailey and Miller [24, 25] formalized the security analyses of various non-
interactive proof systems in the Lean 3 interactive theorem prover. They
analyze [53, 54, 55, 56, 57], and the construction of [23] which has extremely
low communication complexity and is widely deployed. All of these proof
systems are built from cryptographic pairings and have very similar
properties. Their security analysis takes place in a strong idealized model
called the “algebraic group model”, which simplifies both pen-and-paper and
machine security analysis. The analysis focuses on verifying equality between
the coefficients of various multivariate polynomial expressions.

Work on constant-round proof systems includes analyses of Sigma protocols and
their composition properties in [26] and protocols using the “MPC-in-the-head”
paradigm of [27] in [28, 29]. Many signature schemes are also based on
constant-round proof systems, and machine-formalized signature schemes and
implementations of this type include Schnorr [30] and Dilithium [31]
signatures. All of these formalizations use EasyCrypt. The analysis of Sigma
protocols is made more challenging through the use of computational
assumptions and security definitions involving computationally bounded
adversaries, and rewinding algorithms, which we do not consider here. Note
that [26] does consider the sequential composition of Sigma protocols, leading
to the formal analysis of a multi-round protocol. However, a composed Sigma
protocol treats the same instance in each repetition of the Sigma protocol,
whereas the sumcheck protocol reduces to a new instance in each round of the
protocol, in a way that depends on the previous messages in the protocol. Both
Sigma protocols and commitment schemes were formalized in [58] using the
CryptHOL framework based on Isabelle/HOL.

A recent Isabelle formalization of the Schwartz-Zippel lemma [59] also
involves formalizing various probabilistic and inductive statements about
multivariate polynomials similar to some lemmas we prove as part of our
soundness proof.

###  I-D Paper Outline and Supplementary Material

In Section II, we introduce interactive proofs, the sumcheck protocol,
Isabelle/HOL, and notation. We then formalize public-coin interactive proofs
in Isabelle (Section III). In Section IV, we present our formalization of a
generalized sumcheck protocol and in Section V proofs of its security
properties. In Section VI, we instantiate the generalized sumcheck protocol to
the original one using polynomials.

The complete Isabelle/HOL sources for the development in this paper are
available online [60].

##  II Preliminaries

###  II-A Interactive Proofs

Interactive proofs between a _prover_ algorithm P and a _verifier_ algorithm V
were first introduced by Goldwasser, Micali and Rackoff in [1]. In this
section, we give formal definitions of interactive proofs in terms of a
sequence of function executions between P and V. We start by defining
interactions.

######  Definition II.1 (Interactions).

Let $\textbf{P},\textbf{V}:\\{0,1\\}^{*}\rightarrow\\{0,1\\}^{*}$ and
$k\colon\\{0,1\\}^{*}\rightarrow\mathbb{N}$ be functions. We define a _$k(x)$
-round interaction_ between P and V on input $x\in\\{0,1\\}^{*}$ with verifier
randomness r as the following sequence of function outputs:

$\displaystyle a_{1},s_{\textbf{P}}^{1}$
$\displaystyle=\textbf{P}(s_{\textbf{P}}^{0})\enspace,$ $\displaystyle
a_{2},s_{\textbf{V}}^{1}$
$\displaystyle=\textbf{V}(s_{\textbf{V}}^{0},a_{1})\enspace,$ $\displaystyle
a_{3},s_{\textbf{P}}^{2}$
$\displaystyle=\textbf{P}(s_{\textbf{P}}^{1},a_{2})\enspace,$
$\displaystyle\vdots$ $\displaystyle a_{2k(x)},s_{\textbf{V}}^{k(x)}$
$\displaystyle=\textbf{V}(s_{\textbf{V}}^{k(x)-1},a_{2k(x)-1})\enspace.$

Here, $a_{2i-1}$ are messages from prover to verifier, while $a_{2i}$ are
messages from verifier to prover. Further, $s_{\textbf{P}}^{i}$ and
$s_{\textbf{V}}^{i}$ are the states of the prover and verifier respectively at
step $i$. The inputs and outputs are concatenated into single bitstrings using
commas, and we assume suitable encodings of input values that allow tuples to
be parsed unambiguously. The initial prover state $s_{\textbf{P}}^{0}$ is set
to $x$ and the initial verifier state $s_{\textbf{V}}^{0}$ is set to
$(x,\isaid{r})$. The outcome of the interaction is denoted by
$\langle\textbf{P},\textbf{V}(\isaid{r})\rangle(x)=a_{2k(x)}$.

A round in an interaction consists of a message from the prover to the
verifier and the verifier’s corresponding response. These are two moves. Note
that only the verifier has access to the randomness r of the interaction,
ensuring that the prover cannot predict the verifier’s messages.

Now, we define languages, and interactive proofs with respect to particular
languages.

######  Definition II.2 (Languages).

A _language_ is a set $\mathcal{L}\subseteq\\{0,1\\}^{*}$ of binary strings.
An element $x\in\mathcal{L}$ is referred to as an _instance_.

######  Definition II.3 (Interactive Proof Systems).

Let $0<s<1-c<1$. Let $k\colon\\{0,1\\}^{*}\rightarrow\mathbb{N}$. An
_interactive proof system_ for a language $\mathcal{L}$ with completeness
error $c$ and soundness error $s$ is a $k(x)$-round interaction between P and
V satisfying the following conditions:

  * •

Completeness: For all $x\in\mathcal{L}$,

$\textsf{Pr}_{\isaid{r}}[\langle\textbf{P},\textbf{V}(\isaid{r})\rangle(x)=1]\geq
1-c\enspace.$

  * •

Soundness: For all $x\notin\mathcal{L}$ and for all $\hat{\textbf{P}}$,

$\textsf{Pr}_{\isaid{r}}[\langle\hat{\textbf{P}},\textbf{V}(\isaid{r})\rangle(x)=1]\leq
s\enspace.$

  * •

The total running time of the verifier V is polynomially bounded in the length
of $x\in\\{0,1\\}^{*}$.

Here, probabilities are taken over the random value r which denotes the
randomness used by the verifier in the protocol. If
$\langle\textbf{P},\textbf{V}(\isaid{r})\rangle(x)=1$ then we say that the
verifier _accepts_ , and otherwise, we say that the verifier _rejects_.

Intuitively, completeness ensures the honest prover can usually convince the
verifier of a true statement, and soundness guarantees a dishonest prover
cannot usually convince the verifier of a false statement. The completeness
and soundness errors bound the probability that the verifier errs.

Definition II.1 is closely related to the definition of interactive Turing
machines in [1], with the prover and verifier states taking on the role of the
work and input tapes in the Turing machine definition. Definition II.1 only
considers deterministic provers, but this does not alter the class of
languages $\mathcal{L}$ for which an interactive proof exists.

Note that the completeness and soundness errors in Definition II.3 can be
generalized to functions $c,s\colon\mathbb{N}\to[0,1]$ such that
$c(|x|)<1-2^{\poly(|x|)}$, $s(|x|)>2^{-\poly(|x|)}$ and
$c(|x|)>s(|x|)+\frac{1}{\poly(|x|)}$. The completeness and soundness bounds
are then replaced by $c(|x|)$ and $s(|x|)$. This does not change the class of
languages $\mathcal{L}$ for which an interactive proof exists.

Finally, we define public-coin interactive proofs.

######  Definition II.4 (Public-Coin Proofs).

We say that an interactive proof system is _public coin_ if each of the
verifier’s messages is chosen uniformly at random from some set.

###  II-B The Sumcheck Protocol

In this section, we introduce the sumcheck protocol [50], a public-coin
interactive proof for the sumcheck problem, which is defined by the following
language. We assume suitable methods of encoding tuples and their elements
into binary strings.

######  Definition II.5.

Let $\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$ be the set of tuples
$(\mathbb{F},\isaid{H},\isaid{p},\isaid{v})$ such that $\mathbb{F}$ is a
finite field, $\isaid{H}\subseteq\mathbb{F}$,
$\isaid{p}\colon\mathbb{F}^{\isaid{n}}\to\mathbb{F}$ is a polynomial of arity
$n$, and $v\in\mathbb{F}$, satisfying

$\isaid{v}=\sum_{(x_{1},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}}}\isaid{p}(x_{1},x_{2},\ldots,x_{\isaid{n}})\enspace.$

This is the classic definition of the sumcheck problem with polynomials over
finite fields. Both the language $\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
and II.6 below generalize to other structures satisfying suitable properties,
such as polynomials over rings and modules. This will be discussed further in
Section IV.

We give a recursive description of the sumcheck protocol in II.6.

######  Protocol II.6 (Sumcheck Protocol).

The prover P takes as input a state $s_{\textbf{P}}$ containing the instance
$x=(\mathbb{F},\isaid{H},\isaid{p},\isaid{v})$. The verifier V takes as input
a state $s_{\textbf{V}}$ containing the instance $x$ and randomness
$(\isaid{r}_{1},\ldots,\isaid{r}_{\isaid{n}})\in\mathbb{F}^{\isaid{n}}$, where
n is the arity of p.

  * •

If p has arity $0$, then p is a constant polynomial. The prover P does not
send a message to the verifier. The verifier V checks whether
$\isaid{p}=\isaid{v}$ and accepts the proof if so, rejecting otherwise.

  * •

Otherwise, the prover P sends V the polynomial

$\isaid{q}(X):=\sum_{(x_{2},\ldots,\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}-1}}\isaid{p}(X,x_{2},\ldots,x_{\isaid{n}}).$

  * •

The verifier V checks that q is a univariate polynomial of degree at most
$\isaid{deg}(\isaid{p})$, and that
$\isaid{v}\stackrel{{\scriptstyle?}}{{=}}\sum_{x\in\isaid{H}}\isaid{q}(x)$. If
any of the checks fail, V rejects the proof.111Early rejection by the verifier
before the end of the protocol is easily modelled by having the verifier
include a special symbol in their state to ensure that they do reject at the
end. Otherwise V sends randomness $\isaid{r}_{1}$ to P.

  * •

The verifier V computes a reduced instance
${x}^{\prime}=(\mathbb{F},\isaid{H},{\isaid{p}}^{\prime},{\isaid{v}}^{\prime})$
where
${\isaid{p}}^{\prime}(X_{2},\ldots,X_{\isaid{n}}):=\isaid{p}(\isaid{r}_{1},X_{2},\ldots,X_{\isaid{n}})$
and ${\isaid{v}}^{\prime}:=\isaid{q}(\isaid{r}_{1})$, and updates its state to
$s^{\prime}_{\textbf{V}}:=({x}^{\prime},(\isaid{r}_{2},\ldots,\isaid{r}_{\isaid{n}}))$.
The prover P updates its state to $s^{\prime}_{\textbf{P}}:={x}^{\prime}$. The
prover P and verifier V continue the protocol on the reduced instance.

Note that the arity of the polynomial is reduced in each round and therefore
the protocol terminates after at most n reductions.

The main goal of this paper is to produce a machine-checked formalisation of
the following theorem and its proof.

######  Theorem II.7.

The sumcheck protocol defines a public-coin interactive proof for the language
$\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$ with null completeness error and
soundness error $\isaid{n}\cdot\isaid{deg}(\isaid{p})/|\mathbb{F}|$, where p
is the instance polynomial and n its arity.

The proof of this theorem is given in Appendix A.

Here, and throughout the paper, deg refers to the total degree of a
multivariate polynomial. The verifier check that q has degree at most
$\isaid{deg}(\isaid{p})$ is required for the soundness proof of the sumcheck
protocol, which relies on the fact that the number a polynomial’s roots is
bounded by its degree. In fact, $\isaid{deg}(\isaid{p})$ could be defined as
$\max_{i\in\\{1,\ldots,\isaid{n}\\}}\isaid{deg}_{i}(\isaid{p})$, where
$\isaid{deg}_{i}(\isaid{p})$ is the degree of p in variable $x_{i}$, which
gives a tighter bound on the soundness error.

###  II-C Isabelle/HOL and Notation

Isabelle is a generic interactive proof assistant that can be instantiated to
different object logics. We use its higher-order logic instance, Isabelle/HOL
[61], which uses the simply typed $\lambda$-calculus as its underlying
specification language. On top of that it offers various convenient high-level
specification mechanisms, e.g., for datatypes, inductive definitions, and
recursive function definitions. Isabelle/HOL comes with an extensive library
of concepts and theorems (e.g., about algebra, analysis, probability theory).
Isabelle is a foundational prover, i.e., all logical inferences are checked by
a small and well-tested logical kernel, and therefore it provides very strong
soundness guarantees. Isabelle offers a wide range of automated proof tools.
The main ones are a simplifier for rewriting (equational reasoning), a
classical reasoner, and sledgehammer, a binding to various back-end automated
theorem provers and SMT solvers.

An Isabelle/HOL development is organized into a collection of theories, each
defining new types and constants and proving theorems about them. We write
variables and types in italics (e.g., nat) and constants in sans serif font
(e.g., $\mathsf{zip}$). Type variables are marked with a leading quote (e.g.,
’a). We write $t::T$ to indicate that term $t$ has type $T$. Isabelle also
supports type classes, which are used to axiomatize types with a certain
(e.g., algebraic) structure. The (overloaded) notation $\isaid{'a}::\tau$
indicates that the type ’a belongs to type class $\tau$. For example,
$\isaid{xs}::(\isaid{'a}::\isaid{comm\\_monoid})~{}\isaid{list}$ indicates
that xs is a list of elements of a type ’a with a commutative monoid
structure.

We extensively use library functions for lists and maps (i.e., partial
functions): $x\mathrel{\\#}\isaid{xs}$ prepends the element $x$ to the list
xs, $\mathsf{map}~{}f~{}\isaid{xs}$ applies the function $f$ to all elements
of xs, $\mathsf{zip}~{}\isaid{xs}~{}\isaid{ys}$ turns the given lists into a
list of pairs (truncating the longer list, if any),
$\mathsf{set}~{}\isaid{xs}$ turns xs into a set,
$\mathsf{distinct}~{}\isaid{xs}$ asserts the uniqueness of all list elements,
$\mathsf{dom}~{}m$ denotes the map $m$’s domain, and $m_{1}\mathrel{++}m_{2}$
overrides the map $m_{1}$ with the entries of $m_{2}$. We also use some own
auxiliary functions: $\mathsf{tuples}~{}n$ denotes the set of lists of length
$n$ and $\mathsf{substs}~{}V~{}H$ refers to the set of maps from elements of
$V$ to elements of $H$, which we use to model substitutions.

We sometimes take some notational liberties for the sake of readability. For
example, we write
$\textsf{Pr}_{\isaid{r}\>\in\>\isaid{S}}[\isaid{E}~{}\isaid{r}]$ for the
Isabelle term
$(\mathsf{measure\\_pmf.prob}~{}(\mathsf{pmf\\_of\\_set}~{}\isaid{S})~{}\\{\isaid{r}.\;\isaid{E}~{}\isaid{r}\\})$
denoting the probability of the event $E$ under a uniformly random $r$ sampled
from the set $S$.

##  III Formalizing Public-Coin Proofs

$\displaystyle\isakw{type\\_synonym
}(\isaid{'i},\isaid{'r},\isaid{'a},\isaid{'resp},\isaid{'ps})~{}\isaid{prv}=$
$\displaystyle\quad\;\isaid{'i}\Rightarrow\isaid{'a}\Rightarrow\isaid{'a}~{}\isaid{list}\Rightarrow\isaid{'r}\Rightarrow\isaid{'ps}\Rightarrow\isaid{'resp}\times\isaid{'ps}$
$\displaystyle\isakw{locale }\isaid{public\\_coin\\_proof}=$
$\displaystyle\isakw{fixes
}\isaid{ver}_{0}::\isaid{'i}\Rightarrow\isaid{'vs}\Rightarrow\isaid{bool}$
$\displaystyle\isakw{ and
}\isaid{ver}_{1}::\isaid{'i}\Rightarrow\isaid{'resp}\Rightarrow\isaid{'r}\Rightarrow$
$\displaystyle\phantom{\isakw{ and
}\isaid{ver}_{1}::{}}\isaid{'a}\Rightarrow\isaid{'a}~{}\isaid{list}\Rightarrow\isaid{'vs}\Rightarrow\isaid{bool}\times\isaid{'i}\times\isaid{'vs}$
begin $\displaystyle\isakw{fun
}\isaid{prove}::\isaid{'vs}\Rightarrow(\isaid{'i},\isaid{'r},\isaid{'a},\isaid{'resp},\isaid{'ps})~{}\isaid{prv}\Rightarrow\isaid{'ps}\Rightarrow$
$\displaystyle\phantom{\isakw{fun
}\isaid{prove}::{}}\isaid{'i}\Rightarrow\isaid{'r}\Rightarrow(\isaid{'a}\times\isaid{'r})~{}\isaid{list}\Rightarrow\isaid{bool}\isakw{
where }$
$\displaystyle\quad\isaid{prove}~{}\isaid{vs}~{}\isaid{prv}~{}\isaid{ps}~{}\isaid{I}~{}\isaid{r}~{}[]\,\longleftrightarrow\,\isaid{ver}_{0}~{}\isaid{I}~{}\isaid{vs}$
$\displaystyle\quad\isaid{prove}~{}\isaid{vs}~{}\isaid{prv}~{}\isaid{ps}~{}\isaid{I}~{}\isaid{r}~{}((\isaid{x},\isaid{r}^{\prime})\mathrel{\\#}\isaid{rm})\,\longleftrightarrow\,$
$\displaystyle\qquad(\isakw{let
}(\isaid{resp},\isaid{ps}^{\prime})=\isaid{prv}~{}\isaid{I}~{}\isaid{x}~{}(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm})~{}\isaid{r}~{}\isaid{ps}\isakw{
in}$ $\displaystyle\qquad\>\>\isakw{let
}(ok,I^{\prime},vs^{\prime})=\isaid{ver}_{1}~{}\isaid{I}~{}\isaid{resp}~{}\isaid{r}^{\prime}~{}\isaid{x}~{}(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm})~{}\isaid{vs}\isakw{
in}$
$\displaystyle\qquad\>\>\quad\isaid{ok}\,\land\,\isaid{prove}~{}\isaid{vs}^{\prime}~{}\isaid{prv}~{}\isaid{ps}^{\prime}~{}\isaid{I}^{\prime}~{}\isaid{r}^{\prime}~{}\isaid{rm})$
end Figure 1: Public-coin proofs: protocol definition

We formalize public-coin proofs in two _locales_ in Isabelle/HOL (Figures 1
and 2). A locale introduces a context with some variables (fixes section) and
assumptions about them (assumes section), which can be freely used by
definitions and lemmas within that context. Locales can later be instantiated
with concrete constants, whereby the assumptions must be proven. In Section
IV, we will instantiate these locales with the generalized sumcheck protocol
and its security proofs.

###  III-A Generic Protocol Definition

The first locale, public_coin_proof (Figure 1), formalizes the recursive
function prove, which models a public-coin proof. The parameters of this
function are as follows:

  * •

$\isaid{ver}_{0}$ and $\isaid{ver}_{1}$, which are locale parameters, are the
verifier functions for the base case and the recursive case,

  * •

vs is the verifier’s current state,

  * •

prv and ps are the prover and its current state,

  * •

I is the problem instance,

  * •

r is the verifier’s randomness for the current round.

  * •

rm is a list of pairs of per-round public information and randomness, which is
used for the remaining rounds.

The verifier is a locale parameter, as it is part of a protocol definition and
remains fixed, while the soundness theorem is a statement about _arbitrary_
provers.

The base case, where the list rm is empty, determines the verifier’s final
verdict by calling the verifier function $\isaid{ver}_{0}$. In the recursive
case, we first call the prover prv and then pass on its response resp to the
verifier. Here, $(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm})$ projects all
pairs in rm to their first component (i.e., the public information),
$\isaid{ps}^{\prime}$ and $\isaid{vs}^{\prime}$ are the prover’s and the
verifier’s successor states, $I^{\prime}$ is the reduced problem instance, and
ok is the prover’s verdict for the current round. The latter is conjoined to
the result of the recursive call to prove on the prover’s and verifier’s
successor states $\isaid{ps}^{\prime}$ and $\isaid{vs}^{\prime}$, the instance
$\isaid{I}^{\prime}$, the randomness $\isaid{r}^{\prime}$ for the next round,
and the tail rm of the pair list.

There are some differences with Definitions II.1, II.3 and II.4. First, our
prover and verifier functions have additional arguments: the current instance
I, the remaining randomness (r and second components of rm), and some
additional round-wise public information (first components of rm). We assume
that the initial round-wise public information is derivable from the initial
instance I. These elements can be easily encoded into the prover and verifier
states of Definition II.1. Second, our prover always gets a random value, even
in the first round. This uniformity helps with the inductive security proofs.
All these differences are superficial and only introduced for convenience.

$\displaystyle\isakw{locale }\isaid{public\\_coin\\_proof\\_security}=$
$\displaystyle\quad\isaid{public\\_coin\\_proof}~{}\isaid{ver}_{0}~{}\isaid{ver}_{1}+{}$
$\displaystyle\isakw{fixes }\isaid{S}::\isaid{'i}~{}\isaid{set}$
$\displaystyle\isakw{ and
}\isaid{honest\\_pr}::(\isaid{'i},\isaid{'r},\isaid{'a},\isaid{'resp},\isaid{'ps})~{}\isaid{prv}$
$\displaystyle\isakw{ and
}\isaid{sound\\_assm}::\isaid{'vs}\Rightarrow\isaid{'ps}\Rightarrow\isaid{'i}\Rightarrow\isaid{'a}~{}\isaid{list}\Rightarrow\isaid{bool}$
$\displaystyle\isakw{ and
}\isaid{sound\\_err}::\isaid{'i}\Rightarrow\isaid{real}$ $\displaystyle\isakw{
and
}\isaid{compl\\_assm}::\isaid{'vs}\Rightarrow\isaid{'ps}\Rightarrow\isaid{'i}\Rightarrow\isaid{'a}~{}\isaid{list}\Rightarrow\isaid{bool}$
$\displaystyle\isakw{ and
}\isaid{compl\\_err}::\isaid{'i}\Rightarrow\isaid{real}$
$\displaystyle\isakw{assumes }\isaid{soundness}:$
$\displaystyle\qquad\llbracket\>\isaid{I}\notin\isaid{S};\;\isaid{sound\\_assm}~{}\isaid{vs}~{}\isaid{ps}~{}\isaid{I}~{}\isaid{xs}\rrbracket\Longrightarrow$
$\displaystyle\qquad\quad\textsf{Pr}_{rs\>\in\>\mathsf{tuples}\>(\mathsf{length}\>\isaid{xs})}[\>$
$\displaystyle\qquad\qquad\isaid{prove}~{}\isaid{vs}~{}\isaid{prv}~{}\isaid{ps}~{}\isaid{I}~{}\isaid{r}~{}(\mathsf{zip}~{}\isaid{xs}~{}\isaid{rs})$
$\displaystyle\qquad\quad\>]\leq\isaid{sound\\_err}~{}\isaid{I}$
$\displaystyle\isakw{ and }\isaid{completeness}:$
$\displaystyle\qquad\llbracket\>\isaid{I}\in\isaid{S};\;\isaid{compl\\_assm}~{}\isaid{vs}~{}\isaid{ps}~{}\isaid{I}~{}\isaid{xs}\rrbracket\Longrightarrow$
$\displaystyle\qquad\quad\textsf{Pr}_{rs\>\in\>\mathsf{tuples}\>(\mathsf{length}\>\isaid{xs})}[\>$
$\displaystyle\qquad\qquad\isaid{prove}~{}\isaid{vs}~{}\isaid{honest\\_pr}~{}\isaid{ps}~{}\isaid{I}~{}\isaid{r}~{}(\mathsf{zip}~{}\isaid{xs}~{}\isaid{rs})$
$\displaystyle\qquad\quad\>]\geq 1-\isaid{compl\\_err}~{}\isaid{I}$ Figure 2:
Public-coin proofs: security properties

###  III-B Generic Security Properties

The second locale, public_coin_proof_security (Figure 2), formalizes the
desired security properties of public-coin protocols as assumptions, which
must be proven when the locale is instantiated with a concrete protocol. It
extends the first locale (indicated by $+$) with additional parameters and
with assumptions. The parameters are as follows: S is the problem
specification (i.e., a set of instances), honest_pr is the honest prover
following the protocol, sound_assm and compl_assm are the conditions under
which soundness and completeness hold, and sound_err and compl_err are the
soundness and completeness errors. Finally, the assumptions soundness and
completeness formalize the protocol’s security properties as probabilistic
statements over the randomness tuples rs (cf. Definition II.3). Note that,
while the initial value r passed to prove need not be random, the successive
ones are. One can think of r as either as an initialization message for the
prover or as a dummy value.

We have also defined a variant of this locale, where the completeness is
deterministic. We then proved, by instantiating the locale above with the
variant, that this corresponds to the special case of the above completeness
property where the error is $0$.

##  IV The Generalized Sumcheck Protocol

In this section, we present our formalization of the sumcheck protocol in
Isabelle/HOL. We proceed in two stages. First, we axiomatize the required
mathematical properties of multivariate polynomials as locale in Isabelle/HOL
(Section IV-A). Then we formalize a generalized sumcheck protocol in the
context of that locale (Section IV-B). Later, we will generically prove its
completeness and soundness (Section V) and instantiate our locale with a
concrete representation of multivariate polynomials (Section VI). This
approach has the advantage of making the proofs more modular and of
facilitating future proofs about sumcheck variants over other mathematical
structures with properties similar to multivariate polynomials over finite
fields such as polynomials over rings and modules, tensor codes, or structures
in which the required properties only hold under a cryptographic assumption.

###  IV-A Axiomatizing Polynomials

$\displaystyle\isakw{locale }\isaid{multi\\_variate\\_polynomial}=$ fixes
$\displaystyle\quad\isaid{vars}::(\isaid{'p}::\isaid{comm\\_monoid\\_add})\Rightarrow\isaid{'v
set}$ $\displaystyle\quad\isaid{deg}::\isaid{'p}\Rightarrow\isaid{nat}$
$\displaystyle\quad\isaid{eval}::\isaid{'p}\Rightarrow(\isaid{'v},\isaid{'a}::\isaid{finite})~{}\isaid{subst}\Rightarrow$
$\displaystyle\qquad\qquad(\isaid{'b}::\isaid{comm\\_monoid\\_add})$
$\displaystyle\quad\isaid{inst}::\isaid{'p}\Rightarrow(\isaid{'v},\isaid{'a})~{}\isaid{subst}\Rightarrow\isaid{'p}$
assumes
$\displaystyle\quad\isaid{vars\\_finite}:\mathsf{finite}~{}(\isaid{vars}~{}\isaid{p})$
$\displaystyle\quad\isaid{vars\\_zero}:\isaid{vars}~{}0=\emptyset$
$\displaystyle\quad\isaid{vars\\_add}:\isaid{vars}~{}(\isaid{p}+\isaid{q})\subseteq\isaid{vars}~{}\isaid{p}\cup\isaid{vars}~{}\isaid{q}$
$\displaystyle\quad\isaid{vars\\_inst}:\isaid{vars}~{}(\isaid{inst}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$})\subseteq\isaid{vars}~{}\isaid{p}\setminus\mathsf{dom}~{}\textstyle\scalebox{0.9}{$\sigma$}$
$\displaystyle\quad\isaid{deg\\_zero}:\isaid{deg}~{}0=0$
$\displaystyle\quad\isaid{deg\\_add}:\isaid{deg}~{}(\isaid{p}+\isaid{q})\leq\mathsf{max}~{}(\isaid{deg}~{}\isaid{p})~{}(\isaid{deg}~{}\isaid{q})$
$\displaystyle\quad\isaid{deg\\_inst}:\isaid{deg}~{}(\isaid{inst}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$})\leq\isaid{deg}~{}\isaid{p}$
$\displaystyle\quad\isaid{eval\\_zero}:\isaid{eval}~{}0~{}\textstyle\scalebox{0.9}{$\sigma$}=0$
$\displaystyle\quad\isaid{eval\\_add}:\isaid{vars}~{}\isaid{p}\cup\isaid{vars}~{}\isaid{q}\subseteq\mathsf{dom}~{}\textstyle\scalebox{0.9}{$\sigma$}$
$\displaystyle\qquad\quad\;\Longrightarrow\isaid{eval}~{}(\isaid{p}+\isaid{q})~{}\textstyle\scalebox{0.9}{$\sigma$}=\isaid{eval}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}+\isaid{eval}~{}\isaid{q}~{}\textstyle\scalebox{0.9}{$\sigma$}$
$\displaystyle\quad\isaid{eval\\_inst}:\isaid{vars}~{}\isaid{p}\subseteq\mathsf{dom}~{}\textstyle\scalebox{0.9}{$\sigma$}\cup\mathsf{dom}~{}\textstyle\scalebox{0.9}{$\rho$}$
$\displaystyle\qquad\quad\;\Longrightarrow\isaid{eval}~{}(\isaid{inst}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$})~{}\textstyle\scalebox{0.9}{$\rho$}=\isaid{eval}~{}\isaid{p}~{}(\textstyle\scalebox{0.9}{$\rho$}\mathrel{++}\textstyle\scalebox{0.9}{$\sigma$})$
$\displaystyle\quad\isaid{roots}:\lvert\>\\{r\mid\isaid{vars}~{}\isaid{p}\subseteq\\{x\\}\>\land\>\isaid{vars}~{}\isaid{q}\subseteq\\{x\\}$
$\displaystyle\phantom{\quad\isaid{roots}:\lvert\>\\{}\>\land\>\isaid{deg}~{}\isaid{q}\leq\isaid{d}\>\land\>\isaid{deg}~{}\isaid{p}\leq\isaid{d}\>\land\>\isaid{p}\neq\isaid{q}\>\land\>$
$\displaystyle\phantom{\quad\isaid{roots}:\lvert\>\\{}\>\land\>\isaid{eval}~{}\isaid{p}~{}[\isaid{x}\mapsto\isaid{r}]=\isaid{eval}~{}\isaid{q}~{}[\isaid{x}\mapsto\isaid{r}]\\}\>\rvert\leq\isaid{d}$
Figure 3: The locale abstracting multivariate polynomials

We formalize our assumptions about multivariate polynomials in an Isabelle/HOL
locale (Figure 3). This locale declares four function variables along with
their types: given a polynomial p of abstract type ’p and a substitution
(i.e., partial function)  $\sigma$ from variables of type ’v to values of type
’a,

  1. 1.

vars p denotes the set of p’s variables,

  2. 2.

deg p is p’s degree,

  3. 3.

eval p $\sigma$ evaluates p to a value of type ’b using  $\sigma$ , and

  4. 4.

inst p $\sigma$ instantiates p to another polynomial using  $\sigma$ .

In contrast to the common formulation of the sumcheck protocol over a finite
field $\mathbb{F}$, we (only) impose an (additive) commutative monoid
structure on the types of polynomials ’p and their values ’b, and we assume
that the type ’a of their arguments is finite. In Isabelle, we can achieve
this by adding type class constraints to these type variables (e.g.,
$\isaid{'p}::\isaid{comm\\_monoid\\_add}$). Note that eval has different
argument and result types ’a and ’b. While these types coincide for
polynomials over a field $\mathbb{F}$ as used in II.6, they may differ for
other instantiations. For example, one could define a sumcheck protocol for
polynomials over _modules_ over a ring, in which case the arguments would be
ring elements and the results would be module elements.

Each of the four function variables comes with a set of assumptions about it.
Most of these concern the interaction of these functions with the additive
structure and with instantiation. Here, we only discuss the final three in
more detail. The assumption eval_add states that the result of evaluating the
sum $\isaid{p}+\isaid{q}$ of two polynomials under a substitution  $\sigma$
whose domain contains all their variables is the same as adding the results of
their individual evaluation under  $\sigma$ . The assumption eval_inst relates
evaluation and instantiation and expresses that, given two substitutions
$\sigma$ and  $\rho$ whose domains jointly cover p’s variables, first
instantiating a polynomial p with  $\sigma$ , followed by an evaluation under
$\rho$ is the same as evaluating p under the substitution
$\textstyle\scalebox{0.9}{$\rho$}\mathrel{++}\textstyle\scalebox{0.9}{$\sigma$}$,
which updates the substitution  $\rho$ with  $\sigma$ . The final assumption,
roots, states that any pair of different univariate polynomials p and q of
degrees bounded by d are equal on at most d points. We could equivalently
assume that the number of roots of a univariate polynomial is bounded by its
degree. This constitutes the main assumption required for the soundness proof.

Apart from the standard instance of multivariate polynomials over finite
fields, discussed in Section VI, multivariate polynomials over certain rings
satisfy small variants of these assumptions, where the roots assumption is
modified so that polynomials are only required to have a bounded number of
roots in a special _sampling set_ [52], which is a subset of the ring. The
verifier’s random messages in the sumcheck protocol must then be drawn from
the sampling set. Similar considerations hold for modules [42]. Therefore, we
expect that it would take little effort to extend our formalization to work
with sumcheck variants using polynomials over rings and modules with sampling
sets.

We proved a collection of lemmas derived from the locale’s assumptions. These
include finite sum variants of the assumptions involving binary addition and
three lemmas about the interaction of evaluation, instantiation, and finite
sums, which we present below.

The first lemma, eval_sum_inst, simplifies the evaluation of a finite sum of
instantiations to a finite sum of evaluations.

$\displaystyle\isakw{lemma }\isaid{eval\\_sum\\_inst}:$
$\displaystyle\quad\isakw{assumes
}\isaid{vars}~{}\isaid{p}\subseteq\isaid{V}\,\cup\,\mathsf{dom}~{}\textstyle\scalebox{0.9}{$\rho$}\isakw{
and }\mathsf{finite}~{}\isaid{V}$ $\displaystyle\quad\isakw{shows
}\isaid{eval}~{}(\sum_{\sigma\,\in\,\mathsf{substs}\>\isaid{V}\>\isaid{H}}\isaid{inst}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$})~{}\textstyle\scalebox{0.9}{$\rho$}$
$\displaystyle\hskip
36.98857pt=(\sum_{\sigma\,\in\,\mathsf{substs}\>\isaid{V}\>\isaid{H}}\isaid{eval}~{}\isaid{p}~{}(\textstyle\scalebox{0.9}{$\rho$}\mathrel{++}\textstyle\scalebox{0.9}{$\sigma$}))$

The second lemma, eval_sum_inst_commute, simultaneously commutes evaluation
with sum and swaps the substitutions used in the evaluation and the
instantiation, respectively.

$\displaystyle\isakw{lemma }\isaid{eval\\_sum\\_inst\\_commute}:$
$\displaystyle\quad\isakw{assumes
}\isaid{vars}~{}\isaid{p}\subseteq\\{\isaid{x}\\}\cup\isaid{V}\isakw{ and
}\isaid{x}\notin\isaid{V}\isakw{ and }\mathsf{finite}~{}\isaid{V}$
$\displaystyle\quad\isakw{shows
}\isaid{eval}~{}(\sum_{\sigma\,\in\,\isaid{substs}\>\isaid{V}\>\isaid{H}}\isaid{inst}~{}p~{}\textstyle\scalebox{0.9}{$\sigma$})~{}[\isaid{x}\mapsto\isaid{r}]$
$\displaystyle\phantom{\quad\isakw{shows
}}=\sum_{\sigma\,\in\,\isaid{substs}\>\isaid{V}\>\isaid{H}}\isaid{eval}~{}(\isaid{inst}~{}\isaid{p}~{}[\isaid{x}\mapsto{r}])~{}\textstyle\scalebox{0.9}{$\sigma$}$

The third lemma, sum_merge, combines two sums into one, merging a singleton
substitution into one with an extended domain.

$\displaystyle\isakw{lemma }\isaid{sum\\_merge}:$
$\displaystyle\quad\isakw{assumes }\isaid{x}\notin\isaid{V}$
$\displaystyle\quad\isakw{shows
}\sum_{\isaid{h}\,\in\,\isaid{H}}(\sum_{\sigma\in\isaid{substs}\>\isaid{V}\>\isaid{H}}\isaid{eval}~{}\isaid{p}~{}([\isaid{x}\mapsto\isaid{h}]~{}\texttt{++}~{}\textstyle\scalebox{0.9}{$\sigma$}))$
$\displaystyle\phantom{\quad\isakw{shows
}}=\sum_{\sigma\,\in\,\isaid{substs}\>(\\{\isaid{x}\\}\cup\isaid{V})\>\isaid{H}}\isaid{eval}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}$

The proofs of the above three lemmas use basic facts about sums and maps
together with our assumptions on vars, eval, and inst and their aforementioned
extensions to finite sums.

###  IV-B Protocol Formalization

Since we have fixed the types of arguments ’a and results ’b of our abstract
polynomials ’p in our locale, we will henceforth describe sumcheck instances
by triples
$(\isaid{H},\isaid{p},\isaid{v})\in\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
(omitting the finite field $\mathbb{F}$). In Isabelle/HOL, we define
$\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$ as follows.

$\displaystyle\isakw{type\\_synonym
}(\isaid{'p},\isaid{'a},\isaid{'v})~{}\isaid{sc\\_inst}=\isaid{'a
set}\times\isaid{'p}\times\isaid{'v}$ $\displaystyle\isakw{definition
}\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}::(\isaid{'p},\isaid{'a},\isaid{'v})~{}\isaid{sc\\_inst}~{}\isaid{set}\isakw{
where }$
$\displaystyle\quad\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}=\\{(\isaid{H},\isaid{p},\isaid{v})\mid\sum_{\sigma\,\in\,\mathsf{substs}\>(\isaid{vars}\>p)\>H}\isaid{eval}~{}p~{}\textstyle\scalebox{0.9}{$\sigma$}=\isaid{v}\\}$

For better readability and easier reference, we formalize the generalized
sumcheck protocol in Isabelle/HOL as a separate recursively defined predicate
$\mathsf{sumcheck}$, which invokes the prover and integrates the verifier.
However, we do also define the sumcheck protocol as an instance of our generic
definition of public-coin proofs (cf. Figure 1) and establish its equality
with the definition given here.

The predicate $\mathsf{sumcheck}$ is parameterized by the prover, which is a
function of type

$\displaystyle\isakw{type\\_synonym
}(\isaid{'p},\isaid{'a},\isaid{'b},\isaid{'v},\isaid{'s})~{}\isaid{prover}=$
$\displaystyle\quad(\isaid{'p},\isaid{'a},\isaid{'b})~{}\isaid{sc\\_inst}\Rightarrow\isaid{'v}\Rightarrow\isaid{'v
list}\Rightarrow\isaid{'a}\Rightarrow\isaid{'s}\Rightarrow\isaid{'p}\times\isaid{'s}$

Note that this type specializes the prover type prv from Figure 1. For a
prover pr of this type, the application
$(\isaid{pr}~{}\isaid{I}~{}\isaid{x}~{}\isaid{xs}~{}\isaid{r}~{}\isaid{s})$
returns a pair $(\hat{\isaid{q}},\isaid{s}^{\prime})$ consisting of a
univariate polynomial $\hat{\isaid{q}}$, which is sent as the next challenge
to the verifier, and the prover’s successor state $\isaid{s}^{\prime}$. The
parameters are as follows: I is the sumcheck instance, x is the returned
polynomial $\hat{\isaid{q}}$’s expected variable, xs is a list of variables
not containing x such that
$\isaid{vars}~{}\isaid{p}\subseteq\mathsf{set}~{}\isaid{xs}\,\cup\\{\isaid{x}\\}$,
r is the verifier’s next random value, and s is the prover’s current state.

fun
$\displaystyle\mathsf{sumcheck}::(\isaid{'v},\isaid{'a},\isaid{'p},\isaid{'s})~{}\isaid{prover}\Rightarrow\isaid{'s}\Rightarrow\isaid{'a
set}\Rightarrow\isaid{'p}\Rightarrow$ $\displaystyle\hskip
51.21495pt\isaid{'b}\Rightarrow\isaid{'a}\Rightarrow(\isaid{'v}\times\isaid{'a})~{}\isaid{list}\Rightarrow\isaid{bool}\isakw{
where }$
$\displaystyle\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}[]\,\longleftrightarrow\,\isaid{v}=\isaid{eval}~{}\isaid{p}~{}\emptyset$
$\displaystyle\mid\;$
$\displaystyle\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}((\isaid{x},\isaid{r}^{\prime})\mathrel{\\#}\isaid{rm})\,\longleftrightarrow\,$
$\displaystyle\quad\isakw{let
}(\hat{\isaid{q}},\isaid{s}^{\prime})=\isaid{pr}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{x}~{}(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm})~{}\isaid{r}~{}\isaid{s}\isakw{
in}$
$\displaystyle\qquad\isaid{vars}~{}\hat{\isaid{q}}\subseteq\\{\isaid{x}\\}\>\land\>\isaid{deg}~{}\hat{\isaid{q}}\leq\isaid{deg}~{}\isaid{p}\>\land{}$
$\displaystyle\qquad\isaid{v}=\sum_{\isaid{h}\in\isaid{H}}\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{h}]\>\land{}$
$\displaystyle\qquad\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}^{\prime}~{}$
$\displaystyle\qquad\quad(\isaid{H},\,\isaid{inst}~{}\isaid{p}~{}[\isaid{x}\mapsto\isaid{r}^{\prime}],\,\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{r}^{\prime}])~{}\isaid{r}^{\prime}~{}\isaid{rm}$
Figure 4: Formal definition of the sumcheck protocol

We then define the predicate $\mathsf{sumcheck}$ as in Figure 4. An
application
$(\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}~{}(\isaid{H},\;\isaid{p},\;\isaid{v})~{}\isaid{r}~{}\isaid{rm})$
returns the verifier’s verdict (accept or reject). The parameters are as
follows: pr is the prover as described above, s is the prover’s current state,
$(\isaid{H},\isaid{p},\isaid{v})$ describe the current sumcheck instance, r is
the randomness sent by the verifier as an input to the prover, and rm is an
ordered substitution consisting of a list of pairs of variables and random
values.

The predicate $\mathsf{sumcheck}$ is defined using two equations (i.e.,
logical equivalences). The first equation describes the base case where the
list rm is empty and the polynomial p is a constant, which is evaluated under
the empty substitution $\emptyset$ and compared to the value v. The second
equation describes the recursive case, which reduces the instance by executing
one round of the protocol. We first call the prover pr to obtain the prover’s
message to the verifier, i.e., the polynomial $\hat{\isaid{q}}$, and its
successor state $\isaid{s}^{\prime}$. We call the projection
$(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm})$ of rm to the public information
the domain of rm. The verifier then performs the following checks:

  1. (i)

_variable check_ : the received polynomial $\hat{\isaid{q}}$ has (at most) the
expected variable,

  2. (ii)

_degree check_ : $\hat{\isaid{q}}$’s degree is bounded by p’s degree, and

  3. (iii)

_evaluation check_ : the sum of $\hat{\isaid{q}}$ over all
$\isaid{h}\in\isaid{H}$ matches the value v.

These checks are conjoined with a recursive call of the function
$\mathsf{sumcheck}$ with the new state $\isaid{s}^{\prime}$ of the prover and
the reduced sumcheck instance
$(\isaid{H},\isaid{p}^{\prime},\isaid{v}^{\prime})$, where the polynomial
$\isaid{p}^{\prime}=\isaid{inst}~{}\isaid{p}~{}[\isaid{x}\mapsto\isaid{r}^{\prime}]$
instantiates p’s variable x to $\isaid{r}^{\prime}$ and the value
$\isaid{v}^{\prime}=\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{r}^{\prime}]$
evaluates q at $\isaid{r}^{\prime}$. We call this the _recursive check_. Note
that the recursion terminates, since the length of the list rm decreases in
each call.

Finally, we define the honest prover to match the protocol description (cf.
II.6):

$\displaystyle\isakw{definition
}\mathsf{honest\\_prover}::(\isaid{'v},\isaid{'a},\isaid{'p},\isaid{unit})~{}\isaid{prover}\isakw{
where }$
$\displaystyle\quad\mathsf{honest\\_prover}~{}(\isaid{H},\;\isaid{p},\;\isaid{v})~{}\isaid{x}~{}\isaid{xs}~{}\isaid{r}~{}\\_=$
$\displaystyle\qquad(\sum_{\sigma\,\in\,\mathsf{substs}\>(\mathsf{set}\>\isaid{xs})\>\isaid{H}}\isaid{inst}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$},())$

This function returns the univariate polynomial
$\isaid{q}=(\sum_{\sigma\,\in\,\mathsf{substs}\>(\mathsf{set}\>\isaid{xs})\>\isaid{H}}\isaid{inst}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$})$
with variable $\isaid{x}\notin\mathsf{set}~{}\isaid{xs}$, obtained by summing
up all instances of p over all substitutions  $\sigma$ assigning values in H
to the variables in $\mathsf{set}~{}\isaid{xs}$. This prover does not use a
state (hence the state’s type is unit) and ignores the sumcheck instance’s
value v, the current variable x, and the randomness r sent by the verifier.

###  IV-C Discussion of our Formalization

Comparing with common informal accounts of the sumcheck protocol (see, e.g.,
[62, 63]), we find the following additional points noteworthy. First, we
formalize the entire interaction between the prover and the verifier as a
single recursive predicate $\mathsf{sumcheck}$, which is actually an instance
of a general definition (cf. Figure 1), thus replacing an informal sequence of
protocol steps with a compact and rigorous mathematical description. Second,
we model randomness as externally provided rather than generated on-the-fly,
which allows for a simpler formalization and proofs based on deterministic
functions rather than probabilistic monads. Third, we model a generalized
sumcheck protocol, where we abstract the underlying structure of polynomials
by a set of functions and assumptions over them (Figure 3).

We expect that our formalization would extend easily to various
generalizations of the language $\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
and the sumcheck protocol. This includes instances where the polynomial
$\isaid{p}(X_{1},\ldots,X_{\isaid{n}})$ is evaluated and summed over possibly
different sets $\isaid{H}_{1},\ldots,\isaid{H}_{\isaid{n}}$ for each variable
$X_{1},\ldots,X_{\isaid{n}}$, to check whether

$\isaid{v}=\sum_{x_{1}\in\isaid{H}_{1},\ldots,x_{\isaid{n}}\in\isaid{H}_{\isaid{n}}}\isaid{p}(x_{1},x_{2},\ldots,x_{\isaid{n}})\enspace.$

One could also consider weighted sums

$\isaid{v}=\sum_{(x_{1},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}}}w_{1}(x_{1})\cdots
w_{\isaid{n}}(x_{\isaid{n}})\cdot\isaid{p}(x_{1},x_{2},\ldots,x_{\isaid{n}})$

for weight functions $w_{1},\ldots,w_{\isaid{n}}\colon\isaid{H}\to\mathbb{F}$
as in [35], by including $w_{2},\ldots,w_{\isaid{n}}$ in the sum defining q
and changing the verifier checks to
$\isaid{v}\stackrel{{\scriptstyle?}}{{=}}\sum_{x\in\isaid{H}}w_{1}(x_{1})\isaid{q}(x)$.
Setting the weight functions appropriately allows the sumcheck protocol to
work with multisets.

##  V Security Properties

We now turn to the two main results that we proved about the sumcheck
protocol: its completeness and soundness. We have also instantiated the locale
public_coin_proof_security from Figure 2 with our security results, thus
showing that they match the general definitions. We start our presentation
with the (simpler) completeness property.

###  V-A Completeness

The sumcheck protocol’s completeness theorem (cf. Theorem II.7) states that
the verifier will (deterministically) accept any run with the honest prover on
an instance
$(\isaid{H},\isaid{p},\isaid{v})\in\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
of the sumcheck problem. We formalize this theorem as follows.

$\displaystyle\isakw{theorem }\isaid{completeness}:$ assumes
$\displaystyle\qquad(\isaid{H},\isaid{p},\isaid{v})\in\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
$\displaystyle\qquad\isaid{vars}~{}\isaid{p}=\mathsf{set}~{}(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm})$
$\displaystyle\qquad\mathsf{distinct}~{}(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm})$
$\displaystyle\qquad\isaid{H}\neq\emptyset$ $\displaystyle\quad\isakw{shows
}\mathsf{sumcheck}~{}\mathsf{honest\\_prover}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}\isaid{rm}$

The additional assumptions state that (i) the set of p’s variables corresponds
to the domain of rm, (ii) the variables in the domain of rm are all distinct,
and (iii) that the set H is non-empty.

For the inductive proof to succeed, we slightly generalize this statement as
follows.

$\displaystyle\isakw{lemma }\isaid{completeness\\_inductive}:$ assumes
$\displaystyle\qquad\isaid{v}\,=\sum_{\sigma\,\in\,\mathsf{substs}\>(\mathsf{set}\>(\mathsf{map}\>\mathsf{fst}\>\isaid{rm}))\>\isaid{H}}\isaid{eval}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}$
$\displaystyle\qquad\isaid{vars}~{}\isaid{p}\subseteq\mathsf{set}~{}(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm})$
$\displaystyle\qquad\mathsf{distinct}~{}(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm})$
$\displaystyle\qquad\isaid{H}\neq\emptyset$ shows
$\displaystyle\qquad\mathsf{sumcheck}~{}\mathsf{honest\\_prover}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}\isaid{rm}$

Here, the equality in the second assumption has turned into a set inclusion.
The reason is that the arity of p may decrease by more than one in each
recursive call, while the length of rm decreases by exactly one. For example,
$p=xy$ has arity $2$, while $(\isaid{inst}~{}p~{}[x\mapsto 0])=0$ has arity
$0$. As a result, we have also unfolded the definition of
$\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$ and replaced the domain
$\isaid{vars}~{}p$ of the substitutions in the sum by the overapproximation
$\mathsf{set}~{}(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm})$. We now prove this
lemma.

###### Proof.

Our proof proceeds by computation induction on the definition of
$\mathsf{sumcheck}$ (Section IV-B).222An induction on rm would also work, but
would be more tedious. This form of induction exactly follows the structure of
the function definition, for which, crucially, termination is proven as part
of its definition. Isabelle automatically generates a computation induction
rule for each recursively defined function.

_Base case._ For this case, we must show that

$\mathsf{sumcheck}~{}\mathsf{honest\\_prover}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}[]$

holds, which Isabelle’s simplifier proves automatically. Since
$\isaid{rm}=[]$, the goal simplifies to
$\isaid{v}=\isaid{eval}~{}\isaid{p}~{}\emptyset$, as does the theorem’s first
assumption, since $\mathsf{substs}~{}\emptyset~{}\isaid{H}=\\{\emptyset\\}$.

_Inductive step._ In the inductive step, we have to show that

$\mathsf{sumcheck}~{}\mathsf{honest\\_prover}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}((\isaid{x},\isaid{r}^{\prime})\mathrel{\\#}\isaid{rm}^{\prime})$
(2)

holds under the assumptions

$\displaystyle\isaid{v}=\sum_{\sigma\,\in\,\mathsf{substs}\>(\mathsf{set}\>(\mathsf{map}\>\mathsf{fst}\>((\isaid{x},\isaid{r}^{\prime})\mathrel{\\#}\isaid{rm'})))\>\isaid{H}}\isaid{eval}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}$
(3)
$\displaystyle\isaid{vars}~{}\isaid{p}\subseteq\mathsf{set}~{}(\mathsf{map}~{}\mathsf{fst}~{}((\isaid{x},\isaid{r}^{\prime})\mathrel{\\#}\isaid{rm}^{\prime}))$
(4)
$\displaystyle\mathsf{distinct}~{}(\mathsf{map}~{}\mathsf{fst}~{}((\isaid{x},\isaid{r}^{\prime})\mathrel{\\#}\isaid{rm}^{\prime}))$
(5) $\displaystyle\isaid{H}\neq\emptyset$ (6)

and the induction hypothesis (see below). Let
$V=\mathsf{set}~{}(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm}^{\prime})$. By
definition of the $\mathsf{sumcheck}$ function, our goal (2) reduces to
proving that the variable, degree, evaluation and recursive checks succeed
given

$\displaystyle(\hat{\isaid{q}},\isaid{s}^{\prime})$
$\displaystyle=\mathsf{honest\\_prover}~{}\isaid{H}~{}\isaid{p}~{}\isaid{x}~{}V~{}\isaid{r}~{}\isaid{s}$
$\displaystyle=(\sum_{\sigma\,\in\,\mathsf{substs}\>V\>\isaid{H}}\isaid{inst}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$},()).$

The variable and degree checks,
$\isaid{vars}~{}\hat{\isaid{q}}\subseteq\\{\isaid{x}\\}$ and
$\isaid{deg}~{}\hat{\isaid{q}}\leq\isaid{deg}~{}\isaid{p}$, are
straightforward using the definition of the honest prover, locale assumptions
on vars, deg, and inst and the assumptions (4) and (6) above.

The evaluation check, namely, that
$\isaid{v}=\sum_{\isaid{h}\in\isaid{H}}\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{h}]$,
follows the chain of equations

v
$\displaystyle=\sum_{\sigma\,\in\,\mathsf{substs}\>(V\>\cup\>\\{\isaid{x}\\})\>\isaid{H}}\isaid{eval}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}$
(7)
$\displaystyle=\sum_{\isaid{h}\,\in\,\isaid{H}}\left(\sum_{\sigma\,\in\,\mathsf{substs}\>V\>\isaid{H}}\isaid{eval
p}\>([\isaid{x}\mapsto\isaid{h}]\mathrel{++}\textstyle\scalebox{0.9}{$\sigma$})\right)$
(8)
$\displaystyle=\sum_{\isaid{h}\,\in\,\isaid{H}}\isaid{eval}~{}\left(\sum_{\sigma\,\in\,\mathsf{substs}\>V\>H}\isaid{inst}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}\right)~{}[\isaid{x}\mapsto\isaid{h}]$
(9)
$\displaystyle=\sum_{\isaid{h}\,\in\,\isaid{H}}\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{h}],$
(10)

where Equation 7 comes from assumption (3), Equation 8 uses sum_merge (Section
IV-A) and $\isaid{x}\notin\isaid{V}$, which follows from assumption (5),
Equation 9 uses the lemma eval_sum_inst (Section IV-A) and assumption (4) and
Equation 10 holds by definition of $\hat{q}$.

Finally, the recursive check is

$\displaystyle\mathsf{sumcheck}~{}\mathsf{honest\\_prover}~{}\isaid{s}^{\prime}~{}\isaid{I}^{\prime}~{}\isaid{r}^{\prime}~{}\isaid{rm}^{\prime},$

where
$\isaid{I}^{\prime}=(\isaid{H},\isaid{inst}~{}\isaid{p}~{}[\isaid{x}\mapsto\isaid{r}^{\prime}],\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{r}^{\prime}])$.
This is exactly the conclusion of the induction hypothesis, which holds under
the assumptions

$\displaystyle\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{r}^{\prime}]\>=\sum_{\sigma\,\in\,\mathsf{substs}\>V\>\isaid{H}}\isaid{eval}~{}(\isaid{inst}~{}\isaid{p}~{}[\isaid{x}\mapsto\isaid{r}^{\prime}])~{}\textstyle\scalebox{0.9}{$\sigma$}$
(11)
$\displaystyle\isaid{vars}~{}(\isaid{inst}~{}\isaid{p}~{}[\isaid{x}\mapsto\isaid{r}^{\prime}])\subseteq\mathsf{dom}~{}(\mathsf{map\\_of}~{}\isaid{rm}^{\prime})$
(12)
$\displaystyle\mathsf{distinct}~{}(\mathsf{map}~{}\mathsf{fst}~{}\isaid{rm}^{\prime})$
(13) $\displaystyle\isaid{H}\neq\emptyset.$ (14)

Using the lemma eval_sum_inst_commute (Section IV-A), we prove the first
assumption and the remaining ones follow straightforwardly from the locale
assumptions and assumptions (3)-(6) of the induction step, and therefore so
does the recursive check. ∎

###  V-B Soundness

We formalize the soundness theorem of the sumcheck protocol (cf. Theorem II.7)
as follows.

$\displaystyle\isakw{theorem }\isaid{soundness}:$
$\displaystyle\quad\isakw{assumes
}(\isaid{H},\isaid{p},\isaid{v})\notin\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
$\displaystyle\qquad\isakw{ and
}\isaid{vars}~{}\isaid{p}=\mathsf{set}~{}\isaid{vs}\isakw{ and
}\mathsf{distinct}~{}\isaid{vs}\isakw{ and }H\neq\emptyset$
$\displaystyle\quad\isakw{shows
}\textsf{Pr}_{\isaid{rs}\,\in\,\mathsf{tuples}\>(\mathsf{arity}\>\isaid{p})}[\>$
$\displaystyle\qquad\qquad\quad\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}(\mathsf{zip}~{}\isaid{vs}~{}\isaid{rs})$
$\displaystyle\qquad\qquad\>]\leq\frac{\isaid{deg}~{}\isaid{p}\cdot\mathsf{arity}~{}\isaid{p}}{\lvert\mathbb{A}\rvert}$

Some explanatory remarks are in order here. First, the randomness is taken
over a tuple rs of length the arity of p, where $\mathsf{arity}~{}\isaid{p}$
is defined as the size of vars p. Recall that, in our protocol formalization,
the prover always gets an input, so r corresponds to an initial value sent by
the verifier. Although the initial value r need not be random, those passed in
subsequent recursive calls will be. This structure makes all rounds look the
same, which helps when setting up the induction proof. Second, note that the
first two assumptions imply that vs has the same length as rs. Hence, all list
elements are combined into pairs in
$(\mathsf{zip}~{}\isaid{vs}~{}\isaid{rs})$. Third, we use $\mathbb{A}$ to
denote the (finite) set of all elements of the type ’a and
$\lvert\mathbb{A}\rvert$ is its cardinality.

Unlike the completeness statement above we cannot prove this theorem by
computation induction on the definition of $\mathsf{sumcheck}$, since rs in
its last argument $(\mathsf{zip}~{}\isaid{vs}~{}\isaid{rs})$ is bound by the
probability statement. Instead, we use induction on the variable list vs and,
since the variables p, v, s, and r change in recursive calls to
$\mathsf{sumcheck}$, we generalize the induction over these variables, meaning
that they appear universally quantified in the induction hypothesis and can
thus be instantiated with different values in the proof.

Moreover, similar to the completeness theorem, this theorem’s second
assumption, $\isaid{vars}~{}\isaid{p}=\mathsf{set}~{}\isaid{vs}$, is too
strong, and must be weakened to
$\isaid{vars}~{}\isaid{p}\subseteq\mathsf{set}~{}\isaid{vs}$. We also replace
vars p by $\mathsf{set}~{}\isaid{vs}$ and $\mathsf{arity}~{}\isaid{p}$ by
$\mathsf{length}~{}\isaid{vs}$ in the conclusion. Similarly, the degree of the
reduced instance’s $\isaid{p}^{\prime}$ might be (possibly much) smaller than
p’s degree. Hence, we introduce an additional assumption
$\isaid{deg}~{}\isaid{p}\leq\isaid{d}$ with an upper bound d for the degree,
which replaces deg p in the theorem’s soundness error.

This discussion leads to the following inductive generalization of the
soundness theorem for which the sketched induction proof setup succeeds.

$\displaystyle\isakw{lemma }\isaid{soundness\\_inductive}:$ assumes
$\displaystyle\qquad\isaid{deg}~{}\isaid{p}\leq\isaid{d}\isakw{ and
}\isaid{vars}~{}\isaid{p}\subseteq\mathsf{set}~{}\isaid{vs}\isakw{ and }{}$
$\displaystyle\qquad\mathsf{distinct}~{}\isaid{vs}\isakw{ and
}\isaid{H}\neq\emptyset$ shows
$\displaystyle\qquad\textsf{Pr}_{\isaid{rs}\>\in\>\mathsf{tuples}\>(\mathsf{length}\>\isaid{vs})}[$
$\displaystyle\qquad\quad\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}(\mathsf{zip}~{}\isaid{vs}~{}\isaid{rs})\;\land\;$
$\displaystyle\qquad\quad
v\neq\sum_{\sigma\>\in\>\mathsf{substs}\>(\mathsf{set}\>\isaid{vs})\>H}\isaid{eval}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}$
$\displaystyle\qquad]\leq\frac{\isaid{d}\cdot\mathsf{length}~{}\isaid{vs}}{\lvert\mathbb{A}\rvert}$

###### Proof.

By list induction on vs, generalizing over s, p, v, and r.

_Base case._ For $\isaid{vs}=[]$, we have to establish that

$\displaystyle\textsf{Pr}_{rs\>\in\>\mathsf{tuples}\;0}[\>$
$\displaystyle\quad\;\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}[]\,\land\,$
$\displaystyle\quad\;\isaid{v}\neq\isaid{eval}~{}\isaid{p}~{}\emptyset$
$\displaystyle\>]\leq 0$

which is proven automatically by Isabelle’s simplifier, since
$(\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}~{}(\isaid{H},\;\isaid{p},\;\isaid{v})~{}\isaid{r}~{}[])$
reduces to $\isaid{v}=\isaid{eval}~{}\isaid{p}~{}\emptyset$ by the definition
of $\mathsf{sumcheck}$.

_Inductive step._ For $\isaid{vs}=\isaid{x}\mathrel{\\#}\isaid{vs}^{\prime}$,
we have to show that

$\displaystyle\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}\>\in\>\mathsf{tuples}\>(\mathsf{Suc}\>(\mathsf{length}\>\isaid{vs}^{\prime}))}[$
$\displaystyle\quad\;\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}(\mathsf{zip}~{}(\isaid{x}\mathrel{\\#}\isaid{vs}^{\prime})~{}(\isaid{r}_{1}\mathrel{\\#}\isaid{rs}))\>\land\>{}$
$\displaystyle\quad\;\isaid{v}\>\neq\sum_{\sigma\>\in\>\mathsf{substs}\>(\\{\isaid{x}\\}\,\cup\,\mathsf{set}\>\isaid{vs}^{\prime})\>\isaid{H}}\isaid{eval}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}$
$\displaystyle]\leq\frac{\isaid{d}\cdot\mathsf{Suc}~{}(\mathsf{length}~{}\isaid{vs}^{\prime})}{\lvert\mathbb{A}\rvert}$

under the assumptions
$\isaid{vars}~{}\isaid{p}\subseteq\\{\isaid{x}\\}\cup\mathsf{set}~{}\isaid{vs}^{\prime}$,
$\mathsf{distinct}~{}(\isaid{x}\mathrel{\\#}\isaid{vs}^{\prime})$ and the
remaining two (unchanged) assumptions of the lemma.

To make the proof more readable, we introduce some abbreviations. We
abbreviate the (unfolded) language non-membership condition to

$\displaystyle F$
$\displaystyle\>\longleftrightarrow\>\isaid{v}\>\neq\sum_{\sigma\>\in\>\mathsf{substs}\>(\\{\isaid{x}\\}\,\cup\,\mathsf{set}\>\isaid{vs}^{\prime})\>\isaid{H}}\isaid{eval}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}$

and we also introduce abbreviations the verifier’s degree, variable, and
evaluation checks and for the recursive check:

$\displaystyle C_{\isaid{ver}}$
$\displaystyle\>\longleftrightarrow\>\isaid{deg}~{}\hat{\isaid{q}}\leq\isaid{deg}~{}\isaid{p}\>\land\>\isaid{vars}~{}\hat{\isaid{q}}\subseteq\\{\isaid{x}\\}$
$\displaystyle\hskip
28.45274pt\>\land\>\isaid{v}=\sum_{\isaid{h}\in\isaid{H}}\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{h}],$
$\displaystyle C_{\isaid{rec}}~{}\isaid{r}_{1}~{}\isaid{rs}$
$\displaystyle\>\longleftrightarrow\>\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}^{\prime}~{}(\isaid{H},\>\isaid{p}^{\prime}\>\isaid{r}_{1},\>\isaid{v}^{\prime}\>\isaid{r}_{1})~{}\isaid{r}_{1}~{}(\mathsf{zip}~{}\isaid{vs}~{}\isaid{rs}),$

where the prover pr’s polynomial $\hat{\isaid{q}}$, the prover pr’s updated
state $\isaid{s}^{\prime}$, and the reduced sumcheck instance’s polynomial
$\isaid{p}^{\prime}$ and target value $\isaid{v}^{\prime}$ are defined as
follows:

$\displaystyle\hat{\isaid{q}}$
$\displaystyle=\mathsf{fst}~{}(\isaid{pr}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{x}~{}\isaid{vs}~{}\isaid{r}~{}\isaid{s}),$
$\displaystyle\isaid{s}^{\prime}$
$\displaystyle=\mathsf{snd}~{}(\isaid{pr}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{x}~{}\isaid{vs}~{}\isaid{r}~{}\isaid{s}),$
$\displaystyle\isaid{p}^{\prime}~{}\isaid{r}_{1}$
$\displaystyle=\isaid{inst}~{}\isaid{p}~{}[\isaid{x}\mapsto\isaid{r}_{1}],$
$\displaystyle\isaid{v}^{\prime}~{}\isaid{r}_{1}$
$\displaystyle=\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{r}_{1}].$

Here, $\mathsf{fst}$ and $\mathsf{snd}$ denote a pair’s first and second
projection respectively.

We start the proof with the following series of (in)equations, which we
explain below.

$\displaystyle\begin{split}&\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}}[\>\\\
&\qquad\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}~{}(\isaid{H},\isaid{p},\isaid{v})~{}\isaid{r}~{}(\mathsf{zip}~{}(\isaid{x}\mathrel{\\#}\isaid{vs})~{}(\isaid{r}_{1}\mathrel{\\#}\isaid{rs}))\\\
&\qquad\>\land\>F\>]\end{split}$
$\displaystyle=\>\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}}[\>C_{\isaid{ver}}\>\land\>C_{\isaid{rec}}~{}\isaid{r}_{1}~{}\isaid{rs}\>\land\>F\>]$
(15)
$\displaystyle\begin{split}&=\>\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}}[\>C_{\isaid{ver}}\>\land\>C_{\isaid{rec}}~{}\isaid{r}_{1}~{}\isaid{rs}\>\land\>F\>\land\>\hat{\isaid{q}}\neq\isaid{q}\>]\\\
\end{split}$ (16)
$\displaystyle\begin{split}&\leq\>\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}}[\>C_{\isaid{ver}}\>\land\>C_{\isaid{rec}}~{}\isaid{r}_{1}~{}\isaid{rs}\>\land\>\hat{\isaid{q}}\neq\isaid{q}\>]\\\
\end{split}$ (17)

In (15), we simplify the $\mathsf{zip}$ expression to
$(\isaid{x},\isaid{r}_{1})\mathrel{\\#}\mathsf{zip}~{}\isaid{vs}~{}\isaid{rs}^{\prime}$
and unfold the $\mathsf{sumcheck}$ definition. To obtain (16), we split the
resulting probability into a sum of two cases, depending on whether or not
$\hat{\isaid{q}}=\isaid{q}$ holds, where

$\isaid{q}=\sum_{\sigma\,\in\,\mathsf{substs}\>(\mathsf{set}\>\isaid{vs})\>\isaid{H}}\isaid{inst}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}$

is the honest prover’s polynomial. When $\hat{\isaid{q}}=\isaid{q}$, the
probability is $0$ and hence disappears due to a contradiction between $F$ and
the evaluation check in $C_{\isaid{ver}}$, which we derive using the lemmas
eval_sum_inst and sum_merge from Section IV-A. In (17), we over-approximate
the remaining case by removing $F$.

Next, we split the probability once more into a sum of two cases, this time
depending on whether or not
$\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{r}_{1}]=\isaid{eval}~{}\isaid{q}~{}[\isaid{x}\mapsto\isaid{r}_{1}]$
holds.

$\displaystyle\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}}[\>C_{\isaid{ver}}\>\land\>C_{\isaid{rec}}~{}\isaid{r}_{1}~{}\isaid{rs}\>\land\>\hat{\isaid{q}}\neq\isaid{q}\>]$
$\displaystyle=\>\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}}[\>C_{\isaid{ver}}\>\land\>C_{\isaid{rec}}~{}\isaid{r}_{1}~{}\isaid{rs}\>\land\>\hat{\isaid{q}}\neq\isaid{q}\>\land\>$
$\displaystyle\hskip
73.97716pt\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{r}_{1}]=\isaid{eval}~{}\isaid{q}~{}[\isaid{x}\mapsto\isaid{r}_{1}]\>]$
$\displaystyle\,+\>\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}}[\>C_{\isaid{ver}}\>\land\>C_{\isaid{rec}}~{}\isaid{r}_{1}~{}\isaid{rs}\>\land\>\hat{\isaid{q}}\neq\isaid{q}\>\land\>$
$\displaystyle\hskip
73.97716pt\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{r}_{1}]\neq\isaid{eval}~{}\isaid{q}~{}[\isaid{x}\mapsto\isaid{r}_{1}]\>]$
$\displaystyle=\>\textsf{Pr}_{\isaid{left}}+\textsf{Pr}_{\isaid{right}}$ (18)

The final equation (18) above just introduces the abbreviations
$\textsf{Pr}_{\isaid{left}}$ and $\textsf{Pr}_{\isaid{right}}$ for the two
probabilities on its left-hand side. We now bound each of these probabilities
separately. By the degree and variable checks in $C_{\isaid{ver}}$, the
lemma’s first assumption, and the roots locale assumption, the distinct
polynomials q and $\hat{\isaid{q}}$ coincide on at most d values. Hence, we
have

$\displaystyle\textsf{Pr}_{\isaid{left}}$
$\displaystyle\leq\frac{\isaid{d}}{\lvert\mathbb{A}\rvert}.$ (19)

We derive a bound for the probability $\textsf{Pr}_{\isaid{right}}$ as follows
using the induction hypothesis.

$\displaystyle\textsf{Pr}_{\isaid{right}}$
$\displaystyle\>\leq\>\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}}[\>C_{\isaid{rec}}~{}\isaid{r}_{1}~{}\isaid{rs}\,\>\land\>\,{}$
$\displaystyle\hskip
55.48286pt\isaid{eval}~{}\hat{\isaid{q}}~{}[\isaid{x}\mapsto\isaid{r}_{1}]\neq\isaid{eval}~{}\isaid{q}~{}[\isaid{x}\mapsto\isaid{r}_{1}]\>]$
(20)
$\displaystyle\>=\>\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}}[\>C_{\isaid{rec}}~{}\isaid{r}_{1}~{}\isaid{rs}\,\>\land\>\,{}$
$\displaystyle\hskip
55.48286pt\isaid{v}^{\prime}~{}\isaid{r}_{1}\>\neq\sum_{\sigma\,\in\,\mathsf{subst}\>(\mathsf{set}\>\isaid{vs}^{\prime})\>\isaid{H}}\isaid{eval}~{}(\isaid{p}^{\prime}~{}\isaid{r}_{1})~{}\textstyle\scalebox{0.9}{$\sigma$}\>]$
(21)
$\displaystyle\>\leq\>\frac{1}{\lvert\mathbb{A}\rvert}\sum_{\alpha\in\mathbb{A}}\textsf{Pr}_{\isaid{rs}}[\>C_{\isaid{rec}}~{}\textstyle\scalebox{0.9}{$\alpha$}~{}\isaid{rs}\,\>\land\>\,{}$
$\displaystyle\hskip
73.97716pt\isaid{v}^{\prime}~{}\textstyle\scalebox{0.9}{$\alpha$}\>\neq{\displaystyle\sum_{\sigma\,\in\,\mathsf{subst}\>(\mathsf{set}\>\isaid{vs}^{\prime})\>\isaid{H}}\isaid{eval}~{}(\isaid{p}^{\prime}~{}\textstyle\scalebox{0.9}{$\alpha$})~{}\textstyle\scalebox{0.9}{$\sigma$}}\>]$
(22)
$\displaystyle\>\leq\>\frac{1}{\lvert\mathbb{A}\rvert}\sum_{\alpha\in\mathbb{A}}\frac{\isaid{d}\cdot\mathsf{length}~{}\isaid{vs}^{\prime}}{\lvert\mathbb{A}\rvert}$
(23)
$\displaystyle\>\leq\>\frac{\isaid{d}\cdot\mathsf{length}~{}\isaid{vs}^{\prime}}{\lvert\mathbb{A}\rvert}.$
(24)

The inequality (20) holds by monotonicity of Pr. The equality (21) holds by
definition of $(\isaid{v}^{\prime}~{}\isaid{r}_{1})$ and since

$\displaystyle\isaid{eval}~{}\isaid{q}~{}[\isaid{x}\mapsto\isaid{r}_{1}]=\sum_{\sigma\,\in\,\mathsf{subst}\>(\mathsf{set}\>\isaid{vs}^{\prime})\>\isaid{H}}\isaid{eval}~{}(\isaid{p}^{\prime}~{}\isaid{r}_{1})~{}\textstyle\scalebox{0.9}{$\sigma$},$

by the lemma eval_sum_inst_commute from Section IV-A. To derive (22), we use a
lemma about probabilities that allows us to remove $\isaid{r}_{1}$ from the
probability space and to sum over uniformly chosen instantiations with
concrete values instead. This step is required for the application of the
induction hypothesis.

In (23), we apply the induction hypothesis which reads as follows: _for all
_s_ , _p_ , _v_ , and _r__ , we have

$\displaystyle\textsf{Pr}_{\isaid{rs}\>\in\>\mathsf{tuples}\,(\mathsf{length}\>\isaid{vs}^{\prime}))}[$
$\displaystyle\quad\;\mathsf{sumcheck}~{}\isaid{pr}~{}\isaid{s}~{}(\isaid{H},\;\isaid{p},\;\isaid{v})~{}\isaid{r}~{}(\mathsf{zip}~{}\isaid{vs}^{\prime}~{}\isaid{rs})\>\land\>{}$
$\displaystyle\quad\;\isaid{v}\>\neq\sum_{\sigma\>\in\>\mathsf{substs}\>(\mathsf{set}\>\isaid{vs}^{\prime})\>\isaid{H}}\isaid{eval}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}$
$\displaystyle]\leq\frac{\isaid{d}\cdot\mathsf{length}~{}\isaid{vs}^{\prime}}{\lvert\mathbb{A}\rvert},$

provided that
$\isaid{vars}~{}\isaid{p}\subseteq\mathsf{set}~{}\isaid{vs}^{\prime}$,
$\isaid{deg}~{}\isaid{p}\leq\isaid{d}$,
$\mathsf{distinct}~{}\isaid{vs}^{\prime}$ and $\isaid{H}\neq\emptyset$. We
respectively instantiate s, p, v, and r in the induction hypothesis with
$\isaid{s}^{\prime}$,
$(\isaid{p}^{\prime}~{}\textstyle\scalebox{0.9}{$\alpha$})$,
$(\isaid{v}^{\prime}~{}\textstyle\scalebox{0.9}{$\alpha$})$, and  $\alpha$ as
introduced above. The resulting instantiated assumptions follow from those of
the induction step. The final simplification step in (24) yields the desired
bound for $\textsf{Pr}_{\isaid{right}}$.

We can now continue from (18) to finish the proof of the inductive step as
follows.

$\displaystyle\textsf{Pr}_{\isaid{r}_{1}\mathrel{\\#}\isaid{rs}}[\>C_{\isaid{ver}}\>\land\>C_{\isaid{rec}}~{}\isaid{r}_{1}~{}\isaid{rs}\>\land\>\hat{\isaid{q}}\neq\isaid{q}\>]$
$\displaystyle\>=\>\frac{\isaid{d}}{\lvert\mathbb{A}\rvert}+\frac{\isaid{d}\cdot(\mathsf{length}~{}\isaid{vs}^{\prime})}{\lvert\mathbb{A}\rvert}$
$\displaystyle\>\leq\>\frac{\isaid{d}\cdot\mathsf{Suc}~{}(\mathsf{length}~{}\isaid{vs}^{\prime})}{\lvert\mathbb{A}\rvert}.$

This completes the soundness proof. ∎

###  V-C Differences with Pen-and-Paper Proofs

Common pen-and-paper proofs of completeness and soundness generally gloss over
several details that we had to make precise in our formal proof.

These proofs usually proceed by induction over the arity of the polynomial
(cf. Appendix A), ignoring the aforementioned fact that the arity of the
polynomial may decrease by more than one in each round. Instead, our proof
proceeds by induction on an explicit list of variables which contains all of
the variables of the sumcheck polynomial, even if a particular variable never
actually appears. Hence, the informal notation
$\isaid{p}(X_{1},\ldots,X_{\isaid{n}})$ gives an upper bound on the set of
variables that actually occur in p. In an early stage of our development, we
attempted an induction over the arity of p. However, this required stronger
assumptions about polynomials that fail to hold for polynomials represented in
a unique normal form, as is the case for our instantiation in Section VI. For
example, we had initially formulated the locale assumptions vars_add and
vars_inst from Figure 3 with equalities, which we subsequently had to weaken
to set inclusions.

Differently from some informal presentations [64], our inductive security
analysis uses (constant) polynomials of arity zero as the base case, rather
than (univariate) polynomials of arity one. This makes the base case trivial
and avoids the repetition of similar reasoning in the base case and inductive
steps of the analysis.

Moreover, we had to fully specify all probability spaces involved, another
important detail that is often omitted in less formal proofs. This required
proving some additional lemmas to reduce the dimension of the probability
space in the inductive step and enable the use of the induction hypothesis.

##  VI Instantiation with Multivariate Polynomials

Our formalization of the sumcheck protocol in the previous section relies on
the abstract functions vars, deg, eval and inst and a set of assumptions about
them. So far, we have not shown that the assumptions are realizable by any
particular mathematical structure. Instantiating the abstract type ’p with a
concrete type of multivariate polynomials (Section VI-A), defining concrete
instances of the four functions (Section VI-B), and proving the associated
assumptions (Section VI-C) completes the formalization of the completeness and
soundness proofs of the sumcheck protocol for the concrete case of
polynomials. Furthermore, this step proves the consistency of our
axiomatization and provides confidence in the applicability of our abstract
formalization. To achieve this, we use existing Isabelle/HOL libraries for
univariate polynomials [65] and for multivariate polynomials [51]. The latter
also connects univariate with multivariate polynomials with at most one
variable.

###  VI-A The Type of Multivariate Polynomials

The multivariate polynomials of [51] rely on the type of polynomial mappings
from the Isabelle/HOL library, which is defined to be isomorphic to the set of
functions that are zero “almost everywhere”, i.e., on all but a finite number
of arguments. In Isabelle, this type is defined as follows:

$\isakw{typedef
}\isaid{'a}\Rightarrow_{0}\\!\isaid{'b}=\\{\isaid{f}::\isaid{'a}\Rightarrow\isaid{'b::zero}\mid\mathsf{finite}~{}\\{\isaid{x}\mid\isaid{f}~{}\isaid{x}\neq
0\\}\\}$

This construction defines a new type from the indicated set of functions and
comes with the morphism
$\mathsf{lookup}::(\isaid{'a}\Rightarrow_{0}\\!\isaid{'b})\Rightarrow(\isaid{'a}\Rightarrow\isaid{'b})$,
which opens the polynomial mapping abstraction and its inverse
$\mathsf{Abs\\_poly\\_mapping}$, which creates such an abstraction. The
function
$\isaid{keys}::(\isaid{'a}\Rightarrow_{0}\isaid{'b})\Rightarrow\isaid{'a set}$
returns the set of arguments on which the polynomial mapping results in a non-
zero value. Polynomial mappings have a rich algebraic structure, and are
defined in the theory [66].

We now recap how the authors of [51] construct the types of monomials and then
multivariate polynomials using polynomial mappings. We will use the following
running example throughout this subsection to clarify the concepts introduced.
The multivariate polynomial

$p(x_{1},x_{2},x_{3})=3x_{1}^{2}x_{2}x_{3}+2x_{1}x_{3}+x_{3}^{2}$

has three variables and three _monomials_ with non-zero coefficients, namely,
$m_{1}=x_{1}^{2}x_{2}x_{3}$ with coeffcient $3$, $m_{2}=x_{1}x_{3}$ with
coefficient $2$, and $m_{3}=x_{3}^{2}$ with coefficient $1$.

First, we can use polynomial mappings of type
$\isaid{nat}\Rightarrow_{0}\isaid{nat}$ to represent monomials by mapping
variables to their exponent. For example, the monomial $m_{1}$ would be
represented as
$\mathsf{Abs\\_poly\\_mapping}~{}((\lambda\isaid{x}.\,0)(1\mapsto 2,2\mapsto
1,3\mapsto 1))$, which we abbreviate to $[1\mapsto 2,2\mapsto 1,3\mapsto 1]$.
The type of multivariate polynomials then maps monomials of type
$\isaid{nat}\Rightarrow_{0}\isaid{nat}$ to their coefficients of type ’a and
is defined by

$\isakw{typedef }\isaid{'a
}\isaid{mpoly}=\isaid{UNIV}::((\isaid{nat}\Rightarrow_{0}\isaid{nat})\Rightarrow_{0}\isaid{'a})~{}\isaid{set}.$

Here, UNIV is the set of all elements of the indicated type. This type
definition comes with the morphisms $\mathsf{mapping\\_of}$, which opens the
type ’a mpoly, returning the underlying polynomial mapping of type
$(\isaid{nat}\Rightarrow_{0}\isaid{nat})\Rightarrow_{0}\isaid{'a}$.
Accordingly, the polynomial $p(x_{1},x_{2},x_{3})$ can be represented by
$[m_{1}\mapsto 3,m_{2}\mapsto 2,m_{3}\mapsto 1]$, i.e., mapping all other
monomials to 0. Note that $p$ in this example is of type nat mpoly.

###  VI-B Functions on Multivariate Polynomials

We now define the functions vars, deg, eval and inst to instantiate our
locale. While we defined polynomial instantiation ourselves, the former three
are already defined in [51].

####  VI-B1 Variables

The variable function for a multivariate polynomial is defined by

definition $\displaystyle\mathsf{vars}::\isaid{'a mpoly}\Rightarrow\isaid{nat
set}\isakw{ where }$
$\displaystyle\mathsf{vars}~{}\isaid{p}=\bigcup_{m\,\in\,\mathsf{keys}\>(\mathsf{mapping\\_of}\>\isaid{p})}(\mathsf{keys}~{}\isaid{m}).$

Here, $\mathsf{keys}~{}(\mathsf{mapping\\_of}~{}\isaid{p})$ is the set of the
polynomial p’s monomials and the union of these monomials’ sets of keys
constitutes p’s variables. We use this function to instantiate our variables
function in the locale. With our running example, we have
$\mathsf{vars}~{}\isaid{p}=\\{1,2,3\\}$, representing the variables
$x_{1},x_{2},x_{3}$.

####  VI-B2 Degree

As our degree function, deg, we use

$\displaystyle\isakw{lift\\_definition }\mathsf{total\\_degree}::\isaid{'a
mpoly}\Rightarrow\isaid{nat}~{}\isakw{is }$ $\displaystyle\quad\lambda
p.\>\mathsf{Max}~{}(\\{0\\}\cup\\{\sum_{\isaid{v}\,\in\,\mathsf{keys}\>\isaid{m}}\mathsf{lookup}~{}\isaid{m}~{}\isaid{v}\mid\isaid{m}\in\mathsf{keys}~{}\isaid{p}\\}).$

This function returns the maximum of any monomial’s sum of exponents in the
polynomial. More precisely, the expression $(\mathsf{keys}~{}\isaid{p})$
denotes the set of p’s monomials and the sum adds up the exponents of each of
the monomial m’s variables x. This definition makes use of Isabelle’s lifting
definition mechanism, which allows one to write definitions in terms of the
concrete representations of a newly defined type (such as ’a mpoly) and
automatically inserts the required morphisms. Here, the $\lambda$-abstracted p
is of type
$((\isaid{nat}\Rightarrow_{0}\isaid{nat})\Rightarrow\isaid{'a})\Rightarrow\isaid{nat}$,
which is automatically lifted to the argument type ’a mpoly of the defined
function using the morphism $\mathsf{mapping\\_of}$. For our running example,
we thus get $\mathsf{total\\_degree}~{}\isaid{p}=4$ . We note that we apply
this function only to multivariate polynomials in at most one variable, where
the definition collapses to the expected one.

####  VI-B3 Evaluation

We use the existing function $\mathsf{insertion}$, which is defined as
follows.

definition
$\displaystyle\mathsf{insertion\\_fun}::(\isaid{nat}\Rightarrow\isaid{'a})\Rightarrow$
$\displaystyle\hskip
96.73936pt((\isaid{nat}\Rightarrow_{0}\isaid{nat})\Rightarrow\isaid{'a})\Rightarrow\isaid{'a}$
where
$\displaystyle\mathsf{insertion\\_fun}~{}\textstyle\scalebox{0.9}{$\sigma$}~{}\isaid{p}=$
$\displaystyle(\sum_{\isaid{m}\,\in\,\mathsf{keys}\>\isaid{p}}\isaid{p}~{}\isaid{m}\cdot(\prod_{\isaid{v}\,\in\,\mathsf{keys}\>\isaid{m}}(\textstyle\scalebox{0.9}{$\sigma$}~{}\isaid{v})^{\mathsf{lookup}\>\isaid{m}\>\isaid{v}}))$

This definition, through lifting, yields the $\mathsf{insertion}$ function of
type $(\isaid{nat}\Rightarrow\isaid{'a})\Rightarrow\isaid{'a
mpoly}\Rightarrow\isaid{'a}$. We then define our equivalent evaluation
function $\mathsf{eval}::\isaid{'a
mpoly}\Rightarrow(\isaid{nat},\isaid{'a})~{}\isaid{subst}\Rightarrow\isaid{'a}$
by swapping its arguments and converting our partial substitution into a total
one (with some irrelevant undefined values). Taking the substitution
$\textstyle\scalebox{0.9}{$\sigma$}=[1\mapsto 3,2\mapsto 1,3\mapsto 2]$ in our
running example
$p(x_{1},x_{2},x_{3})=3x_{1}^{2}x_{2}x_{3}+2x_{1}x_{3}+x_{3}^{2}$ replaces
$x_{1}$ by $3$, $x_{2}$ by $1$ and $x_{3}$ by $2$ in $p$. Therefore,
$\isaid{eval}~{}p~{}\textstyle\scalebox{0.9}{$\sigma$}=3\cdot 3^{2}\cdot
1\cdot 2+2\cdot 3\cdot 2+2^{2}=70$.

####  VI-B4 Instantiation

Polynomial instantiation substitutes certain variables with values to obtain a
polynomial of smaller arity. It can be understood as a partial evaluation. In
contrast to evaluation, not all variables need to be instantiated. However,
instantiating all variables is equivalent to evaluation. For our example
polynomial $p(x_{1},x_{2},x_{3})=3x_{1}^{2}x_{2}x_{3}+2x_{1}x_{3}+x_{3}^{2}$
and the substitution $\textstyle\scalebox{0.9}{$\sigma$}=[1\mapsto 3,2\mapsto
1]$, which instantiates $x_{1}$ and $x_{2}$ but not $x_{3}$, the resulting
polynomial is $33x_{3}+x_{3}^{2}$. We will discuss this example in more
detail, while introducing the definitions.

We first define instantiation on monomials and then extend it to polynomials.
Recall that the monomials of $p$ are $x_{1}^{2}x_{2}x_{3}$, $x_{1}x_{3}$ and
$x_{3}^{2}$. Applying the substitution to each monomial independently yields
$27x_{3}$, $6x_{3}$ and $x_{3}^{2}$. We note that each of these terms has a
coefficient and a residual monomial, which we respectively define in the
functions $\mathsf{inst\\_mon\\_coeff}$ and $\mathsf{inst\\_mon\\_resid}$ as
follows.

lift_definition $\displaystyle\mathsf{inst\\_mon\\_coeff}::$
$\displaystyle(\isaid{nat}\Rightarrow_{0}\isaid{nat})\Rightarrow(\isaid{nat},\isaid{'a})~{}\isaid{subst}\Rightarrow\isaid{'a}$
is
$\displaystyle\lambda\isaid{m}\>\textstyle\scalebox{0.9}{$\sigma$}.\>(\prod_{\isaid{v}\,\in\,\isaid{dom}\>\sigma}(\textstyle\scalebox{0.9}{$\sigma$}~{}\isaid{v})^{\isaid{m}\>\isaid{v}})$
lift_definition $\displaystyle\mathsf{inst\\_mon\\_resid::}$
$\displaystyle(\isaid{nat}\Rightarrow_{0}\isaid{nat})\Rightarrow(\isaid{nat},\isaid{'a})~{}\isaid{subst}\Rightarrow(\isaid{nat}\Rightarrow_{0}\isaid{nat})$
is
$\displaystyle\lambda\isaid{m}\>\textstyle\scalebox{0.9}{$\sigma$}\>\isaid{v}.\>\isakw{if
}\isaid{v}\notin\isaid{dom}~{}\textstyle\scalebox{0.9}{$\sigma$}\isakw{ then
}\isaid{m}~{}\isaid{v}\isakw{ else }0$

Once we have applied the substitution to each monomial, it remains to multiply
these by their original coefficients in p and group them by the residual
monomials. This is what the function $\mathsf{inst\\_fun}$ will do, which in
our example simplifies $3\cdot 9x_{3}+2\cdot 3x_{3}+x_{3}^{2}$ to the desired
$33x_{3}+x_{3}^{2}$. The function is defined as follows:

$\displaystyle\isakw{definition
}\mathsf{inst\\_fun}::((\isaid{nat}\Rightarrow_{0}\isaid{nat})\Rightarrow\isaid{'a})\Rightarrow$
$\displaystyle\phantom{\isakw{definition
}\mathsf{inst\\_fun}::{}}(\isaid{nat},\isaid{'a})~{}\isaid{subst}\Rightarrow(\isaid{nat}\Rightarrow_{0}\isaid{nat})\Rightarrow\isaid{'a}$
where
$\displaystyle\quad\mathsf{inst\\_fun}~{}\isaid{p}~{}\textstyle\scalebox{0.9}{$\sigma$}=$
$\displaystyle\qquad(\lambda\isaid{m}.\>\sum_{\isaid{m}^{\prime}\,\mid\,\mathsf{inst\\_mon\\_resid}\>\isaid{m}^{\prime}\>\sigma\,=\,\isaid{m}}\isaid{p}~{}\isaid{m}^{\prime}\cdot\mathsf{inst\\_mon\\_coeff}~{}\isaid{m}^{\prime}\>\textstyle\scalebox{0.9}{$\sigma$}).$

Finally, we obtain the function $\mathsf{inst}$ of the correct type $\isaid{'a
mpoly}\Rightarrow(\isaid{nat},\isaid{'a})~{}\isaid{subst}\Rightarrow\isaid{'a
mpoly}$ through lifting.

###  VI-C Proving the Assumptions

We now prove that the locale assumptions from Section IV-A hold for the
functions $\mathsf{vars}$, $\mathsf{total\\_degree}$, $\mathsf{eval}$, and
$\mathsf{inst}$ on polynomials. Note that we discuss the assumptions relating
to inst separately, although in Figure 3 they are grouped with those for vars,
deg and eval.

####  VI-C1 Variables Assumptions

There are existing library lemmas for the function $\mathsf{vars}$ that
exactly correspond to our assumptions vars_finite and vars_add, and the proof
of vars_zero follows directly from the definitions of the variable function
and the zero polynomial.

####  VI-C2 Degree Assumptions

We must prove the assumptions deg_zero and deg_add for the total degree
function $\mathsf{total\\_degree}$. The first one is covered by a library
lemma. We establish deg_add separately. Its proof uses the definition of total
degree and requires simple properties about the $\mathsf{Max}$ function and
the addition of multivariate polynomials.

####  VI-C3 Evaluation Assumptions

We prove the assumptions eval_zero and eval_add directly using existing
library lemmas about the $\mathsf{insertion}$ function and the definition of
$\mathsf{eval}$.

####  VI-C4 Instantiation Assumptions

The proofs of the instantiation assumptions vars_inst, deg_inst and eval_inst
required more work since the concept of polynomial instantiation did not exist
in the existing theories. Although the proofs were more elaborate than for the
other assumptions, they did not require more than basic theorems about sums,
maps, and finiteness, along with the definitions of monomial and polynomial
instantiation.

####  VI-C5 Roots Assumption

We prove the roots assumption using a lemma stating that the number of roots
of a univariate polynomial (of type ’a mpoly) is bounded by its total degree
(which coincides with the expected degree for such polynomials). We first
establish this result for a specialized type, ’a poly, of univariate
polynomials, which exists in the Isabelle/HOL library, and then transfer it to
univariate polynomials of type ’a mpoly. We explain the type ’a poly in
Appendix B and present the proof of the roots bound in Appendix C.

##  VII Conclusion and Future Work

In this paper, we formally verified the completeness and soundness properties
of the sumcheck protocol. Our work took place in three stages:

  * •

Producing a new pen-and-paper security analysis of the sumcheck protocol with
enough detail for a machine-checkable analysis;

  * •

Distilling the necessary properties of multivariate polynomials used in the
sumcheck protocol, and proving the security of a generalized sumcheck protocol
based on these properties in Isabelle; and

  * •

Showing that existing Isabelle formalizations of multivariate polynomials
satisfy the necessary properties, leading to a full security analysis of the
classic sumcheck protocol.

The sumcheck protocol is widely used, with applications ranging from
computational complexity theory to cryptography. We hope that the contrast
between the apparent straightforwardness of the well-known pen-and-paper
proofs for the sumcheck protocol and the thoroughness of our formalization
motivates the use of formal verification. Formalizing proofs will be crucial
to prevent errors and ensure security as cryptographic systems become
increasingly complex.

We also hope that our formalization helps to produce machine-checkable
security analyses of other recursive protocols in the future, whether they are
based on the sumcheck protocol, or other probabilistic proof systems. Future
extensions of our work would be to create machine-checkable proofs of
statements in complexity theory relying on the sumcheck protocol [50, 44, 45,
46, 47, 48], analyses of protocols such as the GKR protocol [32], which rely
directly on sumcheck, generalisations of the sumcheck protocol to
cryptographic groups [42] and tensor codes [43], and producing verified
implementations of these protocols using the Isabelle code generator. Setting
up the code generator to extract an implementation of our verified sumcheck
protocol should be feasible with limited additional effort given the extensive
support for executable polynomials in [51].

## Acknowledgments

We would like to thank the anonymous reviewers, the shepherd, and David Basin
for their useful feedback, which helped improving the paper. The first author
received the support of a fellowship (code LCF/BQ/EU20/11810060) from La Caixa
Foundation (ID 100010434).

## References

  * [1] Shafi Goldwasser, Silvio Micali and Charles Rackoff  “The Knowledge Complexity of Interactive Proof-Systems (Extended Abstract)”  In _Proceedings of the 17th Annual ACM Symposium on Theory of Computing_ , STOC ’85, 1985, pp. 291–304
  * [2] László Babai  “Trading Group Theory for Randomness”  In _Proceedings of the 17th Annual ACM Symposium on Theory of Computing_ , STOC ’85, 1985, pp. 421–429
  * [3] Eiichiro Fujisaki and Tatsuaki Okamoto  “Statistical Zero Knowledge Protocols to Prove Modular Polynomial Relations”  In _Proceedings of the 17th Annual International Cryptology Conference_ 1294, CRYPTO ’97, 1997, pp. 16–30
  * [4] Ivan Damgård and Eiichiro Fujisaki  “A Statistically-Hiding Integer Commitment Scheme Based on Groups with Hidden Order”  In _Proceedings of the 8th International Conference on the Theory and Application of Cryptology and Information Security_ , ASIACRYPT ’02, 2002, pp. 125–142
  * [5] Eli Ben-Sasson, Alessandro Chiesa, Eran Tromer and Madars Virza  “Succinct Non-Interactive Zero Knowledge for a von Neumann Architecture”  In _Proceedings of the 23rd USENIX Security Symposium_ , USENIX ’14, 2014, pp. 781–796
  * [6] Josh Swihart, Benjamin Winston and Sean Bowe  “ZCash Counterfeiting Vulnerability Successfully Remediated”, 2019  URL: https://electriccoin.co/blog/zcash-counterfeiting-vulnerability-successfully-remediated/
  * [7] Benedikt Bünz, Ben Fisch and Alan Szepieniec  “Transparent SNARKs from DARK Compilers”  In _Proceedings of the 39th Annual International Conference on the Theory and Applications of Cryptographic Techniques_ , EUROCRYPT ’20, 2020, pp. 677–706
  * [8] Alexander R Block et al.  “Time- and Space-Efficient Arguments from Groups of Unknown Order”  In _Proceedings of the 41st Annual International Cryptology Conference_ , CRYPTO ’21, 2021, pp. 123–152
  * [9] Arasu Arun et al.  “Dew: A Transparent Constant-Sized Polynomial Commitment Scheme”  In _Proceedings of the 26th IACR International Conference on Practice and Theory of Public-Key Cryptography_ , PKC ’23, 2023, pp. 542–571
  * [10] Benedikt Bünz and Ben Fisch  “Schwartz-Zippel for multilinear polynomials mod N”, IACR Cryptology ePrint Archive, Report 2022/458, 2022  URL: https://eprint.iacr.org/2022/458
  * [11] Jonathan Bootle, Vadim Lyubashevsky, Ngoc Khanh Nguyen and Gregor Seiler  “A Non-PCP Approach to Succinct Quantum-Safe Zero-Knowledge”  In _Proceedings of the 40th Annual International Cryptology Conference_ , CRYPTO ’20, 2020, pp. 441–469
  * [12] Thomas Attema, Ronald Cramer and Lisa Kohl  “A Compressed Sigma-Protocol Theory for Lattices”  In _Proceedings of the 41st Annual International Cryptology Conference_ , CRYPTO ’21, 2021, pp. 549–579
  * [13] Martin R. Albrecht and Russell W. F. Lai  “Subtractive Sets over Cyclotomic Rings - Limits of Schnorr-Like Arguments over Lattices”  In _Proceedings of the 41st Annual International Cryptology Conference_ , CRYPTO ’21, 2021, pp. 519–548
  * [14] Benedikt Bünz et al.  “Bulletproofs: Short Proofs for Confidential Transactions and More”  In _Proceedings of the 39th IEEE Symposium on Security and Privacy_ , S&P ’18, 2018, pp. 315–334
  * [15] Jim Miller  “Coordinated disclosure of vulnerabilities affecting Girault, Bulletproofs, and PlonK”, 2022  URL: https://blog.trailofbits.com/2022/04/13/part-1-coordinated-disclosure-of-vulnerabilities-affecting-girault-bulletproofs-and-plonk/
  * [16] “ZenGo Zero Knowledge Paillier Implementation”  URL: https://github.com/ZenGo-X/zk-paillier
  * [17] “SecBit Labs Zero-Knowledge Proofs Toolkit”  URL: https://github.com/sec-bit/ckb-zkp
  * [18] “Dusk Network Plonk Implementation”  URL: https://github.com/dusk-network/plonk
  * [19] “Iden3 snarkjs Library”  URL: https://github.com/iden3/snarkjs
  * [20] “Consensys gnark Library”  URL: https://github.com/ConsenSys/gnark
  * [21] Mihir Bellare and Phillip Rogaway  “Code-based game-playing proofs and the security of triple encryption”  In _Cryptology ePrint Archive_ , 2004
  * [22] Manuel Barbosa et al.  “SoK: Computer-Aided Cryptography”  In _Proceedings of the 42nd IEEE Symposium on Security and Privacy_ , S&P ’21, 2021, pp. 777–795
  * [23] Jens Groth  “On the Size of Pairing-Based Non-Interactive Arguments”  In _Proceedings of the 35th Annual International Conference on the Theory and Applications of Cryptographic Techniques_ , EUROCRYPT ’16, 2016, pp. 305–326
  * [24] Bolton Bailey and Andrew Miller  “Formalizing Soundness Proofs of SNARKs”, IACR Cryptology ePrint Archive, Report 2023/656, 2023
  * [25] Bolton Bailey  “Formalization of SNARKs”, https://github.com/BoltonBailey/formal-snarks-project, last accessed 22.03.2023
  * [26] Denis Firsov and Dominique Unruh  “Zero-Knowledge in EasyCrypt”  In _Proceedings of the 36th IEEE Computer Security Foundations Symposium_ , CSF ’23, 2023, pp. 1–16
  * [27] Yuval Ishai, Eyal Kushilevitz, Rafail Ostrovsky and Amit Sahai  “Zero-Knowledge Proofs from Secure Multiparty Computation”  In _SIAM J. Comput._ 39, 2009, pp. 1121–1152
  * [28] Nikolaj Sidorenco, Sabine Oechsner and Bas Spitters  “Formal security analysis of MPC-in-the-head zero-knowledge protocols”  In _2021 IEEE 34th Computer Security Foundations Symposium (CSF)_ , CSF ’21, 2021, pp. 1–14
  * [29] José Bacelar Almeida et al.  “Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head”  In _Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security_ , CCS ’21
  * [30] José Bacelar Almeida, Denis Firsov, Tiago Oliveira and Dominique Unruh  “Schnorr protocol in Jasmin”, IACR Cryptology ePrint Archive, Report 2023/752, 2023  URL: https://eprint.iacr.org/2023/752.pdf
  * [31] Manuel Barbosa et al.  “Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium”  In _Proceedings of the 43rd Annual International Cryptology Conference_ , CRYPTO ’23, 2023, pp. 358–389
  * [32] Shafi Goldwasser, Yael Tauman Kalai and Guy N Rothblum  “Delegating computation: interactive proofs for muggles”  In _Journal of the ACM_ 62.4, 2015, pp. 1–64
  * [33] Srinath Setty  “Spartan: Efficient and General-Purpose zkSNARKs Without Trusted Setup”  In _Proceedings of the 40th Annual International Cryptology Conference_ , CRYPTO ’20, 2020, pp. 704–737
  * [34] Jonathan Bootle et al.  “Efficient Zero-Knowledge Arguments for Arithmetic Circuits in the Discrete Log Setting”  In _Proceedings of the 35th Annual International Conference on Theory and Application of Cryptographic Techniques_ , EUROCRYPT ’16, 2016, pp. 327–357
  * [35] Jonathan Bootle, Alessandro Chiesa and Jens Groth  “Linear-Time Arguments with Sublinear Verification from Tensor Codes”  In _Proceedings of the 18th Theory of Cryptography Conference_ , TCC ’20, 2020, pp. 19–46
  * [36] Jonathan Bootle, Alessandro Chiesa and Siqi Liu  “Zero-Knowledge Succinct Arguments with a Linear-Time Prover”  In _Proceedings of the 42nd Annual International Conference on Theory and Application of Cryptographic Techniques_ , EUROCRYPT ’22, 2022, pp. 275–304
  * [37] Noga Ron-Zewi and Ron D. Rothblum  “Proving as Fast as Computing: Succinct Arguments with Constant Prover Overhead”  In _Proceedings of the 54th Annual ACM Symposium on Theory of Computing_ , STOC ’22, 2022
  * [38] Justin Holmgren and Ron Rothblum  “Faster Sounder Succinct Arguments and IOPs”  In _Proceedings of the 42nd Annual International Cryptology Conference_ , CRYPTO ’22, 2022, pp. 474–503
  * [39] Graham Cormode, Michael Mitzenmacher and Justin Thaler  “Practical Verified Computation with Streaming Interactive Proofs”  In _Proceedings of the 3rd Innovations in Theoretical Computer Science Conference_ , ITCS ’12, 2012, pp. 90–112
  * [40] Alexander R. Block et al.  “Public-Coin Zero-Knowledge Arguments with (almost) Minimal Time and Space Overheads”  In _Proceedings of the 18th Theory of Cryptography Conference_ , TCC ’20, 2020, pp. 168–197
  * [41] Jonathan Bootle, Alessandro Chiesa, Yuncong Hu and Michele Orrù  “Gemini: Elastic SNARKs for Diverse Environments”  In _Proceedings of the 41st Annual International Conference on the Theory and Applications of Cryptographic Techniques_ , EUROCRYPT ’22, 2022, pp. 427–457
  * [42] Jonathan Bootle, Alessandro Chiesa and Katerina Sotiraki  “Sumcheck Arguments and their Applications” Extended version at https://eprint.iacr.org/2021/333.pdf.  In _Proceedings of the 41st Annual International Cryptology Conference_ , CRYPTO ’21, 2021, pp. 681–710
  * [43] Or Meir  “IP = PSPACE using error-correcting codes”  In _SIAM Journal on Computing_ 42, 2013, pp. 380–403
  * [44] Adi Shamir  “IP = PSPACE”  In _J. ACM_ 39.4, 1992, pp. 869–877
  * [45] Alexander Shen  “IP = PSPACE: simplified proof”  In _Journal of the ACM_ 39.4, 1992, pp. 878–880
  * [46] Ruta Jawale, Yael Tauman Kalai, Dakshita Khurana and Rachel Yun Zhang  “SNARGs for bounded depth computations and PPAD hardness from sub-exponential LWE”  In _Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing_ , STOC ’21, 2021, pp. 708–721
  * [47] Arka Rai Choudhuri et al.  “Finding a Nash equilibrium is no easier than breaking Fiat-Shamir”  In _Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing_ , STOC ’19, 2019, pp. 1103–1114
  * [48] Yael Tauman Kalai, Alex Lombardi and Vinod Vaikuntanathan  “SNARGs and PPAD Hardness from the Decisional Diffie-Hellman Assumption”  In _Proceedings of the 42nd Annual International Conference on the Theory and Applications of Cryptographic Techniques_ , EUROCRYPT ’23, 2023, pp. 470–498
  * [49] Ran Canetti et al.  “Fiat–Shamir From Simpler Assumptions”, Cryptology ePrint Archive, Report 2018/1004, 2018
  * [50] Carsten Lund, Lance Fortnow, Howard Karloff and Noam Nisan  “Algebraic Methods for Interactive Proof Systems”  In _J. ACM_ 39.4, 1992, pp. 859–868
  * [51] Christian Sternagel et al.  “Executable Multivariate Polynomials” https://isa-afp.org/entries/Polynomials.html, Formal proof development  In _Archive of Formal Proofs_ , 2010
  * [52] Shuo Chen, Jung Hee Cheon, Dongwoo Kim and Daejun Park  “Verifiable Computing for Approximate Computation”, IACR Cryptology ePrint Archive, Report 2019/762, 2019  URL: https://eprint.iacr.org/2019/762
  * [53] Rosario Gennaro, Craig Gentry, Bryan Parno and Mariana Raykova  “Quadratic Span Programs and Succinct NIZKs without PCPs”  In _Proceedings of the 32nd Annual International Conference on the Theory and Applications of Cryptographic Techniques_ , EUROCRYPT ’13’, 2013, pp. 626–645
  * [54] Bryan Parno, Jon Howell, Craig Gentry and Mariana Raykova  “Pinocchio: Nearly Practical Verifiable Computation”  In _Proceedings of the 2013 IEEE Symposium on Security and Privacy_ , S&P ’13, 2013, pp. 238–252
  * [55] Karim Baghery, Markulf Kohlweiss, Janno Siim and Mikhail Volkhov  “Another Look at Extraction and Randomization of Groth’s zk-SNARK”  In _Proceedings of the 25th International Conference on Financial Cryptography and Data Security_ , FC ’21, 2021, pp. 457–475
  * [56] Helger Lipmaa  “Simulation-Extractable SNARKs Revisited”, IACR Cryptology ePrint Archive, Report 2019/612, 2022  URL: https://eprint.iacr.org/2019/612
  * [57] “BabySNARK”  URL: https://github.com/initc3/babySNARK
  * [58] David Butler, Andreas Lochbihler, David Aspinall and Adrià Gascón  “Formalising $\Sigma$-Protocols and Commitment Schemes using CryptHOL”  In _Journal of Automated Reasoning_ 65.4 Springer, 2021, pp. 521–567
  * [59] Sunpill Kim and Yong Kiam Tan  “The Schwartz-Zippel Lemma” https://isa-afp.org/entries/Schwartz_Zippel.html, Formal proof development  In _Archive of Formal Proofs_ , 2023
  * [60] Azucena Garvía, Christoph Sprenger and Jonathan Bootle  “The Sumcheck Protocol” https://isa-afp.org/entries/Sumcheck_Protocol.html, Formal proof development  In _Archive of Formal Proofs_ , 2024
  * [61] Tobias Nipkow, Lawrence C. Paulson and Markus Wenzel  “Isabelle/HOL - A Proof Assistant for Higher-Order Logic” 2283, Lecture Notes in Computer Science, 2002  URL: https://doi.org/10.1007/3-540-45949-9
  * [62] Sanjeev Arora and Boaz Barak  “Computational Complexity: A Modern Approach”  Cambridge University Press, 2009
  * [63] Justin Thaler  “Proofs, Arguments, and Zero-Knowledge”  In _Foundations and Trends in Privacy and Security_ 4.2–4, 2022, pp. 117–660  DOI: 10.1561/3300000030
  * [64] Justin Thaler  “The Sum-Check Protocol” https://people.cs.georgetown.edu/jthaler/sumcheck.pdf
  * [65] “Isabelle/HOL Computational Algebra Library”  URL: https://isabelle.in.tum.de/library/HOL/HOL-Computational_Algebra
  * [66] Andreas Lochbihler and Florian Haftmann  “Theory HOL-Library.Poly_Mapping”  URL: https://isabelle.in.tum.de/library/HOL/HOL-Library/Poly_Mapping.html
  * [67] Brian Huffman, Clemens Ballarin, Amine Chaieb and Florian Haftmann  “Theory Polynomial”  URL: https://isabelle.in.tum.de/library/HOL/HOL-Computational_Algebra/Polynomial.html

##  Appendix A Completeness and Soundness of the Sumcheck Protocol

In this section, we carefully reprove the completeness and soundness
properties of the sumcheck protocol (II.6), thereby proving Theorem II.7.

In the soundness proof, we use probabilities in a loose manner without
specifying the underlying distributions. The proof should be easy to follow
without these details, which are explicitly defined in our formalization in
Section V-B.

###  A-A Completeness

This proof is by induction on the arity of p. We prove that II.6 will always
accept an instance
$(\mathbb{F},\isaid{H},\isaid{p},\isaid{v})\in\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$.
Recall that if
$(\mathbb{F},\isaid{H},\isaid{p},\isaid{v})\in\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$,
then

$\sum_{(x_{1},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}}}\isaid{p}(x_{1},\ldots,x_{\isaid{n}})=\isaid{v}\enspace.$
(25)

_Base Case._ In the base case, p has arity 0, hence (25) simplifies to
$\isaid{p}=\isaid{v}$. The verifier V checks whether $\isaid{p}=\isaid{v}$, so
the proof is accepted with probability $1$. This concludes the base case.

_Inductive Step._ Suppose $p$ has arity $\isaid{n}>0$. The induction
hypothesis states that for all
$(\mathbb{F},\isaid{H},\isaid{p}^{\prime},\isaid{v}^{\prime})\in\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
where $\isaid{p}^{\prime}$ has arity $\isaid{n}-1$, the verifier accepts with
probability $1$. We prove that the verifier accepts
$(\mathbb{F},\isaid{H},\isaid{p},\isaid{v})\in\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
with probability $1$.

Consider an execution of II.6. The prover P computes the honest message

$\isaid{q}(X):=\sum_{(x_{2},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}-1}}\isaid{p}(X,x_{2},\ldots,x_{\isaid{n}})\enspace,$
(26)

and sends it to the verifier V. Then V checks that q is univariate, which is
evident, and that q has degree at most $\isaid{deg}(\isaid{p})$, which follows
from the fact that q is a sum of evaluations of p.

The verifier check
$\isaid{v}\stackrel{{\scriptstyle?}}{{=}}\sum_{x\in\isaid{H}}\isaid{q}(x)$ is
satisfied because

$v=\sum_{(x_{1},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}}}p(x_{1},x_{2},\ldots,x_{\isaid{n}})=\sum_{x\in
H}q(x)\enspace,$

where the first equality follows from (25), and the second follows from (26).

Since the arity n of p is greater than 0, the protocol is now repeated over
the instance
$(\mathbb{F},\isaid{H},\isaid{p}^{\prime},\isaid{v}^{\prime})\in\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
where $\isaid{p}^{\prime}$ is the $(\isaid{n}-1)$-variate polynomial defined
by
$\isaid{p}^{\prime}(X_{2},\ldots,X_{\isaid{n}}):=\isaid{p}(\isaid{r}_{1},X_{2},\ldots,X_{\isaid{n}})$
and $\isaid{v}^{\prime}:=\isaid{q}(\isaid{r}_{1}).$ In order to apply the
induction hypothesis it remains to show that
$(\mathbb{F},\isaid{H},\isaid{p}^{\prime},\isaid{v}^{\prime})\in\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$,
which holds since

$\displaystyle\isaid{v}^{\prime}$
$\displaystyle=\isaid{q}(\isaid{r}_{1})=\sum_{(x_{2},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}-1}}\isaid{p}(\isaid{r}_{1},x_{2},\ldots,x_{\isaid{n}})\enspace,$
$\displaystyle=\sum_{(x_{2},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}-1}}\isaid{p}^{\prime}(x_{2},\ldots,x_{\isaid{n}}).$

Hence, V accepts the smaller instance
$(\mathbb{F},\isaid{H},\isaid{p}^{\prime},\isaid{v}^{\prime})$ with
probability 1 and therefore also the original instance
$(\mathbb{F},\isaid{H},\isaid{p},\isaid{v})$. ∎

###  A-B Soundness

The proof is again by induction on the arity of p. We show that for all
instances
$\mathit{sc}=(\mathbb{F},\isaid{H},\isaid{p},\isaid{v})\notin\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
and for all provers $\hat{\textbf{P}}$ the verifier V accepts with probability
at most $\isaid{n}\isaid{d}/|\mathbb{F}|$ where n is the arity of p and
$\isaid{deg}(\isaid{p})\leq\isaid{d}$. Somewhat more formally, we show that

$\displaystyle\textsf{Pr}_{\isaid{r}_{1},\ldots,\isaid{r}_{n}}[\textsf{acc}_{\mathit{sc}}]$
$\displaystyle\leq\frac{\isaid{n}\isaid{d}}{|\mathbb{F}|}\enspace,$

where
$\textsf{acc}_{\mathit{sc}}:=\langle\hat{\textbf{P}},\textbf{V}(\isaid{r}_{1},\ldots,\isaid{r}_{n})\rangle(\mathit{sc})=1\land\mathit{sc}\notin\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$,
i.e., the verifier accepts the instance
$\mathit{sc}\notin\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$.

_Base Case._ Recall that
$\mathit{sc}\notin\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$ means

$\isaid{v}\neq\sum_{(x_{1},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}}}\isaid{p}(x_{1},x_{2},\ldots,x_{\isaid{n}})\enspace.$

In the base case p has arity 0, hence this disequality simplifies to
$\isaid{p}\neq\isaid{v}$. The verifier V checks whether $\isaid{p}=\isaid{v}$,
so the proof is accepted with probability $0$.

_Inductive Step._ Suppose that $p$ has arity $\isaid{n}>0$. The induction
hypothesis states that for all
$\mathit{sc}^{\prime}=(\mathbb{F},\isaid{H},\isaid{p}^{\prime},\isaid{v}^{\prime})\notin\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$
where $\isaid{p}^{\prime}$ has arity $\isaid{n}-1$ and
$\isaid{deg}(\isaid{p}^{\prime})\leq d$,

$\displaystyle\textsf{Pr}_{\isaid{r}_{2},\ldots,\isaid{r}_{n}}[\textsf{acc}_{\mathit{sc}^{\prime}}]$
$\displaystyle\leq\frac{(\isaid{n}-1)\isaid{d}}{|\mathbb{F}|}\enspace.$

where
$\textsf{acc}_{\mathit{sc}^{\prime}}:=\langle\hat{\textbf{P}},\textbf{V}(\isaid{r}_{2},\ldots,\isaid{r}_{n})\rangle(\mathit{sc}^{\prime})=1\land\mathit{sc}^{\prime}\notin\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$.

We prove that the probability that V accepts the original instance
$\mathit{sc}\notin\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$ is at most
$\isaid{n}\isaid{d}/|\mathbb{F}|$. Recall that the message q sent by the
honest prover P is defined by
$\isaid{q}(X):=\sum_{(x_{2},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}-1}}\isaid{p}(X,x_{2}\ldots,x_{\isaid{n}})$.
Suppose that $\hat{\textbf{P}}$ sends a message $\hat{\isaid{q}}$ to the
verifier. Since either $\isaid{q}=\hat{\isaid{q}}$ or
$\isaid{q}\neq\hat{\isaid{q}}$, we have

$\displaystyle\textsf{Pr}[\textsf{acc}_{\mathit{sc}}]$
$\displaystyle=\textsf{Pr}[\textsf{acc}_{\mathit{sc}}\land\isaid{q}=\hat{\isaid{q}}]+\textsf{Pr}[\textsf{acc}_{\mathit{sc}}\land\isaid{q}\neq\hat{\isaid{q}}]\enspace.$

Note that $\textsf{acc}_{\mathit{sc}}$ implies that $\hat{\isaid{q}}$ is an
univariate polynomial of degree at most d satisfying
$\isaid{v}=\sum_{x\in\isaid{H}}\hat{\isaid{q}}(x)$.

If $\isaid{q}=\hat{\isaid{q}}$, then

v
$\displaystyle\neq\sum_{(x_{1},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}}}\isaid{p}(x_{1},x_{2},\ldots,x_{\isaid{n}})\enspace,$
$\displaystyle=\sum_{x\in\isaid{H}}\isaid{q}(x)=\sum_{x\in\isaid{H}}\hat{\isaid{q}}(x)\enspace,$

which contradicts $\textsf{acc}_{\mathit{sc}}$. Therefore,
$\textsf{Pr}[\textsf{acc}_{\mathit{sc}}\land\isaid{q}=\hat{\isaid{q}}]=0$ and

$\displaystyle\textsf{Pr}[\textsf{acc}_{\mathit{sc}}]=\textsf{Pr}[\textsf{acc}_{\mathit{sc}}\land\isaid{q}\neq\hat{\isaid{q}}]\enspace.$
(27)

Suppose that $\isaid{q}\neq\hat{\isaid{q}}$. We make a further case split, on
whether or not $\isaid{q}(\isaid{r}_{1})=\hat{\isaid{q}}(\isaid{r}_{1})$
holds:

$\displaystyle\textsf{Pr}[\textsf{acc}_{\mathit{sc}}\land\isaid{q}\neq\hat{\isaid{q}}]$
$\displaystyle=\textsf{Pr}[\textsf{acc}_{\mathit{sc}}\land\isaid{q}\neq\hat{\isaid{q}}\land\isaid{q}(\isaid{r}_{1})=\hat{\isaid{q}}(\isaid{r}_{1})]$
(28)
$\displaystyle\;+\textsf{Pr}[\textsf{acc}_{\mathit{sc}}\land\isaid{q}\neq\hat{\isaid{q}}\land\isaid{q}(\isaid{r}_{1})\neq\hat{\isaid{q}}(\isaid{r}_{1})]\enspace.$

We will now consider each of the two cases in turn. Note that
$\isaid{q}(\isaid{r}_{1})=\hat{\isaid{q}}(\isaid{r}_{1})$ for at most d values
of $\isaid{r}_{1}\in\mathbb{F}$, since $\isaid{q}-\hat{\isaid{q}}$ is a non-
zero univariate polynomial of degree at most d. Hence, we have

$\displaystyle\textsf{Pr}[\textsf{acc}_{\mathit{sc}}\land\isaid{q}\neq\hat{\isaid{q}}\land\isaid{q}(\isaid{r}_{1})=\hat{\isaid{q}}(\isaid{r}_{1})]\leq\frac{n}{|\mathbb{F}|}$
(29)

Forthe second probability in (A-B), we have

$\displaystyle\textsf{Pr}[\textsf{acc}_{\mathit{sc}}\land\isaid{q}\neq\hat{\isaid{q}}\land\isaid{q}(\isaid{r}_{1})\neq\hat{\isaid{q}}(\isaid{r}_{1})]$
$\displaystyle\leq\textsf{Pr}[\textsf{acc}_{\mathit{sc}^{\prime}}]$ (30)
$\displaystyle\leq\frac{(\isaid{n}-1)\isaid{d}}{|\mathbb{F}|}\enspace.$ (31)

To see that the inequality (30) holds, consider the reduced instance
$\mathit{sc}^{\prime}=(\mathbb{F},\isaid{H},\isaid{p}^{\prime},\isaid{v}^{\prime})$,
where $\isaid{p}^{\prime}$ is the $(\isaid{n}-1)$-variate polynomial
$\isaid{p}^{\prime}(X_{2},\ldots,X_{\isaid{n}}):=\isaid{p}(\isaid{r}_{1},X_{2},\ldots,X_{\isaid{n}})$
and $\isaid{v}^{\prime}:=\hat{\isaid{q}}(\isaid{r}_{1})$. Since
$\isaid{v}^{\prime}=\hat{\isaid{q}}(\isaid{r}_{1})\neq{\isaid{q}}(\isaid{r}_{1})$
and

$\displaystyle\isaid{q}(\isaid{r}_{1})$
$\displaystyle=\sum_{(x_{2},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}-1}}\isaid{p}(\isaid{r}_{1},x_{2},\ldots,x_{\isaid{n}})\enspace,$
$\displaystyle=\sum_{(x_{2},\ldots,x_{\isaid{n}})\in\isaid{H}^{\isaid{n}-1}}\isaid{p}^{\prime}(x_{2},\ldots,x_{\isaid{n}})\enspace,$

we have
$\mathit{sc}^{\prime}\notin\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$.
Hence, $\textsf{acc}_{\mathit{sc}}$ implies
$\textsf{acc}_{\mathit{sc}^{\prime}}$, i.e., that the verifier V accepts
$\mathit{sc}^{\prime}\notin\mathcal{L}_{\scriptscriptstyle\mathrm{SP}}$.
Finally, since $\isaid{p}^{\prime}$ has arity $\isaid{n}-1$ and degree at most
d, we can justify (31) using the induction hypothesis.

Putting (27)–(31) together, we obtain

$\textsf{Pr}[\textsf{acc}_{\mathit{sc}}]\leq\frac{\isaid{d}}{|\mathbb{F}|}+\frac{(\isaid{n}-1)\isaid{d}}{|\mathbb{F}|}=\frac{\isaid{n}\isaid{d}}{|\mathbb{F}|}\enspace.$

which completes induction step and the soundness proof. ∎

##  Appendix B Univariate Polynomials and their Connection to Multivariate
Polynomials

###  B-A Univariate Polynomials

We use the univariate polynomials from Isabelle’s polynomial theory [67],
which formalizes the algebraic properties and operations of univariate
polynomials. In this section we describe the definitions and lemmas taken from
this theory which are needed in Appendix C to prove the roots bound.

The type of univariate polynomials with coefficients of type ’a is defined by,

$\isakw{typedef }\isaid{'a
poly}=\\{\isaid{f}\isaid{::nat}\Rightarrow(\isaid{'a::zero}).\>\forall_{\infty}\>\isaid{n}.~{}\isaid{f}~{}\isaid{n}=0\\}.$

The functions in this type map natural numbers, which correspond to the
exponent of the monomials, to their coefficients in a type ’a of typeclass
zero, which is the class of types with a $0$ element. This type can only
contain functions which are eventually zero, meaning that only finitely many
coefficients can be non-zero in a polynomial. Note that this type is
isomorphic to the instance $\isaid{nat}\Rightarrow_{0}\isaid{'a}$ of the type
polynomial mappings introduced in Section VI-A. For example, informally
speaking the polynomial $1+2x+4x^{3}$ would be represented by the mapping
$\\{(0,1),(1,2),(3,4)\\}$, sending all remaining numbers to 0.

Equality of polynomials is expressed through the following lemma,

le $\displaystyle\isakw{mma }\isaid{poly\\_eq\\_iff:
}\isaid{p}=\isaid{q}\longleftrightarrow(\forall\isaid{n}.\>\mathsf{coeff}~{}\isaid{p}~{}\isaid{n}=\mathsf{coeff}~{}\isaid{q}~{}\isaid{n})$

where $\mathsf{coeff}$ is the representation morphism of the type ’a poly,
which takes a polynomial and a natural number n and returns the coefficient of
the $\isaid{n}^{\text{th}}$ power of the variable in the polynomial. The lemma
states that p and q are equal if and only if their corresponding coefficients
are equal for all powers of the variable.

##### Degree

The theory defines the degree of a polynomial by,

$\displaystyle\isakw{definition }\mathsf{degree}::\isaid{'a
poly}\Rightarrow\isaid{nat}\isakw{ where }$
$\displaystyle\quad\mathsf{degree}~{}\isaid{p}=(\mathsf{LEAST}~{}\isaid{n}.\>\forall\isaid{i}>\isaid{n}.\>\mathsf{coeff}~{}\isaid{p}~{}\isaid{i}=0)$

so that the degree of a polynomial is the least exponent after which all
coefficients are 0. We use the following two lemmas about the degree of a
polynomial,

$\displaystyle\isakw{lemma }\isaid{degree\\_mult\\_eq}:$
$\displaystyle\quad\isaid{p}\neq 0\Longrightarrow\isaid{q}\neq
0\Longrightarrow\mathsf{degree}~{}(\isaid{p}*\isaid{q})=\mathsf{degree}~{}\isaid{p}+\mathsf{degree}~{}\isaid{q},$
$\displaystyle\isakw{lemma }\isaid{degree\\_power\\_eq}:$
$\displaystyle\quad\isaid{p}\neq
0\Longrightarrow\mathsf{degree}~{}\isaid{p}^{\isaid{n}}=\isaid{n}\cdot\mathsf{degree}~{}\isaid{p}.$

##### Polynomial roots

The identifier poly is overloaded and refers both to the type of univariate
polynomials and their evaluation function; the expression
$\mathsf{poly}~{}\isaid{p}~{}\isaid{a}$ evaluates the polynomial p at the
value a. Therefore the following lemma states the finiteness of the roots of a
polynomial,

le $\displaystyle\isakw{mma }\isaid{poly\\_roots\\_finite: }\isaid{p}\neq
0\Longrightarrow\mathsf{finite}~{}\\{\isaid{a}.\>\mathsf{poly}~{}\isaid{p}~{}\isaid{a}=0\\}.$

##### Order of polynomial roots

The order of an element in a univariate polynomial is defined as follows,

$\displaystyle\isakw{definition
}\mathsf{order}::\isaid{'a}\Rightarrow\isaid{'a
poly}\Rightarrow\isaid{nat}\isakw{ where }$
$\displaystyle\quad\mathsf{order}~{}\isaid{a}~{}\isaid{p}=(\mathsf{LEAST}~{}\isaid{n}.\>\neg\>([:-\isaid{a},1:]^{\mathsf{Suc}~{}\isaid{n}}~{}\mathsf{dvd}~{}\isaid{p}))$

where $[:-\isaid{a},1:]$ represents the polynomial $(\isaid{x}-\isaid{a})$,
supposing the only variable of p is denoted by x. The order of a in p is
therefore the maximum number of times which $(\isaid{x}-{a})$ divides the
polynomial.

There are two useful lemmas regarding the order function,

$\displaystyle\isakw{lemma }\isaid{order\\_root}:$
$\displaystyle\quad\mathsf{poly}~{}\isaid{p}~{}\isaid{a}=0\>\longleftrightarrow\>\isaid{p}=0\>\lor\>\mathsf{order}~{}\isaid{a}~{}\isaid{p}\neq
0\isaid{,}$ $\displaystyle\isakw{lemma }\isaid{order\\_decomp}:$
$\displaystyle\quad\isakw{assumes }\isaid{p}\neq 0$
$\displaystyle\quad\isakw{shows
}\exists\isaid{q}.\;\isaid{p}=[:-\isaid{a},1:]^{\mathsf{order}~{}\isaid{a}~{}\isaid{p}}\cdot\isaid{q}$
$\displaystyle\phantom{\quad\isakw{shows
}\exists\isaid{q}.}\>\land\>\neg\>([:-\isaid{a},1:]~{}\mathsf{dvd}~{}\isaid{q})$

###  B-B Connecting Univariate and Multivariate Polynomials

The theory MPoly_Type_Univariate of the executable multivariate polynomials
library [51] connects the univariate polynomials described above to the
multivariate polynomials from Section VI-A. More specifically, it defines two
mutually inverse morphisms $\mathsf{poly\\_to\\_mpoly}$ and
$\mathsf{mpoly\\_to\\_poly}$, which connect polynomials of type ’a poly to
multivariate polynomials of type ’a mpoly and vice versa. These morphisms will
allow us to transfer theorems about univariate polynomials to univariate
multivariate polynomials in our proof of the roots assumption (Appendix C).

We highlight one lemma which will be needed in our final proof of the roots
bound. This lemma states that the evaluation functions poly and insertion of
univariate and multivariate polynomials, respectively, are equivalent for
univariate multivariate polynomials. It is,

$\displaystyle\isakw{lemma }\isaid{poly\\_eq\\_insertion}:$
$\displaystyle\quad\isakw{assumes
}\mathsf{vars}~{}\isaid{p}\subseteq\\{\isaid{v}\\}$
$\displaystyle\quad\isakw{shows
}\mathsf{poly}~{}(\mathsf{mpoly\\_to\\_poly}~{}\isaid{v}~{}\isaid{p})~{}\isaid{x}=\mathsf{insertion}~{}(\lambda\isaid{v}.\>\isaid{x})~{}\isaid{p}$

##  Appendix C Roots Bound for Univariate and Multivariate Polynomials

In this section, we show that the number of roots of a univariate polynomial p
of type ’a mpoly is bounded by its total degree
$\mathsf{total\\_degree}~{}\isaid{p}$. We refer to the degree of a univariate
polynomial p as $\mathsf{udegree}~{}\isaid{p}$ and the degree of a variable v
in a multivariate polynomial p as $\mathsf{degree}~{}\isaid{p}~{}\isaid{v}$.

We first establish the following roots bound for univariate polynomials of
type ’a poly:

$\displaystyle\isakw{lemma }\isaid{univariate\\_roots\\_bound}:$
$\displaystyle\quad\isakw{assumes }\isaid{p}\neq 0$
$\displaystyle\quad\isakw{shows
}\mathsf{card}~{}\\{\isaid{x}::\isaid{'a}.\;\mathsf{poly}~{}\isaid{p}~{}\isaid{x}=0\\}\leq\mathsf{udegree}~{}\isaid{p}.$

###### Proof (sketch).

We proceed by strong induction on the degree of the polynomial p, using some
lemmas from Appendix B. We find a root r of p (if there are none then the
proof is trivial) and write $\isaid{p}=(\isaid{x}-\isaid{r})\cdot\isaid{q}$
for some q using the lemma order_decomp. By lemma degree_mult_eq we derive
that the degree of p is strictly larger than that of q and therefore we can
apply the inductive hypothesis to conclude that q has strictly less roots than
the degree of p. Since $(\isaid{x}-\isaid{r})$ has exactly one root, and since
we can show that the roots of p are less than or equal to the roots of
$(\isaid{x}-\isaid{r})$ unioned to those of q, we can conclude that p has at
most $\mathsf{udegree}~{}\isaid{p}$ roots. This last step uses the lemmas
order_root and degree_power_eq. ∎

In order to transfer this result to univariate polynomials of type ’a mpoly,
we prove two lemmas relating the different degree functions
$\mathsf{udegree}$, $\mathsf{degree}$ and $\mathsf{total\\_degree}$. These are

$\displaystyle\isakw{lemma }\isaid{udegree\\_eq\\_degree}:$
$\displaystyle\quad\isakw{assumes
}\mathsf{vars}~{}\isaid{p}\subseteq\\{\isaid{v}\\}$
$\displaystyle\quad\isakw{shows
}\mathsf{udegree}~{}(\mathsf{mpoly\\_to\\_poly}~{}\isaid{v}~{}\isaid{p})=\mathsf{degree}~{}\isaid{p}~{}\isaid{v}$
$\displaystyle\isakw{lemma }\isaid{degree\\_eq\\_total\\_degree}:$
$\displaystyle\quad\isakw{assumes
}\mathsf{vars}~{}\isaid{p}\subseteq\\{\isaid{v}\\}$
$\displaystyle\quad\isakw{shows
}\mathsf{total\\_degree}~{}\isaid{p}=\mathsf{degree}~{}\isaid{p}~{}\isaid{v}$

Their proofs rely on basic properties of polynomials, definitions of the
degree functions, and properties of the $\mathsf{Max}$ and $\mathsf{LEAST}$
functions.

Finally, using the lemmas proved above and the lemma poly_eq_insertion of
Appendix B, it is straightforward to prove the following roots bound:

lemma univariate_mpoly_roots_bound: $\displaystyle\quad\isakw{assumes
}\mathsf{vars}~{}\isaid{p}\subseteq\\{\isaid{v}\\}\isakw{ and }\isaid{p}\neq
0$ $\displaystyle\quad\isakw{shows
}\mathsf{card}~{}\\{\isaid{x}.\>\mathsf{insertion}~{}(\lambda\isaid{v}.\>\isaid{x})~{}\isaid{p}=0\\}\leq\mathsf{total\\_degree}~{}\isaid{p}.$

Note that roots assumption from Figure 3 differs from the statement of this
lemma in that it refers to two polynomials instead of one. However, it is easy
to prove the roots assumption from the lemma above by applying it to the
difference of polynomials $\isaid{p}-\isaid{q}$, since
$\mathsf{eval}~{}(\isaid{p}-\isaid{q})~{}[x\mapsto r]=0$ implies that
$\mathsf{eval}~{}\isaid{p}~{}[x\mapsto
r]=\mathsf{eval}~{}\isaid{q}~{}[x\mapsto r]$.