Skip to content

Commit

Permalink
nova support label functionality
Browse files Browse the repository at this point in the history
  • Loading branch information
@hero78119
hero78119 committed Aug 11, 2023
1 parent 9f03bc7 commit 8d639ad
Show file tree
Hide file tree
Showing 5 changed files with 118 additions and 84 deletions.
21 changes: 11 additions & 10 deletions nova/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
```
Expand Down
118 changes: 63 additions & 55 deletions nova/src/circuit.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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::<T, F, CS>(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())
Expand Down Expand Up @@ -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(),
Expand Down Expand Up @@ -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::<T, F, CS>(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))
}
}
Expand Down
50 changes: 37 additions & 13 deletions nova/src/circuit_builder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -123,13 +125,22 @@ pub(crate) fn nova_prove<T: FieldElement>(
// 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);
Expand All @@ -151,7 +162,12 @@ pub(crate) fn nova_prove<T: FieldElement>(
assert!(!*next);
assert_eq!(*namespace, None);
assert_eq!(*index, None);
<G1 as Group>::Scalar::from(regs_index_mapping[name] as u64)
// label or register
if let Some(label_pc) = label_pc_mapping.get(name) {
<G1 as Group>::Scalar::from(*label_pc)
}else {
<G1 as Group>::Scalar::from(regs_index_mapping[name] as u64)
}
},
Number(n) => {
<G1 as Group>::Scalar::from_bytes(&n.to_bytes_le().try_into().unwrap()).unwrap()
Expand Down Expand Up @@ -180,20 +196,27 @@ pub(crate) fn nova_prove<T: FieldElement>(
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(<G1 as Group>::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<<G1 as Group>::Scalar> = inputs.iter().map(|argument| match argument {
pc += 1;
let io_params: Vec<<G1 as Group>::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);
<G1 as Group>::Scalar::from(regs_index_mapping[name] as u64)
// label or register
if let Some(label_pc) = label_pc_mapping.get(name) {
<G1 as Group>::Scalar::from(*label_pc)
}else {
<G1 as Group>::Scalar::from(regs_index_mapping[name] as u64)
}
},
Number(n) => <G1 as Group>::Scalar::from_bytes(&n.to_bytes_le().try_into().unwrap()).unwrap(),
ast::parsed::Expression::UnaryOperation(ope,box Number(n)) => {
Expand All @@ -204,17 +227,18 @@ pub(crate) fn nova_prove<T: FieldElement>(
}
},
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(<G1 as Group>::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::<Vec<BigUint>>()
}}).collect::<Vec<BigUint>>()
}).unwrap();

// rom.iter().for_each(|v| println!("rom value {:#32x}", v));
Expand Down Expand Up @@ -317,7 +341,7 @@ pub(crate) fn nova_prove<T: FieldElement>(
// 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();
Expand Down
6 changes: 3 additions & 3 deletions nova/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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";
7 changes: 4 additions & 3 deletions nova/zero.asm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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;
}
Expand Down

0 comments on commit 8d639ad

Please sign in to comment.