Macro: dynamic-member length/index/forwarding on struct-array elements (unblocks UnlinkPool body translation)

[Th0rgal]

Summary

After #1832 / #1843 shipped, verity_contract now accepts struct-array parameters whose elements carry nested dynamic members (e.g. Array Transaction where each Transaction contains uint256[] nullifierHashes), and projects single-word static leaves from those elements via Expr.arrayElementDynamicWord / Expr.paramDynamicHeadWord.

That is strictly less than what writing the UnlinkPool.transfer / withdraw / emergencyWithdraw bodies actually needs. The roadmap (docs/ROADMAP.md "Unlink Audit Readiness") currently claims that promotion to build_green only requires writing the bodies; an empirical pilot against verity-benchmark@1e9b631 shows three additional macro capabilities are still missing.

Reproducer

UnlinkPool.transfer (UnlinkPool.sol:328-359, pinned commit 4bc46c1f) needs to:

for (uint256 i = 0; i < _transactions.length; i++) {
  Transaction calldata txn = _transactions[i];
  if (txn.nullifierHashes.length != c.inputCount) revert ...;          // (1)
  if (txn.ciphertexts.length != _countNonZero(txn.newCommitments, ...)) // (2)
  _validateContext(..., _computeContextHash(txn.ciphertexts));         // (3)
  _verifyProof(c.verifier, txn.proof, txn.merkleRoot, txn.contextHash,
               txn.nullifierHashes, txn.newCommitments);               // (3)
  emit Transferred(newRoot, startIndex, leaves,
                   _realNullifiers(txn.nullifierHashes), txn.ciphertexts); // (3)
}

Each of (1), (2), (3) is rejected by Verity/Macro/Translate.lean on b2f2ee40:

Specific gaps

G1. arrayLength on a struct-element dynamic member

txn.nullifierHashes.length. arrayLength only resolves direct param refs via lookupNamedValueType? (Translate.lean:2383-2387):

| `(term| arrayLength $name:term) =>
    match lookupNamedValueType? constDecls immutableDecls params locals
      (← expectStringOrIdent name) with
    | some (.array _) => pure .uint256
    | _ => throwErrorAt name "unknown array value"

There is no path for arrayLength (arrayElement _transactions i).nullifierHashes.

G2. Element indexing on struct-element dynamic members

txn.nullifierHashes[k]. arrayElement is gated by requireDirectParamRef name "arrayElement" params at Translate.lean:2390, which rejects anything other than a direct parameter ident.

G3. Passing dynamic arrays to tryExternalCall / externalCall / emit argument lists

tryExternalCall, externalCall, and emit argument lists all require requireWordLikeType (Translate.lean:2411, :2623). There is no way to pass txn.nullifierHashes (or any Array-typed local) as an external-call argument, an event component, or a custom-error payload component.

Combined with #1824, these gaps make the body impossible to write line-by-line: every internal helper that takes dynamic arrays would have to be inlined, and the inlined code still cannot read element counts or individual elements out of the struct-array members.

Desired behavior

Three macro-level lifts, in increasing order of scope:

1. G1: Allow arrayLength (arrayElement <param> <index>).<dynamicField> to lower through a new Expr.arrayElementDynamicMemberLength (or extend arrayElementDynamicWord) — the encoded layout already carries the head pointer; resolving it to the underlying length word is one extra mload/calldataload step.

2. G2: Allow arrayElement (arrayElement <param> <index>).<dynamicField> <innerIndex> similarly — one further bounds-checked word read at headPtr + 32 + innerIndex*32.

3. G3: A whitelisted "pass-through" for Array <wordLike> arguments to tryExternalCall / emit / revertError so the macro can hand off an already-encoded calldata slice (the dynamic member already lives in calldata at a known offset/length) without forcing the caller into word-level encoding.

G1 is the smallest unblocker that lets the macro emit shape-check reverts (PoolInvalidInputShape / PoolInvalidOutputShape / PoolCiphertextCountMismatch). G2 unblocks the per-tx nullifier loop. G3 plus #1824 is the final piece.

Scope

This issue is the macro-level prerequisite for the verity-benchmark cases/unlink_xyz/pool/ promotion to build_green, which the ROADMAP currently lists as the trailing Unlink-audit work item under #1760. The maintainer-facing roadmap and the unlink_xyz/pool Contract.lean footer / case.yaml unsupported_feature_codes will be updated in a paired benchmark PR to reference this issue once filed, replacing the current over-optimistic "only requires writing the bodies" wording.

[Th0rgal]

Closing as implemented.

The three macro lifts this issue tracked are now present on lfglabs/main:

• G1: arrayLength on struct-element dynamic members is represented by Expr.arrayElementDynamicMemberLength and covered in source/proof boundary plumbing.
• G2: indexing struct-element dynamic members is represented by Expr.arrayElementDynamicMemberElement / related data-offset support.
• G3: projected dynamic-array arguments can be forwarded through event/call/error ABI paths, with Unlink-shape smoke coverage.

I also opened a docs cleanup PR to remove the stale roadmap text that still described #1849 and #1824 as the final Unlink body-translation gates. The remaining Unlink helper blocker is the narrower internal-helper ABI lowering gap tracked in #1889.