powdr-labs / powdr

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

Implement vm_to_constrained in PIL or at least make more use of PIL's new features #777

Open chriseth opened 11 months ago

chriseth commented 11 months ago

Rust code inside vm_to_constrained.rs should be reduced and moved to be implemented in PIL instead.

This is more of a brainstorming issue to see if it's possible at all.

The syntax can of course stay exactly as it is now, but instead of transforming the asm syntax into PIL directly, we should transform it into a set of functions that do the actual conversion as part of the evaluator / condenser.

This is roughly how it could look, for example:

// The whole machine is inside a closure, so we can create an instance of it by calling it.
let vm_machine = || {
  let machine = Machine{...};
  // "reg pc[@pc]" is replaced by:
  // this is the column. We need this to exist by that name in this namespace because directly written pil code references it.
  // It is also referenced in the `default_update` field. We could also use a function for default_update that receives the column as input.
  let pc;
  let machine = add_register(machine, Register{column: pc, name: "pc", conditioned_updates = [], default_update = Some(pc + 1)};
  // reg X[<=];
  let X;
  let machine = add_register(machine, Register{column: X, name: "X",  conditioned_updates = [], default_update = None});

  // instr jump l: label { pc' = l }
  let machine = add_instruction(machine, Instruction{name: "jump", inputs: [Input::Label()], outputs: [], constraints: [|input1| pc' = input1]});

  // instr mload Y -> X, Z { ... }
  let machine = add_instruction(machine, Instruction{name: "mload", inputs: [Y], outputs: [X, Z], constraints: [...]});

  machine.create()
};
leonardoalt commented 7 months ago

This would be cool!