Skip to content

Commit 6b9a0b9

Browse files
diegokingstondiegokingston
authored
Feat/inline pc (#505)
* feat: inline PC register access in CPU via direct memory bus Move PC register (x255) read/write from MEMW bus to direct Memory bus interactions in the CPU chip, eliminating one MEMW_R row per CPU cycle. - Add PREV_PC_TIMESTAMP_BORROW and PC_DOUBLE_READ columns (74, 75) - Add PcDoubleReadRs1Constraint and PcDoubleReadBorrowConstraint - Replace CM54 MEMW interaction with 4 Memory bus interactions - Remove PC MemwOperation from trace builder - Update test counts (columns 74→76, constraints 66→70, bus 68→71) * fix: address PR review for inline PC register access - H2: Fix first-cycle timestamp bug by changing starting offset from 4 to 3, so prev_ts = 3-3 = 0 matches REGISTER table's initial PC token at timestamp 0. - H1: Add soundness comment explaining LogUp bus catches pc_double_read tampering (the suggested algebraic constraint is incorrect). - M1: Use explicit 1i64 << 32 for borrow coefficient. - M2: Add comment explaining -1 borrow cancellation in prev_ts_hi. - L1: Move inline PC constraint structs before create_all_cpu_constraints. * style: apply cargo fmt * fix: resolve clippy clone_on_copy errors in inline PC constraints * fix: align inline PC with PR 501 spec Resolves two divergences from the latest spec in PR 501: 1. Register initialization timestamp (spec/memory.typ, commit 5fffb67): "register initialization happens at timestamp 1". REG-C1 now emits the initial token at timestamp 1, RegisterState initializes every register's last-write timestamp at 1, and CPU timestamps use (i*4)+4 so the first row's inline PC prev_ts = timestamp - 3 = 1 matches the REG init. Padding rows in the REGISTER trace are set to TIMESTAMP_LO=1 so REG-C1/REG-C2 still self-cancel. 2. pc_double_read constraints (spec/cpu.typ, commit 44aa87b): spec explicitly states these are unnecessary because "the integrity of the memory argument ensures the correctness of this bit". Removed PcDoubleReadRs1Constraint and PcDoubleReadBorrowConstraint. The columns stay as bit-flag witnesses (IS_BIT-constrained) and feed the inline PC bus formula. NUM_CPU_CONSTRAINTS drops from 70 to 68.
1 parent 62bfbb9 commit 6b9a0b9

7 files changed

Lines changed: 243 additions & 185 deletions

File tree

‎prover/src/constraints/cpu.rs‎

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,9 @@ pub const BIT_FLAG_COLUMNS: &[usize] = &[
9191
// Computed flags
9292
cols::IS_EQUAL,
9393
cols::BRANCH_COND,
94+
// Inline PC columns
95+
cols::PREV_PC_TIMESTAMP_BORROW,
96+
cols::PC_DOUBLE_READ,
9497
];
9598

9699
/// Creates all IS_BIT constraints for CPU flag columns.
@@ -1011,6 +1014,19 @@ pub fn create_jalr_constraints(constraint_idx_start: usize) -> (Vec<AddConstrain
10111014
(vec![jalr_c0, jalr_c1], constraint_idx_start + 2)
10121015
}
10131016

1017+
// =========================================================================
1018+
// Inline PC Constraints
1019+
// =========================================================================
1020+
//
1021+
// Per spec/cpu.typ: "Constraints on `pc_double_read` corresponding to an `AUIPC`
1022+
// instruction are not necessary, as regardless of its value, the old timestamp is
1023+
// guaranteed smaller than the new timestamp, and the integrity of the memory
1024+
// argument therefore ensures the correctness of this bit."
1025+
//
1026+
// The IS_BIT constraints on PC_DOUBLE_READ and PREV_PC_TIMESTAMP_BORROW are
1027+
// sufficient; no extra algebraic constraints linking them to rs1/read_register1
1028+
// or to each other are required.
1029+
10141030
// =========================================================================
10151031
// Constraint Summary
10161032
// =========================================================================
@@ -1036,9 +1052,12 @@ pub fn create_jalr_constraints(constraint_idx_start: usize) -> (Vec<AddConstrain
10361052
/// - rv2 zero-forcing (CM50): 3 (rv2[0..2] when read_register2 = 0)
10371053
/// - Next PC (non-branching): 2
10381054
///
1039-
/// Total: 66 constraints (32 IS_BIT + 8 ADD + 26 other)
1055+
/// Total: 68 constraints (34 IS_BIT + 8 ADD + 26 other)
1056+
/// (The inline PC columns PC_DOUBLE_READ and PREV_PC_TIMESTAMP_BORROW are
1057+
/// IS_BIT-constrained; per spec/cpu.typ no additional algebraic constraints
1058+
/// are required.)
10401059
pub const NUM_CPU_CONSTRAINTS: usize =
1041-
32 + 2 + 2 + 2 + 2 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 7 + 3 + 3 + 3 + 2;
1060+
34 + 2 + 2 + 2 + 2 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 7 + 3 + 3 + 3 + 2;
10421061

10431062
/// Creates all CPU constraints.
10441063
///

‎prover/src/tables/cpu.rs‎

Lines changed: 168 additions & 133 deletions
Original file line numberDiff line numberDiff line change
@@ -232,8 +232,16 @@ pub mod cols {
232232
/// branch_cond: Whether branch is taken
233233
pub const BRANCH_COND: usize = 73;
234234

235+
/// prev_pc_timestamp_borrow: Borrow bit for the 32-bit subtraction timestamp_lo - 3
236+
/// in the inline PC prev_ts formula. Fires only when timestamp_lo < 3 and
237+
/// pc_double_read = 0 (i.e. after timestamp wraps past 2^32 into values 0..2).
238+
pub const PREV_PC_TIMESTAMP_BORROW: usize = 74;
239+
240+
/// pc_double_read: Whether PC is read as rs1 this cycle (AUIPC/JAL)
241+
pub const PC_DOUBLE_READ: usize = 75;
242+
235243
/// Total number of columns
236-
pub const NUM_COLUMNS: usize = 74;
244+
pub const NUM_COLUMNS: usize = 76;
237245

238246
// -------------------------------------------------------------------------
239247
// Helper ranges for iteration
@@ -851,6 +859,17 @@ pub fn generate_cpu_trace(
851859
// Branch columns
852860
data[base + cols::IS_EQUAL] = FE::from(op.is_equal as u64);
853861
data[base + cols::BRANCH_COND] = FE::from(op.branch_cond as u64);
862+
863+
// Inline PC columns
864+
let pc_double_read = (d.read_register1 && d.rs1 == 255) as u64;
865+
let ts_lo = op.timestamp & 0xFFFF_FFFF;
866+
let prev_pc_ts_borrow = if pc_double_read == 0 && ts_lo < 3 {
867+
1u64
868+
} else {
869+
0u64
870+
};
871+
data[base + cols::PC_DOUBLE_READ] = FE::from(pc_double_read);
872+
data[base + cols::PREV_PC_TIMESTAMP_BORROW] = FE::from(prev_pc_ts_borrow);
854873
}
855874

856875
// Padding rows: per spec, padding uses pc=1 (odd address, unreachable during
@@ -884,7 +903,7 @@ pub fn generate_cpu_trace_from_logs(
884903
.ok_or(Error::MissingInstruction(log.current_pc))?;
885904
operations.push(CpuOperation::from_log_and_instruction(
886905
log,
887-
(i as u64) * 4,
906+
(i as u64) * 4 + 4,
888907
instruction,
889908
));
890909
}
@@ -913,7 +932,7 @@ pub fn collect_bitwise_ops_from_logs(
913932
.ok_or(Error::MissingInstruction(log.current_pc))?;
914933
operations.push(CpuOperation::from_log_and_instruction(
915934
log,
916-
(i as u64) * 4,
935+
(i as u64) * 4 + 4,
917936
instruction,
918937
));
919938
}
@@ -1717,137 +1736,153 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
17171736
],
17181737
));
17191738

1720-
// -------------------------------------------------------------------------
1721-
// CM54: MEMW[pc; 1, 510, next_pc, timestamp+1, 1, 0, 0] | 1 - pad
1722-
// -------------------------------------------------------------------------
1723-
// PC register read-write via MEMW. Format: 24 elements (with old)
1724-
// [old[8], is_register, base_addr[2], value[8], timestamp[2], write2, write4, write8]
1725-
//
1726-
// Every non-padding CPU row reads pc and writes next_pc to register x255 (address 510).
1727-
// Multiplicity = sum of all ALU flags = 1 for non-padding rows, 0 for padding.
1728-
interactions.push(BusInteraction::sender(
1729-
BusId::Memw,
1730-
Multiplicity::Linear(vec![
1731-
LinearTerm::Column {
1732-
coefficient: 1,
1733-
column: cols::ADD,
1734-
},
1735-
LinearTerm::Column {
1736-
coefficient: 1,
1737-
column: cols::SUB,
1738-
},
1739-
LinearTerm::Column {
1740-
coefficient: 1,
1741-
column: cols::SLT,
1742-
},
1743-
LinearTerm::Column {
1744-
coefficient: 1,
1745-
column: cols::AND,
1746-
},
1747-
LinearTerm::Column {
1748-
coefficient: 1,
1749-
column: cols::OR,
1750-
},
1751-
LinearTerm::Column {
1752-
coefficient: 1,
1753-
column: cols::XOR,
1754-
},
1755-
LinearTerm::Column {
1756-
coefficient: 1,
1757-
column: cols::SHIFT,
1758-
},
1759-
LinearTerm::Column {
1760-
coefficient: 1,
1761-
column: cols::JALR,
1762-
},
1763-
LinearTerm::Column {
1764-
coefficient: 1,
1765-
column: cols::BEQ,
1766-
},
1767-
LinearTerm::Column {
1768-
coefficient: 1,
1769-
column: cols::BLT,
1770-
},
1771-
LinearTerm::Column {
1772-
coefficient: 1,
1773-
column: cols::LOAD,
1774-
},
1775-
LinearTerm::Column {
1776-
coefficient: 1,
1777-
column: cols::STORE,
1778-
},
1779-
LinearTerm::Column {
1780-
coefficient: 1,
1781-
column: cols::MUL,
1782-
},
1783-
LinearTerm::Column {
1784-
coefficient: 1,
1785-
column: cols::DIVREM,
1786-
},
1787-
LinearTerm::Column {
1788-
coefficient: 1,
1789-
column: cols::ECALL,
1790-
},
1791-
LinearTerm::Column {
1792-
coefficient: 1,
1793-
column: cols::EBREAK,
1794-
},
1795-
]),
1796-
vec![
1797-
// old[0] = PC_0 (low word of current pc)
1798-
BusValue::Packed {
1799-
start_column: cols::PC_0,
1800-
packing: Packing::Direct,
1801-
},
1802-
// old[1] = PC_1 (high word of current pc)
1803-
BusValue::Packed {
1804-
start_column: cols::PC_1,
1805-
packing: Packing::Direct,
1806-
},
1807-
// old[2..7] = 0 (unconstrained for registers)
1808-
BusValue::constant(0),
1809-
BusValue::constant(0),
1810-
BusValue::constant(0),
1811-
BusValue::constant(0),
1812-
BusValue::constant(0),
1813-
BusValue::constant(0),
1814-
// is_register = 1
1815-
BusValue::constant(1),
1816-
// base_address = [510, 0] (register x255)
1817-
BusValue::constant(510),
1818-
BusValue::constant(0),
1819-
// value[0] = NEXT_PC_0 (low word of next_pc)
1820-
BusValue::Packed {
1821-
start_column: cols::NEXT_PC_0,
1822-
packing: Packing::Direct,
1823-
},
1824-
// value[1] = NEXT_PC_1 (high word of next_pc)
1825-
BusValue::Packed {
1826-
start_column: cols::NEXT_PC_1,
1827-
packing: Packing::Direct,
1828-
},
1829-
// value[2..7] = 0 (unconstrained for registers)
1830-
BusValue::constant(0),
1831-
BusValue::constant(0),
1832-
BusValue::constant(0),
1833-
BusValue::constant(0),
1834-
BusValue::constant(0),
1835-
BusValue::constant(0),
1836-
// timestamp[0] = timestamp + 1, timestamp[1] = 0
1837-
BusValue::linear(vec![
1838-
LinearTerm::Column {
1839-
coefficient: 1,
1840-
column: cols::TIMESTAMP,
1739+
// =========================================================================
1740+
// Inline PC memory interactions (replaces CM54 MEMW interaction)
1741+
// =========================================================================
1742+
// CPU directly talks to the low-level memory bus for PC register (x255,
1743+
// addresses 510 and 511), bypassing MEMW_R.
1744+
1745+
// Non-padding multiplicity: sum of all ALU selector flags
1746+
let non_pad_mult = Multiplicity::Linear(vec![
1747+
LinearTerm::Column {
1748+
coefficient: 1,
1749+
column: cols::ADD,
1750+
},
1751+
LinearTerm::Column {
1752+
coefficient: 1,
1753+
column: cols::SUB,
1754+
},
1755+
LinearTerm::Column {
1756+
coefficient: 1,
1757+
column: cols::SLT,
1758+
},
1759+
LinearTerm::Column {
1760+
coefficient: 1,
1761+
column: cols::AND,
1762+
},
1763+
LinearTerm::Column {
1764+
coefficient: 1,
1765+
column: cols::OR,
1766+
},
1767+
LinearTerm::Column {
1768+
coefficient: 1,
1769+
column: cols::XOR,
1770+
},
1771+
LinearTerm::Column {
1772+
coefficient: 1,
1773+
column: cols::SHIFT,
1774+
},
1775+
LinearTerm::Column {
1776+
coefficient: 1,
1777+
column: cols::JALR,
1778+
},
1779+
LinearTerm::Column {
1780+
coefficient: 1,
1781+
column: cols::BEQ,
1782+
},
1783+
LinearTerm::Column {
1784+
coefficient: 1,
1785+
column: cols::BLT,
1786+
},
1787+
LinearTerm::Column {
1788+
coefficient: 1,
1789+
column: cols::LOAD,
1790+
},
1791+
LinearTerm::Column {
1792+
coefficient: 1,
1793+
column: cols::STORE,
1794+
},
1795+
LinearTerm::Column {
1796+
coefficient: 1,
1797+
column: cols::MUL,
1798+
},
1799+
LinearTerm::Column {
1800+
coefficient: 1,
1801+
column: cols::DIVREM,
1802+
},
1803+
LinearTerm::Column {
1804+
coefficient: 1,
1805+
column: cols::ECALL,
1806+
},
1807+
LinearTerm::Column {
1808+
coefficient: 1,
1809+
column: cols::EBREAK,
1810+
},
1811+
]);
1812+
1813+
// prev_ts_lo = timestamp - 3*(1 - pc_double_read) + 2^32 * borrow
1814+
// = timestamp - 3 + 3*pc_double_read + 2^32 * borrow
1815+
let prev_ts_lo = BusValue::linear(vec![
1816+
LinearTerm::Column {
1817+
coefficient: 1,
1818+
column: cols::TIMESTAMP,
1819+
},
1820+
LinearTerm::Constant(-3),
1821+
LinearTerm::Column {
1822+
coefficient: 3,
1823+
column: cols::PC_DOUBLE_READ,
1824+
},
1825+
LinearTerm::Column {
1826+
coefficient: 1i64 << 32,
1827+
column: cols::PREV_PC_TIMESTAMP_BORROW,
1828+
},
1829+
]);
1830+
1831+
// prev_ts_hi = 0 - borrow
1832+
// The -1 cancels the +2^32 added to prev_ts_lo when borrow fires, keeping the
1833+
// 64-bit timestamp correct: (prev_ts_hi * 2^32 + prev_ts_lo) = timestamp - 3.
1834+
let prev_ts_hi = BusValue::linear(vec![LinearTerm::Column {
1835+
coefficient: -1,
1836+
column: cols::PREV_PC_TIMESTAMP_BORROW,
1837+
}]);
1838+
1839+
for i in 0..2u64 {
1840+
// PC read (sender, +1): consume old token
1841+
// memory[1, 510+i, 0, prev_ts_lo, prev_ts_hi, pc[i]]
1842+
interactions.push(BusInteraction::sender(
1843+
BusId::Memory,
1844+
non_pad_mult.clone(),
1845+
vec![
1846+
BusValue::constant(1),
1847+
BusValue::constant(510 + i),
1848+
BusValue::constant(0),
1849+
prev_ts_lo.clone(),
1850+
prev_ts_hi.clone(),
1851+
BusValue::Packed {
1852+
start_column: if i == 0 { cols::PC_0 } else { cols::PC_1 },
1853+
packing: Packing::Direct,
18411854
},
1842-
LinearTerm::Constant(1),
1843-
]),
1844-
BusValue::constant(0),
1845-
// write2=1, write4=0, write8=0 (register access = 2 Words / 64 bits)
1846-
BusValue::constant(1),
1847-
BusValue::constant(0),
1848-
BusValue::constant(0),
1849-
],
1850-
));
1855+
],
1856+
));
1857+
1858+
// PC write (receiver, -1): emit new token
1859+
// memory[1, 510+i, 0, timestamp+1, 0, next_pc[i]]
1860+
interactions.push(BusInteraction::receiver(
1861+
BusId::Memory,
1862+
non_pad_mult.clone(),
1863+
vec![
1864+
BusValue::constant(1),
1865+
BusValue::constant(510 + i),
1866+
BusValue::constant(0),
1867+
BusValue::linear(vec![
1868+
LinearTerm::Column {
1869+
coefficient: 1,
1870+
column: cols::TIMESTAMP,
1871+
},
1872+
LinearTerm::Constant(1),
1873+
]),
1874+
BusValue::constant(0),
1875+
BusValue::Packed {
1876+
start_column: if i == 0 {
1877+
cols::NEXT_PC_0
1878+
} else {
1879+
cols::NEXT_PC_1
1880+
},
1881+
packing: Packing::Direct,
1882+
},
1883+
],
1884+
));
1885+
}
18511886

18521887
// -------------------------------------------------------------------------
18531888
// BRANCH interaction (for branch/jump target calculation)

0 commit comments

Comments
 (0)