前言

学完 Halo2 的基本用法和简单电路设计之后，你是否也想找一个相对简单但也有一定复杂性和趣味性的小应用来练练手？如果是的话，那不妨来看看这个 ZK Wordle 小游戏。

ZK  Wordle 介绍

ZK Wordle 是使用零知识证明的办法构建 Wordle 的程序。Wordle 是一个小游戏，游戏规则是用户有 6 次机会输出 5 个字母排列组成的单词，后台会将用户输入的单词和正确的单词进行匹配。如果输入的字母位置和正确单词的位置相同，那么就会给出绿色标识符，如果用户输入的单词字母在正确单词的某个字母匹配，但是位置可能不一致，这时候就会给出黄色标识符。游戏的胜利机制就是结合之前的绿色和黄色标识提示，在 6 次机会以内找到正确的单词。

假如说你成功找到了某个正确的单词，想向你的朋友炫耀一下。你的朋友可能会对此提出质疑。这个时候你为了打消他的质疑就需要向他证明你确实找到了某个正确单词。最简单的办法就是你直接告诉他正确的单词是什么，这样朋友就可以用这个你说的单词去实际验证一下是否真的正确。

但是这样一来，你相当于泄密了，你的朋友可能之前已经绞尽脑汁尝试了很多次都找不到正确的单词到底是什么，你告诉他这样他知道了，他就可以再别的朋友炫耀说自己找到正确单词（虽然实际上是你告诉他的，但他可能不会告诉别人）。那么有没有什么办法你在不泄露正确单词的情况下依旧向他证明你确实知道正确的单词是什么呢？

答案就是使用零知识证明这项技术。本文接下来就会具体介绍该如何设计和构建这样的证明。现在网络上已经有很多不同版本的使用零知识证明构建 ZK Wordle的项目，接下来我要分析的是使用 Halo2 设计构建的项目，该项目地址在：https://github.com/nalinbhardwaj/zordle

数据处理

dict.rs文件里面包含一个非常巨大的数组，里面是经过处理的数据，数据源自dict.json文件。将5个字母的单词经过自定义的hash运算之后转成数字。方便将来在约束电路中进行约束，来保证用户输入的 5 个字母能够组成单词。自定义 hash 运算格式如下：

pub fn word_to_chars(word: &str) -> Vec<u64> {

    let mut res = vec![];

    for c in word.chars() {

        res.push((c as u64) - ('a' as u64) + 1);

    }

    res

}

pub fn word_to_polyhash(word: &str) -> u64 {

    let chars = word_to_chars(word);

    let mut hash = 0;

    for c in chars {

        hash = hash * BASE;

        hash += c;

    }

    hash

}

我们还需要用到compute_diff函数，他的主要作用是比较输入的单词和正确的单词之间的差异（这些单词都会经过word_to_char处理，所以实际上是比较数字之间的差异），然后放进数组里面。举一个例子，比如正确的单词是“fluff"，用户输入的单词是“fault”，那么"fluff"经过word_to_char处理之后是[6,12,21,6,6]，“fault”是[6,1,21,12,20]，compute_diff输出会是[[1,0,1,0,0], [1,0,1,1,0]]该数组的第一项是green项，也就是字母正确同时位置正确，用 1 表示。其余用 0。数组第二项是yellow项，1 表示该字母在正确单词的字母中，不关心位置是否正确。0 表示该字母在正确的单词中未曾出现。

下面简单介绍一下整个数据处理流程。首先用户有 6 次机会输入单词，然后用上面介绍的方法，把单词转成 hash 数组和word_to_char数组，再同真正正确的单词数组final_char做比较，用于生成 green 和 yellow 项（使用compute_diff），这两项数据最终会输入到 instance 中。用于 circuit 电路的word_diffs_green和word_diffs_yellow数据与green和yellow项类似，只不过没有经过 0 和 1 的二值化处理，还保留原始的结果。

约束电路

接下来是 ZK Wordle 的约束电路设计，主要内容在wordle.rs文件中。我们首先来看一下整体约束电路结构（我假设正确的单词是“fluff”，而用户输入的单词是"fault"）。

图中的 Advice 其实是 11 列，不过为了图表不过于太大便于展示，我将原本 5 列的 char 折叠只选取第一列和最后一列，color_is_zero 列也同样如此。图中类似 big 或者 inv 不是表示 cell 中填入的是字母，而是真实数据，因为数值比较大，完整展示会导致图表比较难以展示，所以用 big 或者 inv 来代替。

接下来具体分析一下图表。其中 Instance 部分比较容易，我们在前一部分数据处理中已经做过分析。接下来分析 Advice 部分。

我们来横向的分析每一个 row，首先是第零行words部分。poly_word 部分是使用自定义的 hash 算法来对输入的单词("fault")处理之后的结果。后面是经过word_to_char 处理过后的单词数值表示。

第一行final_words填入正确单词的数值表示。

第二行 diff_g是将之前数据处理部分的word_diffs_green数据填入，第三行diff_y也是同样的，将word_diffs_yellow数据填入。

第四行diff_g_is_zero和第五行diff_y_is_zero是对word_diffs_green和word_diffs_yellow数据做二值化处理，然后填入。最终的结果应该要和 instance 中的green和yellow项一致。

第六行color_green和第七行color_yellow是将 Instance 列的green和yellow分别填入。

Advice 列的color_is_zero项分别来自diff_g和diff_y的数据做 inv 处理，至于为什么数据会填在diff_g_is_zero和diff_y_is_zero行是来自如下代码设置：

diffs_green_is_zero_chips[i].assign(&mut region, 4, diffs_green[i])?;

diffs_yellow_is_zero_chips[i].assign(&mut region, 5, diffs_yellow[i])?;

下面我们看一下整个电路的约束是如何设计的。

首先是查表约束，用于约束输入的单词是有效的单词而不是乱输入的字母。该约束表在table中，是一个非常巨大的表。

let table = DictTableConfig::configure(meta);

meta.lookup(|meta| {

 let q_lookup = meta.query_selector(q_input);

 let poly_word = meta.query_advice(poly_word, Rotation::cur());

 vec![(q_lookup * poly_word, table.value)] // check if q_lookup * value is in the table.

});

接下来是“range check”约束，用于约束输入的 word 确实是 26 个英文字母输入，因为word_to_char计算会 +1，所以实际上是从 1 开始遍历。

meta.create_gate("character range check", |meta| {

 let q = meta.query_selector(q_input);

 let mut constraints = vec![];

 for idx in 0..WORD_LEN {

  let value = meta.query_advice(chars[idx], Rotation::cur());

  let range_check = |range: usize, value: Expression<F>| {

   assert!(range > 0);

   (1..range).fold(Expression::Constant(F::ONE), |expr, i| {

    expr * (Expression::Constant(F::from(i as u64)) - value.clone())

   })

  };

  constraints.push(q.clone() * range_check(28, value.clone()));

 }

 constraints

});

原始代码处使用.fold(value.clone()...)，但我认为不太妥当，因为如果当 value 值为 0 的话，这个约束总是满足就达不到约束的效果，所以我将其修改为Expression::Constant(F::ONE)。

“poly hashing check”约束用于计算poly_hash和输入的 words 结果的一致性。

“diff_g checker”约束用于确保diff_g行的数据确实是由用户输入的字母和真实结果相减的差。

“diff_y checker”的检查和“diff_g checker”十分相似，但因为是检查 yellow 项，要比 green 检查略微复杂一点。要将每个字母都和 final_char 做差，所以是嵌套迭代。如果差为 0，那么就说明找到这个字母，因为只需要找到一个就可以了，所以是用乘积关系，保证总体乘积是 0。直观解释可能略微苍白，代码比较清晰的展示这一点。

meta.create_gate("diff_y checker", |meta| {

 let q = meta.query_selector(q_diff_y);

 let mut constraints = vec![];

 for i in 0..WORD_LEN {

  let char = meta.query_advice(chars[i], Rotation(-3));

  let diff_y = meta.query_advice(chars[i], Rotation::cur());

  let yellow_check = {

   (0..WORD_LEN).fold(Expression::Constant(F::ONE), |expr, i| {

    let final_char = meta.query_advice(chars[i], Rotation(-2));

    expr * (char.clone() - final_char)

   })

  };

  constraints.push(q.clone() * (yellow_check - diff_y));

 }

 constraints

});

"diff_color_is_zero checker"约束稍微复杂一点，一般的 create_gate 一次定义的时候只会有一个约束项起作用，但是这个 create_gate 定义的时候同时有多个约束项会起作用。

self.q_diff_green_is_zero.enable(&mut region, 4)?;

self.q_color_is_zero.enable(&mut region, 4)?;

self.q_diff_yellow_is_zero.enable(&mut region, 5)?;

self.q_color_is_zero.enable(&mut region, 5)?;

meta.create_gate("diff_color_is_zero checker", |meta| {

 let q_green = meta.query_selector(q_diff_green_is_zero);

 let q_yellow = meta.query_selector(q_diff_yellow_is_zero);

 let q_color_is_zero = meta.query_selector(q_color_is_zero);

 let mut constraints = vec![];

 for i in 0..WORD_LEN {

  let diff_color_is_zero = meta.query_advice(chars[i], Rotation::cur());

  constraints.push(q_color_is_zero.clone() * (diff_color_is_zero - (q_green.clone() * diffs_green_is_zero[i].expr() + q_yellow.clone() * diffs_yellow_is_zero[i].expr())));

 }

 constraints

});

仔细看代码，首先要解决的问题是Rotation::cur()到底在哪一行的问题，特别是这些约束项并不完全在同一行起作用。

我刚研究这段代码的时候也烦糊涂，事实上答案是Rotation::cur()既在第四行，又在第五行。这是一种电路设计技巧，如果你对此觉得疑惑，可以想象我实际写了 2 个create_gate，将其拆分的话是不是就不存在Rotation::cur()到底在哪一行的问题？那么上面这段代码只是把两个近乎一样的create_gate放在一起了而已。

为什么可以放在一起呢？因为q_selector这样的约束项要么值是 1 要么值是 0，如果这一项的值为 0，那么这个约束本身也不起作用。当Rotation::cur()在第四行的时候，第五行的q_yellow项就是 0，那么此时整个约束项就简化成了

q_color_is_zero.clone() * (diff_color_is_zero - q_green.clone() * diffs_green_is_zero[i].expr())

本来结果也就没有第五行任何事情，所以并不需要担心各个约束项不在同一行。

约束式中diffs_green_is_zero[i].expr()是is_zero约束，该约束实际上是值的约束。value * value_inv == 1，那么如果把 value_inv 的值确定了，value 的值就应该确定。也就是diff_g和diff_y的值和color_is_zero行对应的值应该有对应关系。

该约束的主要作用是确保diff_g_is_zero和diff_y_is_zero确实是由diff_g和diff_y的二值化计算二来。我以diff_g_is_zero举例来说明。如果 diff_g 的结果是 0，那么 1 - value * value_inv 的结果是 1，这个时候diff_g_is_zero的结果就应该是 1。如果 diff_g 的结果不是 0，那么 1 - value * value_inv 的结果是 0。这个时候diff_g_is_zero的结果就应该是 1。

“color check”也是有两行约束，分析原理同"diff_color_is_zero checker"一样，这里就不做展开说明了。该约束的主要作用是确保color和diff_color的值相反，和diff_color_is_zero值相同。

最后

以上是对约束的全部介绍，也是 ZK Wordle的核心部分。关于 WebAssembly 部分，这里就不做展开介绍了，这部分在这个地方有详细讲解：https://zcash.github.io/halo2/user/wasm-port.html。需要注意的是因为该项目使用的是 nightly-2022-04-07 toolchain 构建，使用最新的 wasm 无法打包 rust 代码，需要使用更低版本的 wasm，我尝试使用 0.10.3 构建成功。但是该版本打包出来的 js 代码结构和最新版本的 wasm 代码已经有了较大差异，可能不太有足够的学习参考价值。如果对于 Rust 构建 wasm 感兴趣的可以参考这篇教程学习：https://rustwasm.github.io/docs/book/introduction.html

声明：本网站所有相关资料如有侵权请联系站长删除，资料仅供用户学习及研究之用，不构成任何投资建议！