在 R1CS 中構造除法門
我不太明白的一件事是如何天真地處理 rank-1 約束系統 (R1CS) 中的除法運算。
據說
A.s * B.s - C.s = 0允許您執行任何加法/減法/乘法/除法運算，但是您如何在任何 SNARKs 系統中實際從乘法門執行除法？我能想到的唯一一件事是使用要除以的值的乘法逆作為部分B中的輸入A*B，這樣A*B就變成A*B^-1了與執行相同的A/B我的問題是驗證者如何知道發送到除法門的輸入證明者是 的乘法逆
B？似乎驗證者需要信任發送正確輸入的證明者（無法檢查證明者是否正在發送B^-1或其他B'^-1），我在這裡錯過了什麼嗎？-edited 我的問題是關於如何在除法上建立 R1CS 約束。例如，我如何為
(a*b)/(c*d)a、b、c、d 是算術電路的輸入建立一個約束矩陣。
那麼這個問題取決於你的意思 $ \textit{division} $ . R1CS 通常定義在一個有限域上 $ \mathbb{F}_p $ ，所以關於模逆的約束很容易表示。另一方面，如果您要詢問整數除法，而有限域算術本身並不支持它，那麼這將變得更加棘手。
讓我對此進行擴展。我將嘗試遵循Vitalik 的熱門文章中使用的符號。為了表示模逆運算，例如 $ x \cdot y^{-1} = z $ ，我們可以在扁平算術電路中定義兩個約束：
$ \text{one = y}\cdot \text{y_inv} $
$ \text{z = x}\cdot \text{y_inv} $
如您所見，我們引入了額外的變數 $ \text{y_inv} $ 並添加了約束 $ y \cdot y^{-1} = 1 $ （即模逆的定義）。
現在，您可能會問我們如何執行整數除法的問題，即， $ \lfloor\frac{x}{y}\rfloor = z $ ，使用有限域算術？回想一下，這與取模逆有很大不同 $ \mathbb{F}_p $ .
例如，讓我們嘗試 $ 7 / 2 $ 在 $ \mathbb{F}_{11} $ :
$ 7 / 2 = 7 \cdot 2^{-1} = 7 \cdot 6 = 42 = 9 \mod 11 $ ， 自從 $ 6 $ 是的模逆 $ 2 $ 在 $ \mathbb{F}_{11} $ .
然而， $ \lfloor\frac{7}{2}\rfloor = 3 $ （顯然）如果我們在談論整數算術。這種更複雜的操作可以表示為 $ O(\log(p)) $ R1CS 門使用非確定性建議，例如，通過強制執行 $ x = z \cdot y + r $ 和 $ r < y $ ， 在哪裡 $ r $ 由證明者提供。