zero nova initial version

polish comments

supernova finish constaints done, add workaround to collect meta info from asm source

more commments

supernova prove&verify successfully

support unsigned const in instruction param

remove temporarily file

rename zero_nova crate to nova

cosmetics comment

cite private mod from nova

unify way to convert between FieldElement & PrimeField

nova crate readme

support PIL constant constraints in R1CS forcely

nova refactor to separate codebase into different mod

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,22 @@ 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>)>,
+    ) -> Option<Proof> {
+        Some(nova::prove_ast_read_params(
+            pil,
+            main_machine,
+            fixed,
+            witness,
+        ));
+        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,30 @@
+[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"] }
+bellperson = { version = "0.25", 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,99 @@
+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)
+
+### Nova state & Constraints
+public input layout as z0 = `(pc, [writable register...] + [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`
+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.
+
+
+### 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.
+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 bellperson 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 `bellperson R1CS constraints system` automatically, and also encaptulated as blackbox