From 2ace790e52fdbc71ce094e5c8957df7cb04606ae Mon Sep 17 00:00:00 2001 From: "sm.wu" Date: Wed, 9 Aug 2023 23:48:53 +0800 Subject: [PATCH] nova support signed constant ROM encoding --- nova/README.md | 17 ++++++-- nova/src/circuit.rs | 40 ++++++++++++++++--- nova/src/circuit_builder.rs | 37 +++++++++++++++-- nova/src/utils.rs | 80 +++++++++++++++++++++++++++++++++---- nova/zero.asm | 3 +- 5 files changed, 155 insertions(+), 22 deletions(-) diff --git a/nova/README.md b/nova/README.md index f28c177969..c653ecaf35 100644 --- a/nova/README.md +++ b/nova/README.md @@ -14,18 +14,27 @@ Each instruction is compiled into a step circuit, following Nova(Supernova) pape An augmented circuit := step circuit + nova folding verification circuit. Furthermore, an augmented circuit has it own isolated constraints system, means there will be no shared circuit among different augmented circuits. Due to the fact, we can also call it instruction-circuit. There will be `#inst` instruction-circuit (More accurate, `#inst + 1` for 2 cycle curve implementation) -### Nova state & Constraints -public input layout as z0 = `(pc, [writable register...] + [rom_value_pc1, rom_value_pc2, rom_value_pc3...])` +### Nova state & constraints +Nova state layout as z0 = `(pc, [writable register...] ++ ROM)` +where the ROM is defined as an array `[rom_value_pc1, rom_value_pc2, rom_value_pc3...]` Each round an instruction is invoked, and in instruction-circuit it will constraints -1. sequence constraints => `zi[offset + pc] - linear-combination([opcode_index, input reg1, input reg2,...], 1 << limb_width) = 0` +1. sequence constraints => `zi[offset + pc] - linear-combination([opcode_index, input param1, input param2,...output param1, ...], 1 << limb_width) = 0` 2. writable register read/write are value are constraint and match. > While which instruction-circuit is invoked determined by prover, an maliculous prover can not invoke arbitrary any instruction-circuit, otherwise sequence constraints will be failed to pass `is_sat` check in the final stage. +### Sequence constraints +As mentioned, to constraints the sequence, a ROM array is introduced and attach at the end of Nova state. For input params in different type, the linear combination strategy will be adjust accordingly. + +- `reg index`, i.e. x2. `2` will be treat as unsigned index and put into the value +- `sign/unsigned` const. For unsigned value will be put in lc directly. While signed part, it will be convert to signed limb, and on circuit side, signed limb will be convert to negative field value accordingly. +- `label`. i.e. `loop_start`, label will be convert to integer + +Since each instruction circuit has it own params type definition, different constraints circuit will be compiled to handle above situation automatically. ### R1CS constraints An augmented circuit can be viewed as a individual constraint system. PIL in powdr-asm instruction definition body will be compile into respective R1CS constraints. More detail, constraints can be categorized into 2 group -1. sequence constraints + writable register RW => this constraints will be insert into R1CS circuit automatically and transparent to powdr-asm PIL. +1. sequence constraints + writable register RW (or signed/unsigned/label) => this constraints will be insert into R1CS circuit automatically and transparent to powdr-asm PIL. 2. Powdr-asm PIL constraints: will be compiled into R1CS constraints Giving simple example diff --git a/nova/src/circuit.rs b/nova/src/circuit.rs index 226dd2ffdd..e600592d13 100644 --- a/nova/src/circuit.rs +++ b/nova/src/circuit.rs @@ -1,5 +1,6 @@ use std::{ collections::BTreeMap, + iter, marker::PhantomData, sync::{Arc, Mutex}, }; @@ -22,7 +23,7 @@ use crate::{ nonnative::{bignat::BigNat, util::Num}, utils::{ add_allocated_num, alloc_const, alloc_num_equals, alloc_one, conditionally_select, - evaluate_expr, find_pc_expression, get_num_at_index, WitnessGen, + evaluate_expr, find_pc_expression, get_num_at_index, signed_limb_to_neg, WitnessGen, }, LIMB_WIDTH, }; @@ -104,6 +105,19 @@ where // add constant 1 poly_map.insert("ONE".to_string(), alloc_one(cs.namespace(|| "constant 1"))?); + // add constant 2^(LIMB_WIDTH + 1) + let mut max_limb_plus_one = vec![0u8; 64]; + max_limb_plus_one[LIMB_WIDTH / 8] = 1u8; + let max_limb_plus_one = F::from_uniform(&max_limb_plus_one[..]); + poly_map.insert( + "1 <<(LIMB_WIDTH + 1)".to_string(), + alloc_const( + cs.namespace(|| "constant 1 <<(LIMB_WIDTH + 1)"), + max_limb_plus_one, + LIMB_WIDTH + 1, + )?, + ); + // parse inst part to construct step circuit // decompose ROM[pc] into linear combination lc(opcode_index, operand_index1, operand_index2, ... operand_output) // Noted that here only support single output @@ -131,11 +145,27 @@ where let input_output_params_allocnum = rom_value_bignat .as_limbs() .iter() + .zip_eq( + iter::once::>(None) + .chain(input_params.iter().map(|param| Some(param))) + .chain(output_params.iter().map(|param| Some(param))), + ) .enumerate() - .map(|(limb_index, limb)| { - limb.as_allocated_num( - cs.namespace(|| format!("rom decompose index {}", limb_index)), - ) + .map(|(limb_index, (limb, param))| { + match param { + // signed handling + Some(Param { + ty: Some(type_str), .. + }) if type_str == "signed" => signed_limb_to_neg( + cs.namespace(|| format!("limb index {}", limb_index)), + limb, + &poly_map["1 <<(LIMB_WIDTH + 1)"], + LIMB_WIDTH, + ), + _ => limb.as_allocated_num( + cs.namespace(|| format!("rom decompose index {}", limb_index)), + ), + } }) .collect::>, SynthesisError>>()?; diff --git a/nova/src/circuit_builder.rs b/nova/src/circuit_builder.rs index 4b9880ae3b..fe7a08de20 100644 --- a/nova/src/circuit_builder.rs +++ b/nova/src/circuit_builder.rs @@ -14,8 +14,8 @@ use ast::{ UnaryOperator, }, }; -use ff::{Field, PrimeField}; -use nova_snark::provider::bn256_grumpkin; +use ff::PrimeField; +use nova_snark::provider::bn256_grumpkin::{self}; use nova_snark::{ compute_digest, supernova::{gen_commitmentkey_by_r1cs, PublicParams, RecursiveSNARK, RunningClaim}, @@ -129,7 +129,7 @@ pub(crate) fn nova_prove( let value = ::Scalar::from_bytes(&n.to_bytes_le().try_into().unwrap()).unwrap(); match ope { UnaryOperator::Plus => value, - UnaryOperator::Minus => unimplemented!("not support signed constant"), + UnaryOperator::Minus => get_neg_value_within_limbsize(value, LIMB_WIDTH), } }, x => unimplemented!("unsupported expression {}", x), @@ -161,7 +161,7 @@ pub(crate) fn nova_prove( let value = ::Scalar::from_bytes(&n.to_bytes_le().try_into().unwrap()).unwrap(); match ope { UnaryOperator::Plus => value, - UnaryOperator::Minus => value.invert().unwrap(), + UnaryOperator::Minus => get_neg_value_within_limbsize(value, LIMB_WIDTH), } }, x => unimplemented!("unsupported expression {:?}", x), @@ -339,3 +339,32 @@ pub(crate) fn nova_prove( // println!("zi_secondary: {:?}", zi_secondary); // println!("final program_counter: {:?}", program_counter); } + +/// get additive negative of value within limbsize +fn get_neg_value_within_limbsize( + value: ::Scalar, + nbit: usize, +) -> ::Scalar { + let value = value.to_bytes(); + let (lsb, msb) = value.split_at(nbit / 8); + assert_eq!( + msb.iter().map(|v| *v as usize).sum::(), + 0, + "value {:?} is overflow", + value + ); + let mut lsb = lsb.to_vec(); + lsb.resize(32, 0); + let value = ::Scalar::from_bytes(lsb[..].try_into().unwrap()).unwrap(); + + let mut max_limb_plus_one_bytes = vec![0u8; nbit / 8 + 1]; + max_limb_plus_one_bytes[nbit / 8] = 1u8; + max_limb_plus_one_bytes.resize(32, 0); + let max_limb_plus_one = + ::Scalar::from_bytes(max_limb_plus_one_bytes[..].try_into().unwrap()).unwrap(); + + let mut value_neg = (max_limb_plus_one - value).to_bytes()[0..nbit / 8].to_vec(); + value_neg.resize(32, 0); + + ::Scalar::from_bytes(&value_neg[..].try_into().unwrap()).unwrap() +} diff --git a/nova/src/utils.rs b/nova/src/utils.rs index 345628fcf2..c25fa045ec 100644 --- a/nova/src/utils.rs +++ b/nova/src/utils.rs @@ -5,6 +5,8 @@ use std::{ sync::{Arc, Mutex}, }; +use crate::nonnative::util::Num; + #[allow(dead_code)] use super::nonnative::bignat::{nat_to_limbs, BigNat}; use ast::{ @@ -98,7 +100,8 @@ pub fn alloc_const>( ) -> Result, SynthesisError> { let allocations: Vec = value.to_repr().as_bits::()[0..n_bits] .iter() - .map(|raw_bit| { + .enumerate() + .map(|(index, raw_bit)| { let bit = cs.alloc( || "boolean", || { @@ -111,14 +114,14 @@ pub fn alloc_const>( )?; if *raw_bit { cs.enforce( - || format!("bit{raw_bit} == 1"), + || format!("{:?} index {index} true", value), |lc| lc + bit, |lc| lc + CS::one(), |lc| lc + CS::one(), ); } else { cs.enforce( - || format!("bit{raw_bit} == 0"), + || format!("{:?} index {index} false", value), |lc| lc + bit, |lc| lc + CS::one(), |lc| lc, @@ -135,15 +138,18 @@ pub fn alloc_const>( f = f.double(); l }); - let value = AllocatedNum::alloc(cs.namespace(|| "alloc const"), || Ok(value))?; - let sum_lc = LinearCombination::zero() + value.get_variable() - ∑ + let value_alloc = + AllocatedNum::alloc(cs.namespace(|| format!("{:?} alloc const", value)), || { + Ok(value) + })?; + let sum_lc = LinearCombination::zero() + value_alloc.get_variable() - ∑ cs.enforce( - || "sum - value = 0", + || format!("{:?} sum - value = 0", value), |lc| lc + &sum_lc, |lc| lc + CS::one(), |lc| lc, ); - Ok(value) + Ok(value_alloc) } /// Allocate a scalar as a base. Only to be used is the scalar fits in base! @@ -640,6 +646,66 @@ pub fn get_num_at_index>( Ok(selected_num) } +/// get negative field value from signed limb +pub fn signed_limb_to_neg>( + mut cs: CS, + limb: &Num, + max_limb_plus_one_const: &AllocatedNum, + nbit: usize, +) -> Result, SynthesisError> { + let limb_alloc = limb.as_allocated_num(cs.namespace(|| "rom decompose index"))?; + let bits = limb.decompose(cs.namespace(|| "index decompose bits"), nbit)?; + let signed_bit = &bits.allocations[nbit - 1]; + let twos_complement = AllocatedNum::alloc(cs.namespace(|| "alloc twos complement"), || { + max_limb_plus_one_const + .get_value() + .zip(limb_alloc.get_value()) + .map(|(a, b)| a - b) + .ok_or(SynthesisError::AssignmentMissing) + })?; + cs.enforce( + || "constraints 2's complement", + |lc| lc + twos_complement.get_variable() + limb_alloc.get_variable(), + |lc| lc + CS::one(), + |lc| lc + max_limb_plus_one_const.get_variable(), + ); + let twos_complement_neg = AllocatedNum::alloc(cs.namespace(|| " 2's complment neg"), || { + twos_complement + .get_value() + .map(|v| v.neg()) + .ok_or(SynthesisError::AssignmentMissing) + })?; + cs.enforce( + || "constraints 2's complement additive neg", + |lc| lc + twos_complement.get_variable() + twos_complement_neg.get_variable(), + |lc| lc + CS::one(), + |lc| lc, + ); + + let c = AllocatedNum::alloc(cs.namespace(|| "conditional select"), || { + signed_bit + .value + .map(|signed_bit_value| { + if signed_bit_value { + twos_complement_neg.get_value().unwrap() + } else { + limb_alloc.get_value().unwrap() + } + }) + .ok_or(SynthesisError::AssignmentMissing) + })?; + + // twos_complement_neg * condition + limb_alloc*(1-condition) = c -> + // twos_complement_neg * condition - limb_alloc*condition = c - limb_alloc + cs.enforce( + || "index conditional select", + |lc| lc + twos_complement_neg.get_variable() - limb_alloc.get_variable(), + |_| signed_bit.bit.clone(), + |lc| lc + c.get_variable() - limb_alloc.get_variable(), + ); + Ok(c) +} + // TODO optmize constraints to leverage R1CS cost-free additive // TODO combine FieldElement & PrimeField pub fn evaluate_expr<'a, T: FieldElement, F: PrimeFieldExt, CS: ConstraintSystem>( diff --git a/nova/zero.asm b/nova/zero.asm index 6152c00507..5453b912e9 100644 --- a/nova/zero.asm +++ b/nova/zero.asm @@ -70,8 +70,7 @@ 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 <=Z= addi(x0, -2); // x0 = 3 - 2 x0 <=Z= sub(x0, x0); // x0 - x0 = 0 assert_zero x0; // x0 == 0 loop;