The power of two operation currently requires 24 constraints (23 after #199). As noted by @bobbinth:

24 constraints is a lot. Granted, these constraints are quite simple, but still for a single pow2 operation feels like a bit of a waste.

Improving this significantly requires coming up with a new construction for the power of two co-processor. The current design is described here and the implementation is located here.

It seems like compiling large scripts (e.g., sha256 in the standard library) takes quite a bit of time. This is especially apparent when running tests in debug mode (which is the default). For example, sha256 tests takes over 40 seconds to complete, and this is likely driven by the assembler. When running tests in release mode, the situation is better - i.e., under 1 second - but still.

We should investigate what is the bottleneck in the assembler and figure out how to address this. My guess is that a big part of this is driven by computing program hash, but would be good to confirm this.

This issue created to discuss contributing guideline details.

I created raw example adapted from template that I found good: https://gist.github.com/4rgon4ut/ae068b84a50c1b8ae66cd127337c1b9a

I have several topics to discuss(@bobbinth):

1. Do we actually need contributing guideline on current stage of the project?

2. Branching. As I see project have active branch named next and we also have gitbook separated branch, I would like to see your thoughts about which details should be represented.

3. Versioning. Looks like semver, but would be nice to clarify.

4. Any other details that should/shouldn't be represented, and guideline structure.

And the last, should I propose raw version to start discussion in proposal page or maybe create discussion in related section?(I mean link to the gist in issue do not looks like best way of doing it)

Partly addresses #138

Adds a utility package to analyse any given script. Takes a source script as a file input and prints the following information.

• [X] Number of VM cycles it takes to execute the script
• [X] Number of NOOPs executed as part of a program

Input: proc.foo.1 pop.local.0 end begin popw.mem.1 push.17 exec.foo end

Output:

Total Number of VM Cycles: 24
Total Number of NOOPs: 1

Hello everyone, I'm new here, trying to use the next branch of midenVM . I have a question which is probably a bit silly. I tried to use Miden (next branch) and found that no matter what program I use, the verification result is Err (VerifierError (InconsistentOodConstraintEvaluations)).

If the program has push operation, i might have the assertion error:

thread 'main' panicked at 'assertion failed: `(left == right)`
left: `QuadExtension(BaseElement(9801321997299852158), BaseElement(10889698089612978941))`,
right: `QuadExtension(BaseElement(1), BaseElement(0))`', /Users/lisalora/.cargo/git/checkouts/miden-4241ff496f7b0a1f/8b07d87/processor/src/trace/utils.rs:188:9

The program i used is as follows:

use miden;
fn main() {
    // or `begin add end`
    let program = "
    begin 
        push.1 
    end";
  
    let options = &miden::ProofOptions::with_96_bit_security();
    let assembler = miden::Assembler::new(true);
    let program = assembler.compile(&program).unwrap();
    let inputs = miden::ProgramInputs::new(&[1,2,3],&[],vec![]).unwrap();

    let num_stack_outputs = 5;
    let proof = miden::prove(&program, &inputs, num_stack_outputs, options);
    let (output, proof) = proof.unwrap();
    let verify_result = miden::verify(program.hash(), &[], &output, proof);
    println!("verify_result is {:?},output is {:?}",verify_result,output);
}

Could somebody possibly tell me whether it is my fault or i used the wrong commit of miden? If the latest commit cannot be verified, what is the latest workable commit? (I want to try some new function of next(such as read-write random-access memory, etc.), rather than the main version)

Thanks for any reply

Tests for boolean and assertion field operations need to be added to the integration tests.

Tests should follow the existing pattern with the following tests added for each of the boolean field operations and the assert operation:

• a test of simple success cases
• a test with applicable failure cases, if there are any (compilation and/or execution failure)
• ~a proptest of the expected success case~ (removed as it's not necessary)

The u32 bitwise tests provide an example.

Specs for the operations are in the Miden Assembly note.

The field operations which are missing tests are:

• [ ] assert
• [ ] not
• [ ] and
• [ ] or
• [ ] xor

More information can also be seen in the field_ops assembly parsers.

Here I implement field arithmetic for extension field GF(p^5) | p = 2^64 - 2^32 + 1 ( = Miden base field prime ).

This works follows paper https://eprint.iacr.org/2022/274 - I suggest you read that for having a better context. Reference implementation https://github.com/pornin/ecgfp5/tree/ce059c6 is also used quite often.

Routine | Cost ( VM cycles ) --- | --: Addition | 20 Subtraction | 26 Multiplication | 143 Squaring | 88 Inversion | 399 Division | 561

Currently, two crates generate executable files: examples and tools. Both use functionality exposed by the miden crate, which in turn uses processor crate and verifier crate.

This seems like a fairly confusing arrangement, and it will probably get even more confusing as we add more things (e.g., repl tool). So, I'd like to see if we can re-shuffle things a bit to make the structure more intuitive.

One option is to do something like this:

1. Create a prover crate which will expose a prove() function. This function will execute programs and generate proofs of their execution (basically the same as the current execute() function in the miden crate). This will be consistent with having the verifier crate.
2. Change miden crate to output an executable. This executable would be used to run Miden VM from the command line in various modes. This will also allow us to get rid of tools create and probably examples crate as well.

The potential modes of miden executable could be as follows:

• miden run - execute a program and generate an output
• miden prove - execute a program and generate a proof
• miden verify - verify a previously generated proof
• miden analyze - run a script analysis tool
• miden repl - start Miden REPL

We still need to figure out how to provide inputs and read outputs for each mode. For example, for miden prove we could do something like this:

miden prove [path to .masm script file] -i [path to an input file] -n [number of outputs] -p [proof options] -o [output file name]

But much more thinking is needed about how to structure these.

We should start thinking about how each operation should be encoded (right now we basically assign dummy opcodes to operations). There are many things to consider, but for now, I'll just describe the basics.

First, we want to encode each operation with no more than 7 bits. This also means that within the VM we allocate 7 columns for operation bits (or op_bits). Theoretically, we could encode up to 128 different operations using seven bits - but this is not desirable for a number of reasons:

1. 128 is a large number and we'd like to keep the number of operations as small as possible (while not giving up expressivity).
2. With 128 operations, each operation flag would have degree 7. While this should work for most operations, it won't work for all (e.g., many control flow operations should have degree 5, or we'll need to introduce extra columns for degree reduction).

If we keep the number of operations to at most 96, we can create several classes of operations. Consider the following arrangement:

| bit 6 | bit 5 | bit 4 | bit 3 | bit 2 | bit 1 | bit 0 | # of ops | degree | | :---: | :---: | :---: | :---: | :----: | :---: | :---: | :-------: | :------: | | 0 | x | x | x | x | x | x | 64 | 7 | | 1 | 0 | 0 | x | x | x | x | 16 | 7 | | 1 | 0 | 1 | x | x | x | - | 8 | 6 | | 1 | 1 | x | x | x | - | - | 8 | 5 |

In the above, any opcode which starts with 0 can use all of the following 6 bits and thus we get 64 total opcodes and degree of each opcode is 7. Opcodes which start with 100 work in the same way.

However, for opcodes which start with 101 we allow using only 6 bits total. Thus, we can encode 8 opcodes, and degree of each opcode will be 6. We apply the same logic to opcodes which start with 11 but for these opcodes we allow using only 5 bits total. We still can encode 8 opcodes, but the degree of each of these opcodes is now 5.

To summarize, with this arrangement, we get 3 classes of opcodes:

• 80 opcodes of degree 7
• 8 opcodes of degree 6
• 8 opcodes of degree 5

Having had the benefit of writing some simple (and not so simple) programs in Miden assembly, I think there are some opportunities to simplify (and in some cases augment) current assembly instruction set. My thoughts are below - though, these are rather preliminary and many of them might not be a good idea.

Field operations

All looks good here. There is one slightly inconsistent thing in comparison operations: eq and neq operations allow for immediate parameters, while other comparison operations do not. The primary reason for allowing immediate parameters for eq is that eq.0 gets reduced to EQZ VM operation. And if we introduce eqz assembly instruction we could remove immediate parameters from eq (and neq) operation. But I'm not sure if this is a big deal.

u32 operations

I'd love to adopt the same naming convention as we used in u64 stdlib module. For example, we could do something like this:

• u32add -> u32add.checked
• u32add.unsafe -> u32add.overflowing
• u32add.full could be eliminated

But, in this case, it is not clear how to handle immediate values. For example, u32add.checked.5 looks odd to me. And supplying immediate values to "checked" variants may be desirable because we can check whether the parameter is a valid u32 value at compile time pretty easily.

A few other thoughts in u32 category:

• We could probably get rid of safe versions of u32addc and u32madd and have just u32addc.unchecked and u32madd.unchecked.
• We could replace u32addc with u32add3 which would compute a sum of top 3 elements on the stack (and thus would be a more general version of u32addc). To do this, we'd need to think through how the AIR constraints would need to be changed.
• We could replace u32div.full with u32divmod - this would be consistent with the approach used in u64 module.
• Depending on what we do with eq and neq, we could also update u32eq and u32neq.

Stack manipulation

One thing that bothers me somewhat here is that some operations have different costs and these costs are not intuitive. For example:

• dup.7 takes 1 VM cycles, but dup.8 takes 3, and then dup.9 takes 1 VM cycle again. Same goes for movup and movdn.
• Some swap operations take 2 cycles while others take 4.

Thus, writing efficient code requires deep understanding of costs of each operations.

One solution to this could be to get rid of the operations which take multiple cycles. But this reduces future flexibility and I'm not sure it's worth it. We could also do some selective simplifications. For example:

• Get rid of swap operations since they are always emulated using other ops anyway.
• Refactor operations to have a more consistent cost model. For example, general rule could be at accessing the first 8 elements of the stack (e.g., via movup or movdn instructions) always take 1 VM cycle, and then accessing elements 8 - 16 is more expensive (e.g., 3 - 4 VM cycles).

Input operations

Similar to the above, the cost model for these operations requires deep knowledge. E.g., it is not obvious that storew.mem is 4x faster than popw.mem. But short of getting rid of these composite operations, I'm not sure what can be done.

On rebasing from the latest next branch, we see some issues when trying to execute some miden program which seems to be working earlier with no hiccups.

@Al-Kindi-0 highlighted this issue when he was running fri_fold2_ext2 test. Steps to reproduce the error:

1. Go to the following commit in Al's miden fork
2. If you run cargo test fri_fold2_ext2, the program will get executed, but the final stack will not match as the expected stack is not what is written in the test yet. But if we uncomment the part and rerun the test, the test fails even before and returns the following error:

running 1 test
thread 'stdlib::crypto::fri::fri_fold2_ext2' panicked at 'called `Result::unwrap()` on an `Err` value: NotU32Value(BaseElement(6666087519483434683))', miden/tests/integration/helpers/mod.rs:189:36
stack backtrace:

3. We observed a weird thing when we tried to add some redundant code(which doesn't affect the program) in the proc, e.g., push.3 drop, the program was still failing. When we inlined this procedure and used it directly in test program, the test compiled.

The following is working:

use.std::crypto::fri
 begin
          exec.fri::preprocess
          dup                         #[add_i,add_i,num_q,d,g,t_d,add_f,...]
          movdn.6                     #[add_i,num_q,d,g,t_d,add_f,add_i,...]
          mem_storew                  #[num_q,d,g,t_d,...]
          push.0.0.0
          adv_loadw                   #[0,p,e1,e0,d,g,t_d,...]
          drop                        #[p,e1,e0,d,g,t_d,...]
          dup                         #[p,p,e1,e0,d,g,t_d,...]
          movup.5                     #[g,p,p,e1,e0,d,t_d,...]
          swap                        #[p,g,p,e1,e0,d,t_d,...]
          exp.u32 
          push.4
          drop
 end

whereas the following is not:

 use.std::crypto::fri
 begin
        exec.fri::preprocess
        exec.fri::verify_fri
 end

export.verify_fri
    dup                         #[add_i,add_i,num_q,d,g,t_d,add_f,...]
    movdn.6                     #[add_i,num_q,d,g,t_d,add_f,add_i,...]
    mem_storew                  #[num_q,d,g,t_d,...]
    push.0.0.0
    adv_loadw                   #[0,p,e1,e0,d,g,t_d,...]
    drop                        #[p,e1,e0,d,g,t_d,...]
    dup                         #[p,p,e1,e0,d,g,t_d,...]
    movup.5                     #[g,p,p,e1,e0,d,t_d,...]
    swap                        #[p,g,p,e1,e0,d,t_d,...]
    exp.u32                #[poe,p,e1,e0,d,t_d,...]
    push.4
    drop        
end

As part of CI/CD we are running

cargo clippy --all -- -D clippy::all -D warnings

Inspired by that, we can ask clippy to also suggest a few additional fixes:

cargo clippy --all --fix --allow-dirty -- -D clippy::all -D warnings

Most changes are quite trivial (but make the code a bit cleaner), but have a look at miden/tests/integration/stdlib/math/ecgfp5/group.rs for the one non-trivial refactor.

In MVM assembler you can say

use.std::math::u64

begin
    push.1.0
    push.2.0
    exec.u64::checked_add
end

[From the manual]

Here std,math etc are identifiers. Notice no quotes around the names. Therefore they should be declared/defined somewhere. Hence I propose the MVM Assembler parser be modified to accept these "instructions" and initial just forget them:

• program.name
• module.libname.modname

For my research tool i will process files with multiple libraries, modules, and programs, all at once (because for testing, you don't want to stuff about with search paths and multiples files).

There is no library instruction, a library is formed implicitly by using multiple modules with the same libname. MVM Assembler could enforce more stringent requirements. For example, using program.name allows to start checking for illegal exports.

This commit introduces a change of the advice provider to be a trait. It also provides a standard implementation BaseAdviceProvider.

It splits the initialization of the stack from the inputs of the advice provider.

Pending

• [ ] Should we deprecate ProgramInputs?
• [ ] Should we change the VM clock to be an internal implementation detail instead of setting it into the advice provider?
• [ ] Enable the ignored tests (must be done after the pending topics are resolved)

Here we remove a few limitations to allow empty blocks.

This PR implements https://github.com/0xPolygonMiden/miden-vm/issues/585 and will make the job for programmatic generators of Miden Assembly easier.

Describe your changes

Addressing #446.

Checklist before requesting a review

• Repo forked and branch created from next according to naming convention.
• Commit messages and codestyle follow conventions.
• Relevant issues are linked in the PR description.
• Tests added for new functionality.
• Documentation/comments updated according to changes.

Describe your changes

This patch applies a tweak to the hashing function used for MAST nodes to ensure different node types hash to different values. This ensures that the simple exploit from #605 is no longer sufficient to subvert the verification process.

The hashes themselves are transformed by a simple transformation by postmultiplying by a constant chosen based on the node type. This prevents different node types from hashing to the same value. These coefficients were arbitrarily chosen to be sequential primes. 2 was avoided in case the base hash ever switches from elements to something in base "user" numerical range 2^32. Rescue-Prime should by the strong hashing assumption have no meaningful interactions with multiplication by a non-0 constant.

Further, syscalls and calls now hash to different values.

Documentation has been updated to reflect the change.

Checklist before requesting a review

• Repo forked and branch created from next according to naming convention.
• Commit messages and codestyle follow conventions.
• Relevant issues are linked in the PR description.
• Tests added for new functionality.
• Documentation/comments updated according to changes.