compiler

package
v1.2.4 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Feb 20, 2026 License: Apache-2.0 Imports: 22 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

Copyright Consensys Software Inc.

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.

SPDX-License-Identifier: Apache-2.0

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func BigNumber added in v1.1.8 

func BigNumber[T any, E Expr[T, E]](c *big.Int) E

BigNumber constructs a constant expression from a big integer.

func False added in v1.1.17 

func False[T any, E Expr[T, E]]() E

False constructs an expression which never holds.

func If added in v1.1.8 

func If[T any, E Expr[T, E]](condition E, trueBranch E) E

If constructs an if-then expression.

func IfElse added in v1.1.8 

func IfElse[T any, E Expr[T, E]](condition E, trueBranch E, falseBranch E) E

IfElse constructs an if-then-else expression.

func Number added in v1.1.8 

func Number[T any, E Expr[T, E]](c uint) E

Number constructs a constant expression from an unsigned integer.

func Product added in v1.1.8 

func Product[T any, E Expr[T, E]](exprs []E) E

Product constructs a product over one or more expressions.

func ReadRegister added in v1.2.0 

func ReadRegister[T any, E Expr[T, E]](reg BranchGroupId, reader RegisterReader[E]) E

ReadRegister constructs a suitable accessor for referring to a given register. This applies forwarding as appropriate.

func Sum added in v1.1.8 

func Sum[T any, E Expr[T, E]](exprs []E) E

Sum constructs a sum over one or more expressions.

func True added in v1.1.15 

func True[T any, E Expr[T, E]]() E

True constructs an expression which always holds.

func Variable added in v1.1.8 

func Variable[T any, E Expr[T, E]](id T, bitwidth uint, shift int) E

Variable is just a convenient wrapper for creating abstract expressions representing variable accesses.

Types

type BranchCondition added in v1.1.23 

type BranchCondition = logical.Proposition[BranchGroupId, BranchEquality]

BranchCondition abstracts the possible conditions under which a given branch is taken. 

var FALSE BranchCondition = logical.Truth[BranchGroupId, BranchEquality](false)

FALSE represents an unreachable path 

var TRUE BranchCondition = logical.Truth[BranchGroupId, BranchEquality](true)

TRUE represents an path which is always reached

type BranchConjunction added in v1.1.23 

type BranchConjunction = logical.Conjunction[BranchGroupId, BranchEquality]

BranchConjunction represents the conjunction of two paths

type BranchEquality added in v1.1.23 

type BranchEquality = logical.Equality[BranchGroupId]

BranchEquality represents an atomic branch equality

type BranchGroupId added in v1.2.1 

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

BranchGroupId represents a register ID which can additionally indicate whether forwarding is active or not. Forwarding indicates that the register was previously assigned in the given micro instruction and, hence, needs to be "forwarded" to the point where its used.

func (BranchGroupId) Cmp added in v1.2.1 

func (p BranchGroupId) Cmp(o BranchGroupId) int

Cmp implementation of the logical.Variable interface

func (BranchGroupId) Get added in v1.2.1 

func (p BranchGroupId) Get(i uint) BranchGroupId

Get the ith id in this group as a (singleton) group.

func (BranchGroupId) Registers added in v1.2.1 

func (p BranchGroupId) Registers() []register.Id

Registers returns the set of registers in this group.

func (BranchGroupId) String added in v1.2.1 

func (p BranchGroupId) String() string

String implementation of the logical.Variable interface

type BranchState added in v1.2.0 

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

BranchState adapts a branch condition to be an instance of dfa.State.

func (BranchState) Join added in v1.2.0 

func (p BranchState) Join(st BranchState) BranchState

Join implementation for dfa.State interface

func (BranchState) String added in v1.2.0 

func (p BranchState) String(mapping register.Map) string

String implementation for dfa.State interface

type BranchTransferFunction added in v1.2.0 

type BranchTransferFunction func(offset uint, code micro.Code, state BranchState) []dfa.Transfer[BranchState]

BranchTransferFunction represents a transfer function over branch state.

type Compiler 

type Compiler[F Element[F], T any, E Expr[T, E], M Module[F, T, E, M]] struct {
	// contains filtered or unexported fields
}

Compiler packages up everything needed to compile a given assembly down into an HIR schema. Observe that the compiler may fail if the assembly files are malformed in some way (e.g. fail type checking).

func NewCompiler 

func NewCompiler[F Element[F], T any, E Expr[T, E],
	M Module[F, T, E, M]]() *Compiler[F, T, E, M]

NewCompiler constructs a new compiler

func (*Compiler[F, T, E, M]) Compile 

func (p *Compiler[F, T, E, M]) Compile(program MicroProgram)

Compile a given set of micro functions

func (*Compiler[F, T, E, M]) Modules added in v1.1.8 

func (p *Compiler[F, T, E, M]) Modules() []M

Modules returns the abstract modules constructed during compilation.

type Element added in v1.1.17 

type Element[F any] = field.Element[F]

Element provides a convenient shorthand.

type Expr added in v1.1.8 

type Expr[T, E any] interface {
	// Add constructs a sum between this expression and zero or more
	Add(exprs ...E) E

	// And constructs a conjunction between this expression and zero or more
	// expressions.
	And(...E) E

	// Bool constructs a logical truth or falsehood
	Bool(bool) E

	// Equals constructs an equality between two expressions.
	Equals(rhs E) E

	// Then constructs an implication between two expressions.
	Then(trueBranch E) E

	// ThenElse constructs an if-then-else expression with this expression
	// acting as the condition.
	ThenElse(trueBranch E, falseBranch E) E

	// Multiply constructs a product between this expression and zero or more
	// expressions.
	Multiply(...E) E

	// NotEquals constructs a non-equality between two expressions.
	NotEquals(rhs E) E

	// Number constructs a constant expression.
	BigInt(number big.Int) E

	// Or constructs a disjunction between this expression and zero or more
	// expressions.
	Or(...E) E

	// Variable constructs a variable with a given shift.
	Variable(name T, bitwidth uint, shift int) E

	// String returns a suitable string representation
	String(func(T) string) string
}

Expr provides an abstraction over expressions in the constraint language. Using an abstraction, rather than concrete constraint expressions directly, makes it relatively easier to support multiple target languages.

type Framing added in v1.1.15 

type Framing[T any, E Expr[T, E]] interface {
	// Guard provides a suitable guard for the instruction at a given PC offset.
	// This is optional as some forms of framing don't require it.
	Guard(pc uint) E
	// Goto indicates the current instruction is jumping to the given PC value.
	Goto(pc uint) E
	// Return provides a suitable transition to the next frame.
	Return() E
}

Framing is used to manage additional registers required to ensure soundness. In particular, framinging applies to multi-line functions as these require a program counter, and various control lines to manage padding and non-terminal states.

func NewAtomicFraming added in v1.1.15 

func NewAtomicFraming[T any, E Expr[T, E]]() Framing[T, E]

NewAtomicFraming constructs a suitable framing for a one-line instruction.

func NewMultiLineFraming added in v1.1.15 

func NewMultiLineFraming[T any, E Expr[T, E]](pc T, pcWidth uint, ret T, retWidth uint) Framing[T, E]

NewMultiLineFraming constructs a suitable framing for a multi-line instruction.

type FunctionMapping added in v1.1.8 

type FunctionMapping[T any] struct {
	// contains filtered or unexported fields
}

FunctionMapping provides information regarding the mapping of a assembly-level component (e.g. a function) to the corresponding columns in the underlying constraint system.

func (*FunctionMapping[T]) Bus added in v1.1.8 

func (p *FunctionMapping[T]) Bus() []T

Bus returns the set of input/output columns which represent the "Bus" for this component.

func (*FunctionMapping[T]) ColumnsOf added in v1.1.8 

func (p *FunctionMapping[T]) ColumnsOf(registers ...io.RegisterId) []T

ColumnsOf returns the underlying column identifiers for a given set of zero or more registers.

func (*FunctionMapping[T]) ProgramCounter added in v1.1.18 

func (p *FunctionMapping[T]) ProgramCounter() T

ProgramCounter returns the corresponding column

func (*FunctionMapping[T]) ReturnLine added in v1.1.18 

func (p *FunctionMapping[T]) ReturnLine() T

ReturnLine returns the corresponding column

type MicroComponent added in v1.2.0 

type MicroComponent = io.Component[micro.Instruction]

MicroComponent is a component whose instructions (if applicable) are themselves micro instructions. A micro function represents the lowest representation of a function, where each instruction is made up of microcodes.

type MicroFunction added in v1.1.7 

type MicroFunction = io.Function[micro.Instruction]

MicroFunction is a function composed entirely of micro instructions.

type MicroProgram added in v1.1.17 

type MicroProgram = io.Program[micro.Instruction]

MicroProgram is a program made up from micro- (and external) functions.

type MirExpr added in v1.1.11 

type MirExpr[F field.Element[F]] struct {
	// contains filtered or unexported fields
}

MirExpr is a wrapper around a corset expression which provides the necessary interface.

func (MirExpr[F]) Add added in v1.1.11 

func (p MirExpr[F]) Add(exprs ...MirExpr[F]) MirExpr[F]

Add constructs a sum between this expression and zero or more

func (MirExpr[F]) And added in v1.1.11 

func (p MirExpr[F]) And(exprs ...MirExpr[F]) MirExpr[F]

And constructs a conjunction between this expression and zero or more expressions.

func (MirExpr[F]) BigInt added in v1.1.11 

func (p MirExpr[F]) BigInt(number big.Int) MirExpr[F]

BigInt constructs a constant expression from a big integer.

func (MirExpr[F]) Bool added in v1.1.15 

func (p MirExpr[F]) Bool(val bool) MirExpr[F]

Bool constructs a truth or falsehood

func (MirExpr[F]) Equals added in v1.1.11 

func (p MirExpr[F]) Equals(rhs MirExpr[F]) MirExpr[F]

Equals constructs an equality between two expressions.

func (MirExpr[F]) Multiply added in v1.1.11 

func (p MirExpr[F]) Multiply(exprs ...MirExpr[F]) MirExpr[F]

Multiply constructs a product between this expression and zero or more expressions.

func (MirExpr[F]) NotEquals added in v1.1.11 

func (p MirExpr[F]) NotEquals(rhs MirExpr[F]) MirExpr[F]

NotEquals constructs a non-equality between two expressions.

func (MirExpr[F]) Or added in v1.1.11 

func (p MirExpr[F]) Or(exprs ...MirExpr[F]) MirExpr[F]

Or constructs a disjunction between this expression and zero or more expressions.

func (MirExpr[F]) String added in v1.1.15 

func (p MirExpr[F]) String(func(register.Id) string) string

func (MirExpr[F]) Then added in v1.1.11 

func (p MirExpr[F]) Then(trueBranch MirExpr[F]) MirExpr[F]

Then constructs an implication between two expressions.

func (MirExpr[F]) ThenElse added in v1.1.11 

func (p MirExpr[F]) ThenElse(trueBranch MirExpr[F], falseBranch MirExpr[F]) MirExpr[F]

ThenElse constructs an if-then-else expression with this expression acting as the condition.

func (MirExpr[F]) Variable added in v1.1.11 

func (p MirExpr[F]) Variable(index register.Id, bitwidth uint, shift int) MirExpr[F]

Variable constructs a variable with a given shift.

type MirModule added in v1.1.11 

type MirModule[F field.Element[F]] struct {
	Module ModuleBuilder[F]
}

MirModule provides a wrapper around a corset-level module declaration.

func (MirModule[F]) Initialise added in v1.1.11 

func (p MirModule[F]) Initialise(mid uint, fn MicroComponent) MirModule[F]

Initialise this module

func (MirModule[F]) NewAssignment added in v1.1.12 

func (p MirModule[F]) NewAssignment(assignment schema.Assignment[F])

NewAssignment adds a new assignment to this module.

func (MirModule[F]) NewColumn added in v1.1.11 

func (p MirModule[F]) NewColumn(kind register.Type, name string, bitwidth uint, padding big.Int,
) register.Id

NewColumn constructs a new column of the given name and bitwidth within this module.

func (MirModule[F]) NewConstraint added in v1.1.11 

func (p MirModule[F]) NewConstraint(name string, domain util.Option[int], constraint MirExpr[F])

NewConstraint constructs a new vanishing constraint with the given name within this module.

func (MirModule[F]) NewLookup added in v1.1.11 

func (p MirModule[F]) NewLookup(name string, from []register.Id, target MirModule[F], to []register.Id,
	enable util.Option[register.Id])

NewLookup constructs a new lookup constraint

func (MirModule[F]) NewUnusedColumn added in v1.1.15 

func (p MirModule[F]) NewUnusedColumn() register.Id

NewUnusedColumn constructs an empty (i.e. unused) column identifier.

func (MirModule[F]) String added in v1.1.11 

func (p MirModule[F]) String() string

String returns an appropriately formatted representation of the module.

type Module added in v1.1.8 

type Module[F field.Element[F], T any, E Expr[T, E], M any] interface {
	// SetName sets the name of this module.
	Initialise(mid uint, fn MicroComponent) M

	// NewAssignment adds a new assignment to this module.
	NewAssignment(assignment schema.Assignment[F])

	// NewColumn constructs a new column of the given name and bitwidth within
	// this module.
	NewColumn(kind register.Type, name string, bitwidth uint, padding big.Int) T

	// NewUnusedColumn constructs an empty (i.e. unused) column identifier.
	NewUnusedColumn() T

	// NewConstraint constructs a new vanishing constraint with the given name
	// within this module.  An optional "domain" can be given which determines
	// whether or not this is a "local" or "global" constraint.  Specifically, a
	// local constraint applies only on one row whereas a global constraints
	// applies on all rows.  The domain (if supplied) determines the row where a
	// local constraint applies, with negative values being offset from the last
	// row.  Thus, a domain value of 0 (reps -1) represents the first (resp.
	// last) row of the module.
	NewConstraint(name string, domain util.Option[int], expr E)

	// NewLookup constructs a new lookup constraint
	NewLookup(name string, from []T, target M, to []T, enable util.Option[T])

	// String returns an appropriately formatted representation of the module.
	String() string
}

Module provides an abstraction for modules in the underlying constraint system.

type ModuleBuilder added in v1.1.11 

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

ModuleBuilder is used within this translator for building the various modules which are contained within the mixed MIR schema.

type MultiLineFraming added in v1.1.15 

type MultiLineFraming[T any, E Expr[T, E]] struct {
	// contains filtered or unexported fields
}

MultiLineFraming provides suitable control lines for multi-line functions.

func (*MultiLineFraming[T, E]) Goto added in v1.1.15 

func (p *MultiLineFraming[T, E]) Goto(pc uint) E

Goto implementation for Framing interface.

func (*MultiLineFraming[T, E]) Guard added in v1.1.15 

func (p *MultiLineFraming[T, E]) Guard(pc uint) E

Guard implementation for Framing interface.

func (*MultiLineFraming[T, E]) Return added in v1.1.15 

func (p *MultiLineFraming[T, E]) Return() E

Return implementation for Framing interface.

type OneLineFraming added in v1.1.15 

type OneLineFraming[T any, E Expr[T, E]] struct {
}

OneLineFraming is suitable for one-line functions, as these require no control lines.

func (*OneLineFraming[T, E]) Goto added in v1.1.15 

func (p *OneLineFraming[T, E]) Goto(pc uint) E

Goto implementation for Framing interface.

func (*OneLineFraming[T, E]) Guard added in v1.1.15 

func (p *OneLineFraming[T, E]) Guard(pc uint) E

Guard implementation for Framing interface.

func (*OneLineFraming[T, E]) Return added in v1.1.15 

func (p *OneLineFraming[T, E]) Return() E

Return implementation for Framing interface.

type RegisterReader added in v1.2.0 

type RegisterReader[E any] interface {
	// Register returns information about a given register
	Register(io.RegisterId) io.Register
	// RegisterWidths returns the bitwidth of a given set of registers.
	RegisterWidths(reg ...io.RegisterId) []uint
	// ReadRegister constructs a suitable accessor for referring to a given register.
	// This applies forwarding as appropriate.
	ReadRegister(reg io.RegisterId, forwarding bool) E
}

RegisterReader is a simplified view of a translator which is suitable for reading registers only.

type StateTranslator 

type StateTranslator[F field.Element[F], T any, E Expr[T, E], M Module[F, T, E, M]] struct {
	// contains filtered or unexported fields
}

StateTranslator packages up key information regarding how an individual state of the machine is compiled down to the lower level.

func (*StateTranslator[F, T, E, M]) ReadRegister 

func (p *StateTranslator[F, T, E, M]) ReadRegister(regId io.RegisterId) E

ReadRegister constructs a suitable accessor for referring to a given register. This applies forwarding as appropriate.

func (*StateTranslator[F, T, E, M]) ReadRegisters 

func (p *StateTranslator[F, T, E, M]) ReadRegisters(sources []io.RegisterId) []E

ReadRegisters constructs appropriate column accesses for a given set of registers. When appropriate, forwarding will be applied automatically.

func (*StateTranslator[F, T, E, M]) WriteAndShiftRegisters added in v1.1.7 

func (p *StateTranslator[F, T, E, M]) WriteAndShiftRegisters(targets []io.RegisterId) []E

WriteAndShiftRegisters constructs suitable accessors for the those registers written by a given microinstruction, and also shifts them (i.e. so they can be combined in a sum). This activates forwarding for those registers for all states after this, and returns suitable expressions for the assignment.

func (*StateTranslator[F, T, E, M]) WriteRegister added in v1.1.31 

func (p *StateTranslator[F, T, E, M]) WriteRegister(dst io.RegisterId) E

WriteRegister constructs a suitable accessors for a register written by a given microinstruction. This activates forwarding for that register for all states after this, and returns a suitable expression for the assignment.

func (*StateTranslator[F, T, E, M]) WriteRegisters 

func (p *StateTranslator[F, T, E, M]) WriteRegisters(targets []io.RegisterId) []E

WriteRegisters constructs suitable accessors for the those registers written by a given microinstruction. This activates forwarding for those registers for all states after this, and returns suitable expressions for the assignment.

type Translator 

type Translator[F field.Element[F], T any, E Expr[T, E], M Module[F, T, E, M]] struct {
	// Framining identifies any required control lines.
	Framing Framing[T, E]
	// Registers of the given machine
	Registers []io.Register

	// Mapping from registers to column IDs in the underlying constraint system.
	Columns []T
	// contains filtered or unexported fields
}

Translator encapsulates general information related to the mapping from instructions down to constraints.

func (*Translator[F, T, E, M]) ReadRegister added in v1.2.0 

func (p *Translator[F, T, E, M]) ReadRegister(regId io.RegisterId, forwarding bool) E

ReadRegister constructs a suitable accessor for referring to a given register. This applies forwarding as appropriate.

func (*Translator[F, T, E, M]) Register added in v1.2.1 

func (p *Translator[F, T, E, M]) Register(reg io.RegisterId) io.Register

Register implementation for RegisterReader interface

func (*Translator[F, T, E, M]) RegisterWidths added in v1.2.1 

func (p *Translator[F, T, E, M]) RegisterWidths(regs ...io.RegisterId) []uint

RegisterWidths implementation for RegisterReader interface

func (*Translator[F, T, E, M]) Translate 

func (p *Translator[F, T, E, M]) Translate(pc uint, insn micro.Instruction) E

Translate a micro instruction at a given Program Counter value into a given constraint.

func (*Translator[F, T, E, M]) WithConstancyConstraints added in v1.2.0 

func (p *Translator[F, T, E, M]) WithConstancyConstraints(writes dfa.Writes, branchTable []BranchCondition,
	insn micro.Instruction, condition E) E

WithConstancyConstraints adds constancy constraints for all registers which are either not mutated at all by an instruction, or are sometimes mutated by an instruction. Constancy constraints are required when the value of a register should be copied from the previous state into this state (i.e. because it was not changed by this instruction and, hence, must retain its original value).

A key challenge lies with registers that are sometimes assigned by the instruction, and sometimes not assigned (i.e. maybe but not definitely assigned). To resolve this we first determine the conditions under which they are assigned, and negate this to determine the conditions under which they are not assigned.

NOTE: it is possible to further optimise this process by taking into account which registers are actually used (i.e. live) after this instruction.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.