o1-labs / snarky

OCaml DSL for verifiable computation
MIT License
494 stars 74 forks source link

Removing checked_ast 3/3 #761

Closed mimoo closed 1 year ago

mimoo commented 1 year ago

get rids of the AST. Builds on top of https://github.com/o1-labs/snarky/pull/752

mina side PR: https://github.com/MinaProtocol/mina/pull/12360


this deletes the snarkydef module, and replaces its usage with direct calls. All it seemed to do was to wrap functions with a with_label call.

The change looks like adding these lines in most places:

        let label =
          Stdlib.("compare: " ^ __FILE__ ^ ":" ^ string_of_int __LINE__)
        in
        let%bind () = with_label label (fun _ -> return ()) in

This looks like it's correct to me, because return will simply start a Pure (), which the with_label function will replace with:

Function (fun s -> 
  (* ... *)
  (* evaluate [t] on the state *)
  let new_state_with_label, y = Simple.eval (t ()) state_with_label in

and as we can see, eval will simply return the real state and ():

  let eval (t : ('a, 'f) t) : 'f field Run_state.t -> 'f field Run_state.t * 'a
      =
    match t with Pure a -> fun s -> (s, a) | (* ... *)

(I also took the liberty of changing the format slightly to filename:linenumber as most editors linkify such format and allow you to click to source on them.)