Skip to content

Commit 57c8a48

Browse files
committed
Fix soundness: always generate CPU_BITWISE chunk, add Msb16 to bitwise
chip bus interactions, deduplicate padding calculation
1 parent 98e68ef commit 57c8a48

4 files changed

Lines changed: 37 additions & 55 deletions

File tree

prover/src/lib.rs

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,7 @@ impl TableCounts {
104104
pub fn validate(&self) -> Result<(), Error> {
105105
let checks = [
106106
("cpu", self.cpu),
107+
("cpu_bitwise", self.cpu_bitwise),
107108
("lt", self.lt),
108109
("memw", self.memw),
109110
("memw_aligned", self.memw_aligned),
@@ -218,11 +219,7 @@ impl VmAirs {
218219
for (air, trace) in self.cpus.iter().zip(traces.cpus.iter_mut()) {
219220
pairs.push((air, trace, &()));
220221
}
221-
for (air, trace) in self
222-
.cpu_bitwises
223-
.iter()
224-
.zip(traces.cpu_bitwises.iter_mut())
225-
{
222+
for (air, trace) in self.cpu_bitwises.iter().zip(traces.cpu_bitwises.iter_mut()) {
226223
pairs.push((air, trace, &()));
227224
}
228225
for (air, trace) in self.lts.iter().zip(traces.lts.iter_mut()) {

prover/src/tables/cpu.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2067,6 +2067,7 @@ pub fn bus_interactions_bitwise_chip() -> Vec<BusInteraction> {
20672067
BusId::AndByte.into(),
20682068
BusId::OrByte.into(),
20692069
BusId::XorByte.into(),
2070+
BusId::Msb16.into(), // ANDW/ORW/XORW set word_instr=1, triggering MSB16 lookups
20702071
BusId::Memw.into(),
20712072
];
20722073

prover/src/tables/cpu_bitwise.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
//! constraints (conditional constraints are automatically satisfied since
99
//! non-bitwise selectors are always 0).
1010
11-
pub use super::cpu::{cols, generate_cpu_trace, CpuOperation};
11+
pub use super::cpu::{CpuOperation, cols, generate_cpu_trace};
1212

1313
use stark::lookup::BusInteraction;
1414

prover/src/tables/trace_builder.rs

Lines changed: 33 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -1631,6 +1631,19 @@ pub struct Traces {
16311631
pub memw_registers: Vec<TraceTable<GoldilocksField, GoldilocksExtension>>,
16321632
}
16331633

1634+
/// Count total padding rows that `chunk_and_generate` would produce.
1635+
///
1636+
/// Matches `chunk_and_generate` behavior: empty input produces 1 chunk of 4 padding rows.
1637+
fn count_padding_rows<T>(ops: &[T], max_rows: usize) -> usize {
1638+
if ops.is_empty() {
1639+
4 // chunk_and_generate generates 1 chunk, generate_*_trace pads 0 ops to 4
1640+
} else {
1641+
ops.chunks(max_rows)
1642+
.map(|chunk| chunk.len().next_power_of_two().max(4) - chunk.len())
1643+
.sum()
1644+
}
1645+
}
1646+
16341647
/// Chunk raw ops and generate one trace table per chunk.
16351648
fn chunk_and_generate<T>(
16361649
ops: &[T],
@@ -1929,23 +1942,19 @@ impl Traces {
19291942
cpu_ops.into_iter().partition(|op| op.is_bitwise());
19301943

19311944
// CPU and CPU_BITWISE padding rows send IS_BYTE with all-zero values.
1932-
// Computed after partition so padding reflects actual chunk sizes.
1933-
let num_padding_rows: usize = cpu_ops
1934-
.chunks(max_rows.cpu)
1935-
.map(|chunk| chunk.len().next_power_of_two().max(4) - chunk.len())
1936-
.sum::<usize>()
1937-
+ cpu_bitwise_ops
1938-
.chunks(max_rows.cpu)
1939-
.map(|chunk| chunk.len().next_power_of_two().max(4) - chunk.len())
1940-
.sum::<usize>();
1945+
// Uses count_padding_rows to match chunk_and_generate's behavior
1946+
// (including the phantom 4-row chunk for empty input).
1947+
let num_padding_rows: usize = count_padding_rows(&cpu_ops, max_rows.cpu)
1948+
+ count_padding_rows(&cpu_bitwise_ops, max_rows.cpu);
19411949
bitwise_ops.extend(collect_byte_check_ops_for_padding(num_padding_rows));
19421950

19431951
let cpus = chunk_and_generate(&cpu_ops, max_rows.cpu, cpu::generate_cpu_trace);
1944-
let cpu_bitwises = if cpu_bitwise_ops.is_empty() {
1945-
Vec::new()
1946-
} else {
1947-
chunk_and_generate(&cpu_bitwise_ops, max_rows.cpu, cpu::generate_cpu_trace)
1948-
};
1952+
// Always generate at least one CPU_BITWISE chunk (even if empty/padding-only).
1953+
// This is required for soundness: without a CPU_BITWISE AIR, the verifier
1954+
// cannot enforce AND/OR/XOR byte lookups. A malicious prover could omit
1955+
// the chip and forge bitwise results.
1956+
let cpu_bitwises =
1957+
chunk_and_generate(&cpu_bitwise_ops, max_rows.cpu, cpu::generate_cpu_trace);
19491958
let memws = chunk_and_generate(&memw_ops, max_rows.memw, memw::generate_memw_trace);
19501959
let memw_aligneds = chunk_and_generate(
19511960
&memw_aligned_ops,
@@ -1968,20 +1977,9 @@ impl Traces {
19681977
let mut bitwise = bitwise::generate_bitwise_trace();
19691978
bitwise::update_multiplicities(&mut bitwise, &bitwise_ops);
19701979

1971-
// Update DECODE multiplicities
1972-
// Each CPU operation (from both CPU and CPU_BITWISE chips) looks up the DECODE table once.
1973-
// Padding rows also look up pc=1 (the CPU padding entry).
1974-
// When CPU is split, each chunk pads independently.
1980+
// Update DECODE multiplicities (reuses num_padding_rows from IS_BYTE calculation above).
19751981
let mut decode = decode_trace;
19761982
let pc_to_row = decode_pc_to_row;
1977-
let num_padding_rows: usize = cpu_ops
1978-
.chunks(max_rows.cpu)
1979-
.map(|chunk| chunk.len().next_power_of_two().max(4) - chunk.len())
1980-
.sum::<usize>()
1981-
+ cpu_bitwise_ops
1982-
.chunks(max_rows.cpu)
1983-
.map(|chunk| chunk.len().next_power_of_two().max(4) - chunk.len())
1984-
.sum::<usize>();
19851983
let mut decode_lookups: Vec<u64> = cpu_ops.iter().map(|op| op.decode.pc).collect();
19861984
decode_lookups.extend(cpu_bitwise_ops.iter().map(|op| op.decode.pc));
19871985
decode_lookups.extend(std::iter::repeat_n(cpu::CPU_PADDING_PC, num_padding_rows));
@@ -2192,22 +2190,17 @@ impl Traces {
21922190
cpu_ops.into_iter().partition(|op| op.is_bitwise());
21932191

21942192
// CPU and CPU_BITWISE padding rows send IS_BYTE with all-zero values.
2195-
let num_padding_rows: usize = cpu_ops
2196-
.chunks(max_rows.cpu)
2197-
.map(|chunk| chunk.len().next_power_of_two().max(4) - chunk.len())
2198-
.sum::<usize>()
2199-
+ cpu_bitwise_ops
2200-
.chunks(max_rows.cpu)
2201-
.map(|chunk| chunk.len().next_power_of_two().max(4) - chunk.len())
2202-
.sum::<usize>();
2193+
let num_padding_rows: usize = count_padding_rows(&cpu_ops, max_rows.cpu)
2194+
+ count_padding_rows(&cpu_bitwise_ops, max_rows.cpu);
22032195
bitwise_ops.extend(collect_byte_check_ops_for_padding(num_padding_rows));
22042196

22052197
let cpus = chunk_and_generate(&cpu_ops, max_rows.cpu, cpu::generate_cpu_trace);
2206-
let cpu_bitwises = if cpu_bitwise_ops.is_empty() {
2207-
Vec::new()
2208-
} else {
2209-
chunk_and_generate(&cpu_bitwise_ops, max_rows.cpu, cpu::generate_cpu_trace)
2210-
};
2198+
// Always generate at least one CPU_BITWISE chunk (even if empty/padding-only).
2199+
// This is required for soundness: without a CPU_BITWISE AIR, the verifier
2200+
// cannot enforce AND/OR/XOR byte lookups. A malicious prover could omit
2201+
// the chip and forge bitwise results.
2202+
let cpu_bitwises =
2203+
chunk_and_generate(&cpu_bitwise_ops, max_rows.cpu, cpu::generate_cpu_trace);
22112204
let memws = chunk_and_generate(&memw_ops, max_rows.memw, memw::generate_memw_trace);
22122205
let memw_aligneds = chunk_and_generate(
22132206
&memw_aligned_ops,
@@ -2230,17 +2223,8 @@ impl Traces {
22302223
let mut bitwise = bitwise::generate_bitwise_trace();
22312224
bitwise::update_multiplicities(&mut bitwise, &bitwise_ops);
22322225

2233-
// Generate DECODE trace and update multiplicities
2234-
// Both CPU and CPU_BITWISE chips look up DECODE once per row
2226+
// Generate DECODE trace and update multiplicities (reuses num_padding_rows from above).
22352227
let (mut decode, pc_to_row) = decode::generate_decode_trace(&instructions);
2236-
let num_padding_rows: usize = cpu_ops
2237-
.chunks(max_rows.cpu)
2238-
.map(|chunk| chunk.len().next_power_of_two().max(4) - chunk.len())
2239-
.sum::<usize>()
2240-
+ cpu_bitwise_ops
2241-
.chunks(max_rows.cpu)
2242-
.map(|chunk| chunk.len().next_power_of_two().max(4) - chunk.len())
2243-
.sum::<usize>();
22442228
let mut decode_lookups: Vec<u64> = cpu_ops.iter().map(|op| op.decode.pc).collect();
22452229
decode_lookups.extend(cpu_bitwise_ops.iter().map(|op| op.decode.pc));
22462230
decode_lookups.extend(std::iter::repeat_n(cpu::CPU_PADDING_PC, num_padding_rows));

0 commit comments

Comments
 (0)