docs: add inline-pc memory access design spec

Design for moving PC register read/write from the MEMW bus (through MEMW_R)
to direct interactions on the low-level memory bus within the CPU chip.

Eliminates one MEMW_R row per CPU step (~50% MEMW_R reduction).
Adds 2 CPU columns and 4 memory bus interactions.

Based on spec PR #501 (spec/inline-pc).

Author: diegokingston

docs/superpowers/specs/2026-04-16-inline-pc-memory-design.md

@@ -0,0 +1,138 @@
+# Inline PC Memory Access into CPU
+
+## Goal
+
+Eliminate the MEMW_R table rows for the PC register by having the CPU chip interact directly with the low-level `memory` bus for PC reads and writes. This removes one MEMW_R row per CPU step, roughly halving the MEMW_R table size for most programs.
+
+## Context
+
+Currently, every CPU cycle writes `next_pc` to register x255 (address 510-511) via the `MEMW` bus. This routes through MEMW_R (register fast-path), which decomposes the 2-word register operation into two per-word interactions on the `memory` bus. Since the PC register has a completely predictable access pattern (read once, write once, every cycle, at known addresses), this intermediate step is unnecessary.
+
+Two buses are involved:
+- **`MEMW` bus**: High-level, 24-element fingerprint. CPU sends multi-byte operations; MEMW/MEMW_R receive and decompose.
+- **`memory` bus**: Low-level, 6-element fingerprint `(is_register, addr_lo, addr_hi, ts_lo, ts_hi, value)`. MEMW_R, MEMW_A, and PAGE tables interact here. Token-based memory argument: every read consumes a token (sender, +1), every write emits a token (receiver, -1).
+
+Based on spec PR #501 (`spec/inline-pc`).
+
+## Design
+
+### What gets removed
+
+**One MEMW bus interaction from CPU** (currently CM54):
+```
+MEMW[pc; 1, 510, next_pc, timestamp+1, 1, 0, 0]  multiplicity = (1 - pad)
+```
+This 24-element sender to `BusId::Memw` with all-ALU-flags multiplicity.
+
+**One MEMW_R row per CPU cycle**: The trace builder currently creates a `MemwOperation` for the PC at every non-padding row. This routes through MEMW_R, producing one row there.
+
+### What gets added
+
+**Two new CPU columns** (74 → 76):
+
+| Column | Type | Description |
+|--------|------|-------------|
+| `PREV_PC_TIMESTAMP_BORROW` | Bit | Borrow bit for 64-bit subtraction `timestamp - 3`. Set when `timestamp_lo < 3`. |
+| `PC_DOUBLE_READ` | Bit | 1 when `rs1 = 255` (AUIPC/JAL reads PC via M1). Affects previous timestamp. |
+
+**Four new `memory` bus interactions** (replacing the one MEMW interaction):
+
+For `i = 0, 1` (two words of address 510 and 511):
+
+1. **PC read** (sender, +1 multiplicity, consumes old token):
+   ```
+   memory[1, 510+i, 0, prev_ts_lo, prev_ts_hi, pc[i]]
+   multiplicity = (1 - pad)
+   ```
+
+2. **PC write** (receiver, -1 multiplicity, emits new token):
+   ```
+   memory[1, 510+i, 0, timestamp + 1, 0, next_pc[i]]
+   multiplicity = -(1 - pad)
+   ```
+
+Where:
+```
+prev_ts_lo = timestamp - 3*(1 - pc_double_read) + 2^32 * borrow
+prev_ts_hi = 0 - borrow
+```
+(Since timestamps fit in 32 bits, `timestamp_hi = 0` always. The subtraction of 3 can only underflow in the lo word.)
+
+**Four new constraints**:
+1. `pc_double_read * (rs1 - 255) = 0` — pc_double_read=1 only when rs1=255
+2. `pc_double_read * prev_pc_timestamp_borrow = 0` — no borrow when pc_double_read=1 (subtraction is 0)
+3. `IS_BIT[prev_pc_timestamp_borrow]`
+4. `IS_BIT[pc_double_read]`
+
+### Impact summary
+
+| Metric | Before | After | Delta |
+|--------|--------|-------|-------|
+| CPU main columns | 74 | 76 | +2 |
+| CPU MEMW bus interactions | 1 (24 elements) | 0 | -1 |
+| CPU memory bus interactions | 0 | 4 (6 elements each) | +4 |
+| CPU transition constraints | N | N+4 | +4 |
+| MEMW_R rows per CPU cycle | 1 | 0 | -1 |
+
+Net trace savings: for N CPU steps, we add 2N field elements to CPU but remove 10N from MEMW_R (10 columns). Net saving: 8N field elements (~6% total trace reduction for typical programs).
+
+## Timestamp Arithmetic
+
+The CPU stores `timestamp` as a single field element. The memory bus needs `(ts_lo, ts_hi)` where lo/hi are 32-bit words. Since timestamps never exceed 2^32 for practical programs, `ts_hi = 0` always.
+
+**Normal case** (`pc_double_read = 0`): The PC was last written at `T+1` in the previous cycle. With granularity 4, `T_prev + 1 = T - 3`:
+```
+prev_ts_lo = timestamp - 3 + 2^32 * borrow    (field arithmetic)
+prev_ts_hi = 0 - borrow = -borrow              (0 or p-1 in the field, but bus expects 0 or -1 as word)
+```
+When `timestamp < 3` (first cycle), `borrow = 1` corrects the underflow.
+
+**AUIPC/JAL case** (`pc_double_read = 1`): The M1 register read already consumed the previous PC token (via MEMW→MEMW_R→memory bus at timestamp T+0) and emitted a new one at T+0. The inline PC read consumes that fresh token:
+```
+prev_ts_lo = timestamp    (no subtraction)
+prev_ts_hi = 0
+borrow = 0               (forced by constraint)
+```
+
+**Token chain for AUIPC/JAL**: Previous write (T_prev+1) → MEMW_R read (T_prev+1) → MEMW_R write (T+0) → inline read (T+0) → inline write (T+1). Each sender (+1) at timestamp X cancels the receiver (-1) that emitted at timestamp X.
+
+## Files to Change
+
+### 1. `prover/src/tables/cpu.rs`
+
+**Column definitions** (`cols` module):
+- Add `PREV_PC_TIMESTAMP_BORROW` at index 74
+- Add `PC_DOUBLE_READ` at index 75
+- Update `NUM_COLUMNS` from 74 to 76
+
+**Trace generation** (`generate_cpu_trace`):
+- For each row: compute `pc_double_read = (d.rs1 == 255 && d.read_register1) as u64`
+- Compute `prev_pc_timestamp_borrow = (op.timestamp < 3 && pc_double_read == 0) as u64`
+- Write both values to columns 74 and 75
+
+**Bus interactions** (`cpu_bus_interactions`):
+- Remove CM54 (the MEMW sender for PC)
+- Add 4 memory bus interactions (2 reads + 2 writes to `BusId::Memory`)
+
+### 2. `prover/src/constraints/cpu.rs`
+
+- Add constraint: `pc_double_read * (rs1 - 255) = 0`
+- Add constraint: `pc_double_read * prev_pc_timestamp_borrow = 0`
+- Add IS_BIT constraints for both new columns
+
+### 3. `prover/src/tables/trace_builder.rs`
+
+- In `collect_memw_from_cpu` (lines 594-607): Remove the CM54 block that creates a `MemwOperation` for the PC register
+- Keep `register_state.write_pc(op.next_pc, op.timestamp + 1)` — the register state tracker is still needed for M1 interactions when `rs1=255` (AUIPC/JAL), which still go through MEMW_R
+
+### 4. `prover/src/test_utils.rs`
+
+- Update `create_cpu_air` to use 76 columns
+- Add new bus interactions and constraints to the CPU AIR
+
+## Testing
+
+1. **Existing prove-and-verify tests**: All passing tests must continue to pass. The memory bus must still balance globally.
+2. **AUIPC/JAL**: Test programs using `rs1=255` to verify the `pc_double_read` path and token chain correctness.
+3. **First cycle**: Verify `timestamp < 3` triggers the borrow bit correctly.
+4. **Bus balance**: The global LogUp sum must still be zero (or the expected commit offset).