Skip to content

reboot interleaving spec and instrument rt next - #185

Draft
ecioppettini wants to merge 27 commits into
mainfrom
enzo/reboot-interleaving-spec-and-instrument-rt-next
Draft

reboot interleaving spec and instrument rt next#185
ecioppettini wants to merge 27 commits into
mainfrom
enzo/reboot-interleaving-spec-and-instrument-rt-next

Conversation

@ecioppettini

Copy link
Copy Markdown
Contributor

(still WIP/experimental)

Adds a new "interleaving" spec for the (still non existing) new circuit.

The reason for this is not that the existing circuit is necessarily wrong, a lot of the code will just be re-used, but the idea is to write something closer to the current state of the compiler + runtime, now that we have the first designs of actual execution.

The core part of this PR is the starstream-interleaving-spec/spec/starstream.qnt file.

It's role is the one that interleaving/starstream-interleaving-spec/EFFECTS_REFERENCE.md currently has (now renamed to starstream-interleaving-spec-legacy), plus the mocked_verifier.rs in that package (which is a transliteration of the markdown spec)

The reasoning for using quint is that

  • Unlike markdown, it is a formal language, so it can be parsed + typechecked
  • As a specification language, is good to specify the "what" instead of the "how", which is what a zk circuit would run.
  • It can be used to generate tests, or for testing traces. Currently the traces generated from the instrumented runtime run through the spec for validation (the other direction is slightly harder because it would require generating a starstream program out of the host call traces)
  • It's a really simple language, so rewriting it in lean or other formalization won't probably be a big issue anyway.

Extra notes:

This has some unrelated changes to the compiler and runtime. Mostly of things I needed to be able to get a somewhat interesting example to run.

The abis-clear was based on this Discord discussion

For now it's mainly a temporary patch, but the reason for it still stands.

This also removes the runtimes in interleaving. I don't think those are worth keeping at this stage, we lose some small test coverage, but for a circuit/set of instructions that will get rewritten anyway. They were mainly useful for exploration of the problem. Still keeping the circuit code and the ledger specs as a reference.

@ecioppettini ecioppettini self-assigned this Jul 31, 2026
Comment on lines +103 to +127
// TODO: The hook receives the newly created component `Instance`, but
// Wasmtime currently has no API for obtaining the core debug instances
// instantiated underneath it. Until it does, scan the entire store and
// require exactly one core instance without registered trace state. This
// detects uninstrumented contracts, but the repeated full-store scan still
// makes n component instantiations cumulatively O(n²). Ideally Wasmtime
// would expose the component-to-core relationship (for example,
// `Instance::debug_core_instances`), allowing direct registration here.
let core_instances = store.as_context_mut().debug_all_instances();
let unregistered_core_instances = core_instances
.into_iter()
.filter(|instance| {
store
.data()
.wasm_trace_state(instance.debug_index_in_store())
.is_none()
})
.collect::<Vec<_>>();
let [core_instance] = unregistered_core_instances.as_slice() else {
bail!(
"instruction tracing requires exactly one unregistered core instance after component \
instantiation, but found {}",
unregistered_core_instances.len()
)
};

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rvolosatovs this is low priority, but maybe you have any thoughts on this.

basically the tracer needs to know which core instance corresponds to which core program/source code

if you are running plain core wasm, normally you call instantiate and you can just attach the program metadata to that instance id

the problem is that a component instance is different from a core instance

because of this, here I'm basically doing:

-> instantiate component -> loop through all the current (core) instances -> find which one still does not have source metadata attached

this works, but feels kind of hacky, and also doesn't support the case where a component has more than one core module inside

@rvolosatovs rvolosatovs Jul 31, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks like you could use https://docs.rs/wasmtime/latest/wasmtime/struct.Store.html#method.debug_register_component before instantiation, which will internally call https://docs.rs/wasmtime/latest/wasmtime/struct.Store.html#method.debug_register_module per each module in the component. This way you can establish the module -> component mapping.

At a later point you could maybe get the module of the instance through https://docs.rs/wasmtime/latest/wasmtime/struct.Instance.html#method.module and maybe use https://docs.rs/wasmtime/latest/wasmtime/struct.Module.html#method.same to establish a mapping from instance -> component

Would that work?

Comment on lines +202 to +204
let mut target_params = params.to_vec();
target_params[0] = Val::Resource(utxo.resource());
f.call_async(&mut store, &target_params, results).await?;

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think the implementation should be cloning the parameters and/or modifying them in any way. Why is this required?

Comment thread starstream-runtime-next/src/lib.rs Outdated
Comment on lines +877 to +882
let (_, index) = self
.component
.get_export(Some(&self.instance_idx), name)
.context("function export not found in UTXO instance")?;
self.instance
.get_func(store, name)
.get_func(store, index)

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this should be redundant, name should already carry the instance information. This lookup happens ahead-of-time

Comment thread starstream-runtime-next/src/lib.rs Outdated
Comment on lines +839 to +840
component: Component,
instance_idx: ComponentExportIndex,

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we should not need these, the export information is stored in the various *Export structs

pub struct ConstructorExport {
ty: types::ComponentFunc,
idx: ComponentExportIndex,
instance_idx: ComponentExportIndex,

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The idx should already encode this

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

that's the constructor idx, not the utxo idx (which obviously doesn't make sense to have here of course)

tbh most of the change to this package were AI, and I didn't particularly pay that much attention to it because I was planning on dropping these (that's why I labelled the commit as tmp?). Same for the compiler changes.

the reason for this is that I wanted a test case of a coord script calling a utxo method (kind of dynamic dispatch, let's say?), which was not supported, so I hacked it together with a handwritten example.

this was added here to pass it down, to eventually be able to resolve the function from it by its name...

I guess there could be a pre-resolution step at some point and a lookup from the string out of it

In my case I just needed something to start playing around with the import/export instrumentation.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can use get_utxo_method to get the export index by name

/// Get a method of an exported UTXO by name
#[instrument(level = "trace", skip_all)]
pub fn get_utxo_method(&self, utxo: &UtxoExport, name: &str) -> wasmtime::Result<MethodExport> {
let types::ComponentExtern { ty, .. } = utxo
.instance_ty
.get_export(self.pre.engine(), name)
.context("export not found")?;
let types::ComponentItem::ComponentFunc(ty) = ty else {
bail!("export is not a function")
};
self.get_utxo_method_typed(utxo, name, ty)
}

The key point is that the idx stored here uniquely identifies the export on the component, the instance index is irrelevant for the lookup. You do need the instance index if you are doing a string lookup, of course, but this API exists precisely to avoid string lookups.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, I guess this needs to be exposed through UtxoHandler so that this function can reach that function somehow? Instead of putting it into the resource.

pub fn link_utxo_function<T: UtxoHandler>(

I'll assess this later, although maybe things will change again before I get to that

@rvolosatovs rvolosatovs Jul 31, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ty: types::Record,
get: ComponentExportIndex,
set: ComponentExportIndex,
instance_idx: ComponentExportIndex,

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same as in others, this should be redundant

Comment thread starstream-runtime-next/src/lib.rs Outdated
async fn instantiate(
&self,
mut store: impl AsContextMut<Data = T>,
) -> wasmtime::Result<Instance>

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of adding the hook support, let's make this function public and make it return a ContractInstance, which in itself would contain the contract and instance fields and provide accessors to these.
We should then move all methods doing the call to ContractInstance

#[must_use]
pub fn new_wasmtime_config() -> wasmtime::Config {
let mut config = wasmtime::Config::new();
config.wasm_component_model(true);

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
config.wasm_component_model(true);

Component model is enabled by default

rvolosatovs added a commit that referenced this pull request Aug 4, 2026
Make `Contract::instantiate` public and have it return a new
`repr(transparent)` `ContractInstance` wrapper around the wasmtime
`Instance`. Move `create_utxo`, `load_utxo` and
`call_coordination_script` onto `ContractInstance` and drop the
`Contract`-level convenience wrappers, so callers instantiate explicitly
and the runtime keeps track of the instance.

This addresses
#185 (comment)

Signed-off-by: Roman Volosatovs <rvolosatovs@riseup.net>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
…strumented

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
…crates to legacy

the circuit and the spec are still good references while we port things
to the new package/runtime

the runtimes however were mostly exploratory work, and while they
provide some test coverage, it's for a circuit that would be deleted
anyway

the ledger integration is minimal and we'll need a new ledger spec too
anyway

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
…names

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
pre-run quint typecheck on the input
improve error reporting
forbid traces with invalid init behavior (init is not circuit related)

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
the spec just needs to specify which orders are valid (like the circuit
will do too), but we still need to be able to compute the right order

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
…ic one

similar to the existing interleaving circuit, using pending cells for
validating future actions

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
…or event template assignment)

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
… coverage

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
…asmtime_config

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
…te) + wire provisional io values in the runtime

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
ecioppettini force-pushed the enzo/reboot-interleaving-spec-and-instrument-rt-next branch from 1929314 to d8f179d Compare August 6, 2026 04:55
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

Successfully merging this pull request may close these issues.

2 participants