The Imperative API of snarky

[mimoo]

As explained in this document, the interface of snarky is split between two types of APIs: a monadic one, and an imperative one.

In this document I explain the imperative one, refer to the previously linked document for more on the monadic one.

Overview

First, let's point out that most of the logic for an imperative interface already exists in checked_runner.ml (as a Checked_intf.Basic, and further wrapped in checked.ml to create a Checked_intf.S).

They are normally used by the monadic API to parse an AST (and used via bind), but they can actually be used directly as imperative functions that take a state and return a new state (and potentially a value).

For example:

  let add_constraint c s =
    if Run_state.as_prover s then
      (* Don't add constraints as the prover, or the constraint system won't match! *)
      (s, ())
    else (
      Option.iter (Run_state.log_constraint s) ~f:(fun f -> f (Some c)) ;
      if Run_state.eval_constraints s && not (Constraint.eval c (get_value s))
      then
        failwithf
          "Constraint unsatisfied (unreduced):\n\
           %s\n\
           %s\n\n\
           Constraint:\n\
           %s\n\
           Data:\n\
           %s"
          (Constraint.annotation c)
          (stack_to_string (Run_state.stack s))
          (Sexp.to_string (Constraint.sexp_of_t c))
          (log_constraint c s) () ;
      if not (Run_state.as_prover s) then
        Option.iter (Run_state.system s) ~f:(fun system ->
            add_constraint ~stack:(Run_state.stack s) c system ) ;
      (s, ()) )

The second thing to point out is that we do not currently use this logic directly.

The intuition behind the current imperative interface is the following: both checked_runner.ml and checked_ast.ml introduce monads, and both can implement the Checked_intf.Basic interface that Checked requires.

Currently, the imperative interface builds Checked using the AST implementation, which means that the different user-facing functions of snarky, like exists, will still construct an AST.

The difference is that we run AST nodes as soon as we create them, by converting them to the state monad (with ast_runner) and then running them.

But this is not necessary, and we can get rid of the AST monad. This is what #685 attempts to achieve.

Constructing a circuit with the imperative API

snark0 redefines a number of user-facing functions for the imperative API (which is defined in Snark0.Run if you remember). For example:

  let exists ?request ?compute typ =
    let request = Option.map request ~f:As_prover.run_prover in
    let compute = Option.map compute ~f:As_prover.run_prover in
    run (exists ?request ?compute typ)

This will call Checked.exists function, which as I said before is currently implemented with the AST monad (checked_ast).

Thus, this will create an AST node (of tag Exists), which we want to run right away.

For this, the run function is used, and defined as:

let run (checked : _ Checked.t) =
  match checked with
  | Pure x ->
      x
  | _ ->
      if not (is_active_functor_id this_functor_id) then
        failwithf
          "Could not run this function.\n\n\
            Hint: The module used to create this function had internal ID \
            %i, but the module used to run it had internal ID %i. The same \
            instance of Snarky.Snark.Run.Make must be used for both."
          this_functor_id (active_functor_id ()) ()
      else if not (Run_state.is_running !state) then
        failwith
          "This function can't be run outside of a checked computation." ;
      let state', x = Runner.run checked !state in
      state := state' ;
      x

A few things are important to point out here:

• there's a special case for Pure, which I do not currently understand, but removing it will make some snarkyjs tests fail (so it seems to be quite important)
• we do some "a circuit built with this instance of snarky should be ran only with this instance of snarky". This is because circuits are constructed assuming a specific field, and running them with an instance of snarky parameterized over a different field is a recipe for vulnerabilities
• we use Runner.run checked to convert the AST to the state monad (which is a function that takes a state and returns a state + a value)
• we use a global state to evaluate the function contained in the state monad. This is to avoid having the user pass the state, and return it, with every snarky function calls.

Compiling and generating a witness

If you understood the previous explanations, you must have realized that the state is mutated as the user calls circuit-construction functions like exists. As such, the circuit is being compiled, or use to create a witness, when we run the user function that defines a circuit.

This omits that snarky has several steps for compilation of circuits, or witness generation. Before running a circuit, the state must be initialized, and after running a circuit, the state is used further to produce compiled gates or a witness.