Reproduced against the local Rust Jolt checkout at 7dfe8a0f; the relevant files are unchanged from the reviewed e012da54 revision.
This report concerns row index 15 of Rust's stage-1 R1CS matrix.
Counterexample
Put this single instruction at 0x80000000, start the Rust CPU at that address, and trace its execution:
beq x0, x0, 0 # 0x00000063
The comparison is true. Rust's BEQ::exec sets the CPU's PC to the instruction's own address plus the immediate, which is again 0x80000000. On the next tracer iteration, Rust sees that the PC has not changed and stops. The branch executes once, so the trace contains one instruction row. It does not contain a second execution of the branch. That row passes build_trace_rows; the prover's cycle domain then has padding after it.
Honest witness
On the BEQ row, Rust's witness extractors give:
The CPU's final PC is 0x80000000, but that value is not copied into NextUnexpandedPC. The latter comes from the padding successor. Setting it to 0x80000000 would describe a second executed row that the terminating trace does not contain.
Failed constraint
Rust's constraint row requires, over the proof field Fr:
ShouldBranch × (NextUnexpandedPC − UnexpandedPC − Imm) = 0
The branch is taken, so ShouldBranch = 1 activates this constraint. It demands NextUnexpandedPC = UnexpandedPC + Imm = 0x80000000. The witness instead has NextUnexpandedPC = 0 because the next row is padding. Its local residual is:
1 × (0 − 0x80000000 − 0) = −0x80000000 ≠ 0
Reproduced against the local Rust Jolt checkout at
7dfe8a0f; the relevant files are unchanged from the reviewede012da54revision.This report concerns row index 15 of Rust's stage-1 R1CS matrix.
Counterexample
Put this single instruction at
0x80000000, start the Rust CPU at that address, and trace its execution:The comparison is true. Rust's
BEQ::execsets the CPU's PC to the instruction's own address plus the immediate, which is again0x80000000. On the next tracer iteration, Rust sees that the PC has not changed and stops. The branch executes once, so the trace contains one instruction row. It does not contain a second execution of the branch. That row passesbuild_trace_rows; the prover's cycle domain then has padding after it.Honest witness
On the
BEQrow, Rust's witness extractors give:ShouldBranch = 1:BEQhas theBranchinstruction flag, and comparingx0withx0gives lookup output1. See theBEQflags andShouldBranch::extract.UnexpandedPC = 0x80000000: this is the source instruction's address, recorded in the trace row and read byUnexpandedPc::extract.Imm = 0: the branch's immediate, read byImm::extract.NextUnexpandedPC = 0: this column reads the source address of the next trace row, not the CPU's PC after executing the branch. There is no next executed instruction. The witness backend supplies a default padding row, whose unexpanded PC is zero;NextUnexpandedPc::extractreads that successor.The CPU's final PC is
0x80000000, but that value is not copied intoNextUnexpandedPC. The latter comes from the padding successor. Setting it to0x80000000would describe a second executed row that the terminating trace does not contain.Failed constraint
Rust's constraint row requires, over the proof field
Fr:The branch is taken, so
ShouldBranch = 1activates this constraint. It demandsNextUnexpandedPC = UnexpandedPC + Imm = 0x80000000. The witness instead hasNextUnexpandedPC = 0because the next row is padding. Its local residual is: