unify way to convert between FieldElement & PrimeField

nova/Cargo.toml

@@ -17,6 +17,7 @@ ast = { version = "0.1.0", path = "../ast" }
 nova-snark = { git = "https://github.com/hero78119/SuperNova.git", branch = "supernova_trait_mut", default-features = false, features = ["supernova"] }
 bellperson = { version = "0.25", default-features = false}
 ff = { version = "0.13.0", features = ["derive"] }
+polyexen = { git = "https://github.com/Dhole/polyexen", branch = "feature/shuffles" }
 
 [dev-dependencies]
 analysis = { path = "../analysis" }

nova/src/circuit_builder.rs

@@ -23,14 +23,14 @@ use bellperson::{
 use ff::{Field, PrimeField};
 use itertools::Itertools;
 use log::warn;
-use nova_snark::provider::bn256_grumpkin;
 use nova_snark::{
     compute_digest,
     supernova::{gen_commitmentkey_by_r1cs, PublicParams, RecursiveSNARK, RunningClaim},
     traits::{circuit_supernova::StepCircuit, Group},
 };
+use nova_snark::{provider::bn256_grumpkin, traits::PrimeFieldExt};
 use num_bigint::BigUint;
-use number::FieldElement;
+use number::{BigInt, FieldElement};
 
 use crate::{
     nonnative::{
@@ -46,7 +46,7 @@ use crate::{
 /// LIMB WITHD as base, represent 2^16
 const LIMB_WIDTH: usize = 16;
 
-fn get_num_at_index<F: PrimeField, CS: ConstraintSystem<F>>(
+fn get_num_at_index<F: PrimeFieldExt, CS: ConstraintSystem<F>>(
     mut cs: CS,
     index_before_offset: &AllocatedNum<F>,
     z: &[AllocatedNum<F>],
@@ -99,6 +99,11 @@ pub(crate) fn nova_prove<T: FieldElement>(
     _: Vec<(&str, Vec<T>)>,
     witness: Vec<(&str, Vec<T>)>,
 ) -> () {
+    if polyexen::expr::get_field_p::<<G1 as Group>::Scalar>() != T::modulus().to_arbitrary_integer()
+    {
+        panic!("powdr modulus doesn't match nova modulus. Make sure you are using Bn254");
+    }
+
     // TODO to avoid clone witness object, witness are wrapped by lock so it can be shared below
     // need to refactor this part to support parallel folding
     // redesign this part if possible
@@ -182,10 +187,9 @@ pub(crate) fn nova_prove<T: FieldElement>(
                             let value = <G1 as Group>::Scalar::from_bytes(&n.to_bytes_le().try_into().unwrap()).unwrap();
                             match ope {
                                 UnaryOperator::Plus => value,
-                                UnaryOperator::Minus => value.invert().unwrap(),
+                                UnaryOperator::Minus => unimplemented!("not support signed constant"),
                             }
                         },
-                        // TODO support Unary to handle signed
                         x => unimplemented!("unsupported expression {}", x),
                     }),
                     _ => unimplemented!(),
@@ -396,7 +400,7 @@ pub(crate) fn nova_prove<T: FieldElement>(
 
 // TODO optmize constraints to leverage R1CS cost-free additive
 // TODO combine FieldElement & PrimeField
-fn evaluate_expr<'a, T: FieldElement, F: PrimeField, CS: ConstraintSystem<F>>(
+fn evaluate_expr<'a, T: FieldElement, F: PrimeFieldExt, CS: ConstraintSystem<F>>(
     mut cs: CS,
     poly_map: &mut BTreeMap<String, AllocatedNum<F>>,
     expr: &Expression<T>,
@@ -405,10 +409,9 @@ fn evaluate_expr<'a, T: FieldElement, F: PrimeField, CS: ConstraintSystem<F>>(
     match expr {
         Expression::Number(n) => {
             AllocatedNum::alloc(cs.namespace(|| format!("{:x?}", n.to_string())), || {
-                // TODO support number > u64
-                Ok(F::from(u64::from_le_bytes(
-                    n.to_bytes_le()[0..8].try_into().unwrap(),
-                )))
+                let mut n_le = n.to_bytes_le();
+                n_le.resize(64, 0);
+                Ok(F::from_uniform(&n_le[..]))
             })
         }
         // this is refer to another polynomial, in other word, witness
@@ -423,10 +426,10 @@ fn evaluate_expr<'a, T: FieldElement, F: PrimeField, CS: ConstraintSystem<F>>(
                 .entry(name.to_string())
                 .or_insert_with(|| {
                     AllocatedNum::alloc(cs.namespace(|| format!("{}.{}", expr, name)), || {
-                        // TODO need to know how to convert T to F is T is inv
-                        // TODO unify FieldElement and PrimeField to avoid this conversion
                         let wit_value = witgen.lock().unwrap().get_wit_by_key(name).cloned();
-                        let f = F::from_str_vartime(&wit_value.unwrap().to_string()[..]).unwrap();
+                        let mut n_le = wit_value.unwrap().to_bytes_le();
+                        n_le.resize(64, 0);
+                        let f = F::from_uniform(&n_le[..]);
                         Ok(f)
                     })
                     .unwrap()
@@ -531,7 +534,7 @@ where
 
 impl<'a, F, T> StepCircuit<F> for NovaStepCircuit<'a, F, T>
 where
-    F: PrimeField,
+    F: PrimeFieldExt,
     T: FieldElement,
 {
     fn arity(&self) -> usize {
@@ -554,9 +557,9 @@ where
         // TODO Fixme: constant can not be witness!!
         self.analyzed.constants.iter().try_for_each(|(k, v)| {
             let a = AllocatedNum::alloc(cs.namespace(|| format!("{:x?}", v.to_string())), || {
-                Ok(F::from(u64::from_le_bytes(
-                    v.to_bytes_le()[0..8].try_into().unwrap(),
-                )))
+                let mut v_le = v.to_bytes_le();
+                v_le.resize(64, 0);
+                Ok(F::from_uniform(&v_le[..]))
             })?;
             poly_map.insert(k.clone(), a);
             Ok::<(), SynthesisError>(())

nova/zero.asm

@@ -26,7 +26,6 @@ machine NovaZero {
     }
 
     instr incr X -> Y {
-        // range check on X
         Y = X + 1,
         Y = x_b0 + x_b1 * 2 + x_b2 * 2**2 + x_b3 * 2**3,
         pc' = pc + 1
@@ -37,6 +36,11 @@ machine NovaZero {
         pc' = pc + 1
     }
 
+    instr sub X, Y -> Z {
+        Z = X - Y,
+        pc' = pc + 1
+    }
+
     instr decr X -> Y {
         Y = X - 1
     }
@@ -66,9 +70,9 @@ machine NovaZero {
         x1 <=Y= incr(x0); // x1 = 1
         x0 <=Z= add(x1, x1); // x0 = 1 + 1
         x0 <=Z= addi(x0, 1); // x0 = 2 + 1
+        // x0 <=Z= addi(x0, -1); // TODO need support signed constant in instruction assignment
         x0 <=Y= decr(x0); // x0 = 2
-        x0 <=Y= decr(x0); // x0 = 1
-        x0 <=Y= decr(x0); // x0 = 0
+        x0 <=Z= sub(x0, x0); // x0 - x0 = 0
         assert_zero x0; // x0 == 0
         loop;
     }