karatum_rep.circom

pragma circom 2.1.9;

// Karatum zero-knowledge reputation proof (zkrep v1).
//
// Statement: "I know the secret behind a leaf of the Karatum reputation tree with root `root` whose certificate is
// for task class `taskClass`, has tier >= `minTier` and K >= `minKarats`, status VALID and expires after `nowTs`.
// My nullifier for verifier scope `scope` is `nullifier`, and this proof is bound to message `messageHash`."
//
// Hidden: which leaf (so which agent / wallet / build), the exact tier, K and expiry, the identity secret.
// Public:  root, taskClass, minTier, minKarats, nowTs, scope, messageHash and the nullifier (output, first signal).
//
// Leaf    = Poseidon6(idCommitment, taskClass, tier, karats, expiresAt, status)   status: 1 = VALID
// idComm  = Poseidon1(secret)
// Nullif. = Poseidon3(NULLIFIER_DOMAIN, secret, scope)
// Tree    = binary Poseidon2 Merkle tree of fixed depth DEPTH, empty leaves = 0.

include "circomlib/circuits/poseidon.circom";
include "circomlib/circuits/comparators.circom";
include "circomlib/circuits/bitify.circom";

template MerkleRoot(depth) {
    signal input leaf;
    signal input pathElements[depth];
    signal input pathIndices[depth];
    signal output root;

    signal cur[depth + 1];
    signal left[depth];
    signal right[depth];
    component h[depth];
    cur[0] <== leaf;
    for (var i = 0; i < depth; i++) {
        // pathIndices[i] = 1: the current node is the right child.
        pathIndices[i] * (1 - pathIndices[i]) === 0;
        left[i] <== cur[i] + pathIndices[i] * (pathElements[i] - cur[i]);
        right[i] <== pathElements[i] + cur[i] - left[i];
        h[i] = Poseidon(2);
        h[i].inputs[0] <== left[i];
        h[i].inputs[1] <== right[i];
        cur[i + 1] <== h[i].out;
    }
    root <== cur[depth];
}

template KaratumRep(depth) {
    // ---- public inputs
    signal input root;
    signal input taskClass;
    signal input minTier;
    signal input minKarats;
    signal input nowTs;
    signal input scope;
    signal input messageHash;
    // ---- private inputs
    signal input secret;
    signal input tier;
    signal input karats;
    signal input expiresAt;
    signal input pathElements[depth];
    signal input pathIndices[depth];
    // ---- output
    signal output nullifier;

    var STATUS_VALID = 1;
    // keccak256("karatum.zkrep.nullifier.v1") >> 8, a constant domain tag.
    var NULLIFIER_DOMAIN = 0x584a3c508bfb328f419e54e59f6549dd2a40962c5750ac61edc8ec61e4100f;

    // Range checks: comparators below are only sound on bounded inputs.
    component bTier = Num2Bits(8);      bTier.in <== tier;
    component bKarats = Num2Bits(8);    bKarats.in <== karats;
    component bMinTier = Num2Bits(8);   bMinTier.in <== minTier;
    component bMinKarats = Num2Bits(8); bMinKarats.in <== minKarats;
    component bExpires = Num2Bits(64);  bExpires.in <== expiresAt;
    component bNow = Num2Bits(64);      bNow.in <== nowTs;

    component tierOk = GreaterEqThan(8);
    tierOk.in[0] <== tier;
    tierOk.in[1] <== minTier;
    tierOk.out === 1;

    component karatsOk = GreaterEqThan(8);
    karatsOk.in[0] <== karats;
    karatsOk.in[1] <== minKarats;
    karatsOk.out === 1;

    component live = GreaterThan(64);
    live.in[0] <== expiresAt;
    live.in[1] <== nowTs;
    live.out === 1;

    component id = Poseidon(1);
    id.inputs[0] <== secret;

    component leaf = Poseidon(6);
    leaf.inputs[0] <== id.out;
    leaf.inputs[1] <== taskClass;
    leaf.inputs[2] <== tier;
    leaf.inputs[3] <== karats;
    leaf.inputs[4] <== expiresAt;
    leaf.inputs[5] <== STATUS_VALID;

    component tree = MerkleRoot(depth);
    tree.leaf <== leaf.out;
    for (var i = 0; i < depth; i++) {
        tree.pathElements[i] <== pathElements[i];
        tree.pathIndices[i] <== pathIndices[i];
    }
    tree.root === root;

    component nul = Poseidon(3);
    nul.inputs[0] <== NULLIFIER_DOMAIN;
    nul.inputs[1] <== secret;
    nul.inputs[2] <== scope;
    nullifier <== nul.out;

    // Bind the proof to the message (and to scope/taskClass, already used above): a non-trivial constraint so the
    // optimiser cannot drop the public input.
    signal messageSquare;
    messageSquare <== messageHash * messageHash;
}

component main {public [root, taskClass, minTier, minKarats, nowTs, scope, messageHash]} = KaratumRep(20);