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

90.91

/src/lib/snarky_group_map/checked_map.ml

open Core_kernel

module Aux (Impl : Snarky_backendless.Snark_intf.Run) = struct
  open Impl

  let non_residue : Field.Constant.t Lazy.t =
    let open Field.Constant in
    let rec go i = if not (is_square i) then i else go (i + one) in
    lazy (go (of_int 2))

  let sqrt_exn x =
    let y =
      exists Field.typ ~compute:(fun () ->
          Field.Constant.sqrt (As_prover.read_var x) )
    in
    assert_square y x ; y

  (* let sqrt_flagged : Field.t -> Field.t * Boolean.var = *)
  let sqrt_flagged x =
    (*
       imeckler: I learned this trick from Dan Boneh

       m a known non residue

       exists is_square : bool, y.
       if is_square then assert y*y = x else assert y*y = m * x

       <=>

       assert (y*y = if is_square then x else m * x)
    *)
    let is_square =
      exists Boolean.typ ~compute:(fun () ->
          Field.Constant.is_square (As_prover.read_var x) )
    in
    let m = Lazy.force non_residue in
    (sqrt_exn (Field.if_ is_square ~then_:x ~else_:(Field.scale x m)), is_square)
end

let wrap (type f v)
    (module Impl : Snarky_backendless.Snark_intf.Run
      with type field = f
       and type field_var = v ) ~potential_xs ~y_squared =
  let open Impl in
  let module A = Aux (Impl) in
  let open A in
  stage (fun x ->
      let x1, x2, x3 = potential_xs x in
      let y1, b1 = sqrt_flagged (y_squared ~x:x1)
      and y2, b2 = sqrt_flagged (y_squared ~x:x2)
      and y3, b3 = sqrt_flagged (y_squared ~x:x3) in
      Boolean.Assert.any [ b1; b2; b3 ] ;
      let x1_is_first = (b1 :> Field.t)
      and x2_is_first = (Boolean.((not b1) && b2) :> Field.t)
      and x3_is_first = (Boolean.((not b1) && (not b2) && b3) :> Field.t) in
      ( Field.((x1_is_first * x1) + (x2_is_first * x2) + (x3_is_first * x3))
      , Field.((x1_is_first * y1) + (x2_is_first * y2) + (x3_is_first * y3)) ) )

module Make
    (M : Snarky_backendless.Snark_intf.Run) (P : sig
      val params : M.field Group_map.Params.t
    end) =
struct
  open P
  include Group_map.Make (M.Field.Constant) (M.Field) (P)
  open M

  let to_group =
    let { Group_map.Spec.a; b } = Group_map.Params.spec params in
    unstage
      (wrap
         (module M)
         ~potential_xs
         ~y_squared:Field.(fun ~x -> (x * x * x) + scale x a + constant b) )
end

1	open Core_kernel	35✔
2
3	module Aux (Impl : Snarky_backendless.Snark_intf.Run) = struct
4	open Impl
5
6	let non_residue : Field.Constant.t Lazy.t =
7	let open Field.Constant in
8	let rec go i = if not (is_square i) then i else go (i + one) in	16✔
9	lazy (go (of_int 2))	16✔
10
11	let sqrt_exn x =
12	let y =	168✔
13	exists Field.typ ~compute:(fun () ->
14	Field.Constant.sqrt (As_prover.read_var x) )	×
15	in
16	assert_square y x ; y	168✔
17
18	(* let sqrt_flagged : Field.t -> Field.t * Boolean.var = *)
19	let sqrt_flagged x =
20	(*
21	imeckler: I learned this trick from Dan Boneh
22
23	m a known non residue
24
25	exists is_square : bool, y.
26	if is_square then assert yy = x else assert yy = m * x
27
28	<=>
29
30	assert (yy = if is_square then x else m x)
31	*)
32	let is_square =	168✔
33	exists Boolean.typ ~compute:(fun () ->
34	Field.Constant.is_square (As_prover.read_var x) )	×
35	in
36	let m = Lazy.force non_residue in	168✔
37	(sqrt_exn (Field.if_ is_square ~then_:x ~else_:(Field.scale x m)), is_square)	168✔
38	end
39
40	let wrap (type f v)
41	(module Impl : Snarky_backendless.Snark_intf.Run
42	with type field = f
43	and type field_var = v ) ~potential_xs ~y_squared =
44	let open Impl in	16✔
45	let module A = Aux (Impl) in
46	let open A in
47	stage (fun x ->
48	let x1, x2, x3 = potential_xs x in	56✔
49	let y1, b1 = sqrt_flagged (y_squared ~x:x1)	56✔
50	and y2, b2 = sqrt_flagged (y_squared ~x:x2)	56✔
51	and y3, b3 = sqrt_flagged (y_squared ~x:x3) in	56✔
52	Boolean.Assert.any [ b1; b2; b3 ] ;
53	let x1_is_first = (b1 :> Field.t)	56✔
54	and x2_is_first = (Boolean.((not b1) && b2) :> Field.t)	56✔
55	and x3_is_first = (Boolean.((not b1) && (not b2) && b3) :> Field.t) in	56✔
56	( Field.((x1_is_first * x1) + (x2_is_first * x2) + (x3_is_first * x3))
57	, Field.((x1_is_first * y1) + (x2_is_first * y2) + (x3_is_first * y3)) ) )
58
59	module Make
60	(M : Snarky_backendless.Snark_intf.Run) (P : sig
61	val params : M.field Group_map.Params.t
62	end) =
63	struct
64	open P
65	include Group_map.Make (M.Field.Constant) (M.Field) (P)
66	open M
67
68	let to_group =
69	let { Group_map.Spec.a; b } = Group_map.Params.spec params in
70	unstage	8✔
71	(wrap	8✔
72	(module M)
73	~potential_xs
74	~y_squared:Field.(fun ~x -> (x * x * x) + scale x a + constant b) )	24✔
75	end	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