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);
}