Documentation
¶
Overview ¶
Copyright Consensys Software Inc.
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.
SPDX-License-Identifier: Apache-2.0
Copyright Consensys Software Inc.
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.
SPDX-License-Identifier: Apache-2.0
Index ¶
- func HoldsGlobally[F field.Element[F], T term.Testable[F]](handle string, ctx schema.ModuleId, constraint T, trMod trace.Module[F], ...) (bit.Set, schema.Failure)
- func HoldsLocally[F field.Element[F], T term.Testable[F]](k uint, handle string, term T, ctx schema.ModuleId, trMod trace.Module[F], ...) (schema.Failure, uint)
- type Constraint
- func (p Constraint[F, T]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F]) (bit.Set, schema.Failure)
- func (p Constraint[F, T]) Bounds(module uint) util.Bounds
- func (p Constraint[F, T]) Consistent(schema schema.AnySchema[F]) []error
- func (p Constraint[F, T]) Contexts() []schema.ModuleId
- func (p Constraint[F, T]) Lisp(mapping schema.AnySchema[F]) sexp.SExp
- func (p Constraint[F, T]) Name() string
- func (p Constraint[F, T]) Substitute(mapping map[string]F)
- type Failure
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func HoldsGlobally ¶
func HoldsGlobally[F field.Element[F], T term.Testable[F]](handle string, ctx schema.ModuleId, constraint T, trMod trace.Module[F], scMod schema.Module[F]) (bit.Set, schema.Failure)
HoldsGlobally checks whether a given expression vanishes (i.e. evaluates to zero) for all rows of a trace. If not, report an appropriate error.
func HoldsLocally ¶
func HoldsLocally[F field.Element[F], T term.Testable[F]](k uint, handle string, term T, ctx schema.ModuleId, trMod trace.Module[F], scMod schema.Module[F]) (schema.Failure, uint)
HoldsLocally checks whether a given constraint holds (e.g. vanishes) on a specific row of a trace. If not, report an appropriate error.
Types ¶
type Constraint ¶
type Constraint[F field.Element[F], T term.Testable[F]] struct { // A unique identifier for this constraint. This is primarily // useful for debugging. Handle string // Evaluation Context for this constraint which must match that of the // constrained expression itself. Context schema.ModuleId // Indicates (when empty) a global constraint that applies to all rows. // Otherwise, indicates a local constraint which applies to the specific row // given. Domain util.Option[int] // The actual Constraint itself (e.g. an expression which // should evaluate to zero, etc) Constraint T }
Constraint specifies a constraint which should hold on every row of the table. The only exception is when the constraint is undefined (e.g. because it references a non-existent table cell). In such case, the constraint is ignored. This is parameterised by the type of the constraint expression. Thus, we can reuse this definition across the various intermediate representations (e.g. Mid-Level IR, Arithmetic IR, etc).
func NewConstraint ¶
func NewConstraint[F field.Element[F], T term.Testable[F]](handle string, context schema.ModuleId, domain util.Option[int], constraint T) Constraint[F, T]
NewConstraint constructs a new vanishing constraint
func (Constraint[F, T]) Accepts ¶
func (p Constraint[F, T]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F]) (bit.Set, schema.Failure)
Accepts checks whether a vanishing constraint evaluates to zero on every row of a table. If so, return nil otherwise return an error.
func (Constraint[F, T]) Bounds ¶
func (p Constraint[F, T]) Bounds(module uint) util.Bounds
Bounds determines the well-definedness bounds for this constraint for both the negative (left) or positive (right) directions. For example, consider an expression such as "(shift X -1)". This is technically undefined for the first row of any trace and, by association, any constraint evaluating this expression on that first row is also undefined (and hence must pass).
func (Constraint[F, T]) Consistent ¶
func (p Constraint[F, T]) Consistent(schema schema.AnySchema[F]) []error
Consistent applies a number of internal consistency checks. Whilst not strictly necessary, these can highlight otherwise hidden problems as an aid to debugging.
func (Constraint[F, T]) Contexts ¶
func (p Constraint[F, T]) Contexts() []schema.ModuleId
Contexts returns the evaluation contexts (i.e. enclosing module + length multiplier) for this constraint. Most constraints have only a single evaluation context, though some (e.g. lookups) have more. Note that all constraints have at least one context (which we can call the "primary" context).
func (Constraint[F, T]) Lisp ¶
func (p Constraint[F, T]) Lisp(mapping schema.AnySchema[F]) sexp.SExp
Lisp converts this constraint into an S-Expression.
func (Constraint[F, T]) Name ¶
func (p Constraint[F, T]) Name() string
Name returns a unique name for a given constraint. This is useful purely for identifying constraints in reports, etc.
func (Constraint[F, T]) Substitute ¶
func (p Constraint[F, T]) Substitute(mapping map[string]F)
Substitute any matchined labelled constants within this constraint
type Failure ¶
type Failure[F any] struct { // Handle of the failing constraint Handle string // Constraint expression Constraint term.Testable[F] // Module where constraint failed Context schema.ModuleId // Row on which the constraint failed Row uint }
Failure provides structural information about a failing vanishing constraint.
func (*Failure[F]) RequiredCells ¶
RequiredCells identifies the cells required to evaluate the failing constraint at the failing row.
Source Files