constraints

package
v1.2.23 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Jul 22, 2026 License: Apache-2.0 Imports: 33 Imported by: 0

Documentation

Overview

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

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

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

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

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

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

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

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

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

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

Index

Constants

View Source 
const BINFILE_MAJOR_VERSION uint16 = 0

BINFILE_MAJOR_VERSION is the major version of the binary file format. Regardless of version, the file always begins with the ZKBINARY identifier followed by a hand-rolled binary Header. The encoding of everything after the header is determined by the major version.

View Source 
const BINFILE_MINOR_VERSION uint16 = 0

BINFILE_MINOR_VERSION is the minor version of the binary file format. Files with a lower minor version remain readable by this implementation, but files produced by this implementation may not be readable by older versions.

Variables

View Source 
var DEFAULT_TRACE_CONFIG = TraceConfig{
	// contains filtered or unexported fields
}

DEFAULT_TRACE_CONFIG defines a default configuration for tracing.

View Source 
var ZKC_EXEC [8]byte = [8]byte{'z', 'k', 'c', ' ', 'e', 'x', 'e', 'c'}

ZKC_EXEC is used as the file identifier for binary file types. This just helps us identify actual binary files from corrupted files.

Functions

func GenerateAirConstraints 

func GenerateAirConstraints[W vm.Word[W], F field.Element[F]](program vm.Program[W], field field.Config,
	maxStaticDepth uint) air.Schema[F]

GenerateAirConstraints is responsible for converting a bytecode program into a corresponding set of AIR constraints.

func GenerateMirConstraints 

func GenerateMirConstraints[W vm.Word[W], F field.Element[F]](program vm.Program[W], field field.Config,
	maxStaticDepth uint) mir.Schema[F]

GenerateMirConstraints is responsible for converting a bytecode program into a corresponding set of MIR constraints. The translation operates directly over the bytecode program (its modules, registers and bytecode vectors), without going through the legacy word / field machine.

func GetAttribute 

func GetAttribute[T Attribute, F field.Element[F]](binf *BinaryFile[F]) (T, bool)

GetAttribute returns the first instance of a given attribute, or nil if none exists.

func IsBinaryFile 

func IsBinaryFile(data []byte) bool

IsBinaryFile checks whether the given data file begins with the expected "zkc exec" identifier.

Types

type Attribute 

type Attribute interface {
	// AttributeName returns the name of this attribute.
	AttributeName() string
}

Attribute is an extension point for storing arbitrary metadata alongside the compiled schema. Typical uses include source-to-column mappings and debug/profiling annotations. Attribute values must be gob-encodable.

type BinaryFile 

type BinaryFile[F field.Element[F]] struct {
	// contains filtered or unexported fields
}

BinaryFile provides two pieces of functionality: (i) a means for serialising and deserialising a set of AIR constraints; (ii) a means for generating a trace for those constraints from a given set of inputs. Thus, we can write a set of constraints to a binary file (e.g. on disk) which can then be read back and used to generate a zero-knowledge proof.

func NewBinaryFile 

func NewBinaryFile[F field.Element[F]](metadata []byte, attributes []Attribute, config field.Config,
	maxStaticDepth uint, machine vm.Program[vm.Uint]) *BinaryFile[F]

NewBinaryFile constructs a BinaryFile with a header stamped at the current major/minor version. Metadata is an optional JSON blob stored verbatim in the header (pass nil for none). A field configuration is required to allow clients to check they are targeting the expected field.

func (*BinaryFile[F]) AirConstraints 

func (p *BinaryFile[F]) AirConstraints() air.Schema[F]

AirConstraints returns the arithmetic (AIR) constraints encoded in this file.

func (*BinaryFile[F]) Check 

func (p *BinaryFile[F]) Check(tr trace.Trace[F], config TraceConfig) []schema.Failure

Check a given trace against the constraints embodied in this constraints file, potentially producing one (or more) constraint failures.

func (*BinaryFile[F]) Execute 

func (p *BinaryFile[F]) Execute(input map[string][]byte, n uint) (output map[string][]byte, errs []error)

Execute executes the program embodied by these constraints in chunks of n steps at a time, producing any outputs arising. Execution is faster than trace because it does not record any internal information about the trace --- it simply extracts the outputs at the end.

func (*BinaryFile[F]) Field 

func (p *BinaryFile[F]) Field() field.Config

Field returns the field configuration for which this binary file is compiled. The primary purpose of this is to allow sanity check that the fields match between the client and what is embedded in this file.

func (*BinaryFile[F]) Header 

func (p *BinaryFile[F]) Header() Header

Header returns the binary file header, which contains the file version and optional metadata.

func (*BinaryFile[F]) LimbsMap 

func (p *BinaryFile[F]) LimbsMap() module.LimbsMap

LimbsMap provides a mapping from top-level registers to register limbs. This is useful to understand the mapping before / after register splitting.

func (*BinaryFile[F]) MarshalBinary 

func (p *BinaryFile[F]) MarshalBinary() ([]byte, error)

MarshalBinary converts the BinaryFile into a sequence of bytes.

func (*BinaryFile[F]) MaxStaticDepth added in v1.2.21 

func (p *BinaryFile[F]) MaxStaticDepth() uint

MaxStaticDepth records the maximum depth (i.e. number of rows) of static tables used when this binary was compiled. It must be carried in the file so that constraints regenerated from it match those produced at compile time (the range constraints baked into the machine depend on this value).

func (*BinaryFile[F]) Program added in v1.2.21 

func (p *BinaryFile[F]) Program() vm.Program[vm.Uint]

Program returns the bytecode program encoded in this file.

func (*BinaryFile[F]) Trace 

func (p *BinaryFile[F]) Trace(input map[string][]byte, cfg TraceConfig,
) (output map[string][]byte, rtr rtrace.Trace[F], tr trace.Trace[F], errs []error)

Trace generates a suitable trace from the given inputs for the contraints embodied in this file. Inputs are given as byte arrays which are decoded via vm.DecodeInputs() based on the register types of the corresponding memory. This can return one (or more) errors if, for example, the input is malformed (e.g. is missing expected fields and/or contains unexpected fields). The raw (row-major) trace produced by the machine is also returned, since it carries the original register / limb structure before AIR expansion (e.g. for reporting statistics). It is nil when execution fails.

func (*BinaryFile[F]) UnmarshalBinary 

func (p *BinaryFile[F]) UnmarshalBinary(data []byte) error

UnmarshalBinary initialises this BinaryFile from a given set of data bytes. This should match exactly the encoding above.

type Element added in v1.2.21 

type Element[F any] = field.Element[F]

Element provides a useful alias

type Expr 

type Expr[F field.Element[F]] = mirc.MirExpr[F]

Expr is a useful alias for an MIR expression

func TranslateBranchCondition added in v1.2.22 

func TranslateBranchCondition[W vm.Word[W], F field.Element[F], E Expr[F]](p dfa.Path[W],
	reader RegisterReader[F]) Expr[F]

TranslateBranchCondition translates a given branch condition within the context of a given state reader.

func TranslateNegatedBranchCondition added in v1.2.22 

func TranslateNegatedBranchCondition[W vm.Word[W], F field.Element[F], E Expr[F]](p dfa.Path[W],
	reader RegisterReader[F]) Expr[F]

TranslateNegatedBranchCondition translates a negated branch condition within the context of a given state reader.

type Framing 

type Framing[F field.Element[F]] = mirc.Framing[register.Id, Expr[F]]

Framing is a useful alias 

type Header struct {
	// Identifier is the 8-byte magic constant "zkbinary" that marks the file type.
	Identifier [8]byte
	// MajorVersion must match BINFILE_MAJOR_VERSION exactly for the file to be
	// considered compatible.
	MajorVersion uint16
	// MinorVersion must be ≤ BINFILE_MINOR_VERSION for the file to be
	// considered compatible (older minor versions remain readable).
	MinorVersion uint16
	// MetaData is an optional JSON blob carrying key/value pairs (e.g. the
	// source file path, compiler version, or build timestamp).
	MetaData []byte
}

Header is the fixed-layout prefix of every binary file. It is serialised using a hand-rolled big-endian encoding (not gob) so that the magic identifier and version numbers can be read without a full decode.

func (*Header) GetMetaData 

func (p *Header) GetMetaData() (typed.Map, error)

GetMetaData attempts to parse the metadata bytes as JSON which is then unmarshalled into a map. This can fail if the embedded metadata bytes are not, in fact, JSON. Observe that, if there are no metadata bytes, then nil will be returned.

func (*Header) IsCompatible 

func (p *Header) IsCompatible() bool

IsCompatible reports whether this header can be decoded by the current version of go-corset. Compatibility requires the "zkbinary" magic identifier, an exact match on the major version, and a minor version no greater than the current minor version.

func (*Header) MarshalBinary 

func (p *Header) MarshalBinary() ([]byte, error)

MarshalBinary converts the BinaryFile Header into a sequence of bytes. Observe that we don't use GobEncoding here to avoid being tied to that encoding scheme.

func (*Header) SetMetaData 

func (p *Header) SetMetaData(metadata typed.Map) error

SetMetaData attempts to set the metadata bytes for this header, using a JSON encoding of the given map. If this fails, an error is returned and the metadata bytes are unaffected.

func (*Header) UnmarshalBinary 

func (p *Header) UnmarshalBinary(buffer *bytes.Buffer) error

UnmarshalBinary initialises this BinaryFile Header from a given set of data bytes. This should match exactly the encoding above.

type InstructionTranslator 

type InstructionTranslator[W vm.Word[W], F field.Element[F]] struct {
	// contains filtered or unexported fields
}

InstructionTranslator encapsulates key information for translating an individual instruction (e.g. an assignment) into constraints.

func (*InstructionTranslator[W, F]) ReadRegister 

func (p *InstructionTranslator[W, F]) ReadRegister(rid vm.RegisterId) Expr[F]

ReadRegister reads a given register whilst applying forwarding as needed depending on the given writes set.

func (*InstructionTranslator[W, F]) WriteAndShiftRegisters 

func (p *InstructionTranslator[W, F]) WriteAndShiftRegisters(targets ...vm.RegisterId) []Expr[F]

WriteAndShiftRegisters constructs suitable accessors for the those registers written by a given microinstruction, and also shifts them (i.e. so they can be combined in a sum). This activates forwarding for those registers for all states after this, and returns suitable expressions for the assignment.

type Memory added in v1.2.21 

type Memory[W Word[W]] = vm.RuntimeMemory[W]

Memory provides a useful alias

type Module 

type Module[F field.Element[F]] = mirc.MirModule[F]

Module is a useful alias for an MIR module.

type Monomial added in v1.2.21 

type Monomial = poly.Monomial[register.Id]

Monomial is a convenient alias

type Polynomial added in v1.2.21 

type Polynomial = *poly.ArrayPoly[register.Id]

Polynomial defines the type of polynomials over which packets (and register splitting in general) operate.

type RegisterReader 

type RegisterReader[F field.Element[F]] = mirc.RegisterReader[Expr[F]]

RegisterReader is a conenvient alias

type TraceConfig 

type TraceConfig struct {
	// contains filtered or unexported fields
}

TraceConfig provides the necessary configuration for the trace generation.

func (TraceConfig) BatchSize 

func (tb TraceConfig) BatchSize() uint

BatchSize returns the configured batch size for this builder.

func (TraceConfig) PaddingStrategy added in v1.2.21 

func (tb TraceConfig) PaddingStrategy() ir.PaddingStrategy

PaddingStrategy returns the padding strategy configured for this builder.

func (TraceConfig) Parallelism 

func (tb TraceConfig) Parallelism() bool

Parallelism checks whether parallelism is enabled for this builder.

func (TraceConfig) WithBatchSize 

func (tb TraceConfig) WithBatchSize(batchSize uint) TraceConfig

WithBatchSize sets the maximum number of batches to run in parallel during trace expansion.

func (TraceConfig) WithPadding added in v1.2.21 

func (tb TraceConfig) WithPadding(strategy ir.PaddingStrategy) TraceConfig

WithPadding updates a given builder configuration to control how much front padding is added to the generated trace (see ir.PaddingStrategy).

func (TraceConfig) WithParallelism 

func (tb TraceConfig) WithParallelism(flag bool) TraceConfig

WithParallelism updates a given builder configuration to allow trace expansion to be performed concurrently (or not).

func (TraceConfig) WithValidation 

func (tb TraceConfig) WithValidation(flag bool) TraceConfig

WithValidation updates a given builder configuration to perform trace validation (or not).

type VectorInsnTranslator 

type VectorInsnTranslator[W vm.Word[W], F field.Element[F]] struct {
	// contains filtered or unexported fields
}

VectorInsnTranslator encapsulates general information related to the mapping from a bytecode vector into to MIR constraints.

func NewVectorTranslator 

func NewVectorTranslator[W vm.Word[W], F field.Element[F]](ctx schema.ModuleId, pc uint,
	vec vm.BytecodeVector[W], framing Framing[F], enclosing *vm.Function[W]) VectorInsnTranslator[W, F]

NewVectorTranslator constructs a translator for a specific bytecode vector.

func (*VectorInsnTranslator[W, F]) ReadRegister 

func (p *VectorInsnTranslator[W, F]) ReadRegister(regId register.Id, forwarding bool) Expr[F]

ReadRegister constructs a suitable accessor for referring to a given register. This applies forwarding as appropriate.

func (*VectorInsnTranslator[W, F]) Register 

func (p *VectorInsnTranslator[W, F]) Register(reg register.Id) register.Register

Register implementation for RegisterReader interface

func (*VectorInsnTranslator[W, F]) RegisterWidths 

func (p *VectorInsnTranslator[W, F]) RegisterWidths(regs ...io.RegisterId) []uint

RegisterWidths implementation for RegisterReader interface

func (*VectorInsnTranslator[W, F]) WithConstancyConstraints 

func (p *VectorInsnTranslator[W, F]) WithConstancyConstraints(writes dfa.Writes, condition Expr[F]) Expr[F]

WithConstancyConstraints adds constancy constraints for all registers which are either not mutated at all by a bytecode, or are sometimes mutated by a bytecode. Constancy constraints are required when the value of a register should be copied from the previous state into this state (i.e. because it was not changed by this bytecode and, hence, must retain its original value).

A key challenge lies with registers that are sometimes assigned by the bytecode, and sometimes not assigned (i.e. maybe but not definitely assigned). To resolve this we first determine the conditions under which they are assigned, and negate this to determine the conditions under which they are not assigned.

NOTE: it is possible to further optimise this process by taking into account which registers are actually used (i.e. live) after this instruction.

type Word added in v1.2.21 

type Word[W any] = vm.Word[W]

Word provides a useful alias

Source Files

View all Source files

Directories

Path Synopsis

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.