From 8d639ade3fae0f200dde4489cbc8f5749e547cd3 Mon Sep 17 00:00:00 2001 From: "sm.wu" Date: Fri, 11 Aug 2023 16:19:22 +0800 Subject: [PATCH] nova support label functionality --- nova/README.md | 21 ++++--- nova/src/circuit.rs | 118 +++++++++++++++++++----------------- nova/src/circuit_builder.rs | 50 +++++++++++---- nova/src/lib.rs | 6 +- nova/zero.asm | 7 ++- 5 files changed, 118 insertions(+), 84 deletions(-) diff --git a/nova/README.md b/nova/README.md index 3e48d1069..599cc6960 100644 --- a/nova/README.md +++ b/nova/README.md @@ -14,26 +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) +### ROM encoding & label +For each statement in main.ROM, we will encode it as a linear combination under 2 power of LIMB_SIZE, and the LIMB_SIZE is configurable. +ROM array are attached 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`, it will be convert to respective pc index. + +Since each instruction circuit has it own params type definition, different constraints circuit will be compiled to handle above situation automatically. + ### Nova state & constraints Nova state layout as z0 = `(pc, [writable register...] ++ public io ++ ROM)` - public io := array of public input input from prover/verifier - ROM := 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 param1, input param2,...output param1, ...], 1 << limb_width) = 0` +1. sequence constraints => `rom_value_at_current_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. - ### Public IO In powdr-asm, an example of psuedo instruction to query public input ``` diff --git a/nova/src/circuit.rs b/nova/src/circuit.rs index a85cbd104..658f3fc25 100644 --- a/nova/src/circuit.rs +++ b/nova/src/circuit.rs @@ -320,7 +320,61 @@ where ); } - // constraint input name to index value + // process pc_next + // TODO: very inefficient to go through all identities for each folding, need optimisation + 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 + { + // lhs is `pc'` + if name == "main.pc" && *next { + 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( + // evaluate rhs pc bumping logic + cs.namespace(|| format!("pc eval on {}", expr)), + &mut poly_map, + &expr, + self.witgen.clone(), + ) + .ok() + }) + .unwrap_or_else(|| { + // by default pc + 1 + add_allocated_num( + cs.namespace(|| format!("instr {} pc + 1", identity_name)), + &poly_map["pc"], + &poly_map["ONE"], + ) + .unwrap() + }); + poly_map.insert("pc_next".to_string(), pc_next); + } + } + } + _ => (), + } + } + + // constraint input param to assigned reg value input_params_allocnum .iter() .zip_eq(input_params.iter()) @@ -353,13 +407,20 @@ where )?, ) }, + // label + Param { name, ty: Some(ty) } if ty == "label" => { + ( + format!("instr_{}_param_{}", self.identity_name, name), + index.clone(), + ) + }, s => { unimplemented!("not support {}", s) }, }; if let Some(reg) = poly_map.get(&name) { cs.enforce( - || format!("{} - reg[{}_index] = 0", params, params), + || format!("input params {} - reg[{}_index] = 0", params, params), |lc| lc + value.get_variable(), |lc| lc + CS::one(), |lc| lc + reg.get_variable(), @@ -418,59 +479,6 @@ where }, )?; - // process pc_next - // TODO: very inefficient to go through all identities for each folding, need optimisation - 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 - { - // lhs is `pc'` - if name == "main.pc" && *next { - 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( - // evaluate rhs pc bumping logic - cs.namespace(|| format!("pc eval on {}", expr)), - &mut poly_map, - &expr, - self.witgen.clone(), - ) - .ok() - }) - .unwrap_or_else(|| { - // by default pc + 1 - add_allocated_num( - cs.namespace(|| format!("instr {} pc + 1", identity_name)), - &poly_map["pc"], - &poly_map["ONE"], - ) - .unwrap() - }); - poly_map.insert("pc_next".to_string(), pc_next); - } - } - } - _ => (), - } - } Ok((poly_map["pc_next"].clone(), zi_next)) } } diff --git a/nova/src/circuit_builder.rs b/nova/src/circuit_builder.rs index 82a5cf5fb..4108b089d 100644 --- a/nova/src/circuit_builder.rs +++ b/nova/src/circuit_builder.rs @@ -7,7 +7,9 @@ use std::{ use ast::{ analyzed::Analyzed, - asm_analysis::{AssignmentStatement, FunctionStatement, InstructionStatement, Machine}, + asm_analysis::{ + AssignmentStatement, FunctionStatement, InstructionStatement, LabelStatement, Machine, + }, parsed::{ asm::{FunctionCall, Param}, Expression::Number, @@ -123,13 +125,22 @@ pub(crate) fn nova_prove( // TODO1: move this part to setup stage. // TODO2: replace this part with more efficient memory commitment strategy, e.g. folding KZG + let mut label_pc_mapping = BTreeMap::new(); + let mut pc = 0u64; let rom = main_machine.rom.as_ref().map(|rom| { - rom.statements.iter().map(|statement| match statement { + rom.statements.iter().flat_map(|statement| { + + match statement { + FunctionStatement::Label(LabelStatement{ name, .. }) => { + label_pc_mapping.insert(name, pc); + None + }, FunctionStatement::Assignment(AssignmentStatement { lhs, rhs, .. // ignore start }) => { + pc += 1; let instr_name: String = match rhs { box ast::parsed::Expression::FunctionCall(FunctionCall{id, ..}) => { assert!(id != FREE_INPUT_INSTR_NAME, "{} is a reserved instruction name", FREE_INPUT_INSTR_NAME); @@ -151,7 +162,12 @@ pub(crate) fn nova_prove( assert!(!*next); assert_eq!(*namespace, None); assert_eq!(*index, None); - ::Scalar::from(regs_index_mapping[name] as u64) + // label or register + if let Some(label_pc) = label_pc_mapping.get(name) { + ::Scalar::from(*label_pc) + }else { + ::Scalar::from(regs_index_mapping[name] as u64) + } }, Number(n) => { ::Scalar::from_bytes(&n.to_bytes_le().try_into().unwrap()).unwrap() @@ -180,20 +196,27 @@ pub(crate) fn nova_prove( io_params.extend(output_params); // append output register to the back of input register // Now we can do linear combination - if let Some(instr_index) = instr_index_mapping.get(&instr_name) { + let rom_value = if let Some(instr_index) = instr_index_mapping.get(&instr_name) { limbs_to_nat(iter::once(::Scalar::from(*instr_index as u64)).chain(io_params), LIMB_WIDTH).to_biguint().unwrap() } else { panic!("instr_name {:?} not found in instr_index_mapping {:?}", instr_name, instr_index_mapping); - } + }; + Some(rom_value) } FunctionStatement::Instruction(InstructionStatement{ instruction, inputs, ..}) => { - - let io_params: Vec<::Scalar> = inputs.iter().map(|argument| match argument { + pc += 1; + let io_params: Vec<::Scalar> = inputs.iter().map(|argument| { + match argument { ast::parsed::Expression::PolynomialReference(ast::parsed::PolynomialReference{ namespace, name, index, next }) => { assert!(!*next); assert_eq!(*namespace, None); assert_eq!(*index, None); - ::Scalar::from(regs_index_mapping[name] as u64) + // label or register + if let Some(label_pc) = label_pc_mapping.get(name) { + ::Scalar::from(*label_pc) + }else { + ::Scalar::from(regs_index_mapping[name] as u64) + } }, Number(n) => ::Scalar::from_bytes(&n.to_bytes_le().try_into().unwrap()).unwrap(), ast::parsed::Expression::UnaryOperation(ope,box Number(n)) => { @@ -204,17 +227,18 @@ pub(crate) fn nova_prove( } }, x => unimplemented!("unsupported expression {:?}", x), - }).collect(); + }}).collect(); // Now we can do linear combination - if let Some(instr_index) = instr_index_mapping.get(instruction) { + let rom_value = if let Some(instr_index) = instr_index_mapping.get(instruction) { limbs_to_nat(iter::once(::Scalar::from(*instr_index as u64)).chain(io_params), LIMB_WIDTH).to_biguint().unwrap() } else { panic!("instr_name {} not found in instr_index_mapping {:?}", instruction, instr_index_mapping); - } + }; + Some(rom_value) } s => unimplemented!("unimplemented statement {:?}", s), - }).collect::>() + }}).collect::>() }).unwrap(); // rom.iter().for_each(|v| println!("rom value {:#32x}", v)); @@ -317,7 +341,7 @@ pub(crate) fn nova_prove( // Have estimate of iteration via length of witness let num_steps = witness.lock().unwrap().num_of_iteration(); for i in 0..num_steps { - println!("round i {}, total step {}", i, num_steps); + println!("round i {}, total step {}", i, num_steps - 1); if i > 0 { // iterate through next witness row witness.lock().unwrap().next(); diff --git a/nova/src/lib.rs b/nova/src/lib.rs index 2320a55ba..77b4c1262 100644 --- a/nova/src/lib.rs +++ b/nova/src/lib.rs @@ -10,6 +10,6 @@ pub use prover::*; /// LIMB WITHD as base, represent 2^16 pub(crate) const LIMB_WIDTH: usize = 16; -pub(crate) const FREE_INPUT_INSTR_NAME: &'static str = "free_input_instr"; -pub(crate) const FREE_INPUT_TY: &'static str = "free_input_ty"; -pub(crate) const FREE_INPUT_DUMMY_REG: &'static str = "free_input_dummy_reg"; +pub(crate) const FREE_INPUT_INSTR_NAME: &str = "free_input_instr"; +pub(crate) const FREE_INPUT_TY: &str = "free_input_ty"; +pub(crate) const FREE_INPUT_DUMMY_REG: &str = "free_input_dummy_reg"; diff --git a/nova/zero.asm b/nova/zero.asm index 89df95755..91f5a1609 100644 --- a/nova/zero.asm +++ b/nova/zero.asm @@ -64,8 +64,8 @@ machine NovaZero { } // an instruction only proceed pc + 1 if X = 0 - instr contz X { - pc' = (1 - XIsZero) * (pc - 1) + XIsZero * (pc + 1) + instr bnz X, Y: label { + pc' = (1 - XIsZero) * (Y) + XIsZero * (pc + 1) } instr assert_zero X { @@ -87,8 +87,9 @@ machine NovaZero { x0 <=Z= sub(x0, x0); // x0 - x0 = 0 assert_zero x0; // x0 == 0 x1 <=X= ${ ("input", 1) }; + LOOP:: x1 <=Z= addi(x1, -1); - contz x1; + bnz x1, LOOP; assert_zero x1; // x1 == 0 loop; }