From 3ba3e27c5a20d7064836e70c4d637539f7d85347 Mon Sep 17 00:00:00 2001
From: rasmus-kirk <mail@rasmuskirk.com>
Date: Fri, 31 Jan 2025 16:32:04 +0100
Subject: [PATCH] Fixed CI and updated slides

---
 flake.lock       | 27 +++++++++--------
 slides/slides.md | 79 +++++++++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 93 insertions(+), 13 deletions(-)

diff --git a/flake.lock b/flake.lock
index 6685f17..ff719ee 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,14 +8,15 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "path": "./code",
+        "lastModified": 1,
+        "narHash": "sha256-h9jRc0LkpMXB+z4KnepKuX9Papst3+h906R9Ntnh/Do=",
+        "path": "/nix/store/yxknwk8mdxmc3fiihcyzl2k26vc4448g-source/code",
         "type": "path"
       },
       "original": {
-        "path": "./code",
+        "path": "/nix/store/yxknwk8mdxmc3fiihcyzl2k26vc4448g-source/code",
         "type": "path"
-      },
-      "parent": []
+      }
     },
     "nixpkgs": {
       "locked": {
@@ -40,14 +41,15 @@
         ]
       },
       "locked": {
-        "path": "./report",
+        "lastModified": 1,
+        "narHash": "sha256-tdQw23Y0VGrrGRBbtOvTAEEU4IXJ5Dns8U6GwZnZQkI=",
+        "path": "/nix/store/yxknwk8mdxmc3fiihcyzl2k26vc4448g-source/report",
         "type": "path"
       },
       "original": {
-        "path": "./report",
+        "path": "/nix/store/yxknwk8mdxmc3fiihcyzl2k26vc4448g-source/report",
         "type": "path"
-      },
-      "parent": []
+      }
     },
     "root": {
       "inputs": {
@@ -86,14 +88,15 @@
         ]
       },
       "locked": {
-        "path": "./slides",
+        "lastModified": 1,
+        "narHash": "sha256-5xhg0ZegCEAW3GY6KKkw34UOiH4mz9z9wJ2SkXsoJak=",
+        "path": "/nix/store/yxknwk8mdxmc3fiihcyzl2k26vc4448g-source/slides",
         "type": "path"
       },
       "original": {
-        "path": "./slides",
+        "path": "/nix/store/yxknwk8mdxmc3fiihcyzl2k26vc4448g-source/slides",
         "type": "path"
-      },
-      "parent": []
+      }
     },
     "website-builder": {
       "inputs": {
diff --git a/slides/slides.md b/slides/slides.md
index 1acf0d1..d69eb27 100644
--- a/slides/slides.md
+++ b/slides/slides.md
@@ -224,7 +224,84 @@ As for the $\ASDLDecider$, it just runs $\PCDLCheck$ on the provided
 accumulator, which represents a evaluation proof i.e. an instance. This
 check will always pass, as the prover constructed it honestly.
 
-## Soundness proof
+## Soundness proof (1/?)
+
+Let $\CM = (\CMSetup, \CMCommit)$ be a perfectly binding commitment scheme. Fix
+a maximum degree $D \in \Nb$ and a random oracle $\rho$ that takes commitments
+from $\CM$ to $F_\pp$. Then for every family of functions $\{f_\pp\}_\pp$
+and fields $\{F_\pp\}_\pp$ where:
+
+- $f_\pp \in \Mc \to F_\pp^{\leq D}[X]$
+- $F \in \Nb \to \Nb$
+- $|F_\pp| \geq F(\l)$
+
+That is, for all functions, $f_\pp$, that takes a message, $\Mc$ as input and
+outputs a maximum D-degree polynomial. Also, usually $|F_\pp| \approx F(\l)$.
+For every message format $L$ and computationally unbounded $t$-query oracle
+algorithm $\Ac$, the following holds:
+$$
+\Pr\left[
+  \begin{array}{c}
+    p \neq 0 \\
+    \land \\
+    p(z) = 0
+  \end{array}
+  \middle|
+  \begin{array}{c}
+    \rho \from \mathcal{U}(\l) \\
+    \pp_\CM \gets \CMSetup(1^\l, L) \\
+    (m, \omega) \gets \Ac^\rho(\pp_\CM) \\
+    C \gets \CMCommit(m, \o) \\
+    z \in F_{\pp} \from \rho(C) \\
+    p := f_{\pp}(m)
+  \end{array}
+\right] \leq \sqrt{\frac{D(t+1)}{F(\l)}}
+$$
+
+## Soundness proof (1/?)
+
+$$
+\Pr \left[
+  \begin{array}{c}
+    \ASDLVerifier^{\rho_1}((q_{\acc_{i-1}} \cat \vec{q}), \acc_i) = \top, \\
+    \ASDLDecider^{\rho_1}(\acc_i) = \top \\
+    \land \\
+    \exists i \in [n] : \Phi_\AS(q_i) = \bot
+  \end{array}
+\right] \leq \negl(\l)
+$$
+Given:
+$$
+\begin{alignedat}{4}
+  &\rho_0 &&\leftarrow \Uc(\l),                                               &&\quad \rho_1  &&\leftarrow \Uc(\l), \\
+  &\pp_\PC &&\leftarrow \PCDLSetup^{\rho_0}(1^\l, D),                         &&\quad \pp_\AS &&\leftarrow \ASDLSetup^{\rho_1}(1^\l, \pp_\PC), \\
+  &(\vec{q}, \acc_{i-1}, \acc_i) &&\leftarrow \Ac^{\rho_1}(\pp_\AS, \pp_\PC), &&\quad q_{acc_{i-1}} &&\leftarrow \ToInstance(\acc_{i-1})
+\end{alignedat}
+$$
+
+- We call the probability that the adversary $\Ac$ wins the above game
+  $\d$. We bound $\d$ by constructing two adversaries, $\Bc_1, \Bc_2$, for
+  the zero-finding game. Assuming:
+  - $\Pr[\Bc_1 \text{ wins} \lor \Bc_2 \text{wins}] = \delta - \negl(\l)$
+  - $\Pr[\Bc_1 \text{ wins} \lor \Bc_2 \text{wins}] = 0$
+
+## Soundness Proof (3/?)
+
+
+$$
+\begin{aligned}
+  \Pr[\Bc_1 \text{ wins} \lor \Bc_2 \text{ wins}] &= \Pr[\Bc_1 \text{ wins}] + \Pr[\Bc_2\text{ wins}] - \Pr[\Bc_1 \text{ wins} \land \Bc_2 \text{ wins}]\\
+  \Pr[\Bc_1 \text{ wins} \lor \Bc_2 \text{ wins}] &= \Pr[\Bc_1 \text{ wins}] + \Pr[\Bc_2\text{ wins}] - 0 \\
+  \delta - \negl(\l)                              &\leq  \sqrt{\frac{D(t+1)}{F(\l)}} + \sqrt{\frac{D(t+1)}{F(\l)}} \\
+  \delta - \negl(\l)                              &\leq  2 \cdot \sqrt{\frac{D(t+1)}{|\Fb_q|}}                     \\
+  \delta                                          &\leq  2 \cdot \sqrt{\frac{D(t+1)}{|\Fb_q|}} + \negl(\l)         \\
+\end{aligned}
+$$
+
+Meaning that $\delta$ is negligible, since $q = |\Fb_q|$ is superpolynomial
+in $\l$.
+
+## Soundness Proof (3/?)
 
 ## Efficiency analysis