Swapping out the monadic and the imperative interfaces

[mimoo]

In the work of reimplementing parts of snarky in Rust, we want to ideally maintain compatibility with the current usage of snarky in the Mina codebase. There's currently two APIs for snarky: a monadic one, and an imperative one. Both are used in Mina. The imperative one is currently built on top of the monadic one.

We are planning to write snarky-rs as an imperative API, as such we need to either get rid of the monadic API, or make the monadic API a wrapper around the imperative API (invert the current relationship between the two APIs).

The monadic interface is created from a module following the Checked_intf.Basic interface. If we can make that interface generic enough, so that it can contain an implementation of an imperative API, we'll successfully revert the APIs.

Where is snarky used?

examples:

• snarkyjs
• pickles
• mina
  • transaction snark
  • proof of stake
  • snark state
  • fee excess
  • ledger hash
  • pending coinbase
  • etc.

as you can see, lots of usage of the monadic API (let%bind ...)

Changes necessary to invert the APIs

The current Checked_intf.Basic interface has functions like this:

  val add_constraint :
    ('f field Cvar.t, 'f field) Constraint.t -> (unit, 'f field) t

Eventually we will have t here be a runstate used in an imperative implementation (and not an AST like in the monadic implementation). So we'll have to change these kind of signatures to:

  val add_constraint :
    'f field t -> ('f field Cvar.t, 'f field) Constraint.t -> 'f field t

unless we use a global, in which case t will contain nothing? I'm not super clear on what the path forward is there.

Removing dependency on the Checked_ast module in Typ

One of the steps to get there is to make the Typ module generic over a Checked interface. Currently it is not, as can be seen in in snark_intf.ml it still relies on Checked_ast.t:

module type Basic = sig
  (* ... *)
  and Typ : sig
    include
      Typ_intf
        with type field := Field.t
         and type field_var := Field.Var.t
         and type checked_unit := (unit, field) Checked_ast.t
         and type _ checked := unit Checked.t
         and type ('a, 'b, 'c, 'd) data_spec :=
          ('a, 'b, 'c, 'd, field) Typ0.Data_spec.t
         and type 'a prover_ref := 'a As_prover.Ref.t

    include module type of Types.Typ.T
  end

(* ... *)

module type Run_basic = sig
  (* ... *)
  and Typ :
    (Typ_intf
      with type field := Field.Constant.t
       and type field_var := Field.t
       and type checked_unit := (unit, field) Checked_ast.t
       and type _ checked := unit
       and type ('a, 'b, 'c, 'd) data_spec :=
        ('a, 'b, 'c, 'd, field) Typ0.Data_spec.t
       and type 'a prover_ref := 'a As_prover.Ref.t)

[mrmr1993]

Changes necessary to invert the APIs

The current Checked_intf.Basic interface has functions like this:

  val add_constraint :
    ('f field Cvar.t, 'f field) Constraint.t -> (unit, 'f field) t

Eventually we will have t here be a runstate used in an imperative implementation (and not an AST like in the monadic implementation). So we'll have to change these kind of signatures to:

  val add_constraint :
    'f field t -> ('f field Cvar.t, 'f field) Constraint.t -> 'f field t

We shouldn't need to do anything. Consider the monad type

type ('a, 'f) t = 'f Run_state.t -> 'a * Run_state.t

let return x : _ t = fun _run_state -> x

let map (x : _ t) ~f = fun run_state ->
  let x, run_state = x run_state in
  f x, run_state

let bind (x : _ t) ~f = fun run_state ->
  let x, run_state = x run_state in
  let y, run_state = f x run_state in
  y, run_state

Then add_constraint can keep the same type, but the monad allows us to use the functional version. Concretely, the type of add_constraint in the implementation will be

val add_constraint : ('f field Cvar.t, 'f field) Constraint.t -> 'f field Run_state.t -> unit * 'f field Run_state.t

which already matches what will be required by the Basic module type. This currently exists in Checked_runner.

[mimoo]

Oh, that explains a lot of the code I've seen in the checked_runner. So is this code dormant until we can use it?

I think your return is supposed to be:

let return x : _ t = fun run_state -> (x, run_state)

and shouldn't bind also have f only run on run_state? If this happens I don't understand what becomes to r1 here

let bind (x : _ t) ~f = fun run_state ->
  let r1, run_state = x run_state in
  let r, run_state = f run_state in
  r, run_state

I'll think more about that

[mimoo]

A, probably somewhat flawed, picture of the current state: