Add macro event declarations

[Th0rgal]

Summary

• add event_defs declarations to verity_contract
• translate macro event declarations into CompilationModel.events
• cover indexed and unindexed macro event metadata in feature tests

Checks

• lake build Compiler.CompilationModelFeatureTest
• lake build Contracts.Smoke Compiler.CompilationModelFeatureTest Contracts.MacroTranslateInvariantTest
• lake build PrintAxioms
• python3 scripts/generate_print_axioms.py --check
• python3 scripts/check_axioms.py
• git diff --check

---

Note

Medium Risk
Extends the verity_contract macro surface syntax and spec generation to carry event definitions, which may affect downstream compilation/ABI outputs for contracts using the macro. Changes are additive but touch core macro translation paths.

Overview
verity_contract now supports an event_defs section with per-parameter @indexed annotations, and macro translation threads these declarations through parsing/elaboration into CompilationModel.spec.events.

Adds translation support in Verity/Macro/Translate.lean (new EventDecl/EventParamDecl parsing and model term generation) and updates the contract elaborator to pass event declarations into spec generation.

Updates Compiler/CompilationModelFeatureTest.lean with a smoke contract that declares Transfer and asserts the resulting spec carries correct indexed vs unindexed event metadata.

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