零知识证明 - 深入理解Zinc

Star Li
更新于 2022-07-08 15:55
阅读 2451

Zinc语言是一种智能合约语言，能方便的构建其对应的电路。Zinc开发的程序，编译成ZincVM指令，并在ZincVM执行并构建电路。构建电路的过程是将指令顺序执行，跟踪以及统一数据流。因为ZincVM构建电路需要将代码“静态”展开，所以Zinc不支持图灵完备。

疫情在家，多看点代码。对于疫情也感慨几句，对于资深程序员，这么多年了还没有和家人在一起吃晚饭这么多天。老实讲，比平时公司附近晚上吃的好得多。上海停运了，连各种骚扰电话也少了。有空再翻了翻Zinc的设计和代码，感受一下Matter Labs对[zkVM](https://learnblockchain.cn/article/4296)的设计和理念。

Zinc提供一种可靠，简单的电路开发语言。Zinc不支持图灵完备。Zinc从2019年就开始开发，最后一个Patch是2021年9月份。

```
commit 30d43721d98c727327bb92b6888f5903556a4261
Author: Alex Z <hedgar2017@gmail.com>
Date:   Sat Sep 25 15:21:42 2021 +0300

Update README.md
```

### 1. 代码框架

https://github.com/matter-labs/zinc.git

Zinc项目代码包含了比较多的子项目，主要分为如下几部分：

* zinc-book - 系统介绍Zinc的方方面面，从变量类型的定义，表达式，智能合约的实现，vm的基本原理等等。
* zargo - 利用zinc实现的各种包的管理器。
* zinc-types - Zinc相关的基础类型的定义。
* zinc-compiler/zinc-lexical/zinc-syntax - Zinc编译器相关，zinc语言编译成ZincVM支持的指令集。
* zinc-vm - ZincVM的实现，主要实现ZincVM对应的约束系统。

接下来分别介绍相关的子项目。重点介绍ZincVM的实现。

### 2. Zinc Book

Zinc Book给出了Zinc语言的全貌。Zinc语言的语法类似rust语言。具体的语法和表达式，相对简单。利用Zinc语言可以开发智能合约。Zinc语言通过编译器可以编译成ZincVM可以运行的指令。ZincVM的好处是运行的程序可以描述成R1CS的约束，由此可以给出程序执行的证明。

Zinc语言编译器实现在zinc-compiler/zinc-lexical/zinc-syntax，对应词法/语法分析。在深入ZincVM之前，先了解一下ZincVM对应的指令集。

### 3. ZincVM指令集

ZincVM指令集定义在zinc-types/src/instructions/mod.rs：

```
pub enum Instruction {
  /// The no-operation instruction.
  NoOperation(NoOperation),

/// An evaluation stack instruction.
  Push(Push),
  /// An evaluation stack instruction.
  Slice(Slice),
  /// An evaluation stack instruction.
  Copy(Copy),

/// A data stack instruction.
  Load(Load),
  /// A data stack instruction.
  LoadByIndex(LoadByIndex),
  /// A data stack instruction.
  Store(Store),
  /// A data stack instruction.
  StoreByIndex(StoreByIndex),

/// A contract storage instruction.
  StorageInit(StorageInit),
  /// A contract storage instruction.
  StorageFetch(StorageFetch),
  /// A contract storage instruction.
  StorageStore(StorageStore),
  /// A contract storage instruction.
  StorageLoad(StorageLoad),

/// An arithmetic operator instruction.
  Add(Add),
  /// An arithmetic operator instruction.
  Sub(Sub),
  /// An arithmetic operator instruction.
  Mul(Mul),
  /// An arithmetic operator instruction.
  Div(Div),
  /// An arithmetic operator instruction.
  Rem(Rem),
  /// An arithmetic operator instruction.
  Neg(Neg),

/// A logical operator instruction.
  Not(Not),
  /// A logical operator instruction.
  And(And),
  /// A logical operator instruction.
  Or(Or),
  /// A logical operator instruction.
  Xor(Xor),

/// A comparison operator instruction.
  Lt(Lt),
  /// A comparison operator instruction.
  Le(Le),
  /// A comparison operator instruction.
  Eq(Eq),
  /// A comparison operator instruction.
  Ne(Ne),
  /// A comparison operator instruction.
  Ge(Ge),
  /// A comparison operator instruction.
  Gt(Gt),

/// A bitwise operator instruction.
  BitwiseShiftLeft(BitwiseShiftLeft),
  /// A bitwise operator instruction.
  BitwiseShiftRight(BitwiseShiftRight),
  /// A bitwise operator instruction.
  BitwiseAnd(BitwiseAnd),
  /// A bitwise operator instruction.
  BitwiseOr(BitwiseOr),
  /// A bitwise operator instruction.
  BitwiseXor(BitwiseXor),
  /// A bitwise operator instruction.
  BitwiseNot(BitwiseNot),

/// The cast operator instruction.
  Cast(Cast),

/// A flow control instruction.
  If(If),
  /// A flow control instruction.
  Else(Else),
  /// A flow control instruction.
  EndIf(EndIf),
  /// A flow control instruction.
  LoopBegin(LoopBegin),
  /// A flow control instruction.
  LoopEnd(LoopEnd),
  /// A flow control instruction.
  Call(Call),
  /// A flow control instruction.
  Return(Return),

/// An intrinsic function call instruction.
  Dbg(Dbg),
  /// An intrinsic function call instruction.
  Require(Require),
  /// The standard library function call instruction.
  CallLibrary(CallLibrary),

/// A debug location marker instruction.
  FileMarker(FileMarker),
  /// A debug location marker instruction.
  FunctionMarker(FunctionMarker),
  /// A debug location marker instruction.
  LineMarker(LineMarker),
  /// A debug location marker instruction.
  ColumnMarker(ColumnMarker),
}
```

这些指令分为几类：

1/ Memory操作 - Evaluation Stack/Data Stack

2/ Storage操作

3/ 算术计算 - 加减乘除，逻辑比较，位操作

4/ 控制流 - If，Loop以及Call（函数调用）

5/ 其他 - 库调用，debug相关指令

熟悉其他平台指令集的小伙伴对控制流的指令集可能比较好奇。ZincVM的控制流的指令集更像标记，而不是“jump“指令。

### 4. ZincVM

ZincVM的代码结构相对清晰：

![2.png](https://img.learnblockchain.cn/attachments/2022/07/o4wVzs1l62c7e20acc3e6.png!/scale/60)

zvm是虚拟机的执行入口。zvm通过Command的execute函数开始执行。识别出对应的Application后，调用相应的run/test函数。ZincVM的Application定义在zinc-types/src/application/mod.rs：

```
pub enum Application {
  /// The circuit application variant.
  Circuit(Circuit),
  /// The contract application variant.
  Contract(Contract),
  /// The library variant.
  Library(Library),
}
```

也就是说，有三种Application：1/ Circuit - 普通的电路（给定输入，获取输出）2/ Contract - 为zkSync编写的智能合约，操作zkSync的存储 3/ Library - 电路库。

run函数实现如下：

```
pub fn run<CB, F>(
  &mut self,
  circuit: zinc_types::Circuit,
  input_values: Option<&[BigInt]>,
  mut instruction_callback: CB,
  mut check_cs: F,
) -> Result<Vec<Option<BigInt>>, Error>
where
  CB: FnMut(&CS),
  F: FnMut(&CS) -> Result<(), Error>,
{
...
  let one = Scalar::new_constant_usize(1, zinc_types::ScalarType::Boolean);
  self.condition_push(one)?;

let input_size = circuit.input.size();
  self.init_root_frame(circuit.input, input_values)?;

if let Err(error) = zinc_types::Call::new(circuit.address, input_size)
      .execute(self)
      .and(check_cs(&self.counter.cs))
  {
      log::error!("{}\nat {}", error, self.location.to_string().blue());
      return Err(error);
  }

while self.execution_state.instruction_counter < circuit.instructions.len() {
      ...
      let instruction =
          circuit.instructions[self.execution_state.instruction_counter].clone();

self.execution_state.instruction_counter += 1;
      if let Err(error) = instruction.execute(self).and(check_cs(&self.counter.cs)) {
...
      }

self.counter.cs.pop_namespace();
  }

self.get_outputs()
}
```

核心逻辑是在做了一些准备工作后（创建root frame，初始instruction counter等等），**依次**遍历每个Instruction。instructions目录下实现了相关指令的约束实现。gadgets目录下实现了约束系统一些小工具。core目录下是三种应用程序的“核心”实现。特别注意的是，所有的指令是依次执行的，并不像真正执行时候进行跳转。ZincVM针对一个程序的执行情况，“静态”构建相应的电路。也就是说，ZincVM并不是证明某个可能的执行指令序列，而是证明所有的执行序列。

这些模块之间的接口和关系如下图所示：

![3.jpg](https://img.learnblockchain.cn/attachments/2022/07/AUdE1EAe62c7e225a9362.jpg)

ZincVM内部的状态通过ExecuteState表示。整个VM执行对应的约束系统通过ConstraintSystem进行构建。每个Instruction都实现了IExecutable接口，并通过传入的IVirtualMachine的实例修改VirtualMachine的状态，并构建相应的约束系统。

接下来详细分析几个Instruction深入理解ZincVM的电路设计。

#### 4.1 Add

Add指令实现在zinc-vm/src/instructions/operators/arithmetic/add.rs。

```
impl<VM: IVirtualMachine> IExecutable<VM> for Add {
  fn execute(self, vm: &mut VM) -> Result<(), Error> {
      let right = vm.pop()?.try_into_value()?;
      let left = vm.pop()?.try_into_value()?;

let sum_type = zinc_types::ScalarType::expect_same(left.get_type(), right.get_type())?;

let condition = vm.condition_top()?;
      let cs = vm.constraint_system();

let unchecked_sum = gadgets::arithmetic::add::add(cs.namespace(|| "sum"), &left, &right)?;

let sum = Scalar::conditional_type_check(
          cs.namespace(|| "type check"),
          &condition,
          &unchecked_sum,
          sum_type,
      )?;

vm.push(Cell::Value(sum))
  }
}
```

ZincVM是Stack机器。Add指令从Evaluation Stack取得两个操作数（right和left）。从Condition Stack获取condition的“变量”。Add的gadget电路保证unchecked_sum = right + left。在condition的变量为“真”的情况下，对求和的结果进行数据类型的约束。最后将sum放入Evaluation Stack中。

需要注意的地方是，在Stack中存储的并不仅仅是数据，还包括了相应的电路变量。ZincVM中程序执行的过程也就是构建电路各个变量之间的关系的过程。Add指令相对简单。细心的小伙伴肯定要问，如果遇到If/Else的指令，两个不同的逻辑会引起不同的Stack的数据，这种情况如何处理？我们接着看If/Else/Endif的实现逻辑。

#### 4.2 If/Else/Endif

If/Else/Endif指令实现在zinc-vm/src/instructions/flow/conditional.rs：

```
impl<VM: IVirtualMachine> IExecutable<VM> for If {
  fn execute(self, vm: &mut VM) -> Result<(), Error> {
      vm.branch_then()
  }
}

impl<VM: IVirtualMachine> IExecutable<VM> for Else {
  fn execute(self, vm: &mut VM) -> Result<(), Error> {
      vm.branch_else()
  }
}

impl<VM: IVirtualMachine> IExecutable<VM> for EndIf {
  fn execute(self, vm: &mut VM) -> Result<(), Error> {
      vm.branch_end()
  }
}
```

详细查看一下branch_then，branch_else以及branch_end的实现。为了方便起见，我们查看Circuit应用程序对应的实现（zinc-vm/src/core/circuit/mod.rs），了解相关原理。

先看看branch_then：

```
fn branch_then(&mut self) -> Result<(), Error> {
  let condition = self.pop()?.try_into_value()?;

let prev = self.condition_top()?;

let cs = self.constraint_system();
  let next = gadgets::logical::and::and(cs.namespace(|| "branch"), &condition, &prev)?;
  self.execution_state.conditions_stack.push(next);

let branch = Branch {
      condition,
      is_else: false,
  };

self.top_frame()?.blocks.push(Block::Branch(branch));

self.execution_state.evaluation_stack.fork();
  self.execution_state.data_stack.fork();

Ok(())
}
```

If都是会带有条件的，这个条件就是"condition"变量（从Evaluation的Stack获取）。整个“逻辑”块的条件变量存放在"condition stack"中，也就是"prev"变量。因为进入了一个新的“逻辑”块，需要计算新的逻辑条件next (prev & condition) ，并将其存放在 condition stack中。因为进入了一个“逻辑”块，需要创建一个新的“frame”，记录状态。

关键的操作是需要将Evaluation Stack和Data Stack进行“fork”操作。Evaluation Stack的“fork”操作相对简单，就是创建一个新的Stack。Data Stack的“fork”操作相对复杂一些。

```
pub struct DataStack<E: IEngine> {
  pub memory: Vec<Option<Cell<E>>>,
  pub branches: Vec<DataStackBranch<E>>,
}

pub fn fork(&mut self) {
  self.branches.push(DataStackBranch::new());
}

pub enum DataStackBranch<E: IEngine> {
  IfThen(DataStackDelta<E>),
  IfThenElse(DataStackDelta<E>, DataStackDelta<E>),
}

pub type DataStackDelta<E> = BTreeMap<usize, CellDelta<E>>;
```

Data Stack的"fork"操作就是创建一个DataStackBranch，暂时存储新老Data Stack的差异。注意，DataStackBranch有两种类型，一种是有Else，一种是没有Else的。显然，对于有Else的情况下，需要采用两个DataStackDelta，分别存放If和Else情况下的DataStack的差异。

接着查看branch_else：

```
fn branch_else(&mut self) -> Result<(), Error> {
  let frame = self
      .execution_state
      .frames_stack
      .last_mut()
      .ok_or_else(|| Error::InternalError("Root frame is missing".into()))?;

let mut branch = match frame.blocks.pop() {
      Some(Block::Branch(branch)) => Ok(branch),
      Some(_) | None => Err(Error::MalformedBytecode(MalformedBytecode::UnexpectedElse)),
  }?;

if branch.is_else {
      return Err(MalformedBytecode::UnexpectedElse.into());
  } else {
      branch.is_else = true;
  }

let condition = branch.condition.clone();

frame.blocks.push(Block::Branch(branch));

self.condition_pop()?;
  let prev = self.condition_top()?;
  let cs = self.constraint_system();
  let not_cond = gadgets::logical::not::not(cs.namespace(|| "not"), &condition)?;
  let next = gadgets::logical::and::and(cs.namespace(|| "and"), &prev, &not_cond)?;
  self.condition_push(next)?;

self.execution_state.data_stack.switch_branch()?;
  self.execution_state.evaluation_stack.fork();

Ok(())
}
```

既然执行到Else，那在frame Stack中肯定有branch_then执行时创建的frame描述。获取frame描述，并将is_else改成true。因为进入Else分支，需要创建新的condition变量(prev & !condition)。Data Stack需要switch到Else分支。Evaluation Stack需要重新创建。

接着看branch_end：

```
fn branch_end(&mut self) -> Result<(), Error> {
  self.condition_pop()?;

let frame = self
      .execution_state
      .frames_stack
      .last_mut()
      .ok_or_else(|| Error::InternalError("Root frame is missing".into()))?;

let branch = match frame.blocks.pop() {
      Some(Block::Branch(branch)) => Ok(branch),
      Some(_) | None => Err(MalformedBytecode::UnexpectedEndIf),
  }?;

if branch.is_else {
      self.execution_state
          .evaluation_stack
          .merge(self.counter.next(), &branch.condition)?;
  } else {
      self.execution_state.evaluation_stack.revert()?;
  }

self.execution_state
      .data_stack
      .merge(self.counter.next(), branch.condition)?;

Ok(())
}
```

重点看Evaluation Stack和Data Stack的merge操作。在所有的分支执行完成后，需要对相应的状态进行Merge，从而继续执行后续指令。其实两种Stack的Merge操作，逻辑相似。以Evaluation Stack的merge操作为例：

```
pub fn merge<CS>(&mut self, mut cs: CS, condition: &Scalar<E>) -> Result<(), Error>
where
  CS: ConstraintSystem<E>,
{
  let else_case = self
      .stack
      .pop()
      .ok_or_else(|| Error::InternalError("Evaluation stack root frame missing".into()))?;
  let then_case = self
      .stack
      .pop()
      .ok_or_else(|| Error::InternalError("Evaluation stack root frame missing".into()))?;

if then_case.len() != else_case.len() {
      return Err(MalformedBytecode::BranchStacksDoNotMatch.into());
  }

for (index, (main_value, else_value)) in
      then_case.into_iter().zip(else_case.into_iter()).enumerate()
  {
      match (main_value, else_value) {
          (Cell::Value(main_value), Cell::Value(else_value)) => {
              let merged = gadgets::select::conditional(
                  cs.namespace(|| format!("merge {}", index)),
                  condition,
                  &main_value,
                  &else_value,
              )?;

self.push(Cell::Value(merged))?;
          }
      }
  }

Ok(())
}
```

从Evaluation Stack获得Then/Else情况下的两个Stack。通过conditional的gadget对两个Stack相同位置上的数据进行“merge”。所谓的merge，也就是说，创建新的电路变量，满足两种情况下的数据结果。新的变量的计算方式如下：

```
// Selected, Right, Left, Condition
// s = r + c * (l - r)
// (l - r) * (c) = (s - r)
```

If/Else/Endif的电路构造逻辑就介绍完成。Loop指令的电路相对容易，感兴趣的小伙伴可以自行查看。

### **总结：**

Zinc代码结构清晰，开发两年多，在2021年的9月份停止更新。Zinc语言是一种智能合约语言，能方便的构建其对应的电路。Zinc开发的程序，编译成ZincVM指令，并在ZincVM执行并构建电路。构建电路的过程是将指令顺序执行，跟踪以及统一数据流。因为ZincVM构建电路需要将代码“静态”展开，所以Zinc不支持图灵完备。

![](https://img.learnblockchain.cn/2020/08/13/15973018578548.jpg!/scale/20)

> 本文首发于：https://mp.weixin.qq.com/s/n1KIDuFpNDV_Q9SfNPm8xg

疫情在家，多看点代码。对于疫情也感慨几句，对于资深程序员，这么多年了还没有和家人在一起吃晚饭这么多天。老实讲，比平时公司附近晚上吃的好得多。上海停运了，连各种骚扰电话也少了。有空再翻了翻Zinc的设计和代码，感受一下Matter Labs对zkVM的设计和理念。

Zinc提供一种可靠，简单的电路开发语言。Zinc不支持图灵完备。Zinc从2019年就开始开发，最后一个Patch是2021年9月份。

commit 30d43721d98c727327bb92b6888f5903556a4261
Author: Alex Z &lt;hedgar2017@gmail.com>
Date:   Sat Sep 25 15:21:42 2021 +0300

  Update README.md

1. 代码框架

https://github.com/matter-labs/zinc.git

Zinc项目代码包含了比较多的子项目，主要分为如下几部分：

zinc-book - 系统介绍Zinc的方方面面，从变量类型的定义，表达式，智能合约的实现，vm的基本原理等等。
zargo - 利用zinc实现的各种包的管理器。
zinc-types - Zinc相关的基础类型的定义。
zinc-compiler/zinc-lexical/zinc-syntax - Zinc编译器相关，zinc语言编译成ZincVM支持的指令集。
zinc-vm - ZincVM的实现，主要实现ZincVM对应的约束系统。

接下来分别介绍相关的子项目。重点介绍ZincVM的实现。

2. Zinc Book

Zinc语言编译器实现在zinc-compiler/zinc-lexical/zinc-syntax，对应词法/语法分析。在深入ZincVM之前，先了解一下ZincVM对应的指令集。

3. ZincVM指令集

ZincVM指令集定义在zinc-types/src/instructions/mod.rs：

pub enum Instruction {
  /// The no-operation instruction.
  NoOperation(NoOperation),

  /// An evaluation stack instruction.
  Push(Push),
  /// An evaluation stack instruction.
  Slice(Slice),
  /// An evaluation stack instruction.
  Copy(Copy),

  /// A data stack instruction.
  Load(Load),
  /// A data stack instruction.
  LoadByIndex(LoadByIndex),
  /// A data stack instruction.
  Store(Store),
  /// A data stack instruction.
  StoreByIndex(StoreByIndex),

  /// A contract storage instruction.
  StorageInit(StorageInit),
  /// A contract storage instruction.
  StorageFetch(StorageFetch),
  /// A contract storage instruction.
  StorageStore(StorageStore),
  /// A contract storage instruction.
  StorageLoad(StorageLoad),

  /// An arithmetic operator instruction.
  Add(Add),
  /// An arithmetic operator instruction.
  Sub(Sub),
  /// An arithmetic operator instruction.
  Mul(Mul),
  /// An arithmetic operator instruction.
  Div(Div),
  /// An arithmetic operator instruction.
  Rem(Rem),
  /// An arithmetic operator instruction.
  Neg(Neg),

  /// A logical operator instruction.
  Not(Not),
  /// A logical operator instruction.
  And(And),
  /// A logical operator instruction.
  Or(Or),
  /// A logical operator instruction.
  Xor(Xor),

  /// A comparison operator instruction.
  Lt(Lt),
  /// A comparison operator instruction.
  Le(Le),
  /// A comparison operator instruction.
  Eq(Eq),
  /// A comparison operator instruction.
  Ne(Ne),
  /// A comparison operator instruction.
  Ge(Ge),
  /// A comparison operator instruction.
  Gt(Gt),

  /// A bitwise operator instruction.
  BitwiseShiftLeft(BitwiseShiftLeft),
  /// A bitwise operator instruction.
  BitwiseShiftRight(BitwiseShiftRight),
  /// A bitwise operator instruction.
  BitwiseAnd(BitwiseAnd),
  /// A bitwise operator instruction.
  BitwiseOr(BitwiseOr),
  /// A bitwise operator instruction.
  BitwiseXor(BitwiseXor),
  /// A bitwise operator instruction.
  BitwiseNot(BitwiseNot),

  /// The cast operator instruction.
  Cast(Cast),

  /// A flow control instruction.
  If(If),
  /// A flow control instruction.
  Else(Else),
  /// A flow control instruction.
  EndIf(EndIf),
  /// A flow control instruction.
  LoopBegin(LoopBegin),
  /// A flow control instruction.
  LoopEnd(LoopEnd),
  /// A flow control instruction.
  Call(Call),
  /// A flow control instruction.
  Return(Return),

  /// An intrinsic function call instruction.
  Dbg(Dbg),
  /// An intrinsic function call instruction.
  Require(Require),
  /// The standard library function call instruction.
  CallLibrary(CallLibrary),

  /// A debug location marker instruction.
  FileMarker(FileMarker),
  /// A debug location marker instruction.
  FunctionMarker(FunctionMarker),
  /// A debug location marker instruction.
  LineMarker(LineMarker),
  /// A debug location marker instruction.
  ColumnMarker(ColumnMarker),
}

这些指令分为几类：

1/ Memory操作 - Evaluation Stack/Data Stack

2/ Storage操作

3/ 算术计算 - 加减乘除，逻辑比较，位操作

4/ 控制流 - If，Loop以及Call（函数调用）

5/ 其他 - 库调用，debug相关指令

熟悉其他平台指令集的小伙伴对控制流的指令集可能比较好奇。ZincVM的控制流的指令集更像标记，而不是“jump“指令。

4. ZincVM

ZincVM的代码结构相对清晰：

pub enum Application {
  /// The circuit application variant.
  Circuit(Circuit),
  /// The contract application variant.
  Contract(Contract),
  /// The library variant.
  Library(Library),
}

也就是说，有三种Application：1/ Circuit - 普通的电路（给定输入，获取输出）2/ Contract - 为zkSync编写的智能合约，操作zkSync的存储 3/ Library - 电路库。

run函数实现如下：

pub fn run&lt;CB, F>(
  &mut self,
  circuit: zinc_types::Circuit,
  input_values: Option&lt;&[BigInt]>,
  mut instruction_callback: CB,
  mut check_cs: F,
) -> Result&lt;Vec&lt;Option&lt;BigInt>>, Error>
where
  CB: FnMut(&CS),
  F: FnMut(&CS) -> Result&lt;(), Error>,
{
...
  let one = Scalar::new_constant_usize(1, zinc_types::ScalarType::Boolean);
  self.condition_push(one)?;

  let input_size = circuit.input.size();
  self.init_root_frame(circuit.input, input_values)?;

  if let Err(error) = zinc_types::Call::new(circuit.address, input_size)
      .execute(self)
      .and(check_cs(&self.counter.cs))
  {
      log::error!("{}\nat {}", error, self.location.to_string().blue());
      return Err(error);
  }

  while self.execution_state.instruction_counter &lt; circuit.instructions.len() {
      ...
      let instruction =
          circuit.instructions[self.execution_state.instruction_counter].clone();

      self.execution_state.instruction_counter += 1;
      if let Err(error) = instruction.execute(self).and(check_cs(&self.counter.cs)) {
...
      }

      self.counter.cs.pop_namespace();
  }

  self.get_outputs()
}

核心逻辑是在做了一些准备工作后（创建root frame，初始instruction counter等等），依次遍历每个Instruction。instructions目录下实现了相关指令的约束实现。gadgets目录下实现了约束系统一些小工具。core目录下是三种应用程序的“核心”实现。特别注意的是，所有的指令是依次执行的，并不像真正执行时候进行跳转。ZincVM针对一个程序的执行情况，“静态”构建相应的电路。也就是说，ZincVM并不是证明某个可能的执行指令序列，而是证明所有的执行序列。

这些模块之间的接口和关系如下图所示：

接下来详细分析几个Instruction深入理解ZincVM的电路设计。

4.1 Add

Add指令实现在zinc-vm/src/instructions/operators/arithmetic/add.rs。

impl&lt;VM: IVirtualMachine> IExecutable&lt;VM> for Add {
  fn execute(self, vm: &mut VM) -> Result&lt;(), Error> {
      let right = vm.pop()?.try_into_value()?;
      let left = vm.pop()?.try_into_value()?;

      let sum_type = zinc_types::ScalarType::expect_same(left.get_type(), right.get_type())?;

      let condition = vm.condition_top()?;
      let cs = vm.constraint_system();

      let unchecked_sum = gadgets::arithmetic::add::add(cs.namespace(|| "sum"), &left, &right)?;

      let sum = Scalar::conditional_type_check(
          cs.namespace(|| "type check"),
          &condition,
          &unchecked_sum,
          sum_type,
      )?;

      vm.push(Cell::Value(sum))
  }
}

4.2 If/Else/Endif

If/Else/Endif指令实现在zinc-vm/src/instructions/flow/conditional.rs：

impl&lt;VM: IVirtualMachine> IExecutable&lt;VM> for If {
  fn execute(self, vm: &mut VM) -> Result&lt;(), Error> {
      vm.branch_then()
  }
}

impl&lt;VM: IVirtualMachine> IExecutable&lt;VM> for Else {
  fn execute(self, vm: &mut VM) -> Result&lt;(), Error> {
      vm.branch_else()
  }
}

impl&lt;VM: IVirtualMachine> IExecutable&lt;VM> for EndIf {
  fn execute(self, vm: &mut VM) -> Result&lt;(), Error> {
      vm.branch_end()
  }
}

详细查看一下branch_then，branch_else以及branch_end的实现。为了方便起见，我们查看Circuit应用程序对应的实现（zinc-vm/src/core/circuit/mod.rs），了解相关原理。

先看看branch_then：

fn branch_then(&mut self) -> Result&lt;(), Error> {
  let condition = self.pop()?.try_into_value()?;

  let prev = self.condition_top()?;

  let cs = self.constraint_system();
  let next = gadgets::logical::and::and(cs.namespace(|| "branch"), &condition, &prev)?;
  self.execution_state.conditions_stack.push(next);

  let branch = Branch {
      condition,
      is_else: false,
  };

  self.top_frame()?.blocks.push(Block::Branch(branch));

  self.execution_state.evaluation_stack.fork();
  self.execution_state.data_stack.fork();

  Ok(())
}

pub struct DataStack&lt;E: IEngine> {
  pub memory: Vec&lt;Option&lt;Cell&lt;E>>>,
  pub branches: Vec&lt;DataStackBranch&lt;E>>,
}

pub fn fork(&mut self) {
  self.branches.push(DataStackBranch::new());
}

pub enum DataStackBranch&lt;E: IEngine> {
  IfThen(DataStackDelta&lt;E>),
  IfThenElse(DataStackDelta&lt;E>, DataStackDelta&lt;E>),
}

pub type DataStackDelta&lt;E> = BTreeMap&lt;usize, CellDelta&lt;E>>;

接着查看branch_else：

fn branch_else(&mut self) -> Result&lt;(), Error> {
  let frame = self
      .execution_state
      .frames_stack
      .last_mut()
      .ok_or_else(|| Error::InternalError("Root frame is missing".into()))?;

  let mut branch = match frame.blocks.pop() {
      Some(Block::Branch(branch)) => Ok(branch),
      Some(_) | None => Err(Error::MalformedBytecode(MalformedBytecode::UnexpectedElse)),
  }?;

  if branch.is_else {
      return Err(MalformedBytecode::UnexpectedElse.into());
  } else {
      branch.is_else = true;
  }

  let condition = branch.condition.clone();

  frame.blocks.push(Block::Branch(branch));

  self.condition_pop()?;
  let prev = self.condition_top()?;
  let cs = self.constraint_system();
  let not_cond = gadgets::logical::not::not(cs.namespace(|| "not"), &condition)?;
  let next = gadgets::logical::and::and(cs.namespace(|| "and"), &prev, &not_cond)?;
  self.condition_push(next)?;

  self.execution_state.data_stack.switch_branch()?;
  self.execution_state.evaluation_stack.fork();

  Ok(())
}

接着看branch_end：

fn branch_end(&mut self) -> Result&lt;(), Error> {
  self.condition_pop()?;

  let frame = self
      .execution_state
      .frames_stack
      .last_mut()
      .ok_or_else(|| Error::InternalError("Root frame is missing".into()))?;

  let branch = match frame.blocks.pop() {
      Some(Block::Branch(branch)) => Ok(branch),
      Some(_) | None => Err(MalformedBytecode::UnexpectedEndIf),
  }?;

  if branch.is_else {
      self.execution_state
          .evaluation_stack
          .merge(self.counter.next(), &branch.condition)?;
  } else {
      self.execution_state.evaluation_stack.revert()?;
  }

  self.execution_state
      .data_stack
      .merge(self.counter.next(), branch.condition)?;

  Ok(())
}

pub fn merge&lt;CS>(&mut self, mut cs: CS, condition: &Scalar&lt;E>) -> Result&lt;(), Error>
where
  CS: ConstraintSystem&lt;E>,
{
  let else_case = self
      .stack
      .pop()
      .ok_or_else(|| Error::InternalError("Evaluation stack root frame missing".into()))?;
  let then_case = self
      .stack
      .pop()
      .ok_or_else(|| Error::InternalError("Evaluation stack root frame missing".into()))?;

  if then_case.len() != else_case.len() {
      return Err(MalformedBytecode::BranchStacksDoNotMatch.into());
  }

  for (index, (main_value, else_value)) in
      then_case.into_iter().zip(else_case.into_iter()).enumerate()
  {
      match (main_value, else_value) {
          (Cell::Value(main_value), Cell::Value(else_value)) => {
              let merged = gadgets::select::conditional(
                  cs.namespace(|| format!("merge {}", index)),
                  condition,
                  &main_value,
                  &else_value,
              )?;

              self.push(Cell::Value(merged))?;
          }
      }
  }

  Ok(())
}

// Selected, Right, Left, Condition
// s = r + c * (l - r)
// (l - r) * (c) = (s - r)

If/Else/Endif的电路构造逻辑就介绍完成。Loop指令的电路相对容易，感兴趣的小伙伴可以自行查看。

总结：

本文首发于：https://mp.weixin.qq.com/s/n1KIDuFpNDV_Q9SfNPm8xg

转载
学分: 0
分类: 零知识证明
标签: 零知识证明 zkVM Zinc

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。

零知识证明 - 深入理解Zinc

1. 代码框架

2. Zinc Book

3. ZincVM指令集

4. ZincVM

4.1 Add

4.2 If/Else/Endif

总结：

0 条评论

文章目录