transform

func AddRangeConstraints ¶ added in v1.2.21

func AddRangeConstraints[W word.Word[W]](cfg field.Config, program descriptor.Program[W],
	maxStaticDepth uint) descriptor.Program[W]

AddRangeConstraints adds, for every distinct register width occurring in the program, a "range" module which acts as the recipient of a range-proof lookup for registers of that width. Two flavours of range module are generated:

• For a width n <= maxStaticWidth, range_un is a static table enumerating every valid value 0 .. 2^n - 1 in a single value column.

• For a width n > maxStaticWidth, range_un destructures the value into two halves (lo of n/2 bits, hi of n-n/2 bits) via the constraint value = hi::lo, and (later) range-checks each half by lookups into range_u{lo} and range_u{hi}. This recursion bottoms out at the static tables above.

Native (field-element) registers are not ranged-checked.

NOTE: this transform must run after register splitting.

func FactorSkipConditions ¶

func FactorSkipConditions[W word.Word[W]](program descriptor.Program[W]) descriptor.Program[W]

FactorSkipConditions rewrites each equality SkipIf (EQ/NEQ) whose comparison would otherwise be replicated across the guarded writes of its branch. The branch condition is materialised once into a fresh 1-bit register.

Concretely, a skip of the form:

skip_if L == R S   (ifBranch) (elseBranch)

is rewritten into the following diamond (`b` and `zero` are fresh):

zero = 0
skip_if L == R 2     // condition holds => jump to b = 1
b = 0                // condition does not hold
skip 1
b = 1                // condition holds
skip_if b != 0 S     // original skip, now testing the bit
(ifBranch) (elseBranch)

NOTE: this transform must run after vectorisation (so the branch's guarded writes share the condition) and before register splitting (so comparison operands remain single registers).

func FlattenCalls ¶ added in v1.2.21

func FlattenCalls[W word.Word[W]](program descriptor.Program[W]) descriptor.Program[W]

FlattenCalls snapshots, into a fresh temporary, each call argument whose register is also written at or after the call within the same vector.

The lookup gluing a call to its callee reads the argument and return columns at the call's row. If an argument register is also written elsewhere in the call's vector, that column holds the final value rather than the argument actually passed, so we snapshot the argument into a fresh temporary first and let the call read that instead. Two situations require this:

• the argument is also a return of the call (e.g. "x = f(x)"); or
• the argument coincides with a register written by a later instruction in the vector, e.g. the destination of the enclosing assignment in "x = f(x) + 1" (lowered to "$t = f(x); x = $t + 1").

We could avoid the temporary, but it would imply a lookup with a row shift, which makes the prover's life harder. This pass is therefore only meaningful when generating arithmetic constraints (it is not required by the vm) and must run after vectorisation, so the writes which would corrupt the argument column share the call's vector.

func InlineFunctions ¶

func InlineFunctions[W word.Word[W]](program descriptor.Program[W], names []string) descriptor.Program[W]

InlineFunctions constructs an equivalent bytecode program in which every call to one of the named functions has been inlined at its call site, and the named function modules removed. Removing modules shifts the identifiers of those which follow, hence module identifiers within Call / ReadWrite bytecodes are remapped accordingly.

Inlining a call site replaces the Call bytecode with the callee's body, where every callee register is realised by a caller register. Where possible, callee inputs / outputs are aliased directly to the corresponding argument / return registers of the call; otherwise, a fresh (caller-local) shadow register is allocated, along with a copy of the argument register into the shadowed input at entry (resp. of the shadowed output into the return register at exit). Such copies enforce the same dynamic width checks as entering / leaving the callee's stack frame did, hence aliasing additionally requires identically shaped registers (see buildShadowMap for the exact conditions).

Output aliasing assumes the callee never reads an output before assigning it, and assigns every output before returning. Both are guaranteed for compiler-generated functions (see validate.ControlFlow); programs built by other means which violate them may observe the return register's previous value where a true call would have observed the callee's initial (zero) output.

This transform must be applied before vectorisation, since it splits the vector containing a call at the call site. It panics on: an unknown or duplicate name; a native function; the entry function "main"; or (mutual) recursion amongst the named functions.

func InsertCheckCasts ¶ added in v1.2.21

func InsertCheckCasts[W word.Word[W]](program descriptor.Program[W]) descriptor.Program[W]

InsertCheckCasts inserts the width-check (CHECKCAST) bytecodes required by a bytecode program. Codegen emits "core" operations without casts; this pass adds, for each operation, the cast checks needed when a result (or a value crossing a module boundary) is written to a narrower register -- mirroring the width checks the slow word machine performs implicitly on every register write. It is applied per function via bytecode.Vector.Map, which rebuilds the vector and rewrites any branch (skip) offsets to account for the inserted bytecodes. Memories have no body and are returned unchanged.

References to other modules (a call's callee, a memory access's memory) are resolved against the program's module signatures, so this pass must run on a complete program.

func LowerBitwise ¶

func LowerBitwise[W word.Word[W]](program descriptor.Program[W]) descriptor.Program[W]

LowerBitwise rewrites VM-level NOT and SHL/SHR bytecodes: NOT is inlined as (MASK - x), while SHL/SHR become CALLs to helper functions whose modules are appended to the returned program. AND/OR/XOR are left untouched here and are lowered after register splitting instead (see LowerOrXorAnd).

We assume this lowering happens BEFORE vectorization and register splitting.

func LowerComparisons ¶

func LowerComparisons[W word.Word[W]](program descriptor.Program[W]) descriptor.Program[W]

LowerComparisons rewrites SkipIf bytecodes with LT/GT/LTEQ/GTEQ conditions into arithmetic-only sequences using biased subtraction and sign-bit extraction. EQ and NEQ conditions are left unchanged.

NOTE: this transform must run after LowerBitwise.

func LowerDivisions ¶

func LowerDivisions[W word.Word[W]](program descriptor.Program[W]) descriptor.Program[W]

LowerDivisions rewrites INT_DIV and INT_REM bytecodes into a non-deterministic hint followed by arithmetic validation (see expandDivRem for the emitted sequence and the rationale for its structure):

Hint{DIV_HINT, q, r, w, x, y}   // prover fills quotient, remainder and range witness
qy  = q * y
qyr = qy + r
0   = x - qyr            // written into a 0-width register: asserts x == q*y + r
rw1 = r + w + 1
0   = y - rw1            // written into a 0-width register: asserts y == r + w + 1

NOTE: this transform must run before LowerComparisons.

func LowerOrXorAnd ¶ added in v1.2.22

func LowerOrXorAnd[W word.Word[W]](program descriptor.Program[W], maxStaticDepth uint) descriptor.Program[W]

LowerOrXorAnd rewrites VM-level bitwise AND/OR/XOR bytecodes into either a static-table lookup (a memory read) or a CALL to a recursive helper function, appending the helper / table modules to the returned program.

Unlike LowerBitwise (which handles NOT and SHL/SHR before splitting), this pass runs AFTER register splitting: SplitRegisters has already broken each wide AND/OR/XOR into limb-wide bitwise bytecodes (see split.Bitwise), so the helpers built here operate at the (narrow) limb width.

It must run before AddRangeConstraints (so the freshly introduced registers are range-checked) and the CALLs it introduces must subsequently be flattened.

func LowerSwitch ¶ added in v1.2.21

func LowerSwitch[W word.Word[W]](program descriptor.Program[W]) descriptor.Program[W]

LowerSwitch rewrites Switch (multiway skip) bytecodes into equivalent sequences of SkipIf bytecodes. Each dispatch case becomes two codes: a constant load of the case's value into a fresh register, followed by a conditional (EQ) skip against the dispatch register targeting the case's original destination. Cases are tested in order, preserving the first-match-wins semantics of the multiway dispatch; when no case matches, control falls through exactly as before.

NOTE: this transform must run before register splitting (which does not support Switch bytecodes).

func OptimizeDivisions ¶

func OptimizeDivisions[W word.Word[W]](program descriptor.Program[W]) descriptor.Program[W]

OptimizeDivisions is a fast mode optimization that rewrites integer divisions and remainders by a constant power-of-two divisor into a (logical) right shift and a bitwise AND respectively. That is, bytecodes of the form

$4 = 0x2^k ; q = x / $4   =>   $4 = 0xk ; q = x >> $4
$5 = 0x2^k ; r = x % $5   =>   $5 = 0x2^k-1 ; r = x & $5

Because each bytecode maps to exactly one bytecode, no register is left dead and the bytecode count is unchanged (so branch / skip offsets are unaffected).

To stay sound, a divisor register is only repurposed when it holds a single statically-known power-of-two constant and is read exactly once (i.e. only by this division / remainder); otherwise — including the case where a divisor constant is bound to a variable and shared across instructions — the operation is left unchanged.

NOTE: we could apply more optimization here like: - deal with generic constants - when doing remainder and division by the same constant, we can compute the quotient and remainder together

func ProgramToProgram ¶ added in v1.2.21

func ProgramToProgram[W1 word.Word[W1], W2 word.Word[W2]](p descriptor.Program[W1]) descriptor.Program[W2]

ProgramToProgram transforms a bytecode program operating over a given word type (W1) into an identical program which operates over a different word type (W2). Generally speaking, we are going from a larger word (e.g. word.Uint) to a smaller word (e.g. word.Uint64). This is the program-level analogue of WordToWordMachine.

The transformation is purely structural: bytecodes are re-typed but not rewritten or lowered, register declarations are preserved verbatim (no splitting or width changes), and constants are not reduced modulo the field. Only bytecodes and registers carrying a W-typed value (arithmetic constants, dispatch values and register padding) are re-expressed in W2; all others are word-type-agnostic and carry over unchanged. Static memory contents are converted element-wise; non-static memories carry no contents in either representation.

This function will panic if it encounters a register, constant or memory cell which exceeds the bandwidth of W2. Callers needing to target a narrower word size than some source register widths should run SplitRegisters first.

func SplitRegisters ¶

func SplitRegisters[W word.Word[W]](cfg word.Config, program descriptor.Program[W]) descriptor.Program[W]

SplitRegisters splits all registers in a program to meet a given field's bandwidth and maximum register width. This will split all registers wider than the maximum permitted width into two or more "limbs" (i.e. subregisters which do not exceeded the permitted width). For example, consider a register "r" of width u32. Subdividing this register into registers of at most 8bits will result in four limbs: r'0, r'1, r'2 and r'3 where (by convention) r'0 is the least significant.

func Vectorize ¶ added in v1.2.21

func Vectorize[W word.Word[W]](program descriptor.Program[W]) descriptor.Program[W]

Vectorize a given program by merging as many bytecodes as possible into each (vector) bytecode. The strategy is greedy: walking each function, we repeatedly try to absorb the target of a goto back into the vector containing that goto, effectively pulling a successor vector up into its predecessor until no further merging is legal. For example, given two bytecodes "x = y" and "a = b", neither writes a register the other touches and so they can be combined into the single vector "x=y ; a=b" whose constituents execute "in parallel".

The principal obstacle to merging is the appearance of *register conflicts* between bytecodes — that is, data hazards in the classical sense from computer architecture. All three textbook hazards (RAW, WAW, WAR) arise here, where "earlier" and "later" refer to the position of two bytecodes within the same vector:

• RAW (Read-After-Write). A later bytecode reads a register that an earlier bytecode writes. This is the "true" data dependency. Within a vector it is normally resolved by *register forwarding*: the later bytecode simply observes the freshly-written value. However, when the upstream write is *conditional* — i.e. it occurs on some intra-vector control-flow paths but not others — the value to forward is not well-defined and the merge is rejected. This is reported as a "conflicting read".

• WAW (Write-After-Write). Two bytecodes in the same vector both write the same register. The resulting register value would be ambiguous, so the merge is rejected. This is reported as a "conflicting write", and is the most common form of register conflict in practice.

• WAR (Write-After-Read). A later bytecode writes a register that an earlier bytecode reads. This is *not* a hazard in this setting, because forwarding flows strictly forward: the earlier read always observes the pre-vector value, while the later write only takes effect once the whole vector completes. No check is required, and no merge is blocked on this account.

Register forwarding is the mechanism that makes RAW dependencies tractable inside a vector. When one bytecode writes a register, every subsequent bytecode in the same vector observes the freshly-written value rather than the value held at the start of the vector.

In addition to data hazards, two further conditions block a merge:

• Other validation failures. The merged vector must continue to satisfy every well-formedness invariant for vectors.

• Back-edges. A goto whose target would bring control back into the vector being built (a loop) is left alone; otherwise the inliner would unfold it indefinitely.