Feat/shrink cpu byte alu (#644)

* Add shrink-cpu buses, decode layout, EQ chip

* Add BYTEWISE ALU chip

* Add BYTEWISE, STORE and CPU32 chips

* Add CPU32 buses; fix EQ ALU output width

* Register EQ/BYTEWISE/STORE/CPU32 as empty tables

* Migrate CPU + ALU/memory chips to unified ALU bus

* Delegate word instructions to the CPU32 table

* Re-enable and rewrite CPU/decode/constraint tests for the shrink-cpu layout,
   and document the deviations

* remove unnecesary files

* Unify LT/MUL/memw/dvrm onto the ALU bus

* Pin JALR rvd to pc+len

* Align SHIFT shift-amount layout with the spec

* reconcile prover with shrink-cpu spec

* Add spec assumption range checks

* Add explicit IS_BYTE[shift[0]] range check

* Sync CPU with merged shrink-cpu spec

* remove old comments

* use constants

* Propagate carry in branch rvd constraint

* prevent register side effects in CPU32 padding

* Use unreachable for validated carry arms

* Force signed to zero on CPU32 padding rows

* Force res_sign to zero on CPU32 padding rows

* Gate CPU32 sign lookups by signed

* close LT/SHIFT/LOAD underconstrained gaps

* Remove dead LT carry helper and fix stale comments

* Remove legacy byte-op buses

---------

Co-authored-by: Diego K <43053772+diegokingston@users.noreply.github.com>
Co-authored-by: MauroFab <maurotoscano2@gmail.com>
Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com>

Author: 3 people

prover/src/constraints/cpu.rs

@@ -449,7 +449,7 @@ impl AddConstraint {
         let carry = match self.carry_idx {
             0 => self.compute_carry_0(step),
             1 => self.compute_carry_1(step),
-            _ => panic!("Invalid carry index"),
+            _ => unreachable!("carry_idx validated <= 1 at construction"),
         };
 
         if self.cond_cols.is_empty() {

prover/src/constraints/templates.rs

@@ -48,11 +48,12 @@ use crate::tables::trace_builder::Traces;
 use crate::tables::trace_builder::count_table_lengths;
 use crate::tables::types::BusId;
 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_keccak_air, create_keccak_rc_air,
-    create_keccak_rnd_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,
+    E, F, VmAir, create_bitwise_air, create_branch_air, create_bytewise_air, create_commit_air,
+    create_cpu_air, create_cpu32_air, create_decode_air, create_dvrm_air, create_eq_air,
+    create_halt_air, create_keccak_air, create_keccak_rc_air, create_keccak_rnd_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_store_air,
 };
 
 use stark::proof::options::{GoldilocksCubicProofOptions, ProofOptions};
@@ -84,6 +85,11 @@ pub struct TableCounts {
     pub shift: usize,
     pub branch: usize,
     pub memw_register: usize,
+    // Auxiliary ALU / memory / CPU32 dispatch chips
+    pub eq: usize,
+    pub bytewise: usize,
+    pub store: usize,
+    pub cpu32: usize,
 }
 
 impl TableCounts {
@@ -99,6 +105,10 @@ impl TableCounts {
             + self.shift
             + self.branch
             + self.memw_register
+            + self.eq
+            + self.bytewise
+            + self.store
+            + self.cpu32
     }
 
     /// Validate that all required tables have at least one chunk.
@@ -117,6 +127,10 @@ impl TableCounts {
             ("shift", self.shift),
             ("branch", self.branch),
             ("memw_register", self.memw_register),
+            ("eq", self.eq),
+            ("bytewise", self.bytewise),
+            ("store", self.store),
+            ("cpu32", self.cpu32),
         ];
         for (name, count) in checks {
             if count == 0 {
@@ -212,6 +226,11 @@ pub(crate) struct VmAirs {
     pub register: VmAir,
     pub pages: Vec<VmAir>,
     pub memw_registers: Vec<VmAir>,
+    // Auxiliary ALU / memory / CPU32 dispatch chips
+    pub eqs: Vec<VmAir>,
+    pub bytewises: Vec<VmAir>,
+    pub stores: Vec<VmAir>,
+    pub cpu32s: Vec<VmAir>,
 }
 
 impl VmAirs {
@@ -269,6 +288,18 @@ impl VmAirs {
         {
             pairs.push((air, trace, &()));
         }
+        for (air, trace) in self.eqs.iter().zip(traces.eqs.iter_mut()) {
+            pairs.push((air, trace, &()));
+        }
+        for (air, trace) in self.bytewises.iter().zip(traces.bytewises.iter_mut()) {
+            pairs.push((air, trace, &()));
+        }
+        for (air, trace) in self.stores.iter().zip(traces.stores.iter_mut()) {
+            pairs.push((air, trace, &()));
+        }
+        for (air, trace) in self.cpu32s.iter().zip(traces.cpu32s.iter_mut()) {
+            pairs.push((air, trace, &()));
+        }
 
         pairs
     }
@@ -319,6 +350,18 @@ impl VmAirs {
         for air in &self.memw_registers {
             refs.push(air);
         }
+        for air in &self.eqs {
+            refs.push(air);
+        }
+        for air in &self.bytewises {
+            refs.push(air);
+        }
+        for air in &self.stores {
+            refs.push(air);
+        }
+        for air in &self.cpu32s {
+            refs.push(air);
+        }
 
         refs
     }
@@ -454,6 +497,18 @@ impl VmAirs {
         let memw_registers: Vec<_> = (0..table_counts.memw_register)
             .map(|i| create_memw_register_air(proof_options).with_name(&format!("MEMW_R[{}]", i)))
             .collect();
+        let eqs: Vec<_> = (0..table_counts.eq)
+            .map(|i| create_eq_air(proof_options).with_name(&format!("EQ[{}]", i)))
+            .collect();
+        let bytewises: Vec<_> = (0..table_counts.bytewise)
+            .map(|i| create_bytewise_air(proof_options).with_name(&format!("BYTEWISE[{}]", i)))
+            .collect();
+        let stores: Vec<_> = (0..table_counts.store)
+            .map(|i| create_store_air(proof_options).with_name(&format!("STORE[{}]", i)))
+            .collect();
+        let cpu32s: Vec<_> = (0..table_counts.cpu32)
+            .map(|i| create_cpu32_air(proof_options).with_name(&format!("CPU32[{}]", i)))
+            .collect();
 
         #[cfg(feature = "debug-checks")]
         debug_report::print_bus_legend();
@@ -478,6 +533,10 @@ impl VmAirs {
             register,
             pages,
             memw_registers,
+            eqs,
+            bytewises,
+            stores,
+            cpu32s,
         }
     }
 }

prover/src/lib.rs

@@ -16,7 +16,7 @@ use crate::test_utils::E;
 use crate::{RuntimePageRange, TableCounts};
 
 /// Domain-separation tag. Bump the suffix (`_V2`, ...) on any encoding change.
-const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V1";
+const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V2";
 
 fn elf_digest(elf: &[u8]) -> [u8; 32] {
     let mut h = Keccak256::new();
@@ -55,6 +55,10 @@ pub(crate) fn absorb_statement(
         shift,
         branch,
         memw_register,
+        eq,
+        bytewise,
+        store,
+        cpu32,
     } = table_counts;
     for count in [
         cpu,
@@ -67,6 +71,10 @@ pub(crate) fn absorb_statement(
         shift,
         branch,
         memw_register,
+        eq,
+        bytewise,
+        store,
+        cpu32,
     ] {
         t.append_bytes(&(count as u64).to_le_bytes());
     }