From bca191c6e91cc1cc31f114c1ef0b16bfefa97edf Mon Sep 17 00:00:00 2001 From: DavePearce Date: Mon, 24 Aug 2026 16:52:27 +1200 Subject: [PATCH 1/2] feat: preliminary sharding implementation This puts in place an initial sharding implementation which is working, except for the fact that sharding requires true checkpointing functions. Furthermore, the test framework has not been updated yet for sharding. This adds some checks to ensure that you cannot checkpoint on a returning function. Rather you have to checkpoint on a non-returning function. Signed-off-by: DavePearce --- pkg/cmd/corset/check.go | 110 ++++---- pkg/cmd/corset/inspect.go | 15 +- pkg/cmd/corset/trace.go | 89 +++--- pkg/cmd/corset/util.go | 8 +- pkg/cmd/corset/util/lt_trace_mapping.go | 30 -- pkg/cmd/corset/util/schema_stacker.go | 7 +- pkg/cmd/corset/view/builder.go | 2 +- pkg/cmd/zkc/execute.go | 10 +- pkg/cmd/zkc/trace.go | 38 ++- pkg/cmd/zkc/util.go | 7 +- pkg/ir/air/constraint.go | 3 +- pkg/ir/air/gadgets/bitwidth.go | 2 +- pkg/ir/assignment/computed_register.go | 4 +- pkg/ir/assignment/pseudo_inverse.go | 2 +- pkg/ir/assignment/util.go | 2 +- pkg/ir/builder/alignment.go | 2 +- pkg/ir/builder/validation.go | 4 +- pkg/ir/mir/constraint.go | 7 +- pkg/ir/trace_builder.go | 22 +- pkg/schema/assignment.go | 2 +- pkg/schema/constraint.go | 14 +- pkg/schema/constraint/bus/constraint.go | 125 ++++----- pkg/schema/constraint/bus/constraint_test.go | 237 ---------------- pkg/schema/constraint/bus/failure.go | 38 ++- pkg/schema/constraint/failure.go | 20 +- pkg/schema/constraint/lookup/constraint.go | 30 +- pkg/schema/constraint/lookup/failure.go | 19 +- pkg/schema/constraint/lookup/geometry.go | 36 +-- pkg/schema/constraint/ranged/constraint.go | 20 +- pkg/schema/constraint/ranged/failure.go | 19 +- pkg/schema/constraint/util.go | 2 +- pkg/schema/constraint/vanishing/constraint.go | 28 +- pkg/schema/constraint/vanishing/failure.go | 20 +- pkg/schema/context.go | 201 +++++--------- pkg/schema/module/limbs_map.go | 23 +- pkg/schema/module/module.go | 12 +- pkg/schema/register/limbs_map.go | 38 ++- pkg/schema/schema.go | 8 +- pkg/schema/schemas.go | 68 ++--- pkg/test/corset_invalid_test.go | 3 + pkg/test/corset_valid_test.go | 4 + pkg/test/util/check_legacy.go | 257 +++++------------- pkg/test/util/check_valid.go | 33 +-- pkg/test/zkc_bench_test.go | 6 +- pkg/test/zkc_invalid_test.go | 14 + pkg/test/zkc_unit_test.go | 12 +- pkg/trace/json/reader.go | 52 ++-- pkg/trace/json/writer.go | 28 ++ pkg/trace/reduce.go | 8 +- pkg/trace/ref.go | 23 ++ pkg/trace/trace.go | 8 +- pkg/util/collection/hash/hash_map.go | 27 +- pkg/zkc/compiler/ast/decl/annotation.go | 2 + pkg/zkc/compiler/codegen/compile.go | 2 + pkg/zkc/compiler/compiler.go | 2 + pkg/zkc/compiler/validate/global.go | 43 +++ pkg/zkc/compiler/validate/inline.go | 10 +- pkg/zkc/constraints/binary_file.go | 25 +- pkg/zkc/constraints/call_and_memory_lookup.go | 5 + pkg/zkc/constraints/trace/builder.go | 2 +- .../vm/internal/descriptor/function_kind.go | 17 +- .../internal/interpreter/encoding/common.go | 10 +- pkg/zkc/vm/trace_builder.go | 41 +-- testdata/corset/invalid/bus_invalid_08.lisp | 3 + testdata/corset/valid/bus_01.accepts | 16 +- testdata/corset/valid/bus_01.lisp | 4 +- testdata/corset/valid/bus_01.rejects | 16 +- testdata/corset/valid/bus_01.shards.accepts | 8 - testdata/corset/valid/bus_01.shards.rejects | 6 - testdata/corset/valid/bus_02.accepts | 6 +- testdata/corset/valid/bus_02.lisp | 4 +- testdata/corset/valid/bus_02.rejects | 4 +- testdata/corset/valid/bus_03.accepts | 2 + testdata/corset/valid/bus_03.rejects | 2 + testdata/corset/valid/bus_03.shards.accepts | 2 - testdata/corset/valid/bus_03.shards.rejects | 2 - .../{bus_05.shards.accepts => bus_05.accepts} | 0 .../{bus_05.shards.rejects => bus_05.rejects} | 0 testdata/corset/valid/bus_06.accepts | 80 ++++++ testdata/corset/valid/bus_06.lisp | 7 + testdata/corset/valid/bus_06.rejects | 81 ++++++ .../valid/if_01.expanded.bls12_377.rejects | 3 + testdata/corset/valid/if_01.expanded.rejects | 59 ---- ...nded.O1.accepts => if_10.expanded.accepts} | 0 ...nded.O1.accepts => if_12.expanded.accepts} | 0 ...nded.O1.accepts => if_15.expanded.accepts} | 0 ...cepts => if_18.expanded.bls12_377.accepts} | 17 +- .../lookup_03.expanded.bls12_377.rejects | 4 + .../corset/valid/lookup_03.expanded.rejects | 5 +- testdata/zkc/bench/rec_pow.zkc | 1 + testdata/zkc/invalid/global_01.zkc | 10 + testdata/zkc/invalid/inline_07.zkc | 9 + testdata/zkc/unit/basic_86.zkc | 23 +- testdata/zkc/unit/basic_89.zkc | 1 + testdata/zkc/unit/basic_90.zkc | 1 + testdata/zkc/unit/basic_91.zkc | 1 + 96 files changed, 1120 insertions(+), 1215 deletions(-) delete mode 100644 pkg/cmd/corset/util/lt_trace_mapping.go delete mode 100644 pkg/schema/constraint/bus/constraint_test.go create mode 100644 pkg/zkc/compiler/validate/global.go create mode 100644 testdata/corset/invalid/bus_invalid_08.lisp delete mode 100644 testdata/corset/valid/bus_01.shards.accepts delete mode 100644 testdata/corset/valid/bus_01.shards.rejects delete mode 100644 testdata/corset/valid/bus_03.shards.accepts delete mode 100644 testdata/corset/valid/bus_03.shards.rejects rename testdata/corset/valid/{bus_05.shards.accepts => bus_05.accepts} (100%) rename testdata/corset/valid/{bus_05.shards.rejects => bus_05.rejects} (100%) create mode 100644 testdata/corset/valid/bus_06.accepts create mode 100644 testdata/corset/valid/bus_06.lisp create mode 100644 testdata/corset/valid/bus_06.rejects create mode 100644 testdata/corset/valid/if_01.expanded.bls12_377.rejects delete mode 100644 testdata/corset/valid/if_01.expanded.rejects rename testdata/corset/valid/{if_10.expanded.O1.accepts => if_10.expanded.accepts} (100%) rename testdata/corset/valid/{if_12.expanded.O1.accepts => if_12.expanded.accepts} (100%) rename testdata/corset/valid/{if_15.expanded.O1.accepts => if_15.expanded.accepts} (100%) rename testdata/corset/valid/{if_18.expanded.O1.accepts => if_18.expanded.bls12_377.accepts} (99%) create mode 100644 testdata/corset/valid/lookup_03.expanded.bls12_377.rejects create mode 100644 testdata/zkc/invalid/global_01.zkc create mode 100644 testdata/zkc/invalid/inline_07.zkc diff --git a/pkg/cmd/corset/check.go b/pkg/cmd/corset/check.go index 30f890d1b..56c76b24a 100644 --- a/pkg/cmd/corset/check.go +++ b/pkg/cmd/corset/check.go @@ -24,15 +24,10 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/corset" "github.com/LFDT-Lineth/zkc/pkg/ir" sc "github.com/LFDT-Lineth/zkc/pkg/schema" - "github.com/LFDT-Lineth/zkc/pkg/schema/constraint" - "github.com/LFDT-Lineth/zkc/pkg/schema/constraint/bus" - "github.com/LFDT-Lineth/zkc/pkg/schema/constraint/lookup" - "github.com/LFDT-Lineth/zkc/pkg/schema/constraint/ranged" - "github.com/LFDT-Lineth/zkc/pkg/schema/constraint/vanishing" "github.com/LFDT-Lineth/zkc/pkg/schema/module" tr "github.com/LFDT-Lineth/zkc/pkg/trace" "github.com/LFDT-Lineth/zkc/pkg/util" - "github.com/LFDT-Lineth/zkc/pkg/util/collection/set" + "github.com/LFDT-Lineth/zkc/pkg/util/collection/array" "github.com/LFDT-Lineth/zkc/pkg/util/field" "github.com/LFDT-Lineth/zkc/pkg/util/field/bls12_377" "github.com/LFDT-Lineth/zkc/pkg/util/field/gf251" @@ -176,11 +171,7 @@ type CheckConfig struct { func checkWithLegacyPipeline[F field.Element[F]](cfg CheckConfig, batched bool, tracefile string, schemas cmd_util.SchemaStacker[F]) { // - var ( - errors []error - traces []tr.Trace[F] - ok bool = true - ) + var traces []tr.Trace[F] // stats := util.NewPerfStats() // Extract debug information (if available) @@ -196,15 +187,7 @@ func checkWithLegacyPipeline[F field.Element[F]](cfg CheckConfig, batched bool, traces = []tr.Trace[F]{ReadTraceFile[F](tracefile)} } // Go! - if len(errors) == 0 { - ok = checkTraces(traces, schemas, cfg) && ok - } - // Handle errors - if !ok || len(errors) > 0 { - for _, err := range errors { - log.Errorf("%s\n", err.Error()) - } - // + if ok := checkTraces(traces, schemas, cfg); !ok { os.Exit(1) } } @@ -212,7 +195,7 @@ func checkWithLegacyPipeline[F field.Element[F]](cfg CheckConfig, batched bool, func checkTraces[F field.Element[F]](traces []tr.Trace[F], stacker cmd_util.SchemaStacker[F], cfg CheckConfig) bool { // - for _, tf := range traces { + for _, trace := range traces { // Configure stack. This is important to ensure true separation // between runs (e.g. for the io.Executor). stack := stacker.Build() @@ -223,7 +206,7 @@ func checkTraces[F field.Element[F]](traces []tr.Trace[F], stacker cmd_util.Sche // identify schema name ir := stack.ConcreteIrName() // - if ok := CheckTrace(ir, schema, tf, builder, cfg); !ok { + if ok := CheckTrace(ir, schema, builder, cfg, trace); !ok { return false } } @@ -233,24 +216,36 @@ func checkTraces[F field.Element[F]](traces []tr.Trace[F], stacker cmd_util.Sche // CheckTrace checks a given set of constraints against a given trace file using // a configured trace builder and check configuration. -func CheckTrace[F field.Element[F]](ir string, schema sc.AnySchema[F], tf tr.Trace[F], builder ir.TraceBuilder[F], - cfg CheckConfig) bool { +func CheckTrace[F field.Element[F]](ir string, schema sc.AnySchema[F], builder ir.TraceBuilder[F], + cfg CheckConfig, trace tr.Trace[F]) bool { // begin performance measurement - stats := util.NewPerfStats() - trace, errs := builder.Build(schema, tf) + var ( + mapping = module.IdentityMap[F](schema.Modules().Collect()...) + stats = util.NewPerfStats() + recoverable bool = true + errs []error + ) + // + for i, shard := range trace { + var es []error + + trace[i], es = builder.Build(schema, shard) + errs = append(errs, es...) + recoverable = recoverable && (trace[i] != nil) + } // Log cost of expansion stats.Log("Expanding trace columns") // Report any errors reportErrors(ir, errs) // Check whether considered unrecoverable - if trace == nil || len(errs) > 0 { + if !recoverable || len(errs) > 0 { return false } // stats = util.NewPerfStats() // Check constraints if errs := sc.Accepts(builder.Parallelism(), schema, trace); len(errs) > 0 { - ReportFailures(ir, errs, trace, builder.Mapping(), cfg) + ReportFailures(ir, mapping, cfg, trace, errs) return false } // @@ -261,15 +256,13 @@ func CheckTrace[F field.Element[F]](ir string, schema sc.AnySchema[F], tf tr.Tra // ReportFailures reports constraint failures, whilst providing contextual // information (when requested). -func ReportFailures[F field.Element[F]](ir string, failures []sc.Failure, trace tr.Trace[F], - mapping module.LimbsMap, cfg CheckConfig) { +func ReportFailures[F field.Element[F]](ir string, + mapping module.LimbsMap, cfg CheckConfig, trace tr.Trace[F], failures []sc.Failure[F]) { // - var ( - errs = make([]error, len(failures)) - ) + var errs = make([]error, len(failures)) // - for i, f := range failures { - errs[i] = errors.New(f.Message()) + for j, f := range failures { + errs[j] = errors.New(f.Message()) } // First, log errors reportErrors(ir, errs) @@ -282,34 +275,33 @@ func ReportFailures[F field.Element[F]](ir string, failures []sc.Failure, trace } // Print a human-readable report detailing the given failure -func reportFailure[F field.Element[F]](failure sc.Failure, trace tr.Trace[F], mapping module.LimbsMap, +func reportFailure[F field.Element[F]](failure sc.Failure[F], trace tr.Trace[F], mapping module.LimbsMap, cfg CheckConfig) { + // Identify all relevant cells + var cells = failure.RequiredCells(trace) + fmt.Printf("failing constraint %s:\n", failure.Handle()) // - if f, ok := failure.(*vanishing.Failure[F]); ok { - cells := f.RequiredCells(trace) - fmt.Printf("failing constraint %s:\n", f.Handle) - reportRelevantCells(cells, trace, mapping, cfg) - } else if f, ok := failure.(*ranged.Failure[F]); ok { - cells := f.RequiredCells(trace) - fmt.Printf("failing range constraint %s:\n", f.Handle) - reportRelevantCells(cells, trace, mapping, cfg) - } else if f, ok := failure.(*lookup.Failure[F]); ok { - cells := f.RequiredCells(trace) - fmt.Printf("failing lookup constraint %s:\n", f.Handle) - reportRelevantCells(cells, trace, mapping, cfg) - } else if f, ok := failure.(*bus.Failure[F]); ok { - cells := f.RequiredCells(trace) - fmt.Printf("failing bus constraint %s:\n", f.Handle) - reportRelevantCells(cells, trace, mapping, cfg) - } else if f, ok := failure.(*constraint.InternalFailure[F]); ok { - cells := f.RequiredCells(trace) - fmt.Printf("%s:\n", f.Message()) - reportRelevantCells(cells, trace, mapping, cfg) + for i, shard := range trace { + // Filter out cells relevant to the given shard + var ( + lsharded = array.Filter(cells, func(r tr.ShardedCellRef) bool { + return r.Shard == uint(i) + }) + // Map to cell refs + lcells = array.Map(lsharded, func(_ uint, r tr.ShardedCellRef) tr.CellRef { + return r.Ref + }) + ) + // Check whether anything to report for this + if len(lcells) > 0 { + // Print out cells for the given shard. + reportRelevantCells(lcells, shard, mapping, cfg) + } } } // Print a human-readable report detailing the given failure with a vanishing constraint. -func reportRelevantCells[F field.Element[F]](cells *set.AnySortedSet[tr.CellRef], trace tr.Trace[F], +func reportRelevantCells[F field.Element[F]](cells []tr.CellRef, trace tr.Shard[F], mapping module.LimbsMap, cfg CheckConfig) { // Construct trace window builder := view.NewBuilder[F](mapping). @@ -317,7 +309,7 @@ func reportRelevantCells[F field.Element[F]](cells *set.AnySortedSet[tr.CellRef] WithComputed(cfg.ReportComputed). WithCellWidth(cfg.ReportCellWidth). WithTitleWidth(cfg.ReportTitleWidth). - WithFormatting(view.NewCellFormatter(*cells, cfg.AnsiEscapes)) + WithFormatting(view.NewCellFormatter(cells, cfg.AnsiEscapes)) // if cfg.CorsetSourceMap != nil { builder = builder.WithSourceMap(*cfg.CorsetSourceMap) @@ -325,7 +317,7 @@ func reportRelevantCells[F field.Element[F]](cells *set.AnySortedSet[tr.CellRef] // Build window window := builder.Build(trace) // Focus window on those cells relevant to the failure - window = window.Filter(view.FilterForCells(*cells, cfg.ReportPadding)) + window = window.Filter(view.FilterForCells(cells, cfg.ReportPadding)) // Print all windows for i := range window.Width() { var ( diff --git a/pkg/cmd/corset/inspect.go b/pkg/cmd/corset/inspect.go index 5cc95a877..58ef4ac3a 100644 --- a/pkg/cmd/corset/inspect.go +++ b/pkg/cmd/corset/inspect.go @@ -52,7 +52,7 @@ var inspectCmds = []FieldAgnosticCmd{ func runInspectCmd[F field.Element[F]](cmd *cobra.Command, args []string) { var ( errors []error - trace trace.Trace[F] + trace trace.Shard[F] ) // if len(args) != 2 { @@ -91,13 +91,16 @@ func runInspectCmd[F field.Element[F]](cmd *cobra.Command, args []string) { if len(errors) != 0 && validate { fmt.Println("(use --validate=false to ignore trace propagation errors)") fmt.Println() + } else if len(tracefile) != 1 { + errors = append(errors, fmt.Errorf("cannot inspect multiple shards")) } else { - trace, errors = stack.TraceBuilder().Build(schema, tracefile) + trace, errors = stack.TraceBuilder().Build(schema, tracefile[0]) } // if len(errors) == 0 { + mapping := module.IdentityMap[F](schema.Modules().Collect()...) // Run the inspector. - errors = inspect(stack.TraceBuilder().Mapping(), srcmap, trace, showLimbs, cellWidth, titleWidth) + errors = inspect(mapping, srcmap, trace, showLimbs, cellWidth, titleWidth) } // Sanity check what happened if len(errors) > 0 { @@ -117,7 +120,7 @@ func runInspectCmd[F field.Element[F]](cmd *cobra.Command, args []string) { // The optional "public" predicate determines which modules are publicly visible // (shown by default); when nil, all modules are public. Callers use this to // hide synthetic modules such as range-check tables. -func InspectTrace[F field.Element[F]](mapping module.LimbsMap, trace trace.Trace[F], +func InspectTrace[F field.Element[F]](mapping module.LimbsMap, trace trace.Shard[F], public func(string) bool, limbs bool, cellWidth, titleWidth uint) []error { // term, err := termio.NewTerminal() @@ -148,7 +151,7 @@ func InspectTrace[F field.Element[F]](mapping module.LimbsMap, trace trace.Trace } // Inspect a given trace using a given schema. -func inspect[F field.Element[F]](mapping module.LimbsMap, srcmap *corset.SourceMap, trace trace.Trace[F], +func inspect[F field.Element[F]](mapping module.LimbsMap, srcmap *corset.SourceMap, trace trace.Shard[F], limbs bool, cellWidth, titleWidth uint) []error { // Construct inspector window inspector := construct(mapping, trace, srcmap, limbs, cellWidth, titleWidth) @@ -160,7 +163,7 @@ func inspect[F field.Element[F]](mapping module.LimbsMap, srcmap *corset.SourceM return inspector.Start() } -func construct[F field.Element[F]](mapping module.LimbsMap, trace trace.Trace[F], srcmap *corset.SourceMap, limbs bool, +func construct[F field.Element[F]](mapping module.LimbsMap, trace trace.Shard[F], srcmap *corset.SourceMap, limbs bool, cellWidth, titleWidth uint) *inspector.Inspector { // term, err := termio.NewTerminal() diff --git a/pkg/cmd/corset/trace.go b/pkg/cmd/corset/trace.go index 5451c9bf9..797e790ce 100644 --- a/pkg/cmd/corset/trace.go +++ b/pkg/cmd/corset/trace.go @@ -202,7 +202,7 @@ type TraceConfig struct { stats bool } -func constructTraceFilter[F field.Element[F]](cfg TraceConfig, trace tr.Trace[F]) view.TraceFilter { +func constructTraceFilter[F field.Element[F]](cfg TraceConfig, trace tr.Shard[F]) view.TraceFilter { return view.NewTraceFilter(func(mid module.Id) view.ModuleFilter { return view.NewModuleFilter(cfg.startRow, cfg.endRow, func(col view.SourceColumn) bool { // Construct fully qualified name @@ -238,52 +238,63 @@ func expandTrace[F field.Element[F]](tf tr.Trace[F], stack cmd_util.SchemaStack[ var ( tb_errors []error tp_errors []error - tr tr.Trace[F] + tr = make(tr.Trace[F], len(tf)) ) - // Construct expanded trace - tr, tb_errors = bldr.Build(stack.ConcreteSchema(), tf) - // Handle errors - if len(tb_errors) > 0 { - for _, err := range tb_errors { - log.Errorln(err) + // + for i, shard := range tf { + // Construct expanded trace + tr[i], tb_errors = bldr.Build(stack.ConcreteSchema(), shard) + // Handle errors + if len(tb_errors) > 0 { + for _, err := range tb_errors { + log.Errorln(err) + } + // + os.Exit(1) } - // - os.Exit(1) } // Now, reconstruct it! return tr, tp_errors } func printTraceInfo[F field.Element[F]](cfg TraceConfig, trace tr.Trace[F]) { - // Construct trace window - view := view.NewBuilder[F](cfg.mapping). - WithCellWidth(cfg.maxCellWidth). - WithTitleWidth(cfg.maxTitleWidth). - WithLimbs(cfg.showLimbs). - WithComputed(cfg.showComputed) - // Add source map (if applicable) - if cfg.sourceMap != nil { - view = view.WithSourceMap(*cfg.sourceMap) - } - // Construct viewing window - window := view.Build(trace) - // Construct & apply trace filter - window = window.Filter(constructTraceFilter(cfg, trace)) - // Print column summaries (if requested) - if cfg.columns { - listColumns(cfg, window) - } - // Print module summaries (if requested) - if cfg.modules { - listModules(cfg, window) - } - // Print trace summary (if requested) - if cfg.stats { - summaryStats(window) - } - // Print full trace (if requested) - if cfg.trace { - printTrace(window) + for i, shard := range trace { + // + if len(trace) > 0 { + fmt.Println() + fmt.Printf("Shard #%d\n", i) + fmt.Println(strings.Repeat("-", int(80))) + } + // Construct trace window + view := view.NewBuilder[F](cfg.mapping). + WithCellWidth(cfg.maxCellWidth). + WithTitleWidth(cfg.maxTitleWidth). + WithLimbs(cfg.showLimbs). + WithComputed(cfg.showComputed) + // Add source map (if applicable) + if cfg.sourceMap != nil { + view = view.WithSourceMap(*cfg.sourceMap) + } + // Construct viewing window + window := view.Build(shard) + // Construct & apply trace filter + window = window.Filter(constructTraceFilter(cfg, shard)) + // Print column summaries (if requested) + if cfg.columns { + listColumns(cfg, window) + } + // Print module summaries (if requested) + if cfg.modules { + listModules(cfg, window) + } + // Print trace summary (if requested) + if cfg.stats { + summaryStats(window) + } + // Print full trace (if requested) + if cfg.trace { + printTrace(cfg, window) + } } } diff --git a/pkg/cmd/corset/util.go b/pkg/cmd/corset/util.go index a077f4226..a188b282e 100644 --- a/pkg/cmd/corset/util.go +++ b/pkg/cmd/corset/util.go @@ -154,8 +154,8 @@ func writeTraceFile[F field.Element[F]](filename string, tracefile trace.Trace[F // columns. func ReadTraceFile[F field.Element[F]](filename string) trace.Trace[F] { var ( - stats = util.NewPerfStats() - tracefile trace.Trace[F] + stats = util.NewPerfStats() + shards trace.Trace[F] ) // Read data file filename, data, err := file.ReadAndUncompress(filename) @@ -166,7 +166,7 @@ func ReadTraceFile[F field.Element[F]](filename string) trace.Trace[F] { // switch ext { case ".json": - tracefile, err = json.FromBytes[F](data) + shards, err = json.FromBytes[F](data) default: err = fmt.Errorf("unknown trace file format: %s", ext) } @@ -180,7 +180,7 @@ func ReadTraceFile[F field.Element[F]](filename string) trace.Trace[F] { os.Exit(2) } // - return tracefile + return shards } // ReadBatchedTraceFile reads a file containing zero or more traces expressed as diff --git a/pkg/cmd/corset/util/lt_trace_mapping.go b/pkg/cmd/corset/util/lt_trace_mapping.go deleted file mode 100644 index 849ea65f8..000000000 --- a/pkg/cmd/corset/util/lt_trace_mapping.go +++ /dev/null @@ -1,30 +0,0 @@ -// Copyright Consensys Software Inc. -// -// Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with -// the License. You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on -// an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the -// specific language governing permissions and limitations under the License. -// -// SPDX-License-Identifier: Apache-2.0 -package util - -import ( - "math" - - "github.com/LFDT-Lineth/zkc/pkg/schema/module" - "github.com/LFDT-Lineth/zkc/pkg/schema/register" - "github.com/LFDT-Lineth/zkc/pkg/util/field" -) - -// IdentityMapping constructs a trivial (unsplit) limbs map for a set of -// modules, where every register maps to exactly itself. This is used in -// place of a genuine subdivision mapping now that registers are never split -// into limbs. -func IdentityMapping[F field.Element[F], M register.Map](name string, modules ...M) module.LimbsMap { - var cfg = field.Config{Name: name, BandWidth: math.MaxUint, RegisterWidth: math.MaxUint} - return module.NewLimbsMap[F](cfg, modules...) -} diff --git a/pkg/cmd/corset/util/schema_stacker.go b/pkg/cmd/corset/util/schema_stacker.go index 01d4d0d30..502565124 100644 --- a/pkg/cmd/corset/util/schema_stacker.go +++ b/pkg/cmd/corset/util/schema_stacker.go @@ -24,6 +24,7 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/ir/air" "github.com/LFDT-Lineth/zkc/pkg/ir/mir" "github.com/LFDT-Lineth/zkc/pkg/schema" + "github.com/LFDT-Lineth/zkc/pkg/schema/module" "github.com/LFDT-Lineth/zkc/pkg/util" "github.com/LFDT-Lineth/zkc/pkg/util/collection/bit" "github.com/LFDT-Lineth/zkc/pkg/util/field" @@ -157,11 +158,11 @@ func (p SchemaStacker[F]) Build() SchemaStack[F] { mirSchema := mir.Concretize[word.BigEndian, F](absSchema.RawModules()) // Construct a trivial (unsplit) register mapping, since registers are // no longer subdivided into limbs. - mapping := IdentityMapping[F](p.corsetConfig.Field.Name, mirSchema.RawModules()...) - // stats.Log("translation") // Record mapping - stack.mapping = mapping + stack.mapping = module.IdentityMap[F](mirSchema.Modules().Collect()...) + // Copy over builder + stack.traceBuilder = p.traceBuilder // Include Mid-level IR layer (if requested) if p.layers.Contains(MIR_LAYER) { stack.concreteSchemas = append(stack.concreteSchemas, mirSchema) diff --git a/pkg/cmd/corset/view/builder.go b/pkg/cmd/corset/view/builder.go index c3081b9e7..5a0b44d49 100644 --- a/pkg/cmd/corset/view/builder.go +++ b/pkg/cmd/corset/view/builder.go @@ -130,7 +130,7 @@ func (p Builder[F]) WithVisibility(public func(string) bool) Builder[F] { } // Build the viewing window for this trace. -func (p Builder[F]) Build(trace tr.Trace[F]) TraceView { +func (p Builder[F]) Build(trace tr.Shard[F]) TraceView { var windows []ModuleView // srcmap, enums := extractSourceMap(p.srcmap) diff --git a/pkg/cmd/zkc/execute.go b/pkg/cmd/zkc/execute.go index 6b77dc7ec..f87a6f6ed 100644 --- a/pkg/cmd/zkc/execute.go +++ b/pkg/cmd/zkc/execute.go @@ -129,7 +129,7 @@ func runExecuteCmd[F field.Element[F]](cmd *cobra.Command, args []string, field // ===================================================== if check && trace != nil { // NOTE: check ==> tracing - checkConstraints(binfile, trace, traceConfig) + checkConstraints(binfile, traceConfig, trace) } // ===================================================== // Report Execution Failures @@ -144,8 +144,8 @@ func runExecuteCmd[F field.Element[F]](cmd *cobra.Command, args []string, field } } -func checkConstraints[F field.Element[F]](binfile *constraints.BinaryFile[F], tr trace.Trace[F], - cfg vm.TraceConfig) { +func checkConstraints[F field.Element[F]](binfile *constraints.BinaryFile[F], + cfg vm.TraceConfig, trace trace.Trace[F]) { // var checkConfig corset.CheckConfig // Set sensible defaults (for now) @@ -159,8 +159,8 @@ func checkConstraints[F field.Element[F]](binfile *constraints.BinaryFile[F], tr // Construct limbs map mapping := binfile.LimbsMap() // Run the check - if failures := binfile.Check(tr, cfg); len(failures) > 0 { - corset.ReportFailures("AIR", failures, tr, mapping, checkConfig) + if failures := binfile.Check(cfg, trace); len(failures) > 0 { + corset.ReportFailures("AIR", mapping, checkConfig, trace, failures) } } diff --git a/pkg/cmd/zkc/trace.go b/pkg/cmd/zkc/trace.go index f695f5ddc..6a40b0ce6 100644 --- a/pkg/cmd/zkc/trace.go +++ b/pkg/cmd/zkc/trace.go @@ -111,8 +111,8 @@ func runTraceCmd[F field.Element[F]](cmd *cobra.Command, args []string, field fi // print trace statistics (if requested). Only meaningful when a trace was // actually generated (i.e. no execution errors). if stats && len(errors) == 0 { - printTraceStats(trace) - printModuleStats(trace) + printTraceStats(trace...) + printModuleStats(trace...) } // print entire trace (if requested). Unlike the inspector, there is no way // to reveal a module which was hidden, so everything carrying data is shown @@ -129,17 +129,21 @@ func runTraceCmd[F field.Element[F]](cmd *cobra.Command, args []string, field fi // Check Constraints // ===================================================== if check && trace != nil { - checkConstraints(binfile, trace, traceConfig) + checkConstraints(binfile, traceConfig, trace) } // ===================================================== // Inspect // ===================================================== // Open the generated trace in the interactive inspector (if requested). This // takes over the terminal, so it runs last, after any stdout output above. - if inspect && trace != nil { + if inspect && len(trace) == 1 { // Real ZkC functions are public; synthetic modules (e.g. range-check // tables) are private (hidden by default in the inspector). - errors = corset.InspectTrace(binfile.LimbsMap(), trace, publicModule, false, 32, 128) + errors = corset.InspectTrace(binfile.LimbsMap(), trace[0], publicModule, false, 32, 128) + } else if inspect && len(trace) > 0 { + errors = append(errors, fmt.Errorf("cannot inspect multiple trace shards")) + } else if inspect { + errors = append(errors, fmt.Errorf("cannot inspect zero trace shards")) } // ===================================================== // Report Execution Failures @@ -214,15 +218,21 @@ const ( // traced cells (both human-readable and raw) plus a breakdown of columns by // bit-width. Columns backed by field elements (i.e. native registers, which // have no fixed bit-width) are reported separately. -func printTraceStats[F field.Element[F]](rtr trace.Trace[F]) { +func printTraceStats[F field.Element[F]](shards ...trace.Shard[F]) { + for _, shard := range shards { + printShardStats(shard) + } +} + +func printShardStats[F field.Element[F]](shard trace.Shard[F]) { var ( cells uint counts = make([]uint, len(traceStatBuckets)) native uint ) // Tally cells and per-column bit-widths across all modules. - for mid := range rtr.Width() { - mod := rtr.Module(mid) + for mid := range shard.Width() { + mod := shard.Module(mid) cells += mod.Width() * mod.Height() // for _, reg := range mod.Descriptor().Columns { @@ -289,9 +299,15 @@ var moduleStatTitles = []string{"columns", "lines", "bitwidth", "cells", "nonzer // the column count, line (row) count, total bit-width, total cells, non-zero // cells and total bytes. Native (field-element) limbs, which have no fixed // bit-width, are excluded from the bit-width and byte totals. -func printModuleStats[F field.Element[F]](rtr trace.Trace[F]) { +func printModuleStats[F field.Element[F]](shards ...trace.Shard[F]) { + for _, shard := range shards { + printShardModuleStats(shard) + } +} + +func printShardModuleStats[F field.Element[F]](shard trace.Shard[F]) { var ( - n = rtr.Width() + n = shard.Width() tbl = termio.NewFormattedTable(uint(len(moduleStatTitles))+1, n+1) ) // Set column titles (leaving the top-left cell blank, as corset does). @@ -301,7 +317,7 @@ func printModuleStats[F field.Element[F]](rtr trace.Trace[F]) { // Compute a summary row for each module. for mid := range n { var ( - mod = rtr.Module(mid) + mod = shard.Module(mid) columns = mod.Width() lines = mod.Height() bitwidth uint diff --git a/pkg/cmd/zkc/util.go b/pkg/cmd/zkc/util.go index 7bdc8f0ca..255d08620 100644 --- a/pkg/cmd/zkc/util.go +++ b/pkg/cmd/zkc/util.go @@ -177,15 +177,16 @@ func printSyntaxError(err *source.SyntaxError) { } // WriteTraceFile writes a given trace to disk in JSON format. -func WriteTraceFile[F field.Element[F]](filename string, tracefile trace.Trace[F]) { +func WriteTraceFile[F field.Element[F]](filename string, trace trace.Trace[F]) { var err error // Check file extension ext := path.Ext(filename) // switch ext { case ".json": - js := json.ToJsonString(tracefile) - // + // Append data for each shard + js := json.ToJsonString(trace) + // Write out final data if err = os.WriteFile(filename, []byte(js), 0644); err == nil { return } diff --git a/pkg/ir/air/constraint.go b/pkg/ir/air/constraint.go index bfe48ad49..305c43161 100644 --- a/pkg/ir/air/constraint.go +++ b/pkg/ir/air/constraint.go @@ -93,7 +93,8 @@ func (p Air[F, C]) Air() { // Accepts determines whether a given constraint accepts a given trace or // not. If not, a failure is produced. Otherwise, a bitset indicating // branch coverage is returned. -func (p Air[F, C]) Accepts(trace trace.Trace[F], schema schema.AnySchema[F], ctx schema.Context[F]) schema.Failure { +func (p Air[F, C]) Accepts(trace trace.Trace[F], schema schema.AnySchema[F], ctx schema.Context[F], +) []schema.Failure[F] { return p.constraint.Accepts(trace, schema, ctx) } diff --git a/pkg/ir/air/gadgets/bitwidth.go b/pkg/ir/air/gadgets/bitwidth.go index 8a67c551e..35e07f908 100644 --- a/pkg/ir/air/gadgets/bitwidth.go +++ b/pkg/ir/air/gadgets/bitwidth.go @@ -221,7 +221,7 @@ func (p *typeDecomposition[F]) AddSource(source register.Ref) { // Compute computes the values of columns defined by this assignment. // This requires computing the value of each byte column in the decomposition. -func (p *typeDecomposition[F]) Compute(tr trace.Trace[F], schema sc.AnySchema[F], +func (p *typeDecomposition[F]) Compute(tr trace.Shard[F], schema sc.AnySchema[F], ) ([]array.MutArray[F], error) { // Read inputs sources := assignment.ReadRegistersRef(tr, p.sources...) diff --git a/pkg/ir/assignment/computed_register.go b/pkg/ir/assignment/computed_register.go index ec0394867..059500de7 100644 --- a/pkg/ir/assignment/computed_register.go +++ b/pkg/ir/assignment/computed_register.go @@ -69,7 +69,7 @@ func (p *ComputedRegister[F]) Bounds(mid sc.ModuleId) util.Bounds { // Compute the values of columns defined by this assignment. Specifically, this // creates a new column which contains the result of evaluating a given // expression on each row. -func (p *ComputedRegister[F]) Compute(tr trace.Trace[F], schema sc.AnySchema[F], +func (p *ComputedRegister[F]) Compute(tr trace.Shard[F], schema sc.AnySchema[F], ) ([]array.MutArray[F], error) { var ( trModule = tr.Module(p.Module) @@ -164,7 +164,7 @@ func fwdComputation[F field.Element[F]](height uint, data array.MutArray[F], exp // error check if err != nil { e := fmt.Sprintf("%s for %s", err.Error(), expr.Lisp(false, scMod).String(true)) - return constraint.NewInternalFailure[F](scMod.Name(), ctx, i, expr, e) + return constraint.NewInternalFailure[F](scMod.Name(), ctx, i, e) } // Write data data.Set(i, val) diff --git a/pkg/ir/assignment/pseudo_inverse.go b/pkg/ir/assignment/pseudo_inverse.go index 196068e1a..179c42fd4 100644 --- a/pkg/ir/assignment/pseudo_inverse.go +++ b/pkg/ir/assignment/pseudo_inverse.go @@ -57,7 +57,7 @@ func (e *PseudoInverse[F]) Bounds(mid schema.ModuleId) util.Bounds { } // Compute performs the inversion. -func (e *PseudoInverse[F]) Compute(tr trace.Trace[F], schema schema.AnySchema[F]) ([]array.MutArray[F], error) { +func (e *PseudoInverse[F]) Compute(tr trace.Shard[F], schema schema.AnySchema[F]) ([]array.MutArray[F], error) { var ( trModule = tr.Module(e.Target.Module()) scModule = schema.Module(e.Target.Module()) diff --git a/pkg/ir/assignment/util.go b/pkg/ir/assignment/util.go index 9353a9adb..590b9c275 100644 --- a/pkg/ir/assignment/util.go +++ b/pkg/ir/assignment/util.go @@ -20,7 +20,7 @@ import ( ) // ReadRegistersRef reads the values for a given set of registers from a trace. -func ReadRegistersRef[F field.Element[F]](trace trace.Trace[F], regs ...register.Ref) []array.Array[F] { +func ReadRegistersRef[F field.Element[F]](trace trace.Shard[F], regs ...register.Ref) []array.Array[F] { var ( targets = make([]array.Array[F], len(regs)) ) diff --git a/pkg/ir/builder/alignment.go b/pkg/ir/builder/alignment.go index ef39e8b6f..57b838a1d 100644 --- a/pkg/ir/builder/alignment.go +++ b/pkg/ir/builder/alignment.go @@ -57,7 +57,7 @@ type Config struct { // NOTE: alignment is impacted by whether or not the trace is being expanded or // not. Specifically, expanding traces don't need to include data for computed // columns, since these will be added during expansion. -func AlignAndPad[F field.Element[F]](config Config, schema sc.AnySchema[F], tr trace.Trace[F], +func AlignAndPad[F field.Element[F]](config Config, schema sc.AnySchema[F], tr trace.Shard[F], ) (ArrayTrace[F], []error) { // var ( diff --git a/pkg/ir/builder/validation.go b/pkg/ir/builder/validation.go index 6104e2af9..4211c8ff2 100644 --- a/pkg/ir/builder/validation.go +++ b/pkg/ir/builder/validation.go @@ -26,7 +26,7 @@ import ( // TraceValidation validates that values held in trace columns match the // expected type. This is really a sanity check that the trace is not // malformed. -func TraceValidation[F field.Element[F]](config Config, schema sc.AnySchema[F], tr trace.Trace[F]) []error { +func TraceValidation[F field.Element[F]](config Config, schema sc.AnySchema[F], tr trace.Shard[F]) []error { var ( errors []error // Start timer @@ -60,7 +60,7 @@ func TraceValidation[F field.Element[F]](config Config, schema sc.AnySchema[F], return append(errs, errors...) } -func flattenTrace[F field.Element[F]](schema sc.AnySchema[F], tr trace.Trace[F]) ([]trace.ColumnRef, []error) { +func flattenTrace[F field.Element[F]](schema sc.AnySchema[F], tr trace.Shard[F]) ([]trace.ColumnRef, []error) { var ( errors []error // diff --git a/pkg/ir/mir/constraint.go b/pkg/ir/mir/constraint.go index b12180a40..5be67d4a5 100644 --- a/pkg/ir/mir/constraint.go +++ b/pkg/ir/mir/constraint.go @@ -61,10 +61,9 @@ func NewRangeConstraint[F field.Element[F]](handle string, ctx schema.ModuleId, return Constraint[F]{ranged.NewConstraint[F](handle, ctx, registers, bitwidths)} } -// Accepts determines whether a given constraint accepts a given trace or -// not. If not, a failure is produced. Otherwise, a bitset indicating -// branch coverage is returned. -func (p Constraint[F]) Accepts(trace trace.Trace[F], sc schema.AnySchema[F], ctx schema.Context[F]) schema.Failure { +// Accepts implementation of schema.Constraint interface. +func (p Constraint[F]) Accepts(trace trace.Trace[F], sc schema.AnySchema[F], ctx schema.Context[F], +) []schema.Failure[F] { // return p.constraint.Accepts(trace, sc, ctx) } diff --git a/pkg/ir/trace_builder.go b/pkg/ir/trace_builder.go index a7618ba25..f45284d79 100644 --- a/pkg/ir/trace_builder.go +++ b/pkg/ir/trace_builder.go @@ -17,7 +17,6 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/ir/builder" sc "github.com/LFDT-Lineth/zkc/pkg/schema" - "github.com/LFDT-Lineth/zkc/pkg/schema/module" "github.com/LFDT-Lineth/zkc/pkg/trace" "github.com/LFDT-Lineth/zkc/pkg/util/field" ) @@ -44,15 +43,12 @@ type TraceBuilder[F field.Element[F]] struct { parallel bool // Specify the maximum size of any dispatched batch. batchSize uint - // Mapping specifies whether or not columns in the trace need to be split to - // match the given field configuration. - mapping module.LimbsMap } // NewTraceBuilder constructs a default trace builder. The idea is that this // could then be customized as needed following the builder pattern. func NewTraceBuilder[F field.Element[F]]() TraceBuilder[F] { - return TraceBuilder[F]{true, true, NextPowerOfTwoPadding, true, math.MaxUint, nil} + return TraceBuilder[F]{true, true, NextPowerOfTwoPadding, true, math.MaxUint} } // WithExpansion updates a given builder configuration to perform trace expansion (or @@ -64,15 +60,6 @@ func (tb TraceBuilder[F]) WithExpansion(flag bool) TraceBuilder[F] { return ntb } -// WithRegisterMapping updates a given builder configuration to split the trace -// according to a given mapping of registers. -func (tb TraceBuilder[F]) WithRegisterMapping(mapping module.LimbsMap) TraceBuilder[F] { - ntb := tb - ntb.mapping = mapping - // - return ntb -} - // WithValidation updates a given builder configuration to perform trace validation (or // not). func (tb TraceBuilder[F]) WithValidation(flag bool) TraceBuilder[F] { @@ -123,14 +110,9 @@ func (tb TraceBuilder[F]) BatchSize() uint { return tb.batchSize } -// Mapping returns the mapping from registers to limbs used with this builder. -func (tb TraceBuilder[F]) Mapping() module.LimbsMap { - return tb.mapping -} - // Build attempts to construct a trace for a given schema, producing errors if // there are inconsistencies (e.g. missing columns, duplicate columns, etc). -func (tb TraceBuilder[F]) Build(schema sc.AnySchema[F], tf trace.Trace[F]) (tr trace.Trace[F], errs []error) { +func (tb TraceBuilder[F]) Build(schema sc.AnySchema[F], tf trace.Shard[F]) (tr trace.Shard[F], errs []error) { var ( atr builder.ArrayTrace[F] config = builder.Config{ diff --git a/pkg/schema/assignment.go b/pkg/schema/assignment.go index 5a2553d4e..67cf9db49 100644 --- a/pkg/schema/assignment.go +++ b/pkg/schema/assignment.go @@ -39,7 +39,7 @@ type Assignment[F any] interface { // assignment depends must exist (e.g. are either inputs or have been // computed already). Computed columns do not exist in the original trace, // but are added during trace expansion to form the final trace. - Compute(trace.Trace[F], AnySchema[F]) ([]array.MutArray[F], error) + Compute(trace.Shard[F], AnySchema[F]) ([]array.MutArray[F], error) // Consistent applies a number of internal consistency checks. Whilst not // strictly necessary, these can highlight otherwise hidden problems as an aid // to debugging. diff --git a/pkg/schema/constraint.go b/pkg/schema/constraint.go index 5b48ecd2d..afe5ab70f 100644 --- a/pkg/schema/constraint.go +++ b/pkg/schema/constraint.go @@ -29,10 +29,10 @@ import ( // Constraint represents an element which can "accept" a trace, or either reject // with an error (or eventually perhaps report a warning). type Constraint[F any] interface { - // Accepts determines whether a given constraint accepts a given trace or - // not. If not, a failure is produced. Otherwise, a bitset indicating - // branch coverage is returned. - Accepts(trace.Trace[F], AnySchema[F], Context[F]) Failure + // Accepts determines whether a given (local) constraint accepts a given set + // of traces or not. If not, a failure is produced. Observe that, for + // global constraints, this is a no-op. + Accepts(trace.Trace[F], AnySchema[F], Context[F]) []Failure[F] // Determine the well-definedness bounds for this constraint in both the // negative (left) or positive (right) directions. For example, consider an // expression such as "(shift X -1)". This is technically undefined for the @@ -64,9 +64,9 @@ type Constraint[F any] interface { // whilst checking constraints. For example, it provides cached access to data // for lookups to prevent the need to recompute this for individual lookups. type Context[F any] interface { - // LookupSet returns a given module viewed as a set from the perspective of - // a given set of columns, with an optional selector. - Get(SetId) collection.Set[[]F] + // Get returns a given module viewed in a given shard as a set from the + // perspective of a given set of columns, with an optional selector. + Get(shard uint, id SetId) collection.Set[[]F] } // SetId provides a generic mechanism for referring to a particular set of data diff --git a/pkg/schema/constraint/bus/constraint.go b/pkg/schema/constraint/bus/constraint.go index 6edd58fa6..d8031f2bf 100644 --- a/pkg/schema/constraint/bus/constraint.go +++ b/pkg/schema/constraint/bus/constraint.go @@ -17,6 +17,7 @@ import ( "slices" "github.com/LFDT-Lineth/zkc/pkg/schema" + "github.com/LFDT-Lineth/zkc/pkg/schema/register" "github.com/LFDT-Lineth/zkc/pkg/trace" "github.com/LFDT-Lineth/zkc/pkg/util" "github.com/LFDT-Lineth/zkc/pkg/util/collection/hash" @@ -44,18 +45,14 @@ type Constraint[F field.Element[F]] struct { // NewConstraint creates a bus constraint, requiring all ports share one width. func NewConstraint[F field.Element[F]](handle string, sends []Port, receives []Port) Constraint[F] { var width uint - // - for i, ith := range sends { - if i != 0 && ith.Len() != width { - panic("inconsistent number of send registers on bus") - } - - width = ith.Len() - } - // - for _, ith := range receives { - if ith.Len() != width { - panic("inconsistent number of receive registers on bus") + // Take the width from whichever side has ports, rather than from the sends + // alone. A bus missing one direction entirely is a user error reported by + // Consistent, so it must not panic here. + for i, ith := range slices.Concat(sends, receives) { + if i == 0 { + width = ith.Len() + } else if ith.Len() != width { + panic(fmt.Sprintf("inconsistent port widths on bus %q (%d vs %d)", handle, width, ith.Len())) } } @@ -134,19 +131,13 @@ func (p Constraint[F]) Bounds(module uint) util.Bounds { return util.EMPTY_BOUND } -// Accepts checks whether the bus balances within a single trace. -// -//nolint:revive -func (p Constraint[F]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F], ctx schema.Context[F]) schema.Failure { - return p.AcceptsGroup(tr) -} - -// AcceptsGroup checks whether the bus balances across a group of traces +// Accepts checks whether the bus balances across a group of traces // judged together. -func (p Constraint[F]) AcceptsGroup(traces ...trace.Trace[F]) schema.Failure { +func (p Constraint[F]) Accepts(trace trace.Trace[F], sc schema.AnySchema[F], ctx schema.Context[F], +) (failures []schema.Failure[F]) { tally := hash.NewMap[hash.Array[F], int](32) // - for _, tr := range traces { + for _, tr := range trace { p.accumulate(tr, p.Sends, tally, 1) p.accumulate(tr, p.Receives, tally, -1) } @@ -158,51 +149,43 @@ func (p Constraint[F]) AcceptsGroup(traces ...trace.Trace[F]) schema.Failure { if pair.Right != 0 { var ( message = pair.Left.Elements() - sent = p.count(traces, p.Sends, message) - received = p.count(traces, p.Receives, message) + sent = p.count(trace, p.Sends, message) + received = p.count(trace, p.Receives, message) ) // - return &Failure[F]{p.Handle, message, sent, received, p.Sends, p.Receives} + failures = append(failures, &Failure[F]{p.Handle, message, sent, received, p.Sends, p.Receives}) } } // - return nil -} - -// NetTally computes one trace's tally (sends minus receives), allowing a -// checking harness to combine shards by addition. -func (p Constraint[F]) NetTally(tr trace.Trace[F]) *Tally[F] { - tally := hash.NewMap[hash.Array[F], int](32) - // - p.accumulate(tr, p.Sends, tally, 1) - p.accumulate(tr, p.Receives, tally, -1) - // - return tally + return failures } // accumulate adds the given sign to the tally for every selected row of each // port. -func (p Constraint[F]) accumulate(tr trace.Trace[F], ports []Port, tally *Tally[F], sign int) { +func (p Constraint[F]) accumulate(tr trace.Shard[F], ports []Port, tally *Tally[F], sign int) { + // add is the tally update applied to each selected row. + var add = func(count int) int { return count + sign } + // for _, port := range ports { var trModule = tr.Module(port.Module) + // Allocate scratch space for this port. + var buffer = make([]F, port.Len()) // for row := range trModule.Height() { - if trModule.Column(port.Selector.Unwrap()).Get(row).IsZero() { - continue - } - // - var message = make([]F, port.Len()) - // - for i, rid := range port.Registers { - message[i] = trModule.Column(rid.Unwrap()).Get(row) + if isSelected(row, port.Selector, trModule) { + // + for i, rid := range port.Registers { + buffer[i] = trModule.Column(rid.Unwrap()).Get(row) + } + // + var key = hash.NewArray(buffer) + // Insert item whilst checking whether the buffer was consumed or not + if !tally.Update(key, add, sign) { + // Yes, buffer consumed. Therefore, construct fresh buffer to avoid + // aliasing the value now stored in the hash set. + buffer = slices.Clone(buffer) + } } - // - var ( - key = hash.NewArray(message) - count, _ = tally.Get(key) - ) - // - tally.Insert(key, count+sign) } } } @@ -210,7 +193,7 @@ func (p Constraint[F]) accumulate(tr trace.Trace[F], ports []Port, tally *Tally[ // count returns how many times the given message is contributed by the given // ports across all traces. This rescans the traces, which is fine since it // only ever runs when reporting a failure. -func (p Constraint[F]) count(traces []trace.Trace[F], ports []Port, message []F) uint { +func (p Constraint[F]) count(traces trace.Trace[F], ports []Port, message []F) uint { var n uint // for _, tr := range traces { @@ -218,21 +201,19 @@ func (p Constraint[F]) count(traces []trace.Trace[F], ports []Port, message []F) var trModule = tr.Module(port.Module) // for row := range trModule.Height() { - if trModule.Column(port.Selector.Unwrap()).Get(row).IsZero() { - continue - } - // - var matches = true - // - for i, rid := range port.Registers { - if !trModule.Column(rid.Unwrap()).Get(row).Equals(message[i]) { - matches = false - break + if isSelected(row, port.Selector, trModule) { + var matches = true + // + for i, rid := range port.Registers { + if !trModule.Column(rid.Unwrap()).Get(row).Equals(message[i]) { + matches = false + break + } + } + // + if matches { + n++ } - } - // - if matches { - n++ } } } @@ -265,3 +246,11 @@ func (p Constraint[F]) Lisp(mapping schema.AnySchema[F]) sexp.SExp { receives, }) } + +// isSelected determines whether or not the given row of the given vector is +// selected. A row without a selector is always selected; otherwise, it is +// selected when its selector is non-zero. +func isSelected[F field.Element[F]](k uint, id register.Id, trModule trace.Module[F]) bool { + // Otherwise, selected when selector non-zero. + return !trModule.Column(id.Unwrap()).Get(k).IsZero() +} diff --git a/pkg/schema/constraint/bus/constraint_test.go b/pkg/schema/constraint/bus/constraint_test.go deleted file mode 100644 index fdb4f2698..000000000 --- a/pkg/schema/constraint/bus/constraint_test.go +++ /dev/null @@ -1,237 +0,0 @@ -// Copyright Consensys Software Inc. -// -// Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with -// the License. You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on -// an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the -// specific language governing permissions and limitations under the License. -// -// SPDX-License-Identifier: Apache-2.0 -package bus_test - -import ( - "testing" - - sc "github.com/LFDT-Lineth/zkc/pkg/schema" - "github.com/LFDT-Lineth/zkc/pkg/schema/constraint/bus" - "github.com/LFDT-Lineth/zkc/pkg/schema/register" - "github.com/LFDT-Lineth/zkc/pkg/trace" - "github.com/LFDT-Lineth/zkc/pkg/util" - "github.com/LFDT-Lineth/zkc/pkg/util/field" - "github.com/LFDT-Lineth/zkc/pkg/util/field/gf251" -) - -// F is the field used throughout these tests (any field would do). -type F = gf251.Element - -// Compile-time check that a bus constraint satisfies the constraint interface. -var _ sc.Constraint[F] = bus.Constraint[F]{} - -// These tests exercise the multiset mechanics of the bus constraint -// in isolation, using hand-built traces. End-to-end coverage (source -// declarations, lowering, padding, field iteration) comes from the -// Test_Valid_Bus_* / Test_Invalid_Bus_* fixtures under testdata/corset/. - -// Every module in these tests has three columns (SEL, A, B), where SEL is the -// selector and (A, B) the message. onePort describes such a module's port. -func onePort(module sc.ModuleId) bus.Port { - return bus.NewPort(module, columnId(0), columnId(1), columnId(2)) -} - -// xfer constructs the standard bus used by most tests below: module 0 sends -// and module 1 receives. -func xfer() bus.Constraint[F] { - return bus.NewConstraint[F]("xfer", []bus.Port{onePort(0)}, []bus.Port{onePort(1)}) -} - -func Test_Bus_Balanced(t *testing.T) { - tr := newTrace( - newModule("alpha", row(1, 5, 7), row(0, 0, 0), row(1, 9, 2)), - newModule("beta", row(1, 9, 2), row(1, 5, 7))) - // - if failure := xfer().AcceptsGroup(tr); failure != nil { - t.Errorf("balanced bus rejected: %s", failure.Message()) - } -} - -func Test_Bus_EmptyIsBalanced(t *testing.T) { - // A bus on which nothing is sent or received balances trivially, even - // when the participating modules have (unselected) rows. - tr := newTrace( - newModule("alpha", row(0, 1, 2)), - newModule("beta")) - // - if failure := xfer().AcceptsGroup(tr); failure != nil { - t.Errorf("empty bus rejected: %s", failure.Message()) - } -} - -func Test_Bus_Duplicates(t *testing.T) { - // Two identical sends require two identical receives: one is not enough. - // This is exactly what distinguishes a bus from a (de-duplicating) - // lookup. - unbalanced := newTrace( - newModule("alpha", row(1, 5, 7), row(1, 5, 7)), - newModule("beta", row(1, 5, 7))) - balanced := newTrace( - newModule("alpha", row(1, 5, 7), row(1, 5, 7)), - newModule("beta", row(1, 5, 7), row(1, 5, 7))) - // - failure := xfer().AcceptsGroup(unbalanced) - if failure == nil { - t.Errorf("bus with 2 sends vs 1 receive accepted") - } else if f := failure.(*bus.Failure[F]); f.Sent != 2 || f.Received != 1 { - t.Errorf("wrong counts reported: sent %d, received %d", f.Sent, f.Received) - } - // - if failure := xfer().AcceptsGroup(balanced); failure != nil { - t.Errorf("bus with 2 sends vs 2 receives rejected: %s", failure.Message()) - } -} - -func Test_Bus_SelectorZeroInert(t *testing.T) { - // Junk payloads on rows whose selector is zero contribute nothing. This - // is what makes (all-zero) padding rows harmless. - tr := newTrace( - newModule("alpha", row(1, 5, 7), row(0, 123, 250)), - newModule("beta", row(0, 88, 99), row(1, 5, 7))) - // - if failure := xfer().AcceptsGroup(tr); failure != nil { - t.Errorf("junk on unselected rows unbalanced the bus: %s", failure.Message()) - } -} - -func Test_Bus_ReceiveNeverSent(t *testing.T) { - tr := newTrace( - newModule("alpha", row(1, 5, 7)), - newModule("beta", row(1, 5, 7), row(1, 8, 1))) - // - failure := xfer().AcceptsGroup(tr) - if failure == nil { - t.Errorf("bus with an unsent message accepted") - } else if f := failure.(*bus.Failure[F]); f.Sent != 0 || f.Received != 1 { - t.Errorf("wrong counts reported: sent %d, received %d", f.Sent, f.Received) - } -} - -func Test_Bus_FanInFanOut(t *testing.T) { - // Four modules on one bus: two senders (modules 0, 1), two receivers - // (modules 2, 3). Messages from different senders are answered by - // different receivers, and one message is duplicated across senders. - manyPorts := bus.NewConstraint[F]("many", - []bus.Port{onePort(0), onePort(1)}, - []bus.Port{onePort(2), onePort(3)}) - // - balanced := newTrace( - newModule("s1", row(1, 5, 7), row(1, 4, 4)), - newModule("s2", row(1, 9, 2), row(1, 4, 4)), - newModule("r1", row(1, 4, 4), row(1, 9, 2)), - newModule("r2", row(1, 4, 4), row(1, 5, 7))) - // As above, except one copy of the duplicated message (4,4) is missing. - unbalanced := newTrace( - newModule("s1", row(1, 5, 7), row(1, 4, 4)), - newModule("s2", row(1, 9, 2), row(1, 4, 4)), - newModule("r1", row(1, 4, 4), row(1, 9, 2)), - newModule("r2", row(0, 4, 4), row(1, 5, 7))) - // - if failure := manyPorts.AcceptsGroup(balanced); failure != nil { - t.Errorf("balanced fan-in/fan-out bus rejected: %s", failure.Message()) - } - // - if manyPorts.AcceptsGroup(unbalanced) == nil { - t.Errorf("fan-in/fan-out bus missing one duplicate accepted") - } -} - -func Test_Bus_Group(t *testing.T) { - // Shard 1 only sends; shard 2 only receives. Together they balance, - // alone they do not. - shard1 := newTrace( - newModule("alpha", row(1, 5, 7), row(1, 9, 2)), - newModule("beta", row(0, 0, 0))) - shard2 := newTrace( - newModule("alpha", row(0, 0, 0)), - newModule("beta", row(1, 9, 2), row(1, 5, 7))) - // - if failure := xfer().AcceptsGroup(shard1, shard2); failure != nil { - t.Errorf("balanced group rejected: %s", failure.Message()) - } - // - if xfer().AcceptsGroup(shard1) == nil { - t.Errorf("unbalanced shard accepted on its own") - } - // Accepts must agree with a group of one. - if xfer().Accepts(shard1, nil, nil) == nil { - t.Errorf("Accepts disagrees with AcceptsGroup on a single trace") - } -} - -func Test_Bus_GroupDuplicates(t *testing.T) { - // A message sent twice in shard 1 is balanced by one receive in shard 1 - // and one in shard 2 — counts pool across the whole group. - shard1 := newTrace( - newModule("alpha", row(1, 5, 7), row(1, 5, 7)), - newModule("beta", row(1, 5, 7))) - shard2 := newTrace( - newModule("alpha"), - newModule("beta", row(1, 5, 7))) - // - if failure := xfer().AcceptsGroup(shard1, shard2); failure != nil { - t.Errorf("group balancing duplicates across shards rejected: %s", failure.Message()) - } - // A third copy of the receive tips the balance over. - shard3 := newTrace( - newModule("alpha"), - newModule("beta", row(1, 5, 7))) - // - if xfer().AcceptsGroup(shard1, shard2, shard3) == nil { - t.Errorf("group with 2 sends vs 3 receives accepted") - } -} - -// ============================================================================ -// Test helpers -// ============================================================================ - -// columnId is shorthand for constructing a column (i.e. register) identifier. -func columnId(index uint) register.Id { - return register.NewId(index) -} - -// row is shorthand for one row of column values. -func row(values ...uint64) []uint64 { - return values -} - -// newTrace constructs a trace from the given modules; each module's position -// determines its module identifier. -func newTrace(modules ...*trace.CompactModule[F]) trace.Trace[F] { - return trace.NewArray(modules) -} - -// newModule constructs a module with columns (SEL, A, B) holding the given -// rows, where SEL acts as the selector. -func newModule(name string, rows ...[]uint64) *trace.CompactModule[F] { - var columns []trace.ColumnDescriptor - // - for _, col := range []string{"SEL", "A", "B"} { - columns = append(columns, trace.NewColumnDescriptor(col, util.None[uint]())) - } - // - mod := trace.InitCompactModule[F](trace.NewModuleDescriptor(name, columns)) - // - for _, values := range rows { - var elements []F - // - for _, v := range values { - elements = append(elements, field.Uint64[F](v)) - } - // - mod.Append(elements...) - } - // - return mod -} diff --git a/pkg/schema/constraint/bus/failure.go b/pkg/schema/constraint/bus/failure.go index 073069cda..15664f34a 100644 --- a/pkg/schema/constraint/bus/failure.go +++ b/pkg/schema/constraint/bus/failure.go @@ -17,6 +17,7 @@ import ( "strings" "github.com/LFDT-Lineth/zkc/pkg/trace" + tr "github.com/LFDT-Lineth/zkc/pkg/trace" "github.com/LFDT-Lineth/zkc/pkg/util/collection/set" "github.com/LFDT-Lineth/zkc/pkg/util/field" ) @@ -24,7 +25,7 @@ import ( // Failure records a message sent and received a differing number of times. type Failure[F field.Element[F]] struct { // Handle (i.e. bus name) of the failing constraint - Handle string + Bus string // Unbalanced is the offending message Unbalanced []F // Sent is the number of times the message was sent @@ -37,6 +38,11 @@ type Failure[F field.Element[F]] struct { Receives []Port } +// Handle implementation of schema.Failure interface +func (p *Failure[F]) Handle() string { + return p.Bus +} + // Message provides a suitable error message func (p *Failure[F]) Message() string { var builder strings.Builder @@ -50,7 +56,7 @@ func (p *Failure[F]) Message() string { } // return fmt.Sprintf("bus \"%s\" unbalanced: message (%s) sent %d time(s), received %d time(s)", - p.Handle, builder.String(), p.Sent, p.Received) + p.Handle(), builder.String(), p.Sent, p.Received) } func (p *Failure[F]) String() string { @@ -60,23 +66,27 @@ func (p *Failure[F]) String() string { // RequiredCells identifies the cells contributing the offending message // (selectors included). Rescanning the trace is fine here, as this only ever // runs on a failure. -func (p *Failure[F]) RequiredCells(tr trace.Trace[F]) *set.AnySortedSet[trace.CellRef] { - res := set.NewAnySortedSet[trace.CellRef]() - // - for _, port := range p.Sends { - p.requiredCellsOfPort(tr, port, res) - } +func (p *Failure[F]) RequiredCells(trace tr.Trace[F]) set.AnySortedSet[tr.ShardedCellRef] { + res := set.NewAnySortedSet[tr.ShardedCellRef]() // - for _, port := range p.Receives { - p.requiredCellsOfPort(tr, port, res) + for shard, tr := range trace { + for _, port := range p.Sends { + p.requiredCellsOfPort(uint(shard), tr, port, res) + } + // + for _, port := range p.Receives { + p.requiredCellsOfPort(uint(shard), tr, port, res) + } } // - return res + return *res } // requiredCellsOfPort adds the cells of the port's selected rows holding the // offending message. -func (p *Failure[F]) requiredCellsOfPort(tr trace.Trace[F], port Port, res *set.AnySortedSet[trace.CellRef]) { +func (p *Failure[F]) requiredCellsOfPort(shard uint, tr trace.Shard[F], port Port, + res *set.AnySortedSet[trace.ShardedCellRef]) { + // var trModule = tr.Module(port.Module) // for row := range trModule.Height() { @@ -95,11 +105,11 @@ func (p *Failure[F]) requiredCellsOfPort(tr trace.Trace[F], port Port, res *set. // if matches { selRef := trace.NewColumnRef(port.Module, port.Selector) - res.Insert(trace.NewCellRef(selRef, int(row))) + res.Insert(trace.NewShardedCellRef(shard, selRef, int(row))) // for _, rid := range port.Registers { ref := trace.NewColumnRef(port.Module, rid) - res.Insert(trace.NewCellRef(ref, int(row))) + res.Insert(trace.NewShardedCellRef(shard, ref, int(row))) } } } diff --git a/pkg/schema/constraint/failure.go b/pkg/schema/constraint/failure.go index 6b915512b..19640083d 100644 --- a/pkg/schema/constraint/failure.go +++ b/pkg/schema/constraint/failure.go @@ -15,7 +15,6 @@ package constraint import ( "fmt" - "github.com/LFDT-Lineth/zkc/pkg/ir/term" "github.com/LFDT-Lineth/zkc/pkg/schema" "github.com/LFDT-Lineth/zkc/pkg/trace" "github.com/LFDT-Lineth/zkc/pkg/util/collection/set" @@ -30,17 +29,20 @@ type InternalFailure[F any] struct { context schema.ModuleId // Row on which the constraint failed row uint - // Cells involved (if any) - term term.Contextual // Error message error string } // NewInternalFailure constructs a new internal failure object. -func NewInternalFailure[F any](handle string, ctx schema.ModuleId, row uint, term term.Contextual, +func NewInternalFailure[F any](handle string, ctx schema.ModuleId, row uint, err string) *InternalFailure[F] { // - return &InternalFailure[F]{handle, ctx, row, term, err} + return &InternalFailure[F]{handle, ctx, row, err} +} + +// Handle implementation for schema.Failure interface. +func (p *InternalFailure[F]) Handle() string { + return p.handle } // Error provides a suitable error message @@ -54,10 +56,6 @@ func (p *InternalFailure[F]) Message() string { } // RequiredCells identifies the cells required to evaluate the failing constraint at the failing row. -func (p *InternalFailure[F]) RequiredCells(tr trace.Trace[F]) *set.AnySortedSet[trace.CellRef] { - if p.term != nil { - return p.term.RequiredCells(int(p.row), p.context) - } - // Empty set - return set.NewAnySortedSet[trace.CellRef]() +func (p *InternalFailure[F]) RequiredCells(_ trace.Trace[F]) set.AnySortedSet[trace.ShardedCellRef] { + return nil } diff --git a/pkg/schema/constraint/lookup/constraint.go b/pkg/schema/constraint/lookup/constraint.go index e0adc774d..5c44e40ff 100644 --- a/pkg/schema/constraint/lookup/constraint.go +++ b/pkg/schema/constraint/lookup/constraint.go @@ -136,10 +136,23 @@ func (p Constraint[F]) Bounds(module uint) util.Bounds { // all rows of the source columns. // //nolint:revive -func (p Constraint[F]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F], ctx schema.Context[F]) schema.Failure { +func (p Constraint[F]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F], ctx schema.Context[F], +) (failures []schema.Failure[F]) { + // + for i, ith := range tr { + if f := p.accepts(uint(i), ith, sc, ctx); f != nil { + failures = append(failures, f) + } + } + // + return failures +} + +func (p Constraint[F]) accepts(shard uint, tr trace.Shard[F], sc schema.AnySchema[F], ctx schema.Context[F], +) schema.Failure[F] { var ( // Load target sets - targets = loadSets(ctx, p.Targets...) + targets = loadSets(shard, ctx, p.Targets...) // Initialise read buffer buffer = make([]F, p.Sources[0].Len()) ) @@ -147,7 +160,7 @@ func (p Constraint[F]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F], ctx sc for _, source := range p.Sources { var trModule = tr.Module(source.Module) // Check each row in the set determined by this vector. - if err := p.checkSourceSet(source.SetId(), trModule, targets, buffer); err != nil { + if err := p.checkSourceSet(source.SetId(), shard, trModule, targets, buffer); err != nil { return err } } @@ -190,14 +203,15 @@ func (p Constraint[F]) Substitute(mapping map[string]F) { // Check that all rows in a given source set are contained within at least one // of the given target sets. -func (p Constraint[F]) checkSourceSet(src SetId, mod trace.Module[F], sets []Set[[]F], buffer []F) schema.Failure { +func (p Constraint[F]) checkSourceSet(src SetId, shard uint, mod trace.Module[F], sets []Set[[]F], + buffer []F) schema.Failure[F] { if src.HasSelector() { var selector = src.Selector().Unwrap() // for row := range mod.Height() { if !mod.Column(selector).Get(row).IsZero() { if !contains(row, src, mod, sets, buffer) { - return &Failure[F]{p.Handle, src, row} + return &Failure[F]{p.Handle, src, row, shard} } } } @@ -205,7 +219,7 @@ func (p Constraint[F]) checkSourceSet(src SetId, mod trace.Module[F], sets []Set // Optimised path when no selector for row := range mod.Height() { if !contains(row, src, mod, sets, buffer) { - return &Failure[F]{p.Handle, src, row} + return &Failure[F]{p.Handle, src, row, shard} } } } @@ -234,13 +248,13 @@ func contains[F field.Element[F]](row uint, src SetId, mod trace.Module[F], sets } // Load those sets from the context corresponding to the given vectors. -func loadSets[F field.Element[F]](ctx schema.Context[F], vecs ...Vector) []Set[[]F] { +func loadSets[F field.Element[F]](shard uint, ctx schema.Context[F], vecs ...Vector) []Set[[]F] { var ( sets = make([]Set[[]F], len(vecs)) ) // Load target sets for i, v := range vecs { - sets[i] = ctx.Get(v.SetId()) + sets[i] = ctx.Get(shard, v.SetId()) } // return sets diff --git a/pkg/schema/constraint/lookup/failure.go b/pkg/schema/constraint/lookup/failure.go index 23b2d015c..be7e762e4 100644 --- a/pkg/schema/constraint/lookup/failure.go +++ b/pkg/schema/constraint/lookup/failure.go @@ -23,16 +23,23 @@ import ( // Failure provides structural information about a failing lookup constraint. type Failure[F any] struct { // Handle of the failing constraint - Handle string + LookupHandle string // SourceId gives the set identifier of the source SourceId schema.SetId // Row on which the constraint failed Row uint + // Shard on which the constraint failed + Shard uint +} + +// Handle implementation of schema.Failure interface +func (p *Failure[F]) Handle() string { + return p.LookupHandle } // Message provides a suitable error message func (p *Failure[F]) Message() string { - return fmt.Sprintf("lookup \"%s\" failed (row %d)", p.Handle, p.Row) + return fmt.Sprintf("lookup \"%s\" failed (row %d, shard %d)", p.Handle(), p.Row, p.Shard) } func (p *Failure[F]) String() string { @@ -40,15 +47,15 @@ func (p *Failure[F]) String() string { } // RequiredCells identifies the cells required to evaluate the failing constraint at the failing row. -func (p *Failure[F]) RequiredCells(_ trace.Trace[F]) *set.AnySortedSet[trace.CellRef] { - res := set.NewAnySortedSet[trace.CellRef]() +func (p *Failure[F]) RequiredCells(_ trace.Trace[F]) set.AnySortedSet[trace.ShardedCellRef] { + res := set.NewAnySortedSet[trace.ShardedCellRef]() // Handle registers for i := range p.SourceId.Width() { var rid = p.SourceId.Ith(i) // ref := trace.NewColumnRef(p.SourceId.Module(), rid) - res.Insert(trace.NewCellRef(ref, int(p.Row))) + res.Insert(trace.NewShardedCellRef(p.Shard, ref, int(p.Row))) } // - return res + return *res } diff --git a/pkg/schema/constraint/lookup/geometry.go b/pkg/schema/constraint/lookup/geometry.go index fc60236a2..3a1c3b667 100644 --- a/pkg/schema/constraint/lookup/geometry.go +++ b/pkg/schema/constraint/lookup/geometry.go @@ -23,7 +23,7 @@ import ( // a lookup where (X Y) looksup into (A B). Suppose X is 16bit and Y is 32bit, // whilst A is 64bit and B is 8bit. Then, the geometry of the lookup is [16,32]. type Geometry struct { - config field.Config + //config field.Config // bitwidth for each source/target pairing geometry []uint } @@ -43,28 +43,28 @@ func NewGeometry[F field.Element[F], T register.Map](c Constraint[F], mapping mo updateGeometry(geometry, target, mapping) } // - return Geometry{mapping.Field(), geometry} + return Geometry{geometry} } // BandWidth returns maximum field bandwidth available in the field. -func (p *Geometry) BandWidth() uint { - return p.config.BandWidth -} +// func (p *Geometry) BandWidth() uint { +// return p.config.BandWidth +// } -// RegisterWidth returns maximum permitted register width for the field. -func (p *Geometry) RegisterWidth() uint { - return p.config.RegisterWidth -} +// // RegisterWidth returns maximum permitted register width for the field. +// func (p *Geometry) RegisterWidth() uint { +// return p.config.RegisterWidth +// } -// LimbWidths returns the bitwidths for the required limbs for a given -// source/target pairing in the lookup. -func (p *Geometry) LimbWidths(i uint) []uint { - if p.geometry[i] == 0 { - return nil - } - // - return register.LimbWidths(p.config.RegisterWidth, p.geometry[i]) -} +// // LimbWidths returns the bitwidths for the required limbs for a given +// // source/target pairing in the lookup. +// func (p *Geometry) LimbWidths(i uint) []uint { +// if p.geometry[i] == 0 { +// return nil +// } +// // +// return register.LimbWidths(p.config.RegisterWidth, p.geometry[i]) +// } func updateGeometry[T register.Map](geometry []uint, source Vector, mapping module.Map[T]) { // diff --git a/pkg/schema/constraint/ranged/constraint.go b/pkg/schema/constraint/ranged/constraint.go index 79095024e..8da495f58 100644 --- a/pkg/schema/constraint/ranged/constraint.go +++ b/pkg/schema/constraint/ranged/constraint.go @@ -100,14 +100,18 @@ func (p Constraint[F]) Bounds(module uint) util.Bounds { // nil otherwise return an error. // //nolint:revive -func (p Constraint[F]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F], _ schema.Context[F]) schema.Failure { - for i := range p.Sources { - if err := p.accepts(i, tr); err != nil { - return err +func (p Constraint[F]) Accepts(trace trace.Trace[F], sc schema.AnySchema[F], _ schema.Context[F], +) (failures []schema.Failure[F]) { + // + for shard, tr := range trace { + for i := range p.Sources { + if err := p.accepts(i, uint(shard), tr); err != nil { + failures = append(failures, err) + } } } - // All good - return nil + // done + return failures } // Lisp converts this schema element into a simple S-Expression, for example so @@ -135,7 +139,7 @@ func (p Constraint[F]) Lisp(mapping schema.AnySchema[F]) sexp.SExp { // accepts checks the ith register of this constraint holds within its // corresponding bound on every row of the enclosing module. -func (p Constraint[F]) accepts(i int, tr trace.Trace[F]) schema.Failure { +func (p Constraint[F]) accepts(i int, shard uint, tr trace.Shard[F]) schema.Failure[F] { var ( trModule = tr.Module(p.Context) handle = constraint.DetermineHandle(p.Handle, p.Context, tr) @@ -150,7 +154,7 @@ func (p Constraint[F]) accepts(i int, tr trace.Trace[F]) schema.Failure { // Perform the range check if column.Get(k).Cmp(bound) >= 0 { // Evaluation failure - return &Failure[F]{handle, p.Context, source, bitwidth, k} + return &Failure[F]{handle, p.Context, source, bitwidth, k, shard} } } // All good diff --git a/pkg/schema/constraint/ranged/failure.go b/pkg/schema/constraint/ranged/failure.go index 650c0c124..b85a0a64a 100644 --- a/pkg/schema/constraint/ranged/failure.go +++ b/pkg/schema/constraint/ranged/failure.go @@ -24,7 +24,7 @@ import ( // Failure provides structural information about a failing type constraint. type Failure[F any] struct { // Handle of the failing constraint - Handle string + RangeHandle string // Enclosing context Context schema.ModuleId // Constrained register @@ -33,12 +33,19 @@ type Failure[F any] struct { Bitwidth uint // Row on which the constraint failed Row uint + // Shard on which the constraint failed + Shard uint +} + +// Handle implementation of schema.Failure interface +func (p *Failure[F]) Handle() string { + return p.RangeHandle } // Message provides a suitable error message func (p *Failure[F]) Message() string { // Construct useful error message - return fmt.Sprintf("range \"%s\" is u%d does not hold (row %d)", p.Handle, p.Bitwidth, p.Row) + return fmt.Sprintf("range \"%s\" is u%d does not hold (row %d, shard %d)", p.Handle(), p.Bitwidth, p.Row, p.Shard) } func (p *Failure[F]) String() string { @@ -46,13 +53,13 @@ func (p *Failure[F]) String() string { } // RequiredCells identifies the cells required to evaluate the failing constraint at the failing row. -func (p *Failure[F]) RequiredCells(_ trace.Trace[F]) *set.AnySortedSet[trace.CellRef] { +func (p *Failure[F]) RequiredCells(_ trace.Trace[F]) set.AnySortedSet[trace.ShardedCellRef] { var ( - res = set.NewAnySortedSet[trace.CellRef]() + res = set.NewAnySortedSet[trace.ShardedCellRef]() ref = trace.NewColumnRef(p.Context, p.Source) ) // - res.Insert(trace.NewCellRef(ref, int(p.Row))) + res.Insert(trace.NewShardedCellRef(p.Shard, ref, int(p.Row))) // - return res + return *res } diff --git a/pkg/schema/constraint/util.go b/pkg/schema/constraint/util.go index fcc4f30e5..7a2ccde6f 100644 --- a/pkg/schema/constraint/util.go +++ b/pkg/schema/constraint/util.go @@ -49,7 +49,7 @@ func CheckConsistent[F any, E term.Contextual](module uint, schema schema.AnySch // DetermineHandle is a very simple helper which determines a suitable qualified // name for the given constraint handle. -func DetermineHandle[F any](handle string, ctx schema.ModuleId, tr trace.Trace[F]) string { +func DetermineHandle[F any](handle string, ctx schema.ModuleId, tr trace.Shard[F]) string { modName := tr.Module(ctx).Name() // return trace.QualifiedColumnName(modName, handle) diff --git a/pkg/schema/constraint/vanishing/constraint.go b/pkg/schema/constraint/vanishing/constraint.go index 6c33902eb..262b7128f 100644 --- a/pkg/schema/constraint/vanishing/constraint.go +++ b/pkg/schema/constraint/vanishing/constraint.go @@ -98,7 +98,19 @@ func (p Constraint[F, T]) Bounds(module uint) util.Bounds { // of a table. If so, return nil otherwise return an error. // //nolint:revive -func (p Constraint[F, T]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F], _ schema.Context[F]) schema.Failure { +func (p Constraint[F, T]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F], _ schema.Context[F], +) (failures []schema.Failure[F]) { + // + for i, ith := range tr { + if f := p.accepts(uint(i), ith, sc); f != nil { + failures = append(failures, f) + } + } + // + return failures +} + +func (p Constraint[F, T]) accepts(shard uint, tr trace.Shard[F], sc schema.AnySchema[F]) schema.Failure[F] { var ( // Handle is used for error reporting. handle = constraint.DetermineHandle(p.Handle, p.Context, tr) @@ -109,7 +121,7 @@ func (p Constraint[F, T]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F], _ s // if p.Domain.IsEmpty() { // Global Constraint - return HoldsGlobally(handle, p.Context, p.Constraint, trModule, scModule) + return HoldsGlobally(handle, p.Context, p.Constraint, shard, trModule, scModule) } // Extract domain domain := p.Domain.Unwrap() @@ -125,13 +137,13 @@ func (p Constraint[F, T]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F], _ s start = uint(domain) } // Check specific row - return HoldsLocally(start, handle, p.Constraint, p.Context, trModule, scModule) + return HoldsLocally(start, handle, p.Constraint, p.Context, shard, trModule, scModule) } // HoldsGlobally checks whether a given expression vanishes (i.e. evaluates to // zero) for all rows of a trace. If not, report an appropriate error. func HoldsGlobally[F field.Element[F], T term.Testable[F]](handle string, ctx schema.ModuleId, constraint T, - trMod trace.Module[F], scMod schema.Module[F]) schema.Failure { + shard uint, trMod trace.Module[F], scMod schema.Module[F]) schema.Failure[F] { // var ( // Determine height of enclosing module @@ -143,7 +155,7 @@ func HoldsGlobally[F field.Element[F], T term.Testable[F]](handle string, ctx sc if bounds.End < height { // Check all in-bounds values for k := bounds.Start; k < (height - bounds.End); k++ { - err := HoldsLocally(k, handle, constraint, ctx, trMod, scMod) + err := HoldsLocally(k, handle, constraint, ctx, shard, trMod, scMod) if err != nil { return err } @@ -156,15 +168,15 @@ func HoldsGlobally[F field.Element[F], T term.Testable[F]](handle string, ctx sc // HoldsLocally checks whether a given constraint holds (e.g. vanishes) on a // specific row of a trace. If not, report an appropriate error. func HoldsLocally[F field.Element[F], T term.Testable[F]](k uint, handle string, term T, ctx schema.ModuleId, - trMod trace.Module[F], scMod schema.Module[F]) schema.Failure { + shard uint, trMod trace.Module[F], scMod schema.Module[F]) schema.Failure[F] { // ok, _, err := term.TestAt(k, trMod, scMod) // Check for errors if err != nil { - return constraint.NewInternalFailure[F](handle, ctx, k, term, err.Error()) + return constraint.NewInternalFailure[F](handle, ctx, k, err.Error()) } else if !ok { // Evaluation failure - return &Failure[F]{handle, term, ctx, k} + return &Failure[F]{handle, term, ctx, k, shard} } // Success return nil diff --git a/pkg/schema/constraint/vanishing/failure.go b/pkg/schema/constraint/vanishing/failure.go index 19171ec56..b739f4b49 100644 --- a/pkg/schema/constraint/vanishing/failure.go +++ b/pkg/schema/constraint/vanishing/failure.go @@ -18,30 +18,42 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/ir/term" "github.com/LFDT-Lineth/zkc/pkg/schema" "github.com/LFDT-Lineth/zkc/pkg/trace" + "github.com/LFDT-Lineth/zkc/pkg/util/collection/array" "github.com/LFDT-Lineth/zkc/pkg/util/collection/set" ) // Failure provides structural information about a failing vanishing constraint. type Failure[F any] struct { // Handle of the failing constraint - Handle string + VanishingHandle string // Constraint expression Constraint term.Testable[F] // Module where constraint failed Context schema.ModuleId // Row on which the constraint failed Row uint + // Shard on which the constraint failed + Shard uint +} + +// Handle implementation of schema.Failure interface +func (p *Failure[F]) Handle() string { + return p.VanishingHandle } // Message provides a suitable error message func (p *Failure[F]) Message() string { // Construct useful error message - return fmt.Sprintf("constraint \"%s\" does not hold (row %d)", p.Handle, p.Row) + return fmt.Sprintf("constraint \"%s\" does not hold (row %d, shard %d)", p.Handle(), p.Row, p.Shard) } // RequiredCells identifies the cells required to evaluate the failing constraint at the failing row. -func (p *Failure[F]) RequiredCells(tr trace.Trace[F]) *set.AnySortedSet[trace.CellRef] { - return p.Constraint.RequiredCells(int(p.Row), p.Context) +func (p *Failure[F]) RequiredCells(_ trace.Trace[F]) set.AnySortedSet[trace.ShardedCellRef] { + var cells = p.Constraint.RequiredCells(int(p.Row), p.Context) + // Convert from cell ref into sharded cell ref + return array.Map(cells.ToArray(), func(_ uint, r trace.CellRef) trace.ShardedCellRef { + return trace.NewShardedCellRef(p.Shard, r.Column, r.Row) + }) } func (p *Failure[F]) String() string { diff --git a/pkg/schema/context.go b/pkg/schema/context.go index 4b0c8a472..21514f1ce 100644 --- a/pkg/schema/context.go +++ b/pkg/schema/context.go @@ -15,7 +15,6 @@ package schema import ( "fmt" "iter" - "runtime" "slices" "github.com/LFDT-Lineth/zkc/pkg/trace" @@ -30,28 +29,10 @@ import ( // Set provides a convenient alias type Set[F field.Element[F]] = *hash.Set[hash.Array[F]] -// chunksPerWorker determines how many chunks, on average, each available -// processor should receive when building sets in parallel. Using more -// chunks than workers allows the workload to be rebalanced dynamically: a -// worker which finishes its chunks early can pick up further chunks, rather -// than sitting idle whilst a single large chunk is still being built -// elsewhere. -const chunksPerWorker = 10 - -// determineChunkSize computes a suitable chunk size for parallel set -// construction, based on the total number of candidate rows across all sets -// and the number of available processors. Aiming for chunksPerWorker chunks -// per processor balances parallelism against the overhead of the reduce -// phase (more, smaller chunks means more merging work later). -func determineChunkSize(totalRows uint) uint { - return max(1, totalRows/(uint(runtime.NumCPU())*chunksPerWorker)) -} - -// setChunk identifies a sub-range of rows within the set determined by a -// given SetId. -type setChunk struct { - id SetId - start, end uint +// ChunkId identifies a particular set within a given shard. +type ChunkId struct { + shard uint + id SetId } // SeqBuildContext constructs the context from a given schema and trace. @@ -59,20 +40,25 @@ type setChunk struct { // constructing their sets. NOTE: this is done sequentially func SeqBuildContext[F field.Element[F]](tr trace.Trace[F], sc AnySchema[F]) Context[F] { var ( - stats = util.NewPerfStats() - context = make(map[string]*hash.Set[hash.Array[F]]) - sids = determineSets(sc) + stats = util.NewPerfStats() + contexts []map[string]*hash.Set[hash.Array[F]] + sids = determineSets(sc) ) - // sequential set construction (as a single chunk per set) - for _, sid := range sids { - height := setHeight(sid, tr, sc) - // Construct data for this set - context[sid.String()] = buildSetChunk(setChunk{sid, 0, height}, tr, sc) + // Build context for each shard + for i := range tr { + var context = make(map[string]*hash.Set[hash.Array[F]]) + // sequential set construction (as a single chunk per set) + for _, sid := range sids { + // Construct data for this set + context[sid.String()] = buildSetChunk(ChunkId{uint(i), sid}, tr, sc) + } + // + contexts = append(contexts, context) } // - stats.Log(fmt.Sprintf("Building context (%d sets; sequential)", len(context))) + stats.Log(fmt.Sprintf("Building context (%d sets in sequence)", len(sids)*len(tr))) // - return contextImpl[F]{context} + return contextImpl[F]{contexts} } // ParBuildContext constructs the context from a given schema and trace, using @@ -83,36 +69,26 @@ func SeqBuildContext[F field.Element[F]](tr trace.Trace[F], sc AnySchema[F]) Con // "reduce" phase), which is likewise done in parallel across sets. func ParBuildContext[F field.Element[F]](tr trace.Trace[F], sc AnySchema[F]) Context[F] { var ( - stats = util.NewPerfStats() - context = make(map[string]*hash.Set[hash.Array[F]]) - sids = determineSets(sc) - chunks, counts = determineChunks(sids, tr, sc) - // map phase: build every chunk in parallel - partials = array.ParallelMap(chunks, func(_ uint, c setChunk) Set[F] { + stats = util.NewPerfStats() + contexts = make([]map[string]*hash.Set[hash.Array[F]], len(tr)) + chunks = determineChunks(tr, sc) + // build every chunk in parallel + sets = array.ParallelMap(chunks, func(_ uint, c ChunkId) Set[F] { return buildSetChunk(c, tr, sc) }) - // group chunk results by their originating set. Since chunks are - // generated in sids order (see determineChunks), the ith set's chunks - // form a contiguous run of counts[i] entries within partials. - groups = make([][]Set[F], len(sids)) ) - // - for i, offset := 0, uint(0); i < len(sids); i++ { - groups[i] = partials[offset : offset+counts[i]] - offset += counts[i] + // Initialise context for each shard + for i := range tr { + contexts[i] = make(map[string]*hash.Set[hash.Array[F]]) } - // reduce phase: merge the chunks of each set in parallel - merged := array.ParallelMap(sids, func(i uint, sid SetId) Set[F] { - return mergeSets(groups[i]) - }) - // - for i, sid := range sids { - context[sid.String()] = merged[i] + // Flattern individual sets into their shards + for i, chunk := range chunks { + contexts[chunk.shard][chunk.id.String()] = sets[i] } // - stats.Log(fmt.Sprintf("Building context (%d sets, %d chunks; parallel)", len(sids), len(chunks))) + stats.Log(fmt.Sprintf("Building context (%d sets in parallel)", len(chunks))) // - return contextImpl[F]{context} + return contextImpl[F]{contexts} } // determineChunks splits every set identified by sids into one or more @@ -125,75 +101,21 @@ func ParBuildContext[F field.Element[F]](tr trace.Trace[F], sc AnySchema[F]) Con // returns the number of chunks generated for each set (aligned with sids), so // callers can recover the chunks belonging to a given set without a map // lookup. -func determineChunks[F field.Element[F]](sids []SetId, tr trace.Trace[F], sc AnySchema[F]) ([]setChunk, []uint) { +func determineChunks[F field.Element[F]](tr trace.Trace[F], sc AnySchema[F]) []ChunkId { var ( - heights = make([]uint, len(sids)) - total uint + sids = determineSets(sc) + sets = make([]ChunkId, len(sids)*len(tr)) + index = 0 ) - // Determine height of every set, and the total number of rows overall. - for i, sid := range sids { - heights[i] = setHeight(sid, tr, sc) - total += heights[i] - } // - var ( - size = determineChunkSize(total) - chunks []setChunk - counts = make([]uint, len(sids)) - ) - // - for i, height := range heights { - if height == 0 { - chunks = append(chunks, setChunk{sids[i], 0, 0}) - counts[i] = 1 - - continue - } - // - for start := uint(0); start < height; start += size { - chunks = append(chunks, setChunk{sids[i], start, min(start+size, height)}) - counts[i]++ + for i := range tr { + for _, sid := range sids { + sets[index] = ChunkId{uint(i), sid} + index++ } } // - return chunks, counts -} - -// setHeight determines the number of candidate (static or dynamic) rows from -// which the given set is constructed. -func setHeight[F field.Element[F]](id SetId, tr trace.Trace[F], sc AnySchema[F]) uint { - scModule := sc.Module(id.Module()) - // - if scModule.IsStatic() { - return uint(len(scModule.StaticContents())) - } - // - return tr.Module(id.Module()).Height() -} - -// mergeSets combines one or more partial sets (constructed from disjoint -// row-range chunks of the same underlying set) into a single set. -func mergeSets[F field.Element[F]](partials []Set[F]) Set[F] { - // Common case: set was constructed as a single chunk. - if len(partials) == 1 { - return partials[0] - } - // - var size uint - // - for _, p := range partials { - size += p.Size() - } - // - merged := hash.NewSet[hash.Array[F]](size >> 4) - // - for _, p := range partials { - for v := range p.Iter() { - merged.Insert(v) - } - } - // - return merged + return sets } // DetermineSets extracts all unique set identifiers from lookup constraints. @@ -213,27 +135,30 @@ func determineSets[F field.Element[F]](sc AnySchema[F]) []SetId { // buildSetChunk constructs the (partial) set of rows determined by a given // chunk. -func buildSetChunk[F field.Element[F]](c setChunk, tr trace.Trace[F], sc AnySchema[F]) Set[F] { - scModule := sc.Module(c.id.Module()) +func buildSetChunk[F field.Element[F]](c ChunkId, tr trace.Trace[F], sc AnySchema[F]) Set[F] { + var ( + scModule = sc.Module(c.id.Module()) + trModule = tr[c.shard].Module(c.id.Module()) + ) // if scModule.IsStatic() { - return buildStaticSetChunk(c, scModule) + return buildStaticSetChunk(c.id, scModule) } // - return buildDynamicSetChunk(c, tr.Module(c.id.Module())) + return buildDynamicSetChunk(c.id, trModule) } -func buildStaticSetChunk[F field.Element[F]](c setChunk, sm Module[F]) Set[F] { +func buildStaticSetChunk[F field.Element[F]](id SetId, sm Module[F]) Set[F] { var ( - buffer = make([]F, c.id.Width()) - contents = sm.StaticContents()[c.start:c.end] - data = hash.NewSet[hash.Array[F]](uint(len(contents)) >> 4) + buffer = make([]F, id.Width()) + contents = sm.StaticContents() + data = hash.NewSet[hash.Array[F]](uint(len(contents))) ) // Insert all selected rows within this chunk for _, row := range contents { - if isStaticSelected(c.id, row) { + if isStaticSelected(id, row) { // Read each register of this vector - readStaticRegisters(c.id, row, buffer) + readStaticRegisters(id, row, buffer) // Insert item whilst checking whether the buffer was consumed or not if !data.Insert(hash.NewArray(buffer)) { // Yes, buffer consumed. Therefore, construct fresh buffer to avoid @@ -246,16 +171,16 @@ func buildStaticSetChunk[F field.Element[F]](c setChunk, sm Module[F]) Set[F] { return data } -func buildDynamicSetChunk[F field.Element[F]](c setChunk, trModule trace.Module[F]) Set[F] { +func buildDynamicSetChunk[F field.Element[F]](id SetId, trModule trace.Module[F]) Set[F] { var ( - buffer = make([]F, c.id.Width()) - data = hash.NewSet[hash.Array[F]]((c.end - c.start) >> 4) + buffer = make([]F, id.Width()) + data = hash.NewSet[hash.Array[F]](trModule.Height() >> 4) ) // - for i := c.start; i < c.end; i++ { - if isSelected(i, c.id, trModule) { + for i := range trModule.Height() { + if isSelected(i, id, trModule) { // Read each register of this vector - readRegisters(i, c.id, trModule, buffer) + readRegisters(i, id, trModule, buffer) // Insert item whilst checking whether the buffer was consumed or not if !data.Insert(hash.NewArray(buffer)) { // Yes, buffer consumed. Therefore, construct fresh buffer to avoid @@ -316,12 +241,12 @@ func isStaticSelected[F field.Element[F]](id SetId, row []F) bool { // Context provides suitable constrant context type contextImpl[F field.Element[F]] struct { - sets map[string]*hash.Set[hash.Array[F]] + sets []map[string]*hash.Set[hash.Array[F]] } // Get implementation of Context interface. -func (p contextImpl[F]) Get(id SetId) collection.Set[[]F] { - if set, ok := p.sets[id.String()]; ok { +func (p contextImpl[F]) Get(shard uint, id SetId) collection.Set[[]F] { + if set, ok := p.sets[shard][id.String()]; ok { return contextSet[F]{set} } // diff --git a/pkg/schema/module/limbs_map.go b/pkg/schema/module/limbs_map.go index 0a20e2445..58c0d5d27 100644 --- a/pkg/schema/module/limbs_map.go +++ b/pkg/schema/module/limbs_map.go @@ -35,7 +35,20 @@ func NewLimbsMap[F any, M register.Map](field field.Config, modules ...M) LimbsM mappings = append(mappings, regmap) } // - return limbsMap[register.LimbsMap]{field, mappings} + return limbsMap[register.LimbsMap]{mappings} +} + +// IdentityMap constructs a "identity" mapping which maps each register to +// itself. +func IdentityMap[F any, M register.Map](modules ...M) LimbsMap { + var mappings []register.LimbsMap + // + for _, m := range modules { + regmap := register.IdentityMap[F](m) + mappings = append(mappings, regmap) + } + // + return limbsMap[register.LimbsMap]{mappings} } // ============================================================================ @@ -45,15 +58,9 @@ func NewLimbsMap[F any, M register.Map](field field.Config, modules ...M) LimbsM // limbsMap provides a straightforward implementation of the schema.LimbMap // interface. type limbsMap[T register.Map] struct { - field field.Config modules []T } -// Field implementation for schema.LimbMap interface -func (p limbsMap[T]) Field() field.Config { - return p.field -} - // Module implementation for register.RegisterMappings interface func (p limbsMap[T]) Module(mid Id) T { return p.modules[mid] @@ -79,8 +86,6 @@ func (p limbsMap[T]) String() string { var builder strings.Builder // builder.WriteString("[") - builder.WriteString(p.field.Name) - builder.WriteString(":") // for i, m := range p.modules { if i != 0 { diff --git a/pkg/schema/module/module.go b/pkg/schema/module/module.go index b5bc34f55..f05b5fa81 100644 --- a/pkg/schema/module/module.go +++ b/pkg/schema/module/module.go @@ -16,7 +16,6 @@ import ( "fmt" "github.com/LFDT-Lineth/zkc/pkg/schema/register" - "github.com/LFDT-Lineth/zkc/pkg/util/field" ) // Name abstracts the notion of a module name. @@ -29,11 +28,6 @@ type Id = uint // maps. type Map[T register.Map] interface { fmt.Stringer - // Field returns the underlying field configuration used for this mapping. - // This includes the field bandwidth (i.e. number of bits available in - // underlying field) and the maximum register width (i.e. width at which - // registers are capped). - Field() field.Config // Module returns register mapping information for the given module. Module(Id) T // ModuleOf returns register mapping information for the given module. @@ -43,8 +37,8 @@ type Map[T register.Map] interface { } // NewMap constructs a new module map -func NewMap[T register.Map](field field.Config, modules []T) Map[T] { - return limbsMap[T]{field, modules} +func NewMap[T register.Map](modules []T) Map[T] { + return limbsMap[T]{modules} } // Apply converts a module map of one kind into a module map of another kind. @@ -57,5 +51,5 @@ func Apply[S, T register.Map](mapping Map[S], fn func(S) T) Map[T] { mods[i] = fn(mapping.Module(i)) } // - return NewMap(mapping.Field(), mods) + return NewMap(mods) } diff --git a/pkg/schema/register/limbs_map.go b/pkg/schema/register/limbs_map.go index 71f6f82df..af977626b 100644 --- a/pkg/schema/register/limbs_map.go +++ b/pkg/schema/register/limbs_map.go @@ -24,11 +24,6 @@ import ( // register to those limbs into which it was subdivided. type LimbsMap interface { Map - // Field returns the underlying field configuration used for this mapping. - // This includes the field bandwidth (i.e. number of bits available in - // underlying field) and the maximum register width (i.e. width at which - // registers are capped). - Field() field.Config // Limbs identifies the limbs into which a given register is divided. // Observe that limbs are ordered by their position in the original // register. In particular, the first limb (i.e. at index 0) is always @@ -78,7 +73,29 @@ func NewLimbsMap[F any](field field.Config, module Map) limbsMap { // Done return limbsMap{ module.Name(), - field, + regs, + limbs, + mapping, + } +} + +// IdentityMap constructs an identity mapping which maps each register to +// itself, etc. +func IdentityMap[F any](module Map) limbsMap { + var ( + regs = module.Registers() + limbs []Limb + mapping = make([][]LimbId, len(regs)) + ) + // Split up limbs + for i, r := range regs { + limbs = append(limbs, r) + // Assign mapping + mapping[i] = []Id{NewId(uint(i))} + } + // Done + return limbsMap{ + module.Name(), regs, limbs, mapping, @@ -99,8 +116,6 @@ func NewLimbsMap[F any](field field.Config, module Map) limbsMap { type limbsMap struct { // Name of the module to which this mapping corresponds name string - // Field configuration in play - field field.Config // Set of registers in the original schema (i.e. as they were before the // split) registers []Register @@ -110,11 +125,6 @@ type limbsMap struct { mapping [][]LimbId } -// Field implementation for register.Map interface -func (p limbsMap) Field() field.Config { - return p.field -} - // Limbs implementation for the register.Map interface func (p limbsMap) LimbIds(reg Id) []LimbId { return p.mapping[reg.Unwrap()] @@ -133,7 +143,7 @@ func (p limbsMap) Limbs() []Limb { // LimbsMap implementation for the register.Map interface func (p limbsMap) LimbsMap() Map { return limbsMap{ - p.name, p.field, p.limbs, nil, nil, + p.name, p.limbs, nil, nil, } } diff --git a/pkg/schema/schema.go b/pkg/schema/schema.go index 5a0e2ecef..418af5911 100644 --- a/pkg/schema/schema.go +++ b/pkg/schema/schema.go @@ -15,7 +15,9 @@ package schema import ( "github.com/LFDT-Lineth/zkc/pkg/schema/module" "github.com/LFDT-Lineth/zkc/pkg/schema/register" + "github.com/LFDT-Lineth/zkc/pkg/trace" "github.com/LFDT-Lineth/zkc/pkg/util/collection/iter" + "github.com/LFDT-Lineth/zkc/pkg/util/collection/set" ) // Any converts a concrete schema into a generic view of the schema. @@ -67,7 +69,11 @@ type Schema[F any, C any] interface { // Failure embodies structured information about a failing constraint. // This includes the constraint itself, along with the row -type Failure interface { +type Failure[F any] interface { + // Handle returns the handling of the constraints which caused the failure. + Handle() string // Provides a suitable error message Message() string + // Identify set of cells relevant to the error. + RequiredCells(trace.Trace[F]) set.AnySortedSet[trace.ShardedCellRef] } diff --git a/pkg/schema/schemas.go b/pkg/schema/schemas.go index dc571d043..b664ddd30 100644 --- a/pkg/schema/schemas.go +++ b/pkg/schema/schemas.go @@ -19,6 +19,7 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/trace" "github.com/LFDT-Lineth/zkc/pkg/util/collection/array" "github.com/LFDT-Lineth/zkc/pkg/util/collection/iter" + "github.com/LFDT-Lineth/zkc/pkg/util/collection/set" "github.com/LFDT-Lineth/zkc/pkg/util/field" log "github.com/sirupsen/logrus" ) @@ -30,52 +31,45 @@ import ( // //nolint:revive func Accepts[F field.Element[F], C Constraint[F]](parallel bool, schema Schema[F, C], - trace trace.Trace[F]) []Failure { - // - return accepts(parallel, schema.Constraints(), trace, schema) -} - -//nolint:revive -func accepts[F field.Element[F], C Constraint[F]](parallel bool, iter iter.Iterator[C], - trace trace.Trace[F], schema Schema[F, C]) []Failure { + trace trace.Trace[F]) (failures []Failure[F]) { // if parallel { - return parallelAccepts(iter, trace, schema) + return parallelAccepts(schema.Constraints(), trace, schema) } // sequential - return sequentialAccepts(iter, trace, schema) + return sequentialAccepts(schema.Constraints(), trace, schema) } func sequentialAccepts[F field.Element[F], C Constraint[F]](iter iter.Iterator[C], trace trace.Trace[F], - schema Schema[F, C]) []Failure { + schema Schema[F, C]) []Failure[F] { // var ( context = SeqBuildContext(trace, Any(schema)) - errors = make([]Failure, 0) + errors = make([]Failure[F], 0) ) - // for iter.HasNext() { - ith := iter.Next() + var ( + ith = iter.Next() + // + errs = ith.Accepts(trace, Any(schema), context) + ) // - err := ith.Accepts(trace, Any(schema), context) - if err != nil { - errors = append(errors, err) - } + errors = append(errors, errs...) } // return errors } func parallelAccepts[F field.Element[F], C Constraint[F]](iter iter.Iterator[C], trace trace.Trace[F], - schema Schema[F, C]) (errors []Failure) { + schema Schema[F, C]) (errors []Failure[F]) { var ( context = ParBuildContext(trace, Any(schema)) // Collect all constraints into a slice so we can use ParallelMap. constraints = iter.Collect() ) // Process all constraints in parallel using a worker pool. - errors = array.ParallelMap(constraints, func(i uint, constraint C) Failure { + errs := array.ParallelMap(constraints, func(i uint, constraint C) []Failure[F] { if i%1000 == 0 { var percent float64 = float64(100*i) / float64(len(constraints)) log.Debug(fmt.Sprintf("Checking constraints [%0.1f%%]", percent)) @@ -83,15 +77,14 @@ func parallelAccepts[F field.Element[F], C Constraint[F]](iter iter.Iterator[C], // return processConstraint(constraint, trace, schema, context) }) - - // - return array.Filter(errors, func(f Failure) bool { return f != nil }) + // Flattern any generated errors + return array.FlatMap(errs, func(fs []Failure[F]) []Failure[F] { return fs }) } // processConstraint checks a given constraint against the trace, intercepting any // panic and converting it into a PanicFailure. -func processConstraint[F field.Element[F], C Constraint[F]](ith C, trace trace.Trace[F], schema Schema[F, C], - ctx Context[F]) (res Failure) { +func processConstraint[F field.Element[F], C Constraint[F]](ith C, trace trace.Trace[F], + schema Schema[F, C], ctx Context[F]) (res []Failure[F]) { // Setup panic intercept defer func() { var err = recover() @@ -102,28 +95,39 @@ func processConstraint[F field.Element[F], C Constraint[F]](ith C, trace trace.T n = runtime.Stack(buf[:], false) ) // override return - res = &PanicFailure{fmt.Sprintf("%v", err), buf[:n]} + res = []Failure[F]{ + &PanicFailure[F]{ith.Name(), fmt.Sprintf("%v", err), buf[:n]}, + } } }() // Check and send outcome back - err := ith.Accepts(trace, Any(schema), ctx) - // - return err + return ith.Accepts(trace, Any(schema), ctx) } // PanicFailure indicates that a panic arose during constraint checking, rather // than an actual constraint failure. The purpose of this is to allow the // testing framework to distinguish panics from actual constraint failures. -type PanicFailure struct { +type PanicFailure[F any] struct { + handle string message string stackTrace []byte } +// Handle implementation for schema.Failure interface. +func (p *PanicFailure[F]) Handle() string { + return p.handle +} + // Message returns the message associated with this panic. -func (p *PanicFailure) Message() string { +func (p *PanicFailure[F]) Message() string { return p.String() } -func (p *PanicFailure) String() string { +// RequiredCells identifies the cells required to evaluate the failing constraint at the failing row. +func (p *PanicFailure[F]) RequiredCells(_ trace.Trace[F]) set.AnySortedSet[trace.ShardedCellRef] { + return nil +} + +func (p *PanicFailure[F]) String() string { return fmt.Sprintf("%s\n\n%s", p.message, string(p.stackTrace)) } diff --git a/pkg/test/corset_invalid_test.go b/pkg/test/corset_invalid_test.go index 6111fbe56..35179eb48 100644 --- a/pkg/test/corset_invalid_test.go +++ b/pkg/test/corset_invalid_test.go @@ -334,6 +334,9 @@ func Test_Invalid_Bus_06(t *testing.T) { func Test_Invalid_Bus_07(t *testing.T) { checkCorsetInvalid(t, "corset/invalid/bus_invalid_07") } +func Test_Invalid_Bus_08(t *testing.T) { + checkCorsetInvalid(t, "corset/invalid/bus_invalid_08") +} // =================================================================== // Arrays diff --git a/pkg/test/corset_valid_test.go b/pkg/test/corset_valid_test.go index f54016d6e..054eb1e32 100644 --- a/pkg/test/corset_valid_test.go +++ b/pkg/test/corset_valid_test.go @@ -566,6 +566,10 @@ func Test_Valid_Bus_05(t *testing.T) { util.CheckCorset(t, "corset/valid/bus_05", field.BLS12_377, field.KOALABEAR_16, field.GF_8209) } +func Test_Valid_Bus_06(t *testing.T) { + util.CheckCorset(t, "corset/valid/bus_06", field.BLS12_377, field.KOALABEAR_16, field.GF_8209) +} + // =================================================================== // Arrays // =================================================================== diff --git a/pkg/test/util/check_legacy.go b/pkg/test/util/check_legacy.go index d1292df09..1e3920537 100644 --- a/pkg/test/util/check_legacy.go +++ b/pkg/test/util/check_legacy.go @@ -13,7 +13,6 @@ package util import ( - stdjson "encoding/json" "fmt" "os" "regexp" @@ -23,11 +22,8 @@ import ( cmd_util "github.com/LFDT-Lineth/zkc/pkg/cmd/corset/util" "github.com/LFDT-Lineth/zkc/pkg/corset" "github.com/LFDT-Lineth/zkc/pkg/ir" - "github.com/LFDT-Lineth/zkc/pkg/ir/air" "github.com/LFDT-Lineth/zkc/pkg/ir/mir" sc "github.com/LFDT-Lineth/zkc/pkg/schema" - "github.com/LFDT-Lineth/zkc/pkg/schema/constraint/bus" - "github.com/LFDT-Lineth/zkc/pkg/schema/module" "github.com/LFDT-Lineth/zkc/pkg/trace" "github.com/LFDT-Lineth/zkc/pkg/trace/json" "github.com/LFDT-Lineth/zkc/pkg/util/field" @@ -106,6 +102,8 @@ func checkWithField[F field.Element[F]](t *testing.T, test string, padding bool, ) // Record how many tests executed. nTests := 0 + // Check for deprecated extensions + checkForDeprecatedTests(t, test) // Iterate possible testfile extensions for _, cfg := range LEGACY_TESTFILE_EXTENSIONS { var traces []trace.Trace[F] @@ -116,28 +114,16 @@ func checkWithField[F field.Element[F]](t *testing.T, test string, padding bool, // Read traces from file traces = ReadTracesFile[F](testFilename) if len(traces) > 0 { + var tmp = cfg + // Update field name + tmp.field = field.Name // Run tests - fullCheckTraces(t, testFilename, cfg, padding, traces, stacks) + fullCheckTraces(t, testFilename, tmp, padding, traces, stacks) } } // Record how many tests we found nTests += len(traces) } - // Iterate possible group (i.e. sharded) testfile extensions - for _, cfg := range SHARDED_TESTFILE_EXTENSIONS { - testFilename := fmt.Sprintf("%s/%s.%s", TestDir, test, cfg.extension) - // - if cfg.field == "" || cfg.field == field.Name { - groups := ReadShardedTracesFile[F](testFilename) - // - if len(groups) > 0 { - stack := stacks.WithOptimisationConfig(mir.DEFAULT_OPTIMISATION_LEVEL) - checkShardedTraces(t, testFilename, padding, mir.DEFAULT_OPTIMISATION_INDEX, cfg, groups, stack) - } - // - nTests += len(groups) - } - } // Sanity check at least one trace found. if nTests == 0 { panic(fmt.Sprintf("missing any tests for %s", test)) @@ -214,13 +200,13 @@ func checkTraces[F field.Element[F]](t *testing.T, test string, padding bool, op // if tf != nil { // Construct trace identifier - id := traceId{stack.RegisterMapping().Field().Name, ir, test, + id := traceId{cfg.field, ir, test, cfg.expected, cfg.expand, cfg.validate, opt, parallel, i + 1, padding} // if cfg.expand || ir == "AIR" { // Always check if expansion required, otherwise // only check AIR constraints. - checkTrace(t, tf, id, stack.ConcreteSchemaOf(ir), stack.RegisterMapping()) + checkTrace(t, tf, id, stack.ConcreteSchemaOf(ir)) } } } @@ -230,38 +216,45 @@ func checkTraces[F field.Element[F]](t *testing.T, test string, padding bool, op } func checkTrace[F field.Element[F], C sc.Constraint[F]](t *testing.T, tf trace.Trace[F], id traceId, - schema sc.Schema[F, C], mapping module.LimbsMap) { - // Map the legacy padding toggle onto a padding strategy. - paddingStrategy := ir.NaryRowPadding(0) + schema sc.Schema[F, C]) { + var ( + errors []error + // Map the legacy padding toggle onto a padding strategy. + paddingStrategy = ir.NaryRowPadding(0) + // + shards = make(trace.Trace[F], len(tf)) + ) if id.padding { paddingStrategy = ir.NextPowerOfTwoPadding } - // Construct the trace - tr, errs := ir.NewTraceBuilder[F](). + // Construct builder + builder := ir.NewTraceBuilder[F](). WithExpansion(id.expand). WithValidation(id.validate). WithPadding(paddingStrategy). WithParallelism(id.parallel). - WithRegisterMapping(mapping). - WithBatchSize(128). - Build(sc.Any(schema), tf) - // Sanity check construction - if len(errs) > 0 { - t.Errorf("Trace expansion failed (%s): %s", id.String(), errs) - } else { - // Check Constraints - errs := sc.Accepts(id.parallel, schema, tr) - // Determine whether trace accepted or not. - accepted := len(errs) == 0 - // Process what happened versus what was supposed to happen. - if !accepted && id.expected { - //table.PrintTrace(tr) - t.Errorf("Trace rejected incorrectly (%s): %s", id.String(), errs) - } else if accepted && !id.expected { - //printTrace(tr) - t.Errorf("Trace accepted incorrectly (%s)", id.String()) + WithBatchSize(128) + // Construct the trace + for i, shard := range tf { + shards[i], errors = builder.Build(sc.Any(schema), shard) + // + if len(errors) > 0 { + t.Errorf("Trace expansion failed (%s): %s", id.String(), errors) + return } } + // Check Constraints + errs := sc.Accepts(id.parallel, schema, shards) + // Determine whether trace accepted or not. + accepted := len(errs) == 0 + // Process what happened versus what was supposed to happen. + if !accepted && id.expected { + //table.PrintTrace(tr) + t.Errorf("Trace rejected incorrectly (%s): %s", id.String(), errs) + } else if accepted && !id.expected { + //printTrace(tr) + t.Errorf("Trace accepted incorrectly (%s)", id.String()) + } } // SRC_EXTENSIONS identifies the set of currently recognised extensions for @@ -304,178 +297,50 @@ var defaultOptLevel = []uint{1} var LEGACY_TESTFILE_EXTENSIONS []LegacyTestConfig = []LegacyTestConfig{ // should all pass {"accepts", true, true, true, "", allOptLevels}, - {"accepts.bz2", true, true, true, "", allOptLevels}, + {"expanded.accepts", true, false, false, "", defaultOptLevel}, + {"expanded.bls12_377.accepts", true, false, false, "BLS12_377", defaultOptLevel}, {"auto.accepts", true, true, true, "", allOptLevels}, - {"auto.accepts.bz2", true, true, true, "", allOptLevels}, {"bls12_377.accepts", true, true, true, "BLS12_377", allOptLevels}, {"koalabear_16.accepts", true, true, true, "KOALABEAR_16", allOptLevels}, {"gf_8209.accepts", true, true, true, "GF_8209", allOptLevels}, {"bls12_377.accepts.bz2", true, true, true, "BLS12_377", allOptLevels}, {"koalabear_16.accepts.bz2", true, true, true, "KOALABEAR_16", allOptLevels}, - {"expanded.accepts", true, false, false, "BLS12_377", allOptLevels}, - {"expanded.O1.accepts", true, false, false, "BLS12_377", defaultOptLevel}, // should all fail {"rejects", false, true, false, "", allOptLevels}, - {"rejects.bz2", false, true, false, "", allOptLevels}, {"auto.rejects", false, true, false, "", allOptLevels}, + {"expanded.rejects", false, false, false, "", defaultOptLevel}, + {"expanded.bls12_377.rejects", false, false, false, "BLS12_377", defaultOptLevel}, {"bls12_377.rejects", false, true, false, "BLS12_377", allOptLevels}, {"koalabear_16.rejects", false, true, false, "KOALABEAR_16", defaultOptLevel}, {"gf_8209.rejects", false, true, false, "GF_8209", defaultOptLevel}, {"expanded.koalabear_16.rejects", false, false, false, "KOALABEAR_16", defaultOptLevel}, {"expanded.gf_8209.rejects", false, false, false, "GF_8209", defaultOptLevel}, - {"expanded.rejects", false, false, false, "BLS12_377", allOptLevels}, - {"expanded.O1.rejects", false, false, false, "BLS12_377", defaultOptLevel}, } -// SHARDED_TESTFILE_EXTENSIONS identifies the file extensions used for sharded -// tests. Each line of such a file holds a JSON array of traces, forming one -// group of shards judged together: every shard must pass all non-bus -// constraints on its own, whilst bus balance is required of the group as a -// whole (not of any single shard). -var SHARDED_TESTFILE_EXTENSIONS []LegacyTestConfig = []LegacyTestConfig{ - {"shards.accepts", true, true, true, "", defaultOptLevel}, - {"shards.rejects", false, true, false, "", defaultOptLevel}, +// LEGACY_DEPRECATED_EXTENSIONS clarifies test extensions which are no longer +// supported. Any test having one of these extensions is rejected outright. +// Basically, all test vectors must now specify their field explicitly. +var LEGACY_DEPRECATED_EXTENSIONS []string = []string{ + "accepts.bz2", + "auto.accepts.bz2", + "expanded.O1.accepts", + // rejects + "rejects.bz2", + "auto.rejects.bz2", + "expanded.O1.rejects", } -// ReadShardedTracesFile reads a file containing zero or more trace groups -// expressed as JSON, where each group is on a separate line and consists of -// an array of traces (i.e. shards). -func ReadShardedTracesFile[F field.Element[F]](filename string) [][]trace.Trace[F] { - lines, _ := file.ReadInputFileAsLines(filename) - groups := make([][]trace.Trace[F], len(lines)) - // - for i, line := range lines { - if line != "" && !strings.HasPrefix(line, ";;") { - var shards []stdjson.RawMessage - // - if err := stdjson.Unmarshal([]byte(line), &shards); err != nil { - panic(fmt.Sprintf("%s:%d: %s", filename, i+1, err)) - } - // - group := make([]trace.Trace[F], len(shards)) - // - for j, raw := range shards { - tf, err := json.FromBytes[F](raw) - // - if err != nil { - panic(fmt.Sprintf("%s:%d: shard %d: %s", filename, i+1, j+1, err)) - } - // - group[j] = tf - } - // - groups[i] = group - } - } - // - return groups -} - -// Check a given set of trace groups have an expected outcome, mirroring -// checkTraces. -func checkShardedTraces[F field.Element[F]](t *testing.T, test string, padding bool, opt uint, - cfg LegacyTestConfig, groups [][]trace.Trace[F], stacker cmd_util.SchemaStacker[F]) { - // - paddings := []bool{false} - if padding { - paddings = append(paddings, true) - } - // - stack := stacker.Build() - // - for _, padding := range paddings { - t.Run(test, func(t *testing.T) { - t.Parallel() - // - for _, ir := range []string{"MIR", "AIR"} { - for i, group := range groups { - if group != nil { - id := traceId{stack.RegisterMapping().Field().Name, ir, test, - cfg.expected, cfg.expand, cfg.validate, opt, false, i + 1, padding} - // - checkShardGroup(t, group, id, stack.ConcreteSchemaOf(ir), stack.RegisterMapping()) - } - } - } - }) - } -} - -// checkShardGroup checks one group of shards: each shard is built and -// checked locally (any non-bus failure marks a broken fixture, regardless of -// the expected outcome), then every bus is required to balance across the -// whole group. Only the group-level verdict is compared against the -// expected outcome. -func checkShardGroup[F field.Element[F], C sc.Constraint[F]](t *testing.T, group []trace.Trace[F], id traceId, - schema sc.Schema[F, C], mapping module.LimbsMap) { - // - var ( - built = make([]trace.Trace[F], len(group)) - failures []sc.Failure - ) - // Build and locally check every shard - for i, tf := range group { - paddingStrategy := ir.NaryRowPadding(0) - if id.padding { - paddingStrategy = ir.NextPowerOfTwoPadding - } - // - tr, errs := ir.NewTraceBuilder[F](). - WithExpansion(id.expand). - WithValidation(id.validate). - WithPadding(paddingStrategy). - WithRegisterMapping(mapping). - WithBatchSize(128). - Build(sc.Any(schema), tf) - // - if len(errs) > 0 { - t.Errorf("Shard %d expansion failed (%s): %s", i+1, id.String(), errs) - return - } - // Check shard locally, ignoring bus failures (balance is a property - // of the group, not of any single shard). - for _, err := range sc.Accepts(false, schema, tr) { - if _, isBus := err.(*bus.Failure[F]); !isBus { - t.Errorf("Shard %d locally invalid (%s): %s", i+1, id.String(), err.Message()) - return - } +func checkForDeprecatedTests(t *testing.T, test string) { + // Iterate possible testfile extensions + for _, ext := range LEGACY_DEPRECATED_EXTENSIONS { + filename := fmt.Sprintf("%s.%s", test, ext) + // Construct test filename + if _, err := os.Stat(fmt.Sprintf("%s/%s", TestDir, filename)); os.IsNotExist(err) { + continue } // - built[i] = tr - } - // Check every bus balances across the whole group. - for _, busc := range busConstraintsOf(schema) { - if failure := busc.AcceptsGroup(built...); failure != nil { - failures = append(failures, failure) - } - } - // - accepted := len(failures) == 0 - // - if !accepted && id.expected { - t.Errorf("Group rejected incorrectly (%s): %s", id.String(), failures) - } else if accepted && !id.expected { - t.Errorf("Group accepted incorrectly (%s)", id.String()) - } -} - -// busConstraintsOf extracts the bus constraints of a schema, looking through -// the MIR / AIR wrappers. -func busConstraintsOf[F field.Element[F], C sc.Constraint[F]](schema sc.Schema[F, C]) []bus.Constraint[F] { - var buses []bus.Constraint[F] - // - for iter := schema.Constraints(); iter.HasNext(); { - switch c := any(iter.Next()).(type) { - case mir.Constraint[F]: - if b, ok := c.Unwrap().(bus.Constraint[F]); ok { - buses = append(buses, b) - } - case air.BusConstraint[F]: - buses = append(buses, c.Unwrap()) - } + t.Errorf("encountered deprecated test file: %s", filename) } - // - return buses } // A trace identifier uniquely identifies a specific trace within a given test. diff --git a/pkg/test/util/check_valid.go b/pkg/test/util/check_valid.go index 66d675a42..a1164206c 100644 --- a/pkg/test/util/check_valid.go +++ b/pkg/test/util/check_valid.go @@ -71,8 +71,8 @@ type Config struct { // range tables. Widths whose enumeration would exceed this are range-checked // recursively instead. Defaults to codegen.DEFAULT_MAX_STATIC_HEIGHT. maxStaticHeights []uint - // enable checkpoint testing. - parallelTracing util.Option[vm.ShardingStrategy] + // enable sharding. + sharding util.Option[vm.ShardingStrategy] } // MaxStaticHeights sets the maximum heights number of rows) of static range @@ -93,20 +93,9 @@ func (p Config) GoGen(flag bool) Config { return p } -// ParallelTracing enables trace parallelisation with checkpoints at every n ZkC -// instructions. -// -// NOTE: this is currently broken for any program declaring a read-write memory, -// and so must not be enabled for one. Each shard is traced independently and -// the results concatenated by trace.Reduce, so the leading RAM padding row -// emitted by traceReadWriteMemory appears once per shard rather than once per -// trace. That leaves inactive rows scattered through the reduced module, which -// violates the "active_monotony" constraint. ROM/WOM are unaffected, as their -// modules are replicated (reduction keeps a single copy), hence programs -// without a read-write memory can still be sharded. To be fixed separately, -// after which the callers marked "restore ParallelTracing" can be reinstated. -func (p Config) ParallelTracing(fn string, n uint64) Config { - p.parallelTracing = util.Some(vm.NewShardingStrategy(fn, n)) +// Sharding enables trace sharding with checkpoints at every n ZkC instructions. +func (p Config) Sharding(fn string, n uint64) Config { + p.sharding = util.Some(vm.NewShardingStrategy(fn, n)) // return p } @@ -253,10 +242,10 @@ func checkValidMachine(t *testing.T, p vm.Program[vm.Uint], cfg testConfig, test }) } // Parallel tracing (if requested) - if cfg.parallelTracing.HasValue() { - traceCfg := vm.DEFAULT_TRACE_CONFIG.WithSharding(cfg.parallelTracing.Unwrap()) + if cfg.sharding.HasValue() { + traceCfg := vm.DEFAULT_TRACE_CONFIG.WithSharding(cfg.sharding.Unwrap()) // - t.Run("parallel-tracing", func(t *testing.T) { + t.Run("sharded-tracing", func(t *testing.T) { runConstraintTest(t, p, test, field, traceCfg) }) } @@ -308,7 +297,7 @@ func runExecutionTest[F field.Element[F]](t *testing.T, p vm.Program[vm.Uint], t } } else { // Fail automatically on any panic arising during execution - failIf[*schema.PanicFailure](t, errs...) + failIf[*schema.PanicFailure[F]](t, errs...) // Determine whether test accepted or not. accepted := len(errs) == 0 // Process what happened versus what was supposed to happen. @@ -358,9 +347,9 @@ func testConstraintsWithField[F field.Element[F]](t *testing.T, p vm.Program[vm. failIf[*vm.Failure](t, errs...) } // Check constraints - failures := binf.Check(tr, traceCfg) + failures := binf.Check(traceCfg, tr) // Fail automatically on any panic arising during constraint checking - failIf[*schema.PanicFailure](t, failures...) + failIf[*schema.PanicFailure[F]](t, failures...) // Determine whether trace accepted or not. accepted := len(failures) == 0 // Process what happened versus what was supposed to happen. diff --git a/pkg/test/zkc_bench_test.go b/pkg/test/zkc_bench_test.go index af440699b..e5c856d8a 100644 --- a/pkg/test/zkc_bench_test.go +++ b/pkg/test/zkc_bench_test.go @@ -37,7 +37,7 @@ func Test_ZkcBench_FastPow(t *testing.T) { } func Test_ZkcBench_RecPow(t *testing.T) { - checkZkcBench(t, "zkc/bench/rec_pow", DEFAULT_BENCH_CONFIG) + checkZkcBench(t, "zkc/bench/rec_pow", DEFAULT_BENCH_CONFIG.Sharding("pow", 2)) } func Test_ZkcBench_Gcd(t *testing.T) { @@ -49,7 +49,7 @@ func Test_ZkcBench_Fnv1aHash(t *testing.T) { } func Test_ZkcBench_Keccak(t *testing.T) { - checkZkcBench(t, "zkc/bench/keccak", DEFAULT_BENCH_CONFIG.Sampling(0.1).ParallelTracing("keccak_f", 10)) + checkZkcBench(t, "zkc/bench/keccak", DEFAULT_BENCH_CONFIG.Sampling(0.1)) } func Test_ZkcBench_Poseidon(t *testing.T) { // #2007: support implicit sign bit @@ -62,8 +62,6 @@ func Test_ZkcBench_Poseidon(t *testing.T) { // =================================================================== func Test_ZkcBench_Sort(t *testing.T) { - // TODO: restore ParallelTracing("sort_slice", 5) once sharded RAM tracing - // is fixed (see util.Config.ParallelTracing). checkZkcBench(t, "zkc/bench/sort", DEFAULT_BENCH_CONFIG.Sampling(0.1)) } diff --git a/pkg/test/zkc_invalid_test.go b/pkg/test/zkc_invalid_test.go index 1e2fe2404..85396d176 100644 --- a/pkg/test/zkc_invalid_test.go +++ b/pkg/test/zkc_invalid_test.go @@ -1089,6 +1089,11 @@ func Test_ZkcInvalid_Inline_06(t *testing.T) { checkZkcInvalid(t, "zkc/invalid/inline_06") } +func Test_ZkcInvalid_Inline_07(t *testing.T) { + // Non-returning functions cannot be inlined. + checkZkcInvalid(t, "zkc/invalid/inline_07") +} + func Test_ZkcInvalid_Unused_01(t *testing.T) { // A local variable which is never read or written is unused. checkZkcInvalid(t, "zkc/invalid/unused_01") @@ -1139,6 +1144,15 @@ func Test_ZkcInvalid_Unreachable_04(t *testing.T) { checkZkcInvalid(t, "zkc/invalid/unreachable_04") } +// =================================================================== +// Global Tests +// =================================================================== + +func Test_ZkcInvalid_Global_01(t *testing.T) { + // unreachable RAM + checkZkcInvalid(t, "zkc/invalid/global_01") +} + // =================================================================== // Test Helpers // =================================================================== diff --git a/pkg/test/zkc_unit_test.go b/pkg/test/zkc_unit_test.go index 57eefe88d..af426ca46 100644 --- a/pkg/test/zkc_unit_test.go +++ b/pkg/test/zkc_unit_test.go @@ -367,14 +367,10 @@ func Test_ZkcUnit_Basic_85(t *testing.T) { } func Test_ZkcUnit_Basic_86(t *testing.T) { - // TODO: restore ParallelTracing("copy", 1) once sharded RAM tracing is - // fixed (see util.Config.ParallelTracing). - checkZkcUnit(t, "zkc/unit/basic_86", DEFAULT_UNIT_CONFIG) + checkZkcUnit(t, "zkc/unit/basic_86", DEFAULT_UNIT_CONFIG.Sharding("copy", 1)) } func Test_ZkcUnit_Basic_87(t *testing.T) { - // TODO: restore ParallelTracing("copy", 1) once sharded RAM tracing is - // fixed (see util.Config.ParallelTracing). checkZkcUnit(t, "zkc/unit/basic_87", DEFAULT_UNIT_CONFIG) } @@ -383,15 +379,15 @@ func Test_ZkcUnit_Basic_88(t *testing.T) { } func Test_ZkcUnit_Basic_89(t *testing.T) { - checkZkcUnit(t, "zkc/unit/basic_89", DEFAULT_UNIT_CONFIG) + checkZkcUnit(t, "zkc/unit/basic_89", DEFAULT_UNIT_CONFIG.Sharding("checkNonZero", 1)) } func Test_ZkcUnit_Basic_90(t *testing.T) { - checkZkcUnit(t, "zkc/unit/basic_90", DEFAULT_UNIT_CONFIG) + checkZkcUnit(t, "zkc/unit/basic_90", DEFAULT_UNIT_CONFIG.Sharding("checkNonZero", 1)) } func Test_ZkcUnit_Basic_91(t *testing.T) { - checkZkcUnit(t, "zkc/unit/basic_91", DEFAULT_UNIT_CONFIG) + checkZkcUnit(t, "zkc/unit/basic_91", DEFAULT_UNIT_CONFIG.Sharding("checkNonZero", 1)) } func Test_ZkcUnit_AccessOnceMemory_01(t *testing.T) { diff --git a/pkg/trace/json/reader.go b/pkg/trace/json/reader.go index b1e2d02c1..2009efd40 100644 --- a/pkg/trace/json/reader.go +++ b/pkg/trace/json/reader.go @@ -26,36 +26,52 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/util/field" ) -// FromBytes parses a trace expressed in JSON notation. For example, {"X": -// [0], "Y": [1]} is a trace containing one row of data each for two columns "X" -// and "Y". -func FromBytes[F field.Element[F]](data []byte) (trace.Trace[F], error) { +// FromBytes parses a sharded trace expressed in JSON notation. For example, +// {"X": [0], "Y": [1]} is a trace containing one row of data each for two +// columns "X" and "Y". +func FromBytes[F field.Element[F]](data []byte) (tr trace.Trace[F], err error) { var ( - rawData map[string]map[string][]big.Int + shard trace.Shard[F] + unsharded map[string]map[string][]big.Int + sharded []map[string]map[string][]big.Int + legacyUnsharded map[string][]big.Int + legacySharded []map[string][]big.Int ) // Attempt to unmarshall - jsonErr := json.Unmarshal(data, &rawData) - if jsonErr != nil { - // Failed, so try and fall back on the legacy format. - return FromBytesLegacy[F](data) + if err = json.Unmarshal(data, &sharded); err == nil { + for _, data := range sharded { + if shard, err = fromBytesInternal[F](data); err != nil { + return nil, err + } + // + tr = append(tr, shard) + } + } else if err = json.Unmarshal(data, &legacySharded); err == nil { + for _, data := range legacySharded { + if shard, err = fromBytesLegacy[F](data); err != nil { + return nil, err + } + // + tr = append(tr, shard) + } + } else if err = json.Unmarshal(data, &unsharded); err == nil { + shard, err = fromBytesInternal[F](unsharded) + tr = trace.Trace[F]{shard} + } else if err = json.Unmarshal(data, &legacyUnsharded); err == nil { + shard, err = fromBytesLegacy[F](legacyUnsharded) + tr = trace.Trace[F]{shard} } // - return fromBytesInternal[F](rawData) + return tr, err } // FromBytesLegacy parses a trace expressed in JSON notation. For example, {"X": // [0], "Y": [1]} is a trace containing one row of data each for two columns "X" // and "Y". -func FromBytesLegacy[F field.Element[F]](data []byte) (trace.Trace[F], error) { +func fromBytesLegacy[F field.Element[F]](rawData map[string][]big.Int) (trace.Shard[F], error) { var ( - rawData map[string][]big.Int strData = make(map[string]map[string][]big.Int, 0) ) - // Unmarshall - jsonErr := json.Unmarshal(data, &rawData) - if jsonErr != nil { - return nil, jsonErr - } // for name, rawInts := range rawData { // Translate raw bigints into raw field elements @@ -77,7 +93,7 @@ func FromBytesLegacy[F field.Element[F]](data []byte) (trace.Trace[F], error) { return fromBytesInternal[F](strData) } -func fromBytesInternal[F field.Element[F]](rawData map[string]map[string][]big.Int) (trace.Trace[F], error) { +func fromBytesInternal[F field.Element[F]](rawData map[string]map[string][]big.Int) (trace.Shard[F], error) { var modules []*trace.CompactModule[F] // for mod, modData := range rawData { diff --git a/pkg/trace/json/writer.go b/pkg/trace/json/writer.go index 6e88cb1e6..dd6d626e5 100644 --- a/pkg/trace/json/writer.go +++ b/pkg/trace/json/writer.go @@ -22,6 +22,26 @@ import ( // ToJsonString converts a trace into a JSON string. func ToJsonString[F field.Element[F]](tr trace.Trace[F]) string { + var ( + builder strings.Builder + ) + // + if len(tr) == 1 { + return toJsonString(tr[0]) + } + // + for i, shard := range tr { + if i != 0 { + builder.WriteString(", ") + } + // + builder.WriteString(toJsonString(shard)) + } + // + return builder.String() +} + +func toJsonString[F field.Element[F]](tr trace.Shard[F]) string { var ( builder strings.Builder first = true @@ -51,6 +71,14 @@ func ToJsonString[F field.Element[F]](tr trace.Trace[F]) string { builder.WriteString("\"") // Construct qualified column qual_name qual_name := trace.QualifiedColumnName(ith.Name(), name) + // Sanity check + if data == nil { + // Write out column name + builder.WriteString(qual_name) + builder.WriteString("\": []") + // + continue + } // Apply bitwidth restrictions (if applicable) if bitwidth := data.BitWidth(); bitwidth < 256 { // For now, always assume unsigned int. diff --git a/pkg/trace/reduce.go b/pkg/trace/reduce.go index db93bf17f..c27116178 100644 --- a/pkg/trace/reduce.go +++ b/pkg/trace/reduce.go @@ -22,7 +22,7 @@ import ( // share the same module index and matching register (and hence limb) // descriptors. For each module, the rows of every input trace are // concatenated, in trace order, into the corresponding module of the result. -func Reduce[F field.Element[F]](traces []Trace[F]) Trace[F] { +func Reduce[F field.Element[F]](traces []Shard[F]) Shard[F] { if len(traces) == 0 { return nil } @@ -43,7 +43,7 @@ func Reduce[F field.Element[F]](traces []Trace[F]) Trace[F] { // ParallelReduce behaves exactly like Reduce, combining a sequence of aligned // traces into a single trace, but reduces each module of the result // concurrently using a worker pool. -func ParallelReduce[F field.Element[F]](traces []Trace[F]) Trace[F] { +func ParallelReduce[F field.Element[F]](traces []Shard[F]) Shard[F] { if len(traces) == 0 { return nil } @@ -65,7 +65,7 @@ func ParallelReduce[F field.Element[F]](traces []Trace[F]) Trace[F] { // reduceModule concatenates the rows of the module at a given index across all // traces. The module name and descriptor are taken from the first trace, which // aligned traces guarantee match those of every other trace. -func reduceModule[F field.Element[F]](mid uint, descriptor ModuleDescriptor, traces []Trace[F]) *CompactModule[F] { +func reduceModule[F field.Element[F]](mid uint, descriptor ModuleDescriptor, traces []Shard[F]) *CompactModule[F] { // Check whether replicating if descriptor.Replicated { return reduceReplicatedModule(mid, descriptor, traces) @@ -80,7 +80,7 @@ func reduceModule[F field.Element[F]](mid uint, descriptor ModuleDescriptor, tra return acc } -func reduceReplicatedModule[F field.Element[F]](mid uint, descriptor ModuleDescriptor, traces []Trace[F], +func reduceReplicatedModule[F field.Element[F]](mid uint, descriptor ModuleDescriptor, traces []Shard[F], ) *CompactModule[F] { var ( winner Module[F] diff --git a/pkg/trace/ref.go b/pkg/trace/ref.go index f84b648d9..0626f632f 100644 --- a/pkg/trace/ref.go +++ b/pkg/trace/ref.go @@ -45,6 +45,29 @@ func (p CellRef) Cmp(q CellRef) int { return c } +// ShardedCellRef identifies a unique cell within a given table. +type ShardedCellRef struct { + // Shard containing the given cell + Shard uint + // Reference of the given cell + Ref CellRef +} + +// NewShardedCellRef constructs a new (sharded) cell reference. +func NewShardedCellRef(shard uint, column ColumnRef, row int) ShardedCellRef { + return ShardedCellRef{shard, NewCellRef(column, row)} +} + +// Cmp implementation for the set.Comparable interface. This allows a CellRef to +// be used in an AnySortedSet. +func (p ShardedCellRef) Cmp(q ShardedCellRef) int { + if c := cmp.Compare(p.Shard, q.Shard); c != 0 { + return c + } + // + return p.Ref.Cmp(q.Ref) +} + // ============================================================================ // ColumnRef abstracts a complete (i.e. global) Column identifier. diff --git a/pkg/trace/trace.go b/pkg/trace/trace.go index abd86aa2f..705d8b48a 100644 --- a/pkg/trace/trace.go +++ b/pkg/trace/trace.go @@ -20,8 +20,12 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/util/collection/iter" ) -// Trace describes a set of named modules whose data is organised by row. -type Trace[T any] interface { +// Trace represents a complete (sharded) trace. That is, an array of shards. +type Trace[T any] []Shard[T] + +// Shard forms part of a trace, and describes a set of named modules whose data +// is organised by row. +type Shard[T any] interface { // Determine whether this trace has a module with the given name and, if so, // what its module index is. HasModule(name string) (uint, bool) diff --git a/pkg/util/collection/hash/hash_map.go b/pkg/util/collection/hash/hash_map.go index 091cdee4f..9aa32e6d1 100644 --- a/pkg/util/collection/hash/hash_map.go +++ b/pkg/util/collection/hash/hash_map.go @@ -73,7 +73,8 @@ func (p *Map[K, V]) KeyValues() iter.Iterator[util.Pair[K, V]] { } // Insert a new item into this map, returning true if it was already contained -// and false otherwise. +// and false otherwise. Observe that, if this returns false then the key is +// consumed by this function. // //nolint:revive func (p *Map[K, V]) Insert(key K, value V) bool { @@ -90,6 +91,30 @@ func (p *Map[K, V]) Insert(key K, value V) bool { return r } +// Update a given function to a value in the map (if it already exists), or +// insert a given initial value. This returning true if it was already +// contained and false otherwise. Observe that, if this returns false then the +// key is consumed by this function. +func (p *Map[K, V]) Update(key K, fn func(V) V, init V) bool { + var ( + hash = key.Hash() + b1 = p.buckets[hash] + ) + // Key already present, apply function to value and update in place. + for i, k := range b1.keys { + if key.Equals(k) { + b1.values[i] = fn(b1.values[i]) + return true + } + } + // Key not present, so insert initial value. + b1.keys = append(b1.keys, key) + b1.values = append(b1.values, init) + p.buckets[hash] = b1 + // No present + return false +} + // ContainsKey checks whether the given item is contained within this map, or not. // //nolint:revive diff --git a/pkg/zkc/compiler/ast/decl/annotation.go b/pkg/zkc/compiler/ast/decl/annotation.go index 7c4fc3845..4dead4bdb 100644 --- a/pkg/zkc/compiler/ast/decl/annotation.go +++ b/pkg/zkc/compiler/ast/decl/annotation.go @@ -98,4 +98,6 @@ var ANNOTATIONS = []Annotation{ NewAnnotation("debug", "marks a function as debug-only, elided entirely (calls and definition) unless verbose mode is enabled", FUNCTION_KIND), + // + NewAnnotation("global", "marks a function which supports cross-shard calling", FUNCTION_KIND), } diff --git a/pkg/zkc/compiler/codegen/compile.go b/pkg/zkc/compiler/codegen/compile.go index 80bb1307f..0e1691d27 100644 --- a/pkg/zkc/compiler/codegen/compile.go +++ b/pkg/zkc/compiler/codegen/compile.go @@ -276,6 +276,8 @@ func buildFunctionKind(fn *decl.ResolvedFunction) vm.FunctionKind { kind = kind.WithInline(true) case "native": kind = kind.WithNative(true) + case "global": + kind = kind.WithGlobal(true) case "debug": // ignore default: diff --git a/pkg/zkc/compiler/compiler.go b/pkg/zkc/compiler/compiler.go index d9f359054..6f886445f 100644 --- a/pkg/zkc/compiler/compiler.go +++ b/pkg/zkc/compiler/compiler.go @@ -190,6 +190,8 @@ func validateProgram(program ast.Program, field field.Config, srcmaps source.Map errors = append(errors, validate.DebugFunctions(program, srcmaps)...) // Check #[inline] functions can actually be inlined errors = append(errors, validate.InlineFunctions(program, srcmaps)...) + // Check #[global] functions can actually be placed on the bus + errors = append(errors, validate.GlobalFunctions(program, srcmaps)...) // Check no static tables have more rows than max-static-height errors = append(errors, validate.StaticTableHeight(program, srcmaps, maxStaticHeight)...) // diff --git a/pkg/zkc/compiler/validate/global.go b/pkg/zkc/compiler/validate/global.go new file mode 100644 index 000000000..6a72f9ab0 --- /dev/null +++ b/pkg/zkc/compiler/validate/global.go @@ -0,0 +1,43 @@ +// Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with +// the License. You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on +// an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the +// specific language governing permissions and limitations under the License. +// +// SPDX-License-Identifier: Apache-2.0 +package validate + +import ( + "slices" + + "github.com/LFDT-Lineth/zkc/pkg/util/source" + "github.com/LFDT-Lineth/zkc/pkg/zkc/compiler/ast" + "github.com/LFDT-Lineth/zkc/pkg/zkc/compiler/ast/decl" +) + +// GlobalFunctions checks that every function marked with the #[global] +// annotation is declared as non-returning (i.e. "-> !"). A global function is +// placed "on the bus" so that it can be called from another shard. Since +// caller and callee may then reside in different shards, there is no way to +// thread the callee's results back to the caller. Hence, a global function +// which returns is rejected here. +func GlobalFunctions(program ast.Program, srcmaps source.Maps[any]) []source.SyntaxError { + var errors []source.SyntaxError + // + for _, d := range program.Components() { + fn, ok := d.(*decl.ResolvedFunction) + // + if !ok || !slices.Contains(fn.Annotations(), "global") { + continue + } + // + if !fn.NoReturn { + errors = append(errors, srcmaps.SyntaxErrors(fn, "global function must not return")...) + } + } + // + return errors +} diff --git a/pkg/zkc/compiler/validate/inline.go b/pkg/zkc/compiler/validate/inline.go index b85dc4f6f..10a6269d6 100644 --- a/pkg/zkc/compiler/validate/inline.go +++ b/pkg/zkc/compiler/validate/inline.go @@ -29,10 +29,14 @@ import ( // // (2) marked #[native], since native functions have no body to inline; // -// (3) (mutually) recursive with other inlined functions, since inlining such +// (3) non-returning (i.e. declared "-> !"), since a non-returning function +// terminates the enclosing frame rather than resuming its caller, meaning +// there is nothing for the residual code after the call site to inline into; +// +// (4) (mutually) recursive with other inlined functions, since inlining such // functions can never terminate. // -// Observe that (3) only rejects recursive cycles consisting entirely of +// Observe that (4) only rejects recursive cycles consisting entirely of // inlined functions. Recursion through a non-inlined function is fine, since // the residual call to that function simply remains in the inlined body. func InlineFunctions(program ast.Program, srcmaps source.Maps[any]) []source.SyntaxError { @@ -54,6 +58,8 @@ func InlineFunctions(program ast.Program, srcmaps source.Maps[any]) []source.Syn errors = append(errors, srcmaps.SyntaxErrors(fn, "cannot inline entry function")...) case slices.Contains(fn.Annotations(), "native"): errors = append(errors, srcmaps.SyntaxErrors(fn, "cannot inline native function")...) + case fn.NoReturn: + errors = append(errors, srcmaps.SyntaxErrors(fn, "cannot inline non-returning function")...) default: remaining = append(remaining, uint(i)) } diff --git a/pkg/zkc/constraints/binary_file.go b/pkg/zkc/constraints/binary_file.go index bb1985255..f6ab6468a 100644 --- a/pkg/zkc/constraints/binary_file.go +++ b/pkg/zkc/constraints/binary_file.go @@ -273,13 +273,13 @@ func (p *BinaryFile[F]) clearCachedArtifacts() { // Check a given trace against the AIR constraints embodied in this constraints // file, potentially producing one (or more) constraint failures. -func (p *BinaryFile[F]) Check(tr trace.Trace[F], config vm.TraceConfig) []schema.Failure { +func (p *BinaryFile[F]) Check(config vm.TraceConfig, trace trace.Trace[F]) []schema.Failure[F] { var ( sc = p.AirConstraints() stats = util.NewPerfStats() ) // Check constraints - failures := schema.Accepts(config.Parallelism(), sc, tr) + failures := schema.Accepts(config.Parallelism(), sc, trace) // Log stats stats.Log("Constraint checking") // @@ -309,7 +309,7 @@ func (p *BinaryFile[F]) Execute(input map[string][]byte) (output map[string][]by // carries the original register / limb structure before AIR expansion (e.g. for // reporting statistics). It is nil when execution fails. func (p *BinaryFile[F]) Trace(input map[string][]byte, cfg vm.TraceConfig, -) (output map[string][]byte, rtr trace.Trace[F], errs []error) { +) (output map[string][]byte, trace trace.Trace[F], errs []error) { // var ( stats = util.NewPerfStats() @@ -317,9 +317,9 @@ func (p *BinaryFile[F]) Trace(input map[string][]byte, cfg vm.TraceConfig, builder = vm.NewTraceBuilder[vm.Uint32, F, Tracer[F]](cfg, p.TracingProgram()) ) // Execute machine in chunks of 1K steps - rtr, output, errs = builder.BootAndTrace(input) + trace, output, errs = builder.BootAndTrace(input) // - if rtr != nil { + if len(trace) > 0 { var berrs []error // Extract AIR constraints constraints := p.AirConstraints() @@ -331,15 +331,18 @@ func (p *BinaryFile[F]) Trace(input map[string][]byte, cfg vm.TraceConfig, WithParallelism(cfg.Parallelism()). WithBatchSize(cfg.BatchSize()). WithPadding(cfg.PaddingStrategy()) - // Build the trace (finally) - rtr, berrs = builder.Build(constraints, rtr) - // Include any builder errors - errs = append(errs, berrs...) + // Expand shards one-by-one + for i, shard := range trace { + // Build the trace (finally) + trace[i], berrs = builder.Build(constraints, shard) + // Include any builder errors + errs = append(errs, berrs...) + } } // - stats.Log("Trace generation") + stats.Log(fmt.Sprintf("Trace generation (%d shards)", len(trace))) // - return output, rtr, errs + return output, trace, errs } // ============================================================================ diff --git a/pkg/zkc/constraints/call_and_memory_lookup.go b/pkg/zkc/constraints/call_and_memory_lookup.go index b347b1241..0efeb29f3 100644 --- a/pkg/zkc/constraints/call_and_memory_lookup.go +++ b/pkg/zkc/constraints/call_and_memory_lookup.go @@ -80,8 +80,13 @@ func addLookups[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir.Const for _, entry := range group.entries { switch c := entry.code.(type) { case *vm.BytecodeCall[W]: + // TODO: put global functions "on the bus" + // + // var global = infos[c.Target].(*vm.Function[W]).Kind().IsGlobal() + // emitCallLookup(mod, ctx, uint(pc), uint(c.Target), toRegisterIds(c.Arguments), toRegisterIds(c.Returns), srcSelector, infos) + case *vm.BytecodeReadWrite[W]: if infos[c.Id].(*vm.Memory[W]).IsReadWrite() { emitRamLookup(mod, ctx, uint(pc), entry.cc, c, srcSelector, infos, field) diff --git a/pkg/zkc/constraints/trace/builder.go b/pkg/zkc/constraints/trace/builder.go index 2a8b10389..9967ac09c 100644 --- a/pkg/zkc/constraints/trace/builder.go +++ b/pkg/zkc/constraints/trace/builder.go @@ -147,7 +147,7 @@ func (p Builder[W, F, M]) Init(program vm.Program[W]) Builder[W, F, M] { } // Build implementation for TraceBuilder interface. -func (p Builder[W, F, M]) Build() trace.Trace[F] { +func (p Builder[W, F, M]) Build() trace.Shard[F] { return trace.NewArray(p.modules) } diff --git a/pkg/zkc/vm/internal/descriptor/function_kind.go b/pkg/zkc/vm/internal/descriptor/function_kind.go index fbdcfe74b..68211841c 100644 --- a/pkg/zkc/vm/internal/descriptor/function_kind.go +++ b/pkg/zkc/vm/internal/descriptor/function_kind.go @@ -19,7 +19,7 @@ import ( // FunctionKind captures the execution-relevant properties of a function. type FunctionKind struct { - native, unsafeArgs, inline, never bool + native, unsafeArgs, inline, never, global bool } // IsNative reports whether this function is backed by a native circuit rather @@ -28,6 +28,11 @@ func (p FunctionKind) IsNative() bool { return p.native } +// IsGlobal reports whether this function must support cross-shard calls (or not). +func (p FunctionKind) IsGlobal() bool { + return p.global +} + // CanInline reports whether or not this function was marked as inlineable or // not. func (p FunctionKind) CanInline() bool { @@ -61,6 +66,14 @@ func (p FunctionKind) WithNative(flag bool) FunctionKind { return p } +// WithGlobal updates this kind as to whether it represents a global function, +// or not. +func (p FunctionKind) WithGlobal(flag bool) FunctionKind { + p.global = flag + // + return p +} + // WithUnsafeArgs updates the specification as to whether this support unsafe // args, or not. func (p FunctionKind) WithUnsafeArgs(flag bool) FunctionKind { @@ -133,5 +146,5 @@ func (p *FunctionKind) GobDecode(data []byte) error { var ( // BYTECODE_FUNCTION represents a safe function implemented by bytecode. - BYTECODE_FUNCTION = FunctionKind{false, false, false, false} + BYTECODE_FUNCTION = FunctionKind{false, false, false, false, false} ) diff --git a/pkg/zkc/vm/internal/interpreter/encoding/common.go b/pkg/zkc/vm/internal/interpreter/encoding/common.go index e6476be70..2c9d10ead 100644 --- a/pkg/zkc/vm/internal/interpreter/encoding/common.go +++ b/pkg/zkc/vm/internal/interpreter/encoding/common.go @@ -274,10 +274,7 @@ const ( XORC // TAILCALL_n instruction: a call in tail position, sharing ENTER_n's // payload layout but executed differently. Emitted only for calls to - // no-return functions, which never return to their caller: rather than - // allocating a fresh frame and pushing a call-stack record, the caller's - // frame is zeroed and reused (resized to the callee's width) with the - // arguments copied into place. + // no-return functions, which never return to their caller. TAILCALL_n // TAILCALL_2 instruction: dedicated (narrow-only) encoding of TAILCALL_n // for the common single-argument call, exactly as ENTER_2 is to ENTER_n. @@ -415,10 +412,7 @@ const ( WIDE_ORC // WIDE_XORC (xor with constant) instruction [must follow WIDE_ORC] WIDE_XORC - // WIDE_TAILCALL_n instruction: the wide form of TAILCALL_n, exactly as - // WIDE_ENTER_n is to ENTER_n. There is no wide form of TAILCALL_2, just - // as there is none for ENTER_2: a frame width or argument register which - // doesn't fit falls back to the general TAILCALL_n encoding instead. + // WIDE_TAILCALL_n instruction: WIDE_TAILCALL_n // MAX_WIDE_BYTECODE diff --git a/pkg/zkc/vm/trace_builder.go b/pkg/zkc/vm/trace_builder.go index c71af11db..ccae95537 100644 --- a/pkg/zkc/vm/trace_builder.go +++ b/pkg/zkc/vm/trace_builder.go @@ -14,13 +14,12 @@ package vm import ( "github.com/LFDT-Lineth/zkc/pkg/trace" - "github.com/LFDT-Lineth/zkc/pkg/util" "github.com/LFDT-Lineth/zkc/pkg/util/collection/array" "github.com/LFDT-Lineth/zkc/pkg/util/field" ) // Trace defines the type of a general trace -type Trace[F field.Element[F]] = trace.Trace[F] +type Trace[F field.Element[F]] = trace.Shard[F] // Element defines the type of field elements type Element[F any] = field.Element[F] @@ -35,7 +34,7 @@ type Tracer[W Word[W], F Element[F], T any] interface { // Construct the trace for a given memory of some kind TraceMemory(mid uint16, m RuntimeMemory[W], cfg field.Config) // Build the final trace - Build() trace.Trace[F] + Build() trace.Shard[F] } // TraceBuilder provides a generic mechanism for tracing a given program, and @@ -59,42 +58,22 @@ func NewTraceBuilder[W Word[W], F Element[F], T Tracer[W, F, T]](config TraceCon // the input is malformed (e.g. is missing expected fields and/or contains // unexpected fields). func (p TraceBuilder[W, F, T]) BootAndTrace(inputs map[string][]byte, -) (tr trace.Trace[F], outputs map[string][]byte, errors []error) { +) (shards trace.Trace[F], outputs map[string][]byte, errors []error) { // Check whether we have a sharding strategy if p.config.shardingStrategy.IsEmpty() { + var tr trace.Shard[F] // no strategy, therefore trace sequentially - return BootAndTrace[W, F, T](p.tracing, inputs) - } - // apply sharding strategy - shards, outputs, errors := p.checkpointAndTrace(inputs) - // Perform trace reduction - var stats = util.NewPerfStats() - // Recombine shards - if p.config.parallel { - // Parallel - tr = trace.ParallelReduce(shards) - // - stats.Log("Trace reduction (parallel)") - } else { - // Sequential - tr = trace.Reduce(shards) + tr, outputs, errors = BootAndTrace[W, F, T](p.tracing, inputs) // - stats.Log("Trace reduction (sequential)") + return trace.Trace[F]{tr}, outputs, errors } - // - return tr, outputs, errors -} - -// BootAndTraceShards shards generates a given number of shards from a given -// program. -func (p TraceBuilder[W, F, T]) BootAndTraceShards(inputs map[string][]byte, -) (traces []Trace[F], outputs map[string][]byte, errors []error) { - panic("todo") + // apply sharding strategy + return p.bootAndTraceShards(inputs) } -// Parallel BootAndTrace performs sharding according to the given sharding +// Sharded BootAndTrace performs sharding according to the given sharding // strategy. -func (p TraceBuilder[W, F, T]) checkpointAndTrace(inputs map[string][]byte, +func (p TraceBuilder[W, F, T]) bootAndTraceShards(inputs map[string][]byte, ) ([]Trace[F], map[string][]byte, []error) { var ( strategy = p.config.shardingStrategy.Unwrap() diff --git a/testdata/corset/invalid/bus_invalid_08.lisp b/testdata/corset/invalid/bus_invalid_08.lisp new file mode 100644 index 000000000..4e05922be --- /dev/null +++ b/testdata/corset/invalid/bus_invalid_08.lisp @@ -0,0 +1,3 @@ +;;error:3:1-25:bus "bus" has receives but no sends +(defcolumns (SEL :binary) (A :i16)) +(defrecv r1 bus SEL (A)) diff --git a/testdata/corset/valid/bus_01.accepts b/testdata/corset/valid/bus_01.accepts index 98ab67957..fd096d632 100644 --- a/testdata/corset/valid/bus_01.accepts +++ b/testdata/corset/valid/bus_01.accepts @@ -1,8 +1,16 @@ ;; single message, sent and received -{"alpha.SEL": [1], "alpha.A": [5], "alpha.B": [7], "beta.SEL": [1], "beta.X": [5], "beta.Y": [7]} +{"sndr.SEL": [1], "sndr.A": [5], "sndr.B": [7], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [7]} ;; order scrambled, junk on unselected row -{"alpha.SEL": [1,0,1], "alpha.A": [5,999,9], "alpha.B": [7,999,2], "beta.SEL": [1,1], "beta.X": [9,5], "beta.Y": [2,7]} +{"sndr.SEL": [1,0,1], "sndr.A": [5,999,9], "sndr.B": [7,999,2], "rcvr.SEL": [1,1], "rcvr.X": [9,5], "rcvr.Y": [2,7]} ;; duplicate message, twice sent and twice received -{"alpha.SEL": [1,1], "alpha.A": [5,5], "alpha.B": [7,7], "beta.SEL": [1,1], "beta.X": [5,5], "beta.Y": [7,7]} +{"sndr.SEL": [1,1], "sndr.A": [5,5], "sndr.B": [7,7], "rcvr.SEL": [1,1], "rcvr.X": [5,5], "rcvr.Y": [7,7]} ;; nothing on the bus at all, junk on every unselected row -{"alpha.SEL": [0,0], "alpha.A": [3,4], "alpha.B": [5,6], "beta.SEL": [0], "beta.X": [8], "beta.Y": [9]} +{"sndr.SEL": [0,0], "sndr.A": [3,4], "sndr.B": [5,6], "rcvr.SEL": [0], "rcvr.X": [8], "rcvr.Y": [9]} +;; mono-shard +[{"sndr.SEL": [1], "sndr.A": [5], "sndr.B": [7], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [7]}] +;; shard 1 sends, shard 2 receives; balanced together, not alone +[{"sndr.SEL": [1,1], "sndr.A": [5,9], "sndr.B": [7,2], "rcvr.SEL": [0], "rcvr.X": [0], "rcvr.Y": [0]}, {"sndr.SEL": [0], "sndr.A": [0], "sndr.B": [0], "rcvr.SEL": [1,1], "rcvr.X": [9,5], "rcvr.Y": [2,7]}] +;; duplicate message: sent twice in shard 1, received once in each shard +[{"sndr.SEL": [1,1], "sndr.A": [5,5], "sndr.B": [7,7], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [7]}, {"sndr.SEL": [0], "sndr.A": [0], "sndr.B": [0], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [7]}] +;; three shards of differing heights, all traffic crossing shard seams +[{"sndr.SEL": [1,0,1], "sndr.A": [5,0,9], "sndr.B": [7,0,2], "rcvr.SEL": [0], "rcvr.X": [0], "rcvr.Y": [0]}, {"sndr.SEL": [1], "sndr.A": [3], "sndr.B": [4], "rcvr.SEL": [1,0], "rcvr.X": [9,0], "rcvr.Y": [2,0]}, {"sndr.SEL": [0,0], "sndr.A": [0,0], "sndr.B": [0,0], "rcvr.SEL": [1,1], "rcvr.X": [5,3], "rcvr.Y": [7,4]}] diff --git a/testdata/corset/valid/bus_01.lisp b/testdata/corset/valid/bus_01.lisp index a2ddf93af..0e6bc4204 100644 --- a/testdata/corset/valid/bus_01.lisp +++ b/testdata/corset/valid/bus_01.lisp @@ -1,7 +1,7 @@ -(module alpha) +(module sndr) (defcolumns (SEL :binary) (A :i16) (B :i16)) (defsend s1 bus SEL (A B)) -(module beta) +(module rcvr) (defcolumns (SEL :binary) (X :i16) (Y :i16)) (defrecv r1 bus SEL (X Y)) diff --git a/testdata/corset/valid/bus_01.rejects b/testdata/corset/valid/bus_01.rejects index e4a28433b..34877f4f9 100644 --- a/testdata/corset/valid/bus_01.rejects +++ b/testdata/corset/valid/bus_01.rejects @@ -1,10 +1,16 @@ ;; send never received -{"alpha.SEL": [1], "alpha.A": [5], "alpha.B": [7], "beta.SEL": [0], "beta.X": [0], "beta.Y": [0]} +{"sndr.SEL": [1], "sndr.A": [5], "sndr.B": [7], "rcvr.SEL": [0], "rcvr.X": [0], "rcvr.Y": [0]} ;; receive never sent -{"alpha.SEL": [0], "alpha.A": [0], "alpha.B": [0], "beta.SEL": [1], "beta.X": [5], "beta.Y": [7]} +{"sndr.SEL": [0], "sndr.A": [0], "sndr.B": [0], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [7]} ;; two identical sends, only one receive -{"alpha.SEL": [1,1], "alpha.A": [5,5], "alpha.B": [7,7], "beta.SEL": [1], "beta.X": [5], "beta.Y": [7]} +{"sndr.SEL": [1,1], "sndr.A": [5,5], "sndr.B": [7,7], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [7]} ;; received value differs from sent value -{"alpha.SEL": [1], "alpha.A": [5], "alpha.B": [7], "beta.SEL": [1], "beta.X": [5], "beta.Y": [8]} +{"sndr.SEL": [1], "sndr.A": [5], "sndr.B": [7], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [8]} ;; same number of messages on both sides, but counts per message differ -{"alpha.SEL": [1,1], "alpha.A": [5,9], "alpha.B": [7,2], "beta.SEL": [1,1], "beta.X": [5,5], "beta.Y": [7,7]} +{"sndr.SEL": [1,1], "sndr.A": [5,9], "sndr.B": [7,2], "rcvr.SEL": [1,1], "rcvr.X": [5,5], "rcvr.Y": [7,7]} +;; each shard clean on its own, but the received value differs from the sent one +[{"sndr.SEL": [1], "sndr.A": [5], "sndr.B": [7], "rcvr.SEL": [0], "rcvr.X": [0], "rcvr.Y": [0]}, {"sndr.SEL": [0], "sndr.A": [0], "sndr.B": [0], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [8]}] +;; two sends across the group, three receives of the same message +[{"sndr.SEL": [1,1], "sndr.A": [5,5], "sndr.B": [7,7], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [7]}, {"sndr.SEL": [0], "sndr.A": [0], "sndr.B": [0], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [7]}, {"sndr.SEL": [0], "sndr.A": [0], "sndr.B": [0], "rcvr.SEL": [1], "rcvr.X": [5], "rcvr.Y": [7]}] +;; a single-shard group that does not balance +[{"sndr.SEL": [1], "sndr.A": [5], "sndr.B": [7], "rcvr.SEL": [0], "rcvr.X": [0], "rcvr.Y": [0]}] diff --git a/testdata/corset/valid/bus_01.shards.accepts b/testdata/corset/valid/bus_01.shards.accepts deleted file mode 100644 index 4e5d0217f..000000000 --- a/testdata/corset/valid/bus_01.shards.accepts +++ /dev/null @@ -1,8 +0,0 @@ -;; a group of one: must balance like a plain trace -[{"alpha.SEL": [1], "alpha.A": [5], "alpha.B": [7], "beta.SEL": [1], "beta.X": [5], "beta.Y": [7]}] -;; shard 1 only sends, shard 2 only receives; balanced together, not alone -[{"alpha.SEL": [1,1], "alpha.A": [5,9], "alpha.B": [7,2], "beta.SEL": [0], "beta.X": [0], "beta.Y": [0]}, {"alpha.SEL": [0], "alpha.A": [0], "alpha.B": [0], "beta.SEL": [1,1], "beta.X": [9,5], "beta.Y": [2,7]}] -;; duplicate message: sent twice in shard 1, received once in each shard -[{"alpha.SEL": [1,1], "alpha.A": [5,5], "alpha.B": [7,7], "beta.SEL": [1], "beta.X": [5], "beta.Y": [7]}, {"alpha.SEL": [0], "alpha.A": [0], "alpha.B": [0], "beta.SEL": [1], "beta.X": [5], "beta.Y": [7]}] -;; three shards of differing heights, all traffic crossing shard seams -[{"alpha.SEL": [1,0,1], "alpha.A": [5,0,9], "alpha.B": [7,0,2], "beta.SEL": [0], "beta.X": [0], "beta.Y": [0]}, {"alpha.SEL": [1], "alpha.A": [3], "alpha.B": [4], "beta.SEL": [1,0], "beta.X": [9,0], "beta.Y": [2,0]}, {"alpha.SEL": [0,0], "alpha.A": [0,0], "alpha.B": [0,0], "beta.SEL": [1,1], "beta.X": [5,3], "beta.Y": [7,4]}] diff --git a/testdata/corset/valid/bus_01.shards.rejects b/testdata/corset/valid/bus_01.shards.rejects deleted file mode 100644 index 8f338f37a..000000000 --- a/testdata/corset/valid/bus_01.shards.rejects +++ /dev/null @@ -1,6 +0,0 @@ -;; each shard clean on its own, but the received value differs from the sent one -[{"alpha.SEL": [1], "alpha.A": [5], "alpha.B": [7], "beta.SEL": [0], "beta.X": [0], "beta.Y": [0]}, {"alpha.SEL": [0], "alpha.A": [0], "alpha.B": [0], "beta.SEL": [1], "beta.X": [5], "beta.Y": [8]}] -;; two sends across the group, three receives of the same message -[{"alpha.SEL": [1,1], "alpha.A": [5,5], "alpha.B": [7,7], "beta.SEL": [1], "beta.X": [5], "beta.Y": [7]}, {"alpha.SEL": [0], "alpha.A": [0], "alpha.B": [0], "beta.SEL": [1], "beta.X": [5], "beta.Y": [7]}, {"alpha.SEL": [0], "alpha.A": [0], "alpha.B": [0], "beta.SEL": [1], "beta.X": [5], "beta.Y": [7]}] -;; a single-shard group that does not balance -[{"alpha.SEL": [1], "alpha.A": [5], "alpha.B": [7], "beta.SEL": [0], "beta.X": [0], "beta.Y": [0]}] diff --git a/testdata/corset/valid/bus_02.accepts b/testdata/corset/valid/bus_02.accepts index 1ea29e24a..5625afd77 100644 --- a/testdata/corset/valid/bus_02.accepts +++ b/testdata/corset/valid/bus_02.accepts @@ -1,6 +1,6 @@ ;; one message per bus, each answered on its own bus -{"alpha.S1": [1,0], "alpha.S2": [0,1], "alpha.A": [5,9], "beta.R1": [1,0], "beta.R2": [0,1], "beta.X": [5,9]} +{"sndr.S1": [1,0], "sndr.S2": [0,1], "sndr.A": [5,9], "rcvr.R1": [1,0], "rcvr.R2": [0,1], "rcvr.X": [5,9]} ;; same value on both buses simultaneously -{"alpha.S1": [1], "alpha.S2": [1], "alpha.A": [5], "beta.R1": [1], "beta.R2": [1], "beta.X": [5]} +{"sndr.S1": [1], "sndr.S2": [1], "sndr.A": [5], "rcvr.R1": [1], "rcvr.R2": [1], "rcvr.X": [5]} ;; both buses empty -{"alpha.S1": [0], "alpha.S2": [0], "alpha.A": [7], "beta.R1": [0], "beta.R2": [0], "beta.X": [7]} +{"sndr.S1": [0], "sndr.S2": [0], "sndr.A": [7], "rcvr.R1": [0], "rcvr.R2": [0], "rcvr.X": [7]} diff --git a/testdata/corset/valid/bus_02.lisp b/testdata/corset/valid/bus_02.lisp index c4fd51691..e26d65346 100644 --- a/testdata/corset/valid/bus_02.lisp +++ b/testdata/corset/valid/bus_02.lisp @@ -1,9 +1,9 @@ -(module alpha) +(module sndr) (defcolumns (S1 :binary) (S2 :binary) (A :i16)) (defsend s1 bus1 S1 (A)) (defsend s2 bus2 S2 (A)) -(module beta) +(module rcvr) (defcolumns (R1 :binary) (R2 :binary) (X :i16)) (defrecv r1 bus1 R1 (X)) (defrecv r2 bus2 R2 (X)) diff --git a/testdata/corset/valid/bus_02.rejects b/testdata/corset/valid/bus_02.rejects index 7a5dcd9e2..5173cb60b 100644 --- a/testdata/corset/valid/bus_02.rejects +++ b/testdata/corset/valid/bus_02.rejects @@ -1,4 +1,4 @@ ;; send on bus1 answered on bus2 - buses must not cancel against each other -{"alpha.S1": [1], "alpha.S2": [0], "alpha.A": [5], "beta.R1": [0], "beta.R2": [1], "beta.X": [5]} +{"sndr.S1": [1], "sndr.S2": [0], "sndr.A": [5], "rcvr.R1": [0], "rcvr.R2": [1], "rcvr.X": [5]} ;; bus1 balanced, bus2 not -{"alpha.S1": [1], "alpha.S2": [1], "alpha.A": [5], "beta.R1": [1], "beta.R2": [0], "beta.X": [5]} +{"sndr.S1": [1], "sndr.S2": [1], "sndr.A": [5], "rcvr.R1": [1], "rcvr.R2": [0], "rcvr.X": [5]} diff --git a/testdata/corset/valid/bus_03.accepts b/testdata/corset/valid/bus_03.accepts index 1baae647b..bbf73484d 100644 --- a/testdata/corset/valid/bus_03.accepts +++ b/testdata/corset/valid/bus_03.accepts @@ -2,3 +2,5 @@ {"s1.SEL": [1,1], "s1.A": [5,4], "s1.B": [7,4], "s2.SEL": [1,1], "s2.A": [9,4], "s2.B": [2,4], "r1.SEL": [1,1], "r1.X": [4,9], "r1.Y": [4,2], "r2.SEL": [1,1], "r2.X": [4,5], "r2.Y": [4,7]} ;; single sender active, single receiver active {"s1.SEL": [1], "s1.A": [5], "s1.B": [7], "s2.SEL": [0], "s2.A": [0], "s2.B": [0], "r1.SEL": [0], "r1.X": [0], "r1.Y": [0], "r2.SEL": [1], "r2.X": [5], "r2.Y": [7]} +;; four modules, three shards: (5,7) goes s1@shard1 -> r2@shard3, (9,2) goes s2@shard2 -> r1@shard2 (intra-shard), (4,4) goes s2@shard1 -> r1@shard3 +[{"s1.SEL": [1], "s1.A": [5], "s1.B": [7], "s2.SEL": [1], "s2.A": [4], "s2.B": [4], "r1.SEL": [0], "r1.X": [0], "r1.Y": [0], "r2.SEL": [0], "r2.X": [0], "r2.Y": [0]}, {"s1.SEL": [0], "s1.A": [0], "s1.B": [0], "s2.SEL": [1], "s2.A": [9], "s2.B": [2], "r1.SEL": [1], "r1.X": [9], "r1.Y": [2], "r2.SEL": [0], "r2.X": [0], "r2.Y": [0]}, {"s1.SEL": [0], "s1.A": [0], "s1.B": [0], "s2.SEL": [0], "s2.A": [0], "s2.B": [0], "r1.SEL": [1], "r1.X": [4], "r1.Y": [4], "r2.SEL": [1], "r2.X": [5], "r2.Y": [7]}] diff --git a/testdata/corset/valid/bus_03.rejects b/testdata/corset/valid/bus_03.rejects index 5ba19bb96..dcea99a04 100644 --- a/testdata/corset/valid/bus_03.rejects +++ b/testdata/corset/valid/bus_03.rejects @@ -1,2 +1,4 @@ ;; as the balanced fan-in/fan-out case, except one copy of the duplicated (4,4) is not received {"s1.SEL": [1,1], "s1.A": [5,4], "s1.B": [7,4], "s2.SEL": [1,1], "s2.A": [9,4], "s2.B": [2,4], "r1.SEL": [1,1], "r1.X": [4,9], "r1.Y": [4,2], "r2.SEL": [0,1], "r2.X": [4,5], "r2.Y": [4,7]} +;; as the accepted three-shard case, except the cross-shard message (5,7) is never received (r2 inactive in shard 3) +[{"s1.SEL": [1], "s1.A": [5], "s1.B": [7], "s2.SEL": [1], "s2.A": [4], "s2.B": [4], "r1.SEL": [0], "r1.X": [0], "r1.Y": [0], "r2.SEL": [0], "r2.X": [0], "r2.Y": [0]}, {"s1.SEL": [0], "s1.A": [0], "s1.B": [0], "s2.SEL": [1], "s2.A": [9], "s2.B": [2], "r1.SEL": [1], "r1.X": [9], "r1.Y": [2], "r2.SEL": [0], "r2.X": [0], "r2.Y": [0]}, {"s1.SEL": [0], "s1.A": [0], "s1.B": [0], "s2.SEL": [0], "s2.A": [0], "s2.B": [0], "r1.SEL": [1], "r1.X": [4], "r1.Y": [4], "r2.SEL": [0], "r2.X": [5], "r2.Y": [7]}] diff --git a/testdata/corset/valid/bus_03.shards.accepts b/testdata/corset/valid/bus_03.shards.accepts deleted file mode 100644 index 1b3148ed1..000000000 --- a/testdata/corset/valid/bus_03.shards.accepts +++ /dev/null @@ -1,2 +0,0 @@ -;; four modules, three shards: (5,7) goes s1@shard1 -> r2@shard3, (9,2) goes s2@shard2 -> r1@shard2 (intra-shard), (4,4) goes s2@shard1 -> r1@shard3 -[{"s1.SEL": [1], "s1.A": [5], "s1.B": [7], "s2.SEL": [1], "s2.A": [4], "s2.B": [4], "r1.SEL": [0], "r1.X": [0], "r1.Y": [0], "r2.SEL": [0], "r2.X": [0], "r2.Y": [0]}, {"s1.SEL": [0], "s1.A": [0], "s1.B": [0], "s2.SEL": [1], "s2.A": [9], "s2.B": [2], "r1.SEL": [1], "r1.X": [9], "r1.Y": [2], "r2.SEL": [0], "r2.X": [0], "r2.Y": [0]}, {"s1.SEL": [0], "s1.A": [0], "s1.B": [0], "s2.SEL": [0], "s2.A": [0], "s2.B": [0], "r1.SEL": [1], "r1.X": [4], "r1.Y": [4], "r2.SEL": [1], "r2.X": [5], "r2.Y": [7]}] diff --git a/testdata/corset/valid/bus_03.shards.rejects b/testdata/corset/valid/bus_03.shards.rejects deleted file mode 100644 index 0fe9013cb..000000000 --- a/testdata/corset/valid/bus_03.shards.rejects +++ /dev/null @@ -1,2 +0,0 @@ -;; as the accepted three-shard case, except the cross-shard message (5,7) is never received (r2 inactive in shard 3) -[{"s1.SEL": [1], "s1.A": [5], "s1.B": [7], "s2.SEL": [1], "s2.A": [4], "s2.B": [4], "r1.SEL": [0], "r1.X": [0], "r1.Y": [0], "r2.SEL": [0], "r2.X": [0], "r2.Y": [0]}, {"s1.SEL": [0], "s1.A": [0], "s1.B": [0], "s2.SEL": [1], "s2.A": [9], "s2.B": [2], "r1.SEL": [1], "r1.X": [9], "r1.Y": [2], "r2.SEL": [0], "r2.X": [0], "r2.Y": [0]}, {"s1.SEL": [0], "s1.A": [0], "s1.B": [0], "s2.SEL": [0], "s2.A": [0], "s2.B": [0], "r1.SEL": [1], "r1.X": [4], "r1.Y": [4], "r2.SEL": [0], "r2.X": [5], "r2.Y": [7]}] diff --git a/testdata/corset/valid/bus_05.shards.accepts b/testdata/corset/valid/bus_05.accepts similarity index 100% rename from testdata/corset/valid/bus_05.shards.accepts rename to testdata/corset/valid/bus_05.accepts diff --git a/testdata/corset/valid/bus_05.shards.rejects b/testdata/corset/valid/bus_05.rejects similarity index 100% rename from testdata/corset/valid/bus_05.shards.rejects rename to testdata/corset/valid/bus_05.rejects diff --git a/testdata/corset/valid/bus_06.accepts b/testdata/corset/valid/bus_06.accepts new file mode 100644 index 000000000..5f0a90569 --- /dev/null +++ b/testdata/corset/valid/bus_06.accepts @@ -0,0 +1,80 @@ +{ "send": [0], "recv": [0], "data": [0] } +{ "send": [0], "recv": [0], "data": [1] } +{ "send": [0], "recv": [0], "data": [2] } +{ "send": [0], "recv": [0], "data": [3] } +{ "send": [0], "recv": [0], "data": [4] } +{ "send": [1,0], "recv": [0,1], "data": [23,23] } +{ "send": [0,1], "recv": [1,0], "data": [23,23] } +{ "send": [1,0], "recv": [0,1], "data": [87,87] } +{ "send": [0,1], "recv": [1,0], "data": [87,87] } +{ "send": [1,0], "recv": [0,1], "data": [128,128] } +{ "send": [0,1], "recv": [1,0], "data": [128,128] } +{ "send": [0,1,0], "recv": [0,0,1], "data": [0,23,23] } +{ "send": [0,0,1], "recv": [0,1,0], "data": [0,23,23] } +{ "send": [1,0,0], "recv": [0,0,1], "data": [54,0,54] } +{ "send": [0,0,1], "recv": [1,0,0], "data": [54,0,54] } +{ "send": [1,0,0], "recv": [0,1,0], "data": [9,9,0] } +{ "send": [0,1,0], "recv": [1,0,0], "data": [9,9,0] } +{ "send": [0,1,0], "recv": [0,0,1], "data": [3,23,23] } +{ "send": [0,0,1], "recv": [0,1,0], "data": [3,23,23] } +{ "send": [1,0,0], "recv": [0,0,1], "data": [54,3,54] } +{ "send": [0,0,1], "recv": [1,0,0], "data": [54,3,54] } +{ "send": [1,0,0], "recv": [0,1,0], "data": [9,9,3] } +{ "send": [0,1,0], "recv": [1,0,0], "data": [9,9,3] } +{ "send": [0,1,0], "recv": [0,0,1], "data": [125,23,23] } +{ "send": [0,0,1], "recv": [0,1,0], "data": [125,23,23] } +{ "send": [1,0,0], "recv": [0,0,1], "data": [54,125,54] } +{ "send": [0,0,1], "recv": [1,0,0], "data": [54,125,54] } +{ "send": [1,0,0], "recv": [0,1,0], "data": [9,9,125] } +{ "send": [0,1,0], "recv": [1,0,0], "data": [9,9,125] } +;; +{ "send": [1,1,0,0], "recv": [0,0,1,1], "data": [7,7,7,7] } +{ "send": [1,0,1,0], "recv": [0,1,0,1], "data": [7,7,7,7] } +{ "send": [0,1,1,0], "recv": [1,0,0,1], "data": [7,7,7,7] } +{ "send": [0,1,0,1], "recv": [1,0,1,0], "data": [7,7,7,7] } +{ "send": [0,0,1,1], "recv": [1,1,0,0], "data": [7,7,7,7] } +;; +{ "send": [0,1,1,0,0], "recv": [0,0,0,1,1], "data": [1,7,7,7,7] } +{ "send": [0,1,0,1,0], "recv": [0,0,1,0,1], "data": [2,7,7,7,7] } +{ "send": [0,0,1,1,0], "recv": [0,1,0,0,1], "data": [3,7,7,7,7] } +{ "send": [0,0,1,0,1], "recv": [0,1,0,1,0], "data": [4,7,7,7,7] } +{ "send": [0,0,0,1,1], "recv": [0,1,1,0,0], "data": [5,7,7,7,7] } +{ "send": [1,0,1,0,0], "recv": [0,0,0,1,1], "data": [7,1,7,7,7] } +{ "send": [1,0,0,1,0], "recv": [0,0,1,0,1], "data": [7,2,7,7,7] } +{ "send": [0,0,1,1,0], "recv": [1,0,0,0,1], "data": [7,3,7,7,7] } +{ "send": [0,0,1,0,1], "recv": [1,0,0,1,0], "data": [7,4,7,7,7] } +{ "send": [0,0,0,1,1], "recv": [1,0,1,0,0], "data": [7,5,7,7,7] } +{ "send": [1,1,0,0,0], "recv": [0,0,0,1,1], "data": [7,7,1,7,7] } +{ "send": [1,0,0,1,0], "recv": [0,1,0,0,1], "data": [7,7,2,7,7] } +{ "send": [0,1,0,1,0], "recv": [1,0,0,0,1], "data": [7,7,3,7,7] } +{ "send": [0,1,0,0,1], "recv": [1,0,0,1,0], "data": [7,7,4,7,7] } +{ "send": [0,0,0,1,1], "recv": [1,1,0,0,0], "data": [7,7,5,7,7] } +{ "send": [1,1,0,0,0], "recv": [0,0,1,0,1], "data": [7,7,7,1,7] } +{ "send": [1,0,1,0,0], "recv": [0,1,0,0,1], "data": [7,7,7,2,7] } +{ "send": [0,1,1,0,0], "recv": [1,0,0,0,1], "data": [7,7,7,3,7] } +{ "send": [0,1,0,0,1], "recv": [1,0,1,0,0], "data": [7,7,7,4,7] } +{ "send": [0,0,1,0,1], "recv": [1,1,0,0,0], "data": [7,7,7,5,7] } +{ "send": [1,1,0,0,0], "recv": [0,0,1,1,0], "data": [7,7,7,7,1] } +{ "send": [1,0,1,0,0], "recv": [0,1,0,1,0], "data": [7,7,7,7,2] } +{ "send": [0,1,1,0,0], "recv": [1,0,0,1,0], "data": [7,7,7,7,3] } +{ "send": [0,1,0,1,0], "recv": [1,0,1,0,0], "data": [7,7,7,7,4] } +{ "send": [0,0,1,1,0], "recv": [1,1,0,0,0], "data": [7,7,7,7,5] } +;; +{ "send": [1,1,1,0,0,0], "recv": [0,0,0,1,1,1], "data": [1,2,3,3,2,1] } +{ "send": [1,1,1,0,0,0], "recv": [0,0,0,1,1,1], "data": [3,2,1,3,2,1] } +{ "send": [1,1,1,0,0,0], "recv": [0,0,0,1,1,1], "data": [3,1,2,3,2,1] } +{ "send": [1,1,1,0,0,0], "recv": [0,0,0,1,1,1], "data": [2,2,3,3,2,2] } +{ "send": [1,1,1,0,0,0], "recv": [0,0,0,1,1,1], "data": [2,3,2,3,2,2] } +{ "send": [1,1,1,0,0,0], "recv": [0,0,0,1,1,1], "data": [3,2,2,3,2,2] } +;; +{ "send": [1,1,0,1,0,0], "recv": [0,0,1,0,1,1], "data": [1,2,3,3,2,1] } +{ "send": [1,1,0,1,0,0], "recv": [0,0,1,0,1,1], "data": [2,2,3,3,2,2] } +{ "send": [1,1,0,1,0,0], "recv": [0,0,1,0,1,1], "data": [2,2,2,3,3,2] } +{ "send": [1,1,0,1,0,0], "recv": [0,0,1,0,1,1], "data": [2,2,2,3,2,3] } +;; Shards +[{ "send": [1], "recv": [0], "data": [23] },{ "send": [0], "recv": [1], "data": [23] }] +[{ "send": [1,0], "recv": [0,1], "data": [23,46] },{ "send": [0,1], "recv": [1,0], "data": [23,46] }] +[{ "send": [1,0], "recv": [0,1], "data": [23,46] },{ "send": [0,1], "recv": [1,0], "data": [23,52] },{ "send": [0,1], "recv": [1,0], "data": [52,46] }] +[{ "send": [1,1], "recv": [0,0], "data": [23,46] },{ "send": [0], "recv": [1], "data": [23] },{ "send": [0], "recv": [1], "data": [46] }] +[{ "send": [1,1], "recv": [0,0], "data": [23,46] },{ "send": [0,0], "recv": [1,1], "data": [23,46] },{ "send": [], "recv": [], "data": [] }] +[{ "send": [1,1], "recv": [0,0], "data": [23,46] },{ "send": [0,0], "recv": [1,1], "data": [23,46] },{ "send": [0], "recv": [0], "data": [123] }] diff --git a/testdata/corset/valid/bus_06.lisp b/testdata/corset/valid/bus_06.lisp new file mode 100644 index 000000000..b943e7573 --- /dev/null +++ b/testdata/corset/valid/bus_06.lisp @@ -0,0 +1,7 @@ +(defcolumns (send :binary) (recv :binary) (data :i16)) +;; Cannot simultaneously send/receive +(defconstraint xor () (== 0 (* send recv))) +;; Send data item when send line is high +(defsend s1 bus send (data)) +;; Receive data item when recv line is high +(defrecv r1 bus recv (data)) diff --git a/testdata/corset/valid/bus_06.rejects b/testdata/corset/valid/bus_06.rejects new file mode 100644 index 000000000..02e41512f --- /dev/null +++ b/testdata/corset/valid/bus_06.rejects @@ -0,0 +1,81 @@ +{ "send": [1], "recv": [1], "data": [23] } +{ "send": [1], "recv": [0], "data": [23] } +{ "send": [0], "recv": [1], "data": [23] } +;; +{ "send": [1,0], "recv": [0,1], "data": [23,22] } +{ "send": [0,1], "recv": [1,0], "data": [22,23] } +{ "send": [1,0], "recv": [0,1], "data": [89,87] } +{ "send": [0,1], "recv": [1,0], "data": [87,12] } +{ "send": [1,0], "recv": [0,1], "data": [128,0] } +{ "send": [0,1], "recv": [1,0], "data": [128,18] } +{ "send": [0,1,0], "recv": [0,0,1], "data": [0,22,23] } +{ "send": [0,0,1], "recv": [0,1,0], "data": [0,23,21] } +{ "send": [1,0,0], "recv": [0,0,1], "data": [54,0,51] } +{ "send": [0,0,1], "recv": [1,0,0], "data": [54,0,50] } +{ "send": [1,0,0], "recv": [0,1,0], "data": [9,8,0] } +{ "send": [0,1,0], "recv": [1,0,0], "data": [6,9,0] } +{ "send": [0,1,0], "recv": [0,0,1], "data": [3,24,23] } +{ "send": [0,0,1], "recv": [0,1,0], "data": [3,23,24] } +{ "send": [1,0,0], "recv": [0,0,1], "data": [54,3,53] } +{ "send": [0,0,1], "recv": [1,0,0], "data": [53,3,54] } +{ "send": [1,0,0], "recv": [0,1,0], "data": [10,9,3] } +{ "send": [0,1,0], "recv": [1,0,0], "data": [9,1,3] } +{ "send": [0,1,0], "recv": [0,0,1], "data": [125,21,23] } +{ "send": [0,0,1], "recv": [0,1,0], "data": [125,2,23] } +{ "send": [1,0,0], "recv": [0,0,1], "data": [5,125,54] } +{ "send": [0,0,1], "recv": [1,0,0], "data": [54,125,4] } +{ "send": [1,0,0], "recv": [0,1,0], "data": [9,8,125] } +{ "send": [0,1,0], "recv": [1,0,0], "data": [8,9,125] } +{ "send": [0,1,1], "recv": [1,0,0], "data": [8,9,125] } +{ "send": [0,1,1], "recv": [1,0,0], "data": [9,9,125] } +;; +{ "send": [1,1,0,0], "recv": [0,0,1,1], "data": [7,6,7,7] } +{ "send": [1,0,1,0], "recv": [0,1,0,1], "data": [7,7,4,7] } +{ "send": [0,1,1,0], "recv": [1,0,0,1], "data": [7,3,7,7] } +{ "send": [0,1,0,1], "recv": [1,0,1,0], "data": [7,7,2,7] } +{ "send": [0,0,1,1], "recv": [1,1,0,0], "data": [7,1,7,7] } + +{ "send": [1,1,0,0], "recv": [0,0,1,1], "data": [7,6,5,7] } +{ "send": [1,0,1,0], "recv": [0,1,0,1], "data": [1,7,4,7] } +{ "send": [0,1,1,0], "recv": [1,0,0,1], "data": [2,3,7,7] } +{ "send": [0,1,0,1], "recv": [1,0,1,0], "data": [7,3,2,7] } +{ "send": [0,0,1,1], "recv": [1,1,0,0], "data": [7,1,7,2] } +;; +{ "send": [0,1,1,0,0], "recv": [0,0,0,1,1], "data": [1,1,7,7,7] } +{ "send": [0,1,0,1,0], "recv": [0,0,1,0,1], "data": [2,7,2,7,7] } +{ "send": [0,0,1,1,0], "recv": [0,1,0,0,1], "data": [3,7,7,3,7] } +{ "send": [0,0,1,0,1], "recv": [0,1,0,1,0], "data": [4,7,7,7,4] } +{ "send": [0,0,0,1,1], "recv": [0,1,1,0,0], "data": [5,7,7,3,7] } +{ "send": [1,0,1,0,0], "recv": [0,0,0,1,1], "data": [7,1,2,7,7] } +{ "send": [1,0,0,1,0], "recv": [0,0,1,0,1], "data": [7,2,3,7,7] } +{ "send": [0,0,1,1,0], "recv": [1,0,0,0,1], "data": [1,3,7,7,7] } +{ "send": [0,0,1,0,1], "recv": [1,0,0,1,0], "data": [7,4,3,7,7] } +{ "send": [0,0,0,1,1], "recv": [1,0,1,0,0], "data": [7,5,1,7,7] } +{ "send": [1,1,0,0,0], "recv": [0,0,0,1,1], "data": [7,7,1,4,7] } +{ "send": [1,0,0,1,0], "recv": [0,1,0,0,1], "data": [7,7,2,7,5] } +{ "send": [0,1,0,1,0], "recv": [1,0,0,0,1], "data": [1,7,3,7,7] } +{ "send": [0,1,0,0,1], "recv": [1,0,0,1,0], "data": [7,2,4,7,7] } +{ "send": [0,0,0,1,1], "recv": [1,1,0,0,0], "data": [6,6,5,7,7] } +{ "send": [1,1,0,0,0], "recv": [0,0,1,0,1], "data": [7,7,3,1,7] } +{ "send": [1,0,1,0,0], "recv": [0,1,0,0,1], "data": [7,4,7,2,7] } +{ "send": [0,1,1,0,0], "recv": [1,0,0,0,1], "data": [7,7,5,3,7] } +{ "send": [0,1,0,0,1], "recv": [1,0,1,0,0], "data": [7,7,4,4,7] } +{ "send": [0,0,1,0,1], "recv": [1,1,0,0,0], "data": [7,7,5,5,7] } +{ "send": [1,1,0,0,0], "recv": [0,0,1,1,0], "data": [7,7,1,7,1] } +{ "send": [1,0,1,0,0], "recv": [0,1,0,1,0], "data": [7,2,7,7,2] } +{ "send": [0,1,1,0,0], "recv": [1,0,0,1,0], "data": [2,7,7,7,3] } +{ "send": [0,1,0,1,0], "recv": [1,0,1,0,0], "data": [2,7,2,7,4] } +{ "send": [0,0,1,1,0], "recv": [1,1,0,0,0], "data": [7,7,1,7,5] } +;; Shards +[{ "send": [1], "recv": [0], "data": [23] },{ "send": [0], "recv": [1], "data": [24] }] +[{ "send": [1], "recv": [0], "data": [23] },{ "send": [1], "recv": [0], "data": [23] }] +[{ "send": [1], "recv": [0], "data": [23] },{ "send": [0], "recv": [0], "data": [23] }] +[{ "send": [1,1], "recv": [0,0], "data": [23,24] },{ "send": [0], "recv": [0], "data": [23] }] +[{ "send": [1,1], "recv": [0,0], "data": [23,24] },{ "send": [1], "recv": [0], "data": [23] }] +[{ "send": [1,1], "recv": [0,0], "data": [23,24] },{ "send": [0], "recv": [1], "data": [23] }] +[{ "send": [1,1], "recv": [0,0], "data": [23,24] },{ "send": [0], "recv": [1], "data": [24] }] +[{ "send": [1,0], "recv": [0,1], "data": [23,24] },{ "send": [0], "recv": [1], "data": [24] }] +[{ "send": [0,1], "recv": [1,0], "data": [23,24] },{ "send": [1], "recv": [0], "data": [24] }] +[{ "send": [0,1], "recv": [1,0], "data": [23,24] },{ "send": [1,1], "recv": [0,0], "data": [24,23] }] +[{ "send": [0,1], "recv": [1,0], "data": [23,24] },{ "send": [1,1,0], "recv": [0,0,1], "data": [24,23,23] }] +[{ "send": [0,1], "recv": [1,0], "data": [23,24] },{ "send": [1,1,0], "recv": [0,0,1], "data": [24,23,24] }] diff --git a/testdata/corset/valid/if_01.expanded.bls12_377.rejects b/testdata/corset/valid/if_01.expanded.bls12_377.rejects new file mode 100644 index 000000000..c100aadb2 --- /dev/null +++ b/testdata/corset/valid/if_01.expanded.bls12_377.rejects @@ -0,0 +1,3 @@ +{ "A": [1], "B": [0], "(inv A)": [4222230874714185212124412469390773265687949667577031913967616727958704619521] } +{ "A": [1], "B": [0], "(inv A)": [5629641166285580282832549959187697687583932890102709218623488970611606159361] } +{ "A": [1], "B": [0], "(inv A)": [6333346312071277818186618704086159898531924501365547870951425091938056929281] } diff --git a/testdata/corset/valid/if_01.expanded.rejects b/testdata/corset/valid/if_01.expanded.rejects deleted file mode 100644 index 4371068a0..000000000 --- a/testdata/corset/valid/if_01.expanded.rejects +++ /dev/null @@ -1,59 +0,0 @@ -{ "A": [1], "B": [0], "(inv A)": [0] } -{ "A": [1], "B": [0], "(inv A)": [2] } -{ "A": [1], "B": [0], "(inv A)": [3] } -{ "A": [1], "B": [0], "(inv A)": [4] } -{ "A": [1], "B": [0], "(inv A)": [5] } -{ "A": [1], "B": [0], "(inv A)": [18] } -{ "A": [1], "B": [0], "(inv A)": [121] } -{ "A": [1], "B": [0], "(inv A)": [252] } -{ "A": [1], "B": [0], "(inv A)": [234] } -{ "A": [1], "B": [0], "(inv A)": [23487] } -{ "A": [1], "B": [0], "(inv A)": [1234897] } -{ "A": [1], "B": [0], "(inv A)": [4222230874714185212124412469390773265687949667577031913967616727958704619521] } -{ "A": [1], "B": [0], "(inv A)": [5629641166285580282832549959187697687583932890102709218623488970611606159361] } -{ "A": [1], "B": [0], "(inv A)": [6333346312071277818186618704086159898531924501365547870951425091938056929281] } -;; -{ "A": [2], "B": [0], "(inv A)": [0] } -{ "A": [2], "B": [0], "(inv A)": [1] } -{ "A": [2], "B": [0], "(inv A)": [2] } -{ "A": [2], "B": [0], "(inv A)": [3] } -{ "A": [2], "B": [0], "(inv A)": [4] } -{ "A": [2], "B": [0], "(inv A)": [5] } -{ "A": [2], "B": [0], "(inv A)": [18] } -{ "A": [2], "B": [0], "(inv A)": [121] } -{ "A": [2], "B": [0], "(inv A)": [252] } -{ "A": [2], "B": [0], "(inv A)": [234] } -{ "A": [2], "B": [0], "(inv A)": [23487] } -{ "A": [2], "B": [0], "(inv A)": [1234897] } -{ "A": [2], "B": [0], "(inv A)": [5629641166285580282832549959187697687583932890102709218623488970611606159361] } -{ "A": [2], "B": [0], "(inv A)": [6333346312071277818186618704086159898531924501365547870951425091938056929281] } -;; -{ "A": [3], "B": [0], "(inv A)": [0] } -{ "A": [3], "B": [0], "(inv A)": [1] } -{ "A": [3], "B": [0], "(inv A)": [2] } -{ "A": [3], "B": [0], "(inv A)": [3] } -{ "A": [3], "B": [0], "(inv A)": [4] } -{ "A": [3], "B": [0], "(inv A)": [5] } -{ "A": [3], "B": [0], "(inv A)": [18] } -{ "A": [3], "B": [0], "(inv A)": [121] } -{ "A": [3], "B": [0], "(inv A)": [252] } -{ "A": [3], "B": [0], "(inv A)": [234] } -{ "A": [3], "B": [0], "(inv A)": [23487] } -{ "A": [3], "B": [0], "(inv A)": [1234897] } -{ "A": [3], "B": [0], "(inv A)": [4222230874714185212124412469390773265687949667577031913967616727958704619521] } -{ "A": [3], "B": [0], "(inv A)": [6333346312071277818186618704086159898531924501365547870951425091938056929281] } -;; -{ "A": [4], "B": [0], "(inv A)": [0] } -{ "A": [4], "B": [0], "(inv A)": [1] } -{ "A": [4], "B": [0], "(inv A)": [2] } -{ "A": [4], "B": [0], "(inv A)": [3] } -{ "A": [4], "B": [0], "(inv A)": [4] } -{ "A": [4], "B": [0], "(inv A)": [5] } -{ "A": [4], "B": [0], "(inv A)": [18] } -{ "A": [4], "B": [0], "(inv A)": [121] } -{ "A": [4], "B": [0], "(inv A)": [252] } -{ "A": [4], "B": [0], "(inv A)": [234] } -{ "A": [4], "B": [0], "(inv A)": [23487] } -{ "A": [4], "B": [0], "(inv A)": [1234897] } -{ "A": [4], "B": [0], "(inv A)": [4222230874714185212124412469390773265687949667577031913967616727958704619521] } -{ "A": [4], "B": [0], "(inv A)": [5629641166285580282832549959187697687583932890102709218623488970611606159361] } diff --git a/testdata/corset/valid/if_10.expanded.O1.accepts b/testdata/corset/valid/if_10.expanded.accepts similarity index 100% rename from testdata/corset/valid/if_10.expanded.O1.accepts rename to testdata/corset/valid/if_10.expanded.accepts diff --git a/testdata/corset/valid/if_12.expanded.O1.accepts b/testdata/corset/valid/if_12.expanded.accepts similarity index 100% rename from testdata/corset/valid/if_12.expanded.O1.accepts rename to testdata/corset/valid/if_12.expanded.accepts diff --git a/testdata/corset/valid/if_15.expanded.O1.accepts b/testdata/corset/valid/if_15.expanded.accepts similarity index 100% rename from testdata/corset/valid/if_15.expanded.O1.accepts rename to testdata/corset/valid/if_15.expanded.accepts diff --git a/testdata/corset/valid/if_18.expanded.O1.accepts b/testdata/corset/valid/if_18.expanded.bls12_377.accepts similarity index 99% rename from testdata/corset/valid/if_18.expanded.O1.accepts rename to testdata/corset/valid/if_18.expanded.bls12_377.accepts index 162b839e0..2cf6c46b3 100644 --- a/testdata/corset/valid/if_18.expanded.O1.accepts +++ b/testdata/corset/valid/if_18.expanded.bls12_377.accepts @@ -1,23 +1,24 @@ {"X": [0], "Y": [0], "(inv (+ X (shift X -1)))": [0]} {"X": [0, 0], "Y": [0, 0], "(inv (+ X (shift X -1)))": [0, 0]} {"X": [0, 1], "Y": [0, 1], "(inv (+ X (shift X -1)))": [0, 1]} -{"X": [0, 2], "Y": [0, 1], "(inv (+ X (shift X -1)))": [0, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} {"X": [0, 1], "Y": [0, 2], "(inv (+ X (shift X -1)))": [0, 1]} -{"X": [0, 2], "Y": [0, 2], "(inv (+ X (shift X -1)))": [0, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} {"X": [0, 0, 0, 0], "Y": [0, 0, 0, 0], "(inv (+ X (shift X -1)))": [0, 0, 0, 0]} {"X": [0, 0, 1, 0], "Y": [0, 0, 1, 0], "(inv (+ X (shift X -1)))": [0, 0, 1, 1]} {"X": [0, 0, 1, 0], "Y": [0, 0, 0, 1], "(inv (+ X (shift X -1)))": [0, 0, 1, 1]} {"X": [0, 0, 1, 0], "Y": [0, 0, 1, 1], "(inv (+ X (shift X -1)))": [0, 0, 1, 1]} -{"X": [0, 0, 2, 0], "Y": [0, 0, 1, 0], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} -{"X": [0, 0, 2, 0], "Y": [0, 0, 0, 1], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} -{"X": [0, 0, 2, 0], "Y": [0, 0, 1, 1], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} {"X": [0, 0, 1, 0], "Y": [0, 0, 2, 0], "(inv (+ X (shift X -1)))": [0, 0, 1, 1]} {"X": [0, 0, 1, 0], "Y": [0, 0, 0, 2], "(inv (+ X (shift X -1)))": [0, 0, 1, 1]} {"X": [0, 0, 1, 0], "Y": [0, 0, 2, 2], "(inv (+ X (shift X -1)))": [0, 0, 1, 1]} -{"X": [0, 0, 2, 0], "Y": [0, 0, 2, 0], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} -{"X": [0, 0, 2, 0], "Y": [0, 0, 0, 2], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} -{"X": [0, 0, 2, 0], "Y": [0, 0, 2, 2], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} {"X": [0, 0, 0, 0], "Y": [0, 0, 0, 0], "(inv (+ X (shift X -1)))": [0, 0, 0, 0]} {"X": [0, 1, 0, 0], "Y": [0, 1, 0, 0], "(inv (+ X (shift X -1)))": [0, 1, 1, 0]} {"X": [0, 1, 0, 0], "Y": [0, 0, 1, 0], "(inv (+ X (shift X -1)))": [0, 1, 1, 0]} {"X": [0, 1, 0, 0], "Y": [0, 1, 1, 0], "(inv (+ X (shift X -1)))": [0, 1, 1, 0]} +;; +{"X": [0, 2], "Y": [0, 1], "(inv (+ X (shift X -1)))": [0, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} +{"X": [0, 2], "Y": [0, 2], "(inv (+ X (shift X -1)))": [0, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} +{"X": [0, 0, 2, 0], "Y": [0, 0, 1, 0], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} +{"X": [0, 0, 2, 0], "Y": [0, 0, 0, 1], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} +{"X": [0, 0, 2, 0], "Y": [0, 0, 1, 1], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} +{"X": [0, 0, 2, 0], "Y": [0, 0, 2, 0], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} +{"X": [0, 0, 2, 0], "Y": [0, 0, 0, 2], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} +{"X": [0, 0, 2, 0], "Y": [0, 0, 2, 2], "(inv (+ X (shift X -1)))": [0, 0, 4222230874714185212124412469390773265687949667577031913967616727958704619521, 4222230874714185212124412469390773265687949667577031913967616727958704619521]} diff --git a/testdata/corset/valid/lookup_03.expanded.bls12_377.rejects b/testdata/corset/valid/lookup_03.expanded.bls12_377.rejects new file mode 100644 index 000000000..b9748015e --- /dev/null +++ b/testdata/corset/valid/lookup_03.expanded.bls12_377.rejects @@ -0,0 +1,4 @@ +;; BLS12_377 modulus=8444461749428370424248824938781546531375899335154063827935233455917409239041 +{"X": [0], "Y": [0], "X2": [8444461749428370424248824938781546531375899335154063827935233455917409239040]} +{"X": [0, 0], "Y": [0, 0], "X2": [8444461749428370424248824938781546531375899335154063827935233455917409239040, 0]} +{"X": [0, 0], "Y": [0, 0], "X2": [0, 8444461749428370424248824938781546531375899335154063827935233455917409239040]} diff --git a/testdata/corset/valid/lookup_03.expanded.rejects b/testdata/corset/valid/lookup_03.expanded.rejects index 66f353b3e..9cf55b7f0 100644 --- a/testdata/corset/valid/lookup_03.expanded.rejects +++ b/testdata/corset/valid/lookup_03.expanded.rejects @@ -1,11 +1,8 @@ -;; BLS12_377 modulus=8444461749428370424248824938781546531375899335154063827935233455917409239041 -{"X": [0], "Y": [0], "X2": [8444461749428370424248824938781546531375899335154063827935233455917409239040]} + {"X": [0], "Y": [0], "X2": [1]} {"X": [0], "Y": [0], "X2": [2]} {"X": [0], "Y": [0], "X2": [3]} ;; -{"X": [0, 0], "Y": [0, 0], "X2": [8444461749428370424248824938781546531375899335154063827935233455917409239040, 0]} -{"X": [0, 0], "Y": [0, 0], "X2": [0, 8444461749428370424248824938781546531375899335154063827935233455917409239040]} {"X": [0, 0], "Y": [0, 0], "X2": [1, 0]} {"X": [0, 0], "Y": [0, 0], "X2": [0, 1]} ;; diff --git a/testdata/zkc/bench/rec_pow.zkc b/testdata/zkc/bench/rec_pow.zkc index 076532991..616aed5f4 100644 --- a/testdata/zkc/bench/rec_pow.zkc +++ b/testdata/zkc/bench/rec_pow.zkc @@ -9,6 +9,7 @@ fn main() { pow!(k, n as u32, 1, res) } +#[global] fn pow(i:u16, acc:u32, actual:u32, expected:u32) -> ! { var b:u1 var res:u32 diff --git a/testdata/zkc/invalid/global_01.zkc b/testdata/zkc/invalid/global_01.zkc new file mode 100644 index 000000000..2e2807ae3 --- /dev/null +++ b/testdata/zkc/invalid/global_01.zkc @@ -0,0 +1,10 @@ +//error:4:1-23:global function must not return +// global functions must not return. +#[global] +fn f(x:u16) -> (y:u16) { + y = x +} + +fn main() { + var x:u16 = f(0) +} diff --git a/testdata/zkc/invalid/inline_07.zkc b/testdata/zkc/invalid/inline_07.zkc new file mode 100644 index 000000000..b78b00825 --- /dev/null +++ b/testdata/zkc/invalid/inline_07.zkc @@ -0,0 +1,9 @@ +//error:3:1-16:cannot inline non-returning function +#[inline] +fn f(x:u8) -> ! { + fail +} + +fn main() { + f!(0) +} diff --git a/testdata/zkc/unit/basic_86.zkc b/testdata/zkc/unit/basic_86.zkc index efe048965..6675ad016 100644 --- a/testdata/zkc/unit/basic_86.zkc +++ b/testdata/zkc/unit/basic_86.zkc @@ -4,11 +4,26 @@ memory ram[u32](addr:u16) -> (b:u8) fn main() { var n:u16 = data[0] as u16 // - for i:u16 = 0; i(i:u16) { +#[global] +fn copy(i:u16, n:u16) -> ! { + if i == n { + finalise!(n) + } + // recursive case ram[i] = data[i + 1] + // + copy!(i + 1, n) +} + +fn finalise(n:u16) -> ! { + for i:u16 = 0; i ! { if n == 0 { done diff --git a/testdata/zkc/unit/basic_90.zkc b/testdata/zkc/unit/basic_90.zkc index 716787736..88eaf8aec 100644 --- a/testdata/zkc/unit/basic_90.zkc +++ b/testdata/zkc/unit/basic_90.zkc @@ -11,6 +11,7 @@ fn main() { checkNonZero!(n) } +#[global] fn checkNonZero(n:u16) -> ! { if n == 0 { done diff --git a/testdata/zkc/unit/basic_91.zkc b/testdata/zkc/unit/basic_91.zkc index b3dbe0d71..c4babfa93 100644 --- a/testdata/zkc/unit/basic_91.zkc +++ b/testdata/zkc/unit/basic_91.zkc @@ -5,6 +5,7 @@ fn main() { checkNonZero!(n) } +#[global] fn checkNonZero(n:u16) -> ! { var tmp:u16 = n // From fa8be6e917c5ec813f1b86af1c6ed5b5763dc80d Mon Sep 17 00:00:00 2001 From: DavePearce Date: Fri, 28 Aug 2026 13:56:35 +1200 Subject: [PATCH 2/2] feat: wire in bus for global functions This wires in the bus primitives for global functions, and updates the reachablity check accordingly. Tests for sharding are now operational. Signed-off-by: DavePearce --- pkg/cmd/corset/check.go | 17 +- pkg/cmd/corset/inspect.go | 6 +- pkg/cmd/corset/trace.go | 47 +-- pkg/cmd/corset/util/schema_stacker.go | 2 - pkg/ir/builder/alignment.go | 3 - pkg/ir/builder/expansion.go | 4 - pkg/ir/builder/validation.go | 5 - pkg/ir/trace_builder.go | 29 +- pkg/test/util/check_legacy.go | 16 +- pkg/test/zkc_invalid_test.go | 5 + pkg/test/zkc_unit_test.go | 6 +- pkg/util/perfstats.go | 9 +- pkg/zkc/compiler/validate/global.go | 19 +- pkg/zkc/constraints/binary_file.go | 46 +-- pkg/zkc/constraints/call_and_memory_lookup.go | 108 +++++-- pkg/zkc/constraints/range_lookup.go | 17 +- pkg/zkc/constraints/translate_fn.go | 191 ++++++++++++ .../constraints/{ram.go => translate_ram.go} | 8 +- pkg/zkc/constraints/translator.go | 273 +++++------------- pkg/zkc/constraints/validate.go | 32 +- pkg/zkc/vm/internal/checkpoint/checkpoint.go | 16 +- pkg/zkc/vm/internal/checkpoint/memory.go | 12 + pkg/zkc/vm/internal/checkpoint/page.go | 12 + .../vm/internal/descriptor/function_kind.go | 8 + .../vm/internal/interpreter/interpreter.go | 4 +- pkg/zkc/vm/machine.go | 37 +-- pkg/zkc/vm/trace_builder.go | 22 +- testdata/zkc/invalid/global_02.zkc | 11 + 28 files changed, 578 insertions(+), 387 deletions(-) create mode 100644 pkg/zkc/constraints/translate_fn.go rename pkg/zkc/constraints/{ram.go => translate_ram.go} (98%) create mode 100644 testdata/zkc/invalid/global_02.zkc diff --git a/pkg/cmd/corset/check.go b/pkg/cmd/corset/check.go index 56c76b24a..994430b36 100644 --- a/pkg/cmd/corset/check.go +++ b/pkg/cmd/corset/check.go @@ -18,6 +18,7 @@ import ( "os" "runtime" "runtime/pprof" + "slices" cmd_util "github.com/LFDT-Lineth/zkc/pkg/cmd/corset/util" "github.com/LFDT-Lineth/zkc/pkg/cmd/corset/view" @@ -220,19 +221,15 @@ func CheckTrace[F field.Element[F]](ir string, schema sc.AnySchema[F], builder i cfg CheckConfig, trace tr.Trace[F]) bool { // begin performance measurement var ( - mapping = module.IdentityMap[F](schema.Modules().Collect()...) - stats = util.NewPerfStats() - recoverable bool = true + mapping = module.IdentityMap[F](schema.Modules().Collect()...) + stats = util.NewPerfStats() + recoverable bool errs []error ) // - for i, shard := range trace { - var es []error - - trace[i], es = builder.Build(schema, shard) - errs = append(errs, es...) - recoverable = recoverable && (trace[i] != nil) - } + trace, errs = builder.Build(schema, trace) + // Check whether any invalid traces + recoverable = !slices.Contains(trace, nil) // Log cost of expansion stats.Log("Expanding trace columns") // Report any errors diff --git a/pkg/cmd/corset/inspect.go b/pkg/cmd/corset/inspect.go index 58ef4ac3a..51f23929e 100644 --- a/pkg/cmd/corset/inspect.go +++ b/pkg/cmd/corset/inspect.go @@ -21,6 +21,7 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/corset" "github.com/LFDT-Lineth/zkc/pkg/schema/module" "github.com/LFDT-Lineth/zkc/pkg/trace" + tr "github.com/LFDT-Lineth/zkc/pkg/trace" "github.com/LFDT-Lineth/zkc/pkg/util" "github.com/LFDT-Lineth/zkc/pkg/util/field" "github.com/LFDT-Lineth/zkc/pkg/util/field/bls12_377" @@ -94,7 +95,10 @@ func runInspectCmd[F field.Element[F]](cmd *cobra.Command, args []string) { } else if len(tracefile) != 1 { errors = append(errors, fmt.Errorf("cannot inspect multiple shards")) } else { - trace, errors = stack.TraceBuilder().Build(schema, tracefile[0]) + var shards []tr.Shard[F] + + shards, errors = stack.TraceBuilder().Build(schema, []tr.Shard[F]{tracefile[0]}) + trace = shards[0] } // if len(errors) == 0 { diff --git a/pkg/cmd/corset/trace.go b/pkg/cmd/corset/trace.go index 797e790ce..be6443c26 100644 --- a/pkg/cmd/corset/trace.go +++ b/pkg/cmd/corset/trace.go @@ -224,7 +224,7 @@ func expandTraces[F field.Element[F]](traceFiles []tr.Trace[F], stack cmd_util.S for i := range traceFiles { var errs []error // - traces[i], errs = expandTrace(traceFiles[i], stack, bldr) + traces[i], errs = bldr.Build(stack.ConcreteSchema(), traceFiles[i]) // errors = append(errors, errs...) } @@ -232,31 +232,6 @@ func expandTraces[F field.Element[F]](traceFiles []tr.Trace[F], stack cmd_util.S return traces, errors } -func expandTrace[F field.Element[F]](tf tr.Trace[F], stack cmd_util.SchemaStack[F], bldr ir.TraceBuilder[F], -) (tr.Trace[F], []error) { - // - var ( - tb_errors []error - tp_errors []error - tr = make(tr.Trace[F], len(tf)) - ) - // - for i, shard := range tf { - // Construct expanded trace - tr[i], tb_errors = bldr.Build(stack.ConcreteSchema(), shard) - // Handle errors - if len(tb_errors) > 0 { - for _, err := range tb_errors { - log.Errorln(err) - } - // - os.Exit(1) - } - } - // Now, reconstruct it! - return tr, tp_errors -} - func printTraceInfo[F field.Element[F]](cfg TraceConfig, trace tr.Trace[F]) { for i, shard := range trace { // @@ -293,7 +268,7 @@ func printTraceInfo[F field.Element[F]](cfg TraceConfig, trace tr.Trace[F]) { } // Print full trace (if requested) if cfg.trace { - printTrace(cfg, window) + printTrace(window) } } } @@ -305,14 +280,16 @@ func printTraceInfo[F field.Element[F]](cfg TraceConfig, trace tr.Trace[F]) { // which was hidden. func PrintTrace[F field.Element[F]](mapping module.LimbsMap, trace tr.Trace[F], limbs bool, cellWidth, titleWidth uint) { - // Build the viewing window (no source map, so show computed registers). - builder := view.NewBuilder[F](mapping). - WithCellWidth(cellWidth). - WithTitleWidth(titleWidth). - WithLimbs(limbs). - WithComputed(true) - // - printTrace(builder.Build(trace)) + for _, shard := range trace { + // Build the viewing window (no source map, so show computed registers). + builder := view.NewBuilder[F](mapping). + WithCellWidth(cellWidth). + WithTitleWidth(titleWidth). + WithLimbs(limbs). + WithComputed(true) + // + printTrace(builder.Build(shard)) + } } func printTrace(window view.TraceView) { diff --git a/pkg/cmd/corset/util/schema_stacker.go b/pkg/cmd/corset/util/schema_stacker.go index 502565124..adb182d80 100644 --- a/pkg/cmd/corset/util/schema_stacker.go +++ b/pkg/cmd/corset/util/schema_stacker.go @@ -178,8 +178,6 @@ func (p SchemaStacker[F]) Build() SchemaStack[F] { stack.concreteSchemas = append(stack.concreteSchemas, schema.Any(airSchema)) stack.names = append(stack.names, "AIR") } - // Assign trace builder with limb map - stack.traceBuilder = p.traceBuilder.WithRegisterMapping(mapping) // Assign source map used to build the stack stack.sourceMap = p.sourceMap } diff --git a/pkg/ir/builder/alignment.go b/pkg/ir/builder/alignment.go index 57b838a1d..cf6d3d59b 100644 --- a/pkg/ir/builder/alignment.go +++ b/pkg/ir/builder/alignment.go @@ -61,7 +61,6 @@ func AlignAndPad[F field.Element[F]](config Config, schema sc.AnySchema[F], tr t ) (ArrayTrace[F], []error) { // var ( - stats = util.NewPerfStats() errors []error modules = make([]ArrayModule[F], schema.Width()) modmap = make(map[string]uint) @@ -109,8 +108,6 @@ func AlignAndPad[F field.Element[F]](config Config, schema sc.AnySchema[F], tr t modules = padded // errors = append(errors, errs...) - // - stats.Log("Trace alignment and padding") // Done return trace.NewArray(modules), errors } diff --git a/pkg/ir/builder/expansion.go b/pkg/ir/builder/expansion.go index 8ba83dda8..b9d4a3b10 100644 --- a/pkg/ir/builder/expansion.go +++ b/pkg/ir/builder/expansion.go @@ -29,8 +29,6 @@ func TraceExpansion[F field.Element[F]](config Config, schema sc.AnySchema[F], t // var ( err error - // Start timer - stats = util.NewPerfStats() ) // if config.Parallel { @@ -39,8 +37,6 @@ func TraceExpansion[F field.Element[F]](config Config, schema sc.AnySchema[F], t } else { err = SequentialTraceExpansion(schema, trace) } - // Log stats - stats.Log("Trace expansion") // return err } diff --git a/pkg/ir/builder/validation.go b/pkg/ir/builder/validation.go index 4211c8ff2..8afc22ced 100644 --- a/pkg/ir/builder/validation.go +++ b/pkg/ir/builder/validation.go @@ -18,7 +18,6 @@ import ( sc "github.com/LFDT-Lineth/zkc/pkg/schema" "github.com/LFDT-Lineth/zkc/pkg/schema/register" "github.com/LFDT-Lineth/zkc/pkg/trace" - "github.com/LFDT-Lineth/zkc/pkg/util" "github.com/LFDT-Lineth/zkc/pkg/util/collection/array" "github.com/LFDT-Lineth/zkc/pkg/util/field" ) @@ -29,8 +28,6 @@ import ( func TraceValidation[F field.Element[F]](config Config, schema sc.AnySchema[F], tr trace.Shard[F]) []error { var ( errors []error - // Start timer - stats = util.NewPerfStats() // Flatten all columns columns, errs = flattenTrace(schema, tr) // Mapping function @@ -54,8 +51,6 @@ func TraceValidation[F field.Element[F]](config Config, schema sc.AnySchema[F], } // Filter our any nil errors errors = array.Filter(errors, func(e error) bool { return e != nil }) - // Log stats - stats.Log("Trace validation") // Done return append(errs, errors...) } diff --git a/pkg/ir/trace_builder.go b/pkg/ir/trace_builder.go index f45284d79..8a693c659 100644 --- a/pkg/ir/trace_builder.go +++ b/pkg/ir/trace_builder.go @@ -18,6 +18,7 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/ir/builder" sc "github.com/LFDT-Lineth/zkc/pkg/schema" "github.com/LFDT-Lineth/zkc/pkg/trace" + "github.com/LFDT-Lineth/zkc/pkg/util/collection/array" "github.com/LFDT-Lineth/zkc/pkg/util/field" ) @@ -112,11 +113,33 @@ func (tb TraceBuilder[F]) BatchSize() uint { // Build attempts to construct a trace for a given schema, producing errors if // there are inconsistencies (e.g. missing columns, duplicate columns, etc). -func (tb TraceBuilder[F]) Build(schema sc.AnySchema[F], tf trace.Shard[F]) (tr trace.Shard[F], errs []error) { +func (tb TraceBuilder[F]) Build(schema sc.AnySchema[F], tf trace.Trace[F]) (tr trace.Trace[F], errs []error) { var ( - atr builder.ArrayTrace[F] + shards = make([]trace.Shard[F], len(tf)) + errors = make([][]error, len(tf)) + // Trace Expander function + expandFn = func(i uint, shard trace.Shard[F]) { + shards[i], errors[i] = tb.buildShard(schema, i, shard) + } + ) + // Build the trace (using parallelism if requested). + if tb.parallel { + array.ParallelApply(tf, expandFn) + } else { + array.Apply(tf, expandFn) + } + // Flattern errors + return shards, array.FlatMap(errors, func(es []error) []error { return es }) +} + +func (tb TraceBuilder[F]) buildShard(schema sc.AnySchema[F], shard uint, tf trace.Shard[F], +) (tr trace.Shard[F], errs []error) { + // + var ( + atr builder.ArrayTrace[F] + // config = builder.Config{ - Parallel: tb.parallel, + Parallel: false, BatchSize: tb.batchSize, Expanding: tb.expand, Padding: tb.paddingStrategy, diff --git a/pkg/test/util/check_legacy.go b/pkg/test/util/check_legacy.go index 1e3920537..493f2ae49 100644 --- a/pkg/test/util/check_legacy.go +++ b/pkg/test/util/check_legacy.go @@ -218,12 +218,10 @@ func checkTraces[F field.Element[F]](t *testing.T, test string, padding bool, op func checkTrace[F field.Element[F], C sc.Constraint[F]](t *testing.T, tf trace.Trace[F], id traceId, schema sc.Schema[F, C]) { var ( - errors []error // Map the legacy padding toggle onto a padding strategy. paddingStrategy = ir.NaryRowPadding(0) - // - shards = make(trace.Trace[F], len(tf)) ) + // if id.padding { paddingStrategy = ir.NextPowerOfTwoPadding } @@ -235,13 +233,11 @@ func checkTrace[F field.Element[F], C sc.Constraint[F]](t *testing.T, tf trace.T WithParallelism(id.parallel). WithBatchSize(128) // Construct the trace - for i, shard := range tf { - shards[i], errors = builder.Build(sc.Any(schema), shard) - // - if len(errors) > 0 { - t.Errorf("Trace expansion failed (%s): %s", id.String(), errors) - return - } + shards, errors := builder.Build(sc.Any(schema), tf) + // Check for errors + if len(errors) > 0 { + t.Errorf("Trace expansion failed (%s): %s", id.String(), errors) + return } // Check Constraints errs := sc.Accepts(id.parallel, schema, shards) diff --git a/pkg/test/zkc_invalid_test.go b/pkg/test/zkc_invalid_test.go index 85396d176..3b41b5d9d 100644 --- a/pkg/test/zkc_invalid_test.go +++ b/pkg/test/zkc_invalid_test.go @@ -1153,6 +1153,11 @@ func Test_ZkcInvalid_Global_01(t *testing.T) { checkZkcInvalid(t, "zkc/invalid/global_01") } +func Test_ZkcInvalid_Global_02(t *testing.T) { + // native global function + checkZkcInvalid(t, "zkc/invalid/global_02") +} + // =================================================================== // Test Helpers // =================================================================== diff --git a/pkg/test/zkc_unit_test.go b/pkg/test/zkc_unit_test.go index af426ca46..391e63552 100644 --- a/pkg/test/zkc_unit_test.go +++ b/pkg/test/zkc_unit_test.go @@ -379,15 +379,15 @@ func Test_ZkcUnit_Basic_88(t *testing.T) { } func Test_ZkcUnit_Basic_89(t *testing.T) { - checkZkcUnit(t, "zkc/unit/basic_89", DEFAULT_UNIT_CONFIG.Sharding("checkNonZero", 1)) + checkZkcUnit(t, "zkc/unit/basic_89", DEFAULT_UNIT_CONFIG.Sharding("checkNonZero", 256)) } func Test_ZkcUnit_Basic_90(t *testing.T) { - checkZkcUnit(t, "zkc/unit/basic_90", DEFAULT_UNIT_CONFIG.Sharding("checkNonZero", 1)) + checkZkcUnit(t, "zkc/unit/basic_90", DEFAULT_UNIT_CONFIG.Sharding("checkNonZero", 256)) } func Test_ZkcUnit_Basic_91(t *testing.T) { - checkZkcUnit(t, "zkc/unit/basic_91", DEFAULT_UNIT_CONFIG.Sharding("checkNonZero", 1)) + checkZkcUnit(t, "zkc/unit/basic_91", DEFAULT_UNIT_CONFIG.Sharding("checkNonZero", 256)) } func Test_ZkcUnit_AccessOnceMemory_01(t *testing.T) { diff --git a/pkg/util/perfstats.go b/pkg/util/perfstats.go index 8b9df5468..e58eca241 100644 --- a/pkg/util/perfstats.go +++ b/pkg/util/perfstats.go @@ -42,8 +42,11 @@ func NewPerfStats() *PerfStats { } // Reset the performance counter -func (p *PerfStats) Reset() { - var m runtime.MemStats +func (p *PerfStats) Reset() uint { + var ( + m runtime.MemStats + exectime = time.Since(p.startTime).Seconds() + ) // p.startTime = time.Now() // @@ -51,6 +54,8 @@ func (p *PerfStats) Reset() { // p.startMem = m.TotalAlloc p.startGc = m.NumGC + // + return uint(exectime) } // Log logs the difference between the state now and as it was when the PerfStats object was created. diff --git a/pkg/zkc/compiler/validate/global.go b/pkg/zkc/compiler/validate/global.go index 6a72f9ab0..234aa6b23 100644 --- a/pkg/zkc/compiler/validate/global.go +++ b/pkg/zkc/compiler/validate/global.go @@ -19,11 +19,16 @@ import ( ) // GlobalFunctions checks that every function marked with the #[global] -// annotation is declared as non-returning (i.e. "-> !"). A global function is -// placed "on the bus" so that it can be called from another shard. Since -// caller and callee may then reside in different shards, there is no way to -// thread the callee's results back to the caller. Hence, a global function -// which returns is rejected here. +// annotation can actually be placed "on the bus" so that it can be called from +// another shard. Specifically, a global function must not be: +// +// (1) returning (i.e. anything other than "-> !"), since caller and callee may +// then reside in different shards and there is no way to thread the callee's +// results back to the caller; +// +// (2) marked #[native], since a native function is backed by an external +// circuit and, hence, has no activity ($ret) line to serve as the selector of +// the bus's receive port. func GlobalFunctions(program ast.Program, srcmaps source.Maps[any]) []source.SyntaxError { var errors []source.SyntaxError // @@ -37,6 +42,10 @@ func GlobalFunctions(program ast.Program, srcmaps source.Maps[any]) []source.Syn if !fn.NoReturn { errors = append(errors, srcmaps.SyntaxErrors(fn, "global function must not return")...) } + // + if slices.Contains(fn.Annotations(), "native") { + errors = append(errors, srcmaps.SyntaxErrors(fn, "global function must not be native")...) + } } // return errors diff --git a/pkg/zkc/constraints/binary_file.go b/pkg/zkc/constraints/binary_file.go index f6ab6468a..d4cc2aa8b 100644 --- a/pkg/zkc/constraints/binary_file.go +++ b/pkg/zkc/constraints/binary_file.go @@ -309,40 +309,48 @@ func (p *BinaryFile[F]) Execute(input map[string][]byte) (output map[string][]by // carries the original register / limb structure before AIR expansion (e.g. for // reporting statistics). It is nil when execution fails. func (p *BinaryFile[F]) Trace(input map[string][]byte, cfg vm.TraceConfig, -) (output map[string][]byte, trace trace.Trace[F], errs []error) { +) (output map[string][]byte, trace trace.Trace[F], errors []error) { // var ( stats = util.NewPerfStats() // Initialise trace builder from configuration - builder = vm.NewTraceBuilder[vm.Uint32, F, Tracer[F]](cfg, p.TracingProgram()) + builder = vm.NewTraceBuilder[vm.Uint32, F, Tracer[F]](cfg, p.TracingProgram(), p.TracingProgram()) ) // Execute machine in chunks of 1K steps - trace, output, errs = builder.BootAndTrace(input) + trace, output, errors = builder.BootAndTrace(input) + // + stats.Log(fmt.Sprintf("Trace generation (%d shards)", len(trace))) // if len(trace) > 0 { - var berrs []error - // Extract AIR constraints - constraints := p.AirConstraints() + var errs []error // Construct trace builder - builder := ir.NewTraceBuilder[F](). + trace, errs = p.expandTrace(cfg, trace) + // Include any expansion errors + errors = append(errors, errs...) + } + // + return output, trace, errors +} + +func (p *BinaryFile[F]) expandTrace(cfg vm.TraceConfig, tr trace.Trace[F]) (trace.Trace[F], []error) { + // + var ( + stats = util.NewPerfStats() + constraints = p.AirConstraints() + // Construct trace builder + builder = ir.NewTraceBuilder[F](). // NOTE: never use validation, as it hides constraint failures. WithValidation(false). - WithExpansion(true). WithParallelism(cfg.Parallelism()). - WithBatchSize(cfg.BatchSize()). + WithExpansion(true). WithPadding(cfg.PaddingStrategy()) - // Expand shards one-by-one - for i, shard := range trace { - // Build the trace (finally) - trace[i], berrs = builder.Build(constraints, shard) - // Include any builder errors - errs = append(errs, berrs...) - } - } + ) + // Apply trace expansion + etr, errors := builder.Build(constraints, tr) // - stats.Log(fmt.Sprintf("Trace generation (%d shards)", len(trace))) + stats.Log(fmt.Sprintf("Trace expansion (%d shards)", len(etr))) // - return output, trace, errs + return etr, errors } // ============================================================================ diff --git a/pkg/zkc/constraints/call_and_memory_lookup.go b/pkg/zkc/constraints/call_and_memory_lookup.go index 0efeb29f3..24fa78d31 100644 --- a/pkg/zkc/constraints/call_and_memory_lookup.go +++ b/pkg/zkc/constraints/call_and_memory_lookup.go @@ -20,6 +20,7 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/ir/mir" "github.com/LFDT-Lineth/zkc/pkg/ir/term" "github.com/LFDT-Lineth/zkc/pkg/schema" + "github.com/LFDT-Lineth/zkc/pkg/schema/constraint/bus" "github.com/LFDT-Lineth/zkc/pkg/schema/constraint/lookup" "github.com/LFDT-Lineth/zkc/pkg/schema/register" "github.com/LFDT-Lineth/zkc/pkg/util" @@ -38,6 +39,11 @@ import ( // - a memory access's lookup maps the accessor's address/data registers // onto the memory table's address/data columns. // +// Calls into a global function are the exception: they are placed "on the bus" +// instead, since caller and callee may reside in different shards (see +// emitCallBus). Their send ports are accumulated in buses, rather than being +// emitted here. +// // The accessing (source) side is gated on two (potentially combined) conditions: // // - Position: in a multi-line function the access at code line k fires only on @@ -49,13 +55,16 @@ import ( // // Lookups require a register (and not an expression) as the source selector, // so the path selector is materialised as a fresh 1-bit register (if it is not already). -func addLookups[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir.Constraint[F]], +func (p *constraintTranslator[W, F]) addLookups(mod *schema.Table[F, mir.Constraint[F]], ctx schema.ModuleId, fn *vm.Function[W], pcSelectors []register.Id, - ret register.Id, - infos []vm.Module[W], - field field.Config) { + ret register.Id) { + // + var ( + field = p.program.Field() + modules = p.program.Modules() + ) // for pc, vec := range fn.Vectors() { // Branch table giving the condition under which each code in this vector @@ -80,19 +89,22 @@ func addLookups[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir.Const for _, entry := range group.entries { switch c := entry.code.(type) { case *vm.BytecodeCall[W]: - // TODO: put global functions "on the bus" - // - // var global = infos[c.Target].(*vm.Function[W]).Kind().IsGlobal() - // - emitCallLookup(mod, ctx, uint(pc), uint(c.Target), - toRegisterIds(c.Arguments), toRegisterIds(c.Returns), srcSelector, infos) - + if callee := modules[c.Target].(*vm.Function[W]); callee.Kind().IsGlobal() { + // Global function calls go "on the bus" rather than + // using shard-local lookups. + p.addSendPort(c.Target, + bus.NewPort(ctx, srcSelector, toRegisterIds(c.Arguments)...)) + } else { + // Local function calls use shard-local lookups + emitCallLookup(mod, ctx, uint(pc), c.Target, + toRegisterIds(c.Arguments), toRegisterIds(c.Returns), srcSelector, p.program) + } case *vm.BytecodeReadWrite[W]: - if infos[c.Id].(*vm.Memory[W]).IsReadWrite() { - emitRamLookup(mod, ctx, uint(pc), entry.cc, c, srcSelector, infos, field) + if modules[c.Id].(*vm.Memory[W]).IsReadWrite() { + emitRamLookup(mod, ctx, uint(pc), entry.cc, c, srcSelector, p.program) } else { - emitMemoryLookup(mod, ctx, uint(pc), entry.cc, uint(c.Id), - toRegisterIds(c.Address), toRegisterIds(c.Data), srcSelector, infos) + emitMemoryLookup(mod, ctx, uint(pc), entry.cc, c.Id, + toRegisterIds(c.Address), toRegisterIds(c.Data), srcSelector, p.program) } } } @@ -299,10 +311,9 @@ func (p callRegisterReader[F]) ReadRegister(id register.Id, _ bool) Expr[F] { // emitCallLookup constructs and adds a single lookup constraint mapping the // caller's argument/return registers onto the callee's input/output registers. func emitCallLookup[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir.Constraint[F]], ctx schema.ModuleId, - pc, calleeId uint, args, returns []register.Id, - srcSelector register.Id, infos []vm.Module[W]) { + pc uint, calleeId uint16, args, returns []register.Id, srcSelector register.Id, program vm.Program[W]) { var ( - callee = infos[calleeId].(*vm.Function[W]) + callee = program.Module(calleeId).(*vm.Function[W]) calleeRegs = toRegisters(callee.Registers()) handle = fmt.Sprintf("call_%d_%d_%d", ctx, pc, calleeId) // Source ids: the caller's argument registers followed by its return @@ -324,7 +335,7 @@ func emitCallLookup[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir.C // Native module don't have a $ret function // (do we need one ? see https://github.com/LFDT-Lineth/zkc/issues/2025) if callee.IsNative() { - target = lookup.UnfilteredVector(calleeId, tgtIds...) + target = lookup.UnfilteredVector(uint(calleeId), tgtIds...) } else { // Both multi-line and atomic (one-line) callees expose a $ret line which is 1 // on active rows; use it as the lookup selector. @@ -333,12 +344,53 @@ func emitCallLookup[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir.C // Atomic callees have $ret line as well. Only OLI that touches memmory should have one. var retId = register.NewId(uint(len(calleeRegs))) // - target = lookup.FilteredVector(calleeId, retId, tgtIds...) + target = lookup.FilteredVector(uint(calleeId), retId, tgtIds...) } // mod.AddConstraints(mir.NewLookupConstraint[F](handle, []mir.LookupVector{target}, []mir.LookupVector{source})) } +// emitCallBus constructs and adds the bus connecting every call site of a +// global callee (its send ports) to that callee's activation rows (its single +// receive port). A bus is used here, rather than a lookup, because a lookup +// holds shard-locally whereas a bus balances across every shard of a trace. +// Thus, a call made in one shard can be matched by an activation recorded in +// another. +// +// The receive port is gated on the callee's $ret line, which is 1 on exactly +// one row of each activation. Since a global function cannot return, the +// message consists of the callee's input registers alone; these are constant +// throughout a frame and, hence, still hold the arguments on the $ret row. +func (p *constraintTranslator[W, F]) emitCallBus(mod *schema.Table[F, mir.Constraint[F]], + calleeId vm.ModuleId, callee *vm.Function[W]) { + // + var ( + // Send ports of every call site, as accumulated whilst translating the + // enclosing callers. + sends = p.sendPorts[calleeId] + handle = fmt.Sprintf("bus_%s", callee.Name()) + // $ret is allocated immediately after the callee's registers (see + // translateFunction). + retId = register.NewId(uint(len(callee.Registers()))) + // Message: the callee's input registers, which occupy ids + // 0..NumInputs(). + tgtIds = make([]register.Id, callee.NumInputs()) + ) + // + for i := range tgtIds { + tgtIds[i] = register.NewId(uint(i)) + } + // Sanity check every call site agrees with the callee's arity. + for _, send := range sends { + if send.Len() != uint(len(tgtIds)) { + panic(fmt.Sprintf("incorrect number of arguments for call to \"%s\"", callee.Name())) + } + } + // + mod.AddConstraints(mir.NewBusConstraint[F](handle, sends, + []mir.BusPort{bus.NewPort(uint(calleeId), retId, tgtIds...)})) +} + // emitMemoryLookup constructs and adds a single lookup constraint mapping an // accessor's address/data registers onto the address/data columns of a memory // table (SROM, ROM or WOM). Reads and writes share the same shape: both bind @@ -355,10 +407,10 @@ func emitCallLookup[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir.C // each address exactly once (address monotony), so two writes of different // values to the same address cannot both match a row. func emitMemoryLookup[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir.Constraint[F]], - ctx schema.ModuleId, pc, cc, memId uint, - address, data []register.Id, srcSelector register.Id, infos []vm.Module[W]) { + ctx schema.ModuleId, pc, cc uint, memId uint16, + address, data []register.Id, srcSelector register.Id, program vm.Program[W]) { var ( - mem = infos[memId].(*vm.Memory[W]) + mem = program.Module(memId).(*vm.Memory[W]) memRegs = toRegisters(mem.Registers()) // The bytecode index (cc) disambiguates two accesses to the same memory // on the same code line. @@ -383,14 +435,14 @@ func emitMemoryLookup[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir if mem.IsStatic() { // Static tables enumerate their full contents, so every row is a valid // table entry and the target side is unfiltered. - target = lookup.UnfilteredVector(memId, tgtIds...) + target = lookup.UnfilteredVector(uint(memId), tgtIds...) } else { // ROM / WOM tables expose a $access_bit column which is 1 on active // rows; use it as the lookup selector. It is allocated immediately // after the address/data registers (see translateAccessOnceMemory). var accessId = register.NewId(uint(len(memRegs))) // - target = lookup.FilteredVector(memId, accessId, tgtIds...) + target = lookup.FilteredVector(uint(memId), accessId, tgtIds...) } // mod.AddConstraints(mir.NewLookupConstraint[F](handle, []mir.LookupVector{target}, []mir.LookupVector{source})) @@ -411,11 +463,11 @@ func emitMemoryLookup[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir // remains for the offline memory-checking bus (see translateReadWriteMemory). func emitRamLookup[W vm.Word[W], F field.Element[F]](mod *schema.Table[F, mir.Constraint[F]], ctx schema.ModuleId, pc, cc uint, rw *vm.BytecodeReadWrite[W], - srcSelector register.Id, infos []vm.Module[W], fieldCfg field.Config) { + srcSelector register.Id, program vm.Program[W]) { // var ( - mem = infos[rw.Id].(*vm.Memory[W]) - layout = computeRamLayout(mem, fieldCfg) + mem = program.Module(rw.Id).(*vm.Memory[W]) + layout = computeRamLayout(mem, program.Field()) // The bytecode index (cc) disambiguates two accesses to the same memory // on the same code line. handle = fmt.Sprintf("ram_%d_%d_%d_%d", ctx, pc, cc, rw.Id) diff --git a/pkg/zkc/constraints/range_lookup.go b/pkg/zkc/constraints/range_lookup.go index 171ab2534..3429ddc01 100644 --- a/pkg/zkc/constraints/range_lookup.go +++ b/pkg/zkc/constraints/range_lookup.go @@ -49,11 +49,12 @@ type rangeTable struct { // n <= maxStaticWidth; wider registers are range-checked recursively by // a call (lowered via addCallLookups), so only the static tables are collected // here. -func indexRangeTables[W vm.Word[W], F field.Element[F]](modules []vm.Module[W], - maxStaticWidth uint) map[uint]rangeTable { - tables := make(map[uint]rangeTable) +func indexRangeTables[W vm.Word[W], F field.Element[F]](program vm.Program[W], maxStaticWidth uint, +) map[uint]rangeTable { // - for id, m := range modules { + var tables = make(map[uint]rangeTable) + // + for id, m := range program.Modules() { // Only the fully-enumerated static tables serve as direct lookup targets; mem, ok := m.(*vm.Memory[W]) if !ok || !mem.IsStatic() || !strings.HasPrefix(m.Name(), rangeModulePrefix) { @@ -83,8 +84,8 @@ func indexRangeTables[W vm.Word[W], F field.Element[F]](modules []vm.Module[W], // range-checked at runtime by a recursive call which addCallLookups lowers into // a lookup. Native (field-element) and zero-width registers are not // range-checked at all. -func addRangeProofConstraints[F field.Element[F]](mod *schema.Table[F, mir.Constraint[F]], ctx schema.ModuleId, - regs []register.Register, tables map[uint]rangeTable, maxStaticWidth uint) { +func (p *constraintTranslator[W, F]) addRangeProofConstraints(mod *schema.Table[F, mir.Constraint[F]], + ctx schema.ModuleId, regs []register.Register) { // TODO: lots of perf possible here, see // https://github.com/LFDT-Lineth/zkc/issues/1907 // https://github.com/LFDT-Lineth/zkc/issues/1911 @@ -105,10 +106,10 @@ func addRangeProofConstraints[F field.Element[F]](mod *schema.Table[F, mir.Const continue } // - table, ok := tables[reg.Width()] + table, ok := p.rangeTables[reg.Width()] if !ok { // a width <= maxStaticWidth must always have a static table. - if reg.Width() <= maxStaticWidth { + if reg.Width() <= p.maxStaticWidth { panic(fmt.Sprintf("missing static range table for width %d", reg.Width())) } // Wider registers are range-checked recursively via a call lookup. diff --git a/pkg/zkc/constraints/translate_fn.go b/pkg/zkc/constraints/translate_fn.go new file mode 100644 index 000000000..64cc4c72a --- /dev/null +++ b/pkg/zkc/constraints/translate_fn.go @@ -0,0 +1,191 @@ +// Copyright Consensys Software Inc. +// +// Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with +// the License. You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on +// an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the +// specific language governing permissions and limitations under the License. +// +// SPDX-License-Identifier: Apache-2.0 +package constraints + +import ( + "fmt" + + "github.com/LFDT-Lineth/zkc/pkg/ir/mir" + "github.com/LFDT-Lineth/zkc/pkg/schema" + "github.com/LFDT-Lineth/zkc/pkg/schema/module" + "github.com/LFDT-Lineth/zkc/pkg/schema/register" + "github.com/LFDT-Lineth/zkc/pkg/util" + "github.com/LFDT-Lineth/zkc/pkg/util/collection/bit" + "github.com/LFDT-Lineth/zkc/pkg/util/field" + "github.com/LFDT-Lineth/zkc/pkg/zkc/constraints/mirc" + tracer "github.com/LFDT-Lineth/zkc/pkg/zkc/constraints/trace" + "github.com/LFDT-Lineth/zkc/pkg/zkc/vm" +) + +func (p *constraintTranslator[W, F]) translateFunction(ctx schema.ModuleId, fn *vm.Function[W]) mir.Module[F] { + var ( + mod *schema.Table[F, mir.Constraint[F]] + name = fn.Name() + regs = toRegisters(fn.Registers()) + framing Framing[F] + // IS_PC_ program counter selectors, only for MLI. + pcSelectors []register.Id + // $ret register, used to guard lookup for OLI. + // TODO: see https://github.com/LFDT-Lineth/zkc/issues/1975 + ret register.Id + ) + // Initialise module + mod = mod.Init(name, false, false, false, fn.IsNative(), false) + // Add all registers + mod.AddRegisters(regs...) + // Native functions are backed by an external circuit, so we emit only the + // register layout and skip all framing / instruction-level constraints. + if fn.IsNative() { + return mod + } + + ret = register.NewId(mod.Width()) + // Add control registers for Multi Line Instruction + if !fn.IsOneLine() { + var ( + constraints []mir.Constraint[F] + pc = register.NewId(mod.Width() + 1) + ) + + // Create return line + mod.AddRegisters(register.NewComputed(tracer.RET_NAME, 1)) + // Create program counter + mod.AddRegisters(register.NewComputed(tracer.PC_NAME, fn.PcWidth())) + // Add IS_PC_ program counter selectors (one per code line) + pcSelectors = make([]register.Id, len(fn.Vectors())) + for c := range pcSelectors { + pcSelectors[c] = register.NewId(mod.Width()) + mod.AddRegisters(register.NewComputed(tracer.SelectorName(uint(c)), 1)) + } + // Initialise multi-line framing + framing, constraints = initMultiLineFraming[F](ctx, pc, ret, pcSelectors, regs, len(fn.Vectors())) + // Include framing constraints + mod.AddConstraints(constraints...) + } else { + framing = mirc.NewAtomicFraming[register.Id, Expr[F]]() + + mod.AddRegisters(register.NewComputed(tracer.RET_NAME, 1)) + } + // Translate all bytecode vectors + for pc, vec := range fn.Vectors() { + var ( + handle = func() string { + if fn.IsOneLine() { + return "inst" + } + // PC_0 is for padding + return fmt.Sprintf("pc%d", pc+1) + }() + // construct translator for this bytecode vector + tr = NewVectorTranslator(ctx, uint(pc), vec, framing, fn, p.program.Field()) + // extract logical constraint + constraint = tr.translate() + ) + // For atomic functions, gate the constraint on the $ret + // activity line so padding rows ($ret==0) are unconstrained. + // TODO: this is a temporary nuclear option as it brings bad perf: + // - all constraints are gated on $ret, so raising the degree of all constraints by one + // - add one column ($ret) + // see https://github.com/LFDT-Lineth/zkc/issues/1975 + // Note: we might still need to do it for OLI touching memory. + if fn.IsOneLine() { + iomf := mirc.Variable[register.Id, Expr[F]](ret, 1, 0). + NotEquals(mirc.Number[register.Id, Expr[F]](0)) + constraint = mirc.If(iomf, constraint) + } + // translate into MIR constraints + mod.AddConstraints(mir.NewVanishingConstraint(handle, ctx, util.None[int](), constraint.AsLogical())) + } + // Add range proof constraints for all registers. + // Note: while adding lookups from calls and memory read/write might add (bit) registers, + // it is safe to add range proof constraints for all registers before, as the registers + // that will be introduced later will be already range-proved (as a product of bit registers). + // Note that registers coming from control flow have been added to the module before this point, + // so they will be range-proved as well. + p.addRangeProofConstraints(mod, ctx, mod.Registers()) + // Emit lookup constraints for any function calls and memory accesses made + // by this function (recording send ports for calls into global functions). + p.addLookups(mod, ctx, fn, pcSelectors, ret) + // Done + return mod +} + +func initMultiLineFraming[F field.Element[F]](ctx module.Id, pc, ret register.Id, pcSelectors []register.Id, + regs []register.Register, numLines int, +) (Framing[F], []mir.Constraint[F]) { + var ( + // determine suitable width of PC register + pcWidth = bit.Width(uint(1 + numLines)) + // set with of RET register + retWidth = uint(1) + // + pc_i = mirc.Variable[register.Id, Expr[F]](pc, pcWidth, 0) + pc_im1 = mirc.Variable[register.Id, Expr[F]](pc, pcWidth, -1) + ret_i = mirc.Variable[register.Id, Expr[F]](ret, retWidth, 0) + ret_im1 = mirc.Variable[register.Id, Expr[F]](ret, retWidth, -1) + zero = mirc.Number[register.Id, Expr[F]](0) + one = mirc.Number[register.Id, Expr[F]](1) + ) + // PC[i]==0 ==> RET[i]==0 (prevents lookup in padding) + padding := mir.NewVanishingConstraint("padding", ctx, util.None[int](), + mirc.If(pc_i.Equals(zero), ret_i.Equals(zero)).AsLogical()) + // PC[i-1]==0 && PC[i]!=0 ==> PC[i]==1 + init := mir.NewVanishingConstraint("init", ctx, util.None[int](), + mirc.If(pc_im1.Equals(zero), mirc.If(pc_i.NotEquals(zero), pc_i.Equals(one))).AsLogical()) + // RET[i-1]!=0 ==> PC[i]==1 + reset := mir.NewVanishingConstraint("reset", ctx, util.None[int](), + mirc.If(ret_im1.NotEquals(zero), pc_i.Equals(one)).AsLogical()) + // PC[0] != 0 ==> PC[0] == 1 + first := mir.NewVanishingConstraint("first", ctx, util.Some(0), + mirc.If(pc_i.NotEquals(zero), pc_i.Equals(one)).AsLogical()) + // Build one-hot selector terms. The selector for code line c is 1 + // exactly when PC==c+1 (PC==0 is reserved for padding). + var ( + selectorTerms = make([]Expr[F], len(pcSelectors)) + weightedTerms = make([]Expr[F], len(pcSelectors)) + ) + // + for c, sel := range pcSelectors { + sel_i := mirc.Variable[register.Id, Expr[F]](sel, 1, 0) + selectorTerms[c] = sel_i + weightedTerms[c] = mirc.Number[register.Id, Expr[F]](uint(c + 1)).Multiply(sel_i) + } + // S = sum of selectors (the activity indicator). + sum := mirc.Sum(selectorTerms) + // PC == sum_c (c+1)*IS_PC_c (reconstruction) + decoding := mir.NewVanishingConstraint("pc_decoding", ctx, util.None[int](), + pc_i.Equals(mirc.Sum(weightedTerms)).AsLogical()) + // PC*S == PC i.e. exactly one selector is 1 whenever PC!=0 (and, via + // pc_decoding, none when PC==0). + exclusivity := mir.NewVanishingConstraint("is_pc_exclusivity", ctx, util.None[int](), + pc_i.Multiply(sum).Equals(pc_i).AsLogical()) + // + constraints := []mir.Constraint[F]{padding, init, reset, first, decoding, exclusivity} + // Add constancies for all input registers (if applicable): + for i, r := range regs { + if r.IsInput() { + var ( + ith = register.NewId(uint(i)) + name = fmt.Sprintf("const_%s", r.Name()) + reg_i = mirc.Variable[register.Id, Expr[F]](ith, r.Width(), 0) + reg_im1 = mirc.Variable[register.Id, Expr[F]](ith, r.Width(), -1) + ) + // (5) (PC[i]!=0 && PC[i]!=1 ==> reg[i] = reg[i-1] + constraints = append(constraints, + mir.NewVanishingConstraint(name, ctx, util.None[int](), + mirc.If(pc_i.NotEquals(zero), mirc.If(pc_i.NotEquals(one), reg_i.Equals(reg_im1))).AsLogical())) + } + } + // + return mirc.NewMultiLineFraming[register.Id, Expr[F]](pc, pcWidth, ret, 1, pcSelectors), constraints +} diff --git a/pkg/zkc/constraints/ram.go b/pkg/zkc/constraints/translate_ram.go similarity index 98% rename from pkg/zkc/constraints/ram.go rename to pkg/zkc/constraints/translate_ram.go index 236110d9a..68f30fb1c 100644 --- a/pkg/zkc/constraints/ram.go +++ b/pkg/zkc/constraints/translate_ram.go @@ -126,14 +126,12 @@ type ramLayout struct { // the finalization rows are deferred to a follow-up PR; the finalization-phase // constraints below are therefore written but vacuous (no FINL rows are emitted // yet). -func translateReadWriteMemory[W vm.Word[W], F field.Element[F]]( - ctx schema.ModuleId, m *vm.Memory[W], field field.Config, - rangeTables map[uint]rangeTable, maxStaticWidth uint) mir.Module[F] { +func (p *constraintTranslator[W, F]) translateReadWriteMemory(ctx schema.ModuleId, m *vm.Memory[W]) mir.Module[F] { // var ( mod *schema.Table[F, mir.Constraint[F]] regs = toRegisters(m.Registers()) - layout = computeRamLayout(m, field) + layout = computeRamLayout(m, p.program.Field()) ) // Initialise module. Note a leading padding row exists (EXEC == FINL == 0 // there), emitted by the tracer (see traceReadWriteMemory). A read-write @@ -167,7 +165,7 @@ func translateReadWriteMemory[W vm.Word[W], F field.Element[F]]( // value / timestamp-written columns pinned by the caller lookup — are not // otherwise constrained. 1-bit columns (phase bits, carries) get an r*r==r // constraint; wider columns a range-table lookup. - addRangeProofConstraints(mod, ctx, mod.Registers(), rangeTables, maxStaticWidth) + p.addRangeProofConstraints(mod, ctx, mod.Registers()) // return mod } diff --git a/pkg/zkc/constraints/translator.go b/pkg/zkc/constraints/translator.go index ab10de2a5..54f4aa34a 100644 --- a/pkg/zkc/constraints/translator.go +++ b/pkg/zkc/constraints/translator.go @@ -18,10 +18,8 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/ir/air" "github.com/LFDT-Lineth/zkc/pkg/ir/mir" "github.com/LFDT-Lineth/zkc/pkg/schema" - "github.com/LFDT-Lineth/zkc/pkg/schema/module" "github.com/LFDT-Lineth/zkc/pkg/schema/register" "github.com/LFDT-Lineth/zkc/pkg/util" - "github.com/LFDT-Lineth/zkc/pkg/util/collection/bit" "github.com/LFDT-Lineth/zkc/pkg/util/field" util_math "github.com/LFDT-Lineth/zkc/pkg/util/math" "github.com/LFDT-Lineth/zkc/pkg/zkc/constraints/mirc" @@ -35,21 +33,22 @@ import ( // without going through the legacy word / field machine. func GenerateMirConstraints[W vm.Word[W], F field.Element[F]](program vm.Program[W]) mir.Schema[F] { var ( - infos = program.Modules() - modules = make([]mir.Module[F], len(infos)) - // maxStaticWidth is the largest X for which 2^X <= maxStaticHeight, i.e. floor(log2(maxStaticHeight)). - // It represents the maximum register width for which a static table can be use to range-check it. - // Wider registers require recursive range modules, and the call is materialized by a function call - // during codegen. - maxStaticWidth = util_math.FloorLog2(program.MaxStaticHeight()) - // Index the static range-check tables by width, so each register can be - // range-proved by a lookup into the matching $range_un table. - rangeTables = indexRangeTables[W, F](infos, maxStaticWidth) + modules = make([]mir.Module[F], len(program.Modules())) + // construct translator + translator = newConstraintTranslator[W, F](program) ) // - for i, m := range infos { - modules[i] = translateModule[W, F](uint(i), m, infos, rangeTables, program.Field(), - maxStaticWidth, program.MaxStaticHeight()) + for i, m := range program.Modules() { + modules[i] = translator.translateModule(uint(i), m) + } + // Emit the bus connecting every global function with its call sites. This + // can only happen now, since a bus spans modules and, hence, requires them + // all to have been translated. Each bus is placed in its callee's module; + // as for lookups, placement is cosmetic but must be deterministic. + for i, m := range program.Modules() { + if fn, ok := m.(*vm.Function[W]); ok && fn.Kind().IsGlobal() { + translator.emitCallBus(modules[i], vm.ModuleId(i), fn) + } } // return schema.NewUniformSchema(modules) @@ -65,29 +64,67 @@ func GenerateAirConstraints[W vm.Word[W], F field.Element[F]](program vm.Program return mir.LowerToAir(mirc, program.Field().BandWidth, mir.DEFAULT_OPTIMISATION_LEVEL) } -func translateModule[W vm.Word[W], F field.Element[F]](ctx schema.ModuleId, m vm.Module[W], - infos []vm.Module[W], rangeTables map[uint]rangeTable, field field.Config, maxStaticWidth, maxStaticHeight uint, -) mir.Module[F] { +// constraintTranslator provides global context required for generating +// constraints. +type constraintTranslator[W vm.Word[W], F field.Element[F]] struct { + program vm.Program[W] + // rangeTables indexes the static range-check tables by width, so each + // register can be range-proved by a lookup into the matching $range_un + // table. + rangeTables map[uint]rangeTable + // sendPorts records the send port of every call into a global function, + // keyed by the callee. These are accumulated as each caller is translated, + // since a bus spans modules and, hence, can only be constructed once every + // module has been translated (see emitCallBus). + sendPorts map[vm.ModuleId][]mir.BusPort + // maxStaticWidth determines the maximum register width for which a static table + // can be use to range-check it. Wider registers require recursive range + // modules, and the call is materialized by a function call during codegen. + maxStaticWidth uint +} + +// newConstraintTranslator constructs a new translator with the given context +// required for translation. +func newConstraintTranslator[W vm.Word[W], F field.Element[F]](program vm.Program[W]) constraintTranslator[W, F] { + var ( + // Calculate maximum register width which can be range-checked using just a + // static reference table. + maxStaticWidth = util_math.FloorLog2(program.MaxStaticHeight()) + // Index the static range-check tables by width, so each register can be + // range-proved by a lookup into the matching $range_un table. + rangeTables = indexRangeTables[W, F](program, maxStaticWidth) + // Accumulates the send port of every call into a global function. + sendPorts = make(map[vm.ModuleId][]mir.BusPort) + ) + // + return constraintTranslator[W, F]{program, rangeTables, sendPorts, maxStaticWidth} +} + +// addSendPort records a send port for the bus of a given (global) callee. +func (p *constraintTranslator[W, F]) addSendPort(calleeId vm.ModuleId, port mir.BusPort) { + p.sendPorts[calleeId] = append(p.sendPorts[calleeId], port) +} + +func (p *constraintTranslator[W, F]) translateModule(ctx schema.ModuleId, m vm.Module[W]) mir.Module[F] { switch m := m.(type) { case *vm.Function[W]: - return translateFunction[W, F](ctx, m, infos, rangeTables, field, maxStaticWidth) + return p.translateFunction(ctx, m) case *vm.Memory[W]: if m.IsStatic() { - return translateStaticMemory[W, F](ctx, m, maxStaticHeight) + return p.translateStaticMemory(ctx, m) } else if m.IsReadOnly() { - return translateReadOnlyMemory[W, F](ctx, m, rangeTables, maxStaticWidth) + return p.translateReadOnlyMemory(ctx, m) } else if m.IsWriteOnly() { - return translateWriteOnceMemory[W, F](ctx, m, rangeTables, maxStaticWidth) + return p.translateWriteOnceMemory(ctx, m) } // - return translateReadWriteMemory[W, F](ctx, m, field, rangeTables, maxStaticWidth) + return p.translateReadWriteMemory(ctx, m) default: panic(fmt.Sprintf("unknown module \"%s\" encountered", m.Name())) } } -func translateStaticMemory[W vm.Word[W], F field.Element[F]](_ schema.ModuleId, m *vm.Memory[W], - maxStaticHeight uint) mir.Module[F] { +func (p *constraintTranslator[W, F]) translateStaticMemory(_ schema.ModuleId, m *vm.Memory[W]) mir.Module[F] { var ( mod *schema.Table[F, mir.Constraint[F]] name = m.Name() @@ -95,8 +132,9 @@ func translateStaticMemory[W vm.Word[W], F field.Element[F]](_ schema.ModuleId, inputs = toRegisters(m.AddressRegisters()) outputs = toRegisters(m.DataRegisters()) // Convert the static contents from words into field elements. - contents = toFieldElements[W, F](m.StaticContents()) - paddedHeight = util_math.NextPowerOfTwo(uint(len(contents))) + contents = toFieldElements[W, F](m.StaticContents()) + paddedHeight = util_math.NextPowerOfTwo(uint(len(contents))) + maxStaticHeight = p.program.MaxStaticHeight() ) if paddedHeight > maxStaticHeight { panic(fmt.Sprintf("static memory \"%s\" exceeds maximum allowed height of %d", m.Name(), maxStaticHeight)) @@ -113,25 +151,22 @@ func translateStaticMemory[W vm.Word[W], F field.Element[F]](_ schema.ModuleId, return mod } -func translateReadOnlyMemory[W vm.Word[W], F field.Element[F]]( - ctx schema.ModuleId, m *vm.Memory[W], rangeTables map[uint]rangeTable, maxStaticWidth uint) mir.Module[F] { +func (p *constraintTranslator[W, F]) translateReadOnlyMemory(ctx schema.ModuleId, m *vm.Memory[W]) mir.Module[F] { var name = m.Name() - return translateAccessOnceMemory[W, F](ctx, m, name, rangeTables, maxStaticWidth) + return p.translateAccessOnceMemory(ctx, m, name) } // Write once memory and read only memory are equivalent on the constraints level -func translateWriteOnceMemory[W vm.Word[W], F field.Element[F]]( - ctx schema.ModuleId, m *vm.Memory[W], rangeTables map[uint]rangeTable, maxStaticWidth uint) mir.Module[F] { +func (p *constraintTranslator[W, F]) translateWriteOnceMemory(ctx schema.ModuleId, m *vm.Memory[W]) mir.Module[F] { var name = m.Name() - return translateAccessOnceMemory[W, F](ctx, m, name, rangeTables, maxStaticWidth) + return p.translateAccessOnceMemory(ctx, m, name) } // translateAccessOnceMemory handles both // - read once memory // - write once memory -func translateAccessOnceMemory[W vm.Word[W], F field.Element[F]]( - ctx schema.ModuleId, m *vm.Memory[W], name string, - rangeTables map[uint]rangeTable, maxStaticWidth uint) (mod mir.Module[F]) { +func (p *constraintTranslator[W, F]) translateAccessOnceMemory(ctx schema.ModuleId, m *vm.Memory[W], name string, +) (mod mir.Module[F]) { var ( memoryModule *schema.Table[F, mir.Constraint[F]] regs = toRegisters(m.Registers()) @@ -199,7 +234,7 @@ func translateAccessOnceMemory[W vm.Word[W], F field.Element[F]]( } memoryModule.AddConstraints(constraints...) - addRangeProofConstraints(memoryModule, ctx, memoryModule.Registers(), rangeTables, maxStaticWidth) + p.addRangeProofConstraints(memoryModule, ctx, memoryModule.Registers()) return memoryModule } @@ -318,167 +353,3 @@ func multiLineAddressConstraints[F field.Element[F]]( return constraints } - -func translateFunction[W vm.Word[W], F field.Element[F]](ctx schema.ModuleId, fn *vm.Function[W], - infos []vm.Module[W], rangeTables map[uint]rangeTable, field field.Config, maxStaticWidth uint) mir.Module[F] { - var ( - mod *schema.Table[F, mir.Constraint[F]] - name = fn.Name() - regs = toRegisters(fn.Registers()) - framing Framing[F] - // IS_PC_ program counter selectors, only for MLI. - pcSelectors []register.Id - // $ret register, used to guard lookup for OLI. - // TODO: see https://github.com/LFDT-Lineth/zkc/issues/1975 - ret register.Id - ) - // Initialise module - mod = mod.Init(name, false, false, false, fn.IsNative(), false) - // Add all registers - mod.AddRegisters(regs...) - // Native functions are backed by an external circuit, so we emit only the - // register layout and skip all framing / instruction-level constraints. - if fn.IsNative() { - return mod - } - - ret = register.NewId(mod.Width()) - // Add control registers for Multi Line Instruction - if !fn.IsOneLine() { - var ( - constraints []mir.Constraint[F] - pc = register.NewId(mod.Width() + 1) - ) - - // Create return line - mod.AddRegisters(register.NewComputed(tracer.RET_NAME, 1)) - // Create program counter - mod.AddRegisters(register.NewComputed(tracer.PC_NAME, fn.PcWidth())) - // Add IS_PC_ program counter selectors (one per code line) - pcSelectors = make([]register.Id, len(fn.Vectors())) - for c := range pcSelectors { - pcSelectors[c] = register.NewId(mod.Width()) - mod.AddRegisters(register.NewComputed(tracer.SelectorName(uint(c)), 1)) - } - // Initialise multi-line framing - framing, constraints = initMultiLineFraming[F](ctx, pc, ret, pcSelectors, regs, len(fn.Vectors())) - // Include framing constraints - mod.AddConstraints(constraints...) - } else { - framing = mirc.NewAtomicFraming[register.Id, Expr[F]]() - - mod.AddRegisters(register.NewComputed(tracer.RET_NAME, 1)) - } - // Translate all bytecode vectors - for pc, vec := range fn.Vectors() { - var ( - handle = func() string { - if fn.IsOneLine() { - return "inst" - } - // PC_0 is for padding - return fmt.Sprintf("pc%d", pc+1) - }() - // construct translator for this bytecode vector - tr = NewVectorTranslator(ctx, uint(pc), vec, framing, fn, field) - // extract logical constraint - constraint = tr.translate() - ) - // For atomic functions, gate the constraint on the $ret - // activity line so padding rows ($ret==0) are unconstrained. - // TODO: this is a temporary nuclear option as it brings bad perf: - // - all constraints are gated on $ret, so raising the degree of all constraints by one - // - add one column ($ret) - // see https://github.com/LFDT-Lineth/zkc/issues/1975 - // Note: we might still need to do it for OLI touching memory. - if fn.IsOneLine() { - iomf := mirc.Variable[register.Id, Expr[F]](ret, 1, 0). - NotEquals(mirc.Number[register.Id, Expr[F]](0)) - constraint = mirc.If(iomf, constraint) - } - // translate into MIR constraints - mod.AddConstraints(mir.NewVanishingConstraint(handle, ctx, util.None[int](), constraint.AsLogical())) - } - // Add range proof constraints for all registers. - // Note: while adding lookups from calls and memory read/write might add (bit) registers, - // it is safe to add range proof constraints for all registers before, as the registers - // that will be introduced later will be already range-proved (as a product of bit registers). - // Note that registers coming from control flow have been added to the module before this point, - // so they will be range-proved as well. - addRangeProofConstraints(mod, ctx, mod.Registers(), rangeTables, maxStaticWidth) - // Emit lookup constraints for any function calls and memory accesses made - // by this function. - addLookups(mod, ctx, fn, pcSelectors, ret, infos, field) - // Done - return mod -} - -func initMultiLineFraming[F field.Element[F]](ctx module.Id, pc, ret register.Id, pcSelectors []register.Id, - regs []register.Register, numLines int, -) (Framing[F], []mir.Constraint[F]) { - var ( - // determine suitable width of PC register - pcWidth = bit.Width(uint(1 + numLines)) - // set with of RET register - retWidth = uint(1) - // - pc_i = mirc.Variable[register.Id, Expr[F]](pc, pcWidth, 0) - pc_im1 = mirc.Variable[register.Id, Expr[F]](pc, pcWidth, -1) - ret_i = mirc.Variable[register.Id, Expr[F]](ret, retWidth, 0) - ret_im1 = mirc.Variable[register.Id, Expr[F]](ret, retWidth, -1) - zero = mirc.Number[register.Id, Expr[F]](0) - one = mirc.Number[register.Id, Expr[F]](1) - ) - // PC[i]==0 ==> RET[i]==0 (prevents lookup in padding) - padding := mir.NewVanishingConstraint("padding", ctx, util.None[int](), - mirc.If(pc_i.Equals(zero), ret_i.Equals(zero)).AsLogical()) - // PC[i-1]==0 && PC[i]!=0 ==> PC[i]==1 - init := mir.NewVanishingConstraint("init", ctx, util.None[int](), - mirc.If(pc_im1.Equals(zero), mirc.If(pc_i.NotEquals(zero), pc_i.Equals(one))).AsLogical()) - // RET[i-1]!=0 ==> PC[i]==1 - reset := mir.NewVanishingConstraint("reset", ctx, util.None[int](), - mirc.If(ret_im1.NotEquals(zero), pc_i.Equals(one)).AsLogical()) - // PC[0] != 0 ==> PC[0] == 1 - first := mir.NewVanishingConstraint("first", ctx, util.Some(0), - mirc.If(pc_i.NotEquals(zero), pc_i.Equals(one)).AsLogical()) - // Build one-hot selector terms. The selector for code line c is 1 - // exactly when PC==c+1 (PC==0 is reserved for padding). - var ( - selectorTerms = make([]Expr[F], len(pcSelectors)) - weightedTerms = make([]Expr[F], len(pcSelectors)) - ) - // - for c, sel := range pcSelectors { - sel_i := mirc.Variable[register.Id, Expr[F]](sel, 1, 0) - selectorTerms[c] = sel_i - weightedTerms[c] = mirc.Number[register.Id, Expr[F]](uint(c + 1)).Multiply(sel_i) - } - // S = sum of selectors (the activity indicator). - sum := mirc.Sum(selectorTerms) - // PC == sum_c (c+1)*IS_PC_c (reconstruction) - decoding := mir.NewVanishingConstraint("pc_decoding", ctx, util.None[int](), - pc_i.Equals(mirc.Sum(weightedTerms)).AsLogical()) - // PC*S == PC i.e. exactly one selector is 1 whenever PC!=0 (and, via - // pc_decoding, none when PC==0). - exclusivity := mir.NewVanishingConstraint("is_pc_exclusivity", ctx, util.None[int](), - pc_i.Multiply(sum).Equals(pc_i).AsLogical()) - // - constraints := []mir.Constraint[F]{padding, init, reset, first, decoding, exclusivity} - // Add constancies for all input registers (if applicable): - for i, r := range regs { - if r.IsInput() { - var ( - ith = register.NewId(uint(i)) - name = fmt.Sprintf("const_%s", r.Name()) - reg_i = mirc.Variable[register.Id, Expr[F]](ith, r.Width(), 0) - reg_im1 = mirc.Variable[register.Id, Expr[F]](ith, r.Width(), -1) - ) - // (5) (PC[i]!=0 && PC[i]!=1 ==> reg[i] = reg[i-1] - constraints = append(constraints, - mir.NewVanishingConstraint(name, ctx, util.None[int](), - mirc.If(pc_i.NotEquals(zero), mirc.If(pc_i.NotEquals(one), reg_i.Equals(reg_im1))).AsLogical())) - } - } - // - return mirc.NewMultiLineFraming[register.Id, Expr[F]](pc, pcWidth, ret, 1, pcSelectors), constraints -} diff --git a/pkg/zkc/constraints/validate.go b/pkg/zkc/constraints/validate.go index 1e1096e0e..19fd8b4ae 100644 --- a/pkg/zkc/constraints/validate.go +++ b/pkg/zkc/constraints/validate.go @@ -125,7 +125,7 @@ func validateBusConstraint[F field.Element[F]](c bus.Constraint[F], validations } // validateModuleReachability checks that every module is reached by some chain -// of lookups originating in the entry point "main". +// of lookups (or buses) originating in the entry point "main". func validateModuleReachability[F field.Element[F]](schema sc.AnySchema[F]) (errs []error) { // TODO: https://github.com/LFDT-Lineth/zkc/issues/1869 parametrize "main" name for _, name := range UnreachableModules(schema) { @@ -137,11 +137,13 @@ func validateModuleReachability[F field.Element[F]](schema sc.AnySchema[F]) (err } // UnreachableModules returns the name of every module in the given schema which -// cannot be reached by any chain of lookups originating in the entry point -// "main". A lookup reaches a module when one of its target vectors sits in -// that module; it emanates from the modules its source vectors sit in. When -// the schema has no "main" module there is no entry point, and every module is -// considered reachable. +// cannot be reached by any chain of lookups (or buses) originating in the entry +// point "main". A lookup reaches a module when one of its target vectors sits +// in that module; it emanates from the modules its source vectors sit in. +// Likewise, a bus reaches the modules of its receive ports and emanates from +// those of its send ports (this is how a call into a global function is +// connected, see emitCallBus). When the schema has no "main" module there is +// no entry point, and every module is considered reachable. func UnreachableModules[F field.Element[F]](schema sc.AnySchema[F]) (unreachable []string) { var ( reached = make([]bool, schema.Modules().Count()) @@ -160,16 +162,20 @@ func UnreachableModules[F field.Element[F]](schema sc.AnySchema[F]) (unreachable if len(worklist) == 0 { return nil } - // Index every lookup by the modules it emanates from. + // Index every lookup and bus by the modules it emanates from. for iter := schema.Constraints(); iter.HasNext(); { switch c := iter.Next().(type) { case air.LookupConstraint[F]: indexLookupEdges(c.Unwrap(), outgoing) case mir.LookupConstraint[F]: indexLookupEdges(c, outgoing) + case air.BusConstraint[F]: + indexBusEdges(c.Unwrap(), outgoing) + case mir.BusConstraint[F]: + indexBusEdges(c, outgoing) } } - // Follow lookups from reached modules until a fixpoint is hit. + // Follow lookups and buses from reached modules until a fixpoint is hit. for len(worklist) > 0 { mid := worklist[len(worklist)-1] worklist = worklist[:len(worklist)-1] @@ -201,6 +207,16 @@ func indexLookupEdges[F field.Element[F]](c lookup.Constraint[F], outgoing map[s } } +// indexBusEdges records, for each module sending on the given bus, the modules +// receiving from it. +func indexBusEdges[F field.Element[F]](c bus.Constraint[F], outgoing map[sc.ModuleId][]sc.ModuleId) { + for _, send := range c.Sends { + for _, receive := range c.Receives { + outgoing[send.Context()] = append(outgoing[send.Context()], receive.Context()) + } + } +} + // validateStaticTables validates that all static tables in the given schema have a power-of-two height. func validateStaticTables[F field.Element[F]](schema sc.AnySchema[F]) []error { var errors []error diff --git a/pkg/zkc/vm/internal/checkpoint/checkpoint.go b/pkg/zkc/vm/internal/checkpoint/checkpoint.go index de2c30ec6..48b50d079 100644 --- a/pkg/zkc/vm/internal/checkpoint/checkpoint.go +++ b/pkg/zkc/vm/internal/checkpoint/checkpoint.go @@ -1,7 +1,15 @@ -// Package checkpoint provides the data structures used to capture (a snapshot -// of) the state of an executing machine, so that execution can later be resumed -// from that point. See CheckPoint for the central type and a discussion of how -// such snapshots may be optimised. +// Copyright Consensys Software Inc. +// +// Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with +// the License. You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on +// an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the +// specific language governing permissions and limitations under the License. +// +// SPDX-License-Identifier: Apache-2.0 package checkpoint import ( diff --git a/pkg/zkc/vm/internal/checkpoint/memory.go b/pkg/zkc/vm/internal/checkpoint/memory.go index 9a1fdf488..4ff64e1cd 100644 --- a/pkg/zkc/vm/internal/checkpoint/memory.go +++ b/pkg/zkc/vm/internal/checkpoint/memory.go @@ -1,3 +1,15 @@ +// Copyright Consensys Software Inc. +// +// Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with +// the License. You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on +// an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the +// specific language governing permissions and limitations under the License. +// +// SPDX-License-Identifier: Apache-2.0 package checkpoint // Memory captures a snapshot of the contents of a single (mutable) memory diff --git a/pkg/zkc/vm/internal/checkpoint/page.go b/pkg/zkc/vm/internal/checkpoint/page.go index 6218d9098..afefbe229 100644 --- a/pkg/zkc/vm/internal/checkpoint/page.go +++ b/pkg/zkc/vm/internal/checkpoint/page.go @@ -1,3 +1,15 @@ +// Copyright Consensys Software Inc. +// +// Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with +// the License. You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on +// an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the +// specific language governing permissions and limitations under the License. +// +// SPDX-License-Identifier: Apache-2.0 package checkpoint import "slices" diff --git a/pkg/zkc/vm/internal/descriptor/function_kind.go b/pkg/zkc/vm/internal/descriptor/function_kind.go index 68211841c..7fe3eea8d 100644 --- a/pkg/zkc/vm/internal/descriptor/function_kind.go +++ b/pkg/zkc/vm/internal/descriptor/function_kind.go @@ -113,6 +113,10 @@ func (p *FunctionKind) GobEncode() ([]byte, error) { return nil, err } // + if err := gobEncoder.Encode(p.global); err != nil { + return nil, err + } + // return buffer.Bytes(), nil } @@ -141,6 +145,10 @@ func (p *FunctionKind) GobDecode(data []byte) error { return err } // + if err := gobDecoder.Decode(&p.global); err != nil { + return err + } + // return nil } diff --git a/pkg/zkc/vm/internal/interpreter/interpreter.go b/pkg/zkc/vm/internal/interpreter/interpreter.go index 345840d07..5575bdcd8 100644 --- a/pkg/zkc/vm/internal/interpreter/interpreter.go +++ b/pkg/zkc/vm/internal/interpreter/interpreter.go @@ -605,9 +605,9 @@ func (p *Interpreter[W]) Memory(mid uint16) Memory[W] { // its outermost frame (RET with an empty call stack) or an error occurs (e.g. // arithmetic overflow, or an explicit FAIL). It returns the number of steps // actually executed together with any error. -func (p *Interpreter[W]) Execute(steps uint) (uint, error) { +func (p *Interpreter[W]) Execute(steps uint64) (uint64, error) { var ( - nsteps = uint(0) + nsteps = uint64(0) err error frame []W = p.dataStack.SliceEnd(uint(p.fp)) bytecodes = p.program.Bytecodes() diff --git a/pkg/zkc/vm/machine.go b/pkg/zkc/vm/machine.go index baa31dca9..562a6c871 100644 --- a/pkg/zkc/vm/machine.go +++ b/pkg/zkc/vm/machine.go @@ -35,7 +35,7 @@ type Core[W Word[W]] interface { Boot(fun string, input map[string][]W) error // Execute the machine for the given number of steps, returning the actual // number of steps executed and an error (if execution failed). - Execute(steps uint) (uint, error) + Execute(steps uint64) (uint64, error) // Return array of (non-static) input memories Inputs() iter.Iterator[interpreter.InputOutput[W]] // Return array of output memories @@ -64,11 +64,11 @@ type ProgramPoint = descriptor.ProgramPoint // internal machine failure which is not expected (and signals some kind of bug // somewhere). The traceable flag holds when the given execution can be traced // (i.e. when no errors in the latter category arise). -func BootAndExecute[W Word[W], M Core[W]](m M, input map[string][]byte, n uint, +func BootAndExecute[W Word[W], M Core[W]](m M, input map[string][]byte, n uint64, ) (output map[string][]byte, traceable bool, errs []error) { // var ( - steps uint + steps uint64 inputs map[string][]W stats = util.NewPerfStats() ) @@ -101,7 +101,7 @@ func BootAndCheckpoint[W Word[W]](pr Program[W], in map[string][]byte, strategy ) (checkpoints []CheckPoint[W], outputs map[string][]byte, traceable bool, errors []error) { var ( err error - steps uint + steps uint64 stats = util.NewPerfStats() // specify how many steps each shard will be clk = util.NewCounter(strategy.shardSteps) @@ -198,7 +198,7 @@ func BootAndTrace[W Word[W], F Element[F], T Tracer[W, F, T]](pr Program[W], inp // traceable flag holds when the given execution can be traced (i.e. when no // errors in the latter category arise). func RestoreAndTraceFor[W Word[W], F Element[F], T Tracer[W, F, T]](pr Program[W], cp CheckPoint[W], - fn string, nsteps uint64) (trace Trace[F], errs []error) { + fn string, nsteps uint64) (steps uint64, trace Trace[F], errs []error) { // var ( // constracter tracer @@ -212,24 +212,20 @@ func RestoreAndTraceFor[W Word[W], F Element[F], T Tracer[W, F, T]](pr Program[W bci := constructTraceForInterpreter(pr, fn, nsteps, tracer) // Sanity check error arising construct the interpreter. if bci == nil { - return nil, []error{ + return 0, nil, []error{ fmt.Errorf("unknown function \"%s\"", fn), } } // Execute the given machine - if traceable, errs = RestoreAndExecute(bci, cp, math.MaxUint); !traceable { - return nil, errs + if steps, traceable, errs = RestoreAndExecute(bci, cp, math.MaxUint); !traceable { + return steps, nil, errs } - // - var stats = util.NewPerfStats() // Apply post processing array.Apply(bci.ExtractMemory(), func(_ uint, p util.Pair[uint16, RuntimeMemory[W]]) { tracer.TraceMemory(p.Left, p.Right, pr.Field()) }) - // Done - stats.Log("Trace processing") // - return tracer.Build(), errs + return steps, tracer.Build(), errs } // RestoreAndExecute restores the given machine from a checkpoint, and continues @@ -239,12 +235,11 @@ func RestoreAndTraceFor[W Word[W], F Element[F], T Tracer[W, F, T]](pr Program[W // machine failure which is not expected (and signals some kind of bug // somewhere). The traceable flag holds when the given execution can be traced // (i.e. when no errors in the latter category arise). -func RestoreAndExecute[W Word[W], M Core[W]](m M, cp CheckPoint[W], n uint) (traceable bool, errs []error) { +func RestoreAndExecute[W Word[W], M Core[W]](m M, cp CheckPoint[W], n uint64, +) (steps uint64, traceable bool, errs []error) { // var ( - steps uint - err error - stats = util.NewPerfStats() + err error ) // Restore machine state from checkpoint m.Restore(cp) @@ -257,16 +252,14 @@ func RestoreAndExecute[W Word[W], M Core[W]](m M, cp CheckPoint[W], n uint) (tra // Success traceable = true } - // Log stats - stats.Log(fmt.Sprintf("Machine resumed execution (%d steps)", steps)) // - return traceable, errs + return steps, traceable, errs } // ExecuteAll executes a given machine to completion in chunks of n steps, // returning the number of steps executed and/or any error arising. -func ExecuteAll[W Word[W], M Core[W]](machine M, n uint) (uint, error) { - var nsteps uint +func ExecuteAll[W Word[W], M Core[W]](machine M, n uint64) (uint64, error) { + var nsteps uint64 // for { // Execute upto n steps diff --git a/pkg/zkc/vm/trace_builder.go b/pkg/zkc/vm/trace_builder.go index ccae95537..56be4b4b3 100644 --- a/pkg/zkc/vm/trace_builder.go +++ b/pkg/zkc/vm/trace_builder.go @@ -16,6 +16,7 @@ import ( "github.com/LFDT-Lineth/zkc/pkg/trace" "github.com/LFDT-Lineth/zkc/pkg/util/collection/array" "github.com/LFDT-Lineth/zkc/pkg/util/field" + log "github.com/sirupsen/logrus" ) // Trace defines the type of a general trace @@ -41,16 +42,17 @@ type Tracer[W Word[W], F Element[F], T any] interface { // abstracts the myriad different ways this can be done (e.g. sharding, // parallelism, etc). type TraceBuilder[W Word[W], F field.Element[F], T Tracer[W, F, T]] struct { - config TraceConfig - tracing Program[W] + config TraceConfig + execution Program[W] + tracing Program[W] } // NewTraceBuilder constructs a default tracer builder which, most likely, // should be further configured before use. func NewTraceBuilder[W Word[W], F Element[F], T Tracer[W, F, T]](config TraceConfig, - tracing Program[W]) TraceBuilder[W, F, T] { + execution Program[W], tracing Program[W]) TraceBuilder[W, F, T] { // - return TraceBuilder[W, F, T]{config, tracing} + return TraceBuilder[W, F, T]{config, execution, tracing} } // BootAndTrace generates a suitable trace from the given inputs for the contraints @@ -78,7 +80,7 @@ func (p TraceBuilder[W, F, T]) bootAndTraceShards(inputs map[string][]byte, var ( strategy = p.config.shardingStrategy.Unwrap() // fast mode execution to generate checkpoints - checkpoints, outputs, traceable, errors = BootAndCheckpoint(p.tracing, inputs, strategy) + checkpoints, outputs, traceable, errors = BootAndCheckpoint(p.execution, inputs, strategy) // traces = make([]Trace[F], len(checkpoints)) ) @@ -108,7 +110,11 @@ func (p TraceBuilder[W, F, T]) traceCheckPoints(checkpoints []CheckPoint[W]) (jo strategy = p.config.shardingStrategy.Unwrap() // Construct tracing function traceFn = func(i uint, cp CheckPoint[W]) traceJob[F] { - var steps = strategy.shardSteps + var ( + steps = strategy.shardSteps + trace Trace[F] + errs []error + ) // Increment steps for all except first shard to account for the // fact that restoring at the exact point the breakpoint was // triggered will naturally trigger it again. @@ -116,7 +122,9 @@ func (p TraceBuilder[W, F, T]) traceCheckPoints(checkpoints []CheckPoint[W]) (jo steps++ } // Trace ith shard - var trace, errs = RestoreAndTraceFor[W, F, T](p.tracing, cp, strategy.shardFunction, steps) + steps, trace, errs = RestoreAndTraceFor[W, F, T](p.tracing, cp, strategy.shardFunction, steps) + // Log stats + log.Debug("[SHARD ", i, "] machine resumed execution (", steps, " steps)") // Done return traceJob[F]{trace, errs} } diff --git a/testdata/zkc/invalid/global_02.zkc b/testdata/zkc/invalid/global_02.zkc new file mode 100644 index 000000000..cdd082eb4 --- /dev/null +++ b/testdata/zkc/invalid/global_02.zkc @@ -0,0 +1,11 @@ +//error:5:1-16:global function must not be native +// global functions must not be native. +#[native] +#[global] +fn f(x:u8) -> ! { + fail +} + +fn main() { + f!(0) +}