From 56a10dd34714ff077dad7f9507cc77250423d3d2 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 03:47:08 +0000 Subject: [PATCH 01/52] Split collect_input_constraints --- src/base/runners.ml | 35 ++++++++++++++++++++++++++++------- 1 file changed, 28 insertions(+), 7 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 30faa2088..233732454 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -186,8 +186,8 @@ struct Field.Vector.emplace_back primary_input x ; v - let collect_input_constraints : - type checked input_var input_value. + let allocate_public_inputs : + type input_var input_value output_var output_value. int ref -> input_typ: ( input_var @@ -195,12 +195,15 @@ struct , field , (unit, field) Checked.Types.Checked.t ) Types.Typ.typ - -> return_typ:_ Types.Typ.t - -> (unit -> input_var -> checked) - -> _ * (unit -> checked) Checked.t = - fun next_input ~input_typ:(Typ input_typ) ~return_typ:(Typ return_typ) k -> + -> return_typ: + ( output_var + , output_value + , field + , (unit, field) Checked.Types.Checked.t ) + Types.Typ.t + -> input_var * output_var = + fun next_input ~input_typ:(Typ input_typ) ~return_typ:(Typ return_typ) -> (* allocate variables for the public input and the public output *) - let open Checked in let alloc_input { Types0.Typ.var_of_fields ; size_in_field_elements @@ -214,7 +217,25 @@ struct in let var = alloc_input input_typ in let retval = alloc_input return_typ in + (var, retval) + let collect_input_constraints : + type checked input_var input_value. + int ref + -> input_typ: + ( input_var + , input_value + , field + , (unit, field) Checked.Types.Checked.t ) + Types.Typ.typ + -> return_typ:_ Types.Typ.t + -> (unit -> input_var -> checked) + -> _ * (unit -> checked) Checked.t = + fun next_input ~input_typ:(Typ input_typ) ~return_typ k -> + let var, retval = + allocate_public_inputs next_input ~input_typ:(Typ input_typ) ~return_typ + in + let open Checked in (* create constraints to validate the input (using the input [Typ]'s [check]) *) let circuit = let%bind () = input_typ.check var in From 8db1ec00a4766a4c600dd4d6bf415952d3d4aa09 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 03:49:37 +0000 Subject: [PATCH 02/52] Beta-reduce collect_input_constraints --- src/base/runners.ml | 39 +++++++++++++-------------------------- 1 file changed, 13 insertions(+), 26 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 233732454..78412bf05 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -219,30 +219,6 @@ struct let retval = alloc_input return_typ in (var, retval) - let collect_input_constraints : - type checked input_var input_value. - int ref - -> input_typ: - ( input_var - , input_value - , field - , (unit, field) Checked.Types.Checked.t ) - Types.Typ.typ - -> return_typ:_ Types.Typ.t - -> (unit -> input_var -> checked) - -> _ * (unit -> checked) Checked.t = - fun next_input ~input_typ:(Typ input_typ) ~return_typ k -> - let var, retval = - allocate_public_inputs next_input ~input_typ:(Typ input_typ) ~return_typ - in - let open Checked in - (* create constraints to validate the input (using the input [Typ]'s [check]) *) - let circuit = - let%bind () = input_typ.check var in - Checked.return (fun () -> k () var) - in - (retval, circuit) - let r1cs_h : type a checked input_var input_value retval. run:(a, checked) Runner.run @@ -259,8 +235,19 @@ struct fun ~run next_input ~input_typ ~return_typ k -> (* allocate variables for the public input and the public output *) let retval, checked = - collect_input_constraints next_input ~input_typ ~return_typ (fun () -> - k ) + let var, retval = + allocate_public_inputs next_input ~input_typ ~return_typ + in + let open Checked in + (* create constraints to validate the input (using the input [Typ]'s [check]) *) + let circuit = + let%bind () = + let (Typ input_typ) = input_typ in + input_typ.check var + in + Checked.return (fun () -> k var) + in + (retval, circuit) in (* ? *) From d781a339df2385da7c1ba7c219ba7cf36d757cc2 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 03:51:59 +0000 Subject: [PATCH 03/52] Name-discriminate constraint_system functions --- src/base/runners.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 78412bf05..a7b49f4ed 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -45,7 +45,7 @@ struct module Runner = Runner (* TODO-someday: Add pass to unify variables which have an Equal constraint *) - let constraint_system ~run ~num_inputs ~return_typ:(Types.Typ.Typ return_typ) + let constraint_systemy ~run ~num_inputs ~return_typ:(Types.Typ.Typ return_typ) output t : R1CS_constraint_system.t = let input = field_vec () in let next_auxiliary = ref num_inputs in @@ -257,7 +257,7 @@ struct in (* ? *) - constraint_system ~run:run_in_run ~num_inputs:!next_input ~return_typ + constraint_systemy ~run:run_in_run ~num_inputs:!next_input ~return_typ retval (Checked.map ~f:(fun r -> r ()) checked) From 71594cedb12681b6f7d87de9008fe99fa95896de Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 03:53:09 +0000 Subject: [PATCH 04/52] Inline definition of constraint_system --- src/base/runners.ml | 46 +++++++++++++++++++++++---------------------- 1 file changed, 24 insertions(+), 22 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index a7b49f4ed..0eaadb541 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -44,28 +44,6 @@ struct module Runner = Runner - (* TODO-someday: Add pass to unify variables which have an Equal constraint *) - let constraint_systemy ~run ~num_inputs ~return_typ:(Types.Typ.Typ return_typ) - output t : R1CS_constraint_system.t = - let input = field_vec () in - let next_auxiliary = ref num_inputs in - let aux = field_vec () in - let system = R1CS_constraint_system.create () in - let state = - Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system - ~with_witness:false () - in - let state, res = run t state in - let res, _ = return_typ.var_to_fields res in - let output, _ = return_typ.var_to_fields output in - let _state = - Array.fold2_exn ~init:state res output ~f:(fun state res output -> - fst @@ Checked.run (Checked.assert_equal res output) state ) - in - let auxiliary_input_size = !next_auxiliary - num_inputs in - R1CS_constraint_system.set_auxiliary_input_size system auxiliary_input_size ; - system - let auxiliary_input ?system ~run ~num_inputs ?(handlers = ([] : Handler.t list)) t0 (input : Field.Vector.t) ~return_typ:(Types.Typ.Typ return_typ) ~output : Field.Vector.t * _ = @@ -256,6 +234,30 @@ struct run x state in + let constraint_systemy ~run ~num_inputs + ~return_typ:(Types.Typ.Typ return_typ) output t : + R1CS_constraint_system.t = + let input = field_vec () in + let next_auxiliary = ref num_inputs in + let aux = field_vec () in + let system = R1CS_constraint_system.create () in + let state = + Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system + ~with_witness:false () + in + let state, res = run t state in + let res, _ = return_typ.var_to_fields res in + let output, _ = return_typ.var_to_fields output in + let _state = + Array.fold2_exn ~init:state res output ~f:(fun state res output -> + fst @@ Checked.run (Checked.assert_equal res output) state ) + in + let auxiliary_input_size = !next_auxiliary - num_inputs in + R1CS_constraint_system.set_auxiliary_input_size system + auxiliary_input_size ; + system + in + (* ? *) constraint_systemy ~run:run_in_run ~num_inputs:!next_input ~return_typ retval From 0e7984fb3074920afac1ca9e196c2369ffbcd308 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 03:56:06 +0000 Subject: [PATCH 05/52] Inline run --- src/base/runners.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 0eaadb541..05d50a7da 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -234,9 +234,8 @@ struct run x state in - let constraint_systemy ~run ~num_inputs - ~return_typ:(Types.Typ.Typ return_typ) output t : - R1CS_constraint_system.t = + let constraint_systemy ~num_inputs ~return_typ:(Types.Typ.Typ return_typ) + output t : R1CS_constraint_system.t = let input = field_vec () in let next_auxiliary = ref num_inputs in let aux = field_vec () in @@ -245,7 +244,7 @@ struct Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system ~with_witness:false () in - let state, res = run t state in + let state, res = run_in_run t state in let res, _ = return_typ.var_to_fields res in let output, _ = return_typ.var_to_fields output in let _state = @@ -259,8 +258,7 @@ struct in (* ? *) - constraint_systemy ~run:run_in_run ~num_inputs:!next_input ~return_typ - retval + constraint_systemy ~num_inputs:!next_input ~return_typ retval (Checked.map ~f:(fun r -> r ()) checked) let constraint_system (type a checked input_var) : From de64beb0ac2fa44e2a10e4ed93dd94954c920972 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 03:57:11 +0000 Subject: [PATCH 06/52] Inline next_input --- src/base/runners.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 05d50a7da..1642f88c6 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -234,8 +234,9 @@ struct run x state in - let constraint_systemy ~num_inputs ~return_typ:(Types.Typ.Typ return_typ) - output t : R1CS_constraint_system.t = + let constraint_systemy ~return_typ:(Types.Typ.Typ return_typ) output t : + R1CS_constraint_system.t = + let num_inputs = !next_input in let input = field_vec () in let next_auxiliary = ref num_inputs in let aux = field_vec () in @@ -258,7 +259,7 @@ struct in (* ? *) - constraint_systemy ~num_inputs:!next_input ~return_typ retval + constraint_systemy ~return_typ retval (Checked.map ~f:(fun r -> r ()) checked) let constraint_system (type a checked input_var) : From df6520622b67728b21be1f6b5f1505f94d34cb1b Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 03:58:33 +0000 Subject: [PATCH 07/52] beta-reduce run_in_run --- src/base/runners.ml | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 1642f88c6..81b0b29e0 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -228,12 +228,6 @@ struct (retval, circuit) in - (* ? *) - let run_in_run checked state = - let state, x = Checked.run checked state in - run x state - in - let constraint_systemy ~return_typ:(Types.Typ.Typ return_typ) output t : R1CS_constraint_system.t = let num_inputs = !next_input in @@ -245,7 +239,10 @@ struct Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system ~with_witness:false () in - let state, res = run_in_run t state in + let state, res = + let state, x = Checked.run t state in + run x state + in let res, _ = return_typ.var_to_fields res in let output, _ = return_typ.var_to_fields output in let _state = From 2892d624c812f9f4e6418b446de1ea0fc9174fae Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:00:08 +0000 Subject: [PATCH 08/52] Inline checked map --- src/base/runners.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 81b0b29e0..17e10532b 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -240,7 +240,7 @@ struct ~with_witness:false () in let state, res = - let state, x = Checked.run t state in + let state, x = Checked.run (Checked.map ~f:(fun r -> r ()) t) state in run x state in let res, _ = return_typ.var_to_fields res in @@ -256,8 +256,7 @@ struct in (* ? *) - constraint_systemy ~return_typ retval - (Checked.map ~f:(fun r -> r ()) checked) + constraint_systemy ~return_typ retval checked let constraint_system (type a checked input_var) : run:(a, checked) Runner.run From f0c1dce128e254483dcab6b98d7e89bb49e18ee9 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:02:06 +0000 Subject: [PATCH 09/52] Inline return_typ --- src/base/runners.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 17e10532b..baa06e50c 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -228,8 +228,8 @@ struct (retval, circuit) in - let constraint_systemy ~return_typ:(Types.Typ.Typ return_typ) output t : - R1CS_constraint_system.t = + let constraint_systemy output t : R1CS_constraint_system.t = + let (Typ return_typ) = return_typ in let num_inputs = !next_input in let input = field_vec () in let next_auxiliary = ref num_inputs in @@ -256,7 +256,7 @@ struct in (* ? *) - constraint_systemy ~return_typ retval checked + constraint_systemy retval checked let constraint_system (type a checked input_var) : run:(a, checked) Runner.run From 17e550cc81613e89c7dda0d6a2b0e3d4f1807837 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:03:13 +0000 Subject: [PATCH 10/52] Standardize naming --- src/base/runners.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index baa06e50c..9baf5ca4f 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -212,8 +212,8 @@ struct -> R1CS_constraint_system.t = fun ~run next_input ~input_typ ~return_typ k -> (* allocate variables for the public input and the public output *) - let retval, checked = - let var, retval = + let retvar, checked = + let var, retvar = allocate_public_inputs next_input ~input_typ ~return_typ in let open Checked in @@ -225,10 +225,10 @@ struct in Checked.return (fun () -> k var) in - (retval, circuit) + (retvar, circuit) in - let constraint_systemy output t : R1CS_constraint_system.t = + let constraint_systemy retvar t : R1CS_constraint_system.t = let (Typ return_typ) = return_typ in let num_inputs = !next_input in let input = field_vec () in @@ -244,10 +244,10 @@ struct run x state in let res, _ = return_typ.var_to_fields res in - let output, _ = return_typ.var_to_fields output in + let retvar, _ = return_typ.var_to_fields retvar in let _state = - Array.fold2_exn ~init:state res output ~f:(fun state res output -> - fst @@ Checked.run (Checked.assert_equal res output) state ) + Array.fold2_exn ~init:state res retvar ~f:(fun state res retvar -> + fst @@ Checked.run (Checked.assert_equal res retvar) state ) in let auxiliary_input_size = !next_auxiliary - num_inputs in R1CS_constraint_system.set_auxiliary_input_size system @@ -256,7 +256,7 @@ struct in (* ? *) - constraint_systemy retval checked + constraint_systemy retvar checked let constraint_system (type a checked input_var) : run:(a, checked) Runner.run From e06c2d961caa5d162a3d58cf12e870cddd2b685e Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:04:07 +0000 Subject: [PATCH 11/52] Inline retvar --- src/base/runners.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 9baf5ca4f..f591cd1ac 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -228,7 +228,7 @@ struct (retvar, circuit) in - let constraint_systemy retvar t : R1CS_constraint_system.t = + let constraint_systemy t : R1CS_constraint_system.t = let (Typ return_typ) = return_typ in let num_inputs = !next_input in let input = field_vec () in @@ -256,7 +256,7 @@ struct in (* ? *) - constraint_systemy retvar checked + constraint_systemy checked let constraint_system (type a checked input_var) : run:(a, checked) Runner.run From b78d39ac6bf3fbde3d200c75e19f9ecfe8036584 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:05:02 +0000 Subject: [PATCH 12/52] Rename t to checked --- src/base/runners.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index f591cd1ac..8359e1727 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -228,7 +228,7 @@ struct (retvar, circuit) in - let constraint_systemy t : R1CS_constraint_system.t = + let constraint_systemy checked : R1CS_constraint_system.t = let (Typ return_typ) = return_typ in let num_inputs = !next_input in let input = field_vec () in @@ -240,7 +240,9 @@ struct ~with_witness:false () in let state, res = - let state, x = Checked.run (Checked.map ~f:(fun r -> r ()) t) state in + let state, x = + Checked.run (Checked.map ~f:(fun r -> r ()) checked) state + in run x state in let res, _ = return_typ.var_to_fields res in From 3ebb39ed007ff508235bb63079cf3849111f0964 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:05:47 +0000 Subject: [PATCH 13/52] Beta-reduce constraint_systemy --- src/base/runners.ml | 53 ++++++++++++++++++++------------------------- 1 file changed, 24 insertions(+), 29 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 8359e1727..c5446f068 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -228,37 +228,32 @@ struct (retvar, circuit) in - let constraint_systemy checked : R1CS_constraint_system.t = - let (Typ return_typ) = return_typ in - let num_inputs = !next_input in - let input = field_vec () in - let next_auxiliary = ref num_inputs in - let aux = field_vec () in - let system = R1CS_constraint_system.create () in - let state = - Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system - ~with_witness:false () - in - let state, res = - let state, x = - Checked.run (Checked.map ~f:(fun r -> r ()) checked) state - in - run x state - in - let res, _ = return_typ.var_to_fields res in - let retvar, _ = return_typ.var_to_fields retvar in - let _state = - Array.fold2_exn ~init:state res retvar ~f:(fun state res retvar -> - fst @@ Checked.run (Checked.assert_equal res retvar) state ) + let (Typ return_typ) = return_typ in + let num_inputs = !next_input in + let input = field_vec () in + let next_auxiliary = ref num_inputs in + let aux = field_vec () in + let system = R1CS_constraint_system.create () in + let state = + Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system + ~with_witness:false () + in + let state, res = + let state, x = + Checked.run (Checked.map ~f:(fun r -> r ()) checked) state in - let auxiliary_input_size = !next_auxiliary - num_inputs in - R1CS_constraint_system.set_auxiliary_input_size system - auxiliary_input_size ; - system + run x state in - - (* ? *) - constraint_systemy checked + let res, _ = return_typ.var_to_fields res in + let retvar, _ = return_typ.var_to_fields retvar in + let _state = + Array.fold2_exn ~init:state res retvar ~f:(fun state res retvar -> + fst @@ Checked.run (Checked.assert_equal res retvar) state ) + in + let auxiliary_input_size = !next_auxiliary - num_inputs in + R1CS_constraint_system.set_auxiliary_input_size system + auxiliary_input_size ; + system let constraint_system (type a checked input_var) : run:(a, checked) Runner.run From d6ed2a7408c044bb6bc903754c41461976cbac6f Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:07:32 +0000 Subject: [PATCH 14/52] Flatten function --- src/base/runners.ml | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index c5446f068..b87f2b0a7 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -212,20 +212,17 @@ struct -> R1CS_constraint_system.t = fun ~run next_input ~input_typ ~return_typ k -> (* allocate variables for the public input and the public output *) - let retvar, checked = - let var, retvar = - allocate_public_inputs next_input ~input_typ ~return_typ - in + let var, retvar = + allocate_public_inputs next_input ~input_typ ~return_typ + in + (* create constraints to validate the input (using the input [Typ]'s [check]) *) + let checked = let open Checked in - (* create constraints to validate the input (using the input [Typ]'s [check]) *) - let circuit = - let%bind () = - let (Typ input_typ) = input_typ in - input_typ.check var - in - Checked.return (fun () -> k var) + let%bind () = + let (Typ input_typ) = input_typ in + input_typ.check var in - (retvar, circuit) + Checked.return (fun () -> k var) in let (Typ return_typ) = return_typ in From eda32784ede2359f9cbf17a0229b044b8331e734 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:08:09 +0000 Subject: [PATCH 15/52] Inline calculation of checked --- src/base/runners.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index b87f2b0a7..ad0012a9a 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -215,16 +215,6 @@ struct let var, retvar = allocate_public_inputs next_input ~input_typ ~return_typ in - (* create constraints to validate the input (using the input [Typ]'s [check]) *) - let checked = - let open Checked in - let%bind () = - let (Typ input_typ) = input_typ in - input_typ.check var - in - Checked.return (fun () -> k var) - in - let (Typ return_typ) = return_typ in let num_inputs = !next_input in let input = field_vec () in @@ -237,6 +227,16 @@ struct in let state, res = let state, x = + (* create constraints to validate the input (using the input [Typ]'s [check]) *) + let checked = + let open Checked in + let%bind () = + let (Typ input_typ) = input_typ in + input_typ.check var + in + Checked.return (fun () -> k var) + in + Checked.run (Checked.map ~f:(fun r -> r ()) checked) state in run x state From 34c39a342a0e298a9a6925d7588e172b599e7b6e Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:10:39 +0000 Subject: [PATCH 16/52] Separate input validation from main function --- src/base/runners.ml | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index ad0012a9a..e4ba56450 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -226,20 +226,15 @@ struct ~with_witness:false () in let state, res = - let state, x = + let state, () = (* create constraints to validate the input (using the input [Typ]'s [check]) *) let checked = - let open Checked in - let%bind () = - let (Typ input_typ) = input_typ in - input_typ.check var - in - Checked.return (fun () -> k var) + let (Typ input_typ) = input_typ in + input_typ.check var in - - Checked.run (Checked.map ~f:(fun r -> r ()) checked) state + Checked.run checked state in - run x state + run (k var) state in let res, _ = return_typ.var_to_fields res in let retvar, _ = return_typ.var_to_fields retvar in From e742980885f57215d488c1dd486f199c46ab70d1 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:12:50 +0000 Subject: [PATCH 17/52] Beta-reduce next_input parameter --- src/base/runners.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index e4ba56450..86676c5c7 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -200,7 +200,6 @@ struct let r1cs_h : type a checked input_var input_value retval. run:(a, checked) Runner.run - -> int ref -> input_typ: ( input_var , input_value @@ -210,7 +209,8 @@ struct -> return_typ:(a, retval, _, _) Types.Typ.t -> (input_var -> checked) -> R1CS_constraint_system.t = - fun ~run next_input ~input_typ ~return_typ k -> + fun ~run ~input_typ ~return_typ k -> + let next_input = ref 0 in (* allocate variables for the public input and the public output *) let var, retvar = allocate_public_inputs next_input ~input_typ ~return_typ @@ -253,8 +253,7 @@ struct -> return_typ:_ -> (input_var -> checked) -> R1CS_constraint_system.t = - fun ~run ~input_typ ~return_typ k -> - r1cs_h ~run (ref 0) ~input_typ ~return_typ k + fun ~run ~input_typ ~return_typ k -> r1cs_h ~run ~input_typ ~return_typ k let generate_public_input : ('input_var, 'input_value, _, _) Types.Typ.typ From e980851564211377bf1a6e1cc4b840e9a9dc3527 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:13:51 +0000 Subject: [PATCH 18/52] Eta-convert constraint_system --- src/base/runners.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 86676c5c7..8da51376f 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -253,7 +253,7 @@ struct -> return_typ:_ -> (input_var -> checked) -> R1CS_constraint_system.t = - fun ~run ~input_typ ~return_typ k -> r1cs_h ~run ~input_typ ~return_typ k + r1cs_h let generate_public_input : ('input_var, 'input_value, _, _) Types.Typ.typ From 3af8b1f57088672931fe660f969bd44c0f0027db Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:17:30 +0000 Subject: [PATCH 19/52] Lift preamble before computation --- src/base/runners.ml | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 8da51376f..8b482ec96 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -225,17 +225,15 @@ struct Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system ~with_witness:false () in - let state, res = - let state, () = - (* create constraints to validate the input (using the input [Typ]'s [check]) *) - let checked = - let (Typ input_typ) = input_typ in - input_typ.check var - in - Checked.run checked state + let state, () = + (* create constraints to validate the input (using the input [Typ]'s [check]) *) + let checked = + let (Typ input_typ) = input_typ in + input_typ.check var in - run (k var) state + Checked.run checked state in + let state, res = run (k var) state in let res, _ = return_typ.var_to_fields res in let retvar, _ = return_typ.var_to_fields retvar in let _state = From f19d6d384aea9dc5d347734f1807e39656bb1ccb Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:18:51 +0000 Subject: [PATCH 20/52] Constraint_system_builder module --- src/base/runners.ml | 96 +++++++++++++++++++++++---------------------- 1 file changed, 49 insertions(+), 47 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 8b482ec96..b4757cbf0 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -197,53 +197,55 @@ struct let retval = alloc_input return_typ in (var, retval) - let r1cs_h : - type a checked input_var input_value retval. - run:(a, checked) Runner.run - -> input_typ: - ( input_var - , input_value - , field - , (unit, field) Checked.Types.Checked.t ) - Types.Typ.typ - -> return_typ:(a, retval, _, _) Types.Typ.t - -> (input_var -> checked) - -> R1CS_constraint_system.t = - fun ~run ~input_typ ~return_typ k -> - let next_input = ref 0 in - (* allocate variables for the public input and the public output *) - let var, retvar = - allocate_public_inputs next_input ~input_typ ~return_typ - in - let (Typ return_typ) = return_typ in - let num_inputs = !next_input in - let input = field_vec () in - let next_auxiliary = ref num_inputs in - let aux = field_vec () in - let system = R1CS_constraint_system.create () in - let state = - Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system - ~with_witness:false () - in - let state, () = - (* create constraints to validate the input (using the input [Typ]'s [check]) *) - let checked = - let (Typ input_typ) = input_typ in - input_typ.check var + module Constraint_system_builder = struct + let r1cs_h : + type a checked input_var input_value retval. + run:(a, checked) Runner.run + -> input_typ: + ( input_var + , input_value + , field + , (unit, field) Checked.Types.Checked.t ) + Types.Typ.typ + -> return_typ:(a, retval, _, _) Types.Typ.t + -> (input_var -> checked) + -> R1CS_constraint_system.t = + fun ~run ~input_typ ~return_typ k -> + let next_input = ref 0 in + (* allocate variables for the public input and the public output *) + let var, retvar = + allocate_public_inputs next_input ~input_typ ~return_typ in - Checked.run checked state - in - let state, res = run (k var) state in - let res, _ = return_typ.var_to_fields res in - let retvar, _ = return_typ.var_to_fields retvar in - let _state = - Array.fold2_exn ~init:state res retvar ~f:(fun state res retvar -> - fst @@ Checked.run (Checked.assert_equal res retvar) state ) - in - let auxiliary_input_size = !next_auxiliary - num_inputs in - R1CS_constraint_system.set_auxiliary_input_size system - auxiliary_input_size ; - system + let (Typ return_typ) = return_typ in + let num_inputs = !next_input in + let input = field_vec () in + let next_auxiliary = ref num_inputs in + let aux = field_vec () in + let system = R1CS_constraint_system.create () in + let state = + Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system + ~with_witness:false () + in + let state, () = + (* create constraints to validate the input (using the input [Typ]'s [check]) *) + let checked = + let (Typ input_typ) = input_typ in + input_typ.check var + in + Checked.run checked state + in + let state, res = run (k var) state in + let res, _ = return_typ.var_to_fields res in + let retvar, _ = return_typ.var_to_fields retvar in + let _state = + Array.fold2_exn ~init:state res retvar ~f:(fun state res retvar -> + fst @@ Checked.run (Checked.assert_equal res retvar) state ) + in + let auxiliary_input_size = !next_auxiliary - num_inputs in + R1CS_constraint_system.set_auxiliary_input_size system + auxiliary_input_size ; + system + end let constraint_system (type a checked input_var) : run:(a, checked) Runner.run @@ -251,7 +253,7 @@ struct -> return_typ:_ -> (input_var -> checked) -> R1CS_constraint_system.t = - r1cs_h + Constraint_system_builder.r1cs_h let generate_public_input : ('input_var, 'input_value, _, _) Types.Typ.typ From f92e6c9a01df0daf55c41c29b95747c9eb4beee2 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:19:41 +0000 Subject: [PATCH 21/52] Adopt helper function into module --- src/base/runners.ml | 66 ++++++++++++++++++++++----------------------- 1 file changed, 33 insertions(+), 33 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index b4757cbf0..3b57e4b5f 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -164,40 +164,40 @@ struct Field.Vector.emplace_back primary_input x ; v - let allocate_public_inputs : - type input_var input_value output_var output_value. - int ref - -> input_typ: - ( input_var - , input_value - , field - , (unit, field) Checked.Types.Checked.t ) - Types.Typ.typ - -> return_typ: - ( output_var - , output_value - , field - , (unit, field) Checked.Types.Checked.t ) - Types.Typ.t - -> input_var * output_var = - fun next_input ~input_typ:(Typ input_typ) ~return_typ:(Typ return_typ) -> - (* allocate variables for the public input and the public output *) - let alloc_input - { Types0.Typ.var_of_fields - ; size_in_field_elements - ; constraint_system_auxiliary - ; _ - } = - var_of_fields - ( Core_kernel.Array.init size_in_field_elements ~f:(fun _ -> - alloc_var next_input () ) - , constraint_system_auxiliary () ) - in - let var = alloc_input input_typ in - let retval = alloc_input return_typ in - (var, retval) - module Constraint_system_builder = struct + let allocate_public_inputs : + type input_var input_value output_var output_value. + int ref + -> input_typ: + ( input_var + , input_value + , field + , (unit, field) Checked.Types.Checked.t ) + Types.Typ.typ + -> return_typ: + ( output_var + , output_value + , field + , (unit, field) Checked.Types.Checked.t ) + Types.Typ.t + -> input_var * output_var = + fun next_input ~input_typ:(Typ input_typ) ~return_typ:(Typ return_typ) -> + (* allocate variables for the public input and the public output *) + let alloc_input + { Types0.Typ.var_of_fields + ; size_in_field_elements + ; constraint_system_auxiliary + ; _ + } = + var_of_fields + ( Core_kernel.Array.init size_in_field_elements ~f:(fun _ -> + alloc_var next_input () ) + , constraint_system_auxiliary () ) + in + let var = alloc_input input_typ in + let retval = alloc_input return_typ in + (var, retval) + let r1cs_h : type a checked input_var input_value retval. run:(a, checked) Runner.run From 203b44e7dadf5a3153eeaa3c2fcd052a1d9d0960 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:22:52 +0000 Subject: [PATCH 22/52] Begin using builder --- src/base/runners.ml | 33 +++++++++++++++++++++------------ 1 file changed, 21 insertions(+), 12 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 3b57e4b5f..474ae356a 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -198,6 +198,8 @@ struct let retval = alloc_input return_typ in (var, retval) + type t = { run_computation : unit -> R1CS_constraint_system.t } + let r1cs_h : type a checked input_var input_value retval. run:(a, checked) Runner.run @@ -209,7 +211,7 @@ struct Types.Typ.typ -> return_typ:(a, retval, _, _) Types.Typ.t -> (input_var -> checked) - -> R1CS_constraint_system.t = + -> t = fun ~run ~input_typ ~return_typ k -> let next_input = ref 0 in (* allocate variables for the public input and the public output *) @@ -234,17 +236,20 @@ struct in Checked.run checked state in - let state, res = run (k var) state in - let res, _ = return_typ.var_to_fields res in - let retvar, _ = return_typ.var_to_fields retvar in - let _state = - Array.fold2_exn ~init:state res retvar ~f:(fun state res retvar -> - fst @@ Checked.run (Checked.assert_equal res retvar) state ) + let run_computation () = + let state, res = run (k var) state in + let res, _ = return_typ.var_to_fields res in + let retvar, _ = return_typ.var_to_fields retvar in + let _state = + Array.fold2_exn ~init:state res retvar ~f:(fun state res retvar -> + fst @@ Checked.run (Checked.assert_equal res retvar) state ) + in + let auxiliary_input_size = !next_auxiliary - num_inputs in + R1CS_constraint_system.set_auxiliary_input_size system + auxiliary_input_size ; + system in - let auxiliary_input_size = !next_auxiliary - num_inputs in - R1CS_constraint_system.set_auxiliary_input_size system - auxiliary_input_size ; - system + { run_computation } end let constraint_system (type a checked input_var) : @@ -253,7 +258,11 @@ struct -> return_typ:_ -> (input_var -> checked) -> R1CS_constraint_system.t = - Constraint_system_builder.r1cs_h + fun ~run ~input_typ ~return_typ k -> + let builder = + Constraint_system_builder.r1cs_h ~run ~input_typ ~return_typ k + in + builder.run_computation () let generate_public_input : ('input_var, 'input_value, _, _) Types.Typ.typ From 4f1fad2af0cf4712bcf586f3767d06b2ad1ff396 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:23:46 +0000 Subject: [PATCH 23/52] Rename to `build` --- src/base/runners.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 474ae356a..a34f8bc2c 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -200,7 +200,7 @@ struct type t = { run_computation : unit -> R1CS_constraint_system.t } - let r1cs_h : + let build : type a checked input_var input_value retval. run:(a, checked) Runner.run -> input_typ: @@ -260,7 +260,7 @@ struct -> R1CS_constraint_system.t = fun ~run ~input_typ ~return_typ k -> let builder = - Constraint_system_builder.r1cs_h ~run ~input_typ ~return_typ k + Constraint_system_builder.build ~run ~input_typ ~return_typ k in builder.run_computation () From 0554ac0a0e45df62174f19107c5900d2e92335b3 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:24:30 +0000 Subject: [PATCH 24/52] Signature on Constraint_system_builder --- src/base/runners.ml | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index a34f8bc2c..299f2cd5d 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -164,7 +164,26 @@ struct Field.Vector.emplace_back primary_input x ; v - module Constraint_system_builder = struct + module Constraint_system_builder : sig + type t = { run_computation : unit -> R1CS_constraint_system.t } + + val build : + run:('a, 'checked) Runner.run + -> input_typ: + ( 'input_var + , 'input_value + , field + , (unit, field) Checked.Types.Checked.t ) + Types0.Typ.typ + -> return_typ: + ( 'a + , 'retval + , field + , (unit, field) Checked.Types.Checked.t ) + Types0.Typ.typ + -> ('input_var -> 'checked) + -> t + end = struct let allocate_public_inputs : type input_var input_value output_var output_value. int ref From 561f79beb0d3418180abf0875082b3c9fac2d0d6 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:28:46 +0000 Subject: [PATCH 25/52] Push down responsibility for circuit --- src/base/runners.ml | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 299f2cd5d..6475204d0 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -165,7 +165,9 @@ struct v module Constraint_system_builder : sig - type t = { run_computation : unit -> R1CS_constraint_system.t } + type ('input_var, 'checked) t = + { run_computation : ('input_var -> 'checked) -> R1CS_constraint_system.t + } val build : run:('a, 'checked) Runner.run @@ -181,8 +183,7 @@ struct , field , (unit, field) Checked.Types.Checked.t ) Types0.Typ.typ - -> ('input_var -> 'checked) - -> t + -> ('input_var, 'checked) t end = struct let allocate_public_inputs : type input_var input_value output_var output_value. @@ -217,7 +218,9 @@ struct let retval = alloc_input return_typ in (var, retval) - type t = { run_computation : unit -> R1CS_constraint_system.t } + type ('input_var, 'checked) t = + { run_computation : ('input_var -> 'checked) -> R1CS_constraint_system.t + } let build : type a checked input_var input_value retval. @@ -229,9 +232,8 @@ struct , (unit, field) Checked.Types.Checked.t ) Types.Typ.typ -> return_typ:(a, retval, _, _) Types.Typ.t - -> (input_var -> checked) - -> t = - fun ~run ~input_typ ~return_typ k -> + -> (input_var, checked) t = + fun ~run ~input_typ ~return_typ -> let next_input = ref 0 in (* allocate variables for the public input and the public output *) let var, retvar = @@ -255,7 +257,7 @@ struct in Checked.run checked state in - let run_computation () = + let run_computation k = let state, res = run (k var) state in let res, _ = return_typ.var_to_fields res in let retvar, _ = return_typ.var_to_fields retvar in @@ -279,9 +281,9 @@ struct -> R1CS_constraint_system.t = fun ~run ~input_typ ~return_typ k -> let builder = - Constraint_system_builder.build ~run ~input_typ ~return_typ k + Constraint_system_builder.build ~run ~input_typ ~return_typ in - builder.run_computation () + builder.run_computation k let generate_public_input : ('input_var, 'input_value, _, _) Types.Typ.typ From c4af85a957cd58a52109c73d195a6b696ce9d4fa Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:35:28 +0000 Subject: [PATCH 26/52] Split computation into stages --- src/base/runners.ml | 36 +++++++++++++++++++++++------------- 1 file changed, 23 insertions(+), 13 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 6475204d0..0d2a4b2f4 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -165,12 +165,15 @@ struct v module Constraint_system_builder : sig - type ('input_var, 'checked) t = - { run_computation : ('input_var -> 'checked) -> R1CS_constraint_system.t + type ('input_var, 'return_var, 'field, 'checked) t = + { run_computation : + ('input_var -> 'checked) -> 'field Run_state.t * 'return_var + ; finish_computation : + 'field Run_state.t * 'return_var -> R1CS_constraint_system.t } val build : - run:('a, 'checked) Runner.run + run:('retvar, 'checked) Runner.run -> input_typ: ( 'input_var , 'input_value @@ -178,12 +181,12 @@ struct , (unit, field) Checked.Types.Checked.t ) Types0.Typ.typ -> return_typ: - ( 'a + ( 'retvar , 'retval , field , (unit, field) Checked.Types.Checked.t ) Types0.Typ.typ - -> ('input_var, 'checked) t + -> ('input_var, 'retvar, field, 'checked) t end = struct let allocate_public_inputs : type input_var input_value output_var output_value. @@ -218,21 +221,24 @@ struct let retval = alloc_input return_typ in (var, retval) - type ('input_var, 'checked) t = - { run_computation : ('input_var -> 'checked) -> R1CS_constraint_system.t + type ('input_var, 'return_var, 'field, 'checked) t = + { run_computation : + ('input_var -> 'checked) -> 'field Run_state.t * 'return_var + ; finish_computation : + 'field Run_state.t * 'return_var -> R1CS_constraint_system.t } let build : - type a checked input_var input_value retval. - run:(a, checked) Runner.run + type checked input_var input_value retvar retval. + run:(retvar, checked) Runner.run -> input_typ: ( input_var , input_value , field , (unit, field) Checked.Types.Checked.t ) Types.Typ.typ - -> return_typ:(a, retval, _, _) Types.Typ.t - -> (input_var, checked) t = + -> return_typ:(retvar, retval, _, _) Types.Typ.t + -> (input_var, retvar, field, checked) t = fun ~run ~input_typ ~return_typ -> let next_input = ref 0 in (* allocate variables for the public input and the public output *) @@ -259,6 +265,9 @@ struct in let run_computation k = let state, res = run (k var) state in + (state, res) + in + let finish_computation (state, res) = let res, _ = return_typ.var_to_fields res in let retvar, _ = return_typ.var_to_fields retvar in let _state = @@ -270,7 +279,7 @@ struct auxiliary_input_size ; system in - { run_computation } + { run_computation; finish_computation } end let constraint_system (type a checked input_var) : @@ -283,7 +292,8 @@ struct let builder = Constraint_system_builder.build ~run ~input_typ ~return_typ in - builder.run_computation k + let state, res = builder.run_computation k in + builder.finish_computation (state, res) let generate_public_input : ('input_var, 'input_value, _, _) Types.Typ.typ From a5bfe4e60b937af845cde737fe4c84ac8fc8d84a Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 04:42:29 +0000 Subject: [PATCH 27/52] Generalize run_computation --- src/base/runners.ml | 25 +++++++++---------------- 1 file changed, 9 insertions(+), 16 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 0d2a4b2f4..57f77b020 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -166,15 +166,13 @@ struct module Constraint_system_builder : sig type ('input_var, 'return_var, 'field, 'checked) t = - { run_computation : - ('input_var -> 'checked) -> 'field Run_state.t * 'return_var + { run_computation : 'a. ('input_var -> 'field Run_state.t -> 'a) -> 'a ; finish_computation : 'field Run_state.t * 'return_var -> R1CS_constraint_system.t } val build : - run:('retvar, 'checked) Runner.run - -> input_typ: + input_typ: ( 'input_var , 'input_value , field @@ -222,16 +220,14 @@ struct (var, retval) type ('input_var, 'return_var, 'field, 'checked) t = - { run_computation : - ('input_var -> 'checked) -> 'field Run_state.t * 'return_var + { run_computation : 'a. ('input_var -> 'field Run_state.t -> 'a) -> 'a ; finish_computation : 'field Run_state.t * 'return_var -> R1CS_constraint_system.t } let build : type checked input_var input_value retvar retval. - run:(retvar, checked) Runner.run - -> input_typ: + input_typ: ( input_var , input_value , field @@ -239,7 +235,7 @@ struct Types.Typ.typ -> return_typ:(retvar, retval, _, _) Types.Typ.t -> (input_var, retvar, field, checked) t = - fun ~run ~input_typ ~return_typ -> + fun ~input_typ ~return_typ -> let next_input = ref 0 in (* allocate variables for the public input and the public output *) let var, retvar = @@ -263,10 +259,7 @@ struct in Checked.run checked state in - let run_computation k = - let state, res = run (k var) state in - (state, res) - in + let run_computation k = k var state in let finish_computation (state, res) = let res, _ = return_typ.var_to_fields res in let retvar, _ = return_typ.var_to_fields retvar in @@ -289,10 +282,10 @@ struct -> (input_var -> checked) -> R1CS_constraint_system.t = fun ~run ~input_typ ~return_typ k -> - let builder = - Constraint_system_builder.build ~run ~input_typ ~return_typ + let builder = Constraint_system_builder.build ~input_typ ~return_typ in + let state, res = + builder.run_computation (fun var state -> run (k var) state) in - let state, res = builder.run_computation k in builder.finish_computation (state, res) let generate_public_input : From af48c23868944c03457f217976c1f9f34e32bcf0 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 05:16:15 +0000 Subject: [PATCH 28/52] Create `WitnessBuilder` module, move `auxiliary_input` --- src/base/runners.ml | 73 +++++++++++++++++++++++---------------------- 1 file changed, 38 insertions(+), 35 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 57f77b020..5e016d83a 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -44,37 +44,6 @@ struct module Runner = Runner - let auxiliary_input ?system ~run ~num_inputs - ?(handlers = ([] : Handler.t list)) t0 (input : Field.Vector.t) - ~return_typ:(Types.Typ.Typ return_typ) ~output : Field.Vector.t * _ = - let next_auxiliary = ref num_inputs in - let aux = Field.Vector.create () in - let handler = - List.fold ~init:Request.Handler.fail handlers ~f:(fun handler h -> - Request.Handler.(push handler (create_single h)) ) - in - let state = - Runner.State.make ?system ~num_inputs ~input:(pack_field_vec input) - ~next_auxiliary ~aux:(pack_field_vec aux) ~handler ~with_witness:true () - in - let state, res = run t0 state in - let res, auxiliary_output_data = return_typ.var_to_fields res in - let output, _ = return_typ.var_to_fields output in - let _state = - Array.fold2_exn ~init:state res output ~f:(fun state res output -> - Field.Vector.emplace_back input (Runner.get_value state res) ; - fst @@ Checked.run (Checked.assert_equal res output) state ) - in - let true_output = - return_typ.var_of_fields (output, auxiliary_output_data) - in - Option.iter system ~f:(fun system -> - let auxiliary_input_size = !next_auxiliary - num_inputs in - R1CS_constraint_system.set_auxiliary_input_size system - auxiliary_input_size ; - R1CS_constraint_system.finalize system ) ; - (aux, true_output) - let run_and_check_exn' ~run t0 = let num_inputs = 0 in let input = field_vec () in @@ -300,6 +269,40 @@ struct let _fields = Array.map ~f:store_field_elt fields in primary_input + module Witness_builder = struct + let auxiliary_input ?system ~run ~num_inputs + ?(handlers = ([] : Handler.t list)) t0 (input : Field.Vector.t) + ~return_typ:(Types.Typ.Typ return_typ) ~output : Field.Vector.t * _ = + let next_auxiliary = ref num_inputs in + let aux = Field.Vector.create () in + let handler = + List.fold ~init:Request.Handler.fail handlers ~f:(fun handler h -> + Request.Handler.(push handler (create_single h)) ) + in + let state = + Runner.State.make ?system ~num_inputs ~input:(pack_field_vec input) + ~next_auxiliary ~aux:(pack_field_vec aux) ~handler + ~with_witness:true () + in + let state, res = run t0 state in + let res, auxiliary_output_data = return_typ.var_to_fields res in + let output, _ = return_typ.var_to_fields output in + let _state = + Array.fold2_exn ~init:state res output ~f:(fun state res output -> + Field.Vector.emplace_back input (Runner.get_value state res) ; + fst @@ Checked.run (Checked.assert_equal res output) state ) + in + let true_output = + return_typ.var_of_fields (output, auxiliary_output_data) + in + Option.iter system ~f:(fun system -> + let auxiliary_input_size = !next_auxiliary - num_inputs in + R1CS_constraint_system.set_auxiliary_input_size system + auxiliary_input_size ; + R1CS_constraint_system.finalize system ) ; + (aux, true_output) + end + let conv : type r_var r_value. (int -> _ -> r_var -> Field.Vector.t -> r_value) @@ -341,8 +344,8 @@ struct conv (fun num_inputs output c primary -> let auxiliary = - auxiliary_input ~run ?handlers ~return_typ ~output ~num_inputs c - primary + Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output + ~num_inputs c primary in ignore auxiliary ) input_typ return_typ @@ -360,8 +363,8 @@ struct conv (fun num_inputs output c primary -> let auxiliary, output = - auxiliary_input ~run ?handlers ~return_typ ~output ~num_inputs c - primary + Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output + ~num_inputs c primary in let output = let (Typ return_typ) = return_typ in From c260e358a4c40fd5eb5e81a6dd0b14578e4c6623 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 05:23:49 +0000 Subject: [PATCH 29/52] Remove unused optional argument --- src/base/runners.ml | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 5e016d83a..d345ec6cf 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -270,9 +270,9 @@ struct primary_input module Witness_builder = struct - let auxiliary_input ?system ~run ~num_inputs - ?(handlers = ([] : Handler.t list)) t0 (input : Field.Vector.t) - ~return_typ:(Types.Typ.Typ return_typ) ~output : Field.Vector.t * _ = + let auxiliary_input ~run ~num_inputs ?(handlers = ([] : Handler.t list)) + t0 (input : Field.Vector.t) ~return_typ:(Types.Typ.Typ return_typ) + ~output : Field.Vector.t * _ = let next_auxiliary = ref num_inputs in let aux = Field.Vector.create () in let handler = @@ -280,7 +280,7 @@ struct Request.Handler.(push handler (create_single h)) ) in let state = - Runner.State.make ?system ~num_inputs ~input:(pack_field_vec input) + Runner.State.make ~num_inputs ~input:(pack_field_vec input) ~next_auxiliary ~aux:(pack_field_vec aux) ~handler ~with_witness:true () in @@ -295,11 +295,6 @@ struct let true_output = return_typ.var_of_fields (output, auxiliary_output_data) in - Option.iter system ~f:(fun system -> - let auxiliary_input_size = !next_auxiliary - num_inputs in - R1CS_constraint_system.set_auxiliary_input_size system - auxiliary_input_size ; - R1CS_constraint_system.finalize system ) ; (aux, true_output) end From 2f4629e1f7471e3f483f79ba33257532e4d6508f Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 05:33:49 +0000 Subject: [PATCH 30/52] Abstract out final step of witness generation --- src/base/runners.ml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index d345ec6cf..5e3d7a807 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -285,16 +285,17 @@ struct ~with_witness:true () in let state, res = run t0 state in - let res, auxiliary_output_data = return_typ.var_to_fields res in - let output, _ = return_typ.var_to_fields output in - let _state = - Array.fold2_exn ~init:state res output ~f:(fun state res output -> - Field.Vector.emplace_back input (Runner.get_value state res) ; - fst @@ Checked.run (Checked.assert_equal res output) state ) - in - let true_output = + let finish_witness_generation (state, res) = + let res, auxiliary_output_data = return_typ.var_to_fields res in + let output, _ = return_typ.var_to_fields output in + let _state = + Array.fold2_exn ~init:state res output ~f:(fun state res output -> + Field.Vector.emplace_back input (Runner.get_value state res) ; + fst @@ Checked.run (Checked.assert_equal res output) state ) + in return_typ.var_of_fields (output, auxiliary_output_data) in + let true_output = finish_witness_generation (state, res) in (aux, true_output) end From bcdf907364bdfac6ce3d4af29f0bf9b449e8ccd6 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 05:38:25 +0000 Subject: [PATCH 31/52] Restructure function --- src/base/runners.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 5e3d7a807..ce93b171d 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -293,10 +293,10 @@ struct Field.Vector.emplace_back input (Runner.get_value state res) ; fst @@ Checked.run (Checked.assert_equal res output) state ) in - return_typ.var_of_fields (output, auxiliary_output_data) + let true_output = return_typ.var_of_fields (output, auxiliary_output_data) in + (aux, true_output) in - let true_output = finish_witness_generation (state, res) in - (aux, true_output) + finish_witness_generation (state, res) end let conv : From 5520ace64048c9016be1d10397eec28030a9a107 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 05:43:29 +0000 Subject: [PATCH 32/52] Split to use a helper function --- src/base/runners.ml | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index ce93b171d..5fca39713 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -270,9 +270,14 @@ struct primary_input module Witness_builder = struct + type ('input_var, 'return_var, 'return_value, 'field, 'checked) t = + { finish_witness_generation : + 'field Run_state.t * 'return_var -> Field.Vector.t * 'return_value + } + let auxiliary_input ~run ~num_inputs ?(handlers = ([] : Handler.t list)) t0 (input : Field.Vector.t) ~return_typ:(Types.Typ.Typ return_typ) - ~output : Field.Vector.t * _ = + ~output = let next_auxiliary = ref num_inputs in let aux = Field.Vector.create () in let handler = @@ -293,10 +298,12 @@ struct Field.Vector.emplace_back input (Runner.get_value state res) ; fst @@ Checked.run (Checked.assert_equal res output) state ) in - let true_output = return_typ.var_of_fields (output, auxiliary_output_data) in + let true_output = + return_typ.var_of_fields (output, auxiliary_output_data) + in (aux, true_output) in - finish_witness_generation (state, res) + ((state, res), { finish_witness_generation }) end let conv : @@ -339,11 +346,14 @@ struct fun ~run ~input_typ ~return_typ ?handlers k -> conv (fun num_inputs output c primary -> - let auxiliary = + (* NB: No need to finish witness generation, we'll discard the + witness and public output anyway. + *) + let (state, res), { Witness_builder.finish_witness_generation = _ } = Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output ~num_inputs c primary in - ignore auxiliary ) + ignore (state, res) ) input_typ return_typ (fun () -> k) @@ -358,10 +368,13 @@ struct fun ~run ~f ~input_typ ~return_typ ?handlers k -> conv (fun num_inputs output c primary -> - let auxiliary, output = + let (state, res), builder = Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output ~num_inputs c primary in + let auxiliary, output = + builder.finish_witness_generation (state, res) + in let output = let (Typ return_typ) = return_typ in let fields, aux = return_typ.var_to_fields output in From fa7219ccd79c04545edf0c2360749d3616249571 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 05:55:31 +0000 Subject: [PATCH 33/52] Hoist value reading and conversion, avoid a double-pass --- src/base/runners.ml | 38 ++++++++++++++++++-------------------- 1 file changed, 18 insertions(+), 20 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 5fca39713..e1bd8aac4 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -291,15 +291,26 @@ struct in let state, res = run t0 state in let finish_witness_generation (state, res) = - let res, auxiliary_output_data = return_typ.var_to_fields res in - let output, _ = return_typ.var_to_fields output in - let _state = - Array.fold2_exn ~init:state res output ~f:(fun state res output -> - Field.Vector.emplace_back input (Runner.get_value state res) ; - fst @@ Checked.run (Checked.assert_equal res output) state ) + let res_fields, auxiliary_output_data = + return_typ.var_to_fields res + in + let output_fields, _ = return_typ.var_to_fields output in + let state = + Array.fold2_exn ~init:state res_fields output_fields + ~f:(fun state res_field output_field -> + Field.Vector.emplace_back input + (Runner.get_value state res_field) ; + fst + @@ Checked.run + (Checked.assert_equal res_field output_field) + state ) in let true_output = - return_typ.var_of_fields (output, auxiliary_output_data) + (* NB: We use [output_fields] to avoid resolving [Cvar.t]s beyond a + vector access. + *) + let fields = Array.map ~f:(Runner.get_value state) output_fields in + return_typ.value_of_fields (fields, auxiliary_output_data) in (aux, true_output) in @@ -375,19 +386,6 @@ struct let auxiliary, output = builder.finish_witness_generation (state, res) in - let output = - let (Typ return_typ) = return_typ in - let fields, aux = return_typ.var_to_fields output in - let read_cvar = - let get_one i = - if i < num_inputs then Field.Vector.get primary i - else Field.Vector.get auxiliary (i - num_inputs) - in - Cvar.eval (`Return_values_will_be_mutated get_one) - in - let fields = Array.map ~f:read_cvar fields in - return_typ.value_of_fields (fields, aux) - in f { Proof_inputs.public_inputs = primary ; auxiliary_inputs = auxiliary From 150e6c31ff00e70cf226a993f42f531fe3ad88c6 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:00:13 +0000 Subject: [PATCH 34/52] Split conv to add a receive_public_input helper --- src/base/runners.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index e1bd8aac4..1513058eb 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -334,8 +334,8 @@ struct Field.Vector.emplace_back primary_input x ; Cvar.Unsafe.of_index v in - let (Typ { var_of_fields; value_to_fields; _ }) = input_typ in - fun value -> + let receive_public_input value = + let (Typ { var_of_fields; value_to_fields; _ }) = input_typ in let fields, aux = value_to_fields value in let fields = Array.map ~f:store_field_elt fields in let var = var_of_fields (fields, aux) in @@ -345,6 +345,10 @@ struct ~f:(fun _ -> alloc_var next_input ()) , return_typ.constraint_system_auxiliary () ) in + (var, retval) + in + fun value -> + let var, retval = receive_public_input value in cont0 !next_input retval (k0 () var) primary_input let generate_auxiliary_input : From 4da292f3c15e73cdcd1c849ae84a0a97bbffe3e6 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:03:02 +0000 Subject: [PATCH 35/52] Lift `conv` into a module --- src/base/runners.ml | 70 ++++++++++++++++++++++++--------------------- 1 file changed, 37 insertions(+), 33 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 1513058eb..0d1996e73 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -269,6 +269,42 @@ struct let _fields = Array.map ~f:store_field_elt fields in primary_input + module Conv = struct + let conv : + type r_var r_value. + (int -> _ -> r_var -> Field.Vector.t -> r_value) + -> ('input_var, 'input_value, _, _) Types.Typ.t + -> _ Types.Typ.t + -> (unit -> 'input_var -> r_var) + -> 'input_value + -> r_value = + fun cont0 input_typ (Typ return_typ) k0 -> + let primary_input = Field.Vector.create () in + let next_input = ref 0 in + let store_field_elt x = + let v = !next_input in + incr next_input ; + Field.Vector.emplace_back primary_input x ; + Cvar.Unsafe.of_index v + in + let receive_public_input value = + let (Typ { var_of_fields; value_to_fields; _ }) = input_typ in + let fields, aux = value_to_fields value in + let fields = Array.map ~f:store_field_elt fields in + let var = var_of_fields (fields, aux) in + let retval = + return_typ.var_of_fields + ( Core_kernel.Array.init return_typ.size_in_field_elements + ~f:(fun _ -> alloc_var next_input ()) + , return_typ.constraint_system_auxiliary () ) + in + (var, retval) + in + fun value -> + let var, retval = receive_public_input value in + cont0 !next_input retval (k0 () var) primary_input + end + module Witness_builder = struct type ('input_var, 'return_var, 'return_value, 'field, 'checked) t = { finish_witness_generation : @@ -317,39 +353,7 @@ struct ((state, res), { finish_witness_generation }) end - let conv : - type r_var r_value. - (int -> _ -> r_var -> Field.Vector.t -> r_value) - -> ('input_var, 'input_value, _, _) Types.Typ.t - -> _ Types.Typ.t - -> (unit -> 'input_var -> r_var) - -> 'input_value - -> r_value = - fun cont0 input_typ (Typ return_typ) k0 -> - let primary_input = Field.Vector.create () in - let next_input = ref 0 in - let store_field_elt x = - let v = !next_input in - incr next_input ; - Field.Vector.emplace_back primary_input x ; - Cvar.Unsafe.of_index v - in - let receive_public_input value = - let (Typ { var_of_fields; value_to_fields; _ }) = input_typ in - let fields, aux = value_to_fields value in - let fields = Array.map ~f:store_field_elt fields in - let var = var_of_fields (fields, aux) in - let retval = - return_typ.var_of_fields - ( Core_kernel.Array.init return_typ.size_in_field_elements - ~f:(fun _ -> alloc_var next_input ()) - , return_typ.constraint_system_auxiliary () ) - in - (var, retval) - in - fun value -> - let var, retval = receive_public_input value in - cont0 !next_input retval (k0 () var) primary_input + let conv = Conv.conv let generate_auxiliary_input : run:('a, 'checked) Runner.run From b17a3cf4ca3bfc0c4c461eda79df8fc429704dac Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:07:03 +0000 Subject: [PATCH 36/52] Expand scope of receive_public_input --- src/base/runners.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 0d1996e73..09be95b56 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -298,11 +298,14 @@ struct ~f:(fun _ -> alloc_var next_input ()) , return_typ.constraint_system_auxiliary () ) in - (var, retval) + let first_auxiliary = !next_input in + (var, retval, first_auxiliary, primary_input) in fun value -> - let var, retval = receive_public_input value in - cont0 !next_input retval (k0 () var) primary_input + let var, retval, first_auxiliary, primary_input = + receive_public_input value + in + cont0 first_auxiliary retval (k0 () var) primary_input end module Witness_builder = struct From 8f55770f36e7f4f4b45f1aa70f87fb67ee678ba0 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:08:32 +0000 Subject: [PATCH 37/52] Expand conv alias --- src/base/runners.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 09be95b56..c0065969f 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -356,7 +356,16 @@ struct ((state, res), { finish_witness_generation }) end - let conv = Conv.conv + let conv : + type r_var r_value. + (int -> _ -> r_var -> Field.Vector.t -> r_value) + -> ('input_var, 'input_value, _, _) Types.Typ.t + -> _ Types.Typ.t + -> (unit -> 'input_var -> r_var) + -> 'input_value + -> r_value = + fun cont0 input_typ return_typ k0 -> + Conv.conv cont0 input_typ return_typ k0 let generate_auxiliary_input : run:('a, 'checked) Runner.run From e148e8b64960e586cadac98c054d314eb2fd9229 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:11:30 +0000 Subject: [PATCH 38/52] Push some logic back into conv --- src/base/runners.ml | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index c0065969f..8809c0058 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -271,14 +271,11 @@ struct module Conv = struct let conv : - type r_var r_value. - (int -> _ -> r_var -> Field.Vector.t -> r_value) - -> ('input_var, 'input_value, _, _) Types.Typ.t + ('input_var, 'input_value, _, _) Types.Typ.t -> _ Types.Typ.t - -> (unit -> 'input_var -> r_var) -> 'input_value - -> r_value = - fun cont0 input_typ (Typ return_typ) k0 -> + -> _ = + fun input_typ (Typ return_typ) -> let primary_input = Field.Vector.create () in let next_input = ref 0 in let store_field_elt x = @@ -301,11 +298,7 @@ struct let first_auxiliary = !next_input in (var, retval, first_auxiliary, primary_input) in - fun value -> - let var, retval, first_auxiliary, primary_input = - receive_public_input value - in - cont0 first_auxiliary retval (k0 () var) primary_input + receive_public_input end module Witness_builder = struct @@ -365,7 +358,12 @@ struct -> 'input_value -> r_value = fun cont0 input_typ return_typ k0 -> - Conv.conv cont0 input_typ return_typ k0 + let receive_public_input = Conv.conv input_typ return_typ in + fun value -> + let var, retval, first_auxiliary, primary_input = + receive_public_input value + in + cont0 first_auxiliary retval (k0 () var) primary_input let generate_auxiliary_input : run:('a, 'checked) Runner.run From a1a6c77de05abb8b7cf842d58ef134fc35956cf1 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:12:42 +0000 Subject: [PATCH 39/52] Flatten structure of Conv.conv, rename to receive_public_input --- src/base/runners.ml | 41 ++++++++++++++++++----------------------- 1 file changed, 18 insertions(+), 23 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 8809c0058..810711536 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -270,12 +270,12 @@ struct primary_input module Conv = struct - let conv : + let receive_public_input : ('input_var, 'input_value, _, _) Types.Typ.t -> _ Types.Typ.t -> 'input_value -> _ = - fun input_typ (Typ return_typ) -> + fun input_typ (Typ return_typ) value -> let primary_input = Field.Vector.create () in let next_input = ref 0 in let store_field_elt x = @@ -284,21 +284,18 @@ struct Field.Vector.emplace_back primary_input x ; Cvar.Unsafe.of_index v in - let receive_public_input value = - let (Typ { var_of_fields; value_to_fields; _ }) = input_typ in - let fields, aux = value_to_fields value in - let fields = Array.map ~f:store_field_elt fields in - let var = var_of_fields (fields, aux) in - let retval = - return_typ.var_of_fields - ( Core_kernel.Array.init return_typ.size_in_field_elements - ~f:(fun _ -> alloc_var next_input ()) - , return_typ.constraint_system_auxiliary () ) - in - let first_auxiliary = !next_input in - (var, retval, first_auxiliary, primary_input) + let (Typ { var_of_fields; value_to_fields; _ }) = input_typ in + let fields, aux = value_to_fields value in + let fields = Array.map ~f:store_field_elt fields in + let var = var_of_fields (fields, aux) in + let retval = + return_typ.var_of_fields + ( Core_kernel.Array.init return_typ.size_in_field_elements + ~f:(fun _ -> alloc_var next_input ()) + , return_typ.constraint_system_auxiliary () ) in - receive_public_input + let first_auxiliary = !next_input in + (var, retval, first_auxiliary, primary_input) end module Witness_builder = struct @@ -357,13 +354,11 @@ struct -> (unit -> 'input_var -> r_var) -> 'input_value -> r_value = - fun cont0 input_typ return_typ k0 -> - let receive_public_input = Conv.conv input_typ return_typ in - fun value -> - let var, retval, first_auxiliary, primary_input = - receive_public_input value - in - cont0 first_auxiliary retval (k0 () var) primary_input + fun cont0 input_typ return_typ k0 value -> + let var, retval, first_auxiliary, primary_input = + Conv.receive_public_input input_typ return_typ value + in + cont0 first_auxiliary retval (k0 () var) primary_input let generate_auxiliary_input : run:('a, 'checked) Runner.run From cd303ad6b096dcee3fcbc18170f349458a0062da Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:16:04 +0000 Subject: [PATCH 40/52] Add a record for carrying conv data --- src/base/runners.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 810711536..78f03d2c5 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -270,6 +270,13 @@ struct primary_input module Conv = struct + type ('input_var, 'output_var) t = + { input_var : 'input_var + ; output_var : 'output_var + ; first_auxiliary : int + ; primary_input : Field.Vector.t + } + let receive_public_input : ('input_var, 'input_value, _, _) Types.Typ.t -> _ Types.Typ.t @@ -295,7 +302,7 @@ struct , return_typ.constraint_system_auxiliary () ) in let first_auxiliary = !next_input in - (var, retval, first_auxiliary, primary_input) + { input_var = var; output_var = retval; first_auxiliary; primary_input } end module Witness_builder = struct @@ -355,7 +362,11 @@ struct -> 'input_value -> r_value = fun cont0 input_typ return_typ k0 value -> - let var, retval, first_auxiliary, primary_input = + let { Conv.input_var = var + ; output_var = retval + ; first_auxiliary + ; primary_input + } = Conv.receive_public_input input_typ return_typ value in cont0 first_auxiliary retval (k0 () var) primary_input From b674ea30fbb1fa1494ccf2b61fc145f89618ef35 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:16:47 +0000 Subject: [PATCH 41/52] Renaming --- src/base/runners.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 78f03d2c5..29554c32c 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -294,15 +294,15 @@ struct let (Typ { var_of_fields; value_to_fields; _ }) = input_typ in let fields, aux = value_to_fields value in let fields = Array.map ~f:store_field_elt fields in - let var = var_of_fields (fields, aux) in - let retval = + let input_var = var_of_fields (fields, aux) in + let output_var = return_typ.var_of_fields ( Core_kernel.Array.init return_typ.size_in_field_elements ~f:(fun _ -> alloc_var next_input ()) , return_typ.constraint_system_auxiliary () ) in let first_auxiliary = !next_input in - { input_var = var; output_var = retval; first_auxiliary; primary_input } + { input_var; output_var; first_auxiliary; primary_input } end module Witness_builder = struct From 029815c27730a126a0be7fa70fc715ae70e50284 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:17:16 +0000 Subject: [PATCH 42/52] More renaming --- src/base/runners.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 29554c32c..325bebe12 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -362,14 +362,10 @@ struct -> 'input_value -> r_value = fun cont0 input_typ return_typ k0 value -> - let { Conv.input_var = var - ; output_var = retval - ; first_auxiliary - ; primary_input - } = + let { Conv.input_var; output_var; first_auxiliary; primary_input } = Conv.receive_public_input input_typ return_typ value in - cont0 first_auxiliary retval (k0 () var) primary_input + cont0 first_auxiliary output_var (k0 () input_var) primary_input let generate_auxiliary_input : run:('a, 'checked) Runner.run From bb752c98695f39b7835330595e11230e5241a2f3 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:22:39 +0000 Subject: [PATCH 43/52] Expand conv in generate_auxiliary_input --- src/base/runners.ml | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 325bebe12..eab29517c 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -374,19 +374,23 @@ struct -> ?handlers:Handler.t list -> 'k_var -> 'k_value = - fun ~run ~input_typ ~return_typ ?handlers k -> - conv - (fun num_inputs output c primary -> - (* NB: No need to finish witness generation, we'll discard the - witness and public output anyway. - *) - let (state, res), { Witness_builder.finish_witness_generation = _ } = - Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output - ~num_inputs c primary - in - ignore (state, res) ) - input_typ return_typ - (fun () -> k) + fun ~run ~input_typ ~return_typ ?handlers k value -> + let { Conv.input_var + ; output_var = output + ; first_auxiliary = num_inputs + ; primary_input = primary + } = + Conv.receive_public_input input_typ return_typ value + in + let c = (fun () -> k) () input_var in + (* NB: No need to finish witness generation, we'll discard the + witness and public output anyway. + *) + let (state, res), { Witness_builder.finish_witness_generation = _ } = + Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output + ~num_inputs c primary + in + ignore (state, res) let generate_witness_conv : run:('a, 'checked) Runner.run From a8f396ec12fc98bce2977f6641b8d3b619636815 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:24:05 +0000 Subject: [PATCH 44/52] Expand conv in generate_witness_conv --- src/base/runners.ml | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index eab29517c..cd2830c5b 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -400,23 +400,23 @@ struct -> ?handlers:Handler.t list -> 'k_var -> 'k_value = - fun ~run ~f ~input_typ ~return_typ ?handlers k -> - conv - (fun num_inputs output c primary -> - let (state, res), builder = - Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output - ~num_inputs c primary - in - let auxiliary, output = - builder.finish_witness_generation (state, res) - in - f - { Proof_inputs.public_inputs = primary - ; auxiliary_inputs = auxiliary - } - output ) - input_typ return_typ - (fun () -> k) + fun ~run ~f ~input_typ ~return_typ ?handlers k value -> + let { Conv.input_var + ; output_var = output + ; first_auxiliary = num_inputs + ; primary_input = primary + } = + Conv.receive_public_input input_typ return_typ value + in + let c = (fun () -> k) () input_var in + let (state, res), builder = + Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output + ~num_inputs c primary + in + let auxiliary, output = builder.finish_witness_generation (state, res) in + f + { Proof_inputs.public_inputs = primary; auxiliary_inputs = auxiliary } + output let generate_witness = generate_witness_conv ~f:(fun inputs _output -> inputs) From b3e667a1b83323ceb8c70a822bc3f148a3a705de Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:27:13 +0000 Subject: [PATCH 45/52] Push computation of `c` up into auxiliary_input --- src/base/runners.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index cd2830c5b..6b9317fa9 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -313,7 +313,8 @@ struct let auxiliary_input ~run ~num_inputs ?(handlers = ([] : Handler.t list)) t0 (input : Field.Vector.t) ~return_typ:(Types.Typ.Typ return_typ) - ~output = + ~output input_var = + let t0 = (fun () -> t0) () input_var in let next_auxiliary = ref num_inputs in let aux = Field.Vector.create () in let handler = @@ -382,13 +383,12 @@ struct } = Conv.receive_public_input input_typ return_typ value in - let c = (fun () -> k) () input_var in (* NB: No need to finish witness generation, we'll discard the witness and public output anyway. *) let (state, res), { Witness_builder.finish_witness_generation = _ } = Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output - ~num_inputs c primary + ~num_inputs k primary input_var in ignore (state, res) @@ -408,10 +408,9 @@ struct } = Conv.receive_public_input input_typ return_typ value in - let c = (fun () -> k) () input_var in let (state, res), builder = Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output - ~num_inputs c primary + ~num_inputs k primary input_var in let auxiliary, output = builder.finish_witness_generation (state, res) in f From 1859549983530624a1e1ffe4e6bebc9df3237b50 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:28:50 +0000 Subject: [PATCH 46/52] Simplify by reducing --- src/base/runners.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 6b9317fa9..f750d03cb 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -314,7 +314,7 @@ struct let auxiliary_input ~run ~num_inputs ?(handlers = ([] : Handler.t list)) t0 (input : Field.Vector.t) ~return_typ:(Types.Typ.Typ return_typ) ~output input_var = - let t0 = (fun () -> t0) () input_var in + let t0 = t0 input_var in let next_auxiliary = ref num_inputs in let aux = Field.Vector.create () in let handler = From 7c2d8a78cbb3e7327e46331dc30462f9dc9b10b3 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:29:52 +0000 Subject: [PATCH 47/52] Simplify by inlining --- src/base/runners.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index f750d03cb..8674e8b84 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -314,7 +314,6 @@ struct let auxiliary_input ~run ~num_inputs ?(handlers = ([] : Handler.t list)) t0 (input : Field.Vector.t) ~return_typ:(Types.Typ.Typ return_typ) ~output input_var = - let t0 = t0 input_var in let next_auxiliary = ref num_inputs in let aux = Field.Vector.create () in let handler = @@ -326,7 +325,7 @@ struct ~next_auxiliary ~aux:(pack_field_vec aux) ~handler ~with_witness:true () in - let state, res = run t0 state in + let state, res = run (t0 input_var) state in let finish_witness_generation (state, res) = let res_fields, auxiliary_output_data = return_typ.var_to_fields res From c5ab000e4ebbd6fd9ba509fc0cf423e5543e434a Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:33:06 +0000 Subject: [PATCH 48/52] Move up some responsibilities from generate_witness_conv --- src/base/runners.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 8674e8b84..b4832e092 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -308,7 +308,7 @@ struct module Witness_builder = struct type ('input_var, 'return_var, 'return_value, 'field, 'checked) t = { finish_witness_generation : - 'field Run_state.t * 'return_var -> Field.Vector.t * 'return_value + 'field Run_state.t * 'return_var -> Proof_inputs.t * 'return_value } let auxiliary_input ~run ~num_inputs ?(handlers = ([] : Handler.t list)) @@ -348,7 +348,8 @@ struct let fields = Array.map ~f:(Runner.get_value state) output_fields in return_typ.value_of_fields (fields, auxiliary_output_data) in - (aux, true_output) + ( { Proof_inputs.public_inputs = input; auxiliary_inputs = aux } + , true_output ) in ((state, res), { finish_witness_generation }) end @@ -411,10 +412,8 @@ struct Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output ~num_inputs k primary input_var in - let auxiliary, output = builder.finish_witness_generation (state, res) in - f - { Proof_inputs.public_inputs = primary; auxiliary_inputs = auxiliary } - output + let witness, output = builder.finish_witness_generation (state, res) in + f witness output let generate_witness = generate_witness_conv ~f:(fun inputs _output -> inputs) From 57d36ef12f925d7a029c4dcc5f687285d28ed2c1 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:39:44 +0000 Subject: [PATCH 49/52] Remove use of conv in generate_witness_conv and friends --- src/base/runners.ml | 35 ++++++++++++++--------------------- 1 file changed, 14 insertions(+), 21 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index b4832e092..8a3fe2296 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -311,9 +311,15 @@ struct 'field Run_state.t * 'return_var -> Proof_inputs.t * 'return_value } - let auxiliary_input ~run ~num_inputs ?(handlers = ([] : Handler.t list)) - t0 (input : Field.Vector.t) ~return_typ:(Types.Typ.Typ return_typ) - ~output input_var = + let auxiliary_input ~run ?(handlers = ([] : Handler.t list)) t0 ~input_typ + ~return_typ value = + let { Conv.input_var + ; output_var = output + ; first_auxiliary = num_inputs + ; primary_input = input + } = + Conv.receive_public_input input_typ return_typ value + in let next_auxiliary = ref num_inputs in let aux = Field.Vector.create () in let handler = @@ -327,6 +333,7 @@ struct in let state, res = run (t0 input_var) state in let finish_witness_generation (state, res) = + let (Typ return_typ) = return_typ in let res_fields, auxiliary_output_data = return_typ.var_to_fields res in @@ -376,19 +383,12 @@ struct -> 'k_var -> 'k_value = fun ~run ~input_typ ~return_typ ?handlers k value -> - let { Conv.input_var - ; output_var = output - ; first_auxiliary = num_inputs - ; primary_input = primary - } = - Conv.receive_public_input input_typ return_typ value - in (* NB: No need to finish witness generation, we'll discard the witness and public output anyway. *) let (state, res), { Witness_builder.finish_witness_generation = _ } = - Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output - ~num_inputs k primary input_var + Witness_builder.auxiliary_input ~run ?handlers ~input_typ ~return_typ k + value in ignore (state, res) @@ -401,16 +401,9 @@ struct -> 'k_var -> 'k_value = fun ~run ~f ~input_typ ~return_typ ?handlers k value -> - let { Conv.input_var - ; output_var = output - ; first_auxiliary = num_inputs - ; primary_input = primary - } = - Conv.receive_public_input input_typ return_typ value - in let (state, res), builder = - Witness_builder.auxiliary_input ~run ?handlers ~return_typ ~output - ~num_inputs k primary input_var + Witness_builder.auxiliary_input ~run ?handlers ~input_typ ~return_typ k + value in let witness, output = builder.finish_witness_generation (state, res) in f witness output From f302c5a9aa06e8d2d2a1579d2603a595f1be821f Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 06:45:37 +0000 Subject: [PATCH 50/52] Add `run_computation` to builder, stop calling the circuit internally --- src/base/runners.ml | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/src/base/runners.ml b/src/base/runners.ml index 8a3fe2296..bcfef9750 100644 --- a/src/base/runners.ml +++ b/src/base/runners.ml @@ -307,11 +307,12 @@ struct module Witness_builder = struct type ('input_var, 'return_var, 'return_value, 'field, 'checked) t = - { finish_witness_generation : + { run_computation : 'a. ('input_var -> 'field Run_state.t -> 'a) -> 'a + ; finish_witness_generation : 'field Run_state.t * 'return_var -> Proof_inputs.t * 'return_value } - let auxiliary_input ~run ?(handlers = ([] : Handler.t list)) t0 ~input_typ + let auxiliary_input ?(handlers = ([] : Handler.t list)) ~input_typ ~return_typ value = let { Conv.input_var ; output_var = output @@ -331,7 +332,7 @@ struct ~next_auxiliary ~aux:(pack_field_vec aux) ~handler ~with_witness:true () in - let state, res = run (t0 input_var) state in + let run_computation t0 = t0 input_var state in let finish_witness_generation (state, res) = let (Typ return_typ) = return_typ in let res_fields, auxiliary_output_data = @@ -358,7 +359,7 @@ struct ( { Proof_inputs.public_inputs = input; auxiliary_inputs = aux } , true_output ) in - ((state, res), { finish_witness_generation }) + { run_computation; finish_witness_generation } end let conv : @@ -386,9 +387,11 @@ struct (* NB: No need to finish witness generation, we'll discard the witness and public output anyway. *) - let (state, res), { Witness_builder.finish_witness_generation = _ } = - Witness_builder.auxiliary_input ~run ?handlers ~input_typ ~return_typ k - value + let { Witness_builder.run_computation; finish_witness_generation = _ } = + Witness_builder.auxiliary_input ?handlers ~input_typ ~return_typ value + in + let state, res = + run_computation (fun input_var state -> run (k input_var) state) in ignore (state, res) @@ -401,9 +404,12 @@ struct -> 'k_var -> 'k_value = fun ~run ~f ~input_typ ~return_typ ?handlers k value -> - let (state, res), builder = - Witness_builder.auxiliary_input ~run ?handlers ~input_typ ~return_typ k - value + let builder = + Witness_builder.auxiliary_input ?handlers ~input_typ ~return_typ value + in + let state, res = + builder.run_computation (fun input_var state -> + run (k input_var) state ) in let witness, output = builder.finish_witness_generation (state, res) in f witness output From d9c4828ca18269f65563d048c8627d49323ff212 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Sun, 11 Feb 2024 07:29:29 +0000 Subject: [PATCH 51/52] Add callback versions of constraint_system and generate_witness --- src/base/snark0.ml | 90 ++++++++++++++++++++++++++++++++++++++++++ src/base/snark_intf.ml | 19 +++++++++ 2 files changed, 109 insertions(+) diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 04a296cf4..be2853840 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -1294,6 +1294,53 @@ module Run = struct let x = inject_wrapper x ~f:(fun x () -> mark_active ~f:x) in Perform.constraint_system ~run:as_stateful ~input_typ ~return_typ x ) + type ('input_var, 'return_var, 'result) manual_callbacks = + { run_circuit : 'a. ('input_var -> unit -> 'a) -> 'a + ; finish_computation : 'return_var -> 'result + } + + let constraint_system_manual ~input_typ ~return_typ = + let builder = + Run.Constraint_system_builder.build ~input_typ ~return_typ + in + (* FIXME: This behaves badly with exceptions. *) + let cached_state = ref None in + let cached_active_counters = ref None in + let run_circuit circuit = + (* Check the status. *) + if + Option.is_some !cached_state || Option.is_some !cached_active_counters + then failwith "Already generating constraint system" ; + (* Partial [finalize_is_running]. *) + cached_state := Some !state ; + builder.run_computation (fun input state' -> + (* Partial [as_stateful]. *) + state := state' ; + (* Partial [mark_active]. *) + let counters = !active_counters in + cached_active_counters := Some counters ; + active_counters := this_functor_id :: counters ; + (* Start the circuit. *) + circuit input () ) + in + let finish_computation return_var = + (* Check the status. *) + if + Option.is_none !cached_state || Option.is_none !cached_active_counters + then failwith "Constraint system not in a finalizable state" ; + (* Partial [mark_active]. *) + active_counters := Option.value_exn !cached_active_counters ; + (* Create an invalid state, to avoid re-runs. *) + cached_active_counters := None ; + (* Partial [as_stateful]. *) + let state' = !state in + let res = builder.finish_computation (state', return_var) in + (* Partial [finalize_is_running]. *) + state := Option.value_exn !cached_state ; + res + in + { run_circuit; finish_computation } + let generate_public_input t x : As_prover.Vector.t = finalize_is_running (fun () -> generate_public_input t x) @@ -1310,6 +1357,49 @@ module Run = struct Perform.generate_witness_conv ~run:as_stateful ~f ~input_typ ~return_typ x input ) + let generate_witness_manual ?handlers ~input_typ ~return_typ input = + let builder = + Run.Witness_builder.auxiliary_input ?handlers ~input_typ ~return_typ + input + in + (* FIXME: This behaves badly with exceptions. *) + let cached_state = ref None in + let cached_active_counters = ref None in + let run_circuit circuit = + (* Check the status. *) + if + Option.is_some !cached_state || Option.is_some !cached_active_counters + then failwith "Already generating constraint system" ; + (* Partial [finalize_is_running]. *) + cached_state := Some !state ; + builder.run_computation (fun input state' -> + (* Partial [as_stateful]. *) + state := state' ; + (* Partial [mark_active]. *) + let counters = !active_counters in + cached_active_counters := Some counters ; + active_counters := this_functor_id :: counters ; + (* Start the circuit. *) + circuit input () ) + in + let finish_computation return_var = + (* Check the status. *) + if + Option.is_none !cached_state || Option.is_none !cached_active_counters + then failwith "Constraint system not in a finalizable state" ; + (* Partial [mark_active]. *) + active_counters := Option.value_exn !cached_active_counters ; + (* Create an invalid state, to avoid re-runs. *) + cached_active_counters := None ; + (* Partial [as_stateful]. *) + let state' = !state in + let res = builder.finish_witness_generation (state', return_var) in + (* Partial [finalize_is_running]. *) + state := Option.value_exn !cached_state ; + res + in + { run_circuit; finish_computation } + let run_unchecked x = finalize_is_running (fun () -> Perform.run_unchecked ~run:as_stateful (fun () -> mark_active ~f:x) ) diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index 7db66f7fb..877296038 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -1380,6 +1380,25 @@ module type Run_basic = sig -> 'input_value -> Proof_inputs.t + type ('input_var, 'return_var, 'result) manual_callbacks = + { run_circuit : 'a. ('input_var -> unit -> 'a) -> 'a + ; finish_computation : 'return_var -> 'result + } + + (** Callback version of [constraint_system]. *) + val constraint_system_manual : + input_typ:('input_var, 'input_value) Typ.t + -> return_typ:('return_var, 'return_value) Typ.t + -> ('input_var, 'return_var, R1CS_constraint_system.t) manual_callbacks + + (** Callback version of [generate_witness]. *) + val generate_witness_manual : + ?handlers:(request -> response) list + -> input_typ:('input_var, 'input_value) Typ.t + -> return_typ:('return_var, 'return_value) Typ.t + -> 'input_value + -> ('input_var, 'return_var, Proof_inputs.t * 'return_value) manual_callbacks + (** Generate the public input vector for a given statement. *) val generate_public_input : ('input_var, 'input_value) Typ.t -> 'input_value -> Field.Constant.Vector.t From 4f7006fe375302c5aa9abf85b66554ca2e0bb13c Mon Sep 17 00:00:00 2001 From: Gregor Date: Wed, 28 Feb 2024 14:53:05 +0100 Subject: [PATCH 52/52] ocamlformat --- src/base/snark_intf.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index 877296038..777ef6c66 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -1381,9 +1381,9 @@ module type Run_basic = sig -> Proof_inputs.t type ('input_var, 'return_var, 'result) manual_callbacks = - { run_circuit : 'a. ('input_var -> unit -> 'a) -> 'a - ; finish_computation : 'return_var -> 'result - } + { run_circuit : 'a. ('input_var -> unit -> 'a) -> 'a + ; finish_computation : 'return_var -> 'result + } (** Callback version of [constraint_system]. *) val constraint_system_manual : @@ -1397,7 +1397,10 @@ module type Run_basic = sig -> input_typ:('input_var, 'input_value) Typ.t -> return_typ:('return_var, 'return_value) Typ.t -> 'input_value - -> ('input_var, 'return_var, Proof_inputs.t * 'return_value) manual_callbacks + -> ( 'input_var + , 'return_var + , Proof_inputs.t * 'return_value ) + manual_callbacks (** Generate the public input vector for a given statement. *) val generate_public_input :