Polybase feedback

[calummoore]

We're currently building/compiling our Polybase language (based on typescript) to miden assembly.

Firstly, Miden has been incredible to work with, it's amazing what we can already build with it 🔥. Just wanted to share some feedback on our experience working with it.

In order of priority (from our side).

1. Named breaks

Currently there is no way to break early from code, other than using lots of nested if statements.

Current solution for break in loops

# let i = 0;
# while (true) {
#   if (i > 0) {
#     break;
#   }
#   
#   i = i + 1;
# }

begin
    push.0 # value for variable i
    mem_store.1

    push.1
    mem_store.2 # no_break

    while.true
        mem_load.1
        push.0
        gt
        if.true
            push.0
            mem_store.2 # no_break = 0, break
            drop
        end

        mem_load.2
        if.true
            mem_load.1
            push.1
            add
            mem_store.1
            drop
            push.1
        end

        mem_load.2
    end
end

Current solution for early return

# ...
# if (a < 10) {
#   return 10
# }
# ... rest of code

begin
    ...
   if.true
      // rest of code
   end
   push.10
end

Our recommendation, would be to have named break clauses, that allow for breaking within a given block of code. This would enable us to skip blocks of code more easily, and thus implement better throw, return, continue and break logic.

You could achieve this by adding two new commands: block.<name> and break.<name>. This is similar block in WebAssembly.

block.blockA
  push.1
  while.true
    break.blockA
  end
end
// break.blockA would move us here
push. ...

This would also allow us to inline our functions, instead of using procedures. Inlining functions lets us move values around less and optimise things like shift right to use a constant (compile time known) value instead of reading from stack (4 cycles vs 40 cycles).

2. Float32

We can obviously achieve this currently, but I think a lot of optimisation could be done if this was handled by the miden assembly.

3. Miden verification (verify proofs in miden)

This would allow us to:

• create recursive proofs
• run multiple proofs in parallel and then combine them, which could be used to optimize perf or reduce proof size

4. Recursive proc calls

We're unsure how we would be able to do this with the current miden assembly.

5. Advice tape to memory

A lot of the time we are moving data from the advice tape to memory, as the VM can only access the head of the tape. It would be useful to be able to optimise this process if possible.

Currently in order to move from advice tape to memory we use adv_push.n and then mem_store. It would be great to have a single command to move multiple values into the store at once, so instead of:

adv_push mem_store.1 drop adv_push mem_store.2 drop we could have adv_to_mem.2.1 where 2 is the number of field elements to read and 1 is the start addr. It might only be worth doing this if we can reduce the no. of cycles.

6. movup.n

movup.n (and associated cmds) currently only allow to move values from the top 16 items in the stack. This means we have to move more values into memory rather than keeping them in the stack. Now that the stack can be >16, it would be good to be able to use these values by bringing them to the head.

7. Mem store + drop

A variant of mem_store that swallows/drops the value stack element, i.e. equivalent of mem_store drop. As we usually don't need the value immediately after its been put into memory.

8. Int32

Currently we only have unint variants, would be helpful to have an int version. We have already implemented this, but again, I'm sure it would be more performant if it was handled by the compiler.

---

Let me know if you have any questions, or if anything is unclear!

[grjte]

Hey @calummoore thanks so much your feedback! It's great to hear you're enjoying using Miden & also great to get concrete suggestions.

1. Named breaks

As you've pointed out, this would be useful, and I like your suggestion to follow the Web Assembly block model with block.<name> and break.<name>.

However, it would be quite a bit of effort to implement, so it's something we were planning to deal with at a higher language level. If you guys have the bandwidth to work on it, the PR would be very welcome and we'd be happy to discuss and provide guidance throughout.

Since it's your top priority, maybe this makes sense for you - if you want to go for it, feel free to open an issue and we can move future discussion there.

2. Float32

Floating point emulation support would be good to add, but we'd prefer to add this to the standard library rather than to the assembly instruction set.

There's also the question of what your needs are here - do you need true IEEE standard float support or is it sufficient to have some fixed point ops?

Let's move this to an issue - can you create one with a bit more detail about your needs?

3. Recursive proof verification

We're working on this! 🎉 We need a few more things in AirScript before we can finish this though.

We're working on improving the transparency of our roadmap & releases, so expect info about the status/progress of this to be more available in the coming weeks. I can update here once that's happened.

4. Recursive proc calls

This would be possible to do, but it's really complicated, so it's not something we can focus on at the moment unfortunately.

5. Advice tape to memory

We ran into this too and closed an issue on it this week!

We've added adv_pipe. Check it out in the docs and let us know if you have questions. (The issue provides good context too.)

6. movup.n for n > 15

This is difficult to do and probably not worth it at this point. If the main benefit is to manipulate the stack more easily and use memory less then maybe program restructuring can achieve the same goal. @itzmeanjan has done a bunch of miden assembly work on the stdlib hash functions including several rounds of optimizations and can maybe share some general thoughts.

7. mem_store + drop

Actually, we'd be ok with changing mem_store completely so that the value is popped off the stack and stored. This makes sense, since mem_load pushes onto the stack, so they would mirror each other.

However, we could also just do as you've suggested and add another variation.

Let's move this discussion to an issue as well - I've opened #500

8. Int32

Similar to floats - we'd prefer to do this at the stdlib level.

Please feel free to open an issue where we can discuss more.

[calummoore]

1. Named breaks

Created a ticket for this #519 🔥

2. Float32

I'm not really a fan of fixed point floats, because if you're going to do that, you may as well just use an int and manually keep track of the decimal.

Let's see how much of a performance blocker this actually becomes when we start seeing programs. We're going to be doing some benchmarking, so will let you know the results of that too.

3. Recursive proof verification

Great, look forward to seeing that. If we can do anything to help, let us know. We should have probably ranked this slightly higher on the priority list. 😅

4. Recursive proc calls

Makes sense, we can actually get around this if we have the above 👍

5. Advice tape to memory

🔥🎉🚀🔥🎉🚀🔥🎉🚀🔥🎉🚀

6. movup.n for n > 15

I had a feeling this would be the case, are things outside of the top 16 stack essentially just stored in memory anyway?

7. mem_store + drop

We're happy with either approach, I can't see a big use case for keeping it in scope tbh, but also changing it would be a breaking change.

8. Int32

As per 2.

[grjte]

3. Recursive proof verification
   If we can do anything to help, let us know.

Sure! We should have our next steps sketched out in the repo next week. I'll update here, and then you guys can join the discussion and decide how involved you want to be.

2. Float32 (and 8. Int32)
   Let's see how much of a performance blocker this actually becomes when we start seeing programs. We're going to be doing some benchmarking, so will let you know the results of that too.

Sounds good on both counts - we'd be looking at this for stdlib down the line anyway, so we can revisit whenever. It'll be awesome to get benchmark results when you have them

6. movup.n for n > 15
   I had a feeling this would be the case, are things outside of the top 16 stack essentially just stored in memory anyway?

No, actually stack items after the top 16 are no longer stored in the main execution trace. We put them into a "virtual table", and we maintain consistency using multiset checks on a column in an "auxiliary" trace that we build after committing to the main trace using randomness we get from the verifier. (This may be familiar, since I used our stack overflow virtual table as an example in my zkSummit talk about multiset checks in STARKs)

The complexity of doing this would be in the constraints. It's straightforward to enforce constraints against the top 16 stack items because they're all in the main trace. However, if we need to take something out of the virtual table (at an arbitrary row) and put something else into it, then the constraints become more complex and likely higher degree so that we'd have to add another column for degree reduction, etc. The cost doesn't seem worth it in terms of both increased complexity and loss of performance.

7. mem_store + drop
   We're happy with either approach, I can't see a big use case for keeping it in scope tbh, but also changing it would be a breaking change.

Yes, exactly :) I'm going to move this point to the discussion in that issue so the context stays together.