Add Halmos symbolic verification for core contracts

[xhad]

Summary

Adds Halmos symbolic verification for the Chamber protocol contracts, covering key invariants on Board, Chamber, Wallet, Registry, and ERC4626 vault behavior.

Symbolic tests (15 total)

Contract	Property verified
Board	Linked list stays sorted descending after two inserts
Board	Delegate + undelegate conserves node amount
Board	Circuit breaker blocks reentrant delegate
Chamber	Holder delegation never exceeds share balance
Chamber	Board node amount matches holder delegation
Chamber	Partial undelegate updates holder and node consistently
Wallet	Submitted transaction stores keccak256(calldata)
Wallet	Execution reverts on calldata hash mismatch
Registry	Valid seat counts register a new chamber
Registry	Invalid seat counts cannot create a chamber
Registry	Non-admin cannot update implementation pointer
Registry	Admin can update implementation pointer
Registry	First chamber for an asset registers it in the index
Vault	Empty vault previewDeposit scales by decimals offset
Vault	Empty vault deposit mints shares at offset multiplier

How to run locally

cd contracts
pip install -r fv-requirements.txt
make halmos

Infrastructure

• halmos-cheatcodes dependency (submodule)
• contracts/fv-requirements.txt pins halmos==0.3.3
• make halmos / make ci-halmos targets
• .github/workflows/halmos.yaml CI job on contract changes

Notes

• Halmos does not support vm.expectRevert(); revert checks use low-level call + assertFalse(success).
• ERC4626 convertToAssets / withdraw roundtrip tests were intentionally omitted — they introduce nonlinear division that causes Halmos solver timeouts. Those properties remain covered by test/unit/Vault.t.sol fuzz/unit tests.
• Symbolic tests are named symbolic* and are excluded from normal forge test runs (Halmos runs them separately).