From dcf141712086d5bb1a997a1480113c17be9bac3f Mon Sep 17 00:00:00 2001 From: "sm.wu" Date: Wed, 2 Aug 2023 18:34:38 +0800 Subject: [PATCH] supernova finish constaints done, add workaround to collect meta info from asm source --- analysis/src/macro_expansion.rs | 2 +- asm_to_pil/src/lib.rs | 3 + ast/src/asm_analysis/mod.rs | 12 +- backend/src/lib.rs | 15 +- compiler/src/lib.rs | 3 +- number/src/traits.rs | 1 - powdr_cli/src/main.rs | 30 +- zero_nova/commits.bin | Bin 2496 -> 2208 bytes zero_nova/constants.bin | Bin 1248 -> 960 bytes zero_nova/src/circuit_builder.rs | 503 ++++++++++++++++++++++++------ zero_nova/src/nonnative/bignat.rs | 1 + zero_nova/src/prover.rs | 8 +- zero_nova/src/utils.rs | 2 +- zero_nova/zero.asm | 12 +- 14 files changed, 467 insertions(+), 125 deletions(-) diff --git a/analysis/src/macro_expansion.rs b/analysis/src/macro_expansion.rs index b3e7754770..a852157e3d 100644 --- a/analysis/src/macro_expansion.rs +++ b/analysis/src/macro_expansion.rs @@ -42,7 +42,7 @@ where .into_iter() .map(|mut m| { m.statements.iter_mut().for_each(|s| match s { - MachineStatement::InstructionDeclaration(_, _, _, body) => match body { + MachineStatement::InstructionDeclaration(_, _, params, body) => match body { InstructionBody::Local(body) => { body.iter_mut().for_each(|e| match e { InstructionBodyElement::PolynomialIdentity(left, right) => { diff --git a/asm_to_pil/src/lib.rs b/asm_to_pil/src/lib.rs index ed7e46efcd..07e9fe0a8e 100644 --- a/asm_to_pil/src/lib.rs +++ b/asm_to_pil/src/lib.rs @@ -130,6 +130,9 @@ impl ASMPILConverter { } if let Some(rom) = input.rom { + rom.statements + .iter() + .for_each(|v| println!("rom statement: {:?}", v)); let batches = rom.batches.unwrap_or_else(|| { vec![ BatchMetadata { diff --git a/ast/src/asm_analysis/mod.rs b/ast/src/asm_analysis/mod.rs index 446a799fae..674e80a5a0 100644 --- a/ast/src/asm_analysis/mod.rs +++ b/ast/src/asm_analysis/mod.rs @@ -42,7 +42,7 @@ pub struct DegreeStatement { pub degree: BigUint, } -#[derive(Clone)] +#[derive(Clone, Debug)] pub enum FunctionStatement { Assignment(AssignmentStatement), Instruction(InstructionStatement), @@ -74,7 +74,7 @@ impl From for FunctionStatement { } } -#[derive(Clone)] +#[derive(Clone, Debug)] pub struct AssignmentStatement { pub start: usize, pub lhs: Vec, @@ -82,20 +82,20 @@ pub struct AssignmentStatement { pub rhs: Box>, } -#[derive(Clone)] +#[derive(Clone, Debug)] pub struct InstructionStatement { pub start: usize, pub instruction: String, pub inputs: Vec>, } -#[derive(Clone)] +#[derive(Clone, Debug)] pub struct LabelStatement { pub start: usize, pub name: String, } -#[derive(Clone)] +#[derive(Clone, Debug)] pub struct DebugDirective { pub start: usize, pub directive: crate::parsed::asm::DebugDirective, @@ -130,7 +130,7 @@ impl Machine { } } -#[derive(Clone, Default)] +#[derive(Clone, Default, Debug)] pub struct Rom { pub statements: Vec>, pub batches: Option>, diff --git a/backend/src/lib.rs b/backend/src/lib.rs index 1d433b3159..ef27f7213f 100644 --- a/backend/src/lib.rs +++ b/backend/src/lib.rs @@ -1,4 +1,4 @@ -use ast::analyzed::Analyzed; +use ast::{analyzed::Analyzed, asm_analysis::Machine}; use number::FieldElement; use std::io; use strum::{Display, EnumString, EnumVariantNames}; @@ -107,13 +107,20 @@ impl ProverAggregationWithParams for Halo2AggregationBackend { } #[cfg(feature = "nova")] -impl ProverWithoutParams for NovaBackend { - fn prove( +// TODO implement ProverWithoutParams, and remove dependent on main_machine +impl NovaBackend { + pub fn prove( pil: &Analyzed, + main_machine: &Machine, fixed: Vec<(&str, Vec)>, witness: Vec<(&str, Vec)>, ) -> Option { - Some(nova::prove_ast_read_params(pil, fixed, witness)); + Some(nova::prove_ast_read_params( + pil, + main_machine, + fixed, + witness, + )); Some(vec![]) } } diff --git a/compiler/src/lib.rs b/compiler/src/lib.rs index 17fe2e6350..10807bd434 100644 --- a/compiler/src/lib.rs +++ b/compiler/src/lib.rs @@ -14,7 +14,8 @@ use json::JsonValue; pub mod util; mod verify; -use analysis::analyze; +// TODO should analyze be `pub`? +pub use analysis::analyze; pub use backend::{Backend, Proof}; use number::write_polys_file; use pil_analyzer::json_exporter; diff --git a/number/src/traits.rs b/number/src/traits.rs index 1c77dea1e6..00efcf3f02 100644 --- a/number/src/traits.rs +++ b/number/src/traits.rs @@ -1,6 +1,5 @@ use std::{fmt, hash::Hash, ops::*}; -use ark_ff::PrimeField; use num_traits::{One, Zero}; use crate::{AbstractNumberType, DegreeType}; diff --git a/powdr_cli/src/main.rs b/powdr_cli/src/main.rs index 9d894937a0..9356d83759 100644 --- a/powdr_cli/src/main.rs +++ b/powdr_cli/src/main.rs @@ -3,7 +3,7 @@ mod util; use clap::{Parser, Subcommand}; -use compiler::{compile_pil_or_asm, Backend}; +use compiler::{analyze, compile_pil_or_asm, Backend}; use env_logger::{Builder, Target}; use log::LevelFilter; use number::{Bn254Field, FieldElement, GoldilocksField}; @@ -188,6 +188,9 @@ enum Commands { /// Input PIL file file: String, + /// TODO retrive asm info from PIL + asm_file: String, + /// Directory to find the committed and fixed values #[arg(short, long)] #[arg(default_value_t = String::from("."))] @@ -372,10 +375,33 @@ fn run_command(command: Commands) { #[cfg(feature = "nova")] Commands::ProveNova { file, + asm_file, dir, params: _, } => { let pil = Path::new(&file); + let contents = fs::read_to_string(asm_file.clone()).unwrap(); + + let parsed = parser::parse_asm::(Some(&asm_file[..]), &contents[..]) + .unwrap_or_else(|err| { + eprintln!("Error parsing .asm file:"); + err.output_to_stderr(); + panic!(); + }); + let analysed_asm = analyze(parsed).unwrap(); + + // retrieve instance of the Main state machine + let main = match analysed_asm.machines.len() { + // if there is a single machine, treat it as main + 1 => analysed_asm.machines.values().next().unwrap().clone(), + // otherwise, find the machine called "Main" + _ => analysed_asm + .machines + .get("Main") + .expect("couldn't find a Main state machine") + .clone(), + }; + let dir = Path::new(&dir); let pil = compiler::analyze_pil::(pil); @@ -383,7 +409,7 @@ fn run_command(command: Commands) { let witness = compiler::util::read_witness(&pil, dir); // let params = fs::File::open(dir.join(params.unwrap())).unwrap(); - NovaBackend::prove(&pil, fixed.0, witness.0); + NovaBackend::prove(&pil, &main, fixed.0, witness.0); // TODO: this probably should be abstracted alway in a common backends API, // // maybe a function "get_file_extension()". diff --git a/zero_nova/commits.bin b/zero_nova/commits.bin index 339beba2eaec81613f15ca52227775078876853f..f88631ec664fe9187f570061d384a2218c56ada9 100644 GIT binary patch literal 2208 zcmeH_F%Cc>2t)PX|IkhyZ1T|5=_j~g3k6ddV?T3;N96U6y#eK&zr|kX^Mt96c*e-?cxKO?^vsz2Ec`HQ#>M{!ljcE!F*XzZVU^05<>t literal 2496 zcmeH^I}(6E2t)C6|1;Z|f;Tcq#>!b6%#x7Z5Hb6<8Qo^PKGYGvy%2T8oYVEiC$Gc% zEhJC#s#@`@^XVM&HCL5=;X^+k)y}W8p`N(YpB-V?pZaUOtCL=Jy+=trS2t%@$6KuZ aFp-SioLyaZk68O*A{o0mySnWDzx`ZthX6?c diff --git a/zero_nova/constants.bin b/zero_nova/constants.bin index 469111d4bc96ba7fe56293c1a3cd6f8d7e6e4662..60f355b029c9072dff5dbb2c0898d51df56db01c 100644 GIT binary patch literal 960 zcmZQ%Kn0AbTn0jXm~vd|VB#(ICOA%)aZQ1<{p}eY4#TD3;K6&6PPFfJOBUy diff --git a/zero_nova/src/circuit_builder.rs b/zero_nova/src/circuit_builder.rs index fed4f3a407..5b30c11df8 100644 --- a/zero_nova/src/circuit_builder.rs +++ b/zero_nova/src/circuit_builder.rs @@ -1,34 +1,39 @@ -use std::{collections::HashMap, marker::PhantomData}; +use core::panic; +use std::{collections::BTreeMap, iter, marker::PhantomData}; use ast::{ analyzed::{Analyzed, Expression, IdentityKind, PolynomialReference}, - parsed::BinaryOperator, + asm_analysis::{AssignmentStatement, FunctionStatement, Machine}, + parsed::{asm::FunctionCall, BinaryOperator}, }; use bellperson::{ gadgets::{boolean::Boolean, num::AllocatedNum}, ConstraintSystem, SynthesisError, }; use ff::PrimeField; +use itertools::Itertools; 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 num_bigint::BigUint; use number::FieldElement; use crate::utils::{ - add_allocated_num, alloc_num_equals, alloc_zero, conditionally_select, mul_allocated_num, + add_allocated_num, alloc_num_equals, alloc_one, alloc_zero, conditionally_select, + mul_allocated_num, }; -fn get_num_at_pcindex>( +fn get_num_at_index>( mut cs: CS, - pc_counter: &AllocatedNum, + index_before_offset: &AllocatedNum, z: &[AllocatedNum], - rom_offset: usize, + offset: usize, ) -> Result, SynthesisError> { - let pc_offset_in_z = AllocatedNum::alloc(cs.namespace(|| "pc_offset_in_z"), || { - Ok(pc_counter.get_value().unwrap() + F::from(rom_offset as u64)) + let index = AllocatedNum::alloc(cs.namespace(|| "index"), || { + Ok(index_before_offset.get_value().unwrap() + F::from(offset as u64)) })?; // select target when index match or empty @@ -44,7 +49,7 @@ fn get_num_at_pcindex>( let equal_bit = Boolean::from(alloc_num_equals( cs.namespace(|| format!("check selected_circuit_index {:?} equal bit", i)), &i_alloc, - &pc_offset_in_z, + &index, )?); conditionally_select( cs.namespace(|| format!("select on index namespace {:?}", i)), @@ -70,51 +75,111 @@ type G2 = bn256_grumpkin::grumpkin::Point; pub(crate) fn nova_prove( analyzed: &Analyzed, + main_machine: &Machine, _: Vec<(&str, Vec)>, _: Vec<(&str, Vec)>, ) -> () { + // collect all instr from pil file + let instr_index_mapping: BTreeMap = main_machine + .instructions + .iter() + .flat_map(|k| Some(k.name.clone())) + .enumerate() + .map(|(i, v)| (v.clone(), i)) + .collect(); + // collect all register + let regs_index_mapping: BTreeMap = main_machine + .registers + .iter() + .filter(|reg| { + reg.flag.is_none() // only collect writable register + }) + .enumerate() + .map(|(i, reg)| (reg.name.clone(), i)) + .collect(); + // instruction <-> io mapping + let instr_io_mapping = main_machine + .instructions + .iter() + .map(|k| { + let input_index = k + .params + .inputs + .params + .iter() + .map(|input_param| { + assert_eq!(input_param.ty.is_none(), true); // do not support signature other than register type + input_param.name.clone() + }) + .collect::>(); + let output_index = if let Some(output) = &k.params.outputs { + output + .params + .iter() + .map(|output_param| { + assert_eq!(output_param.ty.is_none(), true); // do not support signature other than register type + output_param.name.clone() + }) + .collect::>() + } else { + vec![] + }; + (k.name.clone(), (input_index, output_index)) + }) + .collect::, Vec)>>(); + // firstly, compile pil ROM to simple memory commitment // Idea to represent a instruction is by linear combination lc(, operand1, operand2, operand3, ...), // operand can be register or constant. For register, first we translate to register index - // inst_encoded = + operand1 * 2**32 + operand2 * 2 ** 64 + operand3 * 2 ** 128 + ... - // each operand should be range check into 32 bit + // inst_encoded = + operand1 * 2**16 + operand2 * 2 ** 32 + operand3 * 2 ** 48 + ... + // each operand should be range check into 16 bit // currently max support operand is 6, to fit into overall 254 bit value // TODO1: move this part to other place, like params generator // TODO2: replace this part with more efficient memory commitment strategy, e.g. folding KZG - let rom = []; // Rom can be arbitrary length. - - // collect all instr from pil file - let all_instr: Vec = analyzed - .definitions - .iter() - .flat_map(|(k, _)| { - if k.starts_with("main.instr") { - Some(k.clone()) - } else { - None + // TODO3: figure out how to encode constant + + let rom = main_machine.rom.as_ref().map(|rom| { + rom.statements.iter().map(|statement| match statement { + FunctionStatement::Assignment(AssignmentStatement { + lhs, + rhs, + .. // ignore start + }) => { + assert_eq!(lhs.len(), 1); // only accept lhs register assigment to be 1 + let instr_name = match rhs { + box ast::parsed::Expression::FunctionCall(FunctionCall{id, ..}) => id, + _ => unimplemented!(), + }; + + let mut regs_index: Vec = match rhs { + box ast::parsed::Expression::FunctionCall(FunctionCall{arguments, ..}) => arguments.iter().map(|argument| match argument { + ast::parsed::Expression::PolynomialReference(ast::parsed::PolynomialReference{ namespace, name, index, next }) => { + assert_eq!(*next, false); + assert_eq!(*namespace, None); + assert_eq!(*index, None); + regs_index_mapping[name] + }, + // TODO need to support constant + x => unimplemented!("unsupported expression {:?}", x), + }), + _ => unimplemented!(), + }.collect(); + + let output_reg_index:Vec = lhs.iter().map(|x| regs_index_mapping[x]).collect(); + regs_index.extend(output_reg_index); // append output register to the back of input register + if let Some(instr_index) = instr_index_mapping.get(instr_name) { + iter::once::(*instr_index).chain(regs_index.into_iter()).rev().map(BigUint::from).reduce(|a, b| a * BigUint::from(1_u32 << 16) + b).unwrap() + } else { + panic!("instr_name {:?} not found in instr_index_mapping {:?}", instr_name, instr_index_mapping); + } } - }) - .collect::>(); - - // Println analyzed structure - // analyzed - // .source_order - // .iter() - // .for_each(|f| println!("source order {:?}", f)); - - // analyzed - // .public_declarations - // .iter() - // .for_each(|f| println!("public_declarations {:?}", f)); - - // analyzed - // .definitions - // .iter() - // .for_each(|f| println!("definition {:?}", f)); + s => unimplemented!("unimplemented statement {:?}", s), + }).collect::>() + }).unwrap(); // build step circuit - let circuit_secondary = SecondaryStepCircuit::new(rom.len()); - let num_augmented_circuit = all_instr.len(); + let circuit_secondary = SecondaryStepCircuit::new(regs_index_mapping.len() + rom.len()); + let num_augmented_circuit = instr_index_mapping.len(); // running claims is the list of running instances witness let mut running_claims: Vec< @@ -124,14 +189,16 @@ pub(crate) fn nova_prove( NovaStepCircuit<::Scalar, T>, SecondaryStepCircuit<::Scalar>, >, - > = all_instr + > = instr_index_mapping .iter() - .map(|instr_name| { + .map(|(instr_name, index)| { // Structuring running claims let test_circuit = NovaStepCircuit::<::Scalar, T>::new( rom.len(), instr_name.to_string(), analyzed, + &instr_io_mapping[instr_name], + regs_index_mapping.len(), ); let running_claim = RunningClaim::< G1, @@ -139,7 +206,7 @@ pub(crate) fn nova_prove( NovaStepCircuit<::Scalar, T>, SecondaryStepCircuit<::Scalar>, >::new( - 0, + *index, test_circuit, circuit_secondary.clone(), num_augmented_circuit, @@ -148,6 +215,12 @@ pub(crate) fn nova_prove( }) .collect(); + // sort running claim by augmented_index, assure we can fetch them by augmented index later + running_claims.sort_by(|a, b| { + a.get_augmented_circuit_index() + .cmp(&b.get_augmented_circuit_index()) + }); + // TODO detect the max circuit iterate and inspect all running claim R1CS shape, instead of assume first 1 is largest // generate the commitkey based on max num of constraints and reused it for all other augmented circuit // let (max_index_circuit, _) = running_claims @@ -171,20 +244,22 @@ pub(crate) fn nova_prove( let digest = compute_digest::>(&[running_claims[0].get_publicparams()]); - let num_steps = rom.len(); + let num_steps = 1; let initial_program_counter = ::Scalar::from(0); + // process register + let mut z0_primary: Vec<::Scalar> = iter::repeat(::Scalar::zero()) + .take(instr_index_mapping.len()) + .collect(); // extend z0_primary/secondary with rom content - let mut z0_primary = vec![]; - z0_primary.extend( - rom.iter() - .map(|memory_value| ::Scalar::from(*memory_value as u64)), - ); - let mut z0_secondary = vec![]; - z0_secondary.extend( - rom.iter() - .map(|memory_value| ::Scalar::from(*memory_value as u64)), - ); + z0_primary.extend(rom.iter().map(|memory_value| { + let mut memory_value_bytes = memory_value.to_bytes_le(); + memory_value_bytes.resize(32, 0); + ::Scalar::from_bytes(&memory_value_bytes.try_into().unwrap()).unwrap() + })); + let z0_secondary: Vec<::Scalar> = iter::repeat(::Scalar::zero()) + .take(z0_primary.len() as usize) + .collect(); let mut recursive_snark_option: Option> = None; @@ -196,18 +271,20 @@ pub(crate) fn nova_prove( .unwrap_or_else(|| initial_program_counter); // TODO decompose value_in_rom into (opcode_index, input_operand1, input_operand2, ... output_operand) as witness, // then using opcode_index to invoke respective running instance - let value_in_rom = rom[u32::from_le_bytes( + let value_in_rom = &rom[u32::from_le_bytes( // convert program counter from field to usize (only took le 4 bytes) program_counter.to_repr().as_ref()[0..4].try_into().unwrap(), ) as usize]; - let opcode_index = value_in_rom; + let mut opcode_index_bytes = (value_in_rom % BigUint::from(1_u32 << 16)).to_bytes_le(); + opcode_index_bytes.resize(4, 0); + let opcode_index = u32::from_le_bytes(opcode_index_bytes.try_into().unwrap()); let mut recursive_snark = recursive_snark_option.unwrap_or_else(|| { RecursiveSNARK::iter_base_step( - &running_claims[opcode_index], + &running_claims[opcode_index as usize], digest, program_counter, - value_in_rom, + opcode_index as usize, num_augmented_circuit, &z0_primary, &z0_secondary, @@ -215,13 +292,20 @@ pub(crate) fn nova_prove( .unwrap() }); - let res = - recursive_snark.prove_step(&running_claims[opcode_index], &z0_primary, &z0_secondary); + let res = recursive_snark.prove_step( + &running_claims[opcode_index as usize], + &z0_primary, + &z0_secondary, + ); if let Err(e) = &res { println!("res failed {:?}", e); } assert!(res.is_ok()); - let res = recursive_snark.verify(&running_claims[opcode_index], &z0_primary, &z0_secondary); + let res = recursive_snark.verify( + &running_claims[opcode_index as usize], + &z0_primary, + &z0_secondary, + ); if let Err(e) = &res { println!("res failed {:?}", e); } @@ -247,9 +331,9 @@ pub(crate) fn nova_prove( // TODO optmize constraints to leverage R1CS cost-free additive // TODO combine FieldElement & PrimeField -fn build_constraint_from_expr>( +fn evaluate_expr>( mut cs: CS, - poly_map: &mut HashMap>, + poly_map: &mut BTreeMap>, expr: &Expression, ) -> Result, SynthesisError> { match expr { @@ -264,18 +348,22 @@ fn build_constraint_from_expr { + let name = name.strip_prefix("main.").unwrap(); // TODO FIXME: trim namespace should be happened in unified place assert_eq!(*index, None); assert_eq!(*next, false); - // TODO figure out a way to insert witness - let num = AllocatedNum::alloc(cs.namespace(|| name.clone()), || { - Err(SynthesisError::AssignmentMissing) - })?; - poly_map.insert(name.clone(), num.clone()); // update to polymap - Ok(num) + Ok(poly_map + .entry(name.to_string()) + .or_insert_with(|| { + AllocatedNum::alloc(cs.namespace(|| format!("{:?}.{:?}", expr, name)), || { + Err(SynthesisError::AssignmentMissing) + }) + .unwrap() + }) + .clone()) } Expression::BinaryOperation(lhe, op, rhe) => { - let lhe = build_constraint_from_expr(cs.namespace(|| "lhe"), poly_map, lhe)?; - let rhe = build_constraint_from_expr(cs.namespace(|| "rhe"), poly_map, rhe)?; + let lhe = evaluate_expr(cs.namespace(|| "lhe"), poly_map, lhe)?; + let rhe = evaluate_expr(cs.namespace(|| "rhe"), poly_map, rhe)?; match op { BinaryOperator::Add => add_allocated_num(cs, &lhe, &rhe), BinaryOperator::Sub => { @@ -293,12 +381,44 @@ fn build_constraint_from_expr>( + expr: &Expression, + instr_name: &String, +) -> Option>> { + match expr { + Expression::Number(_) => None, + // this is refer to another polynomial, in other word, witness + Expression::PolynomialReference(PolynomialReference { .. }) => None, + Expression::BinaryOperation(lhe, operator, rhe) => { + let find_match_expr = match lhe { + // early pattern match on lhs to retrive the instr * () + box Expression::PolynomialReference(PolynomialReference { name, .. }) => { + if name == instr_name && *operator == BinaryOperator::Mul { + Some(rhe) + } else { + None + } + } + _ => None, + }; + find_match_expr + .cloned() + .or_else(|| find_pc_expression::(rhe, instr_name)) + .or_else(|| find_pc_expression::(lhe, instr_name)) + } + Expression::Constant(_) => None, + _ => unimplemented!("{:?}", expr), + } +} + #[derive(Clone, Debug)] pub struct NovaStepCircuit<'a, F: PrimeField, T: FieldElement> { _p: PhantomData, - rom_size: usize, + rom_len: usize, identity_name: String, + io_assign_reg_name: &'a (Vec, Vec), // input,output index analyzed: &'a Analyzed, + num_registers: usize, } impl<'a, F, T> NovaStepCircuit<'a, F, T> @@ -307,11 +427,19 @@ where T: FieldElement, { /// new TrivialTestCircuit - pub fn new(rom_size: usize, identity_name: String, analyzed: &'a Analyzed) -> Self { + pub fn new( + rom_len: usize, + identity_name: String, + analyzed: &'a Analyzed, + io_assign_reg_name: &'a (Vec, Vec), + num_registers: usize, + ) -> Self { NovaStepCircuit { - rom_size, + rom_len, identity_name, analyzed, + io_assign_reg_name, + num_registers, _p: PhantomData, } } @@ -323,7 +451,7 @@ where T: FieldElement, { fn arity(&self) -> usize { - self.rom_size // value + rom[].len() + self.num_registers + self.rom_len } fn synthesize>( @@ -332,22 +460,13 @@ where _pc_counter: &AllocatedNum, z: &[AllocatedNum], ) -> Result<(AllocatedNum, Vec>), SynthesisError> { - // 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 - // register value can be constrait via `multiple select + sum` with register index on nova `zi` state - // output register need to be constraints in the last of synthesize - - // NOTES: things that do not support - // 1. next query. only support pc as next, other value are all query on same rotation - // ... + // process constants and build map for its reference + let mut poly_map = BTreeMap::new(); - // TODO decompose ROM[pc] into lc(opcode_index, operand_index1, operand_index2, ... operand_output) - // TODO Then constraints X - register[operand_index1] = 0, Y - register[operand_index2] = 0, Z - register[operand_output] = 0 - // Here suppose X, Y is input registers, and Z is output register. + // add pc + poly_map.insert("pc".to_string(), _pc_counter.clone()); - // process constants and build map for its reference - let mut poly_map = HashMap::new(); + // 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( @@ -357,10 +476,85 @@ where poly_map.insert(k.clone(), a); Ok::<(), SynthesisError>(()) })?; + // add constant -1 poly_map.insert( "-1".to_string(), AllocatedNum::alloc(cs.namespace(|| "constant -1"), || Ok(F::from(1).neg()))?, ); + // add constant 1 + poly_map.insert("1".to_string(), alloc_one(cs.namespace(|| "constant 1"))?); + // add constant 0 + poly_map.insert("0".to_string(), alloc_zero(cs.namespace(|| "constant 0"))?); + // add const 1 << 16 + poly_map.insert( + "2^16".to_string(), + AllocatedNum::alloc(cs.namespace(|| "constant 2^16"), || { + Ok(F::from(1_u64 << 16)) + })?, + ); + + // 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 + // register value can be constrait via `multiple select + sum` with register index on nova `zi` state + // output register need to be constraints in the last of synthesize + + // NOTES: things that do not support + // 1. next query. only support pc as next, other value are all query on same rotation + // ... + + let rom_value = get_num_at_index( + cs.namespace(|| "rom value"), + _pc_counter, + z, + self.num_registers, + )?; + let (input_reg_names, output_reg_names) = self.io_assign_reg_name; + let opcode_index = AllocatedNum::alloc(cs.namespace(|| "opcode_decompose"), || { + Err(SynthesisError::AssignmentMissing) + })?; + // TODO fill witness + // TODO Need to have range check on decomposed value to assure each of them is 2^16 + let input_indexs = (0..input_reg_names.len()) + .map(|i| { + AllocatedNum::alloc( + cs.namespace(|| format!("input_index_decompose {:?}", i)), + || Err(SynthesisError::AssignmentMissing), + ) + }) + .collect::>, SynthesisError>>()?; + let output_indexs = (0..output_reg_names.len()) + .map(|i| { + AllocatedNum::alloc( + cs.namespace(|| format!("output_index_decompose {:?}", i)), + || Err(SynthesisError::AssignmentMissing), + ) + }) + .collect::>, SynthesisError>>()?; + let linear_combination = iter::once(&opcode_index) + .chain(input_indexs.iter()) + .chain(output_indexs.iter()) + .rev() + .enumerate() + .try_fold(poly_map["0"].clone(), |acc, (index, a)| { + let acc_mul = mul_allocated_num( + cs.namespace(|| format!("decompose_mul at index {:?}", index)), + &acc, + &poly_map["2^16"], + )?; + add_allocated_num( + cs.namespace(|| format!("decompose_add at index {:?}", index)), + &acc_mul, + &a, + ) + })?; + // constraint ROM[pc] == lc(opindex, input_reg_index1, input_reg_index2, ..., out_reg_index1, out_reg_index2,...) + cs.enforce( + || "decomposed equality", + |lc| lc + linear_combination.get_variable(), + |lc| lc + CS::one(), + |lc| lc + rom_value.get_variable(), + ); for id in &self.analyzed.identities { match id.kind { @@ -396,7 +590,8 @@ where if contains_next_ref == true { unimplemented!("not support column next in folding scheme") } - let num_eval = build_constraint_from_expr( + let mut cs = cs.namespace(|| format!("rhs {:?}", rhs)); + let num_eval = evaluate_expr( cs.namespace(|| format!("constraint {:?}", name)), &mut poly_map, rhs, @@ -407,15 +602,123 @@ where |lc| lc + CS::one(), |lc| lc, ); - println!("polynomial_ref_name {:?}", name); } } - _ => unimplemented!(), + _ => (), } } - // constraint memory write index - Ok((_pc_counter.clone(), z.to_vec())) + // constraint input name to index value + input_indexs + .iter() + .zip_eq(input_reg_names.iter()) + .try_for_each(|(index, reg_name)| { + let reg_value = get_num_at_index(cs.namespace(|| "regname"), index, z, 0)?; + if let Some(reg) = poly_map.get(reg_name) { + cs.enforce( + || format!("{:?} - reg[{:?}_index] = 0", reg_name, reg_name), + |lc| lc + reg_value.get_variable(), + |lc| lc + CS::one(), + |lc| lc + reg.get_variable(), + ); + Ok::<(), SynthesisError>(()) + } else { + panic!( + "missing output reg name {:?} in polymap {:?}", + reg_name, + poly_map.keys() + ); + } + })?; + + // zi_next[index] = index == output_index ? reg_assign[output_reg_name]: zi[index] + let zi_next = output_indexs + .iter() + .zip_eq(output_reg_names.iter()) + .try_fold(z.to_vec(), |acc, (output_index, output_reg_name)| { + (0..z.len()) + .map(|i| { + let i_alloc = AllocatedNum::alloc( + cs.namespace(|| format!("output reg i{:?} allocated", i)), + || Ok(F::from(i as u64)), + )?; + let equal_bit = Boolean::from(alloc_num_equals( + cs.namespace(|| format!("check reg {:?} equal bit", i)), + &i_alloc, + &output_index, + )?); + if let Some(output) = poly_map.get(output_reg_name) { + conditionally_select( + cs.namespace(|| format!("zi_next constraint with register index {:?} on reg name {:?}",i, output_reg_name)), + output, + &acc[i], + &equal_bit, + ) + } else { + panic!( + "missing output reg name {:?} in polymap {:?}", + output_reg_name, + poly_map.keys() + ); + } + }) + .collect::>, SynthesisError>>() + })?; + + // process pc_next + for id in &self.analyzed.identities { + match id.kind { + IdentityKind::Polynomial => { + // everthing should be in left.selector only + assert_eq!(id.right.expressions.len(), 0); + assert_eq!(id.right.selector, None); + assert_eq!(id.left.expressions.len(), 0); + + let exp = id.expression_for_poly_id(); + + if let Expression::BinaryOperation( + box Expression::PolynomialReference( + PolynomialReference { name, next, .. }, + .., + ), + BinaryOperator::Sub, + box rhs, + .., + ) = exp + { + if name == "main.pc" && *next == true { + // lhs is `pc'` + let identity_name = format!("main.instr_{}", self.identity_name); + let exp = find_pc_expression::(rhs, &identity_name); + let pc_next = exp + .and_then(|expr| { + evaluate_expr( + cs.namespace(|| format!("pc eval on {:?}", expr)), + &mut poly_map, + &expr, + ) + .ok() + }) + .unwrap_or_else(|| { + // by default pc + 1 + add_allocated_num( + cs.namespace(|| { + format!("instr {:?} pc + 1", identity_name) + }), + &poly_map["pc"], + &poly_map["1"], + ) + .unwrap() + }); + poly_map.insert("pc_next".to_string(), pc_next); + } + } + } + _ => (), + } + } + + Ok((poly_map["pc_next"].clone(), zi_next)) } fn output(&self, pc: F, z: &[F]) -> (F, Vec) { @@ -427,7 +730,7 @@ where #[derive(Clone, Debug, Default)] pub struct SecondaryStepCircuit { _p: PhantomData, - rom_size: usize, + arity_len: usize, } impl SecondaryStepCircuit @@ -435,9 +738,9 @@ where F: PrimeField, { /// new TrivialTestCircuit - pub fn new(rom_size: usize) -> Self { + pub fn new(arity_len: usize) -> Self { SecondaryStepCircuit { - rom_size, + arity_len, _p: PhantomData, } } @@ -448,7 +751,7 @@ where F: PrimeField, { fn arity(&self) -> usize { - self.rom_size // value + rom[].len() + self.arity_len } fn synthesize>( diff --git a/zero_nova/src/nonnative/bignat.rs b/zero_nova/src/nonnative/bignat.rs index 55d73b5475..de017ba439 100644 --- a/zero_nova/src/nonnative/bignat.rs +++ b/zero_nova/src/nonnative/bignat.rs @@ -1,3 +1,4 @@ +#[allow(dead_code)] use super::{ util::{ Bitvector, Num, {f_to_nat, nat_to_f}, diff --git a/zero_nova/src/prover.rs b/zero_nova/src/prover.rs index eaa60cea34..d4531d84c7 100644 --- a/zero_nova/src/prover.rs +++ b/zero_nova/src/prover.rs @@ -1,20 +1,22 @@ -use ast::analyzed::Analyzed; +use ast::{analyzed::Analyzed, asm_analysis::Machine}; use number::FieldElement; use crate::circuit_builder::nova_prove; pub fn prove_ast_read_params( pil: &Analyzed, + main_machine: &Machine, fixed: Vec<(&str, Vec)>, witness: Vec<(&str, Vec)>, ) -> () { - prove_ast(pil, fixed, witness) + prove_ast(pil, main_machine, fixed, witness) } pub fn prove_ast( pil: &Analyzed, + main_machine: &Machine, fixed: Vec<(&str, Vec)>, witness: Vec<(&str, Vec)>, ) -> () { log::info!("Starting proof generation..."); - let _ = nova_prove(pil, fixed, witness); + let _ = nova_prove(pil, main_machine, fixed, witness); } diff --git a/zero_nova/src/utils.rs b/zero_nova/src/utils.rs index 4f1f53660d..1a3808f051 100644 --- a/zero_nova/src/utils.rs +++ b/zero_nova/src/utils.rs @@ -1,4 +1,5 @@ //! This module implements various low-level gadgets, which is copy from Nova non-public mod +#[allow(dead_code)] use super::nonnative::bignat::{nat_to_limbs, BigNat}; use bellperson::{ gadgets::{ @@ -433,7 +434,6 @@ pub fn select_num_or_one>( Ok(c) } -#[allow(dead_code)] /// c = a + b where a, b is AllocatedNum pub fn add_allocated_num>( mut cs: CS, diff --git a/zero_nova/zero.asm b/zero_nova/zero.asm index a9ca1635cf..87c64444cc 100644 --- a/zero_nova/zero.asm +++ b/zero_nova/zero.asm @@ -1,6 +1,6 @@ machine NovaZero { - degree 12; + degree 1; // this simple machine does not have submachines @@ -31,8 +31,8 @@ machine NovaZero { instr incr X -> Y { // range check on X - Y = Z + 1, // this one work means assignment register signature `X -> Y` doen't take effect lol ? - // Y = X + 1, + // Y = Z + 1, // this one work means assignment register signature `X -> Y` doen't take effect lol ? + Y = X + 1, Y = x_b0 + x_b1 * 2**1 + x_b2 * 2**2 + x_b3 * 2**3, pc' = pc + 1 } @@ -57,10 +57,10 @@ machine NovaZero { // the main function assigns the first prover input to A, increments it, decrements it, and loops forever function main { - x2 <=X= ${ ("input", 0) }; + // x2 <=X= ${ ("input", 0) }; x3 <=Y= incr(x2); // it seems augmented circuit need to be invoked by string, e.g. incr x2 <=Y= decr(x3); - assert_zero x2; - loop; + // assert_zero x2; + // loop; } }