Removing checked_ast

[mimoo]

Essential information

• This builds on top of https://github.com/o1-labs/snarky/pull/686
• Mina side here: https://github.com/MinaProtocol/mina/pull/12347
• You can review this PR commit by commit

Removing Checked_ast

Checked_ast is still used in some places. We need to remove it from:

• [x] snarkydef <-- done in https://github.com/o1-labs/snarky/pull/761
• [x] checked_runner
• [x] as_prover

The one in As_prover seems to be the most tricky. Ideally we would remove these lines and it would work:

module T : S with module Types = Checked_ast.Types and type 'f field := 'f =
  Make (Checked_ast) (As_prover0)

include T

Problem 1: Checked_runner uses it in its functor:

module Checked_runner = Make_checked (Backend) (As_prover)

This makes sense, but our Checked_runner should also be able to use an As_prover instance created by a functor.

Problem 2: this doesn't work because the As_prover.Make functor takes a Checked.

Solution: what we really want to do is be able to call As_prover.Make without Checked, instantiate a module with it, then use it as argument to Checked_runner.Make_checked.

Roadmap

There's a number of steps to take to make this happen. It seems like the only reason why As_prover needs Checked is because of As_prover.Ref. So let's factor it out:

• [x] move Ref to its own module
• [x] remove the construction of Ref from As_prover.Make and construct it separately
• [x] remove As_prover dependency on Checked
• [x] remove As_prover.T
• [x] change the order of construction to: 1. construct As_prover 2. construct Checked_runner 3. construct As_prover.Ref in both APIs of snarky

[mimoo]

running into some error, that can be reproduce from mina by doing:

make snarkyjs
cd src/lib/snarky_js_bindings/test_module 
npm i
node simple-zkapp-mock-apply.js

the issue is an assert_equals function that does not handle constant variables correctly.

The reason is that it's using what's in checked.ml (which is "impure" as it adds a constraint):

  let assert_ ?label c = add_constraint (Constraint.override_label c label)

  let assert_equal ?label x y = assert_ (Constraint.equal ?label x y)

whereas we want to use the wrapper that's introduced in utils.ml (which handles the constant correctly, and keep the logic "pure"):

  let assert_equal ?label x y =
    match (x, y) with
    | Cvar0.Constant x, Cvar0.Constant y ->
        if Field.equal x y then Checked.return ()
        else
          failwithf !"assert_equal: %{sexp: Field.t} != %{sexp: Field.t}" x y ()
    | _ ->
        Checked.assert_equal ?label x y

to fix this bug I need to understand why this function is defined in two places, and why there seems to be a low-level one vs a high-level one that handles constants

[mimoo]

merged the last part (https://github.com/o1-labs/snarky/pull/761) into this branch to facilitate debugging, working on a fix in https://github.com/o1-labs/snarky/pull/776