You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
|`PUSH`| $f_{push}$ | 4 | An immediate value is pushed onto the stack. |
25
25
26
-
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$.
26
+
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$.
27
27
28
28
As described [previously](index.md#program-decoding), the general idea of the decoder is that the prover provides the program to the VM by populating some of cells in the trace non-deterministically. Values in these are then used to update virtual tables (represented via multiset checks) such as block hash table, block stack table etc. Transition constraints are used to enforce that the tables are updates correctly, and we also apply boundary constraints to enforce the correct initial and final states of these tables. One of these boundary constraints binds the execution trace to the hash of the program being executed. Thus, if the virtual tables were updated correctly and boundary constraints hold, we can be convinced that the prover executed the claimed program on the VM.
Copy file name to clipboardExpand all lines: docs/miden/vm/design/index.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -46,7 +46,7 @@ The system component does not yet have a dedicated documentation section, since
46
46
*`clk` which is used to keep track of the current VM cycle. Values in this column start out at $0$ and are incremented by $1$ with each cycle.
47
47
*`fmp` which contains the value of the free memory pointer used for specifying the region of memory available to procedure locals.
48
48
49
-
AIR constraints for the `fmp` column are described in [system operations](./stack/system_ops.md) section. For the `clk` column, the constraints are straightforward:
49
+
AIR constraints for the `fmp` column are described in [system operations](./stack/system-ops.md) section. For the `clk` column, the constraints are straightforward:
Copy file name to clipboardExpand all lines: docs/miden/vm/design/lookups/logup.md
+4-3Lines changed: 4 additions & 3 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1,4 +1,4 @@
1
-
#LogUp: multivariate lookups with logarithmic derivatives
1
+
## Multivariate lookups with logarithmic derivatives
2
2
3
3
The description of LogUp can be found [here](https://eprint.iacr.org/2022/1530.pdf). In MidenVM, LogUp is used to implement efficient [communication buses](./index.md#communication-buses-in-miden-vm).
4
4
@@ -9,6 +9,7 @@ $$
9
9
$$
10
10
11
11
In the above:
12
+
12
13
- $l$ is the number of values in $a$, which must be smaller than the size of the field. (The prime field used for Miden VM has modulus $p = 2^{64} - 2^{32} + 1$, so $l < p$ must be true.)
13
14
- $n$ is the number of values in $b$, which must be smaller than the size of the field. ($n < p$, for Miden VM)
14
15
- $m_i$ is the multiplicity of $b_i$, which is expected to match the number of times the value $b_i$ is duplicated in column $a$. It must be smaller than the size of the set of lookup values. ($m_i < n$)
@@ -20,9 +21,9 @@ Thus, instead of needing to compute running products, we are able to assert corr
20
21
21
22
The generalized trace columns and constraints for this construction are as follows, where component $X$ is some component in the trace and lookup table $T$ contains the values $v$ which need to be looked up from $X$ and how many times they are looked up (the multiplicity $m$).
The transition constraint for $b$ is now as follows:
53
53
@@ -66,7 +66,7 @@ Additionally, the constraint degree has not increased versus the naive approach,
66
66
67
67
To support 16-bit range checks, let's try to extend the idea of the 8-bit table. Our 16-bit table would look like so (the only difference is that column $v$ now has to end with value $65535$):
While this works, it is rather wasteful. In the worst case, we'd need to enumerate over 65K values, most of which we may not actually need. It would be nice if we could "skip over" the values that we don't want. One way to do this could be to add bridge rows between two values to be range checked and add constraints to enforce the consistency of the gap between these bridge rows.
72
72
@@ -139,12 +139,12 @@ In addition to the transition constraints described above, we also need to enfor
139
139
140
140
### Communication bus
141
141
142
-
$b_{range}$ is the [bus](./lookups/index.md#communication-buses-in-miden-vm) that connects components which require 16-bit range checks to the values in the range checker. The bus constraints are defined by the components that use it to communicate.
142
+
$b_{range}$ is the [bus](lookups/index.md#communication-buses-in-miden-vm) that connects components which require 16-bit range checks to the values in the range checker. The bus constraints are defined by the components that use it to communicate.
143
143
144
144
Requests are sent to the range checker bus by the following components:
145
145
146
-
- The Stack sends requests for 16-bit range checks during some [`u32` operations](./stack/u32-ops.md#range-checks).
147
-
- The [Memory chiplet](./chiplets/memory.md) sends requests for 16-bit range checks against the values in the $d_0$ and $d_1$ trace columns to enforce internal consistency.
146
+
- The Stack sends requests for 16-bit range checks during some [`u32` operations](stack/u32-ops.md#range-checks).
147
+
- The [Memory chiplet](chiplets/memory.md) sends requests for 16-bit range checks against the values in the $d_0$ and $d_1$ trace columns to enforce internal consistency.
148
148
149
149
Responses are provided by the range checker using the transition constraint for the LogUp construction described above.
Copy file name to clipboardExpand all lines: docs/miden/vm/design/stack/field-ops.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -4,7 +4,7 @@ In this section we describe the AIR constraints for Miden VM field operations (i
4
4
5
5
Assume $a$ and $b$ are the elements at the top of the stack. The `ADD` operation computes $c \leftarrow (a + b)$. The diagram below illustrates this graphically.
Copy file name to clipboardExpand all lines: docs/miden/vm/design/stack/index.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -129,7 +129,7 @@ To simplify constraint descriptions, we'll assume that the VM exposes two binary
129
129
| $f_{shr}$ | 6 | When this flag is set to $1$, the instruction executing on the VM is performing a "right shift". |
130
130
| $f_{shl}$ | 5 | When this flag is set to $1$, the instruction executing on the VM is performing a "left shift". |
131
131
132
-
These flags are mutually exclusive. That is, if $f_{shl}=1$, then $f_{shr}=0$ and vice versa. However, both flags can be set to $0$ simultaneously. This happens when the executed instruction does not shift the stack. How these flags are computed is described [here](./op_constraints.md).
132
+
These flags are mutually exclusive. That is, if $f_{shl}=1$, then $f_{shr}=0$ and vice versa. However, both flags can be set to $0$ simultaneously. This happens when the executed instruction does not shift the stack. How these flags are computed is described [here](./op-constraints.md).
0 commit comments