Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

High-level type signatures for imports and exports in the Miden package #354

Open
1 task
greenhat opened this issue Nov 14, 2024 · 5 comments
Open
1 task
Assignees
Milestone

Comments

@greenhat
Copy link
Contributor

greenhat commented Nov 14, 2024

Discovered in #353
Ref #346

Why

We need high-level type signatures for linking and cross-context calls to generate lifting and lowering functions for the Miden ABI.
Let's consider the following example:

WIT:

process-list-felt: func(input: list<felt>) -> list<felt>;

Which generates the following Rust bindings:

#[doc(hidden)]
#[allow(non_snake_case)]
pub unsafe fn _export_process_list_felt_cabi<T: Guest>(
    arg0: *mut u8,
    arg1: usize,
) -> *mut u8 {
    #[cfg(target_arch = "wasm32")] _rt::run_ctors_once();
    let len0 = arg1;
    let result1 = T::process_list_felt(
        _rt::Vec::from_raw_parts(arg0.cast(), len0, len0),
    );
    let ptr2 = _RET_AREA.0.as_mut_ptr().cast::<u8>();
    let vec3 = (result1).into_boxed_slice();
    let ptr3 = vec3.as_ptr().cast::<u8>();
    let len3 = vec3.len();
    ::core::mem::forget(vec3);
    *ptr2.add(4).cast::<usize>() = len3;
    *ptr2.add(0).cast::<*mut u8>() = ptr3.cast_mut();
    ptr2
}
#[doc(hidden)]
#[allow(non_snake_case)]
pub unsafe fn __post_return_process_list_felt<T: Guest>(arg0: *mut u8) {
    let l0 = *arg0.add(0).cast::<*mut u8>();
    let l1 = *arg0.add(4).cast::<usize>();
    let base2 = l0;
    let len2 = l1;
    _rt::cabi_dealloc(base2, len2 * 4, 4);
}
pub trait Guest {
    fn process_list_felt(
        input: _rt::Vec<miden::Felt>,
    ) -> _rt::Vec<miden::Felt>;
}

We need to generate lowering and lifting functions for the cross-context calls when process-list-felt
is called from a different package(context).

The process should look like this:

  1. Store the bytes from the caller's memory (pointed by arg0) into the advice provider;
  2. Allocate in the callee memory via callee's exported cabi_realloc and load bytes from the advice
    provider into the callee's(export_process_list_felt_cabi) memory;
  3. Call callee's export function (export_process_list_felt_cabi) passing the pointer to the bytes loaded
    from the advice provider in step 2;
  4. Store the results (returned via a pointer ptr2) into the advice provider;
  5. Release the callee memory allocated for the result by calling post_return_process_list_felt(ptr2);
  6. Allocate and load the bytes from the advice provider into the caller's memory;
  7. Return the pointer to the bytes loaded from the advice provider in step 5 to the caller.

Suggested solution

To store and load bytes to/from the advice provider, we need to provide a high-level type signatures to calculate the byte size of the data to be stored and loaded.
Since we only can do both allocation (step and 6) when linking the caller (we have callee's cabi_realloc exported from their component) we cannot generate the lowering and lifting functions at the time of the caller's compilation.
We generate the exports lifting (CanonLift) part when we compile the exporting code (e.g. an account) and generate the imports lowering (CanonLower) part when we compile the consuming code (e.g. a note) we have everything we need parsed in the frontend. See #357 (comment) for details.
To use the Miden package as a dependency in a Rust project, we need to store the WIT binary in the Miden package so that cargo-miden could expose the WIT file during the rustc compilation.

Pinging @bitwalker

Tasks

Preview Give feedback
@greenhat
Copy link
Contributor Author

greenhat commented Nov 29, 2024

Well, if we generate the exports lowering part when we compile the exporting code (e.g. an account) and generate imports lifting part when we compile the consuming code (e.g. a note) we have everything we need in the Component imports and exports to generate the liftings and lowerings, and we don't need to store the high-level types separately in a Package.

I'm implementing this approach in #357 and will close this issue after it's done.

@bitwalker
Copy link
Contributor

IMO, one of the things I expect us to provide with Miden packages is a WIT description of the component it represents (or something equivalent, but ideally it would actually be WIT, because that would allow downstream tools to generate bindings for the package from that description.

The exported procedures from the MAST will have the component type signature, so we could probably recover most of the WIT that way, if we don't generate it as a distinct item in the package, but that is not as friendly to consume as WIT, and lacks things like custom types, etc.

@bobbinth
Copy link
Contributor

The exported procedures from the MAST will have the component type signature, so we could probably recover most of the WIT that way, if we don't generate it as a distinct item in the package, but that is not as friendly to consume as WIT, and lacks things like custom types, etc.

By "MAST", do you mean MastForest struct or the Library struct? For MastForest, I wasn't thinking we'd have procedure signatures embedded into it. We don't have it for Library either - but I think here they could be added.

@bitwalker
Copy link
Contributor

@bobbinth I was referring to Library here, we have the procedure names there already, but there is no notion of a procedure signature yet in Miden Assembly. Once that is added, then I would push for us to add those to the metadata for Library exports.

Ultimately, we'll need this signature metadata in a Miden package somewhere. In the assembler, there is no awareness of packages currently (AFAIK), only Library (or Program). We probably will need to make the assembler package-aware to handle that being the predominant way of interacting with dependencies, but we still need a way to describe the package being built.

Ideally, that would be in the form of WIT, since it is more precise (and concise). In the near term, assuming types being added to Miden Assembly syntax, we can probably infer basic WIT for a package from a given Miden Assembly source project, but we're lacking tools (like more precise symbol visibility) to do that well, and those limitations may make it difficult to actually derive the WIT (due to unrepresentable exports), or present useful warnings/errors (because we have to ignore things that are unrepresentable). A better solution might be to allow a WIT file to be provided at the project root, and try to infer one otherwise, if types are present.

An important point here though: we can't emit packages without type signatures, as the purpose of the package is to allow consumers to interact with its exports regardless of source language. So while a Library could have exports without signatures, a Package cannot. The benefit of an explicit WIT description is that it can be used to select only the exports corresponding to that description (which by construction are representable in WIT), while leaving the others for internal use. To fully infer WIT for a Miden Assembly project, we'd require:

  1. A particular project structure, which I've outlined here, along with some small tweaks to the structure of LibraryPath
  2. Type signature support in MASM
  3. The addition of internal symbol visibility, for representing module exports visible only within the project. These symbols would not require type signatures to be provided.
  4. All public exports must adhere to what we're calling in the compiler the CanonLift calling convention - which specifies how Canonical ABI types are represented in Miden ABI terms, i.e. data layout in memory, on the operand stack, and in the advice provider where applicable.

And current status of these items:

  1. Trivial
  2. Adding the type system and syntax is easy, and ABI details can be based on the compiler's spec, but there are questions about how we leverage types in the assembler: Are type signatures going to be required? Do we do any form of type checking? Do we want to represent calling conventions explicitly? Regardless of whether we do or not, handwritten Miden Assembly procedures must adhere to some calling convention, and type signatures must convey, in addition to types, the convention in use. This is most important for package exports, but just in general we may want to not only allow specifying other conventions for other use cases, but be able to leverage signatures to derive calling convention code, check programs statically for type violations, etc. In particular, deriving calling convention code is the most crucial IMO, as doing it by hand will be exceedingly error prone.
  3. Easy
  4. This really is a tooling issue. As mentioned above, with type signatures that include a notion of calling convention (that we have specified the details for), we can automatically emit calling convention lifting/lowering in function prologues and at call sites. However, it is still incumbent on the author of any handwritten Miden Assembly procedure to follow the expectations of any given convention, and there are a number of limitations on our ability to statically check those things. Fundamentally though, this is not any different than hand-written assembly code on any other target, you are taking ownership of those details, regardless of how onerous the obligation is.

Anyway, got kind of carried away here, but hopefully that spells out my reasoning a bit better.

@bobbinth
Copy link
Contributor

I was referring to Library here, we have the procedure names there already, but there is no notion of a procedure signature yet in Miden Assembly. Once that is added, then I would push for us to add those to the metadata for Library exports.

I think this makes sense. One thing I'm wonder if with this change, Library basically covers almost everything we care about in the Package. Previously, i was thinking of packages as Library + WIT definitions + some additional metadata, but if we can derive WIT definitions from library metadata, a package just becomes a pretty thin wrapper around the library.

All public exports must adhere to what we're calling in the compiler the CanonLift calling convention - which specifies how Canonical ABI types are represented in Miden ABI terms, i.e. data layout in memory, on the operand stack, and in the advice provider where applicable.

I wonder if this should be a strong requirement. Maybe it is OK to have some public procedures which don't have matching WIT descriptors. These would be "invisible" for the compiler but maybe still accessible via hand-written MASM.

Adding the type system and syntax is easy, and ABI details can be based on the compiler's spec, but there are questions about how we leverage types in the assembler: Are type signatures going to be required? Do we do any form of type checking? Do we want to represent calling conventions explicitly? Regardless of whether we do or not, handwritten Miden Assembly procedures must adhere to some calling convention, and type signatures must convey, in addition to types, the convention in use. This is most important for package exports, but just in general we may want to not only allow specifying other conventions for other use cases, but be able to leverage signatures to derive calling convention code, check programs statically for type violations, etc. In particular, deriving calling convention code is the most crucial IMO, as doing it by hand will be exceedingly error prone.

I think here we start with simpler things and then we expand into more complex things. For example:

  • As the first step, we could add optional signatures to procedures. These then would be used to derive WIT but nothing else.
    -As the next step, we can try to add some type checks to make sure the procedures are called as intended etc.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants