powdr-labs / powdr

A modular stack for zkVMs, with a focus on productivity, security and performance.
Apache License 2.0
362 stars 76 forks source link

ASM: Allow multiple machines to access the same machine instance #1200

Open georgwiese opened 5 months ago

georgwiese commented 5 months ago

We currently don't have a way to declare a machine instance that is used by more than one calling machine, like this:

graph TD;
    Main --> Hash;
    Main --> Padding;
    Padding --> Hash;

Automatic witness generation for this should already be working!

As far as I'm aware, this is the last missing features we'd need to implement #1055!

Schaeff commented 5 months ago

I think a clean way to achieve this would be to make instantiation explicit rather than implicit now:

let main: [] -> Main = || {
      let hash = Hash {};

      Main { padding: Padding { hash }, hash }
}

And interpret the main function as the entry point just like we use the Main machine type now. That would require machines to be types, which I don't think is the case now?

By doing this we're moving airgen to the front end and making it customisable. Optionally we could still derive the "naive" way to generate the air ~tree~ graph and preserve the current UX:

#[derive(main)]
machine Main {
   Padding padding;
   Hash hash;
}

// derived automatically
let main: [] -> Main = || Main { padding: Padding { hash: Hash {} }, hash: Hash {} };
chriseth commented 5 months ago

I agree, machines should be syntactic sugar for functions that return machine objects.

I think the main open question is where to place the arguments for machines (as in already instatiated sub-machines) if there are any.

leonardoalt commented 4 months ago

Following @Schaeff 's example, wouldn't that then just be this?

#[derive(main)]
struct Main {
   padding: Padding,
   hash: Hash
}

struct Hash;

struct Padding {
    hash: Hash
}

let hash_constructor: () -> Hash = || Hash {};
let h = hash_constructor();
let padding_constructor: (h: Hash) -> Padding = || Padding { hash: h };
let p = padding_constructor();

// derived automatically
let main: () -> Main = || Main { padding: p, hash: h };
leonardoalt commented 4 months ago

We decided in a call to do something like this:


machine Main {
    mem: Memory;
    binary: Binary(mem);
}

machine Binary(mem: Memory) {
    use mem.addr or whatever
    ...
    #[operation_id]
    col witness operation_id;

    #[latch]
    col fixed latch(i) { if (i % 4) == 3 { 1 } else { 0 } };

    ...
}
leonardoalt commented 4 months ago

Depends on https://github.com/powdr-labs/powdr/issues/1251

leonardoalt commented 3 months ago

Was this merged @pacheco ?