ast

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

View Source
const (
	// NOT_COMPUTED signals a column is not a computed column.
	NOT_COMPUTED = 0
	// COMPUTED signals a column is a (non-recursive) computed column.
	COMPUTED = 1
	// COMPUTED_FWD signals a column is a (forward recursive) computed column.
	// This means its value is computed starting from the first row (hence it
	// cannot use a forward shift in its declaration).
	COMPUTED_FWD = 2
	// COMPUTED_BWD signals a column is a (backward recursive) computed column.
	// This means its value is computed starting from the last row (hence it
	// cannot use a backward shift in its declaration).
	COMPUTED_BWD = 3
)
View Source
const (
	// EQUALS indicates an equals (==) relationship
	EQUALS uint8 = 0
	// NOT_EQUALS indicates a not-equals (!=) relationship
	NOT_EQUALS uint8 = 1
)

Variables

View Source
var BOOL_TYPE = &BoolType{}

BOOL_TYPE provides a convenient singleone to use instead of creating a fresh boolean type, etc.

View Source
var NON_FUNCTION util.Option[uint] = util.None[uint]()

NON_FUNCTION is used to signal a symbol which does not represent a function.

View Source
var UINT_TYPE = &IntType{math.INFINITY}

UINT_TYPE represents the infinite integer range. This cannot be translated into a concrete type at the lower level, and therefore can only be used internally (e.g. for type checking).

Functions

func AsConstantOfExpressions

func AsConstantOfExpressions(exprs []Expr, fn func(*big.Int, *big.Int)) *big.Int

AsConstantOfExpressions attempts to fold one or more expressions across a given operation (e.g. add, subtract, etc) to produce a constant value. If any of the expressions are not themselves constant, then neither is the result.

func ListOfExpressions

func ListOfExpressions[E Expr](head sexp.SExp, exprs []E) *sexp.List

ListOfExpressions converts an array of one or more expressions into a list of corresponding lisp expressions.

Types

type Add

type Add struct{ Args []Expr }

Add represents the sum over zero or more expressions.

func (*Add) AsConstant

func (e *Add) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Add) Context

func (e *Add) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Add) Dependencies

func (e *Add) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Add) Lisp

func (e *Add) Lisp() sexp.SExp

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

type AnyType

type AnyType struct{}

AnyType represents the top of the type lattice. This is the type into which values of any other type can flow.

func (*AnyType) HasUnderlying

func (p *AnyType) HasUnderlying() bool

HasUnderlying determines whether or not this type has an underlying representation, or not.

func (*AnyType) LeastUpperBound

func (p *AnyType) LeastUpperBound(other Type) Type

LeastUpperBound computes the least upper bound of this type and another. This is smallest type which contains both of the arguments. For example, i32 is the least upper bound of i1 and i32, etc. If no such type exists, then nil is returned.

func (*AnyType) String

func (p *AnyType) String() string

func (*AnyType) SubtypeOf

func (p *AnyType) SubtypeOf(other Type) bool

SubtypeOf determines whether or not this type is a subtype of another.

func (*AnyType) Width

func (p *AnyType) Width() uint

Width returns the number of underlying columns represented by this column. For example, an array of size n will expand into n underlying columns.

type ArrayAccess

type ArrayAccess struct {
	Name         file.Path
	Arg          Expr
	ArrayBinding Binding
}

ArrayAccess represents the a given value taken to a power.

func (*ArrayAccess) Arity

func (e *ArrayAccess) Arity() util.Option[uint]

Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.

func (*ArrayAccess) AsConstant

func (e *ArrayAccess) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*ArrayAccess) Binding

func (e *ArrayAccess) Binding() Binding

Binding gets binding associated with this interface. This will panic if this symbol is not yet resolved.

func (*ArrayAccess) Context

func (e *ArrayAccess) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*ArrayAccess) Dependencies

func (e *ArrayAccess) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*ArrayAccess) IsResolved

func (e *ArrayAccess) IsResolved() bool

IsResolved checks whether this symbol has been resolved already, or not.

func (*ArrayAccess) Lisp

func (e *ArrayAccess) Lisp() sexp.SExp

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

func (*ArrayAccess) Path

func (e *ArrayAccess) Path() *file.Path

Path returns the given path of this symbol.

func (*ArrayAccess) Resolve

func (e *ArrayAccess) Resolve(binding Binding) bool

Resolve this symbol by associating it with the binding associated with the definition of the symbol to which this refers.

func (*ArrayAccess) Type

func (e *ArrayAccess) Type() Type

Type returns the type associated with this symbol. If the type cannot be determined, then nil is returned.

type ArrayType

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

ArrayType represents a statically-sized array of types.

func NewArrayType

func NewArrayType(element Type, min uint, max uint) *ArrayType

NewArrayType constructs a new array type of a given (fixed) size.

func (*ArrayType) Element

func (p *ArrayType) Element() Type

Element returns the element of this array type.

func (*ArrayType) HasUnderlying

func (p *ArrayType) HasUnderlying() bool

HasUnderlying determines whether or not this type has an underlying representation, or not.

func (*ArrayType) LeastUpperBound

func (p *ArrayType) LeastUpperBound(other Type) Type

LeastUpperBound computes the least upper bound of this type and another. This is smallest type which contains both of the arguments. For example, i32 is the least upper bound of i1 and i32, etc. If no such type exists, then nil is returned.

func (*ArrayType) MaxIndex

func (p *ArrayType) MaxIndex() uint

MaxIndex returns the largest index of elements in this array type.

func (*ArrayType) MinIndex

func (p *ArrayType) MinIndex() uint

MinIndex returns the smallest index of elements in this array type.

func (*ArrayType) String

func (p *ArrayType) String() string

func (*ArrayType) SubtypeOf

func (p *ArrayType) SubtypeOf(other Type) bool

SubtypeOf determines whether or not this type is a subtype of another.

func (*ArrayType) Width

func (p *ArrayType) Width() uint

Width returns the number of underlying columns represented by this column. For example, an array of size n will expand into n underlying columns.

type Binding

type Binding interface {
	// Determine whether this binding is finalised or not.
	IsFinalised() bool
	// Determine whether this binding can be defined recursively or not.
	IsRecursive() bool
}

Binding represents an association between a name, as found in a source file, and concrete item (e.g. a column, function, etc).

type BoolType

type BoolType struct {
}

BoolType represents the type of logical conditions, such as equality, logical or, etc.

func (*BoolType) HasUnderlying

func (p *BoolType) HasUnderlying() bool

HasUnderlying determines whether or not this type has an underlying representation, or not.

func (*BoolType) LeastUpperBound

func (p *BoolType) LeastUpperBound(other Type) Type

LeastUpperBound computes the least upper bound of this type and another. This is smallest type which contains both of the arguments. For example, i32 is the least upper bound of i1 and i32, etc. If no such type exists, then nil is returned.

func (*BoolType) String

func (p *BoolType) String() string

func (*BoolType) SubtypeOf

func (p *BoolType) SubtypeOf(other Type) bool

SubtypeOf determines whether or not this type is a subtype of another.

func (*BoolType) Width

func (p *BoolType) Width() uint

Width returns the number of underlying columns represented by this column. For example, an array of size n will expand into n underlying columns.

type Cast

type Cast struct {
	Arg  Expr
	Type Type
	// Unsafe indicates this is an unsafe cast added explicitly within the
	// constraints based on some developer knowledge.
	Unsafe bool
}

Cast represents a user-supplied annotation indicating the given expression has the given type. This is only sound upto the user.

func (*Cast) AsConstant

func (e *Cast) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Cast) Context

func (e *Cast) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Cast) Dependencies

func (e *Cast) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Cast) Lisp

func (e *Cast) Lisp() sexp.SExp

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

type Circuit

type Circuit struct {
	Modules      []Module
	Declarations []Declaration
}

Circuit represents the root of the Abstract Syntax Tree. This is also referred to as the "prelude". All modules are contained within the root, and declarations can also be declared here as well.

type ColumnBinding

type ColumnBinding struct {
	// Context determines the real (i.e. non-virtual) enclosing module of this
	// column, and should always be a prefix of the path.   If this column was
	// declared in a perspective then it will be the perspective's enclosing
	// module.  Otherwise, it will exactly match the path's parent.
	ColumnContext file.Path
	// Absolute Path of column.  This determines the name of the column, its
	// enclosing module and/or perspective.
	Path file.Path
	// Column's datatype
	DataType Type
	// Determines whether this column must be proven (or not).
	MustProve bool
	// Column's length Multiplier
	Multiplier uint
	// Determines the kind of this column.
	Kind uint8
	// Padding value (defaults to 0)
	Padding big.Int
	// Display modifier
	Display string
}

ColumnBinding represents something bound to a given column.

func (*ColumnBinding) AbsolutePath

func (p *ColumnBinding) AbsolutePath() *file.Path

AbsolutePath returns the fully resolved (absolute) path of the column in question.

func (*ColumnBinding) Context

func (p *ColumnBinding) Context() Context

Context returns the of this column. That is, the module in which this colunm was declared and also the length multiplier of that module it requires.

func (*ColumnBinding) Finalise

func (p *ColumnBinding) Finalise(multiplier uint, datatype Type)

Finalise this binding by providing the necessary missing information.

func (*ColumnBinding) IsComputed

func (p *ColumnBinding) IsComputed() bool

IsComputed checks whether this binding is for a computed column (or not).

func (*ColumnBinding) IsFinalised

func (p *ColumnBinding) IsFinalised() bool

IsFinalised checks whether this binding has been finalised yet or not.

func (*ColumnBinding) IsRecursive

func (p *ColumnBinding) IsRecursive() bool

IsRecursive implementation for Binding interface.

type Concat

type Concat struct {
	Args []Expr
}

Concat represents a bitwise concatenation of expressions. For example, consider the concatenation (:: X Y) where each variable is 16bits. Then the resulting concatenation is 32bits, and corresponds to (X*65536) + Y. The main purpose of concetenations is to smooth the progress of migrating to a field-agnostic code base. We might imagine that this will be deprecated eventually.

func (*Concat) AsConstant

func (e *Concat) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Concat) Context

func (e *Concat) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Concat) Dependencies

func (e *Concat) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Concat) Lisp

func (e *Concat) Lisp() sexp.SExp

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

type Connective

type Connective struct {
	Sign bool // true = OR, false = AND
	Args []Expr
}

Connective represents a logical connective, such as logical AND / logical OR.

func (*Connective) AsConstant

func (e *Connective) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Connective) Context

func (e *Connective) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Connective) Dependencies

func (e *Connective) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Connective) Lisp

func (e *Connective) Lisp() sexp.SExp

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

type Constant

type Constant struct{ Val big.Int }

Constant represents a constant value within an expression.

func (*Constant) AsConstant

func (e *Constant) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Constant) Context

func (e *Constant) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Constant) Dependencies

func (e *Constant) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Constant) Lisp

func (e *Constant) Lisp() sexp.SExp

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

type ConstantBinding

type ConstantBinding struct {
	Path file.Path
	// Explicit type for this constant.  This maybe nil if no type was given
	// and, instead, the type should be inferred from context.
	DataType Type
	// Constant expression which, when evaluated, produces a constant Value.
	Value Expr
	// Determines whether this is an "externalised" constant, or not.
	// Externalised constants are visible at the HIR level and can have their
	// values overridden.
	Extern bool
	// contains filtered or unexported fields
}

ConstantBinding represents a constant definition

func NewConstantBinding

func NewConstantBinding(path file.Path, datatype Type, value Expr, extern bool) ConstantBinding

NewConstantBinding creates a new constant binding (which is initially not finalised).

func (*ConstantBinding) Context

func (p *ConstantBinding) Context() Context

Context returns the of this constant, noting that constants (by definition) do not have a context.

func (*ConstantBinding) Finalise

func (p *ConstantBinding) Finalise()

Finalise this binding.

func (*ConstantBinding) IsFinalised

func (p *ConstantBinding) IsFinalised() bool

IsFinalised checks whether this binding has been finalised yet or not.

func (*ConstantBinding) IsRecursive

func (p *ConstantBinding) IsRecursive() bool

IsRecursive implementation for Binding interface.

type Context

type Context struct {
	// Identifies the module in which this evaluation context exists.  The empty
	// module is given by the maximum index (math.MaxUint).
	ModuleId string
	// Identifies the length multiplier required to complete this context.  In
	// essence, length multiplies divide up a given module into several disjoint
	// "subregions", such than every expression exists only in one of them.
	Multiplier uint
}

Context represents the evaluation context in which an expression can be evaluated. Firstly, every expression must have a single enclosing module (i.e. all columns accessed by the expression are in that module); secondly, the length multiplier for all columns accessed by the expression must be the same. Constant expressions are something of an anomily here since they have neither an enclosing module, nor a length modifier. Instead, we consider that constant expressions are evaluated in the empty --- or void --- context. This is something like a bottom type which is contained within all other contexts.

NOTE: Whilst the evaluation context provides a general abstraction, there are a number of restrictions imposed on it in practice which limit its use. These restrictions arise from what is and is not supported by the underlying constraint system (i.e. the prover). Example restrictions imposed include: multipliers must be powers of 2. Likewise, non-normal expressions (i.e those with a multipler > 1) can only be used in a fairly limited number of situtions (e.g. lookups).

func ConflictingContext

func ConflictingContext() Context

ConflictingContext represents the case where multiple different contexts have been joined together. For example, when determining the context of an expression, the conflicting context is returned when no single context can be deteremed. This value is generally considered to indicate an error.

func ContextOfExpressions

func ContextOfExpressions[E Expr](exprs ...E) (Context, uint)

ContextOfExpressions returns the context for a set of zero or more expressions. Observe that, if there the expressions have no context (i.e. they are all constants) then the void context is returned. Likewise, if there are expressions with different contexts then the conflicted context will be returned. Otherwise, the one consistent context will be returned.

func NewContext

func NewContext(module string, multiplier uint) Context

NewContext returns a context representing the given module with the given length multiplier.

func VoidContext

func VoidContext() Context

VoidContext returns the void (or empty) context. This is the bottom type in the lattice, and is the context contained in all other contexts. It is needed, for example, as the context for constant expressions.

func (Context) IsConflicted

func (p Context) IsConflicted() bool

IsConflicted checks whether this context represents the conflicted context. This is the top element in the lattice, and is used to represent the case where e.g. an expression has multiple conflicting contexts.

func (Context) IsVoid

func (p Context) IsVoid() bool

IsVoid checks whether this context is the void context (or not). This is the bottom element in the lattice.

func (Context) Join

func (p Context) Join(other Context) Context

Join returns the least upper bound of the two contexts, or false if this does not exist (i.e. the two context's are in conflict).

func (Context) LengthMultiplier

func (p Context) LengthMultiplier() uint

LengthMultiplier returns the length multiplier for this context. Note, however, that this is nonsensical in the case of either the void or the conflicted context. In this cases, this method will panic.

func (Context) Module

func (p Context) Module() string

Module returns the module for this context. Note, however, that this is nonsensical in the case of either the void or the conflicted context. In this cases, this method will panic.

func (Context) ModuleName

func (p Context) ModuleName() module.Name

ModuleName returns the name of the module represented by this context. Since context's include length multipliers, this may not match the original (Corset) module name exactly.

func (Context) Multiply

func (p Context) Multiply(factor uint) Context

Multiply updates the length multiplier by multiplying it by a given factor, producing the updated context.

func (Context) String

func (p Context) String() string

type Debug

type Debug struct{ Arg Expr }

Debug is an optional constraint which can be specifically enabled via the debug setting. The intention of debug constraints is that they capture things which are implied by other constraints. The ability to enable them can simply help with debugging, should it arise that they are not actually implied.

func (*Debug) AsConstant

func (e *Debug) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Debug) Context

func (e *Debug) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Debug) Dependencies

func (e *Debug) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Debug) Lisp

func (e *Debug) Lisp() sexp.SExp

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

type Declaration

type Declaration interface {
	Node
	// Returns the set of symbols being defined this declaration.  Observe that
	// these may not yet have been finalised.
	Definitions() iter.Iterator[SymbolDefinition]
	// Return set of columns on which this declaration depends.
	Dependencies() iter.Iterator[Symbol]
	// Check whether this declaration defines a given symbol.  The symbol in
	// question needs to have been resolved already for this to make sense.
	Defines(Symbol) bool
	// Check whether this declaration is finalised already.
	IsFinalised() bool
}

Declaration represents a top-level declaration in a Corset source file (e.g. defconstraint, defcolumns, etc).

type DefAlias

type DefAlias struct {
	// Name of the alias
	Name string
}

DefAlias provides a node on which to hang source information to an alias name.

func NewDefAlias

func NewDefAlias(name string) *DefAlias

NewDefAlias constructs a new instance of DefAlias.

func (*DefAlias) Lisp

func (p *DefAlias) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefAliases

type DefAliases struct {
	// Aliases
	Aliases []*DefAlias
	// Symbols being aliased
	Symbols []Symbol
}

DefAliases represents the declaration of one or more aliases. That is, alternate names for existing symbols.

func NewDefAliases

func NewDefAliases(aliases []*DefAlias, symbols []Symbol) *DefAliases

NewDefAliases constructs a new instance of DefAliases.

func (*DefAliases) Defines

func (p *DefAliases) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefAliases) Definitions

func (p *DefAliases) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefAliases) Dependencies

func (p *DefAliases) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefAliases) IsFinalised

func (p *DefAliases) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefAliases) Lisp

func (p *DefAliases) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefCall

type DefCall struct {
	// Returns for the call
	Returns []Expr
	// Function being called
	Function string
	// Arguments for the call
	Arguments []Expr
	// Optional source selector
	Selector util.Option[Expr]
	// contains filtered or unexported fields
}

DefCall captures a function call between a lisp module and an assembly function. A key feature of this is that it triggers trace propagation.

func NewDefCall

func NewDefCall(returns []Expr, fun string, args []Expr, selector util.Option[Expr]) *DefCall

NewDefCall creates a new (unfinalised) function call.

func (*DefCall) Defines

func (p *DefCall) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefCall) Definitions

func (p *DefCall) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefCall) Dependencies

func (p *DefCall) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefCall) Finalise

func (p *DefCall) Finalise()

Finalise this declaration, which means that all source and target expressions have been resolved.

func (*DefCall) IsFinalised

func (p *DefCall) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefCall) Lisp

func (p *DefCall) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefColumn

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

DefColumn packages together those piece relevant to declaring an individual column, such its name and type.

func NewDefColumn

func NewDefColumn(binding ColumnBinding) *DefColumn

NewDefColumn constructs a new (non-computed) column declaration. Such a column is automatically finalised, since all information is provided at the point of creation.

func NewDefComputedColumn

func NewDefComputedColumn(context file.Path, name file.Path) *DefColumn

NewDefComputedColumn constructs a new column declaration for a computed column. Such a column cannot be finalised yet, since its type and multiplier remains to be determined, etc.

func (*DefColumn) Arity

func (e *DefColumn) Arity() util.Option[uint]

Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.

func (*DefColumn) Binding

func (e *DefColumn) Binding() Binding

Binding returns the allocated binding for this symbol (which may or may not be finalised).

func (*DefColumn) DataType

func (e *DefColumn) DataType() Type

DataType returns the type of this column. If this column have not yet been finalised, then this will panic.

func (*DefColumn) InnerBinding

func (e *DefColumn) InnerBinding() ColumnBinding

InnerBinding returns the allocated binding for this symbol (which may or may not be finalised).

func (*DefColumn) LengthMultiplier

func (e *DefColumn) LengthMultiplier() uint

LengthMultiplier returns the length multiplier of this column (where the height of this column is determined as the product of the enclosing module's height and this length multiplier). If this column have not yet been finalised, then this will panic.

func (*DefColumn) Lisp

func (e *DefColumn) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

func (*DefColumn) MustProve

func (e *DefColumn) MustProve() bool

MustProve determines whether or not the type of this column must be established by the prover (e.g. a range constraint or similar).

func (*DefColumn) Name

func (e *DefColumn) Name() string

Name returns the (unqualified) name of this symbol. For example, "X" for a column X defined in a module m1.

func (*DefColumn) Path

func (e *DefColumn) Path() *file.Path

Path returns the qualified name (i.e. absolute path) of this symbol. For example, "m1.X" for a column X defined in module m1.

type DefColumns

type DefColumns struct {
	Columns []*DefColumn
}

DefColumns captures a set of one or more columns being declared.

func NewDefColumns

func NewDefColumns(columns []*DefColumn) *DefColumns

NewDefColumns constructs a new instance of DefColumns.

func (*DefColumns) Defines

func (p *DefColumns) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefColumns) Definitions

func (p *DefColumns) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefColumns) Dependencies

func (p *DefColumns) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefColumns) IsFinalised

func (p *DefColumns) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefColumns) Lisp

func (p *DefColumns) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefComputed

type DefComputed struct {
	// Columns being assigned by this computation
	Targets []*DefColumn
	// Function being invoked to perform computation
	Function Symbol
	// Source columns as parameters to computation.
	Sources []Symbol
	// Indicates the declaration has been resolved
	Finalised bool
}

DefComputed is an assignment which computes the values for one or more columns based (currently) on a chosen internal function.

func (*DefComputed) Defines

func (p *DefComputed) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefComputed) Definitions

func (p *DefComputed) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefComputed) Dependencies

func (p *DefComputed) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefComputed) Finalise

func (p *DefComputed) Finalise()

Finalise this declaration, which means that all source and target expressions have been resolved.

func (*DefComputed) IsFinalised

func (p *DefComputed) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefComputed) Lisp

func (p *DefComputed) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefComputedColumn

type DefComputedColumn struct {
	// Column being assigned by this computation.
	Target *DefColumn
	// The formula to get the target column from the source columns.
	Computation Expr
	// Indicates the computation has been resolved
	Finalised bool
}

DefComputedColumn is an assignment which computes the values for one column based on a chosen internal function.

func (*DefComputedColumn) Defines

func (p *DefComputedColumn) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefComputedColumn) Definitions

func (p *DefComputedColumn) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefComputedColumn) Dependencies

func (p *DefComputedColumn) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefComputedColumn) Finalise

func (p *DefComputedColumn) Finalise()

Finalise this computed column, which means the target binding and the comptuation itself have been finalised.

func (*DefComputedColumn) IsFinalised

func (p *DefComputedColumn) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefComputedColumn) Lisp

func (p *DefComputedColumn) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefConst

type DefConst struct {
	// List of constant pairs.  Observe that every expression in this list must
	// be constant (i.e. it cannot refer to column values or call impure
	// functions, etc).
	Constants []*DefConstUnit
}

DefConst represents the declaration of one of more constant values which can be used within expressions to improve readability.

func (*DefConst) Defines

func (p *DefConst) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefConst) Definitions

func (p *DefConst) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefConst) Dependencies

func (p *DefConst) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefConst) IsFinalised

func (p *DefConst) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefConst) Lisp

func (p *DefConst) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefConstUnit

type DefConstUnit struct {
	// Binding for this constant.
	ConstBinding ConstantBinding
}

DefConstUnit represents the definition of exactly one constant value. As such, this is an instance of SymbolDefinition and provides a binding.

func (*DefConstUnit) Arity

func (e *DefConstUnit) Arity() util.Option[uint]

Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.

func (*DefConstUnit) Binding

func (e *DefConstUnit) Binding() Binding

Binding returns the allocated binding for this symbol (which may or may not be finalised).

func (*DefConstUnit) Lisp

func (e *DefConstUnit) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

func (*DefConstUnit) Name

func (e *DefConstUnit) Name() string

Name returns the (unqualified) name of this symbol. For example, "X" for a column X defined in a module m1.

func (*DefConstUnit) Path

func (e *DefConstUnit) Path() *file.Path

Path returns the qualified name (i.e. absolute path) of this symbol. For example, "m1.X" for a column X defined in module m1.

type DefConstraint

type DefConstraint struct {
	// Unique handle given to this constraint.  This is primarily useful for
	// debugging (i.e. so we know which constraint failed, etc).
	Handle string
	// Domain of this constraint which, if empty, indicates a global constraint.
	// Otherwise, a given value indicates a single row on which this constraint
	// should apply (where negative values are taken from the end, meaning that
	// -1 represents the last row of a given module).
	Domain util.Option[int]
	// A selector which determines for which rows this constraint is active.
	// Specifically, when the expression evaluates to a non-zero value then the
	// constraint is active; otherwise, its inactive. Nil is permitted to
	// indicate no guard is present.
	Guard Expr
	// Perspective identifies the perspective to which this constraint is
	// associated (if any).
	Perspective *PerspectiveName
	// The constraint itself which (when active) should evaluate to zero for the
	// relevant set of rows.
	Constraint Expr
	// contains filtered or unexported fields
}

DefConstraint represents a vanishing constraint, which is either "local" or "global". A local constraint applies either to the first or last rows, whilst a global constraint applies to all rows. For a constraint to hold, its expression must evaluate to zero for the rows on which it is active. A constraint may also have a "guard" which is an expression that must evaluate to a non-zero value for the constraint to be considered active. The expression for a constraint must have a single context. That is, it can only be applied to columns within the same module (i.e. to ensure they have the same height). Furthermore, within a given module, we require that all columns accessed by the constraint have the same length multiplier.

func NewDefConstraint

func NewDefConstraint(handle string, domain util.Option[int], guard Expr, perspective *PerspectiveName,
	constraint Expr) *DefConstraint

NewDefConstraint constructs a new (unfinalised) constraint.

func (*DefConstraint) Defines

func (p *DefConstraint) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefConstraint) Definitions

func (p *DefConstraint) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefConstraint) Dependencies

func (p *DefConstraint) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefConstraint) Finalise

func (p *DefConstraint) Finalise()

Finalise this declaration, which means that its guard (if applicable) and body have been resolved.

func (*DefConstraint) IsFinalised

func (p *DefConstraint) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefConstraint) Lisp

func (p *DefConstraint) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefFun

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

DefFun represents defines a (possibly pure) "function" (which, in actuality, is more like a macro). Specifically, whenever an invocation of this function is encountered we can imagine that, in the final constraint set, the body of the function is inlined at the point of the call. A pure function is not permitted to access any columns in scope (i.e. it can only manipulate its parameters). In contrast, an impure function can access those columns defined within its enclosing context.

func NewDefFun

func NewDefFun(name *FunctionName, parameters []*DefParameter, ret Type) *DefFun

NewDefFun constructs a new (unfinalised) function declaration.

func (*DefFun) Arity

func (p *DefFun) Arity() util.Option[uint]

Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.

func (*DefFun) Binding

func (p *DefFun) Binding() Binding

Binding returns the allocated binding for this symbol (which may or may not be finalised).

func (*DefFun) Body

func (p *DefFun) Body() Expr

Body Access information about the parameters defined by this declaration.

func (*DefFun) Defines

func (p *DefFun) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefFun) Definitions

func (p *DefFun) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefFun) Dependencies

func (p *DefFun) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefFun) Finalise

func (p *DefFun) Finalise()

Finalise this declaration

func (*DefFun) IsFinalised

func (p *DefFun) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefFun) IsPure

func (p *DefFun) IsPure() bool

IsPure indicates whether or not this is a pure function. That is, a function which is not permitted to access any columns from the enclosing environment (either directly itself, or indirectly via functions it calls).

func (*DefFun) Lisp

func (p *DefFun) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

func (*DefFun) Name

func (p *DefFun) Name() string

Name returns the (unqualified) name of this symbol. For example, "X" for a column X defined in a module m1.

func (*DefFun) Parameters

func (p *DefFun) Parameters() []*DefParameter

Parameters returns information about the parameters defined by this declaration.

func (*DefFun) Path

func (p *DefFun) Path() *file.Path

Path returns the qualified name (i.e. absolute path) of this symbol. For example, "m1.X" for a column X defined in module m1.

func (*DefFun) Return

func (p *DefFun) Return() Type

Return returns the return type of this declaration, which can be nil if no return type was given explicitly.

type DefInRange

type DefInRange struct {
	// The expression whose values are being constrained to within the given
	// bound.
	Expr Expr
	// Bitwidth determines the bitwidth that this range constraint is enforcing.
	Bitwidth uint
	// contains filtered or unexported fields
}

DefInRange restricts all values for a given expression to be within a range [0..n) for some bound n. Any bound is supported, and the system will choose the best underlying implementation as needed.

func (*DefInRange) Defines

func (p *DefInRange) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefInRange) Definitions

func (p *DefInRange) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefInRange) Dependencies

func (p *DefInRange) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefInRange) Finalise

func (p *DefInRange) Finalise()

Finalise this declaration, meaning that the expression has been resolved.

func (*DefInRange) IsFinalised

func (p *DefInRange) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefInRange) Lisp

func (p *DefInRange) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefInterleaved

type DefInterleaved struct {
	// The target column being defined
	Target *DefColumn
	// The source columns used to define the interleaved target column.
	Sources []TypedSymbol
	// Indicates the declaration has been resolved
	Finalised bool
}

DefInterleaved generates a new column by interleaving two or more existing columns. For example, say Z interleaves X and Y (in that order) and we have a trace X=[1,2], Y=[3,4]. Then, the interleaved column Z has the values Z=[1,3,2,4]. All columns must be defined within the same context. Finally, the type of the interleaved column is the widest type of any source columns. For example, consider an interleaving of two columns X and Y with types i16 and i8 respectively. Then, the type of the resulting column is i16 (as this is required to hold an element from any source column).

func (*DefInterleaved) Defines

func (p *DefInterleaved) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefInterleaved) Definitions

func (p *DefInterleaved) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefInterleaved) Dependencies

func (p *DefInterleaved) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefInterleaved) Finalise

func (p *DefInterleaved) Finalise()

Finalise this declaration, which means that all source and target expressions have been resolved.

func (*DefInterleaved) IsFinalised

func (p *DefInterleaved) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefInterleaved) Lisp

func (p *DefInterleaved) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefLookup

type DefLookup struct {
	// Unique handle given to this constraint.  This is primarily useful for
	// debugging (i.e. so we know which constraint failed, etc).
	Handle string
	// Checked determines whether or not "type checking" is enabled for source /
	// target pairs.
	Checked bool
	// Source selector expressions (nil entries mean no selector for corresponding source).
	SourceSelectors []Expr
	// Source expressions for lookup (i.e. these values must all be contained
	// within the targets).
	Sources [][]Expr
	// Target selector expressions (nil entries mean no selector for corresponding source).
	TargetSelectors []Expr
	// Target expressions for lookup (i.e. these values must contain all of the
	// source values, but may contain more).
	Targets [][]Expr
	// contains filtered or unexported fields
}

DefLookup represents a lookup constraint between a set N of source expressions and a set of N target expressions. The source expressions must have a single context (i.e. all be in the same module) and likewise for the target expressions (though the source and target contexts can differ). The constraint can be viewed as a "subset constraint". Let the set of "source tuples" be those obtained by evaluating the source expressions over all rows in the source context, and likewise the "target tuples" those for the target expressions in the target context. Then the lookup constraint holds if the set of source tuples is a subset of the target tuples. This does not need to be a strict subset, so the two sets can be identical. Furthermore, these are not treated as multi-sets, hence the number of occurrences of a given tuple is not relevant.

func NewDefLookup

func NewDefLookup(handle string, checked bool, sourceSelectors []Expr, sources [][]Expr,
	targetSelectors []Expr, targets [][]Expr) *DefLookup

NewDefLookup creates a new (unfinalised) lookup constraint.

func (*DefLookup) Defines

func (p *DefLookup) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefLookup) Definitions

func (p *DefLookup) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefLookup) Dependencies

func (p *DefLookup) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefLookup) Finalise

func (p *DefLookup) Finalise()

Finalise this declaration, which means that all source and target expressions have been resolved.

func (*DefLookup) IsFinalised

func (p *DefLookup) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefLookup) Lisp

func (p *DefLookup) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefParameter

type DefParameter struct {
	Binding LocalVariableBinding
}

DefParameter packages together those piece relevant to declaring an individual parameter, such its name and type.

func NewDefParameter

func NewDefParameter(name string, datatype Type) *DefParameter

NewDefParameter constructs a new parameter declaration.

func (*DefParameter) Lisp

func (p *DefParameter) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefPermutation

type DefPermutation struct {
	Targets []*DefColumn
	Sources []Symbol
	Signs   []bool
}

DefPermutation represents a (lexicographically sorted) permutation of a set of source columns in a given source context, manifested as an assignment to a corresponding set of target columns. The sort direction for each of the source columns can be specified as increasing or decreasing.

func NewDefPermutation

func NewDefPermutation(targets []*DefColumn, sources []Symbol, signs []bool) *DefPermutation

NewDefPermutation constructs a new (unfinalised) sorted permutation assignment.

func (*DefPermutation) Defines

func (p *DefPermutation) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefPermutation) Definitions

func (p *DefPermutation) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefPermutation) Dependencies

func (p *DefPermutation) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefPermutation) IsFinalised

func (p *DefPermutation) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefPermutation) Lisp

func (p *DefPermutation) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefPerspective

type DefPerspective struct {

	// Selector for the perspective.
	Selector Expr
	// Columns defined in this perspective.
	Columns []*DefColumn
	// contains filtered or unexported fields
}

DefPerspective captures the definition of a perspective, its selector and a set of one or more columns being declared within.

func NewDefPerspective

func NewDefPerspective(name *PerspectiveName, selector Expr, columns []*DefColumn) *DefPerspective

NewDefPerspective constructs a new (unfinalised) perspective declaration.

func (*DefPerspective) Arity

func (p *DefPerspective) Arity() util.Option[uint]

Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.

func (*DefPerspective) Binding

func (p *DefPerspective) Binding() Binding

Binding returns the allocated binding for this symbol (which may or may not be finalised).

func (*DefPerspective) Defines

func (p *DefPerspective) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefPerspective) Definitions

func (p *DefPerspective) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefPerspective) Dependencies

func (p *DefPerspective) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefPerspective) Finalise

func (p *DefPerspective) Finalise()

Finalise this perspective, which indicates the selector expression has been finalised.

func (*DefPerspective) IsFinalised

func (p *DefPerspective) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefPerspective) Lisp

func (p *DefPerspective) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

func (*DefPerspective) Name

func (p *DefPerspective) Name() string

Name returns the (unqualified) name of this symbol. For example, "X" for a column X defined in a module m1.

func (*DefPerspective) Path

func (p *DefPerspective) Path() *file.Path

Path returns the qualified name (i.e. absolute path) of this symbol. For example, "m1.X" for a column X defined in module m1.

type DefProperty

type DefProperty struct {
	// Unique handle given to this constraint.  This is primarily useful for
	// debugging (i.e. so we know which constaint failed, etc).
	Handle string
	// Domain of this property which, if empty, indicates the property applies
	// to all rows. Otherwise, a given value indicates a single row on which
	// this property should apply (where negative values are taken from the end,
	// meaning that -1 represents the last row of a given module).
	Domain util.Option[int]
	// The assertion itself which (when active) should evaluate to zero for the
	// relevant set of rows.
	Assertion Expr
	// contains filtered or unexported fields
}

DefProperty represents an assertion to be used only for debugging / testing / verification. Unlike vanishing constraints, property assertions do not represent something that the prover can enforce. Rather, they represent properties which are expected to hold for every valid trace. That is, they should be implied by the actual constraints. Thus, whilst the prover cannot enforce such properties, external tools (such as for formal verification) can attempt to ensure they do indeed always hold.

func NewDefProperty

func NewDefProperty(handle string, domain util.Option[int], assertion Expr) *DefProperty

NewDefProperty constructs a new (unfinalised) property assertion.

func (*DefProperty) Defines

func (p *DefProperty) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefProperty) Definitions

func (p *DefProperty) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefProperty) Dependencies

func (p *DefProperty) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefProperty) Finalise

func (p *DefProperty) Finalise()

Finalise this property, meaning that the assertion has been resolved.

func (*DefProperty) IsFinalised

func (p *DefProperty) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefProperty) Lisp

func (p *DefProperty) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefSorted

type DefSorted struct {
	// Unique handle given to this constraint.  This is primarily useful for
	// debugging (i.e. so we know which constraint failed, etc).
	Handle string
	// Optional selector expression which determines when a sorted constraint is active.
	Selector util.Option[Expr]
	// Source expressions for lookup (i.e. these values must all be contained
	// within the targets).
	Sources []Expr
	// Sorting signs
	Signs []bool
	// Indicates whether sorting constraint is strict (or not).
	Strict bool
	// contains filtered or unexported fields
}

DefSorted ensures that a given set of columns are lexicographically sorted. The sort direction for each of the source columns can be specified as increasing or decreasing.

func NewDefSorted

func NewDefSorted(handle string, selector util.Option[Expr], sources []Expr, signs []bool, strict bool) *DefSorted

NewDefSorted constructs a new (unfinalised) sorted constraint which can (optionally) be controlled by a given selector expression, and may be strict or non-strict. Observe that, for strict sorting, a selector is always needed (i.e. because within padding we cannot guarantee strictness).

func (*DefSorted) Defines

func (p *DefSorted) Defines(symbol Symbol) bool

Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.

func (*DefSorted) Definitions

func (p *DefSorted) Definitions() iter.Iterator[SymbolDefinition]

Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.

func (*DefSorted) Dependencies

func (p *DefSorted) Dependencies() iter.Iterator[Symbol]

Dependencies needed to signal declaration.

func (*DefSorted) Finalise

func (p *DefSorted) Finalise()

Finalise this declaration, which means that all source and target expressions have been resolved.

func (*DefSorted) IsFinalised

func (p *DefSorted) IsFinalised() bool

IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.

func (*DefSorted) Lisp

func (p *DefSorted) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

type DefunBinding

type DefunBinding struct {
	// Flag whether or not is Pure function
	Pure bool
	// Types of parameters (optional)
	ParamTypes []Type
	// Type of return (optional)
	ReturnType Type
	// Body of the function in question.
	Body Expr
	// contains filtered or unexported fields
}

DefunBinding is a function binding arising from a user-defined function (as opposed, for example, to a function binding arising from an intrinsic).

func NewDefunBinding

func NewDefunBinding(pure bool, paramTypes []Type, returnType Type, forced bool, body Expr) DefunBinding

NewDefunBinding constructs a new function binding.

func (*DefunBinding) Finalise

func (p *DefunBinding) Finalise()

Finalise this binding by providing the necessary missing information.

func (*DefunBinding) IsFinalised

func (p *DefunBinding) IsFinalised() bool

IsFinalised checks whether this binding has been finalised yet or not.

func (*DefunBinding) IsNative

func (p *DefunBinding) IsNative() bool

IsNative checks whether this function binding is native (or not).

func (*DefunBinding) IsPure

func (p *DefunBinding) IsPure() bool

IsPure checks whether this is a defpurefun or not

func (*DefunBinding) IsRecursive

func (p *DefunBinding) IsRecursive() bool

IsRecursive implementation for Binding interface.

func (*DefunBinding) Signature

func (p *DefunBinding) Signature() *FunctionSignature

Signature returns the corresponding function signature for this user-defined function.

type Equation

type Equation struct {
	// Indicates equality (true) or non-equality (false).
	Kind uint8
	// Left-Hand Side
	Lhs Expr
	// Right-Hand Side
	Rhs Expr
}

Equation represents either an equality (e.g. X==Y), a non-equality (X!=Y), or an inequality (X<=Y, X<Y, etc).

func (*Equation) AsConstant

func (e *Equation) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Equation) Context

func (e *Equation) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Equation) Dependencies

func (e *Equation) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Equation) LeftHandSide

func (e *Equation) LeftHandSide() Expr

LeftHandSide returns the left-hand side of this condition.

func (*Equation) Lisp

func (e *Equation) Lisp() sexp.SExp

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

func (*Equation) RightHandSide

func (e *Equation) RightHandSide() Expr

RightHandSide returns the right-hand side of this condition.

type Exp

type Exp struct {
	Arg Expr
	Pow Expr
}

Exp represents the a given value taken to a power.

func (*Exp) AsConstant

func (e *Exp) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Exp) Context

func (e *Exp) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Exp) Dependencies

func (e *Exp) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Exp) Lisp

func (e *Exp) Lisp() sexp.SExp

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

type Expr

type Expr interface {
	Node
	// Evaluates this expression as a constant (signed) value.  If this
	// expression is not constant, then nil is returned.
	AsConstant() *big.Int
	// Context returns the context for this expression.  Observe that the
	// expression must have been resolved for this to be defined (i.e. it may
	// panic if it has not been resolved yet).
	Context() Context
	// Return set of columns on which this declaration depends.
	Dependencies() []Symbol
}

Expr represents an arbitrary expression over the columns of a given context (or the parameters of an enclosing function). Such expressions are pitched at a higher-level than those of the underlying constraint system. For example, they can contain conditionals (i.e. if expressions) and normalisations, etc. During the lowering process down to the underlying constraints level (AIR), such expressions are "compiled out" using various techniques (such as introducing computed columns where necessary).

func ShallowCopy

func ShallowCopy(expr Expr) Expr

ShallowCopy creates a copy of the expression itself, but not those expressions it contains (if any). This is useful in e.g. situations where we want to associate different source file information with a specific expression.

func Substitute

func Substitute(expr Expr, mapping map[uint]Expr, srcmap *source.Maps[Node]) Expr

Substitute variables (such as for function parameters) in this expression based on a mapping of said variables to expressions. Furthermore, an (optional) source map is provided which will be updated, such that the freshly created expressions are mapped to their corresponding nodes.

func SubstituteAll

func SubstituteAll(exprs []Expr, mapping map[uint]Expr, srcmap *source.Maps[Node]) []Expr

SubstituteAll substitutes all variables found in a given set of expressions.

func SubstituteOptional

func SubstituteOptional(expr Expr, mapping map[uint]Expr, srcmap *source.Maps[Node]) Expr

SubstituteOptional substitutes through an expression which is optional (i.e. might be nil). In such case, nil is returned.

type For

type For struct {
	// Variable binding
	Binding LocalVariableBinding
	// Start value for Index
	Start uint
	// Last Value for Index
	End uint
	// Body of loop
	Body Expr
}

For represents a for loop of a statically known range of values

func NewFor

func NewFor(name string, start uint, end uint, body Expr) *For

NewFor constructs a new for-expression given a variable name, a static index range and a body.

func (*For) AsConstant

func (e *For) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*For) Context

func (e *For) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*For) Dependencies

func (e *For) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*For) Lisp

func (e *For) Lisp() sexp.SExp

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

func (*For) Multiplicity

func (e *For) Multiplicity() uint

Multiplicity determines the number of values that evaluating this expression can generate.

type FunctionBinding

type FunctionBinding interface {
	Binding
	// IsPure checks whether this function binding has side-effects or not.
	IsPure() bool
	// IsNative checks whether this function binding is native (or not).
	IsNative() bool
	// Signature returns the function signature for this binding.
	Signature() *FunctionSignature
}

FunctionBinding is a special kind of binding which captures the essence of something which can be called. For example, this could be a user-defined function or an intrinsic.

type FunctionName

type FunctionName = Name[*DefunBinding]

FunctionName represents a name used in a position where it can only be resolved as a function.

func NewFunctionName

func NewFunctionName(path file.Path, binding *DefunBinding) *FunctionName

NewFunctionName construct a new column name which is (initially) unresolved.

type FunctionSignature

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

FunctionSignature embodies a concrete function instance. It is necessary to separate bindings from signatures because, in corset, function overloading is supported. That is, we can have different definitions for a function of the same name and arity. The appropriate definition is then selected for the given parameter types.

func NewFunctionSignature

func NewFunctionSignature(pure bool, parameters []Type, ret Type, body Expr) *FunctionSignature

NewFunctionSignature creates a new function signature with a given set of parameter/return types and a body. The signature can also be identified as that of a pure function, or not.

func (*FunctionSignature) Apply

func (p *FunctionSignature) Apply(args []Expr, srcmap *source.Maps[Node]) Expr

Apply a set of concreate arguments to this function. This substitutes them through the body of the function producing a single expression.

func (*FunctionSignature) Arity

func (p *FunctionSignature) Arity() uint

Arity returns the number of parameters in this signature.

func (*FunctionSignature) IsPure

func (p *FunctionSignature) IsPure() bool

IsPure checks whether this function binding has side-effects or not.

func (*FunctionSignature) Parameter

func (p *FunctionSignature) Parameter(index uint) Type

Parameter returns the given parameter in this signature.

func (*FunctionSignature) Return

func (p *FunctionSignature) Return() Type

Return the (optional) return type for this signature. If no declared return type is given, then the intention is that it be inferred from the body.

type If

type If struct {
	// Elements contained within this list.
	Condition Expr
	// True branch (optional).
	TrueBranch Expr
	// False branch (optional).
	FalseBranch Expr
}

If returns the (optional) true branch when the condition evaluates to zero, and the (optional false branch otherwise.

func (*If) AsConstant

func (e *If) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*If) Context

func (e *If) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*If) Dependencies

func (e *If) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*If) Lisp

func (e *If) Lisp() sexp.SExp

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

type IntType

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

IntType represents a set of signed integer values.

func NewIntType

func NewIntType(values math.Interval) *IntType

NewIntType constructs a new integer type containing all values between the lower and upper bounds (inclusive).

func (*IntType) BitWidth

func (p *IntType) BitWidth() uint

BitWidth attempts to determine an appropriate bitwidth for this type.

func (*IntType) HasUnderlying

func (p *IntType) HasUnderlying() bool

HasUnderlying determines whether or not this type has an underlying representation, or not.

func (*IntType) LeastUpperBound

func (p *IntType) LeastUpperBound(other Type) Type

LeastUpperBound computes the least upper bound of this type and another. This is smallest type which contains both of the arguments. For example, i32 is the least upper bound of i1 and i32, etc. If no such type exists, then nil is returned.

func (*IntType) String

func (p *IntType) String() string

func (*IntType) SubtypeOf

func (p *IntType) SubtypeOf(other Type) bool

SubtypeOf determines whether or not this type is a subtype of another.

func (*IntType) Values

func (p *IntType) Values() math.Interval

Values returns the interval of integers contained within this type represents.

func (*IntType) Width

func (p *IntType) Width() uint

Width returns the number of underlying columns represented by this column. For example, an array of size n will expand into n underlying columns.

type Invoke

type Invoke struct {
	Name *VariableAccess
	Args []Expr
}

Invoke represents an attempt to invoke a given function.

func (*Invoke) AsConstant

func (e *Invoke) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Invoke) Context

func (e *Invoke) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Invoke) Dependencies

func (e *Invoke) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Invoke) Lisp

func (e *Invoke) Lisp() sexp.SExp

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

type Let

type Let struct {
	// The set of variables defined by this expression.
	Vars []LocalVariableBinding
	// Identifies the assigned expression for each variable defined.
	Args []Expr
	// Body of the let expression (i.e. where the variables it defines can be
	// used).
	Body Expr
}

Let is a common expression form used in programming languages, particularly functional languages. It allows us to assign a "variable" to a given expression, such that we can reuse that variable in multiple places rather than repeat the entire expression. Note, however, that such variables are functional in nature --- they cannot, for example, be mutated via assignment, etc.

func NewLet

func NewLet(bindings []util.Pair[string, Expr], body Expr) *Let

NewLet constructs a new let-expression for a given number of bindings.

func (*Let) AsConstant

func (e *Let) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Let) Context

func (e *Let) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Let) Dependencies

func (e *Let) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Let) Lisp

func (e *Let) Lisp() sexp.SExp

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

type List

type List struct{ Args []Expr }

List represents a block of zero or more expressions.

func (*List) AsConstant

func (e *List) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*List) Context

func (e *List) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*List) Dependencies

func (e *List) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*List) Lisp

func (e *List) Lisp() sexp.SExp

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

type LocalVariableBinding

type LocalVariableBinding struct {
	// Name the local variable
	Name string
	// Type to use for this parameter.
	DataType Type
	// Identifies the variable or column Index (as appropriate).
	Index uint
}

LocalVariableBinding represents something bound to a given column.

func NewLocalVariableBinding

func NewLocalVariableBinding(name string, datatype Type) LocalVariableBinding

NewLocalVariableBinding constructs an (unitilalised) variable binding. Being uninitialised means that its index identifier remains unknown.

func (*LocalVariableBinding) Finalise

func (p *LocalVariableBinding) Finalise(index uint)

Finalise this local variable binding by allocating it an identifier.

func (*LocalVariableBinding) IsFinalised

func (p *LocalVariableBinding) IsFinalised() bool

IsFinalised checks whether this binding has been finalised yet or not.

func (*LocalVariableBinding) IsRecursive

func (p *LocalVariableBinding) IsRecursive() bool

IsRecursive implementation for Binding interface.

type Module

type Module struct {
	Name         string
	Declarations []Declaration
}

Module represents a top-level module declaration. This corresponds to a table in the final constraint set.

func (*Module) Add

func (p *Module) Add(decl Declaration)

Add a new declaration into this module.

type Mul

type Mul struct{ Args []Expr }

Mul represents the product over zero or more expressions.

func (*Mul) AsConstant

func (e *Mul) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Mul) Context

func (e *Mul) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Mul) Dependencies

func (e *Mul) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Mul) Lisp

func (e *Mul) Lisp() sexp.SExp

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

type Name

type Name[T Binding] struct {
	// contains filtered or unexported fields
}

Name represents a name within some syntactic item. Essentially this wraps a string and provides a mechanism for it to be associated with source line information.

func NewBoundName

func NewBoundName[T Binding](path file.Path, arity util.Option[uint], binding T) *Name[T]

NewBoundName construct a new name which is already unresolved.

func NewUnboundName

func NewUnboundName[T Binding](path file.Path, arity util.Option[uint]) *Name[T]

NewUnboundName construct a new name which is (initially) unresolved.

func (*Name[T]) Arity

func (e *Name[T]) Arity() util.Option[uint]

Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.

func (*Name[T]) Binding

func (e *Name[T]) Binding() Binding

Binding gets binding associated with this interface. This will panic if this symbol is not yet resolved.

func (*Name[T]) InnerBinding

func (e *Name[T]) InnerBinding() T

InnerBinding returns the concrete binding type used within this name.

func (*Name[T]) IsResolved

func (e *Name[T]) IsResolved() bool

IsResolved checks whether this symbol has been resolved already, or not.

func (*Name[T]) Lisp

func (e *Name[T]) Lisp() sexp.SExp

Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.

func (*Name[T]) Name

func (e *Name[T]) Name() string

Name returns the (unqualified) name of this symbol. For example, "X" for a column X defined in a module m1.

func (*Name[T]) Path

func (e *Name[T]) Path() *file.Path

Path returns the qualified name (i.e. absolute path) of this symbol. For example, "m1.X" for a column X defined in module m1.

func (*Name[T]) Resolve

func (e *Name[T]) Resolve(binding Binding) bool

Resolve this symbol by associating it with the binding associated with the definition of the symbol to which this refers.

type Node

type Node interface {
	// Convert this node into its lisp representation.  This is primarily used
	// for debugging purposes.
	Lisp() sexp.SExp
}

Node provides common functionality across all elements of the Abstract Syntax Tree. For example, it ensures every element can converted back into Lisp form for debugging. Furthermore, it provides a reference point for constructing a suitable source map for reporting syntax errors.

type Normalise

type Normalise struct{ Arg Expr }

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

func (*Normalise) AsConstant

func (e *Normalise) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Normalise) Context

func (e *Normalise) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Normalise) Dependencies

func (e *Normalise) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Normalise) Lisp

func (e *Normalise) Lisp() sexp.SExp

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

type Not

type Not struct{ Arg Expr }

Not performs a logical negation on its argument.

func (*Not) AsConstant

func (e *Not) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Not) Context

func (e *Not) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Not) Dependencies

func (e *Not) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Not) Lisp

func (e *Not) Lisp() sexp.SExp

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

type PerspectiveBinding

type PerspectiveBinding struct {
	// Expression which determines when this perspective is enabled.
	Selector Expr
	// contains filtered or unexported fields
}

PerspectiveBinding contains key information about a perspective, such as its selector expression.

func NewPerspectiveBinding

func NewPerspectiveBinding(selector Expr) *PerspectiveBinding

NewPerspectiveBinding constructs a new binding for a given perspective.

func (*PerspectiveBinding) Finalise

func (p *PerspectiveBinding) Finalise()

Finalise this binding, which indicates the selector expression has been finalised.

func (*PerspectiveBinding) IsFinalised

func (p *PerspectiveBinding) IsFinalised() bool

IsFinalised checks whether this binding has been finalised yet or not.

func (*PerspectiveBinding) IsRecursive

func (p *PerspectiveBinding) IsRecursive() bool

IsRecursive implementation for Binding interface.

type PerspectiveName

type PerspectiveName = Name[*PerspectiveBinding]

PerspectiveName represents a name used in a position where it can only be resolved as a perspective.

func NewPerspectiveName

func NewPerspectiveName(path file.Path, binding *PerspectiveBinding) *PerspectiveName

NewPerspectiveName construct a new column name which is (initially) unresolved.

type Reduce

type Reduce struct {
	Name *VariableAccess
	Arg  Expr
}

Reduce reduces (i.e. folds) a list using a given binary function.

func (*Reduce) AsConstant

func (e *Reduce) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Reduce) Context

func (e *Reduce) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Reduce) Dependencies

func (e *Reduce) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Reduce) Lisp

func (e *Reduce) Lisp() sexp.SExp

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

type Shift

type Shift struct {
	// The expression being shifted
	Arg Expr
	// The amount it is being shifted by.
	Shift Expr
}

Shift represents the result of a given expression shifted by a certain amount. In reality, the shift amount must be statically known. However, it is represented here as an expression to allow for constants and the results of function invocations, etc to be used. In all cases, these must still be eventually translated into constant values however.

func (*Shift) AsConstant

func (e *Shift) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Shift) Context

func (e *Shift) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Shift) Dependencies

func (e *Shift) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Shift) Lisp

func (e *Shift) Lisp() sexp.SExp

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

type Sub

type Sub struct{ Args []Expr }

Sub represents the subtraction over zero or more expressions.

func (*Sub) AsConstant

func (e *Sub) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*Sub) Context

func (e *Sub) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*Sub) Dependencies

func (e *Sub) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*Sub) Lisp

func (e *Sub) Lisp() sexp.SExp

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

type Symbol

type Symbol interface {
	Node
	// Path returns the given path of this symbol.
	Path() *file.Path
	// Indicates whether or not this is a function and, if so, what arity (i.e.
	// how many arguments) the function has.
	Arity() util.Option[uint]
	// Checks whether this symbol has been resolved already, or not.
	IsResolved() bool
	// Get binding associated with this interface.  This will panic if this
	// symbol is not yet resolved.
	Binding() Binding
	// Resolve this symbol by associating it with the binding associated with
	// the definition of the symbol to which this refers.  Observe that
	// resolution can fail if we cannot bind the symbol to the given binding
	// (e.g. a function binding was provided, but we're expecting a column
	// binding).
	Resolve(Binding) bool
}

Symbol represents a variable or function access within a declaration. Initially, such the proper interpretation of such accesses is unclear and it is only later when we can distinguish them (e.g. whether its a column access, a constant access, etc).

func DependenciesOfExpressions

func DependenciesOfExpressions(exprs []Expr) []Symbol

DependenciesOfExpressions determines the dependencies for a given set of zero or more expressions.

type SymbolDefinition

type SymbolDefinition interface {
	Node
	// Name returns the (unqualified) name of this symbol.  For example, "X" for
	// a column X defined in a module m1.
	Name() string
	// Path returns the qualified name (i.e. absolute path) of this symbol.  For
	// example, "m1.X" for a column X defined in module m1.
	Path() *file.Path
	// Indicates whether or not this is a function and, if so, what arity (i.e.
	// how many arguments) the function has.
	Arity() util.Option[uint]
	// Allocated binding for the symbol which may or may not be finalised.
	Binding() Binding
}

SymbolDefinition represents a declaration (or part thereof) which defines a particular symbol. For example, "defcolumns" will define one or more symbols representing columns, etc.

type Type

type Type interface {
	// SubtypeOf determines whether or not this type is a subtype of another.
	SubtypeOf(Type) bool

	// LeastUpperBound computes the least upper bound of this type and another. This
	// is smallest type which contains both of the arguments.  For example, i32 is
	// the least upper bound of i1 and i32, etc.  If no such type exists, then nil
	// is returned.
	LeastUpperBound(Type) Type

	// Returns the number of underlying columns represented by this column.  For
	// example, an array of size n will expand into n underlying columns.
	Width() uint

	// Determines whether or not this type has an underlying representation, or
	// not.
	HasUnderlying() bool

	// Produce a string representation of this type.
	String() string
}

Type embodies a richer notion of type found at the Corset level, compared with that found at lower levels (e.g. HIR). below.

var ANY_TYPE Type = &AnyType{}

ANY_TYPE represents the top of the lattice. That is, any type can flow into any.

func LeastUpperBound

func LeastUpperBound(types ...Type) Type

LeastUpperBound computes the Least Upper Bound of two types. This is deliberately coarse-grained and does not, for example, attempt to perform any kind of range analysis for integer types (as this would not make sense).

func LeastUpperBounds

func LeastUpperBounds(lhs []Type, rhs []Type) []Type

LeastUpperBounds returns, for two arrays, the LUB of each type in each position. Either array can be nil, in which case the other is returned. Otherwise, they must have matching lengths (otherwise this will panic).

func NewUintType

func NewUintType(nbits uint) Type

NewUintType constructs a native uint type of the given width which, initially, has no semantic specified.

type TypedSymbol

type TypedSymbol interface {
	Symbol
	// Type returns the type associated with this symbol.  If the type cannot be
	// determined, then nil is returned.
	Type() Type
}

TypedSymbol is an extended form of symbol which contains additional information about a given column access.

type VariableAccess

type VariableAccess struct {
	Name    file.Path
	FnArity util.Option[uint]
	// contains filtered or unexported fields
}

VariableAccess represents reading the value of a given local variable (such as a function parameter).

func NewVariableAccess

func NewVariableAccess(path file.Path, arity util.Option[uint], binding Binding) *VariableAccess

NewVariableAccess creates a new variable access with the given (optionally qualified) path that may (or may not) refer to a function, and which has a given initial binding (which can be nil).

func (*VariableAccess) Arity

func (e *VariableAccess) Arity() util.Option[uint]

Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.

func (*VariableAccess) AsConstant

func (e *VariableAccess) AsConstant() *big.Int

AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.

func (*VariableAccess) Binding

func (e *VariableAccess) Binding() Binding

Binding gets binding associated with this interface. This returns nil if the access has not already been resolved.

func (*VariableAccess) Context

func (e *VariableAccess) Context() Context

Context returns the context for this expression. Observe that the expression must have been resolved for this to be defined (i.e. it may panic if it has not been resolved yet).

func (*VariableAccess) Dependencies

func (e *VariableAccess) Dependencies() []Symbol

Dependencies needed to signal declaration.

func (*VariableAccess) IsResolved

func (e *VariableAccess) IsResolved() bool

IsResolved checks whether this symbol has been resolved already, or not.

func (*VariableAccess) Lisp

func (e *VariableAccess) Lisp() sexp.SExp

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

func (*VariableAccess) Path

func (e *VariableAccess) Path() *file.Path

Path returns the given path of this symbol.

func (*VariableAccess) Resolve

func (e *VariableAccess) Resolve(binding Binding) bool

Resolve this symbol by associating it with the binding associated with the definition of the symbol to which this refers.

func (*VariableAccess) Type

func (e *VariableAccess) Type() Type

Type returns the type associated with this symbol. If the type cannot be determined, then nil is returned.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL