Add generic Solidity ergonomics to Verity macro

[Th0rgal]

Summary

• add generic modifier declarations and with ... modifier use syntax
• support linked external returns flattened from static ABI composites such as structs and fixed arrays
• add abiEncode projection for static ABI composites used as external-call arguments
• allow event arguments to include inline dynamic-array helper calls

Validation

• lake build
• make check
• benchmark: lake build Benchmark.Cases.UnlinkXyz.Pool.Compile
• benchmark: lake build

---

Note

Medium Risk
Medium risk because it changes the Verity macro’s parsing/typechecking/lowering for functions, externals, and event emission; mistakes could miscompile contracts or weaken validation around external-call ABI shapes.

Overview
Adds Solidity-style modifier declarations plus with ... usage in verity_contract, validating modifier references and lowering modifiers as injected internal calls at the start of function bodies.

Extends linked external-call support to static ABI composite returns (tuples/fixed arrays/structs) by flattening return binders to Yul word counts and tightening try wrapper validation to require Bool + flattened return values; updates related error messages/tests.

Introduces abiEncode for projecting static-ABI composite values into flattened head words when used as external-call arguments, and updates event emission to allow inline dynamic-array helper calls by auto-binding temp arrays before emit.

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

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `compiler-regressions`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```

[Th0rgal]

Fixed the try-wrapper validation finding in a494037: validation now requires the wrapper return list to start with Bool before comparing the flattened tail width, and ExternalCallTryWrapperMissingBoolRejected covers the no-Bool regression through #check_contract.

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit a494037. Configure here.}

[cursor]

Missing newtypeOf recursion in return Yul count

Medium Severity

linkedExternalReturnYulCountForType falls through to _ => 1 for ParamType.newtypeOf, but the translation layer's staticAbiLeafNames? recursively unwraps newtypes via .newtype _ baseType => staticAbiLeafNames? baseType. If an external returns a newtype wrapping a tuple or fixedArray, the validation would count 1 expected Yul value while the macro flattens it into multiple result vars, causing a spurious validation error. All other ParamType.newtypeOf handlers in the codebase (e.g. paramHeadSize, isDynamicParamType) correctly recurse through the base type.

Additional Locations (1)

• Verity/Macro/Translate.lean#L1654-L1655

 

^{Reviewed by Cursor Bugbot for commit a494037. Configure here.}