risc0-security-analysis-UDR.ipynb

{
 "cells": [
  {
   "attachments": {},
   "cell_type": "markdown",
   "id": "989e89cd-6c96-4ceb-8508-44e9abb478a8",
   "metadata": {},
   "source": [
    "# RISC Zero Soundness Analysis - Unique Decoding Regime\n",
    "(Originally written by the team at Ulvetanna; this version is an in-process translation of that work to the unique decoding regime.)\n",
    "\n",
    "The goal is to concretely compute the overall error estimate $\\varepsilon_{\\text{IOP}}$ from the [[RISC Zero](https://www.risczero.com/proof-system-in-detail.pdf)] spec. \n",
    "\n",
    "Let's begin by defining some global constants, which depend only on the proof system. These are all taken directly from the spec, with the exception of `h` and `L`, which we obtained by inspecting [the open-source code](https://github.com/risc0/risc0)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 103,
   "id": "8560da35-9398-4050-9370-b50163cc0030",
   "metadata": {},
   "outputs": [],
   "source": [
    "import math\n",
    "\n",
    "k = 2  # negative log of the rate.\n",
    "rho = 1 / (1 << k)  # rate.\n",
    "h = 20  # log of the trace length. this value refers to the default segment size. \n",
    "H = 1 << h  # domain size.\n",
    "D = H / rho  # domain size, after low-degree extension.\n",
    "e = 4  # field extension degree.\n",
    "p = (1 << 32) - (1 << 27) + 1  # field characteristic: Baby Bear prime.\n",
    "F = math.pow(p, e)  # extension field size.\n",
    "C = 16 + 222 + 36  # number of control, data, and accumulation columns, respectively. retrieved from `circuit.get_taps()`, etc.\n",
    "L = C + 4  # number of polynomials which ultimately appear in the FRI batch. we need to add 4 extra columns, for the \"segment polynomials\".\n",
    "s = 150  # number of FRI queries."
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "id": "5bfad65b-f562-40b3-9ec3-91111ac2c4bc",
   "metadata": {},
   "source": [
    "TODO - update this section for UDR \n",
    "The parameter `m` below is the \"Johnson parameter\"; see [[Haböck](https://eprint.iacr.org/2022/1216.pdf)]. This one is subtle, since it doesn't appear directly in the protocol at all; rather, it only appears in the soundness estimates. We have chosen it to here _optimize_ the number of bits of provable security achieved. We comment on this further below."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 104,
   "id": "ee27ec72-0457-4276-b8c2-8997bbf70ba4",
   "metadata": {},
   "outputs": [],
   "source": [
    "m = 16 # TODO update for UDR... do m and m+ both disappear entirely? \n",
    "# i think there will still be some notion of rho+...\n",
    "alpha = 1 - (1 - rho) / 2 # TODO factcheck whether the \"1 - \" is correct here\n",
    "theta = 1 - alpha"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "id": "4057a312-4b94-4335-ac37-957dd4e60a9a",
   "metadata": {},
   "source": [
    "### Provable Soundness\n",
    "\n",
    "The below error terms reflect the _proven_ / known soundness, and derive from Theorem 1.2 of [[Proximity Gaps](https://eprint.iacr.org/2020/654.pdf)]. The below expressions are based on [[Haböck](https://eprint.iacr.org/2022/1216.pdf)] and [[RISC Zero](https://www.risczero.com/proof-system-in-detail.pdf)], which are in agreement.\n",
    "\n",
    "The assertion that e_FRI_constant = (L + 1) * e_proximity_gap is based on the analysis [here](https://hackmd.io/-GVDIdGOT-yiQgFjZA-Ayw)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 105,
   "id": "6c8f38de-8b73-4ea9-9899-b799f3bbec80",
   "metadata": {},
   "outputs": [],
   "source": [
    "e_proximity_gap = D / F\n",
    "e_FRI_constant = (L + 1) * e_proximity_gap \n",
    "e_FRI_queries = math.pow(1 - theta, s)\n",
    "e_FRI = e_FRI_constant + e_FRI_queries"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "id": "0f79c02b-97ab-4c30-932a-fb79c566dbc6",
   "metadata": {},
   "source": [
    "TODO -- revise this note for unique decoding radius\n",
    "\n",
    "There's a further subtlety. In order for the proof of [[Haböck](https://eprint.iacr.org/2022/1216.pdf), Theorem 8] to go through, we need to apply FRI with proximity parameter $\\theta < 1 - \\sqrt{\\rho^+}$ (note the +!). In particular, we can't choose `m` _too_ large, or else $\\theta := 1 - \\sqrt{\\rho} \\cdot \\left( 1 + \\frac{1}{2 \\cdot m} \\right)$ will become larger than $\\frac{1 - \\rho}{2}$, and the key step in that theorem will fail. Specifically, the relevant _configuration's_ distance from Reed–Solomon code $\\mathsf{RS}_{k^+}(K, D)$ over the function field $K := F(Z)$ will exceed the Johnson bound of that code. For our parameters, this doesn't happen until `m = 131073`, so we have plenty of room.\n",
    "\n",
    "Separately, when we calculate $L^+$, we need to use a _different_ `m` than the one up above. Specifically, we need to use $m^+$, say, where $m^+$ is chosen sufficiently large that $\\theta \\leq 1 - \\sqrt{\\rho^+} \\cdot \\left( 1 + \\frac{1}{2 \\cdot m^+} \\right)$ holds. This fact is not explicit in [[Haböck](https://eprint.iacr.org/2022/1216.pdf), Theorem 8], and appears to have been an oversight.\n",
    "\n",
    "Let's calculate a minimal suitable $m^+$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 106,
   "id": "e78cd879-d6ed-45be-9456-f85169e63531",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "3"
      ]
     },
     "execution_count": 106,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "rho_plus = (H + 2) / D  # modified rate of \"extension code\" in function field; controls the agreement we actually need\n",
    "# todo adjust this assertion for unique decoding radius\n",
    "assert theta < 1 - math.sqrt(rho_plus)  # make sure `m` isn't too large.\n",
    "m_plus = math.ceil(1 / (2 * (alpha / math.sqrt(rho_plus) - 1)))\n",
    "# todo adjust this assertion for unique decoding radius\n",
    "assert theta <= 1 - math.sqrt(rho_plus) * (1 + 1 / (2 * m_plus))\n",
    "m_plus"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 107,
   "id": "90d79d1c-c022-4362-81f7-adcb5c62c25c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "-99.28880159528796"
      ]
     },
     "execution_count": 107,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "L_plus = 1 # Since we restrict our analysis to the unique decoding radius, we set the list-size to be 1.\n",
    "\n",
    "e_ALI = L_plus * C / F\n",
    "e_DEEP = L_plus * (4 * (H + 1) + (H - 1)) / (F - H - D)\n",
    "e_PLONK = e * 5 * H / F  # 5 comes from n_{σ_{mem}} == 5.\n",
    "e_PLOOKUP = e * 15 * H / F  # n_{σ_{bytes}} == 15.\n",
    "\n",
    "e_IOP = e_FRI + e_ALI + e_DEEP + e_PLONK + e_PLOOKUP\n",
    "math.log(e_IOP, 2)"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "id": "4a1e1c41-3611-4911-a9c9-0a04b5ab58c5",
   "metadata": {},
   "source": [
    "Thus it seems that 150 queries is sufficient to reach ~100 bits of proven security, overall. \n",
    "\n",
    "The individual values are collected in the table below:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 108,
   "id": "7765dd3b-5aea-4a62-ac11-b4e80245d426",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Term</th>\n",
       "      <th>log_2(P[err])</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>e_FRI_constant</td>\n",
       "      <td>-99.692664</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>e_FRI_queries</td>\n",
       "      <td>-101.710786</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>e_ALI</td>\n",
       "      <td>-119.718753</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>e_DEEP</td>\n",
       "      <td>-107.494854</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>e_PLONK</td>\n",
       "      <td>-105.494857</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>e_PLOOKUP</td>\n",
       "      <td>-103.909895</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "             Term  log_2(P[err])\n",
       "0  e_FRI_constant     -99.692664\n",
       "1   e_FRI_queries    -101.710786\n",
       "2           e_ALI    -119.718753\n",
       "3          e_DEEP    -107.494854\n",
       "4         e_PLONK    -105.494857\n",
       "5       e_PLOOKUP    -103.909895"
      ]
     },
     "execution_count": 108,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import numpy as np\n",
    "import pandas as pd\n",
    "\n",
    "def show_table():\n",
    "    err_terms = pd.DataFrame(\n",
    "        [\n",
    "            [\"e_FRI_constant\", e_FRI_constant],\n",
    "            [\"e_FRI_queries\", e_FRI_queries],\n",
    "            [\"e_ALI\", e_ALI],\n",
    "            [\"e_DEEP\", e_DEEP],\n",
    "            [\"e_PLONK\", e_PLONK],\n",
    "            [\"e_PLOOKUP\", e_PLOOKUP],\n",
    "        ],\n",
    "        columns=[\"Term\", \"P[err]\"]\n",
    "    )\n",
    "    err_terms[\"log_2(P[err])\"] = np.log2(err_terms[\"P[err]\"])\n",
    "    err_terms = err_terms.drop(columns=\"P[err]\")\n",
    "    return err_terms\n",
    "show_table()"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.11.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}