Jolt's output differs after changes to unexecuted code
## Description
When executing the following guest and host code provided, I noticed a weird behavior regarding the output. First, in theory `f1` and `f2` should be semantically equivalent. So I was surprised when getting `4001` as an response instead of the expected `0`. Trying to minimize the example, I discovered that modifying the return values, code structure, as well as removing dead code (code after the supposed exiting statement) changes the guest output.
## Example
First if I execute the code as is, I get:
```bash
$> cargo run --release
...
Output: 4001
```
Now if I comment out the following line
```rust
/* ... */
if f1_out0 ^ f2_out0 != 0 { return 4000_u32; }
if f1_out1 ^ f2_out1 != 0 { return 4001_u32; }
// if f1_out2 ^ f2_out2 { return 4002_u32; }
/* ... */
```
and execute it again, it changes the output:
```bash
$> cargo run --release
...
Output: 0
```
## Sources
**main.rs**
```rust
pub fn main() {
let inputs: [u32; 6] = [0, 4221631021, 0, 0, 0, 3827817732];
let target_dir = "/tmp/jolt-guest-targets";
let mut program = guest::compile_test(target_dir);
let prover_preprocessing = guest::preprocess_prover_test(&mut program);
let verifier_preprocessing = guest::verifier_preprocessing_from_prover_test(&prover_preprocessing);
let prove_test = guest::build_prover_test(program, prover_preprocessing);
let verify_test = guest::build_verifier_test(verifier_preprocessing);
let (output, proof, program_io) = prove_test(inputs.clone(), inputs.clone());
if !verify_test(inputs.clone(), inputs.clone(), output, program_io.panic, proof) {
panic!("verifier failed!");
}
println!("Output: {:?}", output);
}
```
**lib.rs**
```rust
#![cfg_attr(feature = "guest", no_std)]
macro_rules! mulhu {
($a:expr, $b:expr) => {{
let result: u32;
unsafe {
core::arch::asm!(
"mulhu {result}, {a}, {b}",
result = out(reg) result,
a = in(reg) $a,
b = in(reg) $b,
);
}
result
}}
}
macro_rules! sb_lb {
($addr:expr, $val:expr) => {{
let result: u32;
unsafe {
core::arch::asm!(
"sb {val}, 0({addr})",
"lb {result}, 0({addr})",
val = in(reg) $val,
addr = in(reg) $addr,
result = out(reg) result,
);
}
result
}}
}
macro_rules! or {
($a:expr, $b:expr) => {{
let result: u32;
unsafe {
core::arch::asm!(
"or {result}, {a}, {b}",
result = out(reg) result,
a = in(reg) $a,
b = in(reg) $b,
);
}
result
}}
}
macro_rules! srai {
($a:expr, $shamt:literal) => {{
let result: u32;
unsafe {
core::arch::asm!(
"srai {result}, {a}, {imm}",
result = out(reg) result,
a = in(reg) $a,
imm = const $shamt,
);
}
result
}};
}
macro_rules! jal {
() => {{
let result: u32;
unsafe {
core::arch::asm!(
"jal x0, 3f",
"2: addi {result}, x0, 0",
"3: addi {result}, x0, 1",
result = out(reg) result,
);
}
result
}}
}
#[allow(non_snake_case, unused_comparisons, unused_parens, unused_variables)]
pub fn f1(in0: bool, in1: u32, in2: u32, in3: bool, in4: bool, in5: u32) -> (u32, u32, bool, u32, u32, bool, u32) {
let mut memory: [u8; 32] = [0; 32];
let memory_ptr: *mut u8 = memory.as_mut_ptr();
let out0 = in5;
let var0 = (if false { out0 } else { in1 });
let var1 = (2070842490_u32 - var0);
let var2 = (in1 == 0_u32);
let var3 = (if var2 { 1_u32 } else { in1 });
let var4 = (var1 % var3);
let var5 = (! var4);
let out1 = mulhu!(out0, var5);
let var6 = sb_lb!(memory_ptr, 3462559791_u32);
let var7 = (var6 * 1_u32);
let var8 = (out0 | var7);
let var9 = (in5 & 372716253_u32);
let var10 = (var8 != var9);
let out2 = (if in0 { var10 } else { false });
let out3 = 4108507340_u32;
let out4 = 1719129879_u32.pow(1_u32);
let var11 = or!(in2, out1);
let var12 = (if false { 4294967295_u32 } else { out0 });
let var13 = (if false { var11 } else { var12 });
let var14 = (! 4294967295_u32);
let var15 = (var13 + var14);
let var16 = (var15 <= in1);
let out5 = (! var16);
let var17 = srai!(3668900192_u32, 29_u32);
let var18 = (! in3);
let var19 = (var18 && in3);
let var20 = (! in3);
let var21 = (var20 && in3);
let var22 = (var19 || var21);
let var23 = (in1 < in1);
let var24 = (if var22 { false } else { var23 });
let var25 = jal!();
let var26 = (if true { in1 } else { 1317969159_u32 });
let var27 = (if false { 1509152803_u32 } else { var26 });
let var28 = (if var24 { var25 } else { var27 });
let var29 = srai!(in1, 0_u32);
let var30 = (var28 - var29);
let out6 = (var17 & var30);
return (out0, out1, out2, out3, out4, out5, out6);
}
#[allow(non_snake_case, unused_comparisons, unused_parens, unused_variables)]
pub fn f2(in0: bool, in1: u32, in2: u32, in3: bool, in4: bool, in5: u32) -> (u32, u32, bool, u32, u32, bool, u32) {
let mut memory: [u8; 32] = [0; 32];
let memory_ptr: *mut u8 = memory.as_mut_ptr();
let out0 = in5;
let var0 = (if false { out0 } else { in1 });
let var1 = (2070842490_u32 - var0);
let var2 = (in1 == 0_u32);
let var3 = (if var2 { 1_u32 } else { in1 });
let var4 = (var1 % var3);
let var5 = (! var4);
let out1 = mulhu!(out0, var5);
let var6 = sb_lb!(memory_ptr, 3462559791_u32);
let var7 = (var6 * 1_u32);
let var8 = (var7 * 1_u32);
let var9 = (out0 | var8);
let var10 = (in5 & 372716253_u32);
let var11 = (var9 != var10);
let out2 = (if in0 { var11 } else { false });
let out3 = 4108507340_u32;
let out4 = 1719129879_u32.pow(1_u32);
let var12 = or!(in2, out1);
let var13 = (if false { 4294967295_u32 } else { out0 });
let var14 = (if false { var12 } else { var13 });
let var15 = (! 4294967295_u32);
let var16 = (var14 + var15);
let var17 = (var16 <= in1);
let out5 = (! var17);
let var18 = srai!(3668900192_u32, 29_u32);
let var19 = (! in3);
let var20 = (var19 && in3);
let var21 = (! in3);
let var22 = (var21 && in3);
let var23 = (var20 || var22);
let var24 = (in1 < in1);
let var25 = (if var23 { false } else { var24 });
let var26 = jal!();
let var27 = (if true { in1 } else { 1317969159_u32 });
let var28 = (if false { 1509152803_u32 } else { var27 });
let var29 = (if var25 { var26 } else { var28 });
let var30 = srai!(in1, 0_u32);
let var31 = (var29 - var30);
let out6 = (var18 & var31);
return (out0, out1, out2, out3, out4, out5, out6);
}
#[jolt::provable(guest_only, memory_size = 10240, max_trace_length = 65536)]
fn test(xs: [u32; 6], ys: [u32; 6]) -> u32 {
let f1_in0: bool = xs[0] == 0_u32;
let f1_in1: u32 = xs[1];
let f1_in2: u32 = xs[2];
let f1_in3: bool = xs[3] == 0_u32;
let f1_in4: bool = xs[4] == 0_u32;
let f1_in5: u32 = xs[5];
let f2_in0: bool = ys[0] == 0_u32;
let f2_in1: u32 = ys[1];
let f2_in2: u32 = ys[2];
let f2_in3: bool = ys[3] == 0_u32;
let f2_in4: bool = ys[4] == 0_u32;
let f2_in5: u32 = ys[5];
let (f1_out0, f1_out1, f1_out2, f1_out3, f1_out4, f1_out5, f1_out6) = f1(f1_in0, f1_in1, f1_in2, f1_in3, f1_in4, f1_in5);
let (f2_out0, f2_out1, f2_out2, f2_out3, f2_out4, f2_out5, f2_out6) = f2(f2_in0, f2_in1, f2_in2, f2_in3, f2_in4, f2_in5);
if f1_out0 ^ f2_out0 != 0 { return 4000_u32; }
if f1_out1 ^ f2_out1 != 0 { return 4001_u32; }
if f1_out2 ^ f2_out2 { return 4002_u32; }
0_u32
}
```
---
* tested commits:
- 34a9dda9cebdfa7f4d1a4236811b06bfc1a1ee08
- 0017138804dc69240b0d4f4aaf4f40dbd4101f4a
关闭于 2025-10-28 2 条评论