diff --git a/format.md b/format.md index fe6db5a..9b7253d 100644 --- a/format.md +++ b/format.md @@ -1,5 +1,7 @@ # plaf: Plonkish Arithmetization Format +Original notes for Plaf. The current implementation is slightly different. + ``` [info] name = "Circuit Foo" diff --git a/plaf.md b/plaf.md new file mode 100644 index 0000000..0d03ee6 --- /dev/null +++ b/plaf.md @@ -0,0 +1,38 @@ +# plaf: Plonkish Arithmetization Format + +**Disclaimer**: This is a work in process and some parts of the implementation may be incomplete. + +Plaf is an attempt to create a standard format for plonkish circuits so that it can be reused in components that work with plonkish arithmetization. + +Plaf supports the following "plonkish arithmetization" features: +- Listing of columns (or commitment polynomials) with names (aliases) +- Listing of polynomail expressions constraints that use the columns at any level of rotation +- Listing of lookup constraints as list of expression pairs +- Listing of copy constraints as list of column pairs with list of offset pairs +- Partial support for the Challange API: https://github.com/privacy-scaling-explorations/halo2/pull/97 +- Fixed column values + +## Serialization & Deserialization + +Plaf is currently implemented as a Rust struct but it can also be serialized. + +The current implementation supports the serialization of a Plaf circuit into 2 parts: +- A csv file with the fixed column values +- The rest of the circuit definition in a toml file + +Currently the deserialization is not implemented + +## Motivation and goals + +The first motivation is to have a standard format that can be reused among various plonkish systems so that frontends and backend become independent and can be made interchangeable. The definition of frontend and backend used here is this: +- frontend: module that generates the plonkish circuit (encoded as a Plaf circuit), and also is able to generate the witness values +- backend: module that has the following functionalities: + - receive a Plaf circuit and generate the corresponding verifying and proving keys. + - receive a Plaf circuit, a proving key and the witness values and generate a proof. + - receive a Plaf circuit, a verifying key and a proof and verify it. + +The current implemnentation supports the halo2 frontend (the halo2 Rust API) and the halo2 backend (the halo2 provig system implementation). Using halo2 as backend requires a small change in halo2 because the original version only supports circuits defined at compile time. The approach I've followed to support runtime circuit definitions is to add `&self` to `Circuit::configure`: https://github.com/ed255/halo2/commit/63e969673de83a410f21553fabec8f4b35bda1a5 + +A second goal is to have a standard format that supports pretty serialization to help reviewing/auditing circuits. + +A third goal is to have a standard format which circuit analysis tools can target so that they can be reused for circuits targeting different proving systems. diff --git a/src/expr.rs b/src/expr.rs index 1ebbc2c..40a4aa8 100644 --- a/src/expr.rs +++ b/src/expr.rs @@ -6,6 +6,7 @@ use num_bigint::{BigInt, BigUint, RandBigInt, Sign}; use num_integer::Integer; use num_traits::{One, ToPrimitive, Zero}; use rand::Rng; +use std::mem; use std::{ cmp::{Eq, Ord, Ordering, PartialEq}, collections::{HashMap, HashSet}, @@ -598,8 +599,7 @@ impl Expr { _ => self, } } - - pub fn simplify(self, p: &BigUint) -> Self { + pub fn simplify_move(self, p: &BigUint) -> Self { let ip = BigInt::from(p.clone()); let e = self._simplify(p, &ip); let e = e.normalize_linear_comb(); @@ -607,6 +607,13 @@ impl Expr { e } + pub fn simplify(&mut self, p: &BigUint) -> &mut Self { + let e = mem::replace(self, Expr::Const(BigUint::zero())); + let e = e.simplify_move(p); + *self = e; + self + } + fn _normalize(self, p: &BigUint) -> Self { use Expr::*; // p-1 == -1 @@ -614,11 +621,11 @@ impl Expr { match self { Neg(e) => Mul(vec![Const(p_1), *e]), Sum(xs) => { - let xs: Vec> = xs.into_iter().map(|x| x.normalize(p)).collect(); + let xs: Vec> = xs.into_iter().map(|x| x.normalize_move(p)).collect(); Sum(xs) } Mul(xs) => { - let mut xs: Vec> = xs.into_iter().map(|x| x.normalize(p)).collect(); + let mut xs: Vec> = xs.into_iter().map(|x| x.normalize_move(p)).collect(); xs.sort(); let mut iter = xs.into_iter(); let mul_acc = iter.next().unwrap(); @@ -645,8 +652,15 @@ impl Expr { } } - pub fn normalize(self, p: &BigUint) -> Self { - self.simplify(p)._normalize(p).simplify(p) + pub fn normalize_move(self, p: &BigUint) -> Self { + self.simplify_move(p)._normalize(p).simplify_move(p) + } + + pub fn normalize(&mut self, p: &BigUint) -> &mut Self { + let e = mem::replace(self, Expr::Const(BigUint::zero())); + let e = e.normalize_move(p); + *self = e; + self } fn _vars(&self, vars: &mut HashSet) { @@ -669,6 +683,7 @@ impl Expr { vars } + // TODO: Document the probability of success pub fn test_eq(&self, rng: &mut R, other: &Self) -> bool { let p = BigUint::parse_bytes(b"100000000000000000000000000000000", 16).unwrap() - BigUint::from(159u64); @@ -684,6 +699,13 @@ impl Expr { let e2_eval = other.eval(&p, &vars); e1_eval == e2_eval } + + pub fn is_zero(&self) -> bool { + match self { + Self::Const(c) => c.is_zero(), + _ => false, + } + } } pub struct ExprDisplay<'a, V: Var, T> @@ -814,14 +836,14 @@ mod tests { println!("raw e: {:?}", e); println!("e: {}", e); - let e = e.clone().normalize(&p); + let e = e.clone().normalize_move(&p); println!("e.normalize: {}", e); - let e = e.simplify(&p); + let e = e.simplify_move(&p); println!("raw e.normalize: {:?}", e); println!("e.simplify: {}", e); - let e = e.normalize(&p); + let e = e.normalize_move(&p); println!("e.normalize: {}", e); } @@ -863,7 +885,7 @@ mod tests { let mut rng = ChaCha20Rng::seed_from_u64(0); for i in 0..1024 { let e1 = Expr::rand(&mut rng, &p); - let e2 = e1.clone().simplify(&p); + let e2 = e1.clone().simplify_move(&p); let eval1 = e1.eval(&p, &vars); let eval2 = e2.eval(&p, &vars); if eval1 != eval2 { @@ -888,7 +910,7 @@ mod tests { let mut rng = ChaCha20Rng::seed_from_u64(0); for _i in 0..1024 { let e1 = Expr::rand_depth(&mut rng, &p, 3); - let e2 = e1.clone().normalize(&p); + let e2 = e1.clone().normalize_move(&p); let eval1 = e1.eval(&p, &vars); let eval2 = e2.eval(&p, &vars); assert_eq!(eval1, eval2); @@ -933,7 +955,7 @@ mod tests_with_parser { let e1_str = "112 + r_word*(164 + r_word*(133 + r_word*(93 + r_word*(4 + r_word*(216 + r_word*(250 + r_word*(123 + r_word*(59 + r_word*(39 + r_word*(130 + r_word*(202 + r_word*(83 + r_word*(182 + r_word*r_word*(229 + r_word*(192 + r_word*(3 + r_word*(199 + r_word*(220 + r_word*(178 + r_word*(125 + r_word*(126 + r_word*(146 + r_word*(60 + r_word*(35 + r_word*(247 + r_word*(134 + r_word*(1 + r_word*(70 + r_word*(210 + 197*r_word)))))))))))))))))))))))))))))"; let e2_str = "112*r_word^0 + 164*r_word^1 + 133*r_word^2 + 93*r_word^3 + 4*r_word^4 + 216*r_word^5 + 250*r_word^6 + 123*r_word^7 + 59*r_word^8 + 39*r_word^9 + 130*r_word^10 + 202*r_word^11 + 83*r_word^12 + 182*r_word^13 + 0*r_word^14 + 229*r_word^15 + 192*r_word^16 + 3*r_word^17 + 199*r_word^18 + 220*r_word^19 + 178*r_word^20 + 125*r_word^21 + 126*r_word^22 + 146*r_word^23 + 60*r_word^24 + 35*r_word^25 + 247*r_word^26 + 134*r_word^27 + 1*r_word^28 + 70*r_word^29 + 210*r_word^30 + 197*r_word^31"; let e1 = parse_expr(e1_str).unwrap(); - let e2 = e1.simplify(&p); + let e2 = e1.simplify_move(&p); // println!("{:?}", e1.normalize_linear_comb()); let s2 = format!("{}", e2); assert_eq!(s2, e2_str); @@ -944,7 +966,7 @@ mod tests_with_parser { let p = prime(); let e1_str = "1*BYTECODE_q_enable*(1 - 1*(1 - 1*(1 - tag)*(1 - tag[1]))*(1 - BYTECODE_q_last))*(code_hash - (((((((((((((((((((((((((((((((197*r_word + 210)*r_word + 70)*r_word + 1)*r_word + 134)*r_word + 247)*r_word + 35)*r_word + 60)*r_word + 146)*r_word + 126)*r_word + 125)*r_word + 178)*r_word + 220)*r_word + 199)*r_word + 3)*r_word + 192)*r_word + 229)*r_word + 0)*r_word + 182)*r_word + 83)*r_word + 202)*r_word + 130)*r_word + 39)*r_word + 59)*r_word + 123)*r_word + 250)*r_word + 216)*r_word + 4)*r_word + 93)*r_word + 133)*r_word + 164)*r_word + 112))"; let e1 = parse_expr(e1_str).unwrap(); - let e2 = e1.clone().simplify(&p); + let e2 = e1.clone().simplify_move(&p); println!("{}", e2); let vars: HashMap = { @@ -969,7 +991,7 @@ mod tests_with_parser { // TODO: Debug parser with this // let e1_str ="f05*w77*w78*w79*w80*(1 - w76)*(w26 - (w26[-1]*2^0 + w25[-1]*2^1 + w24[-1]*2^2 + w23[-1]*2^3) + 2*(w25*2^0 + w24*2^1 + w23*2^2) + r_word*(w28 - w28[-1]) + r_word*r_word*(w27 - w27[-1]) + r_word*r_word*r_word*(w38 - w38[-1]) + r_word*r_word*r_word*r_word*(w37 - w37[-1]) + r_word*r_word*r_word*r_word*r_word*(w36 - w36[-1]) + r_word*r_word*r_word*r_word*r_word*r_word*(w35 - w35[-1]) + r_word*r_word*r_word*r_word*r_word*r_word*r_word*(w34 - w34[-1]) + r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*(w33 - w33[-1]) + r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*(w32 - w32[-1]) + r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*(w31 - w31[-1]) + r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*(w30 - w30[-1]) + r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*(w29 - w29[-1]) + r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*(w05 - w05[-1]) + r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*r_word*(w69 - (w69[-1] + 2^8*w70[-1]) + 2^8*w70))"; let e1 = parse_expr(e1_str).unwrap(); - let e2 = e1.simplify(&p); + let e2 = e1.simplify_move(&p); // println!("{:?}", e1.normalize_linear_comb()); let s2 = format!("{}", e2); assert_eq!(s2, e2_str); diff --git a/src/plaf.rs b/src/plaf.rs index e770910..d45246c 100644 --- a/src/plaf.rs +++ b/src/plaf.rs @@ -131,43 +131,62 @@ impl Challenge { #[derive(Debug, Default, Clone)] pub struct Columns { + /// List of witness columns. These are called "advice" in halo2. pub witness: Vec, + /// List of fixed columns. pub fixed: Vec, + /// List of public columns. These are called "instance" in halo2. pub public: Vec, } +/// Polynomial constraint #[derive(Debug, Clone)] pub struct Poly { pub name: String, pub exp: Expr, } +/// Lookup constraint #[derive(Debug, Clone)] pub struct Lookup { pub name: String, pub exps: (Vec>, Vec>), } +/// Copy Constraint #[derive(Debug, Clone)] pub struct CopyC { pub columns: (expr::Column, expr::Column), pub offsets: Vec<(usize, usize)>, } +/// Circuit general information #[derive(Debug, Default, Clone)] pub struct Info { + /// Field modulus + pub p: BigUint, + /// Number of rows. This is always a power of 2 in halo2. pub num_rows: usize, + /// List of challenges used. The challange API is a proving system extension applied to pse's + /// fork of halo2: https://github.com/privacy-scaling-explorations/halo2/pull/97 pub challenges: Vec, } /// Plonkish Arithmetization Format #[derive(Debug, Default, Clone)] pub struct Plaf { + /// Circuit general information pub info: Info, + /// Column information pub columns: Columns, + /// List of polynomial identity constraints pub polys: Vec, + /// List of lookup constraints pub lookups: Vec, + /// List of copy constraints pub copys: Vec, + /// Assignment values to the fixed columns. None is used for non-assigned values, which means + /// a 0 value. pub fixed: Vec>>, } @@ -288,6 +307,22 @@ impl Plaf { Pow(e, f) => Pow(Box::new(self.resolve(e, offset)), *f), } } + + /// Simplify expressions in polynomial constraints and lookups. + pub fn simplify(&mut self) { + let p = &self.info.p; + // Polynomial Expressions + for poly in self.polys.iter_mut() { + poly.exp.simplify(p); + } + // Lookups + for lookup in self.lookups.iter_mut() { + for (lhs, rhs) in lookup.exps.0.iter_mut().zip(lookup.exps.1.iter_mut()) { + lhs.simplify(p); + rhs.simplify(p); + } + } + } } /// Adaptor struct to format the fixed columns assignments as CSV diff --git a/src/plaf/frontends/halo2.rs b/src/plaf/frontends/halo2.rs index 8eb5295..1b2b37d 100644 --- a/src/plaf/frontends/halo2.rs +++ b/src/plaf/frontends/halo2.rs @@ -446,6 +446,7 @@ pub fn get_plaf, ConcreteCircuit: Circuit })); let mut plaf = Plaf::default(); let p = get_field_p::(); + plaf.info.p = p; plaf.info.num_rows = 2usize.pow(k); let challenge_phase = cs.challenge_phase(); @@ -490,8 +491,7 @@ pub fn get_plaf, ConcreteCircuit: Circuit let len_log10 = (gate.polynomials().len() as f64).log10().ceil() as usize; for (i, poly) in gate.polynomials().iter().enumerate() { let exp = Expr::::from(poly); - // FIXME: There's a bug in simplify, tested with bytecode circuit - let exp = exp.simplify(&p); + // let exp = exp.simplify(&p); if matches!(exp, Expr::Const(_)) { // Skip constant expressions (which should be `p(x) = 0`) continue; @@ -506,14 +506,8 @@ pub fn get_plaf, ConcreteCircuit: Circuit let name = lookup.name(); let lhs = lookup.input_expressions(); let rhs = lookup.table_expressions(); - let lhs = lhs - .iter() - .map(|e| Expr::::from(e).simplify(&p)) - .collect(); - let rhs = rhs - .iter() - .map(|e| Expr::::from(e).simplify(&p)) - .collect(); + let lhs = lhs.iter().map(|e| Expr::::from(e)).collect(); + let rhs = rhs.iter().map(|e| Expr::::from(e)).collect(); plaf.lookups.push(Lookup { name: name.to_string(), exps: (lhs, rhs),