stackproofs.tex

\documentclass[11pt]{article} % use larger type; default would be 10pt
\usepackage{hyperref}
\usepackage{fullpage}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% packages
\usepackage[
    type={CC},
    modifier={by-nc-sa},
    version={3.0},
]{doclicense}
\usepackage{authblk}
\usepackage[utf8]{inputenc} % set input encoding (not needed with xelatex)
\usepackage[strict]{changepage}
\usepackage{bold-extra}
    %%% examples of article customizations
    % these packages are optional, depending whether you want the features they provide.
    % see the latex companion or other references for full information.


    %%% page dimensions
\usepackage{geometry} % to change the page dimensions
\geometry{a4paper} % or letterpaper (us) or a5paper or....
%     \geometry{margin=2in} % for example, change the margins to 2 inches all round
    % \geometry{landscape} % set up the page for landscape
    %   read geometry.pdf for detailed page layout information
 \usepackage{numdef}

\usepackage{graphicx} % support the \includegraphics command and options
    % some of the article customisations are relevant for this class
\usepackage{amsmath,amsthm,calligra}
\usepackage{amsfonts} % math fonts such as \mathbb{}
\usepackage{amssymb} % \therefore
% \usepackage{bickham}
\usepackage{cryptocode}
\usepackage{framed}
    % \usepackage[parfill]{parskip} % activate to begin paragraphs with an empty line rather than an indent

    %%% packages
\usepackage{booktabs} % for much better looking tables
\usepackage{array} % for better arrays (eg matrices) in maths
\usepackage{paralist} % very flexible & customisable lists (eg. Enumerate/itemize, etc.)
\usepackage{verbatim} % adds environment for commenting out blocks of text & for better verbatim
\usepackage{subfig} % make it possible to include more than one captioned figure/table in a single float
    % % these packages are all incorporated in the memoir class to one degree or another...
\usepackage{mathrsfs}
\usepackage{booktabs}
\usepackage{makecell}
\usepackage{adjustbox}
% \usepackage{pzccal}
% \DeclareFontFamily{OT1}{pzc}{}
% \DeclareFontShape{OT1}{pzc}{m}{it}{<-> s * [1.10] pzcmi7t}{}
% \DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it}
\usepackage{pgfplots}

\renewcommand\theadalign{bc}
\renewcommand\theadfont{\bfseries}
\renewcommand\theadgape{\Gape[4pt]}

    %%% headers & footers
\usepackage{fancyhdr} % this should be set after setting up the page geometry
\pagestyle{fancy} % options: empty, plain, fancy
\renewcommand{\headrulewidth}{0pt} % customise the layout...
\lhead{}\chead{}\rhead{}
\lfoot{}\cfoot{\thepage}\rfoot{}


    %%% section title appearance
\usepackage{sectsty}
\allsectionsfont{\sffamily\mdseries\upshape} % (see the fntguide.pdf for font help)
    % (this matches context defaults)

    %%% toc (table of contents) appearance
\usepackage[nottoc,notlof,notlot]{tocbibind} % put the bibliography in the toc
\usepackage[titles,subfigure]{tocloft} % alter the style of the table of contents
\renewcommand{\cftsecfont}{\rmfamily\mdseries\upshape}
\renewcommand{\cftsecpagefont}{\rmfamily\mdseries\upshape} % no bold!
\usepackage[scr=esstix]  % heavily sloped
%             cal=esstix]   % slightly sloped
           {mathalpha}
 %%% end article customizations

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % macros
 \newcommand{\code}[1]{\texttt{#1}}
\newcommand\tstrut{\rule{0pt}{2.6ex}}         % = `top' strut
\newcommand\bstrut{\rule[-0.9ex]{0pt}{0pt}}   % = `bottom' strut
\newcommand{\bgamma}{\boldsymbol{\gamma}}
\newcommand{\bsigma}{\boldsymbol{\sigma}}
\newcommand{\plonk}{\ensuremath{\mathcal{P} \mathfrak{lon}\mathcal{K}}\xspace}
\newcommand{\cq}{\ensuremath{\mathpgoth{cq}}\xspace}
\newcommand{\cqlin}{\ensuremath{\mathpgoth{cq}\mathscr{\text{\calligra{lin}}}}\xspace}
\newcommand{\cqstar}{\ensuremath{\mathpgoth{cq^{\mathbf{*}}}}\xspace}
\newcommand{\protogal}{{\normalfont\scshape Proto\bfseries{galaxy}}\xspace}
\newcommand{\stackproofs}{s{\ensuremath{\mathfrak{t} \mathpgoth {ack}}\bfseries{proofs}}\xspace}
\newcommand{\protostar}{{\scshape Protostar}\xspace}
\newcommand{\hypernova}{{HyperNova}\xspace}
\newcommand{\flookup}{\ensuremath{\mathsf{\mathpgoth{Flookup}}}\xspace}
\newcommand{\baloo}{\ensuremath{\mathrm{ba}\mathit{loo}}\xspace}
\newcommand{\caulkp}{\ensuremath{\mathsf{\mathrel{Caulk}\mathrel{\scriptstyle{+}}}}\xspace}
\newcommand{\caulk}{\ensuremath{\mathsf{Caulk}}\xspace}
\newcommand{\plookup}{\ensuremath{\mathpgoth{plookup}}\xspace}
\newcommand{\tablegroup}{\ensuremath{\mathbb{H}}\xspace}
\newcommand{\V}{\ensuremath{\mathbf{V}}\xspace}
\newcommand{\relbase}{\ensuremath{\rel_0}\xspace}
\mathchardef\mhyphen="2D

\newcommand{\Patrick}[1]{\textcolor{blue}{{\bf Patrick}: #1}}

\newcommand{\instbase}{\ensuremath{\inst_0}\xspace}
\newcommand{\witbase}{\ensuremath{\wit_0}\xspace}


\newcommand{\papertitle}{\stackproofs: Private proofs of stack and contract execution using \protogal}
%\newcommand{\authorname}}
\newcommand{\company}{}
\title{ \papertitle \\[0.72cm]}
% \author{}
% \author{ Liam Eagen \\ \tt{Alpen Labs}   \and Ariel Gabizon \\ \tt{Zeta Function Technologies} }
\author[1]{Liam Eagen}
\author[2]{Ariel Gabizon}
\author[3]{Marek Sefranek}
\author[2]{Patrick Towa}
\author[2]{Zachary J. Williamson}
\affil[1]{Alpen Labs}
\affil[2]{Aztec Labs}
\affil[3]{TU Wien}
%
% \large{\authorname} \\[0.5cm] \large{\company}
% \\ {DRAFT}
%}
%\date{} % activate to display a given date or no date (if empty),

% otherwise the current date is printed
\DeclareMathAlphabet{\mathpgoth}{OT1}{pgoth}{m}{n}
\ProvidesPackage{numdef}



%% Ariel Macros:
% \num\newcommand{\G1}{\ensuremath{{\mathbb G}_1}\xspace}
\newcommand{\Gi}{\ensuremath{{\mathbb G}_i}\xspace}
\newcommand{\G}{\ensuremath{{\mathbb G}}\xspace}
\newcommand{\Gstar}{\ensuremath{{\mathbb G}^*}\xspace}
\newcommand{\x}{\ensuremath{\mathbf{x}}\xspace}
\newcommand{\z}{\ensuremath{\mathbf{z}}\xspace}
\newcommand{\X}{\ensuremath{\mathbf{X}}\xspace}

% \num\newcommand{\G2}{\ensuremath{{\mathbb G}_2}\xspace}
%\num\newcommand{\G11}{\ensuremath{\G1\setminus \set{0}}\xspace}
%\num\newcommand{\G21}{\ensuremath{\G2\setminus \set{0}}\xspace}
\newcommand{\grouppair}{\ensuremath{G^*}\xspace}
\newcommand{\prvperm}{\ensuremath{\mathrm{P_{\mathsf{\sigma}}}}\xspace}
\newcommand{\verperm}{\ensuremath{\mathrm{V_{\mathsf{\sigma}}}}\xspace}
\newcommand{\alg}{\ensuremath{\mathscr{A}}\xspace}

\newcommand{\Gt}{\ensuremath{{\mathbb G}_t}\xspace}
\newcommand{\F}{\ensuremath{\mathbb F}\xspace}
\newcommand{\Fstar}{\ensuremath{\mathbb F^*}\xspace}

\newcommand{\help}[1]{$#1$-helper\xspace}
\newcommand{\randompair}[1]{\ensuremath{\mathsf{randomPair}(#1)}\xspace}
\newcommand{\pair}[1]{$#1$-pair\xspace}
\newcommand{\pairs}[1]{$#1$-pairs\xspace}
\newcommand{\chalpoint}{\ensuremath{\mathfrak{z}}\xspace}

% \newcommand{\pairone}[1]{\G1-$#1$-pair\xspace}
% \newcommand{\pairtwo}[1]{\G2-$#1$-pair\xspace}
% \newcommand{\sameratio}[2]{\ensuremath{\mathsf{SameRatio}(#1,#2)}\xspace}
\newcommand{\vecc}[2]{\ensuremath{\left(#1\right)_{#2}}\xspace}
\newcommand{\players}{\ensuremath{[n]}\xspace}
\newcommand{\adv}{\ensuremath{\mathcal A}\xspace}
\newcommand{\advprime}{\ensuremath{\mathcal{A}'}\xspace}
\newcommand{\extprime}{\ensuremath{E'}\xspace}
\newcommand{\advrand}{\ensuremath{\mathsf{rand}_{\adv}}\xspace}
% \num\newcommand{\srs1}{\ensuremath{\mathsf{srs_1}}\xspace}
% \num\newcommand{\srs2}{\ensuremath{\mathsf{srs_2}}\xspace}
\newcommand{\srs}{\ensuremath{\mathsf{srs}}\xspace}
\newcommand{\regsrs}[1]{\ensuremath{\sett{\enc1{x^i}}{i\in \set{0,\ldots,#1-1}}}\xspace}
\newcommand{\srsm}{\ensuremath{\mathsf{srs}_M}\xspace}
\newcommand{\srsext}{\ensuremath{\mathsf{srs^*}}\xspace}
\newcommand{\srsbase}{\ensuremath{\mathsf{srs_0}}\xspace}
\newcommand{\srsi}{\ensuremath{\mathsf{srs_i}}\xspace}
\newcommand{\com}{\ensuremath{\mathsf{com}}\xspace}
\newcommand{\comperm}{\ensuremath{\mathsf{com_{\sigma}}}\xspace}
\newcommand{\cm}{\ensuremath{\mathsf{cm}}\xspace}
\newcommand{\cmsig}{\ensuremath{\mathsf{cm_\sigma}}\xspace}
\newcommand{\open}{\ensuremath{\mathsf{open}}\xspace}
\newcommand{\openperm}{\ensuremath{\mathsf{open_{\sigma}}}\xspace}
\newcommand{\sigof}[1]{\ensuremath{\sigma(#1)}\xspace}
\newcommand{\proverexp}{\ensuremath{\mathsf{e}}\xspace}
\newcommand{\reducedelems}{\ensuremath{\mathsf{r}}\xspace}

\newcommand{\ci}{\ensuremath{\mathrm{CI}}\xspace}
\renewcommand{\deg}{\ensuremath{\mathrm{deg}}\xspace}
\newcommand{\pairvec}[1]{$#1$-vector\xspace}
\newcommand{\Fq}{\ensuremath{\mathbb{F}_q}\xspace}
\newcommand{\randpair}[1]{\ensuremath{\mathsf{rp}_{#1}}\xspace}
\newcommand{\randpairone}[1]{\ensuremath{\mathsf{rp}_{#1}^{1}}\xspace}
\newcommand{\negl}{\ensuremath{\mathsf{negl}(\lambda)}\xspace}
\newcommand{\randpairtwo}[1]{\ensuremath{\mathsf{rp_{#1}^2}}\xspace}%the randpair in G2
% \newcommand{\nilp}{\ensuremath{\mathscr N}\xspace}
% \newcommand{\groupgen}{\ensuremath{\mathscr G}\xspace}
% \newcommand{\qap}{\ensuremath{\mathscr Q}\xspace}
\newcommand{\polprot}[4]{$(#1,#2,#3,#4)$-polynomial protocol}
\newcommand{\rangedprot}[5]{$#5$-ranged $(#1,#2,#3,#4)$-polynomial protocol}

\newcommand{\rej}{\ensuremath{\mathsf{reject}}\xspace}
\newcommand{\accept}{\ensuremath{\mathsf{accept}}\xspace}
\newcommand{\res}{\ensuremath{\mathsf{res}}\xspace}
% \newcommand{\sha}[1]{\ensuremath{\mathsf{COMMIT}(#1)}\xspace}
%  \newcommand{\shaa}{\ensuremath{\mathsf{COMMIT}}\xspace}
 \newcommand{\comm}[1]{\ensuremath{\enc1{#1(x)}}\xspace}
 \newcommand{\defeq}{:=}

\newcommand{\B}{\ensuremath{\set{0,1}}\xspace}
\newcommand{\dom}{\ensuremath{H}\xspace}
\newcommand{\C}{\ensuremath{\vec{C}}\xspace}
\newcommand{\Btwo}{\ensuremath{\vec{B_2}}\xspace}
\newcommand{\treevecsimp}{\ensuremath{(\tau,\rho_A,\rho_A \rho_B,\rho_A\alpha_A,\rho_A\rho_B\alpha_B, \rho_A\rho_B\alpha_C,\beta,\beta\gamma)}\xspace}% The sets of elements used in simplifed relation tree in main text body
\newcommand{\rcptc}{random-coefficient subprotocol\xspace}
\newcommand{\rcptcparams}[2]{\ensuremath{\mathrm{RCPC}(#1,#2)}\xspace}
\newcommand{\verifyrcptcparams}[2]{\ensuremath{\mathrm{\mathsf{verify}RCPC}(#1,#2)}\xspace}
\newcommand{\randadv}{\ensuremath{\mathsf{rand}_{\adv}}\xspace}
 \num\newcommand{\ex1}[1]{\ensuremath{#1\cdot g_1}\xspace}
 \num\newcommand{\ex2}[1]{\ensuremath{#1\cdot g_2}\xspace}
 \newcommand{\pr}{\mathrm{Pr}}
%  \newcommand{\powervec}[2]{\ensuremath{(1,#1,#1^{2},\ldots,#1^{#2})}\xspace}
%  \newcommand{\partition}{\ensuremath{\mathcal{T}}\xspace}
%  \newcommand{\partof}[1]{\ensuremath{{\partition_{#1}}}\xspace}
% \num\newcommand{\out1}[1]{\ensuremath{\ex1{\powervec{#1}{d}}}\xspace}
% \num\newcommand{\out2}[1]{\ensuremath{\ex2{\powervec{#1}{d}}}\xspace}
%  \newcommand{\nizk}[2]{\ensuremath{\mathrm{NIZK}(#1,#2)}\xspace}% #2 is the hash concatenation input
%  \newcommand{\verifynizk}[3]{\ensuremath{\mathrm{VERIFY\mhyphen NIZK}(#1,#2,#3)}\xspace}
\newcommand{\protver}{protocol verifier\xspace}
\newcommand{\hash}{\ensuremath{\mathcal{H}}\xspace}
\newcommand{\mulgroup}{\ensuremath{\F^*}\xspace}
\newcommand{\lag}[1]{\ensuremath{L_{#1}}\xspace}
\newcommand{\sett}[2]{\ensuremath{\set{#1}_{#2}}\xspace}
\newcommand{\omegaprod}{\ensuremath{\alpha_{\omega}}\xspace}
\newcommand{\lagvec}[1]{\ensuremath{\mathrm{LAG}_{#1}}\xspace}
\newcommand{\trapdoor}{\ensuremath{r}}
\newcommand{\trapdoorext}{\ensuremath{r_{\mathrm{ext}}}\xspace}
% \newcommand{\trapdoorsim}{\ensuremath{r_{\mathrm{sim}}}\xspace}
\renewcommand{\sim}{\ensuremath{\mathrm{S}}\xspace}
\renewcommand{\mod}{\ensuremath{\;\mathrm{mod}\;}}
\newcommand{\hsub}{\ensuremath{H^*}\xspace}
\num\newcommand{\enc1}[1]{\ensuremath{\left[#1\right]_1}\xspace}
\newcommand{\enci}[1]{\ensuremath{\left[#1\right]_i}\xspace}
\num\newcommand{\enc2}[1]{\ensuremath{\left[#1\right]_2}\xspace}
\newcommand{\gen}{\ensuremath{\mathsf{gen}}\xspace}
\newcommand{\hgen}{\ensuremath{\omega}\xspace}
\newcommand{\gops}{\G1-operations\xspace}
\newcommand{\nlogngops}{$O(n\log n)$ \G1-operations\xspace}
\newcommand{\nlognfops}{$O(n\log n)$ \F-operations\xspace}
\newcommand{\fops}{\F-operations\xspace}
\newcommand{\prv}{\ensuremath{\mathsf{\mathbf{P}}}\xspace}
\newcommand{\prvpoly}{\ensuremath{\mathrm{P_{\mathsf{poly}}}}\xspace}
\newcommand{\prvpc}{\ensuremath{\mathrm{P_{\mathsf{PC}}}}\xspace}
\newcommand{\verpoly}{\ensuremath{\mathrm{V_{\mathsf{poly}}}}\xspace}
\newcommand{\verpc}{\ensuremath{\mathrm{V_{\mathsf{PC}}}}\xspace}
\newcommand{\ideal}{\ensuremath{\mathcal{I}}\xspace}
\newcommand{\prf}{\ensuremath{\mathsf{\pi}}\xspace}
\newcommand{\prfone}{\ensuremath{\mathsf{\pi_1}}\xspace}
% \newcommand{\simprv}{\ensuremath{\mathrm{P^{sim}}}\xspace}

%\newcommand{\enc}[1]{\ensuremath{\left[#1\right]}\xspace}
%\num\newcommand{\G0}{\ensuremath{\mathbf{G}}\xspace}
\newcommand{\GG}{\ensuremath{\mathbf{G^*}}\xspace}  % would have liked to call this G01 but problem with name
\num\newcommand{\g0}{\ensuremath{\mathbf{g}}\xspace}
\newcommand{\inst}{\ensuremath{\phi}\xspace}
\newcommand{\newinst}{\ensuremath{\phi^*}\xspace}
\newcommand{\row}{\ensuremath{\mathsf{R}}\xspace}
\newcommand{\col}{\ensuremath{\mathsf{C}}\xspace}
\newcommand{\inp}{\ensuremath{\mathsf{x}}\xspace}
\newcommand{\wit}{\ensuremath{\mathsf{\omega}}\xspace}
\newcommand{\eps}{\ensuremath{\varepsilon}\xspace}
\newcommand{\inpF}{\ensuremath{\mathscr{x}}\xspace}
\newcommand{\witF}{\ensuremath{\mathscr{w}}\xspace}
\newcommand{\instFprime}{\ensuremath{\inst}\xspace}%\mathpgoth{x}}\xspace}
\newcommand{\witFprime}{\ensuremath{\witinst}\xspace}%\mathpgoth{w}}\xspace}
\newcommand{\acchash}{\ensuremath{\mathscr{h}}\xspace}
\newcommand{\accnew}{\ensuremath{\mathscr{acc}}\xspace}
\newcommand{\cnt}{\ensuremath{\mathsf{count}}\xspace}
\newcommand{\ver}{\ensuremath{\mathsf{\mathbf{V}}}\xspace}
\newcommand{\verpg}{\ensuremath{\ver^{\predinst,\cm}_{PG}}\xspace}
\newcommand{\per}{\ensuremath{\mathsf{\mathbf{P}}}\xspace}
\newcommand{\perpg}{\ensuremath{\per_{PG}}\xspace}
\newcommand{\sonic}{\ensuremath{\mathsf{Sonic}}\xspace}
\newcommand{\aurora}{\ensuremath{\mathsf{Aurora}}\xspace}
\newcommand{\auroralight}{\ensuremath{\mathsf{Auroralight}}\xspace}
\newcommand{\groth}{\ensuremath{\mathsf{Groth'16}}\xspace}
\newcommand{\kate}{\ensuremath{\mathsf{KZG}}\xspace}
\newcommand{\rel}{\ensuremath{\mathcal{R}}\xspace}
\newcommand{\relrand}{\ensuremath{\mathcal{R^{\mathsf{rand}}}}\xspace}
\newcommand{\lang}{\ensuremath{\mathcal{L}}\xspace}
\newcommand{\params}{\ensuremath{\mathsf{params}_{\inst}}\xspace}
\newcommand{\protparams}{\ensuremath{\mathsf{params}_{\inst}^\advv}\xspace}
\num\newcommand{\p1}{\ensuremath{P_1}\xspace}
\newcommand{\advv}{\ensuremath{\mathcal{A}^{\mathbf{*}}}\xspace} % the adversary that uses protocol adversary as black box
\newcommand{\crs}{\ensuremath{\sigma}\xspace}
%\num\newcommand{\crs1}{\ensuremath{\mathrm{\sigma}_1}\xspace}
%\num\newcommand{\crs2}{\ensuremath{\mathrm{\sigma}_2}\xspace}
\newcommand{\set}[1]{\ensuremath{\left\{#1\right\}}\xspace}
% \newcommand{\hgen}{\ensuremath{\mathbf{\omega}}\xspace}
\newcommand{\vgen}{\ensuremath{\mathbf{g}}\xspace}
% \renewcommand{\sim}{\ensuremath{\mathsf{sim}}\xspace}%the distribution of messages when \advv simulates message of \p1
\newcommand{\real}{\ensuremath{\mathsf{real}}\xspace}%the distribution of messages when \p1 is honest and \adv controls rest of players
 \newcommand{\koevec}[2]{\ensuremath{(1,#1,\ldots,#1^{#2},\alpha,\alpha #1,\ldots,\alpha #1^{#2})}\xspace}
\newcommand{\mida}{\ensuremath{A_{\mathrm{mid}}}\xspace}
\newcommand{\midb}{\ensuremath{B_{\mathrm{mid}}}\xspace}
\newcommand{\midc}{\ensuremath{C_{\mathrm{mid}}}\xspace}
\newcommand{\chal}{\ensuremath{\mathsf{challenge}}\xspace}
\newcommand{\attackparams}{\ensuremath{\mathsf{params^{pin}}}\xspace}
\newcommand{\pk}{\ensuremath{\mathsf{pk}}\xspace}
\newcommand{\attackdist}[2]{\ensuremath{AD_{#1}}\xspace}
% \renewcommand{\neg}{\ensuremath{\mathsf{negl}(\lambda)}\xspace}
\newcommand{\ro}{\ensuremath{{\mathscr R}}\xspace}
\newcommand{\elements}[1]{\ensuremath{\mathsf{elements}_{#1}}\xspace}
 \num\newcommand{\elmpowers1}[1]{\ensuremath{\mathrm{\mathsf{e}}^1_{#1}}\xspace}
 \num\newcommand{\elmpowers2}[1]{\ensuremath{\mathrm{\mathsf{e}}^2_{#1}}\xspace}
\newcommand{\elempowrs}[1]{\ensuremath{\mathsf{e}_{#1}}\xspace}
 \newcommand{\secrets}{\ensuremath{\mathsf{secrets}}\xspace}
 \newcommand{\polysofdeg}[1]{\ensuremath{\F_{< #1}[X]}\xspace}
 \newcommand{\polysofdegeq}[1]{\ensuremath{\F_{\leq #1}[X]}\xspace}
 \newcommand{\pols}{\ensuremath{\F[X]}\xspace}
 \newcommand{\bivar}[1]{\ensuremath{\F_{< #1}[X,Y]}\xspace}
 \newcommand{\sig}{\ensuremath{\mathscr{S}}\xspace}
 \newcommand{\prot}{\ensuremath{\mathscr{P}}\xspace}
 \newcommand{\protstar}{\ensuremath{\mathscr{P}^*}\xspace}
 \newcommand{\PCscheme}{\ensuremath{\mathscr{S}}\xspace}
 \newcommand{\protprime}{\ensuremath{\mathscr{P^*}}\xspace}
 \newcommand{\sigprv}{\ensuremath{\mathsf{P_{sc}}}\xspace}
 \newcommand{\sigver}{\ensuremath{\mathsf{V_{sc}}}\xspace}
 \newcommand{\sigpoly}{\ensuremath{\mathsf{S_{\sigma}}}\xspace}
 \newcommand{\idpoly}{\ensuremath{\mathsf{S_{ID}}}\xspace}
\newcommand{\idpolyevala}{\ensuremath{\mathsf{\bar{s}_{ID1}}}\xspace}
\newcommand{\sigpolyevala}{\ensuremath{\mathsf{\bar{s}_{\sigma1}}}\xspace}
\newcommand{\sigpolyevalb}{\ensuremath{\mathsf{\bar{s}_{\sigma2}}}\xspace}
\newcommand{\bctv}{\ensuremath{\mathsf{BCTV}}\xspace}
\newcommand{\PI}{\ensuremath{\mathsf{PI}}\xspace}
\newcommand{\PIb}{\ensuremath{\mathsf{PI_B}}\xspace}
\newcommand{\PIc}{\ensuremath{\mathsf{PI_C}}\xspace}
\newcommand{\dl}[1]{\ensuremath{\widehat{#1}}\xspace}
\newcommand{\obgen}{\ensuremath{\mathcal O}\xspace}
\newcommand{\PC}{\ensuremath{\mathscr{P}}\xspace}
\newcommand{\permscheme}{\ensuremath{\sigma_\mathscr{P}}\xspace}


\newcommand{\selleft}{\ensuremath{\mathbf{q_L}}\xspace}
\newcommand{\selright}{\ensuremath{\mathbf{q_R}}\xspace}
\newcommand{\selout}{\ensuremath{\mathbf{q_O}}\xspace}
\newcommand{\selmult}{\ensuremath{\mathbf{q_M}}\xspace}
\newcommand{\selconst}{\ensuremath{\mathbf{q_C}}\xspace}
\newcommand{\selectors}{\ensuremath{\mathcal{Q}}\xspace}
\newcommand{\lvar}{\ensuremath{\mathbf{a}}\xspace}
\newcommand{\vars}{\ensuremath{\mathcal{V}}\xspace}
\newcommand{\rvar}{\ensuremath{\mathbf{b}}\xspace}
\newcommand{\ovar}{\ensuremath{\mathbf{c}}\xspace}
\newcommand{\pubvars}{\ensuremath{\mathcal{I}}\xspace}
\newcommand{\assignment}{\ensuremath{\mathbf{x}}\xspace}
\newcommand{\constsystem}{\ensuremath{\mathscr{C}}\xspace}
\newcommand{\relof}[1]{\ensuremath{\rel_{#1}}\xspace}
\newcommand{\pubinppoly}{\ensuremath{\mathsf{PI}}\xspace}
\newcommand{\sumi}[1]{\sum_{i\in[#1]}}
\newcommand{\sumzertok}[1]{\sum_{#1=0}^{k}}
\newcommand{\sumpoly}[1]{\sum_{i=0}^{#1-1}}
\newcommand{\summ}[1]{\sum_{i\in[#1]}}
\newcommand{\sumj}[1]{\sum_{j\in[#1]}}
\newcommand{\innerprod}[2]{\langle#1,#2\rangle}
\newcommand{\ZeroH}{\ensuremath{Z_H} \xspace}
\newcommand{\lpoly}{\ensuremath{\mathsf{a}}\xspace}
\newcommand{\rpoly}{\ensuremath{\mathsf{b}}\xspace}
\newcommand{\opoly}{\ensuremath{\mathsf{c}}\xspace}
\newcommand{\idpermpoly}{\ensuremath{\mathsf{z}}\xspace}
\newcommand{\lagrangepoly}{\ensuremath{\mathsf{L}}\xspace}
\newcommand{\zeropoly}{\ensuremath{\mathsf{\ZeroH}}\xspace}
\newcommand{\selmultpoly}{\ensuremath{\mathsf{q_M}}\xspace}
\newcommand{\selleftpoly}{\ensuremath{\mathsf{q_L}}\xspace}
\newcommand{\selrightpoly}{\ensuremath{\mathsf{q_R}}\xspace}
\newcommand{\seloutpoly}{\ensuremath{\mathsf{q_O}}\xspace}
\newcommand{\selconstpoly}{\ensuremath{\mathsf{q_C}}\xspace}
\newcommand{\idcomm}{\ensuremath{[s_{\mathsf{ID1}}]_1}\xspace}
\newcommand{\sigcomma}{\ensuremath{[s_{\mathsf{\sigma1}}]_1}\xspace}
\newcommand{\sigcommb}{\ensuremath{[s_{\mathsf{\sigma2}}]_1}\xspace}
\newcommand{\sigcommc}{\ensuremath{[s_{\mathsf{\sigma3}}]_1}\xspace}
\newcommand{\selleftcomm}{\ensuremath{[q_\mathsf{L}]_1}\xspace}
\newcommand{\selrightcomm}{\ensuremath{[q_\mathsf{R}]_1}\xspace}
\newcommand{\seloutcomm}{\ensuremath{[q_\mathsf{O}]_1}\xspace}
\newcommand{\selconstcomm}{\ensuremath{[q_\mathsf{C}]_1}\xspace}
\newcommand{\selmultcomm}{\ensuremath{[q_\mathsf{M}]_1}\xspace}

\newcommand{\multlinecomment}[1]{\directlua{-- #1}}


\newtheorem{lemma}{Lemma}[section]
\newtheorem{thm}[lemma]{Theorem}
\newtheorem{dfn}[lemma]{Definition}
\newtheorem{remark}[lemma]{Remark}

\newtheorem{claim}[lemma]{Claim}
\newtheorem{corollary}[lemma]{Corollary}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\R}{\mathcal{R}}
\newcommand{\crct}{\ensuremath{\mathsf{C}}\xspace}
\newcommand{\A}{\ensuremath{\mathcal{A}}\xspace}
%\newcommand{\G}{\mathcal{G}}
\newcommand{\Gr}{\mathbb{G}}
%\newcommand{\com}{\textsf{com}}  Ariel defined equivalent that also works in math mode
\newcommand{\cgen}{\text{cgen}}
\newcommand{\poly}{\ensuremath{\mathsf{poly(\lambda)}}\xspace}
\newcommand{\snark}{\ensuremath{\mathsf{snark}}\xspace}
\newcommand{\grandprod}{\mathsf{prod}}
\newcommand{\perm}{\mathsf{S}}
%\newcommand{\open}{\mathsf{open}}
\newcommand{\update}{\mathsf{update}}
\newcommand{\Prove}{\mathcal{P}}
\newcommand{\Verify}{\mathcal{V}}
\newcommand{\Extract}{\mathcal{E}}
\newcommand{\Simulate}{\mathcal{S}}
\newcommand{\Unique}{\mathcal{U}}
\newcommand{\Rpoly}{\R{\poly}}
\newcommand{\Ppoly}{\Prove{\poly}}
\newcommand{\Vpoly}{\Verify{\poly}}
\newcommand{\Psnark}{\prv}%{\Prove{\snark}}
\newcommand{\Vsnark}{\ver}%{\Verify{\snark}}
\newcommand{\Rprod}{\R{\grandprod}}
\newcommand{\Pprod}{\Prove{\grandprod}}
\newcommand{\Vprod}{\Verify{\grandprod}}
\newcommand{\Rperm}{\R{\perm}}
\newcommand{\Pperm}{\Prove{\perm}}
\newcommand{\Vperm}{\Verify{\perm}}
% \newcommand{\zw}[1]{{\textcolor{magenta}{Zac:#1}}}
\newcommand{\ag}[1]{{\textcolor{blue}{\emph{Ariel:#1}}}}
\newcommand{\extprot}{\ensuremath{E_{\prot}}\xspace}
\newcommand{\transcript}{\ensuremath{\mathsf{transcript}}\xspace}
\newcommand{\extpc}{\ensuremath{E_{\PCscheme}}\xspace}
\newcommand{\advpc}{\ensuremath{\mathcal A_{\PCscheme}}\xspace}
\newcommand{\advprot}{\ensuremath{\mathcal A_{\prot}}\xspace}
\newcommand{\protmany}{\ensuremath{\prot_k}\xspace}

\usepackage{pifont}% http://ctan.org/pkg/pifont
\newcommand{\cmark}{\ding{51}}%
\newcommand{\xmark}{\ding{55}}%
\newcommand{\marlin}{\ensuremath{\mathsf{Marlin}}\xspace}
\newcommand{\fractal}{\ensuremath{\mathsf{Fractal}}\xspace}
% \newcommand{\Rsnark}{\R{\snark}}
\newcommand{\Rsnark}{\R}
\newcommand{\subvec}[1]{\ensuremath{#1|_{\subspace}}\xspace}
\newcommand{\restricttovec}[1]{\ensuremath{#1|_{\subgroup}}\xspace}
\newcommand{\isinvanishing}[1]{\ensuremath{\mathsf{IsInVanishing_{\subspace,#1}}}\xspace}
\newcommand{\batchedisinvanishing}[1]{\ensuremath{\mathsf{BatchedIsInVanishing_{\subspace,#1}}}\xspace}
\newcommand{\isconsistent}{\ensuremath{\mathsf{IsConsistent}}\xspace}
\newcommand{\isintable}{\ensuremath{\mathsf{IsInTable}}\xspace}
\newcommand{\lincheck}{\ensuremath{\mathsf {lincheck}}\xspace}
\newcommand{\accprot}{\ensuremath{\mathsf {accProt}}\xspace}
\newcommand{\isinvanishingtable}[1]{\ensuremath{\mathsf{IsInVanishingTable_{\subspace,#1}}}\xspace}
\newcommand{\isvanishingsubtable}[1]{\ensuremath{\mathsf{IsVanishingSubtable_{#1}}}\xspace}
\newcommand{\haslowerdegree}{\ensuremath{\mathsf{HasLowerDegree}}\xspace}
\newcommand{\haslowdegree}[1]{\ensuremath{\mathsf{HasLowDegree_{#1}}}\xspace}
\newcommand{\issubtable}[1]{\ensuremath{\mathsf{IsSubtable_{#1}}}\xspace}
\newcommand{\isinsubtable}[2]{\ensuremath{\mathsf{IsInSubtable_{#1,#2}}}\xspace}
\newcommand{\secbasezero}[1]{\ensuremath{\hat{\tau}_{#1}}\xspace}
\newcommand{\secbase}[1]{\ensuremath{\hat{\tau}_{#1}}\xspace}
\newcommand{\secbasereg}[1]{\ensuremath{\tau_{#1}}\xspace}
\newcommand{\secset}{\ensuremath{I}\xspace}
\newcommand{\pubbase}[1]{\ensuremath{\mu_{#1}}\xspace}
\newcommand{\subspace}{\ensuremath{\mathbb{H}}\xspace}
\newcommand{\subgroup}{\ensuremath{\mathbb{H}}\xspace}
\newcommand{\biggroup}{\ensuremath{\mathbb{V}}\xspace}
\newcommand{\subtable}{\ensuremath{T_0}\xspace}
\newcommand{\tablelang}{\ensuremath{\lang_T}\xspace}
\newcommand{\vanishingtablelang}{\ensuremath{\lang_{\subspace}}\xspace}
\newcommand{\nonorm}[1]{\ensuremath{\Gamma^T_{#1}}\xspace}
\newcommand{\unnorm}[2]{\ensuremath{\Gamma^{#1}_{#2}}\xspace}
\newcommand{\bigspacebase}{\ensuremath{\lambda}\xspace}
\newcommand{\bigspacegen}{\ensuremath{\mathsf{h}}\xspace}
\newcommand{\modvan}[1]{\ensuremath{\mathrm{mod\;}Z_{#1}}\xspace}
\newcommand{\extractevaltable}{\ensuremath{\mathsf{ExtractEvalTable}_{C,\tablegroup}}\xspace}
\newcommand{\witsize}{\ensuremath{n}\xspace}
\newcommand{\witruntime}{\ensuremath{\witsize\log\witsize}\xspace}
\newcommand{\tabsize}{\ensuremath{N}\xspace}
\newcommand{\tabruntime}{\ensuremath{\tabsize\log\tabsize}\xspace}
\newcommand{\tab}{\ensuremath{\mathfrak{t}}\xspace}
 \renewcommand{\a}{\ensuremath{\mathsf{a}}\xspace}
\renewcommand{\b}{\ensuremath{\mathsf{b}_0}\xspace}
\renewcommand{\c}{\ensuremath{\mathsf{c}}\xspace}
\newcommand{\vc}{\ensuremath{\mathsf{c_v}}\xspace}
\renewcommand{\v}{\ensuremath{\mathsf{v}}\xspace}
\renewcommand{\r}{\ensuremath{\mathsf{r}}\xspace}
\newcommand{\f}{\ensuremath{\mathsf{f}}\xspace}
\renewcommand{\g}{\ensuremath{\mathsf{g}}\xspace}
\newcommand{\matrices}{\ensuremath{\F^{n\times n}}\xspace}
\newcommand{\ftwo}{\ensuremath{\mathsf{f}_2}\xspace}
\renewcommand{\p}{\ensuremath{\mathsf{p}}\xspace}
\newcommand{\q}{\ensuremath{\mathsf{q}}\xspace}
\newcommand{\qone}{\ensuremath{\mathsf{q_1}}\xspace}
\newcommand{\s}{\ensuremath{\mathsf{s}}\xspace}
\newcommand{\qa}{\ensuremath{\mathsf{q_a}}\xspace}
\newcommand{\qb}{\ensuremath{\mathsf{q_b}}\xspace}
\newcommand{\m}{\ensuremath{\mathsf{m}}\xspace}
\newcommand{\agam}{\ensuremath{a_\gamma}\xspace}
\newcommand{\gamproof}{\ensuremath{\mathsf{\pi_\gamma}}\xspace}
\newcommand{\zerproof}{\ensuremath{\mathsf{\a}_0}\xspace}
\newcommand{\bgam}{\ensuremath{b_\gamma}\xspace}
\newcommand{\bzergam}{\ensuremath{b_{0,\gamma}}\xspace}
\newcommand{\qbgam}{\ensuremath{Q_{b,\gamma}}\xspace}
\newcommand{\zgam}{\ensuremath{Z_{\bigspace,\gamma}}\xspace}
\newcommand{\betaa}{\ensuremath{\mathbf{\boldsymbol{\beta}}}\xspace}
\newcommand{\deltaa}{\ensuremath{\mathbf{\boldsymbol{\delta}}}\xspace}
\newcommand{\gammaa}{\ensuremath{\mathbf{\boldsymbol{\gamma}}}\xspace}
\newcommand{\witcom}{\ensuremath{\mathsf{W}}\xspace}
\newcommand{\instt}{\ensuremath{\Phi^*}\xspace}
\newcommand{\insttbase}{\ensuremath{\Phi}\xspace}
\newcommand{\pow}{\ensuremath{\mathsf{pow}}\xspace}
\newcommand{\eq}{\ensuremath{\mathsf{eq}}\xspace}
\newcommand{\FFT}{\ensuremath{\mathsf{FFT}}\xspace}
\newcommand{\fgam}{\ensuremath{f_{\gamma}}\xspace}
\newcommand{\pgam}{\ensuremath{P_{\gamma}}\xspace}
\newcommand{\supp}[1]{\ensuremath{\mathrm{supp}(#1)}\xspace}
\newcommand{\degoffset}{\ensuremath{\tabsize-1-(\witsize-2)}\xspace}
\newcommand{\modpoly}[1]{\ensuremath{\;\;\mod #1(X)}\xspace}
\newcommand{\coeff}[2]{\ensuremath{(#1)_{[#2]}}\xspace}
\newcommand{\kzg}[1]{\ensuremath{\mathsf{KZG}_{#1,\subgroup}}\xspace}
\newcommand{\accscheme}[2]{$(#1\mapsto #2)$-folding scheme\xspace}
\newcommand{\accrel}{\ensuremath{\rel_{\mathpgoth{acc}}}\xspace}
\newcommand{\relpair}{\ensuremath{\mathfrak{p}}\xspace}
\newcommand{\inststar}{\ensuremath{\inst^*}\xspace}
\newcommand{\witstar}{\ensuremath{\wit^*}\xspace}
\newcommand{\relpairstar}{\ensuremath{\relpair^*}\xspace}
\newcommand{\witt}{\ensuremath{\mathrm{w}}\xspace}
\newcommand{\nodelabel}{\ensuremath{\mathfrak{n}}\xspace}
\newcommand{\roundnum}{\ensuremath{\mathpgoth{k}}\xspace}
\newcommand{\manyvar}{\ensuremath{\mathfrak{J}}\xspace}
\newcommand{\nmin}{\ensuremath{[n]_0}\xspace}
\newcommand{\zfin}{\ensuremath{z_{\mathscr{final}}}\xspace}
\newcommand{\relapp}{\ensuremath{\rel_{app}}\xspace}
\newcommand{\relexec}{\ensuremath{\rel_{\mathrm{exec}}}\xspace}
\newcommand{\relF}{\ensuremath{\rel_F}\xspace}
\newcommand{\init}{\ensuremath{\mathsf{init}}\xspace}
\newcommand{\add}{\ensuremath{\mathsf{add}}\xspace}
\newcommand{\del}{\ensuremath{\mathsf{del}}\xspace}
\renewcommand{\read}{\ensuremath{\mathsf{read}}\xspace}
\newcommand{\countrange}{\ensuremath{[M]}\xspace}
\newcommand{\true}{\ensuremath{\mathsf{true}}\xspace}
\newcommand{\false}{\ensuremath{\mathsf{false}}\xspace}
\newcommand{\finstate}{\ensuremath{V}\xspace}
\newcommand{\ops}{\ensuremath{\mathcal{O}}\xspace}
\newcommand{\op}{\ensuremath{\mathscr{op}}\xspace}
\newcommand{\instapp}{\ensuremath{\mathfrak{x}}\xspace}
\newcommand{\witapp}{\ensuremath{\mathfrak{w}}\xspace}
\newcommand{\instnoops}{\ensuremath{\mathbf{x}}\xspace}
 \renewcommand{\path}{\ensuremath{\mathbf{p}}\xspace}
\renewcommand{\root}{\ensuremath{\mathbf{r}}\xspace}
\newcommand{\predinst}{\ensuremath{\mathpgoth{f}}\xspace}
\renewcommand{\empty}{\ensuremath{g_{\mathscr{empty}}}\xspace}
\newcommand{\funcs}{\ensuremath{\mathsf{F}}\xspace}
\newcommand{\ztafuncs}{\ensuremath{\mathcal{D}}\xspace}
% \newcommand{\instF}{\ensuremath{\mathrm{x}}\xspace}
% \newcommand{\witF}{\ensuremath{\mathrm{w}}\xspace}
\newcommand{\instexec}{\ensuremath{\mathrm{x_{exec}}}\xspace}
\newcommand{\witexec}{\ensuremath{\mathrm{w_{exec}}}\xspace}
\newcommand{\witf}{\ensuremath{\mathsf{w_f}}\xspace}
\newcommand{\sel}{\ensuremath{\mathsf{q}}\xspace}
% \newcommand{\perm}{\ensuremath{\mathsf{s}}\xspace}
\newcommand{\args}{\ensuremath{\mathsf{args}}\xspace}
\newcommand{\callnum}{\ensuremath{\mathsf{c}}\xspace}
\newcommand{\recset}{\ensuremath{\mathsf{V}}\xspace}
\newcommand{\tree}{\ensuremath{\mathsf{T}}\xspace}
\newcommand{\node}{\ensuremath{\mathsf{n}}\xspace}
\newcommand{\incsum}{\ensuremath{\mathscr{s}}\xspace}
\newcommand{\inchash}{\ensuremath{\mathscr{h}}\xspace}
\newcommand{\shlomomath}[1]{\ensuremath{\text{\usefont{U}{BOONDOX-cal}{m}{n}#1}}\xspace}
\newcommand{\calligmath}[1]{\ensuremath{\text{\calligra{#1}}}\xspace}
\newcommand{\ext}{\ensuremath{\mathbf{E}}\xspace}
\newcommand{\finpred}{\shlomomath{f}}
\newcommand{\zksnark}{zk-SNARK\;}
\newcommand{\n}{\shlomomath{n}}
\newcommand{\dimK}{\calligmath{k}}
\newcommand{\M}{\calligmath{M}}
\newcommand{\cmsetup}{\ensuremath{r_\cm}\xspace}
\newcommand{\relrcg}{\ensuremath{\rel_{F,\finpred}}\xspace}
\newcommand{\relzer}{\ensuremath{\rel_{0}}\xspace}
\newcommand{\relrcgstar}{\ensuremath{\rel_{F^*,\finpred^*}}\xspace}
\begin{document}
    \maketitle
\begin{abstract}
The goal of this note is to describe and analyze a simplified variant of the zk-SNARK construction used in the Aztec protocol.
Taking inspiration from the popular notion of Incrementally Verifiable Computation\cite{ivc} (IVC)
we define a related notion of \emph{Repeated Computation with Global state} (RCG). As opposed to IVC, in RCG we assume the computation terminates before proving starts, and in addition to the local transitions some global consistency checks of the whole computation are allowed. However, we require the space efficiency of the prover to be close to that of an IVC prover not required to prove this global consistency.
We show how RCG is useful for designing a proof system for a private smart contract system like Aztec.
\end{abstract}
\section{Introduction}
Incrementally Verifiable Computation (IVC) \cite{ivc} and its generalization to Proof Carrying Data (PCD) \cite{pcd} are useful tools for constructing space-efficient SNARK provers\cite{BCCT}.
In IVC and PCD we always have an acyclic computation.
However code written in almost any programming language \emph{is} cyclic in the sense of often relying on internal calls --
we start from a function $A$, execute some commands, go into a function $B$, execute its commands, and go back to $A$.
When making a SNARK proof of such an execution, we typically linearize or ``flatten'' the cycle stemming from the internal call, in one of the following two ways.
\begin{enumerate}
 \item The monolithic circuit approach: We ``inline'' all internal calls (as well as loops) into one long program without jumps.
 \item The VM approach: Assume the code of $A,B$ is written in some prespecified instruction set. The program is executed by initially writing the code of $A,B$ into memory, and loading from memory and executing at each step the appropriate instruction according to a program counter. For example, the call to $B$ is made by changing the counter to that of the first instruction of $B$. To prove correctness of the execution, all we need is a SNARK for proving correctness of a certain number of steps of a machine with this instruction set, and some initial memory state.
\end{enumerate}

The second approach is more generic, while the first offers more room for optimization, so we'd want to use it in resource-constrained settings, e.g. client-side proving.


However, what if we're in a situation where $A$ and $B$ have already been ``SNARKified'' separately?
Namely, there is a verification key attached to each one, and we are expected to use these keys specifically.
This is what happens in the Aztec system.
\paragraph{The Aztec private contract system}
Similar to Ethereum we have contracts, and the contracts have functions.\footnote{Detailed documentation of the Aztec protocol can be found \href{https://docs.aztec.network/}{here}.}
A function in a contract can internally call a different function in the same or a different contract. Moreover, while writing the code for the different functions and compiling them to circuits,
we can't predict what function will be internally called by a given contract function. For example, a ``send token'' function could have an internal call to an ``authorize'' function.
But the call to ``authorize'' need not be tied to a specific implementation and consequently, to a specific verification key -- as different token holders are 
allowed to set their own ``authorize'' function.


The goal of the Aztec system is to enable constructing zero-knowledge proofs of such contract function executions.
For this purpose, a contract is deployed by
\begin{enumerate}
\item Computing a verification key for each function of the contract.
\item Adding a commitment to the verification keys of the contract in a global ``function tree''. More accurately, a leaf of this tree is a hash of the
contract address with a Merkle root of a tree whose leaves are the verification keys of that contract's functions.
\end{enumerate}

\paragraph{Dealing with global state}
The global state of the Aztec system is described by a set of notes, which are simply values in a field \F.
% \Patrick{What does it mean for a contract to "have" a set of notes? Perhaps mention instead that there is a global state consisting of notes that can
% 	be modified by any contract}
Each note belongs to a certain contract. While running, a function can read, add or delete notes belonging to its contract.
% \Patrick{Same remark for "belonging"}
We can thus think of the notes as global variables shared between the different functions.

Assume all functions in this system return \accept or \rej. (We can always move the output into the arguments if a function is not of this form.)
Here's a natural way to prove the mentioned execution: Put the arguments to $B$ in the public inputs of both the circuits of $A$ and $B$.
Verify the proofs $\prf_A,\prf_B$ for $A,B$; and check via the public inputs the same value was used in both proofs for the arguments of $B$.

This however, doesn't yet deal with the notes. During execution, note operations happened in a certain order.
We can thus assign a \emph{counter} equal to one for the first operation
% \Patrick{equal to one for the first operation}, 
and increment the counter with each operation.
We then need to check, for example, that if a note was read with a certain counter, it was indeed added
with a smaller counter.
We can include a description of the note operations performed by a function in the inputs of its circuit. This description will contain the operation type (\add, \del, \read), the note value, and the counter.
The issue is, what if $A$ is reading a note that was added in the internal call to $B$?
Checking the existence of an $\add$ operation with smaller counter requires a constraint \emph{between} the inputs of both circuits. And for an execution consisting of more calls, this constraint can involve any two circuits in the call tree.
% Describing the issue more generally, since we are forced to prove things in a different order than they were executed, we must enforce a global consistency between the witnesses of all iterations.

This brings us to the notion of \emph{Repeated Computation with Global state} (RCG). In RCG we have a transition predicate taking us from one state to the next. We wish to prove we know a sequence of witnesses taking us from a legal initial state to a certain publicly known final state. This might remind the reader of the popular notion of \emph{incrementally verifiable computation} (IVC). There are two differences.

\begin{itemize}
 \item
In RCG we are not interested in ``incremental'' proofs of one step, only in proofs for a whole
sequence of transitions ending in a desired final state.
\item In RCG we also have a \emph{final predicate} checking a joint consistency condition between witnesses from all iterations.
\end{itemize}
 One could ask, why not \emph{only} have a final predicate that includes the transition checks? In other words, a monolithic circuit for the whole computation.
The point is that in our use case the final predicate is applied to small parts of each iteration's witness -- namely the note operations. As a result, the decomposition into a transition and final predicate can facilitate obtaining better prover efficiency, especially in terms of prover space.
Roughly, we'll require space sufficient for storing the inputs to the final predicate, in addition to the space required to prove a single transition.

\subsection{Related work}
Recent work \cite{moonmoon, mangrove} as well as ongoing work \cite{jenstalk} uses folding schemes \cite{othernova,nova} to break up proving statements about large computation into smaller statements.
The objective being reducing prover memory and/or improving prover parallelism.
These works have not formally defined a notion like RCG, and rather use the IVC terminology. We believe the RCG framework may be better suited for
capturing the properties of these constructions. In terms of the concrete constructions, there are overlaps with this work, notably a two-pass over
part of the witness to generate a random challenge. As alluded to earlier,
one distinction is that these works start with a computation that is already linear, while here we start with cyclic computation and must ``compile'' it into a ``linear'' statement.
\subsection{Overview of the paper}



In Section \ref{sec:Preliminaries}, we go over terminology and preliminaries.
Notably, in Section \ref{subsec:zta} we introduce the \emph{Zero-Testing Assumption} from \cite{novarecursive} that enables us to
avoid heuristic assumptions as commonly happens in IVC papers due to the need of instantiating the random oracle.
In Section \ref{sec:model}, we introduce our execution model involving record operations and execution trees.
In Section \ref{sec:RCG}, we introduce the notion of Repeated Computation with Global state, and show how to reduce computations in the model of Section \ref{sec:model} to RCG.
In Section \ref{sec:Fstar}, we show how ``log-derivative methods'' \cite{bplusplus,logup} can capture global consistency of operations
as defined in previous sections.
In Section \ref{sec:folding}, we show how the \protogal folding scheme \cite{protogalaxy} can be proven secure under the ZTA (without
the need of a random oracle).
In Section \ref{sec:FtoFprime}, we present our main zk-SNARK construction. The main ingredient is a ``folding to IVC'' reduction similar to the ones in 
\cite{othernova,nova}.
In Section \ref{sec:general}, we outline how RCG can be implemented for a more general set of functions.

A reader wanting to get a feeling of the main construction ideas might want to focus first on Sections \ref{sec:model}--\ref{sec:Fstar}.

\section{Preliminaries}\label{sec:Preliminaries}
\subsection{Terminology and Conventions}\label{sec:terminology}
We assume all algorithms described receive as an implicit parameter the security parameter $\lambda$.
Similarly, all integer parameters in the paper are implicitly functions of $\lambda$, and of size at most \poly unless explicitly stated otherwise.

Whenever we use the term \emph{efficient}, we mean an algorithm running in time \poly. Furthermore,
we assume an \emph{object generator} \obgen that is run with input $\lambda$ before all protocols, and returns all fields and groups used. Specifically, in our protocol $\obgen(\lambda) = (\F, \G,g,\cmsetup)$ where
\begin{itemize}
\item \F is a field of \textbf{prime} size $r = \lambda^{\omega(1)}$
.
\item $\G$ is a group of size $r$.
\item $g$ is a uniformly chosen generator of \G.
\item $\cmsetup$ is a uniformly chosen key for a collision-resistant homomorphic commitment scheme $\cm:\F^M \to \G$.
\end{itemize}
We usually let the $\lambda$ parameter be implicit, e.g. write \F instead of $\F(\lambda)$.
We denote by \polysofdeg{d} the set of univariate polynomials over \F of degree smaller than $d$.
We write \G additively.
\emph{All probabilistic statements in the paper are additionally over the randomness of \obgen.}
% We use the notations $\enc1{x}\defeq x\cdot g_1$ and $\enc2{x}\defeq x\cdot g_2$.

We often denote by $[n]$ the integers \set{1,\ldots,n}.
% For example, when we refer below to the field $\F$, it is in fact a function $\F(\lambda)$ of $\lambda$, and part of
% the output of $\obgen(\lambda)$.
We use the acronym e.w.p. for ``except with probability''; i.e. e.w.p. $\gamma$ means with probability \emph{at least} $1-\gamma$.


% \paragraph{Representing \G}
% Assume an injective function $R:\G \to \F^2$.
% Whenever we discuss $a\in \G$ we assume it is represented as $R(a)$.
% When we say for $b\in \F^2$ that $b\in \G$ we mean that there exists $a\in \G$ with $R(a)=b$.

\subsection{Zero-Testing Assumption}\label{subsec:zta}
Throughout this paper, we'll make use of a variant of the \emph{Zero-Testing Assumption (ZTA)} from \cite{novarecursive} given in Definition \ref{dfn:ZTA} as well as its generalization, the \emph{$t$-variate Zero-Testing Assumption}, we introduce in Definition \ref{dfn:multiZTA}.

\begin{dfn}\label{dfn:ZTA}
Fix $\cm:\F^M\to K$, hash function $\hash:\B^*\to \F$, and integer $d$. Fix the family of functions \ztafuncs.
We say the tuple $(D,x,\tau)$ is a \emph{degree $d$-relation for $(\ztafuncs,\hash,\cm)$} if
\begin{enumerate}
 \item $D\in \ztafuncs$.
 \item $f(X)\defeq D(x,\tau)$ is a non-zero element of \polysofdegeq{d}.
 \item Setting $z\defeq \hash(\cm(x),\tau)$, we have $f(z)=0$.
\end{enumerate}
The Zero-Testing Assumption (ZTA) for $(\ztafuncs,\hash,\cm,d)$ states that for any efficient \adv, the probability that
\adv outputs a degree $d$-relation for $(\ztafuncs,\hash,\cm)$ is \negl.
\end{dfn}

\begin{remark}
The validity of ZTA is very sensitive to the choice of $D$. At first thought, one would want to prohibit $D$ from \emph{any} invocation of \hash or \cm. However, as will be seen later, this will be over-restrictive for capturing what is needed in multi-round protocols. We make sure not to use $D$ where \hash is invoked on $(\cm(x),\tau)$, and conjecture this suffices for avoiding couter-examples. In any case, analyzing a hash-based protocol under ZTA with a specific choice of $D$  allows for falsifiability - as opposed to an analysis in the ROM followed by applying Fiat-Shamir .
\end{remark}



\begin{dfn}[$t$-variate ZTA]\label{dfn:multiZTA}
Fix $\cm:\F^M\to K$, hash function $\hash:\B^*\to \F$, and integer $d$. Fix the family of functions \ztafuncs.
We say the tuple $(D,x,\tau)$ is a \emph{$(t,d)$-relation for $(\ztafuncs,\hash,\cm)$} if
\begin{enumerate}
 \item $D\in \ztafuncs$.
 \item $f(X_1,\ldots,X_t)\defeq D(x,\tau)$ is a non-zero element of $\F_{\leq d}[X_1,\ldots,X_t]$.
 \item Setting $z_i\defeq \hash(\cm(x),\tau,i)$ for $i\in[t]$, we have $f(z_1,\ldots,z_t)=0$.
\end{enumerate}
The $t$-variate Zero-Testing Assumption (ZTA) for $(\ztafuncs,\hash,\cm,d)$ states that for any efficient \adv, the probability that
\adv outputs a $(t,d)$-relation for $(\ztafuncs,\hash,\cm)$ is \negl.
\end{dfn}

We prove that the univariate ZTA implies the $t$-variate ZTA.

\begin{lemma}
Fix a family of functions \ztafuncs whose outputs are polynomials in $\F_{\leq d}[X_1,\ldots,X_t]$. Let $\ztafuncs_t$ be a family of functions to be defined in the proof. Then the univariate ZTA for $(\ztafuncs_t,\hash,\cm,d)$ implies the $t$-variate ZTA for $(\ztafuncs,\hash,\cm,d)$ and $t=\poly$.
\end{lemma}
\begin{proof}
Let \adv be an adversary against the $t$-variate ZTA that outputs the $(t,d)$-relation $(D,x,\tau)$ for $(\ztafuncs,\hash,\cm)$. We construct the adversary \advprime against the univariate ZTA that outputs a degree-$d$ relation for $(\ztafuncs_t,\hash,\cm)$, where $\ztafuncs_t$ will be the union of all the functions $D_i$ defined in the following.

Write $f(X_1,\ldots,X_t)\defeq D(x,\tau)$ as a polynomial in $X_t$ over $\F[X_1,\ldots,X_{t-1}]$:
\[f(X_t)=\sum_{i=0}^d C_i(X_1,\ldots,X_{t-1}) X_t^i.\]
For $i\in[t]$, denote $z_i\defeq\hash(\cm(x),\tau,i)$. Suppose first that $f(z_1,\ldots,z_{t-1},X_t)\not\equiv 0$. Then \advprime can output the degree-$d$ relation $(D_t,x,\tau_t)$, where $D_t$ is the function that computes $f_t(X)\defeq f(z_1,\ldots,z_{t-1},X)$ given $x$ and $\tau_t\defeq(\tau,t)$, deriving $z_1,\ldots,z_{t-1}$ via \hash as part of its operation. Note that $f_t(z_t)=0$ with $z_t=\hash(\cm(x),\tau_t)$.

Otherwise, there is a non-zero polynomial $C_i\in\F_{\leq d}[X_1,\ldots,X_{t-1}]$ which satisfies $C_i(z_1,\ldots,z_{t-1})=0$. If $C_i(z_1,\ldots,z_{t-2},X_{t-1})\not\equiv 0$, \advprime can output the degree-$d$ relation $(D_{t-1},x,\tau_{t-1})$, where $D_{t-1}$ is the function that computes $f_{t-1}(X)\defeq C_i(z_1,\ldots,z_{t-2},X)$ given $x$ and $\tau_{t-1}\defeq(\tau,t-1)$.

Recursively define degree-$d$ relations $(D_i,x,\tau_i)$ until $i=1$ and we have a univariate non-zero polynomial $C_j'\in\F_{\leq d}[X_1]$ with $C_j'(z_1)=0$. In this base case, \advprime can output the degree-$d$ relation $(D_1,x,\tau_1)$, where $D_1$ is the function that computes $f_1(X)\defeq C_j'(X)$ given $x$ and $\tau_1\defeq(\tau,1)$, finishing the proof.
\end{proof}

\section{The execution model}\label{sec:model}
We present a formal framework for describing function executions enabling both internal function calls and global state.

We begin in Section \ref{sec:exec_model:record_ops} by introducing \emph{record operations} which is our specific notion of operating on a global state.
% 	The global state consists of values, simply referred to as \emph{values}, that can be added, read or deleted by the contract functions; and that a 
% 	function can call other functions.
% 	As the called functions modify the global state, for instance -- delete a note that was added during the execution, an ordering on 
% 	the operations on the global state is necessary to guarantee their consistency (e.g.,\ guarantee that a note can only be deleted if it were 
% 	first added).
Record operations keep track of the computation steps at which	records (roughly corresponding to notes in the introduction) were added, read and deleted. 
We then define what it means for a set of such operations to be \emph{consistent}. For example, we want to enforce that a record can be deleted only if it was first added. 

	The eventual goal is to prove that a certain set of records is the output of a function execution (where that execution includes the function's internal calls).
	The proof should not reveal any information about which function was executed, as long as it belongs to a pre-defined set of legal functions,
	or about its arguments.
	To do so, it is sufficient to prove knowledge of an execution tree with the initial function at the root, the functions it calls at its children nodes and so forth. 
% 	The execution of the initial function is valid if the function at each node accepts on its arguments.
	Section \ref{sec:exec_model:relation} defines a relation which formally captures what it means for an individual function to accept on its arguments,
	and Section \ref{sec:validexec} formally defines such execution trees.

\begin{remark}
For simplicity, and in contrast to the introduction, we don't explicitly discuss contracts. We only model functions operating on a shared global state.
As in Aztec each function can only operate on notes of its contract, this corresponds to a system with one contract. Capturing the general system mainly requires modelling the restriction that a function is only operating on the subset of notes belonging to its contract.
\end{remark}

\subsection{Record operations}
\label{sec:exec_model:record_ops}
\emph{Records} are pairs $(\v,\c)$, where $\v\in \F$ is the \emph{value}, and $\c\in \countrange$ is a \emph{counter}.
A \emph{record operation} has one of the following forms:
\begin{itemize}
 \item $(\add,\v,\c)$,
\item $(\del,\v,\vc,\c)$,
\item $(\read,\v,\vc,\c)$.
\end{itemize}
Here $\v\in \F$ is a value and $\c,\vc \in \countrange$ are counters.
$\c$ is interpreted as the counter of the current operation.
$\vc$ is interpreted as the counter of the operation where
the value was added in the case of a \read or \del operation.



We say a sequence \ops of record operations of size $M$ is \emph{consistent} if
\begin{enumerate}
\item The counter values $\c$ are distinct in all elements of \ops, and as a set equal to \countrange.
\item The $\vc$ fields in all $\del$ operations $(\del,\v,\vc,\c)\in \ops$ are distinct.
\item If $(\del,\v,\vc,\c)\in \ops$, then $\vc<\c$ and $(\add,\v,\vc)\in \ops$.
\item If $(\read,\v,\vc,\c)\in \ops$, then $\vc<\c$ and $(\add,\v,\vc)\in \ops$.
\end{enumerate}

Let \recset be a set of records.
We say $\ops$ \emph{has output \recset} if:
\begin{itemize}
 \item $\ops$ is consistent.
 \item $\recset=\set{(\v,\c) \mid (\add,\v,\c)\in \ops \land \forall \c'\in \countrange,(\del,\v,\c,\c')\notin \ops}$. In words,
 \recset is the set of values that were added and not deleted.
\end{itemize}



\subsection{The Plonkish relation}
\label{sec:exec_model:relation}
Now we introduce a relation \relapp describing the individual function executions tailored to make it convenient to later discuss an execution of a \emph{sequence} of functions calling each other.
The executed function is represented in the instance by a single group element \f. In the terminology of \cite{plonk}, \f is a commitment to the permutation and selector values of a specific \plonk circuit. In particular, \relapp is a ``universal'' Plonkish relation where the circuit is not fixed but chosen in the instance. 
% Additionally, the instance contains a group element \f representing, in the terminology of \cite{plonk} functions are represented by commitments which consist of a single group element.}

Additionally, the instance adheres to a form containing both the record operations and the details of the inner calls of the individual function execution.
We stress however, that the \emph{interpretation} of these values as record operations and inner calls, only happens in the next section when we discuss valid executions trees;
and doesn't manifest in the definition of \relapp.
% We stress that these values will be interpreted as record operations and internal only in the next section when we discuss valid executions.
Some choices of constants -- like \args being of size four -- are arbitrary.

We fix a polynomial $G:\F^8\to \F$, and integers $N,\n$ that are implicit parameters in the following definition of relation \relapp.

\relapp consists of all pairs $(\instapp, \witapp)$ having the form
\begin{itemize}
 \item
$\instapp= (\f,\args,\callnum, \f_1,\args_1, \f_2,\args_2,\ops)$
where $\f,\f_1,\f_2 \in \G,\args\in \F^4,\callnum\in \set{0,1,2}$;
\item $\witapp=(\witf,\wit)$
where
\begin{itemize}
 \item
$\witf=(\perm_1,\ldots,\perm_4,\sel_1,\ldots,\sel_4)$,where $\perm_j \in [|\instapp|+N]^{\n},\sel_j \in \F^\n$ for each $j\in [4]$
\item $\wit\in \F^N$
\end{itemize}
\end{itemize}
such that
\begin{enumerate}
\item Setting $x=(\instapp,\wit)$, for all $i\in [\n]$
\[G(\sel_{1,i},\ldots,\sel_{4,i},x_{\perm_{1,i}},\ldots,x_{\perm_{4,i}})=0.\]
\item $\f=\cm(\witf)$.
\end{enumerate}

\subsection{Valid execution trees}\label{sec:validexec}

By an \emph{execution tree of length $n$} we mean a binary tree \tree with $n$ vertices, whose nodes are
labeled by pairs $(\instapp,\witapp)$.
Let \funcs be a set of elements of \G.
% \Patrick{Suggestion: This set represent the set of all contract-function commitments.}
Given such \tree we say it is a \emph{valid execution of length $n$ with function set \funcs and output \recset} if
\begin{enumerate}
 \item For each $\node\in\tree$, its label $(\instapp,\witapp)$ is in \relapp.
    \item For each $\node\in \tree$, let $(\instapp,\witapp)$ be its label. Let
$\instapp= (\f,\args,\callnum, \f_1,\args_1, \f_2,\args_2,\ops)$. Then
    \begin{itemize}
    \item $\f\in \funcs$.
     \item The number of its children is \callnum.
     \item For $i\in [\callnum]$, let $(\f^i,\args^i,\callnum^i, \f^i_1,\args^i_1, \f^i_2,\args^i_2,\ops^i)$ denote the first component of the label of $\node$'s $i$-th child. Then $\f_i=\f^i$ and $\args_i=\args^i$.
     \item Let \ops be the multi-set union of $\instapp.\ops$ over all nodes' labels $(\instapp,\witapp)$. Then \ops has output \recset.
    \end{itemize}
\end{enumerate}
Given a set of group elements \funcs, say it has \emph{Merkle root \root} if \root is the root of a Merkle tree with the elements of \funcs at the leaves using some pre-determined encoding.

We define a relation \relexec capturing knowledge of an execution of bounded length with a certain output set of records.
$\relexec$ consists of the pairs $(\instexec,\witexec)$
of the form
\begin{itemize}
 \item $\instexec=(\root,C,\recset)$,
 \item $\witexec=(n,\tree)$,
\end{itemize}
such that $n\leq C$, and \tree is a valid execution tree of length $n$ with function set \funcs having Merkle root \root, and output set \recset.

\section{Repeated Computation with Global state}\label{sec:RCG}
Motivated by space-efficient proofs for \relexec, we introduce the notion of \emph{Repeated Computation with
Global state} (RCG).
RCGs enable us to deal separately with the local consistency of iterative steps of a transition function,
and over-all consistency of a global state consisting of a part of each iteration's witness.
We first define the general notion, and then in Section \ref{sec:exec->RFC} show how to capture valid execution trees with it.


\paragraph{Defining RCG relations}
An RCG relation is defined by a pair of functions $(F,\finpred)$.
We call $F(Z,W,Z^*,S)\to \set{\accept,\rej}$ the \emph{transition predicate}, and $\finpred(Z,S_1,\ldots,S_n,\recset)\to \set{\accept,\rej}$ the \emph{final predicate}.
We informally think of
\begin{itemize}
\item $Z$ as the public input and $W$ as the private input of $F$.
\item $Z^*$ as the output of $F$ (although the actual output is \set{\accept,\rej}).
\item $S$ as the part of the private input that will be used in the final predicate.
\end{itemize}

\noindent
\emph{The relation $\relrcg$} is the set of pairs $(\inpF,\witF)$ with
\begin{itemize}
\item $\inpF=(\zfin,C,\recset)$,
\item $\witF=(n,z=(z_0,\ldots,z_n),w=(w_1,\ldots,w_n),s=(s_1,\ldots,s_n))$
\end{itemize}
such that
\begin{enumerate}
 \item $z_0.\init = \true$.
% 	 \Patrick{You are here tacitly assuming (and requiring) structure on $z,$ namely that it is a tuple with one component that is a boolean 
% 	 value.}
 \item $z_n=\zfin$.
 \item $n\leq C$.
 \item For each $i\in [n]$, $F(z_{i-1},w_i,z_i,s_i)=\accept$.
 \item $\finpred(\zfin,s_1,\ldots,s_n,\recset)=\accept$.
\end{enumerate}


We say a \zksnark for \relrcg is \emph{space-efficient} if, given $s$ and streaming access
to $z$ and $w$, \prv requires space $O(|F|+|s|+\lambda \log n)$.
Here $|F|$ is defined as $\M+n'$ where $f:\F^\M\to {\F^{n'}}$ is the \protogal constraint function representing $F$ (see Section \ref{sec:folding}).


\subsection{Valid executions as RCGs}\label{sec:exec->RFC}
We define a specific RCG relation \relrcg capturing valid execution trees as defined in Section \ref{sec:validexec}.
Loosely speaking, the transition function $F$ will update a call stack of functions yet to be executed, and execute the function that is
at the top of the stack.
The final predicate \finpred will check the union of record operations from all iterations is consistent.\\

\noindent
More precisely, define the function $F(Z,W,Z^*,S)\to \set{\accept,\rej}$ as follows.
\begin{itemize}
 \item $Z=(g,\root,\init)$ where $g$ is a stack of elements of the form $(\f,\args)$, \root is a root of a Merkle tree, and \init is a boolean.
 \item $Z^*=(g^*,\root^*,\init^*)$ has the same form.
 \item $W=(\path,\instnoops,\witapp)$.
 \item $S$ is a set of record operations.
\end{itemize}

\noindent Under this notation,
$F(Z,W,Z^*,S)=\accept$ if and only if
\begin{enumerate}
 \item If $\init=\true$, $g$ contains exactly one element.
 \item Setting $\instapp=(\instnoops,S)$, we have $(\instapp,\witapp)\in \relapp$.
 \item Denoting $g[0]=(\f,\args)$, we have $\f=\instnoops.\f$ and $\args=\instnoops.\args$.
 \item \path is a Merkle path from \f to \root.
 \item $\root=\root^*$.
 \item $g^*$ is the result of popping $(\f,\args)$ from $g$ and then pushing the $\instapp.\callnum$ elements
 $(\instapp.\f_i,\instapp.\args_i)$ for $i\in [\instapp.\callnum]$.
\end{enumerate}


Denote by \empty the empty stack.
We define $\finpred(z_n,s_1,\ldots,s_n,\recset)$ to output \accept if and only if
\begin{enumerate}
 \item $z_n.g=\empty$,
 \item Defining \ops as the multi-set union of $s_1,\ldots,s_n$, it is a well-formed set of record operations with output \recset.
\end{enumerate}


We show that proving knowledge of a witness for an instance of \relexec can be reduced to proving knowledge of a witness for an instance of 
\relrcg.

\begin{lemma}\label{lem:execasRCG}
There is an efficiently computable and efficiently invertible map $\varphi$ such that the following holds.
Let \funcs be a set of function commitments with Merkle root \root. Fix positive integers $n,C$ with $n\leq C$.
Define $\zfin=(\empty,\root,\false)$. Let \tree be an execution tree of length $n$.

Then $((\root,C,\recset),(n,\tree))\in \relexec$ if and only if $((\zfin,C,\recset),\varphi(n,\tree))\in \relrcg$.
\end{lemma}
\begin{proof}
We describe the operation of $\varphi$.
Given \tree of length $n$, let $(\instapp_1,\witapp_1),\ldots,(\instapp_n,\witapp_n)$ be the labels of its nodes according to
DFS order.
Define a sequence of stacks $g_0,\ldots,g_n$ according to the sequence of labels.

Namely, $g_0$ is the stack containing only $(\instapp_1.\f,\instapp_1.\args)$. And for each $i\in [n]$, $g_i$ is
the stack obtained by popping $g_{i-1}[0]$ and pushing $(\instapp_i.\f_j,\instapp_i.\args_j)$ for $j\in [\instapp_i.\callnum]$.
Now, define $z_0=(g_0,\root,\true)$ and for each $i\in [n]$, $z_i=(g_i,\root,\false)$.

To proceed we need to refer to the record operations in each instance separately.
For this purpose, for each $i\in [n]$ denote $\instapp_i=(\instnoops_i,\ops_i)$.
For each $i\in [n]$, let $\path_i$ be the path from $\instapp_i.\f$ to \root.
Define for each $i\in [n]$, $w_i=(\path_i,\instnoops_i,\witapp_i)$, $s_i=\ops_i$.
Finally set $z=(z_0,\ldots,z_n),w=(w_1,\ldots,w_n),s=(s_1,\ldots,s_n)$
and $\varphi(n,\tree)=(n,z,w,s)$. Given this definition of $\varphi$, the statement of the lemma is straightforward to check.
\end{proof}

\section{Removing the global state via rational identities}\label{sec:Fstar}
	We give rational identities which are equivalent to the consistency of record operations as formally defined 
	in Section \ref{sec:exec_model:record_ops}.
	They arise from ideas similar to those used in ``log-derivative lookups'' \cite{bplusplus,logup}.
	Using these identities, we then define a new RCG relation \relrcgstar capturing valid execution trees, i.e., \relexec. The advantage of \relrcgstar over \relrcg from Section \ref{sec:exec->RFC} is that the final predicate is ``trivial'' in the sense of only depending on the output of the final iteration.
	As we'll see in Section \ref{sec:FtoFprime}, this makes constructing a zk-SNARK for it more convenient.
% \paragraph{Rational Identities}
% Following work on ``log-derivative lookup'' \cite{bplusplus,logup}, we characterize the validity of record operations via rational identities.
\begin{claim}\label{clm:reducetologder}
Assume $\F$ has characteristic larger than $M+1$.
Let \recset be a set of records and $\ops=\sett{(\op_i,\v_i,\vc_i,\c_i)}{i\in \countrange}$ be a set of record operations (defining $\vc_i=0$ when $\op_i=\add$) with $\vc_i<\c_i$ for all $i\in \countrange$.
Then \ops has output \recset if and only if the following rational function identities hold:
\begin{enumerate}
 \item \[\sum_{(\v,\c)\in \recset}\frac{1}{X+\v Y+\c}=\sum_{i\in \countrange,\op_i=\add}\frac{1}{X+\v_i Y+\c_i}-\sum_{i\in \countrange, \op_i=\del}\frac{1}{X+\v_i Y+\vc_i}.\]
 \item For some $m\in \F^M$, we have
 \[\sum_{i\in \countrange,\op_i=\add}\frac{m_i}{X+\v_i Y+\c_i}=\sum_{i\in \countrange, \op_i=\read}\frac{1}{X+\v_i Y+\vc_i}.\]
 \item \[\sum_{i\in \countrange}\frac{1}{X+\c_i}=\sum_{i\in \countrange}\frac{1}{X+i}.\]
\end{enumerate}
\end{claim}
\begin{proof}

We focus on the only if direction. That is, if \ops doesn't have output \recset one of the three identities should not hold.
 Let $R_{v,c}(X,Y)\defeq \frac{1}{X+vY+c}$. The main fact we use is that the rational functions $\sett{R_{v,c}}{(v,c)\in \F^2}$ are linearly independent.
 Thus, $\sum_{v,c} a_{v,c} R_{v,c} = \sum b_{v,c} R_{v,c}$ implies $a_{v,c}=b_{v,c}$ for each $(v,c)\in \F^2$.
 The event of \ops not having output \recset means one of the following occurs.
 \begin{enumerate}
  \item The multi-set of counters $\sett{\c_i}{i\in \countrange}$ doesn't equal \set{1,\ldots,M}. In this case, the LHS of the third identity will not have all one coefficients for the elements \sett{R_{0,i}}{i\in \countrange} and so cannot equal the RHS.

  Note that when we are not in this case the counters in \ops are all distinct, which we assume for the next cases.
 \item For some $\v,\vc,\c$, $(\del,\v,\vc,\c)\in \ops$ but $(\add,\v,0,\vc)\notin \ops$; or for some $\v,\vc,\c_1\neq \c_2$, $(\del,\v,\vc,\c_1),(\del,\v,\vc,\c_2)\in \ops$: In the first identity RHS, we will have $R_{\v,\vc}$ with coefficient in the range $\set{-1,\ldots,-M}$, while in the LHS it has coefficient one or zero.
 \item For some $\v,\vc,\c$, $(\read,\v,\vc,\c)\in \ops$ but $(\add,\v,0,\vc)\notin \ops$: In the second identity RHS $R_{\v,\vc}$ will have a coefficient in the range $\set{1,\ldots,M}$ while in the LHS it has coefficient zero.
 \item \recset is \emph{not} equal to the set $\recset'$ of $(\v,\c)$ for which $(\add,\v,0,\c)\in \ops$ but $(\del,\v,\c,\c')\notin \ops$. We look at the first identity. $\recset'$ is precisely the set of $(\v,\c)$ with coefficient one on the RHS, while \recset is the set of $(\v,\c)$ with coefficient one on the LHS. Hence the first identity cannot hold in this case.
 \end{enumerate}
\end{proof}








% We reduce the relation \relrcg from the last section to \relrcgstar:
\paragraph{Defining \relrcgstar}
	We now define the RCG relation \relrcgstar which will permit efficient proofs that record operations are consistent. 
	The idea is to evaluate the above rational identities at a random point, and have the transition predicate incrementally check the evaluation is correct
	by a running sum.
	For the random evaluation point to be generated in a manner that is sound but also allow for an incremental computation of the rational identity 
	summand by summand, we compute it via a hash chain.
	This chain includes at each step the new set of record operations and the last hash output, which is in essence a commitment to all the record
	operations in previous steps.
	This idea also appears in \cite{moonmoon,mangrove,jenstalk}. We proceed with the formal definition.\\ \\
\noindent	
Let $F$ denote the function $F(Z_F,W_F,Z_F^*,S_F)\to \set{\accept,\rej}$ from Section \ref{sec:exec->RFC}.
Let $k\defeq |S_F|$, $\cm:\F^{5k} \to \G$, and set $M\defeq kn$.\\

\noindent Define the function $F^*:(Z,W,Z^*)\to \set{\accept,\rej}$:
\begin{itemize}
 \item $Z=(Z_F,\inchash,\incsum,\alpha,\beta,\eps)$.
 \item $Z^*=(Z_F^*,\inchash^*,\incsum^*,\alpha^*,\beta^*,\eps^*)$.
 \item $W=(W_F,S_F,m)$.
\end{itemize}
\noindent
Under this notation
$F^*(Z,W,Z^*)=\accept$ if and only if
\begin{enumerate}
\item $F(Z_F,W_F,Z_F^*,S_F)=\accept$.
\item If $Z_F.\init = \true$, $\inchash=\emptyset$ and $\incsum=0$.
\item Let $S_F=\sett{(\op_i,\v_i,\vc_i,\c_i)}{i\in [k]}$. We have $\vc_i<\c_i$ for all $i\in [k]$, and \\
$\incsum^*=\incsum\;+$
\[\sum_{i\in [k];\op_i = \add}\frac{1+ \eps m_i}{\alpha +\beta \v_i+\ \c_i}-\sum_{i\in [k];\op_i = \read}\frac{\eps}{\alpha +\beta \v_i+\vc_i}-\sum_{i\in [k];\op_i = \del}\frac{1}{\alpha +\beta \v_i+ \vc_i}+ \sumi{k}\frac{\eps^2}{\alpha+\c_i}.\]
\item $\alpha^*=\alpha, \beta^*=\beta,\eps^*=\eps$.
\item $\inchash^*=\hash(\inchash,\cm(S_F,m))$. \\
\end{enumerate}

\noindent $\finpred^*(Z,\recset)=\accept$ if and only if
\begin{enumerate}
 \item $Z.g=\empty$,
 \item $\incsum=\sum_{(\v,\c)\in \recset} \frac{1}{\alpha + \beta \v+ \c}+\sum_{i\in \countrange}\frac{\eps^2}{\alpha+i}$,
 \item $\hash(\inchash,\recset,1)=\alpha$, $\hash(\inchash,\recset,2)=\beta$, $\hash(\inchash,\recset,3)=\eps$.
\end{enumerate}

\noindent
We show that \relrcgstar captures \relrcg and consequently valid executions.
\begin{lemma}\label{lem:FtoFstar}
There is an efficiently computable map $\varphi^*$ such that the following holds.
Suppose an efficient adversary \adv outputs $(\inst,\wit)\in \relrcgstar$.
Set $d\defeq 3M+|\recset|+1$. Define $\cm^*(s_1,\ldots,s_n,m_1,\ldots,m_n)\defeq h_n$, where $h_0\defeq\emptyset$ and $h_i\defeq\hash(h_{i-1},\cm(s_i,m_i))$ for $i \in [n]$.
Let \ztafuncs be a function family to be defined in the proof.
Assume the 3-variate ZTA holds for $(\ztafuncs,\hash,\cm^*,d)$.
Then e.w.p. \negl, $\varphi^*(\inst,\wit)\in \relrcg$.
\end{lemma}
\begin{proof}
Given an instance $\inst=(\zfin^*,C,\recset)$ with $\zfin^*=(\zfin,\inchash,\incsum,\alpha,\beta,\eps)$ and witness $\wit=(n,z',w')$ with $z'=(z_0',\ldots,z_n'),w'=(w_1',\ldots,w_n')$ output by \adv, denote
$z_i'=(z_i,\inchash_i,\incsum_i,\alpha_i,\beta_i,\eps_i), w_i'=(w_i,s_i,m_i)$.
Define $\varphi^*(\inst,\wit)\defeq(\inpF,\witF)$ as
\[\inpF\defeq (\zfin,C,\recset),\ \witF\defeq (n,(z_0,\ldots,z_n),(w_1,\ldots,w_n),(s_1,\ldots,s_n)).\]

From $(\inst,\wit)\in \relrcgstar$, we know \witF satisfies the transition constraints, namely for $i\in [n]$,
$F(z_{i-1},w_i,z_i,s_i)=\accept$. We also know that $z_0.\init = \true$, $z_n=\zfin$, and $n\leq C$.
It is left to show that e.w.p. \negl $\finpred(z_n,s_1,\ldots,s_n,\recset)=\accept$. Since $z_n.g=\empty$, this is equivalent to showing that the rational identities from Claim \ref{clm:reducetologder} hold e.w.p. \negl.

From $F^*(z_{i-1}',w_i',z_i')=\accept$ for all $i\in [n]$ and $\finpred^*(z_n',\recset)=\accept$, we know the equations from Claim \ref{clm:reducetologder} hold
at $\alpha,\beta,\eps$. That is, defining the rational function
\begin{align*}
r(X,Y,Z)\defeq&\sum_{(\v,\c)\in \recset}\frac{1}{X+\v Y+\c}-\sum_{i\in \countrange,\op_i=\add}\frac{1}{X+\v_i Y+\c_i}+\sum_{i\in \countrange, \op_i=\del}\frac{1}{X+\v_i Y+\vc_i} \\
&+Z\left(\sum_{i\in \countrange,\op_i=\add}\frac{(m_1\|\ldots\|m_n)_i}{X+\v_i Y+\c_i}-\sum_{i\in \countrange, \op_i=\read}\frac{1}{X+\v_i Y+\vc_i}\right) \\
&+Z^2\left(\sum_{i\in \countrange}\frac{1}{X+\c_i}-\sum_{i\in \countrange}\frac{1}{X+i}\right),
\end{align*}
we have $r(\alpha,\beta,\eps)=0$. If any of the three rational identities from Claim \ref{clm:reducetologder} does not hold, we have $r(X,Y,Z)\not\equiv 0$.
Let $f\in\F_{\leq d}[X,Y,Z]$ denote the resulting non-zero degree-$d$ polynomial when multiplying $r(X,Y,Z)$ with all of its denominators. Note that $f(\alpha,\beta,\eps)=0$. Define $D$ as the function that computes $f(X,Y,Z)$ given $x\defeq(s_1,\ldots,s_n,m_1,\ldots,m_n)$ and $\tau\defeq\recset$. Set $\ztafuncs\defeq\{D\}$. Then we can define an efficient adversary \advprime against the $3$-variate ZTA for $(\ztafuncs,\hash,\cm^*,d)$ that outputs the $(3,d)$-relation $(D,x,\tau)$, which has probability \negl.
\end{proof}





\section{Non-interactive folding schemes}\label{sec:folding}
We fix a vector space $K$ over \F, and an $\F$-linear function $\cm:\F^M\to K$ that will be an implicit parameter in Definition \ref{dfn:accschme}.
We say a relation \rel is \emph{\cm-compatible} if every element of \rel has the form $(\cm(\wit),\wit)$.
We say \rel is \emph{\cm-extendable} if every element of \rel has the form $((\cm(\wit),\tau),\wit)$ for some $\wit,\tau$.
\begin{dfn}\label{dfn:accschme}
Fix relations \rel and \accrel that are \cm-compatible and \cm-extendable, respectively. An \emph{\accscheme{\rel}{\accrel}} is a pair of algorithms $(\prv, \ver)$
such that

\begin{enumerate}
 \item \prv on input $(\insttbase,\inst';\wit,\wit')$ produces a pair $(\instt,\wit^*)$ and proof \prf.
 \item \ver on input $(\insttbase,\inst',\instt,\prf)$ outputs \accept or \rej such that
% \item \ver receives as $\inst,\inst'$ as inputs and outputs \accept or \rej at the end.
\begin{enumerate}
 \item \textbf{Completeness:} If $(\insttbase,\wit)\in \accrel, (\inst',\wit')\in \rel$ and $\prv(\insttbase,\inst';\wit,\wit')=(\instt,\witstar,\prf)$, then with probability $1-\negl$, $(\instt,\witstar)\in \accrel$ and $\ver(\insttbase,\inst',\instt,\prf)=\accept$.
\item \textbf{Knowledge soundness given extractable commitments:}

For any efficient \adv the probability of the following event is \negl:
\adv outputs $(\inst,\tau),\inst',(\inststar,\tau^*),\wit,\wit',\witstar,\prf$
such that
\begin{enumerate}
\item $\cm(\wit)=\inst,\cm(\wit')=\inst',\cm(\witstar)=\inststar$,
\item $\ver((\inst,\tau),\inst',(\inststar,\tau^*),\prf)=\accept$,
\item $((\inststar,\tau^*),\witstar)\in\accrel$,
\item $((\inst,\tau),\wit)\notin\accrel$ or $(\inst',\wit')\notin \rel$.
\end{enumerate}
\end{enumerate}
\end{enumerate}
\end{dfn}
\begin{remark}\label{rem:agm->ext commitments}
 The justification for requiring only knowledge soundness given extractable commitments is as follows.
 We assume the Algebraic Group Model \cite{agm} and use a commitment scheme based on linear combination of group elements like \cite{kate}.
 In this model with such a commitment scheme an adversary \adv must output \wit, with $\cm(\wit)=\inst$ whenever it outputs some $\inst\in K$.
 For more details see \cite{agm} or Section 2.2 of \cite{plonk}, as well as Section \ref{sec:recursive} of this paper.
\end{remark}

\subsection{Relations for folding schemes}
We define a more general satisfiability relation than in \cite{protostar, protogalaxy}.
We have as parameters, integers $n,\M,d$ and an $\F$-vector space $K$.
We have a
\begin{itemize}
 \item \emph{Constraint function} $f:\F^\M\to \F^n$ which is a vector of $n$ $\M$-variate polynomials of degree $\leq d$,
\item \emph{Instance predicate} $\predinst:K \to \set{\accept,\rej}$,
\item \emph{Commitment function} $\cm:\F^\M \to K$ which is $\F$-linear and assumed
to be collision resistant.
\end{itemize}

Given $(f,\predinst,\cm)$ we define a relation $\rel_{f,\predinst,\cm}$ consisting of all pairs
$(\inst,\wit)$ such that
\begin{enumerate}
 \item $f(\wit)=0^n$.
 \item $\predinst(\inst)=\accept$.
 \item $\inst=\cm(\wit)$.
\end{enumerate}
We refer to a relation of this form as a \emph{protostar relation} as the definition is based on relations appearing in \cite{protostar}.
\paragraph{The relation \relrand}
 For brevity, let $\rel=\rel_{f,\predinst,\cm}$.
  As in \cite{protogalaxy}, we define the ``randomized relaxed'' version of \rel, \relrand. First, some required notation.
 Let $t\defeq \log n$. For $i\in [n]$, let $S_i\subseteq \set{0,\ldots,t-1}$ be the set such that $i-1=\sumj{S_i}2^j$. We define the $t$-variate polynomial $\pow_i$ as
 \[\pow_i(X_0,\ldots,X_{t-1}) \defeq \prod_{\ell\in S_i} X_\ell.\]
 Note that if $\betaa=(\beta,\beta^2,\beta^4,\ldots,\beta^{2^{t-1}})$, $\pow_i(\betaa)=\beta^{i-1}$.
% This implies the $n$ \emph{univariate} polynomials
% $\pow_i(X,X^2,\ldots,X^{2^{t-1}})$ are linearly independent.

  Given the above notation, \relrand consists of the pairs $(\insttbase,\wit)$ with $\insttbase=(\inst,\betaa,e)$ such that
 \begin{enumerate}
  \item $\inst=\cm(\wit)$.
  \item $\betaa\in \F^t, e\in \F$ and we have
  \[\sumi{n}\pow_i(\betaa) f_i(\wit) = e.\]
 \end{enumerate}
(Here, $f_i$ denotes the $i$-th output coordinate of $f$.)
\subsection{The \protogal scheme}
Deviating from \cite{protogalaxy}, we explicitly present \protogal as a \emph{non-interactive} folding scheme, and for the special case of folding $k=1$ instances.
We define $Z(X)\defeq X\cdot(1-X)$. We assume below \hash is a function mapping arbitrary strings to elements of \Fstar. \\ \\ \noindent
\underline{$\perpg(\insttbase=(\inst,\betaa,e),\inst_1;\wit,\wit_1)$:}
\begin{enumerate}
% \item \ver checks for each $i\in [k]$ that $\inst_i$ is \hash-consistent, and outputs \rej otherwise.
% \item \ver sends a challenge $\delta \in \F$.
 \item Compute $\delta=\hash(\insttbase,\inst_1)$. Define $\deltaa\defeq (\delta,\delta^2,\ldots,\delta^{2^{t-1}})\in \F^t$.
 \item\label{step:computeF} Compute the polynomial
 \[F(X)\defeq \sumi{n}\pow_i(\betaa+X\deltaa) f_i(\wit).\]
 (Note that $F(0)=\sumi{n} \pow_i(\betaa) f_i(\wit) = e$.)
\item\label{step:sendFcoeffs} Denote the non-constant coefficients of $F$ by $a\defeq (F_1,\ldots,F_t)$.
\item Compute $\alpha = \hash(\insttbase,\inst_1,a)$.
% \item\label{step:computeFalpha} Note that $F(\alpha)= e+\sumi{t}F_i \alpha^i$.
\item\label{step:computeBetastar} Compute $\betaa^*\in \F^t$ where $\betaa^*_i\defeq \betaa_i+\alpha\cdot \deltaa_i$.
\item\label{step:computeG} Define the polynomial $G(X)$ as
\[G(X)\defeq \sumi{n}\pow_i(\betaa^*) f_i(X\cdot \wit + (1-X)\wit_1).\]
\item Compute the polynomial $K(X)$ such that
\[G(X)= F(\alpha) X + Z(X) K(X).\]
\item\label{step:sendK} Let $b\defeq (K_0,\ldots,K_{d-2})$ be the coefficients of $K(X)$.
\item Compute $\gamma=\hash(\insttbase,\inst_1,a,b)$.
\item\label{step:compute-estar} Compute
\[e^* \defeq F(\alpha)\gamma + Z(\gamma)K(\gamma).\]
\end{enumerate}
Finally, output
\begin{itemize}
\item the instance
$\instt=(\inststar,\betaa^*,e^*),$
where \[\inst^*\defeq \gamma\cdot \inst + (1-\gamma) \inst_1,\]
\item the witness
$\witstar\defeq \gamma\cdot \wit + (1-\gamma)\cdot \wit_1,$
\item and the proof $\prf\defeq (a,b)$.\\
\end{itemize}
\noindent


\underline{$\verpg(\insttbase,\inst_1, \instt,\prf=(a,b))$:}
\begin{enumerate}
\item Check that $\predinst(\inst_1)=\accept$. Output \rej otherwise.
\item Compute $\delta,\alpha,\gamma$ as in the prover algorithm given $\insttbase,\inst_1,a,b$.
\item Check that $\instt$ is as computed as in the prover algorithm. Specifically, that
\begin{enumerate}
 \item For each $i\in [t]$, $\betaa^*_i= \betaa_i+\alpha\cdot \deltaa_i$.
 \item $ e^* = F(\alpha)\gamma + Z(\gamma)K(\gamma)$, where the coefficients of $F,K$ are defined by $a,b$ respectively.
 \item $ \inst^*= \gamma\cdot \inst + (1-\gamma) \inst_1$.
\end{enumerate}


Output \accept iff this is the case.
\end{enumerate}

\begin{remark}
 We stress that the verifier's description depends on $\predinst,\cm$ (and $t=\log n$ which is implicitly defined by the former), but not $f$; hence the notation \verpg.
 The independence of the verifier definition from $f$ will be crucial in Section \ref{sec:FtoFprime} to avoid a circular definition of $F'$.
\end{remark}



For the knowledge soundness analysis we'll use a variant of the Zero-Testing Assumption from \cite{novarecursive}, see Definition \ref{dfn:ZTA}.




\begin{thm}\label{thm:pgsoundness}
Set $d'\defeq \max \set{n,d}$. Denote $\cm'((\wit,\betaa,e),\wit_1)\defeq ((\cm(\wit),\betaa,e),\cm(\wit_1))$.
Let \ztafuncs be a family of four functions to be defined in the proof.
Assume that \cm is collision resistant and the ZTA holds for $(\ztafuncs,\hash, \cm',d')$.
Then \protogal is a \accscheme{\rel}{\relrand}.
\end{thm}
\begin{proof}
The main thing to prove is knowledge soundness given extractable commitments.
 Fix any efficient \adv. Let $E$ be the event that \adv outputs
$\insttbase=(\inst,\betaa,e),\inst_1,\instt=(\inststar,\betaa^*,e^*),$ $\wit,\wit_1,\witstar,\prf$ such that
\begin{enumerate}
\item $\cm(\wit)=\inst,\cm(\wit_1)=\inst_1,\cm(\witstar)=\inststar$,
\item $\verpg(\insttbase,\inst_1,\instt,\prf)=\accept$,
\item $(\instt,\witstar)\in\relrand$,
\item $(\insttbase,\wit)\notin\relrand$ or $(\inst_1,\wit_1)\notin \rel$.
\end{enumerate}
According to Definition \ref{dfn:accschme}, knowledge soundness is equivalent to $E$ having
probability \negl for any such \adv.
We construct an efficient \advprime that runs \adv, and when $E$ occurs outputs either a collision of
\cm or a degree $d'$-relation for $(\hash,\cm)$. By the theorem assumption this implies $E$ is contained in two events of
probability \negl, and must have probability \negl itself.

Assume we are in event $E$.
% Since $\verpg(\insttbase,\inst_1,\instt,\prf)=\accept$, we have $\inststar=\gamma \inst +(1-\gamma)\inst_1$.
% And since $(\instt,\witstar)\in \relrand$ we have $\cm(\witstar)=\inststar$.
Using linearity of \cm, when $E$ occurs we have
\[\cm( \gamma\wit+(1-\gamma)\wit_1)=\gamma \inst +(1-\gamma)\inst_1=\inststar=\cm(\witstar).\]
Thus, if $\witstar \neq \gamma \wit + (1-\gamma)\wit_1$, \advprime can output $(\witstar,\gamma\wit+(1-\gamma)\wit_1)$
as a collision of \cm.
Now assume that $\witstar = \gamma \wit + (1-\gamma)\wit_1$.
Suppose $\prf=(a,b)$, with $a=(a_1,\ldots,a_t),b= (b_0,\ldots,b_{d-2})$.
Define $F_0(X)\defeq e+\sum_{i\in [t]} a_iX^i,K'(X)\defeq \sum_{i=0}^{d-2} b_iX^i$.
Let $\delta,\deltaa,\alpha,\betaa^*, \gamma$ be computed as in the prover description given $a,b$.
Define the polynomials
\begin{align*}
F'(X) &\defeq F_0(X)-\sum_{i\in [n]} \pow_i(\betaa+X\deltaa) f_i(\wit), \\
G'(X) &\defeq F_0(\alpha)X+ Z(X)K'(X)-\sum_{i\in [n]}\pow_i( \betaa^*) f_i(X\wit +(1-X)\wit_1).
\end{align*}

Since $((\inststar,\betaa^*,e^*),\witstar)\in \relrand$ and $\verpg(\insttbase,\inst',\instt,\prf)=\accept$,
\begin{align*}
G'(\gamma) &= F_0(\alpha)\gamma + Z(\gamma)K'(\gamma)- \sum_{i\in [n]} \pow_i(\betaa^*) f_i(\gamma\wit +(1-\gamma)\wit_1) \\
           &= e^*-\sum_{i\in [n]} \pow_i(\betaa^*) f_i(\witstar) = e^*-e^* = 0.
\end{align*}

Set $x\defeq ((\wit,\betaa,e),\wit_1)$ and $\tau_1\defeq (a,b)$.
If $G'\not\equiv 0$, \advprime outputs the degree $d'$-relation $(D_1,x,\tau_1)$,
where $D_1$ is the function that computes $G'(X)$ given $x,\tau_1$.

Assume now that $G'\equiv 0$.

If $(\inst_1,\wit_1)\notin \rel$, using $Z(0)=0$ we have
\[G'(0)= -\sum_{i\in [n]}\pow_i( \betaa^*) f_i(\wit_1)=0.\]
Define the polynomial $A(X)\defeq \sumi{n}f_i(\wit_1)\pow_i(\betaa_1+X \delta,\betaa_2 +X \delta^2,\ldots,\betaa_t+X \delta^{2^{t-1}})$.
We have $A(\alpha)=0$. Suppose first that $A(X)\not\equiv 0$. Then setting $D_2$ to be the function that computes $A(X)$ given $x$ and $\tau_2\defeq a$, \advprime can output the degree $n$ relation $(D_2,x,\tau_2)$. Now assume $A(X)\equiv 0$.
Define the polynomial
\[B(X,Y)\defeq \sumi{n}f_i(\wit_1)\pow_i(\betaa_1+XY,\betaa_2+XY^2,\ldots,\betaa_t+X Y^{2^{t-1}}).\]
We have that $B(X,\delta)\equiv 0$.
Write $B(X,Y)$ as a polynomial in $X$ over $\F[Y]$:
\[B(X)=\sum_{i=0}^t C_i(Y)X^i.\]
Because we're in the case $(\inst_1,\wit_1)\notin \rel$, $B$ is a combination of the $n$ linearly independent polynomials $\sett{\pow_i(\betaa_1+XY,\betaa_2+XY^2,\ldots,\betaa_t+X Y^{2^{t-1}})}{i\in [n]}$ with at least one non-zero coefficient, and so $B(X,Y)\not\equiv 0$. This means one of the polynomials $C_i$ is non-zero, while $C_i(\delta)=0$.
We can use this to let \advprime output the degree $n$ relation $(D_3,x,\tau_3)$, where $D_3$ is the function that computes $C_i$ given $x$ and $\tau_3\defeq\emptyset$.

Now, assume that $(\insttbase,\wit)\notin \relrand$.
As we're still assuming $G'\equiv 0$, we have
\[G'(1)=F_0(\alpha)-\sumi{n}\pow_i(\betaa^*) f_i(\wit)=0.\]
But we also have $F'(\alpha)=G'(1)$ and so $F'(\alpha)=0$.
On the other hand,
\[F'(0)=e-\sumi{n}\pow_i(\betaa) f_i(\wit)\neq 0.\]
Setting $\tau_4\defeq a$ and $D_4$ to be the function that computes $F'$ given $x,\tau_4$, we
have that $(D_4,x,\tau_4)$ is a degree $\log n$ relation that \advprime can output in this case.
Setting $\ztafuncs=\set{D_1,D_2,D_3,D_4}$ we have proven knowledge soundness under the theorem assumptions.
\end{proof}

\subsection{Representative protostar-relations}\label{subsec:reprelation}
\begin{dfn}\label{dfn:represent-relation}
Given a relation \relzer we say a protostar-relation $\rel = \rel_{f,\predinst,\cm}$ \emph{represents} \relzer
if there are efficiently computable and invertible maps $\varphi_0, \varphi_1$ such that
\begin{enumerate}
 \item $\varphi_0(\inst)$ is always of the form $(\inst,X)$ for some $X$.
 \item Any efficient \adv has a \negl probability of outputting a pair $(\inst,\wit)$ such that either:
\begin{enumerate}
 \item $(\inst,\wit)\in \relzer$ but $(\varphi_0(\inst),\varphi_1(\wit))\notin \rel$.
 \item $(\inst,\wit)\in \rel$ but $(\varphi^{-1}_0(\inst),\varphi^{-1}_1(\wit))\notin \relzer$.
\end{enumerate}
\end{enumerate}

\end{dfn}
We define the \emph{size} of the protostar relation $R_{f,\predinst,\cm}$ as $\M+n$.
\begin{claim}\label{clm:repplonk}
Assuming ZTA for a constant size family there is a protostar-relation $\rel_{f,\predinst,cm}$ representing \relapp of size $O(N+\n)$.
\end{claim}

% \section{On protogalaxy}
% \subsection{Introspective constraints}
% Constraints $f_i$ on \wit, simply low degree polynomials, but have the ability to refer to
% components of $\cm(m_j)$
% Function $F$ should have ``introspection'' ability to look at commitments.
%
% commitment function will output two representations of $\cm(w)$ - in \G and in \F and
%
% or PI will include \F representation. which will then be part of $w$. \V will check representations match.
\section{Adversaries supporting recursive extraction}\label{sec:recursive}
Following \cite{novarecursive}, we define a model of ``recursive extraction'' for our analysis in Section \ref{sec:FtoFprime}. We assume our commitment function $\cm:\F^\M\to K$ is surjective.
We assume the existence of an efficiently computable injective representation function $R:K\to \F^{\dimK}$. Whenever an adversary \adv outputs $a\in K$ we assume it is represented as $R(a)$.
When analyzing knowledge soundness of our zk-SNARK in the next section, we put the following limitation on \adv. Say \adv outputs a vector
$v$ over \F. If there is an index $i$ such that $(v_i,\ldots,v_{i+\dimK-1})=R(a)$ for some $a\in K$, then \adv must also output $\omega\in \F^\M$ such that $\cm(\omega)=a$. The same requirement of outputting a \cm preimage for substrings in $K$ then holds for $\omega$ and all other outputs of \adv. In other words, \adv
must continue outputting more vectors ``explaining'' elements of $K$, until the explanation vectors do not contain any elements of $K$ as substrings.  
We call such \adv a \emph{recursive algebraic adversary with respect to $\cm$}. We always work with \cm and $R$ such that only a \negl fraction of elements of $F^{\dimK}$ are in $R(K)$. This is to get a \negl probability that a random vector  of  \poly size  has a substring that is an element of $K$ - and thus avoid situations where \adv is forced to ``explain'' elements of $K$ that he didn't purposefully write.


This assumption is motivated by a ``recursive'' interpretation of the Algebraic Group Model\cite{agm} as done in \cite{novarecursive}.
For illustration, consider first the case where $\cm:\F^\n\to\G$ is defined as $\cm(\wit)=\innerprod{\wit}{V}$ for a fixed vector $V\in \G^\n$ derived in a setup procedure. I.e. \cm is a Pedersen commitment in this case.
In this case, the AGM forces \adv when outputting $a\in \G$ to also output $\wit$ such that $\innerprod{\wit}{V}=\cm(\wit)=a$. \cite{novarecursive} now raise the idea that if a prespecified subset of indices of \wit is a valid representation of $b\in \G$, it is reasonable to demand of an algebraic \adv to also output $\wit_2$ with $\innerprod{\wit_2}{V}=b$.\\


Our concrete choice for \cm when using \protogal, is of the following form.\footnote{\cm is of this form because it is derived from an interactive protocol where the prover messages are in committed form, but verifier challenges are in the clear. See \cite{protostar,protogalaxy} for more details.} We have a setup procedure outputting a vector of group elements $V\in \G^\n$ as output.
We have some fixed partition of our input $\wit \in \F^\M$ into continuous segments of size either one or \n. To get $\cm(\wit)$ we operate segment-wise.
If the segment $\wit_i$ is of size one we simply append $\wit_i$ to the output. If a segment $s=(\wit_i,\ldots,\wit_{i+\n-1})$ is of size \n we append $\innerprod{s}{V}$ to the output.
In particular the output $\cm(\wit)$ is a mixture of \F and \G elements, and accordingly the space $K$ is a direct sum of spaces $\mathbb{V}_i\in \set{\F,\G}$. It follows that an algebraic adversary outputting $c\in K$ must output \wit with $\cm(\wit)=c$ as the AGM forces it to send an opening $s\in \F^\n$ to each $a\in \G$.



\newcommand{\instrcg}{\ensuremath{\mathscr{x}}\xspace}
\newcommand{\witrcg}{\ensuremath{\mathscr{w}}\xspace}
\newcommand{\empt}{\calligmath{empty}}

\newcommand{\acc}{\ensuremath{\mathsf{acc}}\xspace}
\newcommand{\accprev}{\ensuremath{\mathsf{acc}_{0}}\xspace}%\calligmath{prev}}}\xspace}
\renewcommand{\inst}{\ensuremath{\mathsf{inst}}\xspace}
\renewcommand{\instt}{\ensuremath{\mathsf{acc}}\xspace}
\renewcommand{\insttbase}{\ensuremath{\mathsf{acc_{0}}}\xspace}
\newcommand{\witacc}{\ensuremath{\mathbf{w\mhyphen}\mathsf{acc}}\xspace}
\newcommand{\witinst}{\ensuremath{\boldsymbol{w}\mhyphen \mathsf{inst}}\xspace}
\newcommand{\relfin}{\ensuremath{\rel_{\mathsf{fin}}}\xspace}
\newcommand{\instfin}{\ensuremath{\shlomomath{x}}}%_{\mathsf{fin}}}\xspace}
\newcommand{\witfin}{\ensuremath{\shlomomath{w}}}%_{\mathsf{fin}}}\xspace}
\newcommand{\emptyacc}{\ensuremath{\acc_{\text{\calligra{empty}}}}\xspace}
% \newcommand{\verpg}{\ensuremath{\ver_{\cm,n}}\xspace}
\newcommand{\prvpg}{\ensuremath{\prv^{\mathrm{PG}}_{\cm,n,f}}\xspace}
\newcommand{\prvsnark}{\ensuremath{\prv_{\mathsf{fin}}}\xspace} %{\calligra{fin}}}}\xspace}
\newcommand{\versnark}{\ensuremath{\ver_{\mathsf{fin}}}\xspace}%text{\calligra{fin}}}}\xspace}
% \newcommand{\prvsnark}{\ensuremath{\prv_{\text{\calligra{fin}}}}\xspace}
% \newcommand{\versnark}{\ensuremath{\ver_{\text{\calligra{fin}}}}\xspace}
\newcommand{\prffin}{\ensuremath{\pi_{\mathsf{fin}}}\xspace}
\newcommand{\prvexec}{\ensuremath{\prv_{\mathrm{exec}}}\xspace}
\newcommand{\verexec}{\ensuremath{\ver_{\mathrm{exec}}}\xspace}
\newcommand{\extexec}{\ensuremath{\ext_{\mathrm{exec}}}\xspace}



\section{The main construction}\label{sec:FtoFprime}
We say an RCG relation \relrcg is \emph{trivial} if the $S$ variable is not used in $F$, and accordingly \finpred depends only on $(\zfin,\recset)$.
We assume in this section \relrcg is trivial, thinking of it as \relrcgstar from Section \ref{sec:Fstar}.

\subsection{The extended function $F'$}
As in \cite{nova,othernova}, we first describe an extended function $F'$ that executes the folding verifier in addition to an iteration of $F$. Loosely speaking, extending $F$ into $F'$ is what enables bootstrapping a folding scheme into an IVC or RCG. We describe the function arguments first.\\

\noindent
$\instFprime=(z,\cnt,\acchash)$
\begin{itemize}
 \item $z$ -- output for $F$
\item $\cnt$ -- counter of IVC step
\item $\acchash$ -- hash of accumulator
\end{itemize}
$\witFprime=(\instt,\insttbase,\instFprime_0,w,\prf)$
\begin{itemize}
\item$\instt$ -- current accumulator instance
\item$\insttbase$ -- previous accumulator instance
\item$\instFprime_0$ -- instance (of $F'$) to be accumulated
\item$w$ -- private input for $F$
\item$\prf$ -- proof for \protogal verifier
\end{itemize}

We fix $\predinst,\cm,\varphi_0,\varphi_1$ to be the values appearing in the statement of Claim \ref{clm:repplonk}.


\noindent
$F'(\instFprime,\witFprime)=\accept$ if and only if:
\begin{enumerate}
    \item $F(\instFprime_0.z, w,z)=\accept$.
    \item If $\cnt=1$:
    \begin{itemize}
        \item $\instFprime_0.z.\init=\true$.
    \end{itemize}
    \item If $\cnt>1$:
    \begin{enumerate}
        \item $\hash(\instt)=\acchash$.
        \item $\hash(\insttbase)=\instFprime_0.\acchash$.
        \item $\instFprime_0.\cnt=\cnt-1$.
        \item $\verpg(\insttbase,\varphi_0(\instFprime_0),\instt,\prf)=\accept$.
    \end{enumerate}
\end{enumerate}
Let $\relzer$ be the set of pairs $(\instFprime,\witFprime)$ with $F'(\instFprime,\witFprime)=\accept$.
Let $\rel$ be a protostar-relation representing \relzer as defined in Section \ref{subsec:reprelation}.

\subsection{Commitment-consistent SNARKs}
It will be convenient to assume a zk-SNARK where the proof contains a commitment to the witness. All SNARK construction we are aware of  (e.g. \cite{plonk}) have this property. 

\begin{dfn}\label{dfn:cmsnark}
Fix a relation \rel. Fix a linear function $\cm:\F\to K$. A \emph{$\cm$-consistent  zk-SNARK for \rel} is a tuple of efficient algorithms $(\prv,\ver,\sim)$ such that  $\ver(\inst,\prf)=\accept$ implies  $\prf=(\prf_1,\prf_2)$ with $\prf_1\in K$.
And additionally,
\begin{itemize}
 \item \textbf{Completeness:} Suppose $(\inst,\wit)\in \rel$. Let $\prf=\prv(\inst,\wit)$. Then with probability $1-\negl$, $\ver(\inst,\prf)=\accept$.
 \item \textbf{Knowledge Soundness given extractable commitments:}
 The probability of any efficient \adv outputting $\inst,\prf=(\prf_1,\prf_2),\wit$ such that
 \begin{enumerate}
  \item $\ver(\inst,\prf)=\accept$,
  \item $\cm(\wit)=\prf_1$,
  \item $(\inst,\wit)\notin \rel$, 
 \end{enumerate}
is \negl.
 \item \textbf{Zero-Knowledge:} Fix any $(\inst,\wit)\in \rel$. $\sim(\inst,\cmsetup)$ outputs a distribution \negl-close to $\prv(\inst,\wit)$.
\end{itemize}
\end{dfn}

For readability, from now on we denote an accumulator by \acc, accumulator witness by \witacc, instance by \inst, and instance witness by \witinst.

\subsection{The relation \relfin}
We define the relation \relfin of pairs $(\instfin,\witfin)$ with
\begin{itemize}
 \item $\instfin = (\acc,\zfin,C,\recset)$
 \item $\witfin = (\witacc,\accprev,\inst,\prf)$
\end{itemize}
such that
\begin{enumerate}
 \item $(\acc,\witacc)\in\relrand$.
\item $\verpg(\accprev,\inst,\acc,\prf)=\accept$.
\item $\inst.z=\zfin$.
\item $\inst.\cnt\leq C$.
\item $\inst.\acchash = \hash(\accprev)$.
\end{enumerate}

\noindent
Let $(\prvsnark,\versnark)$ be a $\cm$-consistent zk-SNARK for \relfin.



\subsection{Main construction}\label{subsec:main}
We now describe the full prover and verifier for a given trivial RCG relation \relrcg.
Later we review how to use this to get a zk-SNARK for the relation \relexec of valid executions, given the reductions of the previous sections. \\ \\
\noindent
\underline{$\prv(\inpF,\witF)$:}
\begin{enumerate}
 \item Let
$\inpF =(\zfin,C,\recset),\witF=(n,(z_0,\ldots,z_n),(w_1,\ldots,w_n))$. Recall that $(\inpF,\witF)\in \relrcg$ implies $F(z_{i-1},w_i,z_i)=\accept$ for each $i\in [n]$, $z_0.\init =\true$, $z_n=\zfin$, $n\le C$ and $\finpred(\zfin,\recset) = \accept$.
% \item For $i\in [n]$, let


\item Choose instance $\inst_0=(z_0,\cnt_0,\acchash_0)$ for arbitrary values $\cnt_0,\acchash_0$. Choose $\acc_0$ arbitrarily.
Let $\inst_1=(z_1,1,\acchash_1)$, $\witinst_1=(\acc_0,\acc_0, \inst_0, w_1, \prf_0)$ for arbitrary values $\acchash_1,\acc_0,\prf_0$. (We can choose some values arbitrarily as they aren't constrained in $F'$ when $\cnt=1$.)

\item Let $\acc_1$ be a randomly chosen satisfiable accumulator. Namely, $\acc_1=(\cm(\witacc_1),\betaa,e)$ where $\witacc_1$ and $\betaa$ are chosen randomly\footnote{We only need $\cm(\witacc_1)$ to be uniformly distributed over the image of \cm. According to \cm's structure, it may suffice to choose only a small subset of $\witacc_1$'s coordinates randomly, and set the rest to zero.}, and $e$ is set to $e=\sum_{i\in [n]}\pow_i(\betaa)f_i(\witacc_1)$.

\item For each $2\leq i\leq n$, compute
\begin{enumerate}
 \item $(\acc_i,\witacc_i,\prf_i) = \prvpg(\acc_{i-1},\witacc_{i-1},\varphi_0(\inst_{i-1}),\varphi_1(\witinst_{i-1}))$
\item $\inst_i = (z_i,i,\hash(\acc_i))$,
\item $\witinst_i=(\acc_i,\acc_{i-1},\inst_{i-1},w_{i},\prf_i)$
\end{enumerate}
\item
$(\acc,\witacc,\prf^*) = \prvpg(\acc_{n},\witacc_{n},\varphi_0(\inst_{n}),\varphi_1(\witinst_{n}))$.
\item Let $\prffin = \prvsnark(\instfin,\witfin)$ where
\begin{itemize}
 \item $\instfin = (\acc,\zfin,C,\recset)$
 \item $\witfin = (\witacc,\acc_n,\varphi_0(\inst_n),\prf^*)$
\end{itemize}
\item Output $\prf=(\acc,\prffin)$.\\
\end{enumerate}

\noindent
\underline{$\ver(\inpF,\prf)$:}
\begin{enumerate}
 \item Parse \inpF as $(\zfin,C,\recset)$, $\prf$ as $(\acc,\prffin)$.
 \item If $\finpred(\zfin,\recset)=\rej$ output \rej.
 \item Let $\instfin\defeq (\acc,\zfin,C,\recset)$.
 \item Return $\versnark(\instfin,\prffin)$.
\end{enumerate}

\begin{thm}\label{thm:main}
Let \relrcg be a trivial RCG relation. Assume that \hash is collision resistant, and that the assumptions in Theorem \ref{thm:pgsoundness} hold. Then
 $(\prv,\ver)$ is a space-efficient zk-SNARK for \relrcg.
\end{thm}
\begin{proof}
 The main thing to prove is knowledge soundness. Let \adv be a recursive algebraic adversary.

We define the following extractor algorithm \ext:
\begin{enumerate}
 \item Given $(\instrcg,\prffin)$, if $\prffin$ is not of the form $(\prf_1,\prf_2)$ with $\prf_1\in K$ output \empt and abort. Otherwise let $\witfin$ be the element output by \adv such that $\cm(\witfin)=\prf_1$.
 \item Parse $\witfin$ as $\witfin=(\witacc,\acc^*,\inst^*,\prf^*)$ where the different elements have the appropriate length in a witness for \relfin. If such parsing fails output \empt and abort.
 \item Let $n\defeq \inst^*.\cnt$. Denote $\acc_n\defeq \acc^*, \inst_n \defeq \inst^*$.
 \item If $(\instfin,\witfin)\notin \relfin$, output \empt and abort. Otherwise, $\verpg(\acc_n,\inst_n,\acc,\prf^*)=\accept$, and thus $\acc_n,\inst_n\in K$. Let $\witacc_n,\witinst_n$ be the elements output by \adv such that $\cm(\witacc_n)=\acc_n$ and $\cm(\witinst_n)=\inst_n$.
 \item For $i=n-1,\ldots,1$:
 \begin{enumerate}
  \item If $(\inst_{i+1},\witinst_{i+1})\notin \rel$, output \empt and abort. Otherwise, as $(\inst_{i+1},\witinst_{i+1})\in \rel$ implies $\acc_{i},\inst_{i}\in K$, let $\witacc_{i},\witinst_{i}$ be the elements output by \adv such that $\acc_i= \cm(\witacc_{i}),\inst_i=\cm(\witinst_i)$.
  \item Parse $\varphi_0^{-1}(\inst_i)$ as $(z_i,\cnt_i,\acchash_i)$. Parse $\varphi_1^{-1}(\witinst_i)$ as $(\acc'_i,\acc_{i-1},\inst_{i-1},w_i,\prf_i)$. Note that through this parsing we have in particular defined $z_i,w_i$ and $\inst_{i-1}$.
 \end{enumerate}
 \item Define $z_0\defeq \inst_0.z$.
\item Output $\witrcg\defeq ( n,(z_0,\ldots,z_n),(w_1,\ldots,w_n))$.
\end{enumerate}

Let $D$ be the event that \adv outputs $(\instrcg,\prf)$ such that $\ver(\instrcg,\prf)=\accept$.
If $D$ has probability \negl we are done. Otherwise, in order to prove knowledge soundness, we need to show that
\[\Pr[(\instrcg,\witrcg)\notin \relrcg \mid D]=\negl.\]
Assume from now we are in the space conditioned on $D$.
Let $E_0$ be the event $(\instfin,\witfin)\notin \relfin$.
For $i\in [n]$, let $E_i$ be the union of the following events:
\begin{enumerate}
 \item $(\inst_i,\witinst_i)\notin \rel$.
\item $(\acc_i,\witacc_i) \notin \relrand$.
\item $\hash(\acc_i)\neq \inst_i.\acchash$.
\end{enumerate}
% \item $D_i:\acc'_i\neq \acc_i$.

We first argue that if $E_0,\ldots, E_n$ \emph{don't} occur, $(\instrcg,\witrcg)\in \relrcg$.
Denote $\instrcg = (\zfin,C,\recset)$ and $\instfin=(\acc,\instrcg)$.
Examining the definition of $\relrcg$, the statement $(\instrcg,\witrcg)\in \relrcg$ is equivalent to the following conditions.
\begin{enumerate}
\item $\finpred(\zfin,\recset)=\accept$: \ver checks this directly so we know it holds.
\item $\inst_n.z = \zfin$ and $n \leq C$: Follows from $(\instfin,\witfin)\in \relfin$.
\item For all $i\in [n]$, $F(z_{i-1},w_i,z_i)=\accept$: Follows directly from $(\inst_i,\witinst_i)\in \rel$ for each $i\in [n]$.
 \item $z_0.\init = \true$:
For this we first prove by backwards induction on $i=n,{n-1},\ldots,1$ that $\inst_i.\cnt =i$.
By our definition of $\inst_n$ this holds for $i=n$. For the induction step, assume it holds for $i$.
Since $(\inst_i,\witinst_i)\in \rel$ we have $\inst_{i-1}.\cnt = \witinst_{i-1}.\inst.\cnt = \inst_i.\cnt -1 =i-1$.

In particular, $\inst_1.\cnt=1$ which implies when $(\inst_1,\witinst_1)\in \rel$ that $z_0.\init = \inst_0.z.\init=\true$.
\end{enumerate}

It is left to show that the probability of $E_0\cup E_1 \cup \ldots \cup E_n$ is \negl. From the knowledge soundness of the zk-SNARK for \relfin
we have $\Pr[E_0]=\negl$. (Recall we are in the event $D$ and assuming its probability is non-negligible.)

For this purpose, we prove by backwards induction on $i$, for each $i\in [n]$, that
the probability that $E_i$ occurs given $E_0,E_{i+1},\ldots,E_n$ \emph{didn't} is \negl.


For $i=n$, assume $E_0$ didn't occur, hence $(\instfin,\witfin)\in \relfin$.
% from the knowledge soudness of $(\prvsnark,\versnark)$ e.w.p. \negl $(\instfin,\witfin)\in \relfin$.
In this case $(\acc,\witacc)\in \relrand$, $\hash(\acc_n)=\inst_n.\acchash$ and $\verpg(\acc_n,\inst_n,\acc,\prf^*)=\accept$.
Define $\adv_n$ to be the algorithm that executes \ext and outputs $\acc_n,\inst_n,\acc,\witacc_n,\witinst_n,\witacc,\prf^*$.
From the knowledge soundness of \protogal applied to $\adv_n$ we have that the probability conditioned on $\neg E_0$ that
$E_n$ occurred is \negl.

Now assume the induction hypothesis for some $i>1$. We have by the hypothesis that the event $D_i\defeq \neg(E_0\cup E_i\cup\ldots\cup E_n)$ has probability $1-\negl$. Assume that we are in $D_i$.
 From $\neg E_i$ we have $\inst_{i}.\acchash=\hash(\acc_i)$. From $(\inst_{i},\witinst_{i})\in \rel$ we have that $\inst_{i}.\acchash = \hash(\acc'_{i})$.
Thus $\hash(\acc_i)=\hash(\acc'_i)$.
From the collision resistance of \hash, we thus have that the probability that $\acc_i\neq \acc'_i$ is \negl.
If $\acc_i=\acc'_i$ we have from $(\inst_i,\witinst_i)\in \rel$ that $\ver(\acc_{i-1},\inst_{i-1},\acc_i,\prf_i) =\accept$.
Define $\adv_i$ to be the algorithm that executes \ext and outputs $\acc_{i-1},\inst_{i-1},\acc_{i},\witacc_{i-1},$ $\witinst_{i-1},\witacc_i,\prf_i$.
From the knowledge soundness of \protogal applied to $\adv_i$, we have that the probability that $(\inst_{i-1},\witinst_{i-1})\notin \rel$ or $(\acc_{i-1},\witacc_{i-1})\notin \relrand$ given $D_i$ is \negl. Noting that $(\inst_i,\witinst_i)\in \rel$ also implies $\hash(\acc_{i-1}) = \inst_{i-1}.\acchash$, $\Pr[E_{i-1} \mid D_i]=\negl$; which is the desired inductive statement.
\end{proof}



\subsection{Constructing proofs for \relexec}
Going through the reductions of the previous sections, we get the following zk-SNARK for the relation \relexec from Section \ref{sec:validexec} describing valid executions.\\ \\
\noindent
\underline{$\prvexec(\instexec,\witexec)$:}
\begin{enumerate}
\item Let $\instexec=(\root,C,\recset),\zfin=(\empty,\root,\false)$ and $\instrcg=(\zfin,C,\recset)$.
Let $\varphi$ be the map in Lemma \ref{lem:execasRCG}, and compute $\witrcg=\varphi(\witexec)$.
\item Let $\witrcg = (n,(z_0,\ldots,z_n),(w_1,\ldots,w_n),(s_1,\ldots,s_n))$.
    \begin{enumerate}
    \item For each $i\in [n]$, define  $m_i\in \F^k$ such that $m_{i,j}$ is the number of times a record is read when $s_{i,j}$ is an \add operation, and 0 otherwise.
    \item Set $\inchash_0=\emptyset$ and compute $\inchash_i=\hash(\inchash_{i-1},\cm(s_i,m_i))$ for $i \in [n]$.
    \item Compute
$(\alpha,\beta,\eps) = (\hash(\inchash_n,\recset,1),\hash(\inchash_n,\recset,2),\hash(\inchash_n,\recset,3))$.
    \item Set $\incsum_0=0$ and compute $\incsum_i$ for $i \in [n]$ as in the definition of $F^*$ in Section \ref{sec:Fstar}.
    \item Let $\zfin^*=(\zfin,\inchash_n,\incsum_n,\alpha,\beta,\eps)$, for $0 \le i \le n$, let $z_i^*=(z_i,\inchash_i,\incsum_i,\alpha,\beta,\eps)$, and for $i \in [n]$, let $w_i^*=(w_i,s_i,m_i)$.
    \item Set $\instrcg^*=(\zfin^*,C,\recset)$ and $\witrcg^*=(n,(z_0^*,\ldots,z_n^*),(w_1^*,\ldots,w_n^*))$.
    \end{enumerate}
\item Compute the proof $\prf^*$ for $(\instrcg^*,\witrcg^*)\in \relrcgstar$ according to \prv in Section \ref{subsec:main}.
\item Output $\prf=(\inchash_n,\incsum_n,\alpha,\beta,\eps,\prf^*)$.
\end{enumerate}

\noindent
\underline{$\verexec(\instexec,\prf)$:}
\begin{enumerate}
\item Parse $\instexec$ as $(\root,C,\recset)$ and $\prf$ as $(\inchash,\incsum,\alpha,\beta,\eps,\prf^*)$. Let $\zfin=(\empty,\root,\false)$, $\zfin^*=(\zfin,\inchash,\incsum,\alpha,\beta,\eps)$ and $\instrcg^*=(\zfin^*,C,\recset)$.
\item Return $\ver(\instrcg^*,\prf^*)$ according to \ver in Section \ref{subsec:main}.
\end{enumerate}

\begin{thm}
If $(\prv,\ver)$ from Section \ref{subsec:main} is knowledge-sound for \relrcgstar and the necessary assumptions from Lemma \ref{lem:FtoFstar} hold, $(\prvexec,\verexec)$ is knowledge-sound for \relexec.
\end{thm}
\begin{proof}
Let \adv be a recursive algebraic adversary that outputs $\instexec=(\root,C,\recset)$ and $\prf=(\inchash,\incsum,\alpha,\beta,\eps,\prf^*)$. Let $\zfin=(\empty,\root,\false)$, $\zfin^*=(\zfin,\inchash,\incsum,\alpha,\beta,\eps)$, and $\instrcg^*=(\zfin^*,C,\recset)$. Define $\adv^*$ as the adversary that runs \adv but outputs $(\instrcg^*,\prf^*)$. Define the following extractor \extexec:
\begin{enumerate}
    \item Given $(\instexec,\prf)$, use \ext from Section \ref{subsec:main} to extract $\witrcg^*$ from the adversary $\adv^*$.
    \item Compute $(\instrcg,\witrcg)=\varphi^*(\instrcg^*,\witrcg^*)$, where $\varphi^*$ is the map from Lemma \ref{lem:FtoFstar}.
    \item Output $\witexec=\varphi^{-1}(\witrcg)$, where $\varphi$ is the map from Lemma \ref{lem:execasRCG}.
\end{enumerate}
We need to show that
\[\Pr[\verexec(\instexec,\prf)=\accept \land (\instexec,\witexec)\notin\relexec]=\negl.\]

If the first event in the above expression has negligible probability, we are done.

Otherwise, assuming we are in the first event, i.e., \verexec accepts, we show the second event has negligible probability. In particular, this means $\ver(\instrcg^*,\prf^*)=\accept$.

From the knowledge soundness of $(\prv,\ver)$ for \relrcgstar, we get that the witness $\witrcg^*$ output by \ext satisfies $(\instrcg^*,\witrcg^*)\in\relrcgstar$ e.w.p. \negl.

From Lemma \ref{lem:FtoFstar}, we get $(\instrcg,\witrcg)\in\relrcg$ e.w.p. \negl.

From Lemma \ref{lem:execasRCG}, we get $(\instexec,\witexec)\in\relexec$ e.w.p. \negl, finishing the proof.
\end{proof}



\section{General Final predicate}\label{sec:general}
\renewcommand{\s}{\incsum}
We sketch how to deal with a \emph{general} final predicate \finpred, rather than the one described so far for checking record operations. A more detailed explanation will appear in an updated version of the paper.

The basic idea is that a general final predicate reduces to the concatenation predicate.
Namely, suppose we can prove an element $\s$ is the commitment to the concatenation of the \set{s_i} from all $n$ iterations.
Then we can modify the final zk-SNARK in Section \ref{sec:FtoFprime} to also check that $\finpred(\zfin, s_1,\ldots,s_n,\recset)=\accept$.

For this purpose, instead of the function $F^*$ in Section \ref{sec:Fstar} we add \protogal constraints to the transition function $F$ to obtain at iteration $i$ a vector $S_i$ that is the concatenation of $S_{i-1}$ with $s_i$.

\subsection{Efficient Proofs of Concatenation with \protogal}
% WIP
% TODO not sure if variable names conflict, check
Given a sequence consisting of vectors \sett{s_i}{i\in [n]} of field elements of length $k$ and a bound $C$ on $n$, we can define a system of linear protogalaxy constraints that a concatenation was correctly carried out.
We highlight that it is important the constraint system does not depend on the current iteration $i$, or actual sequence length $n$, only on the bound $C$.
The idea is that if we append the new elements \emph{at the beginning} of the vector, the concatenation constraints can be written as linear constraints that indeed only depend on $k,C$ but not $i$ or $n$.

Fix vector $b\in \F^k$ and vectors $a,a'\in \F^{kC}$.
For each $j\in [kC]$ we define the constraint $f_j(a,b,a')$ as follows.
\begin{equation*}
f_j(a, b, a') \defeq \begin{cases}
    a'_j - b_j & i \leq k \\
    a'_j - a_{j - k} & j > k
\end{cases}.
\end{equation*}
In words, the constraints \set{f_j} enforce that $a'$ consists of the $k$ elements of $b$ followed by the first $(C-1)k$ elements
of $a$.
Additionally, we will constrain (using the \init variable) that $S_0$ is the zero vector of length $kC$.
In the $i$-th iteration, our transition function $F$ will check for each $j\in [kC]$ the constraint $f_j(S_i,s_i,S_{i+1})=0$.

One can now show inductively that when starting from the zero vector, under the assumptions that $n\leq C$ and $|s_i|\leq k$ for each $i\in [n]$, we end up with $S_n=(s_1\|\ldots\|s_n)$ possibly padded with zeroes.

% Now we wish to append $b\in \F^k$ to $S_i$; that is, to construct $S_{i+1} = b \| S_i$.
%
% it is sufficient to check for all $j \in [k C]$ that $f_j(S_i,b,S_{i+1})=0$ where
%
% These constraints clearly encode the concatenation relation.
\paragraph{Prover efficiency}
If the stack is folded in order, then even in the new randomized instance, the zero padding is preserved.
That is, higher order elements above $ ki$ are still zero after folding.
So the prover only needs to perform one field multiplication per stack element to compute the folded witness.
These constraints are also linear so they do not contribute to any of the error terms in the $G(X)$ polynomial.

For all $j > k (i+1)$ notice that $f_j(S_i, s_i, S_{i+1}) = 0$ identically, so they do not even contribute to the cost of computing the $F(X)$ polynomial.
Assuming all of these constraints are organized adjacently in the highest order indices of the overall protogalaxy constraint system, there is a straightforward modification of the $F(X)$ computation which incurs no cost for constraints that are identically zero.
In brief, if an entire subtree consists of leaves that are zero, then the prover can avoid any computation for that subtree.
Therefore, the total prover computation depends only on the size of the vector $S_{i+1}$.


% TODO is it outside the scope of the section to discuss how commitments to the vectors work?
% like the vector a should be the a' of the previous folding and we should copy the commitments
% then checking depends only on the instance.


% \subsection{RCG and Goblin \plonk}
% The ``Global'' in RCG suggests a final predicate checking conditions \emph{between} the different $s_i$. However, as suggested in \cite{goblin}, it might 
\section*{Acknowledgements}
The third author was funded by the Vienna Science and Technology Fund (WWTF) [10.47379/VRG18002] and by the Austrian Science Fund (FWF) [10.55776/F8515-N].

\bibliographystyle{alpha}
\bibliography{references}
\end{document}