diff --git a/docs/src/design/stack/main.md b/docs/src/design/stack/main.md
index 2b71ce38b..db428f797 100644
--- a/docs/src/design/stack/main.md
+++ b/docs/src/design/stack/main.md
@@ -3,6 +3,7 @@
 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 $2^{32}$), but only the top $16$ items are directly accessible to the VM. Items on the stack are elements in a prime field with modulus $2^{64} - 2^{32} + 1$.
 
 To keep the constraint system for the stack manageable, we impose the following rules:
+
 1. 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.
 2. 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.
 3. 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.
@@ -12,24 +13,28 @@ To ensure that managing stack depth does not impose significant burden, we adopt
 * 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.
 
 ## Stack representation
+
 The VM allocates $19$ trace columns for the stack. The layout of the columns is illustrated below.
 
-![](../../assets/design/stack/trace_layout.png)
+![trace_layout](../../assets/design/stack/trace_layout.png)
 
 The meaning of the above columns is as follows:
+
 * $s_0 ... s_{15}$ are the columns representing the top $16$ slots of the stack.
 * Column $b_0$ 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 $b_0 = 16$.
 * Column $b_1$ 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 $b_1 = 0$, it means that all stack data fits into the top $16$ slots of the stack.
 * Helper column $h_0$ is used to ensure that stack depth does not drop below $16$. Values in this column are set by the prover non-deterministically to $\frac{1}{b_0 - 16}$ when $b_0 \neq 16$, and to any other value otherwise.
 
 ### Overflow table
+
 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](../lookups/multiset.md#virtual-tables). To represent this table, we'll use a single auxiliary column $p_1$.
 
 The table itself can be thought of as having 3 columns as illustrated below.
 
-![](../../assets/design/stack/overflow_table_layout.png)
+![overflow_table_layout](../../assets/design/stack/overflow_table_layout.png)
 
 The meaning of the columns is as follows:
+
 * Column $t_0$ contains row address. Every address in the table must be unique.
 * Column $t_1$ contains the value that overflowed the stack.
 * Column $t_2$ 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$.
@@ -55,15 +60,17 @@ $$
 The initial value of $p_1$ 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), $p_1$ 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.
 
 ## Right shift
+
 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:
 
-![](../../assets/design/stack/stack_right_shift.png)
+![stack_right_shift](../../assets/design/stack/stack_right_shift.png)
 
 Here, we pushed value $v_{17}$ 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, $v_1$ needs to be moved to the overflow table.
 
@@ -71,21 +78,22 @@ To do this, we need to rely on another column: $k_0$. This is a system column wh
 
 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:
 
-![](../../assets/design/stack/stack_overflow_table_post_1_right_shift.png)
+![stack_overflow_table_post_1_right_shift](../../assets/design/stack/stack_overflow_table_post_1_right_shift.png)
 
 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:
 
-![](../../assets/design/stack/stack_overflow_push_2nd_item.png)
+![stack_overflow_push_2nd_item](../../assets/design/stack/stack_overflow_push_2nd_item.png)
 
 Again, as we push $v_{18}$ onto the stack, all items on the stack are shifted to the right, and now $v_2$ 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:
 
-![](../../assets/design/stack/stack_overflow_table_post_2_right_shift.png)
+![stack_overflow_table_post_2_right_shift](../../assets/design/stack/stack_overflow_table_post_2_right_shift.png)
 
 Notice that $t_2$ for row which contains value $v_2$ 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 $s_0, ..., s_{14}$ right by $1$ slot.
 * Add a row to the overflow table described by tuple $(k_0, s_{15}, b_0)$.
@@ -94,9 +102,10 @@ Overall, during a right shift we do the following:
 Also, as mentioned previously, the prover sets values in $h_0$ non-deterministically to $\frac{1}{b_0 - 16}$.
 
 ## Left shift
+
 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:
 
-![](../../assets/design/stack/stack_1st_left_shift.png)
+![stack_1st_left_shift](../../assets/design/stack/stack_1st_left_shift.png)
 
 Overall, during the left shift we do the following:
 
@@ -115,6 +124,7 @@ Overall, during the left shift we do the following:
 If the stack depth becomes (or remains) $16$, the prover can set $h_0$ to any value (e.g., $0$). But if the depth is greater than $16$ the prover sets $h_0$ to $\frac{1}{b_0 - 16}$.
 
 ## AIR Constraints
+
 To simplify constraint descriptions, we'll assume that the VM exposes two binary flag values described below.
 
 | Flag      | Degree | Description                                                                                      |
@@ -125,6 +135,7 @@ To simplify constraint descriptions, we'll assume that the VM exposes two binary
 These flags are mutually exclusive. That is, if $f_{shl}=1$, then $f_{shr}=0$ and vice versa. However, both flags can be set to $0$ simultaneously. This happens when the executed instruction does not shift the stack. How these flags are computed is described [here](./op_constraints.md).
 
 ### Stack overflow flag
+
 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:
 
 $$
diff --git a/docs/src/intro/overview.md b/docs/src/intro/overview.md
index 9059cd717..7e72f54fb 100644
--- a/docs/src/intro/overview.md
+++ b/docs/src/intro/overview.md
@@ -1,11 +1,13 @@
-## Miden VM overview
+# Miden VM overview
+
 Miden VM is a stack machine. The base data type of the MV is a field element in a 64-bit [prime field](https://en.wikipedia.org/wiki/Finite_field) defined by modulus $p = 2^{64} - 2^{32} + 1$. This means that all values that the VM operates with are field elements in this field (i.e., values between $0$ and $2^{64} - 2^{32}$, both inclusive).
 
 Miden VM consists of four high-level components as illustrated below.
 
-![](../assets/intro/vm_components.png)
+![vm_components](../assets/intro/vm_components.png)
 
 These components are:
+
 * **Stack** which is a push-down stack where each item is a field element. Most assembly instructions operate with values located on the stack. The stack can grow up to $2^{32}$ items deep, however, only the top 16 items are directly accessible.
 * **Memory** which is a linear random-access read-write memory. The memory is word-addressable, meaning, four elements are located at each address, and we can read and write elements to/from memory in batches of four. Memory addresses can be in the range $[0, 2^{32})$.
 * **Chiplets** which are specialized circuits for accelerating certain types of computations. These include Rescue Prime Optimized (RPO) hash function, 32-bit binary operations, and 16-bit range checks.
@@ -14,32 +16,37 @@ These components are:
 Miden VM comes with a default implementation of the host interface (with an in-memory advice provider). However, the users are able to provide their own implementations which can connect the VM to arbitrary data sources (e.g., a database or RPC calls) and define custom logic for handling events emitted by the VM.
 
 ## Writing programs
+
 Our goal is to make Miden VM an easy compilation target for high-level languages such as Rust, Move, Sway, and others. We believe it is important to let people write programs in the languages of their choice. However, compilers to help with this have not been developed yet. Thus, for now, the primary way to write programs for Miden VM is to use [Miden assembly](../user_docs/assembly/main.md).
 
 While writing programs in assembly is far from ideal, Miden assembly does make this task a little bit easier by supporting high-level flow control structures and named procedures.
 
 ## Inputs and outputs
+
 External inputs can be provided to Miden VM in two ways:
 
-1. Public inputs can be supplied to the VM by initializing the stack with desired values before a program starts executing. Any number of stack items can be initialized in this way, but providing a large number of public inputs will increase the cost for the verifier.
+1. Public inputs can be supplied to the VM by initializing the stack with desired values before a program starts executing. At most 16 values can be initialized in this way, so providing more than 16 values will cause an error.
 2. Secret (or nondeterministic) inputs can be supplied to the VM via the [*advice provider*](#nondeterministic-inputs). There is no limit on how much data the advice provider can hold.
 
-After a program finishes executing, the elements remaining on the stack become the outputs of the program. Since these outputs will be public inputs for the verifier, having a large stack at the end of execution will increase cost to the verifier. Therefore, it's best to drop unneeded output values. We've provided the [`truncate_stack`](../user_docs/stdlib/sys.md) utility function in the standard library for this purpose.
+After a program finishes executing, the elements remaining on the stack become the outputs of the program. Notice that having more than 16 values on the stack at the end of execution will cause an error, so the values beyond the top 16 elements of the stack should be dropped. We've provided the [`truncate_stack`](../user_docs/stdlib/sys.md) utility procedure in the standard library for this purpose.
 
 The number of public inputs and outputs of a program can be reduced by making use of the advice stack and Merkle trees. Just 4 elements are sufficient to represent a root of a Merkle tree, which can be expanded into an arbitrary number of values.
 
 For example, if we wanted to provide a thousand public input values to the VM, we could put these values into a Merkle tree, initialize the stack with the root of this tree, initialize the advice provider with the tree itself, and then retrieve values from the tree during program execution using `mtree_get` instruction (described [here](../user_docs/assembly/cryptographic_operations.md#hashing-and-merkle-trees)).
 
 ### Stack depth restrictions
+
 For reasons explained [here](../design/stack/main.md), the VM imposes the restriction that the stack depth cannot be smaller than $16$. This has the following effects:
 
-- When initializing a program with fewer than $16$ inputs, the VM will pad the stack with zeros to ensure the depth is $16$ at the beginning of execution.
-- If an operation would result in the stack depth dropping below $16$, the VM will insert a zero at the deep end of the stack to make sure the depth stays at $16$.
+* When initializing a program with fewer than $16$ inputs, the VM will pad the stack with zeros to ensure the depth is $16$ at the beginning of execution.
+* If an operation would result in the stack depth dropping below $16$, the VM will insert a zero at the deep end of the stack to make sure the depth stays at $16$.
 
 ### Nondeterministic inputs
+
 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.
diff --git a/docs/src/intro/usage.md b/docs/src/intro/usage.md
index 9ca9e1db4..d019fdf4d 100644
--- a/docs/src/intro/usage.md
+++ b/docs/src/intro/usage.md
@@ -16,19 +16,19 @@ The above functionality is also exposed via the single [miden-vm](https://crates
 
 To compile Miden VM into a binary, we have a [Makefile](https://www.gnu.org/software/make/manual/make.html) with the following tasks:
 
-```
+```shell
 make exec
 ```
 
 This will place an optimized, multi-threaded `miden` executable into the `./target/optimized` directory. It is equivalent to executing:
 
-```
+```shell
 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:
 
-```
+```shell
 make exec-single
 ```
 
@@ -40,7 +40,7 @@ Internally, Miden VM uses [rayon](https://github.com/rayon-rs/rayon) for paralle
 
 Miden VM proof generation can be accelerated via GPUs. Currently, GPU acceleration is enabled only on Apple Silicon hardware (via [Metal](<https://en.wikipedia.org/wiki/Metal_(API)>)). To compile Miden VM with Metal acceleration enabled, you can run the following command:
 
-```
+```shell
 make exec-metal
 ```
 
@@ -54,13 +54,13 @@ Miden VM execution and proof generation can be accelerated via vectorized instru
 
 To compile Miden VM with AVX2 acceleration enabled, you can run the following command:
 
-```
+```shell
 make exec-avx2
 ```
 
 To compile Miden VM with SVE acceleration enabled, you can run the following command:
 
-```
+```shell
 make exec-sve
 ```
 
@@ -72,7 +72,7 @@ Similar to Metal acceleration, SVE/AVX2 acceleration is currently applicable onl
 
 Once the executable has been compiled, you can run Miden VM like so:
 
-```
+```shell
 ./target/optimized/miden [subcommand] [parameters]
 ```
 
@@ -89,13 +89,13 @@ Currently, Miden VM can be executed with the following subcommands:
 
 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:
 
-```
+```shell
 ./target/optimized/miden [subcommand] --help
 ```
 
 For example:
 
-```
+```shell
 ./target/optimized/miden prove --help
 ```
 
@@ -105,7 +105,7 @@ To execute a program using the Miden VM there needs to be a `.masm` file contain
 
 You can use `MIDEN_LOG` environment variable to control how much logging output the VM produces. For example:
 
-```
+```shell
 MIDEN_LOG=trace ./target/optimized/miden [subcommand] [parameters]
 ```
 
@@ -124,7 +124,7 @@ You can use the run command with `--debug` parameter to enable debugging with th
 As described [here](https://0xpolygonmiden.github.io/miden-vm/intro/overview.html#inputs-and-outputs) 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.
+  - `operand_stack` - can be supplied to the VM to initialize the stack with the desired values before a program starts executing. If the number of provided input values is less than 16, the input stack will be padded with zeros to the length of 16. The maximum number of the stack inputs is limited by 16 values, providing more than 16 values will cause an error.
 - 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.
@@ -135,7 +135,7 @@ As described [here](https://0xpolygonmiden.github.io/miden-vm/intro/overview.htm
 
 _Check out the [comparison example](https://github.com/0xPolygonMiden/examples/blob/main/examples/comparison.masm) 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](../design/stack/main.md#overflow-table).
+After a program finishes executing, the elements that remain on the stack become the outputs of the program. Notice that the number of values on the operand stack at the end of the program execution can not be greater than 16, otherwise the program will return an error. The [`truncate_stack`](../user_docs/stdlib/sys.md) utility procedure from the standard library could be used to conveniently truncate the stack at the end of the program.
 
 ## Fibonacci example
 
diff --git a/miden/README.md b/miden/README.md
index 4ba24e7d5..d0f412950 100644
--- a/miden/README.md
+++ b/miden/README.md
@@ -21,12 +21,12 @@ All Miden programs can be reduced to a single 32-byte value, called program hash
 Currently, there are 3 ways to get values onto the stack:
 
 1. You can use `push` instruction to push values onto the stack. These values become a part of the program itself, and, therefore, cannot be changed between program executions. You can think of them as constants.
-2. The stack can be initialized to some set of values at the beginning of the program. These inputs are public and must be shared with the verifier for them to verify a proof of the correct execution of a Miden program. While it is possible to initialize the stack with a large number of values, we recommend keeping the number of initial values at 16 or fewer as each initial value beyond 16 increases verifier complexity.
+2. The stack can be initialized to some set of values at the beginning of the program. These inputs are public and must be shared with the verifier for them to verify a proof of the correct execution of a Miden program. At most 16 values could be provided for the stack initialization, attempts to provide more than 16 values will cause an error.
 3. The program may request nondeterministic advice inputs from the prover. These inputs are secret inputs. This means that the prover does not need to share them with the verifier. There are three types of advice inputs: (1) a single advice stack which can contain any number of elements; (2) a key-mapped element lists which can be pushed onto the advice stack; (3) a Merkle store, which is used to provide nondeterministic inputs for instructions which work with Merkle trees. There are no restrictions on the number of advice inputs a program can request.
 
 The stack is provided to Miden VM via `StackInputs` struct. These are public inputs of the execution, and should also be provided to the verifier. The secret inputs for the program are provided via the `Host` interface. The default implementation of the host relies on in-memory advice provider (`MemAdviceProvider`) that can be commonly used for operations that won't require persistence.
 
-Values remaining on the stack after a program is executed can be returned as stack outputs. You can specify exactly how many values (from the top of the stack) should be returned. Similar to stack inputs, a large number of values can be returned via the stack, however, we recommend keeping this number to under 16 not to overburden the verifier.
+Values remaining on the stack after a program is executed can be returned as stack outputs. You can specify exactly how many values (from the top of the stack) should be returned. Notice, that, similar to stack inputs, at most 16 values can be returned via the stack. Attempts to return more than 16 values will cause an error.
 
 Having a small number elements to describe public inputs and outputs of a program may seem limiting, however, just 4 elements are sufficient to represent a root of a Merkle tree or a sequential hash of elements. Both of these can be expanded into an arbitrary number of values by supplying the actual values non-deterministically via the host interface.
 
@@ -308,7 +308,7 @@ Miden VM can be compiled with the following features:
 - `executable` - required for building Miden VM binary as described above. Implies `std`.
 - `metal` - enables [Metal](<https://en.wikipedia.org/wiki/Metal_(API)>)-based acceleration of proof generation (for recursive proofs) on supported platforms (e.g., Apple silicon).
 - `no_std` does not rely on the Rust standard library and enables compilation to WebAssembly.
-    - Only the `wasm32-unknown-unknown` and `wasm32-wasip1` targets are officially supported.
+  - Only the `wasm32-unknown-unknown` and `wasm32-wasip1` targets are officially supported.
 
 To compile with `no_std`, disable default features via `--no-default-features` flag.