Nova backend in Supernova R1CS #453

hero78119 · 2023-07-31T13:18:10Z

This PR is aimed for powdr-asm VM to support folding scheme nova backend as R1CS, to benefit constant size circuit & prove on arbitrary length of computation

In the prelimenary version, most of circuit logic are in circuit_builder.rs

Features highlights (TBC)

on R1CS, no lookup.
folding per instruction.
ROM lookup will be replaced by memory commitment and handled by nova backend circuit automatically. Inst only need to do range check.
only pc witness support mark next.
...

Features list:

eval polynomials in instr into bellperson constraints.
pil compile to bellman R1CS circuit. constraint ROM, instruction input/output registers mapping.
able to handle instruction with arbitrary length of input params/output params
introduce ROM array to constraint instruction execution order
witness assignement => next challenge part, need to think about how to adapt witness assigment into bellperson framework
accept prover-input
polyomial reference handling in constraints area (outside instruction body) , see comments Nova backend in Supernova R1CS #453 (comment)
label encoding to ROM value

Step to run

compile pil

cargo run --release pil nova/zero.asm --field bn254 -f -o nova -i 10,3

run nova prove step

cargo run --release prove-nova --field bn254 --dir ./nova/ ./nova/zero_opt.pil ./nova/zero.asm -i 10,3

Spotted Issues

(general issue, might be hidden bug) if there are some defined but non-used reg in asm then compile to pil, compile will success also show witness inference success, however some witness are wrong by print out them to check. Detail reason still unknown

hero78119 · 2023-08-02T15:22:11Z

Updated:

pil compile to bellman R1CS circuit is done. ROM, instruct input/output registers are constrainted.
features added: able to handle instruction with arbitrary length of input params/output params
workaround: fetch instruction params definition from asm file, later can think about how to encode this information in PIL.

TODO

(Ongoing) witness assignement => next challenge part, need to think about how to adapt witness assigment into bellperson framework
adapt public input from prover

leonardoalt · 2023-08-03T13:11:40Z

Thanks! I'll start reviewing it today.

hero78119 · 2023-08-03T15:09:17Z

Updated:

witness assignment is done and works well follow existing mechanism
prove on supernova successfully

leonardoalt · 2023-08-04T13:59:57Z

(general issue, might be hidden bug) if there are some defined but non-used reg in asm then compile to pil, compile will success also show witness inference success, however some witness are wrong by print out them to check. Detail reason still unknown

about this @hero78119 . What do you mean by witnesses are wrong? Currently unused columns should be removed completely, so if this is buggy we should open a separate issue and investigate there.

leonardoalt

Basic review for the non-Nova related things. Doing the new nova crate next.

backend/Cargo.toml

leonardoalt · 2023-08-04T14:15:02Z

rust-toolchain.toml

@@ -1,2 +1,2 @@
 [toolchain]
-channel = "stable"
+channel = "nightly"


I don't think this is a good idea... why do we need nightly?

because im using a #![feature(box_patterns)] pattern match to retrieve expression inside Box<Expression> to make code less verbose, and this feature is not in stable channel.
it just temporarily here and will remove it once figure out how to make pattern match efficiently

leonardoalt · 2023-08-04T14:16:05Z

backend/src/lib.rs

@@ -62,6 +62,9 @@ pub struct Halo2MockBackend;
 #[cfg(feature = "halo2")]
 pub struct Halo2AggregationBackend;

+#[cfg(feature = "nova")]
+pub struct NovaBackend;


There's currently a refactoring going on changing this backend crate, #417 . It shouldn't be too hard to rebase after it gets merged.

Notice that after 417 merge, if adding powdr-asm raw parsed data then it will affect other backend, i.e. Halo2 as well, because now prove function are unified.
Since now Nova still need to parse information from powdr-asm meta. Will rebase later once we figure out a better way to deal with meta info from PIL directly.

leonardoalt · 2023-08-04T14:16:34Z

compiler/src/lib.rs

@@ -14,7 +14,8 @@ use json::JsonValue;
 pub mod util;
 mod verify;

-use analysis::analyze;
+// TODO should analyze be `pub`?


If needed, sure.

leonardoalt · 2023-08-04T14:19:46Z

powdr_cli/src/main.rs

@@ -184,6 +186,29 @@ enum Commands {
        params: Option<String>,
    },

+    ProveNova {


It probably does make sense to keep Nova separated from the other backends for now since it needs the asm file too, but eventually we should also just add Nova to the backends enum and support it in the normal pipeline.

zero_nova/Cargo.toml

hero78119 · 2023-08-04T15:16:19Z

PR Updated

support unsigned constant in instruction assignment
=> signed is blocked by unifying FieldElement & PrimeField, since PrimeField very hard to use, however is required by Nova dependency. Still try figure out the way to remove them
code cosmetics, rename to nova crate

(general issue, might be hidden bug) if there are some defined but non-used reg in asm then compile to pil, compile will success also show witness inference success, however some witness are wrong by print out them to check. Detail reason still unknown

about this @hero78119 . What do you mean by witnesses are wrong? Currently unused columns should be removed completely, so if this is buggy we should open a separate issue and investigate there.

Witness are wrong means the witness doesnt satisfy the constraints, I will try to reproduce it later and if confirm, will report in a separate issue

leonardoalt

A few more comments, missing only the main part of circuit_builder.rs

leonardoalt · 2023-08-04T14:23:32Z

zero_nova/zero.asm

+
+    instr incr X -> Y {
+        // range check on X
+        // Y = Z + 1, // this one work means assignment register signature `X -> Y` doen't take effect lol ?


Currently all registers are available in instructions so you can use the byte registers for example for byte composition, the input/output ones are just to typecheck the calls and do assignments.

yes I aware of this.

As the time of writing, now each instruction augmented circuit only parse the constraints inside the instruction definition, but not parsing the general constraints due to efficiency concern.

@leonardoalt I think there are 2 design choices

inline support: since each instruction is self-contained in current folding schems, do you think it make sense to have some inline feature during asm -> pil compiler, so all the constraints being touch by instruction A, it will be layout in the line of i.e. instr_A * (all the constrains chain) ?

nova augment circuit builder optimisation: introduce some lazily constraints compiling strategy in nova augment circuit parsing, such as DFS recursive traverse to expand polynomial reference in constraints area. This is optimise so other un-related constraints will not be compiled into the circuit

or is there other better way is welcome :)

Currently this is done like this, but I think inside constraints for next-registers. Need to think about it.

This direction sounds good, yes.

Another thing that I haven't understood so far is, what happens to the constraints block of a machine? These constraints should be true for every line, so are they used in the single-instruction-circuits?

zero_nova/zero.asm

zero_nova/src/nonnative/util.rs

zero_nova/src/utils.rs

zero_nova/src/circuit_builder.rs

leonardoalt · 2023-08-04T16:56:13Z

The comments above show as outdated because of the change in the directory name from zero_nova to nova, but you can still just answer them in the comments and I'll check them while reading the crate again.

hero78119 · 2023-08-05T02:16:04Z

The comments above show as outdated because of the change in the directory name from zero_nova to nova, but you can still just answer them in the comments and I'll check them while reading the crate again.

Sure :) along with renaming crate to nova, I also rename few variables to make it self-explanation

leonardoalt · 2023-08-05T09:25:47Z

Impressive work @hero78119 ! I'm still going through the main parts of circuit_builder.rs, it's a lot to unpack, please bear with me :)

There's one thing that could make it easier for me and others to review/understand it: if it's not too much work, could you add a README in the Nova crate with a succinct explanation of how the constraint generation works, perhaps over a small example, like the test you added? Visualizing the source instructions/program and the generated constraints would help a lot in matching the behavior to the code. Thanks!

hero78119 · 2023-08-07T15:33:50Z

Impressive work @hero78119 ! I'm still going through the main parts of circuit_builder.rs, it's a lot to unpack, please bear with me :)

There's one thing that could make it easier for me and others to review/understand it: if it's not too much work, could you add a README in the Nova crate with a succinct explanation of how the constraint generation works, perhaps over a small example, like the test you added? Visualizing the source instructions/program and the generated constraints would help a lot in matching the behavior to the code. Thanks!

Hi @leonardoalt, an simple README is added in latest commit 9bce29f
Hopefully it can helpful a bit :)

hero78119 · 2023-08-08T14:42:29Z

Updated:

add README in Nova backend
utility to allocate constant defined in PIL in R1CS circuit.

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

hero78119 · 2023-08-09T16:02:07Z

Updated:

support signed constant in ROM value encoding (unsigned already support in prev commit)

Right now 3 major functionality are lefted

process public input
support label encoding
polyomial reference handling in constraints area (outside instruction body)

Following by another big topic

RW memory handling

After that, I think Nova backend will be preliminary ready as a folding backend in R1CS.

hero78119 · 2023-08-11T08:23:37Z

Updated:
All computation functionality should be supported now!

Pending Topic:

RW memory handling

Schaeff · 2023-08-18T15:39:54Z

Super cool stuff! I have yet to dig into the low level details but jugging from the high level my main thoughts now are:

Intermediate values in instruction circuits

You turn instruction blocks into R1CS. What would be your plan when it comes to introducing intermediate values? I'm thinking you could allow local declarations of committed polynomials:

instr not_0 X {
   pol commit XInv;
   XInv * X = 1;
}

This is abusing the semantics of PIL a bit, but it seems to me that it would work: if you consider a single row of the execution trace, each instruction circuit can "extend" the set of columns with more columns and have constraints between them on that same row.

I like that the implementation is self contained and doesn't change the powdr asm language. Are there however any changes on the powdr side which would make this nicer to work with?
It would be nice to have a list of tests, ranging from very simple (even empty) VMs to more advanced ones, as well as architectures which would not be supported now, with something like #[should_panic = "cause"]. They could then be fixed in the future.

I'll add more thoughts as I understand the internals better.

hero78119 · 2023-08-23T01:49:30Z

Hi~ sorry a bit late reply for being on vocation 😃

Super cool stuff! I have yet to dig into the low level details but jugging from the high level my main thoughts now are:

Intermediate values in instruction circuits

You turn instruction blocks into R1CS. What would be your plan when it comes to introducing intermediate values? I'm thinking you could allow local declarations of committed polynomials:
instr not_0 X {
   pol commit XInv;
   XInv * X = 1;
}
This is abusing the semantics of PIL a bit, but it seems to me that it would work: if you consider a single row of the execution trace, each instruction circuit can "extend" the set of columns with more columns and have constraints between them on that same row.

For current PR circuit parser design, extending intermediate variables defined in its respective instr block is well supported without need for any change. Each instruction is in respective isolated constraint system, so there is also free of variables naming confliction problem.

One nice features is, supporting inline features for pil parser, such that for Intermediate values either defined in instr or in constraints block, are able to flatten into single row instr_XXXX * (all the constraints here) then it will help a lot during circuit parsing. For now, intermediate variables define in constraints will be compiling into augment circuit no matter current instruction use them or not. If we can have inline mode in pil, then the circuit parser can deal with them efficiently.

I like that the implementation is self contained and doesn't change the powdr asm language. Are there however any changes on the powdr side which would make this nicer to work with?

I think one open question is powdr asm meta info => now for building Nova circuit, there are few meta info fetching from powdr asm
- list of instructions -> help to determine how many augment circuits.
- list of registers -> register name will be encoding into field when generating ROM, and later decoding from instruction itself
- instruction input/output params -> known param type sign/unsign/label/register so the respective circuit is generated.

=> we need a way to integrate them together with PIL language so we can fetch them from same place, or we find way to unify both infornation into a new structure data.

It would be nice to have a list of tests, ranging from very simple (even empty) VMs to more advanced ones, as well as architectures which would not be supported now, with something like #[should_panic = "cause"]. They could then be fixed in the future.

Yeah and good idea! I will do that sooner

I'll add more thoughts as I understand the internals better.

Appreciated if for further review :)

leonardoalt · 2023-09-04T09:59:55Z

I'm trying to run some tests with the Nova backend, and I ran into a panic.
The commands I'm running are:

# running this first to get the pil file out of the asm file
cargo run --release pil test_data/asm/simple_sum.asm -f -i "1,1,1" --field bn254

# then the nova backend
cargo run --release prove-nova simple_sum_opt.pil test_data/asm/simple_sum.asm -i "1,1,1"

Any ideas why?

hero78119 · 2023-09-04T13:26:38Z

I'm trying to run some tests with the Nova backend, and I ran into a panic. The commands I'm running are:
# running this first to get the pil file out of the asm file
cargo run --release pil test_data/asm/simple_sum.asm -f -i "1,1,1" --field bn254

# then the nova backend
cargo run --release prove-nova simple_sum_opt.pil test_data/asm/simple_sum.asm -i "1,1,1"
Any ideas why?

Hi, it's due to previously I assumed only support jump to the label ahead.
Updated in 27a5caa to have 2 pass rom compilation to support jump label behind.

Now with command

cargo run --release prove-nova simple_sum_opt.pil test_data/asm/simple_sum.asm -i "1,1,1"

it will run into new error

not implemented: BinaryOperation(PolynomialReference(PolynomialReference { namespace: None, name: "A", index: None, next: false }), Add, FreeInput(Tuple([String("input"), BinaryOperation(PolynomialReference(PolynomialReference { namespace: None, name: "CNT", index: None, next: false }), Add, Number(Bn254Field { value: BigInt([1, 0, 0, 0]) }))])))

This is expected for now, because with current folding per instruction design philosophy with SuperNova, it's hard to support syntax input retrieving with expression ${ ("input", Expression) }. This flexible powdr-asm syntax is not that friendly for Nova use case for now, because it hard to encode expressions to single field value as program ROM. Now only support is ${ ("input", Number) } use case, which I believe should support most of VM defined in powdr?

Understand there will be another scenario for Frontend program which will touch the dynamic input position via expression + variable. One workaround I can imagine is linker assembly stage convert it to memory load instruction. Then the prover input is also encode into memory commitment, then it will be work nicely in Nova use case

Appreciated if there is further suggestion :)

leonardoalt · 2023-11-15T13:01:06Z

I met IRL with @hero78119 and we had a discussion about this PR, I understand how it works now! It's really neat.
It still doesn't support things like parametric instructions and expressions as arguments, so we decided to keep the PR open as a draft until support for those things is added so that it works for RISCV.

add some nova experiments

27997aa

hero78119 marked this pull request as draft July 31, 2023 13:18

hero78119 changed the title ~~[Draft] Nova backend in supernova R1CS~~ [Draft] Nova backend in Supernova R1CS Jul 31, 2023

hero78119 force-pushed the nova branch from dcf1417 to e7268e8 Compare August 2, 2023 15:34

leonardoalt reviewed Aug 4, 2023

View reviewed changes

hero78119 force-pushed the nova branch 2 times, most recently from 3af4c2f to 7bea53f Compare August 5, 2023 03:01

hero78119 force-pushed the nova branch 3 times, most recently from a35c65a to a3078ae Compare August 8, 2023 14:40

hero78119 force-pushed the nova branch from 34ef7d9 to 64f6fdf Compare August 8, 2023 15:16

hero78119 marked this pull request as ready for review August 9, 2023 15:54

hero78119 changed the title ~~[Draft] Nova backend in Supernova R1CS~~ Nova backend in Supernova R1CS Aug 9, 2023

nova support signed constant ROM encoding

2ace790

hero78119 force-pushed the nova branch from a197102 to 2ace790 Compare August 9, 2023 16:05

hero78119 added 2 commits August 10, 2023 16:44

fix soundness related to const allocation

03fe3d6

clippy fix

3145872

hero78119 added 3 commits August 11, 2023 12:09

nova support read from public io

495aede

nova support evaluate shared constraints

9f03bc7

nova support label functionality

8d639ad

hero78119 force-pushed the nova branch from 3354f88 to 8d639ad Compare August 11, 2023 08:21

hero78119 mentioned this pull request Aug 17, 2023

supernova implementation with naive opcode commitment for argumented circuit sequence. microsoft/Nova#204

Closed

update dependency to use bellpepper-core, aligned with nova

976c329

compile rom in 2 pass to support jump to the labels behind

27a5caa

leonardoalt marked this pull request as draft November 15, 2023 13:01

leonardoalt deleted the branch powdr-labs:nova January 15, 2024 11:14

leonardoalt closed this Jan 15, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Nova backend in Supernova R1CS #453

Nova backend in Supernova R1CS #453

hero78119 commented Jul 31, 2023 •

edited

hero78119 commented Aug 2, 2023 •

edited

leonardoalt commented Aug 3, 2023

hero78119 commented Aug 3, 2023 •

edited

leonardoalt commented Aug 4, 2023

leonardoalt left a comment

leonardoalt Aug 4, 2023

hero78119 Aug 4, 2023 •

edited

leonardoalt Aug 4, 2023

hero78119 Aug 8, 2023 •

edited

leonardoalt Aug 4, 2023

leonardoalt Aug 4, 2023

hero78119 commented Aug 4, 2023 •

edited

leonardoalt left a comment

leonardoalt Aug 4, 2023

hero78119 Aug 5, 2023 •

edited

leonardoalt Aug 5, 2023

leonardoalt commented Aug 4, 2023

hero78119 commented Aug 5, 2023

leonardoalt commented Aug 5, 2023

hero78119 commented Aug 7, 2023 •

edited

hero78119 commented Aug 8, 2023 •

edited

hero78119 commented Aug 9, 2023 •

edited

hero78119 commented Aug 11, 2023

Schaeff commented Aug 18, 2023

hero78119 commented Aug 23, 2023

leonardoalt commented Sep 4, 2023 •

edited

hero78119 commented Sep 4, 2023 •

edited

leonardoalt commented Nov 15, 2023

Nova backend in Supernova R1CS #453

Nova backend in Supernova R1CS #453

Conversation

hero78119 commented Jul 31, 2023 • edited

Step to run

Spotted Issues

hero78119 commented Aug 2, 2023 • edited

leonardoalt commented Aug 3, 2023

hero78119 commented Aug 3, 2023 • edited

leonardoalt commented Aug 4, 2023

leonardoalt left a comment

Choose a reason for hiding this comment

leonardoalt Aug 4, 2023

Choose a reason for hiding this comment

hero78119 Aug 4, 2023 • edited

Choose a reason for hiding this comment

leonardoalt Aug 4, 2023

Choose a reason for hiding this comment

hero78119 Aug 8, 2023 • edited

Choose a reason for hiding this comment

leonardoalt Aug 4, 2023

Choose a reason for hiding this comment

leonardoalt Aug 4, 2023

Choose a reason for hiding this comment

hero78119 commented Aug 4, 2023 • edited

leonardoalt left a comment

Choose a reason for hiding this comment

leonardoalt Aug 4, 2023

Choose a reason for hiding this comment

hero78119 Aug 5, 2023 • edited

Choose a reason for hiding this comment

leonardoalt Aug 5, 2023

Choose a reason for hiding this comment

leonardoalt commented Aug 4, 2023

hero78119 commented Aug 5, 2023

leonardoalt commented Aug 5, 2023

hero78119 commented Aug 7, 2023 • edited

hero78119 commented Aug 8, 2023 • edited

hero78119 commented Aug 9, 2023 • edited

hero78119 commented Aug 11, 2023

Schaeff commented Aug 18, 2023

hero78119 commented Aug 23, 2023

leonardoalt commented Sep 4, 2023 • edited

hero78119 commented Sep 4, 2023 • edited

leonardoalt commented Nov 15, 2023

hero78119 commented Jul 31, 2023 •

edited

hero78119 commented Aug 2, 2023 •

edited

hero78119 commented Aug 3, 2023 •

edited

hero78119 Aug 4, 2023 •

edited

hero78119 Aug 8, 2023 •

edited

hero78119 commented Aug 4, 2023 •

edited

hero78119 Aug 5, 2023 •

edited

hero78119 commented Aug 7, 2023 •

edited

hero78119 commented Aug 8, 2023 •

edited

hero78119 commented Aug 9, 2023 •

edited

leonardoalt commented Sep 4, 2023 •

edited

hero78119 commented Sep 4, 2023 •

edited