From 73dd6c56fa37cc6f777253952913e5a7a52aa3c1 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Wed, 20 Nov 2024 13:04:46 +0000
Subject: [PATCH 01/12] Inline Typ definition

---
 src/base/snark0.ml     |  3 +++
 src/base/snark_intf.ml | 50 +++++++++++++++++++++++++++---------------
 src/base/typ.ml        | 42 ++++++++++++++++++-----------------
 3 files changed, 57 insertions(+), 38 deletions(-)

diff --git a/src/base/snark0.ml b/src/base/snark0.ml
index 11ffde363d..755e4ddba1 100644
--- a/src/base/snark0.ml
+++ b/src/base/snark0.ml
@@ -767,8 +767,11 @@ module Run = struct
     module Constraint = Snark.Constraint
 
     module Typ = struct
+      include Types.Typ.T
       open Snark.Typ
 
+      module Data_spec = Typ.Data_spec
+
       type nonrec ('var, 'value) t = ('var, 'value) t
 
       let unit = unit
diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml
index 465daf2089..718a837821 100644
--- a/src/base/snark_intf.ml
+++ b/src/base/snark_intf.ml
@@ -133,10 +133,32 @@ module type Typ_intf = sig
 
   type checked_unit
 
-  type (_, _, _, _) data_spec
-
   type _ prover_ref
 
+  type ('var, 'value, 'aux, 'field, 'checked) typ' =
+    { var_to_fields : 'var -> 'field Cvar.t array * 'aux
+    ; var_of_fields : 'field Cvar.t array * 'aux -> 'var
+    ; value_to_fields : 'value -> 'field array * 'aux
+    ; value_of_fields : 'field array * 'aux -> 'value
+    ; size_in_field_elements : int
+    ; constraint_system_auxiliary : unit -> 'aux
+    ; check : 'var -> 'checked
+    }
+
+  type ('var, 'value, 'field, 'checked) typ =
+    | Typ :
+        ('var, 'value, 'aux, 'field, 'checked) typ'
+        -> ('var, 'value, 'field, 'checked) typ
+
+  module Data_spec : sig
+    type ('r_var, 'r_value, 'k_var, 'k_value, 'field) t =
+      | ( :: ) :
+          ('var, 'value, 'field, checked_unit) typ
+          * ('r_var, 'r_value, 'k_var, 'k_value, 'field) t
+          -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value, 'field) t
+      | [] : ('r_var, 'r_value, 'r_var, 'r_value, 'field) t
+  end
+
   (** The type [('var, 'value) t] describes a mapping from the OCaml type
         ['value] to a type representing the value using R1CS variables
         (['var]).
@@ -150,7 +172,7 @@ module type Typ_intf = sig
           example, that a [Boolean.t] is either a {!val:Field.zero} or a
           {!val:Field.one}.
     *)
-  type ('var, 'value) t = ('var, 'value, field, checked_unit) Types.Typ.t
+  type ('var, 'value) t = ('var, 'value, field, checked_unit) typ
 
   (** Basic instances: *)
 
@@ -204,7 +226,7 @@ module type Typ_intf = sig
   (** Unpack a {!type:Data_spec.t} list to a {!type:t}. The return value relates
         a polymorphic list of OCaml types to a polymorphic list of R1CS types. *)
   val hlist :
-       (unit, unit, 'k_var, 'k_value) data_spec
+       (unit, unit, 'k_var, 'k_value, field) Data_spec.t
     -> ((unit, 'k_var) H_list.t, (unit, 'k_value) H_list.t) t
 
   (** Convert relationships over
@@ -227,7 +249,7 @@ module type Typ_intf = sig
         {!type:Data_spec.t}.
     *)
   val of_hlistable :
-       (unit, unit, 'k_var, 'k_value) data_spec
+       (unit, unit, 'k_var, 'k_value, field) Data_spec.t
     -> var_to_hlist:('var -> (unit, 'k_var) H_list.t)
     -> var_of_hlist:((unit, 'k_var) H_list.t -> 'var)
     -> value_to_hlist:('value -> (unit, 'k_value) H_list.t)
@@ -584,11 +606,7 @@ module type Basic = sig
          and type field_var := Field.Var.t
          and type checked_unit := unit Checked.t
          and type _ checked := unit Checked.t
-         and type ('a, 'b, 'c, 'd) data_spec :=
-          ('a, 'b, 'c, 'd, field, unit Checked.t) Typ0.Data_spec0.data_spec
          and type 'a prover_ref := 'a As_prover_ref.t
-
-    include module type of Types.Typ.T
   end
 
   (** Representation of booleans within a field.
@@ -1143,14 +1161,6 @@ module type Run_basic = sig
        and type field_var := Field.t
        and type checked_unit := unit Internal_Basic.Checked.t
        and type _ checked := unit
-       and type ('a, 'b, 'c, 'd) data_spec :=
-        ( 'a
-        , 'b
-        , 'c
-        , 'd
-        , field
-        , unit Internal_Basic.Checked.t )
-        Typ0.Data_spec0.data_spec
        and type 'a prover_ref := 'a As_prover_ref.t)
 
   (** Representation of booleans within a field.
@@ -1268,7 +1278,11 @@ module type Run_basic = sig
     (Basic
       with type field = field
        and type 'a Checked.t = ('a, field) Checked_runner.Simple.t
-       and type 'a As_prover.Ref.t = 'a As_prover_ref.t)
+       and type 'a As_prover.Ref.t = 'a As_prover_ref.t
+       and type ('var, 'value, 'aux, 'field, 'checked) Typ.typ' =
+        ('var, 'value, 'aux, 'field, 'checked) Typ.typ'
+       and type ('var, 'value, 'field, 'checked) Typ.typ =
+        ('var, 'value, 'field, 'checked) Typ.typ)
 
   module Bitstring_checked : sig
     type t = Boolean.var list
diff --git a/src/base/typ.ml b/src/base/typ.ml
index af16e2538d..3e792add64 100644
--- a/src/base/typ.ml
+++ b/src/base/typ.ml
@@ -100,27 +100,29 @@ module Make (Checked : Checked_monad) = struct
          and type field_var := field Cvar.t
   end
 
-  module Data_spec = struct
-    include Data_spec0
-
-    type ('r_var, 'r_value, 'k_var, 'k_value, 'f) t =
-      ('r_var, 'r_value, 'k_var, 'k_value, 'f, (unit, 'f) Checked.t) data_spec
-
-    let size t =
-      let rec go :
-          type r_var r_value k_var k_value.
-          int -> (r_var, r_value, k_var, k_value, 'f) t -> int =
-       fun acc t ->
-        match t with
-        | [] ->
-            acc
-        | Typ { size_in_field_elements; _ } :: t' ->
-            go (acc + size_in_field_elements) t'
-      in
-      go 0 t
-  end
-
   module T = struct
+    module Data_spec = struct
+      type ('r_var, 'r_value, 'k_var, 'k_value, 'field) t =
+        | ( :: ) :
+            ('var, 'value, 'field) typ
+            * ('r_var, 'r_value, 'k_var, 'k_value, 'field) t
+            -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value, 'field) t
+        | [] : ('r_var, 'r_value, 'r_var, 'r_value, 'field) t
+
+      let size t =
+        let rec go :
+            type r_var r_value k_var k_value.
+            int -> (r_var, r_value, k_var, k_value, 'f) t -> int =
+         fun acc t ->
+          match t with
+          | [] ->
+              acc
+          | Typ { size_in_field_elements; _ } :: t' ->
+              go (acc + size_in_field_elements) t'
+        in
+        go 0 t
+    end
+
     let unit () : (unit, unit, 'field) t =
       Typ
         { var_to_fields = (fun () -> ([||], ()))

From ceff57333acddbf969524b9836e711ac832187a3 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Wed, 20 Nov 2024 17:23:21 +0000
Subject: [PATCH 02/12] Remove toplevel `Typ.t`

---
 src/base/typ.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/base/typ.ml b/src/base/typ.ml
index 3e792add64..c98f0505ac 100644
--- a/src/base/typ.ml
+++ b/src/base/typ.ml
@@ -463,5 +463,3 @@ module Make (Checked : Checked_monad) = struct
 
   include T
 end
-
-include Make (Checked_runner.Simple)

From 681d6833da225201ad97d5b0df779faf7057d498 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Wed, 20 Nov 2024 20:39:16 +0000
Subject: [PATCH 03/12] Reformat

---
 src/base/snark0.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/base/snark0.ml b/src/base/snark0.ml
index 755e4ddba1..6fcef9c5fa 100644
--- a/src/base/snark0.ml
+++ b/src/base/snark0.ml
@@ -769,7 +769,6 @@ module Run = struct
     module Typ = struct
       include Types.Typ.T
       open Snark.Typ
-
       module Data_spec = Typ.Data_spec
 
       type nonrec ('var, 'value) t = ('var, 'value) t

From d7a81a01b0942bb7226cf9f56c0a1e8114b0d673 Mon Sep 17 00:00:00 2001
From: martyall <martyall@protonmail.com>
Date: Sat, 23 Nov 2024 12:25:39 -0800
Subject: [PATCH 04/12] remove unused free monad module

---
 README.md                      |   7 ---
 src/base/free_monad.ml         | 100 ---------------------------------
 src/base/snarky_backendless.ml |   1 -
 src/snarky.ml                  |   1 -
 4 files changed, 109 deletions(-)
 delete mode 100644 src/base/free_monad.ml

diff --git a/README.md b/README.md
index 1002b73faa..c37bfc1f72 100644
--- a/README.md
+++ b/README.md
@@ -101,13 +101,6 @@ let implied_root_unchecked entry_hash addr0 path0 =
 The two obviously look very similar, but the first one can be run to generate an R1CS
 (and also an "auxiliary input") to verify that computation. 
 
-## Implementation
-
-Currently, the library uses a free-monad style AST to represent the snark computation.
-This may change in future versions if the overhead of creating the AST is significant.
-Most likely it will stick around since the overhead doesn't seem to be too bad and it
-enables optimizations like eliminating equality constraints.
-
 ## Building
 
 ```
diff --git a/src/base/free_monad.ml b/src/base/free_monad.ml
deleted file mode 100644
index 1619d84caa..0000000000
--- a/src/base/free_monad.ml
+++ /dev/null
@@ -1,100 +0,0 @@
-module Functor = struct
-  module type S = sig
-    type 'a t
-
-    val map : 'a t -> f:('a -> 'b) -> 'b t
-  end
-
-  module type S2 = sig
-    type ('a, 'e) t
-
-    val map : ('a, 'e) t -> f:('a -> 'b) -> ('b, 'e) t
-  end
-
-  module type S3 = sig
-    type ('a, 'x, 'y) t
-
-    val map : ('a, 'x, 'y) t -> f:('a -> 'b) -> ('b, 'x, 'y) t
-  end
-end
-
-module Make (F : Functor.S) : sig
-  type 'a t = Pure of 'a | Free of 'a t F.t
-
-  include Monad_let.S with type 'a t := 'a t
-end = struct
-  module T = struct
-    type 'a t = Pure of 'a | Free of 'a t F.t
-
-    let rec map t ~f =
-      match t with
-      | Pure x ->
-          Pure (f x)
-      | Free tf ->
-          Free (F.map tf ~f:(map ~f))
-
-    let map = `Custom map
-
-    let return x = Pure x
-
-    let rec bind t ~f =
-      match t with Pure x -> f x | Free tf -> Free (F.map tf ~f:(bind ~f))
-  end
-
-  include T
-  include Monad_let.Make (T)
-end
-
-module Make2 (F : Functor.S2) : sig
-  type ('a, 'x) t = Pure of 'a | Free of (('a, 'x) t, 'x) F.t
-
-  include Monad_let.S2 with type ('a, 'x) t := ('a, 'x) t
-end = struct
-  module T = struct
-    type ('a, 'x) t = Pure of 'a | Free of (('a, 'x) t, 'x) F.t
-
-    let rec map t ~f =
-      match t with
-      | Pure x ->
-          Pure (f x)
-      | Free tf ->
-          Free (F.map tf ~f:(map ~f))
-
-    let map = `Custom map
-
-    let return x = Pure x
-
-    let rec bind t ~f =
-      match t with Pure x -> f x | Free tf -> Free (F.map tf ~f:(bind ~f))
-  end
-
-  include T
-  include Monad_let.Make2 (T)
-end
-
-module Make3 (F : Functor.S3) : sig
-  type ('a, 'x, 'y) t = Pure of 'a | Free of (('a, 'x, 'y) t, 'x, 'y) F.t
-
-  include Monad_let.S3 with type ('a, 'x, 'y) t := ('a, 'x, 'y) t
-end = struct
-  module T = struct
-    type ('a, 'x, 'y) t = Pure of 'a | Free of (('a, 'x, 'y) t, 'x, 'y) F.t
-
-    let rec map t ~f =
-      match t with
-      | Pure x ->
-          Pure (f x)
-      | Free tf ->
-          Free (F.map tf ~f:(map ~f))
-
-    let map = `Custom map
-
-    let return x = Pure x
-
-    let rec bind t ~f =
-      match t with Pure x -> f x | Free tf -> Free (F.map tf ~f:(bind ~f))
-  end
-
-  include T
-  include Monad_let.Make3 (T)
-end
diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml
index bf06a9b46e..df1e433e1f 100644
--- a/src/base/snarky_backendless.ml
+++ b/src/base/snarky_backendless.ml
@@ -13,7 +13,6 @@ module Cvar = Cvar
 module Enumerable = Enumerable
 module Enumerable_intf = Enumerable_intf
 module Field_intf = Snarky_intf.Field
-module Free_monad = Free_monad
 module H_list = H_list
 module Handle = Handle
 module Merkle_tree = Merkle_tree
diff --git a/src/snarky.ml b/src/snarky.ml
index ea15b29258..190f362933 100644
--- a/src/snarky.ml
+++ b/src/snarky.ml
@@ -13,7 +13,6 @@ module Cvar = Snarky_backendless.Cvar
 module Enumerable = Snarky_backendless.Enumerable
 module Enumerable_intf = Snarky_backendless.Enumerable_intf
 module Field_intf = Snarky_intf.Field
-module Free_monad = Snarky_backendless.Free_monad
 module H_list = H_list
 module Handle = Snarky_backendless.Handle
 module Merkle_tree = Snarky_backendless.Merkle_tree

From 905da2e3aa55cf5d9746d379aa44a8d432499145 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Wed, 11 Dec 2024 16:47:23 +0000
Subject: [PATCH 05/12] Remove now-unused Typ toplevel module

---
 src/base/snarky_backendless.ml | 1 -
 src/snarky.ml                  | 1 -
 2 files changed, 2 deletions(-)

diff --git a/src/base/snarky_backendless.ml b/src/base/snarky_backendless.ml
index df1e433e1f..55b31bf8ba 100644
--- a/src/base/snarky_backendless.ml
+++ b/src/base/snarky_backendless.ml
@@ -27,5 +27,4 @@ module Run_state = Run_state
 module Snark = Snark
 module Snark0 = Snark0
 module Snark_intf = Snark_intf
-module Typ = Typ
 module Types = Types
diff --git a/src/snarky.ml b/src/snarky.ml
index 190f362933..08d3fbdd24 100644
--- a/src/snarky.ml
+++ b/src/snarky.ml
@@ -27,5 +27,4 @@ module Run_state = Snarky_backendless.Run_state
 module Snark = Snark
 module Snark0 = Snarky_backendless.Snark0
 module Snark_intf = Snarky_backendless.Snark_intf
-module Typ = Snarky_backendless.Typ
 module Types = Snarky_backendless.Types

From 889a5b66dadc64f758ef0365db0ec0f8a0b4c97b Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Wed, 11 Dec 2024 16:55:20 +0000
Subject: [PATCH 06/12] Remove unused function

---
 src/base/typ.ml | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/src/base/typ.ml b/src/base/typ.ml
index c98f0505ac..35aeb9d14c 100644
--- a/src/base/typ.ml
+++ b/src/base/typ.ml
@@ -108,19 +108,6 @@ module Make (Checked : Checked_monad) = struct
             * ('r_var, 'r_value, 'k_var, 'k_value, 'field) t
             -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value, 'field) t
         | [] : ('r_var, 'r_value, 'r_var, 'r_value, 'field) t
-
-      let size t =
-        let rec go :
-            type r_var r_value k_var k_value.
-            int -> (r_var, r_value, k_var, k_value, 'f) t -> int =
-         fun acc t ->
-          match t with
-          | [] ->
-              acc
-          | Typ { size_in_field_elements; _ } :: t' ->
-              go (acc + size_in_field_elements) t'
-        in
-        go 0 t
     end
 
     let unit () : (unit, unit, 'field) t =

From 98805117bcce13e09a6e7de0da24ed2e50e9b267 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Wed, 11 Dec 2024 17:57:17 +0000
Subject: [PATCH 07/12] Replace Typ.Internal and As_prover.Ref with
 prover_value

---
 src/base/as_prover_ref.ml | 68 ---------------------------------------
 src/base/snark0.ml        | 28 +++-------------
 src/base/snark_intf.ml    | 60 ++++------------------------------
 src/base/typ.ml           | 23 ++++++-------
 4 files changed, 19 insertions(+), 160 deletions(-)
 delete mode 100644 src/base/as_prover_ref.ml

diff --git a/src/base/as_prover_ref.ml b/src/base/as_prover_ref.ml
deleted file mode 100644
index a818f29605..0000000000
--- a/src/base/as_prover_ref.ml
+++ /dev/null
@@ -1,68 +0,0 @@
-open Core_kernel
-
-type 'a t = 'a option ref
-
-module Make_ref_typ (Checked : Monad_let.S2) = struct
-  let typ : ('a t, 'a, _, _) Types.Typ.t =
-    Typ
-      { var_to_fields = (fun x -> ([||], !x))
-      ; var_of_fields = (fun (_, x) -> ref x)
-      ; value_to_fields = (fun x -> ([||], Some x))
-      ; value_of_fields = (fun (_, x) -> Option.value_exn x)
-      ; size_in_field_elements = 0
-      ; constraint_system_auxiliary = (fun () -> None)
-      ; check = (fun _ -> Checked.return ())
-      }
-end
-
-module type S = sig
-  module Types : Types.Types
-
-  type ('a, 'f) checked
-
-  type 'f field
-
-  type nonrec 'a t = 'a t
-
-  val create : ('a, 'f field) As_prover0.t -> ('a t, 'f field) checked
-
-  val get : 'a t -> ('a, 'f field) As_prover0.t
-
-  val set : 'a t -> 'a -> (unit, 'f field) As_prover0.t
-end
-
-module Make
-    (Checked : Checked_intf.S)
-    (As_prover : As_prover_intf.Basic
-                   with type 'f field := 'f Checked.field
-                    and type ('a, 'f) Provider.t =
-                     ('a, 'f) Checked.Types.Provider.t) :
-  S
-    with module Types = Checked.Types
-     and type ('a, 'f) checked := ('a, 'f) Checked.t
-     and type 'f field = 'f Checked.field = struct
-  module Types = Checked.Types
-
-  type 'f field = 'f Checked.field
-
-  type nonrec 'a t = 'a t
-
-  let create (x : ('a, 'f Checked.field) As_prover.t) :
-      ('a t, 'f Checked.field) Checked.t =
-    let r = ref None in
-    let open Checked in
-    let%map () =
-      Checked.as_prover (As_prover.map x ~f:(fun x -> r := Some x))
-    in
-    r
-
-  open As_prover.Let_syntax
-
-  let get (r : 'a t) =
-    let%map () = As_prover.return () in
-    Option.value_exn !r
-
-  let set (r : 'a t) x =
-    let%map () = As_prover.return () in
-    r := Some x
-end
diff --git a/src/base/snark0.ml b/src/base/snark0.ml
index 6fcef9c5fa..b0ed161e97 100644
--- a/src/base/snark0.ml
+++ b/src/base/snark0.ml
@@ -12,10 +12,6 @@ module Make_basic
     (Backend : Backend_extended.S)
     (Checked : Checked_intf.Extended with type field = Backend.Field.t)
     (As_prover : As_prover0.Extended with type field := Backend.Field.t)
-    (Ref : As_prover_ref.S
-             with module Types := Checked.Types
-              and type 'f field := Backend.Field.t
-              and type ('a, 'f) checked := 'a Checked.t)
     (Runner : Runner.S
                 with module Types := Checked.Types
                 with type field := Backend.Field.t
@@ -659,13 +655,6 @@ module Make (Backend : Backend_intf.S) = struct
 
   module As_prover_ext = As_prover0.Make_extended (Field_T) (As_prover0)
 
-  module Ref :
-    As_prover_ref.S
-      with module Types = Checked1.Types
-       and type ('a, 'f) checked := ('a, 'f) Checked1.t
-       and type 'f field := Backend_extended.Field.t =
-    As_prover_ref.Make (Checked1) (As_prover0)
-
   module Checked_for_basic = struct
     include (
       Checked1 :
@@ -682,8 +671,7 @@ module Make (Backend : Backend_intf.S) = struct
   end
 
   module Basic =
-    Make_basic (Backend_extended) (Checked_for_basic) (As_prover_ext) (Ref)
-      (Runner0)
+    Make_basic (Backend_extended) (Checked_for_basic) (As_prover_ext) (Runner0)
   include Basic
   module Number = Number.Make (Basic)
   module Enumerable = Enumerable.Make (Basic)
@@ -795,7 +783,9 @@ module Run = struct
 
       let of_hlistable = of_hlistable
 
-      module Internal = Internal
+      type nonrec 'a prover_value = 'a prover_value
+
+      let prover_value = prover_value
     end
 
     let constant (Typ typ : _ Typ.t) x =
@@ -1133,16 +1123,6 @@ module Run = struct
 
       include Field.Constant.T
 
-      module Ref = struct
-        type 'a t = 'a As_prover_ref.t
-
-        let create f = run As_prover.(Ref.create (map (return ()) ~f))
-
-        let get r = eval_as_prover (As_prover.Ref.get r)
-
-        let set r x = eval_as_prover (As_prover.Ref.set r x)
-      end
-
       let run_prover f _tbl =
         (* Allow for nesting of prover blocks, by caching the current value and
            restoring it once we're done.
diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml
index 718a837821..e5164b7110 100644
--- a/src/base/snark_intf.ml
+++ b/src/base/snark_intf.ml
@@ -133,8 +133,6 @@ module type Typ_intf = sig
 
   type checked_unit
 
-  type _ prover_ref
-
   type ('var, 'value, 'aux, 'field, 'checked) typ' =
     { var_to_fields : 'var -> 'field Cvar.t array * 'aux
     ; var_of_fields : 'field Cvar.t array * 'aux -> 'var
@@ -256,33 +254,15 @@ module type Typ_intf = sig
     -> value_of_hlist:((unit, 'k_value) H_list.t -> 'value)
     -> ('var, 'value) t
 
-  (** [Typ.t]s that make it easier to write a [Typ.t] for a mix of R1CS data
-        and normal OCaml data.
-
-        Using this module is not recommended.
-    *)
-  module Internal : sig
-    (** A do-nothing [Typ.t] that returns the input value for all modes. This
-          may be used to convert objects from the [Checked] world into and
-          through [As_prover] blocks.
+  type _ prover_value
 
-          This is the dual of [ref], which allows [OCaml] values from
-          [As_prover] blocks to pass through the [Checked] world.
-
-          Note: Reading or writing using this [Typ.t] will assert that the
-          argument and the value stored are physically equal -- ie. that they
-          refer to the same object.
-      *)
-    val snarkless : 'a -> ('a, 'a) t
-
-    (** A [Typ.t] for marshalling OCaml values generated in [As_prover]
+  (** A [Typ.t] for marshalling OCaml values generated in [As_prover]
           blocks, while keeping them opaque to the [Checked] world.
 
           This is the dual of [snarkless], which allows [OCaml] values from the
           [Checked] world to pass through [As_prover] blocks.
     *)
-    val ref : unit -> ('a As_prover_ref.t, 'a) t
-  end
+  val prover_value : unit -> ('a prover_value, 'a) t
 end
 
 module type Constraint_intf = sig
@@ -606,7 +586,6 @@ module type Basic = sig
          and type field_var := Field.Var.t
          and type checked_unit := unit Checked.t
          and type _ checked := unit Checked.t
-         and type 'a prover_ref := 'a As_prover_ref.t
   end
 
   (** Representation of booleans within a field.
@@ -736,19 +715,6 @@ let multiply3 (x : Field.Var.t) (y : Field.Var.t) (z : Field.Var.t)
 
     type 'a as_prover = 'a t
 
-    (** Mutable references for use by the prover in a checked computation. *)
-    module Ref : sig
-      (** A mutable reference to an ['a] value, which may be used in checked
-          computations. *)
-      type 'a t = 'a As_prover_ref.t
-
-      val create : 'a as_prover -> 'a t Checked.t
-
-      val get : 'a t -> 'a as_prover
-
-      val set : 'a t -> 'a -> unit as_prover
-    end
-
     include Monad_let.S with type 'a t := 'a t
 
     (** Combine 2 {!type:As_prover.t} blocks using another function. *)
@@ -1160,8 +1126,7 @@ module type Run_basic = sig
       with type field := Field.Constant.t
        and type field_var := Field.t
        and type checked_unit := unit Internal_Basic.Checked.t
-       and type _ checked := unit
-       and type 'a prover_ref := 'a As_prover_ref.t)
+       and type _ checked := unit)
 
   (** Representation of booleans within a field.
 
@@ -1240,19 +1205,6 @@ module type Run_basic = sig
 
     type 'a as_prover = 'a t
 
-    (** Opaque references for use by the prover in a checked computation. *)
-    module Ref : sig
-      (** A mutable reference to an ['a] value, which may be used in checked
-          computations. *)
-      type 'a t = 'a As_prover_ref.t
-
-      val create : (unit -> 'a) as_prover -> 'a t
-
-      val get : 'a t -> 'a as_prover
-
-      val set : 'a t -> 'a -> unit as_prover
-    end
-
     val in_prover_block : unit -> bool
 
     val read_var : Field.t -> Field.Constant.t
@@ -1278,11 +1230,11 @@ module type Run_basic = sig
     (Basic
       with type field = field
        and type 'a Checked.t = ('a, field) Checked_runner.Simple.t
-       and type 'a As_prover.Ref.t = 'a As_prover_ref.t
        and type ('var, 'value, 'aux, 'field, 'checked) Typ.typ' =
         ('var, 'value, 'aux, 'field, 'checked) Typ.typ'
        and type ('var, 'value, 'field, 'checked) Typ.typ =
-        ('var, 'value, 'field, 'checked) Typ.typ)
+        ('var, 'value, 'field, 'checked) Typ.typ
+       and type 'a Typ.prover_value = 'a Typ.prover_value)
 
   module Bitstring_checked : sig
     type t = Boolean.var list
diff --git a/src/base/typ.ml b/src/base/typ.ml
index 35aeb9d14c..90da372dc5 100644
--- a/src/base/typ.ml
+++ b/src/base/typ.ml
@@ -132,24 +132,19 @@ module Make (Checked : Checked_monad) = struct
         ; check = (fun _ -> Checked.return ())
         }
 
-    module Internal = struct
-      let snarkless value : _ t =
+    include struct
+      type 'a prover_value = 'a option
+
+      let prover_value () : _ t =
         Typ
-          { var_to_fields = (fun _ -> ([||], ()))
-          ; var_of_fields = (fun _ -> value)
-          ; value_to_fields =
-              (fun value' ->
-                assert (phys_equal value value') ;
-                ([||], ()) )
-          ; value_of_fields = (fun _ -> value)
+          { var_to_fields = (fun x -> ([||], x))
+          ; var_of_fields = (fun (_, x) -> x)
+          ; value_to_fields = (fun x -> ([||], Some x))
+          ; value_of_fields = (fun (_, x) -> Option.value_exn x)
           ; size_in_field_elements = 0
-          ; constraint_system_auxiliary = (fun () -> ())
+          ; constraint_system_auxiliary = (fun () -> None)
           ; check = (fun _ -> Checked.return ())
           }
-
-      module Ref_typ = As_prover_ref.Make_ref_typ (Checked)
-
-      let ref () = Ref_typ.typ
     end
 
     let transport (type var value1 value2 field)

From a06b3a595d0cbc79dee6ee1f0702ad03fb3a5d65 Mon Sep 17 00:00:00 2001
From: Danny Willems <be.danny.willems@gmail.com>
Date: Thu, 12 Dec 2024 10:31:56 +0100
Subject: [PATCH 08/12] CI: bump up actions/checkout to v4 + use newest v and
 path for ocaml

---
 .github/workflows/build.yml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index f61322cddf..ea0217db85 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -18,12 +18,13 @@ jobs:
 
     steps:
       - name: Get code
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
 
       - name: Use OCaml ${{ matrix.ocaml-version }}
-        uses: avsm/setup-ocaml@v1
+        uses: ocaml/setup-ocaml@v3
         with:
-          ocaml-version: ${{ matrix.ocaml-version }}
+          ocaml-compiler: ${{ matrix.ocaml-version }}
+          disable-cache: true
 
       - name: Build
         run: |

From d9daae6f7a0f256faab330f629516ed9404dc7ce Mon Sep 17 00:00:00 2001
From: Danny Willems <be.danny.willems@gmail.com>
Date: Thu, 12 Dec 2024 10:38:35 +0100
Subject: [PATCH 09/12] CI/build: use relatively more modern syntax

---
 .github/workflows/build.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index ea0217db85..e0263e4861 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -1,7 +1,7 @@
 name: Check build
 
 on:
-  [pull_request]
+  pull_request:
 
 jobs:
   check_build:

From 89855ba0c7bd0cf5f9dc403dc09f4838b58d94a1 Mon Sep 17 00:00:00 2001
From: Danny Willems <be.danny.willems@gmail.com>
Date: Thu, 12 Dec 2024 10:38:53 +0100
Subject: [PATCH 10/12] CI/docker: use relatively more modern syntax

---
 .github/workflows/docker.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
index 6e5c4e9758..bac27b1429 100644
--- a/.github/workflows/docker.yml
+++ b/.github/workflows/docker.yml
@@ -1,7 +1,7 @@
 name: ci
 
 on:
-  [pull_request]
+  pull_request:
 
 jobs:
   docker-build:

From ab55c6dc8e6a44ea5a2a39157789881a31998ac2 Mon Sep 17 00:00:00 2001
From: Danny Willems <be.danny.willems@gmail.com>
Date: Thu, 12 Dec 2024 10:39:09 +0100
Subject: [PATCH 11/12] CI/docs: replace tabs by spaces to have smth uniform

---
 .github/workflows/docs.yml | 62 ++++++++++++++++++--------------------
 1 file changed, 30 insertions(+), 32 deletions(-)

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 266d5d94ca..605863148e 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -1,39 +1,37 @@
 name: Deploy Docs to GitHub Pages
 
 on:
-    push:
-        branches:
-            - master
+  push:
+    branches:
+      - master
 
 jobs:
-    release:
-        name: GitHub Pages
-        runs-on: ubuntu-latest
+  release:
+    name: GitHub Pages
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v2
 
-        steps:
-            - name: Checkout Repository
-              uses: actions/checkout@v2
+      - name: Use OCaml "4.14.0"
+        uses: avsm/setup-ocaml@v1
+        with:
+          ocaml-version: 4.14.0
 
-            - name: Use OCaml "4.14.0"
-              uses: avsm/setup-ocaml@v1
-              with:
-                ocaml-version: 4.14.0
-              
-            - name: Build Documentation
-              run: |
-                eval $(opam env)
-                opam pin add . -y
-                opam install odoc
-                make website
-                cd website/website
-                yarn
-                yarn build
-                pwd
-                ls
-                ls build
-
-            - name: Deploy
-              uses: peaceiris/actions-gh-pages@v3
-              with:
-                github_token: ${{ secrets.GITHUB_TOKEN }}
-                publish_dir: ./website/website/build/snarky
+      - name: Build Documentation
+        run: |
+          eval $(opam env)
+          opam pin add . -y
+          opam install odoc
+          make website
+          cd website/website
+          yarn
+          yarn build
+          pwd
+          ls
+          ls build
+      - name: Deploy
+        uses: peaceiris/actions-gh-pages@v3
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          publish_dir: ./website/website/build/snarky

From e343a65393bcd1da41671b7f12148a89e2cca020 Mon Sep 17 00:00:00 2001
From: Danny Willems <be.danny.willems@gmail.com>
Date: Thu, 12 Dec 2024 10:39:31 +0100
Subject: [PATCH 12/12] CI/docker: bump up GH actions versions

---
 .github/workflows/docker.yml | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
index bac27b1429..3c3e58365c 100644
--- a/.github/workflows/docker.yml
+++ b/.github/workflows/docker.yml
@@ -7,15 +7,12 @@ jobs:
   docker-build:
     runs-on: ubuntu-latest
     steps:
-      -
-        name: Checkout
-        uses: actions/checkout@v2
-      -
-        uses: docker/setup-buildx-action@v1
+      - name: Checkout
+        uses: actions/checkout@v4
+      - uses: docker/setup-buildx-action@v3
         id: docker-build
         with:
           install: true
-      -
-        name: Build
+      - name: Build
         run: |
           docker build . # will run buildx