triton_vm::constraints

Function static_air_constraint_evaluation_tasm

Source
pub fn static_air_constraint_evaluation_tasm(
    mem_layout: StaticTasmConstraintEvaluationMemoryLayout,
) -> Vec<LabelledInstruction>
Expand description

The emitted Triton assembly has the following signature:

§Signature

BEFORE: _
AFTER:  _ *evaluated_constraints

§Requirements

In order for this method to emit Triton assembly, various memory regions need to be declared. This is done through StaticTasmConstraintEvaluationMemoryLayout. The memory layout must be integral.

§Guarantees

  • The emitted code does not declare any labels.
  • The emitted code is “straight-line”, i.e., does not contain any of the instructions call, return, recurse, recurse_or_return, or skiz.
  • The emitted code does not contain instruction halt.
  • All memory write access of the emitted code is within the bounds of the memory region pointed to by *free_memory_page.
  • *evaluated_constraints points to an array of XFieldElements of length NUM_CONSTRAINTS. Each element is the evaluation of one constraint. In particular, the disjoint sequence of slices containing NUM_INITIAL_CONSTRAINTS, NUM_CONSISTENCY_CONSTRAINTS, NUM_TRANSITION_CONSTRAINTS, and NUM_TERMINAL_CONSTRAINTS (respectively and in this order) correspond to the evaluations of the initial, consistency, transition, and terminal constraints.