Jolt zkVM上的一个挑战 - ZKSECURITY

zksecurity
发布于 2024-09-25 12:37
阅读 21

本文介绍了MOCA意大利黑客训练营CTF竞赛中一个名为“2+2=5”的密码学挑战，该挑战利用了修改后的Jolt zkVM。挑战要求参与者构造一个无效的RISC-V程序执行证明，利用Jolt库中的漏洞，使得程序输出错误的结果“5”，从而绕过服务器的验证并获得flag。

上周末，我参与了在 [MOCA 意大利黑客训练营](https://ctftime.org/event/2294) 期间为 CTF 活动创建一些挑战。
我编写的任务之一是一个名为 **“2+2=5”** 的密码学挑战，其中涉及到 Jolt zkVM：它涉及到为一个无效的 RISC-V 程序执行制作证明，该程序利用了 Jolt 库的修改版本。

这篇文章将介绍挑战声明和解决方案，如果你想自己尝试解决这个挑战，可以从[这里](https://github.com/fibonhack/MOCA-2024-finals-challs/raw/refs/heads/main/crypto/two_plus_two/two_plus_two.zip)下载原始附件！

### 什么是 Jolt？

[Jolt](https://jolt.a16zcrypto.com/) 是一个以 RISC-V ISA 为目标的 zkVM。
要使用 Jolt，我们需要编写两个 Rust 程序：

- **guest**(访客程序) 是我们想要证明其执行的程序。在 Jolt 中，这个程序将被编译成 RISC-V ELF 文件，并且假定 prover 和 verifier 双方都知道它。
- **host**(宿主程序) 是与 Jolt SDK 交互以发出访客执行证明或验证先前生成的给定目标访客程序的证明的组件。

访客程序被编译和模拟以计算其**执行轨迹**，这是一个保存所有已执行的有序指令的结构，以及指令执行、内存读取、内存写入等的具体值。
Jolt zkVM 接受执行轨迹，并为其有效性发出证明。
粗略地说，如果输入轨迹编码了访客程序的正确执行，且符合 RISC-V 语义，则证明将被 verifier 接受。

[文档](https://jolt.a16zcrypto.com/how/architecture.html)中给出了 Jolt 证明系统的架构概述。
Jolt zkVM 中有四个主要组件：

- **读写内存**：它使用内存检查参数来检查内存中的读写是否正确。对寄存器的读写操作是使用特殊地址的内存操作来实现的。
- **指令查找**：它使用一个名为 [Lasso](https://eprint.iacr.org/2023/1216) 的自定义查找参数来检查指令的执行是否正确，例如，`add` 指令的执行结果是否真的是操作数的总和。
- **字节码**：它使用只读内存检查参数来对访客程序的解码指令执行读取。
- **R1CS**：它处理程序计数器更新，并作为所有其他模块的粘合剂，例如，对跨其他组件的值施加约束。

### 挑战描述

该挑战允许用户与服务器交互，附件包含远程服务的源代码。

```sh
.
├── jolt         # 修改后的 Jolt crate
├── server       # 宿主服务器
│   └── guest    # 访客程序
├── diff.patch   # 应用于 Jolt 的补丁
├── Dockerfile   # Dockerfile 用于运行服务器
└── readme.txt   # Readme

```

要在本地运行它，只需构建 Docker 容器并运行它！

```sh
$ docker build . -t two_plus_two
$ docker run -p 5555:5555 -e FLAG="flag{some_secret_value}" -t two_plus_two

```

#### 服务器

服务器是一个 Rust 程序，它将充当 Jolt zkVM 的宿主程序。
它构建访客程序，从用户那里获取访客程序的执行证明并验证它。
除了实际的验证之外，服务器还执行一些额外的检查：

- 它检查访客程序是否没有输入，
- 它检查输出值是否为 `5`，并且
- 它检查程序在执行期间是否没有出现 panic。

如果用户提供了满足这些检查的有效证明，服务器将返回 flag，挑战将被解决！

```rust
use jolt_sdk::RV32IHyraxProof;

pub fn main() {
    let (_prove_two_plus_two, verify_two_plus_two) = guest::build_two_plus_two();

println!("Can you prove that 2+2=5?");

let line = std::io::stdin().lines().next().unwrap().unwrap();
    if line.len() == 0 {
        println!("k thx bye");
        return;
    }

let proof = RV32IHyraxProof::deserialize_from_bytes(
            &hex::decode(line).unwrap()
        ).unwrap();

let inputs = &proof.proof.program_io.inputs;
    println!("inputs: {:?}", inputs);
    assert_eq!(inputs.len(), 0);

let outputs = &proof.proof.program_io.outputs;
    println!("outputs: {:?}", outputs);
    assert_eq!(outputs.len(), 1);
    assert_eq!(outputs[0], 5); // 2+2 is 5!

let panics = &proof.proof.program_io.panic;
    println!("panics: {:?}", panics);
    assert!(!panics);

println!("Verifying the proof...");
    let is_valid = verify_two_plus_two(proof);
    if is_valid {
        println!("The proof is valid!");
        println!("FLAG: {}", std::env::var("FLAG").unwrap());
    } else {
        println!("The proof is invalid! :(");
    }
}

```

#### 访客程序

访客程序是一个计算 `2+2` 并返回结果的 Rust 程序。
附加到 `two_plus_two` 函数的 `#[jolt::provable]` 属性指定此函数实现了一个我们想要证明其执行的访客程序。
此属性将自动生成一些在宿主中可见的附加函数（例如，`build_two_plus_two`），这些函数将为宿主提供证明和验证函数。

`two_plus_two` 函数的主体可能看起来很复杂，它只是将值 `2` 加载到寄存器中，将其自身相加（即，计算 `2+2`），然后返回结果。
访客程序是使用内联汇编编写的，以避免 Rust 编译器执行的优化。
目的是在最终的访客可执行文件中保留 `add` 指令，但这对挑战的核心影响很小，除了使预期的解决方案稍微容易一些之外。

```rust
##![cfg_attr(feature = "guest", no_std)]
##![no_main]

##[jolt::provable]
fn two_plus_two() -> u16 {
    let mut n: u16 = 2;

#[cfg(any(target_arch = "riscv32", target_arch = "riscv64"))]
    unsafe {
        core::arch::asm!(
            "li {n}, 2",
            "add {n}, {n}, {n}",
            n = inout(reg) n,
        );
    }

#[cfg(target_arch = "x86_64")]
    unsafe {
        core::arch::asm!(
            "mov {n}, 2",
            "add {n}, {n}, {n}",
            n = inout(reg) n,
        );
    }
    n
}

```

按照 ISA 语义，此程序将始终返回 `4`，这是计算 `2+2` 的结果。
挑战的重点是制作一个输出为 `5` 的执行证明！

#### 修改后的 Jolt 库

`readme.txt` 文件解释了获取修改后的 Jolt 库所采取的步骤。

```sh
git clone git@github.com:a16z/jolt.git
cd jolt

## just the latest commit at time of writing
git checkout 0cc7aa31981ff8503fe256706d2aa9c320abd1cd
git apply ../diff.patch

```

Jolt 存储库按原样获取自上次提交（在编写挑战时），并对其应用了一个补丁。
该补丁可以在 `diff.patch` 文件中找到：它从 `jolt-core/src/r1cs/jolt_constraints.rs` 文件中删除了一些行。

```patch
diff --git a/jolt-core/src/r1cs/jolt_constraints.rs b/jolt-core/src/r1cs/jolt_constraints.rs
index 5fb0d871..295dce32 100644
--- a/jolt-core/src/r1cs/jolt_constraints.rs
+++ b/jolt-core/src/r1cs/jolt_constraints.rs
@@ -289,13 +289,8 @@ impl<F: JoltField> R1CSConstraintBuilder<F> for UniformJoltConstraints {

// if (rd != 0 && update_rd_with_lookup_output == 1) constrain(rd_val == LookupOutput)
         // if (rd != 0 && is_jump_instr == 1) constrain(rd_val == 4 * PC)
--        let rd_nonzero_and_lookup_to_rd =
-+        let _rd_nonzero_and_lookup_to_rd =
+            cs.allocate_prod(JoltIn::Bytecode_RD, JoltIn::OpFlags_LookupOutToRd);
--        cs.constrain_eq_conditional(
--            rd_nonzero_and_lookup_to_rd,
--            JoltIn::RD_Write,
--            JoltIn::LookupOutput,
--        );
  let rd_nonzero_and_jmp = cs.allocate_prod(JoltIn::Bytecode_RD, JoltIn::OpFlags_IsJmp);
         let lhs = JoltIn::Bytecode_ELFAddress + (PC_START_ADDRESS - PC_NOOP_SHIFT);
         let rhs = JoltIn::RD_Write;

```

##### 总结

要解决这个挑战，我们需要向服务器提供访客程序的执行证明，输出为 5。
为了做到这一点，我们需要利用 Jolt 已被修改并且可能不再健全的事实。

### 补丁分析

该补丁删除了 [R1CS 组件](https://jolt.a16zcrypto.com/how/r1cs_constraints.html)中的一个约束，让我们仔细看看被删除的约束。

```c
cs.constrain_eq_conditional(
    rd_nonzero_and_lookup_to_rd,
    JoltIn::RD_Write,
    JoltIn::LookupOutput,
);

```

如果第一个参数设置为 `1`，则 `constrain_eq_conditional` 函数会将第二个和第三个参数之间的相等约束添加到 R1CS 约束系统中。
粗略地说，发出的约束等效于以下等式。

```c
cs.constrain_eq_conditional(condition, left, right);
// condition  * (left - right) == 0

```

上面几行还有一个有用的注释，解释了约束。

```c
// if (rd != 0 && update_rd_with_lookup_output == 1) constrain(rd_val == LookupOutput)
cs.constrain_eq_conditional(
    rd_nonzero_and_lookup_to_rd,
    JoltIn::RD_Write,
    JoltIn::LookupOutput,
);

```

`RD_Write` 值来自读写内存组件，它表示写入输出寄存器的内存值。
相反，`LookupOutput` 值来自指令查找组件，它表示查找参数“返回”的输出值，该参数执行指令执行检查。
约束的目标是在这两个值之间提供**粘合**。
一个直观的解释如下。

> 如果指令应该将其结果写入寄存器，并且如果输出寄存器不为零，则写入输出寄存器的值应等于执行查找参数的结果。

删除了此约束后，利用思路很简单：制作一个执行轨迹，其中对 2 和 2 求和的 `add` 指令，不是将值 4 写回输出寄存器，而是写入值 5。
在生成的轨迹中：

- 查找参数将返回 4，因为该指令是 `add` 且操作数值均为 2，但是
- 写回输出寄存器的值将为 5。

由于删除了强制这两个值相等的约束，因此该轨迹将被接受。
然后，程序将继续正常运行并返回计算出的值，因此最终修改后的执行轨迹的输出将恰好为 `5`！

### 制作证明

一旦我们了解了所有活动的部件，实际的利用就非常容易：我们只需要在 `tracer` 模块中修补 Jolt，该模块是生成执行轨迹的模块。
我们修改了 `jolt/tracer/src/emulator/cpu.rs` 文件，更改了 `ADD` 操作仿真的语义：如果操作数均为 2，则将值 5 写回输出寄存器。

```rust
Instruction {
    mask: 0xfe00707f,
    data: 0x00000033,
    name: "ADD",
    operation: |cpu, word, _address| {
        let f = parse_format_r(word);

// If the operands are both 2, then write 5 in the output register
        // otherwise apply normal addition semantics
        if cpu.x[f.rs1] == 2 && cpu.x[f.rs2] == 2 {
            cpu.x[f.rd] = cpu.sign_extend(5);
        } else {
            cpu.x[f.rd] = cpu.sign_extend(cpu.x[f.rs1].wrapping_add(cpu.x[f.rs2]));
        }
        Ok(())
    },
    disassemble: dump_format_r,
    trace: Some(trace_r),
},

```

我们可以打印出来的一个有趣的事情是在执行 `add {n}, {n}, {n}` 指令的确切步骤中的执行轨迹。
这里要注意的主要部分是内存操作：该指令是 `ADD`，两个操作数都等于 `2`，因此有两个读取操作，但是然后有一个写入操作到具有值 5 的同一寄存器！

```rust
Trace[5]
JoltTraceStep {
    instruction_lookup: Some(ADD(ADDInstruction(2, 2))),
    bytecode_row: BytecodeRow {
        address: 2147483672,
        bitflags: 17448304640,
        rd: 10,
        rs1: 10,
        rs2: 10,
        imm: 0,
        virtual_sequence_remaining: None
    },
    memory_ops: [Read(10), Read(10), Write(10, 5), Read(0), Read(0), Read(0), Read(0)]
}

```

我们还可以直接打印 R1CS 系统的输入，这些输入存储在 `R1CSInputs` 结构中。
正如我们所看到的，查找正确返回 `4`，但是写入输出寄存器的值是 `5`。

```py
pc[7] = 9
bytecode_a[7] = 9
bytecode_v[7] = 9
memreg_a_rw[7] = 0
memreg_v_reads[7] = 2
memreg_v_writes[7] = 5
chunks_x[7] = 0
chunks_y[7] = 0
chunks_query[7] = 0
lookup_outputs[7] = 4
circuit_flags_bits[7] = 0
instruction_flags_bits[7] = 1

```

总而言之，主要的求解器 Rust 程序非常简单（使用修改后的 Jolt 库）。
运行此程序将输出一个证明，该证明提供给服务器将返回 flag！

```rust
use jolt_sdk::RV32IHyraxProof;

pub fn main() {
    let (prove_two_plus_two, verify_two_plus_two) = guest::build_two_plus_two();
    let (output, proof_gen) = prove_two_plus_two();
    println!("Proof generated! {}", output);
    let proof_bytes = proof_gen.serialize_to_bytes().unwrap();
    println!("{}", hex::encode(&proof_bytes));
}

```

这是一种解决挑战的方法，但实际上删除该特定约束提供了一个更强大的原语：我们可以为每个将其结果写回寄存器的指令将任意值写入寄存器！

### 结论

编写和解决挑战本质上是解决明确的 **假设** 实验。
这种方法是获得对底层技术和库（如本例中的 Jolt zkVM）的安全导向理解的绝佳途径。
此外，编写求解器程序或脚本的实践经验迫使我们以**具体**的方式展示 bug 的影响，这是在密码学审计中进行日常工作时的一项关键技能。

>- 原文链接： [blog.zksecurity.xyz/post...](https://learnblockchain.cn/article/17846/jolt-challenge)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

上周末，我参与了在 MOCA 意大利黑客训练营期间为 CTF 活动创建一些挑战。我编写的任务之一是一个名为 “2+2=5” 的密码学挑战，其中涉及到 Jolt zkVM：它涉及到为一个无效的 RISC-V 程序执行制作证明，该程序利用了 Jolt 库的修改版本。

这篇文章将介绍挑战声明和解决方案，如果你想自己尝试解决这个挑战，可以从这里下载原始附件！

什么是 Jolt？

Jolt 是一个以 RISC-V ISA 为目标的 zkVM。要使用 Jolt，我们需要编写两个 Rust 程序：

guest(访客程序) 是我们想要证明其执行的程序。在 Jolt 中，这个程序将被编译成 RISC-V ELF 文件，并且假定 prover 和 verifier 双方都知道它。
host(宿主程序) 是与 Jolt SDK 交互以发出访客执行证明或验证先前生成的给定目标访客程序的证明的组件。

访客程序被编译和模拟以计算其执行轨迹，这是一个保存所有已执行的有序指令的结构，以及指令执行、内存读取、内存写入等的具体值。 Jolt zkVM 接受执行轨迹，并为其有效性发出证明。粗略地说，如果输入轨迹编码了访客程序的正确执行，且符合 RISC-V 语义，则证明将被 verifier 接受。

文档中给出了 Jolt 证明系统的架构概述。 Jolt zkVM 中有四个主要组件：

读写内存：它使用内存检查参数来检查内存中的读写是否正确。对寄存器的读写操作是使用特殊地址的内存操作来实现的。
指令查找：它使用一个名为 Lasso 的自定义查找参数来检查指令的执行是否正确，例如，add 指令的执行结果是否真的是操作数的总和。
字节码：它使用只读内存检查参数来对访客程序的解码指令执行读取。
R1CS：它处理程序计数器更新，并作为所有其他模块的粘合剂，例如，对跨其他组件的值施加约束。

挑战描述

该挑战允许用户与服务器交互，附件包含远程服务的源代码。

.
├── jolt         # 修改后的 Jolt crate
├── server       # 宿主服务器
│   └── guest    # 访客程序
├── diff.patch   # 应用于 Jolt 的补丁
├── Dockerfile   # Dockerfile 用于运行服务器
└── readme.txt   # Readme

要在本地运行它，只需构建 Docker 容器并运行它！

$ docker build . -t two_plus_two
$ docker run -p 5555:5555 -e FLAG="flag{some_secret_value}" -t two_plus_two

服务器

服务器是一个 Rust 程序，它将充当 Jolt zkVM 的宿主程序。它构建访客程序，从用户那里获取访客程序的执行证明并验证它。除了实际的验证之外，服务器还执行一些额外的检查：

它检查访客程序是否没有输入，
它检查输出值是否为 5，并且
它检查程序在执行期间是否没有出现 panic。

如果用户提供了满足这些检查的有效证明，服务器将返回 flag，挑战将被解决！

use jolt_sdk::RV32IHyraxProof;

pub fn main() {
    let (_prove_two_plus_two, verify_two_plus_two) = guest::build_two_plus_two();

    println!("Can you prove that 2+2=5?");

    let line = std::io::stdin().lines().next().unwrap().unwrap();
    if line.len() == 0 {
        println!("k thx bye");
        return;
    }

    let proof = RV32IHyraxProof::deserialize_from_bytes(
            &hex::decode(line).unwrap()
        ).unwrap();

    let inputs = &proof.proof.program_io.inputs;
    println!("inputs: {:?}", inputs);
    assert_eq!(inputs.len(), 0);

    let outputs = &proof.proof.program_io.outputs;
    println!("outputs: {:?}", outputs);
    assert_eq!(outputs.len(), 1);
    assert_eq!(outputs[0], 5); // 2+2 is 5!

    let panics = &proof.proof.program_io.panic;
    println!("panics: {:?}", panics);
    assert!(!panics);

    println!("Verifying the proof...");
    let is_valid = verify_two_plus_two(proof);
    if is_valid {
        println!("The proof is valid!");
        println!("FLAG: {}", std::env::var("FLAG").unwrap());
    } else {
        println!("The proof is invalid! :(");
    }
}

访客程序

访客程序是一个计算 2+2 并返回结果的 Rust 程序。附加到 two_plus_two 函数的 #[jolt::provable] 属性指定此函数实现了一个我们想要证明其执行的访客程序。此属性将自动生成一些在宿主中可见的附加函数（例如，build_two_plus_two），这些函数将为宿主提供证明和验证函数。

two_plus_two 函数的主体可能看起来很复杂，它只是将值 2 加载到寄存器中，将其自身相加（即，计算 2+2），然后返回结果。访客程序是使用内联汇编编写的，以避免 Rust 编译器执行的优化。目的是在最终的访客可执行文件中保留 add 指令，但这对挑战的核心影响很小，除了使预期的解决方案稍微容易一些之外。

##![cfg_attr(feature = "guest", no_std)]
##![no_main]

##[jolt::provable]
fn two_plus_two() -> u16 {
    let mut n: u16 = 2;

    #[cfg(any(target_arch = "riscv32", target_arch = "riscv64"))]
    unsafe {
        core::arch::asm!(
            "li {n}, 2",
            "add {n}, {n}, {n}",
            n = inout(reg) n,
        );
    }

    #[cfg(target_arch = "x86_64")]
    unsafe {
        core::arch::asm!(
            "mov {n}, 2",
            "add {n}, {n}, {n}",
            n = inout(reg) n,
        );
    }
    n
}

按照 ISA 语义，此程序将始终返回 4，这是计算 2+2 的结果。挑战的重点是制作一个输出为 5 的执行证明！

修改后的 Jolt 库

readme.txt 文件解释了获取修改后的 Jolt 库所采取的步骤。

git clone git@github.com:a16z/jolt.git
cd jolt

## just the latest commit at time of writing
git checkout 0cc7aa31981ff8503fe256706d2aa9c320abd1cd
git apply ../diff.patch

Jolt 存储库按原样获取自上次提交（在编写挑战时），并对其应用了一个补丁。该补丁可以在 diff.patch 文件中找到：它从 jolt-core/src/r1cs/jolt_constraints.rs 文件中删除了一些行。

diff --git a/jolt-core/src/r1cs/jolt_constraints.rs b/jolt-core/src/r1cs/jolt_constraints.rs
index 5fb0d871..295dce32 100644
--- a/jolt-core/src/r1cs/jolt_constraints.rs
+++ b/jolt-core/src/r1cs/jolt_constraints.rs
@@ -289,13 +289,8 @@ impl&lt;F: JoltField> R1CSConstraintBuilder&lt;F> for UniformJoltConstraints {

         // if (rd != 0 && update_rd_with_lookup_output == 1) constrain(rd_val == LookupOutput)
         // if (rd != 0 && is_jump_instr == 1) constrain(rd_val == 4 * PC)
--        let rd_nonzero_and_lookup_to_rd =
-+        let _rd_nonzero_and_lookup_to_rd =
+            cs.allocate_prod(JoltIn::Bytecode_RD, JoltIn::OpFlags_LookupOutToRd);
--        cs.constrain_eq_conditional(
--            rd_nonzero_and_lookup_to_rd,
--            JoltIn::RD_Write,
--            JoltIn::LookupOutput,
--        );
  let rd_nonzero_and_jmp = cs.allocate_prod(JoltIn::Bytecode_RD, JoltIn::OpFlags_IsJmp);
         let lhs = JoltIn::Bytecode_ELFAddress + (PC_START_ADDRESS - PC_NOOP_SHIFT);
         let rhs = JoltIn::RD_Write;

总结

要解决这个挑战，我们需要向服务器提供访客程序的执行证明，输出为 5。为了做到这一点，我们需要利用 Jolt 已被修改并且可能不再健全的事实。

补丁分析

该补丁删除了 R1CS 组件中的一个约束，让我们仔细看看被删除的约束。

cs.constrain_eq_conditional(
    rd_nonzero_and_lookup_to_rd,
    JoltIn::RD_Write,
    JoltIn::LookupOutput,
);

如果第一个参数设置为 1，则 constrain_eq_conditional 函数会将第二个和第三个参数之间的相等约束添加到 R1CS 约束系统中。粗略地说，发出的约束等效于以下等式。

cs.constrain_eq_conditional(condition, left, right);
// condition  * (left - right) == 0

上面几行还有一个有用的注释，解释了约束。

// if (rd != 0 && update_rd_with_lookup_output == 1) constrain(rd_val == LookupOutput)
cs.constrain_eq_conditional(
    rd_nonzero_and_lookup_to_rd,
    JoltIn::RD_Write,
    JoltIn::LookupOutput,
);

RD_Write 值来自读写内存组件，它表示写入输出寄存器的内存值。相反，LookupOutput 值来自指令查找组件，它表示查找参数“返回”的输出值，该参数执行指令执行检查。约束的目标是在这两个值之间提供粘合。一个直观的解释如下。

如果指令应该将其结果写入寄存器，并且如果输出寄存器不为零，则写入输出寄存器的值应等于执行查找参数的结果。

删除了此约束后，利用思路很简单：制作一个执行轨迹，其中对 2 和 2 求和的 add 指令，不是将值 4 写回输出寄存器，而是写入值 5。在生成的轨迹中：

查找参数将返回 4，因为该指令是 add 且操作数值均为 2，但是
写回输出寄存器的值将为 5。

由于删除了强制这两个值相等的约束，因此该轨迹将被接受。然后，程序将继续正常运行并返回计算出的值，因此最终修改后的执行轨迹的输出将恰好为 5！

制作证明

一旦我们了解了所有活动的部件，实际的利用就非常容易：我们只需要在 tracer 模块中修补 Jolt，该模块是生成执行轨迹的模块。我们修改了 jolt/tracer/src/emulator/cpu.rs 文件，更改了 ADD 操作仿真的语义：如果操作数均为 2，则将值 5 写回输出寄存器。

Instruction {
    mask: 0xfe00707f,
    data: 0x00000033,
    name: "ADD",
    operation: |cpu, word, _address| {
        let f = parse_format_r(word);

        // If the operands are both 2, then write 5 in the output register
        // otherwise apply normal addition semantics
        if cpu.x[f.rs1] == 2 && cpu.x[f.rs2] == 2 {
            cpu.x[f.rd] = cpu.sign_extend(5);
        } else {
            cpu.x[f.rd] = cpu.sign_extend(cpu.x[f.rs1].wrapping_add(cpu.x[f.rs2]));
        }
        Ok(())
    },
    disassemble: dump_format_r,
    trace: Some(trace_r),
},

我们可以打印出来的一个有趣的事情是在执行 add {n}, {n}, {n} 指令的确切步骤中的执行轨迹。这里要注意的主要部分是内存操作：该指令是 ADD，两个操作数都等于 2，因此有两个读取操作，但是然后有一个写入操作到具有值 5 的同一寄存器！

Trace[5]
JoltTraceStep {
    instruction_lookup: Some(ADD(ADDInstruction(2, 2))),
    bytecode_row: BytecodeRow {
        address: 2147483672,
        bitflags: 17448304640,
        rd: 10,
        rs1: 10,
        rs2: 10,
        imm: 0,
        virtual_sequence_remaining: None
    },
    memory_ops: [Read(10), Read(10), Write(10, 5), Read(0), Read(0), Read(0), Read(0)]
}

我们还可以直接打印 R1CS 系统的输入，这些输入存储在 R1CSInputs 结构中。正如我们所看到的，查找正确返回 4，但是写入输出寄存器的值是 5。

pc[7] = 9
bytecode_a[7] = 9
bytecode_v[7] = 9
memreg_a_rw[7] = 0
memreg_v_reads[7] = 2
memreg_v_writes[7] = 5
chunks_x[7] = 0
chunks_y[7] = 0
chunks_query[7] = 0
lookup_outputs[7] = 4
circuit_flags_bits[7] = 0
instruction_flags_bits[7] = 1

总而言之，主要的求解器 Rust 程序非常简单（使用修改后的 Jolt 库）。运行此程序将输出一个证明，该证明提供给服务器将返回 flag！

use jolt_sdk::RV32IHyraxProof;

pub fn main() {
    let (prove_two_plus_two, verify_two_plus_two) = guest::build_two_plus_two();
    let (output, proof_gen) = prove_two_plus_two();
    println!("Proof generated! {}", output);
    let proof_bytes = proof_gen.serialize_to_bytes().unwrap();
    println!("{}", hex::encode(&proof_bytes));
}

这是一种解决挑战的方法，但实际上删除该特定约束提供了一个更强大的原语：我们可以为每个将其结果写回寄存器的指令将任意值写入寄存器！