Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
270 changes: 194 additions & 76 deletions generalized-predicates/README.md

Large diffs are not rendered by default.

45 changes: 38 additions & 7 deletions wallet-unit-poc/circom/circuits/components/eval-predicates.circom
Original file line number Diff line number Diff line change
Expand Up @@ -7,20 +7,21 @@ include "eval-predicate.circom";
/// @notice Evaluates an array of atomic predicates over a fixed-size claim array.
/// @dev Claim references are integer indices into `claimValues`.
/// @dev Predicate tuple encoding per slot i:
/// @dev [predicateClaimRefs[i], predicateOps[i], predicateCompareValues[i]]
/// @dev [predicateClaimRefs[i], predicateOps[i], rhsIsRef[i], rhsRef[i], rhsValue[i]]
/// @dev Operator encoding:
/// @dev 0 = <=
/// @dev 1 = >=
/// @dev 2 = ==
template EvalPredicates(N_CLAIMS, MAX_PREDICATES, VALUE_BITS) {
signal input claimValues[N_CLAIMS];
signal input claimValues[N_CLAIMS]; // Canonically normalized claim values.

// Number of active predicate tuples in [0, MAX_PREDICATES]
signal input predicateLen;
signal input predicateLen; // Number of active predicate tuples.

signal input predicateClaimRefs[MAX_PREDICATES];
signal input predicateOps[MAX_PREDICATES];
signal input predicateCompareValues[MAX_PREDICATES];
signal input predicateClaimRefs[MAX_PREDICATES]; // Left-hand claim reference per predicate.
signal input predicateOps[MAX_PREDICATES]; // Operator per predicate: 0<=, 1>=, 2==.
signal input predicateRhsIsRef[MAX_PREDICATES]; // Right-hand side (RHS) mode: 0=literal, 1=claim reference.
signal input predicateRhsValues[MAX_PREDICATES]; // RHS operand: claim index when predicateRhsIsRef is 1, literal value when 0.

signal output predicateResults[MAX_PREDICATES];

Expand All @@ -30,6 +31,17 @@ template EvalPredicates(N_CLAIMS, MAX_PREDICATES, VALUE_BITS) {
signal refCount[MAX_PREDICATES][N_CLAIMS + 1];
signal refAccum[MAX_PREDICATES][N_CLAIMS + 1];
signal selectedClaimValues[MAX_PREDICATES];
component rhsRefEq[MAX_PREDICATES][N_CLAIMS];
signal rhsRefSelected[MAX_PREDICATES][N_CLAIMS];
signal rhsRefProduct[MAX_PREDICATES][N_CLAIMS];
signal rhsRefCount[MAX_PREDICATES][N_CLAIMS + 1];
signal rhsRefAccum[MAX_PREDICATES][N_CLAIMS + 1];
signal selectedRhsRefValues[MAX_PREDICATES];
signal rhsIsRef[MAX_PREDICATES];
signal rhsRefActive[MAX_PREDICATES];
signal literalRhsValue[MAX_PREDICATES];
signal refRhsValue[MAX_PREDICATES];
signal selectedCompareValues[MAX_PREDICATES];
component activeLt[MAX_PREDICATES];
signal isActive[MAX_PREDICATES];
signal effectiveClaimValue[MAX_PREDICATES];
Expand All @@ -49,9 +61,14 @@ template EvalPredicates(N_CLAIMS, MAX_PREDICATES, VALUE_BITS) {
activeLt[i].in[0] <== i;
activeLt[i].in[1] <== predicateLen;
isActive[i] <== activeLt[i].out;
rhsIsRef[i] <== predicateRhsIsRef[i];
rhsIsRef[i] * (rhsIsRef[i] - 1) === 0;
rhsRefActive[i] <== isActive[i] * rhsIsRef[i];

refCount[i][0] <== 0;
refAccum[i][0] <== 0;
rhsRefCount[i][0] <== 0;
rhsRefAccum[i][0] <== 0;

for (var j = 0; j < N_CLAIMS; j++) {
claimRefEq[i][j] = IsEqual();
Expand All @@ -62,15 +79,29 @@ template EvalPredicates(N_CLAIMS, MAX_PREDICATES, VALUE_BITS) {
refProduct[i][j] <== refSelected[i][j] * claimValues[j];
refCount[i][j + 1] <== refCount[i][j] + refSelected[i][j];
refAccum[i][j + 1] <== refAccum[i][j] + refProduct[i][j];

rhsRefEq[i][j] = IsEqual();
rhsRefEq[i][j].in[0] <== predicateRhsValues[i];
rhsRefEq[i][j].in[1] <== j;

rhsRefSelected[i][j] <== rhsRefActive[i] * rhsRefEq[i][j].out;
rhsRefProduct[i][j] <== rhsRefSelected[i][j] * claimValues[j];
rhsRefCount[i][j + 1] <== rhsRefCount[i][j] + rhsRefSelected[i][j];
rhsRefAccum[i][j + 1] <== rhsRefAccum[i][j] + rhsRefProduct[i][j];
}

// Active predicates must reference exactly one valid claim index.
// Inactive predicates must reference none (count 0).
refCount[i][N_CLAIMS] - isActive[i] === 0;
rhsRefCount[i][N_CLAIMS] - rhsRefActive[i] === 0;

selectedClaimValues[i] <== refAccum[i][N_CLAIMS];
selectedRhsRefValues[i] <== rhsRefAccum[i][N_CLAIMS];
literalRhsValue[i] <== (1 - rhsIsRef[i]) * predicateRhsValues[i];
refRhsValue[i] <== rhsIsRef[i] * selectedRhsRefValues[i];
selectedCompareValues[i] <== literalRhsValue[i] + refRhsValue[i];
effectiveClaimValue[i] <== isActive[i] * selectedClaimValues[i];
effectiveCompareValue[i] <== isActive[i] * predicateCompareValues[i];
effectiveCompareValue[i] <== isActive[i] * selectedCompareValues[i];
effectiveOp[i] <== isActive[i] * predicateOps[i] + (1 - isActive[i]) * 2;

predicateEval[i] = EvalPredicate(VALUE_BITS);
Expand Down
22 changes: 12 additions & 10 deletions wallet-unit-poc/circom/circuits/components/expression.circom
Original file line number Diff line number Diff line change
Expand Up @@ -10,20 +10,21 @@ include "logical-expressions.circom";
/// @dev Claims are referenced by integer indices into `claimValues`.
/// @dev Claim values must already be canonically encoded as field elements.
template ExpressionEvaluator(N_CLAIMS, MAX_PREDICATES, MAX_EXPR_TOKENS, VALUE_BITS) {
signal input claimValues[N_CLAIMS];
signal input claimValues[N_CLAIMS]; // Canonically normalized claim values.

// Predicate tuples: [claimRef, op, compareValue]
signal input predicateLen;
signal input predicateClaimRefs[MAX_PREDICATES];
signal input predicateOps[MAX_PREDICATES];
signal input predicateCompareValues[MAX_PREDICATES];
// Predicate tuples: [claimRef, op, rhsIsRef, rhsRef, rhsValue]
signal input predicateLen; // Number of active predicate tuples.
signal input predicateClaimRefs[MAX_PREDICATES]; // Left-hand claim reference per predicate.
signal input predicateOps[MAX_PREDICATES]; // Operator per predicate: 0<=, 1>=, 2==.
signal input predicateRhsIsRef[MAX_PREDICATES]; // Right-hand side (RHS) mode: 0=literal, 1=claim reference.
signal input predicateRhsValues[MAX_PREDICATES]; // RHS operand: claim index when predicateRhsIsRef is 1, literal value when 0.

// Postfix expression token arrays.
// tokenTypes[i]: 0=REF, 1=AND, 2=OR, 3=NOT
// tokenValues[i]: predicate index for REF, else 0
signal input tokenTypes[MAX_EXPR_TOKENS];
signal input tokenValues[MAX_EXPR_TOKENS];
signal input exprLen;
signal input tokenTypes[MAX_EXPR_TOKENS]; // Postfix token kind: 0=REF, 1=AND, 2=OR, 3=NOT.
signal input tokenValues[MAX_EXPR_TOKENS]; // Token payload: predicate index for REF tokens.
signal input exprLen; // Number of active logical-expression tokens.

signal output predicateResults[MAX_PREDICATES];
signal output finalResult;
Expand All @@ -33,7 +34,8 @@ template ExpressionEvaluator(N_CLAIMS, MAX_PREDICATES, MAX_EXPR_TOKENS, VALUE_BI
predicatePhase.predicateLen <== predicateLen;
predicatePhase.predicateClaimRefs <== predicateClaimRefs;
predicatePhase.predicateOps <== predicateOps;
predicatePhase.predicateCompareValues <== predicateCompareValues;
predicatePhase.predicateRhsIsRef <== predicateRhsIsRef;
predicatePhase.predicateRhsValues <== predicateRhsValues;

predicateResults <== predicatePhase.predicateResults;

Expand Down
30 changes: 16 additions & 14 deletions wallet-unit-poc/circom/circuits/show.circom
Original file line number Diff line number Diff line change
Expand Up @@ -14,23 +14,24 @@ include "components/expression.circom";
/// tokenTypes[i]: 0=REF, 1=AND, 2=OR, 3=NOT
/// tokenValues[i]: predicate index for REF, else 0
template Show(nClaims, maxPredicates, maxLogicTokens, valueBits) {
signal input deviceKeyX;
signal input deviceKeyY;
signal input messageHash;
signal input sig_r;
signal input sig_s_inverse;
signal input deviceKeyX; // Device binding public key x-coordinate.
signal input deviceKeyY; // Device binding public key y-coordinate.
signal input messageHash; // Scalar-field reduced hash of the verifier nonce.
signal input sig_r; // ECDSA signature r value over messageHash.
signal input sig_s_inverse; // Multiplicative inverse of signature s in the scalar field.

// Generalized predicate phase inputs
signal input predicateLen;
signal input claimValues[nClaims];
signal input predicateClaimRefs[maxPredicates];
signal input predicateOps[maxPredicates];
signal input predicateCompareValues[maxPredicates];
signal input predicateLen; // Number of active predicates.
signal input claimValues[nClaims]; // Normalized claim values addressable by reference index.
signal input predicateClaimRefs[maxPredicates]; // Left-hand claim reference per predicate.
signal input predicateOps[maxPredicates]; // Operator per predicate: 0<=, 1>=, 2==.
signal input predicateRhsIsRef[maxPredicates]; // Right-hand side (RHS) mode per predicate: 0=literal, 1=claim reference.
signal input predicateRhsValues[maxPredicates]; // RHS operand: claim index when predicateRhsIsRef is 1, literal value when 0.

// Logical expression over predicate results in Reverse Polish Notation.
signal input tokenTypes[maxLogicTokens];
signal input tokenValues[maxLogicTokens];
signal input exprLen;
signal input tokenTypes[maxLogicTokens]; // Postfix token kind: 0=REF, 1=AND, 2=OR, 3=NOT.
signal input tokenValues[maxLogicTokens]; // Token payload: predicate index for REF tokens.
signal input exprLen; // Number of active expression tokens.

// Output: result of the logical expression over all predicate results
signal output expressionResult;
Expand All @@ -48,7 +49,8 @@ template Show(nClaims, maxPredicates, maxLogicTokens, valueBits) {
expressionEval.predicateLen <== predicateLen;
expressionEval.predicateClaimRefs <== predicateClaimRefs;
expressionEval.predicateOps <== predicateOps;
expressionEval.predicateCompareValues <== predicateCompareValues;
expressionEval.predicateRhsIsRef <== predicateRhsIsRef;
expressionEval.predicateRhsValues <== predicateRhsValues;
expressionEval.tokenTypes <== tokenTypes;
expressionEval.tokenValues <== tokenValues;
expressionEval.exprLen <== exprLen;
Expand Down
Loading
Loading