diff --git a/design/lookups/logup.html b/design/lookups/logup.html index 8064d7c57c..318313b23f 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.

+

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.

In the above:

@@ -192,7 +192,7 @@

Usage in

logup_component_x

logup_table_t

Constraints

-

The diagrams above show running sum columns for computing the logarithmic derivatives for both and . As an optimization, we can combine these values into a single auxiliary column in the extension field that contains the running sum of values from both logarithmic derivatives. We'll refer to this column as a communication bus , since it communicates the lookup request from the component to the lookup table .

+

The diagrams above show running sum columns for computing the logarithmic derivatives for both and . As an optimization, we can combine these values into a single auxiliary column in the extension field that contains the running sum of values from both logarithmic derivatives. We'll refer to this column as a communication bus , since it communicates the lookup request from the component to the lookup table .

This can be expressed as follows:

diff --git a/design/stack/io_ops.html b/design/stack/io_ops.html index 0c98b804e6..4cbd28c9d6 100644 --- a/design/stack/io_ops.html +++ b/design/stack/io_ops.html @@ -315,7 +315,7 @@

MSTREAM

The effect of this operation on the rest of the stack is:

    -
  • No change starting from position except position
    • +
  • No change starting from position except position .

diff --git a/print.html b/print.html index 8acf8b797a..f8ecc39e11 100644 --- a/print.html +++ b/print.html @@ -721,7 +721,7 @@

Constants

Miden assembly supports constant declarations. These constants are scoped to the module they are defined in and can be used as immediate parameters for Miden assembly instructions. Constants are supported as immediate values for the following instructions: push, assert, assertz, asert_eq, assert_eqw, locaddr, loc_load, loc_loadw, loc_store, loc_storew, mem_load, mem_loadw, mem_store, mem_storew.

-

Constants must be declared right after module imports and before any procedures or program bodies. A constant's name must start with an upper-case letter and can contain any combination of numbers, upper-case ASCII letters, and underscores (_). The number of characters in a constant name cannot exceed 100.

+

Constants must be declared right after module imports and before any procedures or program bodies. A constant's name must start with an upper-case letter and can contain any combination of numbers, upper-case ASCII letters, and underscores (_). The number of characters in a constant name cannot exceed 100.

A constant's value must be in the range between and (both inclusive) and can be defined by an arithmetic expression using +, -, *, /, //, (, ) operators and references to the previously defined constants. Here / is a field division and // is an integer division. Note that the arithmetic expression cannot contain spaces.

use.std::math::u64
 
@@ -3462,7 +3462,7 @@ 
MSTREAM

 
 
The effect of this operation on the rest of the stack is:

 
 

 
Cryptographic operations

@@ -4587,7 +4587,7 @@ 
, which communicates with all of the chiplets (Hash, Bitwise, and Memory).

 

 
LogUp: multivariate lookups with logarithmic derivatives

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

+
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.

 

 
In the above:

@@ -4603,7 +4603,7 @@ 
Usage in
 
logup_component_x

 
logup_table_t

 
Constraints

-
The diagrams above show running sum columns for computing the logarithmic derivatives for both  and . As an optimization, we can combine these values into a single auxiliary column in the extension field that contains the running sum of values from both logarithmic derivatives. We'll refer to this column as a communication bus , since it communicates the lookup request from the component  to the lookup table . 

+
The diagrams above show running sum columns for computing the logarithmic derivatives for both  and . As an optimization, we can combine these values into a single auxiliary column in the extension field that contains the running sum of values from both logarithmic derivatives. We'll refer to this column as a communication bus , since it communicates the lookup request from the component  to the lookup table .

 
This can be expressed as follows:

 

 

diff --git a/searchindex.js b/searchindex.js
index 22d049de5e..df67d70433 100644
--- a/searchindex.js
+++ b/searchindex.js
@@ -1 +1 @@
-Object.assign(window.search, {"doc_urls":["intro/main.html#introduction","intro/main.html#status-and-features","intro/main.html#feature-highlights","intro/main.html#planned-features","intro/main.html#structure-of-this-document","intro/main.html#license","intro/overview.html#miden-vm-overview","intro/overview.html#writing-programs","intro/overview.html#inputs-and-outputs","intro/overview.html#stack-depth-restrictions","intro/overview.html#nondeterministic-inputs","intro/usage.html#usage","intro/usage.html#cli-interface","intro/usage.html#compiling-miden-vm","intro/usage.html#controlling-parallelism","intro/usage.html#gpu-acceleration","intro/usage.html#simd-acceleration","intro/usage.html#running-miden-vm","intro/usage.html#inputs","intro/usage.html#fibonacci-example","intro/performance.html#performance","intro/performance.html#single-core-prover-performance","intro/performance.html#multi-core-prover-performance","intro/performance.html#recursive-proofs","tools/main.html#development-tools-and-resources","tools/debugger.html#miden-debugger","tools/repl.html#miden-repl","tools/repl.html#miden-assembly-instruction","tools/repl.html#help","tools/repl.html#program","tools/repl.html#stack","tools/repl.html#mem","tools/repl.html#memaddr","tools/repl.html#undo","user_docs/main.html#user-documentation","user_docs/assembly/main.html#miden-assembly","user_docs/assembly/main.html#terms-and-notations","user_docs/assembly/main.html#design-goals","user_docs/assembly/code_organization.html#code-organization","user_docs/assembly/code_organization.html#procedures","user_docs/assembly/code_organization.html#modules","user_docs/assembly/code_organization.html#constants","user_docs/assembly/code_organization.html#comments","user_docs/assembly/execution_contexts.html#execution-contexts","user_docs/assembly/execution_contexts.html#procedure-invocation-semantics","user_docs/assembly/execution_contexts.html#kernels","user_docs/assembly/execution_contexts.html#memory-layout","user_docs/assembly/execution_contexts.html#example","user_docs/assembly/flow_control.html#flow-control","user_docs/assembly/flow_control.html#conditional-execution","user_docs/assembly/flow_control.html#counter-controlled-loops","user_docs/assembly/flow_control.html#condition-controlled-loops","user_docs/assembly/field_operations.html#field-operations","user_docs/assembly/field_operations.html#assertions-and-tests","user_docs/assembly/field_operations.html#arithmetic-and-boolean-operations","user_docs/assembly/field_operations.html#comparison-operations","user_docs/assembly/field_operations.html#extension-field-operations","user_docs/assembly/u32_operations.html#u32-operations","user_docs/assembly/u32_operations.html#conversions-and-tests","user_docs/assembly/u32_operations.html#arithmetic-operations","user_docs/assembly/u32_operations.html#bitwise-operations","user_docs/assembly/u32_operations.html#comparison-operations","user_docs/assembly/stack_manipulation.html#stack-manipulation","user_docs/assembly/stack_manipulation.html#conditional-manipulation","user_docs/assembly/io_operations.html#input--output-operations","user_docs/assembly/io_operations.html#constant-inputs","user_docs/assembly/io_operations.html#environment-inputs","user_docs/assembly/io_operations.html#nondeterministic-inputs","user_docs/assembly/io_operations.html#random-access-memory","user_docs/assembly/cryptographic_operations.html#cryptographic-operations","user_docs/assembly/cryptographic_operations.html#hashing-and-merkle-trees","user_docs/assembly/events.html#events","user_docs/assembly/debugging.html#debugging","user_docs/stdlib/main.html#miden-standard-library","user_docs/stdlib/main.html#terms-and-notations","user_docs/stdlib/main.html#organization-and-usage","user_docs/stdlib/main.html#available-modules","user_docs/stdlib/collections.html#collections","user_docs/stdlib/collections.html#merkle-mountain-range","user_docs/stdlib/collections.html#sparse-merkle-tree-64","user_docs/stdlib/collections.html#sparse-merkle-tree-256","user_docs/stdlib/crypto/dsa.html#digital-signatures","user_docs/stdlib/crypto/dsa.html#rpo-falcon512","user_docs/stdlib/crypto/fri.html#fri-verification-procedures","user_docs/stdlib/crypto/fri.html#fri-extension-2-fold-4","user_docs/stdlib/crypto/hashes.html#cryptographic-hashes","user_docs/stdlib/crypto/hashes.html#blake3","user_docs/stdlib/crypto/hashes.html#sha256","user_docs/stdlib/math/u64.html#unsigned-64-bit-integer-operations","user_docs/stdlib/math/u64.html#arithmetic-operations","user_docs/stdlib/math/u64.html#comparison-operations","user_docs/stdlib/math/u64.html#bitwise-operations","user_docs/stdlib/mem.html#memory-procedures","user_docs/stdlib/sys.html#system-procedures","design/main.html#design","design/main.html#vm-components","design/main.html#vm-execution-trace","design/programs.html#programs-in-miden-vm","design/programs.html#code-blocks","design/programs.html#join-block","design/programs.html#split-block","design/programs.html#loop-block","design/programs.html#dyn-block","design/programs.html#call-block","design/programs.html#syscall-block","design/programs.html#span-block","design/programs.html#program-example","design/programs.html#program-hash-computation","design/decoder/main.html#miden-vm-program-decoder","design/decoder/main.html#program-execution","design/decoder/main.html#decoder-structure","design/decoder/main.html#decoder-trace","design/decoder/main.html#program-block-hashing","design/decoder/main.html#control-flow-tables","design/decoder/main.html#control-flow-operation-semantics","design/decoder/main.html#program-decoding","design/decoder/main.html#join-block-decoding","design/decoder/main.html#split-block-decoding","design/decoder/main.html#loop-block-decoding","design/decoder/main.html#dyn-block-decoding","design/decoder/main.html#span-block-decoding","design/decoder/main.html#program-decoding-example","design/decoder/constraints.html#miden-vm-decoder-air-constraints","design/decoder/constraints.html#general-constraints","design/decoder/constraints.html#block-hash-computation-constraints","design/decoder/constraints.html#chiplets-bus-constraints","design/decoder/constraints.html#block-stack-table-constraints","design/decoder/constraints.html#block-hash-table-constraints","design/decoder/constraints.html#span-block","design/decoder/constraints.html#in-span-column-constraints","design/decoder/constraints.html#block-address-constraints","design/decoder/constraints.html#group-count-constraints","design/decoder/constraints.html#op-group-decoding-constraints","design/decoder/constraints.html#op-index-constraints","design/decoder/constraints.html#op-batch-flags-constraints","design/decoder/constraints.html#op-group-table-constraints","design/stack/main.html#operand-stack","design/stack/main.html#stack-representation","design/stack/main.html#overflow-table","design/stack/main.html#right-shift","design/stack/main.html#left-shift","design/stack/main.html#air-constraints","design/stack/main.html#stack-overflow-flag","design/stack/main.html#stack-depth-constraints","design/stack/main.html#overflow-table-constraints","design/stack/main.html#boundary-constraints","design/stack/op_constraints.html#stack-operation-constraints","design/stack/op_constraints.html#operation-flags","design/stack/op_constraints.html#no-stack-shift-operations","design/stack/op_constraints.html#left-stack-shift-operations","design/stack/op_constraints.html#right-stack-shift-operations","design/stack/op_constraints.html#u32-operations","design/stack/op_constraints.html#high-degree-operations","design/stack/op_constraints.html#very-high-degree-operations","design/stack/op_constraints.html#composite-flags","design/stack/op_constraints.html#shift-right-flag","design/stack/op_constraints.html#shift-left-flag","design/stack/op_constraints.html#control-flow-flag","design/stack/system_ops.html#system-operations","design/stack/system_ops.html#noop","design/stack/system_ops.html#assert","design/stack/system_ops.html#fmpadd","design/stack/system_ops.html#fmpupdate","design/stack/system_ops.html#clk","design/stack/field_ops.html#field-operations","design/stack/field_ops.html#add","design/stack/field_ops.html#neg","design/stack/field_ops.html#mul","design/stack/field_ops.html#inv","design/stack/field_ops.html#incr","design/stack/field_ops.html#not","design/stack/field_ops.html#and","design/stack/field_ops.html#or","design/stack/field_ops.html#eq","design/stack/field_ops.html#eqz","design/stack/field_ops.html#expacc","design/stack/field_ops.html#ext2mul","design/stack/u32_ops.html#u32-operations","design/stack/u32_ops.html#range-checks","design/stack/u32_ops.html#checking-element-validity","design/stack/u32_ops.html#u32split","design/stack/u32_ops.html#u32assert2","design/stack/u32_ops.html#u32add","design/stack/u32_ops.html#u32add3","design/stack/u32_ops.html#u32sub","design/stack/u32_ops.html#u32mul","design/stack/u32_ops.html#u32madd","design/stack/u32_ops.html#u32div","design/stack/u32_ops.html#u32and","design/stack/u32_ops.html#u32xor","design/stack/stack_ops.html#stack-manipulation","design/stack/stack_ops.html#pad","design/stack/stack_ops.html#drop","design/stack/stack_ops.html#dupn","design/stack/stack_ops.html#swap","design/stack/stack_ops.html#swapw","design/stack/stack_ops.html#swapw2","design/stack/stack_ops.html#swapw3","design/stack/stack_ops.html#swapdw","design/stack/stack_ops.html#movupn","design/stack/stack_ops.html#movdnn","design/stack/stack_ops.html#cswap","design/stack/stack_ops.html#cswapw","design/stack/io_ops.html#input--output-operations","design/stack/io_ops.html#push","design/stack/io_ops.html#sdepth","design/stack/io_ops.html#advpop","design/stack/io_ops.html#advpopw","design/stack/io_ops.html#memory-access-operations","design/stack/io_ops.html#mloadw","design/stack/io_ops.html#mload","design/stack/io_ops.html#mstorew","design/stack/io_ops.html#mstore","design/stack/io_ops.html#mstream","design/stack/crypto_ops.html#cryptographic-operations","design/stack/crypto_ops.html#hperm","design/stack/crypto_ops.html#mpverify","design/stack/crypto_ops.html#mrupdate","design/stack/crypto_ops.html#frie2f4","design/range.html#range-checker","design/range.html#8-bit-range-checks","design/range.html#a-better-construction","design/range.html#16-bit-range-checks","design/range.html#miden-approach","design/range.html#requirements","design/range.html#capabilities","design/range.html#execution-trace","design/range.html#execution-trace-constraints","design/range.html#communication-bus","design/chiplets/main.html#chiplets","design/chiplets/main.html#chiplets-module-trace","design/chiplets/main.html#chiplets-order","design/chiplets/main.html#additional-requirements-for-stacking-execution-traces","design/chiplets/main.html#operation-labels","design/chiplets/main.html#chiplets-module-constraints","design/chiplets/main.html#chiplet-constraints","design/chiplets/main.html#chiplet-selector-constraints","design/chiplets/main.html#chiplets-bus","design/chiplets/main.html#chiplets-bus-constraints","design/chiplets/main.html#chiplets-virtual-table","design/chiplets/main.html#chiplets-virtual-table-constraints","design/chiplets/hasher.html#hash-chiplet","design/chiplets/hasher.html#chiplet-trace","design/chiplets/hasher.html#instruction-flags","design/chiplets/hasher.html#computation-examples","design/chiplets/hasher.html#single-permutation","design/chiplets/hasher.html#simple-2-to-1-hash","design/chiplets/hasher.html#linear-hash-of-n-elements","design/chiplets/hasher.html#verify-merkle-path","design/chiplets/hasher.html#update-merkle-root","design/chiplets/hasher.html#air-constraints","design/chiplets/hasher.html#selector-columns-constraints","design/chiplets/hasher.html#node-index-constraints","design/chiplets/hasher.html#hasher-state-constraints","design/chiplets/hasher.html#multiset-check-constraints","design/chiplets/bitwise.html#bitwise-chiplet","design/chiplets/bitwise.html#example","design/chiplets/bitwise.html#constraints","design/chiplets/bitwise.html#selectors","design/chiplets/bitwise.html#input-decomposition","design/chiplets/bitwise.html#output-aggregation","design/chiplets/bitwise.html#chiplets-bus-constraints","design/chiplets/memory.html#memory-chiplet","design/chiplets/memory.html#alternative-designs","design/chiplets/memory.html#read-write-memory","design/chiplets/memory.html#non-contiguous-memory","design/chiplets/memory.html#context-separation","design/chiplets/memory.html#miden-approach","design/chiplets/memory.html#air-constraints","design/chiplets/kernel_rom.html#kernel-rom-chiplet","design/chiplets/kernel_rom.html#kernel-rom-trace","design/chiplets/kernel_rom.html#constraints","design/chiplets/kernel_rom.html#chiplets-bus-constraints","design/chiplets/kernel_rom.html#kernel-procedure-table-constraints","design/lookups/main.html#lookup-arguments-in-miden-vm","design/lookups/main.html#virtual-tables-in-miden-vm","design/lookups/main.html#communication-buses-in-miden-vm","design/lookups/main.html#length-of-auxiliary-columns-for-lookup-arguments","design/lookups/main.html#cost-of-auxiliary-columns-for-lookup-arguments","design/lookups/multiset.html#multiset-checks","design/lookups/multiset.html#running-product-columns","design/lookups/multiset.html#virtual-tables","design/lookups/multiset.html#computing-a-virtual-tables-trace-column","design/lookups/multiset.html#virtual-tables-in-miden-vm","design/lookups/multiset.html#communication-buses-via-multiset-checks","design/lookups/multiset.html#communication-bus-constraints","design/lookups/multiset.html#communication-buses-in-miden-vm","design/lookups/logup.html#logup-multivariate-lookups-with-logarithmic-derivatives","design/lookups/logup.html#usage-in-miden-vm","design/lookups/logup.html#constraints","design/lookups/logup.html#extending-the-construction-to-multiple-components","design/lookups/logup.html#extending-the-construction-with-flags","background.html#background-material"],"index":{"documentStore":{"docInfo":{"0":{"body":34,"breadcrumbs":2,"title":1},"1":{"body":53,"breadcrumbs":3,"title":2},"10":{"body":115,"breadcrumbs":4,"title":2},"100":{"body":41,"breadcrumbs":4,"title":2},"101":{"body":67,"breadcrumbs":4,"title":2},"102":{"body":54,"breadcrumbs":4,"title":2},"103":{"body":82,"breadcrumbs":4,"title":2},"104":{"body":85,"breadcrumbs":4,"title":2},"105":{"body":196,"breadcrumbs":4,"title":2},"106":{"body":200,"breadcrumbs":4,"title":2},"107":{"body":239,"breadcrumbs":5,"title":3},"108":{"body":131,"breadcrumbs":7,"title":4},"109":{"body":215,"breadcrumbs":5,"title":2},"11":{"body":72,"breadcrumbs":3,"title":1},"110":{"body":45,"breadcrumbs":5,"title":2},"111":{"body":183,"breadcrumbs":5,"title":2},"112":{"body":298,"breadcrumbs":6,"title":3},"113":{"body":516,"breadcrumbs":6,"title":3},"114":{"body":899,"breadcrumbs":7,"title":4},"115":{"body":91,"breadcrumbs":5,"title":2},"116":{"body":59,"breadcrumbs":6,"title":3},"117":{"body":54,"breadcrumbs":6,"title":3},"118":{"body":227,"breadcrumbs":6,"title":3},"119":{"body":60,"breadcrumbs":6,"title":3},"12":{"body":0,"breadcrumbs":4,"title":2},"120":{"body":1069,"breadcrumbs":6,"title":3},"121":{"body":292,"breadcrumbs":6,"title":3},"122":{"body":306,"breadcrumbs":10,"title":5},"123":{"body":147,"breadcrumbs":7,"title":2},"124":{"body":153,"breadcrumbs":9,"title":4},"125":{"body":448,"breadcrumbs":8,"title":3},"126":{"body":317,"breadcrumbs":9,"title":4},"127":{"body":436,"breadcrumbs":9,"title":4},"128":{"body":26,"breadcrumbs":7,"title":2},"129":{"body":135,"breadcrumbs":8,"title":3},"13":{"body":62,"breadcrumbs":5,"title":3},"130":{"body":70,"breadcrumbs":8,"title":3},"131":{"body":184,"breadcrumbs":8,"title":3},"132":{"body":225,"breadcrumbs":9,"title":4},"133":{"body":132,"breadcrumbs":8,"title":3},"134":{"body":141,"breadcrumbs":9,"title":4},"135":{"body":349,"breadcrumbs":9,"title":4},"136":{"body":120,"breadcrumbs":5,"title":2},"137":{"body":80,"breadcrumbs":5,"title":2},"138":{"body":172,"breadcrumbs":5,"title":2},"139":{"body":172,"breadcrumbs":5,"title":2},"14":{"body":18,"breadcrumbs":4,"title":2},"140":{"body":114,"breadcrumbs":5,"title":2},"141":{"body":59,"breadcrumbs":5,"title":2},"142":{"body":58,"breadcrumbs":6,"title":3},"143":{"body":51,"breadcrumbs":6,"title":3},"144":{"body":132,"breadcrumbs":6,"title":3},"145":{"body":27,"breadcrumbs":5,"title":2},"146":{"body":181,"breadcrumbs":8,"title":3},"147":{"body":312,"breadcrumbs":7,"title":2},"148":{"body":216,"breadcrumbs":8,"title":3},"149":{"body":129,"breadcrumbs":9,"title":4},"15":{"body":48,"breadcrumbs":4,"title":2},"150":{"body":133,"breadcrumbs":9,"title":4},"151":{"body":167,"breadcrumbs":7,"title":2},"152":{"body":162,"breadcrumbs":8,"title":3},"153":{"body":113,"breadcrumbs":9,"title":4},"154":{"body":13,"breadcrumbs":7,"title":2},"155":{"body":41,"breadcrumbs":8,"title":3},"156":{"body":93,"breadcrumbs":8,"title":3},"157":{"body":37,"breadcrumbs":8,"title":3},"158":{"body":8,"breadcrumbs":7,"title":2},"159":{"body":34,"breadcrumbs":6,"title":1},"16":{"body":51,"breadcrumbs":4,"title":2},"160":{"body":33,"breadcrumbs":6,"title":1},"161":{"body":35,"breadcrumbs":6,"title":1},"162":{"body":31,"breadcrumbs":6,"title":1},"163":{"body":30,"breadcrumbs":6,"title":1},"164":{"body":14,"breadcrumbs":7,"title":2},"165":{"body":30,"breadcrumbs":6,"title":1},"166":{"body":28,"breadcrumbs":6,"title":1},"167":{"body":30,"breadcrumbs":6,"title":1},"168":{"body":34,"breadcrumbs":6,"title":1},"169":{"body":28,"breadcrumbs":6,"title":1},"17":{"body":118,"breadcrumbs":5,"title":3},"170":{"body":41,"breadcrumbs":5,"title":0},"171":{"body":46,"breadcrumbs":5,"title":0},"172":{"body":46,"breadcrumbs":5,"title":0},"173":{"body":56,"breadcrumbs":6,"title":1},"174":{"body":54,"breadcrumbs":6,"title":1},"175":{"body":85,"breadcrumbs":6,"title":1},"176":{"body":71,"breadcrumbs":6,"title":1},"177":{"body":17,"breadcrumbs":7,"title":2},"178":{"body":111,"breadcrumbs":7,"title":2},"179":{"body":113,"breadcrumbs":8,"title":3},"18":{"body":177,"breadcrumbs":3,"title":1},"180":{"body":95,"breadcrumbs":6,"title":1},"181":{"body":76,"breadcrumbs":6,"title":1},"182":{"body":83,"breadcrumbs":6,"title":1},"183":{"body":85,"breadcrumbs":6,"title":1},"184":{"body":83,"breadcrumbs":6,"title":1},"185":{"body":98,"breadcrumbs":6,"title":1},"186":{"body":114,"breadcrumbs":6,"title":1},"187":{"body":70,"breadcrumbs":6,"title":1},"188":{"body":74,"breadcrumbs":6,"title":1},"189":{"body":77,"breadcrumbs":6,"title":1},"19":{"body":63,"breadcrumbs":4,"title":2},"190":{"body":9,"breadcrumbs":7,"title":2},"191":{"body":28,"breadcrumbs":6,"title":1},"192":{"body":35,"breadcrumbs":6,"title":1},"193":{"body":62,"breadcrumbs":6,"title":1},"194":{"body":30,"breadcrumbs":6,"title":1},"195":{"body":33,"breadcrumbs":6,"title":1},"196":{"body":36,"breadcrumbs":6,"title":1},"197":{"body":36,"breadcrumbs":6,"title":1},"198":{"body":33,"breadcrumbs":6,"title":1},"199":{"body":71,"breadcrumbs":6,"title":1},"2":{"body":250,"breadcrumbs":3,"title":2},"20":{"body":124,"breadcrumbs":3,"title":1},"200":{"body":70,"breadcrumbs":6,"title":1},"201":{"body":60,"breadcrumbs":6,"title":1},"202":{"body":62,"breadcrumbs":6,"title":1},"203":{"body":24,"breadcrumbs":9,"title":3},"204":{"body":34,"breadcrumbs":7,"title":1},"205":{"body":37,"breadcrumbs":7,"title":1},"206":{"body":38,"breadcrumbs":7,"title":1},"207":{"body":49,"breadcrumbs":7,"title":1},"208":{"body":73,"breadcrumbs":9,"title":3},"209":{"body":90,"breadcrumbs":7,"title":1},"21":{"body":207,"breadcrumbs":6,"title":4},"210":{"body":95,"breadcrumbs":7,"title":1},"211":{"body":90,"breadcrumbs":7,"title":1},"212":{"body":102,"breadcrumbs":7,"title":1},"213":{"body":100,"breadcrumbs":7,"title":1},"214":{"body":54,"breadcrumbs":7,"title":2},"215":{"body":118,"breadcrumbs":6,"title":1},"216":{"body":169,"breadcrumbs":6,"title":1},"217":{"body":204,"breadcrumbs":6,"title":1},"218":{"body":281,"breadcrumbs":6,"title":1},"219":{"body":65,"breadcrumbs":5,"title":2},"22":{"body":116,"breadcrumbs":6,"title":4},"220":{"body":213,"breadcrumbs":7,"title":4},"221":{"body":86,"breadcrumbs":5,"title":2},"222":{"body":130,"breadcrumbs":7,"title":4},"223":{"body":7,"breadcrumbs":5,"title":2},"224":{"body":34,"breadcrumbs":4,"title":1},"225":{"body":32,"breadcrumbs":4,"title":1},"226":{"body":64,"breadcrumbs":5,"title":2},"227":{"body":35,"breadcrumbs":6,"title":3},"228":{"body":174,"breadcrumbs":5,"title":2},"229":{"body":98,"breadcrumbs":3,"title":1},"23":{"body":157,"breadcrumbs":4,"title":2},"230":{"body":121,"breadcrumbs":5,"title":3},"231":{"body":101,"breadcrumbs":4,"title":2},"232":{"body":137,"breadcrumbs":7,"title":5},"233":{"body":121,"breadcrumbs":4,"title":2},"234":{"body":0,"breadcrumbs":5,"title":3},"235":{"body":75,"breadcrumbs":4,"title":2},"236":{"body":116,"breadcrumbs":5,"title":3},"237":{"body":123,"breadcrumbs":4,"title":2},"238":{"body":52,"breadcrumbs":5,"title":3},"239":{"body":65,"breadcrumbs":5,"title":3},"24":{"body":59,"breadcrumbs":5,"title":3},"240":{"body":86,"breadcrumbs":6,"title":4},"241":{"body":313,"breadcrumbs":6,"title":2},"242":{"body":331,"breadcrumbs":6,"title":2},"243":{"body":266,"breadcrumbs":6,"title":2},"244":{"body":0,"breadcrumbs":6,"title":2},"245":{"body":73,"breadcrumbs":6,"title":2},"246":{"body":84,"breadcrumbs":8,"title":4},"247":{"body":143,"breadcrumbs":8,"title":4},"248":{"body":197,"breadcrumbs":7,"title":3},"249":{"body":215,"breadcrumbs":7,"title":3},"25":{"body":212,"breadcrumbs":5,"title":2},"250":{"body":30,"breadcrumbs":6,"title":2},"251":{"body":98,"breadcrumbs":7,"title":3},"252":{"body":148,"breadcrumbs":7,"title":3},"253":{"body":105,"breadcrumbs":7,"title":3},"254":{"body":559,"breadcrumbs":7,"title":3},"255":{"body":227,"breadcrumbs":6,"title":2},"256":{"body":180,"breadcrumbs":5,"title":1},"257":{"body":24,"breadcrumbs":5,"title":1},"258":{"body":24,"breadcrumbs":5,"title":1},"259":{"body":117,"breadcrumbs":6,"title":2},"26":{"body":55,"breadcrumbs":5,"title":2},"260":{"body":86,"breadcrumbs":6,"title":2},"261":{"body":114,"breadcrumbs":7,"title":3},"262":{"body":66,"breadcrumbs":6,"title":2},"263":{"body":139,"breadcrumbs":6,"title":2},"264":{"body":228,"breadcrumbs":7,"title":3},"265":{"body":147,"breadcrumbs":7,"title":3},"266":{"body":230,"breadcrumbs":6,"title":2},"267":{"body":418,"breadcrumbs":6,"title":2},"268":{"body":253,"breadcrumbs":6,"title":2},"269":{"body":38,"breadcrumbs":8,"title":3},"27":{"body":55,"breadcrumbs":6,"title":3},"270":{"body":54,"breadcrumbs":8,"title":3},"271":{"body":103,"breadcrumbs":6,"title":1},"272":{"body":85,"breadcrumbs":8,"title":3},"273":{"body":101,"breadcrumbs":9,"title":4},"274":{"body":144,"breadcrumbs":7,"title":4},"275":{"body":44,"breadcrumbs":7,"title":4},"276":{"body":117,"breadcrumbs":7,"title":4},"277":{"body":53,"breadcrumbs":8,"title":5},"278":{"body":42,"breadcrumbs":8,"title":5},"279":{"body":17,"breadcrumbs":7,"title":2},"28":{"body":8,"breadcrumbs":4,"title":1},"280":{"body":72,"breadcrumbs":8,"title":3},"281":{"body":105,"breadcrumbs":7,"title":2},"282":{"body":58,"breadcrumbs":10,"title":5},"283":{"body":40,"breadcrumbs":9,"title":4},"284":{"body":111,"breadcrumbs":10,"title":5},"285":{"body":105,"breadcrumbs":8,"title":3},"286":{"body":35,"breadcrumbs":9,"title":4},"287":{"body":113,"breadcrumbs":9,"title":5},"288":{"body":28,"breadcrumbs":7,"title":3},"289":{"body":83,"breadcrumbs":5,"title":1},"29":{"body":25,"breadcrumbs":4,"title":1},"290":{"body":40,"breadcrumbs":8,"title":4},"291":{"body":45,"breadcrumbs":7,"title":3},"292":{"body":117,"breadcrumbs":4,"title":2},"3":{"body":69,"breadcrumbs":3,"title":2},"30":{"body":57,"breadcrumbs":4,"title":1},"31":{"body":48,"breadcrumbs":4,"title":1},"32":{"body":24,"breadcrumbs":4,"title":1},"33":{"body":110,"breadcrumbs":4,"title":1},"34":{"body":57,"breadcrumbs":4,"title":2},"35":{"body":165,"breadcrumbs":6,"title":2},"36":{"body":79,"breadcrumbs":6,"title":2},"37":{"body":160,"breadcrumbs":6,"title":2},"38":{"body":53,"breadcrumbs":8,"title":2},"39":{"body":269,"breadcrumbs":7,"title":1},"4":{"body":78,"breadcrumbs":3,"title":2},"40":{"body":237,"breadcrumbs":7,"title":1},"41":{"body":102,"breadcrumbs":7,"title":1},"42":{"body":37,"breadcrumbs":7,"title":1},"43":{"body":96,"breadcrumbs":8,"title":2},"44":{"body":205,"breadcrumbs":9,"title":3},"45":{"body":90,"breadcrumbs":7,"title":1},"46":{"body":138,"breadcrumbs":8,"title":2},"47":{"body":274,"breadcrumbs":7,"title":1},"48":{"body":26,"breadcrumbs":8,"title":2},"49":{"body":69,"breadcrumbs":8,"title":2},"5":{"body":4,"breadcrumbs":2,"title":1},"50":{"body":49,"breadcrumbs":9,"title":3},"51":{"body":93,"breadcrumbs":9,"title":3},"52":{"body":53,"breadcrumbs":8,"title":2},"53":{"body":61,"breadcrumbs":8,"title":2},"54":{"body":118,"breadcrumbs":9,"title":3},"55":{"body":70,"breadcrumbs":8,"title":2},"56":{"body":75,"breadcrumbs":9,"title":3},"57":{"body":112,"breadcrumbs":8,"title":2},"58":{"body":74,"breadcrumbs":8,"title":2},"59":{"body":263,"breadcrumbs":8,"title":2},"6":{"body":173,"breadcrumbs":5,"title":3},"60":{"body":221,"breadcrumbs":8,"title":2},"61":{"body":156,"breadcrumbs":8,"title":2},"62":{"body":235,"breadcrumbs":8,"title":2},"63":{"body":56,"breadcrumbs":8,"title":2},"64":{"body":120,"breadcrumbs":10,"title":3},"65":{"body":93,"breadcrumbs":9,"title":2},"66":{"body":64,"breadcrumbs":9,"title":2},"67":{"body":473,"breadcrumbs":9,"title":2},"68":{"body":348,"breadcrumbs":10,"title":3},"69":{"body":13,"breadcrumbs":8,"title":2},"7":{"body":56,"breadcrumbs":4,"title":2},"70":{"body":243,"breadcrumbs":9,"title":3},"71":{"body":78,"breadcrumbs":6,"title":1},"72":{"body":145,"breadcrumbs":6,"title":1},"73":{"body":59,"breadcrumbs":8,"title":3},"74":{"body":79,"breadcrumbs":7,"title":2},"75":{"body":47,"breadcrumbs":7,"title":2},"76":{"body":100,"breadcrumbs":7,"title":2},"77":{"body":25,"breadcrumbs":7,"title":1},"78":{"body":144,"breadcrumbs":9,"title":3},"79":{"body":177,"breadcrumbs":10,"title":4},"8":{"body":137,"breadcrumbs":4,"title":2},"80":{"body":202,"breadcrumbs":10,"title":4},"81":{"body":19,"breadcrumbs":8,"title":2},"82":{"body":114,"breadcrumbs":8,"title":2},"83":{"body":7,"breadcrumbs":9,"title":3},"84":{"body":210,"breadcrumbs":11,"title":5},"85":{"body":9,"breadcrumbs":8,"title":2},"86":{"body":83,"breadcrumbs":7,"title":1},"87":{"body":83,"breadcrumbs":7,"title":1},"88":{"body":125,"breadcrumbs":11,"title":5},"89":{"body":493,"breadcrumbs":8,"title":2},"9":{"body":44,"breadcrumbs":5,"title":3},"90":{"body":595,"breadcrumbs":8,"title":2},"91":{"body":373,"breadcrumbs":8,"title":2},"92":{"body":124,"breadcrumbs":8,"title":2},"93":{"body":58,"breadcrumbs":8,"title":2},"94":{"body":187,"breadcrumbs":2,"title":1},"95":{"body":151,"breadcrumbs":3,"title":2},"96":{"body":103,"breadcrumbs":4,"title":3},"97":{"body":48,"breadcrumbs":5,"title":3},"98":{"body":0,"breadcrumbs":4,"title":2},"99":{"body":27,"breadcrumbs":4,"title":2}},"docs":{"0":{"body":"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.","breadcrumbs":"Introduction » Introduction","id":"0","title":"Introduction"},"1":{"body":"Miden VM is currently on release v0.8. In this release, most of the core features of the VM have been stabilized, and most of the STARK proof generation has been implemented. While we expect to keep making changes to the VM internals, the external interfaces should remain relatively stable, and we will do our best to minimize the amount of breaking changes going forward. At this point, Miden VM is good enough for experimentation, and even for real-world applications, but it is not yet ready for production use. The codebase has not been audited and contains known and unknown bugs and security flaws.","breadcrumbs":"Introduction » Status and features","id":"1","title":"Status and features"},"10":{"body":"The advice provider component is responsible for supplying nondeterministic inputs to the VM. These inputs only need to be known to the prover (i.e., they do not need to be shared with the verifier). The advice provider consists of three components: Advice stack which is a one-dimensional array of field elements. Being a stack, the VM can either push new elements onto the advice stack, or pop the elements from its top. Advice map which is a key-value map where keys are words and values are vectors of field elements. The VM can copy values from the advice map onto the advice stack as well as insert new values into the advice map (e.g., from a region of memory). Merkle store which contain structured data reducible to Merkle paths. Some examples of such structures are: Merkle tree, Sparse Merkle Tree, and a collection of Merkle paths. The VM can request Merkle paths from the Merkle store, as well as mutate it by updating or merging nodes contained in the store. The prover initializes the advice provider prior to executing a program, and from that point on the advice provider is manipulated solely by executing operations on the VM.","breadcrumbs":"Introduction » Overview » Nondeterministic inputs","id":"10","title":"Nondeterministic inputs"},"100":{"body":"A split block is used to describe conditional execution. When the VM encounters a split block, it checks the top of the stack. If the top of the stack is 1, it executes the left child, if the top of the stack is 0, it executes the right child. If the top of the stack is neither 0 nor 1, the execution fails. split_block A split block must always have two children, and thus, cannot be a leaf node in the tree.","breadcrumbs":"Design » Programs » Split block","id":"100","title":"Split block"},"101":{"body":"A loop block is used to describe condition-based iterative execution. When the VM encounters a loop block, it checks the top of the stack. If the top of the stack is 1, it executes the loop body, if the top of the stack is 0, the block is not executed. If the top of the stack is neither 0 nor 1, the execution fails. After the body of the loop is executed, the VM checks the top of the stack again. If the top of the stack is 1, the body is executed again, if the top of the stack is 0, the loop is exited. If the top of the stack is neither 0 nor 1, the execution fails. loop_block A loop block must always have one child, and thus, cannot be a leaf node in the tree.","breadcrumbs":"Design » Programs » Loop block","id":"101","title":"Loop block"},"102":{"body":"A dyn block is used to describe a node whose target is specified dynamically via the stack. When the VM encounters a dyn block, it executes a program which hashes to the target specified by the top of the stack. Thus, it has a dynamic target rather than a hardcoded target. In order to execute a dyn block, the VM must be aware of a program with the hash value that is specified by the top of the stack. Otherwise, the execution fails. dyn_block A dyn block must always have one (dynamically-specified) child. Thus, it cannot be a leaf node in the tree.","breadcrumbs":"Design » Programs » Dyn block","id":"102","title":"Dyn block"},"103":{"body":"A call block is used to describe a function call which is executed in a user context . When the VM encounters a call block, it creates a new user context, then executes a program which hashes to the target specified by the call block in the new context. Thus, in order to execute a call block, the VM must be aware of a program with the specified hash. Otherwise, the execution fails. At the end of the call block, execution returns to the previous context. When executing a call block, the VM does the following: Checks if a syscall is already being executed and fails if so. Sets the depth of the stack to 16. Upon return, checks that the depth of the stack is 16. If so, the original stack depth is restored. Otherwise, an error occurs. call_block A call block does not have any children. Thus, it must be leaf node in the tree.","breadcrumbs":"Design » Programs » Call block","id":"103","title":"Call block"},"104":{"body":"A syscall block is used to describe a function call which is executed in the root context . When the VM encounters a syscall block, it returns to the root context, then executes a program which hashes to the target specified by the syscall block. Thus, in order to execute a syscall block, the VM must be aware of a program with the specified hash, and that program must belong to the kernel against which the code is compiled. Otherwise, the execution fails. At the end of the syscall block, execution returns to the previous context. When executing a syscall block, the VM does the following: Checks if a syscall is already being executed and fails if so. Sets the depth of the stack to 16. Upon return, checks that the depth of the stack is 16. If so, the original stack depth is restored. Otherwise, an error occurs. syscall_block A syscall block does not have any children. Thus, it must be leaf node in the tree.","breadcrumbs":"Design » Programs » Syscall block","id":"104","title":"Syscall block"},"105":{"body":"A span block is used to describe a linear sequence of operations. When the VM encounters a span block, it breaks the sequence of operations into batches and groups according to the following rules: A group is represented by a single field element. Thus, assuming a single operation can be encoded using 7 bits, and assuming we are using a 64-bit field, a single group may encode up to 9 operations or a single immediate value. A batch is a set of groups which can be absorbed by a hash function used by the VM in a single permutation. For example, assuming the hash function can absorb up to 8 field elements in a single permutation, a single batch may contain up to 8 groups. There is no limit on the number of batches contained within a single span. Thus, for example, executing 8 pushes in a row will result in two operation batches as illustrated in the picture below: span_block_creation The first batch will contain 8 groups, with the first group containing 7 PUSH opcodes and 1 NOOP, and the remaining 7 groups containing immediate values for each of the push operations. The reason for the NOOP is explained later in this section. The second batch will contain 2 groups, with the first group containing 1 PUSH opcode and 1 NOOP, and the second group containing the immediate value for the last push operation. If a sequence of operations does not have any operations which carry immediate values, up to 72 operations can fit into a single batch. From the user's perspective, all operations are executed in order, however, the VM may insert occasional NOOPs to ensure proper alignment of all operations in the sequence. Currently, the alignment requirements are as follows: An operation carrying an immediate value cannot be the last operation in a group. Thus, for example, if a PUSH operation is the last operation in a group, the VM will insert a NOOP after it. A span block does not have any children, and thus, must be leaf node in the tree.","breadcrumbs":"Design » Programs » Span block","id":"105","title":"Span block"},"106":{"body":"Consider the following program, where a0​,...,ai​, b0​,...,bj​ etc. represent individual operations: a_0, ..., a_i\nif.true b_0, ..., b_j\nelse c_0, ..., c_k while.true d_0, ..., d_n end e_0, ..., e_m\nend\nf_0, ..., f_l A MAST for this program would look as follows: mast_of_program Execution of this program would proceed as follows: The VM will start execution at the root of the program which is block B5​. Since, B5​ is a join block , the VM will attempt to execute block B4​ first, and only after that execute block f. Block B4​ is also a join block , and thus, the VM will execute block a by executing operations a0​,...,ai​ in sequence, and then execute block B3​. Block B3​ is a split block , and thus, the VM will pop the value off the top of the stack. If the popped value is 1, operations from block b will be executed in sequence. If the popped value is 0, then the VM will attempt to execute block B2​. B2​ is a join block , thus, the VM will try to execute block B1​ first, and then execute operations from block e. Block B1​ is also a join_block , and thus, the VM will first execute all operations in block c, and then will attempt to execute block B0​. Block B0​ is a loop block, thus, the VM will pop the value off the top of the stack. If the pooped value is 1, the VM will execute the body of the loop defined by block d. If the popped value is 0, the VM will not execute block d and instead will move up the tree executing first block e, then f. If the VM does enter the loop, then after operation dn​ is executed, the VM will pop the value off the top of the stack again. If the popped value is 1, the VM will execute block d again, and again until the top of the stack becomes 0. Once the top of the stack becomes 0, the VM will exit the loop and will move up the tree executing first block e, then f.","breadcrumbs":"Design » Programs » Program example","id":"106","title":"Program example"},"107":{"body":"Every Miden VM program can be reduced to a unique hash value. Specifically, it is infeasible to find two Miden VM programs with distinct semantics which hash to the same value. Padding a program with NOOPs does not change a program's execution semantics, and thus, programs which differ only in the number and/or placement of NOOPs may hash to the same value, although in most cases padding with NOOP should not affect program hash. To prevent program hash collisions we implement domain separation across the variants of control blocks. We define the domain value to be the opcode of the operation that initializes the control block. Below we denote hash to be an arithmetization-friendly hash function with 4-element output and capable of absorbing 8 elements in a single permutation. The hash domain is specified as the subscript of the hash function and its value is used to populate the second capacity register upon initialization of control block hashing - hashdomain​(a,b). The hash of a join block is computed as hashjoin​(a,b), where a and b are hashes of the code block being joined. The hash of a split block is computed as hashsplit​(a,b), where a is a hash of a code block corresponding to the true branch of execution, and b is a hash of a code block corresponding to the false branch of execution. The hash of a loop block is computed as hashloop​(a,0), where a is a hash of a code block corresponding to the loop body. The hash of a dyn block is set to a constant, so it is the same for all dyn blocks. It does not depend on the hash of the dynamic child. This constant is computed as the RPO hash of two empty words ([ZERO, ZERO, ZERO, ZERO]) using a domain value of DYN_DOMAIN, where DYN_DOMAIN is the op code of the Dyn operation. The hash of a call block is computed as hashcall​(a,0), where a is a hash of a program of which the VM is aware. The hash of a syscall block is computed as hashsyscall​(a,0), where a is a hash of a program belonging to the kernel against which the code was compiled. The hash of a span block is computed as hash(a1​,...,ak​), where ai​ is the ith batch of operations in the span block. Each batch of operations is defined as containing 8 field elements, and thus, hashing a k-batch span block requires k absorption steps. In cases when the number of operations is insufficient to fill the last batch entirely, NOOPs are appended to the end of the last batch to ensure that the number of operations in the batch is always equal to 8.","breadcrumbs":"Design » Programs » Program hash computation","id":"107","title":"Program hash computation"},"108":{"body":"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: Decodes a sequence of field elements supplied by the prover into individual operation codes (or opcodes for short). Organizes the sequence of field elements into code blocks, and computes the hash of the program according to the methodology described here . 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: An opcode requires 7 bits to represent. An immediate value requires one full field element to represent. 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.","breadcrumbs":"Design » Program decoder » Miden VM Program decoder","id":"108","title":"Miden VM Program decoder"},"109":{"body":"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 require exactly one VM cycle to execute. Operation Description JOIN Initiates processing of a new Join block . SPLIT Initiates processing of a new Split block . LOOP Initiates processing of a new Loop block . REPEAT Initiates a new iteration of an executing loop. SPAN Initiates processing of a new Span block . RESPAN Initiates processing of a new operation batch within a span block. DYN Initiates processing of a new Dyn block . CALL Initiates processing of a new Call block . SYSCALL Initiates processing ofa new 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  if.true  else  end\nend Block structure of this program is shown below. JOIN SPAN  END SPLIT SPAN  END SPAN  END END\nEND Executing this program on the VM can result in one of two possible instruction sequences. First, if after operations in  are executed the top of the stack is 1, the VM will execute the following: JOIN\nSPAN\n\nEND\nSPLIT\nSPAN\n\nEND\nEND\nEND\nHALT However, if after  are executed, the top of the stack is 0, the VM will execute the following: JOIN\nSPAN\n\nEND\nSPLIT\nSPAN\n\nEND\nEND\nEND\nHALT The main task of the decoder is to output exactly the same program hash, regardless of which one of the two possible execution paths was taken. However, before we can describe how this is achieved, we need to give an overview of the overall decoder structure.","breadcrumbs":"Design » Program decoder » Program execution","id":"109","title":"Program execution"},"11":{"body":"Before you can use Miden VM, you'll need to make sure you have Rust installed . Miden VM v0.8 requires Rust version 1.73 or later. Miden VM consists of several crates, each of which exposes a small set of functionality. The most notable of these crates are: miden-processor , which can be used to execute Miden VM programs. miden-prover , which can be used to execute Miden VM programs and generate proofs of their execution. miden-verifier , which can be used to verify proofs of program execution generated by Miden VM prover. The above functionality is also exposed via the single miden-vm crate, which also provides a CLI interface for interacting with Miden VM.","breadcrumbs":"Introduction » Usage » Usage","id":"11","title":"Usage"},"110":{"body":"The decoder is one of the more complex parts of the VM. It consists of the following components: Main execution trace consisting of 24 trace columns which contain the state of the decoder at a given cycle of a computation. Connection to the hash chiplet, which is used to offload hash computations from the decoder. 3 virtual tables (implemented via multi-set checks), which keep track of code blocks and operations executing on the VM.","breadcrumbs":"Design » Program decoder » Decoder structure","id":"110","title":"Decoder structure"},"111":{"body":"Decoder trace columns can be grouped into several logical sets of registers as illustrated below. decoder_trace.png These registers have the following meanings: Block address register a. This register contains address of the hasher for the current block (row index from the auxiliary hashing table). It also serves the role of unique block identifiers. This is convenient, because hasher addresses are guaranteed to be unique. Registers b0​,...,b6​, which encode opcodes for operation to be executed by the VM. Each of these registers can contain a single binary value (either 1 or 0). And together these values describe a single opcode. Hasher registers h0​,...,h7​. When control flow operations are executed, these registers are used to provide inputs for the current block's hash computation (e.g., for JOIN, SPLIT, LOOP, SPAN, CALL, SYSCALL operations) or to record the result of the hash computation (i.e., for END operation). However, when regular operations are executed, 2 of these registers are used to help with op group decoding, and the remaining 6 can be used to hold operation-specific helper variables. Register sp which contains a binary flag indicating whether the VM is currently executing instructions inside a span block. The flag is set to 1 when the VM executes non-control flow instructions, and is set to 0 otherwise. Register gc which keep track of the number of unprocessed operation groups in a given span block. Register ox which keeps track of a currently executing operation's index within its operation group. Operation batch flags c0​,c1​,c2​ which indicate how many operation groups a given operation batch contains. These flags are set only for SPAN and RESPAN operations, and are set to 0's otherwise. Two additional registers (not shown) used primarily for constraint degree reduction.","breadcrumbs":"Design » Program decoder » Decoder trace","id":"111","title":"Decoder trace"},"112":{"body":"To compute hashes of program blocks, the decoder relies on the hash chiplet . Specifically, the decoder needs to perform two types of hashing operations: A simple 2-to-1 hash, where we provide a sequence of 8 field elements, and get back 4 field elements representing the result. Computing such a hash requires 8 rows in the hash chiplet. A sequential hash of n elements. Computing such a hash requires multiple absorption steps, and at each step 8 field elements are absorbed into the hasher. Thus, computing a sequential hash of n elements requires ⌈n/8⌉ rows in the hash chiplet. At the end, we also get 4 field elements representing the result. To make hashing requests to the hash chiplet and to read the results from it, we will need to divide out relevant values from the chiplets bus column bchip​ as described below. Simple 2-to-1 hash To initiate a 2-to-1 hash of 8 elements (v0​,...,v7​) we need to divide bchip​ by the following value: α0​+α1​⋅mbp​+α2​⋅r+i=0∑7​(αi+8​⋅vi​) where: mbp​ is a label indicating beginning of a new permutation. Value of this label is computed based on hash chiplet selector flags according to the methodology described here . r is the address of the row at which the hashing begins. Some α values are skipped in the above (e.g., α3​) because of the specifics of how auxiliary hasher table rows are reduced to field elements (described here ). For example, α3​ is used as a coefficient for node index values during Merkle path computations in the hasher, and thus, is not relevant in this case. The α4​ term is omitted when the number of items being hashed is a multiple of the rate width (8) because it is multiplied by 0 - the value of the first capacity register as determined by the hasher chiplet logic . To read the 4-element result (u0​,...,u3​), we need to divide bchip​ by the following value: α0​+α1​⋅mhout​+α2​⋅(r+7)+i=0∑3​(αi+8​⋅ui​) where: mhout​ is a label indicating return of the hash value. Value of this label is computed based on hash chiplet selector flags according to the methodology described here . r is the address of the row at which the hashing began. Sequential hash To initiate a sequential hash of n elements (v0​,...,vn−1​), we need to divide bchip​ by the following value: α0​+α1​⋅mbp​+α2​⋅r+α4​⋅n+i=0∑7​(αi+8​⋅vi​) This also absorbs the first 8 elements of the sequence into the hasher state. Then, to absorb the next sequence of 8 elements (e.g., v8​,...,v15​), we need to divide bchip​ by the following value: α0​+α1​⋅mabp​+α2​⋅(r+7)+i=0∑7​(αi+8​⋅vi+8​) Where mabp​ is a label indicating absorption of more elements into the hasher state. Value of this label is computed based on hash chiplet selector flags according to the methodology described here . We can keep absorbing elements into the hasher in the similar manner until all elements have been absorbed. Then, to read the result (e.g., u0​,...,u3​), we need to divide bchip​ by the following value: α0​+α1​⋅mhout​+α2​⋅(r+⌈n/8⌉⋅8−1)+i=0∑3​(αi+8​⋅ui​) Thus, for example, if n=14, the result will of the hash will be available at hasher row r+15.","breadcrumbs":"Design » Program decoder » Program block hashing","id":"112","title":"Program block hashing"},"113":{"body":"In addition to the hash chiplet, control flow operations rely on 3 virtual tables: block stack table, block hash table, and op group table. These tables are virtual in that they don't require separate trace columns. Their state is described solely by running product columns: p1​, p2​, and p3​. The tables are described in the following sections. Block stack table When the VM starts executing a new program block, it adds its block ID together with the ID of its parent block (and some additional info) to the block stack table. When a program block is fully executed, it is removed from the table. In this way, the table represents a stack of blocks which are currently executing on the VM. By the time program execution completes, block stack table must be empty. The table can be thought of as consisting of 3 columns as shown below: decoder_block_stack_table where: The first column (t0​) contains the ID of the block. The second column (t1​) contains the ID of the parent block. If the block has no parent (i.e., it is a root block of the program), parent ID is 0. The third column (t2​) contains a binary value which is set to 1 is the block is a loop block, and to 0 otherwise. Running product column p1​ is used to keep track of the state of the table. At any step of the computation, the current value of p1​ defines which rows are present in the table. To reduce a row in the block stack table to a single value, we compute the following. row=α0​+i=0∑3​(αi+1​⋅ti​) Where α0​,...,α3​ are the random values provided by the verifier. 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 its hash from the block hash table. Thus, by the time program execution completes, block hash table must be empty. The table can be thought of as consisting of 7 columns as shown below: block_hash_table where: The first column (t0​) contains the ID of the block's parent. For program root, parent ID is 0. The next 4 columns (t1​,...,t4​) contain the hash of the block. The next column (t5​) contains a binary value which is set to 1 if the block is the first child of a join block, and to 0 otherwise. The last column (t6​) contains a binary value which is set to 1 if the block is a body of a loop, and to 0 otherwise. Running product column p2​ is used to keep track of the state of the table. At any step of the computation, the current value of p2​ defines which rows are present in the table. To reduce a row in the block hash table to a single value, we compute the following. row=α0​+i=0∑6​(αi+1​⋅ti​) Where α0​,...,α7​ are the random values provided by the verifier. Unlike other virtual tables, block hash table does not start out in an empty state. Specifically, it is initialized with a single row containing the hash of the program's root block. This needs to be done because the root block does not have a parent and, thus, otherwise it would never be added to the block hash table. Initialization of the block hash table is done by setting the initial value of p2​ to the value of the row containing the hash of a program's root block. Op group table Op group table is used in decoding of span blocks, which are leaves in a program's MAST. As described here , a span block can contain one or more operation batches, each batch containing up to 8 operation groups. When the VM starts executing a new batch of operations, it adds all operation groups within a batch, except for the first one, to the op group table. Then, as the VM starts executing an operation group, it removes the group from the table. Thus, by the time all operation groups in a batch have been executed, the op group table must be empty. The table can be thought of as consisting of 3 columns as shown below: decoder_op_group_table The meaning of the columns is as follows: The first column (t0​) contains operation batch ID. During the execution of the program, each operation batch is assigned a unique ID. The second column (t1​) contains the position of the group in the span block (not just in the current batch). The position is 1-based and is counted from the end. Thus, for example, if a span block consists of a single batch with 4 groups, the position of the first group would be 4, the position of the second group would be 3 etc. (the reason for this is explained in this section). Note that the group with position 4 is not added to the table, because it is the first group in the batch, so the first row of the table will be for the group with position 3. The third column (t2​) contains the actual values of operation groups (this could include up to 9 opcodes or a single immediate value). Permutation column p3​ is used to keep track of the state of the table. At any step of the computation, the current value of p3​ defines which rows are present in the table. To reduce a row in the op group table to a single value, we compute the following. row=α0​+i=0∑2​(αi+1​⋅ti​) Where α0​,...,α3​ are the random values provided by the verifier.","breadcrumbs":"Design » Program decoder » Control flow tables","id":"113","title":"Control flow tables"},"114":{"body":"In this section we describe high-level semantics of executing all control flow operations. The descriptions are not meant to be complete and omit some low-level details. However, they provide good intuition on how these operations work. JOIN operation Before a JOIN operation is executed by the VM, the prover populates h0​,...,h7​ registers with hashes of left and right children of the join program block as shown in the diagram below. decoder_join_operation In the above diagram, blk is the ID of the join block which is about to be executed. blk is also the address of the hasher row in the auxiliary hasher table. prnt is the ID of the block's parent. When the VM executes a JOIN operation, it does the following: Adds a tuple (blk, prnt, 0) to the block stack table. Adds tuples (blk, left_child_hash, 1, 0) and (blk, right_child_hash, 0, 0) to the block hash table. Initiates a 2-to-1 hash computation in the hash chiplet (as described here ) using blk as row address in the auxiliary hashing table and h0​,...,h7​ as input values. SPLIT operation Before a SPLIT operation is executed by the VM, the prover populates h0​,...,h7​ registers with hashes of true and false branches of the split program block as shown in the diagram below. decoder_split_operation In the above diagram, blk is the ID of the split block which is about to be executed. blk is also the address of the hasher row in the auxiliary hasher table. prnt is the ID of the block's parent. When the VM executes a SPLIT operation, it does the following: Adds a tuple (blk, prnt, 0) to the block stack table. Pops the stack and: a. If the popped value is 1, adds a tuple (blk, true_branch_hash, 0, 0) to the block hash table. b. If the popped value is 0, adds a tuple (blk, false_branch_hash, 0, 0) to the block hash table. c. If the popped value is neither 1 nor 0, the execution fails. Initiates a 2-to-1 hash computation in the hash chiplet (as described here ) using blk as row address in the auxiliary hashing table and h0​,...,h7​ as input values. LOOP operation Before a LOOP operation is executed by the VM, the prover populates h0​,...,h3​ registers with hash of the loop's body as shown in the diagram below. decoder_loop_operation In the above diagram, blk is the ID of the loop block which is about to be executed. blk is also the address of the hasher row in the auxiliary hasher table. prnt is the ID of the block's parent. When the VM executes a LOOP operation, it does the following: Pops the stack and: a. If the popped value is 1 adds a tuple (blk, prnt, 1) to the block stack table (the 1 indicates that the loop's body is expected to be executed). Then, adds a tuple (blk, loop_body_hash, 0, 1) to the block hash table. b. If the popped value is 0, adds (blk, prnt, 0) to the block stack table. In this case, nothing is added to the block hash table. c. If the popped value is neither 1 nor 0, the execution fails. Initiates a 2-to-1 hash computation in the hash chiplet (as described here ) using blk as row address in the auxiliary hashing table and h0​,...,h3​ as input values. SPAN operation Before a SPAN operation is executed by the VM, the prover populates h0​,...,h7​ registers with contents of the first operation batch of the span block as shown in the diagram below. The prover also sets the group count register gc to the total number of operation groups in the span block. decoder_span_block In the above diagram, blk is the ID of the span block which is about to be executed. blk is also the address of the hasher row in the auxiliary hasher table. prnt is the ID of the block's parent. g0_op0 is the first operation of the batch, and g_0' is the first operation group of the batch with the first operation removed. When the VM executes a SPAN operation, it does the following: Adds a tuple (blk, prnt, 0) to the block stack table. Adds groups of the operation batch, as specified by op batch flags (see here ) to the op group table. Initiates a sequential hash computation in the hash chiplet (as described here ) using blk as row address in the auxiliary hashing table and h0​,...,h7​ as input values. Sets the in_span register to 1. Decrements group_count register by 1. Sets the op_index register to 0. DYN operation Before a DYN operation is executed by the VM, the prover populates h0​,...,h7​ registers with 0 as shown in the diagram below. decoder_dyn_operation In the above diagram, blk is the ID of the dyn block which is about to be executed. blk is also the address of the hasher row in the auxiliary hasher table. prnt is the ID of the block's parent. When the VM executes a DYN operation, it does the following: Adds a tuple (blk, prnt, 0) to the block stack table. Gets the hash of the dynamic code block dynamic_block_hash from the top four elements of the stack. Adds the tuple (blk, dynamic_block_hash, 0, 0) to the block hash table. Initiates a 2-to-1 hash computation in the hash chiplet (as described here ) using blk as row address in the auxiliary hashing table and h0​,...,h7​ as input values. END operation Before an END operation is executed by the VM, the prover populates h0​,...,h3​ registers with the hash of the block which is about to end. The prover also sets values in h4​ and h5​ registers as follows: h4​ is set to 1 if the block is a body of a loop block. We denote this value as f0. h5​ is set to 1 if the block is a loop block. We denote this value as f1. decoder_end_operation In the above diagram, blk is the ID of the block which is about to finish executing. prnt is the ID of the block's parent. When the VM executes an END operation, it does the following: Removes a tuple (blk, prnt, f1) from the block stack table. Removes a tuple (prnt, current_block_hash, nxt, f0) from the block hash table, where nxt=0 if the next operation is either END or REPEAT, and 1 otherwise. Reads the hash result from the hash chiplet (as described here ) using blk + 7 as row address in the auxiliary hashing table. If h5​=1 (i.e., we are exiting a loop block), pops the value off the top of the stack and verifies that the value is 0. Verifies that group_count register is set to 0. HALT operation Before a HALT operation is executed by the VM, the VM copies values in h0​,...,h3​ registers to the next row as illustrated in the diagram below: decoder_halt_operation In the above diagram, blk is the ID of the block which is about to finish executing. When the VM executes a HALT operation, it does the following: Verifies that block address register is set to 0. If we are not at the last row of the trace, verifies that the next operation is HALT. Copies values of h0​,...,h3​ registers to the next row. Populates all other decoder registers with 0's in the next row. REPEAT operation Before a REPEAT operation is executed by the VM, the VM copies values in registers h0​,...,h4​ to the next row as shown in the diagram below. decoder_repeat_operation In the above diagram, blk is the ID of the loop's body and prnt is the ID of the loop. When the VM executes a REPEAT operation, it does the following: Checks whether register h4​ is set to 1. If it isn't (i.e., we are not in a loop), the execution fails. Pops the stack and if the popped value is 1, adds a tuple (prnt, loop_body_loop 0, 1) to the block hash table. If the popped value is not 1, the execution fails. The effect of the above is that the VM needs to execute the loop's body again to clear the block hash table. RESPAN operation Before a RESPAN operation is executed by the VM, the VM copies the ID of the current block blk and the number of remaining operation groups in the span to the next row, and sets the value of in_span column to 0. The prover also sets the value of h1​ register for the next row to the ID of the current block's parent prnt as shown in the diagram below: decoder_respan_operation In the above diagram, g0_op0 is the first operation of the new operation batch, and g0' is the first operation group of the batch with g0_op0 operation removed. When the VM executes a RESPAN operation, it does the following: Increments block address by 8. Removes the tuple (blk, prnt, 0) from the block stack table. Adds the tuple (blk+8, prnt, 0) to the block stack table. Absorbs values in registers h0​,...,h7​ into the hasher state of the hash chiplet (as described here ). Sets the in_span register to 1. Adds groups of the operation batch, as specified by op batch flags (see here ) to the op group table using blk+8 as batch ID. The net result of the above is that we incremented the ID of the current block by 8 and added the next set of operation groups to the op group table.","breadcrumbs":"Design » Program decoder » Control flow operation semantics","id":"114","title":"Control flow operation semantics"},"115":{"body":"When decoding a program, we start at the root block of the program. We can compute the hash of the root block directly from hashes of its children. The prover provides hashes of the child blocks non-deterministically, and we use them to compute the program's hash (here we rely on the hash chiplet). We then verify the program hash via boundary constraints. Thus, if the prover provided valid hashes for the child blocks, we will get the expected program hash. Now, we need to verify that the VM executed the child blocks correctly. We do this recursively similar to what is described above: for each of the blocks, the prover provides hashes of its children non-deterministically and we verify that the hash has been computed correctly. We do this until we get to the leaf nodes (i.e., span blocks). Hashes of span blocks are computed sequentially from the instructions executed by the VM. The sections below illustrate how different types of code blocks are decoded by the VM.","breadcrumbs":"Design » Program decoder » Program decoding","id":"115","title":"Program decoding"},"116":{"body":"When decoding a join bock, the VM first executes a JOIN operation, then executes the first child block, followed by the second child block. Once the children of the join block are executed, the VM executes an END operation. This is illustrated in the diagram below. decoder_join_block_decoding As described previously, when the VM executes a JOIN operation, hashes of both children are added to the block hash table. These hashes are removed only when the END operations for the child blocks are executed. Thus, until both child blocks are executed, the block hash table is not cleared.","breadcrumbs":"Design » Program decoder » JOIN block decoding","id":"116","title":"JOIN block decoding"},"117":{"body":"When decoding a split block, the decoder pops an element off the top of the stack, and if the popped element is 1, executes the block corresponding to the true branch. If the popped element is 0, the decoder executes the block corresponding to the false branch. This is illustrated on the diagram below. decoder_split_block_decoding As described previously, when the VM executes a SPLIT operation, only the hash of the branch to be executed is added to the block hash table. Thus, until the child block corresponding to the required branch is executed, the block hash table is not cleared.","breadcrumbs":"Design » Program decoder » SPLIT block decoding","id":"117","title":"SPLIT block decoding"},"118":{"body":"When decoding a loop bock, we need to consider two possible scenarios: When the top of the stack is 1, we need to enter the loop and execute loop body at least once. When the top of the stack is, 0 we need to skip the loop. In both cases, we need to pop an element off the top of the stack. Executing the loop If the top of the stack is 1, the VM executes a LOOP operation. This removes the top element from the stack and adds the hash of the loop's body to the block hash table. It also adds a row to the block stack table setting the is_loop value to 1. To clear the block hash table, the VM needs to execute the loop body (executing the END operation for the loop body block will remove the corresponding row from the block hash table). After loop body is executed, if the top of the stack is 1, the VM executes a REPEAT operation (executing REPEAT operation when the top of the stack is 0 will result in an error). This operation again adds the hash of the loop's body to the block hash table. Thus, the VM needs to execute the loop body again to clear the block hash table. This process is illustrated on the diagram below. decoder_loop_execution The above steps are repeated until the top of the stack becomes 0, at which point the VM executes the END operation. Since in the beginning we set is_loop column in the block stack table to 1, h6​ column will be set to 1 when the END operation is executed. Thus, executing the END operation will also remove the top value from the stack. If the removed value is not 0, the operation will fail. Thus, the VM can exit the loop block only when the top of the stack is 0. Skipping the loop If the top of the stack is 0, the VM still executes the LOOP operation. But unlike in the case when we need to enter the loop, the VM sets is_loop flag to 0 in the block stack table, and does not add any rows to the block hash table. The last point means that the only possible operation to be executed after the LOOP operation is the END operation. This is illustrated in the diagram below. decoder_loop_skipping Moreover, since we've set the is_loop flag to 0, executing the END operation does not remove any items from the stack.","breadcrumbs":"Design » Program decoder » LOOP block decoding","id":"118","title":"LOOP block decoding"},"119":{"body":"When decoding a dyn bock, the VM first executes a DYN operation, then executes the child block dynamically specified by the top of the stack. Once the child of the dyn block has been executed, the VM executes an END operation. This is illustrated in the diagram below. decoder_dyn_block_decoding As described previously, when the VM executes a DYN operation, the hash of the child is added to the block hash table. This hash is removed only when the END operation for the child block is executed. Thus, until the child block corresponding to the dynamically specified target is executed, the block hash table is not cleared.","breadcrumbs":"Design » Program decoder » DYN block decoding","id":"119","title":"DYN block decoding"},"12":{"body":"","breadcrumbs":"Introduction » Usage » CLI interface","id":"12","title":"CLI interface"},"120":{"body":"As described here , a span block can contain one or more operation batches, each batch containing up to 8 operation groups. At the high level, decoding of a span block is done as follows: At the beginning of the block, we make a request to the hash chiplet which initiates the hasher, absorbs the first operation batch (8 field elements) into the hasher, and returns the row address of the hasher, which we use as the unique ID for the span block (see here ). We then add groups of the operation batch, as specified by op batch flags (but always skipping the first one) to the op group table. We then remove operation groups from the op group table in the FIFO order one by one, and decode them in the manner similar to the one described here . Once all operation groups in a batch have been decoded, we absorb the next batch into the hasher and repeat the process described above. Once all batches have been decoded, we return the hash of the span block from the hasher. Overall, three control flow operations are used when decoding a span block: SPAN operation is used to initialize a hasher and absorbs the first operation batch into it. RESPAN operation is used to absorb any additional batches in the span block. END operation is used to end the decoding of a span block and retrieve its hash from the hash chiplet. Operation group decoding As described here , an operation group is a sequence of operations which can be encoded into a single field element. For a field element of 64 bits, we can fit up to 9 operations into a group. We do this by concatenating binary representations of opcodes together with the first operation located in the least significant position. We can read opcodes from the group by simply subtracting them from the op group value and then dividing the result by 27. Once the value of the op group reaches 0, we know that all opcodes have been read. Graphically, this can be illustrated like so: decoder_operation_group_decoding Notice that despite their appearance, op bits is actually 7 separate registers, while op group is just a single register. We also need to make sure that at most 9 operations are executed as a part of a single group. For this purpose we use the op_index column. Values in this column start out at 0 for each operation group, and are incremented by 1 for each executed operation. To make sure that at most 9 operations can be executed in a group, the value of the op_index column is not allowed to exceed 8. Operation batch flags Operation batch flags are used to specify how many operation groups comprise a given operation batch. For most batches, the number of groups will be equal to 8. However, for the last batch in a block (or for the first batch, if the block consists of only a single batch), the number of groups may be less than 8. Since processing of new batches starts only on SPAN and RESPAN operations, only for these operations the flags can be set to non-zero values. To simplify the constraint system, the number of groups in a batch can be only one of the following values: 1, 2, 4, and 8. If the number of groups in a batch does not match one of these values, the batch is simply padded with NOOP's (one NOOP per added group). Consider the diagram below. decoder_OPERATION_batch_flags In the above, the batch contains 3 operation groups. To bring the count up to 4, we consider the 4-th group (i.e., 0) to be a part of the batch. Since a numeric value for NOOP operation is 0, op group value of 0 can be interpreted as a single NOOP. Operation batch flags (denoted as c0​,c1​,c2​), encode the number of groups and define how many groups are added to the op group table as follows: (1, 0, 0) - 8 groups. Groups in h1​,...h7​ are added to the op group table. (0, 1, 0) - 4 groups. Groups in h1​,...h3​ are added to the op group table (0, 0, 1) - 2 groups. Groups in h1​ is added to the op group table. (0, 1, 1) - 1 group. Nothing is added to the op group table (0, 0, 0) - not a SPAN or RESPAN operation. Single-batch span The simplest example of a span block is a block with a single batch. This batch may contain up to 8 operation groups (e.g., g0​,...,g7​). Decoding of such a block is illustrated in the diagram below. decoder_single_batch_span Before the VM starts processing this span block, the prover populates registers h0​,...,h7​ with operation groups g0​,...,g7​. The prover also puts the total number of groups into the group_count register gc. In this case, the total number of groups is 8. When the VM executes a SPAN operation, it does the following: Initiates hashing of elements g0​,...,g7​ using hash chiplet. The hasher address is used as the block ID blk, and it is inserted into addr register in the next row. Adds a tuple (blk, prnt, 0) to the block stack table. Sets the is_span register to 1 in the next row. Sets the op_index register to 0 in the next row. Decrements group_count register by 1. Sets op bits registers at the next step to the first operation of g0​, and also copies g0​ with the first operation removed (denoted as g0′​) to the next row. Adds groups g1​,...,g7​ to the op group table. Thus, after the SPAN operation is executed, op group table looks as shown below. decoder_op_group_table_after_span_op Then, with every step the next operation is removed from g0​, and by step 9, the value of g0​ is 0. Once this happens, the VM does the following: Decrements group_count register by 1. Sets op bits registers at the next step to the first operation of g1​. Sets hasher register h0​ to the value of g1​ with the first operation removed (denoted as g1′​). Removes row (blk, 7, g1) from the op group table. This row can be obtained by taking values from registers: addr, group_count, and h0′​+i=0∑6​(2i⋅bi′​) for i∈[0,7), where h0′​ and bi′​ refer to values in the next row for the first hasher column and op_bits columns respectively. Note that we rely on the group_count column to construct the row to be removed from the op group table. Since group count is decremented from the total number of groups to 0, to remove groups from the op group table in correct order, we need to assign group position to groups in the op group table in the reverse order. For example, the first group to be removed should have position 7, the second group to be removed should have position 6 etc. Decoding of g1​ is performed in the same manner as decoding of g0​: with every subsequent step the next operation is removed from g1​ until its value reaches 0, at which point, decoding of group g2​ begins. The above steps are executed until value of group_count reaches 0. Once group_count reaches 0 and the last operation group g7​ is executed, the VM executes the END operation. Semantics of the END operation are described here . Notice that by the time we get to the END operation, all rows are removed from the op group table. Multi-batch span A span block may contain an unlimited number of operation batches. As mentioned previously, to absorb a new batch into the hasher, the VM executes a RESPAN operation. The diagram below illustrates decoding of a span block consisting of two operation batches. decoder_multi_batch_span Decoding of such a block will look very similar to decoding of the single-span block described previously, but there also will be some differences. First, after the SPAN operation is executed, the op group table will look as follows: decoder_op_group_table_multi_span Notice that while the same groups (g1​,...,g7​) are added to the table, their positions now reflect the total number of groups in the span block. Second, executing a RESPAN operation increments hasher address by 8. This is done because absorbing additional 8 elements into the hasher state requires 8 more rows in the auxiliary hasher table. Incrementing value of addr register actually changes the ID of the span block (though, for a span block, it may be more appropriate to view values in this column as IDs of individual operation batches). This means that we also need to update the block stack table. Specifically, we need to remove row (blk, prnt, 0) from it, and replace it with row (blk + 8, prnt, 0). To perform this operation, the prover sets the value of h1​ in the next row to prnt. Executing a RESPAN operation also adds groups g9​,g10​,g11​ to the op group table, which now would look as follows: decoder_op_group_table_post_respan Then, the execution of the second batch proceeds in a manner similar to the first batch: we remove operations from the current op group, execute them, and when the value of the op group reaches 0, we start executing the next group in the batch. Thus, by the time we get to the END operation, the op group table should be empty. When executing the END operation, the hash of the span block will be read from hasher row at address addr + 7, which, in our example, will be equal to blk + 15. Handling immediate values Miden VM operations can carry immediate values. Currently, the only such operation is a PUSH operation. Since immediate values can be thought of as constants embedded into program code, we need to make sure that changing immediate values affects program hash. To achieve this, we treat immediate values in a manner similar to how we treat operation groups. Specifically, when computing hash of a span block, immediate values are absorbed into the hasher state in the same way as operation groups are. As mentioned previously, an immediate value is represented by a single field element, and thus, an immediate value takes place of a single operation group. The diagram below illustrates decoding of a span block with 9 operations one of which is a PUSH operation. decoder_decoding_span_block_with_push In the above, when the SPAN operation is executed, immediate value imm0 will be added to the op group table, which will look as follows: decoder_imm_vale_op_group_table Then, when the PUSH operation is executed, the VM will do the following: Decrement group_count by 1. Remove a row from the op group table equal to (addr, group_count, s0'), where s0′​ is the value of the top of the stack at the next row (i.e., it is the value that is pushed onto the stack). Thus, after the PUSH operation is executed, the op group table is cleared, and group count decreases to 0 (which means that there are no more op groups to execute). Decoding of the rest of the op group proceeds as described in the previous sections.","breadcrumbs":"Design » Program decoder » SPAN block decoding","id":"120","title":"SPAN block decoding"},"121":{"body":"Let's run through an example of decoding a simple program shown previously: begin  if.true  else  end\nend Translating this into code blocks with IDs assigned, we get the following: b0: JOIN b1: SPAN  b1: END b2: SPLIT b3: SPAN  b3: END b4: SPAN  b4: END b2: END\nb0: END The root of the program is a join block b0​. This block contains two children: a span bock b1​ and a split block b2​. In turn, the split block b2​ contains two children: a span block b3​ and a span block b4​. When this program is executed on the VM, the following happens: Before the program starts executing, block hash table is initialized with a single row containing the hash of b0​. Then, JOIN operation for b0​ is executed. It adds hashes of b1​ and b2​ to the block hash table. It also adds an entry for b0​ to the block stack table. States of both tables after this step are illustrated below. Then, span b1​ is executed and a sequential hash of its operations is computed. Also, when SPAN operation for b1​ is executed, an entry for b1​ is added to the block stack table. At the end of b1​ (when END is executed), entries for b1​ are removed from both the block hash and block stack tables. Then, SPLIT operation for b2​ is executed. It adds an entry for b2​ to the block stack table. Also, depending on whether the top of the stack is 1 or 0, either hash of b3​ or hash of b4​ is added to the block hash table. Let's say the top of the stack is 1. Then, at this point, the block hash and block stack tables will look like in the second picture below. Then, span b3​ is executed and a sequential hash of its instructions is computed. Also, when SPAN operation for b3​ is executed, an entry for b3​ is added to the block stack table. At the end of b3​ (when END is executed), entries for b3​ are removed from both the block hash and block stack tables. Then, END operation for b2​ is executed. It removes the hash of b2​ from the block hash table, and also removes the entry for b2​ from the block stack table. The third picture below illustrates the states of block stack and block hash tables after this step. Then, END for b0​ is executed, which removes entries for b0​ from the block stack and block hash tables. At this point both tables are empty. Finally, a sequence of HALT operations is executed until the length of the trace reaches a power of two. States of block hash and block stack tables after step 2: decoder_state_block_hash_2 States of block hash and block stack tables after step 4: decoder_state_block_hash_4 States of block hash and block stack tables after step 6: decoder_state_block_hash_6","breadcrumbs":"Design » Program decoder » Program decoding example","id":"121","title":"Program decoding example"},"122":{"body":"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 s0​. air_decoder_columns 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 fopname​. For example, when the VM executes a PUSH operation, flag fpush​=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 fjoin​ 5 Stack remains unchanged. SPLIT fsplit​ 5 Top stack element is dropped. LOOP floop​ 5 Top stack element is dropped. REPEAT frepeat​ 4 Top stack element is dropped. SPAN fspan​ 5 Stack remains unchanged. RESPAN frespan​ 4 Stack remains unchanged. DYN fdyn​ 5 Stack remains unchanged. CALL fcall​ 4 Stack remains unchanged. SYSCALL fsyscall​ 4 Stack remains unchanged. END fend​ 4 When exiting a loop block, top stack element is dropped; otherwise, the stack remains unchanged. HALT fhalt​ 4 Stack remains unchanged. PUSH fpush​ 4 An immediate value is pushed onto the stack. We also use the control flow flag fctrl​ 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 , the general idea of the decoder is that the prover provides the program to the VM by populating some of cells in the trace non-deterministically. Values in these are then used to update virtual tables (represented via multiset checks) such as block hash table, block stack table etc. Transition constraints are used to enforce that the tables are updates correctly, and we also apply boundary constraints to enforce the correct initial and final states of these tables. One of these boundary constraints binds the execution trace to the hash of the program being executed. Thus, if the virtual tables were updated correctly and boundary constraints hold, we can be convinced that the prover executed the claimed program on the VM. 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.","breadcrumbs":"Design » Program decoder » Decoder constraints » Miden VM decoder AIR constraints","id":"122","title":"Miden VM decoder AIR constraints"},"123":{"body":"When SPLIT or LOOP operation is executed, the top of the operand stack must contain a binary value: (fsplit​+floop​)⋅(s02​−s0​)=0 | degree=7 When a DYN operation is executed, the hasher registers must all be set to 0: fdyn​⋅(1−hi​)=0 for i∈[0,8) | degree=6 When REPEAT operation is executed, the value at the top of the operand stack must be 1: frepeat​⋅(1−s0​)=0 | degree=5 Also, when REPEAT operation is executed, the value in h4​ column (the is_loop_body flag), must be set to 1. This ensures that REPEAT operation can be executed only inside a loop: frepeat​⋅(1−h4​)=0 | degree=5 When RESPAN operation is executed, we need to make sure that the block ID is incremented by 8: frespan​⋅(a′−a−8)=0 | degree=5 When END operation is executed and we are exiting a loop block (i.e., is_loop, value which is stored in h5​, is 1), the value at the top of the operand stack must be 0: fend​⋅h5​⋅s0​=0 | degree=6 Also, when END operation is executed and the next operation is REPEAT, values in h0​,...,h4​ (the hash of the current block and the is_loop_body flag) must be copied to the next row: fend​⋅frepeat′​⋅(hi′​−hi​)=0 for i∈[0,5) | degree=9 A HALT instruction can be followed only by another HALT instruction: fhalt​⋅(1−fhalt′​)=0 | degree=8 When a HALT operation is executed, block address column must be 0: fhalt​⋅a=0 | degree=5 Values in op_bits columns must be binary (i.e., either 1 or 0): bi2​−bi​=0 for i∈[0,7) | 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−fctrl​=0 | degree=5","breadcrumbs":"Design » Program decoder » Decoder constraints » General constraints","id":"123","title":"General constraints"},"124":{"body":"As described previously , 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 h0​,...,h7​. 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 span 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 h0​,...,h7​. 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.","breadcrumbs":"Design » Program decoder » Decoder constraints » Block hash computation constraints","id":"124","title":"Block hash computation constraints"},"125":{"body":"The decoder communicates with the hash chiplet via the chiplets bus . This works by dividing values of the multiset check column bchip​ by the values of operations providing inputs to or reading outputs from the hash chiplet. A constraint to enforce this would look as bchip′​⋅u=bchip​, 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 for an explanation of how values for these labels are computed): mbp​ this label specifies that we are starting a new hash computation. mabp​ this label specifies that we are absorbing the next sequence of 8 elements into an ongoing hash computation. mhout​ this label specifies that we are reading the result of a hash computation. To simplify constraint description, we define the following variables: hinit​=α0​+α1​⋅mbp​+α2​⋅a′+i=0∑7​(αi+8​⋅hi​) In the above, hinit​ can be thought of as initiating a hasher with address a′ and absorbing 8 elements from the hasher state (h0​,...,h7​) into it. Control blocks are always padded to fill the hasher rate and as such the α4​ (first capacity register) term is set to 0. habp​=α0​+α1​⋅mabp​+α2​⋅a′+i=0∑7​(αi+8​⋅hi​) 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 habp​ 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 habp​ label is happening. hres​=α0​+α1​⋅mhout​+α2​⋅(a+7)+i=0∑3​(αi+8​⋅hi​) 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. fctrli​=fjoin​+fsplit​+floop​+fdyn​+fcall​ | degree=5 In the above, fctrli​ is set to 1 when a control flow operation that signifies the initialization of a control block is being executed on the VM. Otherwise, it is set to 0. An exception is made for the SYSCALL operation. Although it also signifies the initialization of a control block, it must additionally send a procedure access request to the kernel ROM chiplet via the chiplets bus. Therefore, it is excluded from this flag and its communication with the chiplets bus is handled separately. d=b=0∑6​(bi​⋅2i) 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 α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, DYN, CALL, SYSCALL) is executed, a new hasher is initialized and the contents of h0​,...,h7​ are absorbed into the hasher. As mentioned above, the opcode value d is populated in the second capacity resister via the α5​ term. uctrli​=fctrli​⋅(hinit​+α5​⋅d) | 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 kproc​. kproc​=α6​+α7​⋅opkrom​+i=0∑3​(αi+8​⋅hi​) In the above, opkrom​ is the unique operation label of the kernel procedure call operation. The values h0​,h1​,h2​,h3​ contain the root hash of the procedure being called, which is the procedure that must be requested from the kernel ROM chiplet. usyscall​=fsyscall​⋅(hinit​+α5​⋅d)⋅kproc​ | degree=7 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. When SPAN operation is executed, a new hasher is initialized and contents of h0​,...,h7​ 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 α4​ is set to 0: uspan​=fspan​⋅hinit​ | degree=6 When RESPAN operation is executed, contents of h0​,...,h7​ (which contain the new operation batch) are absorbed into the hasher: urespan​=frespan​⋅habp​ | degree=5 When END operation is executed, the hash result is copied into registers h0​,..,h3​: uend​=fend​⋅hres​ | degree=5 Using the above definitions, we can describe the constraint for computing block hashes as follows: bchip′​⋅(uctrli​+usyscall​+uspan​+urespan​+uend​+1−(fctrli​+fsyscall​+fspan​+frespan​+fend​))=bchip​ 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 bchip′​=bchip​. The degree of this constraint is 8.","breadcrumbs":"Design » Program decoder » Decoder constraints » Chiplets bus constraints","id":"125","title":"Chiplets bus constraints"},"126":{"body":"As described previously , 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 p1​ by a value representing a tuple (blk_id, prnt_id, is_loop). A constraint to enforce this would look as p1′​=p1​⋅v, where v is the value representing the row to be added. To remove an entry, we divide the value in column p1​ by a value representing a tuple (blk_id, prnt_id, is_loop). A constraint to enforce this would look as p1′​⋅u=p1​, where u is the value representing the row to be removed. 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 h1​. When JOIN operation is executed, row (a′,a,0) is added to the block stack table: vjoin​=fjoin​⋅(α0​+α1​⋅a′+α2​⋅a) | degree=6 When SPLIT operation is executed, row (a′,a,0) is added to the block stack table: vsplit​=fsplit​⋅(α0​+α1​⋅a′+α2​⋅a) | 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: vloop​=floop​⋅(α0​+α1​⋅a′+α2​⋅a+α3​⋅s0​) | degree=6 When SPAN operation is executed, row (a′,a,0) is added to the block stack table: vspan​=fspan​⋅(α0​+α1​⋅a′+α2​⋅a) | degree=6 When RESPAN operation is executed, row (a,h1′​,0) is removed from the block stack table, and row (a′,h1′​,0) is added to the table. The prover sets the value of register h1​ at the next row to the ID of the parent block: urespan​=frespan​⋅(α0​+α1​⋅a+α2​⋅h1′​) | degree=5vrespan​=frespan​⋅(α0​+α1​⋅a′+α2​⋅h1′​) | degree=5 When a DYN operation is executed, row (a′,a,0) is added to the block stack table: vdyn​=fdyn​⋅(α0​+α1​⋅a′+α2​⋅a) | degree=6 When END operation is executed, row (a,a′,h5​) is removed from the block span table. Register h5​ contains the is_loop flag: uend​=fend​⋅(α0​+α1​⋅a+α2​⋅a′+α3​⋅h5​) | degree=5 Using the above definitions, we can describe the constraint for updating the block stack table as follows: p1′​⋅(uend​+urespan​+1−(fend​+frespan​))=p1​⋅(vjoin​+vsplit​+vloop​+vspan​+vrespan​+vdyn​+1−(fjoin​+fsplit​+floop​+fspan​+frespan​+fdyn​)) 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 p1′​=p1​. The degree of this constraint is 7. In addition to the above transition constraint, we also need to impose boundary constraints against the p1​ column to make sure the first and the last value in the column is set to 1. This enforces that the block stack table starts and ends in an empty state.","breadcrumbs":"Design » Program decoder » Decoder constraints » Block stack table constraints","id":"126","title":"Block stack table constraints"},"127":{"body":"As described previously , 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 span 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 p2​ by a value representing a tuple (prnt_id, block_hash, is_first_child, is_loop_body). A constraint to enforce this would look as p2′​=p2​⋅v, where v is the value representing the row to be added. To remove an entry, we divide the value in column p2​ by a value representing a tuple (prnt_id, block_hash, is_first_child, is_loop_body). A constraint to enforce this would look as p2′​⋅u=p2​, 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: ch1​=α0​+α1​⋅a′+i=0∑3​(αi+2​⋅hi​) | degree=1ch2​=α0​+α1​⋅a′+i=0∑3​(αi+2​⋅hi+4​) | degree=1 Graphically, this looks like so: air_decoder_left_right_child In a similar manner, we define a value representing the result of hash computation as follows: bh=α0​+α1​⋅a+i=0∑3​(αi+2​⋅hi​)+α7​⋅h4​ | degree=1 Note that in the above we use a (block address from the current row) rather than a′ (block address from the next row) as we did for for values of ch1​ and ch2​. Also, note that we are not adding a flag indicating whether the block is the first child of a join block (i.e., α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 α6​ term to the first child value to differentiate it from the second child (i.e., this sets is_first_child to 1): vjoin​=fjoin​⋅(ch1​+α6​)⋅ch2​ | 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: vsplit​=fsplit​⋅(s0​⋅ch1​+(1−s0​)⋅ch2​) | 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 α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: vloop​=floop​⋅s0​⋅(ch1​+α7​) | degree=7 When REPEAT operation is executed, hash of loop body is added to the block hash table. We add α7​ term to indicate that the child is a body of a loop: vrepeat​=frepeat​⋅(ch1​+α7​) | degree=5 When the DYN operation is executed, the hash of the dynamic child is added to the block hash table. Since the child is dynamically specified by the top four elements of the stack, the value representing the dyn block's child must be computed based on the stack rather than from the decoder's hasher registers: chdyn​=α0​+α1​⋅a′+i=0∑3​(αi+2​⋅s3−i​) | degree=1 vdyn​=fdyn​⋅chdyn​ | 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 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 we need to set the term for α6​ coefficient to 1 as shown below: uend​=fend​⋅(bh+α6​⋅(1−(fend′​+frepeat′​))) | degree=8 Using the above definitions, we can describe the constraint for updating the block hash table as follows: p2′​⋅(uend​+1−fend​)=p2​⋅(vjoin​+vsplit​+vloop​+vrepeat​+vdyn​+1−(fjoin​+fsplit​+floop​+frepeat​+fdyn​)) 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 p2′​=p2​. 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 p2​ 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.","breadcrumbs":"Design » Program decoder » Decoder constraints » Block hash table constraints","id":"127","title":"Block hash table constraints"},"128":{"body":"Span block constraints ensure proper decoding of span blocks. In addition to the block stack table constraints and block hash table constraints described previously, decoding of span blocks requires constraints described below.","breadcrumbs":"Design » Program decoder » Decoder constraints » Span block","id":"128","title":"Span block"},"129":{"body":"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. air_decoder_in_spans_column_constraint 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: (fspan​+frespan​)⋅(1−sp′)=0 | degree=6 When the next operation is END or RESPAN, the next value in sp column must be set 0. (fend′​+frespan′​)⋅sp′=0 | degree=5 In all other cases, the value in sp column must be copied over to the next row: (1−fspan​−frespan​−fend′​−frespan′​)⋅(sp′−sp)=0 | 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.","breadcrumbs":"Design » Program decoder » Decoder constraints » In-span column constraints","id":"129","title":"In-span column constraints"},"13":{"body":"To compile Miden VM into a binary, we have a Makefile with the following tasks: make exec This will place an optimized, multi-threaded miden executable into the ./target/optimized directory. It is equivalent to executing: cargo build --profile optimized --features concurrent,executable If you would like to enable single-threaded mode, you can compile Miden VM using the following command: cargo build --profile optimized --features executable For a faster build, you can compile with less optimizations, replacing --profile optimized by --release. Example: cargo build --release --features concurrent,executable In this case, the miden executable will be placed in the ./target/release directory.","breadcrumbs":"Introduction » Usage » Compiling Miden VM","id":"13","title":"Compiling Miden VM"},"130":{"body":"When we are inside a span block, values in block address columns (denoted as a) must remain the same. This can be enforced with the following constraint: sp⋅(a′−a)=0 | 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.","breadcrumbs":"Design » Program decoder » Decoder constraints » Block address constraints","id":"130","title":"Block address constraints"},"131":{"body":"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 span block. In the beginning of a span 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 span 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 h0​=0 inside a span block), the count is decremented by 1. When SPAN, RESPAN, or PUSH operations are executed, the count is decremented by 1. Note that these rules imply that PUSH operation cannot be the last operation in an operation group (otherwise the count would have to be decremented by 2). To simplify the description of the constraints, we will define the following variable: Δgc=gc−gc′ Using this variable, we can describe the constraints against the gc column as follows: Inside a span block, group count can either stay the same or decrease by one: sp⋅Δgc⋅(Δgc−1)=0 | degree=3 When group count is decremented inside a span block, either h0​ must be 0 (we consumed all operations in a group) or we must be executing PUSH operation: sp⋅Δgc⋅(1−fpush​)⋅h0​=0 | degree=7 Notice that the above constraint does not preclude fpush​=1 and h0​=0 from being true at the same time. If this happens, op group decoding constraints (described here ) will force that the operation following the PUSH operation is a NOOP. When executing a SPAN, a RESPAN, or a PUSH operation, group count must be decremented by 1: (fspan​+frespan​+fpush​)⋅(Δgc−1)=0 | degree=6 If the next operation is either an END or a RESPAN, group count must remain the same: Δgc⋅(fend′​+frespan′​)=0 | degree=5 When an END operation is executed, group count must be 0: fend​⋅gc=0 | degree=5","breadcrumbs":"Design » Program decoder » Decoder constraints » Group count constraints","id":"131","title":"Group count constraints"},"132":{"body":"Inside a span block, register h0​ 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. air_decoder_op_group_constraint In the above: The prover sets the value of h0​ 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 27. 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 h0​ 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=i=0∑6​(bi​⋅2i)fsgc​=sp⋅sp′⋅(1−Δgc) op is just an opcode value implied by the values in op_bits registers. fsgc​ is a flag which is set to 1 when the group count within a span 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 fsgc​ flag is mutually exclusive with fspan​, frespan​, and fpush​ 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 a PUSH operation is executed or when the group count does not change, the value in h0​ should be decremented by the value of the opcode in the next row. (fspan​+frespan​+fpush​+fsgc​)⋅(h0​−h0′​⋅27−op′)=0 | degree=6 Notice that when the group count does change, and we are not executing fspan​, frespan​, or fpush​ operations, no constraints are placed against h0​, and thus, the prover can populate this register non-deterministically. When we are in a span block and the next operation is END or RESPAN, the current value in h0​ column must be 0. sp⋅(fend′​+frespan′​)⋅h0​=0 | degree=6","breadcrumbs":"Design » Program decoder » Decoder constraints » Op group decoding constraints","id":"132","title":"Op group decoding constraints"},"133":{"body":"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=Δgc−fpush​Δ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 a PUSH operation). 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: (fspan​+frespan​)⋅ox′=0 | degree=6 When starting a new operation group inside a span 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⋅ng⋅ox′=0 | degree=6 When inside a span 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⋅sp′⋅(1−ng)⋅(Δox−1)=0 | degree=7 Values of op_index must be in the range [0,8]. i=0∏8​(ox−i)=0 | degree=9","breadcrumbs":"Design » Program decoder » Decoder constraints » Op index constraints","id":"133","title":"Op index constraints"},"134":{"body":"Operation batch flag columns (denoted bc0​, bc1​, and bc2​) are used to specify how many operation groups are present in an operation batch. This is relevant for the last batch in a span 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: fg8​=bc0​: there are 8 operation groups in the batch. fg4​=(1−bc0​)⋅bc1​⋅bc2​: there are 4 operation groups in the batch. fg2​=(1−bc0​)⋅(1−bc1​)⋅bc2​: there are 2 operation groups in the batch. fg1​=(1−bc0​)⋅bc1​⋅(1−bc2​): there is only 1 operation groups in the batch. Notice that the degree of fg8​ 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: bci2​−bci​=0 for i∈[0,3) | degree=2 When SPAN or RESPAN operations is executed, one of the batch flags must be set to 1. (fspan​+frespan​)−(fg1​+fg2​+fg4​+fg8​)=0 | degree=5 When we have at most 4 groups in a batch, registers h4​,...,h7​ should be set to 0's. (fg1​+fg2​+fg4​)⋅hi​=0 for i∈[4,8) | degree=4 When we have at most 2 groups in a batch, registers h2​ and h3​ should also be set to 0's. (fg1​+fg2​)⋅hi​=0 for i∈2,3 | degree=4 When we have at most 1 groups in a batch, register h1​ should also be set to 0. fg1​⋅h1​=0 | degree=4","breadcrumbs":"Design » Program decoder » Decoder constraints » Op batch flags constraints","id":"134","title":"Op batch flags constraints"},"135":{"body":"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 span 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 p3​ by a value representing a tuple (batch_id, group_pos, group). A constraint to enforce this would look as p3′​=p3​⋅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., p3′​=p3​⋅v1​⋅v2​⋅v3​...). Flags fg1​, fg2​, fg4​, and fg8​ 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 p3​ by a value representing a tuple (batch_id, group_pos, group). A constraint to enforce this would look as p3′​⋅u=p3​, 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: vi​=α0​+α1​⋅a′+α2​⋅(gc−i)+α3​⋅hi​ | degree=1 Where i∈[1,8). Thus, v1​ defines row value for group in h1​, v2​ defines row value for group h2​ 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=α0​+α1​⋅a+α2​⋅gc+α3​⋅((h0′​⋅27+op′)⋅(1−fpush​)+s0′​⋅fpush​) | degree=5 In the above, the value of the group is computed as (h0′​⋅27+op′)⋅(1−fpush​)+s0′​⋅fpush​. 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 s0​) 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 h0​ 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. fdg​=sp⋅Δgc 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 fg2​, fg4​, fg8​ defined in the previous section, we describe the constraint for updating op group table as follows (note that we do not use fg1​ flag as when a batch consists of a single group, nothing is added to the op group table): p3′​⋅(fdg​⋅u+1−fdg​)=p3​⋅(fg2​⋅v1​+fg4​⋅i=1∏3​vi​+fg8​⋅i=1∏7​vi​−1+(fspan​+frespan​)) The above constraint specifies that: When SPAN or RESPAN operations are executed, we add between 1 and 7 groups to the op group table. When group count is decremented inside a span block, we remove a group from the op group table. The degree of this constraint is 9. In addition to the above transition constraint, we also need to impose boundary constraints against the p3​ 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.","breadcrumbs":"Design » Program decoder » Decoder constraints » Op group table constraints","id":"135","title":"Op group table constraints"},"136":{"body":"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 232), but only the top 16 items are directly accessible to the VM. Items on the stack are elements in a prime field with modulus 264−232+1. To keep the constraint system for the stack manageable, we impose the following rules: All operations executed on the VM can shift the stack by at most one item. That is, the end result of an operation must be that the stack shrinks by one item, grows by one item, or the number of items on the stack stays the same. Stack depth must always be greater than or equal to 16. At the start of program execution, the stack is initialized with exactly 16 input values, all of which could be 0's. By the end of program execution, exactly 16 items must remain on the stack (again, all of them could be 0's). These items comprise the output of the program. To ensure that managing stack depth does not impose significant burden, we adopt the following rule: When the stack depth is 16, removing additional items from the stack does not change its depth. To keep the depth at 16, 0's are inserted into the deep end of the stack for each removed item.","breadcrumbs":"Design » Operand stack » Operand stack","id":"136","title":"Operand stack"},"137":{"body":"The VM allocates 19 trace columns for the stack. The layout of the columns is illustrated below. The meaning of the above columns is as follows: s0​...s15​ are the columns representing the top 16 slots of the stack. Column b0​ contains the number of items on the stack (i.e., the stack depth). In the above picture, there are 16 items on the stacks, so b0​=16. Column b1​ contains an address of a row in the \"overflow table\" in which we'll store the data that doesn't fit into the top 16 slots. When b1​=0, it means that all stack data fits into the top 16 slots of the stack. Helper column h0​ is used to ensure that stack depth does not drop below 16. Values in this column are set by the prover non-deterministically to b0​−161​ when b0​=16, and to any other value otherwise.","breadcrumbs":"Design » Operand stack » Stack representation","id":"137","title":"Stack representation"},"138":{"body":"To keep track of the data which doesn't fit into the top 16 stack slots, we'll use an overflow table. This will be a virtual table . To represent this table, we'll use a single auxiliary column p1​. The table itself can be thought of as having 3 columns as illustrated below. The meaning of the columns is as follows: Column t0​ contains row address. Every address in the table must be unique. Column t1​ contains the value that overflowed the stack. Column t2​ contains the address of the row containing the value that overflowed the stack right before the value in the current row. For example, in the picture above, first value a overflowed the stack, then b overflowed the stack, and then value c overflowed the stack. Thus, row with value b points back to the row with value a, and row with value c points back to the row with value b. To reduce a table row to a single value, we'll compute a randomized product of column values as follows: ri​=α0​+α1​⋅t0,i​+α2​⋅t1,i​+α3​⋅t2,i​ Then, when row i is added to the table, we'll update the value in the p1​ column like so: p1′​=p1​⋅ri​ Analogously, when row i is removed from the table, we'll update the value in column p1​ like so: p1′​=ri​p1​​ The initial value of p1​ is set to 1. Thus, if by the time Miden VM finishes executing a program the table is empty (we added and then removed exactly the same set of rows), p1​ will also be equal to 1. There are a couple of other rules we'll need to enforce: We can delete a row only after the row has been inserted into the table. We can't insert a row with the same address twice into the table (even if the row was inserted and then deleted). How these are enforced will be described a bit later.","breadcrumbs":"Design » Operand stack » Overflow table","id":"138","title":"Overflow table"},"139":{"body":"If an operation adds data to the stack, we say that the operation caused a right shift. For example, PUSH and DUP operations cause a right shift. Graphically, this looks like so: Here, we pushed value v17​ onto the stack. All other values on the stack are shifted by one slot to the right and the stack depth increases by 1. There is not enough space at the top of the stack for all 17 values, thus, v1​ needs to be moved to the overflow table. To do this, we need to rely on another column: k0​. This is a system column which keeps track of the current VM cycle. The value in this column is simply incremented by 1 with every step. The row we want to add to the overflow table is defined by tuple (clk,v1,0), and after it is added, the table would look like so: The reason we use VM clock cycle as row address is that the clock cycle is guaranteed to be unique, and thus, the same row can not be added to the table twice. Let's push another item onto the stack: Again, as we push v18​ onto the stack, all items on the stack are shifted to the right, and now v2​ needs to be moved to the overflow table. The tuple we want to insert into the table now is (clk+1,v2,clk). After the operation, the overflow table will look like so: Notice that t2​ for row which contains value v2​ points back to the row with address clk. Overall, during a right shift we do the following: Increment stack depth by 1. Shift stack columns s0​,...,s14​ right by 1 slot. Add a row to the overflow table described by tuple (k0​,s15​,b0​). Set the next value of b1​ to the current value of k0​. Also, as mentioned previously, the prover sets values in h0​ non-deterministically to b0​−161​.","breadcrumbs":"Design » Operand stack » Right shift","id":"139","title":"Right shift"},"14":{"body":"Internally, Miden VM uses rayon for parallel computations. To control the number of threads used to generate a STARK proof, you can use RAYON_NUM_THREADS environment variable.","breadcrumbs":"Introduction » Usage » Controlling parallelism","id":"14","title":"Controlling parallelism"},"140":{"body":"If an operation removes an item from the stack, we say that the operation caused a left shift. For example, a DROP operation causes a left shift. Assuming the stack is in the state we left it at the end of the previous section, graphically, this looks like so: Overall, during the left shift we do the following: When stack depth is greater than 16: Decrement stack depth by 1. Shift stack columns s1​,...,s15​ left by 1 slot. Remove a row from the overflow table with t0​ equal to the current value of b1​. Set the next value of s15​ to the value in t1​ of the removed overflow table row. Set the next value of b1​ to the value in t2​ of the removed overflow table row. When the stack depth is equal to 16: Keep the stack depth the same. Shift stack columns s1​,...,s15​ left by 1 slot. Set the value of s15​ to 0. Set the value to h0​ to 0 (or any other value). If the stack depth becomes (or remains) 16, the prover can set h0​ to any value (e.g., 0). But if the depth is greater than 16 the prover sets h0​ to b0​−161​.","breadcrumbs":"Design » Operand stack » Left shift","id":"140","title":"Left shift"},"141":{"body":"To simplify constraint descriptions, we'll assume that the VM exposes two binary flag values described below. Flag Degree Description fshr​ 6 When this flag is set to 1, the instruction executing on the VM is performing a \"right shift\". fshl​ 5 When this flag is set to 1, the instruction executing on the VM is performing a \"left shift\". These flags are mutually exclusive. That is, if fshl​=1, then fshr​=0 and vice versa. However, both flags can be set to 0 simultaneously. This happens when the executed instruction does not shift the stack. How these flags are computed is described here .","breadcrumbs":"Design » Operand stack » AIR Constraints","id":"141","title":"AIR Constraints"},"142":{"body":"Additionally, we'll define a flag to indicate whether the overflow table contains values. This flag will be set to 0 when the overflow table is empty, and to 1 otherwise (i.e., when stack depth >16). This flag can be computed as follows: fov​=(b0​−16)⋅h0​ | degree=2 To ensure that this flag is set correctly, we need to impose the following constraint: (1−fov​)⋅(b0​−16)=0 | degree=3 The above constraint can be satisfied only when either of the following holds: b0​=16, in which case fov​ evaluates to 0, regardless of the value of h0​. fov​=1, in which case b0​ cannot be equal to 16 (and h0​ must be set to b0​−161​).","breadcrumbs":"Design » Operand stack » Stack overflow flag","id":"142","title":"Stack overflow flag"},"143":{"body":"To make sure stack depth column b0​ is updated correctly, we need to impose the following constraints: Condition Constraint__ Description fshr​=1 b0′​=b0​+1 When the stack is shifted to the right, stack depth should be incremented by 1. fshl​=1 fov​=1 b0′​=b0​−1 When the stack is shifted to the left and the overflow table is not empty, stack depth should be decremented by 1. otherwise b0′​=b0​ In all other cases, stack depth should not change. We can combine the above constraints into a single expression as follows: b0′​−b0​+fshl​⋅fov​−fshr​=0 | degree=7","breadcrumbs":"Design » Operand stack » Stack depth constraints","id":"143","title":"Stack depth constraints"},"144":{"body":"When the stack is shifted to the right, a tuple (k0​,s15​,b1​) should be added to the overflow table. We will denote value of the row to be added to the table as follows: v=α0​+α1​⋅k0​+α2​⋅s15​+α3​⋅b1​ When the stack is shifted to the left, a tuple (b1​,s15′​,b1′​) should be removed from the overflow table. We will denote value of the row to be removed from the table as follows. u=α0​+α1​⋅b1​+α2​⋅s15′​+α3​⋅b1′​ Using the above variables, we can ensure that right and left shifts update the overflow table correctly by enforcing the following constraint: p1′​⋅(u⋅fshl​⋅fov​+1−fshl​⋅fov​)=p1​⋅(v⋅fshr​+1−fshr​) | degree=9 The above constraint reduces to the following under various flag conditions: Condition Applied constraint fshl​=1, fshr​=0, fov​=0 p1′​=p1​ fshl​=1, fshr​=0, fov​=1 p1′​⋅u=p1​ fshl​=0, fshr​=1, fov​=1 or 0 p1′​=p1​⋅v fshl​=0, fshr​=0, fov​=1 or 0 p1′​=p1​ Notice that in the case of the left shift, the constraint forces the prover to set the next values of s15​ and b1​ to values t1​ and t2​ 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 b1​ is set to the current value of k0​. This can be done with the following constraint: fshr​⋅(b1′​−k0​)=0 | 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., s15​ is set to 0). This can be done with the following constraint: fshl​⋅(1−fov​)⋅s15′​=0 | degree=8","breadcrumbs":"Design » Operand stack » Overflow table constraints","id":"144","title":"Overflow table constraints"},"145":{"body":"In addition to the constraints described above, we also need to enforce the following boundary constraints: b0​=16 at the first and at the last row of execution trace. b1​=0 at the first and at the last row of execution trace. p1​=1 at the first and at the last row of execution trace.","breadcrumbs":"Design » Operand stack » Boundary constraints","id":"145","title":"Boundary constraints"},"146":{"body":"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 fopname​. For example, fdup​ would be set to 1 when DUP operation is executed, and to 0 otherwise. Operation flags are discussed in detail in the section below . 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: fdup​⋅(s0′​−s0​)=0fdup​⋅(si+1′​−si​)=0 for i∈[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: fdup1​⋅(s0′​−s1​)=0fdup1​⋅(si+1′​−si​)=0 for i∈[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).","breadcrumbs":"Design » Operand stack » Operation constraints » Stack operation constraints","id":"146","title":"Stack operation constraints"},"147":{"body":"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 . 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 b0​,...,b6​. 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 b6​ to b0​. For example, the value of the flag for NOOP, which is encoded as 0000000, is computed as follows: fnoop​=(1−b6​)⋅(1−b5​)⋅(1−b4​)⋅(1−b3​)⋅(1−b2​)⋅(1−b1​)⋅(1−b0​) While the value of the DROP operation, which is encoded as 0101001 is computed as follows: fdrop​=(1−b6​)⋅b5​⋅(1−b4​)⋅b3​⋅(1−b2​)⋅(1−b1​)⋅b0​ 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 e0​ and e1​ for degree reduction: b6​ b5​ b4​ b3​ b2​ b1​ b0​ e0​ e1​ # 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 e0​ (which is set to b6​⋅(1−b5​)⋅b4​) 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 e1​ (which is set to b6​⋅b5​) 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.","breadcrumbs":"Design » Operand stack » Operation constraints » Operation flags","id":"147","title":"Operation flags"},"148":{"body":"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 7 EQZ 1 000_0001 Field ops 7 NEG 2 000_0010 Field ops 7 INV 3 000_0011 Field ops 7 INCR 4 000_0100 Field ops 7 NOT 5 000_0101 Field ops 7 FMPADD 6 000_0110 System ops 7 MLOAD 7 000_0111 I/O ops 7 SWAP 8 000_1000 Stack ops 7 CALLER 9 000_1001 System ops 7 MOVUP2 10 000_1010 Stack ops 7 MOVDN2 11 000_1011 Stack ops 7 MOVUP3 12 000_1100 Stack ops 7 MOVDN3 13 000_1101 Stack ops 7 ADVPOPW 14 000_1110 I/O ops 7 EXPACC 15 000_1111 Field ops 7 MOVUP4 16 001_0000 Stack ops 7 MOVDN4 17 001_0001 Stack ops 7 MOVUP5 18 001_0010 Stack ops 7 MOVDN5 19 001_0011 Stack ops 7 MOVUP6 20 001_0100 Stack ops 7 MOVDN6 21 001_0101 Stack ops 7 MOVUP7 22 001_0110 Stack ops 7 MOVDN7 23 001_0111 Stack ops 7 SWAPW 24 001_1000 Stack ops 7 EXT2MUL 25 001_1001 Field ops 7 MOVUP8 26 001_1010 Stack ops 7 MOVDN8 27 001_1011 Stack ops 7 SWAPW2 28 001_1100 Stack ops 7 SWAPW3 29 001_1101 Stack ops 7 SWAPDW 30 001_1110 Stack ops 7  31 001_1111 7","breadcrumbs":"Design » Operand stack » Operation constraints » No stack shift operations","id":"148","title":"No stack shift operations"},"149":{"body":"This group contains 16 operations which shift the stack to the left (i.e., remove an item from the stack). Most of left-shift operations are contained in this group. 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 ASSERT 32 010_0000 System ops 7 EQ 33 010_0001 Field ops 7 ADD 34 010_0010 Field ops 7 MUL 35 010_0011 Field ops 7 AND 36 010_0100 Field ops 7 OR 37 010_0101 Field ops 7 U32AND 38 010_0110 u32 ops 7 U32XOR 39 010_0111 u32 ops 7 FRIE2F4 40 010_1000 Crypto ops 7 DROP 41 010_1001 Stack ops 7 CSWAP 42 010_1010 Stack ops 7 CSWAPW 43 010_1011 Stack ops 7 MLOADW 44 010_1100 I/O ops 7 MSTORE 45 010_1101 I/O ops 7 MSTOREW 46 010_1110 I/O ops 7 FMPUPDATE 47 010_1111 System ops 7","breadcrumbs":"Design » Operand stack » Operation constraints » Left stack shift operations","id":"149","title":"Left stack shift operations"},"15":{"body":"Miden VM proof generation can be accelerated via GPUs. Currently, GPU acceleration is enabled only on Apple silicon hardware (via Metal ). To compile Miden VM with Metal acceleration enabled, you can run the following command: make exec-metal Similar to make exec command, this will place the resulting miden executable into the ./target/optimized directory. Currently, GPU acceleration is applicable only to recursive proofs which can be generated using the -r flag.","breadcrumbs":"Introduction » Usage » GPU acceleration","id":"15","title":"GPU acceleration"},"150":{"body":"This group contains 16 operations which shift the stack to the right (i.e., push a new item onto the stack). Most of right-shift operations are contained in this group. 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 PAD 48 011_0000 Stack ops 7 DUP 49 011_0001 Stack ops 7 DUP1 50 011_0010 Stack ops 7 DUP2 51 011_0011 Stack ops 7 DUP3 52 011_0100 Stack ops 7 DUP4 53 011_0101 Stack ops 7 DUP5 54 011_0110 Stack ops 7 DUP6 55 011_0111 Stack ops 7 DUP7 56 011_1000 Stack ops 7 DUP9 57 011_1001 Stack ops 7 DUP11 58 011_1010 Stack ops 7 DUP13 59 011_1011 Stack ops 7 DUP15 60 011_1100 Stack ops 7 ADVPOP 61 011_1101 I/O ops 7 SDEPTH 62 011_1110 I/O ops 7 CLK 63 011_1111 System ops 7","breadcrumbs":"Design » Operand stack » Operation constraints » Right stack shift operations","id":"150","title":"Right stack shift operations"},"151":{"body":"This group contains 8 u32 operations. These operations are grouped together because all of them require range checks. The constraints for range checks are of degree 5, however, since all these operations require them, we can define a flag with common prefix 100 to serve as a selector for the range check constraints. The value of this flag is computed as follows: fu32rc​=b6​⋅(1−b5​)⋅(1−b4​) The degree of this flag is 3, which is acceptable for a selector for degree 5 constraints. Operation Opcode value Binary encoding Operation group Flag degree U32ADD 64 100_0000 u32 ops 6 U32SUB 66 100_0010 u32 ops 6 U32MUL 68 100_0100 u32 ops 6 U32DIV 70 100_0110 u32 ops 6 U32SPLIT 72 100_1000 u32 ops 6 U32ASSERT2 74 100_1010 u32 ops 6 U32ADD3 76 100_1100 u32 ops 6 U32MADD 78 100_1110 u32 ops 6 As mentioned previously, the last bit of the opcode is not used in computation of the flag for these operations. We force this bit to always be set to 0 with the following constraint: b6​⋅(1−b5​)⋅(1−b4​)⋅b0​=0 | degree=4 Putting these operations into a group with flag degree 6 is important for two other reasons: Constraints for the U32SPLIT operation have degree 3. Thus, the degree of the op flag for this operation cannot exceed 6. Operations U32ADD3 and U32MADD shift the stack to the left. Thus, having these two operations in this group and putting them under the common prefix 10011 allows us to create a common flag for these operations of degree 5 (recall that the left-shift flag cannot exceed degree 5).","breadcrumbs":"Design » Operand stack » Operation constraints » u32 operations","id":"151","title":"u32 operations"},"152":{"body":"This group contains operations which require constraints with degree up to 3. All 7 operation bits are used for these flags. The extra e0​ column is used for degree reduction of the three high-degree bits. Operation Opcode value Binary encoding Operation group Flag degree HPERM 80 101_0000 Crypto ops 5 MPVERIFY 81 101_0001 Crypto ops 5 PIPE 82 101_0010 I/O ops 5 MSTREAM 83 101_0011 I/O ops 5 SPLIT 84 101_0100 Flow control ops 5 LOOP 85 101_0101 Flow control ops 5 SPAN 86 101_0110 Flow control ops 5 JOIN 87 101_0111 Flow control ops 5 DYN 88 101_1000 Flow control ops 5  89 101_1001 5  90 101_1010 5  91 101_1011 5  92 101_1100 5  93 101_1101 5  94 101_1110 5  95 101_1111 5 Note that the SPLIT and LOOP operations are grouped together under the common prefix 101010, and thus can have a common flag of degree 4 (using e0​ for degree reduction). This is important because both of these operations shift the stack to the left. Also, we need to make sure that extra register e0​, which is used to reduce the flag degree by 2, is set to 1 when b6​=1, b5​=0, and b4​=1: e0​−b6​⋅(1−b5​)⋅b4​=0 | degree=3","breadcrumbs":"Design » Operand stack » Operation constraints » High-degree operations","id":"152","title":"High-degree operations"},"153":{"body":"This group contains operations which require constraints with degree up to 5. Operation Opcode value Binary encoding Operation group Flag degree MRUPDATE 96 110_0000 Crypto ops 4 PUSH 100 110_0100 I/O ops 4 SYSCALL 104 110_1000 Flow control ops 4 CALL 108 110_1100 Flow control ops 4 END 112 111_0000 Flow control ops 4 REPEAT 116 111_0100 Flow control ops 4 RESPAN 120 111_1000 Flow control ops 4 HALT 124 111_1100 Flow control ops 4 As mentioned previously, the last two bits of the opcode are not used in computation of the flag for these operations. We force these bits to always be set to 0 with the following constraints: b6​⋅b5​⋅b0​=0 | degree=3 b6​⋅b5​⋅b1​=0 | degree=3 Also, we need to make sure that extra register e1​, which is used to reduce the flag degree by 1, is set to 1 when both b6​ and b5​ columns are set to 1: e1​−b6​⋅b5​=0 | degree=2","breadcrumbs":"Design » Operand stack » Operation constraints » Very high-degree operations","id":"153","title":"Very high-degree operations"},"154":{"body":"Using the operation flags defined above, we can compute several composite flags which are used by various constraints in the VM.","breadcrumbs":"Design » Operand stack » Operation constraints » Composite flags","id":"154","title":"Composite flags"},"155":{"body":"The right-shift flag indicates that an operation shifts the stack to the right. This flag is computed as follows: fshr​=(1−b6​)⋅b5​⋅b4​+fu32split​+fpush​ | degree=6 In the above, (1−b6​)⋅b5​⋅b4​ evaluates to 1 for all right stack shift operations described previously. This works because all these operations have a common prefix 011. We also need to add in flags for other operations which shift the stack to the right but are not a part of the above group (e.g., PUSH operation).","breadcrumbs":"Design » Operand stack » Operation constraints » Shift right flag","id":"155","title":"Shift right flag"},"156":{"body":"The left-shift flag indicates that a given operation shifts the stack to the left. To simplify the description of this flag, we will first compute the following intermediate variables: A flag which is set to 1 when fu32add3​=1 or fu32madd​=1: fadd3_madd​=b6​⋅(1−b5​)⋅(1−b4​)⋅b3​⋅b2​ | degree=5 A flag which is set to 1 when fsplit​=1 or floop​=1: fsplit_loop​=e0​⋅(1−b3​)⋅b2​⋅(1−b1​) | degree=4 Using the above variables, we compute left-shift flag as follows: fshl​=(1−b6​)⋅b5​⋅(1−b4​)+fadd3_madd​+fsplit_loop​+frepeat​+fend​⋅h5​ | degree=5 In the above: (1−b6​)⋅b5​⋅(1−b4​) evaluates to 1 for all left stack shift operations described previously. This works because all these operations have a common prefix 010. h5​ is the helper register in the decoder which is set to 1 when we are exiting a LOOP block, and to 0 otherwise. Thus, similarly to the right-shift flag, we compute the value of the left-shift flag based on the prefix of the operation group which contains most left shift operations, and add in flag values for other operations which shift the stack to the left but are not a part of this group.","breadcrumbs":"Design » Operand stack » Operation constraints » Shift left flag","id":"156","title":"Shift left flag"},"157":{"body":"The control flow flag fctrl​ is set to 1 when a control flow operation is being executed by the VM, and to 0 otherwise. Naively, this flag can be computed as follows: fctrl​=fjoin​+fsplit​+floop​+frepeat​+fspan​+frespan​+fcall​+fsyscall​+fend​+fhalt​ | degree=6 However, this can be computed more efficiently via the common operation prefixes for the two groups of control flow operations as follows. fspan,join,split,loop​=e0​⋅(1−b3​)⋅b2​ | degree=3 fend,repeat,respan,halt​=e1​⋅b4​ | degree=2 fctrl​=fspan,join,split,loop​+fend,repeat,respan,halt​+fdyn​+fcall​+fsyscall​ | degree=5","breadcrumbs":"Design » Operand stack » Operation constraints » Control flow flag","id":"157","title":"Control flow flag"},"158":{"body":"In this section we describe the AIR constraints for Miden VM system operations.","breadcrumbs":"Design » Operand stack » System operations » System Operations","id":"158","title":"System Operations"},"159":{"body":"The NOOP operation advances the cycle counter but does not change the state of the operand stack (i.e., the depth of the stack and the values on the stack remain the same). The NOOP operation does not impose any constraints besides the ones needed to ensure that the entire state of the stack is copied over. This constraint looks like so: si′​−si​=0 for i∈[0,16) | degree=1","breadcrumbs":"Design » Operand stack » System operations » NOOP","id":"159","title":"NOOP"},"16":{"body":"Miden VM execution and proof generation can be accelerated via vectorized instructions. Currently, SIMD acceleration can be enabled only on platforms supporting SVE instructions (e.g., Graviton 3). To compile Miden VM with SVE acceleration enabled, you can run the following command: make exec-graviton This will place the resulting miden executable into the ./target/optimized directory. Similar to Metal acceleration, SVE acceleration is currently applicable only to recursive proofs which can be generated using the -r flag.","breadcrumbs":"Introduction » Usage » SIMD acceleration","id":"16","title":"SIMD acceleration"},"160":{"body":"The ASSERT operation pops an element off the stack and checks if the popped element is equal to 1. If the element is not equal to 1, program execution fails. assert Stack transition for this operation must satisfy the following constraints: s0​−1=0 | degree=1 The effect on the rest of the stack is: Left shift starting from position 1.","breadcrumbs":"Design » Operand stack » System operations » ASSERT","id":"160","title":"ASSERT"},"161":{"body":"The FMPADD operation pops an element off the stack, adds the current value of the fmp register to it, and pushes the result back onto the stack. The diagram below illustrates this graphically. fmpadd Stack transition for this operation must satisfy the following constraints: s0′​−(s0​+fmp)=0 | degree=1 The effect on the rest of the stack is: No change starting from position 1.","breadcrumbs":"Design » Operand stack » System operations » FMPADD","id":"161","title":"FMPADD"},"162":{"body":"The FMPUPDATE operation pops an element off the stack and adds it to the current value of the fmp register. The diagram below illustrates this graphically. fmpupdate The stack transition for this operation must follow the following constraint: fmp′−(fmp+s0​)=0 | degree=1 The effect on the rest of the stack is: Left shift starting from position 1.","breadcrumbs":"Design » Operand stack » System operations » FMPUPDATE","id":"162","title":"FMPUPDATE"},"163":{"body":"The CLK operation pushes the current value of the clock cycle onto the stack. The diagram below illustrates this graphically. clk The stack transition for this operation must follow the following constraint: s0′​−clk=0 | degree=1 The effect on the rest of the stack is: Right shift starting from position 0.","breadcrumbs":"Design » Operand stack » System operations » CLK","id":"163","title":"CLK"},"164":{"body":"In this section we describe the AIR constraints for Miden VM field operations (i.e., arithmetic operations over field elements).","breadcrumbs":"Design » Operand stack » Field operations » Field Operations","id":"164","title":"Field Operations"},"165":{"body":"Assume a and b are the elements at the top of the stack. The ADD operation computes c←(a+b). The diagram below illustrates this graphically. add Stack transition for this operation must satisfy the following constraints: s0′​−(s0​+s1​)=0 | degree=1 The effect on the rest of the stack is: Left shift starting from position 2.","breadcrumbs":"Design » Operand stack » Field operations » ADD","id":"165","title":"ADD"},"166":{"body":"Assume a is the element at the top of the stack. The NEG operation computes b←(−a). The diagram below illustrates this graphically. neg Stack transition for this operation must satisfy the following constraints: s0′​+s0​=0 | degree=1 The effect on the rest of the stack is: No change starting from position 1.","breadcrumbs":"Design » Operand stack » Field operations » NEG","id":"166","title":"NEG"},"167":{"body":"Assume a and b are the elements at the top of the stack. The MUL operation computes c←(a⋅b). The diagram below illustrates this graphically. mul Stack transition for this operation must satisfy the following constraints: s0′​−s0​⋅s1​=0 | degree=2 The effect on the rest of the stack is: Left shift starting from position 2.","breadcrumbs":"Design » Operand stack » Field operations » MUL","id":"167","title":"MUL"},"168":{"body":"Assume a is the element at the top of the stack. The INV operation computes b←(a−1). The diagram below illustrates this graphically. inv Stack transition for this operation must satisfy the following constraints: 1−s0′​⋅s0​=0 | degree=2 Note that the above constraint can be satisfied only if the value in s0​=0. The effect on the rest of the stack is: No change starting from position 1.","breadcrumbs":"Design » Operand stack » Field operations » INV","id":"168","title":"INV"},"169":{"body":"Assume a is the element at the top of the stack. The INCR operation computes b←(a+1). The diagram below illustrates this graphically. incr Stack transition for this operation must satisfy the following constraints: s0′​−(s0​+1)=0 | degree=1 The effect on the rest of the stack is: No change starting from position 1.","breadcrumbs":"Design » Operand stack » Field operations » INCR","id":"169","title":"INCR"},"17":{"body":"Once the executable has been compiled, you can run Miden VM like so: ./target/optimized/miden [subcommand] [parameters] Currently, Miden VM can be executed with the following subcommands: run - this will execute a Miden assembly program and output the result, but will not generate a proof of execution. prove - this will execute a Miden assembly program, and will also generate a STARK proof of execution. verify - this will verify a previously generated proof of execution for a given program. compile - this will compile a Miden assembly program (i.e., build a program MAST ) and outputs stats about the compilation process. debug - this will instantiate a Miden debugger against the specified Miden assembly program and inputs. analyze - this will run a Miden assembly program against specific inputs and will output stats about its execution. repl - this will initiate the Miden REPL tool. All of the above subcommands require various parameters to be provided. To get more detailed help on what is needed for a given subcommand, you can run the following: ./target/optimized/miden [subcommand] --help For example: ./target/optimized/miden prove --help To execute a program using the Miden VM there needs to be a .masm file containing the Miden Assembly code and a .inputs file containing the inputs.","breadcrumbs":"Introduction » Usage » Running Miden VM","id":"17","title":"Running Miden VM"},"170":{"body":"Assume a is a binary value at the top of the stack. The NOT operation computes b←(¬a). The diagram below illustrates this graphically. not Stack transition for this operation must satisfy the following constraints: s02​−s0​=0 | degree=2 s0′​−(1−s0​)=0 | degree=1 The first constraint ensures that the value in s0​ is binary, and the second constraint ensures the correctness of the boolean NOT operation. The effect on the rest of the stack is: No change starting from position 1.","breadcrumbs":"Design » Operand stack » Field operations » NOT","id":"170","title":"NOT"},"171":{"body":"Assume a and b are binary values at the top of the stack. The AND operation computes c←(a∧b). The diagram below illustrates this graphically. and Stack transition for this operation must satisfy the following constraints: si2​−si​=0 for i∈{0,1} | degree=2 s0′​−s0​⋅s1​=0 | degree=2 The first two constraints ensure that the value in s0​ and s1​ are binary, and the third constraint ensures the correctness of the boolean AND operation. The effect on the rest of the stack is: Left shift starting from position 2.","breadcrumbs":"Design » Operand stack » Field operations » AND","id":"171","title":"AND"},"172":{"body":"Assume a and b are binary values at the top of the stack. The OR operation computes c←(a∨b) The diagram below illustrates this graphically. or Stack transition for this operation must satisfy the following constraints: si2​−si​=0 for i∈{0,1} | degree=2 s0′​−(s1​+s0​−s1​⋅s0​)=0 | degree=2 The first two constraints ensure that the value in s0​ and s1​ are binary, and the third constraint ensures the correctness of the boolean OR operation. The effect on the rest of the stack is: Left shift starting from position 2.","breadcrumbs":"Design » Operand stack » Field operations » OR","id":"172","title":"OR"},"173":{"body":"Assume a and b are the elements at the top of the stack. The EQ operation computes c such that c=1 if a=b, and 0 otherwise. The diagram below illustrates this graphically. eq Stack transition for this operation must satisfy the following constraints: s0′​⋅(s0​−s1​)=0 | degree=2 s0′​−(1−(s0​−s1​)⋅h0​)=0 | degree=2 To satisfy the above constraints, the prover must populate the value of helper register h0​ as follows: If s0​=s1​, set h0​=s0​−s1​1​. Otherwise, set h0​ to any value (e.g., 0). The effect on the rest of the stack is: Left shift starting from position 2.","breadcrumbs":"Design » Operand stack » Field operations » EQ","id":"173","title":"EQ"},"174":{"body":"Assume a is the element at the top of the stack. The EQZ operation computes b such that b=1 if a=0, and 0 otherwise. The diagram below illustrates this graphically. eqz Stack transition for this operation must satisfy the following constraints: s0′​⋅s0​=0 | degree=2 s0′​−(1−s0​⋅h0​)=0 | degree=2 To satisfy the above constraints, the prover must populate the value of helper register h0​ as follows: If s0​=0, set h0​=s0​1​. Otherwise, set h0​ to any value (e.g., 0). The effect on the rest of the stack is: No change starting from position 1.","breadcrumbs":"Design » Operand stack » Field operations » EQZ","id":"174","title":"EQZ"},"175":{"body":"The EXPACC operation pops top 4 elements from the top of the stack, performs a single round of exponent aggregation, and pushes the resulting 4 values onto the stack. The diagram below illustrates this graphically. expacc Stack transition for this operation must satisfy the following constraints: bit should be a binary. s0′2​−s0′​=0 | degree=2 The exp in the next frame should be the square of the exp in the current frame. s1′​−s12​=0 | degree=2 The value val in the helper register is computed correctly using the bit and exp in next and current frame respectively. h0​−((s1​−1)∗s0′​+1)=0 | degree=2 The acc in the next frame is the product of val and acc in the current frame. s2′​−s2​∗h0​=0 | degree=2 b in the next frame is the right shift of b in the current frame. s3′​−(s3​∗2+s0′​)=0 | degree=1 The effect on the rest of the stack is: No change starting from position 4.","breadcrumbs":"Design » Operand stack » Field operations » EXPACC","id":"175","title":"EXPACC"},"176":{"body":"The EXT2MUL operation pops top 4 values from the top of the stack, performs mulitplication between the two extension field elements, and pushes the resulting 4 values onto the stack. The diagram below illustrates this graphically. ext2mul Stack transition for this operation must satisfy the following constraints: The first stack element should be unchanged in the next frame. s0′​−s0​=0 | degree=1 The second stack element should be unchanged in the next frame. s1′​−s1​=0 | degree=1 The third stack element should satisfy the following constraint. s2′​−(s0​+s1​)⋅(s2​+s3​)+s0​⋅s2​=0 | degree=2 The fourth stack element should satisfy the following constraint. s3′​−s1​⋅s3​+2⋅s0​⋅s2​=0 | degree=2 The effect on the rest of the stack is: No change starting from position 4.","breadcrumbs":"Design » Operand stack » Field operations » EXT2MUL","id":"176","title":"EXT2MUL"},"177":{"body":"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.","breadcrumbs":"Design » Operand stack » u32 operations » u32 Operations","id":"177","title":"u32 Operations"},"178":{"body":"Most operations described below require some number of 16-bit range checks (i.e., verifying that the value of a field element is smaller than 216). The number of required range checks varies between 2 and 4, depending on the operation. However, to simplify the constraint system, we force each relevant operation to consume exactly 4 range checks. To perform these range checks, the prover puts the values to be range-checked into helper registers h0​,...,h3​, and then updates the range checker bus column brange​ according to the LogUp construction described in the range checker documentation, using multiplicity 1 for each value. This operation is enforced via the following constraint. Note that since constraints cannot include divisions, the actual constraint which is enforced will be expressed equivalently with all denominators multiplied through, resulting in a constraint of degree 5. brange′​=brange​−(α−h0​)1​−(α−h1​)1​−(α−h2​)1​−(α−h3​)1​ | degree=5 The above is just a partial constraint as it does not show the range checker's part of the constraint, which adds the required values into the bus column. It also omits the selector flag which is used to turn this constraint on only when executing relevant operations.","breadcrumbs":"Design » Operand stack » u32 operations » Range checks","id":"178","title":"Range checks"},"179":{"body":"Another primitive which is required by most of the operations described below is checking whether four 16-bit values form a valid field element. Assume t0​, t1​, t2​, and t3​ are known to be 16-bit values, and we want to verify that 248⋅t3​+232⋅t2​+216⋅t1​+t0​ is a valid field element. For simplicity, let's denote: vhi​=216⋅t3​+t2​vlo​=216⋅t1​+t0​ We can then impose the following constraint to verify element validity: (1−m⋅(232−1−vhi​))⋅vlo​=0 | degree=3 Where m is a value set non-deterministically by the prover. The above constraint should hold only if either of the following hold: vlo​=0 vhi​=232−1 To satisfy the latter equation, the prover needs to set m=(232−1−vhi​)−1, which is possible only when vhi​=232−1. This constraint is sufficient because modulus 264−232+1 in binary representation is 32 ones, followed by 31 zeros, followed by a single one: 1111111111111111111111111111111100000000000000000000000000000001 This implies that the largest possible 64-bit value encoding a valid field element would be 32 ones, followed by 32 zeros: 1111111111111111111111111111111100000000000000000000000000000000 Thus, for a 64-bit value to encode a valid field element, either the lower 32 bits must be all zeros, or the upper 32 bits must not be all ones (which is 232−1).","breadcrumbs":"Design » Operand stack » u32 operations » Checking element validity","id":"179","title":"Checking element validity"},"18":{"body":"As described here the Miden VM can consume public and secret inputs. Public inputs: operand_stack - can be supplied to the VM to initialize the stack with the desired values before a program starts executing. There is no limit on the number of stack inputs that can be initialized in this way, although increasing the number of public inputs increases the cost to the verifier. Secret (or nondeterministic) inputs: advice_stack - can be supplied to the VM. There is no limit on how much data the advice provider can hold. This is provided as a string array where each string entry represents a field element. advice_map - is supplied as a map of 64-character hex keys, each mapped to an array of numbers. The hex keys are interpreted as 4 field elements and the arrays of numbers are interpreted as arrays of field elements. merkle_store - the Merkle store is container that allows the user to define merkle_tree, sparse_merkle_tree and partial_merkle_tree data structures. merkle_tree - is supplied as an array of 64-character hex values where each value represents a leaf (4 elements) in the tree. sparse_merkle_tree - is supplied as an array of tuples of the form (number, 64-character hex string). The number represents the leaf index and the hex string represents the leaf value (4 elements). partial_merkle_tree - is supplied as an array of tuples of the form ((number, number), 64-character hex string). The internal tuple represents the leaf depth and index at this depth, and the hex string represents the leaf value (4 elements). Check out the comparison example to see how secret inputs work. After a program finishes executing, the elements that remain on the stack become the outputs of the program, along with the overflow addresses (overflow_addrs) that are required to reconstruct the stack overflow table .","breadcrumbs":"Introduction » Usage » Inputs","id":"18","title":"Inputs"},"180":{"body":"Assume a is the element at the top of the stack. The U32SPLIT operation computes (b,c)←a, where b contains the lower 32 bits of a, and c contains the upper 32 bits of a. The diagram below illustrates this graphically. u32split To facilitate this operation, the prover sets values in h0​,...,h3​ to 16-bit limbs of a with h0​ being the least significant limb. Thus, stack transition for this operation must satisfy the following constraints: s0​=248⋅h3​+232⋅h2​+216⋅h1​+h0​ | degree=1 s1′​=216⋅h1​+h0​ | degree=1 s0′​=216⋅h3​+h2​ | degree=1 In addition to the above constraints, we also need to verify that values in h0​,...,h3​ are smaller than 216, which we can do using 16-bit range checks as described previously . Also, we need to make sure that values in h0​,...,h3​, when combined, form a valid field element, which we can do by putting a nondeterministic value m into helper register h4​ and using the technique described here . The effect of this operation on the rest of the stack is: Right shift starting from position 1.","breadcrumbs":"Design » Operand stack » u32 operations » U32SPLIT","id":"180","title":"U32SPLIT"},"181":{"body":"Assume a and b are the elements at the top of the stack. The U32ASSERT2 verifies that both a and b are smaller than 232. The diagram below illustrates this graphically. u32assert2 To facilitate this operation, the prover sets values in h0​ and h1​ to low and high 16-bit limbs of a, and values in h2​ and h3​ to to low and high 16-bit limbs of b. Thus, stack transition for this operation must satisfy the following constraints: s0′​=216⋅h3​+h2​ | degree=1 s1′​=216⋅h1​+h0​ | degree=1 In addition to the above constraints, we also need to verify that values in h0​,...,h3​ are smaller than 216, which we can do using 16-bit range checks as described previously . The effect of this operation on the rest of the stack is: No change starting from position 0 - i.e., the state of the stack does not change.","breadcrumbs":"Design » Operand stack » u32 operations » U32ASSERT2","id":"181","title":"U32ASSERT2"},"182":{"body":"Assume a and b are the values at the top of the stack which are known to be smaller than 232. The U32ADD operation computes (c,d)←a+b, where c contains the low 32-bits of the result, and d is the carry bit. The diagram below illustrates this graphically. u32add To facilitate this operation, the prover sets values in h0​, h1​, and h2​ to 16-bit limbs of a+b with h0​ being the least significant limb. Value in h3​ is set to 0. Thus, stack transition for this operation must satisfy the following constraints: s0​+s1​=232⋅h2​+216⋅h1​+h0​ | degree=1 s0′​=h2​ | degree=1 s1′​=216⋅h1​+h0​ | degree=1 In addition to the above constraints, we also need to verify that values in h0​,...,h3​ are smaller than 216, which we can do using 16-bit range checks as described previously . The effect of this operation on the rest of the stack is: No change starting from position 2.","breadcrumbs":"Design » Operand stack » u32 operations » U32ADD","id":"182","title":"U32ADD"},"183":{"body":"Assume a, b, c are the values at the top of the stack which are known to be smaller than 232. The U32ADD3 operation computes (d,e)←a+b+c, where c and d contains the low and the high 32-bits of the result respectively. The diagram below illustrates this graphically. u32add3 To facilitate this operation, the prover sets values in h0​, h1​, and h2​ to 16-bit limbs of a+b+c with h0​ being the least significant limb. Value in h3​ is set to 0. Thus, stack transition for this operation must satisfy the following constraints: s0​+s1​+s2​=232⋅h2​+216⋅h1​+h0​ | degree=1 s0′​=h2​ | degree=1 s1′​=216⋅h1​+h0​ | degree=1 In addition to the above constraints, we also need to verify that values in h0​,...,h3​ are smaller than 216, which we can do using 16-bit range checks as described previously . The effect of this operation on the rest of the stack is: Left shift starting from position 3.","breadcrumbs":"Design » Operand stack » u32 operations » U32ADD3","id":"183","title":"U32ADD3"},"184":{"body":"Assume a and b are the values at the top of the stack which are known to be smaller than 232. The U32SUB operation computes (c,d)←a−b, where c contains the 32-bit result in two's complement, and d is the borrow bit. The diagram below illustrates this graphically. u32sub To facilitate this operation, the prover sets values in h0​ and h1​ to the low and the high 16-bit limbs of a−b respectively. Values in h2​ and h3​ are set to 0. Thus, stack transition for this operation must satisfy the following constraints: s1​=s0​+s1′​+232⋅s0′​ | degree=1 s0′2​−s0′​=0 | degree=2 s1′​=216⋅h1​+h0​ | degree=1 In addition to the above constraints, we also need to verify that values in h0​,...,h3​ are smaller than 216, which we can do using 16-bit range checks as described previously . The effect of this operation on the rest of the stack is: No change starting from position 2.","breadcrumbs":"Design » Operand stack » u32 operations » U32SUB","id":"184","title":"U32SUB"},"185":{"body":"Assume a and b are the values at the top of the stack which are known to be smaller than 232. The U32MUL operation computes (c,d)←a⋅b, where c and d contain the low and the high 32-bits of the result respectively. The diagram below illustrates this graphically. u32mul To facilitate this operation, the prover sets values in h0​,...,h3​ to 16-bit limbs of a⋅b with h0​ being the least significant limb. Thus, stack transition for this operation must satisfy the following constraints: s0​⋅s1​=248⋅h3​+232⋅h2​+216⋅h1​+h0​ | degree=2 s1′​=216⋅h1​+h0​ | degree=1 s0′​=216⋅h3​+h2​ | degree=1 In addition to the above constraints, we also need to verify that values in h0​,...,h3​ are smaller than 216, which we can do using 16-bit range checks as described previously . Also, we need to make sure that values in h0​,...,h3​, when combined, form a valid field element, which we can do by putting a nondeterministic value m into helper register h4​ and using the technique described here . The effect of this operation on the rest of the stack is: No change starting from position 2.","breadcrumbs":"Design » Operand stack » u32 operations » U32MUL","id":"185","title":"U32MUL"},"186":{"body":"Assume a, b, c are the values at the top of the stack which are known to be smaller than 232. The U32MADD operation computes (d,e)←a+b⋅c, where c and d contains the low and the high 32-bits of a+b⋅c. The diagram below illustrates this graphically. u32madd To facilitate this operation, the prover sets values in h0​,...,h3​ to 16-bit limbs of a+b⋅c with h0​ being the least significant limb. Thus, stack transition for this operation must satisfy the following constraints: s0​⋅s1​+s2​=248⋅h3​+232⋅h2​+216⋅h1​+h0​ | degree=2 s1′​=216⋅h1​+h0​ | degree=1 s0′​=216⋅h3​+h2​ | degree=1 In addition to the above constraints, we also need to verify that values in h0​,...,h3​ are smaller than 216, which we can do using 16-bit range checks as described previously . Also, we need to make sure that values in h0​,...,h3​, when combined, form a valid field element, which we can do by putting a nondeterministic value m into helper register h4​ and using the technique described here . Note : that the above constraints guarantee the correctness of the operation iff a+b⋅c cannot overflow field modules (which is the case for the field with modulus 264−232+1). The effect of this operation on the rest of the stack is: Left shift starting from position 3.","breadcrumbs":"Design » Operand stack » u32 operations » U32MADD","id":"186","title":"U32MADD"},"187":{"body":"Assume a and b are the values at the top of the stack which are known to be smaller than 232. The U32DIV operation computes (c,d)←a/b, where c contains the quotient and d contains the remainder. The diagram below illustrates this graphically. u32div To facilitate this operation, the prover sets values in h0​ and h1​ to 16-bit limbs of a−c, and values in h2​ and h3​ to 16-bit limbs of b−d−1. Thus, stack transition for this operation must satisfy the following constraints: s1​=s0​⋅s1′​+s0′​ | degree=2 s1​−s1′​=216⋅h1​+h0​ | degree=1 s0​−s0′​−1=216⋅h2​+h3​ | degree=1 The second constraint enforces that s1′​≤s1​, while the third constraint enforces that s0′​216, m<216 must hold, and for short traces m216), we can do an essentially unlimited number of arbitrary 16-bit range-checks. For short traces (25> In order to add a breakpoint, the user should insert a breakpoint instruction into the MASM file. This will generate a Noop operation that will be decorated with the debug break configuration. This is a provisory solution until the source mapping is implemented. The following example will halt on the third instruction of foo: proc.foo dup dup.2 breakpoint swap add.1\nend begin exec.foo\nend","breadcrumbs":"Development tooling » Debugger » Miden Debugger","id":"25","title":"Miden Debugger"},"250":{"body":"When describing AIR constraints, we adopt the following notation: for column x, we denote the value in the current row simply as x, and the value in the next row of the column as x′. Thus, all transition constraints described in this note work with two consecutive rows of the execution trace.","breadcrumbs":"Design » Chiplets » Hash Chiplet » AIR constraints","id":"250","title":"AIR constraints"},"251":{"body":"For selector columns, first we must ensure that only binary values are allowed in these columns. This can be done with the following constraints: s02​−s0​=0 | degree=2s12​−s1​=0 | degree=2s22​−s2​=0 | degree=2 Next, we need to make sure that unless fout​=1 or fout′​=1, the values in columns s1​ and s2​ are copied over to the next row. This can be done with the following constraints: (s1′​−s1​)⋅(1−fout′​)⋅(1−fout​)=0 | degree=7(s2′​−s2​)⋅(1−fout′​)⋅(1−fout​)=0 | degree=7 Next, we need to enforce that if any of fabp​,fmpa​,fmva​,fmua​ flags is set to 1, the next value of s0​ is 0. In all other cases, s0​ should be unconstrained. These flags will only be set for rows that are 1 less than a multiple of 8 (the last row of each cycle). This can be done with the following constraint: s0′​⋅(fabp​+fmpa​+fmva​+fmua​)=0 | degree=5 Lastly, we need to make sure that no invalid combinations of flags are allowed. This can be done with the following constraints: k0​⋅(1−s0​)⋅s1​=0 | degree=3 The above constraints enforce that on every step which is one less than a multiple of 8, if s0​=0, then s1​ must also be set to 0. Basically, if we set s0​=0, then we must make sure that either fhout​=1 or fsout​=1.","breadcrumbs":"Design » Chiplets » Hash Chiplet » Selector columns constraints","id":"251","title":"Selector columns constraints"},"252":{"body":"Node index column i is relevant only for Merkle path verification and Merkle root update computations, but to simplify the overall constraint system, the same constraints will be imposed on this column for all computations. Overall, we want values in the index column to behave as follows: When we start a new computation, we should be able to set i to an arbitrary value. When a computation is finished, value in i must be 0. When we absorb a new node into the hasher state we must shift the value in i by one bit to the right. In all other cases value in i should not change. A shift by one bit to the right can be described with the following equation: i=2⋅i′+b, where b is the value of the bit which is discarded. Thus, as long as b is a binary value, the shift to the right is performed correctly, and this can be enforced with the following constraint: b2−b=0 Since we want to enforce this constraint only when a new node is absorbed into the hasher state, we'll define a flag for when this should happen as follows: fan​=fmp​+fmv​+fmu​+fmpa​+fmva​+fmua​ And then the full constraint would looks as follows: fan​⋅(b2−b)=0 | degree=6 Next, to make sure when a computation is finished i=0, we can use the following constraint: fout​⋅i=0 | degree=4 Finally, to make sure that the value in i is copied over to the next row unless we are absorbing a new row or the computation is finished, we impose the following constraint: (1−fan​−fout​)⋅(i′−i)=0 | degree=5 To satisfy these constraints for computations not related to Merkle paths (i.e., 2-to-1 hash and liner hash of elements), we can set i=0 at the start of the computation. This guarantees that i will remain 0 until the end of the computation.","breadcrumbs":"Design » Chiplets » Hash Chiplet » Node index constraints","id":"252","title":"Node index constraints"},"253":{"body":"Hasher state columns h0​,...,h11​ should behave as follows: For the first 7 row of every 8-row cycle (i.e., when k0​=0), we need to apply Rescue Prime Optimized round constraints to the hasher state. For brevity, we omit these constraints from this note. On the 8th row of every 8-row cycle, we apply the constraints based on which transition flag is set as described in the table below. Specifically, when absorbing the next set of elements into the state during linear hash computation (i.e., fabp​=1), the first 4 elements (the capacity portion) are carried over to the next row. For j∈[0,4) this can be described as follows: fabp​⋅(hj′​−hj​)=0 | degree=5 When absorbing the next node during Merkle path computation (i.e., fmp​+fmv​+fmu​=1), the result of the previous hash (h4​,...,h7​) are copied over either to (h4′​,...,h7′​) or to (h8′​,...,h11′​) depending on the value of b, which is defined in the same way as in the previous section. For j∈[0,4) this can be described as follows: (fmp​+fmv​+fmu​)⋅((1−b)⋅(hj+4′​−hj+4​)+b⋅(hj+8′​−hj+4​))=0 | degree=6 Note, that when a computation is completed (i.e., fout​=1), the next hasher state is unconstrained.","breadcrumbs":"Design » Chiplets » Hash Chiplet » Hasher state constraints","id":"253","title":"Hasher state constraints"},"254":{"body":"In this sections we describe constraints which enforce updates for multiset check columns bchip​ and p1​. These columns can be updated only on rows which are multiples of 8 or 1 less than a multiple of 8. On all other rows the values in the columns remain the same. To simplify description of the constraints, we define the following variables. Below, we denote random values sent by the verifier after the prover commits to the main execution trace as α0​, α1​, α2​ etc. m=oplabel​+24⋅k0​+25⋅k2​vh​=α0​+α1​⋅m+α2​⋅(clk+1)+α3​⋅iva​=j=0∑3​(αj+4​⋅hj​)vb​=j=4∑7​(αj+4​⋅hj​)vc​=j=8∑11​(αj+4​⋅hj​)vd​=j=8∑11​(αj​⋅hj​) In the above: m is a transition label , composed of the operation label and the periodic columns that uniquely identify each transition function. The values in the k0​ and k2​ periodic columns are included to identify the row in the hash cycle where the operation occurs. They serve to differentiate between operations that share selectors but occur at different rows in the cycle, such as BP, which uses oplinhash​ at the first row in the cycle to initiatiate a linear hash, and ABP, which uses oplinhash​ at the last row in the cycle to absorb new elements. vh​ is a common header which is a combination of the transition label, a unique row address, and the node index. For the unique row address, the clk column from the system component is used, but we add 1, because the system's clk column starts at 0. va​, vb​, vc​ are the first, second, and third words (4 elements) of the hasher state. vd​ is the third word of the hasher state but computed using the same α values as used for the second word. This is needed for computing the value of vleaf​ below to ensure that the same α values are used for the leaf node regardless of which part of the state the node comes from. Chiplets bus constraints As described previously, the chiplets bus bchip​, implemented as a running product column, is used to tie the hash chiplet with the main VM's stack and decoder. When receiving inputs from or returning results to the stack (or decoder), the hash chiplet multiplies bchip​ by their respective values. On the other side, when sending inputs to the hash chiplet or receiving results from the chiplet, the stack (or decoder) divides bchip​ by their values. In the section below we describe only the hash chiplet side of the constraints (i.e., multiplying bchip​ by relevant values). We define the values which are to be multiplied into bchip​ for each operation as follows: When starting a new simple or linear hash computation (i.e., fbp​=1) or when returning the entire state of the hasher (fsout​=1), the entire hasher state is included into bchip​: vall​=vh​+va​+vb​+vc​ When starting a Merkle path computation (i.e., fmp​+fmv​+fmu​=1), we include the leaf of the path into bchip​. The leaf is selected from the state based on value of b (defined as in the previous section): vleaf​=vh​+(1−b)⋅vb​+b⋅vd​ When absorbing a new set of elements into the state while computing a linear hash (i.e., fabp​=1), we include deltas between the last 8 elements of the hasher state (the rate) into bchip​: vabp​=vh​+vb′​+vc′​−(vb​+vc​) When a computation is complete (i.e., fhout​=1), we include the second word of the hasher state (the result) into bchip​: vres​=vh​+vb​ Using the above values, we can describe the constraints for updating column bchip​ as follows. bchip′​=bchip​⋅((fbp​+fsout​)⋅vall​+(fmp​+fmv​+fmu​)⋅vleaf​+fabp​⋅vabp​+fhout​⋅vres​+1−(fbp​+fmp​+fmv​+fmu​+fabp​+fout​)) The above constraint reduces to the following under various flag conditions: Condition Applied constraint fbp​=1 bchip′​=bchip​⋅vall​ fsout​=1 bchip′​=bchip​⋅vall​ fmp​=1 bchip′​=bchip​⋅vleaf​ fmv​=1 bchip′​=bchip​⋅vleaf​ fmu​=1 bchip′​=bchip​⋅vleaf​ fabp​=1 bchip′​=bchip​⋅vabp​ fhout​=1 bchip′​=bchip​⋅vres​ Otherwise bchip′​=bchip​ Note that the degree of the above constraint is 7. Sibling table constraints Note: Although this table is described independently, it is implemented as part of the chiplets virtual table , which combines all virtual tables required by the any of the chiplets into a single master table. As mentioned previously, the sibling table (represented by running column p1​) is used to keep track of sibling nodes used during Merkle root update computations. For this computation, we need to enforce the following rules: When computing the old Merkle root, whenever a new sibling node is absorbed into the hasher state (i.e., fmv​+fmva​=1), an entry for this sibling should be included into p1​. When computing the new Merkle root, whenever a new sibling node is absorbed into the hasher state (i.e., fmu​+fmua​=1), the entry for this sibling should be removed from p1​. To simplify the description of the constraints, we use variables vb​ and vc​ defined above and define the value representing an entry in the sibling table as follows: vsibling​=α0​+α3​⋅i+b⋅vb​+(1−b)⋅vc​ Using the above value, we can define the constraint for updating p1​ as follows: p1′​⋅((fmv​+fmva​)⋅vsibling​+1−(fmv​+fmva​))=p1​⋅((fmu​+fmua​)⋅vsibling​+1−(fmu​+fmua​)) The above constraint reduces to the following under various flag conditions: Condition Applied constraint fmv​=1 p1′​⋅vsibling​=p1​ fmva​=1 p1′​⋅vsibling​=p1​ fmu​=1 p1′​=p1​⋅vsibling​ fmua​=1 p1′​=p1​⋅vsibling​ Otherwise p1′​=p1​ Note that the degree of the above constraint is 7. To make sure computation of the old Merkle root is immediately followed by the computation of the new Merkle root, we impose the following constraint: (fbp​+fmp​+fmv​)⋅(1−p1​)=0 | degree=5 The above means that whenever we start a new computation which is not the computation of the new Merkle root, the sibling table must be empty. Thus, after the hash chiplet computes the old Merkle root, the only way to clear the table is to compute the new Merkle root. Together with boundary constraints enforcing that p1​=1 at the first and last rows of the running product column which implements the sibling table, the above constraints ensure that if a node was included into p1​ as a part of computing the old Merkle root, the same node must be removed from p1​ as a part of computing the new Merkle root. These two boundary constraints are described as part of the chiplets virtual table constraints .","breadcrumbs":"Design » Chiplets » Hash Chiplet » Multiset check constraints","id":"254","title":"Multiset check constraints"},"255":{"body":"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 a and b are field elements in a 64-bit prime field. Assume also that a and b are known to contain values smaller than 232. We want to compute a⊕b→z, where ⊕ is either bitwise AND or XOR, and z is a field element containing the result of the corresponding bitwise operation. First, observe that we can compute AND and XOR relations for single bit values as follows: and(a,b)=a⋅b xor(a,b)=a+b−2⋅a⋅b To compute bitwise operations for multi-bit values, we will decompose the values into individual bits, apply the operations to single bits, and then aggregate the bitwsie results into the final result. To perform this operation we will use a table with 12 columns, and computing a single AND or XOR operation will require 8 table rows. We will also rely on two periodic columns as shown below. bitwise_execution_trace In the above, the columns have the following meanings: Periodic columns k0​ and k1​. These columns contain values needed to switch various constraints on or off. k0​ contains a single one, followed by a repeating sequence of seven zeros. k1​ contains a repeating sequence of seven ones, followed by a single zero. Input columns a and b. On the first row of each 8-row cycle, the prover will set values in these columns to the upper 4 bits of the values to which a bitwise operation is to be applied. For all subsequent rows, we will append the next-most-significant 4-bit limb to each value. Thus, by the final row columns a and b will contain the full input values for the bitwise operation. Columns a0​, a1​, a2​, a3​, b0​, b1​, b2​, b3​ will contain lower 4 bits of their corresponding values. Output column zp​. This column represents the value of column z for the prior row. For the first row, it is set to 0. Output column z. This column will be used to aggregate the results of bitwise operations performed over columns a0​, a1​, a2​, a3​, b0​, b1​, b2​, b3​. By the time we get to the last row in each 8-row cycle, this column will contain the final result.","breadcrumbs":"Design » Chiplets » Bitwise Chiplet » Bitwise chiplet","id":"255","title":"Bitwise chiplet"},"256":{"body":"Let's illustrate the above table on a concrete example. For simplicity, we'll use 16-bit values, and thus, we'll only need 4 rows to complete the operation (rather than 8 for 32-bit values). Let's say a=41851 (b1010_0011_0111_1011) and b=40426 (b1001_1101_1110_1010), then and(a,b)=33130 (b1000_0001_0110_1010). The table for this computation looks like so: a b a0 a1 a2 a3 b0 b1 b2 b3 zp z 10 9 0 1 0 1 1 0 0 1 0 8 163 157 1 1 0 0 1 0 1 1 8 129 2615 2526 1 1 1 0 0 1 1 1 129 2070 41851 40426 1 1 0 1 0 1 0 1 2070 33130 Here, in the first row, we set each of the a and b columns to the value of their most-significant 4-bit limb. The bit columns (a0​..a3​ and b0​..b3​) in the first row contain the lower 4 bits of their corresponding values (b1010 and b1001). Column z contains the result of bitwise AND for the upper 4 bits (b1000), while column zp​ contains that result for the prior row. With every subsequent row, we inject the next-most-significant 4 bits of each value into the bit columns, increase the a and b columns accordingly, and aggregate the result of bitwise AND into the z column, adding it to 24 times the value of z in the previous row. We set column zp​ to be the value of z in the prior row. By the time we get to the last row, the z column contains the result of the bitwise AND, while columns a and b contain their original values.","breadcrumbs":"Design » Chiplets » Bitwise Chiplet » Example","id":"256","title":"Example"},"257":{"body":"AIR constraints needed to ensure the correctness of the above table are described below. We also add one more column s to the execution trace, to allow us to select between two bitwise operations (U32AND and U32XOR).","breadcrumbs":"Design » Chiplets » Bitwise Chiplet » Constraints","id":"257","title":"Constraints"},"258":{"body":"The Bitwise chiplet supports two operations with the following operation selectors: U32AND: s=0 U32XOR: s=1 The constraints must require that the selectors be binary and stay the same throughout the cycle: s2−s=0 | degree=2 k1​⋅(s′−s)=0 | degree=2","breadcrumbs":"Design » Chiplets » Bitwise Chiplet » Selectors","id":"258","title":"Selectors"},"259":{"body":"We need to make sure that inputs a and b are decomposed correctly into their individual bits. To do this, first, we need to make sure that columns a0​, a1​, a2​, a3​, b0​, b1​, b2​, b3​, can contain only binary values (0 or 1). This can be accomplished with the following constraints (for i ranging between 0 and 3): ai2​−ai​=0 | degree=2 bi2​−bi​=0 | degree=2 Then, we need to make sure that on the first row of every 8-row cycle, the values in the columns a and b are exactly equal to the aggregation of binary values contained in the individual bit columns ai​, and bi​. This can be enforced with the following constraints: k0​⋅(a−i=0∑3​(2i⋅ai​))=0 | degree=2 k0​⋅(b−i=0∑3​(2i⋅bi​))=0 | degree=2 The above constraints enforce that when k0​=1, a=∑i=03​(2i⋅ai​) and b=∑i=03​(2i⋅bi​). Lastly, we need to make sure that for all rows in an 8-row cycle except for the last one, the values in a and b columns are increased by the values contained in the individual bit columns ai​ and bi​. Denoting a as the value of column a in the current row, and a′ as the value of column a in the next row, we can enforce these conditions as follows: k1​⋅(a′−(a⋅16+i=0∑3​(2i⋅ai′​)))=0 | degree=2 k1​⋅(b′−(b⋅16+i=0∑3​(2i⋅bi′​)))=0 | degree=2 The above constraints enforce that when k1​=1 , a′=16⋅a+∑i=03​(2i⋅ai′​) and b′=16⋅b+∑i=03​(2i⋅bi′​).","breadcrumbs":"Design » Chiplets » Bitwise Chiplet » Input decomposition","id":"259","title":"Input decomposition"},"26":{"body":"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: ./target/optimized/miden repl","breadcrumbs":"Development tooling » REPL » Miden REPL","id":"26","title":"Miden REPL"},"260":{"body":"To ensure correct aggregation of operations over individual bits, first we need to ensure that in the first row, the aggregated output value of the previous row should be 0. k0​⋅zp​=0 | degree=2 Next, we need to ensure that for each row except the last, the aggregated output value must equal the previous aggregated output value in the next row. k1​⋅(z−zp′​)=0 | degree=2 Lastly, we need to ensure that for all rows the value in the z column is computed by multiplying the previous output value (from the zp​ column in the current row) by 16 and then adding it to the bitwise operation applied to the row's set of bits of a and b. The entire constraint must also be multiplied by the operation selector flag to ensure it is only applied for the appropriate operation. For U32AND, this is enforced with the following constraint: (1−s)⋅(z−(zp​⋅16+i=0∑3​(2i⋅ai​⋅bi​)))=0 | degree=3 For U32XOR, this is enforced with the following constraint: s⋅(z−(zp​⋅16+i=0∑3​(2i⋅(ai​+bi​−2⋅ai​⋅bi​))))=0 | degree=3","breadcrumbs":"Design » Chiplets » Bitwise Chiplet » Output aggregation","id":"260","title":"Output aggregation"},"261":{"body":"To simplify the notation for describing bitwise constraints on the chiplets bus, we'll first define variable u, which represents how a, b, and z in the execution trace are reduced to a single value. Denoting the random values received from the verifier as α0​,α1​, etc., this can be achieved as follows. u=α0​+α1​⋅opbit​+α2​⋅a+α3​⋅b+α4​⋅z Where, opbit​ is the unique operation label of the bitwise operation. The request side of the constraint for the bitwise operation is described in the stack bitwise operation section . To provide the results of bitwise operations to the chiplets bus, we want to include values of a, b and z at the last row of the cycle. First, we'll define another intermediate variable vi​. It will include u into the product when k1​=0. (ui​ represents the value of u for row i of the trace.) vi​=(1−k1​)⋅ui​ Then, setting m=1−k1​, we can compute the permutation product from the bitwise chiplet as follows: i=0∏n​(vi​⋅mi​+1−mi​) The above ensures that when 1−k1​=0 (which is true for all rows in the 8-row cycle except for the last one), the product does not change. Otherwise, vi​ gets included into the product. The response side of the bus communication can be enforced with the following constraint: bchip′​=bchip​⋅(vi​⋅mi​+1−mi​) | degree=4","breadcrumbs":"Design » Chiplets » Bitwise Chiplet » Chiplets bus constraints","id":"261","title":"Chiplets bus constraints"},"262":{"body":"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 64-bit prime field with modulus 264−232+1. 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. The design makes extensive use of 16-bit range checks. An efficient way of implementing such range checks is described here .","breadcrumbs":"Design » Chiplets » Memory Chiplet » Memory chiplet","id":"262","title":"Memory chiplet"},"263":{"body":"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. memory_alternative_design 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)⋅(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)⋅(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.","breadcrumbs":"Design » Chiplets » Memory Chiplet » Alternative designs","id":"263","title":"Alternative designs"},"264":{"body":"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. memory_read_write 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)⋅(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)⋅vold′​=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′)⋅(vnew​−vold′​)=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: memory_limitation_diagram 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′)⋅((i′−i−1)−(216⋅d1′​+d0′​))=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.","breadcrumbs":"Design » Chiplets » Memory Chiplet » Read-write memory","id":"264","title":"Read-write memory"},"265":{"body":"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: memory_non_contiguous_memory 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)⋅t′ Then, to make sure the prover sets the value of t correctly, we'll impose the following constraints: n2−n=0(1−n)⋅(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)−(216⋅d1′​+d0′​)=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)−(216⋅d1′​+d0′​)=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: (n⋅(a′−a)+(1−n)⋅(i′−i−1))−(216⋅d1′​+d0′​)=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.","breadcrumbs":"Design » Chiplets » Memory Chiplet » Non-contiguous memory","id":"265","title":"Non-contiguous memory"},"266":{"body":"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. memory_context_separation 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 n0​ and n1​ as follows: n0​=(c′−c)⋅t′n1​=(a′−a)⋅t′ Thus, n0​=1 when the context changes, and 0 otherwise. Also, (1−n0​)⋅n1​=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: n02​−n0​=0(1−n0​)⋅(c′−c)=0(1−n0​)⋅(n12​−n1​)=0(1−n0​)⋅(1−n1​)⋅(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 n0​=1 (c′−c)−(216⋅d1′​+d0′​)=0 When the context changes, columns d0 and d1 at the next row should contain the delta between the old and the new contexts. n0​=0 n1​=1 (a′−a)−(216⋅d1′​+d0′​)=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. n0​=0 n1​=0 (i′−i−1)−(216⋅d1′​+d0′​)=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: (n0​⋅(c′−c)+(1−n0​)⋅(n1​⋅(a−a′)+(1−n1​)⋅(i′−i−1)))−(216⋅d1′​+d0′​)=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.","breadcrumbs":"Design » Chiplets » Memory Chiplet » Context separation","id":"266","title":"Context separation"},"267":{"body":"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 6x 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 memory word-addressable . That is 4 field elements are located at each memory address, and we can read and write elements to/from memory in batches of four. The layout of Miden VM memory table is shown below: memory_miden_vm_layout where: s0 is a selector column which is set to 1 for read operations and 0 for write operations. s1 is a selector oclumn which is set to 1 when previously accessed memory is being read and 0 otherwise. In other words, it is set to 1 only when the context and address are the same as they were in the previous row and the s0 operation selector is set to 1 (indicating a read). ctx contains context ID. Values in this column must increase monotonically but there can be gaps between two consecutive values of up to 232. Also, two consecutive values can be the same. In AIR constraint description below, we refer to this column as c. addr contains memory address. Values in this column must increase monotonically for a given context but there can be gaps between two consecutive values of up to 232. Also, two consecutive values can be the same. In AIR constraint description below, we refer to this column as a. clk contains clock cycle at which the memory operation happened. Values in this column must increase monotonically for a given context and memory address but there can be gaps between two consecutive values of up to 232. In AIR constraint description below, we refer to this column as i. v0, v1, v2, v3 columns contain field elements stored at a given context/address/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, these columns contain (c′−c). When the context remains the same but the address changes, these columns contain (a′−a). When both the context and the address remain the same, these columns contain (i′−i−1). Column t contains the inverse of the delta between two consecutive context IDs, addresses, or clock cycles. Specifically: When the context changes, this column contains the inverse of (c′−c). When the context remains the same but the address changes, this column contains the inverse of (a′−a). When both the context and the address remain the same, this column contains the inverse of (i′−i−1). For every memory access operation (i.e., read or write), a new row is added to the memory table. For read operations, s0 is set to 1. If neither ctx nor addr have changed, then s1 is set to 1 and the v columns are set to equal the values from the previous row. If ctx or addr have changed, then s1 is set to 0 and the v columns are initialized to 0. For write operations, the values may be different, and both selector columns s0 and s1 are set to 0. The amortized cost of reading or writing a single value is between 4 and 5 trace cells (this accounts for the trace cells needed for 16-bit range checks). Thus, from performance standpoint, this approach is roughly 2.5x worse than the simple contiguous write-once memory described earlier. However, our view is that this trade-off is worth it given that this approach provides read-write memory, context separation, and eliminates the contiguous memory requirement.","breadcrumbs":"Design » Chiplets » Memory Chiplet » Miden approach","id":"267","title":"Miden approach"},"268":{"body":"To simplify description of constraints, we'll define two variables n0​ and n1​ as follows: n0​=Δc⋅t′n1​=Δa⋅t′ Where Δc=c′−c and Δa=a′−a. To make sure the prover sets the value of column t correctly, we'll need to impose the following constraints: n02​−n0​=0 | degree=4 (1−n0​)⋅Δc=0 | degree=3 (1−n0​)⋅(n12​−n1​)=0 | degree=6 (1−n0​)⋅(1−n1​)⋅Δa=0 | degree=5 The above constraints guarantee that when context changes, n0​=1. When context remains the same but address changes, (1−n0​)⋅n1​=1. And when neither the context nor the address change, (1−n0​)⋅(1−n1​)=1. To enforce the values of the selector columns, we first require that they both contain only binary values. s02​−s0​=0 | degree=2 s12​−s1​=0 | degree=2 Then we require that s1​ is always set to 1 during read operations when the context and address did not change and to 0 in all other cases. (1−n0​)⋅(1−n1​)⋅s0′​⋅(1−s1′​)=0 | degree=6 (n0​+(1−n0​)⋅n1​+(1−s0′​))⋅s1′​=0 | degree=5 The first constraint enforces that s_1 is 1 when the operation is a read and ctx and addr are both unchanged. The second constraint enforces that when either the context changed, the address changed, or the operation is a write, then s_1 is set to 0. To enforce the values of context ID, address, and clock cycle grow monotonically as described in the previous section, we define the following constraint. (n0​⋅Δc+(1−n0​)⋅(n1​⋅Δa+(1−n1​)⋅Δi))−(216⋅d1′​+d0′​)=0 | degree=5 Where Δi=i′−i−1. In addition to this constraint, we also need to make sure that the values in registers d0​ and d1​ are less than 216, and this can be done with range checks . Next, we need to make sure that values at a given memory address are always initialized to 0. This can be done with the following constraint: s0​⋅(1−s1​)⋅vi​=0 for i∈{0,1,2,3} | degree=3 Thus, when the operation is a read and either the context changes or the address changes, values in the vi​ columns are guaranteed to be zeros. Lastly, we need to make sure that for the same context/address combination, the vi​ columns of the current row are equal to the corresponding vi​ columns of the next row. This can be done with the following constraints: s1​⋅(vi′​−vi​)=0 for i∈{0,1,2,3} | degree=2 Chiplets bus constraints Communication between the memory chiplet and the stack is accomplished via the chiplets bus bchip​. To respond to memory access requests from the stack, we need to divide the current value in bchip​ by the value representing a row in the memory table. This value can be computed as follows: vmem​=α0​+α1​⋅opmem​+α2​⋅c+α3​⋅a+α4​⋅i+j=0∑3​(αj+5​⋅vj​) Where, opmem​ is the unique operation label of the memory access operation. To ensure that values of memory table rows are included into the chiplets bus, we impose the following constraint: bchip′​=bchip​⋅vmem​ | degree=2 On the stack side, for every memory access request, a corresponding value is divided out of the bchip​ column. Specifics of how this is done are described here .","breadcrumbs":"Design » Chiplets » Memory Chiplet » AIR constraints","id":"268","title":"AIR constraints"},"269":{"body":"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 .","breadcrumbs":"Design » Chiplets » Kernel ROM Chiplet » Kernel ROM chiplet","id":"269","title":"Kernel ROM chiplet"},"27":{"body":"All Miden instructions mentioned in the Miden Assembly sections are valid. One can either input instructions one by one or multiple instructions in one input. For example, the below two commands will result in the same output. >> push.1\n>> push.2\n>> push.3 push.1 push.2 push.3 To execute a control flow operation, one must write the entire statement in a single line with spaces between individual operations. repeat.20 pow2\nend The above example should be written as follows in the REPL tool: repeat.20 pow2 end","breadcrumbs":"Development tooling » REPL » Miden assembly instruction","id":"27","title":"Miden assembly instruction"},"270":{"body":"The kernel ROM table consists of 6 columns. kernel_rom_execution_trace The meaning of columns in the above is as follows: Column s0​ specifies whether the value in the row should be included into the chiplets bus bchip​. addr is a row address column which starts out at 0 and must either remain the same or be incremented by 1 with every row. r0​,...,r3​ are contain the roots of the kernel functions. The values in these columns can change only when the value in the addr column changes. If the addr column remains the same, the values in the r columns must also remain the same.","breadcrumbs":"Design » Chiplets » Kernel ROM Chiplet » Kernel ROM trace","id":"270","title":"Kernel ROM trace"},"271":{"body":"The following constraints are required to enforce correctness of the kernel ROM trace. For convenience, let's define Δaddr=addr′−addr. The s0​ column must be binary. s02​−s0​=0 | degree=2 The value in the addr column must either stay the same or increase by 1. Δaddr⋅(1−Δaddr)=0 | degree=2 Finally, if the addr column stays the same then the kernel procedure root must not change. This can be achieved by enforcing the following constraint against each of the four procedure root columns: (1−Δaddr)⋅(ri′​−ri​)=0 | degree=2 These constraints on addr should not be applied to the very last row of the kernel ROM's execution trace, since we do not want to enforce a value that would conflict with the first row of a subsequent chiplet (or padding). Therefore we can create a special virtual flag for this constraint using the chip_s3​ selector column from the chiplets module that selects for the kernel ROM chiplet. The modified constraints which should be applied are the following: (1−chip_s3′​)⋅Δaddr⋅(1−Δaddr)=0 | degree=3 (1−chip_s3′​)⋅(1−Δaddr)⋅(ri′​−ri​)=0 | degree=3 Note: these constraints should also be multiplied by chiplets module's selector flag for the kernel ROM chiplet, as is true for all constraints in this chiplet.","breadcrumbs":"Design » Chiplets » Kernel ROM Chiplet » Constraints","id":"271","title":"Constraints"},"272":{"body":"The chiplets bus is used to keep track of all kernel function calls. To simplify the notation for describing kernel ROM constraints on the chiplets bus, we'll first define variable u, which represents how each kernel procedure in the kernel ROM's execution trace is reduced to a single value. Denoting the random values received from the verifier as α0​,α1​, etc., this can be achieved as follows. v=α0​+α1​⋅opkrom​+i=0∑3​(αi+2​⋅ri​) Where, opkrom​ is the unique operation label of the kernel procedure call operation. The request side of the constraint for the operation is enforced during program block hashing of the SYSCALL operation . To provide accessed kernel procedures to the chiplets bus, we must send the kernel procedure to the bus every time it is called, which is indicated by the s0​ column. bchip′​=bchip​⋅(s0​⋅v+1−s0​) | degree=3 Thus, when s0​=0 this reduces to bchip′​=bchip​, but when s0​=1 it becomes bchip′​=bchip​⋅u.","breadcrumbs":"Design » Chiplets » Kernel ROM Chiplet » Chiplets bus constraints","id":"272","title":"Chiplets bus constraints"},"273":{"body":"Note: Although this table is described independently, it is implemented as part of the chiplets virtual table , which combines all virtual tables required by the any of the chiplets into a single master table. This kernel procedure table keeps track of all unique kernel function roots. The values in this table will be updated only when the value in the address column changes. The row value included into vtchip​ is: v=α0​+α1​⋅addr+i=0∑3​(αi+2​⋅ri​) The constraint against vtchip​ is: vtchip′​=vtchip​⋅(Δaddr⋅v+1−Δaddr) | degree=3 Thus, when Δaddr=0, the above reduces to vtchip′​=vtchip​, but when Δaddr=1, the above becomes vtchip′​=vtchip​⋅v. We also need to impose boundary constraints to make sure that running product column implementing the kernel procedure table is equal to 1 when the kernel procedure table begins and to the product of all unique kernel functions when it ends. The last boundary constraint means that the verifier only needs to know which kernel was used, but doesn't need to know which functions were invoked within the kernel. These two constraints are described as part of the chiplets virtual table constraints .","breadcrumbs":"Design » Chiplets » Kernel ROM Chiplet » Kernel procedure table constraints","id":"273","title":"Kernel procedure table constraints"},"274":{"body":"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: 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). To prove correct interaction between two independent sections of the execution trace, e.g., between the main trace where the result of some operation is required, but would be expensive to compute, and a specialized component which can perform that operation cheaply. The first is achieved using virtual tables of data, where we add a row at some cycle in the trace and remove it at a later cycle when it is needed again. Instead of maintaining the entire table in the execution trace, multiset checks allow us to prove data consistency of this table using one running product column. The second is done by reducing each operation to a lookup value and then using a communication bus to provably connect the two sections of the trace. These communication buses can be implemented either via multiset checks or via the LogUp argument .","breadcrumbs":"Design » Lookup arguments » Lookup arguments in Miden VM","id":"274","title":"Lookup arguments in Miden VM"},"275":{"body":"Miden VM makes use of 6 virtual tables across 4 components, all of which are implemented via multiset checks : Stack: Overflow table Decoder: Block stack table Block hash table Op group table Chiplets: Chiplets virtual table , which combines the following two tables into one: Hash chiplet sibling table Kernel ROM chiplet procedure table","breadcrumbs":"Design » Lookup arguments » Virtual tables in Miden VM","id":"275","title":"Virtual tables in Miden VM"},"276":{"body":"One strategy for improving the efficiency of a zero knowledge virtual machine is to use specialized components for complex operations and have the main circuit “offload” those operations to the corresponding components by specifying inputs and outputs and allowing the proof of execution to be done by the dedicated component instead of by the main circuit. These specialized components are designed to prove the internal correctness of the execution of the operations they support. However, in isolation they cannot make any guarantees about the source of the input data or the destination of the output data. In order to prove that the inputs and outputs specified by the main circuit match the inputs and outputs provably executed in the specialized component, some kind of provable communication bus is needed. This bus is typically implemented as some kind of lookup argument, and in Miden VM in particular we use multiset checks or LogUp. Miden VM uses 2 communication buses: The chiplets bus bchip​ , which communicates with all of the chiplets (Hash, Bitwise, Memory, and Kernel ROM). It is implemented using multiset checks. The range checker bus brange​ , which facilitates requests between the stack and memory components and the range checker . It is implemented using LogUp.","breadcrumbs":"Design » Lookup arguments » Communication buses in Miden VM","id":"276","title":"Communication buses in Miden VM"},"277":{"body":"The auxiliary columns used for buses and virtual tables are computed by including information from the current row of the main execution trace into the next row of the auxiliary trace column. Thus, in order to ensure that the trace is long enough to give the auxiliary column space for its final value, a padding row may be required at the end of the trace of the component upon which the auxiliary column depends. This is true when the data in the main trace could go all the way to the end of the trace, such as in the case of the range checker.","breadcrumbs":"Design » Lookup arguments » Length of auxiliary columns for lookup arguments","id":"277","title":"Length of auxiliary columns for lookup arguments"},"278":{"body":"It is important to note that depending on the field in which we operate, an auxilliary column implementing a lookup argument may actually require more than one trace column. This is specifically true for small fields. Since Miden uses a 64-bit field, each auxiliary column needs to be represented by 2 columns to achieve ~100-bit security and by 3 columns to achieve ~128-bit security.","breadcrumbs":"Design » Lookup arguments » Cost of auxiliary columns for lookup arguments","id":"278","title":"Cost of auxiliary columns for lookup arguments"},"279":{"body":"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 .","breadcrumbs":"Design » Lookup arguments » Multiset checks » Multiset checks","id":"279","title":"Multiset checks"},"28":{"body":"The !help command prints out all the available commands in the REPL tool.","breadcrumbs":"Development tooling » REPL » !help","id":"28","title":"!help"},"280":{"body":"Although the multiset equality check can be thought of as comparing multiset equality between two vectors a and b, in Miden VM it is implemented as a single running product column in the following way: The running product column is initialized to a value x at the beginning of the trace. (We typically use x=1.) All values of a are multiplied into the running product column. All values of b are divided out of the running product column. If a and b were multiset equal, then the running product column will equal x at the end of the trace. Running product columns are computed using a set of random values α0​, α1​,... sent to the prover by the verifier after the prover commits to the execution trace of the program.","breadcrumbs":"Design » Lookup arguments » Multiset checks » Running product columns","id":"280","title":"Running product columns"},"281":{"body":"Virtual tables can be used to store intermediate data which is computed at one cycle and used at a different cycle. When the data is computed, the row is added to the table, and when it is used later, the row is deleted from the table. Thus, all that needs to be proved is the data consistency between the row that was added and the row that was deleted. The consistency of a virtual table can be proved with a single trace column p, which keeps a running product of rows that were inserted into and deleted from the table. This is done by reducing each row to a single value, multiplying the value into p when the row is inserted, and dividing the value out of p when the row is removed. Thus, at any step of the computation, p​ will contain a product of all rows currently in the table. The initial value of p​ is set to 1. Thus, if the table is empty by the time Miden VM finishes executing a program (we added and then removed exactly the same set of rows), the final value of p​ will also be equal to 1. The initial and final values are enforced via boundary constraints.","breadcrumbs":"Design » Lookup arguments » Multiset checks » Virtual tables","id":"281","title":"Virtual tables"},"282":{"body":"To compute a product of rows, we'll first need to reduce each row to a single value. This can be done as follows. Let t0​,t1​,t2​,... be columns in the virtual table, and assume the verifier sends a set of random values α0​, α1​,... to the prover after the prover commits to the execution trace of the program. The prover reduces row i in the table to a single value ri​ as: ri​=α0​+α1​⋅t0,i​+α2​⋅t1,i​+α3​⋅t2,i​+... Then, when row i is added to the table, we'll update the value in the p column like so: p′=p⋅ri​ Analogously, when row i is removed from the table, we'll update the value in column p like so: p′=ri​p​","breadcrumbs":"Design » Lookup arguments » Multiset checks » Computing a virtual table's trace column","id":"282","title":"Computing a virtual table's trace column"},"283":{"body":"Miden VM makes use of 6 virtual tables across 4 components: Stack: Overflow table Decoder: Block stack table Block hash table Op group table Chiplets: Chiplets virtual table , which combines the following two tables into one: Hash chiplet sibling table Kernel ROM chiplet procedure table","breadcrumbs":"Design » Lookup arguments » Multiset checks » Virtual tables in Miden VM","id":"283","title":"Virtual tables in Miden VM"},"284":{"body":"A bus can be implemented as a single trace column b where a request can be sent to a specific component and a corresponding response will be sent back by that component. The values in this column contain a running product of the communication with the component as follows: Each request is “sent” by computing a lookup value from some information that's specific to the specialized component, the operation inputs, and the operation outputs, and then dividing it out of the running product column b. Each chiplet response is “sent” by computing the same lookup value from the component-specific information, inputs, and outputs, and then multiplying it into the running product column b. Thus, if the requests and responses match, and the bus column b is initialized to 1, then b will start and end with the value 1. This condition is enforced by boundary constraints on column b. Note that the order of the requests and responses does not matter, as long as they are all included in b. In fact, requests and responses for the same operation will generally occur at different cycles. Additionally, there could be multiple requests sent in the same cycle, and there could also be a response provided at the same cycle that a request is received.","breadcrumbs":"Design » Lookup arguments » Multiset checks » Communication buses via multiset checks","id":"284","title":"Communication buses via multiset checks"},"285":{"body":"These constraints can be expressed in a general way with the 2 following requirements: The lookup value must be computed using random values α0​,α1​, etc. that are provided by the verifier after the prover has committed to the main execution trace. The lookup value must include all uniquely identifying information for the component/operation and its inputs and outputs. Given an example operation opex​ with inputs i0​,...,in​ and outputs o0​,...,om​, the lookup value can be computed as follows: lookup=α0​+α1​⋅opex​+α2​⋅i0​+...+αn+2​⋅in​+αn+3​⋅o0​+...+αn+2+m​⋅om​ The constraint for sending this to the bus as a request would be: b′⋅lookup=b The constraint for sending this to the bus as a response would be: b′=b⋅lookup However, these constraints must be combined, since it's possible that requests and responses both occur during the same cycle. To combine them, let ulookup​ be the request value and let vlookup​ be the response value. These values are both computed the same way as shown above, but the data sources are different, since the input/output values used to compute ulookup​ come from the trace of the component that's \"offloading\" the computation, while the input/output values used to compute vlookup​ come from the trace of the specialized component. The final constraint can be expressed as: b′⋅ulookup​=b⋅vlookup​","breadcrumbs":"Design » Lookup arguments » Multiset checks » Communication bus constraints","id":"285","title":"Communication bus constraints"},"286":{"body":"In Miden VM, the specialized components are implemented as dedicated segments of the execution trace, which include the 3 chiplets in the Chiplets module (the hash chiplet, bitwise chiplet, and memory chiplet). Miden VM currently uses multiset checks to implement the chiplets bus bchip​ , which communicates with all of the chiplets (Hash, Bitwise, and Memory).","breadcrumbs":"Design » Lookup arguments » Multiset checks » Communication buses in Miden VM","id":"286","title":"Communication buses in Miden VM"},"287":{"body":"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 a and b in the main trace where a contains duplicates and b does not (i.e. b is part of the lookup table), LogUp allows us to compute two logarithmic derivatives and check their equality. i=0∑l​(α−ai​)1​=i=0∑n​(α−bi​)mi​​ In the above: l is the number of values in a, which must be smaller than the size of the field. (The prime field used for Miden VM has modulus p=264−232+1, so l
> push.1.2.3.4\n>> repeat.16 pow2 end\n>> u32checked_add >> !program\nbegin push.1.2.3.4 repeat.16 pow2 end u32checked_add\nend","breadcrumbs":"Development tooling » REPL » !program","id":"29","title":"!program"},"290":{"body":"The functionality of the bus can easily be extended to receive lookup requests from multiple components. For example, to additionally support requests from column y, the bus constraint would be modified to the following: b′=b+(α−v)m​−(α−x)1​−(α−y)1​ | degree=4 Since the maximum constraint degree in Miden VM is 9, the lookup table T could accommodate requests from at most 7 trace columns in the same trace row via this construction.","breadcrumbs":"Design » Lookup arguments » LogUp » Extending the construction to multiple components","id":"290","title":"Extending the construction to multiple components"},"291":{"body":"Boolean flags can also be used to determine when requests from various components are sent to the bus. For example, let fx​ be 1 when a request should be sent from x and 0 otherwise, and let fy​ be similarly defined for column y. We can use the following constraint to turn requests on or off: b′=b+(α−v)m​−(α−x)fx​​−(α−y)fy​​ | degree=4 If any of these flags have degree greater than 2 then this will increase the overall degree of the constraint and reduce the number of lookup requests that can be accommodated by the bus per row.","breadcrumbs":"Design » Lookup arguments » LogUp » Extending the construction with flags","id":"291","title":"Extending the construction with flags"},"292":{"body":"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: STARKs paper: Scalable, transparent, and post-quantum secure computational integrity STARKs vs. SNARKs: A Cambrian Explosion of Crypto Proofs Vitalik Buterin's blog series on zk-STARKs: STARKs, part 1: Proofs with Polynomials STARKs, part 2: Thank Goodness it's FRI-day STARKs, part 3: Into the Weeds Alan Szepieniec's STARK tutorials: Anatomy of a STARK BrainSTARK StarkWare's STARK Math blog series: STARK Math: The Journey Begins Arithmetization I Arithmetization II Low Degree Testing A Framework for Efficient STARKs StarkWare's STARK tutorial: STARK 101","breadcrumbs":"Background Material » Background Material","id":"292","title":"Background Material"},"3":{"body":"In the coming months we plan to finalize the design of the VM and implement support for the following features: Recursive proofs. Miden VM will soon be able to verify a proof of its own execution. This will enable infinitely recursive proofs, an extremely useful tool for real-world applications. Better debugging. Miden VM will provide a better debugging experience including the ability to place breakpoints, better source mapping, and more complete program analysis info. Faulty execution. Miden VM will support generating proofs for programs with faulty execution (a notoriously complex task in ZK context). That is, it will be possible to prove that execution of some program resulted in an error.","breadcrumbs":"Introduction » Planned features","id":"3","title":"Planned features"},"30":{"body":"The !stack command prints out the state of the stack at the last executed instruction. Since the stack always contains at least 16 elements, 16 or more elements will be printed out (even if all of them are zeros). >> push.1 push.2 push.3 push.4 push.5\n>> exp\n>> u32checked_mul\n>> swap\n>> eq.2\n>> assert The !stack command will print out the following state of the stack: >> !stack\n3072 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0","breadcrumbs":"Development tooling » REPL » !stack","id":"30","title":"!stack"},"31":{"body":"The !mem command prints out the contents of all initialized memory locations. For each such location, the address, along with its memory values, is printed. Recall that four elements are stored at each memory address. If the memory has at least one value that has been initialized: >> !mem\n7: [1, 2, 0, 3]\n8: [5, 7, 3, 32]\n9: [9, 10, 2, 0] If the memory is not yet been initialized: >> !mem\nThe memory has not been initialized yet","breadcrumbs":"Development tooling » REPL » !mem","id":"31","title":"!mem"},"32":{"body":"The !mem[addr] command prints out memory contents at the address specified by addr. If the addr has been initialized: >> !mem[9]\n9: [9, 10, 2, 0] If the addr has not been initialized: >> !mem[87]\nMemory at address 87 is empty","breadcrumbs":"Development tooling » REPL » !mem[addr]","id":"32","title":"!mem[addr]"},"33":{"body":"The !undo command reverts to the previous state of the stack and memory by dropping off the last executed assembly instruction from the program. One could use !undo as often as they want to restore the state of a stack and memory n instructions ago (provided there are n instructions in the program). The !undo command will result in an error if no remaining instructions are left in the Miden program. >> push.1 push.2 push.3\n>> push.4\n>> !stack\n4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 >> push.5\n>> !stack\n5 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 >> !undo\n4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 >> !undo\n3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0","breadcrumbs":"Development tooling » REPL » !undo","id":"33","title":"!undo"},"34":{"body":"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: Miden assembly which provides a detailed description of Miden assembly language, which is the native language of Miden VM. 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.","breadcrumbs":"User Documentation » User Documentation","id":"34","title":"User Documentation"},"35":{"body":"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. assembly_to_VM As compared to raw Miden VM instructions, Miden assembly has several advantages: Miden assembly is intended to be a more stable external interface for the VM. That is, while we plan to make significant changes to the underlying VM to optimize it for stability, performance etc., we intend to make very few breaking changes to Miden assembly. Miden assembly natively supports control flow expressions which the assembler automatically transforms into a program MAST. This greatly simplifies writing programs with complex execution logic. Miden assembly supports macro instructions . These instructions expand into short sequences of raw Miden VM instructions making it easier to encode common operations. Miden assembly supports procedures . These are stand-alone blocks of code which the assembler inlines into program MAST at compile time. This improves program modularity and code organization. The last two points also make Miden assembly much more concise as compared to the raw program MAST. This may be important in the blockchain context where pubic programs need to be stored on chain.","breadcrumbs":"User Documentation » Miden Assembly » Miden Assembly","id":"35","title":"Miden Assembly"},"36":{"body":"In this document we use the following terms and notations: p is the modulus of the VM's base field which is equal to 264−232+1. A binary value means a field element which is either 0 or 1. Inequality comparisons are assumed to be performed on integer representations of field elements in the range [0,p). Throughout this document, we use lower-case letters to refer to individual field elements (e.g., a). Sometimes it is convenient to describe operations over groups of elements. For these purposes we define a word to be a group of four elements. We use upper-case letters to refer to words (e.g., A). To refer to individual elements within a word, we use numerical subscripts. For example, a0​ is the first element of word A, b3​ is the last element of word B, etc.","breadcrumbs":"User Documentation » Miden Assembly » Terms and notations","id":"36","title":"Terms and notations"},"37":{"body":"The design of Miden assembly tries to achieve the following goals: Miden assembly should be an easy compilation target for high-level languages. Programs written in Miden assembly should be readable, even if the code is generated by a compiler from a high-level language. Control flow should be easy to understand to help in manual inspection, formal verification, and optimization. Compilation of Miden assembly into Miden program MAST should be as straight-forward as possible. Serialization of Miden assembly into a binary representation should be as compact and as straight-forward as possible. In order to achieve the first goal, Miden assembly exposes a set of native operations over 32-bit integers and supports linear read-write memory. Thus, from the stand-point of a higher-level language compiler, Miden VM can be viewed as a regular 32-bit stack machine with linear read-write memory. In 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.","breadcrumbs":"User Documentation » Miden Assembly » Design goals","id":"37","title":"Design goals"},"38":{"body":"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. Miden assembly programs are organized into procedures. Procedures, in turn, can be grouped into modules.","breadcrumbs":"User Documentation » Miden Assembly » Code Organization » Code organization","id":"38","title":"Code organization"},"39":{"body":"A procedure can be used to encapsulate a frequently-used sequence of instructions which can later be invoked via a label. A procedure must start with a proc.
> push.1.2.3.4\n>> repeat.16 pow2 end\n>> u32checked_add >> !program\nbegin push.1.2.3.4 repeat.16 pow2 end u32checked_add\nend","breadcrumbs":"Development tooling » REPL » !program","id":"29","title":"!program"},"290":{"body":"The functionality of the bus can easily be extended to receive lookup requests from multiple components. For example, to additionally support requests from column y, the bus constraint would be modified to the following: b′=b+(α−v)m​−(α−x)1​−(α−y)1​ | degree=4 Since the maximum constraint degree in Miden VM is 9, the lookup table T could accommodate requests from at most 7 trace columns in the same trace row via this construction.","breadcrumbs":"Design » Lookup arguments » LogUp » Extending the construction to multiple components","id":"290","title":"Extending the construction to multiple components"},"291":{"body":"Boolean flags can also be used to determine when requests from various components are sent to the bus. For example, let fx​ be 1 when a request should be sent from x and 0 otherwise, and let fy​ be similarly defined for column y. We can use the following constraint to turn requests on or off: b′=b+(α−v)m​−(α−x)fx​​−(α−y)fy​​ | degree=4 If any of these flags have degree greater than 2 then this will increase the overall degree of the constraint and reduce the number of lookup requests that can be accommodated by the bus per row.","breadcrumbs":"Design » Lookup arguments » LogUp » Extending the construction with flags","id":"291","title":"Extending the construction with flags"},"292":{"body":"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: STARKs paper: Scalable, transparent, and post-quantum secure computational integrity STARKs vs. SNARKs: A Cambrian Explosion of Crypto Proofs Vitalik Buterin's blog series on zk-STARKs: STARKs, part 1: Proofs with Polynomials STARKs, part 2: Thank Goodness it's FRI-day STARKs, part 3: Into the Weeds Alan Szepieniec's STARK tutorials: Anatomy of a STARK BrainSTARK StarkWare's STARK Math blog series: STARK Math: The Journey Begins Arithmetization I Arithmetization II Low Degree Testing A Framework for Efficient STARKs StarkWare's STARK tutorial: STARK 101","breadcrumbs":"Background Material » Background Material","id":"292","title":"Background Material"},"3":{"body":"In the coming months we plan to finalize the design of the VM and implement support for the following features: Recursive proofs. Miden VM will soon be able to verify a proof of its own execution. This will enable infinitely recursive proofs, an extremely useful tool for real-world applications. Better debugging. Miden VM will provide a better debugging experience including the ability to place breakpoints, better source mapping, and more complete program analysis info. Faulty execution. Miden VM will support generating proofs for programs with faulty execution (a notoriously complex task in ZK context). That is, it will be possible to prove that execution of some program resulted in an error.","breadcrumbs":"Introduction » Planned features","id":"3","title":"Planned features"},"30":{"body":"The !stack command prints out the state of the stack at the last executed instruction. Since the stack always contains at least 16 elements, 16 or more elements will be printed out (even if all of them are zeros). >> push.1 push.2 push.3 push.4 push.5\n>> exp\n>> u32checked_mul\n>> swap\n>> eq.2\n>> assert The !stack command will print out the following state of the stack: >> !stack\n3072 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0","breadcrumbs":"Development tooling » REPL » !stack","id":"30","title":"!stack"},"31":{"body":"The !mem command prints out the contents of all initialized memory locations. For each such location, the address, along with its memory values, is printed. Recall that four elements are stored at each memory address. If the memory has at least one value that has been initialized: >> !mem\n7: [1, 2, 0, 3]\n8: [5, 7, 3, 32]\n9: [9, 10, 2, 0] If the memory is not yet been initialized: >> !mem\nThe memory has not been initialized yet","breadcrumbs":"Development tooling » REPL » !mem","id":"31","title":"!mem"},"32":{"body":"The !mem[addr] command prints out memory contents at the address specified by addr. If the addr has been initialized: >> !mem[9]\n9: [9, 10, 2, 0] If the addr has not been initialized: >> !mem[87]\nMemory at address 87 is empty","breadcrumbs":"Development tooling » REPL » !mem[addr]","id":"32","title":"!mem[addr]"},"33":{"body":"The !undo command reverts to the previous state of the stack and memory by dropping off the last executed assembly instruction from the program. One could use !undo as often as they want to restore the state of a stack and memory n instructions ago (provided there are n instructions in the program). The !undo command will result in an error if no remaining instructions are left in the Miden program. >> push.1 push.2 push.3\n>> push.4\n>> !stack\n4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 >> push.5\n>> !stack\n5 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 >> !undo\n4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 >> !undo\n3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0","breadcrumbs":"Development tooling » REPL » !undo","id":"33","title":"!undo"},"34":{"body":"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: Miden assembly which provides a detailed description of Miden assembly language, which is the native language of Miden VM. 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.","breadcrumbs":"User Documentation » User Documentation","id":"34","title":"User Documentation"},"35":{"body":"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. assembly_to_VM As compared to raw Miden VM instructions, Miden assembly has several advantages: Miden assembly is intended to be a more stable external interface for the VM. That is, while we plan to make significant changes to the underlying VM to optimize it for stability, performance etc., we intend to make very few breaking changes to Miden assembly. Miden assembly natively supports control flow expressions which the assembler automatically transforms into a program MAST. This greatly simplifies writing programs with complex execution logic. Miden assembly supports macro instructions . These instructions expand into short sequences of raw Miden VM instructions making it easier to encode common operations. Miden assembly supports procedures . These are stand-alone blocks of code which the assembler inlines into program MAST at compile time. This improves program modularity and code organization. The last two points also make Miden assembly much more concise as compared to the raw program MAST. This may be important in the blockchain context where pubic programs need to be stored on chain.","breadcrumbs":"User Documentation » Miden Assembly » Miden Assembly","id":"35","title":"Miden Assembly"},"36":{"body":"In this document we use the following terms and notations: p is the modulus of the VM's base field which is equal to 264−232+1. A binary value means a field element which is either 0 or 1. Inequality comparisons are assumed to be performed on integer representations of field elements in the range [0,p). Throughout this document, we use lower-case letters to refer to individual field elements (e.g., a). Sometimes it is convenient to describe operations over groups of elements. For these purposes we define a word to be a group of four elements. We use upper-case letters to refer to words (e.g., A). To refer to individual elements within a word, we use numerical subscripts. For example, a0​ is the first element of word A, b3​ is the last element of word B, etc.","breadcrumbs":"User Documentation » Miden Assembly » Terms and notations","id":"36","title":"Terms and notations"},"37":{"body":"The design of Miden assembly tries to achieve the following goals: Miden assembly should be an easy compilation target for high-level languages. Programs written in Miden assembly should be readable, even if the code is generated by a compiler from a high-level language. Control flow should be easy to understand to help in manual inspection, formal verification, and optimization. Compilation of Miden assembly into Miden program MAST should be as straight-forward as possible. Serialization of Miden assembly into a binary representation should be as compact and as straight-forward as possible. In order to achieve the first goal, Miden assembly exposes a set of native operations over 32-bit integers and supports linear read-write memory. Thus, from the stand-point of a higher-level language compiler, Miden VM can be viewed as a regular 32-bit stack machine with linear read-write memory. In 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.","breadcrumbs":"User Documentation » Miden Assembly » Design goals","id":"37","title":"Design goals"},"38":{"body":"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. Miden assembly programs are organized into procedures. Procedures, in turn, can be grouped into modules.","breadcrumbs":"User Documentation » Miden Assembly » Code Organization » Code organization","id":"38","title":"Code organization"},"39":{"body":"A procedure can be used to encapsulate a frequently-used sequence of instructions which can later be invoked via a label. A procedure must start with a proc.
> push.1.2.3.4\n>> repeat.16 pow2 end\n>> u32checked_add >> !program\nbegin push.1.2.3.4 repeat.16 pow2 end u32checked_add\nend","breadcrumbs":"Development tooling » REPL » !program","id":"29","title":"!program"},"290":{"body":"The functionality of the bus can easily be extended to receive lookup requests from multiple components. For example, to additionally support requests from column y, the bus constraint would be modified to the following: b′=b+(α−v)m​−(α−x)1​−(α−y)1​ | degree=4 Since the maximum constraint degree in Miden VM is 9, the lookup table T could accommodate requests from at most 7 trace columns in the same trace row via this construction.","breadcrumbs":"Design » Lookup arguments » LogUp » Extending the construction to multiple components","id":"290","title":"Extending the construction to multiple components"},"291":{"body":"Boolean flags can also be used to determine when requests from various components are sent to the bus. For example, let fx​ be 1 when a request should be sent from x and 0 otherwise, and let fy​ be similarly defined for column y. We can use the following constraint to turn requests on or off: b′=b+(α−v)m​−(α−x)fx​​−(α−y)fy​​ | degree=4 If any of these flags have degree greater than 2 then this will increase the overall degree of the constraint and reduce the number of lookup requests that can be accommodated by the bus per row.","breadcrumbs":"Design » Lookup arguments » LogUp » Extending the construction with flags","id":"291","title":"Extending the construction with flags"},"292":{"body":"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: STARKs paper: Scalable, transparent, and post-quantum secure computational integrity STARKs vs. SNARKs: A Cambrian Explosion of Crypto Proofs Vitalik Buterin's blog series on zk-STARKs: STARKs, part 1: Proofs with Polynomials STARKs, part 2: Thank Goodness it's FRI-day STARKs, part 3: Into the Weeds Alan Szepieniec's STARK tutorials: Anatomy of a STARK BrainSTARK StarkWare's STARK Math blog series: STARK Math: The Journey Begins Arithmetization I Arithmetization II Low Degree Testing A Framework for Efficient STARKs StarkWare's STARK tutorial: STARK 101","breadcrumbs":"Background Material » Background Material","id":"292","title":"Background Material"},"3":{"body":"In the coming months we plan to finalize the design of the VM and implement support for the following features: Recursive proofs. Miden VM will soon be able to verify a proof of its own execution. This will enable infinitely recursive proofs, an extremely useful tool for real-world applications. Better debugging. Miden VM will provide a better debugging experience including the ability to place breakpoints, better source mapping, and more complete program analysis info. Faulty execution. Miden VM will support generating proofs for programs with faulty execution (a notoriously complex task in ZK context). That is, it will be possible to prove that execution of some program resulted in an error.","breadcrumbs":"Introduction » Planned features","id":"3","title":"Planned features"},"30":{"body":"The !stack command prints out the state of the stack at the last executed instruction. Since the stack always contains at least 16 elements, 16 or more elements will be printed out (even if all of them are zeros). >> push.1 push.2 push.3 push.4 push.5\n>> exp\n>> u32checked_mul\n>> swap\n>> eq.2\n>> assert The !stack command will print out the following state of the stack: >> !stack\n3072 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0","breadcrumbs":"Development tooling » REPL » !stack","id":"30","title":"!stack"},"31":{"body":"The !mem command prints out the contents of all initialized memory locations. For each such location, the address, along with its memory values, is printed. Recall that four elements are stored at each memory address. If the memory has at least one value that has been initialized: >> !mem\n7: [1, 2, 0, 3]\n8: [5, 7, 3, 32]\n9: [9, 10, 2, 0] If the memory is not yet been initialized: >> !mem\nThe memory has not been initialized yet","breadcrumbs":"Development tooling » REPL » !mem","id":"31","title":"!mem"},"32":{"body":"The !mem[addr] command prints out memory contents at the address specified by addr. If the addr has been initialized: >> !mem[9]\n9: [9, 10, 2, 0] If the addr has not been initialized: >> !mem[87]\nMemory at address 87 is empty","breadcrumbs":"Development tooling » REPL » !mem[addr]","id":"32","title":"!mem[addr]"},"33":{"body":"The !undo command reverts to the previous state of the stack and memory by dropping off the last executed assembly instruction from the program. One could use !undo as often as they want to restore the state of a stack and memory n instructions ago (provided there are n instructions in the program). The !undo command will result in an error if no remaining instructions are left in the Miden program. >> push.1 push.2 push.3\n>> push.4\n>> !stack\n4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 >> push.5\n>> !stack\n5 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 >> !undo\n4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 >> !undo\n3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0","breadcrumbs":"Development tooling » REPL » !undo","id":"33","title":"!undo"},"34":{"body":"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: Miden assembly which provides a detailed description of Miden assembly language, which is the native language of Miden VM. 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.","breadcrumbs":"User Documentation » User Documentation","id":"34","title":"User Documentation"},"35":{"body":"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. assembly_to_VM As compared to raw Miden VM instructions, Miden assembly has several advantages: Miden assembly is intended to be a more stable external interface for the VM. That is, while we plan to make significant changes to the underlying VM to optimize it for stability, performance etc., we intend to make very few breaking changes to Miden assembly. Miden assembly natively supports control flow expressions which the assembler automatically transforms into a program MAST. This greatly simplifies writing programs with complex execution logic. Miden assembly supports macro instructions . These instructions expand into short sequences of raw Miden VM instructions making it easier to encode common operations. Miden assembly supports procedures . These are stand-alone blocks of code which the assembler inlines into program MAST at compile time. This improves program modularity and code organization. The last two points also make Miden assembly much more concise as compared to the raw program MAST. This may be important in the blockchain context where pubic programs need to be stored on chain.","breadcrumbs":"User Documentation » Miden Assembly » Miden Assembly","id":"35","title":"Miden Assembly"},"36":{"body":"In this document we use the following terms and notations: p is the modulus of the VM's base field which is equal to 264−232+1. A binary value means a field element which is either 0 or 1. Inequality comparisons are assumed to be performed on integer representations of field elements in the range [0,p). Throughout this document, we use lower-case letters to refer to individual field elements (e.g., a). Sometimes it is convenient to describe operations over groups of elements. For these purposes we define a word to be a group of four elements. We use upper-case letters to refer to words (e.g., A). To refer to individual elements within a word, we use numerical subscripts. For example, a0​ is the first element of word A, b3​ is the last element of word B, etc.","breadcrumbs":"User Documentation » Miden Assembly » Terms and notations","id":"36","title":"Terms and notations"},"37":{"body":"The design of Miden assembly tries to achieve the following goals: Miden assembly should be an easy compilation target for high-level languages. Programs written in Miden assembly should be readable, even if the code is generated by a compiler from a high-level language. Control flow should be easy to understand to help in manual inspection, formal verification, and optimization. Compilation of Miden assembly into Miden program MAST should be as straight-forward as possible. Serialization of Miden assembly into a binary representation should be as compact and as straight-forward as possible. In order to achieve the first goal, Miden assembly exposes a set of native operations over 32-bit integers and supports linear read-write memory. Thus, from the stand-point of a higher-level language compiler, Miden VM can be viewed as a regular 32-bit stack machine with linear read-write memory. In 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.","breadcrumbs":"User Documentation » Miden Assembly » Design goals","id":"37","title":"Design goals"},"38":{"body":"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. Miden assembly programs are organized into procedures. Procedures, in turn, can be grouped into modules.","breadcrumbs":"User Documentation » Miden Assembly » Code Organization » Code organization","id":"38","title":"Code organization"},"39":{"body":"A procedure can be used to encapsulate a frequently-used sequence of instructions which can later be invoked via a label. A procedure must start with a proc.
> push.1.2.3.4\n>> repeat.16 pow2 end\n>> u32checked_add >> !program\nbegin push.1.2.3.4 repeat.16 pow2 end u32checked_add\nend","breadcrumbs":"Development tooling » REPL » !program","id":"29","title":"!program"},"290":{"body":"The functionality of the bus can easily be extended to receive lookup requests from multiple components. For example, to additionally support requests from column y, the bus constraint would be modified to the following: b′=b+(α−v)m​−(α−x)1​−(α−y)1​ | degree=4 Since the maximum constraint degree in Miden VM is 9, the lookup table T could accommodate requests from at most 7 trace columns in the same trace row via this construction.","breadcrumbs":"Design » Lookup arguments » LogUp » Extending the construction to multiple components","id":"290","title":"Extending the construction to multiple components"},"291":{"body":"Boolean flags can also be used to determine when requests from various components are sent to the bus. For example, let fx​ be 1 when a request should be sent from x and 0 otherwise, and let fy​ be similarly defined for column y. We can use the following constraint to turn requests on or off: b′=b+(α−v)m​−(α−x)fx​​−(α−y)fy​​ | degree=4 If any of these flags have degree greater than 2 then this will increase the overall degree of the constraint and reduce the number of lookup requests that can be accommodated by the bus per row.","breadcrumbs":"Design » Lookup arguments » LogUp » Extending the construction with flags","id":"291","title":"Extending the construction with flags"},"292":{"body":"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: STARKs paper: Scalable, transparent, and post-quantum secure computational integrity STARKs vs. SNARKs: A Cambrian Explosion of Crypto Proofs Vitalik Buterin's blog series on zk-STARKs: STARKs, part 1: Proofs with Polynomials STARKs, part 2: Thank Goodness it's FRI-day STARKs, part 3: Into the Weeds Alan Szepieniec's STARK tutorials: Anatomy of a STARK BrainSTARK StarkWare's STARK Math blog series: STARK Math: The Journey Begins Arithmetization I Arithmetization II Low Degree Testing A Framework for Efficient STARKs StarkWare's STARK tutorial: STARK 101","breadcrumbs":"Background Material » Background Material","id":"292","title":"Background Material"},"3":{"body":"In the coming months we plan to finalize the design of the VM and implement support for the following features: Recursive proofs. Miden VM will soon be able to verify a proof of its own execution. This will enable infinitely recursive proofs, an extremely useful tool for real-world applications. Better debugging. Miden VM will provide a better debugging experience including the ability to place breakpoints, better source mapping, and more complete program analysis info. Faulty execution. Miden VM will support generating proofs for programs with faulty execution (a notoriously complex task in ZK context). That is, it will be possible to prove that execution of some program resulted in an error.","breadcrumbs":"Introduction » Planned features","id":"3","title":"Planned features"},"30":{"body":"The !stack command prints out the state of the stack at the last executed instruction. Since the stack always contains at least 16 elements, 16 or more elements will be printed out (even if all of them are zeros). >> push.1 push.2 push.3 push.4 push.5\n>> exp\n>> u32checked_mul\n>> swap\n>> eq.2\n>> assert The !stack command will print out the following state of the stack: >> !stack\n3072 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0","breadcrumbs":"Development tooling » REPL » !stack","id":"30","title":"!stack"},"31":{"body":"The !mem command prints out the contents of all initialized memory locations. For each such location, the address, along with its memory values, is printed. Recall that four elements are stored at each memory address. If the memory has at least one value that has been initialized: >> !mem\n7: [1, 2, 0, 3]\n8: [5, 7, 3, 32]\n9: [9, 10, 2, 0] If the memory is not yet been initialized: >> !mem\nThe memory has not been initialized yet","breadcrumbs":"Development tooling » REPL » !mem","id":"31","title":"!mem"},"32":{"body":"The !mem[addr] command prints out memory contents at the address specified by addr. If the addr has been initialized: >> !mem[9]\n9: [9, 10, 2, 0] If the addr has not been initialized: >> !mem[87]\nMemory at address 87 is empty","breadcrumbs":"Development tooling » REPL » !mem[addr]","id":"32","title":"!mem[addr]"},"33":{"body":"The !undo command reverts to the previous state of the stack and memory by dropping off the last executed assembly instruction from the program. One could use !undo as often as they want to restore the state of a stack and memory n instructions ago (provided there are n instructions in the program). The !undo command will result in an error if no remaining instructions are left in the Miden program. >> push.1 push.2 push.3\n>> push.4\n>> !stack\n4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 >> push.5\n>> !stack\n5 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 >> !undo\n4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 >> !undo\n3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0","breadcrumbs":"Development tooling » REPL » !undo","id":"33","title":"!undo"},"34":{"body":"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: Miden assembly which provides a detailed description of Miden assembly language, which is the native language of Miden VM. 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.","breadcrumbs":"User Documentation » User Documentation","id":"34","title":"User Documentation"},"35":{"body":"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. assembly_to_VM As compared to raw Miden VM instructions, Miden assembly has several advantages: Miden assembly is intended to be a more stable external interface for the VM. That is, while we plan to make significant changes to the underlying VM to optimize it for stability, performance etc., we intend to make very few breaking changes to Miden assembly. Miden assembly natively supports control flow expressions which the assembler automatically transforms into a program MAST. This greatly simplifies writing programs with complex execution logic. Miden assembly supports macro instructions . These instructions expand into short sequences of raw Miden VM instructions making it easier to encode common operations. Miden assembly supports procedures . These are stand-alone blocks of code which the assembler inlines into program MAST at compile time. This improves program modularity and code organization. The last two points also make Miden assembly much more concise as compared to the raw program MAST. This may be important in the blockchain context where pubic programs need to be stored on chain.","breadcrumbs":"User Documentation » Miden Assembly » Miden Assembly","id":"35","title":"Miden Assembly"},"36":{"body":"In this document we use the following terms and notations: p is the modulus of the VM's base field which is equal to 264−232+1. A binary value means a field element which is either 0 or 1. Inequality comparisons are assumed to be performed on integer representations of field elements in the range [0,p). Throughout this document, we use lower-case letters to refer to individual field elements (e.g., a). Sometimes it is convenient to describe operations over groups of elements. For these purposes we define a word to be a group of four elements. We use upper-case letters to refer to words (e.g., A). To refer to individual elements within a word, we use numerical subscripts. For example, a0​ is the first element of word A, b3​ is the last element of word B, etc.","breadcrumbs":"User Documentation » Miden Assembly » Terms and notations","id":"36","title":"Terms and notations"},"37":{"body":"The design of Miden assembly tries to achieve the following goals: Miden assembly should be an easy compilation target for high-level languages. Programs written in Miden assembly should be readable, even if the code is generated by a compiler from a high-level language. Control flow should be easy to understand to help in manual inspection, formal verification, and optimization. Compilation of Miden assembly into Miden program MAST should be as straight-forward as possible. Serialization of Miden assembly into a binary representation should be as compact and as straight-forward as possible. In order to achieve the first goal, Miden assembly exposes a set of native operations over 32-bit integers and supports linear read-write memory. Thus, from the stand-point of a higher-level language compiler, Miden VM can be viewed as a regular 32-bit stack machine with linear read-write memory. In 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.","breadcrumbs":"User Documentation » Miden Assembly » Design goals","id":"37","title":"Design goals"},"38":{"body":"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. Miden assembly programs are organized into procedures. Procedures, in turn, can be grouped into modules.","breadcrumbs":"User Documentation » Miden Assembly » Code Organization » Code organization","id":"38","title":"Code organization"},"39":{"body":"A procedure can be used to encapsulate a frequently-used sequence of instructions which can later be invoked via a label. A procedure must start with a proc.
Constants

 
Miden assembly supports constant declarations. These constants are scoped to the module they are defined in and can be used as immediate parameters for Miden assembly instructions. Constants are supported as immediate values for the following instructions: push, assert, assertz, asert_eq, assert_eqw, locaddr, loc_load, loc_loadw, loc_store, loc_storew, mem_load, mem_loadw, mem_store, mem_storew.

-
Constants must be declared right after module imports and before any procedures or program bodies. A constant's name must start with an upper-case letter and can contain any combination of numbers, upper-case ASCII letters, and underscores (_). The number of characters in a constant name cannot exceed 100. 

+
Constants must be declared right after module imports and before any procedures or program bodies. A constant's name must start with an upper-case letter and can contain any combination of numbers, upper-case ASCII letters, and underscores (_). The number of characters in a constant name cannot exceed 100.

 
A constant's value must be in the range between  and  (both inclusive) and can be defined by an arithmetic expression using +, -, *, /, //, (, ) operators and references to the previously defined constants. Here / is a field division and // is an integer division. Note that the arithmetic expression cannot contain spaces.

 
use.std::math::u64