Feat/structural witin add (#740)

Work for #654

---------

Co-authored-by: sm.wu <[email protected]>
Co-authored-by: Matthias Görgens <[email protected]>
Co-authored-by: Ho <[email protected]>
Co-authored-by: mcalancea <[email protected]>
Co-authored-by: noelwei <[email protected]>

Author: 5 people

ceno_zkvm/src/chip_handler/general.rs

@@ -3,7 +3,7 @@ use ff_ext::ExtensionField;
 use crate::{
     circuit_builder::{CircuitBuilder, ConstraintSystem, SetTableSpec},
     error::ZKVMError,
-    expression::{Expression, Fixed, Instance, ToExpr, WitIn},
+    expression::{Expression, Fixed, Instance, StructuralWitIn, ToExpr, WitIn},
     instructions::riscv::constants::{
         END_CYCLE_IDX, END_PC_IDX, EXIT_CODE_IDX, INIT_CYCLE_IDX, INIT_PC_IDX, PUBLIC_IO_IDX,
         UINT_LIMBS,
@@ -28,6 +28,21 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> {
         self.cs.create_witin(name_fn)
     }
 
+    pub fn create_structural_witin<NR, N>(
+        &mut self,
+        name_fn: N,
+        max_len: usize,
+        offset: u32,
+        multi_factor: usize,
+    ) -> StructuralWitIn
+    where
+        NR: Into<String>,
+        N: FnOnce() -> NR,
+    {
+        self.cs
+            .create_structural_witin(name_fn, max_len, offset, multi_factor)
+    }
+
     pub fn create_fixed<NR, N>(&mut self, name_fn: N) -> Result<Fixed, ZKVMError>
     where
         NR: Into<String>,

ceno_zkvm/src/circuit_builder.rs

@@ -9,7 +9,7 @@ use crate::{
     ROMType,
     chip_handler::utils::rlc_chip_record,
     error::ZKVMError,
-    expression::{Expression, Fixed, Instance, WitIn},
+    expression::{Expression, Fixed, Instance, StructuralWitIn, WitIn},
     structs::{ProgramParams, ProvingKey, RAMType, VerifyingKey, WitnessId},
     witness::RowMajorMatrix,
 };
@@ -59,14 +59,6 @@ pub struct LogupTableExpression<E: ExtensionField> {
     pub table_len: usize,
 }
 
-// TODO encapsulate few information of table spec to SetTableAddrType value
-// once confirm syntax is friendly and parsed by recursive verifier
-#[derive(Clone, Debug)]
-pub enum SetTableAddrType {
-    FixedAddr,
-    DynamicAddr(DynamicAddr),
-}
-
 #[derive(Clone, Debug)]
 pub struct DynamicAddr {
     pub addr_witin_id: usize,
@@ -75,12 +67,13 @@ pub struct DynamicAddr {
 
 #[derive(Clone, Debug)]
 pub struct SetTableSpec {
-    pub addr_type: SetTableAddrType,
-    pub len: usize,
+    pub len: Option<usize>,
+    pub structural_witins: Vec<StructuralWitIn>,
 }
 
 #[derive(Clone, Debug)]
 pub struct SetTableExpression<E: ExtensionField> {
+    /// table expression
     pub expr: Expression<E>,
 
     // TODO make decision to have enum/struct
@@ -92,10 +85,12 @@ pub struct SetTableExpression<E: ExtensionField> {
 pub struct ConstraintSystem<E: ExtensionField> {
     pub(crate) ns: NameSpace,
 
-    // pub platform: Platform,
     pub num_witin: WitnessId,
     pub witin_namespace_map: Vec<String>,
 
+    pub num_structural_witin: WitnessId,
+    pub structural_witin_namespace_map: Vec<String>,
+
     pub num_fixed: usize,
     pub fixed_namespace_map: Vec<String>,
 
@@ -152,6 +147,8 @@ impl<E: ExtensionField> ConstraintSystem<E> {
             num_witin: 0,
             // platform,
             witin_namespace_map: vec![],
+            num_structural_witin: 0,
+            structural_witin_namespace_map: vec![],
             num_fixed: 0,
             fixed_namespace_map: vec![],
             ns: NameSpace::new(root_name_fn),
@@ -209,20 +206,36 @@ impl<E: ExtensionField> ConstraintSystem<E> {
     }
 
     pub fn create_witin<NR: Into<String>, N: FnOnce() -> NR>(&mut self, n: N) -> WitIn {
-        let wit_in = WitIn {
-            id: {
-                let id = self.num_witin;
-                self.num_witin = self.num_witin.strict_add(1);
-                id
-            },
-        };
+        let wit_in = WitIn { id: self.num_witin };
+        self.num_witin = self.num_witin.strict_add(1);
 
         let path = self.ns.compute_path(n().into());
         self.witin_namespace_map.push(path);
 
         wit_in
     }
 
+    pub fn create_structural_witin<NR: Into<String>, N: FnOnce() -> NR>(
+        &mut self,
+        n: N,
+        max_len: usize,
+        offset: u32,
+        multi_factor: usize,
+    ) -> StructuralWitIn {
+        let wit_in = StructuralWitIn {
+            id: self.num_structural_witin,
+            max_len,
+            offset,
+            multi_factor,
+        };
+        self.num_structural_witin = self.num_structural_witin.strict_add(1);
+
+        let path = self.ns.compute_path(n().into());
+        self.structural_witin_namespace_map.push(path);
+
+        wit_in
+    }
+
     pub fn create_fixed<NR: Into<String>, N: FnOnce() -> NR>(
         &mut self,
         n: N,