mir

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: 30 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

This section is empty.

Variables

View Source 
var DEFAULT_OPTIMISATION_INDEX = uint(1)

DEFAULT_OPTIMISATION_INDEX gives the index of the default optimisation level in OPTIMISATION_LEVELS.

View Source 
var DEFAULT_OPTIMISATION_LEVEL = OPTIMISATION_LEVELS[DEFAULT_OPTIMISATION_INDEX]

DEFAULT_OPTIMISATION_LEVEL provides a default level of optimisation which should be used in most cases.

View Source 
var EXPLODING_MULTIPLIER = uint(10)

EXPLODING_MULTIPLIER determines the multipler to use for logging "exploding" constraints. This is essentially an aid to debugging.

View Source 
var OPTIMISATION_LEVELS = []OptimisationConfig{

	{0, 16, false},

	{1, 16, true},
}

OPTIMISATION_LEVELS provides a set of precanned optimisation configurations. Here 0 implies no optimisation and, otherwise, increasing levels implies increasingly aggressive optimisation (though that doesn't mean they will always improve performance).

Functions

func InitialiseConstantRegisters 

func InitialiseConstantRegisters[F Element[F]](offset uint, modules []Module[F])

InitialiseConstantRegisters initialises any constant registers declared within the given set of MIR modules. At this time, the only form of a constant register is the so-called "zero register" (i.e. the register which is always zero). At the moment, these are implemented manually using constraints and assignments to fill them. Eventually, this approach should be deprecated in favour of direct prover support.

func LowerToAir 

func LowerToAir[F field.Element[F]](schema Schema[F], fieldBandwith uint, config OptimisationConfig) air.Schema[F]

LowerToAir lowers (or refines) an MIR schema into an AIR schema. That means lowering all the columns and constraints, whilst adding additional columns / constraints as necessary to preserve the original semantics.

func SubdivideRegisterRefs 

func SubdivideRegisterRefs[F field.Element[F]](mapping module.LimbsMap, refs ...register.Refs) []register.Refs

SubdivideRegisterRefs subdivides a set of register references according to a given mapping.

func SubstituteConstants 

func SubstituteConstants[F field.Element[F]](schema schema.AnySchema[F], mapping map[string]F)

SubstituteConstants substitutes the value of matching labelled constants for all expressions used within the schema.

Types

type Add 

type Add[F field.Element[F]] = term.Add[F, Term[F]]

Add represents the addition of zero or more expressions.

type AirLowering 

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

AirLowering captures all auxiliary state required in the process of lowering modules from MIR to AIR. This state is because, as part of the lowering process, we may introduce some number of additional modules (e.g. for managing type proofs).

func NewAirLowering 

func NewAirLowering[F field.Element[F]](fieldBandwidth uint, mirSchema Schema[F]) AirLowering[F]

NewAirLowering constructs an initial state for lowering a given MIR schema.

func (*AirLowering[F]) ConfigureOptimisation 

func (p *AirLowering[F]) ConfigureOptimisation(config OptimisationConfig)

ConfigureOptimisation configures the amount of optimisation to apply during the lowering process.

func (*AirLowering[F]) InitialiseModule 

func (p *AirLowering[F]) InitialiseModule(index uint)

InitialiseModule simply initialises all registers within the module, but does not lower any constraint or assignments.

func (*AirLowering[F]) Lower 

func (p *AirLowering[F]) Lower() air.Schema[F]

Lower the MIR schema provide when this lowering instance was created into an equivalent AIR schema.

func (*AirLowering[F]) LowerModule 

func (p *AirLowering[F]) LowerModule(index uint)

LowerModule lowers the given MIR module into the corresponding AIR module. This includes all constraints and assignments.

type Assertion 

type Assertion[F field.Element[F]] = constraint.Assertion[F]

Assertion captures the notion of an arbitrary property which should hold for all acceptable traces. However, such a property is not enforced by the prover.

type Computation 

type Computation = term.Computation[word.BigEndian]

Computation captures the notion of computations used in a small number of places.

type Conjunct 

type Conjunct[F field.Element[F]] = term.Conjunct[F, LogicalTerm[F]]

Conjunct represents a logical conjunction at the MIR level.

type Constant 

type Constant[F field.Element[F]] = term.Constant[F, Term[F]]

Constant represents a constant value within an expression.

type Constraint 

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

Constraint attempts to encapsulate the notion of a valid constraint at the MIR level. Since this is the fundamental level, only certain constraint forms are permitted. As such, we want to try and ensure that arbitrary constraints are not found at the Constraint[F] level.

func NewAssertion 

func NewAssertion[F field.Element[F]](handle string, ctx schema.ModuleId, domain util.Option[int],
	term constraint.Property) Constraint[F]

NewAssertion constructs a new assertion

func NewInterleavingConstraint 

func NewInterleavingConstraint[F field.Element[F]](handle string, targetContext schema.ModuleId,
	sourceContext schema.ModuleId, target *VectorAccess[F], sources []*VectorAccess[F]) Constraint[F]

NewInterleavingConstraint creates a new interleaving constraint with a given handle.

func NewLookupConstraint 

func NewLookupConstraint[F field.Element[F]](handle string, targets []LookupVector[F],
	sources []LookupVector[F]) Constraint[F]

NewLookupConstraint creates a new lookup constraint with a given handle.

func NewPermutationConstraint 

func NewPermutationConstraint[F field.Element[F]](handle string, context schema.ModuleId, targets []register.Id,
	sources []register.Id) Constraint[F]

NewPermutationConstraint creates a new permutation

func NewRangeConstraint 

func NewRangeConstraint[F field.Element[F]](handle string, ctx schema.ModuleId, registers []*RegisterAccess[F],
	bitwidths []uint) Constraint[F]

NewRangeConstraint constructs a new Range constraint

func NewSortedConstraint 

func NewSortedConstraint[F field.Element[F]](handle string, context schema.ModuleId, bitwidth uint,
	selector util.Option[*RegisterAccess[F]], sources []*RegisterAccess[F], signs []bool, strict bool) Constraint[F]

NewSortedConstraint creates a new Sorted

func NewVanishingConstraint 

func NewVanishingConstraint[F field.Element[F]](handle string, ctx schema.ModuleId, domain util.Option[int],
	term LogicalTerm[F]) Constraint[F]

NewVanishingConstraint constructs a new vanishing constraint

func (Constraint[F]) Accepts 

func (p Constraint[F]) Accepts(trace trace.Trace[F],
	schema schema.AnySchema[F]) (bit.Set, schema.Failure)

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 (Constraint[F]) Bounds 

func (p Constraint[F]) Bounds(module uint) util.Bounds

Bounds determines 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 first row of any trace and, by association, any constraint evaluating this expression on that first row is also undefined (and hence must pass)

func (Constraint[F]) Complexity 

func (p Constraint[F]) Complexity() uint

Complexity implementation for constraint interface

func (Constraint[F]) Consistent 

func (p Constraint[F]) Consistent(schema schema.AnySchema[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.

func (Constraint[F]) Contexts 

func (p Constraint[F]) Contexts() []schema.ModuleId

Contexts returns the evaluation contexts (i.e. enclosing module + length multiplier) for this constraint. Most constraints have only a single evaluation context, though some (e.g. lookups) have more. Note that all constraints have at least one context (which we can call the "primary" context).

func (Constraint[F]) Lisp 

func (p Constraint[F]) Lisp(schema schema.AnySchema[F]) sexp.SExp

Lisp converts this schema element into a simple S-Expression, for example so it can be printed.

func (Constraint[F]) Name 

func (p Constraint[F]) Name() string

Name returns a unique name and case number for a given constraint. This is useful purely for identifying constraints in reports, etc.

func (Constraint[F]) Substitute 

func (p Constraint[F]) Substitute(mapping map[string]F)

Substitute any matchined labelled constants within this constraint

func (Constraint[F]) Unwrap 

func (p Constraint[F]) Unwrap() schema.Constraint[F]

Unwrap provides access to the underlying constraint.

type Disjunct 

type Disjunct[F field.Element[F]] = term.Disjunct[F, LogicalTerm[F]]

Disjunct represents a logical conjunction at the MIR level.

type Element 

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

Element provides a convenient shorthand.

type Equal 

type Equal[F field.Element[F]] = term.Equal[F, LogicalTerm[F], Term[F]]

Equal represents an equality comparator between two arithmetic terms at the MIR level.

type InterleavingConstraint 

type InterleavingConstraint[F field.Element[F]] = interleaving.Constraint[F, *VectorAccess[F]]

InterleavingConstraint captures the essence of an interleaving constraint at the MIR level.

type Ite 

type Ite[F field.Element[F]] = term.Ite[F, LogicalTerm[F]]

Ite represents an If-Then-Else expression where either branch is optional (though we must have at least one).

type LogicalComputation 

type LogicalComputation = term.LogicalComputation[word.BigEndian]

LogicalComputation captures the notion of computations used in a small number of places.

type LogicalTerm 

type LogicalTerm[F any] interface {
	term.Logical[F, LogicalTerm[F]]
}

LogicalTerm represents the fundamental for logical expressions in the MIR representation.

type LookupConstraint 

type LookupConstraint[F field.Element[F]] = lookup.Constraint[F, *RegisterAccess[F]]

LookupConstraint captures the essence of a lookup constraint at the MIR level.

type LookupVector 

type LookupVector[F field.Element[F]] = lookup.Vector[F, *RegisterAccess[F]]

LookupVector provides a convenient shorthand

type Module 

type Module[F field.Element[F]] = *schema.Table[F, Constraint[F]]

Module captures the essence of a module at the MIR level. Specifically, it is limited to only those constraint forms permitted at the MIR level.

func Concretize 

func Concretize[F1 Element[F1], F2 Element[F2], E register.ConstMap](mapping module.LimbsMap, externs []E,
	mods []Module[F1]) []Module[F2]

Concretize converts an MIR schema for a given field F1 into an MIR schema for another field F2. This is awkward as we have to rebuild the entire Intermediate Representation in order to match the type appropriately. In doing this, we take some opportunities to simplify, such as removing labelled constants (which no longer make sense). Furthermore, this stage can technically fail if the relevant constraints cannot be correctly concretized. For example, they contain a constant which does not fit within the field.

func Subdivide 

func Subdivide[F field.Element[F], E register.ConstMap](mapping module.LimbsMap, externs []E,
	mods []Module[F]) []Module[F]

Subdivide all modules to meet a given bandwidth and maximum register width. This will split all registers wider than the maximum permitted width into two or more "limbs" (i.e. subregisters which do not exceeded the permitted width). For example, consider a register "r" of width u32. Subdividing this register into registers of at most 8bits will result in four limbs: r'0, r'1, r'2 and r'3 where (by convention) r'0 is the least significant.

As part of the subdivision process, constraints may also need to be divided when they exceed the maximum permitted bandwidth. For example, consider a simple constraint such as "x = y + 1" using 16bit registers x,y. Subdividing for a bandwidth of 10bits and a maximum register width of 8bits means splitting each register into two limbs, and transforming our constraint into:

256*x'1 + x'0 = 256*y'1 + y'0 + 1

However, as it stands, this constraint exceeds our bandwidth requirement since it requires at least 17bits of information to safely evaluate each side. Thus, the constraint itself must be subdivided into two parts:

256*c + x'0 = y'0 + 1 // lower 

x'1 = y'1 + c  // upper

Here, c is a 1bit register introduced as part of the transformation to act as a "carry" between the two constraints.

type ModuleBuilder 

type ModuleBuilder[F field.Element[F]] = ir.ModuleBuilder[F, Constraint[F], Term[F]]

ModuleBuilder is used for building various MIR modules.

type Mul 

type Mul[F field.Element[F]] = term.Mul[F, Term[F]]

Mul represents the product over zero or more expressions.

type Negate 

type Negate[F field.Element[F]] = term.Negate[F, LogicalTerm[F]]

Negate represents a logical negation at the MIR level.

type NotEqual 

type NotEqual[F field.Element[F]] = term.NotEqual[F, LogicalTerm[F], Term[F]]

NotEqual represents a non-equality comparator between two arithmetic terms at the MIR level.

type OptimisationConfig 

type OptimisationConfig struct {
	// InverseEliminationLevel sets an upper bound on the range cardinality at
	// which inverses will be eliminated in favour of constraints.  A level of 0
	// means no inverses will be eliminated, a range of 1 means only trivial
	// ranges (i.e. {-1,0}, {0,1} and {-1,0,1}) will be eliminated; Otherwise,
	// the level indicates the range cardinality.  For example, level 2 means
	// any range of cardinality 2 is eliminated (e.g. {1,2}, {5,6}, etc).
	InverseEliminiationLevel uint
	// MaxRangeConstraint determines the largest bitwidth for which range
	// constraints are translated into AIR range constraints, versus  using a
	// horizontal bitwidth gadget.
	MaxRangeConstraint uint
	// ShiftNormalisation is an optimisation for inverse columns involving
	// shifts.
	ShiftNormalisation bool
}

OptimisationConfig provides a mechanism for controlling how optimisations are applied during MIR lowering.

type PermutationConstraint 

type PermutationConstraint[F field.Element[F]] = permutation.Constraint[F]

PermutationConstraint captures the essence of a permutation constraint at the MIR level.

type Polynomial 

type Polynomial = agnostic.DynamicPolynomial

Polynomial provides a useful alias

type RangeConstraint 

type RangeConstraint[F field.Element[F]] = ranged.Constraint[F, *RegisterAccess[F]]

RangeConstraint captures the essence of a range constraints at the MIR level.

type RegisterAccess 

type RegisterAccess[F field.Element[F]] = term.RegisterAccess[F, Term[F]]

RegisterAccess represents reading the value held at a given column in the tabular context. Furthermore, the current row maybe shifted up (or down) by a given amount.

type Schema 

type Schema[F field.Element[F]] = schema.UniformSchema[F, Module[F]]

Schema captures the notion of an MIR schema which is uniform and consists of MIR modules only.

type SchemaBuilder 

type SchemaBuilder[F field.Element[F]] = ir.SchemaBuilder[F, Constraint[F], Term[F]]

SchemaBuilder is used for building the MIR schemas

type SortedConstraint 

type SortedConstraint[F field.Element[F]] = sorted.Constraint[F, *RegisterAccess[F]]

SortedConstraint captures the essence of a sorted constraint at the MIR level.

type Sub 

type Sub[F field.Element[F]] = term.Sub[F, Term[F]]

Sub represents the subtraction over zero or more expressions.

type Subdivider 

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

Subdivider is responsible for subdividing modules to ensure they fit within a given target field configuration (as determined by the mapping). More specificially, any registers used within (and constraints, etc) are subdivided as necessary to ensure a maximum bandwidth requirement is met. Here, bandwidth refers to the maximum number of data bits which can be stored in the underlying field. As a simple example, the prime field F_7 has a bandwidth of 2bits. To target a specific prime field, two parameters are used: the maximum bandwidth (as determined by the prime); the maximum register width (which should be smaller than the bandwidth). The maximum register width determines the maximum permitted width of any register after subdivision. Since every register value will be stored as a field element, it follows that the maximum width cannot be greater than the bandwidth. However, in practice, we want it to be marginally less than the bandwidth to ensure there is some capacity for calculations involving registers.

func (*Subdivider[F]) FlushAllocator 

func (p *Subdivider[F]) FlushAllocator(mid module.Id, alloc agnostic.RegisterAllocator)

FlushAllocator causes the given register allocator to crystalise any allocated registers into the corresponding module.

func (*Subdivider[F]) FreshAllocator 

func (p *Subdivider[F]) FreshAllocator(mid module.Id) agnostic.RegisterAllocator

FreshAllocator creates a fresh allocator for the given module.

func (*Subdivider[F]) SubdivideModule 

func (p *Subdivider[F]) SubdivideModule(mid module.Id, rawModule Module[F])

SubdivideModule subdivides all registers, constraints and assignments within a given module.

func (*Subdivider[F]) ZeroRegister 

func (p *Subdivider[F]) ZeroRegister(mid module.Id) register.Id

ZeroRegister returns a register in the given module whose value is always the constant zero.

type Term 

type Term[F any] interface {
	term.Expr[F, Term[F]]
}

Term represents the fundamental for arithmetic expressions in the MIR representation.

type VanishingConstraint 

type VanishingConstraint[F field.Element[F]] = vanishing.Constraint[F, LogicalTerm[F]]

VanishingConstraint captures the essence of a vanishing constraint at the MIR level. A vanishing constraint is a row constraint which must evaluate to zero.

type VectorAccess 

type VectorAccess[F field.Element[F]] = term.VectorAccess[F, Term[F]]

VectorAccess represents a compound variable

Source Files

View all Source files

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.