nova support evaluate shared constraints

powdr-labs · Aug 11, 2023 · 9f03bc7 · 9f03bc7
1 parent 495aede
commit 9f03bc7
Show file tree

Hide file tree

Showing 2 changed files with 79 additions and 15 deletions.
diff --git a/nova/src/circuit.rs b/nova/src/circuit.rs
@@ -188,7 +188,10 @@ where
             |lc| lc + expected_opcode_index.get_variable(),
         );
 
-        for id in &self.analyzed.identities {
+        // process identites
+        // all the shared constraints will be compiled into each augmented circuit
+        // TODO optimized to compile only nessesary shared constraints
+        for (index, id) in self.analyzed.identities.iter().enumerate() {
             match id.kind {
                 IdentityKind::Polynomial => {
                     // everthing should be in left.selector only
@@ -198,22 +201,34 @@ where
 
                     let exp = id.expression_for_poly_id();
 
+                    // identities process as below
+                    // case 1: ((main.instr_XXXX * ) - 0) = 0 => `BinaryOperation(BinaryOperation... `
+                    // case 1.1: (() - 0) = 0 => `BinaryOperation(BinaryOperation... `
+                    // case 2: PolynomialReference - () = 0 => `BinaryOperation(PolynomialReference...`
                     match exp {
+                        // case 1/1.1
                         Expression::BinaryOperation(
                             box Expression::BinaryOperation(
                                 box Expression::PolynomialReference(
-                                    PolynomialReference { name, .. },
+                                    PolynomialReference { name, next, .. },
                                     ..,
                                 ),
-                                BinaryOperator::Mul,
+                                _,
                                 box rhs,
                             ),
                             ..,
                         ) => {
-                            // only build constraints on matched identities
-                            // TODO replace with better regular expression ?
-                            if !(name.starts_with("main.instr")
-                                && name.ends_with(&self.identity_name[..]))
+                            // skip next
+                            if *next {
+                                unimplemented!("not support column next in folding scheme")
+                            }
+                            // skip first_step, for it's not being used in folding scheme
+                            if name == "main.first_step" {
+                                continue;
+                            }
+                            // only skip if constraint is dedicated to other instruction
+                            if name.starts_with("main.instr")
+                                && !name.ends_with(&self.identity_name[..])
                             {
                                 continue;
                             }
@@ -222,21 +237,56 @@ where
                             if contains_next_ref {
                                 unimplemented!("not support column next in folding scheme")
                             }
-                            let mut cs = cs.namespace(|| format!("rhs {}", rhs));
+                            let num_eval = if name.starts_with("main.instr")
+                                && name.ends_with(&self.identity_name[..])
+                            {
+                                evaluate_expr(
+                                    cs.namespace(|| format!("id index {} rhs {}", index, rhs)),
+                                    &mut poly_map,
+                                    rhs,
+                                    self.witgen.clone(),
+                                )?
+                            } else {
+                                evaluate_expr(
+                                    cs.namespace(|| format!("id index {} exp {}", index, exp)),
+                                    &mut poly_map,
+                                    exp,
+                                    self.witgen.clone(),
+                                )?
+                            };
+                            cs.enforce(
+                                || format!("id index {} constraint {} = 0", index, name),
+                                |lc| lc + num_eval.get_variable(),
+                                |lc| lc + CS::one(),
+                                |lc| lc,
+                            );
+                        }
+                        // case 2
+                        Expression::BinaryOperation(
+                            box Expression::PolynomialReference(
+                                PolynomialReference { name, next, .. },
+                                ..,
+                            ),
+                            _,
+                            _,
+                        ) => {
+                            if *next {
+                                continue;
+                            }
                             let num_eval = evaluate_expr(
-                                cs.namespace(|| format!("constraint {}", name)),
+                                cs.namespace(|| format!("id index {} exp {}", index, exp)),
                                 &mut poly_map,
-                                rhs,
+                                exp,
                                 self.witgen.clone(),
                             )?;
                             cs.enforce(
-                                || format!("constraint {} = 0", name),
+                                || format!("id index {} constraint {} = 0", index, name),
                                 |lc| lc + num_eval.get_variable(),
                                 |lc| lc + CS::one(),
                                 |lc| lc,
                             );
                         }
-                        _ => (), // println!("exp {:?} not support", exp),
+                        _ => unimplemented!("exp {:?} not support", exp),
                     }
                 }
                 _ => (),

diff --git a/nova/zero.asm b/nova/zero.asm
@@ -1,6 +1,6 @@
 machine NovaZero {
 
-    degree 20;
+    degree 32;
 
     // this simple machine does not have submachines
 
@@ -11,6 +11,14 @@ machine NovaZero {
     reg x0;
     reg x1;
 
+    constraints {
+        col witness XInv;
+        col witness XIsZero;
+        XIsZero = 1 - X * XInv;
+        XIsZero * X = 0;
+        XIsZero * (1 - XIsZero) = 0;
+    }
+
     constraints {
         col witness x_b0;
         col witness x_b1;
@@ -27,7 +35,7 @@ machine NovaZero {
 
     instr incr X -> Y {
         Y = X + 1,
-        Y = x_b0 + x_b1 * 2 + x_b2 * 2**2 + x_b3 * 2**3,
+        X = x_b0 + x_b1 * 2 + x_b2 * 2**2 + x_b3 * 2**3,
         pc' = pc + 1
     }
 
@@ -55,6 +63,11 @@ machine NovaZero {
         pc' = pc
     }
 
+    // an instruction only proceed pc + 1 if X = 0
+    instr contz X {
+        pc' = (1 - XIsZero) * (pc - 1) + XIsZero * (pc + 1)
+    }
+
     instr assert_zero X {
         X = 0
     }
@@ -74,7 +87,8 @@ machine NovaZero {
         x0 <=Z= sub(x0, x0); // x0 - x0 = 0
         assert_zero x0; // x0 == 0
         x1 <=X= ${ ("input", 1) };
-        x1 <=Z= sub(x1, x1); // x1 - x1 = 0
+        x1 <=Z= addi(x1, -1);
+        contz x1;
         assert_zero x1; // x1 == 0
         loop;
     }