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
Index ¶
- func CheckConsistent[F any, E term.Contextual](module uint, schema schema.AnySchema[F], terms ...E) []error
- func DetermineHandle[F any](handle string, ctx schema.ModuleId, tr trace.Trace[F]) string
- type Assertion
- func (p Assertion[F]) Accepts(tr trace.Trace[F], sc schema.AnySchema[F]) (bit.Set, schema.Failure)
- func (p Assertion[F]) Bounds(module uint) util.Bounds
- func (p Assertion[F]) Consistent(schema schema.AnySchema[F]) []error
- func (p Assertion[F]) Contexts() []schema.ModuleId
- func (p Assertion[F]) Lisp(schema schema.AnySchema[F]) sexp.SExp
- func (p Assertion[F]) Name() string
- func (p Assertion[F]) Substitute(mapping map[string]F)
- type AssertionFailure
- type InternalFailure
- type Property
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func CheckConsistent ¶
func CheckConsistent[F any, E term.Contextual](module uint, schema schema.AnySchema[F], terms ...E) []error
CheckConsistent performs a simple consistency check for terms in a given module. Specifically, to check that: (1) the module exists; (2) all used registers existing with then given module.
Types ¶
type Assertion ¶
type Assertion[F field.Element[F]] struct { // A unique identifier for this constraint. This is primarily // useful for debugging. Handle string // Enclosing module for this assertion. This restricts the asserted // property to access only columns from within this module. Context schema.ModuleId // Indicates (when empty) a property that applies to all rows. Otherwise, // indicates a property which applies to the specific row given. Domain util.Option[int] // The actual assertion itself, namely an expression which // should hold (i.e. vanish) for every row of a trace. // Observe that this can be any function which is computable // on a given trace --- we are not restricted to expressions // which can be arithmetised. Property term.LogicalComputation[word.BigEndian] }
Assertion is similar to a vanishing constraint but is 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 NewAssertion ¶
func NewAssertion[F field.Element[F]](handle string, ctx schema.ModuleId, domain util.Option[int], property Property) Assertion[F]
NewAssertion constructs a new property assertion!
func (Assertion[F]) Accepts ¶
Accepts checks whether a vanishing constraint evaluates to zero on every row of a table. If so, return nil otherwise return an error.
func (Assertion[F]) Bounds ¶
Bounds is not required for a property assertion since these are not real constraints.
func (Assertion[F]) Consistent ¶
Consistent applies a number of internal consistency checks. Whilst not strictly necessary, these can highlight otherwise hidden problems as an aid to debugging.
func (Assertion[F]) Contexts ¶
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 (Assertion[F]) Name ¶
Name returns a unique name for a given constraint. This is useful purely for identifying constraints in reports, etc.
func (Assertion[F]) Substitute ¶
Substitute any matchined labelled constants within this constraint
type AssertionFailure ¶
type AssertionFailure[F any] struct { // Handle of the failing constraint Handle string // Context schema.ModuleId // Constraint expression Constraint Property // Row on which the constraint failed Row uint }
AssertionFailure provides structural information about a failing vanishing constraint.
func (*AssertionFailure[F]) Message ¶
func (p *AssertionFailure[F]) Message() string
Message provides a suitable error message
func (*AssertionFailure[F]) RequiredCells ¶
func (p *AssertionFailure[F]) RequiredCells(tr trace.Trace[F]) *set.AnySortedSet[trace.CellRef]
RequiredCells identifies the cells required to evaluate the failing constraint at the failing row.
func (*AssertionFailure[F]) String ¶
func (p *AssertionFailure[F]) String() string
type InternalFailure ¶
type InternalFailure[F any] struct { // contains filtered or unexported fields }
InternalFailure is a generic mechanism for reporting failures, particularly as arising from evaluation of a given expression.
func NewInternalFailure ¶
func NewInternalFailure[F any](handle string, ctx schema.ModuleId, row uint, term term.Contextual, err string) *InternalFailure[F]
NewInternalFailure constructs a new internal failure object.
func (*InternalFailure[F]) Error ¶
func (p *InternalFailure[F]) Error() string
Error provides a suitable error message
func (*InternalFailure[F]) Message ¶
func (p *InternalFailure[F]) Message() string
Message provides a suitable error message
func (*InternalFailure[F]) RequiredCells ¶
func (p *InternalFailure[F]) RequiredCells(tr trace.Trace[F]) *set.AnySortedSet[trace.CellRef]
RequiredCells identifies the cells required to evaluate the failing constraint at the failing row.
Source Files
Directories