improve AIR constraints for execution table

Author: TomWambsgans

crates/lean_vm/src/tables/execution/air.rs

@@ -74,7 +74,7 @@ impl<const BUS: bool> Air for ExecutionTable<BUS> {
         vec![]
     }
     fn n_constraints(&self) -> usize {
-        16
+        14
     }
 
     #[inline]
@@ -158,14 +158,14 @@ impl<const BUS: bool> Air for ExecutionTable<BUS> {
         builder.assert_zero(deref.clone() * aux.clone() * (value_c.clone() - nu_b.clone()));
         builder.assert_zero(deref.clone() * (aux.clone() - AB::F::ONE) * (value_c.clone() - fp.clone()));
 
-        builder.assert_zero((jump.clone() - AB::F::ONE) * (next_pc.clone() - pc_plus_one.clone()));
-        builder.assert_zero((jump.clone() - AB::F::ONE) * (next_fp.clone() - fp.clone()));
+        let jump_and_condition = jump.clone() * nu_a.clone();
 
-        builder.assert_zero(jump.clone() * nu_a.clone() * nu_a_minus_one.clone());
-        builder.assert_zero(jump.clone() * nu_a.clone() * (next_pc.clone() - nu_b.clone()));
-        builder.assert_zero(jump.clone() * nu_a.clone() * (next_fp.clone() - nu_c.clone()));
-        builder.assert_zero(jump.clone() * nu_a_minus_one.clone() * (next_pc.clone() - pc_plus_one.clone()));
-        builder.assert_zero(jump.clone() * nu_a_minus_one.clone() * (next_fp.clone() - fp.clone()));
+        builder.assert_zero(jump_and_condition.clone() * nu_a_minus_one.clone());
+        builder.assert_zero(jump_and_condition.clone() * (next_pc.clone() - nu_b.clone()));
+        builder.assert_zero(jump_and_condition.clone() * (next_fp.clone() - nu_c.clone()));
+        let not_jump_and_condition = AB::F::ONE - jump_and_condition;
+        builder.assert_zero(not_jump_and_condition.clone() * (next_pc.clone() - pc_plus_one.clone()));
+        builder.assert_zero(not_jump_and_condition * (next_fp.clone() - fp.clone()));
     }
 }
 

misc/minimal_zkVM.tex

@@ -413,21 +413,13 @@ \subsubsection{AIR transition constraints}
 
 \vspace{3mm}\centerline{\rule{10cm}{0.4pt}}\vspace{5mm}
 
-When there is no jump:
+For jump and conditional state transitions, let $J = \text{JUMP} \cdot \nu_A$:
 \begin{itemize}
-    \item $(1 - \text{JUMP}) \cdot ( \text{next(pc)} - (\text{pc} + 1)) = 0$
-    \item $(1 - \text{JUMP}) \cdot (\text{next(fp)} - \text{fp}) = 0$
-\end{itemize}
-
-\vspace{3mm}
-
-When JUMP $= 1$, the condition is represented by $\nu_A$:
-\begin{itemize}
-    \item $\text{JUMP} \cdot \nu_A \cdot (1 - \nu_A) = 0$ 
-    \item $\text{JUMP} \cdot \nu_A \cdot ( \text{next(pc)} - \nu_B) = 0$
-    \item $\text{JUMP} \cdot \nu_A \cdot ( \text{next(fp)} - \nu_C) = 0$
-    \item $\text{JUMP} \cdot (1 - \nu_A) \cdot ( \text{next(pc)} - (\text{pc} + 1)) = 0$
-    \item $\text{JUMP} \cdot (1 - \nu_A) \cdot (\text{next(fp)} - \text{fp}) = 0$
+    \item $\text{JUMP} \cdot \nu_A \cdot (1 - \nu_A) = 0$
+    \item $J \cdot ( \text{next(pc)} - \nu_B) = 0$
+    \item $J \cdot ( \text{next(fp)} - \nu_C) = 0$
+    \item $(1 - J) \cdot ( \text{next(pc)} - (\text{pc} + 1)) = 0$
+    \item $(1 - J) \cdot (\text{next(fp)} - \text{fp}) = 0$
 \end{itemize}
 
 Note: the constraint $\text{JUMP} \cdot \nu_A \cdot (1 - \nu_A) = 0$ could be removed, as long as it's correctly enforced in the bytecode.