diff --git a/nova/README.md b/nova/README.md index 3e48d10693..599cc69606 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 a85cbd104f..658f3fc25b 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 82a5cf5fb4..4108b089d4 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/zero.asm b/nova/zero.asm index 89df957556..91f5a16097 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; }