Use hashNote for withdrawal commitment check

[Th0rgal]

Summary

• compare the withdrawal output slot against the modeled hashNote boundary
• keep the recipient cast/check ordering closer to the Solidity _executeWithdrawal body

Verification

• git diff --check
• lake build Benchmark.Cases.UnlinkXyz.Pool.Compile

---

Note

Medium Risk
Changes the withdrawal commitment validation logic and the ordering of recipient casting/checks, which could affect withdrawal acceptance/rejection if the modeled hash does not match the on-chain contract behavior.

Overview
Updates executeWithdrawal in Benchmark/Cases/UnlinkXyz/Pool/Contract.lean to derive the withdrawal commitment hash via hashNote(npk, token, amount) instead of a simple arithmetic combination, and compares the withdrawal output slot against this modeled hash.

Reorders recipient derivation to occur after the npk bounds check, keeping the cast/check sequence closer to the upstream Solidity _executeWithdrawal.

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