Skip to content

refactor(prover): centralize u64 limb decomposition (dword_wl/dword_hl) #697

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
MauroToscano wants to merge 2 commits into
base: main
Choose a base branch
from
Open

refactor(prover): centralize u64 limb decomposition (dword_wl/dword_hl) #697

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
38a3b73
refactor(prover): centralize u64 limb decomposition into dword_wl/dwo…
MauroToscano Jun 22, 2026
e209613
refactor(prover): single-source the limb decomposition in remaining s…
MauroToscano Jun 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 11 additions & 18 deletions prover/src/tables/branch.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}
use stark::table::TableView;
use stark::trace::TraceTable;

use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, SHIFT_16, alu_op};
use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, SHIFT_16, alu_op, dword_wl};

// =========================================================================
// Column indices for BRANCH table
Expand Down Expand Up @@ -173,17 +173,10 @@ pub fn generate_branch_trace(
for (row_idx, (op, multiplicity)) in unique_ops.iter().enumerate() {
let base = row_idx * cols::NUM_COLUMNS;

// Extract pc as DWordWL: [Word, Word]
let pc_0 = (op.pc & 0xFFFF_FFFF) as u32;
let pc_1 = (op.pc >> 32) as u32;

// Extract offset as DWordWL: [Word, Word]
let offset_0 = (op.offset & 0xFFFF_FFFF) as u32;
let offset_1 = (op.offset >> 32) as u32;

// Extract register as DWordWL: [Word, Word]
let register_0 = (op.register & 0xFFFF_FFFF) as u32;
let register_1 = (op.register >> 32) as u32;
// Extract pc, offset, register as DWordWL: [Word, Word]
let [pc_0, pc_1] = dword_wl(op.pc);
let [offset_0, offset_1] = dword_wl(op.offset);
let [register_0, register_1] = dword_wl(op.register);

// Compute next_pc
let next_pc_unmasked = op.compute_next_pc_unmasked();
Expand All @@ -203,12 +196,12 @@ pub fn generate_branch_trace(
let next_pc_high_2 = ((next_pc >> 48) & 0xFFFF) as u16;

// Store columns
data[base + cols::PC_0] = FE::from(pc_0 as u64);
data[base + cols::PC_1] = FE::from(pc_1 as u64);
data[base + cols::OFFSET_0] = FE::from(offset_0 as u64);
data[base + cols::OFFSET_1] = FE::from(offset_1 as u64);
data[base + cols::REGISTER_0] = FE::from(register_0 as u64);
data[base + cols::REGISTER_1] = FE::from(register_1 as u64);
data[base + cols::PC_0] = pc_0;
data[base + cols::PC_1] = pc_1;
data[base + cols::OFFSET_0] = offset_0;
data[base + cols::OFFSET_1] = offset_1;
data[base + cols::REGISTER_0] = register_0;
data[base + cols::REGISTER_1] = register_1;
data[base + cols::JALR] = FE::from(if op.jalr { 1u64 } else { 0u64 });
data[base + cols::NEXT_PC_HIGH_0] = FE::from(next_pc_high_0 as u64);
data[base + cols::NEXT_PC_HIGH_1] = FE::from(next_pc_high_1 as u64);
Expand Down
35 changes: 20 additions & 15 deletions prover/src/tables/commit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ use stark::trace::TraceTable;

use crate::constraints::templates::{AddConstraint, AddOperand};

use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField};
use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, dword_hl, dword_wl};

// =========================================================================
// Column indices for COMMIT table
Expand Down Expand Up @@ -170,37 +170,42 @@ pub fn generate_commit_trace(
let base = row_idx * cols::NUM_COLUMNS;

// Timestamp (DWordWL)
data[base + cols::TIMESTAMP_0] = FE::from(op.timestamp & 0xFFFF_FFFF);
data[base + cols::TIMESTAMP_1] = FE::from(op.timestamp >> 32);
let [ts0, ts1] = dword_wl(op.timestamp);
data[base + cols::TIMESTAMP_0] = ts0;
data[base + cols::TIMESTAMP_1] = ts1;

// Index (BaseField)
data[base + cols::INDEX] = FE::from(op.index);

// Address (DWordWL)
data[base + cols::ADDRESS_0] = FE::from(op.address & 0xFFFF_FFFF);
data[base + cols::ADDRESS_1] = FE::from(op.address >> 32);
let [addr0, addr1] = dword_wl(op.address);
data[base + cols::ADDRESS_0] = addr0;
data[base + cols::ADDRESS_1] = addr1;

// address_incr = address + 1 (DWordHL: 4 halfwords)
let address_incr = op.address.wrapping_add(1);
data[base + cols::ADDRESS_INCR_0] = FE::from(address_incr & 0xFFFF);
data[base + cols::ADDRESS_INCR_1] = FE::from((address_incr >> 16) & 0xFFFF);
data[base + cols::ADDRESS_INCR_2] = FE::from((address_incr >> 32) & 0xFFFF);
data[base + cols::ADDRESS_INCR_3] = FE::from((address_incr >> 48) & 0xFFFF);
let [ai0, ai1, ai2, ai3] = dword_hl(address_incr);
data[base + cols::ADDRESS_INCR_0] = ai0;
data[base + cols::ADDRESS_INCR_1] = ai1;
data[base + cols::ADDRESS_INCR_2] = ai2;
data[base + cols::ADDRESS_INCR_3] = ai3;

// Count (DWordWL)
data[base + cols::COUNT_0] = FE::from(op.count & 0xFFFF_FFFF);
data[base + cols::COUNT_1] = FE::from(op.count >> 32);
let [cnt0, cnt1] = dword_wl(op.count);
data[base + cols::COUNT_0] = cnt0;
data[base + cols::COUNT_1] = cnt1;

// count_decr: if count == 0, use 0xFFFF_FFFF_FFFF_FFFF; else count - 1
let count_decr = if op.count == 0 {
u64::MAX
} else {
op.count - 1
};
data[base + cols::COUNT_DECR_0] = FE::from(count_decr & 0xFFFF);
data[base + cols::COUNT_DECR_1] = FE::from((count_decr >> 16) & 0xFFFF);
data[base + cols::COUNT_DECR_2] = FE::from((count_decr >> 32) & 0xFFFF);
data[base + cols::COUNT_DECR_3] = FE::from((count_decr >> 48) & 0xFFFF);
let [cd0, cd1, cd2, cd3] = dword_hl(count_decr);
data[base + cols::COUNT_DECR_0] = cd0;
data[base + cols::COUNT_DECR_1] = cd1;
data[base + cols::COUNT_DECR_2] = cd2;
data[base + cols::COUNT_DECR_3] = cd3;

// Control bits
data[base + cols::FIRST] = FE::from(op.first as u64);
Expand Down
43 changes: 26 additions & 17 deletions prover/src/tables/cpu.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,9 @@
//! JALR bit (the memory-width bits are 0), so `mem_flags ∈ {0,1} = JALR` and the
//! `mem_flags` column is used directly as `JALR` wherever it is gated by `BRANCH`.

use super::types::{BusId, DecodeEntry, FE, GoldilocksExtension, GoldilocksField, alu_op};
use super::types::{
BusId, DecodeEntry, FE, GoldilocksExtension, GoldilocksField, alu_op, dword_hl, dword_wl,
};
use crate::Error;
use executor::vm::{
instruction::{decoding::Instruction, execution::SyscallNumbers},
Expand Down Expand Up @@ -451,8 +453,9 @@ pub fn generate_cpu_trace(
let effective = |flag: bool| (!word && flag) as u64;

data[base + cols::TIMESTAMP] = FE::from(op.timestamp);
data[base + cols::PC_0] = FE::from(op.decode.pc & 0xFFFF_FFFF);
data[base + cols::PC_1] = FE::from(op.decode.pc >> 32);
let [pc0, pc1] = dword_wl(op.decode.pc);
data[base + cols::PC_0] = pc0;
data[base + cols::PC_1] = pc1;

// rs1/rs2/rd and read/write flags are only present on non-word rows.
let (rs1, rs2, rd) = if word {
Expand Down Expand Up @@ -480,8 +483,9 @@ pub fn generate_cpu_trace(
(op.decode.imm, op.rvd, op.rv1, op.rv2, op.arg2, op.res)
};

data[base + cols::IMM_0] = FE::from(imm & 0xFFFF_FFFF);
data[base + cols::IMM_1] = FE::from(imm >> 32);
let [imm0, imm1] = dword_wl(imm);
data[base + cols::IMM_0] = imm0;
data[base + cols::IMM_1] = imm1;

data[base + cols::HALF_INSTRUCTION_LENGTH] = FE::from(f.half_instruction_length as u64);
data[base + cols::WORD_INSTR] = FE::from(word as u64);
Expand All @@ -495,23 +499,28 @@ pub fn generate_cpu_trace(
data[base + cols::BRANCH] = FE::from(effective(f.branch));
data[base + cols::ECALL] = FE::from(effective(f.ecall));

data[base + cols::NEXT_PC_0] = FE::from(op.next_pc & 0xFFFF_FFFF);
data[base + cols::NEXT_PC_1] = FE::from(op.next_pc >> 32);
let [npc0, npc1] = dword_wl(op.next_pc);
data[base + cols::NEXT_PC_0] = npc0;
data[base + cols::NEXT_PC_1] = npc1;

data[base + cols::RVD_0] = FE::from(rvd & 0xFFFF_FFFF);
data[base + cols::RVD_1] = FE::from(rvd >> 32);
let [rvd0, rvd1] = dword_wl(rvd);
data[base + cols::RVD_0] = rvd0;
data[base + cols::RVD_1] = rvd1;

// rv1/rv2/arg2 as DWordWL (2 × 32-bit words).
data[base + cols::RV1_0] = FE::from(rv1 & 0xFFFF_FFFF);
data[base + cols::RV1_1] = FE::from(rv1 >> 32);
data[base + cols::RV2_0] = FE::from(rv2 & 0xFFFF_FFFF);
data[base + cols::RV2_1] = FE::from(rv2 >> 32);
data[base + cols::ARG2_0] = FE::from(arg2 & 0xFFFF_FFFF);
data[base + cols::ARG2_1] = FE::from(arg2 >> 32);
let [rv1_0, rv1_1] = dword_wl(rv1);
data[base + cols::RV1_0] = rv1_0;
data[base + cols::RV1_1] = rv1_1;
let [rv2_0, rv2_1] = dword_wl(rv2);
data[base + cols::RV2_0] = rv2_0;
data[base + cols::RV2_1] = rv2_1;
let [arg2_0, arg2_1] = dword_wl(arg2);
data[base + cols::ARG2_0] = arg2_0;
data[base + cols::ARG2_1] = arg2_1;

// res as DWordHL (4 × 16-bit halves).
for i in 0..4 {
data[base + cols::RES[i]] = FE::from((res >> (i * 16)) & 0xFFFF);
for (&col, limb) in cols::RES.iter().zip(dword_hl(res)) {
data[base + col] = limb;
}

data[base + cols::BRANCH_COND] = FE::from(op.branch_cond as u64);
Expand Down
42 changes: 25 additions & 17 deletions prover/src/tables/cpu32.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,8 @@ use stark::table::TableView;
use stark::trace::TraceTable;

use super::types::{
BusId, FE, GoldilocksExtension, GoldilocksField, SHIFT_16, alu_op, packed_decode_shrunk,
BusId, FE, GoldilocksExtension, GoldilocksField, SHIFT_16, alu_op, dword_hl, dword_wl,
packed_decode_shrunk,
};
use crate::constraints::templates::{AddConstraint, AddOperand, new_is_bit_constraints};

Expand Down Expand Up @@ -204,10 +205,12 @@ pub fn generate_cpu32_trace(
let aux = op.compute_aux();

// Inputs
data[base + cols::TIMESTAMP_0] = FE::from(op.timestamp & 0xFFFF_FFFF);
data[base + cols::TIMESTAMP_1] = FE::from(op.timestamp >> 32);
data[base + cols::PC_0] = FE::from(op.pc & 0xFFFF_FFFF);
data[base + cols::PC_1] = FE::from(op.pc >> 32);
let [ts0, ts1] = dword_wl(op.timestamp);
data[base + cols::TIMESTAMP_0] = ts0;
data[base + cols::TIMESTAMP_1] = ts1;
let [pc0, pc1] = dword_wl(op.pc);
data[base + cols::PC_0] = pc0;
data[base + cols::PC_1] = pc1;

// rv1 as DWordWHH: [Half, Half, Word]
data[base + cols::RS1] = FE::from(op.rs1 as u64);
Expand All @@ -216,8 +219,9 @@ pub fn generate_cpu32_trace(
data[base + cols::RV1_1] = FE::from((op.rv1 >> 16) & 0xFFFF);
data[base + cols::RV1_2] = FE::from(op.rv1 >> 32);
data[base + cols::RV1_SIGN] = FE::from(aux.rv1_sign as u64);
data[base + cols::ARG1_0] = FE::from(aux.arg1 & 0xFFFF_FFFF);
data[base + cols::ARG1_1] = FE::from(aux.arg1 >> 32);
let [arg1_0, arg1_1] = dword_wl(aux.arg1);
data[base + cols::ARG1_0] = arg1_0;
data[base + cols::ARG1_1] = arg1_1;

// rv2 as DWordWHH
data[base + cols::RS2] = FE::from(op.rs2 as u64);
Expand All @@ -226,23 +230,27 @@ pub fn generate_cpu32_trace(
data[base + cols::RV2_1] = FE::from((op.rv2 >> 16) & 0xFFFF);
data[base + cols::RV2_2] = FE::from(op.rv2 >> 32);
data[base + cols::RV2_SIGN] = FE::from(aux.rv2_sign as u64);
data[base + cols::IMM_0] = FE::from(op.imm & 0xFFFF_FFFF);
data[base + cols::IMM_1] = FE::from(op.imm >> 32);
data[base + cols::ARG2_0] = FE::from(aux.arg2 & 0xFFFF_FFFF);
data[base + cols::ARG2_1] = FE::from(aux.arg2 >> 32);
let [imm0, imm1] = dword_wl(op.imm);
data[base + cols::IMM_0] = imm0;
data[base + cols::IMM_1] = imm1;
let [arg2_0, arg2_1] = dword_wl(aux.arg2);
data[base + cols::ARG2_0] = arg2_0;
data[base + cols::ARG2_1] = arg2_1;

// res as DWordHL: 4 halves
data[base + cols::RES_0] = FE::from(op.res & 0xFFFF);
data[base + cols::RES_1] = FE::from((op.res >> 16) & 0xFFFF);
data[base + cols::RES_2] = FE::from((op.res >> 32) & 0xFFFF);
data[base + cols::RES_3] = FE::from((op.res >> 48) & 0xFFFF);
let [res0, res1, res2, res3] = dword_hl(op.res);
data[base + cols::RES_0] = res0;
data[base + cols::RES_1] = res1;
data[base + cols::RES_2] = res2;
data[base + cols::RES_3] = res3;
data[base + cols::RES_SIGN] = FE::from(aux.res_sign as u64);

// rd write
data[base + cols::RD] = FE::from(op.rd as u64);
data[base + cols::WRITE_REGISTER] = FE::from(op.write_register as u64);
data[base + cols::RVD_0] = FE::from(aux.rvd & 0xFFFF_FFFF);
data[base + cols::RVD_1] = FE::from(aux.rvd >> 32);
let [rvd0, rvd1] = dword_wl(aux.rvd);
data[base + cols::RVD_0] = rvd0;
data[base + cols::RVD_1] = rvd1;

// ALU control
data[base + cols::ALU] = FE::from(op.alu as u64);
Expand Down
62 changes: 37 additions & 25 deletions prover/src/tables/decode.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ use stark::proof::options::ProofOptions;
use stark::prover::evaluate_polynomial_on_lde_domain;
use stark::trace::{TraceTable, columns2rows};

use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField};
use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, dword_wl};

// Re-export DecodeEntry from types for backwards compatibility
pub use super::types::DecodeEntry;
Expand Down Expand Up @@ -135,40 +135,46 @@ pub fn generate_decode_trace(
let base = row_idx * cols::NUM_COLUMNS;

// PC as DWordWL
data[base + cols::PC_0] = FE::from(entry.pc & 0xFFFF_FFFF);
data[base + cols::PC_1] = FE::from(entry.pc >> 32);
let [pc0, pc1] = dword_wl(entry.pc);
data[base + cols::PC_0] = pc0;
data[base + cols::PC_1] = pc1;

// packed_decode
data[base + cols::PACKED_DECODE] = FE::from(entry.packed_decode());

// imm as DWordWL
data[base + cols::IMM_0] = FE::from(entry.imm & 0xFFFF_FFFF);
data[base + cols::IMM_1] = FE::from(entry.imm >> 32);
let [imm0, imm1] = dword_wl(entry.imm);
data[base + cols::IMM_0] = imm0;
data[base + cols::IMM_1] = imm1;

// MU = 0 (already zero from vec initialization)
}

// Write CPU padding entry (pc=1, all flags=0)
{
let base = cpu_padding_row * cols::NUM_COLUMNS;
data[base + cols::PC_0] = FE::from(cpu_padding_entry.pc & 0xFFFF_FFFF);
data[base + cols::PC_1] = FE::from(cpu_padding_entry.pc >> 32);
let [pc0, pc1] = dword_wl(cpu_padding_entry.pc);
data[base + cols::PC_0] = pc0;
data[base + cols::PC_1] = pc1;
data[base + cols::PACKED_DECODE] = FE::from(cpu_padding_entry.packed_decode());
data[base + cols::IMM_0] = FE::from(cpu_padding_entry.imm & 0xFFFF_FFFF);
data[base + cols::IMM_1] = FE::from(cpu_padding_entry.imm >> 32);
let [imm0, imm1] = dword_wl(cpu_padding_entry.imm);
data[base + cols::IMM_0] = imm0;
data[base + cols::IMM_1] = imm1;
}

// Fill padding rows with the DECODE padding pattern: odd pc=1, all flags 0
// (unprovable as a fetch target; same row the CPU pads to).
let padding_entry = DecodeEntry::padding_entry();
let [pad_pc0, pad_pc1] = dword_wl(padding_entry.pc);
let [pad_imm0, pad_imm1] = dword_wl(padding_entry.imm);
for row_idx in num_entries..num_rows {
let base = row_idx * cols::NUM_COLUMNS;

data[base + cols::PC_0] = FE::from(padding_entry.pc & 0xFFFF_FFFF);
data[base + cols::PC_1] = FE::from(padding_entry.pc >> 32);
data[base + cols::PC_0] = pad_pc0;
data[base + cols::PC_1] = pad_pc1;
data[base + cols::PACKED_DECODE] = FE::from(padding_entry.packed_decode());
data[base + cols::IMM_0] = FE::from(padding_entry.imm & 0xFFFF_FFFF);
data[base + cols::IMM_1] = FE::from(padding_entry.imm >> 32);
data[base + cols::IMM_0] = pad_imm0;
data[base + cols::IMM_1] = pad_imm1;
// MU = 0 for padding rows (already zero from vec initialization)
}

Expand Down Expand Up @@ -407,32 +413,38 @@ fn build_decode_table(
// Fill actual entries
for (row_idx, entry) in entries.iter().enumerate() {
let base = row_idx * cols::NUM_COLUMNS;
data[base + cols::PC_0] = FE::from(entry.pc & 0xFFFF_FFFF);
data[base + cols::PC_1] = FE::from(entry.pc >> 32);
let [pc0, pc1] = dword_wl(entry.pc);
data[base + cols::PC_0] = pc0;
data[base + cols::PC_1] = pc1;
data[base + cols::PACKED_DECODE] = FE::from(entry.packed_decode());
data[base + cols::IMM_0] = FE::from(entry.imm & 0xFFFF_FFFF);
data[base + cols::IMM_1] = FE::from(entry.imm >> 32);
let [imm0, imm1] = dword_wl(entry.imm);
data[base + cols::IMM_0] = imm0;
data[base + cols::IMM_1] = imm1;
}

// Write CPU padding entry
{
let base = cpu_padding_row * cols::NUM_COLUMNS;
data[base + cols::PC_0] = FE::from(cpu_padding_entry.pc & 0xFFFF_FFFF);
data[base + cols::PC_1] = FE::from(cpu_padding_entry.pc >> 32);
let [pc0, pc1] = dword_wl(cpu_padding_entry.pc);
data[base + cols::PC_0] = pc0;
data[base + cols::PC_1] = pc1;
data[base + cols::PACKED_DECODE] = FE::from(cpu_padding_entry.packed_decode());
data[base + cols::IMM_0] = FE::from(cpu_padding_entry.imm & 0xFFFF_FFFF);
data[base + cols::IMM_1] = FE::from(cpu_padding_entry.imm >> 32);
let [imm0, imm1] = dword_wl(cpu_padding_entry.imm);
data[base + cols::IMM_0] = imm0;
data[base + cols::IMM_1] = imm1;
}

// Fill padding rows with DECODE padding pattern
let padding_entry = DecodeEntry::padding_entry();
let [pad_pc0, pad_pc1] = dword_wl(padding_entry.pc);
let [pad_imm0, pad_imm1] = dword_wl(padding_entry.imm);
for row_idx in num_entries..num_rows {
let base = row_idx * cols::NUM_COLUMNS;
data[base + cols::PC_0] = FE::from(padding_entry.pc & 0xFFFF_FFFF);
data[base + cols::PC_1] = FE::from(padding_entry.pc >> 32);
data[base + cols::PC_0] = pad_pc0;
data[base + cols::PC_1] = pad_pc1;
data[base + cols::PACKED_DECODE] = FE::from(padding_entry.packed_decode());
data[base + cols::IMM_0] = FE::from(padding_entry.imm & 0xFFFF_FFFF);
data[base + cols::IMM_1] = FE::from(padding_entry.imm >> 32);
data[base + cols::IMM_0] = pad_imm0;
data[base + cols::IMM_1] = pad_imm1;
}

TraceTable::new_main(data, cols::NUM_COLUMNS, 1)
Expand Down
Loading
Loading