Skip to content

Commit

Permalink
feat: implement error codes for the mtree_verify instructions (#1328)
Browse files Browse the repository at this point in the history
  • Loading branch information
Fumuran authored Jun 6, 2024
1 parent ac9b07c commit 02d153f
Show file tree
Hide file tree
Showing 41 changed files with 155 additions and 112 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
- Removed unused `find_lone_leaf()` function from the Advice Provider (#1262).
- [BREAKING] Changed fields type of the `StackOutputs` struct from `Vec<u64>` to `Vec<Felt>` (#1268).
- [BREAKING] Migrated to `miden-crypto` v0.9.0 (#1287).
- Added error codes support for the `mtree_verify` instruction (#1328).

## 0.8.0 (02-26-2024)

Expand Down
4 changes: 2 additions & 2 deletions air/src/constraints/chiplets/hasher/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -101,9 +101,9 @@ pub fn get_transition_constraint_count() -> usize {
/// Enforces constraints for the hasher chiplet.
///
/// - The `hasher_flag` determines if the hasher chiplet is currently enabled. It should be
/// computed by the caller and set to `Felt::ONE`
/// computed by the caller and set to `Felt::ONE`
/// - The `transition_flag` indicates whether this is the last row this chiplet's execution trace,
/// and therefore the constraints should not be enforced.
/// and therefore the constraints should not be enforced.
pub fn enforce_constraints<E: FieldElement<BaseField = Felt>>(
frame: &EvaluationFrame<E>,
periodic_values: &[E],
Expand Down
8 changes: 4 additions & 4 deletions air/src/constraints/stack/field_ops/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -188,7 +188,7 @@ pub fn enforce_incr_constraints<E: FieldElement>(
/// enforced:
/// - The top element should be a binary. It is enforced as a general constraint.
/// - The first element of the next frame should be a binary not of the first element of
/// the current frame. s0` + s0 = 1.
/// the current frame. s0` + s0 = 1.
pub fn enforce_not_constraints<E: FieldElement>(
frame: &EvaluationFrame<E>,
result: &mut [E],
Expand All @@ -207,7 +207,7 @@ pub fn enforce_not_constraints<E: FieldElement>(
/// Enforces constraints of the AND operation. The AND operation computes the bitwise and of the
/// first two elements in the current trace. Therefore, the following constraints are enforced:
/// - The top two element in the current frame of the stack should be binary. s0^2 - s0 = 0,
/// s1^2 - s1 = 0. The top element is binary or not is enforced as a general constraint.
/// s1^2 - s1 = 0. The top element is binary or not is enforced as a general constraint.
/// - The first element of the next frame should be a binary and of the first two elements in the
/// current frame. s0` - s0 * s1 = 0.
pub fn enforce_and_constraints<E: FieldElement>(
Expand All @@ -234,7 +234,7 @@ pub fn enforce_and_constraints<E: FieldElement>(
/// Enforces constraints of the OR operation. The OR operation computes the bitwise or of the
/// first two elements in the current trace. Therefore, the following constraints are enforced:
/// - The top two element in the current frame of the stack should be binary. s0^2 - s0 = 0,
/// s1^2 - s1 = 0. The top element is binary or not is enforced as a general constraint.
/// s1^2 - s1 = 0. The top element is binary or not is enforced as a general constraint.
/// - The first element of the next frame should be a binary or of the first two elements in the
/// current frame. s0` - ( s0 + s1 - s0 * s1 ) = 0.
pub fn enforce_or_constraints<E: FieldElement>(
Expand Down Expand Up @@ -324,7 +324,7 @@ pub fn enforce_eqz_constraints<E: FieldElement>(
/// constraint.
/// - The exp value in the next frame should be the square of exp value in the current frame.
/// - The accumulation value in the next frame is the product of the accumulation value in the
/// current frame and the value which needs to be included in this turn.
/// current frame and the value which needs to be included in this turn.
/// - The b value is right shifted by 1 bit.
pub fn enforce_expacc_constraints<E: FieldElement>(
frame: &EvaluationFrame<E>,
Expand Down
4 changes: 2 additions & 2 deletions air/src/constraints/stack/op_flags/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ impl<E: FieldElement> OpFlags<E> {
/// - composite flag for the stack if the stack has been shifted to the right.
/// - composite flag if the current operation being executed is a control flow operation or not.
/// - composite flag if the current operation being executed has a binary element constraint on
/// the top element in the stack.
/// the top element in the stack.
pub fn new(frame: &EvaluationFrame<E>) -> Self {
// intermediary array to cache the value of intermediate flags.
let mut degree7_op_flags = [E::ZERO; NUM_DEGREE_7_OPS];
Expand Down Expand Up @@ -866,7 +866,7 @@ impl<E: FieldElement> OpFlags<E> {
/// Operation Flag of MPVERIFY operation.
#[inline(always)]
pub fn mpverify(&self) -> E {
self.degree5_op_flags[get_op_index(Operation::MpVerify.op_code())]
self.degree5_op_flags[get_op_index(Operation::MpVerify(0).op_code())]
}

/// Operation Flag of SPLIT operation.
Expand Down
4 changes: 2 additions & 2 deletions air/src/constraints/stack/op_flags/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ fn degree_4_op_flags() {
fn composite_flags() {
// ------ no change 0 ---------------------------------------------------------------------

let op_no_change_0 = [Operation::MpVerify, Operation::Span, Operation::Halt];
let op_no_change_0 = [Operation::MpVerify(0), Operation::Span, Operation::Halt];
for op in op_no_change_0 {
// frame initialised with an op operation.
let frame = generate_evaluation_frame(op.op_code().into());
Expand All @@ -169,7 +169,7 @@ fn composite_flags() {
assert_eq!(op_flags.left_shift(), ZERO);
assert_eq!(op_flags.top_binary(), ZERO);

if op == Operation::MpVerify {
if op == Operation::MpVerify(0) {
assert_eq!(op_flags.control_flow(), ZERO);
} else if op == Operation::Span || op == Operation::Halt {
assert_eq!(op_flags.control_flow(), ONE);
Expand Down
6 changes: 3 additions & 3 deletions air/src/constraints/stack/overflow/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ pub fn enforce_stack_depth_constraints<E: FieldElement>(
/// Enforces constraints on the overflow flag h0. Therefore, the following constraints
/// are enforced:
/// - If overflow table has values, then, h0 should be set to ONE, otherwise it should
/// be ZERO.
/// be ZERO.
pub fn enforce_overflow_flag_constraints<E: FieldElement>(
frame: &EvaluationFrame<E>,
result: &mut [E],
Expand All @@ -108,9 +108,9 @@ pub fn enforce_overflow_flag_constraints<E: FieldElement>(

/// Enforces constraints on the bookkeeping index `b1`. The following constraints are enforced:
/// - In the case of a right shift operation, the next b1 index should be updated with current
/// `clk` value.
/// `clk` value.
/// - In the case of a left shift operation, the last stack item should be set to ZERO when the
/// depth of the stack is 16.
/// depth of the stack is 16.
pub fn enforce_overflow_index_constraints<E: FieldElement>(
frame: &EvaluationFrame<E>,
result: &mut [E],
Expand Down
4 changes: 2 additions & 2 deletions air/src/constraints/stack/stack_manipulation/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ pub fn enforce_pad_constraints<E: FieldElement>(
/// at depth n in the stack and pushes the copy onto the stack, whereas MOVUPn opearation moves the
/// element at depth n to the top of the stack. Therefore, the following constraints are enforced:
/// - The top element in the next frame should be equal to the element at depth n in the
/// current frame. s0` - sn = 0.
/// current frame. s0` - sn = 0.
pub fn enforce_dup_movup_n_constraints<E: FieldElement>(
frame: &EvaluationFrame<E>,
result: &mut [E],
Expand Down Expand Up @@ -245,7 +245,7 @@ pub fn enforce_swapwx_constraints<E: FieldElement>(
/// Enforces constraints of the MOVDNn operation. The MOVDNn operation moves the top element
/// to depth n in the stack. Therefore, the following constraints are enforced:
/// - The top element in the current frame should be equal to the element at depth n in the
/// next frame. s0 - sn` = 0.
/// next frame. s0 - sn` = 0.
pub fn enforce_movdnn_constraints<E: FieldElement>(
frame: &EvaluationFrame<E>,
result: &mut [E],
Expand Down
9 changes: 4 additions & 5 deletions air/src/constraints/stack/u32_ops/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ pub fn enforce_u32split_constraints<E: FieldElement<BaseField = Felt>>(
/// elements in the current trace of the stack. Therefore, the following constraints are
/// enforced:
/// - The aggregation of limbs from the helper registers is equal to the sum of the top two
/// element in the stack.
/// element in the stack.
pub fn enforce_u32add_constraints<E: FieldElement<BaseField = Felt>>(
frame: &EvaluationFrame<E>,
result: &mut [E],
Expand All @@ -141,7 +141,7 @@ pub fn enforce_u32add_constraints<E: FieldElement<BaseField = Felt>>(
/// elements in the current trace of the stack. Therefore, the following constraints are
/// enforced:
/// - The aggregation of limbs from the helper registers is equal to the sum of the top three
/// elements in the stack.
/// elements in the stack.
pub fn enforce_u32add3_constraints<E: FieldElement<BaseField = Felt>>(
frame: &EvaluationFrame<E>,
result: &mut [E],
Expand Down Expand Up @@ -289,10 +289,9 @@ pub fn enforce_check_element_validity<E: FieldElement<BaseField = Felt>>(
/// Enforces constraints of the general operation. The constaints checks if the lower 16-bits limbs
/// are aggregated correctly or not. Therefore, the following constraints are enforced:
/// - The aggregation of lower two lower 16-bits limbs in the helper registers is equal to the
/// second
/// element in the next row.
/// second element in the next row.
/// - The aggregation of lower two upper 16-bits limbs in the helper registers is equal to the first
/// element in the next row.
/// element in the next row.
pub fn enforce_limbs_agg<E: FieldElement<BaseField = Felt>>(
frame: &EvaluationFrame<E>,
result: &mut [E],
Expand Down
17 changes: 1 addition & 16 deletions assembly/src/assembler/instruction/crypto_ops.rs
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,7 @@ pub(super) fn mtree_get(span: &mut SpanBuilder) {
let ops = [
// verify the node V for root R with depth d and index i
// => [V, d, i, R, ...]
MpVerify,
MpVerify(0),

// move d, i back to the top of the stack and are dropped since they are
// no longer needed => [V, R, ...]
Expand Down Expand Up @@ -172,21 +172,6 @@ pub(super) fn mtree_merge(span: &mut SpanBuilder) {
hmerge(span);
}

/// Verifies if the node value `V`, on depth `d` and index `i` opens to the root `R` of a Merkle
/// tree by appending a [Operation::MpVerify]. The stack is expected to be arranged as follows
/// (from the top):
/// - node value `V`, 4 elements
/// - depth of the node `d`, 1 element
/// - index of the node `i`, 1 element
/// - root of the tree `R`, 4 elements
///
/// After the operation is executed, the stack remains unchanged.
///
/// This operation takes 1 VM cycle.
pub(super) fn mtree_verify(span: &mut SpanBuilder) {
span.push_op(MpVerify);
}

// MERKLE TREES - HELPERS
// ================================================================================================

Expand Down
5 changes: 4 additions & 1 deletion assembly/src/assembler/instruction/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -349,7 +349,10 @@ impl Assembler {
Instruction::MTreeGet => crypto_ops::mtree_get(span_builder),
Instruction::MTreeSet => crypto_ops::mtree_set(span_builder),
Instruction::MTreeMerge => crypto_ops::mtree_merge(span_builder),
Instruction::MTreeVerify => crypto_ops::mtree_verify(span_builder),
Instruction::MTreeVerify => span_builder.push_op(MpVerify(0)),
Instruction::MTreeVerifyWithError(err_code) => {
span_builder.push_op(MpVerify(err_code.expect_value()))
}

// ----- STARK proof verification -----------------------------------------------------
Instruction::FriExt2Fold4 => span_builder.push_op(FriE2F4),
Expand Down
8 changes: 4 additions & 4 deletions assembly/src/assembler/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,12 +77,12 @@ pub enum ArtifactKind {
/// </div>
///
/// * If you have a single executable module you want to compile, just call [Assembler::compile] or
/// [Assembler::compile_ast], depending on whether you have source code in raw or parsed form.
/// [Assembler::compile_ast], depending on whether you have source code in raw or parsed form.
///
/// * If you want to link your executable to a few other modules that implement supporting
/// procedures, build the assembler with them first, using the various builder methods on
/// [Assembler], e.g. [Assembler::with_module], [Assembler::with_library], etc. Then, call
/// [Assembler::compile] or [Assembler::compile_ast] to get your compiled program.
/// procedures, build the assembler with them first, using the various builder methods on
/// [Assembler], e.g. [Assembler::with_module], [Assembler::with_library], etc. Then, call
/// [Assembler::compile] or [Assembler::compile_ast] to get your compiled program.
pub struct Assembler {
/// The global [ModuleGraph] for this assembler. All new [AssemblyContext]s inherit this graph
/// as a baseline.
Expand Down
4 changes: 2 additions & 2 deletions assembly/src/assembler/module_graph/rewrites/module.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,8 @@ use crate::{
/// added to a [ModuleGraph]. These rewrites include:
///
/// * Resolving, at least partially, all of the invocation targets in procedures of the module, and
/// rewriting those targets as concretely as possible OR as phantom calls representing procedures
/// referenced by MAST root for which we have no definition.
/// rewriting those targets as concretely as possible OR as phantom calls representing procedures
/// referenced by MAST root for which we have no definition.
pub struct ModuleRewriter<'a, 'b: 'a> {
resolver: &'a NameResolver<'b>,
module_id: ModuleIndex,
Expand Down
3 changes: 3 additions & 0 deletions assembly/src/ast/instruction/deserialize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -272,6 +272,9 @@ impl Deserializable for Instruction {
OpCode::MTreeSet => Ok(Self::MTreeSet),
OpCode::MTreeMerge => Ok(Self::MTreeMerge),
OpCode::MTreeVerify => Ok(Self::MTreeVerify),
OpCode::MTreeVerifyWithError => {
Ok(Self::MTreeVerifyWithError(source.read_u32()?.into()))
}

// ----- STARK proof verification -----------------------------------------------------
OpCode::FriExt2Fold4 => Ok(Self::FriExt2Fold4),
Expand Down
1 change: 1 addition & 0 deletions assembly/src/ast/instruction/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -251,6 +251,7 @@ pub enum Instruction {
MTreeSet,
MTreeMerge,
MTreeVerify,
MTreeVerifyWithError(ErrorCode),

// ----- STARK proof verification ------------------------------------------------------------
FriExt2Fold4,
Expand Down
1 change: 1 addition & 0 deletions assembly/src/ast/instruction/opcode.rs
Original file line number Diff line number Diff line change
Expand Up @@ -241,6 +241,7 @@ pub enum OpCode {
MTreeSet,
MTreeMerge,
MTreeVerify,
MTreeVerifyWithError,

// ----- STARK proof verification ------------------------------------------------------------
FriExt2Fold4,
Expand Down
3 changes: 3 additions & 0 deletions assembly/src/ast/instruction/print.rs
Original file line number Diff line number Diff line change
Expand Up @@ -258,6 +258,9 @@ impl PrettyPrint for Instruction {
Self::MTreeSet => const_text("mtree_set"),
Self::MTreeMerge => const_text("mtree_merge"),
Self::MTreeVerify => const_text("mtree_verify"),
Self::MTreeVerifyWithError(err_code) => {
flatten(const_text("mtree_verify.err") + const_text("=") + display(err_code))
}

// ----- STARK proof verification -----------------------------------------------------
Self::FriExt2Fold4 => const_text("fri_ext2fold4"),
Expand Down
4 changes: 4 additions & 0 deletions assembly/src/ast/instruction/serialize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -386,6 +386,10 @@ impl Serializable for Instruction {
Self::MTreeSet => OpCode::MTreeSet.write_into(target),
Self::MTreeMerge => OpCode::MTreeMerge.write_into(target),
Self::MTreeVerify => OpCode::MTreeVerify.write_into(target),
Self::MTreeVerifyWithError(err_code) => {
OpCode::MTreeVerifyWithError.write_into(target);
target.write_u32(err_code.expect_value());
}

// ----- STARK proof verification -----------------------------------------------------
Self::FriExt2Fold4 => OpCode::FriExt2Fold4.write_into(target),
Expand Down
8 changes: 4 additions & 4 deletions assembly/src/ast/module.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,11 +46,11 @@ pub enum ModuleKind {
/// A kernel is like a library module, but is special in a few ways:
///
/// * Its code always executes in the root context, so it is stateful in a way that normal
/// libraries cannot replicate. This can be used to provide core services that would otherwise
/// not be possible to implement.
/// libraries cannot replicate. This can be used to provide core services that would otherwise
/// not be possible to implement.
///
/// * The procedures exported from the kernel may be the target of the `syscall` instruction,
/// and in fact _must_ be called that way.
/// and in fact _must_ be called that way.
///
/// * Kernels may not use `syscall` or `call` instructions internally.
Kernel = 2,
Expand Down Expand Up @@ -294,7 +294,7 @@ impl Module {
///
/// * The module was constructed in-memory via AST structures, and not derived from source code.
/// * The module was serialized without debug info, and then deserialized. Without debug info,
/// the source code is lost when round-tripping through serialization.
/// the source code is lost when round-tripping through serialization.
pub fn source_file(&self) -> Option<Arc<SourceFile>> {
self.source_file.clone()
}
Expand Down
21 changes: 11 additions & 10 deletions assembly/src/ast/visit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,16 +22,15 @@
//! of the visitor, but here are some examples:
//!
//! 1. When implementing a visitor that performs constant folding/propagation, you need to visit the
//! operands of an expression before the operator, in order to determine whether it is possible to
//! fold, and if so, what the actual values of the operands are. As a result, this is implemented as
//! a postorder visitor, so that the AST node corresponding to the expression is rewritten after all
//! of it's children.
//! operands of an expression before the operator, in order to determine whether it is possible
//! to fold, and if so, what the actual values of the operands are. As a result, this is
//! implemented as a postorder visitor, so that the AST node corresponding to the expression is
//! rewritten after all of it's children.
//!
//! 2. When implementing an analysis based on lexical scope, it is necessary to "push down" context
//! from
//! the root to the leaves of the AST - the context being the contents of each AST nodes inherited
//! scope. As a result, this is implemented as a preorder traversal, so that the context at each
//! node can be computed before visiting the children of that node.
//! from the root to the leaves of the AST - the context being the contents of each AST nodes
//! inherited scope. As a result, this is implemented as a preorder traversal, so that the
//! context at each node can be computed before visiting the children of that node.
//!
//! In both cases, the implementor must call the free function corresponding to the _current_ AST
//! node at the appropriate point (i.e. before/after executing the logic for the node), so that the
Expand Down Expand Up @@ -295,7 +294,8 @@ where
| AssertzWithError(ref code)
| U32AssertWithError(ref code)
| U32Assert2WithError(ref code)
| U32AssertWWithError(ref code) => visitor.visit_immediate_error_code(code),
| U32AssertWWithError(ref code)
| MTreeVerifyWithError(ref code) => visitor.visit_immediate_error_code(code),
AddImm(ref imm) | SubImm(ref imm) | MulImm(ref imm) | DivImm(ref imm) | ExpImm(ref imm)
| EqImm(ref imm) | NeqImm(ref imm) | Push(ref imm) => visitor.visit_immediate_felt(imm),
U32WrappingAddImm(ref imm)
Expand Down Expand Up @@ -734,7 +734,8 @@ where
| AssertzWithError(ref mut code)
| U32AssertWithError(ref mut code)
| U32Assert2WithError(ref mut code)
| U32AssertWWithError(ref mut code) => visitor.visit_mut_immediate_error_code(code),
| U32AssertWWithError(ref mut code)
| MTreeVerifyWithError(ref mut code) => visitor.visit_mut_immediate_error_code(code),
AddImm(ref mut imm) | SubImm(ref mut imm) | MulImm(ref mut imm) | DivImm(ref mut imm)
| ExpImm(ref mut imm) | EqImm(ref mut imm) | NeqImm(ref mut imm) | Push(ref mut imm) => {
visitor.visit_mut_immediate_felt(imm)
Expand Down
Loading

0 comments on commit 02d153f

Please sign in to comment.