Files
darkfi/proof/lead.zk
parazyd 6a024ab801 zkas: Add a field definition on top of the circuit file.
Currently unused, but will probably be expanded to define proofs over
different fields.
2023-08-14 17:09:18 +02:00

98 lines
3.2 KiB
Plaintext

k = 13;
field = "pallas";
constant "Lead" {
EcFixedPointShort VALUE_COMMIT_VALUE,
EcFixedPoint VALUE_COMMIT_RANDOM,
EcFixedPointBase NULLIFIER_K,
}
witness "Lead" {
MerklePath c1_cm_path,
Uint32 c1_cm_pos,
Uint32 c1_sk_pos,
Base c1_sk,
Base c1_sk_root,
MerklePath c1_sk_path,
Base c1_slot,
Base c1_rho,
Scalar c1_opening,
Base value,
Scalar c2_opening,
Base mu_rho,
Base mu_y,
Base sigma1,
Base sigma2,
Base headstart,
}
circuit "Lead" {
ZERO = witness_base(0);
ONE = witness_base(1);
REWARD = witness_base(1);
PREFIX_EVL = witness_base(2);
PREFIX_SEED = witness_base(3);
PREFIX_CM = witness_base(4);
PREFIX_PK = witness_base(5);
PREFIX_SN = witness_base(6);
# coin (1) pk
pk = poseidon_hash(PREFIX_PK, c1_sk_root, c1_slot, ZERO);
constrain_instance(pk);
# coin (1) cm/commitment
c1_cm_msg = poseidon_hash(PREFIX_CM, pk, value, c1_rho);
c1_cm_v = ec_mul_base(c1_cm_msg, NULLIFIER_K);
c1_cm_r = ec_mul(c1_opening, VALUE_COMMIT_RANDOM);
c1_cm = ec_add(c1_cm_v, c1_cm_r);
c1_cm_x = ec_get_x(c1_cm);
c1_cm_y = ec_get_y(c1_cm);
c1_cm_hash = poseidon_hash(c1_cm_x, c1_cm_y);
constrain_instance(c1_cm_x);
constrain_instance(c1_cm_y);
# coin (2) rho/nonce
c2_rho = poseidon_hash(PREFIX_EVL, c1_sk_root, c1_rho, ZERO);
# coin (2) cm/commitment
# reward
c2_value = base_add(value, REWARD);
c2_cm_msg = poseidon_hash(PREFIX_CM, pk, c2_value, c2_rho);
c2_cm_v = ec_mul_base(c2_cm_msg, NULLIFIER_K);
c2_cm_r = ec_mul(c2_opening, VALUE_COMMIT_RANDOM);
c2_cm = ec_add(c2_cm_v, c2_cm_r);
c2_cm_x = ec_get_x(c2_cm);
c2_cm_y = ec_get_y(c2_cm);
constrain_instance(c2_cm_x);
constrain_instance(c2_cm_y);
# root of path to burnt coin commitment at given pos
root = merkle_root(c1_cm_pos, c1_cm_path, c1_cm_hash);
constrain_instance(root);
# root of path at c1_sk_pos
root_sk = merkle_root(c1_sk_pos, c1_sk_path, c1_sk);
constrain_instance(root_sk);
# coin (1) sn/nullifier
sn = poseidon_hash(PREFIX_SN, c1_sk_root, c1_rho, ZERO);
constrain_instance(sn);
# lottery seed
seed = poseidon_hash(PREFIX_SEED, c1_sk_root, c1_rho, ZERO);
# y
y = poseidon_hash(seed, mu_y);
###
constrain_instance(mu_y);
constrain_instance(y);
# rho
rho = poseidon_hash(seed, mu_rho);
constrain_instance(mu_rho);
constrain_instance(rho);
# target
term1 = base_mul(sigma1, value);
term2_1 = base_mul(sigma2, value);
term2 = base_mul(term2_1, value);
target = base_add(term1, term2);
shifted_target = base_add(target, headstart);
#lottery
#constrain public value sigma1
constrain_instance(sigma1);
# constrain public value sigma2
constrain_instance(sigma2);
less_than_loose(y, shifted_target);
}