Communicating with the host

[hackaugusto]

The Miden VM can perform arbitrary computation, that means the user program may create arbitrarily complicated data structures, and it may be useful to communicate the data produced by the Miden execution back to the host.

Here is an small example that builds a Merkle tree and supports an odd number of elements (not properly tested):

Code to build a Merkle tree

#! Initialize the memory to contain a merkle tree
#!
#! input: [tree_addr, ...]
#! output: [...]
proc.init
  # A new tree only needs the element counter to be set to zero. The memory is
  # guaranteed to be initialized to zeros, but it is not know if this address
  # has been used before, so overwrite it with a 0.
  padw movup.4 mem_storew dropw
end

#! This procedure will push a word as an element of the tree.
#!
#! input: [tree_addr, W, ...]
#! output: [...]
proc.add_word
  # load current element count
  dup.0 mem_load

  # update element count to the value after this procedure
  dup.0 add.1 dup.2 mem_store

  # pointer to the end of the structure
  add

  # save the element
  mem_storew

  # clean the stack
  dropw
end

#! This procedure will build the Merkle tree using the data stored in
#! `tree_addr`, after this operation `add_word` may no longer be used.
#!
#! input: [tree_addr, ...]
#! output: [...]
proc.build
  # load bottom layer_size
  dup.0 mem_load

  # special case: nothing to do for an empty or one-element trees
  dup.0 dup.0 mul sub not
  # stack: [is_larger_than_one, read_addr, ...]

  # while the current layer has more than one element 1. merge elements
  # pair-wise 2. if present carry over odd element
  while.true
    # stack: [read_addr, ...]

    dup.0 mem_load
    # stack: [layer_size, read_addr, ...]

    # compute the number of elements pairs in the current layer_size
    dup.0 is_odd dup.0 movdn.3 dup.1 sub div.2
    # stack: [number_pairs, layer_size, read_addr, is_odd, ...]

    # compute the write_addr
    dup.2 movup.2 add
    # stack: [write_addr, number_pairs, read_addr, is_odd, ...]

    # compute the new layer_size
    dup.3 dup.2 add
    # stack: [new_layer_size, write_addr, number_pairs, read_addr, is_odd, ...]

    # save new layer_size to memory
    dup.1 mem_store
    # stack: [write_addr, number_pairs, read_addr, is_odd, ...]

    # prepare stack for inner loop
    movdn.2
    # stack: [number_pairs, read_addr, write_addr, is_odd, ...]

    # loop while there are pairs to be hashed together
    dup.0 neq.0

    while.true
      # stack: [number_pairs, read_addr, write_addr, is_odd, ...]

      movdn.2
      # stack: [read_addr, write_addr, number_pairs, is_odd, ...]

      # load first word
      add.1 dup.0 mem_loadw
      # stack: [A, read_addr+1, write_addr, number_pairs, is_odd, ...]

      # load second word
      dup.4 add.1 mem_loadw
      # stack: [B, A, read_addr+1, write_addr, number_pairs, is_odd, ...]

      # hash elements together
      hmerge
      # stack: [C, read_addr+1, write_addr, number_pairs, is_odd, ...]

      # write to memory
      dup.5 mem_storew dropw
      # stack: [read_addr+1, write_addr, number_pairs, is_odd, ...]

      # update counters (read_addr, write_addr, and number_pairs)
      add.1 swap add.1 movup.2 sub.2
      # stack: [number_pairs-2, read_addr+2, write_addr+1, is_odd, ...]

      # continue while there are pairs of element left to merge
      dup.0 neq.0
    end
    # stack: [0, end_curr_level, end_next_level, is_odd, ...]

    # drop counter and end_next_level
    drop swap drop
    # stack: [end_curr_level, is_odd, ...]

    # copy odd element if needed
    swap
    if.true
      # stack: [end_curr_level, ...]
      dup.0 mem_loadw dup.4 add.1 mem_storew dropw
      
      # update end_next_level to account for the odd element
      add.1
      # stack: [end_curr_level, ...]
    end
    # stack: [end_curr_level, ...]

    # copy odd element
  end
end

Assuming a program like this:

begin
  # add <repeat> leafs to a tree in memory
  padw repeat.7
    add.1 dupw.0            # modify the leaf element and make a copy
    pus.1000 exec.add_word  # push the element to the tree at mem position 1000
  end dropw
  
  # build the merkle tree layers
  push.1000 exec.build
end

At the end of the execution we will have in memory a tree like this:

This discussion is on how to extract that data from the VM's memory into the host program.

[hackaugusto]

I think we can stack this problem like the following:

1. direction of the data
2. structure of the data
3. validation of the data

Each option has stronger features for VM -> Host communication.

Direction

Miden definitely needs a way for the host to inject data into the VM, and this is solved with the Advice provider. However, it is unclear if the other direction from the VM to the host is also required.

In this scenario the VM can not provide data to the host program. The VM execution would represent a state transition function of the host program. The VM's inputs would be something like the hash of the previous state and next, and the VM execution would validate that the protocol invariants are held through the transition. The assumption is that the host program has already executed its progam code, and it only needs to provide to the VM the data it needs to prove the execution was valid w.r.t. its protocol.

Pros

The advantage of not supporting pushing data form the VM to the host is simplicity. In this case there is no need to add instructions to the VM and APIs to the Miden code base for the host to read data.

With this approach even though the VM is capable of running arbitrary computation, the user code would not be structured for that. IOW, the host program would be fully fledged, and run the complete program, and the VM would only run a model that proves the host program was executed correctly. This means the code executed in the VM would be simpler, take fewer cycles and maybe result in better proving performance.

Cons

This effectively means the VM is intended to run a small model of the full program, which means there is a need for two implementations, one in Miden and one in the host program.

Structure

In this scenario Miden would be more than a prover, instead the VM execution would be part of the host program architecture and the host program needs to read data from the VM. For this the VM needs to expose APIs to read data, but the interpretation of the data is left to the host program, i.e. the host program can read bytes &[u8] and the VM is unaware of the structure and invariants of the data. In this case the programmer would be responsible to write correct code, producing a valid encoding of its data structure inside the Miden VM, and the host program would need to read and decode the data.

This is scenario is akin to memory mapping some of the VM's memory on the host.

Pros

The advantage of not having knowledge of the structure in the VM, is that we don't need to add complex APIs to represent this in the VM. We just have to document the APIs to read the VM's memory and leave for the API's user to:

1. Define a convention on memory layout, i.e. memory addresses to read from after the VM execution finished to extract the data
2. Ensure the data is not corrupt and its intended invariant are held.

Cons

This will likely be harder to debug

Validity of the data

In this scenario, not only the Miden program is part of the host architecture, but there are APIs allowing the host to integrate with the VM and validate the data produced during the VM execution. The host program would not need to deserialize data and instead would implement some interface to be plugged in the VM, at the end of the execution the data structures would be available to the host program.

Pros

Perhaps this would be the best programming model if VM -> Host communication is allowed. Assuming debugging would be easier because the Host data structure implementation would validate the data, and the execution would fail on the instruction that produced invalid data

Cons

This is way more complex, and would probably require a lot of work

[hackaugusto]

this has been implemented with events