diff --git a/pkg/cmd/corset/check.go b/pkg/cmd/corset/check.go index 30f890d1b..994430b36 100644 --- a/pkg/cmd/corset/check.go +++ b/pkg/cmd/corset/check.go @@ -18,21 +18,17 @@ 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" "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 +172,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 +188,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 +196,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 +207,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 +217,32 @@ 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 + errs []error + ) + // + 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 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 +253,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 +272,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 +306,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 +314,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..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" @@ -52,7 +53,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 +92,19 @@ 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) + var shards []tr.Shard[F] + + shards, errors = stack.TraceBuilder().Build(schema, []tr.Shard[F]{tracefile[0]}) + trace = shards[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 +124,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 +155,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 +167,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..be6443c26 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 @@ -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,58 +232,44 @@ 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 tr.Trace[F] - ) - // 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) - } - // - 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(window) + } } } @@ -294,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.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..adb182d80 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) @@ -177,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/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..cf6d3d59b 100644 --- a/pkg/ir/builder/alignment.go +++ b/pkg/ir/builder/alignment.go @@ -57,11 +57,10 @@ 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 ( - 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 6104e2af9..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" ) @@ -26,11 +25,9 @@ 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 - stats = util.NewPerfStats() // Flatten all columns columns, errs = flattenTrace(schema, tr) // Mapping function @@ -54,13 +51,11 @@ 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...) } -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..8a693c659 100644 --- a/pkg/ir/trace_builder.go +++ b/pkg/ir/trace_builder.go @@ -17,8 +17,8 @@ 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/collection/array" "github.com/LFDT-Lineth/zkc/pkg/util/field" ) @@ -44,15 +44,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 +61,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,18 +111,35 @@ 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) { 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/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..493f2ae49 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,37 +216,40 @@ 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 ( + // Map the legacy padding toggle onto a padding strategy. + paddingStrategy = ir.NaryRowPadding(0) + ) + // 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 + 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) + // 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()) } } @@ -304,178 +293,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}, -} - -// 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 +// 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", } -// 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 + t.Errorf("encountered deprecated test file: %s", filename) } - // 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()) - } - } - // - 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..3b41b5d9d 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,20 @@ 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") +} + +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 57eefe88d..391e63552 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", 256)) } 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", 256)) } 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", 256)) } 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/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/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..234aa6b23 --- /dev/null +++ b/pkg/zkc/compiler/validate/global.go @@ -0,0 +1,52 @@ +// 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 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 + // + 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")...) + } + // + 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/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..d4cc2aa8b 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,37 +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, rtr 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 - rtr, output, errs = builder.BootAndTrace(input) + trace, output, errors = builder.BootAndTrace(input) // - if rtr != nil { - var berrs []error - // Extract AIR constraints - constraints := p.AirConstraints() + stats.Log(fmt.Sprintf("Trace generation (%d shards)", len(trace))) + // + if len(trace) > 0 { + var errs []error + // Construct trace builder + 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](). + 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()) - // Build the trace (finally) - rtr, berrs = builder.Build(constraints, rtr) - // Include any builder errors - errs = append(errs, berrs...) - } + ) + // Apply trace expansion + etr, errors := builder.Build(constraints, tr) // - stats.Log("Trace generation") + stats.Log(fmt.Sprintf("Trace expansion (%d shards)", len(etr))) // - return output, rtr, 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 b347b1241..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,14 +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]: - 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) } } } @@ -294,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 @@ -319,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. @@ -328,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 @@ -350,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. @@ -378,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})) @@ -406,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/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/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 fbdcfe74b..7fe3eea8d 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 { @@ -100,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 } @@ -128,10 +145,14 @@ func (p *FunctionKind) GobDecode(data []byte) error { return err } // + if err := gobDecoder.Decode(&p.global); err != nil { + return err + } + // return nil } 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/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 c71af11db..56be4b4b3 100644 --- a/pkg/zkc/vm/trace_builder.go +++ b/pkg/zkc/vm/trace_builder.go @@ -14,13 +14,13 @@ 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" + log "github.com/sirupsen/logrus" ) // 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,23 +35,24 @@ 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 // 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 @@ -59,47 +60,27 @@ 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() // 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)) ) @@ -129,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. @@ -137,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/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/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) +} 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 //