Add interleaving proof circuit with reference ledger/spec

[ecioppettini]

This is a long running branch, so my apologies to reviewers this. There are still missing things, but in theory it should be possible to start integrating some of these things with the DSL, and maybe the mock ledger, so it's probably worth merging sooner rather than later. If preferred I could squash the commits, but that's probably better to do at merge time.

As a demo of how everything fits together, this test covers a big part of the flow:

DEBUG_WAT=1 cargo test -p starstream-runtime --release test_runtime_effect_handlers_cross_calls -- --include-ignored --nocapture

Which does:

output.mp4

(Note: the test is currently ignored since it's kind of heavy)

Review guide

As a guide, there are are 5 new crates added:

ark-goldilocks

This one is mainly a small wrapper to define the goldilocks prime field for arkworks. Since the interleaving-proof-circuit currently uses arkworks as the DSL.

ark-poseidon2

A plonky3-compatible version of Poseidon2 for Arkworks, so that we can use it for R1CS (it's currently used to commit to the interleaving traces).

Currently only the compression mode is really used, but the idea is to also use the sponge mode for computing the contract hashes eventually (at least if we need to prove it).

Something else that is missing is allowing setting up proper constants.

interleaving/starstream-interleaving-spec

A crate that acts as a reference for the ledger + ledger effects (coordination script or utxo opcodes). It contains the document with the high-level architectural design, plus how the high-level language constructs are supposed to compile into it.

It contains a more or less working ledger, with the main purpose of being able to show how to link the proven statement with the on-chain state transition.

It also has a "mocked_verifier", which is not really a mock, but more like a non-zk + non-optimized version of the circuit logic. It's currently used to have examples/tests with the reference ledger, and also for cross-checking proofs in the integration tests (although currently the mocked verifier runs after the proof, which probably should be the other way around).

Ideally changes to the interleaving proof system need be done in this order:

1. Update spec (EFFECTS_REFERENCE.md)
2. Update the mocked verifier
3. Update the tests in the spec crate if needed
4. Update the circuit (starstream-intereleaving-proof)
5. Update intergration tests and circuit tests.

But of course it really depends on the changes.

interleaving/starstream-interleaving-proof

The interleaving proof circuit and the Nightstream connection.

In terms of readability some parts are still a bit rough, but I have some ideas for improving that. But as a framework it's more or less functional.

It currently implements all the effects/opcodes, and can generate Nightstream proofs, although there are still some things that are underconstrained/unbound.

Some of these include:

• The cross-step ivc linking step (this is just a few lines to add)
• The length/counters of the traces for each coroutine (but the traces are bound, so I'm not actually sure yet if we need this)
• Probably the trace commitment should include some domain separator, as a custom IV.

interleaving/starstream-runtime

A demo wasm runtime using wasmi for interleaving trace generation.

Plus integration tests using an ad-hoc wasm dsl (which we can probably throw away after the proper Starstream dsl has enough features to generate the traces).

Note: I guess we are probably not going to use wasmi, I mainly picked that becuase I was familiar with the api, and it supported the suspensions. For the proof we'll need a dedicated runtime, probably. And for the tracing for tests we could also probably use wasmtime too I imagine, although I haven't tried it yet.

This is to say the code in the runtime is also probably going to be replaced too, but for the time being it's a simple way of getting a full flow.

NOTE: I'm probably going to replace the multi-value return used for the host calls with out parameters soon, since that has a few benefits in terms of support.

[ecioppettini]

it seems to take about a minute to run this test in the CI, do you think that's big enough to ignore it @SpaceManiac ?

[SpaceManiac]

I think total CI time is still acceptable with this test running. We can ignore it later if CI time grows.

[SpaceManiac]

First pass stuff I noticed

[SpaceManiac]

Seems unnecessary to me. cargo test --release still works fine if I revert this.

[SpaceManiac]

Seems leftover

[SpaceManiac]

I think total CI time is still acceptable with this test running. We can ignore it later if CI time grows.

[TenStrings]

I'm starting to think that maybe Yield should not have a return value, and then we just use Activation to get the resumption argument...

Then utxos would basically always have to do

yield some_data; // gets suspended
let (resumption_arg, resumer) = activation(); // runs when resumed

(as long as they actually care about the argument/resumer)

Instead of the maybe weird

let maybe_resumed = yield some_data;
let (resumption_arg, resumer) = maybe_resumed.unwrap_or_else(activation);

Any thoughts @SpaceManiac ?

Of course this doesn't mean the language can't expose yield as an atomic call, it's just that it would be compiled into two host-calls instead of one. It may be less optimal I guess, since it would be a bigger trace and more host-calls, but that may be a premature optimization. And while it changes the semantics a bit, I think it's still sound.

[SpaceManiac]

I can see it going either way in the end. If having them separate for now is easier to reason about, go for it.

[SpaceManiac]

To be honest, I think I'll need to actually try integrating other parts of the code with this to fully understand it, but I've at least given a once-over to everything and I don't see anything that should block merging.

[ecioppettini]

To be honest, I think I'll need to actually try integrating other parts of the code with this to fully understand it, but I've at least given a once-over to everything and I don't see anything that should block merging.

I'll merge then (after a last rebase). I can scope features better with individual PRs after that.

Would you rather do a merge commit or a squash btw?

[SpaceManiac]

In this case, I think the detailed commits may be worth preserving, so merge commit should do.