Closed wenjin1997 closed 2 months ago
基于单列有序的表格，Lasso 论文定义了一类新的 Lookup Argument，称之为 Indexed Lookup Argument： $$ \forall i\in [m], fi = t{a_i} $$
基于单列有序的表格，Lasso 论文定义了一类新的 Lookup Argument，称之为 Indexed Lookup Argument：
$$ \forall i\in [m], fi = t{a_i} $$
对于 $[m]$ ，在有的编码理论书籍中 $[m]$ 表示的是集合 $\{1,2, \cdots, m\}$，这里其实想表达 $\{0, 1, \cdots, m - 1\}$，当然如果将 $[m]$ 理解为计算机中数组的下标，和想表达的 $\{0, 1, \cdots, m - 1\}$ 是一致的，这里并未对此符号做特别说明，因此可以利用上下文中使用过的的区间表示形式 $[0,m)$ 来表达相同的意思。
我们可以找到一个值， $\kappa>\mathsf{max}\{t_i, i\in[0,N-1)\}$ ，然后通过 $\kappa$ 把索引列合并到原表格列：
根据后文表述“Prover还要额外证明表格列中的每一项 $t_i < \kappa$ ，这需要 $N$个 Range Arguments”，这里选取的 $\kappa$ 应该是 $\vec{t}$ 中所有 $N$ 个元素的最大值。（我不确定论文中是否是这样，我没找到相关说明😅）
$$ M\vec{t} = \vec{f} $$
以及矩阵与向量的乘法运算， 矩阵 $M$ 的大小应该是 $m \times N$ 或者 $m \times n$ 。
其中 $\vec{t}$ 为表格，长度为 $m$，$\vec{f}$ 为 lookup 记录，长度为 $n$。这个核心公式来自 [Baloo] 论文。 矩阵 $M\in\mathbb{F}^{N\times m}$ 充当了选择器的角色。
其中 $\vec{t}$ 为表格，长度为 $m$，$\vec{f}$ 为 lookup 记录，长度为 $n$。这个核心公式来自 [Baloo] 论文。
矩阵 $M\in\mathbb{F}^{N\times m}$ 充当了选择器的角色。
理解Lasso（零）：带索引的查询证明
对于 $[m]$ ，在有的编码理论书籍中 $[m]$ 表示的是集合 $\{1,2, \cdots, m\}$，这里其实想表达 $\{0, 1, \cdots, m - 1\}$，当然如果将 $[m]$ 理解为计算机中数组的下标，和想表达的 $\{0, 1, \cdots, m - 1\}$ 是一致的，这里并未对此符号做特别说明，因此可以利用上下文中使用过的的区间表示形式 $[0,m)$ 来表达相同的意思。
根据后文表述“Prover还要额外证明表格列中的每一项 $t_i < \kappa$ ，这需要 $N$个 Range Arguments”，这里选取的 $\kappa$ 应该是 $\vec{t}$ 中所有 $N$ 个元素的最大值。（我不确定论文中是否是这样，我没找到相关说明😅）
$$ M\vec{t} = \vec{f} $$
以及矩阵与向量的乘法运算， 矩阵 $M$ 的大小应该是 $m \times N$ 或者 $m \times n$ 。