From 9a1c34ffb210a796f7fee19dcab9e24aa6785457 Mon Sep 17 00:00:00 2001 From: Philippe Laferriere Date: Fri, 13 Sep 2024 14:50:22 -0400 Subject: [PATCH 1/4] feat: introduce `Emit` instruction --- CHANGELOG.md | 1 + air/src/constraints/stack/op_flags/mod.rs | 1 + air/src/constraints/stack/op_flags/tests.rs | 5 ++- assembly/src/assembler/tests.rs | 37 +++++++++++++++++++ core/src/mast/serialization/tests.rs | 2 + core/src/operations/mod.rs | 26 +++++++++++-- docs/src/design/stack/io_ops.md | 2 +- docs/src/design/stack/system_ops.md | 11 ++++++ miden/tests/integration/operations/sys_ops.rs | 9 +++++ .../src/decoder/aux_trace/op_group_table.rs | 23 +++++++----- processor/src/decoder/tests.rs | 10 ++--- processor/src/decoder/trace.rs | 2 + processor/src/operations/mod.rs | 1 + processor/src/operations/sys_ops.rs | 14 +++++++ 14 files changed, 124 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index db12ba0a1f..6182624323 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,7 @@ - Added `miden_core::utils::sync::racy_lock` module (#1463). - Updated `miden_core::utils` to re-export `std::sync::LazyLock` and `racy_lock::RacyLock as LazyLock` for std and no_std environments, respectively (#1463). - Made the undocumented behavior of the VM with regard to undefined behavior of u32 operations, stricter (#1480) +- Introduced the `Emit` instruction (#1496) #### Fixes diff --git a/air/src/constraints/stack/op_flags/mod.rs b/air/src/constraints/stack/op_flags/mod.rs index 7913ed6738..2473def1df 100644 --- a/air/src/constraints/stack/op_flags/mod.rs +++ b/air/src/constraints/stack/op_flags/mod.rs @@ -292,6 +292,7 @@ impl OpFlags { + degree5_op_flags[1] // MPVERIFY + degree5_op_flags[6] // SPAN + degree5_op_flags[7] // JOIN + + degree5_op_flags[10] // EMIT + degree4_op_flags[6] // RESPAN + degree4_op_flags[7] // HALT + degree4_op_flags[3] // CALL diff --git a/air/src/constraints/stack/op_flags/tests.rs b/air/src/constraints/stack/op_flags/tests.rs index bfbc594f0f..d4d9a469d0 100644 --- a/air/src/constraints/stack/op_flags/tests.rs +++ b/air/src/constraints/stack/op_flags/tests.rs @@ -144,7 +144,8 @@ fn degree_4_op_flags() { fn composite_flags() { // ------ no change 0 --------------------------------------------------------------------- - let op_no_change_0 = [Operation::MpVerify(0), Operation::Span, Operation::Halt]; + let op_no_change_0 = + [Operation::MpVerify(0), Operation::Span, Operation::Halt, Operation::Emit(42)]; for op in op_no_change_0 { // frame initialised with an op operation. let frame = generate_evaluation_frame(op.op_code().into()); @@ -168,7 +169,7 @@ fn composite_flags() { assert_eq!(op_flags.left_shift(), ZERO); assert_eq!(op_flags.top_binary(), ZERO); - if op == Operation::MpVerify(0) { + if op == Operation::MpVerify(0) || op == Operation::Emit(42) { assert_eq!(op_flags.control_flow(), ZERO); } else if op == Operation::Span || op == Operation::Halt { assert_eq!(op_flags.control_flow(), ONE); diff --git a/assembly/src/assembler/tests.rs b/assembly/src/assembler/tests.rs index 597b4826dc..cb45e88ca8 100644 --- a/assembly/src/assembler/tests.rs +++ b/assembly/src/assembler/tests.rs @@ -1,6 +1,9 @@ +use alloc::vec::Vec; + use pretty_assertions::assert_eq; use vm_core::{ assert_matches, + crypto::hash::RpoDigest, mast::{MastForest, MastNode}, Program, }; @@ -158,6 +161,40 @@ fn nested_blocks() -> Result<(), Report> { Ok(()) } +/// Ensures that the arguments of `emit` do indeed modify the digest of a basic block +#[test] +fn emit_instruction_digest() { + let context = TestContext::new(); + + let program_source = r#" + proc.foo + emit.1 + end + + proc.bar + emit.2 + end + + begin + # specific impl irrelevant + exec.foo + exec.bar + end + "#; + + let program = context.assemble(program_source).unwrap(); + + let procedure_digests: Vec = program.mast_forest().procedure_digests().collect(); + + // foo, bar and entrypoint + assert_eq!(3, procedure_digests.len()); + + // Ensure that foo, bar and entrypoint all have different digests + assert_ne!(procedure_digests[0], procedure_digests[1]); + assert_ne!(procedure_digests[0], procedure_digests[2]); + assert_ne!(procedure_digests[1], procedure_digests[2]); +} + /// Since `foo` and `bar` have the same body, we only expect them to be added once to the program. #[test] fn duplicate_procedure() { diff --git a/core/src/mast/serialization/tests.rs b/core/src/mast/serialization/tests.rs index f8ed98e953..4dbb27c92e 100644 --- a/core/src/mast/serialization/tests.rs +++ b/core/src/mast/serialization/tests.rs @@ -104,6 +104,7 @@ fn confirm_operation_and_decorator_structure() { Operation::MrUpdate => (), Operation::FriE2F4 => (), Operation::RCombBase => (), + Operation::Emit(_) => (), }; match Decorator::Event(0) { @@ -236,6 +237,7 @@ fn serialize_deserialize_all_nodes() { Operation::MrUpdate, Operation::FriE2F4, Operation::RCombBase, + Operation::Emit(42), ]; let num_operations = operations.len(); diff --git a/core/src/operations/mod.rs b/core/src/operations/mod.rs index 8a8770139e..cbed7eb258 100644 --- a/core/src/operations/mod.rs +++ b/core/src/operations/mod.rs @@ -109,6 +109,7 @@ pub(super) mod opcode_constants { pub const OPCODE_JOIN: u8 = 0b0101_0111; pub const OPCODE_DYN: u8 = 0b0101_1000; pub const OPCODE_RCOMBBASE: u8 = 0b0101_1001; + pub const OPCODE_EMIT: u8 = 0b0101_1010; pub const OPCODE_MRUPDATE: u8 = 0b0110_0000; pub const OPCODE_PUSH: u8 = 0b0110_0100; @@ -156,6 +157,16 @@ pub enum Operation { /// instruction. Clk = OPCODE_CLK, + /// Emits an event id (`u32` value) to the host. + /// + /// We interpret the event id as follows: + /// - 16 most significant bits identify the event source, + /// - 16 least significant bits identify the actual event. + /// + /// Similar to Noop, this operation does not change the state of user stack. The immediate + /// value affects the program MAST root computation. + Emit(u32) = OPCODE_EMIT, + // ----- flow control operations ------------------------------------------------------------- /// Marks the beginning of a join block. Join = OPCODE_JOIN, @@ -570,8 +581,9 @@ impl Operation { /// Returns an immediate value carried by this operation. pub fn imm_value(&self) -> Option { - match self { - Self::Push(imm) => Some(*imm), + match *self { + Self::Push(imm) => Some(imm), + Self::Emit(imm) => Some(imm.into()), _ => None, } } @@ -718,6 +730,8 @@ impl fmt::Display for Operation { Self::MStream => write!(f, "mstream"), Self::Pipe => write!(f, "pipe"), + Self::Emit(value) => write!(f, "emit({value})"), + // ----- cryptographic operations ----------------------------------------------------- Self::HPerm => write!(f, "hperm"), Self::MpVerify(err_code) => write!(f, "mpverify({err_code})"), @@ -737,9 +751,10 @@ impl Serializable for Operation { Operation::Assert(err_code) | Operation::MpVerify(err_code) | Operation::U32assert2(err_code) => { - err_code.to_le_bytes().write_into(target); + err_code.write_into(target); }, Operation::Push(value) => value.as_int().write_into(target), + Operation::Emit(value) => value.write_into(target), // Note: we explicitly write out all the operations so that whenever we make a // modification to the `Operation` enum, we get a compile error here. This @@ -947,6 +962,11 @@ impl Deserializable for Operation { Self::Push(value_felt) }, + OPCODE_EMIT => { + let value = source.read_u32()?; + + Self::Emit(value) + }, OPCODE_SYSCALL => Self::SysCall, OPCODE_CALL => Self::Call, OPCODE_END => Self::End, diff --git a/docs/src/design/stack/io_ops.md b/docs/src/design/stack/io_ops.md index 822d0fa831..96acf4104b 100644 --- a/docs/src/design/stack/io_ops.md +++ b/docs/src/design/stack/io_ops.md @@ -2,7 +2,7 @@ In this section we describe the AIR constraints for Miden VM input / output operations. These operations move values between the stack and other components of the VM such as program code (i.e., decoder), memory, and advice provider. ### PUSH -The `PUSH` operation pushes the provided immediate value onto the stack (i.e., sets the value of $s_0$ register). Currently, it is the only operation in Miden VM which carries an immediate value. The semantics of this operation are explained in the [decoder section](../decoder/main.html#handling-immediate-values). +The `PUSH` operation pushes the provided immediate value onto the stack non-deterministically (i.e., sets the value of $s_0$ register); it is the responsibility of the [Op Group Table](../decoder/main.md#op-group-table) to ensure that the correct value was pushed on the stack. Currently, it is the only operation in Miden VM which carries an immediate value. The semantics of this operation are explained in the [decoder section](../decoder/main.html#handling-immediate-values). The effect of this operation on the rest of the stack is: * **Right shift** starting from position $0$. diff --git a/docs/src/design/stack/system_ops.md b/docs/src/design/stack/system_ops.md index bebd639f23..becbbadae3 100644 --- a/docs/src/design/stack/system_ops.md +++ b/docs/src/design/stack/system_ops.md @@ -10,6 +10,17 @@ The `NOOP` operation does not impose any constraints besides the ones needed to s'_i - s_i = 0 \ \text{ for } i \in [0, 16) \text { | degree} = 1 $$ +## EMIT +Similarly to `NOOP`, the `EMIT` operation advances the cycle counter but does not change the state of the operand stack (i.e., the depth of the stack and the values on the stack remain the same). + +The `EMIT` operation does not impose any constraints besides the ones needed to ensure that the entire state of the stack is copied over. This constraint looks like so: + +>$$ +s'_i - s_i = 0 \ \text{ for } i \in [0, 16) \text { | degree} = 1 +$$ + +Additionally, the prover puts `EMIT`'s immediate value in the first user op helper register non-deterministically. The [Op Group Table](../decoder/main.md#op-group-table) is responsible for ensuring that the prover sets the appropriate value. + ## ASSERT The `ASSERT` operation pops an element off the stack and checks if the popped element is equal to $1$. If the element is not equal to $1$, program execution fails. diff --git a/miden/tests/integration/operations/sys_ops.rs b/miden/tests/integration/operations/sys_ops.rs index 366173d0fb..a0e4a081a0 100644 --- a/miden/tests/integration/operations/sys_ops.rs +++ b/miden/tests/integration/operations/sys_ops.rs @@ -81,3 +81,12 @@ fn assert_eq_fail() { } ); } + +// EMITTING EVENTS +// ================================================================================================ + +#[test] +fn emit() { + let test = build_op_test!("emit.42", &[0, 0, 0, 0]); + test.prove_and_verify(vec![], false); +} diff --git a/processor/src/decoder/aux_trace/op_group_table.rs b/processor/src/decoder/aux_trace/op_group_table.rs index c81e6510e4..5800a6b2e2 100644 --- a/processor/src/decoder/aux_trace/op_group_table.rs +++ b/processor/src/decoder/aux_trace/op_group_table.rs @@ -2,7 +2,7 @@ use miden_air::{ trace::decoder::{OP_BATCH_2_GROUPS, OP_BATCH_4_GROUPS, OP_BATCH_8_GROUPS}, RowIndex, }; -use vm_core::{OPCODE_PUSH, OPCODE_RESPAN, OPCODE_SPAN}; +use vm_core::{OPCODE_EMIT, OPCODE_PUSH, OPCODE_RESPAN, OPCODE_SPAN}; use super::{AuxColumnBuilder, Felt, FieldElement, MainTrace, ONE}; @@ -88,18 +88,23 @@ fn get_op_group_table_removal_multiplicand>( ) -> E { let group_count = main_trace.group_count(i); let block_id = main_trace.addr(i); + let group_value = { + let op_code = main_trace.get_op_code(i); - let op_code = main_trace.get_op_code(i); - let tmp = if op_code == Felt::from(OPCODE_PUSH) { - main_trace.stack_element(0, i + 1) - } else { - let h0 = main_trace.decoder_hasher_state_first_half(i + 1)[0]; + if op_code == Felt::from(OPCODE_PUSH) { + main_trace.stack_element(0, i + 1) + } else if op_code == Felt::from(OPCODE_EMIT) { + main_trace.helper_register(0, i) + } else { + let h0 = main_trace.decoder_hasher_state_first_half(i + 1)[0]; - let op_prime = main_trace.get_op_code(i + 1); - h0.mul_small(1 << 7) + op_prime + let op_prime = main_trace.get_op_code(i + 1); + h0.mul_small(1 << 7) + op_prime + } }; + alphas[0] + alphas[1].mul_base(block_id) + alphas[2].mul_base(group_count) - + alphas[3].mul_base(tmp) + + alphas[3].mul_base(group_value) } diff --git a/processor/src/decoder/tests.rs b/processor/src/decoder/tests.rs index 1f5d7b404a..8451faeccb 100644 --- a/processor/src/decoder/tests.rs +++ b/processor/src/decoder/tests.rs @@ -92,8 +92,7 @@ fn basic_block_one_group() { #[test] fn basic_block_small() { - let iv = [ONE, TWO]; - let ops = vec![Operation::Push(iv[0]), Operation::Push(iv[1]), Operation::Add]; + let ops = vec![Operation::Push(ONE), Operation::Emit(1), Operation::Add]; let basic_block = BasicBlockNode::new(ops.clone(), None).unwrap(); let program = { let mut mast_forest = MastForest::new(); @@ -109,8 +108,8 @@ fn basic_block_small() { // --- check block address, op_bits, group count, op_index, and in_span columns --------------- check_op_decoding(&trace, 0, ZERO, Operation::Span, 4, 0, 0); - check_op_decoding(&trace, 1, INIT_ADDR, Operation::Push(iv[0]), 3, 0, 1); - check_op_decoding(&trace, 2, INIT_ADDR, Operation::Push(iv[1]), 2, 1, 1); + check_op_decoding(&trace, 1, INIT_ADDR, Operation::Push(ONE), 3, 0, 1); + check_op_decoding(&trace, 2, INIT_ADDR, Operation::Emit(1), 2, 1, 1); check_op_decoding(&trace, 3, INIT_ADDR, Operation::Add, 1, 2, 1); // starting new group: NOOP group is inserted by the processor to make sure number of groups // is a power of two @@ -125,7 +124,8 @@ fn basic_block_small() { vec![ basic_block.op_batches()[0].groups().to_vec(), vec![build_op_group(&ops[1..])], - vec![build_op_group(&ops[2..])], + // emit(1) + vec![build_op_group(&ops[2..]), ZERO, ONE], vec![], vec![], program_hash.to_vec(), // last row should contain program hash diff --git a/processor/src/decoder/trace.rs b/processor/src/decoder/trace.rs index a815395375..6842c504e3 100644 --- a/processor/src/decoder/trace.rs +++ b/processor/src/decoder/trace.rs @@ -299,6 +299,8 @@ impl DecoderTrace { self.hasher_trace[0].push(group_ops_left); self.hasher_trace[1].push(parent_addr); + // Note: use `Decoder::set_user_op_helpers()` when processing an instruction to set any of + // these values to something other than 0 for idx in USER_OP_HELPERS { self.hasher_trace[idx].push(ZERO); } diff --git a/processor/src/operations/mod.rs b/processor/src/operations/mod.rs index a3b7af5880..6c1b98268c 100644 --- a/processor/src/operations/mod.rs +++ b/processor/src/operations/mod.rs @@ -41,6 +41,7 @@ where Operation::Caller => self.op_caller()?, Operation::Clk => self.op_clk()?, + Operation::Emit(event_id) => self.op_emit(event_id)?, // ----- flow control operations ------------------------------------------------------ // control flow operations are never executed directly diff --git a/processor/src/operations/sys_ops.rs b/processor/src/operations/sys_ops.rs index 046c86f748..8e2606887e 100644 --- a/processor/src/operations/sys_ops.rs +++ b/processor/src/operations/sys_ops.rs @@ -1,3 +1,5 @@ +use vm_core::Operation; + use super::{ super::{ system::{FMP_MAX, FMP_MIN}, @@ -108,6 +110,18 @@ where self.stack.shift_right(0); Ok(()) } + + // EVENTS + // -------------------------------------------------------------------------------------------- + + /// Forwards the emitted event id to the host. + pub(super) fn op_emit(&mut self, event_id: u32) -> Result<(), ExecutionError> { + self.stack.copy_state(0); + self.decoder.set_user_op_helpers(Operation::Emit(event_id), &[event_id.into()]); + self.host.borrow_mut().on_event(self, event_id)?; + + Ok(()) + } } // TESTS From 0b1c2f6225ffad38a0e56c1ce197ffa238c239c0 Mon Sep 17 00:00:00 2001 From: Philippe Laferriere Date: Fri, 13 Sep 2024 15:02:57 -0400 Subject: [PATCH 2/4] feat: remove `Decorator::Event` --- assembly/src/assembler/instruction/mod.rs | 2 +- core/src/mast/node/basic_block_node/tests.rs | 10 +++++----- core/src/mast/serialization/decorator.rs | 9 +-------- core/src/mast/serialization/tests.rs | 4 +--- core/src/operations/decorators/mod.rs | 4 ---- processor/src/lib.rs | 3 --- 6 files changed, 8 insertions(+), 24 deletions(-) diff --git a/assembly/src/assembler/instruction/mod.rs b/assembly/src/assembler/instruction/mod.rs index 28d532c8bc..49e8bec164 100644 --- a/assembly/src/assembler/instruction/mod.rs +++ b/assembly/src/assembler/instruction/mod.rs @@ -432,7 +432,7 @@ impl Assembler { // ----- emit instruction ------------------------------------------------------------- Instruction::Emit(event_id) => { - block_builder.push_decorator(Decorator::Event(event_id.expect_value()))?; + block_builder.push_op(Operation::Emit(event_id.expect_value())); }, // ----- trace instruction ------------------------------------------------------------ diff --git a/core/src/mast/node/basic_block_node/tests.rs b/core/src/mast/node/basic_block_node/tests.rs index dd3f56269c..607793642c 100644 --- a/core/src/mast/node/basic_block_node/tests.rs +++ b/core/src/mast/node/basic_block_node/tests.rs @@ -300,11 +300,11 @@ fn operation_or_decorator_iterator() { // Note: there are 2 decorators after the last instruction let decorators = vec![ - (0, Decorator::Event(0)), // ID: 0 - (0, Decorator::Event(1)), // ID: 1 - (3, Decorator::Event(2)), // ID: 2 - (4, Decorator::Event(3)), // ID: 3 - (4, Decorator::Event(4)), // ID: 4 + (0, Decorator::Trace(0)), // ID: 0 + (0, Decorator::Trace(1)), // ID: 1 + (3, Decorator::Trace(2)), // ID: 2 + (4, Decorator::Trace(3)), // ID: 3 + (4, Decorator::Trace(4)), // ID: 4 ]; let node = diff --git a/core/src/mast/serialization/decorator.rs b/core/src/mast/serialization/decorator.rs index 8638d712e7..a8b2041e3c 100644 --- a/core/src/mast/serialization/decorator.rs +++ b/core/src/mast/serialization/decorator.rs @@ -178,11 +178,6 @@ impl DecoratorInfo { Ok(Decorator::Debug(DebugOptions::LocalInterval(start, second, end))) }, - EncodedDecoratorVariant::Event => { - let value = data_reader.read_u32()?; - - Ok(Decorator::Event(value)) - }, EncodedDecoratorVariant::Trace => { let value = data_reader.read_u32()?; @@ -245,7 +240,6 @@ pub enum EncodedDecoratorVariant { DebugOptionsMemAll, DebugOptionsMemInterval, DebugOptionsLocalInterval, - Event, Trace, } @@ -298,7 +292,6 @@ impl From<&Decorator> for EncodedDecoratorVariant { DebugOptions::MemInterval(..) => Self::DebugOptionsMemInterval, DebugOptions::LocalInterval(..) => Self::DebugOptionsLocalInterval, }, - Decorator::Event(_) => Self::Event, Decorator::Trace(_) => Self::Trace, } } @@ -432,7 +425,7 @@ impl DecoratorDataBuilder { }, DebugOptions::StackAll | DebugOptions::MemAll => None, }, - Decorator::Event(value) | Decorator::Trace(value) => { + Decorator::Trace(value) => { self.decorator_data.extend(value.to_le_bytes()); Some(data_offset) diff --git a/core/src/mast/serialization/tests.rs b/core/src/mast/serialization/tests.rs index 4dbb27c92e..c76a3ff3ac 100644 --- a/core/src/mast/serialization/tests.rs +++ b/core/src/mast/serialization/tests.rs @@ -107,7 +107,7 @@ fn confirm_operation_and_decorator_structure() { Operation::Emit(_) => (), }; - match Decorator::Event(0) { + match Decorator::Trace(0) { Decorator::Advice(advice) => match advice { AdviceInjector::MerkleNodeMerge => (), AdviceInjector::MerkleNodeToStack => (), @@ -137,7 +137,6 @@ fn confirm_operation_and_decorator_structure() { DebugOptions::MemInterval(..) => (), DebugOptions::LocalInterval(..) => (), }, - Decorator::Event(_) => (), Decorator::Trace(_) => (), }; } @@ -290,7 +289,6 @@ fn serialize_deserialize_all_nodes() { (15, Decorator::Debug(DebugOptions::MemAll)), (15, Decorator::Debug(DebugOptions::MemInterval(0, 16))), (17, Decorator::Debug(DebugOptions::LocalInterval(1, 2, 3))), - (num_operations, Decorator::Event(45)), (num_operations, Decorator::Trace(55)), ]; diff --git a/core/src/operations/decorators/mod.rs b/core/src/operations/decorators/mod.rs index 4122d26026..ecfac643df 100644 --- a/core/src/operations/decorators/mod.rs +++ b/core/src/operations/decorators/mod.rs @@ -35,8 +35,6 @@ pub enum Decorator { /// Prints out information about the state of the VM based on the specified options. This /// decorator is executed only in debug mode. Debug(DebugOptions), - /// Emits an event to the host. - Event(u32), /// Emits a trace to the host. Trace(u32), } @@ -60,7 +58,6 @@ impl Decorator { Blake3_256::hash(&bytes_to_hash) }, Self::Debug(debug) => Blake3_256::hash(debug.to_string().as_bytes()), - Self::Event(event) => Blake3_256::hash(&event.to_le_bytes()), Self::Trace(trace) => Blake3_256::hash(&trace.to_le_bytes()), } } @@ -80,7 +77,6 @@ impl fmt::Display for Decorator { write!(f, "asmOp({}, {})", assembly_op.op(), assembly_op.num_cycles()) }, Self::Debug(options) => write!(f, "debug({options})"), - Self::Event(event_id) => write!(f, "event({})", event_id), Self::Trace(trace_id) => write!(f, "trace({})", trace_id), } } diff --git a/processor/src/lib.rs b/processor/src/lib.rs index 398219c8f8..0ec4dad086 100644 --- a/processor/src/lib.rs +++ b/processor/src/lib.rs @@ -591,9 +591,6 @@ where self.decoder.append_asmop(self.system.clk(), assembly_op.clone()); } }, - Decorator::Event(id) => { - self.host.borrow_mut().on_event(self, *id)?; - }, Decorator::Trace(id) => { if self.enable_tracing { self.host.borrow_mut().on_trace(self, *id)?; From 354052bab8eb081feb590962aa032b2dd7a3320e Mon Sep 17 00:00:00 2001 From: Philippe Laferriere Date: Tue, 17 Sep 2024 12:42:17 -0400 Subject: [PATCH 3/4] docs: fix docs after adding emit instruction --- docs/src/design/decoder/constraints.md | 26 ++++++++++++------------- docs/src/design/stack/op_constraints.md | 10 ++++++++++ 2 files changed, 23 insertions(+), 13 deletions(-) diff --git a/docs/src/design/decoder/constraints.md b/docs/src/design/decoder/constraints.md index 63e2ec3588..d3236c5942 100644 --- a/docs/src/design/decoder/constraints.md +++ b/docs/src/design/decoder/constraints.md @@ -422,18 +422,18 @@ Inside a *span* block, group count can either stay the same or decrease by one: sp \cdot \Delta gc \cdot (\Delta gc - 1) = 0 \text{ | degree} = 3 $$ -When group count is decremented inside a *span* block, either $h_0$ must be $0$ (we consumed all operations in a group) or we must be executing `PUSH` operation: +When group count is decremented inside a *span* block, either $h_0$ must be $0$ (we consumed all operations in a group) or we must be executing an operation with an immediate value: > $$ -sp \cdot \Delta gc \cdot (1 - f_{push})\cdot h_0 = 0 \text{ | degree} = 7 +sp \cdot \Delta gc \cdot (1 - f_{imm})\cdot h_0 = 0 \text{ | degree} = 8 $$ -Notice that the above constraint does not preclude $f_{push} = 1$ and $h_0 = 0$ from being true at the same time. If this happens, op group decoding constraints (described [here](#op-group-decoding-constraints)) will force that the operation following the `PUSH` operation is a `NOOP`. +Notice that the above constraint does not preclude $f_{imm} = 1$ and $h_0 = 0$ from being true at the same time. If this happens, op group decoding constraints (described [here](#op-group-decoding-constraints)) will force that the operation following the operation with an immediate value is a `NOOP`. -When executing a `SPAN`, a `RESPAN`, or a `PUSH` operation, group count must be decremented by $1$: +When executing a `SPAN`, a `RESPAN`, or an operation with an immediate value, group count must be decremented by $1$: > $$ -(f_{span} + f_{respan} + f_{push}) \cdot (\Delta gc - 1) = 0 \text{ | degree} = 6 +(f_{span} + f_{respan} + f_{imm}) \cdot (\Delta gc - 1) = 0 \text{ | degree} = 6 $$ If the next operation is either an `END` or a `RESPAN`, group count must remain the same: @@ -467,17 +467,17 @@ op = \sum_{i=0}^6 (b_i \cdot 2^i) \\ f_{sgc} = sp \cdot sp' \cdot (1 - \Delta gc) $$ -$op$ is just an opcode value implied by the values in `op_bits` registers. $f_{sgc}$ is a flag which is set to $1$ when the group count within a *span* block does not change. We multiply it by $sp'$ to make sure the flag is $0$ when we are about to end decoding of an operation batch. Note that $f_{sgc}$ flag is mutually exclusive with $f_{span}$, $f_{respan}$, and $f_{push}$ flags as these three operations decrement the group count. +$op$ is just an opcode value implied by the values in `op_bits` registers. $f_{sgc}$ is a flag which is set to $1$ when the group count within a *span* block does not change. We multiply it by $sp'$ to make sure the flag is $0$ when we are about to end decoding of an operation batch. Note that $f_{sgc}$ flag is mutually exclusive with $f_{span}$, $f_{respan}$, and $f_{imm}$ flags as these three operations decrement the group count. Using these variables, we can describe operation group decoding constraints as follows: -When a `SPAN`, a `RESPAN`, or a `PUSH` operation is executed or when the group count does not change, the value in $h_0$ should be decremented by the value of the opcode in the next row. +When a `SPAN`, a `RESPAN`, or an operation with an immediate value is executed or when the group count does not change, the value in $h_0$ should be decremented by the value of the opcode in the next row. > $$ -(f_{span} + f_{respan} + f_{push} + f_{sgc}) \cdot (h_0 - h_0' \cdot 2^7 - op') = 0 \text{ | degree} = 6 +(f_{span} + f_{respan} + f_{imm} + f_{sgc}) \cdot (h_0 - h_0' \cdot 2^7 - op') = 0 \text{ | degree} = 6 $$ -Notice that when the group count does change, and we are not executing $f_{span}$, $f_{respan}$, or $f_{push}$ operations, no constraints are placed against $h_0$, and thus, the prover can populate this register non-deterministically. +Notice that when the group count does change, and we are not executing $f_{span}$, $f_{respan}$, or $f_{imm}$ operations, no constraints are placed against $h_0$, and thus, the prover can populate this register non-deterministically. When we are in a *span* block and the next operation is `END` or `RESPAN`, the current value in $h_0$ column must be $0$. @@ -491,11 +491,11 @@ The `op_index` column (denoted as $ox$) tracks index of an operation within its To simplify the description of the constraints, we will define the following variables: $$ -ng = \Delta gc - f_{push} \\ +ng = \Delta gc - f_{imm} \\ \Delta ox = ox' - ox $$ -The value of $ng$ is set to $1$ when we are about to start executing a new operation group (i.e., group count is decremented but we did not execute a `PUSH` operation). Using these variables, we can describe the constraints against the $ox$ column as follows. +The value of $ng$ is set to $1$ when we are about to start executing a new operation group (i.e., group count is decremented but we did not execute an operation with an immediate value). Using these variables, we can describe the constraints against the $ox$ column as follows. When executing `SPAN` or `RESPAN` operations the next value of `op_index` must be set to $0$: @@ -590,10 +590,10 @@ Where $i \in [1, 8)$. Thus, $v_1$ defines row value for group in $h_1$, $v_2$ de We compute the value of the row to be removed from the op group table as follows: $$ -u = \alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot gc + \alpha_3 \cdot ((h_0' \cdot 2^7 + op') \cdot (1 - f_{push}) + s_0' \cdot f_{push}) \text{ | degree} = 5 +u = \alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot gc + \alpha_3 \cdot ((h_0' \cdot 2^7 + op') \cdot (1 - f_{imm}) + s_0' \cdot f_{push} + h_2 \cdot f_{emit}) \text{ | degree} = 6 $$ -In the above, the value of the group is computed as $(h_0' \cdot 2^7 + op') \cdot (1 - f_{push}) + s_0' \cdot f_{push}$. This basically says that when we execute a `PUSH` operation we need to remove the immediate value from the table. This value is at the top of the stack (column $s_0$) in the next row. However, when we are not executing a `PUSH` operation, the value to be removed is an op group value which is a combination of values in $h_0$ and `op_bits` columns (also in the next row). Note also that value for batch address comes from the current value in the block address column ($a$), and the group position comes from the current value of the group count column ($gc$). +In the above, the value of the group is computed as $(h_0' \cdot 2^7 + op') \cdot (1 - f_{push}) + s_0' \cdot f_{push} + h_2 \cdot f_{emit}$. This basically says that when we execute a `PUSH` or `EMIT` operation we need to remove the immediate value from the table. For `PUSH`, this value is at the top of the stack (column $s_0$) in the next row; for `EMIT`, it is found in $h_2$. However, when we are executing neither a `PUSH` nor `EMIT` operation, the value to be removed is an op group value which is a combination of values in $h_0$ and `op_bits` columns (also in the next row). Note also that value for batch address comes from the current value in the block address column ($a$), and the group position comes from the current value of the group count column ($gc$). We also define a flag which is set to $1$ when a group needs to be removed from the op group table. diff --git a/docs/src/design/stack/op_constraints.md b/docs/src/design/stack/op_constraints.md index f4502b2daa..57d937a359 100644 --- a/docs/src/design/stack/op_constraints.md +++ b/docs/src/design/stack/op_constraints.md @@ -294,3 +294,13 @@ $$ $$ f_{ctrl} = f_{span,join,split,loop} + f_{end,repeat,respan,halt} + f_{dyn} + f_{call} + f_{syscall} \text{ | degree} = 5 $$ + +### Immediate value flag + +The immediate value flag $f_{imm}$ is set to 1 when an operation has an immediate value, and 0 otherwise: + +$$ +f_{imm} = f_{push} + f_{emit} \text{ | degree} = 5 +$$ + +Note that the `ASSERT`, `MPVERIFY` and other operations have immediate values too. However, these immediate values are not included in the MAST digest, and hence are not considered for the $f_{imm}$ flag. From 0e2d4c4bc52a54330a143a28edab8ae458f327e0 Mon Sep 17 00:00:00 2001 From: Philippe Laferriere Date: Wed, 18 Sep 2024 10:46:29 -0400 Subject: [PATCH 4/4] fix: move push instruction to degree 5 flags --- air/src/constraints/stack/op_flags/mod.rs | 8 ++++---- air/src/trace/main_trace.rs | 4 ++-- assembly/src/tests.rs | 2 +- core/src/operations/mod.rs | 3 ++- docs/src/design/decoder/constraints.md | 9 +++++---- docs/src/design/stack/io_ops.md | 2 +- docs/src/design/stack/op_constraints.md | 8 ++++---- miden/tests/integration/flow_control/mod.rs | 12 ++++++------ 8 files changed, 25 insertions(+), 23 deletions(-) diff --git a/air/src/constraints/stack/op_flags/mod.rs b/air/src/constraints/stack/op_flags/mod.rs index 2473def1df..f0a8342583 100644 --- a/air/src/constraints/stack/op_flags/mod.rs +++ b/air/src/constraints/stack/op_flags/mod.rs @@ -267,7 +267,7 @@ impl OpFlags { // degree 6 flags do not use the first two bits (op_bits[0], op_bits[1]) degree4_op_flags[0] = not_2_not_3; // MRUPDATE - degree4_op_flags[1] = yes_2_not_3; // PUSH + degree4_op_flags[1] = yes_2_not_3; // (unused) degree4_op_flags[2] = not_2_yes_3; // SYSCALL degree4_op_flags[3] = yes_2_yes_3; // CALL @@ -376,7 +376,7 @@ impl OpFlags { + degree7_op_flags[22] + degree7_op_flags[26]; - right_shift_flags[0] = f011 + degree4_op_flags[1] + movupn_flag; + right_shift_flags[0] = f011 + degree5_op_flags[11] + movupn_flag; // degree 5: PUSH right_shift_flags[1] = right_shift_flags[0] + degree6_op_flags[4]; // degree 6: U32SPLIT @@ -396,7 +396,7 @@ impl OpFlags { right_shift_flags[15] = right_shift_flags[8]; // Flag if the stack has been shifted to the right. - let right_shift = f011 + degree4_op_flags[1] + degree6_op_flags[4]; // PUSH; U32SPLIT + let right_shift = f011 + degree5_op_flags[11] + degree6_op_flags[4]; // PUSH; U32SPLIT // Flag if the stack has been shifted to the left. let left_shift = @@ -908,7 +908,7 @@ impl OpFlags { /// Operation Flag of PUSH operation. #[inline(always)] pub fn push(&self) -> E { - self.degree4_op_flags[get_op_index(Operation::Push(ONE).op_code())] + self.degree5_op_flags[get_op_index(Operation::Push(ONE).op_code())] } /// Operation Flag of CALL operation. diff --git a/air/src/trace/main_trace.rs b/air/src/trace/main_trace.rs index 79092a1b06..5abffe7327 100644 --- a/air/src/trace/main_trace.rs +++ b/air/src/trace/main_trace.rs @@ -259,8 +259,8 @@ impl MainTrace { [b6, b5, b4] == [ZERO, ONE, ONE]|| // u32SPLIT 100_1000 ([b6, b5, b4, b3, b2, b1, b0] == [ONE, ZERO, ZERO, ONE, ZERO, ZERO, ZERO]) || - // PUSH i.e., 110_0100 - ([b6, b5, b4, b3, b2, b1, b0] == [ONE, ONE, ZERO, ZERO, ONE, ZERO, ZERO]) + // PUSH i.e., 101_1011 + ([b6, b5, b4, b3, b2, b1, b0] == [ONE, ZERO, ONE, ONE, ZERO, ONE, ONE]) } // STACK COLUMNS diff --git a/assembly/src/tests.rs b/assembly/src/tests.rs index c679d36ac1..7fb90cab29 100644 --- a/assembly/src/tests.rs +++ b/assembly/src/tests.rs @@ -1180,7 +1180,7 @@ fn decorators_external() -> TestResult { let expected = "\ begin trace(0) - external.0x178d0a56b911f3eb23bbf18fb9f130130ba0c5d321e420610f64bb41790ca070 + external.0xe776df8dc02329acc43a09fe8e510b44a87dfd876e375ad383891470ece4f6de trace(1) end"; let program = Assembler::new(context.source_manager()) diff --git a/core/src/operations/mod.rs b/core/src/operations/mod.rs index cbed7eb258..1bb1c7afad 100644 --- a/core/src/operations/mod.rs +++ b/core/src/operations/mod.rs @@ -110,9 +110,10 @@ pub(super) mod opcode_constants { pub const OPCODE_DYN: u8 = 0b0101_1000; pub const OPCODE_RCOMBBASE: u8 = 0b0101_1001; pub const OPCODE_EMIT: u8 = 0b0101_1010; + pub const OPCODE_PUSH: u8 = 0b0101_1011; pub const OPCODE_MRUPDATE: u8 = 0b0110_0000; - pub const OPCODE_PUSH: u8 = 0b0110_0100; + /* unused: 0b0110_0100 */ pub const OPCODE_SYSCALL: u8 = 0b0110_1000; pub const OPCODE_CALL: u8 = 0b0110_1100; pub const OPCODE_END: u8 = 0b0111_0000; diff --git a/docs/src/design/decoder/constraints.md b/docs/src/design/decoder/constraints.md index d3236c5942..4067c41da1 100644 --- a/docs/src/design/decoder/constraints.md +++ b/docs/src/design/decoder/constraints.md @@ -23,7 +23,8 @@ AIR constraints for the decoder involve operations listed in the table below. Fo | `SYSCALL` | $f_{syscall}$ | 4 | Stack remains unchanged. | | `END` | $f_{end}$ | 4 | When exiting a loop block, top stack element is dropped; otherwise, the stack remains unchanged. | | `HALT` | $f_{halt}$ | 4 | Stack remains unchanged. | -| `PUSH` | $f_{push}$ | 4 | An immediate value is pushed onto the stack. | +| `PUSH` | $f_{push}$ | 5 | An immediate value is pushed onto the stack. | +| `EMIT` | $f_{emit}$ | 5 | Stack remains unchanged. | We also use the [control flow flag](../stack/op_constraints.md#control-flow-flag) $f_{ctrl}$ exposed by the VM, which is set when any one of the above control flow operations is being executed. It has degree $5$. @@ -404,9 +405,9 @@ In the beginning of a span block (i.e., when `SPAN` operation is executed), the The rules for decrementing values in the $gc$ column are as follows: * The count cannot be decremented by more than $1$ in a single row. * When an operation group is fully executed (which happens when $h_0 = 0$ inside a span block), the count is decremented by $1$. -* When `SPAN`, `RESPAN`, or `PUSH` operations are executed, the count is decremented by $1$. +* When `SPAN`, `RESPAN`, `EMIT` or `PUSH` operations are executed, the count is decremented by $1$. -Note that these rules imply that `PUSH` operation cannot be the last operation in an operation group (otherwise the count would have to be decremented by $2$). +Note that these rules imply that the `EMIT` and `PUSH` operations cannot be the last operation in an operation group (otherwise the count would have to be decremented by $2$). To simplify the description of the constraints, we will define the following variable: @@ -425,7 +426,7 @@ $$ When group count is decremented inside a *span* block, either $h_0$ must be $0$ (we consumed all operations in a group) or we must be executing an operation with an immediate value: > $$ -sp \cdot \Delta gc \cdot (1 - f_{imm})\cdot h_0 = 0 \text{ | degree} = 8 +sp \cdot \Delta gc \cdot (1 - f_{imm})\cdot h_0 = 0 \text{ | degree} = 7 $$ Notice that the above constraint does not preclude $f_{imm} = 1$ and $h_0 = 0$ from being true at the same time. If this happens, op group decoding constraints (described [here](#op-group-decoding-constraints)) will force that the operation following the operation with an immediate value is a `NOOP`. diff --git a/docs/src/design/stack/io_ops.md b/docs/src/design/stack/io_ops.md index 96acf4104b..08df6dfd93 100644 --- a/docs/src/design/stack/io_ops.md +++ b/docs/src/design/stack/io_ops.md @@ -2,7 +2,7 @@ In this section we describe the AIR constraints for Miden VM input / output operations. These operations move values between the stack and other components of the VM such as program code (i.e., decoder), memory, and advice provider. ### PUSH -The `PUSH` operation pushes the provided immediate value onto the stack non-deterministically (i.e., sets the value of $s_0$ register); it is the responsibility of the [Op Group Table](../decoder/main.md#op-group-table) to ensure that the correct value was pushed on the stack. Currently, it is the only operation in Miden VM which carries an immediate value. The semantics of this operation are explained in the [decoder section](../decoder/main.html#handling-immediate-values). +The `PUSH` operation pushes the provided immediate value onto the stack non-deterministically (i.e., sets the value of $s_0$ register); it is the responsibility of the [Op Group Table](../decoder/main.md#op-group-table) to ensure that the correct value was pushed on the stack. The semantics of this operation are explained in the [decoder section](../decoder/main.html#handling-immediate-values). The effect of this operation on the rest of the stack is: * **Right shift** starting from position $0$. diff --git a/docs/src/design/stack/op_constraints.md b/docs/src/design/stack/op_constraints.md index 57d937a359..d60e186dbb 100644 --- a/docs/src/design/stack/op_constraints.md +++ b/docs/src/design/stack/op_constraints.md @@ -189,8 +189,8 @@ This group contains operations which require constraints with degree up to $3$. | `JOIN` | $87$ | `101_0111` | [Flow control ops](../decoder/main.md) | $5$ | | `DYN` | $88$ | `101_1000` | [Flow control ops](../decoder/main.md) | $5$ | | `RCOMBBASE` | $89$ | `101_1001` | [Crypto ops](./crypto_ops.md) | $5$ | -| `` | $90$ | `101_1010` | | $5$ | -| `` | $91$ | `101_1011` | | $5$ | +| `EMIT` | $90$ | `101_1010` | [System ops](./system_ops.md) | $5$ | +| `PUSH` | $91$ | `101_1011` | [I/O ops](./io_ops.md) | $5$ | | `` | $92$ | `101_1100` | | $5$ | | `` | $93$ | `101_1101` | | $5$ | | `` | $94$ | `101_1110` | | $5$ | @@ -211,7 +211,7 @@ This group contains operations which require constraints with degree up to $5$. | Operation | Opcode value | Binary encoding | Operation group | Flag degree | | ------------ | :----------: | :-------------: | :-------------------------------------:| :---------: | | `MRUPDATE` | $96$ | `110_0000` | [Crypto ops](./crypto_ops.md) | $4$ | -| `PUSH` | $100$ | `110_0100` | [I/O ops](./io_ops.md) | $4$ | +| `` | $100$ | `110_0100` | | $4$ | | `SYSCALL` | $104$ | `110_1000` | [Flow control ops](../decoder/main.md) | $4$ | | `CALL` | $108$ | `110_1100` | [Flow control ops](../decoder/main.md) | $4$ | | `END` | $112$ | `111_0000` | [Flow control ops](../decoder/main.md) | $4$ | @@ -300,7 +300,7 @@ $$ The immediate value flag $f_{imm}$ is set to 1 when an operation has an immediate value, and 0 otherwise: $$ -f_{imm} = f_{push} + f_{emit} \text{ | degree} = 5 +f_{imm} = f_{push} + f_{emit} \text{ | degree} = 4 $$ Note that the `ASSERT`, `MPVERIFY` and other operations have immediate values too. However, these immediate values are not included in the MAST digest, and hence are not considered for the $f_{imm}$ flag. diff --git a/miden/tests/integration/flow_control/mod.rs b/miden/tests/integration/flow_control/mod.rs index 0ae5de84e1..6bcc801fbf 100644 --- a/miden/tests/integration/flow_control/mod.rs +++ b/miden/tests/integration/flow_control/mod.rs @@ -347,12 +347,12 @@ fn simple_dyncall() { dyncall end"; - // The hash of foo can be obtained from the code block table by: - // let program = test.compile(); - // let cb_table = program.cb_table(); - // Result: - // [BaseElement(3961142802598954486), BaseElement(5305628994393606376), - // BaseElement(7971171833137344204), BaseElement(10465350313512331391)] + // The hash of foo can be obtained with: + // let context = TestContext::new(); + // let program = context.assemble(program_source).unwrap(); + // let procedure_digests: Vec = program.mast_forest().procedure_digests().collect(); + // let foo_digest = procedure_digests[0]; + // // Integer values can be obtained via Felt::from_mont(14592192105906586403).as_int(), etc. // As ints: // [8324248212344458853, 17691992706129158519, 18131640149172243086, 16129275750103409835]