Callcium
Building Policies

Array Constraints

Constrain elements of array parameters using path quantifiers.

Array parameters are constrained element-by-element using path quantifiers. A quantifier extends the arg() path to apply a constraint across every element, or to require that at least one element satisfies it.

Path indexing

To constrain a specific element, add the element index as the next step after the array argument index:

import { arg } from "callcium/Constraint.sol";

arg(0, 0)  // first element of the first parameter
arg(0, 3)  // fourth element of the first parameter

This is the same indexing syntax used for struct fields.

Quantifiers

Path.ALL and Path.ANY replace a concrete element index to apply a constraint across the entire array. Import them from Path:

import { Path } from "callcium/Path.sol";
QuantifierSemanticsEmpty array
Path.ALLEvery element satisfies the loop's constraintsPasses
Path.ANYAt least one element satisfies all of themFails

The constraints of a group that share an array and a quantifier form one loop over that array. Under ALL, every element satisfies each of them. Under ANY, one element satisfies all of them together:

import { arg } from "callcium/Constraint.sol";
import { Path } from "callcium/Path.sol";
import { PolicyBuilder } from "callcium/PolicyBuilder.sol";

// struct Transfer { address to; uint256 amount; }
// function batchTransfer(Transfer[] transfers)
bytes memory policy = PolicyBuilder
    .create("batchTransfer((address,uint256)[])")
    .add(arg(0, Path.ANY, 0).eq(TREASURY))                // transfers[any].to
    .add(arg(0, Path.ANY, 1).gte(uint256(1_000e18)))      // transfers[any].amount
    .build();

The data is valid against this policy only when a single transfer goes to the treasury with at least 1,000 tokens. A transfer to the treasury of 1 token beside a transfer of 1,000 tokens elsewhere does not satisfy it.

Path.ALL is vacuously true on an empty array. When an empty array must be rejected, add a length constraint to the same group: lengthGt(0) alongside the ALL constraint.

import { arg } from "callcium/Constraint.sol";
import { Path } from "callcium/Path.sol";
import { PolicyBuilder } from "callcium/PolicyBuilder.sol";

// function batchTransfer(address[] recipients, uint256[] amounts)
bytes memory policy = PolicyBuilder
    .create("batchTransfer(address[],uint256[])")
    .add(arg(0, Path.ALL).isIn(allowlist))           // recipients — all must be approved
    .add(arg(1, Path.ALL).lte(uint256(1_000e18)))    // amounts — all within limit
    .build();

Nested patterns

Quantifiers compose with the rest of the path. To constrain a field inside each element of an array of structs, place the quantifier between the array step and the field step:

import { arg } from "callcium/Constraint.sol";
import { Path } from "callcium/Path.sol";
import { PolicyBuilder } from "callcium/PolicyBuilder.sol";

// struct Transfer { address to; uint256 amount; }
// function batchTransfer(Transfer[] transfers)
bytes memory policy = PolicyBuilder
    .create("batchTransfer((address,uint256)[])")
    .add(arg(0, Path.ALL, 0).isIn(allowlist))           // transfers[*].to
    .add(arg(0, Path.ALL, 1).lte(uint256(1_000e18)))    // transfers[*].amount
    .build();

A struct that contains an array is navigated in the opposite order — reach the array via its field index, then apply the quantifier:

import { arg } from "callcium/Constraint.sol";
import { Path } from "callcium/Path.sol";
import { PolicyBuilder } from "callcium/PolicyBuilder.sol";

// struct Order { address spender; uint256[] amounts; }
// function submit(Order order)
bytes memory policy = PolicyBuilder
    .create("submit((address,uint256[]))")
    .add(arg(0, 0).eq(TREASURY))                          // order.spender
    .add(arg(0, 1, Path.ALL).lte(uint256(1_000e18)))      // order.amounts[*]
    .build();

Limits

A path holds at most MAX_PATH_DEPTH steps, counted from the argument across the loop it passes through, the quantifier not included (PWF-14). It passes through at most one quantifier. add() rejects a second quantifier, and the builder a deeper path.

A loop evaluates at most MAX_QUANTIFIED_ARRAY_LENGTH elements — enforcement reverts with QuantifierLimitExceeded on a longer array.

Loops dominate enforcement gas. Cost grows with the root rules and, in a loop, with the array's elements times the body's tests; each test adds one offset read per hop on its path. MAX_QUANTIFIED_ARRAY_LENGTH and MAX_PATH_DEPTH bound one loop and one path, not a policy: they keep the verdict independent of the chain, and they do not keep a policy within a transaction's gas cap. Benchmark a policy with many loops or heavy loop bodies on the target chain before storing it — opcode costs and transaction gas caps are chain-specific.

On this page