diff --git a/priv/stdlib/BLS12_381.aes b/priv/stdlib/BLS12_381.aes new file mode 100644 index 0000000..4bc27ff --- /dev/null +++ b/priv/stdlib/BLS12_381.aes @@ -0,0 +1,68 @@ +namespace BLS12_381 = + type fr = MCL_BLS12_381.fr + type fp = MCL_BLS12_381.fp + record fp2 = { x1 : fp, x2 : fp } + record g1 = { x : fp, y : fp, z : fp } + record g2 = { x : fp2, y : fp2, z : fp2 } + record gt = { x1 : fp, x2 : fp, x3 : fp, x4 : fp, x5 : fp, x6 : fp, + x7 : fp, x8 : fp, x9 : fp, x10 : fp, x11 : fp, x12 : fp } + + function pairing_check(xs : list(g1), ys : list(g2)) = + switch((xs, ys)) + ([], []) => true + (x :: xs, y :: ys) => pairing_check_(pairing(x, y), xs, ys) + + function pairing_check_(acc : gt, xs : list(g1), ys : list(g2)) = + switch((xs, ys)) + ([], []) => gt_is_one(acc) + (x :: xs, y :: ys) => + pairing_check_(gt_mul(acc, pairing(x, y)), xs, ys) + + function int_to_fr(x : int) = MCL_BLS12_381.int_to_fr(x) + function int_to_fp(x : int) = MCL_BLS12_381.int_to_fp(x) + function fr_to_int(x : fr) = MCL_BLS12_381.fr_to_int(x) + function fp_to_int(x : fp) = MCL_BLS12_381.fp_to_int(x) + + function mk_g1(x : int, y : int, z : int) : g1 = + { x = int_to_fp(x), y = int_to_fp(y), z = int_to_fp(z) } + + function mk_g2(x1 : int, x2 : int, y1 : int, y2 : int, z1 : int, z2 : int) : g2 = + { x = {x1 = int_to_fp(x1), x2 = int_to_fp(x2)}, + y = {x1 = int_to_fp(y1), x2 = int_to_fp(y2)}, + z = {x1 = int_to_fp(z1), x2 = int_to_fp(z2)} } + + function pack_g1(t) = switch(t) + (x, y, z) => {x = x, y = y, z = z} : g1 + function pack_g2(t) = switch(t) + ((x1, x2), (y1, y2), (z1, z2)) => + {x = {x1 = x1, x2 = x2}, y = {x1 = y1, x2 = y2}, z = {x1 = z1, x2 = z2}} : g2 + function pack_gt(t) = switch(t) + (x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) => + {x1 = x1, x2 = x2, x3 = x3, x4 = x4, x5 = x5, x6 = x6, + x7 = x7, x8 = x8, x9 = x9, x10 = x10, x11 = x11, x12 = x12} : gt + + function g1_neg(p : g1) = pack_g1(MCL_BLS12_381.g1_neg((p.x, p.y, p.z))) + function g1_norm(p : g1) = pack_g1(MCL_BLS12_381.g1_norm((p.x, p.y, p.z))) + function g1_valid(p : g1) = MCL_BLS12_381.g1_valid((p.x, p.y, p.z)) + function g1_is_zero(p : g1) = MCL_BLS12_381.g1_is_zero((p.x, p.y, p.z)) + function g1_add(p : g1, q : g1) = pack_g1(MCL_BLS12_381.g1_add((p.x, p.y, p.z), (q.x, q.y, q.z))) + function g1_mul(k : fr, p : g1) = pack_g1(MCL_BLS12_381.g1_mul(k, (p.x, p.y, p.z))) + + function g2_neg(p : g2) = pack_g2(MCL_BLS12_381.g2_neg(((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2)))) + function g2_norm(p : g2) = pack_g2(MCL_BLS12_381.g2_norm(((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2)))) + function g2_valid(p : g2) = MCL_BLS12_381.g2_valid(((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2))) + function g2_is_zero(p : g2) = MCL_BLS12_381.g2_is_zero(((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2))) + function g2_add(p : g2, q : g2) = pack_g2(MCL_BLS12_381.g2_add(((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2)), + ((q.x.x1, q.x.x2), (q.y.x1, q.y.x2), (q.z.x1, q.z.x2)))) + function g2_mul(k : fr, p : g2) = pack_g2(MCL_BLS12_381.g2_mul(k, ((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2)))) + + function gt_inv(p : gt) = pack_gt(MCL_BLS12_381.gt_inv((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12))) + function gt_add(p : gt, q : gt) = pack_gt(MCL_BLS12_381.gt_add((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12), + (q.x1, q.x2, q.x3, q.x4, q.x5, q.x6, q.x7, q.x8, q.x9, q.x10, q.x11, q.x12))) + function gt_mul(p : gt, q : gt) = pack_gt(MCL_BLS12_381.gt_mul((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12), + (q.x1, q.x2, q.x3, q.x4, q.x5, q.x6, q.x7, q.x8, q.x9, q.x10, q.x11, q.x12))) + function gt_pow(p : gt, k : fr) = pack_gt(MCL_BLS12_381.gt_pow((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12), k)) + function gt_is_one(p : gt) = MCL_BLS12_381.gt_is_one((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12)) + function pairing(p : g1, q : g2) = pack_gt(MCL_BLS12_381.pairing((p.x, p.y, p.z), ((q.x.x1, q.x.x2), (q.y.x1, q.y.x2), (q.z.x1, q.z.x2)))) + function miller_loop(p : g1, q : g2) = pack_gt(MCL_BLS12_381.miller_loop((p.x, p.y, p.z), ((q.x.x1, q.x.x2), (q.y.x1, q.y.x2), (q.z.x1, q.z.x2)))) + function final_exp(p : gt) = pack_gt(MCL_BLS12_381.final_exp((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12))) diff --git a/rebar.config b/rebar.config index 5360196..aa6dcc1 100644 --- a/rebar.config +++ b/rebar.config @@ -2,7 +2,7 @@ {erl_opts, [debug_info]}. -{deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {ref,"b040dcc"}}} +{deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {ref,"e4b09d7"}}} , {getopt, "1.0.1"} , {eblake2, "1.0.0"} , {jsx, {git, "https://github.com/talentdeficit/jsx.git", diff --git a/rebar.lock b/rebar.lock index 0e0b07b..0395056 100644 --- a/rebar.lock +++ b/rebar.lock @@ -1,7 +1,7 @@ {"1.1.0", [{<<"aebytecode">>, {git,"https://github.com/aeternity/aebytecode.git", - {ref,"b040dccdefb0713198986264bc2d19d3fb84398d"}}, + {ref,"e4b09d7c5c85030636b3b88df7dd9f89f3d1e2cb"}}, 0}, {<<"aeserialization">>, {git,"https://github.com/aeternity/aeserialization.git", diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index e585ac5..d290f25 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -390,6 +390,12 @@ global_env() -> SignFun = fun(Ts, T) -> {type_sig, [stateful|Ann], none, [Signature], Ts, T} end, TTL = {qid, Ann, ["Chain", "ttl"]}, Pointee = {qid, Ann, ["AENS", "pointee"]}, + Fr = {qid, Ann, ["MCL_BLS12_381", "fr"]}, + Fp = {qid, Ann, ["MCL_BLS12_381", "fp"]}, + Fp2 = {tuple_t, Ann, [Fp, Fp]}, + G1 = {tuple_t, Ann, [Fp, Fp, Fp]}, + G2 = {tuple_t, Ann, [Fp2, Fp2, Fp2]}, + GT = {tuple_t, Ann, lists:duplicate(12, Fp)}, Fee = Int, [A, Q, R, K, V] = lists:map(TVar, ["a", "q", "r", "k", "v"]), @@ -493,6 +499,40 @@ global_env() -> {"sha256", Fun1(A, Hash)}, {"blake2b", Fun1(A, Hash)}]) }, + %% Fancy BLS12-381 crypto operations + MCL_BLS12_381_Scope = #scope + { funs = MkDefs( + [{"g1_neg", Fun1(G1, G1)}, + {"g1_norm", Fun1(G1, G1)}, + {"g1_valid", Fun1(G1, Bool)}, + {"g1_is_zero", Fun1(G1, Bool)}, + {"g1_add", Fun ([G1, G1], G1)}, + {"g1_mul", Fun ([Fr, G1], G1)}, + + {"g2_neg", Fun1(G2, G2)}, + {"g2_norm", Fun1(G2, G2)}, + {"g2_valid", Fun1(G2, Bool)}, + {"g2_is_zero", Fun1(G2, Bool)}, + {"g2_add", Fun ([G2, G2], G2)}, + {"g2_mul", Fun ([Fr, G2], G2)}, + + {"gt_inv", Fun1(GT, GT)}, + {"gt_add", Fun ([GT, GT], GT)}, + {"gt_mul", Fun ([GT, GT], GT)}, + {"gt_pow", Fun ([GT, Fr], GT)}, + {"gt_is_one", Fun1(GT, Bool)}, + {"pairing", Fun ([G1, G2], GT)}, + {"miller_loop", Fun ([G1, G2], GT)}, + {"final_exp", Fun1(GT, GT)}, + + {"int_to_fr", Fun1(Int, Fr)}, + {"int_to_fp", Fun1(Int, Fp)}, + {"fr_to_int", Fun1(Fr, Int)}, + {"fp_to_int", Fun1(Fp, Int)} + ]), + types = MkDefs( + [{"fr", 0}, {"fp", 0}]) }, + %% Authentication AuthScope = #scope { funs = MkDefs( @@ -547,12 +587,15 @@ global_env() -> , ["Map"] => MapScope , ["Auth"] => AuthScope , ["Crypto"] => CryptoScope + , ["MCL_BLS12_381"] => MCL_BLS12_381_Scope , ["String"] => StringScope , ["Bits"] => BitsScope , ["Bytes"] => BytesScope , ["Int"] => IntScope , ["Address"] => AddressScope - } }. + } + }. + option_t(As, T) -> {app_t, As, {id, As, "option"}, [T]}. map_t(As, K, V) -> {app_t, As, {id, As, "map"}, [K, V]}. diff --git a/src/aeso_ast_to_fcode.erl b/src/aeso_ast_to_fcode.erl index 6fa163a..9b28e78 100644 --- a/src/aeso_ast_to_fcode.erl +++ b/src/aeso_ast_to_fcode.erl @@ -34,7 +34,14 @@ bits_intersection | bits_union | bits_difference | contract_to_address | address_to_contract | crypto_verify_sig | crypto_verify_sig_secp256k1 | crypto_sha3 | crypto_sha256 | crypto_blake2b | - crypto_ecverify_secp256k1 | crypto_ecrecover_secp256k1. + crypto_ecverify_secp256k1 | crypto_ecrecover_secp256k1 | + mcl_bls12_381_g1_neg | mcl_bls12_381_g1_norm | mcl_bls12_381_g1_valid | + mcl_bls12_381_g1_is_zero | mcl_bls12_381_g1_add | mcl_bls12_381_g1_mul | + mcl_bls12_381_g2_neg | mcl_bls12_381_g2_norm | mcl_bls12_381_g2_valid | + mcl_bls12_381_g2_is_zero | mcl_bls12_381_g2_add | mcl_bls12_381_g2_mul | + mcl_bls12_381_gt_inv | mcl_bls12_381_gt_add | mcl_bls12_381_gt_mul | mcl_bls12_381_gt_pow | + mcl_bls12_381_gt_is_one | mcl_bls12_381_pairing | mcl_bls12_381_miller_loop | mcl_bls12_381_final_exp | + mcl_bls12_381_int_to_fr | mcl_bls12_381_int_to_fp | mcl_bls12_381_fr_to_int | mcl_bls12_381_fp_to_int. -type flit() :: {int, integer()} | {string, binary()} @@ -197,6 +204,11 @@ builtins() -> {["Crypto"], [{"verify_sig", 3}, {"verify_sig_secp256k1", 3}, {"ecverify_secp256k1", 3}, {"ecrecover_secp256k1", 2}, {"sha3", 1}, {"sha256", 1}, {"blake2b", 1}]}, + {["MCL_BLS12_381"], [{"g1_neg", 1}, {"g1_norm", 1}, {"g1_valid", 1}, {"g1_is_zero", 1}, {"g1_add", 2}, {"g1_mul", 2}, + {"g2_neg", 1}, {"g2_norm", 1}, {"g2_valid", 1}, {"g2_is_zero", 1}, {"g2_add", 2}, {"g2_mul", 2}, + {"gt_inv", 1}, {"gt_add", 2}, {"gt_mul", 2}, {"gt_pow", 2}, {"gt_is_one", 1}, + {"pairing", 2}, {"miller_loop", 2}, {"final_exp", 1}, + {"int_to_fr", 1}, {"int_to_fp", 1}, {"fr_to_int", 1}, {"fp_to_int", 1}]}, {["Auth"], [{"tx_hash", none}]}, {["String"], [{"length", 1}, {"concat", 2}, {"sha3", 1}, {"sha256", 1}, {"blake2b", 1}]}, {["Bits"], [{"set", 2}, {"clear", 2}, {"test", 2}, {"sum", 1}, {"intersection", 2}, @@ -229,7 +241,9 @@ init_type_env() -> ["map"] => ?type(K, V, {map, K, V}), ["option"] => ?type(T, {variant, [[], [T]]}), ["Chain", "ttl"] => ?type({variant, [[integer], [integer]]}), - ["AENS", "pointee"] => ?type({variant, [[address], [address], [address]]}) + ["AENS", "pointee"] => ?type({variant, [[address], [address], [address]]}), + ["MCL_BLS12_381", "fr"] => ?type({bytes, 32}), + ["MCL_BLS12_381", "fp"] => ?type({bytes, 48}) }. is_no_code(Env) -> @@ -910,7 +924,14 @@ op_builtins() -> bits_difference, int_to_str, address_to_str, crypto_verify_sig, address_to_contract, crypto_verify_sig_secp256k1, crypto_sha3, crypto_sha256, crypto_blake2b, - crypto_ecverify_secp256k1, crypto_ecrecover_secp256k1 + crypto_ecverify_secp256k1, crypto_ecrecover_secp256k1, + mcl_bls12_381_g1_neg, mcl_bls12_381_g1_norm, mcl_bls12_381_g1_valid, + mcl_bls12_381_g1_is_zero, mcl_bls12_381_g1_add, mcl_bls12_381_g1_mul, + mcl_bls12_381_g2_neg, mcl_bls12_381_g2_norm, mcl_bls12_381_g2_valid, + mcl_bls12_381_g2_is_zero, mcl_bls12_381_g2_add, mcl_bls12_381_g2_mul, + mcl_bls12_381_gt_inv, mcl_bls12_381_gt_add, mcl_bls12_381_gt_mul, mcl_bls12_381_gt_pow, + mcl_bls12_381_gt_is_one, mcl_bls12_381_pairing, mcl_bls12_381_miller_loop, mcl_bls12_381_final_exp, + mcl_bls12_381_int_to_fr, mcl_bls12_381_int_to_fp, mcl_bls12_381_fr_to_int, mcl_bls12_381_fp_to_int ]. builtin_to_fcode(require, [Cond, Msg]) -> diff --git a/src/aeso_fcode_to_fate.erl b/src/aeso_fcode_to_fate.erl index 411f26b..46f827d 100644 --- a/src/aeso_fcode_to_fate.erl +++ b/src/aeso_fcode_to_fate.erl @@ -570,7 +570,31 @@ op_to_scode(crypto_sha256) -> aeb_fate_ops:sha256(?a, ?a); op_to_scode(crypto_blake2b) -> aeb_fate_ops:blake2b(?a, ?a); op_to_scode(string_sha3) -> aeb_fate_ops:sha3(?a, ?a); op_to_scode(string_sha256) -> aeb_fate_ops:sha256(?a, ?a); -op_to_scode(string_blake2b) -> aeb_fate_ops:blake2b(?a, ?a). +op_to_scode(string_blake2b) -> aeb_fate_ops:blake2b(?a, ?a); +op_to_scode(mcl_bls12_381_g1_neg) -> aeb_fate_ops:bls12_381_g1_neg(?a, ?a); +op_to_scode(mcl_bls12_381_g1_norm) -> aeb_fate_ops:bls12_381_g1_norm(?a, ?a); +op_to_scode(mcl_bls12_381_g1_valid) -> aeb_fate_ops:bls12_381_g1_valid(?a, ?a); +op_to_scode(mcl_bls12_381_g1_is_zero) -> aeb_fate_ops:bls12_381_g1_is_zero(?a, ?a); +op_to_scode(mcl_bls12_381_g1_add) -> aeb_fate_ops:bls12_381_g1_add(?a, ?a, ?a); +op_to_scode(mcl_bls12_381_g1_mul) -> aeb_fate_ops:bls12_381_g1_mul(?a, ?a, ?a); +op_to_scode(mcl_bls12_381_g2_neg) -> aeb_fate_ops:bls12_381_g2_neg(?a, ?a); +op_to_scode(mcl_bls12_381_g2_norm) -> aeb_fate_ops:bls12_381_g2_norm(?a, ?a); +op_to_scode(mcl_bls12_381_g2_valid) -> aeb_fate_ops:bls12_381_g2_valid(?a, ?a); +op_to_scode(mcl_bls12_381_g2_is_zero) -> aeb_fate_ops:bls12_381_g2_is_zero(?a, ?a); +op_to_scode(mcl_bls12_381_g2_add) -> aeb_fate_ops:bls12_381_g2_add(?a, ?a, ?a); +op_to_scode(mcl_bls12_381_g2_mul) -> aeb_fate_ops:bls12_381_g2_mul(?a, ?a, ?a); +op_to_scode(mcl_bls12_381_gt_inv) -> aeb_fate_ops:bls12_381_gt_inv(?a, ?a); +op_to_scode(mcl_bls12_381_gt_add) -> aeb_fate_ops:bls12_381_gt_add(?a, ?a, ?a); +op_to_scode(mcl_bls12_381_gt_mul) -> aeb_fate_ops:bls12_381_gt_mul(?a, ?a, ?a); +op_to_scode(mcl_bls12_381_gt_pow) -> aeb_fate_ops:bls12_381_gt_pow(?a, ?a, ?a); +op_to_scode(mcl_bls12_381_gt_is_one) -> aeb_fate_ops:bls12_381_gt_is_one(?a, ?a); +op_to_scode(mcl_bls12_381_pairing) -> aeb_fate_ops:bls12_381_pairing(?a, ?a, ?a); +op_to_scode(mcl_bls12_381_miller_loop) -> aeb_fate_ops:bls12_381_miller_loop(?a, ?a, ?a); +op_to_scode(mcl_bls12_381_final_exp) -> aeb_fate_ops:bls12_381_final_exp(?a, ?a); +op_to_scode(mcl_bls12_381_int_to_fr) -> aeb_fate_ops:bls12_381_int_to_fr(?a, ?a); +op_to_scode(mcl_bls12_381_int_to_fp) -> aeb_fate_ops:bls12_381_int_to_fp(?a, ?a); +op_to_scode(mcl_bls12_381_fr_to_int) -> aeb_fate_ops:bls12_381_fr_to_int(?a, ?a); +op_to_scode(mcl_bls12_381_fp_to_int) -> aeb_fate_ops:bls12_381_fp_to_int(?a, ?a). %% PUSH and STORE ?a are the same, so we use STORE to make optimizations %% easier, and specialize to PUSH (which is cheaper) at the end. @@ -843,6 +867,30 @@ attributes(I) -> {'AENS_UPDATE', A, B, C, D, E, F} -> Impure(none, [A, B, C, D, E, F]); {'AENS_TRANSFER', A, B, C, D} -> Impure(none, [A, B, C, D]); {'AENS_REVOKE', A, B, C} -> Impure(none, [A, B, C]); + {'BLS12_381_G1_NEG', A, B} -> Pure(A, [B]); + {'BLS12_381_G1_NORM', A, B} -> Pure(A, [B]); + {'BLS12_381_G1_VALID', A, B} -> Pure(A, [B]); + {'BLS12_381_G1_IS_ZERO', A, B} -> Pure(A, [B]); + {'BLS12_381_G1_ADD', A, B, C} -> Pure(A, [B, C]); + {'BLS12_381_G1_MUL', A, B, C} -> Pure(A, [B, C]); + {'BLS12_381_G2_NEG', A, B} -> Pure(A, [B]); + {'BLS12_381_G2_NORM', A, B} -> Pure(A, [B]); + {'BLS12_381_G2_VALID', A, B} -> Pure(A, [B]); + {'BLS12_381_G2_IS_ZERO', A, B} -> Pure(A, [B]); + {'BLS12_381_G2_ADD', A, B, C} -> Pure(A, [B, C]); + {'BLS12_381_G2_MUL', A, B, C} -> Pure(A, [B, C]); + {'BLS12_381_GT_INV', A, B} -> Pure(A, [B]); + {'BLS12_381_GT_ADD', A, B, C} -> Pure(A, [B, C]); + {'BLS12_381_GT_MUL', A, B, C} -> Pure(A, [B, C]); + {'BLS12_381_GT_POW', A, B, C} -> Pure(A, [B, C]); + {'BLS12_381_GT_IS_ONE', A, B} -> Pure(A, [B]); + {'BLS12_381_PAIRING', A, B, C} -> Pure(A, [B, C]); + {'BLS12_381_MILLER_LOOP', A, B, C} -> Pure(A, [B, C]); + {'BLS12_381_FINAL_EXP', A, B} -> Pure(A, [B]); + {'BLS12_381_INT_TO_FR', A, B} -> Pure(A, [B]); + {'BLS12_381_INT_TO_FP', A, B} -> Pure(A, [B]); + {'BLS12_381_FR_TO_INT', A, B} -> Pure(A, [B]); + {'BLS12_381_FP_TO_INT', A, B} -> Pure(A, [B]); {'ABORT', A} -> Impure(pc, A); {'EXIT', A} -> Impure(pc, A); 'NOP' -> Pure(none, []) diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl index 50130e6..5506da9 100644 --- a/test/aeso_compiler_tests.erl +++ b/test/aeso_compiler_tests.erl @@ -161,11 +161,12 @@ compilable_contracts() -> "list_comp", "payable", "unapplied_builtins", - "underscore_number_literals" + "underscore_number_literals", + "pairing_crypto" ]. not_yet_compilable(fate) -> []; -not_yet_compilable(aevm) -> []. +not_yet_compilable(aevm) -> ["pairing_crypto"]. %% Contracts that should produce type errors diff --git a/test/contracts/pairing_crypto.aes b/test/contracts/pairing_crypto.aes new file mode 100644 index 0000000..93f4a24 --- /dev/null +++ b/test/contracts/pairing_crypto.aes @@ -0,0 +1,30 @@ +include "BLS12_381.aes" + +contract GrothVerify = + type fr = BLS12_381.fr + type g1 = BLS12_381.g1 + type g2 = BLS12_381.g2 + + record proof = { a : g1, b : g2, c : g1 } + record verify_key = { a : g1, b : g2, c : g2, d : g2, ic : list(g1) } + + record state = { vk : verify_key } + + entrypoint init(vk0 : verify_key) = {vk = vk0} + + entrypoint verify_proof(p : proof, input : list(fr)) = + let vk = state.vk + let vk_x = calc_vk_x(vk.ic, input) + + BLS12_381.pairing_check([BLS12_381.g1_neg(p.a), vk.a, vk_x, p.c], + [p.b, vk.b, vk.c, vk.d]) + + function calc_vk_x(ics : list(g1), xs : list(fr)) = + switch(ics) + (ic :: ics) => calc_vk_x_(ic, ics, xs) + + function calc_vk_x_(vk_x : g1, ics : list(g1), xs : list(fr)) = + switch((ics, xs)) + ([], []) => vk_x + (ic :: ics, x :: xs) => calc_vk_x_(BLS12_381.g1_add(vk_x, BLS12_381.g1_mul(x, ic)), ics, xs) +