Zodiac Roles v3 Decoder Faithfulness

Zodiac Roles lets Safe accounts scope what a role can call. In v2, some integrations needed custom verifiers because the permission checker had to interpret calldata exactly the way the target contract would. A decoder mismatch is an authorization bug: the check can pass on one value while the callee executes a different value.

This benchmark targets the unreleased Roles v3 decoder on the `contracts-v3` branch. We modeled the lazy ABI walker around AbiLocation.sol, Topology.sol, and ConditionEvaluator.__input, then proved a focused faithfulness and bounds-safety result.

Why It Matters

The dangerous failure mode is not an ordinary revert. It is a decoder/callee mismatch: a role condition is checked against one interpreted argument, while the target contract executes another. For permission systems, that is an authorization bypass.

The main theorem says that, for the modeled ABI type tree and leaf path, the Roles decoder and a hand-written canonical ABI v2 layout model isolate the same byte region. The bounds theorem says every successful Roles extraction is inside calldata; malformed guarded reads, non-forward tails, and out-of-range tails return overflow.

How This Was Modeled and Proven

The reference model is deliberately hand-written from ABI HEAD/TAIL layout rather than built from Roles' packed condition metadata. It is not an external ABI oracle. The proof shows that the Roles-shaped model and the ABI-shaped model agree; reviewers also cross-checked the transcriptions against the Solidity source and the ABI layout rules.

Tuple and dynamic-array sizes are full encoded regions. Dynamic tuple children contribute their offset word plus tail payload. Dynamic arrays contribute the length word plus every encoded element. This matches the shape of `AbiLocation.size`.

The proof is split into metadata, size, traversal, and bounds lemmas. The metadata bridge proves Roles inline metadata agrees with ABI staticness. The encoded-size lemmas cover static words, dynamic bytes and strings, tuples, dynamic arrays, nested ABI encoded payloads, and transparent logical wrappers.

git clone --branch zodiac-roles-decoder-faithfulness https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.Zodiac.RolesDecoderFaithfulness

Assumptions

These are proof boundaries and model choices, not hidden proof steps. The checked Lean theorems have no case-specific axioms; this table explains what the focused decoder model assumes about upstream validation, calldata shape, and comparison helpers.

• integrity_roundtripwell-formed tree metadata

  Integrity.enforce + pack/unpack

  The flat condition array is assumed to unpack into a finite type tree whose metadata equals the modeled Roles inline predicates.

• canonical_calldatafaithfulness interpretation

  Solidity ABI v2

  Canonical calldata is the premise for saying the callee reads the same governed field. Malformed calldata is handled by the overflow and bounds theorem.

• hash_and_subword_pathscomparison layer

  ConditionEvaluator

  Keccak injectivity and big-endian shift/mask identities are needed only when applying extracted byte regions to hash or sub-word comparison paths.

Learn More

`#print axioms` reports no case-specific axioms. The public theorems depend only on Lean foundations: `propext`, and `Quot.sound` for the main faithfulness theorem.

Read the pinned Roles v3 source, the model, and the checked proofs.