Source-shaped dynamic event proof surface (#2000)

[Th0rgal]

Summary

• Adds source-shaped event proof-surface predicates for dynamic/struct ABI event payload declarations
• eventParamSourceShapeProofSupported_of_scalar / eventDefSourceShapeProofSupported_of_scalar keep the existing scalar-event semantic bridge intact and additive
• Smoke examples: dynamic tuples, static structs/tuples, indexed dynamic struct arrays, fixed arrays + ADT-shaped payloads

Part of #2000. Stacked on #2017 (task/1974-reverterror-args).

Note: the word-by-word semantic bridge remains the scalar bridge; this adds the dynamic/struct proof surface without claiming the scalar bridge proves non-scalar log execution.

Test plan

• lake build Verity Contracts Compiler PrintAxioms — Build completed successfully
• scripts/refresh_verification_artifacts.sh — [refresh] PASS
• make check — All checks passed

---

Note

Low Risk
Proof-catalog additions only; existing scalar event emission semantics and bridges are explicitly unchanged.

Overview
Adds additive proof-side predicates in SupportedSpec.lean for ABI event declarations with dynamic/struct payloads, separate from the existing scalar eventEmissionProofSupported bridge (word-by-word log semantics stay scalar-only).

eventParamSourceShapeProofSupported is currently a permissive catalog (true for all represented ParamType constructors). eventDefSourceShapeProofSupported checks all params pass that catalog, at most three indexed params, and eventDefScratchBounded. eventParamSourceShapeProofSupported_of_scalar and eventDefSourceShapeProofSupported_of_scalar show scalar-supported events still satisfy the new surface.

Four rfl smoke EventDef examples (dynamic tuples, static struct tuples, indexed dynamic struct arrays, fixed arrays + ADT) document that non-scalar payload shapes are admitted by the new predicate. PrintAxioms.lean registers the two new theorems and bumps the public theorem count by 2.

^{Reviewed by Cursor Bugbot for commit 22d551a. 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 11:55pm