中点 VM

此包将中点 VM 的所有组件聚合在一个地方。具体来说，它从 处理器、验证器 和 验证器 包中导出功能。此外，当编译为可执行文件时，此包可以通过 CLI 接口 使用，以执行中点 VM 程序并验证其执行的正确性。

基本概念

有关中点 VM 的详细介绍可在完整的 中点 VM 文档 中找到。在本节中，我们仅介绍基础知识，以便使包含的示例更容易理解。

编写程序

我们的目标是使中点 VM 成为易于编译的高级区块链语言（如 Solidity、Move、Sway 等）的目标。我们相信让人们用他们选择的语言编写程序很重要。然而，帮助完成此任务的编译器尚未开发出来。因此，目前编写中点 VM 程序的主要方法是使用 中点汇编。

中点汇编器将汇编源代码编译成 程序 MAST，该程序由 Program 结构体表示。手动构建 Program 结构体是可能的，但我们不建议这样做，因为它很繁琐，容易出错，并且需要深入了解 VM 内部机制。所有这些文档中的示例都使用汇编语法。

程序哈希

所有Miden程序都可以缩减为一个32字节的值，称为程序哈希。一旦构造了一个Program对象，您可以通过Program::hash()方法访问此哈希值。验证者在验证程序执行时使用此哈希值。这确保验证者验证的是特定程序的执行（例如，验证者之前已提交的程序）。计算程序哈希的方法在这里描述。

输入/输出

目前，有3种方法可以将值推送到堆栈上

1. 您可以使用push指令将值推送到堆栈上。这些值成为程序本身的一部分，因此，在程序执行之间不能更改。您可以将其视为常量。
2. 堆栈可以在程序开始时初始化为某些值集。这些输入是公开的，必须与验证者共享，以便他们验证Miden程序的正确执行证明。可以接收初始值的堆栈顶部元素的数量限制为16。
3. 程序可能需要从证明者请求非确定性建议输入。这些输入是秘密输入。这意味着证明者不需要与验证者共享它们。有两种类型的建议输入：（1）一个可以包含任意数量元素的单一建议带；（2）一组建议集，用于为与Merkle树一起工作的指令提供非确定性输入。程序可以请求的建议输入数量没有限制。

堆栈和建议输入通过ProgramInputs结构提供给Miden虚拟机。要实例化此结构，您可以使用ProgramInputs::new()构造函数，以及ProgramInputs::from_stack_inputs()和ProgramInputs:none()便捷构造函数。

程序执行后剩余在堆栈上的值可以作为程序输出返回。您可以指定应返回多少值（从堆栈顶部）。目前，输出值的最大数量限制为16。

仅有16个元素来描述程序的公开输入和输出可能看起来很有限，但是只需4个元素就足以表示Merkle树的根或元素的顺序哈希。这两种都可以通过通过建议提供者非确定性提供实际值来扩展为任意数量的值。

用法

Miden存储库公开了一些函数，可以用于执行程序、生成其正确执行的证明以及验证生成的证明。如何做到这一点在下面解释，但您还可以查看工作示例这里，以及通过CLI运行它们的说明这里。

执行程序

要在Miden虚拟机上执行程序，您可以使用execute()或execute_iter()函数。这两个函数接受相同的参数

• program: &Program - 要执行的可执行Miden程序的引用。
• inputs: &ProgramInputs - 要执行程序的公共和秘密输入的引用。

execute()函数返回一个Result<ExecutionTrace, ExecutionError>，其中包含程序执行成功的执行跟踪，或者执行失败时的错误。您可以检查跟踪以从其中获取虚拟机的最终状态，但通常，这个跟踪是为了在证明生成过程中由证明者内部使用。

execute_iter()函数返回一个VmStateIterator，可用于迭代执行程序的循环以进行调试。实际上，当我们使用此函数执行程序时，保留了大量的调试信息，我们可以得到任何循环的虚拟机状态的精确图像。此外，如果执行结果为错误，VmStateIterator仍然可以用于检查直到错误发生的循环的虚拟机状态。

例如

use miden::{Assembler, ProgramInputs};

// instantiate the assembler
let assembler = Assembler::default();

// compile Miden assembly source code into a program
let program = assembler.compile("begin push.3 push.5 add end").unwrap();

// execute the program with no inputs
let trace = miden::execute(&program, &ProgramInputs::none()).unwrap();

// now, execute the same program in debug mode and iterate over VM states
for vm_state in miden::execute_iter(&program, &ProgramInputs::none()) {
    match vm_state {
        Ok(vm_state) => println!("{:?}", vm_state),
        Err(_) => println!("something went terribly wrong!"),
    }
}

证明程序执行

要在Miden虚拟机上执行程序并生成证明以证明程序已正确执行，您可以使用prove()函数。此函数需要以下参数

• program: &Program - 要执行的可执行Miden程序的引用。
• inputs: &ProgramInputs - 要执行程序的公共和秘密输入的引用。
• num_stack_outputs: usize - 要作为程序输出返回的堆栈上项的数量。
• options: &ProofOptions - 证明生成配置参数。默认选项针对96位安全级别。

如果程序执行成功，该函数返回一个包含两个元素的元组

• outputs: Vec<u64> - 程序生成的输出。向量中的元素数量将等于num_stack_outputs参数。
• proof: StarkProof - 程序执行证明。StarkProof可以使用to_bytes()和from_bytes()函数分别轻松序列化和反序列化。

证明生成示例

这是一个执行程序并将两个数字推入堆栈然后计算它们之和的简单示例

use miden::{Assembler, ProgramInputs, ProofOptions};

// instantiate the assembler
let assembler = Assembler::default();

// this is our program, we compile it from assembly code
let program = assembler.compile("begin push.3 push.5 add end").unwrap();

// let's execute it and generate a STARK proof
let (outputs, proof) = miden::prove(
    &program,
    &ProgramInputs::none(),   // we won't provide any inputs
    1,                        // we'll return one item from the stack
    &ProofOptions::default(), // we'll be using default options
)
.unwrap();

// the output should be 8
assert_eq!(vec![8], outputs);

验证程序执行

要验证程序执行，您可以使用verify()函数。该函数需要以下参数

• program_hash: Digest - 要验证的程序哈希（表示为32字节摘要）。
• stack_inputs: &[u64] - 在程序执行之前初始化堆栈的值的列表。
• stack_outputs: &[u64] - 程序完成执行后从堆栈返回的值的列表。
• proof: StarkProof - 程序执行过程中生成的证明。

栈输入期望按顺序排列，仿佛它们会依次压入栈中。因此，它们在栈中的预期顺序将是它们提供顺序的相反，并且 stack_inputs 切片中的最后一个值预期是栈顶的值。

栈输出期望按顺序排列，仿佛它们会依次从栈中弹出。因此，栈顶的值预期在 stack_outputs 切片的第一位置，其余输出元素的顺序也将与栈上的顺序匹配。这与 stack_inputs 切片的顺序相反。

函数返回 Result<(), VerificationError>，如果验证通过，则为 Ok(())，如果验证失败，则为 Err(VerificationError)，其中 VerificationError 描述了失败的原因。

如果执行一个具有提供的哈希的程序，并针对某些秘密输入和提供的公共输入，它将产生提供的输出。

注意验证者只需要知道程序的哈希，而不是实际的程序是什么。

证明验证示例

以下是验证上一个示例中程序执行的一个简单示例

use miden;

let program =   /* value from previous example */;
let proof =     /* value from previous example */;

// let's verify program execution
match miden::verify(program.hash(), &[], &[8], proof) {
    Ok(_) => println!("Execution verified!"),
    Err(msg) => println!("Something went terribly wrong: {}", msg),
}

斐波那契计算器

让我们为 Miden VM 编写一个简单的程序（使用 Miden 汇编）。我们的程序将计算第 5 个 斐波那契数

push.0      // stack state: 0
push.1      // stack state: 1 0
swap        // stack state: 0 1
dup.1       // stack state: 1 0 1
add         // stack state: 1 1
swap        // stack state: 1 1
dup.1       // stack state: 1 1 1
add         // stack state: 2 1
swap        // stack state: 1 2
dup.1       // stack state: 2 1 2
add         // stack state: 3 2

请注意，除了初始化栈的前两个操作外，swap dup.1 add 操作序列会不断重复。事实上，我们可以重复这些操作任意次数来计算任意斐波那契数。在 Rust 中，它看起来像这样（这实际上是 fibonacci.rs 中的示例的简化版本）

use miden::{Assembler, ProgramInputs, ProofOptions};

// set the number of terms to compute
let n = 50;

// instantiate the default assembler and compile the program
let source = format!(
    "
    begin 
        repeat.{}
            swap dup.1 add
        end
    end",
    n - 1
);
let program = Assembler::default().compile(&source).unwrap();

// initialize the stack with values 0 and 1
let inputs = ProgramInputs::from_stack_inputs(&[0, 1]).unwrap();

// execute the program
let (outputs, proof) = miden::prove(
    &program,
    &inputs,
    1,                        // top stack item is the output
    &ProofOptions::default(), // use default proof options
)
.unwrap();

// the output should be the 50th Fibonacci number
assert_eq!(vec![12586269025], outputs);

在上面的代码中，我们使用了公共输入来初始化栈，而不是使用 push 操作。这使得程序变得更简单，同时也允许我们从任意起始点运行程序，而不改变程序哈希。

命令行界面

如果您想在 Miden VM 上执行、证明和验证程序，但又不想编写 Rust 代码，您可以使用 Miden CLI。它还包含一些有用的工具，可以帮助分析和调试程序。

Miden VM 编译

首先，请确保您已经安装了 Rust 安装。当前版本的 Miden VM 需要 Rust 版本 1.62 或更高版本。

然后，要将 Miden VM 编译成二进制文件，请运行以下命令

cargo build --release --features executable

这将把 miden 可执行文件放在 ./target/release 目录中。

默认情况下，可执行文件将以单线程模式编译。如果您想启用多线程证明生成，可以使用以下命令编译 Miden VM

cargo build --release --features "executable concurrent"

运行 Miden VM

一旦编译了可执行文件，您就可以像这样运行 Miden VM

./target/release/miden [subcommand] [parameters]

目前，Miden VM 可以使用以下子命令执行

• run - 这将执行 Miden 汇编程序并输出结果，但不会生成执行证明。
• prove - 这将执行 Miden 汇编程序，并生成 STARK 执行证明。
• verify - 这将验证给定程序之前生成的执行证明。
• compile - 这将编译 Miden 汇编程序，并输出编译过程的相关统计信息。
• analyze - 这将运行 Miden 汇编程序针对特定输入，并输出其执行的相关统计信息。

以上所有子命令都需要提供各种参数。要获取有关给定子命令所需信息的更详细帮助，您可以运行以下命令

./target/release/miden [subcommand] --help

例如

./target/release/miden prove --help

斐波那契示例

在 miden/examples/fib 目录中，我们提供了一个非常简单的斐波那契计算器示例。此示例计算斐波那契数列的第1000项。您可以在 Miden 虚拟机上执行此示例，如下所示

./target/release/miden run -a miden/examples/fib/fib.masm -n 1

这将运行示例代码直到完成，并将输出栈顶剩余的元素。

软件包功能

Miden 虚拟机可以编译以下功能

• std - 默认启用，并依赖于 Rust 标准库。
• concurrent - 意味着 std，并且还启用多线程证明生成。
• executable - 如上所述构建 Miden 虚拟机二进制文件所必需的。意味着 std。
• no_std 不依赖于 Rust 标准库，并允许编译为 WebAssembly。

要使用 no_std 编译，通过 --no-default-features 标志禁用默认功能。

并发证明生成

当启用 concurrent 功能时，虚拟机将使用多个线程生成 STARK 证明。有关并发证明生成的优势，请参阅这些 基准测试。

内部，我们使用 rayon 进行并行计算。要控制生成 STARK 证明时使用的线程数，您可以使用 RAYON_NUM_THREADS 环境变量。

许可证

本项目采用 MIT 许可。