nova support signed constant ROM encoding

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

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::<Option<&Param>>(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::<Result<Vec<AllocatedNum<F>>, SynthesisError>>()?;
 

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<T: FieldElement>(
                             let value = <G1 as Group>::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<T: FieldElement>(
                         let value = <G1 as Group>::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<T: FieldElement>(
     // 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: <G1 as Group>::Scalar,
+    nbit: usize,
+) -> <G1 as Group>::Scalar {
+    let value = value.to_bytes();
+    let (lsb, msb) = value.split_at(nbit / 8);
+    assert_eq!(
+        msb.iter().map(|v| *v as usize).sum::<usize>(),
+        0,
+        "value {:?} is overflow",
+        value
+    );
+    let mut lsb = lsb.to_vec();
+    lsb.resize(32, 0);
+    let value = <G1 as Group>::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 =
+        <G1 as Group>::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);
+
+    <G1 as Group>::Scalar::from_bytes(&value_neg[..].try_into().unwrap()).unwrap()
+}

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<F: PrimeField, CS: ConstraintSystem<F>>(
 ) -> Result<AllocatedNum<F>, SynthesisError> {
     let allocations: Vec<Variable> = value.to_repr().as_bits::<Lsb0>()[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<F: PrimeField, CS: ConstraintSystem<F>>(
             )?;
             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: PrimeField, CS: ConstraintSystem<F>>(
             f = f.double();
             l
         });
-    let value = AllocatedNum::alloc(cs.namespace(|| "alloc const"), || Ok(value))?;
-    let sum_lc = LinearCombination::zero() + value.get_variable() - &sum;
+    let value_alloc =
+        AllocatedNum::alloc(cs.namespace(|| format!("{:?} alloc const", value)), || {
+            Ok(value)
+        })?;
+    let sum_lc = LinearCombination::zero() + value_alloc.get_variable() - &sum;
     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<F: PrimeFieldExt, CS: ConstraintSystem<F>>(
     Ok(selected_num)
 }
 
+/// get negative field value from signed limb
+pub fn signed_limb_to_neg<F: PrimeFieldExt, CS: ConstraintSystem<F>>(
+    mut cs: CS,
+    limb: &Num<F>,
+    max_limb_plus_one_const: &AllocatedNum<F>,
+    nbit: usize,
+) -> Result<AllocatedNum<F>, 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<F>>(

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;