From 0e2d4c4bc52a54330a143a28edab8ae458f327e0 Mon Sep 17 00:00:00 2001 From: Philippe Laferriere Date: Wed, 18 Sep 2024 10:46:29 -0400 Subject: [PATCH] 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 2473def1d..f0a834258 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 79092a1b0..5abffe732 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 c679d36ac..7fb90cab2 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 cbed7eb25..1bb1c7afa 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 d3236c594..4067c41da 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 96acf4104..08df6dfd9 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 57d937a35..d60e186db 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 0ae5de84e..6bcc801fb 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]