Accept struct-parameter projection from ABI-dynamic root (#1832)

[Th0rgal]

Summary

Adds Expr.paramDynamicHeadWord (name : String) (wordOffset : Nat) and routes direct dynamic-tuple parameter leaf projections through it. Closes the single remaining genuinely-open P0 item from umbrella #1760 (see audit comment for why the other two P0 — no existing issue checkboxes were already shipped).

Fixes #1832. Depends on #1841 (param-loader fix) and #1842 (wildcard refactor).

What now works

struct DynamicConfig where
  notes : Array Uint256,   -- makes DynamicConfig ABI-dynamic
  maker : Address

function read (config : DynamicConfig) : Address := do
  return config.maker     -- now lowers to Expr.paramDynamicHeadWord

Before this PR the macro rejected the above with the diagnostic "struct parameter projection from an ABI-dynamic root is not supported; use a static struct parameter or wait for nested-dynamic ABI decoding" (Verity/Macro/Translate.lean:1715).

Implementation

• New Expr constructor Expr.paramDynamicHeadWord (name : String) (wordOffset : Nat) (Compiler/CompilationModel/Types.lean).
• New Yul helpers __verity_param_dynamic_head_word_{calldata,memory}_checked reading data_offset + word_offset * 32 with a calldatasize - 32 upper bound check (Compiler/CompilationModel/DynamicData.lean).
• Helper emission gated on a new contractUsesParamDynamicHeadWord detector (UsageAnalysis.lean), threaded through Dispatch.compileValidatedCore and ValidationCalls.reservedExternalNames.
• New macro resolver paramDynamicHeadProjection? shadow-mirrors paramStructProjectionResolved? but uses structFieldHeadOffset? (the same helper the array case already uses via arrayElementStructProjectionResolved?) to compute the head-word offset. Routing in translatePureExprWithTypes and inferPureExprType checks this resolver first when the param is ABI-dynamic.
• Rejection helpers isParamStructDynamicRootProjection and throwStructDynamicRootProjectionError removed; the non-leaf rejection stays.
• paramDynamicHeadWord case added to every existing Expr traversal: LogicalPurity (pure leaves), UsageAnalysis (4 sites), Validation (3 sites + exprWritesState/exprContainsExternalCall/exprMayContainExternalCall wildcard expansion), ValidationHelpers, ScopeValidation (substantive tuple-shape + wordOffset bounds check), ValidationInterop, ValidationCalls, ExpressionCompile (lowering).

Smoke + invariant + property-test coverage

• Contracts.Smoke.NamedStructDynamicRootLeafProjection replaces the previous rejection #guard_msgs test with an accepted contract.
• Listed in MacroTranslateInvariantTest (spec list, function signature index, selector index) and MacroTranslateRoundTripFuzz (spec list).
• Auto-generated Foundry property stub at artifacts/macro_property_tests/PropertyNamedStructDynamicRootLeafProjection.t.sol.

Test plan

• lake build succeeds (all 105 targets).
• make check passes locally (macro health, IR/Yul identity diff, selector audit, property-test artifacts).
• The previously-rejected shape now compiles end-to-end with the new helper emitted.

Scope

No new axiom or trust surface — the helper is local bytes-reading with a calldatasize - 32 bound check. AUDIT.md / AXIOMS.md / TRUST_ASSUMPTIONS.md unaffected.

docs/INTERPRETER_FEATURE_MATRIX.md deserves a parallel "Param dynamic head word" row alongside the existing "Dynamic struct-array head word"; doc update is queued for a follow-up.

Downstream

verity-benchmark cases/unlink_xyz/pool/Contract.lean carries BLOCKED(verity#1832) markers on the three public ZK entry points (transfer / withdraw / emergencyWithdraw — bodies at UnlinkPool.sol:309-583). Once this PR (and its two prerequisites) reaches the lakefile pin, those markers come down and the entrypoints can be filled in. Foundry differential test against solc-emitted ABI for the full Transaction struct is a follow-up; the current property-test artifact is the baseline that make check enforces.

🤖 Generated with Claude Code

---

Note

Medium Risk
Medium risk: adds a new expression form and Yul helper used in ABI decoding paths; mistakes in head-offset calculation or bounds checks could cause incorrect reads or unexpected reverts for dynamic tuple parameters.

Overview
Adds support for projecting a single-word static leaf field from a struct/tuple parameter whose ABI encoding is dynamic (nested dynamic members), by introducing Expr.paramDynamicHeadWord and routing param.field macro translations through it.

Implements new checked Yul helpers (__verity_param_dynamic_head_word_{calldata,memory}_checked) and emits them only when used via a new contractUsesParamDynamicHeadWord analysis, with corresponding reserved-name handling and compilation/validation traversal updates.

Updates smoke/fuzz/invariant coverage by replacing the prior rejection test with an accepted NamedStructDynamicRootLeafProjection contract and adding the generated Foundry property-test stub.

^{Reviewed by Cursor Bugbot for commit 22a8848. 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 caa4600. Configure here.}

[github-actions]

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