From 8e15884db6b3421fe4b818637bf58f6b91900b8e Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Thu, 5 Oct 2023 22:51:20 +0100 Subject: [PATCH] Use arrays for chunks in Plonk_verification_evals.t --- .../common/dlog_plonk_based_keypair.ml | 8 +- src/lib/pickles/common.ml | 23 +-- src/lib/pickles/common.mli | 4 +- src/lib/pickles/compile.ml | 27 ++- src/lib/pickles/compile.mli | 4 +- src/lib/pickles/pickles.ml | 22 ++- src/lib/pickles/requests.ml | 5 +- src/lib/pickles/requests.mli | 2 +- src/lib/pickles/step.ml | 2 +- src/lib/pickles/step.mli | 2 +- src/lib/pickles/step_main.ml | 4 +- src/lib/pickles/step_verifier.ml | 23 ++- src/lib/pickles/step_verifier.mli | 6 +- src/lib/pickles/types_map.ml | 19 ++- src/lib/pickles/types_map.mli | 7 +- src/lib/pickles/verify.ml | 5 +- src/lib/pickles/wrap.mli | 3 +- src/lib/pickles/wrap_domains.ml | 6 +- src/lib/pickles/wrap_main.ml | 8 +- src/lib/pickles/wrap_main.mli | 4 +- src/lib/pickles/wrap_verifier.ml | 158 +++++++++--------- src/lib/pickles/wrap_verifier.mli | 12 +- src/lib/pickles_types/pcs_batch.ml | 15 +- src/lib/pickles_types/pcs_batch.mli | 8 +- 24 files changed, 220 insertions(+), 157 deletions(-) diff --git a/src/lib/crypto/kimchi_backend/common/dlog_plonk_based_keypair.ml b/src/lib/crypto/kimchi_backend/common/dlog_plonk_based_keypair.ml index 5a527071512..84d79803e2c 100644 --- a/src/lib/crypto/kimchi_backend/common/dlog_plonk_based_keypair.ml +++ b/src/lib/crypto/kimchi_backend/common/dlog_plonk_based_keypair.ml @@ -225,13 +225,13 @@ module Make (Inputs : Inputs_intf) = struct } let full_vk_commitments (t : Inputs.Verifier_index.t) : - ( Inputs.Curve.Affine.t - , Inputs.Curve.Affine.t option ) + ( Inputs.Curve.Affine.t array + , Inputs.Curve.Affine.t array option ) Pickles_types.Plonk_verification_key_evals.Step.t = - let g c : Inputs.Curve.Affine.t = + let g c : Inputs.Curve.Affine.t array = match Inputs.Poly_comm.of_backend_without_degree_bound c with | `Without_degree_bound x -> - x.(0) + x | `With_degree_bound _ -> assert false in diff --git a/src/lib/pickles/common.ml b/src/lib/pickles/common.ml index ce75b44a45d..4c5252b5a59 100644 --- a/src/lib/pickles/common.ml +++ b/src/lib/pickles/common.ml @@ -49,7 +49,8 @@ let hash_messages_for_next_step_proof ~app_state let g (x, y) = [ x; y ] in Tick_field_sponge.digest Tick_field_sponge.params (Types.Step.Proof_state.Messages_for_next_step_proof.to_field_elements t ~g - ~comm:(fun (x : Tock.Curve.Affine.t) -> Array.of_list (g x)) + ~comm:(fun (x : Tock.Curve.Affine.t array) -> + Array.concat_map x ~f:(fun x -> Array.of_list (g x)) ) ~app_state ) let dlog_pcs_batch (type nat proofs_verified total) @@ -230,22 +231,24 @@ let tick_public_input_of_statement ~max_proofs_verified ~f:(Backend.Tick.Field.Vector.get input) let ft_comm ~add:( + ) ~scale ~endoscale:_ ~negate - ~verification_key:(m : _ Plonk_verification_key_evals.t) ~alpha:_ + ~verification_key:(m : _ array Plonk_verification_key_evals.t) ~alpha:_ ~(plonk : _ Types.Wrap.Proof_state.Deferred_values.Plonk.In_circuit.t) ~t_comm = + let reduce_chunks comm = + let n = Array.length comm in + let res = ref comm.(n - 1) in + for i = n - 2 downto 0 do + res := comm.(i) + scale !res plonk.zeta_to_srs_length + done ; + !res + in let ( * ) x g = scale g x in let _, [ sigma_comm_last ] = Vector.split m.sigma_comm (snd (Plonk_types.Permuts_minus_1.add Nat.N1.n)) in + let sigma_comm_last = reduce_chunks sigma_comm_last in let f_comm = List.reduce_exn ~f:( + ) [ plonk.perm * sigma_comm_last ] in - let chunked_t_comm = - let n = Array.length t_comm in - let res = ref t_comm.(n - 1) in - for i = n - 2 downto 0 do - res := t_comm.(i) + scale !res plonk.zeta_to_srs_length - done ; - !res - in + let chunked_t_comm = reduce_chunks t_comm in f_comm + chunked_t_comm + negate (scale chunked_t_comm plonk.zeta_to_domain_size) diff --git a/src/lib/pickles/common.mli b/src/lib/pickles/common.mli index 52ed6859c0c..1cbf66c850a 100644 --- a/src/lib/pickles/common.mli +++ b/src/lib/pickles/common.mli @@ -40,7 +40,7 @@ val ft_comm : -> scale:('a -> 'b -> 'a) -> endoscale:('a -> 'c -> 'a) -> negate:('a -> 'a) - -> verification_key:'a Pickles_types.Plonk_verification_key_evals.t + -> verification_key:'a array Pickles_types.Plonk_verification_key_evals.t -> alpha:'c -> plonk: ( 'd @@ -145,7 +145,7 @@ end val hash_messages_for_next_step_proof : app_state:('a -> Kimchi_pasta.Basic.Fp.Stable.Latest.t Core_kernel.Array.t) - -> ( Backend.Tock.Curve.Affine.t + -> ( Backend.Tock.Curve.Affine.t array , 'a , ( Kimchi_pasta.Basic.Fp.Stable.Latest.t * Kimchi_pasta.Basic.Fp.Stable.Latest.t diff --git a/src/lib/pickles/compile.ml b/src/lib/pickles/compile.ml index 478401383ae..f85f4b271a6 100644 --- a/src/lib/pickles/compile.ml +++ b/src/lib/pickles/compile.ml @@ -117,8 +117,8 @@ type ('max_proofs_verified, 'branches, 'prev_varss) wrap_main_generic = , 'max_local_max_proofs_verifieds ) Full_signature.t -> ('prev_varss, 'branches) Hlist.Length.t - -> ( ( Wrap_main_inputs.Inner_curve.Constant.t - , Wrap_main_inputs.Inner_curve.Constant.t option ) + -> ( ( Wrap_main_inputs.Inner_curve.Constant.t array + , Wrap_main_inputs.Inner_curve.Constant.t array option ) Wrap_verifier.index' , 'branches ) Vector.t @@ -727,7 +727,11 @@ struct let step handler next_state = let wrap_vk = Lazy.force wrap_vk in S.f ?handler branch_data next_state ~prevs_length:prev_vars_length - ~self ~step_domains ~self_dlog_plonk_index:wrap_vk.commitments + ~self ~step_domains + ~self_dlog_plonk_index: + ((* TODO *) Plonk_verification_key_evals.map + ~f:(fun x -> [| x |]) + wrap_vk.commitments ) ~public_input ~auxiliary_typ ~feature_flags (Impls.Step.Keypair.pk (fst (Lazy.force step_pk))) wrap_vk.index @@ -771,8 +775,12 @@ struct Wrap.wrap ~proof_cache ~max_proofs_verified:Max_proofs_verified.n ~feature_flags ~actual_feature_flags:b.feature_flags full_signature.maxes wrap_requests ?tweak_statement - ~dlog_plonk_index:wrap_vk.commitments wrap_main ~typ ~step_vk - ~step_plonk_indices:(Lazy.force step_vks) ~actual_wrap_domains + ~dlog_plonk_index: + ((* TODO *) Plonk_verification_key_evals.map + ~f:(fun x -> [| x |]) + wrap_vk.commitments ) + wrap_main ~typ ~step_vk ~step_plonk_indices:(Lazy.force step_vks) + ~actual_wrap_domains (Impls.Wrap.Keypair.pk (fst (Lazy.force wrap_pk))) proof in @@ -819,7 +827,10 @@ struct ; proofs_verifieds ; max_proofs_verified ; public_input = typ - ; wrap_key = Lazy.map wrap_vk ~f:Verification_key.commitments + ; wrap_key = + Lazy.map wrap_vk ~f:(fun x -> + Plonk_verification_key_evals.map (Verification_key.commitments x) + ~f:(fun x -> [| x |]) ) ; wrap_vk = Lazy.map wrap_vk ~f:Verification_key.index ; wrap_domains ; step_domains @@ -847,7 +858,9 @@ module Side_loaded = struct ~log_2_domain_size:(Lazy.force d.wrap_vk).domain.log_size_of_group in { wrap_vk = Some (Lazy.force d.wrap_vk) - ; wrap_index = Lazy.force d.wrap_key + ; wrap_index = + Plonk_verification_key_evals.map (Lazy.force d.wrap_key) ~f:(fun x -> + x.(0) ) ; max_proofs_verified = Pickles_base.Proofs_verified.of_nat (Nat.Add.n d.max_proofs_verified) ; actual_wrap_domain_size diff --git a/src/lib/pickles/compile.mli b/src/lib/pickles/compile.mli index f54ebfe93ed..8adb2de2955 100644 --- a/src/lib/pickles/compile.mli +++ b/src/lib/pickles/compile.mli @@ -154,8 +154,8 @@ type ('max_proofs_verified, 'branches, 'prev_varss) wrap_main_generic = , 'max_local_max_proofs_verifieds ) Full_signature.t -> ('prev_varss, 'branches) Hlist.Length.t - -> ( ( Wrap_main_inputs.Inner_curve.Constant.t - , Wrap_main_inputs.Inner_curve.Constant.t option ) + -> ( ( Wrap_main_inputs.Inner_curve.Constant.t array + , Wrap_main_inputs.Inner_curve.Constant.t array option ) Wrap_verifier.index' , 'branches ) Vector.t diff --git a/src/lib/pickles/pickles.ml b/src/lib/pickles/pickles.ml index 55fc0828357..8d5690b17ff 100644 --- a/src/lib/pickles/pickles.ml +++ b/src/lib/pickles/pickles.ml @@ -224,7 +224,9 @@ module Make_str (_ : Wire_types.Concrete) = struct ~log_2_domain_size:(Lazy.force d.wrap_vk).domain.log_size_of_group in { wrap_vk = Some (Lazy.force d.wrap_vk) - ; wrap_index = Lazy.force d.wrap_key + ; wrap_index = + Plonk_verification_key_evals.map (Lazy.force d.wrap_key) + ~f:(fun x -> x.(0)) ; max_proofs_verified = Pickles_base.Proofs_verified.of_nat (Nat.Add.n d.max_proofs_verified) @@ -1291,7 +1293,10 @@ module Make_str (_ : Wire_types.Concrete) = struct S.f branch_data () ~feature_flags ~prevs_length:prev_vars_length ~self ~public_input:(Input typ) ~auxiliary_typ:Impls.Step.Typ.unit ~step_domains - ~self_dlog_plonk_index:wrap_vk.commitments + ~self_dlog_plonk_index: + ((* TODO *) Plonk_verification_key_evals.map + ~f:(fun x -> [| x |]) + wrap_vk.commitments ) (Impls.Step.Keypair.pk (fst (Lazy.force step_pk))) wrap_vk.index in @@ -1772,7 +1777,11 @@ module Make_str (_ : Wire_types.Concrete) = struct : _ P.Base.Wrap.t ) in wrap ~max_proofs_verified:Max_proofs_verified.n - full_signature.maxes ~dlog_plonk_index:wrap_vk.commitments + full_signature.maxes + ~dlog_plonk_index: + ((* TODO *) Plonk_verification_key_evals.map + ~f:(fun x -> [| x |]) + wrap_vk.commitments ) wrap_main A_value.to_field_elements ~pairing_vk ~step_domains:b.domains ~pairing_plonk_indices:(Lazy.force step_vks) ~wrap_domains @@ -1800,7 +1809,12 @@ module Make_str (_ : Wire_types.Concrete) = struct ; proofs_verifieds ; max_proofs_verified = (module Max_proofs_verified) ; public_input = typ - ; wrap_key = Lazy.map wrap_vk ~f:Verification_key.commitments + ; wrap_key = + Lazy.map wrap_vk ~f:(fun x -> + (* TODO *) + Plonk_verification_key_evals.map + ~f:(fun x -> [| x |]) + (Verification_key.commitments x) ) ; wrap_vk = Lazy.map wrap_vk ~f:Verification_key.index ; wrap_domains ; step_domains diff --git a/src/lib/pickles/requests.ml b/src/lib/pickles/requests.ml index 4ad0875d1c1..352f4a22eaa 100644 --- a/src/lib/pickles/requests.ml +++ b/src/lib/pickles/requests.ml @@ -129,7 +129,7 @@ module Step = struct , local_branches ) H3.T(Per_proof_witness.Constant.No_app_state).t t - | Wrap_index : Tock.Curve.Affine.t Plonk_verification_key_evals.t t + | Wrap_index : Tock.Curve.Affine.t array Plonk_verification_key_evals.t t | App_state : statement t | Return_value : return_value -> unit t | Auxiliary_value : auxiliary_value -> unit t @@ -183,7 +183,8 @@ module Step = struct , local_branches ) H3.T(Per_proof_witness.Constant.No_app_state).t t - | Wrap_index : Tock.Curve.Affine.t Plonk_verification_key_evals.t t + | Wrap_index : + Tock.Curve.Affine.t array Plonk_verification_key_evals.t t | App_state : statement t | Return_value : return_value -> unit t | Auxiliary_value : auxiliary_value -> unit t diff --git a/src/lib/pickles/requests.mli b/src/lib/pickles/requests.mli index 9eef00a1c78..6f9439de8ff 100644 --- a/src/lib/pickles/requests.mli +++ b/src/lib/pickles/requests.mli @@ -35,7 +35,7 @@ module Step : sig Hlist.H3.T(Per_proof_witness.Constant.No_app_state).t Snarky_backendless.Request.t | Wrap_index : - Backend.Tock.Curve.Affine.t Plonk_verification_key_evals.t + Backend.Tock.Curve.Affine.t array Plonk_verification_key_evals.t Snarky_backendless.Request.t | App_state : statement Snarky_backendless.Request.t | Return_value : return_value -> unit Snarky_backendless.Request.t diff --git a/src/lib/pickles/step.ml b/src/lib/pickles/step.ml index 48df56feaf5..ed38eb776ab 100644 --- a/src/lib/pickles/step.ml +++ b/src/lib/pickles/step.ml @@ -121,7 +121,7 @@ struct let expand_proof : type var value local_max_proofs_verified m. Impls.Wrap.Verification_key.t - -> 'a + -> _ array Plonk_verification_key_evals.t -> value -> (local_max_proofs_verified, local_max_proofs_verified) Proof.t -> (var, value, local_max_proofs_verified, m) Tag.t diff --git a/src/lib/pickles/step.mli b/src/lib/pickles/step.mli index e07411fab6d..54a2271ed40 100644 --- a/src/lib/pickles/step.mli +++ b/src/lib/pickles/step.mli @@ -33,7 +33,7 @@ module Make -> step_domains:(Import.Domains.t, 'self_branches) Pickles_types.Vector.t -> feature_flags:Opt.Flag.t Plonk_types.Features.Full.t -> self_dlog_plonk_index: - Backend.Tick.Inner_curve.Affine.t + Backend.Tick.Inner_curve.Affine.t array Pickles_types.Plonk_verification_key_evals.t -> public_input: ( 'var diff --git a/src/lib/pickles/step_main.ml b/src/lib/pickles/step_main.ml index 59079d407db..d5313005dca 100644 --- a/src/lib/pickles/step_main.ml +++ b/src/lib/pickles/step_main.ml @@ -339,9 +339,11 @@ let step_main : in Req.Compute_prev_proof_parts previous_proof_statements ) ; let dlog_plonk_index = + let num_chunks = (* TODO *) 1 in exists ~request:(fun () -> Req.Wrap_index) - (Plonk_verification_key_evals.typ Inner_curve.typ) + (Plonk_verification_key_evals.typ + (Typ.array ~length:num_chunks Inner_curve.typ) ) and prevs = exists (Prev_typ.f prev_proof_typs) ~request:(fun () -> Req.Proof_with_datas ) diff --git a/src/lib/pickles/step_verifier.ml b/src/lib/pickles/step_verifier.ml index 2008c39b4cc..702e9804b71 100644 --- a/src/lib/pickles/step_verifier.ml +++ b/src/lib/pickles/step_verifier.ml @@ -241,6 +241,13 @@ struct let combined_polynomial (* Corresponds to xi in figure 7 of WTS *) = with_label "combined_polynomial" (fun () -> Pcs_batch.combine_split_commitments pcs_batch + ~reduce_without_degree_bound:Array.to_list + ~reduce_with_degree_bound:(fun { Plonk_types.Poly_comm + .With_degree_bound + .unshifted + ; shifted + } -> + Array.to_list unshifted @ [ shifted ] ) ~scale_and_add:(fun ~(acc : [ `Maybe_finite of Boolean.var * Inner_curve.t @@ -572,14 +579,11 @@ struct let without_degree_bound = Vector.append (Vector.map sg_old ~f:(fun g -> [| g |])) - ( [| x_hat |] :: [| ft_comm |] :: z_comm :: [| m.generic_comm |] - :: [| m.psm_comm |] :: [| m.complete_add_comm |] - :: [| m.mul_comm |] :: [| m.emul_comm |] - :: [| m.endomul_scalar_comm |] + ( [| x_hat |] :: [| ft_comm |] :: z_comm :: m.generic_comm + :: m.psm_comm :: m.complete_add_comm :: m.mul_comm :: m.emul_comm + :: m.endomul_scalar_comm :: Vector.append w_comm - (Vector.append - (Vector.map m.coefficients_comm ~f:(fun g -> [| g |])) - (Vector.map sigma_comm_init ~f:(fun g -> [| g |])) + (Vector.append m.coefficients_comm sigma_comm_init (snd Plonk_types.(Columns.add Permuts_minus_1.n)) ) (snd Plonk_types.( @@ -1107,8 +1111,9 @@ struct let sponge = Sponge.create sponge_params in Array.iter (Types.index_to_field_elements - ~g:(fun (z : Inputs.Inner_curve.t) -> - List.to_array (Inner_curve.to_field_elements z) ) + ~g: + (Array.concat_map ~f:(fun (z : Inputs.Inner_curve.t) -> + List.to_array (Inner_curve.to_field_elements z) ) ) index ) ~f:(fun x -> Sponge.absorb sponge (`Field x)) ; sponge diff --git a/src/lib/pickles/step_verifier.mli b/src/lib/pickles/step_verifier.mli index 3feaa3b075d..1bbc74d88b1 100644 --- a/src/lib/pickles/step_verifier.mli +++ b/src/lib/pickles/step_verifier.mli @@ -76,7 +76,7 @@ val finalize_other_proof : val hash_messages_for_next_step_proof : index: - Step_main_inputs.Inner_curve.t + Step_main_inputs.Inner_curve.t array Pickles_types.Plonk_verification_key_evals.t -> ('s -> Step_main_inputs.Impl.Field.t array) -> ( ( 'a @@ -91,7 +91,7 @@ val hash_messages_for_next_step_proof : val hash_messages_for_next_step_proof_opt : index: - Step_main_inputs.Inner_curve.t + Step_main_inputs.Inner_curve.t array Pickles_types.Plonk_verification_key_evals.t -> ('s -> Step_main_inputs.Impl.Field.t array) -> Step_main_inputs.Sponge.t @@ -135,7 +135,7 @@ val verify : Step_main_inputs.Impl.field Composition_types.Branch_data.Proofs_verified.One_hot.Checked.t ] -> wrap_verification_key: - Step_main_inputs.Inner_curve.t + Step_main_inputs.Inner_curve.t array Pickles_types.Plonk_verification_key_evals.t -> ( Step_main_inputs.Impl.field Limb_vector.Challenge.t , Step_main_inputs.Impl.field Limb_vector.Challenge.t diff --git a/src/lib/pickles/types_map.ml b/src/lib/pickles/types_map.ml index a6ce9ba9d3f..3496edd08f3 100644 --- a/src/lib/pickles/types_map.ml +++ b/src/lib/pickles/types_map.ml @@ -16,7 +16,7 @@ module Basic = struct ; public_input : ('var, 'value) Impls.Step.Typ.t ; branches : 'n2 Nat.t ; wrap_domains : Domains.t - ; wrap_key : Tick.Inner_curve.Affine.t Plonk_verification_key_evals.t + ; wrap_key : Tick.Inner_curve.Affine.t array Plonk_verification_key_evals.t ; wrap_vk : Impls.Wrap.Verification_key.t ; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t } @@ -59,7 +59,10 @@ module Side_loaded = struct let wrap_key, wrap_vk = match ephemeral with | Some { index = `In_prover i | `In_both (i, _) } -> - (i.wrap_index, i.wrap_vk) + let wrap_index = + Plonk_verification_key_evals.map i.wrap_index ~f:(fun x -> [| x |]) + in + (wrap_index, i.wrap_vk) | _ -> failwithf "Side_loaded.to_basic: Expected `In_prover (%s)" __LOC__ () in @@ -95,7 +98,8 @@ module Compiled = struct ; proofs_verifieds : (int, 'branches) Vector.t (* For each branch in this rule, how many predecessor proofs does it have? *) ; public_input : ('a_var, 'a_value) Impls.Step.Typ.t - ; wrap_key : Tick.Inner_curve.Affine.t Plonk_verification_key_evals.t Lazy.t + ; wrap_key : + Tick.Inner_curve.Affine.t array Plonk_verification_key_evals.t Lazy.t ; wrap_vk : Impls.Wrap.Verification_key.t Lazy.t ; wrap_domains : Domains.t ; step_domains : (Domains.t, 'branches) Vector.t @@ -134,7 +138,7 @@ module For_step = struct ; proofs_verifieds : [ `Known of (Impls.Step.Field.t, 'branches) Vector.t | `Side_loaded ] ; public_input : ('a_var, 'a_value) Impls.Step.Typ.t - ; wrap_key : inner_curve_var Plonk_verification_key_evals.t + ; wrap_key : inner_curve_var array Plonk_verification_key_evals.t ; wrap_domain : [ `Known of Domain.t | `Side_loaded of @@ -157,11 +161,14 @@ module For_step = struct failwithf "For_step.side_loaded: Expected `In_circuit (%s)" __LOC__ () in let T = Nat.eq_exn branches Side_loaded_verification_key.Max_branches.n in + let wrap_key = + Plonk_verification_key_evals.map index.wrap_index ~f:(fun x -> [| x |]) + in { branches ; max_proofs_verified ; public_input ; proofs_verifieds = `Side_loaded - ; wrap_key = index.wrap_index + ; wrap_key ; wrap_domain = `Side_loaded index.actual_wrap_domain_size ; step_domains = `Side_loaded ; feature_flags @@ -186,7 +193,7 @@ module For_step = struct ; public_input ; wrap_key = Plonk_verification_key_evals.map (Lazy.force wrap_key) - ~f:Step_main_inputs.Inner_curve.constant + ~f:(Array.map ~f:Step_main_inputs.Inner_curve.constant) ; wrap_domain = `Known wrap_domains.h ; step_domains = `Known step_domains ; feature_flags diff --git a/src/lib/pickles/types_map.mli b/src/lib/pickles/types_map.mli index 991be8ff433..7377fce3206 100644 --- a/src/lib/pickles/types_map.mli +++ b/src/lib/pickles/types_map.mli @@ -11,7 +11,7 @@ module Basic : sig ; branches : 'n2 Pickles_types.Nat.t ; wrap_domains : Import.Domains.t ; wrap_key : - Backend.Tick.Inner_curve.Affine.t + Backend.Tick.Inner_curve.Affine.t array Pickles_types.Plonk_verification_key_evals.t ; wrap_vk : Impls.Wrap.Verification_key.t ; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t @@ -69,7 +69,7 @@ module Compiled : sig (* For each branch in this rule, how many predecessor proofs does it have? *) ; public_input : ('a_var, 'a_value) Impls.Step.Typ.t ; wrap_key : - Backend.Tick.Inner_curve.Affine.t + Backend.Tick.Inner_curve.Affine.t array Pickles_types.Plonk_verification_key_evals.t Lazy.t ; wrap_vk : Impls.Wrap.Verification_key.t Lazy.t @@ -88,7 +88,8 @@ module For_step : sig [ `Known of (Impls.Step.Field.t, 'branches) Pickles_types.Vector.t | `Side_loaded ] ; public_input : ('a_var, 'a_value) Impls.Step.Typ.t - ; wrap_key : inner_curve_var Pickles_types.Plonk_verification_key_evals.t + ; wrap_key : + inner_curve_var array Pickles_types.Plonk_verification_key_evals.t ; wrap_domain : [ `Known of Import.Domain.t | `Side_loaded of diff --git a/src/lib/pickles/verify.ml b/src/lib/pickles/verify.ml index b18a252b068..32f2b3464b0 100644 --- a/src/lib/pickles/verify.ml +++ b/src/lib/pickles/verify.ml @@ -157,7 +157,10 @@ let verify_heterogenous (ts : Instance.t list) = Common.hash_messages_for_next_step_proof ~app_state:A_value.to_field_elements (Reduced_messages_for_next_proof_over_same_field.Step.prepare - ~dlog_plonk_index:key.commitments + ~dlog_plonk_index: + (Plonk_verification_key_evals.map + ~f:(fun x -> [| x |]) + key.commitments ) { t.statement.messages_for_next_step_proof with app_state } ) ; proof_state = { deferred_values = diff --git a/src/lib/pickles/wrap.mli b/src/lib/pickles/wrap.mli index 71d58c592b6..c29d587a459 100644 --- a/src/lib/pickles/wrap.mli +++ b/src/lib/pickles/wrap.mli @@ -8,7 +8,8 @@ val wrap : and type ns = 'max_local_max_proofs_verifieds ) -> ('max_proofs_verified, 'max_local_max_proofs_verifieds) Requests.Wrap.t -> dlog_plonk_index: - Backend.Tock.Curve.Affine.t Pickles_types.Plonk_verification_key_evals.t + Backend.Tock.Curve.Affine.t array + Pickles_types.Plonk_verification_key_evals.t -> ( ( Impls.Wrap.Impl.Field.t , Impls.Wrap.Impl.Field.t Composition_types.Scalar_challenge.t , Impls.Wrap.Impl.Field.t Pickles_types.Shifted_value.Type1.t diff --git a/src/lib/pickles/wrap_domains.ml b/src/lib/pickles/wrap_domains.ml index 920b942b0cf..e8d27e2c20c 100644 --- a/src/lib/pickles/wrap_domains.ml +++ b/src/lib/pickles/wrap_domains.ml @@ -28,7 +28,11 @@ struct let dummy_step_keys = lazy (Vector.init num_choices ~f:(fun _ -> - let g = Backend.Tock.Inner_curve.(to_affine_exn one) in + let num_chunks = (* TODO *) 1 in + let g = + Array.init num_chunks ~f:(fun _ -> + Backend.Tock.Inner_curve.(to_affine_exn one) ) + in Verification_key.dummy_step_commitments g ) ) in Timer.clock __LOC__ ; diff --git a/src/lib/pickles/wrap_main.ml b/src/lib/pickles/wrap_main.ml index b751b3a2db5..ccdfbe2b8d2 100644 --- a/src/lib/pickles/wrap_main.ml +++ b/src/lib/pickles/wrap_main.ml @@ -90,8 +90,8 @@ let wrap_main , max_local_max_proofs_verifieds ) Full_signature.t ) (pi_branches : (prev_varss, branches) Hlist.Length.t) (step_keys : - ( ( Wrap_main_inputs.Inner_curve.Constant.t - , Wrap_main_inputs.Inner_curve.Constant.t option ) + ( ( Wrap_main_inputs.Inner_curve.Constant.t array + , Wrap_main_inputs.Inner_curve.Constant.t array option ) Wrap_verifier.index' , branches ) Vector.t @@ -214,11 +214,11 @@ let wrap_main (Vector.map (Lazy.force step_keys) ~f: (Plonk_verification_key_evals.Step.map - ~f:Inner_curve.constant ~f_opt:(function + ~f:(Array.map ~f:Inner_curve.constant) ~f_opt:(function | None -> Opt.nothing | Some x -> - Opt.just (Inner_curve.constant x) ) ) ) ) + Opt.just (Array.map ~f:Inner_curve.constant x) ) ) ) ) in let prev_step_accs = with_label __LOC__ (fun () -> diff --git a/src/lib/pickles/wrap_main.mli b/src/lib/pickles/wrap_main.mli index bb834f15b11..04d903002bc 100644 --- a/src/lib/pickles/wrap_main.mli +++ b/src/lib/pickles/wrap_main.mli @@ -9,8 +9,8 @@ val wrap_main : , 'max_local_max_proofs_verifieds ) Full_signature.t -> ('prev_varss, 'branches) Pickles_types.Hlist.Length.t - -> ( ( Wrap_main_inputs.Inner_curve.Constant.t - , Wrap_main_inputs.Inner_curve.Constant.t option ) + -> ( ( Wrap_main_inputs.Inner_curve.Constant.t array + , Wrap_main_inputs.Inner_curve.Constant.t array option ) Wrap_verifier.index' , 'branches ) Pickles_types.Vector.t diff --git a/src/lib/pickles/wrap_verifier.ml b/src/lib/pickles/wrap_verifier.ml index 049c4e22f45..da3e52994d5 100644 --- a/src/lib/pickles/wrap_verifier.ml +++ b/src/lib/pickles/wrap_verifier.ml @@ -192,10 +192,11 @@ struct let choose_key : type n. n One_hot_vector.t - -> ( (Inner_curve.t, (Inner_curve.t, Boolean.var) Opt.t) index' + -> ( (Inner_curve.t array, (Inner_curve.t array, Boolean.var) Opt.t) index' , n ) Vector.t - -> (Inner_curve.t, (Inner_curve.t, Boolean.var) Opt.t) index' = + -> (Inner_curve.t array, (Inner_curve.t array, Boolean.var) Opt.t) index' + = let open Tuple_lib in fun bs keys -> let open Field in @@ -204,7 +205,7 @@ struct keys ~f:(fun b key -> Plonk_verification_key_evals.Step.map key - ~f:(fun g -> Double.map g ~f:(( * ) (b :> t))) + ~f:(Array.map ~f:(fun g -> Double.map g ~f:(( * ) (b :> t)))) ~f_opt:(function (* Here, we split the 3 variants into 3 separate accumulators. This allows us to only compute the 'maybe' flag when we need to, and @@ -223,7 +224,8 @@ struct ([ (b, x) ], [], []) ) ) |> Vector.reduce_exn ~f: - (Plonk_verification_key_evals.Step.map2 ~f:(Double.map2 ~f:( + )) + (Plonk_verification_key_evals.Step.map2 + ~f:(Array.map2_exn ~f:(Double.map2 ~f:( + ))) ~f_opt:(fun (yes_1, maybe_1, no_1) (yes_2, maybe_2, no_2) -> (yes_1 @ yes_2, maybe_1 @ maybe_2, no_1 @ no_2) ) ) |> Plonk_verification_key_evals.Step.map ~f:Fn.id ~f_opt:(function @@ -239,8 +241,9 @@ struct let sum = somes |> List.map ~f:(fun ((b : Boolean.var), g) -> - Double.map g ~f:(( * ) (b :> t)) ) - |> List.reduce_exn ~f:(Double.map2 ~f:( + )) + Array.map g ~f:(Double.map ~f:(( * ) (b :> t))) ) + |> List.reduce_exn + ~f:(Array.map2_exn ~f:(Double.map2 ~f:( + ))) in Opt.just sum | somes, maybes, nones -> @@ -250,18 +253,20 @@ struct Boolean.Unsafe.of_cvar Field.(add (b1 :> t) (b2 :> t)) ) in let none_sum = + let num_chunks = (* TODO *) 1 in Option.map is_none ~f:(fun (b : Boolean.var) -> - Double.map Inner_curve.one ~f:(( * ) (b :> t)) ) + Array.init num_chunks ~f:(fun _ -> + Double.map Inner_curve.one ~f:(( * ) (b :> t)) ) ) in let some_is_yes, some_sum = somes |> List.map ~f:(fun ((b : Boolean.var), g) -> - (b, Double.map g ~f:(( * ) (b :> t))) ) + (b, Array.map g ~f:(Double.map ~f:(( * ) (b :> t)))) ) |> List.reduce ~f:(fun ((b1 : Boolean.var), g1) ((b2 : Boolean.var), g2) -> ( Boolean.Unsafe.of_cvar Field.(add (b1 :> t) (b2 :> t)) - , Double.map2 ~f:( + ) g1 g2 ) ) + , Array.map2_exn ~f:(Double.map2 ~f:( + )) g1 g2 ) ) |> fun x -> (Option.map ~f:fst x, Option.map ~f:snd x) in let maybe_is_yes, maybe_sum = @@ -269,12 +274,12 @@ struct |> List.map ~f:(fun ((b : Boolean.var), (b_g : Boolean.var), g) -> ( Boolean.Unsafe.of_cvar Field.(mul (b :> t) (b_g :> t)) - , Double.map g ~f:(( * ) (b :> t)) ) ) + , Array.map g ~f:(Double.map ~f:(( * ) (b :> t))) ) ) |> List.reduce ~f:(fun ((b1 : Boolean.var), g1) ((b2 : Boolean.var), g2) -> ( Boolean.Unsafe.of_cvar Field.(add (b1 :> t) (b2 :> t)) - , Double.map2 ~f:( + ) g1 g2 ) ) + , Array.map2_exn ~f:(Double.map2 ~f:( + )) g1 g2 ) ) |> fun x -> (Option.map ~f:fst x, Option.map ~f:snd x) in let is_yes = @@ -287,7 +292,8 @@ struct let sum = [| none_sum; maybe_sum; some_sum |] |> Array.filter_map ~f:Fn.id - |> Array.reduce_exn ~f:(Double.map2 ~f:( + )) + |> Array.reduce_exn + ~f:(Array.map2_exn ~f:(Double.map2 ~f:( + ))) in Opt.Maybe (is_yes, sum) ) @@ -411,12 +417,18 @@ struct [ `Finite of Inner_curve.t | `Maybe_finite of Boolean.var * Inner_curve.t ] - let finite : t -> Boolean.var = function + let _finite : t -> Boolean.var = function | `Finite _ -> Boolean.true_ | `Maybe_finite (b, _) -> b + let assert_finite : t -> unit = function + | `Finite _ -> + () + | `Maybe_finite _ -> + failwith "Not finite" + let add (p : t) (q : Inner_curve.t) = match p with | `Finite p -> @@ -432,10 +444,19 @@ struct end let combine batch ~xi without_bound with_bound = + let reduce_point p = + let point = ref (Point.underlying p.(Array.length p - 1)) in + for i = Array.length p - 2 downto 0 do + point := Point.add p.(i) (Scalar_challenge.endo !point xi) + done ; + !point + in let { Curve_opt.non_zero; point } = Pcs_batch.combine_split_commitments batch + ~reduce_with_degree_bound:(fun _ -> assert false) + ~reduce_without_degree_bound:(fun x -> [ x ]) ~scale_and_add:(fun ~(acc : Curve_opt.t) ~xi - (p : (Point.t, Boolean.var) Opt.t) -> + (p : (Point.t array, Boolean.var) Opt.t) -> (* match acc.non_zero, keep with | false, false -> acc | true, false -> acc @@ -443,22 +464,25 @@ struct | true, true -> { point= p + xi * acc; non_zero= true } *) let point keep p = - let point = + let base_point = + let p = p.(Array.length p - 1) in Inner_curve.( - if_ keep - ~then_: - (if_ acc.non_zero - ~then_: - (Point.add p (Scalar_challenge.endo acc.point xi)) - ~else_: - ((* In this branch, the accumulator was zero, so there is no harm in - putting the potentially junk underlying point here. *) - Point.underlying p ) ) - ~else_:acc.point) + if_ acc.non_zero + ~then_:(Point.add p (Scalar_challenge.endo acc.point xi)) + ~else_: + ((* In this branch, the accumulator was zero, so there is no harm in + putting the potentially junk underlying point here. *) + Point.underlying p )) in - let non_zero = - Boolean.(keep &&& Point.finite p ||| acc.non_zero) + let point = ref base_point in + for i = Array.length p - 2 downto 0 do + point := Point.add p.(i) (Scalar_challenge.endo !point xi) + done ; + let point = + Inner_curve.(if_ keep ~then_:!point ~else_:acc.point) in + Array.iter ~f:Point.assert_finite p ; + let non_zero = Boolean.(keep &&& true_ ||| acc.non_zero) in { Curve_opt.non_zero; point } in match p with @@ -473,14 +497,16 @@ struct | Opt.Nothing -> None | Opt.Maybe (keep, p) -> + Array.iter ~f:Point.assert_finite p ; Some - { non_zero = Boolean.(keep &&& Point.finite p) - ; point = Point.underlying p + { non_zero = Boolean.(keep &&& true_) + ; point = reduce_point p } | Opt.Just p -> + Array.iter ~f:Point.assert_finite p ; Some - { non_zero = Boolean.(true_ &&& Point.finite p) - ; point = Point.underlying p + { non_zero = Boolean.(true_ &&& true_) + ; point = reduce_point p } ) without_bound with_bound in @@ -730,7 +756,8 @@ struct let incrementally_verify_proof (type b) (module Max_proofs_verified : Nat.Add.Intf with type n = b) ~actual_proofs_verified_mask ~step_domains ~srs - ~verification_key:(m : _ Plonk_verification_key_evals.Step.t) ~xi ~sponge + ~verification_key:(m : (_ array, _) Plonk_verification_key_evals.Step.t) + ~xi ~sponge ~(public_input : [ `Field of Field.t * Boolean.var | `Packed_bits of Field.t * int ] array ) ~(sg_old : (_, Max_proofs_verified.n) Vector.t) ~advice @@ -740,7 +767,7 @@ struct let sg_old = with_label __LOC__ (fun () -> Vector.map2 actual_proofs_verified_mask sg_old ~f:(fun keep sg -> - [| (keep, sg) |] ) ) + (keep, sg) ) ) in with_label __LOC__ (fun () -> let sample () = Opt.challenge sponge in @@ -752,8 +779,9 @@ struct let index_sponge = Sponge.create sponge_params in List.iter (index_to_field_elements - ~g:(fun (z : Inputs.Inner_curve.t) -> - List.to_array (Inner_curve.to_field_elements z) ) + ~g: + (Array.concat_map ~f:(fun (z : Inputs.Inner_curve.t) -> + List.to_array (Inner_curve.to_field_elements z) ) ) m ) ~f:(fun x -> let (_ : (unit, _) Pickles_types.Opt.t) = @@ -769,7 +797,7 @@ struct absorb sponge without (Array.map gs ~f:(fun g -> (Boolean.true_, g))) in absorb sponge Field (Boolean.true_, index_digest) ; - Vector.iter ~f:(Array.iter ~f:(absorb sponge PC)) sg_old ; + Vector.iter ~f:(absorb sponge PC) sg_old ; let x_hat = let domain = (which_branch, step_domains) in let public_input = @@ -946,11 +974,7 @@ struct let lookup_table_comm = let compute_lookup_table_comm (l : _ Messages.Lookup.In_circuit.t) joint_combiner = - let (first_column :: second_column :: rest) = - Vector.map - ~f:(Types.Opt.map ~f:(fun x -> [| x |])) - m.lookup_table_comm - in + let (first_column :: second_column :: rest) = m.lookup_table_comm in let second_column_with_runtime = match (second_column, l.runtime) with | Types.Opt.Nothing, comm | comm, Types.Opt.Nothing -> @@ -1004,10 +1028,7 @@ struct let rest_rev = Vector.rev (first_column :: second_column_with_runtime :: rest) in - let table_ids = - Types.Opt.map m.lookup_table_ids ~f:(fun x -> [| x |]) - in - Vector.fold ~init:table_ids rest_rev ~f:(fun acc comm -> + Vector.fold ~init:m.lookup_table_ids rest_rev ~f:(fun acc comm -> match acc with | Types.Opt.Nothing -> comm @@ -1200,11 +1221,6 @@ struct let append_chain len second first = Vector.append first second len in - let undo_chunking = - Types.Opt.map ~f:(fun x -> - assert (Array.length x = 1) ; - x.(0) ) - in (* sg_old x_hat ft_comm @@ -1214,31 +1230,26 @@ struct w_comms all but last sigma_comm *) - Vector.map sg_old - ~f: - (Array.map ~f:(fun (keep, p) -> - Pickles_types.Opt.Maybe (keep, p) ) ) + Vector.map sg_old ~f:(fun (keep, p) -> + Pickles_types.Opt.Maybe (keep, [| p |]) ) |> append_chain (snd (Max_proofs_verified.add len_6)) ( [ [| x_hat |] ; [| ft_comm |] ; z_comm - ; [| m.generic_comm |] - ; [| m.psm_comm |] - ; [| m.complete_add_comm |] - ; [| m.mul_comm |] - ; [| m.emul_comm |] - ; [| m.endomul_scalar_comm |] + ; m.generic_comm + ; m.psm_comm + ; m.complete_add_comm + ; m.mul_comm + ; m.emul_comm + ; m.endomul_scalar_comm ] |> append_chain len_3_add (Vector.append w_comm - (Vector.append - (Vector.map m.coefficients_comm ~f:(fun g -> - [| g |] ) ) - (Vector.map sigma_comm_init ~f:(fun g -> [| g |])) + (Vector.append m.coefficients_comm sigma_comm_init len_1_add ) len_2_add ) - |> Vector.map ~f:(Array.map ~f:Pickles_types.Opt.just) + |> Vector.map ~f:Pickles_types.Opt.just |> append_chain len_6_add ( [ m.range_check0_comm ; m.range_check1_comm @@ -1247,20 +1258,17 @@ struct ; m.xor_comm ; m.rot_comm ] - |> append_chain len_4_add - (Vector.map ~f:undo_chunking lookup_sorted) + |> append_chain len_4_add lookup_sorted |> append_chain len_5_add - [ undo_chunking - @@ Pickles_types.Opt.map messages.lookup - ~f:(fun l -> l.aggreg) - ; undo_chunking lookup_table_comm + [ Pickles_types.Opt.map messages.lookup ~f:(fun l -> + l.aggreg ) + ; lookup_table_comm ; m.runtime_tables_selector ; m.lookup_selector_xor ; m.lookup_selector_lookup ; m.lookup_selector_range_check ; m.lookup_selector_ffmul - ] - |> Vector.map ~f:(fun x -> [| x |]) ) ) + ] ) ) in check_bulletproof ~pcs_batch: @@ -1270,8 +1278,8 @@ struct ~polynomials: ( Vector.map without_degree_bound ~f: - (Array.map - ~f:(Pickles_types.Opt.map ~f:(fun x -> `Finite x)) ) + (Pickles_types.Opt.map + ~f:(Array.map ~f:(fun x -> `Finite x)) ) , [] ) in assert_eq_plonk diff --git a/src/lib/pickles/wrap_verifier.mli b/src/lib/pickles/wrap_verifier.mli index 8a537cd3ab0..baffd665ecd 100644 --- a/src/lib/pickles/wrap_verifier.mli +++ b/src/lib/pickles/wrap_verifier.mli @@ -62,8 +62,8 @@ val incrementally_verify_proof : -> step_domains:(Import.Domains.t, 'a) Pickles_types.Vector.t -> srs:Kimchi_bindings.Protocol.SRS.Fp.t -> verification_key: - ( Wrap_main_inputs.Inner_curve.t - , ( Wrap_main_inputs.Inner_curve.t + ( Wrap_main_inputs.Inner_curve.t array + , ( Wrap_main_inputs.Inner_curve.t array , Impls.Wrap.Boolean.var ) Pickles_types.Opt.t ) Pickles_types.Plonk_verification_key_evals.Step.t @@ -144,15 +144,15 @@ val finalize_other_proof : val choose_key : 'n. 'n One_hot_vector.t - -> ( ( Wrap_main_inputs.Inner_curve.t - , ( Wrap_main_inputs.Inner_curve.t + -> ( ( Wrap_main_inputs.Inner_curve.t array + , ( Wrap_main_inputs.Inner_curve.t array , Impls.Wrap.Boolean.var ) Pickles_types.Opt.t ) index' , 'n ) Pickles_types.Vector.t - -> ( Wrap_main_inputs.Inner_curve.t - , ( Wrap_main_inputs.Inner_curve.t + -> ( Wrap_main_inputs.Inner_curve.t array + , ( Wrap_main_inputs.Inner_curve.t array , Impls.Wrap.Boolean.var ) Pickles_types.Opt.t ) index' diff --git a/src/lib/pickles_types/pcs_batch.ml b/src/lib/pickles_types/pcs_batch.ml index e4a37ef5d20..e115635c46e 100644 --- a/src/lib/pickles_types/pcs_batch.ml +++ b/src/lib/pickles_types/pcs_batch.ml @@ -65,15 +65,16 @@ let combine_evaluations (type f) t ~crs_max_degree ~(mul : f -> f -> f) ~add ~shifted_pow:(fun deg x -> pow x (crs_max_degree - deg)) ~mul ~add ~one ~evaluation_point ~xi -open Plonk_types.Poly_comm - -let combine_split_commitments _t ~scale_and_add ~init:i ~xi (type n) +let combine_split_commitments _t ~scale_and_add ~init:i ~xi + ~reduce_without_degree_bound ~reduce_with_degree_bound (type n) (without_degree_bound : (_, n) Vector.t) with_degree_bound = let flat = - List.concat_map (Vector.to_list without_degree_bound) ~f:Array.to_list - @ List.concat_map (Vector.to_list with_degree_bound) - ~f:(fun { With_degree_bound.unshifted; shifted } -> - Array.to_list unshifted @ [ shifted ] ) + List.concat_map + (Vector.to_list without_degree_bound) + ~f:reduce_without_degree_bound + @ List.concat_map + (Vector.to_list with_degree_bound) + ~f:reduce_with_degree_bound in let rec go = function | [] -> diff --git a/src/lib/pickles_types/pcs_batch.mli b/src/lib/pickles_types/pcs_batch.mli index 7317ae097ec..dee36ea90b4 100644 --- a/src/lib/pickles_types/pcs_batch.mli +++ b/src/lib/pickles_types/pcs_batch.mli @@ -46,15 +46,15 @@ val combine_evaluations' : -> ('f, 'm) Vector.t -> 'f -open Plonk_types.Poly_comm - val combine_split_commitments : (_, 'n, 'm) t -> scale_and_add:(acc:'g_acc -> xi:'f -> 'g -> 'g_acc) -> init:('g -> 'g_acc option) -> xi:'f - -> ('g Without_degree_bound.t, 'n) Vector.t - -> ('g With_degree_bound.t, 'm) Vector.t + -> reduce_without_degree_bound:('without_degree_bound -> 'g list) + -> reduce_with_degree_bound:('with_degree_bound -> 'g list) + -> ('without_degree_bound, 'n) Vector.t + -> ('with_degree_bound, 'm) Vector.t -> 'g_acc val combine_split_evaluations :