Skip to content

Commit

Permalink
Update Makefile and usage.md with nextest + build commands
Browse files Browse the repository at this point in the history
  • Loading branch information
phklive committed Jun 18, 2024
1 parent b005e53 commit be89e11
Show file tree
Hide file tree
Showing 2 changed files with 75 additions and 35 deletions.
16 changes: 12 additions & 4 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -41,20 +41,28 @@ lint: format fix clippy ## Runs all linting tasks at once (Clippy, fixing, forma

.PHONY: test
test: ## Runs all tests
$(DEBUG_ASSERTIONS) cargo test --profile test-release --features internals
$(DEBUG_ASSERTIONS) cargo nextest run --cargo-profile test-release --features internals

# --- docs ----------------------------------------------------------------------------------------

.PHONY: doc
doc: ## Generates & checks documentation
doc: ## Generates & checks documentation
$(WARNINGS) cargo doc --all-features --keep-going --release

# --- building ------------------------------------------------------------------------------------

.PHONY: build
build: ## Builds VM with default profile and features
build: ## Builds VM with optimized profile and features
cargo build --profile optimized $(FEATURES_CONCURRENT_EXEC)

.PHONY: build-single
build-single: ## Builds VM in single-threaded mode
cargo build --profile optimized --features executable

.PHONY: build-release
build-release: ## Builds VM with release mode and no optimizations
cargo build --release $(FEATURES_CONCURRENT_EXEC)

.PHONY: build-metal
build-metal: ## Builds VM for metal
cargo build --profile optimized $(FEATURES_METAL_EXEC)
Expand All @@ -75,4 +83,4 @@ build-info: ## Builds VM with log tree

.PHONY: bench
bench: ## Runs VM benchmarks
cargo bench --profile optimized
cargo bench --profile optimized
94 changes: 63 additions & 31 deletions docs/src/intro/usage.md
Original file line number Diff line number Diff line change
@@ -1,124 +1,156 @@
# Usage

Before you can use Miden VM, you'll need to make sure you have Rust [installed](https://www.rust-lang.org/tools/install). Miden VM v0.9 requires Rust version **1.75** or later.

Miden VM consists of several crates, each of which exposes a small set of functionality. The most notable of these crates are:
* [miden-processor](https://crates.io/crates/miden-processor), which can be used to execute Miden VM programs.
* [miden-prover](https://crates.io/crates/miden-prover), which can be used to execute Miden VM programs and generate proofs of their execution.
* [miden-verifier](https://crates.io/crates/miden-verifier), which can be used to verify proofs of program execution generated by Miden VM prover.

- [miden-processor](https://crates.io/crates/miden-processor), which can be used to execute Miden VM programs.
- [miden-prover](https://crates.io/crates/miden-prover), which can be used to execute Miden VM programs and generate proofs of their execution.
- [miden-verifier](https://crates.io/crates/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](https://crates.io/crates/miden-vm) crate, which also provides a CLI interface for interacting with Miden VM.

## CLI interface

### Compiling Miden VM

To compile Miden VM into a binary, we have a [Makefile](https://www.gnu.org/software/make/manual/make.html) with the following tasks:

```
make exec
make build
```

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
make build-single
```

For a faster build, you can compile with less optimizations, replacing `--profile optimized` by `--release`. Example:

```
cargo build --release --features concurrent,executable
make build-release
```

In this case, the `miden` executable will be placed in the `./target/release` directory.

### Controlling parallelism

Internally, Miden VM uses [rayon](https://github.com/rayon-rs/rayon) for parallel computations. To control the number of threads used to generate a STARK proof, you can use `RAYON_NUM_THREADS` environment variable.

### GPU acceleration
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:

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:

```
make exec-metal
make build-metal
```

Similar to `make exec` command, this will place the resulting `miden` executable into the `./target/optimized` directory.
Similar to `make build` 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.

### SIMD acceleration
Miden VM execution and proof generation can be accelerated via vectorized instructions. Currently, SIMD acceleration can be enabled on platforms supporting [SVE](https://en.wikipedia.org/wiki/AArch64#Scalable_Vector_Extension_(SVE)) and [AVX2](https://en.wikipedia.org/wiki/Advanced_Vector_Extensions#Advanced_Vector_Extensions_2) instructions.

Miden VM execution and proof generation can be accelerated via vectorized instructions. Currently, SIMD acceleration can be enabled on platforms supporting [SVE](<https://en.wikipedia.org/wiki/AArch64#Scalable_Vector_Extension_(SVE)>) and [AVX2](https://en.wikipedia.org/wiki/Advanced_Vector_Extensions#Advanced_Vector_Extensions_2) instructions.

To compile Miden VM with AVX2 acceleration enabled, you can run the following command:

```
make exec-avx2
make build-avx2
```

To compile Miden VM with SVE acceleration enabled, you can run the following command:

```
make exec-sve
make build-sve
```

This will place the resulting `miden` executable into the `./target/optimized` directory.

Similar to Metal acceleration, SVE/AVX2 acceleration is currently applicable only to recursive proofs which can be generated using the `-r` flag.

### Running Miden VM

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](../design/programs.md)) and outputs stats about the compilation process.
* `debug` - this will instantiate a [Miden debugger](../tools/debugger.md) 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](../tools/repl.md) tool.
* `example` - this will execute a Miden assembly example program, generate a STARK proof of execution and verify it. Currently it is possible to run `blake3` and `fibonacci` examples.

- `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](../design/programs.md)) and outputs stats about the compilation process.
- `debug` - this will instantiate a [Miden debugger](../tools/debugger.md) 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](../tools/repl.md) tool.
- `example` - this will execute a Miden assembly example program, generate a STARK proof of execution and verify it. Currently it is possible to run `blake3` and `fibonacci` examples.

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.

#### Enabling logging

You can use `MIDEN_LOG` environment variable to control how much logging output the VM produces. For example:

```
MIDEN_LOG=trace ./target/optimized/miden [subcommand] [parameters]
```
If the level is not specified, `warn` level is set as default.

If the level is not specified, `warn` level is set as default.

### Inputs

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.
* 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).
- 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](https://github.com/0xPolygonMiden/examples/blob/main/examples/comparison.masm) to see how secret inputs work.*
_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).

## Fibonacci example

In the `miden/examples/fib` directory, we provide a very simple Fibonacci calculator example. This example computes the 1001st term of the Fibonacci sequence. You can execute this example on Miden VM like so:

```
./target/optimized/miden run -a miden/examples/fib/fib.masm -n 1
```

This will run the example code to completion and will output the top element remaining on the stack.

If you want the output of the program in a file, you can use the `--output` or `-o` flag and specify the path to the output file. For example:

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

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

0 comments on commit be89e11

Please sign in to comment.