hir

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

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func DisjunctIfTerms 

func DisjunctIfTerms(fn BinaryLogicalFn, lhs, rhs IfTerm) mir.LogicalTerm[word.BigEndian]

DisjunctIfTerms is similar to MapIfTerms but produces the logical disjunction of all constructed logical terms.

func LowerToMir 

func LowerToMir[E register.ConstMap](externs []E, modules []Module) []mir.Module[word.BigEndian]

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

func SubstituteConstants 

func SubstituteConstants(schema schema.AnySchema[word.BigEndian], mapping map[string]word.BigEndian)

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

Types

type Add 

type Add = term.Add[word.BigEndian, Term]

Add represents the addition of zero or more expressions.

type Assertion 

type Assertion = constraint.Assertion[word.BigEndian]

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 BinaryLogicalFn 

type BinaryLogicalFn func(l, r mirTerm) mir.LogicalTerm[word.BigEndian]

BinaryLogicalFn describes a function whichs a logical MIR term from exactly two terms.

type Cast 

type Cast = term.Cast[word.BigEndian, Term]

Cast attempts to narrow the width a given expression.

type Conjunct 

type Conjunct = term.Conjunct[word.BigEndian, LogicalTerm]

Conjunct represents a logical conjunction at the HIR level.

type Constant 

type Constant = term.Constant[word.BigEndian, Term]

Constant represents a constant value within an expression.

type Constraint 

type Constraint 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 level.

func NewAssertion 

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

NewAssertion constructs a new assertion

func NewFunctionCall 

func NewFunctionCall(handle string, caller, callee module.Id,
	returns []Term, args []Term, selector util.Option[LogicalTerm]) Constraint

NewFunctionCall creates a new function call with a given handle

func NewInterleavingConstraint 

func NewInterleavingConstraint(handle string, targetContext schema.ModuleId,
	sourceContext schema.ModuleId, target Term, sources []Term) Constraint

NewInterleavingConstraint creates a new interleaving constraint with a given handle.

func NewLookupConstraint 

func NewLookupConstraint(handle string, targets []lookup.Vector[word.BigEndian, Term],
	sources []lookup.Vector[word.BigEndian, Term]) Constraint

NewLookupConstraint creates a new lookup constraint with a given handle.

func NewPermutationConstraint 

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

NewPermutationConstraint creates a new permutation

func NewRangeConstraint 

func NewRangeConstraint(handle string, ctx schema.ModuleId, expr Term,
	bitwidth uint) Constraint

NewRangeConstraint constructs a new Range constraint

func NewSortedConstraint 

func NewSortedConstraint(handle string, context schema.ModuleId, bitwidth uint,
	selector util.Option[Term], sources []Term, signs []bool, strict bool) Constraint

NewSortedConstraint creates a new Sorted

func NewVanishingConstraint 

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

NewVanishingConstraint constructs a new vanishing constraint

func (Constraint) Accepts 

func (p Constraint) Accepts(trace trace.Trace[word.BigEndian],
	schema schema.AnySchema[word.BigEndian]) (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) Bounds 

func (p Constraint) 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) Complexity 

func (p Constraint) Complexity() uint

Complexity implementation for constraint interface

func (Constraint) Consistent 

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

func (p Constraint) 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) GobDecode 

func (p *Constraint) GobDecode(data []byte) error

GobDecode a previously encoded option

func (Constraint) GobEncode 

func (p Constraint) GobEncode() (data []byte, err error)

GobEncode an option. This allows it to be marshalled into a binary form.

func (Constraint) Lisp 

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

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

func (Constraint) Name 

func (p Constraint) 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) Substitute 

func (p Constraint) Substitute(mapping map[string]word.BigEndian)

Substitute any matchined labelled constants within this constraint

func (Constraint) Unwrap 

func (p Constraint) Unwrap() schema.Constraint[word.BigEndian]

Unwrap provides access to the underlying constraint.

type Disjunct 

type Disjunct = term.Disjunct[word.BigEndian, LogicalTerm]

Disjunct represents a logical conjunction at the HIR level.

type Equal 

type Equal = term.Equal[word.BigEndian, LogicalTerm, Term]

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

type Exp 

type Exp = term.Exp[word.BigEndian, Term]

Exp represents the a given value taken to a power.

type Expr 

type Expr[T any] = term.Expr[word.BigEndian, T]

Expr provides a convenient shorthand

type FunctionCall 

type FunctionCall struct {
	Handle         string
	Callee, Caller module.Id
	Returns        []Term
	Arguments      []Term
	Selector       util.Option[LogicalTerm]
}

FunctionCall represents a special kind of lookup constraint which triggers trace propagation.

func (FunctionCall) Accepts 

func (p FunctionCall) Accepts(_ trace.Trace[word.BigEndian], _ schema.AnySchema[word.BigEndian],
) (bit.Set, schema.Failure)

Accepts checks whether a lookup constraint into the target columns holds for all rows of the source columns.

func (FunctionCall) Bounds 

func (p FunctionCall) Bounds(module uint) util.Bounds

Bounds determines the well-definedness bounds for this constraint for 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 (FunctionCall) Complexity 

func (p FunctionCall) Complexity() uint

Complexity implementation for constraint interface

func (FunctionCall) Consistent 

func (p FunctionCall) Consistent(schema schema.AnySchema[word.BigEndian]) []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 (FunctionCall) Contexts 

func (p FunctionCall) 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 (FunctionCall) Lisp 

func (p FunctionCall) Lisp(mapping schema.AnySchema[word.BigEndian]) sexp.SExp

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

func (FunctionCall) Name 

func (p FunctionCall) Name() string

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

func (FunctionCall) Substitute 

func (p FunctionCall) Substitute(mapping map[string]word.BigEndian)

Substitute any matchined labelled constants within this constraint

type IfTerm 

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

IfTerm represents a set of one or more conditional terms. Observe that the conditions are expected to be total. Hence, if there is only one term, then its condition must be true.

func IfEqElse 

func IfEqElse(lhs IfTerm, rhs mirTerm, tt, ff mirTerm) IfTerm

IfEqElse constructs an IfTerm representing an if-eq expression.

func IfThenElse 

func IfThenElse(cond mir.LogicalTerm[word.BigEndian], tt, ff IfTerm) IfTerm

IfThenElse constructs an IfTerm representing an if-then else expression.

func MapIfTerms 

func MapIfTerms(fn NaryFn, terms ...IfTerm) IfTerm

MapIfTerms applies a given function to each target of the given argument terms, effectively producing their cross product.

func UnconditionalTerm 

func UnconditionalTerm(value mirTerm) IfTerm

UnconditionalTerm returns a term which has no condition associated with it.

func (*IfTerm) Equate 

func (p *IfTerm) Equate(target register.Id, bitwidth uint) mir.LogicalTerm[word.BigEndian]

Equate returns a logical condition that constraints the target register to hold the values represented by this term on each row.

func (*IfTerm) Map 

func (p *IfTerm) Map(fn func(mirTerm) mirTerm) IfTerm

Map a given function over the targets of this set of conditional terms.

type IfZero 

type IfZero = term.IfZero[word.BigEndian, LogicalTerm, Term]

IfZero represents a conditional branch at the HIR level.

type InterleavingConstraint 

type InterleavingConstraint = interleaving.Constraint[word.BigEndian, Term]

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

type Ite 

type Ite = term.Ite[word.BigEndian, LogicalTerm]

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

type LabelledConst 

type LabelledConst = term.LabelledConst[word.BigEndian, Term]

LabelledConst represents a labelled constant at the HIR level.

type Logical 

type Logical[T any] = term.Logical[word.BigEndian, T]

Logical provides a convenient shorthand

type LogicalTerm 

type LogicalTerm interface {
	term.Logical[word.BigEndian, LogicalTerm]
}

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

type LookupConstraint 

type LookupConstraint = lookup.Constraint[word.BigEndian, Term]

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

type MirLowering 

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

MirLowering captures all auxiliary state required in the process of lowering modules from HIR to MIR. 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 NewMirLowering 

func NewMirLowering[E register.ConstMap](externs []E, modules []Module) MirLowering

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

func (*MirLowering) Lower 

func (p *MirLowering) Lower() []mir.Module[word.BigEndian]

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

type Module 

type Module = *schema.Table[word.BigEndian, Constraint]

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

type Mul 

type Mul = term.Mul[word.BigEndian, Term]

Mul represents the product over zero or more expressions.

type NaryFn 

type NaryFn func([]mirTerm) mirTerm

NaryFn describes a function which constructs an MIR term from a given set of zero or more terms.

type Negate 

type Negate = term.Negate[word.BigEndian, LogicalTerm]

Negate represents a logical negation at the HIR level.

type Norm 

type Norm = term.Norm[word.BigEndian, Term]

Norm reduces the value of an expression to either zero (if it was zero) or one (otherwise).

type NotEqual 

type NotEqual = term.NotEqual[word.BigEndian, LogicalTerm, Term]

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

type PermutationConstraint 

type PermutationConstraint = permutation.Constraint[word.BigEndian]

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

type RangeConstraint 

type RangeConstraint = ranged.Constraint[word.BigEndian, Term]

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

type RegisterAccess 

type RegisterAccess = term.RegisterAccess[word.BigEndian, Term]

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 = schema.UniformSchema[word.BigEndian, Module]

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

type SortedConstraint 

type SortedConstraint = sorted.Constraint[word.BigEndian, Term]

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

type Sub 

type Sub = term.Sub[word.BigEndian, Term]

Sub represents the subtraction over zero or more expressions.

type Term 

type Term interface {
	term.Expr[word.BigEndian, Term]
}

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

type VanishingConstraint 

type VanishingConstraint = vanishing.Constraint[word.BigEndian, LogicalTerm]

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

type VectorAccess 

type VectorAccess = term.VectorAccess[word.BigEndian, Term]

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.