Nova backend in Supernova R1CS

ast/src/asm_analysis/mod.rs

@@ -42,7 +42,7 @@ pub struct DegreeStatement {
     pub degree: BigUint,
 }
 
-#[derive(Clone)]
+#[derive(Clone, Debug)]
 pub enum FunctionStatement<T> {
     Assignment(AssignmentStatement<T>),
     Instruction(InstructionStatement<T>),
@@ -74,28 +74,28 @@ impl<T> From<DebugDirective> for FunctionStatement<T> {
     }
 }
 
-#[derive(Clone)]
+#[derive(Clone, Debug)]
 pub struct AssignmentStatement<T> {
     pub start: usize,
     pub lhs: Vec<String>,
     pub using_reg: Option<String>,
     pub rhs: Box<Expression<T>>,
 }
 
-#[derive(Clone)]
+#[derive(Clone, Debug)]
 pub struct InstructionStatement<T> {
     pub start: usize,
     pub instruction: String,
     pub inputs: Vec<Expression<T>>,
 }
 
-#[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<T> Machine<T> {
     }
 }
 
-#[derive(Clone, Default)]
+#[derive(Clone, Default, Debug)]
 pub struct Rom<T> {
     pub statements: Vec<FunctionStatement<T>>,
     pub batches: Option<Vec<BatchMetadata>>,

backend/Cargo.toml

@@ -5,9 +5,11 @@ edition = "2021"
 
 [features]
 halo2 = ["dep:halo2"]
+nova = ["dep:nova"]
 
 [dependencies]
 halo2 = { path = "../halo2", optional = true }
+nova = { path = "../nova", optional = true }
 pil_analyzer = { path = "../pil_analyzer" }
 number = { path = "../number" }
 strum = { version = "0.24.1", features = ["derive"] }

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};
@@ -62,6 +62,9 @@ pub struct Halo2MockBackend;
 #[cfg(feature = "halo2")]
 pub struct Halo2AggregationBackend;
 
+#[cfg(feature = "nova")]
+pub struct NovaBackend;
+
 #[cfg(feature = "halo2")]
 impl ProverWithParams for Halo2Backend {
     fn prove<T: FieldElement, R: io::Read>(
@@ -102,3 +105,24 @@ impl ProverAggregationWithParams for Halo2AggregationBackend {
         halo2::prove_aggr_read_proof_params(pil, fixed, witness, proof, params)
     }
 }
+
+#[cfg(feature = "nova")]
+// TODO implement ProverWithoutParams, and remove dependent on main_machine
+impl NovaBackend {
+    pub fn prove<T: FieldElement>(
+        pil: &Analyzed<T>,
+        main_machine: &Machine<T>,
+        fixed: Vec<(&str, Vec<T>)>,
+        witness: Vec<(&str, Vec<T>)>,
+        public_io: Vec<T>,
+    ) -> Option<Proof> {
+        Some(nova::prove_ast_read_params(
+            pil,
+            main_machine,
+            fixed,
+            witness,
+            public_io,
+        ));
+        Some(vec![])
+    }
+}

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;

nova/Cargo.toml

@@ -0,0 +1,31 @@
+[package]
+name = "nova"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+number = { path = "../number" }
+pil_analyzer = { path = "../pil_analyzer" }
+num-traits = "0.2.15"
+num-integer = "0.1.45"
+itertools = "^0.10"
+num-bigint = "^0.4"
+log = "0.4.17"
+rand = "0.8.5"
+pasta_curves = { version = "0.5", features = ["repr-c", "serde"] }
+ast = { version = "0.1.0", path = "../ast" }
+nova-snark = { git = "https://github.com/hero78119/SuperNova.git", branch = "supernova", default-features = false, features = ["supernova"] }
+bellpepper-core = { version="0.2.0", default-features = false }
+bellpepper = { version="0.2.0", default-features = false }
+ff = { version = "0.13.0", features = ["derive"] }
+polyexen = { git = "https://github.com/Dhole/polyexen", branch = "feature/shuffles" }
+
+[dev-dependencies]
+analysis = { path = "../analysis" }
+executor = { path = "../executor" }
+parser = { path = "../parser" }
+asm_to_pil = { path = "../asm_to_pil" }
+test-log = "0.2.12"
+env_logger = "0.10.0"
+linker = { path = "../linker" }
+

nova/README.md

@@ -0,0 +1,124 @@
+Nova
+===========
+This implementation is based on Supernova https://eprint.iacr.org/2022/1758, a Non-Uniform IVC scheme to `solve a stateful machine with a particular instruction set (e.g., EVM, RISC-V)` under R1CS.
+
+This implemetation is based on https://github.com/microsoft/Nova  with toggling "supernova" features
+
+> 07 Aug 2024 Update: supernova PR still under review https://github.com/microsoft/Nova/pull/204. Therefore temporarily depends on private repo https://github.com/hero78119/SuperNova/tree/supernova_trait_mut
+
+### folding schemes of powdr-asm
+Recursive/folding logical boundary is cut on per instruction defined in powdr-asm. Each instruction will form a relaxed running instance in supernova. Therefore, there will be totally `#inst` (relaxed R1CS) running instance. More accurately, it's `#inst + 1` running instance, for extra `+1` is for folding secondary circuit on primary circuit. Detail is omitted and encourge to check Microsoft Nova repo https://github.com/microsoft/Nova for how 2 cycle of curve was implemented
+
+### augmented circuit
+Each instruction is compiled into a step circuit, following Nova(Supernova) paper terminology, it's also called F circuit.
+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 => `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.
+
+### Public IO
+In powdr-asm, an example of psuedo instruction to query public input
+```
+reg <=X= ${ ("input", 0) };
+```
+which means query public input at index `0` and store into reg
+
+In Nova, psuedo instruction is also represented as a individual augmented circuit with below check, similar as other instruction
+- sequence constraints: same as other instruction circuit to check `zi[offset + pc] - linear-combination([opcode_index, input param1, input param2,...output param1, ...], 1 << limb_width) = 0`
+- writable register read/write constraints => `z[public_io_offset] - writable register = 0`
+
+Public-io psuedo instruction is not declared in powdr-asm instruction body. To make the circuit compiler flow similar as other normal instruction, a dummy input/output params will be auto populated, so the constraints for `writable register read/write` will reuse the same flow as others.
+
+### 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 (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
+
+```
+machine NovaZero {
+
+    ...
+    instr incr X -> Y {
+        Y = X + 1,
+    }
+
+    instr decr X -> Y {
+        Y = X - 1
+    }
+
+    instr loop {
+        pc' = pc
+    }
+
+    instr assert_zero X {
+        X = 0
+    }
+
+    // the main function assigns the first prover input to A, increments it, decrements it, and loops forever
+    function main {
+        x0 <=Z= incr(x0); // x0' = 1
+        x0 <=Y= decr(x0) // x0' = 0
+        assert_zero x0; // x0 == 0
+        loop;
+    }
+}
+```
+
+It will be compiled to below R1CS instance
+```
+// in incr instruction circuit
+(X*1 + 1*1) * 1 = Y
+...
+
+// in decr instruction circuit
+(x*1 + 1.inv()) * 1 = Y
+...
+
+// in assert_zero circuit
+(X*1) * 1 = 0
+...
+```
+
+Note that, the only way to pass data to next round is via writable register, so the `<reg>next` will be handled by instruction assignment automatically. There is forbidden to have `<reg>next` usage in instruction body. Only exception is `pc'` value, since the only place to mark next pc value is in instruction body.
+
+The circuit to constraints `Writable Register` will be generate automatically to constraints
+- `zi[end_of_reg_offset + pc] - linear-combination([opcode_index, input reg1, input reg2,..., output reg1, output reg2,...], 1 << limb_width) = 0 // in R1CS`
+- `zi[input reg1] - assignemnt_reg_1 = 0 // constraints equality with respective PIL polynomial reference`
+- `zi[input reg2] - assignemnt_reg_2 = 0 // ...`
+- ...
+- `zi[output reg1] - assignemnt_reg_3 = 0 // output is optional`
+- ...
+
+> For R1CS in the future, a more efficient `memory commitment` should be also part of the Nova state. For example, merkle tree root, or KZG vector commitment. This enable to constraints RAM Read/Write consistency. For KZG, potientially it can fit into R1CS folding scheme by random linear combination and defering the pairing to the last step then SNARK it. See `https://eprint.iacr.org/2019/1047.pdf` `9.2 Optimizations for the polynomial commitment scheme` for pairing linear combination on LHS/RHS which is potientially applicable to folding scheme.
+
+
+### witness assignment
+For 2 groups of constraints in a instruction circuit
+- sequence constraints
+- pil constrains
+
+Powdr framework can infer and provide pil constrains, so in witness assigment we just reuse it.
+For sequence constraints, it's infer via bellpepper R1CS constraints system automatically, since it's transparent in PIL logic.
+
+> An fact is, there are also constraints related to (Super)Nova verifier circuit. Its also automatically infer via `bellpepper R1CS constraints system` automatically, and also encaptulated as blackbox