Skip to content

Commit

Permalink
fix: move push instruction to degree 5 flags
Browse files Browse the repository at this point in the history
  • Loading branch information
plafer committed Sep 18, 2024
1 parent 354052b commit 0e2d4c4
Show file tree
Hide file tree
Showing 8 changed files with 25 additions and 23 deletions.
8 changes: 4 additions & 4 deletions air/src/constraints/stack/op_flags/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -267,7 +267,7 @@ impl<E: FieldElement> OpFlags<E> {

// 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

Expand Down Expand Up @@ -376,7 +376,7 @@ impl<E: FieldElement> OpFlags<E> {
+ 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

Expand All @@ -396,7 +396,7 @@ impl<E: FieldElement> OpFlags<E> {
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 =
Expand Down Expand Up @@ -908,7 +908,7 @@ impl<E: FieldElement> OpFlags<E> {
/// 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.
Expand Down
4 changes: 2 additions & 2 deletions air/src/trace/main_trace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion assembly/src/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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())
Expand Down
3 changes: 2 additions & 1 deletion core/src/operations/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
9 changes: 5 additions & 4 deletions docs/src/design/decoder/constraints.md
Original file line number Diff line number Diff line change
Expand Up @@ -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$.

Expand Down Expand Up @@ -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:

Expand All @@ -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`.
Expand Down
2 changes: 1 addition & 1 deletion docs/src/design/stack/io_ops.md
Original file line number Diff line number Diff line change
Expand Up @@ -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$.
Expand Down
8 changes: 4 additions & 4 deletions docs/src/design/stack/op_constraints.md
Original file line number Diff line number Diff line change
Expand Up @@ -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$ |
| `<unused>` | $90$ | `101_1010` | | $5$ |
| `<unused>` | $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$ |
| `<unused>` | $92$ | `101_1100` | | $5$ |
| `<unused>` | $93$ | `101_1101` | | $5$ |
| `<unused>` | $94$ | `101_1110` | | $5$ |
Expand All @@ -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$ |
| `<unused>` | $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$ |
Expand Down Expand Up @@ -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.
12 changes: 6 additions & 6 deletions miden/tests/integration/flow_control/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<Digest> = 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]
Expand Down

0 comments on commit 0e2d4c4

Please sign in to comment.