From 8cbda0b73334954794021712b6305b3ba8a54404 Mon Sep 17 00:00:00 2001 From: Gregor Date: Wed, 28 Feb 2024 16:04:11 +0100 Subject: [PATCH 1/4] expose state --- src/base/snark_intf.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index 777ef6c66..a54d6d418 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -1122,6 +1122,9 @@ module type Run_basic = sig (** The finite field over which the R1CS operates. *) type field + (* a reference to the internal Run_state.t *) + val state : field Run_state.t ref + module Bigint : sig include Snarky_intf.Bigint_intf.Extended with type field := field From 1b07509eaa4e87cf1fa3e777aa70647aa412553e Mon Sep 17 00:00:00 2001 From: Gregor Date: Tue, 5 Mar 2024 13:33:08 +0100 Subject: [PATCH 2/4] add state accessors --- src/base/snark0.ml | 4 ++++ src/base/snark_intf.ml | 16 ++++++++++++---- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 9521fad9f..202aad44f 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -724,6 +724,10 @@ module Run = struct ~eval_constraints:false ~num_inputs:0 ~next_auxiliary:(ref 0) ~with_witness:false ~stack:[] ~is_running:false () ) + let get_state () = !state + + let set_state s = state := s + let dump () = Run_state.dump !state let in_prover () : bool = Run_state.has_witness !state diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index 877296038..242dac132 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -1122,6 +1122,11 @@ module type Run_basic = sig (** The finite field over which the R1CS operates. *) type field + (* get and set the internal Run_state.t *) + val get_state : unit -> field Run_state.t + + val set_state : field Run_state.t -> unit + module Bigint : sig include Snarky_intf.Bigint_intf.Extended with type field := field @@ -1381,9 +1386,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 +1402,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 : From 46b1300da2e6c66ff68506b62009df2b762eb417 Mon Sep 17 00:00:00 2001 From: Gregor Date: Tue, 5 Mar 2024 16:40:22 +0100 Subject: [PATCH 3/4] instead of exposing state, add a manual version of exists --- src/base/snark0.ml | 39 +++++++++++++++++++++++++++++++++++---- src/base/snark_intf.ml | 8 +++----- 2 files changed, 38 insertions(+), 9 deletions(-) diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 202aad44f..15f8f6ee0 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -724,10 +724,6 @@ module Run = struct ~eval_constraints:false ~num_inputs:0 ~next_auxiliary:(ref 0) ~with_witness:false ~stack:[] ~is_running:false () ) - let get_state () = !state - - let set_state s = state := s - let dump () = Run_state.dump !state let in_prover () : bool = Run_state.has_witness !state @@ -1397,6 +1393,41 @@ module Run = struct in { run_circuit; finish_computation } + (* start an as_prover / exists block and return a function to finish it and witness a given list of fields *) + let as_prover_manual (size_to_witness : int) : + field array option -> Field.t array = + let s = !state in + let old_as_prover = Run_state.as_prover s in + (* enter the as_prover block *) + Run_state.set_as_prover s true ; + + let finish_computation (values_to_witness : field array option) = + (* leave the as_prover block *) + Run_state.set_as_prover s old_as_prover ; + + (* return variables *) + match (Run_state.has_witness s, values_to_witness) with + (* in compile mode, we return empty vars *) + | false, None -> + Core_kernel.Array.init size_to_witness ~f:(fun _ -> + Run_state.alloc_var s () ) + (* in prover mode, we expect values to turn into vars *) + | true, Some values_to_witness -> + let store_value = + (* If we're nested in a prover block, create constants instead of + storing. *) + if old_as_prover then Field.constant + else Run_state.store_field_elt s + in + Core_kernel.Array.map values_to_witness ~f:store_value + (* the other cases are invalid *) + | false, Some _ -> + failwith "Did not expect values to witness" + | true, None -> + failwith "Expected values to witness" + in + 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 242dac132..bd2706888 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -1122,11 +1122,6 @@ module type Run_basic = sig (** The finite field over which the R1CS operates. *) type field - (* get and set the internal Run_state.t *) - val get_state : unit -> field Run_state.t - - val set_state : field Run_state.t -> unit - module Bigint : sig include Snarky_intf.Bigint_intf.Extended with type field := field @@ -1407,6 +1402,9 @@ module type Run_basic = sig , Proof_inputs.t * 'return_value ) manual_callbacks + (* Callback, low-level version of [as_prover] and [exists]. *) + val as_prover_manual : int -> field array option -> Field.t array + (** 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 f27f6d8c7065ffc840d4f3e80e17e44de02da653 Mon Sep 17 00:00:00 2001 From: Gregor Date: Tue, 5 Mar 2024 17:27:01 +0100 Subject: [PATCH 4/4] use staged --- src/base/snark0.ml | 4 ++-- src/base/snark_intf.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 15f8f6ee0..473b7117a 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -1395,7 +1395,7 @@ module Run = struct (* start an as_prover / exists block and return a function to finish it and witness a given list of fields *) let as_prover_manual (size_to_witness : int) : - field array option -> Field.t array = + (field array option -> Field.t array) Staged.t = let s = !state in let old_as_prover = Run_state.as_prover s in (* enter the as_prover block *) @@ -1426,7 +1426,7 @@ module Run = struct | true, None -> failwith "Expected values to witness" in - finish_computation + Staged.stage finish_computation let run_unchecked x = finalize_is_running (fun () -> diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index bd2706888..a6416ca31 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -1403,7 +1403,7 @@ module type Run_basic = sig manual_callbacks (* Callback, low-level version of [as_prover] and [exists]. *) - val as_prover_manual : int -> field array option -> Field.t array + val as_prover_manual : int -> (field array option -> Field.t array) Staged.t (** Generate the public input vector for a given statement. *) val generate_public_input :