From 75383e5a2ef9ef6dcc05d0e505c379500700b6e6 Mon Sep 17 00:00:00 2001 From: gunadigani Date: Tue, 16 Sep 2025 17:21:38 -0400 Subject: [PATCH 1/2] docs: update the analysis of IsLessThanArray chip --- .../src/is_less_than_array/README.md | 64 ++++++++++++++----- 1 file changed, 48 insertions(+), 16 deletions(-) diff --git a/crates/circuits/primitives/src/is_less_than_array/README.md b/crates/circuits/primitives/src/is_less_than_array/README.md index 1caeb4b04b..336cd289e2 100644 --- a/crates/circuits/primitives/src/is_less_than_array/README.md +++ b/crates/circuits/primitives/src/is_less_than_array/README.md @@ -31,11 +31,10 @@ The comparison is performed by: ```math \begin{align} -m_i \cdot (m_i - 1) &= 0 & \forall\ i < N &\hspace{2em} (1)\\ -s\cdot\left[1 - \sum^{i-1}_{k=0} m_k\right] \cdot (y_i - x_i) &= 0 & \forall\ i < N &\hspace{2em} (2)\\ -m_i \cdot \left[(y_i - x_i) \cdot \texttt{diff\_inv} - 1\right] &= 0 & \forall\ i < N &\hspace{2em} (3)\\ -\sum^{N-1}_{i=0} m_i \cdot \left(\sum^{N-1}_{i=0} m_i - 1\right) &= 0 & &\hspace{2em} (4)\\ -s\cdot\left[1 - \sum^{N-1}_{i=0} m_i\right] \cdot \texttt{out} &= 0 & &\hspace{2em} (5) +m_i \cdot (m_i - 1) &= 0 & \forall\ i < N &\hspace{2em} \\ +s\cdot\left[1 - \sum^{i}_{j=0} m_j \right] \cdot (y_i - x_i) &= 0 & \forall\ i < N &\hspace{2em} \\ +m_i \cdot \left[(y_i - x_i) \cdot \texttt{diff\_inv} - 1\right] &= 0 & \forall\ i < N &\hspace{2em} \\ +s\cdot\left[1 - \sum^{N-1}_{j=0} m_j\right] \cdot \texttt{out} &= 0 & &\hspace{2em} \end{align} ``` @@ -43,7 +42,7 @@ Additionally, the chip applies the following constraint: ```math \begin{align} -\texttt{IsLessThan}\left(\sum^{N-1}_{i=0} m_i\cdot(y_i - x_i),\ \texttt{out},\ s,\ \texttt{lt\_decomp}\right) & &\hspace{2em} (6) +\texttt{IsLessThan}\left(\sum^{N-1}_{j=0} m_j \cdot(y_j - x_j),\ \texttt{out},\ s,\ \texttt{lt\_decomp}\right) & &\hspace{2em} \end{align} ``` @@ -52,13 +51,46 @@ Constraint (1) ensures all $`m_i`$ are boolean (either 0 or 1) There are two cases to consider: 1. When $`x = y`$ (arrays are identical): - - Since all $`x_i = y_i`$, constraint (2) is satisfied for all indices. - - Constraint (3) ensures all $`m_i = 0`$. - - Constraint (5) then forces $`\texttt{out} = 0`$ when $`s \neq 0`$. - -2. When $`x \neq y`$ (arrays differ): - - Let $`k`$ be the first index where $`x_k \neq y_k`$. - - For all $`i < k`$, we have $`x_i = y_i`$, so constraint (2) is satisfied when $`m_i = 0`$. - - At index $`k`$, constraint (2) requires $`m_k = 1`$ since $`y_k - x_k \neq 0`$ and all previous $`m_i = 0`$ where $`i < k`$. - - For all $`i > k`$, constraint (2) is satisfied when $`\sum^{i}_{j=0} m_j = 1`$. Since $`\sum^{k}_{j=0} m_j = 1`$ and each $`m_i`$ is boolean, this forces all subsequent $`m_i = 0`$. - - Constraint (6) determines whether $`x_k < y_k`$ and sets $`\texttt{out}`$ accordingly. + - Suppose that the constraints are satisfied. + - Constraint (3) ensures all $`m_i = 0`$ because $m_i \cdot (-1) = 0$ implies $m_i = 0$. + - Constraint (4) then forces $`\texttt{out} = 0`$ when $`s \neq 0`$ because $\sum_{j=0}^{N-1} m_j = 0$. + - Thus $m$ is all zero and $\texttt{out} = 0$ as desired. + - Now suppose that $m$ is all zero and $\texttt{out} = 1$. + - So by $m_i = 0$ for all $i=0,1,\cdots,n-1$ constraint (1) and (3) are satisfied. + - Since $x = y$, constraint (2) is also satisfied. + - Since $\texttt{out} = 0$, constraint (4) is also satisfied. + - Hence $m$ is all zero and $\texttt{out} = 0$ if and only if the constraints are satisfied. + +2. When $x \neq y$ (arrays are different): + - Let $k$ be the first index where $x_k \neq y_k$. + - Suppose that the constraints are satisfied and $s \not= 0$. + - For all $i \in \{0,1,\cdots,n-1\}$ such that $x_i = y_i$, constraint (3) satisfied forces $m_i = 0$ because + + ```math + m_i \cdot \bigl((x_i - y_i) \cdot \texttt{diff\_inv} - 1 \bigr) + = m_i \cdot \bigl( 0 \cdot \texttt{diff\_inv} - 1 \bigr) + = 0 + ``` + + which implies $m_i= 0$. + + - At index $k$, constraint (2) requires $m_k = 1$ because $y_k - x_k \not= 0$ and, by previous bullet point, all $i < k$ have $m_i = 0$. So $(y_k - x_k) \neq 0$. Thus $1 - \sum_{i=0}^{k} m_i = 1 - m_k = 0$. + - For all $i > k$ with $x_i \not= y_i$ constraint (2) being satisfied forces $m_i = 0$ by the following reasoning: + - Let $S = \{ p_0, p_1, \cdots, p_k \}$ be the set of position such that $x_{p_i} \neq y_{p_i}$ for $i \in \{0,1,\cdots,k\}$. So by definition of $k$, $p_0 = k$. + - For each $i=0,1,\cdots,k$: For each $j < p_i$ and $j \not \in S$ we have $x_j = y_j$, so $m_j = 0$. For each $j < p_i$ and $j \in S$ we have $m_j = 1$ if $j = k$ and $m_j = 0$ otherwise. + So + ```math + \sum_{j=0}^{p_i} m_j = m_k + m_{p_i} + \sum_{j=0}^{k-1} m_j + \sum_{j=k+1}^{p_i-1} m_j = 1 + m_{p_i} + ``` + - Because $x_{p_i} \not= y_{p_i}$ so $1 - \sum_{j=0}^{p_i} m_j = 0$ must hold for constraint (2) to be satisfied at $p_i$. So $1 = \sum_{j = 0}^{p_i} m_j = 1 + m_{p_i}$ which implies $m_{p_i} = 0$. + - Now we have showed that for all positions $i$ that have $x_i = y_i$, $m_i = 0$ must hold. For all positions $i > k$ with $x_i \not= y_i$, $m_i = 0$, and $m_k = 1$. Hence $m_j = 1$ if $j = k$ and $0$ otherwise. + - So if the constraints are satisfied then $m$ is $1$ at position $k$ and $0$ everywhere else. + + - Now suppose that $m$ is $1$ at position $k$ and $0$ everywhere else. + - Then $m$ is a boolean so it satisfies constraint (1). + - Also $\sum_{j=0}^{i} m_j = 1$ for $i \geq k$ and $y_i - x_i = 0$ for $i < k$. Hence constraint (2) satisfied for all $i$. + - For all $i$ with $x_i = y_i$ we have $m_i = 0$ so constraint (3) is satisfied. For all $i$ with $x_i \neq y_i$, either $i = k$ or $i > k$. When $i = k$, $(y_i - x_i) \cdot \texttt{diff\_inv} - 1 = (y_i - x_i) \cdot (y_i - x_i)^{-1} - 1 = 0$. When $i > k$, we have $m_i = 0$. So in all three cases, constraint (3) is satisfied. + - We also know that $\sum_{i=0}^{N-1} m_i = 1$ so constraint (4) is satisfied. + +Thus we showed that the constraints are satisfied iff $m$ is as desired. Then we pass $m$ to the $\texttt{IsLessThan}$ AIR which ensures $\texttt{out} = 1$ if and only if $x_k < y_k$. So $\texttt{IsLessThan}$ returns $\texttt{out} = 1$ if and only if $x$ is lexicographically smaller than $y$. + From 7bbf43db8636783662c336eec5b304acb95b54e3 Mon Sep 17 00:00:00 2001 From: gunadigani Date: Tue, 16 Sep 2025 17:22:22 -0400 Subject: [PATCH 2/2] fix: remove unnecessary constraint in is_less_than_array chip --- crates/circuits/primitives/src/is_less_than_array/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/circuits/primitives/src/is_less_than_array/mod.rs b/crates/circuits/primitives/src/is_less_than_array/mod.rs index 5113a83ad7..2b2ebf1457 100644 --- a/crates/circuits/primitives/src/is_less_than_array/mod.rs +++ b/crates/circuits/primitives/src/is_less_than_array/mod.rs @@ -134,7 +134,7 @@ impl IsLtArraySubAir { .assert_zero(not::(prefix_sum.clone()) * diff.clone()); builder.when(marker).assert_one(diff * diff_inv); } - builder.assert_bool(prefix_sum.clone()); + // When condition != 0, // - If `x != y`, then `prefix_sum = 1` so marker[i] must be nonzero iff i is the first // index where `x[i] != y[i]`. Constrains that `diff_inv * (y[i] - x[i]) = 1` (`diff_val`