expose mock-proving as a separate CLI step

compiler/src/lib.rs

@@ -2,16 +2,17 @@
 
 use std::ffi::OsStr;
 use std::fs;
-use std::io::{BufWriter, Write};
+use std::io::BufWriter;
 use std::path::Path;
 use std::time::Instant;
 
 mod verify;
+use number::write_polys_file;
 use pil_analyzer::json_exporter;
 pub use verify::{compile_asm_string_temp, verify, verify_asm_string};
 
 use executor::constant_evaluator;
-use number::{DegreeType, FieldElement};
+use number::FieldElement;
 use parser::ast::PILFile;
 
 pub fn no_callback<T>() -> Option<fn(&str) -> Option<T>> {
@@ -160,20 +161,6 @@ fn compile<T: FieldElement>(
     success
 }
 
-fn write_polys_file<T: FieldElement>(
-    file: &mut impl Write,
-    degree: DegreeType,
-    polys: &Vec<(&str, Vec<T>)>,
-) {
-    for i in 0..degree as usize {
-        for (_name, constant) in polys {
-            let bytes = constant[i].to_bytes_le();
-            assert_eq!(bytes.len(), 8);
-            file.write_all(&bytes).unwrap();
-        }
-    }
-}
-
 fn inputs_to_query_callback<T: FieldElement>(inputs: Vec<T>) -> impl Fn(&str) -> Option<T> {
     move |query: &str| -> Option<T> {
         let items = query.split(',').map(|s| s.trim()).collect::<Vec<_>>();

executor/src/witgen/bit_constraints.rs

@@ -1,7 +1,6 @@
 use std::collections::{BTreeMap, BTreeSet};
 use std::fmt::{Debug, Display, Formatter};
 
-use crate::witgen::util::contains_next_ref;
 use number::{log2_exact, BigInt, FieldElement};
 use pil_analyzer::{BinaryOperator, Expression, Identity, IdentityKind, PolynomialReference};
 
@@ -286,7 +285,7 @@ fn try_transfer_constraints<'a, 'b, T: FieldElement>(
     expr: &'a Expression<T>,
     known_constraints: &'b BTreeMap<&'b PolynomialReference, BitConstraint<T>>,
 ) -> Option<(&'a PolynomialReference, BitConstraint<T>)> {
-    if contains_next_ref(expr) {
+    if expr.contains_next_ref() {
         return None;
     }
 

executor/src/witgen/generator.rs

@@ -12,7 +12,6 @@ use super::bit_constraints::{BitConstraint, BitConstraintSet};
 use super::expression_evaluator::ExpressionEvaluator;
 use super::machines::{FixedLookup, Machine};
 use super::symbolic_witness_evaluator::{SymoblicWitnessEvaluator, WitnessColumnEvaluator};
-use super::util::contains_next_witness_ref;
 use super::{Constraint, EvalResult, EvalValue, FixedData, IncompleteCause, WitnessColumn};
 
 pub struct Generator<'a, T: FieldElement, QueryCallback> {
@@ -146,8 +145,6 @@ where
                 break;
             }
         }
-        // Identity check failure on the first row is not fatal. We will proceed with
-        // "unknown", report zero and re-check the wrap-around against the zero values at the end.
         if identity_failed {
             log::error!(
                 "\nError: Row {next_row}: Identity check failed or unable to derive values for some witness columns.\nSet RUST_LOG=debug for more information.");
@@ -357,7 +354,7 @@ where
     fn process_polynomial_identity<'b>(&self, identity: &'b Expression<T>) -> EvalResult<'b, T> {
         // If there is no "next" reference in the expression,
         // we just evaluate it directly on the "next" row.
-        let row = if contains_next_witness_ref(identity) {
+        let row = if identity.contains_next_witness_ref() {
             // TODO this is the only situation where we use "current"
             // TODO this is the only that actually uses a window.
             EvaluationRow::Current

executor/src/witgen/machines/fixed_lookup_machine.rs

@@ -8,8 +8,8 @@ use pil_analyzer::{Identity, IdentityKind, PolyID, PolynomialReference, Selected
 
 use crate::witgen::affine_expression::AffineResult;
 use crate::witgen::util::try_to_simple_poly_ref;
-use crate::witgen::{util::contains_witness_ref, EvalResult, FixedData};
 use crate::witgen::{EvalError, EvalValue, IncompleteCause};
+use crate::witgen::{EvalResult, FixedData};
 
 type Application = (Vec<u64>, Vec<u64>);
 type Index<T> = BTreeMap<Vec<T>, IndexValue>;
@@ -185,7 +185,7 @@ impl<T: FieldElement> FixedLookup<T> {
         // This is a matching machine if it is a plookup and the RHS is fully constant.
         if kind != IdentityKind::Plookup
             || right.selector.is_some()
-            || right.expressions.iter().any(contains_witness_ref)
+            || right.expressions.iter().any(|e| e.contains_witness_ref())
         {
             return None;
         }

executor/src/witgen/util.rs

@@ -1,33 +1,8 @@
 use std::collections::HashMap;
 
-use pil_analyzer::util::{expr_any, previsit_expressions_in_identity_mut};
+use pil_analyzer::util::previsit_expressions_in_identity_mut;
 use pil_analyzer::{Expression, Identity, PolyID, PolynomialReference};
 
-/// @returns true if the expression contains a reference to a next value of a
-/// (witness or fixed) column
-pub fn contains_next_ref<T>(expr: &Expression<T>) -> bool {
-    expr_any(expr, |e| match e {
-        Expression::PolynomialReference(poly) => poly.next,
-        _ => false,
-    })
-}
-
-/// @returns true if the expression contains a reference to a next value of a witness column.
-pub fn contains_next_witness_ref<T>(expr: &Expression<T>) -> bool {
-    expr_any(expr, |e| match e {
-        Expression::PolynomialReference(poly) => poly.next && poly.is_witness(),
-        _ => false,
-    })
-}
-
-/// @returns true if the expression contains a reference to a witness column.
-pub fn contains_witness_ref<T>(expr: &Expression<T>) -> bool {
-    expr_any(expr, |e| match e {
-        Expression::PolynomialReference(poly) => poly.is_witness(),
-        _ => false,
-    })
-}
-
 /// Checks if an expression is
 /// - a polynomial
 /// - not part of a polynomial array

halo2/Cargo.toml

@@ -6,16 +6,18 @@ edition = "2021"
 [dependencies]
 number = { path = "../number" }
 pil_analyzer = { path = "../pil_analyzer" }
-executor = { path = "../executor" }
-pilgen = { path = "../pilgen" }
 polyexen = { git = "https://github.com/Dhole/polyexen", rev="c4864d2debf9ae21138c9d67a99c93c3362df19b"}
 halo2_proofs = "0.2"
-prettytable = "0.10.0"
 num-traits = "0.2.15"
 num-integer = "0.1.45"
 itertools = "0.10.5"
 num-bigint = "^0.4"
 log = "0.4.17"
+rand = "0.8.5"
+
+[dev-dependencies]
+executor = { path = "../executor" }
+pilgen = { path = "../pilgen" }
 
 [build-dependencies]
 lalrpop = "^0.19"

halo2/src/circuit_builder.rs

@@ -11,34 +11,33 @@ use super::circuit_data::CircuitData;
 
 pub(crate) fn analyzed_to_circuit<T: FieldElement>(
     analyzed: &pil_analyzer::Analyzed<T>,
-    query_callback: Option<impl FnMut(&str) -> Option<T>>,
+    fixed: Vec<(&str, Vec<T>)>,
+    witness: Vec<(&str, Vec<T>)>,
 ) -> PlafH2Circuit {
     // The structure of the table is as following
     //
     // | constant columns | __enable_cur | __enable_next |  witness columns | \
-    // |  bla_bla_bla     |    1         |       1       |   bla_bla_bla    |  |
-    // |  bla_bla_bla     |    1         |       1       |   bla_bla_bla    |  |>  witness + fixed  2^(k-1)
+    // |  c[0]            |    1         |       1       |   w[0]           |  |
+    // |  c[1]            |    1         |       1       |   w[1]           |  |>  N actual circuit rows
     // |  ...             |   ...        |      ...      |   ...            |  |
-    // |  bla_bla_bla     |    1         |       0       |   bla_bla_bla    | /     <- __enable_next == 0 since there's no state transition
+    // |  c[N - 2]        |    1         |       1       |   w[N - 2]       |  |
+    // |  c[N - 1]        |    1         |       0       |   w[N - 1]       | /     <- __enable_next == 0 since there's no state transition
     // |  0               |    0         |       0       |   0              | \
     // |  0               |    0         |       0       |   0              |  |
-    // |  ...             |   ...        |      ...      |   ...            |  |> 2^2-1
+    // |  ...             |   ...        |      ...      |   ...            |  |>  (2**(ceil(log2(N)) + 1) - N) padding rows to fit the halo2 unusable rows
+    // |  0               |    0         |       0       |   0              |  |
     // |  0               |    0         |       0       |   <unusable>     |  |
     // |  0               |    0         |       0       |   <unusable>     | /
 
     // generate fixed and witness (witness).
 
     let query = |column, rotation| Expr::Var(PlonkVar::ColumnQuery { column, rotation });
 
-    let (fixed, degree) = executor::constant_evaluator::generate(analyzed);
-    let witness = executor::witgen::generate(analyzed, degree, &fixed, query_callback);
-
     let mut cd = CircuitData::from(fixed, witness);
 
-    // append to fixed columns:
-    // - one that enables constraints that do not have rotations
-    // - and another that enables constraints that have a rotation
-    // (note this is not activated) in last row.
+    // append two fixed columns:
+    // - one that enables constraints that do not have rotations (__enable_cur) in the actual circuit
+    // - and another that enables constraints that have a rotation (__enable_next) in the actual circuit except in the last actual row
 
     let num_rows = cd.len();
 
@@ -92,14 +91,17 @@ pub(crate) fn analyzed_to_circuit<T: FieldElement>(
             assert_eq!(id.right.selector, None);
             assert_eq!(id.left.expressions.len(), 0);
 
-            let (exp, is_next) = expression_2_expr(&cd, id.left.selector.as_ref().unwrap());
+            let exp = id.left.selector.as_ref().unwrap();
+            let contains_next_ref = exp.contains_next_ref();
+
+            let exp = expression_2_expr(&cd, exp);
 
             // depending whether this polynomial contains a rotation,
             // enable for all rows or all except the last one.
 
             let exp = Expr::Mul(vec![
                 exp,
-                if is_next {
+                if contains_next_ref {
                     q_enable_next.clone()
                 } else {
                     q_enable_cur.clone()
@@ -119,21 +121,21 @@ pub(crate) fn analyzed_to_circuit<T: FieldElement>(
                 .selector
                 .clone()
                 .map_or(Expr::Const(BigUint::one()), |expr| {
-                    expression_2_expr(&cd, &expr).0
+                    expression_2_expr(&cd, &expr)
                 });
 
             let left = id
                 .left
                 .expressions
                 .iter()
-                .map(|expr| left_selector.clone() * expression_2_expr(&cd, expr).0)
+                .map(|expr| left_selector.clone() * expression_2_expr(&cd, expr))
                 .collect();
 
             let right = id
                 .right
                 .expressions
                 .iter()
-                .map(|expr| expression_2_expr(&cd, expr).0)
+                .map(|expr| expression_2_expr(&cd, expr))
                 .collect();
 
             lookups.push(Lookup {
@@ -201,12 +203,9 @@ pub(crate) fn analyzed_to_circuit<T: FieldElement>(
     PlafH2Circuit { plaf, wit }
 }
 
-fn expression_2_expr<T: FieldElement>(
-    cd: &CircuitData<T>,
-    expr: &Expression<T>,
-) -> (Expr<PlonkVar>, bool) {
+fn expression_2_expr<T: FieldElement>(cd: &CircuitData<T>, expr: &Expression<T>) -> Expr<PlonkVar> {
     match expr {
-        Expression::Number(n) => (Expr::Const(n.to_arbitrary_integer()), false),
+        Expression::Number(n) => Expr::Const(n.to_arbitrary_integer()),
         Expression::PolynomialReference(polyref) => {
             assert_eq!(polyref.index, None);
 
@@ -215,18 +214,17 @@ fn expression_2_expr<T: FieldElement>(
                 rotation: polyref.next as i32,
             };
 
-            (Expr::Var(plonkvar), polyref.next)
+            Expr::Var(plonkvar)
         }
         Expression::BinaryOperation(lhe, op, rhe) => {
-            let (lhe, lhe_rot) = expression_2_expr(cd, lhe);
-            let (rhe, rhe_rot) = expression_2_expr(cd, rhe);
-            let res = match op {
+            let lhe = expression_2_expr(cd, lhe);
+            let rhe = expression_2_expr(cd, rhe);
+            match op {
                 BinaryOperator::Add => Expr::Sum(vec![lhe, rhe]),
                 BinaryOperator::Sub => Expr::Sum(vec![lhe, Expr::Neg(Box::new(rhe))]),
                 BinaryOperator::Mul => Expr::Mul(vec![lhe, rhe]),
                 _ => unimplemented!("{:?}", expr),
-            };
-            (res, std::cmp::max(lhe_rot, rhe_rot))
+            }
         }
 
         _ => unimplemented!("{:?}", expr),

halo2/src/lib.rs

@@ -2,4 +2,4 @@ pub(crate) mod circuit_builder;
 pub(crate) mod circuit_data;
 pub(crate) mod mock_prover;
 
-pub use mock_prover::mock_prove_asm;
+pub use mock_prover::mock_prove;