diff --git a/prover-ray/go.mod b/prover-ray/go.mod index 83c5c406a3f..2d42324c441 100644 --- a/prover-ray/go.mod +++ b/prover-ray/go.mod @@ -5,7 +5,7 @@ go 1.25.7 require ( github.com/consensys/gnark v0.14.1-0.20260219004710-bbfb2f70a565 github.com/consensys/gnark-crypto v0.20.2-0.20260514182922-df0578435b08 - github.com/consensys/go-corset v1.2.10 + github.com/consensys/go-corset v1.2.17 github.com/go-playground/assert/v2 v2.2.0 github.com/sirupsen/logrus v1.9.4 github.com/stretchr/testify v1.11.1 diff --git a/prover-ray/go.sum b/prover-ray/go.sum index 9a7849aaf0b..bb539199493 100644 --- a/prover-ray/go.sum +++ b/prover-ray/go.sum @@ -15,8 +15,8 @@ github.com/consensys/gnark v0.14.1-0.20260219004710-bbfb2f70a565 h1:NlOAmbLYsVb/ github.com/consensys/gnark v0.14.1-0.20260219004710-bbfb2f70a565/go.mod h1:EoWWbEboQRydCqJDSA7zrFxucIeoy/5R+MDx04oFpF4= github.com/consensys/gnark-crypto v0.20.2-0.20260514182922-df0578435b08 h1:EdljQKaHxACX5JMSTXlVM9R8qASU/W1husqDsB2b5tU= github.com/consensys/gnark-crypto v0.20.2-0.20260514182922-df0578435b08/go.mod h1:NzeBHSZ49bIM7RtrNTYYR2kymTqwvI/A4eTgQlyQc+Q= -github.com/consensys/go-corset v1.2.10 h1:uKUICiHmERuMWzDRiRJr285fV2WncNGiCENSdNcQodY= -github.com/consensys/go-corset v1.2.10/go.mod h1:QKFoNJZHdCrDslg9XFjk+GoFMgrhKSVdBNnx4hq7WJA= +github.com/consensys/go-corset v1.2.17 h1:zy30Snj1JTQePoBzk8vEkAXUE1i7p0AdNHGxWwbdkC4= +github.com/consensys/go-corset v1.2.17/go.mod h1:QKFoNJZHdCrDslg9XFjk+GoFMgrhKSVdBNnx4hq7WJA= github.com/creack/pty v1.1.9/go.mod h1:oKZEueFk5CKHvIhNR5MUki03XCEU+Q6VDXinZuGJ33E= github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= github.com/davecgh/go-spew v1.1.1/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= diff --git a/prover-ray/wiop/wiop_column.go b/prover-ray/wiop/wiop_column.go index 5d40052ccce..9b377a11a3f 100644 --- a/prover-ray/wiop/wiop_column.go +++ b/prover-ray/wiop/wiop_column.go @@ -172,6 +172,9 @@ func (m *Module) NewPrecomputedColumn(ctx *ContextFrame, vis Visibility, assignm if ctx.ID != 0 { panic(fmt.Sprintf("wiop: ContextFrame %q is already registered (id=%d)", ctx.Path(), ctx.ID)) } + if assignment.promise != nil { + panic("wiop: Module.NewPrecomputedColumn requires a non-promised assignment") + } ctx.ID = newColumnID(m.index, len(m.Columns)) pr := m.system.PrecomputedRound col := &Column{ @@ -182,6 +185,7 @@ func (m *Module) NewPrecomputedColumn(ctx *ContextFrame, vis Visibility, assignm Module: m, round: &pr.Round, } + assignment.promise = col.View() m.Columns = append(m.Columns, col) pr.addPrecomputedColumn(col, assignment) return col diff --git a/prover-ray/zkcdriver/assignment.go b/prover-ray/zkcdriver/assignment.go index 82256e26b50..00c7354a452 100644 --- a/prover-ray/zkcdriver/assignment.go +++ b/prover-ray/zkcdriver/assignment.go @@ -3,6 +3,7 @@ package zkcdriver import ( "unsafe" + "github.com/consensys/go-corset/pkg/ir/air" "github.com/consensys/go-corset/pkg/trace" "github.com/consensys/go-corset/pkg/util/field/koalabear" "github.com/consensys/linea-monorepo/prover-ray/maths/koalabear/field" @@ -19,14 +20,23 @@ var _ [1]uint32 = field.Element{} // ReadExpandedTraces parses the provided trace file, expands it and returns the // corset object holding the expanded traces. -func AssignFromLtTraces(run *wiop.Runtime, expTraces trace.Trace[koalabear.Element]) { +func AssignFromTrace(run *wiop.Runtime, traces trace.Trace[koalabear.Element], schema air.Schema[koalabear.Element]) { // Parallelize across modules eg := &errgroup.Group{} - for modID := range expTraces.Width() { + for modID := range traces.Width() { eg.Go(func() error { - trMod := expTraces.Module(modID) + trMod := traces.Module(modID) + scMod := schema.Module(modID) + + if scMod.IsStatic() { + // @alex: the current version of corset flags modules as being + // static or not static. But it may be the case, that a module + // has static size, some its column have static content but some + // do not have static content. + return nil + } // Iterate each column in module parallel.Execute(int(trMod.Width()), func(start, stop int) { @@ -41,7 +51,7 @@ func AssignFromLtTraces(run *wiop.Runtime, expTraces trace.Trace[koalabear.Eleme ) if _, ok := columnIDMap[name]; !ok { - logrus.Debugf("zkcdriver: AssignFromLtTraces: skipping unknown column %q", name) + logrus.Debugf("zkcdriver: AssignFromTrace: skipping unknown column %q", name) continue } @@ -74,6 +84,6 @@ func AssignFromLtTraces(run *wiop.Runtime, expTraces trace.Trace[koalabear.Eleme }) } if err := eg.Wait(); err != nil { - logrus.Panicf("AssignFromLtTraces failed: %v", err) + logrus.Panicf("zkcdriver: AssignFromTrace failed: %v", err) } } diff --git a/prover-ray/zkcdriver/definition.go b/prover-ray/zkcdriver/definition.go index df6870aa645..bb52d66c556 100644 --- a/prover-ray/zkcdriver/definition.go +++ b/prover-ray/zkcdriver/definition.go @@ -6,6 +6,7 @@ import ( "github.com/consensys/linea-monorepo/prover-ray/maths/koalabear/field" "github.com/consensys/linea-monorepo/prover-ray/wiop" + "github.com/sirupsen/logrus" "github.com/consensys/go-corset/pkg/ir/air" "github.com/consensys/go-corset/pkg/schema" @@ -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, + ) + + // 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)}, + ) + ) - // The "root" module is part of the if the list of the modules. It - // expectedly does not contains any column. We need to skip it because - // we would not be able to find its name. - if modDecl.Name().String() == "" { - if modDecl.Width() != 0 { - utils.Panic("found a module with no names but with columns") + s.ColumnIDs[colQualifiedName] = col.Context.ID } + continue } + if modDecl.IsNative() { + // @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). + logrus.Panic("zkcdriver: add support for native modules!") + } + // 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]: - utils.Panic("RangeConstraint is not yet supported (constraint: %s)", name) + + 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. - case air.InterleavingConstraint[koalabear.Element]: - panic("to be removed once corset, removes it. We will never support this.") default: utils.Panic("unexpected constraint type: %s", cs.Lisp(s.Schema).String(false)) diff --git a/prover-ray/zkcdriver/definition_test.go b/prover-ray/zkcdriver/definition_test.go deleted file mode 100644 index aef3e4758bd..00000000000 --- a/prover-ray/zkcdriver/definition_test.go +++ /dev/null @@ -1,24 +0,0 @@ -package zkcdriver_test - -import ( - "testing" - - "github.com/consensys/go-corset/pkg/ir/mir" - "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 TestZkEVMDefinition(t *testing.T) { - // @alex: I checked that it worked with Ranges and Interleavings. I will - // leave it as skipped for now but we will need to eventually. - t.Skipf("you will need to relax the non-support for range-checks in ray") - - sys := wiop.NewSystemf("zkevm-test") - sys.NewRound() - _ = zkcdriver.NewZkCDriver( - sys, - zkcdriver.Settings{OptimisationLevel: &mir.DEFAULT_OPTIMISATION_LEVEL}, - files.MustRead("./testdata/zkevm.bin"), - ) -} diff --git a/prover-ray/zkcdriver/example_test.go b/prover-ray/zkcdriver/example_test.go new file mode 100644 index 00000000000..9c8a9a1d893 --- /dev/null +++ b/prover-ray/zkcdriver/example_test.go @@ -0,0 +1,83 @@ +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/wiop/wioptest" + "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) + + if err := wioptest.RunAndVerify(&rt); err != nil { + t.Fatalf("error running verifier: %v", err) + } + // FIXME: run the prover to complete the test. For now, I just used + // 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() + } +} diff --git a/prover-ray/zkcdriver/files.go b/prover-ray/zkcdriver/files.go index 3a20ea71c09..4eace149f9c 100644 --- a/prover-ray/zkcdriver/files.go +++ b/prover-ray/zkcdriver/files.go @@ -3,101 +3,56 @@ package zkcdriver import ( "compress/gzip" _ "embed" - "encoding/gob" "errors" "fmt" "io" "os" "strings" - "github.com/consensys/go-corset/pkg/asm" - "github.com/consensys/go-corset/pkg/binfile" - "github.com/consensys/go-corset/pkg/corset" - "github.com/consensys/go-corset/pkg/ir/air" - "github.com/consensys/go-corset/pkg/ir/mir" - "github.com/consensys/go-corset/pkg/schema/module" - "github.com/consensys/go-corset/pkg/trace/lt" "github.com/consensys/go-corset/pkg/util/collection/typed" - "github.com/consensys/go-corset/pkg/util/field" - "github.com/consensys/go-corset/pkg/util/field/koalabear" + zkc_util "github.com/consensys/go-corset/pkg/zkc/util" "github.com/sirupsen/logrus" ) -// UnmarshalZkEVMBin parses and compiles a "zkevm.bin" buffered file into a -// BinaryFile. This additionally extracts the metadata map from the zkevm.bin -// file. This contains information which can be used to cross-check the -// zkevm.bin file, such as the git commit of the enclosing repository when it -// was built. -func ReadZkevmBin(r io.Reader) (*binfile.BinaryFile, typed.Map, error) { +// ReadConstraintsFile reads in a binary representation of the constraints to be +// used for creating proofs. This additionally extracts the metadata map from +// the binary file. This contains information which can be used to cross-check +// the constraints file (e.g. the git commit of the enclosing repository when it +// was built). +func ReadConstraintsFile(r io.Reader) (*BinaryFile, typed.Map, error) { buf, err := io.ReadAll(r) if err != nil { return nil, typed.Map{}, fmt.Errorf("io.ReadAll failed to read zkevm.bin: %w", err) } - return UnmarshalZkEVMBin(buf) + return UnmarshalConstraintsFile(buf) } -// UnmarshalZkEVMBin parses and compiles a "zkevm.bin" buffered file into a -// BinaryFile. This additionally extracts the metadata map from the zkevm.bin -// file. This contains information which can be used to cross-check the -// zkevm.bin file, such as the git commit of the enclosing repository when it -// was built. -func UnmarshalZkEVMBin(buf []byte) (*binfile.BinaryFile, typed.Map, error) { +// UnmarshalConstraintsFile parses a binary constraints file (e.g. blake.bin) +// into a BinaryFile instance. This additionally extracts the metadata map from +// the binary file. This contains information which can be used to cross-check +// the constraints file (e.g. the git commit of the enclosing repository when it +// was built). +func UnmarshalConstraintsFile(buf []byte) (*BinaryFile, typed.Map, error) { var ( - binf binfile.BinaryFile + binf BinaryFile metadata typed.Map ) - // - gob.Register(binfile.Attribute(&corset.SourceMap{})) // Parse zkbinary file err := binf.UnmarshalBinary(buf) // Sanity check for errors if err != nil { - return nil, metadata, fmt.Errorf("could not parse the read bytes of the 'zkevm.bin' file into a schema: %w", err) + return nil, metadata, fmt.Errorf("failed parsing binary constraints file: %w", err) } - // Attempt to extract metadata from bin file, and sanity check constraints - // commit information is available. - if metadata, err = binf.Header.GetMetaData(); metadata.IsEmpty() { - return nil, metadata, errors.New("missing metatdata from 'zkevm.bin' file") + // extract file header (which contains versioning info + metadata) + header := binf.Header() + // Check metadata in binary constraints file is valid + if metadata, err = header.GetMetaData(); err != nil { + return nil, metadata, errors.New("corrupt metatdata in binary constraints file") } // Done return &binf, metadata, err } -// Compile a "zkevm.bin" BinaryFile into an air.Schema, whilst applying whatever -// optimisations are requested. This also produces a "limb mapping" which -// determines how to map columns from the trace file into columns in the -// expanded trace. -// -// NOTE: optimisations can impact the size of the generated schema -// and, consequently, the size of the expanded trace. For example, certain -// optimisations eliminate unnecessary columns creates for multiplicative -// inverses. However, optimisations do not always improve overall performance, -// as they can increase the complexity of other constraints. The -// DEFAULT_OPTIMISATION_LEVEL is the recommended level to use in general, whilst -// others are intended for testing purposes (i.e. to try out new optimisations -// to see whether they help or hinder, etc). -func CompileZkevmBin( - binf *binfile.BinaryFile, - optConfig *mir.OptimisationConfig, -) ( - *air.Schema[koalabear.Element], - module.LimbsMap, -) { - // There are no useful choices for the assembly config. We must always - // vectorize, and there is only one choice of field (within the prover). - asmConfig := asm.LoweringConfig{Field: field.KOALABEAR_16, Vectorize: true} - // Lower to mixed micro schema - uasmSchema := asm.LowerMixedMacroProgram(asmConfig.Vectorize, binf.Schema) - // Apply register splitting for field agnosticity - nasmSchema, mapping := asm.Concretize[koalabear.Element](asmConfig.Field, uasmSchema) - // Compile - mirSchema := asm.Compile(nasmSchema) - // Lower to AIR - airSchema := mir.LowerToAir(mirSchema, 30, *optConfig) - // This performs the corset compilation - return &airSchema, mapping -} - type readCloserChain struct { io.Reader closers []io.Closer @@ -113,23 +68,20 @@ func (r *readCloserChain) Close() error { return firstErr } -// readTraceFile returns a reader over the trace data. -// If the file ends with .gz, it transparently decompresses it. -// The caller (See ReadLtTraces below) MUST close the returned io.ReadCloser. -func readTraceFile(path string) (io.ReadCloser, error) { - +// ReadMaybeCompressedFile returns a reader over the zkc input data. If the file +// ends with .gz, it transparently decompresses it. The caller (See ReadLtTraces +// below) MUST close the returned io.ReadCloser. +func ReadMaybeCompressedFile(path string) (io.ReadCloser, error) { f, err := os.Open(path) if err != nil { if os.IsNotExist(err) { - err = fmt.Errorf("missing trace file, at %v : %w", path, err) + err = fmt.Errorf("missing zkc inputs file, at %v : %w", path, err) } else { - err = fmt.Errorf("unable to open trace file %q: %w", path, err) + err = fmt.Errorf("unable to open zkc inputs file %q: %w", path, err) } return nil, err - } - - if !strings.HasSuffix(path, ".gz") { + } else if !strings.HasSuffix(path, ".gz") { return f, nil } @@ -151,32 +103,18 @@ func readTraceFile(path string) (io.ReadCloser, error) { return rc, nil } -// ReadLtTraces reads a given LT trace file which contains (unexpanded) column -// data, and additionally extracts the metadata map from the zkevm.bin file. The -// metadata contains information which can be used to cross-check the zkevm.bin -// file, such as the git commit of the enclosing repository when it was built. -func ReadLtTraces(f io.ReadCloser) (rawTrace lt.TraceFile, metadata typed.Map, err error) { - var ( - traceFile lt.TraceFile - ok bool - ) +// ReadZkcInputFile reads a given JSON inputs file which contains byte strings +// (e.g. in hex) for each input memory declared in the ZkC program. +func ReadZkcInputFile(f io.ReadCloser) (inputs map[string][]byte, err error) { defer f.Close() // Read the trace file, including any metadata embedded within. readBytes, err := io.ReadAll(f) if err != nil { - return traceFile, metadata, fmt.Errorf("failed reading the file: %w", err) - } else if err = traceFile.UnmarshalBinary(readBytes); err != nil { - return traceFile, metadata, fmt.Errorf("failed parsing the bytes of the raw trace '.lt' file: %w", err) - } - // Extract trace file header - header := traceFile.Header() - // Attempt to extract metadata from trace file, and sanity check the - // constraints commit information is present. - if metadata, err = header.GetMetaData(); metadata.IsEmpty() { - return traceFile, metadata, errors.New("missing metatdata from '.lt' file") - } else if metadata, ok = metadata.Map("constraints"); !ok { - return traceFile, metadata, errors.New("missing constraints metatdata from '.lt' file") + return inputs, fmt.Errorf("failed reading the file: %w", err) + } else if inputs, err = zkc_util.ParseJsonInputFile(readBytes); err != nil { + // wrap parser error with something more useful. + return inputs, fmt.Errorf("failed parsing zkc input file: %w", err) } - // Done - return traceFile, metadata, nil + // + return inputs, nil } diff --git a/prover-ray/zkcdriver/testdata/zkc_01.bin b/prover-ray/zkcdriver/testdata/zkc_01.bin new file mode 100644 index 00000000000..05055fe1ec2 Binary files /dev/null and b/prover-ray/zkcdriver/testdata/zkc_01.bin differ diff --git a/prover-ray/zkcdriver/testdata/zkc_01.zkc b/prover-ray/zkcdriver/testdata/zkc_01.zkc new file mode 100644 index 00000000000..3da1df8a284 --- /dev/null +++ b/prover-ray/zkcdriver/testdata/zkc_01.zkc @@ -0,0 +1,15 @@ +pub input data(address:u16) -> (byte:u16) + +// prove that two numbers add up to a third. +fn main() { + var lhs:u16 = data[0] + var res:u16 = data[1] + + lhs = lhs + 1 + + if lhs != res { + fail + } + + return +} diff --git a/prover-ray/zkcdriver/testdata/zkc_02.bin b/prover-ray/zkcdriver/testdata/zkc_02.bin new file mode 100644 index 00000000000..2f3547b8f27 Binary files /dev/null and b/prover-ray/zkcdriver/testdata/zkc_02.bin differ diff --git a/prover-ray/zkcdriver/testdata/zkc_02.zkc b/prover-ray/zkcdriver/testdata/zkc_02.zkc new file mode 100644 index 00000000000..39a55f96fe5 --- /dev/null +++ b/prover-ray/zkcdriver/testdata/zkc_02.zkc @@ -0,0 +1,18 @@ +pub input data(address:u16) -> (byte:u16) + +// prove that two numbers add up to a third. +fn main() { + var n:u16 = data[0] + var r:u16 = data[1] + var i:u16 = 0 + var v:u16 = 1 + // + while i != n { + v = v + v + i = i + 1 + } + // + if v != r { + fail + } +} diff --git a/prover-ray/zkcdriver/testdata/zkevm.bin b/prover-ray/zkcdriver/testdata/zkevm.bin deleted file mode 100644 index fd6282d12f1..00000000000 Binary files a/prover-ray/zkcdriver/testdata/zkevm.bin and /dev/null differ diff --git a/prover-ray/zkcdriver/zkcdriver.go b/prover-ray/zkcdriver/zkcdriver.go index 77889263902..cb12c0dd958 100644 --- a/prover-ray/zkcdriver/zkcdriver.go +++ b/prover-ray/zkcdriver/zkcdriver.go @@ -2,55 +2,44 @@ package zkcdriver import ( "errors" - "fmt" "io" "time" - "github.com/consensys/go-corset/pkg/asm" - "github.com/consensys/go-corset/pkg/binfile" - "github.com/consensys/go-corset/pkg/ir" - "github.com/consensys/go-corset/pkg/ir/air" - "github.com/consensys/go-corset/pkg/ir/mir" - "github.com/consensys/go-corset/pkg/schema/module" - "github.com/consensys/go-corset/pkg/trace/lt" "github.com/consensys/go-corset/pkg/util/collection/typed" "github.com/consensys/go-corset/pkg/util/field/koalabear" + "github.com/consensys/go-corset/pkg/zkc/constraints" "github.com/consensys/linea-monorepo/prover-ray/wiop" "github.com/sirupsen/logrus" ) -// Settings specifies the parameters for the arithmetization part of the zkEVM. +// BinaryFile represents a given set of constraints generated from a ZkC +// program. A BinaryFile is typically obtained by decoding an array of bytes, +// though it can also be obtained by compiling a given set of ZkC source files. +// A BinaryFile provides two key pieces of functionality: firstly, it provides +// access to the AIR constraints representing the given ZkC program; secondly, +// it provides a means to generate a trace of that program from a given set of +// inputs. +type BinaryFile = constraints.BinaryFile[koalabear.Element] + +// Settings specifies the parameters for the arithmetization (a.k.a. the +// "constraints"). type Settings struct { - // IgnoreCompatibilityCheck disables the strong compatibility check. - // Specifically, it does not require the constraints and the trace file to - // have both originated from the same commit. By default, the compatibility - // check should be enabled. - IgnoreCompatibilityCheck bool - // OptimisationLevel determines the optimisation level which go-corset will - // apply when compiling the zkevm.bin file to AIR constraints. If in doubt, - // use mir.DEFAULT_OPTIMISATION_LEVEL. - OptimisationLevel *mir.OptimisationConfig } -// ZkCDriver exposes all the methods relevant for the user to interact -// with the arithmetization of the zkEVM. It is a sub-component of the whole -// ZkEvm object as it does not includes the precompiles, the keccaks and the -// signature verification. +// ZkCDriver exposes all the methods relevant for the user to interact with the +// constraints being used for proving. This includes all constraints arising +// from the target ZkC program, but it does not include any native circuits +// (e.g. for precompiles, or accelerators, etc). type ZkCDriver struct { Settings *Settings - // Binary encoding of the zkevm.bin file, which captures the high-level - // structure of constraints. This is primarily useful for assembly - // functions (as these have big differences between their assembly - // representation and their constraints representation). - BinaryFile *binfile.BinaryFile `serde:"omit"` - // Air schema defines the low-level columns, constraints and computations - // used to expand a given trace, and to subsequently to check - // satisfiability. - AirSchema *air.Schema[koalabear.Element] `serde:"omit"` - // Maps each column in the raw trace file into one (or more) columns in the - // expanded trace file. In particular, columns which are too large for the - // given field are split into multiple "limbs". - LimbMapping module.LimbsMap `serde:"omit"` + // Binary constraints file generated from a ZkC program. This includes the + // raw arithmetic (AIR) constraints generated from the program, as well as + // functionality for tracing the program from a given set of inputs. + BinaryFile *BinaryFile `serde:"omit"` + // Configuration options for tracing (e.g. whether or not to use + // parallelisation, what batch size to use, etc). Generally speaking this + // should be left to the provided defaults. + TracingConfig constraints.TraceConfig `serde:"omit"` // Metadata embedded in the zkevm.bin file, as needed to check // compatibility. Guaranteed non-nil. Metadata typed.Map `serde:"omit"` @@ -61,22 +50,20 @@ type ZkCDriver struct { func NewZkCDriver(sys *wiop.System, settings Settings, bin io.Reader) *ZkCDriver { // Read and parse the binary file - binf, metadata, errS := ReadZkevmBin(bin) + binf, metadata, errS := ReadConstraintsFile(bin) if errS != nil { panic(errS) } - - // Compile binary file into an air.Schema - schema, mapping := CompileZkevmBin(binf, settings.OptimisationLevel) + // Extract the AIR constraints from the binary file + schema := binf.AirConstraints() // Translate air.Schema into prover's internal representation - Define(sys, schema) - + Define(sys, &schema) + // Construct the driver return &ZkCDriver{ - BinaryFile: binf, - AirSchema: schema, - Settings: &settings, - LimbMapping: mapping, - Metadata: metadata, + BinaryFile: binf, + TracingConfig: constraints.DEFAULT_TRACE_CONFIG, + Settings: &settings, + Metadata: metadata, } } @@ -86,104 +73,68 @@ func NewZkCDriver(sys *wiop.System, settings Settings, bin io.Reader) *ZkCDriver // according to the given schema. The expansion process is about filling in // computed columns with concrete values, such for determining multiplicative // inverses, etc. -func (a *ZkCDriver) Assign(run *wiop.Runtime, traceFile string) { - a.AssignWithPreRead(run, PreReadTrace(traceFile)) +func (a *ZkCDriver) Assign(run *wiop.Runtime, inputsFile string) { + a.AssignWithPreRead(run, ReadZkcInputs(inputsFile)) } -// PreReadResult holds the result of pre-reading a trace file. -type PreReadResult struct { - RawTrace lt.TraceFile - Metadata typed.Map - Err error - TraceFile string +// PreReadInputs holds the result of pre-reading a trace file. +type PreReadInputs struct { + // Inputs as required for the zkc program. Each input corresponds with a + // (non-static) input memory of the ZkC program. For the RISC-V + // interpreter, the inputs will include the full binary of the guest program + // (hence, some entries could be 100Mb or more). + Inputs map[string][]byte + // Errors arising from parsing the input file. + Err error + // Name of the input file. + InputsFile string } -// PreReadTrace reads and parses a trace file, returning the raw trace data. -// This can be called early to overlap I/O with other work. -func PreReadTrace(traceFile string) PreReadResult { - traceF, err := readTraceFile(traceFile) +// ReadZkcInputs reads and parses a zkc inputs file, returning the "pre-read" +// input data. This can be called early to overlap I/O with other work. +func ReadZkcInputs(inputsFile string) PreReadInputs { + traceF, err := ReadMaybeCompressedFile(inputsFile) if err != nil { - return PreReadResult{Err: err, TraceFile: traceFile} + return PreReadInputs{Err: err, InputsFile: inputsFile} } - rawTrace, metadata, err := ReadLtTraces(traceF) - return PreReadResult{RawTrace: rawTrace, Metadata: metadata, Err: err, TraceFile: traceFile} + inputs, err := ReadZkcInputFile(traceF) + return PreReadInputs{Inputs: inputs, Err: err, InputsFile: inputsFile} } // AssignWithPreRead assigns arithmetization columns using a pre-read trace. -func (a *ZkCDriver) AssignWithPreRead(run *wiop.Runtime, preRead PreReadResult) { +func (a *ZkCDriver) AssignWithPreRead(run *wiop.Runtime, preRead PreReadInputs) { assignStart := time.Now() var ( - errs []error - rawTrace = preRead.RawTrace - metadata = preRead.Metadata - errT = preRead.Err + errs []error + inputs = preRead.Inputs + errT = preRead.Err ) logrus.Infof("[bootstrapper] trace available (pre-read): %v", time.Since(assignStart)) // Extract commit metadata from both files - zkevmBinCommit, zkevmBinCommitOk := a.Metadata.String("commit") - traceFileCommit, traceFileCommitOk := metadata.String("commit") - - // Performs a compatibility check by comparing the constraints - // commit of zkevm.bin with the constraints commit of the trace file. - // Panics if an incompatibility is detected. - if !a.Settings.IgnoreCompatibilityCheck { - var errors []string - - if !zkevmBinCommitOk { - errors = append(errors, "missing constraints commit metadata in 'zkevm.bin'") - } - - if !traceFileCommitOk { - errors = append(errors, "missing constraints commit metadata in '.lt' file") - } - - // Check commit mismatch - if zkevmBinCommit != traceFileCommit { - errors = append(errors, "zkevm.bin incompatible with trace file") - errors = append(errors, fmt.Sprintf("zkevm.bin: %s", zkevmBinCommit)) - errors = append(errors, fmt.Sprintf("trace file: %s", traceFileCommit)) - } - - // Panic only if there are errors - if len(errors) > 0 { - for _, err := range errors { - logrus.Error(err) - } - logrus.Panic("compatibility check failed") - } - } else { - logrus.Info("Skip constraints compatibility check between zkevm.bin and trace file") - logrus.Infof("zkevm.bin: %s", zkevmBinCommit) - logrus.Infof("trace file: %s", traceFileCommit) - } + binfCommit, binfCommitOk := a.Metadata.String("commit") - if errT != nil { - logrus.Warnf("error loading the trace fpath=%q err=%v", preRead.TraceFile, errT.Error()) + if !binfCommitOk { + logrus.Warn("missing commit metadata from binary constraints file") } + // + logrus.Infof("constraints commit: %s", binfCommit) - propStart := time.Now() - rawTrace, errs = asm.Propagate(a.BinaryFile.Schema, rawTrace) - - if len(errs) > 0 { - logrus.Warnf("corset propagation gave the following errors: %v", errors.Join(errs...).Error()) + if errT != nil { + logrus.Warnf("error loading the trace fpath=%q err=%v", preRead.InputsFile, errT.Error()) } - - logrus.Infof("[bootstrapper] propagation: %v", time.Since(propStart)) - - expStart := time.Now() - expandedTrace, errs := ir.NewTraceBuilder[koalabear.Element](). - WithBatchSize(1024). - WithRegisterMapping(a.LimbMapping). - Build(a.AirSchema, rawTrace) + // Attempt to trace the ZkC program using the provided inputs, generating a + // fully expanded AIR-compatible trace. + tracingStart := time.Now() + expandedTrace, errs := a.BinaryFile.Trace(inputs, a.TracingConfig) if len(errs) > 0 { - logrus.Warnf("corset expansion gave the following errors: %v", errors.Join(errs...).Error()) + logrus.Panicf("tracing failed: %v", errors.Join(errs...).Error()) } - logrus.Infof("[bootstrapper] expansion: %v", time.Since(expStart)) + logrus.Infof("[bootstrapper] tracing: %v", time.Since(tracingStart)) copyStart := time.Now() - AssignFromLtTraces(run, expandedTrace) + AssignFromTrace(run, expandedTrace, a.BinaryFile.AirConstraints()) logrus.Infof("[bootstrapper] column assignment: %v", time.Since(copyStart)) logrus.Infof("[bootstrapper] total Arithmetization.Assign: %v", time.Since(assignStart)) }