feat(EDSL): arrayLength for Bytes/String dynamic values (supersedes #1991)

[Th0rgal]

Summary

Supersedes #1991 (thanks @poonai — your commit is included as-is, you're a co-author of this PR). This lands arrayLength support for bytes/string dynamic values at the executable level, plus the CI fix and a small architecture review pass.

What's included

poonai's commit (cherry-picked, authorship preserved):

• ArrayLength typeclass in Contracts/Common.lean so arrayLength accepts non-Array dynamic values.
• ArrayElementDynamicMemberBytesSmoke covering arrayLength ops.callData (struct param member) and arrayLength (arrayElement ops idx).callData (struct-array element member).

Follow-up commit (review findings):

1. Removed the Bytes32 instance. Verity.Bytes32 is a reducible abbrev of Uint256, so instance : ArrayLength Bytes32 := 32 silently made arrayLength (x : Uint256) typecheck and return 32 for every word value — a spec-level footgun. It was also unreachable from contract bodies: the macro type gate (Verity/Macro/Translate/Expr.lean) rejects arrayLength on non-dynamic named values, and bytes32 carries no ABI length word. Documented the decision in a docstring.
2. Added the String instance (String.utf8ByteSize). .string dynamic members pass the exact same macro gate (paramDynamicMemberProjection? accepts .array | .bytes | .string), so without it the string analogue of the fixed case still failed executable elaboration. utf8ByteSize matches the EVM ABI length-word semantics (byte length, not codepoints).
3. Extended the smoke with a String-member case (labelLength, asserting paramDynamicMemberLength "ops" 1) and normalized formatting to match ArrayElementDynamicMemberLengthSmoke.
4. Committed the generated property-test artifact PropertyArrayElementDynamicMemberBytesSmoke.t.sol (the missing artifact that failed checks on make array length work for Bytes and Bytes32 #1991) via scripts/check_macro_property_test_generation.py.
5. Docs: docs-site/content/edsl-api-reference.mdx dynamic-arrays section now documents arrayLength on Bytes/String members, the lowering path, and why fixed-width word types intentionally have no length surface.

Verification

• make check passes locally (including the macro property-test artifact check — the job that failed on make array length work for Bytes and Bytes32 #1991).
• A local lake build Contracts.Smoke.ArrayElementDynamicMemberBytesSmoke was still running when this PR was opened; CI is the authority for the Lean compilation of the smoke rfl examples and the executable elaboration through the new instances.

Relation to issues

This is an EDSL-surface primitive on the dynamic-ABI track (#1982 P0-1). It does not close #1975 (struct-array calldata decoding), which needs ABI head/tail lowering in codegen.

---

Note

Low Risk
EDSL executable/runtime surface and tests/docs only; no auth or on-chain behavior changes, and the Bytes32 removal reduces incorrect typechecking risk.

Overview
Replaces the old arrayLength on Array α only with an ArrayLength typeclass so executable Lean code can take byte length from ByteArray, String (utf8ByteSize), and Array α, matching ABI length-word semantics for dynamic types.

Deliberately omits a Bytes32 instance so arrayLength cannot typecheck on arbitrary words (since Bytes32 abbreviates Uint256).

Adds ArrayElementDynamicMemberBytesSmoke with rfl proofs that arrayLength on struct bytes/string members and on (arrayElement ops idx).callData lowers to paramDynamicMemberLength / arrayElementDynamicMemberLength. Commits the generated Solidity property-test stub for CI. Docs now describe member-level arrayLength and why fixed-width words have no length surface.

^{Reviewed by Cursor Bugbot for commit 0a78f9d. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jun 12, 2026 3:56pm