Merge pull request #15919 from MinaProtocol/feature/refined-statement…

…-types

Give a name to an overly-verbose pickles type

src/lib/pickles/common.ml

@@ -218,11 +218,10 @@ let tock_public_input_of_statement ~feature_flags s =
   tock_unpadded_public_input_of_statement ~feature_flags s
 
 let tick_public_input_of_statement ~max_proofs_verified
-    (prev_statement : _ Types.Step.Statement.t) =
+    (prev_statement : _ Impls.Step.statement) =
   let input =
     let (T (input, _conv, _conv_inv)) =
       Impls.Step.input ~proofs_verified:max_proofs_verified
-        ~wrap_rounds:Tock.Rounds.n
     in
     Impls.Step.generate_public_input input prev_statement
   in

src/lib/pickles/common.mli

@@ -163,23 +163,8 @@ val hash_messages_for_next_step_proof :
   -> Import.Types.Digest.Constant.t
 
 val tick_public_input_of_statement :
-     max_proofs_verified:'a Pickles_types.Nat.t
-  -> ( ( ( Impls.Step.Challenge.Constant.t
-         , Impls.Step.Challenge.Constant.t Composition_types.Scalar_challenge.t
-         , Impls.Step.Other_field.Constant.t Pickles_types.Shifted_value.Type2.t
-         , ( Limb_vector.Challenge.Constant.t
-             Kimchi_backend_common.Scalar_challenge.t
-             Composition_types.Bulletproof_challenge.t
-           , Pickles_types.Nat.z Backend.Tock.Rounds.plus_n )
-           Pickles_types.Vector.t
-         , Import.Types.Digest.Constant.t
-         , bool )
-         Composition_types.Step.Proof_state.Per_proof.In_circuit.t
-       , 'a )
-       Pickles_types.Vector.t
-     , Import.Types.Digest.Constant.t
-     , (Import.Types.Digest.Constant.t, 'a) Pickles_types.Vector.t )
-     Import.Types.Step.Statement.t
+     max_proofs_verified:'max_proofs_verified Pickles_types.Nat.t
+  -> 'max_proofs_verified Impls.Step.statement
   -> Backend.Tick.Field.Vector.elt list
 
 val tock_public_input_of_statement :

src/lib/pickles/compile.ml

@@ -560,9 +560,7 @@ struct
       let module M =
         H4.Map (Branch_data) (E04 (Lazy_keys))
           (struct
-            let etyp =
-              Impls.Step.input ~proofs_verified:Max_proofs_verified.n
-                ~wrap_rounds:Tock.Rounds.n
+            let etyp = Impls.Step.input ~proofs_verified:Max_proofs_verified.n
 
             let f (T b : _ Branch_data.t) =
               let open Impls.Step in

src/lib/pickles/impls.ml

@@ -112,9 +112,46 @@ module Step = struct
   module Digest = Digest.Make (Impl)
   module Challenge = Challenge.Make (Impl)
 
-  let input ~proofs_verified ~wrap_rounds =
+  type unfinalized_proof =
+    ( Challenge.Constant.t
+    , Challenge.Constant.t Scalar_challenge.t
+    , Tock.Field.t Shifted_value.Type2.t
+    , ( Challenge.Constant.t Scalar_challenge.t Bulletproof_challenge.t
+      , Tock.Rounds.n )
+      Vector.t
+    , Digest.Constant.t
+    , bool )
+    Types.Step.Proof_state.Per_proof.In_circuit.t
+
+  type 'proofs_verified statement =
+    ( (unfinalized_proof, 'proofs_verified) Pickles_types.Vector.t
+    , Import.Types.Digest.Constant.t
+    , (Import.Types.Digest.Constant.t, 'proofs_verified) Pickles_types.Vector.t
+    )
+    Import.Types.Step.Statement.t
+
+  type unfinalized_proof_var =
+    ( Field.t
+    , Field.t Scalar_challenge.t
+    , Other_field.t Shifted_value.Type2.t
+    , ( Field.t Scalar_challenge.t Bulletproof_challenge.t
+      , Tock.Rounds.n )
+      Pickles_types.Vector.t
+    , Field.t
+    , Boolean.var )
+    Types.Step.Proof_state.Per_proof.In_circuit.t
+
+  type 'proofs_verified statement_var =
+    ( (unfinalized_proof_var, 'proofs_verified) Pickles_types.Vector.t
+    , Impl.field Snarky_backendless.Cvar.t
+    , ( Impl.field Snarky_backendless.Cvar.t
+      , 'proofs_verified )
+      Pickles_types.Vector.t )
+    Import.Types.Step.Statement.t
+
+  let input ~proofs_verified =
     let open Types.Step.Statement in
-    let spec = spec proofs_verified wrap_rounds in
+    let spec = spec proofs_verified Tock.Rounds.n in
     let (T (typ, f, f_inv)) =
       Spec.packed_typ
         (module Impl)

src/lib/pickles/impls.mli

@@ -38,42 +38,45 @@ module Step : sig
     val typ : (t, Constant.t, Internal_Basic.field) Snarky_backendless.Typ.t
   end
 
+  type unfinalized_proof =
+    ( Challenge.Constant.t
+    , Challenge.Constant.t Import.Scalar_challenge.t
+    , Backend.Tock.Field.t Shifted_value.Type2.t
+    , ( Challenge.Constant.t Import.Scalar_challenge.t
+        Import.Types.Bulletproof_challenge.t
+      , Backend.Tock.Rounds.n )
+      Vector.t
+    , Digest.Constant.t
+    , bool )
+    Import.Types.Step.Proof_state.Per_proof.In_circuit.t
+
+  type 'proofs_verified statement =
+    ( (unfinalized_proof, 'proofs_verified) Vector.t
+    , Import.Types.Digest.Constant.t
+    , (Import.Types.Digest.Constant.t, 'proofs_verified) Vector.t )
+    Import.Types.Step.Statement.t
+
+  type unfinalized_proof_var =
+    ( Field.t
+    , Field.t Import.Scalar_challenge.t
+    , Other_field.t Shifted_value.Type2.t
+    , ( Field.t Import.Scalar_challenge.t Import.Types.Bulletproof_challenge.t
+      , Backend.Tock.Rounds.n )
+      Vector.t
+    , Field.t
+    , Boolean.var )
+    Import.Types.Step.Proof_state.Per_proof.In_circuit.t
+
+  type 'proofs_verified statement_var =
+    ( (unfinalized_proof_var, 'proofs_verified) Vector.t
+    , Impl.field Snarky_backendless.Cvar.t
+    , (Impl.field Snarky_backendless.Cvar.t, 'proofs_verified) Vector.t )
+    Import.Types.Step.Statement.t
+
   val input :
-       proofs_verified:'a Pickles_types.Nat.t
-    -> wrap_rounds:'b Pickles_types.Nat.t
-    -> ( ( ( ( Impl.Field.t
-             , Impl.Field.t Composition_types.Scalar_challenge.t
-             , Other_field.t Pickles_types.Shifted_value.Type2.t
-             , ( Impl.field Snarky_backendless.Cvar.t
-                 Kimchi_backend_common.Scalar_challenge.t
-                 Composition_types.Bulletproof_challenge.t
-               , 'b )
-               Pickles_types.Vector.t
-             , Impl.field Snarky_backendless.Cvar.t
-             , Impl.field Snarky_backendless.Cvar.t
-               Snarky_backendless.Snark_intf.Boolean0.t )
-             Composition_types.Step.Proof_state.Per_proof.In_circuit.t
-           , 'a )
-           Pickles_types.Vector.t
-         , Impl.field Snarky_backendless.Cvar.t
-         , (Impl.field Snarky_backendless.Cvar.t, 'a) Pickles_types.Vector.t )
-         Import.Types.Step.Statement.t
-       , ( ( ( Challenge.Constant.t
-             , Challenge.Constant.t Composition_types.Scalar_challenge.t
-             , Other_field.Constant.t Pickles_types.Shifted_value.Type2.t
-             , ( Limb_vector.Challenge.Constant.t
-                 Kimchi_backend_common.Scalar_challenge.t
-                 Composition_types.Bulletproof_challenge.t
-               , 'b )
-               Pickles_types.Vector.t
-             , Import.Types.Digest.Constant.t
-             , bool )
-             Composition_types.Step.Proof_state.Per_proof.In_circuit.t
-           , 'a )
-           Pickles_types.Vector.t
-         , Import.Types.Digest.Constant.t
-         , (Import.Types.Digest.Constant.t, 'a) Pickles_types.Vector.t )
-         Import.Types.Step.Statement.t
+       proofs_verified:'proofs_verified Nat.t
+    -> ( 'proofs_verified statement_var
+       , 'proofs_verified statement
        , Impl.field )
        Import.Spec.ETyp.t
 

src/lib/pickles/pickles.ml

@@ -1154,7 +1154,6 @@ module Make_str (_ : Wire_types.Concrete) = struct
           let step_keypair =
             let etyp =
               Impls.Step.input ~proofs_verified:Max_proofs_verified.n
-                ~wrap_rounds:Tock.Rounds.n
             in
             let open Impls.Step in
             let k_p =
@@ -1367,7 +1366,7 @@ module Make_str (_ : Wire_types.Concrete) = struct
                       in
                       M.f prev_statement.messages_for_next_wrap_proof
                     in
-                    let prev_statement_with_hashes : _ Types.Step.Statement.t =
+                    let prev_statement_with_hashes : _ Impls.Step.statement =
                       { proof_state =
                           { prev_statement.proof_state with
                             messages_for_next_step_proof =

src/lib/pickles/step.ml

@@ -803,7 +803,6 @@ struct
                     , _next_statement_hashed ) =
       let (T (input, _conv, conv_inv)) =
         Impls.Step.input ~proofs_verified:Max_proofs_verified.n
-          ~wrap_rounds:Tock.Rounds.n
       in
       let%bind.Promise main = branch_data.main ~step_domains in
       let%bind.Promise step_domains = step_domains in

src/lib/pickles/step_branch_data.ml

@@ -215,7 +215,6 @@ let create
     in
     let etyp =
       Impls.Step.input ~proofs_verified:max_proofs_verified
-        ~wrap_rounds:Backend.Tock.Rounds.n
       (* TODO *)
     in
     let%bind.Promise () = chain_to in

src/lib/pickles/step_verifier.ml

@@ -1159,14 +1159,7 @@ struct
   let verify ~proofs_verified ~is_base_case ~sg_old ~sponge_after_index
       ~lookup_parameters ~feature_flags ~(proof : Wrap_proof.Checked.t) ~srs
       ~wrap_domain ~wrap_verification_key statement
-      (unfinalized :
-        ( _
-        , _
-        , _ Shifted_value.Type2.t
-        , _
-        , _
-        , _ )
-        Types.Step.Proof_state.Per_proof.In_circuit.t ) =
+      (unfinalized : Impls.Step.unfinalized_proof_var) =
     let public_input :
         [ `Field of Field.t | `Packed_bits of Field.t * int ] array =
       with_label "pack_statement" (fun () ->

src/lib/pickles/step_verifier.mli

@@ -161,17 +161,7 @@ val verify :
      , Step_main_inputs.Impl.field Composition_types.Branch_data.Checked.t )
      Import.Types.Wrap.Statement.In_circuit.t
      (* statement *)
-  -> ( Step_main_inputs.Impl.Field.t
-     , Step_main_inputs.Impl.Field.t Import.Scalar_challenge.t
-     , Other_field.t Pickles_types.Shifted_value.Type2.t
-     , ( Step_main_inputs.Impl.Field.t Import.Scalar_challenge.t
-         Import.Bulletproof_challenge.t
-       , 'd )
-       Pickles_types.Vector.t
-     , Step_main_inputs.Impl.Field.t
-     , Step_main_inputs.Impl.Boolean.var )
-     Import.Types.Step.Proof_state.Per_proof.In_circuit.t
-     (* unfinalized *)
+  -> Impls.Step.unfinalized_proof_var (* unfinalized *)
   -> Step_main_inputs.Impl.Boolean.var
 
 module For_tests_only : sig

src/lib/pickles/test/test_side_loaded_verification_key.ml

@@ -13,9 +13,7 @@ open Pickles_types
 let input_size w =
   (* This should be an affine function in [a]. *)
   let size proofs_verified =
-    let (T (Typ typ, _conv, _conv_inv)) =
-      Impls.Step.input ~proofs_verified ~wrap_rounds:Backend.Tock.Rounds.n
-    in
+    let (T (Typ typ, _conv, _conv_inv)) = Impls.Step.input ~proofs_verified in
     typ.size_in_field_elements
   in
   let f0 = size Nat.N0.n in
@@ -33,7 +31,6 @@ let test_input_size () =
         (let (T a) = Pickles_types.Nat.of_int n in
          let (T (Typ typ, _conv, _conv_inv)) =
            Impls.Step.input ~proofs_verified:a
-             ~wrap_rounds:Backend.Tock.Rounds.n
          in
          typ.size_in_field_elements ) )
 

src/lib/pickles/unfinalized.ml

@@ -10,33 +10,15 @@ module Shifted_value = Shifted_value.Type2
    is expected to verify. This allows for situations like the blockchain
    SNARK where we let the previous proof fail in the base case.
 *)
-type t =
-  ( Field.t
-  , Field.t Scalar_challenge.t
-  , Other_field.t Shifted_value.t
-  , ( Field.t Scalar_challenge.t Bulletproof_challenge.t
-    , Tock.Rounds.n )
-    Pickles_types.Vector.t
-  , Field.t
-  , Boolean.var )
-  Types.Step.Proof_state.Per_proof.In_circuit.t
+type t = Impls.Step.unfinalized_proof_var
 
 module Plonk_checks = struct
   include Plonk_checks
   include Plonk_checks.Make (Shifted_value) (Plonk_checks.Scalars.Tock)
 end
 
 module Constant = struct
-  type t =
-    ( Challenge.Constant.t
-    , Challenge.Constant.t Scalar_challenge.t
-    , Tock.Field.t Shifted_value.t
-    , ( Challenge.Constant.t Scalar_challenge.t Bulletproof_challenge.t
-      , Tock.Rounds.n )
-      Vector.t
-    , Digest.Constant.t
-    , bool )
-    Types.Step.Proof_state.Per_proof.In_circuit.t
+  type t = Impls.Step.unfinalized_proof
 
   let shift = Shifted_value.Shift.create (module Tock.Field)
 

src/lib/pickles/unfinalized.mli

@@ -1,31 +1,12 @@
 module Constant : sig
-  type t =
-    ( Import.Challenge.Constant.t
-    , Import.Challenge.Constant.t Import.Scalar_challenge.t
-    , Backend.Tock.Field.t Pickles_types.Shifted_value.Type2.t
-    , ( Import.Challenge.Constant.t Import.Scalar_challenge.t
-        Import.Bulletproof_challenge.t
-      , Backend.Tock.Rounds.n )
-      Pickles_types.Vector.t
-    , Import.Digest.Constant.t
-    , bool )
-    Import.Types.Step.Proof_state.Per_proof.In_circuit.t
+  type t = Impls.Step.unfinalized_proof
 
   (* val shift : Backend.Tock.Field.t Pickles_types.Shifted_value.Type2.Shift.t *)
 
   val dummy : t Lazy.t
 end
 
-type t =
-  ( Impls.Step.Field.t
-  , Impls.Step.Field.t Import.Scalar_challenge.t
-  , Impls.Step.Other_field.t Pickles_types.Shifted_value.Type2.t
-  , ( Impls.Step.Field.t Import.Scalar_challenge.t Import.Bulletproof_challenge.t
-    , Backend.Tock.Rounds.n )
-    Pickles_types.Vector.t
-  , Impls.Step.Field.t
-  , Impls.Step.Boolean.var )
-  Import.Types.Step.Proof_state.Per_proof.In_circuit.t
+type t = Impls.Step.unfinalized_proof_var
 
 val typ : wrap_rounds:'a -> (t, Constant.t) Impls.Step.Typ.t
 

src/lib/pickles/wrap.mli

@@ -100,16 +100,7 @@ val wrap :
            Import.Types.Wrap.Statement.In_circuit.t )
   -> Kimchi_pasta.Pallas_based_plonk.Keypair.t
   -> ( 'b
-     , ( ( Impls.Wrap.Challenge.Constant.t
-         , Impls.Wrap.Challenge.Constant.t Import.Types.Scalar_challenge.t
-         , Impls.Wrap.Field.Constant.t Pickles_types.Shifted_value.Type2.t
-         , ( Impls.Wrap.Challenge.Constant.t Import.Types.Scalar_challenge.t
-             Import.Types.Bulletproof_challenge.t
-           , Backend.Tock.Rounds.n )
-           Pickles_types.Vector.t
-         , Impls.Wrap.Digest.Constant.t
-         , bool )
-         Import.Types.Step.Proof_state.Per_proof.In_circuit.t
+     , ( Impls.Step.unfinalized_proof
        , 'max_proofs_verified )
        Pickles_types.Vector.t
      , ( Kimchi_pasta.Basic.Fp.Stable.Latest.t