new interleaving prover/circuit matching the compiler/runtime by ecioppettini · Pull Request #232 · LFDT-Nightstream/Starstream

ecioppettini · 2026-09-17T19:50:11Z

I wouldn't merge this yet, mainly because it depends on things in Nightstream that are unmerged yet (and some things that won't even be merged, since they were already rewritten in one of the ongoing branches)

However, I think it can be reviewed right now.

This adds mainly a "replacement" for starstream-interleaving-proof-legacy.

It also adds some missing things to the quint spec, since it was needed to get a few tests going.

Limitations:

No inputs yet (although technically set-storage is somewhat handled, but there are still multiple missing things)
The host-call scripts (which are called templates right now) are still WIP, and based somewhat on some heuristics. Eventually we'll probably need more compiler-generated metadata to infer some things.

rvolosatovs

How can one try this out? Is it at a point where it could make sense to integrate into the ledger runtime?

Starstream/starstream-ledger/src/client/runtime.rs

Line 273 in 1b27dcb

proof: Box::default(), // TODO: add proof

(possibly just logging errors for now)

ecioppettini · 2026-09-23T15:16:55Z

How can one try this out?

Well, right now only the tests (plus there will be a demo soonish)

Is it at a point where it could make sense to integrate into the ledger runtime?

Good question, maybe? I'll try it. In theory it should not be that far away. The only thing I'm still not really sure about is the Wizer part. This branch currently has support for inputs technically, in the circuit and instrumentation. But it's driven entirely though the set-storage call.

So to verify the proof, the ledger needs to be able to provide the same thing that is passed to set-storage, and check that it is the current storage (somehow).

(Also, while technically we support data segments in neo-wasm, there are some details that need to be sorted out because how it could be implemented for this depends on still unimplemented apis in Nightstream)

ecioppettini · 2026-09-30T19:45:13Z

            code.instructions()
                .i32_const(0)
-                .return_call(self.current_resource.as_ref().unwrap().resource_new_fn)
+                .call(self.current_resource.as_ref().unwrap().resource_new_fn)


@SpaceManiac thoughts on this?

I could technically get this to work, but it's less trivial than I originally I thought for a few reasons (tail calls into host functions rather than guest). Not really about proving it, but about tracing it. And for proving it I think the way to do it is to re-write it into this anyway, so it also doesn't change that much in that regard I think.

ecioppettini · 2026-10-05T14:48:58Z


 use bytes::{Bytes, BytesMut};
 use sha2::{Digest as _, Sha256};
+#[cfg(feature = "proving-instrumentation")]


@rvolosatovs could you take a quick look at this (the file, not this line)? there are still many things to do, but I wanted to at least sanity check this (and also since you asked about it)

I will do a deeper look tomorrow, but is there a particular reason we don't want to always enable this and just integrate this directly into call_coordination_script?

it could be by default I guess... mainly it was to not pull Nightstream unnecessarily, since it's not the smallest dep, but I guess for most people it will be already there

also partially because the ledger probably supports more things than the instrumentation/interleaving circuit (for example, I don't think the sha256 circuit would work right now), and I'm almost sure it will lag behind eventually, so I didn't want to block things

that said, we could remove the feature and just route things through a normal runtime flag I guess

that said, we could remove the feature and just route things through a normal runtime flag I guess

and which could be on by default and just provide a bypass

because I think tracing errors shouldn't stop the execution, but missing things on the setup side could

I fear that with the feature sprinkled around the file we will inevitably break stuff, could we have just one call_coordination_script with a boolean flag?

I unified them, and made all the instrumentation + interleaving checking have its own result type instead (which also makes guest_debug that boolean flag, technically)

rvolosatovs

On the first glance, this looks good to me overall, and I am wondering if we could just have one call_coordination_script function always producing the trace

rvolosatovs · 2026-10-05T18:23:27Z


 use bytes::{Bytes, BytesMut};
 use sha2::{Digest as _, Sha256};
+#[cfg(feature = "proving-instrumentation")]


I will do a deeper look tomorrow, but is there a particular reason we don't want to always enable this and just integrate this directly into call_coordination_script?

rvolosatovs · 2026-10-05T18:27:46Z

        inputs,
        outputs: tx_outputs,
        events,
        proof: Box::default(), // TODO: add proof


could we encode the proof and submit it to the ledger?

not right now, or at least not in a way it makes sense

first of all currently this integration is not proving anything, it's just generating the witnesses and running them through the circuit equations

if there is something wrong it will fail (and so that thing is not provable right now)

but even if we do run the prover, the nightstream version we are pointing to right now doesn't expose an easy way of serializing the proof

and even if we do that (which is quite hardware intensive), it's not the actual proof we'd want here (it's not a succinct folding proof, that's currently not supported on main)

Is there something we could just debug-print here with format!("{:?}")?

Is there something we could just debug-print here with format!("{:?}")?

I was thinking we may want Transaction<CapturedExecution> and Transaction<Proof> tbh (plus there may be other things that could be parametrized like whether it is signed or something)

Or we can just have UnprovenTransaction and Transaction. With fn prove(UnprovenTransaction) -> Transaction.

The midnight codebase has something like this for example (Transaction<ProofPreimage> I think?), since it's not that rare to have an unproven transaction (for example, you can send it to a proof server, or you could merge it with another or idk).

Right now call_coordination_script returns wasmtime::Result<(Transaction, wasmtime::Result<CapturedExecution>)>

But I was considering putting the second element of the tuple in there directly. I didn't do it because I'd need to derive all the cbor traits for it, but I could do it if you think that could be useful.

rvolosatovs · 2026-10-06T13:56:25Z


 use bytes::{Bytes, BytesMut};
 use sha2::{Digest as _, Sha256};
+#[cfg(feature = "proving-instrumentation")]


I fear that with the feature sprinkled around the file we will inevitably break stuff, could we have just one call_coordination_script with a boolean flag?

rvolosatovs · 2026-10-06T14:22:31Z

+                        | Type::Float32
+                        | Type::Float64


I don't think we support floats

we don't, but this is checking for scalar types... I guess I could remove them, the error would be misleading but it won't happen anyway

rvolosatovs · 2026-10-06T14:38:58Z

+    let [root, rest @ ..] = components.as_slice() else {
+        unreachable!("root component is always registered");
+    };


Ideally, I'd like to remove the need for this

maybe done? or well... not sure, the split is gone, the unreachable is there, although I could just let it panic without message, unless I don't use a vec?

rvolosatovs · 2026-10-06T14:40:53Z

+
+/// Register the contract's core module and create a single-step tracing store.
+/// Neo-Wasm discovers each instance and captures its entry inputs automatically.
+pub fn new_tracing_wasmtime_store<T: neo_wasm::WasmTraceSink + Send + 'static>(


could we rename this function to something like enable_tracing and take &mut Store<T> as parameter instead of calling Store::new?

rvolosatovs · 2026-10-06T14:42:33Z

+        // Direct scalar/resource parameters each lower to _one_ core local.
+        // TODO: Support composite and indirectly lowered coordinator arguments.
+        // (the indexes of utxo inputs will be invalid as computed right now otherwise)
+        ensure!(


could we move this check to the top of the function to fail early?

rvolosatovs · 2026-10-06T14:44:27Z

+        if let ResolvedCoordinationScriptArg::Utxo(input) = arg {
+            input_locals.push(index);
+            input_methods.push(
+                input
+                    .output
+                    .methods
+                    .iter()
+                    .map(|&(a, b, c, d)| {
+                        starstream_proving_runtime::MethodHash::from_u64_words([a, b, c, d])
+                    })
+                    .collect::<Vec<_>>(),
+            );
+            let (_, instrumented) = wizer.instrument_component(&input.wasm)?;
+            let scripts = input
+                .contract
+                .coordination_scripts()
+                .map(|(name, export)| export.map(|_| name))
+                .collect::<wasmtime::Result<Vec<_>>>()?;
+            let templates =
+                build_component_templates(&instrumented, &scripts).map_err(|error| {
+                    wasmtime::format_err!("failed to build input trace templates: {error}")
+                })?;
+            components.push(TracingComponent {
+                instrumented,
+                templates,
+            });
+        }


could we do this while iterating the args during resolution?
If we unify all of this in call_coordination_script we probably also would not need the ResolvedCoordinationScriptArg enum

rvolosatovs · 2026-10-06T14:48:34Z

+    script: &str,
+    export: &CoordinationScriptExport,


could we add a TODO here to only require one of these?

well, I put the name in CoordinationScriptExport now... I don't see another easy way of recovering it otherwise

rvolosatovs · 2026-10-07T09:54:11Z

+    // tracked for the proving instrumentation
+    //
+    // we use this as a key into the core-wasm function namespace, since
+    // wasmtime doesn't expose enough information to get the core module id for
+    // the export otherwise
+    name: String,


Suggested change

// tracked for the proving instrumentation

//

// we use this as a key into the core-wasm function namespace, since

// wasmtime doesn't expose enough information to get the core module id for

// the export otherwise

name: String,

name: Arc<str>,

rvolosatovs · 2026-10-07T09:55:46Z

+#[allow(dead_code)]
+mod common;


Suggested change

#[allow(dead_code)]

mod common;

pub mod common;

rvolosatovs · 2026-10-07T09:58:31Z

+enum ResolvedCoordinationScriptArg {
+    Val(Val),
+    Utxo(ResolvedUtxoInput),
+}
+
+struct ResolvedUtxoInput {
+    input: TransactionInput,
+    output: TransactionOutput,
+    contract: starstream_runtime_next::Contract<Ctx>,
+    external_id: Option<Arc<str>>,
+    wasm: Vec<u8>,
+}


l still feel like these should not be necessary, if we just inline everything in call_coordination_script, at least to begin with, we can always refactor later.

That would also minimize the diff in the PR making it easier to review

rvolosatovs

The ledger/runtime part looks good to me, and I am happy to refactor things later