3409

Committed 26 Feb 2025 01:10PM UTC coverage: 32.353% (-28.4%) from 60.756%

Build # 3409

Build Type

push

buildkite

Committed by

web-flow

Commit Message

Merge pull request #16687 from MinaProtocol/dw/merge-compatible-into-develop-20250225

Merge compatible into develop [20250224]

Run Details

23144 of 71535 relevant lines covered (32.35%)

16324.05 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

44.32

/src/lib/pickles/types_map.ml

open Core_kernel
open Pickles_types
open Import
open Backend

(* We maintain a global hash table which stores for each inductive proof system some
   data.
*)
type inner_curve_var = Impls.Step.Field.t * Impls.Step.Field.t

module Basic = struct
  type ('var, 'value, 'n1, 'n2) t =
    { max_proofs_verified : (module Nat.Add.Intf with type n = 'n1)
    ; public_input : ('var, 'value) Impls.Step.Typ.t
    ; branches : 'n2 Nat.t
    ; wrap_domains : Domains.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
    ; num_chunks : int
    ; zk_rows : int
    }
end

module Side_loaded = struct
  module Ephemeral = struct
    type t =
      { index :
          [ `In_circuit of Side_loaded_verification_key.Checked.t
          | `In_prover of Side_loaded_verification_key.t
          | `In_both of
            Side_loaded_verification_key.t
            * Side_loaded_verification_key.Checked.t ]
      }
  end

  module Permanent = struct
    type ('var, 'value, 'n1, 'n2) t =
      { max_proofs_verified : (module Nat.Add.Intf with type n = 'n1)
      ; public_input : ('var, 'value) Impls.Step.Typ.t
      ; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t
      ; branches : 'n2 Nat.t
      ; num_chunks : int
      ; zk_rows : int
      }
  end

  type ('var, 'value, 'n1, 'n2) t =
    { ephemeral : Ephemeral.t option
    ; permanent : ('var, 'value, 'n1, 'n2) Permanent.t
    }

  type packed =
    | T : ('var, 'value, 'n1, 'n2) Tag.id * ('var, 'value, 'n1, 'n2) t -> packed

  let to_basic
      { permanent =
          { max_proofs_verified
          ; public_input
          ; branches
          ; feature_flags
          ; num_chunks
          ; zk_rows
          }
      ; ephemeral
      } =
    let wrap_key, wrap_vk =
      match ephemeral with
      | Some { index = `In_prover i | `In_both (i, _) } ->
          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
    let proofs_verified = Nat.to_int (Nat.Add.n max_proofs_verified) in
    let wrap_vk = Option.value_exn ~here:[%here] wrap_vk in
    { Basic.max_proofs_verified
    ; wrap_vk
    ; public_input
    ; branches
    ; wrap_domains = Common.wrap_domains ~proofs_verified
    ; wrap_key
    ; feature_flags
    ; num_chunks
    ; zk_rows
    }
end

module Compiled = struct
  type ('a_var, 'a_value, 'max_proofs_verified, 'branches) basic =
    { public_input : ('a_var, 'a_value) Impls.Step.Typ.t
    ; proofs_verifieds : (int, 'branches) Vector.t
          (* For each branch in this rule, how many predecessor proofs does it have? *)
    ; wrap_domains : Domains.t
    ; step_domains : (Domains.t, 'branches) Vector.t
    ; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t
    ; num_chunks : int
    ; zk_rows : int
    }

  (* This is the data associated to an inductive proof system with statement type
     ['a_var], which has ['branches] many "variants" each of which depends on at most
     ['max_proofs_verified] many previous statements. *)
  type ('a_var, 'a_value, 'max_proofs_verified, 'branches) t =
    { branches : 'branches Nat.t
    ; max_proofs_verified :
        (module Nat.Add.Intf with type n = 'max_proofs_verified)
    ; 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 array Plonk_verification_key_evals.t Promise.t
        Lazy.t
    ; wrap_vk : Impls.Wrap.Verification_key.t Promise.t Lazy.t
    ; wrap_domains : Domains.t
    ; step_domains : (Domains.t Promise.t, 'branches) Vector.t
    ; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t
    ; num_chunks : int
    ; zk_rows : int
    }

  type packed =
    | T : ('var, 'value, 'n1, 'n2) Tag.id * ('var, 'value, 'n1, 'n2) t -> packed

  let to_basic
      { branches = _
      ; max_proofs_verified
      ; proofs_verifieds = _
      ; public_input
      ; wrap_vk
      ; wrap_domains
      ; step_domains
      ; wrap_key
      ; feature_flags
      ; num_chunks
      ; zk_rows
      } =
    let%bind.Promise wrap_key = Lazy.force wrap_key in
    let%map.Promise wrap_vk = Lazy.force wrap_vk in
    { Basic.max_proofs_verified
    ; wrap_domains
    ; public_input
    ; branches = Vector.length step_domains
    ; wrap_key
    ; wrap_vk
    ; feature_flags
    ; num_chunks
    ; zk_rows
    }
end

module For_step = struct
  type ('a_var, 'a_value, 'max_proofs_verified, 'branches) t =
    { branches : 'branches Nat.t
    ; max_proofs_verified :
        (module Nat.Add.Intf with type n = 'max_proofs_verified)
    ; 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 array Plonk_verification_key_evals.t
    ; wrap_domain :
        [ `Known of Domain.t
        | `Side_loaded of Pickles_base.Proofs_verified.One_hot.Checked.t ]
    ; step_domains : [ `Known of (Domains.t, 'branches) Vector.t | `Side_loaded ]
    ; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t
    ; num_chunks : int
    ; zk_rows : int
    }

  let of_side_loaded (type a b c d)
      ({ ephemeral
       ; permanent =
           { branches
           ; max_proofs_verified
           ; public_input
           ; feature_flags
           ; num_chunks
           ; zk_rows
           }
       } :
        (a, b, c, d) Side_loaded.t ) : (a, b, c, d) t =
    let index =
      match ephemeral with
      | Some { index = `In_circuit i | `In_both (_, i) } ->
          i
      | _ ->
          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
    ; wrap_domain = `Side_loaded index.actual_wrap_domain_size
    ; step_domains = `Side_loaded
    ; feature_flags
    ; num_chunks
    ; zk_rows
    }

  module Optional_wrap_key = struct
    type 'branches known =
      { wrap_key :
          Tick.Inner_curve.Affine.t array Plonk_verification_key_evals.t
      ; step_domains : (Domains.t, 'branches) Vector.t
      }

    type 'branches t = 'branches known option
  end

  let of_compiled_with_known_wrap_key
      ({ wrap_key; step_domains } : _ Optional_wrap_key.known)
      ({ branches
       ; max_proofs_verified
       ; proofs_verifieds
       ; public_input
       ; wrap_key = _
       ; wrap_domains
       ; step_domains = _
       ; feature_flags
       ; wrap_vk = _
       ; num_chunks
       ; zk_rows
       } :
        _ Compiled.t ) =
    { branches
    ; max_proofs_verified
    ; proofs_verifieds =
        `Known (Vector.map proofs_verifieds ~f:Impls.Step.Field.of_int)
    ; public_input
    ; wrap_key =
        Plonk_verification_key_evals.map wrap_key
          ~f:(Array.map ~f:Step_main_inputs.Inner_curve.constant)
    ; wrap_domain = `Known wrap_domains.h
    ; step_domains = `Known step_domains
    ; feature_flags
    ; num_chunks
    ; zk_rows
    }

  let of_compiled ({ wrap_key; step_domains; _ } as t : _ Compiled.t) =
    let%map.Promise wrap_key = Lazy.force wrap_key
    and step_domains =
      let%map.Promise () =
        (* Wait for promises to resolve. *)
        Vector.fold ~init:(Promise.return ()) step_domains
          ~f:(fun acc step_domain ->
            let%bind.Promise _ = step_domain in
            acc )
      in
      Vector.map ~f:(fun x -> Option.value_exn @@ Promise.peek x) step_domains
    in
    of_compiled_with_known_wrap_key { wrap_key; step_domains } t
end

type t =
  { compiled : Compiled.packed Type_equal.Id.Uid.Table.t
  ; side_loaded : Side_loaded.packed Type_equal.Id.Uid.Table.t
  }

let univ : t =
  { compiled = Type_equal.Id.Uid.Table.create ()
  ; side_loaded = Type_equal.Id.Uid.Table.create ()
  }

let find t k =
  match Hashtbl.find t k with None -> failwith "key not found" | Some x -> x

let lookup_compiled :
    type var value n m.
    (var, value, n, m) Tag.id -> (var, value, n, m) Compiled.t =
 fun t ->
  let (T (other_id, d)) = find univ.compiled (Type_equal.Id.uid t) in
  let T = Type_equal.Id.same_witness_exn t other_id in
  d

let lookup_side_loaded :
    type var value n m.
    (var, value, n, m) Tag.id -> (var, value, n, m) Side_loaded.t =
 fun t ->
  let (T (other_id, d)) = find univ.side_loaded (Type_equal.Id.uid t) in
  let T = Type_equal.Id.same_witness_exn t other_id in
  d

let lookup_basic :
    type var value n m.
    (var, value, n, m) Tag.t -> (var, value, n, m) Basic.t Promise.t =
 fun t ->
  match t.kind with
  | Compiled ->
      Compiled.to_basic (lookup_compiled t.id)
  | Side_loaded ->
      Promise.return @@ Side_loaded.to_basic (lookup_side_loaded t.id)

let max_proofs_verified :
    type n1. (_, _, n1, _) Tag.t -> (module Nat.Add.Intf with type n = n1) =
 fun tag ->
  match tag.kind with
  | Compiled ->
      (lookup_compiled tag.id).max_proofs_verified
  | Side_loaded ->
      (lookup_side_loaded tag.id).permanent.max_proofs_verified

let public_input :
    type var value. (var, value, _, _) Tag.t -> (var, value) Impls.Step.Typ.t =
 fun tag ->
  match tag.kind with
  | Compiled ->
      (lookup_compiled tag.id).public_input
  | Side_loaded ->
      (lookup_side_loaded tag.id).permanent.public_input

let feature_flags :
    type var value.
    (var, value, _, _) Tag.t -> Opt.Flag.t Plonk_types.Features.Full.t =
 fun tag ->
  match tag.kind with
  | Compiled ->
      (lookup_compiled tag.id).feature_flags
  | Side_loaded ->
      (lookup_side_loaded tag.id).permanent.feature_flags

let num_chunks : type var value. (var, value, _, _) Tag.t -> int =
 fun tag ->
  match tag.kind with
  | Compiled ->
      (lookup_compiled tag.id).num_chunks
  | Side_loaded ->
      (lookup_side_loaded tag.id).permanent.num_chunks

let _value_to_field_elements :
    type a. (_, a, _, _) Tag.t -> a -> Backend.Tick.Field.t array =
 fun t ->
  let (Typ typ) = public_input t in
  fun x -> fst (typ.value_to_fields x)

let _lookup_map (type var value c d) (t : (var, value, c, d) Tag.t) ~self
    ~default
    ~(f :
          [ `Compiled of (var, value, c, d) Compiled.t
          | `Side_loaded of (var, value, c, d) Side_loaded.t ]
       -> _ ) =
  match Type_equal.Id.same_witness t.id self with
  | Some _ ->
      default
  | None -> (
      match t.kind with
      | Compiled ->
          let (T (other_id, d)) = find univ.compiled (Type_equal.Id.uid t.id) in
          let T = Type_equal.Id.same_witness_exn t.id other_id in
          f (`Compiled d)
      | Side_loaded ->
          let (T (other_id, d)) =
            find univ.side_loaded (Type_equal.Id.uid t.id)
          in
          let T = Type_equal.Id.same_witness_exn t.id other_id in
          f (`Side_loaded d) )

let add_side_loaded ~name permanent =
  let (Tag.{ id; _ } as tag) = Tag.(create ~kind:Side_loaded name) in
  Hashtbl.add_exn univ.side_loaded ~key:(Type_equal.Id.uid id)
    ~data:(T (id, { ephemeral = None; permanent })) ;
  tag

let set_ephemeral { Tag.kind; id } (eph : Side_loaded.Ephemeral.t) =
  assert (match kind with Side_loaded -> true | Compiled -> false) ;
  Hashtbl.update univ.side_loaded (Type_equal.Id.uid id) ~f:(function
    | None ->
        assert false
    | Some (T (id, d)) ->
        let ephemeral =
          match (d.ephemeral, eph.index) with
          | None, _ | Some _, `In_prover _ ->
              (* Giving prover only always resets. *)
              Some eph
          | Some { index = `In_prover prover }, `In_circuit circuit
          | Some { index = `In_both (prover, _) }, `In_circuit circuit ->
              (* In-circuit extends prover if one was given. *)
              Some { index = `In_both (prover, circuit) }
          | _ ->
              (* Otherwise, just use the given value. *)
              Some eph
        in
        T (id, { d with ephemeral }) )

let add_exn (type var value c d) (tag : (var, value, c, d) Tag.t)
    (data : (var, value, c, d) Compiled.t) =
  Hashtbl.add_exn univ.compiled ~key:(Type_equal.Id.uid tag.id)
    ~data:(Compiled.T (tag.id, data))

1	open Core_kernel	35✔
2	open Pickles_types
3	open Import
4	open Backend
5
6	(* We maintain a global hash table which stores for each inductive proof system some
7	data.
8	*)
9	type inner_curve_var = Impls.Step.Field.t * Impls.Step.Field.t
10
11	module Basic = struct
12	type ('var, 'value, 'n1, 'n2) t =
13	{ max_proofs_verified : (module Nat.Add.Intf with type n = 'n1)
14	; public_input : ('var, 'value) Impls.Step.Typ.t
15	; branches : 'n2 Nat.t
16	; wrap_domains : Domains.t
17	; wrap_key : Tick.Inner_curve.Affine.t array Plonk_verification_key_evals.t
18	; wrap_vk : Impls.Wrap.Verification_key.t
19	; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t
20	; num_chunks : int
21	; zk_rows : int
22	}
23	end
24
25	module Side_loaded = struct
26	module Ephemeral = struct
27	type t =
28	{ index :
29	[ `In_circuit of Side_loaded_verification_key.Checked.t
30	\| `In_prover of Side_loaded_verification_key.t
31	\| `In_both of
32	Side_loaded_verification_key.t
33	* Side_loaded_verification_key.Checked.t ]
34	}
35	end
36
37	module Permanent = struct
38	type ('var, 'value, 'n1, 'n2) t =
39	{ max_proofs_verified : (module Nat.Add.Intf with type n = 'n1)
40	; public_input : ('var, 'value) Impls.Step.Typ.t
41	; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t
42	; branches : 'n2 Nat.t
43	; num_chunks : int
44	; zk_rows : int
45	}
46	end
47
48	type ('var, 'value, 'n1, 'n2) t =
49	{ ephemeral : Ephemeral.t option
50	; permanent : ('var, 'value, 'n1, 'n2) Permanent.t
51	}
52
53	type packed =
54	\| T : ('var, 'value, 'n1, 'n2) Tag.id * ('var, 'value, 'n1, 'n2) t -> packed
55
56	let to_basic
57	{ permanent =
58	{ max_proofs_verified
59	; public_input
60	; branches
61	; feature_flags
62	; num_chunks
63	; zk_rows
64	}
65	; ephemeral
66	} =
67	let wrap_key, wrap_vk =	×
68	match ephemeral with
69	\| Some { index = `In_prover i \| `In_both (i, _) } ->	×
70	let wrap_index =
71	Plonk_verification_key_evals.map i.wrap_index ~f:(fun x -> [\| x \|])	×
72	in
73	(wrap_index, i.wrap_vk)	×
74	\| _ ->	×
75	failwithf "Side_loaded.to_basic: Expected `In_prover (%s)" __LOC__ ()	×
76	in
77	let proofs_verified = Nat.to_int (Nat.Add.n max_proofs_verified) in	×
78	let wrap_vk = Option.value_exn ~here:[%here] wrap_vk in	×
79	{ Basic.max_proofs_verified	×
80	; wrap_vk
81	; public_input
82	; branches
83	; wrap_domains = Common.wrap_domains ~proofs_verified
84	; wrap_key
85	; feature_flags
86	; num_chunks
87	; zk_rows
88	}
89	end
90
91	module Compiled = struct
92	type ('a_var, 'a_value, 'max_proofs_verified, 'branches) basic =
93	{ public_input : ('a_var, 'a_value) Impls.Step.Typ.t
94	; proofs_verifieds : (int, 'branches) Vector.t
95	(* For each branch in this rule, how many predecessor proofs does it have? *)
96	; wrap_domains : Domains.t
97	; step_domains : (Domains.t, 'branches) Vector.t
98	; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t
99	; num_chunks : int
100	; zk_rows : int
101	}
102
103	(* This is the data associated to an inductive proof system with statement type
104	['a_var], which has ['branches] many "variants" each of which depends on at most
105	['max_proofs_verified] many previous statements. *)
106	type ('a_var, 'a_value, 'max_proofs_verified, 'branches) t =
107	{ branches : 'branches Nat.t
108	; max_proofs_verified :
109	(module Nat.Add.Intf with type n = 'max_proofs_verified)
110	; proofs_verifieds : (int, 'branches) Vector.t
111	(* For each branch in this rule, how many predecessor proofs does it have? *)
112	; public_input : ('a_var, 'a_value) Impls.Step.Typ.t
113	; wrap_key :
114	Tick.Inner_curve.Affine.t array Plonk_verification_key_evals.t Promise.t
115	Lazy.t
116	; wrap_vk : Impls.Wrap.Verification_key.t Promise.t Lazy.t
117	; wrap_domains : Domains.t
118	; step_domains : (Domains.t Promise.t, 'branches) Vector.t
119	; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t
120	; num_chunks : int
121	; zk_rows : int
122	}
123
124	type packed =
125	\| T : ('var, 'value, 'n1, 'n2) Tag.id * ('var, 'value, 'n1, 'n2) t -> packed
126
127	let to_basic
128	{ branches = _
129	; max_proofs_verified
130	; proofs_verifieds = _
131	; public_input
132	; wrap_vk
133	; wrap_domains
134	; step_domains
135	; wrap_key
136	; feature_flags
137	; num_chunks
138	; zk_rows
139	} =
140	let%bind.Promise wrap_key = Lazy.force wrap_key in	×
141	let%map.Promise wrap_vk = Lazy.force wrap_vk in	×
142	{ Basic.max_proofs_verified	×
143	; wrap_domains
144	; public_input
145	; branches = Vector.length step_domains	×
146	; wrap_key
147	; wrap_vk
148	; feature_flags
149	; num_chunks
150	; zk_rows
151	}
152	end
153
154	module For_step = struct
155	type ('a_var, 'a_value, 'max_proofs_verified, 'branches) t =
156	{ branches : 'branches Nat.t
157	; max_proofs_verified :
158	(module Nat.Add.Intf with type n = 'max_proofs_verified)
159	; proofs_verifieds :
160	[ `Known of (Impls.Step.Field.t, 'branches) Vector.t \| `Side_loaded ]
161	; public_input : ('a_var, 'a_value) Impls.Step.Typ.t
162	; wrap_key : inner_curve_var array Plonk_verification_key_evals.t
163	; wrap_domain :
164	[ `Known of Domain.t
165	\| `Side_loaded of Pickles_base.Proofs_verified.One_hot.Checked.t ]
166	; step_domains : [ `Known of (Domains.t, 'branches) Vector.t \| `Side_loaded ]
167	; feature_flags : Opt.Flag.t Plonk_types.Features.Full.t
168	; num_chunks : int
169	; zk_rows : int
170	}
171
172	let of_side_loaded (type a b c d)
173	({ ephemeral
174	; permanent =
175	{ branches
176	; max_proofs_verified
177	; public_input
178	; feature_flags
179	; num_chunks
180	; zk_rows
181	}
182	} :
183	(a, b, c, d) Side_loaded.t ) : (a, b, c, d) t =
184	let index =	8✔
185	match ephemeral with
186	\| Some { index = `In_circuit i \| `In_both (_, i) } ->	×
187	i
188	\| _ ->	×
189	failwithf "For_step.side_loaded: Expected `In_circuit (%s)" __LOC__ ()	×
190	in
191	let T = Nat.eq_exn branches Side_loaded_verification_key.Max_branches.n in
192	let wrap_key =	8✔
193	Plonk_verification_key_evals.map index.wrap_index ~f:(fun x -> [\| x \|])	224✔
194	in
195	{ branches	8✔
196	; max_proofs_verified
197	; public_input
198	; proofs_verifieds = `Side_loaded
199	; wrap_key
200	; wrap_domain = `Side_loaded index.actual_wrap_domain_size
201	; step_domains = `Side_loaded
202	; feature_flags
203	; num_chunks
204	; zk_rows
205	}
206
207	module Optional_wrap_key = struct
208	type 'branches known =
209	{ wrap_key :
210	Tick.Inner_curve.Affine.t array Plonk_verification_key_evals.t
211	; step_domains : (Domains.t, 'branches) Vector.t
212	}
213
214	type 'branches t = 'branches known option
215	end
216
217	let of_compiled_with_known_wrap_key
218	({ wrap_key; step_domains } : _ Optional_wrap_key.known)
219	({ branches
220	; max_proofs_verified
221	; proofs_verifieds
222	; public_input
223	; wrap_key = _
224	; wrap_domains
225	; step_domains = _
226	; feature_flags
227	; wrap_vk = _
228	; num_chunks
229	; zk_rows
230	} :
231	_ Compiled.t ) =
232	{ branches	8✔
233	; max_proofs_verified
234	; proofs_verifieds =
235	`Known (Vector.map proofs_verifieds ~f:Impls.Step.Field.of_int)	8✔
236	; public_input
237	; wrap_key =
238	Plonk_verification_key_evals.map wrap_key	8✔
239	~f:(Array.map ~f:Step_main_inputs.Inner_curve.constant)
240	; wrap_domain = `Known wrap_domains.h
241	; step_domains = `Known step_domains
242	; feature_flags
243	; num_chunks
244	; zk_rows
245	}
246
247	let of_compiled ({ wrap_key; step_domains; _ } as t : _ Compiled.t) =
248	let%map.Promise wrap_key = Lazy.force wrap_key	×
249	and step_domains =
250	let%map.Promise () =
251	(* Wait for promises to resolve. *)
252	Vector.fold ~init:(Promise.return ()) step_domains	×
253	~f:(fun acc step_domain ->
254	let%bind.Promise _ = step_domain in
255	acc )	×
256	in
257	Vector.map ~f:(fun x -> Option.value_exn @@ Promise.peek x) step_domains	×
258	in
259	of_compiled_with_known_wrap_key { wrap_key; step_domains } t	×
260	end
261
262	type t =
263	{ compiled : Compiled.packed Type_equal.Id.Uid.Table.t
264	; side_loaded : Side_loaded.packed Type_equal.Id.Uid.Table.t
265	}
266
267	let univ : t =
268	{ compiled = Type_equal.Id.Uid.Table.create ()	35✔
269	; side_loaded = Type_equal.Id.Uid.Table.create ()	35✔
270	}
271
272	let find t k =
273	match Hashtbl.find t k with None -> failwith "key not found" \| Some x -> x	×
274
275	let lookup_compiled :
276	type var value n m.
277	(var, value, n, m) Tag.id -> (var, value, n, m) Compiled.t =
278	fun t ->
279	let (T (other_id, d)) = find univ.compiled (Type_equal.Id.uid t) in	36✔
280	let T = Type_equal.Id.same_witness_exn t other_id in	36✔
281	d	36✔
282
283	let lookup_side_loaded :
284	type var value n m.
285	(var, value, n, m) Tag.id -> (var, value, n, m) Side_loaded.t =
286	fun t ->
287	let (T (other_id, d)) = find univ.side_loaded (Type_equal.Id.uid t) in	32✔
288	let T = Type_equal.Id.same_witness_exn t other_id in	32✔
289	d	32✔
290
291	let lookup_basic :
292	type var value n m.
293	(var, value, n, m) Tag.t -> (var, value, n, m) Basic.t Promise.t =
294	fun t ->
295	match t.kind with	×
296	\| Compiled ->	×
297	Compiled.to_basic (lookup_compiled t.id)	×
298	\| Side_loaded ->	×
299	Promise.return @@ Side_loaded.to_basic (lookup_side_loaded t.id)	×
300
301	let max_proofs_verified :
302	type n1. (_, _, n1, _) Tag.t -> (module Nat.Add.Intf with type n = n1) =
303	fun tag ->
304	match tag.kind with	8✔
305	\| Compiled ->	4✔
306	(lookup_compiled tag.id).max_proofs_verified	4✔
307	\| Side_loaded ->	4✔
308	(lookup_side_loaded tag.id).permanent.max_proofs_verified	4✔
309
310	let public_input :
311	type var value. (var, value, _, _) Tag.t -> (var, value) Impls.Step.Typ.t =
312	fun tag ->
313	match tag.kind with	×
314	\| Compiled ->	×
315	(lookup_compiled tag.id).public_input	×
316	\| Side_loaded ->	×
317	(lookup_side_loaded tag.id).permanent.public_input	×
318
319	let feature_flags :
320	type var value.
321	(var, value, _, _) Tag.t -> Opt.Flag.t Plonk_types.Features.Full.t =
322	fun tag ->
323	match tag.kind with	16✔
324	\| Compiled ->	8✔
325	(lookup_compiled tag.id).feature_flags	8✔
326	\| Side_loaded ->	8✔
327	(lookup_side_loaded tag.id).permanent.feature_flags	8✔
328
329	let num_chunks : type var value. (var, value, _, _) Tag.t -> int =
330	fun tag ->
331	match tag.kind with	16✔
332	\| Compiled ->	8✔
333	(lookup_compiled tag.id).num_chunks	8✔
334	\| Side_loaded ->	8✔
335	(lookup_side_loaded tag.id).permanent.num_chunks	8✔
336
337	let _value_to_field_elements :
338	type a. (_, a, _, _) Tag.t -> a -> Backend.Tick.Field.t array =
339	fun t ->
340	let (Typ typ) = public_input t in	×
341	fun x -> fst (typ.value_to_fields x)	×
342
343	let _lookup_map (type var value c d) (t : (var, value, c, d) Tag.t) ~self
344	~default
345	~(f :
346	[ `Compiled of (var, value, c, d) Compiled.t
347	\| `Side_loaded of (var, value, c, d) Side_loaded.t ]
348	-> _ ) =
349	match Type_equal.Id.same_witness t.id self with	×
350	\| Some _ ->	×
351	default
352	\| None -> (	×
353	match t.kind with
354	\| Compiled ->	×
355	let (T (other_id, d)) = find univ.compiled (Type_equal.Id.uid t.id) in	×
356	let T = Type_equal.Id.same_witness_exn t.id other_id in	×
357	f (`Compiled d)	×
358	\| Side_loaded ->	×
359	let (T (other_id, d)) =
360	find univ.side_loaded (Type_equal.Id.uid t.id)	×
361	in
362	let T = Type_equal.Id.same_witness_exn t.id other_id in	×
363	f (`Side_loaded d) )	×
364
365	let add_side_loaded ~name permanent =
366	let (Tag.{ id; _ } as tag) = Tag.(create ~kind:Side_loaded name) in	4✔
367	Hashtbl.add_exn univ.side_loaded ~key:(Type_equal.Id.uid id)	4✔
368	~data:(T (id, { ephemeral = None; permanent })) ;
369	tag	4✔
370
371	let set_ephemeral { Tag.kind; id } (eph : Side_loaded.Ephemeral.t) =
372	assert (match kind with Side_loaded -> true \| Compiled -> false) ;	×
373	Hashtbl.update univ.side_loaded (Type_equal.Id.uid id) ~f:(function	8✔
374	\| None ->
375	assert false
376	\| Some (T (id, d)) ->	8✔
377	let ephemeral =
378	match (d.ephemeral, eph.index) with
379	\| None, _ \| Some _, `In_prover _ ->	×
380	(* Giving prover only always resets. *)
381	Some eph
382	\| Some { index = `In_prover prover }, `In_circuit circuit	×
383	\| Some { index = `In_both (prover, _) }, `In_circuit circuit ->	×
384	(* In-circuit extends prover if one was given. *)
385	Some { index = `In_both (prover, circuit) }
386	\| _ ->	4✔
387	(* Otherwise, just use the given value. *)
388	Some eph
389	in
390	T (id, { d with ephemeral }) )
391
392	let add_exn (type var value c d) (tag : (var, value, c, d) Tag.t)
393	(data : (var, value, c, d) Compiled.t) =
394	Hashtbl.add_exn univ.compiled ~key:(Type_equal.Id.uid tag.id)	8✔
395	~data:(Compiled.T (tag.id, data))	70✔

MinaProtocol / mina / 3409

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous