0xPolygonMiden / miden-vm

STARK-based virtual machine
MIT License
630 stars 160 forks source link

Assembler with support for computed offset #638

Open hackaugusto opened 1 year ago

hackaugusto commented 1 year ago

Feature request

It seems all the opcodes that modify the stack use immediate values. So it should be possible to track of a value in the stack, and compute the offset for operations like dup, swap, movup etc. This would make it easier to write largish pieces of assembly and prevent errors.

bobbinth commented 1 year ago

If I understood correctly, this would be like reading the offset off the top of the stack - right? If so, this would be quite difficult to do and probably will require major redesign of the VM (and I'm not sure if performance implications of this will be positive). The primary reason for this is handling of dynamic offsets in AIR constraints.

I'll keep this issue open, in case someone comes up with a clever way to do it in the current design - but it is unlikely to happen in the foreseeable future.

hackaugusto commented 1 year ago

If I understood correctly, this would be like reading the offset off the top of the stack

My suggestion would have no impact on the binary representation or runtime, it should be done by the assembler prior to emitting the binary (well, I guess in our case the AST). The idea would be similar in spirit to what $-$$ achieves in nasm, basically that allows operations to be added or removed from an assembly file, without breaking code, because the assembler computes the offsets for you.

The suggestion here would be similar, but for the offset in the stack. This would have saved me a few hours the last couple of days, because I had added dup somewhere, and missed the update to some movup opcodes.

bobbinth commented 1 year ago

Ah - interesting! I'm still not sure I fully understand how this will look like. Could you give an example?

hackaugusto commented 1 year ago

Suppose we have a small piece of code to load data from memory and add one to the first element of the word:

push.1
padw push.1000 loadw
movup.4 add

And then we remember that we shouldn't consume the element but instead duplicated it prior to adding:

push.1
padw push.1000 loadw
dup movup.4 add

If we forget to update the movup.4 like I have done above, that is a bug. The idea would be to give a tag to some value, maybe like this first@push.1 which basically names the stack position. Then we could write:

first@push.1
padw push.1000 loadw
movup.@first

And when adding the dup we don't have to manually recompute the offsets.

One way of implementing this is to use a simple vector as a stack, give tags to the untagged values, and modify the tag stack as the assemblying happens:

# stack starts empty on the top of a procedure []

# push the tag to the stack [first]
first@push.0

# padw pushes 4 values to the stack, push an unnamed tag for each [t0, t1, t2, t3, first]
padw

# push is only one new items
# [t4, t0, t1, t2, t3, first]
push.1000

# loadw consumes the first element, and replaces the following 4, so the tags must be invalidated
# [t5, t6, t7, t8, first]
loadw

# the tag first is at position 4, so here the assembler computes `moveup.4`
# and its position is updated
# [first, t5, t6, t7, t8]
moveup.@first

In the example above, after adding dup, the tag stack would be [t9, t5, t6, t7, t8, first], the new position of @first is 5, so then the moveup.@first would compute to moveup.5, making it easier to maintain the code.

With this feature, this would fail to assemble:

if.true
  n@push.0 push.1 [n, t1]
else
  push.1 n@push.0 [t2, n]
end

Because at the end of the two blocks, the named tags do not match. For all the control flow blocks the named tags prior to it and after, and the tags on all execution branches, have to match position. Which I believe is correct, because you can't operate on the value n if its position is not consistent. There are some situation were one may want to do that, e.g. when pushing computed values on the bottom of the stack. In that case the feature can not be used.

And operations that consume a value, also consume a tag.

one@push.1 # [one]
push.2 # [one, t1]
add # [t2]

So in the case above the result would have to be retagged one@add.

And we can do this across exec and calls because as far as I know we don't have dynamic dispatch, only static. For dynamic dispatch we could get the same feature if we define a calling convention.

But that is just a suggestion, maybe it doesn't make sense to spend time with this idea and go directly to a proper high level language.