perf: eliminate REGISTER table by computing bus contributions in verifier

The REGISTER table (67 rows, 5 columns) provided init/fini anchors on the
Memory bus for all registers. Since all init and fini values are fully
deterministic from the ELF entry point, the verifier can compute these
bus contributions directly instead of proving them.

Changes:
- Add HALT finalization for x0 and x254 at ts=MAX, making all 67 register
  word addresses have deterministic fini state (value=0 except x255[510]=1,
  ts=MAX for all). x254 uses width-1 format (write2=0).
- Add `compute_register_bus_offset` in prover/src/lib.rs: computes the
  LogUp sum for REG-C1 (receiver, init) and REG-C2 (sender, fini) across
  all 67 addresses using the same fingerprint formula as the STARK prover.
- Rename `compute_expected_commit_bus_balance` to `compute_expected_bus_balance`
  which now sums both COMMIT and REGISTER offsets.
- Remove REGISTER from VmAirs (struct, air_trace_pairs, air_refs, new).
- Remove register trace from Traces struct and generation pipeline.
- Update expected_proof_count from 5 fixed tables to 4 (bitwise, decode,
  halt, commit).

This saves one full table proof (LDE, Merkle tree, FRI) and its
preprocessed commitment computation per proof.

Author: diegokingston

prover/src/lib.rs

@@ -42,7 +42,7 @@ use crate::test_utils::{
     E, F, VmAir, create_bitwise_air, create_branch_air, create_commit_air, create_cpu_air,
     create_decode_air, create_dvrm_air, create_halt_air, create_load_air, create_lt_air,
     create_memw_air, create_memw_aligned_air, create_memw_register_air, create_mul_air,
-    create_page_air, create_register_air, create_shift_air,
+    create_page_air, create_shift_air,
 };
 
 use stark::proof::options::{GoldilocksCubicProofOptions, ProofOptions};
@@ -196,7 +196,6 @@ pub(crate) struct VmAirs {
     pub branches: Vec<VmAir>,
     pub halt: VmAir,
     pub commit: VmAir,
-    pub register: VmAir,
     pub pages: Vec<VmAir>,
     pub memw_registers: Vec<VmAir>,
 }
@@ -209,7 +208,6 @@ impl VmAirs {
             (&self.decode, &mut traces.decode, &()),
             (&self.halt, &mut traces.halt, &()),
             (&self.commit, &mut traces.commit, &()),
-            (&self.register, &mut traces.register, &()),
         ];
 
         for (air, trace) in self.cpus.iter().zip(traces.cpus.iter_mut()) {
@@ -264,7 +262,6 @@ impl VmAirs {
             &self.decode,
             &self.halt,
             &self.commit,
-            &self.register,
         ];
 
         for air in &self.cpus {
@@ -359,10 +356,6 @@ impl VmAirs {
             .collect();
         let halt = create_halt_air(proof_options);
         let commit = create_commit_air(proof_options);
-        let register = create_register_air(proof_options).with_preprocessed(
-            register::preprocessed_commitment(proof_options, elf.entry_point),
-            register::NUM_PREPROCESSED_COLS,
-        );
         let pages: Vec<_> = page_configs
             .iter()
             .map(|config| {
@@ -393,7 +386,6 @@ impl VmAirs {
             branches,
             halt,
             commit,
-            register,
             pages,
             memw_registers,
         }
@@ -459,18 +451,109 @@ pub(crate) fn compute_commit_bus_offset(
     Some(total)
 }
 
-/// Compute the expected COMMIT bus balance for a `MultiProof`.
+/// Compute the bus balance offset for the REGISTER table on the Memory bus.
+///
+/// For each of the 67 register word addresses, computes the LogUp contribution
+/// of both REG-C1 (receiver, init token) and REG-C2 (sender, fini token).
+///
+/// After HALT finalization, all registers have deterministic fini state:
+/// - x0-x31 (addr 0-63): fini=0, ts=MAX
+/// - x254 (addr 508): fini=0, ts=MAX
+/// - x255 (addr 510-511): fini_lo=1, fini_hi=0, ts=MAX
+///
+/// Init values are also deterministic from the ELF entry point:
+/// - SP (x2): init = STACK_TOP
+/// - PC (x255): init = entry_point
+/// - All others: init = 0
+///
+/// The fingerprint formula per bus interaction is:
+///   `lc = BusId::Memory * α^0 + is_register * α^1 + addr * α^2 + addr_hi * α^3
+///         + ts_lo * α^4 + ts_hi * α^5 + value * α^6`
+///   `fingerprint = z - lc`
+///
+/// REG-C1 (receiver): contribution = -1/fingerprint
+/// REG-C2 (sender):   contribution = +1/fingerprint
+///
+/// Returns `Some(Σ contributions)`, or `None` on a fingerprint collision.
+pub(crate) fn compute_register_bus_offset(
+    entry_point: u64,
+    z: &FieldElement<E>,
+    alpha: &FieldElement<E>,
+) -> Option<FieldElement<E>> {
+    let bus_id = FieldElement::<E>::from(BusId::Memory as u64);
+    let alpha2 = alpha * alpha;
+    let alpha3 = &alpha2 * alpha;
+    let alpha4 = &alpha3 * alpha;
+    let alpha5 = &alpha4 * alpha;
+    let alpha6 = &alpha5 * alpha;
+
+    // Precompute constants that are the same for all addresses
+    let is_register = FieldElement::<E>::one(); // is_register = 1
+    // addr_hi = 0, contributes nothing
+    let base_lc = &bus_id + &(&is_register * alpha);
+
+    // Fini timestamp: ts = u64::MAX = 0xFFFFFFFF_FFFFFFFF
+    let ts_lo = FieldElement::<E>::from(0xFFFF_FFFFu64);
+    let ts_hi = FieldElement::<E>::from(0xFFFF_FFFFu64);
+    let fini_ts_contrib = &(&ts_lo * &alpha4) + &(&ts_hi * &alpha5);
+
+    let mut total = FieldElement::<E>::zero();
+
+    let addr_list = register::register_word_address_list();
+
+    for &addr in &addr_list {
+        let addr_fe = FieldElement::<E>::from(addr);
+        let addr_contrib = &addr_fe * &alpha2;
+
+        // Init value: deterministic from entry_point
+        let init_value = register::init_value_for_address(addr, entry_point);
+
+        // Fini value: deterministic after HALT finalization
+        // HALT writes 0 to all registers except x255 which gets value=1.
+        // x255 lo word (addr 510) → fini=1, x255 hi word (addr 511) → fini=0.
+        let fini_value: u32 = if addr == 510 { 1 } else { 0 };
+
+        // REG-C1 (receiver, sign=-1): init token with ts=0
+        // lc = base_lc + addr * α^2 + 0*α^3 + 0*α^4 + 0*α^5 + init_value * α^6
+        let lc_init = &base_lc
+            + &addr_contrib
+            + &(FieldElement::<E>::from(init_value as u64) * &alpha6);
+        let fp_init = z - &lc_init;
+        let inv_init = fp_init.inv().ok()?;
+        total = total - inv_init; // receiver: -1/fp
+
+        // REG-C2 (sender, sign=+1): fini token with ts=MAX
+        // lc = base_lc + addr * α^2 + 0*α^3 + MAX_LO*α^4 + MAX_HI*α^5 + fini_value * α^6
+        let lc_fini = &base_lc
+            + &addr_contrib
+            + &fini_ts_contrib
+            + &(FieldElement::<E>::from(fini_value as u64) * &alpha6);
+        let fp_fini = z - &lc_fini;
+        let inv_fini = fp_fini.inv().ok()?;
+        total = total + inv_fini; // sender: +1/fp
+    }
+
+    Some(total)
+}
+
+/// Compute the expected bus balance for a `MultiProof`.
 ///
 /// Replays Phase A of the transcript to recover (z, alpha), then computes
-/// the offset from the given public output bytes. Call this after `multi_prove`
-/// and before `multi_verify`.
-pub(crate) fn compute_expected_commit_bus_balance(
+/// the combined offset from:
+/// 1. COMMIT output bus (public output bytes)
+/// 2. REGISTER Memory bus (verifier-computed init/fini tokens)
+///
+/// Call this after `multi_prove` and before `multi_verify`.
+pub(crate) fn compute_expected_bus_balance(
     airs: &[&dyn AIR<Field = F, FieldExtension = E, PublicInputs = ()>],
     proof: &MultiProof<F, E, ()>,
     public_output_bytes: &[u8],
+    entry_point: u64,
 ) -> Option<FieldElement<E>> {
     let (z, alpha) = replay_transcript_phase_a(airs, proof);
-    compute_commit_bus_offset(public_output_bytes, &z, &alpha)
+    let commit_offset = compute_commit_bus_offset(public_output_bytes, &z, &alpha)?;
+    let register_offset = compute_register_bus_offset(entry_point, &z, &alpha)?;
+    Some(commit_offset + register_offset)
 }
 
 // =============================================================================
@@ -612,11 +695,12 @@ pub fn verify_with_options(
         Traces::page_configs_from_elf_and_runtime(&program, &vm_proof.runtime_page_ranges);
 
     // Cross-check: table_counts must match the number of sub-proofs.
-    // Fixed tables (bitwise, decode, halt, commit, register) = 5, plus page tables.
-    let expected_proof_count = vm_proof.table_counts.total() + 5 + page_configs.len();
+    // Fixed tables (bitwise, decode, halt, commit) = 4, plus page tables.
+    // REGISTER table is eliminated: its bus contribution is verifier-computed.
+    let expected_proof_count = vm_proof.table_counts.total() + 4 + page_configs.len();
     if expected_proof_count != vm_proof.proof.proofs.len() {
         return Err(Error::InvalidTableCounts(format!(
-            "table_counts total ({}) + 5 fixed + {} pages = {}, but proof contains {} sub-proofs",
+            "table_counts total ({}) + 4 fixed + {} pages = {}, but proof contains {} sub-proofs",
             vm_proof.table_counts.total(),
             page_configs.len(),
             expected_proof_count,
@@ -632,14 +716,16 @@ pub fn verify_with_options(
         &vm_proof.table_counts,
     );
 
-    // Recompute the COMMIT output bus offset from VmProof.public_output.
-    // If public_output was tampered, the recomputed offset won't match the
-    // actual bus total in the proof, and multi_verify will reject.
+    // Recompute bus offsets from verifier-known data:
+    // 1. COMMIT output bus: from VmProof.public_output
+    // 2. REGISTER Memory bus: from ELF entry_point (init/fini are deterministic)
+    // Tampering with either will cause bus imbalance and multi_verify rejection.
     let air_refs = airs.air_refs();
-    let expected_bus_balance = match compute_expected_commit_bus_balance(
+    let expected_bus_balance = match compute_expected_bus_balance(
         &air_refs,
         &vm_proof.proof,
         &vm_proof.public_output,
+        program.entry_point,
     ) {
         Some(balance) => balance,
         None => return Ok(false),

prover/src/tables/halt.rs

@@ -131,16 +131,43 @@ fn halt_write_bus_values(base_addr: u64, value_lo: u64) -> Vec<BusValue> {
     ]
 }
 
+/// Returns the 16-element MEMW write bus values for a width-1 register finalization.
+///
+/// Format matches CO17 (write receiver): `[is_register, base_addr[0..1], value[0..7],
+/// timestamp[0..1], write2, write4, write8]` with write2=write4=write8=0 (width=1).
+fn halt_write_bus_values_w1(base_addr: u64, value_lo: u64) -> Vec<BusValue> {
+    vec![
+        BusValue::constant(1),           // is_register = 1
+        BusValue::constant(base_addr),   // base_address[0]
+        BusValue::constant(0),           // base_address[1]
+        BusValue::constant(value_lo),    // value[0]
+        BusValue::constant(0),           // value[1]
+        BusValue::constant(0),           // value[2]
+        BusValue::constant(0),           // value[3]
+        BusValue::constant(0),           // value[4]
+        BusValue::constant(0),           // value[5]
+        BusValue::constant(0),           // value[6]
+        BusValue::constant(0),           // value[7]
+        BusValue::constant(0xFFFF_FFFF), // timestamp[0] = lo(2^64-1)
+        BusValue::constant(0xFFFF_FFFF), // timestamp[1] = hi(2^64-1)
+        BusValue::constant(0),           // write2 = 0 (width-1)
+        BusValue::constant(0),           // write4 = 0
+        BusValue::constant(0),           // write8 = 0
+    ]
+}
+
 /// Creates all bus interactions for the HALT table.
 ///
 /// - **ECALL receiver**: receives `[timestamp, cast(rv1, DWordWL)]` from CPU
-/// - **MEMW senders** (32 total): register finalization at `ts = 2^64-1`
+/// - **MEMW senders** (34 total): register finalization at `ts = 2^64-1`
+///   - x0: write 0 (explicit finalization for verifier-computed bus balance)
 ///   - x1-x9: write 0 (zeroize lo GPRs)
 ///   - x10: read with old=0 (enforce exit_code=0)
 ///   - x11-x31: write 0 (zeroize hi GPRs)
+///   - x254: write 0 (finalize commit index, width-1)
 ///   - x255: write 1 (PC halted sentinel)
 pub fn bus_interactions() -> Vec<BusInteraction> {
-    let mut interactions = Vec::with_capacity(33);
+    let mut interactions = Vec::with_capacity(36);
 
     // ECALL receiver: receives [timestamp, cast(rv1, DWordWL)] from CPU
     // rv1 must be 93 (sys_exit) for bus to balance; otherwise proof fails.
@@ -161,6 +188,15 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
         ],
     ));
 
+    // x0: write 0 at ts=2^64-1 (explicit finalization)
+    // x0 is hardwired zero, but we finalize it so the verifier can compute
+    // the REGISTER bus balance deterministically (no self-cancellation needed).
+    interactions.push(BusInteraction::sender(
+        BusId::Memw,
+        Multiplicity::One,
+        halt_write_bus_values(0, 0),
+    ));
+
     // x1-x9: write 0 at ts=2^64-1 (zeroize lo registers)
     for i in 1..=9u64 {
         interactions.push(BusInteraction::sender(
@@ -188,6 +224,14 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
         ));
     }
 
+    // x254 (commit index): write 0 at ts=2^64-1 (finalize, width-1)
+    // Single-word register at address 508; uses width-1 format (write2=0).
+    interactions.push(BusInteraction::sender(
+        BusId::Memw,
+        Multiplicity::One,
+        halt_write_bus_values_w1(508, 0),
+    ));
+
     // x255 (PC): write 1 at ts=2^64-1 (halted sentinel)
     interactions.push(BusInteraction::sender(
         BusId::Memw,

prover/src/tables/register.rs

@@ -100,7 +100,7 @@ pub type FinalRegisterStateMap = HashMap<u64, FinalRegisterWordState>;
 /// Returns the Word addresses for all register table rows.
 ///
 /// x0-x31 use addresses 0..63, x254 uses address 508, x255 uses 510..511.
-fn register_word_address_list() -> [u64; NUM_REGISTER_ADDRESSES] {
+pub(crate) fn register_word_address_list() -> [u64; NUM_REGISTER_ADDRESSES] {
     let mut addrs = [0u64; NUM_REGISTER_ADDRESSES];
     // x0-x31: addresses 0..63
     for (i, addr) in addrs.iter_mut().enumerate().take(64) {
@@ -120,7 +120,7 @@ fn register_word_address_list() -> [u64; NUM_REGISTER_ADDRESSES] {
 /// - x254 at offset 508 is the synthetic commit index, initialized to 0
 /// - PC (x255) words at offset 510,511 hold entry_point
 /// - All others are 0
-fn init_value_for_address(word_addr: u64, entry_point: u64) -> u32 {
+pub(crate) fn init_value_for_address(word_addr: u64, entry_point: u64) -> u32 {
     match word_addr {
         4 => (STACK_TOP & 0xFFFF_FFFF) as u32,
         5 => (STACK_TOP >> 32) as u32,