RISCV - integrate zkc pipeline into prover #3132
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -2,6 +2,7 @@ package zkcdriver | |
|
|
||
| import ( | ||
| "fmt" | ||
| "log" | ||
| "sort" | ||
|
|
||
| "github.com/consensys/linea-monorepo/prover-ray/maths/koalabear/field" | ||
|
|
@@ -64,17 +65,62 @@ func (s *schemaScanner) scanColumns() { | |
| // Use the pre-sorted modules from the scanner to ensure deterministic ordering | ||
| // Iterate each declared module | ||
| for _, modDecl := range s.Modules { | ||
| // Check for special cases | ||
| if modDecl.IsStatic() { | ||
|
|
||
| content := modDecl.StaticContents() | ||
| moduleName := modDecl.Name().String() | ||
| moduleWIOP := s.Sys.NewSizedModule( | ||
| s.Sys.Context.Childf("module-%v", moduleName), | ||
| len(content), | ||
| wiop.PaddingDirectionLeft, | ||
|
AlexandreBelling marked this conversation as resolved.
|
||
| ) | ||
|
|
||
| // This works assuming the [System] appends-only to the list of modules. | ||
| s.ModulesIDsWiop[moduleName] = len(s.Sys.Modules) - 1 | ||
|
|
||
| for i, colDecl := range modDecl.Registers() { | ||
|
|
||
| vec := make([]field.Element, len(content)) | ||
| for j := range content { | ||
| vec[j] = field.Element(content[j][i]) | ||
| } | ||
|
|
||
| var ( | ||
| colName = colDecl.Name() | ||
| colQualifiedName = qualifiedCorsetName(moduleName, colName) | ||
| col = moduleWIOP.NewPrecomputedColumn( | ||
| moduleWIOP.Context.Childf("column-%v", colName), | ||
| wiop.VisibilityOracle, | ||
| &wiop.ConcreteVector{Plain: field.VecFromBase(vec)}, | ||
| ) | ||
| ) | ||
|
|
||
| s.ColumnIDs[colQualifiedName] = col.Context.ID | ||
| } | ||
|
|
||
|
cursor[bot] marked this conversation as resolved.
|
||
| continue | ||
| } | ||
|
|
||
| if modDecl.IsNative() { | ||
|
Contributor
Author
There was a problem hiding this comment. @ivokub @YaoJGalteland @Tabaie @arijitdutta67 This is meant to serve as entrypoint for the implementation of the precompiles, when they get added |
||
| // @david: need to add support for native modules. These correspond | ||
| // to ZkC functions declared with the "native" attribute". The | ||
| // expectation is that the prover will maintain a list of supported | ||
| // native modules. Each of these will have an expected number of | ||
| // columns (which the prover may wish to check matches the | ||
| // declaration here). These columns correspond to the input/output | ||
| // registers of the corresponding ZkC function. | ||
| // | ||
| // A key aspect of native modules is that ZkC will not generate any | ||
| // constraints for them. Instead, the expectation is that whatever | ||
| // constraints are required will be added somehow / somewhere by the | ||
| // prover. Since forgetting to do this is a critical soundness | ||
| // issue, care must be taken to ensure it really happens (e.g. | ||
| // through testing negative cases which should cause constraint | ||
| // failures). | ||
| log.Panic("zkcdriver: add support for native modules!") | ||
|
cursor[bot] marked this conversation as resolved.
Outdated
|
||
| } | ||
|
|
||
| // moduleName is the name of the module as given by the arithmetization | ||
| moduleName := modDecl.Name().String() | ||
| moduleWIOP := s.Sys.NewDynamicModule( | ||
|
|
@@ -243,12 +289,26 @@ func (s *schemaScanner) addConstraintInComp(name string, corsetCS schema.Constra | |
| module.NewVanishing(module.Context.Childf("local-%v", name), wExpr) | ||
|
|
||
| case air.RangeConstraint[koalabear.Element]: | ||
|
|
||
| rc := cs.Unwrap() | ||
|
|
||
| // Sanity check: If a RangeConstraint ever has more than one source/bitwidth, the second iteration will panic | ||
| // because the first iteration already registered that QueryID in the CompiledIOP. In practice | ||
| // the len is always expected to be either 0 (no-op) or 1 (single pass). | ||
| if len(rc.Bitwidths) > 1 { | ||
| utils.Panic("multiple bitwidths for range constraints not supported") | ||
| } | ||
|
|
||
| for i, bitwidth := range rc.Bitwidths { | ||
| // Determine bound for this range constraint | ||
| bound := 1 << bitwidth | ||
| col := s.compColumnByCorsetID(rc.Context, rc.Sources[i].Register()) | ||
| col.Module.NewRangeCheck(col.Context.Childf("range-%v", name), col, bound) | ||
| } | ||
|
|
||
| case air.Assertion[koalabear.Element]: | ||
| // Property assertions can be ignored, as they are a debugging tool and | ||
| // not part of the constraints proper. | ||
|
|
||
| default: | ||
| utils.Panic("unexpected constraint type: %s", cs.Lisp(s.Schema).String(false)) | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,78 @@ | ||
| package zkcdriver_test | ||
|
|
||
| import ( | ||
| "fmt" | ||
| "testing" | ||
|
|
||
| zkc_util "github.com/consensys/go-corset/pkg/zkc/util" | ||
| "github.com/consensys/linea-monorepo/prover-ray/utils/files" | ||
| "github.com/consensys/linea-monorepo/prover-ray/wiop" | ||
| "github.com/consensys/linea-monorepo/prover-ray/zkcdriver" | ||
| ) | ||
|
|
||
| func TestZkc_01a(t *testing.T) { | ||
| runTest(t, "zkc_01", "{\"data\": \"0x0000_0001\" }") | ||
| } | ||
|
|
||
| func TestZkc_01b(t *testing.T) { | ||
| runTest(t, "zkc_01", "{\"data\": \"0x0041_0042\" }") | ||
| } | ||
|
|
||
| func TestZkc_02a(t *testing.T) { | ||
| runTest(t, "zkc_02", "{\"data\": \"0x0003_0008\" }") | ||
| } | ||
|
|
||
| func TestZkc_02b(t *testing.T) { | ||
| runTest(t, "zkc_02", "{\"data\": \"0x000f_8000\" }") | ||
| } | ||
|
|
||
| // nolint | ||
| func runTest(t *testing.T, test, input string) { | ||
| sys := wiop.NewSystemf("zkc-test") | ||
| // set an example input | ||
| var ( | ||
| testfile = fmt.Sprintf("./testdata/%s.bin", test) | ||
| // construct inputs map | ||
| inputs zkcdriver.PreReadInputs | ||
| ) | ||
| // parse example input | ||
| inputs.Inputs, inputs.Err = zkc_util.ParseJsonInputFile([]byte(input)) | ||
| // Sanity check | ||
| if inputs.Err != nil { | ||
| t.Errorf("error parsing program inputs (%v)", inputs.Err) | ||
| t.FailNow() | ||
| } | ||
| // initialise round | ||
| sys.NewRound() | ||
| // construct ZkC driver | ||
| driver := zkcdriver.NewZkCDriver( | ||
| sys, | ||
| zkcdriver.Settings{}, | ||
| files.MustRead(testfile)) | ||
| rt := wiop.NewRuntime(sys) | ||
| driver.AssignWithPreRead(&rt, inputs) | ||
| // FIXME: run the prover to complete the test. For now, I just used | ||
|
AlexandreBelling marked this conversation as resolved.
Contributor
There was a problem hiding this comment. You still have a |
||
| // go-corset's internal check to illustrate how this can work (e.g. it might | ||
| // be useful for debugging). Run go-corset constraint check | ||
| runZkcConstraintCheck(t, driver, inputs.Inputs) | ||
| } | ||
|
|
||
| func runZkcConstraintCheck(t *testing.T, driver *zkcdriver.ZkCDriver, input map[string][]byte) { | ||
| t.Helper() | ||
| // trace program with given input | ||
| tr, errs := driver.BinaryFile.Trace(input, driver.TracingConfig) | ||
| // sanity check | ||
| if len(errs) > 0 { | ||
| for _, err := range errs { | ||
| t.Errorf("%s", err.Error()) | ||
| } | ||
| t.FailNow() | ||
| } | ||
| // | ||
| if errs := driver.BinaryFile.Check(tr, driver.TracingConfig); len(errs) > 0 { | ||
| for _, err := range errs { | ||
| t.Errorf("%s", err.Message()) | ||
| } | ||
| t.FailNow() | ||
| } | ||
| } | ||
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.