+
+ Miden Web App
+Open your browser console to see WebClient logs.
+ +
+
+
+
+
+ );
+}
diff --git a/src/theme/DocItem/Layout/styles.module.css b/src/theme/DocItem/Layout/styles.module.css
new file mode 100644
index 0000000..d3161d6
--- /dev/null
+++ b/src/theme/DocItem/Layout/styles.module.css
@@ -0,0 +1,28 @@
+.docItemWrapper {
+ position: relative;
+}
+
+.copyButtonContainer {
+ display: flex;
+ justify-content: flex-end;
+ margin-bottom: 0.5rem;
+ padding-right: 0;
+}
+
+/* Adjust position on larger screens */
+@media (min-width: 997px) {
+ .copyButtonContainer {
+ position: absolute;
+ top: 0;
+ right: -60px;
+ margin-bottom: 0;
+ z-index: 10;
+ }
+}
+
+/* Even wider screens - push further right */
+@media (min-width: 1200px) {
+ .copyButtonContainer {
+ right: -100px;
+ }
+}
diff --git a/versioned_docs/version-0.12 (stable)/_category_.json b/versioned_docs/version-0.12 (stable)/_category_.json
new file mode 100644
index 0000000..38de553
--- /dev/null
+++ b/versioned_docs/version-0.12 (stable)/_category_.json
@@ -0,0 +1,5 @@
+{
+ "label": "Docs",
+ "position": 1,
+ "collapsed": false
+}
diff --git a/versioned_docs/version-0.12 (stable)/compiler/_category_.yml b/versioned_docs/version-0.12 (stable)/compiler/_category_.yml
new file mode 100644
index 0000000..adabe49
--- /dev/null
+++ b/versioned_docs/version-0.12 (stable)/compiler/_category_.yml
@@ -0,0 +1,4 @@
+label: Compiler
+# Determines where this documentation section appears relative to other sections on the main documentation page (which is the parent of this folder in the miden-docs repository)
+position: 8
+collapsed: true
diff --git a/versioned_docs/version-0.12 (stable)/compiler/appendix/_category_.yml b/versioned_docs/version-0.12 (stable)/compiler/appendix/_category_.yml
new file mode 100644
index 0000000..ab3d9c7
--- /dev/null
+++ b/versioned_docs/version-0.12 (stable)/compiler/appendix/_category_.yml
@@ -0,0 +1,4 @@
+label: Compiler
+# Determines where this documentation section appears relative to other sections in the parent folder
+position: 4
+collapsed: true
diff --git a/versioned_docs/version-0.12 (stable)/compiler/appendix/calling-conventions.md b/versioned_docs/version-0.12 (stable)/compiler/appendix/calling-conventions.md
new file mode 100644
index 0000000..bee90c0
--- /dev/null
+++ b/versioned_docs/version-0.12 (stable)/compiler/appendix/calling-conventions.md
@@ -0,0 +1,304 @@
+---
+title: Calling Conventions
+draft: true
+---
+
+# Calling conventions
+
+This document describes the various calling conventions recognized/handled by the compiler,
+including a specification for the interaction with the IR type system.
+
+There are four calling conventions represented in the compiler:
+
+- `C` aka `SystemV`, which corresponds to the C ABI commonly used for C foreign-function interfaces (FFI).
+ We specifically use the System V ABI because it is well understood, documented, and straightforward.
+- `Fast`, this convention allows the compiler to follow either the `C` calling convention, or modify it
+ as it sees fit on a function-by-function basis. This convention provides no guarantees about how a
+ callee will expect arguments to be passed, so should not be used for functions which are expected to
+ have a stable, predictable interface. This is a good choice for local functions, or functions which are
+ only used within an executable/library and are not part of the public interface.
+- `Kernel`, this is a special calling convention that is used when defining kernel modules in the IR.
+ Functions which are part of the kernel's public API are required to use this convention, and it is not
+ possible to call a function via `syscall` if the callee is not defined with this convention. Because of
+ the semantics of `syscall`, this convention is highly restrictive. In particular, it is not permitted to
+ pass pointer arguments, or aggregates containing pointers, as `syscall` involves a context switch, and
+ thus memory in the caller is not accessible to the callee, and vice versa.
+- `Contract`, this is a special calling convention that is used when defining smart contract functions, i.e.
+ functions that can be `call`'d. The compiler will not permit you to `call` a function if the callee is not
+ defined with this convention, and functions with this convention cannot be called via `exec`. Like `syscall`,
+ the `call` instruction involves a context switch, however, unlike the `Kernel` convention, the `Contract`
+ convention is allowed to have types in its signature that are/contain pointers, with certain caveats around
+ those pointers.
+
+All four conventions above are based on the System V C ABI, tailored to the Miden VM. The only exception is
+`Fast`, which may modify the ABI arbitrarily as it sees fit, and makes no guarantees about what modifications,
+if any, it will make.
+
+## Data representation
+
+The following is a description of how the IR type system is represented in the `C` calling convention. Later,
+a description of how the other conventions extend/restrict/modify this representation will be provided.
+
+### Scalars
+
+General type | C Type | IR Type | `sizeof` | Alignment (bytes) | Miden Type
+-|-|-|-|-|-
+ Integer | `_Bool`/`bool` | `I1` | 1 | 1 | u32
+ Integer | `char`, `signed char` | `I8` | 1 | 1 | i32[^1]
+ Integer | `unsigned char` | `U8` | 1 | 1 | u32
+ Integer | `short` / `signed short` | `I16` | 2 | 2 | i32[^1]
+ Integer | `unsigned short` | `U16` | 2 | 2 | u32
+ Integer | `int` / `signed int` / `enum` | `I32` | 4 | 4 | i32[^1][^8]
+ Integer | `unsigned int` | `U32` | 4 | 4 | u32
+ Integer | `long` / `signed long` | `I32` | 4 | 4 | i32[^1]
+ Integer | `unsigned long` / `size_t` | `U32` | 4 | 4 | u32
+ Integer | `long long` / `signed long long` | `I64` | 8 | 8 | i64[^2]
+ Integer | `unsigned long long` | `U64` | 8 | 8 | u64[^3]
+ Pointer | *`any-type *`* / *`any-type (*)()`* | `Ptr(_)` | 4 | 4 | u32[^6][^7]
+ Floating point | `float` | `F32` | 4 | 4 | u32[^4]
+ Floating point | `double` | `F64` | 8 | 8 | u64[^4]
+ Floating point | `long double` | 16 | 16 | (none)[^5]
+
+[^1]: i32 is not a native Miden type, but is implemented using compiler intrinsics on top of the native u32 type
+
+[^2]: i64 is not a native Miden type, but is implemented using compiler intrinsics on top of the stdlib u64 type
+
+[^3]: u64 is not a native Miden type, but is implemented in software using two 32-bit limbs (i.e. a pair of field elements)
+
+[^4]: floating-point types are not currently supported, but will be implemented using compiler intrinsics
+
+[^5]: `long double` values correspond to 128-bit IEEE-754 quad-precision binary128 values. These are not currently
+supported, and we have no plans to support them in the near term. Should we ever provide such support, we will do
+so using compiler intrinsics.
+
+[^6]: A null pointer (for all types) always has the value zero.
+
+[^7]: Miden's linear memory is word-addressable, not byte-addressable. The `Ptr` type has an `AddressSpace` parameter,
+that by default is set to the byte-addressable address space. The compiler translates values of `Ptr` type that are in
+this address space, into the Miden-native, word-addressable address space during codegen of load/store operations. See
+the section on the memory model below for more details.
+
+[^8]: An `enum` is `i32` if all members of the enumeration can be represented by an `int`/`unsigned int`, otherwise it
+uses i64.
+
+:::note
+
+The compiler does not support scalars larger than one word (128 bits) at this time. As a result, anything that is
+larger than that must be allocated in linear memory, or in an automatic allocation (function-local memory), and passed
+around by reference.
+
+:::
+
+The native scalar type for the Miden VM is a "field element", specifically a 64-bit value representing an integer
+in the "Goldilocks" field, i.e. `0..(2^64-2^32+1)`. A number of instructions in the VM operate on field elements directly.
+However, the native integral/pointer type, i.e. a "machine word", is actually `u32`. This is because a field element
+can fully represent 32-bit integers, but not the full 64-bit integer range. Values of `u32` type are valid field element
+values, and can be used anywhere that a field element is expected (barring other constraints).
+
+Miden also has the notion of a "word", not to be confused with a "machine word" (by which we mean the native integral
+type used to represent pointers), which corresponds to a set of 4 field elements. Words are commonly used in Miden,
+particularly to represent hashes, and a number of VM instructions operate on word-sized operands. As an aside, 128-bit
+integer values are represented using a word, or two 64-bit limbs (each limb consisting of two 32-bit limbs).
+
+All integral types mentioned above, barring field elements, use two's complement encoding. Unsigned integral types
+make use of the sign bit to change the value range (i.e. 0..2^32-1, rather than -2^31..2^31-1), but the encoding follows
+two's complement rules.
+
+The Miden VM only has native support for field elements, words, and `u32`; all other types are implemented in software
+using intrinsics.
+
+### Aggregates and unions
+
+Structures and unions assume the alignment of their most strictly aligned component. Each member is assigned to the
+lowest available offset with the appropriate alignment. The size of any object is always a multiple of the object's alignment.
+An array uses the same alignment as its elements. Structure and union objects can require padding to meet size and alignment
+constraints. The contents of any padding is undefined.
+
+### Memory model
+
+Interacting with memory in Miden is quite similar to WebAssembly in some ways:
+
+* The address space is linear, with addresses starting at zero, and ranging up to 2^32-1
+* There is no memory protection per se, you either have full read/write access, or no access to a specific memory context
+* How memory is used is completely up to the program being executed
+
+This is where it begins to differ though, and takes on qualities unique to Miden (in part, or whole):
+
+* Certain regions of the address space are "reserved" for special uses, improper use of those regions may result in
+undefined behavior.
+* Miden has different types of function call instructions: `call` vs `syscall` vs `exec`. The first two
+perform a context switch when transferring control to the callee, and the callee has no access to the
+caller's memory (and the caller has no access to the callee's memory). As a result, references to memory
+cannot be passed from caller to callee in arguments, nor can they be returned from the callee to the caller.
+* Most significant of all though, is that Miden does not have byte-addressable memory, it is instead word-addressable,
+i.e. every address refers to a full word.
+* It is not possible to load a specific field element from a word in memory, unless it happens to be the first element
+of the word. Instead, one must load the full word, and drop the elements you don't need.
+
+This presents some complications, particularly:
+
+* Most languages assume a byte-oriented memory model, which is not trivially mapped to a word-oriented model
+* Simple things, such as taking the address of a field in a struct, and then dereferencing it, cannot be directly
+represented in Miden using native pointer arithmetic and `load` instruction. Operations like this must be translated
+into instruction sequences that load whole words from memory, extract the data needed, and discard the unused bits.
+This makes the choice of where in memory to store something much more important than byte-addressable memory, as
+loads of values which are not aligned to element or word boundaries can be quite inefficient in some cases.
+
+The compiler solves this by providing a byte-addressable IR, and internally translating operations in the IR to the equivalent
+sequence of Miden instructions needed to emulate that operation. This translation is done during code generation, and uses
+the following semantics to determine how a particular operation gets lowered:
+
+* A byte-addressable pointer can be emulated in Miden's word-addressable environment using three pieces of information:
+ - The address of the word containing the first byte of the value, this is a "native" Miden address value
+ - The index of the field element within that word containing the first byte of the value
+ - The offset (in bytes) from the start of the 4 byte chunk represented by the selected element, corresponding
+ to the first byte of the value. Since the chunk is represented as a u32 value, the offset is relative to the
+ most-significant bit (i.e. the byte with the lowest address is found in bits 55-63, since Miden integers are little-endian)
+* This relies on us treating Miden's linear memory as an array of 16-byte chunks of raw memory (each word is 4 field elements,
+each element represents a 4-byte chunk). In short, much like translating a virtual memory address to a physical one, we must
+translate byte-addressable "virtual" pointers to "real" Miden pointers with enough metadata to be able to extract the data we're
+trying to load (or encode the data we're trying to store).
+
+Because we're essentially emulating byte-addressable memory on word-addressable memory, loads/stores can range from simple and
+straightforward, to expensive and complicated, depending on the size and alignment of the value type. The process goes as follows:
+
+* If the value type is word-aligned, it can be loaded/stored in as little as a single instruction depending on the size of the type
+* Likewise if the value type is element-aligned, and the address is word-aligned
+* Element-aligned values require some extra instructions to load a full word and drop the unused elements (or in the case of stores,
+loading the full word and replacing the element being stored)
+* Loads/stores of types with sub-element alignment depend on the alignment of the pointer itself. Element or word-aligned addresses
+are still quite efficient to load/store from, but if the first byte of the value occurs in the middle of an element, then the bytes
+of that value must be shifted into place (or unused bytes masked out). If the value crosses an element boundary, then the bytes in
+both elements must be isolated and shifted into position such that they can be bitwise-OR'd together to obtain the aligned value on
+the operand stack. If a value crosses a word boundary, then elements from both words must be loaded, irrelevant ones discarded, the
+relevant bytes isolated and shifted into position so that the resulting operand on the stack is aligned and laid out correctly.
+* Stores are further complicated by the need to preserve memory that is not being explicitly written to, so values that do not overwrite
+a full word or element, require combining bytes from the operand being stored and what currently resides in memory.
+
+The worst case scenario for an unaligned load or store involves a word-sized type starting somewhere in the last element of the first
+word. This will require loading elements from three consecutive words, plus a lot of shuffling bits around to get the final, aligned
+word-sized value on the operand stack. Luckily, such operations should be quite rare, as by default all word-sized scalar types are
+word-aligned or element-aligned, so an unaligned load or store would require either a packed struct, or a type such as an array of
+bytes starting at some arbitrary address. In practice, most loads/stores are likely to be element-aligned, so most overhead from
+emulation will come from values which cross an element or word boundary.
+
+## Function calls
+
+This section describes the conventions followed when executing a function call via `exec`, including how arguments are passed on the
+operand stack, stack frames, etc. Later, we'll cover the differences when executing calls via `call` or `syscall`.
+
+### Locals and the stack frame
+
+Miden does not have registers in the style of hardware architectures. Instead it has an operand stack, on which an arbitrary number of
+operands may be stored, and local variables. In both cases - an operand on the operand stack, or a single local variable - the value
+type is nominally a field element, but it is easier to reason about them as untyped element-sized values. The operand stack is used
+for function arguments, return values, temporary variables, and scratch space. Local variables are not always used, but are typically
+used to hold multiply-used values which you don't want to keep on the operand stack, function-scoped automatic allocations (i.e. `alloca`),
+and other such uses.
+
+Miden does not have a stack frame per se. When you call a procedure in Miden Assembly, any local variables declared by that procedure
+are allocated space in a reserved region of linear memory in a single consecutive chunk. However, there is no stack or frame pointer,
+and because Miden is a Harvard architecture machine, there are no return addresses. Instead, languages (such as C) which have the concept
+of a stack frame with implications for the semantics of say, taking the address of a local variable, will need to emit code in function
+prologues and epilogues to maintain a shadow stack in Miden's linear memory. If all you need is local variables, you can get away with
+leaning on Miden's notion of local variables without implementing a shadow stack.
+
+Because there are no registers, the notion of callee-saved or caller-saved registers does not have a direct equivalent in Miden. However,
+in its place, a somewhat equivalent set of rules defines the contract between caller and callee in terms of the state of the operand stack,
+those are described below in the section covering the operand stack.
+
+#### The shadow stack
+
+Miden is a [Harvard](https://en.wikipedia.org/wiki/Harvard_architecture) architecture; as such, code and data are not in the same memory
+space. More precisely, in Miden, code is only addressable via the hash of the MAST root of that code, which must correspond to code that
+has been loaded into the VM. The hash of the MAST root of a function can be used to call that function both directly and indirectly, but
+that is the only action you can take with it. Code can not be generated and called on the fly, and it is not stored anywhere that is
+accessible to code that is currently executing.
+
+One consequence of this is that there are no return addresses or instruction pointers visible to executing code. The runtime call stack is
+managed by the VM itself, and is not exposed to executing code in any way. This means that address-taken local C variables need to be on a
+separate stack in linear memory (which we refer to as a "shadow stack"). Not all functions necessarily require a frame in the shadow stack,
+as it cannot be used to perform unwinding, so only functions which have locals require a frame.
+
+The Miden VM actually provides some built-in support for stack frames when using Miden Assembly. Procedures which are declared with some
+number of locals, will be automatically allocated sufficient space for those locals in a reserved region of linear memory when called. If
+you use the `locaddr` instruction to get the actual address of a local, that address can be passed as an argument to callees (within the
+constraints of the callee's calling convention).
+
+Languages with more elaborate requirements with regard to the stack will need to implement their own shadow stack, and emit code in function
+prologues/epilogues to manage it.
+
+#### The operand stack
+
+The Miden virtual machine is a stack machine, not a register machine. Rather than having a fixed set of registers that are used to
+store and manipulate scalar values, the Miden VM has the operand stack, which can hold an arbitrary number of operands (where each
+operand is a single field element), of which the first 16 can be directly manipulated using special stack instructions. The operand
+stack is, as the name implies, a last-in/first-out data structure.
+
+The following are basic rules all conventions are expected to follow with regard to the operand stack:
+
+1. The state of the operand stack from the point of view of the caller should be preserved, with two exceptions:
+ - The callee is expected to consume all of its arguments, and the caller will expect those operands to be gone when control is returned to it
+ - If the callee signature declares a return value, the caller expects to see that on top of the stack when control is returned to it
+2. No more than 16 elements of the operand stack may be used for passing arguments. If more than that is required to represent all of the arguments,
+then one of the following must happen:
+ - Spill to stack frame: in this scenario, up to 15 elements of the operand stack are used for arguments, and the remaining element is used to hold
+ a pointer to a local variable in the caller's stack frame. That local variable is a struct whose fields are the spilled arguments, appearing in
+ the same order as they would be passed. The callee must use the pointer it is given to compute the effective address for each spilled argument
+ that it wishes to access.
+ - Spill to heap: this is basically identical to the approach above, except the memory is allocated from the global heap, rather than using memory
+ associated with the caller's stack frame.
+ - Spill to the advice provider: in this scenario, 12 elements of the stack are used for arguments, and the remaining 4 are used to hold a hash
+ which refers to the remaining arguments on the advice provider stack. The callee must arrange to fetch the spilled arguments from the advice
+ provider using that hash.
+
+#### Function signatures
+
+Miden Abstract Syntax Trees (MASTs) do not have any notion of functions, and as such are not aware of parameters, return values, etc. For
+this document, that's not a useful level of abstraction to examine. Even a step higher, Miden Assembly (MASM) has functions (procedures
+in MASM parlance), but no function signature, i.e. given a MASM procedure, there is no way to know how many arguments it expects, how
+many values it returns, let alone the types of arguments/return values. Instead, we're going to specify calling conventions in terms of
+Miden IR, which has a fairly expressive type system more or less equivalent to that of LLVM, and how that translates to Miden primitives.
+
+Functions in Miden IR always have a signature, which specify the following:
+
+* The calling convention required to call the function
+* The number and types of the function arguments
+* The type of value, if any, returned by the function, and whether it is returned by value or reference
+
+The following table relates IR types to how they are expected to be passed from the caller to the callee, and vice versa:
+
+Type | Parameter | Result |
+--------------------------|---------------|----------|
+scalar | direct | direct |
+empty struct or union[^1] | ignored | ignored |
+scalar struct or union[^2] | direct | direct |
+other struct or union | indirect | indirect |
+array | indirect | N/A |
+
+[^1]: Zero-sized types have no representation in memory, so they are ignored/skipped
+
+[^2]: Any struct or union that recursively (including through nested structs,
+unions, and arrays) contains just a single scalar value and is not specified to
+have greater than natural alignment.
+
+The compiler will automatically generate code that follows these rules, but if emitting MASM from your own backend, it is necessary to do so manually.
+For example, a function whose signature specifies that it returns a non-scalar struct by value, must actually be written such that it expects to receive
+a pointer to memory allocated by the caller sufficient to hold the return value, as the first parameter of the function (i.e. the parameter is prepended
+to the parameter list). When returning, the function must write the return value to that pointer, rather than returning it on the operand stack. In this
+example, the return value is returned indirectly (by reference).
+
+A universal rule is that the arguments are passed in reverse order, i.e. the first argument in the parameter list of a function will be on top of the
+operand stack. This is different than many Miden instructions which seemingly use the opposite convention, e.g. `add`, which expects the right-hand
+operand on top of the stack, so `a + b` is represented like `push a, push b, add`. If we were to implement `add` as a function, it would instead be
+`push b, push a, exec.add`. The rationale behind this is that, in general, the more frequently used arguments appear earlier in the parameter list,
+and thus we want those closer to the top of the operand stack to reduce the amount of stack manipulation we need to do.
+
+Arguments/return values are laid out on the operand stack just like they would be as if you had just loaded it from memory, so all arguments are aligned,
+but may span multiple operands on the operand stack as necessary based on the size of the type (i.e. a struct type that contains a `u32` and a `i1`
+field would require two operands to represent). If the maximum number of operands allowed for the call is reached, any remaining arguments must be
+spilled to the caller's stack frame, or to the advice provider. The former is used in the case of `exec`/`dynexec`, while the latter is used for `call`
+and `syscall`, as caller memory is not accessible to the callee with those instructions.
+
+While ostensibly 16 elements is the maximum number of operands on the operand stack that can represent function arguments, due to the way `dynexec`/`dyncall`
+work, it is actually limited to 12 elements, because at least 4 must be free to hold the hash of the function being indirectly called.
diff --git a/versioned_docs/version-0.12 (stable)/compiler/appendix/canonabi-adhocabi-mismatch.md b/versioned_docs/version-0.12 (stable)/compiler/appendix/canonabi-adhocabi-mismatch.md
new file mode 100644
index 0000000..a83132f
--- /dev/null
+++ b/versioned_docs/version-0.12 (stable)/compiler/appendix/canonabi-adhocabi-mismatch.md
@@ -0,0 +1,315 @@
+---
+title: Canonical ABI vs Miden ABI Incompatibility
+draft: true
+---
+
+# Canonical ABI vs Miden ABI incompatibility
+
+:::note
+
+This document describes an issue that arises when trying to map the ad-hoc calling convention/ABI
+used by various Miden Assembly procedures, such as those comprising the transaction kernel, and
+the "canonical" ABI(s) representable in Rust. It proposes a solution to this problem in the form
+of _adapter functions_, where the details of a given adapter are one of a closed set of known
+ABI _transformation strategies_.
+
+:::
+
+## Summary
+
+The gist of the problem is that in Miden, the size and number of procedure results is only constrained
+by the maximum addressable operand stack depth. In most programming languages, particularly those in
+which interop is typically performed using some variant of the C ABI (commonly the one described
+in the System V specification), the number of results is almost always limited to a single result,
+and the size of the result type is almost always limited to the size of a single machine word, in
+some cases two. On these platforms, procedure results of greater arity or size are typically handled
+by reserving space in the caller's stack frame, and implicitly prepending the parameter list of the
+callee with an extra parameter: a pointer to the memory allocated for the return value. The callee
+will directly write the return value via this pointer, instead of returning a value in a register.
+
+In the case of Rust, this means that attempting to represent a procedure that returns multiple values,
+or returns a larger-than-machine-word type, such as `Word`, will trigger the implicit transformation
+described above, as this is allowed by the standard Rust calling conventions. Since various Miden
+procedures that are part of the standard library and the transaction kernel are affected by this,
+the question becomes "how do we define bindings for these procedures in Rust?".
+
+The solution is to have the compiler emit glue code that closes the gap between the two ABIs. It
+does so by generating adapter functions, which wrap functions that have an ABI unrepresentable in
+Rust, and orchestrate lifting/lowering arguments and results between the adapter and the "real"
+function.
+
+When type signatures are available for all Miden Assembly procedures, we can completely automate
+this process. For now, we will require a manually curated list of known procedures, their signatures,
+and the strategy used to "adapt" those procedures for binding in Rust.
+
+## Background
+
+After analyzing all of the functions in the transaction kernel API, the most common cause of a mismatch
+between Miden and Rust ABIs, is due to implicit "sret" parameters, i.e. the transformation mentioned
+above which inserts an implicit pointer to the caller's stack frame for the callee to write the return
+value to, rather than doing so in a register (or in our case, on the operand stack). This seems to
+happen for any type that is larger than 8 bytes (i64).
+
+:::tip
+
+For a complete list of the transaction kernel functions, in WIT format, see
+[miden.wit](https://github.com/0xMiden/compiler/blob/main/tests/rust-apps-wasm/wit-sdk/sdk/wit/miden.wit).
+
+:::
+
+For most transaction kernel functions, the adapter function can be generated automatically using the
+pattern recognition and adapter functions described below.
+
+### Prerequisites
+
+- The compiler must know the type signature for any function we wish to apply the adapter strategy to
+
+### Implementation
+
+The compiler will analyze every component import to determine if that import requires an adapter,
+as determined by matching against a predefined set of patterns. The adapter generation will take
+place in the frontend, as it has access to all of the needed information, and ensures that we do
+not have any transformations or analyses that make decisions on the un-adapted procedure.
+
+The following pseudo-code can be used to recognize the various Miden ABI patterns:
+
+```rust
+pub enum MidenAbiPattern {
+ /// Calling this procedure will require an sret parameter on the Rust side, so
+ /// we need to emit an adapter that will lift/lower calls according to that
+ /// strategy.
+ ReturnViaPointer,
+ /// The underlying procedure is fully representable in Rust, and requires no adaptation.
+ NoAdapterNeeded,
+}
+
+pub struct MidenAbiPatternRecognition {
+ pattern: Option
+
+ _and_ that occur on `LINE` (literal, if provided) are hit. | +| `b in NAME` | Break when the glob pattern `NAME` matches the fully-qualified procedure name
containing the current instruction | +| `b for OPCODE` | Break when the an instruction with opcode `OPCODE` is exactly matched
(including immediate values) | +| `b next` | Break on the next instruction | +| `b after N` | Break after `N` cycles | +| `b at CYCLE` | Break when the cycle count reaches `CYCLE`.
If `CYCLE` has already occurred, this has no effect | + +When a breakpoint is hit, it will be highlighted, and the breakpoint window will display the number +of hit breakpoints in the lower right. + +After a breakpoint is hit, it expires if it is one of the following types: + +- Break after N +- Break at CYCLE +- Break next + +When a breakpoint expires, it is removed from the breakpoint list on the next cycle. + +## Reading memory + +Another useful diagnostic task is examining the contents of linear memory, to verify that expected +data has been written. You can do this via the command prompt, using `r` (or `read`), followed by +a space, and then the desired memory address and options: + +The format for read expressions is `:r ADDR [OPTIONS..]`, where `ADDR` is a memory address in +decimal or hexadecimal format (the latter requires the `0x` prefix). The `read` command supports +the following for `OPTIONS`: + +| Option | Alias | Values | Default | Description | +| ---------------- | ----- | --------------------------------------------------- | --------- | ---------------------------------------------------------------------------------------------------------------------------- | +| `-mode MODE` | `-m` | `words` (`word`, `w`), `bytes` (`byte`, `b`) | `words` | Specify a memory addressing mode | +| `-format FORMAT` | `-f` | `decimal` (`d`), `hex` (`x`), `binary` (`bin`, `b`) | `decimal` | Specify the format used to print integral values | +| `-count N` | `-c` | | `1` | Specify the number of units to read | +| `-type TYPE` | `-t` | See [Types](#types) | `word` | Specify the type of value to read
This also has the effect of modifying the default `-format` and unit size for `-count` | + +Any invalid combination of options, or invalid syntax, will display an error in the status bar. + +### Types + +| Type | Description | +| ------------------ | -------------------------------------------------- | +| `iN` | A signed integer of `N` bits | +| `uN` | An unsigned integer of `N` bits | +| `felt` | A field element | +| `word` | A Miden word, i.e. an array of four field elements | +| `ptr` or `pointer` | A 32-bit memory address (implies `-format hex`) | + +## Roadmap + +The following are some features planned for the near future: + +- **Watchpoints**, i.e. cause execution to break when a memory store touches a specific address +- **Conditional breakpoints**, i.e. only trigger a breakpoint when an expression attached to it + evaluates to true +- More DYIM-style breakpoints, i.e. when breaking on first hitting a match for a file or + procedure, we probably shouldn't continue to break for every instruction to which that + breakpoint technically applies. Instead, it would make sense to break and then temporarily + disable that breakpoint until something changes that would make breaking again useful. + This will rely on the ability to disable breakpoints, not delete them, which we don't yet + support. +- More robust type support in the `read` command +- Display procedure locals and their contents in a dedicated pane diff --git a/versioned_docs/version-0.12 (stable)/compiler/guides/develop_miden_in_rust.md b/versioned_docs/version-0.12 (stable)/compiler/guides/develop_miden_in_rust.md new file mode 100644 index 0000000..2af0205 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/guides/develop_miden_in_rust.md @@ -0,0 +1,45 @@ +--- +title: Developing Miden Programs in Rust +sidebar_position: 3 +--- + +# Developing Miden programs in Rust + +This chapter will walk through how to develop Miden programs in Rust using the standard library +provided by the `miden-stdlib-sys` crate (see the +[README](https://github.com/0xMiden/compiler/blob/main/sdk/stdlib-sys/README.md). + +## Getting started + +Import the standard library from the `miden-stdlib-sys` crate: + +```rust +use miden_stdlib_sys::*; +``` + +## Using `Felt` (field element) type + +The `Felt` type is a field element type that is used to represent the field element values of the +Miden VM. + +To initialize a `Felt` value from an integer constant checking the range at compile time, use the +`felt!` macro: + +```rust +let a = felt!(42); +``` + +Otherwise, use the `Felt::new` constructor: + +```rust +let a = Felt::new(some_integer_var).unwrap(); +``` + +The constructor returns an error if the value is not a valid field element, e.g. if it is not in the +range `0..=M` where `M` is the modulus of the field (2^64 - 2^32 + 1). + +The `Felt` type implements the standard arithmetic operations, e.g. addition, subtraction, +multiplication, division, etc. which are accessible through the standard Rust operators `+`, `-`, +`*`, `/`, etc. All arithmetic operations are wrapping, i.e. performed modulo `M`. + +TODO: Add examples of using operations on `Felt` type and available functions (`assert*`, etc.). diff --git a/versioned_docs/version-0.12 (stable)/compiler/guides/develop_miden_rollup_accounts_and_note_scripts_in_rust.md b/versioned_docs/version-0.12 (stable)/compiler/guides/develop_miden_rollup_accounts_and_note_scripts_in_rust.md new file mode 100644 index 0000000..ca0e632 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/guides/develop_miden_rollup_accounts_and_note_scripts_in_rust.md @@ -0,0 +1,8 @@ +--- +title: Developing Miden Rollup Accounts and Note Scripts in Rust +sidebar_position: 4 +--- + +# Developing Miden rollup accounts and note scripts in Rust + +This chapter walks you through how to develop Miden rollup accounts and note scripts in Rust using the Miden SDK crate. diff --git a/versioned_docs/version-0.12 (stable)/compiler/guides/index.md b/versioned_docs/version-0.12 (stable)/compiler/guides/index.md new file mode 100644 index 0000000..413bb0a --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/guides/index.md @@ -0,0 +1,13 @@ +--- +title: Guides +sidebar_position: 1 +--- + +# Guides + +This section contains practical guides for working with the Miden compiler: + +* [Compiling Rust to WebAssembly](./rust_to_wasm.md) - Walks through compiling Rust code to WebAssembly modules +* [WebAssembly to Miden Assembly](./wasm_to_masm.md) - Explains compiling Wasm modules to Miden Assembly +* [Developing Miden Programs in Rust](./develop_miden_in_rust.md) - Demonstrates using Rust with Miden's standard library +* [Developing Miden Rollup Accounts and Note Scripts in Rust](./develop_miden_rollup_accounts_and_note_scripts_in_rust.md) - Shows Rust development for Miden rollup components diff --git a/versioned_docs/version-0.12 (stable)/compiler/guides/rust_to_wasm.md b/versioned_docs/version-0.12 (stable)/compiler/guides/rust_to_wasm.md new file mode 100644 index 0000000..bdc41e5 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/guides/rust_to_wasm.md @@ -0,0 +1,181 @@ +--- +title: Rust to WebAssembly +sidebar_position: 1 +--- + +# Compiling Rust To WebAssembly + +This chapter will walk you through compiling a Rust crate to a WebAssembly (Wasm) module +in binary (i.e. `.wasm`) form. The Miden compiler has a frontend which can take such +modules and compile them on to Miden Assembly, which will be covered in the next chapter. + +## Setup + +First, let's set up a simple Rust project that contains an implementation of the Fibonacci +function (I know, it's overdone, but we're trying to keep things as simple as possible to +make it easier to show the results at each step, so bear with me): + +Start by creating a new library crate: + + cargo new --lib wasm-fib && cd wasm-fib + +To compile to WebAssembly, you must have the appropriate Rust toolchain installed, so let's add +a toolchain file to our project root so that `rustup` and `cargo` will know what we need, and use +them by default: + + cat <<EOF > rust-toolchain.toml + [toolchain] + channel = "stable" + targets = ["wasm32-wasip1"] + EOF + +Next, edit the `Cargo.toml` file as follows: + +```toml +[package] +name = "wasm-fib" +version = "0.1.0" +edition = "2021" + +[lib] +# Build this crate as a self-contained, C-style dynamic library +# This is required to emit the proper Wasm module type +crate-type = ["cdylib"] + +[dependencies] +# Use a tiny allocator in place of the default one, if we want +# to make use of types in the `alloc` crate, e.g. String. We +# don't need that now, but it's good information to have in hand. +#miden-sdk-alloc = "0.0.5" + +# When we build for Wasm, we'll use the release profile +[profile.release] +# Explicitly disable panic infrastructure on Wasm, as +# there is no proper support for them anyway, and it +# ensures that panics do not pull in a bunch of standard +# library code unintentionally +panic = "abort" +# Enable debug information so that we get useful debugging output +debug = true +# Optimize the output for size +opt-level = "z" +``` + +Most of these things are done to keep the generated code size as small as possible. Miden is a target +where the conventional wisdom about performance should be treated very carefully: we're almost always +going to benefit from less code, even if conventionally that code would be less efficient, simply due +to the difference in proving time accumulated due to extra instructions. That said, there are no hard +and fast rules, but these defaults are good ones to start with. + +:::tip + +We reference a simple bump allocator provided by `miden-sdk-alloc` above, but any simple +allocator will do. The trade offs made by these small allocators are not generally suitable for +long-running, or allocation-heavy applications, as they "leak" memory (generally because they +make little to no attempt to recover freed allocations), however they are very useful for +one-shot programs that do minimal allocation, which is going to be the typical case for Miden +programs. + +::: + +Next, edit `src/lib.rs` as shown below: + +```rust +// Do not link against libstd (i.e. anything defined in `std::`) +#![no_std] + +// However, we could still use some standard library types while +// remaining no-std compatible, if we uncommented the following lines: +// +// extern crate alloc; +// use alloc::{string::String, vec::Vec}; + +// If we wanted to use the types mentioned above, it would also be +// a good idea to use the allocator we pulled in as a dependency +// in Cargo.toml, like so: +//#[global_allocator] +//static ALLOC: miden_sdk_alloc::BumpAlloc = miden_sdk_alloc::BumpAlloc::new(); + +// Required for no-std crates +#[panic_handler] +fn panic(_info: &core::panic::PanicInfo) -> ! { + // Compiles to a trap instruction in WebAssembly + core::arch::wasm32::unreachable() +} + +// Marking the function no_mangle ensures that it is exported +// from the compiled binary as `fib`, otherwise it would have +// a mangled name that has no stable form. +// +// You can specify a different name from the library than the +// name in the source code using the `#[export_name = "foo"]` +// attribute, which will make the function callable as `foo` +// externally (in this example) +#[no_mangle] +pub fn fib(n: u32) -> u32 { + let mut a = 0; + let mut b = 1; + for _ in 0..n { + let c = a + b; + a = b; + b = c; + } + a +} +``` + +This exports our `fib` function from the library, making it callable from within a larger Miden program. + +All that remains is to compile to WebAssembly: + + cargo build --release --target=wasm32-wasip1 + +This places a `wasm_fib.wasm` file under the `target/wasm32-wasip1/release/` directory, which +we can then examine with [wasm2wat](https://github.com/WebAssembly/wabt) to set the code we generated: + + wasm2wat target/wasm32-wasip1/release/wasm_fib.wasm + +Which dumps the following output (may differ slightly on your machine, depending on the specific compiler version): + +```wat +(module $wasm_fib.wasm + (type (;0;) (func (param i32) (result i32))) + (func $fib (type 0) (param i32) (result i32) + (local i32 i32 i32) + i32.const 0 + local.set 1 + i32.const 1 + local.set 2 + loop (result i32) ;; label = @1 + local.get 2 + local.set 3 + block ;; label = @2 + local.get 0 + br_if 0 (;@2;) + local.get 1 + return + end + local.get 0 + i32.const -1 + i32.add + local.set 0 + local.get 1 + local.get 3 + i32.add + local.set 2 + local.get 3 + local.set 1 + br 0 (;@1;) + end) + (memory (;0;) 16) + (global $__stack_pointer (mut i32) (i32.const 1048576)) + (export "memory" (memory 0)) + (export "fib" (func $fib))) +``` + +Success! + +## Next steps + +In [Compiling WebAssembly to Miden Assembly](wasm_to_masm.md), we walk through how to take the +WebAssembly module we just compiled, and lower it to Miden Assembly using `midenc`! diff --git a/versioned_docs/version-0.12 (stable)/compiler/guides/wasm_to_masm.md b/versioned_docs/version-0.12 (stable)/compiler/guides/wasm_to_masm.md new file mode 100644 index 0000000..8b6bb44 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/guides/wasm_to_masm.md @@ -0,0 +1,143 @@ +--- +title: WebAssembly to Miden Assembly +sidebar_position: 2 +--- + +# Compiling WebAssembly to Miden Assembly + +This guide will walk you through compiling a WebAssembly (Wasm) module, in binary form +(i.e. a `.wasm` file), to Miden Assembly (Masm), both in its binary package form (a `.masp` file), +and in textual Miden Assembly syntax form (i.e. a `.masm` file). + +## Setup + +We will be making use of the example crate we created in [Compiling Rust to WebAssembly](rust_to_wasm.md), +which produces a small Wasm module that is easy to examine in Wasm text format, and demonstrates a +good set of default choices for a project compiling to Miden Assembly from Rust. + +In this chapter, we will be compiling Wasm to Masm using the `midenc` executable, so ensure that +you have followed the instructions in the [Getting Started with `midenc`](../usage/midenc.md) guide +and then return here. + +:::note + +While we are using `midenc` for this guide, the more common use case will be to use the +`cargo-miden` Cargo extension to handle the gritty details of compiling from Rust to Wasm +for you. However, the purpose of this guide is to show you what `cargo-miden` is handling +for you, and to give you a foundation for using `midenc` yourself if needed. + +::: + +## Compiling to Miden Assembly + +In the last chapter, we compiled a Rust crate to WebAssembly that contains an implementation +of the Fibonacci function called `fib`, that was emitted to +`target/wasm32-wasip1/release/wasm_fib.wasm`. All that remains is to tell `midenc` to compile this +module to Miden Assembly. + +Currently, by default, the compiler will emit an experimental package format that the Miden VM does +not yet support. We will instead use `midenc run` to execute the package using the VM for us, but +once the package format is stabilized, this same approach will work with `miden run` as well. + +We also want to examine the Miden Assembly generated by the compiler, so we're going to ask the +compiler to emit both types of artifacts: + +```bash +midenc compile --emit masm=wasm_fib.masm,masp target/wasm32-wasip1/release/wasm_fib.wasm +``` + +This will compile our Wasm module to a Miden package with the `.masp` extension, and also emit the +textual Masm to `wasm_fib.masm` so we can review it. The `wasm_fib.masp` file will be emitted in the +default output directory, which is the current working directory by default. + +If we dump the contents of `wasm_fib.masm`, we'll see the following generated code: + +```masm +export.fib + push.0 + push.1 + movup.2 + swap.1 + dup.1 + neq.0 + push.1 + while.true + if.true + push.4294967295 + movup.2 + swap.1 + u32wrapping_add + dup.1 + swap.1 + swap.3 + swap.1 + u32wrapping_add + movup.2 + swap.1 + dup.1 + neq.0 + push.1 + else + drop + drop + push.0 + end + end +end +``` + +If you compare this to the WebAssembly text format, you can see that this is a fairly +faithful translation, but there may be areas where we generate sub-optimal Miden Assembly. + +:::note + +At the moment the compiler does only minimal optimization, late in the pipeline during codegen, +and only in an effort to minimize operand stack management code. So if you see an instruction +sequence you think is bad, bring it to our attention, and if it is something that we can solve +as part of our overall optimization efforts, we will be sure to do so. There _are_ limits to +what we can generate compared to what one can write by hand, particularly because Rust's +memory model requires us to emulate byte-addressable memory on top of Miden's word-addressable +memory, however our goal is to keep this overhead within an acceptable bound in the general case, +and easily-recognized patterns that can be simplified using peephole optimization are precisely +the kind of thing we'd like to know about, as those kinds of optimizations are likely to produce +the most significant wins. + +::: + +## Testing with the Miden VM + +:::note + +Because the compiler ships with the VM embedded for `midenc debug`, you can run your program +without having to install the VM separately, though you should do that as well, as `midenc` only +exposes a limited set of commands for executing programs, intended for debugging. + +::: + +We can test our compiled program like so: + +```bash +$ midenc run --num-outputs 1 wasm_fib.masp -- 10 +============================================================ +Run program: wasm_fib.masp +============================================================ +Executed program with hash 0xe5ba88695040ec2477821b26190e9addbb1c9571ae30c564f5bbfd6cabf6c535 in 19 milliseconds +Output: [55] +VM cycles: 295 extended to 512 steps (42% padding). +├── Stack rows: 295 +├── Range checker rows: 67 +└── Chiplets rows: 250 +├── Hash chiplet rows: 248 +├── Bitwise chiplet rows: 0 +├── Memory chiplet rows: 1 +└── Kernel ROM rows: 0 +``` + +Success! We got the expected result of `55`. + +## Next steps + +This guide is not comprehensive, as we have not yet examined in detail the differences between +compiling libraries vs programs, linking together multiple libraries, packages, or discussed some of +the more esoteric compiler options. We will be updating this documentation with those details and +more in the coming weeks and months, so bear with us while we flesh out our guides! diff --git a/versioned_docs/version-0.12 (stable)/compiler/index.md b/versioned_docs/version-0.12 (stable)/compiler/index.md new file mode 100644 index 0000000..d309639 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/index.md @@ -0,0 +1,106 @@ +--- +title: Compiler +sidebar_position: 1 +--- + +# Getting Started + +Welcome to the documentation for the Miden compiler toolchain. + +:::caution + +The compiler is currently in an experimental state, and has known bugs and limitations, it is +not yet ready for production usage. However, we'd encourage you to start experimenting with it +yourself, and give us feedback on any issues or sharp edges you encounter. + +::: + +The documentation found here should provide a good starting point for the current capabilities of +the toolchain, however if you find something that is not covered, but is not listed as +unimplemented or a known limitation, please let us know by reporting an issue on the compiler +[issue tracker](https://github.com/0xMiden/compiler/issues). + +## What is provided? + +The compiler toolchain consists of the following primary components: + +- An intermediate representation (IR), which can be lowered to by compiler backends wishing to + support Miden as a target. The Miden IR is an SSA IR, much like Cranelift or LLVM, providing a + much simpler path from any given source language (e.g. Rust), to Miden Assembly. It is used + internally by the rest of the Miden compiler suite. +- A WebAssembly (Wasm) frontend for Miden IR. It can handle lowering both core Wasm modules, as + well as basic components using the experimental WebAssembly Component Model. Currently, the Wasm + frontend is known to work with Wasm modules produced by `rustc`, which is largely just what LLVM + produces, but with the shadow stack placed at the start of linear memory rather than after + read-only data. In the future we intend to support more variety in the structure of Wasm modules + we accept, but for the time being we're primarily focused on using this as the path for lowering + Rust to Miden. +- The compiler driver, in the form of the `midenc` executable, and a Rust crate, `midenc-compiler` + to allow integrating the compiler into other tools. This plays the same role as `rustc` does in + the Rust ecosystem. +- A Cargo extension, `cargo-miden`, that provides a convenient developer experience for creating + and compiling Rust projects targeting Miden. It contains a project template for a basic Rust crate, + and handles orchestrating `rustc` and `midenc` to compile the crate to WebAssembly, and then to + Miden Assembly. +- A terminal-based interactive debugger, available via `midenc debug`, which provides a UI very + similar to `lldb` or `gdb` when using the TUI mode. You can use this to run a program, or step + through it cycle-by-cycle. You can set various types of breakpoints; see the source code, call + stack, and contents of the operand stack at the current program point; as well as interatively + read memory and format it in various ways for display. +- A Miden SDK for Rust, which provides types and bindings to functionality exported from the Miden + standard library, as well as the Miden transaction kernel API. You can use this to access native + Miden features which are not provided by Rust out-of-the-box. The project template generated by + `cargo miden new` automatically adds this as a dependency. + +## What can I do with it? + +That all sounds great, but what can you do with the compiler today? The answer depends a bit on what +aspect of the compiler you are interested in: + +### Rust + +The most practically useful, and interesting capability provided by the compiler currently, is the +ability to compile arbitrary Rust programs to Miden Assembly. See the guides for more information +on setting up and compiling a Rust crate for execution via Miden. + +### WebAssembly + +More generally, the compiler frontend is capable of compiling WebAssembly modules, with some +constraints, to Miden Assembly. As a result, it is possible to compile a wider variety of languages +to Miden Assembly than just Rust, so long as the language can compile to WebAssembly. However, we +do not currently provide any of the language-level support for languages other than Rust, and +have limited ability to provide engineering support for languages other than Rust at this time. + +Our Wasm frontend does not support all of the extensions to the WebAssembly MVP, most notably the +reference types and GC proposals. + +### Miden IR + +If you are interested in compiling to Miden from your own compiler, you can target Miden IR, and +invoke the driver from your compiler to emit Miden artifacts. At this point in time, we don't have +the resources to provide much in the way of engineering support for this use case, but if you find +issues in your efforts to use the IR in your compiler, we would certainly like to know about them! + +We do not currently perform any optimizations on the IR, since we are primarily working with the +output of compiler backends which have already applied optimizations, at this time. This may change +in the future, but for now it is expected that you implement your own optimization passes as needed. + +## Known bugs and limitations + +For the latest information on known bugs and limitations, see the [issue tracker](https://github.com/0xMiden/compiler/issues). + +## Where to start? + +Provided here are a set of guides which are focused on documenting a couple of supported workflows +we expect will meet the needs of most users, within the constraints of the current feature set of +the compiler. If you find that there is something you wish to do that is not covered, and is not +one of our known limitations, please open an issue, and we will try to address the missing docs as +soon as possible. + +## Installation + +To get started, there are a few ways you might use the Miden compiler. Select the one that applies +to you, and the corresponding guide will walk you through getting up and running: + +1. [Using the Cargo extension](usage/cargo-miden.md) +2. [Using the `midenc` executable](usage/midenc.md) diff --git a/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Danger.tsx b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Danger.tsx new file mode 100644 index 0000000..ab14d7d --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Danger.tsx @@ -0,0 +1,19 @@ +import React, { type ReactNode } from "react"; +import type { Props } from "@theme/Admonition/Icon/Danger"; + +export default function AdmonitionIconDanger(props: Props): ReactNode { + return ( + + ); +} diff --git a/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Info.tsx b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Info.tsx new file mode 100644 index 0000000..59e48a5 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Info.tsx @@ -0,0 +1,20 @@ +import React, { type ReactNode } from "react"; +import type { Props } from "@theme/Admonition/Icon/Info"; + +export default function AdmonitionIconInfo(props: Props): ReactNode { + return ( + + ); +} diff --git a/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Note.tsx b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Note.tsx new file mode 100644 index 0000000..d7c524b --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Note.tsx @@ -0,0 +1,20 @@ +import React, { type ReactNode } from "react"; +import type { Props } from "@theme/Admonition/Icon/Note"; + +export default function AdmonitionIconNote(props: Props): ReactNode { + return ( + + ); +} diff --git a/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Tip.tsx b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Tip.tsx new file mode 100644 index 0000000..219bb8d --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Tip.tsx @@ -0,0 +1,20 @@ +import React, { type ReactNode } from "react"; +import type { Props } from "@theme/Admonition/Icon/Tip"; + +export default function AdmonitionIconTip(props: Props): ReactNode { + return ( + + ); +} diff --git a/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Warning.tsx b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Warning.tsx new file mode 100644 index 0000000..f96398d --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Icon/Warning.tsx @@ -0,0 +1,20 @@ +import React, { type ReactNode } from "react"; +import type { Props } from "@theme/Admonition/Icon/Warning"; + +export default function AdmonitionIconCaution(props: Props): ReactNode { + return ( + + ); +} diff --git a/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Layout/index.tsx b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Layout/index.tsx new file mode 100644 index 0000000..7b2c170 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/compiler/theme/Admonition/Layout/index.tsx @@ -0,0 +1,51 @@ +import React, { type ReactNode } from "react"; +import clsx from "clsx"; +import { ThemeClassNames } from "@docusaurus/theme-common"; + +import type { Props } from "@theme/Admonition/Layout"; + +import styles from "./styles.module.css"; + +function AdmonitionContainer({ + type, + className, + children, +}: Pick
+ {children}
+
+ );
+}
+
+function AdmonitionHeading({ icon, title }: Pick
+ {icon}
+ {/* {title} */}
+
+ );
+}
+
+function AdmonitionContent({ children }: Pick{children}
+ ) : null;
+}
+
+export default function AdmonitionLayout(props: Props): ReactNode {
+ const { type, icon, title, children, className } = props;
+ return (
+
+ .default})
+
+ .default})
+
+ .default})
+
+ .default})
+
+ .default})
+
+ .default})
+
+ .default})
+
+ .default})
+
+ .default})
+
**Inputs:** `[]`
**Outputs:** `[account_id_prefix, account_id_suffix]` | Any | +| `get_nonce` | Returns the nonce of the active account. Always returns the initial nonce as it can only be incremented in auth procedures.
**Inputs:** `[]`
**Outputs:** `[nonce]` | Any | +| `get_initial_commitment` | Returns the active account commitment at the beginning of the transaction.
**Inputs:** `[]`
**Outputs:** `[INIT_COMMITMENT]` | Any | +| `compute_commitment` | Computes and returns the account commitment from account data stored in memory.
**Inputs:** `[]`
**Outputs:** `[ACCOUNT_COMMITMENT]` | Any | +| `get_code_commitment` | Gets the account code commitment of the active account.
**Inputs:** `[]`
**Outputs:** `[CODE_COMMITMENT]` | Account | +| `get_initial_storage_commitment` | Returns the storage commitment of the active account at the beginning of the transaction.
**Inputs:** `[]`
**Outputs:** `[INIT_STORAGE_COMMITMENT]` | Any | +| `compute_storage_commitment` | Computes the latest account storage commitment of the active account.
**Inputs:** `[]`
**Outputs:** `[STORAGE_COMMITMENT]` | Account | +| `get_item` | Gets an item from the account storage.
**Inputs:** `[index]`
**Outputs:** `[VALUE]` | Account | +| `get_initial_item` | Gets the initial item from the account storage slot as it was at the beginning of the transaction.
**Inputs:** `[index]`
**Outputs:** `[VALUE]` | Account | +| `get_map_item` | Returns the VALUE located under the specified KEY within the map contained in the given account storage slot.
**Inputs:** `[index, KEY]`
**Outputs:** `[VALUE]` | Account | +| `get_initial_map_item` | Gets the initial VALUE from the account storage map as it was at the beginning of the transaction.
**Inputs:** `[index, KEY]`
**Outputs:** `[VALUE]` | Account | +| `get_balance` | Returns the balance of the fungible asset associated with the provided faucet_id in the active account's vault.
**Inputs:** `[faucet_id_prefix, faucet_id_suffix]`
**Outputs:** `[balance]` | Any | +| `get_initial_balance` | Returns the balance of the fungible asset associated with the provided faucet_id in the active account's vault at the beginning of the transaction.
**Inputs:** `[faucet_id_prefix, faucet_id_suffix]`
**Outputs:** `[init_balance]` | Any | +| `has_non_fungible_asset` | Returns a boolean indicating whether the non-fungible asset is present in the active account's vault.
**Inputs:** `[ASSET]`
**Outputs:** `[has_asset]` | Any | +| `get_initial_vault_root` | Returns the vault root of the active account at the beginning of the transaction.
**Inputs:** `[]`
**Outputs:** `[INIT_VAULT_ROOT]` | Any | +| `get_vault_root` | Returns the vault root of the active account.
**Inputs:** `[]`
**Outputs:** `[VAULT_ROOT]` | Any | +| `get_num_procedures` | Returns the number of procedures in the active account.
**Inputs:** `[]`
**Outputs:** `[num_procedures]` | Any | +| `get_procedure_root` | Returns the procedure root for the procedure at the specified index.
**Inputs:** `[index]`
**Outputs:** `[PROC_ROOT]` | Any | +| `has_procedure` | Returns the binary flag indicating whether the procedure with the provided root is available on the active account.
**Inputs:** `[PROC_ROOT]`
**Outputs:** `[is_procedure_available]` | Any | + +## Native account Procedures (`miden::native_account`) + +Native account procedures can be used to write to storage, add or remove assets from the vault and compute delta commitment of the native account. + +| Procedure | Description | Context | +| ------------------------------ | ------------------------------ | ------------------------------ | +| `get_id` | Returns the ID of the native account of the transaction.
**Inputs:** `[]`
**Outputs:** `[account_id_prefix, account_id_suffix]` | Any | +| `incr_nonce` | Increments the nonce of the native account by one and returns the new nonce. Can only be called from auth procedures.
**Inputs:** `[]`
**Outputs:** `[final_nonce]` | Auth | +| `compute_delta_commitment` | Computes the commitment to the native account's delta. Can only be called from auth procedures.
**Inputs:** `[]`
**Outputs:** `[DELTA_COMMITMENT]` | Auth | +| `set_item` | Sets an item in the native account storage.
**Inputs:** `[index, VALUE]`
**Outputs:** `[OLD_VALUE]` | Native & Account | +| `set_map_item` | Sets VALUE under the specified KEY within the map contained in the given native account storage slot.
**Inputs:** `[index, KEY, VALUE]`
**Outputs:** `[OLD_MAP_ROOT, OLD_MAP_VALUE]` | Native & Account | +| `add_asset` | Adds the specified asset to the vault. For fungible assets, returns the total after addition.
**Inputs:** `[ASSET]`
**Outputs:** `[ASSET']` | Native & Account | +| `remove_asset` | Removes the specified asset from the vault.
**Inputs:** `[ASSET]`
**Outputs:** `[ASSET]` | Native & Account | +| `was_procedure_called` | Returns 1 if a native account procedure was called during transaction execution, and 0 otherwise.
**Inputs:** `[PROC_ROOT]`
**Outputs:** `[was_called]` | Any | + +## Active Note Procedures (`miden::active_note`) + +Active note procedures can be used to fetch data from the note that is currently being processed by the transaction kernel. + +| Procedure | Description | Context | +| ----------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------- | +| `get_assets` | Writes the [assets](note.md#assets) of the active note into memory starting at the specified address.
**Inputs:** `[dest_ptr]`
**Outputs:** `[num_assets, dest_ptr]` | Note | +| `get_recipient` | Returns the [recipient](note.md#note-recipient-restricting-consumption) of the active note.
**Inputs:** `[]`
**Outputs:** `[RECIPIENT]` | Note | +| `get_inputs` | Writes the note's [inputs](note.md#inputs) to the specified memory address.
**Inputs:** `[dest_ptr]`
**Outputs:** `[num_inputs, dest_ptr]` | Note | +| `get_metadata` | Returns the [metadata](note.md#metadata) of the active note.
**Inputs:** `[]`
**Outputs:** `[METADATA]` | Note | +| `get_sender` | Returns the sender of the active note.
**Inputs:** `[]`
**Outputs:** `[sender_id_prefix, sender_id_suffix]` | Note | +| `get_serial_number` | Returns the [serial number](note.md#serial-number) of the active note.
**Inputs:** `[]`
**Outputs:** `[SERIAL_NUMBER]` | Note | +| `get_script_root` | Returns the [script root](note.md#script) of the active note.
**Inputs:** `[]`
**Outputs:** `[SCRIPT_ROOT]` | Note | +| `add_assets_to_account` | Adds all assets from the active note to the account vault.
**Inputs:** `[]`
**Outputs:** `[]` | Note | + +## Input Note Procedures (`miden::input_note`) + +Input note procedures can be used to fetch data on input notes consumed by the transaction. + +| Procedure | Description | Context | +| ------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | ------- | +| `get_assets_info` | Returns the information about [assets](note.md#assets) in the input note with the specified index.
**Inputs:** `[note_index]`
**Outputs:** `[ASSETS_COMMITMENT, num_assets]` | Any | +| `get_assets` | Writes the [assets](note.md#assets) of the input note with the specified index into memory starting at the specified address.
**Inputs:** `[dest_ptr, note_index]`
**Outputs:** `[num_assets, dest_ptr, note_index]` | Any | +| `get_recipient` | Returns the [recipient](note.md#note-recipient-restricting-consumption) of the input note with the specified index.
**Inputs:** `[note_index]`
**Outputs:** `[RECIPIENT]` | Any | +| `get_metadata` | Returns the [metadata](note.md#metadata) of the input note with the specified index.
**Inputs:** `[note_index]`
**Outputs:** `[METADATA]` | Any | +| `get_sender` | Returns the sender of the input note with the specified index.
**Inputs:** `[note_index]`
**Outputs:** `[sender_id_prefix, sender_id_suffix]` | Any | +| `get_inputs_info` | Returns the [inputs](note.md#inputs) commitment and length of the input note with the specified index.
**Inputs:** `[note_index]`
**Outputs:** `[NOTE_INPUTS_COMMITMENT, num_inputs]` | Any | +| `get_script_root` | Returns the [script root](note.md#script) of the input note with the specified index.
**Inputs:** `[note_index]`
**Outputs:** `[SCRIPT_ROOT]` | Any | +| `get_serial_number` | Returns the [serial number](note.md#serial-number) of the input note with the specified index.
**Inputs:** `[note_index]`
**Outputs:** `[SERIAL_NUMBER]` | Any | + +## Output Note Procedures (`miden::output_note`) + +Output note procedures can be used to fetch data on output notes created by the transaction. + +| Procedure | Description | Context | +| ----------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------- | +| `create` | Creates a new output note and returns its index.
**Inputs:** `[tag, aux, note_type, execution_hint, RECIPIENT]`
**Outputs:** `[note_idx]` | Native & Account | +| `get_assets_info` | Returns the information about assets in the output note with the specified index.
**Inputs:** `[note_index]`
**Outputs:** `[ASSETS_COMMITMENT, num_assets]` | Any | +| `get_assets` | Writes the assets of the output note with the specified index into memory starting at the specified address.
**Inputs:** `[dest_ptr, note_index]`
**Outputs:** `[num_assets, dest_ptr, note_index]` | Any | +| `add_asset` | Adds the `ASSET` to the output note specified by the index.
**Inputs:** `[ASSET, note_idx]`
**Outputs:** `[]` | Native | +| `get_recipient` | Returns the [recipient](note#note-recipient-restricting-consumption) of the output note with the specified index.
**Inputs:** `[note_index]`
**Outputs:** `[RECIPIENT]` | Any | +| `get_metadata` | Returns the [metadata](note#metadata) of the output note with the specified index.
**Inputs:** `[note_index]`
**Outputs:** `[METADATA]` | Any | + +## Note Utility Procedures (`miden::note`) + +Note utility procedures can be used to compute the required utility data or write note data to memory. + +| Procedure | Description | Context | +| --------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------- | +| `compute_inputs_commitment` | Computes the commitment to the output note inputs starting at the specified memory address.
**Inputs:** `[inputs_ptr, num_inputs]`
**Outputs:** `[INPUTS_COMMITMENT]` | Any | +| `get_max_inputs_per_note` | Returns the max allowed number of input values per note.
**Inputs:** `[]`
**Outputs:** `[max_inputs_per_note]` | Any | +| `write_assets_to_memory` | Writes the assets data stored in the advice map to the memory specified by the provided destination pointer.
**Inputs:** `[ASSETS_COMMITMENT, num_assets, dest_ptr]`
**Outputs:** `[num_assets, dest_ptr]` | Any | +| `build_recipient_hash` | Returns the `RECIPIENT` for a specified `SERIAL_NUM`, `SCRIPT_ROOT`, and inputs commitment.
**Inputs:** `[SERIAL_NUM, SCRIPT_ROOT, INPUT_COMMITMENT]`
**Outputs:** `[RECIPIENT]` | Any | +| `build_recipient` | Builds the recipient hash from note inputs, script root, and serial number.
**Inputs:** `[inputs_ptr, num_inputs, SERIAL_NUM, SCRIPT_ROOT]`
**Outputs:** `[RECIPIENT]` | Any | +| `extract_sender_from_metadata` | Extracts the sender ID from the provided metadata word.
**Inputs:** `[METADATA]`
**Outputs:** `[sender_id_prefix, sender_id_suffix]` | Any | + +## Transaction Procedures (`miden::tx`) + +Transaction procedures manage transaction-level operations including note creation, context switching, and reading transaction metadata. + +| Procedure | Description | Context | +| ------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------- | +| `get_block_number` | Returns the block number of the transaction reference block.
**Inputs:** `[]`
**Outputs:** `[num]` | Any | +| `get_block_commitment` | Returns the block commitment of the reference block.
**Inputs:** `[]`
**Outputs:** `[BLOCK_COMMITMENT]` | Any | +| `get_block_timestamp` | Returns the timestamp of the reference block for this transaction.
**Inputs:** `[]`
**Outputs:** `[timestamp]` | Any | +| `get_input_notes_commitment` | Returns the input notes commitment hash.
**Inputs:** `[]`
**Outputs:** `[INPUT_NOTES_COMMITMENT]` | Any | +| `get_output_notes_commitment` | Returns the output notes commitment hash.
**Inputs:** `[]`
**Outputs:** `[OUTPUT_NOTES_COMMITMENT]` | Any | +| `get_num_input_notes` | Returns the total number of input notes consumed by this transaction.
**Inputs:** `[]`
**Outputs:** `[num_input_notes]` | Any | +| `get_num_output_notes` | Returns the current number of output notes created in this transaction.
**Inputs:** `[]`
**Outputs:** `[num_output_notes]` | Any | +| `execute_foreign_procedure` | Executes the provided procedure against the foreign account.
**Inputs:** `[foreign_account_id_prefix, foreign_account_id_suffix, FOREIGN_PROC_ROOT,
**Outputs:** `[
**Inputs:** `[]`
**Outputs:** `[block_height_delta]` | Any | +| `update_expiration_block_delta` | Updates the transaction expiration delta.
**Inputs:** `[block_height_delta]`
**Outputs:** `[]` | Any | + +## Faucet Procedures (`miden::faucet`) + +Faucet procedures allow reading and writing to faucet accounts to mint and burn assets. + +| Procedure | Description | Context | +| ------------------------------ | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------- | +| `create_fungible_asset` | Creates a fungible asset for the faucet the transaction is being executed against.
**Inputs:** `[amount]`
**Outputs:** `[ASSET]` | Faucet | +| `create_non_fungible_asset` | Creates a non-fungible asset for the faucet the transaction is being executed against.
**Inputs:** `[DATA_HASH]`
**Outputs:** `[ASSET]` | Faucet | +| `mint` | Mint an asset from the faucet the transaction is being executed against.
**Inputs:** `[ASSET]`
**Outputs:** `[ASSET]` | Native & Account & Faucet | +| `burn` | Burn an asset from the faucet the transaction is being executed against.
**Inputs:** `[ASSET]`
**Outputs:** `[ASSET]` | Native & Account & Faucet | +| `get_total_issuance` | Returns the total issuance of the fungible faucet the transaction is being executed against.
**Inputs:** `[]`
**Outputs:** `[total_issuance]` | Faucet | +| `is_non_fungible_asset_issued` | Returns a boolean indicating whether the provided non-fungible asset has been already issued by this faucet.
**Inputs:** `[ASSET]`
**Outputs:** `[is_issued]` | Faucet | + +## Asset Procedures (`miden::asset`) + +Asset procedures provide utilities for creating fungible and non-fungible assets. + +| Procedure | Description | Context | +| -------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------- | +| `build_fungible_asset` | Builds a fungible asset for the specified fungible faucet and amount.
**Inputs:** `[faucet_id_prefix, faucet_id_suffix, amount]`
**Outputs:** `[ASSET]` | Any | +| `build_non_fungible_asset` | Builds a non-fungible asset for the specified non-fungible faucet and data hash.
**Inputs:** `[faucet_id_prefix, DATA_HASH]`
**Outputs:** `[ASSET]` | Any | diff --git a/versioned_docs/version-0.12 (stable)/miden-base/state.md b/versioned_docs/version-0.12 (stable)/miden-base/state.md new file mode 100644 index 0000000..6257959 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/miden-base/state.md @@ -0,0 +1,131 @@ +--- +sidebar_position: 6 +--- + +# State + +The `State` describes the current condition of all accounts, notes, nullifiers and their statuses. Reflecting the "current reality" of the protocol at any given time. + +## What is the purpose of the Miden state model? + +By employing a concurrent `State` model with local execution and proving, Miden achieves three primary properties: preserving privacy, supporting parallel transactions, and reducing state-bloat by minimizing on-chain data storage. + +Miden’s `State` model focuses on: + +- **Concurrency:** + Multiple transactions can be processed concurrently by distinct actors using local transaction execution which improves throughput and efficiency. + +- **Flexible data storage:** + Users can store data privately on their own devices or within the network. This approach reduces reliance on the network for data availability, helps maintain user sovereignty, and minimizes unnecessary on-chain storage. + +- **Privacy:** + By using notes and nullifiers, Miden ensures that value transfers remain confidential. Zero-knowledge proofs allow users to prove correctness without revealing sensitive information. + +## State model components + +The Miden node maintains three databases to describe `State`: + +1. Accounts +2. Notes +3. Nullifiers + +
+ .default})
+
+ .default})
+
+ .default})
+
+ .default})
+
+ .default})
+
+ {children}
+
+ );
+}
+
+function AdmonitionHeading({ icon, title }: Pick
+ {icon}
+ {/* {title} */}
+
+ );
+}
+
+function AdmonitionContent({ children }: Pick{children}
+ ) : null;
+}
+
+export default function AdmonitionLayout(props: Props): ReactNode {
+ const { type, icon, title, children, className } = props;
+ return (
+
+ .default})
+
+ .default})
+
+
+Span and attribute naming is unstable and should not be relied upon. This also means changes here will not be considered
+breaking, however we will do our best to document them.
+
+
+
+### RPC request/response
+
+Not yet implemented.
+
+### Block building
+
+This trace covers the building, proving and submission of a block.
+
+
+
+
+### Batch building
+
+This trace covers the building and proving of a batch.
+
+Span tree
+ +```sh +block_builder.build_block +┝━ block_builder.select_block +│ ┝━ mempool.lock +│ ┕━ mempool.select_block +┝━ block_builder.get_block_inputs +│ ┝━ block_builder.summarize_batches +│ ┕━ store.client.get_block_inputs +│ ┕━ store.rpc/GetBlockInputs +│ ┕━ store.server.get_block_inputs +│ ┝━ validate_nullifiers +│ ┝━ read_account_ids +│ ┝━ validate_note_commitments +│ ┝━ select_block_header_by_block_num +│ ┝━ select_note_inclusion_proofs +│ ┕━ select_block_headers +┝━ block_builder.prove_block +│ ┝━ execute_program +│ ┕━ block_builder.simulate_proving +┝━ block_builder.inject_failure +┕━ block_builder.commit_block + ┝━ store.client.apply_block + │ ┕━ store.rpc/ApplyBlock + │ ┕━ store.server.apply_block + │ ┕━ apply_block + │ ┝━ select_block_header_by_block_num + │ ┕━ update_in_memory_structs + ┝━ mempool.lock + ┕━ mempool.commit_block + ┕━ mempool.revert_expired_transactions + ┕━ mempool.revert_transactions +``` + +
+
+
+## Verbosity
+
+We log important spans and events at `info` level or higher, which is also the default log level.
+
+Changing this level should rarely be required - let us know if you're missing information that should be at `info`.
+
+The available log levels are `trace`, `debug`, `info` (default), `warn`, `error` which can be configured using the
+`RUST_LOG` environment variable e.g.
+
+```sh
+export RUST_LOG=debug
+```
+
+The verbosity can also be specified by component (when running them as a single process):
+
+```sh
+export RUST_LOG=warn,block-producer=debug,rpc=error
+```
+
+The above would set the general level to `warn`, and the `block-producer` and `rpc` components would be overridden to
+`debug` and `error` respectively. Though as mentioned, it should be unusual to do this.
+
+## Configuration
+
+The OpenTelemetry trace exporter is enabled by adding the `--enable-otel` flag to the node's start command:
+
+```sh
+miden-node bundled start --enable-otel
+```
+
+The exporter can be configured using environment variables as specified in the official
+[documents](httpthes://opentelemetry.io/docs/specs/otel/protocol/exporter/).
+
+Span tree
+ +```sh +batch_builder.build_batch +┝━ batch_builder.wait_for_available_worker +┝━ batch_builder.select_batch +│ ┝━ mempool.lock +│ ┕━ mempool.select_batch +┝━ batch_builder.get_batch_inputs +│ ┕━ store.client.get_batch_inputs +┝━ batch_builder.propose_batch +┝━ batch_builder.prove_batch +┝━ batch_builder.inject_failure +┕━ batch_builder.commit_batch + ┝━ mempool.lock + ┕━ mempool.commit_batch +``` + +
+Not all options are fully supported. We are limited to what the Rust OpenTelemetry implementation supports. If you have any problems please open an issue and we'll do our best to resolve it.
+
+Note: we only support gRPC as the export protocol.
+
+
+
+#### Example: Honeycomb configuration
+
+This is based off Honeycomb's OpenTelemetry
+[setup guide](https://docs.honeycomb.io/send-data/opentelemetry/#using-the-honeycomb-opentelemetry-endpoint).
+
+```sh
+OTEL_EXPORTER_OTLP_ENDPOINT=https://api.honeycomb.io:443 \
+OTEL_EXPORTER_OTLP_HEADERS="x-honeycomb-team=your-api-key" \
+miden-node bundled start --enable-otel
+```
+
+### Honeycomb queries, triggers and board examples
+
+#### Example Queries
+
+Here are some useful Honeycomb queries to help monitor your Miden node:
+
+**Block building performance**:
+
+```honeycomb
+VISUALIZE
+HEATMAP(duration_ms) AVG(duration_ms)
+WHERE
+name = "block_builder.build_block"
+GROUP BY block.number
+ORDER BY block.number DESC
+LIMIT 100
+```
+
+**Batch processing latency**:
+
+```honeycomb
+VISUALIZE
+HEATMAP(duration_ms) AVG(duration_ms) P95(duration_ms)
+WHERE
+name = "batch_builder.build_batch"
+GROUP BY batch.id
+LIMIT 100
+```
+
+**Block proving failures**:
+
+```honeycomb
+VISUALIZE
+COUNT
+WHERE
+name = "block_builder.build_block"
+AND status = "error"
+CALCULATE RATE
+```
+
+**Transaction volume by block**:
+
+```honeycomb
+VISUALIZE
+MAX(transactions.count)
+WHERE
+name = "block_builder.build_block"
+GROUP BY block.number
+ORDER BY block.number DESC
+LIMIT 100
+```
+
+**RPC request rate by endpoint**:
+
+```honeycomb
+VISUALIZE
+COUNT
+WHERE
+name contains "rpc"
+GROUP BY name
+```
+
+**RPC latency by endpoint**:
+
+```honeycomb
+VISUALIZE
+AVG(duration_ms) P95(duration_ms)
+WHERE
+name contains "rpc"
+GROUP BY name
+```
+
+**RPC errors by status code**:
+
+```honeycomb
+VISUALIZE
+COUNT
+WHERE
+name contains "rpc"
+GROUP BY status_code
+```
+
+#### Example Triggers
+
+Create triggers in Honeycomb to alert you when important thresholds are crossed:
+
+**Slow block building**:
+
+- Query:
+
+```honeycomb
+VISUALIZE
+AVG(duration_ms)
+WHERE
+name = "block_builder.build_block"
+```
+
+- Trigger condition: `AVG(duration_ms) > 30000` (adjust based on your expected block time)
+- Description: Alert when blocks take too long to build (more than 30 seconds on average)
+
+**High failure rate**:
+
+- Query:
+
+```honeycomb
+VISUALIZE
+COUNT
+WHERE
+name = "block_builder.build_block" AND error = true
+```
+
+- Trigger condition: `COUNT > 100 WHERE error = true`
+- Description: Alert when more than 100 block builds are failing
+
+#### Advanced investigation with BubbleUp
+
+To identify the root cause of performance issues or errors, use Honeycomb's BubbleUp feature:
+
+1. Create a query for a specific issue (e.g., high latency for block building)
+2. Click on a specific high-latency point in the visualization
+3. Use BubbleUp to see which attributes differ significantly between normal and slow operations
+4. Inspect the related spans in the trace to pinpoint the exact step causing problems
+
+This approach helps identify patterns like:
+
+- Which types of transactions are causing slow blocks
+- Which specific operations within block/batch processing take the most time
+- Correlations between resource usage and performance
+- Common patterns in error cases
diff --git a/versioned_docs/version-0.12 (stable)/miden-node/operator/usage.md b/versioned_docs/version-0.12 (stable)/miden-node/operator/usage.md
new file mode 100644
index 0000000..fa48617
--- /dev/null
+++ b/versioned_docs/version-0.12 (stable)/miden-node/operator/usage.md
@@ -0,0 +1,132 @@
+---
+sidebar_position: 4
+---
+
+# Configuration and Usage
+
+As outlined in the [Architecture](./architecture) chapter, the node consists of several components which can be run
+separately or as a single bundled process. At present, the recommended way to operate a node is in bundled mode and is
+what this guide will focus on. Operating the components separately is very similar and should be relatively
+straight-forward to derive from these instructions.
+
+This guide focuses on basic usage. To discover more advanced options we recommend exploring the various help menus
+which can be accessed by appending `--help` to any of the commands.
+
+## Bootstrapping
+
+The first step in starting a new Miden network is to initialize the genesis block data. This is a
+one-off operation using the `bootstrap` command and by default the genesis block will contain a single
+faucet account.
+
+```sh
+# Create a folder to store the node's data.
+mkdir data
+
+# Bootstrap the node.
+#
+# This creates the node's database and initializes it with the genesis data.
+#
+# The genesis block currently contains a single public faucet account. The
+# secret for this account is stored in the `
+ {children}
+
+ );
+}
+
+function AdmonitionHeading({ icon, title }: Pick
+ {icon}
+ {/* {title} */}
+
+ );
+}
+
+function AdmonitionContent({ children }: Pick{children}
+ ) : null;
+}
+
+export default function AdmonitionLayout(props: Props): ReactNode {
+ const { type, icon, title, children, className } = props;
+ return (
+
+ {children}
+
+ );
+}
+
+function AdmonitionHeading({ icon, title }: Pick
+ {icon}
+ {/* {title} */}
+
+ );
+}
+
+function AdmonitionContent({ children }: Pick{children}
+ ) : null;
+}
+
+export default function AdmonitionLayout(props: Props): ReactNode {
+ const { type, icon, title, children, className } = props;
+ return (
+
+
+ Miden Web App
+Open your browser console to see WebClient logs.
+ +
+
+
+
+
+ Miden Web App
+Open your browser console to see WebClient logs.
+ +
+
+
+
+
+ Miden FPI Web App
+Open your browser console to see WebClient logs.
+ +
+
+
+
+
+ Miden Web App
+Open your browser console to see WebClient logs.
+ +
+
+
+ Selector Flags | Label | Value | +| ---------------------- | ---------------------------------------- | --------------- | ----- | +| `HASHER_LINEAR_HASH` | $\{0 \,\|\, 1, 0, 0\}$ | `1 + 0b001_0` | 3 | +| `HASHER_MP_VERIFY` | $\{0 \,\|\, 1, 0, 1\}$ | `1 + 0b101_0` | 11 | +| `HASHER_MR_UPDATE_OLD` | $\{0 \,\|\, 1, 1, 0\}$ | `1 + 0b011_0` | 7 | +| `HASHER_MR_UPDATE_NEW` | $\{0 \,\|\, 1, 1, 1\}$ | `1 + 0b111_0` | 15 | +| `HASHER_RETURN_HASH` | $\{0 \,\|\, 0, 0, 0\}$ | `1 + 0b000_0` | 1 | +| `HASHER_RETURN_STATE` | $\{0 \,\|\, 0, 0, 1\}$ | `1 + 0b100_0` | 9 | +| `BITWISE_AND` | $\{1, 0 \,\|\, 0\}$ | `1 + 0b0_01` | 2 | +| `BITWISE_XOR` | $\{1, 0 \,\|\, 1\}$ | `1 + 0b1_01` | 6 | +| `MEMORY_WRITE_ELEMENT` | $\{1, 1, 0 \,\|\, 0, 0\}$ | `1 + 0b00_011` | 4 | +| `MEMORY_WRITE_WORD` | $\{1, 1, 0 \,\|\, 0, 1\}$ | `1 + 0b10_011` | 20 | +| `MEMORY_READ_ELEMENT` | $\{1, 1, 0 \,\|\, 1, 0\}$ | `1 + 0b01_011` | 12 | +| `MEMORY_READ_WORD` | $\{1, 1, 0 \,\|\, 1, 1\}$ | `1 + 0b11_011` | 28 | +| `ACE_INIT` | $\{1, 1, 1, 0 \,\|\, - \}$ | `1 + 0b_0111` | 8 | +| `KERNEL_PROC_CALL` | $\{1, 1, 1, 1, 0 \,\|\, 0\}$ | `1 + 0b0_01111` | 16 | +| `KERNEL_PROC_INIT` | $\{1, 1, 1, 1, 0 \,\|\, 1\}$ | `1 + 0b1_01111` | 48 | + +## Chiplets module constraints + +### Chiplet constraints + +Each chiplet's internal constraints are defined in the documentation for the individual chiplets. To ensure that constraints are only ever selected for one chiplet at a time, the module's selector columns $s_0, s_1, s_2, s_3, s_4$ are combined into flags. Each chiplet's internal constraints are multiplied by its chiplet selector flag, and the degree of each constraint is correspondingly increased. + +This gives the following sets of constraints: + +> $$ +> (1 - s_0) \cdot c_{hash} = 0 \text{ | degree} = 1 + \deg(c_{hash}) +> $$ + +> $$ +> s_0 \cdot (1 - s_1) \cdot c_{bitwise} = 0 \text{ | degree} = 2 + \deg(c_{bitwise}) +> $$ + +> $$ +> s_0 \cdot s_1 \cdot (1 - s'_2) \cdot c_{memory} = 0 \text{ | degree} = 3 + \deg(c_{memory}) +> $$ + +> $$ +> s_0 \cdot s_1 \cdot (s_2) \cdot (1 - s'_3) \cdot c_{ace} = 0 \text{ | degree} = 4 + \deg(c_{ace}) +> $$ + +> $$ +> s_0 \cdot s_1 \cdot (s_2) \cdot (s_3) \cdot (1 - s'_4) \cdot c_{krom} = 0 \text{ | degree} = 5 + \deg(c_{krom}) +> $$ + +In the above: + +- $c_{hash}, c_{bitwise}, c_{memory}, c_{ace}, c_{krom}$ each represent an internal constraint from the indicated chiplet. +- $\deg(c)$ indicates the degree of the specified constraint. +- flags are applied in a like manner for all internal constraints in each respective chiplet. +- the selector for the memory chiplet excludes the last row of the chiplet (as discussed [above](#additional-requirements-for-stacking-execution-traces)). + +### Chiplet selector constraints + +We also need to ensure that the chiplet selector columns are set correctly. Although there are three columns for chiplet selectors, the stacked trace design means that they do not all act as selectors for the entire trace. Thus, selector constraints should only be applied to selector columns when they are acting as selectors. + +- $s_0$ acts as a selector for the entire trace. +- $s_1$ acts as a selector column when $s_0 = 1$. +- $s_2$ acts as a selector column when $s_0 = 1$ and $s_1 = 1$. +- $s_3$ acts as a selector column when $s_0 = 1$, $s_1 = 1$, and $s_2 = 1$. +- $s_4$ acts as a selector column when $s_0 = 1$, $s_1 = 1$, $s_2 = 1$, and $s_3 = 1$. + +Two conditions must be enforced for columns acting as chiplet selectors. + +1. When acting as a selector, the value in the selector column must be binary. +2. When acting as a selector, the value in the selector column may only change from $0 \rightarrow 1$. + +The following constraints ensure that selector values are binary. + +> $$ +> s_0^2 - s_0 = 0 \text{ | degree} = 2 +> s_0 \cdot (s_1^2 - s_1) = 0 \text{ | degree} = 3 +> s_0 \cdot s_1 \cdot (s_2^2 - s_2) = 0 \text{ | degree} = 4 +> s_0 \cdot s_1 \cdot s_2 \cdot (s_3^2 - s_3) = 0 \text{ | degree} = 5 +> s_0 \cdot s_1 \cdot s_2 \cdot s_3 \cdot (s_4^2 - s_4) = 0 \text{ | degree} = 6 +> $$ + +The following constraints ensure that the chiplets are stacked correctly by restricting selector values so they can only change from $0 \rightarrow 1$. + +> $$ +> s_0 \cdot (s_0 - s'_0) = 0 \text{ | degree} = 2 +> s_0 \cdot s_1 \cdot (s_1 - s'_1) \text{ | degree} = 3 +> s_0 \cdot s_1 \cdot s_2 \cdot (s_2 - s'_2) \text{ | degree} = 4 +> s_0 \cdot s_1 \cdot s_2 \cdot s_3 \cdot (s_3 - s'_3) \text{ | degree} = 5 +> s_0 \cdot s_1 \cdot s_2 \cdot s_3 \cdot s_4 \cdot (s_4 - s'_4) \text{ | degree} = 6 +> $$ + +In other words, the above constraints enforce that if a selector is $0$ in the current row, then it must be either $0$ or $1$ in the next row; if it is $1$ in the current row, it must be $1$ in the next row. + +## Chiplets bus + +The chiplets must be explicitly connected to the rest of the VM in order for it to use their operations. This connection must prove that all specialized operations which a given VM component claimed to offload to one of the chiplets were in fact executed by the correct chiplet with the same set of inputs and outputs as those used by the offloading component. + +This is achieved via a [bus](../lookups/index.md#communication-buses-in-miden-vm) called $b_{chip}$ where a request can be sent to any chiplet and a corresponding response will be sent back by that chiplet. + +The bus is implemented as a single [running product column](../lookups/multiset.md) where: + +- Each request is “sent” by computing an operation-specific lookup value from an [operation-specific label](#operation-labels), the operation inputs, and the operation outputs, and then dividing it out of the $b_{chip}$ running product column. +- Each chiplet response is “sent” by computing the same operation-specific lookup value from the label, inputs, and outputs, and then multiplying it into the $b_{chip}$ running product column. + +Thus, if the requests and responses match, then the bus column $b_{chip}$ will start and end with the value $1$. This condition is enforced by boundary constraints on the $b_{chip}$ column. +It is also possible to invoke chiplet computations through public inputs, by initializing the bus with requests that must be responded to by the chiplets. +In this case, the verifier computes the product of all randomness-reduced requests, treating it as a constant when evaluating the boundary constraint for the initial value of the bus column. +Currently, this is only used to request the initialization of kernel procedure digests for the kernel ROM chiplet. + +Note that the order of the requests and responses does not matter, as long as they are all included in $b_{chip}$. In fact, requests and responses for the same operation will generally occur at different cycles. + +### Chiplets bus constraints + +The chiplets bus constraints are defined by the components that use it to communicate. + +Lookup requests are sent to the chiplets bus by the following components: + +- The stack sends requests for [bitwise](../stack/u32_ops.md#u32and), [memory](../stack/io_ops.md#memory-access-operations), and [cryptographic hash operations](../stack/crypto_ops.md). +- The decoder sends requests for [hash operations](../decoder/index.md#program-block-hashing) for program block hashing. +- The decoder sends a procedure access request to the [Kernel ROM chiplet](./kernel_rom.md) for each `SYSCALL` during [program block hashing](../decoder/index.md#program-block-hashing). +- The verifier initializes the bus with requests to the [Kernel ROM chiplet](./kernel_rom.md) for each unique kernel procedure digest. + +Responses are provided by the [hash](./hasher.md#chiplets-bus-constraints), [bitwise](./bitwise.md#chiplets-bus-constraints), [memory](./memory.md#chiplets-bus-constraints), and [kernel ROM](./kernel_rom.md#chiplets-bus-constraints) chiplets. + +The chiplet bus can be initialized with randomness-reduced requests $v_0, v_1, \ldots$ by computing their product $v_{init} = \prod_i v_i$, and enforcing the boundary constraint in the first row to ensure +$b_{chip} = \frac{1}{v_{init}}$. +Note that $v_{init}$ is a constant, and therefore does not contribute to the constraint degree. + +> $$ +> b_{chip} \cdot v_{init} - 1 = 0 \text{ | degree} = 1 +> $$ + +## Chiplets virtual table + +_Note: over time, the use of this construction has evolved to the point where its name doesn't match the way it is used. This is documented in [issue #1779](https://github.com/0xMiden/miden-vm/issues/1779)._ + +The [virtual table](../lookups/multiset.md#virtual-tables) bus $vt_{chip}$ is used by several chiplets as a way to maintain and enforce the correctness of their internal states, and enable communication with each other. + +The hasher chiplet uses it as a way to store [sibling nodes](./hasher.md#sibling-table-constraints) when performing a Merkle tree update. +In particular, it expects an empty bus at the start of this operation, and ensures that all entries it inserts are removed once the new tree is finalized. +Consequently, the column representing this table must be equal to 1 at the boundaries of the hasher chiplet's trace, preventing communication with other chiplets. + +Other chiplets use the table as an extension of the chiplet bus, since both multi-sets are merged in the last row of the overall trace. + +This enables chiplets to make bus requests to other chiplets, without affecting the degree of the chiplet bus. +As currently implemented, a single constraint is required to include all requests made by the main trace and corresponding responses from the chiplets. +The degree of this constraint is the maximum of both message types and is currently reached by the requests by the main trace, +preventing chiplets from performing any requests using the same bus. +Instead, a chiplet can make a request through the $vt_{chip}$ bus, with the receiving chiplet responding through the main chiplet bus $b_{chip}$. + +At the moment, this feature is only used by the [ACE](./ace.md) allowing it to read inputs and circuit instructions stored in the memory chiplet. +Note that the [memory](./memory.md#chiplets-bus-constraints) chiplet responds via the chiplet bus $b_{chip}$. + +To combine these correctly, the [running product column](../lookups/multiset.md) for this table must be constrained not only at the beginning and the end of the trace, but also where the hash chiplet ends. + +### Chiplets virtual table constraints + +Although the [hasher chiplet](./hasher.md#sibling-table-constraints) ensures the sibling table is empty between any Merkle tree update computation, +we must also enforce this property at the boundary of the chiplet itself. +Using the hasher chiplet's selector $s_0$, the following constraint ensures the bus equals one whenever $s_0$ transitions. + +> $$ +> (s'_0 - s_0) \cdot (1 - vt_{chip}) = 0 \text{ | degree} = 2 +> $$ + +To connect the chiplet virtual table and the bus, we enforce the following constraint in the last row, ensuring the product of both their running products is 1. + +> $$ +> vt_{chip} \cdot b_{chip} - 1 = 0 \text{ | degree} = 2. +> $$ + +## Chiplet logUp bus + +An auxiliary [logUp bus](../lookups/logup.md) is available to chiplets, though it is currently only used by the [ACE chiplet](./ace.md#wire-bus) to check the wiring of the arithmetic circuit being evaluated. We refer to that chiplet's documentation for constraint applied to the corresponding auxiliary column. + +Since this column could later be used by other chiplets, we require boundary constraints over the entire chiplet trace to constrain the running sum to be zero in the first and final row of the auxiliary column. diff --git a/versioned_docs/version-0.12 (stable)/miden-vm/design/chiplets/kernel_rom.md b/versioned_docs/version-0.12 (stable)/miden-vm/design/chiplets/kernel_rom.md new file mode 100644 index 0000000..4103434 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/miden-vm/design/chiplets/kernel_rom.md @@ -0,0 +1,119 @@ +--- +title: "Kernel ROM Chiplet" +sidebar_position: 6 +--- + +# Kernel ROM chiplet + +The kernel ROM enables executing predefined kernel procedures. +These procedures are always executed in the root context and can only be accessed by a `SYSCALL` operation. +The chiplet tracks and enforces correctness of all kernel procedure calls as well as maintaining a list of all the procedures defined for the kernel, whether they are executed or not. +More background about Miden VM execution contexts can be found [here](../../user_docs/assembly/execution_contexts.md). + +## Kernel ROM trace + +The kernel ROM table consists of five columns. +The following example table shows the execution trace of the kernel ROM with procedure digests $a, b, c$, which were called 1, 2, and 0 times, respectively. +Each digest is included once to respond to the initialization request by the public inputs, and then repeated for each call made by the decoder. + +| $s_{first}$ | $r_0$ | $r_1$ | $r_2$ | $r_3$ | +|-------------|-------|-------|-------|-------| +| 1 | $a_0$ | $a_1$ | $a_2$ | $a_3$ | +| 0 | $a_0$ | $a_1$ | $a_2$ | $a_3$ | +| 1 | $b_0$ | $b_1$ | $b_2$ | $b_3$ | +| 0 | $b_0$ | $b_1$ | $b_2$ | $b_3$ | +| 0 | $b_0$ | $b_1$ | $b_2$ | $b_3$ | +| 1 | $c_0$ | $c_1$ | $c_2$ | $c_3$ | + +The meaning of columns in the above is as follows: + +- Column $s_{first}$ specifies the start of a block of rows with identical kernel procedure digests. +- $r_0, ..., r_3$ contain the digests of the kernel procedures. The values in these columns can change only when $s_{first}$ is set to 1 in the next row. Otherwise, the values in the $r$ columns remain the same. + +## Constraints + +> Note: the following assumes the ACE chiplet is included in the previous slot, whose documentation will be included +> in a subsequent PR. + +The following constraints are required to enforce the correctness of the kernel ROM trace. + +_Note: Unless otherwise stated, these constraints should also be multiplied by chiplets module's virtual flag $f_{krom}$ which is active in all rows the kernel ROM chiplet._ + +The $s_{first}$ column is a selector indicating the start of a new digest included in the kernel ROM chiplet trace. +In this row, the chiplet responds to a bus request made by the verifier to ensure consistency with the set of kernel procedure digests given as public inputs. + +As $s_{first}$ is a selector, it must be binary. + +> $$ +> s_{first}^2 - s_{first} = 0 \text{ | degree} = 2 +> $$ + + +The flag $s_{first}$ must be set to be 1 in the first row of the kernel ROM chiplet. +Otherwise, the digest in this row would not be matched with one of the input procedure roots. +This constraint is enforced in the last row of the previous trace, using selector columns from the [chiplets](index.md) module. +More precisely, we use the virtual $f_{ACE}$ flag from the chiplet selectors $s_0, s_1, \ldots, s_{ACE}$ which is active in all rows of the previous (in this case ACE) chiplet, +along with the selector $s_{ACE}$ which transitions from 0 to 1 in the last row, allowing us to target the first row of the kernel ROM trace. + +> $$ +> f_{ACE} \cdot s_{ACE}' \cdot (1 - s_{first}') = 0 \text{ | degree} = \deg(f_{prev}) + 2 +> $$ + +_Note that this selector need not be multiplied by the kernel ROM chiplet flag $chip\_s_4$, since it is only active when the previous chiplet is active._ + +The contiguity of the digests in a block is ensured by enforcing equality between digests across two consecutive rows, whenever the next row is not the start of a new block. +That is, when $s_{first}' = 0$, it must hold that $r_i = r_i'$. +We disable this constraint in the last row of the kernel ROM chiplet trace by using the kernel ROM chiplet selector $s_4'$, since the latter transitions from 0 to 1 when the next chiplet starts. + +> $$ +> (1 - s_4') \cdot (1 - s_{first}') \cdot (r_i' - r_i) = 0 \text{ | degree} = 3 +> $$ + +_**Note**: we could technically remove the selector $(1-s_4')$ since $s_4$ and $s_{first}$ correspond to the same column. We include it here for completeness though._ + +### Chiplets bus constraints + +The kernel ROM chiplet must ensure that all kernel procedure digests requested by the decoder correspond to one of the digests provided by the verifier through public inputs. +This is achieved by making use of the chiplet bus $b_{bus}$, responding to requests made by the decoder and by the verifier through public inputs. + +In the first row of each new block of hashes in the kernel ROM chiplet trace (i.e., when $s_{first} = 1$), the chiplet responds to a message $v_{init}$ requested by the verifier. +Since these initialization messages must match, the set of digests across all blocks must be equal to the set of procedure digests provided by the verifier (though not necessarily in the same order). + +Whenever a digest is requested by the decoder during program block hashing of the [`SYSCALL` operation](../decoder/constraints.md#block-hash-computation-constraints), a new row is added to the trace after the first row which is used to respond to one of the initialization requests made by the verifier using public inputs. +The chiplet responds to the request with a message $v_{call}$. + +In other words, the selector $s_{first}$ indicates whether the chiplet should respond to the decoder or the verifier initialization requests. +If a digest is requested $n$ times by the decoder, the same digest appears in a single block of length $n+1$. + +The variables $v_{init}$ and $v_{call}$ representing the bus messages contain reduced bus messages containing a kernel procedure digest. +Denoting the random values received from the verifier as $\alpha_0, \alpha_1$, etc., this can be defined as + +$$ +\begin{aligned} +\tilde{r} &= \sum_{i=0}^3 (\alpha_{i + 2} \cdot r_i) +v_{init} &= \alpha_0 + \alpha_1 \cdot \textsf{KERNEL\_PROC\_INIT} + \tilde{r} +v_{call} &= \alpha_0 + \alpha_1 \cdot \textsf{KERNEL\_PROC\_CALL} + \tilde{r} +\end{aligned} +$$ + +Here, $\textsf{KERNEL\_PROC\_INIT}$ and $\textsf{KERNEL\_PROC\_CALL}$ are the unique [operation labels](./index.md#operation-labels) for the kernel ROM bus message. + +Each row of the kernel ROM chiplet trace responds to either a procedure digest initialization or decoder call request. +Since the $s_{first}$ column defines which type of response is sent to the bus, it is used to combine both requests into a single constraint given by + +> $$ +> b'_{chip} = b_{chip} \cdot (s_{first} \cdot v_{init} + (1 - s_{first}) \cdot v_{call}) \text{ | degree} = 3. +> $$ + +The above simplifies to + +- $s_{first} = 1$: $b'_{chip} = b_{chip} \cdot v_{init}$, when responding to a $\textsf{KERNEL\_PROC\_INIT}$ request. +- $s_{first} = 0$: $b'_{chip} = b_{chip} \cdot v_{call}$, when responding to a $\textsf{KERNEL\_PROC\_CALL}$ request. + +The kernel procedure digests initialization requests are implemented by imposing a boundary constraint in the first row of the $b_{chip}$ column. +This is described in the [chiplets bus constraints](../chiplets/index.md#chiplets-bus-constraints). + +By using the bus to initialize the kernel ROM procedure digest in this way, the verifier only learns which procedures can be invoked but doesn't learn how often they were called, if at all. + +The full set of constraints applied to the $b_{chip}$ are described as part of the [chiplets bus constraints](../chiplets/index.md#chiplets-bus-constraints). + diff --git a/versioned_docs/version-0.12 (stable)/miden-vm/design/chiplets/memory.md b/versioned_docs/version-0.12 (stable)/miden-vm/design/chiplets/memory.md new file mode 100644 index 0000000..926501b --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/miden-vm/design/chiplets/memory.md @@ -0,0 +1,359 @@ +--- +title: "Memory Chiplet" +sidebar_position: 4 +--- + +# Memory chiplet + +Miden VM supports linear read-write random access memory. This memory is element-addressable, meaning that a single value is located at each address, although reading and writing values to/from memory in batches of four is supported. Each value is a field element in a $64$-bit prime field with modulus $2^{64} - 2^{32} + 1$. A memory address is a field element in the range $[0, 2^{32})$. + +In this note we describe the rationale for selecting the above design and describe AIR constraints needed to support it. + +The design makes extensive use of $16$-bit range checks. An efficient way of implementing such range checks is described [here](../range.md). + +## Alternative designs + +The simplest (and most efficient) alternative to the above design is contiguous write-once memory. To support such memory, we need to allocate just two trace columns as illustrated below. + + + +In the above, `addr` column holds memory address, and `value` column holds the field element representing the value stored at this address. Notice that some rows in this table are duplicated. This is because we need one row per memory access (either read or write operation). In the example above, value $b$ was first stored at memory address $1$, and then read from this address. + +The AIR constraints for this design are very simple. First, we need to ensure that values in the `addr` column either remain the same or are incremented by $1$ as we move from one row to the next. This can be achieved with the following constraint: + +$$ +(a' - a) \cdot (a' - a - 1) = 0 +$$ + +where $a$ is the value in `addr` column in the current row, and $a'$ is the value in this column in the next row. + +Second, we need to make sure that if the value in the `addr` column didn't change, the value in the `value` column also remained the same (i.e., a value stored in a given address can only be set once). This can be achieved with the following constraint: + +$$ +(v' - v) \cdot (a' - a - 1) = 0 +$$ + +where $v$ is the value in `value` column at the current row, and $v'$ is the value in this column in the next row. + +As mentioned above, this approach is very efficient: each memory access requires just $2$ trace cells. + +### Read-write memory + +Write-once memory is tricky to work with, and many developers may need to climb a steep learning curve before they become comfortable working in this model. Thus, ideally, we'd want to support read-write memory. To do this, we need to introduce additional columns as illustrated below. + + + +In the above, we added `clk` column, which keeps track of the clock cycle at which memory access happened. We also need to differentiate between memory reads and writes. To do this, we now use two columns to keep track of the value: `old val` contains the value stored at the address before the operation, and `new val` contains the value after the operation. Thus, if `old val` and `new val` are the same, it was a read operation. If they are different, it was a write operation. + +The AIR constraints needed to support the above structure are as follows. + +We still need to make sure memory addresses are contiguous: + +$$ +(a' - a) \cdot (a' - a - 1) = 0 +$$ + +Whenever memory address changes, we want to make sure that `old val` is set to $0$ (i.e., our memory is always initialized to $0$). This can be done with the following constraint: + +$$ +(a' - a) \cdot v_{old}' = 0 +$$ + +On the other hand, if memory address doesn't change, we want to make sure that `new val` in the current row is the same as `old val` in the next row. This can be done with the following constraint: + +$$ +(1 + a - a') \cdot (v_{new} - v_{old}') = 0 +$$ + +Lastly, we need to make sure that for the same address values in `clk` column are always increasing. One way to do this is to perform a $16$-bit range check on the value of $(i' - i - 1)$, where $i$ is the reference to `clk` column. However, this would mean that memory operations involving the same address must happen within $65536$ VM cycles from each other. This limitation would be difficult to enforce statically. To remove this limitation, we need to add two more columns as shown below: + + + +In the above column `d0` contains the lower $16$ bits of $(i' - i - 1)$ while `d1` contains the upper $16$ bits. The constraint needed to enforces this is as follows: + +$$ +(1 + a - a') \cdot ((i' - i - 1) - (2^{16} \cdot d_1' + d_0')) = 0 +$$ + +Additionally, we need to apply $16$-bit range checks to columns `d0` and `d1`. + +Overall, the cost of reading or writing a single element is now $6$ trace cells and $2$ $16$-bit range-checks. + +### Non-contiguous memory + +Requiring that memory addresses are contiguous may also be a difficult limitation to impose statically. To remove this limitation, we need to introduce one more column as shown below: + + + +In the above, the prover sets the value in the new column `t` to $0$ when the address doesn't change, and to $1 / (a' - a)$ otherwise. To simplify constraint description, we'll define variable $n$ computed as follows: + +$$ +n = (a' - a) \cdot t' +$$ + +Then, to make sure the prover sets the value of $t$ correctly, we'll impose the following constraints: + +$$ +n^2 - n = 0 +(1 - n) \cdot (a' - a) = 0 +$$ + +The above constraints ensure that $n=1$ whenever the address changes, and $n=0$ otherwise. We can then define the following constraints to make sure values in columns `d0` and `d1` contain either the delta between addresses or between clock cycles. + +| Condition | Constraint | Comments | +| --------- | ----------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------ | +| $n=1$ | $(a' - a) - (2^{16} \cdot d_1' + d_0') = 0$ | When the address changes, columns `d0` and `d1` at the next row should contain the delta between the old and the new address. | +| $n=0$ | $(i' - i - 1) - (2^{16} \cdot d_1' + d_0') = 0$ | When the address remains the same, columns `d0` and `d1` at the next row should contain the delta between the old and the new clock cycle. | + +We can combine the above constraints as follows: + +$$ +\left(n \cdot (a' - a) + (1 - n) \cdot (i' - i - 1)\right) - (2^{16} \cdot d_1' + d_0') = 0 +$$ + +The above constraint, in combination with $16$-bit range checks against columns `d0` and `d1` ensure that values in `addr` and `clk` columns always increase monotonically, and also that column `addr` may contain duplicates, while values in `clk` column must be unique for a given address. + +### Context separation + +In many situations it may be desirable to assign memories to different contexts. For example, when making a cross-contract calls, the memories of the caller and the callee should be separate. That is, the caller should not be able to access the memory of the callee and vice-versa. + +To accommodate this feature, we need to add one more column as illustrated below. + + + +This new column `ctx` should behave similarly to the address column: values in it should increase monotonically, and there could be breaks between them. We also need to change how the prover populates column `t`: + +- If the context changes, `t` should be set to the inverse $(c' - c)$, where $c$ is a reference to column `ctx`. +- If the context remains the same but the address changes, column `t` should be set to the inverse of $(a' - a)$. +- Otherwise, column `t` should be set to $0$. + +To simplify the description of constraints, we'll define two variables $n_0$ and $n_1$ as follows: + +$$ +n_0 = (c' - c) \cdot t' +n_1 = (a' - a) \cdot t' +$$ + +Thus, $n_0 = 1$ when the context changes, and $0$ otherwise. Also, $(1 - n_0) \cdot n_1 = 1$ when context remains the same and address changes, and $0$ otherwise. + +To make sure the prover sets the value of column `t` correctly, we'll need to impose the following constraints: + +$$ +n_0^2 - n_0 = 0 +(1 - n_0) \cdot (c' - c) = 0 +(1 - n_0) \cdot (n_1^2 - n_1) = 0 +(1 - n_0) \cdot (1 - n_1) \cdot (a' - a) = 0 +$$ + +We can then define the following constraints to make sure values in columns `d0` and `d1` contain the delta between contexts, between addresses, or between clock cycles. + +| Condition | Constraint | Comments | +| -------------------- | ----------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| $n_0=1$ | $(c' - c) - (2^{16} \cdot d_1' + d_0') = 0$ | When the context changes, columns `d0` and `d1` at the next row should contain the delta between the old and the new contexts. | +| $n_0=0$
$n_1=1$ | $(a' - a) - (2^{16} \cdot d_1' + d_0') = 0$ | When the context remains the same but the address changes, columns `d0` and `d1` at the next row should contain the delta between the old and the new addresses. | +| $n_0=0$
$n_1=0$ | $(i' - i - 1) - (2^{16} \cdot d_1' + d_0') = 0$ | When both the context and the address remain the same, columns `d0` and `d1` at the next row should contain the delta between the old and the new clock cycle. | + +We can combine the above constraints as follows: + +$$ +\left(n_0 \cdot (c' - c) + (1 - n_0) \cdot \left(n_1 \cdot (a - a') + (1 - n_1) \cdot (i' - i - 1) \right) \right) - (2^{16} \cdot d_1' + d_0') = 0 +$$ + +The above constraint, in combination with $16$-bit range checks against columns `d0` and `d1` ensure that values in `ctx`, `addr`, and `clk` columns always increase monotonically, and also that columns `ctx` and `addr` may contain duplicates, while the values in column `clk` must be unique for a given combination of `ctx` and `addr`. + +Notice that the above constraint has degree $5$. + +## Miden approach + +While the approach described above works, it comes at significant cost. Reading or writing a single value requires $8$ trace cells and $2$ $16$-bit range checks. Assuming a single range check requires roughly $2$ trace cells, the total number of trace cells needed grows to $12$. This is about $6$x worse the simple contiguous write-once memory described earlier. + +Miden VM frequently needs to deal with batches of $4$ field elements, which we call _words_. For example, the output of Rescue Prime Optimized hash function is a single word. A single 256-bit integer value can be stored as two words (where each element contains one $32$-bit value). Thus, we can optimize for this common use case by making the chiplet handle *words* as opposed to individual elements. That is, memory is still element-addressable in that each memory address stores a single field element, and memory addresses may be read or written individually. However, the chiplet also handles reading and writing elements in batches of four simultaneously, with the restriction that such batches be *word-aligned* addresses (*i.e.* the address is a multiple of 4). + +The layout of Miden VM memory table is shown below: + + + +where: + +- `rw` is a selector column which is set to $1$ for read operations and $0$ for write operations. +- `ew` is a selector column which is set to $1$ when a word is being accessed, and $0$ when an element is being accessed. +- `ctx` contains context ID. Values in this column must increase monotonically but there can be gaps between two consecutive values of up to $2^{32}$. Also, two consecutive values can be the same. +- `word_addr` contains the memory address of the first element in the word. Values in this column must increase monotonically for a given context but there can be gaps between two consecutive values of up to $2^{32}$. Values in this column must be divisible by 4. Also, two consecutive values can be the same. +- `idx0` and `idx1` are selector columns used to identify which element in the word is being accessed. Specifically, the index within the word is computed as `idx1 * 2 + idx0`. + - However, when `ew` is set to $1$ (indicating that a word is accessed), these columns are meaningless and are set to $0$. +- `clk` contains clock cycle at which the memory operation happened. Values in this column must increase monotonically for a given context and memory word but there can be gaps between two consecutive values of up to $2^{32}$. + - Unlike the previously described approaches, we allow `clk` to be constant in the same context/word address, with the restriction that when this is the case, then only reads are allowed. +- `v0, v1, v2, v3` columns contain field elements stored at a given context/word/clock cycle after the memory operation. +- Columns `d0` and `d1` contain lower and upper $16$ bits of the delta between two consecutive context IDs, addresses, or clock cycles. Specifically: + - When the context changes within a frame, these columns contain $(ctx' - ctx)$ in the "next" row. + - When the context remains the same but the word address changes within a frame, these columns contain $(a' - a)$ in the "next" row. + - When both the context and the word address remain the same within a frame, these columns contain $(clk' - clk)$ in the "next" row. +- Column `t` contains the inverse of the delta between two consecutive context IDs, addresses, or clock cycles. Specifically: + - When the context changes within a frame, this column contains the inverse of $(ctx' - ctx)$ in the "next" row. + - When the context remains the same but the word address changes within a frame, this column contains the inverse of $(a' - a)$ in the "next" row. + - When both the context and the word address remain the same within a frame, this column contains the inverse of $(clk' - clk)$ in the "next" row. +- Column `f_scw` stands for "flag same context and word address", which is set to $1$ when the current and previous rows have the same context and word address, and $0$ otherwise. + +For every memory access operation (i.e., read or write a word or element), a new row is added to the memory table. If neither `ctx` nor `addr` have changed, the `v` columns are set to equal the values from the previous row (except for any element written to). If `ctx` or `addr` have changed, then the `v` columns are initialized to $0$ (except for any element written to). + +### AIR constraints + +We first define the memory chiplet selector flags. $s_0$, $s_1$ and $s_2$ will refer to the chiplet selector flags. + +- $f_{mem}$ is set to 1 when the current row is in the memory chiplet. +$$ +f_{mem} = s_0 \cdot s_1 \cdot (1 - s_2) \text{ | degree} = 3 +$$ + +- $f_{mem\_nl}$ is set to 1 when the current row is in the memory chiplet, except for the last row of the chiplet. + +$$ +f_{mem\_nl} = s_0 \cdot s_1 \cdot (1 - s_2') \text{ | degree} = 3 +$$ + +- $f_{mem\_fr}$ is set to 1 when the next row is the first row of the memory chiplet. + +$$ +f_{mem\_fr} = (1 - s_0) \cdot f_{mem}' \text{ | degree} = 4 +$$ + +To simplify description of constraints, we'll define two variables $n_0$ and $n_1$ as follows: + +$$ +n_0 = \Delta ctx \cdot t' +n_1 = \Delta a \cdot t' +$$ + +Where $\Delta ctx = ctx' - ctx$ and $\Delta a = a' - a$. + +To make sure the prover sets the value of column `t` correctly, we'll need to impose the following constraints: + +$$ +f_{mem\_nl} \cdot (n_0^2 - n_0) = 0 \text{ | degree} = 7 +$$ + +$$ +f_{mem\_nl} \cdot (1 - n_0) \cdot \Delta ctx = 0 \text{ | degree} = 7 +$$ + +$$ +f_{mem\_nl} \cdot (1 - n_0) \cdot (n_1^2 - n_1) = 0 \text{ | degree} = 9 +$$ + +$$ +f_{mem\_nl} \cdot (1 - n_0) \cdot (1 - n_1) \cdot \Delta a = 0 \text{ | degree} = 8 +$$ + +The above constraints guarantee that when context changes, $n_0 = 1$. When context remains the same but word address changes, $(1 - n_0) \cdot n_1 = 1$. And when neither the context nor the word address change, $(1 - n_0) \cdot (1 - n_1) = 1$. + +We enforce that the `rw`, `ew`, `idx0` and `idx1` contain binary values. + +$$ +f_{mem} \cdot (rw^2 - rw) = 0 \text{ | degree} = 5 +$$ + +$$ +f_{mem} \cdot (ew^2 - ew) = 0 \text{ | degree} = 5 +$$ + +$$ +f_{mem} \cdot (idx0^2 - idx0) = 0 \text{ | degree} = 5 +$$ + +$$ +f_{mem} \cdot (idx1^2 - idx1) = 0 \text{ | degree} = 5 +$$ + + +To enforce the values of context ID, word address, and clock cycle grow monotonically as described in the previous section, we define the following constraint. + +$$ +f_{mem\_nl} \cdot \left(n_0 \cdot \Delta ctx + (1 - n_0) \cdot (n_1 \cdot \Delta a + (1 - n_1) \cdot \Delta clk) \right) - (2^{16} \cdot d_1' + d_0') = 0 \text{ | degree} = 8 +$$ + +In addition to this constraint, we also need to make sure that the values in registers $d_0$ and $d_1$ are less than $2^{16}$, and this can be done with [range checks](../range.md). + +Next, we need to ensure that when the context, word address and clock are constant in a frame, then only read operations are allowed in that clock cycle. + +$$ +f_{mem\_nl} \cdot f_{scw}' \cdot (1 - \Delta clk \cdot t') \cdot (1 - rw) \cdot (1 - rw') = 0 \text{ | degree} = 8 +$$ + + +Next, for all frames where the "current" and "next" rows are in the chiplet, we need to ensure that the value of the `f_scw` column in the "next" row is set to $1$ when the context and word address are the same, and $0$ otherwise. + +$$ +f_{mem\_nl} \cdot (f_{scw}' - (1 - n_0) \cdot (1-n_1)) = 0 \text{ | degree} = 7 +$$ + +Note that this does not constrain the value of `f_scw` in the first row of the chiplet. This is intended, as the first row's constraints do not depend on the previous row (since the previous row is not part of the same chiplet), and therefore do not depend on `f_scw` (see "first row" constraints below). + +Finally, we need to constrain the `v0, v1, v2, v3` columns. We will define a few variables to help in defining the constraints. + +$$ +\begin{align*} +f_0 &= (1 - idx1) \cdot (1 - idx0) \text{ | degree} = 2 +f_1 &= (1 - idx1) \cdot idx0 \text{ | degree} = 2 +f_2 &= idx1 \cdot (1 - idx0) \text{ | degree} = 2 +f_3 &= idx1 \cdot idx0 \text{ | degree} = 2 +\end{align*} +$$ + +The flag $f_i$ is set to $1$ when $v_i$ is being accessed, and $0$ otherwise. Next, for $0 \leq i < 4$, + +$$ +c_i = rw' + (1 - rw') \cdot (1 - ew') \cdot (1 - f_i') \text{ | degree} = 4 +$$ + +which is set to $1$ when $v_i$ is *not* written to, and $0$ otherwise. + +We're now ready to describe the constraints for the `v0, v1, v2, v3` columns. + +- For the first row of the chiplet (in the "next" position of the frame), for $0 \leq i < 4$, + +$$ +f_{mem\_fr} \cdot c_i \cdot v_i' = 0 \text{ | degree} = 9 +$$ + +That is, if the next row is the first row of the memory chiplet, and $v_i'$ is not written to, then $v_i'$ must be $0$. + +- For all rows of the chiplet except the first, for $0 \leq i < 4$, + +$$ +f_{mem\_nl} \cdot c_i \cdot (f_{scw}' \cdot (v_i' - v_i) + (1 - f_{scw}') \cdot v_i') = 0 \text{ | degree} = 9 +$$ + +That is, if $v_i$ is not written to, then either its value needs to be copied over from the previous row (when $f_{scw}' = 1$), or it must be set to 0 (when $f_{scw}' = 0$). + +#### Chiplets bus constraints {#chiplets-bus-constraints} + +Communication between the memory chiplet and the stack is accomplished via the chiplets bus $b_{chip}$. To respond to memory access requests from the stack, we need to divide the current value in $b_{chip}$ by the value representing a row in the memory table. + +##### Memory row value {#memory-row-value} + +This value can be computed as follows: + +$$ +\begin{align*} +v_{mem} = \alpha_0 + \alpha_1 \cdot op_{mem} + \alpha_2 \cdot ctx + \alpha_3 \cdot a + \alpha_4 \cdot clk + ew \cdot v_{word} + (1 - ew) \cdot v_{element} \text{ | degree} = 4 +\end{align*} +$$ + +where + +$$ +\begin{align*} +v_{word} &= \sum_{j=0}^3(\alpha_{j + 5} \cdot v_j) \text{ | degree} = 1 +v_{element} &= \alpha_5 \cdot \sum_{i=0}^3 f_i \cdot v_i \text{ | degree} = 3 +\end{align*} +$$ + +and where $op_{mem}$ is the appropriate [operation label](./index.md#operation-labels) of the memory access operation. + +To ensure that values of memory table rows are included into the chiplets bus, we impose the following constraint: + +$$ +b_{chip}' = b_{chip} \cdot v_{mem} \text{ | degree} = 5 +$$ + +On the stack side, for every memory access request, a corresponding value is divided out of the $b_{chip}$ column. Specifics of how this is done are described [here](../stack/io_ops.md#memory-access-operations). diff --git a/versioned_docs/version-0.12 (stable)/miden-vm/design/decoder/_category_.yml b/versioned_docs/version-0.12 (stable)/miden-vm/design/decoder/_category_.yml new file mode 100644 index 0000000..3f761fa --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/miden-vm/design/decoder/_category_.yml @@ -0,0 +1,4 @@ +label: "Program decoder" +# Determines where this documentation section appears relative to other sections in the parent folder +position: 2 +collapsed: true diff --git a/versioned_docs/version-0.12 (stable)/miden-vm/design/decoder/constraints.md b/versioned_docs/version-0.12 (stable)/miden-vm/design/decoder/constraints.md new file mode 100644 index 0000000..fb8e7bb --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/miden-vm/design/decoder/constraints.md @@ -0,0 +1,676 @@ +--- +title: "Miden VM Decoder AIR Constraints" +sidebar_position: 2 +--- + +# Miden VM decoder AIR constraints + +In this section we describe AIR constraints for Miden VM program decoder. These constraints enforce that the execution trace generated by the prover when executing a particular program complies with the rules described in the [previous section](./index.md). + +To refer to decoder execution trace columns, we use the names shown on the diagram below (these are the same names as in the previous section). Additionally, we denote the register containing the value at the top of the stack as $s_0$. + + + +We assume that the VM exposes a flag per operation which is set to $1$ when the operation is executed, and to $0$ otherwise. The notation for such flags is $f_{opname}$. For example, when the VM executes a `PUSH` operation, flag $f_{push} = 1$. All flags are mutually exclusive - i.e., when one flag is set to $1$ all other flags are set to $0$. The flags are computed based on values in `op_bits` columns. + +AIR constraints for the decoder involve operations listed in the table below. For each operation we also provide the degree of the corresponding flag and the effect that the operation has on the operand stack (however, in this section we do not cover the constraints needed to enforce the correct transition of the operand stack). + +| Operation | Flag | Degree | Effect on stack | +| --------- | :-----------: |:------:| ------------------------------------------------------------------------------------------------ | +| `JOIN` | $f_{join}$ | 5 | Stack remains unchanged. | +| `SPLIT` | $f_{split}$ | 5 | Top stack element is dropped. | +| `LOOP` | $f_{loop}$ | 5 | Top stack element is dropped. | +| `REPEAT` | $f_{repeat}$ | 4 | Top stack element is dropped. | +| `SPAN` | $f_{span}$ | 5 | Stack remains unchanged. | +| `RESPAN` | $f_{respan}$ | 4 | Stack remains unchanged. | +| `DYN` | $f_{dyn}$ | 5 | Stack remains unchanged. | +| `CALL` | $f_{call}$ | 4 | Stack remains unchanged. | +| `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}$ | 5 | An immediate value is pushed onto the stack. | +| `EMIT` | $f_{emit}$ | 7 | 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$. + +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 ensure 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. + +In the sections below, we describe constraints according to their logical grouping. However, we start out with a set of general constraints which are applicable to multiple parts of the decoder. + +## General constraints + +When `SPLIT` or `LOOP` operation is executed, the top of the operand stack must contain a binary value: + +> $$ +> (f_{split} + f_{loop}) \cdot (s_0^2 - s_0) = 0 \text{ | degree} = 7 +> $$ + +When a `DYN` operation is executed, the hasher registers must all be set to $0$: + +> $$ +> f_{dyn} \cdot (1 - h_i) = 0 \text { for } i \in [0, 8) \text{ | degree} = 6 +> $$ + +When `REPEAT` operation is executed, the value at the top of the operand stack must be $1$: + +> $$ +> f_{repeat} \cdot (1 - s_0) = 0 \text{ | degree} = 5 +> $$ + +Also, when `REPEAT` operation is executed, the value in $h_4$ column (the `is_loop_body` flag), must be set to $1$. This ensures that `REPEAT` operation can be executed only inside a loop: + +> $$ +> f_{repeat} \cdot (1 - h_4) = 0 \text{ | degree} = 5 +> $$ + +When `RESPAN` operation is executed, we need to make sure that the block ID is incremented by $8$: + +> $$ +> f_{respan} \cdot (a' - a - 8) = 0 \text{ | degree} = 5 +> $$ + +When `END` operation is executed and we are exiting a *loop* block (i.e., `is_loop`, value which is stored in $h_5$, is $1$), the value at the top of the operand stack must be $0$: + +> $$ +> f_{end} \cdot h_5 \cdot s_0 = 0 \text{ | degree} = 6 +> $$ + +Also, when `END` operation is executed and the next operation is `REPEAT`, values in $h_0, ..., h_4$ (the hash of the current block and the `is_loop_body` flag) must be copied to the next row: + +> $$ +> f_{end} \cdot f_{repeat}' \cdot (h_i' - h_i) = 0 \text { for } i \in [0, 5) \text{ | degree} = 9 +> $$ + +A `HALT` instruction can be followed only by another `HALT` instruction: + +> $$ +> f_{halt} \cdot (1 - f_{halt}') = 0 \text{ | degree} = 8 +> $$ + +When a `HALT` operation is executed, block address column must be $0$: + +> $$ +> f_{halt} \cdot a = 0 \text{ | degree} = 5 +> $$ + +Values in `op_bits` columns must be binary (i.e., either $1$ or $0$): + +> $$ +> b_i^2 - b_i = 0 \text{ for } i \in [0, 7) \text{ | degree} = 2 +> $$ + +When the value in `in_span` column is set to $1$, control flow operations cannot be executed on the VM, but when `in_span` flag is $0$, only control flow operations can be executed on the VM: + +> $$ +> 1 - sp - f_{ctrl} = 0 \text{ | degree} = 5 +> $$ + +## Block hash computation constraints +As described [previously](./index.md#program-block-hashing), when the VM starts executing a new block, it also initiates computation of the block's hash. There are two separate methodologies for computing block hashes. + +For *join*, *split*, and *loop* blocks, the hash is computed directly from the hashes of the block's children. The prover provides these child hashes non-deterministically by populating registers $h_0,..., h_7$. For *dyn*, the hasher registers are populated with zeros, so the resulting hash is a constant value. The hasher is initialized using the hash chiplet, and we use the address of the hasher as the block's ID. The result of the hash is available $7$ rows down in the hasher table (i.e., at row with index equal to block ID plus $7$). We read the result from the hasher table at the time the `END` operation is executed for a given block. + +For *basic* blocks, the hash is computed by absorbing a linear sequence of instructions (organized into operation groups and batches) into the hasher and then returning the result. The prover provides operation batches non-deterministically by populating registers $h_0, ..., h_7$. Similarly to other blocks, the hasher is initialized using the hash chiplet at the start of the block, and we use the address of the hasher as the ID of the first operation batch in the block. As we absorb additional operation batches into the hasher (by executing `RESPAN` operation), the batch address is incremented by $8$. This moves the "pointer" into the hasher table $8$ rows down with every new batch. We read the result from the hasher table at the time the `END` operation is executed for a given block. + +### Chiplets bus constraints + +The decoder communicates with the hash chiplet via the [chiplets bus](../chiplets/index.md#chiplets-bus). This works by dividing values of the multiset check column $b_{chip}$ by the values of operations providing inputs to or reading outputs from the hash chiplet. A constraint to enforce this would look as $b_{chip}' \cdot u = b_{chip}$, where $u$ is the value which defines the operation. + +In constructing value of $u$ for decoder AIR constraints, we will use the following labels (see [here](../chiplets/hasher.md#multiset-check-constraints) for an explanation of how values for these labels are computed): + +* $m_{bp}$ this label specifies that we are starting a new hash computation. +* $m_{abp}$ this label specifies that we are absorbing the next sequence of $8$ elements into an ongoing hash computation. +* $m_{hout}$ this label specifies that we are reading the result of a hash computation. + +To simplify constraint description, we define the following variables: + +$$ +h_{init} = \alpha_0 + \alpha_1 \cdot m_{bp} + \alpha_2 \cdot a' + \sum_{i=0}^7(\alpha_{i + 8} \cdot h_i) +$$ + +In the above, $h_{init}$ can be thought of as initiating a hasher with address $a'$ and absorbing $8$ elements from the hasher state ($h_0, ..., h_7$) into it. Control blocks are always padded to fill the hasher rate and as such the $\alpha_4$ (first capacity register) term is set to $0$. + +$$ +h_{abp} = \alpha_0 + \alpha_1 \cdot m_{abp} + \alpha_2 \cdot a' + \sum_{i=0}^7(\alpha_{i + 8} \cdot h_i) +$$ + +It should be noted that $a$ refers to a column in the decoder, as depicted. The addresses in this column are set using the address from the hasher chiplet for the corresponding hash initialization / absorption / return. In the case of $h_{abp}$ the value of the address in column $a$ in the current row of the decoder is set to equal the value of the address of the row in the hasher chiplet where the previous absorption (or initialization) occurred. $a'$ is the address of the next row of the decoder, which is set to equal the address in the hasher chiplet where the absorption referred to by the $h_{abp}$ label is happening. + +$$ +h_{res} = \alpha_0 + \alpha_1 \cdot m_{hout} + \alpha_2 \cdot (a + 7) + \sum_{i=0}^3(\alpha_{i + 8} \cdot h_i) +$$ + +In the above, $a$ represents the address value in the decoder which corresponds to the hasher chiplet address at which the hasher was initialized (or the last absorption took place). As such, $a + 7$ corresponds to the hasher chiplet address at which the result is returned. + +$$ +f_{ctrli} = f_{join} + f_{split} + f_{loop} \text{ | degree} = 5 +$$ + +In the above, $f_{ctrli}$ is set to $1$ when a control flow operation that signifies the initialization of a control block is being executed on the VM (only those control blocks that don't do any concurrent requests to the chiplets bus). Otherwise, it is set to $0$. An exception is made for the `DYN`, `DYNCALL`, `CALL` and `SYSCALL` operations, since although they initialize a control block, they also run another concurrent bus request, and so are handled separately. + +$$ +d = \sum_{b=0}^6(b_i \cdot 2^i) +$$ + +In the above, $d$ represents the opcode value of the opcode being executed on the virtual machine. It is calculated via a bitwise combination of the op bits. We leverage the opcode value to achieve domain separation when hashing control blocks. This is done by populating the second capacity register of the hasher with the value $d$ via the $\alpha_5$ term when initializing the hasher. + +Using the above variables, we define operation values as described below. + +When a control block initializer operation (`JOIN`, `SPLIT`, `LOOP`) is executed, a new hasher is initialized and the contents of $h_0, ..., h_7$ are absorbed into the hasher. As mentioned above, the opcode value $d$ is populated in the second capacity register via the $\alpha_5$ term. + +$$ +u_{ctrli} = f_{ctrli} \cdot (h_{init} + \alpha_5 \cdot d) \text{ | degree} = 6 +$$ + +As mentioned previously, the value sent by the `SYSCALL` operation is defined separately, since in addition to communicating with the hash chiplet it must also send a kernel procedure access request to the kernel ROM chiplet. This value of this kernel procedure request is described by $k_{proc}$. + +$$ +k_{proc} = \alpha_6 + \alpha_7 \cdot op_{krom} + \sum_{i=0}^3 (\alpha_{i + 8} \cdot h_i) +$$ + +In the above, $op_{krom}$ is the unique [operation label](../chiplets/index.md#operation-labels) of the kernel procedure call operation. The values $h_0, h_1, h_2, h_3$ contain the root hash of the procedure being called, which is the procedure that must be requested from the kernel ROM chiplet. + +$$ +u_{syscall} = f_{syscall} \cdot (h_{init} + \alpha_5 \cdot d) \cdot k_{proc} \text{ | degree} = 6 +$$ + +The above value sends both the hash initialization request and the kernel procedure access request to the chiplets bus when the `SYSCALL` operation is executed. + +Similar to `SYSCALL`, `CALL` is handled separately, since in addition to communicating with the hash chiplet, it must also initialize the frame memory pointer (stored in memory at constant address `fmpaddr` with constant value `fmpinit`): + +$$ +m_{fmpwrite} = \alpha_0 + \alpha_1 \cdot m_{writeele} + \alpha_2 \cdot ctx' + \alpha_3 \cdot fmpaddr + \alpha_4 \cdot clk + alpha_5 \cdot fmpinit +$$ + +In the above, $m_{fmpwrite}$ represents a "write element" memory request equivalent to `mem[fmpaddr] = fmpinit` (in pseudo-code) in the new memory context (*i.e.* the memory context of the callee). Currently $fmpaddr = 2^{32} - 1$, and $fmpinit = 2^{31}$. + +$$ +u_{call} = f_{call} \cdot (h_{init} + \alpha_5 \cdot d) \cdot m_{fmpwrite} \text{ | degree} = 6 +$$ + +Similar to `SYSCALL` and `CALL`, `DYN` and `DYNCALL` are handled separately, since in addition to communicating with the hash chiplet they must also issue a memory read operation for the hash of the procedure being called. + +$$ +h_{dynordyncall} = \alpha_0 + \alpha_1 \cdot m_{bp} + \alpha_2 \cdot a' +$$ + +$$ +m_{dynordyncall} = \alpha_0 + \alpha_1 \cdot m_{read} + \alpha_2 \cdot ctx + \alpha_3 \cdot s_0 + \alpha_4 \cdot clk + <[\alpha_5 \dots \alpha_8], h[0 \dots 4]> +$$ + +$$ +u_{dyn} = f_{dyn} \cdot h_{dynordyncall} \cdot m_{dynordyncall} \text{ | degree} = 7 +$$ +$$ +u_{dyncall} = f_{dyncall} \cdot h_{dynordyncall} \cdot m_{dynordyncall} \cdot m_{fmpwrite} \text{ | degree} = 8 +$$ + +In the above, $h_{dynordyncall}$ can be thought of as $h_{init}$, but where the values used for the hasher decoder trace registers is all 0's. $m_{dynordyncall}$ represents a memory read request from memory address $s_0$ (the top stack element), where the result is placed in the first half of the decoder hasher trace, and where $m_{read}$ is a label that represents a memory element read request. Note that similar to `CALL`, `DYNCALL` also creates a new memory context, and hence must also initialize the `fmp`. + +When `SPAN` operation is executed, a new hasher is initialized and contents of $h_0, ..., h_7$ are absorbed into the hasher. The number of operation groups to be hashed is padded to a multiple of the rate width ($8$) and so the $\alpha_4$ is set to 0: + +$$ +u_{span} = f_{span} \cdot h_{init} \text{ | degree} = 6 +$$ + +When `RESPAN` operation is executed, contents of $h_0, ..., h_7$ (which contain the new operation batch) are absorbed into the hasher: + +$$ +u_{respan} = f_{respan} \cdot h_{abp} \text{ | degree} = 5 +$$ + +When `END` operation is executed, the hash result is copied into registers $h_0, .., h_3$: + +$$ +u_{end} = f_{end} \cdot h_{res} \text{ | degree} = 5 +$$ + +Using the above definitions, we can describe the constraint for computing block hashes as follows: + +> $$ +> b_{chip}' \cdot (u_{ctrli} + u_{syscall} + u_{dynordyncall} + u_{span} + u_{respan} + u_{end} + \\ +> 1 - (f_{ctrli} + f_{syscall} + f_{dyn} + f_{dyncall} + f_{span} + f_{respan} + f_{end})) = b_{chip} +> $$ + +We need to add $1$ and subtract the sum of the relevant operation flags to ensure that when none of the flags is set to $1$, the above constraint reduces to $b_{chip}' = b_{chip}$. + +The degree of this constraint is $9$. + +## Block stack table constraints +As described [previously](./index.md#block-stack-table), block stack table keeps track of program blocks currently executing on the VM. Thus, whenever the VM starts executing a new block, an entry for this block is added to the block stack table. And when execution of a block completes, it is removed from the block stack table. + +Adding and removing entries to/from the block stack table is accomplished as follows: +* To add an entry, we multiply the value in column $p_1$ by a value representing a tuple `(blk, prnt, is_loop, ctx_next, b0_next, b1_next, fn_hash_next)` +. A constraint to enforce this would look as $p_1' = p_1 \cdot v$, where $v$ is the value representing the row to be added. +* To remove an entry, we divide the value in column $p_1$ by a value representing a tuple `(blk, prnt, is_loop, ctx_next, b0_next, b1_next, fn_hash_next)`. A constraint to enforce this would look as $p_1' \cdot u = p_1$, where $u$ is the value representing the row to be removed. + +> Recall that the columns `ctx_next, b0_next, b1_next, fn_hash_next` are only set on `CALL`, `SYSCALL`, and their corresponding `END` block. Therefore, for simplicity, we will ignore them when documenting all other block types (such that their values are set to `0`). + +Before describing the constraints for the block stack table, we first describe how we compute the values to be added and removed from the table for each operation. In the below, for block start operations (`JOIN`, `SPLIT`, `LOOP`, `SPAN`) $a$ refers to the ID of the parent block, and $a'$ refers to the ID of the starting block. For `END` operation, the situation is reversed: $a$ is the ID of the ending block, and $a'$ is the ID of the parent block. For `RESPAN` operation, $a$ refers to the ID of the current operation batch, $a'$ refers to the ID of the next batch, and the parent ID for both batches is set by the prover non-deterministically in register $h_1$. + +When `JOIN` operation is executed, row $(a', a, 0)$ is added to the block stack table: + +$$ +v_{join} = f_{join} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a) \text{ | degree} = 6 +$$ + +When `SPLIT` operation is executed, row $(a', a, 0)$ is added to the block stack table: + +$$ +v_{split} = f_{split} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a) \text{ | degree} = 6 +$$ + +When `LOOP` operation is executed, row $(a', a, 1)$ is added to the block stack table if the value at the top of the operand stack is $1$, and row $(a', a, 0)$ is added to the block stack table if the value at the top of the operand stack is $0$: + +$$ +v_{loop} = f_{loop} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a + \alpha_3 \cdot s_0) \text{ | degree} = 6 +$$ + +When `SPAN` operation is executed, row $(a', a, 0)$ is added to the block stack table: + +$$ +v_{span} = f_{span} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a) \text{ | degree} = 6 +$$ + +When `RESPAN` operation is executed, row $(a, h_1', 0)$ is removed from the block stack table, and row $(a', h_1', 0)$ is added to the table. The prover sets the value of register $h_1$ at the next row to the ID of the parent block: + +$$ +u_{respan} = f_{respan} \cdot (\alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot h_1') \text{ | degree} = 5 +v_{respan} = f_{respan} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot h_1') \text{ | degree} = 5 +$$ + +When a `DYN` operation is executed, row $(a', a, 0)$ is added to the block stack table: + +$$ +v_{dyn} = f_{dyn} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a) \text{ | degree} = 6 +$$ + +When a `DYNCALL` operation is executed, row $(a', a, 0, ctx, b_0, b_1, \mathrm{fnhash}[0..3])$ is added to the block stack table: + +$$ +\begin{align*} +v_{dyncall} &= f_{dyncall} \cdot (\alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot a' + \alpha_4 \cdot ctx +&+ \alpha_5 \cdot b_0 + \alpha_6 \cdot b_1 + <[\alpha_7, \alpha_{10}], \mathrm{fnhash}[0..3]>) \text{ | degree} = 6 +\end{align*} +$$ + +When a `CALL` or `SYSCALL` operation is executed, row $(a', a, 0, ctx, b_0, b_1, \mathrm{fnhash}[0..3])$ is added to the block stack table: + +$$ +\begin{align*} +v_{callorsyscall} &= (f_{call} + f_{syscall}) \cdot (\alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot a' + \alpha_4 \cdot ctx +&+ \alpha_5 \cdot b_0 + \alpha_6 \cdot b_1 + <[\alpha_7, \alpha_{10}], \mathrm{fnhash}[0..3]>) \text{ | degree} = 5 +\end{align*} +$$ + +When `END` operation is executed, how we construct the row will depend on whether the `IS_CALL` or `IS_SYSCALL` values are set (stored in registers $h_6$ and $h_7$ respectively). If they are not set, then row $(a, a', h_5)$ is removed from the block span table (where $h_5$ contains the `is_loop` flag); otherwise, row $(a ,a', 0, ctx', b_0', b_1', \mathrm{fnhash}'[0..3])$. + +$$ +\begin{align*} +u_{endnocall} &=\alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot a' +u_{endcall} &= u_{endnocall} + \alpha_4 \cdot ctx' + \alpha_5 \cdot b_0' + \alpha_6 \cdot b_1' + <[\alpha_7, \alpha_{10}], \mathrm{fnhash}'[0..3]> +u_{end} &= f_{end} \cdot ((1 - h_6 - h_7) \cdot u_{endnocall} + (h_6 + h_7) \cdot u_{endcall} ) \text{ | degree} = 6 +\end{align*} +$$ + +Using the above definitions, we can describe the constraint for updating the block stack table as follows: + +> $$ +> p_1' \cdot (u_{end} + u_{respan} + 1 - (f_{end} + f_{respan})) = p_1 \cdot +> (v_{join} + v_{split} + v_{loop} + v_{span} + v_{respan} + v_{dyn} + v_{dyncall} + v_{callorsyscall} + 1 - +> (f_{join} + f_{split} + f_{loop} + f_{span} + f_{respan} + f_{dyn} + f_{dyncall} + f_{call} + f_{syscall})) +> $$ + +We need to add $1$ and subtract the sum of the relevant operation flags from each side to ensure that when none of the flags is set to $1$, the above constraint reduces to $p_1' = p_1$. + +The degree of this constraint is $7$. + +In addition to the above transition constraint, we also need to impose boundary constraints against the $p_1$ column to make sure the first and the last values in the column are set to $1$. This enforces that the block stack table starts and ends in an empty state. + +## Block hash table constraints +As described [previously](./index.md#block-hash-table), when the VM starts executing a new program block, it adds hashes of the block's children to the block hash table. And when the VM finishes executing a block, it removes the block's hash from the block hash table. This means that the block hash table gets updated when we execute the `JOIN`, `SPLIT`, `LOOP`, `REPEAT`, `DYN`, and `END` operations (executing `SPAN` operation does not affect the block hash table because a *basic* block has no children). + +Adding and removing entries to/from the block hash table is accomplished as follows: +* To add an entry, we multiply the value in column $p_2$ by a value representing a tuple `(prnt_id, block_hash, is_first_child, is_loop_body)`. A constraint to enforce this would look as $p_2' = p_2 \cdot v$, where $v$ is the value representing the row to be added. +* To remove an entry, we divide the value in column $p_2$ by a value representing a tuple `(prnt_id, block_hash, is_first_child, is_loop_body)`. A constraint to enforce this would look as $p_2' \cdot u = p_2$, where $u$ is the value representing the row to be removed. + +To simplify constraint descriptions, we define values representing left and right children of a block as follows: + +$$ +ch_1 = \alpha_0 + \alpha_1 \cdot a' + \sum_{i=0}^3(\alpha_{i+2} \cdot h_i) \text{ | degree} = 1 +ch_2 = \alpha_0 + \alpha_1 \cdot a' + \sum_{i=0}^3(\alpha_{i+2} \cdot h_{i+4}) \text{ | degree} = 1 +$$ + +Graphically, this looks like so: + + + +In a similar manner, we define a value representing the result of hash computation as follows: + +$$ +bh = \alpha_0 + \alpha_1 \cdot a' + \sum_{i=0}^3(\alpha_{i+2} \cdot h_i) + \alpha_7 \cdot f_{is\_loop\_body} \text{ | degree} = 1 +$$ + +Above, $f_{is\_loop\_body}$ refers to the value in the `IS_LOOP_BODY` column (already constrained to be 0 or 1), located in $h_4$. Also, note that we are not adding a flag indicating whether the block is the first child of a join block (i.e., $\alpha_6$ term is missing). It will be added later on. + +Using the above variables, we define row values to be added to and removed from the block hash table as follows. + +When `JOIN` operation is executed, hashes of both child nodes are added to the block hash table. We add $\alpha_6$ term to the first child value to differentiate it from the second child (i.e., this sets `is_first_child` to $1$): + +$$ +v_{join} = f_{join} \cdot (ch_1 + \alpha_6) \cdot ch_2 \text{ | degree} = 7 +$$ + +When `SPLIT` operation is executed and the top of the stack is $1$, hash of the *true* branch is added to the block hash table, but when the top of the stack is $0$, hash of the *false* branch is added to the block hash table: + +$$ +v_{split} = f_{split} \cdot (s_0 \cdot ch_1 + (1 - s_0) \cdot ch_2) \text{ | degree} = 7 +$$ + +When `LOOP` operation is executed and the top of the stack is $1$, hash of loop body is added to the block hash table. We add $\alpha_7$ term to indicate that the child is a body of a loop. The below also means that if the top of the stack is $0$, nothing is added to the block hash table as the expression evaluates to $0$: + +$$ +v_{loop} = f_{loop} \cdot s_0 \cdot (ch_1 + \alpha_7) \text{ | degree} = 7 +$$ + +When `REPEAT` operation is executed, hash of loop body is added to the block hash table. We add $\alpha_7$ term to indicate that the child is a body of a loop: + +$$v_{repeat} = f_{repeat} \cdot (ch_1 + \alpha_7) \text{ | } \text{degree} = 5$$ + +When `DYN`, `DYNCALL`, `CALL` or `SYSCALL` operation is executed, the hash of the child is added to the block hash table. In all cases, this child is found in the first half of the decoder hasher state. + +$$ +v_{allcalls} = (f_{dyn} + f_{dyncall} + f_{call} + f_{syscall}) \cdot ch_1 \text{ | degree} = 6 +$$ + +When `END` operation is executed, hash of the completed block is removed from the block hash table. However, we also need to differentiate between removing the first and the second child of a *join* block. We do this by looking at the next operation. Specifically, if the next operation is neither `END` nor `REPEAT` nor `HALT`, we know that another block is about to be executed, and thus, we have just finished executing the first child of a *join* block. Thus, if the next operation is neither `END` nor `REPEAT` nor `HALT` we need to set the term for $\alpha_6$ coefficient to $1$ as shown below: + +$$ +u_{end} = f_{end} \cdot (bh + \alpha_6 \cdot (1 - (f_{end}' + f_{repeat}' + f_{halt}'))) \text{ | } \text{degree} = 8 +$$ + +Using the above definitions, we can describe the constraint for updating the block hash table as follows: + +> $$ +> p_2' \cdot (u_{end} + 1 - f_{end}) = +> p_2 \cdot (v_{join} + v_{split} + v_{loop} + v_{repeat} + v_{allcalls} + 1 - (f_{join} + f_{split} + f_{loop} + f_{repeat} + f_{dyn} + f_{dyncall} + f_{call} + f_{syscall})) +> $$ + +We need to add $1$ and subtract the sum of the relevant operation flags from each side to ensure that when none of the flags is set to $1$, the above constraint reduces to $p_2' = p_2$. + +The degree of this constraint is $9$. + +In addition to the above transition constraint, we also need to set the following boundary constraints against the $p_2$ column: +* The first value in the column represents a row for the entire program. Specifically, the row tuple would be `(0, program_hash, 0, 0)`. This row should be removed from the table when the last `END` operation is executed. +* The last value in the column is $1$ - i.e., the block hash table is empty. + +## Basic block +Basic block constraints ensure proper decoding of basic blocks. In addition to the block stack table constraints and block hash table constraints described previously, decoding of basic blocks requires constraints described below. + +### In-span column constraints +The `in_span` column (denoted as $sp$) is used to identify rows which execute non-control flow operations. The values in this column are set as follows: + +* Executing a `SPAN` operation sets the value of `in_span` column to $1$. +* The value remains $1$ until the `END` operation is executed. +* If `RESPAN` operation is executed between `SPAN` and `END` operations, in the row at which `RESPAN` operation is executed `in_span` is set to $0$. It is then reset to $1$ in the following row. +* In all other cases, value in the `in_span` column should be $0$. + +The picture below illustrates the above rules. + + + +To enforce the above rules we need the following constraints. + +When executing `SPAN` or `RESPAN` operation, the next value in $sp$ column must be set to $1$: + +> $$ +> (f_{span} + f_{respan}) \cdot (1 - sp') = 0 \text{ | degree} = 6 +> $$ + +When the next operation is `END` or `RESPAN`, the next value in $sp$ column must be set $0$. + +> $$ +> (f_{end}' + f_{respan}') \cdot sp' = 0 \text{ | degree} = 5 +> $$ + +In all other cases, the value in $sp$ column must be copied over to the next row: + +> $$ +> (1 - f_{span} - f_{respan} - f_{end}' - f_{respan}') \cdot (sp' - sp) = 0 \text{ | degree} = 6 +> $$ + +Additionally, we will need to impose a boundary constraint which specifies that the first value in $sp = 0$. Note, however, that we do not need to impose a constraint ensuring that values in $sp$ are binary - this will follow naturally from the above constraints. + +Also, note that the combination of the above constraints makes it impossible to execute `END` or `RESPAN` operations right after `SPAN` or `RESPAN` operations. + +### Block address constraints +When we are inside a *basic* block, values in block address columns (denoted as $a$) must remain the same. This can be enforced with the following constraint: + +> $$ +> sp \cdot (a' - a) = 0 \text{ | degree} = 2 +> $$ + +Notice that this constraint does not apply when we execute any of the control flow operations. For such operations, the prover sets the value of the $a$ column non-deterministically, except for the `RESPAN` operation. For the `RESPAN` operation the value in the $a$ column is incremented by $8$, which is enforced by a constraint described previously. + +Notice also that this constraint implies that when the next operation is the `END` operation, the value in the $a$ column must also be copied over to the next row. This is exactly the behavior we want to enforce so that when the `END` operation is executed, the block address is set to the address of the current span batch. + +### Group count constraints +The `group_count` column (denoted as $gc$) is used to keep track of the number of operation groups which remains to be executed in a basic block. + +In the beginning of a basic block (i.e., when `SPAN` operation is executed), the prover sets the value of $gc$ non-deterministically. This value is subsequently decremented according to the rules described below. By the time we exit the basic block (i.e., when `END` operation is executed), the value in $gc$ must be $0$. + +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 basic block), the count is decremented by $1$. +* When `SPAN`, `RESPAN`, or `PUSH` operations are executed, the count is decremented by $1$. + +Note that these rules imply that the `PUSH` operation (or any operation with an immediate value) 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: + +$$ +\Delta gc = gc - gc' +$$ + +Using this variable, we can describe the constraints against the $gc$ column as follows: + +Inside a *basic* 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 *basic* 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 +> $$ + +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 an operation with an immediate value, group count must be decremented by $1$: + +> $$ +> (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: + +> $$ +> \Delta gc \cdot (f_{end}' + f_{respan}') = 0 \text{ | degree} = 5 +> $$ + +When an `END` operation is executed, group count must be $0$: + +> $$ +> f_{end} \cdot gc = 0 \text{ | degree} = 5 +> $$ + +### Op group decoding constraints +Inside a *basic* block, register $h_0$ is used to keep track of operations to be executed in the current operation group. The value of this register is set by the prover non-deterministically at the time when the prover executes a `SPAN` or a `RESPAN` operation, or when processing of a new operation group within a batch starts. The picture below illustrates this. + + + +In the above: +* The prover sets the value of $h_0$ non-deterministically at row $0$. The value is set to an operation group containing operations `op0` through `op8`. +* As we start executing the group, at every row we "remove" the least significant operation from the group. This can be done by subtracting opcode of the operation from the group, and then dividing the result by $2^7$. +* By row $9$ the group is fully executed. This decrements the group count and set `op_index` to $0$ (constraints against `op_index` column are described in the next section). +* At row $10$ we start executing the next group with operations `op9` through `op11`. In this case, the prover populates $h_0$ with the group having its first operation (`op9`) already removed, and sets the `op_bits` registers to the value encoding `op9`. +* By row $12$ this group is also fully executed. + +To simplify the description of the constraints, we define the following variables: + +$$ +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 *basic* 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 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_{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_{imm}$ operations, no constraints are placed against $h_0$, and thus, the prover can populate this register non-deterministically. + +When we are in a *basic* block and the next operation is `END` or `RESPAN`, the current value in $h_0$ column must be $0$. + +> $$ +> sp \cdot (f_{end}' + f_{respan}') \cdot h_0 = 0 \text{ | degree} = 6 +> $$ + +### Op index constraints +The `op_index` column (denoted as $ox$) tracks index of an operation within its operation group. It is used to ensure that the number of operations executed per group never exceeds $9$. The index is zero-based, and thus, the possible set of values for $ox$ is between $0$ and $8$ (both inclusive). + +To simplify the description of the constraints, we will define the following variables: + +$$ +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 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$: + +> $$ +> (f_{span} + f_{respan}) \cdot ox' = 0 \text{ | degree} = 6 +> $$ + +When starting a new operation group inside a *basic* block, the next value of `op_index` must be set to $0$. Note that we multiply by $sp$ to exclude the cases when the group count is decremented because of `SPAN` or `RESPAN` operations: + +> $$ +> sp \cdot ng \cdot ox' = 0 \text{ | degree} = 6 +> $$ + +When inside a *basic* block but not starting a new operation group, `op_index` must be incremented by $1$. Note that we multiply by $sp'$ to exclude the cases when we are about to exit processing of an operation batch (i.e., the next operation is either `END` or `RESPAN`): + +> $$ +> sp \cdot sp' \cdot (1 - ng) \cdot (\Delta ox - 1) = 0 \text{ | degree} = 7 +> $$ + +Values of `op_index` must be in the range $[0, 8]$. + +> $$ +> \prod_{i=0}^{8}(ox - i) = 0 \text{ | degree} = 9 +> $$ + +### Op batch flags constraints +Operation batch flag columns (denoted $bc_0$, $bc_1$, and $bc_2$) are used to specify how many operation groups are present in an operation batch. This is relevant for the last batch in a basic block (or the first batch if there is only one batch in a block) as all other batches should be completely full (i.e., contain 8 operation groups). + +These columns are used to define the following 4 flags: + +* $f_{g8} = bc_0$: there are 8 operation groups in the batch. +* $f_{g4} = (1 - bc_0) \cdot bc_1 \cdot bc_2$: there are 4 operation groups in the batch. +* $f_{g2} = (1 - bc_0) \cdot (1 - bc_1) \cdot bc_2$: there are 2 operation groups in the batch. +* $f_{g1} = (1 - bc_0) \cdot bc_1 \cdot (1 - bc_2)$: there is only 1 operation groups in the batch. + +Notice that the degree of $f_{g8}$ is $1$, while the degree of the remaining flags is $3$. + +These flags can be set to $1$ only when we are executing `SPAN` or `RESPAN` operations as this is when the VM starts processing new operation batches. Also, for a given flag we need to ensure that only the specified number of operations groups are present in a batch. This can be done with the following constraints. + +All batch flags must be binary: + +> $$ +> bc_i^2 - bc_i = 0 \text{ for } i \in [0, 3) \text{ | degree} = 2 +> $$ + +When `SPAN` or `RESPAN` operations is executed, one of the batch flags must be set to $1$. + +> $$ +> (f_{span} + f_{respan}) - (f_{g1} + f_{g2} + f_{g4} + f_{g8}) = 0 \text{ | degree} = 5 +> $$ + +When neither `SPAN` nor `RESPAN` is executed, all batch flags must be set to $0$. + +$$ +(1 - (f_{span} + f_{respan})) \cdot (bc_0 + bc_1 + bc_2) = 0 \text{ | degree} = 6 +$$ + +When we have at most 4 groups in a batch, registers $h_4, ..., h_7$ should be set to $0$'s. + +> $$ +> (f_{g1} + f_{g2} + f_{g4}) \cdot h_i = 0 \text{ for } i \in [4, 8) \text{ | degree} = 4 +> $$ + +When we have at most 2 groups in a batch, registers $h_2$ and $h_3$ should also be set to $0$'s. + +> $$ +> (f_{g1} + f_{g2}) \cdot h_i = 0 \text{ for } i \in 2, 3 \text{ | degree} = 4 +> $$ + +When we have at most 1 groups in a batch, register $h_1$ should also be set to $0$. + +> $$ +> f_{g1} \cdot h_1 = 0 \text{ | degree} = 4 +> $$ + +### Op group table constraints +Op group table is used to ensure that all operation groups in a given batch are consumed before a new batch is started (i.e., via a `RESPAN` operation) or the execution of a *basic* block is complete (i.e., via an `END` operation). The op group table is updated according to the following rules: + +* When a new operation batch is started, we add groups from this batch to the table. To add a group to the table, we multiply the value in column $p_3$ by a value representing a tuple `(batch_id, group_pos, group)`. A constraint to enforce this would look as $p_3' = p_3 \cdot v$, where $v$ is the value representing the row to be added. Depending on the batch, we may need to add multiple groups to the table (i.e., $p_3' = p_3 \cdot v_1 \cdot v_2 \cdot v_3 ...$). Flags $f_{g1}$, $f_{g2}$, $f_{g4}$, and $f_{g8}$ are used to define how many groups to add. +* When a new operation group starts executing or when an immediate value is consumed, we remove the corresponding group from the table. To do this, we divide the value in column $p_3$ by a value representing a tuple `(batch_id, group_pos, group)`. A constraint to enforce this would look as $p_3' \cdot u = p_3$, where $u$ is the value representing the row to be removed. + +To simplify constraint descriptions, we first define variables representing the rows to be added to and removed from the op group table. + +When a `SPAN` or a `RESPAN` operation is executed, we compute the values of the rows to be added to the op group table as follows: + +$$ +v_i = \alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot (gc - i) + \alpha_3 \cdot h_{i} \text{ | degree} = 1 +$$ + +Where $i \in [1, 8)$. Thus, $v_1$ defines row value for group in $h_1$, $v_2$ defines row value for group $h_2$ etc. Note that batch address column comes from the next row of the block address column ($a'$). + +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_{imm}) + s_0' \cdot f_{push}) \text{ | degree} = 7 +$$ + +In the above, the value of the group is computed as $(h_0' \cdot 2^7 + op') \cdot (1 - f_{imm}) + 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$). + +We also define a flag which is set to $1$ when a group needs to be removed from the op group table. + +$$ +f_{dg} = sp \cdot \Delta gc \text{ | degree} = 2 +$$ + +The above says that we remove groups from the op group table whenever group count is decremented. We multiply by $sp$ to exclude the cases when the group count is decremented due to `SPAN` or `RESPAN` operations. + +Using the above variables together with flags $f_{g2}$, $f_{g4}$, $f_{g8}$ defined in the previous section, we describe the constraint for updating op group table as follows (note that we do not use $f_{g1}$ flag as when a batch consists of a single group, nothing is added to the op group table): + +> $$ +> p_3' \cdot (f_{dg} \cdot u + 1 - f_{dg}) = p_3 \cdot (f_{g2} \cdot v_1 + f_{g4} \cdot \prod_{i=1}^3 v_i + f_{g8} \cdot (\prod_{i=1}^7 v_i) + 1 - (f_{span} + f_{respan})) +> $$ + +The above constraint specifies that: +* When `SPAN` or `RESPAN` operations are executed, we add between $1$ and $7$ groups to the op group table; else, leave $p3$ untouched. +* When group count is decremented inside a *basic* block, we remove a group from the op group table; else, leave $p3'$ untouched. + +The degree of this constraint is $9$. + +In addition to the above transition constraint, we also need to impose boundary constraints against the $p_3$ column to make sure the first and the last value in the column is set to $1$. This enforces that the op group table table starts and ends in an empty state. diff --git a/versioned_docs/version-0.12 (stable)/miden-vm/design/decoder/index.md b/versioned_docs/version-0.12 (stable)/miden-vm/design/decoder/index.md new file mode 100644 index 0000000..d75cc56 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/miden-vm/design/decoder/index.md @@ -0,0 +1,738 @@ +--- +title: "Miden VM Program Decoder" +sidebar_position: 1 +--- + +# Miden VM Program decoder + +Miden VM program decoder is responsible for ensuring that a program with a given [MAST root](../programs.md) is executed by the VM. As the VM executes a program, the decoder does the following: + +1. Decodes a sequence of field elements supplied by the prover into individual operation codes (or *opcodes* for short). +2. Organizes the sequence of field elements into code blocks, and computes the hash of the program according to the methodology described [here](../programs.md#program-hash-computation). + +At the end of program execution, the decoder outputs the computed program hash. This hash binds the sequence of opcodes executed by the VM to a program the prover claims to have executed. The verifier uses this hash during the STARK proof verification process to verify that the proof attests to a correct execution of a specific program (i.e., the prover didn't claim to execute program $A$ while in fact executing a different program $B$). + +The sections below describe how Miden VM decoder works. Throughout these sections we make the following assumptions: + +1. An opcode requires $7$ bits to represent. +2. An immediate value requires one full field element to represent. +3. A `NOOP` operation has a numeric value of $0$, and thus, can be encoded as seven zeros. Executing a `NOOP` operation does not change the state of the VM, but it does advance operation counter, and may affect program hash. + +## Program execution + +Miden VM programs consist of a set of code blocks organized into a binary tree. The leaves of the tree contain linear sequences of instructions, and control flow is defined by the internal nodes of the tree. + +Managing control flow in the VM is accomplished by executing control flow operations listed in the table below. Each of these operations requires exactly one VM cycle to execute. + +| Operation | Description | +| --------- | ---------------------------------------------------------------------------- | +| `JOIN` | Initiates processing of a new [Join block](../programs.md#join-block). | +| `SPLIT` | Initiates processing of a new [Split block](../programs.md#split-block). | +| `LOOP` | Initiates processing of a new [Loop block](../programs.md#loop-block). | +| `REPEAT` | Initiates a new iteration of an executing loop. | +| `SPAN` | Initiates processing of a new [Basic block](../programs.md#basic-block). (historically called "span block") | +| `RESPAN` | Initiates processing of a new operation batch within a basic block. (historically called "span block") | +| `DYN` | Initiates processing of a new [Dyn block](../programs.md#dyn-block). | +| `CALL` | Initiates processing of a new [Call block](../programs.md#call-block). | +| `SYSCALL` | Initiates processing ofa new [Syscall block](../programs.md#syscall-block). | +| `END` | Marks the end of a program block. | +| `HALT` | Marks the end of the entire program. | + +Let's consider a simple program below: + +``` +begin +
$f_{ov}=1$ | $b'_0 = b_0 - 1$ | When the stack is shifted to the left and the overflow table is not empty, stack depth should be decremented by $1$. | +| otherwise | $b'_0 = b_0$ | In all other cases, stack depth should not change. | + +We can combine the above constraints into a single expression as follows: + +$$ +b'_0 - b_0 + f_{shl} \cdot f_{ov} - f_{shr} = 0 \text{ | degree} = 7 +$$ + +### Overflow table constraints + +When the stack is shifted to the right, a tuple $(k_0, s_{15}, b_1)$ should be added to the overflow table. We will denote value of the row to be added to the table as follows: + +$$ +v = \alpha_0 + \alpha_1 \cdot k_0 + \alpha_2 \cdot s_{15} + \alpha_3 \cdot b_1 +$$ + +When the stack is shifted to the left, a tuple $(b_1, s'_{15}, b'_1)$ should be removed from the overflow table. We will denote value of the row to be removed from the table as follows. + +$$ +u = \alpha_0 + \alpha_1 \cdot b_1 + \alpha_2 \cdot s'_{15} + \alpha_3 \cdot b'_1 +$$ + +Using the above variables, we can ensure that right and left shifts update the overflow table correctly by enforcing the following constraint: + +$$ +p_1' \cdot (u \cdot f_{shl} \cdot f_{ov} + 1 - f_{shl} \cdot f_{ov}) = p_1 \cdot (v \cdot f_{shr} + 1 - f_{shr}) \text{ | degree} = 9 +$$ + +The above constraint reduces to the following under various flag conditions: + +| Condition | Applied constraint | +| -------------------------------------------------- | -------------------- | +| $f_{shl}=1$, $f_{shr}=0$, $f_{ov}=0$ | $p_1' = p_1$ | +| $f_{shl}=1$, $f_{shr}=0$, $f_{ov}=1$ | $p_1' \cdot u = p_1$ | +| $f_{shl}=0$, $f_{shr}=1$, $f_{ov}=1 \text{ or } 0$ | $p_1' = p_1 \cdot v$ | +| $f_{shl}=0$, $f_{shr}=0$, $f_{ov}=1 \text{ or } 0$ | $p_1' = p_1$ | + +Notice that in the case of the left shift, the constraint forces the prover to set the next values of $s_{15}$ and $b_1$ to values $t_1$ and $t_2$ of the row removed from the overflow table. + +In case of a right shift, we also need to make sure that the next value of $b_1$ is set to the current value of $k_0$. This can be done with the following constraint: + +$$ +f_{shr} \cdot (b'_1 - k_0) = 0 \text{ | degree} = 7 +$$ + +In case of a left shift, when the overflow table is empty, we need to make sure that a $0$ is "shifted in" from the right (i.e., $s_{15}$ is set to $0$). This can be done with the following constraint: + +$$ +f_{shl} \cdot (1 - f_{ov}) \cdot s_{15}' = 0 \text{ | degree} = 8 +$$ + +### Boundary constraints +In addition to the constraints described above, we also need to enforce the following boundary constraints: +* $b_0 = 16$ at the first and at the last row of execution trace. +* $b_1 = 0$ at the first and at the last row of execution trace. +* $p_1 = 1$ at the first and at the last row of execution trace. diff --git a/versioned_docs/version-0.12 (stable)/miden-vm/design/stack/io_ops.md b/versioned_docs/version-0.12 (stable)/miden-vm/design/stack/io_ops.md new file mode 100644 index 0000000..dda8533 --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/miden-vm/design/stack/io_ops.md @@ -0,0 +1,202 @@ +--- +title: "Input / Output Operations" +sidebar_position: 7 +--- + +# Input / output operations +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/index.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/index.md#handling-immediate-values). + +The effect of this operation on the rest of the stack is: +* **Right shift** starting from position $0$. + +### SDEPTH +Assume $a$ is the current depth of the stack stored in the stack bookkeeping register $b_0$ (as described [here](./index.md#stack-representation)). The `SDEPTH` pushes $a$ onto the stack. The diagram below illustrates this graphically. + + + +Stack transition for this operation must satisfy the following constraints: + +$$ +s_0' - b_0 = 0 \text{ | degree} = 1 +$$ + +The effect of this operation on the rest of the stack is: +* **Right shift** starting from position $0$. + +### ADVPOP +Assume $a$ is an element at the top of the advice stack. The `ADVPOP` operation removes $a$ from the advice stack and pushes it onto the operand stack. The diagram below illustrates this graphically. + + + +The `ADVPOP` operation does not impose any constraints against the first element of the operand stack. + +The effect of this operation on the rest of the operand stack is: +* **Right shift** starting from position $0$. + +### ADVPOPW +Assume $a$, $b$, $c$, and $d$, are the elements at the top of the advice stack (with $a$ being on top). The `ADVPOPW` operation removes these elements from the advice stack and puts them onto the operand stack by overwriting the top $4$ stack elements. The diagram below illustrates this graphically. + + + +The `ADVPOPW` operation does not impose any constraints against the top $4$ elements of the operand stack. + +The effect of this operation on the rest of the operand stack is: +* **No change** starting from position $4$. + +## Memory access operations +Miden VM exposes several operations for reading from and writing to random access memory. Memory in Miden VM is managed by the [Memory chiplet](../chiplets/memory.md). + +Communication between the stack and the memory chiplet is accomplished via the chiplet bus $b_{chip}$. To make requests to the chiplet bus we need to divide its current value by the value representing memory access request. The structure of memory access request value is described [here](../chiplets/memory.md#memory-row-value). + +To enforce the correctness of memory access, we can use the following constraint: + +$$ +b_{chip}' \cdot u_{mem} = b_{chip} \text{ | degree} = 2 +$$ + +In the above, $u_{mem}$ is the value of memory access request. Thus, to describe AIR constraint for memory operations, it is sufficient to describe how $u_{mem}$ is computed. We do this in the following sections. + +### MLOADW +Assume that the word with elements $v_0, v_1, v_2, v_3$ is located in memory starting at address $a$. The `MLOADW` operation pops an element off the stack, interprets it as a memory address, and replaces the remaining 4 elements at the top of the stack with values located at the specified address. The diagram below illustrates this graphically. + + + +To simplify description of the memory access request value, we first define a variable for the value that represents the state of memory after the operation: + +$$ +v = \sum_{i=0}^3\alpha_{i+5} \cdot s_{3-i}' +$$ + +Using the above variable, we define the value representing the memory access request as follows: + +$$ +u_{mem} = \alpha_0 + \alpha_1 \cdot op_{mem\_readword} + \alpha_2 \cdot ctx + \alpha_3 \cdot s_0 + \alpha_4 \cdot clk + v +$$ + +In the above: +- $op_{mem\_readword}$ is the unique [operation label](../chiplets/index.md#operation-labels) of the memory "read word" operation. +- $ctx$ is the identifier of the current memory context. +- $s_0$ is the memory address from which the values are to be loaded onto the stack. +- $clk$ is the current clock cycle of the VM. + +The effect of this operation on the rest of the stack is: +* **Left shift** starting from position $5$. + +### MLOAD +Assume that the element $v$ is located in memory at address $a$. The `MLOAD` operation pops an element off the stack, interprets it as a memory address, and pushes the element located at the specified address to the stack. The diagram below illustrates this graphically. + + + + +We define the value representing the memory access request as follows: + +$$ +u_{mem} = \alpha_0 + \alpha_1 \cdot op_{mem\_readelement} + \alpha_2 \cdot ctx + \alpha_3 \cdot s_0 + \alpha_4 \cdot clk + \alpha_5 \cdot v +$$ + +In the above: +- $op_{mem\_readelement}$ is the unique [operation label](../chiplets/index.md#operation-labels) of the memory "read element" operation. +- $ctx$ is the identifier of the current memory context. +- $s_0$ is the memory address from which the value is to be loaded onto the stack. +- $clk$ is the current clock cycle of the VM. + +The effect of this operation on the rest of the stack is: +* **No change** starting from position $1$. + +### MSTOREW +The `MSTOREW` operation pops an element off the stack, interprets it as a memory address, and writes the remaining $4$ elements at the top of the stack into memory starting at the specified address. The stored elements are not removed from the stack. The diagram below illustrates this graphically. + + + +After the operation the contents of memory at addresses $a$, $a+1$, $a+2$, $a+3$ would be set to $v_0, v_1, v_2, v_3$, respectively. + +To simplify description of the memory access request value, we first define a variable for the value that represents the state of memory after the operation: + +$$ +v = \sum_{i=0}^3\alpha_{i+5} \cdot s_{3-i}' +$$ + +Using the above variable, we define the value representing the memory access request as follows: + +$$ +u_{mem} = \alpha_0 + \alpha_1 \cdot op_{mem\_writeword} + \alpha_2 \cdot ctx + \alpha_3 \cdot s_0 + \alpha_4 \cdot clk + v +$$ + +In the above: +- $op_{mem\_writeword}$ is the unique [operation label](../chiplets/index.md#operation-labels) of the memory "write word" operation. +- $ctx$ is the identifier of the current memory context. +- $s_0$ is the memory address into which the values from the stack are to be saved. +- $clk$ is the current clock cycle of the VM. + +The effect of this operation on the rest of the stack is: +* **Left shift** starting from position $1$. + +### MSTORE +The `MSTORE` operation pops an element off the stack, interprets it as a memory address, and writes the remaining element at the top of the stack into memory at the specified memory address. The diagram below illustrates this graphically. + + + +After the operation the contents of memory at address $a$ would be set to $b$. + +We define the value representing the memory access request as follows: + +$$ +u_{mem} = \alpha_0 + \alpha_1 \cdot op_{mem\_writeelement} + \alpha_2 \cdot ctx + \alpha_3 \cdot s_0 + \alpha_4 \cdot clk + \alpha_5 \cdot v +$$ + +In the above: +- $op_{mem\_writeelement} $ is the unique [operation label](../chiplets/index.md#operation-labels) of the memory "write element" operation. +- $ctx$ is the identifier of the current memory context. +- $s_0$ is the memory address into which the value from the stack is to be saved. +- $clk$ is the current clock cycle of the VM. + +The effect of this operation on the rest of the stack is: +* **Left shift** starting from position $1$. + +### MSTREAM + +The `MSTREAM` operation loads two words from memory, and replaces the top 8 elements of the stack with them, element-wise, in stack order. The start memory address from which the words are loaded is stored in the 13th stack element (position 12). The diagram below illustrates this graphically. + + + +After the operation, the memory address is incremented by 8. + +$$ +s_{12}' = s_{12} + 8 +$$ + +To simplify description of the memory access request value, we first define variables for the values that represent the state of memory after the operation: + +$$ +v_1 = \sum_{i=0}^3\alpha_{i+5} \cdot s_{7-i}' +$$ + +$$ +v_2 = \sum_{i=0}^3\alpha_{i+5} \cdot s_{3-i}' +$$ + +Using the above variables, we define the values representing the memory access request as follows: + +$$ +u_{mem, 1} = \alpha_0 + \alpha_1 \cdot op_{mem\_readword} + \alpha_2 \cdot ctx + \alpha_3 \cdot s_{12} + \alpha_4 \cdot clk + v_1 +$$ + +$$ +u_{mem, 2} = \alpha_0 + \alpha_1 \cdot op_{mem\_readword} + \alpha_2 \cdot ctx + \alpha_3 \cdot (s_{12} + 4) + \alpha_4 \cdot clk + v_2 +$$ + +$$ +u_{mem} = u_{mem, 1} \cdot u_{mem, 2} +$$ + +In the above: +- $op_{mem\_readword}$ is the unique [operation label](../chiplets/index.md#operation-labels) of the memory "read word" operation. +- $ctx$ is the identifier of the current memory context. +- $s_{12}$ and $s_{12} + 4$ are the memory addresses from which the words are to be loaded onto the stack. +- $clk$ is the current clock cycle of the VM. + +The effect of this operation on the rest of the stack is: +* **No change** starting from position $8$ except position $12$. diff --git a/versioned_docs/version-0.12 (stable)/miden-vm/design/stack/op_constraints.md b/versioned_docs/version-0.12 (stable)/miden-vm/design/stack/op_constraints.md new file mode 100644 index 0000000..f10466e --- /dev/null +++ b/versioned_docs/version-0.12 (stable)/miden-vm/design/stack/op_constraints.md @@ -0,0 +1,311 @@ +--- +title: "Stack Operation Constraints" +sidebar_position: 2 +--- + +# Stack operation constraints + +In addition to the constraints described in the previous section, we need to impose constraints to check that each VM operation is executed correctly. + +For this purpose the VM exposes a set of operation-specific flags. These flags are set to $1$ when a given operation is executed, and to $0$ otherwise. The naming convention for these flags is $f_{opname}$. For example, $f_{dup}$ would be set to $1$ when `DUP` operation is executed, and to $0$ otherwise. Operation flags are discussed in detail in the section [below](#operation-flags). + +To describe how operation-specific constraints work, let's use an example with `DUP` operation. This operation pushes a copy of the top stack item onto the stack. The constraints we need to impose for this operation are as follows: + +$$ +f_{dup} \cdot (s'_0 - s_0) = 0 +f_{dup} \cdot (s'_{i+1} - s_i) = 0 \ \text{ for } i \in [0, 15) +$$ + +The first constraint enforces that the top stack item in the next row is the same as the top stack item in the current row. The second constraint enforces that all stack items (starting from item $0$) are shifted to the right by $1$. We also need to impose all the constraints discussed in the previous section, be we omit them here. + +Let's write similar constraints for `DUP1` operation, which pushes a copy of the second stack item onto the stack: + +$$ +f_{dup1} \cdot (s'_0 - s_1) = 0 +f_{dup1} \cdot (s'_{i+1} - s_i) = 0 \ \text{ for } i \in [0, 15) +$$ + +It is easy to notice that while the first constraint changed, the second constraint remained the same - i.e., we are still just shifting the stack to the right. + +In fact, for most operations it makes sense to make a distinction between constraints unique to the operation vs. more general constraints which enforce correct behavior for the stack items not affected by the operation. In the subsequent sections we describe in detail only the former constraints, and provide high-level descriptions of the more general constraints. Specifically, we indicate how the operation affects the rest of the stack (e.g., shifts right starting from position $0$). + +## Operation flags +As mentioned above, operation flags are used as selectors to enforce operation-specific constraints. That is, they turn on relevant constraints for a given operation. In total, the VM provides $88$ unique operations, and thus, there are $88$ operation flags (not all of them currently used). + +Operation flags are mutually exclusive. That is, if one flag is set to $1$, all other flags are set to $0$. Also, one of the flags is always guaranteed to be set to $1$. + +To compute values of operation flags we use _op bits_ registers located in the [decoder](../decoder/index.md#decoder-trace). These registers contain binary representations of operation codes (opcodes). Each opcode consists of $7$ bits, and thus, there are $7$ _op bits_ registers. We denote these registers as $b_0, ..., b_6$. The values are computed by multiplying the op bit registers in various combinations. Notice that binary encoding down below is showed in big-endian order, so the flag bits correspond to the reverse order of the _op bits_ registers, from $b_6$ to $b_0$. + +For example, the value of the flag for `NOOP`, which is encoded as `0000000`, is computed as follows: + +$$ +f_{noop} = (1 - b_6) \cdot (1 - b_5) \cdot (1 - b_4) \cdot (1 - b_3) \cdot (1 - b_2) \cdot (1 - b_1) \cdot (1 - b_0) +$$ + +While the value of the `DROP` operation, which is encoded as `0101001` is computed as follows: + +$$ +f_{drop} = (1 - b_6) \cdot b_5 \cdot (1 - b_4) \cdot b_3 \cdot (1 - b_2) \cdot (1 - b_1) \cdot b_0 +$$ + +As can be seen from above, the degree for both of these flags is $7$. Since degree of constraints in Miden VM can go up to $9$, this means that operation-specific constraints cannot exceed degree $2$. However, there are some operations which require constraints of higher degree (e.g., $3$ or even $5$). To support such constraints, we adopt the following scheme. + +We organize the operations into $4$ groups as shown below and also introduce two extra registers $e_0$ and $e_1$ for degree reduction: + +| $b_6$ | $b_5$ | $b_4$ | $b_3$ | $b_2$ | $b_1$ | $b_0$ | $e_0$ | $e_1$ | # of ops | degree | +| :---: | :---: | :---: | :---: | :---: | :---: | :---: | :---: | :---: | :------: | :----: | +| 0 | x | x | x | x | x | x | 0 | 0 | 64 | 7 | +| 1 | 0 | 0 | x | x | x | - | 0 | 0 | 8 | 6 | +| 1 | 0 | 1 | x | x | x | x | 1 | 0 | 16 | 5 | +| 1 | 1 | x | x | x | - | - | 0 | 1 | 8 | 4 | + +In the above: +* Operation flags for operations in the first group (with prefix `0`), are computed using all $7$ op bits, and thus their degree is $7$. +* Operation flags for operations in the second group (with prefix `100`), are computed using only the first $6$ op bits, and thus their degree is $6$. +* Operation flags for operations in the third group (with prefix `101`), are computed using all $7$ op bits. We use the extra register $e_0$ (which is set to $b_6 \cdot (1-b_5) \cdot b_4$) to reduce the degree by $2$. Thus, the degree of op flags in this group is $5$. +* Operation flags for operations in the fourth group (with prefix `11`), are computed using only the first $5$ op bits. We use the extra register $e_1$ (which is set to $b_6 \cdot b_5$) to reduce the degree by $1$. Thus, the degree of op flags in this group is $4$. + +How operations are distributed between these $4$ groups is described in the sections below. + +### No stack shift operations +This group contains $32$ operations which do not shift the stack (this is almost all such operations). Since the op flag degree for these operations is $7$, constraints for these operations cannot exceed degree $2$. + +| Operation | Opcode value | Binary encoding | Operation group | Flag degree | +|-----------|:------------:|:---------------:|:-----------------------------:|:-----------:| +| `NOOP` | $0$ | `000_0000` | [System ops](./system_ops.md) | $7$ | +| `EQZ ` | $1$ | `000_0001` | [Field ops](./field_ops.md) | $7$ | +| `NEG` | $2$ | `000_0010` | [Field ops](./field_ops.md) | $7$ | +| `INV` | $3$ | `000_0011` | [Field ops](./field_ops.md) | $7$ | +| `INCR` | $4$ | `000_0100` | [Field ops](./field_ops.md) | $7$ | +| `NOT` | $5$ | `000_0101` | [Field ops](./field_ops.md) | $7$ | +| `
+ {children}
+
+ );
+}
+
+function AdmonitionHeading({ icon, title }: Pick
+ {icon}
+ {/* {title} */}
+
+ );
+}
+
+function AdmonitionContent({ children }: Pick{children}
+ ) : null;
+}
+
+export default function AdmonitionLayout(props: Props): ReactNode {
+ const { type, icon, title, children, className } = props;
+ return (
+