diff --git a/background.html b/background.html index 45680a867a..ca1d240473 100644 --- a/background.html +++ b/background.html @@ -176,7 +176,7 @@

Polygon Miden VM

- +

Background Material

Proofs of execution generated by Miden VM are based on STARKs. A STARK is a novel proof-of-computation scheme that allows you to create an efficiently verifiable proof that a computation was executed correctly. The scheme was developed by Eli Ben-Sasson, Michael Riabzev et al. at Technion - Israel Institute of Technology. STARKs do not require an initial trusted setup, and rely on very few cryptographic assumptions.

Here are some resources to learn more about STARKs:

diff --git a/design/chiplets/bitwise.html b/design/chiplets/bitwise.html index 86e32eba82..3c7b52c6e4 100644 --- a/design/chiplets/bitwise.html +++ b/design/chiplets/bitwise.html @@ -176,7 +176,7 @@

Polygon Miden VM

- +

Bitwise chiplet

In this note we describe how to compute bitwise AND and XOR operations on 32-bit values and the constraints required for proving correct execution.

Assume that and are field elements in a 64-bit prime field. Assume also that and are known to contain values smaller than . We want to compute , where is either bitwise AND or XOR, and is a field element containing the result of the corresponding bitwise operation.

diff --git a/design/chiplets/hasher.html b/design/chiplets/hasher.html index 7d2e7436ab..80feedb095 100644 --- a/design/chiplets/hasher.html +++ b/design/chiplets/hasher.html @@ -176,7 +176,7 @@

Polygon Miden VM

- +

Hash chiplet

Miden VM "offloads" all hash-related computations to a separate hash processor. This chiplet supports executing the Rescue Prime Optimized hash function (or rather a specific instantiation of it) in the following settings:

    diff --git a/design/chiplets/kernel_rom.html b/design/chiplets/kernel_rom.html index 738afe1479..a0ea3e8f86 100644 --- a/design/chiplets/kernel_rom.html +++ b/design/chiplets/kernel_rom.html @@ -176,7 +176,7 @@

    Polygon Miden VM

    - +

    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.

    Kernel ROM trace

    diff --git a/design/chiplets/main.html b/design/chiplets/main.html index 2d60809cef..ab5f68fd65 100644 --- a/design/chiplets/main.html +++ b/design/chiplets/main.html @@ -176,7 +176,7 @@

    Polygon Miden VM

    - +

    Chiplets

    The Chiplets module contains specialized components dedicated to accelerating complex computations. Each chiplet specializes in executing a specific type of computation and is responsible for proving both the correctness of its computations and its own internal consistency.

    Currently, Miden VM relies on 4 chiplets:

    diff --git a/design/chiplets/memory.html b/design/chiplets/memory.html index b7c560095f..a41aabbfae 100644 --- a/design/chiplets/memory.html +++ b/design/chiplets/memory.html @@ -176,7 +176,7 @@

    Polygon Miden VM

    - +

    Memory chiplet

    Miden VM supports linear read-write random access memory. This memory is word-addressable, meaning, four values are located at each address, and we can read and write values to/from memory in batches of four. Each value is a field element in a -bit prime field with modulus . Memory address can be any field element.

    In this note we describe the rationale for selecting the above design and describe AIR constraints needed to support it.

    diff --git a/design/decoder/constraints.html b/design/decoder/constraints.html index fbcfdfbc55..3357d4ae74 100644 --- a/design/decoder/constraints.html +++ b/design/decoder/constraints.html @@ -176,7 +176,7 @@

    Polygon Miden VM

    - +

    Miden VM decoder AIR constraints

    In this section we describe AIR constraint 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.

    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 .

    diff --git a/design/decoder/main.html b/design/decoder/main.html index 2f846d9565..9008e7ae2c 100644 --- a/design/decoder/main.html +++ b/design/decoder/main.html @@ -176,7 +176,7 @@

    Polygon Miden VM

    - +

    Miden VM Program decoder

    Miden VM program decoder is responsible for ensuring that a program with a given MAST root is executed by the VM. As the VM executes a program, the decoder does the following:

      diff --git a/design/lookups/logup.html b/design/lookups/logup.html index 95fcfd958a..0fbec1851f 100644 --- a/design/lookups/logup.html +++ b/design/lookups/logup.html @@ -176,7 +176,7 @@

      Polygon Miden VM

      - +

      LogUp: multivariate lookups with logarithmic derivatives

      The description of LogUp can be found here. In MidenVM, LogUp is used to implement efficient communication buses.

      Using the LogUp construction instead of a simple multiset check with running products reduces the computational effort for the prover and the verifier. Given two columns and in the main trace where contains duplicates and does not (i.e. is part of the lookup table), LogUp allows us to compute two logarithmic derivatives and check their equality.

      diff --git a/design/lookups/main.html b/design/lookups/main.html index f30b21f5f3..1739ed2900 100644 --- a/design/lookups/main.html +++ b/design/lookups/main.html @@ -176,9 +176,9 @@

      Polygon Miden VM

      - +

      Lookup arguments in Miden VM

      -

      Zero knowledge virtual machines frequently make use of lookup arguments to enable performance optimizations. Miden VM uses two types of arguments: multiset checks and a multivariate lookup based on logarithmic derivatives known as LogUp. A brief introduction to multiset checks can be found here. The description of LogUp can be found here.

      +

      Zero knowledge virtual machines frequently make use of lookup arguments to enable performance optimizations. Miden VM uses two types of arguments: multiset checks and a multivariate lookup based on logarithmic derivatives known as LogUp. A brief introduction to multiset checks can be found here. The description of LogUp can be found here.

      In Miden VM, lookup arguments are used for two purposes:

      1. To prove the consistency of intermediate values that must persist between different cycles of the trace without storing the full data in the execution trace (which would require adding more columns to the trace).
        2. diff --git a/design/lookups/multiset.html b/design/lookups/multiset.html index 03a24f13fc..b2dd0308dc 100644 --- a/design/lookups/multiset.html +++ b/design/lookups/multiset.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Multiset checks

        A brief introduction to multiset checks can be found here. In Miden VM, multiset checks are used to implement virtual tables and efficient communication buses.

        Running product columns

        diff --git a/design/main.html b/design/main.html index 3fc2826844..ec3348a639 100644 --- a/design/main.html +++ b/design/main.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Design

        In the following sections, we provide in-depth descriptions of Miden VM internals, including all AIR constraints for the proving system. We also provide rationale for making specific design choices.

        Throughout these sections we adopt the following notations and assumptions:

        diff --git a/design/programs.html b/design/programs.html index 050c14ab20..733ba4ddc2 100644 --- a/design/programs.html +++ b/design/programs.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Programs in Miden VM

        Miden VM consumes programs in a form of a Merkelized Abstract Syntax Tree (MAST). This tree is a binary tree where each node is a code block. The VM starts execution at the root of the tree, and attempts to recursively execute each required block according to its semantics. If the execution of a code block fails, the VM halts at that point and no further blocks are executed. A set of currently available blocks and their execution semantics are described below.

        Code blocks

        diff --git a/design/range.html b/design/range.html index e4371a1ef8..bd5babe355 100644 --- a/design/range.html +++ b/design/range.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Range Checker

        Miden VM relies very heavily on 16-bit range-checks (checking if a value of a field element is between and ). For example, most of the u32 operations need to perform between two and four 16-bit range-checks per operation. Similarly, operations involving memory (e.g. load and store) require two 16-bit range-checks per operation.

        Thus, it is very important for the VM to be able to perform a large number of 16-bit range checks very efficiently. In this note we describe how this can be achieved using the LogUp lookup argument.

        diff --git a/design/stack/crypto_ops.html b/design/stack/crypto_ops.html index aca7d49124..cc631f8d72 100644 --- a/design/stack/crypto_ops.html +++ b/design/stack/crypto_ops.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Cryptographic operations

        In this section we describe the AIR constraints for Miden VM cryptographic operations.

        Cryptographic operations in Miden VM are performed by the Hash chiplet. Communication between the stack and the hash chiplet is accomplished via the chiplet bus . To make requests to and to read results from the chiplet bus we need to divide its current value by the value representing the request.

        diff --git a/design/stack/field_ops.html b/design/stack/field_ops.html index c0a0efcffd..40fa2d1df3 100644 --- a/design/stack/field_ops.html +++ b/design/stack/field_ops.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Field Operations

        In this section we describe the AIR constraints for Miden VM field operations (i.e., arithmetic operations over field elements).

        ADD

        diff --git a/design/stack/io_ops.html b/design/stack/io_ops.html index 5fb675d9b6..1298681271 100644 --- a/design/stack/io_ops.html +++ b/design/stack/io_ops.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        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

        diff --git a/design/stack/main.html b/design/stack/main.html index 0f2800d16d..f134cd9b68 100644 --- a/design/stack/main.html +++ b/design/stack/main.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Operand stack

        Miden VM is a stack machine. The stack is a push-down stack of practically unlimited depth (in practical terms, the depth will never exceed ), but only the top items are directly accessible to the VM. Items on the stack are elements in a prime field with modulus .

        To keep the constraint system for the stack manageable, we impose the following rules:

        diff --git a/design/stack/op_constraints.html b/design/stack/op_constraints.html index 36cf12831d..eee0fc0540 100644 --- a/design/stack/op_constraints.html +++ b/design/stack/op_constraints.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        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 when a given operation is executed, and to otherwise. The naming convention for these flags is . For example, would be set to when DUP operation is executed, and to otherwise. Operation flags are discussed in detail in the section below.

        diff --git a/design/stack/stack_ops.html b/design/stack/stack_ops.html index bf6b4135ae..4bbadaf434 100644 --- a/design/stack/stack_ops.html +++ b/design/stack/stack_ops.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Stack Manipulation

        In this section we describe the AIR constraints for Miden VM stack manipulation operations.

        PAD

        diff --git a/design/stack/system_ops.html b/design/stack/system_ops.html index a501f825a4..08543df7a1 100644 --- a/design/stack/system_ops.html +++ b/design/stack/system_ops.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        System Operations

        In this section we describe the AIR constraints for Miden VM system operations.

        NOOP

        diff --git a/design/stack/u32_ops.html b/design/stack/u32_ops.html index 8432a13045..d9a8d58586 100644 --- a/design/stack/u32_ops.html +++ b/design/stack/u32_ops.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        u32 Operations

        In this section we describe semantics and AIR constraints of operations over u32 values (i.e., 32-bit unsigned integers) as they are implemented in Miden VM.

        Range checks

        diff --git a/index.html b/index.html index a8f38a026d..4610d34ba8 100644 --- a/index.html +++ b/index.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Introduction

        Miden VM is a zero-knowledge virtual machine written in Rust. For any program executed on Miden VM, a STARK-based proof of execution is automatically generated. This proof can then be used by anyone to verify that the program was executed correctly without the need for re-executing the program or even knowing the contents of the program.

        Status and features

        diff --git a/intro/main.html b/intro/main.html index 1901a40fb4..fc428fe310 100644 --- a/intro/main.html +++ b/intro/main.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Introduction

        Miden VM is a zero-knowledge virtual machine written in Rust. For any program executed on Miden VM, a STARK-based proof of execution is automatically generated. This proof can then be used by anyone to verify that the program was executed correctly without the need for re-executing the program or even knowing the contents of the program.

        Status and features

        diff --git a/intro/overview.html b/intro/overview.html index 94e81b75e4..f4ed626687 100644 --- a/intro/overview.html +++ b/intro/overview.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Miden VM overview

        Miden VM is a stack machine. The base data type of the MV is a field element in a 64-bit prime field defined by modulus . This means that all values that the VM operates with are field elements in this field (i.e., values between and , both inclusive).

        Miden VM consists of four high-level components as illustrated below.

        diff --git a/intro/performance.html b/intro/performance.html index 59b54a0246..44dbf429ac 100644 --- a/intro/performance.html +++ b/intro/performance.html @@ -176,7 +176,7 @@

        Polygon Miden VM

        - +

        Performance

        The benchmarks below should be viewed only as a rough guide for expected future performance. The reasons for this are twofold:

          diff --git a/intro/usage.html b/intro/usage.html index d094eacd1a..2ae778206d 100644 --- a/intro/usage.html +++ b/intro/usage.html @@ -176,7 +176,7 @@

          Polygon Miden VM

          - +

          Usage

          Before you can use Miden VM, you'll need to make sure you have Rust installed. Miden VM v0.8 requires Rust version 1.75 or later.

          Miden VM consists of several crates, each of which exposes a small set of functionality. The most notable of these crates are:

          diff --git a/print.html b/print.html index 4a1ee1310d..09a836939b 100644 --- a/print.html +++ b/print.html @@ -177,7 +177,7 @@

          Polygon Miden VM

          - +

          Introduction

          Miden VM is a zero-knowledge virtual machine written in Rust. For any program executed on Miden VM, a STARK-based proof of execution is automatically generated. This proof can then be used by anyone to verify that the program was executed correctly without the need for re-executing the program or even knowing the contents of the program.

          Status and features

          @@ -213,7 +213,7 @@

          License

          Licensed under the MIT license.

          -
          +

          Miden VM overview

          Miden VM is a stack machine. The base data type of the MV is a field element in a 64-bit prime field defined by modulus . This means that all values that the VM operates with are field elements in this field (i.e., values between and , both inclusive).

          Miden VM consists of four high-level components as illustrated below.

          @@ -253,7 +253,7 @@

          +

          Usage

          Before you can use Miden VM, you'll need to make sure you have Rust installed. Miden VM v0.8 requires Rust version 1.75 or later.

          Miden VM consists of several crates, each of which exposes a small set of functionality. The most notable of these crates are:

          @@ -356,7 +356,7 @@

          Fibonacci 
          ./target/optimized/miden run -a miden/examples/fib/fib.masm -o fib.out

          This will dump the output of the program into the fib.out file. The output file will contain the state of the stack at the end of the program execution.

          -
          +

          Performance

          The benchmarks below should be viewed only as a rough guide for expected future performance. The reasons for this are twofold:

            @@ -418,7 +418,7 @@

            Recursive p
          1. On Apple M1/M2 platforms the built-in GPU is used for a part of proof generation process.
          2. On the Graviton platform, SVE vector extension is used to accelerate RPO computations.

-
+

Development Tools and Resources

The following tools are available for interacting with Miden VM:

-
+

Miden Debugger

The Miden debugger is a command-line interface (CLI) application, inspired by GNU gdb, which allows debugging of Miden assembly (MASM) programs. The debugger allows the user to step through the execution of the program, both forward and backward, either per clock cycle tick, or via breakpoints.

The Miden debugger supports the following commands:

@@ -486,7 +486,7 @@

Miden Debugger< exec.foo end -
+

Miden REPL

The Miden Read–eval–print loop (REPL) is a Miden shell that allows for quick and easy debugging of Miden assembly. After the REPL gets initialized, you can execute any Miden instruction, undo executed instructions, check the state of the stack and memory at a given point, and do many other useful things! When the REPL is exited, a history.txt file is saved. One thing to note is that all the REPL native commands start with an ! to differentiate them from regular assembly instructions.

Miden REPL can be started via the CLI repl command like so:

@@ -601,7 +601,7 @@

!undo

>> !undo 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0 -
+

User Documentation

In the following sections, we provide developer-focused documentation useful to those who want to develop on Miden VM or build compilers from higher-level languages to Miden VM.

This documentation consists of two high-level sections:

@@ -610,7 +610,7 @@

User Do
  • Miden Standard Library which provides descriptions of all procedures available in Miden Standard Library.

    • For info on how to run programs on Miden VM, please refer to the usage section in the introduction.

    -
    +

    Miden Assembly

    Miden assembly is a simple, low-level language for writing programs for Miden VM. It stands just above raw Miden VM instruction set, and in fact, many instructions of Miden assembly map directly to raw instructions of Miden VM.

    Before Miden assembly can be executed on Miden VM, it needs to be compiled into a Program MAST (Merkelized Abstract Syntax Tree) which is a binary tree of code blocks each containing raw Miden VM instructions.

    @@ -644,7 +644,7 @@

    Design goalsIn order to achieve the second and third goals, Miden assembly facilitates flow control via high-level constructs like while loops, if-else statements, and function calls with statically defined targets. Thus, for example, there are no explicit jump instructions.

    In order to achieve the fourth goal, Miden assembly retains direct access to the VM stack rather than abstracting it away with higher-level constructs and named variables.

    Lastly, in order to achieve the fifth goal, each instruction of Miden assembly can be encoded using a single byte. The resulting byte-code is simply a one-to-one mapping of instructions to their binary values.

    -
    +

    Code organization

    A Miden assembly program is just a sequence of instructions each describing a specific directive or an operation. You can use any combination of whitespace characters to separate one instruction from another.

    In turn, Miden assembly instructions are just keywords which can be parameterized by zero or more parameters. The notation for specifying parameters is keyword.param1.param2 - i.e., the parameters are separated by periods. For example, push.123 instruction denotes a push operation which is parameterized by value 123.

    @@ -782,7 +782,7 @@

    Comments

    end

    Documentation comments must precede a procedure declaration. Using them inside a procedure body is an error.

    -
    +

    Execution contexts

    Miden assembly program execution can span multiple isolated contexts. An execution context defines its own memory space which is not accessible from other execution contexts.

    All programs start executing in a root context. Thus, the main procedure of a program is always executed in the root context. To move execution into a different context, we can invoke a procedure using the call instruction. In fact, any time we invoke a procedure using the call instruction, the procedure is executed in a new context. We refer to all non-root contexts as user contexts.

    @@ -880,7 +880,7 @@

    Example

  • When syscall.baz is executed the second time, execution moves into the root context again. However, now, when caller is executed inside baz, the first 4 elements of the stack are populated with the hash of foo (not bar). This happens because this time around bar does not have its own context and baz is invoked from foo's context.
  • Finally, when baz returns, execution moves back to ctx1, and then as bar and foo return, back to ctx0, and the program terminates.
    • -
    +

    Flow control

    As mentioned above, Miden assembly provides high-level constructs to facilitate flow control. These constructs are:

      @@ -944,7 +944,7 @@

    +

    Field operations

    Miden assembly provides a set of instructions which can perform operations with raw field elements. These instructions are described in the tables below.

    While most operations place no restrictions on inputs, some operations expect inputs to be binary values, and fail if executed with non-binary inputs.

    @@ -1001,7 +1001,7 @@


    Fails if ext2div
    - (11 cycles)
    [b1, b0, a1, a0, ...][c1, c0,] fails if , where multiplication and inversion are as defined by the operations above -

    +

    u32 operations

    Miden assembly provides a set of instructions which can perform operations on regular two-complement 32-bit integers. These instructions are described in the tables below.

    For instructions where one or more operands can be provided as immediate parameters (e.g., u32wrapping_add and u32wrapping_add.b), we provide stack transition diagrams only for the non-immediate version. For the immediate version, it can be assumed that the operand with the specified name is not present on the stack.

    @@ -1065,7 +1065,7 @@


    Undefined if u32max
    - (9 cycles)[b, a, ...][c, ...]
    Undefined if -
    +

    Stack manipulation

    Miden VM stack is a push-down stack of field elements. The stack has a maximum depth of , but only the top elements are directly accessible via the instructions listed below.

    In addition to the typical stack manipulation instructions such as drop, dup, swap etc., Miden assembly provides several conditional instructions which can be used to manipulate the stack based on some condition - e.g., conditional swap cswap or conditional drop cdrop.

    @@ -1091,7 +1091,7 @@


    Fails if cdropw
    - (5 cycles)[c, B, A, ... ][D, ... ]
    Fails if -
    +

    Input / output operations

    Miden assembly provides a set of instructions for moving data between the operand stack and several other sources. These sources include: