Support projected static composite event payloads

[Th0rgal]

Summary

• add Expr.paramDynamicStaticComposite for static composite fields projected from dynamically encoded tuple parameters
• lower projected static composite event payloads by loading ABI words from the dynamic parameter data region
• allow source-shaped emit "NoteLogged" [txn.withdrawal] in the macro path and add regression coverage

Verification

• git diff --check
• lake build Compiler.CompilationModelFeatureTest
• python3 scripts/generate_print_axioms.py --check
• python3 scripts/check_axioms.py
• lake build Benchmark.Cases.UnlinkXyz.Pool.Compile in verity-benchmark against this local Verity checkout

---

Note

Medium Risk
Touches event ABI/log emission and macro translation logic; incorrect offsets/word loading could silently produce malformed event data/topics even though scope/shape validations and feature tests were updated.

Overview
Enables emit arguments to reference static composite fields projected out of a dynamically-encoded tuple parameter via a new Expr.paramDynamicStaticComposite projection.

Event lowering now accepts these projected sources for static composite event params and encodes them by loading ABI words from the dynamic parameter’s data region (applies to both unindexed payload storage and indexed topic hashing).

Macro translation/typing and validations were updated to recognize and typecheck these projections for emit, and feature tests + proof/analysis utilities were extended to cover the new Expr constructor.

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

[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 4b251a4. Configure here.}

[cursor]

Missing dynamic parent guard in projection function

Medium Severity

paramDynamicStaticCompositeProjection? doesn't verify valueTypeUsesDynamicData param.ty before returning some, unlike the analogous paramDynamicHeadProjection? and paramDynamicMemberProjection? which both include this guard. This means a multi-word static composite field projection from a statically-encoded parent parameter would incorrectly produce an Expr.paramDynamicStaticComposite node, which references a nonexistent {name}_data_offset variable, causing a confusing scope-validation error instead of falling through to the standard translation path.

 

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