air

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

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

This section is empty.

Types

type Add 

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

Add represents the addition of zero or more AIR expressio

type Air 

type Air[F field.Element[F], C ConstraintBound[F]] struct {
	// contains filtered or unexported fields
}

Air attempts to encapsulate the notion of a valid constraint at the AIR 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 Air level.

func (Air[F, C]) Accepts 

func (p Air[F, C]) 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 (Air[F, C]) Air 

func (p Air[F, C]) Air()

Air marks the constraint as being valid for the AIR representation.

func (Air[F, C]) Bounds 

func (p Air[F, C]) 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 (Air[F, C]) Complexity 

func (p Air[F, C]) Complexity() uint

Complexity implementation for constraint interface

func (Air[F, C]) Consistent 

func (p Air[F, C]) 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 (Air[F, C]) Contexts 

func (p Air[F, C]) 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 (Air[F, C]) Lisp 

func (p Air[F, C]) 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 (Air[F, C]) Name 

func (p Air[F, C]) 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 (Air[F, C]) Substitute 

func (p Air[F, C]) Substitute(map[string]F)

Substitute any matchined labelled constants within this constraint

func (Air[F, C]) Unwrap 

func (p Air[F, C]) Unwrap() C

Unwrap provides access to the underlying constraint.

type Assertion 

type Assertion[F field.Element[F]] = Air[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.

func NewAssertion 

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

NewAssertion constructs a new AIR assertion

type ColumnAccess 

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

ColumnAccess 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 Constant 

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

Constant represents a constant value within AIR an expression.

type Constraint 

type Constraint[F field.Element[F]] interface {
	schema.Constraint[F]
	// Air marks the constraints as been valid for the AIR representation.
	Air()
}

Constraint captures the essence of a constraint at the AIR level.

func NewInterleavingConstraint 

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

NewInterleavingConstraint creates a new interleaving 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

type ConstraintBound 

type ConstraintBound[F field.Element[F]] interface {
	schema.Constraint[F]

	constraint.Assertion[F] |
		interleaving.Constraint[F, *ColumnAccess[F]] |
		lookup.Constraint[F, *ColumnAccess[F]] |
		permutation.Constraint[F] |
		ranged.Constraint[F, *ColumnAccess[F]] |
		vanishing.Constraint[F, LogicalTerm[F]]
}

ConstraintBound limits the permitted set of underlying constraints. This should never change, unless the underlying prover changes in some way to offer different or more fundamental primitives.

type InterleavingConstraint 

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

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

type LogicalTerm 

type LogicalTerm[F field.Element[F]] struct {
	Term Term[F]
}

LogicalTerm provides a wrapper around a given term allowing to be "testable". That is, it provides a default TestAt implementation.

func (LogicalTerm[F]) Bounds 

func (p LogicalTerm[F]) Bounds() util.Bounds

Bounds implementation for Boundable interface.

func (LogicalTerm[F]) Lisp 

func (p LogicalTerm[F]) Lisp(global bool, mapping register.Map) sexp.SExp

Lisp returns a lisp representation of this NotEqual, which is useful for debugging.

func (LogicalTerm[F]) RequiredCells 

func (p LogicalTerm[F]) RequiredCells(row int, mid trace.ModuleId) *set.AnySortedSet[trace.CellRef]

RequiredCells implementation for Contextual interface

func (LogicalTerm[F]) RequiredRegisters 

func (p LogicalTerm[F]) RequiredRegisters() *set.SortedSet[uint]

RequiredRegisters implementation for Contextual interface.

func (LogicalTerm[F]) Substitute 

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

Substitute implementation for Substitutable interface.

func (LogicalTerm[F]) TestAt 

func (p LogicalTerm[F]) TestAt(k int, tr trace.Module[F], sc register.Map) (bool, uint, error)

TestAt implementation for Testable interface.

type LookupConstraint 

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

LookupConstraint captures the essence of a lookup constraint at the AIR level. At the AIR level, lookup constraints are only permitted between columns (i.e. not arbitrary expressions).

func NewLookupConstraint 

func NewLookupConstraint[F field.Element[F]](handle string, targets []lookup.Vector[F, *ColumnAccess[F]],
	sources []lookup.Vector[F, *ColumnAccess[F]]) LookupConstraint[F]

NewLookupConstraint constructs a new AIR lookup constraint

type Module 

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

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

type ModuleBuilder 

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

ModuleBuilder is used for building various AIR modules.

type Mul 

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

Mul represents the product over zero or more expressions.

type PermutationConstraint 

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

PermutationConstraint captures the essence of a permutation constraint at the AIR level. Specifically, it represents a constraint that one (or more) columns are a permutation of another.

type RangeConstraint 

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

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

func NewRangeConstraint 

func NewRangeConstraint[F field.Element[F]](handle string, ctx schema.ModuleId, exprs []*ColumnAccess[F],
	bitwidths []uint) RangeConstraint[F]

NewRangeConstraint constructs a new AIR range constraint

type Schema 

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

Schema captures the essence of an arithmetisation at the AIR level. Specifically, it is limited to only those constraint forms permitted at the AIR level.

type SchemaBuilder 

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

SchemaBuilder is used for building the AIR schemas

type Sub 

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

Sub represents the subtraction over zero or more expressions.

type Term 

type Term[F field.Element[F]] interface {
	term.Expr[F, Term[F]]
	// Air marks terms which are valid for the AIR representation.
	Air()
}

Term represents the fundamental for arithmetic expressions in the AIR representation. This should only support addition, subtraction and multiplication of constants and column accesses. No other terms are permitted at this, the lowest, layer of the stack.

type VanishingConstraint 

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

VanishingConstraint captures the essence of a vanishing constraint at the AIR level.

func NewVanishingConstraint 

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

NewVanishingConstraint constructs a new AIR vanishing constraint

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.