Add formal verification tests using Halmos

[hieronx]

No description provided.

[github-actions]

Coverage after merging symbolic-tests into main will be

96.33%

Coverage Report

File	Stmts	Branches	Funcs	Lines	Uncovered Lines
src/adapters
AxelarAdapter.sol	90.91%	83.33%	100%	92.59%	45–46, 55–56
WormholeAdapter.sol	100%	100%	100%	100%
src/common
BaseValuation.sol	100%	100%	100%	100%
GasService.sol	80%	50%	100%	97.65%	101, 103, 105, 107, 109, 111, 113, 115, 117, 120, 122, 124, 127, 129, 131, 133, 135, 137, 139, 142, 85, 87, 89, 91, 93, 95, 97, 99
Gateway.sol	100%	100%	100%	100%
Guardian.sol	90.12%	64.29%	100%	93.88%	153, 153–154, 51–55
MessageDispatcher.sol	97.40%	92.59%	100%	99.12%	64–68
MessageProcessor.sol	95.27%	91.07%	100%	97.70%	191, 51–55, 69
MultiAdapter.sol	100%	100%	100%	100%
PoolEscrow.sol	100%	100%	100%	100%
Root.sol	100%	100%	100%	100%
TokenRecoverer.sol	100%	100%	100%	100%
src/common/factories
PoolEscrowFactory.sol	100%	100%	100%	100%
src/common/libraries
MessageLib.sol	100%	100%	100%	100%
MessageProofLib.sol	100%	100%	100%	100%
PricingLib.sol	100%	100%	100%	100%
RequestCallbackMessageLib.sol	88.64%	50%	100%	100%	106, 141, 38, 57, 77
RequestMessageLib.sol	88.89%	50%	100%	100%	37, 55, 72, 89
src/hooks
BaseTransferHook.sol	78.30%	83.33%	50%	85.29%	103, 107, 111, 115, 120, 124, 154, 178, 45, 87, 91, 95, 99
FreelyTransferable.sol	100%	100%	100%	100%
FreezeOnly.sol	100%	100%	100%	100%
FullRestrictions.sol	100%	100%	100%	100%
RedemptionRestrictions.sol	100%	100%	100%	100%
src/hooks/libraries
UpdateRestrictionMessageLib.sol	89.29%	50%	100%	100%	40, 61, 82
src/hub
Accounting.sol	93.75%	96%	100%	91.53%	114–115, 118–119, 134, 137
Holdings.sol	97.46%	88%	100%	100%	116, 222, 82
Hub.sol	85.27%	44.68%	100%	90.50%	110, 290, 429–430, 433, 433–434, 452, 455, 455–456, 476, 493, 510, 537, 541, 571–572, 572, 572–573, 573, 573, 578, 583, 601, 611, 621, 621, 621, 623, 637, 644–646, 736, 79–80, 80–81, 81–82, 82–83, 83–85
HubHelpers.sol	88.46%	87.50%	90%	88.54%	155–157, 163–165, 215, 239, 244–247, 54–55
HubRegistry.sol	93.51%	79.17%	100%	100%	104, 110, 116, 33, 44
ShareClassManager.sol	100%	100%	100%	100%
src/managers
MerkleProofManager.sol	79.45%	61.11%	88.89%	84.78%	104, 111, 130–131, 131, 131, 133–134, 136–137, 40–41, 44, 54
OnOfframpManager.sol	90.59%	82.14%	100%	94%	132, 52, 63, 67–68, 78, 84, 87
src/managers/decoders
BaseDecoder.sol	75%	100%	75%	75%	43–44
CircleDecoder.sol	0%	100%	0%	0%	11, 16, 20, 22
VaultDecoder.sol	0%	100%	0%	0%	10, 104, 110, 15–16, 22, 28, 34, 40, 46, 52, 58, 64, 69, 75, 80, 86, 9, 92, 98
src/misc
Auth.sol	100%	100%	100%	100%
ERC20.sol	100%	100%	100%	100%
Escrow.sol	56.25%	33.33%	100%	66.67%	15, 17, 21–22, 22, 22, 24
Multicall.sol	83.33%	33.33%	100%	100%	17, 17
Recoverable.sol	100%	100%	100%	100%
ReentrancyProtection.sol	90%	75%	100%	100%	22
src/misc/libraries
ArrayLib.sol	95.83%	75%	100%	100%	26
BitmapLib.sol	100%	100%	100%	100%
BytesLib.sol	90.09%	54.17%	100%	100%	109, 120, 131, 14, 142, 153, 16, 164, 175, 186, 87
CastLib.sol	95.12%	66.67%	100%	100%	31, 7
EIP712Lib.sol	100%	100%	100%	100%
MathLib.sol	92.47%	70.59%	100%	97.06%	33–34, 43, 45, 47, 49, 51
MerkleProofLib.sol	100%	100%	100%	100%
SafeTransferLib.sol	96.97%	92.86%	100%	100%	75
SignatureLib.sol	95.24%	80%	100%	100%	17
StringLib.sol	100%	100%	100%	100%
TransientArrayLib.sol	100%	100%	100%	100%
TransientBytesLib.sol	100%	100%	100%	100%
TransientStorageLib.sol	100%	100%	100%	100%
src/spoke
BalanceSheet.sol	99.45%	96.55%	100%	100%	59
ContractUpdater.sol	100%	100%	100%	100%
ShareToken.sol	93.51%	66.67%	94.12%	98.04%	101, 113, 146, 33
Spoke.sol	96.32%	86.81%	100%	99.56%	124, 124–125, 125, 127, 331, 341–343, 98, 98–99, 99
src/spoke/factories
TokenFactory.sol	92%	50%	100%	94.74%	24–25
src/spoke/libraries
UpdateContractMessageLib.sol	88.89%	50%	100%	100%	110, 40, 62, 86
src/valuations
IdentityValuation.sol	100%	100%	100%	100%
src/vaults
AsyncRequestManager.sol	94.29%	82.35%	93.48%	98.43%	194, 197, 200, 203, 214, 226, 231, 250, 257, 290, 324, 438, 443, 482, 484, 76–77, 90–91
AsyncVault.sol	96.15%	83.33%	94.44%	98.15%	148, 49
BaseVaults.sol	92.61%	80.77%	95.35%	94.03%	126, 139, 246, 319–320, 406–407, 87–88, 88, 88–90
SyncDepositVault.sol	100%	100%	100%	100%
SyncManager.sol	83.19%	70%	87.50%	85.71%	106–107, 109, 161, 181–182, 227–228, 59–61, 63, 63, 63, 65, 70, 75
VaultRouter.sol	91.16%	53.85%	100%	98.97%	105, 108–109, 122, 122–123, 123, 138–139, 158, 158, 175, 221
src/vaults/factories
AsyncVaultFactory.sol	88.89%	50%	100%	92.86%	36, 46
SyncDepositVaultFactory.sol	90.91%	50%	100%	94.44%	45, 58