What is is_running?

[mimoo]

In run_state.ml, the state contains a boolean is_running:

type 'field t =
  { 
  (* ... *)
  ; is_running : bool
  (* ... *)
  }

What is this variable? It is used in two places in the imperative interface of snark0.ml:

let in_checked_computation () : bool =
  is_active_functor_id this_functor_id && Run_state.is_running !state

this is exposed to snarkyjs and not used in snarky, so who knows what they're doing with it. (CC @mitschabaude)

The second one is used in:

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

run is evaluated whenever a user-facing function of the imperative API of snarky is evaluated (e.g. exists, as_prover, assert_r1cs, Field.equal, etc.)

My guess is that it is making sure that we've initialized the state before running something. This is important because we're using a global state, and so we must:

• only run one circuit at a time (can't this become a problem in snarkyjs? especially when ran as a backend with node? CC @mitschabaude)
• correctly initialize the state before running a circuit

[mimoo]

I'm trying to understand the special case of Pure. It sounds like some commands that we want to run will just return values that we can directly read. No need to act on a state. In these cases, we can simply return the value instead of checking that it's in the right instance of snarky or that the state has been initialized.

What is x in Pure x though? My guess: it's a container of field elements, or it's a container of variables. But nothing more. Hard to tell from the definition of the AST alone, as it's not bound to anything

[mitschabaude]

I thought x is a function

[mimoo]

I don't think that's right, I think it can be any value that we return like a circuit variable. The monadic API is defined with the following return function:

let return x = Pure x

which, for example, I use in an example circuit here with (): https://github.com/MinaProtocol/mina/pull/12168/files#diff-3276fb9ec8826f76854e0d8cf3e8525dab33437a62e76d64b1c3b5000cbdf3f0R52

It's also used in the monadic API to do the same here:

  let add_constraint c = Add_constraint (c, return ())

  let as_prover x = As_prover (x, return ())

[mimoo]

I'm wondering if we can do one of these instead: check that the returned state is same as input state. Like so:

let run (checked : _ Checked.t) =
  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 (
  let state', x = Runner.run checked !state in
  (if (not (Run_state.is_running !state)) && (Run_state.compare state' !state) = 0 then
    failwith "This function can't be run outside of a checked computation." );
  state := state' ;
  x
  )

this way we can tell if it was a pure computation or not

The problem I'm facing is that it seems like we've disabled comparisons in our codebase. So I have to implement compare on the run state.

I'm trying this:

module T = struct
  open Core_kernel

  (** The internal state used to run a checked computation. *)
  type 'field t =
    { system : 'field Constraint_system.t option
    ; input : 'field Vector.t
    ; aux : 'field Vector.t
    ; eval_constraints : bool
    ; num_inputs : int
    ; next_auxiliary : int ref
    ; has_witness : bool
    ; stack : string list
    ; handler : Request.Handler.t
    ; is_running : bool
    ; as_prover : bool ref
    ; log_constraint :
        (   ?at_label_boundary:[ `Start | `End ] * string
         -> ('field Cvar.t, 'field) Constraint.t option
         -> unit )
        option
          [@compare.ignore]
    }
  [@@deriving compare]
end

include T

but it seems like I can't use that ppx to derive it on the GADTs (Constraint_system.t and Vector.t). So I need to implement the compare functions manually on these types.

The following doesn't seem to work:

type 'f t =
  | T :
      (module Backend_intf.Constraint_system_intf
         with type Field.t = 'f
          and type t = 't )
      * 't
      -> 'f t

let compare (type f) (t1 : f t) (t2 : f t) =
  match (t1, t2) with T ((module Cs1), t1), T (_, t2) -> Cs1.compare t1 t2

I think I need to use Type_equal to first prove that Cs1 = Cs2, although now I'm wondering:

• why is constraint_system abstracted?
• why is it abstracted using a GADT?

Perhaps a better solution here would be to use the kimchi_backend directly (it might also facilitate moving to a rust backend?) It is a bit annoying though, because that means we'd have to move the kimchi backend code in this repo OR create a functor for run_state instead of a top-level type (and I think we have enough functors)

[mitschabaude]

The check for whether state stays equal makes a lot of sense to me! That's the property that I would expect from a Pure AST node

[mimoo]

if you're curious, we fixed it in https://github.com/o1-labs/snarky/pull/730/files by changing the type of the monad to:

- type ('a, 'f) t = 'f Run_state.t -> 'f Run_state.t * 'a
+ type ('a, 'f) t = Pure of 'a | Function of ('f Run_state.t -> 'f Run_state.t * 'a)

[mitschabaude]

We can get rid of in_checked_computation in snarkyjs. It wasn't always working as the name suggested so we built a separate system of keeping track of these global states in JS

[mimoo]

Ah good to know! Btw just to make sure if you missed it, I CC'ed you in two different places here :D wondering what you think about the other one.

[mitschabaude]

Global variables -- yes, it means we can't run two circuits asynchronously at the same time. In snarkyjs, we immediately throw an error if a user would try that. Getting rid of the globals would be fantastic, but in my mind it's a major refactor both of snarky and snarkyjs. So maybe for a start we could build some way of using snarky that doesn't rely on global state, e.g. by having the variables reference the constraint system, and over time replace usages that rely on global state

[mimoo]

OK good to know :) I think as long as you have some ways to prevent users from doing that in snarkyjs it's much more robust

[mimoo]

Interestingly, it always seems to be set to false for the imperative interface (and the monadic interface seems to always use it set to true). And we never set it to true there. So I'm wondering:

• is this actually useful?
• snarkyjs must be setting it to true at some point, but there's no code in snarky that can mutate this variable.

[mimoo]

@mitschabaude do you know where snarkyjs sets it to true? It seems like you can't mutate that variable from the code I'm reading o_O

EDIT: I guess one way would be to create a state, or use a state created by the monadic API, and pass that to the as_stateful function or the functions that use it (make_checked):

    let as_stateful x state' =
      state := state' ;
      let a = x () in
      (!state, a)

    let make_checked (type a) (f : unit -> a) : run_state -> run_state * a =
      as_stateful f

[mimoo]

OK so I think what you said is true in snarky as well! I can run the following code at the top-level if it's run after I ran a circuit, but not before:

let _thing : Impl.Field.t =
  let one = Impl.Field.Constant.one in
  let input = [| one |] in
  let _const_digest : Impl.field = Random_oracle.hash input in
  let x = Impl.Field.constant (Impl.Field.Constant.random ()) in
  let y = Impl.Field.constant (Impl.Field.Constant.random ()) in
  printf "debug\n" ; Impl.Field.mul x y

my current guess is that as_stateful is used and replaces the original state with one that has is_running = true. I still don't understand why though, this seems like a bug.

[mitschabaude]

Awesome to hear that you can reproduce this! It also seems like a bug to me, would be great to get to the root of this

[mimoo]

@imeckler & I looked at it today (https://github.com/o1-labs/snarky/pull/730/files) and we realized that you could also call functions that create constraints out of a circuit as long as you did that after a circuit had been run at least once. This should be fixed when these PRs are merged : )

[mitschabaude]

Nice!

[mimoo]

OK so my final understanding of is_running is that:

• it is set to false when the imperative API is used, and when the imperative API "runs" it will use that global state and check that it is indeed set to false
• it is set to true otherwise

thus the only utility is to make sure that the imperative API never runs with a state that's not the global state it has set up (although in theory I could still create another state with is_running set to false).