Add Polygon AgglayerBridge benchmark

[fricoben]

Summary

• Adds a Polygon AgglayerBridge benchmark for successful claim membership plus nullifier consumption.
• Models claimAsset, claimMessage, _verifyLeaf, _verifyLeafAndSetNullifier, _setAndCheckClaimed, global-index decoding, and bitmap nullifier handling.
• Adds reference proofs for the public claim tasks, the shared nullifier helper, and direct corollaries combining both into leaf-validity plus nullifier-consumption statements.

Proof shape

• Public claim theorems prove that a successful claim validates the modeled leaf against an accepted global exit root and successfully reaches _setAndCheckClaimed.
• setAndCheckClaimed_consumes proves successful _setAndCheckClaimed execution flips the correct bitmap word and consumes the source-network/leaf-index nullifier.
• claimAsset_valid_leaf_and_nullifier_consumed_direct and claimMessage_valid_leaf_and_nullifier_consumed_direct compose those facts into the direct invariant.
• No sorry or axiom is used in the Agglayer benchmark files.

Modeling notes

• Dynamic bytes metadata is represented as a metadataHash parameter.
• The 32-step Merkle proof loop is summarized by a deterministic word combiner while preserving the branch structure and required checks.
• Token/message side effects after nullifier consumption are elided because the invariant is about accepted leaf membership and single-use nullifier behavior.
• Calls through helpers with Array Uint256 parameters are inlined in claim functions due to the current Verity macro gap tracked in verity_contract cannot call internal helpers with Array parameters verity#1824.

Validation

• python3 scripts/validate_manifests.py
• lake build Benchmark.Cases.Polygon.AgglayerBridge.Proofs
• lake build
• Generated task files fail only at intentional exact ?_ placeholders when checked directly.